From 85f4d6ff03dcf89ccb3f458bd959e6c197a1ba07 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Thu, 2 Jul 2026 20:12:57 +0000 Subject: [PATCH 1/4] 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/4] 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/4] 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/4] =?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