vj_sim/sva/

incremental.rs

//! Incremental sequence evaluation for the live engine (`sva-perf`).
//!
//! The reference evaluator ([`super::property::Evaluator`]) is stateless: every
//! pending attempt re-runs every sequence search from its start over the whole
//! window each time a position is appended ([`super::trace::attempt_word_calls`]
//! is a tick-ordered BTreeSet search). That is `O(window)` per attempt per tick,
//! and `O(window^2)` for a weak sequence, which re-runs the search once per cut.
//!
//! [`Accel`] keeps the search state of every `(sequence entry, start tick, local
//! frame)` that has been asked about between calls, and advances it by the ticks
//! that arrived since. The result is, by construction, what the reference
//! returns; the engine's differential mode (see `engine.rs`) runs both and asserts
//! it, and so does a property-level exhaustive test.
//!
//! # The model
//!
//! A search over a word `w = real samples ++ constant tail` is a set of
//! *configurations* `(tick, state, frame)` closed under the automaton's edges.
//! Everything that happens at a REAL tick (`tick < real`) depends on the samples
//! only, so it is the same for every word and is advanced exactly once, forever.
//! What differs between words is the tail: from tick `real` on every position is
//! the letter `⊤` or `⊥` (a guard holds on `⊤` only, a value read there is `0`),
//! so the search over the tail is a pure function of the *frontier* -- the
//! configurations that are still alive at tick `real` -- and of the letter spec.
//! The frontier is stored as a pool of [`Rng`]s ("`(state, frame)` is alive at
//! every tick of `lo..=hi`", which is what a `##[m:n]` edge produces), canonical
//! per `(state, frame)`, and the tail search is memoized by the frontier's
//! signature relative to `real`: thousands of attempts that are in the same
//! position share one tail search.
//!
//! # What it declines
//!
//! Anything the reference does that is not a function of the above is declined
//! (the caller falls back to the reference, which is always correct): several
//! clocks, subroutine calls, end points, `first_match`, aborts, a sequence leaf
//! that is the `disable iff` condition (its value changes under a position), a
//! query for an earlier word than one already advanced past, any error, and an
//! interner that outgrew its cap.
//!
//! Where the reference can fail on a LETTER tick (only a `LocalVarStep` reads a
//! variable there) the accelerator never skips a tail search the reference runs
//! (`exact`): a skipped search could hide an error.
use std::collections::{BTreeMap, BTreeSet, HashMap, HashSet};
use std::hash::{BuildHasherDefault, Hasher};

use super::ir::{Automaton, LeafId, ThreadStateId, Transition};
use super::property::{Prop, PropEnv, PropId, PropertyIr};
use super::trace::{Frame, Matches, read_local};

/// The end of an unbounded range.
const INF: u64 = u64::MAX;
/// Distinct local-variable frames the interner may hold before the accelerator
/// switches itself off (and everything it knows is dropped).
const MAX_FRAMES: usize = 1 << 20;
/// Memoized tail searches before the memo is cleared.
const MAX_MEMO: usize = 1 << 16;

#[derive(Default, Clone, Copy)]
struct Fx(u64);

impl Fx {
    #[inline]
    fn add(&mut self, w: u64) {
        self.0 = (self.0.rotate_left(5) ^ w).wrapping_mul(0x517c_c1b7_2722_0a95);
    }
}

impl Hasher for Fx {
    #[inline]
    fn finish(&self) -> u64 {
        self.0
    }
    #[inline]
    fn write(&mut self, bytes: &[u8]) {
        for &b in bytes {
            self.add(u64::from(b));
        }
    }
    #[inline]
    fn write_u8(&mut self, i: u8) {
        self.add(u64::from(i));
    }
    #[inline]
    fn write_u32(&mut self, i: u32) {
        self.add(u64::from(i));
    }
    #[inline]
    fn write_u64(&mut self, i: u64) {
        self.add(i);
    }
    #[inline]
    fn write_i64(&mut self, i: i64) {
        self.add(i as u64);
    }
    #[inline]
    fn write_usize(&mut self, i: usize) {
        self.add(i as u64);
    }
}

/// The search states of a window, by start tick: each key is `(entry, start,
/// frame id, weak)` of a [`Seq`]. Nearly every start has one, kept inline.
type ByStart = BTreeMap<u64, smallvec::SmallVec<[(u32, u64, u32, bool); 1]>>;
type FxMap<K, V> = HashMap<K, V, BuildHasherDefault<Fx>>;
type FxSet<K> = HashSet<K, BuildHasherDefault<Fx>>;

/// `(state, frame)` is alive at every tick of `lo..=hi`.
#[derive(Clone, Copy, PartialEq, Eq, Debug)]
struct Rng {
    state: u32,
    frame: u32,
    lo: u64,
    hi: u64,
}

impl Rng {
    fn same_key(&self, o: &Rng) -> bool {
        self.state == o.state && self.frame == o.frame
    }

