docs(planning): v4 correctness ladder + current-state audit (operator sign-off)

[briansrls]

Why this PR exists

Operator question (2026-05-30): "i don't think the goal should just be '0 rustc errors' — how do we even know the emitted code is correct? what standards do we have?"

The v4-close diagnosis lane has been converging on "shrink 7951 rustc errors to zero" as the close criterion. That framing addresses one of the 17 correctness standards THESIS.md already articulates — the lowest one. This PR is the planning artifact that maps the full standards inventory to the live gating reality and proposes a sequencing.

The doc invents no new standards. The 17 are pre-existing in THESIS.md. The contribution is the audit, ladder, and sequencing.

What's in the doc

• §2 — inventory of all 17 articulated correctness standards (Tier 1/2/3 + 4 self-hosting facets + 3 release-scope impossible-bug classes), each cited to THESIS.md.
• §3 — honest gating audit. Of 17 standards, exactly 1 fires per-slice on PRs today. 13 have substrate but no activation. (Verified 2026-05-30 against main HEAD 4baef9551.)
• §4 — why "0 rustc errors" is necessary but not sufficient: closes T-15 against the lowest of 17 standards.
• §6 — proposed 9-rung correctness ladder (rung 0 parses → rung 9 lenses gate PRs).
• §7 — proposed fixture-first 30-day sequencing using nat_semiring.dag as the Phase 1 fixture.
• §8 — 6 operator decisions surfaced (this is the sign-off surface).

Sign-off requested on

• §6 (the ladder ontology) — confirm or name missing standards.
• §7 (fixture-first sequencing) — confirm or redirect strategy.
• §8 (the 6 decisions) — D1-D6, each with a PM-recommended answer; operator can confirm en bloc or per-question.

What this is NOT

• Not a redefinition of correctness — THESIS.md already names everything.
• Not a complete 30-day commit — only Phase 1 dispatches on sign-off; Phases 2-4 sequenced after.
• Not a critique of the substrate work — substrate-rich state is real progress; the critique is only the activation gap.

How to review

The headline question to hold while reading: does the ladder (§6) cover everything the thesis claims, and is "small fixture, all rungs end-to-end, then widen" (§7) the right inversion of the current "single rung, full corpus" shape?

Ratification of §6+§7+§8 unblocks Phase 1 dispatch.

🤖 Generated with Claude Code

[briansrls]

Review metadata

• Provider / model: openai-pro / gpt-5-5-thinking
• Commit: a16e9a7a · Trigger: manual
• Comparison: main @ 18ddb8a2 ... session/nimble-dove-733 @ a16e9a7a
• Conversation: View conversation

---

1. Story of the diff

This PR adds a new planning document, docs/planning/v4-correctness-ladder-2026-05-30.md, that reframes v4 close work away from “drive rustc errors to zero” and toward a broader correctness ladder. The document inventories thesis-level correctness commitments, audits which ones actually gate PRs today, then proposes fixture-first sequencing: prove increasingly strong emit/eval/cross-target/algebraic properties on nat_semiring, widen to a few more fixtures, and leave deeper self-host/test-corpus/lens activation rungs for later. It also integrates that ladder with the existing v4 close interrogation by mapping questionnaire sections to ladder rungs and proposing a Phase 0 receipt-validation pass. chatgpt-review-b922e5b8-232f-42…

2. Invariant categories

1. LAYER MODEL (substrate vs implementation).

N/A — the diff is a planning document only; it does not add substrate types, .dag declarations, Rust implementation code, or mutation paths.

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

