vj_sim/constraints/

ir.rs

//! The word-level constraint IR (plan section 1.2) and its direct evaluator.
//!
//! The IR is a small tree of 2-state bit-vector expressions. It is built once
//! per constraint block by `build` (from the bound sv-lang AST), consumed
//! structurally by the BDD bit-blaster, and *evaluated directly* by [`eval`]
//! here, which is the semantic oracle every solver gadget is checked against
//! (a bit-blasted BDD must agree with [`eval`] on every assignment).
//!
//! # Semantics (deliberately NOT codegen's 4-state semantics)
//!
//! LRM 18.3: constraints are 2-state only. There is no X/Z lane, no
//! "any-unknown-propagates" rule: arithmetic is plain two's-complement
//! modulo `2^width`. The one place a 4-state value can reach the IR is a
//! state-variable read; a state value with an X/Z bit is the typed
//! evaluation error [`ConstraintEvalError::StateUnknown`] (decision E9), never
//! a silent 0.
//!
//! # Typing
//!
//! Every node carries its result [`Ty`] (width and signedness), so [`Expr::ty`]
//! is O(1). The builder derives the types from sv-lang, whose context-
//! determined-width rule (LRM 11.6) has already inserted the `Conversion`
//! nodes that equalise operand types; [`Expr::validate`] re-checks the same
//! rules so an ill-typed tree is a loud [`IrError`] at build time rather than
//! a wrong answer at solve time. Operand rules:
//!
//! - `Add Sub Mul Div Mod And Or Xor Xnor`: both operands and the result share
//!   one type.
//! - `Shl Shr Ashr`: the result has the left operand's type; the shift
//!   amount may be any width and is always read unsigned (LRM 11.4.10).
//! - `Eq Ne Lt Le Gt Ge`: both operands share one type (signedness selects
//!   signed vs unsigned ordering); the result is one unsigned bit.
//! - `LogAnd LogOr LogImpl LogEquiv`, `LogNot`, reductions: operands of any
//!   type (truthiness = "nonzero"), one unsigned result bit.
//! - `AllDistinct`: every member shares one type; one unsigned result bit.

use core::fmt;
use num_bigint::{BigInt, BigUint};
use num_traits::{One, Zero};

/// Index of a random (solved) variable.
pub type VarId = u32;
/// Index of a state variable (a value fixed before the solve).
pub type StateId = u32;

/// A bit-vector type: `width >= 1` bits, interpreted signed or unsigned.
#[derive(Clone, Copy, Debug, PartialEq, Eq, Hash, serde::Serialize, serde::Deserialize)]
pub struct Ty {
    /// Number of bits, at least 1.
    pub width: u32,
    /// Two's-complement signed when set.
    pub signed: bool,
}

impl Ty {
    /// An unsigned type of `width` bits.
    pub const fn unsigned(width: u32) -> Ty {
        Ty {
            width,
            signed: false,
        }
    }
    /// A signed type of `width` bits.
    pub const fn signed(width: u32) -> Ty {
        Ty {
            width,
            signed: true,
        }
    }
    /// The one-bit unsigned type every boolean-valued node produces.
    pub const BIT: Ty = Ty::unsigned(1);
}

impl fmt::Display for Ty {
    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
        write!(f, "{}[{}]", if self.signed { "s" } else { "u" }, self.width)
    }
}

/// Unary operators.
#[derive(Clone, Copy, Debug, PartialEq, Eq, Hash, serde::Serialize, serde::Deserialize)]
pub enum UnOp {
    /// Bitwise `~`. Result type = operand type.
    BitNot,
    /// Arithmetic negation `-`. Result type = operand type.
    Neg,
    /// Logical `!`. One-bit result.
    LogNot,
    /// Reduction `&`. One-bit result.
    RedAnd,
    /// Reduction `|`. One-bit result.
    RedOr,
    /// Reduction `^`. One-bit result.
    RedXor,
    /// Reduction `~&`. One-bit result.
    RedNand,
    /// Reduction `~|`. One-bit result.
    RedNor,
    /// Reduction `~^`. One-bit result.
    RedXnor,
}

/// Binary operators.
#[derive(Clone, Copy, Debug, PartialEq, Eq, Hash, serde::Serialize, serde::Deserialize)]
pub enum BinOp {
    /// `+`.
    Add,
    /// `-`.
    Sub,
    /// `*`.
    Mul,
    /// `/` (truncating; signed when the operand type is).
    Div,
    /// `%` (sign of the dividend; signed when the operand type is).
    Mod,
    /// Bitwise `&`.
    And,
    /// Bitwise `|`.
    Or,
    /// Bitwise `^`.
    Xor,
    /// Bitwise `~^` / `^~`.
    Xnor,
    /// `<<` and `<<<` (identical).
    Shl,
    /// `>>` (logical).
    Shr,
    /// `>>>` (sign-filling when the left operand is signed).
    Ashr,
    /// `==`.
    Eq,
    /// `!=`.
    Ne,
    /// `<`.
    Lt,
    /// `<=`.
    Le,
    /// `>`.
    Gt,
    /// `>=`.
    Ge,
    /// `&&`.
    LogAnd,
    /// `||`.
    LogOr,
    /// `->` (logical implication: `!a || b`).
    LogImpl,
    /// `<->` (logical equivalence).
    LogEquiv,
}

impl BinOp {
    fn is_compare(self) -> bool {
        matches!(
            self,
            BinOp::Eq | BinOp::Ne | BinOp::Lt | BinOp::Le | BinOp::Gt | BinOp::Ge
        )
    }
    fn is_logical(self) -> bool {
        matches!(
            self,
            BinOp::LogAnd | BinOp::LogOr | BinOp::LogImpl | BinOp::LogEquiv
        )
    }
    fn is_shift(self) -> bool {
        matches!(self, BinOp::Shl | BinOp::Shr | BinOp::Ashr)
    }
}

