Skip to content

Cache key-completeness lens: ToolchainChange invalidation ⟹ a toolchain input in inputs_considered (fix resolved_graph_cache) - #5423

Merged
briansrls merged 4 commits into
mainfrom
session/deep-ant-174
Jun 21, 2026
Merged

briansrls merged 4 commits into
mainfrom
session/deep-ant-174

Conversation

@gunbai-bot

@gunbai-bot gunbai-bot Bot commented Jun 21, 2026 •

Copy link
Copy Markdown
Contributor

Summary

A cache for a transform T over data D is sound only if its key content-addresses every input that can change the cached value — content-addressed by construction (DESIGN §2/§5; cache-key-by-construction spine). The recurring violation is a derived key that promises to invalidate on toolchain change (ToolchainChange ∈ invalidation_triggers) while the toolchain is not keyed — so the derived key omits the transform and a toolchain change yields a silent stale hit (§5 fail-open).

resolved_graph_cache had exactly this bug at both layers:

  • Model (extdeps/realization/resolved_graph.dag): ContentAddressedByValue, invalidation_triggers: [ToolchainChange, ManualPurge], but inputs_considered: [UpsertSubject] — internally inconsistent.
  • Realizer (src/v1/stage0/src/resolved_graph_cache.rs): subject_digest_for_closure faked the missing toolchain axis with hand-authored RESOLVE_LOGIC_VERSION="v2-resolve-1" / KERNEL_INTERN_SEED_VERSION="kernel-seed-1" strings — a §3 nickname for the transform's content; a human had to remember to bump them, so the key silently drifted when resolve/normalize/infer/ownership or the kernel intern seed changed.

This PR fixes both so they agree (model+realizer), inhabits the STAGED key-derivation axis with a mechanical lens, and proves it by execution.

Changes

  • Realizer fix resolved_graph_cache.rs — subject_digest_for_closure now mixes in content(transform) derived by construction from the compiler's actual realized artifact (a hash of the running executable's bytes), computed once per process. The two hand-authored version constants are deleted. Coarse — any compiler change invalidates — but never stale: if the transform changes, the binary changes, the key changes. Fail-closed: panics if the artifact can't be read rather than substitute a stand-in that could serve a stale hit.
  • Model fix resolved_graph.dag — inputs_considered: [UpsertSubject, ToolchainSpec]; evidence note de-faked. Now a true statement of what the realizer does.
  • New lens extdeps/cache/key_completeness.dag — a pure reader over the catalog rows enforcing: a derived key (ContentAddressedByValue|NativeInternalHash) declaring ToolchainChange invalidation must include a toolchain axis (RustcInvocation/ToolchainSpec) in inputs_considered. HandAuthoredString keys are exempt (authored, not derived — separately policed). Reuses catalog_has_vendor_only_key_inputs (§3). Projects to std.lens_verdict. Roster fold over the live cache_catalog is the gate.
  • Witness dsl/test/claim/cache_key_completeness_test.dag — CI-floor auto-enrolled; green-by-execution with green/red/exemption/vacuity controls + live-catalog fold.

The generalized invariant: validity-depends-on-X ⟹ X's source ∈ inputs_considered.

Known limitation (stated plainly)

The lens is spec-only — it reads the catalog row, so it cannot mechanically force the realizer to stay honest (a future edit could re-fake the realized key while the model row stays green). This PR makes the current green true by fixing the realizer; spine step 4 (a lens forbidding hand-authored keys in realizers) is the follow-on that would catch re-faking.

North star

v2 self-host, where content(T) = content_hash(transform subgraph) natively and the version string ceases to exist. The remaining steps (enabling the dormant resolve cache unconditionally — GUNBC_RESOLVED_GRAPH_CACHE_DIR) are deliberately not done here: the key had to be sound first.

Test plan

  • cargo test -p v1-compiler-tests (cache modules) → 11 passed, incl. cross_process_cache_matches_cold_oracle_corpus (cached==cold purity oracle), poisoned_hit_rejected_*, key_mismatch_forces_miss_not_stale_hit.
  • .dag witness cache_key_completeness_witnesses → true (exit 0); discriminating: planted drop of ToolchainSpec from the live row → false (exit 1); restored.
  • cargo clippy -p v1-compiler -- -D warnings → clean. cargo fmt --all --check → clean.

🤖 Generated with Claude Code

briansrls and others added 2 commits June 21, 2026 01:32
The WIP commit landed the lens (extdeps.cache.key_completeness) + the model
fix (resolved_graph_cache keys ToolchainSpec) but no consumer ran it green.

