vj-sim 0.2.0

//! The incremental sequence evaluator ([`Accel`]) against the reference
//! evaluator it stands in for: on every trace of a few signals up to a few ticks
//! long, grown one tick at a time the way the engine grows its window (one
//! accelerator, kept across the lengths), every start tick must get the same
//! disposition, the same nonvacuity and the same cover-sequence matches. The
//! reference is the oracle; nothing here is compared with a hand-written answer.
use super::*;
use crate::sva::trace::read_local;

/// Checks `ir` over every trace of `leaves` signals of `max_len` ticks, for both
/// strengths of a bare sequence and both start orders.
fn agree(ir: &PropertyIr, leaves: usize, max_len: usize) {
    for env in all_traces(leaves, max_len) {
        agree_on(ir, &env, max_len as u32);
    }
}

fn agree_on(ir: &PropertyIr, env: &dyn PropEnv, max_len: u32) {
    for strong in [false, true] {
        for reversed in [false, true] {
            let cell = RefCell::new(Accel::new(ir, 1, false, false).expect("an eligible shape"));
            for len in 1..=max_len {
                cell.borrow_mut().set_base(0);
                let starts: Vec<u32> = if reversed {
                    (0..len).rev().collect()
                } else {
                    (0..len).collect()
                };
                for start in starts {
                    let fast = Evaluator::new(ir, env, strong)
                        .open_future()
                        .with_accel(Some(&cell));
                    let slow = Evaluator::new(ir, env, strong).open_future();
                    let (a, b) = (fast.attempt(len, start), slow.attempt(len, start));
                    assert_eq!(a, b, "attempt len {len} start {start} strong {strong}");
                    if b == Ok(Disposition::Passes) {
                        assert_eq!(
                            fast.nonvacuous(len, start),
                            slow.nonvacuous(len, start),
                            "nonvacuous len {len} start {start} strong {strong}"
                        );
                    }
                    if matches!(ir.prop(ir.root), Prop::Seq { .. }) {
                        assert_eq!(
                            fast.root_sequence_matches(len, start),
                            slow.root_sequence_matches(len, start),
                            "matches len {len} start {start}"
                        );
                    }
                }
            }
        }
    }
}

/// `a |-> p` or `a |=> p` for the sequence property `p`.
fn implies(b: &mut B, a: SeqRef, p: PropId, overlapped: bool) -> PropId {
    b.prop(Prop::Implication {
        ante: a,
        cons: p,
        overlapped,
    })
}

fn bare(b: &mut B, seq: SeqRef, strength: Option<Strength>) -> PropId {
    b.prop(Prop::Seq { seq, strength })
}

#[test]
fn implication_with_a_ranged_consequent() {
    for overlapped in [true, false] {
        let mut b = B::new();
        let a = b.leaf(0);
        let c = b.seq_r(&[1, 2], &[(1, Some(2))]);
        let p = bare(&mut b, c, None);
        let root = implies(&mut b, a, p, overlapped);
        agree(&b.finish(root), 3, 4);
    }
}

#[test]
fn unbounded_delays_weak_and_strong() {
    for strength in [None, Some(Strength::Strong), Some(Strength::Weak)] {
        let mut b = B::new();
        let a = b.leaf(0);
        let c = b.seq_r(&[1, 2], &[(1, None)]);
        let p = bare(&mut b, c, strength);
        let root = implies(&mut b, a, p, true);
        agree(&b.finish(root), 3, 4);
    }
}

#[test]
fn bare_sequences_of_several_delays() {
    for strength in [None, Some(Strength::Strong)] {
        let mut b = B::new();
        let s = b.seq_r(&[0, 1, 2], &[(0, Some(1)), (1, None)]);
        let root = bare(&mut b, s, strength);
        agree(&b.finish(root), 3, 4);
        let mut b = B::new();
        let s = b.seq_r(&[0, 1], &[(0, Some(2))]);
        let root = bare(&mut b, s, strength);
        agree(&b.finish(root), 2, 6);
        let mut b = B::new();
        let s = b.seq_r(&[0, 1, 0], &[(2, Some(3)), (0, Some(0))]);
        let root = bare(&mut b, s, strength);
        agree(&b.finish(root), 2, 6);
    }
}

#[test]
fn a_ranged_antecedent_with_zero_delay() {
    let mut b = B::new();
    let a = b.seq_r(&[0, 1], &[(0, Some(2))]);
    let c = b.leaf(2);
    let p = bare(&mut b, c, None);
    let root = implies(&mut b, a, p, true);
    agree(&b.finish(root), 3, 4);
}