    /// Whether the two ranges overlap or touch (so their union is one range).
    fn joins(&self, o: &Rng) -> bool {
        self.lo <= o.hi.saturating_add(1) && o.lo <= self.hi.saturating_add(1)
    }
}

/// Adds `a` to a canonical pool: per `(state, frame)` the ranges stay disjoint
/// and non-adjacent.
fn add_range(pool: &mut Vec<Rng>, mut a: Rng) {
    loop {
        let hit = pool.iter().position(|e| e.same_key(&a) && e.joins(&a));
        match hit {
            Some(i) => {
                let e = pool.swap_remove(i);
                a.lo = a.lo.min(e.lo);
                a.hi = a.hi.max(e.hi);
            }
            None => break,
        }
    }
    pool.push(a);
}

/// The interner of local-variable frames: a frame is its id everywhere else.
#[derive(Clone)]
struct Frames {
    list: Vec<Frame>,
    ids: FxMap<Frame, u32>,
    /// The id of the frame of zero slots.
    empty: u32,
}

impl Frames {
    fn new() -> Self {
        let mut f = Frames {
            list: Vec::new(),
            ids: FxMap::default(),
            empty: 0,
        };
        f.empty = f.intern_owned(Vec::new());
        f
    }

    fn len(&self) -> usize {
        self.list.len()
    }

    fn get(&self, id: u32) -> &Frame {
        &self.list[id as usize]
    }

    fn intern(&mut self, f: &[Option<i64>]) -> u32 {
        if f.is_empty() {
            return self.empty;
        }
        if let Some(&id) = self.ids.get(f) {
            return id;
        }
        self.intern_owned(f.to_vec())
    }

    fn intern_owned(&mut self, f: Frame) -> u32 {
        if let Some(&id) = self.ids.get(&f) {
            return id;
        }
        let id = self.list.len() as u32;
        self.list.push(f.clone());
        self.ids.insert(f, id);
        id
    }
}

/// The search state of one `(entry, start, frame)`.
#[derive(Clone)]
struct Seq {
    /// Every tick below this has been processed.
    processed: u64,
    /// The configurations alive at `processed` and later.
    pool: Vec<Rng>,
    /// The matches that ended at a real tick below `processed`, by end tick
    /// (ascending), each tick's frames sorted and distinct.
    matches: Vec<(u64, u32)>,
    /// A weak state: the first `n` such that `w^{start..n-1} ⊤^ω` has no strong
    /// match, or [`INF`] while there is none below `processed`.
    false_at: u64,
    /// A weak state that has matched at a real tick: every cut holds from now on,
    /// so the search stops.
    done: bool,
    /// An error was met: this state is never used again.
    poisoned: bool,
}

/// What a tail search is asked for.
#[derive(Clone, Copy, PartialEq, Eq, Hash, Debug)]
enum Want {
    /// Whether any match ends on the tail.
    Exists,
    /// Every match that ends on the tail.
    All,
    /// For a `⊥` tail, whether every longer cut (`⊥^k` then `⊤`, `1 <= k <=
    /// span + 1`) of a weak sequence has a match.
    ExtraCuts,
    /// [`Want::ExtraCuts`] without the early exit at the first cut that fails:
    /// what the reference runs when every cut has a match already (`exact`).
    ExtraCutsAll,
}

/// The memo key of a tail search.
#[derive(Clone, PartialEq, Eq, Hash)]
struct MemoKey {
    /// The frontier relative to the tail's first tick, sorted.
    sig: Vec<(u32, u32, u64, u64)>,
    /// How many `⊥` letters precede the tail proper.
    k: u32,
    top: bool,
    want: Want,
}

#[derive(Clone)]
enum Found {
    Bool(bool),
    /// `(offset from the tail's first tick, frame)`, ascending by offset.
    List(Vec<(u32, u32)>),
}

/// The part of the accelerator that is not per-sequence state (kept apart so a
/// search state can be borrowed from the map while this is used).
#[derive(Clone)]
struct Core {
    frames: Frames,
    memo: FxMap<MemoKey, Found>,
    span: u32,
    /// The automaton has a `LocalVarStep`, the one edge that can fail on a
    /// letter tick: never skip a tail search the reference would run.
    exact: bool,
    stack: Vec<(u32, u32)>,
    seen: FxSet<(u32, u32)>,
    adds: Vec<Rng>,
    hits: Vec<u32>,
    /// The signature buffer [`Core::tail`] builds each memo key in; a memo hit
    /// hands it back, so only a miss allocates.
    sig_buf: Vec<(u32, u32, u64, u64)>,
}

/// The guard leaf of a one-letter Boolean sequence from `entry`: one edge
/// `guard / Epsilon` into a state whose only edge is a `Match` (16.9.1: a lone
/// Boolean expression as a sequence). Such a sequence matches at its start tick
/// exactly when the leaf holds there, which needs no search state.
fn one_letter_guard(au: &Automaton, entry: ThreadStateId) -> Option<LeafId> {
    let [edge] = au.states[entry.0 as usize].edges.as_slice() else {
        return None;
    };
    let guard = edge.guard?;
    if !matches!(edge.label, Transition::Epsilon) {
        return None;
    }
    let [end] = au.states[edge.target.0 as usize].edges.as_slice() else {
        return None;
    };
    (end.guard.is_none() && matches!(end.label, Transition::Match { .. })).then_some(guard)
}