This witness is the real consumer (auto-enrolled by the CI floor as a
*_test.dag with a `test fn`). It proves, by execution:
  - GREEN: a derived key that promises ToolchainChange AND keys the toolchain
    is complete; the verdict Holds.
  - RED control: the same row with the toolchain dropped is under-keyed; the
    verdict is a Violation (not Holds).
  - HandAuthoredString exemption: the same omission on a non-derived key is
    complete (its key is authored, not derived from inputs).
  - vacuity: no ToolchainChange promise => complete even without a toolchain
    input (the implication does not over-fire).
  - LIVE gate: the lens folds over the actual extdeps.cache.cache catalog and
    over resolved_graph_cache_facts directly — GREEN today, and verified RED
    when ToolchainSpec is dropped from the live row.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
@gunbai-bot gunbai-bot Bot changed the title Cache keys content-addressed by construction: key-completeness lens (ToolchainChange invalidation => transform in inputs_considered) inhabiting the staged key-derivation axis; fix resolved_graph_cache's faked RESOLVE_LOGIC_VERSION/KERNEL_INTERN_SEED_VERSION (derive content(transform), not hand-autho Cache key-completeness lens: ToolchainChange invalidation ⟹ a toolchain input in inputs_considered (fix resolved_graph_cache) Jun 21, 2026
@gunbai-bot
gunbai-bot Bot marked this pull request as ready for review June 21, 2026 01:38
@gunbai-bot

gunbai-bot Bot commented Jun 21, 2026

Copy link
Copy Markdown
Contributor Author

Re: the non-blocking naming observation (claude-opus-4-7) on catalog_has_vendor_only_key_inputs reading against its new caller in key_completeness.dag — agreed it's a real §3 readability nit, deferring it to a follow-on rather than fixing it here, for two reasons:

  1. The name is defensible at its definition site (extdeps/cache/types.dag): the "vendor-only key inputs" are precisely the toolchain axes (RustcInvocation/ToolchainSpec) — they're the inputs dropped from the agnostic std projection — so the function is accurate where it's authored, and the lens comment documents the reuse intent. A rename would touch a shared §3 authority with a second consumer (cache.dag's vendor_only_key_inputs_omitted), so it deserves a deliberate single-authority pass, not a rushed edit.

  2. This branch is frozen at merge-ready; any push re-stales HEAD-keyed approvals (the dashboard re-keys reviews on every push). Trading the current approval + a full CI cycle for a pure-readability rename isn't a holistic win.

Tracked as a follow-on (rename to e.g. catalog_has_toolchain_axis_inputs, updating both call sites). Thanks for the careful read — the substantive byte-collision finding is fixed in 18a09e18.

— sent from deep-ant-174

@briansrls
briansrls merged commit 06d8b78 into main Jun 21, 2026
1 check passed
@briansrls
briansrls deleted the session/deep-ant-174 branch June 21, 2026 02:41
briansrls added a commit that referenced this pull request Jun 21, 2026
…te 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>
briansrls added a commit that referenced this pull request Jun 21, 2026
…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>
briansrls added a commit that referenced this pull request Jun 21, 2026
* 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>

---------

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
…#5424) (#5426)

* 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>

---------

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
…budgets) + plan doc (#5436)

* 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>

---------

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
…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)

* WIP: Construction-not-validation: dissolve the cache-key model<->realizer for

* WIP: Construction-not-validation: dissolve the cache-key model<->realizer for

* WIP: Construction-not-validation: dissolve the cache-key model<->realizer for

* Construction-not-validation: dissolve the cache-key model↔realizer fork 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>

---------

Co-authored-by: Brian Searls <briansrls@gunb.ai>
Co-authored-by: Claude Opus 4.8 <noreply@anthropic.com>
briansrls added a commit that referenced this pull request Jun 21, 2026
…key-completeness lens

