Repository navigation
docs(ROADMAP): log P4 debt — surface int-literals host-narrowed at concept layer - #745
Merged
Merged
Conversation
Amendment bundling three artifacts that promote the proposal at PR #695 from architectural proposal into committed post-R1 program scope. 1. THESIS.md — add "Grounding completeness" as a Tier 1 structural-correctness claim. Target-side primitive types are structurally modeled from target language references (Rust Reference §Types, Python data model, Go specification), with algebra inhabitance declared structurally rather than as string-typed shortcuts in a lookup table. Coercion becomes a structural algebra-homomorphism search. Fail-closed on ungrounded types. Cites single-emitter-design.md for architecture and target-grounding-proposal.md for the concrete work breakdown. 2. ROADMAP.md — add "Post-R1 Program — Grounding Completeness" section between R1 and the status-at-a-glance table. Decomposes into seven lanes: - T-Ground-Pilot (S, Day-1 no blockers; Rust integer family) - T-Ground-Rust (XL, blocks on DB-11 + cardinality-substrate) - T-Ground-Python (L, same substrate blockers) - T-Ground-Go (L, same) - T-Ground-Engine (M, inhabitance-search walker) - T-Ground-Tests (S, routing-stability + L4 witness cert) - T-Ground-Dissolve (S, Track 13 closure single PR) Critical path: Pilot → Rust → Engine → Tests → Dissolve. Python/Go parallel after Pilot. Acceptance gates named for future TestClaim authoring. 3. docs/briefs/grounding-manager.md — Grounding Manager brief authored under the same governance model as R1 managers. Slice declaration, sequence + dispatch, hand-off points to Surface/Testgen/Director, pilot-gate acceptance as the dispatch gate for the whole program, working-state checklist per lane. Rationale (user framing, this PR's originating message): "i think its a good representation of correctness - without it, i feel like the project is half baked." Grounding-completeness as a first-class Tier 1 claim closes the gap where the user-side algebra is structurally modeled but the target-side is a string lookup. The thesis's "structure, not declaration" discipline applies at the realization boundary too; this program lands the infrastructure that makes that true. Relationship to related in-flight work: - PR #695 (target-grounding-proposal.md) stays PROPOSAL mode until this amendment merges; a follow-up PR then flips its status line from "PROPOSAL" to "committed design spec for the ROADMAP Grounding Completeness program." - Architectural parent docs/single-emitter-design.md remains the coercion-is-emission authority; this program is its concrete dispatch path. - R1 Director Brief's escalation model continues to apply (scope changes route to director). Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Per session discussion, the T-Ground-Dissolve lane should
explicitly commit to deleting the entire coercion scaffolding
surface, not just its routing-path usage. The prior wording said
"TypeCheckpoint / InhabitantDecl declarations survive as testgen-
assertion inputs per verifiability-invariant.md L0 role" — that
graduation framing is the wrong direction. Routing-stability
assertions are better authored as direct TestClaim declarations
under T-Ground-Tests; the scaffolding has no surviving role.
Updated in two places:
1. ROADMAP.md T-Ground-Dissolve row scope: now names
dsl/std/coercion.dag (the schema file), the per-target
dsl/extdeps/languages/{rust,python,go,dag}/types.dag tables,
and TypeRealization.carrier: String field deletion
explicitly. Also removes the "graduate to testgen-assertion
role" caveat — TestClaim declarations under T-Ground-Tests
own the assertion surface directly.
2. Grounding Manager brief Sequence + dispatch and Working
state sections: enumerated per-file deletions (5 files
total); working-state checklist expanded from 2 items to
10, one per concrete deletion, ensuring the closure PR's
scope is mechanically tracked.
User framing: "I would also make sure to include the deletion
of coercion.dag as a requirement" — this commits it.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
…ompleteness-program
Codex P2 on PR #721 caught that grounding-manager.md:15's link to docs/thesis/target-grounding-proposal.md is dangling — the file doesn't exist on main (it's on PR #695's branch, pending merge). Same issue at three other sites: - ROADMAP.md:141 (program intro text) - ROADMAP.md:155 (T-Ground-Engine lane description) - THESIS.md:173 (Grounding completeness claim) - docs/briefs/grounding-manager.md:73 (adjacent mention) Chose to annotate each reference with explicit PR #695 dependency rather than remove/weaken the refs. This makes the merge-order dependency transparent: PR #695 merges first (target-grounding proposal lands on main), then this amendment (#721) merges with the file refs resolving. Until #695 merges, readers of this amendment see "[PR #695](link), landing at path on merge" rather than a broken filesystem link. All five sites consistently annotate: - THESIS.md:173 (Grounding completeness Tier 1 claim) - ROADMAP.md:141 (program intro) - ROADMAP.md:155 (T-Ground-Engine lane row) - docs/briefs/grounding-manager.md:15 (primary work-breakdown reference) - docs/briefs/grounding-manager.md:73 (secondary mention) When #695 merges, a follow-up can clean the "landing at ... on merge" language down to direct file references — ~5 line edits. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Codex review on PR #721 (sha:408743c2) caught that grounding-manager.md's citation of ROADMAP.md:305 for the cardinality-substrate blocker now resolves to "Compiler-std consolidation" instead — line numbers have drifted since I drafted the brief (tracked-debt ledger grew as work landed on main). The actual cardinality-substrate row is now at ROADMAP.md:338. Fixed the citation to be drift-resistant: name the row title explicitly ("Fixed-width types aren't structurally fixed") and give the current line number as a hint, with an explicit note that line numbers drift and search by title is preferred. The other finding in the same codex review — that target-grounding-proposal.md doesn't resolve in-tree — was the same finding the inline comment at the same sha flagged. Already addressed in 4275226 which annotates all five refs with explicit PR #695 dependency. No change needed here. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Codex review inline on PR #721 (sha:408743c2, THESIS.md:173 + ROADMAP.md:152) flagged a faithfulness violation on the T-Ground-Rust lane: the description claimed "systematic Rust Reference §Types coverage" but mixed std-library carriers (String, Vec, Box, Rc, Arc) into that authority. std-library types are NOT in Rust Reference §Types — they have separate std documentation. Also missed reference-listed forms: `impl Trait` and function pointer types (`fn(...) -> ...`) distinct from function item / closure types. Per MODELING M3 / INVARIANTS P1 Modeling Faithfulness — the external-spec grounding has to be faithful, which means authority boundaries must not be blurred. Fix: split each language lane into two-authority modeling with explicit categories: **Rust (T-Ground-Rust):** (a) Rust Reference §Types — boolean, numeric, textual (char, str), never, tuple, array, slice, struct, enum, union, function item, function pointer, closure, reference, raw pointer, trait object, impl Trait. URL-cited authority. (b) Std-library carriers — String, Vec<T>, Box<T>, Rc<T>, Arc<T>, HashMap, BTreeMap, HashSet, BTreeSet, Option, Result. std documentation is the authority, separate from the reference. **Python (T-Ground-Python):** (a) Python language reference built-ins (numeric, bool, None, sequences, text, binary, mappings, sets, callables, modules, classes). (b) CPython stdlib (typing, collections) when scope grows beyond built-ins. **Go (T-Ground-Go):** (a) Go language specification (https://go.dev/ref/spec) — boolean, numeric, string, array, slice, struct, pointer, function, interface, map, channel. (b) Go standard library carriers when modeling beyond spec. Applied in both ROADMAP.md (the lane-authority table) and the Grounding Manager brief's slice declaration. Each category now cites its own source-of-record; mixing is called out explicitly as prohibited. Dropped mentions added previously: impl Trait, function pointer types for Rust (both were missing); added URL citations for Go spec (was just "Go specification" before). Note: the dangling-link finding at THESIS.md:173 in the same review round was already fixed by 4275226 + annotated with PR #695 dependency. No action there. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
…ompleteness-program
…ompleteness-program
…ompleteness-program
…ompleteness-program
…ompleteness-program
…ompleteness-program
…ompleteness-program
…ompleteness-program
…ompleteness-program
…ompleteness-program
…ompleteness-program
…ompleteness-program
…ompleteness-program
…ompleteness-program
…ncept layer Logged as a P4 (type refinement / modeling faithfulness) sibling to the existing fixed-width-types row. Surfaced 2026-04-24 by substrate lane-owner analysis of the i64::MIN literal edge: `IntLit(Int)` at `src/v3/std/tokenize.dag:30` where `Int = Int64` means the lexer's digit-run → token concept is already host-narrowed to i64 at the tokenizer boundary, so `2^63` magnitude is unrepresentable. Dissolution direction recorded: `IntLit` carries an unbounded magnitude at the concept layer, narrows to target int algebra at reconciliation; negation stays `OrderedRing` additive-inverse (no unary-minus parse primary — `parse_tables.dag:413-448` closes that set with a full 4-pattern audit). Adjacent to the Post-R1 Grounding Completeness Program as a natural surface-side Tier-1 vignette. No R1 gate blocks on this; `(0 - MAX - 1)` is a correct workaround under ring arithmetic. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
briansrls
added a commit
that referenced
this pull request
Apr 24, 2026
The `src/v3/compiler/tokenize.dag` entry drifted on main since #744 (PR #739 / #745 CI runs on main also fail this test). Refreshed via `cargo test -p v3-compiler refresh_handwritten_parse_snapshot_manifest -- --ignored` so this PR unblocks and the pending merge queue clears. Ride-along with PR #746 docs-only work. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
briansrls
added a commit
that referenced
this pull request
Apr 24, 2026
* WIP: T-PB-B * WIP: T-PB-B * WIP: T-PB-B * WIP: T-PB-B * WIP: T-PB-B * WIP: T-PB-B * chore: refresh parse_corpus_manifest.txt after main-side drift The `src/v3/compiler/tokenize.dag` entry drifted on main since #744 (PR #739 / #745 CI runs on main also fail this test). Refreshed via `cargo test -p v3-compiler refresh_handwritten_parse_snapshot_manifest -- --ignored` so this PR unblocks and the pending merge queue clears. Ride-along with PR #746 docs-only work. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> --------- Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
1 task done
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
ROADMAP.mdas a sibling to the existing fixed-width-types entry.i64::MINliteral edge:IntLit(Int)atsrc/v3/std/tokenize.dag:30withInt = Int64 = OrderedRing<Word64>means the lexer's digit-run → token concept is already narrowed to hosti64at the tokenizer boundary, so2^63magnitude is unrepresentable.UInt64 2^64-1and silent narrowing of typed numerics in non-Int64contexts.Dissolution direction (recorded in the entry)
IntLitcarries an unbounded magnitude at the concept layer (candidate:std.natural), narrows to target int algebra at reconciliation.OrderedRingadditive-inverse — no unary-minus parse primary is needed.src/v3/compiler/parse_tables.dag:413-448already documents the closed-set prefix-opener dispatch with a full 4-pattern dissolution audit;-x = 0 - xdesugars principally under the ring.Why now
(0 - MAX - 1)is correct under ring arithmetic and is the attested workaround.Test plan
🤖 Generated with Claude Code