type Real<'a> = Option<(&'a dyn PropEnv, u64)>;

impl Core {
    /// Processes tick `t` over `pool` (every range with `lo == t` is alive now,
    /// and consumed; the ranges the tick creates are merged in). Returns whether
    /// a match ended on it, pushing `(t, frame)` per distinct matching frame
    /// onto `out`. `real` is the environment of a real tick (`None`: the tick is
    /// the letter `letter`).
    fn process_tick(
        &mut self,
        au: &Automaton,
        real: Real<'_>,
        letter: Option<bool>,
        t: u64,
        pool: &mut Vec<Rng>,
        out: &mut Vec<(u64, u32)>,
    ) -> Result<bool, ()> {
        self.stack.clear();
        self.seen.clear();
        self.adds.clear();
        self.hits.clear();
        for r in pool.iter_mut() {
            debug_assert!(r.lo >= t);
            if r.lo == t {
                self.stack.push((r.state, r.frame));
                r.lo += 1;
            }
        }
        pool.retain(|r| r.lo <= r.hi);
        while let Some((s, f)) = self.stack.pop() {
            if !self.seen.insert((s, f)) {
                continue;
            }
            for edge in &au.states[s as usize].edges {
                if let Some(g) = edge.guard {
                    let holds = match (letter, real) {
                        (Some(top), _) => top,
                        (None, Some((env, base))) => {
                            env.value(g, (t - base) as u32, self.frames.get(f).as_slice())
                                .map_err(|_| ())?
                                != 0
                        }
                        (None, None) => return Err(()),
                    };
                    if !holds {
                        continue;
                    }
                }
                let target = edge.target.0;
                match &edge.label {
                    Transition::Epsilon => self.stack.push((target, f)),
                    Transition::Delay { min, max } => {
                        let hi = match max {
                            Some(m) => t + u64::from(*m),
                            None => INF,
                        };
                        if *min == 0 {
                            self.stack.push((target, f));
                            if hi > t {
                                self.adds.push(Rng {
                                    state: target,
                                    frame: f,
                                    lo: t + 1,
                                    hi,
                                });
                            }
                        } else {
                            let lo = t + u64::from(*min);
                            if lo <= hi {
                                self.adds.push(Rng {
                                    state: target,
                                    frame: f,
                                    lo,
                                    hi,
                                });
                            }
                        }
                    }
                    Transition::Match { .. } => self.hits.push(f),
                    Transition::LocalVarWrite { var, value } => {
                        let raw = match (letter, real) {
                            (Some(_), _) => 0,
                            (None, Some((env, base))) => env
                                .value(*value, (t - base) as u32, self.frames.get(f).as_slice())
                                .map_err(|_| ())?,
                            (None, None) => return Err(()),
                        };
                        let v = au.local_var(*var).cast(raw);
                        let mut f2 = self.frames.get(f).clone();
                        f2[var.0 as usize] = Some(v);
                        let id = self.frames.intern_owned(f2);
                        self.stack.push((target, id));
                    }
                    Transition::LocalVarCopy { dst, src } => {
                        let src_frame = self.frames.get(f);
                        let mut f2 = src_frame.clone();
                        // Wide variables copy limb by limb with extension/truncation
                        // (`wide::copy_local`), the same code the reference trace runs.
                        super::wide::copy_local(
                            &mut f2,
                            *dst,
                            au.local_var(*dst),
                            src_frame,
                            *src,
                            au.local_var(*src),
                        );
                        let id = self.frames.intern_owned(f2);
                        self.stack.push((target, id));
                    }
                    Transition::LocalVarStep { var, delta } => {
                        let decl = au.local_var(*var);
                        let mut f2 = self.frames.get(f).clone();
                        if decl.is_wide() {
                            super::wide::step_local(&mut f2, *var, decl, *delta).ok_or(())?;
                        } else {
                            let cur = read_local(self.frames.get(f), *var).map_err(|_| ())?;
                            f2[var.0 as usize] = Some(decl.cast(cur.wrapping_add(*delta)));
                        }
                        let id = self.frames.intern_owned(f2);
                        self.stack.push((target, id));
                    }
                    // Eligibility excludes every other edge.
                    _ => return Err(()),
                }
            }
        }
        // Drain, not `take`: the buffer (and its capacity) stays for the next tick.
        let mut adds = std::mem::take(&mut self.adds);
        for a in adds.drain(..) {
            add_range(pool, a);
        }
        self.adds = adds;
        let hit = !self.hits.is_empty();
        if hit {
            self.hits.sort_unstable();
            self.hits.dedup();
            out.extend(self.hits.iter().map(|&f| (t, f)));
        }
        Ok(hit)
    }