/// A word-level 2-state expression.
#[derive(Clone, Debug, PartialEq, Eq, Hash, serde::Serialize, serde::Deserialize)]
pub enum Expr {
    /// A constant; the value is below `2^width`.
    Const(Ty, BigUint),
    /// A random variable being solved for.
    Var(VarId, Ty),
    /// A state variable: a value fixed before the solve.
    State(StateId, Ty),
    /// A unary operation; the [`Ty`] is the result type.
    Unary(UnOp, Box<Expr>, Ty),
    /// A binary operation; the [`Ty`] is the result type.
    Binary(BinOp, Box<Expr>, Box<Expr>, Ty),
    /// `cond ? t : f` where `cond` is read as its truthiness.
    Ite(Box<Expr>, Box<Expr>, Box<Expr>, Ty),
    /// A constraint-level `if (pred) then else else_` or `pred -> then`
    /// (LRM 18.5.5, 18.5.6): the same value as [`Expr::Ite`] on `pred`, but
    /// marked so [`super::guard::resolve`] can treat `pred` as a *constraint
    /// guard* (LRM 18.5.12) before the solve. An expression-level `->` or
    /// `?:` is never a guard and keeps its own node. Evaluated and
    /// bit-blasted exactly like `Ite`, so a tree that still holds one (a
    /// builder test, a guard whose value is `RANDOM`) means what it says.
    Guard(Box<Expr>, Box<Expr>, Box<Expr>, Ty),
    /// Width/sign change: truncates, or extends using the *operand's*
    /// signedness (LRM 11.8.2), then relabels with the result signedness.
    Resize(Box<Expr>, Ty),
    /// Concatenation, first element most significant. Always unsigned.
    Concat(Vec<Expr>, Ty),
    /// The constant window `[lo + width - 1 : lo]` of the operand
    /// (physical bit positions, bit 0 least significant). Always unsigned.
    Slice(Box<Expr>, u32, Ty),
    /// `unique { m0, m1, ... }` (LRM 18.5.4): true iff no two members hold
    /// the same value. Always `u[1]`. The members are random or state
    /// variables of one type (checked by [`Expr::validate`]); a group of
    /// fewer than two members is never built (the LRM makes it a no-op), but a
    /// tree that holds one is simply true.
    AllDistinct(Vec<Expr>),
    /// An array-level node (LRM 18.4, 18.5.7): an array's size or element, a
    /// `foreach` loop or an array reduction, and (LRM 18.5.11) a function
    /// call, which is not about arrays but is resolved at the same point and
    /// by the same rule. These exist only between the
    /// builder and the run-time expansion (`super::array::expand`), which
    /// replaces every one with plain scalar IR once the array sizes are known;
    /// [`eval`] and the bit-blaster reject a tree that still holds one with
    /// [`ConstraintEvalError::Unexpanded`].
    Array(ArrayNode),
}

/// Index of an array in a program's array table.
pub type ArrayId = u32;
/// Identity of one `foreach` loop variable or reduction `item` binding.
pub type LoopId = u32;

/// An array reduction method (LRM 7.12.3).
#[derive(Clone, Copy, Debug, PartialEq, Eq, Hash, serde::Serialize, serde::Deserialize)]
pub enum ReduceOp {
    /// `sum()`: identity 0.
    Sum,
    /// `product()`: identity 1.
    Product,
    /// `and()`: identity all ones.
    And,
    /// `or()`: identity 0.
    Or,
    /// `xor()`: identity 0.
    Xor,
}

/// The array-level IR nodes (see [`Expr::Array`]).
#[derive(Clone, Debug, PartialEq, Eq, Hash, serde::Serialize, serde::Deserialize)]
pub enum ArrayNode {
    /// `A.size()`: the array's length, `s[32]`.
    Size(ArrayId),
    /// `A[index]` (LRM 18.5.7.1). After loop-variable substitution the index
    /// must be free of random variables (the builder rejects the rest).
    Elem {
        /// The indexed array.
        array: ArrayId,
        /// The index expression.
        index: Box<Expr>,
        /// The element type.
        ty: Ty,
    },
    /// The current value of a `foreach` loop variable or reduction iterator.
    Loop(LoopId, Ty),
    /// `foreach (A[i]) body`: `body` holds for every index `i` of `A`. One
    /// bit. The body reads the index as `Loop(var, s[32])`.
    Foreach {
        /// The iterated array.
        array: ArrayId,
        /// The loop variable.
        var: LoopId,
        /// The constraint body (a boolean expression).
        body: Box<Expr>,
    },
    /// `A.op() with (body)`: the reduction of `body` over every element,
    /// read as `Loop(var, elem_ty)` for the item and `Loop(idx, s[32])` for
    /// `item.index`. The body's type is the result type.
    Reduce {
        /// The reduction.
        op: ReduceOp,
        /// The reduced array.
        array: ArrayId,
        /// The `item` binding.
        var: LoopId,
        /// The `item.index` binding.
        index_var: LoopId,
        /// The per-element expression (the item itself without a `with`).
        body: Box<Expr>,
    },
    /// A call of a user function (LRM 18.5.11), `func` indexing the program's
    /// function table ([`super::func`]). Like the nodes above it is resolved
    /// before the solver sees the tree: once its arguments are constants the
    /// call is evaluated and replaced by the constant it returns (the return
    /// value is a state variable of the constraint that holds it).
    Call {
        /// The called function.
        func: FuncId,
        /// The actual arguments, one per formal, already converted to the
        /// formal's type.
        args: Vec<Expr>,
        /// The return type.
        ty: Ty,
    },
    /// `A[index]` over a fixed-size unpacked array held in a class property
    /// (LRM 7.4, 18.4): every element is its own variable or state, and the
    /// element read is the one the index names. The index is a constant, a state
    /// or a loop variable, so it is known once the node is expanded; only the
    /// chosen element is expanded, so an index outside the array is an error
    /// only when this node is live (LRM 18.5.7.1: the user excludes such indices
    /// with a guard).
    Pick {
        /// The index expression.
        index: Box<Expr>,
        /// The array's lowest declared index: `elems[i - low]` is element `i`.
        low: i64,
        /// The elements, lowest declared index first; all of type `ty`.
        elems: Vec<Expr>,
        /// The element type.
        ty: Ty,
    },
    /// `unique { m0, m1, ... }` (LRM 18.5.4) whose group holds a whole
    /// dynamic array or queue, whose length is known only at run time: true
    /// iff no two of the `scalars` and of every element of every array in
    /// `arrays` hold the same value. One bit. Expansion replaces it with the
    /// [`Expr::AllDistinct`] over the scalars followed by each array's
    /// elements (a group of fewer than two members is simply true).
    Distinct {
        /// The singular members (variables or states of the element type).
        scalars: Vec<Expr>,
        /// The dynamic arrays or queues whose every element is a member.
        arrays: Vec<ArrayId>,
    },
    /// `body` read with the row array `template` standing for row `row` of the
    /// array of arrays that `template` is the row template of (LRM 18.4, 7.4.5:
    /// `a[i].size`, `a[i][j]`, `a[i].sum()` over `rand int a[][]`). The row
    /// arrays of an array of dynamic arrays or queues are not known when the
    /// constraints are built (the outer size is solved first, then every row
    /// gets its own size and elements), so `body` is ordinary one-dimensional
    /// array IR over `template`, and expansion rebinds `template` to the
    /// concrete row array of the row `row` names once the outer size is fixed
    /// ([`super::array::lower_rows`]). `row` is free of random variables, like
    /// an element index.
    RowScope {
        /// The row template: a program array that only stands for "the row".
        template: ArrayId,
        /// The row index (an index into the outer array).
        row: Box<Expr>,
        /// The expression over `template`.
        body: Box<Expr>,
    },
}

/// Index of a function in a program's function table.
pub type FuncId = u32;

/// A malformed IR tree (a builder bug or an out-of-contract construction).
#[derive(Clone, Debug, PartialEq, Eq)]
pub enum IrError {
    /// A node violates its operand/result typing rule.
    IllTyped {
        /// Which node and rule.
        what: String,
    },
}

impl fmt::Display for IrError {
    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
        match self {
            IrError::IllTyped { what } => write!(f, "ill-typed constraint IR: {what}"),
        }
    }
}

impl std::error::Error for IrError {}

