docs(planning): rung-3 acceptance predicate spec — phase1/nat_semiring (dag W1 / W1b staged)

[briansrls]

Summary

• Ladder/Fixture Manager third artifact (after rungs 0-2 in Ladder/Fixture Manager — authority over 9-rung correctness ladder, fixture set, rung gate shape (acceptance predicates per rung), 'no rustc-clean as headline' enforcement per PR #3938 §11.1. First artifact: nat_semiring × rungs 0-2 acceptance predicate spec; ratify nat_semiring as Phase 1 fixture; d #3946, rung 4 in docs(planning): rung-4 acceptance predicate spec — phase1/nat_semiring (Rust W2) #3990). Authors rung-3 acceptance predicate spec for phase1/nat_semiring per PR docs(planning): v4 correctness ladder + current-state audit (operator sign-off) #3938 §11.1 lane 2 and joint runner spec (compiler-spine-runtime-rung34-min-runner-interface-2026-05-30.md) §3 row "rung 3" + §4.4 rung-split.
• Cites W1: RoundTripClaim eval path (ingest⁻¹ on dag target) — PR #3938 §11.4 / joint runner spec §6 #3960 (W1: RoundTripClaim eval path; ingest⁻¹ on .dag target — run_test_claim_round_trip_verdict + dag_round_trip_wave1_authorities_ready) as the landed substrate. NOT Phase 1 dispatch (PR #3959 §11.4 step 4): R1 fixture generator + runner against rustc for rust.dag per merged leaf-model verification doc. Phase 1 scope: R1 (i32 surface spelling) — emit Rust source 'pub fn r1_test() -> i32 { 0i32 }' as fixture; invoke rustc; capture verdict; falsification probe = e #3972 (that's leaf-model verification, orthogonal lane — explicit out-of-scope §1).
• Additive to companion specs (Ladder/Fixture Manager — authority over 9-rung correctness ladder, fixture set, rung gate shape (acceptance predicates per rung), 'no rustc-clean as headline' enforcement per PR #3938 §11.1. First artifact: nat_semiring × rungs 0-2 acceptance predicate spec; ratify nat_semiring as Phase 1 fixture; d #3946, docs(planning): rung-4 acceptance predicate spec — phase1/nat_semiring (Rust W2) #3990) — cites §2.4 cell vocabulary, §3 acceptance rule, §4 headline rule rather than restating them.

Staging — W1 vs W1b honesty

The landed W1 substrate proves wave-1 lex/grammar/C5-trivia authorities are present and re-derivable from dag.dag (dag_round_trip_wave1_authorities_ready). It does not yet prove emit→ingest bit-identical fidelity on the fixture — that's W1b/T-36, called out verbatim in the landed claim label and in dag_ingest_round_trip.dag:3.

Spec accordingly stages two predicates:

• R3-dag-roundtrip-wave1-ready (W1, landed) — run_test_claim_round_trip_verdict returns Pass.
• R3-dag-roundtrip-fidelity (W1b, T-36 unlanded) — explicit SKIP cell with upstream_blocked:w1b_emit_ingest_comparator_unlanded.

Row aggregate stays FAIL until W1b lands. That's the honest reading of the THESIS rung-3 standard ("round-trip preserved"), not a regression.

Aux-fixture handling

The committed claim_dag_ingest_round_trip binds to dag_round_trip_mvp1, not the ladder fixture. Spec renders that as a parallel diagnostic row phase1-aux/dag_round_trip_mvp1, with the ladder fixture rung-3 row showing dag=SKIP upstream_blocked:claim_nat_semiring_module_roundtrip_not_authored until the migration (joint spec §5 module-loader landing) closes the wedge.

§5 spot-checks (vs origin/main @ 0ace5f8b7)

Confirmed: 05_eval.dag W1 verdict path (:1723-1742) + runtime variant (:1745-1768), dag.dag wave-1 authorities readiness gate (:3168+), C5 trivia DeclaredNormalized (:3160-3166), claim W1/W1b split (dag_ingest_round_trip.dag:3,80), no RoundTripClaim row on nat_semiring (wedge confirmed).

Out of scope (named in §1, §7)

• Leaf-model verification (PR Phase 1 dispatch (PR #3959 §11.4 step 4): R1 fixture generator + runner against rustc for rust.dag per merged leaf-model verification doc. Phase 1 scope: R1 (i32 surface spelling) — emit Rust source 'pub fn r1_test() -> i32 { 0i32 }' as fixture; invoke rustc; capture verdict; falsification probe = e #3972) — orthogonal lane, NOT rung 3.
• R3 for emitted rust/python/go — rung 5 cross-target.
• Rung-4 predicate (companion spec PR docs(planning): rung-4 acceptance predicate spec — phase1/nat_semiring (Rust W2) #3990).
• Rungs 5-9 (Phase 3+).
• Module-loader claim migration (Runtime/TestClaim or Compiler Spine follow-up).
• W1b emit→ingest comparator (T-36 follow-up).

Coordination

• PM (nimble-dove-733) flagged a brief conflation (R1 leaf-model vs rung-3 RoundTrip); STOP-and-clarify escalation resolved with PM confirming option (b): cite W1: RoundTripClaim eval path (ingest⁻¹ on dag target) — PR #3938 §11.4 / joint runner spec §6 #3960, not Phase 1 dispatch (PR #3959 §11.4 step 4): R1 fixture generator + runner against rustc for rust.dag per merged leaf-model verification doc. Phase 1 scope: R1 (i32 surface spelling) — emit Rust source 'pub fn r1_test() -> i32 { 0i32 }' as fixture; invoke rustc; capture verdict; falsification probe = e #3972. This PR ships per the corrected brief.
• Companion specs Ladder/Fixture Manager — authority over 9-rung correctness ladder, fixture set, rung gate shape (acceptance predicates per rung), 'no rustc-clean as headline' enforcement per PR #3938 §11.1. First artifact: nat_semiring × rungs 0-2 acceptance predicate spec; ratify nat_semiring as Phase 1 fixture; d #3946 (rungs 0-2), docs(planning): rung-4 acceptance predicate spec — phase1/nat_semiring (Rust W2) #3990 (rung 4) — see status.
• Cross-lane review welcome from Compiler Spine on §2.2/§2.3 alignment with run_test_claim_round_trip_verdict semantics.

Test plan

• §5 spot-checks re-verified by reviewer against origin/main (re-pin if main advances past 0ace5f8b7).
• Compiler Spine ack on W1/W1b staging vs landed substrate intent.
• No edits to load-bearing files — pure docs/planning addition.
• Headline policy (§4) matches companion specs verbatim where applicable.

🤖 Generated with Claude Code

[briansrls]

Review metadata

• Provider / model: openai-pro / gpt-5-5-thinking
• Commit: 5bb2f8ba · Trigger: manual
• Comparison: main @ 0ace5f8b ... session/zesty-bat-510-rung3 @ 5bb2f8ba
• Conversation: View conversation

---

1. Story of the diff

This PR adds a new planning authority for rung 3 of the v4 ladder on phase1/nat_semiring: it defines how the .dag RoundTripClaim row should be evaluated, how W1 “wave-1 authorities ready” differs from W1b bit-identical emit→ingest fidelity, and how the existing aux fixture should be reported without falsely closing the ladder fixture. The load-bearing mechanism is staged reporting: R3-dag-roundtrip-wave1-ready can prove only the landed W1 substrate gate, while R3-dag-roundtrip-fidelity remains blocked until T-36/W1b; therefore the rung-3 aggregate must remain FAIL until both stages pass. The doc mostly preserves that boundary, but one required headline example contradicts the aggregate rule and would let downstream reports mark aux rung 3 as PASS on W1 alone. chatgpt-review-62bc6cfc-1ece-4a…

2. Invariant categories

1. LAYER MODEL (substrate vs implementation).

N/A — the diff adds a planning doc only; it does not change Dag substrate types, compiler passes, std/ declarations, or runtime code.

1. INVARIANTS.md + modeling-discipline.md.

Finding — P2 Boundary Discipline / single reporting authority: docs/planning/v4-ladder-rung-spec-rung3-2026-05-30.md:183 gives a required headline example of phase1-aux/dag_round_trip_mvp1: rung3 PASS (dag=PASS — W1 wave-1 authorities ready), but the same spec’s aggregate authority says rung-3 PASS requires both W1 and W1b and that the row remains FAIL while W1b is unlanded at docs/planning/v4-ladder-rung-spec-rung3-2026-05-30.md:76. Section 6 repeats the expected aux baseline as rung3: FAIL (dag=SKIP) with upstream_blocked:w1b_emit_ingest_comparator_unlanded at docs/planning/v4-ladder-rung-spec-rung3-2026-05-30.md:222-234. That leaves two authoritative reporting shapes for the same fixture: W1-only PASS vs aggregate FAIL. Fix the headline example to report the W1 stage without making the rung aggregate PASS, e.g. rung3 FAIL (dag=SKIP/W1 PASS; W1b SKIP upstream_blocked:w1b_emit_ingest_comparator_unlanded) or whatever exact cell convention the spec intends.

1. CODING.md.

N/A — no Rust implementation code, APIs, helpers, error shapes, or comments in code are changed; the prose planning artifact itself is the intended deliverable.

1. TESTING.md.

Compliant — for a planning-only PR, it does not need to add executable tests. It does name the future executable receipt anchor, requiring the first nat_semiring RoundTripClaim PR to extend scripts/v4-phase1-nat-semiring-rung-gate.sh and supersede this expected baseline with an executed one at docs/planning/v4-ladder-rung-spec-rung3-2026-05-30.md:239.

1. LOCKED DESIGN DECISIONS.

Compliant aside from the reporting finding above — the doc preserves the high-level “round-trip preserved” standard by explicitly refusing to close rung 3 until W1b bit-identical fidelity lands, rather than treating W1 readiness as the final proof.

1. TRACKED vs UNTRACKED DEBT.

Compliant — the temporary gaps are named and bounded: module-loader-blocked migration of the RoundTripClaim row, W1b/T-36 fidelity comparator, and host gate script/CI extension are all listed as pending with concrete triggers at docs/planning/v4-ladder-rung-spec-rung3-2026-05-30.md:255-257.

2.5. Top-down PM intent review

Finding — brief could cause a worker to report the wrong rung state: the PM-level intent of this spec is “honest staging”: rung 3 is not actually closed until round-trip preservation is proven, and the doc’s own authority says W1 readiness does not prove bit-identical emit→ingest fidelity at docs/planning/v4-ladder-rung-spec-rung3-2026-05-30.md:23. The aggregate rule then makes that operational: rung-3 PASS requires both stages, and W1b-unlanded means aggregate FAIL at docs/planning/v4-ladder-rung-spec-rung3-2026-05-30.md:76. But the required headline example at docs/planning/v4-ladder-rung-spec-rung3-2026-05-30.md:183 tells workers to report the aux fixture as rung3 PASS for W1 readiness alone. A worker following that headline faithfully could publish exactly the semantic dilution the spec is otherwise trying to prevent: a rung-3 PASS without W1b fidelity.

3. Verdict

REQUEST_CHANGES. The spec is otherwise careful and well-scoped, but the contradictory required headline is load-bearing because this PR is itself a worker-facing planning authority. Fixing that one reporting example should align the doc with its own staged aggregate rule.