Repository navigation
v2 complexity.dag rework — well-modeled lens applying v4 modeling discipline (CALIBRATION investigation, brief at /tmp/v2_complexity_lens_brief.md) - #3398
Conversation
briansrls
left a comment
There was a problem hiding this comment.
Review metadata
- Provider / model:
codex/unknown - Commit:
1f8d55e2· Trigger:schedule - Thinking:
269s wall
BLOCKING (3)
Root Cause
src/v2/complexity.dagasymptotic class is being modeled as a new local enum rather than projected through std.induction.CostBound/ProductBound → reuse the existing bound carrier or add a valid dissolution-tagged bridge with a concrete trigger.src/v2/complexity.dagComplexityBound lacks structural product/log-factor coordinates even though CostBound already has ProductBound factors → represent polynomial and log factors structurally or keep classification on normalized CostExpr/CostBound.src/v2/complexity.dagnear-miss semantics are encoded both in discharge_complexity_lens_tdd_case and again at the table call site → keep the expectation semantics in one place and call the case directly.
| // Node -> Witness<ComplexityBound> via cost_of_expr + asymptotic projection. | ||
| // ========================================================================= | ||
|
|
||
| type ComplexityBound |
There was a problem hiding this comment.
BLOCKING: ComplexityBound adds a new substrate coproduct without the required 🟢/🟡/🔴 tag and duplicates the existing std.induction.CostBound asymptotic-bound algebra instead of grounding in it (INVARIANTS P1/P5, MODELING M9).
| BoundLinear => BoundQuadratic | ||
| BoundQuadratic => BoundPolynomial { degree: 3 } | ||
| BoundPolynomial { degree: d } => BoundPolynomial { degree: d + 1 } | ||
| other => other |
There was a problem hiding this comment.
BLOCKING: The new multiplication projection underestimates O(n * log n): BoundLinear times BoundLog falls through to BoundLog instead of BoundLinearithmic, so classify_complexity can report a lower class than CostExpr proves (INVARIANTS P1/P3).
| && discharge_complexity_lens_tdd_case(case: complexity_lens_tdd_linear_pass()) | ||
| && discharge_complexity_lens_tdd_case(case: complexity_lens_tdd_quadratic_fires()) | ||
| && discharge_complexity_lens_tdd_case(case: complexity_lens_tdd_unknown_advisory()) | ||
| && !discharge_complexity_lens_tdd_case(case: complexity_lens_tdd_near_miss()) |
There was a problem hiding this comment.
BLOCKING: complexity_lens_tdd_table_passes negates the near-miss case even though ExpectNearMiss already discharges as !matches, making the table fail when the near-miss behaves correctly.
|
Closing per operator wrap-up directive 2026-05-20. Worker deep-seal-431 is archived; closing on their behalf as PM. Branch stays in place. |
Auto-opened by session-dashboard for session
deep-seal-431.Pushing to
session/deep-seal-431advances this PR.Worker attestation
Before flipping this PR to ready for review, confirm each item:
npm test,cargo test) and the result.Closes #Ndirective.Summary
TODO: replace this paragraph with one or two sentences naming the change and its motivation. Reviewers read this first.
Test plan