    /// The matches of a tail search from the frontier `pool` at tick `r`, over the
    /// letters `⊥^k` then `top` forever, to the horizon `r + k + span + 1`.
    /// `exists` stops at the first match.
    fn tail_run(
        &mut self,
        au: &Automaton,
        pool: &[Rng],
        r: u64,
        k: u32,
        top: bool,
        exists: bool,
    ) -> Result<Found, ()> {
        let h = r + u64::from(k) + u64::from(self.span) + 1;
        let mut pool: Vec<Rng> = pool.iter().filter(|x| x.lo < h).copied().collect();
        let mut found: Vec<(u64, u32)> = Vec::new();
        let stop_early = exists && !self.exact;
        let mut any = false;
        let mut t = r;
        while let Some(next) = pool.iter().map(|x| x.lo).min() {
            t = t.max(next);
            if t >= h {
                break;
            }
            let letter = if t - r < u64::from(k) { false } else { top };
            let hit = self.process_tick(au, None, Some(letter), t, &mut pool, &mut found)?;
            if hit {
                any = true;
                if stop_early {
                    return Ok(Found::Bool(true));
                }
            }
            t += 1;
        }
        if exists {
            return Ok(Found::Bool(any));
        }
        Ok(Found::List(
            found
                .into_iter()
                .map(|(t, f)| ((t - r) as u32, f))
                .collect(),
        ))
    }

    /// [`Self::tail_run`], memoized by the frontier's signature.
    fn tail(
        &mut self,
        au: &Automaton,
        pool: &[Rng],
        r: u64,
        k: u32,
        top: bool,
        want: Want,
    ) -> Result<Found, ()> {
        if pool.is_empty() {
            return Ok(match want {
                Want::All => Found::List(Vec::new()),
                Want::Exists => Found::Bool(false),
                // No frontier: no cut has a match.
                Want::ExtraCuts | Want::ExtraCutsAll => Found::Bool(false),
            });
        }
        let h = r + u64::from(k) + u64::from(self.span) + 1;
        let mut sig = std::mem::take(&mut self.sig_buf);
        sig.clear();
        sig.extend(
            pool.iter()
                .filter(|x| x.lo < h)
                .map(|x| (x.state, x.frame, x.lo - r, x.hi.min(h - 1) - r)),
        );
        sig.sort_unstable();
        let key = MemoKey { sig, k, top, want };
        if let Some(v) = self.memo.get(&key) {
            let v = v.clone();
            self.sig_buf = key.sig;
            return Ok(v);
        }
        let res = match want {
            Want::Exists => self.tail_run(au, pool, r, k, top, true)?,
            Want::All => self.tail_run(au, pool, r, k, top, false)?,
            Want::ExtraCuts | Want::ExtraCutsAll => {
                let mut all = true;
                for kk in 1..=self.span + 1 {
                    match self.tail_run(au, pool, r, kk, true, true)? {
                        Found::Bool(true) => {}
                        _ => {
                            all = false;
                            if want == Want::ExtraCuts {
                                break;
                            }
                        }
                    }
                }
                Found::Bool(all)
            }
        };
        if self.memo.len() >= MAX_MEMO {
            self.memo.clear();
        }
        self.memo.insert(key, res.clone());
        Ok(res)
    }

    /// Advances a (non-weak) state to tick `to`.
    fn advance(
        &mut self,
        au: &Automaton,
        real: (&dyn PropEnv, u64),
        seq: &mut Seq,
        to: u64,
    ) -> Result<(), ()> {
        while seq.processed < to {
            let Some(next) = seq.pool.iter().map(|x| x.lo).min() else {
                seq.processed = to;
                break;
            };
            if next > seq.processed {
                seq.processed = next.min(to);
                continue;
            }
            let t = seq.processed;
            self.process_tick(au, Some(real), None, t, &mut seq.pool, &mut seq.matches)?;
            seq.processed = t + 1;
        }
        Ok(())
    }

    /// Advances a weak state to tick `to`, stopping at the first cut that has no
    /// match.
    fn advance_weak(
        &mut self,
        au: &Automaton,
        real: (&dyn PropEnv, u64),
        seq: &mut Seq,
        to: u64,
    ) -> Result<(), ()> {
        while seq.processed < to && seq.false_at == INF && !seq.done {
            let t = seq.processed;
            self.process_tick(au, Some(real), None, t, &mut seq.pool, &mut seq.matches)?;
            seq.processed = t + 1;
            let n = t + 1;
            let has = !seq.matches.is_empty();
            if has && !self.exact {
                seq.done = true;
                seq.pool.clear();
                seq.processed = to;
                break;
            }
            let ran = if seq.pool.is_empty() {
                false
            } else {
                matches!(
                    self.tail(au, &seq.pool, n, 0, true, Want::Exists)?,
                    Found::Bool(true)
                )
            };
            if !has && !ran {
                seq.false_at = n;
            }
        }
        Ok(())
    }
}