#[test]
fn negation_swaps_the_strength() {
    let mut b = B::new();
    let s = b.seq_r(&[0, 1], &[(1, Some(2))]);
    let p = bare(&mut b, s, None);
    let root = b.not(p);
    agree(&b.finish(root), 2, 6);
}

#[test]
fn always_eventually_until_over_implications() {
    let mut b = B::new();
    let a = b.leaf(0);
    let c = b.seq_r(&[1, 2], &[(1, Some(1))]);
    let p = bare(&mut b, c, None);
    let imp = implies(&mut b, a, p, true);
    let root = b.prop(Prop::Always {
        p: imp,
        lo: 0,
        hi: None,
        strong: false,
    });
    agree(&b.finish(root), 3, 4);

    let mut b = B::new();
    let a = b.leaf(0);
    let q = b.b(1, None);
    let ev = b.prop(Prop::Eventually {
        p: q,
        lo: 0,
        hi: None,
        strong: true,
    });
    let root = implies(&mut b, a, ev, false);
    agree(&b.finish(root), 2, 6);

    for strong in [false, true] {
        let mut b = B::new();
        let a = b.leaf(0);
        let p = b.b(1, None);
        let q = b.b(2, None);
        let un = b.prop(Prop::Until { p, q, strong });
        let root = implies(&mut b, a, un, true);
        agree(&b.finish(root), 3, 4);
    }
}

#[test]
fn boolean_combinations_of_sequences() {
    let mut b = B::new();
    let s1 = b.seq_r(&[0, 1], &[(1, Some(2))]);
    let s2 = b.seq_r(&[1, 2], &[(0, None)]);
    let p1 = bare(&mut b, s1, None);
    let p2 = bare(&mut b, s2, Some(Strength::Strong));
    let and = b.prop(Prop::And(p1, p2));
    agree(&b.finish(and), 3, 4);
    let mut b = B::new();
    let s1 = b.seq_r(&[0, 1], &[(1, Some(2))]);
    let s2 = b.seq_r(&[1, 2], &[(0, None)]);
    let p1 = bare(&mut b, s1, None);
    let p2 = bare(&mut b, s2, Some(Strength::Strong));
    let or = b.prop(Prop::Or(p1, p2));
    agree(&b.finish(or), 3, 4);
}

/// A trace of two signals whose leaf `5` reads local variable 0 and says whether
/// it equals leaf 1's value at the tick; leaves below 5 are the rows.
struct LocalRows(Rows);

impl PropEnv for LocalRows {
    fn value(&self, leaf: LeafId, tick: u32, frame: &[Option<i64>]) -> Result<i64, TraceError> {
        if leaf.0 == 5 {
            let v = read_local(frame, LocalVarId(0))?;
            return Ok(i64::from(v == self.0.value(LeafId(1), tick, frame)?));
        }
        self.0.value(leaf, tick, frame)
    }
    fn case_match(
        &self,
        _: LeafId,
        _: LeafId,
        _: u32,
        _: &[Option<i64>],
    ) -> Result<bool, TraceError> {
        Ok(false)
    }
}

fn agree_locals(ir: &PropertyIr, max_len: usize, locals_read: bool) {
    for rows in all_traces(2, max_len) {
        let env = LocalRows(rows);
        for strong in [false, true] {
            let cell = RefCell::new(Accel::new(ir, 1, false, locals_read).expect("eligible"));
            for len in 1..=max_len as u32 {
                cell.borrow_mut().set_base(0);
                for start in 0..len {
                    let fast = Evaluator::new(ir, &env, strong)
                        .open_future()
                        .with_accel(Some(&cell));
                    let slow = Evaluator::new(ir, &env, strong).open_future();
                    assert_eq!(
                        fast.attempt(len, start),
                        slow.attempt(len, start),
                        "len {len} start {start} strong {strong}"
                    );
                    if matches!(ir.prop(ir.root), Prop::Seq { .. }) {
                        assert_eq!(
                            fast.root_sequence_matches(len, start),
                            slow.root_sequence_matches(len, start),
                            "matches len {len} start {start}"
                        );
                    }
                }
            }
        }
    }
}