/// A failure while evaluating an [`Expr`] directly.
#[derive(Clone, Debug, PartialEq, Eq)]
pub enum ConstraintEvalError {
    /// The state variable had an X/Z bit (LRM 18.3: 4-state values in a
    /// constraint are an error; decision E9).
    StateUnknown(StateId),
    /// `/` or `%` with a zero divisor.
    DivideByZero,
    /// The assignment has no value for this random variable.
    UnboundVar(VarId),
    /// The assignment has no entry for this state variable.
    UnboundState(StateId),
    /// The tree still holds an array-level node ([`Expr::Array`]); the
    /// run-time expansion must replace it before evaluation.
    Unexpanded,
}

impl fmt::Display for ConstraintEvalError {
    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
        match self {
            ConstraintEvalError::StateUnknown(s) => write!(
                f,
                "state variable #{s} has an X/Z bit; a 4-state value in a constraint is an \
                 error (IEEE 1800-2023 18.3)"
            ),
            ConstraintEvalError::DivideByZero => f.write_str("division by zero in a constraint"),
            ConstraintEvalError::UnboundVar(v) => write!(f, "no value for random variable #{v}"),
            ConstraintEvalError::UnboundState(s) => {
                write!(f, "no value for state variable #{s}")
            }
            ConstraintEvalError::Unexpanded => {
                f.write_str("an array-level constraint node was not expanded before evaluation")
            }
        }
    }
}

impl std::error::Error for ConstraintEvalError {}

/// Concrete values for [`eval`]. A `None` state entry means the state
/// variable currently holds an X/Z bit.
#[derive(Clone, Debug, Default, PartialEq, Eq)]
pub struct Assignment {
    /// Random-variable values, indexed by [`VarId`] (each below `2^width`).
    pub vars: Vec<BigUint>,
    /// State-variable values, indexed by [`StateId`]; `None` = has X/Z.
    pub states: Vec<Option<BigUint>>,
}

/// `2^w - 1`.
pub fn mask(w: u32) -> BigUint {
    (BigUint::one() << w) - BigUint::one()
}

fn to_signed(v: &BigUint, w: u32) -> BigInt {
    if v.bit(u64::from(w) - 1) {
        BigInt::from(v.clone()) - (BigInt::one() << w)
    } else {
        BigInt::from(v.clone())
    }
}

fn from_signed(i: &BigInt, w: u32) -> BigUint {
    let m = BigInt::one() << w;
    let r = ((i % &m) + &m) % &m;
    r.to_biguint().expect("reduced into [0, 2^w)")
}

fn bit(b: bool) -> BigUint {
    if b { BigUint::one() } else { BigUint::zero() }
}

impl Expr {
    /// A constant of type `ty` holding `val` truncated to the width.
    pub fn constant(ty: Ty, val: impl Into<BigUint>) -> Expr {
        Expr::Const(ty, val.into() & mask(ty.width))
    }

    /// The result type of this node.
    pub fn ty(&self) -> Ty {
        match self {
            Expr::Const(t, _)
            | Expr::Var(_, t)
            | Expr::State(_, t)
            | Expr::Unary(_, _, t)
            | Expr::Binary(_, _, _, t)
            | Expr::Ite(_, _, _, t)
            | Expr::Guard(_, _, _, t)
            | Expr::Resize(_, t)
            | Expr::Concat(_, t)
            | Expr::Slice(_, _, t) => *t,
            Expr::AllDistinct(_) => Ty::BIT,
            Expr::Array(n) => n.ty(),
        }
    }

    /// Checks every node against its typing rule (module docs).
    pub fn validate(&self) -> Result<(), IrError> {
        let bad = |what: String| Err(IrError::IllTyped { what });
        match self {
            Expr::Const(t, v) => {
                if t.width == 0 {
                    return bad("zero-width constant".into());
                }
                if v.bits() > u64::from(t.width) {
                    return bad(format!("constant {v} does not fit {t}"));
                }
                Ok(())
            }
            Expr::Var(_, t) | Expr::State(_, t) => {
                if t.width == 0 {
                    return bad("zero-width variable".into());
                }
                Ok(())
            }
            Expr::Unary(op, a, t) => {
                a.validate()?;
                let at = a.ty();
                let want = match op {
                    UnOp::BitNot | UnOp::Neg => at,
                    _ => Ty::BIT,
                };
                if *t != want {
                    return bad(format!("{op:?} on {at} must produce {want}, has {t}"));
                }
                Ok(())
            }
            Expr::Binary(op, l, r, t) => {
                l.validate()?;
                r.validate()?;
                let (lt, rt) = (l.ty(), r.ty());
                if op.is_logical() {
                    if *t != Ty::BIT {
                        return bad(format!("{op:?} must produce u[1], has {t}"));
                    }
                } else if op.is_compare() {
                    if lt != rt {
                        return bad(format!("{op:?} operands differ: {lt} vs {rt}"));
                    }
                    if *t != Ty::BIT {
                        return bad(format!("{op:?} must produce u[1], has {t}"));
                    }
                } else if op.is_shift() {
                    if *t != lt {
                        return bad(format!("{op:?} result {t} must equal left operand {lt}"));
                    }
                } else if lt != rt || *t != lt {
                    return bad(format!("{op:?} operands/result differ: {lt}, {rt}, {t}"));
                }
                Ok(())
            }
            Expr::Ite(c, a, b, t) | Expr::Guard(c, a, b, t) => {
                c.validate()?;
                a.validate()?;
                b.validate()?;
                if a.ty() != *t || b.ty() != *t {
                    return bad(format!(
                        "ternary arms {} / {} must both equal result {t}",
                        a.ty(),
                        b.ty()
                    ));
                }
                Ok(())
            }
            Expr::Resize(a, t) => {
                a.validate()?;
                if t.width == 0 {
                    return bad("resize to zero width".into());
                }
                Ok(())
            }
            Expr::Concat(parts, t) => {
                if parts.is_empty() {
                    return bad("empty concatenation".into());
                }
                let mut w = 0u32;
                for p in parts {
                    p.validate()?;
                    w += p.ty().width;
                }
                if *t != Ty::unsigned(w) {
                    return bad(format!("concatenation of {w} bits has type {t}"));
                }
                Ok(())
            }
            Expr::Slice(a, lo, t) => {
                a.validate()?;
                if t.signed || t.width == 0 || lo + t.width > a.ty().width {
                    return bad(format!(
                        "slice [{}+:{}] of {} (result {t})",
                        lo,
                        t.width,
                        a.ty()
                    ));
                }
                Ok(())
            }
            Expr::AllDistinct(members) => {
                let Some(first) = members.first() else {
                    return bad("empty uniqueness group".into());
                };
                let t = first.ty();
                for m in members {
                    m.validate()?;
                    if m.ty() != t {
                        return bad(format!(
                            "uniqueness members differ in type: {t} vs {}",
                            m.ty()
                        ));
                    }
                }
                Ok(())
            }
            Expr::Array(n) => n.validate(),
        }
    }

    /// Calls `f` on every random variable this expression reads.
    pub fn for_each_var(&self, f: &mut impl FnMut(VarId, Ty)) {
        match self {
            Expr::Var(v, t) => f(*v, *t),
            Expr::Const(..) | Expr::State(..) => {}
            Expr::Unary(_, a, _) | Expr::Resize(a, _) | Expr::Slice(a, _, _) => {
                a.for_each_var(f);
            }
            Expr::Binary(_, a, b, _) => {
                a.for_each_var(f);
                b.for_each_var(f);
            }
            Expr::Ite(c, a, b, _) | Expr::Guard(c, a, b, _) => {
                c.for_each_var(f);
                a.for_each_var(f);
                b.for_each_var(f);
            }
            Expr::Concat(parts, _) | Expr::AllDistinct(parts) => {
                parts.iter().for_each(|p| p.for_each_var(f));
            }
            Expr::Array(n) => n.for_each_child(&mut |c| c.for_each_var(f)),
        }
    }