/// The incremental sequence evaluator of one assertion.
#[derive(Clone)]
pub struct Accel {
    /// The absolute index of the window's first position.
    base: u64,
    off: bool,
    seqs: FxMap<(u32, u64, u32, bool), Seq>,
    by_start: ByStart,
    core: Core,
    /// Per property node, how many ticks past a start its verdict can look (`None`:
    /// unboundedly far), see [`reach_table`].
    reach: Vec<Option<u32>>,
    /// Per property node, the verdicts that no later sample can change, see
    /// [`Fin`]. Empty when [`Self::memo_ok`] is not.
    fins: Vec<Fin>,
    /// Whether verdicts of one tick can be shared across attempts, see
    /// [`Accel::new`].
    memo_ok: bool,
}

/// The settled verdicts of one property node `p` (the operand of an `always`,
/// `eventually` or `until`).
///
/// A verdict `sat(p, t)` of a node whose lookahead is `R` ticks reads only the
/// samples `t..=t+R`; once `t + R` is a real tick of the window it is the same on
/// every word, whatever the tail or the length, so it can be computed once and
/// then every attempt that passes over `t` reads it back instead of evaluating
/// `p` there again. The ticks are settled in order (`next` is the first that is
/// not), and only the verdict the operators ask for is kept: the first FALSE tick
/// at or after a start decides an `always`, the first TRUE one an `eventually`.
#[derive(Clone, Default)]
struct Fin {
    /// Absolute ticks below `next` (and from the window's base) are settled.
    next: u64,
    /// The verdict of tick `next` is an error (it fails the same way every time
    /// it is asked): nothing is settled past it.
    blocked: bool,
    keep_ones: bool,
    keep_zeros: bool,
    ones: BTreeSet<u64>,
    zeros: BTreeSet<u64>,
}

impl Fin {
    fn evict(&mut self, base: u64) {
        if self.next < base {
            self.next = base;
            self.blocked = false;
        }
        if self.ones.first().is_some_and(|&t| t < base) {
            self.ones = self.ones.split_off(&base);
        }
        if self.zeros.first().is_some_and(|&t| t < base) {
            self.zeros = self.zeros.split_off(&base);
        }
    }
}

/// How many ticks past its start the longest simple path of the sequence entered
/// at `entry` can span, plus one; `None` when the automaton has a cycle or an
/// unbounded delay on a path from `entry` (a search then goes on as long as the
/// word does).
fn seq_reach(au: &Automaton, entry: u32) -> Option<u32> {
    let n = au.states.len();
    let mut color = vec![0u8; n];
    let mut best = vec![0u32; n];
    let mut stack = vec![(entry as usize, 0usize)];
    *color.get_mut(entry as usize)? = 1;
    while let Some(&(s, i)) = stack.last() {
        let edges = &au.states[s].edges;
        if let Some(e) = edges.get(i) {
            stack.last_mut()?.1 += 1;
            if matches!(e.label, Transition::Match { .. }) {
                // A match ends the thread; its target is never entered.
                continue;
            }
            let t = e.target.0 as usize;
            match *color.get(t)? {
                1 => return None,
                0 => {
                    color[t] = 1;
                    stack.push((t, 0));
                }
                _ => {}
            }
        } else {
            let mut longest = 0u32;
            for e in edges {
                let w = match e.label {
                    Transition::Match { .. } => continue,
                    Transition::Delay { min, max } => max?.max(min),
                    _ => 0,
                };
                longest = longest.max(w.checked_add(best[e.target.0 as usize])?);
            }
            if longest > MAX_REACH {
                return None;
            }
            best[s] = longest;
            color[s] = 2;
            stack.pop();
        }
    }
    Some(best[entry as usize] + 1)
}

/// The most ticks past a start a verdict may look for the node to be memoized.
const MAX_REACH: u32 = 1 << 16;

