diff --git a/docs/plans/ci-humming.md b/docs/plans/ci-humming.md index 668ff2ed3fe..1b4de86a4c7 100644 --- a/docs/plans/ci-humming.md +++ b/docs/plans/ci-humming.md @@ -62,3 +62,7 @@ The hosts co-host the agent-session fleet AND the CI runners. Full safe-by-const ## Critical path to capacity (do first, both hosts ASAP) T0 (un-zero the runner slice) → model derives sane N + per-slot caps → T1+T2 verified-effective apply on srv1+srv2, **with the session slice either capped (5) or oomd-backstopped** → safe by construction (Σ caps + overhead + baselines ≤ physical). T4 (peak → 8GiB) multiplies N afterward. oomd is not required on the critical path. + +## Dissolution trigger (DESIGN §6) + +Delete this doc when CI throughput, wall-clock, and reliability all fall out of the single modeled fleet budget consumed by a verified-effective apply (T0 un-zeroes the runner slice, T1/T2 caps are verified-effective on srv1+srv2, and the session slice is capped or oomd-backstopped) — so capacity is safe by construction rather than hand-managed. diff --git a/docs/plans/edge-b-rust-dag-provenance-brief.md b/docs/plans/edge-b-rust-dag-provenance-brief.md index 9bdbcca28e9..43748303992 100644 --- a/docs/plans/edge-b-rust-dag-provenance-brief.md +++ b/docs/plans/edge-b-rust-dag-provenance-brief.md @@ -1,115 +1,60 @@ # Edge-(b) scoped dispatch brief — rust-test ↔ consumed-.dag provenance (the coverage keystone) -**Status: SCOPING ONLY.** The multi-day build holds for the operator's explicit greenlight. -This document is the decision artifact for that greenlight call. +**Status: SCOPING ONLY.** The multi-day build holds for the operator's explicit greenlight. This document is the decision artifact for that greenlight call. ## Goal -Make the rust↔.dag dependency a **declared structural fact**, recorded once and read in two -directions. It is the single fact under three consumers (DESIGN §4, one grammar both directions), -which is why this is the §1 *coverage keystone*, not a cost follow-up. +Make the rust↔.dag dependency a **declared structural fact**, recorded once and read in two directions. It is the single fact under three consumers (DESIGN §4, one grammar both directions), which is why this is the §1 *coverage keystone*, not a cost follow-up. ## Why — one fact, three consumers -1. **Coverage wall (soundness, fail-closed).** Today a pure-.dag PR fires *no* rust gate: - `any_rust_monolith` (`dsl/tools/rust_stage0_gates.dag`) matches only `.rs`/Cargo/toolchain - suffixes. But rust tests *read* `.dag` via opaque `filesystem_read`/`ws.join`, so a `.dag` - change that breaks a rust test ships **silently green** — a §5 fail-OPEN. That file's own - COMPLETENESS CLAIM ("every change that can alter a rust gate's verdict carries a `.rs`/Cargo - suffix") is *false* for .dag-consuming tests, and its header names per-file rust→.dag - dependence as the deliberately-skipped proper model. Edge-(b) FIRES the rust gate when a - changed `.dag` is in a rust test's declared closure → makes the claim true. This is the - operator's "lock fail-closed before you expand" priority. +1. **Coverage wall (soundness, fail-closed).** Today a pure-.dag PR fires *no* rust gate: `any_rust_monolith` (`dsl/tools/rust_stage0_gates.dag`) matches only `.rs`/Cargo/toolchain suffixes. But rust tests *read* `.dag` via opaque `filesystem_read`/`ws.join`, so a `.dag` change that breaks a rust test ships **silently green** — a §5 fail-OPEN. That file's own COMPLETENESS CLAIM ("every change that can alter a rust gate's verdict carries a `.rs`/Cargo suffix") is *false* for .dag-consuming tests, and its header names per-file rust→.dag dependence as the deliberately-skipped proper model. Edge-(b) FIRES the rust gate when a changed `.dag` is in a rust test's declared closure → makes the claim true. This is the operator's "lock fail-closed before you expand" priority. +2. **Affordability selector.** The *same* declared closure read the other way — skip rust tests whose closure the diff doesn't touch — is the affected-set shrink (the ROADMAP end-state: run-all baseline SHRUNK to affected). cargo has *zero* affected-test selection (every `#[test]` every run; nextest too) and can't see `.dag` deps, so a declared closure is the *only* path to it. +3. **Testgen reflection.** The rust-test→.dag closure is the same provenance testgen needs to regenerate the right tests when a `.dag` node changes. -2. **Affordability selector.** The *same* declared closure read the other way — skip rust tests - whose closure the diff doesn't touch — is the affected-set shrink (the ROADMAP end-state: - run-all baseline SHRUNK to affected). cargo has *zero* affected-test selection (every `#[test]` - every run; nextest too) and can't see `.dag` deps, so a declared closure is the *only* path to it. - -3. **Testgen reflection.** The rust-test→.dag closure is the same provenance testgen needs to - regenerate the right tests when a `.dag` node changes. - -FIRE-when-consumed and SKIP-when-unaffected are the single fact read in opposite directions — -that unification is the moat (one carrier, three consumers). +FIRE-when-consumed and SKIP-when-unaffected are the single fact read in opposite directions — that unification is the moat (one carrier, three consumers). ## The asymmetry that decides what the build buys (construction, not validation) -The two directions have **asymmetric robustness to an incomplete declaration**, and this is the -construction-vs-validation lesson made concrete: +The two directions have **asymmetric robustness to an incomplete declaration**, and this is the construction-vs-validation lesson made concrete: -- **Affordability (skip-unaffected) is fail-SAFE to over-declaration.** Declare too much → you just - run more → never unsound. Robust to a sloppy/partial closure. -- **Coverage (fire-on-change) is fail-OPEN to UNDER-declaration.** If a test reads `.dag` A and B but - its closure declares only A, a change to B does NOT fire the gate → the exact `.dag`→rust fail-open - we are closing, silently re-introduced as **declaration drift**. The coverage wall is only as sound - as the declaration is COMPLETE: **closure ⊇ actual-.dag-reads**. +- **Affordability (skip-unaffected) is fail-SAFE to over-declaration.** Declare too much → you just run more → never unsound. Robust to a sloppy/partial closure. +- **Coverage (fire-on-change) is fail-OPEN to UNDER-declaration.** If a test reads `.dag` A and B but its closure declares only A, a change to B does NOT fire the gate → the exact `.dag`→rust fail-open we are closing, silently re-introduced as **declaration drift**. The coverage wall is only as sound as the declaration is COMPLETE: **closure ⊇ actual-.dag-reads**. -Consequence: the coverage wall's soundness lives entirely in the *completeness* of the closure, which -means a **hand-authored closure is the §3/§5 fork** — for the coverage consumer it silently re-opens -the hole. So the closure MUST be structurally derived (drift-proof); any hand-authored interim must be -marked **NON-SOUND** (delivers affordability only, not the coverage wall). The "shared blocker" below -is therefore not the tail of the work — it is *where the soundness lives*. +Consequence: the coverage wall's soundness lives entirely in the *completeness* of the closure, which means a **hand-authored closure is the §3/§5 fork** — for the coverage consumer it silently re-opens the hole. So the closure MUST be structurally derived (drift-proof); any hand-authored interim must be marked **NON-SOUND** (delivers affordability only, not the coverage wall). The "shared blocker" below is therefore not the tail of the work — it is *where the soundness lives*. ## Bounded core -1. **Declare rust-test → consumed-.dag-paths on the EXISTING `NodeArtifactProvenance` / - `EditLocusBinding` carrier** — no parallel mint (§3 single authority). Implementer must first - verify the carrier shape fits `rust-test-identity → .dag-path list`; if not, add a *sibling - entry on the same authority*, never a new module. -2. **Gate integration is small and precise:** extend `should_run_gates` / `any_rust_monolith` - (`dsl/tools/rust_stage0_gates.dag`) so a changed `.dag` path in the union of declared rust-test - closures ALSO returns true. -3. **Fail-closed default AT THE CONSUMER:** a rust test with no declared closure → *must-run*, - never skip. Absent provenance = run. This keeps the soundness direction safe while declarations - are added incrementally. -4. **Completeness-lens gated — on CORRECTNESS, not presence.** A lens that merely asserts "every - rust test HAS a closure declaration" checks *presence*, which is exactly the §5 trap: it is - satisfiable by editing the declaration while the realization diverges (the faked-cache-key / - dead-field pattern). The lens must check **closure ⊇ actual-.dag-reads** — otherwise a partial or - stale declaration passes the lens AND leaks coverage. Presence-only is not enough; correctness - (the superset relation) is the soundness condition. +1. **Declare rust-test → consumed-.dag-paths on the EXISTING `NodeArtifactProvenance` / `EditLocusBinding` carrier** — no parallel mint (§3 single authority). Implementer must first verify the carrier shape fits `rust-test-identity → .dag-path list`; if not, add a *sibling entry on the same authority*, never a new module. +2. **Gate integration is small and precise:** extend `should_run_gates` / `any_rust_monolith` (`dsl/tools/rust_stage0_gates.dag`) so a changed `.dag` path in the union of declared rust-test closures ALSO returns true. +3. **Fail-closed default AT THE CONSUMER:** a rust test with no declared closure → *must-run*, never skip. Absent provenance = run. This keeps the soundness direction safe while declarations are added incrementally. +4. **Completeness-lens gated — on CORRECTNESS, not presence.** A lens that merely asserts "every rust test HAS a closure declaration" checks *presence*, which is exactly the §5 trap: it is satisfiable by editing the declaration while the realization diverges (the faked-cache-key / dead-field pattern). The lens must check **closure ⊇ actual-.dag-reads** — otherwise a partial or stale declaration passes the lens AND leaks coverage. Presence-only is not enough; correctness (the superset relation) is the soundness condition. ## Shared blocker (testgen-reflection) — this IS the soundness, not optional polish -Per the asymmetry above: the `.dag`-closure must be DISCOVERED structurally, not hand-listed -(hand-listing is the §3/§5 fork that rots, and for the coverage consumer it *silently re-opens the -hole*). The reflection infra exists *partially* — `v2.std.node_query` + `dependency_lens` + the -`affected_set` node-frontier (compile-time, structural over Node/DependencyView). The missing piece: -rust tests reach `.dag` through *opaque host paths* (`ws.join`/`filesystem_read`), so the closure -isn't visible to the Node-tree lens. Surfacing each rust test's `.dag` reads as a declared, -lens-visible dependency is the shared blocker all three consumers wait on — and because the coverage -wall is only sound when `closure ⊇ actual-reads`, this structural discovery is the **load-bearing -core**, not the tail. It is the hard part and the multi-day driver precisely because it is where the -soundness is bought. +Per the asymmetry above: the `.dag`-closure must be DISCOVERED structurally, not hand-listed (hand-listing is the §3/§5 fork that rots, and for the coverage consumer it *silently re-opens the hole*). The reflection infra exists *partially* — `v2.std.node_query` + `dependency_lens` + the `affected_set` node-frontier (compile-time, structural over Node/DependencyView). The missing piece: rust tests reach `.dag` through *opaque host paths* (`ws.join`/`filesystem_read`), so the closure isn't visible to the Node-tree lens. Surfacing each rust test's `.dag` reads as a declared, lens-visible dependency is the shared blocker all three consumers wait on — and because the coverage wall is only sound when `closure ⊇ actual-reads`, this structural discovery is the **load-bearing core**, not the tail. It is the hard part and the multi-day driver precisely because it is where the soundness is bought. ## First vertical slice (smallest end-to-end, green-by-execution) -- Pick ONE rust test with a clear `.dag` closure — `coproduct_reflection_conformance_test` - (inputs entirely `.dag`) is the natural first. +- Pick ONE rust test with a clear `.dag` closure — `coproduct_reflection_conformance_test` (inputs entirely `.dag`) is the natural first. - Declare its consumed-.dag closure on the carrier. - Wire `should_run_gates` to fire when a changed path is in THAT test's declared closure. -- Prove by execution with a discriminating control: a diff to a `.dag` IN the closure FIRES the - gate; a diff to a `.dag` OUTSIDE the closure does NOT. Green = both directions observed. +- Prove by execution with a discriminating control: a diff to a `.dag` IN the closure FIRES the gate; a diff to a `.dag` OUTSIDE the closure does NOT. Green = both directions observed. - This proves the structural fact end-to-end on one test before any corpus fan-out. -- **State explicitly which the slice proves.** For the slice to prove the *coverage direction - soundly*, `coproduct_reflection_conformance_test`'s closure must be **structurally derived** (so a - newly-added `.dag` read is captured automatically). If slice-1 hand-lists the closure as an interim, - it proves the *wiring* (fire/skip plumbing) but NOT the *wall* (drift-proof completeness) — and must - be labelled accordingly. The keystone's value is the wall, so the slice should target the derived - closure, not the hand-listed one. +- **State explicitly which the slice proves.** For the slice to prove the *coverage direction soundly*, `coproduct_reflection_conformance_test`'s closure must be **structurally derived** (so a newly-added `.dag` read is captured automatically). If slice-1 hand-lists the closure as an interim, it proves the *wiring* (fire/skip plumbing) but NOT the *wall* (drift-proof completeness) — and must be labelled accordingly. The keystone's value is the wall, so the slice should target the derived closure, not the hand-listed one. ## Honest estimate Multi-day. + - Slice 1 (one test: declare + gate-fire + discriminating control): ~1 day. -- Shared blocker (structural .dag-closure discovery through opaque host reads, lens-visible): - the bulk — ~2–4 days, depending on whether the host-read seam can surface declarations cheaply - or needs the reflection layer deepened. +- Shared blocker (structural .dag-closure discovery through opaque host reads, lens-visible): the bulk — ~2–4 days, depending on whether the host-read seam can surface declarations cheaply or needs the reflection layer deepened. - Corpus fan-out + completeness lens: after. ## Decoupling -Independent of #5427. #5427 is the cheap `.rs`-hole-closer (widen the rust gate's test command on -`.rs`-touching PRs) — lands now, behind the two operator levers. Edge-(b) is the structural -keystone that later makes the rust gate BOTH sound on `.dag` changes AND affordable by selection. -Neither blocks the other. +Independent of #5427. #5427 is the cheap `.rs`-hole-closer (widen the rust gate's test command on `.rs`-touching PRs) — lands now, behind the two operator levers. Edge-(b) is the structural keystone that later makes the rust gate BOTH sound on `.dag` changes AND affordable by selection. Neither blocks the other. + +## Dissolution trigger (DESIGN §6) + +Delete this brief once edge-(b) is built and merged — the rust-test→consumed-.dag closure is a structurally-derived (drift-proof) declared fact on the NodeArtifactProvenance carrier, the coverage wall fires the rust gate on an in-closure .dag change (closure ⊇ actual-reads, lens-checked on correctness not presence), and the affordability selector skips unaffected rust tests — so the scoping decision this doc records is realized. diff --git a/docs/plans/realization-measurement-loop.md b/docs/plans/realization-measurement-loop.md index e93862462a6..1ba45fb1a6e 100644 --- a/docs/plans/realization-measurement-loop.md +++ b/docs/plans/realization-measurement-loop.md @@ -1,25 +1,16 @@ # Plan — Realization & Measurement: closing the cost → schedule loop (+ infra onto `.dag`) -**Status:** stable coordination plan · dispatch workers per phase · **DESIGN.md + the carriers remain the -authority** — this doc is a worker-dispatch tracker, not a fact ledger, and each phase dissolves into a -mark on its carrier when it lands (DESIGN §6 "no parallel-ledger docs"). A phase's real state is its -branch/PR, not this file (mirrors `ROADMAP.md`). +**Status:** stable coordination plan · dispatch workers per phase · **DESIGN.md + the carriers remain the authority** — this doc is a worker-dispatch tracker, not a fact ledger, and each phase dissolves into a mark on its carrier when it lands (DESIGN §6 "no parallel-ledger docs"). A phase's real state is its branch/PR, not this file (mirrors `ROADMAP.md`). -**Owner:** unowned (original coordinator `zesty-deer-479` archived 2026-06-21) — operator-coordinated; -consolidates the formerly-separate quick-ant-298 dependency-ordered roadmap (single authority, no fork). -Linked from `ROADMAP.md` §2 *Minimal work — caching by realization*. +**Owner:** unowned (original coordinator `zesty-deer-479` archived 2026-06-21) — operator-coordinated; consolidates the formerly-separate quick-ant-298 dependency-ordered roadmap (single authority, no fork). Linked from `ROADMAP.md` §2 *Minimal work — caching by realization*. --- ## 0. Thesis — the substrate is shape-complete but input-starved -The realization layer is *fully modeled and almost entirely inert*: every carrier that should drive -"minimal work, as parallel as possible, guaranteed" exists with the right type and is read by **no -scheduler, fed by **no measurement, consulted by **no router. This is DESIGN §6's failure mode — *"the -tier where the machinery exists but nothing gates on it"* — landed squarely on §1's **cost axis**. +The realization layer is *fully modeled and almost entirely inert*: every carrier that should drive "minimal work, as parallel as possible, guaranteed" exists with the right type and is read by **no scheduler, fed by **no measurement, consulted by **no router. This is DESIGN §6's failure mode — *"the tier where the machinery exists but nothing gates on it"* — landed squarely on §1's **cost axis**. -The fix is **one control loop**, not a pile of local patches (this is why §4 "evaluate the whole -pipeline" is load-bearing, not a footnote): +The fix is **one control loop**, not a pile of local patches (this is why §4 "evaluate the whole pipeline" is load-bearing, not a footnote): ``` measure (Phase 0) ← the keystone; makes cost a real fact @@ -30,103 +21,50 @@ pipeline" is load-bearing, not a footnote): → total rolled up along the CRITICAL PATH, not the node sum (Phase 1.5) ``` -The three notes from the operator are **not peers — they are a dependency chain rooted at measurement**: -`minimal work` = §2 (cache planner) and `as parallel as possible` = §1 (width) can only be *optimized -against a measured cost*, and `guaranteed` = §5 (measured, not predicted). Cost must become a measured -fact before anything can plan against it. The independent CI audit reached the same conclusion ("add the -two-clock timing first"); the dependency structure above is *why*. +The three notes from the operator are **not peers — they are a dependency chain rooted at measurement**: `minimal work` = §2 (cache planner) and `as parallel as possible` = §1 (width) can only be *optimized against a measured cost*, and `guaranteed` = §5 (measured, not predicted). Cost must become a measured fact before anything can plan against it. The independent CI audit reached the same conclusion ("add the two-clock timing first"); the dependency structure above is *why*. ### The end-state acceptance gate (what the whole plan builds to) -> For every pure transform `T` (resolve, parse, typecheck, *and* derived analyses like -> complexity-synthesis / affected-set — see `ROADMAP.md` §3 *Complexity / synthesis lens* and §4 *Testgen*), `realize(T)` returns a result -> content-addressed by `hash(inputs ⊕ content(T))`, materialized at the **minimal `Placement` spanning -> T's consumers (its reach)**. A transform that is **non-redundant** (shared across a layer boundary, or -> recompute-cost > cache-cost) with **no cache supplier at its reach layer** is a located, typed -> **ERROR** that emits a *request to provision a supplier there*. No silent `Recompute`; no under-keyed -> hit. +> For every pure transform `T` (resolve, parse, typecheck, *and* derived analyses like complexity-synthesis / affected-set — see `ROADMAP.md` §3 *Complexity / synthesis lens* and §4 *Testgen*), `realize(T)` returns a result content-addressed by `hash(inputs ⊕ content(T))`, materialized at the **minimal `Placement` spanning T's consumers (its reach)**. A transform that is **non-redundant** (shared across a layer boundary, or recompute-cost > cache-cost) with **no cache supplier at its reach layer** is a located, typed **ERROR** that emits a *request to provision a supplier there*. No silent `Recompute`; no under-keyed hit. -This is §5 (fail-closed) turned on the cost axis: uncached non-redundant work is not "slow", it is an -*error*. The earliest truthful point to assert it is the **redundancy-only** cut (shared-across-boundary -— needs reach, not measurement); the cost-based "non-redundant" half waits on measured cost (Phase 0 / -§4). The phases below are the path to this gate; the dependency-ordered spine that maps work items onto -it is in **§ Dependency-ordered spine** (before Sequencing). +This is §5 (fail-closed) turned on the cost axis: uncached non-redundant work is not "slow", it is an *error*. The earliest truthful point to assert it is the **redundancy-only** cut (shared-across-boundary — needs reach, not measurement); the cost-based "non-redundant" half waits on measured cost (Phase 0 / §4). The phases below are the path to this gate; the dependency-ordered spine that maps work items onto it is in **§ Dependency-ordered spine** (before Sequencing). ### The invariant that governs every phase (DESIGN §3 / §4) -> **Pure schedule TOPOLOGY stays central and deterministic; every measurement-fed decision is a -> PERIPHERAL realization.** - -The schedule (`Schedule = List>`) is a deterministic partial order — it expresses what -*can* run in parallel, hardware-free, and is pinned by the `schedule_eq` / -`schedule_generates_identical_schedule` witnesses (`realization_schedule.dag:222-236`; -`src/v2/test/claim/realization_schedule_witness.dag:35-48`). A schedule whose *width or membership* -depended on a measured per-machine `HardwareThreadCount` would break that equality across hosts. So: -**measured ⇒ peripheral, by construction.** Width, shard balance, cache-layer choice, and the timing tap -all live in the periphery (`extdeps/realization`, the host realizer), checked by *"given these -DeploymentFacts + these measured costs, the realizer picks X"* witnesses — deterministic *given their -inputs*. This is exactly what the `CostAccount` dissolve-on comment anticipates -(`realization_schedule.dag:25-26`). Most `.dag` programs are stateless/short-lived: they declare -dependency structure and never mention hardware; the width-fold degenerates to "just run it." +> **Pure schedule TOPOLOGY stays central and deterministic; every measurement-fed decision is a PERIPHERAL realization.** + +The schedule (`Schedule = List>`) is a deterministic partial order — it expresses what *can* run in parallel, hardware-free, and is pinned by the `schedule_eq` / `schedule_generates_identical_schedule` witnesses (`realization_schedule.dag:222-236`; `src/v2/test/claim/realization_schedule_witness.dag:35-48`). A schedule whose *width or membership* depended on a measured per-machine `HardwareThreadCount` would break that equality across hosts. So: **measured ⇒ peripheral, by construction.** Width, shard balance, cache-layer choice, and the timing tap all live in the periphery (`extdeps/realization`, the host realizer), checked by *"given these DeploymentFacts + these measured costs, the realizer picks X"* witnesses — deterministic *given their inputs*. This is exactly what the `CostAccount` dissolve-on comment anticipates (`realization_schedule.dag:25-26`). Most `.dag` programs are stateless/short-lived: they declare dependency structure and never mention hardware; the width-fold degenerates to "just run it." ### Realization has THREE dimensions (schedule · cache · compute-fabric) -"Realization" is one concept with three orthogonal-but-composed dimensions, **all keyed on the same -content-addressed `ExecutionReceipt`**, all **peripheral** (§3), all governed by the **same measured cost -+ Pareto objective**: +"Realization" is one concept with three orthogonal-but-composed dimensions, **all keyed on the same content-addressed `ExecutionReceipt`**, all **peripheral** (§3), all governed by the **same measured cost + Pareto objective**: | Dimension | Carrier | Asks | §1 axis | -|---|---|---|---| +| --- | --- | --- | --- | | **schedule** | `std.realization_schedule` | *when / how parallel* | parallel | | **cache** | `std.cache_interface` | *whether it needs to run at all* | §2 minimal work | | **compute fabric** | `product.compute_fabric` | *where / on what it runs* (provision) | placement / $ | -The proof they are dimensions of *one* concept rather than three separate models is **structural and -already in the tree**: cache `MUST NOT import compute_fabric` (`cache_interface.dag:4`) and compute_fabric -`MUST NOT import cache_interface` (`compute_fabric.dag:9`); **both compose only over `ExecutionReceipt`**. -They meet *only* at the content-addressed receipt — never by direct coupling (§3/§4). - -**The `compute_fabric()` zero-arg interface is the same §3 move as the whole plan.** `compute_fabric` is a -**demand → placement → supply** market: an execution emits a `WorkDemand` (isolation, memory, GPU) and -`satisfies(offer, demand)` (`compute_fabric.dag:377`) places it on a satisfying `ComputeOffer`. "Provision -compute for this execution" with **empty args** = the `WorkDemand` is *inferred from the .dag-modeled -execution*, and placement is *resolved from the deployment's offers* — **neither is a caller argument**. -Identical to the cache planner auto-wiring and the scheduler's hardware-budget fold: *caller declares -intent; the realization is resolved from modeled deployment facts.* All three dimensions share this. - -**Layering discipline (§3):** `compute_fabric` and `placement_supply` are **product**; schedule/cache are **std** (imports point -toward std). Split: product owns the *placement projection carrier* (`product.placement_supply` ✓) and std owns the `{time,space,power}` -cost-axis measure carriers it composes; product `compute_fabric` owns the **$/billing axis** (`CostClass`, `MoneyMicros`) and *projects* -fleet rows into that carrier (`placement_supply_row`, `compute_fabric.dag:220`); the **peripheral host -realizer** bridges product→std and runs the Pareto pick. std stays product-free. +The proof they are dimensions of *one* concept rather than three separate models is **structural and already in the tree**: cache `MUST NOT import compute_fabric` (`cache_interface.dag:4`) and compute_fabric `MUST NOT import cache_interface` (`compute_fabric.dag:9`); **both compose only over `ExecutionReceipt`**. They meet *only* at the content-addressed receipt — never by direct coupling (§3/§4). + +**The `compute_fabric()` zero-arg interface is the same §3 move as the whole plan.** `compute_fabric` is a **demand → placement → supply** market: an execution emits a `WorkDemand` (isolation, memory, GPU) and `satisfies(offer, demand)` (`compute_fabric.dag:377`) places it on a satisfying `ComputeOffer`. "Provision compute for this execution" with **empty args** = the `WorkDemand` is *inferred from the .dag-modeled execution*, and placement is *resolved from the deployment's offers* — **neither is a caller argument**. Identical to the cache planner auto-wiring and the scheduler's hardware-budget fold: *caller declares intent; the realization is resolved from modeled deployment facts.* All three dimensions share this. + +**Layering discipline (§3):** `compute_fabric` and `placement_supply` are **product**; schedule/cache are **std** (imports point toward std). Split: product owns the *placement projection carrier* (`product.placement_supply` ✓) and std owns the `{time,space,power}` cost-axis measure carriers it composes; product `compute_fabric` owns the **$/billing axis** (`CostClass`, `MoneyMicros`) and *projects* fleet rows into that carrier (`placement_supply_row`, `compute_fabric.dag:220`); the **peripheral host realizer** bridges product→std and runs the Pareto pick. std stays product-free. ### v2 is the target; v1 is the proving ground (DESIGN §7) -v1 (the Rust seed) is shrinking to zero; v2 (the self-hosted `.dag` compiler) is what must benefit. -**Every phase's durable artifact is `.dag` that v2 inherits; the Rust seed is only the proving *handler* -— where a host-effect attaches today, while v2 is mid-bootstrap and the v1 interpreter is still the only -evaluator that actually runs.** You MAY edit v1 (it's a proving ground), but: - -> **The v2-benefit test:** if a phase's deliverable is a Rust patch with *no `.dag` model*, it failed. -> The carrier / lens / kernel / effect-shape is the artifact; the Rust code is one handler of it -> (§2 one-shape-N-handlers; §3 measured⇒peripheral; §7 Rust→zero). - -This is *why* the keystone's measurement is modeled as an **effect-shape + `PerformanceReceipt` carrier + -a roll-up lens over the Node fold** (the same `fold_node` v2's own evaluator uses) — so when v2 self-hosts, -the instrumentation, the cache kernel, the scheduler, and the fabric all come along for free. The Rust tap -in `v1_interpreter.rs` *proves* the model green-by-execution today; it is the realization, not the -authority. Per-phase split: **Phase 0** durable = the `.dag` measure model/lens, proving = the Rust eval -tap; **Phase 1** durable = the `.dag` width-fold (`scheduler.dag` is already v2), proving = the -`claim_executor` spawn cap; **Phase 1.5a/2/3** are already `.dag`-native (`v2.lens.affected_set`, the -cache catalog/kernel, `compute_fabric`/`ci_yaml_emit`) — v2-inheriting by construction; only the cache -*backends* (`resolved_graph_cache.rs`, `ParseTableMemo`) stay v1 handlers of the one `.dag` kernel. +v1 (the Rust seed) is shrinking to zero; v2 (the self-hosted `.dag` compiler) is what must benefit. **Every phase's durable artifact is `.dag` that v2 inherits; the Rust seed is only the proving *handler* — where a host-effect attaches today, while v2 is mid-bootstrap and the v1 interpreter is still the only evaluator that actually runs.** You MAY edit v1 (it's a proving ground), but: + +> **The v2-benefit test:** if a phase's deliverable is a Rust patch with *no `.dag` model*, it failed. The carrier / lens / kernel / effect-shape is the artifact; the Rust code is one handler of it (§2 one-shape-N-handlers; §3 measured⇒peripheral; §7 Rust→zero). + +This is *why* the keystone's measurement is modeled as an **effect-shape + `PerformanceReceipt` carrier + a roll-up lens over the Node fold** (the same `fold_node` v2's own evaluator uses) — so when v2 self-hosts, the instrumentation, the cache kernel, the scheduler, and the fabric all come along for free. The Rust tap in `v1_interpreter.rs` *proves* the model green-by-execution today; it is the realization, not the authority. Per-phase split: **Phase 0** durable = the `.dag` measure model/lens, proving = the Rust eval tap; **Phase 1** durable = the `.dag` width-fold (`scheduler.dag` is already v2), proving = the `claim_executor` spawn cap; **Phase 1.5a/2/3** are already `.dag`-native (`v2.lens.affected_set`, the cache catalog/kernel, `compute_fabric`/`ci_yaml_emit`) — v2-inheriting by construction; only the cache *backends* (`resolved_graph_cache.rs`, `ParseTableMemo`) stay v1 handlers of the one `.dag` kernel. --- ## Verified ground truth (file:line — do not re-derive) | Fact | Evidence | -|---|---| +| --- | --- | | Schedule width = full dependency frontier, **no capacity bound** | `ReadinessLayer.ready: List` `src/v2/workflow/scheduler.dag:29`; `runnable_frontier_from_dependencies` `scheduler.dag:147-154` | | Thread-spawn **unbounded by hardware** (one OS thread per runnable-in-batch) | `thread::spawn(... run_one_runnable ...)` `src/v1/stage0/src/bin/claim_executor.rs:403-410` | | Corpus = **one** `RunnableDiscoveryBatch` node → serial `for` loop (293 witnesses invisible) | `ci_floor_plan.dag:107`; `run_discovery_corpus` serial loop `cli_run.rs:2148-2171` | @@ -149,46 +87,16 @@ cache catalog/kernel, `compute_fabric`/`ci_yaml_emit`) — v2-inheriting by cons ## Phase 0 — Measured cost (THE KEYSTONE) -**Goal:** flip `CostAccount.time` from `predicted_zero` to `Measured`. Everything quantitative depends on -this. NB: the timing *primitives already exist* — this is **"wire the existing tap to a content-hash key -+ CostAccount,"** not "build timing from scratch." - -- **Grain decision (settled this session): key on the content-hash of the cache SUBJECT, not per-AST-node, - not per-variant.** Rationale: the `Node` is an `Rc` with **no ambient content-hash** (today the - profiler keys by `expr_variant_index`), so per-node hashing at `eval_expr` is *not free* and would - perturb the measurement (§5 observer effect). The cache-subject frame is exactly where a content-hash - *is already computed*, and it is the grain the scheduler (per-Runnable) and the cache router - (per-subject recompute cost) both consume — so per-subject is the §2 "model once, derive every use" - point: per-Runnable is its aggregate, per-variant its `group-by`, full per-node an **opt-in deep - projection** over the same seam. Per-variant counters are a *dead end* (a variant is not a cacheable - identity → can't feed Phase 2). -- **Instrumentation = the dual of the cache.** Both wrap the same fold boundary keyed by the same - content-hash: the cache stores node→value, the instrument stores node→duration. The *analysis* is a pure - lens; the measurement itself is a §1 host-effect. Use the existing gross−children self-time decomposition - (`v1_interpreter.rs:1466-1476`). -- **The measurement output is a `PerformanceReceipt`, NOT a new struct (§3 — do not coin a 4th).** The - observation carrier already exists: `compute_fabric.PerformanceReceipt{ wall_duration, sample_count, - confidence }` (`compute_fabric.dag:414-423`), and `ExecutionReceipt.performance` (`:453`) already hangs it - on the receipt. So Phase 0 emits a `PerformanceReceipt` keyed by the cache-subject hash → it rolls up into - `CostAccount.time` (the aggregate). This is what *fuses the keystone to the compute-fabric deliverable*: - the thing Phase 0 measures **is** the fabric's execution receipt, and `MeasurementConfidence` - (SingleSample/Range/DistributionSummary) is exactly the per-witness-distribution honesty the audit's - observability gap needs. -- **Feed `CostAccount`.** Add `CostBasis = Measured | Predicted` (the `:25-26` dissolve-on); aggregate - PerformanceReceipts → `RealizationPlan.total`. -- **Converge the time authorities — there are THREE, not two (§3).** `NanosecondDuration` (`measure.dag:258`) - is the authority. `TestNodeCostDimension.measured_ms` (Milliseconds, `verification.dag`) **dissolves** - into a budget-*predicate* over the measured `CostAccount.time` (a ns threshold), not a parallel measured - field (ms truncates a 5 ns step to 0 — DESIGN §6). And `PerformanceReceipt.wall_duration` is the - *observation* feeding the roll-up — observation vs roll-up, not a fork. Net: one observation carrier - (`PerformanceReceipt`), one roll-up (`CostAccount.time`), `measured_ms` deleted. -- **Persist the dropped timing.** Carry per-witness/per-entry timing through `DiscoverySummary` and the - floor path (`claim_executor`), closing the audit's observability gap (the "two-clock" per-entry-resolve - vs aggregate-per-witness split) — which is *itself* the profiling the operator was about to do by hand, - made first-class. +**Goal:** flip `CostAccount.time` from `predicted_zero` to `Measured`. Everything quantitative depends on this. NB: the timing *primitives already exist* — this is **"wire the existing tap to a content-hash key + CostAccount,"** not "build timing from scratch." + +- **Grain decision (settled this session): key on the content-hash of the cache SUBJECT, not per-AST-node, not per-variant.** Rationale: the `Node` is an `Rc` with **no ambient content-hash** (today the profiler keys by `expr_variant_index`), so per-node hashing at `eval_expr` is *not free* and would perturb the measurement (§5 observer effect). The cache-subject frame is exactly where a content-hash *is already computed*, and it is the grain the scheduler (per-Runnable) and the cache router (per-subject recompute cost) both consume — so per-subject is the §2 "model once, derive every use" point: per-Runnable is its aggregate, per-variant its `group-by`, full per-node an **opt-in deep projection** over the same seam. Per-variant counters are a *dead end* (a variant is not a cacheable identity → can't feed Phase 2). +- **Instrumentation = the dual of the cache.** Both wrap the same fold boundary keyed by the same content-hash: the cache stores node→value, the instrument stores node→duration. The *analysis* is a pure lens; the measurement itself is a §1 host-effect. Use the existing gross−children self-time decomposition (`v1_interpreter.rs:1466-1476`). +- **The measurement output is a `PerformanceReceipt`, NOT a new struct (§3 — do not coin a 4th).** The observation carrier already exists: `compute_fabric.PerformanceReceipt{ wall_duration, sample_count, confidence }` (`compute_fabric.dag:414-423`), and `ExecutionReceipt.performance` (`:453`) already hangs it on the receipt. So Phase 0 emits a `PerformanceReceipt` keyed by the cache-subject hash → it rolls up into `CostAccount.time` (the aggregate). This is what *fuses the keystone to the compute-fabric deliverable*: the thing Phase 0 measures **is** the fabric's execution receipt, and `MeasurementConfidence` (SingleSample/Range/DistributionSummary) is exactly the per-witness-distribution honesty the audit's observability gap needs. +- **Feed `CostAccount`.** Add `CostBasis = Measured | Predicted` (the `:25-26` dissolve-on); aggregate PerformanceReceipts → `RealizationPlan.total`. +- **Converge the time authorities — there are THREE, not two (§3).** `NanosecondDuration` (`measure.dag:258`) is the authority. `TestNodeCostDimension.measured_ms` (Milliseconds, `verification.dag`) **dissolves** into a budget-*predicate* over the measured `CostAccount.time` (a ns threshold), not a parallel measured field (ms truncates a 5 ns step to 0 — DESIGN §6). And `PerformanceReceipt.wall_duration` is the *observation* feeding the roll-up — observation vs roll-up, not a fork. Net: one observation carrier (`PerformanceReceipt`), one roll-up (`CostAccount.time`), `measured_ms` deleted. +- **Persist the dropped timing.** Carry per-witness/per-entry timing through `DiscoverySummary` and the floor path (`claim_executor`), closing the audit's observability gap (the "two-clock" per-entry-resolve vs aggregate-per-witness split) — which is *itself* the profiling the operator was about to do by hand, made first-class. - **§5 gate:** purity oracle — witness verdicts byte-identical instrumented vs not. -- **Dissolution trigger:** `cost_account_predicted_zero()` has no callers on the floor path; `measured_ms` - deleted. +- **Dissolution trigger:** `cost_account_predicted_zero()` has no callers on the floor path; `measured_ms` deleted. --- @@ -196,43 +104,20 @@ this. NB: the timing *primitives already exist* — this is **"wire the existing **Depends on:** Phase 0 (shard balance needs measured per-shard cost). -- **Explode the corpus node** (`ci_floor_plan.dag:107`) into per-entry-group `Runnable`s — **rows, not - Rust**. Express it as a `WorkDemand` whose `parallelism = IndependentShards{shard_count}` - (`compute_fabric.dag:282`) — the corpus is today a *degenerate (unsharded) projection* of exactly that, - so this reuses the carrier rather than minting a scheduler-local shard list. Shard *by whole entry-group* - to preserve the warm `typed_module_cache` (splitting an entry's witnesses re-incurs its cold resolve). - This is the keystone both background audits independently named. -- **The hardware budget is what `compute_fabric` PROVISIONS — do not coin a fresh carrier (§2/§3).** The - width-fold reads the `PlacementSupplyRow` that `compute_fabric` already projects (`placement_supply_row`, - `compute_fabric.dag:220`; `PlacementSupplyRow.hardware_threads` `placement_supply.dag:29-31`). **The - width decision *is* a placement decision:** today `satisfies(offer, demand)` (`compute_fabric.dag:377`) - checks *isolation only* — Phase 1 is "add the thread-count / Pareto dimension to placement." So this - phase is co-designed with Phase 3 (compute_fabric is the provisioning interface; the runner *declares* - the offer, the scheduler *consumes* the placement — one market, two readers). DFS `PlacementSupplyRow` + - `CpuDeploymentFacts` (`cpu/types.dag:42`) before extending; do **not** invent `DeploymentFacts`. -- **The width-fold.** Schedule stays the pure partial order; a peripheral realizer folds it against the - `HardwareBudget` → actual width, a Pareto pick over `{wall-time↓, peak-memory↓}` bounded by `width ≤ - cores` — reusing `std.pareto` + `RealizationObjective.goals` (already `List` — wiring carriers - that already speak the same vocabulary, not inventing one). -- **Bound the spawner** (`claim_executor.rs:403-410`) by `available_parallelism`/budget — fixes the *dual* - hazard: under-parallel (serial corpus) **and** over-parallel (unbounded spawn on a wide batch). -- **Determinism:** schedule topology stays witness-stable; width/shard are peripheral, checked by - given-these-facts witnesses. +- **Explode the corpus node** (`ci_floor_plan.dag:107`) into per-entry-group `Runnable`s — **rows, not Rust**. Express it as a `WorkDemand` whose `parallelism = IndependentShards{shard_count}` (`compute_fabric.dag:282`) — the corpus is today a *degenerate (unsharded) projection* of exactly that, so this reuses the carrier rather than minting a scheduler-local shard list. Shard *by whole entry-group* to preserve the warm `typed_module_cache` (splitting an entry's witnesses re-incurs its cold resolve). This is the keystone both background audits independently named. +- **The hardware budget is what `compute_fabric` PROVISIONS — do not coin a fresh carrier (§2/§3).** The width-fold reads the `PlacementSupplyRow` that `compute_fabric` already projects (`placement_supply_row`, `compute_fabric.dag:220`; `PlacementSupplyRow.hardware_threads` `placement_supply.dag:29-31`). **The width decision *is* a placement decision:** today `satisfies(offer, demand)` (`compute_fabric.dag:377`) checks *isolation only* — Phase 1 is "add the thread-count / Pareto dimension to placement." So this phase is co-designed with Phase 3 (compute_fabric is the provisioning interface; the runner *declares* the offer, the scheduler *consumes* the placement — one market, two readers). DFS `PlacementSupplyRow` + `CpuDeploymentFacts` (`cpu/types.dag:42`) before extending; do **not** invent `DeploymentFacts`. +- **The width-fold.** Schedule stays the pure partial order; a peripheral realizer folds it against the `HardwareBudget` → actual width, a Pareto pick over `{wall-time↓, peak-memory↓}` bounded by `width ≤ cores` — reusing `std.pareto` + `RealizationObjective.goals` (already `List` — wiring carriers that already speak the same vocabulary, not inventing one). +- **Bound the spawner** (`claim_executor.rs:403-410`) by `available_parallelism`/budget — fixes the *dual* hazard: under-parallel (serial corpus) **and** over-parallel (unbounded spawn on a wide batch). +- **Determinism:** schedule topology stays witness-stable; width/shard are peripheral, checked by given-these-facts witnesses. - **Dissolution trigger:** the corpus is ≥2 runnables in the schedule; the spawner reads a budget. --- ## Phase 1.5 — Holistic cleanups (note 4) · mostly parallel to 1 -- **Wire `affected_set` into the corpus + gate roster** (audit lever #1). The compile-time, fail-closed - `v2.lens.affected_set` + runner + superset proof exist and are green but unimported. Skip only on a - content-addressed match to a verified-green baseline; **fail closed** on any miss. Biggest wall-clock - lever on PR branches. (Independent of Phase 0.) -- **`total` = measured critical-path roll-up** (note 4): weights a short phase *on the critical path* - (the perturb gate) at full cost and a short phase *hidden under a parallel branch* at ~0. (Needs Phase 0.) -- **Collapse the perturb cold-recompile** (~14 s, fail-fast root, critical path): resolve the planted - (fresh-name, unimported) module against the green compile's index instead of `cp -r dsl` + cold rebuild; - preserves the discriminating-red (§5). (Independent of Phase 0.) +- **Wire `affected_set` into the corpus + gate roster** (audit lever #1). The compile-time, fail-closed `v2.lens.affected_set` + runner + superset proof exist and are green but unimported. Skip only on a content-addressed match to a verified-green baseline; **fail closed** on any miss. Biggest wall-clock lever on PR branches. (Independent of Phase 0.) +- **`total` = measured critical-path roll-up** (note 4): weights a short phase *on the critical path* (the perturb gate) at full cost and a short phase *hidden under a parallel branch* at ~0. (Needs Phase 0.) +- **Collapse the perturb cold-recompile** (~14 s, fail-fast root, critical path): resolve the planted (fresh-name, unimported) module against the green compile's index instead of `cp -r dsl` + cold rebuild; preserves the discriminating-red (§5). (Independent of Phase 0.) --- @@ -240,116 +125,47 @@ this. NB: the timing *primitives already exist* — this is **"wire the existing **Depends on:** Phase 0 (cost-aware reach needs measured recompute cost). -- **Land the planner the catalog header already promises** (`cache_interface.dag:21` "downstream cache - lookup planner"; dissolve-on-arrival "when first consumer lands"). Given the `CacheInterfaceFacts` rows + - a deployment's *available* backends, emit a `CacheLayerPlan` (type exists, `:91`): L1 in-process → L2 - sccache / cargo target / resolved-graph → L3 CAS. -- **One content-address lookup kernel, N backends bound by `transport_encoding`** (§4 one-kernel/N-handlers). - The in-process memo is just the `InProcess` row of the *same* kernel. **Converge the key derivations onto - ONE content-addressed subject identity.** Today there are *four* keyings: `parse_cache` by path, - `typed_module_cache` by module-name, `resolved_graph` by content-hash, `pure_call_memo` by address — **and - the `ExecutionReceipt` digest the whole three-dimension unification rests on is itself a 4th stub**: - `execution_receipt_digest` returns `receipt.work.id`, a hand-authored brand, not a content hash - (`compute_fabric.dag:588-594`). The §0 thesis ("all three dimensions keyed on one `ExecutionReceipt`") - is only *true once this digest becomes a real content hash aligned with the cache-subject identity* — so - this convergence is shared work between Phase 2 (cache) and the compute-fabric track, not cache-local. - The `key_derivation` axis exists for exactly this. -- **Cost-aware reach (§1).** Reach for a layer only when its predicted delta favors it: - `min(recompute, lookup + p(miss)·recompute)` — `read_latency` (InProcessNs…WanTensMs) is already a - modeled axis; `recompute` comes from Phase 0. A WAN CAS hit can lose to recomputing a cheap node. -- **Auto-wire (the operator's "user shouldn't wire it themselves").** The deployment declares which - backends it offers; the planner emits the wiring — dissolving the bespoke `if sccache --show-stats` - shell in `ci.yml` and the `GUNBC_RESOLVED_GRAPH_CACHE_DIR` env read. -- **Fail-closed (§5).** A backend probe that is absent/unauthorized falls through to the next layer → - ultimately recompute, **never** serves a stale/unverified hit (`CacheRejectReason` already enumerates - `BackendUnavailable`/`BackendUnauthorized`). Verdict-identity, not byte-identity, until the deferred - canonical-byte compare lands — so do NOT route emit/lower consumers through it yet. -- **First free measurement:** un-dormant `resolved_graph_cache` in CI (read by the seed, unset in - `ci.yml`) as a warm A/B. +- **Land the planner the catalog header already promises** (`cache_interface.dag:21` "downstream cache lookup planner"; dissolve-on-arrival "when first consumer lands"). Given the `CacheInterfaceFacts` rows + a deployment's *available* backends, emit a `CacheLayerPlan` (type exists, `:91`): L1 in-process → L2 sccache / cargo target / resolved-graph → L3 CAS. +- **One content-address lookup kernel, N backends bound by `transport_encoding`** (§4 one-kernel/N-handlers). The in-process memo is just the `InProcess` row of the *same* kernel. **Converge the key derivations onto ONE content-addressed subject identity.** Today there are *four* keyings: `parse_cache` by path, `typed_module_cache` by module-name, `resolved_graph` by content-hash, `pure_call_memo` by address — **and the `ExecutionReceipt` digest the whole three-dimension unification rests on is itself a 4th stub**: `execution_receipt_digest` returns `receipt.work.id`, a hand-authored brand, not a content hash (`compute_fabric.dag:588-594`). The §0 thesis ("all three dimensions keyed on one `ExecutionReceipt`") is only *true once this digest becomes a real content hash aligned with the cache-subject identity* — so this convergence is shared work between Phase 2 (cache) and the compute-fabric track, not cache-local. The `key_derivation` axis exists for exactly this. +- **Cost-aware reach (§1).** Reach for a layer only when its predicted delta favors it: `min(recompute, lookup + p(miss)·recompute)` — `read_latency` (InProcessNs…WanTensMs) is already a modeled axis; `recompute` comes from Phase 0. A WAN CAS hit can lose to recomputing a cheap node. +- **Auto-wire (the operator's "user shouldn't wire it themselves").** The deployment declares which backends it offers; the planner emits the wiring — dissolving the bespoke `if sccache --show-stats` shell in `ci.yml` and the `GUNBC_RESOLVED_GRAPH_CACHE_DIR` env read. +- **Fail-closed (§5).** A backend probe that is absent/unauthorized falls through to the next layer → ultimately recompute, **never** serves a stale/unverified hit (`CacheRejectReason` already enumerates `BackendUnavailable`/`BackendUnauthorized`). Verdict-identity, not byte-identity, until the deferred canonical-byte compare lands — so do NOT route emit/lower consumers through it yet. +- **First free measurement:** un-dormant `resolved_graph_cache` in CI (read by the seed, unset in `ci.yml`) as a warm A/B. - **Dissolution trigger:** `ci.yml` carries no hand-wired cache shell; one lookup kernel; one subject key. --- ## Phase 3 — Infra / deployment onto `.dag` (srv1 / srv2) · the second ask -**Goal:** model the actual infra/deployment — runner config, access, host config — as **data**, dissolving -bespoke `ci.yml` shell + manual runner setup. **"Get CI onto `.dag`" = instantiate `compute_fabric` for -srv1/srv2:** a self-hosted runner is one `ComputeOffer`; GHA-hosted, `Ubicloud`, `GcloudRun` are others -(already enumerated, `compute_fabric.dag:71`). This meets note 1 at the placement carrier — the offer the -runner *declares* is the budget Phase 1's scheduler *consumes*. - -**§3 boundary — THREE tiers, not two (refined after the #5177 review).** The operator's rule: keep the -*generic* "CI runner" cleanly apart from *our* CI runner; CI does not need to know our fleet. So: - -- **3a-generic — "CI runner" in the abstract (any project).** What we expect *any* CI runner to do, - project-agnostic: **a workflow triggered by an event** (`trigger → workflow`), realized per platform. - The GHA realization already exists — `Workflow{ on: List, jobs }` + `WorkflowTrigger` - (`actions.dag:56,79`) and `RunnerSpec` (`:233`). The **generic `offer → RunnerSpec` projection** - (`runner_spec_from_offer`, kernel/arch → labels) belongs HERE, next to `RunnerSpec` in the generalized - layer — it works for *any* fleet offer. **This tier MUST NOT import a concrete SKU - (`extdeps.cpu.ampere`) or name srv1/srv2.** (GitLab/Buildkite/etc. would be sibling platform handlers — - one generic interface, N realizations, §2/§4.) -- **3a-ours — OUR gunbc CI runner (our repo's META-modeling).** OUR workflow instance + OUR fleet: the - srv1/srv2 *instantiation* (the Ampere-Altra `ComputeOffer`, the `gunbc-ci-fleet` identity, the - per-thread Hz). This **must live in a file that is gunbc's own meta-model** (`dsl/gunbc/ci_*`), and it - *consumes* the 3a-generic interface — it is where the concrete SKU import is legitimate. The srv1/srv2 - instantiation meta-model is public-in-our-repo; only secrets cross into ctrl. -- **3b — ctrl concrete fleet (private).** Access creds, runner registration tokens, truly-secret per-host - config — **ctrl `plans.fabric.operator_fleet`** (`compute_fabric.dag:5`; `hardware_selection.dag:8`; - memory `idea-pr-compiler-ctrl-boundary`). Concrete rows instantiated against the 3a-ours meta-model. - -**⚠️ #5177 needs this rework (do right after it merges).** `dsl/gunbc/ci_runner.dag` as merged **fuses -3a-generic with 3a-ours**: the generic `runner_spec_from_offer` projection + kernel/arch label tables sit -in the *same module* as our concrete fleet (`gunbc_ci_cpu = altra_q6430_catalog`, `gunbc_ci_host_identity -= "gunbc-ci-fleet"`), and it `import extdeps.cpu.ampere` — a concrete SKU — into what should be the -generic interface. Split it: **generic projection → the generalized layer beside `RunnerSpec`** (no SKU -import, no fleet rows); **our fleet offer → a `dsl/gunbc/` meta-model file** that consumes the generic -projection. Keep the generic interface MINIMAL (trigger→workflow + offer→RunnerSpec) — "CI doesn't need -to know everything." ci.yml stays generated + byte-drift-gated (`expected_ci_yml()` -`dsl/gunbc/ci_yaml_emit.dag:9`, gate `dsl/tools/ci_yaml_gate.dag`); the emit consumes *our* runner spec, -which is *our* fleet offer projected through the *generic* seam. ⚠️ also delete the stale -`extdeps/github/ci.dag:7` "hand-edited, not generated" comment. - -**Dissolution trigger:** `.github/workflows/ci.yml` is emitted from a `.dag` spec whose runner block is -*our* fleet offer projected through the *generic* `offer → RunnerSpec` seam (no hand-authored runner -block, no fleet SKU in the generic tier); the `HardwareBudget` the scheduler reads is the one *our* offer -declares. +**Goal:** model the actual infra/deployment — runner config, access, host config — as **data**, dissolving bespoke `ci.yml` shell + manual runner setup. **"Get CI onto `.dag`" = instantiate `compute_fabric` for srv1/srv2:** a self-hosted runner is one `ComputeOffer`; GHA-hosted, `Ubicloud`, `GcloudRun` are others (already enumerated, `compute_fabric.dag:71`). This meets note 1 at the placement carrier — the offer the runner *declares* is the budget Phase 1's scheduler *consumes*. + +**§3 boundary — THREE tiers, not two (refined after the #5177 review).** The operator's rule: keep the *generic* "CI runner" cleanly apart from *our* CI runner; CI does not need to know our fleet. So: + +- **3a-generic — "CI runner" in the abstract (any project).** What we expect *any* CI runner to do, project-agnostic: **a workflow triggered by an event** (`trigger → workflow`), realized per platform. The GHA realization already exists — `Workflow{ on: List, jobs }` + `WorkflowTrigger` (`actions.dag:56,79`) and `RunnerSpec` (`:233`). The **generic `offer → RunnerSpec` projection** (`runner_spec_from_offer`, kernel/arch → labels) belongs HERE, next to `RunnerSpec` in the generalized layer — it works for *any* fleet offer. **This tier MUST NOT import a concrete SKU (`extdeps.cpu.ampere`) or name srv1/srv2.** (GitLab/Buildkite/etc. would be sibling platform handlers — one generic interface, N realizations, §2/§4.) +- **3a-ours — OUR gunbc CI runner (our repo's META-modeling).** OUR workflow instance + OUR fleet: the srv1/srv2 *instantiation* (the Ampere-Altra `ComputeOffer`, the `gunbc-ci-fleet` identity, the per-thread Hz). This **must live in a file that is gunbc's own meta-model** (`dsl/gunbc/ci_*`), and it *consumes* the 3a-generic interface — it is where the concrete SKU import is legitimate. The srv1/srv2 instantiation meta-model is public-in-our-repo; only secrets cross into ctrl. +- **3b — ctrl concrete fleet (private).** Access creds, runner registration tokens, truly-secret per-host config — **ctrl `plans.fabric.operator_fleet`** (`compute_fabric.dag:5`; `hardware_selection.dag:8`; memory `idea-pr-compiler-ctrl-boundary`). Concrete rows instantiated against the 3a-ours meta-model. + +**⚠️ #5177 needs this rework (do right after it merges).** `dsl/gunbc/ci_runner.dag` as merged **fuses 3a-generic with 3a-ours**: the generic `runner_spec_from_offer` projection + kernel/arch label tables sit in the *same module* as our concrete fleet (`gunbc_ci_cpu = altra_q6430_catalog`, `gunbc_ci_host_identity = "gunbc-ci-fleet"`), and it `import extdeps.cpu.ampere` — a concrete SKU — into what should be the generic interface. Split it: **generic projection → the generalized layer beside `RunnerSpec`** (no SKU import, no fleet rows); **our fleet offer → a `dsl/gunbc/` meta-model file** that consumes the generic projection. Keep the generic interface MINIMAL (trigger→workflow + offer→RunnerSpec) — "CI doesn't need to know everything." ci.yml stays generated + byte-drift-gated (`expected_ci_yml()` `dsl/gunbc/ci_yaml_emit.dag:9`, gate `dsl/tools/ci_yaml_gate.dag`); the emit consumes *our* runner spec, which is *our* fleet offer projected through the *generic* seam. ⚠️ also delete the stale `extdeps/github/ci.dag:7` "hand-edited, not generated" comment. + +**Dissolution trigger:** `.github/workflows/ci.yml` is emitted from a `.dag` spec whose runner block is *our* fleet offer projected through the *generic* `offer → RunnerSpec` seam (no hand-authored runner block, no fleet SKU in the generic tier); the `HardwareBudget` the scheduler reads is the one *our* offer declares. --- ## Dependency-ordered spine (foundation → end state) -The work-item view of the phases above, ordered by dependency toward the acceptance gate (absorbed from -the former quick-ant-298 roadmap; maps onto the phases, does not replace them). +The work-item view of the phases above, ordered by dependency toward the acceptance gate (absorbed from the former quick-ant-298 roadmap; maps onto the phases, does not replace them). - **F1** scheduler gives heavy nodes the budgeted width — *#5421 merged* (= Phase 1 width landing). -- **F2/F3** key-completeness lens (`ToolchainChange ∈ triggers ⟹ input ∈ inputs_considered`) + - `resolved_graph` keyed by construction — *#5423, in review* (= the Phase 2 key-derivation axis, spec-level). -- **P1 — honest keys, verified by execution** *(deps F2,F3)*: realizer-key lens (executed digest ⊇ - declared `inputs_considered`, RED otherwise — would have caught the `from_utf8_lossy` collision); - stable transform-id (reproducible source/commit/tree hash, not binary bytes); census parity for - `parse_table_memo`. (= Phase 2 "converge key derivations".) -- **P2 — one door: caching by inhabitance** *(deps P1)*: `realize(subject)` as the sole API; eliminate - raw bypass (`build_multi_entry_index`, hand-rolled `ParseTable` HashMap → inhabited via `realize`, - DESIGN §6's own example). (= Phase 2 one-kernel/N-backends.) -- **P3 — reach → layer + completeness fail-closed** *(deps P2)* — **the core ask / the acceptance gate**: - reach analysis lens (consumer set + boundary → minimal sufficient `Placement`); completeness gate - (subject realized below reach → ERROR; non-redundant transform with no supplier at reach → ERROR — - **land the redundancy-only cut first**, cost half waits on §4); supplier provisioning + typed request. -- **P4 — economic tier** *(deps Phase 0 measurement)*: per-transform measured cost (`PerformanceReceipt` - → cost-aware reach); `Materialization` = `Recompute | Memoize | Share` chosen by measured cost. -- **P5 — v2 dissolution** *(deps B2)*: `content(T) = content_hash(subgraph)` native; dissolves the - binary-hash/version-string approximations and makes P1's spec↔realizer check structural. - -**External blockers (track as work-items):** **B1** #5295 generic-instantiation (FreeMonoid cached -without variants — itself an under-keyed in-proc cache) → gates cross-shard `Share` (Phase 2.2). **B2** -v2 cross-tree content-hash ("increment 4", the `ContentHash` subject on `RealizedStep`; cf. the -`execution_receipt_digest` stub at `compute_fabric.dag:588-594`) → gates P5. - -**Critical path:** `F2/F3 → P1 → P2 → P3 (redundancy cut) → P3 supplier`. `P1.census`, `P4`, and -Phase-2 sub-items parallelize off it; cross-shard `Share` and P5 wait on B1/B2. The redundancy-only P3 -cut is the earliest point "uncached non-redundant work is an error" is truthful — it needs reach, not -the cost model. +- **F2/F3** key-completeness lens (`ToolchainChange ∈ triggers ⟹ input ∈ inputs_considered`) + `resolved_graph` keyed by construction — *#5423, in review* (= the Phase 2 key-derivation axis, spec-level). +- **P1 — honest keys, verified by execution** *(deps F2,F3)*: realizer-key lens (executed digest ⊇ declared `inputs_considered`, RED otherwise — would have caught the `from_utf8_lossy` collision); stable transform-id (reproducible source/commit/tree hash, not binary bytes); census parity for `parse_table_memo`. (= Phase 2 "converge key derivations".) +- **P2 — one door: caching by inhabitance** *(deps P1)*: `realize(subject)` as the sole API; eliminate raw bypass (`build_multi_entry_index`, hand-rolled `ParseTable` HashMap → inhabited via `realize`, DESIGN §6's own example). (= Phase 2 one-kernel/N-backends.) +- **P3 — reach → layer + completeness fail-closed** *(deps P2)* — **the core ask / the acceptance gate**: reach analysis lens (consumer set + boundary → minimal sufficient `Placement`); completeness gate (subject realized below reach → ERROR; non-redundant transform with no supplier at reach → ERROR — **land the redundancy-only cut first**, cost half waits on §4); supplier provisioning + typed request. +- **P4 — economic tier** *(deps Phase 0 measurement)*: per-transform measured cost (`PerformanceReceipt` → cost-aware reach); `Materialization` = `Recompute | Memoize | Share` chosen by measured cost. +- **P5 — v2 dissolution** *(deps B2)*: `content(T) = content_hash(subgraph)` native; dissolves the binary-hash/version-string approximations and makes P1's spec↔realizer check structural. + +**External blockers (track as work-items):** **B1** #5295 generic-instantiation (FreeMonoid cached without variants — itself an under-keyed in-proc cache) → gates cross-shard `Share` (Phase 2.2). **B2** v2 cross-tree content-hash ("increment 4", the `ContentHash` subject on `RealizedStep`; cf. the `execution_receipt_digest` stub at `compute_fabric.dag:588-594`) → gates P5. + +**Critical path:** `F2/F3 → P1 → P2 → P3 (redundancy cut) → P3 supplier`. `P1.census`, `P4`, and Phase-2 sub-items parallelize off it; cross-shard `Share` and P5 wait on B1/B2. The redundancy-only P3 cut is the earliest point "uncached non-redundant work is an error" is truthful — it needs reach, not the cost model. ## Sequencing & dispatch @@ -367,62 +183,39 @@ the cost model. ``` | Phase | Depends on | Intricacy / Volume | Notes | -|---|---|---|---| +| --- | --- | --- | --- | | 0 keystone | — | high / medium | root of everything quantitative; load-bearing seam (`v1_interpreter.rs`, escalate per DESIGN) | | 1 visible parallelism + width | 0 | high / medium | shares `HardwareBudget` carrier with 3a | | 1.5a affected_set | — | medium / small | fail-closed; can start now | -| 1.5b critical-path total | 0 | medium / small | | +| 1.5b critical-path total | 0 | medium / small | | | 1.5c perturb collapse | — | medium / small | can start now | | 2 cache planner | 0 | high / large | converges 3 key derivations; first catalog consumer | | 3a runner schema + ci.yml gen | (1 for budget carrier) | high / large | public; extends `CiFloorSpec` emission | | 3b ctrl srv1/srv2 | 3a | — | **private `~/ctrl`**, separate PR | -**Start-now lanes (no measurement dependency):** 1.5a (affected_set), 1.5c (perturb), and 3a schema -groundwork. **Critical path:** Phase 0 → 1 / 2. +**Start-now lanes (no measurement dependency):** 1.5a (affected_set), 1.5c (perturb), and 3a schema groundwork. **Critical path:** Phase 0 → 1 / 2. --- ## Guardrails for every worker (DESIGN) -- **Pure central spec, peripheral measured realization** (the §3 invariant above). Anything measured is - peripheral — never in the schedule topology the `schedule_eq` witnesses pin. -- **DFS existing carriers before minting** (§2/§3): `PlacementSupplyRow`, `CpuDeploymentFacts`, - `RunnerSpec`, the cache catalog, `std.pareto`, `RealizationObjective.goals`. The vocabulary mostly - exists — wire it, don't re-coin it. (Background verification specifically flagged: do not invent a fresh - `DeploymentFacts`.) -- **Rows, not Rust** — express new schedule/cache/runner facts as data; do not cement the seed to satisfy - a ratchet (the ratchet is downstream of substrate migration). -- **v2-benefit test (§7)** — the durable artifact is `.dag` that v2 inherits; the Rust seed is only the - proving *handler*. A deliverable that is a Rust patch with no `.dag` model failed. (See the §0 "v2 is the - target" principle.) -- **Fail-closed (§5)** + **purity oracle** on every memo/measurement (byte-identical warm-vs-cold; verdict - identical instrumented-vs-not). A bounded "forever" ≠ an "unknown" error. -- **Green by execution, not spec-without-execution.** A real consumer runs green + a discriminating input - goes red. Typecheck + grep are not consumers. -- **Each phase lands with a named dissolution trigger; the mark is on the carrier.** This doc is - coordination only; delete its entry when the carrier records the fact. -- **Load-bearing files** (DESIGN-named pipeline stages, substrate types, gates: `v1_interpreter.rs`, - `cli_run.rs`, the scheduler, `realization_schedule.dag`) carry a higher bar — escalate before touching - under a brief that pre-dates the relevant model PR. +- **Pure central spec, peripheral measured realization** (the §3 invariant above). Anything measured is peripheral — never in the schedule topology the `schedule_eq` witnesses pin. +- **DFS existing carriers before minting** (§2/§3): `PlacementSupplyRow`, `CpuDeploymentFacts`, `RunnerSpec`, the cache catalog, `std.pareto`, `RealizationObjective.goals`. The vocabulary mostly exists — wire it, don't re-coin it. (Background verification specifically flagged: do not invent a fresh `DeploymentFacts`.) +- **Rows, not Rust** — express new schedule/cache/runner facts as data; do not cement the seed to satisfy a ratchet (the ratchet is downstream of substrate migration). +- **v2-benefit test (§7)** — the durable artifact is `.dag` that v2 inherits; the Rust seed is only the proving *handler*. A deliverable that is a Rust patch with no `.dag` model failed. (See the §0 "v2 is the target" principle.) +- **Fail-closed (§5)** + **purity oracle** on every memo/measurement (byte-identical warm-vs-cold; verdict identical instrumented-vs-not). A bounded "forever" ≠ an "unknown" error. +- **Green by execution, not spec-without-execution.** A real consumer runs green + a discriminating input goes red. Typecheck + grep are not consumers. +- **Each phase lands with a named dissolution trigger; the mark is on the carrier.** This doc is coordination only; delete its entry when the carrier records the fact. +- **Load-bearing files** (DESIGN-named pipeline stages, substrate types, gates: `v1_interpreter.rs`, `cli_run.rs`, the scheduler, `realization_schedule.dag`) carry a higher bar — escalate before touching under a brief that pre-dates the relevant model PR. ## Open decisions to confirm before scoping the affected phase -1. **Placement/budget carrier** — extend `compute_fabric`'s `satisfies` + `PlacementSupplyRow` with the - thread-count/Pareto dimension (the width decision = a placement decision), vs a sibling carrier? (DFS - task in Phase 1 / 3a.) Do not invent `DeploymentFacts`. -2. **The $/billing cost axis crosses the std↔product line.** std `CostAccount` carries `{time,space,power}`; - the $ axis (`CostClass`, `MoneyMicros`) lives in product `compute_fabric`. Confirm: the std schedule's - objective stays `{time,space,power}`; the **peripheral host realizer** combines it with the product $ - axis for the full Pareto pick. (Keeps std product-free.) -3. **Cache planner timing** — the *plan* (which layers, what order) can be compile-time data; only the - *availability probe* is runtime/peripheral. Confirm the split when scoping Phase 2. -4. **Runner-label vocabulary** — how far to close `SelfHosted{labels: List}` toward a typed - topology / a `compute_fabric` offer (3a) without over-fitting to srv1/srv2 (which live in ctrl). -5. **Sharding lives in the demand model — Phase 1 and 3 meet at the parallelism shape, not just the - budget.** `ParallelismShape = ... | IndependentShards{shard_count} | PartitionedReduce{...}` - (`compute_fabric.dag:280-289`) already exists, and the corpus `RunnableDiscoveryBatch` is a **degenerate - (unsharded) projection of a `WorkDemand` whose `parallelism = IndependentShards`** (independent - witnesses). So the easy case needs no new stubs; the `Partitioner`/`Reducer`/`SymbolicCost = Node` - forwards (`:48-58`) are only for the harder `PartitionedReduce` (whole-tree compile → reduce verdicts). - Decide: does Phase 1 express the corpus as an `IndependentShards` `WorkDemand` (preferred — reuses the - carrier) vs a scheduler-local shard list? +1. **Placement/budget carrier** — extend `compute_fabric`'s `satisfies` + `PlacementSupplyRow` with the thread-count/Pareto dimension (the width decision = a placement decision), vs a sibling carrier? (DFS task in Phase 1 / 3a.) Do not invent `DeploymentFacts`. +2. **The $/billing cost axis crosses the std↔product line.** std `CostAccount` carries `{time,space,power}`; the $ axis (`CostClass`, `MoneyMicros`) lives in product `compute_fabric`. Confirm: the std schedule's objective stays `{time,space,power}`; the **peripheral host realizer** combines it with the product $ axis for the full Pareto pick. (Keeps std product-free.) +3. **Cache planner timing** — the *plan* (which layers, what order) can be compile-time data; only the *availability probe* is runtime/peripheral. Confirm the split when scoping Phase 2. +4. **Runner-label vocabulary** — how far to close `SelfHosted{labels: List}` toward a typed topology / a `compute_fabric` offer (3a) without over-fitting to srv1/srv2 (which live in ctrl). +5. **Sharding lives in the demand model — Phase 1 and 3 meet at the parallelism shape, not just the budget.** `ParallelismShape = ... | IndependentShards{shard_count} | PartitionedReduce{...}` (`compute_fabric.dag:280-289`) already exists, and the corpus `RunnableDiscoveryBatch` is a **degenerate (unsharded) projection of a `WorkDemand` whose `parallelism = IndependentShards`** (independent witnesses). So the easy case needs no new stubs; the `Partitioner`/`Reducer`/`SymbolicCost = Node` forwards (`:48-58`) are only for the harder `PartitionedReduce` (whole-tree compile → reduce verdicts). Decide: does Phase 1 express the corpus as an `IndependentShards` `WorkDemand` (preferred — reuses the carrier) vs a scheduler-local shard list? + +## Dissolution trigger (DESIGN §6) + +Delete this plan once the cost→schedule loop is closed — every pure transform's realize(T) is content-addressed by hash(inputs ⊕ content(T)) and materialized at its minimal Placement, CostAccount is fed by Measured basis (not hardcoded zero), schedule width is hardware-bounded and the spawner is bounded by available_parallelism, the cache catalog has live runtime consumers, and a non-redundant transform with no cache supplier at its reach is a located typed ERROR — so the substrate is measurement-fed rather than input-starved. diff --git a/docs/plans/resolver-type-name-collision-wall.md b/docs/plans/resolver-type-name-collision-wall.md index 68e8fe013b3..a6b1d368c88 100644 --- a/docs/plans/resolver-type-name-collision-wall.md +++ b/docs/plans/resolver-type-name-collision-wall.md @@ -1,59 +1,32 @@ # Resolver type-name-collision wall (§5 construction wall) — model-before-implement -Status: **MODEL — SIGNED (parent bright-stag, 2026-06-23).** The model (mechanism + Q2 policy + -activation) is signed; **no resolver edit lands** until the §4 grounding de-fork is clean — the -resolver guard is a separate, operator-gated future PR that lands on the de-forked tree. This -document is the signed model; §3/§4 record the final ruling. +Status: **MODEL — SIGNED (parent bright-stag, 2026-06-23).** The model (mechanism + Q2 policy + activation) is signed; **no resolver edit lands** until the §4 grounding de-fork is clean — the resolver guard is a separate, operator-gated future PR that lands on the de-forked tree. This document is the signed model; §3/§4 record the final ruling. -Owner: jolly-ant-231 (deepest resolver context from the A1 diagnosis). Capstone of the std -de-fork lane. Q2 evidence: `docs/plans/dsl-v2-defork-audit.md` §2A (executed distribution). +Owner: jolly-ant-231 (deepest resolver context from the A1 diagnosis). Capstone of the std de-fork lane. Q2 evidence: `docs/plans/dsl-v2-defork-audit.md` §2A (executed distribution). --- ## 1. The hole this wall closes (grounding) -The A1 (#5615) incident — `type 'EqualsClaim' not found in scope` on -`src/v2/workflow/affected_set_floor_runner_test.dag` — was a **fail-OPEN in the resolver** -(DESIGN §5): a wrong type resolution passed silently as a different, plausible binding. +The A1 (#5615) incident — `type 'EqualsClaim' not found in scope` on `src/v2/workflow/affected_set_floor_runner_test.dag` — was a **fail-OPEN in the resolver** (DESIGN §5): a wrong type resolution passed silently as a different, plausible binding. Mechanism (proven by execution during the diagnosis; receipt below): -- The per-module type scope (`TypeEnv.bindings`) is a `HashMap>` keyed by - the **interned id of the UNQUALIFIED type name** — the intern table is global, so two - module-level types sharing a short name (`v2.std.verification.TestClaim` the Disj coproduct - vs `std.verification.TestClaim` the Conj record) hash to the **same key**. -- `import_bindings` is assembled by folding each imported module's bindings with a blind - `v1_rt::rc_map_merge` (`v1_compiler_infer.rs` ~11799 and the duplicate ~12393). **Map merge - overwrites on duplicate key — last writer wins, no diagnostic.** One authority silently - shadows the other. -- Because variant-constructor registration (`build_module_context`'s `variant_fold`, ~12894) - only fires for `Disj` bindings, when the **record** won the `TestClaim` slot the coproduct's - constructors (`EqualsClaim`, `StructuralEqualsClaim`, …) were never registered → "not found - in scope". A1 was an innocent trigger: it merely grew the test's import-closure to include - `std.verification(dsl)` (via `gunbc.ci_failure_class → extdeps.cache.sccache → - std.cache_interface → std.verification`). - -The existing **`VariantCollision`** guard (`v1_std_core.rs:420`, -`VariantCollision { variant, enum1, enum2, span }`; emitted in `variant_fold` ~12908) already -fails-closed on two imported coproducts sharing a **variant** name. It does **not** cover the -level above: two modules contributing the same **type/enum name** to one closure. The wall is -that guard lifted one level up — the §5 principle of making the bad state *unwritable* rather -than letting it resolve to a plausible wrong binding. - -`#5640` (the `TestClaim → AssertionClaim` rename) dissolved the single instance. The wall -makes the **class** unwritable so the next closure-expanding PR cannot re-arm it. - -Decidability: a closure exporting two distinct authorities under one unqualified name is a -**decidable** condition (finite set of `(name_id, declaring_file)` pairs), so this is a §5 -*wall now*, not a forever-ratchet. "never" is honest here. +- The per-module type scope (`TypeEnv.bindings`) is a `HashMap>` keyed by the **interned id of the UNQUALIFIED type name** — the intern table is global, so two module-level types sharing a short name (`v2.std.verification.TestClaim` the Disj coproduct vs `std.verification.TestClaim` the Conj record) hash to the **same key**. +- `import_bindings` is assembled by folding each imported module's bindings with a blind `v1_rt::rc_map_merge` (`v1_compiler_infer.rs` ~11799 and the duplicate ~12393). **Map merge overwrites on duplicate key — last writer wins, no diagnostic.** One authority silently shadows the other. +- Because variant-constructor registration (`build_module_context`'s `variant_fold`, ~12894) only fires for `Disj` bindings, when the **record** won the `TestClaim` slot the coproduct's constructors (`EqualsClaim`, `StructuralEqualsClaim`, …) were never registered → "not found in scope". A1 was an innocent trigger: it merely grew the test's import-closure to include `std.verification(dsl)` (via `gunbc.ci_failure_class → extdeps.cache.sccache → std.cache_interface → std.verification`). + +The existing **`VariantCollision`** guard (`v1_std_core.rs:420`, `VariantCollision { variant, enum1, enum2, span }`; emitted in `variant_fold` ~12908) already fails-closed on two imported coproducts sharing a **variant** name. It does **not** cover the level above: two modules contributing the same **type/enum name** to one closure. The wall is that guard lifted one level up — the §5 principle of making the bad state *unwritable* rather than letting it resolve to a plausible wrong binding. + +`#5640` (the `TestClaim → AssertionClaim` rename) dissolved the single instance. The wall makes the **class** unwritable so the next closure-expanding PR cannot re-arm it. + +Decidability: a closure exporting two distinct authorities under one unqualified name is a **decidable** condition (finite set of `(name_id, declaring_file)` pairs), so this is a §5 *wall now*, not a forever-ratchet. "never" is honest here. --- ## 2. Mechanism (the model) -Replace the blind `rc_map_merge` of type bindings, at **both** import-binding assembly sites -(`v1_compiler_infer.rs` ~11761 and ~12355 — themselves a §2 duplication this work should -dissolve into **one** shared helper), with a **collision-checking merge**: +Replace the blind `rc_map_merge` of type bindings, at **both** import-binding assembly sites (`v1_compiler_infer.rs` ~11761 and ~12355 — themselves a §2 duplication this work should dissolve into **one** shared helper), with a **collision-checking merge**: ``` merge_type_bindings(acc, incoming, policy) -> { bindings, collisions } @@ -72,21 +45,11 @@ merge_type_bindings(acc, incoming, policy) -> { bindings, collisions } Where: -- `same_authority(a, b)` ≡ `a.resolved.span.file == b.resolved.span.file` (one declaring file - reached via multiple import paths is the SAME authority — a benign re-export, must NOT - flag). `TypeBinding` is `{ name, resolved: Rc, provenance }` and `Node.span.file` - carries the declaring file, so two-authorities-vs-one-re-export is distinguishable today — - **no new field required.** -- `TypeNameCollision` is a new `CompilerDiagnostic` variant modeled exactly on - `VariantCollision`: `{ name: String, module_a: String, module_b: String, span }`, classified - **blocking** (`is_error_diagnostic` true), so it fails the resolve/typecheck closed with a - located, typed message — the §5 "loud error, never a warning". -- Determinism: on collision keep the **first-seen** binding (stable under the existing - dep-order traversal) so the error set is reproducible regardless of which authority "would - have won" the old overwrite. - -This is one mechanism; §3 (the policy) and §4 (activation) are knobs on it, not separate -machinery. +- `same_authority(a, b)` ≡ `a.resolved.span.file == b.resolved.span.file` (one declaring file reached via multiple import paths is the SAME authority — a benign re-export, must NOT flag). `TypeBinding` is `{ name, resolved: Rc, provenance }` and `Node.span.file` carries the declaring file, so two-authorities-vs-one-re-export is distinguishable today — **no new field required.** +- `TypeNameCollision` is a new `CompilerDiagnostic` variant modeled exactly on `VariantCollision`: `{ name: String, module_a: String, module_b: String, span }`, classified **blocking** (`is_error_diagnostic` true), so it fails the resolve/typecheck closed with a located, typed message — the §5 "loud error, never a warning". +- Determinism: on collision keep the **first-seen** binding (stable under the existing dep-order traversal) so the error set is reproducible regardless of which authority "would have won" the old overwrite. + +This is one mechanism; §3 (the policy) and §4 (activation) are knobs on it, not separate machinery. --- @@ -94,26 +57,15 @@ machinery. **One predicate, one boolean knob** — `policy.flags(existing, incoming)`: -- **flag-ANY** (`require_structural_divergence = false`): - `flags = true` for any two distinct authorities (different declaring files) under one name. - Even a **byte/structurally-identical mirror** flags — because it is still *two authorities - for one concept*, the §3 single-authority violation, just benign-looking. It remains a - writable re-fork surface: nothing stops the two copies drifting apart later (which is exactly - how A1's landmine formed). - -- **flag-DIVERGENT** (`require_structural_divergence = true`): - `flags = structural_inequality(existing.resolved, incoming.resolved)`. - Fires only when the two definitions actually differ (connective and/or children) — like the - Disj-coproduct vs Conj-record case. True mirrors are **excused**. +- **flag-ANY** (`require_structural_divergence = false`): `flags = true` for any two distinct authorities (different declaring files) under one name. Even a **byte/structurally-identical mirror** flags — because it is still *two authorities for one concept*, the §3 single-authority violation, just benign-looking. It remains a writable re-fork surface: nothing stops the two copies drifting apart later (which is exactly how A1's landmine formed). +- **flag-DIVERGENT** (`require_structural_divergence = true`): `flags = structural_inequality(existing.resolved, incoming.resolved)`. Fires only when the two definitions actually differ (connective and/or children) — like the Disj-coproduct vs Conj-record case. True mirrors are **excused**. -`structural_inequality` is a normalized structural compare of the two resolved type Nodes -(connective + children names + field types), modulo span/occurrence — the same shape the -emitter's coercion homomorphism check already walks; no new comparison primitive needed. +`structural_inequality` is a normalized structural compare of the two resolved type Nodes (connective + children names + field types), modulo span/occurrence — the same shape the emitter's coercion homomorphism check already walks; no new comparison primitive needed. ### Trade-off (parent rules on the real distribution) -| | flag-ANY | flag-DIVERGENT | -|---|---|---| +| | flag-ANY | flag-DIVERGENT | +| --- | --- | --- | | Catches the A1 class (divergent shadow) | yes | yes | | Catches a *future* mirror that later drifts | yes (at fork time) | no (only after drift, when a closure re-imports both) | | De-fork scope it demands | **all** same-name pairs resolved: divergent → rename-apart, mirror → **merge to one authority** | only divergent pairs resolved; mirrors may stay | @@ -122,31 +74,12 @@ emitter's coercion homomorphism check already walks; no new comparison primitive ### RULED — `flag-ANY` (parent bright-stag, signed 2026-06-23) -**`require_structural_divergence = FALSE`.** Settled against the measured distribution (the -executed per-basename audit in `docs/plans/dsl-v2-defork-audit.md` §2A — `structural_inequality` -run over all 9 std basename pairs + a 351-entry floor-closure reachability BFS). The audit -confirmed the cant-unify-yet set (basenames needing a milestone *later than* the grounding -de-fork) is **{node, coercion} exactly** — no third stuck mirror — so flag-ANY does not block on -an un-unifiable pair. +**`require_structural_divergence = FALSE`.** Settled against the measured distribution (the executed per-basename audit in `docs/plans/dsl-v2-defork-audit.md` §2A — `structural_inequality` run over all 9 std basename pairs + a 351-entry floor-closure reachability BFS). The audit confirmed the cant-unify-yet set (basenames needing a milestone *later than* the grounding de-fork) is **{node, coercion} exactly** — no third stuck mirror — so flag-ANY does not block on an un-unifiable pair. Two consequences parent reconfirmed: -- **flag-ANY FIRES on byte-identical mirror shared type-names too** (the audit's 3 in `algebra`, - 3 in `integer`, 1 in `float`), not only on differing ones. This is **intended**: a - byte-identical mirror is still *two homes for one type* = the §3 single-authority violation and - a writable re-fork surface. So the de-fork must **merge even the mirrors** (delete the v2 copy, - repoint imports), and flag-ANY is exactly what forces that. flag-DIVERGENT would *tolerate* the - byte-mirrors — a standing §3 hole — so it is strictly worse here (it also still fires on every - grounding, sparing nothing). Mirrors are therefore **resolved by the de-fork, not exempted**. - -- **The exemption roster carries NO `{node, coercion}` entry — DROPPED as vacuous.** node and - coercion (and `logic`, and post-#5640 `verification`) share **zero** type names — only the - *basename* — so the type-name guard **never fires** on them. A roster entry for a collision the - mechanism cannot produce is a §5 inert scaffold (a dead line). Their collision is a - module-**basename** rename on the Route-C / v1-delete surface — a *different* mechanism, still - tracked (audit category-(c), `dissolve-on = v1-delete`), not by this guard. The guard's roster - is therefore **deliberately empty** — recorded here so its emptiness reads as a decision, not an - omission. (See §6.) +- **flag-ANY FIRES on byte-identical mirror shared type-names too** (the audit's 3 in `algebra`, 3 in `integer`, 1 in `float`), not only on differing ones. This is **intended**: a byte-identical mirror is still *two homes for one type* = the §3 single-authority violation and a writable re-fork surface. So the de-fork must **merge even the mirrors** (delete the v2 copy, repoint imports), and flag-ANY is exactly what forces that. flag-DIVERGENT would *tolerate* the byte-mirrors — a standing §3 hole — so it is strictly worse here (it also still fires on every grounding, sparing nothing). Mirrors are therefore **resolved by the de-fork, not exempted**. +- **The exemption roster carries NO `{node, coercion}` entry — DROPPED as vacuous.** node and coercion (and `logic`, and post-#5640 `verification`) share **zero** type names — only the *basename* — so the type-name guard **never fires** on them. A roster entry for a collision the mechanism cannot produce is a §5 inert scaffold (a dead line). Their collision is a module-**basename** rename on the Route-C / v1-delete surface — a *different* mechanism, still tracked (audit category-(c), `dissolve-on = v1-delete`), not by this guard. The guard's roster is therefore **deliberately empty** — recorded here so its emptiness reads as a decision, not an omission. (See §6.) --- @@ -154,79 +87,37 @@ Two consequences parent reconfirmed: Two options: -- **Staged-enable** (guard lands dormant, flips fail-closed later): carries **dormant-guard - state** — a loaded mechanism left unwired. DESIGN §5/§6 names this an anti-pattern: an inert - guard is "coverage by illusion", a latent lie until the flip, and adds a flip-event to - sequence and a window where the guard exists but does not gate. - -- **Lands-already-green** (preferred): the de-fork lane first removes **every** collision the - chosen policy flags from the tree; *then* the guard lands **already fail-closed and green**. - No dormant state, no flip event. The guard's own green landing is **self-certifying**: it is - green only if zero flagged collisions remain, so merging it *proves* the tree is - collision-free under the policy. This is the §5 "wall lands live or not at all". - -Sequencing (hard dependency, RULED): **the grounding de-fork of the shared-type-name set -`{algebra, nat, effects, float, integer}` → guard lands flag-ANY, fail-closed, green, in one -PR.** Each of those five is merged to a single authority (delete the v2 copy / repoint, or the -operator grounding-unification design where the bodies diverge) — mirrors included (§3). The set -is fronted by the **LIVE pair `{algebra (75 floor entries), nat (4)}`** (their `std.` / -`v2.std.` co-occur in real floor closures today and silently fail-open — benign only because -they shadow record-with-record, not the coproduct-variant-drop that broke `verification` under -A1) and completed by the **latent `{effects, float, integer}`** (no co-occurring closure today, -but re-arm risks — exactly how `verification` went latent→LIVE under A1's closure expansion). -`verification` already cleared (#5640); `{node, coercion, logic}` are off this surface (zero -shared type-names). - -The guard PR is mergeable iff the full floor corpus resolves clean **with the guard active** — -which holds iff that five-basename de-fork is complete. Its green landing therefore -**self-certifies** the shared-type-name surface is collision-free: the wall is the **capstone** -of the de-fork lane, correctly located. No dormant-guard state, no flip event — lands-already-green. +- **Staged-enable** (guard lands dormant, flips fail-closed later): carries **dormant-guard state** — a loaded mechanism left unwired. DESIGN §5/§6 names this an anti-pattern: an inert guard is "coverage by illusion", a latent lie until the flip, and adds a flip-event to sequence and a window where the guard exists but does not gate. +- **Lands-already-green** (preferred): the de-fork lane first removes **every** collision the chosen policy flags from the tree; *then* the guard lands **already fail-closed and green**. No dormant state, no flip event. The guard's own green landing is **self-certifying**: it is green only if zero flagged collisions remain, so merging it *proves* the tree is collision-free under the policy. This is the §5 "wall lands live or not at all". + +Sequencing (hard dependency, RULED): **the grounding de-fork of the shared-type-name set `{algebra, nat, effects, float, integer}` → guard lands flag-ANY, fail-closed, green, in one PR.** Each of those five is merged to a single authority (delete the v2 copy / repoint, or the operator grounding-unification design where the bodies diverge) — mirrors included (§3). The set is fronted by the **LIVE pair `{algebra (75 floor entries), nat (4)}`** (their `std.` / `v2.std.` co-occur in real floor closures today and silently fail-open — benign only because they shadow record-with-record, not the coproduct-variant-drop that broke `verification` under A1) and completed by the **latent `{effects, float, integer}`** (no co-occurring closure today, but re-arm risks — exactly how `verification` went latent→LIVE under A1's closure expansion). `verification` already cleared (#5640); `{node, coercion, logic}` are off this surface (zero shared type-names). + +The guard PR is mergeable iff the full floor corpus resolves clean **with the guard active** — which holds iff that five-basename de-fork is complete. Its green landing therefore **self-certifies** the shared-type-name surface is collision-free: the wall is the **capstone** of the de-fork lane, correctly located. No dormant-guard state, no flip event — lands-already-green. --- ## 5. Proof plan (model-only; how it is proven by execution when authored) -Per DESIGN §5 ("done" = a real consumer green by execution + a discriminating input that goes -red when the behavior is wrong): - -- **GREEN-by-execution:** with the de-fork complete, run the exact floor closure - (`claim_executor --source-root dsl --source-root src/v2`, both orders) — full corpus resolves - clean **with the guard active**. (Baseline receipt already in hand from #1: post-rename, - `affected_set_floor_runner_test` PASSes both orders, 56 modules.) -- **Discriminating RED (the falsifier):** re-introduce a single synthetic same-name pair into a - test's closure and assert the guard emits `TypeNameCollision` and fails closed — and that - *removing* it returns green. Run it **twice** to pin the flag-ANY semantics: once with a - **divergent** pair (different bodies) and once with a **byte-identical mirror** pair — *both* - must fire (flag-ANY excuses neither). A flag-DIVERGENT build would let the mirror through; that - it does **not** is the §3-fidelity control. -- **No-regression control:** a type legitimately re-exported through multiple import paths - (one declaring file, many hops) must stay green — proves `same_authority` (span.file - identity) correctly excuses re-exports and the wall is not over-broad. +Per DESIGN §5 ("done" = a real consumer green by execution + a discriminating input that goes red when the behavior is wrong): + +- **GREEN-by-execution:** with the de-fork complete, run the exact floor closure (`claim_executor --source-root dsl --source-root src/v2`, both orders) — full corpus resolves clean **with the guard active**. (Baseline receipt already in hand from #1: post-rename, `affected_set_floor_runner_test` PASSes both orders, 56 modules.) +- **Discriminating RED (the falsifier):** re-introduce a single synthetic same-name pair into a test's closure and assert the guard emits `TypeNameCollision` and fails closed — and that *removing* it returns green. Run it **twice** to pin the flag-ANY semantics: once with a **divergent** pair (different bodies) and once with a **byte-identical mirror** pair — *both* must fire (flag-ANY excuses neither). A flag-DIVERGENT build would let the mirror through; that it does **not** is the §3-fidelity control. +- **No-regression control:** a type legitimately re-exported through multiple import paths (one declaring file, many hops) must stay green — proves `same_authority` (span.file identity) correctly excuses re-exports and the wall is not over-broad. --- ## 6. Scope guard / what this is NOT - **No resolver edit lands** here — model only until checkpoint-sign + de-fork clean. -- Does **not** touch the dsl↔v2 std module-**basename** reorganization (Route C / v1-delete) — - orthogonal, operator-strategic. The wall keys on shared **type-name** identity within a - closure, so the zero-shared-type-name basenames `{node, coercion, logic, verification}` are - off its surface entirely (this is why the roster carries no `{node, coercion}` entry, §3). - Their basename de-fork stays tracked in the audit's category-(c) (`dissolve-on = v1-delete`), - a different mechanism. The wall is compatible with whatever Route C decides. -- Mirrors the existing `VariantCollision` precedent; introduces no new resolver concept beyond - lifting that guard one level and dissolving the duplicate import-binding folds into one - checked-merge helper (a §2 win bundled in). +- Does **not** touch the dsl↔v2 std module-**basename** reorganization (Route C / v1-delete) — orthogonal, operator-strategic. The wall keys on shared **type-name** identity within a closure, so the zero-shared-type-name basenames `{node, coercion, logic, verification}` are off its surface entirely (this is why the roster carries no `{node, coercion}` entry, §3). Their basename de-fork stays tracked in the audit's category-(c) (`dissolve-on = v1-delete`), a different mechanism. The wall is compatible with whatever Route C decides. +- Mirrors the existing `VariantCollision` precedent; introduces no new resolver concept beyond lifting that guard one level and dissolving the duplicate import-binding folds into one checked-merge helper (a §2 win bundled in). ## 7. Open items -- **RESOLVED** — Q2 policy: `flag-ANY` signed (§3); per-basename audit executed and homed in - `docs/plans/dsl-v2-defork-audit.md` §2A; activation gate set to the five-basename grounding - de-fork (§4). Roster: deliberately empty (§3). -- Carried to the future resolver PR (not this model): confirm both import-binding assembly sites - (~11761, ~12355) are the only type-binding merge loci (the `std.types`-special-cased branch - folds key-by-key already and is naturally covered by the same checked-merge helper). -- Dependency owned elsewhere: the five-basename grounding de-fork (`algebra` authority ruled; - `nat`/`integer`/`float` via #5428 numeric tower; `effects` axis decision) must complete before - the guard PR can land green. `{node, coercion}` basename de-fork stays on the Route-C / v1-delete - surface (audit category-(c)), unaffected by this guard. +- **RESOLVED** — Q2 policy: `flag-ANY` signed (§3); per-basename audit executed and homed in `docs/plans/dsl-v2-defork-audit.md` §2A; activation gate set to the five-basename grounding de-fork (§4). Roster: deliberately empty (§3). +- Carried to the future resolver PR (not this model): confirm both import-binding assembly sites (~11761, ~12355) are the only type-binding merge loci (the `std.types`-special-cased branch folds key-by-key already and is naturally covered by the same checked-merge helper). +- Dependency owned elsewhere: the five-basename grounding de-fork (`algebra` authority ruled; `nat`/`integer`/`float` via #5428 numeric tower; `effects` axis decision) must complete before the guard PR can land green. `{node, coercion}` basename de-fork stays on the Route-C / v1-delete surface (audit category-(c)), unaffected by this guard. + +## Dissolution trigger (DESIGN §6) + +Delete this model-only DESIGN doc once the resolver type-name-collision wall is implemented and merged — the flag-ANY guard fires fail-closed on any same-name cross-authority type pair (TypeNameCollision diagnostic), the floor closure lands already-green after the de-fork, and the discriminating RED witness (synthetic divergent + byte-identical-mirror pairs both fire) is proven by execution — so this model is realized in the resolver. diff --git a/dsl/gunbc/plan_registry.dag b/dsl/gunbc/plan_registry.dag index d4e900d4cb2..4d2c46230e7 100644 --- a/dsl/gunbc/plan_registry.dag +++ b/dsl/gunbc/plan_registry.dag @@ -8,6 +8,7 @@ import gunbc.plan_registry_batch_c { batch_c_plans } import gunbc.plan_registry_batch_d { batch_d_plans } import gunbc.plan_registry_batch_e { batch_e_plans } import gunbc.plan_registry_batch_f { batch_f_plans } +import gunbc.plan_registry_batch_g { batch_g_plans } data all_plans: List = concat( [idea_machine_plan], @@ -15,4 +16,5 @@ data all_plans: List = concat( concat(batch_b_plans, concat(batch_c_plans, concat(batch_d_plans, - concat(batch_e_plans, batch_f_plans)))))) + concat(batch_e_plans, + concat(batch_f_plans, batch_g_plans))))))) diff --git a/dsl/gunbc/plan_registry_batch_g.dag b/dsl/gunbc/plan_registry_batch_g.dag new file mode 100644 index 00000000000..072b0b6f2fe --- /dev/null +++ b/dsl/gunbc/plan_registry_batch_g.dag @@ -0,0 +1,14 @@ +module gunbc.plan_registry_batch_g + +import gunbc.plan { Plan } +import gunbc.plans.ci_humming { ci_humming_plan } +import gunbc.plans.edge_b_rust_dag_provenance_brief { edge_b_rust_dag_provenance_brief_plan } +import gunbc.plans.resolver_type_name_collision_wall { resolver_type_name_collision_wall_plan } +import gunbc.plans.realization_measurement_loop { realization_measurement_loop_plan } + +data batch_g_plans: List = [ + ci_humming_plan, + edge_b_rust_dag_provenance_brief_plan, + resolver_type_name_collision_wall_plan, + realization_measurement_loop_plan +] diff --git a/dsl/gunbc/plans/ci_humming.dag b/dsl/gunbc/plans/ci_humming.dag new file mode 100644 index 00000000000..d659d57dbd3 --- /dev/null +++ b/dsl/gunbc/plans/ci_humming.dag @@ -0,0 +1,67 @@ +module gunbc.plans.ci_humming + +import gunbc.plan { Plan, DissolutionTrigger, HasTrigger } +import std.markdown { MarkdownBlock } +import gunbc.plans.md_helpers { h2, p, li, ul } + +fn ci_humming_body() -> List { + [ + p(text: "Home: ROADMAP §1 (CI as the substrate integration dogfood). This is the **▸ NOW — host-operation on `.dag`** milestone made concrete: placement, runner deployment, and caps are hand-managed and off-fabric today; this plan migrates them onto the modeled budget + carrier and uses that to un-throttle CI."), + p(text: "**GOAL.** CI fast (low wall-clock per PR) + high throughput (many PRs concurrent) + reliable (no reds / OOM / flakes) — and all three falling *out* of a single modeled budget consumed by a verified-effective apply, never a hand-picked number (§2/§5)."), + h2(text: "Root cause (live-verified 2026-06-23)"), + p(text: "srv1 + srv2 (128c / 125GiB each) sit at ~10-34% CPU, ~24-32% MEM, with only **~3 runner slots per host** — so PRs **queue while the cores idle**. The throttle is the runner-slot count, which is set by the per-host **memory budget allocation**, not by saturation, not by fleet capacity, not by OOM."), + p(text: "The slot count is starved because the budget model (`dsl/gunbc/fleet_host_budget.dag`) derives `runner_slice_cap ≈ 0`: build memory is subtracted as a `build_pool` **and** re-charged inside the per-job whole-tree-peak divisor. A GHA-CI runner job *is* a build — its `rustc` lives **inside** `system-actions-runner.slice` — so the build memory must be counted **once**, not twice."), + h2(text: "oomd demoted (operator §5 insight)"), + p(text: "Proper allocation (slice cap + per-slot caps ≤ physical − overhead, **verified-effective**) makes OOM impossible *by construction*. oomd is defense-in-depth for the **residue that is not yet capped-by-construction**, not a hard precondition. The srv2 reboots were construction *failing to realize* (the authored cap sat at `MemoryMax=infinity` on the live cgroup), not a missing daemon."), + p(text: "→ Relax `fleet_host_plan`'s hard `OomdUnverified` gate; the primary gate is **caps verified-effective**. oomd stays as a non-blocking backstop, and its honest residual job is the one co-resident slice still uncapped — see SessionSliceEnforcement below."), + h2(text: "1. Throughput (the capacity critical path)"), + ul(items: [ + li(text: "**T0 — build-pool vs runner-slice double-count** [CRITICAL, design call signed]: `runner_slice` must NOT subtract the GHA-CI build memory it already contains. Revised model (smart-pike-244): `runner_slice = host − overhead − session_worst_case_slice − headroom`; `runner_count = min(slice / per_job_peak, effective_build_tokens, cpu_cores_available)` — a 3-axis min-over-constraints. Fix this and the model derives > 0 runners. (smart-pike #5674.)"), + li(text: "**T1 — verified-effective slice cap** (construction; primary wall; the srv2 fix): ctrl PR built + signed, awaiting operator GO to open. The authored cap becomes *effective* on the live cgroup (reconcile verifies `MemoryMax != infinity`), closing the inert-cap hole."), + li(text: "**T2 — per-slot `MemoryMax` caps**: a job that over-caps is cgroup-killed in isolation, not the host. Part of the apply."), + li(text: "**T3 — budget manifest** (`.github/fleet-runner-deploy.manifest`: per-host count + per-slot cap + tokens): smart-pike #5674 landed; emits typed `UNSOUND` until the caps are sound (correct fail-closed)."), + li(text: "**T4 — per-job peak / build-pool sizing 24 → 8GiB**: cap `rustc`/slot via jobserver tokens; confirm `mem_reserve`. Same problem as T0 from the sizing angle. **manager-owned.**"), + li(text: "**T5 — ctrl apply**: consume the manifest → enable N slots + per-slot caps + tokens on srv1/srv2, verified-effective. Was blocked on #1753; operator now authorizes execute-ASAP. **The live host apply is surfaced to the operator before it executes.**"), + li(text: "**T6 — cpu.weight priority axis**: runner slice = `BatchLatencyTolerant` (weight 100, cgroup v2 default); sessions slice = `InteractiveLatencySensitive` (weight 1000, 10x). cgroup v2 cpu.weight is work-conserving: raising sessions above runners costs zero CI throughput when sessions are idle; under contention interactive sessions preempt batch builds. Fixes dashboard slowness on srv2 under CI load. (merry-stag-459, `WorkloadClass` modeled + emitted on manifest.)"), + ]), + h2(text: "2. Wall-clock (faster runs)"), + ul(items: [ + li(text: "**W1 — floor `spawn_width` memory-aware**: designed in `std.realization_width`; VERIFY it is wired to the executor. **manager-verify.**"), + li(text: "**W2 — split the cargo-test debug monolith** (~16m tentpole; also halves the T4 peak). **manager-owned.**"), + li(text: "**W3 — sccache corruption flakes** (false reds + full rebuilds). **manager-owned.**"), + ]), + h2(text: "3. Reliability (no reds / flakes) — folds in the red-rate lockdown lane"), + ul(items: [ + li(text: "**R1 — floor OOM exit137**: solved by T1+T2+T4 construction; oomd backstop."), + li(text: "**R2 — gate-trigger false-green** (`.dag`-only changes run 0 tests). **manager-owned.**"), + li(text: "**R3 — merge-result re-run** (catch stale-green merge skew): VERIFY wired."), + li(text: "The existing **main-red-rate lockdown** (structural floor defects, merge-freshness, anchor-completeness; crisp-carp-603 / quick-carp-124) is the reliability arm of this plan — the CI-humming manager coordinates it as one CI authority rather than letting throughput and reliability drift into unrelated workstreams."), + ]), + h2(text: "4. The carrier (mechanism for T5 + all host config)"), + ul(items: [ + li(text: "**C1 — std reconcile / verify-ground carrier** (signed signature; home = std): `reconcile(apply_effect, show_read, grounding) → Converged\{evidence\} | NotConverged\{reason\}`, with the §5 type-level invariant that the evidence carrier is constructible only via the grounding over a real read — \"verify the realization, not the declaration\" promoted to a constructor restriction. valiant-pike-233."), + li(text: "**C2 — `extdeps/os/systemd` unit-mgmt + apt install-effect**: re-homed under `extdeps/os/`, reusing the existing `extdeps.os.systemd` state. valiant-pike-233."), + li(text: "**C3 — oomd model + install Realization** (now defense-in-depth, off the critical path): valiant-pike-233 (#5677)."), + li(text: "**C4 — PXE/autoinstall + GCP keyless token**: neat-boar-71 (+ children)."), + li(text: "**One emit-from-fleet-model Realization** (§2 regime-2 projection fold): `ci.yml` + `fleet-runner-deploy.manifest` + Ubuntu user-data + `dnsmasq.conf` + the oomd drop-in are all the same projection."), + ]), + h2(text: "5. SessionSliceEnforcement (the safe-apply gate — new)"), + p(text: "The hosts co-host the agent-session fleet AND the CI runners. Full safe-by-construction needs **both** slices capped-verified-effective (runner + session), summing all maxes ≤ 125GiB. Today the agent-session cgroups have **no** citable verified-effective cap — that is the residual over-commit vector, and exactly where oomd-as-backstop earns its keep until a `SessionSliceEnforcement` carrier (parallel to the runner-slot enforcement) lands."), + p(text: "**Apply rule:** do NOT apply the runner cap while sessions are *both* uncapped AND oomd-absent — that is an un-backstopped over-commit (the srv2 vector). Pick (a) cap both slices verified-effective → no oomd needed, or (b) cap the runner slice + keep oomd live as the session backstop. The single `resolve_session_slice` figure is the §3 authority: it is subtracted by the runner budget AND drives the dashboard session reservation — one number, passed *down* into the budget, never imported up."), + h2(text: "6. Auth (separate, near-resolved)"), + ul(items: [ + li(text: "**A1 — `resolve_auth` `svc_auth_input` realization**: #5661 (8 approvals, CLEAN) — the positive path, live-verified on GCP."), + li(text: "**A2 — `AuthDeclaredButUnwired` guard** (additive fail-closed delta on #5661; its own PR): re-homed under neat-boar-71."), + li(text: "**A3 — perturbation confirm** (the §5 done-bar: drop the token → typed error PRE-SEND, never a remote 401): snappy-otter-298."), + ]), + h2(text: "Critical path to capacity (do first, both hosts ASAP)"), + p(text: "T0 (un-zero the runner slice) → model derives sane N + per-slot caps → T1+T2 verified-effective apply on srv1+srv2, **with the session slice either capped (5) or oomd-backstopped** → safe by construction (Σ caps + overhead + baselines ≤ physical). T4 (peak → 8GiB) multiplies N afterward. oomd is not required on the critical path."), + ] +} + +data ci_humming_plan: Plan = Plan { + slug: "ci-humming", + title: "CI humming — throughput, wall-clock, reliability (the single CI-operations authority)", + body: ci_humming_body(), + dissolution: HasTrigger { text: "Delete this doc when CI throughput, wall-clock, and reliability all fall out of the single modeled fleet budget consumed by a verified-effective apply (T0 un-zeroes the runner slice, T1/T2 caps are verified-effective on srv1+srv2, and the session slice is capped or oomd-backstopped) — so capacity is safe by construction rather than hand-managed." } +} diff --git a/dsl/gunbc/plans/edge_b_rust_dag_provenance_brief.dag b/dsl/gunbc/plans/edge_b_rust_dag_provenance_brief.dag new file mode 100644 index 00000000000..4828f014ecf --- /dev/null +++ b/dsl/gunbc/plans/edge_b_rust_dag_provenance_brief.dag @@ -0,0 +1,63 @@ +module gunbc.plans.edge_b_rust_dag_provenance_brief + +import gunbc.plan { Plan, DissolutionTrigger, HasTrigger } +import std.markdown { MarkdownBlock } +import gunbc.plans.md_helpers { h2, p, li, ul, ol } + +fn edge_b_rust_dag_provenance_brief_body() -> List { + [ + p(text: "**Status: SCOPING ONLY.** The multi-day build holds for the operator's explicit greenlight. This document is the decision artifact for that greenlight call."), + h2(text: "Goal"), + p(text: "Make the rust↔.dag dependency a **declared structural fact**, recorded once and read in two directions. It is the single fact under three consumers (DESIGN §4, one grammar both directions), which is why this is the §1 *coverage keystone*, not a cost follow-up."), + h2(text: "Why — one fact, three consumers"), + ol(items: [ + li(text: "**Coverage wall (soundness, fail-closed).** Today a pure-.dag PR fires *no* rust gate: `any_rust_monolith` (`dsl/tools/rust_stage0_gates.dag`) matches only `.rs`/Cargo/toolchain suffixes. But rust tests *read* `.dag` via opaque `filesystem_read`/`ws.join`, so a `.dag` change that breaks a rust test ships **silently green** — a §5 fail-OPEN. That file's own COMPLETENESS CLAIM (\"every change that can alter a rust gate's verdict carries a `.rs`/Cargo suffix\") is *false* for .dag-consuming tests, and its header names per-file rust→.dag dependence as the deliberately-skipped proper model. Edge-(b) FIRES the rust gate when a changed `.dag` is in a rust test's declared closure → makes the claim true. This is the operator's \"lock fail-closed before you expand\" priority."), + li(text: "**Affordability selector.** The *same* declared closure read the other way — skip rust tests whose closure the diff doesn't touch — is the affected-set shrink (the ROADMAP end-state: run-all baseline SHRUNK to affected). cargo has *zero* affected-test selection (every `#[test]` every run; nextest too) and can't see `.dag` deps, so a declared closure is the *only* path to it."), + li(text: "**Testgen reflection.** The rust-test→.dag closure is the same provenance testgen needs to regenerate the right tests when a `.dag` node changes."), + ]), + p(text: "FIRE-when-consumed and SKIP-when-unaffected are the single fact read in opposite directions — that unification is the moat (one carrier, three consumers)."), + h2(text: "The asymmetry that decides what the build buys (construction, not validation)"), + p(text: "The two directions have **asymmetric robustness to an incomplete declaration**, and this is the construction-vs-validation lesson made concrete:"), + ul(items: [ + li(text: "**Affordability (skip-unaffected) is fail-SAFE to over-declaration.** Declare too much → you just run more → never unsound. Robust to a sloppy/partial closure."), + li(text: "**Coverage (fire-on-change) is fail-OPEN to UNDER-declaration.** If a test reads `.dag` A and B but its closure declares only A, a change to B does NOT fire the gate → the exact `.dag`→rust fail-open we are closing, silently re-introduced as **declaration drift**. The coverage wall is only as sound as the declaration is COMPLETE: **closure ⊇ actual-.dag-reads**."), + ]), + p(text: "Consequence: the coverage wall's soundness lives entirely in the *completeness* of the closure, which means a **hand-authored closure is the §3/§5 fork** — for the coverage consumer it silently re-opens the hole. So the closure MUST be structurally derived (drift-proof); any hand-authored interim must be marked **NON-SOUND** (delivers affordability only, not the coverage wall). The \"shared blocker\" below is therefore not the tail of the work — it is *where the soundness lives*."), + h2(text: "Bounded core"), + ol(items: [ + li(text: "**Declare rust-test → consumed-.dag-paths on the EXISTING `NodeArtifactProvenance` / `EditLocusBinding` carrier** — no parallel mint (§3 single authority). Implementer must first verify the carrier shape fits `rust-test-identity → .dag-path list`; if not, add a *sibling entry on the same authority*, never a new module."), + li(text: "**Gate integration is small and precise:** extend `should_run_gates` / `any_rust_monolith` (`dsl/tools/rust_stage0_gates.dag`) so a changed `.dag` path in the union of declared rust-test closures ALSO returns true."), + li(text: "**Fail-closed default AT THE CONSUMER:** a rust test with no declared closure → *must-run*, never skip. Absent provenance = run. This keeps the soundness direction safe while declarations are added incrementally."), + li(text: "**Completeness-lens gated — on CORRECTNESS, not presence.** A lens that merely asserts \"every rust test HAS a closure declaration\" checks *presence*, which is exactly the §5 trap: it is satisfiable by editing the declaration while the realization diverges (the faked-cache-key / dead-field pattern). The lens must check **closure ⊇ actual-.dag-reads** — otherwise a partial or stale declaration passes the lens AND leaks coverage. Presence-only is not enough; correctness (the superset relation) is the soundness condition."), + ]), + h2(text: "Shared blocker (testgen-reflection) — this IS the soundness, not optional polish"), + p(text: "Per the asymmetry above: the `.dag`-closure must be DISCOVERED structurally, not hand-listed (hand-listing is the §3/§5 fork that rots, and for the coverage consumer it *silently re-opens the hole*). The reflection infra exists *partially* — `v2.std.node_query` + `dependency_lens` + the `affected_set` node-frontier (compile-time, structural over Node/DependencyView). The missing piece: rust tests reach `.dag` through *opaque host paths* (`ws.join`/`filesystem_read`), so the closure isn't visible to the Node-tree lens. Surfacing each rust test's `.dag` reads as a declared, lens-visible dependency is the shared blocker all three consumers wait on — and because the coverage wall is only sound when `closure ⊇ actual-reads`, this structural discovery is the **load-bearing core**, not the tail. It is the hard part and the multi-day driver precisely because it is where the soundness is bought."), + h2(text: "First vertical slice (smallest end-to-end, green-by-execution)"), + ul(items: [ + li(text: "Pick ONE rust test with a clear `.dag` closure — `coproduct_reflection_conformance_test` (inputs entirely `.dag`) is the natural first."), + li(text: "Declare its consumed-.dag closure on the carrier."), + li(text: "Wire `should_run_gates` to fire when a changed path is in THAT test's declared closure."), + li(text: "Prove by execution with a discriminating control: a diff to a `.dag` IN the closure FIRES the gate; a diff to a `.dag` OUTSIDE the closure does NOT. Green = both directions observed."), + li(text: "This proves the structural fact end-to-end on one test before any corpus fan-out."), + li(text: "**State explicitly which the slice proves.** For the slice to prove the *coverage direction soundly*, `coproduct_reflection_conformance_test`'s closure must be **structurally derived** (so a newly-added `.dag` read is captured automatically). If slice-1 hand-lists the closure as an interim, it proves the *wiring* (fire/skip plumbing) but NOT the *wall* (drift-proof completeness) — and must be labelled accordingly. The keystone's value is the wall, so the slice should target the derived closure, not the hand-listed one."), + ]), + h2(text: "Honest estimate"), + p(text: "Multi-day."), + ul(items: [ + li(text: "Slice 1 (one test: declare + gate-fire + discriminating control): ~1 day."), + li(text: "Shared blocker (structural .dag-closure discovery through opaque host reads, lens-visible): the bulk — ~2–4 days, depending on whether the host-read seam can surface declarations cheaply or needs the reflection layer deepened."), + li(text: "Corpus fan-out + completeness lens: after."), + ]), + h2(text: "Decoupling"), + p(text: "Independent of #5427. #5427 is the cheap `.rs`-hole-closer (widen the rust gate's test command on `.rs`-touching PRs) — lands now, behind the two operator levers. Edge-(b) is the structural keystone that later makes the rust gate BOTH sound on `.dag` changes AND affordable by selection. Neither blocks the other."), + ] +} + +data edge_b_rust_dag_provenance_brief_plan: Plan = Plan { + slug: "edge-b-rust-dag-provenance-brief", + title: "Edge-(b) scoped dispatch brief — rust-test ↔ consumed-.dag provenance (the coverage keystone)", + body: edge_b_rust_dag_provenance_brief_body(), + dissolution: HasTrigger { + text: "Delete this brief once edge-(b) is built and merged — the rust-test→consumed-.dag closure is a structurally-derived (drift-proof) declared fact on the NodeArtifactProvenance carrier, the coverage wall fires the rust gate on an in-closure .dag change (closure ⊇ actual-reads, lens-checked on correctness not presence), and the affordability selector skips unaffected rust tests — so the scoping decision this doc records is realized." + } +} diff --git a/dsl/gunbc/plans/realization_measurement_loop.dag b/dsl/gunbc/plans/realization_measurement_loop.dag new file mode 100644 index 00000000000..9f27d7b02d5 --- /dev/null +++ b/dsl/gunbc/plans/realization_measurement_loop.dag @@ -0,0 +1,187 @@ +module gunbc.plans.realization_measurement_loop + +import gunbc.plan { Plan, DissolutionTrigger, HasTrigger } +import std.markdown { MarkdownBlock, CodeBlock, TableBlock, AlignNone, ThematicBreak } +import gunbc.plans.md_helpers { h2, h3, p, li, ul, ol, cell, row, quote, hr } + +fn realization_measurement_loop_body() -> List { + [ + p(text: "**Status:** stable coordination plan · dispatch workers per phase · **DESIGN.md + the carriers remain the authority** — this doc is a worker-dispatch tracker, not a fact ledger, and each phase dissolves into a mark on its carrier when it lands (DESIGN §6 \"no parallel-ledger docs\"). A phase's real state is its branch/PR, not this file (mirrors `ROADMAP.md`)."), + p(text: "**Owner:** unowned (original coordinator `zesty-deer-479` archived 2026-06-21) — operator-coordinated; consolidates the formerly-separate quick-ant-298 dependency-ordered roadmap (single authority, no fork). Linked from `ROADMAP.md` §2 *Minimal work — caching by realization*."), + hr(), + h2(text: "0. Thesis — the substrate is shape-complete but input-starved"), + p(text: "The realization layer is *fully modeled and almost entirely inert*: every carrier that should drive \"minimal work, as parallel as possible, guaranteed\" exists with the right type and is read by **no scheduler, fed by **no measurement, consulted by **no router. This is DESIGN §6's failure mode — *\"the tier where the machinery exists but nothing gates on it\"* — landed squarely on §1's **cost axis**."), + p(text: "The fix is **one control loop**, not a pile of local patches (this is why §4 \"evaluate the whole pipeline\" is load-bearing, not a footnote):"), + CodeBlock { code: " measure (Phase 0) ← the keystone; makes cost a real fact\n → CostAccount.time = Measured (today: cost_account_predicted_zero())\n → RealizationObjective Pareto over \{time, space, power, $\}\n bounded by a deployment HardwareBudget (Phase 1 / Phase 3)\n → Schedule width + shard balance + cache-layer choice\n → total rolled up along the CRITICAL PATH, not the node sum (Phase 1.5)\n" }, + p(text: "The three notes from the operator are **not peers — they are a dependency chain rooted at measurement**: `minimal work` = §2 (cache planner) and `as parallel as possible` = §1 (width) can only be *optimized against a measured cost*, and `guaranteed` = §5 (measured, not predicted). Cost must become a measured fact before anything can plan against it. The independent CI audit reached the same conclusion (\"add the two-clock timing first\"); the dependency structure above is *why*."), + h3(text: "The end-state acceptance gate (what the whole plan builds to)"), + quote(blocks: [ + p(text: "For every pure transform `T` (resolve, parse, typecheck, *and* derived analyses like complexity-synthesis / affected-set — see `ROADMAP.md` §3 *Complexity / synthesis lens* and §4 *Testgen*), `realize(T)` returns a result content-addressed by `hash(inputs ⊕ content(T))`, materialized at the **minimal `Placement` spanning T's consumers (its reach)**. A transform that is **non-redundant** (shared across a layer boundary, or recompute-cost > cache-cost) with **no cache supplier at its reach layer** is a located, typed **ERROR** that emits a *request to provision a supplier there*. No silent `Recompute`; no under-keyed hit."), + ]), + p(text: "This is §5 (fail-closed) turned on the cost axis: uncached non-redundant work is not \"slow\", it is an *error*. The earliest truthful point to assert it is the **redundancy-only** cut (shared-across-boundary — needs reach, not measurement); the cost-based \"non-redundant\" half waits on measured cost (Phase 0 / §4). The phases below are the path to this gate; the dependency-ordered spine that maps work items onto it is in **§ Dependency-ordered spine** (before Sequencing)."), + h3(text: "The invariant that governs every phase (DESIGN §3 / §4)"), + quote(blocks: [ + p(text: "**Pure schedule TOPOLOGY stays central and deterministic; every measurement-fed decision is a PERIPHERAL realization.**"), + ]), + p(text: "The schedule (`Schedule = List>`) is a deterministic partial order — it expresses what *can* run in parallel, hardware-free, and is pinned by the `schedule_eq` / `schedule_generates_identical_schedule` witnesses (`realization_schedule.dag:222-236`; `src/v2/test/claim/realization_schedule_witness.dag:35-48`). A schedule whose *width or membership* depended on a measured per-machine `HardwareThreadCount` would break that equality across hosts. So: **measured ⇒ peripheral, by construction.** Width, shard balance, cache-layer choice, and the timing tap all live in the periphery (`extdeps/realization`, the host realizer), checked by *\"given these DeploymentFacts + these measured costs, the realizer picks X\"* witnesses — deterministic *given their inputs*. This is exactly what the `CostAccount` dissolve-on comment anticipates (`realization_schedule.dag:25-26`). Most `.dag` programs are stateless/short-lived: they declare dependency structure and never mention hardware; the width-fold degenerates to \"just run it.\""), + h3(text: "Realization has THREE dimensions (schedule · cache · compute-fabric)"), + p(text: "\"Realization\" is one concept with three orthogonal-but-composed dimensions, **all keyed on the same content-addressed `ExecutionReceipt`**, all **peripheral** (§3), all governed by the **same measured cost + Pareto objective**:"), + TableBlock { + header: row(cells: [cell(text: "Dimension"), cell(text: "Carrier"), cell(text: "Asks"), cell(text: "§1 axis")]), + alignments: [AlignNone, AlignNone, AlignNone, AlignNone], + rows: [ + row(cells: [cell(text: "**schedule**"), cell(text: "`std.realization_schedule`"), cell(text: "*when / how parallel*"), cell(text: "parallel")]), + row(cells: [cell(text: "**cache**"), cell(text: "`std.cache_interface`"), cell(text: "*whether it needs to run at all*"), cell(text: "§2 minimal work")]), + row(cells: [cell(text: "**compute fabric**"), cell(text: "`product.compute_fabric`"), cell(text: "*where / on what it runs* (provision)"), cell(text: "placement / $")]), + ], + }, + p(text: "The proof they are dimensions of *one* concept rather than three separate models is **structural and already in the tree**: cache `MUST NOT import compute_fabric` (`cache_interface.dag:4`) and compute_fabric `MUST NOT import cache_interface` (`compute_fabric.dag:9`); **both compose only over `ExecutionReceipt`**. They meet *only* at the content-addressed receipt — never by direct coupling (§3/§4)."), + p(text: "**The `compute_fabric()` zero-arg interface is the same §3 move as the whole plan.** `compute_fabric` is a **demand → placement → supply** market: an execution emits a `WorkDemand` (isolation, memory, GPU) and `satisfies(offer, demand)` (`compute_fabric.dag:377`) places it on a satisfying `ComputeOffer`. \"Provision compute for this execution\" with **empty args** = the `WorkDemand` is *inferred from the .dag-modeled execution*, and placement is *resolved from the deployment's offers* — **neither is a caller argument**. Identical to the cache planner auto-wiring and the scheduler's hardware-budget fold: *caller declares intent; the realization is resolved from modeled deployment facts.* All three dimensions share this."), + p(text: "**Layering discipline (§3):** `compute_fabric` and `placement_supply` are **product**; schedule/cache are **std** (imports point toward std). Split: product owns the *placement projection carrier* (`product.placement_supply` ✓) and std owns the `\{time,space,power\}` cost-axis measure carriers it composes; product `compute_fabric` owns the **$/billing axis** (`CostClass`, `MoneyMicros`) and *projects* fleet rows into that carrier (`placement_supply_row`, `compute_fabric.dag:220`); the **peripheral host realizer** bridges product→std and runs the Pareto pick. std stays product-free."), + h3(text: "v2 is the target; v1 is the proving ground (DESIGN §7)"), + p(text: "v1 (the Rust seed) is shrinking to zero; v2 (the self-hosted `.dag` compiler) is what must benefit. **Every phase's durable artifact is `.dag` that v2 inherits; the Rust seed is only the proving *handler* — where a host-effect attaches today, while v2 is mid-bootstrap and the v1 interpreter is still the only evaluator that actually runs.** You MAY edit v1 (it's a proving ground), but:"), + quote(blocks: [ + p(text: "**The v2-benefit test:** if a phase's deliverable is a Rust patch with *no `.dag` model*, it failed. The carrier / lens / kernel / effect-shape is the artifact; the Rust code is one handler of it (§2 one-shape-N-handlers; §3 measured⇒peripheral; §7 Rust→zero)."), + ]), + p(text: "This is *why* the keystone's measurement is modeled as an **effect-shape + `PerformanceReceipt` carrier + a roll-up lens over the Node fold** (the same `fold_node` v2's own evaluator uses) — so when v2 self-hosts, the instrumentation, the cache kernel, the scheduler, and the fabric all come along for free. The Rust tap in `v1_interpreter.rs` *proves* the model green-by-execution today; it is the realization, not the authority. Per-phase split: **Phase 0** durable = the `.dag` measure model/lens, proving = the Rust eval tap; **Phase 1** durable = the `.dag` width-fold (`scheduler.dag` is already v2), proving = the `claim_executor` spawn cap; **Phase 1.5a/2/3** are already `.dag`-native (`v2.lens.affected_set`, the cache catalog/kernel, `compute_fabric`/`ci_yaml_emit`) — v2-inheriting by construction; only the cache *backends* (`resolved_graph_cache.rs`, `ParseTableMemo`) stay v1 handlers of the one `.dag` kernel."), + hr(), + h2(text: "Verified ground truth (file:line — do not re-derive)"), + TableBlock { + header: row(cells: [cell(text: "Fact"), cell(text: "Evidence")]), + alignments: [AlignNone, AlignNone], + rows: [ + row(cells: [cell(text: "Schedule width = full dependency frontier, **no capacity bound**"), cell(text: "`ReadinessLayer.ready: List` `src/v2/workflow/scheduler.dag:29`; `runnable_frontier_from_dependencies` `scheduler.dag:147-154`")]), + row(cells: [cell(text: "Thread-spawn **unbounded by hardware** (one OS thread per runnable-in-batch)"), cell(text: "`thread::spawn(... run_one_runnable ...)` `src/v1/stage0/src/bin/claim_executor.rs:403-410`")]), + row(cells: [cell(text: "Corpus = **one** `RunnableDiscoveryBatch` node → serial `for` loop (293 witnesses invisible)"), cell(text: "`ci_floor_plan.dag:107`; `run_discovery_corpus` serial loop `cli_run.rs:2148-2171`")]), + row(cells: [cell(text: "`CostAccount.total` is hardcoded zero"), cell(text: "`cost_account_predicted_zero()` `realization_schedule.dag:33-39`; `CostBasis/Measured` exist **only** in the `:25-26` dissolve-on comment")]), + row(cells: [cell(text: "Single eval seam exists; per-variant self-time tap already there, **not** content-hash-keyed, **not** fed to CostAccount"), cell(text: "`eval_expr` `v1_interpreter.rs:1451`; profiler `:1466-1476` (keys by `expr_variant_index`)")]), + row(cells: [cell(text: "Per-witness/per-resolve wall-clock timing **exists but only goes to stderr**"), cell(text: "`claim_batch.rs:372,404`; the floor runner `claim_executor.rs` does no timing; `DiscoverySummary` keeps only `\{total,passed,failures\}` `cli_run.rs ~1903`")]), + row(cells: [cell(text: "Cache catalog has **zero runtime consumers**; `CacheLayerPlan` unused"), cell(text: "`cache_interface.dag:91`; importers are comments only (`realization.dag:16`, `02_parse.dag:162-168`)")]), + row(cells: [cell(text: "3 live caches hand-wired, **3 different key derivations**"), cell(text: "`resolved_graph_cache.rs:76-199` (content-hash); `ParseTableMemo` `v1_interpreter.rs:768,1116` (in-proc map); `pure_call_memo` keys by **address** `(usize,Vec)` not hash `v1_interpreter.rs:748-752`; sccache external")]), + row(cells: [cell(text: "Carrier for hardware budget **already exists**"), cell(text: "`HardwareThreadCount = Measure` `measure.dag:254`; `PlacementSupplyRow.hardware_threads` `placement_supply.dag:29-31`; `CpuDeploymentFacts` `cpu/types.dag:42`")]), + row(cells: [cell(text: "Pareto kernel + objective vocabulary already shared"), cell(text: "`std.pareto` dominance + `AxisGoal`; `RealizationObjective.goals: List` `realization_schedule.dag:41`")]), + row(cells: [cell(text: "Runner model exists; ci.yml **is generated + byte-drift-gated**"), cell(text: "`RunnerSpec = HostedRunner \| SelfHosted\{labels\}` `extdeps/github/actions.dag:233` (emission consumer is a future trigger, `:226-232`); generator = `expected_ci_yml()` `dsl/gunbc/ci_yaml_emit.dag:9`, drift gate `dsl/tools/ci_yaml_gate.dag` (byte-for-byte), parse-validate `dsl/gunbc/ci_yaml_validate.dag`. **NOT** `dsl/tools/gunbc_ci.dag` (a 732B wrapper). ⚠️ `extdeps/github/ci.dag:7` has a **stale** comment \"ci.yml is hand-edited, not generated\" — contradicts the live gate; ignore it (track for deletion). `runs-on: [self-hosted,linux,arm64]` is emitted as a **literal** today — the seam Phase 3a routes through `RunnerSpec`")]), + row(cells: [cell(text: "A 3rd (richest) measured-time carrier already exists"), cell(text: "`compute_fabric.PerformanceReceipt\{wall_duration:Duration, sample_count, confidence: MeasurementConfidence = SingleSample\|Range\|DistributionSummary\}` `:414-423`; on `ExecutionReceipt.performance :453` + `ComputeSupplyFacts.observed_performance :166`")]), + row(cells: [cell(text: "`ExecutionReceipt` digest is **itself a stub** (not yet a content hash)"), cell(text: "`execution_receipt_digest` returns `receipt.work.id` (a hand-authored brand) `:588-594` — \"full canonical encoding supplied by the harness when Outcome/ArtifactRef inhabit\"")]), + row(cells: [cell(text: "Corpus sharding already has a demand-model home"), cell(text: "`ParallelismShape = ... \| IndependentShards\{shard_count\} \| PartitionedReduce\{...\}` `compute_fabric.dag:280-289`; `WorkDemand.parallelism :273`")]), + row(cells: [cell(text: "srv1/srv2 concrete facts are **ctrl-tier (private), not public gunbc**"), cell(text: "`hardware_selection.dag:8`; `compute_fabric.dag:5` (\"ctrl `plans.fabric.operator_fleet`\")")]), + row(cells: [cell(text: "compute fabric = demand→placement→supply market; provisioning is `satisfies(offer, demand)`; composes over `ExecutionReceipt`"), cell(text: "`product.compute_fabric` — `WorkDemand` `:268`, `ComputeOffer`/`satisfies` `:377`, `ExecutionReceipt` `:449`, projects `PlacementSupplyRow` `:220`; `satisfies` checks **isolation only** today (no thread-count/Pareto dim)")]), + row(cells: [cell(text: "map→reduce execution decomposition is forward-stubbed (`= Node`) — anticipates sharding"), cell(text: "`WorkGraph`/`Partitioner`/`Reducer`/`SymbolicCost`/`EffectBoundary` `compute_fabric.dag:48-58`")]), + ], + }, + hr(), + h2(text: "Phase 0 — Measured cost (THE KEYSTONE)"), + p(text: "**Goal:** flip `CostAccount.time` from `predicted_zero` to `Measured`. Everything quantitative depends on this. NB: the timing *primitives already exist* — this is **\"wire the existing tap to a content-hash key + CostAccount,\"** not \"build timing from scratch.\""), + ul(items: [ + li(text: "**Grain decision (settled this session): key on the content-hash of the cache SUBJECT, not per-AST-node, not per-variant.** Rationale: the `Node` is an `Rc` with **no ambient content-hash** (today the profiler keys by `expr_variant_index`), so per-node hashing at `eval_expr` is *not free* and would perturb the measurement (§5 observer effect). The cache-subject frame is exactly where a content-hash *is already computed*, and it is the grain the scheduler (per-Runnable) and the cache router (per-subject recompute cost) both consume — so per-subject is the §2 \"model once, derive every use\" point: per-Runnable is its aggregate, per-variant its `group-by`, full per-node an **opt-in deep projection** over the same seam. Per-variant counters are a *dead end* (a variant is not a cacheable identity → can't feed Phase 2)."), + li(text: "**Instrumentation = the dual of the cache.** Both wrap the same fold boundary keyed by the same content-hash: the cache stores node→value, the instrument stores node→duration. The *analysis* is a pure lens; the measurement itself is a §1 host-effect. Use the existing gross−children self-time decomposition (`v1_interpreter.rs:1466-1476`)."), + li(text: "**The measurement output is a `PerformanceReceipt`, NOT a new struct (§3 — do not coin a 4th).** The observation carrier already exists: `compute_fabric.PerformanceReceipt\{ wall_duration, sample_count, confidence \}` (`compute_fabric.dag:414-423`), and `ExecutionReceipt.performance` (`:453`) already hangs it on the receipt. So Phase 0 emits a `PerformanceReceipt` keyed by the cache-subject hash → it rolls up into `CostAccount.time` (the aggregate). This is what *fuses the keystone to the compute-fabric deliverable*: the thing Phase 0 measures **is** the fabric's execution receipt, and `MeasurementConfidence` (SingleSample/Range/DistributionSummary) is exactly the per-witness-distribution honesty the audit's observability gap needs."), + li(text: "**Feed `CostAccount`.** Add `CostBasis = Measured | Predicted` (the `:25-26` dissolve-on); aggregate PerformanceReceipts → `RealizationPlan.total`."), + li(text: "**Converge the time authorities — there are THREE, not two (§3).** `NanosecondDuration` (`measure.dag:258`) is the authority. `TestNodeCostDimension.measured_ms` (Milliseconds, `verification.dag`) **dissolves** into a budget-*predicate* over the measured `CostAccount.time` (a ns threshold), not a parallel measured field (ms truncates a 5 ns step to 0 — DESIGN §6). And `PerformanceReceipt.wall_duration` is the *observation* feeding the roll-up — observation vs roll-up, not a fork. Net: one observation carrier (`PerformanceReceipt`), one roll-up (`CostAccount.time`), `measured_ms` deleted."), + li(text: "**Persist the dropped timing.** Carry per-witness/per-entry timing through `DiscoverySummary` and the floor path (`claim_executor`), closing the audit's observability gap (the \"two-clock\" per-entry-resolve vs aggregate-per-witness split) — which is *itself* the profiling the operator was about to do by hand, made first-class."), + li(text: "**§5 gate:** purity oracle — witness verdicts byte-identical instrumented vs not."), + li(text: "**Dissolution trigger:** `cost_account_predicted_zero()` has no callers on the floor path; `measured_ms` deleted."), + ]), + hr(), + h2(text: "Phase 1 — Make parallelism visible + hardware-bounded width (note 1)"), + p(text: "**Depends on:** Phase 0 (shard balance needs measured per-shard cost)."), + ul(items: [ + li(text: "**Explode the corpus node** (`ci_floor_plan.dag:107`) into per-entry-group `Runnable`s — **rows, not Rust**. Express it as a `WorkDemand` whose `parallelism = IndependentShards\{shard_count\}` (`compute_fabric.dag:282`) — the corpus is today a *degenerate (unsharded) projection* of exactly that, so this reuses the carrier rather than minting a scheduler-local shard list. Shard *by whole entry-group* to preserve the warm `typed_module_cache` (splitting an entry's witnesses re-incurs its cold resolve). This is the keystone both background audits independently named."), + li(text: "**The hardware budget is what `compute_fabric` PROVISIONS — do not coin a fresh carrier (§2/§3).** The width-fold reads the `PlacementSupplyRow` that `compute_fabric` already projects (`placement_supply_row`, `compute_fabric.dag:220`; `PlacementSupplyRow.hardware_threads` `placement_supply.dag:29-31`). **The width decision *is* a placement decision:** today `satisfies(offer, demand)` (`compute_fabric.dag:377`) checks *isolation only* — Phase 1 is \"add the thread-count / Pareto dimension to placement.\" So this phase is co-designed with Phase 3 (compute_fabric is the provisioning interface; the runner *declares* the offer, the scheduler *consumes* the placement — one market, two readers). DFS `PlacementSupplyRow` + `CpuDeploymentFacts` (`cpu/types.dag:42`) before extending; do **not** invent `DeploymentFacts`."), + li(text: "**The width-fold.** Schedule stays the pure partial order; a peripheral realizer folds it against the `HardwareBudget` → actual width, a Pareto pick over `\{wall-time↓, peak-memory↓\}` bounded by `width ≤ cores` — reusing `std.pareto` + `RealizationObjective.goals` (already `List` — wiring carriers that already speak the same vocabulary, not inventing one)."), + li(text: "**Bound the spawner** (`claim_executor.rs:403-410`) by `available_parallelism`/budget — fixes the *dual* hazard: under-parallel (serial corpus) **and** over-parallel (unbounded spawn on a wide batch)."), + li(text: "**Determinism:** schedule topology stays witness-stable; width/shard are peripheral, checked by given-these-facts witnesses."), + li(text: "**Dissolution trigger:** the corpus is ≥2 runnables in the schedule; the spawner reads a budget."), + ]), + hr(), + h2(text: "Phase 1.5 — Holistic cleanups (note 4) · mostly parallel to 1"), + ul(items: [ + li(text: "**Wire `affected_set` into the corpus + gate roster** (audit lever #1). The compile-time, fail-closed `v2.lens.affected_set` + runner + superset proof exist and are green but unimported. Skip only on a content-addressed match to a verified-green baseline; **fail closed** on any miss. Biggest wall-clock lever on PR branches. (Independent of Phase 0.)"), + li(text: "**`total` = measured critical-path roll-up** (note 4): weights a short phase *on the critical path* (the perturb gate) at full cost and a short phase *hidden under a parallel branch* at ~0. (Needs Phase 0.)"), + li(text: "**Collapse the perturb cold-recompile** (~14 s, fail-fast root, critical path): resolve the planted (fresh-name, unimported) module against the green compile's index instead of `cp -r dsl` + cold rebuild; preserves the discriminating-red (§5). (Independent of Phase 0.)"), + ]), + hr(), + h2(text: "Phase 2 — Cache-layer planner: the catalog's first consumer (note 2)"), + p(text: "**Depends on:** Phase 0 (cost-aware reach needs measured recompute cost)."), + ul(items: [ + li(text: "**Land the planner the catalog header already promises** (`cache_interface.dag:21` \"downstream cache lookup planner\"; dissolve-on-arrival \"when first consumer lands\"). Given the `CacheInterfaceFacts` rows + a deployment's *available* backends, emit a `CacheLayerPlan` (type exists, `:91`): L1 in-process → L2 sccache / cargo target / resolved-graph → L3 CAS."), + li(text: "**One content-address lookup kernel, N backends bound by `transport_encoding`** (§4 one-kernel/N-handlers). The in-process memo is just the `InProcess` row of the *same* kernel. **Converge the key derivations onto ONE content-addressed subject identity.** Today there are *four* keyings: `parse_cache` by path, `typed_module_cache` by module-name, `resolved_graph` by content-hash, `pure_call_memo` by address — **and the `ExecutionReceipt` digest the whole three-dimension unification rests on is itself a 4th stub**: `execution_receipt_digest` returns `receipt.work.id`, a hand-authored brand, not a content hash (`compute_fabric.dag:588-594`). The §0 thesis (\"all three dimensions keyed on one `ExecutionReceipt`\") is only *true once this digest becomes a real content hash aligned with the cache-subject identity* — so this convergence is shared work between Phase 2 (cache) and the compute-fabric track, not cache-local. The `key_derivation` axis exists for exactly this."), + li(text: "**Cost-aware reach (§1).** Reach for a layer only when its predicted delta favors it: `min(recompute, lookup + p(miss)·recompute)` — `read_latency` (InProcessNs…WanTensMs) is already a modeled axis; `recompute` comes from Phase 0. A WAN CAS hit can lose to recomputing a cheap node."), + li(text: "**Auto-wire (the operator's \"user shouldn't wire it themselves\").** The deployment declares which backends it offers; the planner emits the wiring — dissolving the bespoke `if sccache --show-stats` shell in `ci.yml` and the `GUNBC_RESOLVED_GRAPH_CACHE_DIR` env read."), + li(text: "**Fail-closed (§5).** A backend probe that is absent/unauthorized falls through to the next layer → ultimately recompute, **never** serves a stale/unverified hit (`CacheRejectReason` already enumerates `BackendUnavailable`/`BackendUnauthorized`). Verdict-identity, not byte-identity, until the deferred canonical-byte compare lands — so do NOT route emit/lower consumers through it yet."), + li(text: "**First free measurement:** un-dormant `resolved_graph_cache` in CI (read by the seed, unset in `ci.yml`) as a warm A/B."), + li(text: "**Dissolution trigger:** `ci.yml` carries no hand-wired cache shell; one lookup kernel; one subject key."), + ]), + hr(), + h2(text: "Phase 3 — Infra / deployment onto `.dag` (srv1 / srv2) · the second ask"), + p(text: "**Goal:** model the actual infra/deployment — runner config, access, host config — as **data**, dissolving bespoke `ci.yml` shell + manual runner setup. **\"Get CI onto `.dag`\" = instantiate `compute_fabric` for srv1/srv2:** a self-hosted runner is one `ComputeOffer`; GHA-hosted, `Ubicloud`, `GcloudRun` are others (already enumerated, `compute_fabric.dag:71`). This meets note 1 at the placement carrier — the offer the runner *declares* is the budget Phase 1's scheduler *consumes*."), + p(text: "**§3 boundary — THREE tiers, not two (refined after the #5177 review).** The operator's rule: keep the *generic* \"CI runner\" cleanly apart from *our* CI runner; CI does not need to know our fleet. So:"), + ul(items: [ + li(text: "**3a-generic — \"CI runner\" in the abstract (any project).** What we expect *any* CI runner to do, project-agnostic: **a workflow triggered by an event** (`trigger → workflow`), realized per platform. The GHA realization already exists — `Workflow\{ on: List, jobs \}` + `WorkflowTrigger` (`actions.dag:56,79`) and `RunnerSpec` (`:233`). The **generic `offer → RunnerSpec` projection** (`runner_spec_from_offer`, kernel/arch → labels) belongs HERE, next to `RunnerSpec` in the generalized layer — it works for *any* fleet offer. **This tier MUST NOT import a concrete SKU (`extdeps.cpu.ampere`) or name srv1/srv2.** (GitLab/Buildkite/etc. would be sibling platform handlers — one generic interface, N realizations, §2/§4.)"), + li(text: "**3a-ours — OUR gunbc CI runner (our repo's META-modeling).** OUR workflow instance + OUR fleet: the srv1/srv2 *instantiation* (the Ampere-Altra `ComputeOffer`, the `gunbc-ci-fleet` identity, the per-thread Hz). This **must live in a file that is gunbc's own meta-model** (`dsl/gunbc/ci_*`), and it *consumes* the 3a-generic interface — it is where the concrete SKU import is legitimate. The srv1/srv2 instantiation meta-model is public-in-our-repo; only secrets cross into ctrl."), + li(text: "**3b — ctrl concrete fleet (private).** Access creds, runner registration tokens, truly-secret per-host config — **ctrl `plans.fabric.operator_fleet`** (`compute_fabric.dag:5`; `hardware_selection.dag:8`; memory `idea-pr-compiler-ctrl-boundary`). Concrete rows instantiated against the 3a-ours meta-model."), + ]), + p(text: "**⚠️ #5177 needs this rework (do right after it merges).** `dsl/gunbc/ci_runner.dag` as merged **fuses 3a-generic with 3a-ours**: the generic `runner_spec_from_offer` projection + kernel/arch label tables sit in the *same module* as our concrete fleet (`gunbc_ci_cpu = altra_q6430_catalog`, `gunbc_ci_host_identity = \"gunbc-ci-fleet\"`), and it `import extdeps.cpu.ampere` — a concrete SKU — into what should be the generic interface. Split it: **generic projection → the generalized layer beside `RunnerSpec`** (no SKU import, no fleet rows); **our fleet offer → a `dsl/gunbc/` meta-model file** that consumes the generic projection. Keep the generic interface MINIMAL (trigger→workflow + offer→RunnerSpec) — \"CI doesn't need to know everything.\" ci.yml stays generated + byte-drift-gated (`expected_ci_yml()` `dsl/gunbc/ci_yaml_emit.dag:9`, gate `dsl/tools/ci_yaml_gate.dag`); the emit consumes *our* runner spec, which is *our* fleet offer projected through the *generic* seam. ⚠️ also delete the stale `extdeps/github/ci.dag:7` \"hand-edited, not generated\" comment."), + p(text: "**Dissolution trigger:** `.github/workflows/ci.yml` is emitted from a `.dag` spec whose runner block is *our* fleet offer projected through the *generic* `offer → RunnerSpec` seam (no hand-authored runner block, no fleet SKU in the generic tier); the `HardwareBudget` the scheduler reads is the one *our* offer declares."), + hr(), + h2(text: "Dependency-ordered spine (foundation → end state)"), + p(text: "The work-item view of the phases above, ordered by dependency toward the acceptance gate (absorbed from the former quick-ant-298 roadmap; maps onto the phases, does not replace them)."), + ul(items: [ + li(text: "**F1** scheduler gives heavy nodes the budgeted width — *#5421 merged* (= Phase 1 width landing)."), + li(text: "**F2/F3** key-completeness lens (`ToolchainChange ∈ triggers ⟹ input ∈ inputs_considered`) + `resolved_graph` keyed by construction — *#5423, in review* (= the Phase 2 key-derivation axis, spec-level)."), + li(text: "**P1 — honest keys, verified by execution** *(deps F2,F3)*: realizer-key lens (executed digest ⊇ declared `inputs_considered`, RED otherwise — would have caught the `from_utf8_lossy` collision); stable transform-id (reproducible source/commit/tree hash, not binary bytes); census parity for `parse_table_memo`. (= Phase 2 \"converge key derivations\".)"), + li(text: "**P2 — one door: caching by inhabitance** *(deps P1)*: `realize(subject)` as the sole API; eliminate raw bypass (`build_multi_entry_index`, hand-rolled `ParseTable` HashMap → inhabited via `realize`, DESIGN §6's own example). (= Phase 2 one-kernel/N-backends.)"), + li(text: "**P3 — reach → layer + completeness fail-closed** *(deps P2)* — **the core ask / the acceptance gate**: reach analysis lens (consumer set + boundary → minimal sufficient `Placement`); completeness gate (subject realized below reach → ERROR; non-redundant transform with no supplier at reach → ERROR — **land the redundancy-only cut first**, cost half waits on §4); supplier provisioning + typed request."), + li(text: "**P4 — economic tier** *(deps Phase 0 measurement)*: per-transform measured cost (`PerformanceReceipt` → cost-aware reach); `Materialization` = `Recompute | Memoize | Share` chosen by measured cost."), + li(text: "**P5 — v2 dissolution** *(deps B2)*: `content(T) = content_hash(subgraph)` native; dissolves the binary-hash/version-string approximations and makes P1's spec↔realizer check structural."), + ]), + p(text: "**External blockers (track as work-items):** **B1** #5295 generic-instantiation (FreeMonoid cached without variants — itself an under-keyed in-proc cache) → gates cross-shard `Share` (Phase 2.2). **B2** v2 cross-tree content-hash (\"increment 4\", the `ContentHash` subject on `RealizedStep`; cf. the `execution_receipt_digest` stub at `compute_fabric.dag:588-594`) → gates P5."), + p(text: "**Critical path:** `F2/F3 → P1 → P2 → P3 (redundancy cut) → P3 supplier`. `P1.census`, `P4`, and Phase-2 sub-items parallelize off it; cross-shard `Share` and P5 wait on B1/B2. The redundancy-only P3 cut is the earliest point \"uncached non-redundant work is an error\" is truthful — it needs reach, not the cost model."), + h2(text: "Sequencing & dispatch"), + CodeBlock { code: " ┌─────────────── Phase 0 (keystone: measured cost) ───────────────┐\n │ │\n Phase 1.5a (affected_set) Phase 1 (visible parallelism Phase 2 (cache planner)\n Phase 1.5c (perturb) + hardware-bounded width) │\n — independent of 0 │ │\n │ Phase 1.5b (critical-path total) ←──────┘ (needs 0)\n │\n Phase 3a (runner schema + ci.yml gen) — HardwareBudget carrier co-designed with Phase 1\n │\n Phase 3b (ctrl: srv1/srv2 concrete) — private, separate repo\n" }, + TableBlock { + header: row(cells: [cell(text: "Phase"), cell(text: "Depends on"), cell(text: "Intricacy / Volume"), cell(text: "Notes")]), + alignments: [AlignNone, AlignNone, AlignNone, AlignNone], + rows: [ + row(cells: [cell(text: "0 keystone"), cell(text: "—"), cell(text: "high / medium"), cell(text: "root of everything quantitative; load-bearing seam (`v1_interpreter.rs`, escalate per DESIGN)")]), + row(cells: [cell(text: "1 visible parallelism + width"), cell(text: "0"), cell(text: "high / medium"), cell(text: "shares `HardwareBudget` carrier with 3a")]), + row(cells: [cell(text: "1.5a affected_set"), cell(text: "—"), cell(text: "medium / small"), cell(text: "fail-closed; can start now")]), + row(cells: [cell(text: "1.5b critical-path total"), cell(text: "0"), cell(text: "medium / small"), cell(text: "")]), + row(cells: [cell(text: "1.5c perturb collapse"), cell(text: "—"), cell(text: "medium / small"), cell(text: "can start now")]), + row(cells: [cell(text: "2 cache planner"), cell(text: "0"), cell(text: "high / large"), cell(text: "converges 3 key derivations; first catalog consumer")]), + row(cells: [cell(text: "3a runner schema + ci.yml gen"), cell(text: "(1 for budget carrier)"), cell(text: "high / large"), cell(text: "public; extends `CiFloorSpec` emission")]), + row(cells: [cell(text: "3b ctrl srv1/srv2"), cell(text: "3a"), cell(text: "—"), cell(text: "**private `~/ctrl`**, separate PR")]), + ], + }, + p(text: "**Start-now lanes (no measurement dependency):** 1.5a (affected_set), 1.5c (perturb), and 3a schema groundwork. **Critical path:** Phase 0 → 1 / 2."), + hr(), + h2(text: "Guardrails for every worker (DESIGN)"), + ul(items: [ + li(text: "**Pure central spec, peripheral measured realization** (the §3 invariant above). Anything measured is peripheral — never in the schedule topology the `schedule_eq` witnesses pin."), + li(text: "**DFS existing carriers before minting** (§2/§3): `PlacementSupplyRow`, `CpuDeploymentFacts`, `RunnerSpec`, the cache catalog, `std.pareto`, `RealizationObjective.goals`. The vocabulary mostly exists — wire it, don't re-coin it. (Background verification specifically flagged: do not invent a fresh `DeploymentFacts`.)"), + li(text: "**Rows, not Rust** — express new schedule/cache/runner facts as data; do not cement the seed to satisfy a ratchet (the ratchet is downstream of substrate migration)."), + li(text: "**v2-benefit test (§7)** — the durable artifact is `.dag` that v2 inherits; the Rust seed is only the proving *handler*. A deliverable that is a Rust patch with no `.dag` model failed. (See the §0 \"v2 is the target\" principle.)"), + li(text: "**Fail-closed (§5)** + **purity oracle** on every memo/measurement (byte-identical warm-vs-cold; verdict identical instrumented-vs-not). A bounded \"forever\" ≠ an \"unknown\" error."), + li(text: "**Green by execution, not spec-without-execution.** A real consumer runs green + a discriminating input goes red. Typecheck + grep are not consumers."), + li(text: "**Each phase lands with a named dissolution trigger; the mark is on the carrier.** This doc is coordination only; delete its entry when the carrier records the fact."), + li(text: "**Load-bearing files** (DESIGN-named pipeline stages, substrate types, gates: `v1_interpreter.rs`, `cli_run.rs`, the scheduler, `realization_schedule.dag`) carry a higher bar — escalate before touching under a brief that pre-dates the relevant model PR."), + ]), + h2(text: "Open decisions to confirm before scoping the affected phase"), + ol(items: [ + li(text: "**Placement/budget carrier** — extend `compute_fabric`'s `satisfies` + `PlacementSupplyRow` with the thread-count/Pareto dimension (the width decision = a placement decision), vs a sibling carrier? (DFS task in Phase 1 / 3a.) Do not invent `DeploymentFacts`."), + li(text: "**The $/billing cost axis crosses the std↔product line.** std `CostAccount` carries `\{time,space,power\}`; the $ axis (`CostClass`, `MoneyMicros`) lives in product `compute_fabric`. Confirm: the std schedule's objective stays `\{time,space,power\}`; the **peripheral host realizer** combines it with the product $ axis for the full Pareto pick. (Keeps std product-free.)"), + li(text: "**Cache planner timing** — the *plan* (which layers, what order) can be compile-time data; only the *availability probe* is runtime/peripheral. Confirm the split when scoping Phase 2."), + li(text: "**Runner-label vocabulary** — how far to close `SelfHosted\{labels: List\}` toward a typed topology / a `compute_fabric` offer (3a) without over-fitting to srv1/srv2 (which live in ctrl)."), + li(text: "**Sharding lives in the demand model — Phase 1 and 3 meet at the parallelism shape, not just the budget.** `ParallelismShape = ... | IndependentShards\{shard_count\} | PartitionedReduce\{...\}` (`compute_fabric.dag:280-289`) already exists, and the corpus `RunnableDiscoveryBatch` is a **degenerate (unsharded) projection of a `WorkDemand` whose `parallelism = IndependentShards`** (independent witnesses). So the easy case needs no new stubs; the `Partitioner`/`Reducer`/`SymbolicCost = Node` forwards (`:48-58`) are only for the harder `PartitionedReduce` (whole-tree compile → reduce verdicts). Decide: does Phase 1 express the corpus as an `IndependentShards` `WorkDemand` (preferred — reuses the carrier) vs a scheduler-local shard list?"), + ]), + ] +} + +data realization_measurement_loop_plan: Plan = Plan { + slug: "realization-measurement-loop", + title: "Plan — Realization & Measurement: closing the cost → schedule loop (+ infra onto `.dag`)", + body: realization_measurement_loop_body(), + dissolution: HasTrigger { + text: "Delete this plan once the cost→schedule loop is closed — every pure transform's realize(T) is content-addressed by hash(inputs ⊕ content(T)) and materialized at its minimal Placement, CostAccount is fed by Measured basis (not hardcoded zero), schedule width is hardware-bounded and the spawner is bounded by available_parallelism, the cache catalog has live runtime consumers, and a non-redundant transform with no cache supplier at its reach is a located typed ERROR — so the substrate is measurement-fed rather than input-starved." + } +} diff --git a/dsl/gunbc/plans/resolver_type_name_collision_wall.dag b/dsl/gunbc/plans/resolver_type_name_collision_wall.dag new file mode 100644 index 00000000000..3d480bcc835 --- /dev/null +++ b/dsl/gunbc/plans/resolver_type_name_collision_wall.dag @@ -0,0 +1,125 @@ +module gunbc.plans.resolver_type_name_collision_wall + +import gunbc.plan { Plan, DissolutionTrigger, HasTrigger } +import std.markdown { MarkdownBlock, CodeBlock, TableBlock, AlignNone } +import gunbc.plans.md_helpers { h2, h3, p, li, ul, cell, row, hr } + +fn resolver_type_name_collision_wall_body() -> List { + [ + p(text: "Status: **MODEL — SIGNED (parent bright-stag, 2026-06-23).** The model (mechanism + Q2 policy + activation) is signed; **no resolver edit lands** until the §4 grounding de-fork is clean — the resolver guard is a separate, operator-gated future PR that lands on the de-forked tree. This document is the signed model; §3/§4 record the final ruling."), + p(text: "Owner: jolly-ant-231 (deepest resolver context from the A1 diagnosis). Capstone of the std de-fork lane. Q2 evidence: `docs/plans/dsl-v2-defork-audit.md` §2A (executed distribution)."), + hr(), + h2(text: "1. The hole this wall closes (grounding)"), + p(text: "The A1 (#5615) incident — `type 'EqualsClaim' not found in scope` on `src/v2/workflow/affected_set_floor_runner_test.dag` — was a **fail-OPEN in the resolver** (DESIGN §5): a wrong type resolution passed silently as a different, plausible binding."), + p(text: "Mechanism (proven by execution during the diagnosis; receipt below):"), + ul(items: [ + li(text: "The per-module type scope (`TypeEnv.bindings`) is a `HashMap>` keyed by the **interned id of the UNQUALIFIED type name** — the intern table is global, so two module-level types sharing a short name (`v2.std.verification.TestClaim` the Disj coproduct vs `std.verification.TestClaim` the Conj record) hash to the **same key**."), + li(text: "`import_bindings` is assembled by folding each imported module's bindings with a blind `v1_rt::rc_map_merge` (`v1_compiler_infer.rs` ~11799 and the duplicate ~12393). **Map merge overwrites on duplicate key — last writer wins, no diagnostic.** One authority silently shadows the other."), + li(text: "Because variant-constructor registration (`build_module_context`'s `variant_fold`, ~12894) only fires for `Disj` bindings, when the **record** won the `TestClaim` slot the coproduct's constructors (`EqualsClaim`, `StructuralEqualsClaim`, …) were never registered → \"not found in scope\". A1 was an innocent trigger: it merely grew the test's import-closure to include `std.verification(dsl)` (via `gunbc.ci_failure_class → extdeps.cache.sccache → std.cache_interface → std.verification`)."), + ]), + p(text: "The existing **`VariantCollision`** guard (`v1_std_core.rs:420`, `VariantCollision \{ variant, enum1, enum2, span \}`; emitted in `variant_fold` ~12908) already fails-closed on two imported coproducts sharing a **variant** name. It does **not** cover the level above: two modules contributing the same **type/enum name** to one closure. The wall is that guard lifted one level up — the §5 principle of making the bad state *unwritable* rather than letting it resolve to a plausible wrong binding."), + p(text: "`#5640` (the `TestClaim → AssertionClaim` rename) dissolved the single instance. The wall makes the **class** unwritable so the next closure-expanding PR cannot re-arm it."), + p(text: "Decidability: a closure exporting two distinct authorities under one unqualified name is a **decidable** condition (finite set of `(name_id, declaring_file)` pairs), so this is a §5 *wall now*, not a forever-ratchet. \"never\" is honest here."), + hr(), + h2(text: "2. Mechanism (the model)"), + p(text: "Replace the blind `rc_map_merge` of type bindings, at **both** import-binding assembly sites (`v1_compiler_infer.rs` ~11761 and ~12355 — themselves a §2 duplication this work should dissolve into **one** shared helper), with a **collision-checking merge**:"), + CodeBlock { code: "merge_type_bindings(acc, incoming, policy) -> \{ bindings, collisions \}\n for each (name_id, incoming_binding) in incoming:\n case acc.get(name_id):\n None -> insert\n Some(existing) ->\n if same_authority(existing, incoming): # re-export of ONE authority\n keep existing (no flag)\n else if policy.flags(existing, incoming): # TWO authorities, one name\n emit TypeNameCollision\{ name, module_a, module_b, span \}\n keep existing (deterministic) — fail-closed downstream\n else:\n keep existing (policy excused it)\n" }, + p(text: "Where:"), + ul(items: [ + li(text: "`same_authority(a, b)` ≡ `a.resolved.span.file == b.resolved.span.file` (one declaring file reached via multiple import paths is the SAME authority — a benign re-export, must NOT flag). `TypeBinding` is `\{ name, resolved: Rc, provenance \}` and `Node.span.file` carries the declaring file, so two-authorities-vs-one-re-export is distinguishable today — **no new field required.**"), + li(text: "`TypeNameCollision` is a new `CompilerDiagnostic` variant modeled exactly on `VariantCollision`: `\{ name: String, module_a: String, module_b: String, span \}`, classified **blocking** (`is_error_diagnostic` true), so it fails the resolve/typecheck closed with a located, typed message — the §5 \"loud error, never a warning\"."), + li(text: "Determinism: on collision keep the **first-seen** binding (stable under the existing dep-order traversal) so the error set is reproducible regardless of which authority \"would have won\" the old overwrite."), + ]), + p(text: "This is one mechanism; §3 (the policy) and §4 (activation) are knobs on it, not separate machinery."), + hr(), + h2(text: "3. KEY DECISION (parent's Q2): which collisions fail closed?"), + p(text: "**One predicate, one boolean knob** — `policy.flags(existing, incoming)`:"), + ul(items: [ + li(text: "**flag-ANY** (`require_structural_divergence = false`): `flags = true` for any two distinct authorities (different declaring files) under one name. Even a **byte/structurally-identical mirror** flags — because it is still *two authorities for one concept*, the §3 single-authority violation, just benign-looking. It remains a writable re-fork surface: nothing stops the two copies drifting apart later (which is exactly how A1's landmine formed)."), + li(text: "**flag-DIVERGENT** (`require_structural_divergence = true`): `flags = structural_inequality(existing.resolved, incoming.resolved)`. Fires only when the two definitions actually differ (connective and/or children) — like the Disj-coproduct vs Conj-record case. True mirrors are **excused**."), + ]), + p(text: "`structural_inequality` is a normalized structural compare of the two resolved type Nodes (connective + children names + field types), modulo span/occurrence — the same shape the emitter's coercion homomorphism check already walks; no new comparison primitive needed."), + h3(text: "Trade-off (parent rules on the real distribution)"), + TableBlock { + header: row(cells: [ + cell(text: ""), + cell(text: "flag-ANY"), + cell(text: "flag-DIVERGENT"), + ]), + alignments: [AlignNone, AlignNone, AlignNone], + rows: [ + row(cells: [ + cell(text: "Catches the A1 class (divergent shadow)"), + cell(text: "yes"), + cell(text: "yes"), + ]), + row(cells: [ + cell(text: "Catches a *future* mirror that later drifts"), + cell(text: "yes (at fork time)"), + cell(text: "no (only after drift, when a closure re-imports both)"), + ]), + row(cells: [ + cell(text: "De-fork scope it demands"), + cell(text: "**all** same-name pairs resolved: divergent → rename-apart, mirror → **merge to one authority**"), + cell(text: "only divergent pairs resolved; mirrors may stay"), + ]), + row(cells: [ + cell(text: "False-positive risk"), + cell(text: "a legitimately-duplicated mirror that *cannot* be merged yet would block until merged"), + cell(text: "a divergent pair that *looks* similar but isn't structurally-equal still correctly fires"), + ]), + row(cells: [ + cell(text: "§3 fidelity"), + cell(text: "full (one name ⇒ one authority, tree-wide)"), + cell(text: "partial (tolerates two authorities iff currently identical)"), + ]), + ], + }, + h3(text: "RULED — `flag-ANY` (parent bright-stag, signed 2026-06-23)"), + p(text: "**`require_structural_divergence = FALSE`.** Settled against the measured distribution (the executed per-basename audit in `docs/plans/dsl-v2-defork-audit.md` §2A — `structural_inequality` run over all 9 std basename pairs + a 351-entry floor-closure reachability BFS). The audit confirmed the cant-unify-yet set (basenames needing a milestone *later than* the grounding de-fork) is **\{node, coercion\} exactly** — no third stuck mirror — so flag-ANY does not block on an un-unifiable pair."), + p(text: "Two consequences parent reconfirmed:"), + ul(items: [ + li(text: "**flag-ANY FIRES on byte-identical mirror shared type-names too** (the audit's 3 in `algebra`, 3 in `integer`, 1 in `float`), not only on differing ones. This is **intended**: a byte-identical mirror is still *two homes for one type* = the §3 single-authority violation and a writable re-fork surface. So the de-fork must **merge even the mirrors** (delete the v2 copy, repoint imports), and flag-ANY is exactly what forces that. flag-DIVERGENT would *tolerate* the byte-mirrors — a standing §3 hole — so it is strictly worse here (it also still fires on every grounding, sparing nothing). Mirrors are therefore **resolved by the de-fork, not exempted**."), + li(text: "**The exemption roster carries NO `\{node, coercion\}` entry — DROPPED as vacuous.** node and coercion (and `logic`, and post-#5640 `verification`) share **zero** type names — only the *basename* — so the type-name guard **never fires** on them. A roster entry for a collision the mechanism cannot produce is a §5 inert scaffold (a dead line). Their collision is a module-**basename** rename on the Route-C / v1-delete surface — a *different* mechanism, still tracked (audit category-(c), `dissolve-on = v1-delete`), not by this guard. The guard's roster is therefore **deliberately empty** — recorded here so its emptiness reads as a decision, not an omission. (See §6.)"), + ]), + hr(), + h2(text: "4. ACTIVATION / DORMANCY (parent's Q3): **lands-already-green** (preferred)"), + p(text: "Two options:"), + ul(items: [ + li(text: "**Staged-enable** (guard lands dormant, flips fail-closed later): carries **dormant-guard state** — a loaded mechanism left unwired. DESIGN §5/§6 names this an anti-pattern: an inert guard is \"coverage by illusion\", a latent lie until the flip, and adds a flip-event to sequence and a window where the guard exists but does not gate."), + li(text: "**Lands-already-green** (preferred): the de-fork lane first removes **every** collision the chosen policy flags from the tree; *then* the guard lands **already fail-closed and green**. No dormant state, no flip event. The guard's own green landing is **self-certifying**: it is green only if zero flagged collisions remain, so merging it *proves* the tree is collision-free under the policy. This is the §5 \"wall lands live or not at all\"."), + ]), + p(text: "Sequencing (hard dependency, RULED): **the grounding de-fork of the shared-type-name set `\{algebra, nat, effects, float, integer\}` → guard lands flag-ANY, fail-closed, green, in one PR.** Each of those five is merged to a single authority (delete the v2 copy / repoint, or the operator grounding-unification design where the bodies diverge) — mirrors included (§3). The set is fronted by the **LIVE pair `\{algebra (75 floor entries), nat (4)\}`** (their `std.` / `v2.std.` co-occur in real floor closures today and silently fail-open — benign only because they shadow record-with-record, not the coproduct-variant-drop that broke `verification` under A1) and completed by the **latent `\{effects, float, integer\}`** (no co-occurring closure today, but re-arm risks — exactly how `verification` went latent→LIVE under A1's closure expansion). `verification` already cleared (#5640); `\{node, coercion, logic\}` are off this surface (zero shared type-names)."), + p(text: "The guard PR is mergeable iff the full floor corpus resolves clean **with the guard active** — which holds iff that five-basename de-fork is complete. Its green landing therefore **self-certifies** the shared-type-name surface is collision-free: the wall is the **capstone** of the de-fork lane, correctly located. No dormant-guard state, no flip event — lands-already-green."), + hr(), + h2(text: "5. Proof plan (model-only; how it is proven by execution when authored)"), + p(text: "Per DESIGN §5 (\"done\" = a real consumer green by execution + a discriminating input that goes red when the behavior is wrong):"), + ul(items: [ + li(text: "**GREEN-by-execution:** with the de-fork complete, run the exact floor closure (`claim_executor --source-root dsl --source-root src/v2`, both orders) — full corpus resolves clean **with the guard active**. (Baseline receipt already in hand from #1: post-rename, `affected_set_floor_runner_test` PASSes both orders, 56 modules.)"), + li(text: "**Discriminating RED (the falsifier):** re-introduce a single synthetic same-name pair into a test's closure and assert the guard emits `TypeNameCollision` and fails closed — and that *removing* it returns green. Run it **twice** to pin the flag-ANY semantics: once with a **divergent** pair (different bodies) and once with a **byte-identical mirror** pair — *both* must fire (flag-ANY excuses neither). A flag-DIVERGENT build would let the mirror through; that it does **not** is the §3-fidelity control."), + li(text: "**No-regression control:** a type legitimately re-exported through multiple import paths (one declaring file, many hops) must stay green — proves `same_authority` (span.file identity) correctly excuses re-exports and the wall is not over-broad."), + ]), + hr(), + h2(text: "6. Scope guard / what this is NOT"), + ul(items: [ + li(text: "**No resolver edit lands** here — model only until checkpoint-sign + de-fork clean."), + li(text: "Does **not** touch the dsl↔v2 std module-**basename** reorganization (Route C / v1-delete) — orthogonal, operator-strategic. The wall keys on shared **type-name** identity within a closure, so the zero-shared-type-name basenames `\{node, coercion, logic, verification\}` are off its surface entirely (this is why the roster carries no `\{node, coercion\}` entry, §3). Their basename de-fork stays tracked in the audit's category-(c) (`dissolve-on = v1-delete`), a different mechanism. The wall is compatible with whatever Route C decides."), + li(text: "Mirrors the existing `VariantCollision` precedent; introduces no new resolver concept beyond lifting that guard one level and dissolving the duplicate import-binding folds into one checked-merge helper (a §2 win bundled in)."), + ]), + h2(text: "7. Open items"), + ul(items: [ + li(text: "**RESOLVED** — Q2 policy: `flag-ANY` signed (§3); per-basename audit executed and homed in `docs/plans/dsl-v2-defork-audit.md` §2A; activation gate set to the five-basename grounding de-fork (§4). Roster: deliberately empty (§3)."), + li(text: "Carried to the future resolver PR (not this model): confirm both import-binding assembly sites (~11761, ~12355) are the only type-binding merge loci (the `std.types`-special-cased branch folds key-by-key already and is naturally covered by the same checked-merge helper)."), + li(text: "Dependency owned elsewhere: the five-basename grounding de-fork (`algebra` authority ruled; `nat`/`integer`/`float` via #5428 numeric tower; `effects` axis decision) must complete before the guard PR can land green. `\{node, coercion\}` basename de-fork stays on the Route-C / v1-delete surface (audit category-(c)), unaffected by this guard."), + ]), + ] +} + +data resolver_type_name_collision_wall_plan: Plan = Plan { + slug: "resolver-type-name-collision-wall", + title: "Resolver type-name-collision wall (§5 construction wall) — model-before-implement", + body: resolver_type_name_collision_wall_body(), + dissolution: HasTrigger { + text: "Delete this model-only DESIGN doc once the resolver type-name-collision wall is implemented and merged — the flag-ANY guard fires fail-closed on any same-name cross-authority type pair (TypeNameCollision diagnostic), the floor closure lands already-green after the de-fork, and the discriminating RED witness (synthetic divergent + byte-identical-mirror pairs both fire) is proven by execution — so this model is realized in the resolver." + } +} diff --git a/src/v2/compiler/manual/typescript_bind_let_iife_emit_test.dag b/src/v2/compiler/manual/typescript_bind_let_iife_emit_test.dag new file mode 100644 index 00000000000..99716ce1c33 --- /dev/null +++ b/src/v2/compiler/manual/typescript_bind_let_iife_emit_test.dag @@ -0,0 +1,168 @@ +module v2.test.manual.typescript_bind_let_iife_emit + +import v2.std.host_transport { target_emit_host_runtime_row_unconfigured } +import v2.std.diagnostic { Accepted, Outcome, Rejected, bind_outcome } +import v2.std.collection { Map, empty_map, map_insert } +import v2.std.node { Symbol } +import v2.std.compilers.target_model { + ValueProducing, + TargetModel, + TargetValueExpression, + TargetValueExpressionProjection, + target_value_expression_binding_ref, + target_value_expression_bind_let, + target_value_expression_loop, + target_value_expression_closure, + target_value_expression_to_concrete_tokens, + target_model_emit_transforms_empty +} +import extdeps.communication.medium { Medium } +import v2.compiler.translate { serialize_concrete_syntax_tokens_to_source } +import v2.extdeps.languages.typescript { + ts_mvp1_target_model_node, + ts_operator_realizations_catalog_node, + ts_value_expression_projection, + ts_value_expression_projection_with_block_evaluation_mode, + ts_wave2a_lex +} +import v2.extdeps.languages.dag { + dag_value_expression_projection, + dag_operator_realizations_catalog_node +} +import v2.std.logic { Bool } + +fn bind_let_binding_spellings() -> Map { + map_insert( + map_insert( + map_insert(empty_map(), ^bind_let_binding_k, "k"), + ^bind_let_binding_v, + "v" + ), + ^bind_let_binding_b, + "b" + ) +} + +fn bind_let_target_model() -> TargetModel { + TargetModel { + bundle: ts_mvp1_target_model_node(), + lex: ts_wave2a_lex(), + binding_spellings: bind_let_binding_spellings(), + token_class_emit_transforms: target_model_emit_transforms_empty, + authority_source_text: "", + runtime_row: target_emit_host_runtime_row_unconfigured + } +} + +fn ts_bind_let_expr() -> TargetValueExpression { + target_value_expression_bind_let( + bind_key: target_value_expression_binding_ref(binding: ^bind_let_binding_k), + bind_value: target_value_expression_binding_ref(binding: ^bind_let_binding_v), + bind_body: target_value_expression_binding_ref(binding: ^bind_let_binding_b) + ) +} + +fn ts_bind_let_emit_with_projection( + projection: TargetValueExpressionProjection +) -> Outcome> { + bind_outcome( + o: target_value_expression_to_concrete_tokens( + expr: ts_bind_let_expr(), + projection: projection, + catalog: ts_operator_realizations_catalog_node() + ), + f: fn(tokens) { + serialize_concrete_syntax_tokens_to_source( + target: bind_let_target_model(), + tokens: tokens + ) + } + ) +} + +fn ts_bind_let_emit_statement_sequenced() -> String { + match ts_bind_let_emit_with_projection( + projection: ts_value_expression_projection() + ) { + Accepted { value: source, diagnostics: _ } => source.carried + Rejected { diagnostics: _ } => "BIND_LET_EMIT_REJECTED" + } +} + +fn ts_bind_let_emit_value_producing() -> String { + match ts_bind_let_emit_with_projection( + projection: ts_value_expression_projection_with_block_evaluation_mode( + block_evaluation_mode: ValueProducing + ) + ) { + Accepted { value: source, diagnostics: _ } => source.carried + Rejected { diagnostics: _ } => "BIND_LET_EMIT_REJECTED" + } +} + +test fn ts_bind_let_iife_emit_exact_holds() -> Bool { + ts_bind_let_emit_statement_sequenced() == "(function () { let k =v;return b; })()" +} + +test fn ts_bind_let_mode_perturbation_flips_holds() -> Bool { + (ts_bind_let_emit_statement_sequenced() == "(function () { let k =v;return b; })()") + && (ts_bind_let_emit_statement_sequenced() != ts_bind_let_emit_value_producing()) + && (ts_bind_let_emit_statement_sequenced() != "BIND_LET_EMIT_REJECTED") +} + +fn block_construct_loop_expr() -> TargetValueExpression { + target_value_expression_loop( + body: target_value_expression_binding_ref(binding: ^bind_let_binding_b) + ) +} + +test fn ts_loop_statement_sequenced_fails_closed_holds() -> Bool { + match target_value_expression_to_concrete_tokens( + expr: block_construct_loop_expr(), + projection: ts_value_expression_projection(), + catalog: ts_operator_realizations_catalog_node() + ) { + Accepted { value: _, diagnostics: _ } => false + Rejected { diagnostics: _ } => true + } +} + +test fn dag_loop_value_producing_emits_holds() -> Bool { + match target_value_expression_to_concrete_tokens( + expr: block_construct_loop_expr(), + projection: dag_value_expression_projection(), + catalog: dag_operator_realizations_catalog_node() + ) { + Accepted { value: _, diagnostics: _ } => true + Rejected { diagnostics: _ } => false + } +} + +fn block_construct_closure_expr() -> TargetValueExpression { + target_value_expression_closure( + params: [^bind_let_binding_k], + body: target_value_expression_binding_ref(binding: ^bind_let_binding_b) + ) +} + +test fn ts_closure_statement_sequenced_fails_closed_holds() -> Bool { + match target_value_expression_to_concrete_tokens( + expr: block_construct_closure_expr(), + projection: ts_value_expression_projection(), + catalog: ts_operator_realizations_catalog_node() + ) { + Accepted { value: _, diagnostics: _ } => false + Rejected { diagnostics: _ } => true + } +} + +test fn dag_closure_value_producing_emits_holds() -> Bool { + match target_value_expression_to_concrete_tokens( + expr: block_construct_closure_expr(), + projection: dag_value_expression_projection(), + catalog: dag_operator_realizations_catalog_node() + ) { + Accepted { value: _, diagnostics: _ } => true + Rejected { diagnostics: _ } => false + } +} diff --git a/src/v2/extdeps/languages/dag.dag b/src/v2/extdeps/languages/dag.dag index 846d2e64d21..824abd98d1b 100644 --- a/src/v2/extdeps/languages/dag.dag +++ b/src/v2/extdeps/languages/dag.dag @@ -120,7 +120,10 @@ import v2.std.compilers.target_model { grammar_relation_row_attach_bodied_scaffold, target_operator_realizations_catalog_node, value_expr_projection_bundle_node, target_model_emit_transforms_empty, - Prepend} + Prepend, + BlockEvaluationMode, + ValueProducing, + derive_bodied_arrow_scaffold} import v2.std.logic { Bool } import v2.std.algebra { Cons, Empty, fold_list, for_all, list_append, list_snoc_item } import v2.std.diagnostic { @@ -4952,10 +4955,15 @@ fn dag_value_expression_projection() -> TargetValueExpressionProjection { close: ^dag_token_rbrace, fat_arrow: ^dag_token_fat_arrow, arm_separator: ^dag_token_comma - } + }, + block_evaluation_mode: dag_block_evaluation_mode() } } +fn dag_block_evaluation_mode() -> BlockEvaluationMode { + ValueProducing +} + fn dag_operator_realizations_catalog_node() -> Node { target_operator_realizations_catalog_node(rows: []) } @@ -4977,10 +4985,11 @@ fn dag_mvp1_pick_statement_suffix_tokens() -> List { } fn dag_mvp1_pick_bodied_arrow_statement_scaffold() -> TargetBodiedArrowStatementScaffold { - TargetBodiedArrowStatementScaffold { - prefix: dag_mvp1_pick_statement_prefix_tokens(), - suffix: dag_mvp1_pick_statement_suffix_tokens() - } + derive_bodied_arrow_scaffold( + signature_with_open: dag_mvp1_pick_statement_prefix_tokens(), + block_close: dag_mvp1_pick_statement_suffix_tokens(), + mode: dag_block_evaluation_mode() + ) } fn dag_mvp1_pick_grammar_relation_row_node() -> Node { @@ -5119,10 +5128,11 @@ fn dag_mvp1_bind_statement_prefix_tokens() -> List { } fn dag_mvp1_bind_bodied_arrow_statement_scaffold() -> TargetBodiedArrowStatementScaffold { - TargetBodiedArrowStatementScaffold { - prefix: dag_mvp1_bind_statement_prefix_tokens(), - suffix: dag_mvp1_pick_statement_suffix_tokens() - } + derive_bodied_arrow_scaffold( + signature_with_open: dag_mvp1_bind_statement_prefix_tokens(), + block_close: dag_mvp1_pick_statement_suffix_tokens(), + mode: dag_block_evaluation_mode() + ) } fn dag_mvp1_bind_grammar_relation_row_node() -> Node { @@ -5261,10 +5271,11 @@ fn dag_mvp1_loop_statement_prefix_tokens() -> List { } fn dag_mvp1_loop_bodied_arrow_statement_scaffold() -> TargetBodiedArrowStatementScaffold { - TargetBodiedArrowStatementScaffold { - prefix: dag_mvp1_loop_statement_prefix_tokens(), - suffix: dag_mvp1_pick_statement_suffix_tokens() - } + derive_bodied_arrow_scaffold( + signature_with_open: dag_mvp1_loop_statement_prefix_tokens(), + block_close: dag_mvp1_pick_statement_suffix_tokens(), + mode: dag_block_evaluation_mode() + ) } fn dag_mvp1_loop_grammar_relation_row_node() -> Node { @@ -5525,10 +5536,11 @@ fn dag_mvp1_rec_statement_prefix_tokens() -> List { } fn dag_mvp1_rec_bodied_arrow_statement_scaffold() -> TargetBodiedArrowStatementScaffold { - TargetBodiedArrowStatementScaffold { - prefix: dag_mvp1_rec_statement_prefix_tokens(), - suffix: dag_mvp1_pick_statement_suffix_tokens() - } + derive_bodied_arrow_scaffold( + signature_with_open: dag_mvp1_rec_statement_prefix_tokens(), + block_close: dag_mvp1_pick_statement_suffix_tokens(), + mode: dag_block_evaluation_mode() + ) } fn dag_mvp1_rec_grammar_relation_row_node() -> Node { @@ -5669,10 +5681,11 @@ fn dag_mvp1_field_access_statement_prefix_tokens() -> List } fn dag_mvp1_field_access_bodied_arrow_statement_scaffold() -> TargetBodiedArrowStatementScaffold { - TargetBodiedArrowStatementScaffold { - prefix: dag_mvp1_field_access_statement_prefix_tokens(), - suffix: dag_mvp1_pick_statement_suffix_tokens() - } + derive_bodied_arrow_scaffold( + signature_with_open: dag_mvp1_field_access_statement_prefix_tokens(), + block_close: dag_mvp1_pick_statement_suffix_tokens(), + mode: dag_block_evaluation_mode() + ) } fn dag_mvp1_field_access_grammar_relation_row_node() -> Node { diff --git a/src/v2/extdeps/languages/typescript.dag b/src/v2/extdeps/languages/typescript.dag index 5c570b2b6db..bf91167e65c 100644 --- a/src/v2/extdeps/languages/typescript.dag +++ b/src/v2/extdeps/languages/typescript.dag @@ -145,7 +145,11 @@ import v2.std.compilers.target_model { value_expr_projection_bundle_node, RecordLiteralTypeNaming, Omit, - Prepend + Prepend, + BlockEvaluationMode, + ValueProducing, + StatementSequenced, + derive_bodied_arrow_scaffold } import v2.std.node { Arrow, @@ -536,13 +540,33 @@ fn ts_mvp1_emitted_add_fn_with_body_node() -> Node { } fn ts_value_expression_projection() -> TargetValueExpressionProjection { - ts_value_expression_projection_with_record_literal_naming( - record_literal_names_type: Omit + ts_value_expression_projection_full( + record_literal_names_type: Omit, + block_evaluation_mode: ts_block_evaluation_mode() ) } fn ts_value_expression_projection_with_record_literal_naming( record_literal_names_type: RecordLiteralTypeNaming +) -> TargetValueExpressionProjection { + ts_value_expression_projection_full( + record_literal_names_type: record_literal_names_type, + block_evaluation_mode: ts_block_evaluation_mode() + ) +} + +fn ts_value_expression_projection_with_block_evaluation_mode( + block_evaluation_mode: BlockEvaluationMode +) -> TargetValueExpressionProjection { + ts_value_expression_projection_full( + record_literal_names_type: Omit, + block_evaluation_mode: block_evaluation_mode + ) +} + +fn ts_value_expression_projection_full( + record_literal_names_type: RecordLiteralTypeNaming, + block_evaluation_mode: BlockEvaluationMode ) -> TargetValueExpressionProjection { TargetValueExpressionProjection { binding_ref_form: TargetBindingRefShape { ident_token: ^ts_token_ident }, @@ -559,13 +583,13 @@ fn ts_value_expression_projection_with_record_literal_naming( }, closure_form: TargetClosureShape { - fn_token: ^ts_closure_emit_unsupported, - open: ^ts_closure_emit_unsupported, - separator: ^ts_closure_emit_unsupported, - close: ^ts_closure_emit_unsupported, - body_open: ^ts_closure_emit_unsupported, - body_close: ^ts_closure_emit_unsupported, - param_ident_token: ^ts_closure_emit_unsupported + fn_token: ^ts_token_kw_function, + open: ^ts_token_lparen, + separator: ^ts_token_comma, + close: ^ts_token_rparen, + body_open: ^ts_token_lbrace, + body_close: ^ts_token_rbrace, + param_ident_token: ^ts_token_ident }, effect_apply_form: TargetEffectApplyShape { @@ -615,7 +639,8 @@ fn ts_value_expression_projection_with_record_literal_naming( close: ^ts_token_rbrace, fat_arrow: ^ts_token_fat_arrow, arm_separator: ^ts_token_comma - } + }, + block_evaluation_mode: block_evaluation_mode } } @@ -630,7 +655,14 @@ fn ts_operator_realizations_catalog_node() -> Node { target_operator_realizations_catalog_node(rows: [ts_add_operator_realization_row()]) } -fn ts_mvp1_fn_add_statement_prefix_tokens() -> List { +fn ts_block_evaluation_mode() -> BlockEvaluationMode { + StatementSequenced { + return_token: ^ts_token_kw_return, + statement_terminator: ^ts_token_semicolon + } +} + +fn ts_add_signature_with_open() -> List { [ FixedToken { token_class: ^ts_token_kw_function }, BoundToken { token_class: ^ts_token_ident, binding: ^ts_binding_fn_add }, @@ -645,23 +677,32 @@ fn ts_mvp1_fn_add_statement_prefix_tokens() -> List { FixedToken { token_class: ^ts_token_rparen }, FixedToken { token_class: ^ts_token_colon }, FixedToken { token_class: ^ts_token_ty_number }, - FixedToken { token_class: ^ts_token_lbrace }, - FixedToken { token_class: ^ts_token_kw_return } + FixedToken { token_class: ^ts_token_lbrace } ] } -fn ts_mvp1_fn_add_statement_suffix_tokens() -> List { +fn ts_add_block_close() -> List { [ - FixedToken { token_class: ^ts_token_semicolon }, FixedToken { token_class: ^ts_token_rbrace } ] } fn ts_mvp1_bodied_arrow_statement_scaffold() -> TargetBodiedArrowStatementScaffold { - TargetBodiedArrowStatementScaffold { - prefix: ts_mvp1_fn_add_statement_prefix_tokens(), - suffix: ts_mvp1_fn_add_statement_suffix_tokens() - } + derive_bodied_arrow_scaffold( + signature_with_open: ts_add_signature_with_open(), + block_close: ts_add_block_close(), + mode: ts_block_evaluation_mode() + ) +} + +fn ts_mvp1_fn_add_statement_prefix_tokens() -> List { + let scaffold = ts_mvp1_bodied_arrow_statement_scaffold() + scaffold.prefix +} + +fn ts_mvp1_fn_add_statement_suffix_tokens() -> List { + let scaffold = ts_mvp1_bodied_arrow_statement_scaffold() + scaffold.suffix } fn ts_mvp1_compose_add_fn_tokens(body_tokens: List) -> List { diff --git a/src/v2/std/compilers/target_model.dag b/src/v2/std/compilers/target_model.dag index df83e5dbf0b..5bb0e5797a7 100644 --- a/src/v2/std/compilers/target_model.dag +++ b/src/v2/std/compilers/target_model.dag @@ -710,6 +710,13 @@ type TargetLoopShape { loop_token: Symbol } +type BlockEvaluationMode + = ValueProducing + | StatementSequenced { + return_token: Symbol + statement_terminator: Symbol + } + type RecordLiteralTypeNaming = Prepend | Omit @@ -746,6 +753,7 @@ type TargetValueExpressionProjection { record_construct_form: TargetRecordConstructShape field_access_form: TargetFieldAccessShape match_form: TargetMatchShape + block_evaluation_mode: BlockEvaluationMode } type TargetBodiedArrowStatementScaffold { @@ -753,6 +761,34 @@ type TargetBodiedArrowStatementScaffold { suffix: List } +fn derive_bodied_arrow_scaffold( + signature_with_open: List, + block_close: List, + mode: BlockEvaluationMode +) -> TargetBodiedArrowStatementScaffold { + match mode { + ValueProducing => + TargetBodiedArrowStatementScaffold { + prefix: signature_with_open, + suffix: block_close + } + StatementSequenced { + return_token: return_token, + statement_terminator: statement_terminator + } => + TargetBodiedArrowStatementScaffold { + prefix: list_snoc_item( + xs: signature_with_open, + item: FixedToken { token_class: return_token } + ), + suffix: list_append( + left: [FixedToken { token_class: statement_terminator }], + right: block_close + ) + } + } +} + fn target_model_type_atom_node(identity: Symbol) -> Node { Node { kind: TypeNode { connective: Atom { identity: identity } }, @@ -1535,6 +1571,87 @@ fn record_literal_type_naming_from_symbol(symbol: Symbol) -> Outcome Node { + match mode { + ValueProducing => + target_model_type_conj_node( + children: [ + target_model_named_edge( + name: ^target_value_expr_field_block_eval_kind, + target: target_model_type_atom_node( + identity: ^block_evaluation_mode_value_producing + ) + ) + ] + ) + StatementSequenced { + return_token: return_token, + statement_terminator: statement_terminator + } => + target_model_type_conj_node( + children: [ + target_model_named_edge( + name: ^target_value_expr_field_block_eval_kind, + target: target_model_type_atom_node( + identity: ^block_evaluation_mode_statement_sequenced + ) + ), + target_model_named_edge( + name: ^target_value_expr_field_block_eval_return_token, + target: target_model_type_atom_node(identity: return_token) + ), + target_model_named_edge( + name: ^target_value_expr_field_block_eval_terminator, + target: target_model_type_atom_node(identity: statement_terminator) + ) + ] + ) + } +} + +fn decode_block_evaluation_mode(bundle: Node) -> Outcome { + bind_outcome( + o: projection_bundle_symbol_field( + bundle: bundle, + field: ^target_value_expr_field_block_eval_kind + ), + f: fn(kind) { + if kind == ^block_evaluation_mode_value_producing { + outcome_accepted(ValueProducing) + } else if kind == ^block_evaluation_mode_statement_sequenced { + bind_outcome( + o: projection_bundle_symbol_field( + bundle: bundle, + field: ^target_value_expr_field_block_eval_return_token + ), + f: fn(return_token) { + bind_outcome( + o: projection_bundle_symbol_field( + bundle: bundle, + field: ^target_value_expr_field_block_eval_terminator + ), + f: fn(statement_terminator) { + outcome_accepted( + StatementSequenced { + return_token: return_token, + statement_terminator: statement_terminator + } + ) + } + ) + } + ) + } else { + outcome_rejected( + target_value_expr_operand_wire_malformed_diagnostic( + wire: bundle + ) + ) + } + } + ) +} + fn decode_record_construct_shape_bundle(bundle: Node) -> Outcome { bind_outcome( o: projection_bundle_symbol_field(bundle: bundle, field: ^target_value_expr_field_record_open), @@ -1924,6 +2041,48 @@ fn decode_vep_chain_match( bind_outcome( o: decode_vep_parent_match(bundle: bundle), f: fn(match_form) { + decode_vep_chain_block_eval( + bundle: bundle, + binding_ref_form: binding_ref_form, + primitive_apply_form: primitive_apply_form, + callable_apply_form: callable_apply_form, + closure_form: closure_form, + effect_apply_form: effect_apply_form, + conditional_form: conditional_form, + let_form: let_form, + loop_form: loop_form, + record_construct_form: record_construct_form, + field_access_form: field_access_form, + match_form: match_form + ) + } + ) +} + +fn decode_vep_parent_block_eval(bundle: Node) -> Outcome { + bind_outcome( + o: projection_bundle_child(bundle: bundle, name: ^target_value_expr_field_block_eval), + f: decode_block_evaluation_mode + ) +} + +fn decode_vep_chain_block_eval( + bundle: Node, + binding_ref_form: TargetBindingRefShape, + primitive_apply_form: TargetPrimitiveApplyShape, + callable_apply_form: TargetCallApplyShape, + closure_form: TargetClosureShape, + effect_apply_form: TargetEffectApplyShape, + conditional_form: TargetConditionalShape, + let_form: TargetBindLetShape, + loop_form: TargetLoopShape, + record_construct_form: TargetRecordConstructShape, + field_access_form: TargetFieldAccessShape, + match_form: TargetMatchShape +) -> Outcome { + bind_outcome( + o: decode_vep_parent_block_eval(bundle: bundle), + f: fn(block_evaluation_mode) { outcome_accepted( TargetValueExpressionProjection { binding_ref_form: binding_ref_form, @@ -1936,7 +2095,8 @@ fn decode_vep_chain_match( loop_form: loop_form, record_construct_form: record_construct_form, field_access_form: field_access_form, - match_form: match_form + match_form: match_form, + block_evaluation_mode: block_evaluation_mode } ) } @@ -4527,6 +4687,83 @@ fn target_value_expr_bind_let_child_from_wire( target_value_expr_conditional_child_from_wire(wire: wire, field: field) } +fn bind_let_value_producing_tokens( + projection: TargetValueExpressionProjection, + key_tokens: List, + value_tokens: List, + body_tokens: List +) -> List { + list_append( + left: list_append( + left: list_append( + left: list_append( + left: list_append( + left: [ + FixedToken { token_class: projection.let_form.let_token } + ], + right: key_tokens + ), + right: [ + FixedToken { token_class: projection.let_form.assign_token } + ] + ), + right: value_tokens + ), + right: [ + FixedToken { token_class: projection.let_form.in_token } + ] + ), + right: body_tokens + ) +} + +fn bind_let_statement_sequenced_tokens( + projection: TargetValueExpressionProjection, + key_tokens: List, + value_tokens: List, + body_tokens: List, + return_token: Symbol, + statement_terminator: Symbol +) -> List { + list_append( + left: list_append( + left: list_append( + left: list_append( + left: list_append( + left: list_append( + left: [ + FixedToken { token_class: projection.primitive_apply_form.open }, + FixedToken { token_class: projection.closure_form.fn_token }, + FixedToken { token_class: projection.closure_form.open }, + FixedToken { token_class: projection.closure_form.close }, + FixedToken { token_class: projection.closure_form.body_open }, + FixedToken { token_class: projection.let_form.let_token } + ], + right: key_tokens + ), + right: [ + FixedToken { token_class: projection.let_form.assign_token } + ] + ), + right: value_tokens + ), + right: [ + FixedToken { token_class: statement_terminator }, + FixedToken { token_class: return_token } + ] + ), + right: body_tokens + ), + right: [ + FixedToken { token_class: statement_terminator }, + FixedToken { token_class: projection.closure_form.body_close }, + FixedToken { token_class: projection.primitive_apply_form.close }, + FixedToken { token_class: projection.primitive_apply_form.open }, + FixedToken { token_class: projection.primitive_apply_form.close } + ] + ) +} + fn target_value_expression_bind_let_to_concrete_tokens( expr: TargetValueExpression, projection: TargetValueExpressionProjection, @@ -4574,39 +4811,31 @@ fn target_value_expression_bind_let_to_concrete_tokens( catalog: catalog ), f: fn(body_tokens) { - outcome_accepted( - list_append( - left: list_append( - left: list_append( - left: list_append( - left: list_append( - left: Cons { - head: FixedToken { - token_class: projection.let_form.let_token - }, - tail: Empty - }, - right: key_tokens - ), - right: Cons { - head: FixedToken { - token_class: projection.let_form.assign_token - }, - tail: Empty - } - ), - right: value_tokens - ), - right: Cons { - head: FixedToken { - token_class: projection.let_form.in_token - }, - tail: Empty - } - ), - right: body_tokens - ) - ) + match projection.block_evaluation_mode { + ValueProducing => + outcome_accepted( + bind_let_value_producing_tokens( + projection: projection, + key_tokens: key_tokens, + value_tokens: value_tokens, + body_tokens: body_tokens + ) + ) + StatementSequenced { + return_token: return_token, + statement_terminator: statement_terminator + } => + outcome_accepted( + bind_let_statement_sequenced_tokens( + projection: projection, + key_tokens: key_tokens, + value_tokens: value_tokens, + body_tokens: body_tokens, + return_token: return_token, + statement_terminator: statement_terminator + ) + ) + } } ) } @@ -4654,10 +4883,54 @@ fn target_value_expr_loop_child_from_wire(wire: Node) -> Outcome Diagnostic { + Diagnostic { + reason: ^statement_sequenced_block_construct_unwired, + at: node_locus(node: wire), + correction: Unavailable { reason: ExternalContractUnknown } + } +} + +fn statement_sequenced_block_construct_guard( + block_evaluation_mode: BlockEvaluationMode, + wire: Node +) -> Outcome { + match block_evaluation_mode { + ValueProducing => outcome_accepted(true) + StatementSequenced { + return_token: _, + statement_terminator: _ + } => + outcome_rejected( + statement_sequenced_block_construct_unwired_diagnostic(wire: wire) + ) + } +} + fn target_value_expression_loop_to_concrete_tokens( expr: TargetValueExpression, projection: TargetValueExpressionProjection, catalog: Node +) -> Outcome> { + bind_outcome( + o: statement_sequenced_block_construct_guard( + block_evaluation_mode: projection.block_evaluation_mode, + wire: expr.node + ), + f: fn(_) { + target_value_expression_loop_to_concrete_tokens_inner( + expr: expr, + projection: projection, + catalog: catalog + ) + } + ) +} + +fn target_value_expression_loop_to_concrete_tokens_inner( + expr: TargetValueExpression, + projection: TargetValueExpressionProjection, + catalog: Node ) -> Outcome> { bind_outcome( o: target_value_expr_loop_wire_schema_valid(wire: expr.node), @@ -5332,6 +5605,26 @@ fn target_value_expression_match_to_concrete_tokens( expr: TargetValueExpression, projection: TargetValueExpressionProjection, catalog: Node +) -> Outcome> { + bind_outcome( + o: statement_sequenced_block_construct_guard( + block_evaluation_mode: projection.block_evaluation_mode, + wire: expr.node + ), + f: fn(_) { + target_value_expression_match_to_concrete_tokens_inner( + expr: expr, + projection: projection, + catalog: catalog + ) + } + ) +} + +fn target_value_expression_match_to_concrete_tokens_inner( + expr: TargetValueExpression, + projection: TargetValueExpressionProjection, + catalog: Node ) -> Outcome> { bind_outcome( o: target_value_expr_match_wire_schema_valid(wire: expr.node), @@ -5745,6 +6038,26 @@ fn target_value_expression_closure_to_concrete_tokens( expr: TargetValueExpression, projection: TargetValueExpressionProjection, catalog: Node +) -> Outcome> { + bind_outcome( + o: statement_sequenced_block_construct_guard( + block_evaluation_mode: projection.block_evaluation_mode, + wire: expr.node + ), + f: fn(_) { + target_value_expression_closure_to_concrete_tokens_inner( + expr: expr, + projection: projection, + catalog: catalog + ) + } + ) +} + +fn target_value_expression_closure_to_concrete_tokens_inner( + expr: TargetValueExpression, + projection: TargetValueExpressionProjection, + catalog: Node ) -> Outcome> { bind_outcome( o: target_value_expr_closure_params_from_wire(wire: expr.node), @@ -6350,6 +6663,12 @@ fn value_expr_projection_bundle_node(projection: TargetValueExpressionProjection ) ] ) + ), + target_model_named_edge( + name: ^target_value_expr_field_block_eval, + target: block_evaluation_mode_to_node( + mode: projection.block_evaluation_mode + ) ) ] )