Repository navigation
INVARIANTS: promote E-6/E-7/E-8 emission rules - #493
Merged
Merged
Conversation
The principle audit on PR #490 identified a class of issue that kept recurring across three review rounds: target-spec fields declared but not consumed, target-private realization schemas without dissolution triggers, and silent semantic collapse on unsupported Behavior variants. Each individual fix was landing per-instance; the rules were not. Promote the three rules the reviews already discovered: - E-6: No target-spec field without a same-PR consumer. Speculative target-spec fields become advisory metadata; the "declare now, consume later" pattern normalizes a non-authoritative target spec. Canonical counter-example: the go_gc_targets_skip_rendering_model_loading test, which codified "declared target fact is non-authoritative" as a unit-tested property. - E-7: No target-private realization schema without a dissolution ratchet. Parallel realization families (PythonTypeRealization, PythonCallableRealization, etc.) are permitted only as time-bounded scaffolds with explicit dissolution triggers naming a PR or lane. Grep gate: target-private realization data types outside v3/std/emit_model.dag must carry an adjacent scaffold comment. - E-8: Unsupported core behaviors fail closed, never collapse semantically. When an emitter reaches a Behavior variant with no rendering strategy, it returns UnsupportedBehavior — never a structural substitute. Canonical incident: emit_go and emit_python silently rendering Behavior::Loop as "the loop body's result port," which collapsed fold(list, init, f) into f(init, head(list)). Each rule has: the rule itself, why it's distinct from existing invariants, the canonical incident, structural prevention (CI grep gate or review test), and a PR-review test. Placed as siblings of "Emission is translation, not decision-making" since they specialize the emitter-boundary principle. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
briansrls
added a commit
that referenced
this pull request
Apr 17, 2026
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>
briansrls
added a commit
that referenced
this pull request
Apr 17, 2026
* 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>
briansrls
added a commit
that referenced
this pull request
Apr 17, 2026
Declares the clean-emission contract type system (8 rules in std/clean_emission.dag), populates rust_clean_emission in spec/ rust.dag, wires emit_rust to dispatch on PatternBindingRule:: EmitUnderscoreWhenUnused in render_branch_pattern, and adds INVARIANTS.md E-5. Match-arm payload bindings that the arm body does not consume now render as `_` by construction, so the emitted code passes `rustc -D unused_variables` without suppression. Port-liveness is a structural walk from path.output over producer→input edges; no textual scanning of rendered body strings. Scope split documented in the stage doc and src/v3/ROADMAP.md active-deferrals: PR 2 adds Go + Python pilots; PR 3 wires post_emit_verifier as a hard CI gate. Also reconciles the stage doc with DB-4 (5→8 fields, strikes the stale "candidate companion invariants E-6/E-7/E-8" section — those already landed in PR #493). Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
8 tasks done
briansrls
added a commit
that referenced
this pull request
Apr 17, 2026
* Lane 1 Stage 1c PR 1: E-5 clean-emission invariant + Rust pilot Declares the clean-emission contract type system (8 rules in std/clean_emission.dag), populates rust_clean_emission in spec/ rust.dag, wires emit_rust to dispatch on PatternBindingRule:: EmitUnderscoreWhenUnused in render_branch_pattern, and adds INVARIANTS.md E-5. Match-arm payload bindings that the arm body does not consume now render as `_` by construction, so the emitted code passes `rustc -D unused_variables` without suppression. Port-liveness is a structural walk from path.output over producer→input edges; no textual scanning of rendered body strings. Scope split documented in the stage doc and src/v3/ROADMAP.md active-deferrals: PR 2 adds Go + Python pilots; PR 3 wires post_emit_verifier as a hard CI gate. Also reconciles the stage doc with DB-4 (5→8 fields, strikes the stale "candidate companion invariants E-6/E-7/E-8" section — those already landed in PR #493). Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * Fix Rust wildcard payload aliasing * Reject invalid Rust pattern binding rules * Format Rust pattern binding hardening * Model verifier output policy structurally --------- Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
Why this PR (Path B from the meta-review)
The principle audit on #490 identified that individual fact-drop / silent-collapse / parallel-schema fixes were landing per-instance, but the structural rules were not. Per-instance fixes keep the same class of bug moving to new files. The meta-review's verdict was PAUSE_AND_REGROUP — "write the structural rule the reviews already discovered" before accepting more per-instance compromises.
#490 landed E-8 as a fix (Loop fail-closed in emit_go + emit_python). E-6 and E-7 fixes are partial — the canonical counter-examples (
go_gc_targets_skip_rendering_model_loadingtest, Python-private realization schema) are still there. This PR promotes all three to INVARIANTS.md so:Test plan
go_gc_targets_skip_rendering_model_loading, add dissolution triggers on the five Python private realization types (PythonTypeRealization, PythonOperatorRealization, PythonCallableRealization, PythonTypeInstantiationRealization, PythonPatternRealization)🤖 Generated with Claude Code