/// The lookahead of every property node (`None`: unbounded, or not modelled): an
/// upper bound on how far past its start tick `sat` of the node reads. The
/// operators' own arithmetic is the reference evaluator's: a nonoverlapped
/// implication's consequent starts one tick after the end point, `nexttime [n]`
/// moves `n` ticks, `always`/`eventually [lo:hi]` reach `hi` ticks.
fn reach_table(ir: &PropertyIr) -> Vec<Option<u32>> {
    let au = &ir.automaton;
    let mut seqs: FxMap<u32, Option<u32>> = FxMap::default();
    let mut out: Vec<Option<u32>> = Vec::with_capacity(ir.props.len());
    for prop in &ir.props {
        let get = |out: &[Option<u32>], id: PropId| out.get(id.0 as usize).copied().flatten();
        let mut seq = |entry: ThreadStateId| {
            *seqs
                .entry(entry.0)
                .or_insert_with(|| seq_reach(au, entry.0))
        };
        let r = match prop {
            Prop::Seq { seq: s, .. } => seq(s.entry),
            Prop::Not(p) | Prop::Clocked { p, .. } => get(&out, *p),
            Prop::And(a, b) | Prop::Or(a, b) => {
                get(&out, *a).zip(get(&out, *b)).map(|(a, b)| a.max(b))
            }
            Prop::If { then, els, .. } => {
                let e = els.map_or(Some(0), |e| get(&out, e));
                get(&out, *then).zip(e).map(|(a, b)| a.max(b))
            }
            Prop::Case { arms, default, .. } => {
                let mut r = default.map_or(Some(0), |d| get(&out, d));
                for arm in arms {
                    r = r.zip(get(&out, arm.body)).map(|(a, b)| a.max(b));
                }
                r
            }
            Prop::Implication {
                ante,
                cons,
                overlapped,
            } => seq(ante.entry)
                .zip(get(&out, *cons))
                .map(|(a, c)| a.saturating_add(c).saturating_add(u32::from(!*overlapped))),
            Prop::Nexttime { p, n, .. } => get(&out, *p).map(|r| r.saturating_add(*n)),
            Prop::Always { p, hi, .. } | Prop::Eventually { p, hi, .. } => {
                hi.zip(get(&out, *p)).map(|(h, r)| h.saturating_add(r))
            }
            Prop::Until { .. } | Prop::Abort { .. } | Prop::Let { .. } | Prop::Call { .. } => None,
        };
        out.push(r.filter(|&r| r <= MAX_REACH));
    }
    out
}

/// The `Σ delay bound` bound on how many ticks a simple path of the automaton
/// can span, as [`super::property::Evaluator`] computes it.
pub fn automaton_span(au: &Automaton) -> u32 {
    1 + au
        .states
        .iter()
        .flat_map(|s| &s.edges)
        .map(|e| match e.label {
            Transition::Delay { min, max } => max.unwrap_or(min).max(1),
            _ => 1,
        })
        .sum::<u32>()
}

impl Accel {
    /// The accelerator for `ir`, or `None` when it has a shape the accelerator
    /// does not model (see the module docs).
    ///
    /// `locals_read`: some leaf reads a local variable, which makes evaluating
    /// it fallible (an unassigned read), so the accelerator then never skips work
    /// the reference does (`exact`).
    pub fn new(
        ir: &PropertyIr,
        n_clocks: usize,
        has_calls: bool,
        locals_read: bool,
    ) -> Option<Accel> {
        let au = &ir.automaton;
        if n_clocks > 1
            || has_calls
            || !au.end_points.is_empty()
            || au.first_match_groups != 0
            || ir
                .props
                .iter()
                .any(|p| matches!(p, Prop::Abort { .. } | Prop::Call { .. }))
        {
            return None;
        }
        let mut exact = locals_read;
        let mut reads = |l: LeafId| Some(l) == ir.disable;
        for e in au.states.iter().flat_map(|s| &s.edges) {
            if e.guard.is_some_and(&mut reads) {
                return None;
            }
            match &e.label {
                Transition::Epsilon
                | Transition::Delay { .. }
                | Transition::Match { .. }
                | Transition::LocalVarCopy { .. } => {}
                Transition::LocalVarWrite { value, .. } => {
                    if reads(*value) {
                        return None;
                    }
                }
                Transition::LocalVarStep { .. } => exact = true,
                _ => return None,
            }
        }
        // A settled verdict must not depend on anything that changes under a
        // position: the `disable iff` condition's current value does (`If`/`Case`
        // may read it as a plain leaf), and a local variable's value is a
        // property of the thread, not of the tick (`exact`).
        let reads_disable = ir.props.iter().any(|p| match p {
            Prop::If { cond, .. } => reads(*cond),
            Prop::Case { selector, arms, .. } => {
                reads(*selector) || arms.iter().any(|a| a.labels.iter().any(|&l| reads(l)))
            }
            _ => false,
        });
        let memo_ok = !exact && !reads_disable;
        let mut fins = Vec::new();
        if memo_ok {
            fins.resize_with(ir.props.len(), Fin::default);
            for p in &ir.props {
                match p {
                    Prop::Always { p, .. } => fins[p.0 as usize].keep_zeros = true,
                    Prop::Eventually { p, .. } => fins[p.0 as usize].keep_ones = true,
                    Prop::Until { p, q, .. } => {
                        fins[p.0 as usize].keep_zeros = true;
                        fins[q.0 as usize].keep_ones = true;
                    }
                    _ => {}
                }
            }
        }
        Some(Accel {
            reach: if memo_ok { reach_table(ir) } else { Vec::new() },
            fins,
            memo_ok,
            base: 0,
            off: false,
            seqs: FxMap::default(),
            by_start: BTreeMap::new(),
            core: Core {
                frames: Frames::new(),
                memo: FxMap::default(),
                span: automaton_span(au),
                exact,
                stack: Vec::new(),
                seen: FxSet::default(),
                adds: Vec::new(),
                hits: Vec::new(),
                sig_buf: Vec::new(),
            },
        })
    }

    /// The absolute index of the first position of the window the next queries
    /// are over.
    pub fn set_base(&mut self, base: u64) {
        self.base = base;
    }