#5418's external-authority gate scans the LIVE extdeps tree and fail-closes on any
module lacking an anchor. Once #5422 cleared the FreeMonoid collision and the missing
gate_is_heavy_resolve arm let the plan resolve, the gate correctly flagged 5 modules
that landed on main AFTER #5418 authored its roster and were neither anchored nor
backfilled:

  missing: extdeps.access.{aws_iam,posix,rbac,zanzibar}   (#5415 access model)
  missing: extdeps.cache.key_completeness                 (#5423 cache lens)

The 4 access modules already carry their real upstream citation in a `// Source:`
comment (AWS IAM grammar, POSIX.1-2017/opengroup, ANSI/NIST RBAC, the Zanzibar USENIX
paper) — promoted each to the structured `extdeps_external_authority_anchor` carrier
the gate gates on (DESIGN §3: the mark on the carrier is the authority). No access
sibling is backfilled, so anchoring (not backfilling) is the consistent treatment.

extdeps.cache.key_completeness is an internal §5 cache-soundness LENS (a pure reader
over the cache catalog), not a cited external-system model — so it joins its 8
extdeps.cache.* siblings on the backfill_pending roster as tracked debt, not a fake
external anchor.

Verified by execution: the floor's discovery-corpus (587 witnesses) and
extdeps_external_authority_gate_passes both go GREEN with this change (live
violation set empty, roster count > 150).

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
briansrls added a commit that referenced this pull request Jun 21, 2026
…ive #5297) (#5418)

* extdeps: external-authority anchor carrier + fail-closed CI lens (revive #5297)

Land the never-merged #5297 mechanism onto current main: a structured,
lens-checkable external-authority citation on every dsl/extdeps module,
enforced fail-closed on the CI floor.

Carriers
- extdeps.uri: Uri { scheme: UriScheme, locator } with closed-sum
  UriScheme = Http | Https | File | Ftp (RFC 3986 / 7595 grounded).
- extdeps.external_authority: ExternalAuthority { uri }, FactAuthorityOverride,
  and the canonical `data extdeps_external_authority_anchor` row.

Lens (v2.lens.extdeps_external_authority)
- Fail-closed live policy per module: machinery-exempt -> backfill-pending ->
  else require a present external Http/Https anchor. Scheme decoded by exhaustive
  constructor identity (decode_uri_scheme), never a URL-prefix string.
- Violations: MissingFormalAnchor / UnrecognizedAnchorScheme / NonExternalAnchorScheme.

Host projection (extdeps_shape_transport_policy_project.rs)
- Structural read of the anchor record; live roster derived from the module-path
  index (declared module name, not directory); backfill + machinery-exempt facts.
- 9 builtins wired through 04_method.dag / v1_interpreter.rs / v1_compiler_infer_method.rs.

CI
- ExtdepsExternalAuthorityGate enrolled in gunbc_ci_spec and scheduled on the floor;
  runs uri witnesses + live-corpus clean-tree + RED perturb receipts.

44 extdeps modules carry external anchors; 125 remain in the shrinking
backfill_pending snapshot.

Reconciliation onto current main: the snapshot keys on declared module name, so
the post-#5391 directory reorganizations (rust/, package_managers/, ...) need no
rename. The only stale entry, extdeps.diagnostic.redfish, was dropped (redfish
moved to extdeps.bmc.redfish, separately covered).

Verified by execution: 18 projection unit tests; 14 floor-enrolled .dag witnesses
(GREEN clean-tree + machinery-exempt fold + 3 RED perturbs + live anchor-drop RED);
live-tree discrimination on a real cited module (Https->File and anchor-drop both
flip the gate RED, revert restores GREEN); ci_spec/ci_floor_plan enrollment
witnesses; gate main -> ExitSuccess via real shell; cargo fmt + clippy -D warnings.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_019Mi3t2wX7UPzgqLyYAE1kS

* ci_floor_plan: add missing gate_is_heavy_resolve arm for ExtdepsExternalAuthorityGate

#5418 added ExtdepsExternalAuthorityGate to the Gate enum and to every match
over it EXCEPT gate_is_heavy_resolve (ci_floor_plan.dag:154), so once the v1↔v2
FreeMonoid collision cleared (#5422 now in this branch) the plan resolve reached
this fn and fail-closed on a non-exhaustive match:

  ci_floor_plan.dag:154:3: error: non-exhaustive match:
    missing variant(s) ExtdepsExternalAuthorityGate

The extdeps external-authority gate is a focused lens witness (filesystem_read
over dsl/extdeps/**), not a whole-tree heavy resolve like SourceRootIngest /
DslCompileClean — so it joins the other lens gates (Layering/ResolvedImports) at
`false`. Plan-data only; resolved at runtime by claim_executor, no stage0 seed.

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

* extdeps live-clean: anchor the 4 access modules + backfill the cache key-completeness lens

#5418's external-authority gate scans the LIVE extdeps tree and fail-closes on any
module lacking an anchor. Once #5422 cleared the FreeMonoid collision and the missing
gate_is_heavy_resolve arm let the plan resolve, the gate correctly flagged 5 modules
that landed on main AFTER #5418 authored its roster and were neither anchored nor
backfilled:

  missing: extdeps.access.{aws_iam,posix,rbac,zanzibar}   (#5415 access model)
  missing: extdeps.cache.key_completeness                 (#5423 cache lens)

The 4 access modules already carry their real upstream citation in a `// Source:`
comment (AWS IAM grammar, POSIX.1-2017/opengroup, ANSI/NIST RBAC, the Zanzibar USENIX
paper) — promoted each to the structured `extdeps_external_authority_anchor` carrier
the gate gates on (DESIGN §3: the mark on the carrier is the authority). No access
sibling is backfilled, so anchoring (not backfilling) is the consistent treatment.

extdeps.cache.key_completeness is an internal §5 cache-soundness LENS (a pure reader
over the cache catalog), not a cited external-system model — so it joins its 8
extdeps.cache.* siblings on the backfill_pending roster as tracked debt, not a fake
external anchor.

Verified by execution: the floor's discovery-corpus (587 witnesses) and
extdeps_external_authority_gate_passes both go GREEN with this change (live
violation set empty, roster count > 150).

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

---------

Co-authored-by: Claude <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>
gunbai-bot Bot pushed a commit that referenced this pull request Jun 22, 2026
… green-fixpoint yet)

Re-repair the .dag authority so it matches the committed seed's end products,
reducing the regen drift surface. Additive, cargo-green on the current seed; the
clean green regen fixpoint + the drift-gate are deferred (they converge with the
Route-A emitter self-host, since regen-write still emits a non-building seed from
~150 emitter-completeness gaps, not these pieces).

.dag authority (single-authority, no hand-Rust-logic in seed):
- runtime_rust.dag: add host-fn bytes_identity_hash (byte-level authority);
  atom_identity_hash now delegates to it.
- compile.dag: model compile_to_resolved_discovery_corpus_advisory +
  compile_to_resolved_with_options_gated + is_resolved_pipeline_typecheck_blocking;
  import is_discovery_corpus_blocking_diagnostic.
- 05_emit_rust.dag emit_lib_rs hand-module list + regen_stage0.rs
  HAND_MAINTAINED_STAGE0_FILES: wire doc_reachability_project and the two further
  drifted-in hand modules cache_purity_oracle + medium_structure_project (#5423/#5500).

Mirror sync (generated .rs kept in lockstep with the .dag edits, concat-associative):
- v1_compiler_emit_rust.rs hand_maintained_mods string == the .dag list.
- v1_compiler_runtime_rust.rs rt_hash_ops emits bytes_identity_hash + delegation.
- v1_compiler_compile.rs already carried the advisory family (consistent).

Also fix a leftover v2->v1 rename in a regen_stage0 unit test fixture (#5028).

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
briansrls added a commit that referenced this pull request Jun 22, 2026
…achability + 2 drifted hand-mods, bytes_identity_hash host-fn, advisory family) (#5514)

* WIP: Stage0 regen-lockstep RE-REPAIR plus a regen-equals-committed CI drift-g

* WIP: Stage0 regen-lockstep RE-REPAIR plus a regen-equals-committed CI drift-g

* WIP: Stage0 regen-lockstep RE-REPAIR plus a regen-equals-committed CI drift-g

* Stage0 regen lockstep: .dag authority pieces + consistent mirrors (no green-fixpoint yet)

Re-repair the .dag authority so it matches the committed seed's end products,
reducing the regen drift surface. Additive, cargo-green on the current seed; the
clean green regen fixpoint + the drift-gate are deferred (they converge with the
Route-A emitter self-host, since regen-write still emits a non-building seed from
~150 emitter-completeness gaps, not these pieces).

.dag authority (single-authority, no hand-Rust-logic in seed):
- runtime_rust.dag: add host-fn bytes_identity_hash (byte-level authority);
  atom_identity_hash now delegates to it.
- compile.dag: model compile_to_resolved_discovery_corpus_advisory +
  compile_to_resolved_with_options_gated + is_resolved_pipeline_typecheck_blocking;
  import is_discovery_corpus_blocking_diagnostic.
- 05_emit_rust.dag emit_lib_rs hand-module list + regen_stage0.rs
  HAND_MAINTAINED_STAGE0_FILES: wire doc_reachability_project and the two further
  drifted-in hand modules cache_purity_oracle + medium_structure_project (#5423/#5500).

Mirror sync (generated .rs kept in lockstep with the .dag edits, concat-associative):
- v1_compiler_emit_rust.rs hand_maintained_mods string == the .dag list.
- v1_compiler_runtime_rust.rs rt_hash_ops emits bytes_identity_hash + delegation.
- v1_compiler_compile.rs already carried the advisory family (consistent).

Also fix a leftover v2->v1 rename in a regen_stage0 unit test fixture (#5028).

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

---------

Co-authored-by: Brian Searls <briansearls1@gmail.com>
Co-authored-by: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant