Skip to content

PM May 24 - #3653

Merged
briansrls merged 40 commits into
mainfrom
docs/v4-compilation-milestones
May 25, 2026
Merged

briansrls merged 40 commits into
mainfrom
docs/v4-compilation-milestones

Conversation

@briansrls

Copy link
Copy Markdown
Contributor

Auto-opened by session-dashboard for session loyal-stag-23.
Pushing to docs/v4-compilation-milestones advances this PR.

Worker attestation

Before flipping this PR to ready for review, confirm each item:

  • Title describes the change (not the session id or branch).
  • PR body summarises what and why (replace the TODO below).
  • Tests run: name the command (e.g. npm test, cargo test) and the result.
  • If this closes a work item, the body contains a Closes #N directive.
  • No commits on this branch are surprises (no fork/cherry-pick I did not make).
  • No secrets / credentials / large binaries staged.

Summary

TODO: replace this paragraph with one or two sentences naming the change and its motivation. Reviewers read this first.

Test plan

  • TODO: list the commands that ran (or "no tests changed; relied on CI") and the outcome.

briansrls and others added 8 commits May 25, 2026 01:29
…ncing

- 04_infer.dag: add algebra_ref_is_grounded guard in
  canonical_grounding_from_inferred_facts; fires infer_algebra_ref_ungrounded
  when AlgebraRef.algebra is a bare Atom (bridge symbol or scaffolded identity
  solver). New helpers: algebra_connective_is_atom, algebra_ref_is_grounded,
  infer_algebra_ref_ungrounded{,_diagnostic}. Imports Atom/Connective/TypeNode.

- TASKS.md T-2: add explicit Node-constructor deliverable (ordered_ring_node()
  → Node etc.) as a gate for T-4 Wave 2b.

- TASKS.md T-4 Wave 2b: tighten [needs] to include T-2 Node constructors;
  explain that bridge-symbol algebra fields fail-closed at T-9.

- model_core.dag: fix wave1_void dissolution condition — two-part: non-empty
  ModelCore AND no bare-Atom AlgebraInhabitanceDecl.algebra fields.

- rust.dag: mark bridge symbols (rust_model_core_bridge_*) as 🟡 scaffolds
  with explicit dissolve-on: T-2 Node constructors + T-4 Wave 2b.

- test/claim/manual/infer_algebra_ref_grounding_anchor.dag: Option B behavior
  receipts — algebra_ref_is_grounded unit checks + canonical_grounding_from_
  inferred_facts rejection anchor for bare-Atom algebra.

Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
algebra_connective_is_atom was a hand-rolled Bool predicate over the
Connective coproduct (match → true/false per variant) with no dissolution
disposition — exactly Practice 10's blocking predicate-dissolution shape.

Fix: inline the nested pattern into algebra_ref_is_grounded using a
single TypeNode { connective: Atom { identity: _ } } arm, eliminating
the Bool predicate over Connective entirely. Drop Connective from the
import (no longer needed as an explicit type). Add a 🟡 predicate-
dissolution interim tag to algebra_ref_is_grounded itself, which also
matches the *_is_* Bool-over-Node mechanical trigger.

Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
algebra_ref_is_grounded's wildcard arm `_ => true` silently passed
ComputationNode algebra evidence as grounded. Computation nodes are
never valid algebra types — only TypeNode shapes are (Conj, Arrow,
Instantiation, etc.).

Fix: replace the catch-all with a two-arm exhaustive match over the
node kind coproduct. TypeNode dispatches to an inner match on the
connective (Atom { identity: _ } => false, _ => true). ComputationNode
explicitly returns false. Adds ComputationNode to the v4.std.node import.

Test claim: add algebra_ref_computation_node_is_ungrounded receipt
(ComputationNode → !grounded) alongside the existing Atom/Conj cases.

Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
…hor.dag

v4 parser requires data declaration expressions on the same line as =;
multiline form triggered parse error at CI.

Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
Maps bootstrap.dag's four-stage chain (seed→stage0→stage1→stage2)
to observable milestones with explicit evidence criteria and known
blockers. Surfaces the current gap: CI runs --target dag (structural
check) but the --target rust → rustc → binary step (M1) has never
been wired. Identifies four design gaps requiring operator decisions
before dispatch.

Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
@briansrls
briansrls marked this pull request as ready for review May 25, 2026 04:34
…ro mandate

Gap 2 previously framed 'write in Rust vs .dag' as an open operator
choice. Per THESIS.md and design-pure-bootstrap-zero.md, v4 compiler
logic must be authored in .dag; a Rust path would be a named P5 scaffold
requiring an explicit dissolution receipt. Reframe: M2 depends on the
eval track (T-34→T-22), dispatch both tracks in parallel.

Addresses codex REQUEST_CHANGES on PR #3653.

Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>

@briansrls briansrls left a comment

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Review metadata

  • Provider / model: codex / unknown
  • Commit: 727517a4 · Trigger: schedule
  • Thinking: 253s wall

BLOCKING (3)

Root Cause

  • docs/v4-compilation-milestones.md The milestone model collapsed the canonical compiler spine after parse → include T-8 normalize/resolve and T-9 infer in M2 required work/dependencies before treating T-10 as the emit gate.
  • docs/v4-compilation-milestones.md Pure Bootstrap Zero's ".dag-authored" mandate was conflated with "must run through the eval interpreter" → keep T-6/T-7 authored in .dag, but route M2 through the emitted stage0 compiler pipeline unless a higher authority changes TASKS.
  • docs/v4-compilation-milestones.md The milestone snapshot was authored from an older Wave-1 parser state → refresh T-7 status from the current 02_parse.dag and name the remaining parser gaps precisely.

⚠️ The new planning authority needs its M2/T-7 dependency model reconciled with the current v4 compiler spine before merge.

Comment thread docs/v4-compilation-milestones.md Outdated
- Implement parser walk in 02_parse.dag (algorithm, 1 worker, ~200-400 lines)
- Wire T-10 emit to produce real Rust source text from a translated node tree

**Sequential dependency:** T-6 walk → T-7 walk → T-10 emit → M2.

This comment was marked as resolved.

Comment thread docs/v4-compilation-milestones.md Outdated
explicit dissolution receipt naming the exact trigger (T-22+T-34 running the .dag
walks) before a worker can be dispatched on a Rust path.

The consequence: **M2 depends on the eval track.** T-6/T-7 walks written in .dag

This comment was marked as resolved.

Comment thread docs/v4-compilation-milestones.md Outdated

**Known blockers:**
1. **T-6 lexer walk ("not realized").** `01_tokenize.dag` has `ModeledLexRules { root: _ } → Rejected("lexical walk not realized")`. The lex rule data is modeled but the walk algorithm that uses it is a stub. This MUST be real for M2. One worker, one file.
2. **T-7 parser walk ("not realized").** Same pattern in `02_parse.dag`. `ModeledGrammar { root: _ } → Rejected("grammar walk not realized")`. dag.dag grammar data is filled; the walk algorithm is not.

This comment was marked as resolved.

briansrls and others added 2 commits May 25, 2026 04:50
Line 119: T-7 blocker description was stale — parse() now dispatches
through parse_production; remaining stub is parse_expr (🟡 gated).

Line 128: M2 dependency chain omitted T-8 and T-9. Added them with
accurate status (modeled, in chain, not additional blockers for trivial
single-file input).

Line 218: Gap 2 incorrectly claimed M2 depends on T-22/T-34. Corrected:
T-6/T-7 walks are authored in .dag, v2 emits Rust from them (--target
rust), stage0 runs them natively. T-22/T-34 is the eval/TestClaim track
only, genuinely independent of the compiler pipeline at M2.

Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
@briansrls

Copy link
Copy Markdown
Contributor Author

Relay finding at line 119 (T-7 description stale) is addressed in 9b0cc93 — the description was updated to accurately reflect the post-#3626 state: parse() now dispatches through grammar_lookup_production → parse_production → parse_expr; parse_expr is the remaining stub with its 🟡 gated — feature:T-7-parse-walk-realization marker. All three blockers from the codex review on 727517a are resolved in 9b0cc93.

— sent from loyal-stag-23

Finding 1 (M0 evidence overstates CI green): The CI gate has two arms —
full compile receipt and resolve-posture bridge receipt. M0 status is
only confirmed by the full-compile arm. Clarify what each receipt proves
and instruct readers to check the gate log.

Finding 2 (T-28 description wrong): resolve_with_graph passes the
ModuleGraph to namespace_from_tree_and_graph; the 🟡 gate is on
namespace_from_tree_and_graph (does not walk ModuleGraph.entries), not
on resolve_with_graph dropping the parameter. Both occurrences fixed
(M3 blockers and Gap 3).

Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
@briansrls

Copy link
Copy Markdown
Contributor Author

Addressed both cursor/composer-2.5 findings in 43c466c:

Finding 1 (M0 evidence overstates CI green): The CI gate has two arms — full compile receipt and resolve-posture bridge receipt. M0 is only confirmed by the full-compile arm. Updated Evidence block to distinguish the two arms and explain what each proves. The Status line now notes that CI green must be verified as the full-compile arm before treating it as M0 confirmation.

Finding 2 (T-28 description wrong): The 🟡 gate is at namespace_from_tree_and_graph (line 564-570 of 03_resolve.dag), which receives the ModuleGraph but does not walk ModuleGraph.entries. resolve_with_graph itself passes the graph through — it does not drop it. Both occurrences (M3 blockers section and Gap 3) corrected to name the actual gated function.

— sent from loyal-stag-23

dag_wave1_grammar() (ModeledGrammar with production bodies) exists but
neither pipeline-facing LM function uses it — both call
dag_wave1_g0_void_grammar() (VoidGrammar). parse() dispatches VoidGrammar
to the accept-empty arm, so any real program input is rejected at parse.

This is not T-7 scope (generic walk algorithm); it is dag.dag data wiring,
a separate follow-on task. Named and scoped correctly per nimble-koi-111
independent verification.

Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
@briansrls

Copy link
Copy Markdown
Contributor Author

Added dag.dag LM wiring as an explicit M2 blocker in d72f3b7 (per nimble-koi-111 independent verification + scope ruling).

Finding: dag_wave1_grammar() → ModeledGrammar exists in dag.dag but neither pipeline-facing LM function uses it — both call dag_wave1_g0_void_grammar() (VoidGrammar). parse() dispatches VoidGrammar to the accept-empty arm, rejecting any real program input at parse. Adding a pipeline-facing dag_language_model_wave1() using ModeledGrammar is not T-7 scope (generic walk algorithm) — it is dag.dag data wiring, a separate follow-on task.

Blocker 3 now names this explicitly. Blocker 4 (was 3) and 5 (was 4) renumbered.

— sent from loyal-stag-23

@briansrls

Copy link
Copy Markdown
Contributor Author

Reviewing the claims in docs/v4-compilation-milestones.md, I think this needs revision before merging. The high-level framing is useful, but a few claims are inaccurate or internally inconsistent against the current repo state.

Findings:

  1. docs/v4-compilation-milestones.md:94 / :205 claim no CI step runs --target rust over all of src/v4. That is false. The T-22 host eval CI receipt runs scripts/check-v4-host-eval-receipt.py, which sets SOURCE_ROOT = src/v4 and invokes v2-compiler compile --source-root src/v4 --target rust, then checks the clean compile receipt. The real missing piece appears to be full emitted-crate link/build/run, not full-tree Rust emission.

  2. docs/v4-compilation-milestones.md:128 says M2 has only serial blockers T-6 -> T-7 -> T-10, but :218 and :246 say M2 depends on T-22/T-34. Those claims conflict. src/v4/TASKS.md lists the compiler critical path as T-6 -> T-7 -> T-8 -> T-9 -> T-10; T-22 is the sibling eval/TestClaim path, not listed as a prerequisite for the compile pipeline. Pure Bootstrap supports authoring compiler behavior in .dag, but I do not see authority for “T-6/T-7 cannot execute until T-22/T-34” in the generated-Rust stage0 path.

  3. docs/v4-compilation-milestones.md:57 says “CURRENT, CI green.” Current PR checks were still pending when checked. The gate exists, and recent main runs include successes, but a planning doc should avoid claiming “CI green” without pinning a specific run/date or wording it as “expected/current gate.”

  4. docs/v4-compilation-milestones.md:191 overstates eval as “nothing can execute.” Some wave-1 runtime hooks accept literals/binds; the rejecting hooks are the nontrivial transform/branch/loop/call path in src/v4/extdeps/runtimes/v4_evaluator.dag.

Most other claims checked out: bootstrap.dag models the seed/stage0/stage1/stage2 chain, CI bootstrap viability uses --target dag, tokenize/parse modeled walks are still stubbed, and resolve_with_graph currently ignores the module graph. The main fix is to revise the M1/M2 dependency story so it matches existing CI and TASKS.md.

briansrls and others added 2 commits May 25, 2026 05:23
Finding 1 (M1 --target rust already in CI): The T-22 host eval receipt
already runs --target rust src/v4 with zero v2 diagnostics. Corrected
doc to say what's missing is cargo check/build of the emitted crate,
not the emission step itself. Updated M1 definition, blockers, Gap 1,
and the current-CI-state table accordingly.

Finding 2 (parallel track table implies M2 requires T-22): Added explicit
note that the eval-track column is NOT a prerequisite for the compiler-
track row. Reformatted table header to avoid co-dependency misread.

Finding 3 (heading "CI green"): Removed snapshot CI claim from section
heading; CI status belongs in the body, not the title.

Finding 4 (eval "nothing can execute" too strong): Named which hooks
are deferred (call_primitive, choose_branch, step_loop, call,
represent_literal, all arms of transfer) vs. which accept (bind_value,
allocate, return_value, terminal_value Continue/Return arms). Replaced
"nothing can execute" with "no nontrivial expression can evaluate
end-to-end while transfer rejects all control-transfer arms."

Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
@briansrls

Copy link
Copy Markdown
Contributor Author

All four findings are valid. Fixed in 7b77fe9:

Finding 1 (M1 --target rust already in CI): check-v4-host-eval-receipt.py already runs --source-root src/v4 --target rust with zero v2 diagnostics. The doc incorrectly said 'no CI step runs --target rust over full src/v4.' Corrected: the Rust emission step exists; what's missing is cargo check/cargo build of the emitted crate. Updated M1 definition, blockers (blocker 2 is now the ~4,900 rustc errors from PR #3654), Gap 1, and the current-CI-state paragraph.

Finding 2 (parallel track table): Added an explicit note before the table: 'The eval track column is NOT a prerequisite for the compiler track row. M2 does not require T-22 or T-34.' Reformatted table header to make the independence unambiguous.

Finding 3 (heading 'CI green'): Changed 'CURRENT, CI green' → 'CURRENT STATE' in the M0 heading. CI status belongs in the body, not the title.

Finding 4 (eval 'nothing can execute' too strong): Named the deferred hooks precisely: call_primitive, choose_branch, step_loop, call, represent_literal, all arms of transfer. Named the accepting hooks: bind_value, allocate, return_value, terminal_value (Continue/Return arms). Changed 'nothing can execute' to 'no nontrivial expression can evaluate end-to-end while transfer rejects all control-transfer arms.'

— sent from loyal-stag-23

@briansrls briansrls left a comment

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Review metadata

  • Provider / model: codex / unknown
  • Commit: 7b77fe9d · Trigger: schedule
  • Thinking: 271s wall

BLOCKING (2)

Root Cause

  • docs/v4-compilation-milestones.md M2 models trivial emit as only the local compiler spine → add the T-4/T-33 side branch and algebra-grounding gates wherever T-9/T-10 require target facts.
  • docs/v4-compilation-milestones.md M4 collapses T-15 to hash equality after M3 → preserve TASKS' full T-15 gate, including T-16 and T-36 before fixed-point validation is meaningful.

⚠️ Two planning-authority contradictions remain and should be reconciled before merge.

Comment thread docs/v4-compilation-milestones.md Outdated
- Add `dag_language_model_wave1()` to dag.dag using `dag_wave1_grammar()` (not VoidGrammar) and wire into the pipeline
- Wire T-10 emit to produce real Rust source text from a translated node tree
- T-8 normalize + resolve: modeled and in the chain; single-file trivial input does not hit the T-28 cross-file bridge gate
- T-9 infer: modeled and in the chain; no additional work for trivial input

This comment was marked as resolved.

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Addressed in 8e4ae24. Line 146 now says: 'T-9 infer: modeled and in the chain; requires T-4 algebra grounding (formal TASKS.md prerequisite) — T-9 fail-closes on bare-Atom bridge symbols until T-4 fills real Node constructors for each algebra type.' T-4 and T-33 added as explicit M2 Known blockers (5 and 6) with TASKS.md line citations. Sequential dependency section updated to name the T-33 → T-4 → T-9 chain.

Comment thread docs/v4-compilation-milestones.md Outdated
**Status:** Defined structurally in bootstrap.dag (content hash pins are placeholder Symbols,
awaiting real B1 content_hash computation). Milestone reached only after M3 is stable.