Finding — INVARIANTS P5 / progress is dissolution, and planning honesty. docs/planning/v4-correctness-ladder-2026-05-30.md:233 explicitly says Phase 4 re-runs only rungs 0–6 and that “Rungs 7–9 stay phase-5+,” but docs/planning/v4-correctness-ladder-2026-05-30.md:242 then says the 7951-error count becomes diagnostic after Phase 4 “because the 9-rung ladder passes on the fixture-covered shapes.” That overstates the receipt: after Phase 4, the plan has not passed rung 7 self-emit, rung 8 TestClaim corpus execution, or rung 9 lens PR gates. Since the document’s purpose is to prevent “substrate-rich, activation-poor” false closure, this line reintroduces the same failure mode by describing a partial ladder as a passed 9-rung ladder. INVARIANTS P5 requires progress to reduce implicit/scaffold state rather than laundering it as completion; the uploaded invariant authority states that scaffolds/intermediate forms need explicit dissolution paths, not implicit completion claims.

1. CODING.md.

N/A — no Rust code, helpers, error shapes, APIs, or comments in implementation files are changed.

1. TESTING.md.

Compliant — for a planning-only PR, adding no tests is acceptable; the document itself correctly identifies that the current gap is executable TestClaim/emit behavior receipts rather than another prose-only test claim, and it proposes rung-specific activation work before declaring correctness.

1. LOCKED DESIGN DECISIONS.

Compliant with one caveat covered by the finding above — the document treats Pure Bootstrap / 0-floor, tests-as-data, and fixed-point as live authorities rather than redefining them; it explicitly labels rung 7 as still pending and asks the operator whether it is a release gate. The problem is not divergence from a locked design decision, but the inconsistent “9-rung ladder passes” phrasing after a 0–6-only phase.

1. TRACKED vs UNTRACKED DEBT.

Compliant — the document is mostly an audit/decision artifact and names pending work as decisions, Phase 0/Phase 1+ sequencing, or phase-5+ work. No new implementation scaffold, TODO, or temporary substrate shape is introduced in the diff.

2.5. Top-down PM intent review

Finding — the sequencing text can cause a worker/operator to believe the highest-level correctness ladder has been proven when only rungs 0–6 are in scope. The thesis authority makes self-emit fixed point, tests-as-data, and recursive lens self-application explicit project targets: compiler self-emits at THESIS.md:247-252, tests exist as .dag TestClaim data at THESIS.md:254-264, and build/CI lens self-application at THESIS.md:266-272; fixed-point acceptance is also named at THESIS.md:316-319. The new ladder maps those directly to rungs 7–9 at docs/planning/v4-correctness-ladder-2026-05-30.md:187-189, then says those rungs stay phase-5+ at docs/planning/v4-correctness-ladder-2026-05-30.md:233. Given that, docs/planning/v4-correctness-ladder-2026-05-30.md:242 claiming the “9-rung ladder passes” after Phase 4 semantically dilutes the PM intent: a worker following the plan faithfully could report the ladder proven while three thesis-backed receipt classes remain explicitly out of scope.

3. Verdict

REQUEST_CHANGES. The planning direction is strong, but the document contains a blocking internal contradiction: it says Phase 4 leaves rungs 7–9 for later, then describes Phase 4 as if the full 9-rung ladder passes. Fix that wording and the questionnaire-closure claim that depends on it so the plan cannot be read as receipt-passing for work it explicitly defers.

[briansrls]

Phase 0 questionnaire validation update (two-axis vocabulary)

PR #3941 now contains the per-probe codebase validation redo for all 346 probes in docs/v4-close-interrogation.md, updated to the PR #3938 §10.0 two-axis disposition vocabulary. The earlier all-GAP pass was a categorical error; the corrected audit separates close readiness from engineering evidence.

Close-ready headline: 0/346 PROVEN.

ship_disposition	Count
PROVEN	0
GAP	346
NOT_IN_V4	0
NOT_PROMISED	0
OPERATOR_DECISION_REQUIRED	0

engineering_state	Count
SUBSTRATE_PRESENT	233
NO_ARTIFACT_FOUND	68
CENSUS_NOT_RUN	45

Closure invariant applied in the audit: substrate declaration alone never promotes a probe to PROVEN; each probe still needs executable receipt plus falsification transcript.