    /// Calls `f` on every state variable this expression reads.
    pub fn for_each_state(&self, f: &mut impl FnMut(StateId)) {
        match self {
            Expr::State(s, _) => f(*s),
            Expr::Const(..) | Expr::Var(..) => {}
            Expr::Unary(_, a, _) | Expr::Resize(a, _) | Expr::Slice(a, _, _) => {
                a.for_each_state(f);
            }
            Expr::Binary(_, a, b, _) => {
                a.for_each_state(f);
                b.for_each_state(f);
            }
            Expr::Ite(c, a, b, _) | Expr::Guard(c, a, b, _) => {
                c.for_each_state(f);
                a.for_each_state(f);
                b.for_each_state(f);
            }
            Expr::Concat(parts, _) | Expr::AllDistinct(parts) => {
                parts.iter().for_each(|p| p.for_each_state(f));
            }
            Expr::Array(n) => n.for_each_child(&mut |c| c.for_each_state(f)),
        }
    }

    /// A copy of this expression with every random-variable read replaced by
    /// `f(id, ty)`. The replacement must have type `ty` (the caller's
    /// contract: a renumbered [`Expr::Var`] or a same-typed constant); the
    /// debug assertion pins that so a mis-typed substitution fails loudly
    /// instead of producing an ill-typed tree.
    ///
    /// This is how `rand_mode(0)` variables are turned into state before a
    /// solve (LRM 18.8: an inactive random variable "is treated the same as
    /// any other state variable"), and how the surviving active variables are
    /// renumbered densely.
    pub fn substitute_vars(&self, f: &mut impl FnMut(VarId, Ty) -> Expr) -> Expr {
        match self {
            Expr::Var(v, t) => {
                let r = f(*v, *t);
                debug_assert_eq!(r.ty(), *t, "substitute_vars: replacement type differs");
                r
            }
            Expr::Const(..) | Expr::State(..) => self.clone(),
            Expr::Unary(op, a, t) => Expr::Unary(*op, Box::new(a.substitute_vars(f)), *t),
            Expr::Resize(a, t) => Expr::Resize(Box::new(a.substitute_vars(f)), *t),
            Expr::Slice(a, lo, t) => Expr::Slice(Box::new(a.substitute_vars(f)), *lo, *t),
            Expr::Binary(op, a, b, t) => {
                let a = Box::new(a.substitute_vars(f));
                let b = Box::new(b.substitute_vars(f));
                Expr::Binary(*op, a, b, *t)
            }
            Expr::Ite(c, a, b, t) => {
                let c = Box::new(c.substitute_vars(f));
                let a = Box::new(a.substitute_vars(f));
                let b = Box::new(b.substitute_vars(f));
                Expr::Ite(c, a, b, *t)
            }
            Expr::Guard(c, a, b, t) => {
                let c = Box::new(c.substitute_vars(f));
                let a = Box::new(a.substitute_vars(f));
                let b = Box::new(b.substitute_vars(f));
                Expr::Guard(c, a, b, *t)
            }
            Expr::Concat(parts, t) => {
                Expr::Concat(parts.iter().map(|p| p.substitute_vars(f)).collect(), *t)
            }
            Expr::AllDistinct(parts) => {
                Expr::AllDistinct(parts.iter().map(|p| p.substitute_vars(f)).collect())
            }
            Expr::Array(n) => Expr::Array(n.map_children(&mut |c| c.substitute_vars(f))),
        }
    }
}

impl Expr {
    /// A copy of this expression with every direct sub-expression replaced by
    /// `f(child)` (the first error wins). Leaves are copied unchanged.
    pub fn try_map_children<E>(
        &self,
        f: &mut impl FnMut(&Expr) -> Result<Expr, E>,
    ) -> Result<Expr, E> {
        Ok(match self {
            Expr::Const(..) | Expr::Var(..) | Expr::State(..) => self.clone(),
            Expr::Unary(op, a, t) => Expr::Unary(*op, Box::new(f(a)?), *t),
            Expr::Binary(op, a, b, t) => Expr::Binary(*op, Box::new(f(a)?), Box::new(f(b)?), *t),
            Expr::Ite(c, a, b, t) => {
                Expr::Ite(Box::new(f(c)?), Box::new(f(a)?), Box::new(f(b)?), *t)
            }
            Expr::Guard(c, a, b, t) => {
                Expr::Guard(Box::new(f(c)?), Box::new(f(a)?), Box::new(f(b)?), *t)
            }
            Expr::Resize(a, t) => Expr::Resize(Box::new(f(a)?), *t),
            Expr::Concat(parts, t) => {
                Expr::Concat(parts.iter().map(&mut *f).collect::<Result<_, _>>()?, *t)
            }
            Expr::Slice(a, lo, t) => Expr::Slice(Box::new(f(a)?), *lo, *t),
            Expr::AllDistinct(parts) => {
                Expr::AllDistinct(parts.iter().map(&mut *f).collect::<Result<_, _>>()?)
            }
            Expr::Array(n) => {
                let mut err = None;
                let r = n.map_children(&mut |c| match f(c) {
                    Ok(x) => x,
                    Err(e) => {
                        err.get_or_insert(e);
                        c.clone()
                    }
                });
                if let Some(e) = err {
                    return Err(e);
                }
                Expr::Array(r)
            }
        })
    }

    /// Whether any node of this expression satisfies `pred`.
    pub fn any_node(&self, pred: &mut impl FnMut(&Expr) -> bool) -> bool {
        if pred(self) {
            return true;
        }
        let mut found = false;
        let mut visit = |c: &Expr| {
            if !found && c.any_node(pred) {
                found = true;
            }
        };
        match self {
            Expr::Const(..) | Expr::Var(..) | Expr::State(..) => {}
            Expr::Unary(_, a, _) | Expr::Resize(a, _) | Expr::Slice(a, _, _) => visit(a),
            Expr::Binary(_, a, b, _) => {
                visit(a);
                visit(b);
            }
            Expr::Ite(c, a, b, _) | Expr::Guard(c, a, b, _) => {
                visit(c);
                visit(a);
                visit(b);
            }
            Expr::Concat(parts, _) | Expr::AllDistinct(parts) => parts.iter().for_each(visit),
            Expr::Array(n) => n.for_each_child(&mut visit),
        }
        found
    }
}

impl ArrayNode {
    /// The result type of this node.
    pub fn ty(&self) -> Ty {
        match self {
            ArrayNode::Size(_) => Ty::signed(32),
            ArrayNode::Elem { ty, .. } | ArrayNode::Loop(_, ty) => *ty,
            ArrayNode::Foreach { .. } | ArrayNode::Distinct { .. } => Ty::BIT,
            ArrayNode::Reduce { body, .. } | ArrayNode::RowScope { body, .. } => body.ty(),
            ArrayNode::Call { ty, .. } | ArrayNode::Pick { ty, .. } => *ty,
        }
    }

