Repository navigation
B - #529
B#529
Conversation
|
ChatGPT review in progress... (view conversation) Check back in ~30 minutes for the full review. |
briansrls
left a comment
There was a problem hiding this comment.
codex · gpt-5.4 · b42edc15
BLOCKING (1)
Root Cause
docs/design-composed-effect-reshape.mdThe reshape stops at replacing the Bool + String? pair and reuses unconstrained OperationEffect as the breaker witness; introduce a breaker-only carrier or otherwise narrow the BrokenBy payload before treating the boundary as cleared.
Non-blocking — Strengths
docs/design-composed-effect-reshape.mdThe brief is otherwise well-scoped: it names the consumer boundary, keeps v2 explicitly out of scope, and records the rationale instead of letting the reshape land as undocumented drift.
ROADMAP — Incomplete
- Lane 2 Stage 2a / Track 17a boundary: The old correlated fields are gone, but the new verdict still accepts non-breaking OperationEffect payloads, so this boundary is improved rather than fully cleared.
| // into `ComposedEffect.operations`. | ||
| type CompositionVerdict | ||
| = IdempotentComposition | ||
| | BrokenBy { first_breaker: OperationEffect } |
This comment was marked as resolved.
This comment was marked as resolved.
Sorry, something went wrong.
This comment has been minimized.
This comment has been minimized.
This comment has been minimized.
This comment has been minimized.
|
ChatGPT review in progress... (view conversation) Check back in ~30 minutes for the full review. |
ChatGPT ReviewPrinciple audit. Fail-closed. Looks good. Illegal states unrepresentable. R2 definitely improves this: Facts flow forward. Satisfied, and improved. Narrowing the breaker carrier to Coproduct dissolution. Mostly satisfied. I think Single authority. Not satisfied. API-level enforcement. Not satisfied. A contributor can still construct Loop health. This round does make real forward progress: Codex’s blocker about “breaker payload is still too broad” is addressed. But the root wrapper-level coherence problem remains, and the changed docs/roadmap now bank it as “cleared,” which is the wrong direction for the review loop. LOOP HEALTH: stagnant — one illegal-state edge was dissolved, but the same evidence-chain/coherence blocker is still live and is now being normalized as done. Design question. Is That is the structural decision this PR still leaves unresolved. R2 makes the copy narrower, which is good, but if the project wants single-authority substrate, the breaker wants the same handle shape the roadmap is already moving toward for other “this field must refer to an element of that carrier” cases. If it is only a copy, then the boundary is improved but not actually closed. Path to convergence. Before merge, I would do one of two things, with a strong preference for the first because there are still no real consumers. Either make the breaker a witness anchored in What can wait is smaller. The smoke test can be strengthened later; right now it only name-checks the added carriers ( Verdict. REQUEST_CHANGES R2 is real progress, and it fixes the blocker Codex called out. But the deeper single-authority / API-enforcement issue is still present, and this PR now documents that boundary as fully cleared when it is not. |
|
Meta-review in progress... (view conversation) Loop-health check: is this review cycle making forward progress, or shifting debt? Posts in ~5-15 minutes. |
|
ChatGPT review in progress... (view conversation) Check back in ~30 minutes for the full review. |
Promotes Stage 2b's workflow control-flow shape from a lens-level re-derivation to a first-class substrate carrier. Four-variant coproduct (LinearEffect | BranchEffect | LoopEffect | ParallelEffect) with BranchArm helper record; Q4 dissolution receipt stamped inline; Q1–Q6 substrate-principle audit stamped inline. LinearEffect is the only Stage 2b consumer — other variants emit C-8 fail-closed diagnostics naming the downstream stage. Coexists orthogonally with PR #529's CompositionVerdict (input structure vs output verdict; no enclosing record pairs them). Part 1 is design only; Part 2 implementation is gated on PR #529 landing (pre-start gate named in the doc). Also adds an additive subsection to lane2-compile-time-proofs.md §Stage 2b pointing at DB-18 — placed between Escalation and Pre-start gate, both of which PR #529 leaves untouched — so merges without conflict. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
briansrls
left a comment
There was a problem hiding this comment.
codex · gpt-5.4 · 74d2339b
✅ Review (blocking: 0, non-blocking: 2+/0-)
Non-blocking — Strengths
src/v3/std/effects.dagR3 removes both previously flagged incoherence sites: the breaker payload is breaker-only by type shape, and compose_effects no longer returns a record that can disagree with the evidence list.docs/design-composed-effect-reshape.mdThe brief documents the R1→R3 review arc clearly enough that Stage 2b inherits the rationale for the cleared boundary instead of rediscovering it piecemeal.
ROADMAP — Verified
- Lane 2 Stage 2a / Track 17a boundary: The roadmap and lane doc now agree on the landed endpoint: ComposedEffect is gone, CompositionVerdict is the Stage 2a output, and the remaining breaker-handle question is an explicit Stage 2b/Track 17a follow-up rather than hidden debt.
✅ No blocking concerns: the substrate change closes the illegal-state holes from R1/R2, and the remaining copy-vs-witness tradeoff is documented, bounded, and deferred to the first consumer instead of being baked into the Stage 2a carrier.
|
✅ Review (blocking: 0, non-blocking: 2+/0-) Non-blocking — Strengths
ROADMAP — Verified
✅ No blocking concerns: the substrate change closes the illegal-state holes from R1/R2, and the remaining copy-vs-witness tradeoff is documented, bounded, and deferred to the first consumer instead of being baked into the Stage 2a carrier. |
ChatGPT ReviewPrinciple audit. Fail-closed. Looks good. The only new Illegal states unrepresentable. This is the big win, and I think it now lands. The old contradictory workflow-summary states are gone, the breaker payload can no longer carry an idempotent shape, and the outer Facts flow forward. Satisfied. The diff is explicit about which facts are intentionally not carried forward ( Coproduct dissolution. I think this round is materially better than the old convenience record. The wrapper that was acting as compressed duplicated state is gone, and the remaining sums are carrying real judgment-space distinctions rather than “bool + optional blame” bookkeeping ( Single-authority metadata. Satisfied at the boundary this PR touches. The important change is that the caller owns the evidence chain and API-level enforcement. Also satisfied here. The old bad states are no longer prevented only by “please go through Design question. When Stage 2b needs to point from Right now I think the PR makes the correct trade: it refuses to pair Path to convergence. Before merge, I do not see a structural blocker left in this PR. The earlier blocker was the wrapper-level coherence hole, and this diff actually removes it in code, doc, and roadmap ( Can ship as tracked follow-up debt: when Stage 2b lands, replace the draft LOOP HEALTH: converging — this round removes the exact wrapper-level debt prior reviews kept finding, adds no new scaffold, and updates the design docs/roadmap to match the substrate instead of banking an open hole as “cleared.” Verdict. APPROVE_WITH_COMMENTS The R3 reshape looks like the right final move for this boundary. The prior inner-payload and outer-wrapper coherence problems both look resolved now, and the remaining comment is about how Stage 2b should preserve occurrence identity later without reintroducing the old pair. |
Meta-Review (Loop Health)According to a document from 2026-04-18, this loop has crossed the point where another review round on the same substrate shape is less valuable than merging and forcing the next real consumer to prove it. The right call is: ⚖️ SHIP_WITH_DEBT Loop summaryThis PR shows 3 substantive review rounds in the attached history: 1 codex-cli review and 2 chatgpt-browser reviews, plus 2 browser “review in progress” status pings. The visible review window runs from 2026-04-18 14:36:16Z to 2026-04-18 15:25:41Z, so the documented loop took about 49 minutes end to end, with the substantive review span running about 40 minutes from the codex review at 14:45:57Z to the second browser review at 15:25:41Z. The current diff also documents three visible revision states (R1/R2/R3), but only the review history is explicitly timestamped in the attachments. Forward progress evidenceThere was real forward progress inside the loop. Codex’s original blocker was that The more important signal is that the loop did not stop at that cheaper partial fix. The recurring browser blocker after R1 and R2 was the wrapper-level duplicate authority: So on principle 2 and principle 5, the latest direction is good: the loop did dissolve one scaffolded compromise instead of adding another one, and the most recent requested fix was structural rather than “good enough for now.” That matters. Debt accumulation evidenceThe loop also accumulated debt before it paid it down. R1 replaced the obvious bad pair ( The bigger debt signal is that no consumer was enabled. The roadmap’s modeling-consumption gap still lists And the recurring pattern in this loop is exactly the one your current invariant system already knows how to name: secondary authority, convention-level enforcement, and bridge-like duplication at a substrate boundary. The project’s own current guidance says those cases should be fixed structurally, not normalized as “single constructor” discipline. Cheating signalLow cheating signal overall. The implementer is not hiding compromises. The review history shows the exact blocker sequence in public, and the latest requested fixes are structural: narrow the breaker carrier, then eliminate the detached wrapper authority. That is not “smaller blast radius triage”; it is movement toward a single-authority shape. The browser review itself says the direction is good and that the remaining issue is the detached record wrapper, not the judgment-space coproduct. There was one cheating-adjacent moment in the middle of the loop: R2 started documenting the boundary as “cleared” while the browser review still saw a convention-enforced duplicate authority. That is the one place the loop started rationalizing a partial fix as done. But because the next revision moved further structurally instead of doubling down on prose, I would call that a temporary bluff, not a calcified one. Path to convergenceBecause I’m choosing SHIP_WITH_DEBT, the question is not “what justifies another round on this same PR?” It is “what debt is acceptable to carry, and where should it be tracked?” The acceptable debt to carry is: The first acceptable debt is consumer debt: The second acceptable debt is test-strength debt. The review history notes that the smoke test acceptance text expects coverage of The third acceptable debt is doctrinal debt: the loop has not graduated this recurring class into a new invariant because it did not need to — the project already has the right general invariant vocabulary for it. What it needs now is not more naming; it needs the consumer-side ratchet the thesis already prefers: a structural consumer and, ideally, a lens or test that makes reintroduction expensive. The existing layer-opacity / semantic-authority path is already the right home for that. So the concrete follow-up artifact is: keep the remaining debt on Bottom lineThis loop was shifting debt in the middle, but it is not doing that anymore. It found the real blocker class, pushed past the cheap partial fixes, and appears to have converged on the right substrate shape. The remaining problem is that this shape still has no consumer, and your own roadmap says wiring the first consumer is “strictly cheaper than new design.” At that point, another review round on the same PR is negative marginal value. Meta-verdict: ⚖️ SHIP_WITH_DEBT. Merge the structural reshape, but do not pretend the modeling is proven until Track 17a makes |
Resolves conflict in docs/lane2-compile-time-proofs.md after PR #529 (ComposedEffect reshape) landed on main. Kept the DB-18 insertion in place, superseded the pre-#529 Pre-start gate text with #529's "cleared" version, and kept #529's new Stage 2b / Track 17a design-axis paragraph. Updated the DB-18 "Design:" line to reflect that the Part 2 gate is now cleared (was forward-looking at write time). Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Post-PR #529 the file grew from ~569 to 673 lines (partition types, CompositionVerdict, new fns); WorkflowEffectConcern shifted from :565-569 to :669-673. Cite both the new and old ranges so the historical anchor is preserved. Addresses the single callout in the claude-review on #531. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
…d authority site Responds to two structural reviews (ChatGPT: 3 BLOCKING; codex: 2 BLOCKING) on PR #531 R1 draft. BLOCKING (ChatGPT 1+2 / codex 1): `branch_arm_of(port, body)->Option` and raw `condition: PortId` kept the "port is Bool-typed" invariant at constructor-convention level — a non-Bool branch condition is a user-reachable modeling error, not a benign absence. R2 introduces `BoolPortRef` as a Track 9-style typed opaque handle (third Track 9 primitive after ParamRef / TransformRef from DB-9 R2.1). Sole constructor `bool_port_of(dag, port) -> BoolPortRef?` validates the port's declared type is Bool; no unsafe escape hatch. BranchArm's condition field is `BoolPortRef`, not `PortId` — raw-literal construction around a non-Bool port is a type error. Fail-closed discipline relocated to the caller boundary: lowering emits `Diagnostic::BranchConditionNotBool` on None per C-8, explicitly required as a Part 2 review gate. BLOCKING (ChatGPT 3): `LinearEffect.ops: NonEmptyList<OperationEffect>` excluded the empty word, but `compose_effects([])` returns `IdempotentComposition` (the monoidal identity). The asymmetry between carrier and algebra rejected real workflow shapes (no-op paths, empty branch arms). R2 relaxes to `List<OperationEffect>`; the empty case is the honest monoidal identity representation. BLOCKING (codex 2): Open Question §5 left authority site for WorkflowEffect values undefined ("any declaration slot") — a Q5 single-authority violation. R2 locks the authority site to user-declared `data` declarations typed `WorkflowEffect`. No new declaration kind (per feedback_std_over_patterns — reuse `data`, don't invent WorkflowDeclaration); no sidecar table (a WorkflowEffect is single-declaration-local, unlike DB-9 R2.1's Cluster sidecar). Closes R1 Open Q §5. Non-blocking (codex): lane2-compile-time-proofs.md said PR #529 gate was cleared while DB-18 treated it as pre-start dependency. R2 syncs — DB-18 Pre-start gate now reads "CLEARED" with the commit SHA preserved for record; the original gate rationale is preserved as a rejected-alternative-style trail. Non-blocking (ChatGPT): Acceptance item 1 tightened — locked VARIANTS and MANDATORY fields now; additive extension fields (LoopEffect.bound for Stage 2d, ParallelEffect.commutativity for Stage 2e) explicitly flagged as downstream-binding refinements. Fixes the doc-coherence gap between Open Q §3 ("Stage 2d will almost certainly need bound") and the previous "exact payload shapes" language. Also adds R-alt-E (raw PortId rejection) and R-alt-G (deferred-host rejection) to the Rejected-alternatives list, preserving the design rationale for reviewers who hit this design again. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
* docs: DB-18 Part 1 — WorkflowEffect substrate carrier (Stage 2b) Promotes Stage 2b's workflow control-flow shape from a lens-level re-derivation to a first-class substrate carrier. Four-variant coproduct (LinearEffect | BranchEffect | LoopEffect | ParallelEffect) with BranchArm helper record; Q4 dissolution receipt stamped inline; Q1–Q6 substrate-principle audit stamped inline. LinearEffect is the only Stage 2b consumer — other variants emit C-8 fail-closed diagnostics naming the downstream stage. Coexists orthogonally with PR #529's CompositionVerdict (input structure vs output verdict; no enclosing record pairs them). Part 1 is design only; Part 2 implementation is gated on PR #529 landing (pre-start gate named in the doc). Also adds an additive subsection to lane2-compile-time-proofs.md §Stage 2b pointing at DB-18 — placed between Escalation and Pre-start gate, both of which PR #529 leaves untouched — so merges without conflict. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * Merge main into session/bright-bat-435 Resolves conflict in docs/lane2-compile-time-proofs.md after PR #529 (ComposedEffect reshape) landed on main. Kept the DB-18 insertion in place, superseded the pre-#529 Pre-start gate text with #529's "cleared" version, and kept #529's new Stage 2b / Track 17a design-axis paragraph. Updated the DB-18 "Design:" line to reflect that the Part 2 gate is now cleared (was forward-looking at write time). Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * docs: DB-18 — update WorkflowEffectConcern line-range citation Post-PR #529 the file grew from ~569 to 673 lines (partition types, CompositionVerdict, new fns); WorkflowEffectConcern shifted from :565-569 to :669-673. Cite both the new and old ranges so the historical anchor is preserved. Addresses the single callout in the claude-review on #531. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * WIP: B' * WIP: B' * WIP: B' * WIP: B' * WIP: B' * WIP: B' * docs: DB-18 R2 — typed BoolPortRef witness, empty LinearEffect, locked authority site Responds to two structural reviews (ChatGPT: 3 BLOCKING; codex: 2 BLOCKING) on PR #531 R1 draft. BLOCKING (ChatGPT 1+2 / codex 1): `branch_arm_of(port, body)->Option` and raw `condition: PortId` kept the "port is Bool-typed" invariant at constructor-convention level — a non-Bool branch condition is a user-reachable modeling error, not a benign absence. R2 introduces `BoolPortRef` as a Track 9-style typed opaque handle (third Track 9 primitive after ParamRef / TransformRef from DB-9 R2.1). Sole constructor `bool_port_of(dag, port) -> BoolPortRef?` validates the port's declared type is Bool; no unsafe escape hatch. BranchArm's condition field is `BoolPortRef`, not `PortId` — raw-literal construction around a non-Bool port is a type error. Fail-closed discipline relocated to the caller boundary: lowering emits `Diagnostic::BranchConditionNotBool` on None per C-8, explicitly required as a Part 2 review gate. BLOCKING (ChatGPT 3): `LinearEffect.ops: NonEmptyList<OperationEffect>` excluded the empty word, but `compose_effects([])` returns `IdempotentComposition` (the monoidal identity). The asymmetry between carrier and algebra rejected real workflow shapes (no-op paths, empty branch arms). R2 relaxes to `List<OperationEffect>`; the empty case is the honest monoidal identity representation. BLOCKING (codex 2): Open Question §5 left authority site for WorkflowEffect values undefined ("any declaration slot") — a Q5 single-authority violation. R2 locks the authority site to user-declared `data` declarations typed `WorkflowEffect`. No new declaration kind (per feedback_std_over_patterns — reuse `data`, don't invent WorkflowDeclaration); no sidecar table (a WorkflowEffect is single-declaration-local, unlike DB-9 R2.1's Cluster sidecar). Closes R1 Open Q §5. Non-blocking (codex): lane2-compile-time-proofs.md said PR #529 gate was cleared while DB-18 treated it as pre-start dependency. R2 syncs — DB-18 Pre-start gate now reads "CLEARED" with the commit SHA preserved for record; the original gate rationale is preserved as a rejected-alternative-style trail. Non-blocking (ChatGPT): Acceptance item 1 tightened — locked VARIANTS and MANDATORY fields now; additive extension fields (LoopEffect.bound for Stage 2d, ParallelEffect.commutativity for Stage 2e) explicitly flagged as downstream-binding refinements. Fixes the doc-coherence gap between Open Q §3 ("Stage 2d will almost certainly need bound") and the previous "exact payload shapes" language. Also adds R-alt-E (raw PortId rejection) and R-alt-G (deferred-host rejection) to the Rejected-alternatives list, preserving the design rationale for reviewers who hit this design again. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * docs: DB-18 R2 propagation — two stale pre-R2 references in constraints + Pattern 3 ChatGPT review at bb08594 flagged "two different carriers described" because R2 was mid-edit at that SHA. Most of the propagation landed in 1ac587a, but two genuine gaps remained: 1. Constraint 3 (Bounded kernel invariant) still cited `LinearEffect.ops: NonEmptyList<OperationEffect>` — updated to `List<OperationEffect>` with an explicit "empty list is a well-defined leaf" clause. 2. Pattern 3 (Algebraic-form) described the carrier as "the free monoid on OperationEffect less the empty word" — inconsistent with R2's empty-word inclusion. Updated to read "the free monoid on OperationEffect — including the empty word, which is the monoidal identity the R2 relaxation explicitly preserves," matching the Q1 audit and the worked examples. The reviewer's other concerns ("Q4 table still cites PortId", "audit Q1/Q2/Q6 still reasons about NonEmptyList", "worked examples", "acceptance", "lane2 subsection", "authority site still open") were already resolved by R2 at 1ac587a — their review's line citations are against the pre-R2 WIP snapshot, not the current tip. All remaining mentions of `PortId` in the doc are now in appropriate historical/constructor-signature context (R1 revision history, R-alt-E rejection record, bool_port_of's input-parameter type, port_of's return type, Worked Example C's authoring comment). All remaining mentions of `NonEmptyList` are in Track 9 primitive references (the family still exists; DB-18 just doesn't consume it post-R2) or historical R1 references. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * WIP: B' * docs: DB-18 R2.2 — lock source-to-handle contract for BranchArm.condition PR #531 ChatGPT review round 3 (at 1ac587a) accepted the R2 carrier direction and the R2.1 propagation fix, and flagged ONE remaining BLOCKING gap: the R2 doc locked *where* WorkflowEffect values live (user-declared `data` typed WorkflowEffect) but not *how* a user writes a condition expression that lowering resolves to a BoolPortRef. Without that lock, Part 2 could invent three distinct single-authority escape hatches: (a) name-keyed port recovery (violating feedback_no_metadata_markers), (b) raw NodeId/PortId literals (violating structural opacity), or (c) lowering-time synthesis of a bool witness without a source anchor (violating feedback_declare_facts_dont_derive). Each would reopen the Q5 single-authority question at the source boundary. R2.2 adds §"Source-to-handle contract" under the existing Authority Site section, locking the single legal path: source: ordinary Bool-typed expression (no DB-18-specific syntax) lowering: expression → sub-DAG → output port → bool_port_of fail-closed: Diagnostic::BranchConditionNotBool on None, with span pointing at the source expression (not the wrapping BranchArm) rejected: named-port lookup, raw-id literals, anchor-less synthesis Per feedback_std_over_patterns, reuses the existing Bool-expression surface (same form used by if/where/modifier predicates) rather than inventing a DB-18 port-reference syntax. Part 1 acceptance item 7 added to lock the contract. Part 2 acceptance item 4 tightened (source-span-precise diagnostic) and new item 4b added (single source-to-handle path with three escape hatches explicitly rejected as Part 2 review gates). This closes the ChatGPT review round 3 BLOCKING; the review's other observations (R2 direction good, R2.1 propagation good, LOOP HEALTH converging) are carried forward unchanged. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * WIP: B' * WIP: B' * WIP: B' * WIP: B' * docs: DB-18 — fix Workflow B type error in worked example codex review at d7f226a (APPROVE, 0 BLOCKING) flagged one non-blocking fix-in-PR-if-easy: Workflow B shows `BrokenBy.first_breaker.shape: IsBreaking(AppendEffect)` but BreakingOperation.shape is typed BreakingShape (not EffectShape), so the outer IsBreaking wrapper is redundant and the example wouldn't typecheck as written. Updated to show AppendEffect directly and added a parenthetical explaining why no wrapper is needed. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * WIP: B' * WIP: B' * WIP: B' * WIP: B' * WIP: B' * docs: DB-18 — remediate to live state (β's PR #534 shipped; Part 3 deferred) Per director: doc should describe live state, not aspirational state. β's PR #534 (eager-fox-851) shipped DB-18 Part 2 as Rust mirrors on the computation substrate — WorkflowEffect / BranchArm / BranchPredicateRef in dag.rs, Dag::branch_arm_of constructor, ValueNode.lane2_workflow authority field, workflow_idempotency:: analyze_workflow consumer. The data-declaration authoring surface (data my_flow: WorkflowEffect = ...) is NOT shipped; it's Part 3 follow-up. Changes: - Authority site: rewrote §"Authority site for WorkflowEffect" from "user-declared data declarations typed WorkflowEffect" (aspirational) to "ValueNode.lane2_workflow on the computation-substrate Value node at the workflow root" (shipped). Explicitly names Part 3 as reflection + data-declaration surface work. - Naming: renamed BoolPortRef → BranchPredicateRef throughout to match β's shipped Rust type. bool_port_of → Dag::branch_arm_of (which takes root/port/body and builds the full BranchArm rather than a bare predicate ref). - Source-to-handle contract: reframed as Part 3 forward-looking contract. The three escape hatches (named-port lookup, raw-id literal, synthesis) remain explicitly rejected. - Consumer contract: rewrote the analyzer pseudocode as Rust to match β's shipped workflow_idempotency::analyze_workflow signature (takes `(&Dag, NodeId)`, returns WorkflowIdempotencyReport with Linear{verdict} / Unsupported{detail} variants). - Acceptance: split into Part 2 (shipped in #534) and Part 3 (follow-up). Part 3 items explicitly enumerated. - STOP-AND-ESCALATE: reframed as Part 3 dispatch rules; added a rule for the ValueBody/FieldValue encoding question (substrate extension requires escalation, not in-flight patch). - Worked example C: rewrote in Rust using Dag::branch_arm_of + try_register_lane2_workflow_effect to match shipped API. - Rejected alternatives: updated the hosting discussion — the adopted host is ValueNode.lane2_workflow; data-declaration surface reuse (not a new declaration kind) is still the Part 3 authoring surface. - Cross-references: added PR #534 reference (β's shipped impl). - lane2-compile-time-proofs.md §Stage 2b subsection: updated type block to show shipped Rust shape; rewrote the analyzer signature + authority-site prose to match live state; Part 3 follow-up named explicitly. Also addresses the codex BLOCKING at d7f226a and dea9fb4 (ValueBody substrate encoding for BoolPortRef — now obviated because the authority site is ValueNode.lane2_workflow, not ValueBody; Part 3 explicitly names the data-declaration-surface-vs-ValueBody question as an escalation trigger rather than an in-flight patch). Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * WIP: B' * WIP: B' * WIP: B' * WIP: B' * docs: DB-18 — verify-against-β fixes (5 points) Inline review at 2026-04-18T21:27:28Z flagged specific verifiable discrepancies between my remediation and β's actual PR #534 impl. Verified each claim against β's current head (a4dfa2e) and fixed all five: 1. **PR #534 is OPEN, not merged.** Changed "shipped in PR #534" to "implemented in PR #534 (OPEN)" throughout. The doc now tracks #534's head SHA; "OPEN" marker becomes the merge SHA when #534 lands. 2. **WorkflowEffect is 🟡 SCAFFOLD, not 🟢 terminal.** β's impl explicitly marks it as scaffold ("Four-variant workflow sum aligned with effects.dag; graduates to 🟢 when all four variants have consumers"). The doc now reflects this with the graduation trigger spelled out (all four variants have consumers + reflected into substrate.dag). 3. **LinearEffect.ops is NonEmptyList<OperationEffect>, not List<OperationEffect>.** β did NOT adopt R2's monoidal-identity relaxation; shipped NonEmptyList. The doc now reflects live: - Substrate-changes block shows NonEmptyList<OperationEffect> - Q1 audit explains why β chose the tighter carrier (no representation duality between "zero-ops LinearEffect" and "no workflow here") - Pattern 3 algebraic-form explains the free-semigroup vs free-monoid distinction (workflow input carrier is the semigroup; monoidal identity lives at the algebra boundary) - Q6 no-representation-duality argument reworked: no-workflow is lane2_workflow: None, NOT a zero-ops LinearEffect - Worked Examples A and C use NonEmptyList constructor form - Open Q §4 updated to NonEmptyList<WorkflowEffect> vs NonEmptyList<OperationEffect> - Part 2 test-coverage list drops the "empty-LinearEffect monoidal-identity case" (not representable) 4. **lane2_workflow lives on BOTH Value AND Bind behaviors**, not just Value. β's try_register + lane2_workflow_effect_at both pattern-match the two variants. Authority-site section rewritten to show fields on both behaviors and the accessor impls. Added a paragraph explaining why both (Value for top-level data-decl roots; Bind for let-bound sub-workflows). 5. **Dag::branch_arm_of takes (&self, port, body), no root arg.** Port-type resolution uses the Dag's own graph state. Substrate- changes block, source-to-handle contract (Part 3), Worked Example C, Acceptance items, and STOP-AND-ESCALATE rules all updated to the 2-arg signature. All five are factual fixes against live code, not stylistic changes. The Q4 dissolution receipt and overall design contract are preserved. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> --------- Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
…abitance, not signature shape Cursor BLOCKING finding on PR #1480 at design-effect-enumeration-resource- threading.md:151: the design's "structural recognition" claim was actually convention-level. \`R in / R out\` and \`R in / R' out\` (same type, different value) have the SAME typed signature — \`.dag\` doesn't encode value- preservation as a substrate fact. ReadShaped vs WriteShaped via signature shape alone was P1 modeling-faithfulness violation. Resolution: split the unified rule into two structural carriers per §2.4: (a) Effect SET — derived from signature: resource types in input ∩ output. Structural; the signature carries it. (b) Effect KIND — declared via algebra inhabitance on the callable: \`inhabits IdempotentRead<R>\` (read), \`inhabits Mutating<R>\` (write), \`inhabits Append<R>\` (append). Structural; the inhabitance carrier captures it. The lens consults BOTH — signature for set, inhabitance for kind. Absence of any kind inhabitance with the resource in the effect set is a fail- closed Diagnostic (EffectKindUndeclared), not a silent default. Updates: - §2.1 line 151: replace "same-value vs modified" framing with explicit effect-set-vs-effect-kind distinction; cross-link to §2.4 + §8.1. - §2.3: same fix for Network read example. - §2.4: split the unified rule into (a) effect SET (signature) + (b) effect KIND (algebra inhabitance) with pseudocode for the lens-side classification. - §4.3: update EffectShape derivation source from "signature shape" to "algebra inhabitance lookup". - §8.1: full reframe — from "same-value resolved" to "algebra inhabitance is the structural authority", with explicit rationale (per-callable authority, not per-call; rejected phantom-marker alternative per feedback_no_annotations). - §3 lens fold pseudocode: dispatch on §2.4(a) for set + §2.4(b) for kind. Preserves the existing EffectShape = IsIdempotent | IsBreaking partition (per design-composed-effect-reshape.md PR #529 R3) — only the source of the shape changes (declared inhabitance, not derived from signature). P1 modeling-faithfulness restored. Cursor finding fully resolved. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
… program (#1480) * docs(roadmap): fold 2026-05-01 paired exploratory + reflective analyses Director relayed two analyses against current main: - Exploratory (gpt-5-5-pro main@8cd5359): 9 findings against dsl/std/*.dag, src/v2/tests/src/*.rs, dsl/extdeps/, THESIS, INVARIANTS, MODELING, ROADMAP — 2 novel correctness bugs (SymbolicCost semiring violation, emitter expect() panic paths), 3 sharpened tracked items (SubValueRelation lattice-law contradiction, ?? / % syntax-parser drift, CollectionOps/StringOps/ MapOps duplicates), 4 already-tracked items - Reflective (gpt-5-5-pro main@6ea9812 → now): 5 cross-PR patterns + 6 highest-priority course corrections + verdict "advancing, scaffold-velocity dominates" PM ingestion folds into single ROADMAP debt section per Director's prior 2026-04-30 analyses ingestion pattern (PR #1319). Sections: - A: Exploratory novel correctness bugs (SymbolicCost product-zero bug, SubValueRelation BoundedLattice claim violation, emitter expect panic paths) - B: Exploratory sharpened tracked items (?? / % drift, CollectionOps/StringOps/MapOps duplicates) - C: Exploratory already-tracked confirmations (no new ROADMAP rows) - D: Reflective 5 cross-PR patterns (author-now/fire-later, test_ runner.rs second predicate language, typed-carrier-Rust-mirror accumulation, numeric philosophy mid-window shift validating T-Numeric-Construction reframe, bridge retirement tracked-not- retired) - E: Reflective 6 highest-priority course corrections with owner attribution + lane connection table - F: CI cost signal (e765c86 60min timeout) + velocity-tripwire calibration (64 docs / 16 feat / 9 fix ratio) - G: PM strategic synthesis: 3 cross-cutting meta-themes (algebraic-law-witness coverage gap; "make scaffolds executable" cluster; "tighten existing structural enforcement" cluster) Per-finding/correction owner attribution names R3 Substrate Mgr, R3 Verification Mgr, R3 Grounding Mgr, R3 PB Mgr per ownership boundaries. Lane connections cite T-V-L4-L7-Direct, T-Free- Consequences-Demonstration, T-Ground-Services parser-grammar slice, T-Numeric-Construction Slice 2 sequencing, etc. Highest-value novel: SymbolicCost product-zero bug (cost-lens reads incorrect facts; iterate(ConstantCost(0), ...) returns body cost instead of zero) + emitter expect() panics. Highest-value sharpened-tracked: SubValueRelation BoundedLattice false-claim. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * WIP: Gunbc PM * docs(r3): R3 scope expansion 12 → 16 lanes + standing R3 Debt-Paydown program Per Director ratification 2026-05-02 at gunbc#828 comment 4362742638: User directive: per the strict reading of "nothing deferred past R3", all "accidentally deferred" gaps absorb into R3. Plus three additional asks: behavioral expectations docs per feature; compile-error complexity ratchet generalized as lens-application-surface (per user reframe); in-cycle debt-paydown discipline. NEW R3 LANES (4 added; lane count 12 → 16): 13. T-E-P-Producer-Broadening (Substrate; M-L; foundational) - broaden per-call DescentEvidence/CallPattern/SubValueRelation from first slice to full ExprCall.descent_evidence parity - prerequisite for T-Lens-Behavioral-Parity 14. T-Lens-Behavioral-Parity (Substrate + Verification cross-program; L-XL) - 4 sub-slices: complexity / cost / parallelism / effect_enumeration - bring lens-capability-register from PROXY/STUB/PARTIAL → COMPLETE - includes symbolic CostExpr full algebra; work/span split; asymptotic classification; cementing test against v2 oracle; Stage 2e parallelism walk port; resource-threading migration 15. T-Tests-As-Data-Completeness (Verification; L) - tests-as-data full coverage (thesis facet 3) - property-based testing surface (ForAll/Exists quantifiers + ProgramGenerator carrier) - cementing test discipline for .dag lenses 16. T-Lens-Application-Surface (Substrate + Verification; L-XL) - per user reframe: lens application as first-class authoring surface - apply_lens(lens, section, config) where config.violation_policy = CompileError | Warning | Silent - subsumes prior T-Complexity-Contract-Compile-Error + T-User-Authored-Cost-Basis-Discipline as configurations - 4 worked examples: complexity-contract-compile-error + CRDT cost basis + memory-peak cost basis + opt-in cross-iteration parallelism - default policy for complexity contract: opt-out NEW STANDING PROGRAM: R3 Debt-Paydown Manager (9th standing R3 Mgr) - hybrid mechanism: per-PR debt-receipt rule + standing capacity - closure gate: r3_debt_paydown_zero_remaining - per feedback_standing_managers_need_owned_deliverables FOLD-INS (3; no new lanes): - T-V-L4-L7-Direct: per-(algebra, inhabitant, law) exhaustive witness coverage (catches SymbolicCost product-zero bug class structurally) - T-Ground-Diagnostic: closed-axis enforcement (no String dispatch on closed sets); replaces MissingEmissionPath { connective: String, ... } - T-LensProducer-Retirement: ownership d/e/f confirmed delivered (not separately deferred) T-Behavioral-Expectations-Documentation (parallel-dispatchable; 7 load- bearing features per Director ratification): lens framework + 4 lens instances + complexity contract + cross-target consistency. Updates to docs/r3-structure.md: - §Summary: 12 lanes + 1 standing program → 16 lanes + 1 standing program - §Lane structure: 4 new rows - §Manager structure: 8 → 9 standing managers; 3 → 4 modifications - NEW §Standing program — R3 Debt-Paydown section authored - T-Numeric-Construction lane row updated to 13 types in scope (was 8; per 2026-05-02 PM audit + Substrate Mgr ack) R3 scope ratchet: ~58% (over current 12-lane denominator) → ~38% (over expanded 17-lane denominator); numerator unchanged. Honest timeline projection: R3 close in 5-8 weeks at current velocity. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * docs(r3): T-Numeric-Construction row — 8-type → 13-type scope citation + traceability Director callout on PR #1480: §Summary item 6 says 13 types in scope but §Lane structure table row 138 still said 8. Internal inconsistency. Fix: §Lane structure table row 138 updated to 13 types in scope, with explicit citation chain: - original 8-type count from PR #1430 §A audit - extended to 13 after fresh PM sweep found 5 additional Int-inherited refinement types (RetryCount / HttpStatus / Port / PositiveInt / NonNegativeInt) at dsl/std/types.dag:232-245 - Substrate Mgr ack at gunbc#1130 comment 4360482400 Includes: Nat-alignment opportunity flagged (NonNegativeInt → Nat, PositiveInt → Nat where range(min: 1)), cost-lens candidates for bounded-range types (RetryCount → Nat<3>, HttpStatus → Nat<10>, Port → Nat<16>) once refinement composition lands. Per Director recommendation: brief addendum documenting the audit so lane scope stays anchored. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * docs(r3): address PR #1480 cursor findings — §P5 mix-up + restored locked dispositions Fixes 3 cursor findings on PR #1480 (sha 0f32605) plus 1 exploratory: 1. §P5(b)/(c) mix-up (line 44): "vague deferrals rejected" attributes to §P5(b) per-PR gate (the rule that actually rejects vague deferrals), not §P5(c) Velocity tripwire (windowed dispatch-pause). Now also explicitly surfaces §P5(c) as separate (b) windowed-enforcement clause. 2. Restored Post-R2 emergent work disposition on Substrate/PB continuation bullet (line 187): Director-locked 2026-04-28 — emergent post-R2 work absorbs into Substrate Manager continuation, not new managers. 3. Restored Verification scope negations on Verification Manager bullet (line 189): "L6 NOT in Verification scope" + "T-CostLens-Composition NOT in Verification scope" — both Director-locked 2026-04-28. 4. Updated stale "9 of 12" / "3 non-gated" counts in §"Dependency on R2" (lines 393, 397, 399, 400, 402) to "11 of 16" / "5 non-gated" matching line 59 Summary; added T-Lens-Behavioral-Parity + T-Lens-Application-Surface to Evaluator-gated list with cascade gate note. All Director-locked 2026-04-28 dispositions tagged "carried forward through 2026-05-02 expansion" so the locks survive the lane-count change. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * docs(r3): close P5 escape hatch in r3_debt_paydown_zero_remaining gate Cursor BLOCKING finding on PR #1480 at docs/r3-structure.md:173: gate contradicted itself by allowing "deferred-to-post-R3 with Director sign-off" after stating "no tracked-debt rows survive R3 close", weakening P5/strict- forward-progress into a disposition convention. Fix: remove the deferral escape hatch entirely. Gate is unconditional — every tracked-debt row retires with PR receipt before R3 close. Grounds in user directive 2026-05-02: "all 'accidentally deferred to post R3' into R3 now". If a row appears unretirable, it surfaces as a substrate gap requiring a named R3 lane (the directive that motivated this manager's creation), not a Director-sign-off deferral. Cites INVARIANTS §P5 directly: tracked-debt deferred past R3 close is the bridge-as-steady-state pattern P5 explicitly forbids; the escape hatch reintroduced that pattern at lower cadence. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * WIP: Gunbc PM * docs(r3): reconcile T-Tests-As-Data-Completeness Evaluator-gating contradiction gpt-5-5-pro REQUEST_CHANGES finding on PR #1480 (sha 0f32605): line 59 summary said T-Tests-As-Data-Completeness is in the "5 self-contained non-Evaluator-gated" group, but lane table at line 147 lists its dependency as "R2-Evaluator (test execution runtime)". Schedulers got two incompatible authorities (P2 single-authority violation). Lane table is correct — porting Rust tests to .dag TestClaim requires the Evaluator to execute the resulting test artifacts. Updated: - Line 59 summary: 11 → 12 Evaluator-gated; 5 → 4 non-gated; T-Tests-As- Data-Completeness moved into Evaluator-gated list with reason - Line 393 (Dependency on R2): same reclassification - Line 395 (substrate-carrier-fed list): drop T-Tests-As-Data-Completeness - Line 399 (precondition applies-to list): 11 → 12 lanes - Line 400 (carve-out): 5 → 4 lanes; drop T-Tests-As-Data-Completeness - Line 402 (split-resolution sentence): 11 → 12, 5 → 4 (Findings #2 and #3 already addressed at 0c449a8 and 0de2bda respectively.) Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * docs(r3): T-Lens-Application-Surface design doc — substrate shape + 4 worked examples Per user directive 2026-05-02 ("all designs upfront, implementation sketches if needed, minimize escalations"), authoring foundational design doc that unblocks T-Lens-Application-Surface lane dispatch. Resolves design questions: 1. **Section reference shape**: `SectionRef = DeclarationScope { DeclarationId } | NodeScope { DeclarationId, NodeId }`. Three of four user-named scopes (function / module / declaration) use DeclarationId uniformly; expression scope is the exception (NodeId required because expressions live inside Declaration body sub-DAGs). 2. **Violation-policy semantics**: user-named `CompileError | Warning | Silent` resolved to fail-closed-compatible binary `Enforce | Introspect` per INVARIANTS C-8. Warning forbidden (allows violations as steady state, bridge pattern P5 forbids); Silent forbidden ("silent None" exactly the pattern feedback_fail_closed_discipline bans). 3. **Default complexity-contract policy**: opt-out (compiler enforces; explicit waiver required). Waiver shape is structural `ComplexityBudgetWaiver` declaration with `justification` field, NOT an annotation per feedback_no_annotations. 4. **4 worked examples** ratified by Director (complexity-contract / CRDT cost / memory-peak cost / opt-in parallelism) — each grounded in substrate carriers + lens-fold integration. 5. **5 open design questions** flagged for Director ratification before substrate authoring begins (module-level semantics, multiple-applications- per-section, budget-inference for default, waiver dissolution, cross-section composition). Updates r3-structure.md lane 16 row to reference the design doc, replace the @complexity_budget_waived annotation language with structural carrier name, and replace the original `CompileError | Warning | Silent` enum with the fail-closed-resolved Enforce/Introspect binary. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * docs(r3): resolve all 5 §8 open design questions in-doc per minimize-escalations directive Per user directive 2026-05-02 ("minimize escalations"), resolved the 5 open design questions that were flagged for Director ratification: §8.1 — Module-level semantics: aggregate-across-module (preserves structural distinction between module-scope and per-function-scope). §8.2 — Multiple applications: fail-closed reject duplicate (lens, section) Enforce-mode pairs; multiple Introspect admitted (idempotent). §8.3 — Default-application budget: regression-detection class, gated on T-Lens-Behavioral-Parity COMPLETE; pre-cascade Introspect-only. §8.4 — Waiver lifecycle: future lens_stale_waivers lens with named dissolution trigger; tracked in lens-library-design.md §6. §8.5 — Cross-section composition: read declared budget, not computed class (preserves abstraction barrier; cost-of-change=1). Each resolution carries explicit reasoning grounded in INVARIANTS P2/P5 + feedback memory. Implementation can proceed once cascade gates clear (T-Lens-Behavioral-Parity COMPLETE for §8.3 flip; R2-Evaluator landed for worker dispatch precondition). No further Director ratification needed on these specific points. r3-structure.md row 16 updated to reflect the design-doc resolution. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * WIP: Gunbc PM * docs(r3): cross-design coherence pass + master design index Coherence audit across the 5 design docs identified 5 cross-doc conflicts; this commit resolves all 5 and lands the master index linking them. Fixes: 1. **Producer-query single-authority** (P2): complexity-lens §2 + cost-lens §3.2 now both reference `per_call_pattern_at(d, call_site) -> CallPattern?` as the typed query surface (single authority); the underlying `per_call_descent_evidence` side-table is named as the storage backend only. Eliminates parallel-authority risk. 2. **Cementing-test shape unified** (DB-15): cost-lens §5 reshaped from custom `ForAll { p: SourceProgram in programs }` (which violated tests- as-data §2.5 — quantifiers belong on claims, not predicates) to `QuantifiedTestClaim { generator, quantifier: ForAll, predicate: DifferentialEquals }`. Now matches complexity-lens §4 and tests-as-data §2.2 shape. 3. **DB-18 element-type-refinement cross-reference**: effect-enumeration §4.1 now explicitly states that DB-18's STOP-AND-ESCALATE locks the `WorkflowEffect` variant set + variant payload shape, not element-type within `LinearEffect.ops: List<X>`. The `OperationEffect` → `Operation` retypes is additive tightening within DB-18's permitted refinement scope. 4. **Resource-threaded signature compatibility**: cost-lens §3.3 now explicitly notes that `per_call_pattern_at` reads from threaded arrow signatures (per effect-enumeration §2.4) — signature-shape-agnostic producer; broadening covers both pre-migration and post-migration signature shapes. 5. **TestClaim shape for lens-application demonstrations**: lens-application §4 now declares all 4 worked-example closure gates use `TestClaim` (DB-15 enumerated form), not `QuantifiedTestClaim`. Property tests over the lens-application substrate live in T-Tests-As-Data scope, not T-Lens-Application-Surface scope. 6. **Register-migration sequencing**: tests-as-data §8.3 now lists the 4 sibling lens design docs whose register-row "→ COMPLETE" closure steps depend on the markdown→.dag migration landing first (substrate work in sibling lanes does NOT depend; only the closure-gate row update does). Plus: NEW `docs/design-r3-lens-substrate-index.md` — master index linking all 5 design docs, documenting cross-doc edges (substrate authority single-points + cementing-test format + cross-cutting invariants), and naming lane dispatch order. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * docs(r3): address 4 cursor findings on PR #1480 (sha 16340c5) 1. **Lane 16 row 40 stale text vs row 148 resolved** (P2 single-authority): row 40 still carried the original `CompileError | Warning | Silent` enum + `@complexity_budget_waived` annotation language; row 148 had the resolved `ViolationPolicy = Enforce | Introspect` + structural `ComplexityBudgetWaiver` carrier. Updated row 40 to match the resolved story (single authority). 2. **Line 44 duplicate (b) and (c) labels**: the Hybrid mechanism outer enumeration used (a)/(b)/(c) but referenced INVARIANTS §P5 sub- mechanisms (a)/(b)/(c) inside; same letter labels at different levels confused parsing. Renamed outer enumeration to (1)/(2)/(3) with footnote explaining the distinction. 3. **Line 175 contradicts line 173** (P5): line 175 said "Does enforce: tracked-debt rows get retirement PRs or explicit deferral" — the "or explicit deferral" reads like deferral remains an outcome, contradicting line 173's unconditional "no post-R3 deferral path". Removed the deferral language; line 175 now restates the unconditional rule + names the substrate-gap escalation path. 4. **design-complexity-lens-behavioral-completeness.md:125-127 variant- count mismatch** (P1 self-faithfulness): comment said "closed seven-variant set" / "Adding an eighth variant" but `AsymptoticClass` enumerates 8 variants (ClassConstant/Log/Linear/Linearithmic/ Quadratic/Polynomial/Exponential/Unknown). Updated comment to "eight-variant" / "ninth". Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * docs(r3): retract cost-lens parallel SizeExpr proposal — align with complexity-lens single authority Cursor BLOCKING finding on PR #1480: cost-lens proposed a new SizeExpr 5-variant coproduct as authority, while complexity-lens proposed SizeVariable.display_name enrichment for the same SymbolicCost payloads. P2/P5 violation — same substrate fact, two incompatible target shapes. Resolution: complexity-lens has the structurally correct framing. - DB-7's SymbolicCost is the unified algebra (locked). - SymbolicCost already covers SizeAdd (via SumCost) and SizeMax (via dominance ordering) — no parallel SizeExpr algebra needed. - Descent semantics like "n - 1" live in std.computation::CallPattern (the canonical E-C site), not in size expressions. A SizeShrink variant would duplicate that fact in parallel. - Asymptotically O(n - 1) ≡ O(n); descent is a call-site property, not a size-shape property. Aligned cost-lens to complexity-lens: SizeVariable gains an optional display_name: String? field; no parallel SizeExpr carrier; SymbolicCost DB-7 lock preserved unchanged. Updated: - §1.1 problem framing — drop "size arithmetic" / "aggregate sizes" framing (already covered by SymbolicCost); keep only the "named-binding semantics" gap that motivates display_name. - §1.2 target shape — SizeVariable.display_name: String? (matches complexity-lens §1.2 verbatim). - §1.3 explicit rationale for unified-algebra over parallel-SizeExpr. - §1.4 migration shape — additive field, no carrier rename, no deletion. - §3 / §5 code examples — replaced SizePort with SizeVariable shape. - §8.1 resolved-question reframe — names the rejected alternative (parallel SizeExpr) for future readers. - §8.2 names-on-carrier resolution — display_name shape per §1.2. - §10 implementation step 1 closure gate renamed size_expr_substrate_landed → sizevariable_displayname_landed. P2 single-authority restored across the 5-doc design surface. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * docs(r3): effect-enumeration — read/write distinction via algebra inhabitance, not signature shape Cursor BLOCKING finding on PR #1480 at design-effect-enumeration-resource- threading.md:151: the design's "structural recognition" claim was actually convention-level. \`R in / R out\` and \`R in / R' out\` (same type, different value) have the SAME typed signature — \`.dag\` doesn't encode value- preservation as a substrate fact. ReadShaped vs WriteShaped via signature shape alone was P1 modeling-faithfulness violation. Resolution: split the unified rule into two structural carriers per §2.4: (a) Effect SET — derived from signature: resource types in input ∩ output. Structural; the signature carries it. (b) Effect KIND — declared via algebra inhabitance on the callable: \`inhabits IdempotentRead<R>\` (read), \`inhabits Mutating<R>\` (write), \`inhabits Append<R>\` (append). Structural; the inhabitance carrier captures it. The lens consults BOTH — signature for set, inhabitance for kind. Absence of any kind inhabitance with the resource in the effect set is a fail- closed Diagnostic (EffectKindUndeclared), not a silent default. Updates: - §2.1 line 151: replace "same-value vs modified" framing with explicit effect-set-vs-effect-kind distinction; cross-link to §2.4 + §8.1. - §2.3: same fix for Network read example. - §2.4: split the unified rule into (a) effect SET (signature) + (b) effect KIND (algebra inhabitance) with pseudocode for the lens-side classification. - §4.3: update EffectShape derivation source from "signature shape" to "algebra inhabitance lookup". - §8.1: full reframe — from "same-value resolved" to "algebra inhabitance is the structural authority", with explicit rationale (per-callable authority, not per-call; rejected phantom-marker alternative per feedback_no_annotations). - §3 lens fold pseudocode: dispatch on §2.4(a) for set + §2.4(b) for kind. Preserves the existing EffectShape = IsIdempotent | IsBreaking partition (per design-composed-effect-reshape.md PR #529 R3) — only the source of the shape changes (declared inhabitance, not derived from signature). P1 modeling-faithfulness restored. Cursor finding fully resolved. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * docs(r3): lens-application — collapse ApplicationConfig into sum-type, illegal states unrepresentable Cursor BLOCKING finding on PR #1480 at design-lens-application-surface.md:43: ApplicationConfig was a record with budget: LensBudget? + violation_policy: ViolationPolicy as separate fields. This admitted illegal state combinations: - Enforce + budget=None (illegal: enforcement requires a budget) - Introspect + budget=Some(_) (illegal: introspection takes no budget) The doc explicitly noted these as type-checker-enforced invariants (lines 136-137), but per feedback_state_space_vs_behavioral_invariants those are behavioral invariants, not state-space invariants — exactly the bug pattern modeling-discipline principles 2/6 prohibit. Illegal states must be unrepresentable at the type level. Resolution: collapse ApplicationConfig and ViolationPolicy into a single sum-type that pairs budget with Enforce by construction: ```dag type ApplicationConfig = Enforce { budget: LensBudget, diagnostic_severity: DiagnosticSeverity } | Introspect ``` By construction: - Enforce ALWAYS has a budget (it's a coordinate of the variant). - Introspect NEVER has a budget (it has no payload). The "Enforce without budget" and "Introspect with budget" combinations cannot be constructed; the type-checker has no rejection rule to enforce them — they don't exist in the state space. Updates: - §2: replaced ApplicationConfig record + ViolationPolicy sum with single ApplicationConfig sum carrying budget inside Enforce variant. - §3: rewrote framing to match — the binary Enforce/Introspect is the ApplicationConfig sum itself; budget pairing is structural. - §4: all 4 worked-example syntaxes updated to `Enforce { budget, diagnostic_severity }` directly (no separate violation_policy field). - §5.1: synthesized default-application uses `Enforce { budget: <inferred>, diagnostic_severity: Error }` shape. - §3.2: explicit-introspection override syntax `apply_lens(complexity, fn, Introspect)` (no separate budget=None). - r3-structure.md rows 40 + 148: updated substrate-carrier description to name ApplicationConfig as sum-type with the structural-invariance note. Modeling principles 2/6 honored. P1 modeling-faithfulness restored. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * docs(r3): codex non-blocking findings #2 + #3 — heading/count consistency Codex review on PR #1480 sha 58f49e9 noted two non-blocking inconsistencies: NB2: design-cost-lens-sizevar-dimension-wiring.md §4.2 heading said 'CommutativeSemiring<SymbolicCost>' but §8.5 resolves to 'Semiring<SymbolicCost>' (multiplicative side does NOT enforce commutativity per §8.5 reasoning). Fixed §4.2 heading to match §8.5 resolution. NB3: design-tests-as-data-completeness.md §3.1 said 'six classes' / 'decomposes into six structural classes' but §10 step 3 enumerates C1-C7 (seven classes). Fixed §3.1 to say 'seven classes' with explicit C1-C7 cross-reference. Both load-bearing for doc-as-authority discipline (P1 modeling-faithfulness of the spec to itself). (All 4 BLOCKING findings from same review at sha 58f49e9 are already addressed at earlier commits — see PR comment for the receipts: ef21e1a / 92d9b11 / 255cca3 / 8640e67.) Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * docs(r3): fix line 199 active-surface arithmetic + line 23 exploratory clarity Cursor APPROVE_WITH_COMMENTS finding on PR #1480 sha 92d9b11: **Main finding (line 199)**: arithmetic was internally inconsistent — "expanded from 13 active surfaces" + "4 new lanes + 1 new standing program" = 18, not 17. The baseline should have been 12 (12 lanes + 0 standing programs at the 2026-04-30 lock), making 12 + 5 = 17 consistent. Fixed by restating the baseline as 12 with explicit arithmetic: 4 new lanes (enumerated by name) + 1 new standing program = +5; 12 + 5 = 17. Also pinned T-Behavioral-Expectations-Documentation explicitly as "parallel-dispatchable across existing lanes, not a separate surface" so readers don't double-count it as a 5th new lane. **Exploratory finding (line 23)**: the "added..." list mixed 4 new lanes + T-Behavioral-Expectations-Documentation (not a separate lane) + standing program in one breath. Restructured the parenthetical to enumerate the 4 new lanes by name and call out T-Behavioral-Expectations-Documentation as parallel-dispatchable explicitly. Reader can no longer mis-count. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * docs(r3): drop SizeVariable.display_name; InternTable single-authority for size names gpt-5-5-pro REQUEST_CHANGES on PR #1480 sha ef21e1a — BLOCKING #3 + #4: BLOCKING #3: SizeVariable.display_name + intern_table::name_of(source_port) created TWO authorities for the user-facing size-variable name. The §8.2 implementation note confirmed the parallel: "when display_name = Some(name), renderer uses it directly; when None, falls back to InternTable lookup". P2 single-authority violation; consumers could diverge on the same source_port. BLOCKING #4: master index design-r3-lens-substrate-index.md still claimed SizeExpr replaces SizeVariable, but cost-lens design (post-ef21e1a00) had already retracted SizeExpr in favor of unified SymbolicCost. Cross-doc authority drift. Resolution (both BLOCKINGs): - Drop display_name field entirely from cost-lens + complexity-lens designs. - SizeVariable substrate stays UNCHANGED at { source_port: PortId }. - InternTable is the single canonical name authority — already populated at parse time keyed by port_id. Renderer reads via intern_table::name_of(source_port). - The "Named SizeVar" gap from the capability register is closed by renderer-side wiring (no substrate change), not by adding a field. - Master index updated: SizeVariable line replaces the old SizeExpr line; notes InternTable as name authority. Updates: - design-cost-lens §1.2: target shape removes display_name field from SizeVariable carrier; rationale rewritten as InternTable-as-single-authority. - design-cost-lens §1.4 / §3 / §5 / §8.1 / §8.2: all display_name references scrubbed; "renderer-side InternTable name wiring" replaces "SizeVariable. display_name enrichment" throughout. - design-cost-lens §10 step 1: closure gate renamed sizevariable_displayname_landed -> renderer_intern_table_name_wiring_landed. - design-complexity-lens §1.2: same rewrite — SizeVariable carrier UNCHANGED; InternTable as name authority; explicit cross-link to cost-lens §1.2. - design-complexity-lens §7.2: resolved-question reframe. - design-r3-lens-substrate-index.md: SizeVariable line replaces SizeExpr line with InternTable-name-authority note. P2 single-authority restored. Cross-doc consistency restored. (BLOCKING #1 + #2 from same review at sha ef21e1a are already addressed at earlier commits — see PR comment for receipts: 92d9b11 + 255cca3.) Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> --------- Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
…1488) * docs(roadmap): fold 2026-05-01 paired exploratory + reflective analyses Director relayed two analyses against current main: - Exploratory (gpt-5-5-pro main@8cd5359): 9 findings against dsl/std/*.dag, src/v2/tests/src/*.rs, dsl/extdeps/, THESIS, INVARIANTS, MODELING, ROADMAP — 2 novel correctness bugs (SymbolicCost semiring violation, emitter expect() panic paths), 3 sharpened tracked items (SubValueRelation lattice-law contradiction, ?? / % syntax-parser drift, CollectionOps/StringOps/ MapOps duplicates), 4 already-tracked items - Reflective (gpt-5-5-pro main@6ea9812 → now): 5 cross-PR patterns + 6 highest-priority course corrections + verdict "advancing, scaffold-velocity dominates" PM ingestion folds into single ROADMAP debt section per Director's prior 2026-04-30 analyses ingestion pattern (PR #1319). Sections: - A: Exploratory novel correctness bugs (SymbolicCost product-zero bug, SubValueRelation BoundedLattice claim violation, emitter expect panic paths) - B: Exploratory sharpened tracked items (?? / % drift, CollectionOps/StringOps/MapOps duplicates) - C: Exploratory already-tracked confirmations (no new ROADMAP rows) - D: Reflective 5 cross-PR patterns (author-now/fire-later, test_ runner.rs second predicate language, typed-carrier-Rust-mirror accumulation, numeric philosophy mid-window shift validating T-Numeric-Construction reframe, bridge retirement tracked-not- retired) - E: Reflective 6 highest-priority course corrections with owner attribution + lane connection table - F: CI cost signal (e765c86a 60min timeout) + velocity-tripwire calibration (64 docs / 16 feat / 9 fix ratio) - G: PM strategic synthesis: 3 cross-cutting meta-themes (algebraic-law-witness coverage gap; "make scaffolds executable" cluster; "tighten existing structural enforcement" cluster) Per-finding/correction owner attribution names R3 Substrate Mgr, R3 Verification Mgr, R3 Grounding Mgr, R3 PB Mgr per ownership boundaries. Lane connections cite T-V-L4-L7-Direct, T-Free- Consequences-Demonstration, T-Ground-Services parser-grammar slice, T-Numeric-Construction Slice 2 sequencing, etc. Highest-value novel: SymbolicCost product-zero bug (cost-lens reads incorrect facts; iterate(ConstantCost(0), ...) returns body cost instead of zero) + emitter expect() panics. Highest-value sharpened-tracked: SubValueRelation BoundedLattice false-claim. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * WIP: Gunbc PM * docs(r3): R3 scope expansion 12 → 16 lanes + standing R3 Debt-Paydown program Per Director ratification 2026-05-02 at gunbc#828 comment 4362742638: User directive: per the strict reading of "nothing deferred past R3", all "accidentally deferred" gaps absorb into R3. Plus three additional asks: behavioral expectations docs per feature; compile-error complexity ratchet generalized as lens-application-surface (per user reframe); in-cycle debt-paydown discipline. NEW R3 LANES (4 added; lane count 12 → 16): 13. T-E-P-Producer-Broadening (Substrate; M-L; foundational) - broaden per-call DescentEvidence/CallPattern/SubValueRelation from first slice to full ExprCall.descent_evidence parity - prerequisite for T-Lens-Behavioral-Parity 14. T-Lens-Behavioral-Parity (Substrate + Verification cross-program; L-XL) - 4 sub-slices: complexity / cost / parallelism / effect_enumeration - bring lens-capability-register from PROXY/STUB/PARTIAL → COMPLETE - includes symbolic CostExpr full algebra; work/span split; asymptotic classification; cementing test against v2 oracle; Stage 2e parallelism walk port; resource-threading migration 15. T-Tests-As-Data-Completeness (Verification; L) - tests-as-data full coverage (thesis facet 3) - property-based testing surface (ForAll/Exists quantifiers + ProgramGenerator carrier) - cementing test discipline for .dag lenses 16. T-Lens-Application-Surface (Substrate + Verification; L-XL) - per user reframe: lens application as first-class authoring surface - apply_lens(lens, section, config) where config.violation_policy = CompileError | Warning | Silent - subsumes prior T-Complexity-Contract-Compile-Error + T-User-Authored-Cost-Basis-Discipline as configurations - 4 worked examples: complexity-contract-compile-error + CRDT cost basis + memory-peak cost basis + opt-in cross-iteration parallelism - default policy for complexity contract: opt-out NEW STANDING PROGRAM: R3 Debt-Paydown Manager (9th standing R3 Mgr) - hybrid mechanism: per-PR debt-receipt rule + standing capacity - closure gate: r3_debt_paydown_zero_remaining - per feedback_standing_managers_need_owned_deliverables FOLD-INS (3; no new lanes): - T-V-L4-L7-Direct: per-(algebra, inhabitant, law) exhaustive witness coverage (catches SymbolicCost product-zero bug class structurally) - T-Ground-Diagnostic: closed-axis enforcement (no String dispatch on closed sets); replaces MissingEmissionPath { connective: String, ... } - T-LensProducer-Retirement: ownership d/e/f confirmed delivered (not separately deferred) T-Behavioral-Expectations-Documentation (parallel-dispatchable; 7 load- bearing features per Director ratification): lens framework + 4 lens instances + complexity contract + cross-target consistency. Updates to docs/r3-structure.md: - §Summary: 12 lanes + 1 standing program → 16 lanes + 1 standing program - §Lane structure: 4 new rows - §Manager structure: 8 → 9 standing managers; 3 → 4 modifications - NEW §Standing program — R3 Debt-Paydown section authored - T-Numeric-Construction lane row updated to 13 types in scope (was 8; per 2026-05-02 PM audit + Substrate Mgr ack) R3 scope ratchet: ~58% (over current 12-lane denominator) → ~38% (over expanded 17-lane denominator); numerator unchanged. Honest timeline projection: R3 close in 5-8 weeks at current velocity. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * docs(r3): T-Numeric-Construction row — 8-type → 13-type scope citation + traceability Director callout on PR #1480: §Summary item 6 says 13 types in scope but §Lane structure table row 138 still said 8. Internal inconsistency. Fix: §Lane structure table row 138 updated to 13 types in scope, with explicit citation chain: - original 8-type count from PR #1430 §A audit - extended to 13 after fresh PM sweep found 5 additional Int-inherited refinement types (RetryCount / HttpStatus / Port / PositiveInt / NonNegativeInt) at dsl/std/types.dag:232-245 - Substrate Mgr ack at gunbc#1130 comment 4360482400 Includes: Nat-alignment opportunity flagged (NonNegativeInt → Nat, PositiveInt → Nat where range(min: 1)), cost-lens candidates for bounded-range types (RetryCount → Nat<3>, HttpStatus → Nat<10>, Port → Nat<16>) once refinement composition lands. Per Director recommendation: brief addendum documenting the audit so lane scope stays anchored. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * docs(r3): address PR #1480 cursor findings — §P5 mix-up + restored locked dispositions Fixes 3 cursor findings on PR #1480 (sha 0f32605d) plus 1 exploratory: 1. §P5(b)/(c) mix-up (line 44): "vague deferrals rejected" attributes to §P5(b) per-PR gate (the rule that actually rejects vague deferrals), not §P5(c) Velocity tripwire (windowed dispatch-pause). Now also explicitly surfaces §P5(c) as separate (b) windowed-enforcement clause. 2. Restored Post-R2 emergent work disposition on Substrate/PB continuation bullet (line 187): Director-locked 2026-04-28 — emergent post-R2 work absorbs into Substrate Manager continuation, not new managers. 3. Restored Verification scope negations on Verification Manager bullet (line 189): "L6 NOT in Verification scope" + "T-CostLens-Composition NOT in Verification scope" — both Director-locked 2026-04-28. 4. Updated stale "9 of 12" / "3 non-gated" counts in §"Dependency on R2" (lines 393, 397, 399, 400, 402) to "11 of 16" / "5 non-gated" matching line 59 Summary; added T-Lens-Behavioral-Parity + T-Lens-Application-Surface to Evaluator-gated list with cascade gate note. All Director-locked 2026-04-28 dispositions tagged "carried forward through 2026-05-02 expansion" so the locks survive the lane-count change. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * docs(r3): close P5 escape hatch in r3_debt_paydown_zero_remaining gate Cursor BLOCKING finding on PR #1480 at docs/r3-structure.md:173: gate contradicted itself by allowing "deferred-to-post-R3 with Director sign-off" after stating "no tracked-debt rows survive R3 close", weakening P5/strict- forward-progress into a disposition convention. Fix: remove the deferral escape hatch entirely. Gate is unconditional — every tracked-debt row retires with PR receipt before R3 close. Grounds in user directive 2026-05-02: "all 'accidentally deferred to post R3' into R3 now". If a row appears unretirable, it surfaces as a substrate gap requiring a named R3 lane (the directive that motivated this manager's creation), not a Director-sign-off deferral. Cites INVARIANTS §P5 directly: tracked-debt deferred past R3 close is the bridge-as-steady-state pattern P5 explicitly forbids; the escape hatch reintroduced that pattern at lower cadence. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * WIP: Gunbc PM * docs(r3): reconcile T-Tests-As-Data-Completeness Evaluator-gating contradiction gpt-5-5-pro REQUEST_CHANGES finding on PR #1480 (sha 0f32605d): line 59 summary said T-Tests-As-Data-Completeness is in the "5 self-contained non-Evaluator-gated" group, but lane table at line 147 lists its dependency as "R2-Evaluator (test execution runtime)". Schedulers got two incompatible authorities (P2 single-authority violation). Lane table is correct — porting Rust tests to .dag TestClaim requires the Evaluator to execute the resulting test artifacts. Updated: - Line 59 summary: 11 → 12 Evaluator-gated; 5 → 4 non-gated; T-Tests-As- Data-Completeness moved into Evaluator-gated list with reason - Line 393 (Dependency on R2): same reclassification - Line 395 (substrate-carrier-fed list): drop T-Tests-As-Data-Completeness - Line 399 (precondition applies-to list): 11 → 12 lanes - Line 400 (carve-out): 5 → 4 lanes; drop T-Tests-As-Data-Completeness - Line 402 (split-resolution sentence): 11 → 12, 5 → 4 (Findings #2 and #3 already addressed at 0c449a869 and 0de2bda06 respectively.) Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * docs(r3): T-Lens-Application-Surface design doc — substrate shape + 4 worked examples Per user directive 2026-05-02 ("all designs upfront, implementation sketches if needed, minimize escalations"), authoring foundational design doc that unblocks T-Lens-Application-Surface lane dispatch. Resolves design questions: 1. **Section reference shape**: `SectionRef = DeclarationScope { DeclarationId } | NodeScope { DeclarationId, NodeId }`. Three of four user-named scopes (function / module / declaration) use DeclarationId uniformly; expression scope is the exception (NodeId required because expressions live inside Declaration body sub-DAGs). 2. **Violation-policy semantics**: user-named `CompileError | Warning | Silent` resolved to fail-closed-compatible binary `Enforce | Introspect` per INVARIANTS C-8. Warning forbidden (allows violations as steady state, bridge pattern P5 forbids); Silent forbidden ("silent None" exactly the pattern feedback_fail_closed_discipline bans). 3. **Default complexity-contract policy**: opt-out (compiler enforces; explicit waiver required). Waiver shape is structural `ComplexityBudgetWaiver` declaration with `justification` field, NOT an annotation per feedback_no_annotations. 4. **4 worked examples** ratified by Director (complexity-contract / CRDT cost / memory-peak cost / opt-in parallelism) — each grounded in substrate carriers + lens-fold integration. 5. **5 open design questions** flagged for Director ratification before substrate authoring begins (module-level semantics, multiple-applications- per-section, budget-inference for default, waiver dissolution, cross-section composition). Updates r3-structure.md lane 16 row to reference the design doc, replace the @complexity_budget_waived annotation language with structural carrier name, and replace the original `CompileError | Warning | Silent` enum with the fail-closed-resolved Enforce/Introspect binary. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * docs(r3): resolve all 5 §8 open design questions in-doc per minimize-escalations directive Per user directive 2026-05-02 ("minimize escalations"), resolved the 5 open design questions that were flagged for Director ratification: §8.1 — Module-level semantics: aggregate-across-module (preserves structural distinction between module-scope and per-function-scope). §8.2 — Multiple applications: fail-closed reject duplicate (lens, section) Enforce-mode pairs; multiple Introspect admitted (idempotent). §8.3 — Default-application budget: regression-detection class, gated on T-Lens-Behavioral-Parity COMPLETE; pre-cascade Introspect-only. §8.4 — Waiver lifecycle: future lens_stale_waivers lens with named dissolution trigger; tracked in lens-library-design.md §6. §8.5 — Cross-section composition: read declared budget, not computed class (preserves abstraction barrier; cost-of-change=1). Each resolution carries explicit reasoning grounded in INVARIANTS P2/P5 + feedback memory. Implementation can proceed once cascade gates clear (T-Lens-Behavioral-Parity COMPLETE for §8.3 flip; R2-Evaluator landed for worker dispatch precondition). No further Director ratification needed on these specific points. r3-structure.md row 16 updated to reflect the design-doc resolution. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * WIP: Gunbc PM * docs(r3): cross-design coherence pass + master design index Coherence audit across the 5 design docs identified 5 cross-doc conflicts; this commit resolves all 5 and lands the master index linking them. Fixes: 1. **Producer-query single-authority** (P2): complexity-lens §2 + cost-lens §3.2 now both reference `per_call_pattern_at(d, call_site) -> CallPattern?` as the typed query surface (single authority); the underlying `per_call_descent_evidence` side-table is named as the storage backend only. Eliminates parallel-authority risk. 2. **Cementing-test shape unified** (DB-15): cost-lens §5 reshaped from custom `ForAll { p: SourceProgram in programs }` (which violated tests- as-data §2.5 — quantifiers belong on claims, not predicates) to `QuantifiedTestClaim { generator, quantifier: ForAll, predicate: DifferentialEquals }`. Now matches complexity-lens §4 and tests-as-data §2.2 shape. 3. **DB-18 element-type-refinement cross-reference**: effect-enumeration §4.1 now explicitly states that DB-18's STOP-AND-ESCALATE locks the `WorkflowEffect` variant set + variant payload shape, not element-type within `LinearEffect.ops: List<X>`. The `OperationEffect` → `Operation` retypes is additive tightening within DB-18's permitted refinement scope. 4. **Resource-threaded signature compatibility**: cost-lens §3.3 now explicitly notes that `per_call_pattern_at` reads from threaded arrow signatures (per effect-enumeration §2.4) — signature-shape-agnostic producer; broadening covers both pre-migration and post-migration signature shapes. 5. **TestClaim shape for lens-application demonstrations**: lens-application §4 now declares all 4 worked-example closure gates use `TestClaim` (DB-15 enumerated form), not `QuantifiedTestClaim`. Property tests over the lens-application substrate live in T-Tests-As-Data scope, not T-Lens-Application-Surface scope. 6. **Register-migration sequencing**: tests-as-data §8.3 now lists the 4 sibling lens design docs whose register-row "→ COMPLETE" closure steps depend on the markdown→.dag migration landing first (substrate work in sibling lanes does NOT depend; only the closure-gate row update does). Plus: NEW `docs/design-r3-lens-substrate-index.md` — master index linking all 5 design docs, documenting cross-doc edges (substrate authority single-points + cementing-test format + cross-cutting invariants), and naming lane dispatch order. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * docs(r3): address 4 cursor findings on PR #1480 (sha 16340c52) 1. **Lane 16 row 40 stale text vs row 148 resolved** (P2 single-authority): row 40 still carried the original `CompileError | Warning | Silent` enum + `@complexity_budget_waived` annotation language; row 148 had the resolved `ViolationPolicy = Enforce | Introspect` + structural `ComplexityBudgetWaiver` carrier. Updated row 40 to match the resolved story (single authority). 2. **Line 44 duplicate (b) and (c) labels**: the Hybrid mechanism outer enumeration used (a)/(b)/(c) but referenced INVARIANTS §P5 sub- mechanisms (a)/(b)/(c) inside; same letter labels at different levels confused parsing. Renamed outer enumeration to (1)/(2)/(3) with footnote explaining the distinction. 3. **Line 175 contradicts line 173** (P5): line 175 said "Does enforce: tracked-debt rows get retirement PRs or explicit deferral" — the "or explicit deferral" reads like deferral remains an outcome, contradicting line 173's unconditional "no post-R3 deferral path". Removed the deferral language; line 175 now restates the unconditional rule + names the substrate-gap escalation path. 4. **design-complexity-lens-behavioral-completeness.md:125-127 variant- count mismatch** (P1 self-faithfulness): comment said "closed seven-variant set" / "Adding an eighth variant" but `AsymptoticClass` enumerates 8 variants (ClassConstant/Log/Linear/Linearithmic/ Quadratic/Polynomial/Exponential/Unknown). Updated comment to "eight-variant" / "ninth". Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * docs(r3): retract cost-lens parallel SizeExpr proposal — align with complexity-lens single authority Cursor BLOCKING finding on PR #1480: cost-lens proposed a new SizeExpr 5-variant coproduct as authority, while complexity-lens proposed SizeVariable.display_name enrichment for the same SymbolicCost payloads. P2/P5 violation — same substrate fact, two incompatible target shapes. Resolution: complexity-lens has the structurally correct framing. - DB-7's SymbolicCost is the unified algebra (locked). - SymbolicCost already covers SizeAdd (via SumCost) and SizeMax (via dominance ordering) — no parallel SizeExpr algebra needed. - Descent semantics like "n - 1" live in std.computation::CallPattern (the canonical E-C site), not in size expressions. A SizeShrink variant would duplicate that fact in parallel. - Asymptotically O(n - 1) ≡ O(n); descent is a call-site property, not a size-shape property. Aligned cost-lens to complexity-lens: SizeVariable gains an optional display_name: String? field; no parallel SizeExpr carrier; SymbolicCost DB-7 lock preserved unchanged. Updated: - §1.1 problem framing — drop "size arithmetic" / "aggregate sizes" framing (already covered by SymbolicCost); keep only the "named-binding semantics" gap that motivates display_name. - §1.2 target shape — SizeVariable.display_name: String? (matches complexity-lens §1.2 verbatim). - §1.3 explicit rationale for unified-algebra over parallel-SizeExpr. - §1.4 migration shape — additive field, no carrier rename, no deletion. - §3 / §5 code examples — replaced SizePort with SizeVariable shape. - §8.1 resolved-question reframe — names the rejected alternative (parallel SizeExpr) for future readers. - §8.2 names-on-carrier resolution — display_name shape per §1.2. - §10 implementation step 1 closure gate renamed size_expr_substrate_landed → sizevariable_displayname_landed. P2 single-authority restored across the 5-doc design surface. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * docs(r3): effect-enumeration — read/write distinction via algebra inhabitance, not signature shape Cursor BLOCKING finding on PR #1480 at design-effect-enumeration-resource- threading.md:151: the design's "structural recognition" claim was actually convention-level. \`R in / R out\` and \`R in / R' out\` (same type, different value) have the SAME typed signature — \`.dag\` doesn't encode value- preservation as a substrate fact. ReadShaped vs WriteShaped via signature shape alone was P1 modeling-faithfulness violation. Resolution: split the unified rule into two structural carriers per §2.4: (a) Effect SET — derived from signature: resource types in input ∩ output. Structural; the signature carries it. (b) Effect KIND — declared via algebra inhabitance on the callable: \`inhabits IdempotentRead<R>\` (read), \`inhabits Mutating<R>\` (write), \`inhabits Append<R>\` (append). Structural; the inhabitance carrier captures it. The lens consults BOTH — signature for set, inhabitance for kind. Absence of any kind inhabitance with the resource in the effect set is a fail- closed Diagnostic (EffectKindUndeclared), not a silent default. Updates: - §2.1 line 151: replace "same-value vs modified" framing with explicit effect-set-vs-effect-kind distinction; cross-link to §2.4 + §8.1. - §2.3: same fix for Network read example. - §2.4: split the unified rule into (a) effect SET (signature) + (b) effect KIND (algebra inhabitance) with pseudocode for the lens-side classification. - §4.3: update EffectShape derivation source from "signature shape" to "algebra inhabitance lookup". - §8.1: full reframe — from "same-value resolved" to "algebra inhabitance is the structural authority", with explicit rationale (per-callable authority, not per-call; rejected phantom-marker alternative per feedback_no_annotations). - §3 lens fold pseudocode: dispatch on §2.4(a) for set + §2.4(b) for kind. Preserves the existing EffectShape = IsIdempotent | IsBreaking partition (per design-composed-effect-reshape.md PR #529 R3) — only the source of the shape changes (declared inhabitance, not derived from signature). P1 modeling-faithfulness restored. Cursor finding fully resolved. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * docs(r3): lens-application — collapse ApplicationConfig into sum-type, illegal states unrepresentable Cursor BLOCKING finding on PR #1480 at design-lens-application-surface.md:43: ApplicationConfig was a record with budget: LensBudget? + violation_policy: ViolationPolicy as separate fields. This admitted illegal state combinations: - Enforce + budget=None (illegal: enforcement requires a budget) - Introspect + budget=Some(_) (illegal: introspection takes no budget) The doc explicitly noted these as type-checker-enforced invariants (lines 136-137), but per feedback_state_space_vs_behavioral_invariants those are behavioral invariants, not state-space invariants — exactly the bug pattern modeling-discipline principles 2/6 prohibit. Illegal states must be unrepresentable at the type level. Resolution: collapse ApplicationConfig and ViolationPolicy into a single sum-type that pairs budget with Enforce by construction: ```dag type ApplicationConfig = Enforce { budget: LensBudget, diagnostic_severity: DiagnosticSeverity } | Introspect ``` By construction: - Enforce ALWAYS has a budget (it's a coordinate of the variant). - Introspect NEVER has a budget (it has no payload). The "Enforce without budget" and "Introspect with budget" combinations cannot be constructed; the type-checker has no rejection rule to enforce them — they don't exist in the state space. Updates: - §2: replaced ApplicationConfig record + ViolationPolicy sum with single ApplicationConfig sum carrying budget inside Enforce variant. - §3: rewrote framing to match — the binary Enforce/Introspect is the ApplicationConfig sum itself; budget pairing is structural. - §4: all 4 worked-example syntaxes updated to `Enforce { budget, diagnostic_severity }` directly (no separate violation_policy field). - §5.1: synthesized default-application uses `Enforce { budget: <inferred>, diagnostic_severity: Error }` shape. - §3.2: explicit-introspection override syntax `apply_lens(complexity, fn, Introspect)` (no separate budget=None). - r3-structure.md rows 40 + 148: updated substrate-carrier description to name ApplicationConfig as sum-type with the structural-invariance note. Modeling principles 2/6 honored. P1 modeling-faithfulness restored. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * docs(r3): codex non-blocking findings #2 + #3 — heading/count consistency Codex review on PR #1480 sha 58f49e91 noted two non-blocking inconsistencies: NB2: design-cost-lens-sizevar-dimension-wiring.md §4.2 heading said 'CommutativeSemiring<SymbolicCost>' but §8.5 resolves to 'Semiring<SymbolicCost>' (multiplicative side does NOT enforce commutativity per §8.5 reasoning). Fixed §4.2 heading to match §8.5 resolution. NB3: design-tests-as-data-completeness.md §3.1 said 'six classes' / 'decomposes into six structural classes' but §10 step 3 enumerates C1-C7 (seven classes). Fixed §3.1 to say 'seven classes' with explicit C1-C7 cross-reference. Both load-bearing for doc-as-authority discipline (P1 modeling-faithfulness of the spec to itself). (All 4 BLOCKING findings from same review at sha 58f49e91 are already addressed at earlier commits — see PR comment for the receipts: ef21e1a00 / 92d9b11cf / 255cca3cb / 8640e6701.) Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * docs(r3): fix line 199 active-surface arithmetic + line 23 exploratory clarity Cursor APPROVE_WITH_COMMENTS finding on PR #1480 sha 92d9b11c: **Main finding (line 199)**: arithmetic was internally inconsistent — "expanded from 13 active surfaces" + "4 new lanes + 1 new standing program" = 18, not 17. The baseline should have been 12 (12 lanes + 0 standing programs at the 2026-04-30 lock), making 12 + 5 = 17 consistent. Fixed by restating the baseline as 12 with explicit arithmetic: 4 new lanes (enumerated by name) + 1 new standing program = +5; 12 + 5 = 17. Also pinned T-Behavioral-Expectations-Documentation explicitly as "parallel-dispatchable across existing lanes, not a separate surface" so readers don't double-count it as a 5th new lane. **Exploratory finding (line 23)**: the "added..." list mixed 4 new lanes + T-Behavioral-Expectations-Documentation (not a separate lane) + standing program in one breath. Restructured the parenthetical to enumerate the 4 new lanes by name and call out T-Behavioral-Expectations-Documentation as parallel-dispatchable explicitly. Reader can no longer mis-count. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * docs(r3): drop SizeVariable.display_name; InternTable single-authority for size names gpt-5-5-pro REQUEST_CHANGES on PR #1480 sha ef21e1a0 — BLOCKING #3 + #4: BLOCKING #3: SizeVariable.display_name + intern_table::name_of(source_port) created TWO authorities for the user-facing size-variable name. The §8.2 implementation note confirmed the parallel: "when display_name = Some(name), renderer uses it directly; when None, falls back to InternTable lookup". P2 single-authority violation; consumers could diverge on the same source_port. BLOCKING #4: master index design-r3-lens-substrate-index.md still claimed SizeExpr replaces SizeVariable, but cost-lens design (post-ef21e1a00) had already retracted SizeExpr in favor of unified SymbolicCost. Cross-doc authority drift. Resolution (both BLOCKINGs): - Drop display_name field entirely from cost-lens + complexity-lens designs. - SizeVariable substrate stays UNCHANGED at { source_port: PortId }. - InternTable is the single canonical name authority — already populated at parse time keyed by port_id. Renderer reads via intern_table::name_of(source_port). - The "Named SizeVar" gap from the capability register is closed by renderer-side wiring (no substrate change), not by adding a field. - Master index updated: SizeVariable line replaces the old SizeExpr line; notes InternTable as name authority. Updates: - design-cost-lens §1.2: target shape removes display_name field from SizeVariable carrier; rationale rewritten as InternTable-as-single-authority. - design-cost-lens §1.4 / §3 / §5 / §8.1 / §8.2: all display_name references scrubbed; "renderer-side InternTable name wiring" replaces "SizeVariable. display_name enrichment" throughout. - design-cost-lens §10 step 1: closure gate renamed sizevariable_displayname_landed -> renderer_intern_table_name_wiring_landed. - design-complexity-lens §1.2: same rewrite — SizeVariable carrier UNCHANGED; InternTable as name authority; explicit cross-link to cost-lens §1.2. - design-complexity-lens §7.2: resolved-question reframe. - design-r3-lens-substrate-index.md: SizeVariable line replaces SizeExpr line with InternTable-name-authority note. P2 single-authority restored. Cross-doc consistency restored. (BLOCKING #1 + #2 from same review at sha ef21e1a0 are already addressed at earlier commits — see PR comment for receipts: 92d9b11cf + 255cca3cb.) Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * docs(r3): codex review wave (sha 98f2fc4f) — 4 BLOCKING + 2 NB findings addressed BLOCKING #1: lens-application config not parametric in C — lens/budget pair relied on type-checker convention rather than structural typing. Fix: SectionedLensApplication<C> + ApplicationConfig<C> parametric in the lens carrier C; lens: Lens<C> and config.budget: C share the same C structurally. Mismatch is unrepresentable, not type-checker-rejected. Per-lens budgets dissolve into the existing Lens<C> carrier — no separate ComplexityBudget/CostBudget/ParallelismBudget carriers needed. BLOCKING #2: complexity-lens Certainty composed independently from cost dominance. Fix: define joint compose_summary function (§3.1) where certainty composition is cost-aware — when dominance drops a cost component, that component's certainty does NOT enter the result. Surfaces v2's implicit Θ(n²) Proven semantics; cost-unaware certainty would diverge from v2 on the cementing fixture corpus. BLOCKING #3: effect-enumeration line 17 prose still claimed signature is "one structural authority" for effects. Fix: updated to name the two orthogonal authorities — signature for effect SET, algebra inhabitance for effect KIND. Aligned with §2.4 + §8.1 that I'd already fixed at 92d9b11cf. BLOCKING #4: sibling lens docs and tests-as-data didn't share one cementing closure shape — complexity + effect proposed Rust cementing tests, cost (after my earlier fix at ef21e1a00) proposed QuantifiedTestClaim. Inconsistency. Fix: align all three on **Rust cementing today + dissolution trigger to tests-as-data step 5 .dag port**. Per-lens divergence is now explicitly forbidden in the master index. NB1: cost-lens §1.4 still said "single field addition" / "Rust mirror single field add" after the InternTable fix removed the field add. Cleaned up to "renderer-only, no substrate change". NB2: tests-as-data §3 said "17 variants" but enumerated 22 (Compiles ... BridgeLedgerZero). Fixed count to 22. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * docs(r3): scrub residual non-parametric LensBudget references Cursor BLOCKING at sha 98f2fc4f line 102 — incomplete fix for parametric SectionedLensApplication<C> migration at 812f6a141. Three lines still referenced the old non-parametric framing: - Line 100: "type-checker verifies b inhabits lens.budget_type" — type-checker convention rather than structural typing. - Line 114: ApplicationConfig redeclared without <C> parameter. - Line 262: substrate-owner mention of "per-lens budget_type declaration extension". - Line 351: "each lens owns its own LensBudget definition" — implied separate budget carriers. - Line 357: implementation step said "Lens<C>.budget_type field added". All updated to reflect the parametric resolution (per §2): - ApplicationConfig<C> parametric in lens carrier C; lens/budget pair is structural via shared C. - Mismatch is unrepresentable, NOT type-checker-rejected. - No budget_type field on Lens<C>; the parameter C IS the structural authority. - Each lens's existing Lens<C> carrier IS the budget type; no new per-lens budget carriers. References to "budget_type" / "LensBudget" remain only in negation form ("not via budget_type field", "no LensBudget definition") to document the rejected alternative for future readers. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * docs(r3): lens-application — dissolve regression_baseline_pinned optional field Cursor BLOCKING at sha 98f2fc4f line 323 (actually line 308 — drift after prior edits): regression_baseline_pinned: AsymptoticClass? was an optional field on SectionedLensApplication where absence = introspection mode and presence = enforcement mode. This re-creates EXACTLY the illegal-states-representable pattern that the §2 ApplicationConfig sum-type fix dissolved (the original finding at design-lens-application- surface.md:43 from a prior wave). Fix: dissolve the optional field. The cascade-flip (T-Lens-Behavioral- Parity COMPLETE flipping default complexity from Introspect to Enforce) is purely SYNTHESIZER-side, not substrate-side: - Pre-cascade: synthesizer emits `Introspect` for every default complexity application. - Post-cascade: synthesizer emits `Enforce { budget: <computed class>, diagnostic_severity: Error }` — the computed class IS the regression baseline; the variant choice carries the fact structurally. No optional field on the carrier. The cascade just changes which variant the synthesizer constructs. Same illegal-states-unrepresentable discipline as §2. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * docs(r3): drop certainty_lattice — Certainty composition is cost-aware, not lattice-fold Cursor BLOCKING at sha 98f2fc4f line 196: join_certainty's "Proven wins under alternative" semantic was P1 unfaithful — a Proven branch arm could hide a Conservative arm carrying the actual worst-case bound, so the result's certainty would no longer faithfully describe the bound it qualifies. Same cost-unaware pattern as the §3.1 BLOCKING from earlier in the wave (composition independent from cost dominance). Resolution: drop the BoundedLattice<Certainty> declaration entirely. Certainty does NOT compose via lattice meet/join; composition is cost-aware per §3.1 compose_summary_* family. The lattice declaration was misleading — it suggested an independent composition pattern that contradicts the cost-aware design. Updates: - §1.5: removed `data certainty_lattice` declaration + meet_certainty + join_certainty function bodies. Replaced with prose explaining cost-aware composition + tightness-ordering distinction (ordering is implicit when projecting; not a composition operation). - §3.1: meet_certainty(...) call → meet_pair(...) inline helper, with explicit comment that it's used ONLY when both contributions survive cost composition (NOT a free-standing lattice op). - §11 cascade-gate list: removed "data certainty_lattice" from the class-5-grammar dependent declarations list with explanatory note. Same illegal-states-unrepresentable + cost-aware-composition discipline preserved end-to-end across the §3.1 + §1.5 + §3.x compose_summary_* chain. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * docs(r3): effect-enumeration §8.4 — derive readonly deletion from algebra inhabitance, not signature shape Cursor BLOCKING at sha 98f2fc4f line 442: §8.4 "readonly keyword deletion" rationale said the keyword is "structurally derivable: an operation is read-shaped iff every threaded resource appears unchanged in input and output." This contradicts §2.4's locked rule that effect KIND is declared only via algebra inhabitance (inhabits IdempotentRead<R>), NOT derived from signature shape — same modeling-discipline violation as the line 151 BLOCKING from the prior wave (cursor BLOCKING #2 of this codex-wave). Resolution: rewrite §8.4 to derive readonly's deletion rationale from algebra inhabitance, not signature shape: - After migration, read kind is declared via `inhabits IdempotentRead<R>` on the callable (per §2.4 + §8.1) — structural fact. - The `readonly` keyword duplicates that inhabitance: same fact, two carriers. P2 single-authority + feedback_no_annotations forbid this. - Keyword is redundant AND drift-prone (feedback_state_space_vs_ behavioral_invariants: keyword could disagree with inhabitance). - Implementation-mechanical: every operation currently using `readonly` already has a corresponding `inhabits IdempotentRead<R>` declared at the migration site (one-to-one mapping in the atomic PR per §6). The §2.4 → §8.1 → §8.4 chain is now consistent end-to-end: signature carries effect SET; algebra inhabitance carries effect KIND; the readonly annotation is the same parallel-authority bug pattern P5/P2 forbid. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * docs(r3): fix tests-as-data dissolution-trigger cross-reference §10 → §6 Cursor APPROVE_WITH_COMMENTS finding on PR #1488 (sha 95b54f54): all 4 docs cross-referencing the cementing-dispatch-port dissolution trigger pointed at "tests-as-data §10 step 5", but tests-as-data has no §10 — the implementation-order list (containing step 5 = cementing dispatch port) is at §6. Fixed in 4 places: - docs/design-r3-lens-substrate-index.md:39 - docs/design-complexity-lens-behavioral-completeness.md:425 - docs/design-cost-lens-sizevar-dimension-wiring.md:314 - docs/design-effect-enumeration-resource-threading.md:489 Per INVARIANTS "Documentation Describes Live State" — readers can now resolve the cited anchor. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * docs(r3): cost-lens cementing — tighten Band-C parity claim to full SymbolicCost/CostExpr carrier gpt-5-5-pro APPROVE_WITH_COMMENTS finding on PR #1488 sha fa5f1675: line 316 said "asserting structural equivalence on the asymptotic class" which could weaken the Band-C parity assertion if read literally — the asymptotic class is a projection of SymbolicCost, not the full carrier. Tightened to commit to the stronger claim: cementing asserts structural equivalence on the FULL SymbolicCost/CostExpr carrier shape (not a projection). Asymptotic-class equivalence is a downstream consequence, not a substitute. Aligns with the structural_equivalent() function shape already declared at line 318. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * docs(r3): remove implicit Enforce-with-inferred-baseline; align Certainty no-lattice references Codex BLOCKING on PR #1488 sha 265d8ef7: §8.3 + §3.2 + §5.1 said the default complexity application post-cascade flips to Enforce mode with "budget = computed asymptotic class at synthesis time" — but the synthesizer recomputes from the current body each compile, so the baseline moves with the body. Whatever class the function has becomes both "current" and "baseline"; they always agree; no regression ever fires. The fact the design claimed to enforce was lost on every recompile. P2 single-authority + facts-flow-forward violation. Resolution: remove the implicit Enforce mode entirely. Default is Introspect-only for unannotated functions; user explicitly authors Enforce { budget: <chosen class>, ... } to opt into enforcement. No auto-inferred baseline — those would need persisted authority (either generated source, forbidden by feedback_no_generated_code_on_disk, or sidecar files, same problem). The structural answer: complexity contracts are user-authored. Re-framing "opt-out for complexity" per the original user directive: the user can opt out (by not authoring an Enforce application or by authoring Introspect); compile errors fire when the user opts IN with a budget the actual function exceeds. ComplexityBudgetWaiver retains its purpose — accepting known violations of explicit user contracts. Codex NB: residual references to "Certainty + lattice declaration" / "two new lattice instances" in complexity-lens lines 535 + 579 didn't match the §1.5 lattice deletion. Updated both to single BoundedLattice<AsymptoticClass> instance + Certainty 2-variant sum WITHOUT lattice (composition is cost-aware via §3.1 compose_summary_*). Updates: - §3.2 (Default policy): full reframe to user-driven contracts. - §5.1 (Default-application synthesis): synthesizer never emits Enforce; only Introspect for unannotated functions. - §8.3 (Default-application semantics): RESOLVED with new framing — user-driven contracts; no implicit baseline; explicit rationale for why generated-source is not the answer. - complexity-lens §5 step 2 + §7.4: drop "Certainty + lattice declaration" and "BoundedLattice<Certainty>" from the substrate-landing list and ROADMAP-P2 dissolution accounting. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * WIP: Gunbc PM * docs(r3): lens-application — add LensEnforcement<Output, Budget> projection carrier Codex BLOCKING on PR #1488 sha 265d8ef7 line 100: tying ApplicationConfig<C> to the same C as Lens<C> made the complexity lens budget = AsymptoticClass, but the complexity-lens design publishes Lookup<ComplexitySummary> with work/span/certainty as the lens output. Either drop downstream facts (force output = AsymptoticClass) or contradict the lens-output contract (output = ComplexitySummary; budget = AsymptoticClass; type system can't enforce compatibility). P1 modeling faithfulness + facts-flow-forward violation. Resolution: introduce LensEnforcement<Output, Budget> projection carrier in §2. Each lens declares both: - Lens<Output> for the read function (rich output type — load-bearing for lens-fold composition per compose_summary_*) - LensEnforcement<Output, Budget> for the projection from Output to the budget-comparable type (identity for cost; summary.asymptotic_class for complexity) SectionedLensApplication<Output, Budget> is parametric in BOTH parameters; the type system enforces lens/projection/budget compatibility through the shared Output and Budget. Mismatched triples (e.g., complexity-lens with SymbolicCost budget) are unrepresentable. Why projection rather than single-carrier: the lens output for complexity is rich (ComplexitySummary {work, span, asymptotic_class, certainty}) — required by §3.1 compose_summary_* composition. The budget is simple — the user's "function should be O(log n)" contract. Forcing budget = output over-constrains user authoring; forcing output = budget drops facts the composition needs. The projection separates the concerns. Updates: - §2: introduce LensEnforcement<Output, Budget>; SectionedLensApplication becomes parametric in (Output, Budget). Worked examples for all 4 lens enforcements added. - §3: ApplicationConfig<Budget> (was <C>); narrative updated to reference Output + Budget pair. - §6: Substrate Manager scope expanded to include LensEnforcement declarations. - §9 (NOT-modify list): per-lens budget types now declared via LensEnforcement, not via shared C. - §10 step 1: closure gate adds lens_enforcement_carrier_landed; substrate authoring includes per-lens LensEnforcement declarations. - design-r3-lens-substrate-index.md substrate-authority table: updated to list the 4 parametric carriers. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * WIP: Gunbc PM * WIP: Gunbc PM * docs(r3): split SectionedLensApplication into per-variant carriers + scrub stale QuantifiedTestClaim ref Two BLOCKINGs from codex on PR #1488 sha c6e61914: BLOCKING #1 (lens-application §2 lines 94 + 129): the previous shape SectionedLensApplication<Output, Budget> required EVERY application (including Introspect) to declare a Budget type and an enforcement projection. But §3 + line 129 said Introspect has "no projection or comparison" — leaving Introspect carrying enforcement metadata it cannot consume. P2 / illegal-states-unrepresentable: an Introspect application should not have enforcement axes. Resolution: split into two carriers + sum: - EnforcedApplication<Output, Budget> — carries lens, enforcement, section, budget, diagnostic_severity, span. Both type parameters relevant. - IntrospectApplication<Output> — carries only lens, section, span. No Budget axis, no enforcement projection. - SectionedLensApplication = Enforce<O,B>(EnforcedApplication<O,B>) | Introspect<O>(IntrospectApplication<O>) — sum where each variant carries exactly its required parameters. Now Introspect cannot accidentally carry enforcement state; mismatched triples (lens, projection, budget) remain unrepresentable for Enforce applications. Both illegal classes structurally rejected. BLOCKING #2 (cost-lens line 332): residual paragraph still said "The QuantifiedTestClaim runs..." asserting equivalence on asymptotic class only — contradicted line 312's "Rust cementing test today" + line 316's "full SymbolicCost/CostExpr structural equivalence" Band-C parity claim. Two incompatible closure-gate authorities in same section. Resolution: rewrote line 332 to align with Rust cementing + full SymbolicCost/CostExpr structural equivalence. Single authority restored. Also updated downstream references: - §3 narrative: ApplicationConfig sum-type declaration removed (folded into EnforcedApplication directly per §2). Pairing semantics still documented; the carrier shape is the single authority. - §3.2 ComplexityBudgetWaiver rationale: updated to "an Introspect application" instead of "SectionedLensApplication { config: Introspect }". - §4.1 worked example: substrate-after-parsing block now uses Enforce<ComplexitySummary, AsymptoticClass>(EnforcedApplication { ... }) with all coordinates explicit. - §5.1 default synthesis: synthesizer emits Introspect<ComplexitySummary>(IntrospectApplication { ... }). - §6 substrate-owner scope: 5 carriers now (was 4 before split). - §10 step 1: closure gates updated; substrate authoring includes per-variant carriers + per-lens LensEnforcement declarations. - master index substrate-authority table: row updated to reflect the carrier split. - r3-structure.md rows 40 + 148: lane-row carriers list updated to match the per-variant shape. P2 single-authority + illegal-states-unrepresentable preserved end-to-end. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * docs(r3): r3-structure default-policy text — sync with design-lens-application-surface §3.2 + §8.3 Cursor APPROVE_WITH_COMMENTS finding on PR #1488 sha 96899484: r3-structure.md lane-16 blurbs (lines 40 + 148) still said "opt-out (default check fires; explicit waiver...)" — matched the OLD default-enforcement story before my fix at e9d67113e which resolved the design to user-driven contracts (no implicit baseline; synthesized Introspect-only for unannotated functions). Parallel prose authority for the same decision violated P2 (single authoritative description) — r3-structure summary contradicted the canonical owning design doc. Fixed both occurrences to match the resolved framing: - Unannotated functions: synthesized Introspect-only. - Enforcement: requires explicit user authoring of apply_lens with Enforce + budget. - "Opt-out" reframed: user can opt out (no Enforce / explicit Introspect); compile errors fire when user opts IN with a budget the function exceeds. - ComplexityBudgetWaiver preserved purpose: accepting known violations of explicit user contracts. Single-authority restored; lane summary now points correctly at the canonical design doc resolution. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * docs(r3): LensEnforcement carries violation relation, not just projection Cursor BLOCKING on PR #1488 sha 96899484 line 74: LensEnforcement<Output, Budget> carried only `project: Output -> Budget`, leaving the fold-pass "budget exceeded" check without per-lens substrate authority for the violation relation. The check would have been API-level convention (the fold-pass hardcoding "use lattice ordering for AsymptoticClass / dominance for SymbolicCost / mode-mismatch for ParallelismMode" instead of reading declared facts). P2/P6 single-authority + API-level-enforcement violation. Resolution: extend LensEnforcement<Output, Budget> to carry both the projection AND the violation relation: ```dag type LensEnforcement<Output, Budget> { project: Output -> Budget violates: (declared: Budget, observed: Budget) -> Bool } ``` Each per-lens enforcement declares its own violation semantics structurally: - complexity_enforcement.violates: lattice ordering on AsymptoticClass - cost_enforcement.violates: dominance ordering on SymbolicCost (observed dominates declared) - parallelism_enforcement.violates: mode-mismatch (OptInIndependent declared but lens computed Sequential = violation) The fold-pass dispatch reads the per-lens violation relation directly (no hardcoded comparison logic in the fold-pass; the dispatch is fully substrate-driven). Updates: - §2 LensEnforcement carrier definition: extended with violates field + rationale. - §2 per-lens enforcement examples: each declares both project and violates. - §4.1 worked example "Compiler-side processing": fold-pass description reads enforcement.project then enforcement.violates. - §5 lens-fold integration step 2: dispatch reads project + violates. Per-lens substrate authority for violation relation restored. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * docs(r3): per-dimension certainty composition (work + span independent dominance) Cursor BLOCKING on PR #1488 sha 96899484 line 380: certainty_of_surviving derived certainty from composed_work only, but ComplexitySummary publishes BOTH work and span. Span has independent dominance from work (different inputs to iterate — span uses outer.work + body.span, while work uses outer.work + body.work). A conservative span contributor could be dropped from work's dominance walk while its span bound survived in span's dominance walk — the surviving span contributor's certainty would not enter the result's certainty. P1 modeling faithfulness + facts-flow- forward: certainty no longer faithful to the bound it qualifies on the span dimension. Resolution: per-dimension cost-aware certainty composition. Each dimension (work, span, future per-DB-3) computes its own surviving- contributor certainty independently; the result certainty is the meet across dimensions (any unproven dimension makes the whole result unproven). ```dag let work_cert = certainty_of_surviving_per_dim(outer, body, outer.work, body.work, composed_work) let span_cert = certainty_of_surviving_per_dim(outer, body, outer.work, body.span, composed_span) let composed_certainty = meet_pair(work_cert, span_cert) ``` certainty_of_surviving_per_dim is generalized to take per-dimension inputs (outer's contribution to this dimension, body's contribution, the composed dimension result) and walks dominance specifically on that dimension. Updates: - §3.1 compose_summary_iterate: per-dimension certainty composition with explicit work + span tracking. - §3.1 certainty_of_surviving renamed to certainty_of_surviving_per_dim; signature parameterized over dimension. - §3.1 compose_summary_sequential / compose_summary_branch comments updated to name the per-dimension pattern. - §1.5 (Why no BoundedLattice<Certainty>): updated to reference certainty_of_surviving_per_dim and per-dimension composition. Faithful certainty composition restored across all published dimensions. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * docs(r3): effect-enumeration — lens body MUST change to read inhabitance, not signature shape Cursor BLOCKING on PR #1488 sha 96899484 line 17: the doc moved effect KIND authority to algebra inhabitance (per §2.4 + §8.1) but the implementation plan asserted "the lens body does not change. callable_ arrow_effect already implements §2.4's rule" (line 373) + listed the lens fold body in the NOT-modify list (line 479) + size estimate said "lens-fold itself is unchanged" (line 494). But callable_arrow_effect TODAY derives effect kind from signature/body shape — if the body stays unchanged, it does NOT consume the new inhabits IdempotentRead<R> / inhabits Mutating<R> facts. Facts-flow-forward / P2 violation: new substrate authority not consumed by downstream. Resolution: the lens body MUST change in its kind-classification dispatch. Specifically: - The fold STRUCTURE (per-callable walk + report aggregation) is unchanged. - The per-callable kind classifier IS rewritten — from signature/body shape inference to algebra-inhabitance lookup (callable_inhabits(callable, idempotent_read_for(resource)) / callable_inhabits(callable, mutating_for(resource))). Updates: - §6.2 first reason: lens body framing flipped from "does not change" to "changes only in its kind-classification dispatch", with explicit rationale citing this BLOCKING. - §9 NOT-modify list: lens fold STRUCTURE preserved; per-callable kind classifier explicitly listed as modified (with cross-reference). - §9 size estimate: "lens-fold itself is unchanged" → "lens-fold structure is unchanged; per-callable kind classifier rewrite is S". - §10 implementation order: NEW step 5 ("Lens kind-classifier rewrite") inserted between OperationEffect retirement (step 4) and cementing test (now step 6). Total steps 6 → 7; steps-summary paragraph updated. Facts-flow-forward restored across the full migration: new inhabitance authority lands → lens classifier reads it → effect kind facts flow into ReadShaped / WriteShaped lens output. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * docs(r3): add lens_enforcement_carrier_landed to r3-structure lane gates gpt-5-5-pro REQUEST_CHANGES on PR #1488 sha 85a6bb0e (BLOCKING #3): design-lens-application-surface §10 step 1 declared lens_enforcement_ carrier_landed as a closure gate, but the r3-structure.md lane summary (lines 40 + 148) omitted it from the authoritative gate list. Per "tracked vs untracked debt" discipline: a named substrate carrier (LensEnforcement<Output, Budget>) without a tracked landing gate in the roadmap leaves new substrate work outside the closure-receipt mechanism. Resolution: add lens_enforcement_carrier_landed to both lane-summary gate lists (line 40 + line 148) with explanatory note that it covers the per-lens projection + violation-relation declarations co-located with each lens. (BLOCKINGs #1 + #2 from same review wave at sha 85a6bb0e are already addressed at e554f85e6 — LensEnforcement carries both project AND violates per-lens violation relation; substrate authority for budget-exceeded check is structural, not API-level.) Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * docs(r3): §8.5 implementation note — read EnforcedApplication.budget, not config.budget Codex BLOCKING on PR #1488 sha a525baf0: §8.5 still pointed implementers at `config.budget`, but the per-variant split at 968994843 dissolved ApplicationConfig — budget now lives on EnforcedApplication<Output, Budget> inside the Enforce variant of SectionedLensApplication. Stale implementation guidance pointing at non-existent authority. P2 violation. Fixed: §8.5 now describes the lens-fold matching on Enforce(EnforcedApplication { budget, ... }) and the Introspect case (no budget). Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * docs(r3): effect-enumeration lens body reads signature directly, not via LensEnforcement Cursor BLOCKING on PR #1488 sha c41b8ce8 line 373: my §6.2 fix said the new effect_enumeration lens body "reads enforcement.project for the effect set". But LensEnforcement is the lens-application-surface budget-projection carrier (T-Lens-Application-Surface lane). The effect-enumeration lens body is part of T-Lens-Behavioral-Parity slice 4 — which CASCADES into T-Lens-Application-Surface (the latter gates on the former being COMPLETE). Reading enforcement.project from the lens body inverts the cascade AND gives the effect-set fact a second authority (signature-derived per §2.4(a) vs LensEnforcement projection). Resolution: lens body reads effect set DIRECTLY from the callable's arrow signature (existing substrate query — resource types in input ∩ output, per §2.4(a)). Kind classification reads callable_inhabits(...) per §2.4(b). Both queries are within T-Lens-Behavioral-Parity slice 4 scope; neither depends on LensEnforcement. Updated §6.2 line 373 to: - Replace "reads enforcement.project for the effect set" with "reads the effect set directly from the callable's arrow signature (existing substrate query; structurally derivable per §2.4(a) without any lens-application-surface artifact)". - Add explicit "neither depends on LensEnforcement from T-Lens- Application-Surface (cascade flows the other direction)". Cascade direction preserved: T-Lens-Behavioral-Parity COMPLETE → T-Lens-Application-Surface, not vice versa. Effect-set fact has single authority (signature query); kind fact has single authority (algebra inhabitance). No lens-application carriers consumed by lens body. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * WIP: Gunbc PM * docs(r3): per-coordinate certainty on ComplexitySummary (no global collapse) Codex BLOCKING on PR #1488 sha 75a6ab57: §3.1 computed independent work_cert and span_cert per-dimension, then immediately collapsed them into one global ComplexitySummary.certainty via meet_pair. That collapse loses the per-dimension proof-tightness fact: if work is Proven but span is Conservative (or vice versa), downstream display/enforcement consumers see only "globally Conservative" and cannot know the work bound was proven. P1 modeling faithfulness + P2 facts-flow-forward violation: the certainty fact each dimension carries gets fused into ambiguity. Resolution: ComplexitySummary now carries per-coordinate certainty — work_certainty and span_certainty as independent fields. No global certainty field; no meet across dimensions. Each coordinate's certainty stays on that coordinate through composition. ```dag type ComplexitySummary { work: SymbolicCost span: SymbolicCost asymptotic_class: AsymptoticClass work_certainty: Certainty // per-coordinate per BLOCKING fix span_certainty: Certainty } ``` Updates: - §1.7 ComplexitySummary declaration: split certainty into work_certainty + span_certainty with explicit rationale citing this BLOCKING. - §3 ComplexitySummary declaration in lens body section: same split. - §3 outer Loop construction: outer.span = outer.work, so both certainties = bound_cert. - §3.1 compose_summary_iterate: drop the global meet across dimensions; work_certainty := work_cert, span_certainty := span_cert independently. - §3.1 certainty_of_surviving_per_dim signature: takes per-dimension certainty inputs (outer_cert, body_cert) explicitly; no global outer.certainty / body.certainty lookup. - §3.1 compose_summary_sequential / compose_summary_branch comments: pattern updated to "no meet across dimensions; per-coordinate independence preserved on output". asymptotic_class is still a projection of work; its certainty is work_certainty (no separate class_certainty since the class is derived, not independent). All facts faithful to the dimension they qualify. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * docs(r3): align lens-application doc with per-coordinate certainty (work_certainty / span_certainty) Cursor APPROVE_WITH_COMMENTS finding on PR #1488 sha 37f3bc62: lens- application-surface lines 125 + 152 still described ComplexitySummary with a single `certainty` field, but my fix at 955cafe2c split certainty into per-coordinate work_certainty + span_certainty in the complexity- lens design. Sibling-doc mismatch — same carrier shape described two ways across two design docs in the same PR. Updated lines 125 + 152 to match complexity-lens §1.7's per-coordinate shape: - Line 125 inline comment: "rich output: work/span/asymptotic_class/ work_certainty/span_certainty". - Line 152 narrative: "rich (ComplexitySummary { work, span, asymptotic_class, work_certainty, span_certainty } — per complexity- lens §1.7, certainty is per-coordinate to avoid collapsing per- dimension proof-tightness facts)". - "Forcing output = budget would drop work/span/certainty facts" → "drop work/span/per-coordinate-certainty facts". Cross-doc carrier-shape consistency restored. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * WIP: Gunbc PM * docs(r3): codex BLOCKINGs #1-3 (sha 37f3bc62) — substrate assumptions aligned with v3 reality 3 BLOCKINGs at sha 37f3bc62, all claiming docs lock substrate assumptions v3 cannot currently express: BLOCKING #1 (cost-lens SizeVariable label): doc said renderer reads via intern_table::name_of(port_id). Verified: src/v3/std/algebra.dag:143 explicitly says "InternTable lookup the lens doesn't yet run". v3 has some InternTable machinery (PR #367 Phase 1) but the port-id-to-name query is NOT landed. Cannot assume it. Resolution: re-introduce SizeVariable.display_name: String? as the single substrate authority for the user-facing name. No InternTable lookup assumed. Field is single-source (not parallel with anything); parser populates from authored binding names where present, None for inferred. Earlier "parallel authority" concern (gpt-5-5-pro at ef21e1a0) doesn't apply because there's no second source — InternTable lookup isn't landed and isn't claimed. BLOCKING #2 (per-variant generics): doc declared SectionedLensApplication = Enforce<Output, Budget>(...) | Introspect< Output>(...) — but v3 .dag sums use uniform type parameters across variants (e.g., Lookup<C> = Miss | Hit(C); both share C). Per-variant parameter binding / existential packaging not currently supported. Resolution: drop the SectionedLensApplication SUM. Use TWO SEPARATE top-level carriers — EnforcedApplication<Output, Budget> and IntrospectApplication<Output>. Lens-fold pass walks two separate lists and emits Diagnostics from Enforce walks, records values from Introspect walks. No per-variant generics required. Each lens application in .dag source is one or the other; user authoring chooses at apply_lens site. BLOCKING #3 (TestPredicate maturity): doc said "Today's TestPredicate coproduct covers 22 variants" listed by name, treating them as uniformly-live substrate. Per verification.dag inline annotations, many are 🟡 Scaffold with named dissolution triggers (ExecuteCommand, ForAllTargets, LensOutputEquals, DifferentialEquals, BinaryDimensionReportEquals, AlgebraicLaw, ReleaseDeferredClaim, SubstrateResearchDeferredClaim). Resolution: §1 explicitly disclose 🟢 TERMINAL vs 🟡 Scaffold partition; note that ports landing on Scaffold variants are inherently scoped by that variant's named dissolution trigger; new-carrier residual is in scope of T-Tests-As-Data-Completeness, not assumed live. Updates: - design-cost-lens §1.2: SizeVariable.display_name reintroduced as single authority; revert §1.4 from renderer-only to additive field; both wave reviews now reconciled. - design-lens-application-surface §2: SectionedLensApplication sum removed; two top-level carriers (EnforcedApplication + IntrospectApplication). Downstream §3 + §4 + §5 + §6 + §8.5 + §9 + §10 references updated to "two separate top-level carriers" framing. - design-tests-as-data §1: TestPredicate maturity disclosure (TERMINAL vs Scaffold partition with named dissolution triggers per verification.dag inline annotations). - design-r3-lens-substrate-index: substrate-authority table updated to drop "sum" and list two separate carriers. All three BLOCKINGs reflect the constraint: design docs cannot assume substrate facilities not yet landed, and cannot use shapes v3 cannot currently express. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * docs(r3): cementing test asserts per-coordinate certainty (work + span), not collapsed Codex BLOCKING on PR #1488 sha e3010014: §1.7 changed ComplexitySummary to per-coordinate work_certainty + span_certainty (closing the global- collapse bug at PR #1488 / 955cafe2c), but §4.1 cementing test still asserted a single global v3.certainty. Internally inconsistent: closure gate would not validate the per-coordinate claim §1.7 makes; the test would either pass on a v3 that secretl…
…+ EnforceableLens uniqueness (#1500) * docs(roadmap): fold 2026-05-01 paired exploratory + reflective analyses Director relayed two analyses against current main: - Exploratory (gpt-5-5-pro main@8cd5359): 9 findings against dsl/std/*.dag, src/v2/tests/src/*.rs, dsl/extdeps/, THESIS, INVARIANTS, MODELING, ROADMAP — 2 novel correctness bugs (SymbolicCost semiring violation, emitter expect() panic paths), 3 sharpened tracked items (SubValueRelation lattice-law contradiction, ?? / % syntax-parser drift, CollectionOps/StringOps/ MapOps duplicates), 4 already-tracked items - Reflective (gpt-5-5-pro main@6ea9812 → now): 5 cross-PR patterns + 6 highest-priority course corrections + verdict "advancing, scaffold-velocity dominates" PM ingestion folds into single ROADMAP debt section per Director's prior 2026-04-30 analyses ingestion pattern (PR #1319). Sections: - A: Exploratory novel correctness bugs (SymbolicCost product-zero bug, SubValueRelation BoundedLattice claim violation, emitter expect panic paths) - B: Exploratory sharpened tracked items (?? / % drift, CollectionOps/StringOps/MapOps duplicates) - C: Exploratory already-tracked confirmations (no new ROADMAP rows) - D: Reflective 5 cross-PR patterns (author-now/fire-later, test_ runner.rs second predicate language, typed-carrier-Rust-mirror accumulation, numeric philosophy mid-window shift validating T-Numeric-Construction reframe, bridge retirement tracked-not- retired) - E: Reflective 6 highest-priority course corrections with owner attribution + lane connection table - F: CI cost signal (e765c86a 60min timeout) + velocity-tripwire calibration (64 docs / 16 feat / 9 fix ratio) - G: PM strategic synthesis: 3 cross-cutting meta-themes (algebraic-law-witness coverage gap; "make scaffolds executable" cluster; "tighten existing structural enforcement" cluster) Per-finding/correction owner attribution names R3 Substrate Mgr, R3 Verification Mgr, R3 Grounding Mgr, R3 PB Mgr per ownership boundaries. Lane connections cite T-V-L4-L7-Direct, T-Free- Consequences-Demonstration, T-Ground-Services parser-grammar slice, T-Numeric-Construction Slice 2 sequencing, etc. Highest-value novel: SymbolicCost product-zero bug (cost-lens reads incorrect facts; iterate(ConstantCost(0), ...) returns body cost instead of zero) + emitter expect() panics. Highest-value sharpened-tracked: SubValueRelation BoundedLattice false-claim. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * WIP: Gunbc PM * docs(r3): R3 scope expansion 12 → 16 lanes + standing R3 Debt-Paydown program Per Director ratification 2026-05-02 at gunbc#828 comment 4362742638: User directive: per the strict reading of "nothing deferred past R3", all "accidentally deferred" gaps absorb into R3. Plus three additional asks: behavioral expectations docs per feature; compile-error complexity ratchet generalized as lens-application-surface (per user reframe); in-cycle debt-paydown discipline. NEW R3 LANES (4 added; lane count 12 → 16): 13. T-E-P-Producer-Broadening (Substrate; M-L; foundational) - broaden per-call DescentEvidence/CallPattern/SubValueRelation from first slice to full ExprCall.descent_evidence parity - prerequisite for T-Lens-Behavioral-Parity 14. T-Lens-Behavioral-Parity (Substrate + Verification cross-program; L-XL) - 4 sub-slices: complexity / cost / parallelism / effect_enumeration - bring lens-capability-register from PROXY/STUB/PARTIAL → COMPLETE - includes symbolic CostExpr full algebra; work/span split; asymptotic classification; cementing test against v2 oracle; Stage 2e parallelism walk port; resource-threading migration 15. T-Tests-As-Data-Completeness (Verification; L) - tests-as-data full coverage (thesis facet 3) - property-based testing surface (ForAll/Exists quantifiers + ProgramGenerator carrier) - cementing test discipline for .dag lenses 16. T-Lens-Application-Surface (Substrate + Verification; L-XL) - per user reframe: lens application as first-class authoring surface - apply_lens(lens, section, config) where config.violation_policy = CompileError | Warning | Silent - subsumes prior T-Complexity-Contract-Compile-Error + T-User-Authored-Cost-Basis-Discipline as configurations - 4 worked examples: complexity-contract-compile-error + CRDT cost basis + memory-peak cost basis + opt-in cross-iteration parallelism - default policy for complexity contract: opt-out NEW STANDING PROGRAM: R3 Debt-Paydown Manager (9th standing R3 Mgr) - hybrid mechanism: per-PR debt-receipt rule + standing capacity - closure gate: r3_debt_paydown_zero_remaining - per feedback_standing_managers_need_owned_deliverables FOLD-INS (3; no new lanes): - T-V-L4-L7-Direct: per-(algebra, inhabitant, law) exhaustive witness coverage (catches SymbolicCost product-zero bug class structurally) - T-Ground-Diagnostic: closed-axis enforcement (no String dispatch on closed sets); replaces MissingEmissionPath { connective: String, ... } - T-LensProducer-Retirement: ownership d/e/f confirmed delivered (not separately deferred) T-Behavioral-Expectations-Documentation (parallel-dispatchable; 7 load- bearing features per Director ratification): lens framework + 4 lens instances + complexity contract + cross-target consistency. Updates to docs/r3-structure.md: - §Summary: 12 lanes + 1 standing program → 16 lanes + 1 standing program - §Lane structure: 4 new rows - §Manager structure: 8 → 9 standing managers; 3 → 4 modifications - NEW §Standing program — R3 Debt-Paydown section authored - T-Numeric-Construction lane row updated to 13 types in scope (was 8; per 2026-05-02 PM audit + Substrate Mgr ack) R3 scope ratchet: ~58% (over current 12-lane denominator) → ~38% (over expanded 17-lane denominator); numerator unchanged. Honest timeline projection: R3 close in 5-8 weeks at current velocity. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * docs(r3): T-Numeric-Construction row — 8-type → 13-type scope citation + traceability Director callout on PR #1480: §Summary item 6 says 13 types in scope but §Lane structure table row 138 still said 8. Internal inconsistency. Fix: §Lane structure table row 138 updated to 13 types in scope, with explicit citation chain: - original 8-type count from PR #1430 §A audit - extended to 13 after fresh PM sweep found 5 additional Int-inherited refinement types (RetryCount / HttpStatus / Port / PositiveInt / NonNegativeInt) at dsl/std/types.dag:232-245 - Substrate Mgr ack at gunbc#1130 comment 4360482400 Includes: Nat-alignment opportunity flagged (NonNegativeInt → Nat, PositiveInt → Nat where range(min: 1)), cost-lens candidates for bounded-range types (RetryCount → Nat<3>, HttpStatus → Nat<10>, Port → Nat<16>) once refinement composition lands. Per Director recommendation: brief addendum documenting the audit so lane scope stays anchored. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * docs(r3): address PR #1480 cursor findings — §P5 mix-up + restored locked dispositions Fixes 3 cursor findings on PR #1480 (sha 0f32605d) plus 1 exploratory: 1. §P5(b)/(c) mix-up (line 44): "vague deferrals rejected" attributes to §P5(b) per-PR gate (the rule that actually rejects vague deferrals), not §P5(c) Velocity tripwire (windowed dispatch-pause). Now also explicitly surfaces §P5(c) as separate (b) windowed-enforcement clause. 2. Restored Post-R2 emergent work disposition on Substrate/PB continuation bullet (line 187): Director-locked 2026-04-28 — emergent post-R2 work absorbs into Substrate Manager continuation, not new managers. 3. Restored Verification scope negations on Verification Manager bullet (line 189): "L6 NOT in Verification scope" + "T-CostLens-Composition NOT in Verification scope" — both Director-locked 2026-04-28. 4. Updated stale "9 of 12" / "3 non-gated" counts in §"Dependency on R2" (lines 393, 397, 399, 400, 402) to "11 of 16" / "5 non-gated" matching line 59 Summary; added T-Lens-Behavioral-Parity + T-Lens-Application-Surface to Evaluator-gated list with cascade gate note. All Director-locked 2026-04-28 dispositions tagged "carried forward through 2026-05-02 expansion" so the locks survive the lane-count change. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * docs(r3): close P5 escape hatch in r3_debt_paydown_zero_remaining gate Cursor BLOCKING finding on PR #1480 at docs/r3-structure.md:173: gate contradicted itself by allowing "deferred-to-post-R3 with Director sign-off" after stating "no tracked-debt rows survive R3 close", weakening P5/strict- forward-progress into a disposition convention. Fix: remove the deferral escape hatch entirely. Gate is unconditional — every tracked-debt row retires with PR receipt before R3 close. Grounds in user directive 2026-05-02: "all 'accidentally deferred to post R3' into R3 now". If a row appears unretirable, it surfaces as a substrate gap requiring a named R3 lane (the directive that motivated this manager's creation), not a Director-sign-off deferral. Cites INVARIANTS §P5 directly: tracked-debt deferred past R3 close is the bridge-as-steady-state pattern P5 explicitly forbids; the escape hatch reintroduced that pattern at lower cadence. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * WIP: Gunbc PM * docs(r3): reconcile T-Tests-As-Data-Completeness Evaluator-gating contradiction gpt-5-5-pro REQUEST_CHANGES finding on PR #1480 (sha 0f32605d): line 59 summary said T-Tests-As-Data-Completeness is in the "5 self-contained non-Evaluator-gated" group, but lane table at line 147 lists its dependency as "R2-Evaluator (test execution runtime)". Schedulers got two incompatible authorities (P2 single-authority violation). Lane table is correct — porting Rust tests to .dag TestClaim requires the Evaluator to execute the resulting test artifacts. Updated: - Line 59 summary: 11 → 12 Evaluator-gated; 5 → 4 non-gated; T-Tests-As- Data-Completeness moved into Evaluator-gated list with reason - Line 393 (Dependency on R2): same reclassification - Line 395 (substrate-carrier-fed list): drop T-Tests-As-Data-Completeness - Line 399 (precondition applies-to list): 11 → 12 lanes - Line 400 (carve-out): 5 → 4 lanes; drop T-Tests-As-Data-Completeness - Line 402 (split-resolution sentence): 11 → 12, 5 → 4 (Findings #2 and #3 already addressed at 0c449a869 and 0de2bda06 respectively.) Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * docs(r3): T-Lens-Application-Surface design doc — substrate shape + 4 worked examples Per user directive 2026-05-02 ("all designs upfront, implementation sketches if needed, minimize escalations"), authoring foundational design doc that unblocks T-Lens-Application-Surface lane dispatch. Resolves design questions: 1. **Section reference shape**: `SectionRef = DeclarationScope { DeclarationId } | NodeScope { DeclarationId, NodeId }`. Three of four user-named scopes (function / module / declaration) use DeclarationId uniformly; expression scope is the exception (NodeId required because expressions live inside Declaration body sub-DAGs). 2. **Violation-policy semantics**: user-named `CompileError | Warning | Silent` resolved to fail-closed-compatible binary `Enforce | Introspect` per INVARIANTS C-8. Warning forbidden (allows violations as steady state, bridge pattern P5 forbids); Silent forbidden ("silent None" exactly the pattern feedback_fail_closed_discipline bans). 3. **Default complexity-contract policy**: opt-out (compiler enforces; explicit waiver required). Waiver shape is structural `ComplexityBudgetWaiver` declaration with `justification` field, NOT an annotation per feedback_no_annotations. 4. **4 worked examples** ratified by Director (complexity-contract / CRDT cost / memory-peak cost / opt-in parallelism) — each grounded in substrate carriers + lens-fold integration. 5. **5 open design questions** flagged for Director ratification before substrate authoring begins (module-level semantics, multiple-applications- per-section, budget-inference for default, waiver dissolution, cross-section composition). Updates r3-structure.md lane 16 row to reference the design doc, replace the @complexity_budget_waived annotation language with structural carrier name, and replace the original `CompileError | Warning | Silent` enum with the fail-closed-resolved Enforce/Introspect binary. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * docs(r3): resolve all 5 §8 open design questions in-doc per minimize-escalations directive Per user directive 2026-05-02 ("minimize escalations"), resolved the 5 open design questions that were flagged for Director ratification: §8.1 — Module-level semantics: aggregate-across-module (preserves structural distinction between module-scope and per-function-scope). §8.2 — Multiple applications: fail-closed reject duplicate (lens, section) Enforce-mode pairs; multiple Introspect admitted (idempotent). §8.3 — Default-application budget: regression-detection class, gated on T-Lens-Behavioral-Parity COMPLETE; pre-cascade Introspect-only. §8.4 — Waiver lifecycle: future lens_stale_waivers lens with named dissolution trigger; tracked in lens-library-design.md §6. §8.5 — Cross-section composition: read declared budget, not computed class (preserves abstraction barrier; cost-of-change=1). Each resolution carries explicit reasoning grounded in INVARIANTS P2/P5 + feedback memory. Implementation can proceed once cascade gates clear (T-Lens-Behavioral-Parity COMPLETE for §8.3 flip; R2-Evaluator landed for worker dispatch precondition). No further Director ratification needed on these specific points. r3-structure.md row 16 updated to reflect the design-doc resolution. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * WIP: Gunbc PM * docs(r3): cross-design coherence pass + master design index Coherence audit across the 5 design docs identified 5 cross-doc conflicts; this commit resolves all 5 and lands the master index linking them. Fixes: 1. **Producer-query single-authority** (P2): complexity-lens §2 + cost-lens §3.2 now both reference `per_call_pattern_at(d, call_site) -> CallPattern?` as the typed query surface (single authority); the underlying `per_call_descent_evidence` side-table is named as the storage backend only. Eliminates parallel-authority risk. 2. **Cementing-test shape unified** (DB-15): cost-lens §5 reshaped from custom `ForAll { p: SourceProgram in programs }` (which violated tests- as-data §2.5 — quantifiers belong on claims, not predicates) to `QuantifiedTestClaim { generator, quantifier: ForAll, predicate: DifferentialEquals }`. Now matches complexity-lens §4 and tests-as-data §2.2 shape. 3. **DB-18 element-type-refinement cross-reference**: effect-enumeration §4.1 now explicitly states that DB-18's STOP-AND-ESCALATE locks the `WorkflowEffect` variant set + variant payload shape, not element-type within `LinearEffect.ops: List<X>`. The `OperationEffect` → `Operation` retypes is additive tightening within DB-18's permitted refinement scope. 4. **Resource-threaded signature compatibility**: cost-lens §3.3 now explicitly notes that `per_call_pattern_at` reads from threaded arrow signatures (per effect-enumeration §2.4) — signature-shape-agnostic producer; broadening covers both pre-migration and post-migration signature shapes. 5. **TestClaim shape for lens-application demonstrations**: lens-application §4 now declares all 4 worked-example closure gates use `TestClaim` (DB-15 enumerated form), not `QuantifiedTestClaim`. Property tests over the lens-application substrate live in T-Tests-As-Data scope, not T-Lens-Application-Surface scope. 6. **Register-migration sequencing**: tests-as-data §8.3 now lists the 4 sibling lens design docs whose register-row "→ COMPLETE" closure steps depend on the markdown→.dag migration landing first (substrate work in sibling lanes does NOT depend; only the closure-gate row update does). Plus: NEW `docs/design-r3-lens-substrate-index.md` — master index linking all 5 design docs, documenting cross-doc edges (substrate authority single-points + cementing-test format + cross-cutting invariants), and naming lane dispatch order. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * docs(r3): address 4 cursor findings on PR #1480 (sha 16340c52) 1. **Lane 16 row 40 stale text vs row 148 resolved** (P2 single-authority): row 40 still carried the original `CompileError | Warning | Silent` enum + `@complexity_budget_waived` annotation language; row 148 had the resolved `ViolationPolicy = Enforce | Introspect` + structural `ComplexityBudgetWaiver` carrier. Updated row 40 to match the resolved story (single authority). 2. **Line 44 duplicate (b) and (c) labels**: the Hybrid mechanism outer enumeration used (a)/(b)/(c) but referenced INVARIANTS §P5 sub- mechanisms (a)/(b)/(c) inside; same letter labels at different levels confused parsing. Renamed outer enumeration to (1)/(2)/(3) with footnote explaining the distinction. 3. **Line 175 contradicts line 173** (P5): line 175 said "Does enforce: tracked-debt rows get retirement PRs or explicit deferral" — the "or explicit deferral" reads like deferral remains an outcome, contradicting line 173's unconditional "no post-R3 deferral path". Removed the deferral language; line 175 now restates the unconditional rule + names the substrate-gap escalation path. 4. **design-complexity-lens-behavioral-completeness.md:125-127 variant- count mismatch** (P1 self-faithfulness): comment said "closed seven-variant set" / "Adding an eighth variant" but `AsymptoticClass` enumerates 8 variants (ClassConstant/Log/Linear/Linearithmic/ Quadratic/Polynomial/Exponential/Unknown). Updated comment to "eight-variant" / "ninth". Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * docs(r3): retract cost-lens parallel SizeExpr proposal — align with complexity-lens single authority Cursor BLOCKING finding on PR #1480: cost-lens proposed a new SizeExpr 5-variant coproduct as authority, while complexity-lens proposed SizeVariable.display_name enrichment for the same SymbolicCost payloads. P2/P5 violation — same substrate fact, two incompatible target shapes. Resolution: complexity-lens has the structurally correct framing. - DB-7's SymbolicCost is the unified algebra (locked). - SymbolicCost already covers SizeAdd (via SumCost) and SizeMax (via dominance ordering) — no parallel SizeExpr algebra needed. - Descent semantics like "n - 1" live in std.computation::CallPattern (the canonical E-C site), not in size expressions. A SizeShrink variant would duplicate that fact in parallel. - Asymptotically O(n - 1) ≡ O(n); descent is a call-site property, not a size-shape property. Aligned cost-lens to complexity-lens: SizeVariable gains an optional display_name: String? field; no parallel SizeExpr carrier; SymbolicCost DB-7 lock preserved unchanged. Updated: - §1.1 problem framing — drop "size arithmetic" / "aggregate sizes" framing (already covered by SymbolicCost); keep only the "named-binding semantics" gap that motivates display_name. - §1.2 target shape — SizeVariable.display_name: String? (matches complexity-lens §1.2 verbatim). - §1.3 explicit rationale for unified-algebra over parallel-SizeExpr. - §1.4 migration shape — additive field, no carrier rename, no deletion. - §3 / §5 code examples — replaced SizePort with SizeVariable shape. - §8.1 resolved-question reframe — names the rejected alternative (parallel SizeExpr) for future readers. - §8.2 names-on-carrier resolution — display_name shape per §1.2. - §10 implementation step 1 closure gate renamed size_expr_substrate_landed → sizevariable_displayname_landed. P2 single-authority restored across the 5-doc design surface. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * docs(r3): effect-enumeration — read/write distinction via algebra inhabitance, not signature shape Cursor BLOCKING finding on PR #1480 at design-effect-enumeration-resource- threading.md:151: the design's "structural recognition" claim was actually convention-level. \`R in / R out\` and \`R in / R' out\` (same type, different value) have the SAME typed signature — \`.dag\` doesn't encode value- preservation as a substrate fact. ReadShaped vs WriteShaped via signature shape alone was P1 modeling-faithfulness violation. Resolution: split the unified rule into two structural carriers per §2.4: (a) Effect SET — derived from signature: resource types in input ∩ output. Structural; the signature carries it. (b) Effect KIND — declared via algebra inhabitance on the callable: \`inhabits IdempotentRead<R>\` (read), \`inhabits Mutating<R>\` (write), \`inhabits Append<R>\` (append). Structural; the inhabitance carrier captures it. The lens consults BOTH — signature for set, inhabitance for kind. Absence of any kind inhabitance with the resource in the effect set is a fail- closed Diagnostic (EffectKindUndeclared), not a silent default. Updates: - §2.1 line 151: replace "same-value vs modified" framing with explicit effect-set-vs-effect-kind distinction; cross-link to §2.4 + §8.1. - §2.3: same fix for Network read example. - §2.4: split the unified rule into (a) effect SET (signature) + (b) effect KIND (algebra inhabitance) with pseudocode for the lens-side classification. - §4.3: update EffectShape derivation source from "signature shape" to "algebra inhabitance lookup". - §8.1: full reframe — from "same-value resolved" to "algebra inhabitance is the structural authority", with explicit rationale (per-callable authority, not per-call; rejected phantom-marker alternative per feedback_no_annotations). - §3 lens fold pseudocode: dispatch on §2.4(a) for set + §2.4(b) for kind. Preserves the existing EffectShape = IsIdempotent | IsBreaking partition (per design-composed-effect-reshape.md PR #529 R3) — only the source of the shape changes (declared inhabitance, not derived from signature). P1 modeling-faithfulness restored. Cursor finding fully resolved. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * docs(r3): lens-application — collapse ApplicationConfig into sum-type, illegal states unrepresentable Cursor BLOCKING finding on PR #1480 at design-lens-application-surface.md:43: ApplicationConfig was a record with budget: LensBudget? + violation_policy: ViolationPolicy as separate fields. This admitted illegal state combinations: - Enforce + budget=None (illegal: enforcement requires a budget) - Introspect + budget=Some(_) (illegal: introspection takes no budget) The doc explicitly noted these as type-checker-enforced invariants (lines 136-137), but per feedback_state_space_vs_behavioral_invariants those are behavioral invariants, not state-space invariants — exactly the bug pattern modeling-discipline principles 2/6 prohibit. Illegal states must be unrepresentable at the type level. Resolution: collapse ApplicationConfig and ViolationPolicy into a single sum-type that pairs budget with Enforce by construction: ```dag type ApplicationConfig = Enforce { budget: LensBudget, diagnostic_severity: DiagnosticSeverity } | Introspect ``` By construction: - Enforce ALWAYS has a budget (it's a coordinate of the variant). - Introspect NEVER has a budget (it has no payload). The "Enforce without budget" and "Introspect with budget" combinations cannot be constructed; the type-checker has no rejection rule to enforce them — they don't exist in the state space. Updates: - §2: replaced ApplicationConfig record + ViolationPolicy sum with single ApplicationConfig sum carrying budget inside Enforce variant. - §3: rewrote framing to match — the binary Enforce/Introspect is the ApplicationConfig sum itself; budget pairing is structural. - §4: all 4 worked-example syntaxes updated to `Enforce { budget, diagnostic_severity }` directly (no separate violation_policy field). - §5.1: synthesized default-application uses `Enforce { budget: <inferred>, diagnostic_severity: Error }` shape. - §3.2: explicit-introspection override syntax `apply_lens(complexity, fn, Introspect)` (no separate budget=None). - r3-structure.md rows 40 + 148: updated substrate-carrier description to name ApplicationConfig as sum-type with the structural-invariance note. Modeling principles 2/6 honored. P1 modeling-faithfulness restored. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * docs(r3): codex non-blocking findings #2 + #3 — heading/count consistency Codex review on PR #1480 sha 58f49e91 noted two non-blocking inconsistencies: NB2: design-cost-lens-sizevar-dimension-wiring.md §4.2 heading said 'CommutativeSemiring<SymbolicCost>' but §8.5 resolves to 'Semiring<SymbolicCost>' (multiplicative side does NOT enforce commutativity per §8.5 reasoning). Fixed §4.2 heading to match §8.5 resolution. NB3: design-tests-as-data-completeness.md §3.1 said 'six classes' / 'decomposes into six structural classes' but §10 step 3 enumerates C1-C7 (seven classes). Fixed §3.1 to say 'seven classes' with explicit C1-C7 cross-reference. Both load-bearing for doc-as-authority discipline (P1 modeling-faithfulness of the spec to itself). (All 4 BLOCKING findings from same review at sha 58f49e91 are already addressed at earlier commits — see PR comment for the receipts: ef21e1a00 / 92d9b11cf / 255cca3cb / 8640e6701.) Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * docs(r3): fix line 199 active-surface arithmetic + line 23 exploratory clarity Cursor APPROVE_WITH_COMMENTS finding on PR #1480 sha 92d9b11c: **Main finding (line 199)**: arithmetic was internally inconsistent — "expanded from 13 active surfaces" + "4 new lanes + 1 new standing program" = 18, not 17. The baseline should have been 12 (12 lanes + 0 standing programs at the 2026-04-30 lock), making 12 + 5 = 17 consistent. Fixed by restating the baseline as 12 with explicit arithmetic: 4 new lanes (enumerated by name) + 1 new standing program = +5; 12 + 5 = 17. Also pinned T-Behavioral-Expectations-Documentation explicitly as "parallel-dispatchable across existing lanes, not a separate surface" so readers don't double-count it as a 5th new lane. **Exploratory finding (line 23)**: the "added..." list mixed 4 new lanes + T-Behavioral-Expectations-Documentation (not a separate lane) + standing program in one breath. Restructured the parenthetical to enumerate the 4 new lanes by name and call out T-Behavioral-Expectations-Documentation as parallel-dispatchable explicitly. Reader can no longer mis-count. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * docs(r3): drop SizeVariable.display_name; InternTable single-authority for size names gpt-5-5-pro REQUEST_CHANGES on PR #1480 sha ef21e1a0 — BLOCKING #3 + #4: BLOCKING #3: SizeVariable.display_name + intern_table::name_of(source_port) created TWO authorities for the user-facing size-variable name. The §8.2 implementation note confirmed the parallel: "when display_name = Some(name), renderer uses it directly; when None, falls back to InternTable lookup". P2 single-authority violation; consumers could diverge on the same source_port. BLOCKING #4: master index design-r3-lens-substrate-index.md still claimed SizeExpr replaces SizeVariable, but cost-lens design (post-ef21e1a00) had already retracted SizeExpr in favor of unified SymbolicCost. Cross-doc authority drift. Resolution (both BLOCKINGs): - Drop display_name field entirely from cost-lens + complexity-lens designs. - SizeVariable substrate stays UNCHANGED at { source_port: PortId }. - InternTable is the single canonical name authority — already populated at parse time keyed by port_id. Renderer reads via intern_table::name_of(source_port). - The "Named SizeVar" gap from the capability register is closed by renderer-side wiring (no substrate change), not by adding a field. - Master index updated: SizeVariable line replaces the old SizeExpr line; notes InternTable as name authority. Updates: - design-cost-lens §1.2: target shape removes display_name field from SizeVariable carrier; rationale rewritten as InternTable-as-single-authority. - design-cost-lens §1.4 / §3 / §5 / §8.1 / §8.2: all display_name references scrubbed; "renderer-side InternTable name wiring" replaces "SizeVariable. display_name enrichment" throughout. - design-cost-lens §10 step 1: closure gate renamed sizevariable_displayname_landed -> renderer_intern_table_name_wiring_landed. - design-complexity-lens §1.2: same rewrite — SizeVariable carrier UNCHANGED; InternTable as name authority; explicit cross-link to cost-lens §1.2. - design-complexity-lens §7.2: resolved-question reframe. - design-r3-lens-substrate-index.md: SizeVariable line replaces SizeExpr line with InternTable-name-authority note. P2 single-authority restored. Cross-doc consistency restored. (BLOCKING #1 + #2 from same review at sha ef21e1a0 are already addressed at earlier commits — see PR comment for receipts: 92d9b11cf + 255cca3cb.) Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * docs(r3): codex review wave (sha 98f2fc4f) — 4 BLOCKING + 2 NB findings addressed BLOCKING #1: lens-application config not parametric in C — lens/budget pair relied on type-checker convention rather than structural typing. Fix: SectionedLensApplication<C> + ApplicationConfig<C> parametric in the lens carrier C; lens: Lens<C> and config.budget: C share the same C structurally. Mismatch is unrepresentable, not type-checker-rejected. Per-lens budgets dissolve into the existing Lens<C> carrier — no separate ComplexityBudget/CostBudget/ParallelismBudget carriers needed. BLOCKING #2: complexity-lens Certainty composed independently from cost dominance. Fix: define joint compose_summary function (§3.1) where certainty composition is cost-aware — when dominance drops a cost component, that component's certainty does NOT enter the result. Surfaces v2's implicit Θ(n²) Proven semantics; cost-unaware certainty would diverge from v2 on the cementing fixture corpus. BLOCKING #3: effect-enumeration line 17 prose still claimed signature is "one structural authority" for effects. Fix: updated to name the two orthogonal authorities — signature for effect SET, algebra inhabitance for effect KIND. Aligned with §2.4 + §8.1 that I'd already fixed at 92d9b11cf. BLOCKING #4: sibling lens docs and tests-as-data didn't share one cementing closure shape — complexity + effect proposed Rust cementing tests, cost (after my earlier fix at ef21e1a00) proposed QuantifiedTestClaim. Inconsistency. Fix: align all three on **Rust cementing today + dissolution trigger to tests-as-data step 5 .dag port**. Per-lens divergence is now explicitly forbidden in the master index. NB1: cost-lens §1.4 still said "single field addition" / "Rust mirror single field add" after the InternTable fix removed the field add. Cleaned up to "renderer-only, no substrate change". NB2: tests-as-data §3 said "17 variants" but enumerated 22 (Compiles ... BridgeLedgerZero). Fixed count to 22. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * docs(r3): scrub residual non-parametric LensBudget references Cursor BLOCKING at sha 98f2fc4f line 102 — incomplete fix for parametric SectionedLensApplication<C> migration at 812f6a141. Three lines still referenced the old non-parametric framing: - Line 100: "type-checker verifies b inhabits lens.budget_type" — type-checker convention rather than structural typing. - Line 114: ApplicationConfig redeclared without <C> parameter. - Line 262: substrate-owner mention of "per-lens budget_type declaration extension". - Line 351: "each lens owns its own LensBudget definition" — implied separate budget carriers. - Line 357: implementation step said "Lens<C>.budget_type field added". All updated to reflect the parametric resolution (per §2): - ApplicationConfig<C> parametric in lens carrier C; lens/budget pair is structural via shared C. - Mismatch is unrepresentable, NOT type-checker-rejected. - No budget_type field on Lens<C>; the parameter C IS the structural authority. - Each lens's existing Lens<C> carrier IS the budget type; no new per-lens budget carriers. References to "budget_type" / "LensBudget" remain only in negation form ("not via budget_type field", "no LensBudget definition") to document the rejected alternative for future readers. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * docs(r3): lens-application — dissolve regression_baseline_pinned optional field Cursor BLOCKING at sha 98f2fc4f line 323 (actually line 308 — drift after prior edits): regression_baseline_pinned: AsymptoticClass? was an optional field on SectionedLensApplication where absence = introspection mode and presence = enforcement mode. This re-creates EXACTLY the illegal-states-representable pattern that the §2 ApplicationConfig sum-type fix dissolved (the original finding at design-lens-application- surface.md:43 from a prior wave). Fix: dissolve the optional field. The cascade-flip (T-Lens-Behavioral- Parity COMPLETE flipping default complexity from Introspect to Enforce) is purely SYNTHESIZER-side, not substrate-side: - Pre-cascade: synthesizer emits `Introspect` for every default complexity application. - Post-cascade: synthesizer emits `Enforce { budget: <computed class>, diagnostic_severity: Error }` — the computed class IS the regression baseline; the variant choice carries the fact structurally. No optional field on the carrier. The cascade just changes which variant the synthesizer constructs. Same illegal-states-unrepresentable discipline as §2. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * docs(r3): drop certainty_lattice — Certainty composition is cost-aware, not lattice-fold Cursor BLOCKING at sha 98f2fc4f line 196: join_certainty's "Proven wins under alternative" semantic was P1 unfaithful — a Proven branch arm could hide a Conservative arm carrying the actual worst-case bound, so the result's certainty would no longer faithfully describe the bound it qualifies. Same cost-unaware pattern as the §3.1 BLOCKING from earlier in the wave (composition independent from cost dominance). Resolution: drop the BoundedLattice<Certainty> declaration entirely. Certainty does NOT compose via lattice meet/join; composition is cost-aware per §3.1 compose_summary_* family. The lattice declaration was misleading — it suggested an independent composition pattern that contradicts the cost-aware design. Updates: - §1.5: removed `data certainty_lattice` declaration + meet_certainty + join_certainty function bodies. Replaced with prose explaining cost-aware composition + tightness-ordering distinction (ordering is implicit when projecting; not a composition operation). - §3.1: meet_certainty(...) call → meet_pair(...) inline helper, with explicit comment that it's used ONLY when both contributions survive cost composition (NOT a free-standing lattice op). - §11 cascade-gate list: removed "data certainty_lattice" from the class-5-grammar dependent declarations list with explanatory note. Same illegal-states-unrepresentable + cost-aware-composition discipline preserved end-to-end across the §3.1 + §1.5 + §3.x compose_summary_* chain. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * docs(r3): effect-enumeration §8.4 — derive readonly deletion from algebra inhabitance, not signature shape Cursor BLOCKING at sha 98f2fc4f line 442: §8.4 "readonly keyword deletion" rationale said the keyword is "structurally derivable: an operation is read-shaped iff every threaded resource appears unchanged in input and output." This contradicts §2.4's locked rule that effect KIND is declared only via algebra inhabitance (inhabits IdempotentRead<R>), NOT derived from signature shape — same modeling-discipline violation as the line 151 BLOCKING from the prior wave (cursor BLOCKING #2 of this codex-wave). Resolution: rewrite §8.4 to derive readonly's deletion rationale from algebra inhabitance, not signature shape: - After migration, read kind is declared via `inhabits IdempotentRead<R>` on the callable (per §2.4 + §8.1) — structural fact. - The `readonly` keyword duplicates that inhabitance: same fact, two carriers. P2 single-authority + feedback_no_annotations forbid this. - Keyword is redundant AND drift-prone (feedback_state_space_vs_ behavioral_invariants: keyword could disagree with inhabitance). - Implementation-mechanical: every operation currently using `readonly` already has a corresponding `inhabits IdempotentRead<R>` declared at the migration site (one-to-one mapping in the atomic PR per §6). The §2.4 → §8.1 → §8.4 chain is now consistent end-to-end: signature carries effect SET; algebra inhabitance carries effect KIND; the readonly annotation is the same parallel-authority bug pattern P5/P2 forbid. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * docs(r3): fix tests-as-data dissolution-trigger cross-reference §10 → §6 Cursor APPROVE_WITH_COMMENTS finding on PR #1488 (sha 95b54f54): all 4 docs cross-referencing the cementing-dispatch-port dissolution trigger pointed at "tests-as-data §10 step 5", but tests-as-data has no §10 — the implementation-order list (containing step 5 = cementing dispatch port) is at §6. Fixed in 4 places: - docs/design-r3-lens-substrate-index.md:39 - docs/design-complexity-lens-behavioral-completeness.md:425 - docs/design-cost-lens-sizevar-dimension-wiring.md:314 - docs/design-effect-enumeration-resource-threading.md:489 Per INVARIANTS "Documentation Describes Live State" — readers can now resolve the cited anchor. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * docs(r3): cost-lens cementing — tighten Band-C parity claim to full SymbolicCost/CostExpr carrier gpt-5-5-pro APPROVE_WITH_COMMENTS finding on PR #1488 sha fa5f1675: line 316 said "asserting structural equivalence on the asymptotic class" which could weaken the Band-C parity assertion if read literally — the asymptotic class is a projection of SymbolicCost, not the full carrier. Tightened to commit to the stronger claim: cementing asserts structural equivalence on the FULL SymbolicCost/CostExpr carrier shape (not a projection). Asymptotic-class equivalence is a downstream consequence, not a substitute. Aligns with the structural_equivalent() function shape already declared at line 318. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * docs(r3): remove implicit Enforce-with-inferred-baseline; align Certainty no-lattice references Codex BLOCKING on PR #1488 sha 265d8ef7: §8.3 + §3.2 + §5.1 said the default complexity application post-cascade flips to Enforce mode with "budget = computed asymptotic class at synthesis time" — but the synthesizer recomputes from the current body each compile, so the baseline moves with the body. Whatever class the function has becomes both "current" and "baseline"; they always agree; no regression ever fires. The fact the design claimed to enforce was lost on every recompile. P2 single-authority + facts-flow-forward violation. Resolution: remove the implicit Enforce mode entirely. Default is Introspect-only for unannotated functions; user explicitly authors Enforce { budget: <chosen class>, ... } to opt into enforcement. No auto-inferred baseline — those would need persisted authority (either generated source, forbidden by feedback_no_generated_code_on_disk, or sidecar files, same problem). The structural answer: complexity contracts are user-authored. Re-framing "opt-out for complexity" per the original user directive: the user can opt out (by not authoring an Enforce application or by authoring Introspect); compile errors fire when the user opts IN with a budget the actual function exceeds. ComplexityBudgetWaiver retains its purpose — accepting known violations of explicit user contracts. Codex NB: residual references to "Certainty + lattice declaration" / "two new lattice instances" in complexity-lens lines 535 + 579 didn't match the §1.5 lattice deletion. Updated both to single BoundedLattice<AsymptoticClass> instance + Certainty 2-variant sum WITHOUT lattice (composition is cost-aware via §3.1 compose_summary_*). Updates: - §3.2 (Default policy): full reframe to user-driven contracts. - §5.1 (Default-application synthesis): synthesizer never emits Enforce; only Introspect for unannotated functions. - §8.3 (Default-application semantics): RESOLVED with new framing — user-driven contracts; no implicit baseline; explicit rationale for why generated-source is not the answer. - complexity-lens §5 step 2 + §7.4: drop "Certainty + lattice declaration" and "BoundedLattice<Certainty>" from the substrate-landing list and ROADMAP-P2 dissolution accounting. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * WIP: Gunbc PM * docs(r3): lens-application — add LensEnforcement<Output, Budget> projection carrier Codex BLOCKING on PR #1488 sha 265d8ef7 line 100: tying ApplicationConfig<C> to the same C as Lens<C> made the complexity lens budget = AsymptoticClass, but the complexity-lens design publishes Lookup<ComplexitySummary> with work/span/certainty as the lens output. Either drop downstream facts (force output = AsymptoticClass) or contradict the lens-output contract (output = ComplexitySummary; budget = AsymptoticClass; type system can't enforce compatibility). P1 modeling faithfulness + facts-flow-forward violation. Resolution: introduce LensEnforcement<Output, Budget> projection carrier in §2. Each lens declares both: - Lens<Output> for the read function (rich output type — load-bearing for lens-fold composition per compose_summary_*) - LensEnforcement<Output, Budget> for the projection from Output to the budget-comparable type (identity for cost; summary.asymptotic_class for complexity) SectionedLensApplication<Output, Budget> is parametric in BOTH parameters; the type system enforces lens/projection/budget compatibility through the shared Output and Budget. Mismatched triples (e.g., complexity-lens with SymbolicCost budget) are unrepresentable. Why projection rather than single-carrier: the lens output for complexity is rich (ComplexitySummary {work, span, asymptotic_class, certainty}) — required by §3.1 compose_summary_* composition. The budget is simple — the user's "function should be O(log n)" contract. Forcing budget = output over-constrains user authoring; forcing output = budget drops facts the composition needs. The projection separates the concerns. Updates: - §2: introduce LensEnforcement<Output, Budget>; SectionedLensApplication becomes parametric in (Output, Budget). Worked examples for all 4 lens enforcements added. - §3: ApplicationConfig<Budget> (was <C>); narrative updated to reference Output + Budget pair. - §6: Substrate Manager scope expanded to include LensEnforcement declarations. - §9 (NOT-modify list): per-lens budget types now declared via LensEnforcement, not via shared C. - §10 step 1: closure gate adds lens_enforcement_carrier_landed; substrate authoring includes per-lens LensEnforcement declarations. - design-r3-lens-substrate-index.md substrate-authority table: updated to list the 4 parametric carriers. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * WIP: Gunbc PM * WIP: Gunbc PM * docs(r3): split SectionedLensApplication into per-variant carriers + scrub stale QuantifiedTestClaim ref Two BLOCKINGs from codex on PR #1488 sha c6e61914: BLOCKING #1 (lens-application §2 lines 94 + 129): the previous shape SectionedLensApplication<Output, Budget> required EVERY application (including Introspect) to declare a Budget type and an enforcement projection. But §3 + line 129 said Introspect has "no projection or comparison" — leaving Introspect carrying enforcement metadata it cannot consume. P2 / illegal-states-unrepresentable: an Introspect application should not have enforcement axes. Resolution: split into two carriers + sum: - EnforcedApplication<Output, Budget> — carries lens, enforcement, section, budget, diagnostic_severity, span. Both type parameters relevant. - IntrospectApplication<Output> — carries only lens, section, span. No Budget axis, no enforcement projection. - SectionedLensApplication = Enforce<O,B>(EnforcedApplication<O,B>) | Introspect<O>(IntrospectApplication<O>) — sum where each variant carries exactly its required parameters. Now Introspect cannot accidentally carry enforcement state; mismatched triples (lens, projection, budget) remain unrepresentable for Enforce applications. Both illegal classes structurally rejected. BLOCKING #2 (cost-lens line 332): residual paragraph still said "The QuantifiedTestClaim runs..." asserting equivalence on asymptotic class only — contradicted line 312's "Rust cementing test today" + line 316's "full SymbolicCost/CostExpr structural equivalence" Band-C parity claim. Two incompatible closure-gate authorities in same section. Resolution: rewrote line 332 to align with Rust cementing + full SymbolicCost/CostExpr structural equivalence. Single authority restored. Also updated downstream references: - §3 narrative: ApplicationConfig sum-type declaration removed (folded into EnforcedApplication directly per §2). Pairing semantics still documented; the carrier shape is the single authority. - §3.2 ComplexityBudgetWaiver rationale: updated to "an Introspect application" instead of "SectionedLensApplication { config: Introspect }". - §4.1 worked example: substrate-after-parsing block now uses Enforce<ComplexitySummary, AsymptoticClass>(EnforcedApplication { ... }) with all coordinates explicit. - §5.1 default synthesis: synthesizer emits Introspect<ComplexitySummary>(IntrospectApplication { ... }). - §6 substrate-owner scope: 5 carriers now (was 4 before split). - §10 step 1: closure gates updated; substrate authoring includes per-variant carriers + per-lens LensEnforcement declarations. - master index substrate-authority table: row updated to reflect the carrier split. - r3-structure.md rows 40 + 148: lane-row carriers list updated to match the per-variant shape. P2 single-authority + illegal-states-unrepresentable preserved end-to-end. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * docs(r3): r3-structure default-policy text — sync with design-lens-application-surface §3.2 + §8.3 Cursor APPROVE_WITH_COMMENTS finding on PR #1488 sha 96899484: r3-structure.md lane-16 blurbs (lines 40 + 148) still said "opt-out (default check fires; explicit waiver...)" — matched the OLD default-enforcement story before my fix at e9d67113e which resolved the design to user-driven contracts (no implicit baseline; synthesized Introspect-only for unannotated functions). Parallel prose authority for the same decision violated P2 (single authoritative description) — r3-structure summary contradicted the canonical owning design doc. Fixed both occurrences to match the resolved framing: - Unannotated functions: synthesized Introspect-only. - Enforcement: requires explicit user authoring of apply_lens with Enforce + budget. - "Opt-out" reframed: user can opt out (no Enforce / explicit Introspect); compile errors fire when user opts IN with a budget the function exceeds. - ComplexityBudgetWaiver preserved purpose: accepting known violations of explicit user contracts. Single-authority restored; lane summary now points correctly at the canonical design doc resolution. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * docs(r3): LensEnforcement carries violation relation, not just projection Cursor BLOCKING on PR #1488 sha 96899484 line 74: LensEnforcement<Output, Budget> carried only `project: Output -> Budget`, leaving the fold-pass "budget exceeded" check without per-lens substrate authority for the violation relation. The check would have been API-level convention (the fold-pass hardcoding "use lattice ordering for AsymptoticClass / dominance for SymbolicCost / mode-mismatch for ParallelismMode" instead of reading declared facts). P2/P6 single-authority + API-level-enforcement violation. Resolution: extend LensEnforcement<Output, Budget> to carry both the projection AND the violation relation: ```dag type LensEnforcement<Output, Budget> { project: Output -> Budget violates: (declared: Budget, observed: Budget) -> Bool } ``` Each per-lens enforcement declares its own violation semantics structurally: - complexity_enforcement.violates: lattice ordering on AsymptoticClass - cost_enforcement.violates: dominance ordering on SymbolicCost (observed dominates declared) - parallelism_enforcement.violates: mode-mismatch (OptInIndependent declared but lens computed Sequential = violation) The fold-pass dispatch reads the per-lens violation relation directly (no hardcoded comparison logic in the fold-pass; the dispatch is fully substrate-driven). Updates: - §2 LensEnforcement carrier definition: extended with violates field + rationale. - §2 per-lens enforcement examples: each declares both project and violates. - §4.1 worked example "Compiler-side processing": fold-pass description reads enforcement.project then enforcement.violates. - §5 lens-fold integration step 2: dispatch reads project + violates. Per-lens substrate authority for violation relation restored. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * docs(r3): per-dimension certainty composition (work + span independent dominance) Cursor BLOCKING on PR #1488 sha 96899484 line 380: certainty_of_surviving derived certainty from composed_work only, but ComplexitySummary publishes BOTH work and span. Span has independent dominance from work (different inputs to iterate — span uses outer.work + body.span, while work uses outer.work + body.work). A conservative span contributor could be dropped from work's dominance walk while its span bound survived in span's dominance walk — the surviving span contributor's certainty would not enter the result's certainty. P1 modeling faithfulness + facts-flow- forward: certainty no longer faithful to the bound it qualifies on the span dimension. Resolution: per-dimension cost-aware certainty composition. Each dimension (work, span, future per-DB-3) computes its own surviving- contributor certainty independently; the result certainty is the meet across dimensions (any unproven dimension makes the whole result unproven). ```dag let work_cert = certainty_of_surviving_per_dim(outer, body, outer.work, body.work, composed_work) let span_cert = certainty_of_surviving_per_dim(outer, body, outer.work, body.span, composed_span) let composed_certainty = meet_pair(work_cert, span_cert) ``` certainty_of_surviving_per_dim is generalized to take per-dimension inputs (outer's contribution to this dimension, body's contribution, the composed dimension result) and walks dominance specifically on that dimension. Updates: - §3.1 compose_summary_iterate: per-dimension certainty composition with explicit work + span tracking. - §3.1 certainty_of_surviving renamed to certainty_of_surviving_per_dim; signature parameterized over dimension. - §3.1 compose_summary_sequential / compose_summary_branch comments updated to name the per-dimension pattern. - §1.5 (Why no BoundedLattice<Certainty>): updated to reference certainty_of_surviving_per_dim and per-dimension composition. Faithful certainty composition restored across all published dimensions. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * docs(r3): effect-enumeration — lens body MUST change to read inhabitance, not signature shape Cursor BLOCKING on PR #1488 sha 96899484 line 17: the doc moved effect KIND authority to algebra inhabitance (per §2.4 + §8.1) but the implementation plan asserted "the lens body does not change. callable_ arrow_effect already implements §2.4's rule" (line 373) + listed the lens fold body in the NOT-modify list (line 479) + size estimate said "lens-fold itself is unchanged" (line 494). But callable_arrow_effect TODAY derives effect kind from signature/body shape — if the body stays unchanged, it does NOT consume the new inhabits IdempotentRead<R> / inhabits Mutating<R> facts. Facts-flow-forward / P2 violation: new substrate authority not consumed by downstream. Resolution: the lens body MUST change in its kind-classification dispatch. Specifically: - The fold STRUCTURE (per-callable walk + report aggregation) is unchanged. - The per-callable kind classifier IS rewritten — from signature/body shape inference to algebra-inhabitance lookup (callable_inhabits(callable, idempotent_read_for(resource)) / callable_inhabits(callable, mutating_for(resource))). Updates: - §6.2 first reason: lens body framing flipped from "does not change" to "changes only in its kind-classification dispatch", with explicit rationale citing this BLOCKING. - §9 NOT-modify list: lens fold STRUCTURE preserved; per-callable kind classifier explicitly listed as modified (with cross-reference). - §9 size estimate: "lens-fold itself is unchanged" → "lens-fold structure is unchanged; per-callable kind classifier rewrite is S". - §10 implementation order: NEW step 5 ("Lens kind-classifier rewrite") inserted between OperationEffect retirement (step 4) and cementing test (now step 6). Total steps 6 → 7; steps-summary paragraph updated. Facts-flow-forward restored across the full migration: new inhabitance authority lands → lens classifier reads it → effect kind facts flow into ReadShaped / WriteShaped lens output. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * docs(r3): add lens_enforcement_carrier_landed to r3-structure lane gates gpt-5-5-pro REQUEST_CHANGES on PR #1488 sha 85a6bb0e (BLOCKING #3): design-lens-application-surface §10 step 1 declared lens_enforcement_ carrier_landed as a closure gate, but the r3-structure.md lane summary (lines 40 + 148) omitted it from the authoritative gate list. Per "tracked vs untracked debt" discipline: a named substrate carrier (LensEnforcement<Output, Budget>) without a tracked landing gate in the roadmap leaves new substrate work outside the closure-receipt mechanism. Resolution: add lens_enforcement_carrier_landed to both lane-summary gate lists (line 40 + line 148) with explanatory note that it covers the per-lens projection + violation-relation declarations co-located with each lens. (BLOCKINGs #1 + #2 from same review wave at sha 85a6bb0e are already addressed at e554f85e6 — LensEnforcement carries both project AND violates per-lens violation relation; substrate authority for budget-exceeded check is structural, not API-level.) Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * docs(r3): §8.5 implementation note — read EnforcedApplication.budget, not config.budget Codex BLOCKING on PR #1488 sha a525baf0: §8.5 still pointed implementers at `config.budget`, but the per-variant split at 968994843 dissolved ApplicationConfig — budget now lives on EnforcedApplication<Output, Budget> inside the Enforce variant of SectionedLensApplication. Stale implementation guidance pointing at non-existent authority. P2 violation. Fixed: §8.5 now describes the lens-fold matching on Enforce(EnforcedApplication { budget, ... }) and the Introspect case (no budget). Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * docs(r3): effect-enumeration lens body reads signature directly, not via LensEnforcement Cursor BLOCKING on PR #1488 sha c41b8ce8 line 373: my §6.2 fix said the new effect_enumeration lens body "reads enforcement.project for the effect set". But LensEnforcement is the lens-application-surface budget-projection carrier (T-Lens-Application-Surface lane). The effect-enumeration lens body is part of T-Lens-Behavioral-Parity slice 4 — which CASCADES into T-Lens-Application-Surface (the latter gates on the former being COMPLETE). Reading enforcement.project from the lens body inverts the cascade AND gives the effect-set fact a second authority (signature-derived per §2.4(a) vs LensEnforcement projection). Resolution: lens body reads effect set DIRECTLY from the callable's arrow signature (existing substrate query — resource types in input ∩ output, per §2.4(a)). Kind classification reads callable_inhabits(...) per §2.4(b). Both queries are within T-Lens-Behavioral-Parity slice 4 scope; neither depends on LensEnforcement. Updated §6.2 line 373 to: - Replace "reads enforcement.project for the effect set" with "reads the effect set directly from the callable's arrow signature (existing substrate query; structurally derivable per §2.4(a) without any lens-application-surface artifact)". - Add explicit "neither depends on LensEnforcement from T-Lens- Application-Surface (cascade flows the other direction)". Cascade direction preserved: T-Lens-Behavioral-Parity COMPLETE → T-Lens-Application-Surface, not vice versa. Effect-set fact has single authority (signature query); kind fact has single authority (algebra inhabitance). No lens-application carriers consumed by lens body. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * WIP: Gunbc PM * docs(r3): per-coordinate certainty on ComplexitySummary (no global collapse) Codex BLOCKING on PR #1488 sha 75a6ab57: §3.1 computed independent work_cert and span_cert per-dimension, then immediately collapsed them into one global ComplexitySummary.certainty via meet_pair. That collapse loses the per-dimension proof-tightness fact: if work is Proven but span is Conservative (or vice versa), downstream display/enforcement consumers see only "globally Conservative" and cannot know the work bound was proven. P1 modeling faithfulness + P2 facts-flow-forward violation: the certainty fact each dimension carries gets fused into ambiguity. Resolution: ComplexitySummary now carries per-coordinate certainty — work_certainty and span_certainty as independent fields. No global certainty field; no meet across dimensions. Each coordinate's certainty stays on that coordinate through composition. ```dag type ComplexitySummary { work: SymbolicCost span: SymbolicCost asymptotic_class: AsymptoticClass work_certainty: Certainty // per-coordinate per BLOCKING fix span_certainty: Certainty } ``` Updates: - §1.7 ComplexitySummary declaration: split certainty into work_certainty + span_certainty with explicit rationale citing this BLOCKING. - §3 ComplexitySummary declaration in lens body section: same split. - §3 outer Loop construction: outer.span = outer.work, so both certainties = bound_cert. - §3.1 compose_summary_iterate: drop the global meet across dimensions; work_certainty := work_cert, span_certainty := span_cert independently. - §3.1 certainty_of_surviving_per_dim signature: takes per-dimension certainty inputs (outer_cert, body_cert) explicitly; no global outer.certainty / body.certainty lookup. - §3.1 compose_summary_sequential / compose_summary_branch comments: pattern updated to "no meet across dimensions; per-coordinate independence preserved on output". asymptotic_class is still a projection of work; its certainty is work_certainty (no separate class_certainty since the class is derived, not independent). All facts faithful to the dimension they qualify. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * docs(r3): align lens-application doc with per-coordinate certainty (work_certainty / span_certainty) Cursor APPROVE_WITH_COMMENTS finding on PR #1488 sha 37f3bc62: lens- application-surface lines 125 + 152 still described ComplexitySummary with a single `certainty` field, but my fix at 955cafe2c split certainty into per-coordinate work_certainty + span_certainty in the complexity- lens design. Sibling-doc mismatch — same carrier shape described two ways across two design docs in the same PR. Updated lines 125 + 152 to match complexity-lens §1.7's per-coordinate shape: - Line 125 inline comment: "rich output: work/span/asymptotic_class/ work_certainty/span_certainty". - Line 152 narrative: "rich (ComplexitySummary { work, span, asymptotic_class, work_certainty, span_certainty } — per complexity- lens §1.7, certainty is per-coordinate to avoid collapsing per- dimension proof-tightness facts)". - "Forcing output = budget would drop work/span/certainty facts" → "drop work/span/per-coordinate-certainty facts". Cross-doc carrier-shape consistency restored. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * WIP: Gunbc PM * docs(r3): codex BLOCKINGs #1-3 (sha 37f3bc62) — substrate assumptions aligned with v3 reality 3 BLOCKINGs at sha 37f3bc62, all claiming docs lock substrate assumptions v3 cannot currently express: BLOCKING #1 (cost-lens SizeVariable label): doc said renderer reads via intern_table::name_of(port_id). Verified: src/v3/std/algebra.dag:143 explicitly says "InternTable lookup the lens doesn't yet run". v3 has some InternTable machinery (PR #367 Phase 1) but the port-id-to-name query is NOT landed. Cannot assume it. Resolution: re-introduce SizeVariable.display_name: String? as the single substrate authority for the user-facing name. No InternTable lookup assumed. Field is single-source (not parallel with anything); parser populates from authored binding names where present, None for inferred. Earlier "parallel authority" concern (gpt-5-5-pro at ef21e1a0) doesn't apply because there's no second source — InternTable lookup isn't landed and isn't claimed. BLOCKING #2 (per-variant generics): doc declared SectionedLensApplication = Enforce<Output, Budget>(...) | Introspect< Output>(...) — but v3 .dag sums use uniform type parameters across variants (e.g., Lookup<C> = Miss | Hit(C); both share C). Per-variant parameter binding / existential packaging not currently supported. Resolution: drop the SectionedLensApplication SUM. Use TWO SEPARATE top-level carriers — EnforcedApplication<Output, Budget> and IntrospectApplication<Output>. Lens-fold pass walks two separate lists and emits Diagnostics from Enforce walks, records values from Introspect walks. No per-variant generics required. Each lens application in .dag source is one or the other; user authoring chooses at apply_lens site. BLOCKING #3 (TestPredicate maturity): doc said "Today's TestPredicate coproduct covers 22 variants" listed by name, treating them as uniformly-live substrate. Per verification.dag inline annotations, many are 🟡 Scaffold with named dissolution triggers (ExecuteCommand, ForAllTargets, LensOutputEquals, DifferentialEquals, BinaryDimensionReportEquals, AlgebraicLaw, ReleaseDeferredClaim, SubstrateResearchDeferredClaim). Resolution: §1 explicitly disclose 🟢 TERMINAL vs 🟡 Scaffold partition; note that ports landing on Scaffold variants are inherently scoped by that variant's named dissolution trigger; new-carrier residual is in scope of T-Tests-As-Data-Completeness, not assumed live. Updates: - design-cost-lens §1.2: SizeVariable.display_name reintroduced as single authority; revert §1.4 from renderer-only to additive field; both wave reviews now reconciled. - design-lens-application-surface §2: SectionedLensApplication sum removed; two top-level carriers (EnforcedApplication + IntrospectApplication). Downstream §3 + §4 + §5 + §6 + §8.5 + §9 + §10 references updated to "two separate top-level carriers" framing. - design-tests-as-data §1: TestPredicate maturity disclosure (TERMINAL vs Scaffold partition with named dissolution triggers per verification.dag inline annotations). - design-r3-lens-substrate-index: substrate-authority table updated to drop "sum" and list two separate carriers. All three BLOCKINGs reflect the constraint: design docs cannot assume substrate facilities not yet landed, and cannot use shapes v3 cannot currently express. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * docs(r3): cementing test asserts per-coordinate certainty (work + span), not collapsed Codex BLOCKING on PR #1488 sha e3010014: §1.7 changed ComplexitySummary to per-coordinate work_certainty + span_certainty (closing the global- collapse bug at PR #1488 / 955cafe2c), but §4.1 cementing test still asserted a single global v3.certainty. Internally inconsistent: closure gate would not validate the per-coordinate claim §1.7 makes; the test would…
Opened from session-dashboard for session
warm-newt-750.