Repository navigation
Construction-not-validation: dissolve the cache-key model<->realizer fork into single authority (realized key DERIVED from declared inputs_considered, so declare-without-keying is unwritable) — replaces the spec-only validating lens from #5423; triage roadmap lens items into make-impossible-by-const - #5425
Merged
Merged
Conversation
…rk into single authority The cache key had TWO hand-authored authorities — the .dag model row's inputs_considered and the Rust realizer's digest — which could diverge. PR #5423 shipped a SPEC-ONLY lens over the model row; it false-greened (a worker satisfied the declaration while the realizer keyed wrong). This collapses the fork by construction instead of validating it post-hoc. Model side (the class-kill): CatalogKeyDerivationFacts's classification+inputs_considered pair becomes a single CatalogKeyInputs sum. ContentAddressed (OUR caches) has NO inputs field — inputs are DERIVED from invalidation_triggers (content_addressed_inputs), so a content-addressed cache cannot declare-without-keying or key-without-declaring; it is unwritable for all 5 CAV rows present and future. NativeInternal/HandAuthored (external vendor caches) carry CITED inputs — observations of a system we don't control (§3); that is the genuinely-unstructurable residue the key_completeness lens now guards (cited rows only; CAV exempt=construction, HandAuthored exempt=authored). Realizer side: subject_digest_for_closure now folds a TOTAL materializer over a closed KeyInputAxis set (resolved_graph_cache.rs) — keyed axes = the enum's variants, cannot drift. std KeyDerivationFacts drops classification+inputs_considered: both were unconsumed and anonymous-literal-authorable (a divergence one layer down); the agnostic key-input list now exists only as the derived projection of the extdeps sum. Sole std consumer (vendor_only_key_inputs_omitted) preserved. Proven by EXECUTION (the #5423 lesson): - CAV derivation: content_addressed_inputs perturbed by triggers; live resolved_graph row derives [UpsertSubject, ToolchainSpec]; RED when the live row drops ToolchainChange. - realizer axis-sensitivity falsifiers (Rust): perturb transform/closure axis ⟹ key changes; RED proven by dropping TransformContent from the fold (teeth on the realizer). - whole-tree dsl_compile_clean gate ExitSuccess; fmt+clippy clean. Residual (named, v2-gated): the Rust axis set and the .dag derived set are two impls of one rule; full R←M single authority needs v2/realize (realizer = .dag subgraph, content(T)=content_hash(subgraph)). Absorbed by the self-host lane, not papered with a lens. ROADMAP: construct-vs-cite triage criterion + root-cause-before-lens documented. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
# Conflicts: # ROADMAP.md
briansrls
added a commit
that referenced
this pull request
Jun 21, 2026
…ize kernel
The §5 caching-via-realization principle made executable: a content-keyed
realization promises output = f(declared key inputs); an input read at realize
time but absent from the content-key makes a WARM hit serve a stale result a
fresh COLD recompute would no longer produce. The cache IS the purity falsifier.
- extdeps/realization/cache_purity.dag — CachePurityVerdict carrier (Pure |
Impure{located violation naming the read-but-unkeyed axis}); the durable
artifact v2 inherits. Discovery witness in dsl/test/claim.
- cache_purity_oracle.rs — v1 proving handler: audit_warm_equals_cold holds the
content-key fixed, perturbs candidate hidden inputs, and raises a located,
typed, LOUD CachePurityViolation on divergence (fail-closed). Probes that move
the key are declared axes (a miss, not a stale hit) and are skipped.
- cache_purity_oracle_test.rs — discriminating witnesses (DESIGN §5
spec-without-execution): REAL kernel warm==cold byte-identical round-trip +
real realization PURE under non-keyed probes (green by execution) PLUS an
injected hidden non-keyed input that goes RED with the loud located error.
ROADMAP §2 P1. Consumes subject_digest_for_closure (no re-fork of #5425's key).
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
This was referenced Jun 21, 2026
3 tasks
briansrls
added a commit
that referenced
this pull request
Jun 21, 2026
) #5428 (smart-crane) grounded Nat construction-side — Zero→Int(0), Succ{prev:Int(k)}→Int(k+1) — so native form == modeled form. Deferred doc update explicitly to lane manager post-#5425. DESIGN.md §5 open-thread (b): mark numeric tower GROUNDED; note that eval_binop CrossRepresentationEquality guard is dead-in-corpus for numerics but kept as fail-closed backstop until Value::Null split (guard removal bundled with that work, fenced out of this window). docs/plans/model-realization-fork.md §3.1: numeric row landed→grounded; records the exact realization, discriminating witness, and why the guard stays (bundled removal, not a regression). §3.2 (Value::Null split) unchanged — still the deeper root, its own runway. Co-authored-by: Brian Searls <briansrls@gunb.ai> Co-authored-by: Claude Sonnet 4.6 <noreply@anthropic.com>
briansrls
added a commit
that referenced
this pull request
Jun 21, 2026
Flip [ ]→[x] for unambiguously-merged work (PR-ref'd for traceability): - §0 numeric-tower grounding (#5428 — == straddle guard dead-in-corpus) - §0 inert-lens hygiene executable backstop (#5433) - §2 F2/F3 resolved_graph key derived from inputs_considered (#5425) - §3 cost-lens symbolic_max zero-absorption fix (#5437) - §4 gate existing generated testgen output (#5434) - §4 affected-set completeness (#5430) Partial/compound items left for their lane managers to flip in the PR that completes them. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
briansrls
added a commit
that referenced
this pull request
Jun 21, 2026
…gestion⁻¹ past syntax (#5442) * WIP: dsl -> v2 scoping * WIP: ROADMAP planning * WIP: ROADMAP planning * WIP: ROADMAP planning * ROADMAP: scannable dependency-ordered checklist; consolidate caching plan (de-fork zesty-deer-479 owner, absorb quick-ant-298 spine) Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> * WIP: ROADMAP planning * self-host: add bootstrap purity (no stage0 hand-edits / regen-lockstep keystone) + precise v1 cutover Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> * ROADMAP §0 fail-closed lock-down (blocks expansion) + audit doc; §4 website demo Audit: cache lossy-digest flake (resolved_graph_cache.rs:146, verified), ~inert analytical lenses (complexity/cost/etc), regen --verify unwired (#5325). Lock-down checklist gates expansion. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> * ROADMAP: flesh §2 idea->idea compiler (medium/language axes); §0 → lock-down LANE (audits→fixes→meta), name model<->realization fork as suspected root Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> * WIP: ROADMAP planning * lock-down: add CI-coverage-completeness audit (rust gate runs 3 of 60 v1 suites) + axiom/syllogism lens (DESIGN open thread #1 — lock down the reasoning) Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> * WIP: ROADMAP planning * roadmap §0/§7 + lockdown: lead with correctness-by-construction, demote lenses to residue Folds in the operator principle (relayed via quick-ant-298): a lens is validation — it concedes the bad thing is writable. Root-cause to make it unwritable (single authority / realization derived from model); reserve lenses for the genuinely- unstructurable (complexity/necessity). #5423's spec-only key lens shipped a false-green as the live proof. - ROADMAP §0: add the principle; split Fixes into tier-1 construction (dissolve model↔realization fork; cache-key derived-from-declared-inputs; self-host purity by construction) and tier-2 lens (complexity/cost; cache-redundancy; purity oracle; promote-inert). Meta-invariant → construction-justification rule. - ROADMAP §7: P1 cache-key reframed from 'realizer-key lens' to key derived from declared inputs_considered (construction). - fail-closed-lockdown.md: construction principle in the thesis; §4 checklist re-ordered construction-first / lens-residue; meta = construction-justification. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> * roadmap §0: add Disposition carrier + 'confront skipped modeling decisions' Captures the lens/coproduct disposition decision (operator). One typed carrier (Terminal{reason} | Scaffold{dissolves_to}) for BOTH lens-lifecycle tags AND coproduct dissolve-markers — today freeform 🟡 comments, unreadable by lens since comments aren't Nodes. Decision: middle path (construction-capable carrier + selectively-enforcing lens that ratchets coverage) now, #1 (substrate can't-define-untagged) as the named end-state. The lens is itself a Scaffold{dissolves_to: substrate-mandatory-tag} — self-dissolving when coverage = whole tree. Rejected jumping to #1 on sequencing (load-bearing §4 substrate change → escalate; flag-day migration; derived coproducts need disposition derived not authored), not on principle. Enforceability split: presence = construction (non-optional field, no meta-lens); redundancy (scaffold + successor both present) = hard gate; Terminal-vs-Scaffold correctness = retro/judgment (synthesis-feasibility limit). - docs/plans/disposition-carrier.md (new) - ROADMAP §0 tier-1 + meta 'confront skipped decisions' standing practice Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> * WIP: ROADMAP planning * DESIGN §5/§6: promote construction-over-validation; roadmap: scope-partition §0, testgen §1, shelve dashboard Addresses the review's four flags + sequencing nuance. - DESIGN.md §5: 'correctness by construction, not validation' is now an axiom (a check re-stating a model constraint is a 2nd representation §2/§3; prefer realization derived from a single authority; reserve checks for the unstructurable residue). §6 'enforce with lenses' reconciled: construction first, lens = residue mechanism, AND the executable inert-lens backstop is NOT superseded by the authoring-time construction-justification judgment. (flag 4 home + flag 3) - ROADMAP §0 partitioned: In-scope this window (numeric-tower grounding; cache trustworthy + warm==cold oracle shipped NOW as detective; widen rust gate; promote inert lenses) vs Fenced-OUT fan-out (Value::Null 131-site split; self-host purity gate; cross-tree import activation; Disposition carrier). Honest framing: window reduces fail-open surface, does NOT 'lock' the class — Null split stays open. (flags 1, 2, sequencing nuance) - ROADMAP §0 meta: restored executable inert-lens hygiene backstop, construction- justification layered on top (not 'supersedes'). (flag 3) - De-dup: principle no longer restated in ROADMAP/lockdown §0; both point to DESIGN §5. cache-key construction homed in §7, §0 references it. (flag 4) - ROADMAP §1 = testgen as bug-class oracle (+ affected-set completeness half + parked anemia lens); dashboard shelved to §8. - docs/plans/testgen-oracle.md (new), fail-closed-lockdown.md realigned. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> * WIP: ROADMAP planning * DESIGN §5/§6/§7: wall-vs-ratchet decidability, displaced-pain denominator, open language design Folds in the operator's product thesis + the two bounds that keep it honest. - §5: construction makes a class unwritable only when membership is DECIDABLE — trichotomy (wall now / wall after grounding / ratchet forever); 'never' is the trap (lets an undecidable ratchet masquerade as a wall — optimality by Rice). - §6: denominate the benefit — the deliverable is a displaced cost (§1 time / a paid-for pain), the lens/substrate is the moat not the product; priced in elegance the work is unbounded (the economic twin of 'never'). - §7: the recursion's payoff — language design itself opens up. It's locked by cost (a check = a compiler fork; a language = an adoption problem); both dissolve here (a wall is a row §2, applied over a medium-agnostic substrate §4), so (compiler-fork × language) → (row + medium). Sound where ingest is Lossless, fail-closed where not (DecodeFidelity §4). Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> * WIP: ROADMAP planning * ROADMAP: fix doc-graph violations from bright-eagle-46 review of #5424 Apply the apex axiom/syllogism lens (single authority / no orphan / no cycle) to the roadmap itself — manual acyclicity pass: - orphan: testgen-oracle.md backlinked §1 → repoint §4 (its own lane) - single authority: §0 cache-key now a pure pointer (= §2 F2/F3/P1); §0 numeric-tower marked the authoritative home (§5 de-fork / fork plan point here, no second checkbox) - §0↔§5 cycle: self-host purity reframed as a §5 deliverable §0's expansion-gate depends on (edge §5 → §0-gate → products), not §0-owned - undeclared edge: §7 react/html declares its dependency on §6 media - backlink sweep: the reorg had broken every numeric backlink across 7 plan docs; re-point all and anchor each to the stable section TITLE so a future renumber can't silently break them again Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> * ROADMAP §3 + plan: algorithmic-cost reduction by construction (rewrite, not budget) Reframe §3 from per-fn complexity budgets to the actual intent: rewrite common suboptimal patterns (O(n²)→O(n), O(2ⁿ)→O(n), O(n)→O(log n)) to the cheaper equivalent — construction on the cost axis, not a warning. New plan doc docs/plans/algebraic-rewrite-optimization.md captures the up-front design: the decidability split (modeled EffectShape makes the preconditions structural; equivalence stays undecidable so no optimality oracle), rewrite-rule-as-row + once-proven soundness, the common-case catalog tiered by precondition, D1 canonical-form-is-truth / D2 two seed rules / D4 constant-factor deferred, the four-witness DONE bar (incl. the non-firing control half-done versions skip), and a corpus hit-rate acceptance gate. complexity.dag is the cost oracle; synthesis.dag stays the advisory undecidable residue. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> * ROADMAP §2: Phase-0 measurement instrument done (#5431 peak-RSS) — remaining is the Phase-1 consumer Per quick-ant-298: the measurement keystone was nearly complete — model side already floor-enrolled, step timing already emitted; the only gap was peak-RSS, closed by #5431. P4's Phase-0 dependency is satisfied; remaining is the Phase-1 measured->plan feedback + width-fold (also unblocks §1-C). Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> * plan/§3: detection-vs-enforcement containment (E⊆D′⊆D) + explicit seed-rule I/O up front Grounded in cost.dag U2 + complexity.dag (investigated, not theorized): - detection is TOTAL by construction (kernel-level cost fold; arbitrary fns detectable); boundary is precision (ClassUnknown), not coverage - enforced rewrites are a strict subset structurally guaranteed by the class-drop witness: E ⊆ D′(precise) ⊆ D(all) - n√n excluded for a MODEL reason (PolynomialDegree is integer-only, n^1.5 unrepresentable); ternary search excluded (log base is not a class) - today's small gate roster = subject-production limit (fn-body reflection), NOT a detection limit - new §3a fully specifies the two seed rules up front: input→output→ precondition→non-firing control→discriminating equivalence input, so the worker builds to spec and the project can actually finish Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> * ROADMAP §0/§1: rust-gate is cadence-decoupling, not run-all (per fierce-hawk #5427) The 3-filter allowlist was COST selection, not arbitrary gatekeeping — the v1 SEED compiler costs ~tens of CPU-sec per trivial test, so run-all-per-PR is CPU-hours (off the table). True shape: per-PR cost-bounded subset + measured #[ignore="expensive: Ns"] + completeness lens (#5427); nightly --ignored lane as the destination for expensive + the 58 currently-ignored tests (owned by §1/quick-ant, after #5431, escalate for load-bearing CI-gen). Completeness = every test runs on >=1 cadence (fail-closed). Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> * plan §2a: generalize by structural-redundancy keying (O(n^x)->O(n^(x-1)) free); flag n-log-n as substitution Per operator: catalog must generalize polynomial-degree reduction without edge cases. Resolution: rules key on the structural redundancy, never on degree — degree is not evidence of redundancy (would fire on genuine O(n^x)). A structurally-keyed nested-membership->set peels one level wherever it matches; fold-to-fixpoint gives O(n^3)->O(n^2)->O(n). Cost model supports arbitrary integer degree, so witness (b) holds at every peel. Flagged OPEN (operator input invited): O(n^x)->O(n log n) is algorithmic SUBSTITUTION (different algorithms, same I/O) not redundancy elimination — verges on undecidable equivalence; tractable form is per-idiom rules (sort-based dedup, repeated-min->heap), not a parameterized rule. Seed Rule 1 now authored structurally + carries a depth-2 generalization witness. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> * plan §1b: Unknown is an anemic atom — dissolve over time (reuse Disposition), never a false pass Per operator: classifying Unknown isn't a fixed up-front split — it's the standing anemic-leaf dissolution practice (DESIGN §2 decompress->map->reduce) applied to the cost lens. UnknownCost{diagnostic} already carries its reason; the anemia is the free-form reason. Each decomposition resolves an Unknown to construction (now-precise class -> new D′) or a grounded Terminal (genuinely undecidable, positively recognized -> advisory comment). DFS-first: this IS the Disposition carrier (resolves to construction-or-justified-Terminal), so reuse it, don't fork an unknown-reason enum. Supersedes the static Undecidable|Undetermined split. Two invariants fixed up front: never a false pass (Unknown=>Violates, already holds); every Unknown on the dissolution frontier. cost.dag enrichment + un-parking Disposition are operator-gated. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> * ROADMAP: §3 reverts to budget-gate validation (stability); rewrite-engine relocated to §5 (post-stability) Operator decision 2026-06-21: budget-gate validation is fine for the stability window; the algorithmic-cost REWRITE construction design is expansion, homed with self-hosting (§5) — IR-rewrite/canonicalization is most natural once .dag is the self-hosted truth. - §3 = complexity budget gate (validation): cost-lens symbolic_max fix (#5437) + per-fn subject + budget-gates-whole-codebase (gated on fn-body reflection) + synthesis advisory. #5437 foundation stays in-window. - §5 gains an 'adjacent expansion lane' = the rewrite engine, pointing at the preserved plan doc; marked post-stability. - plan doc status -> POST-STABILITY EXPANSION, relocated to §5. Nothing deleted — the rewrite design is preserved, just fenced out of the stability window (same as Disposition / Value::Null-split). Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> * WIP: ROADMAP planning * #5442 review fix (warm-lark-306): grep-as-authority for the sidecar roster (10 not 9) The §0-guard impl PR (#5445) grepped current main and found 10 importers of extdeps.languages.bash.program, not 9 — the 10th (dsl/gunbc/ci_spec.dag) landed via #5432 after the original pre-merge grep. Rather than bump the frozen count, make the live grep the authority (the roster shrinks to 0 as the bash-sidecar arc migrates consumers, so any frozen number rots — the single-authority point). Also note the two *_test importers are intentionally not walled (guard scans consumer-source roots only). Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> * ROADMAP: check off 6 merged items (catch-up sweep) Flip [ ]→[x] for unambiguously-merged work (PR-ref'd for traceability): - §0 numeric-tower grounding (#5428 — == straddle guard dead-in-corpus) - §0 inert-lens hygiene executable backstop (#5433) - §2 F2/F3 resolved_graph key derived from inputs_considered (#5425) - §3 cost-lens symbolic_max zero-absorption fix (#5437) - §4 gate existing generated testgen output (#5434) - §4 affected-set completeness (#5430) Partial/compound items left for their lane managers to flip in the PR that completes them. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> * ROADMAP §1: add compile-clean-gate force-checks-every-fn-body box (2(ii) fail-open) New floor-coverage item: the compile-clean gate is fail-open — unreached fn bodies escape typecheck, so undefined symbols in dead code pass green (execution-proven on utf8_decode_bytes). Construction fix = typecheck total over every declared body. Owned by §1 (quick-ant); measure-first, operator-gated enforce-flip. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> * ROADMAP §0: correct the 2(ii) box — registry-leak mechanism, not unreached-bodies snappy-gull's deeper diagnosis: the fail-open is NOT unreached bodies (bodies ARE visited). utf8_decode_bytes resolves because it's a global builtin_function_registry entry (04_method.dag, a marked bridge scaffold) not scoped to the compiled tree. Reframe the box to tree-scoped builtin availability / registry partition; instance fix = real std fn + remove the registry bridge entry. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> * WIP: ROADMAP planning * plan doc: enforcement roster is a FROZEN grandfather set, not derived (warm-lark correction) Deriving the realization-vocab exception roster from a live grep would make the guard vacuous (leak = non-edge importer AND NOT-in-roster; derived roster ⇒ every importer always in it ⇒ leak_count always 0 ⇒ never fires). Distinguish the informational prose count (rots, re-grep) from the lens's enforcement roster (frozen, so a new unrostered importer goes RED = the teeth). Add the 11th importer (extdeps_external_authority_transport, the #5418→#5445 race, fixed by #5453) and the roster-completeness assertion as the steady-state race-hardening. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> * WIP: ROADMAP planning * ROADMAP refresh: §1 nightly→Pop-B (opt-level won), §2 resolve-cache GO + P2 de-fork-dependent, §0 census regression + gate-hygiene Reflects decisions/findings that landed 2026-06-21: - §1: the "expensive" tests were debug-build amplification, not intrinsic seed cost (proud-deer cause-table); opt-level=3 (#5456) restores Pop-A to per-PR; nightly lane reduced to Pop-B wet-captures only. Mirror corrected in §0. - §2: resolve-cache enable = GO (~18% floor-wall, purity-proven, #5429-gated); P2 ParseTable dissolution reclassified as a downstream consumer of the dsl→v2 de-fork (keen-otter: v2-local rewire is cosmetic); #5446 realize kernel green. - §0: stage0 clone-census ratchet went inert + the seed regressed 1138 over budget (rust-side coverage-by-illusion + thesis regression; #5427 surfaced it); gate-hygiene rule (floor-enrolled gate must be green-on-main at merge) + roster-completeness assertion promoted to should-land (the #5445 floor-skew). - §1: registry-partition instance fix = #5452 (verified sound). Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> --------- Co-authored-by: Brian Searls <briansrls@gunb.ai> Co-authored-by: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
briansrls
added a commit
that referenced
this pull request
Jun 21, 2026
* WIP: warm==cold cache purity detective (§2 P1->P3)
* warm==cold cache purity detective: executable §5 oracle over the realize kernel
The §5 caching-via-realization principle made executable: a content-keyed
realization promises output = f(declared key inputs); an input read at realize
time but absent from the content-key makes a WARM hit serve a stale result a
fresh COLD recompute would no longer produce. The cache IS the purity falsifier.
- extdeps/realization/cache_purity.dag — CachePurityVerdict carrier (Pure |
Impure{located violation naming the read-but-unkeyed axis}); the durable
artifact v2 inherits. Discovery witness in dsl/test/claim.
- cache_purity_oracle.rs — v1 proving handler: audit_warm_equals_cold holds the
content-key fixed, perturbs candidate hidden inputs, and raises a located,
typed, LOUD CachePurityViolation on divergence (fail-closed). Probes that move
the key are declared axes (a miss, not a stale hit) and are skipped.
- cache_purity_oracle_test.rs — discriminating witnesses (DESIGN §5
spec-without-execution): REAL kernel warm==cold byte-identical round-trip +
real realization PURE under non-keyed probes (green by execution) PLUS an
injected hidden non-keyed input that goes RED with the loud located error.
ROADMAP §2 P1. Consumes subject_digest_for_closure (no re-fork of #5425's key).
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
* cache purity: address review — dissolve is_pure predicate; add §7 Rust-shrinkage receipt
Review (claude-opus-4-7, APPROVE) soft concerns:
- predicate-dissolution: cache_purity_is_pure was a Bool restating the
CachePurityVerdict coproduct. Deleted it; consumers (and the witness) match the
verdict directly so the located violation stays in hand on the Impure arm.
- §7 hand-Rust receipt: added an explicit SCAFFOLD dissolve-on trigger to the
oracle module header (net-new capability bound to the v2 realize-fold fixed
point, ROADMAP §2 P5), matching the codebase's named-dissolution convention.
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
* cache purity test: make pure-under-probes test hermetic (isolate cache dir)
Review (claude-opus-4-7) valid non-blocking finding:
real_resolved_graph_realization_is_pure_under_nonkeyed_probes took
CACHE_ENV_MUTEX but never isolated GUNBC_RESOLVED_GRAPH_CACHE_DIR, so a host
with that var set could leak into the test. Replaced the bare mutex lock with
CacheEnvGuard::set(temp) — which both isolates the cache dir and serializes the
env-var probe — matching tests 1 and 3.
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
---------
Co-authored-by: Brian Searls <briansrls@gunb.ai>
Co-authored-by: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Co-authored-by: Brian Searls <11205878+briansrls@users.noreply.github.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.
Construction-not-validation: dissolve the cache-key model↔realizer fork
The resolved-graph cache key had two hand-authored authorities — the
.dagmodel row'sinputs_consideredand the Rust realizer's digest — that could diverge. PR #5423 added aspec-only lens over the model row and false-greened: a worker satisfied the declaration
while the realizer still keyed wrong. Per the governing principle (correctness by
construction, not validation), this makes the divergence unwritable rather than caught.
Model side — the class-kill
CatalogKeyDerivationFacts'sclassification+inputs_consideredpair → oneCatalogKeyInputssum:ContentAddressed(OUR caches) — no inputs field; inputs are DERIVED frominvalidation_triggers(content_addressed_inputs:[UpsertSubject]+ToolchainSpeciffit invalidates on toolchain). Declaring-without-keying / keying-without-declaring is
unwritable for all 5 content-addressed rows (resolved_graph, buildbuddy,
parse_table_memo, hermetic_fixture×2), present and future.
NativeInternal/HandAuthored(EXTERNAL vendor caches: cargo/rustup/sccache/gha) —inputs are a CITED observation of a system we don't control (§3). This is the
genuinely-unstructurable residue:
key_completenessnow validates that citation only(ToolchainChange ⟹ a cited toolchain axis), firing on
NativeInternalrows alone.Realizer side
subject_digest_for_closurefolds a total materializer over a closedKeyInputAxisset(
resolved_graph_cache.rs): keyed axes ≡ the enum's variants, so they cannot drift.std cleanup
std KeyDerivationFactsdropsclassification+inputs_considered— both unconsumed andanonymous-literal-authorable (a divergence one layer down). The agnostic key-input list now
exists only as the derived projection of the extdeps sum. std
KeyDerivationFactshas noliteral-authoring path; its sole constructor is
cache_interface_facts_from_catalog, and theonly consumed field (
vendor_only_key_inputs_omitted) is preserved.Proven by EXECUTION (the #5423 lesson)
content_addressed_inputs([ToolchainChange])keys the toolchain vs([ManualPurge])does not; liveresolved_graphrow derives[UpsertSubject, ToolchainSpec];RED verified by dropping
ToolchainChangefrom the live row.determinism holds. RED verified by dropping
TransformContentfrom the fold (teeth onthe realizer, not just the spec).
dsl_compile_cleangate →ExitSuccess;cargo fmt --check+clippy -D warningsclean; cache test modules green.Residual (named, not papered — v2-gated)
The Rust realizer's axis set and the
.dagmodel's derived set are two implementations of onerule. Full R←M single authority needs v2/realize (realizer =
.dagsubgraph,content(T) = content_hash(subgraph)); the v1 seed can't have the realizer read the model rowat key-compute time without re-entering this cache. Absorbed by the self-host lane.
Secondary
ROADMAP: the construct-vs-cite triage criterion + root-cause before lens documented.
🤖 Generated with Claude Code