    fn validate(&self) -> Result<(), IrError> {
        let bad = |what: String| Err(IrError::IllTyped { what });
        match self {
            ArrayNode::Size(_) => Ok(()),
            ArrayNode::Loop(_, t) => {
                if t.width == 0 {
                    return bad("zero-width loop variable".into());
                }
                Ok(())
            }
            ArrayNode::Elem { index, ty, .. } => {
                index.validate()?;
                if ty.width == 0 {
                    return bad("zero-width array element".into());
                }
                Ok(())
            }
            ArrayNode::Foreach { body, .. } => body.validate(),
            ArrayNode::RowScope { row, body, .. } => {
                row.validate()?;
                body.validate()
            }
            ArrayNode::Distinct { scalars, arrays } => {
                if scalars.is_empty() && arrays.is_empty() {
                    return bad("a distinct group with no members".into());
                }
                scalars.iter().try_for_each(Expr::validate)
            }
            ArrayNode::Reduce { op, body, .. } => {
                body.validate()?;
                if matches!(op, ReduceOp::And | ReduceOp::Or | ReduceOp::Xor)
                    && body.ty().width == 0
                {
                    return bad("zero-width reduction".into());
                }
                Ok(())
            }
            ArrayNode::Call { args, ty, .. } => {
                if ty.width == 0 {
                    return bad("zero-width function result".into());
                }
                args.iter().try_for_each(Expr::validate)
            }
            ArrayNode::Pick {
                index, elems, ty, ..
            } => {
                index.validate()?;
                if ty.width == 0 {
                    return bad("zero-width array element".into());
                }
                if elems.is_empty() {
                    return bad("a pick over no elements".into());
                }
                if elems.iter().any(|e| e.ty() != *ty) {
                    return bad("a pick element of another type".into());
                }
                elems.iter().try_for_each(Expr::validate)
            }
        }
    }

    /// Calls `f` on every direct sub-expression.
    pub fn for_each_child(&self, f: &mut impl FnMut(&Expr)) {
        match self {
            ArrayNode::Size(_) | ArrayNode::Loop(..) => {}
            ArrayNode::Pick { index, elems, .. } => {
                f(index);
                elems.iter().for_each(f);
            }
            ArrayNode::Call { args, .. } => args.iter().for_each(f),
            ArrayNode::Distinct { scalars, .. } => scalars.iter().for_each(f),
            ArrayNode::Elem { index, .. } => f(index),
            ArrayNode::Foreach { body, .. } | ArrayNode::Reduce { body, .. } => f(body),
            ArrayNode::RowScope { row, body, .. } => {
                f(row);
                f(body);
            }
        }
    }

    /// A copy with every direct sub-expression replaced by `f(child)`.
    pub fn map_children(&self, f: &mut impl FnMut(&Expr) -> Expr) -> ArrayNode {
        match self {
            ArrayNode::Size(_) | ArrayNode::Loop(..) => self.clone(),
            ArrayNode::Pick {
                index,
                low,
                elems,
                ty,
            } => ArrayNode::Pick {
                index: Box::new(f(index)),
                low: *low,
                elems: elems.iter().map(&mut *f).collect(),
                ty: *ty,
            },
            ArrayNode::Call { func, args, ty } => ArrayNode::Call {
                func: *func,
                args: args.iter().map(&mut *f).collect(),
                ty: *ty,
            },
            ArrayNode::Distinct { scalars, arrays } => ArrayNode::Distinct {
                scalars: scalars.iter().map(&mut *f).collect(),
                arrays: arrays.clone(),
            },
            ArrayNode::Elem { array, index, ty } => ArrayNode::Elem {
                array: *array,
                index: Box::new(f(index)),
                ty: *ty,
            },
            ArrayNode::Foreach { array, var, body } => ArrayNode::Foreach {
                array: *array,
                var: *var,
                body: Box::new(f(body)),
            },
            ArrayNode::RowScope {
                template,
                row,
                body,
            } => ArrayNode::RowScope {
                template: *template,
                row: Box::new(f(row)),
                body: Box::new(f(body)),
            },
            ArrayNode::Reduce {
                op,
                array,
                var,
                index_var,
                body,
            } => ArrayNode::Reduce {
                op: *op,
                array: *array,
                var: *var,
                index_var: *index_var,
                body: Box::new(f(body)),
            },
        }
    }
}

