Repository navigation
ROADMAP §0+§6: realization-vocabulary containment guard + emission=ingestion⁻¹ past syntax - #5442
Merged
Merged
Conversation
…plan (de-fork zesty-deer-479 owner, absorb quick-ant-298 spine) Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
…p keystone) + precise v1 cutover Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
…ebsite 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>
…ck-down LANE (audits→fixes→meta), name model<->realization fork as suspected root Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
… 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>
…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>
…sions'
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>
…rtition §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>
…ator, 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>
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>
# Conflicts: # ROADMAP.md # docs/plans/dsl-v2-defork-audit.md # docs/plans/idea-machine.md # docs/plans/realization-measurement-loop.md # docs/plans/testgen-oracle.md # docs/plans/v2-self-hosting.md
…e, 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>
…maining 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>
…d-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>
…ce-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>
…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>
…sition), 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>
…gine 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>
gunbai-bot
Bot
changed the title
…oster (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>
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>
…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>
…ached-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>
… (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>
…O + 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>
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.
Two operator-approved roadmap items from warm-lark-306's bash-sidecar audit, routed through me (single ROADMAP writer) as one PR to avoid both a #5436-style concurrent-edit collision and a dangling-doc-pointer.
The audit
dsl/tools/build_step.dag'sbuild_verify_echohand-authors bash (echo … >&2) and the GitHub-Actions::error::annotation in one function → it can never re-emit to Rust (anemic). The sweep found 9.dagconsumers importing the bash-AST sidecar (extdeps.languages.bash.program) to express portable intent, becauseemission = ingestion⁻¹(the row-driven inverse already realized for language emit in06_translate) was never extended to the intent/effect layer.The two items
lens/layering_importsforbidden-edge machinery (N+M, not a new lens), forbidding target-AST imports outside the realization edge. Ships as a shrinking 9-importer ratchet with dissolve-on = bash-sidecar arc empties the roster → flips to a pure wall →program.dagdeletable.emit ∘ ingest = idround-trip law, honest per-medium viaDecodeFidelity.Review-cleanliness
Both items declare their cross-arc edges inline (guard ↔ bash-sidecar arc ↔ §6) to avoid reintroducing the bright-eagle-46 undeclared-edge class that #5426 just fixed. Architecture lives in the new plan doc (
docs/plans/emission-ingestion-inverse.md) per DESIGN no-dual-representation; the ROADMAP items are thin pointers into it (both land in this PR, so nothing dangles).The §0-guard implementation and an independent
lit("dsl")§3-hygiene cleanup found in the same sweep are dispatched separately by warm-lark-306 — not part of this doc PR.🤖 Generated with Claude Code