fail-closed cross-representation == (numeric model↔realization fork)

DESIGN.md

@@ -186,6 +186,23 @@ still a violation) · internal review finds missing tests, external review finds
   the argument itself; the §7 recursion, with this document as the first target). (operator's next
   project)
 - can a lens mechanically diagnose the *leaf-side* of decomposition (§2)? (operator-parked)
+- the model↔realization fork is systemic, and where unfinished it fails open: every primitive is
+  modeled as a coproduct and realized as a native `Value`, reconciled by per-site bridges, so coverage
+  is accidental and non-compositional. `match` bridges `Int→Zero/Succ` but `Value::eq` has no
+  `Int↔Variant` arm, so `nat_add(85, 32) == 117` silently compared `false` at its `_ => false`
+  chokepoint — a §5 fail-open, not the §2/§7 redundancy the 🟡 dissolve-on markers track. **Landed:** the
+  *numeric tower* fork now fails closed — `eval_binop`'s `BinOp::Eq`/`Ne` raises
+  `InterpError::CrossRepresentationEquality` when a `false` result is *explained* by a native
+  `Int`/`Float` vs `Nat`-coproduct straddle (recursive: catches `nat_add == nat_add` and
+  `[nat_add(1,1)] == [2]`), with `Value::eq` left infallible so it stays the single `CanonKey` map-key
+  authority. The discriminating witness is `cross_representation_equality_test` (forks → typed error;
+  reconciled/native → `true`; genuine diffs `1 == 2`/`Succ{..} == Zero` → `false`, not error). **Remaining:**
+  (a) the same straddle for `Bool True|False` over `Value::Bool` (no `==` site in the corpus today) and
+  `Optional/Witness` over `Value::Null` — the latter resists a blanket guard because `Value::Null` is
+  the overloaded `None`/`Absent`/miss sentinel and `present == None` (131 sites) is a *legitimate* `false`,
+  so it needs grounding, not an error arm; (b) the root fix (§1/§2/§7) — ground each primitive into its
+  realization (numeric tower first, `Int = GroupCompletion<Nat>` still bottoming in Peano `Nat`), which
+  dissolves the straddle and makes the guard dead code. (operator: `==` fail-closed, 2026-06-20)
 - the remaining deleted-`docs/` references in `.dag` comments — provenance / `bind:` pointers into the bankrupted `docs/` tree (e.g. `docs/planning/*`, `design-*.md`) — fold into the dep-graph reform, not a blind repoint. (The named-corpus ledger marks — `Practice N`, and `INVARIANTS` / `THESIS` / `MODELING` / `RELEASE_TODO` / … citations — were swept: dropped, or re-homed to DESIGN.md §-anchors.)
 
 ## Building & checks

src/v1/stage0/src/v1_interpreter.rs

@@ -747,6 +747,13 @@ pub enum InterpError {
     NoSuchVariable { name: String },
     NoSuchField { type_name: String, field: String },
     TypeError { msg: String },
+    // A `==`/`!=` whose operands straddle the model↔realization boundary — a
+    // native scalar number (`Int`/`Float`) against the coproduct model encoding
+    // of a number (a `Nat` `Zero`/`Succ` Variant). `Value::eq` cannot decide such
+    // a pair and would silently return `false` (its `_ => false` arm) — a §5
+    // fail-open. Raised at the eval seam so the silent wrong answer becomes a
+    // loud, typed one. (DESIGN §5; operator: `==` fail-closed, 2026-06-20.)
+    CrossRepresentationEquality { detail: String },
     PatternMatchFailure { value: String },
     DivisionByZero,
     Unimplemented { what: String },
@@ -763,6 +770,9 @@ impl fmt::Display for InterpError {
                 write!(f, "no field '{}' on type '{}'", field, type_name)
             }
             InterpError::TypeError { msg } => write!(f, "type error: {}", msg),
+            InterpError::CrossRepresentationEquality { detail } => {
+                write!(f, "cross-representation equality: {}", detail)
+            }
             InterpError::PatternMatchFailure { value } => {
                 write!(f, "non-exhaustive pattern match on: {}", value)
             }
@@ -1884,12 +1894,32 @@ fn eval_binop(op: &BinOp, left: Value, right: Value, ctx: &InterpContext) -> Int
         }
     }
 
-    // Equality (works on all comparable types)
-    if matches!(op, BinOp::Eq) {
-        return Ok(Value::Bool(left == right));
-    }
-    if matches!(op, BinOp::Ne) {
-        return Ok(Value::Bool(left != right));
+    // Equality (works on all comparable types). `Value::eq` is the single
+    // equality authority (also the `CanonKey` map-key authority, so it stays an
+    // infallible `PartialEq` and its `Hash`-consistent `false` must stand). A
+    // heterogeneous model↔realization pair it cannot decide funnels through its
+    // `_ => false` arm; fabricating that `false` is a §5 fail-open — e.g.
+    // `nat_add(85, 32)` builds `Succ^85(Int(32))` and silently compares unequal
+    // to the native `Int(117)`. Fail closed: when the result is `false` AND a
+    // cross-representation numeric straddle *explains* it, raise a typed error
+    // here at the eval seam rather than returning the silent `false`. The check
+    // only runs on a `false` result and only flags the straddle, so genuine
+    // inequalities (`1 == 2`, `Succ {..} == Zero`) and reconciled forks
+    // (`[1,2,3] == Cons {..}`) pass through untouched. (DESIGN §5; operator:
+    // `==` fail-closed, 2026-06-20.)
+    if matches!(op, BinOp::Eq | BinOp::Ne) {
+        let equal = left == right;
+        if !equal {
+            if let Some(detail) = cross_representation_numeric_straddle(&left, &right) {
+                return Err(InterpError::CrossRepresentationEquality { detail });
+            }
+        }
+        let result = if matches!(op, BinOp::Eq) {
+            equal
+        } else {
+            !equal
+        };
+        return Ok(Value::Bool(result));
     }
 
     // Boolean operators
@@ -1927,6 +1957,121 @@ fn eval_binop(op: &BinOp, left: Value, right: Value, ctx: &InterpContext) -> Int
     }
 }
 