/// Directly evaluates `e` under `a`; the result is below `2^e.ty().width`.
pub fn eval(e: &Expr, a: &Assignment) -> Result<BigUint, ConstraintEvalError> {
    match e {
        Expr::Const(_, v) => Ok(v.clone()),
        Expr::Var(id, t) => a
            .vars
            .get(*id as usize)
            .map(|v| v & mask(t.width))
            .ok_or(ConstraintEvalError::UnboundVar(*id)),
        Expr::State(id, t) => match a.states.get(*id as usize) {
            None => Err(ConstraintEvalError::UnboundState(*id)),
            Some(None) => Err(ConstraintEvalError::StateUnknown(*id)),
            Some(Some(v)) => Ok(v & mask(t.width)),
        },
        Expr::Unary(op, x, t) => {
            let v = eval(x, a)?;
            let w = x.ty().width;
            let r = match op {
                UnOp::BitNot => mask(w) ^ v,
                UnOp::Neg => ((BigUint::one() << w) - v) & mask(w),
                UnOp::LogNot => bit(v.is_zero()),
                UnOp::RedAnd => bit(v == mask(w)),
                UnOp::RedNand => bit(v != mask(w)),
                UnOp::RedOr => bit(!v.is_zero()),
                UnOp::RedNor => bit(v.is_zero()),
                UnOp::RedXor => bit(popcount(&v) % 2 == 1),
                UnOp::RedXnor => bit(popcount(&v).is_multiple_of(2)),
            };
            Ok(r & mask(t.width))
        }
        Expr::Binary(op @ (BinOp::LogAnd | BinOp::LogOr | BinOp::LogImpl), l, r, _) => {
            // `&&`, `||` and `->` short-circuit (LRM 11.4.7/11.4.8): the right
            // operand is only evaluated when the left does not decide the
            // result, so a division by zero in a decided-away arm is not an
            // error. The bit-blaster's definedness gating mirrors this.
            let l_true = !eval(l, a)?.is_zero();
            let decided = match op {
                BinOp::LogAnd | BinOp::LogImpl => !l_true,
                _ => l_true,
            };
            if decided {
                return Ok(bit(*op != BinOp::LogAnd));
            }
            Ok(bit(!eval(r, a)?.is_zero()))
        }
        Expr::Binary(op, l, r, t) => {
            let lv = eval(l, a)?;
            let rv = eval(r, a)?;
            let lt = l.ty();
            let w = t.width;
            let m = mask(w);
            Ok(match op {
                BinOp::Add => (lv + rv) & m,
                BinOp::Sub => ((BigUint::one() << w) + lv - rv) & m,
                BinOp::Mul => (lv * rv) & m,
                BinOp::Div | BinOp::Mod => {
                    if rv.is_zero() {
                        return Err(ConstraintEvalError::DivideByZero);
                    }
                    if lt.signed {
                        let (x, y) = (to_signed(&lv, w), to_signed(&rv, w));
                        from_signed(&if *op == BinOp::Div { x / y } else { x % y }, w)
                    } else if *op == BinOp::Div {
                        lv / rv
                    } else {
                        lv % rv
                    }
                }
                BinOp::And => lv & rv,
                BinOp::Or => lv | rv,
                BinOp::Xor => lv ^ rv,
                BinOp::Xnor => (lv ^ rv) ^ m,
                BinOp::Shl | BinOp::Shr | BinOp::Ashr => {
                    // The amount is unsigned; at or past the width it
                    // shifts everything out (or fills with the sign).
                    let amt = if rv < BigUint::from(w) {
                        u32::try_from(&rv).expect("below w")
                    } else {
                        w
                    };
                    match op {
                        BinOp::Shl => (lv << amt) & m,
                        BinOp::Shr => lv >> amt,
                        _ => {
                            if lt.signed && lv.bit(u64::from(w) - 1) {
                                let x = to_signed(&lv, w) >> amt;
                                from_signed(&x, w)
                            } else {
                                lv >> amt
                            }
                        }
                    }
                }
                BinOp::Eq => bit(lv == rv),
                BinOp::Ne => bit(lv != rv),
                BinOp::Lt | BinOp::Le | BinOp::Gt | BinOp::Ge => {
                    let ord = if lt.signed {
                        to_signed(&lv, lt.width).cmp(&to_signed(&rv, lt.width))
                    } else {
                        lv.cmp(&rv)
                    };
                    bit(match op {
                        BinOp::Lt => ord.is_lt(),
                        BinOp::Le => ord.is_le(),
                        BinOp::Gt => ord.is_gt(),
                        _ => ord.is_ge(),
                    })
                }
                BinOp::LogAnd => bit(!lv.is_zero() && !rv.is_zero()),
                BinOp::LogOr => bit(!lv.is_zero() || !rv.is_zero()),
                BinOp::LogImpl => bit(lv.is_zero() || !rv.is_zero()),
                BinOp::LogEquiv => bit(lv.is_zero() == rv.is_zero()),
            })
        }
        Expr::Ite(c, x, y, _) | Expr::Guard(c, x, y, _) => {
            if eval(c, a)?.is_zero() {
                eval(y, a)
            } else {
                eval(x, a)
            }
        }
        Expr::Resize(x, t) => {
            let v = eval(x, a)?;
            let from = x.ty();
            Ok(if t.width <= from.width {
                v & mask(t.width)
            } else if from.signed {
                from_signed(&to_signed(&v, from.width), t.width)
            } else {
                v
            })
        }
        Expr::Concat(parts, _) => {
            let mut acc = BigUint::zero();
            for p in parts {
                let v = eval(p, a)?;
                acc = (acc << p.ty().width) | v;
            }
            Ok(acc)
        }
        Expr::Slice(x, lo, t) => Ok((eval(x, a)? >> *lo) & mask(t.width)),
        Expr::AllDistinct(members) => {
            // Every member is read (an unreadable one is an error whatever
            // the others hold), then compared pairwise.
            let vals = members
                .iter()
                .map(|m| eval(m, a))
                .collect::<Result<Vec<_>, _>>()?;
            Ok(bit(vals
                .iter()
                .enumerate()
                .all(|(i, v)| vals[i + 1..].iter().all(|w| w != v))))
        }
        Expr::Array(_) => Err(ConstraintEvalError::Unexpanded),
    }
}

/// Number of one bits.
pub fn popcount(v: &BigUint) -> u64 {
    v.iter_u64_digits().map(|d| u64::from(d.count_ones())).sum()
}

#[cfg(test)]
mod tests {
    use super::*;

    fn u(w: u32) -> Ty {
        Ty::unsigned(w)
    }
    fn s(w: u32) -> Ty {
        Ty::signed(w)
    }
    fn c(t: Ty, v: i64) -> Expr {
        // Two's-complement truncation of a possibly negative literal.
        Expr::Const(t, from_signed(&BigInt::from(v), t.width))
    }
    fn var(id: u32, t: Ty) -> Expr {
        Expr::Var(id, t)
    }
    fn bin(op: BinOp, l: Expr, r: Expr) -> Expr {
        let t = if op.is_compare() || op.is_logical() {
            Ty::BIT
        } else {
            l.ty()
        };
        Expr::Binary(op, Box::new(l), Box::new(r), t)
    }
    fn asg(vars: &[u64]) -> Assignment {
        Assignment {
            vars: vars.iter().map(|v| BigUint::from(*v)).collect(),
            states: vec![],
        }
    }
    fn ev(e: &Expr, vars: &[u64]) -> u64 {
        e.validate().expect("well typed");
        u64::try_from(eval(e, &asg(vars)).expect("evaluates")).expect("fits u64")
    }

    /// Array-level nodes (Task C14) are typed, validate through their
    /// sub-expressions, and are never evaluated directly: `eval` reports
    /// [`ConstraintEvalError::Unexpanded`] until `array::expand` has replaced
    /// them.
    #[test]
    fn array_nodes_validate_and_refuse_direct_evaluation() {
        let size = Expr::Array(ArrayNode::Size(0));
        assert_eq!(size.ty(), s(32));
        let elem = Expr::Array(ArrayNode::Elem {
            array: 0,
            index: Box::new(c(s(32), 1)),
            ty: u(8),
        });
        assert_eq!(elem.ty(), u(8));
        let each = Expr::Array(ArrayNode::Foreach {
            array: 0,
            var: 0,
            body: Box::new(bin(BinOp::Gt, elem.clone(), c(u(8), 0))),
        });
        assert_eq!(each.ty(), Ty::BIT);
        let sum = Expr::Array(ArrayNode::Reduce {
            op: ReduceOp::Sum,
            array: 0,
            var: 0,
            index_var: 1,
            body: Box::new(Expr::Array(ArrayNode::Loop(0, u(8)))),
        });
        assert_eq!(sum.ty(), u(8), "a reduction folds at the body's type");
        for e in [&size, &elem, &each, &sum] {
            e.validate().expect("well typed");
            assert_eq!(
                eval(e, &asg(&[])),
                Err(ConstraintEvalError::Unexpanded),
                "{e:?}"
            );
        }
        // A bad sub-expression is found through the node.
        let bad = Expr::Array(ArrayNode::Elem {
            array: 0,
            index: Box::new(Expr::Const(u(0), BigUint::default())),
            ty: u(8),
        });
        assert!(bad.validate().is_err());
        let zero = Expr::Array(ArrayNode::Elem {
            array: 0,
            index: Box::new(c(s(32), 0)),
            ty: u(0),
        });
        assert!(zero.validate().is_err());
    }

    #[test]
    fn wraparound_arithmetic_is_modular() {
        let a = var(0, u(8));
        let b = var(1, u(8));
        assert_eq!(ev(&bin(BinOp::Add, a.clone(), b.clone()), &[200, 100]), 44);
        assert_eq!(ev(&bin(BinOp::Sub, a.clone(), b.clone()), &[3, 5]), 254);
        assert_eq!(ev(&bin(BinOp::Mul, a, b), &[16, 17]), 16);
    }

