From 85f4d6ff03dcf89ccb3f458bd959e6c197a1ba07 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Thu, 2 Jul 2026 20:12:57 +0000 Subject: [PATCH 1/7] WIP: STRUCTURAL-QUADRATIC WALLS (not a ratchet): make the OBVIOUS, DECIDABLE --- dsl/gunbc/plan_registry_batch_g.dag | 4 +- dsl/gunbc/plans/expressibility_frontier.dag | 2 +- ...ructural_quadratic_wall_coverage_audit.dag | 65 +++++++++++++++++++ 3 files changed, 69 insertions(+), 2 deletions(-) create mode 100644 dsl/gunbc/plans/structural_quadratic_wall_coverage_audit.dag diff --git a/dsl/gunbc/plan_registry_batch_g.dag b/dsl/gunbc/plan_registry_batch_g.dag index a996cb1683b..dfff559d88e 100644 --- a/dsl/gunbc/plan_registry_batch_g.dag +++ b/dsl/gunbc/plan_registry_batch_g.dag @@ -12,6 +12,7 @@ import gunbc.plans.representation_minimization { representation_minimization_pla import gunbc.plans.reference_grounding_migration { reference_grounding_migration_plan } import gunbc.plans.typescript_gap_census { typescript_gap_census_plan } import gunbc.plans.fleet_acceptance_criteria { fleet_acceptance_criteria_plan } +import gunbc.plans.structural_quadratic_wall_coverage_audit { structural_quadratic_wall_coverage_audit_plan } data batch_g_plans: List = [ ci_humming_plan, @@ -24,5 +25,6 @@ data batch_g_plans: List = [ representation_minimization_plan, reference_grounding_migration_plan, typescript_gap_census_plan, - fleet_acceptance_criteria_plan + fleet_acceptance_criteria_plan, + structural_quadratic_wall_coverage_audit_plan ] diff --git a/dsl/gunbc/plans/expressibility_frontier.dag b/dsl/gunbc/plans/expressibility_frontier.dag index 06218cf74b4..6bc0c0878a0 100644 --- a/dsl/gunbc/plans/expressibility_frontier.dag +++ b/dsl/gunbc/plans/expressibility_frontier.dag @@ -56,7 +56,7 @@ fn expressibility_frontier_body() -> List { }, p(text: "The reading: anemic-modeling and complexity are not analogous by coincidence — they are **two samples of one structure**. Each has a constructive core (①), a detectable-but-not-yet-walled middle (②), and an undecidable tail (③) that is honestly review-bound forever. The win in each is the **same move**: drag instances leftward — review → lens → construction — and *stop* at the decidability boundary."), h2(text: "4. The methodology (and its two failure modes)"), - p(text: "For any discipline D we propose to enforce: **partition D's instances into ① ② ③ *before* building enforcement.** The partition is the deliverable; the gate is downstream of it."), + p(text: "For any discipline D we propose to enforce: **partition D's instances into ① ② ③ *before* building enforcement.** The partition is the deliverable; the gate is downstream of it. The worked instance for algorithmic complexity is the [structural-quadratic wall coverage audit](structural-quadratic-wall-coverage-audit.md) — every live cost/complexity mechanism located on these three regions, with an execution receipt."), p(text: "The two ways to get the partition wrong are exactly DESIGN's two named traps:"), ul(items: [ li(text: "**Region ③ priced as ①** → the **\"never\" trap** (§5): a ratchet sold as a wall. You build a \"gate\" that can never be complete (optimality, leaf-decomposition), then either it silently lets things through (coverage-by-illusion) or it grows without bound chasing completeness (the **purity trap**, §6 — the economic twin). Tell: the gate's success criterion contains \"never\" over an undecidable set."), diff --git a/dsl/gunbc/plans/structural_quadratic_wall_coverage_audit.dag b/dsl/gunbc/plans/structural_quadratic_wall_coverage_audit.dag new file mode 100644 index 00000000000..5a5f94ece55 --- /dev/null +++ b/dsl/gunbc/plans/structural_quadratic_wall_coverage_audit.dag @@ -0,0 +1,65 @@ +module gunbc.plans.structural_quadratic_wall_coverage_audit + +import gunbc.plan { Plan, DissolutionTrigger, HasTrigger } +import std.markdown { MarkdownBlock, TableBlock, AlignNone } +import gunbc.plans.md_helpers { h2, h3, p, li, ul, ol, quote, cell, row } + +fn structural_quadratic_wall_coverage_audit_body() -> List { + [ + quote(blocks: [ + p(text: "Coverage audit + execution receipt (DELIVERABLE 1 of the structural-quadratic-wall lane), authored FIRST so the wall decision is *determined by the census, not searched* (the expressibility-frontier discipline: partition into wall / lens-residue / review BEFORE building enforcement). Goal of the lane: make the OBVIOUS, DECIDABLE bad complexity shapes fail-closed. NON-goals (stated by the brief): a general complexity oracle, and a cost-inference algebra. DESIGN refs: SS1 (displaced cost = time), SS5 (fail-closed; construction over validation; the \"never\" trap), SS6 (lenses are residue; coverage-by-illusion; the purity trap). This is the concrete instance-census under [expressibility-frontier](expressibility-frontier.md)'s \"algorithmic complexity\" column."), + ]), + h2(text: "1. What this audits, and the one question it answers"), + p(text: "The brief orders the census first. The question it must answer is not \"how do we detect quadratics\" but: **is a NEW structural-quadratic wall even on-dial, or is the decidable class already walled and the residue already correctly classified?** ROADMAP SS4 shelves the complexity-gate family explicitly (\"a new wall must displace a measured cost on a pillar path to un-shelve\"), so the census must locate every existing mechanism against the SS5 trichotomy and report what is already covered before proposing anything."), + p(text: "Method: inventory every mechanism that models, gates, budgets, or ratchets computational cost / algorithmic complexity / resource use; classify each as a WALL (fail-closed, bad state unwritable or errors), a RATCHET (a committed threshold that can be bumped), a RESIDUE LENS (a Bool check that concedes the bad state is writable), an AUDIT (emit-only, no gate), or INERT (machinery exists, nothing gates on it); record whether it is FLOOR-ENROLLED (a real consumer runs it green-by-execution); and mark whether it addresses STRUCTURAL/algorithmic complexity or merely RESOURCE budgeting."), + h2(text: "2. Execution receipt"), + p(text: "The one whole-corpus mechanism that runs today is the emit-only `complexity_linearity_audit` bin (a syntactic proxy, NOT floor-enrolled). Ran it against main at commit `6e881a11` via `ctrl-build -- cargo run --bin complexity_linearity_audit` (BuildBuddy remote, exit 0):"), + quote(blocks: [ + p(text: "scanned 1132 file(s), parsed 1132, 10212 fn(s), 428 syntactic finding(s). cost syntactic proxy (Node.body walk): `syntactic_high_match_fanout` = 22 site(s). wildcard arms: total=406 on_roster=75 off_roster=331; triage kernel-permanent=52, migration-debt=23, closed-coproduct-debt=3, open-domain=328. resolved-half roster proxies: non_fold_residue total=78 unrostered=3, inert_carrier inert=12."), + ]), + p(text: "Reading of the receipt: the whole-corpus mechanism that actually executes is a *syntactic* proxy (match-fanout, wildcard arms) standing in for cost until fn-body reflection grounds (blocked on `decl_facts(roots)` #5966 and compile-graph access gunbc#5364). Its 22 `syntactic_high_match_fanout` hits are a match-count heuristic, NOT an asymptotic-class verdict. The REAL asymptotic engine (`src/v2/lens/cost.dag`, next section) is floor-enrolled but roster-bound, so it never walks these 1132 files. That gap -- whole-corpus reach vs. real asymptotic verdict -- is the entire subject of the lane."), + h2(text: "3. The inventory"), + TableBlock { + header: row(cells: [cell(text: "Mechanism"), cell(text: "Carrier"), cell(text: "Measures"), cell(text: "Class"), cell(text: "Floor?"), cell(text: "Struct/Resource")]), + alignments: [AlignNone, AlignNone, AlignNone, AlignNone, AlignNone, AlignNone], + rows: [ + row(cells: [cell(text: "symbolic cost engine"), cell(text: "`src/v2/lens/cost.dag` (`SymbolicCost`, `asymptotic_class_of_cost`, `cost_lens`)"), cell(text: "asymptotic class Constant..Polynomial{deg}..Factorial/Unknown, folded over the Node kernel; loops lower to an iteration product (Linear x Linear -> Poly{2})"), cell(text: "**WALL** (`WallNow`; `UnknownCost` fails to top)"), cell(text: "YES (by exec, `cost/*_test.dag`)"), cell(text: "STRUCTURAL")]), + row(cells: [cell(text: "complexity lens"), cell(text: "`src/v2/lens/complexity.dag`"), cell(text: "projects SymbolicCost -> ComplexityBound over a curated roster"), cell(text: "RESIDUE / RATCHET (`RatchetForever`; `complexity_variables_admits` returns true -> concedes writability; roster-bound)"), cell(text: "YES (by exec)"), cell(text: "STRUCTURAL")]), + row(cells: [cell(text: "complexity-lowering catalog"), cell(text: "`src/v2/lens/complexity_lowering.dag` (`loop_invariant_hoist`, `catalog_is_sound`)"), cell(text: "whether a cost class is strictly lowerable O(n^2)->O(n); soundness = every rule strictly lowers"), cell(text: "RESIDUE + WALL-after-grounding (catalog soundness is the wall)"), cell(text: "YES (by exec)"), cell(text: "STRUCTURAL")]), + row(cells: [cell(text: "intent-linearity lens"), cell(text: "`src/v2/lens/intent_linearity.dag`"), cell(text: "simulated/unrollable chains + lowerable-cost nodes across term-chain / type-forest / import-graph"), cell(text: "WALL-after-grounding (`closure_drift` wall)"), cell(text: "PARTIAL"), cell(text: "STRUCTURAL")]), + row(cells: [cell(text: "synthesis / lower-bound gap"), cell(text: "`src/v2/lens/synthesis.dag`"), cell(text: "realization cost vs declared relation's structural lower bound"), cell(text: "RESIDUE / AUDIT (`AdvisoryLens`, never gates -- the SS5 region-(3) residue: optimality is Rice-undecidable)"), cell(text: "tests run; lens advisory"), cell(text: "STRUCTURAL (non-gating)")]), + row(cells: [cell(text: "complexity_linearity_audit bin"), cell(text: "`src/v1/stage0/src/bin/complexity_linearity_audit.rs` + `_project.rs`"), cell(text: "syntactic match-wildcard arms + `syntactic_high_match_fanout` (parse-only whole-corpus proxy)"), cell(text: "AUDIT / emit-only (exit 0 unless `--fail-on-findings`)"), cell(text: "NO (scaffold, until #5966)"), cell(text: "SYNTACTIC PROXY")]), + row(cells: [cell(text: "termination / DescentEvidence"), cell(text: "`dsl/std/termination.dag`; v1 checker `src/v1/complexity.dag` + `CostBound`/`PolyCost` in `dsl/std/induction.dag`"), cell(text: "well-founded descent; poly cost bound; `Strict|NonIncreasing|DescentUnknown` bounded lattice, bottom fails closed"), cell(text: "**WALL** primitive (`DescentUnknown` blocks a proof)"), cell(text: "via v1-seed consumers"), cell(text: "STRUCTURAL (termination)")]), + row(cells: [cell(text: "realization_width / memory_bounded_fit_count"), cell(text: "`dsl/std/realization_width.dag`; actuator `cli_run.rs` `spawn_width_cap`"), cell(text: "memory-bounded parallel width = budget / per-shard peak; caps spawn width so co-resident VmHWM <= cgroup cap"), cell(text: "**WALL** / actuator (real floor consumer, fail-closed under-parallelize)"), cell(text: "YES (real consumer)"), cell(text: "RESOURCE (memory)")]), + row(cells: [cell(text: "budget tree (accounting)"), cell(text: "`dsl/extdeps/accounting/budget.dag` (`admit_line_item`); `dsl/product/budget_tree.dag` (`node_conserves`); `dsl/gunbc/ci_budget_tree.dag`"), cell(text: "capped-resource -> line-item admission (Memory); conservation Bool"), cell(text: "admission construction (over-cap unwritable on the admit path) + RESIDUE (`node_conserves` for raw literals)"), cell(text: "YES (`*budget*_witness_test.dag`)"), cell(text: "RESOURCE (memory/money)")]), + row(cells: [cell(text: "node_wall_clock_ratchet"), cell(text: "`dsl/gunbc/test_node_wall_clock_ratchet.dag`"), cell(text: "committed roster of test names permitted to emit wall-clock/time warnings"), cell(text: "RATCHET (bumpable roster)"), cell(text: "via testgen oracle"), cell(text: "RESOURCE (wall-clock)")]), + row(cells: [cell(text: "EffortBudget (op-count)"), cell(text: "prose only in `dsl/gunbc/plans/budget_tree.dag`; nearest live: `estimate_expr_size` `budget: Int` guard in `src/v1/complexity.dag`"), cell(text: "op-count recursion budget"), cell(text: "INERT (no `EffortBudget` type exists in the tree)"), cell(text: "NO"), cell(text: "RESOURCE (op-count)")]), + row(cells: [cell(text: "algebraic-rewrite optimization"), cell(text: "`dsl/gunbc/plans/algebraic_rewrite_optimization.dag`"), cell(text: "design spec for an O(n^2)->O(n) rewrite catalog + `Unknown` dissolution"), cell(text: "INERT / design-only (POST-STABILITY; no rewrite rows exist)"), cell(text: "NO"), cell(text: "STRUCTURAL (unbuilt)")]), + row(cells: [cell(text: "resolver-pathology quadratics"), cell(text: "targets in `v1_compiler_infer.rs` `build_type_env` / `seed_kernel_intern_table`; tracked `dsl/gunbc/plans/representation_minimization.dag`"), cell(text: "whole-ancestry-per-module resolve, `func_env.sigs` module x closure-width, per-module intern_table copy"), cell(text: "AUDIT / MEASURED (VmHWM probe; being killed by sibling lanes) -- NO shape gate against reintroduction"), cell(text: "symptom bounded by the memory WALL (#8), not the shape"), cell(text: "RESOURCE symptom, STRUCTURAL root")]), + ], + }, + h2(text: "4. The verdict -- the structural-quadratic class partitioned"), + p(text: "Placing the census on the expressibility frontier's three regions for algorithmic complexity yields a clean, and somewhat surprising, result: **the decidable structural-quadratic WALL already exists.**"), + ul(items: [ + li(text: "**Region (1) -- Wall (already built).** Budget-dominance over the symbolic cost fold is decidable and IS walled: `cost.dag` `cost_lens` carries `WallNow`, folds `SymbolicCost` over the Node kernel, and detects Poly{2} structurally (Linear x Linear). `termination.dag` + the v1 `DescentEvidence` checker wall non-termination fail-closed. The memory actuator (`realization_width`) walls the resource symptom. So the OBVIOUS decidable quadratic *shape* -- a per-element loop whose body is itself linear in the whole input -- is already caught where the cost engine reaches."), + li(text: "**Region (2) -- Lens-residue (the real gap).** The cost wall is **roster-bound** -- it does not walk the 1132-file corpus. Whole-corpus reach (ROADMAP SS3 `3-gates-whole`) is a SS5 residue that is *decidable but not yet unwritable*, and it is **blocked on the same reflection host-builtin** (`decl_facts(roots)` #5966, compile-graph gunbc#5364) that the emit-only audit bin is scaffolding around. The resolver-pathology quadratics live here too: measured, being killed by sibling lanes (bold-ibex-109 compositional `build_type_env`; representation-minimization), but with NO structural wall against *reintroduction* -- the floor memory cap bounds the symptom, not the shape."), + li(text: "**Region (3) -- Review forever.** Optimality (\"is this minimal cost?\") is Rice-undecidable; synthesis (\"produce a faster version\") has no constructive patch. `synthesis.dag` is honestly `AdvisoryLens` / never-gates, and `complexity.dag` is honestly `RatchetForever`. Pricing either as a wall would be the SS5 \"never\" trap."), + ]), + h2(text: "5. Recommendation (what the census determines about the wall)"), + ol(items: [ + li(text: "**Do NOT build a new complexity oracle or cost-inference algebra.** The brief forbids both, and the census confirms the asymptotic engine already exists (`cost.dag`); a second one would be a SS3 fork of the cost authority."), + li(text: "**The only on-dial structural-quadratic wall increment is extending `cost.dag`'s reach whole-corpus** -- but that is region-(2) residue **blocked on `decl_facts(roots)` #5966 / gunbc#5364**, the identical blocker that shelves ROADMAP SS3 `3-gates-whole`. Until that host-builtin grounds, a whole-corpus asymptotic wall cannot be built without duplicating the emit-only syntactic proxy, which is exactly the scaffold to be dissolved, not extended."), + li(text: "**The measured-cost residue with the strongest pillar claim** is a *reintroduction wall* for the resolver-pathology quadratic shape once the sibling lanes land their fix -- a structural fence so the killed O(corpus^2) `build_type_env` shape cannot be re-authored. This is the single candidate that could \"displace a measured cost on a pillar path\" (ROADMAP SS4's un-shelve bar), and it should be sequenced AFTER bold-ibex-109 lands, co-designed with that lane, not raced ahead of it."), + li(text: "**Net:** DELIVERABLE 1 says the decidable class is already walled where reflection reaches; the wall lane's real content is not a new detector but (a) the blocked whole-corpus reach and (b) a post-fix reintroduction fence -- both gated on other lanes. Escalate the sequencing decision rather than improvising a redundant oracle."), + ]), + ] +} + +data structural_quadratic_wall_coverage_audit_plan: Plan = Plan { + slug: "structural-quadratic-wall-coverage-audit", + title: "Structural-quadratic wall -- coverage audit and execution receipt", + body: structural_quadratic_wall_coverage_audit_body(), + dissolution: HasTrigger { + text: "Dissolves when the whole-corpus asymptotic cost gate grounds (`decl_facts(roots)` #5966 + compile-graph gunbc#5364 land, flipping cost.dag from roster-bound to whole-corpus): at that point the region-(2) \"un-walled residue\" rows close, the emit-only `complexity_linearity_audit` bin is deleted, and this census is superseded by the live gate's own coverage report. Also re-run the section-2 receipt whenever a sibling lane lands a resolver-pathology quadratic fix, to confirm the reintroduction-fence candidate is still measured-live." + } +} From e4b02e67f8f0c308077d83bd39f572c84dcee3b2 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Thu, 2 Jul 2026 20:16:59 +0000 Subject: [PATCH 2/7] Structural-quadratic walls DELIVERABLE 1: complexity-mechanism coverage audit + execution receipt MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Census-first, per the brief: inventory every complexity mechanism (gate / lens / budget / ratchet) and locate each on the expressibility-frontier trichotomy (wall / lens-residue / review) BEFORE proposing any new wall. New modeled plan gunbc.plans.structural_quadratic_wall_coverage_audit (projected to docs/plans/structural-quadratic-wall-coverage-audit.md, registered in plan_registry_batch_g, linked from the frontier plan so it is not an orphan doc). Contents: - Execution receipt: ran the emit-only complexity_linearity_audit bin over main@6e881a11 (1132 files, 10212 fns, 428 syntactic findings; cost proxy fired on 22 sites; wildcard arms 406). - 13-row inventory table classifying every cost/complexity/budget mechanism by class, floor-enrollment, and structural-vs-resource. - Verdict: the decidable structural-quadratic WALL already exists (src/v2/lens/cost.dag WallNow + termination DescentEvidence + the memory actuator), but is roster-bound; whole-corpus reach is region-(2) residue blocked on the same decl_facts(roots) #5966 / gunbc#5364 reflection that shelves ROADMAP §3 `3-gates-whole`. Recommendation: build no new oracle; the only on-dial increment is a post-fix reintroduction fence for the resolver-pathology quadratic, sequenced AFTER the sibling lanes land. Co-Authored-By: Claude Opus 4.8 (1M context) --- .githooks/pre-push | 1 + docs/plans/expressibility-frontier.md | 2 +- ...tructural-quadratic-wall-coverage-audit.md | 54 +++++++++++++++++++ ...ructural_quadratic_wall_coverage_audit.dag | 4 +- 4 files changed, 58 insertions(+), 3 deletions(-) create mode 100644 docs/plans/structural-quadratic-wall-coverage-audit.md diff --git a/.githooks/pre-push b/.githooks/pre-push index 90d7279772d..1dc91d086e3 100755 --- a/.githooks/pre-push +++ b/.githooks/pre-push @@ -86,6 +86,7 @@ fresh_artifact_path() { docs/plans/reference-grounding-migration.md*) return 0 ;; docs/plans/typescript-gap-census.md*) return 0 ;; docs/plans/fleet-acceptance-criteria.md*) return 0 ;; + docs/plans/structural-quadratic-wall-coverage-audit.md*) return 0 ;; dsl/**) return 0 ;; src/v2/**) return 0 ;; esac diff --git a/docs/plans/expressibility-frontier.md b/docs/plans/expressibility-frontier.md index f3797acba1a..719a6c4475b 100644 --- a/docs/plans/expressibility-frontier.md +++ b/docs/plans/expressibility-frontier.md @@ -52,7 +52,7 @@ The reading: anemic-modeling and complexity are not analogous by coincidence — ## 4. The methodology (and its two failure modes) -For any discipline D we propose to enforce: **partition D's instances into ① ② ③ *before* building enforcement.** The partition is the deliverable; the gate is downstream of it. +For any discipline D we propose to enforce: **partition D's instances into ① ② ③ *before* building enforcement.** The partition is the deliverable; the gate is downstream of it. The worked instance for algorithmic complexity is the [structural-quadratic wall coverage audit](structural-quadratic-wall-coverage-audit.md) — every live cost/complexity mechanism located on these three regions, with an execution receipt. The two ways to get the partition wrong are exactly DESIGN's two named traps: diff --git a/docs/plans/structural-quadratic-wall-coverage-audit.md b/docs/plans/structural-quadratic-wall-coverage-audit.md new file mode 100644 index 00000000000..04ca48fafb9 --- /dev/null +++ b/docs/plans/structural-quadratic-wall-coverage-audit.md @@ -0,0 +1,54 @@ +# Structural-quadratic wall -- coverage audit and execution receipt + +> Coverage audit + execution receipt (DELIVERABLE 1 of the structural-quadratic-wall lane), authored FIRST so the wall decision is *determined by the census, not searched* (the expressibility-frontier discipline: partition into wall / lens-residue / review BEFORE building enforcement). Goal of the lane: make the OBVIOUS, DECIDABLE bad complexity shapes fail-closed. NON-goals (stated by the brief): a general complexity oracle, and a cost-inference algebra. DESIGN refs: SS1 (displaced cost = time), SS5 (fail-closed; construction over validation; the "never" trap), SS6 (lenses are residue; coverage-by-illusion; the purity trap). This is the concrete instance-census under [expressibility-frontier](expressibility-frontier.md)'s "algorithmic complexity" column. + +## 1. What this audits, and the one question it answers + +The brief orders the census first. The question it must answer is not "how do we detect quadratics" but: **is a NEW structural-quadratic wall even on-dial, or is the decidable class already walled and the residue already correctly classified?** ROADMAP SS4 shelves the complexity-gate family explicitly ("a new wall must displace a measured cost on a pillar path to un-shelve"), so the census must locate every existing mechanism against the SS5 trichotomy and report what is already covered before proposing anything. + +Method: inventory every mechanism that models, gates, budgets, or ratchets computational cost / algorithmic complexity / resource use; classify each as a WALL (fail-closed, bad state unwritable or errors), a RATCHET (a committed threshold that can be bumped), a RESIDUE LENS (a Bool check that concedes the bad state is writable), an AUDIT (emit-only, no gate), or INERT (machinery exists, nothing gates on it); record whether it is FLOOR-ENROLLED (a real consumer runs it green-by-execution); and mark whether it addresses STRUCTURAL/algorithmic complexity or merely RESOURCE budgeting. + +## 2. Execution receipt + +The one whole-corpus mechanism that runs today is the emit-only `complexity_linearity_audit` bin (a syntactic proxy, NOT floor-enrolled). Ran it against main at commit `6e881a11` via `ctrl-build -- cargo run --bin complexity_linearity_audit` (BuildBuddy remote, exit 0): + +> scanned 1132 file(s), parsed 1132, 10212 fn(s), 428 syntactic finding(s). cost syntactic proxy (Node.body walk): `syntactic_high_match_fanout` = 22 site(s). wildcard arms: total=406 on_roster=75 off_roster=331; triage kernel-permanent=52, migration-debt=23, closed-coproduct-debt=3, open-domain=328. resolved-half roster proxies: non_fold_residue total=78 unrostered=3, inert_carrier inert=12. + +Reading of the receipt: the whole-corpus mechanism that actually executes is a *syntactic* proxy (match-fanout, wildcard arms) standing in for cost until fn-body reflection grounds (blocked on `decl_facts(roots)` #5966 and compile-graph access gunbc#5364). Its 22 `syntactic_high_match_fanout` hits are a match-count heuristic, NOT an asymptotic-class verdict. The REAL asymptotic engine (`src/v2/lens/cost.dag`, next section) is floor-enrolled but roster-bound, so it never walks these 1132 files. That gap -- whole-corpus reach vs. real asymptotic verdict -- is the entire subject of the lane. + +## 3. The inventory + +| Mechanism | Carrier | Measures | Class | Floor? | Struct/Resource | +| --- | --- | --- | --- | --- | --- | +| symbolic cost engine | `src/v2/lens/cost.dag` (`SymbolicCost`, `asymptotic_class_of_cost`, `cost_lens`) | asymptotic class Constant..Polynomial(deg)..Factorial/Unknown, folded over the Node kernel; loops lower to an iteration product (Linear x Linear -> Poly(2)) | **WALL** (`WallNow`; `UnknownCost` fails to top) | YES (by exec, `cost/*_test.dag`) | STRUCTURAL | +| complexity lens | `src/v2/lens/complexity.dag` | projects SymbolicCost -> ComplexityBound over a curated roster | RESIDUE / RATCHET (`RatchetForever`; `complexity_variables_admits` returns true -> concedes writability; roster-bound) | YES (by exec) | STRUCTURAL | +| complexity-lowering catalog | `src/v2/lens/complexity_lowering.dag` (`loop_invariant_hoist`, `catalog_is_sound`) | whether a cost class is strictly lowerable O(n^2)->O(n); soundness = every rule strictly lowers | RESIDUE + WALL-after-grounding (catalog soundness is the wall) | YES (by exec) | STRUCTURAL | +| intent-linearity lens | `src/v2/lens/intent_linearity.dag` | simulated/unrollable chains + lowerable-cost nodes across term-chain / type-forest / import-graph | WALL-after-grounding (`closure_drift` wall) | PARTIAL | STRUCTURAL | +| synthesis / lower-bound gap | `src/v2/lens/synthesis.dag` | realization cost vs declared relation's structural lower bound | RESIDUE / AUDIT (`AdvisoryLens`, never gates -- the SS5 region-(3) residue: optimality is Rice-undecidable) | tests run; lens advisory | STRUCTURAL (non-gating) | +| complexity_linearity_audit bin | `src/v1/stage0/src/bin/complexity_linearity_audit.rs` + `_project.rs` | syntactic match-wildcard arms + `syntactic_high_match_fanout` (parse-only whole-corpus proxy) | AUDIT / emit-only (exit 0 unless `--fail-on-findings`) | NO (scaffold, until #5966) | SYNTACTIC PROXY | +| termination / DescentEvidence | `dsl/std/termination.dag`; v1 checker `src/v1/complexity.dag` + `CostBound`/`PolyCost` in `dsl/std/induction.dag` | well-founded descent; poly cost bound; `Strict|NonIncreasing|DescentUnknown` bounded lattice, bottom fails closed | **WALL** primitive (`DescentUnknown` blocks a proof) | via v1-seed consumers | STRUCTURAL (termination) | +| realization_width / memory_bounded_fit_count | `dsl/std/realization_width.dag`; actuator `cli_run.rs` `spawn_width_cap` | memory-bounded parallel width = budget / per-shard peak; caps spawn width so co-resident VmHWM <= cgroup cap | **WALL** / actuator (real floor consumer, fail-closed under-parallelize) | YES (real consumer) | RESOURCE (memory) | +| budget tree (accounting) | `dsl/extdeps/accounting/budget.dag` (`admit_line_item`); `dsl/product/budget_tree.dag` (`node_conserves`); `dsl/gunbc/ci_budget_tree.dag` | capped-resource -> line-item admission (Memory); conservation Bool | admission construction (over-cap unwritable on the admit path) + RESIDUE (`node_conserves` for raw literals) | YES (`*budget*_witness_test.dag`) | RESOURCE (memory/money) | +| node_wall_clock_ratchet | `dsl/gunbc/test_node_wall_clock_ratchet.dag` | committed roster of test names permitted to emit wall-clock/time warnings | RATCHET (bumpable roster) | via testgen oracle | RESOURCE (wall-clock) | +| EffortBudget (op-count) | prose only in `dsl/gunbc/plans/budget_tree.dag`; nearest live: `estimate_expr_size` `budget: Int` guard in `src/v1/complexity.dag` | op-count recursion budget | INERT (no `EffortBudget` type exists in the tree) | NO | RESOURCE (op-count) | +| algebraic-rewrite optimization | `dsl/gunbc/plans/algebraic_rewrite_optimization.dag` | design spec for an O(n^2)->O(n) rewrite catalog + `Unknown` dissolution | INERT / design-only (POST-STABILITY; no rewrite rows exist) | NO | STRUCTURAL (unbuilt) | +| resolver-pathology quadratics | targets in `v1_compiler_infer.rs` `build_type_env` / `seed_kernel_intern_table`; tracked `dsl/gunbc/plans/representation_minimization.dag` | whole-ancestry-per-module resolve, `func_env.sigs` module x closure-width, per-module intern_table copy | AUDIT / MEASURED (VmHWM probe; being killed by sibling lanes) -- NO shape gate against reintroduction | symptom bounded by the memory WALL (#8), not the shape | RESOURCE symptom, STRUCTURAL root | + +## 4. The verdict -- the structural-quadratic class partitioned + +Placing the census on the expressibility frontier's three regions for algorithmic complexity yields a clean, and somewhat surprising, result: **the decidable structural-quadratic WALL already exists.** + +- **Region (1) -- Wall (already built).** Budget-dominance over the symbolic cost fold is decidable and IS walled: `cost.dag` `cost_lens` carries `WallNow`, folds `SymbolicCost` over the Node kernel, and detects Poly(2) structurally (Linear x Linear). `termination.dag` + the v1 `DescentEvidence` checker wall non-termination fail-closed. The memory actuator (`realization_width`) walls the resource symptom. So the OBVIOUS decidable quadratic *shape* -- a per-element loop whose body is itself linear in the whole input -- is already caught where the cost engine reaches. +- **Region (2) -- Lens-residue (the real gap).** The cost wall is **roster-bound** -- it does not walk the 1132-file corpus. Whole-corpus reach (ROADMAP SS3 `3-gates-whole`) is a SS5 residue that is *decidable but not yet unwritable*, and it is **blocked on the same reflection host-builtin** (`decl_facts(roots)` #5966, compile-graph gunbc#5364) that the emit-only audit bin is scaffolding around. The resolver-pathology quadratics live here too: measured, being killed by sibling lanes (bold-ibex-109 compositional `build_type_env`; representation-minimization), but with NO structural wall against *reintroduction* -- the floor memory cap bounds the symptom, not the shape. +- **Region (3) -- Review forever.** Optimality ("is this minimal cost?") is Rice-undecidable; synthesis ("produce a faster version") has no constructive patch. `synthesis.dag` is honestly `AdvisoryLens` / never-gates, and `complexity.dag` is honestly `RatchetForever`. Pricing either as a wall would be the SS5 "never" trap. + +## 5. Recommendation (what the census determines about the wall) + +1. **Do NOT build a new complexity oracle or cost-inference algebra.** The brief forbids both, and the census confirms the asymptotic engine already exists (`cost.dag`); a second one would be a SS3 fork of the cost authority. +2. **The only on-dial structural-quadratic wall increment is extending `cost.dag`'s reach whole-corpus** -- but that is region-(2) residue **blocked on `decl_facts(roots)` #5966 / gunbc#5364**, the identical blocker that shelves ROADMAP SS3 `3-gates-whole`. Until that host-builtin grounds, a whole-corpus asymptotic wall cannot be built without duplicating the emit-only syntactic proxy, which is exactly the scaffold to be dissolved, not extended. +3. **The measured-cost residue with the strongest pillar claim** is a *reintroduction wall* for the resolver-pathology quadratic shape once the sibling lanes land their fix -- a structural fence so the killed O(corpus^2) `build_type_env` shape cannot be re-authored. This is the single candidate that could "displace a measured cost on a pillar path" (ROADMAP SS4's un-shelve bar), and it should be sequenced AFTER bold-ibex-109 lands, co-designed with that lane, not raced ahead of it. +4. **Net:** DELIVERABLE 1 says the decidable class is already walled where reflection reaches; the wall lane's real content is not a new detector but (a) the blocked whole-corpus reach and (b) a post-fix reintroduction fence -- both gated on other lanes. Escalate the sequencing decision rather than improvising a redundant oracle. + +## Dissolution trigger (DESIGN §6) + +Dissolves when the whole-corpus asymptotic cost gate grounds (`decl_facts(roots)` #5966 + compile-graph gunbc#5364 land, flipping cost.dag from roster-bound to whole-corpus): at that point the region-(2) "un-walled residue" rows close, the emit-only `complexity_linearity_audit` bin is deleted, and this census is superseded by the live gate's own coverage report. Also re-run the section-2 receipt whenever a sibling lane lands a resolver-pathology quadratic fix, to confirm the reintroduction-fence candidate is still measured-live. diff --git a/dsl/gunbc/plans/structural_quadratic_wall_coverage_audit.dag b/dsl/gunbc/plans/structural_quadratic_wall_coverage_audit.dag index 5a5f94ece55..08be5df93fc 100644 --- a/dsl/gunbc/plans/structural_quadratic_wall_coverage_audit.dag +++ b/dsl/gunbc/plans/structural_quadratic_wall_coverage_audit.dag @@ -23,7 +23,7 @@ fn structural_quadratic_wall_coverage_audit_body() -> List { header: row(cells: [cell(text: "Mechanism"), cell(text: "Carrier"), cell(text: "Measures"), cell(text: "Class"), cell(text: "Floor?"), cell(text: "Struct/Resource")]), alignments: [AlignNone, AlignNone, AlignNone, AlignNone, AlignNone, AlignNone], rows: [ - row(cells: [cell(text: "symbolic cost engine"), cell(text: "`src/v2/lens/cost.dag` (`SymbolicCost`, `asymptotic_class_of_cost`, `cost_lens`)"), cell(text: "asymptotic class Constant..Polynomial{deg}..Factorial/Unknown, folded over the Node kernel; loops lower to an iteration product (Linear x Linear -> Poly{2})"), cell(text: "**WALL** (`WallNow`; `UnknownCost` fails to top)"), cell(text: "YES (by exec, `cost/*_test.dag`)"), cell(text: "STRUCTURAL")]), + row(cells: [cell(text: "symbolic cost engine"), cell(text: "`src/v2/lens/cost.dag` (`SymbolicCost`, `asymptotic_class_of_cost`, `cost_lens`)"), cell(text: "asymptotic class Constant..Polynomial(deg)..Factorial/Unknown, folded over the Node kernel; loops lower to an iteration product (Linear x Linear -> Poly(2))"), cell(text: "**WALL** (`WallNow`; `UnknownCost` fails to top)"), cell(text: "YES (by exec, `cost/*_test.dag`)"), cell(text: "STRUCTURAL")]), row(cells: [cell(text: "complexity lens"), cell(text: "`src/v2/lens/complexity.dag`"), cell(text: "projects SymbolicCost -> ComplexityBound over a curated roster"), cell(text: "RESIDUE / RATCHET (`RatchetForever`; `complexity_variables_admits` returns true -> concedes writability; roster-bound)"), cell(text: "YES (by exec)"), cell(text: "STRUCTURAL")]), row(cells: [cell(text: "complexity-lowering catalog"), cell(text: "`src/v2/lens/complexity_lowering.dag` (`loop_invariant_hoist`, `catalog_is_sound`)"), cell(text: "whether a cost class is strictly lowerable O(n^2)->O(n); soundness = every rule strictly lowers"), cell(text: "RESIDUE + WALL-after-grounding (catalog soundness is the wall)"), cell(text: "YES (by exec)"), cell(text: "STRUCTURAL")]), row(cells: [cell(text: "intent-linearity lens"), cell(text: "`src/v2/lens/intent_linearity.dag`"), cell(text: "simulated/unrollable chains + lowerable-cost nodes across term-chain / type-forest / import-graph"), cell(text: "WALL-after-grounding (`closure_drift` wall)"), cell(text: "PARTIAL"), cell(text: "STRUCTURAL")]), @@ -41,7 +41,7 @@ fn structural_quadratic_wall_coverage_audit_body() -> List { h2(text: "4. The verdict -- the structural-quadratic class partitioned"), p(text: "Placing the census on the expressibility frontier's three regions for algorithmic complexity yields a clean, and somewhat surprising, result: **the decidable structural-quadratic WALL already exists.**"), ul(items: [ - li(text: "**Region (1) -- Wall (already built).** Budget-dominance over the symbolic cost fold is decidable and IS walled: `cost.dag` `cost_lens` carries `WallNow`, folds `SymbolicCost` over the Node kernel, and detects Poly{2} structurally (Linear x Linear). `termination.dag` + the v1 `DescentEvidence` checker wall non-termination fail-closed. The memory actuator (`realization_width`) walls the resource symptom. So the OBVIOUS decidable quadratic *shape* -- a per-element loop whose body is itself linear in the whole input -- is already caught where the cost engine reaches."), + li(text: "**Region (1) -- Wall (already built).** Budget-dominance over the symbolic cost fold is decidable and IS walled: `cost.dag` `cost_lens` carries `WallNow`, folds `SymbolicCost` over the Node kernel, and detects Poly(2) structurally (Linear x Linear). `termination.dag` + the v1 `DescentEvidence` checker wall non-termination fail-closed. The memory actuator (`realization_width`) walls the resource symptom. So the OBVIOUS decidable quadratic *shape* -- a per-element loop whose body is itself linear in the whole input -- is already caught where the cost engine reaches."), li(text: "**Region (2) -- Lens-residue (the real gap).** The cost wall is **roster-bound** -- it does not walk the 1132-file corpus. Whole-corpus reach (ROADMAP SS3 `3-gates-whole`) is a SS5 residue that is *decidable but not yet unwritable*, and it is **blocked on the same reflection host-builtin** (`decl_facts(roots)` #5966, compile-graph gunbc#5364) that the emit-only audit bin is scaffolding around. The resolver-pathology quadratics live here too: measured, being killed by sibling lanes (bold-ibex-109 compositional `build_type_env`; representation-minimization), but with NO structural wall against *reintroduction* -- the floor memory cap bounds the symptom, not the shape."), li(text: "**Region (3) -- Review forever.** Optimality (\"is this minimal cost?\") is Rice-undecidable; synthesis (\"produce a faster version\") has no constructive patch. `synthesis.dag` is honestly `AdvisoryLens` / never-gates, and `complexity.dag` is honestly `RatchetForever`. Pricing either as a wall would be the SS5 \"never\" trap."), ]), From dc5d24a329d6e0c29f8cb420c6abb67df3dc7b76 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Thu, 2 Jul 2026 21:35:53 +0000 Subject: [PATCH 3/7] Merge origin/main (dsl/->dag/ rename) into session/silent-ferret-137 Relocate the coverage-audit plan to dag/gunbc/plans/; keep the pre-push freshness entry for docs/plans/structural-quadratic-wall-coverage-audit.md alongside main's dag/** roster. Regen follows to reconcile generated docs. --- .githooks/pre-push | 4 ---- 1 file changed, 4 deletions(-) diff --git a/.githooks/pre-push b/.githooks/pre-push index 34adb217ef3..20afeec3b95 100755 --- a/.githooks/pre-push +++ b/.githooks/pre-push @@ -86,12 +86,8 @@ fresh_artifact_path() { docs/plans/reference-grounding-migration.md*) return 0 ;; docs/plans/typescript-gap-census.md*) return 0 ;; docs/plans/fleet-acceptance-criteria.md*) return 0 ;; -<<<<<<< HEAD docs/plans/structural-quadratic-wall-coverage-audit.md*) return 0 ;; - dsl/**) return 0 ;; -======= dag/**) return 0 ;; ->>>>>>> origin/main src/v2/**) return 0 ;; esac return 1 From dc16b2fe48f5f22e566d197edf211733fd71fea9 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Thu, 2 Jul 2026 21:57:23 +0000 Subject: [PATCH 4/7] =?UTF-8?q?Review=20fix=20(#6162):=20retarget=20audit?= =?UTF-8?q?=20inventory=20carriers=20dsl/->dag/=20(=C2=A73=20grounding)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit main renamed the substrate tree dsl/->dag/; the coverage-audit inventory column still cited dsl/std/*, dsl/extdeps/*, dsl/gunbc/* paths that no longer exist. Retargeted all 10 to dag/ and regenerated the mirror markdown (main_wet). Addresses cursor/composer-2.5 REQUEST_CHANGES on #6162. Co-Authored-By: Claude Opus 4.8 (1M context) --- .../structural_quadratic_wall_coverage_audit.dag | 14 +++++++------- .../structural-quadratic-wall-coverage-audit.md | 14 +++++++------- 2 files changed, 14 insertions(+), 14 deletions(-) diff --git a/dag/gunbc/plans/structural_quadratic_wall_coverage_audit.dag b/dag/gunbc/plans/structural_quadratic_wall_coverage_audit.dag index 08be5df93fc..ea073d7738b 100644 --- a/dag/gunbc/plans/structural_quadratic_wall_coverage_audit.dag +++ b/dag/gunbc/plans/structural_quadratic_wall_coverage_audit.dag @@ -29,13 +29,13 @@ fn structural_quadratic_wall_coverage_audit_body() -> List { row(cells: [cell(text: "intent-linearity lens"), cell(text: "`src/v2/lens/intent_linearity.dag`"), cell(text: "simulated/unrollable chains + lowerable-cost nodes across term-chain / type-forest / import-graph"), cell(text: "WALL-after-grounding (`closure_drift` wall)"), cell(text: "PARTIAL"), cell(text: "STRUCTURAL")]), row(cells: [cell(text: "synthesis / lower-bound gap"), cell(text: "`src/v2/lens/synthesis.dag`"), cell(text: "realization cost vs declared relation's structural lower bound"), cell(text: "RESIDUE / AUDIT (`AdvisoryLens`, never gates -- the SS5 region-(3) residue: optimality is Rice-undecidable)"), cell(text: "tests run; lens advisory"), cell(text: "STRUCTURAL (non-gating)")]), row(cells: [cell(text: "complexity_linearity_audit bin"), cell(text: "`src/v1/stage0/src/bin/complexity_linearity_audit.rs` + `_project.rs`"), cell(text: "syntactic match-wildcard arms + `syntactic_high_match_fanout` (parse-only whole-corpus proxy)"), cell(text: "AUDIT / emit-only (exit 0 unless `--fail-on-findings`)"), cell(text: "NO (scaffold, until #5966)"), cell(text: "SYNTACTIC PROXY")]), - row(cells: [cell(text: "termination / DescentEvidence"), cell(text: "`dsl/std/termination.dag`; v1 checker `src/v1/complexity.dag` + `CostBound`/`PolyCost` in `dsl/std/induction.dag`"), cell(text: "well-founded descent; poly cost bound; `Strict|NonIncreasing|DescentUnknown` bounded lattice, bottom fails closed"), cell(text: "**WALL** primitive (`DescentUnknown` blocks a proof)"), cell(text: "via v1-seed consumers"), cell(text: "STRUCTURAL (termination)")]), - row(cells: [cell(text: "realization_width / memory_bounded_fit_count"), cell(text: "`dsl/std/realization_width.dag`; actuator `cli_run.rs` `spawn_width_cap`"), cell(text: "memory-bounded parallel width = budget / per-shard peak; caps spawn width so co-resident VmHWM <= cgroup cap"), cell(text: "**WALL** / actuator (real floor consumer, fail-closed under-parallelize)"), cell(text: "YES (real consumer)"), cell(text: "RESOURCE (memory)")]), - row(cells: [cell(text: "budget tree (accounting)"), cell(text: "`dsl/extdeps/accounting/budget.dag` (`admit_line_item`); `dsl/product/budget_tree.dag` (`node_conserves`); `dsl/gunbc/ci_budget_tree.dag`"), cell(text: "capped-resource -> line-item admission (Memory); conservation Bool"), cell(text: "admission construction (over-cap unwritable on the admit path) + RESIDUE (`node_conserves` for raw literals)"), cell(text: "YES (`*budget*_witness_test.dag`)"), cell(text: "RESOURCE (memory/money)")]), - row(cells: [cell(text: "node_wall_clock_ratchet"), cell(text: "`dsl/gunbc/test_node_wall_clock_ratchet.dag`"), cell(text: "committed roster of test names permitted to emit wall-clock/time warnings"), cell(text: "RATCHET (bumpable roster)"), cell(text: "via testgen oracle"), cell(text: "RESOURCE (wall-clock)")]), - row(cells: [cell(text: "EffortBudget (op-count)"), cell(text: "prose only in `dsl/gunbc/plans/budget_tree.dag`; nearest live: `estimate_expr_size` `budget: Int` guard in `src/v1/complexity.dag`"), cell(text: "op-count recursion budget"), cell(text: "INERT (no `EffortBudget` type exists in the tree)"), cell(text: "NO"), cell(text: "RESOURCE (op-count)")]), - row(cells: [cell(text: "algebraic-rewrite optimization"), cell(text: "`dsl/gunbc/plans/algebraic_rewrite_optimization.dag`"), cell(text: "design spec for an O(n^2)->O(n) rewrite catalog + `Unknown` dissolution"), cell(text: "INERT / design-only (POST-STABILITY; no rewrite rows exist)"), cell(text: "NO"), cell(text: "STRUCTURAL (unbuilt)")]), - row(cells: [cell(text: "resolver-pathology quadratics"), cell(text: "targets in `v1_compiler_infer.rs` `build_type_env` / `seed_kernel_intern_table`; tracked `dsl/gunbc/plans/representation_minimization.dag`"), cell(text: "whole-ancestry-per-module resolve, `func_env.sigs` module x closure-width, per-module intern_table copy"), cell(text: "AUDIT / MEASURED (VmHWM probe; being killed by sibling lanes) -- NO shape gate against reintroduction"), cell(text: "symptom bounded by the memory WALL (#8), not the shape"), cell(text: "RESOURCE symptom, STRUCTURAL root")]), + row(cells: [cell(text: "termination / DescentEvidence"), cell(text: "`dag/std/termination.dag`; v1 checker `src/v1/complexity.dag` + `CostBound`/`PolyCost` in `dag/std/induction.dag`"), cell(text: "well-founded descent; poly cost bound; `Strict|NonIncreasing|DescentUnknown` bounded lattice, bottom fails closed"), cell(text: "**WALL** primitive (`DescentUnknown` blocks a proof)"), cell(text: "via v1-seed consumers"), cell(text: "STRUCTURAL (termination)")]), + row(cells: [cell(text: "realization_width / memory_bounded_fit_count"), cell(text: "`dag/std/realization_width.dag`; actuator `cli_run.rs` `spawn_width_cap`"), cell(text: "memory-bounded parallel width = budget / per-shard peak; caps spawn width so co-resident VmHWM <= cgroup cap"), cell(text: "**WALL** / actuator (real floor consumer, fail-closed under-parallelize)"), cell(text: "YES (real consumer)"), cell(text: "RESOURCE (memory)")]), + row(cells: [cell(text: "budget tree (accounting)"), cell(text: "`dag/extdeps/accounting/budget.dag` (`admit_line_item`); `dag/product/budget_tree.dag` (`node_conserves`); `dag/gunbc/ci_budget_tree.dag`"), cell(text: "capped-resource -> line-item admission (Memory); conservation Bool"), cell(text: "admission construction (over-cap unwritable on the admit path) + RESIDUE (`node_conserves` for raw literals)"), cell(text: "YES (`*budget*_witness_test.dag`)"), cell(text: "RESOURCE (memory/money)")]), + row(cells: [cell(text: "node_wall_clock_ratchet"), cell(text: "`dag/gunbc/test_node_wall_clock_ratchet.dag`"), cell(text: "committed roster of test names permitted to emit wall-clock/time warnings"), cell(text: "RATCHET (bumpable roster)"), cell(text: "via testgen oracle"), cell(text: "RESOURCE (wall-clock)")]), + row(cells: [cell(text: "EffortBudget (op-count)"), cell(text: "prose only in `dag/gunbc/plans/budget_tree.dag`; nearest live: `estimate_expr_size` `budget: Int` guard in `src/v1/complexity.dag`"), cell(text: "op-count recursion budget"), cell(text: "INERT (no `EffortBudget` type exists in the tree)"), cell(text: "NO"), cell(text: "RESOURCE (op-count)")]), + row(cells: [cell(text: "algebraic-rewrite optimization"), cell(text: "`dag/gunbc/plans/algebraic_rewrite_optimization.dag`"), cell(text: "design spec for an O(n^2)->O(n) rewrite catalog + `Unknown` dissolution"), cell(text: "INERT / design-only (POST-STABILITY; no rewrite rows exist)"), cell(text: "NO"), cell(text: "STRUCTURAL (unbuilt)")]), + row(cells: [cell(text: "resolver-pathology quadratics"), cell(text: "targets in `v1_compiler_infer.rs` `build_type_env` / `seed_kernel_intern_table`; tracked `dag/gunbc/plans/representation_minimization.dag`"), cell(text: "whole-ancestry-per-module resolve, `func_env.sigs` module x closure-width, per-module intern_table copy"), cell(text: "AUDIT / MEASURED (VmHWM probe; being killed by sibling lanes) -- NO shape gate against reintroduction"), cell(text: "symptom bounded by the memory WALL (#8), not the shape"), cell(text: "RESOURCE symptom, STRUCTURAL root")]), ], }, h2(text: "4. The verdict -- the structural-quadratic class partitioned"), diff --git a/docs/plans/structural-quadratic-wall-coverage-audit.md b/docs/plans/structural-quadratic-wall-coverage-audit.md index 04ca48fafb9..cf130bbff8f 100644 --- a/docs/plans/structural-quadratic-wall-coverage-audit.md +++ b/docs/plans/structural-quadratic-wall-coverage-audit.md @@ -26,13 +26,13 @@ Reading of the receipt: the whole-corpus mechanism that actually executes is a * | intent-linearity lens | `src/v2/lens/intent_linearity.dag` | simulated/unrollable chains + lowerable-cost nodes across term-chain / type-forest / import-graph | WALL-after-grounding (`closure_drift` wall) | PARTIAL | STRUCTURAL | | synthesis / lower-bound gap | `src/v2/lens/synthesis.dag` | realization cost vs declared relation's structural lower bound | RESIDUE / AUDIT (`AdvisoryLens`, never gates -- the SS5 region-(3) residue: optimality is Rice-undecidable) | tests run; lens advisory | STRUCTURAL (non-gating) | | complexity_linearity_audit bin | `src/v1/stage0/src/bin/complexity_linearity_audit.rs` + `_project.rs` | syntactic match-wildcard arms + `syntactic_high_match_fanout` (parse-only whole-corpus proxy) | AUDIT / emit-only (exit 0 unless `--fail-on-findings`) | NO (scaffold, until #5966) | SYNTACTIC PROXY | -| termination / DescentEvidence | `dsl/std/termination.dag`; v1 checker `src/v1/complexity.dag` + `CostBound`/`PolyCost` in `dsl/std/induction.dag` | well-founded descent; poly cost bound; `Strict|NonIncreasing|DescentUnknown` bounded lattice, bottom fails closed | **WALL** primitive (`DescentUnknown` blocks a proof) | via v1-seed consumers | STRUCTURAL (termination) | -| realization_width / memory_bounded_fit_count | `dsl/std/realization_width.dag`; actuator `cli_run.rs` `spawn_width_cap` | memory-bounded parallel width = budget / per-shard peak; caps spawn width so co-resident VmHWM <= cgroup cap | **WALL** / actuator (real floor consumer, fail-closed under-parallelize) | YES (real consumer) | RESOURCE (memory) | -| budget tree (accounting) | `dsl/extdeps/accounting/budget.dag` (`admit_line_item`); `dsl/product/budget_tree.dag` (`node_conserves`); `dsl/gunbc/ci_budget_tree.dag` | capped-resource -> line-item admission (Memory); conservation Bool | admission construction (over-cap unwritable on the admit path) + RESIDUE (`node_conserves` for raw literals) | YES (`*budget*_witness_test.dag`) | RESOURCE (memory/money) | -| node_wall_clock_ratchet | `dsl/gunbc/test_node_wall_clock_ratchet.dag` | committed roster of test names permitted to emit wall-clock/time warnings | RATCHET (bumpable roster) | via testgen oracle | RESOURCE (wall-clock) | -| EffortBudget (op-count) | prose only in `dsl/gunbc/plans/budget_tree.dag`; nearest live: `estimate_expr_size` `budget: Int` guard in `src/v1/complexity.dag` | op-count recursion budget | INERT (no `EffortBudget` type exists in the tree) | NO | RESOURCE (op-count) | -| algebraic-rewrite optimization | `dsl/gunbc/plans/algebraic_rewrite_optimization.dag` | design spec for an O(n^2)->O(n) rewrite catalog + `Unknown` dissolution | INERT / design-only (POST-STABILITY; no rewrite rows exist) | NO | STRUCTURAL (unbuilt) | -| resolver-pathology quadratics | targets in `v1_compiler_infer.rs` `build_type_env` / `seed_kernel_intern_table`; tracked `dsl/gunbc/plans/representation_minimization.dag` | whole-ancestry-per-module resolve, `func_env.sigs` module x closure-width, per-module intern_table copy | AUDIT / MEASURED (VmHWM probe; being killed by sibling lanes) -- NO shape gate against reintroduction | symptom bounded by the memory WALL (#8), not the shape | RESOURCE symptom, STRUCTURAL root | +| termination / DescentEvidence | `dag/std/termination.dag`; v1 checker `src/v1/complexity.dag` + `CostBound`/`PolyCost` in `dag/std/induction.dag` | well-founded descent; poly cost bound; `Strict|NonIncreasing|DescentUnknown` bounded lattice, bottom fails closed | **WALL** primitive (`DescentUnknown` blocks a proof) | via v1-seed consumers | STRUCTURAL (termination) | +| realization_width / memory_bounded_fit_count | `dag/std/realization_width.dag`; actuator `cli_run.rs` `spawn_width_cap` | memory-bounded parallel width = budget / per-shard peak; caps spawn width so co-resident VmHWM <= cgroup cap | **WALL** / actuator (real floor consumer, fail-closed under-parallelize) | YES (real consumer) | RESOURCE (memory) | +| budget tree (accounting) | `dag/extdeps/accounting/budget.dag` (`admit_line_item`); `dag/product/budget_tree.dag` (`node_conserves`); `dag/gunbc/ci_budget_tree.dag` | capped-resource -> line-item admission (Memory); conservation Bool | admission construction (over-cap unwritable on the admit path) + RESIDUE (`node_conserves` for raw literals) | YES (`*budget*_witness_test.dag`) | RESOURCE (memory/money) | +| node_wall_clock_ratchet | `dag/gunbc/test_node_wall_clock_ratchet.dag` | committed roster of test names permitted to emit wall-clock/time warnings | RATCHET (bumpable roster) | via testgen oracle | RESOURCE (wall-clock) | +| EffortBudget (op-count) | prose only in `dag/gunbc/plans/budget_tree.dag`; nearest live: `estimate_expr_size` `budget: Int` guard in `src/v1/complexity.dag` | op-count recursion budget | INERT (no `EffortBudget` type exists in the tree) | NO | RESOURCE (op-count) | +| algebraic-rewrite optimization | `dag/gunbc/plans/algebraic_rewrite_optimization.dag` | design spec for an O(n^2)->O(n) rewrite catalog + `Unknown` dissolution | INERT / design-only (POST-STABILITY; no rewrite rows exist) | NO | STRUCTURAL (unbuilt) | +| resolver-pathology quadratics | targets in `v1_compiler_infer.rs` `build_type_env` / `seed_kernel_intern_table`; tracked `dag/gunbc/plans/representation_minimization.dag` | whole-ancestry-per-module resolve, `func_env.sigs` module x closure-width, per-module intern_table copy | AUDIT / MEASURED (VmHWM probe; being killed by sibling lanes) -- NO shape gate against reintroduction | symptom bounded by the memory WALL (#8), not the shape | RESOURCE symptom, STRUCTURAL root | ## 4. The verdict -- the structural-quadratic class partitioned From 004a4df3b03775adebb0714944e572bc0fb9bbc5 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Fri, 3 Jul 2026 02:33:18 +0000 Subject: [PATCH 5/7] Complexity gating (i): completeness-gated import-closure parallel-representation prevention wall MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit First real enforced wall from the complexity-gating lane (Deliverable 1 audit: detection real, enforcement zero). A change-time / §2-§4 STRUCTURAL wall: a module's DECLARED consumed-input closure must equal its DERIVED import closure (import_closure_live). It FOLDS the whole declared_consumed_input_closures registry, so any future declared closure is auto-covered — closing the "only the one conformance closure is hand-witnessed" gap. Forward-looking ask-once-compile-forever prevention; registry is 1 clean entry (0 drift) so it lands clean, no self-poison. Adds entry_path to ConsumedInputClosure (additive; existing consumers read consumed_dag_paths/unit only; conformance witness regression PASS). Green-by-execution on the v1 floor engine (claim_batch), 3 witnesses: clean (0 drift), red control (drifted closure detected), completeness (injected drift into the fold auto-caught). Enforcement maturity (honest): realized as a floor witness (fail-closed — a red witness fails the floor). A corpus-level registry-fold check does not fit always_required_lenses (per-compiled-node CompileLens); the floor witness is the correct fail-closed realization. Because main ci.yml cancels at the 30-min compile-clean timeout before batch-2 witnesses run, this wall — like every batch-2 witness — enforces on the local/scheduled floor run, not yet on main CI; full CI enforcement follows the compile-clean-serial lane. Runtime-quadratic walls remain blocked on the v2 body-lowering milestone (real fn bodies do not lower to inspectable Loop nodes); dispatched separately. Co-Authored-By: Claude Opus 4.8 (1M context) --- dag/tools/rust_stage0_gates.dag | 2 + .../import_closure_completeness_test.dag | 45 +++++++++++++++++++ 2 files changed, 47 insertions(+) create mode 100644 src/v2/test/claim/intent_linearity/lens_unit/import_closure_completeness_test.dag diff --git a/dag/tools/rust_stage0_gates.dag b/dag/tools/rust_stage0_gates.dag index 74ee67b4725..d7a965372c6 100644 --- a/dag/tools/rust_stage0_gates.dag +++ b/dag/tools/rust_stage0_gates.dag @@ -41,11 +41,13 @@ data consumed_input_closure_slice1_status: Disposition = Scaffold { type ConsumedInputClosure { unit: String + entry_path: String consumed_dag_paths: List } data coproduct_reflection_conformance_consumed_closure: ConsumedInputClosure = ConsumedInputClosure { unit: "coproduct_reflection_conformance_test", + entry_path: "src/v2/test/claim/manual/coproduct_reflection_conformance_test.dag", consumed_dag_paths: [ "src/v2/test/claim/manual/coproduct_reflection_conformance_test.dag", "src/v2/std/algebra.dag", diff --git a/src/v2/test/claim/intent_linearity/lens_unit/import_closure_completeness_test.dag b/src/v2/test/claim/intent_linearity/lens_unit/import_closure_completeness_test.dag new file mode 100644 index 00000000000..0c15ab2e4c3 --- /dev/null +++ b/src/v2/test/claim/intent_linearity/lens_unit/import_closure_completeness_test.dag @@ -0,0 +1,45 @@ +module v2.test.intent_linearity.lens_unit.import_closure_completeness + +import v2.lens.intent_linearity { import_closure_is_clean_live } +import tools.rust_stage0_gates { ConsumedInputClosure, declared_consumed_input_closures } +import gunbc.ci_layer_roots { witness_layer_roots } +import v2.std.algebra { FreeMonoid, for_all, list_snoc_item } +import v2.std.collection { List } +import v2.std.logic { Bool } +import v2.std.text { String } + +data import_closure_completeness_doc: String = "Completeness-gated parallel-representation wall (change-time / §2-§4): a module's DECLARED consumed-input closure must equal its DERIVED import closure (import_closure_live over witness_layer_roots). This FOLDS over the whole declared_consumed_input_closures registry, so ANY future declared closure is auto-covered by the same gate — closing the 'only the one conformance closure is hand-witnessed' gap. Forward-looking ask-once-compile-forever prevention, not instance-count-bound (today the registry is 1 clean entry, 0 drift). ENFORCEMENT MATURITY: this is a floor witness (fail-closed on the v1 floor engine — a red witness fails the floor). Because main ci.yml currently CANCELS at the 30-min compile-clean timeout before batch-2 witnesses run, this wall — like every batch-2 witness — is enforced on the LOCAL/scheduled floor run, NOT yet on main CI; full CI enforcement follows the compile-clean-serial lane. Green-by-execution verified on claim_batch (v1 engine)." + +fn closure_row_is_clean(c: ConsumedInputClosure) -> Bool { + import_closure_is_clean_live( + declared: c.consumed_dag_paths, + entry_path: c.entry_path, + pool_roots: witness_layer_roots + ) +} + +fn all_closures_clean(closures: List) -> Bool { + for_all(xs: closures, predicate: closure_row_is_clean) +} + +data synthetic_drifted_closure: ConsumedInputClosure = ConsumedInputClosure { + unit: "synthetic_drift_control", + entry_path: "src/v2/test/claim/manual/coproduct_reflection_conformance_test.dag", + consumed_dag_paths: ["src/v2/std/__bogus_never_imported__.dag"] +} + +fn registry_with_injected_drift() -> FreeMonoid { + list_snoc_item(xs: declared_consumed_input_closures, item: synthetic_drifted_closure) +} + +test fn all_declared_import_closures_have_no_drift() -> Bool { + return all_closures_clean(closures: declared_consumed_input_closures) +} + +test fn completeness_fold_reds_on_a_drifted_closure() -> Bool { + return !all_closures_clean(closures: [synthetic_drifted_closure]) +} + +test fn fold_auto_covers_a_newly_added_closure() -> Bool { + return !all_closures_clean(closures: registry_with_injected_drift()) +} From 105a18c982439f8448e55b9cab450d5a53e1fed3 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Fri, 3 Jul 2026 04:47:47 +0000 Subject: [PATCH 6/7] WIP: STRUCTURAL-QUADRATIC WALLS (not a ratchet): make the OBVIOUS, DECIDABLE --- dag/gunbc/plans/structural_quadratic_wall_coverage_audit.dag | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/dag/gunbc/plans/structural_quadratic_wall_coverage_audit.dag b/dag/gunbc/plans/structural_quadratic_wall_coverage_audit.dag index ea073d7738b..57572331a99 100644 --- a/dag/gunbc/plans/structural_quadratic_wall_coverage_audit.dag +++ b/dag/gunbc/plans/structural_quadratic_wall_coverage_audit.dag @@ -29,7 +29,9 @@ fn structural_quadratic_wall_coverage_audit_body() -> List { row(cells: [cell(text: "intent-linearity lens"), cell(text: "`src/v2/lens/intent_linearity.dag`"), cell(text: "simulated/unrollable chains + lowerable-cost nodes across term-chain / type-forest / import-graph"), cell(text: "WALL-after-grounding (`closure_drift` wall)"), cell(text: "PARTIAL"), cell(text: "STRUCTURAL")]), row(cells: [cell(text: "synthesis / lower-bound gap"), cell(text: "`src/v2/lens/synthesis.dag`"), cell(text: "realization cost vs declared relation's structural lower bound"), cell(text: "RESIDUE / AUDIT (`AdvisoryLens`, never gates -- the SS5 region-(3) residue: optimality is Rice-undecidable)"), cell(text: "tests run; lens advisory"), cell(text: "STRUCTURAL (non-gating)")]), row(cells: [cell(text: "complexity_linearity_audit bin"), cell(text: "`src/v1/stage0/src/bin/complexity_linearity_audit.rs` + `_project.rs`"), cell(text: "syntactic match-wildcard arms + `syntactic_high_match_fanout` (parse-only whole-corpus proxy)"), cell(text: "AUDIT / emit-only (exit 0 unless `--fail-on-findings`)"), cell(text: "NO (scaffold, until #5966)"), cell(text: "SYNTACTIC PROXY")]), - row(cells: [cell(text: "termination / DescentEvidence"), cell(text: "`dag/std/termination.dag`; v1 checker `src/v1/complexity.dag` + `CostBound`/`PolyCost` in `dag/std/induction.dag`"), cell(text: "well-founded descent; poly cost bound; `Strict|NonIncreasing|DescentUnknown` bounded lattice, bottom fails closed"), cell(text: "**WALL** primitive (`DescentUnknown` blocks a proof)"), cell(text: "via v1-seed consumers"), cell(text: "STRUCTURAL (termination)")]), + row(cells: [cell(text: "termination / DescentEvidence (live authority)"), cell(text: "`dag/std/termination.dag`; v1 checker `src/v1/complexity.dag` + `CostBound`/`PolyCost` in `dag/std/induction.dag`"), cell(text: "well-founded descent; poly cost bound; `Strict|NonIncreasing|DescentUnknown` bounded lattice (meet/join/promote_to_strict), bottom fails closed"), cell(text: "**WALL** primitive (`DescentUnknown` blocks a proof)"), cell(text: "via v1-seed consumers"), cell(text: "STRUCTURAL (termination)")]), + row(cells: [cell(text: "DescentEvidence -- v2 FORK (SS3)"), cell(text: "`src/v2/std/cardinality.dag:108` bare `DescentEvidence` (no lattice), byte-identical variant set to the `std.termination` authority above but in a different namespace"), cell(text: "same `Strict|NonIncreasing|DescentUnknown` variants; INERT-by-execution -- never constructed or matched anywhere in v2 (grep-clean); sole consumer is a type annotation on `While.bound`, and `While` is emit-REJECTED (`05_emit_orchestration.dag`), so the field is never read"), cell(text: "INERT + **SS3 FORK** of the live authority -- a DECIDABLE-WALL CANDIDATE (variant-set equality across a layer boundary is decidable by construction; the SS5-`WallNow` twin of the SS4 `import_closure` parallel-rep wall). Consolidation ruled FLAG-A (dag/std wins); body-lowering Stage-1 dissolves it (construction fix), after which a prevention wall fences re-introduction at 0 instances"), cell(text: "NO (inert)"), cell(text: "STRUCTURAL (termination)")]), + row(cells: [cell(text: "v2 loop-termination multiplicity"), cell(text: "`src/v2/std/cardinality.dag:219-284` `behavior_multiplicity(Loop)` -> `node_multiplicity` -> `termination_proof_witness_for_node`"), cell(text: "`Loop => RequiresTerminationProof` decided TAG-ONLY (node + measure not in scope) -> `Violates` unconditionally"), cell(text: "WALL but MISCALIBRATED / over-broad -- fail-CLOSED (walls ALL loops incl. provable ones because it never reads the measure); body-lowering Stage-2 refinement makes it read the measure (`Strict` passes, `DescentUnknown` still walls)"), cell(text: "YES (by exec: `04_infer.dag:217` + loop/branch/bind eval witnesses)"), cell(text: "STRUCTURAL (termination)")]), row(cells: [cell(text: "realization_width / memory_bounded_fit_count"), cell(text: "`dag/std/realization_width.dag`; actuator `cli_run.rs` `spawn_width_cap`"), cell(text: "memory-bounded parallel width = budget / per-shard peak; caps spawn width so co-resident VmHWM <= cgroup cap"), cell(text: "**WALL** / actuator (real floor consumer, fail-closed under-parallelize)"), cell(text: "YES (real consumer)"), cell(text: "RESOURCE (memory)")]), row(cells: [cell(text: "budget tree (accounting)"), cell(text: "`dag/extdeps/accounting/budget.dag` (`admit_line_item`); `dag/product/budget_tree.dag` (`node_conserves`); `dag/gunbc/ci_budget_tree.dag`"), cell(text: "capped-resource -> line-item admission (Memory); conservation Bool"), cell(text: "admission construction (over-cap unwritable on the admit path) + RESIDUE (`node_conserves` for raw literals)"), cell(text: "YES (`*budget*_witness_test.dag`)"), cell(text: "RESOURCE (memory/money)")]), row(cells: [cell(text: "node_wall_clock_ratchet"), cell(text: "`dag/gunbc/test_node_wall_clock_ratchet.dag`"), cell(text: "committed roster of test names permitted to emit wall-clock/time warnings"), cell(text: "RATCHET (bumpable roster)"), cell(text: "via testgen oracle"), cell(text: "RESOURCE (wall-clock)")]), From 69bdfb26e08f045bb04c9956c67192502318cf29 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Fri, 3 Jul 2026 04:50:55 +0000 Subject: [PATCH 7/7] Revert stray auto-committed audit-row edit (restore .dag<->.md consistency) The v2 DescentEvidence-fork audit rows were mid-edit when the auto-committer captured them into 105a18c982 without the paired plan-doc regen (which routes to BuildBuddy remote and cannot see a working-tree edit), leaving the committed .dag drifted from its generated .md projection = a drift-gate self-poison. The fold is deferred to fierce-bee's body-lowering Stage-1, where the DescentEvidence fork is consolidated (so the row's final content is determined there) and the plan-doc regen is already part of that lane's workflow. Co-Authored-By: Claude Opus 4.8 (1M context) --- dag/gunbc/plans/structural_quadratic_wall_coverage_audit.dag | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) diff --git a/dag/gunbc/plans/structural_quadratic_wall_coverage_audit.dag b/dag/gunbc/plans/structural_quadratic_wall_coverage_audit.dag index 57572331a99..ea073d7738b 100644 --- a/dag/gunbc/plans/structural_quadratic_wall_coverage_audit.dag +++ b/dag/gunbc/plans/structural_quadratic_wall_coverage_audit.dag @@ -29,9 +29,7 @@ fn structural_quadratic_wall_coverage_audit_body() -> List { row(cells: [cell(text: "intent-linearity lens"), cell(text: "`src/v2/lens/intent_linearity.dag`"), cell(text: "simulated/unrollable chains + lowerable-cost nodes across term-chain / type-forest / import-graph"), cell(text: "WALL-after-grounding (`closure_drift` wall)"), cell(text: "PARTIAL"), cell(text: "STRUCTURAL")]), row(cells: [cell(text: "synthesis / lower-bound gap"), cell(text: "`src/v2/lens/synthesis.dag`"), cell(text: "realization cost vs declared relation's structural lower bound"), cell(text: "RESIDUE / AUDIT (`AdvisoryLens`, never gates -- the SS5 region-(3) residue: optimality is Rice-undecidable)"), cell(text: "tests run; lens advisory"), cell(text: "STRUCTURAL (non-gating)")]), row(cells: [cell(text: "complexity_linearity_audit bin"), cell(text: "`src/v1/stage0/src/bin/complexity_linearity_audit.rs` + `_project.rs`"), cell(text: "syntactic match-wildcard arms + `syntactic_high_match_fanout` (parse-only whole-corpus proxy)"), cell(text: "AUDIT / emit-only (exit 0 unless `--fail-on-findings`)"), cell(text: "NO (scaffold, until #5966)"), cell(text: "SYNTACTIC PROXY")]), - row(cells: [cell(text: "termination / DescentEvidence (live authority)"), cell(text: "`dag/std/termination.dag`; v1 checker `src/v1/complexity.dag` + `CostBound`/`PolyCost` in `dag/std/induction.dag`"), cell(text: "well-founded descent; poly cost bound; `Strict|NonIncreasing|DescentUnknown` bounded lattice (meet/join/promote_to_strict), bottom fails closed"), cell(text: "**WALL** primitive (`DescentUnknown` blocks a proof)"), cell(text: "via v1-seed consumers"), cell(text: "STRUCTURAL (termination)")]), - row(cells: [cell(text: "DescentEvidence -- v2 FORK (SS3)"), cell(text: "`src/v2/std/cardinality.dag:108` bare `DescentEvidence` (no lattice), byte-identical variant set to the `std.termination` authority above but in a different namespace"), cell(text: "same `Strict|NonIncreasing|DescentUnknown` variants; INERT-by-execution -- never constructed or matched anywhere in v2 (grep-clean); sole consumer is a type annotation on `While.bound`, and `While` is emit-REJECTED (`05_emit_orchestration.dag`), so the field is never read"), cell(text: "INERT + **SS3 FORK** of the live authority -- a DECIDABLE-WALL CANDIDATE (variant-set equality across a layer boundary is decidable by construction; the SS5-`WallNow` twin of the SS4 `import_closure` parallel-rep wall). Consolidation ruled FLAG-A (dag/std wins); body-lowering Stage-1 dissolves it (construction fix), after which a prevention wall fences re-introduction at 0 instances"), cell(text: "NO (inert)"), cell(text: "STRUCTURAL (termination)")]), - row(cells: [cell(text: "v2 loop-termination multiplicity"), cell(text: "`src/v2/std/cardinality.dag:219-284` `behavior_multiplicity(Loop)` -> `node_multiplicity` -> `termination_proof_witness_for_node`"), cell(text: "`Loop => RequiresTerminationProof` decided TAG-ONLY (node + measure not in scope) -> `Violates` unconditionally"), cell(text: "WALL but MISCALIBRATED / over-broad -- fail-CLOSED (walls ALL loops incl. provable ones because it never reads the measure); body-lowering Stage-2 refinement makes it read the measure (`Strict` passes, `DescentUnknown` still walls)"), cell(text: "YES (by exec: `04_infer.dag:217` + loop/branch/bind eval witnesses)"), cell(text: "STRUCTURAL (termination)")]), + row(cells: [cell(text: "termination / DescentEvidence"), cell(text: "`dag/std/termination.dag`; v1 checker `src/v1/complexity.dag` + `CostBound`/`PolyCost` in `dag/std/induction.dag`"), cell(text: "well-founded descent; poly cost bound; `Strict|NonIncreasing|DescentUnknown` bounded lattice, bottom fails closed"), cell(text: "**WALL** primitive (`DescentUnknown` blocks a proof)"), cell(text: "via v1-seed consumers"), cell(text: "STRUCTURAL (termination)")]), row(cells: [cell(text: "realization_width / memory_bounded_fit_count"), cell(text: "`dag/std/realization_width.dag`; actuator `cli_run.rs` `spawn_width_cap`"), cell(text: "memory-bounded parallel width = budget / per-shard peak; caps spawn width so co-resident VmHWM <= cgroup cap"), cell(text: "**WALL** / actuator (real floor consumer, fail-closed under-parallelize)"), cell(text: "YES (real consumer)"), cell(text: "RESOURCE (memory)")]), row(cells: [cell(text: "budget tree (accounting)"), cell(text: "`dag/extdeps/accounting/budget.dag` (`admit_line_item`); `dag/product/budget_tree.dag` (`node_conserves`); `dag/gunbc/ci_budget_tree.dag`"), cell(text: "capped-resource -> line-item admission (Memory); conservation Bool"), cell(text: "admission construction (over-cap unwritable on the admit path) + RESIDUE (`node_conserves` for raw literals)"), cell(text: "YES (`*budget*_witness_test.dag`)"), cell(text: "RESOURCE (memory/money)")]), row(cells: [cell(text: "node_wall_clock_ratchet"), cell(text: "`dag/gunbc/test_node_wall_clock_ratchet.dag`"), cell(text: "committed roster of test names permitted to emit wall-clock/time warnings"), cell(text: "RATCHET (bumpable roster)"), cell(text: "via testgen oracle"), cell(text: "RESOURCE (wall-clock)")]),