docs: testgen, invariant lenses, corrections, ownership rendering design

[briansrls]

Summary

Sequences four new commitments into the self-hosting roadmap, all shipping at L1.5 (not deferred to M4):

• §14.1-14.4 Test generation — structural testgen from types (L1.5), behavioral testgen + mocks (L2.6), composition testgen (L3). KF-3 becomes empirical progressively.
• §14.5 Invariant lenses — 7 INVARIANTS.md rules become self-enforcing lenses (layer opacity, decidability, single authority, etc.) running against the compiler's own .dag code.
• §14.6 Diagnostics as corrections — every diagnostic carries the literal fixed code. Roundtrip test pattern: break → diagnose → apply correction → recompile → zero diagnostics.
• §14.7 Ownership + clone elision — dedicated parallel track with design doc (docs/ownership-rendering-design.md). All 5 design questions resolved. Key insight: count consumer NODES not port references — dissolves 200+ lines of v2 reconstruction.

Also adds IL-1 through IL-6 (invariant lens claims) and DC-1 through DC-6 (correction roundtrip claims) to thesis-validation-plan.md.

Files changed

• src/v3/SELF_HOSTING.md — §14 with six subsections, L2.6/L2.7 in dependency diagram, gating rules 6-7
• docs/ownership-rendering-design.md — NEW, 5 dimensions, all questions resolved, Phase 1-3 implementable
• docs/thesis-validation-plan.md — invariant lenses, correction roundtrips, ownership milestones in summary table
• src/v3/ROADMAP.md — M4 testgen + ownership bullets
• ROADMAP.md — KF-3 status update
• src/v3/compiler/src/diagnostics.rs — target shape comment updated with correction field

Test plan

• Design review of ownership rendering design (docs/ownership-rendering-design.md)
• Verify thesis-validation-plan.md summary table counts are consistent
• No code changes — doc + comment only

🤖 Generated with Claude Code

[briansrls]

ChatGPT Review

Principle audit.

1. Fail-closed. Mostly satisfied. The new validation-plan doc usefully forces each thesis claim into TESTED, TESTABLE AT, or DEFERRED with a named blocker, and the new diagnostics material pushes toward break → diagnose → fix → recompile roundtrips instead of silent continuation. I didn’t see a new fail-open path in the docs changes.

2. Illegal states unrepresentable. One NON-BLOCKING concern: Correction = Exact { source: String } | Choice { options: List<Fix> } in src/v3/SELF_HOSTING.md:1828-1833 gives “one valid fix” two representations (Exact, or Choice with one element). That is a parallel representation in the proposed diagnostic model before it even lands in code. I’d flatten this to a single non-empty list-of-fixes shape before the correction: Option<Correction> direction in src/v3/compiler/src/diagnostics.rs:28 hardens.

3. Facts flow forward. One BLOCKING concern: the new ownership design drops a fact the emitter still needs. docs/ownership-rendering-design.md:268-286 resolves fan-out by deduplicating to “distinct consumer nodes,” and Phase 1 immediately maps single=Move, multi=Clone at docs/ownership-rendering-design.md:414-415. That fixes Loop overcounting, but it undercounts same-node multi-use like Transform(x, x): one node, two consuming slots. In Rust that is not equivalent to a single use, so the current design loses semantic multiplicity on the way to emission.

4. Coproduct dissolution. Satisfied in code: no new substrate Rust enum lands in this diff. The only doc-level shape I’d flatten before implementation is again Correction = Exact | Choice; that split looks dissolvable-now, not terminal.

5. Single-authority metadata. One BLOCKING concern: the ownership track now has competing authorities. docs/ownership-rendering-design.md:31-39 says ownership is “a first-class pipeline feature, not a lens,” and docs/ownership-rendering-design.md:268-286 says count distinct consumer nodes. But src/v3/SELF_HOSTING.md:117-119 still says lens_fanout — count port references, and that framing propagates into src/v3/ROADMAP.md:403-409 and docs/thesis-validation-plan.md:417-424. That is exactly the kind of parallel design source that will drift the moment implementation starts.

6. API-level enforcement. Mostly good direction: this PR repeatedly turns “we should test that” into concrete fixture and ratchet plans, which is the right instinct. The blocking gap is that the ownership API boundary still doesn’t name the semantic use unit. Until the design chooses “input slot / role / edge kind” instead of oscillating between raw references and node-counts, the eventual API cannot enforce the invariant structurally.

Design question. What is the semantic unit of ownership consumption: raw input references, distinct behavior nodes, or typed input roles?

That choice is load-bearing for the whole ownership track. Raw reference counts overclone Loop; node-dedup undercounts Transform(x, x); the current docs say both in different places. I think the model wants a richer per-edge or per-input-role fact so bookkeeping references in Loop can coalesce while repeated argument positions still count as two real uses.

Verdict. REQUEST_CHANGES.

This is a strong docs round overall: the thesis-validation mapping is useful, the diagnostics-as-corrections direction is good, and promoting clean bootstrap to L1.5 makes sense. But I would not merge the ownership track as written until the fan-out/consumer model is collapsed to one authority and made semantically sound.

