Repository navigation
§1 measurement keystone (instrument): emit floor concurrent-peak RSS (VmHWM) so width derives from a MEASURED peak, not a hand-grounded literal - #5431
Merged
Conversation
briansrls
added a commit
that referenced
this pull request
Jun 21, 2026
…maining is the Phase-1 consumer Per quick-ant-298: the measurement keystone was nearly complete — model side already floor-enrolled, step timing already emitted; the only gap was peak-RSS, closed by #5431. P4's Phase-0 dependency is satisfied; remaining is the Phase-1 measured->plan feedback + width-fold (also unblocks §1-C). Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
This was referenced Jun 21, 2026
Merged
briansrls
added a commit
that referenced
this pull request
Jun 21, 2026
…ce-hawk #5427) The 3-filter allowlist was COST selection, not arbitrary gatekeeping — the v1 SEED compiler costs ~tens of CPU-sec per trivial test, so run-all-per-PR is CPU-hours (off the table). True shape: per-PR cost-bounded subset + measured #[ignore="expensive: Ns"] + completeness lens (#5427); nightly --ignored lane as the destination for expensive + the 58 currently-ignored tests (owned by §1/quick-ant, after #5431, escalate for load-bearing CI-gen). Completeness = every test runs on >=1 cadence (fail-closed). Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
briansrls
added a commit
that referenced
this pull request
Jun 21, 2026
…budgets) + plan doc (#5436) * WIP: dsl -> v2 scoping * WIP: ROADMAP planning * WIP: ROADMAP planning * WIP: ROADMAP planning * ROADMAP: scannable dependency-ordered checklist; consolidate caching plan (de-fork zesty-deer-479 owner, absorb quick-ant-298 spine) Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> * WIP: ROADMAP planning * self-host: add bootstrap purity (no stage0 hand-edits / regen-lockstep keystone) + precise v1 cutover Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> * ROADMAP §0 fail-closed lock-down (blocks expansion) + audit doc; §4 website demo Audit: cache lossy-digest flake (resolved_graph_cache.rs:146, verified), ~inert analytical lenses (complexity/cost/etc), regen --verify unwired (#5325). Lock-down checklist gates expansion. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> * ROADMAP: flesh §2 idea->idea compiler (medium/language axes); §0 → lock-down LANE (audits→fixes→meta), name model<->realization fork as suspected root Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> * WIP: ROADMAP planning * lock-down: add CI-coverage-completeness audit (rust gate runs 3 of 60 v1 suites) + axiom/syllogism lens (DESIGN open thread #1 — lock down the reasoning) Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> * WIP: ROADMAP planning * roadmap §0/§7 + lockdown: lead with correctness-by-construction, demote lenses to residue Folds in the operator principle (relayed via quick-ant-298): a lens is validation — it concedes the bad thing is writable. Root-cause to make it unwritable (single authority / realization derived from model); reserve lenses for the genuinely- unstructurable (complexity/necessity). #5423's spec-only key lens shipped a false-green as the live proof. - ROADMAP §0: add the principle; split Fixes into tier-1 construction (dissolve model↔realization fork; cache-key derived-from-declared-inputs; self-host purity by construction) and tier-2 lens (complexity/cost; cache-redundancy; purity oracle; promote-inert). Meta-invariant → construction-justification rule. - ROADMAP §7: P1 cache-key reframed from 'realizer-key lens' to key derived from declared inputs_considered (construction). - fail-closed-lockdown.md: construction principle in the thesis; §4 checklist re-ordered construction-first / lens-residue; meta = construction-justification. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> * roadmap §0: add Disposition carrier + 'confront skipped modeling decisions' Captures the lens/coproduct disposition decision (operator). One typed carrier (Terminal{reason} | Scaffold{dissolves_to}) for BOTH lens-lifecycle tags AND coproduct dissolve-markers — today freeform 🟡 comments, unreadable by lens since comments aren't Nodes. Decision: middle path (construction-capable carrier + selectively-enforcing lens that ratchets coverage) now, #1 (substrate can't-define-untagged) as the named end-state. The lens is itself a Scaffold{dissolves_to: substrate-mandatory-tag} — self-dissolving when coverage = whole tree. Rejected jumping to #1 on sequencing (load-bearing §4 substrate change → escalate; flag-day migration; derived coproducts need disposition derived not authored), not on principle. Enforceability split: presence = construction (non-optional field, no meta-lens); redundancy (scaffold + successor both present) = hard gate; Terminal-vs-Scaffold correctness = retro/judgment (synthesis-feasibility limit). - docs/plans/disposition-carrier.md (new) - ROADMAP §0 tier-1 + meta 'confront skipped decisions' standing practice Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> * WIP: ROADMAP planning * DESIGN §5/§6: promote construction-over-validation; roadmap: scope-partition §0, testgen §1, shelve dashboard Addresses the review's four flags + sequencing nuance. - DESIGN.md §5: 'correctness by construction, not validation' is now an axiom (a check re-stating a model constraint is a 2nd representation §2/§3; prefer realization derived from a single authority; reserve checks for the unstructurable residue). §6 'enforce with lenses' reconciled: construction first, lens = residue mechanism, AND the executable inert-lens backstop is NOT superseded by the authoring-time construction-justification judgment. (flag 4 home + flag 3) - ROADMAP §0 partitioned: In-scope this window (numeric-tower grounding; cache trustworthy + warm==cold oracle shipped NOW as detective; widen rust gate; promote inert lenses) vs Fenced-OUT fan-out (Value::Null 131-site split; self-host purity gate; cross-tree import activation; Disposition carrier). Honest framing: window reduces fail-open surface, does NOT 'lock' the class — Null split stays open. (flags 1, 2, sequencing nuance) - ROADMAP §0 meta: restored executable inert-lens hygiene backstop, construction- justification layered on top (not 'supersedes'). (flag 3) - De-dup: principle no longer restated in ROADMAP/lockdown §0; both point to DESIGN §5. cache-key construction homed in §7, §0 references it. (flag 4) - ROADMAP §1 = testgen as bug-class oracle (+ affected-set completeness half + parked anemia lens); dashboard shelved to §8. - docs/plans/testgen-oracle.md (new), fail-closed-lockdown.md realigned. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> * WIP: ROADMAP planning * DESIGN §5/§6/§7: wall-vs-ratchet decidability, displaced-pain denominator, open language design Folds in the operator's product thesis + the two bounds that keep it honest. - §5: construction makes a class unwritable only when membership is DECIDABLE — trichotomy (wall now / wall after grounding / ratchet forever); 'never' is the trap (lets an undecidable ratchet masquerade as a wall — optimality by Rice). - §6: denominate the benefit — the deliverable is a displaced cost (§1 time / a paid-for pain), the lens/substrate is the moat not the product; priced in elegance the work is unbounded (the economic twin of 'never'). - §7: the recursion's payoff — language design itself opens up. It's locked by cost (a check = a compiler fork; a language = an adoption problem); both dissolve here (a wall is a row §2, applied over a medium-agnostic substrate §4), so (compiler-fork × language) → (row + medium). Sound where ingest is Lossless, fail-closed where not (DecodeFidelity §4). Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> * WIP: ROADMAP planning * ROADMAP: fix doc-graph violations from bright-eagle-46 review of #5424 Apply the apex axiom/syllogism lens (single authority / no orphan / no cycle) to the roadmap itself — manual acyclicity pass: - orphan: testgen-oracle.md backlinked §1 → repoint §4 (its own lane) - single authority: §0 cache-key now a pure pointer (= §2 F2/F3/P1); §0 numeric-tower marked the authoritative home (§5 de-fork / fork plan point here, no second checkbox) - §0↔§5 cycle: self-host purity reframed as a §5 deliverable §0's expansion-gate depends on (edge §5 → §0-gate → products), not §0-owned - undeclared edge: §7 react/html declares its dependency on §6 media - backlink sweep: the reorg had broken every numeric backlink across 7 plan docs; re-point all and anchor each to the stable section TITLE so a future renumber can't silently break them again Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> * ROADMAP §3 + plan: algorithmic-cost reduction by construction (rewrite, not budget) Reframe §3 from per-fn complexity budgets to the actual intent: rewrite common suboptimal patterns (O(n²)→O(n), O(2ⁿ)→O(n), O(n)→O(log n)) to the cheaper equivalent — construction on the cost axis, not a warning. New plan doc docs/plans/algebraic-rewrite-optimization.md captures the up-front design: the decidability split (modeled EffectShape makes the preconditions structural; equivalence stays undecidable so no optimality oracle), rewrite-rule-as-row + once-proven soundness, the common-case catalog tiered by precondition, D1 canonical-form-is-truth / D2 two seed rules / D4 constant-factor deferred, the four-witness DONE bar (incl. the non-firing control half-done versions skip), and a corpus hit-rate acceptance gate. complexity.dag is the cost oracle; synthesis.dag stays the advisory undecidable residue. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> * ROADMAP §2: Phase-0 measurement instrument done (#5431 peak-RSS) — remaining is the Phase-1 consumer Per quick-ant-298: the measurement keystone was nearly complete — model side already floor-enrolled, step timing already emitted; the only gap was peak-RSS, closed by #5431. P4's Phase-0 dependency is satisfied; remaining is the Phase-1 measured->plan feedback + width-fold (also unblocks §1-C). Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> * plan/§3: detection-vs-enforcement containment (E⊆D′⊆D) + explicit seed-rule I/O up front Grounded in cost.dag U2 + complexity.dag (investigated, not theorized): - detection is TOTAL by construction (kernel-level cost fold; arbitrary fns detectable); boundary is precision (ClassUnknown), not coverage - enforced rewrites are a strict subset structurally guaranteed by the class-drop witness: E ⊆ D′(precise) ⊆ D(all) - n√n excluded for a MODEL reason (PolynomialDegree is integer-only, n^1.5 unrepresentable); ternary search excluded (log base is not a class) - today's small gate roster = subject-production limit (fn-body reflection), NOT a detection limit - new §3a fully specifies the two seed rules up front: input→output→ precondition→non-firing control→discriminating equivalence input, so the worker builds to spec and the project can actually finish Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> * ROADMAP §0/§1: rust-gate is cadence-decoupling, not run-all (per fierce-hawk #5427) The 3-filter allowlist was COST selection, not arbitrary gatekeeping — the v1 SEED compiler costs ~tens of CPU-sec per trivial test, so run-all-per-PR is CPU-hours (off the table). True shape: per-PR cost-bounded subset + measured #[ignore="expensive: Ns"] + completeness lens (#5427); nightly --ignored lane as the destination for expensive + the 58 currently-ignored tests (owned by §1/quick-ant, after #5431, escalate for load-bearing CI-gen). Completeness = every test runs on >=1 cadence (fail-closed). Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> * plan §2a: generalize by structural-redundancy keying (O(n^x)->O(n^(x-1)) free); flag n-log-n as substitution Per operator: catalog must generalize polynomial-degree reduction without edge cases. Resolution: rules key on the structural redundancy, never on degree — degree is not evidence of redundancy (would fire on genuine O(n^x)). A structurally-keyed nested-membership->set peels one level wherever it matches; fold-to-fixpoint gives O(n^3)->O(n^2)->O(n). Cost model supports arbitrary integer degree, so witness (b) holds at every peel. Flagged OPEN (operator input invited): O(n^x)->O(n log n) is algorithmic SUBSTITUTION (different algorithms, same I/O) not redundancy elimination — verges on undecidable equivalence; tractable form is per-idiom rules (sort-based dedup, repeated-min->heap), not a parameterized rule. Seed Rule 1 now authored structurally + carries a depth-2 generalization witness. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> * plan §1b: Unknown is an anemic atom — dissolve over time (reuse Disposition), never a false pass Per operator: classifying Unknown isn't a fixed up-front split — it's the standing anemic-leaf dissolution practice (DESIGN §2 decompress->map->reduce) applied to the cost lens. UnknownCost{diagnostic} already carries its reason; the anemia is the free-form reason. Each decomposition resolves an Unknown to construction (now-precise class -> new D′) or a grounded Terminal (genuinely undecidable, positively recognized -> advisory comment). DFS-first: this IS the Disposition carrier (resolves to construction-or-justified-Terminal), so reuse it, don't fork an unknown-reason enum. Supersedes the static Undecidable|Undetermined split. Two invariants fixed up front: never a false pass (Unknown=>Violates, already holds); every Unknown on the dissolution frontier. cost.dag enrichment + un-parking Disposition are operator-gated. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> * ROADMAP: §3 reverts to budget-gate validation (stability); rewrite-engine relocated to §5 (post-stability) Operator decision 2026-06-21: budget-gate validation is fine for the stability window; the algorithmic-cost REWRITE construction design is expansion, homed with self-hosting (§5) — IR-rewrite/canonicalization is most natural once .dag is the self-hosted truth. - §3 = complexity budget gate (validation): cost-lens symbolic_max fix (#5437) + per-fn subject + budget-gates-whole-codebase (gated on fn-body reflection) + synthesis advisory. #5437 foundation stays in-window. - §5 gains an 'adjacent expansion lane' = the rewrite engine, pointing at the preserved plan doc; marked post-stability. - plan doc status -> POST-STABILITY EXPANSION, relocated to §5. Nothing deleted — the rewrite design is preserved, just fenced out of the stability window (same as Disposition / Value::Null-split). Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> --------- Co-authored-by: Brian Searls <briansrls@gunb.ai> Co-authored-by: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
briansrls
added a commit
that referenced
this pull request
Jun 21, 2026
…pinned 4) Wire the measurement->plan loop #5431 opened: gunbc_ci_floor_spawn_width now returns min(shard_count, hardware_threads, floor(0.8*live_budget / measured_peak)) instead of hardware_thread_count(4). - gunbc.ci_floor_measurement (new): committed MEASURED per-shard peak, stamped from #5431's VmHWM emit (run 27893441091: 8400113664 bytes at width 4 => /4 = ~2.1GB/shard), NOT the ~14GB hand-grounded literal #5419 deleted. + dissolve-on drift-gate marker. - std.realization_width: memory_aware_spawn_width fold (pure, v2-inheriting) with a 0.8 safety fraction; fail-closed to a conservative committed width when budget unreadable. - claim_executor: reads the LIVE cgroup memory.max (meminfo fallback) and threads it into the .dag fold via run_in_context_with_args (DESIGN §3 measured=>peripheral: we commit our measurement, read the external-authored budget live). - witnesses: non-binding (4->7), tight-budget backoff, unreadable->fallback, fraction load-bearing, sub-unit->1. Proven by execution: derived spawn_width=7. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
briansrls
added a commit
that referenced
this pull request
Jun 21, 2026
briansrls
added a commit
that referenced
this pull request
Jun 21, 2026
briansrls
added a commit
that referenced
this pull request
Jun 21, 2026
…gestion⁻¹ past syntax (#5442) * WIP: dsl -> v2 scoping * WIP: ROADMAP planning * WIP: ROADMAP planning * WIP: ROADMAP planning * ROADMAP: scannable dependency-ordered checklist; consolidate caching plan (de-fork zesty-deer-479 owner, absorb quick-ant-298 spine) Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> * WIP: ROADMAP planning * self-host: add bootstrap purity (no stage0 hand-edits / regen-lockstep keystone) + precise v1 cutover Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> * ROADMAP §0 fail-closed lock-down (blocks expansion) + audit doc; §4 website demo Audit: cache lossy-digest flake (resolved_graph_cache.rs:146, verified), ~inert analytical lenses (complexity/cost/etc), regen --verify unwired (#5325). Lock-down checklist gates expansion. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> * ROADMAP: flesh §2 idea->idea compiler (medium/language axes); §0 → lock-down LANE (audits→fixes→meta), name model<->realization fork as suspected root Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> * WIP: ROADMAP planning * lock-down: add CI-coverage-completeness audit (rust gate runs 3 of 60 v1 suites) + axiom/syllogism lens (DESIGN open thread #1 — lock down the reasoning) Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> * WIP: ROADMAP planning * roadmap §0/§7 + lockdown: lead with correctness-by-construction, demote lenses to residue Folds in the operator principle (relayed via quick-ant-298): a lens is validation — it concedes the bad thing is writable. Root-cause to make it unwritable (single authority / realization derived from model); reserve lenses for the genuinely- unstructurable (complexity/necessity). #5423's spec-only key lens shipped a false-green as the live proof. - ROADMAP §0: add the principle; split Fixes into tier-1 construction (dissolve model↔realization fork; cache-key derived-from-declared-inputs; self-host purity by construction) and tier-2 lens (complexity/cost; cache-redundancy; purity oracle; promote-inert). Meta-invariant → construction-justification rule. - ROADMAP §7: P1 cache-key reframed from 'realizer-key lens' to key derived from declared inputs_considered (construction). - fail-closed-lockdown.md: construction principle in the thesis; §4 checklist re-ordered construction-first / lens-residue; meta = construction-justification. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> * roadmap §0: add Disposition carrier + 'confront skipped modeling decisions' Captures the lens/coproduct disposition decision (operator). One typed carrier (Terminal{reason} | Scaffold{dissolves_to}) for BOTH lens-lifecycle tags AND coproduct dissolve-markers — today freeform 🟡 comments, unreadable by lens since comments aren't Nodes. Decision: middle path (construction-capable carrier + selectively-enforcing lens that ratchets coverage) now, #1 (substrate can't-define-untagged) as the named end-state. The lens is itself a Scaffold{dissolves_to: substrate-mandatory-tag} — self-dissolving when coverage = whole tree. Rejected jumping to #1 on sequencing (load-bearing §4 substrate change → escalate; flag-day migration; derived coproducts need disposition derived not authored), not on principle. Enforceability split: presence = construction (non-optional field, no meta-lens); redundancy (scaffold + successor both present) = hard gate; Terminal-vs-Scaffold correctness = retro/judgment (synthesis-feasibility limit). - docs/plans/disposition-carrier.md (new) - ROADMAP §0 tier-1 + meta 'confront skipped decisions' standing practice Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> * WIP: ROADMAP planning * DESIGN §5/§6: promote construction-over-validation; roadmap: scope-partition §0, testgen §1, shelve dashboard Addresses the review's four flags + sequencing nuance. - DESIGN.md §5: 'correctness by construction, not validation' is now an axiom (a check re-stating a model constraint is a 2nd representation §2/§3; prefer realization derived from a single authority; reserve checks for the unstructurable residue). §6 'enforce with lenses' reconciled: construction first, lens = residue mechanism, AND the executable inert-lens backstop is NOT superseded by the authoring-time construction-justification judgment. (flag 4 home + flag 3) - ROADMAP §0 partitioned: In-scope this window (numeric-tower grounding; cache trustworthy + warm==cold oracle shipped NOW as detective; widen rust gate; promote inert lenses) vs Fenced-OUT fan-out (Value::Null 131-site split; self-host purity gate; cross-tree import activation; Disposition carrier). Honest framing: window reduces fail-open surface, does NOT 'lock' the class — Null split stays open. (flags 1, 2, sequencing nuance) - ROADMAP §0 meta: restored executable inert-lens hygiene backstop, construction- justification layered on top (not 'supersedes'). (flag 3) - De-dup: principle no longer restated in ROADMAP/lockdown §0; both point to DESIGN §5. cache-key construction homed in §7, §0 references it. (flag 4) - ROADMAP §1 = testgen as bug-class oracle (+ affected-set completeness half + parked anemia lens); dashboard shelved to §8. - docs/plans/testgen-oracle.md (new), fail-closed-lockdown.md realigned. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> * WIP: ROADMAP planning * DESIGN §5/§6/§7: wall-vs-ratchet decidability, displaced-pain denominator, open language design Folds in the operator's product thesis + the two bounds that keep it honest. - §5: construction makes a class unwritable only when membership is DECIDABLE — trichotomy (wall now / wall after grounding / ratchet forever); 'never' is the trap (lets an undecidable ratchet masquerade as a wall — optimality by Rice). - §6: denominate the benefit — the deliverable is a displaced cost (§1 time / a paid-for pain), the lens/substrate is the moat not the product; priced in elegance the work is unbounded (the economic twin of 'never'). - §7: the recursion's payoff — language design itself opens up. It's locked by cost (a check = a compiler fork; a language = an adoption problem); both dissolve here (a wall is a row §2, applied over a medium-agnostic substrate §4), so (compiler-fork × language) → (row + medium). Sound where ingest is Lossless, fail-closed where not (DecodeFidelity §4). Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> * WIP: ROADMAP planning * ROADMAP: fix doc-graph violations from bright-eagle-46 review of #5424 Apply the apex axiom/syllogism lens (single authority / no orphan / no cycle) to the roadmap itself — manual acyclicity pass: - orphan: testgen-oracle.md backlinked §1 → repoint §4 (its own lane) - single authority: §0 cache-key now a pure pointer (= §2 F2/F3/P1); §0 numeric-tower marked the authoritative home (§5 de-fork / fork plan point here, no second checkbox) - §0↔§5 cycle: self-host purity reframed as a §5 deliverable §0's expansion-gate depends on (edge §5 → §0-gate → products), not §0-owned - undeclared edge: §7 react/html declares its dependency on §6 media - backlink sweep: the reorg had broken every numeric backlink across 7 plan docs; re-point all and anchor each to the stable section TITLE so a future renumber can't silently break them again Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> * ROADMAP §3 + plan: algorithmic-cost reduction by construction (rewrite, not budget) Reframe §3 from per-fn complexity budgets to the actual intent: rewrite common suboptimal patterns (O(n²)→O(n), O(2ⁿ)→O(n), O(n)→O(log n)) to the cheaper equivalent — construction on the cost axis, not a warning. New plan doc docs/plans/algebraic-rewrite-optimization.md captures the up-front design: the decidability split (modeled EffectShape makes the preconditions structural; equivalence stays undecidable so no optimality oracle), rewrite-rule-as-row + once-proven soundness, the common-case catalog tiered by precondition, D1 canonical-form-is-truth / D2 two seed rules / D4 constant-factor deferred, the four-witness DONE bar (incl. the non-firing control half-done versions skip), and a corpus hit-rate acceptance gate. complexity.dag is the cost oracle; synthesis.dag stays the advisory undecidable residue. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> * ROADMAP §2: Phase-0 measurement instrument done (#5431 peak-RSS) — remaining is the Phase-1 consumer Per quick-ant-298: the measurement keystone was nearly complete — model side already floor-enrolled, step timing already emitted; the only gap was peak-RSS, closed by #5431. P4's Phase-0 dependency is satisfied; remaining is the Phase-1 measured->plan feedback + width-fold (also unblocks §1-C). Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> * plan/§3: detection-vs-enforcement containment (E⊆D′⊆D) + explicit seed-rule I/O up front Grounded in cost.dag U2 + complexity.dag (investigated, not theorized): - detection is TOTAL by construction (kernel-level cost fold; arbitrary fns detectable); boundary is precision (ClassUnknown), not coverage - enforced rewrites are a strict subset structurally guaranteed by the class-drop witness: E ⊆ D′(precise) ⊆ D(all) - n√n excluded for a MODEL reason (PolynomialDegree is integer-only, n^1.5 unrepresentable); ternary search excluded (log base is not a class) - today's small gate roster = subject-production limit (fn-body reflection), NOT a detection limit - new §3a fully specifies the two seed rules up front: input→output→ precondition→non-firing control→discriminating equivalence input, so the worker builds to spec and the project can actually finish Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> * ROADMAP §0/§1: rust-gate is cadence-decoupling, not run-all (per fierce-hawk #5427) The 3-filter allowlist was COST selection, not arbitrary gatekeeping — the v1 SEED compiler costs ~tens of CPU-sec per trivial test, so run-all-per-PR is CPU-hours (off the table). True shape: per-PR cost-bounded subset + measured #[ignore="expensive: Ns"] + completeness lens (#5427); nightly --ignored lane as the destination for expensive + the 58 currently-ignored tests (owned by §1/quick-ant, after #5431, escalate for load-bearing CI-gen). Completeness = every test runs on >=1 cadence (fail-closed). Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> * plan §2a: generalize by structural-redundancy keying (O(n^x)->O(n^(x-1)) free); flag n-log-n as substitution Per operator: catalog must generalize polynomial-degree reduction without edge cases. Resolution: rules key on the structural redundancy, never on degree — degree is not evidence of redundancy (would fire on genuine O(n^x)). A structurally-keyed nested-membership->set peels one level wherever it matches; fold-to-fixpoint gives O(n^3)->O(n^2)->O(n). Cost model supports arbitrary integer degree, so witness (b) holds at every peel. Flagged OPEN (operator input invited): O(n^x)->O(n log n) is algorithmic SUBSTITUTION (different algorithms, same I/O) not redundancy elimination — verges on undecidable equivalence; tractable form is per-idiom rules (sort-based dedup, repeated-min->heap), not a parameterized rule. Seed Rule 1 now authored structurally + carries a depth-2 generalization witness. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> * plan §1b: Unknown is an anemic atom — dissolve over time (reuse Disposition), never a false pass Per operator: classifying Unknown isn't a fixed up-front split — it's the standing anemic-leaf dissolution practice (DESIGN §2 decompress->map->reduce) applied to the cost lens. UnknownCost{diagnostic} already carries its reason; the anemia is the free-form reason. Each decomposition resolves an Unknown to construction (now-precise class -> new D′) or a grounded Terminal (genuinely undecidable, positively recognized -> advisory comment). DFS-first: this IS the Disposition carrier (resolves to construction-or-justified-Terminal), so reuse it, don't fork an unknown-reason enum. Supersedes the static Undecidable|Undetermined split. Two invariants fixed up front: never a false pass (Unknown=>Violates, already holds); every Unknown on the dissolution frontier. cost.dag enrichment + un-parking Disposition are operator-gated. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> * ROADMAP: §3 reverts to budget-gate validation (stability); rewrite-engine relocated to §5 (post-stability) Operator decision 2026-06-21: budget-gate validation is fine for the stability window; the algorithmic-cost REWRITE construction design is expansion, homed with self-hosting (§5) — IR-rewrite/canonicalization is most natural once .dag is the self-hosted truth. - §3 = complexity budget gate (validation): cost-lens symbolic_max fix (#5437) + per-fn subject + budget-gates-whole-codebase (gated on fn-body reflection) + synthesis advisory. #5437 foundation stays in-window. - §5 gains an 'adjacent expansion lane' = the rewrite engine, pointing at the preserved plan doc; marked post-stability. - plan doc status -> POST-STABILITY EXPANSION, relocated to §5. Nothing deleted — the rewrite design is preserved, just fenced out of the stability window (same as Disposition / Value::Null-split). Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> * WIP: ROADMAP planning * #5442 review fix (warm-lark-306): grep-as-authority for the sidecar roster (10 not 9) The §0-guard impl PR (#5445) grepped current main and found 10 importers of extdeps.languages.bash.program, not 9 — the 10th (dsl/gunbc/ci_spec.dag) landed via #5432 after the original pre-merge grep. Rather than bump the frozen count, make the live grep the authority (the roster shrinks to 0 as the bash-sidecar arc migrates consumers, so any frozen number rots — the single-authority point). Also note the two *_test importers are intentionally not walled (guard scans consumer-source roots only). Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> * ROADMAP: check off 6 merged items (catch-up sweep) Flip [ ]→[x] for unambiguously-merged work (PR-ref'd for traceability): - §0 numeric-tower grounding (#5428 — == straddle guard dead-in-corpus) - §0 inert-lens hygiene executable backstop (#5433) - §2 F2/F3 resolved_graph key derived from inputs_considered (#5425) - §3 cost-lens symbolic_max zero-absorption fix (#5437) - §4 gate existing generated testgen output (#5434) - §4 affected-set completeness (#5430) Partial/compound items left for their lane managers to flip in the PR that completes them. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> * ROADMAP §1: add compile-clean-gate force-checks-every-fn-body box (2(ii) fail-open) New floor-coverage item: the compile-clean gate is fail-open — unreached fn bodies escape typecheck, so undefined symbols in dead code pass green (execution-proven on utf8_decode_bytes). Construction fix = typecheck total over every declared body. Owned by §1 (quick-ant); measure-first, operator-gated enforce-flip. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> * ROADMAP §0: correct the 2(ii) box — registry-leak mechanism, not unreached-bodies snappy-gull's deeper diagnosis: the fail-open is NOT unreached bodies (bodies ARE visited). utf8_decode_bytes resolves because it's a global builtin_function_registry entry (04_method.dag, a marked bridge scaffold) not scoped to the compiled tree. Reframe the box to tree-scoped builtin availability / registry partition; instance fix = real std fn + remove the registry bridge entry. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> * WIP: ROADMAP planning * plan doc: enforcement roster is a FROZEN grandfather set, not derived (warm-lark correction) Deriving the realization-vocab exception roster from a live grep would make the guard vacuous (leak = non-edge importer AND NOT-in-roster; derived roster ⇒ every importer always in it ⇒ leak_count always 0 ⇒ never fires). Distinguish the informational prose count (rots, re-grep) from the lens's enforcement roster (frozen, so a new unrostered importer goes RED = the teeth). Add the 11th importer (extdeps_external_authority_transport, the #5418→#5445 race, fixed by #5453) and the roster-completeness assertion as the steady-state race-hardening. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> * WIP: ROADMAP planning * ROADMAP refresh: §1 nightly→Pop-B (opt-level won), §2 resolve-cache GO + P2 de-fork-dependent, §0 census regression + gate-hygiene Reflects decisions/findings that landed 2026-06-21: - §1: the "expensive" tests were debug-build amplification, not intrinsic seed cost (proud-deer cause-table); opt-level=3 (#5456) restores Pop-A to per-PR; nightly lane reduced to Pop-B wet-captures only. Mirror corrected in §0. - §2: resolve-cache enable = GO (~18% floor-wall, purity-proven, #5429-gated); P2 ParseTable dissolution reclassified as a downstream consumer of the dsl→v2 de-fork (keen-otter: v2-local rewire is cosmetic); #5446 realize kernel green. - §0: stage0 clone-census ratchet went inert + the seed regressed 1138 over budget (rust-side coverage-by-illusion + thesis regression; #5427 surfaced it); gate-hygiene rule (floor-enrolled gate must be green-on-main at merge) + roster-completeness assertion promoted to should-land (the #5445 floor-skew). - §1: registry-partition instance fix = #5452 (verified sound). Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> --------- Co-authored-by: Brian Searls <briansrls@gunb.ai> Co-authored-by: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
briansrls
added a commit
that referenced
this pull request
Jun 21, 2026
briansrls
added a commit
that referenced
this pull request
Jun 21, 2026
… peak + live budget (not pinned 4) (#5444) * WIP: §1-C memory-aware width (consume the merged #5431 measurement keystone): * §1-C: derive floor spawn_width from measured peak + live budget (not pinned 4) Wire the measurement->plan loop #5431 opened: gunbc_ci_floor_spawn_width now returns min(shard_count, hardware_threads, floor(0.8*live_budget / measured_peak)) instead of hardware_thread_count(4). - gunbc.ci_floor_measurement (new): committed MEASURED per-shard peak, stamped from #5431's VmHWM emit (run 27893441091: 8400113664 bytes at width 4 => /4 = ~2.1GB/shard), NOT the ~14GB hand-grounded literal #5419 deleted. + dissolve-on drift-gate marker. - std.realization_width: memory_aware_spawn_width fold (pure, v2-inheriting) with a 0.8 safety fraction; fail-closed to a conservative committed width when budget unreadable. - claim_executor: reads the LIVE cgroup memory.max (meminfo fallback) and threads it into the .dag fold via run_in_context_with_args (DESIGN §3 measured=>peripheral: we commit our measurement, read the external-authored budget live). - witnesses: non-binding (4->7), tight-budget backoff, unreadable->fallback, fraction load-bearing, sub-unit->1. Proven by execution: derived spawn_width=7. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> * fmt: rustfmt claim_executor §1-C changes Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> * WIP: §1-C memory-aware width (consume the merged #5431 measurement keystone): * §1-C review fix: type byte fields as std.measure ByteSize (REQUEST_CHANGES) Addresses claude-opus-4-7 REQUEST_CHANGES: the public byte-carrying fields in dsl/std/realization_width.dag (the authority layer) must consume std.measure ByteSize, not flat Int (DESIGN §2/§3 unit modeling). - memory_aware_spawn_width + memory_aware_width_value: memory_budget / per_shard_peak are now ByteSize (the canonical Memory carrier). Counts projected to Int at the boundary via byte_size_count_int (Nat subset Int, the int_min/cores widening idiom). - gunbc.ci_floor_measurement.per_shard_peak_rss_bytes returns ByteSize. - ci_floor_plan grounds the raw host Int budget into byte_size() at the host seam. - internal arithmetic helpers stay Int on extracted counts (not flagged; the placement_supply idiom). Fixes the prior WIP's Int/Nat if-branch type error. Proven by execution: realization_width_witnesses + ci_floor_plan_witnesses green; end-to-end claim_executor still derives spawn_width=7. compile --target rust clean (only the pre-existing unrelated gcp utf8_decode_bytes error remains). Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> * WIP: §1-C memory-aware width (consume the merged #5431 measurement keystone): * WIP: §1-C memory-aware width (consume the merged #5431 measurement keystone): * §1-C: de-anemic measured peak — typed ConcurrentMemoryPeakSample + measure-op per-share derivation Operator review: the floor's measured peak was modeled as two loose data rows (peak: ByteSize + spawn_width: Int) with the per-shard division inlined in the consumer (byte_size(count: byte_size_count(...) / int)) — anemic on two axes: - the observation is a FACT BUNDLE (a peak RSS only meaningful AT the concurrency it was sampled at: concurrent peak ≈ per-share × concurrency) held as two rows that can drift apart and neither reads as 'a measurement' (DESIGN §2/§3); - the per-share derivation was a one-off unwrap/divide/re-ground expression, not a grounded measure operation (DESIGN §4 — operations come from inhabitance). Fix, modeled on the existing std measure-algebra (time_measure_seq/_list_total in std.realization_measurement, which project via measure_count → magnitude arithmetic → reconstruct): - std.realization_measurement: add the agnostic SHAPE — type ConcurrentMemoryPeakSample { peak: ByteSize, concurrency: Int } + concurrent_memory_peak_per_share(sample) that divides the Memory magnitude by the sample concurrency and re-grounds at the same carrier; fail-closed (§5) on non-positive concurrency → whole peak (share count 1). + discriminating witness witness_concurrent_memory_peak_per_share_divides, wired into the keystone test aggregator. - gunbc.ci_floor_measurement: the measured VALUES now live as ONE typed sample (peak 8400113664 @ concurrency 4, §3 measured⇒peripheral); per-shard fn delegates to the std measure op — no inline arithmetic. Green by execution: keystone witnesses true; gunbc_ci_floor_per_shard_peak_rss_bytes() = ByteSize { count: 2100028416 } (= 8400113664 / 4, unchanged); realization_width_witnesses true. Consumer signature (ci_floor_plan) unchanged. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> --------- Co-authored-by: Brian Searls <briansrls@gunb.ai> Co-authored-by: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
What
Phase-0 measurement keystone — the instrument half (per realization-measurement-loop.md §0; scoped by bright-stag-194 to instrument only, defer the economic-tier consumer).
The floor already emits measured step timing (
[measurement] discovery corpus: … resolve <ms>, evalu <ms>) and the model carriers already exist (CostAccount.basis,PerformanceReceipt, the roll-up lenses, and the floor-enrolled discriminator witnessrealization_measurement_keystone_test.dag). The one missing measured fact was memory: the floor executor emitted no peak-RSS at all.This adds it: after the floor run,
claim_executorreads processVmHWM(/proc/self/status) and emitsVmHWMis the concurrent peak across the whole floor run at thatspawn_width— exactly the quantity a memory budget must bound. Per-shard peak ≈ this ÷ effective concurrency (a width=1 run measures one shard's peak directly).Why (construction, not a hand-authored literal)
This is the measured fact that lets the §1-C memory-aware width derivation key on a measured peak rather than the hand-grounded 14 GB literal #5419 deleted as unwired. Same anti-pattern as the cache version-string: a pinned constant standing in for a fact that should be measured. The instrument produces the fact; the width-fold that consumes it is the deferred Phase-1 step.
ci_floor_plan.dag:256(total: cost_account_predicted_zero()) intentionally stays predicted at plan time — there is no measurement before the run; the measured→plan feedback is the deferred consumer, not this PR.Scope / non-goals
Verification
cargo build -p v1-compiler --bin claim_executor --release, exit 0).strings target/release/claim_executor | grep 'floor peak RSS'→ present./procread +eprintln; it does not touch eval, so witness verdicts are unperturbed (the §5 purity property holds by construction for this edit). Fail-soft: printsunavailable(never fabricates) when/proc/self/statusis absent (non-linux).🤖 Generated with Claude Code