feat(v3): gate #92 T-LAS complexity enforcement compile error

[briansrls]

Codex @ 444316f0 (2026-05-09) — verified

• Strengths match 444316f08: complexity.dag stays on the honest T-LAS surface (read / compose / branch / iterate / enforcement); enforced_lens_application.rs still fail-closes unresolved section, budget decode, and complexity_of Miss with ParseError diagnostics.
• ROADMAP receipt complexity_violation_compile_error_demonstrated is still covered by t_las_complexity_contract_compile_error_test + fixture.

No code change required for this item (non-blocking, no findings).

Merge readiness (re-check)

Check	Status
CI (fmt, ci, v3)	Pass on latest run for 444316f08
mergeStateStatus	CLEAN; mergeable
≥2× Verdict: APPROVE (distinct api-review, grep PR comments)	Not found — gh api issue comments: no Verdict: APPROVE; PR reviews list is COMMENTED only (including this codex pass)
gh pr merge	Not run — branch protection / relay bar (“≥2 APPROVE”) not satisfied from automation

Escalation: If policy allows merge on green CI + CLEAN without formal Verdict: APPROVE lines, a human needs to approve in GitHub or adjust the gate; I can’t fabricate review state.

— sent from still-ibex-188 (for dashboard parity where a thread comment is expected)

---

  

[briansrls]

Review metadata

• Provider / model: codex / unknown
• Commit: 9e4bb808 · Trigger: schedule
• Thinking: 426s wall

---

BLOCKING (1)

Root Cause

• src/v3/compiler/src/enforced_lens_application.rs enforcement semantics live in a host-side complexity special case instead of the declared LensEnforcement.project/violates functions → make the .dag enforcement relation truthful and consume it, or land the bridge with a bounded named dissolution trigger.

⚠️ The compile-error path works as a demonstration, but the new canonical enforcement carrier currently says no violation is possible.

[briansrls]

Review metadata

• Provider / model: codex / unknown
• Commit: 54463c75 · Trigger: schedule
• Thinking: 322s wall

---

BLOCKING (1)

Root Cause

• src/v3/compiler/src/complexity_lattice.rs hand-written host mirror of asymptotic_dominates erases PositiveDescentAmount degree → generate/consume the .dag relation or compare polynomial degrees structurally.

ROADMAP — Incomplete

• complexity_violation_compile_error_demonstrated: The ClassLog witness is present, but the landed enforcement relation is not yet faithful for polynomial budgets.

⚠️ One substrate-relevant budget fact is dropped in the enforcement bridge.

[briansrls]

Review metadata

• Provider / model: openai-pro / gpt-5-5-pro
• Commit: 0fc70c32 · Trigger: manual
• Comparison: main @ 15cf2d31 ... cursor/t-las-complexity-compile-error-b113 @ 6fdc3f10
• Conversation: View conversation

---

1. Story of the diff

This PR turns T-LAS gate #92 from a declared acceptance row into an executable compile-time receipt. When a user module imports lenses.complexity, compile_to_dag now prepends src/v3/lenses/complexity.dag before lowering the user module (src/v3/compiler/src/lib.rs:4494-4498, src/v3/compiler/src/lower.rs:183-193), then infer invokes a new enforcement pass (src/v3/compiler/src/infer.rs:278-279). That pass scans EnforcedApplication<ComplexitySummary, AsymptoticClass> data, resolves the declared DeclarationScope, computes the section’s complexity via complexity_of, and emits a compile diagnostic if the generated complexity_enforcement_violates relation says the observed class exceeds the budget (src/v3/compiler/src/enforced_lens_application.rs:140-164).

The PR also adds Rust support needed for that path to compile: a generated lens_cost export for complexity_enforcement_project / complexity_enforcement_violates (src/v3/compiler/src/lens_cost_generated.rs:506-519), a hand Rust asymptotic comparison bridge (src/v3/compiler/src/complexity_lattice.rs:11-69), Rust target instantiations for Witness, Lens, Monoid, LensEnforcement, and EnforceableLens (src/v3/spec/rust.dag:1304-1337), and a new regression fixture/test proving an over-budget recursive witness fails compilation (src/v3/compiler/tests/fixtures/t_las_complexity_contract_demo.dag:14-23, src/v3/compiler/tests/integration/t_las_complexity_contract_compile_error_test.rs:16-42). The generated bootstrap files are regenerated to account for the changed .dag surface.

2. Invariant categories

1. LAYER MODEL — Finding

BLOCKING — substrate-facing Lens is now published with fabricated behavior. The diff introduces data complexity_lens: Lens<ComplexitySummary> and wires it to functions that do not perform the complexity analysis they claim to model: complexity_lens_read_stub returns Inhabits(zero_summary()) for every Dag/Behavior (src/v3/lenses/complexity.dag:418-419), complexity_lens_validate_stub always returns NoDiagnostic (src/v3/lenses/complexity.dag:424-425), and the published Lens record uses those stubs as its read / validate fields (src/v3/lenses/complexity.dag:444-450). Meanwhile the actual enforcement consumer bypasses the Lens record and calls complexity_of(dag, &port) directly (src/v3/compiler/src/enforced_lens_application.rs:140-141). Since lenses are substrate declarations, this makes the declared substrate object untruthful and creates a second authority for the analysis behavior.

