brink-format 0.0.17

//! Law: **deep/structural equality** (`docs/value-model-spec.md` §3, §5) —
//! issue #746 item 3, the "dedicated deep-equality law suite" left as
//! residue by #738's `law_cow_sharing.rs`. That suite proves the *sharing*
//! side of §3 (a mutated shared clone and a mutated deep copy converge) for
//! `Array`/`Map`/`Record` only. This suite proves the *equality relation
//! itself* — `impl PartialEq for Value` (`brink-format/src/value.rs`) — over
//! every `Value` variant except the runtime-only `TempPointer` (never
//! generated by [`law_support::arb_value_full`] — it has no wire
//! representation to round-trip and no meaningful equality outside a single
//! VM step, see that module's doc comment), via
//! [`law_support::arb_value_full`]:
//!
//! - **reflexive**: `v == v` for every generated `v` (mod the one
//!   documented IEEE-754 exception below);
//! - **symmetric**: `a == b` iff `b == a`;
//! - **variant-discriminating**: two values of different `Value` variants
//!   are never equal, regardless of payload — pins the hand-written impl's
//!   trailing `_ => false` catch-all against ever being silently bypassed by
//!   a future match-arm edit that reintroduces cross-variant coercion;
//! - **independent of `Arc` identity**: an independently-allocated deep copy
//!   of a value compares equal to the original even though it shares no
//!   backing allocation — the same "no observable difference between shared
//!   and deep-copied values" property `law_cow_sharing.rs` proves for
//!   `Array`/`Map`/`Record`, generalized here to every heap-allocated
//!   variant (`List`, `Closure`, `Projection` too).
//!
//! ## The NaN exception (documented, not a bug)
//!
//! `value.rs`'s own doc comment on `impl PartialEq for Value` calls this
//! out directly: "NaN-bearing collections that are not the same snapshot
//! never compare equal ... a collection compared against itself (same
//! `Arc`) is equal even if it contains a NaN". `f32::NAN != f32::NAN` by
//! IEEE-754, and `Value::Float` carries no `Arc` wrapper to short-circuit
//! through — so a **bare, non-collection** `Value::Float(NaN)` (or one
//! reached without an intervening `Arc::ptr_eq` shortcut, i.e. a NaN inside
//! an independently-allocated deep copy) genuinely fails reflexivity. This
//! is expected float semantics, not a law violation, so the reflexive and
//! deep-copy laws both filter out any generated value containing a NaN
//! anywhere in its structure (`contains_nan`) rather than assert something
//! IEEE-754 makes false.
//!
//! Reproducibility (house determinism rule, `CLAUDE.md`): proptest's default
//! RNG is entropy-seeded per run, not fixed — generated cases differ run to
//! run. Reproducibility instead comes from `ProptestConfig::with_cases`
//! (a fixed, deterministic *count* of cases every run) and from proptest's
//! own failure-persistence file (`.proptest-regressions`), which pins the
//! exact seed of any failing case for replay. Set `PROPTEST_RNG_SEED` if
//! bit-for-bit seed reproducibility across every run — not just failures —
//! is ever required.

#![allow(clippy::unwrap_used, clippy::expect_used)]

mod law_support;

use std::mem::discriminant;
use std::sync::Arc;

use brink_format::{ClosureEnvEntry, ClosureValue, ListValue, OrderedMap, ProjSegment, Value};
use law_support::arb_value_full;
use proptest::prelude::*;

/// True if `v` contains an `f32::NAN` anywhere in its structure (recursing
/// through every collection/function/projection variant). Used to filter
/// generated cases out of the laws that assert something IEEE-754 makes
/// false for a bare NaN scalar — see the module doc's "NaN exception".
fn contains_nan(v: &Value) -> bool {
    match v {
        Value::Float(f) => f.is_nan(),
        Value::Array(items) => items.iter().any(contains_nan),
        Value::Map(map) => map.iter().any(|(_, val)| contains_nan(val)),
        Value::Record { fields, .. } => fields.iter().any(contains_nan),
        Value::Closure(c) => c.env.iter().any(|e| contains_nan(&e.payload)),
        Value::Projection(p) => p.segments.iter().any(|seg| match seg {
            ProjSegment::Index(_) => false,
            ProjSegment::Key(k) => contains_nan(k),
        }),
        Value::OptionVal(inner) => inner.as_deref().is_some_and(contains_nan),
        // NS-A7 weighted tables: a NaN anywhere in an entry value counts
        // (weights are ints, never NaN-able).
        Value::Weighted(w) => w.entries.iter().any(|(_, val)| contains_nan(val)),
        // NS-A8 tower values: a NaN lane anywhere counts (T4 — a
        // NaN-bearing vector is never equal to itself, like bare float).
        Value::Vec2(v) => v.is_nan(),
        Value::Vec3(v) => v.is_nan(),
        Value::Vec4(v) => v.is_nan(),
        Value::Quat(q) => q.is_nan(),
        Value::Mat2(m) => m.is_nan(),
        Value::Mat3(m) => m.is_nan(),
        Value::Mat4(m) => m.is_nan(),
        Value::Range { .. }
        | Value::Int(_)
        | Value::Bool(_)
        | Value::String(_)
        | Value::List(_)
        | Value::DivertTarget(_)
        | Value::VariablePointer(_)
        | Value::TempPointer { .. }
        | Value::Null
        | Value::FragmentRef(_)
        | Value::FnRef(_)
        | Value::Handle { .. } => false,
    }
}