/// `l0 [v = l1] ##[m:n] (l5: v == l1) [v step?]`.
fn locals_seq(b: &mut B, step: bool, delay: (u32, Option<u32>)) -> SeqRef {
    let v = b.au.new_local_var(2, false);
    let entry = b.au.new_state();
    let (s1, s2, s3, s4, s5) = (
        b.au.new_state(),
        b.au.new_state(),
        b.au.new_state(),
        b.au.new_state(),
        b.au.new_state(),
    );
    b.au.add_edge(entry, Some(LeafId(0)), Transition::Epsilon, s1);
    b.au.add_edge(
        s1,
        None,
        Transition::LocalVarWrite {
            var: v,
            value: LeafId(1),
        },
        s2,
    );
    let (min, max) = delay;
    b.au.add_edge(s2, None, Transition::Delay { min, max }, s3);
    let mut at = s3;
    if step {
        b.au.add_edge(at, None, Transition::LocalVarStep { var: v, delta: 1 }, s4);
        at = s4;
    }
    b.au.add_edge(at, Some(LeafId(5)), Transition::Epsilon, s5);
    b.au.add_edge(
        s5,
        None,
        Transition::Match {
            actions: Vec::new(),
        },
        s5,
    );
    SeqRef::single(entry, false)
}

#[test]
fn local_variables_written_and_read() {
    for step in [false, true] {
        for delay in [(1, Some(1)), (1, Some(3)), (0, Some(2)), (1, None)] {
            for strength in [None, Some(Strength::Strong)] {
                for locals_read in [false, true] {
                    let mut b = B::new();
                    let s = locals_seq(&mut b, step, delay);
                    let root = bare(&mut b, s, strength);
                    agree_locals(&b.finish(root), 5, locals_read);
                }
            }
        }
    }
}

#[test]
fn local_variables_through_an_implication() {
    for step in [false, true] {
        let mut b = B::new();
        let a = locals_seq(&mut b, step, (1, Some(2)));
        let c = b.leaf(0);
        let p = bare(&mut b, c, None);
        let root = implies(&mut b, a, p, true);
        agree_locals(&b.finish(root), 5, true);
    }
}

#[test]
fn an_unassigned_read_fails_the_same_way() {
    // `l0 [v++] ##1 l5`: the step reads `v` before anything wrote it.
    let mut b = B::new();
    let v = b.au.new_local_var(2, false);
    let entry = b.au.new_state();
    let (s1, s2, s3) = (b.au.new_state(), b.au.new_state(), b.au.new_state());
    b.au.add_edge(entry, Some(LeafId(0)), Transition::Epsilon, s1);
    b.au.add_edge(s1, None, Transition::LocalVarStep { var: v, delta: 1 }, s2);
    b.au.add_edge(s2, Some(LeafId(5)), Transition::Epsilon, s3);
    b.au.add_edge(
        s3,
        None,
        Transition::Match {
            actions: Vec::new(),
        },
        s3,
    );
    let s = SeqRef::single(entry, false);
    let root = bare(&mut b, s, None);
    agree_locals(&b.finish(root), 4, true);
}

/// Windows that move: the accelerator is told the new base the way the engine
/// does when it drops the positions no pending attempt needs.
#[test]
fn a_sliding_window_agrees() {
    let mut b = B::new();
    let a = b.leaf(0);
    let c = b.seq_r(&[1, 2], &[(1, Some(2))]);
    let p = bare(&mut b, c, None);
    let root = implies(&mut b, a, p, true);
    let ir = b.finish(root);
    for env in all_traces(3, 4) {
        let cell = RefCell::new(Accel::new(&ir, 1, false, false).expect("eligible"));
        // The window is the trace from `base` on: a view with the first `base`
        // ticks cut off.
        for abs_len in 1..=4u32 {
            let base = abs_len / 2;
            let view = Rows(
                env.0
                    .iter()
                    .map(|r| r[base as usize..].to_vec())
                    .collect::<Vec<_>>(),
            );
            cell.borrow_mut().set_base(u64::from(base));
            cell.borrow_mut().evict_before(u64::from(base));
            let len = abs_len - base;
            for start in 0..len {
                let fast = Evaluator::new(&ir, &view, false)
                    .open_future()
                    .with_accel(Some(&cell));
                let slow = Evaluator::new(&ir, &view, false).open_future();
                assert_eq!(fast.attempt(len, start), slow.attempt(len, start));
            }
        }
    }
}

/// A tiny deterministic generator for the long-trace tests.
struct Xorshift(u64);

