diff --git a/ROADMAP.md b/ROADMAP.md index a1df1c4c5b7..4beb806f3fa 100644 --- a/ROADMAP.md +++ b/ROADMAP.md @@ -77,6 +77,8 @@ This window = a few days of STABILITY — shrink the fail-open surface, don't "l - [ ] **confront the skipped modeling decisions** — the `🟡` comment backlog [Disposition plan](docs/plans/disposition-carrier.md) - [ ] **axiom + syllogism lens** (DESIGN open thread #1) — every claim chains back to an axiom, no orphan/cycle; stays `[ ]` until it runs executably over this doc [scope](docs/plans/axiom-syllogism-lens.md) +**Dispatch discipline (anti-stale-ledger, §6):** a lever earns a lane only after it is re-measured against CURRENT main — a displaced cost already paid by another merge is the purity trap (e.g. rust-test sharding, ruled out post-#5427's nextest cut). And the lane/parked list is DERIVED from this authority, never hand-typed (a hand-list drifts exactly like a second representation). The authority tracks ALL planned work; work-items dispatch only the active subset. + ## 1. CI as the substrate integration dogfood (the correctness floor) A flaky or green-but-broken floor means no gate protects anything — so CI is upstream of every §0 claim. CI is also the one workload that flexes *every* substrate layer at once (execution · scheduling · caching · secrets/effects · emission), so it is the forcing function that turns each modeled-but-inert abstraction load-bearing. **Deliverable = shared abstractions proven by CI consuming them** (one Materialization kernel · one Placement authority · one secrets model); faster CI falls *out* of that, it is not the goal (§6 — price the lane in displaced cost, "move with confidence", not elegance). @@ -103,6 +105,7 @@ A flaky or green-but-broken floor means no gate protects anything — so CI is u **Adjacent gaps (smaller, outside the host band):** - [ ] **G4 dispatch dup** — `workflow_dispatch`+PR fire two same-SHA runs; `run_id` concurrency fallback won't collapse them → OOM [decision record](docs/plans/ci-merge-freshness.md) +- [ ] **CI inline-shell de-fork** — `RunStep.run` is raw concat'd bash across ~26 sites; #5427 modeled `cargo.Build.Nextest` but bypasses it for the release build (`ci_release_build_script` hand-writes bash) = a model↔realization fork in one file (+ hardcoded `CARGO_BUILD_JOBS`, pinned nextest version, a bash `uname` arch-case we already model as `TargetArchitecture`). Root: `RunStep` carries modeled effects, not a `String`; revive the inline-shell reducibility lens — §3 transport-fusion de-fork (the N×M adapter trap → one shape + N bound handlers). Sequence after #5427/#5546 (same file). [plan](docs/plans/emission-ingestion-inverse.md) - [ ] **G5 rust-gate selection** — rust fmt/clippy/run-all is all-or-nothing on `.rs` PRs; no affected-set (the `.dag` floor already has one) [plan](docs/plans/ci-selection-vs-scheduling.md) - [ ] **floor runs the right things** — SELECTION (what changed) vs SCHEDULING (by cost); cost never drives selection [plan](docs/plans/ci-selection-vs-scheduling.md) - [x] opt-level=3 restores Pop-A to per-PR (#5456) — merged @@ -115,6 +118,7 @@ A flaky or green-but-broken floor means no gate protects anything — so CI is u - [ ] **one Materialization kernel** — collapse sccache / resolve / ParseTable-memo / RecordedFixture / BuildBuddy onto `realize(subject)` (§2 P2) - [ ] **one Placement authority** — jobs (GitHub) · threads (`spawn_width`) · sessions (ctrl `plans.capacity`) are 3 forks of "put work on a host" +- [ ] **resource budget tree** (§2 one-concept-every-scale, money→memory→infra) — grounded in real accounting (`extdeps.accounting.budget`, anchored, zero-based) generic over `Measure` (money = instantiation #1, memory = #2); a recursive tree where a child's appropriation is a line item charged at its parent (divide-once, structural). Three §5-distinct verdicts, never conflated: **admission** (`admit_all`, zero-based justified-&-approved) is the **construction** path — the committed set is provably within appropriation, over-commit unwritable on it; `node_conserves` is the honest **residue lens** for raw literals (the unstructurable residue, *not* a wall — the §5 distinction); runtime intent-vs-actual **reconcile** is the fail-closed **handler** (evict by QoS / loud-error on unsatisfiable Guaranteed). Subsumes spawn-width (#5444) · placement (#5559) · compile-jobs (#5546) as consumer leaves; a survey found `realization_width` + complexity `EffortBudget` are the SAME capped-resource→claims concept (§3 convergence candidates onto the one authority). **Protective only paired with an enforcement actuator** (admission cap or cgroup `memory.max`, operator-fenced): the model decides budgets, it does not itself prevent the kernel OOM, so interim the L1 claim-count must be the conservative-HIGH ceiling (carrier #5582). [carrier](dsl/product/budget_tree.dag) [grounding](docs/plans/budget-tree.md) - [ ] **shared secrets/effects** — BMC · tokens · sccache-auth modeled once (when the fork is the pain) **Downstream / parked:** @@ -190,7 +194,8 @@ Adjacent lane — algorithmic-cost rewrite engine (the §3 construction design; - [ ] real fixed point: `content_hash` stage1==stage2 (dissolve placeholder hashes) - [ ] wire `regen_stage0 --verify` lockstep gate into CI — enforces no stage0 hand-edits ← **keystone** - [ ] dissolve seed hand-patches (`patch_*` / `HAND_MAINTAINED_STAGE0_FILES`) — the `emit_rust` hand-sync caveat the gate must reproduce: [required facts](docs/plans/regen-verify-gate-required-facts.md) - - [ ] TypeScript to first-class (beyond the `add` slice) + - [ ] **TypeScript self-host (own lane)** — emit the compiler ITSELF as TypeScript and reproduce a per-realization merkle fixed point (the Rust `regen --verify` gate, mirrored for the TS realization). This is what makes "language design collapses to a row" real at full scale — §7 medium-agnostic proof, emit Rust *and* TypeScript, fixed point *per realization*. `5-ts-first-class` is the emit seed; this is the self-host. Gated on the Rust fixed point. + - [ ] TypeScript to first-class (beyond the `add` slice) — the emit SEED - [ ] seed-honesty discharge (Diverse Double-Compiling) - [ ] collapse `src/v1` → pinned v2-emitted seed; delete the 154k hand-written lines (terminal, not a big-bang `rm`) @@ -202,6 +207,7 @@ A program is a canonical `Node` (the *idea*); ingest / emit / eval across many m - [x] **medium axis** — `Medium` + `DecodeFidelity`; `LanguageModel` unified (13 forks dissolved); `compile(Eval) → EvalResult{value: Medium}` - [x] **round-trip law (ingest∘emit = id, DecodeFidelity-bounded)** (#5525/#5527) — established across two structurally-different media: markdown (block-document) and GHA-expr (recursive-expression). v2-TargetModel convergence is the deferred single-authority destination; per-medium round-trips are v1-seed interim. Authority for the law: the round-trip oracle #5513 §5.2 [plan](docs/plans/emission-ingestion-inverse.md) +- [ ] **ingestion as a first-class direction** — fold foreign surface INTO the node tree (the inverse of emit): `Lossless` where decidable, fail-closed `DecodeFidelity` where not, and **emit = ingest⁻¹ over ONE `GrammarRelation`** (§4: one grammar read both directions; the §7 "any language with a typed honesty boundary" payoff). Emission is well-covered (round-trip law, language axis); ingest *at large* — beyond the per-medium round-trips — has no lane. (parser-wall #5553 is one corner; the direction needs an owner.) [plan](docs/plans/emission-ingestion-inverse.md) - [ ] **language axis** — 15+ targets wave-1; English emit proven - [ ] English vocabulary closure → fail-closed English ingest (today's catch-all is fail-open; also §0) - [ ] English ingest round-trip (only emit proven today) diff --git a/docs/plans/budget-tree.md b/docs/plans/budget-tree.md new file mode 100644 index 00000000000..b4aa498eef9 --- /dev/null +++ b/docs/plans/budget-tree.md @@ -0,0 +1,68 @@ +# Resource budget tree — grounding notes + +Carriers: [dsl/extdeps/accounting/budget.dag](../../dsl/extdeps/accounting/budget.dag) (the §3 +authority), [dsl/product/budget_tree.dag](../../dsl/product/budget_tree.dag) (the memory +instantiation). Roadmap node: §1 `1-budget-tree`. PR #5582. + +Rationale is homed here, not in-file: ctrl#1793 strips `.dag` comments tree-wide, so a +comment-heavy carrier would red main when that wall lands. These are the planning-level +grounding facts the carrier cannot carry; the model itself lives on the carrier (§6). + +## 1. Grounded in real accounting (§1 reduce-convention-to-necessity, §3) + +Budgeting is a real, well-developed framework, so the tree is grounded in it rather than in a +coined abstraction: `extdeps.accounting.budget` is the §3 authority, anchored to a real +`ExternalAuthority` (`Https en.wikipedia.org/wiki/Budget`), with the upstream's real names — +`Appropriation` ("max amount for a certain expenditure"), `LineItem`, `BudgetBalance` +(`Surplus | Balanced | Deficit`), `BudgetingMethod` (`ZeroBased | Incremental | ActivityBased`). +Two methods are adopted: **zero-based** (admission) and **appropriation-as-ceiling** +(`within_appropriation`). Being a proper anchored module, it does not trip the unrostered-module +anchor-completeness lens. + +## 2. One concept over Measure (§2 one-concept-every-scale) + +The authority is generic over `Measure`: **money is instantiation #1, memory is #2** (the +product tree binds `Measure`). A future CPU / thread / energy dimension extends the +same surface — never a parallel budget tree. This is realized in code (the generic +`measure_add` / `measure_le` lifted to `std.measure`), not just documented. The QoS class +vocabulary (`Guaranteed` / `Burstable` / `BestEffort`, the Kubernetes QoS classes derived from +cgroup-v2 `memory.{min,low,max}`) follows the same extdeps-anchor grounding pattern as a named +follow-up. + +## 3. The §5 trichotomy — construction vs residue-lens vs handler (never conflated) + +A Bool conservation *check* is **validation**, not construction (it concedes the over-commit is +writable). So the three verdicts are kept distinct: + +- **construction** — `admit_all` (zero-based "justified & approved") builds a committed set + provably within appropriation; over-commit is **unwritable on the admission path**. This is the + real §5 wall. +- **residue lens** — `node_conserves` is an honest Bool lens for **raw literals** that bypass + admission (the unstructurable residue you cannot forbid structurally). It is *not* a wall. +- **handler** — runtime intent-vs-actual `reconcile` (capacity drop → evict by QoS / reschedule / + loud-error on an unsatisfiable `Guaranteed`): a runtime fail-closed handler, not a compile wall. + +The tree is recursive: a child's `Appropriation` is charged as a `LineItem` at its parent, so +`node_conserves` recurses and divide-once is structural. + +## 4. Convergence survey (§3 single authority) + +The budget concept was already forked: `realization_width` (`memory_bounded_fit_count`) and the +complexity gate's `EffortBudget` (op-count) are the SAME capped-resource→claims concept over +different measures. They are **convergence candidates** onto `extdeps.accounting.budget` — future +consumers, reported not refactored (the PR stays atomic). + +## 5. Actuator dependency (the protective-only boundary) + +`admit_all` / `node_conserves` / `reconcile` are MODEL computations: they **decide** budgets, they +do NOT by themselves prevent the kernel OOM. The tree is PROTECTIVE only paired with an +enforcement actuator: + +- (a) admission control holding actual-run-count ≤ authored-claim-count (the merry-otter enforced + cap), **or** +- (b) cgroup `memory.max` caps (operator-fenced). + +On the uncapped fleet the physical OOM-killer pre-empts `reconcile`, so **interim** the authored +L1 run-claim count must be the conservative-HIGH ceiling, never an observed sample. This is the +honest §5 boundary: merging the tree is necessary but not sufficient to end the OOMs — the +actuator is the other half. diff --git a/dsl/gunbc/roadmap_authority.dag b/dsl/gunbc/roadmap_authority.dag index 20efd14fd95..1891e145c45 100644 --- a/dsl/gunbc/roadmap_authority.dag +++ b/dsl/gunbc/roadmap_authority.dag @@ -110,6 +110,7 @@ fn section_0() -> RoadmapSection { ], edges: [], ), + section_prose(content: "**Dispatch discipline (anti-stale-ledger, §6):** a lever earns a lane only after it is re-measured against CURRENT main — a displaced cost already paid by another merge is the purity trap (e.g. rust-test sharding, ruled out post-#5427's nextest cut). And the lane/parked list is DERIVED from this authority, never hand-typed (a hand-list drifts exactly like a second representation). The authority tracks ALL planned work; work-items dispatch only the active subset."), ], } } @@ -146,6 +147,7 @@ fn section_1() -> RoadmapSection { label: "Adjacent gaps (smaller, outside the host band)", nodes: [ authored_pp(id: "1-g4-dispatch", done: false, content: "**G4 dispatch dup** — `workflow_dispatch`+PR fire two same-SHA runs; `run_id` concurrency fallback won't collapse them → OOM", carriers: [ptr(label: "decision record", path: "docs/plans/ci-merge-freshness.md")]), + authored_doc(id: "1-inline-shell-defork", done: false, content: "**CI inline-shell de-fork** — `RunStep.run` is raw concat'd bash across ~26 sites; #5427 modeled `cargo.Build.Nextest` but bypasses it for the release build (`ci_release_build_script` hand-writes bash) = a model↔realization fork in one file (+ hardcoded `CARGO_BUILD_JOBS`, pinned nextest version, a bash `uname` arch-case we already model as `TargetArchitecture`). Root: `RunStep` carries modeled effects, not a `String`; revive the inline-shell reducibility lens — §3 transport-fusion de-fork (the N×M adapter trap → one shape + N bound handlers). Sequence after #5427/#5546 (same file).", path: "docs/plans/emission-ingestion-inverse.md"), authored_doc(id: "1-g5-rust-selection", done: false, content: "**G5 rust-gate selection** — rust fmt/clippy/run-all is all-or-nothing on `.rs` PRs; no affected-set (the `.dag` floor already has one)", path: "docs/plans/ci-selection-vs-scheduling.md"), authored_doc(id: "1-floor-right-things", done: false, content: "**floor runs the right things** — SELECTION (what changed) vs SCHEDULING (by cost); cost never drives selection", path: "docs/plans/ci-selection-vs-scheduling.md"), @@ -166,6 +168,7 @@ fn section_1() -> RoadmapSection { nodes: [ authored(id: "1-materialization-kernel", done: false, content: "**one Materialization kernel** — collapse sccache / resolve / ParseTable-memo / RecordedFixture / BuildBuddy onto `realize(subject)` (§2 P2)"), authored(id: "1-placement-authority", done: false, content: "**one Placement authority** — jobs (GitHub) · threads (`spawn_width`) · sessions (ctrl `plans.capacity`) are 3 forks of \"put work on a host\""), + authored_pp(id: "1-budget-tree", done: false, content: "**resource budget tree** (§2 one-concept-every-scale, money→memory→infra) — grounded in real accounting (`extdeps.accounting.budget`, anchored, zero-based) generic over `Measure` (money = instantiation #1, memory = #2); a recursive tree where a child's appropriation is a line item charged at its parent (divide-once, structural). Three §5-distinct verdicts, never conflated: **admission** (`admit_all`, zero-based justified-&-approved) is the **construction** path — the committed set is provably within appropriation, over-commit unwritable on it; `node_conserves` is the honest **residue lens** for raw literals (the unstructurable residue, *not* a wall — the §5 distinction); runtime intent-vs-actual **reconcile** is the fail-closed **handler** (evict by QoS / loud-error on unsatisfiable Guaranteed). Subsumes spawn-width (#5444) · placement (#5559) · compile-jobs (#5546) as consumer leaves; a survey found `realization_width` + complexity `EffortBudget` are the SAME capped-resource→claims concept (§3 convergence candidates onto the one authority). **Protective only paired with an enforcement actuator** (admission cap or cgroup `memory.max`, operator-fenced): the model decides budgets, it does not itself prevent the kernel OOM, so interim the L1 claim-count must be the conservative-HIGH ceiling (carrier #5582).", carriers: [ptr(label: "carrier", path: "dsl/product/budget_tree.dag"), ptr(label: "grounding", path: "docs/plans/budget-tree.md")]), authored(id: "1-shared-secrets", done: false, content: "**shared secrets/effects** — BMC · tokens · sccache-auth modeled once (when the fork is the pain)"), ], edges: [], @@ -290,7 +293,8 @@ fn section_5() -> RoadmapSection { authored(id: "5-real-fixpoint", done: false, content: "real fixed point: `content_hash` stage1==stage2 (dissolve placeholder hashes)"), authored(id: "5-regen-verify", done: false, content: "wire `regen_stage0 --verify` lockstep gate into CI — enforces no stage0 hand-edits ← **keystone**"), authored_pp(id: "5-dissolve-patches", done: false, content: "dissolve seed hand-patches (`patch_*` / `HAND_MAINTAINED_STAGE0_FILES`) — the `emit_rust` hand-sync caveat the gate must reproduce:", carriers: [ptr(label: "required facts", path: "docs/plans/regen-verify-gate-required-facts.md")]), - authored(id: "5-ts-first-class", done: false, content: "TypeScript to first-class (beyond the `add` slice)"), + authored(id: "5-ts-first-class", done: false, content: "TypeScript to first-class (beyond the `add` slice) — the emit SEED"), + authored(id: "5-ts-selfhost", done: false, content: "**TypeScript self-host (own lane)** — emit the compiler ITSELF as TypeScript and reproduce a per-realization merkle fixed point (the Rust `regen --verify` gate, mirrored for the TS realization). This is what makes \"language design collapses to a row\" real at full scale — §7 medium-agnostic proof, emit Rust *and* TypeScript, fixed point *per realization*. `5-ts-first-class` is the emit seed; this is the self-host. Gated on the Rust fixed point."), authored(id: "5-seed-honesty", done: false, content: "seed-honesty discharge (Diverse Double-Compiling)"), authored(id: "5-collapse-v1", done: false, content: "collapse `src/v1` → pinned v2-emitted seed; delete the 154k hand-written lines (terminal, not a big-bang `rm`)"), ], @@ -303,6 +307,7 @@ fn section_5() -> RoadmapSection { RoadmapEdge { child: nid(s: "5-regen-verify"), parent: nid(s: "5-real-fixpoint") }, RoadmapEdge { child: nid(s: "5-dissolve-patches"), parent: nid(s: "5-regen-verify") }, RoadmapEdge { child: nid(s: "5-ts-first-class"), parent: nid(s: "5-cargo-green") }, + RoadmapEdge { child: nid(s: "5-ts-selfhost"), parent: nid(s: "5-real-fixpoint") }, RoadmapEdge { child: nid(s: "5-seed-honesty"), parent: nid(s: "5-cargo-green") }, RoadmapEdge { child: nid(s: "5-collapse-v1"), parent: nid(s: "5-cargo-green") }, ], @@ -323,6 +328,7 @@ fn section_6() -> RoadmapSection { authored(id: "6-medium-axis", done: true, content: "**medium axis** — `Medium` + `DecodeFidelity`; `LanguageModel` unified (13 forks dissolved); `compile(Eval) → EvalResult\{value: Medium\}`"), derivable_doc(id: "6-roundtrip-law", prs: [5525, 5527], title: "**round-trip law (ingest∘emit = id, DecodeFidelity-bounded)**", description: "— established across two structurally-different media: markdown (block-document) and GHA-expr (recursive-expression). v2-TargetModel convergence is the deferred single-authority destination; per-medium round-trips are v1-seed interim. Authority for the law: the round-trip oracle #5513 §5.2", path: "docs/plans/emission-ingestion-inverse.md"), + authored_doc(id: "6-ingestion-first-class", done: false, content: "**ingestion as a first-class direction** — fold foreign surface INTO the node tree (the inverse of emit): `Lossless` where decidable, fail-closed `DecodeFidelity` where not, and **emit = ingest⁻¹ over ONE `GrammarRelation`** (§4: one grammar read both directions; the §7 \"any language with a typed honesty boundary\" payoff). Emission is well-covered (round-trip law, language axis); ingest *at large* — beyond the per-medium round-trips — has no lane. (parser-wall #5553 is one corner; the direction needs an owner.)", path: "docs/plans/emission-ingestion-inverse.md"), authored(id: "6-language-axis", done: false, content: "**language axis** — 15+ targets wave-1; English emit proven"), authored(id: "6-cross-media", done: false, content: "**cross-media targets beyond syntax** — JSON / react / diagram as first-class media (not stringified)"), authored(id: "6-medium-homo", done: false, content: "`Medium ↔ Medium` homomorphisms"),