Derive the self converge-receipt verdict from the knob⊓revision meet (close the empty-observation narrow)

dag/gunbc/fleet_converge_cli.dag

@@ -25,7 +25,7 @@ import gunbc.host_converge_slice1 {
 }
 import gunbc.host_runner_memory_provision { runner_memory_host_converge }
 import gunbc.host_runner_memory_cap_verify { runner_memory_cap_verify_run }
-import gunbc.host_converge { fleet_converge_policy, find_by_identity, converge_verdict, converge_verdict_label }
+import gunbc.host_converge { fleet_converge_policy, find_by_identity, converge_verdict, converge_verdict_label, converge_verdict_meet }
 import gunbc.fleet_intent_network {
   operator_host_srv1,
   operator_host_srv2,
@@ -370,66 +370,115 @@ fn converge_cli_publish(out: ConvergeCliOutput, resolved: String, revision_line:
   }
 }
 
-// Operator verdict join 1 (2026-08-09): the self route is where a host READS the
-// desired ref. The knob receipt alone cannot claim convergence while the deployed tree
-// is not at the admitted revision — revision drift or an unobserved ref demotes the
-// output to not-converged with the typed cause, and the published receipt carries the
-// revision cell as its own line so the collector (join 5) sees BOTH cells. Drifted
-// names both sides (desired AND local): tree-sync is the catch-up realization, and its
-// safe form is a compare-and-swap needing the prior. The repo path is the ONE
-// host_layout convention row (byte-identical across enrolled hosts per its note).
-fn converge_cli_revision_gate(out: ConvergeCliOutput, standing: FleetRevisionStanding) -> ConvergeCliOutput {
+// Operator verdict join 1 (2026-08-09; construction rework 2026-08-10, the empty-observation
+// narrow §5): the self route is where a host READS the desired ref, and the knob receipt
+// alone cannot claim convergence while the deployed tree is not at the admitted revision.
+// converge_cli_receipt_join_revision MEETS the knob verdict with the revision standing on
+// the ConvergeVerdict lattice (converge_verdict_meet, Absent < Drifted < VerdictConverged)
+// BEFORE the receipt line is rendered, so verdict=converged on the published converge-receipt
+// line is only constructable when the revision was observed AND matched. RevisionUnobserved
+// pulls the joint to Absent — an applied=0/drifted=0 knob run that never observed the desired
+// revision can no longer render "converged" (bottom-as-ignorance is no longer written as
+// bottom-as-answer). The collector (join 5, fleet_receipt_collector parse_converge_receipt_line)
+// reads THIS one joint verdict off the converge-receipt line; converge_cli_revision_line
+// carries the revision OBSERVATION as evidence (observed=/drift/unobserved) and no longer a
+// second verdict= token, so the receipt holds exactly one verdict and the two cells cannot
+// disagree. This REPLACES the former bool-only converge_cli_revision_gate, which demoted the
+// converged flag while leaving the rendered line saying verdict=converged — the dual
+// representation the collector inherited. Drifted names both sides (desired AND local):
+// tree-sync is the catch-up realization, its safe form a compare-and-swap needing the prior.
+// The repo path is the ONE host_layout convention row.
+// DECLARED IMPRECISION, next-rung item (review, 2026-08-10). RevisionUnobserved maps to
+// Absent, but converge_verdict (host_converge) already mints Absent for "subject not present
+// on the host". So the isolated verdict=absent TOKEN conflates two states with OPPOSITE
+// remedies — install/converge the subject, vs fix the desired-ref observation (the srv1 b1
+// git-credential defect — different lane). This is the sentinel review 50817 warned about on
+// parse_converge_verdict_label, one level down in the value rather than the decode. It is
+// fail-closed, not fail-open (both fold not-converged, so acceptance correctly fails and the
+// collector is never misled), and the receipt as a WHOLE disambiguates: the self path always
+// emits the converge-revision evidence line beside this one, so verdict=absent + "unobserved
+// cause=" is the revision case and verdict=absent + "observed=<hex>" is the subject-absent
+// case. Only the isolated line-1 token is ambiguous, and only to a human remedy-router who
+// ignores line 2. A precise fix is a distinct Unobserved verdict, DEFERRED with the same
+// reasoning as the GitObjectId-in-VerdictConverged trigger below: it widens the shared
+// ConvergeVerdict enum that knob-only convergence uses and would never emit. That the enum
+// cannot carry this without burdening an unrelated consumer is itself the dual-representation
+// smell one rung up (the enum doing two jobs) — named here, not fixed here.
+fn converge_cli_revision_verdict(standing: FleetRevisionStanding) -> ConvergeVerdict {
   match standing {
-    RevisionConverged { revision: _ } => out
+    RevisionConverged { revision: _ } => VerdictConverged
+    RevisionDrifted { desired: _, local: _ } => Drifted
+    RevisionUnobserved { cause: _ } => Absent
+  }
+}
+
+fn converge_cli_receipt_join_revision(r: ConvergeCliReceipt, standing: FleetRevisionStanding) -> ConvergeCliReceipt {
+  ConvergeCliReceipt {
+    host: r.host,
+    applied: r.applied,
+    drifted: r.drifted,
+    verdict: converge_verdict_meet(a: r.verdict, b: converge_cli_revision_verdict(standing: standing)),
+    reason: r.reason,
+  }
+}
+
+fn converge_cli_revision_reason(standing: FleetRevisionStanding) -> String? {
+  match standing {
+    RevisionConverged { revision: _ } => none
     RevisionDrifted { desired: d, local: l } =>
-      ConvergeCliOutput {
-        line: out.line,
-        converged: false,
-        reason: Present {
-          value: join([
-            "gunbc converge: revision drift — desired ",
-            git_object_id_wire_hex(oid: d) as String,
-            ", local tree at ",
-            git_object_id_wire_hex(oid: l) as String,
-            "; tree-sync is the catch-up realization",
-          ], ""),
-        },
+      Present {
+        value: join([
+          "gunbc converge: revision drift — desired ",
+          git_object_id_wire_hex(oid: d) as String,
+          ", local tree at ",
+          git_object_id_wire_hex(oid: l) as String,
+          "; tree-sync is the catch-up realization",
+        ], ""),
       }
     RevisionUnobserved { cause: c } =>
-      ConvergeCliOutput {
-        line: out.line,
-        converged: false,
-        reason: Present { value: concat("gunbc converge: desired revision unobserved — ", c) },
-      }
+      Present { value: concat("gunbc converge: desired revision unobserved — ", c) }
   }
 }
 
 fn converge_cli_revision_line(standing: FleetRevisionStanding) -> String {
   match standing {
     RevisionConverged { revision: r } =>
-      concat("converge-revision verdict=converged revision=", git_object_id_wire_hex(oid: r) as String)
+      concat("converge-revision observed=", git_object_id_wire_hex(oid: r) as String)
     RevisionDrifted { desired: d, local: l } =>
       join([
-        "converge-revision verdict=drifted desired=",
+        "converge-revision drift desired=",
         git_object_id_wire_hex(oid: d) as String,
         " local=",
         git_object_id_wire_hex(oid: l) as String,
       ], "")
-    RevisionUnobserved { cause: c } => concat("converge-revision verdict=unobserved cause=", c)
+    RevisionUnobserved { cause: c } => concat("converge-revision unobserved cause=", c)
   }
 }
 
 fn converge_cli_output(host: String) -> ConvergeCliOutput {
-  let out = converge_cli_output_with_verify(host: host, verify_only: false)
   if host == "self" {
+    let resolved = converge_cli_resolve_self(host: host)
+    let r = converge_cli_run(host: resolved)
     let standing = fleet_revision_standing(repo: srv1_gunbc_repo_root)
+    let joint = converge_cli_receipt_join_revision(r: r, standing: standing)
+    let base_reason = match r.reason {
+      Present { value: cause } => Present { value: converge_cli_refusal_message(cause: cause) }
+      Absent => none
+    }
     converge_cli_publish(
-      out: converge_cli_revision_gate(out: out, standing: standing),
-      resolved: converge_cli_resolve_self(host: host),
+      out: ConvergeCliOutput {
+        line: converge_cli_receipt_line(r: joint),
+        converged: converge_cli_receipt_converged(r: joint),
+        reason: match converge_cli_revision_reason(standing: standing) {
+          Present { value: why } => Present { value: why }
+          Absent => base_reason
+        },
+      },
+      resolved: resolved,
       revision_line: converge_cli_revision_line(standing: standing),
     )
   } else {
-    out
+    converge_cli_output_with_verify(host: host, verify_only: false)
   }
 }
 

dag/gunbc/host_converge.dag

@@ -136,6 +136,21 @@ fn converge_verdict_label(v: ConvergeVerdict) -> String {
   }
 }
 
+// The convergence verdict lattice, meet: Absent < Drifted < VerdictConverged. A host's
+// verdict cannot outrank the WEAKEST evidence that grounds it — so a knob verdict is met
+// with the revision standing before it is reported, and any not-converged evidence pulls
+// the joint below converged. This is the construction that makes an empty-observation
+// narrow unwritable: verdict=converged is only reachable when BOTH inputs are converged
+// (fleet_converge_cli converge_cli_receipt_join_revision), never from applied=0/drifted=0
+// alone when the desired revision was never observed.
+fn converge_verdict_meet(a: ConvergeVerdict, b: ConvergeVerdict) -> ConvergeVerdict {
+  match a {
+    Absent => Absent
+    Drifted => match b { Absent => Absent  _ => Drifted }
+    VerdictConverged => b
+  }
+}
+
 type ConvergeSlice
   = GunbcSlice
   | RunnerSlice

dag/test/claim/fleet_converge_cli_witness_test.dag

@@ -131,35 +131,50 @@ test fn witness_converge_cli_output_projects_receipt_and_exit_signal() -> Bool {
 }
 
 
-// Join 1 (operator verdict): the revision cell gates the self route. Converged passes
-// the knob output through untouched; Drifted demotes to not-converged carrying BOTH
-// revisions (the catch-up realization needs the prior); Unobserved demotes with the
-// typed cause and is never satisfied. The rendered receipt line carries the cell for
-// the collector, one verdict token per arm.
-test fn witness_revision_gate_demotes_drift_and_unobserved_never_converged_passthrough() -> Bool {
+// Join 1 (operator verdict) — construction rework 2026-08-10, the §5 empty-observation
+// narrow. converge_cli_receipt_join_revision MEETS the knob verdict with the revision
+// standing (converge_verdict_meet), and the RENDERED converge-receipt line is derived from
+// that joint — so a knob run that converged its knobs but never observed the desired
+// revision renders verdict=absent on line 1, NOT converged. This is the exact srv1 defect
+// (applied=0 drifted=0 verdict=converged persisted while the revision was unobserved, and
+// the collector then folded it as converged). RED both directions: an unobserved/drifted
+// standing must never render verdict=converged on the receipt line, and a converged standing
+// must pass the knob verdict through. The end-to-end clause feeds the joint line back through
+// the collector's own parser (parse_converge_receipt_line) and asserts the collector reads
+// NOT-converged — the narrow is closed at the seam the collector actually reads. Also asserts
+// the converge-revision line now carries the OBSERVATION as evidence (observed=/drift/
+// unobserved), never a second verdict= token, so the receipt holds exactly one verdict.
+test fn witness_self_receipt_verdict_is_joint_never_false_converged() -> Bool {
   let a = revision_fixture_oid(hex: "aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa")
   let b = revision_fixture_oid(hex: "bbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbb")
-  let out = ConvergeCliOutput { line: "converge-receipt host=srv1 applied=1 drifted=0 verdict=converged", converged: true, reason: none }
-  let gated_ok = converge_cli_revision_gate(out: out, standing: RevisionConverged { revision: a })
-  let gated_drift = converge_cli_revision_gate(out: out, standing: RevisionDrifted { desired: a, local: b })
-  let gated_unobs = converge_cli_revision_gate(out: out, standing: RevisionUnobserved { cause: "ls-remote refused: no route" })
-  gated_ok.converged
-    && !gated_drift.converged
-    && match gated_drift.reason {
-      Present { value: why } =>
-        string_contains(s: why, pattern: "revision drift")
-          && string_contains(s: why, pattern: "aaaaaaaa")
-          && string_contains(s: why, pattern: "bbbbbbbb")
-      _ => false
-    }
-    && !gated_unobs.converged
-    && match gated_unobs.reason {
-      Present { value: why } => string_contains(s: why, pattern: "unobserved")
-      _ => false
+  // knob run converged (nothing to apply) — the srv1 shape
+  let knob = ConvergeCliReceipt { host: "srv1", applied: 0, drifted: 0, verdict: VerdictConverged, reason: none }
+  let joint_ok = converge_cli_receipt_join_revision(r: knob, standing: RevisionConverged { revision: a })
+  let joint_drift = converge_cli_receipt_join_revision(r: knob, standing: RevisionDrifted { desired: a, local: b })
+  let joint_unobs = converge_cli_receipt_join_revision(r: knob, standing: RevisionUnobserved { cause: "ls-remote refused: no route" })
+  // revision converged: knob verdict passes through -> converged, line says verdict=converged
+  converge_verdict_label(v: joint_ok.verdict) == "converged"
+    && converge_cli_receipt_converged(r: joint_ok)
+    && string_contains(s: converge_cli_receipt_line(r: joint_ok), pattern: "verdict=converged")
+    // revision drift: joint demotes to drifted, line does NOT say converged
+    && converge_verdict_label(v: joint_drift.verdict) == "drifted"
+    && !converge_cli_receipt_converged(r: joint_drift)
+    && !string_contains(s: converge_cli_receipt_line(r: joint_drift), pattern: "verdict=converged")
+    // revision unobserved: joint demotes to absent, line says absent NOT converged (srv1 narrow, closed)
+    && converge_verdict_label(v: joint_unobs.verdict) == "absent"
+    && !converge_cli_receipt_converged(r: joint_unobs)
+    && string_contains(s: converge_cli_receipt_line(r: joint_unobs), pattern: "verdict=absent")
+    && !string_contains(s: converge_cli_receipt_line(r: joint_unobs), pattern: "verdict=converged")
+    // end-to-end: the collector's OWN parser, fed the joint unobserved line, reads not-converged
+    && match parse_converge_receipt_line(line: converge_cli_receipt_line(r: joint_unobs)) {
+      Present { value: parsed } => !converge_cli_receipt_converged(r: parsed)
+      Absent => false
     }
-    && string_contains(s: converge_cli_revision_line(standing: RevisionConverged { revision: a }), pattern: "verdict=converged")
-    && string_contains(s: converge_cli_revision_line(standing: RevisionDrifted { desired: a, local: b }), pattern: "verdict=drifted")
-    && string_contains(s: converge_cli_revision_line(standing: RevisionUnobserved { cause: "x" }), pattern: "verdict=unobserved")
+    // the revision line carries the observation as evidence, never a second verdict= token
+    && string_contains(s: converge_cli_revision_line(standing: RevisionConverged { revision: a }), pattern: "observed=")
+    && string_contains(s: converge_cli_revision_line(standing: RevisionDrifted { desired: a, local: b }), pattern: "drift desired=")
+    && string_contains(s: converge_cli_revision_line(standing: RevisionUnobserved { cause: "x" }), pattern: "unobserved cause=")
+    && !string_contains(s: converge_cli_revision_line(standing: RevisionUnobserved { cause: "x" }), pattern: "verdict=")
 }
 
 fn revision_fixture_oid(hex: String) -> GitObjectId {