Skip to content

complexity-gate S1a: source-bridged add lens witness (design-lens-subject-supply) - #4669

Merged
briansrls merged 5 commits into
mainfrom
session/snappy-heron-686
Jun 11, 2026
Merged

briansrls merged 5 commits into
mainfrom
session/snappy-heron-686

Conversation

@briansrls

@briansrls briansrls commented Jun 11, 2026 •

Copy link
Copy Markdown
Contributor

Summary

Lands complexity-gate S1a per docs/design-lens-subject-supply.md (PR #4670): one perturb-checked lens_ci_gate row whose witness obtains a real compiled COMPREP wave-1 add body via the sanctioned source-bridge pipeline (tokenize → parse → normalize → resolve → body_producer), extracts the body with arrow_body_target_lookup, and gates via cost_lens → complexity_lens → complexity_bound_dominates. Honest label: source-bridged add, not 02_parse stage coverage (unreachable until COMPREP waves 2+).

Design

  • Implements design §2 recipe in src/v4/test/claim/complexity_gate/source_bridged_add_budget.dag
  • No host/--subject flag (design §4 R2 rejected)
  • No runtime body_of / module-table lookup
  • §6 in-witness semantic red: constant declared budget fails to dominate synthetic linear bound

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
  • bash scripts/v4-lens-ci-gate.sh --perturb-check → 7/7 green + perturb red

Brian Searls and others added 3 commits June 11, 2026 12:36
…subject-supply

Implement the COMPREP source-bridge handoff (tokenize→parse→normalize→resolve→
body_producer) with arrow_body_target_lookup body extraction, cost/complexity
fold, and dominance gating. Replace unreachable 02_parse target with honestly
labeled wave-1 add exemplar row in lens_ci_gate.

Co-authored-by: Cursor <cursoragent@cursor.com>
@briansrls briansrls changed the title complexity-gate S1a (reflection bridge + exemplar witness): make a real compiled compiler-stage function body available as a Node subject to lens witnesses — reuse the COMPREP body_producer/resolve-bridge (#4608/#4624/#4660), NOT hand-built SyntheticOccurrence fixtures and NOT PROV/spans. Then land complexity-gate S1a: source-bridged add lens witness (design-lens-subject-supply) Jun 11, 2026
@briansrls
briansrls marked this pull request as ready for review June 11, 2026 12:56
Dissolve parallel lookup reimplementation flagged in review; delegate to
the canonical node_query accessor used by COMPREP sibling claims.

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

Copy link
Copy Markdown
Contributor Author

Addressed in 7a54bf2: removed complexity_gate_arrow_body, the local complexity_gate_diagnostic helper, and the four complexity_gate_reason_* symbols. Body extraction now delegates to find_arrow_body_child from v4.std.node_query, matching comprep_add_body_producer.dag and 03_body_producer.dag.

Witness re-verified green locally (source_bridged_add_budget_claim_holds → true).

— sent from snappy-heron-686

@briansrls
briansrls merged commit 6bd5557 into main Jun 11, 2026
11 checks passed
@briansrls
briansrls deleted the session/snappy-heron-686 branch June 11, 2026 13:44
briansrls added a commit that referenced this pull request Jun 11, 2026
…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)

* WIP: complexity-gate S2 (completeness gate + S1 convergence): fail-closed bud

* WIP: complexity-gate S2 (completeness gate + S1 convergence): fail-closed bud

* fix(complexity-gate): mark fn-ref dispatch scaffold and fix diagnostic 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>

* chore(complexity-gate): drop dead import and declare virtual file symbol

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>

* WIP: complexity-gate S2 (completeness gate + S1 convergence): fail-closed bud

---------

Co-authored-by: Brian Searls <briansearls1@gmail.com>
Co-authored-by: Cursor <cursoragent@cursor.com>
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