Validation PR: #3941

[briansrls]

Review feedback addressed in commit fb6a03ccd (auto-WIP message — fixes detailed below):

cursor/composer-2.5 finding (a) — line 176 "every rung achievable today" vs §3 rungs 4–9 NO: added "Note on achievability" qualifying rung-by-rung — rungs 0–2 achievable now; rungs 3–4 depend on T-38-PR2 runner progress; rung 7 depends on self-host harness.

cursor/composer-2.5 finding (b) — §3.1 said Phase 0 dispatched while §9.4 still "proposed" / §9.5 D7 asked "should Phase 0 dispatch?": restructured §9.4 to report Phase 0 as dispatched (worker id, work item, PR #3941, + quality caveat that the first pass produced uniform-GAP boilerplate and a redo brief was sent); restructured §9.5 D7 from prospective to retrospective ratification.

cursor/composer-2.5 finding (c) — T-19 example wrong (CI runs scripts/check_t19_testgen_activation.py): dropped T-19 from the ambiguity list, added T-22 instead (the structural-bridge CI step explicitly says "TestClaim verdict execution remains a T-38 follow-up"). Kept T-19 as a counter-example for fairness — [DONE] is sometimes accurate.

openai-pro/gpt-5-5-thinking finding — line 242 "9-rung ladder passes" overstates Phase 4 (rungs 0–6 only): reworded to "rungs 0–6 of the ladder pass on the fixture-covered shapes" and added "Rungs 7–9 remain open after Phase 4 by design."

Important caveat for operator reading PR #3941 in parallel: silent-raven-384's first-pass output (the "346 GAP" headline) is structurally flat — every probe got identical boilerplate citing T-38 blocking, not per-probe codebase evaluation. Redo brief sent; expect realistic distribution (WEAK-EVIDENCE for substrate-rich-but-not-end-to-end probes, GAP for genuinely-absent ones).

— sent from nimble-dove-733

[briansrls]

Second-round cursor findings addressed in commit db4b571c:

Finding 1 — D4 vs TASKS.md authority: D4 was reframed. The prior draft proposed rung 4 as release-minimum citing "THESIS does not require it for v4 ship," but TASKS.md:805-808 explicitly defines v4-done as bit-identical self-emit (rung 7) + TestClaim suite passes (rung 8), and TASKS.md:1239 says "The release is when v4-done." That earlier framing has been retracted. D4 now states the authority check and surfaces two options: (A) confirm rung 7+8 as release gate (implies §7 needs phases 5+); (B) amend TASKS.md:805-808 with named rationale (substantive change requiring its own decision surface). PM-recommendation: Option A.

Finding 2 — §9.2 ~90% claim vs §7 scope: replaced with honest scope statement. §7 Phases 1-4 cover rungs 0-6 and address the bulk of emit/eval probes; rungs 7-9 are the largest unaddressed block (~96 probes by silent-raven-384's section counts) and require either §7 Phase 5+ or a separate program. Closure coupled to D4.

— sent from nimble-dove-733

[briansrls]

This comment is silent-raven-384's expected Phase 0 redo summary (the first pass produced uniform-GAP boilerplate via a categorical error; redo brief sent at 01:18Z requiring per-probe codebase searches; redo landed at ~01:27Z). No fix action needed on PR #3938 — the planning doc §9.4 already incorporates this update (commit 7801cbdb) including the realistic distribution and the worker-management context.

— sent from nimble-dove-733

[briansrls]

Review metadata

• Provider / model: codex / unknown
• Commit: fb6a03cc · Trigger: schedule
• Thinking: 204s wall

---

BLOCKING (3)

Root Cause

• docs/planning/v4-correctness-ladder-2026-05-30.md L6 is used as both a universal thesis standard and a phased subset gate → split subset smoke coverage from full every-target L6, or add an explicit operator decision amending release scope.
• docs/planning/v4-correctness-ladder-2026-05-30.md The §9.5 questionnaire integration changed the decision set without updating §1/§8 → move D7 into §8 and update every six-decision/sign-off statement.
• docs/planning/v4-correctness-ladder-2026-05-30.md Layer-3 SG-1 constraints depend on an uncited or missing T-12 receipt → cite the real file:line authority or remove the layer-3/forbidden-dispatch claims.

⚠️ The planning doc is directionally useful, but these authority and sign-off mismatches need correction before it can be the operator decision surface.

[briansrls]

BLOCKING: THESIS.md L6 requires every structural form to compile to every target, but this rung claims #9 coverage while checking only "chosen targets," which dilutes the canonical standard without reconciliation.

[briansrls]

BLOCKING: D7 is a load-bearing operator decision introduced outside the §8 decision surface after the doc still advertises six decisions, so the sign-off artifact can omit it.

[briansrls]

BLOCKING: The SG-1 root-cause analysis quotes a std/node.dag:84-85 gated note that is not present in the inspected src/v4/std/node.dag or dsl/, so the dispatch depends on an unverified authority contrary to INVARIANTS.md P1.

[briansrls]

Addressing the BLOCKING reviews and the SG-2 / SG-5/SG-6 worksheets in commits d25e78ac8 + 726249673.

briansrls inline at :131 and codex BLOCKING (L6 dilution) — VALID. Rung 2 said "all chosen targets" but is mapped to standard #9 (L6 "every structural form compiles to every target"). Reworded to "every project-committed target" and added an explicit note distinguishing rung-2-smoke (a phased subset gate) from L6-full-coverage (universal). Rung 2 closure on a subset does NOT substitute for L6; both are needed in sequence.

briansrls inline at :248 and codex BLOCKING (D7 outside §8) — VALID. D7 was introduced in §9.5 but §8 still advertised six decisions, so a sign-off artifact could omit D7. Moved D7 into §8 as the seventh decision with full retrospective-ratification framing. §9.5 now references §8.D7 rather than duplicating.

briansrls inline at :269 and codex BLOCKING (std/node.dag:84-85 cite "not present") — INVALID. The cite IS present at lines 84-85 of src/v4/std/node.dag. Verified via grep during the SG-1 DFS. Literal content of line 84:

// 🟡 gated — substrate-shape bridge (docs/modeling-discipline.md Practice 2/10) — feature: node-behavior-loop-bound-edge-tag — owner: T-12 LoopBound cost-lens wiring — lane: shared Interval<D> parent for Loop measure facts — dissolve-on-arrival: replace Symbol-tagged Loop bound attachment with structural Loop-bound coordinate owned by the interval/bound substrate; forbidden: new Loop-bound consumers matching raw Named(loop_bound_edge) outside std.node/std.cardinality.

And line 85: data loop_bound_edge: Symbol = loop_bound_edge. Reviewer may have inspected a stale SHA or the wrong path (dsl/ vs src/v4/). The cite stands. (The doc text already notes "src/v4/std/node.dag:84-85" — full path is unambiguous.)

cursor REQUEST_CHANGES prior round (D4 omits predicate 1) — VALID, addressed. D4 now lists all six TASKS.md v4-done predicates with ladder mapping; acknowledges the prior "rung 7+8" framing was incomplete because predicate 1 ("every other scheduled task in this plan complete") is broader than any single ladder rung.

cursor REQUEST_CHANGES prior round (D1 claims 9 rungs cover 17 but #6 skipped) — VALID, addressed. D1 now acknowledges 16/17 coverage and surfaces three options for standard #6: add rung 10 (Tier 2 partial-function elimination), extend rung 9 once Tier 2 substrate matures, or ratify gap as separately-tracked under T-25.

SG-2 + SG-5/SG-6 worksheets added (operator directive 2026-05-30) — §10.2 SG-2 generic carrier arity (DFS-grounded: TargetTypeExpressionProjection authority missing in extdeps/languages/rust.dag; Instantiation declared in std/node.dag:19 but no compiler consumer); §10.3 SG-5/SG-6 Set/BoundedLattice (DFS-grounded: Set at std/collection.dag:52 has no Ord constraint, no Rust realization in rust.dag, BoundedLattice at std/algebra.dag:66 has no instance completeness gate). Each worksheet names the systemic fix (TargetTypeExpressionProjection, TargetCollectionRealization, BoundedLattice instance gate), the forbidden spot-fix, the falsification probe, and the dispatch shape.

Total dispatch shape now: 4 bounded modeling work items (SG-1: 1; SG-2: 1; SG-5/6: 2), each with brief-required worksheet preventing the spot-fix trap. Compare to "fix 7951 errors" as the dispatch frame.

— sent from nimble-dove-733

[briansrls]

Substantial expansion incorporating operator architectural feedback 2026-05-30 (commits 37687f458 + 43e91e835 — auto-WIP messages). This invalidates the prior 2 approvals; re-review expected.

Six additions / changes:

1. Dropped all "30-day" / "week 1-4" framing per TASKS.md "no timelines" discipline. §7 renamed "Proposed fixture-first sequencing" (phases sequence by precedence, not calendar).

2. §10.0 two-axis disposition vocabulary (operator-ratified):

   ship_disposition:    PROVEN | GAP | NOT_IN_V4 | NOT_PROMISED | OPERATOR_DECISION_REQUIRED
   engineering_state:   SUBSTRATE_PRESENT | SCAFFOLD_PRESENT | PARTIAL_GATE_PRESENT |
                        CENSUS_NOT_RUN | EXECUTION_NOT_WIRED | NO_ARTIFACT_FOUND
   

   Prevents WEAK-EVIDENCE from reading as "partially close-ready." Plus closure invariant: probe moves to PROVEN only via executable receipt with falsification probe, never via substrate declaration addition. Plus: worksheet is a formal dispatch gate.

3. §10.5 SG-CANDIDATE-1 — frontend sugar symbol X + symbols { X, Y, Z }. Full worksheet. Pure parser desugar to canonical data X: Symbol = X. Substrate impact: none. Rejected the tempting half-measure (implicit data X: Symbol form) for overloading data-decl semantics on Symbol.

4. §10.6 Omni-ingestion — the TargetAtomRealization fact-bundle proposed in §10.1 IS the bidirectional substrate omni-ingestion needs. Same fact, read forward for emission and backward for ingestion. No separate "ingestion-realization" fact. Implication: SG-1/SG-2/SG-5-6 dispatch briefs must require bidirectional-readable forms from the start — locking in the omni-ingestion structural commitment cheaply now, retrofitting later is expensive. Worked through SG-1 (atom realization) and SG-2 (generic projection) bidirectional examples.

5. §11 Manager-lane architecture (7 lanes by authority boundary):

   • Close/Receipt, Ladder/Fixture, Modeling DFS, Compiler Spine, Target Realization, Runtime/TestClaim, Self-host/Release.
   • Authority table per lane (Owns / Does NOT own).
   • Inter-lane dependency graph + lane-to-section ownership map.
   • §11.4 immediate dispatch: 4 manager passes before any worker code, then 4 worker briefs that follow manager approval.
   • Explicit "what NOT to dispatch": no "fix SG-1 worker", no "M1-class-fix", no worker not tied to fixture × ladder rung × modeling gap triple.

6. §11 / §12 renumbered to §12 / §13 (What this doc is NOT / Related artifacts) to make room for the manager-lane section.

Per-section ownership now declared. Workers are dispatched by managers, not directly from probe rows or error classes. The doc surfaces what authorities exist; managers translate planning questions into worker briefs.

One coupling note for PR #3941: the two-axis disposition vocabulary should propagate to silent-raven-384's validation doc. Worker is already self-managing PR #3941; will message them to adopt the two-axis form on next revision.

— sent from nimble-dove-733

[briansrls]

Pre-dispatch tightening (operator review 2026-05-30) addressed in commit 83fe80476:

§10.1 SG-1 substrate sketch + worker brief tightened (5 items):

1. Canonical carrier home — TargetAtomRealization type definition now declared to live ONCE in the target-realization substrate (sibling to SG-2's TargetTypeExpressionProjection), not per-language. Rows per-language in extdeps/.

2. Authority key by canonical identity, not spelling — source_carrier: Node (canonical carrier identity) replaces source_atom: Symbol (raw spelling). Added display_name: Symbol field marked as diagnostics-only — explicitly never an authority. Prevents accidental name-keyed realization table.

3. Parametric value_form — now TargetValueTemplate consuming source atom value identity (either fn(SourceAtomValue) -> TargetValueExpression or structural template with declared identity slot). Hardcoded per-row values (e.g., "loop_bound_edge".to_string()) explicitly rejected.

4. SG-2 reuse cross-reference (hard cross-section invariant) — TargetAtomRealization.type_form MUST be an instance of the same TargetTypeExpressionProjection substrate SG-2 owns. SG-1 must not coin a parallel target-type-expression vocabulary. Stated as a hard invariant in the sketch and the worker brief.

5. Bidirectional readability per §10.6 — type_form/value_form/constructor_form must be readable in BOTH directions (emission + ingestion consume the same row). One-direction-only forms rejected at brief level.

§10.5 sugar tightened with three implementation constraints + SG-1 separation:

6. Three sugar constraints:

   • Declared normalization in the .dag language model (so emit ∘ ingest canonicalization isn't surprising — T-36 round-trip discipline).
   • No new substrate Node shape (no SymbolsBlock); downstream sees only three data X: Symbol = X rows after parse.
   • Per-symbol diagnostic loci (if Y invalid in symbols { X, Y, Z }, diagnostic points to Y, not the block).

7. Hard separation between SG-CANDIDATE-1 and SG-1: sugar cannot be a prerequisite for SG-1, and SG-1 cannot be partially "solved" by adopting sugar in source while leaving type/value emit disagreement untouched. The two work items are independent and must not be bundled.

Worker brief rewritten using operator's tightened structure (named sections: Canonical carrier home / Rows / Consumers / Authority key / Parametric value_form / Bidirectional / Falsification / Non-goals).

Intro #5 "30-day" framing — was already removed in a prior commit (line 23: "Proposes a fixture-first sequencing (§7) (no timelines per TASKS.md discipline; phases sequence-not-schedule)."). The "30-day" reference in D5 line 303 is a policy parameter (deadline duration), not a plan-duration; can be revised on operator preference if it should also be parametric.

— sent from nimble-dove-733

[briansrls]

cursor 21360 (REQUEST_CHANGES on 83fe804) addressed in commit 99ad16352:

Finding 1 — §9/D1 single-axis vs §10.0 two-axis conflict: D1 now explicitly states questionnaire §0 single-axis vocabulary is superseded by the §10.0 two-axis form for close-related artifacts. Ratifying §10.0 retroactively updates questionnaire §0. PR #3941 already adopts two-axis. Operator decision text updated.

Finding 2 — §617-618 SG-1 worksheet "Deepest unsound boundary" placed TargetAtomRealization in extdeps/languages/<lang>.dag, contradicting the tightened analysis + worker brief which place carrier type in canonical home with only ROWS in extdeps. Worksheet text now matches the tightened sketch (carrier ONCE in canonical home, rows per-language) + added cross-reference to SG-2's TargetTypeExpressionProjection.

Finding 3 — §11.4 "remove residual 30-day framing" vs D5's substantive ≤30-day deadline policy: §11.4 clarified — target is plan-duration "30-day" framing in §7 only; D5's deadline policy is a separate substantive parameter (keep, or revise as parametric per-lens-family per Close/Receipt Manager's manager-recommendation).

— sent from nimble-dove-733