    #[test]
    fn neg_and_not() {
        let a = var(0, u(4));
        let neg = Expr::Unary(UnOp::Neg, Box::new(a.clone()), u(4));
        assert_eq!(ev(&neg, &[1]), 15);
        assert_eq!(ev(&neg, &[0]), 0);
        let not = Expr::Unary(UnOp::BitNot, Box::new(a), u(4));
        assert_eq!(ev(&not, &[0b1010]), 0b0101);
    }

    #[test]
    fn signed_compare_differs_from_unsigned() {
        // 8'hFF is -1 signed, 255 unsigned.
        let lt_s = bin(BinOp::Lt, var(0, s(8)), c(s(8), 0));
        let lt_u = bin(BinOp::Lt, var(0, u(8)), c(u(8), 0));
        assert_eq!(ev(&lt_s, &[0xFF]), 1);
        assert_eq!(ev(&lt_u, &[0xFF]), 0);
        let ge_s = bin(BinOp::Ge, var(0, s(8)), c(s(8), -2));
        assert_eq!(ev(&ge_s, &[0xFF]), 1);
        assert_eq!(ev(&ge_s, &[0xFD]), 0);
    }

    #[test]
    fn signed_division_truncates_toward_zero() {
        let q = bin(BinOp::Div, var(0, s(8)), var(1, s(8)));
        let r = bin(BinOp::Mod, var(0, s(8)), var(1, s(8)));
        // -7 / 2 = -3, -7 % 2 = -1.
        assert_eq!(ev(&q, &[0xF9, 2]), 0xFD);
        assert_eq!(ev(&r, &[0xF9, 2]), 0xFF);
        // Unsigned: 249 / 2 = 124.
        let uq = bin(BinOp::Div, var(0, u(8)), var(1, u(8)));
        assert_eq!(ev(&uq, &[0xF9, 2]), 124);
    }

    #[test]
    fn divide_by_zero_is_a_typed_error() {
        let q = bin(BinOp::Div, var(0, u(8)), var(1, u(8)));
        assert_eq!(
            eval(&q, &asg(&[1, 0])),
            Err(ConstraintEvalError::DivideByZero)
        );
    }

    #[test]
    fn shifts() {
        let a = var(0, u(8));
        let sh = |op, n: u64| bin(op, a.clone(), c(u(4), n as i64));
        assert_eq!(ev(&sh(BinOp::Shl, 3), &[0b1011_0001]), 0b1000_1000);
        assert_eq!(ev(&sh(BinOp::Shr, 3), &[0b1011_0001]), 0b0001_0110);
        // Shifting by >= the width clears everything.
        assert_eq!(ev(&sh(BinOp::Shl, 9), &[0xFF]), 0);
        assert_eq!(ev(&sh(BinOp::Shr, 12), &[0xFF]), 0);
        // `>>>` on an unsigned operand is a logical shift (11.4.10) ...
        assert_eq!(ev(&sh(BinOp::Ashr, 2), &[0x80]), 0x20);
        // ... and on a signed one it fills with the sign.
        let sa = bin(BinOp::Ashr, var(0, s(8)), c(u(4), 2));
        assert_eq!(ev(&sa, &[0x80]), 0xE0);
        let sa_big = bin(BinOp::Ashr, var(0, s(8)), c(u(4), 12));
        assert_eq!(ev(&sa_big, &[0x80]), 0xFF);
        assert_eq!(ev(&sa_big, &[0x40]), 0x00);
    }

    #[test]
    fn reductions_and_logical_ops() {
        let a = var(0, u(4));
        let red = |op| Expr::Unary(op, Box::new(a.clone()), Ty::BIT);
        assert_eq!(ev(&red(UnOp::RedAnd), &[0b1111]), 1);
        assert_eq!(ev(&red(UnOp::RedAnd), &[0b1110]), 0);
        assert_eq!(ev(&red(UnOp::RedNand), &[0b1110]), 1);
        assert_eq!(ev(&red(UnOp::RedOr), &[0]), 0);
        assert_eq!(ev(&red(UnOp::RedNor), &[0]), 1);
        assert_eq!(ev(&red(UnOp::RedXor), &[0b0111]), 1);
        assert_eq!(ev(&red(UnOp::RedXnor), &[0b0111]), 0);
        assert_eq!(ev(&red(UnOp::LogNot), &[0]), 1);
        // 8 -> 1, 0 -> 0 as truthiness; implication and equivalence.
        let imp = bin(BinOp::LogImpl, var(0, u(4)), var(1, u(4)));
        assert_eq!(ev(&imp, &[8, 0]), 0);
        assert_eq!(ev(&imp, &[0, 0]), 1);
        assert_eq!(ev(&imp, &[8, 3]), 1);
        let eqv = bin(BinOp::LogEquiv, var(0, u(4)), var(1, u(4)));
        assert_eq!(ev(&eqv, &[8, 1]), 1);
        assert_eq!(ev(&eqv, &[8, 0]), 0);
    }

    #[test]
    fn resize_extends_by_the_operand_signedness() {
        // 4'b1000 sign-extends to 8'hF8 when signed, 8'h08 when unsigned.
        let zs = Expr::Resize(Box::new(var(0, s(4))), s(8));
        let zu = Expr::Resize(Box::new(var(0, u(4))), s(8));
        assert_eq!(ev(&zs, &[0b1000]), 0xF8);
        assert_eq!(ev(&zu, &[0b1000]), 0x08);
        let tr = Expr::Resize(Box::new(var(0, u(8))), u(4));
        assert_eq!(ev(&tr, &[0xAB]), 0xB);
    }

    #[test]
    fn concat_and_slice() {
        let cat = Expr::Concat(vec![var(0, u(4)), var(1, u(4))], u(8));
        assert_eq!(ev(&cat, &[0xA, 0x5]), 0xA5);
        let sl = Expr::Slice(Box::new(var(0, u(8))), 2, u(3));
        assert_eq!(ev(&sl, &[0b1011_0100]), 0b101);
    }

    #[test]
    fn all_distinct_is_every_pair_not_just_neighbours() {
        let e = Expr::AllDistinct(vec![var(0, u(2)), var(1, u(2)), var(2, u(2))]);
        assert_eq!(e.ty(), Ty::BIT);
        for a in 0..4u64 {
            for b in 0..4u64 {
                for d in 0..4u64 {
                    let want = u64::from(a != b && b != d && a != d);
                    assert_eq!(ev(&e, &[a, b, d]), want, "{a} {b} {d}");
                }
            }
        }
        // The same variable twice is two equal members.
        let twice = Expr::AllDistinct(vec![var(0, u(2)), var(0, u(2))]);
        assert_eq!(ev(&twice, &[1]), 0);
        // A group with one member (the builder never makes one) is trivially distinct.
        assert_eq!(ev(&Expr::AllDistinct(vec![var(0, u(2))]), &[1]), 1);
    }