LOOP HEALTH: converging — this round turns several vague claims into named fixtures and milestones, but the ownership/fan-out concept now leaks across multiple docs with conflicting semantics, so fix that once at the model boundary before Phase 1 ratchets fossilize it.

---

View conversation

[briansrls]

codex · gpt-5.4 · fdff8653

⚠️ Review (blocking: 2, non-blocking: 0+/1-)

BLOCKING (2)

Root Cause

• src/v3/compiler/src/dag.rs Loop inputs carry position (source/init/bound.count) but no ownership-role authority, so the design compensates with node-counting → add explicit per-input role/edge-kind facts and derive semantic consumer count from that authority.
• docs/ownership-rendering-design.md Container sharing is still treated as an optimization knob instead of a required ownership fact → make the escaping multi-consumer path choose the shared carrier in the target spec/phase plan, not a post-ratchet refinement.

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

• docs/thesis-validation-plan.md A few TESTED rows are ahead of the current v3 implementation: emit_rust still does not emit record fields, and v3 diagnostics are still ResolveError/generic rather than FieldNotFound/NonExhaustiveMatch; tightening those rows would keep the validation plan single-authority (roadmap lane: L1.5 diagnostics/testgen sync).

ROADMAP — Verified

• KF-3 layering: The new structural/behavioral/compositional split makes the verification-from-structure claim schedulable instead of leaving it as one late-stage promise.

ROADMAP — Incomplete

• ownership rollout: SELF_HOSTING.md §14.7 and docs/ownership-rendering-design.md §6 still disagree about whether fold/lambda ownership work is already dissolved or remains a distinct L2 phase, so the rollout is not yet single-authority.

⚠️ The testgen/correction direction is strong, but the ownership design still resolves two load-bearing v2 lessons by collapsing facts the current invariants say must stay explicit.

[briansrls]

BLOCKING: Q1 resolves fold linearity by deduplicating Loop.source, Loop.init, and bound.count into one consumer, but those are already distinct substrate roles and v2 ownership only excludes some roles via explicit edge kinds, so this collapses semantics instead of letting facts flow forward.

[briansrls]

BLOCKING: The Rust SharingModel sets multi_consumer_escaping to Clone, even though FF-8 already root-causes escaping multi-consumer containers to shared representation rather than O(n) clone fallback; leaving RcWrap as a later refinement keeps the known bug class inside the "resolved" design.

[briansrls]

codex · gpt-5.4 · fdff8653

⚠️ Review (blocking: 2, non-blocking: 0+/1-)

BLOCKING (2)

Root Cause

• src/v3/compiler/src/dag.rs Loop inputs carry position (source/init/bound.count) but no ownership-role authority, so the design compensates with node-counting → add explicit per-input role/edge-kind facts and derive semantic consumer count from that authority.
• docs/ownership-rendering-design.md Container sharing is still treated as an optimization knob instead of a required ownership fact → make the escaping multi-consumer path choose the shared carrier in the target spec/phase plan, not a post-ratchet refinement.

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

• docs/thesis-validation-plan.md A few TESTED rows are ahead of the current v3 implementation: emit_rust still does not emit record fields, and v3 diagnostics are still ResolveError/generic rather than FieldNotFound/NonExhaustiveMatch; tightening those rows would keep the validation plan single-authority (roadmap lane: L1.5 diagnostics/testgen sync).

ROADMAP — Verified

• KF-3 layering: The new structural/behavioral/compositional split makes the verification-from-structure claim schedulable instead of leaving it as one late-stage promise.

ROADMAP — Incomplete

• ownership rollout: SELF_HOSTING.md §14.7 and docs/ownership-rendering-design.md §6 still disagree about whether fold/lambda ownership work is already dissolved or remains a distinct L2 phase, so the rollout is not yet single-authority.

⚠️ The testgen/correction direction is strong, but the ownership design still resolves two load-bearing v2 lessons by collapsing facts the current invariants say must stay explicit.

[briansrls]

ChatGPT Review

Principle audit.

1. Fail-closed. Mostly satisfied. The new docs push in the right direction: docs/thesis-validation-plan.md now maps thesis claims to concrete milestones and fixtures, and src/v3/SELF_HOSTING.md’s diagnostics-as-corrections section is explicitly break → diagnose → fix → recompile instead of “report and hope.” I did not see a new fail-open path in the changed material.

2. Illegal states unrepresentable. One BLOCKING concern: the proposed mock authority type admits invalid mocks. MockRealization { source: DeclarationId, strategy: MockStrategy } with MockStrategy = DefaultInhabitant | FixedValue { value: Value } | FailWith { error: Value } at src/v3/SELF_HOSTING.md:1685-1695 allows at least three illegal states: a fixed value that does not inhabit the source arrow’s return type, FailWith on a declaration whose return type has no error branch, and an error payload that does not match that branch. For a substrate test authority, those should be unrepresentable, not checked later by convention.

