Repository navigation
Gate the complexity lens by-execution (discoverable test fn witnesses) - #5085
Merged
Merged
Conversation
gunbai-bot
Bot
changed the title
briansrls
added a commit
that referenced
this pull request
Jun 17, 2026
…ty_gate witnesses to discoverable test fn *_test.dag (#5087) The budget gate — complexity_bound_dominates(declared_budget, computed_class) over the source-bridged COMPREP `add` subject — was written as plain fn ..._claim_holds in non-*_test.dag files, so claim_batch --roster-from-discovery ran it ZERO times (coverage-by-illusion; the lens_ci_gate.dag roster that named it is dead/unconsumed). Rename source_bridged_add_budget.dag and budget_roster_completeness.dag to *_test.dag and mark the gate functions test fn so the CI floor discovers them: - source_bridged_add_budget_claim_holds: real add body costs, its ConstantComplexity budget dominates the computed class, and a too-tight constant budget does NOT dominate a linear class (over-budget -> RED, §6 lattice control). - complexity_budget_roster_family_gate_holds: fail-closed family fold over the real roster (empty -> false, never vacuous green) + embedded planted-bad-row red. - complexity_budget_roster_unrated_declared_budget_semantic_red_holds: explicit planted-bad-row discrimination (unrated budget appended -> family fold rejects). Verified by execution: all 3 green AND present in claim_batch's discovered roster (178 -> 181 witnesses, 0 FAIL). Disjoint from #5085 (complexity lens). The gate grows as bind/branch/loop subjects get rostered later. Co-authored-by: Brian Searls <briansrls@gmail.com> Co-authored-by: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
6 tasks done
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
Gate CI on the complexity lens (
src/v2/lens/complexity.dag) by-execution.The lens is the asymptotic projection of
lens/cost.dag'sSymbolicCost(ratifiedU2: it consumes
cost_lensand never re-derives cost). It had five witness filesunder
src/v2/lens/complexity/that declaredexpected_*claims and*_actual_*helpers — but no
test fnBool assertion, and weren't named*_test.dag. Thelive CI gate is
claim_batch --roster-from-discovery, which discoverstest fnwitnesses in
*_test.dagacrosssrc/v2. So discovery skipped them: the lens wasspecified without execution (the §5 trap). (The hand-roster in
src/v2/workflow/lens_ci_gate.dagthat references the lens is no longer consumed byanything — it's a dead leftover from the pre-discovery gate; left untouched here.)
This converts four witnesses to discoverable
test fn*_test.dagform, assertingthe lens output against the declared expectation:
map_id— Cardinality(Transform) →LinearCost/ linear complexity.nested— nested Cardinality → product cost / multidimensional quadraticbound over two distinct size variables.
while_external_condition— fail-closed (§5): a Loop with an undeclared boundmust
Violate, never fabricate a finite bound; the projection propagates theViolation.
algebra_receipts— degree-4 product algebra (two degree-2 polynomials overdistinct variables) and variable-sensitive dominance (two linear bounds over
different variables are incomparable).
Each assertion is
actual == declared_expected, structurally discriminating (aRED control comparing the linear cost against
zero_cost()returns false/exit 1).Finding (not fixed here, out of scope)
The fifth witness,
typescript_wave2a_type_alias_task, declared a linearexpectation that is wrong: the lens actually projects constant complexity for
that subject — a
Cardinalityover a zero-cost emitted record body, becausecost.dag'sIterativeCostmultiplies the linear traversal base by the zero-costbody → zero. Whether
IterativeCostshould preserve the linear traversal term whenthe body is zero-cost is a
cost.dagmodeling question (U2: not my authority tore-derive cost). Left as-is (reverted to its original ungated descriptive form) and
flagged for a cost-model review rather than cementing a debatable behavior.
Test plan
claim_batch --source-root src/v2 --roster-from-discovery --scan-dir src/v2/test(the CI floor): 186 witnesses passed, 0 FAIL (was 178; +8 new complexity-lens
witnesses now discovered and green).
gunbc run ... --claim-run: all 8 green; RED control confirms theequality assertions discriminate.
Closes #5085 work item (node://adhoc-191c6374-90e).