    #[test]
    fn all_distinct_reads_every_member_and_state() {
        let e = Expr::AllDistinct(vec![var(0, u(4)), Expr::State(0, u(4)), var(1, u(4))]);
        let st = |v: Option<u8>| Assignment {
            vars: vec![BigUint::from(1u8), BigUint::from(2u8)],
            states: vec![v.map(BigUint::from)],
        };
        assert_eq!(eval(&e, &st(Some(3))), Ok(BigUint::one()));
        assert_eq!(eval(&e, &st(Some(2))), Ok(BigUint::zero()));
        // An unreadable member is an error even when two others already
        // collide (the group is not short-circuited past it).
        let dup = Expr::AllDistinct(vec![var(0, u(4)), var(0, u(4)), Expr::State(0, u(4))]);
        assert_eq!(
            eval(&dup, &st(None)),
            Err(ConstraintEvalError::StateUnknown(0))
        );
        let mut vars = vec![];
        e.for_each_var(&mut |v, _| vars.push(v));
        assert_eq!(vars, [0, 1]);
        let mut states = vec![];
        e.for_each_state(&mut |s| states.push(s));
        assert_eq!(states, [0]);
    }

    #[test]
    fn all_distinct_substitution_keeps_member_order() {
        let e = Expr::AllDistinct(vec![var(0, u(4)), var(1, u(4)), var(2, u(4))]);
        let sub = e.substitute_vars(&mut |v, t| match v {
            1 => Expr::constant(t, 9u8),
            other => Expr::Var(other + 10, t),
        });
        assert_eq!(
            sub,
            Expr::AllDistinct(vec![var(10, u(4)), c(u(4), 9), var(12, u(4))])
        );
    }

    #[test]
    fn all_distinct_validation_demands_one_member_type() {
        assert!(
            Expr::AllDistinct(vec![var(0, u(4)), var(1, u(4))])
                .validate()
                .is_ok()
        );
        // The empty group has no type to agree on: a builder bug.
        assert!(Expr::AllDistinct(vec![]).validate().is_err());
        // Width and signedness must agree (6.22.1 equivalence).
        assert!(
            Expr::AllDistinct(vec![var(0, u(4)), var(1, u(8))])
                .validate()
                .is_err()
        );
        assert!(
            Expr::AllDistinct(vec![var(0, u(4)), var(1, s(4))])
                .validate()
                .is_err()
        );
        // A member's own tree is validated too.
        let bad_member = Expr::Const(u(4), BigUint::from(16u8));
        assert!(
            Expr::AllDistinct(vec![var(0, u(4)), bad_member])
                .validate()
                .is_err()
        );
    }

    #[test]
    fn ite_reads_truthiness() {
        let e = Expr::Ite(
            Box::new(var(0, u(4))),
            Box::new(c(u(8), 7)),
            Box::new(c(u(8), 9)),
            u(8),
        );
        assert_eq!(ev(&e, &[0]), 9);
        assert_eq!(ev(&e, &[2]), 7);
    }

    #[test]
    fn state_with_unknown_bits_is_an_error_never_zero() {
        let e = bin(BinOp::Add, Expr::State(0, u(8)), c(u(8), 1));
        let ok = Assignment {
            vars: vec![],
            states: vec![Some(BigUint::from(4u8))],
        };
        assert_eq!(eval(&e, &ok), Ok(BigUint::from(5u8)));
        let xz = Assignment {
            vars: vec![],
            states: vec![None],
        };
        assert_eq!(eval(&e, &xz), Err(ConstraintEvalError::StateUnknown(0)));
        let none = Assignment::default();
        assert_eq!(eval(&e, &none), Err(ConstraintEvalError::UnboundState(0)));
    }

    #[test]
    fn wide_values_beyond_64_bits() {
        let w = 100;
        let a = Expr::Var(0, u(w));
        let e = bin(BinOp::Add, a, Expr::constant(u(w), 1u8));
        let all_ones = Assignment {
            vars: vec![mask(w)],
            states: vec![],
        };
        // 2^100 - 1 + 1 wraps to 0.
        assert_eq!(eval(&e, &all_ones), Ok(BigUint::zero()));
        let half = Assignment {
            vars: vec![BigUint::one() << 99],
            states: vec![],
        };
        assert_eq!(eval(&e, &half), Ok((BigUint::one() << 99) + BigUint::one()));
    }

    #[test]
    fn validation_rejects_ill_typed_trees() {
        // Operand widths differ.
        let bad = Expr::Binary(
            BinOp::Add,
            Box::new(var(0, u(8))),
            Box::new(var(1, u(4))),
            u(8),
        );
        assert!(matches!(bad.validate(), Err(IrError::IllTyped { .. })));
        // A comparison must produce one bit.
        let bad = Expr::Binary(
            BinOp::Lt,
            Box::new(var(0, u(8))),
            Box::new(var(1, u(8))),
            u(8),
        );
        assert!(bad.validate().is_err());
        // Slice out of range.
        let bad = Expr::Slice(Box::new(var(0, u(8))), 6, u(4));
        assert!(bad.validate().is_err());
        // Constant too wide for its type.
        let bad = Expr::Const(u(4), BigUint::from(16u8));
        assert!(bad.validate().is_err());
        // Concat width mismatch.
        let bad = Expr::Concat(vec![var(0, u(4)), var(1, u(4))], u(9));
        assert!(bad.validate().is_err());
        // Mixed signedness in a comparison is a builder bug, not a coercion.
        let bad = Expr::Binary(
            BinOp::Lt,
            Box::new(var(0, s(8))),
            Box::new(var(1, u(8))),
            Ty::BIT,
        );
        assert!(bad.validate().is_err());
    }

    #[test]
    fn for_each_var_visits_every_read() {
        let e = bin(
            BinOp::Add,
            Expr::Concat(vec![var(3, u(4)), var(1, u(4))], u(8)),
            Expr::Ite(
                Box::new(var(2, u(1))),
                Box::new(Expr::Const(u(8), BigUint::one())),
                Box::new(Expr::State(0, u(8))),
                u(8),
            ),
        );
        let mut seen = vec![];
        e.for_each_var(&mut |v, _| seen.push(v));
        seen.sort_unstable();
        assert_eq!(seen, [1, 2, 3]);
    }

    #[test]
    fn substitute_vars_replaces_and_preserves_evaluation() {
        // x0 + concat(x1, x2)[7:0] with x1 replaced by the constant 5 and the
        // others renumbered (x0 -> 1, x2 -> 0): the substituted tree must
        // evaluate exactly like the original under the matching assignment.
        let e = bin(
            BinOp::Add,
            var(0, u(8)),
            Expr::Concat(vec![var(1, u(4)), var(2, u(4))], u(8)),
        );
        let sub = e.substitute_vars(&mut |v, t| match v {
            0 => Expr::Var(1, t),
            1 => Expr::constant(t, 5u8),
            _ => Expr::Var(0, t),
        });
        sub.validate().expect("still well-typed");
        let mut seen = vec![];
        sub.for_each_var(&mut |v, _| seen.push(v));
        seen.sort_unstable();
        assert_eq!(seen, [0, 1], "x1 is gone, the others renumbered");
        let full = Assignment {
            vars: vec![BigUint::from(10u8), BigUint::from(5u8), BigUint::from(3u8)],
            states: vec![],
        };
        let part = Assignment {
            vars: vec![BigUint::from(3u8), BigUint::from(10u8)],
            states: vec![],
        };
        assert_eq!(eval(&e, &full), eval(&sub, &part));
        assert_eq!(eval(&sub, &part), Ok(BigUint::from(10u8 + 0x53)));
    }
}