Floor resolve realization: identity-join obligation roster (0B)

dag/gunbc/ci_materialization.dag

@@ -20,6 +20,9 @@ import extdeps.cache.materialization {
 import extdeps.cache.sccache { sccache_local_facts, sccache_local_id }
 import v2.workflow.ci_release_build_emit { ci_release_build_script }
 import extdeps.github.actions { Workflow, Job, Step, RunStep, UsesStep }
+import gunbc.floor_materialization { floor_entry_walk_memo_provider_id }
+import v2.std.algebra { any, for_all }
+import std.measure { Nanosecond, nanosecond, nanosecond_count }
 
 
 data ci_materialization_note: String = "The worked example the ladder was built for (operator, 2026-07-08): CI emits shell which runs the gunbc binary, and the runs in shell are one frame above the runs in the binary — not fundamentally different, since both are emitted by the same program. This module models the emitted GitHub Actions workflow as a frame tree (workflow = isolated children; each job = a shared-state frame of steps), extracts every RunStep script as a FrameDemand at its site, and declares the cache providers that discharge the obligations the ladder finds. The flagship: the release build script is demanded by THREE sibling jobs (ci, ci_regen, rust_tests warm) whose LCA is the workflow isolation boundary — unrewireable redundancy, so it MUST be discharged by a covering store-tier provider; that provider is the sccache row below, and the shell fragment that realizes it in the emitted ci.yml is DERIVED from this module (ci_sccache_provider_shell_injection), so deleting the provider row would orphan the injection, and deleting the injection while the row stands is drift the witness reds. Grain honesty: identity is the step's run-script string — deploy scripts EMBED the release build script as a superset string and do not group with it at this grain; sub-step decomposition arrives when demands derive from the DependencyView rather than emitted argv (the forward-wiring thread). UsesStep actions are foreign computations and carry no demand row yet; their caching (actions/cache) is itself a provider to model when uses-grain demands land."
@@ -172,7 +175,199 @@ data ci_floor_resolve_receipt_path: String = "target/floor-resolve-receipt.txt"
 
 data ci_floor_admission_capture_resolve_receipt_note: String = "RECEIPT 7 — CONSCIOUS RAISING 1 -> 2 (2026-07-31, first capture placement): the production WalkPlan run with the old declaration refused exactly `floor resolve count 2 differs from declared 1` and wrote target/floor-resolve-receipt.txt with `resolves_total=2`, `resolve_ms_total=64486`. The then-ordinary first-batch capture_tested_subject claim was one new entry class whose closure escaped the compile anchor. The two non-heavy success stages use a separate entry and may each resolve it; those resolves belong to the attempt-scoped on-success receipt, not the ordinary-floor count. This was the empirical law above operating as designed, not a guessed increment. The same red run proved the safety boundary: finalization refusal left `0 of 2` success stages run. Receipt 8 records why the capture placement and this temporary raise were later retired."
 
-data ci_floor_declared_resolve_count: Nat = 2
+data ci_floor_declared_resolve_count_obligation_note: String = "SEMANTICS (shared CI floor item 0B, operator ruling 2026-08-04): this row names the CLOSED UNIVERSE of semantic resolve OBLIGATIONS the floor roster structurally owes each run — compile-anchor-whole-tree plus native-bundle-escaping-entry — NOT the count of physical cold resolves (resolve_nanos > 0). THE LAW (single authority here, observed by claim_executor, transported by ci_floor_plan only): expected obligation identities == observed realization obligation identities. Warm shared-pool satisfaction is SatisfiedFromSharedPool with provider + receipt, never absence. cold_resolves_total in target/floor-resolve-receipt.txt is observational only. STANDING CONSTRAINT: stays at 2 until identity-based finalization REPLACES it via a conscious roster change in the PR that adds or removes an escaping entry class."
+
+data ci_floor_resolve_obligation_authority_note: String = "AUTHORITY SPLIT (0B): gunbc.ci_materialization owns ci_floor_expected_resolve_obligations and resolve_realization_finalization_holds. claim_executor records ResolveRealization observations at reuse sites using the same variant names as ResolveRealization (ColdResolvePerformed | SatisfiedFromSharedPool) and joins observed rows to the obligation population transported in WalkPlan.finalization.expected_resolve_obligations — no HAND-Rust subject literals, no timing-derived disposition. ci_floor_plan transports ci_floor_expected_resolve_obligations() unchanged into FloorFinalization only. Dissolve-on: witness-realization P4 decodes modeled .dag observations instead of seed re-authoring."
+
+type ResolveObligationIdentity
+  = CompileAnchorWholeTree
+  | NativeBundleEscapingEntry
+
+type ResolveObligationSubject {
+  entry: String
+  function: String
+}
+
+type ResolveObligation {
+  identity: ResolveObligationIdentity
+  subject: ResolveObligationSubject
+}
+
+data compile_anchor_obligation_subject: ResolveObligationSubject = ResolveObligationSubject {
+  entry: "dag/tools/floor_effect_gate_witness.dag",
+  function: "dag_compile_clean_gate_passes",
+}
+
+data native_bundle_obligation_subject: ResolveObligationSubject = ResolveObligationSubject {
+  entry: "src/v2/test/claim/execution/native_selected_witness_bundle_production.dag",
+  function: "native_selected_logic_production_spec",
+}
+
+fn expected_obligation(id: ResolveObligationIdentity) -> ResolveObligation {
+  match id {
+    CompileAnchorWholeTree => ResolveObligation {
+      identity: CompileAnchorWholeTree,
+      subject: compile_anchor_obligation_subject,
+    }
+    NativeBundleEscapingEntry => ResolveObligation {
+      identity: NativeBundleEscapingEntry,
+      subject: native_bundle_obligation_subject,
+    }
+  }
+}
+
+fn ci_floor_expected_resolve_obligations() -> List<ResolveObligation> {
+  [
+    expected_obligation(id: CompileAnchorWholeTree),
+    expected_obligation(id: NativeBundleEscapingEntry),
+  ]
+}
+
+fn ci_floor_expected_resolve_obligation_count() -> Nat {
+  ci_floor_expected_resolve_obligations() |> count
+}
+
+fn ci_floor_declared_resolve_count() -> Nat {
+  ci_floor_expected_resolve_obligation_count()
+}
+
+fn ci_floor_resolve_obligation_identities() -> List<ResolveObligationIdentity> {
+  map(ci_floor_expected_resolve_obligations(), o => o.identity)
+}
+
+type ResolveColdReceipt {
+  resolve_nanos: Nanosecond
+}
+
+type ResolveSharedPoolProvider {
+  provider_id: String
+}
+
+type ResolveSharedPoolReceipt {
+  provider_id: String
+}
+
+type ResolveRealization
+  = ColdResolvePerformed { obligation: ResolveObligation, receipt: ResolveColdReceipt }
+  | SatisfiedFromSharedPool {
+      obligation: ResolveObligation,
+      provider: ResolveSharedPoolProvider,
+      receipt: ResolveSharedPoolReceipt,
+    }
+
+fn realization_obligation(r: ResolveRealization) -> ResolveObligation {
+  match r {
+    ColdResolvePerformed { obligation: o, receipt: _ } => o
+    SatisfiedFromSharedPool { obligation: o, provider: _, receipt: _ } => o
+  }
+}
+
+fn realization_identity(r: ResolveRealization) -> ResolveObligationIdentity {
+  realization_obligation(r: r).identity
+}
+
+fn obligation_matches_expected(o: ResolveObligation) -> Bool {
+  let exp = expected_obligation(id: o.identity)
+  o.subject.entry == exp.subject.entry && o.subject.function == exp.subject.function
+}
+
+fn realization_is_well_formed(r: ResolveRealization) -> Bool {
+  match r {
+    ColdResolvePerformed { obligation: o, receipt: rec } =>
+      obligation_matches_expected(o: o) && nanosecond_count(rec.resolve_nanos) > 0
+    SatisfiedFromSharedPool { obligation: o, provider: p, receipt: rec } =>
+      obligation_matches_expected(o: o)
+        && p.provider_id != ""
+        && rec.provider_id != ""
+        && rec.provider_id == p.provider_id
+  }
+}
+
+fn warm_without_provider_receipt(r: ResolveRealization) -> Bool {
+  match r {
+    SatisfiedFromSharedPool { obligation: _, provider: p, receipt: rec } =>
+      p.provider_id == "" || rec.provider_id == "" || rec.provider_id != p.provider_id
+    _ => false
+  }
+}
+
+fn cold_without_resolve_receipt(r: ResolveRealization) -> Bool {
+  match r {
+    ColdResolvePerformed { obligation: _, receipt: rec } => nanosecond_count(rec.resolve_nanos) == 0
+    _ => false
+  }
+}
+
+fn resolve_obligation_receipt_has_identity(
+  realizations: List<ResolveRealization>,
+  id: ResolveObligationIdentity,
+) -> Bool {
+  any(realizations, r => realization_identity(r: r) == id)
+}
+
+fn native_obligation_absent(realizations: List<ResolveRealization>) -> Bool {
+  !resolve_obligation_receipt_has_identity(
+    realizations: realizations,
+    id: NativeBundleEscapingEntry,
+  )
+}
+
+fn unknown_obligation_appeared(realizations: List<ResolveRealization>) -> Bool {
+  any(realizations, r => !obligation_matches_expected(o: realization_obligation(r: r)))
+}
+
+fn obligation_realized_twice(
+  realizations: List<ResolveRealization>,
+  id: ResolveObligationIdentity,
+) -> Bool {
+  let n = fold(realizations, init: 0, f: fn(acc, r) {
+    if realization_identity(r: r) == id { acc + 1 } else { acc }
+  })
+  n > 1
+}
+
+fn same_obligation_realized_twice(realizations: List<ResolveRealization>) -> Bool {
+  any(
+    ci_floor_resolve_obligation_identities(),
+    id => obligation_realized_twice(realizations: realizations, id: id),
+  )
+}
+
+fn resolve_realization_finalization_holds(
+  realizations: List<ResolveRealization>,
+  unattributed_physical_resolves: Nat,
+) -> Bool {
+  unattributed_physical_resolves == 0
+    && (realizations |> count) == ci_floor_expected_resolve_obligation_count()
+    && for_all(ci_floor_expected_resolve_obligations(), exp =>
+        resolve_obligation_receipt_has_identity(realizations: realizations, id: exp.identity))
+    && for_all(realizations, r => realization_is_well_formed(r: r))
+    && !same_obligation_realized_twice(realizations: realizations)
+    && !unknown_obligation_appeared(realizations: realizations)
+}
+
+fn cold_realization(id: ResolveObligationIdentity, nanos: Nat) -> ResolveRealization {
+  ColdResolvePerformed {
+    obligation: expected_obligation(id: id),
+    receipt: ResolveColdReceipt { resolve_nanos: nanosecond(count: nanos) },
+  }
+}
+fn warm_realization(id: ResolveObligationIdentity) -> ResolveRealization {
+  SatisfiedFromSharedPool {
+    obligation: expected_obligation(id: id),
+    provider: ResolveSharedPoolProvider { provider_id: floor_entry_walk_memo_provider_id },
+    receipt: ResolveSharedPoolReceipt { provider_id: floor_entry_walk_memo_provider_id },
+  }
+}
+
+fn cold_resolves_performed(realizations: List<ResolveRealization>) -> Nat {
+  fold(realizations, init: 0, f: fn(acc, r) {
+    match r {
+      ColdResolvePerformed { obligation: _, receipt: _ } => acc + 1
+      SatisfiedFromSharedPool { obligation: _, provider: _, receipt: _ } => acc
+    }
+  })
+}
 
 data ci_floor_native_batch_resolve_receipt_note: String = "RECEIPT 9 — CONSCIOUS RAISING 1 -> 2 (2026-08-02, native-bundle production enrollment): CI run 30767841790 refused exactly `floor resolve count 2 differs from declared 1` and wrote target/floor-resolve-receipt.txt with resolves_total=2, resolve_ms_total=79064. The cause is the empirical law above operating as designed: gunbc_pr_native_batch enrolls as a RunnableSingleClaim on its own entry file (src/v2/test/claim/pr_native_batch_test.dag), an entry class whose closure escapes the batch-1 whole-tree materialization, so it pays its own cold resolve — 1 anchor + 1 escaping entry = 2. Same run: the batch itself PASSED via the counted outage fallback (verdict fallback:native_realization_refused, transport causes located), so the resolve count is the sole finalization refusal. Ratchet direction unchanged: the persistent content-keyed store still owes the permanent pin at 1, and de-enrolling the native batch (or pooling its closure warm) lowers this row consciously in the PR that does it. Merge note (2026-08-03, #7522 x #7671): the warm merge-admission capture stays OUTSIDE this count — its claim_batch child owns the capture resolve per Receipt 8 — so the two lanes compose at 2, not 3."
 
@@ -182,10 +377,10 @@ data floor_finalization_note: String = "The CI floor's post-batch contract, and
 
 TWO LAWS, ONE FIELD. Materialization disclosure was briefly a `require_materialization_disclosure: Bool` beside the count, and that Bool was a writable bypass with a lie attached: the executor returned before checking the materialization receipt when it was false, while its success message — unconditional on the Bool — still reported that disclosure held. One consumer exists and it requires disclosure, so the `false` state was pre-authored for nobody. Disclosure is now INTRINSIC to the type: inhabiting FloorFinalization is what obligates both laws. A future consumer that genuinely needs resolve-count validation alone introduces its own finalization type when it exists, rather than being pre-authored as a bypass here (§5 — the state a check can be satisfied by editing away is the state that should not be writable).
 
-declared_resolve_count is Nat, not Int: a negative declared count has no meaning, and making it unrepresentable is cheaper than guaranteeing it mismatches later."
+expected_resolve_obligations is the transported closed universe (identity + subject per row); unattributed physical resolves are counted at entry grain — a cold resolve on a co-resident function of a rostered obligation entry is not unattributed (cheap gates and compile-clean share dag/tools/floor_effect_gate_witness.dag via walk_memo)."
 
 type FloorFinalization {
-  declared_resolve_count: Nat
+  expected_resolve_obligations: List<ResolveObligation>
 }
 
 data ci_sccache_provider_shell_injection_dissolution_trigger: Disposition = Scaffold {

dag/gunbc/floor_materialization.dag

@@ -6,6 +6,8 @@ data floor_three_quantities_note: String = "GRAIN (merry-moth-539, 2026-07-09) 
 
 data floor_index_build_share_provider_id: String = "process_shared_index"
 
+data floor_entry_walk_memo_provider_id: String = "walk_memo"
+
 data floor_index_build_identity: String = "union-index-build(dag,src/v2)"
 
 fn floor_executor_process_frame() -> std.materialization_ladder.Frame {

dag/gunbc/floor_resolve_realization.dag

@@ -0,0 +1,27 @@
+module gunbc.floor_resolve_realization
+
+import gunbc.ci_materialization {
+  ResolveObligationIdentity,
+  ResolveObligation,
+  ResolveRealization,
+  CompileAnchorWholeTree,
+  NativeBundleEscapingEntry,
+  ci_floor_declared_resolve_count,
+  ci_floor_expected_resolve_obligations,
+  ci_floor_expected_resolve_obligation_count,
+  ci_floor_resolve_obligation_identities,
+  resolve_realization_finalization_holds,
+  cold_realization,
+  warm_realization,
+  cold_resolves_performed,
+  native_obligation_absent,
+  unknown_obligation_appeared,
+  same_obligation_realized_twice,
+  warm_without_provider_receipt,
+  cold_without_resolve_receipt,
+}
+import std.nat { Nat }
+import v2.std.text { String }
+import v2.std.collection { List }
+
+data floor_resolve_realization_note: String = "Thin re-export of gunbc.ci_materialization resolve-obligation authority (0B, 2026-08-04). Expected population and finalization law live in ci_materialization; claim_executor records observations at reuse sites; ci_floor_plan transports expected_resolve_obligations only."

dag/gunbc/non_fold_residue.dag

@@ -65,6 +65,8 @@ data nfr_dissolve_native_agreement_octet: String = "RuntimeValue model↔realiza
 
 data nfr_reason_observation_hold_cause: String = "the CI-log renderer names the two memory-pressure holds (PsiPressure, CurrentHighWater — the crawl-window narrative) with a specific cause and gives the other five SchedulerHold variants a generic 'blocked on scheduler admission'; landed with the progress-and-observation stack (session/sleek-ibex-634, #7168) and surfaced by the whole-corpus nfr receipt after per-PR affected-set selection predict-skipped the corpus-read nfr witness at merge time (the masking class); declared so the ratchet re-arms"
 
+data nfr_reason_resolve_realization_predicate: String = "discriminating subset predicate over ResolveRealization (param scrutinee, off-variant wildcard arm returning false) — each arms an independent RED control in floor_resolve_realization_witness_test.dag; landed with #7810 resolve-realization 0B obligation model and surfaced by the whole-corpus nfr receipt; declared so the ratchet re-arms"
+
 data nfr_reason_provider_terminal_absorb: String = "terminal-state absorption over the provider/worker observation coproducts: the arm names each TERMINAL variant (ProviderCompleted / ProviderFailed / ProviderEventsRefused, or WorkerProcessRunning) and gives every non-terminal variant one shared arm, because those variants reduce to the identical behaviour — enumerating them would clone the arm per variant, which is the redundancy DESIGN §2 forbids rather than the totality DESIGN §4 asks for. Landed with the Codex dispatch and recursive workflow evidence slice; declared at landing (not surfaced by a later cold sweep) so the ratchet arms with the code."
 
 data nfr_dissolve_provider_terminal_absorb: String = "ProviderExecutionState and WorkerProcessEvidence carry a DERIVED terminality projection from inhabitance (dag/std/algebra, DESIGN §3/§4 — the same move as derived equality), so these folds match on the partition rather than on the variant list, the shared arm becomes a named case instead of a wildcard, and the rows delete."
@@ -767,6 +769,16 @@ data non_fold_residue_frontier: List<FrontierRow> = [
     reason: nfr_reason_legacy_slice1_bridge,
     trigger: TriggerProse { text: "DISSOLVE-ON: membership apply dispatch derives off-variant noop from MemberAction inhabitance (MemberTeardown/MemberTeardownRefused are construction-unreachable for Ensured bindings) and the wildcard arm deletes with the row" },
   },
+  FrontierRow {
+    subject: PathSubject { path: "dag/gunbc/ci_materialization.dag::warm_without_provider_receipt" },
+    reason: nfr_reason_resolve_realization_predicate,
+    trigger: TriggerProse { text: nfr_dissolve_wildcard_total },
+  },
+  FrontierRow {
+    subject: PathSubject { path: "dag/gunbc/ci_materialization.dag::cold_without_resolve_receipt" },
+    reason: nfr_reason_resolve_realization_predicate,
+    trigger: TriggerProse { text: nfr_dissolve_wildcard_total },
+  },
 ]
 
 fn non_fold_residue_frontier_units() -> List<String> {