Actuate BMC fan convergence with typed rollback

dag/gunbc/ci_fleet.dag

@@ -144,6 +144,7 @@ data gunbc_ci_host_memory_deferral_disposition: Disposition = Scaffold {
 data gunbc_ci_host: ComputeHost = ComputeHost {
   identity: gunbc_ci_host_identity,
   baseboard: none,
+  bmc_intent: none,
   processors: [CpuProcessor { cpu: gunbc_ci_cpu }],
   memory: [MemoryDevice { capacity: byte_size(134217728000), memory_kind: Dram, bandwidth: none }],
   storage: [],
@@ -168,4 +169,3 @@ data gunbc_ci_fleet_offer: ComputeOffer = ComputeOffer {
   available_window: AvailabilityWindow { open: "always-open", close: none },
   cost_quote: none,
 }
-

dag/gunbc/host_effect_realize.dag

@@ -1131,6 +1131,7 @@ fn provision_build_cache_arch_unknown_host_fixture() -> ComputeHost {
   ComputeHost {
     identity: srv1_host.identity,
     baseboard: none,
+    bmc_intent: none,
     processors: [],
     memory: [],
     storage: [],

dag/gunbc/host_phase_status.dag

@@ -7,8 +7,6 @@ import std.decl_ref { DeclarationRef, WholeDeclaration }
 import gunbc.host_standup {
   HostStandupStep,
   PhaseDisposition,
-  ModeledCompose,
-  DeclaredGap,
   host_standup_spine,
 }
 import gunbc.host_standup_assimilation_deduction { srv3_post_install_actuation_verdict }
@@ -26,9 +24,9 @@ import gunbc.fleet_intent_network { operator_host_srv1, operator_host_srv2, oper
 import product.placement_supply { HostIdentity }
 import std.measure { millisecond }
 
-data host_phase_status_authority_note: String = "THE per-(host x phase) status axis for the host-standup spine. It exists because the spine could describe itself but not its RELATIONSHIP TO THE LIVE FLEET: every phase carried a PhaseDisposition (is there a modeled authority?) and nothing carried an observation (does this host actually agree with it?). Answering 'where does subsumption stand' therefore meant a session reconstruction — hand ssh probes, prose transcription — and the answer went stale the moment it was written. Two axes, kept ORTHOGONAL on purpose, because collapsing them is the state-space conflation this lane keeps paying for: the MODELED axis is PhaseDisposition, a property of the phase, the same for every host; the LIVE axis is std.upsert_decision.ObservationVerdict, a property of the (host, phase) CELL. A phase can be fully modeled AND Inaccessible on a given host — that is exactly srv1/srv2 for the build-cache phase today — and a single fused enum could not say it. Note what is NOT minted here: no Converged|Diverged|Unreachable|Unmodeled verdict of our own. ObservationVerdict already carries Converged/Absent/Drifted/Conflict/Inaccessible/UnknownRefused, which is STRICTLY FINER on the diverged and unreachable axes, and it is already consumed by twelve modules including host_standup itself; a parallel four-arm verdict beside it would be the §3 nickname, duplicated again in everything derived from it. 'Unmodeled' is likewise not an observation and does not become a verdict arm — it stays on PhaseDisposition, carried on the cell beside the observation and derived from the spine, never authored. CORRECTION, found by execution 2026-07-25: the cell was FIRST written as a SUM (StatusUnmodeled | StatusObserved), which forced the two axes to be mutually exclusive and made the fold discard the observation on any DeclaredGap phase. The witness caught it immediately, because the single cell that HAS a live producer today is (srv3, prefix:os-install-actuated) — a DeclaredGap phase — so live-observation coverage computed as 0 while a real Converged verdict sat one branch away. The sum was the very conflation this note claims to avoid, written into the type by the same hand that wrote the warning. The cell is now a PRODUCT of both axes, which also gives the lane a state it could not previously say: observed Converged on an unmodeled phase means the host is in the desired condition by means the model cannot reproduce — true of srv3's OS install, and exactly the kind of fact that should never round to either 'modeled' or 'gap'."
+data host_phase_status_authority_note: String = "THE per-(host x phase) status axis for the host-standup spine. Two axes stay orthogonal: PhaseDisposition is the shared model state, while std.upsert_decision.ObservationVerdict is the per-host live state. PhaseDisposition is a PRODUCT of authorities and typed gaps, so a partial phase can truthfully carry comparison logic while still refusing an absent observer or actuator. A cell is model-complete only when it has at least one authority and zero gaps. It may independently be Converged, Drifted, Inaccessible, or UnknownRefused. No second BMC- or host-specific verdict is introduced; both control planes reuse ObservationVerdict. Missing producers remain UnknownRefused, and a partial-but-observed-Converged cell still records reproducibility work rather than rounding green."
 
-data host_phase_cell_grain_note: String = "The cell is keyed by (host, phase_label) and NOT by (host, phase) structurally, because phase_label is already the spine's own stable identity for a step (it is what the gap ledger keyed on, what the refusal strings name, and what an operator reads). Keying on the label keeps ONE identity for a phase across the spine, this matrix, and every refusal message, rather than introducing a second notion of phase identity that could disagree with the first. key_of returns identity, never content (membership_reconcile's R2 contract): a cell whose STATUS changes is Modified — the same cell re-derived — not Removed+Added, which would read as a host leaving and rejoining the fleet."
+data host_phase_cell_grain_note: String = "The cell is keyed by (host, phase_label) and NOT by (host, phase) structurally, because phase_label is the spine's stable identity for a step: it keys the derived gap projection, refusal strings, and operator view. key_of returns identity, never content (membership_reconcile's R2 contract): a cell whose status changes is Modified, not Removed+Added."
 
 type HostPhaseCell {
   host: HostIdentity
@@ -81,11 +79,17 @@ fn host_phase_cell_verdict(c: HostPhaseCellStatus) -> ObservationVerdict {
   host_phase_verdict_from(observation: c.observation)
 }
 
-fn host_phase_cell_is_modeled(c: HostPhaseCellStatus) -> Bool {
-  match c.disposition {
-    ModeledCompose { authorities: _ } => true
-    DeclaredGap { interim_realization: _, refusal: _ } => false
-  }
+fn host_phase_cell_is_model_complete(c: HostPhaseCellStatus) -> Bool {
+  c.disposition.authorities.length() > 0
+    && c.disposition.gaps.length() == 0
+}
+
+fn host_phase_cell_has_authority(c: HostPhaseCellStatus) -> Bool {
+  c.disposition.authorities.length() > 0
+}
+
+fn host_phase_cell_has_model_gap(c: HostPhaseCellStatus) -> Bool {
+  c.disposition.gaps.length() > 0
 }
 
 fn host_phase_cell_has_live_producer(c: HostPhaseCellStatus) -> Bool {
@@ -143,7 +147,7 @@ fn host_phase_cell_key_eq(a: String, b: String) -> Bool {
 }
 
 fn host_phase_status_eq(a: HostPhaseCellStatus, b: HostPhaseCellStatus) -> Bool {
-  let modeled_agrees = host_phase_cell_is_modeled(c: a) == host_phase_cell_is_modeled(c: b)
+  let modeled_agrees = host_phase_cell_is_model_complete(c: a) == host_phase_cell_is_model_complete(c: b)
   let verdict_agrees = observation_verdict_eq(
     a: host_phase_cell_verdict(c: a),
     b: host_phase_cell_verdict(c: b),
@@ -188,17 +192,18 @@ fn host_phase_desired(hosts: List<HostIdentity>) -> List<HostPhaseCellStatus> {
   )
 }
 
-data host_phase_desired_disposition_note: String = "Desired pins BOTH axes to their end state, not just the verdict: a modeled authority AND an observed Converged. Pinning only the verdict would make a DeclaredGap phase whose host happens to be Converged compare equal to desired — which is exactly srv3 and prefix:os-install-actuated today, a host that IS installed while the actuation that installed it is not reproducible. That cell is real remaining work (the model cannot rebuild the host), so it must produce a hunk; a desired row that ignored the disposition would silently retire it."
+data host_phase_desired_disposition_note: String = "Desired pins BOTH axes to their end state: one-or-more modeled authorities with zero gaps, plus an observed Converged verdict. Pinning only the verdict would make a partial phase whose host happens to be Converged compare equal to desired, silently retiring work that the model cannot reproduce."
 
 fn host_phase_desired_disposition() -> PhaseDisposition {
-  ModeledCompose {
+  PhaseDisposition {
     authorities: [
       DeclarationRef {
         module_path: "gunbc.host_phase_status",
         decl_name: "host_phase_desired_disposition",
         field: WholeDeclaration,
       },
-    ]
+    ],
+    gaps: [],
   }
 }
 
@@ -249,13 +254,17 @@ fn host_phase_converged_cell_count(hosts: List<HostIdentity>) -> Int {
 data host_phase_finished_note: String = "FINISHED is both axes at their end state — a modeled authority AND an observed Converged — and it is deliberately stricter than converged. A host that is in the desired condition by unmodeled means is not finished: nothing can rebuild it, so the next host repeats the toil, which is the entire cost this lane exists to remove. srv3's OS install is that cell today. Counting it as done would make the lane's own progress number flatter than the truth in exactly the direction that feels good."
 
 fn host_phase_cell_is_finished(c: HostPhaseCellStatus) -> Bool {
-  host_phase_cell_is_modeled(c: c) && host_phase_cell_is_converged(c: c)
+  host_phase_cell_is_model_complete(c: c) && host_phase_cell_is_converged(c: c)
 }
 
 fn host_phase_finished_cell_count(hosts: List<HostIdentity>) -> Int {
   filter(host_fleet_phase_matrix(hosts: hosts), c => host_phase_cell_is_finished(c: c)).length()
 }
 
-fn host_phase_unmodeled_count(hosts: List<HostIdentity>) -> Int {
-  filter(host_fleet_phase_matrix(hosts: hosts), c => !host_phase_cell_is_modeled(c: c)).length()
+fn host_phase_model_incomplete_count(hosts: List<HostIdentity>) -> Int {
+  filter(host_fleet_phase_matrix(hosts: hosts), c => !host_phase_cell_is_model_complete(c: c)).length()
+}
+
+fn host_phase_model_gap_cell_count(hosts: List<HostIdentity>) -> Int {
+  filter(host_fleet_phase_matrix(hosts: hosts), c => host_phase_cell_has_model_gap(c: c)).length()
 }