vj-sim 0.2.0

//! Constraint guards (LRM 1800-2023 18.5.12): the 4-valued `FALSE`/`TRUE`/
//! `ERROR`/`RANDOM` evaluator run on an implication's or `if`'s predicate
//! before the constraint reaches the solver (plan section 1.7).
//!
//! # What a guard is
//!
//! The predicate of a constraint-level `->` or `if` is a *guard*, not a
//! relation for the solver to satisfy: it is evaluated first, over constants,
//! state variables and object handles, and only what it cannot decide (it
//! reads a random variable) becomes a conditional constraint. Evaluating it
//! yields one of four values ([`GuardValue`]) by Figure 18-3's three truth
//! tables, applied bottom-up over the predicate's `&&`/`||`/`!` tree:
//!
//! | final value | outcome |
//! | ----------- | ------- |
//! | `TRUE`      | the body is an unconditional constraint |
//! | `FALSE`     | the constraint is eliminated, and "can generate no error" |
//! | `ERROR`     | `randomize()` fails with an error ([`GuardError`]) |
//! | `RANDOM`    | a conditional constraint: the guard stays in the IR |
//!
//! The tables are *not* Rust's short-circuit semantics. `FALSE` dominates
//! `ERROR` under `&&` in either order (`E && 0` is `0`), and `TRUE` dominates
//! it under `||`, so `a.x == 5 || b.x > 0` with a null `b` and `a.x == 5` is
//! an unconditional constraint and not an error (LRM 18.5.12 Example 1,
//! Case 1), while `ERROR` dominates `RANDOM` (`R && E` is `E`). The guard's
//! sub-expressions are "evaluated in an arbitrary order", so the result may
//! not depend on operand order, and the tables here are symmetric.
//!
//! # Leaves
//!
//! Only `&&`, `||` and `!` are structural. Every other node is a *leaf*:
//!
//! * a leaf that reads a state variable whose value cannot be read (a null
//!   handle on the way to it, a deleted object, an X/Z value) is `ERROR`,
//!   even when it also reads a random variable: dereferencing a null handle
//!   is the error the guard exists to prevent;
//! * otherwise a leaf that reads a random variable is `RANDOM`;
//! * otherwise the leaf is evaluated ([`super::ir::eval`]) and is `TRUE` or
//!   `FALSE` by its truthiness, or `ERROR` if its evaluation fails (a
//!   division by zero).
//!
//! # Resolving a program
//!
//! [`resolve`] rewrites a conjunct's [`Expr::Guard`] nodes under the state
//! values read for one `randomize()` call. A `RANDOM` predicate is rewritten
//! too: each maximal sub-tree that is decided (`TRUE`/`FALSE`, which also
//! drops an `ERROR` it dominates) becomes a constant, so what reaches the
//! solver reads only random variables and readable state, and a state read
//! the predicate dodges (`R || (T || E)`) can never make the BDD fail. That
//! is exact: a node whose final value is `RANDOM` has only `TRUE`/`RANDOM`
//! children under `&&` and only `FALSE`/`RANDOM` under `||`, so a decided
//! child is the identity of its operator.

use super::ir::{Assignment, BinOp, ConstraintEvalError, Expr, StateId, Ty, UnOp, eval};
use core::fmt;
use num_bigint::BigUint;
use num_traits::{One, Zero};

/// The value of a guard (sub-)expression (LRM 18.5.12).
#[derive(Clone, Copy, Debug, PartialEq, Eq)]
pub enum GuardValue {
    /// `0`: the sub-expression is false.
    False,
    /// `1`: the sub-expression is true.
    True,
    /// `E`: the sub-expression causes an evaluation error.
    Error,
    /// `R`: the sub-expression reads a random variable and cannot be
    /// evaluated yet.
    Random,
}

impl GuardValue {
    /// Conjunction, Figure 18-3 (left table): `FALSE` dominates, then
    /// `ERROR`, then `RANDOM`.
    pub fn and(self, other: GuardValue) -> GuardValue {
        use GuardValue::{Error as E, False as F, Random as R, True as T};
        match (self, other) {
            (F, _) | (_, F) => F,
            (E, _) | (_, E) => E,
            (R, _) | (_, R) => R,
            (T, T) => T,
        }
    }

    /// Disjunction, Figure 18-3 (middle table): `TRUE` dominates, then
    /// `ERROR`, then `RANDOM`.
    pub fn or(self, other: GuardValue) -> GuardValue {
        use GuardValue::{Error as E, False as F, Random as R, True as T};
        match (self, other) {
            (T, _) | (_, T) => T,
            (E, _) | (_, E) => E,
            (R, _) | (_, R) => R,
            (F, F) => F,
        }
    }

    /// Negation, Figure 18-3 (right table): swaps `TRUE` and `FALSE`, keeps
    /// `ERROR` and `RANDOM`.
    #[allow(clippy::should_implement_trait)]
    pub fn not(self) -> GuardValue {
        match self {
            GuardValue::False => GuardValue::True,
            GuardValue::True => GuardValue::False,
            GuardValue::Error => GuardValue::Error,
            GuardValue::Random => GuardValue::Random,
        }
    }
}

/// Why a guard evaluated to `ERROR`.
#[derive(Clone, Debug, PartialEq, Eq)]
pub enum GuardCause {
    /// A leaf reads a state variable that has no value: a null or deleted
    /// object on the way to it, or an X/Z value.
    UnreadableState(StateId),
    /// A leaf failed to evaluate (a division by zero).
    Eval(ConstraintEvalError),
}

/// A guard whose final value is `ERROR`: `randomize()` fails (LRM 18.5.12).
#[derive(Clone, Debug, PartialEq, Eq)]
pub struct GuardError {
    /// The first erroring leaf.
    pub cause: GuardCause,
}

impl fmt::Display for GuardError {
    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
        match &self.cause {
            GuardCause::UnreadableState(s) => write!(
                f,
                "constraint guard error: state variable #{s} cannot be read (a null or deleted \
                 object handle, or an X/Z value)"
            ),
            GuardCause::Eval(e) => write!(f, "constraint guard error: {e}"),
        }
    }
}

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

/// Whether `e` reads any random variable.
fn reads_var(e: &Expr) -> bool {
    let mut any = false;
    e.for_each_var(&mut |_, _| any = true);
    any
}

/// The first state variable `e` reads that has no value under `a`.
fn unreadable_state(e: &Expr, a: &Assignment) -> Option<StateId> {
    let mut bad = None;
    e.for_each_state(&mut |s| {
        if bad.is_none() && !matches!(a.states.get(s as usize), Some(Some(_))) {
            bad = Some(s);
        }
    });
    bad
}

/// The value of one leaf (module docs), or why it is `ERROR`.
fn leaf(e: &Expr, a: &Assignment) -> Result<GuardValue, GuardCause> {
    if let Some(s) = unreadable_state(e, a) {
        return Err(GuardCause::UnreadableState(s));
    }
    if reads_var(e) {
        return Ok(GuardValue::Random);
    }
    match eval(e, a) {
        Ok(v) if v.is_zero() => Ok(GuardValue::False),
        Ok(_) => Ok(GuardValue::True),
        Err(e) => Err(GuardCause::Eval(e)),
    }
}

/// The value of the predicate `pred` under `a` (only `a.states` is read; a
/// state of `None` is unreadable), by Figure 18-3 applied recursively.
pub fn value(pred: &Expr, a: &Assignment) -> GuardValue {
    match pred {
        Expr::Binary(BinOp::LogAnd, l, r, _) => value(l, a).and(value(r, a)),
        Expr::Binary(BinOp::LogOr, l, r, _) => value(l, a).or(value(r, a)),
        Expr::Unary(UnOp::LogNot, x, _) => value(x, a).not(),
        other => leaf(other, a).unwrap_or(GuardValue::Error),
    }
}

/// The first leaf that makes the `ERROR` predicate `pred` an error. `pred`
/// must have [`value`] `Error`.
fn cause(pred: &Expr, a: &Assignment) -> GuardError {
    let erroring = |e: &Expr| value(e, a) == GuardValue::Error;
    let inner = match pred {
        Expr::Binary(BinOp::LogAnd | BinOp::LogOr, l, r, _) => {
            if erroring(l) {
                Some(&**l)
            } else if erroring(r) {
                Some(&**r)
            } else {
                None
            }
        }
        Expr::Unary(UnOp::LogNot, x, _) if erroring(x) => Some(&**x),
        _ => None,
    };
    match inner {
        Some(i) => cause(i, a),
        None => GuardError {
            cause: match leaf(pred, a) {
                Err(c) => c,
                Ok(_) => unreachable!("`cause` is only asked of an erroring predicate"),
            },
        },
    }
}

fn constant(b: bool) -> Expr {
    Expr::Const(Ty::BIT, if b { BigUint::one() } else { BigUint::zero() })
}

/// The `RANDOM` predicate `pred` with every decided sub-tree replaced by a
/// constant (module docs).
fn simplify(pred: &Expr, a: &Assignment) -> Result<Expr, GuardError> {
    match value(pred, a) {
        GuardValue::True => Ok(constant(true)),
        GuardValue::False => Ok(constant(false)),
        GuardValue::Error => Err(cause(pred, a)),
        GuardValue::Random => Ok(match pred {
            Expr::Binary(op @ (BinOp::LogAnd | BinOp::LogOr), l, r, t) => Expr::Binary(
                *op,
                Box::new(simplify(l, a)?),
                Box::new(simplify(r, a)?),
                *t,
            ),
            Expr::Unary(UnOp::LogNot, x, t) => {
                Expr::Unary(UnOp::LogNot, Box::new(simplify(x, a)?), *t)
            }
            leaf => leaf.clone(),
        }),
    }
}

/// `e` with every [`Expr::Guard`] resolved under the state values of `a`
/// (module docs): a `FALSE` guard becomes its else arm, a `TRUE` guard its
/// body, a `RANDOM` guard a guard over the simplified predicate, and an
/// `ERROR` guard is the call's failure. An arm that is not selected is
/// dropped unexamined, so a guard inside it cannot raise an error ("the
/// constraint is eliminated and can generate no error").
pub fn resolve(e: &Expr, a: &Assignment) -> Result<Expr, GuardError> {
    Ok(match e {
        Expr::Const(..) | Expr::Var(..) | Expr::State(..) => e.clone(),
        Expr::Guard(p, then, otherwise, t) => match value(p, a) {
            GuardValue::True => resolve(then, a)?,
            GuardValue::False => resolve(otherwise, a)?,
            GuardValue::Error => return Err(cause(p, a)),
            GuardValue::Random => Expr::Guard(
                Box::new(simplify(p, a)?),
                Box::new(resolve(then, a)?),
                Box::new(resolve(otherwise, a)?),
                *t,
            ),
        },
        Expr::Unary(op, x, t) => Expr::Unary(*op, Box::new(resolve(x, a)?), *t),
        Expr::Binary(op, l, r, t) => {
            Expr::Binary(*op, Box::new(resolve(l, a)?), Box::new(resolve(r, a)?), *t)
        }
        Expr::Ite(c, x, y, t) => Expr::Ite(
            Box::new(resolve(c, a)?),
            Box::new(resolve(x, a)?),
            Box::new(resolve(y, a)?),
            *t,
        ),
        Expr::Resize(x, t) => Expr::Resize(Box::new(resolve(x, a)?), *t),
        Expr::Concat(parts, t) => Expr::Concat(
            parts
                .iter()
                .map(|p| resolve(p, a))
                .collect::<Result<_, _>>()?,
            *t,
        ),
        Expr::Slice(x, lo, t) => Expr::Slice(Box::new(resolve(x, a)?), *lo, *t),
        Expr::AllDistinct(members) => Expr::AllDistinct(
            members
                .iter()
                .map(|m| resolve(m, a))
                .collect::<Result<_, _>>()?,
        ),
        Expr::Array(n) => {
            let mut err = None;
            let r = n.map_children(&mut |c| match resolve(c, a) {
                Ok(x) => x,
                Err(e) => {
                    err.get_or_insert(e);
                    c.clone()
                }
            });
            if let Some(e) = err {
                return Err(e);
            }
            Expr::Array(r)
        }
    })
}

#[cfg(test)]
mod tests {
    use super::GuardValue::{Error as E, False as F, Random as R, True as T};
    use super::*;

    const ALL: [GuardValue; 4] = [F, T, E, R];

    /// Figure 18-3 transcribed: rows and columns in the figure's order
    /// `0 1 E R`.
    const AND: [[GuardValue; 4]; 4] = [
        [F, F, F, F], // 0
        [F, T, E, R], // 1
        [F, E, E, E], // E
        [F, R, E, R], // R
    ];
    const OR: [[GuardValue; 4]; 4] = [
        [F, T, E, R], // 0
        [T, T, T, T], // 1
        [E, T, E, E], // E
        [R, T, E, R], // R
    ];
    const NOT: [GuardValue; 4] = [T, F, E, R];

    #[test]
    fn conjunction_matches_figure_18_3_in_every_cell() {
        for (i, a) in ALL.iter().enumerate() {
            for (j, b) in ALL.iter().enumerate() {
                assert_eq!(a.and(*b), AND[i][j], "{a:?} && {b:?}");
            }
        }
    }

    #[test]
    fn disjunction_matches_figure_18_3_in_every_cell() {
        for (i, a) in ALL.iter().enumerate() {
            for (j, b) in ALL.iter().enumerate() {
                assert_eq!(a.or(*b), OR[i][j], "{a:?} || {b:?}");
            }
        }
    }

    #[test]
    fn negation_matches_figure_18_3() {
        for (i, a) in ALL.iter().enumerate() {
            assert_eq!(a.not(), NOT[i], "!{a:?}");
        }
    }

    #[test]
    fn the_tables_do_not_depend_on_operand_order() {
        // "The subexpressions are evaluated in an arbitrary order."
        for a in ALL {
            for b in ALL {
                assert_eq!(a.and(b), b.and(a));
                assert_eq!(a.or(b), b.or(a));
            }
        }
    }

    fn u8t() -> Ty {
        Ty::unsigned(8)
    }
    fn st(i: u32) -> Expr {
        Expr::State(i, u8t())
    }
    fn var(i: u32) -> Expr {
        Expr::Var(i, u8t())
    }
    fn k(v: u64) -> Expr {
        Expr::constant(u8t(), v)
    }
    fn bin(op: BinOp, l: Expr, r: Expr) -> Expr {
        let t = match op {
            BinOp::Eq
            | BinOp::Ne
            | BinOp::Lt
            | BinOp::Gt
            | BinOp::LogAnd
            | BinOp::LogOr
            | BinOp::LogImpl => Ty::BIT,
            _ => l.ty(),
        };
        Expr::Binary(op, Box::new(l), Box::new(r), t)
    }
    fn not(x: Expr) -> Expr {
        Expr::Unary(UnOp::LogNot, Box::new(x), Ty::BIT)
    }
    fn guard(p: Expr, then: Expr, otherwise: Expr) -> Expr {
        Expr::Guard(Box::new(p), Box::new(then), Box::new(otherwise), Ty::BIT)
    }
    fn states(v: &[Option<u64>]) -> Assignment {
        Assignment {
            vars: vec![],
            states: v.iter().map(|x| x.map(BigUint::from)).collect(),
        }
    }

    /// A leaf with each of the four values: `s0 == 1` is `TRUE` and
    /// `s0 == 2` `FALSE` under `s0 = 1`, `s1 == 0` reads the unreadable
    /// `s1` (`ERROR`) and `v0 == 3` reads a random variable (`RANDOM`).
    fn leaf_of(v: GuardValue) -> Expr {
        match v {
            T => bin(BinOp::Eq, st(0), k(1)),
            F => bin(BinOp::Eq, st(0), k(2)),
            E => bin(BinOp::Eq, st(1), k(0)),
            R => bin(BinOp::Eq, var(0), k(3)),
        }
    }
    fn env() -> Assignment {
        states(&[Some(1), None])
    }

    #[test]
    fn leaves_are_classified_by_what_they_read() {
        let a = env();
        for v in ALL {
            assert_eq!(value(&leaf_of(v), &a), v, "leaf for {v:?}");
        }
        // A leaf reading both a random variable and an unreadable state is
        // an error: the dereference is the error, whatever else it reads.
        let both = bin(BinOp::Lt, var(0), st(1));
        assert_eq!(value(&both, &a), E);
        // A state-only leaf whose evaluation fails is an error too.
        let div = bin(BinOp::Div, st(0), k(0));
        let div = bin(BinOp::Eq, div, k(0));
        assert_eq!(value(&div, &a), E);
        // Truthiness: a non-bit leaf is true when nonzero.
        assert_eq!(value(&st(0), &a), T);
        assert_eq!(value(&k(0), &a), F);
    }

    #[test]
    fn predicates_combine_by_the_tables_for_every_pair() {
        let a = env();
        for (i, x) in ALL.iter().enumerate() {
            for (j, y) in ALL.iter().enumerate() {
                let and = bin(BinOp::LogAnd, leaf_of(*x), leaf_of(*y));
                let or = bin(BinOp::LogOr, leaf_of(*x), leaf_of(*y));
                assert_eq!(value(&and, &a), AND[i][j], "{x:?} && {y:?}");
                assert_eq!(value(&or, &a), OR[i][j], "{x:?} || {y:?}");
            }
            assert_eq!(value(&not(leaf_of(*x)), &a), NOT[i], "!{x:?}");
        }
    }

    #[test]
    fn false_dominates_error_and_true_dominates_error_unlike_left_to_right() {
        let a = env();
        // E && 0: a left-to-right evaluator would already have failed.
        let e_and_f = bin(BinOp::LogAnd, leaf_of(E), leaf_of(F));
        assert_eq!(value(&e_and_f, &a), F);
        let e_or_t = bin(BinOp::LogOr, leaf_of(E), leaf_of(T));
        assert_eq!(value(&e_or_t, &a), T);
        // 1 && E: the error survives.
        let t_and_e = bin(BinOp::LogAnd, leaf_of(T), leaf_of(E));
        assert_eq!(value(&t_and_e, &a), E);
    }

    #[test]
    fn a_false_guard_takes_the_else_arm_and_drops_an_erroring_then_arm() {
        let a = env();
        // if (s0 == 2) <guard that errors> else v0 == 5
        let bad_then = guard(leaf_of(E), k_bit(1), k_bit(1));
        let else_arm = bin(BinOp::Eq, var(0), k(5));
        let g = guard(leaf_of(F), bad_then, else_arm.clone());
        assert_eq!(resolve(&g, &a), Ok(else_arm));
        // `a -> b` is a guard whose else arm is the constant 1: eliminated.
        let imp = guard(leaf_of(F), bin(BinOp::Eq, var(0), k(5)), k_bit(1));
        assert_eq!(resolve(&imp, &a), Ok(k_bit(1)));
    }

    fn k_bit(v: u64) -> Expr {
        Expr::constant(Ty::BIT, v)
    }

    #[test]
    fn a_true_guard_is_its_body_unconditionally() {
        let a = env();
        let body = bin(BinOp::Eq, var(0), k(5));
        let g = guard(leaf_of(T), body.clone(), k_bit(1));
        assert_eq!(resolve(&g, &a), Ok(body));
    }

    #[test]
    fn an_error_guard_fails_with_the_erroring_leaf() {
        let a = env();
        let g = guard(leaf_of(E), k_bit(1), k_bit(1));
        assert_eq!(
            resolve(&g, &a),
            Err(GuardError {
                cause: GuardCause::UnreadableState(1)
            })
        );
        // The cause is the leaf that decides the value, not one the tables
        // dominated: (E && 0) || E fails on the second E (state #1 both
        // times here, so use an eval error for the dominated one).
        let div = bin(BinOp::Eq, bin(BinOp::Div, st(0), k(0)), k(0));
        let p = bin(
            BinOp::LogOr,
            bin(BinOp::LogAnd, div, leaf_of(F)),
            leaf_of(E),
        );
        let g = guard(p, k_bit(1), k_bit(1));
        assert_eq!(
            resolve(&g, &a),
            Err(GuardError {
                cause: GuardCause::UnreadableState(1)
            })
        );
    }

    #[test]
    fn a_random_guard_stays_with_its_decided_subtrees_folded() {
        let a = env();
        // (v0 == 3 || s0 == 2 || (s1 == 0 && s0 == 2)) -> body: the second
        // and third disjuncts are FALSE (the third drops its ERROR), so the
        // conditional constraint is `(v0 == 3 || 0 || 0) -> body`.
        let p = bin(
            BinOp::LogOr,
            bin(BinOp::LogOr, leaf_of(R), leaf_of(F)),
            bin(BinOp::LogAnd, leaf_of(E), leaf_of(F)),
        );
        let body = bin(BinOp::Eq, var(1), k(7));
        let g = guard(p, body.clone(), k_bit(1));
        let want_p = bin(
            BinOp::LogOr,
            bin(BinOp::LogOr, leaf_of(R), k_bit(0)),
            k_bit(0),
        );
        assert_eq!(resolve(&g, &a), Ok(guard(want_p, body, k_bit(1))));
    }

    #[test]
    fn a_random_guard_with_an_error_disjunct_fails() {
        let a = env();
        // R || E is E: the guard cannot be left conditional.
        let p = bin(BinOp::LogOr, leaf_of(R), leaf_of(E));
        let g = guard(p, k_bit(1), k_bit(1));
        assert!(resolve(&g, &a).is_err());
    }

    #[test]
    fn guards_nest_and_resolve_inside_other_nodes() {
        let a = env();
        // (if (s0==1) (if (s0==2) X else Y)) && Z resolves to Y && Z.
        let y = bin(BinOp::Eq, var(0), k(1));
        let z = bin(BinOp::Eq, var(0), k(2));
        let x = bin(BinOp::Eq, var(0), k(9));
        let inner = guard(leaf_of(F), x, y.clone());
        let outer = guard(leaf_of(T), inner, k_bit(1));
        let all = bin(BinOp::LogAnd, outer, z.clone());
        assert_eq!(resolve(&all, &a), Ok(bin(BinOp::LogAnd, y, z)));
    }

    #[test]
    fn a_uniqueness_group_is_resolved_through_its_guards() {
        let a = env();
        let group = |m: Vec<Expr>| Expr::AllDistinct(m);
        // The taken arm of a decided guard is the group itself.
        let g = guard(
            leaf_of(T),
            group(vec![var(0), var(1), st(0)]),
            group(vec![var(0), var(1)]),
        );
        assert_eq!(resolve(&g, &a), Ok(group(vec![var(0), var(1), st(0)])));
        let g = guard(
            leaf_of(F),
            group(vec![var(0), var(1), st(0)]),
            group(vec![var(0), var(1)]),
        );
        assert_eq!(resolve(&g, &a), Ok(group(vec![var(0), var(1)])));
        // A random guard keeps the group as its body.
        let g = guard(leaf_of(R), group(vec![var(0), var(1)]), k_bit(1));
        assert_eq!(
            resolve(&g, &a),
            Ok(guard(leaf_of(R), group(vec![var(0), var(1)]), k_bit(1)))
        );
        // A guard inside a member is resolved in place, in member order.
        let member = bin(BinOp::Add, var(1), k(1));
        let wrapped = guard(leaf_of(T), member.clone(), k_bit(1));
        let g = group(vec![var(0), wrapped]);
        assert_eq!(resolve(&g, &a), Ok(group(vec![var(0), member])));
        // An unreadable state in a taken guard is still the loud error.
        let g = group(vec![var(0), guard(leaf_of(E), var(1), var(0))]);
        assert!(resolve(&g, &a).is_err());
    }

    #[test]
    fn an_expression_without_guards_resolves_to_itself() {
        let a = env();
        let e = bin(
            BinOp::LogImpl,
            bin(BinOp::Lt, var(0), st(0)),
            bin(BinOp::Eq, var(1), k(4)),
        );
        assert_eq!(resolve(&e, &a), Ok(e));
    }
}