    /// Forgets the searches that started before absolute position `base`.
    pub fn evict_before(&mut self, base: u64) {
        for fin in &mut self.fins {
            fin.evict(base);
        }
        if self.by_start.is_empty() || self.by_start.keys().next().is_none_or(|&s| s >= base) {
            return;
        }
        // Pops the old starts one by one: no split-off map is built per trim.
        while let Some(old) = self.by_start.first_entry()
            && *old.key() < base
        {
            for key in old.remove() {
                self.seqs.remove(&key);
            }
        }
    }

    /// The absolute index of the window's first position.
    pub fn base(&self) -> u64 {
        self.base
    }

    /// How many ticks past a start the verdict of `id` can look, when the verdicts
    /// of `id` can be settled and shared across attempts (see [`Fin`]); `None`
    /// when they cannot.
    pub fn final_reach(&self, id: PropId) -> Option<u32> {
        if self.off || !self.memo_ok {
            return None;
        }
        self.reach.get(id.0 as usize).copied().flatten()
    }

    /// The first absolute tick whose verdict of `id` is not settled yet, and
    /// whether settling stopped there (an error): the settled ticks are
    /// `base..next`.
    pub fn final_next(&mut self, id: PropId) -> (u64, bool) {
        let base = self.base;
        let fin = &mut self.fins[id.0 as usize];
        if fin.next < base {
            fin.next = base;
            fin.blocked = false;
        }
        (fin.next, fin.blocked)
    }

    /// Settles tick `at` (which must be [`Self::final_next`]) of `id`: its verdict,
    /// or `None` when evaluating it is an error.
    pub fn final_record(&mut self, id: PropId, at: u64, verdict: Option<bool>) {
        let fin = &mut self.fins[id.0 as usize];
        debug_assert_eq!(fin.next, at);
        match verdict {
            Some(true) => {
                if fin.keep_ones {
                    fin.ones.insert(at);
                }
            }
            Some(false) => {
                if fin.keep_zeros {
                    fin.zeros.insert(at);
                }
            }
            None => {
                fin.blocked = true;
                return;
            }
        }
        fin.next = at + 1;
    }

    /// The first settled tick of `id` at or after `from` whose verdict is `v`
    /// (only the verdicts the operators ask for are kept: false for the operand
    /// of an `always` or the left of an `until`, true for `eventually` and the
    /// right of an `until`).
    pub fn final_first(&self, id: PropId, v: bool, from: u64) -> Option<u64> {
        let fin = &self.fins[id.0 as usize];
        let set = if v { &fin.ones } else { &fin.zeros };
        set.range(from..).next().copied()
    }

    fn disable(&mut self) {
        self.off = true;
        self.seqs.clear();
        self.by_start.clear();
        for fin in &mut self.fins {
            fin.ones.clear();
            fin.zeros.clear();
        }
        self.core.memo.clear();
        self.core.frames = Frames::new();
    }

    /// Common checks: `(real tick (absolute), start tick (absolute), frame id)`.
    fn prep(
        &mut self,
        env: &dyn PropEnv,
        real: u32,
        pos: u32,
        frame: &Frame,
    ) -> Option<(u64, u64, u32)> {
        if self.off || pos > real || env.timeline().is_some() {
            return None;
        }
        if self.core.frames.len() > MAX_FRAMES {
            self.disable();
            return None;
        }
        let fid = self.core.frames.intern(frame);
        Some((self.base + u64::from(real), self.base + u64::from(pos), fid))
    }

