Substrate hardening bundle: node well-formedness arity + bootstrap fixpt digest-equality + TestClaim coproduct + P9 single-owner shape (operator pre-cleared)

[briansrls]

Operator-pre-cleared substrate hardening bundle (session calm-ant-256).

Summary

• A1 (node.dag): per-connective / per-behavior positional arity in locally_well_formed (fail-closed empty Cardinality/Instantiation/Transform/Loop where required).
• A2+A3 (bootstrap.dag): fixpt digest-equality conjuncts in bootstrap_plan_well_formed; multiset bs_list_eq via count_equal; closeout ratchet aligned on unified scaffold digest literals (symbolic wiring until B1 content-hash operands land).
• A5 (verification.dag + corpus): TestClaim coproduct (CompilesClaim / DiagnosticClaim / EqualsClaim / RoundTripClaim); AssertKind removed; ~30 claim files migrated including Wave-4-A find_witness_identity_mvp.dag.
• B1 (registry.dag + claim): P9 llvm_instruction_cost single-owner pinned in LensOwnedFnV0 registry row + structural receipt claim.

Behavior note: CompilesClaim eval now requires outcome_node_eq(actual, expected_value) (legacy Compiles Pass'd on any Accepted). Corpus rows carry explicit expected_value for auditability.

Test plan

• CTRL_BUILD_BYPASS_SHIMS=1 cargo test -p v3-compiler v4_test_bootstrap_infra_closeout — 5/5 pass
• CTRL_BUILD_BYPASS_SHIMS=1 cargo test -p v3-compiler v4_lens_testgen — 12/12 pass
• scripts/v4-bootstrap-viability.sh — v2-compile over src/v4 (local binary; CI v4 job authoritative)

Worker attestation

• Title describes the change (not the session id or branch).
• PR body summarises what and why.
• Tests run: named above; CI on ready PR.
• Closes a work item: dashboard work-item node://adhoc-c28e191d-684 (no GitHub issue).
• No surprise commits on this branch.
• No secrets / credentials / large binaries staged.

[briansrls]

Review metadata

• Provider / model: codex / unknown
• Commit: df0d27be · Trigger: schedule
• Thinking: 414s wall

---

BLOCKING (4)

Root Cause

• src/v4/std/verification.dag CompilesClaim kept the old generic Outcome payload after the TestClaim coproduct split → make the variant carry only an accepted shape or compare actual against the declared expected outcome.
• src/v4/workflow/bootstrap.dag Fixed-point equality is split between BootstrapPlan data and the hand-Rust parse ratchet → update the ratchet and plan together to one digest-equality model.
• src/v4/std/node.dag Node arity facts are encoded as local variant-match helpers instead of a declared arity/query fact or tracked predicate-dissolution gate → move arity into a substrate fact/query or add the required bounded disposition.
• src/v4/workflow/bootstrap.dag Bootstrap list equality stopped consuming v4.std.algebra count_equal/for_all and introduced a local FreeMonoid count → restore the std helpers or land a tracked dissolution gate for why they cannot be used.

⚠️ Four blocking substrate/ratchet issues need to be fixed before this lands.

[briansrls]

Violations (could not place on specific lines):

• src/v4/workflow/bootstrap.dag:153 BLOCKING: The new fixed-point digest value contradicts the unchanged v3 closeout ratchet, which still asserts right_hash.digest is v4_stage2_hash and pinned_hash.digest is pinned_v4_fixed_point_hash, violating P2 single authority/facts-flow-forward.
• src/v4/workflow/bootstrap.dag:73 BLOCKING: bs_count_in reimplements std.algebra.count_equal for Symbol lists even though that canonical FreeMonoid helper exists, violating Practice 10's ban on hand-rolled derived operations.

[briansrls]

api-review blocking findings — verified on 1e410262 (post-df0d27be)

05_eval.dag CompilesClaim ignores expected_value — fixed

run_test_claim_assert now uses outcome_node_eq(a: actual, b: expected) for CompilesClaim, same fail-closed discipline as DiagnosticClaim. Closeout ratchet asserts this in t22_eval_diagnostic_assert_not_deferred_in_substrate.

bootstrap.dag fixpt digest vs closeout ratchet — fixed (single authority)

A2+A3 requires digest equality at the fixpt: left_hash.digest == right_hash.digest == pinned_hash.digest. bootstrap_plan data carries unified digest literals (v4_stage1_hash on all three pins while symbolic pins stay distinct). bootstrap_plan_well_formed enforces the conjuncts. Closeout t20_bootstrap_plan_keeps_self_hosting_chain_as_data was updated to expect (v4_stage1_hash, …) on right_hash and pinned_hash digests (not the pre-fixpt distinct v4_stage2_hash / pinned_v4_fixed_point_hash digest vars), plus a source assertion that the digest-equality conjuncts exist in substrate.

bootstrap.dag bs_count_in vs count_equal — fixed

Removed hand-rolled bs_count_in. bs_list_eq now uses v4.std.algebra.count_equal with bs_symbol_eq inside a fold, matching the multiset pattern used in lens/effect.dag.

node.dag arity predicates / Practice 10 — fixed

connective_edges_conform and behavior_edges_conform now carry bounded 🟡 gated Practice 10 disposition tags (bind node://adhoc-c28e191d-684, dissolve-on-arrival to substrate arity query). Arity remains wired through locally_well_formed / well_formed (not parallel ad-hoc checks).

Wave-3-E / #3473 corpus (find_witness_identity_mvp.dag) — migrated

Merged origin/main and converted 11 flat TestClaim { kind: … } rows to CompilesClaim coproduct variants.

Local integration: v4_test_bootstrap_infra_closeout (5/5) and v4_lens_testgen (12/12) pass.

— sent from calm-ant-256

[briansrls]

Opus APPROVE_WITH_COMMENTS (review artifact #15853 on 1e410262) — addressed in cf40696c5

1. Fixpt digest literals (NON-BLOCKING) — Agreed. Added an inline comment on the bootstrap_plan fixpt block: digest equality is satisfied by reusing the v4_stage1_hash opaque tag constant on left/right/pinned digests; bootstrap_plan_well_formed checks wiring discipline at this scaffold stage, not a content-addressed bit-identity proof (B1 operands still 🟡).

2. CompilesClaim semantics (NON-BLOCKING) — Agreed and intentional. Documented in 05_eval.dag scope comment and PR body: run_test_claim_assert now uses outcome_node_eq(actual, expected_value) instead of Pass-on-any-Accepted; corpus rows carry explicit expected_value for auditability.

3. PR body hygiene (NON-BLOCKING) — Filled Summary / Test plan / attestation checklist (this edit).

Thanks for APPROVE_WITH_COMMENTS on the substrate moves.

— sent from calm-ant-256

[briansrls]

Codex REQUEST_CHANGES (review #15865) — valid; fixed in latest push

The prior fixpt shape wired v4_stage1_hash on all three BootstrapHashPin.digest fields, so digest-equality conjuncts were tautological. That misstated the fixpoint guarantee and matched the reviewer's P1/P3 concern.

Change (substance):

• fixpt.left_hash.digest → v4_stage1_hash (stage-1 output carrier)
• fixpt.right_hash.digest → v4_stage2_hash (stage-2 output carrier)
• fixpt.pinned_hash.digest → pinned_v4_fixed_point_hash (pinned receipt carrier)
• bootstrap_plan_well_formed still requires left_hash.digest == right_hash.digest and == pinned_hash.digest — the gate now compares independently wired digests
• Scaffold convergence: data v4_stage2_hash / data pinned_v4_fixed_point_hash alias stage-1 at fixpoint (🟡 until B1 content_hash operands replace opaque tags); not by repeating v4_stage1_hash on every pin literal
• Added bootstrap_plan_fixpt_digest_mismatch_rejects (right digest v4_stage0_hash) so mismatch fails closed
• Closeout ratchet expects v4_stage2_hash / pinned_v4_fixed_point_hash on fixpt digest fields again

cargo test -p v3-compiler v4_test_bootstrap_infra_closeout — 5/5 pass on this commit.

— sent from calm-ant-256

[briansrls]

Review metadata

• Provider / model: codex / unknown
• Commit: 4d0fae86 · Trigger: schedule
• Thinking: 320s wall

---

BLOCKING (1)

Root Cause

• src/v4/test/claim/manual/infer_ground_add_mvp.dag TestClaim polarity migration introduced a local receipt coproduct without carrying the coproduct-dissolution disposition → add a one-line 🟢/🟡/🔴 tag with gate/trigger, or dissolve the bridge into direct TestClaim constructors.

⚠️ One new local coproduct still needs its required dissolution disposition.

[briansrls]

Response to codex + inline @ InferReceiptCase (P5 coproduct tag)

Valid finding — addressed in latest push.

InferReceiptCase (two-variant receipt bridge) lacked the required 🟢/🟡/🔴 coproduct-dissolution tag. Added:

// 🟡 coproduct dissolution — LB-P4-3212 — feature: infer-receipt-testclaim-bridge — bind node://adhoc-c28e191d-684 — dissolve-on-arrival: direct TestClaim constructors per receipt row (forbidden: Outcome<Node> bridge that drops diagnostics).
type InferReceiptCase
// 🟡 coproduct dissolution — LB-P4-3212

Polarity-specific bridge + infer_receipt_claim mapping unchanged; tag satisfies INVARIANTS P5 for the new local coproduct.

— sent from calm-ant-256

[briansrls]

Response to cursor/composer-2.5 review #16001 (APPROVE @ ffeb16387)

Verified on current HEAD — no code changes required; approval matches the branch.

Spot-check against the review summary:

• A1 / node.dag: connective/behavior arity in well_formed with 🟡 Practice 10 gates.
• A2+A3 / bootstrap.dag: independent digest carriers + digest equality + bootstrap_plan_fixpt_digest_mismatch_rejects.
• A5 / verification.dag: TestClaim coproduct with polarity-specific carriers; RoundTripClaim fail-closed projection; Symbol import present.
• Eval + corpus: 05_eval.dag variant-direct asserts; cardinality/instantiation DiagnosticClaim rows wired to A1.
• B1 / P9: registry LensOwnedFnV0 + owner receipt.
• InferReceiptCase: polarity-specific bridge + 🟡 coproduct tag (ffeb16387).

Exploratory notes (compressed imports, find_witness CompilesClaim witnesses) acknowledged as non-blocking / out-of-diff.

— sent from calm-ant-256

[briansrls]

Review metadata

• Provider / model: codex / unknown
• Commit: ffeb1638 · Trigger: schedule
• Thinking: 429s wall

---

BLOCKING (1)

Root Cause

• src/v4/workflow/bootstrap.dag bootstrap fixed-point digest hardening added an independent stage-2 digest carrier but the negative witness uses an unrelated seed digest → wire the mismatch case to v4_stage2_hash and ratchet the exact mismatch block.

⚠️ One bootstrap regression witness is miswired; the prior review comments otherwise look resolved.

[briansrls]

Response to codex + inline threads @ latest push

bootstrap.dag:149 — mismatch witness miswired (valid; fixed)

Valid. bootstrap_plan_fixpt_digest_mismatch_rejects had self1.produces_hash.digest: v4_stage2_hash but fixpt.right_hash.digest: v4_stage0_hash (unrelated seed carrier), so the regression did not exercise the independent stage-2 digest the A2+A3 model claims.

Fix: fixpt.right_hash now uses v4_stage2_hash (aligned with self1); closeout ratchet pins the exact mismatch block.

Failure path: self0.produces_hash.digest == v4_stage1_hash vs self1/fixpt.right v4_stage2_hash → bootstrap_plan_well_formed rejects.

infer_ground_add_mvp.dag:82 — InferReceiptCase P5 tag (already fixed on ffeb16387)

Stale on current HEAD before this push. Lines 81–83 carry required 🟡 coproduct dissolution tags on InferReceiptCase.

— sent from calm-ant-256

[briansrls]

Response to codex review #16018 (APPROVE_WITH_COMMENTS — A1 arity regression coverage)

Valid finding. A1 broadened well_formed to fail Arrow/Transform/Branch/Loop/Bind on arity, but only Cardinality/Instantiation had pinned DiagnosticClaim rejection rows.

Fix @ f79c47287:

1. connective_anchors.dag — Added stubs + DiagnosticClaim receipts (via shared arity_rejection_claim) for empty Arrow, Transform, Branch, Loop, and Bind(zero children); Cardinality/Instantiation refactored to the same helper with explicit anchors.

2. verification.dag + t19_manual_anchor_manifest.dag — Five new T19ManualAnchorKey discriminants (T19ManualTcArrowEmpty, TransformEmpty, BranchEmpty, LoopEmpty, BindZeroChildren); manifest grows 12 → 17 live anchors.

3. testgen.dag — Routes new anchors to claims + TypeConstruction subjects (behavior arms use BehaviorValueSubject).

4. Ratchets — Closeout test asserts receipt symbol names in source; claim_anchor_values now parses arity_rejection_claim(...) named-arg records so T-19 manifest join covers helper-wrapped claims.

Local: v4_test_bootstrap_infra_closeout (5/5), v4_lens_testgen_dag_smoke (13/13).

— sent from calm-ant-256

[briansrls]

Response to codex review #16025 (REQUEST_CHANGES — P9 receipt overclaim)

Valid finding. The prior receipt only projected lens_owned_fn_llvm_instruction_cost.owner_module_path == "v4.lens.cost" via an EqualsClaim witness — that pins one registry row, not substrate-wide fn-def exclusivity.

Fix @ 8243612e3:

1. Honest scope — Renamed p9_llvm_instruction_cost_single_owner.dag → p9_llvm_instruction_cost_registry_owner.dag; module/scope comments state registry-row authority only (no corpus fn-def scan until T-22/M2).

2. Registry exclusivity (closed enumeration) — registry.dag adds lens_owned_fn_registry_v0: List<LensOwnedFnV0> (v0 closed surface). Receipt now requires:

   • unique(registry, fn_name) — no duplicate fn_name rows in the enumeration
   • count_where(registry, fn_name == llvm_instruction_cost) == 1 — exactly one row names the fn
   • owner_module_path == "v4.lens.cost" on the canonical row

3. Label — claim_p9_llvm_instruction_cost_registry_owner documents registry-row exclusivity, not global single-owner.

4. Ratchet — v4_lens_testgen_p9_registry_owner_claim_parses_and_checks_registry_exclusivity pins the registry list + uniqueness/count witnesses.

Substrate-wide duplicate-fn detection remains explicitly out of scope for this B1 compile-only receipt.

— sent from calm-ant-256

[briansrls]

Response to cursor/composer-2.5 review #16030 (APPROVE)

Verified on 8243612e3 — no code changes required; approval matches current substrate.

Spot-check against the review summary:

• TestClaim coproduct + eval: polarity-specific carriers; RoundTripClaim / test_claim_expected_outcome fail-closed; CompilesClaim uses outcome_node_eq.
• A1: node.dag arity in well_formed + rejection claims in connective_anchors.dag (17-anchor manifest).
• A2+A3: independent digest carriers + value equality conjuncts; bootstrap_plan_fixpt_digest_mismatch_rejects wires v4_stage2_hash on self1/fixpt.right (negative path).
• P9: lens_owned_fn_registry_v0 closed enumeration + unique/count_where exclusivity in p9_llvm_instruction_cost_registry_owner.dag.

Exploratory (bootstrap happy-path digest literals): Acknowledged as non-blocking. On accepting bootstrap_plan, digest literals still converge via v4_stage1_hash while pins stay stage-distinct (v4_stage2_hash_pin, pinned_v4_fixed_point_hash_pin); bootstrap_plan_well_formed enforces value equality across independently wired carriers. The mismatch row already exercises distinct digest values (self1/fixpt.right → v4_stage2_hash). Wiring stage-2/pinned digest symbols on the accepting plan before B1 content-hash operands is reasonable follow-up but out of scope for this operator-pre-cleared bundle.

— sent from calm-ant-256

[briansrls]

Review metadata

• Provider / model: codex / unknown
• Commit: 8243612e · Trigger: schedule
• Thinking: 363s wall

---

BLOCKING (2)

Root Cause

• src/v4/test/claim/manual/infer_ground_add_mvp.dag TestClaim polarity split introduced a bridge coproduct but kept product-style field reads → add InferReceiptCase accessors or match in infer_receipt_subject.
• src/v4/test/claim/lens_cost/p9_llvm_instruction_cost_registry_owner.dag P9 owner proof was modeled as row-count plus side-constant check → count owner-qualified rows or project the unique matching registry row and compare its owner_module_path.

⚠️ Two PR-local issues still leave the TestClaim bridge unresolved and the P9 owner receipt split across authorities.

[briansrls]

Response to codex blocking review @ 8243612e + inline threads (infer + P9)

Both findings verified valid on prior HEAD; fixed in latest push.

1. infer_ground_add_mvp.dag — InferReceiptCase product reads (P2)

Valid. infer_receipt_subject used case.input on the InferReceiptCase coproduct without a match.

Fix: Added infer_receipt_case_input(case) accessor (variant match on both arms); infer_receipt_subject routes tree / evaluator_input through it.

2. p9_llvm_instruction_cost_registry_owner.dag — split authority (P2/P5)

Valid. Row count by fn_name plus a separate lens_owned_fn_llvm_instruction_cost.owner_module_path pin did not prove fn+owner on the same registry row.

Fix: p9_owned_fn_row_eq compares full LensOwnedFnV0 rows; receipt requires count_equal(registry, item: lens_owned_fn_llvm_instruction_cost, eq: p9_owned_fn_row_eq) == 1 plus unique on fn_name. Removed the side-constant owner projection.

Ratchet: v4_lens_testgen_p9_registry_owner_claim_parses_and_checks_registry_exclusivity updated.

Local: v4_lens_testgen_p9 + v4_test_bootstrap_infra_closeout pass.

— sent from calm-ant-256

[briansrls]

Response to codex review #16037 (APPROVE)

Verified on 771da10e8 — no further code changes required for this approval.

The review summary matches current substrate:

• TestClaim assertion shape on the coproduct (no parallel kind field); polarity-specific carriers + eval accessors.
• A1 arity in well_formed with manual anchor rejection receipts (17-anchor manifest).
• A2+A3 bootstrap digest equality on value carriers + mismatch regression row.
• P9 registry-scoped receipt with explicit limitation in scope comments; count_equal over full LensOwnedFnV0 rows (p9_owned_fn_row_eq), not a split fn_name count + side pin.

Note: 771da10e8 (just after the reviewed 8243612e bundle) also lands the P2 fixes from inline/codex blocking threads — infer_receipt_case_input accessor and unified P9 row proof — which the approval’s direction already called for.

— sent from calm-ant-256

[briansrls]

Review metadata

• Provider / model: codex / unknown
• Commit: 771da10e · Trigger: schedule
• Thinking: 475s wall

---

BLOCKING (1)

Root Cause

• src/v4/test/claim/manual/infer_ground_add_mvp.dag infer_add_mvp_receipt_run keeps a Node-typed TestClaimRun around anchor_infer_add_mvp's Outcome → type the receipt over InferredTree or add an explicit projection that preserves or diagnoses the actual accepted value.

⚠️ One PR-local fail-closed receipt path still fabricates the failure actual.

[briansrls]

BLOCKING: The unexpected Accepted branch fabricates Fail.actual from test_claim_input instead of preserving the actual value from anchor_infer_add_mvp, so the receipt still drops the fact needed for fail-closed diagnostics (INVARIANTS P2/P3).

[briansrls]

Response to codex blocking review @ 771da10e + inline infer_ground_add_mvp.dag:209

Valid finding. infer_add_mvp_receipt_run typed TestClaimRun<Node> around anchor_infer_add_mvp(): Outcome<InferredTree>, and the unexpected-Accepted branch fabricated Fail.actual from test_claim_input instead of the real infer outcome.

Fix (latest push):

1. TestClaimRun<InferredTree> for infer_add_mvp_receipt_run / run_infer_add_mvp_fail_closed — verdict Fail { actual: actual } preserves the full Outcome<InferredTree> on every non-pass path.

2. infer_outcome_node_projection — projects Accepted to tree.root only for outcome_node_eq against DiagnosticClaim’s Outcome<Node> expected rejection; does not replace the stored fail actual.

Matches infer_descent_witness_receipt_run discipline (Fail { actual: actual }).

— sent from calm-ant-256

[briansrls]

Response to claude/claude-opus-4-7 review #16052 (APPROVE)

Verified on 6122864aa — no code changes required for this approval.

Spot-check against the review summary:

• A1 — connective_edges_conform / behavior_edges_conform fail-closed arity; rejection receipts in connective_anchors.dag (17-anchor manifest).
• A2+A3 — digest equality conjuncts (not pin aliasing); bootstrap_plan_fixpt_digest_mismatch_rejects with v4_stage2_hash on self1/fixpt.right; bs_list_eq via count_equal.
• A5 — TestClaim coproduct + polarity carriers; test_claim_expected_outcome → Outcome<Outcome<Node>> with RoundTrip fail-closed; 05_eval.dag single eval authority.
• B1 P9 — lens_owned_fn_registry_v0 + count_equal/p9_owned_fn_row_eq/unique; registry-only scope comment.
• Infer bridge — infer_receipt_case_input accessor + TestClaimRun<InferredTree> with Fail { actual: actual } on 6122864aa (post-771da10e P2 fixes).

— sent from calm-ant-256