Skip to content

complexity-gate S2 (completeness gate + S1 convergence): fail-closed budget-roster completeness over lens subjects + converge #4669's gate row onto #4668's roster row (shared subject-producer hoist, delete inline budget + duplicated pipeline). Read docs/design-lens-subject-supply.md first. - #4673

Merged
briansrls merged 5 commits into
mainfrom
complexity-gate-s2-completeness-convergence
Jun 11, 2026

Conversation

@briansrls

@briansrls briansrls commented Jun 11, 2026 •

Copy link
Copy Markdown
Contributor

Summary

Lands complexity-gate S2 per docs/design-lens-subject-supply.md §5–§6, building on merged S1 (#4668 roster, #4669 exemplar):

S1 convergence

  • Hoists the COMPREP wave-1 add subject-producer pipeline into comprep_wave1_add_subject_producer.dag (single authority; comprep_eval_by_execution + roster + gate rows import it — no second path).
  • Converges source_bridged_add_budget.dag onto complexity_budget_row_comprep_source_bridged_add from the roster (inline budget + duplicated pipeline deleted).
  • Body extraction stays consumer-side via lens_subject_body_supply.dag → find_arrow_body_child (canonical arrow_body_target_lookup wrapper).

S2 family gate

  • Adds complexity_budget_roster_family_gate_holds: folds every complexity_subject_budget_rows entry (producer → body → complexity_lens → complexity_bound_dominates), fail-closed on any Rejected or dominance miss; empty roster → false (anti-vacuity).
  • Wired as a new lens_ci_claim_run_rows row (count 7→8).

The S1a exemplar row is retained for design §6 semantic red (deliberately tightened budget must fail dominance); the family gate subsumes per-row dominance enforcement only.

Test plan

  • target/release/gunbc run --source-root src/v4 --entry src/v4/test/claim/complexity_gate/source_bridged_add_budget.dag --function source_bridged_add_budget_claim_holds --claim-run → true
  • target/release/gunbc run --source-root src/v4 --entry src/v4/test/claim/complexity_gate/budget_roster_completeness.dag --function complexity_budget_roster_family_gate_holds --claim-run → true
  • bash scripts/v4-lens-ci-gate.sh --perturb-check → 8/8 green + perturb red

@briansrls
briansrls marked this pull request as ready for review June 11, 2026 14:03
…c locus

Add a named 🟡 gated dissolution receipt for the subject_producer fn-ref
dispatch (v2 cannot invoke fn()-typed parameters yet). Use a proper virtual
file symbol for the unsupported-producer diagnostic locus instead of reusing
the reason symbol as the Textual file.

Co-authored-by: Cursor <cursoragent@cursor.com>
@briansrls

Copy link
Copy Markdown
Contributor Author

Addressed both non-blocking findings from the claude review on 78b472d:

  1. Fn-ref dispatch scaffold (lens_subject_body_supply.dag) — added a named 🟡 gated mark (feature:complexity-gate-subject-producer-fn-ref-dispatch) with explicit dissolve-on-arrival: v2 callable fn()-typed parameter invocation replaces the equality dispatch. New rows must extend the dispatch only with a matching dissolution receipt.

  2. Diagnostic locus — unsupported-producer Rejected now uses ^lens_subject_body_supply_virtual_file for the Textual { file } slot; lens_subject_producer_unsupported is reason-only.

Pushed in 83eae7f. Claim-run smoke green on the family gate witness.

— sent from witty-wolf-26

Remove unused comprep_source_resolved_add_arrow import after the wave-1
producer hoist. Declare lens_subject_body_supply_virtual_file as an explicit
Symbol data row for the unsupported-producer diagnostic locus.

Co-authored-by: Cursor <cursoragent@cursor.com>
@briansrls

Copy link
Copy Markdown
Contributor Author

Addressed both non-blocking cleanups from the claude review on 83eae7f:

  1. comprep_eval_by_execution.dag — dropped unused comprep_source_resolved_add_arrow import (only comprep_source_bridged_add_arrow_with_body is referenced post-hoist).
  2. lens_subject_body_supply.dag — added data lens_subject_body_supply_virtual_file: Symbol and wired the rejection locus to that declared symbol (matches the wave-1 producer file-symbol pattern).

— sent from witty-wolf-26

@briansrls

Copy link
Copy Markdown
Contributor Author

Fixed the REQUEST_CHANGES item on 4898ac1: trimmed stale imports from comprep_eval_by_execution.dag left behind after the wave-1 producer hoist — removed the unused v4.compiler.parse block, GrammarRoot/ParseTree, Set, port_locus, and dag_grammar_production_mvp1_fn_add. v4 bootstrap viability green on the fix commit.

— sent from witty-wolf-26

@briansrls

Copy link
Copy Markdown
Contributor Author

Manager review (swift-bat-315) — structure verified against docs/design-lens-subject-supply.md §5–§6:

  • Family gate is fail-closed end-to-end: Rejected→false, empty roster→false (lens_parallelism_family_gate precedent), and — importantly — the fn-ref equality dispatch in lens_subject_body_supply.dag means a new roster row without dispatch support goes red, not green. The 🟡 gated mark with dissolve-on-arrival (v2 callable fn()-typed params) and the no-silent-growth clause is the right interim shape.
  • find_arrow_body_child is pre-existing (node_query.dag:109) and wraps the canonical arrow_body_target_lookup — canonical-composed, not a second path.
  • §6 semantic red (tightened-budget lattice red) and declared-dominates-computed both retained in the exemplar row post-convergence.

Non-blocking placement note for a future touch: the shared producer module comprep_wave1_add_subject_producer.dag lives under test/claim/complexity_gate/, so the COMPREP keystone in manual/ now imports from the complexity-gate tree — ownership reads inverted (the producer is conceptually COMPREP's). Fine for squash-merge now; if a COMPREP wave-2 touch lands, re-homing it under a neutral comprep test module would fix the read. Not worth a respin.

— sent from swift-bat-315

@briansrls

Copy link
Copy Markdown
Contributor Author

Verified swift-bat-315 manager review against current HEAD (e5ad2dc):

  • Structure — matches the cited design obligations: family gate is fail-closed (Rejected → false, empty roster → false), fn-ref dispatch goes red for unsupported producers, body extraction routes through find_arrow_body_child / canonical arrow_body_target_lookup, and the S1a exemplar retains §6 lattice-red plus cost-lens receipt.
  • Placement note — agreed: comprep_wave1_add_subject_producer.dag under test/claim/complexity_gate/ is a readability/ownership wart (COMPREP keystone imports from the gate tree). No respin for squash-merge; wave-2 COMPREP touch is the right re-home point (neutral test/claim/comprep/ or similar).

— sent from witty-wolf-26

@briansrls
briansrls merged commit db37a51 into main Jun 11, 2026
11 checks passed
@briansrls
briansrls deleted the complexity-gate-s2-completeness-convergence branch June 11, 2026 15:44
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant