Repository navigation
Half A: merge #485 + #486 + #487 (tests + L2 lens migrations) - #489
Conversation
Wire the four canonical fixtures (id / drop / wrap / is_empty) from
docs/dependency-and-rendering-design.md §3.3 as executable tests.
Each fixture isolates a reachability pattern from the §3.3 table;
together they pin the model's one-fact-shape abstraction claim so a
per-fixture regression fires in one CI run.
Today the assertions use the UnusedParametersLens ("param used vs
unused"), which separates `drop` from the other three — the
strongest reachability fact available pre-Track-1-Phase-2. When
Phase 2 ships ParameterDisposition, the assertions tighten to
`Consumed | Borrowed` per the §3.3 table without the test interface
changing.
Clone-count ratchets pinned at zero per fixture.
`#[ignore]`'d go.dag cross-target variants stubbed for Lane 3.
Notes on fixture adaptations (documented in-file):
- `is_empty` swaps List<Int>+Empty/Cons → BoxedFx+BoxedV/Nil
because match-on-List core-type lowering isn't wired yet and
`is_empty`/`Empty` collide with src/v3/std/list.dag. The §3.3
abstraction (match-read-only, param inspected not forwarded) is
preserved; canonical form restorable later without test churn.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Address codex-review blocking comment: the previous clone-count
ratchet used Copy-typed data, which collapses Consumed and
Borrowed renderings observationally — so a green signal could
arrive before §3.3 is actually implemented.
Per §9 ("tests verify the facts, not symptoms"), the assertions
now check the parameter contract directly via emitted Rust
signature shape:
Borrowed → `fn <name>(p0: &T, ...)` (leading `&` on param)
Consumed → `fn <name>(p0: T, ...)` (no `&` on param)
Signature-shape is a fact, not a symptom: Copy-ness does not
collapse it. `fn id(p0: i64)` and `fn id(p0: &i64)` are
distinguishable regardless of whether the type is Copy.
Structure:
- Borrowed-contract tests (`drop`, `is_empty`) run live today —
Phase-1 conservative default already matches Borrowed, so they
verify the §3.3 fact and pass in one step.
- Consumed-contract tests (`id`, `wrap`) are `#[ignore]`'d with
a named Phase-2 unignore trigger. They encode the sound §3.3
fact; running them ignored today confirms they fail as expected
(the emitter renders `&i64` where §3.3 says `i64` for Consumed).
Removing `#[ignore]` is the single action that promotes Lane 6
from half-gate to full §3.3 gate when Phase 2 lands.
Removed the clone-count ratchet entirely — it was unsound and
the reviewer was right to flag it.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Move the one-hop `produced_by` walk from hand-written Rust to src/v3/lenses/provenance.dag. Rust callers consume an auto-emitted snapshot via `v3_compiler::lens_provenance::origin_of`; the hand-written `lens_provenance.rs` is deleted. Migration test (m2_lens_provenance_migration_test.rs) pins the .dag snapshot, ratchets the emitted clone count, and verifies behavioral equivalence against a hand-written oracle across four fixtures. Origin reshaped from 4 variants over `Option<NodeId>` to 5 flat variants because v3's current surface grammar doesn't support Some/None in expression position — `NoProducer` splits out the `by: None` case, `Source(NodeId)` subsumes `by: Some(_)`. Placement is src/v3/lenses/ (sibling to unused_parameters.dag), not src/v3/std/, to avoid double-loading via STAGED_FILES; moving into std/ is follow-up once the compile pipeline tolerates re-lowering files bootstrap already staged. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
# Conflicts: # src/v2/tests/src/bootstrap.rs
ChatGPT ReviewBased on the uploaded diff and the current thesis/review docs: Principle audit. 1. Fail-closed. The provenance migration gets this right: chatgpt-review-52e78a51-3c14-47… 2. Illegal states unrepresentable. Most of the diff moves the right way: generated lens code now comes from chatgpt-review-5dad20b9-0d94-4a… 3. Facts flow forward. This is the strongest part of the PR. Deleting the hand-written provenance lens, introducing chatgpt-review-9665d132-0bfc-4e… chatgpt-review-9665d132-0bfc-4e… 4. Coproduct dissolution. No real concern from me here. The new coproducts in this diff ( 5. Single-authority metadata. Mostly satisfied. chatgpt-review-691b20d4-fb87-4d… 6. API-level enforcement. This is the other place I’m uneasy. The migration harness does not actually prove the new chatgpt-review-52e78a51-3c14-47… Design question. Do you want chatgpt-review-52e78a51-3c14-47… Verdict. REQUEST_CHANGES. The direction is good — especially deleting the hand-written provenance lens and adding real consumer-facing fixture coverage — but I would not merge the cost lens as authority until the silent LOOP HEALTH: converging — this round deletes one real hand-written authority and adds real consumers/tests, but it also surfaces one repeated upstream gap (missing substrate accessors / unpinned |
![chatgpt-codex-connector[bot]](https://avatars.githubusercontent.com/in/1144995?s=60&v=4){kind=small}
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 22651feb59
ℹ️ About Codex in GitHub
Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you
- Open a pull request for review
- Mark a draft as ready
- Comment "@codex review".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".
| remaining - 1, | ||
| d, | ||
| SumPorts, | ||
| port_id, | ||
| payload.tail, |
There was a problem hiding this comment.
The remaining counter is decremented again when recursing over payload.tail, so list traversal burns the same budget as graph descent. In unary chains this undercounts cost because each transform consumes two fuel steps (enter SumPorts + walk tail), causing early cutoff before deeper nodes are visited (a 3-transform chain can report 2). This makes CostLens::cost_of return incorrect values; the tail-walk recursion should not consume depth budget the same way child-port traversal does (the same pattern is also present in MaxPaths).
Useful? React with 👍 / 👎.
briansrls
left a comment
briansrls
left a comment
There was a problem hiding this comment.
codex · gpt-5.4 · 22651feb
BLOCKING (1)
Root Cause
src/v3/std/substrate.dagThe reflected substrate only exposes Dag.ports and Dag.nodes as linear lists, so migrated lenses are forced to invent partial lookups; add total keyed accessors or an explicit lookup-failure carrier, then make complexity.dag propagate that failure instead of returning 0.
Non-blocking — Strengths
src/v3/compiler/src/lib.rsThe new provenance wrapper re-exports only Origin and origin_of, so the lookup scaffolding stays crate-private instead of becoming a second public authority.src/v3/compiler/tests/four_fixture_regression_test.rsThe ignored Consumed cases are documented, bounded, and tied to a named Phase 2 unignore trigger, so Lane 6 lands as tracked debt rather than a false-green gate.
| match mode { | ||
| Port => | ||
| match find_port(d.ports, port_id) { | ||
| MissingPort => 0 |
This comment was marked as resolved.
This comment was marked as resolved.
Sorry, something went wrong.
|
BLOCKING (1) Root Cause
Non-blocking — Strengths
|
…fold
**Bug fix.** The prior fuel seed was `port_count` but each recursive
step decrements fuel twice (once entering a Transform's SumPorts
mode, once walking the input-list tail). Unary transform chains
therefore ran out of fuel early — a 3-transform chain returned 2
instead of 3. Fix: seed = 2 × port_count, which accommodates the
double-decrement without premature termination.
**Scaffold receipt.** Fuel is not the thesis-correct pattern; it's
a workaround for .dag's termination checker. The header comment
now carries a 🟡 scaffold receipt naming three concrete dissolution
triggers:
(a) .dag gains mutual recursion support → graph-descent and
list-descent split into separate structural functions (tried
in this PR, blocked by "mutual recursion not yet supported").
(b) .dag termination checker accepts DAG-walk termination via
substrate invariants (the DAG is acyclic and finite).
(c) Substrate exposes a fold_backward(d, port, f) or forward-fold-
by-topological-order primitive (tried in this PR as forward
fold over d.nodes; blocked by emit_rust dispatch_producer
failing on the new record-literal shape; investigation
deferred).
The oracle for correct behavior remains the original Rust cost
lens at `src/v3/compiler/src/lens_cost.rs` on commit 1247f4b —
a clean recursive walk via total Dag.port() / Dag.node() accessors,
no fuel needed (Rust has no termination checker). This .dag lens
agrees with it on the existing oracle fixture; when any dissolution
trigger fires, the fuel and CostMode scaffold disappear and the
lens becomes a pure structural walk matching the Rust oracle's
shape.
All migration tests pass (complexity_dag_compiles_cleanly,
complexity_dag_matches_handwritten_oracle_on_core_fixtures,
complexity_generated_module_matches_checked_in_snapshot). Generated
module regenerated to reflect the new seed.
Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
ChatGPT ReviewPrinciple audit. 1. Fail-closed. Grounded in THESIS.md’s “if it compiles, the intent is sound” claim and the active fail-closed rule in modeling-discipline.md, I think the provenance migration is in good shape: 2. Illegal states unrepresentable. Most of this diff moves the right way. Lane 6 models 3. Facts flow forward. This is the strongest part of the PR. Deleting the handwritten provenance lens, making 4. Coproduct dissolution. No real issue for me here. The new enums are lens-local carriers, not new substrate enums on 5. Single-authority metadata. Mostly satisfied. 6. API-level enforcement. Lane 6 is careful here: the tests assert a structural consequence of the contract, not a convention, and the ignored cases are honest about what is and is not enforced today ( Design question. What is the canonical decreasing measure for graph-walking compiled lenses over the reflected substrate: ports, edges, or a substrate-level total fold that makes the walk structural by construction? What’s at stake is whether future L2 lens migrations inherit a real substrate guarantee, or whether each one invents a local fuel proof that can silently truncate while still claiming equivalence to the old Rust authority. Verdict. REQUEST_CHANGES. Provenance migration and the four-fixture ownership suite both look clean and genuinely useful. I would not merge the complexity migration yet: the earlier miss-to- LOOP HEALTH: converging — this round deletes one real handwritten authority and adds real consumer tests, but it also introduces a new lens-local proof scaffold whose bound does not match the structure it descends; fix that once before more graph-walking L2 lenses copy the pattern. |
The fuel counter was a 🟡 scaffold that papered over a false gap. The actual blocker in the prior attempt was `Cons(...)` as expression-form constructor (a parser limitation), misattributed as "substrate needs fold_backward primitive." Fix: import `cons` from std.list. Rewrite as forward fold over `d.nodes` — the substrate already emits nodes in dependency order, so a single `fold(d.nodes, empty(), |acc, node| cons(entry_for(acc, node), acc))` walk builds a port→cost entry list in one pass. Termination is structural on the finite List<Behavior>. No fuel, no mutual recursion. Outcomes: - complexity.dag: 271 → 128 lines - lens_cost_generated.rs: 231 → 128 lines - All 250 v3-compiler tests pass - Receipt: 🟡 Scaffold → 🟢 TERMINAL Also adds src/v3/compiler/src/bin/regen_lens_cost.rs to regenerate the snapshot after future complexity.dag edits. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Multi-line method chains broken per rustfmt on the new regen bin. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Two blockers from PR #489 review: A2 — fail-closed on malformed references. lookup_int returned 0 on MissingCost, collapsing "port referenced but absent from d.nodes" into "legitimate zero-cost leaf." Pre-seed the cost accumulator with FoundCost(0) entries for every bind.params port (the only real absent-from-d.nodes zero-cost leaves) and propagate MissingCost through the sum/max helpers via a new CostLookup coproduct. cost_of now returns CostLookup; CostLens::cost_of panics on MissingCost at the Rust boundary, surfacing the fail-closed contract. Bind semantics — explicit boundary. complexity.dag's Bind branch uses `bind.result_port` (substrate name), tests use `bind.value` (Rust struct field). BindNode::result_port() is the single point of agreement; doc comment now says so. Added two Bind-with-parameters fixtures (`fn double(x)`, `fn add(x, y)`) that exercise both the seed_bind_params pre-seed and the Bind branch of entry_for. Test harness: roundtrip harness now compiles once, reads fixtures from argv, and runs inner rustc with -D warnings. Applied uniformly across all three lens migration tests. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
The rustc roundtrip tests added `-D warnings` + `#[allow(warnings, clippy::all)]`
on the emitted `mod emitted { ... }` wrapper. That masks emitter warnings
(unused parens, unused pattern bindings, unused diagnostics import) at the
consumer instead of fixing them at the source.
Deferring the structural fix to a follow-up that teaches emit_rust to:
1. Wrap binops by precedence context, not unconditionally
2. Emit `_` for pattern bindings not referenced in the arm body
3. Include `use v3_compiler::diagnostics::*` only when the module uses it
The compile-once-run-many perf refactor (build_roundtrip_harness) stays
— that is a real structural win independent of the warning story.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
|
ChatGPT review in progress... (view conversation) Check back in ~30 minutes for the full review. |
Meta-Review (Loop Health)Loop summary. 3 substantive rounds, not counting one browser “review in progress” stub. The preserved log shows 1 Codex CLI review and 3 browser events total, of which 2 are full reviews and 1 is only a placeholder. The visible review window runs from 2026-04-16 23:31Z to 2026-04-17 00:27Z, so the recorded loop spans about 57 minutes. The exact total commit count is not recoverable from the uploaded artifacts, but the preserved history clearly shows roughly 2 reviewed commit turns inside this loop. Forward progress evidence. Yes, the loop made real progress. It deleted one real handwritten authority: the provenance lens moved from Rust to The current diff also appears to cash out some of the loop’s earlier blocker reports rather than just rephrase them: the cost lens now separates missing cost from found cost and routes unresolved cost through a fail-closed boundary instead of silently returning a valid-looking Debt accumulation evidence. The same upstream defect was rediscovered across rounds and did not get promoted to a structural fix in this PR: the reflected substrate still exposes There is also tracked but real test debt. The reviews explicitly praise that the ignored Most importantly, the recurring finding did not graduate into a new standing invariant or lens gate, even though the thesis explicitly says the point of lenses is to turn repeated review work into permanent invariant enforcement, and the invariants explicitly say consumers must not reconstruct missing substrate facts locally. On your Principle 3, that is the loop’s real miss. Cheating signal. Low hiding, high accounting. The implementer is not quietly slipping in “good enough for now” patches. The compromises are loud: crate-private scaffolding, named unignore triggers, and explicit review comments tying the remaining lookup helpers to a future keyed-accessor dissolution. The latest fixes are mostly structural, not cosmetic: delete handwritten authority, add real consumers, and move toward substrate-declared lenses. This is implementer triage with accounting, not implementer cheating by concealment. But there is one exhaustion signal: the loop is still accepting lens-local reconstruction because the substrate gap remains open. That is not hidden cheating; it is rational blast-radius minimization under review pressure. The accounting is honest. The structure is still incomplete. Meta-verdict — ⚖️ SHIP_WITH_DEBT This loop is making real forward progress, so it is not a regroup or revert case. But the marginal value of another round on this PR is now low. The remaining problem is clearly upstream substrate shape, not one more local patch in this half. This PR already deleted a real parallel authority and added real consumers. Another review round will mostly keep sanding the same local surfaces while the repeated root cause remains unsolved. Merge this half. Then force the next PR to do the thing this loop kept circling: surface keyed |
Each rustc invocation paid ~3-5s cold linker/codegen on CI; 14 tests serialized into ~60s of pure rustc. Batch all 9 self-contained-program fixtures into one binary (compiled with plain rustc) and all 5 reflected-module fixtures into another (compiled with v3_compiler --extern). Tests dispatch via argv[1]; harnesses are built lazily via `OnceLock<PathBuf>` on first access. Local wall time: m1_3 dropped from 3.37s → 1.70s (-50%). CI win scales with cold-cache rustc cost — expect 40-60s less on the v3 job. Fixture descriptors live in const arrays (`PROGRAM_FIXTURES`, `REFLECTED_FIXTURES`); submodule naming namespaces the emissions so type and function declarations don't collide across fixtures. Group 1 programs get `fn main()` → `pub fn main()` rewritten so the nested main is callable from the dispatcher. The hand-written `roundtrip_stdout` helper stays because the `#[ignore]`d `rustc_roundtrip_int_addition_prints_three` anchor test uses it as the canonical end-to-end example. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
briansrls
left a comment
briansrls
left a comment
There was a problem hiding this comment.
codex · gpt-5.4 · 8bac8978
✅ Review (blocking: 0, non-blocking: 0+/0-)
ROADMAP — Verified
- L2 lens migrations:
complexity.dagandprovenance.dagare now the live authorities with checked-in generated snapshots and passing Rust-oracle roundtrips, which matches theLenses Are Substrate Declarationsratchet. - Lane 6 four-fixture pressure suite:
four_fixture_regression_test.rsasserts the §3.3 fact at the contract/signature layer and bounds the remaining Consumed cases with explicit Phase 2 ignore triggers.
✅ I did not find new concerns; the prior fail-open cost-lens blocker is fixed, and the focused tests I ran (m2_lens_cost_migration_test, m2_lens_provenance_migration_test, m2_lens_unused_parameters_migration_test, four_fixture_regression_test, and m0_acceptance) all passed.
|
✅ Review (blocking: 0, non-blocking: 0+/0-) ROADMAP — Verified
✅ I did not find new concerns; the prior fail-open cost-lens blocker is fixed, and the focused tests I ran ( |
Five test binaries (m1_3_emit_rust, m2_lens_{cost,provenance,unused_parameters}_migration)
each carried identical copies of `deps_dir`, `find_current_rlib`,
`next_roundtrip_dir`, and `compile_with_current_crate`. Extract into
`tests/common/mod.rs`; each test file imports via `mod common;`.
The harness API:
- `RustcHarness::new(scope)` — one per test binary, owns scratch root
and an atomic child-dir counter.
- `harness.compile(source, bin_name, HarnessLinkMode)` — rustc invoke
keyed on link mode. `Standalone` for self-contained emissions,
`WithV3Compiler` for reflected-DAG modules that need the v3_compiler
rlib.
- `RustcHarness::run(bin, args)` — spawn + assert + capture stdout.
Lazy init: each test file wraps `RustcHarness` in its own
`OnceLock<RustcHarness>` so construction happens at first test access
and the harness is reused across every `#[test]` in that binary.
Batched compilations remain lazy via `OnceLock<PathBuf>` on top of
the shared harness.
Net: 339 lines removed, 214 added. Helpers are declared once, and
the "which link mode does this test need?" question becomes a typed
enum rather than a choice between copy/pasted helpers.
`#[allow(dead_code)]` on common/mod.rs: each test binary exercises a
subset of the API (e.g. the cost lens migration never builds a
Standalone harness), so unused items per-binary would otherwise trip
clippy's -D warnings.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Merging origin/main brought in PR #492 (cached bootstrapped DAG construction) and Half A (#489 — lens migrations + tests). Two half-b-introduced semantic changes interacted with the lens snapshot tests: (B3) `is_last_use` was tracking ONLY consume edges; my earlier B3 fix extended it to also record borrows so a Consume followed by a later Borrow correctly returns "not last use." But the OwnedConstructLastUse optimization that consumes the result is unsound when rendered templates reorder evaluation relative to dag.nodes() iteration order — `cons(entry_for(acc, _), acc)` renders as `let mut __list = acc; __list.insert(0, entry_for(&acc, _))`, moving acc (slot 1) before borrowing it (slot 0). Now conservatively emit OwnedConstruct (clone) for every Consumed disposition, matching origin/main's safe behavior. The is_last_use fact is still computed and tracked; the renderer just doesn't act on it. Future template-aware last-use will turn the optimization back on. (B4) decl_is_copy_rec was extended beyond a cycle guard to also walk Conj/Disj structurally — concluding that a user-defined sum like CostLookup is "Copy" because all its leaves are. But emit_rust derives `#[derive(Clone, Debug)]` on user-defined types (NOT Copy), so the algebraic Copy report mismatched the emitted Rust and caused use-after-move (`(__list_head).cost` instead of `((__list_head).cost).clone()`). Reverted the structural walk to match origin/main: only realized types report Copy via their TypeRealization.is_copy field; user-defined Conj/Disj/Instantiation/Cardinality return false. The cycle guard for self-referential types remains in place for B4 correctness. Regenerated lens_cost_generated.rs and lens_unused_parameters_generated.rs from their .dag sources via the regen tools. Added regen_lens_unused_parameters to mirror regen_lens_cost. Bumped MAX_CLONE_CALLS from 1 to 5 (the new conservative count, still below origin/main's 6) with a comment explaining why the optimization was pessimized. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
* Add Go multi-target validation
* [codex] Ownership phase 2 emitter API
* [codex] Allow reserved ownership edge variants
* Fix Go emitter statement separators
* Carry target scope through emitters
* Add Python target emitter for v3
* Exclude pipeline authority from Go emission
* Map DeclarationRef in python target
* Fix Rust field binding regression test
* Fix python emitter clippy warnings
* [codex] Fix ownership clippy lint
* Fix remaining v3 CI regressions
* Address python emitter review feedback
* Fix Go emitter review regressions
* Format compiler sources
* Fix v2 bootstrap CI normalization
* [codex] Fix CI bootstrap verification
* Resolve duplicate type declarations between python.dag and shared computation_model.dag
* Fix CI: rustfmt function rename + cargo fmt
- bootstrap.rs: 3 lingering rustfmt_rs_files call sites from the
Half B merge had not been renamed to rustfmt_generated_crate.
The new function takes a crate root with Cargo.toml; updated
fixed-point check to pass *_dir instead of *_src, removed the
redundant second formatting pass after pass2 (pass already did it).
- emit_python.rs + m1_4_emit_python_test.rs: cargo fmt normalization.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
* emit_rust: address 4 ownership/fail-closed violations
B4 — decl_is_copy now carries a HashSet visited-set, breaking infinite
recursion on self-referential types (e.g. Node { next: Node? }). A type
that contains itself can never be Copy on any target we emit (it needs
heap indirection), so the cycle case fail-closes to false.
B7 — Behavior::Bind no longer merges Consumed when walking user-defined
callable bodies. Bind is a naming node per thesis; the disposition of
the bound value is determined by the downstream consumer of the bound
name, not by the binding itself. Walks transparently now.
B6 — analyze_user_defined_callable returns Result<Vec<...>, EmitError>
with a new MalformedUserDefinedCallable variant. Previous all-Borrowed
fallback on impossible Arrow shapes was fail-open (Arrow body not Bind,
Bind.params shorter than Arrow inputs, etc.). The IR is supposed to be
well-formed when emit runs; reaching these arms is an upstream bug, so
it surfaces as an emit error instead of silently producing wrong code.
B3 — InputUseFacts::build now records every input edge (Borrow and
Consume), and last_use_order_by_port tracks the last edge of any kind
to touch a port. is_last_consumed_use renamed to is_last_use to reflect
the actual semantic ("safe to move at this consume" requires no later
borrow OR consume). Previously the table only stored Consumed edges,
so a `concat(xs, ys)` followed by `length(xs)` could move xs at concat
and then fail to compile when length tried to borrow it.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
* emit_python + emit_go: 3 authority fixes (B14, B-NEW-2, B-NEW-3)
B14 — algebra_field_for_operator now walks the operand type's
instantiation chain to its actual algebra Conj before falling back to
canonical OrderedRing, instead of always pulling from OrderedRing
regardless of operand. Mirrors emit_rust's resolution. Operators on
non-OrderedRing types now dispatch correctly.
B-NEW-2 — emit_go now parses and validates the parameter_dispositions
field on every CallableRealization, fail-closed. Go's GC rendering
doesn't act on the value, but the shared CallableRealization schema
requires the field, and a malformed disposition vector is a spec bug
even when this target ignores the result. Mirrors emit_rust's
require_parameter_dispositions / parse_parameter_disposition.
B-NEW-3 — emit_python's PythonTarget no longer demotes memory and scope
to String. Typed MemoryModelBinding / ScopeModelBinding mirror emit_go,
and the gating check uses enum equality instead of string equality.
Adds scope validation: previously scope was parsed and discarded;
emit_python now also requires scope == LexicalScoping.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
* B1 + B-NEW-1: typed CallableParameter + dissolution receipts
B1 — CallableRealization.parameter_dispositions: List<ParameterDisposition>
becomes parameters: List<CallableParameter>, where each CallableParameter
bundles slot:Int with disposition:ParameterDisposition. Build-time
validation requires every slot in [0, arity) to appear exactly once,
making arity drift, slot duplication, and out-of-range slots all
unrepresentable instead of silently defaulting to Borrowed.
The schema change exposed two pre-existing arity-drift bugs that the
silent default had been masking: rust+go fold_callable was missing
slot 2 (function reference, Borrowed), and map+filter were missing
slot 1 (function reference, Borrowed). Both fixed.
emit_rust + emit_go now compute expected_arity from the callable's
Arrow.inputs.len() and pass it to require_parameter_dispositions,
which fail-closes on any mismatch. New regression test
parameter_dispositions_reject_arity_drift_and_slot_collisions covers
the five failure modes (low arity, high arity, slot duplication,
out-of-range slot, negative slot) plus a well-formed parse.
B-NEW-1 — Every new sum type in computation_model.dag, emit_model.dag,
and python.dag now carries an explicit dissolution receipt:
- Mutability/Purity/Structure/Iteration/MemoryModel/ScopeModel: 🟢
TERMINAL (durable substrate axes, irreducible categories)
- FieldAccess/ParameterDisposition: 🟢 TERMINAL (durable distinctions
every memory-managed target makes)
- ReadStrategy/ConstructStrategy: 🟡 SCAFFOLD (dissolves when
per-edge derivation from MemoryModel × ParameterDisposition lands)
- PythonCallableStrategy/PythonPatternStrategy: 🟡 SCAFFOLD (dissolves
when emit_python migrates to the shared CallableRealization /
PatternRealization schema)
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
* B11: typed TargetLanguage dispatch replaces name-prefix filter
emit_rust and emit_go used to filter shared realization data items by
checking decl.name.starts_with("rust_") / "go_". A realization with
an off-prefix name was silently invisible to its target's emitter,
and renaming a realization for any reason would change which target
owned it. The name was load-bearing where a typed substrate fact
should have been.
Replaces with v3.std.emit_model.TargetLanguage = Rust | Go, added
as a `language: TargetLanguage` field on every shared realization
type (TypeRealization, OperatorRealization, BehaviorRealization,
CallableRealization, PatternRealization, TypeInstantiationRealization).
Each emit_rust / emit_go reads the field and filters by typed equality
instead of name prefix. The realization NAME is no longer load-bearing
for ownership.
All 68 entries in rust.dag and 68 in go.dag updated to declare their
`language`. emit_rust hosts require_target_language and the
TargetLanguageBinding enum (pub(crate) for emit_go to consume).
New regression test target_language_reads_typed_field_not_realization_name
verifies the typed field wins over surface naming: a realization
named e.g. `rust_*` but tagged `language: Go` resolves to Go. The
m1_3_prb_rust_dag_bootstrap_loads_structurally substrate test
updated to expect the new field count (5 instead of 4).
Done gates: grep starts_with("rust_") / starts_with("go_") in emit_*.rs
shows only doc-comment references, no real filter code.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
* Merge main; reconcile lens snapshots after B3+B4 emission semantics
Merging origin/main brought in PR #492 (cached bootstrapped DAG
construction) and Half A (#489 — lens migrations + tests). Two
half-b-introduced semantic changes interacted with the lens snapshot
tests:
(B3) `is_last_use` was tracking ONLY consume edges; my earlier
B3 fix extended it to also record borrows so a Consume followed by
a later Borrow correctly returns "not last use." But the
OwnedConstructLastUse optimization that consumes the result is
unsound when rendered templates reorder evaluation relative to
dag.nodes() iteration order — `cons(entry_for(acc, _), acc)` renders
as `let mut __list = acc; __list.insert(0, entry_for(&acc, _))`,
moving acc (slot 1) before borrowing it (slot 0). Now conservatively
emit OwnedConstruct (clone) for every Consumed disposition, matching
origin/main's safe behavior. The is_last_use fact is still computed
and tracked; the renderer just doesn't act on it. Future
template-aware last-use will turn the optimization back on.
(B4) decl_is_copy_rec was extended beyond a cycle guard to also walk
Conj/Disj structurally — concluding that a user-defined sum like
CostLookup is "Copy" because all its leaves are. But emit_rust derives
`#[derive(Clone, Debug)]` on user-defined types (NOT Copy), so the
algebraic Copy report mismatched the emitted Rust and caused
use-after-move (`(__list_head).cost` instead of `((__list_head).cost).clone()`).
Reverted the structural walk to match origin/main: only realized types
report Copy via their TypeRealization.is_copy field; user-defined
Conj/Disj/Instantiation/Cardinality return false. The cycle guard for
self-referential types remains in place for B4 correctness.
Regenerated lens_cost_generated.rs and lens_unused_parameters_generated.rs
from their .dag sources via the regen tools. Added regen_lens_unused_parameters
to mirror regen_lens_cost. Bumped MAX_CLONE_CALLS from 1 to 5 (the
new conservative count, still below origin/main's 6) with a comment
explaining why the optimization was pessimized.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
* Address codex BLOCKING review on 89a551f: 2 fact-drops fixed
(1) emit_go: PatternRealizationBinding now carries empty_pattern and
cons_pattern from the shared schema. Previously the spec declared
both fields but the Go binding only kept scrutinee/head_expr/tail_expr,
silently dropping two facts at the spec→emitter boundary. The
hardcoded `if len(__list) == 0` is replaced with a render of
`empty_pattern` (Go spec template `"len({expr}) == 0"`). cons_pattern
(Go spec template `"{expr}"` — passthrough) becomes the list
expression that head_expr/tail_expr extract from. Both fields now
participate in emission, satisfying Facts Flow Forward at the
PatternRealization authority.
(2) emit_rust: TargetExecutionModelBinding now carries scope alongside
memory. Previously TargetExecutionModelBinding::build read only
`memory` from rust_execution_model, dropping the scope axis that
the shared TargetExecutionModel schema declared. Added
ScopeModelBinding enum + require_scope_model parser + is_lexically_scoped
predicate (mirror of emit_go); emit_rust_with_mode now fail-closes if
rust_execution_model.scope != LexicalScoping (parallel to the
LexicalScoping check emit_go and emit_python already enforce). Same
fact-drop class as B-NEW-3 which was fixed for Python; Rust missed
the analogous fix.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
* Address principle audit BLOCKING: Python loader + Loop fail-closed
Two structural fixes from the principle audit on commit 89a551f.
(1) emit_python: PythonIndexes::build silently skipped meta-tagged
declarations whose value_body wasn't Structural, AND silently
overwrote duplicate inserts (every HashMap::insert result discarded).
Now fail-closes via new EmitPythonError::DuplicateRealization variant
+ MalformedSpec on non-structural value bodies. Mirrors emit_rust and
emit_go discipline; spec collisions and inhabitance leaks now surface
loudly instead of producing the last-wins emission silently.
(2) emit_go + emit_python: Behavior::Loop was silently rendered as
"the loop body's result port" — semantically collapsing iteration
into its first iteration's expression. Now fail-closes with
EmitError::UnsupportedBehavior / EmitPythonError::Unsupported. The
silent collapse was masking the fact that Loop emission isn't yet
modeled in either target; the BLOCKING audit found it three rounds
running.
The two non-trivial Go/Python lens tests
(emit_go_lens_unused_parameters_module,
emit_python_module_marks_ownership_as_skipped_for_gc_target,
emitted_python_lens_matches_emitted_rust_lens_on_reflected_programs)
now #[ignore] with explicit reasons — they were passing only because
of the silent Loop collapse. They re-enable when Lane 1e consolidation
gains spec-driven Loop emission for Go/Python.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
* fmt: remove stray blank line left after behavior_result_port deletion
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
* Half B reconcile against INVARIANTS E-6/E-7 (PR #493)
After #493 promoted the three meta-review structural rules to
INVARIANTS.md, Half B reconciles against the canonical counter-
examples the audit called out:
E-6 (no target-spec field without a same-PR consumer): delete
go_gc_targets_skip_rendering_model_loading. The test deliberately
corrupted go_rendering and asserted emission succeeded — the
clearest possible "declared target fact is non-authoritative"
signal. Its removal frees go_rendering to become load-bearing.
E-7 (no target-private realization schema without a dissolution
ratchet): add 🟡 SCAFFOLD comments with explicit dissolution
triggers on all five Python-private realization types in
src/v3/spec/python.dag:
- PythonTypeRealization: trigger = Lane 1e + schema grows is_copy
- PythonOperatorRealization: trigger = Lane 1e (pure migration)
- PythonCallableRealization: trigger = Lane 1e decides parameters
policy (schema has slot-keyed dispositions Python doesn't need)
- PythonTypeInstantiationRealization: trigger = Lane 1e (pure)
- PythonPatternRealization: trigger = B13 (parser dotted-path
variant access) + Lane 1e migration
The PythonCallableStrategy / PythonPatternStrategy enums already
had dissolution prose; this commit closes the gap between "two
enums with scaffold notes" and "five realization records without."
Prose discipline now covers the full private realization family.
E-8 was landed as emission-level fail-closed in 128d663 (Loop).
INVARIANTS.md now carries E-8 as the rule the fix implemented.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
* TargetLanguage enum → DeclarationRef typed edge; drop go_rendering
Addresses two structural BLOCKING concerns on PR #490:
(1) Principle audit — target ownership is a compiler roster.
The previous shape `TargetLanguage = Rust | Go` in
v3/std/emit_model.dag enumerated the shared target list AS A
COMPILER-OWNED VARIANT ROSTER. Adding a new shared target (Swift,
Verilog, etc.) required touching the enum, a `TargetLanguageBinding`
mirror in emit_rust, a `require_target_language` helper that
hardcoded Rust/Go variant lookups, and Dag cache slots per target —
exactly the "new target = new compiler path" pattern the thesis
claims to eliminate.
Replaced with a typed edge: every shared realization carries
`language: DeclarationRef` pointing at the owning target's
language-spec declaration (`rust_language`, `go_language`). Each
emitter caches its own language-spec declaration id once at index
build time and filters realizations by declaration-identity
comparison. Adding a new shared target is now strictly a spec-file
change — write `swift.dag` with `data swift_language: LanguageSpec`
and reference it from each `data swift_*` realization. No emit_model
edits, no emit_rust/emit_go edits.
- emit_model.dag: drop `type TargetLanguage`; change every
realization's `language: TargetLanguage` to `language: DeclarationRef`
- rust.dag / go.dag: drop `TargetLanguage, Rust|Go` imports; each
data entry `language: Rust` → `language: rust_language` (typed
ref resolved via dotted-path lowering, same mechanism as `target`)
- emit_rust: delete `TargetLanguageBinding` enum + `require_target_language`
helper; filter = `require_field_decl_ref(...) != rust_language_id`
- emit_go: same filter shape
- m1_substrate_test: update to expect Reference(rust_language_id)
instead of Variant(Rust)
- target_language test rewritten to verify the two language-spec
ids are distinct (the structural signal the filter relies on)
(2) codex BLOCKING on fd654c1 — `go_rendering: RenderingModel` is
declared-not-consumed.
emit_go's GC rendering makes no borrow/move distinctions, so the
ReadStrategy/ConstructStrategy record sits in the spec unused —
speculative authority. Deleted per INVARIANTS.md E-6 (no target-spec
field without a same-PR consumer). Also dropped the dag.rs cache
slot (`go_rendering: Option<DeclarationId>`) and `go_rendering_spec()`
accessor. When Go grows a rendering choice that needs the model,
re-declare it AND wire the emitter consumer in the same PR.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
---------
Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
1 participant
Summary
Half A of the reconciliation split — the three PRs that are largely independent of the ownership schema (Half B covers #482 + #483 + #484, taken by another agent).
Merged in order:
Verification
Local on reconciled branch:
```
cargo test -p v3-compiler
test result: ok. 19 passed (integration tests)
test result: ok. 6 passed (lib tests)
test result: ok. 5 passed, 6 ignored (four-fixture)
test result: ok. 3 passed (cost migration)
test result: ok. 4 passed, 1 ignored (provenance migration)
cargo fmt --all --check → clean
cargo clippy -p v3-compiler --all-targets -- -D warnings → clean
```
Known follow-ups from closed-PR reviews
These are review notes captured in `docs/pr-harvest-summary.md` (on the `reconciliation-l1.5` branch); not blocking for Half A to land:
Coordination with Half B
Half B (other agent): #482 ownership Phase 2 + #483 Go + #484 Python. Half B has schema authority over `TargetExecutionModel`, `CallableRealization::parameter_contracts`, `ParameterDisposition`, and related types. Half A doesn't touch those.
Recommended merge order: Half A first (no schema ownership) → Half B (establishes canonical schema) → follow-ups.
Test plan
🤖 Generated with Claude Code