3. Facts flow forward. One BLOCKING concern, same root cause: the new test authority layer stops naming which existing substrate facts are actually flowing. TestClaim { subject: Expression, predicate: Predicate } is introduced as “the structural authority for what a test IS” at src/v3/SELF_HOSTING.md:1611-1631, but the doc never says whether Expression means a computation node, a declaration ref, a rendered snippet, or something else. The same problem shows up in MockStrategy’s raw Value payloads at 1685-1695. Under the thesis’s two-substrate model, this is exactly where I want the doc to name the lowering target instead of introducing opaque carriers.

4. Coproduct dissolution. Satisfied for this diff. No new substrate Rust enum lands. I am not re-opening the already-raised Correction = Exact | Choice point here.

5. Single authority. Mostly satisfied, and this round is stronger than the previous one. docs/thesis-validation-plan.md is a real improvement because it gives one claim → milestone/fixture map instead of leaving KF-3 and related claims as loose aspirations. My only concern is that unless Expression / Predicate / raw Value are dissolved into named substrate refs, std/verification.dag will become a parallel authority for “what is being tested” rather than a reader of the existing substrates.

6. API-level enforcement. One BLOCKING concern: the current testgen API would rely on unwritten rules. Nothing in TestClaim forces subject and predicate to be existing substrate forms, and nothing in MockRealization forces the stubbed value to match the source declaration’s type or error shape (src/v3/SELF_HOSTING.md:1611-1631, 1685-1695). A contributor can construct an invalid test artifact unless they already know the convention. That is the opposite of API-level enforcement.

Design question. Are generated tests and mocks ordinary data over the existing two substrates, or is std/verification.dag introducing a third opaque test-language layer?

That is the load-bearing question for this round. The thesis commits v3 to two coordinated substrates, not a third carrier layer, and the active design rule is that a doc has to name the existing substrate element that expresses new semantics before calling the feature ready. Right now Expression, Predicate, and raw Value read like placeholders for “something test-ish” rather than named substrate forms. If they are really aliases for existing refs, the doc should say exactly which ones now; if not, the feature needs an option walk before L1.5 is treated as settled.

Verdict. REQUEST_CHANGES.

This is a strong docs round overall: the validation mapping is materially better, and the ownership doc is much clearer than the earlier iteration. Setting aside the already-raised ownership follow-ups, the new blocker for me is the test authority layer — I would not lock in the L1.5 testgen/correction story until those authority types lower cleanly to existing substrate forms and make invalid mocks unrepresentable.

LOOP HEALTH: converging — this round turns vague thesis claims into named milestones and fixtures, and the blocker is a real model-boundary question rather than more scattered cleanup, but it should be fixed now before std/verification.dag grows consumers.

---

View conversation

[briansrls]

codex · gpt-5.4 · dae1c78a

⚠️ Review (blocking: 1, non-blocking: 0+/2-)

BLOCKING (1)

Root Cause

• src/v3/SELF_HOSTING.md The testgen design did not consume the existing std/verification.dag authority already cited by src/v2/tests/testing-strategy.md → either align §14.1 to the current AssertKind/TestClaim/TestCase schema or replace that authority atomically in the same design change.

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

• docs/ownership-rendering-design.md Dimension 1 reuses the name ValueSemantics for source immutability even though dsl/std/languages.dag already uses ValueSemantics for target passing rules, so rename or explicitly compose the two axes before L2.7 to keep ownership terminology single-authority.
• ROADMAP.md KF-3 now points readers to SELF_HOSTING.md §15, but the staged testgen design lives in §14, so fix the citation to keep the roadmap cross-reference reliable.

⚠️ The staged testgen/correction direction is strong, but §14.1 currently forks the existing verification substrate instead of extending its single authority.

[briansrls]

BLOCKING: §14.1 redefines TestClaim/TestCase as new authority shapes even though dsl/std/verification.dag already defines those substrate types, violating single-authority and forking the test model before L1.5.

[briansrls]

codex · gpt-5.4 · dae1c78a

⚠️ Review (blocking: 1, non-blocking: 0+/2-)

BLOCKING (1)

Root Cause

• src/v3/SELF_HOSTING.md The testgen design did not consume the existing std/verification.dag authority already cited by src/v2/tests/testing-strategy.md → either align §14.1 to the current AssertKind/TestClaim/TestCase schema or replace that authority atomically in the same design change.

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

• docs/ownership-rendering-design.md Dimension 1 reuses the name ValueSemantics for source immutability even though dsl/std/languages.dag already uses ValueSemantics for target passing rules, so rename or explicitly compose the two axes before L2.7 to keep ownership terminology single-authority.
• ROADMAP.md KF-3 now points readers to SELF_HOSTING.md §15, but the staged testgen design lives in §14, so fix the citation to keep the roadmap cross-reference reliable.

⚠️ The staged testgen/correction direction is strong, but §14.1 currently forks the existing verification substrate instead of extending its single authority.

[briansrls]

Meta-review in progress... (view conversation)

Loop-health check: is this review cycle making forward progress, or shifting debt? Posts in ~5-15 minutes.

[briansrls]

ChatGPT review in progress... (view conversation)

Check back in ~30 minutes for the full review.