/// Rebuild `v` from scratch through the public constructors, allocating a
/// fresh `Arc` at every heap-allocated level — mirrors `law_cow_sharing.rs`'s
/// `deep_copy_*` family but total over every `Value` variant instead of just
/// `Array`/`Map`/`Record`, matching this suite's broader "every variant"
/// scope (issue #746 item 3).
fn deep_copy(v: &Value) -> Value {
    match v {
        Value::Array(items) => Value::array(items.iter().map(deep_copy).collect()),
        Value::Map(map) => {
            let mut out = OrderedMap::with_capacity(map.len());
            for (key, val) in map.iter() {
                out.insert(key.clone(), deep_copy(val));
            }
            Value::map(out)
        }
        Value::Record { shape, fields } => {
            Value::record(*shape, fields.iter().map(deep_copy).collect())
        }
        Value::Closure(c) => {
            let ClosureValue { target, env } = c.as_ref();
            let env = env
                .iter()
                .map(|e| ClosureEnvEntry {
                    name: e.name,
                    is_ref: e.is_ref,
                    payload: deep_copy(&e.payload),
                })
                .collect();
            Value::closure(*target, env)
        }
        Value::Projection(p) => {
            let segments = p
                .segments
                .iter()
                .map(|seg| match seg {
                    ProjSegment::Index(n) => ProjSegment::Index(*n),
                    ProjSegment::Key(k) => ProjSegment::Key(deep_copy(k)),
                })
                .collect();
            Value::projection(p.cell, segments)
        }
        Value::List(lv) => Value::List(Arc::new(ListValue {
            items: lv.items.clone(),
            origins: lv.origins.clone(),
        })),
        // Scalars (including `Handle`, a `Copy`-cheap token with no `Arc`):
        // `.clone()` already yields an independent value, nothing to defeat.
        other => other.clone(),
    }
}

/// True if `a` and `b` are the "same" heap allocation for whichever
/// Arc-wrapped variant they happen to be (used only to sanity-check that
/// `deep_copy` really did allocate independently — if this were ever true
/// the deep-copy law below would pass vacuously).
fn shares_backing(a: &Value, b: &Value) -> bool {
    match (a, b) {
        (Value::Array(x), Value::Array(y))
        | (Value::Record { fields: x, .. }, Value::Record { fields: y, .. }) => Arc::ptr_eq(x, y),
        (Value::Map(x), Value::Map(y)) => Arc::ptr_eq(x, y),
        (Value::Closure(x), Value::Closure(y)) => Arc::ptr_eq(x, y),
        (Value::Projection(x), Value::Projection(y)) => Arc::ptr_eq(x, y),
        (Value::List(x), Value::List(y)) => Arc::ptr_eq(x, y),
        _ => false,
    }
}

proptest! {
    #![proptest_config(ProptestConfig::with_cases(512))]

    /// `v == v` for every generated value, except the documented bare-NaN
    /// exception (module doc).
    #[test]
    fn eq_is_reflexive(v in arb_value_full()) {
        prop_assume!(!contains_nan(&v));
        prop_assert!(v == v, "value not equal to itself: {v:?}");
    }

    /// `a == b` iff `b == a` — holds unconditionally, including for NaN
    /// (both directions read `false` the same way, so symmetry never
    /// breaks even where reflexivity does).
    #[test]
    fn eq_is_symmetric(a in arb_value_full(), b in arb_value_full()) {
        prop_assert_eq!(a == b, b == a);
    }

    /// Two values of different `Value` variants are never equal — pins the
    /// `impl PartialEq for Value`'s trailing `_ => false` catch-all.
    #[test]
    fn different_variant_never_equal(a in arb_value_full(), b in arb_value_full()) {
        prop_assume!(discriminant(&a) != discriminant(&b));
        prop_assert_ne!(a, b);
    }

    /// An independently-allocated deep copy compares equal to the original
    /// (sharing-unobservable, §3/§5), generalized to every `Value` variant —
    /// `law_cow_sharing.rs` proves the same convergence but only for
    /// `Array`/`Map`/`Record`.
    #[test]
    fn deep_copy_is_structurally_equal(v in arb_value_full()) {
        prop_assume!(!contains_nan(&v));
        let copy = deep_copy(&v);

        // Sanity: the copy really is independently allocated for every
        // Arc-wrapped variant (scalars have nothing to share, so this is
        // vacuously true for them) — if this ever failed the equality
        // assertion below would pass vacuously via the `ptr_eq` fast path
        // instead of proving the structural comparison.
        prop_assert!(!shares_backing(&v, &copy));
        prop_assert_eq!(&v, &copy);
    }
}