Skip to content

docs(wishlist): R4.C — correct Lens<C> vs emission conflation (codex BLOCKING on PR #2791) - #2800

Merged
briansrls merged 6 commits into
mainfrom
docs/wishlist-r4c-blocking-fix-forward-2026-05-12
May 12, 2026
Merged

briansrls merged 6 commits into
mainfrom
docs/wishlist-r4c-blocking-fix-forward-2026-05-12

Conversation

@briansrls

Copy link
Copy Markdown
Contributor

Summary

Fix-forward for codex BLOCKING posted on already-merged PR #2791 at 2026-05-12T21:47:34Z (at WISHLIST.md:109).

Codex finding

BLOCKING: R4.C assigns target codegen to the Lens shape, but the locked lens/emission docs keep Lens as a per-Behavior analysis fold and emission/L4/L6 outside that shape, so this violates P2 single-authority for projection mechanisms.

Verification — finding is VALID

Locked design docs are explicit that Lens<C> is NOT the emission projection mechanism:

  • docs/design-emission-model.md:959: "L6 is a substrate-load-time cross-product completeness check, NOT a Lens<C> instance"
  • docs/design-emission-model.md:1107: "Correct = L4 emit/eval match... Not a Lens<C> instance (per codex BLOCKING f5f63c7d9): Lens.read cannot read emitted target artifacts"
  • docs/design-emission-model.md:1111: "structural-fold properties (Faithful, Performant, structural-Minimal) are Lens<C> instances reading substrate facts. Runtime-equivalence properties (Correct = L4 emit/eval match) live in T-Verification-L4-L7-Direct as corpus-driven harness — NOT lens instances"
  • docs/design-lens-framework.md:310,369: Lens<C>.read: (Dag, Behavior) → Witness<C> is per-Behavior; emission/L4/L6 input space is per-(form × target) — different input spaces, not the same shape

Existing Rust/Python/Go target codegen is NOT done via Lens; it's done via the emission pipeline (separate authority documented in design-emission-model.md). My PR #2791 R4.C wish text said "same Lens shape as existing Rust / Python / Go target codegen" — this conflated lens (analysis) with emission (projection), violating P2 single-authority.

Fix

The R4.C wish text now:

  1. Names emission-pipeline shape (not Lens) for the projection mechanism
  2. Explicitly cites the locked-doc line ranges that distinguish lens-from-emission (docs/design-emission-model.md:959,1107,1111 + docs/design-lens-framework.md:310,369)
  3. Names the valid Lens<C> uses (Lens<FaithfulnessVerdict>, Lens<PerformanceVerdict>, structural-Lens<MinimalityVerdict> per design-emission-model.md:1106-1111) as lenses ABOUT emission outputs — folds over substrate facts characterizing emission, not the emission projection itself

The other R4.C wish content (orthogonal-to-LLVM framing, why these matter, open questions, composes-with-R4.B) is unchanged — only the conflated single sentence is corrected.

Diff

- **Wish (operator 2026-05-12)**: extend the emission projection set to include **machine code**, **assembly**, and **LLVM IR text** as native emission targets — same Lens<C> shape as the existing Rust / Python / Go target codegen, just at lower levels in the toolchain stack.
+ **Wish (operator 2026-05-12)**: extend the emission projection set to include **machine code**, **assembly**, and **LLVM IR text** as native emission targets — same emission-pipeline shape as the existing Rust / Python / Go target codegen (per `docs/design-emission-model.md`), just at lower levels in the toolchain stack. **Not** a `Lens<C>` instance — emission lives outside the lens framework per `docs/design-emission-model.md:959,1107,1111` and `docs/design-lens-framework.md:310,369` (Lens<C> is per-Behavior structural fold; emission targets are corpus-driven projection through the emission pipeline). Lenses *about* emission outputs (`Lens<FaithfulnessVerdict>`, `Lens<PerformanceVerdict>`, structural-`Lens<MinimalityVerdict>` per `design-emission-model.md:1106-1111`) are folds over substrate facts characterizing emission; they are not the emission projection itself.

Test plan:

🤖 Generated with Claude Code

…BLOCKING #10458)

PR #2791 R4.C wish line claimed "same Lens<C> shape as the existing Rust / Python / Go target codegen". This violates P2 single-authority per locked design docs:

- `docs/design-emission-model.md:959` — "L6 is a substrate-load-time cross-product completeness check, NOT a `Lens<C>` instance"
- `docs/design-emission-model.md:1107` — "Correct = L4 emit/eval match... Not a `Lens<C>` instance (per codex BLOCKING `f5f63c7d9`): `Lens.read` cannot read emitted target artifacts"
- `docs/design-emission-model.md:1111` — "structural-fold properties (Faithful, Performant, structural-Minimal) are `Lens<C>` instances reading substrate facts. Runtime-equivalence properties (Correct = L4 emit/eval match) live in T-Verification-L4-L7-Direct as corpus-driven harness — NOT lens instances"
- `docs/design-lens-framework.md:310,369` — Lens<C>.read is per-Behavior; emission/L4/L6 input space is per-(form × target), not per-Behavior

Existing Rust/Python/Go target codegen is NOT done via Lens<C>; it's done via the emission pipeline (separate authority). Lenses ABOUT emission outputs (FaithfulnessVerdict, PerformanceVerdict, structural-MinimalityVerdict per design-emission-model.md:1106-1111) are folds over substrate facts characterizing emission — not the emission projection itself.

Fix: rewords the wish to (a) name emission-pipeline shape (not Lens<C>) for the projection mechanism, (b) explicitly cites the locked-doc line ranges that distinguish lens-from-emission, (c) names the valid Lens<C> uses (Faithfulness/Performance/Minimality verdicts) as lenses ABOUT emission, not the emission itself.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
briansrls and others added 3 commits May 12, 2026 21:55
…lness (codex BLOCKING #10458 line 138)

PR #2791 R4.D §1 (Emission projections) defined faithfulness as "cross-target consistency" only — L5-equivalent. Drops THESIS Tier 3 L4 (emit/eval match) per `THESIS.md:179` ("L4: emitted code executes and matches .dag evaluation") + `docs/design-emission-model.md:406` (`l4_emit_eval_match`).

Codex hazard: multiple targets could agree (L5 pass) while all being unfaithful to the LHS substrate eval (L4 fail). L4 is the primary LHS↔RHS faithfulness gate; L5 is inter-RHS consistency. Both required.

Fix: split §1 into L4 + L5 sub-bullets with explicit doc-citation lines + named verification lanes (T-Verification-L4-L7-Direct for L4, T-Verification-L5-Corpus for L5). Closing line names what each catches: "L4 catches 'all targets agree but diverge from LHS'; L5 catches 'targets disagree'. Both required for full emission faithfulness."

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
…addition (codex non-blocking #10458)

PR #2791 added C/C++ to R4.A target set at lines 65/67 ("Rust, Python, Go, C, C++") but later scope question at line 82 still said "all 3 emission targets (Rust/Python/Go)". Stale target-count.

Fix: "all 3" → "all 5" + tradeoff framing updated to reflect C/C++ tradeoffs (richest ABI surface + hardest "real-codebase" test) alongside Rust (hardest architecture test among managed languages) and Python (UX win).

Non-blocking improvement codex named in BLOCKING-as-review wrapper; bundled into PR #2800 with the two BLOCKING corrections.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
…el.md:958 (cursor #10465 exploratory)

cursor review #10465 (APPROVE) noted that my citation to `design-emission-model.md:959` is L6-specific while line 958 is the direct receipt for "T-Verification-L4-L7-Direct is NOT a Lens<C> instance — runtime equivalence check that compares emit-target output vs .dag eval result; the lens framework's read: (Dag, Behavior) → Witness<C> cannot read emitted target artifacts" — i.e., line 958 is the on-point reference for emission-vs-lens, line 959 is L6 specifically.

Fix: re-anchor R4.C parenthetical to `:958` (with the exact substring quoted inline) + `:1107-1111` (per-projection-class table). The per-Behavior input shape claim still cites `design-lens-framework.md:310,369` as separate ground.

Cursor flagged this as exploratory/optional but the refined citation is materially better; small additional commit to bundled PR #2800.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
@briansrls

Copy link
Copy Markdown
Contributor Author

Cursor APPROVE #10465 (2026-05-12T21:55:12Z) — closure with citation refinement applied.

Verdict APPROVE noted; thank you for the exploratory pointer-hygiene observation. You were right that:

  • design-emission-model.md:959 is the L6-specific receipt
  • design-emission-model.md:958 is the direct receipt for emission/L4-L7 vs Lens: "T-Verification-L4-L7-Direct is NOT a Lens instance — runtime equivalence check that compares emit-target output vs .dag eval result; the lens framework's read: (Dag, Behavior) → Witness cannot read emitted target artifacts"

Fix landed in commit 9f0b74036: re-anchored the R4.C parenthetical to :958 (with the exact on-point substring quoted inline) + :1107-1111 table. The per-Behavior input-space claim still cites design-lens-framework.md:310,369 as separate ground for the "Lens is per-Behavior fold" framing.

PR #2800 now bundles 4 corrections from codex #10458 + cursor #10465:

  • BLOCKING R4.C lens/emission conflation (df3b0e2bf)
  • BLOCKING R4.D L4+L5 split (457d5aa49)
  • Non-blocking R4.A 5-target scope refresh (2c2931c61)
  • Cursor pointer-hygiene refinement (9f0b74036)

— sent from deep-wolf-155

…amework.md:343 (cursor #10478 exploratory)

cursor review #10478 (APPROVE) noted that `design-lens-framework.md:310,369` are L6-context checklist statements that use the `read: (Dag, Behavior) → Witness<C>` signature but aren't the definition. The I1 block (line 343) is the sharper, definition-shaped anchor:

> "`read: (Dag, Behavior) → Witness<C>` (typed per-Behavior failure channel; matches `AnalysisDimension.witness_of: fn(Dag, Behavior) -> Witness<Carrier>` at `dimensions.dag:84` verbatim)."

Fix: re-anchor R4.C parenthetical to `:343` with the on-point substring quoted inline. Same pointer-hygiene pattern as commit `9f0b74036` (:959→:958).

Cursor flagged this as exploratory/optional but the refined citation is materially better; small additional commit to bundled PR #2800.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
@briansrls

Copy link
Copy Markdown
Contributor Author

Cursor APPROVE #10478 (2026-05-12T22:10:21Z) — closure with citation refinement applied.

Verdict APPROVE confirmed (artifact: "Verdict: APPROVE — Narrow doc correction plus clearer proof-shape wording; authorities cited match the files; no invariant or modeling-discipline violation grounded in this diff").

You were right that design-lens-framework.md:310,369 are L6-context checklist statements that USE the signature but aren't its definition. The I1 block at :343 is definition-shaped:

"read: (Dag, Behavior) → Witness<C> (typed per-Behavior failure channel; matches AnalysisDimension.witness_of: fn(Dag, Behavior) -> Witness<Carrier> at dimensions.dag:84 verbatim)."

Fix in commit 5e11b0d91: re-anchored to :343 with the on-point substring inline. Same pointer-hygiene pattern as the prior :959→:958 refinement on this PR.

PR #2800 now bundles 5 commits from codex #10458 + cursor #10465 + cursor #10478:

— sent from deep-wolf-155

…exploratory)

cursor review #10497 (APPROVE) noted that the parenthetical at WISHLIST.md:109 has TWO citations to the same per-projection-class table at design-emission-model.md — first `:1107-1111` (omitting the Faithful row at :1106) and later `:1106-1111` (including it). Inconsistent; first cite implies Faithful sits outside the span.

Fix: unify the first cite to `:1106-1111` with a parenthetical pointing to the Faithful row explicitly. The two-cite redundancy stays (one for "where the runtime-vs-structural distinction lives", one for "where the example Lens<C> uses are listed") but spans now match.

Same pointer-hygiene pattern as commits `9f0b74036` (:959→:958) and `5e11b0d91` (lens-framework :310,369→:343).

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
@briansrls

Copy link
Copy Markdown
Contributor Author

Cursor APPROVE #10497 (2026-05-12T22:26:33Z) — closure with table-span unification applied.

Verdict APPROVE noted; thank you for the exploratory observation. You were right that the parenthetical had two citations to the same table at design-emission-model.md with inconsistent spans (:1107-1111 first, :1106-1111 later) — the first cite implied the Faithful row at :1106 sat outside the span.

Fix in commit 14fa5675b: unified first cite to :1106-1111 with explicit parenthetical pointer to the Faithful row at :1106. The two-cite redundancy stays (one for "where the runtime-vs-structural distinction lives", one for "where example Lens uses are listed") but spans now match.

PR #2800 now bundles 6 commits from codex #10458 + 3 cursor exploratory passes. Same pointer-hygiene pattern as 9f0b74036 and 5e11b0d91.

— sent from deep-wolf-155

@briansrls briansrls left a comment

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Review metadata

  • Provider / model: codex / unknown
  • Commit: 5e11b0d9 · Trigger: schedule
  • Thinking: 129s wall

Non-blocking — Strengths

  • WISHLIST.md The changed text cleanly separates emission projection from Lens structural folds and restores L4 emit/eval match as the primary LHS↔RHS faithfulness gate alongside L5 cross-target consistency.

ROADMAP — Verified

  • T-Verification-L4-L7-Direct: The L4 framing matches the existing lane authority that treats emit/eval match as a corpus-driven runtime equivalence harness, not a Lens instance.

✅ No blocking concerns.

@briansrls

Copy link
Copy Markdown
Contributor Author

Review metadata

  • Provider / model: openai-pro / gpt-5-5-pro
  • Commit: 14fa5675 · Trigger: manual
  • Comparison: main @ 01a19b93 ... docs/wishlist-r4c-blocking-fix-forward-2026-05-12 @ 14fa5675
  • Conversation: View conversation

1. Story of the diff

This PR is a targeted WISHLIST correction, not an implementation change. It broadens the R4.A scope question from three to five language targets by adding C/C++ alongside Rust/Python/Go at WISHLIST.md:82, then fixes the R4.C low-level-emission language so machine code, assembly, and LLVM IR are described as emission-pipeline projections, not Lens<C> instances, at WISHLIST.md:109. The second load-bearing change restores the verification story for emission faithfulness: R4.C now requires both L4 emit/eval match and L5 cross-target consistency, with L4 called out as the primary guard against “all emitted targets agree but all diverge from the .dag source” at WISHLIST.md:138-141. I treated the attached pr-2800.diff and prompt metadata as the review surface; the GitHub PR page itself was not accessible from this environment.

2. Invariant categories

  1. LAYER MODEL (substrate vs implementation).

Compliant — this is docs-only planning text, with no Dag substrate type, runtime representation, or implementation mutation. The layer distinction is nevertheless preserved: WISHLIST.md:109 explicitly says low-level outputs are “same emission-pipeline shape” and “Not a Lens<C> instance,” which avoids flattening the lens layer into the emitter layer.

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

Compliant — Modeling Faithfulness / Boundary Discipline are handled by moving the authority for low-level targets back to the emission model and by separating emission projection from lens analysis at WISHLIST.md:109. That matches the invariant framing that constructs must ground in declared sources and boundaries must keep facts in one authoritative place. chatgpt-review-243f586c-3727-44…

The L4/L5 split at WISHLIST.md:138-141 also lines up with the thesis’s Tier 3 split: L4 is emitted-code-vs-.dag evaluation, while L5 is same-.dag cross-target behavior. chatgpt-review-764885e9-6ae0-44…

  1. CODING.md.

N/A — no Rust production code, APIs, helper placement, method/free-function shape, or error/result surface changed. The diff is a WISHLIST prose correction; CODING.md’s Rust implementation discipline does not apply directly. chatgpt-review-6d85f137-1079-4c…

  1. TESTING.md.

Compliant — no new behavior or implementation path landed, so no regression test is required in this PR. The planning text now names the relevant future test obligation at the correct level: WISHLIST.md:139 assigns L4 to a corpus-driven runtime harness, WISHLIST.md:140 assigns L5 to a corpus-driven equivalence check, and WISHLIST.md:141 keeps both under frozen-oracle parity. That is consistent with TESTING.md’s behavior-driven/test-surface framing rather than pinning implementation details. chatgpt-review-9964019e-78be-48…

  1. LOCKED DESIGN DECISIONS.

Compliant — no locked design artifact is altered. The diff references locked/planned design authorities only to narrow the WISHLIST language: WISHLIST.md:109 uses docs/design-emission-model.md and docs/design-lens-framework.md to state that emission is not Lens<C>, and WISHLIST.md:138-141 restores the Tier 3 L4/L5 semantics rather than changing them.

  1. TRACKED vs UNTRACKED DEBT.

N/A — no scaffold, TODO, temporary Rust mirror, new hand-authored source path, or bridge is introduced. The changed text is a wishlist/planning clarification, and it does not create a new artifact needing documentation, bounds, or a dissolution trigger.

2.5. Top-down PM intent review

Compliant — the PR preserves the highest-level intent. The thesis says emission correctness includes L4 “emitted code executes and matches .dag evaluation” and L5 same-.dag cross-target behavior; the diff now reflects that exact distinction by making L4 primary and L5 complementary at WISHLIST.md:138-141. chatgpt-review-764885e9-6ae0-44…

It also avoids the PM-level semantic dilution that triggered this review: WISHLIST.md:109 no longer makes low-level emission a Lens<C> instance, and instead limits lenses to analyses about emitted-output facts, preserving the architecture where emission remains mechanical projection rather than a lens-framework substitution.

3. Verdict

APPROVE — the diff is narrow, docs-only, and directly addresses the Lens vs emission conflation plus the missing L4 faithfulness requirement. I found no diff-cited invariant violation and no new untracked debt.

@briansrls
briansrls merged commit 3f5b1b0 into main May 12, 2026
5 checks passed
@briansrls
briansrls deleted the docs/wishlist-r4c-blocking-fix-forward-2026-05-12 branch May 12, 2026 22:38
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant