Repository navigation
Design sketch: floor shared-computation memoization (no code) - #5959
Merged
Merged
Conversation
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 <noreply@anthropic.com>
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 <noreply@anthropic.com>
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 <noreply@anthropic.com>
Contributor
Author
|
Both findings are valid — fixed in commit 5ec93ca. Finding 1 (artifact dependency graph / §3 M2): Confirmed via source. The three gates use distinct
No artifact sharing is possible across gates. The claim that DslCompileCleanGate and RegenVerifyGate could consume EmitDeterminismGate's proven-canonical artifact was wrong — different source roots → different compilations. M2 is now stated as forward-proofing only (future gate adds a Finding 2 (displacement math / §6): M2 saves 0 compiles today (no two gates share a tuple in the current set; the EmitDeterminismGate oracle pair is intentional and must survive). Displacement table corrected: M1 saves ~35s (resolve memo), M2's maximum future saving is 1× compile (~537s) if the oracle pair collapses after Also fixed: M1's dissolution trigger was wrong (said it dissolves into M2; corrected to orthogonal — M1 is Axis-B resolve memo, M2 is Axis-A subprocess compile declarations, they don't subsume each other). — sent from tidy-hawk-120 |
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 <noreply@anthropic.com>
Contributor
Author
|
Both findings valid — fixed in commit 06cf6ea. Finding 1 (§6 table, line 142): Stale row leftover from before the distinct-tuple rewrite. The table said '×2 (oracle pair survives)' but that contradicts the oracle pair surviving (2 compiles survive → 4→3, not 4→2). Fixed to '×3 (oracle pair 2→1; other two tuples unchanged)' and total updated to ~1611s + ~37s. Finding 2 (§7, line 168): '1× total compile' was impossible — even after oracle pair collapses to 1×, the three distinct-tuple operations (DslCompileClean, EmitDeterminism×1, RegenVerify) all remain necessary. Corrected to 'reduces from 4× to 3×; further reduction below 3× would require collapsing two tuples or removing a gate, neither in scope here.' — sent from tidy-hawk-120 |
…05s (not ~35s) 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 <noreply@anthropic.com>
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 <noreply@anthropic.com>
… 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 <noreply@anthropic.com>
briansrls
pushed a commit
that referenced
this pull request
Jun 30, 2026
…le_tree_published_mock_keys on scoped diff (docs only) (#5994) * Design sketch: affected-set precompute pruning (docs/plans only, no implementation) Spec for guarding precompute_whole_tree_published_mock_keys on a scoped diff. Covers: consumer fn + plug point, diff_touches_published_mock_closure fn, input carrier (NodeArtifactProvenance), non-flaky structural None/Some witness + measured delta logged, soundness lemma (verified against fn body: output bounded to transitive closure of PublishedMockCase declarers, no whole-tree scan in resolve path), acceptance witness (real gunbc floor, 3 parts), fail-safe, and composition with tidy-hawk-120 (#5959). Returns to stern-moth-225 → loyal-bee/operator for sign-off before any code. Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com> * Fix cursor findings on #5994: correct carrier (line_ranges_by_file) and tri-state PrecomputeOutcome Finding 1: §5 named NodeArtifactProvenance as the carrier — not in the v1 Rust path. Actual carrier is line_ranges_by_file produced by floor_git_diff_range() → parse_unified_diff_line_ranges (cli_run.rs:3533-3536); collect_frontier_seeds consumes it for execution-skip, not yields it. Corrected. Finding 2: whole_tree_published_keys=None has two existing meanings (ran+empty at line 3510; proposed skip). Indistinguishable without a carrier change. Fix: spec now requires tri-state PrecomputeOutcome {Skipped, EmptyKeys, Keys(_)} so the structural witness asserts outcome==Skipped unambiguously. Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com> * Fix second cursor round on #5994: purge remaining None/Some conflations - Line 103 (§6 summary): 'structural None/Some' → 'PrecomputeOutcome::Skipped/Keys(_)' - §9 acceptance criteria (a)(c): replace whole_tree_published_keys==None/Some(_) with outcome==PrecomputeOutcome::Skipped/Keys(_), matching §6 tri-state - §7: replace 'Passing None' with 'PrecomputeOutcome::Skipped path' - §10: 'None early-exit path' → 'PrecomputeOutcome::Skipped early-exit path' - §3 code block: update guard sketch to show PrecomputeOutcome tri-state (Skipped / EmptyKeys / Keys) replacing the Option<HashSet> pattern All Option/None/Some references that survived in doc now either explain the OLD ambiguity (problem statement in §6 prerequisite, fine) or are in the existing cli_run.rs code context (authoritative, not spec language). Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com> * Fix third cursor round on #5994: tighten skip guard + fix control assertion Finding 1: mock-closure check alone is insufficient — a diff can miss the PublishedMockCase closure yet still leave witnesses that use mock keys at eval time (v1_interpreter.rs:1114-1121 fallback under-populates governed_services). Fix: §3 guard requires BOTH !diff_touches_published_mock_closure AND all_witnesses_will_skip; §7 names the fail-open path and the two safe alternatives (conjunction guard, or M1 cache from tidy-hawk-120 §10). Finding 2: in-closure control at §6 item 4 asserted Keys(_) specifically, but declarers can legitimately produce EmptyKeys. Fix: assert outcome != PrecomputeOutcome::Skipped (i.e. EmptyKeys | Keys(_)) instead. Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com> * Register affected-set-precompute-pruning.md in the ROADMAP doc graph Adds a ROADMAP entry linking docs/plans/affected-set-precompute-pruning.md so doc_graph_has_no_orphan_docs passes (CI was failing with Bool(false)). Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com> * WIP: DESIGN SKETCH ONLY (no code, returns to stern-moth-225 + operator for si * Fix three cursor RC findings on precompute-pruning sketch Finding 1: §6 item 1 fixture was under-specified — "outside the mock closure" alone is insufficient when the file is also in a witness frontier. Tightened to require outside BOTH the mock closure AND every witness's node frontier; explains why a test-only .dag edit can prevent Skipped from being assertable. Finding 2: §9(c) required Keys(_) but §6 item 4 allows EmptyKeys|Keys(_) (!= Skipped). Aligned §9(c) to != Skipped (consistent with §6's structural guarantee that precompute ran, not that it yielded keys). Finding 3: M1 in tidy-hawk-120 is a resolve_entry_graph memo (~105s Axis B), not a precompute-keys cache. Fixed §2 table row, §7 guard description (removed CachedKeys/M1 alternative paragraph), §10 scope boundary, and ROADMAP entry — all mis-scoped M1 as caching the precompute result. The two lanes are orthogonal; M1 cuts resolve cost when the corpus runs, this guard cuts precompute cost when all witnesses skip. Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com> * Fix two cursor RC findings: §3 M1 OR branch + all_witnesses_will_skip spec Finding 1: §3 comment still said 'all_witnesses_skip OR M1 can serve keys' — contradicts §7/§10/§2 which confirm M1 is a resolve memo (cannot serve precompute keys). Removed the OR branch; condition is now AND-only. Finding 2: all_witnesses_will_skip was referenced as a required conjunct in §3/:44 with no spec. Added §4b with signature, algorithm (bulk pre-flight of the existing per-row predicate at cli_run.rs:3721-3731), tie to !current_entry_touches && !function_edited, cost analysis, and fail-closed invariant (must replicate or over-approximate the inner loop predicate, never under-approximate). Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com> * Fix two cursor RC findings: frontier_files field + §9(a) acceptance bar Finding 1: §4b cost model cited frontier_seeds.frontier_files which does not exist. NodeFrontierSeeds (cli_run.rs:3275-3278) has only overlapping_data_items, edited_test_fns, force_run_all. Rewrote all_witnesses_will_skip algorithm to use the actual fields: O(1) conservative check (!force_run_all && overlapping_data_items.is_empty() && edited_test_fns.is_empty()). This avoids resolve entirely: when overlapping_data_items is empty, entry_frontier_nodes_from_seeds returns empty for every entry and entry_touches_frontier_seeds returns false — all witnesses skip. Explained why the per-entry touch check requires a full InterpContext and cannot be used at the precompute plug point. Finding 2: §9(a) only required "disjoint from the PublishedMockCase closure" but the §3 guard also requires all_witnesses_will_skip. A diff outside the closure that fires a witness frontier would fail Skipped. Added "disjoint from BOTH closure AND every witness's node frontier (produces empty NodeFrontierSeeds)" and explicit note that a diff satisfying only one conjunct correctly runs precompute and fails (a). Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com> * WIP: DESIGN SKETCH ONLY (no code, returns to stern-moth-225 + operator for si * Address cursor + stern-moth-225 review notes on de-fork plan Three substantive fixes from cursor RC (#33547): - Step 1: Document the function_edited gap in floor_witness_run_disposition (currently models only node-frontier, not edited_test_fns bypass) - Step 4 Consumer 1: Require both skip axes (node-frontier + function-edited) to be modeled before migration; floor_witness_run_disposition must be extended before wiring - Step 4 Consumer 2: Fix precompute-skip guard to require both RerunNodeSetProduced{nodes:[]} AND edited_test_fns.is_empty(); label as conservative vs the mock-closure tightening (future follow-on) - Acceptance witness (a): Promote to FULL-PREDICATE equivalence check covering both skip axes, not just entry_touches_frontier_seeds Two non-blocking notes from stern-moth-225: - Step 1: Add consumer-surface paragraph (probe_selector, affected_testgen_ci_runner, affected_set_selection already import Impl 1 — only the Rust floor forks the authority) - Step 3: Promote prerequisite to explicit numbered hard-gate sequence (prove → migrate → verify → THEN delete) Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com> * WIP: DESIGN SKETCH ONLY (no code, returns to stern-moth-225 + operator for si * Register affected-set-precompute-pruning.md in roadmap_authority.dag; regen ROADMAP.md The prior hand-edit to ROADMAP.md was not backed by an authored_doc entry in roadmap_authority.dag, causing generated_artifact_drift_gate_passes to fail after the main merge. Fix: add the authored_doc node to the authority and let main_wet regenerate ROADMAP.md from the single source. Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com> --------- Co-authored-by: Brian Searls <briansearls1@gmail.com> Co-authored-by: Claude Sonnet 4.6 <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
gunbc compile(~537s each) within one CI run, plus 2× in-processresolve_entry_graph(~30–40s each) for the same closure.RunnableCompileas a first-class plan node, gated onv2.std.determinism(§5 determinism mechanism P1: core axis, roster, compose algebra, witnesses #5941)).Correction (v2 — 2026-06-29)
Initial M2 sketch incorrectly proposed that
EmitDeterminismGate's x2 diff "evaporates" if the compile is content-addressed. This is backwards. Content-addressing assumes determinism; it doesn't prove it. Emit is KNOWN-NONDETERMINISTIC today (HashMap iteration order;v2.std.determinismis at P1). The corrected M2:EmitDeterminismGatekeeps BOTH cold, independent compiles — it is the oracle that licenses the artifact as canonical.DslCompileCleanGateandRegenVerifyGateconsume the oracle's proven-canonical artifact. Net: 4→2 compiles, ~18 min saved.v2.std.determinism(§5 determinism mechanism P1: core axis, roster, compose algebra, witnesses #5941) closing the non-determinism gap before content-addressing compile output is sound.Grounding
docs/plans/ci-floor-fractal-gantt.md(run 28136318404, 2026-06-24).gunbc compiletoday:DslCompileCleanGate(1×),EmitDeterminismGate(2×),RegenVerifyGate(1×).Test plan
v2.std.determinism(§5 determinism mechanism P1: core axis, roster, compose algebra, witnesses #5941)🤖 Generated with Claude Code