R3 gate #36: bridge_retirement_ledger_zero (T-Bridge-Retirement)

[briansrls]

Auto-opened by session-dashboard for session sunny-heron-621.
Pushing to session/sunny-heron-621 advances this PR.

Worker attestation

Before flipping this PR to ready for review, confirm each item:

• Title describes the change (not the session id or branch).
• PR body summarises what and why (replace the TODO below).
• Tests run: name the command (e.g. npm test, cargo test) and the result.
• If this closes a work item, the body contains a Closes #N directive.
• No commits on this branch are surprises (no fork/cherry-pick I did not make).
• No secrets / credentials / large binaries staged.

Summary

TODO: replace this paragraph with one or two sentences naming the change and its motivation. Reviewers read this first.

Test plan

• TODO: list the commands that ran (or "no tests changed; relied on CI") and the outcome.

[briansrls]

Review item (codex / #11868) — verified

Walked the current tree against the artifact summary:

• Kernel Bool → BooleanAlgebra<Bool> wiring lives in lower_type_sum / wire_kernel_bool_boolean_algebra_inhabits (lower.rs), still fail-closed on missing BooleanAlgebra / bad arity via attach_bootstrap_diagnostic, and still gated to BootstrapAuthorityKey::for_kernel_bool().path() + True/False variant shape.
• bridge_ledger.dag keeps bridge_exact_string_semantic_patching_residual as Open (no overstated retirement).

CI follow-up (valid failure, not a review nit): regen_bootstrap --verify on the previous HEAD failed because dsl/std/types.dag comment edits shifted embedded SourceSpan byte ranges vs the committed PB-1-e snapshots. Pushed b5b7e3da6 — regenerated bootstrap_std_generated.rs, bootstrap_generated.rs, and bootstrap_generated_without_parse_surface.rs; local regen_bootstrap --verify is green.

Merge readiness: Dashboard rule still needs a second distinct approving provider on the current HEAD after CI re-runs; codex approval is on the prior SHA until reviews refresh. Not squash-merging until ≥2 approvals, no REQUEST_CHANGES, mergeable clean, and checks green on the tip commit.

— sent from sunny-heron-621

[briansrls]

Review metadata

• Provider / model: codex / unknown
• Commit: 88709cf5 · Trigger: schedule
• Thinking: 343s wall

---

BLOCKING (1)

Root Cause

• src/v3/compiler/src/lower.rs bootstrap invariant "kernel Bool exists and inhabits BooleanAlgebra" was collapsed into per-item lowering that only runs when the item exists → keep the lower-time wiring, but add a bootstrap/finalization validation that diagnoses missing kernel Bool or missing Bool.inhabits.

Non-blocking — Improvements (fix in-PR if easy, else defer to roadmap)

• src/v3/std/bridge_ledger.dag Clarify that the Bool Row-4 class is narrowed but not retired because it remains host-side name/file keyed wiring; defer under T-Bridge-Retirement Row-4 BR-19 until direct authored inhabits lands.

⚠️ One fail-closed bootstrap regression should be fixed before landing.

[briansrls]

Blocking review (lower.rs:3588 + bootstrap P3) — verified and addressed on tip

The concern is valid: wiring kernel Bool only inside the optional lower_type_sum branch means a regression where the authoritative dsl/std/types.dag sum never lowers would not hit that path.

Mitigation on main of this PR (already in the branch before the latest push):

1. bootstrap::ensure_kernel_bool_lane1e2b_bootstrap_witness — After every committed snapshot loads, this scans for Bool at BootstrapAuthorityKey::for_kernel_bool().path(). If absent → attach_bootstrap_diagnostic with a Lane 1e-2b ResolveError (same fail-closed channel as the old post-parse patch “Bool not found”). If present but inhabits is still None → calls lower::wire_kernel_bool_boolean_algebra_inhabits once; if still unset, wire_* has already attached its diagnostics. If inhabits is present but not a BooleanAlgebra<Bool> instantiation → another bootstrap-attributed ResolveError.

2. Dag::finalize_runtime_bootstrap_from_generated_snapshot calls that witness immediately after populate_primitive_cache() so every Dag::new() / snapshot finalization enforces the invariant (INVARIANTS P3), independent of whether the lower_type_sum branch ran.

Latest push f2618dcf6: regen_bootstrap + rustfmt only — bridge_ledger.dag comment lines shifted embedded SourceSpans; CI regen_bootstrap --verify must stay green.

Merge: Dashboard shows 2/2 approvals on an earlier SHA; GitHub mergeable is still UNKNOWN and checks pending on the new tip — not squash-merging until that settles green.

— sent from sunny-heron-621

[briansrls]

Review #11931 (cursor/composer-2) — verified + exploratory applied

• APPROVE / rubric: Confirmed on tip: single wire_kernel_bool_boolean_algebra_inhabits path, ensure_kernel_bool_lane1e2b_bootstrap_witness at snapshot finalization, bridge_exact_string_semantic_patching_residual still Open with honest prose — matches the artifact.

• Exploratory (.expect in witness): Addressed in ae2ac54e6 — after optional wire_*, let Some(inh_id) = declaration(bool_id).inhabits else { return }; replaces the redundant double-is_none guard + .expect, so unset inhabitance never panics (fail-closed stays on the diagnostic table only).

Merge: GitHub mergeStateStatus is BLOCKED / checks still in flight on the new HEAD after this push — not squash-merging until mergeable=CLEAN and CI green per operator bar.

— sent from sunny-heron-621

[briansrls]

Review #11968 (claude / claude-opus-4-7) — verified; one factual correction

Substance of the APPROVE matches HEAD:

• Post-parse patch_kernel_bool_boolean_algebra_inhabits is gone; lower_type_sum gates on BootstrapAuthorityKey::for_kernel_bool().path() + True/False and calls wire_kernel_bool_boolean_algebra_inhabits.
• Fail-closed witness ensure_kernel_bool_lane1e2b_bootstrap_witness exists and attaches BootstrapDiagnostic on missing kernel Bool, unset inhabitance after wire_*, or malformed BooleanAlgebra<Bool> shape.
• bridge_ledger.dag keeps bridge_exact_string_semantic_patching_residual Open with honest Row-4 / host-side wiring prose.

Artifact typo: the log says the witness is “invoked from Dag::populate_primitive_cache”. In code it is Dag::finalize_runtime_bootstrap_from_generated_snapshot, immediately after self.populate_primitive_cache() (see dag.rs around the populate_primitive_cache / ensure_kernel_bool_lane1e2b_bootstrap_witness pair). populate_primitive_cache itself is unchanged and does not call bootstrap witness logic.

Merge: GitHub mergeStateStatus is DIRTY (needs branch update / base sync) and v3 is still in progress on the latest workflow — not squash-merging until mergeable=CLEAN and checks are green.

— sent from sunny-heron-621

[briansrls]

Follow-up (merge hygiene + #11968)

• Pushed e9d5bfafe: merge origin/main into this branch (GitHub had mergeStateStatus: DIRTY behind main). Resolved the three bootstrap_*_generated*.rs conflicts by regen_bootstrap so snapshots match the combined .dag authorities after mainline landings (#3102, #3117, etc.). Local regen_bootstrap --verify + cargo clippy -p v3-compiler --all-targets -D warnings are green on that merge result.

• Main repair: the fifth annotation parse refusal today (fabric_storage_wire_witness_test) #11968 call-site note remains as in the prior comment: witness runs in finalize_runtime_bootstrap_from_generated_snapshot, immediately after populate_primitive_cache(), not inside populate_primitive_cache.

CI will need to cycle on the new merge commit before squash-merge.

— sent from sunny-heron-621

[briansrls]

Review #12020 (cursor / composer-2) — verified on current HEAD

• patch_kernel_bool_boolean_algebra_inhabits: No remaining references under src/v3/compiler/ (rg clean); the post-parse sweep is fully retired.
• Wiring: Kernel Bool → BooleanAlgebra<Bool> still flows through lower_type_sum → wire_kernel_bool_boolean_algebra_inhabits with BootstrapAuthorityKey::for_kernel_bool().path() + True/False gate.
• Witness: ensure_kernel_bool_lane1e2b_bootstrap_witness still runs from finalize_runtime_bootstrap_from_generated_snapshot immediately after populate_primitive_cache(), with Instantiation shape validation in bootstrap.rs (no .expect on the inhabits binding after the last refactor).
• bridge_ledger.dag: Row data unchanged; semantic row stays Open as described.

Merge readiness: Dashboard shows ≥2 distinct approving providers (codex + cursor + claude on recent artifacts) and no REQUEST_CHANGES, but checks_state is still pending (v3 in flight on workflow 25878225263) and GitHub reviewDecision is empty / merge state not yet CLEAN for a worker-side squash-merge. gh pr merge --squash remains blocked by branch protection until required GitHub reviews + green v3 land — operator / Verification Mgr path unchanged.

— sent from sunny-heron-621

[briansrls]

Review #12065 (cursor / composer-2) — verified

Confirmed on pre-merge HEAD: no patch_kernel_bool_* sweep in bootstrap_regen_fresh / bootstrap.rs; kernel Bool → BooleanAlgebra<Bool> wired in lower_type_sum + wire_kernel_bool_boolean_algebra_inhabits; finalize_runtime_bootstrap_from_generated_snapshot invokes ensure_kernel_bool_lane1e2b_bootstrap_witness after populate_primitive_cache(); bridge_ledger.dag prose matches remaining Open Row-4 reality. No further code changes for this artifact.

Merge: All checks green (fmt, ci, v3, self_host_ratchet), mergeStateStatus CLEAN, mergeable MERGEABLE — gh pr merge 3101 --squash --delete-branch completed (merged 2026-05-14T18:58:03Z).

— sent from sunny-heron-621

[briansrls]

Review metadata

• Provider / model: codex / unknown
• Commit: dd52ca2d · Trigger: schedule
• Thinking: 301s wall

---

BLOCKING (1)

Root Cause

• src/v3/compiler/src/bootstrap.rs Finalization combines validation with mutation → split the witness from repair: lower may wire Bool, but finalization should diagnose when authoritative Bool lacks a valid BooleanAlgebra inhabitance.

⚠️ One fail-closed bootstrap validation gap remains.

[briansrls]

BLOCKING: The finalization witness still silently repairs a missing Bool.inhabits by calling the lower-time wiring, so a skipped lower_type_sum branch or drifted snapshot can succeed without the INVARIANTS P3 diagnostic promised by the new check.