2. INVARIANTS.md + modeling-discipline.md — Finding

BLOCKING — fail-closed / modeling faithfulness violation. Witness<ComplexitySummary> is a success carrier, but complexity_lens_read_stub fabricates success with Inhabits(zero_summary()) regardless of the input behavior (src/v3/lenses/complexity.dag:418-419). That is not a typed failure, an unknown, or a bounded placeholder; it is a plausible successful complexity summary that downstream lens consumers could treat as real. The same issue appears in validation: complexity_lens_validate_stub always reports NoDiagnostic (src/v3/lenses/complexity.dag:424-425). The PR’s compile-error path may be fail-closed, but the newly published Lens surface itself is not.

3. CODING.md — Finding

NON-BLOCKING but should be fixed with this PR — build dependency declaration regressed. The build script comment still says Cargo must rerun when any staged std/spec/compiler file changes because otherwise bootstrap can silently miss additions (src/v3/compiler/build.rs:362-364), but the PR deletes the std_dir rerun declaration (src/v3/compiler/build.rs:365). Since this PR also changes src/v3/std/algebra.dag, removing the std directory watch makes the bootstrap dependency less explicit and risks stale generated bootstrap state for future std changes or new std files.

4. TESTING.md — Compliant

The gate-level regression is correctly behavior-driven: the new fixture declares a concrete over-budget EnforcedApplication (src/v3/compiler/tests/fixtures/t_las_complexity_contract_demo.dag:17-23), and the integration test asserts compile_to_dag fails with a semantic DAG containing a ParseError whose message identifies the lens enforcement violation (src/v3/compiler/tests/integration/t_las_complexity_contract_compile_error_test.rs:26-42). That is the right level for “compile error demonstrated.”

5. LOCKED DESIGN DECISIONS — N/A

N/A — the diff updates the R3 plan receipt row (docs/r3-program-plan.md:290) but does not itself alter a file or paragraph marked LOCKED.

6. TRACKED vs UNTRACKED DEBT — Finding

BLOCKING — the new scaffold is documented, but not bounded to dissolution. The diff explicitly calls the new complexity lens a nominal carrier rather than the behavioral implementation: “complexity_lens is a nominal Lens<ComplexitySummary> carrier” and “the behavioral fold remains complexity_of / compute_summaries” (src/v3/lenses/complexity.dag:397-399). It then lands multiple *_stub functions (src/v3/lenses/complexity.dag:418-431) and removes the old stop-ratchet assertion that data complexity_lens must not ship while read/validation are dishonest (src/v3/compiler/tests/integration/m2_lens_cost_migration_test.rs:151-158). I do not see a bounded scope plus named dissolution trigger for when those stubs are replaced or made uncallable, so this is an untracked bridge rather than tracked debt.

3. Verdict

REQUEST_CHANGES

The enforcement pass and regression test are directionally good, and the core compile-error receipt is present. The blocking problem is that the PR lands an importable substrate-facing Lens<ComplexitySummary> whose read and validate fields fabricate successful results while the real enforcement code uses a separate complexity_of path; that violates single-authority and fail-closed modeling. The build-script rerun deletion is also worth correcting before merge because it weakens bootstrap freshness for src/v3/std changes.

[briansrls]

Review metadata

• Provider / model: openai-pro / gpt-5-5-pro
• Commit: 6fdc3f10 · Trigger: manual
• Comparison: main @ 15cf2d31 ... cursor/t-las-complexity-compile-error-b113 @ 9560d2ea
• Conversation: View conversation

---

1. Story of the diff

This PR turns T-LAS gate #92 from a declared acceptance item into an executable compile-failure demonstration. It adds a complexity_enforceable authority in src/v3/lenses/complexity.dag, emits the relevant enforcement functions into lens_cost_generated.rs, wires a new enforced_lens_application infer-time consumer that finds EnforcedApplication<ComplexitySummary, AsymptoticClass> data and attaches a diagnostic when observed complexity exceeds the declared budget, and adds a fixture/test that proves the recursive demo fails compilation with a lens-enforcement diagnostic. Around that, it adds Rust realization carriers for Lens / Monoid / LensEnforcement, a Rust asymptotic lattice bridge for executable enforcement, bootstrap regen, and CI/test-timeout accommodations for the slow demo.

The load-bearing shape is: user imports lenses.complexity, compile_to_dag prepends the complexity authority before lowering, infer runs check_enforced_lens_applications, and that consumer evaluates the budget via lens_cost::complexity_of plus the generated complexity_enforcement_project / complexity_enforcement_violates functions. The intent is clear, but the PR also makes complexity_lens a substrate-visible Lens<ComplexitySummary> whose actual read / validate / algebra functions are stubs, which turns the carrier into an untruthful authority rather than a purely enforcement-only receipt.

2. Invariant categories