+/// Diagnose a *cross-representation numeric straddle*: a native scalar number
+/// (`Value::Int`/`Value::Float`) compared, at some structural position, against
+/// the coproduct **model** encoding of a number (a `Nat` `Zero`/`Succ` Variant,
+/// the §1/§2/§7 model↔realization fork). The two sides denote one value space in
+/// two encodings, so `Value::eq` cannot decide them and silently returns `false`
+/// through its `_ => false` arm. Returns a description of the first straddle
+/// found so the caller can fail closed (§5) instead of fabricating that `false`;
+/// returns `None` when the inequality is a genuine value difference
+/// (`1 == 2`, `Succ {..} == Zero`).
+///
+/// Single-authority (§3): this NEVER decides equality — `Value::eq` is the one
+/// authority and is left untouched. This is a read-only *diagnosis* of why `eq`
+/// already returned `false`, so it is called only on that `false` and mirrors
+/// `eq`'s structural recursion (matching variant names / record fields / flattened
+/// FreeMonoid elements) — it inspects exactly the positions `eq` compared.
+fn cross_representation_numeric_straddle(a: &Value, b: &Value) -> Option<String> {
+    match (a, b) {
+        // The straddle itself: a native scalar number vs a *non-FreeMonoid*
+        // coproduct Variant (a `Nat` `Zero`/`Succ` chain). A list-shaped Variant is
+        // reconciled by `Value::eq`, and an Int-vs-list pair is a genuine
+        // difference, so exclude FreeMonoid variants.
+        (Value::Int(_) | Value::Float(_), v @ Value::Variant { .. })
+        | (v @ Value::Variant { .. }, Value::Int(_) | Value::Float(_))
+            if free_monoid_to_vec(v).is_none() =>
+        {
+            Some(format!(
+                "{} vs {} — a number and its coproduct (Nat Zero/Succ) encoding are \
+                 two representations of one value; Value::eq cannot decide them, so \
+                 `==` would silently fabricate `false` (DESIGN §5). Ground the \
+                 primitive into its realization to compare (DESIGN §1/§2/§7).",
+                describe_repr(a),
+                describe_repr(b),
+            ))
+        }
+        // No Variant present ⇒ no numeric straddle. This is the hot path for a
+        // `false` `==` (two Strs, two Ints, …): short-circuit WITHOUT flattening.
+        // A `Str` is a sequence of `Int` codepoints, so two scalars/strings can only
+        // ever compare Int-vs-Int, never number-vs-Variant — flattening every false
+        // string compare (self-compile does millions) would be the dominant cost.
+        (
+            Value::Int(_)
+            | Value::Float(_)
+            | Value::Bool(_)
+            | Value::Null
+            | Value::Unit
+            | Value::Str(_),
+            Value::Int(_)
+            | Value::Float(_)
+            | Value::Bool(_)
+            | Value::Null
+            | Value::Unit
+            | Value::Str(_),
+        ) => None,
+        // Same-name coproduct or any record: recurse the matching structure, so a
+        // straddle nested inside (two non-canonical `Succ^k(Int)` chains, or a
+        // number inside a field) is still caught.
+        (
+            Value::Variant {
+                variant_name: an,
+                fields: af,
+                ..
+            },
+            Value::Variant {
+                variant_name: bn,
+                fields: bf,
+                ..
+            },
+        ) if an == bn => fields_numeric_straddle(af, bf),
+        (Value::Record { fields: af, .. }, Value::Record { fields: bf, .. }) => {
+            fields_numeric_straddle(af, bf)
+        }
+        // Native lists: walk elements in place (no materialization) — a forked
+        // element straddles (`[nat_add(1,1)] == [2]`) even though `Value::eq`
+        // reconciles the container.
+        (Value::List(av), Value::List(bv)) => av
+            .iter()
+            .zip(bv.iter())
+            .filter(|(x, y)| x != y)
+            .find_map(|(x, y)| cross_representation_numeric_straddle(x, y)),
+        // Rare mixed FreeMonoid forms (Cons-chain vs List/Str): flatten only here.
+        _ => match (free_monoid_to_vec(a), free_monoid_to_vec(b)) {
+            (Some(av), Some(bv)) => av
+                .iter()
+                .zip(bv.iter())
+                .filter(|(x, y)| x != y)
+                .find_map(|(x, y)| cross_representation_numeric_straddle(x, y)),
+            _ => None,
+        },
+    }
+}
+
+/// Shared-key field walk for [`cross_representation_numeric_straddle`]: recurse
+/// only the positions `Value::eq` compared (shared keys with unequal values).
+fn fields_numeric_straddle(
+    af: &HashMap<Symbol, Value>,
+    bf: &HashMap<Symbol, Value>,
+) -> Option<String> {
+    af.iter()
+        .filter_map(|(k, av)| bf.get(k).map(|bv| (av, bv)))
+        .filter(|(av, bv)| av != bv)
+        .find_map(|(av, bv)| cross_representation_numeric_straddle(av, bv))
+}
+
+/// One operand's representation, for the cross-representation diagnostic.
+fn describe_repr(v: &Value) -> String {
+    match v {
+        Value::Int(n) => format!("native Int({})", n),
+        Value::Float(f) => format!("native Float({})", f),
+        Value::Variant { variant_name, .. } => {
+            format!("coproduct Variant `{}`", resolve_sym(*variant_name))
+        }
+        other => other.type_label().to_string(),
+    }
+}
+
 fn eval_int_binop(op: &BinOp, a: i64, b: i64) -> InterpResult<Value> {
     match op {
         BinOp::Add => Ok(Value::Int(a + b)),

src/v1/tests/src/cross_representation_equality_test.rs

@@ -0,0 +1,135 @@
+//! Fail-closed cross-representation `==` (DESIGN §5; operator: `==` fail-closed,
+//! 2026-06-20).
+//!
+//! Every v2 primitive is modeled as a coproduct and realized as a native
+//! `Value`; where a bridge is missing the two representations silently disagree.
+//! `nat_add(a, b)` folds via `nat_cata(n: a, zero: b, ..)`, so it builds the
+//! non-canonical hybrid `Succ^a(Int(b))` — a `Variant` chain with a native `Int`
+//! leaf. Comparing that to a native `Int` funnels through `Value::eq`'s
+//! `_ => false` arm and silently returns `false` — a §5 fail-open
+//! (`nat_add(85, 32) == 117` → `false`).
+//!
+//! The fix makes such a comparison a typed, located error at the `eval_binop`
+//! `BinOp::Eq`/`Ne` seam (leaving `Value::eq` infallible for `CanonKey`). This
+//! is the discriminating witness for that safety property: the forks below go
+//! RED (a silent `false`/`true`) the instant the guard regresses, while genuine
+//! inequalities and reconciled forks must keep returning a plain bool.
+
+use std::rc::Rc;
+
+use v1_compiler::cli_run;
+use v1_compiler::v1_compiler_compile::{compile_to_resolved, ResolvedPipelineResult};
+use v1_compiler::v1_interpreter::{self, ExecutionMode, InterpError, Value};
+
+use crate::helpers::{resolve_imports_transitively_with_source_roots, workspace_root};
+
+/// Receipts from the operator's diagnosis (2026-06-20), authored as individual
+/// witness functions so each can be run and classified independently.
+const RECEIPTS_SOURCE: &str = r#"
+module test.xrepr
+
+import v2.std.logic { Bool }
+import v2.std.nat { Nat, Succ, Zero, nat_add }
+import v2.std.algebra { Cons, Empty }
+
+// --- forks: must FAIL CLOSED (typed error), never a silent bool ---
+fn fork_nat_add_eq_int() -> Bool { nat_add(a: 85, b: 32) == 117 }
+fn fork_nat_add_1_1_eq_2() -> Bool { nat_add(a: 1, b: 1) == 2 }
+fn fork_nat_add_noncanon() -> Bool { nat_add(a: 85, b: 32) == nat_add(a: 100, b: 17) }
+fn fork_list_element() -> Bool { [nat_add(a: 1, b: 1)] == [2] }
+fn fork_ne_path() -> Bool { nat_add(a: 1, b: 1) != 2 }
+
+// --- controls: reconciled / native, must stay Bool(true) ---
+fn ok_native_int_eq() -> Bool { (85 + 32) == 117 }
+fn ok_nat_add_reflexive() -> Bool { nat_add(a: 85, b: 32) == nat_add(a: 85, b: 32) }
+fn ok_list_freemonoid_reconciled() -> Bool {
+  [1, 2, 3] == Cons { head: 1, tail: Cons { head: 2, tail: Cons { head: 3, tail: Empty } } }
+}
+
+// --- genuine differences: must stay Bool(false), NOT error (no false positives) ---
+fn diff_int() -> Bool { 1 == 2 }
+fn diff_variant_name() -> Bool { (Succ { prev: Zero }) == Zero }
+fn diff_list_elements() -> Bool { [1, 2] == [1, 3] }
+"#;
+
+fn assert_resolved(resolved: &ResolvedPipelineResult) {
+    let msgs: Vec<String> = resolved
+        .diagnostics
+        .iter()
+        .map(|d| v1_compiler::v1_std_core::diagnostic_to_message(d.diagnostic.clone()))
+        .filter(|m| !m.starts_with("complexity: "))
+        .collect();
+    assert!(
+        msgs.is_empty() && resolved.graph.is_some(),
+        "receipts source should resolve cleanly, got {:?} (graph present: {})",
+        msgs,
+        resolved.graph.is_some(),
+    );
+}
+
+/// Resolve the receipts once and run `body` against the eval context, keeping the
+/// resolved graph alive for the duration of the call (the context borrows it).
+fn with_receipts_ctx<R>(body: impl FnOnce(&v1_interpreter::InterpContext) -> R) -> R {
+    let ws = workspace_root();
+    let roots = [ws.join("src/v2"), ws.join("dsl")];
+    let sources =
+        resolve_imports_transitively_with_source_roots("test.dag", RECEIPTS_SOURCE, &roots);
+    let resolved = compile_to_resolved(Rc::new(sources));
+    assert_resolved(&resolved);
+    let graph = resolved.graph.as_ref().expect("graph");
+    let ctx =
+        cli_run::make_eval_context(graph, resolved.source_indices.clone(), ExecutionMode::Wet);
+    body(&ctx)
+}
+
+#[test]
+fn cross_representation_forks_fail_closed() {
+    with_receipts_ctx(|ctx| {
+        for f in [
+            "fork_nat_add_eq_int",
+            "fork_nat_add_1_1_eq_2",
+            "fork_nat_add_noncanon",
+            "fork_list_element",
+            "fork_ne_path",
+        ] {
+            match v1_interpreter::run_in_context(ctx, f, false) {
+                Err(InterpError::CrossRepresentationEquality { .. }) => {}
+                other => panic!(
+                    "{f}: expected Err(CrossRepresentationEquality) — a silent bool here is the \
+                     §5 fail-open this guard closes; got {other:?}"
+                ),
+            }
+        }
+    });
+}
+
+#[test]
+fn reconciled_and_native_equality_still_true() {
+    with_receipts_ctx(|ctx| {
+        for f in [
+            "ok_native_int_eq",
+            "ok_nat_add_reflexive",
+            "ok_list_freemonoid_reconciled",
+        ] {
+            match v1_interpreter::run_in_context(ctx, f, false) {
+                Ok(Value::Bool(true)) => {}
+                other => panic!("{f}: expected Bool(true), got {other:?}"),
+            }
+        }
+    });
+}
+
+#[test]
+fn genuine_inequalities_stay_false_not_errors() {
+    with_receipts_ctx(|ctx| {
+        for f in ["diff_int", "diff_variant_name", "diff_list_elements"] {
+            match v1_interpreter::run_in_context(ctx, f, false) {
+                Ok(Value::Bool(false)) => {}
+                other => panic!(
+                    "{f}: expected Bool(false) — the guard must flag only representation \
+                     straddles, not genuine differences; got {other:?}"
+                ),
+            }
+        }
+    });
+}

src/v1/tests/src/lib.rs

@@ -28,6 +28,8 @@ mod coproduct_reflection_conformance_test;
 #[cfg(test)]
 mod cron_tag_test;
 #[cfg(test)]
+mod cross_representation_equality_test;
+#[cfg(test)]
 mod data_cache_scoping_test;
 #[cfg(test)]
 mod dependency_pool_index_compile_test;