impl Xorshift {
    fn next(&mut self) -> u64 {
        self.0 ^= self.0 << 13;
        self.0 ^= self.0 >> 7;
        self.0 ^= self.0 << 17;
        self.0
    }
}

/// `ir` over random traces much longer than its lookahead, grown one tick at a
/// time with the window sliding at random points (the engine's `trim`), for both
/// strengths: every attempt's disposition and nonvacuity must be the
/// reference's. `ones` of 8 is the chance, in eighths, of a signal being high at
/// a tick: a property that holds for a long time needs a high density, one that
/// fails often a low one.
fn agree_long(ir: &PropertyIr, leaves: usize, len: u32, traces: u64, ones: [u64; 3]) {
    let mut rng = Xorshift(0x9e37_79b9_7f4a_7c15);
    for trace in 0..traces {
        let density = ones[(trace % 3) as usize];
        let abs: Vec<Vec<bool>> = (0..leaves)
            .map(|_| {
                (0..len)
                    .map(|_| rng.next() % 8 < density)
                    .collect::<Vec<_>>()
            })
            .collect();
        for strong in [false, true] {
            let cell = RefCell::new(Accel::new(ir, 1, false, false).expect("an eligible shape"));
            let mut base = 0u32;
            for abs_len in 1..=len {
                if base + 1 < abs_len && rng.next().is_multiple_of(4) {
                    base += (rng.next() % u64::from(abs_len - base)) as u32;
                    cell.borrow_mut().evict_before(u64::from(base));
                }
                cell.borrow_mut().set_base(u64::from(base));
                let view = Rows(
                    abs.iter()
                        .map(|r| r[base as usize..abs_len as usize].to_vec())
                        .collect(),
                );
                let wlen = abs_len - base;
                for start in 0..wlen {
                    let fast = Evaluator::new(ir, &view, strong)
                        .open_future()
                        .with_accel(Some(&cell));
                    let slow = Evaluator::new(ir, &view, strong).open_future();
                    let (a, b) = (fast.attempt(wlen, start), slow.attempt(wlen, start));
                    assert_eq!(
                        a, b,
                        "trace {trace} strong {strong} base {base} len {wlen} start {start}"
                    );
                    if b == Ok(Disposition::Passes) {
                        assert_eq!(
                            fast.nonvacuous(wlen, start),
                            slow.nonvacuous(wlen, start),
                            "nonvacuous trace {trace} base {base} len {wlen} start {start}"
                        );
                    }
                }
            }
        }
    }
}

fn always(b: &mut B, p: PropId, lo: u32, hi: Option<u32>) -> PropId {
    b.prop(Prop::Always {
        p,
        lo,
        hi,
        strong: false,
    })
}

fn eventually(b: &mut B, p: PropId, lo: u32, hi: Option<u32>) -> PropId {
    b.prop(Prop::Eventually {
        p,
        lo,
        hi,
        strong: false,
    })
}

const DENSITIES: [u64; 3] = [4, 6, 7];

#[test]
fn long_always_over_implications() {
    for overlapped in [true, false] {
        for (consequent, hi) in [
            (&[1u32][..], None),
            (&[1, 2][..], Some(3)),
            (&[1][..], Some(0)),
        ] {
            let mut b = B::new();
            let a = b.leaf(0);
            let c = if consequent.len() == 1 {
                b.leaf(1)
            } else {
                b.seq_r(consequent, &[(1, hi)])
            };
            let p = bare(&mut b, c, None);
            let imp = implies(&mut b, a, p, overlapped);
            let root = always(&mut b, imp, 0, None);
            agree_long(&b.finish(root), 3, 24, 30, DENSITIES);
        }
    }
}

#[test]
fn long_bounded_always_and_eventually() {
    for (lo, hi) in [
        (0, Some(2)),
        (1, Some(3)),
        (2, Some(2)),
        (0, None),
        (3, None),
    ] {
        let mut b = B::new();
        let a = b.leaf(0);
        let c = b.seq_r(&[1, 2], &[(1, Some(2))]);
        let p = bare(&mut b, c, None);
        let imp = implies(&mut b, a, p, false);
        let root = always(&mut b, imp, lo, hi);
        agree_long(&b.finish(root), 3, 20, 20, DENSITIES);

        let mut b = B::new();
        let q = b.b(1, None);
        let ev = eventually(&mut b, q, lo, hi);
        let a = b.leaf(0);
        let root = implies(&mut b, a, ev, true);
        agree_long(&b.finish(root), 3, 20, 20, DENSITIES);

        let mut b = B::new();
        let c = b.seq_r(&[1, 2], &[(1, Some(2))]);
        let q = bare(&mut b, c, Some(Strength::Strong));
        let ev = eventually(&mut b, q, lo, hi);
        let a = b.leaf(0);
        let root = implies(&mut b, a, ev, false);
        agree_long(&b.finish(root), 3, 20, 20, DENSITIES);
    }
}

#[test]
fn long_until() {
    for strong in [false, true] {
        let mut b = B::new();
        let a = b.leaf(0);
        let p = b.b(1, None);
        let q = b.b(2, None);
        let un = b.prop(Prop::Until { p, q, strong });
        let root = implies(&mut b, a, un, true);
        agree_long(&b.finish(root), 3, 20, 20, DENSITIES);

        let mut b = B::new();
        let c = b.seq_r(&[1, 2], &[(0, Some(1))]);
        let p = bare(&mut b, c, None);
        let q = b.b(0, None);
        let root = b.prop(Prop::Until { p, q, strong });
        agree_long(&b.finish(root), 3, 20, 20, DENSITIES);
    }
}

#[test]
fn long_nested_operators() {
    // always (a |-> eventually b): the eventually's operand settles, the
    // always's does not (unbounded).
    let mut b = B::new();
    let a = b.leaf(0);
    let q = b.b(1, None);
    let ev = eventually(&mut b, q, 0, None);
    let imp = implies(&mut b, a, ev, true);
    let root = always(&mut b, imp, 0, None);
    agree_long(&b.finish(root), 3, 20, 20, DENSITIES);

    // not (always [0:3] (a or nexttime [2] b))
    let mut b = B::new();
    let p1 = b.b(0, None);
    let p2 = b.b(1, None);
    let nx = b.prop(Prop::Nexttime {
        p: p2,
        n: 2,
        strong: false,
    });
    let or = b.prop(Prop::Or(p1, nx));
    let al = always(&mut b, or, 0, Some(3));
    let root = b.not(al);
    agree_long(&b.finish(root), 3, 20, 20, DENSITIES);

    // a |-> always [1:3] (b and (c until d))
    let mut b = B::new();
    let a = b.leaf(0);
    let p = b.b(1, None);
    let q = b.b(2, None);
    let un = b.prop(Prop::Until {
        p,
        q,
        strong: false,
    });
    let pb = b.b(1, None);
    let and = b.prop(Prop::And(pb, un));
    let al = always(&mut b, and, 1, Some(3));
    let root = implies(&mut b, a, al, false);
    agree_long(&b.finish(root), 3, 20, 20, DENSITIES);

    // always (if (a) b else (c |=> a))
    let mut b = B::new();
    let t = b.b(1, None);
    let cc = b.leaf(2);
    let aa = b.b(0, None);
    let e = implies(&mut b, cc, aa, false);
    let iff = b.prop(Prop::If {
        cond: LeafId(0),
        then: t,
        els: Some(e),
    });
    let root = always(&mut b, iff, 0, None);
    agree_long(&b.finish(root), 3, 20, 20, DENSITIES);
}

/// A lone Boolean antecedent (the shape of `a |-> ...`) is answered by the
/// one-letter guard: the same matches as the reference evaluator, held inline
/// in the result (no heap allocation per attempt tick, which is what the SVA
/// benchmark's `ALLOCS` line measures).
#[test]
fn lone_boolean_matches_stay_inline_and_agree() {
    let mut b = B::new();
    let a = b.leaf(0);
    let root = bare(&mut b, a, None);
    let ir = b.finish(root);
    let word = TailWord::strong(3);
    for env in all_traces(1, 3) {
        let cell = RefCell::new(Accel::new(&ir, 1, false, false).expect("an eligible shape"));
        cell.borrow_mut().set_base(0);
        let fast = Evaluator::new(&ir, &env, true)
            .open_future()
            .with_accel(Some(&cell));
        let slow = Evaluator::new(&ir, &env, true).open_future();
        for pos in 0..2 {
            let got = fast.matches(a, &word, pos, &Vec::new()).unwrap();
            assert!(!got.spilled(), "pos {pos}: matches left the inline buffer");
            assert_eq!(got, slow.matches(a, &word, pos, &Vec::new()).unwrap());
        }
    }
}