1. LAYER MODEL — Finding, BLOCKING. The diff touches substrate-facing .dag modeling by declaring data complexity_lens: Lens<ComplexitySummary>, but the declared lens is wired to fabricated behavior: src/v3/lenses/complexity.dag:446 says read: complexity_lens_read_stub, while src/v3/lenses/complexity.dag:419 returns Inhabits(zero_summary()) for every (Dag, Behavior). That makes a substrate-level Lens inhabitant available even though its core lens operation is not the complexity analysis it claims to model.
2. INVARIANTS.md + modeling-discipline.md — Finding, BLOCKING. This violates Fail-Closed and Single Authority / facts flow forward. The declared lens fabricates success (src/v3/lenses/complexity.dag:425: NoDiagnostic) and a plausible zero summary (src/v3/lenses/complexity.dag:419: Inhabits(zero_summary())), while the enforcement consumer separately reads the real fact from src/v3/compiler/src/enforced_lens_application.rs:140: let observed = match complexity_of(dag, &port) {. That leaves two authorities for “the complexity lens result”: the declared Lens says constant zero/no diagnostic, and the Rust enforcement path says complexity_of.
3. CODING.md — Finding, NON-BLOCKING unless this is the only std rerun hook. The build script hunk deletes src/v3/compiler/build.rs:365: println!("cargo:rerun-if-changed={}", std_dir.display());, immediately under a comment saying Cargo must rerun when staged std/spec/compiler files change. If there is not another unchanged std_dir rerun directive elsewhere, this breaks explicit dependency declaration for the bootstrap build edge: future src/v3/std/** edits can leave generated bootstrap state stale until some other tracked path changes.
4. TESTING.md — Compliant for the requested gate. The new test is integration-level because the promised behavior is end-to-end compile failure: src/v3/compiler/tests/integration/t_las_complexity_contract_compile_error_test.rs:26 calls compile_to_dag, :27 requires failure, and :36-38 checks that a ParseError carries the lens-enforcement receipt. The slow-test exemption is also bounded with a specific row and paydown direction at scripts/slow-test-exemptions.txt:81.
5. LOCKED DESIGN DECISIONS — N/A. I do not see the diff referencing or editing a line marked LOCKED; the issue above is against the live substrate/lens contract introduced in the diff, not a claimed divergence from a locked design paragraph.
6. TRACKED vs UNTRACKED DEBT — Finding, BLOCKING. The PR explicitly acknowledges the new carrier is a stub: src/v3/compiler/tests/integration/m2_lens_cost_migration_test.rs:154-155 says data complexity_lens lands as a “T-LAS substrate stub” and that “read/validate remain stubs.” That documents the debt, but I do not see bounds or a named dissolution trigger for when the substrate-visible false Lens must be replaced. The concrete stubbed lines are src/v3/lenses/complexity.dag:418-425 and :427-431; because this is substrate-visible modeling, an unbounded stub is not an acceptable bridge.

3. Verdict

REQUEST_CHANGES

The compile-error gate is wired coherently, and the regression test targets the right user-visible behavior. I would not merge this shape while complexity_lens is a substrate-declared Lens whose read/validate/algebra behavior fabricates results; either make the lens honest, make the enforcement carrier not require a fake lens, or land the bridge with explicit bounds and a checkable dissolution trigger. The build.rs rerun deletion also needs confirmation or restoration so std changes cannot silently stale the bootstrap.

[briansrls]

Review metadata

• Provider / model: openai-pro / gpt-5-5-pro
• Commit: ddf99d85 · Trigger: manual
• Comparison: main @ cf1d5230 ... cursor/t-las-complexity-compile-error-b113 @ ddf99d85
• Conversation: View conversation

---

1. Story of the diff

This PR turns T-LAS gate #92 from a declared demo into an executable receipt. complexity.dag now declares a LensEnforcement<ComplexitySummary, AsymptoticClass> plus complexity_enforceable, the generated module is renamed to complexity_lens_generated.rs, and compile_to_dag prepends the complexity lens authority whenever user code imports lenses.complexity. The new infer-side consumer, check_enforced_lens_applications, scans EnforcedApplication data, resolves DeclarationScope to a function result port, runs complexity_of, projects to AsymptoticClass, and attaches a compile diagnostic when the observed class strictly exceeds the budget. The PR also adds Rust realization support for the new lens carriers, a Rust asymptotic dominance bridge for executable generated code, a regression fixture/test for ClassLog being exceeded, and the expected bootstrap/manifest/census updates.

2. Invariant categories

1. LAYER MODEL (substrate vs implementation).

Finding — BLOCKING. This is not implementation-only: the diff lands a new public lens declaration, src/v3/lenses/complexity.dag:444: data complexity_lens: Lens<ComplexitySummary> = {, whose fields point at stub behavior: src/v3/lenses/complexity.dag:446: read: complexity_lens_read_stub and src/v3/lenses/complexity.dag:450: validate: complexity_lens_validate_stub. The corresponding stub bodies fabricate a successful witness and diagnostic-free validation, e.g. src/v3/lenses/complexity.dag:418: fn complexity_lens_read_stub(d: Dag, b: Behavior) -> Witness<ComplexitySummary> = followed by src/v3/lenses/complexity.dag:419: Inhabits(zero_summary()), and src/v3/lenses/complexity.dag:424: fn complexity_lens_validate_stub(d: Dag, c: ComplexitySummary) -> OptionalDiagnostic = followed by src/v3/lenses/complexity.dag:425: NoDiagnostic. Because this is a Lens<ComplexitySummary> substrate/lens value, future consumers can treat it as real even though its read/validate surface is only nominal.

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

Finding — P5 Progress Is Dissolution / P3 Fail-Closed. The enforcement authority itself is shaped correctly: src/v3/lenses/complexity.dag:406: fn complexity_enforcement_project(summary: ComplexitySummary) -> AsymptoticClass = and src/v3/lenses/complexity.dag:412: fn complexity_enforcement_violates(declared: AsymptoticClass, observed: AsymptoticClass) -> Bool = define the declared budget relation, and the Rust consumer imports those generated functions at src/v3/compiler/src/enforced_lens_application.rs:17-18. But the same diff also ships the nominal Lens with fabricated-success stubs above, which violates fail-closed modeling unless it is explicitly bounded as temporary debt with a dissolution trigger. The generated Rust preserves the same fabricated behavior at src/v3/compiler/src/complexity_lens_generated.rs:520-527.

1. CODING.md.

Finding — explicit dependencies. The build script hunk removes the std-directory rebuild dependency: src/v3/compiler/build.rs:365 (removed): println!("cargo:rerun-if-changed={}", std_dir.display());. That line sat directly under the comment saying staged std/spec/compiler file changes must rerun the build or bootstrap may silently miss them. This PR changes src/v3/std/algebra.dag and src/v3/std/lookup.dag, so dropping the std_dir trigger weakens the explicit build dependency surface for the same class of inputs this PR relies on.

1. TESTING.md.

Compliant. The PR adds a behavior-level integration receipt for the actual user contract: src/v3/compiler/tests/integration/t_las_complexity_contract_compile_error_test.rs:26-27 compiles the demo and expects failure, while src/v3/compiler/tests/integration/t_las_complexity_contract_compile_error_test.rs:36-37 checks the emitted diagnostic kind/message for the documented “lens enforcement violation” receipt. The fixture is also minimal for this compile-error demonstration, with the contract data concentrated at src/v3/compiler/tests/fixtures/t_las_complexity_contract_demo.dag:17-22.

1. LOCKED DESIGN DECISIONS.

N/A — no locked thesis/design decision is modified in the diff. The R3 program-plan row is updated to a receipt at docs/r3-program-plan.md:293, and the coarse .dag vs executable polynomial-degree behavior is explicitly documented at src/v3/std/algebra.dag:410-414.

1. TRACKED vs UNTRACKED DEBT.

Finding — BLOCKING. The diff explicitly acknowledges the new scaffold: src/v3/compiler/tests/integration/m2_lens_cost_migration_test.rs:154: /// Gate #92 lands nominal \data complexity_lens as a **T-LAS substrate stub**andsrc/v3/compiler/tests/integration/m2_lens_cost_migration_test.rs:155: /// (read/validate remain stubs).Documentation and some bounds are present, but I do not see a named dissolution trigger replacing the removed stop-ratchet that previously rejectedcomplexity_lensuntil the read/class-5 validation surface was honest. Under the tracked-debt rule, the PR should either name the concrete trigger/ROADMAP row for replacing these stubs, or avoid exposing the nominalLens<ComplexitySummary> as a real substrate value yet.

3. Verdict

REQUEST_CHANGES

The enforcement path is coherent and the regression test targets the right user-visible behavior, but the PR ships a public Lens<ComplexitySummary> surface backed by fabricated-success stubs without a named dissolution trigger. I would also restore or replace the removed std_dir build dependency so std DAG changes continue to invalidate generated/bootstrap artifacts predictably.

[briansrls]

Review metadata

• Provider / model: codex / unknown
• Commit: 9560d2ea · Trigger: schedule
• Thinking: 353s wall

---

BLOCKING (1)

Root Cause

• src/v3/lenses/complexity.dag nominal Lens was promoted to substrate before honest read/sequential/branch/iterate functions or a bounded dissolution trigger existed -> wire the existing complexity fold into the Lens fields or keep EnforceableLens from exposing a Lens until the real instance lands.

ROADMAP — Incomplete

• complexity_violation_compile_error_demonstrated: The compile-error consumer exists, but the receipt still lands an untruthful Lens Monoid stub that would mislead generic T-LAS consumers.

⚠️ One substrate-level Lens instance law violation should be fixed before landing.

[briansrls]

Review metadata

• Provider / model: openai-pro / gpt-5-5-pro
• Commit: e4267051 · Trigger: manual
• Comparison: main @ cf1d5230 ... cursor/t-las-complexity-compile-error-b113 @ 45b8164c
• Conversation: View conversation

---

1. Story of the diff

This PR wires the T-LAS complexity-contract demo from declaration to enforcement: user programs that import lenses.complexity now get src/v3/lenses/complexity.dag prepended during lowering (src/v3/compiler/src/lib.rs:4503-4507, src/v3/compiler/src/lower.rs:183-193), and inference runs a new Rust consumer that scans EnforcedApplication<ComplexitySummary, AsymptoticClass> values, resolves the declared section, computes complexity_of, projects the observed class, and attaches a compile diagnostic when the budget is exceeded (src/v3/compiler/src/infer.rs:279, src/v3/compiler/src/enforced_lens_application.rs:21-169). The .dag side now declares the canonical complexity Lens, LensEnforcement, and EnforceableLens surfaces (src/v3/lenses/complexity.dag:485-504), while Rust emission gets generated complexity-lens functions, helper carriers, Rust target instantiations, and a small executable asymptotic lattice bridge. The regression fixture demonstrates a recursive function capped at ClassLog and asserts compilation fails with a lens-enforcement diagnostic (src/v3/compiler/tests/fixtures/t_las_complexity_contract_demo.dag:14-22, src/v3/compiler/tests/integration/t_las_complexity_contract_compile_error_test.rs:26-38).

2. Invariant categories

1. LAYER MODEL (substrate vs implementation). — Finding (BLOCKING)

Principle: single authority / substrate truth. The diff declares that .dag LensEnforcement remains the authority, but then gives polynomial-vs-polynomial enforcement a different Rust-only meaning. The declared enforcement uses asymptotic_dominates in complexity.dag:

src/v3/lenses/complexity.dag:417-419 — if asymptotic_dominates(observed, declared) then ...

But the same diff documents that the .dag carrier stays coarse:

src/v3/std/algebra.dag:410-413 — “asymptotic_dominates(ClassPolynomial, ClassPolynomial) stays coarse ... Polynomial degree is enforced ... in the executable bridge”

and then injects that Rust bridge into the generated complexity module:

src/v3/compiler/src/lib.rs:3351 — use crate::complexity_lattice::asymptotic_dominates;

with degree-aware behavior:

src/v3/compiler/src/complexity_lattice.rs:28-30 — positive_descent_count(da) >= positive_descent_count(db)

That means the declared complexity_enforcement_violates can answer differently depending on whether the consumer evaluates the .dag relation or the Rust bridge. For example, observed = ClassPolynomial(5) and declared = ClassPolynomial(3) is non-strict under the documented .dag coarse relation but strict under the Rust bridge. If polynomial degree matters for T-LAS budgets, the degree-aware relation needs to be the declared substrate relation, or it needs a separately named declared enforcement relation that Rust consumes exactly. This is a substrate/implementation split, not just an implementation optimization. chatgpt-review-2ca521a2-1938-41…

1. INVARIANTS.md + modeling-discipline.md. — Finding (BLOCKING)

Principle: fail-closed / API-level enforcement. The exported consistency predicate appears to check the dominance direction backwards:

src/v3/lenses/complexity.dag:468-469 — fn complexity_summary_work_class_consistent(c: ComplexitySummary) -> Bool = asymptotic_dominates(classify_symbolic_cost(c.work), c.asymptotic_class)

Given the lattice order used elsewhere in this diff, a stored summary class should at least cover the classified work class. The predicate above returns true when the classified work dominates the stored class, so an underreported summary such as work = LinearCost(...) with asymptotic_class = ClassConstant would pass. Since the same block says this predicate is exported for callers/folds (src/v3/lenses/complexity.dag:403-407), this leaks an unsafe predicate at the declared lens surface even though validate is currently scaffolded to NoDiagnostic. chatgpt-review-cc1c4a2a-f44a-47…

1. CODING.md. — Compliant

The new enforcement consumer is a free function wired from inference rather than a new Dag method or object-style pass: infer calls crate::enforced_lens_application::check_enforced_lens_applications(dag) at src/v3/compiler/src/infer.rs:279, and the implementation keeps helper logic local with typed carriers like AsymptoticClass, Lookup, FieldValue, and Diagnostic (src/v3/compiler/src/enforced_lens_application.rs:12-19). That matches the data-plus-functions style and explicit dependency shape. chatgpt-review-c4a04185-b2d3-40…

1. TESTING.md. — Finding (NON-BLOCKING once the authority split is fixed)

The added tests cover the demo compile error and the Rust bridge’s local polynomial ordering, but not the declared .dag enforcement semantics that now diverge. The bridge unit test pins only complexity_lattice::asymptotic_dominates (src/v3/compiler/src/complexity_lattice.rs:82-88), while the integration demo exercises ClassUnknown > ClassLog (src/v3/compiler/tests/fixtures/t_las_complexity_contract_demo.dag:3-7, src/v3/compiler/tests/integration/t_las_complexity_contract_compile_error_test.rs:36-38). After the single-authority fix, add a behavior test for EnforcedApplication with polynomial budgets so the published enforcement contract, not just the Rust helper, is pinned. chatgpt-review-70b608c8-d5e8-44…

1. LOCKED DESIGN DECISIONS. — N/A

N/A — the diff updates the R3 program-plan receipt row and Rust realization surfaces, but I do not see a change to a locked thesis/design decision in the diff.

1. TRACKED vs UNTRACKED DEBT. — Finding (BLOCKING as part of the layer-model issue)

The validate scaffold is tracked well enough: it documents the temporary NoDiagnostic behavior, bounds it to SomeDiagnostic lowering limitations, and names the class-5 diagnostic-authorship/span-witness dissolution path (src/v3/lenses/complexity.dag:403-407). The polynomial asymptotic bridge is not similarly tracked: src/v3/std/algebra.dag:410-414 documents that .dag remains coarse while Rust enforces degree, but it does not name a dissolution trigger for when the executable bridge stops being a parallel semantic authority. That missing trigger makes the bridge untracked debt under the progress-is-dissolution rule. chatgpt-review-2ca521a2-1938-41…

3. Verdict

REQUEST_CHANGES

The compile-error path itself is understandable and mostly well-wired, but the PR currently splits the complexity-budget ordering between a coarse declared .dag relation and a stricter Rust bridge while presenting the lens enforcement as substrate truth. Fix the single-authority issue, and correct or remove the reversed exported consistency predicate before this lands.

[briansrls]

Review metadata

• Provider / model: codex / unknown
• Commit: 9f080c07 · Trigger: schedule
• Thinking: 393s wall

---

BLOCKING (1)

Root Cause

• src/v3/lenses/complexity.dag the exported consistency predicate has no ratchet case for classified work strictly exceeding the stored asymptotic_class → swap the dominance order, or require mutual dominance for exactness, and add a negative ClassLinear-vs-ClassLog test before generic lens consumers rely on it.

ROADMAP — Incomplete

• complexity_violation_compile_error_demonstrated: The compile-error path is present, but the same lens authority now exports an unsound class-consistency predicate.

⚠️ One substrate-level complexity predicate should be corrected before this lands.

[briansrls]

Review metadata

• Provider / model: openai-pro / gpt-5-5-pro
• Commit: 45b8164c · Trigger: manual
• Comparison: main @ cf1d5230 ... cursor/t-las-complexity-compile-error-b113 @ f543c780
• Conversation: View conversation

---

1. Story of the diff

This PR turns T-LAS gate #92 from a declared acceptance item into a concrete compile-fail receipt. It adds real complexity lens authority in src/v3/lenses/complexity.dag: complexity_lens, its LensEnforcement, and complexity_enforceable; then compile_to_dag conditionally prepends that authority when a user module imports lenses.complexity, so the user fixture can author an EnforcedApplication<ComplexitySummary, AsymptoticClass>. During infer, the new check_enforced_lens_applications pass finds complexity enforceable applications, resolves the DeclarationScope function, reads the function result port through the generated complexity lens, projects its asymptotic class, and emits a ParseError diagnostic when the observed class strictly exceeds the declared budget.

The Rust side supports that by renaming the generated lens snapshot to complexity_lens_generated.rs, adding T-LAS carrier structs for emitted Lens / Monoid / LensEnforcement records, and adding a hand-written complexity_lattice::asymptotic_dominates executable bridge so generated complexity enforcement can compare polynomial degrees. The regression fixture is intentionally small: a recursive function capped at ClassLog, expected to compile-fail with a lens enforcement violation, plus timeout/stack accommodations for the heavy integration path.

2. Invariant categories

1. LAYER MODEL — Finding, BLOCKING: single authority / substrate semantics.

The diff now has two authorities for the same named cost-ordering fact. src/v3/std/algebra.dag:410-414 says: “asymptotic_dominates(ClassPolynomial, ClassPolynomial) stays coarse at the .dag lattice tier … Polynomial degree is enforced … in the executable bridge v3_compiler::complexity_lattice::asymptotic_dominates.” The bridge then implements degree-sensitive behavior at src/v3/compiler/src/complexity_lattice.rs:25-31, including positive_descent_count(da) >= positive_descent_count(db). Because complexity_enforcement_violates calls asymptotic_dominates as the enforcement relation (src/v3/compiler/src/complexity_lens_generated.rs:509-511), consumers can now observe different answers depending on whether they consume the .dag substrate function or the Rust bridge. That violates Boundary Discipline / single authority for a substrate-level cost lattice. Either move the degree-aware relation into the .dag authority, or make the Rust bridge an explicitly named bounded adapter with a dissolution trigger and a ratchet proving no other consumer treats it as the canonical asymptotic_dominates.

1. INVARIANTS.md + modeling-discipline.md — Finding, BLOCKING: fail-closed + illegal states unrepresentable.

The lattice comment preserves the invariant that ClassPolynomial means k>=3: src/v3/std/algebra.dag:408 says ClassQuadratic <= ClassPolynomial(k>=3). But the new enforcement decoder accepts any positive descent amount as a polynomial degree: src/v3/compiler/src/enforced_lens_application.rs:311-314 decodes ClassPolynomial and immediately returns Some(AsymptoticClass::ClassPolynomial { degree }), and src/v3/compiler/src/enforced_lens_application.rs:352 accepts "OneStep" as a valid PositiveDescentAmount. Combined with src/v3/compiler/src/complexity_lattice.rs:31, where any ClassPolynomial { .. } dominates ClassQuadratic | ClassLinearithmic | ClassLinear | ClassLog | ClassConstant, a user-authored ClassPolynomial { degree: OneStep } budget can be treated as more permissive than ClassQuadratic instead of being rejected as an invalid budget shape. The enforcement path should fail closed for polynomial degrees below 3, or the type should make sub-cubic polynomial classes unrepresentable.

1. CODING.md — Compliant.

The new enforcement logic is implemented as explicit data + free functions, not hidden object state: src/v3/compiler/src/enforced_lens_application.rs:21-22 defines check_enforced_lens_applications(dag: &mut Dag), and src/v3/compiler/src/infer.rs:279 wires it as a clear pipeline step.

1. TESTING.md — Compliant with the main behavior target.

The added test is an integration test because the contract is the full compile_to_dag boundary producing a semantic compile error, and the test names that behavior directly at src/v3/compiler/tests/integration/t_las_complexity_contract_compile_error_test.rs:1-6. The fixture is focused on one enforcement claim: import complexity authority, define one recursive function, and attach one EnforcedApplication with a ClassLog budget (src/v3/compiler/tests/fixtures/t_las_complexity_contract_demo.dag:13-21).

1. LOCKED DESIGN DECISIONS — N/A.

I do not see this diff editing a section marked locked in the supplied design/thesis materials; the touched program-plan row records gate #92 as a receipt but does not itself alter a locked design decision.

1. TRACKED vs UNTRACKED DEBT — Finding, NON-BLOCKING: slow-test exemption lacks a checkable dissolution trigger.

scripts/slow-test-exemptions.txt:81 adds a 14s exemption and says: “paydown shared OnceLock / slimmer demo or fold into existing cached demo harness.” That documents the reason and gives possible strategies, but it is not a named dissolution trigger. The neighboring exemption shows the expected shape: delete the line and lower TEST_TIMEOUT_MAX_EXEMPTIONS once a specific timed command is <=2000ms (scripts/slow-test-exemptions.txt:79). Add the same checkable trigger to the new exemption so this remains tracked debt rather than a permanent slow-test carveout.

3. Verdict

REQUEST_CHANGES

The compile-error demonstration is wired end-to-end and the regression test targets the right boundary, but the PR currently introduces a divergent Rust authority for a substrate cost-ordering fact and lets invalid sub-cubic ClassPolynomial budgets pass through the new enforcement decoder. Those are substrate/modeling issues, so I would fix them before landing; the slow-test exemption trigger can be cleaned up in the same pass.

[briansrls]

Review metadata

• Provider / model: codex / unknown
• Commit: 765aaddc · Trigger: schedule
• Thinking: 435s wall

---

Non-blocking — Strengths

• src/v3/lenses/complexity.dag The complexity lens authority now keeps read, compose, branch, iterate, and enforcement on the same generated substrate-backed surface.

ROADMAP — Verified

• complexity_violation_compile_error_demonstrated: The PR adds the EnforcedApplication fixture and compile-error test showing a ClassLog complexity budget violation becomes a typed compile diagnostic.

✅ No blocking concerns found for the changed code, .dag substrate, or roadmap receipt.

[briansrls]

Review metadata

• Provider / model: codex / unknown
• Commit: 444316f0 · Trigger: schedule
• Thinking: 171s wall

---

Non-blocking — Strengths

• src/v3/lenses/complexity.dag The complexity lens now keeps read, compose, branch, iterate, and enforcement on the declared T-LAS surface.
• src/v3/compiler/src/enforced_lens_application.rs The enforcement consumer fail-closes unresolved section, budget, and complexity Miss cases with diagnostics.

ROADMAP — Verified

• complexity_violation_compile_error_demonstrated: The PR adds the T-LAS complexity demo fixture and compile-error test proving a ClassLog budget violation becomes a typed compile diagnostic.

✅ No blocking concerns found for the changed code, .dag model surface, or roadmap receipt.

[briansrls]

Review metadata

• Provider / model: openai-pro / gpt-5-5-pro
• Commit: 444316f0 · Trigger: manual
• Comparison: main @ cf1d5230 ... cursor/t-las-complexity-compile-error-b113 @ 444316f0
• Conversation: View conversation

---

1. Story of the diff

This PR turns the T-LAS complexity contract from a declared lens surface into an exercised compile-time enforcement path. The substrate-side authority is added in src/v3/lenses/complexity.dag: the complexity lens now exposes project/violates, wires LensEnforcement into complexity_enforceable, and aliases the concrete EnforcedApplication<ComplexitySummary, AsymptoticClass> shape at src/v3/lenses/complexity.dag:518-528. On the compiler side, compile_to_dag prepends lenses/complexity.dag only when the user imports lenses.complexity, seals that prepended range as non-user authority, and then infer invokes the enforcement checker (src/v3/compiler/src/lib.rs:4529-4552, src/v3/compiler/src/lower.rs:183-192, src/v3/compiler/src/infer.rs:279).

The checker resolves complexity EnforcedApplication data, extracts the declared section and budget, computes complexity_of for the function result port, projects its asymptotic class through the generated complexity-lens function, and emits a ParseError when the observed class strictly exceeds the declared budget (src/v3/compiler/src/enforced_lens_application.rs:142-166). The PR also adds a Rust-side complexity_enforcement_budget_dominates bridge for the enforcement-grade asymptotic order, including degree-sensitive ClassPolynomial comparison while documenting that the .dag lattice remains poly-tier coarse for now (src/v3/compiler/src/complexity_lattice.rs:1-17, src/v3/compiler/src/complexity_lattice.rs:31-36, src/v3/std/algebra.dag:410-418). The user-visible receipt is the new fixture declaring a recursive witness capped at ClassLog, plus an integration test that expects CompileError::Semantic with a ParseError containing lens enforcement violation (src/v3/compiler/tests/fixtures/t_las_complexity_contract_demo.dag:14-23, src/v3/compiler/tests/integration/t_las_complexity_contract_compile_error_test.rs:26-41).

2. Invariant categories

1. LAYER MODEL (substrate vs implementation).

Compliant — this diff does touch substrate-facing lens declarations, but the authority remains in .dag: complexity_enforcement names project and violates, and complexity_enforceable composes that with complexity_lens rather than inventing a Rust-only contract surface (src/v3/lenses/complexity.dag:518-526). The Rust consumer reads the generated functions via complexity_enforcement_project / complexity_enforcement_violates, so the implementation path is a consumer of the declared lens authority, not a parallel enforcement definition (src/v3/compiler/src/enforced_lens_application.rs:17-19, src/v3/compiler/src/enforced_lens_application.rs:142-155).

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

Compliant — fail-closed behavior is explicit at the enforcement boundary: missing complexity output becomes a diagnostic instead of a fabricated pass (src/v3/compiler/src/enforced_lens_application.rs:142-153), malformed ClassPolynomial budgets reject sub-cubic Peano degrees instead of silently treating them as polynomial (src/v3/compiler/src/enforced_lens_application.rs:313-321), and an actual violation emits a typed compiler diagnostic (src/v3/compiler/src/enforced_lens_application.rs:158-166). Facts also flow forward through the prepended authority range: the compiler seals the prepended complexity lens declarations before lowering the user module, so strict user-only sweeps do not confuse authority declarations with the user range (src/v3/compiler/src/dag.rs:3045-3049, src/v3/compiler/src/lower.rs:186-192).

1. CODING.md.

Compliant — the new logic is mostly data-plus-free-functions: complexity_enforcement_budget_dominates(a, b) -> bool is a pure helper over explicit inputs (src/v3/compiler/src/complexity_lattice.rs:17-18), and the enforcement pass is a free function over &mut Dag rather than a method-heavy object layer (src/v3/compiler/src/enforced_lens_application.rs:21-22). The one new Dag method is narrowly scoped to mutating Dag’s own append-boundary invariant, which is the appropriate owner for that state transition (src/v3/compiler/src/dag.rs:3045-3049).

1. TESTING.md.

Compliant — the test shape matches the feature’s actual boundary: the contract is “a source-level EnforcedApplication fails compilation,” so the integration test drives compile_to_dag on a minimal .dag fixture and asserts the published error behavior rather than internal map layout (src/v3/compiler/tests/fixtures/t_las_complexity_contract_demo.dag:17-23, src/v3/compiler/tests/integration/t_las_complexity_contract_compile_error_test.rs:26-41). The degree-sensitive lattice bridge also has focused unit coverage for poly degree ordering (src/v3/compiler/src/complexity_lattice.rs:95-101).

1. LOCKED DESIGN DECISIONS.

N/A — I did not see this diff alter a LOCKED design paragraph or change a locked thesis decision. The R3 program-plan row for gate #92 is updated to a receipt, but that is a status update tied to the new fixture/test receipt, not a locked-design divergence (docs/r3-program-plan.md:92 row change shown in diff).

1. TRACKED vs UNTRACKED DEBT.

Compliant — the temporary poly-degree split is documented and bounded: enforcement uses the Rust bridge for degree-sensitive ClassPolynomial budgets, while .dag asymptotic_dominates remains tier-coarse until payload-pattern lowering can carry the same Peano comparison (src/v3/compiler/src/complexity_lattice.rs:4-8, src/v3/std/algebra.dag:410-418). The validate hook’s current NoDiagnostic shape is also explicitly bounded to the missing SomeDiagnostic lowering path and names a dissolution route through lens-authored diagnostics/span witnesses (src/v3/lenses/complexity.dag:403-408, src/v3/lenses/complexity.dag:491-492). The slow-test exemption is tracked with documentation, a bound, and a concrete deletion/lower-floor trigger (scripts/slow-test-exemptions.txt:81), and the added hand-authored paths are paired through SG-0 (scripts/ci-merge/sg0-pr-body-append.2340.txt:1-3).

3. Verdict

APPROVE

I did not find a line-backed blocking issue. The PR keeps the substrate authority in complexity.dag, consumes it through generated/projected functions, fails closed on missing or over-budget complexity evidence, and adds an integration receipt for the gate it claims to close.