    /// The search state of `(entry, start, fid)`, advanced to `r`; `None` when
    /// it cannot be (poisoned, or already past `r`, or an error).
    #[allow(clippy::too_many_arguments)]
    fn state<'a>(
        seqs: &'a mut FxMap<(u32, u64, u32, bool), Seq>,
        by_start: &mut ByStart,
        core: &mut Core,
        au: &Automaton,
        env: &dyn PropEnv,
        base: u64,
        key: (u32, u64, u32, bool),
        r: u64,
    ) -> Option<&'a mut Seq> {
        let (entry, start, fid, weak) = key;
        let seq = seqs.entry(key).or_insert_with(|| {
            by_start.entry(start).or_default().push(key);
            Seq {
                processed: start,
                pool: vec![Rng {
                    state: entry,
                    frame: fid,
                    lo: start,
                    hi: start,
                }],
                matches: Vec::new(),
                false_at: INF,
                done: false,
                poisoned: false,
            }
        });
        if seq.poisoned || seq.processed > r {
            return None;
        }
        let res = if weak {
            core.advance_weak(au, (env, base), seq, r)
        } else {
            core.advance(au, (env, base), seq, r)
        };
        if res.is_err() {
            seq.poisoned = true;
            return None;
        }
        Some(seq)
    }

    /// Every nonempty match of the sequence starting at `entry` at position
    /// `pos` with `frame`, on the word of `real` samples and the tail `top`: what
    /// `Evaluator::matches` returns, ascending by `(end tick, frame)`.
    #[allow(clippy::too_many_arguments)]
    pub fn matches(
        &mut self,
        au: &Automaton,
        env: &dyn PropEnv,
        entry: ThreadStateId,
        real: u32,
        top: bool,
        pos: u32,
        frame: &Frame,
    ) -> Option<Matches> {
        let (r, start, fid) = self.prep(env, real, pos, frame)?;
        if start < r
            && let Some(g) = one_letter_guard(au, entry)
        {
            let held = env.value(g, pos, frame.as_slice()).ok()? != 0;
            let mut one = Matches::new();
            if held {
                one.push((pos, frame.clone()));
            }
            return Some(one);
        }
        let mut all: Vec<(u64, u32)>;
        if start == r {
            let pool = [Rng {
                state: entry.0,
                frame: fid,
                lo: r,
                hi: r,
            }];
            let found = self.core.tail(au, &pool, r, 0, top, Want::All).ok()?;
            let Found::List(l) = found else { return None };
            all = l.into_iter().map(|(o, f)| (r + u64::from(o), f)).collect();
        } else {
            let key = (entry.0, start, fid, false);
            let seq = Self::state(
                &mut self.seqs,
                &mut self.by_start,
                &mut self.core,
                au,
                env,
                self.base,
                key,
                r,
            )?;
            let found = self.core.tail(au, &seq.pool, r, 0, top, Want::All).ok()?;
            let Found::List(l) = found else { return None };
            all = seq.matches.clone();
            all.extend(l.into_iter().map(|(o, f)| (r + u64::from(o), f)));
        }
        let frames = &self.core.frames;
        all.sort_unstable_by(|a, b| {
            a.0.cmp(&b.0)
                .then_with(|| frames.get(a.1).cmp(frames.get(b.1)))
        });
        all.dedup();
        Some(
            all.into_iter()
                .map(|(e, f)| ((e - self.base) as u32, frames.get(f).clone()))
                .collect(),
        )
    }

    /// Whether the sequence has a match at all (`strong(seq)`).
    #[allow(clippy::too_many_arguments)]
    pub fn strong(
        &mut self,
        au: &Automaton,
        env: &dyn PropEnv,
        entry: ThreadStateId,
        real: u32,
        top: bool,
        pos: u32,
        frame: &Frame,
    ) -> Option<bool> {
        let (r, start, fid) = self.prep(env, real, pos, frame)?;
        if start < r
            && let Some(g) = one_letter_guard(au, entry)
        {
            return Some(env.value(g, pos, frame.as_slice()).ok()? != 0);
        }
        if start == r {
            let pool = [Rng {
                state: entry.0,
                frame: fid,
                lo: r,
                hi: r,
            }];
            return match self.core.tail(au, &pool, r, 0, top, Want::Exists).ok()? {
                Found::Bool(b) => Some(b),
                Found::List(_) => None,
            };
        }
        let key = (entry.0, start, fid, false);
        let seq = Self::state(
            &mut self.seqs,
            &mut self.by_start,
            &mut self.core,
            au,
            env,
            self.base,
            key,
            r,
        )?;
        let has = !seq.matches.is_empty();
        if has && !self.core.exact {
            return Some(true);
        }
        match self
            .core
            .tail(au, &seq.pool, r, 0, top, Want::Exists)
            .ok()?
        {
            Found::Bool(b) => Some(has || b),
            Found::List(_) => None,
        }
    }

    /// `weak(seq)` from `pos` (F.5.3.1): every cut of the word, completed with
    /// `⊤`, has a match.
    #[allow(clippy::too_many_arguments)]
    pub fn weak(
        &mut self,
        au: &Automaton,
        env: &dyn PropEnv,
        entry: ThreadStateId,
        real: u32,
        top: bool,
        pos: u32,
        frame: &Frame,
    ) -> Option<bool> {
        let (r, start, fid) = self.prep(env, real, pos, frame)?;
        if start == r {
            let pool = [Rng {
                state: entry.0,
                frame: fid,
                lo: r,
                hi: r,
            }];
            let want = if top { Want::Exists } else { Want::ExtraCuts };
            return match self.core.tail(au, &pool, r, 0, true, want).ok()? {
                Found::Bool(b) => Some(b),
                Found::List(_) => None,
            };
        }
        let key = (entry.0, start, fid, true);
        let seq = Self::state(
            &mut self.seqs,
            &mut self.by_start,
            &mut self.core,
            au,
            env,
            self.base,
            key,
            r,
        )?;
        if seq.false_at <= r {
            return Some(false);
        }
        if top {
            return Some(true);
        }
        let has = !seq.matches.is_empty() || seq.done;
        if has && !self.core.exact {
            return Some(true);
        }
        // Every cut has the real match, so the reference runs them all.
        let want = if has {
            Want::ExtraCutsAll
        } else {
            Want::ExtraCuts
        };
        match self.core.tail(au, &seq.pool, r, 0, true, want).ok()? {
            Found::Bool(b) => Some(has || b),
            Found::List(_) => None,
        }
    }
}