From f776e83c6a4e25e233b63593f29ba0e1199e8220 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Mon, 29 Jun 2026 17:14:04 +0000 Subject: [PATCH 01/25] Design sketch: floor shared-computation memoization (no implementation) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Documents the root (double-paid full-tree compile: 4× subprocess + 2× in-process resolve_entry_graph), two fix axes (M1 within-walk resolve memo + M2 RunnableCompile artifact node), and the four operator decisions needed before any implementation lands. Co-Authored-By: Claude Sonnet 4.6 --- .../plans/floor-shared-compute-memoization.md | 152 ++++++++++++++++++ 1 file changed, 152 insertions(+) create mode 100644 docs/plans/floor-shared-compute-memoization.md diff --git a/docs/plans/floor-shared-compute-memoization.md b/docs/plans/floor-shared-compute-memoization.md new file mode 100644 index 00000000000..3c458e495b5 --- /dev/null +++ b/docs/plans/floor-shared-compute-memoization.md @@ -0,0 +1,152 @@ +# Floor shared-computation memoization — design sketch + +**Status:** DESIGN SKETCH — no implementation. Returns to stern-moth-225 + operator for approval before any code. + +**Grounded 2026-06-29.** Root measurement: 537s clean-tree compile. Design principle: DESIGN.md §2 (minimize redundancy), §5 (correctness by construction, not validation). + +--- + +## 1. Root — what is actually paid twice (and more) + +The CI floor runs one `claim_executor` process per CI job, executing the plan as a sequence of batches. Within a batch, `SharedClaims` groups already deduplicate: all `RunnableSingleClaim` items sharing one `entry` file resolve that file's closure exactly once. This is correct and already lands. + +The gap is **cross-batch and subprocess**: two independent dimensions of redundant work. + +### Axis A — subprocess `gunbc compile` (the expensive one: ~537s each) + +Three gates independently invoke `gunbc compile --target rust` over the same corpus: + +| Gate | Compiles | +|---|---| +| `DslCompileCleanGate` | 1× `gunbc compile --source-root dsl --source-root src/v2` | +| `EmitDeterminismGate` | 2× `gunbc compile --source-root dsl` in sequence (to diff output trees) | +| `RegenVerifyGate` | 1× via `regen_stage0 --verify` (internally compiles to compare against committed seed) | + +On a clean tree with the same compiler binary: compile-1 and compile-2 (and compile-3 and compile-4) are pure functions of `(source_content, compiler_binary)` and produce byte-identical output. Running the same pure function 4 times is a §2 violation; the 3 extra runs are each ~537s of wasted wall time. + +`EmitDeterminismGate` is particularly telling: it proves determinism by running the SAME compile TWICE and diffing — but if the compile is content-addressed, the proof is already in the hash (same key → same output; re-running is redundant). The gate's intent (verify determinism) can be satisfied by the content-address invariant, not by re-execution. + +### Axis B — in-process `resolve_entry_graph` cross-batch (~30–40s per call) + +`claim_executor`'s `run_walk` runs batches sequentially. The current batch-local `SharedClaims` deduplication does not persist across batch boundaries. The `floor_effect_gate_witness.dag` closure (~106 modules) is resolved in: + +- Batch 1: evaluate `dsl_compile_clean_gate_passes` → 1 call to `resolve_entry_graph` +- Batch 2: evaluate all Group-A gate witnesses → 1 call to `resolve_entry_graph` for the SAME entry + +These are the same `(source_roots, entry)` pair; same pure function; same output. Both calls happen in the same OS process within ~52s of each other. The second pays a full ~30–40s re-resolve for no reason. + +Any future `heavy_whole_tree_resolve` gate added to `floor_effect_gate_witness.dag` will silently add another ~30–40s re-resolve. The behavior is not unwritable — it just happens automatically. + +--- + +## 2. Current model has no shared-output node + +The plan in `std.realization_schedule` represents runnables as independent units. `RunnableSingleClaim` carries `entry`, `function`, and `profile` — but has no concept of a produced artifact that other runnables consume. `DataDependsOn` edges declare ordering (compile gate must pass before corpus runs) but they carry no payload (the resolved graph or compiled artifact). + +This means the executor cannot share the output of one runnable as the input of another. Each runnable independently recomputes from source. The double-payment is not a bug in the executor — it is an honest consequence of a model that has no shared-output primitive. Fixing it by adding a memo to `claim_executor` without changing the model would be a §5 validation standing where construction was available: a future gate added to `floor_effect_gate_witness.dag` would again silently double-pay. + +--- + +## 3. Proposed design — two complementary mechanisms + +### M1 — Within-walk resolve memo (Axis B) + +**Mechanism:** `run_walk` in `claim_executor` maintains a `HashMap<(source_roots_hash, entry), Arc>` across all batch executions. When a `SharedClaims` group resolves its entry, the result is stored. If a later batch resolves the same `(source_roots, entry)`, it gets the `Arc` clone — zero re-parse, zero re-typecheck. + +**Correctness:** Pure function of `(source_roots, entry)` — the source files don't change during a single `run_walk`. The Batch 1 → Batch 2 execution is sequential (no concurrent mutation), so `Arc` is safe with no locking. + +**Memory:** The resolved graph for `floor_effect_gate_witness.dag` is ~0.9 GiB. Since the heavy-resolve chain already serializes these batches (Batch 1 finishes before Batch 2 starts), both batches hold the graph at different times — the memo doesn't increase peak memory, it keeps the Batch 1 graph alive slightly longer. This is acceptable. + +**By-construction property:** Any gate in any entry that `run_walk` has already resolved in this run gets the memo automatically. A future gate added to `floor_effect_gate_witness.dag` cannot accidentally double-pay — the walk owns the resolve decision. + +**Model surface needed (DESIGN.md §5 "model before implement"):** The `RunnableResourceProfile` already carries `heavy_whole_tree_resolve: Bool`. A new field `resolve_scope: ResolveScope` where `ResolveScope = ResolveScopeIsolated | ResolveScopeShared` lets the model explicitly declare which runnables participate in the shared resolve pool. The executor enforces: `ResolveScopeShared` entries may NOT re-resolve; a future runnable without this field defaults to `ResolveScopeIsolated` (safe, fail-closed — it re-resolves rather than silently sharing stale data). The lens verifies that every `heavy_whole_tree_resolve: true` runnable declares `ResolveScopeShared`. + +### M2 — Compile artifact as a first-class plan node (Axis A) + +**Mechanism:** Introduce `RunnableCompile` as a variant of `Runnable` in `std.realization_schedule`: + +``` +type Runnable + = RunnableSingleClaim { ... } -- existing + | RunnableDiscoveryBatch { ... } -- existing + | RunnableCompile { -- NEW + source_roots: List + target: EmitTarget + artifact_id: ContentHash -- the content-address key + profile: RunnableResourceProfile + } +``` + +A `RunnableCompile` is a plan node that: +1. Invokes `gunbc compile --source-root ... --target ...` +2. Content-addresses its output (directory tree hash) +3. Stores the artifact under `artifact_id` in a within-run artifact store +4. Exposes a typed `CompiledArtifact` handle to dependent nodes via `DataDependsOn` + +Dependent nodes change their contract: +- `DslCompileCleanGate` → becomes: verify the `RunnableCompile` node exits 0 (it already IS the compile; the gate just checks success) +- `EmitDeterminismGate` → becomes: verify `artifact.content_hash == artifact.content_hash` — trivially true. The real check is that the `RunnableCompile` is deterministic, which is proved by the content-address invariant (same `(source_content, compiler_binary)` → same hash). **The x2 diff evaporates.** If the operator wants to keep a stronger empirical determinism check (run twice, diff the trees), that becomes a separate `RunnableVerifyDeterminism` that receives two `CompiledArtifact` handles from two `RunnableCompile` nodes with the same `source_roots` — but those two runs now share the SAME in-process resolved graph (M1) and differ only in the output directory. +- `RegenVerifyGate` → becomes: verify that the committed seed bytes match `artifact.content_hash`. Does not re-compile. + +**Compile count:** 4× → 1× (or 2× if the operator wants empirical x2 determinism verification, still down from 4×). + +**By-construction property:** The plan has exactly ONE `RunnableCompile` node per `(source_roots, target)` tuple. The executor raises a typed error if it encounters two `RunnableCompile` nodes with the same key — the plan is malformed, not silently redundant. A future gate that needs the compiled artifact adds a `DataDependsOn` on the existing `RunnableCompile` node; it cannot accidentally introduce a second compile without explicitly creating a second `RunnableCompile` node, which the lens will flag. + +--- + +## 4. Scope — what this is NOT + +**This is NOT the cross-run resolve cache (#4867).** The `resolved_graph_cache.rs` disk cache enables sharing across separate `claim_executor` invocations (separate runs, separate PRs). It is currently dormant in CI (compiler binary changes every commit → cold cache; the JSON I/O buffers multi-GiB into memory). That lane's fix is streaming serialization + a content-key that doesn't include the compiler binary for stable sub-closures. That work is independent and orthogonal. + +**This is NOT a general memoization of all interpreter calls.** `pure_call_memo` and `ParseTable` memo are separate mechanisms with separate key derivations. This design only addresses the floor's cross-batch resolve cost and the subprocess compile cost. + +**This is NOT a change to the CI schedule ordering.** The `DataDependsOn` / `ResourceDependsOn` dependency model stays. `RunnableCompile` becomes a new batch-1 node; all gates that consume its artifact become batch-2 (already the case via `floor_depends_on_compile`). + +--- + +## 5. Operator decisions required before implementation + +**D1 — Where does `ResolveScope` live?** +Option A: Add `resolve_scope: ResolveScope` to `RunnableResourceProfile` in `std.realization_schedule`. Clean: the profile already describes resource semantics. +Option B: Keep it implicit — the executor memos all same-entry resolves with no model surface. Simpler but concedes the bad state is writable (a new gate won't know it's sharing). +**Recommendation: A** (model before implement, §5). + +**D2 — Does M2 land in this PR or a follow-on?** +M1 (within-walk resolve memo) is lower-risk and immediately addressable. M2 (`RunnableCompile`) requires a new substrate type, a new executor code path, and a refactor of three gate transports to consume an artifact handle instead of shelling out. These are independently beneficial. +**Recommendation: M1 first (one PR, small, purely additive); M2 as a follow-on with operator approval of the substrate shape.** + +**D3 — Does `EmitDeterminismGate` survive M2, or does it dissolve?** +If `RunnableCompile` content-addresses its output, determinism is proved by construction (same key → same content). The x2 diff becomes redundant. The gate could be replaced by a `witness_compile_output_is_content_addressed()` Boolean claim. +**Recommendation: Operator decides whether to keep the empirical x2 check as belt-and-suspenders or to accept the construction proof. Either is valid; this design supports both.** + +**D4 — Scope of `RunnableCompile.source_roots`.** +`DslCompileCleanGate` compiles `dsl + src/v2` (the full floor corpus). `EmitDeterminismGate` today compiles only `dsl`. These are different `(source_roots, target)` tuples — two `RunnableCompile` nodes. Is this the intended split, or should both use the same full-corpus compile? (The difference is intentional today because emit_determinism targets only `dsl`.) +**Recommendation: Preserve the existing split; document it explicitly in the plan as two separate `RunnableCompile` nodes with different `source_roots`.** + +--- + +## 6. Displacement analysis + +| Cost today | Cost after M1 | Cost after M1+M2 | +|---|---|---| +| `resolve_entry_graph` × 2 per run (~30–40s each) | × 1 (memo deduplicates Batch 1 → Batch 2) | × 1 | +| `gunbc compile` × 4 per run (~537s each) | × 4 (M1 doesn't help subprocess) | × 1 or × 2 | +| **Total compile cost per run** | ~1074s – ~37s ≈ same subprocess cost, saved resolve | **~537s or ~1074s → 1×** | + +M1 saves ~30–40s per run (the Axis-B double-resolve). Small absolute, but the mechanism is a construction wall. + +M2 saves ~537s × 3 (or × 2 if empirical determinism is kept) — the dominant saving. At ~537s per compile, eliminating 3 extra compiles saves ~26–27 minutes of CI wall time that currently runs sequentially. + +The combined displacement: **~1600s → ~537s for the compile-related floor costs** (eliminating 3 out of 4 compiles plus 1 resolve), roughly a 3× improvement in compile-related CI floor wall time. + +--- + +## 7. Dissolution triggers + +M1 (`ResolveScopeShared` memo): +- Dissolves into M2 (`RunnableCompile`)'s pre-resolve: once the compile node holds the compiled+resolved graph as a typed artifact, the within-walk memo becomes a special case of "artifact produced by Batch-1 consumed by Batch-2" — the general mechanism subsumes it. +- Intermediate milestone: lens verifies all `heavy_whole_tree_resolve: true` runnables carry `ResolveScopeShared`. + +M2 (`RunnableCompile`): +- Dissolves into the v2 scheduler (resource-aware-scheduler.md Node B/C) once the scheduler derives `Runnable.cost` from the compile node's output rather than static measurement rows. +- Dissolves into the Realization pattern (#4867) for cross-run caching once M2's content-addressed artifact is stored on disk between runs. From d2bc7d527541bc8788f0687ea7e1b5eecd7cd3c2 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Mon, 29 Jun 2026 17:17:19 +0000 Subject: [PATCH 02/25] WIP: DESIGN SKETCH ONLY (no code; returns to stern-moth-225 + operator before --- .../plans/floor-shared-compute-memoization.md | 34 +++++++++++-------- 1 file changed, 20 insertions(+), 14 deletions(-) diff --git a/docs/plans/floor-shared-compute-memoization.md b/docs/plans/floor-shared-compute-memoization.md index 3c458e495b5..c1de6350ac9 100644 --- a/docs/plans/floor-shared-compute-memoization.md +++ b/docs/plans/floor-shared-compute-memoization.md @@ -83,12 +83,16 @@ A `RunnableCompile` is a plan node that: 3. Stores the artifact under `artifact_id` in a within-run artifact store 4. Exposes a typed `CompiledArtifact` handle to dependent nodes via `DataDependsOn` -Dependent nodes change their contract: -- `DslCompileCleanGate` → becomes: verify the `RunnableCompile` node exits 0 (it already IS the compile; the gate just checks success) -- `EmitDeterminismGate` → becomes: verify `artifact.content_hash == artifact.content_hash` — trivially true. The real check is that the `RunnableCompile` is deterministic, which is proved by the content-address invariant (same `(source_content, compiler_binary)` → same hash). **The x2 diff evaporates.** If the operator wants to keep a stronger empirical determinism check (run twice, diff the trees), that becomes a separate `RunnableVerifyDeterminism` that receives two `CompiledArtifact` handles from two `RunnableCompile` nodes with the same `source_roots` — but those two runs now share the SAME in-process resolved graph (M1) and differ only in the output directory. -- `RegenVerifyGate` → becomes: verify that the committed seed bytes match `artifact.content_hash`. Does not re-compile. +**CRITICAL DEPENDENCY:** M2 is GATED on emit being deterministic. Today's Rust emitter has known non-determinism (HashMap iteration order in the emit path; `v2.std.determinism` is only at P1 as of 2026-06-29). Content-addressing a non-deterministic compile is unsound: two cold runs produce DIFFERING outputs, so a content-address key would collide on differing artifacts and serve an arbitrary one to consumers — the exact "key went green while the realizer faked the key" §5 fail-open trap. **M2 must not land until the determinism mechanism (#5941, `v2.std.determinism`) closes the non-determinism gap.** Sequence: M1 → determinism mechanism → M2. -**Compile count:** 4× → 1× (or 2× if the operator wants empirical x2 determinism verification, still down from 4×). +**The determinism gate is the ORACLE, not a redundancy.** `EmitDeterminismGate`'s two cold, independent compiles are the empirical oracle for non-reproducible emit. Content-addressing does not prove determinism — it assumes it. Memoizing the pair to one artifact would delete the only live check for a known bug, making the gate inert (§5 coverage-by-illusion). The x2 compiles REMAIN in M2. + +Dependent nodes change their contract under M2: +- `EmitDeterminismGate` → **unchanged**: still runs 2× cold, independent `gunbc compile` and diffs. It is the oracle that LICENSES the artifact as canonical. Both runs benefit from the M1 in-process resolve memo (same source closure, so each resolves once). Net: 2× compile (same as today for this gate), ~30–40s of resolve saved. +- `DslCompileCleanGate` → consumes `EmitDeterminismGate`'s proven-canonical `CompiledArtifact` via `DataDependsOn`. Checks that the compile exits 0. Does NOT re-compile. (Previously: 1× compile. After M2: 0× compile.) +- `RegenVerifyGate` → consumes the same proven-canonical `CompiledArtifact`. Verifies committed seed matches it. Does NOT re-compile. (Previously: 1× compile. After M2: 0× compile.) + +**Compile count:** 4× → 2× (the determinism oracle pair). Saves ~537s × 2 ≈ 18 min. **By-construction property:** The plan has exactly ONE `RunnableCompile` node per `(source_roots, target)` tuple. The executor raises a typed error if it encounters two `RunnableCompile` nodes with the same key — the plan is malformed, not silently redundant. A future gate that needs the compiled artifact adds a `DataDependsOn` on the existing `RunnableCompile` node; it cannot accidentally introduce a second compile without explicitly creating a second `RunnableCompile` node, which the lens will flag. @@ -115,9 +119,9 @@ Option B: Keep it implicit — the executor memos all same-entry resolves with n M1 (within-walk resolve memo) is lower-risk and immediately addressable. M2 (`RunnableCompile`) requires a new substrate type, a new executor code path, and a refactor of three gate transports to consume an artifact handle instead of shelling out. These are independently beneficial. **Recommendation: M1 first (one PR, small, purely additive); M2 as a follow-on with operator approval of the substrate shape.** -**D3 — Does `EmitDeterminismGate` survive M2, or does it dissolve?** -If `RunnableCompile` content-addresses its output, determinism is proved by construction (same key → same content). The x2 diff becomes redundant. The gate could be replaced by a `witness_compile_output_is_content_addressed()` Boolean claim. -**Recommendation: Operator decides whether to keep the empirical x2 check as belt-and-suspenders or to accept the construction proof. Either is valid; this design supports both.** +**D3 — Does `EmitDeterminismGate` survive M2?** +Yes, it survives unchanged as the oracle. Its x2 compiles are not a cost to eliminate — they are the discriminating witness for non-reproducible emit, a known live bug. The gate dissolves only when the determinism mechanism (`v2.std.determinism`, #5941) closes the bug and makes non-determinism unwritable by construction; at that point the two cold compiles become definitionally redundant and the gate can be replaced by a construction-side check. Until then, deleting or memoizing the pair is a §5 coverage-by-illusion. +**Recommendation: keep both compiles; gate M2 on the determinism mechanism landing.** **D4 — Scope of `RunnableCompile.source_roots`.** `DslCompileCleanGate` compiles `dsl + src/v2` (the full floor corpus). `EmitDeterminismGate` today compiles only `dsl`. These are different `(source_roots, target)` tuples — two `RunnableCompile` nodes. Is this the intended split, or should both use the same full-corpus compile? (The difference is intentional today because emit_determinism targets only `dsl`.) @@ -127,17 +131,17 @@ If `RunnableCompile` content-addresses its output, determinism is proved by cons ## 6. Displacement analysis -| Cost today | Cost after M1 | Cost after M1+M2 | +| Cost today | Cost after M1 | Cost after M1+M2 (gated on determinism) | |---|---|---| | `resolve_entry_graph` × 2 per run (~30–40s each) | × 1 (memo deduplicates Batch 1 → Batch 2) | × 1 | -| `gunbc compile` × 4 per run (~537s each) | × 4 (M1 doesn't help subprocess) | × 1 or × 2 | -| **Total compile cost per run** | ~1074s – ~37s ≈ same subprocess cost, saved resolve | **~537s or ~1074s → 1×** | +| `gunbc compile` × 4 per run (~537s each) | × 4 (M1 doesn't help subprocess) | × 2 (determinism oracle pair survives) | +| **Total compile cost per run** | ~2148s – ~37s ≈ same subprocess cost, saved resolve | **~1074s + ~37s → 2× compile, 1× resolve** | -M1 saves ~30–40s per run (the Axis-B double-resolve). Small absolute, but the mechanism is a construction wall. +M1 saves ~30–40s per run (the Axis-B double-resolve). Small absolute, but the mechanism is a construction wall. Unblocked today. -M2 saves ~537s × 3 (or × 2 if empirical determinism is kept) — the dominant saving. At ~537s per compile, eliminating 3 extra compiles saves ~26–27 minutes of CI wall time that currently runs sequentially. +M2 saves ~537s × 2 — the other two compiles (DslCompileCleanGate and RegenVerifyGate) consume the determinism oracle's proven-canonical artifact. That is ~18 minutes of CI wall time removed per run. **Gated on `v2.std.determinism` (#5941) closing the non-determinism gap before content-addressing compile output is sound.** -The combined displacement: **~1600s → ~537s for the compile-related floor costs** (eliminating 3 out of 4 compiles plus 1 resolve), roughly a 3× improvement in compile-related CI floor wall time. +The combined displacement: **~2148s → ~1074s for the compile-related floor costs** (4→2 compiles, 2→1 resolve), roughly a 2× improvement. The remaining 2× (the determinism oracle pair) is load-bearing and dissolves only when emit is provably deterministic. --- @@ -148,5 +152,7 @@ M1 (`ResolveScopeShared` memo): - Intermediate milestone: lens verifies all `heavy_whole_tree_resolve: true` runnables carry `ResolveScopeShared`. M2 (`RunnableCompile`): +- **Gated on**: `v2.std.determinism` (#5941) closing non-reproducible emit. Content-addressing the artifact is unsound until emit is deterministic. Do not land M2 before this gate closes. +- After determinism closes: `EmitDeterminismGate` dissolves from an empirical oracle into a construction-verified witness; the 2× oracle pair becomes 1× (and M2 can collapse further to 1× total compile). - Dissolves into the v2 scheduler (resource-aware-scheduler.md Node B/C) once the scheduler derives `Runnable.cost` from the compile node's output rather than static measurement rows. - Dissolves into the Realization pattern (#4867) for cross-run caching once M2's content-addressed artifact is stored on disk between runs. From e9f8ed13710ee9d64640c0384582555f7c6dc6de Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Mon, 29 Jun 2026 17:18:49 +0000 Subject: [PATCH 03/25] =?UTF-8?q?Fix=20stale=20=C2=A71=20framing=20of=20Em?= =?UTF-8?q?itDeterminismGate=20(oracle,=20not=20redundant)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The original text said the x2 diff was redundant if compile is content-addressed. Corrected: the gate is a load-bearing oracle for known-live non-determinism; content-addressing assumes determinism not proves it. Co-Authored-By: Claude Sonnet 4.6 --- docs/plans/floor-shared-compute-memoization.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/docs/plans/floor-shared-compute-memoization.md b/docs/plans/floor-shared-compute-memoization.md index c1de6350ac9..57fd653d913 100644 --- a/docs/plans/floor-shared-compute-memoization.md +++ b/docs/plans/floor-shared-compute-memoization.md @@ -24,7 +24,7 @@ Three gates independently invoke `gunbc compile --target rust` over the same cor On a clean tree with the same compiler binary: compile-1 and compile-2 (and compile-3 and compile-4) are pure functions of `(source_content, compiler_binary)` and produce byte-identical output. Running the same pure function 4 times is a §2 violation; the 3 extra runs are each ~537s of wasted wall time. -`EmitDeterminismGate` is particularly telling: it proves determinism by running the SAME compile TWICE and diffing — but if the compile is content-addressed, the proof is already in the hash (same key → same output; re-running is redundant). The gate's intent (verify determinism) can be satisfied by the content-address invariant, not by re-execution. +`EmitDeterminismGate` is the empirical oracle for non-reproducible emit: it runs the SAME compile TWICE independently and diffs the output trees. This is load-bearing — emit is KNOWN-NONDETERMINISTIC today (Rust emitter HashMap iteration order; `v2.std.determinism` at P1). Content-addressing does not make this gate redundant; it requires the gate to have already confirmed determinism before a content-address can be trusted. ### Axis B — in-process `resolve_entry_graph` cross-batch (~30–40s per call) From bb3cd31af6485f65098b8d4531bef15b5cf5e822 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Mon, 29 Jun 2026 17:35:26 +0000 Subject: [PATCH 04/25] WIP: DESIGN SKETCH ONLY (no code; returns to stern-moth-225 + operator before --- .../plans/floor-shared-compute-memoization.md | 26 +++++++++++-------- 1 file changed, 15 insertions(+), 11 deletions(-) diff --git a/docs/plans/floor-shared-compute-memoization.md b/docs/plans/floor-shared-compute-memoization.md index 57fd653d913..fc439662d3e 100644 --- a/docs/plans/floor-shared-compute-memoization.md +++ b/docs/plans/floor-shared-compute-memoization.md @@ -12,19 +12,21 @@ The CI floor runs one `claim_executor` process per CI job, executing the plan as The gap is **cross-batch and subprocess**: two independent dimensions of redundant work. -### Axis A — subprocess `gunbc compile` (the expensive one: ~537s each) +### Axis A — subprocess compiles (the expensive ones: ~537s each) -Three gates independently invoke `gunbc compile --target rust` over the same corpus: +Three gates invoke compile-like subprocesses, each with a **distinct (source_roots, binary) tuple**: -| Gate | Compiles | -|---|---| -| `DslCompileCleanGate` | 1× `gunbc compile --source-root dsl --source-root src/v2` | -| `EmitDeterminismGate` | 2× `gunbc compile --source-root dsl` in sequence (to diff output trees) | -| `RegenVerifyGate` | 1× via `regen_stage0 --verify` (internally compiles to compare against committed seed) | +| Gate | Binary | Source roots | Notes | +|---|---|---|---| +| `DslCompileCleanGate` | `gunbc compile` | `dsl src/v2` | `witness_layer_roots` via `dsl_compile_clean_transport.dag` | +| `EmitDeterminismGate` | `gunbc compile` | `dsl` only | `emit_determinism_corpus_roots = ["dsl"]` — intentionally narrower scope | +| `RegenVerifyGate` | `regen_stage0 --verify` | `src/v1 + dsl` (internal) | Different binary; verifies committed v1 seed against a fresh regen | -On a clean tree with the same compiler binary: compile-1 and compile-2 (and compile-3 and compile-4) are pure functions of `(source_content, compiler_binary)` and produce byte-identical output. Running the same pure function 4 times is a §2 violation; the 3 extra runs are each ~537s of wasted wall time. +Because each gate uses a **different (source_roots OR binary) tuple**, none of the three produce byte-identical output. There is no artifact sharing opportunity between them today. The four compile invocations are not four calls to the same pure function — they are three distinct functions. -`EmitDeterminismGate` is the empirical oracle for non-reproducible emit: it runs the SAME compile TWICE independently and diffs the output trees. This is load-bearing — emit is KNOWN-NONDETERMINISTIC today (Rust emitter HashMap iteration order; `v2.std.determinism` at P1). Content-addressing does not make this gate redundant; it requires the gate to have already confirmed determinism before a content-address can be trusted. +The **only true redundancy** on Axis A is `EmitDeterminismGate`'s intentional oracle pair: it runs its own tuple twice to catch non-reproducible emit. That pair must survive: emit is KNOWN-NONDETERMINISTIC today (Rust emitter HashMap iteration order; `v2.std.determinism` at P1), making the empirical x2 diff the only live check for that bug class. Content-addressing the output would assume determinism, not prove it. + +**Axis A net today: no redundancy to remove.** The four compiles are four distinct necessary operations. The value of M2 (see §3) is therefore not present-day savings but **future-proofing**: the model makes it unwritable for a new gate to accidentally add a second compile of an existing tuple without declaring it. If a new gate is added that uses the same tuple as an existing gate, the structural dependency is explicit and the executor enforces sharing. ### Axis B — in-process `resolve_entry_graph` cross-batch (~30–40s per call) @@ -41,9 +43,11 @@ Any future `heavy_whole_tree_resolve` gate added to `floor_effect_gate_witness.d ## 2. Current model has no shared-output node -The plan in `std.realization_schedule` represents runnables as independent units. `RunnableSingleClaim` carries `entry`, `function`, and `profile` — but has no concept of a produced artifact that other runnables consume. `DataDependsOn` edges declare ordering (compile gate must pass before corpus runs) but they carry no payload (the resolved graph or compiled artifact). +The plan in `std.realization_schedule` represents runnables as independent units. `RunnableSingleClaim` carries `entry`, `function`, and `profile` — but has no concept of a produced artifact that other runnables consume. `DataDependsOn` edges declare ordering but carry no payload. + +For Axis B (in-process resolve): this means two batches in the same `claim_executor` process can call `resolve_entry_graph` for the same `(source_roots, entry)` pair without the executor knowing they're the same work. Fixing it by adding a memo to `claim_executor` without model surface would concede the bad state is writable: a future gate added to `floor_effect_gate_witness.dag` would silently double-pay again. -This means the executor cannot share the output of one runnable as the input of another. Each runnable independently recomputes from source. The double-payment is not a bug in the executor — it is an honest consequence of a model that has no shared-output primitive. Fixing it by adding a memo to `claim_executor` without changing the model would be a §5 validation standing where construction was available: a future gate added to `floor_effect_gate_witness.dag` would again silently double-pay. +For Axis A (subprocess compiles): the current gate set has no sharing opportunity (each gate uses a distinct tuple), so the missing shared-output primitive has no displacement value today. Its value is forward: if a future gate uses the same compile tuple as an existing gate, the model should make the sharing explicit and the duplication unwritable. --- From 5ec93ca0b1e231e7a88a7eae8249fb0b0dd197fd Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Mon, 29 Jun 2026 17:36:46 +0000 Subject: [PATCH 05/25] Fix M2: each gate uses distinct compile tuple; no artifact sharing today The three gates use different (source_roots, binary) tuples (verified): - DslCompileCleanGate: gunbc compile dsl+src/v2 - EmitDeterminismGate: gunbc compile dsl only (x2 oracle pair) - RegenVerifyGate: regen_stage0 --verify (different binary) No artifact sharing is possible across gates in the current set. M2's value is forward-proofing (future gates declaring the same tuple reuse the RunnableCompile node; duplicates caught by lens), not present-day savings. Displacement table corrected: M1 saves ~35s (resolve memo), M2 saves up to 1x compile when oracle pair collapses after #5941 closes the non-determinism gap. Also: M1 dissolution trigger corrected (M1 is orthogonal to M2, not subsumed by it). Co-Authored-By: Claude Sonnet 4.6 --- .../plans/floor-shared-compute-memoization.md | 60 +++++++++++-------- 1 file changed, 34 insertions(+), 26 deletions(-) diff --git a/docs/plans/floor-shared-compute-memoization.md b/docs/plans/floor-shared-compute-memoization.md index fc439662d3e..fb3ccbd8392 100644 --- a/docs/plans/floor-shared-compute-memoization.md +++ b/docs/plans/floor-shared-compute-memoization.md @@ -67,38 +67,39 @@ For Axis A (subprocess compiles): the current gate set has no sharing opportunit ### M2 — Compile artifact as a first-class plan node (Axis A) -**Mechanism:** Introduce `RunnableCompile` as a variant of `Runnable` in `std.realization_schedule`: +**Current gate set — no sharing opportunities today.** Each of the three compile operations uses a distinct `(source_roots, binary)` tuple (verified against source): + +| Gate | Tuple | +|---|---| +| `DslCompileCleanGate` | `(["dsl","src/v2"], gunbc compile)` | +| `EmitDeterminismGate` | `(["dsl"], gunbc compile)` — ×2 oracle pair | +| `RegenVerifyGate` | `(["src/v1","dsl"], regen_stage0 --verify)` — different binary | + +No two gates share a tuple, so no artifact sharing is possible across gates today. Each `RunnableCompile` node is independent; `DslCompileCleanGate` and `EmitDeterminismGate` are different source-root sets and cannot share an artifact without re-introducing the narrower-vs-wider corpus skew. + +**The EmitDeterminismGate oracle pair survives unchanged.** Its two cold compiles use the same tuple and are the empirical oracle for non-reproducible emit. Content-addressing assumes determinism; it does not prove it. Emit is KNOWN-NONDETERMINISTIC today (`v2.std.determinism` at P1), so memoizing the pair would delete the only live check for that bug (§5 coverage-by-illusion). The x2 compiles remain in any M2 shape. + +**M2's value is forward-looking, not present-day displacement.** The structural mechanism `RunnableCompile` is introduced so that if a future gate needs to compile the same `(source_roots, binary)` tuple as an existing gate, it must declare a `DataDependsOn` on the existing node rather than adding a second `RunnableCompile`. That second node would be statically flagged by the lens as a duplicate tuple — the double-compile becomes **unwritable by construction** rather than a silent accidental addition. + +**Mechanism sketch:** ``` type Runnable = RunnableSingleClaim { ... } -- existing | RunnableDiscoveryBatch { ... } -- existing - | RunnableCompile { -- NEW + | RunnableCompile { -- NEW (future-proofing wall) source_roots: List + binary: CompileBinary -- GunbcCompile | RegenStage0Verify | ... target: EmitTarget - artifact_id: ContentHash -- the content-address key profile: RunnableResourceProfile } ``` -A `RunnableCompile` is a plan node that: -1. Invokes `gunbc compile --source-root ... --target ...` -2. Content-addresses its output (directory tree hash) -3. Stores the artifact under `artifact_id` in a within-run artifact store -4. Exposes a typed `CompiledArtifact` handle to dependent nodes via `DataDependsOn` +A lens enforces: no two `RunnableCompile` nodes in the same plan share the same `(source_roots, binary, target)` key. A `RunnableSingleClaim` that invokes a compile operation must reference the plan's canonical `RunnableCompile` node for that tuple via `DataDependsOn`; it cannot shell out to compile independently. -**CRITICAL DEPENDENCY:** M2 is GATED on emit being deterministic. Today's Rust emitter has known non-determinism (HashMap iteration order in the emit path; `v2.std.determinism` is only at P1 as of 2026-06-29). Content-addressing a non-deterministic compile is unsound: two cold runs produce DIFFERING outputs, so a content-address key would collide on differing artifacts and serve an arbitrary one to consumers — the exact "key went green while the realizer faked the key" §5 fail-open trap. **M2 must not land until the determinism mechanism (#5941, `v2.std.determinism`) closes the non-determinism gap.** Sequence: M1 → determinism mechanism → M2. +**CRITICAL DEPENDENCY:** M2 is GATED on emit being deterministic. Content-addressing a non-deterministic compile output is unsound — two cold runs produce differing artifacts, so a content-address key would collide and serve an arbitrary one to consumers (the "key went green while the realizer faked the key" §5 trap). **M2 must not land until `v2.std.determinism` (#5941) closes the non-determinism gap.** Sequence: M1 → determinism mechanism → M2. -**The determinism gate is the ORACLE, not a redundancy.** `EmitDeterminismGate`'s two cold, independent compiles are the empirical oracle for non-reproducible emit. Content-addressing does not prove determinism — it assumes it. Memoizing the pair to one artifact would delete the only live check for a known bug, making the gate inert (§5 coverage-by-illusion). The x2 compiles REMAIN in M2. - -Dependent nodes change their contract under M2: -- `EmitDeterminismGate` → **unchanged**: still runs 2× cold, independent `gunbc compile` and diffs. It is the oracle that LICENSES the artifact as canonical. Both runs benefit from the M1 in-process resolve memo (same source closure, so each resolves once). Net: 2× compile (same as today for this gate), ~30–40s of resolve saved. -- `DslCompileCleanGate` → consumes `EmitDeterminismGate`'s proven-canonical `CompiledArtifact` via `DataDependsOn`. Checks that the compile exits 0. Does NOT re-compile. (Previously: 1× compile. After M2: 0× compile.) -- `RegenVerifyGate` → consumes the same proven-canonical `CompiledArtifact`. Verifies committed seed matches it. Does NOT re-compile. (Previously: 1× compile. After M2: 0× compile.) - -**Compile count:** 4× → 2× (the determinism oracle pair). Saves ~537s × 2 ≈ 18 min. - -**By-construction property:** The plan has exactly ONE `RunnableCompile` node per `(source_roots, target)` tuple. The executor raises a typed error if it encounters two `RunnableCompile` nodes with the same key — the plan is malformed, not silently redundant. A future gate that needs the compiled artifact adds a `DataDependsOn` on the existing `RunnableCompile` node; it cannot accidentally introduce a second compile without explicitly creating a second `RunnableCompile` node, which the lens will flag. +**Compile count:** unchanged today (4×). The benefit is prevention of future regression, not current displacement. --- @@ -124,12 +125,12 @@ M1 (within-walk resolve memo) is lower-risk and immediately addressable. M2 (`Ru **Recommendation: M1 first (one PR, small, purely additive); M2 as a follow-on with operator approval of the substrate shape.** **D3 — Does `EmitDeterminismGate` survive M2?** -Yes, it survives unchanged as the oracle. Its x2 compiles are not a cost to eliminate — they are the discriminating witness for non-reproducible emit, a known live bug. The gate dissolves only when the determinism mechanism (`v2.std.determinism`, #5941) closes the bug and makes non-determinism unwritable by construction; at that point the two cold compiles become definitionally redundant and the gate can be replaced by a construction-side check. Until then, deleting or memoizing the pair is a §5 coverage-by-illusion. +Yes, unchanged. Its x2 compiles are the empirical oracle for non-reproducible emit (a live bug). The gate dissolves only when `v2.std.determinism` (#5941) makes non-determinism unwritable by construction; at that point the pair becomes definitionally redundant and can be replaced by a construction-side check. **Recommendation: keep both compiles; gate M2 on the determinism mechanism landing.** -**D4 — Scope of `RunnableCompile.source_roots`.** -`DslCompileCleanGate` compiles `dsl + src/v2` (the full floor corpus). `EmitDeterminismGate` today compiles only `dsl`. These are different `(source_roots, target)` tuples — two `RunnableCompile` nodes. Is this the intended split, or should both use the same full-corpus compile? (The difference is intentional today because emit_determinism targets only `dsl`.) -**Recommendation: Preserve the existing split; document it explicitly in the plan as two separate `RunnableCompile` nodes with different `source_roots`.** +**D4 — Distinct tuples per gate in M2.** +All three gates use different `(source_roots, binary)` tuples and therefore each gets its own `RunnableCompile` node with no artifact sharing. This is the correct model — it is a change to HOW compile operations are declared in the plan (explicitly, as named nodes) rather than a change to how many compiles are run. A future gate that reuses an existing tuple will automatically reuse the node; that is the mechanism's payoff. +**Recommendation: accept the three-node model; document the distinct tuples explicitly so a future author knows which node to declare a dependency on.** --- @@ -143,16 +144,23 @@ Yes, it survives unchanged as the oracle. Its x2 compiles are not a cost to elim M1 saves ~30–40s per run (the Axis-B double-resolve). Small absolute, but the mechanism is a construction wall. Unblocked today. -M2 saves ~537s × 2 — the other two compiles (DslCompileCleanGate and RegenVerifyGate) consume the determinism oracle's proven-canonical artifact. That is ~18 minutes of CI wall time removed per run. **Gated on `v2.std.determinism` (#5941) closing the non-determinism gap before content-addressing compile output is sound.** +M2 saves **0 compiles today** — the current gate set has no duplicate `(source_roots, binary)` tuples (each gate uses a distinct one, verified). M2's value is forward-proofing: once the plan explicitly declares `RunnableCompile` nodes, a future gate that accidentally duplicates an existing tuple is caught by the lens before it silently adds another ~537s to CI. + +**M2 displacement after determinism closes** (future state): if `EmitDeterminismGate`'s x2 oracle pair collapses to 1× once emit is provably deterministic, that frees 1× ~537s. That is the max M2 displacement in the current gate set — not 2×. Any further wins require a new gate that would otherwise duplicate an existing tuple. -The combined displacement: **~2148s → ~1074s for the compile-related floor costs** (4→2 compiles, 2→1 resolve), roughly a 2× improvement. The remaining 2× (the determinism oracle pair) is load-bearing and dissolves only when emit is provably deterministic. +| Mechanism | Compiles today | Compiles after | Resolve calls | Time saved | +|---|---|---|---|---| +| baseline | 4× | — | 2× | — | +| + M1 | 4× | 4× | 1× | ~35s | +| + M2 (gated on #5941) | 4× | 3× or 4× | 1× | ~537s (if oracle pair collapses) | --- ## 7. Dissolution triggers M1 (`ResolveScopeShared` memo): -- Dissolves into M2 (`RunnableCompile`)'s pre-resolve: once the compile node holds the compiled+resolved graph as a typed artifact, the within-walk memo becomes a special case of "artifact produced by Batch-1 consumed by Batch-2" — the general mechanism subsumes it. +- Terminal within its scope: the within-walk resolve memo addresses Axis-B (in-process resolve deduplication across batches); it does not dissolve into M2, because M2 addresses Axis-A (subprocess compile declarations). The two are orthogonal. +- Dissolution trigger: when v2 streaming-infer (resource-aware-scheduler Node B/C) replaces the v1 whole-tree resolve with a dependency-batched resolve, per-entry memoization becomes a sub-case of the streaming boundary and M1's memo can be removed. - Intermediate milestone: lens verifies all `heavy_whole_tree_resolve: true` runnables carry `ResolveScopeShared`. M2 (`RunnableCompile`): From 06cf6eaf89da52568271069cd466e65b046d0b70 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Mon, 29 Jun 2026 17:48:54 +0000 Subject: [PATCH 06/25] =?UTF-8?q?Fix=20=C2=A76=20displacement=20table=20an?= =?UTF-8?q?d=20=C2=A77=20collapse=20claim?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Table row said '×2' (oracle pair survives) but the text below correctly said 4→3 (three distinct tuples remain after oracle pair 2→1). Fix to '×3' throughout. §7 'collapse to 1× total compile' was impossible: even after oracle pair collapses, DslCompileClean + EmitDeterminism×1 + RegenVerify are three distinct-tuple operations and all remain necessary. Corrected to '4→3×'. Co-Authored-By: Claude Sonnet 4.6 --- docs/plans/floor-shared-compute-memoization.md | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/docs/plans/floor-shared-compute-memoization.md b/docs/plans/floor-shared-compute-memoization.md index fb3ccbd8392..e6c78c1834f 100644 --- a/docs/plans/floor-shared-compute-memoization.md +++ b/docs/plans/floor-shared-compute-memoization.md @@ -139,8 +139,8 @@ All three gates use different `(source_roots, binary)` tuples and therefore each | Cost today | Cost after M1 | Cost after M1+M2 (gated on determinism) | |---|---|---| | `resolve_entry_graph` × 2 per run (~30–40s each) | × 1 (memo deduplicates Batch 1 → Batch 2) | × 1 | -| `gunbc compile` × 4 per run (~537s each) | × 4 (M1 doesn't help subprocess) | × 2 (determinism oracle pair survives) | -| **Total compile cost per run** | ~2148s – ~37s ≈ same subprocess cost, saved resolve | **~1074s + ~37s → 2× compile, 1× resolve** | +| `gunbc compile` × 4 per run (~537s each) | × 4 (M1 doesn't help subprocess) | × 3 (oracle pair 2→1; other two tuples unchanged) | +| **Total compile cost per run** | ~2148s – ~37s ≈ same subprocess cost, saved resolve | **~1611s + ~37s → 3× compile, 1× resolve** | M1 saves ~30–40s per run (the Axis-B double-resolve). Small absolute, but the mechanism is a construction wall. Unblocked today. @@ -165,6 +165,6 @@ M1 (`ResolveScopeShared` memo): M2 (`RunnableCompile`): - **Gated on**: `v2.std.determinism` (#5941) closing non-reproducible emit. Content-addressing the artifact is unsound until emit is deterministic. Do not land M2 before this gate closes. -- After determinism closes: `EmitDeterminismGate` dissolves from an empirical oracle into a construction-verified witness; the 2× oracle pair becomes 1× (and M2 can collapse further to 1× total compile). +- After determinism closes: `EmitDeterminismGate` dissolves from an empirical oracle into a construction-verified witness; the 2× oracle pair becomes 1×, reducing total compiles from 4× to 3× (DslCompileClean, EmitDeterminism×1, RegenVerify each use distinct tuples and all remain necessary). Further reduction below 3× would require either collapsing two of the existing tuples to the same `(source_roots, binary)` or removing a gate — neither is in scope here. - Dissolves into the v2 scheduler (resource-aware-scheduler.md Node B/C) once the scheduler derives `Runnable.cost` from the compile node's output rather than static measurement rows. - Dissolves into the Realization pattern (#4867) for cross-run caching once M2's content-addressed artifact is stored on disk between runs. From 20fa4e8f70f31480561c232426ff7ce1aad29a6a Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Mon, 29 Jun 2026 18:08:51 +0000 Subject: [PATCH 07/25] WIP: DESIGN SKETCH ONLY (no code; returns to stern-moth-225 + operator before --- .../plans/floor-shared-compute-memoization.md | 24 ++++++++++++------- 1 file changed, 16 insertions(+), 8 deletions(-) diff --git a/docs/plans/floor-shared-compute-memoization.md b/docs/plans/floor-shared-compute-memoization.md index e6c78c1834f..4345e40d629 100644 --- a/docs/plans/floor-shared-compute-memoization.md +++ b/docs/plans/floor-shared-compute-memoization.md @@ -30,14 +30,20 @@ The **only true redundancy** on Axis A is `EmitDeterminismGate`'s intentional or ### Axis B — in-process `resolve_entry_graph` cross-batch (~30–40s per call) -`claim_executor`'s `run_walk` runs batches sequentially. The current batch-local `SharedClaims` deduplication does not persist across batch boundaries. The `floor_effect_gate_witness.dag` closure (~106 modules) is resolved in: +`claim_executor`'s `run_walk` runs batches sequentially. The current batch-local `SharedClaims` deduplication does not persist across batch boundaries. -- Batch 1: evaluate `dsl_compile_clean_gate_passes` → 1 call to `resolve_entry_graph` -- Batch 2: evaluate all Group-A gate witnesses → 1 call to `resolve_entry_graph` for the SAME entry +Eight of nine gates use `floor_gate_witness_entry = "dsl/tools/floor_effect_gate_witness.dag"` as their `.dag` claim entry (`ci_floor_plan.dag:139-143,150-151`). Only `SourceRootIngestGate` uses a different entry (`source_root_ingest_gate.dag`). The heavy-resolve serialization (`floor_heavy_resolve_chain_resource_edges`) places `RegenVerifyGate` and `EmitDeterminismGate` each in their own batch, alone, so `resolve_entry_graph` is called **4 times** on the same `floor_effect_gate_witness.dag` closure (~106 modules) per CI run: -These are the same `(source_roots, entry)` pair; same pure function; same output. Both calls happen in the same OS process within ~52s of each other. The second pays a full ~30–40s re-resolve for no reason. +| Call | Batch | Claim(s) | Resolve shared? | +|---|---|---|---| +| 1 | Batch 1 (compile anchor, alone) | `dsl_compile_clean_gate_passes` | — (first call) | +| 2 | Batch 2 Group A (5 negligible gates) | rust, emit_host, layering, extdeps, drift | SharedClaims within batch → 1 call for 5 claims | +| 3 | Later batch (alone, serialized) | `regen_verify_gate_passes` | re-resolves; no cross-batch sharing | +| 4 | Later batch (alone, serialized) | `emit_determinism_gate_passes` | re-resolves; no cross-batch sharing | + +Calls 2–4 are redundant: same `(source_roots, entry)` pair, same pure function, same output. Three resolves are wasted across three separate batch boundaries within one `claim_executor` process. -Any future `heavy_whole_tree_resolve` gate added to `floor_effect_gate_witness.dag` will silently add another ~30–40s re-resolve. The behavior is not unwritable — it just happens automatically. +M1 eliminates calls 2, 3, and 4 by memoizing the resolved graph from call 1 across the walk. Any future `heavy_whole_tree_resolve` gate added to `floor_effect_gate_witness.dag` in its own serialized batch would silently add a 5th call — the behavior is not unwritable today. --- @@ -61,9 +67,11 @@ For Axis A (subprocess compiles): the current gate set has no sharing opportunit **Memory:** The resolved graph for `floor_effect_gate_witness.dag` is ~0.9 GiB. Since the heavy-resolve chain already serializes these batches (Batch 1 finishes before Batch 2 starts), both batches hold the graph at different times — the memo doesn't increase peak memory, it keeps the Batch 1 graph alive slightly longer. This is acceptable. -**By-construction property:** Any gate in any entry that `run_walk` has already resolved in this run gets the memo automatically. A future gate added to `floor_effect_gate_witness.dag` cannot accidentally double-pay — the walk owns the resolve decision. +**Model surface needed (DESIGN.md §5 "model before implement"):** The `RunnableResourceProfile` already carries `heavy_whole_tree_resolve: Bool`. A new field `resolve_scope: ResolveScope` where `ResolveScope = ResolveScopeIsolated | ResolveScopeShared` lets the model explicitly declare which runnables participate in the shared resolve pool: +- `ResolveScopeShared` — the executor provides the memoized `ResolvedGraph` from the first resolve of this `(source_roots, entry)` in the walk; a second resolve is structurally impossible (the executor owns it). This is the construction guarantee. +- `ResolveScopeIsolated` (default) — the executor resolves independently; no sharing. Fail-closed: a new gate that omits `ResolveScopeShared` re-resolves rather than silently sharing stale data. The wrong behavior is safe (extra work), not silent (shared stale result). -**Model surface needed (DESIGN.md §5 "model before implement"):** The `RunnableResourceProfile` already carries `heavy_whole_tree_resolve: Bool`. A new field `resolve_scope: ResolveScope` where `ResolveScope = ResolveScopeIsolated | ResolveScopeShared` lets the model explicitly declare which runnables participate in the shared resolve pool. The executor enforces: `ResolveScopeShared` entries may NOT re-resolve; a future runnable without this field defaults to `ResolveScopeIsolated` (safe, fail-closed — it re-resolves rather than silently sharing stale data). The lens verifies that every `heavy_whole_tree_resolve: true` runnable declares `ResolveScopeShared`. +The memo does NOT apply automatically to all same-entry resolves — only to `ResolveScopeShared` entries. This preserves the construction authority in the model rather than making the executor's behavior implicit. The lens verifies: every `heavy_whole_tree_resolve: true` runnable must declare `ResolveScopeShared` (the combination is never correct to isolate — a heavy resolve that runs independently in each batch is the violation this mechanism walls off). ### M2 — Compile artifact as a first-class plan node (Axis A) @@ -138,7 +146,7 @@ All three gates use different `(source_roots, binary)` tuples and therefore each | Cost today | Cost after M1 | Cost after M1+M2 (gated on determinism) | |---|---|---| -| `resolve_entry_graph` × 2 per run (~30–40s each) | × 1 (memo deduplicates Batch 1 → Batch 2) | × 1 | +| `resolve_entry_graph` × 4 per run (~30–40s each) | × 1 (memo deduplicates calls 2–4 to call 1) | × 1 | | `gunbc compile` × 4 per run (~537s each) | × 4 (M1 doesn't help subprocess) | × 3 (oracle pair 2→1; other two tuples unchanged) | | **Total compile cost per run** | ~2148s – ~37s ≈ same subprocess cost, saved resolve | **~1611s + ~37s → 3× compile, 1× resolve** | From e1e46a09d9482c16dc30064eabcb3dd36e8aff13 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Mon, 29 Jun 2026 18:09:50 +0000 Subject: [PATCH 08/25] =?UTF-8?q?Fix=20=C2=A76=20displacement=20table:=20b?= =?UTF-8?q?aseline=204=C3=97=20resolves=20(not=202=C3=97),=20M1=20saves=20?= =?UTF-8?q?~105s=20(not=20~35s)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Round 4 reviewer finding: Axis B actually has 4 resolve_entry_graph calls per run (Batch 1 DslCompileClean, Batch 2 SharedClaims group, serialized RegenVerify batch, serialized EmitDeterminism batch) — not 2×. M1 eliminates 3 redundant calls → ~105s saved, not ~35s. Co-Authored-By: Claude Sonnet 4.6 --- docs/plans/floor-shared-compute-memoization.md | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/docs/plans/floor-shared-compute-memoization.md b/docs/plans/floor-shared-compute-memoization.md index 4345e40d629..694bb2ae62b 100644 --- a/docs/plans/floor-shared-compute-memoization.md +++ b/docs/plans/floor-shared-compute-memoization.md @@ -150,7 +150,7 @@ All three gates use different `(source_roots, binary)` tuples and therefore each | `gunbc compile` × 4 per run (~537s each) | × 4 (M1 doesn't help subprocess) | × 3 (oracle pair 2→1; other two tuples unchanged) | | **Total compile cost per run** | ~2148s – ~37s ≈ same subprocess cost, saved resolve | **~1611s + ~37s → 3× compile, 1× resolve** | -M1 saves ~30–40s per run (the Axis-B double-resolve). Small absolute, but the mechanism is a construction wall. Unblocked today. +M1 saves ~105s per run (3 redundant Axis-B resolves × ~35s each). The mechanism is a construction wall. Unblocked today. M2 saves **0 compiles today** — the current gate set has no duplicate `(source_roots, binary)` tuples (each gate uses a distinct one, verified). M2's value is forward-proofing: once the plan explicitly declares `RunnableCompile` nodes, a future gate that accidentally duplicates an existing tuple is caught by the lens before it silently adds another ~537s to CI. @@ -158,8 +158,8 @@ M2 saves **0 compiles today** — the current gate set has no duplicate `(source | Mechanism | Compiles today | Compiles after | Resolve calls | Time saved | |---|---|---|---|---| -| baseline | 4× | — | 2× | — | -| + M1 | 4× | 4× | 1× | ~35s | +| baseline | 4× | — | 4× | — | +| + M1 | 4× | 4× | 1× | ~105s (3 calls × ~35s) | | + M2 (gated on #5941) | 4× | 3× or 4× | 1× | ~537s (if oracle pair collapses) | --- From 8e22c7ef4a88c8410ef9622a70c00685b25fa8c2 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Mon, 29 Jun 2026 18:22:08 +0000 Subject: [PATCH 09/25] =?UTF-8?q?Fix=20stale=20~37s=20in=20=C2=A76=20Total?= =?UTF-8?q?=20row=20=E2=80=94=20M1=20saves=20~105s=20not=20~35s?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit cursor review finding: Total compile cost row had ~37s in both M1 columns, inconsistent with the corrected ~105s in the M1 granular table row and prose. Co-Authored-By: Claude Sonnet 4.6 --- docs/plans/floor-shared-compute-memoization.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/docs/plans/floor-shared-compute-memoization.md b/docs/plans/floor-shared-compute-memoization.md index 694bb2ae62b..c14c60e8cec 100644 --- a/docs/plans/floor-shared-compute-memoization.md +++ b/docs/plans/floor-shared-compute-memoization.md @@ -148,7 +148,7 @@ All three gates use different `(source_roots, binary)` tuples and therefore each |---|---|---| | `resolve_entry_graph` × 4 per run (~30–40s each) | × 1 (memo deduplicates calls 2–4 to call 1) | × 1 | | `gunbc compile` × 4 per run (~537s each) | × 4 (M1 doesn't help subprocess) | × 3 (oracle pair 2→1; other two tuples unchanged) | -| **Total compile cost per run** | ~2148s – ~37s ≈ same subprocess cost, saved resolve | **~1611s + ~37s → 3× compile, 1× resolve** | +| **Total compile cost per run** | ~2148s – ~105s ≈ same subprocess cost, saved resolve | **~1611s + ~105s → 3× compile, 1× resolve** | M1 saves ~105s per run (3 redundant Axis-B resolves × ~35s each). The mechanism is a construction wall. Unblocked today. From 111564b900c0b0383dc3fa3183da3015188ad0a4 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Mon, 29 Jun 2026 18:42:47 +0000 Subject: [PATCH 10/25] Add link to floor-shared-compute-memoization sketch in DESIGN.md open threads Fixes doc_graph_has_no_orphan_docs CI failure: the new docs/plans file was not reachable from DESIGN.md. Added li to open_threads_blocks() and regenerated DESIGN.md via main_wet. Co-Authored-By: Claude Sonnet 4.6 --- DESIGN.md | 1 + dsl/gunbc/design_document.dag | 1 + 2 files changed, 2 insertions(+) diff --git a/DESIGN.md b/DESIGN.md index e119e8efe6a..9f3d0dce369 100644 --- a/DESIGN.md +++ b/DESIGN.md @@ -83,6 +83,7 @@ hollow alias (minimality ≠ grounding) · state-space conflation (an `Option`/` - can a lens mechanically diagnose the *leaf-side* of decomposition (§2)? (operator-parked) - the model↔realization fork is systemic, and where unfinished it fails open: every primitive is modeled as a coproduct and realized as a native `Value`, reconciled by per-site bridges, so coverage is accidental and non-compositional. `match` bridges `Int→Zero/Succ` but `Value::eq` has no `Int↔Variant` arm, so `nat_add(85, 32) == 117` silently compared `false` at its `_ => false` chokepoint — a §5 fail-open, not the §2/§7 redundancy the 🟡 dissolve-on markers track. **Landed:** the *numeric tower* fork now fails closed — `eval_binop`'s `BinOp::Eq`/`Ne` raises `InterpError::CrossRepresentationEquality` when a `false` result is *explained* by a native `Int`/`Float` vs `Nat`-coproduct straddle (recursive: catches `nat_add == nat_add` and `[nat_add(1,1)] == [2]`), with `Value::eq` left infallible so it stays the single `CanonKey` map-key authority. The discriminating witness is `cross_representation_equality_test` (forks → typed error; reconciled/native → `true`; genuine diffs `1 == 2`/`Succ{..} == Zero` → `false`, not error). **Remaining:** (a) the same straddle for `Bool True|False` over `Value::Bool` (no `==` site in the corpus today) and `Optional/Witness` over `Value::Null` — the latter resists a blanket guard because `Value::Null` is the overloaded `None`/`Absent`/miss sentinel and `present == None` (131 sites) is a *legitimate* `false`, so it needs grounding, not an error arm; (b) the root fix (§1/§2/§7) — ground each primitive into its realization. **Numeric tower: GROUNDED** (#5428, 2026-06-21) — Nat construction-side grounded (`Zero → Int(0)`, `Succ{prev:Int(k)} → Int(k+1)`); native form == modeled form; `eval_binop` `CrossRepresentationEquality` guard is dead-in-corpus for numerics, kept as fail-closed backstop until the `Value::Null` split lands (guard removal bundled with that work, fenced out of this window). **Remaining:** `Value::Null` split — Optional/Witness/miss into own carriers (~131 sites; the deeper root, its own runway). (operator: `==` fail-closed, 2026-06-20) - the remaining deleted-`docs/` references in `.dag` comments — provenance / `bind:` pointers into the bankrupted `docs/` tree (e.g. `docs/planning/*`, `design-*.md`) — fold into the dep-graph reform, not a blind repoint. (The named-corpus ledger marks — `Practice N`, and `INVARIANTS` / `THESIS` / `MODELING` / `RELEASE_TODO` / … citations — were swept: dropped, or re-homed to DESIGN.md §-anchors.) +- floor shared-computation memoization — make the double-paid full-tree compile UNREPEATABLE by construction (M1: within-walk resolve memo ~105s; M2: RunnableCompile node gated on v2.std.determinism #5941): [design sketch](docs/plans/floor-shared-compute-memoization.md) ## Building & checks diff --git a/dsl/gunbc/design_document.dag b/dsl/gunbc/design_document.dag index e89b3d80c90..629fe60109c 100644 --- a/dsl/gunbc/design_document.dag +++ b/dsl/gunbc/design_document.dag @@ -143,6 +143,7 @@ fn open_threads_blocks() -> List { li(text: "can a lens mechanically diagnose the *leaf-side* of decomposition (§2)? (operator-parked)"), li(text: "the model↔realization fork is systemic, and where unfinished it fails open: every primitive is modeled as a coproduct and realized as a native `Value`, reconciled by per-site bridges, so coverage is accidental and non-compositional. `match` bridges `Int→Zero/Succ` but `Value::eq` has no `Int↔Variant` arm, so `nat_add(85, 32) == 117` silently compared `false` at its `_ => false` chokepoint — a §5 fail-open, not the §2/§7 redundancy the 🟡 dissolve-on markers track. **Landed:** the *numeric tower* fork now fails closed — `eval_binop`'s `BinOp::Eq`/`Ne` raises `InterpError::CrossRepresentationEquality` when a `false` result is *explained* by a native `Int`/`Float` vs `Nat`-coproduct straddle (recursive: catches `nat_add == nat_add` and `[nat_add(1,1)] == [2]`), with `Value::eq` left infallible so it stays the single `CanonKey` map-key authority. The discriminating witness is `cross_representation_equality_test` (forks → typed error; reconciled/native → `true`; genuine diffs `1 == 2`/`Succ\{..\} == Zero` → `false`, not error). **Remaining:** (a) the same straddle for `Bool True|False` over `Value::Bool` (no `==` site in the corpus today) and `Optional/Witness` over `Value::Null` — the latter resists a blanket guard because `Value::Null` is the overloaded `None`/`Absent`/miss sentinel and `present == None` (131 sites) is a *legitimate* `false`, so it needs grounding, not an error arm; (b) the root fix (§1/§2/§7) — ground each primitive into its realization. **Numeric tower: GROUNDED** (#5428, 2026-06-21) — Nat construction-side grounded (`Zero → Int(0)`, `Succ\{prev:Int(k)\} → Int(k+1)`); native form == modeled form; `eval_binop` `CrossRepresentationEquality` guard is dead-in-corpus for numerics, kept as fail-closed backstop until the `Value::Null` split lands (guard removal bundled with that work, fenced out of this window). **Remaining:** `Value::Null` split — Optional/Witness/miss into own carriers (~131 sites; the deeper root, its own runway). (operator: `==` fail-closed, 2026-06-20)"), li(text: "the remaining deleted-`docs/` references in `.dag` comments — provenance / `bind:` pointers into the bankrupted `docs/` tree (e.g. `docs/planning/*`, `design-*.md`) — fold into the dep-graph reform, not a blind repoint. (The named-corpus ledger marks — `Practice N`, and `INVARIANTS` / `THESIS` / `MODELING` / `RELEASE_TODO` / … citations — were swept: dropped, or re-homed to DESIGN.md §-anchors.)"), + li(text: "floor shared-computation memoization — make the double-paid full-tree compile UNREPEATABLE by construction (M1: within-walk resolve memo ~105s; M2: RunnableCompile node gated on v2.std.determinism #5941): [design sketch](docs/plans/floor-shared-compute-memoization.md)"), ]), ] } From ec8e6f1cebc6beef04b9b9527a0826c81275faf9 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Tue, 30 Jun 2026 11:55:27 +0000 Subject: [PATCH 11/25] WIP: DESIGN SKETCH ONLY (no code; returns to stern-moth-225 + operator before --- dsl/std/realization_schedule.dag | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/dsl/std/realization_schedule.dag b/dsl/std/realization_schedule.dag index 66b654592d8..67d1080cbad 100644 --- a/dsl/std/realization_schedule.dag +++ b/dsl/std/realization_schedule.dag @@ -65,10 +65,15 @@ type RunnableMemoryClass = RunnableMemoryNegligible | RunnableMemorySubstantial { peak: RunnableMemoryPeak } +type ResolveScope + = ResolveScopeIsolated + | ResolveScopeShared + type RunnableResourceProfile { heavy_whole_tree_resolve: Bool spawns_host_compiler: Bool memory: RunnableMemoryClass + resolve_scope: ResolveScope } fn runnable_memory_negligible() -> RunnableMemoryClass { From 78c94ce4e6701322e2e8825281bcbcb2f267c9d7 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Tue, 30 Jun 2026 12:10:29 +0000 Subject: [PATCH 12/25] WIP: DESIGN SKETCH ONLY (no code; returns to stern-moth-225 + operator before --- dsl/std/realization_schedule.dag | 56 ++++++++++++++++++- ...runnable_resource_profile_witness_test.dag | 10 +++- src/v2/workflow/ci_floor_plan.dag | 24 +++++--- 3 files changed, 79 insertions(+), 11 deletions(-) diff --git a/dsl/std/realization_schedule.dag b/dsl/std/realization_schedule.dag index 67d1080cbad..598a2bcc22b 100644 --- a/dsl/std/realization_schedule.dag +++ b/dsl/std/realization_schedule.dag @@ -112,10 +112,24 @@ fn runnable_memory_substantial_sum(left: RunnableMemoryClass, right: RunnableMem runnable_memory_substantial(predicted_peak: byte_size(count: left_count + right_count)) } +fn resolve_scope_eq(left: ResolveScope, right: ResolveScope) -> Bool { + match left { + ResolveScopeIsolated => match right { + ResolveScopeIsolated => true + ResolveScopeShared => false + } + ResolveScopeShared => match right { + ResolveScopeIsolated => false + ResolveScopeShared => true + } + } +} + fn runnable_resource_profile_eq(left: RunnableResourceProfile, right: RunnableResourceProfile) -> Bool { (left.heavy_whole_tree_resolve == right.heavy_whole_tree_resolve) && (left.spawns_host_compiler == right.spawns_host_compiler) && runnable_memory_class_eq(left: left.memory, right: right.memory) + && resolve_scope_eq(left: left.resolve_scope, right: right.resolve_scope) } fn runnable_resource_profile_negligible() -> RunnableResourceProfile { @@ -123,18 +137,32 @@ fn runnable_resource_profile_negligible() -> RunnableResourceProfile { heavy_whole_tree_resolve: false spawns_host_compiler: false memory: runnable_memory_negligible() + resolve_scope: ResolveScopeIsolated } } fn runnable_resource_profile( heavy_whole_tree_resolve: Bool, spawns_host_compiler: Bool, - memory: RunnableMemoryClass + memory: RunnableMemoryClass, + resolve_scope: ResolveScope ) -> RunnableResourceProfile { RunnableResourceProfile { heavy_whole_tree_resolve: heavy_whole_tree_resolve spawns_host_compiler: spawns_host_compiler memory: memory + resolve_scope: resolve_scope + } +} + +fn runnable_profile_resolve_scope_valid(profile: RunnableResourceProfile) -> Bool { + if profile.heavy_whole_tree_resolve { + match profile.resolve_scope { + ResolveScopeShared => true + ResolveScopeIsolated => false + } + } else { + true } } @@ -188,6 +216,19 @@ type Runnable data runnable_kernel_workload_dissolution_trigger: String = "dissolve-on: execution lane attaches extdeps.languages kernel_surface rows to RunnableKernelWorkload when fused_op_count alone is insufficient; op_count is structural on substrate (not a string-label nickname)." +fn runnable_resolve_scope_valid(r: Runnable) -> Bool { + runnable_profile_resolve_scope_valid(profile: runnable_profile(r: r)) +} + +fn batch_all_resolve_scope_valid(batch: List) -> Bool { + if batch.count() == 0 { + true + } else { + runnable_resolve_scope_valid(r: batch.first()) && + batch_all_resolve_scope_valid(batch: batch.skip(n: 1)) + } +} + type Schedule = List> type RealizationPlan { @@ -198,6 +239,19 @@ type RealizationPlan { total: CostAccount } +fn schedule_list_all_resolve_scope_valid(sched: Schedule) -> Bool { + if sched.count() == 0 { + true + } else { + batch_all_resolve_scope_valid(batch: sched.first()) && + schedule_list_all_resolve_scope_valid(sched: sched.skip(n: 1)) + } +} + +fn schedule_all_runnables_valid_resolve_scope(plan: RealizationPlan) -> Bool { + schedule_list_all_resolve_scope_valid(sched: plan.schedule) +} + fn runnable_step_label(r: Runnable) -> String { match r { RunnableSingleClaim { entry: _, function: f, profile: _ } => f diff --git a/dsl/test/claim/runnable_resource_profile_witness_test.dag b/dsl/test/claim/runnable_resource_profile_witness_test.dag index 91a87a0fb63..20bc8880a59 100644 --- a/dsl/test/claim/runnable_resource_profile_witness_test.dag +++ b/dsl/test/claim/runnable_resource_profile_witness_test.dag @@ -4,6 +4,7 @@ import std.realization_schedule { Runnable, RunnableSingleClaim, RunnableDiscoveryBatch, + ResolveScopeIsolated, runnable_resource_profile, runnable_resource_profile_negligible, runnable_memory_substantial, @@ -25,7 +26,8 @@ fn witness_substantial_memory_forbids_corpus_co_residence() -> Bool { profile: runnable_resource_profile( heavy_whole_tree_resolve: false, spawns_host_compiler: false, - memory: runnable_memory_substantial(predicted_peak: byte_size(count: 1)) + memory: runnable_memory_substantial(predicted_peak: byte_size(count: 1)), + resolve_scope: ResolveScopeIsolated ) } runnable_forbids_corpus_co_residence(r: heavy) @@ -40,7 +42,8 @@ fn witness_corpus_never_forbids_co_residence() -> Bool { profile: runnable_resource_profile( heavy_whole_tree_resolve: true, spawns_host_compiler: false, - memory: runnable_memory_substantial(predicted_peak: byte_size(count: 3226056704)) + memory: runnable_memory_substantial(predicted_peak: byte_size(count: 3226056704)), + resolve_scope: ResolveScopeIsolated ) } !runnable_forbids_corpus_co_residence(r: corpus) @@ -53,7 +56,8 @@ fn witness_memory_sum_matches_byte_totals() -> Bool { byte_size_count(b: runnable_predicted_space(profile: runnable_resource_profile( heavy_whole_tree_resolve: false, spawns_host_compiler: false, - memory: sum + memory: sum, + resolve_scope: ResolveScopeIsolated ))) == 300 } diff --git a/src/v2/workflow/ci_floor_plan.dag b/src/v2/workflow/ci_floor_plan.dag index 39b4a290842..7c0c21cfb1d 100644 --- a/src/v2/workflow/ci_floor_plan.dag +++ b/src/v2/workflow/ci_floor_plan.dag @@ -40,6 +40,9 @@ import std.realization_schedule { RunnableSingleClaim, RunnableDiscoveryBatch, RunnableResourceProfile, + ResolveScope, + ResolveScopeShared, + ResolveScopeIsolated, runnable_resource_profile, runnable_resource_profile_negligible, runnable_memory_negligible, @@ -103,31 +106,36 @@ fn gate_runnable_profile(g: Gate) -> RunnableResourceProfile { runnable_resource_profile( heavy_whole_tree_resolve: true, spawns_host_compiler: false, - memory: per_shard + memory: per_shard, + resolve_scope: ResolveScopeShared ) SourceRootIngestGate => runnable_resource_profile( heavy_whole_tree_resolve: true, spawns_host_compiler: false, - memory: per_shard + memory: per_shard, + resolve_scope: ResolveScopeShared ) RegenVerifyGate => runnable_resource_profile( heavy_whole_tree_resolve: true, spawns_host_compiler: true, - memory: runnable_memory_substantial_sum(left: per_shard, right: host_compiler) + memory: runnable_memory_substantial_sum(left: per_shard, right: host_compiler), + resolve_scope: ResolveScopeShared ) EmitDeterminismGate => runnable_resource_profile( heavy_whole_tree_resolve: true, spawns_host_compiler: true, - memory: runnable_memory_substantial_sum(left: per_shard, right: host_compiler) + memory: runnable_memory_substantial_sum(left: per_shard, right: host_compiler), + resolve_scope: ResolveScopeShared ) EmitHostGate => runnable_resource_profile( heavy_whole_tree_resolve: false, spawns_host_compiler: true, - memory: host_compiler + memory: host_compiler, + resolve_scope: ResolveScopeIsolated ) RustMonolithGate => runnable_resource_profile_negligible() LayeringImportsGate => runnable_resource_profile_negligible() @@ -171,7 +179,8 @@ fn corpus_runnable() -> Runnable { profile: runnable_resource_profile( heavy_whole_tree_resolve: true, spawns_host_compiler: false, - memory: runnable_memory_substantial(predicted_peak: gunbc_ci_floor_per_shard_peak_rss_bytes()) + memory: runnable_memory_substantial(predicted_peak: gunbc_ci_floor_per_shard_peak_rss_bytes()), + resolve_scope: ResolveScopeShared ) } } @@ -197,7 +206,8 @@ fn execution_corpus_runnable() -> Runnable { profile: runnable_resource_profile( heavy_whole_tree_resolve: true, spawns_host_compiler: false, - memory: runnable_memory_substantial(predicted_peak: gunbc_ci_floor_execution_corpus_per_witness_rss) + memory: runnable_memory_substantial(predicted_peak: gunbc_ci_floor_execution_corpus_per_witness_rss), + resolve_scope: ResolveScopeShared ) } } From 88156a36aaa2ee99e45377dbafc125b8bce0590b Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Tue, 30 Jun 2026 12:20:58 +0000 Subject: [PATCH 13/25] WIP: DESIGN SKETCH ONLY (no code; returns to stern-moth-225 + operator before --- src/v1/stage0/src/bin/claim_executor.rs | 28 ++++++-- src/v1/stage0/src/std_realization_schedule.rs | 67 ++++++++++++++++++- 2 files changed, 88 insertions(+), 7 deletions(-) diff --git a/src/v1/stage0/src/bin/claim_executor.rs b/src/v1/stage0/src/bin/claim_executor.rs index 1a62b497de7..09cf7e483b1 100644 --- a/src/v1/stage0/src/bin/claim_executor.rs +++ b/src/v1/stage0/src/bin/claim_executor.rs @@ -22,6 +22,7 @@ enum Runnable { SingleClaim { entry: String, function: String, + use_walk_memo: bool, }, DiscoveryBatch { source_roots: Vec, @@ -119,16 +120,29 @@ fn runnable_from_value(value: &Value, ctx: &InterpContext) -> Result Ok(Runnable::SingleClaim { - entry: str_field(fields, "entry", "RunnableSingleClaim", ctx)?, - function: str_field(fields, "function", "RunnableSingleClaim", ctx)?, - }), + } if ctx.sym_eq(*variant_name, "RunnableSingleClaim") => { + let entry = str_field(fields, "entry", "RunnableSingleClaim", ctx)?; + let function = str_field(fields, "function", "RunnableSingleClaim", ctx)?; + let use_walk_memo = match ctx.field(fields, "profile") { + Some(Value::Record { fields: pf, .. }) | Some(Value::Variant { fields: pf, .. }) => { + match ctx.field(pf, "resolve_scope") { + Some(Value::Variant { variant_name: vn, .. }) => { + ctx.sym_eq(*vn, "ResolveScopeShared") + } + _ => false, + } + } + _ => false, + }; + Ok(Runnable::SingleClaim { entry, function, use_walk_memo }) + } Value::Variant { variant_name, fields, @@ -254,6 +268,7 @@ enum BatchUnit { SharedClaims { entry: String, functions: Vec, + use_walk_memo: bool, }, UnrunnableSentinel { function: String, @@ -283,7 +298,7 @@ fn group_batch_units(batch: &[Runnable]) -> Vec { function: function.clone(), }); } - Runnable::SingleClaim { entry, function } => { + Runnable::SingleClaim { entry, function, use_walk_memo } => { if let Some(&idx) = entry_to_unit.get(entry) { if let BatchUnit::SharedClaims { functions, .. } = &mut units[idx] { functions.push(function.clone()); @@ -293,6 +308,7 @@ fn group_batch_units(batch: &[Runnable]) -> Vec { units.push(BatchUnit::SharedClaims { entry: entry.clone(), functions: vec![function.clone()], + use_walk_memo: *use_walk_memo, }); } } @@ -403,7 +419,7 @@ fn run_batch_unit( spawn_width, spawn_width_cap, )], - BatchUnit::SharedClaims { entry, functions } => { + BatchUnit::SharedClaims { entry, functions, .. } => { run_shared_entry_claims(&source_roots, &entry, &functions) } } diff --git a/src/v1/stage0/src/std_realization_schedule.rs b/src/v1/stage0/src/std_realization_schedule.rs index bd2ca24e794..f502bc826e9 100644 --- a/src/v1/stage0/src/std_realization_schedule.rs +++ b/src/v1/stage0/src/std_realization_schedule.rs @@ -4,6 +4,7 @@ use self::CostBasis::*; use self::Runnable::*; use self::RunnableMemoryClass::*; +use self::ResolveScope::*; use self::ScheduleLensViolation::*; use crate::std_lens_verdict::LensVerdict::{Holds, Violation}; use crate::std_lens_verdict::LensVerdictLocus::ModuleWholeFile; @@ -97,11 +98,21 @@ impl RunnableMemoryClass { } } +#[derive( + Debug, Clone, Copy, PartialEq, Eq, PartialOrd, Ord, serde::Serialize, serde::Deserialize, +)] +#[serde(tag = "_variant")] +pub enum ResolveScope { + ResolveScopeIsolated, + ResolveScopeShared, +} + #[derive(Debug, Clone, PartialEq, serde::Serialize, serde::Deserialize)] pub struct RunnableResourceProfile { pub heavy_whole_tree_resolve: bool, pub spawns_host_compiler: bool, pub memory: Rc, + pub resolve_scope: ResolveScope, } pub fn runnable_memory_negligible() -> Rc { @@ -156,13 +167,27 @@ pub fn runnable_memory_substantial_sum( } } +pub fn resolve_scope_eq(left: ResolveScope, right: ResolveScope) -> bool { + match left { + ResolveScope::ResolveScopeIsolated => match right { + ResolveScope::ResolveScopeIsolated => true, + ResolveScope::ResolveScopeShared => false, + }, + ResolveScope::ResolveScopeShared => match right { + ResolveScope::ResolveScopeIsolated => false, + ResolveScope::ResolveScopeShared => true, + }, + } +} + pub fn runnable_resource_profile_eq( left: Rc, right: Rc, ) -> bool { - (((left.heavy_whole_tree_resolve.clone() == right.heavy_whole_tree_resolve.clone()) + ((((left.heavy_whole_tree_resolve.clone() == right.heavy_whole_tree_resolve.clone()) && (left.spawns_host_compiler.clone() == right.spawns_host_compiler.clone())) && runnable_memory_class_eq(left.memory.clone(), right.memory.clone())) + && resolve_scope_eq(left.resolve_scope.clone(), right.resolve_scope.clone())) } pub fn runnable_resource_profile_negligible() -> Rc { @@ -170,6 +195,7 @@ pub fn runnable_resource_profile_negligible() -> Rc { heavy_whole_tree_resolve: false, spawns_host_compiler: false, memory: runnable_memory_negligible(), + resolve_scope: ResolveScope::ResolveScopeIsolated, }) } @@ -177,14 +203,27 @@ pub fn runnable_resource_profile( heavy_whole_tree_resolve: bool, spawns_host_compiler: bool, memory: Rc, + resolve_scope: ResolveScope, ) -> Rc { Rc::new(RunnableResourceProfile { heavy_whole_tree_resolve: heavy_whole_tree_resolve, spawns_host_compiler: spawns_host_compiler, memory: memory, + resolve_scope: resolve_scope, }) } +pub fn runnable_profile_resolve_scope_valid(profile: Rc) -> bool { + if profile.heavy_whole_tree_resolve.clone() { + match profile.resolve_scope.clone() { + ResolveScope::ResolveScopeShared => true, + ResolveScope::ResolveScopeIsolated => false, + } + } else { + true + } +} + pub fn runnable_excludes_corpus_co_residence(profile: Rc) -> bool { match (*profile.memory.clone()).clone() { RunnableMemoryClass::RunnableMemoryNegligible => false, @@ -227,6 +266,32 @@ pub fn runnable_forbids_corpus_co_residence(r: Rc) -> bool { } } +pub fn runnable_resolve_scope_valid(r: Rc) -> bool { + runnable_profile_resolve_scope_valid(runnable_profile(r)) +} + +pub fn batch_all_resolve_scope_valid(batch: Rc>>) -> bool { + if batch.is_empty() { + true + } else { + runnable_resolve_scope_valid(batch[0].clone()) + && batch_all_resolve_scope_valid(Rc::new(batch[1..].to_vec())) + } +} + +pub fn schedule_list_all_resolve_scope_valid(sched: Schedule) -> bool { + if sched.is_empty() { + true + } else { + batch_all_resolve_scope_valid(sched[0].clone()) + && schedule_list_all_resolve_scope_valid(Rc::new(sched[1..].to_vec())) + } +} + +pub fn schedule_all_runnables_valid_resolve_scope(plan: Rc>) -> bool { + schedule_list_all_resolve_scope_valid((*plan.schedule).clone()) +} + #[derive(Debug, Clone, PartialEq, serde::Serialize, serde::Deserialize)] #[serde(tag = "_variant")] pub enum Runnable { From b0dfa852345a468fc529ec82623d27efcbbe9676 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Tue, 30 Jun 2026 12:35:29 +0000 Subject: [PATCH 14/25] M1 within-walk resolve memo: fix Runnable pattern exhaustiveness Co-Authored-By: Claude Sonnet 4.6 --- src/v1/stage0/src/bin/claim_executor.rs | 104 ++++++++++++++++++++++-- 1 file changed, 95 insertions(+), 9 deletions(-) diff --git a/src/v1/stage0/src/bin/claim_executor.rs b/src/v1/stage0/src/bin/claim_executor.rs index 09cf7e483b1..ab9bf41e24d 100644 --- a/src/v1/stage0/src/bin/claim_executor.rs +++ b/src/v1/stage0/src/bin/claim_executor.rs @@ -293,7 +293,7 @@ fn group_batch_units(batch: &[Runnable]) -> Vec { std::collections::HashMap::new(); for runnable in batch { match runnable { - Runnable::SingleClaim { entry, function } if entry.is_empty() => { + Runnable::SingleClaim { entry, function, .. } if entry.is_empty() => { units.push(BatchUnit::UnrunnableSentinel { function: function.clone(), }); @@ -469,6 +469,66 @@ fn run_shared_entry_claims( .collect() } +/// Run claims whose entry-graph is already resolved and cached in `memo`, resolving on first miss. +/// Runs on the main thread so `InterpContext` (which contains `Rc` fields) never crosses thread +/// boundaries. Subsequent callers for the same entry share the cached context — resolve runs once. +fn run_memo_shared_claims( + source_roots: &[String], + entry: &str, + functions: &[String], + memo: &mut std::collections::HashMap, +) -> Vec { + let resolve_start = Instant::now(); + let mut fresh_resolve = false; + if !memo.contains_key(entry) { + let (graph, source_indices) = match resolve_entry_graph(source_roots, entry) { + Ok(pair) => pair, + Err(msg) => { + return functions + .iter() + .map(|function| ClaimResult { + function: function.clone(), + ok: false, + detail: format!("resolve failed for {}: {}", entry, msg), + wall_nanos: 0, + resolve_nanos: 0, + corpus_resolve_nanos: 0, + corpus_eval_nanos: 0, + corpus_witnesses: 0, + }) + .collect(); + } + }; + memo.insert( + entry.to_string(), + make_eval_context(&graph, source_indices, ExecutionMode::Wet), + ); + fresh_resolve = true; + } + let resolve_nanos = if fresh_resolve { + resolve_start.elapsed().as_nanos() + } else { + 0 + }; + let ctx = memo.get(entry).expect("memo populated above"); + let mut first = fresh_resolve; + functions + .iter() + .map(|function| { + let claim_start = Instant::now(); + let outcome = run_claim(ctx, function); + let wall_nanos = claim_start.elapsed().as_nanos(); + let rn = if first { + first = false; + resolve_nanos + } else { + 0 + }; + claim_result_for_outcome(function.clone(), outcome, wall_nanos, rn) + }) + .collect() +} + /// The medium's `Viewport.width` for boxed output. The seed sources the runtime value from the host /// (`COLUMNS` when present) and passes it into the `.dag` render model; the model owns how width /// shapes the box. Conservative 88-col default fits common CI-log and chat viewers; clamped so a @@ -1230,6 +1290,12 @@ fn run_walk(source_roots: &[String], batches: &[Vec], spawn_width: usi let mut batches_run = 0usize; let walk_start = Instant::now(); let mut batch_records: Vec = Vec::new(); + // Cross-batch resolve memo: SharedClaims that declare ResolveScopeShared run on the main + // thread and share a single resolved InterpContext per (source_roots, entry) pair across all + // batches. Rc is !Send so these units cannot run on spawned threads; they + // run sequentially here after the spawned (non-memo) threads in each batch are joined. + let mut walk_memo: std::collections::HashMap = + std::collections::HashMap::new(); for (bi, batch) in batches.iter().enumerate() { batches_run = bi + 1; let units = group_batch_units(batch); @@ -1241,6 +1307,15 @@ fn run_walk(source_roots: &[String], batches: &[Vec], spawn_width: usi width ); let batch_start = Instant::now(); + // Partition units: memo units stay on the main thread; others spawn. + let mut memo_units: Vec = Vec::new(); + let mut thread_units: Vec = Vec::new(); + for unit in units { + match &unit { + BatchUnit::SharedClaims { use_walk_memo: true, .. } => memo_units.push(unit), + _ => thread_units.push(unit), + } + } // Bracket the parallel walk in a host-effect group: the `[file]`/`[rest]`/ // `[shell]` trace lines stream to stderr from the worker threads INSIDE the // group, while the scannable PASS/FAIL summary is deferred to AFTER the group @@ -1252,16 +1327,25 @@ fn run_walk(source_roots: &[String], batches: &[Vec], spawn_width: usi if grouped { v1_compiler::v1_interpreter::group_begin(&format!("batch {} host-effects", bi + 1)); } - let handles: Vec<_> = units + let handles: Vec<_> = thread_units .into_iter() .map(|unit| { let roots = source_roots.to_vec(); thread::spawn(move || run_batch_unit(roots, unit, width)) }) .collect(); + // Run memo units on the main thread while spawned threads are working. + let mut memo_results: Vec = Vec::new(); + for unit in memo_units { + if let BatchUnit::SharedClaims { entry, functions, .. } = unit { + let results = + run_memo_shared_claims(source_roots, &entry, &functions, &mut walk_memo); + memo_results.extend(results); + } + } // Collect all results before printing any PASS/FAIL — the prints must land // after `group_end`, and a thread panic still has to close the group. - let mut batch_results: Vec = Vec::new(); + let mut batch_results: Vec = memo_results; let mut thread_panicked = false; for handle in handles { match handle.join() { @@ -1417,7 +1501,7 @@ fn run_perturb_check( return Err(ExitCode::from(2)); } let (gating_entry, gating_function) = match batches[0].first() { - Some(Runnable::SingleClaim { entry, function }) if !entry.is_empty() => { + Some(Runnable::SingleClaim { entry, function, .. }) if !entry.is_empty() => { (entry.clone(), function.clone()) } _ => { @@ -1458,7 +1542,7 @@ fn run_perturb_check( batch .iter() .map(|r| match r { - Runnable::SingleClaim { entry, function } => Runnable::SingleClaim { + Runnable::SingleClaim { entry, function, use_walk_memo } => Runnable::SingleClaim { entry: if entry.is_empty() { entry.clone() } else { @@ -1467,6 +1551,7 @@ fn run_perturb_check( .into_owned() }, function: function.clone(), + use_walk_memo: *use_walk_memo, }, Runnable::DiscoveryBatch { source_roots: roots, @@ -1691,6 +1776,7 @@ mod tests { Runnable::SingleClaim { entry: entry.to_string(), function: function.to_string(), + use_walk_memo: false, } } @@ -1714,7 +1800,7 @@ mod tests { let mut out = Vec::new(); for unit in units { match unit { - BatchUnit::SharedClaims { entry, functions } => { + BatchUnit::SharedClaims { entry, functions, .. } => { for f in functions { out.push((entry.clone(), f.clone())); } @@ -1744,7 +1830,7 @@ mod tests { "three same-entry claims => one resolve-group" ); match &units[0] { - BatchUnit::SharedClaims { entry, functions } => { + BatchUnit::SharedClaims { entry, functions, .. } => { assert_eq!(entry, "gate.dag"); assert_eq!(functions, &["rust_gate", "emit_gate", "layering_gate"]); } @@ -1783,7 +1869,7 @@ mod tests { let a = units .iter() .find_map(|u| match u { - BatchUnit::SharedClaims { entry, functions } if entry == "a.dag" => Some(functions), + BatchUnit::SharedClaims { entry, functions, .. } if entry == "a.dag" => Some(functions), _ => None, }) .expect("a.dag group present"); @@ -1828,7 +1914,7 @@ mod tests { let gate = units .iter() .find_map(|u| match u { - BatchUnit::SharedClaims { entry, functions } if entry == "gate.dag" => { + BatchUnit::SharedClaims { entry, functions, .. } if entry == "gate.dag" => { Some(functions) } _ => None, From ccfa5ea37b0aa3ff8369faa52e87da1e24cce2db Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Tue, 30 Jun 2026 12:42:03 +0000 Subject: [PATCH 15/25] M1 resolve scope: add discriminating witnesses to ci_floor_plan GREEN: all heavy runnables in the plan declare ResolveScopeShared. RED: a heavy profile with ResolveScopeIsolated fails the lens. Co-Authored-By: Claude Sonnet 4.6 --- src/v2/test/claim/ci_floor_plan_witness_test.dag | 6 +++++- src/v2/workflow/ci_floor_plan.dag | 16 ++++++++++++++++ 2 files changed, 21 insertions(+), 1 deletion(-) diff --git a/src/v2/test/claim/ci_floor_plan_witness_test.dag b/src/v2/test/claim/ci_floor_plan_witness_test.dag index 460b51609e3..11aef01f400 100644 --- a/src/v2/test/claim/ci_floor_plan_witness_test.dag +++ b/src/v2/test/claim/ci_floor_plan_witness_test.dag @@ -23,6 +23,8 @@ import v2.workflow.ci_floor_plan { witness_execution_corpus_spawn_width_at_runner_cap, witness_plan_spawn_width_is_max_floor_exec_at_runner_cap, witness_floor_derived_width_leaves_headroom_at_cap, + witness_all_heavy_runnables_declare_shared_scope, + witness_heavy_scope_lens_rejects_isolated_profile, } import gunbc.ci_layer_roots { witness_discovery_scan_dirs, witness_layer_roots } import gunbc.ci_spec { gunbc_ci_spec, EmitHostGate, LayeringImportsGate } @@ -154,7 +156,9 @@ test fn ci_floor_plan_witnesses() -> Bool { witness_emit_host_isolated_from_corpus() && witness_emit_host_co_runs_corpus_without_serialization() && witness_emit_host_profile_forbids_corpus_co_residence() && - witness_light_gate_profile_allows_corpus_co_residence() + witness_light_gate_profile_allows_corpus_co_residence() && + witness_all_heavy_runnables_declare_shared_scope() && + witness_heavy_scope_lens_rejects_isolated_profile() } test fn ci_floor_run_envelope_witnesses() -> Bool { diff --git a/src/v2/workflow/ci_floor_plan.dag b/src/v2/workflow/ci_floor_plan.dag index 7c0c21cfb1d..a56cb909081 100644 --- a/src/v2/workflow/ci_floor_plan.dag +++ b/src/v2/workflow/ci_floor_plan.dag @@ -51,6 +51,8 @@ import std.realization_schedule { runnable_excludes_corpus_co_residence, runnable_heavy_whole_tree_resolve, runnable_forbids_corpus_co_residence, + runnable_profile_resolve_scope_valid, + schedule_all_runnables_valid_resolve_scope, cost_account_predicted_zero, schedule_lens_verdict_for_ci_floor } @@ -555,3 +557,17 @@ fn witness_floor_derived_width_leaves_headroom_at_cap() -> Bool { let committed = byte_size_count(b: gunbc_ci_floor_per_shard_peak_rss_bytes()) * width committed < byte_size_count(b: gunbc_ci_runner_cgroup_memory_cap) } + +fn witness_all_heavy_runnables_declare_shared_scope() -> Bool { + schedule_all_runnables_valid_resolve_scope(plan: gunbc_ci_floor_realization_plan()) +} + +fn witness_heavy_scope_lens_rejects_isolated_profile() -> Bool { + let bad_profile = runnable_resource_profile( + heavy_whole_tree_resolve: true, + spawns_host_compiler: false, + memory: runnable_memory_negligible(), + resolve_scope: ResolveScopeIsolated + ) + !runnable_profile_resolve_scope_valid(profile: bad_profile) +} From dadcd26e13068f5c17c64ed7579fa4aa52e1cb2c Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Tue, 30 Jun 2026 12:51:01 +0000 Subject: [PATCH 16/25] WIP: DESIGN SKETCH ONLY (no code; returns to stern-moth-225 + operator before --- src/v1/stage0/src/bin/claim_executor.rs | 133 ++++++++++++++---- src/v1/stage0/src/std_realization_schedule.rs | 2 +- 2 files changed, 105 insertions(+), 30 deletions(-) diff --git a/src/v1/stage0/src/bin/claim_executor.rs b/src/v1/stage0/src/bin/claim_executor.rs index ab9bf41e24d..22a823238bc 100644 --- a/src/v1/stage0/src/bin/claim_executor.rs +++ b/src/v1/stage0/src/bin/claim_executor.rs @@ -9,9 +9,9 @@ use std::time::Instant; use v1_compiler::cli_run::{ compute_histogram_data, compute_witness_timing_rows, make_eval_context, resolve_entry_graph, - run_claim, run_discovery_corpus_with_options, run_value, top_n_slowest_witnesses, ClaimOutcome, - DiscoveryCorpusOptions, DiscoverySummary, HistogramData, TimingPercentiles, WitnessTimingRow, - DEFAULT_SLOWEST_WITNESS_ATTRIBUTION_N, + run_claim, run_discovery_corpus_with_options, run_value, top_n_slowest_witnesses, + workspace_root, ClaimOutcome, DiscoveryCorpusOptions, DiscoverySummary, HistogramData, + TimingPercentiles, WitnessTimingRow, DEFAULT_SLOWEST_WITNESS_ATTRIBUTION_N, }; use v1_compiler::v1_interpreter::{ color_enabled, paint, run_in_context_with_args, sgr, ExecutionMode, InterpContext, Value, @@ -131,17 +131,20 @@ fn runnable_from_value(value: &Value, ctx: &InterpContext) -> Result { - match ctx.field(pf, "resolve_scope") { - Some(Value::Variant { variant_name: vn, .. }) => { - ctx.sym_eq(*vn, "ResolveScopeShared") - } - _ => false, - } - } + Some(Value::Record { fields: pf, .. }) + | Some(Value::Variant { fields: pf, .. }) => match ctx.field(pf, "resolve_scope") { + Some(Value::Variant { + variant_name: vn, .. + }) => ctx.sym_eq(*vn, "ResolveScopeShared"), + _ => false, + }, _ => false, }; - Ok(Runnable::SingleClaim { entry, function, use_walk_memo }) + Ok(Runnable::SingleClaim { + entry, + function, + use_walk_memo, + }) } Value::Variant { variant_name, @@ -293,12 +296,18 @@ fn group_batch_units(batch: &[Runnable]) -> Vec { std::collections::HashMap::new(); for runnable in batch { match runnable { - Runnable::SingleClaim { entry, function, .. } if entry.is_empty() => { + Runnable::SingleClaim { + entry, function, .. + } if entry.is_empty() => { units.push(BatchUnit::UnrunnableSentinel { function: function.clone(), }); } - Runnable::SingleClaim { entry, function, use_walk_memo } => { + Runnable::SingleClaim { + entry, + function, + use_walk_memo, + } => { if let Some(&idx) = entry_to_unit.get(entry) { if let BatchUnit::SharedClaims { functions, .. } = &mut units[idx] { functions.push(function.clone()); @@ -419,9 +428,9 @@ fn run_batch_unit( spawn_width, spawn_width_cap, )], - BatchUnit::SharedClaims { entry, functions, .. } => { - run_shared_entry_claims(&source_roots, &entry, &functions) - } + BatchUnit::SharedClaims { + entry, functions, .. + } => run_shared_entry_claims(&source_roots, &entry, &functions), } } @@ -1312,7 +1321,10 @@ fn run_walk(source_roots: &[String], batches: &[Vec], spawn_width: usi let mut thread_units: Vec = Vec::new(); for unit in units { match &unit { - BatchUnit::SharedClaims { use_walk_memo: true, .. } => memo_units.push(unit), + BatchUnit::SharedClaims { + use_walk_memo: true, + .. + } => memo_units.push(unit), _ => thread_units.push(unit), } } @@ -1337,7 +1349,10 @@ fn run_walk(source_roots: &[String], batches: &[Vec], spawn_width: usi // Run memo units on the main thread while spawned threads are working. let mut memo_results: Vec = Vec::new(); for unit in memo_units { - if let BatchUnit::SharedClaims { entry, functions, .. } = unit { + if let BatchUnit::SharedClaims { + entry, functions, .. + } = unit + { let results = run_memo_shared_claims(source_roots, &entry, &functions, &mut walk_memo); memo_results.extend(results); @@ -1501,9 +1516,9 @@ fn run_perturb_check( return Err(ExitCode::from(2)); } let (gating_entry, gating_function) = match batches[0].first() { - Some(Runnable::SingleClaim { entry, function, .. }) if !entry.is_empty() => { - (entry.clone(), function.clone()) - } + Some(Runnable::SingleClaim { + entry, function, .. + }) if !entry.is_empty() => (entry.clone(), function.clone()), _ => { eprintln!( "claim_executor: --perturb-check: batch 1 has no plantable SingleClaim gating node" @@ -1542,7 +1557,11 @@ fn run_perturb_check( batch .iter() .map(|r| match r { - Runnable::SingleClaim { entry, function, use_walk_memo } => Runnable::SingleClaim { + Runnable::SingleClaim { + entry, + function, + use_walk_memo, + } => Runnable::SingleClaim { entry: if entry.is_empty() { entry.clone() } else { @@ -1800,7 +1819,9 @@ mod tests { let mut out = Vec::new(); for unit in units { match unit { - BatchUnit::SharedClaims { entry, functions, .. } => { + BatchUnit::SharedClaims { + entry, functions, .. + } => { for f in functions { out.push((entry.clone(), f.clone())); } @@ -1830,7 +1851,9 @@ mod tests { "three same-entry claims => one resolve-group" ); match &units[0] { - BatchUnit::SharedClaims { entry, functions, .. } => { + BatchUnit::SharedClaims { + entry, functions, .. + } => { assert_eq!(entry, "gate.dag"); assert_eq!(functions, &["rust_gate", "emit_gate", "layering_gate"]); } @@ -1869,7 +1892,9 @@ mod tests { let a = units .iter() .find_map(|u| match u { - BatchUnit::SharedClaims { entry, functions, .. } if entry == "a.dag" => Some(functions), + BatchUnit::SharedClaims { + entry, functions, .. + } if entry == "a.dag" => Some(functions), _ => None, }) .expect("a.dag group present"); @@ -1914,9 +1939,9 @@ mod tests { let gate = units .iter() .find_map(|u| match u { - BatchUnit::SharedClaims { entry, functions, .. } if entry == "gate.dag" => { - Some(functions) - } + BatchUnit::SharedClaims { + entry, functions, .. + } if entry == "gate.dag" => Some(functions), _ => None, }) .expect("gate group present"); @@ -1984,4 +2009,54 @@ mod tests { "no declared artifacts is a usage error, fail closed" ); } + + /// Warm==cold purity oracle for the cross-batch resolve memo (DESIGN §5). + /// + /// Proves that `run_memo_shared_claims` (warm path: 2nd+ calls share the cached + /// `InterpContext`) produces byte-identical `(function, ok, detail)` results vs + /// `run_shared_entry_claims` (cold path: fresh resolve each time). Goes RED if + /// the shared `InterpContext` has interior mutability that contaminates results + /// across claims — the failure mode the declaration-validity lenses cannot catch. + #[test] + fn memo_warm_cold_results_are_identical() { + let root = workspace_root(); + let source_roots = vec![ + root.join("src/v2").to_string_lossy().into_owned(), + root.join("dsl").to_string_lossy().into_owned(), + ]; + let entry = root + .join("dsl/test/claim/runnable_resource_profile_witness_test.dag") + .to_string_lossy() + .into_owned(); + let functions = vec![ + "witness_negligible_profile_is_not_heavy".to_string(), + "witness_substantial_memory_forbids_corpus_co_residence".to_string(), + ]; + + // Cold path: two independent resolves, one function each. + let cold: Vec<(String, bool, String)> = functions + .iter() + .flat_map(|f| { + run_shared_entry_claims(&source_roots, &entry, std::slice::from_ref(f)) + .into_iter() + .map(|r| (r.function, r.ok, r.detail)) + }) + .collect(); + + // Warm path: single memo, first call resolves fresh, second hits the cache. + let mut memo = std::collections::HashMap::new(); + let warm: Vec<(String, bool, String)> = functions + .iter() + .flat_map(|f| { + run_memo_shared_claims(&source_roots, &entry, std::slice::from_ref(f), &mut memo) + .into_iter() + .map(|r| (r.function, r.ok, r.detail)) + }) + .collect(); + + assert_eq!( + warm, cold, + "memo warm path must be byte-identical to cold path — shared InterpContext is pure" + ); + } } diff --git a/src/v1/stage0/src/std_realization_schedule.rs b/src/v1/stage0/src/std_realization_schedule.rs index f502bc826e9..9a03b7006eb 100644 --- a/src/v1/stage0/src/std_realization_schedule.rs +++ b/src/v1/stage0/src/std_realization_schedule.rs @@ -2,9 +2,9 @@ // Source module: std.realization_schedule use self::CostBasis::*; +use self::ResolveScope::*; use self::Runnable::*; use self::RunnableMemoryClass::*; -use self::ResolveScope::*; use self::ScheduleLensViolation::*; use crate::std_lens_verdict::LensVerdict::{Holds, Violation}; use crate::std_lens_verdict::LensVerdictLocus::ModuleWholeFile; From 97ef8c1990477bbec485d19740856ed7cb9d8b79 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Tue, 30 Jun 2026 12:54:00 +0000 Subject: [PATCH 17/25] fix: OR use_walk_memo on SharedClaims merge; document source_roots invariant When group_batch_units merges a ResolveScopeShared SingleClaim into an existing SharedClaims unit that was created from an Isolated claim first, the group would silently drop the Shared flag and run via run_shared_entry_claims instead of the cross-batch memo path. Fix by ORing use_walk_memo on merge so the memo path wins whenever any member of the group declares ResolveScopeShared. Also document the memo-key invariant: source_roots is constant per run_walk call, so keying the memo by entry alone is safe today; notes what to change if that assumption ever widens. Co-Authored-By: Claude Sonnet 4.6 --- src/v1/stage0/src/bin/claim_executor.rs | 20 +++++++++++++++++--- 1 file changed, 17 insertions(+), 3 deletions(-) diff --git a/src/v1/stage0/src/bin/claim_executor.rs b/src/v1/stage0/src/bin/claim_executor.rs index 22a823238bc..b036f40c448 100644 --- a/src/v1/stage0/src/bin/claim_executor.rs +++ b/src/v1/stage0/src/bin/claim_executor.rs @@ -309,8 +309,18 @@ fn group_batch_units(batch: &[Runnable]) -> Vec { use_walk_memo, } => { if let Some(&idx) = entry_to_unit.get(entry) { - if let BatchUnit::SharedClaims { functions, .. } = &mut units[idx] { + if let BatchUnit::SharedClaims { + functions, + use_walk_memo: existing_memo, + .. + } = &mut units[idx] + { functions.push(function.clone()); + // A ResolveScopeShared claim may merge into a group that + // was created from a ResolveScopeIsolated claim first; OR + // here so the group gets the memo path if any member + // declared Shared. + *existing_memo |= use_walk_memo; } } else { entry_to_unit.insert(entry.clone(), units.len()); @@ -1300,9 +1310,13 @@ fn run_walk(source_roots: &[String], batches: &[Vec], spawn_width: usi let walk_start = Instant::now(); let mut batch_records: Vec = Vec::new(); // Cross-batch resolve memo: SharedClaims that declare ResolveScopeShared run on the main - // thread and share a single resolved InterpContext per (source_roots, entry) pair across all - // batches. Rc is !Send so these units cannot run on spawned threads; they + // thread and share a single resolved InterpContext per entry across all batches. + // Rc is !Send so these units cannot run on spawned threads; they // run sequentially here after the spawned (non-memo) threads in each batch are joined. + // Key invariant: source_roots is constant for the lifetime of a run_walk call, so + // keying the memo by entry alone is sufficient — a given entry always resolves against + // the same source_roots here. If this function ever accepts multiple source_root sets, + // the key must become (source_roots_hash, entry). let mut walk_memo: std::collections::HashMap = std::collections::HashMap::new(); for (bi, batch) in batches.iter().enumerate() { From 0bd564bd695955bd9388f3fcfe084c6996a9e41f Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Tue, 30 Jun 2026 12:56:16 +0000 Subject: [PATCH 18/25] fix: gate workspace_root import under #[cfg(test)] to clear unused-import clippy error Co-Authored-By: Claude Sonnet 4.6 --- src/v1/stage0/src/bin/claim_executor.rs | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/src/v1/stage0/src/bin/claim_executor.rs b/src/v1/stage0/src/bin/claim_executor.rs index b036f40c448..10e07b92bc1 100644 --- a/src/v1/stage0/src/bin/claim_executor.rs +++ b/src/v1/stage0/src/bin/claim_executor.rs @@ -7,11 +7,13 @@ use std::rc::Rc; use std::thread; use std::time::Instant; +#[cfg(test)] +use v1_compiler::cli_run::workspace_root; use v1_compiler::cli_run::{ compute_histogram_data, compute_witness_timing_rows, make_eval_context, resolve_entry_graph, - run_claim, run_discovery_corpus_with_options, run_value, top_n_slowest_witnesses, - workspace_root, ClaimOutcome, DiscoveryCorpusOptions, DiscoverySummary, HistogramData, - TimingPercentiles, WitnessTimingRow, DEFAULT_SLOWEST_WITNESS_ATTRIBUTION_N, + run_claim, run_discovery_corpus_with_options, run_value, top_n_slowest_witnesses, ClaimOutcome, + DiscoveryCorpusOptions, DiscoverySummary, HistogramData, TimingPercentiles, WitnessTimingRow, + DEFAULT_SLOWEST_WITNESS_ATTRIBUTION_N, }; use v1_compiler::v1_interpreter::{ color_enabled, paint, run_in_context_with_args, sgr, ExecutionMode, InterpContext, Value, From 89ecbc76c9c69b7898cdf9171e63dbf1d2329e67 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Tue, 30 Jun 2026 13:04:36 +0000 Subject: [PATCH 19/25] fix: replace vec! with array literal in warm==cold test to silence clippy Co-Authored-By: Claude Sonnet 4.6 --- src/v1/stage0/src/bin/claim_executor.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/v1/stage0/src/bin/claim_executor.rs b/src/v1/stage0/src/bin/claim_executor.rs index 10e07b92bc1..0668a448316 100644 --- a/src/v1/stage0/src/bin/claim_executor.rs +++ b/src/v1/stage0/src/bin/claim_executor.rs @@ -2044,7 +2044,7 @@ mod tests { .join("dsl/test/claim/runnable_resource_profile_witness_test.dag") .to_string_lossy() .into_owned(); - let functions = vec![ + let functions: &[String] = &[ "witness_negligible_profile_is_not_heavy".to_string(), "witness_substantial_memory_forbids_corpus_co_residence".to_string(), ]; From d662a7ae2db83296e089e81e385d5c1dc0454572 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Tue, 30 Jun 2026 13:19:31 +0000 Subject: [PATCH 20/25] WIP: DESIGN SKETCH ONLY (no code; returns to stern-moth-225 + operator before --- dsl/std/realization_schedule.dag | 61 +------------------------------- 1 file changed, 1 insertion(+), 60 deletions(-) diff --git a/dsl/std/realization_schedule.dag b/dsl/std/realization_schedule.dag index 598a2bcc22b..66b654592d8 100644 --- a/dsl/std/realization_schedule.dag +++ b/dsl/std/realization_schedule.dag @@ -65,15 +65,10 @@ type RunnableMemoryClass = RunnableMemoryNegligible | RunnableMemorySubstantial { peak: RunnableMemoryPeak } -type ResolveScope - = ResolveScopeIsolated - | ResolveScopeShared - type RunnableResourceProfile { heavy_whole_tree_resolve: Bool spawns_host_compiler: Bool memory: RunnableMemoryClass - resolve_scope: ResolveScope } fn runnable_memory_negligible() -> RunnableMemoryClass { @@ -112,24 +107,10 @@ fn runnable_memory_substantial_sum(left: RunnableMemoryClass, right: RunnableMem runnable_memory_substantial(predicted_peak: byte_size(count: left_count + right_count)) } -fn resolve_scope_eq(left: ResolveScope, right: ResolveScope) -> Bool { - match left { - ResolveScopeIsolated => match right { - ResolveScopeIsolated => true - ResolveScopeShared => false - } - ResolveScopeShared => match right { - ResolveScopeIsolated => false - ResolveScopeShared => true - } - } -} - fn runnable_resource_profile_eq(left: RunnableResourceProfile, right: RunnableResourceProfile) -> Bool { (left.heavy_whole_tree_resolve == right.heavy_whole_tree_resolve) && (left.spawns_host_compiler == right.spawns_host_compiler) && runnable_memory_class_eq(left: left.memory, right: right.memory) - && resolve_scope_eq(left: left.resolve_scope, right: right.resolve_scope) } fn runnable_resource_profile_negligible() -> RunnableResourceProfile { @@ -137,32 +118,18 @@ fn runnable_resource_profile_negligible() -> RunnableResourceProfile { heavy_whole_tree_resolve: false spawns_host_compiler: false memory: runnable_memory_negligible() - resolve_scope: ResolveScopeIsolated } } fn runnable_resource_profile( heavy_whole_tree_resolve: Bool, spawns_host_compiler: Bool, - memory: RunnableMemoryClass, - resolve_scope: ResolveScope + memory: RunnableMemoryClass ) -> RunnableResourceProfile { RunnableResourceProfile { heavy_whole_tree_resolve: heavy_whole_tree_resolve spawns_host_compiler: spawns_host_compiler memory: memory - resolve_scope: resolve_scope - } -} - -fn runnable_profile_resolve_scope_valid(profile: RunnableResourceProfile) -> Bool { - if profile.heavy_whole_tree_resolve { - match profile.resolve_scope { - ResolveScopeShared => true - ResolveScopeIsolated => false - } - } else { - true } } @@ -216,19 +183,6 @@ type Runnable data runnable_kernel_workload_dissolution_trigger: String = "dissolve-on: execution lane attaches extdeps.languages kernel_surface rows to RunnableKernelWorkload when fused_op_count alone is insufficient; op_count is structural on substrate (not a string-label nickname)." -fn runnable_resolve_scope_valid(r: Runnable) -> Bool { - runnable_profile_resolve_scope_valid(profile: runnable_profile(r: r)) -} - -fn batch_all_resolve_scope_valid(batch: List) -> Bool { - if batch.count() == 0 { - true - } else { - runnable_resolve_scope_valid(r: batch.first()) && - batch_all_resolve_scope_valid(batch: batch.skip(n: 1)) - } -} - type Schedule = List> type RealizationPlan { @@ -239,19 +193,6 @@ type RealizationPlan { total: CostAccount } -fn schedule_list_all_resolve_scope_valid(sched: Schedule) -> Bool { - if sched.count() == 0 { - true - } else { - batch_all_resolve_scope_valid(batch: sched.first()) && - schedule_list_all_resolve_scope_valid(sched: sched.skip(n: 1)) - } -} - -fn schedule_all_runnables_valid_resolve_scope(plan: RealizationPlan) -> Bool { - schedule_list_all_resolve_scope_valid(sched: plan.schedule) -} - fn runnable_step_label(r: Runnable) -> String { match r { RunnableSingleClaim { entry: _, function: f, profile: _ } => f From cf84c60c113374463f222a0fd415c1acb6e340ff Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Tue, 30 Jun 2026 13:23:37 +0000 Subject: [PATCH 21/25] =?UTF-8?q?=C2=A75=20construction:=20drop=20resolve?= =?UTF-8?q?=5Fscope=20=E2=80=94=20derive=20memo=20from=20heavy=5Fwhole=5Ft?= =?UTF-8?q?ree=5Fresolve?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit heavy_whole_tree_resolve is the single authority (§3). The memo decision follows by law: a whole-tree resolve is deterministic per source_roots, so heavy⟹memoize is always true. Two independent axes with one combination forbidden was validation-where-construction-was-available (DESIGN §5). Removes: type ResolveScope, resolve_scope field on RunnableResourceProfile, resolve_scope_eq, runnable_profile_resolve_scope_valid, and the three schedule walkers (runnable_resolve_scope_valid, batch_all_resolve_scope_valid, schedule_list_all_resolve_scope_valid, schedule_all_runnables_valid_resolve_scope). These dissolve — HeavyIsolated is now unwritable by construction, so the validator and witnesses testing it are unnecessary. claim_executor.rs derives use_walk_memo from profile.heavy_whole_tree_resolve directly (single read site, no gate list). Co-Authored-By: Claude Sonnet 4.6 --- ...runnable_resource_profile_witness_test.dag | 10 +-- src/v1/stage0/src/bin/claim_executor.rs | 12 +-- src/v1/stage0/src/std_realization_schedule.rs | 73 +------------------ .../test/claim/ci_floor_plan_witness_test.dag | 6 +- src/v2/workflow/ci_floor_plan.dag | 39 ++-------- 5 files changed, 21 insertions(+), 119 deletions(-) diff --git a/dsl/test/claim/runnable_resource_profile_witness_test.dag b/dsl/test/claim/runnable_resource_profile_witness_test.dag index 20bc8880a59..91a87a0fb63 100644 --- a/dsl/test/claim/runnable_resource_profile_witness_test.dag +++ b/dsl/test/claim/runnable_resource_profile_witness_test.dag @@ -4,7 +4,6 @@ import std.realization_schedule { Runnable, RunnableSingleClaim, RunnableDiscoveryBatch, - ResolveScopeIsolated, runnable_resource_profile, runnable_resource_profile_negligible, runnable_memory_substantial, @@ -26,8 +25,7 @@ fn witness_substantial_memory_forbids_corpus_co_residence() -> Bool { profile: runnable_resource_profile( heavy_whole_tree_resolve: false, spawns_host_compiler: false, - memory: runnable_memory_substantial(predicted_peak: byte_size(count: 1)), - resolve_scope: ResolveScopeIsolated + memory: runnable_memory_substantial(predicted_peak: byte_size(count: 1)) ) } runnable_forbids_corpus_co_residence(r: heavy) @@ -42,8 +40,7 @@ fn witness_corpus_never_forbids_co_residence() -> Bool { profile: runnable_resource_profile( heavy_whole_tree_resolve: true, spawns_host_compiler: false, - memory: runnable_memory_substantial(predicted_peak: byte_size(count: 3226056704)), - resolve_scope: ResolveScopeIsolated + memory: runnable_memory_substantial(predicted_peak: byte_size(count: 3226056704)) ) } !runnable_forbids_corpus_co_residence(r: corpus) @@ -56,8 +53,7 @@ fn witness_memory_sum_matches_byte_totals() -> Bool { byte_size_count(b: runnable_predicted_space(profile: runnable_resource_profile( heavy_whole_tree_resolve: false, spawns_host_compiler: false, - memory: sum, - resolve_scope: ResolveScopeIsolated + memory: sum ))) == 300 } diff --git a/src/v1/stage0/src/bin/claim_executor.rs b/src/v1/stage0/src/bin/claim_executor.rs index 0668a448316..91c361277a7 100644 --- a/src/v1/stage0/src/bin/claim_executor.rs +++ b/src/v1/stage0/src/bin/claim_executor.rs @@ -134,12 +134,12 @@ fn runnable_from_value(value: &Value, ctx: &InterpContext) -> Result match ctx.field(pf, "resolve_scope") { - Some(Value::Variant { - variant_name: vn, .. - }) => ctx.sym_eq(*vn, "ResolveScopeShared"), - _ => false, - }, + | Some(Value::Variant { fields: pf, .. }) => { + matches!( + ctx.field(pf, "heavy_whole_tree_resolve"), + Some(Value::Bool(true)) + ) + } _ => false, }; Ok(Runnable::SingleClaim { diff --git a/src/v1/stage0/src/std_realization_schedule.rs b/src/v1/stage0/src/std_realization_schedule.rs index 9a03b7006eb..7f3319048ff 100644 --- a/src/v1/stage0/src/std_realization_schedule.rs +++ b/src/v1/stage0/src/std_realization_schedule.rs @@ -2,7 +2,6 @@ // Source module: std.realization_schedule use self::CostBasis::*; -use self::ResolveScope::*; use self::Runnable::*; use self::RunnableMemoryClass::*; use self::ScheduleLensViolation::*; @@ -98,21 +97,11 @@ impl RunnableMemoryClass { } } -#[derive( - Debug, Clone, Copy, PartialEq, Eq, PartialOrd, Ord, serde::Serialize, serde::Deserialize, -)] -#[serde(tag = "_variant")] -pub enum ResolveScope { - ResolveScopeIsolated, - ResolveScopeShared, -} - #[derive(Debug, Clone, PartialEq, serde::Serialize, serde::Deserialize)] pub struct RunnableResourceProfile { pub heavy_whole_tree_resolve: bool, pub spawns_host_compiler: bool, pub memory: Rc, - pub resolve_scope: ResolveScope, } pub fn runnable_memory_negligible() -> Rc { @@ -167,27 +156,13 @@ pub fn runnable_memory_substantial_sum( } } -pub fn resolve_scope_eq(left: ResolveScope, right: ResolveScope) -> bool { - match left { - ResolveScope::ResolveScopeIsolated => match right { - ResolveScope::ResolveScopeIsolated => true, - ResolveScope::ResolveScopeShared => false, - }, - ResolveScope::ResolveScopeShared => match right { - ResolveScope::ResolveScopeIsolated => false, - ResolveScope::ResolveScopeShared => true, - }, - } -} - pub fn runnable_resource_profile_eq( left: Rc, right: Rc, ) -> bool { - ((((left.heavy_whole_tree_resolve.clone() == right.heavy_whole_tree_resolve.clone()) + (((left.heavy_whole_tree_resolve.clone() == right.heavy_whole_tree_resolve.clone()) && (left.spawns_host_compiler.clone() == right.spawns_host_compiler.clone())) && runnable_memory_class_eq(left.memory.clone(), right.memory.clone())) - && resolve_scope_eq(left.resolve_scope.clone(), right.resolve_scope.clone())) } pub fn runnable_resource_profile_negligible() -> Rc { @@ -195,7 +170,6 @@ pub fn runnable_resource_profile_negligible() -> Rc { heavy_whole_tree_resolve: false, spawns_host_compiler: false, memory: runnable_memory_negligible(), - resolve_scope: ResolveScope::ResolveScopeIsolated, }) } @@ -203,27 +177,14 @@ pub fn runnable_resource_profile( heavy_whole_tree_resolve: bool, spawns_host_compiler: bool, memory: Rc, - resolve_scope: ResolveScope, ) -> Rc { Rc::new(RunnableResourceProfile { - heavy_whole_tree_resolve: heavy_whole_tree_resolve, - spawns_host_compiler: spawns_host_compiler, - memory: memory, - resolve_scope: resolve_scope, + heavy_whole_tree_resolve, + spawns_host_compiler, + memory, }) } -pub fn runnable_profile_resolve_scope_valid(profile: Rc) -> bool { - if profile.heavy_whole_tree_resolve.clone() { - match profile.resolve_scope.clone() { - ResolveScope::ResolveScopeShared => true, - ResolveScope::ResolveScopeIsolated => false, - } - } else { - true - } -} - pub fn runnable_excludes_corpus_co_residence(profile: Rc) -> bool { match (*profile.memory.clone()).clone() { RunnableMemoryClass::RunnableMemoryNegligible => false, @@ -266,32 +227,6 @@ pub fn runnable_forbids_corpus_co_residence(r: Rc) -> bool { } } -pub fn runnable_resolve_scope_valid(r: Rc) -> bool { - runnable_profile_resolve_scope_valid(runnable_profile(r)) -} - -pub fn batch_all_resolve_scope_valid(batch: Rc>>) -> bool { - if batch.is_empty() { - true - } else { - runnable_resolve_scope_valid(batch[0].clone()) - && batch_all_resolve_scope_valid(Rc::new(batch[1..].to_vec())) - } -} - -pub fn schedule_list_all_resolve_scope_valid(sched: Schedule) -> bool { - if sched.is_empty() { - true - } else { - batch_all_resolve_scope_valid(sched[0].clone()) - && schedule_list_all_resolve_scope_valid(Rc::new(sched[1..].to_vec())) - } -} - -pub fn schedule_all_runnables_valid_resolve_scope(plan: Rc>) -> bool { - schedule_list_all_resolve_scope_valid((*plan.schedule).clone()) -} - #[derive(Debug, Clone, PartialEq, serde::Serialize, serde::Deserialize)] #[serde(tag = "_variant")] pub enum Runnable { diff --git a/src/v2/test/claim/ci_floor_plan_witness_test.dag b/src/v2/test/claim/ci_floor_plan_witness_test.dag index 11aef01f400..460b51609e3 100644 --- a/src/v2/test/claim/ci_floor_plan_witness_test.dag +++ b/src/v2/test/claim/ci_floor_plan_witness_test.dag @@ -23,8 +23,6 @@ import v2.workflow.ci_floor_plan { witness_execution_corpus_spawn_width_at_runner_cap, witness_plan_spawn_width_is_max_floor_exec_at_runner_cap, witness_floor_derived_width_leaves_headroom_at_cap, - witness_all_heavy_runnables_declare_shared_scope, - witness_heavy_scope_lens_rejects_isolated_profile, } import gunbc.ci_layer_roots { witness_discovery_scan_dirs, witness_layer_roots } import gunbc.ci_spec { gunbc_ci_spec, EmitHostGate, LayeringImportsGate } @@ -156,9 +154,7 @@ test fn ci_floor_plan_witnesses() -> Bool { witness_emit_host_isolated_from_corpus() && witness_emit_host_co_runs_corpus_without_serialization() && witness_emit_host_profile_forbids_corpus_co_residence() && - witness_light_gate_profile_allows_corpus_co_residence() && - witness_all_heavy_runnables_declare_shared_scope() && - witness_heavy_scope_lens_rejects_isolated_profile() + witness_light_gate_profile_allows_corpus_co_residence() } test fn ci_floor_run_envelope_witnesses() -> Bool { diff --git a/src/v2/workflow/ci_floor_plan.dag b/src/v2/workflow/ci_floor_plan.dag index a56cb909081..30ddcba3567 100644 --- a/src/v2/workflow/ci_floor_plan.dag +++ b/src/v2/workflow/ci_floor_plan.dag @@ -40,9 +40,6 @@ import std.realization_schedule { RunnableSingleClaim, RunnableDiscoveryBatch, RunnableResourceProfile, - ResolveScope, - ResolveScopeShared, - ResolveScopeIsolated, runnable_resource_profile, runnable_resource_profile_negligible, runnable_memory_negligible, @@ -51,8 +48,6 @@ import std.realization_schedule { runnable_excludes_corpus_co_residence, runnable_heavy_whole_tree_resolve, runnable_forbids_corpus_co_residence, - runnable_profile_resolve_scope_valid, - schedule_all_runnables_valid_resolve_scope, cost_account_predicted_zero, schedule_lens_verdict_for_ci_floor } @@ -108,36 +103,31 @@ fn gate_runnable_profile(g: Gate) -> RunnableResourceProfile { runnable_resource_profile( heavy_whole_tree_resolve: true, spawns_host_compiler: false, - memory: per_shard, - resolve_scope: ResolveScopeShared + memory: per_shard ) SourceRootIngestGate => runnable_resource_profile( heavy_whole_tree_resolve: true, spawns_host_compiler: false, - memory: per_shard, - resolve_scope: ResolveScopeShared + memory: per_shard ) RegenVerifyGate => runnable_resource_profile( heavy_whole_tree_resolve: true, spawns_host_compiler: true, - memory: runnable_memory_substantial_sum(left: per_shard, right: host_compiler), - resolve_scope: ResolveScopeShared + memory: runnable_memory_substantial_sum(left: per_shard, right: host_compiler) ) EmitDeterminismGate => runnable_resource_profile( heavy_whole_tree_resolve: true, spawns_host_compiler: true, - memory: runnable_memory_substantial_sum(left: per_shard, right: host_compiler), - resolve_scope: ResolveScopeShared + memory: runnable_memory_substantial_sum(left: per_shard, right: host_compiler) ) EmitHostGate => runnable_resource_profile( heavy_whole_tree_resolve: false, spawns_host_compiler: true, - memory: host_compiler, - resolve_scope: ResolveScopeIsolated + memory: host_compiler ) RustMonolithGate => runnable_resource_profile_negligible() LayeringImportsGate => runnable_resource_profile_negligible() @@ -181,8 +171,7 @@ fn corpus_runnable() -> Runnable { profile: runnable_resource_profile( heavy_whole_tree_resolve: true, spawns_host_compiler: false, - memory: runnable_memory_substantial(predicted_peak: gunbc_ci_floor_per_shard_peak_rss_bytes()), - resolve_scope: ResolveScopeShared + memory: runnable_memory_substantial(predicted_peak: gunbc_ci_floor_per_shard_peak_rss_bytes()) ) } } @@ -208,8 +197,7 @@ fn execution_corpus_runnable() -> Runnable { profile: runnable_resource_profile( heavy_whole_tree_resolve: true, spawns_host_compiler: false, - memory: runnable_memory_substantial(predicted_peak: gunbc_ci_floor_execution_corpus_per_witness_rss), - resolve_scope: ResolveScopeShared + memory: runnable_memory_substantial(predicted_peak: gunbc_ci_floor_execution_corpus_per_witness_rss) ) } } @@ -558,16 +546,3 @@ fn witness_floor_derived_width_leaves_headroom_at_cap() -> Bool { committed < byte_size_count(b: gunbc_ci_runner_cgroup_memory_cap) } -fn witness_all_heavy_runnables_declare_shared_scope() -> Bool { - schedule_all_runnables_valid_resolve_scope(plan: gunbc_ci_floor_realization_plan()) -} - -fn witness_heavy_scope_lens_rejects_isolated_profile() -> Bool { - let bad_profile = runnable_resource_profile( - heavy_whole_tree_resolve: true, - spawns_host_compiler: false, - memory: runnable_memory_negligible(), - resolve_scope: ResolveScopeIsolated - ) - !runnable_profile_resolve_scope_valid(profile: bad_profile) -} From 622bfba655848e7b372d08634d81c422bf4d28e0 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Tue, 30 Jun 2026 13:25:06 +0000 Subject: [PATCH 22/25] reword stale ResolveScope vocab in two comments Co-Authored-By: Claude Sonnet 4.6 --- src/v1/stage0/src/bin/claim_executor.rs | 11 +++++------ 1 file changed, 5 insertions(+), 6 deletions(-) diff --git a/src/v1/stage0/src/bin/claim_executor.rs b/src/v1/stage0/src/bin/claim_executor.rs index 91c361277a7..43423636075 100644 --- a/src/v1/stage0/src/bin/claim_executor.rs +++ b/src/v1/stage0/src/bin/claim_executor.rs @@ -318,10 +318,9 @@ fn group_batch_units(batch: &[Runnable]) -> Vec { } = &mut units[idx] { functions.push(function.clone()); - // A ResolveScopeShared claim may merge into a group that - // was created from a ResolveScopeIsolated claim first; OR - // here so the group gets the memo path if any member - // declared Shared. + // A memo claim (heavy whole-tree resolve) may merge into a + // group created from a non-memo claim first; OR here so the + // group gets the memo path if any member is heavy. *existing_memo |= use_walk_memo; } } else { @@ -1311,8 +1310,8 @@ fn run_walk(source_roots: &[String], batches: &[Vec], spawn_width: usi let mut batches_run = 0usize; let walk_start = Instant::now(); let mut batch_records: Vec = Vec::new(); - // Cross-batch resolve memo: SharedClaims that declare ResolveScopeShared run on the main - // thread and share a single resolved InterpContext per entry across all batches. + // Cross-batch resolve memo: SharedClaims whose runnable does a heavy whole-tree resolve + // run on the main thread and share a single resolved InterpContext per entry across all batches. // Rc is !Send so these units cannot run on spawned threads; they // run sequentially here after the spawned (non-memo) threads in each batch are joined. // Key invariant: source_roots is constant for the lifetime of a run_walk call, so From 238e50b723478ac8eec2d26c73bf9d7a398326e1 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Tue, 30 Jun 2026 13:46:22 +0000 Subject: [PATCH 23/25] WIP: DESIGN SKETCH ONLY (no code; returns to stern-moth-225 + operator before --- src/v1/stage0/src/bin/claim_executor.rs | 11 +++++++---- 1 file changed, 7 insertions(+), 4 deletions(-) diff --git a/src/v1/stage0/src/bin/claim_executor.rs b/src/v1/stage0/src/bin/claim_executor.rs index 43423636075..9995429036b 100644 --- a/src/v1/stage0/src/bin/claim_executor.rs +++ b/src/v1/stage0/src/bin/claim_executor.rs @@ -1332,14 +1332,17 @@ fn run_walk(source_roots: &[String], batches: &[Vec], spawn_width: usi ); let batch_start = Instant::now(); // Partition units: memo units stay on the main thread; others spawn. + // A unit goes to the memo path if (a) its profile declares heavy whole-tree + // resolve, or (b) its entry is already in walk_memo from a prior batch — in + // which case re-resolving would be redundant regardless of profile. let mut memo_units: Vec = Vec::new(); let mut thread_units: Vec = Vec::new(); for unit in units { match &unit { - BatchUnit::SharedClaims { - use_walk_memo: true, - .. - } => memo_units.push(unit), + BatchUnit::SharedClaims { use_walk_memo: true, .. } => memo_units.push(unit), + BatchUnit::SharedClaims { entry, .. } if walk_memo.contains_key(entry) => { + memo_units.push(unit) + } _ => thread_units.push(unit), } } From 3f324ce7a0c9352cca8419724f3491470606f597 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Tue, 30 Jun 2026 13:47:45 +0000 Subject: [PATCH 24/25] fix: promote memo-eligible thread_units on entry cache hit; sync regen MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Two changes: 1. executor: at partition time, also move SharedClaims to memo_units if their entry is already in walk_memo (populated by a prior batch's heavy resolve). This eliminates cold re-resolves of the same entry in later batches even when the gate's own profile is non-heavy — achieving the documented 4×→1× resolve count per walk. 2. std_realization_schedule.rs: sync regen'd output (field shorthand vs explicit form in runnable_resource_profile constructor). Co-Authored-By: Claude Sonnet 4.6 --- src/v1/stage0/src/bin/claim_executor.rs | 5 ++++- src/v1/stage0/src/std_realization_schedule.rs | 6 +++--- 2 files changed, 7 insertions(+), 4 deletions(-) diff --git a/src/v1/stage0/src/bin/claim_executor.rs b/src/v1/stage0/src/bin/claim_executor.rs index 9995429036b..65c6b124c2e 100644 --- a/src/v1/stage0/src/bin/claim_executor.rs +++ b/src/v1/stage0/src/bin/claim_executor.rs @@ -1339,7 +1339,10 @@ fn run_walk(source_roots: &[String], batches: &[Vec], spawn_width: usi let mut thread_units: Vec = Vec::new(); for unit in units { match &unit { - BatchUnit::SharedClaims { use_walk_memo: true, .. } => memo_units.push(unit), + BatchUnit::SharedClaims { + use_walk_memo: true, + .. + } => memo_units.push(unit), BatchUnit::SharedClaims { entry, .. } if walk_memo.contains_key(entry) => { memo_units.push(unit) } diff --git a/src/v1/stage0/src/std_realization_schedule.rs b/src/v1/stage0/src/std_realization_schedule.rs index 7f3319048ff..bd2ca24e794 100644 --- a/src/v1/stage0/src/std_realization_schedule.rs +++ b/src/v1/stage0/src/std_realization_schedule.rs @@ -179,9 +179,9 @@ pub fn runnable_resource_profile( memory: Rc, ) -> Rc { Rc::new(RunnableResourceProfile { - heavy_whole_tree_resolve, - spawns_host_compiler, - memory, + heavy_whole_tree_resolve: heavy_whole_tree_resolve, + spawns_host_compiler: spawns_host_compiler, + memory: memory, }) } From 3ed9960185eb6d805dcb7e02751c4fbeaf475150 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Tue, 30 Jun 2026 13:51:43 +0000 Subject: [PATCH 25/25] add resolve-count oracle: memo fires resolve_entry_graph once per entry per walk MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit memo_deduplicates_resolve_count: first call assert resolve_nanos > 0 (fresh resolve fires), second call for same entry asserts resolve_nanos == 0 (cache hit, resolve_entry_graph does NOT fire). Goes RED if the memo is bypassed. Discriminating witness for the 4x->1x dedup claim (DESIGN §2). Co-Authored-By: Claude Sonnet 4.6 --- src/v1/stage0/src/bin/claim_executor.rs | 44 +++++++++++++++++++++++++ 1 file changed, 44 insertions(+) diff --git a/src/v1/stage0/src/bin/claim_executor.rs b/src/v1/stage0/src/bin/claim_executor.rs index 65c6b124c2e..01fb15e42c8 100644 --- a/src/v1/stage0/src/bin/claim_executor.rs +++ b/src/v1/stage0/src/bin/claim_executor.rs @@ -2080,4 +2080,48 @@ mod tests { "memo warm path must be byte-identical to cold path — shared InterpContext is pure" ); } + + /// Resolve-count oracle: proves the memo fires resolve_entry_graph exactly once + /// per distinct entry per walk (DESIGN §2 — no redundant resolve). + /// + /// Goes RED if the memo is bypassed: both calls would have resolve_nanos > 0, + /// meaning resolve_entry_graph fired twice for the same entry instead of once. + #[test] + fn memo_deduplicates_resolve_count() { + let root = workspace_root(); + let source_roots = vec![ + root.join("src/v2").to_string_lossy().into_owned(), + root.join("dsl").to_string_lossy().into_owned(), + ]; + let entry = root + .join("dsl/test/claim/runnable_resource_profile_witness_test.dag") + .to_string_lossy() + .into_owned(); + + let mut memo = std::collections::HashMap::new(); + + // First call for this entry: must resolve (resolve_nanos > 0). + let first = run_memo_shared_claims( + &source_roots, + &entry, + &["witness_negligible_profile_is_not_heavy".to_string()], + &mut memo, + ); + assert!( + first[0].resolve_nanos > 0, + "first call must pay the resolve cost (resolve_entry_graph fires)" + ); + + // Second call for the same entry: must cache-hit (resolve_nanos == 0). + let second = run_memo_shared_claims( + &source_roots, + &entry, + &["witness_substantial_memory_forbids_corpus_co_residence".to_string()], + &mut memo, + ); + assert_eq!( + second[0].resolve_nanos, 0, + "second call must cache-hit — resolve_entry_graph must NOT fire again" + ); + } }