Repository navigation
fail-closed cross-representation == (numeric model↔realization fork) - #5420
Merged
Merged
Conversation
`Value::eq` funnels heterogeneous model↔realization pairs through its
`_ => false` arm, so `nat_add(85, 32)` — folded as `Succ^85(Int(32))` by
`nat_cata(n: a, zero: b, ..)` — silently compared unequal to the native
`Int(117)`. That is a §5 fail-open, not the §2/§7 redundancy the 🟡
dissolve-on markers track.
Per operator decision (`==` fail-closed, 2026-06-20): raise a typed,
located `InterpError::CrossRepresentationEquality` at the `eval_binop`
`BinOp::Eq`/`Ne` seam when a `false` result is *explained* by a native
`Int`/`Float` vs `Nat`-coproduct straddle. `Value::eq` stays infallible
— it is the single `CanonKey` map-key authority and its `Hash`-consistent
`false` must stand — so the guard is a read-only diagnosis over the same
structural recursion, run only on a `false`. It recurses, so
`nat_add == nat_add` and `[nat_add(1,1)] == [2]` are caught; genuine
inequalities (`1 == 2`, `Succ{..} == Zero`) and reconciled forks
(`[1,2,3] == Cons{..}`) pass through as a plain bool. Scalar/string pairs
short-circuit without flattening, so the hot path stays O(1).
Scope is the numeric tower — the proven, corpus-safe fork. The corpus has
no native-`Bool` vs `True|False` `==`, and `Optional/Witness` over
`Value::Null` can't take a blanket guard (`Value::Null` is the overloaded
`None`/`Absent`/miss sentinel; `present == None`, 131 sites, is a
legitimate `false`) — those need the root grounding, recorded in DESIGN.md
"Open threads".
Regression: `cross_representation_equality_test` runs the operator's
receipts by execution — forks → typed error, controls → bool.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01CL6KyE555dMLV9PWMXiEtS
briansrls
added a commit
that referenced
this pull request
Jun 21, 2026
… (fixes v1↔v2 FreeMonoid collision) The type/constructor environment keyed names by bare interned string and an implicit bootstrap bridge injected v1 `std.types`' whole transitive env as a base into every module that didn't import it. Together these let v1's `std.algebra` FreeMonoid (a record) and v2's `v2.std.algebra` FreeMonoid (`Empty | Cons` sum) collide — the winner decided by the topological typecheck order, which the std.types implicit edges coupled across the v1 and v2 trees into one global sort. Adding import edges (e.g. #5418's 44 extdeps anchors) perturbed that order, so `v2.std.node_query` bound FreeMonoid to the leaked v1 record and produced `undefined variable 'Empty'` / `variant 'Empty' not found in type 'FreeMonoid'` across the v2 tree. A §3 single-authority violation. Fix (authority in src/v1/*.dag, mirrored in the stage0 seed .rs): - 03_resolve.dag `topological_sort`: drop the implicit `std.types -> *` edges and the implicit in-degree term. Ordering is now import-driven only, so the two trees decouple and a module is always typechecked after the modules it actually imports — no order-sensitivity to re-tune. - 04_infer.dag `build_type_env` / `build_type_env_unresolved`: drop the `std.types` base-injection. Import bindings start empty and are seeded only by the module's explicit imports; kernel primitives still come from the kernel env. No second, implicit authority for names. Witness (src/v1/tests/src/module_authority_resolution_test.rs): a module that never imports `std.types` no longer inherits a type `std.types` declares — the reference is a hard UnresolvedType (RED without the fix, where the leak silently resolved it). Plus two §3 invariant guards for same-named types across modules. Verified by execution: the #5418-anchored discovery-corpus repro (wet_hermetic_scaffold_roster_filter_uses_dag_prefix_authority) goes green; regen_stage0 self-compiles the v1 tree clean without the leak; full `cargo test --workspace` green except the pre-existing regen receipt-hash red (#5420); clippy + fmt clean. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
briansrls
added a commit
that referenced
this pull request
Jun 21, 2026
… (fixes v1↔v2 FreeMonoid collision) The type/constructor environment keyed names by bare interned string and an implicit bootstrap bridge injected v1 `std.types`' whole transitive env as a base into every module that didn't import it. Together these let v1's `std.algebra` FreeMonoid (a record) and v2's `v2.std.algebra` FreeMonoid (`Empty | Cons` sum) collide — the winner decided by the topological typecheck order, which the std.types implicit edges coupled across the v1 and v2 trees into one global sort. Adding import edges (e.g. #5418's 44 extdeps anchors) perturbed that order, so `v2.std.node_query` bound FreeMonoid to the leaked v1 record and produced `undefined variable 'Empty'` / `variant 'Empty' not found in type 'FreeMonoid'` across the v2 tree. A §3 single-authority violation. Fix (authority in src/v1/*.dag, mirrored in the stage0 seed .rs): - 03_resolve.dag `topological_sort`: drop the implicit `std.types -> *` edges and the implicit in-degree term. Ordering is now import-driven only, so the two trees decouple and a module is always typechecked after the modules it actually imports — no order-sensitivity to re-tune. - 04_infer.dag `build_type_env` / `build_type_env_unresolved`: drop the `std.types` base-injection. Import bindings start empty and are seeded only by the module's explicit imports; kernel primitives still come from the kernel env. No second, implicit authority for names. Witness (src/v1/tests/src/module_authority_resolution_test.rs): a module that never imports `std.types` no longer inherits a type `std.types` declares — the reference is a hard UnresolvedType (RED without the fix, where the leak silently resolved it). Plus two §3 invariant guards for same-named types across modules. Verified by execution: the #5418-anchored discovery-corpus repro (wet_hermetic_scaffold_roster_filter_uses_dag_prefix_authority) goes green; regen_stage0 self-compiles the v1 tree clean without the leak; full `cargo test --workspace` green except the pre-existing regen receipt-hash red (#5420); clippy + fmt clean. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
briansrls
added a commit
that referenced
this pull request
Jun 21, 2026
… (fixes v1↔v2 FreeMonoid collision) (#5422) The type/constructor environment keyed names by bare interned string and an implicit bootstrap bridge injected v1 `std.types`' whole transitive env as a base into every module that didn't import it. Together these let v1's `std.algebra` FreeMonoid (a record) and v2's `v2.std.algebra` FreeMonoid (`Empty | Cons` sum) collide — the winner decided by the topological typecheck order, which the std.types implicit edges coupled across the v1 and v2 trees into one global sort. Adding import edges (e.g. #5418's 44 extdeps anchors) perturbed that order, so `v2.std.node_query` bound FreeMonoid to the leaked v1 record and produced `undefined variable 'Empty'` / `variant 'Empty' not found in type 'FreeMonoid'` across the v2 tree. A §3 single-authority violation. Fix (authority in src/v1/*.dag, mirrored in the stage0 seed .rs): - 03_resolve.dag `topological_sort`: drop the implicit `std.types -> *` edges and the implicit in-degree term. Ordering is now import-driven only, so the two trees decouple and a module is always typechecked after the modules it actually imports — no order-sensitivity to re-tune. - 04_infer.dag `build_type_env` / `build_type_env_unresolved`: drop the `std.types` base-injection. Import bindings start empty and are seeded only by the module's explicit imports; kernel primitives still come from the kernel env. No second, implicit authority for names. Witness (src/v1/tests/src/module_authority_resolution_test.rs): a module that never imports `std.types` no longer inherits a type `std.types` declares — the reference is a hard UnresolvedType (RED without the fix, where the leak silently resolved it). Plus two §3 invariant guards for same-named types across modules. Verified by execution: the #5418-anchored discovery-corpus repro (wet_hermetic_scaffold_roster_filter_uses_dag_prefix_authority) goes green; regen_stage0 self-compiles the v1 tree clean without the leak; full `cargo test --workspace` green except the pre-existing regen receipt-hash red (#5420); clippy + fmt clean. Co-authored-by: Brian Searls <briansrls@gunb.ai> Co-authored-by: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
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.
What
nat_add(85, 32) == 117silently returnedfalse.nat_addfolds vianat_cata(n: a, zero: b, ..), building the non-canonical hybridSucc^85(Int(32))— aVariantchain with a nativeIntleaf — whichValue::eqcannot reconcile against the nativeInt(117), so it falls through its_ => falsearm and fabricatesfalse. That is a §5 fail-open (a silent wrong answer), not the §2/§7 migration redundancy the 🟡 dissolve-on markers track.Per the operator decision (
==fail-closed, 2026-06-20), this makes a cross-representation==/!=a typed, located error instead of a silentfalse.How
InterpError::CrossRepresentationEquality, raised at theeval_binopBinOp::Eq/Neseam when afalseresult is explained by a nativeInt/FloatvsNat-coproduct straddle.Value::eqis left infallible — it is the singleCanonKeymap-key authority and itsHash-consistentfalsemust stand (§3). The guard is a read-only diagnosis over the same structural recursion, run only on afalse, so it never becomes a second equality authority.nat_add(85,32) == 117), the Variant-vs-Variant non-canonical fork (nat_add(85,32) == nat_add(100,17)), and forked list elements ([nat_add(1,1)] == [2]).1 == 2,Succ{..} == Zero) and reconciled forks ([1,2,3] == Cons{..}) pass through as a plain bool. Scalar/string pairs short-circuit without flattening, so the hot path stays O(1).Scope
Numeric tower only — the proven, corpus-safe fork. Deliberately not a blanket guard:
Bool True|FalseoverValue::Bool: no native-BoolvsTrue|False==site exists in the corpus.Optional/WitnessoverValue::Null:Value::Nullis the overloadedNone/Absent/miss sentinel, andpresent == None(131 sites) is a legitimatefalse— a blanket guard would break it. These need the root grounding (§1/§2/§7), recorded inDESIGN.md"Open threads".Verification (by execution)
cross_representation_equality_testruns the operator's receipts: forks → typed error, controls →true, genuine diffs →false. 3/3 green.cargo clippy --all-targets -- -D warningsandcargo fmt --all --check: clean.claim_batch --roster-from-discovery): no new failures vs baseline (only the 3 pre-existing hermetic-mock skips).Note (pre-existing, unrelated)
cargo test --workspacefails fast onregen_stage0'scargo_invalidation_receipt_hashes_workspace_and_stage0_manifests— a test whose setup createssrc/v2/stage0/Cargo.tomlbut assertssrc/v1/stage0/...(a stale v1→v2 migration artifact committed in32bade1, in a file this PR does not touch). Left for a separate fix since the correct migration direction is ambiguous.🤖 Generated with Claude Code
Generated by Claude Code