**Note:** M4 is T-15. It is the "v4 done" gate per TASKS.md. All other tasks (T-16 omni

This comment was marked as resolved.

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Addressed in 8e4ae24. M4 Note now explicitly names T-16 and T-36 as prerequisites per TASKS.md lines 31-33 ('Both must be complete before T-15'), shows the critical path T-10 -> T-11 -> T-16 and T-36 both feeding T-15, and explains that asserting fixpoint before those gates is a correctness claim about an incomplete binary.

briansrls and others added 2 commits May 25, 2026 06:08
… in M4

Addresses codex BLOCKING review on 7b77fe9:

Finding 1 — M2 missing T-4/T-33 side branch and algebra-grounding gates:
TASKS.md line 42 states T-9 [needs T-8, T-2, T-3, and T-4]; line 43 states
T-10 [needs T-9, T-4]. T-9 infer rejects bare-Atom algebra refs via
infer_algebra_ref_ungrounded until T-4 Wave 2b fills real Node constructors
(ordered_ring_node, etc.) for AlgebraInhabitanceDecl.algebra. Added as
blockers 5 and 6 with precise TASKS.md citations. Updated Required Work and
Sequential dependency sections accordingly.

Finding 2 — M4 treats T-16/T-36 as optional when TASKS.md makes them prerequisites:
TASKS.md lines 31-33: "Both must be complete before T-15." Fixed M4 Note to
state T-16 and T-36 are prerequisites, cite the critical path
T-10 → T-11 → T-16 and T-36 → T-15, and explain why asserting fixpoint
before those gates is a claim about an incomplete binary.

Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
@briansrls

Copy link
Copy Markdown
Contributor Author

Addressed both codex BLOCKING findings from review on 7b77fe9 in 8e4ae24:

Finding 1 — M2 missing T-4/T-33 side branch:
TASKS.md line 42: "T-9 [needs T-8, T-2, T-3, and T-4]"; line 43: "T-10 [needs T-9, T-4]." Added as M2 Known blockers 5 and 6:

  • Blocker 5 (T-4): T-9 infer rejects bare-Atom algebra references via infer_algebra_ref_ungrounded. rust.dag uses bridge Symbols as placeholders (e.g., rust_model_core_bridge_std_ordered_ring_representable_integer) that fail-closed at T-9 until T-4 Wave 2b fills real Node constructors (ordered_ring_node(inhabitant: Node) -> Node, etc.). Applies even for trivial fn add(a, b) = a + b targeting Rust.
  • Blocker 6 (T-33): T-4 cannot ground primitives or algebra references without std/model_core.dag (T-33). Side branch {P1-KEYSTONE, T-30, T-29, T-25-core, T-33} → T-4 → T-9 is a watch item per TASKS.md.
    Required Work and Sequential dependency sections updated to reflect formal TASKS.md prerequisites.

Finding 2 — M4 collapsed T-15 to hash equality, treating T-16/T-36 as optional:
TASKS.md lines 31–33: "T-11 → T-16 (full-stack omni-emission demo) and T-36 (ingest round-trip fidelity claim). Both must be complete before T-15." Fixed M4 Note to name T-16 and T-36 as prerequisites with explicit citation, show the critical path T-10 → T-11 → T-16 and T-36 both feeding T-15, and explain that asserting fixpoint before those gates is a correctness claim about an incomplete binary.

— sent from loyal-stag-23

@briansrls

Copy link
Copy Markdown
Contributor Author

Review metadata

  • Provider / model: openai-pro / gpt-5-5-pro
  • Commit: 8e4ae248 · Trigger: manual
  • Comparison: main @ 3a9be658 ... docs/v4-compilation-milestones @ 8e4ae248
  • Conversation: View conversation

1. Story of the diff

This PR adds a new planning document, docs/v4-compilation-milestones.md, whose job is to define observable v4 compilation milestones rather than edit compiler behavior directly. The doc separates structural .dag compilation, Rust emission, and full bootstrap into distinct evidence levels (docs/v4-compilation-milestones.md:38-56), then walks M0 through M4: M0 is current structural compile, M1 is emitted Rust linking to a runnable stage0, M2 is stage0 compiling a trivial program, M3 is stage0 producing stage1 from src/v4, and M4 is the bit-identical fixed point (docs/v4-compilation-milestones.md:60-238). The load-bearing intent is good: it tries to prevent CI’s current “compile” language from being mistaken for a runnable v4 binary, and it names the compiler-pipeline track separately from the TestClaim/eval track (docs/v4-compilation-milestones.md:203-238). The risk is that because this is a planning authority, imprecise milestone labels become dispatch instructions.

2. Invariant categories

  1. LAYER MODEL (substrate vs implementation).

N/A — this is a docs-only PR; it does not introduce or modify substrate types, Dag storage, cross-pass carriers, .dag variants, or reusable algebraic helpers.

  1. INVARIANTS.md + modeling-discipline.md.

Compliant — fail-closed / no fabricated success: M0 explicitly distinguishes the full compile receipt from the resolve-posture bridge and says the bridge does not guarantee zero diagnostics or full parse coverage (docs/v4-compilation-milestones.md:64-82). That is the right shape for avoiding a fabricated “M0 achieved” claim.

  1. CODING.md.

N/A — no Rust code or implementation helpers are changed; CODING.md’s data/free-function, method, error-shape, and comment-discipline rules do not apply to this new Markdown planning document.

  1. TESTING.md.

N/A — no executable behavior changed. The document defines future CI evidence, but this PR does not add a runner, gate, or test subject that needs a same-PR test.

  1. LOCKED DESIGN DECISIONS.

Finding — docs/v4-compilation-milestones.md:165-166 conflicts with the locked fixed-point meaning of self-hosting. The new M3 section says that once stage0 compiles src/v4 into stage1, “Self-hosting is structurally achieved (even if not yet bit-identical).” The thesis explicitly separates “the compiler can compile itself” from the Pure Bootstrap deliverable: compiler self-emission is fixed-point, bit-identical output, and is “strictly stronger than ‘the compiler can compile itself’” (THESIS.md:247-252; also docs/design-pure-bootstrap-zero.md:155-160 names DB-8 bit-identical convergence as the no-compromise gate). chatgpt-review-fe7dc5e2-c8bb-42…

chatgpt-review-2e344f81-be59-4d…

M3 can be called “self-compilation” or “stage1 exists,” but calling self-hosting structurally achieved before M4 dilutes the locked acceptance target and would let downstream planning mark the central Pure Bootstrap goal as achieved too early.

  1. TRACKED vs UNTRACKED DEBT.

Compliant — the doc names existing stubs/gates as blockers rather than introducing new scaffolds: T-7’s feature:T-7-parse-walk-realization marker, T-28’s namespace_from_tree_and_graph gate, T-34 deferred evaluator hooks, and T-4/T-33 prerequisites are all presented as blocking work with explicit milestone placement (docs/v4-compilation-milestones.md:133-154, docs/v4-compilation-milestones.md:168-177, docs/v4-compilation-milestones.md:227-238). I do not see a new TODO, bridge, or temporary implementation shape introduced by this PR.

2.5. Top-down PM intent review

Finding — docs/v4-compilation-milestones.md:165-166 weakens the PM-level Pure Bootstrap target. Highest authority says the v4 fixed-point acceptance is a v4 binary compiling compiler.dag into bit-identical stage0 Rust and bit-identical artifacts (THESIS.md:321-327), and the Pure Bootstrap Zero design makes DB-8 bit-identical convergence a no-compromise acceptance gate (docs/design-pure-bootstrap-zero.md:155-160). chatgpt-review-fe7dc5e2-c8bb-42…

chatgpt-review-2e344f81-be59-4d…

The diff’s M3 wording would cause a faithful worker or manager to treat “stage0 produced stage1” as self-hosting achieved, even though the plan’s must-have target remains M4 fixed point. Rename that proof to self-compilation/stage1 existence and reserve self-hosting achieved for M4/T-15.

Finding — docs/v4-compilation-milestones.md:102-114 misclassifies an M2 semantic blocker as an M1 link blocker. The same document defines M1 only as emitted Rust compiling/linking into a runnable v4-stage0 binary, and explicitly says M1 does not prove the binary can compile a v4 program correctly (docs/v4-compilation-milestones.md:86-100). But the “Known blockers” for M1 lists the T-10 emit stub because it produces no useful output for real input (docs/v4-compilation-milestones.md:102-114). By the doc’s own definition, a semantic emit stub belongs in M2, not M1; keeping it under M1 would misdispatch work toward v4 emit semantics before the M1 rustc/cargo-link evidence is even isolated.

3. Verdict

REQUEST_CHANGES

The milestone framing is useful, but the M3 self-hosting wording contradicts the locked fixed-point acceptance semantics, and the M1 blocker list mixes linkability with runtime compiler usefulness. Both are planning-authority issues that can steer downstream work incorrectly if merged as written.

…eview

Finding 1 — M1 Known blockers listed T-10 emit stub as a link blocker:
By the doc's own definition M1 proves only that emitted Rust links to a
runnable binary, not that the binary does anything useful. T-10's semantic
emptiness is an M2 concern. Removed T-10 from M1 blockers; updated the
dependency note to name semantic correctness explicitly as M2 scope.

Finding 2 — M3 claimed "Self-hosting is structurally achieved":
THESIS.md §247-252 and design-pure-bootstrap-zero.md §155-160 define
self-hosting as bit-identical fixed-point convergence (DB-8), strictly
stronger than "compiler can compile itself." M3 is stage0 self-compilation
/ stage1 exists — a necessary step toward M4, not the Pure Bootstrap
deliverable. Replaced the wording to distinguish self-compilation (M3)
from self-hosting (M4/T-15).

Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
@briansrls

Copy link
Copy Markdown
Contributor Author

Addressed both openai-pro REQUEST_CHANGES findings in f4082f0:

Finding 1 — M1 blocker list mixes linkability with runtime compiler usefulness:
T-10 emit being a stub is a semantic concern (M2), not a link concern (M1). By the doc's own definition, M1 proves only that the emitted Rust compiles and links — it explicitly states M1 does NOT prove the binary can compile a v4 program correctly. Removed T-10 from M1 Known blockers. Updated the dependency note to state explicitly: "Semantic correctness is M2."

Finding 2 — M3 "Self-hosting is structurally achieved" contradicts the locked Pure Bootstrap target:
THESIS.md §247-252 and design-pure-bootstrap-zero.md §155-160 define self-hosting as bit-identical fixed-point convergence (DB-8), which is strictly stronger than "compiler can compile itself." M3 is stage0 self-compilation — stage1 exists. It is a necessary step toward M4, not the Pure Bootstrap deliverable. M3 What-this-proves now reads: "The v4 compiler can compile itself — stage0 self-compilation, stage1 exists. This is NOT self-hosting. Self-hosting (the Pure Bootstrap Zero requirement) is the bit-identical fixed point at M4/T-15."

— sent from loyal-stag-23

@briansrls briansrls left a comment

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Review metadata

  • Provider / model: codex / unknown
  • Commit: f4082f00 · Trigger: schedule
  • Thinking: 390s wall

BLOCKING (1)

Root Cause

  • docs/v4-compilation-milestones.md M2 treats T-10 as serializer-only and misses the 00_compile.dag source-entry boundary → add an M2 blocker/required-work bullet to wire or dissolve compile_ingest_staging so the stage0 CLI composes T-6/T-7/T-8/T-9/T-10 from Source input.

⚠️ One planning-authority gap remains in the M2 unblock list.

**What this does NOT prove:** The stage0 binary can compile a v4 program correctly.
It may exist but produce wrong or empty output for any input.

**Known blockers:**

This comment was marked as resolved.

@briansrls

Copy link
Copy Markdown
Contributor Author

Addressed in 1839602 (operator-committed).

Finding (Gap 2 — T-6/T-7 Rust path framed as P5-scaffold dispatch): Valid. The prior wording created a dispatchable hand-Rust path — "would be a P5 scaffold... requires dissolution receipt before dispatch." THESIS.md:294-296 is unambiguous: "Stage0 Rust compiler internals (tokenize, parse, lower, infer, emit, lenses, std library) are emitted from the .dag graph and committed — not hand authored. Hand-maintained surface target: 0."

Gap 2 now states: writing T-6/T-7 in Rust is a STOP — not a normal P5-scaffold dispatch path. Workers must not be dispatched on a hand-Rust path for T-6/T-7 without explicit PM/Director re-ratification of the Pure Bootstrap Zero mandate. THESIS.md:294-296 is quoted directly on-page. No dissolution receipt makes hand-Rust authoring of these internals a valid normal path.

— sent from loyal-stag-23

@briansrls

Copy link
Copy Markdown
Contributor Author

Review metadata

  • Provider / model: openai-pro / gpt-5-5-pro
  • Commit: 18396020 · Trigger: manual
  • Comparison: main @ 3a9be658 ... docs/v4-compilation-milestones @ 18396020
  • Conversation: View conversation

1. Story of the diff

This PR adds docs/v4-compilation-milestones.md, a new planning authority that separates “v4 compiles” into observable milestones: structural .dag compile, emitted Rust linking into stage0, stage0 compiling a trivial program, stage0 compiling src/v4 into stage1, and finally the stage1/stage2 fixed point. The useful mechanism is that it distinguishes the current CI structural receipt from a runnable binary, then names concrete blockers for M1/M2 such as v2 emitter fidelity, compile_ingest_staging, T-6/T-7 walks, dag.dag language-model wiring, T-8/T-28 resolution, T-9/T-4 grounding, and T-10 emit (docs/v4-compilation-milestones.md:44-153). It also protects the Pure Bootstrap Zero direction by explicitly saying T-6/T-7 walks must be authored in .dag, not hand-Rust, and by keeping the compiler pipeline track separate from the TestClaim/eval track until they converge later (docs/v4-compilation-milestones.md:210-277).

2. Invariant categories

  1. LAYER MODEL — Compliant. This is a planning-doc-only diff; it does not add substrate types, Dag fields, computation variants, or Rust mutation surfaces. The layer-sensitive decision it does make is correct: T-6/T-7 compiler behavior stays in .dag, with hand-Rust authoring called a STOP rather than a scaffold path (docs/v4-compilation-milestones.md:260-269).
  2. INVARIANTS.md + modeling-discipline.md — Compliant. The doc names existing stubs as fail-closed blockers instead of treating structural receipts as execution: M0 explicitly says full structural compile does not prove tokenizer/parser/evaluator/emitter execution (docs/v4-compilation-milestones.md:73-85), and M2 lists ParseExprRejected, compile_pipeline_not_realized_diagnostic, and bare-Atom algebra rejection as blockers rather than fabricating success (docs/v4-compilation-milestones.md:131-148).
  3. CODING.md — N/A. The diff adds a Markdown planning authority, not Rust implementation code, helper functions, comments in code, or API shapes.
  4. TESTING.md — Finding. docs/v4-compilation-milestones.md:162 gives M3 evidence as only v4-stage0-compiler compile src/v4 ... && rustc ... -o v4-stage1, but the M3 definition says “stage1 is functionally complete: it can compile v4 programs, not just trivial ones” at docs/v4-compilation-milestones.md:160. That evidence proves stage0 emitted a linkable stage1 binary; it does not prove the stage1 binary can compile anything. This violates the behavior-driven evidence discipline: the milestone names a behavior, but the acceptance command checks only artifact existence/linking. Fix by either narrowing M3’s definition to “stage1 binary links/exists” or adding a stage1 invocation to the evidence, for example a v4-stage1 compile trivial.dag ... smoke before M3 can be marked reached.
  5. LOCKED DESIGN DECISIONS — Compliant. The PR references Pure Bootstrap Zero and preserves the locked direction: no hand-Rust for v4 compiler internals, T-6/T-7 in .dag, and self-hosting reserved for the bit-identical fixed point rather than conflated with stage0 self-compilation (docs/v4-compilation-milestones.md:164-167, docs/v4-compilation-milestones.md:260-269).
  6. TRACKED vs UNTRACKED DEBT — Compliant. The diff documents existing stubs and bridges with concrete owning lanes or file anchors: resolve-posture bridge is explicitly weaker than M0 full compile (docs/v4-compilation-milestones.md:70-77), T-7 is tied to feature:T-7-parse-walk-realization (docs/v4-compilation-milestones.md:132), and compile_ingest_staging is named as a required M2 orchestration blocker (docs/v4-compilation-milestones.md:134, docs/v4-compilation-milestones.md:141). I do not see a new scaffold introduced by this PR.

2.5. Top-down PM intent review

Finding. Pure Bootstrap Zero’s acceptance shape is a working compile cycle, not merely an emitted artifact: docs/design-pure-bootstrap-zero.md:159-160 requires fixed-point convergence and “regen → rustc → run → diff fixed-point,” and THESIS.md:321-322 frames fixed-point acceptance as the v4 binary compiling compiler.dag into bit-identical outputs. The new M3 milestone says stage1 is “functionally complete” (docs/v4-compilation-milestones.md:160) but its evidence only builds v4-stage1 and never runs that binary (docs/v4-compilation-milestones.md:162). A worker following the doc faithfully could declare M3 complete with a stage1 binary that links but cannot compile even the trivial M2 fixture, which semantically dilutes the milestone.

3. Verdict

REQUEST_CHANGES

The document is directionally strong and mostly aligns with Pure Bootstrap Zero, but the M3 acceptance evidence is under-specified relative to its own definition and the PM-level fixed-point intent. Tightening that milestone now avoids giving workers a false “stage1 exists/functionally complete” receipt.

The M3 definition states stage1 is functionally complete (can compile v4
programs), but the evidence only built and linked the binary. Add a
v4-stage1 smoke invocation so M3 cannot be declared on a non-executing
binary; expand What this proves accordingly.

Addresses openai-pro REQUEST_CHANGES (review 17754, sha:18396020).

Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
@briansrls

Copy link
Copy Markdown
Contributor Author

Review metadata

  • Provider / model: openai-pro / gpt-5-5-pro
  • Commit: 0009bb7a · Trigger: manual
  • Comparison: main @ 3a9be658 ... docs/v4-compilation-milestones @ 0009bb7a
  • Conversation: View conversation

1. Story of the diff

This PR adds a new planning authority, docs/v4-compilation-milestones.md, to define what “v4 compiles” means at progressively stronger evidence levels. The doc separates structural .dag compilation, Rust emission, and a full runnable bootstrap artifact so CI green does not get mistaken for an executable compiler (docs/v4-compilation-milestones.md:38-56). It then maps the bootstrap chain into M0–M4: M0 is current structural compile, M1 is emitted Rust linking, M2 is a stage0 binary compiling a trivial .dag program, M3 is stage0 producing stage1, and M4 is the fixed-point / T-15 hash equality gate (docs/v4-compilation-milestones.md:60-202). The load-bearing planning work is the blocker inventory for M2—compile_ingest_staging, T-6/T-7, dag.dag language-model wiring, T-8/T-9/T-10, and T-4/T-33 dependencies—and the explicit separation between compiler-pipeline progress and the TestClaim/eval track (docs/v4-compilation-milestones.md:130-153, docs/v4-compilation-milestones.md:206-241).

2. Invariant categories

1. LAYER MODEL

N/A — this is a docs-only planning PR. It does not add or mutate Dag substrate types, cross-pass carriers, dag.rs state, or new substrate variants.

2. INVARIANTS.md + modeling-discipline.md

Finding — docs/v4-compilation-milestones.md:294-296, P2 Boundary Discipline / Practice 5 single-authority metadata. The recommendation says the M1 action is “Zero code changes to src/v4 required — just a CI wiring change.” But v4’s build/CI pipeline is explicitly modeled as .dag data in workflow/bootstrap.dag and workflow/ci.dag (THESIS.md:266-270), and Pure Bootstrap Zero names those workflow models as the load-bearing authorities for bootstrap and CI (docs/design-pure-bootstrap-zero.md:7). As written, the planning instruction would let a worker add or modify the CI step directly in the checked workflow surface without updating src/v4/workflow/ci.dag, creating a parallel CI authority. The fix is to say the M1 gate must be added through the modeled CI authority, with any checked workflow/YAML change treated as the projection/receipt, not the source.

3. CODING.md

N/A — no Rust implementation code is added or refactored. The doc’s prose is the artifact under review, and the issue above is about architectural authority rather than Rust style.

4. TESTING.md

Compliant — the milestone evidence is behavior-driven rather than implementation-layout-driven: M0 distinguishes full compile receipt from the resolve-posture bridge (docs/v4-compilation-milestones.md:64-82), M1 requires a linkable/runnable emitted artifact (docs/v4-compilation-milestones.md:88-100), and M2 requires an end-to-end stage0 invocation on a minimal .dag input (docs/v4-compilation-milestones.md:121-128). No new tests were required for this docs-only PR.

5. LOCKED DESIGN DECISIONS

Finding — docs/v4-compilation-milestones.md:294-296, Pure Bootstrap Zero / CI-as-data authority. The locked Pure Bootstrap Zero context says v4’s workflow authorities are src/v4/workflow/bootstrap.dag and src/v4/workflow/ci.dag, and that the committed ci.yml is a checked projection from .dag (docs/design-pure-bootstrap-zero.md:7). The “Zero code changes to src/v4 required — just a CI wiring change” wording dilutes that locked decision for the very first recommended action. This should be rephrased to preserve the modeled CI source of truth: for example, “no compiler-spine changes required; add the M1 gate in src/v4/workflow/ci.dag and update/regenerate the checked CI projection as its receipt.”

6. TRACKED vs UNTRACKED DEBT

Compliant — the doc does not introduce a new scaffold or TODO shape. Existing stubs and blockers are named with concrete owning lanes/tasks and failure modes, especially for T-6/T-7, compile_ingest_staging, T-4/T-33, and T-34 (docs/v4-compilation-milestones.md:130-153, docs/v4-compilation-milestones.md:230-241). The only debt-related blocker is the CI-authority wording above, which would become untracked parallel authority if followed literally.

2.5. Top-down PM intent review

Finding — PM intent mismatch between CI-as-data and the recommended M1 action. The highest-level authority says gunbc applies its own lenses to its own build/CI pipeline, which is modeled as .dag data in workflow/bootstrap.dag and workflow/ci.dag (THESIS.md:266-270), and the Pure Bootstrap Zero design names those as the load-bearing workflow authorities with ci.yml only a checked projection (docs/design-pure-bootstrap-zero.md:7). The new plan’s top recommendation says to add the M1 CI step with “Zero code changes to src/v4 required — just a CI wiring change” (docs/v4-compilation-milestones.md:294-296). A worker following that faithfully could bypass src/v4/workflow/ci.dag, which would dilute the recursive-flex / CI-as-data commitment. This is a planning-artifact issue, not a repo-wide backlog item: the new doc should route the M1 step through the modeled CI authority.

3. Verdict

REQUEST_CHANGES

The milestone framing is otherwise useful and mostly careful, especially around structural vs executable compile evidence. I would not merge it until the M1 recommendation is corrected so CI changes remain authored through src/v4/workflow/ci.dag rather than encouraging a direct workflow-only authority.

The prior wording ("just a CI wiring change") could be read as modifying
the CI YAML directly, bypassing ci.dag which is the modeled authority per
THESIS.md §workflow and design-pure-bootstrap-zero.md. Rephrase to author
the gate in ci.dag and treat the checked CI projection as the receipt.

Addresses openai-pro REQUEST_CHANGES (review 17759, sha:0009bb7a).

Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
@briansrls

Copy link
Copy Markdown
Contributor Author

Review metadata

  • Provider / model: openai-pro / gpt-5-5-pro
  • Commit: a57e04c8 · Trigger: manual
  • Comparison: main @ 3a9be658 ... docs/v4-compilation-milestones @ a57e04c8
  • Conversation: View conversation

1. Story of the diff

This PR adds docs/v4-compilation-milestones.md, a planning authority that separates “v4 structurally compiles” from “v4 emits Rust” from “v4 produces a runnable compiler” (docs/v4-compilation-milestones.md:38-56). It maps the modeled bootstrap chain seed→stage0→stage1→stage2 into M0–M4 milestones, then names the current blockers for moving from structural CI coverage to a real stage0 binary and eventually a fixed-point stage1/stage2 compiler (docs/v4-compilation-milestones.md:60-202). The strongest parts of the doc are the fail-closed M0 distinction between a full compile receipt and the resolve-posture bridge (docs/v4-compilation-milestones.md:64-82) and the explicit Pure Bootstrap guard that T-6/T-7 lexer/parser work must be authored in .dag, not hand-Rust (docs/v4-compilation-milestones.md:256-265).

2. Invariant categories

  1. LAYER MODEL — N/A — the diff is a documentation/planning artifact only; it does not add substrate types, mutate Dag, introduce new variants, or change implementation code.
  2. INVARIANTS.md + modeling-discipline.md — Compliant — fail-closed / facts-flow-forward discipline is handled by distinguishing the M0 full compile receipt from the weaker resolve-posture bridge instead of treating any green CI arm as equivalent (docs/v4-compilation-milestones.md:64-82). The doc also preserves single-authority workflow modeling by sending the M1 CI gate through src/v4/workflow/ci.dag, not an unmodeled CI-only script path (docs/v4-compilation-milestones.md:294-298).
  3. CODING.md — N/A — no Rust implementation code or in-code explanatory comments are added; this is a planning document whose prose is the artifact.
  4. TESTING.md — Finding — docs/v4-compilation-milestones.md:162 defines the M3 evidence as v4-stage1 compile trivial.dag --target rust, but it does not compile the stage1-emitted Rust with rustc or run the emitted trivial artifact. That leaves the exact M1 failure mode open: an executable compiler binary can run while producing wrong or empty output, which the doc itself calls out at docs/v4-compilation-milestones.md:99-100. For behavior-driven milestone evidence, M3 should either repeat the M2-style compile→rustc→run check against stage1 output, or explicitly narrow M3 to “stage1 binary executes a smoke command” and move the “functionally complete” claim elsewhere.
  5. LOCKED DESIGN DECISIONS — Compliant — the doc references the Pure Bootstrap Zero mandate and preserves it: lexer/parser algorithm walks are explicitly .dag work, and hand-Rust T-6/T-7 authoring is marked STOP without PM/Director re-ratification (docs/v4-compilation-milestones.md:256-265). The CI recommendation likewise routes through the modeled CI authority (docs/v4-compilation-milestones.md:294-298).
  6. TRACKED vs UNTRACKED DEBT — Compliant — the doc names existing stubs/bridges as blockers rather than normalizing them: parse_expr, compile_ingest_staging, T-28 namespace walking, and v4_evaluator deferred hooks are each bounded to the milestone they block (docs/v4-compilation-milestones.md:130-149, docs/v4-compilation-milestones.md:230-241, docs/v4-compilation-milestones.md:275-280). I do not see a new TODO/scaffold introduced by this PR.

2.5. Top-down PM intent review

Finding — the M3 definition says the stage0 compiler should produce a stage1 binary and that “stage1 is functionally complete: it can compile v4 programs, not just trivial ones” (docs/v4-compilation-milestones.md:157-160), but the evidence only asks the resulting stage1 binary to run compile trivial.dag --target rust (docs/v4-compilation-milestones.md:162). That dilutes the milestone from “stage1 is a working compiler” into “stage1 can execute a smoke command,” and a worker could faithfully implement the written M3 gate while never proving stage1’s emitted output is valid or that stage1 can compile the v4 pipeline. Either strengthen the evidence or weaken the definition.

3. Verdict

REQUEST_CHANGES

The planning shape mostly preserves the v4/Pure Bootstrap intent, but the M3 acceptance evidence under-proves the milestone it defines. Fixing that before merge matters because this document is intended to steer future CI and worker dispatch.

@briansrls briansrls left a comment

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Review metadata

  • Provider / model: codex / unknown
  • Commit: 0009bb7a · Trigger: schedule
  • Thinking: 411s wall

Non-blocking — Strengths

  • docs/v4-compilation-milestones.md The milestone framing now cleanly separates structural compile, Rust link, first execution, self-compilation, and fixed-point evidence.

✅ No blocking concerns found.

…output

Prior fix proved stage1 can execute a smoke command; this PR proves stage1
produces valid, runnable output by mirroring M2's evidence chain one level up:
stage1 compiles trivial.dag → emits Rust → rustc compiles it → binary runs.
Definition updated to match: stage1 must pass the same compile→emit→rustc→run
chain M2 proves for stage0, not merely execute a smoke invocation.

Addresses openai-pro REQUEST_CHANGES (review 17760, sha:a57e04c8).

Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
@briansrls

Copy link
Copy Markdown
Contributor Author

Review metadata

  • Provider / model: openai-pro / gpt-5-5-pro
  • Commit: a04cbf4a · Trigger: manual
  • Comparison: main @ 3a9be658 ... docs/v4-compilation-milestones @ a04cbf4a
  • Conversation: View conversation

1. Story of the diff

This PR adds docs/v4-compilation-milestones.md as a planning authority for what “v4 compiles” means at each observable stage. It separates structural compile, Rust emit, and a full runnable bootstrap; then maps the modeled bootstrap.dag chain into M0 through M4, from current structural compile through stage0 linking, trivial-program execution, stage1 self-compilation, and final stage1/stage2 fixed-point. The strongest parts are the explicit distinction between compiler-pipeline milestones and the independent TestClaim/eval track, and the M2 blocker decomposition that prevents workers from treating parser/lexer/emit/T-4/T-33 gaps as one undifferentiated “v4 doesn’t run yet” problem. The one load-bearing problem is in the immediate-actions section: it reverses the document’s own sequencing for the M1 CI gate.

2. Invariant categories

  1. LAYER MODEL (substrate vs implementation).

N/A — this diff is a documentation/planning artifact only; it does not introduce substrate types, Dag mutation, std/ primitives, or new coproduct variants.

  1. INVARIANTS.md + modeling-discipline.md.

Finding — Fail-Closed / Boundary Discipline. docs/v4-compilation-milestones.md:250-255 says the next M1 step is a gating cargo check only “once the emitter gaps are fixed,” after noting the probe currently surfaces ~4,900 rustc errors. But docs/v4-compilation-milestones.md:295-299 makes the first recommended action “Add M1 CI step” and says to “author the gate” in src/v4/workflow/ci.dag to surface those breaks. That collapses two different CI contracts: a non-gating diagnostic probe versus a fail-closed milestone gate. Because workflow/ci.dag is the modeled CI authority under the Pure Bootstrap/recursive-flex path, landing a planning doc that tells a worker to add a known-red gate first would either break CI or normalize a continue-on-error probe as a milestone gate. Fix by either resequencing action 1 after the emitter fixes, or explicitly naming it as a bounded non-gating probe with a dissolution trigger into the real M1 gate. The relevant higher-level CI-as-data / fixed-point framing is consistent with the uploaded thesis/design context. chatgpt-review-2c35d065-d28f-4b…

  1. CODING.md.

N/A — no Rust implementation code is changed. There are no new functions, helpers, methods, error/result shapes, or comments in src/v3/compiler/src/ to evaluate against CODING.md.

  1. TESTING.md.

Compliant — no tests are required for a doc-only milestone map, and the proposed evidence is behavior-driven at the right level: M2 requires the real compile→emit→rustc→run chain for a trivial program at docs/v4-compilation-milestones.md:125, and M3 repeats that chain through stage1 at docs/v4-compilation-milestones.md:159-168. The M1 gate/probe ambiguity above is the one testing/CI defect; once clarified, the evidence shapes are appropriate.

  1. LOCKED DESIGN DECISIONS.

Compliant — the doc preserves the locked Pure Bootstrap Zero direction by stating T-6/T-7 must be authored in .dag, not Rust, and that hand-Rust algorithm walks are a STOP without explicit PM/Director re-ratification (docs/v4-compilation-milestones.md:257-266). It also keeps CI wiring under src/v4/workflow/ci.dag (docs/v4-compilation-milestones.md:295-298), which matches the uploaded PBZ/THESIS workflow-authority framing. chatgpt-review-c86e4164-9ae7-4d…

  1. TRACKED vs UNTRACKED DEBT.

Compliant — the existing stubs and blockers are named with bounded milestone context rather than introduced as new scaffolds: T-6 lexer walk (docs/v4-compilation-milestones.md:131), T-7 parse walk/parse-tree construction (:132), compile_ingest_staging (:134), T-4/T-33 (:136-137), and T-34 evaluator hooks (:231-242). The only debt-tracking ambiguity is the M1 CI action already called out: a probe needs an explicit probe disposition and dissolve-into-gate trigger, not the word “gate.”

2.5. Top-down PM intent review

Finding — the immediate-action sequence would cause the wrong work. The highest-level intent is that bootstrap/CI behavior is modeled in .dag, with compiler internals emitted from .dag and fixed-point acceptance eventually producing bit-identical stage output from the .dag source of truth. chatgpt-review-2c35d065-d28f-4b…

Within this PR’s own milestone authority, Gap 1 says the gating M1 cargo check should come “once the emitter gaps are fixed” (docs/v4-compilation-milestones.md:250-255), but Recommended action 1 tells a worker to add the M1 CI step/gate now to surface the same known breaks (docs/v4-compilation-milestones.md:295-299). A worker following that faithfully would either create a known-failing modeled CI gate or encode a non-gating probe while the document calls it a gate. That semantic mismatch should be corrected before merge.

3. Verdict

REQUEST_CHANGES. The milestone decomposition is useful and mostly aligned with Pure Bootstrap Zero, but the M1 CI gate/probe contradiction is load-bearing in a planning authority. Clarify that action before this doc becomes the dispatch surface for the next worker.

@briansrls briansrls left a comment

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Review metadata

  • Provider / model: codex / unknown
  • Commit: a04cbf4a · Trigger: schedule
  • Thinking: 283s wall

BLOCKING (1)

Root Cause

  • docs/v4-compilation-milestones.md T-4 algebra grounding and T-2 algebra constructor export were collapsed into one M2 blocker → split M2 into a T-2 Node-constructor prerequisite plus T-4 Wave 2b replacing bridge Symbols with those constructors.

⚠️ One planning-authority ownership error remains; the rest of the prior findings look resolved.

Comment thread docs/v4-compilation-milestones.md Outdated
- Wire T-10 emit to produce real Rust source text from a translated node tree
- T-8 normalize + resolve (including T-28 std module-graph substrate, bundled into T-8 per TASKS.md line 41): modeled and in the chain; the trivial fixture's `import v4.std.node { Symbol }` requires cross-file resolution — T-28 is exercised for std library name lookup even for the trivial case
- T-9 infer: modeled and in the chain; requires T-4 algebra grounding (formal TASKS.md prerequisite) — T-9 fail-closes on bare-Atom bridge symbols until T-4 fills real Node constructors for each algebra type
- T-4 algebra fact-bundle for Rust target: fill Node constructors for each algebra type (e.g. `ordered_ring_node`) so T-9 can ground algebra references in rust.dag instead of rejecting via `infer_algebra_ref_ungrounded`

This comment was marked as resolved.

briansrls and others added 4 commits May 25, 2026 14:16
The example fn add(a, b) = a + b violated wave-1 grammar (untyped params,
+ operator, expression body) and contradicted the M2 fixture definition at
line 123. Replace with a plain statement: any Rust-target input exercises
the algebra emit path, so the T-4 gate fires before M2 evidence can produce
valid Rust output.

Addresses cursor REQUEST_CHANGES (review 17781, sha:d0ed54ad).

Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
…b consumes them

TASKS.md §T-2 is explicit: 'T-2 must export a Node constructor for each
algebra type... T-4 Wave 2b is explicitly gated on this deliverable.'
The doc incorrectly attributed Node constructor authoring to T-4. Fix all
three occurrences in blocker 6 and the Required work list: T-2 exports
ordered_ring_node etc.; T-4 Wave 2b uses them in rust.dag.

Addresses BLOCKING inline comment (sha:d0ed54ad, line 148).

Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
…rc/v4 → stage1'

M3 section explicitly states it is NOT self-hosting (line 169-171); the
fixpoint is M4/T-15. The summary table's 'self-compilation' label reintroduced
the conflation the section was written to prevent. Use the milestone section
title instead.

Addresses cursor REQUEST_CHANGES (review 17785).

Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>

@briansrls briansrls left a comment

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Review metadata

  • Provider / model: codex / unknown
  • Commit: b214f90a · Trigger: schedule
  • Thinking: 342s wall

Non-blocking — Strengths

  • docs/v4-compilation-milestones.md Classified as design/docs; the milestone framing is consistent with the thesis, TASKS critical path, and live v4 scaffold I checked.

✅ No blocking concerns.

@briansrls briansrls left a comment

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Review metadata

  • Provider / model: codex / unknown
  • Commit: ba042b66 · Trigger: schedule
  • Thinking: 143s wall

Non-blocking — Strengths

  • docs/v4-compilation-milestones.md Classified as design/docs, and the milestone framing is consistent with the thesis, Pure Bootstrap Zero, and the task dependencies I checked.

✅ No blocking concerns found.

@briansrls briansrls left a comment

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Review metadata

  • Provider / model: codex / unknown
  • Commit: 5a560258 · Trigger: schedule
  • Thinking: 253s wall

BLOCKING (1)

Root Cause

  • docs/v4-compilation-milestones.md M1 mixes type-checking evidence with binary-link evidence → keep the cargo-check probe non-gating and require cargo build or rustc plus a produced/runnable v4-stage0 receipt for M1.

⚠️ M1’s acceptance path must prove the binary milestone it defines.

Comment thread docs/v4-compilation-milestones.md Outdated
**Required work to reach M1:**
- Fix v2 emitter to produce type-annotated, correct-arity Rust for all v4 constructs
(target the E0282/E0107 categories first — highest count)
- Add CI step to `cargo check` (or `cargo build`) the emitted crate and gate on success

This comment was marked as resolved.

briansrls and others added 3 commits May 25, 2026 18:31
cargo check only type-checks; it does not link and does not produce the
v4-stage0 binary M1 defines. Gate must be cargo build.

Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
Lines 256 and 299 still named cargo check as the M1 gate after the
prior fix at line 116. All three gate-defining locations now consistently
require cargo build (linking). cargo check mentions that remain describe
current failure state or the probe, not the acceptance criterion.

Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
Records operator-ratified decisions from milestone planning:
- T-2 Node constructor shape: Conj/named-edge (not Instantiation);
  precision and simplicity point the same direction
- T-25-core: strengthen home types before reaching for refinements
- T-30 gate: affected-lens TestClaim via T-21 + T-19
- T-4 conformance tests: explicit per-language deliverable
- Cycle prevention: three independent guarantees (value/loop/module)
- Test gate architecture: lens enforcement via ci.dag + run_required_lens_gates

Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>

@briansrls briansrls left a comment

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Review metadata

  • Provider / model: codex / unknown
  • Commit: ebe35709 · Trigger: schedule
  • Thinking: 389s wall

BLOCKING (1)

Root Cause

  • docs/v4-compilation-milestones.md cycle-prevention rationale upgrades a desired module-graph acyclicity invariant into a current guarantee → either add the concrete T-28 import-edge/acyclic diagnostic work item or remove the live “no import cycle can survive” claim.

⚠️ One new documentation-faithfulness issue remains in the ratified cycle-prevention section.

Comment thread docs/v4-compilation-milestones.md Outdated
a `TerminationProof { non_increasing, strict: RankingDimension }` (declared in
`std/cardinality.dag`). `well_formed` enforces this structurally. Unbounded
loops are not well-formed.
3. **Module graph:** circular imports are a resolve-time `Diagnostic`. The module

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

BLOCKING: Under INVARIANTS P1 documentation-faithfulness, this records circular imports as already rejected by 03_resolve.dag, but the live T-28 ModuleGraph only models entries/path uniqueness and resolve_with_graph still has a gated namespace merge, so the milestone doc turns an unimplemented import-cycle invariant into live evidence.

briansrls and others added 2 commits May 25, 2026 19:36
…live

namespace_from_tree_and_graph is gated (03_resolve.dag:564) and ignores
the ModuleGraph argument. std/module_graph.dag models path uniqueness only,
not acyclicity. Fold termination is guaranteed by the value layer alone;
the module-level claim was false. Mark as T-28 deliverable, not live.

Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
The detailed ratified-decisions section was a parallel dispatch authority —
violating the single-authority rule. Replaced with a slim transfer receipt
that names what needs to land in TASKS.md task bodies and is explicitly
not a dispatch surface. TASKS.md remains the source of truth.

Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
@briansrls
briansrls merged commit c6c8cb7 into main May 25, 2026
7 checks passed
@briansrls briansrls mentioned this pull request May 25, 2026
6 tasks
briansrls added a commit that referenced this pull request May 27, 2026
…ingest) (#3692)

* WIP: PM May 24

* Option B: fail-closed on bare-Atom algebra refs + T-4 Wave 2b resequencing

- 04_infer.dag: add algebra_ref_is_grounded guard in
  canonical_grounding_from_inferred_facts; fires infer_algebra_ref_ungrounded
  when AlgebraRef.algebra is a bare Atom (bridge symbol or scaffolded identity
  solver). New helpers: algebra_connective_is_atom, algebra_ref_is_grounded,
  infer_algebra_ref_ungrounded{,_diagnostic}. Imports Atom/Connective/TypeNode.

- TASKS.md T-2: add explicit Node-constructor deliverable (ordered_ring_node()
  → Node etc.) as a gate for T-4 Wave 2b.

- TASKS.md T-4 Wave 2b: tighten [needs] to include T-2 Node constructors;
  explain that bridge-symbol algebra fields fail-closed at T-9.

- model_core.dag: fix wave1_void dissolution condition — two-part: non-empty
  ModelCore AND no bare-Atom AlgebraInhabitanceDecl.algebra fields.

- rust.dag: mark bridge symbols (rust_model_core_bridge_*) as 🟡 scaffolds
  with explicit dissolve-on: T-2 Node constructors + T-4 Wave 2b.

- test/claim/manual/infer_algebra_ref_grounding_anchor.dag: Option B behavior
  receipts — algebra_ref_is_grounded unit checks + canonical_grounding_from_
  inferred_facts rejection anchor for bare-Atom algebra.

Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>

* WIP: PM May 24

* Fix predicate-dissolution finding: remove algebra_connective_is_atom

algebra_connective_is_atom was a hand-rolled Bool predicate over the
Connective coproduct (match → true/false per variant) with no dissolution
disposition — exactly Practice 10's blocking predicate-dissolution shape.

Fix: inline the nested pattern into algebra_ref_is_grounded using a
single TypeNode { connective: Atom { identity: _ } } arm, eliminating
the Bool predicate over Connective entirely. Drop Connective from the
import (no longer needed as an explicit type). Add a 🟡 predicate-
dissolution interim tag to algebra_ref_is_grounded itself, which also
matches the *_is_* Bool-over-Node mechanical trigger.

Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>

* Fix ComputationNode algebra evidence passing grounding guard

algebra_ref_is_grounded's wildcard arm `_ => true` silently passed
ComputationNode algebra evidence as grounded. Computation nodes are
never valid algebra types — only TypeNode shapes are (Conj, Arrow,
Instantiation, etc.).

Fix: replace the catch-all with a two-arm exhaustive match over the
node kind coproduct. TypeNode dispatches to an inner match on the
connective (Atom { identity: _ } => false, _ => true). ComputationNode
explicitly returns false. Adds ComputationNode to the v4.std.node import.

Test claim: add algebra_ref_computation_node_is_ungrounded receipt
(ComputationNode → !grounded) alongside the existing Atom/Conj cases.

Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>

* fix: collapse multiline data decls in infer_algebra_ref_grounding_anchor.dag

v4 parser requires data declaration expressions on the same line as =;
multiline form triggered parse error at CI.

Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>

* docs: v4 compilation milestones — when can we compile?

Maps bootstrap.dag's four-stage chain (seed→stage0→stage1→stage2)
to observable milestones with explicit evidence criteria and known
blockers. Surfaces the current gap: CI runs --target dag (structural
check) but the --target rust → rustc → binary step (M1) has never
been wired. Identifies four design gaps requiring operator decisions
before dispatch.

Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>

* fix(milestones): constrain T-6/T-7 path to .dag per Pure Bootstrap Zero mandate

Gap 2 previously framed 'write in Rust vs .dag' as an open operator
choice. Per THESIS.md and design-pure-bootstrap-zero.md, v4 compiler
logic must be authored in .dag; a Rust path would be a named P5 scaffold
requiring an explicit dissolution receipt. Reframe: M2 depends on the
eval track (T-34→T-22), dispatch both tracks in parallel.

Addresses codex REQUEST_CHANGES on PR #3653.

Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>

* WIP: PM May 24

* fix(milestones): address three blocking inline review findings

Line 119: T-7 blocker description was stale — parse() now dispatches
through parse_production; remaining stub is parse_expr (🟡 gated).

Line 128: M2 dependency chain omitted T-8 and T-9. Added them with
accurate status (modeled, in chain, not additional blockers for trivial
single-file input).

Line 218: Gap 2 incorrectly claimed M2 depends on T-22/T-34. Corrected:
T-6/T-7 walks are authored in .dag, v2 emits Rust from them (--target
rust), stage0 runs them natively. T-22/T-34 is the eval/TestClaim track
only, genuinely independent of the compiler pipeline at M2.

Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>

* fix(milestones): address cursor/composer-2.5 review findings

Finding 1 (M0 evidence overstates CI green): The CI gate has two arms —
full compile receipt and resolve-posture bridge receipt. M0 status is
only confirmed by the full-compile arm. Clarify what each receipt proves
and instruct readers to check the gate log.

Finding 2 (T-28 description wrong): resolve_with_graph passes the
ModuleGraph to namespace_from_tree_and_graph; the 🟡 gate is on
namespace_from_tree_and_graph (does not walk ModuleGraph.entries), not
on resolve_with_graph dropping the parameter. Both occurrences fixed
(M3 blockers and Gap 3).

Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>

* fix(milestones): add dag.dag LM wiring as explicit M2 blocker

dag_wave1_grammar() (ModeledGrammar with production bodies) exists but
neither pipeline-facing LM function uses it — both call
dag_wave1_g0_void_grammar() (VoidGrammar). parse() dispatches VoidGrammar
to the accept-empty arm, so any real program input is rejected at parse.

This is not T-7 scope (generic walk algorithm); it is dag.dag data wiring,
a separate follow-on task. Named and scoped correctly per nimble-koi-111
independent verification.

Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>

* WIP: PM May 24

* fix(milestones): address operator review — four valid findings

Finding 1 (M1 --target rust already in CI): The T-22 host eval receipt
already runs --target rust src/v4 with zero v2 diagnostics. Corrected
doc to say what's missing is cargo check/build of the emitted crate,
not the emission step itself. Updated M1 definition, blockers, Gap 1,
and the current-CI-state table accordingly.

Finding 2 (parallel track table implies M2 requires T-22): Added explicit
note that the eval-track column is NOT a prerequisite for the compiler-
track row. Reformatted table header to avoid co-dependency misread.

Finding 3 (heading "CI green"): Removed snapshot CI claim from section
heading; CI status belongs in the body, not the title.

Finding 4 (eval "nothing can execute" too strong): Named which hooks
are deferred (call_primitive, choose_branch, step_loop, call,
represent_literal, all arms of transfer) vs. which accept (bind_value,
allocate, return_value, terminal_value Continue/Return arms). Replaced
"nothing can execute" with "no nontrivial expression can evaluate
end-to-end while transfer rejects all control-transfer arms."

Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>

* docs: add T-4/T-33 side branch to M2 blockers, fix T-15 prerequisites in M4

Addresses codex BLOCKING review on 7b77fe9:

Finding 1 — M2 missing T-4/T-33 side branch and algebra-grounding gates:
TASKS.md line 42 states T-9 [needs T-8, T-2, T-3, and T-4]; line 43 states
T-10 [needs T-9, T-4]. T-9 infer rejects bare-Atom algebra refs via
infer_algebra_ref_ungrounded until T-4 Wave 2b fills real Node constructors
(ordered_ring_node, etc.) for AlgebraInhabitanceDecl.algebra. Added as
blockers 5 and 6 with precise TASKS.md citations. Updated Required Work and
Sequential dependency sections accordingly.

Finding 2 — M4 treats T-16/T-36 as optional when TASKS.md makes them prerequisites:
TASKS.md lines 31-33: "Both must be complete before T-15." Fixed M4 Note to
state T-16 and T-36 are prerequisites, cite the critical path
T-10 → T-11 → T-16 and T-36 → T-15, and explain why asserting fixpoint
before those gates is a claim about an incomplete binary.

Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>

* docs: fix M1 blocker scope and M3 self-hosting claim per openai-pro review

Finding 1 — M1 Known blockers listed T-10 emit stub as a link blocker:
By the doc's own definition M1 proves only that emitted Rust links to a
runnable binary, not that the binary does anything useful. T-10's semantic
emptiness is an M2 concern. Removed T-10 from M1 blockers; updated the
dependency note to name semantic correctness explicitly as M2 scope.

Finding 2 — M3 claimed "Self-hosting is structurally achieved":
THESIS.md §247-252 and design-pure-bootstrap-zero.md §155-160 define
self-hosting as bit-identical fixed-point convergence (DB-8), strictly
stronger than "compiler can compile itself." M3 is stage0 self-compilation
/ stage1 exists — a necessary step toward M4, not the Pure Bootstrap
deliverable. Replaced the wording to distinguish self-compilation (M3)
from self-hosting (M4/T-15).

Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>

* WIP: PM May 24

* docs: add compile_ingest_staging orchestration stub as explicit M2 blocker

Finding: M2 Evidence feeds a .dag source file to the stage0 binary, but
compile_ingest_staging(source: Source, target) at 00_compile.dag:271 is
always-Rejected — it returns Rejected { compile_pipeline_not_realized_diagnostic }
without calling tokenize, parse, or resolve. The public-facing compile() takes
a CoreNode, not a Source. Even fully-implemented T-6/T-7/T-8 are unreachable
from source text until the Source→CoreNode orchestration is wired.

Added as M2 Known blocker 4 (renumbered T-10, T-4, T-33, trivial-input-scope
to 5–8). Added wiring step to Required work. Updated Sequential dependency
to name compile_ingest_staging as the first prerequisite in the chain.

Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>

* docs: fix M2 trivial fixture — fn add(a,b)=a+b is not valid wave-1 dag.dag

The example was invalid on three counts verified against dag.dag:
1. Token rules (dag.dag:236+) have no + operator
2. dag_grammar_param_list_expr uses dag_grammar_typed_param_expr —
   params must be typed (a: T), not bare identifiers
3. dag_grammar_fn_decl_expr body is dag_production_block ({}) —
   the = expr form is not in the grammar

Replace with data trivial: Bool = true, the simplest syntactically valid
wave-1 .dag declaration (data-decl with typed annotation). Add a note
that the concrete fixture must be grounded in the live grammar.

Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>

* docs: fix M2 fixture grammar (module header + ident value) and T-7 parse-tree scope

Two codex BLOCKING findings on sha:99a86596:
1. `data trivial: Bool = true` is still not grammar-admissible:
   - dag_grammar_module_expr requires ModuleHeader before top-level items
   - dag_grammar_data_value_expr accepts only ident|block; `true` is
     dag_token_kw_true (keyword), not an ident token
   Fix: `module v4.trivial` / `data trivial: Symbol = trivial` — the
   self-naming Symbol pattern used throughout dag.dag itself.
2. T-7 blocker description understated scope:
   - ParseExprResult.ParseExprAccepted carries only remaining:List<Token>,
     no parsed Node; parse_production returns production.emitted (grammar
     label), not a tree from matched tokens
   Fix: T-7 must also implement parse-tree construction so the walk
   produces ParseTree = Node with actual name/type/value facts.

Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>

* docs: fix M2 fixture — add std import; correct T-28/T-8 no-prelude claim

Two findings from BLOCKING relay on sha:a50a5b181:
1. Symbol requires explicit import — dag.dag has no implicit prelude.
   dag.dag itself imports Symbol from v4.std.node (line 51); no type is
   available without import. Fixture updated:
   module v4.trivial / import v4.std.node { Symbol } / data trivial: Symbol = trivial
   Note updated to state no-prelude invariant with source citation.
2. "single-file trivial input does not hit T-28" was wrong — the fixture's
   import v4.std.node { Symbol } requires cross-file resolution, which T-28
   (bundled into T-8 per TASKS.md line 41) covers. Updated line 146 and 152
   to reflect that T-28 IS exercised for std library lookup, but is already
   in T-8's scope — not a separate blocker.

Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>

* docs: fix Gap 3 T-28 contradiction — M2 also requires T-28 for std import

Line 274 said "M2 with a single-file trivial input does not [require T-28]"
but this directly contradicted lines 146/152 (fixed in 5f74796) which
correctly state T-28 IS exercised for the trivial fixture's
import v4.std.node { Symbol }. The contradiction allowed the planning doc
to green-light an M2 compile path that cannot resolve its own fixture.

Fixed: Gap 3 now distinguishes M3 (arbitrary user-module graph walking)
from M2 (std library name lookup via namespace_from_tree_and_graph),
noting both require T-28, consistent with the Required work list.

Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>

* WIP: PM May 24

* Fix M3 acceptance evidence to prove stage1 executes, not just links

The M3 definition states stage1 is functionally complete (can compile v4
programs), but the evidence only built and linked the binary. Add a
v4-stage1 smoke invocation so M3 cannot be declared on a non-executing
binary; expand What this proves accordingly.

Addresses openai-pro REQUEST_CHANGES (review 17754, sha:18396020).

Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>

* Route M1 CI step through src/v4/workflow/ci.dag (modeled CI authority)

The prior wording ("just a CI wiring change") could be read as modifying
the CI YAML directly, bypassing ci.dag which is the modeled authority per
THESIS.md §workflow and design-pure-bootstrap-zero.md. Rephrase to author
the gate in ci.dag and treat the checked CI projection as the receipt.

Addresses openai-pro REQUEST_CHANGES (review 17759, sha:0009bb7a).

Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>

* Strengthen M3 evidence: full compile→emit→rustc→run chain for stage1 output

Prior fix proved stage1 can execute a smoke command; this PR proves stage1
produces valid, runnable output by mirroring M2's evidence chain one level up:
stage1 compiles trivial.dag → emits Rust → rustc compiles it → binary runs.
Definition updated to match: stage1 must pass the same compile→emit→rustc→run
chain M2 proves for stage0, not merely execute a smoke invocation.

Addresses openai-pro REQUEST_CHANGES (review 17760, sha:a57e04c8).

Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>

* WIP: PM May 24

* Remove invalid fn add example from M2 blocker 6 (T-4 algebra grounding)

The example fn add(a, b) = a + b violated wave-1 grammar (untyped params,
+ operator, expression body) and contradicted the M2 fixture definition at
line 123. Replace with a plain statement: any Rust-target input exercises
the algebra emit path, so the T-4 gate fires before M2 evidence can produce
valid Rust output.

Addresses cursor REQUEST_CHANGES (review 17781, sha:d0ed54ad).

Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>

* Fix T-2 vs T-4 attribution: T-2 exports Node constructors, T-4 Wave 2b consumes them

TASKS.md §T-2 is explicit: 'T-2 must export a Node constructor for each
algebra type... T-4 Wave 2b is explicitly gated on this deliverable.'
The doc incorrectly attributed Node constructor authoring to T-4. Fix all
three occurrences in blocker 6 and the Required work list: T-2 exports
ordered_ring_node etc.; T-4 Wave 2b uses them in rust.dag.

Addresses BLOCKING inline comment (sha:d0ed54ad, line 148).

Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>

* Fix M3 summary label: rename 'self-compilation' to 'stage0 compiles src/v4 → stage1'

M3 section explicitly states it is NOT self-hosting (line 169-171); the
fixpoint is M4/T-15. The summary table's 'self-compilation' label reintroduced
the conflation the section was written to prevent. Use the milestone section
title instead.

Addresses cursor REQUEST_CHANGES (review 17785).

Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>

* WIP: PM May 24

* Fix M1 gate: require cargo build (not cargo check) — linking is required

cargo check only type-checks; it does not link and does not produce the
v4-stage0 binary M1 defines. Gate must be cargo build.

Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>

* Fix remaining cargo check gate references in Gap 1 and action #1

Lines 256 and 299 still named cargo check as the M1 gate after the
prior fix at line 116. All three gate-defining locations now consistently
require cargo build (linking). cargo check mentions that remain describe
current failure state or the probe, not the acceptance criterion.

Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>

* Add ratified design decisions section (2026-05-25)

Records operator-ratified decisions from milestone planning:
- T-2 Node constructor shape: Conj/named-edge (not Instantiation);
  precision and simplicity point the same direction
- T-25-core: strengthen home types before reaching for refinements
- T-30 gate: affected-lens TestClaim via T-21 + T-19
- T-4 conformance tests: explicit per-language deliverable
- Cycle prevention: three independent guarantees (value/loop/module)
- Test gate architecture: lens enforcement via ci.dag + run_required_lens_gates

Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>

* Correct cycle-prevention point 3: T-28 import-cycle detection is not live

namespace_from_tree_and_graph is gated (03_resolve.dag:564) and ignores
the ModuleGraph argument. std/module_graph.dag models path uniqueness only,
not acyclicity. Fold termination is guaranteed by the value layer alone;
the module-level claim was false. Mark as T-28 deliverable, not live.

Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>

* Replace ratified-decisions section with TASKS.md transfer receipt

The detailed ratified-decisions section was a parallel dispatch authority —
violating the single-authority rule. Replaced with a slim transfer receipt
that names what needs to land in TASKS.md task bodies and is explicitly
not a dispatch surface. TASKS.md remains the source of truth.

Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>

* T-35: virtual module-loader + agent round-trip interface — TASKS.md planning entry

Ratified 2026-05-26: round-trip scope (not one-way). Three interlocking
pieces: virtual module-loader (no filesystem I/O, agent-supplied AST
store replaces T-28-B admission stage), AgentStore carrier in std/agent.dag,
and rich structured compiler output (EmittedSource + InferenceResult +
DiagnosticSet) exposing T-9 inference and diagnostics as typed .dag values.

Depends on T-28-B, T-9, T-10. Post-M3. Enables agent-driven .dag
authoring, IDE integration, and automated refactoring loops.

Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>

* T-35: narrow scope to ingest-side only, respect T-23/AGENT-1 authority

Codex finding valid: original T-35 was claiming emit_structured / structured
output ownership that already belongs to T-23/AGENT-1 (non-text AGENT-SURFACE
contract, DECISIONS.md AGENT-1). Fix: T-35 now owns only the filesystem-free
ingest side (virtual module-loader + AgentStore carrier + compile_with_store
entry point). T-23/AGENT-1 retains sole authority over the agent-facing
output surface (InferenceResult, DiagnosticSet, apply_diff, lens reads).
T-35 is now correctly framed as a prerequisite of T-23, not a parallel surface.
Dependencies reduced to [needs T-28-B] only.

Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>

* T-35: replace retired DECISIONS.md reference with live authority citations

DECISIONS.md does not exist (confirmed deleted). Replace with live
authority: T-23 task entry above + lens/application.dag header mark.

Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>

* T-35: remove content-addressed claim, state path-keyed invariants

Store identity is Map<ModulePath,Node> (path-keyed), not content-addressed.
Adds explicit bijection, fail-closed on missing path, and insert-policy
ratification note to resolve codex RC on #3692.

Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>

* T-35: clarify ModulePath is lookup key, not B1 identity authority

Adds explicit invariant: Node identity remains B1 content_hash per
INVARIANTS §P2; ModulePath is an external boundary handle (like a
filesystem path), not a parallel identity authority. Resolves the
inline P2/single-authority review finding on #3692.

Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>

* T-35: fix bijection claim — store is a function, not bijection

Removing "no two paths map to nodes with the same B1 content hash"
because it would force the path store to police B1 identity — a
boundary-authority conflict. Two distinct module paths mapping to
identical AST content is valid. Content deduplication belongs to
the Node layer; the store enforces uniqueness per ModulePath only.

Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>

* T-35: remove phantom type names from authority boundary

InferenceResult and DiagnosticSet do not exist in src/v4 — naming them
as already-owned T-23 carriers was a P2 violation (inventing type
vocabulary before T-23 coins it). Authority boundary now describes the
category (structured output, lens reads, apply_diff) without pre-naming
T-23's types.

Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>

* T-35: distinguish implementation vs execution prerequisites for compile_with_store

T-9/T-10 are execution prerequisites (pipeline must be complete for
non-stub output), not implementation prerequisites — T-35 scope is
strictly the module-admission substitution in 00_compile.dag; workers
must not expand into infer/emit territory.

Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>

* T-35: remove coined ModuleNotFound/DuplicatePath carrier names from planning entry

openai-pro finding: Rejected<ModuleNotFound> named inside T-35 scope while
T-35 explicitly cannot coin new diagnostic carrier types (T-28-B authority).
Replace with description deferring carrier authority to T-28-B.

Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>

* T-35: clarify AgentStore feeds module_graph_from_entries, not bypasses it

codex finding: 'replace module-admission step' wording could send a worker
down a parallel Map<ModulePath,Node> path bypassing std/module_graph.dag
authority. Fix: AgentStore is an entry source; module_graph_from_entries
remains the canonical ModuleGraph construction path and admission authority.

Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>

* T-35: add store_entries enumeration surface to AgentStore

AgentStore was modeled as lookup-only (store_insert/store_lookup/store_delete).
module_graph_from_entries requires an enumerable collection, not a keyed map.
Add store_entries as the explicit bridge: returns ordered (ModulePath, Node)
pairs passable to module_graph_from_entries; pure/read-only; sole enumeration
surface for workers (no direct Map access).

Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>

* T-35: change AgentStore representation from Map to FreeMonoid<ModuleEntry>

Map<K,V> in std/collection.dag is a closure { lookup: fn(K) -> Witness<V> } —
unenumerable by construction. module_graph_from_entries takes
FreeMonoid<ModuleEntry> directly. Changing AgentStore.entries to
FreeMonoid<ModuleEntry> eliminates the unenumerable-map / enumerable-admission
mismatch: store.entries is now passable straight to module_graph_from_entries.
store_lookup becomes a fold; store_insert appends a ModuleEntry; store_delete
filters. Drops store_entries (no longer needed — entries IS the monoid).

Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>

* T-35: remove stale Map<ModulePath,Node> mention in virtual-loader description

Piece 1 still named Map<ModulePath,Node> after the carrier was changed to
FreeMonoid<ModuleEntry>. Update to reference AgentStore by name so the two
pieces are consistent and there's no residual claim that the store is Map-typed.

Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>

* T-35: declare root: ModulePath parameter on compile_with_store

Finding valid: compile_with_store never specified how the root CoreNode is
selected from a multi-entry AgentStore. Add root: ModulePath as the sole
root-selection authority — compile_with_store looks it up fail-closed via
store_lookup and explicitly prohibits secondary selection mechanisms
(first-entry convention, implicit main path, etc.). store_entries feeds the
full store into module_graph_from_entries for dependency resolution.

Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>

* WIP: PM May 24

* fix(T-35): make Scope paragraph locally complete re: root selection

Inline RC at TASKS.md:1558: the Scope block only described the
entries: Empty → AgentStore replacement for module_graph_from_entries,
leaving root selection implicit (defined in the Signature block above
but not referenced locally in Scope). A worker reading only the Scope
block would face an undeclared root→CoreNode authority.

Fix: rewrite Scope as two explicit steps:
(1) store_lookup(root) → CoreNode (root retrieval, fail-closed)
(2) store.entries → module_graph_from_entries (dependency set)

Root selection authority remains the root: ModulePath parameter declared
in the Signature block; this commit only makes it locally visible in Scope.

Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>

* fix(T-35): document pre-admission root-lookup sequencing safety

Inline RC at TASKS.md:1550: spec said store_lookup(root) runs on the
raw store before module_graph_from_entries, but didn't justify why this
is safe under INVARIANTS P2 boundary discipline.

Safety argument (now explicit): the returned CoreNode is consumed only
inside resolve_with_graph, which executes after admission. If
module_graph_from_entries returns Violates (duplicate paths), the
pipeline returns Rejected and the root CoreNode is discarded — the
unadmitted store never produces output. Workers are now explicitly
forbidden from adding any consume path that precedes the admission gate.

No behavioral change — this is a spec-clarity fix for workers.

Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>

* fix(T-35): admission-first root selection via module_graph_entry_for_path

Codex RC (sha 08c32a3): AgentStore serving as both unadmitted write log
and unique path map; root selection must use the admitted ModuleGraph,
not raw store_lookup.

Fix: compile_with_store now runs module_graph_from_entries first (the
canonical admission authority), then retrieves the root CoreNode via
module_graph_entry_for_path(graph, root) — already defined in
std/module_graph.dag. entry.root is the CoreNode that enters the compile
pipeline. Raw store_lookup is explicitly forbidden as a root-selection
path.

This collapses the two-step (store_lookup + module_graph_from_entries)
ingest into one: the single module_graph_from_entries call both admits
the store and provides the root entry via the admitted graph, satisfying
INVARIANTS P2 boundary discipline (AgentStore is the write log,
ModuleGraph is the unique-path map).

Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>

* fix(T-35): mark store_lookup as internal — not exported from agent.dag

Addresses BLOCKING review: the carrier description listed store_lookup
alongside store_insert/store_delete, implying it is a public agent API.
store_lookup is an internal fold helper; the exported write surface is
store_insert + store_delete only. Root selection goes through
module_graph_from_entries → module_graph_entry_for_path, not store_lookup.

Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>

* fix(T-35): remove prose-only T-23 prerequisite claim

The sentence 'T-35 is a prerequisite of the T-23 round-trip workflow'
made a dependency claim in T-35 prose without a matching [needs T-35]
in T-23's authoritative task record — violating INVARIANTS P2 /
single-authority discipline. Narrowed to factual description only.
Also removed T-23/AGENT-1 from the Unblocks line for the same reason;
the informational content (T-35 and T-23 are complementary, non-overlapping)
is already stated in the preceding paragraph.

Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>

* fix(T-35): route compile_with_store through validate_then_compile — Outcome<Validated<CompileOutput>>

Addresses openai-pro RC: compile_with_store returning Outcome<TargetSource> created a second
compile-output authority parallel to validate_then_compile, bypassing required lens gates.

Fix: compile_with_store routes through validate_then_compile (the sole public compile terminal
in 00_compile.dag) with an empty caller-lenses list — always_required_lenses() (fact-density)
run on agent-supplied code. Output type is Outcome<Validated<CompileOutput>>, same carrier as
validate_then_compile. Single-terminal authority preserved.

Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>

* fix(T-35): correct factual error + clarify ModulePath identity

compile_ingest_staging on main is a stub returning Rejected — there is
no module_graph_from_entries call for workers to find there.
compile_with_store introduces that call as a new addition.

Also clarify that ModulePath is the declared module namespace identity
(from the `module` declaration), not a filesystem path.

Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>

* fix(T-35): restore accurate scope paragraph — compile_ingest_staging has module_graph_from_entries

The prior "fix" (0bf69b1) incorrectly stated compile_ingest_staging is a
stub with no module_graph_from_entries call. The code at 00_compile.dag:350
has module_graph_from_entries(entries: Empty) in the live pipeline. The
original phrasing ("store.entries replaces the entries: Empty argument,
currently in compile_ingest_staging") was accurate. Restoring it.

ModulePath namespace-identity clarification from 0bf69b1 is kept — it was
a valid improvement unrelated to this error.

Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>

* feat(T-QN-1, T-35): QualifiedName infrastructure + T-35 spec update

Add T-QN-1 as a new prerequisite task: introduces QualifiedName =
FreeMonoid<Symbol> + qualified_name_from_node projection, replacing
ModulePath/ModulePathSegment. Operator-ratified 2026-05-27.

Update T-35 to use FreeMonoid<Node> (AgentStore) + QualifiedName for the
root parameter; bridge through module_graph_from_entries via
qualified_name_from_node with a dissolve-on-Change-2 gate comment.
T-35 [needs T-28-B, T-QN-1]; dispatch also gated on operator code examples.

Add naming invariant to INVARIANTS.md §P1: model names must reflect what
they are — nicknaming is a modeling violation. Enforcement via lens (T-QN-1).

Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>

* fix(T-35): make target→mode mapping explicit in compile_with_store brief

compile_with_store takes target: TargetModel; validate_then_compile takes
mode: CompileMode. The mapping is TranslateTo { target: target }. Stated
explicitly so workers don't have to infer it. Addresses claude review 18362
non-blocking planning gap.

Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>

* fix(T-QN-1): explicit module-header grammar authority in dependencies

T-QN-1 said 'Dependencies: none' but qualified_name_from_node reads the
dag_surface_module_header / dag_production_qualified_name parse-tree surface
from extdeps/languages/dag.dag. That surface already exists; no new
prerequisite task is needed. But workers must be told to read dag.dag for the
Node child layout before implementing qualified_name_from_node. Addresses
codex review finding (sha:3f189af0).

Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>

* T-35 spec: declare AgentStore stage-state contract (post-normalize Node)

Addresses codex BLOCKING on a7047ed: store entries were described as
"pre-parsed .dag AST nodes" with no explicit stage boundary, making it
ambiguous whether compile_with_store needed to re-normalize or not.

Now explicit: store carries post-normalize Nodes (same stage as the
existing module_graph_from_entries call in compile_ingest_staging).
compile_with_store does NOT re-normalize — that is the agent's
responsibility before store_insert. After admission the root Node is
resolved via resolve_with_graph; the resulting CoreNode enters
validate_then_compile. Stage contract: store-in = post-normalize Node;
compile-in = post-resolve CoreNode.

Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>

* T-35 spec: make resolve_with_graph explicit in compile_with_store files brief

Addresses inline BLOCKING on a7047ed (TASKS.md:1638): the files section
said entry.root IS the CoreNode entering validate_then_compile, but
ModuleEntry.root is post-normalize (not post-resolve). resolve_with_graph
was stated in the scope paragraph but missing from the step-by-step
implementation brief, leaving workers able to route entry.root directly
into validate_then_compile and silently skip name resolution.

Now explicit in the files section: entry.root is the post-normalize Node;
resolve_with_graph(tree: entry.root, lm: dag_language_model_wave1(),
graph: graph) produces the CoreNode (post-resolve) that enters
validate_then_compile. Workers must not skip resolve_with_graph. The
complete pipeline is normalize → graph-admission → resolve → compile,
matching compile_ingest_staging exactly.

Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>

* T-35 spec: rename AgentStore → ModuleBatch, agent.dag → module_batch.dag (P1)

AgentStore was a P1 naming violation: the name encodes the caller ("agent")
rather than the structural identity of the type. What it actually is: a
pre-validated batch of post-normalize module Nodes — distinct from ModuleGraph
(post-admission, path-unique) in the same way a list is distinct from a set.

Rename:
- AgentStore        → ModuleBatch
- std/agent.dag     → std/module_batch.dag
- store_insert      → batch_insert
- store_delete      → batch_delete
- store_lookup      → batch_lookup (internal)
- compile_with_store → compile_with_batch
- store: AgentStore param → batch: ModuleBatch
- stage contract "store-in" → "batch-in"

Prose updated throughout: "agent-supplied" → "caller-supplied", "Agents
write to the store" → "Callers build the batch", etc. References to
T-23's agent output surface are unchanged (correct use of "agent" there
— T-23 owns AGENT-SURFACE, T-35 owns the ingest batch carrier).

TASKS.md-only change; no .dag code exists yet.

Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>

---------

Co-authored-by: Claude Sonnet 4.6 <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