vj_sim/sva/

property.rs

//! SV-B (`docs/superpowers/plans/2026-10-03-sva.md` T19-T26): the property
//! layer over T9-T18's sequence automata, and a reference evaluator for it --
//! the oracle every property operator is tested against, as [`super::trace`] is
//! for sequences. The runtime engine (T29) is a separate, incremental
//! implementation of the same contract; this one evaluates the definitions of
//! IEEE 1800-2023 Annex F.5 and F.7 as literally as it can, favouring being
//! obviously right over being fast, and is never on a simulation path.
//!
//! A [`PropertyIr`] is a DAG of [`Prop`] nodes over ONE shared sequence
//! [`Automaton`]: every sequence of the property (an antecedent, a `strong(...)`
//! operand, a bare sequence property) is an entry state of that automaton and
//! they share its local-variable slot table, so a frame carried out of an
//! antecedent match is valid for the consequent's sequences. Like
//! [`super::ir`] this module has no `sv-lang` dependency.
//!
//! # Semantics
//!
//! Satisfaction is over the infinite words of F.5.3: a finite trace of `len`
//! samples completed by `⊤^ω` is the WEAK verdict (nothing has failed yet) and by
//! `⊥^ω` the STRONG one (everything still owed has failed), see
//! [`TailWord`]. [`Evaluator::verdict`] returns both. The relations are
//! implemented as Annex F states them:
//!
//! - `strong(R)`: some NONEMPTY match of `R` from the start point.
//!   `weak(R)`: for every `j`, the first `j` letters followed by `⊤^ω` strongly
//!   satisfy `R` (no finite prefix witnesses the inability to match).
//! - `not P` holds on `w` iff `P` does not hold on the dual word `w̄` (every
//!   `⊤` letter `⊥` and vice versa): `not` switches strength.
//! - `P1 or P2`, `P1 and P2`: the Boolean combinations. `P1 implies P2` is
//!   `not P1 or P2` and `P1 iff P2` is `(P1 implies P2) and (P2 implies P1)`
//!   (F.3.4.3, applied by the builder).
//! - `R |-> P`: for every match of `R` from the start, `P` holds from its end
//!   tick, with the frame the matching thread ended with. `R |=> P` is
//!   `R ##1 1 |-> P`.
//! - `nexttime`, `always`, `eventually`, `until`: positions are `w^{i..}`;
//!   `s_nexttime p` is `not nexttime not p`, which on an infinite word is
//!   `nexttime p` again (nexttime is self-dual there), and likewise for the other
//!   `s_` operators of a bounded range -- the strong and weak forms differ only
//!   in the verdict they are judged at, so the evaluator keeps one rule for each
//!   pair and the builder keeps the strength for its legality checks.
//! - `accept_on(b) P`: `P` holds and no letter satisfies `b`, or for some `i`,
//!   `w_i ⊨ b` and `w^{0,i-1}⊤^ω ⊨ P` (F.5.6.1). `reject_on(b) P` is
//!   `not accept_on(b) not P`.
//! - Recursive properties (F.7): `w ⊨ π` iff `w ⊨ π[k]` for every `k`, where
//!   `π[0]` is `1'b1` and `π[k+1]` unfolds each recursive instance once. See
//!   [`Evaluator::recursion_limit`] for the bound `k` is run to.
use std::cell::{Cell, RefCell};
use std::collections::{BTreeSet, HashMap};
use std::rc::Rc;

use super::incremental::{Accel, automaton_span};
use super::ir::{AbortMode, Automaton, ClockId, LeafId, LocalVarId, ThreadStateId, Transition};
use super::trace::{CallEvent, Frame, Matches, TailWord, Timeline, TraceError, attempt_word_calls};

/// Index of a [`Prop`] in [`PropertyIr::props`].
#[derive(Clone, Copy, Debug, PartialEq, Eq, PartialOrd, Ord, Hash)]
pub struct PropId(pub u32);

/// Index of a [`PropDecl`] in [`PropertyIr::decls`].
#[derive(Clone, Copy, Debug, PartialEq, Eq, PartialOrd, Ord, Hash)]
pub struct DeclId(pub u32);

/// One sequence of the property: its entry state in the shared automaton and
/// whether it admits the empty match (16.9.2.1), which is a flag of the
/// sequence, not a path of the automaton.
///
/// `clock` is the clock the sequence STARTS on and `end_clock` the one it ends on
/// (16.13: they differ for a multiclocked sequence, `a ##1 @(c1) b`). The
/// builder stamps both from the clock flow; a single-clock property has
/// `ClockId(0)` in both.
#[derive(Clone, Copy, Debug, PartialEq, Eq)]
pub struct SeqRef {
    pub entry: ThreadStateId,
    pub admits_empty: bool,
    pub clock: ClockId,
    pub end_clock: ClockId,
}

impl SeqRef {
    /// A single-clocked sequence on the assertion's clock (`ClockId(0)`).
    pub fn single(entry: ThreadStateId, admits_empty: bool) -> Self {
        SeqRef {
            entry,
            admits_empty,
            clock: ClockId(0),
            end_clock: ClockId(0),
        }
    }
}

/// The `strong`/`weak` operator written on a sequence property (16.12.2).
#[derive(Clone, Copy, Debug, PartialEq, Eq)]
pub enum Strength {
    Strong,
    Weak,
}

/// One arm of a `case` property: the labels that select it and its property.
#[derive(Clone, Debug, PartialEq, Eq)]
pub struct CaseArm {
    pub labels: Vec<LeafId>,
    pub body: PropId,
}

/// One property operator (16.12). Operands are [`PropId`]s of nodes built before
/// this one, so the table is a DAG in topological order (a shared operand, as in
/// the `iff` expansion, is one node referenced twice).
#[derive(Clone, Debug, PartialEq, Eq)]
pub enum Prop {
    /// A sequence used as a property (16.12.2). `strength` is the explicit
    /// `strong`/`weak` operator, or `None` for a bare sequence, which is weak
    /// under `assert`/`assume` and strong under `cover` (the evaluator's
    /// `implicit_strong`).
    Seq {
        seq: SeqRef,
        strength: Option<Strength>,
    },
    /// `not p` (16.12.3).
    Not(PropId),
    /// `p1 and p2` (16.12.5).
    And(PropId, PropId),
    /// `p1 or p2` (16.12.4).
    Or(PropId, PropId),
    /// `if (cond) then [else els]` (16.12.6): `cond` is a Boolean leaf, and an
    /// absent `else` is true.
    If {
        cond: LeafId,
        then: PropId,
        els: Option<PropId>,
    },
    /// `case (selector) labels: body ... [default: body] endcase` (16.12.16): the
    /// first arm one of whose labels matches the selector is taken; no arm and no
    /// `default` is vacuously true.
    Case {
        selector: LeafId,
        arms: Vec<CaseArm>,
        default: Option<PropId>,
    },
    /// `ante |-> cons` (`overlapped`) or `ante |=> cons` (16.12.7).
    Implication {
        ante: SeqRef,
        cons: PropId,
        overlapped: bool,
    },
    /// `nexttime [n] p` / `s_nexttime [n] p` (16.12.10).
    Nexttime { p: PropId, n: u32, strong: bool },
    /// `always [lo:hi] p` / `s_always [lo:hi] p` (16.12.11): `hi == None` is `$`.
    Always {
        p: PropId,
        lo: u32,
        hi: Option<u32>,
        strong: bool,
    },
    /// `eventually [lo:hi] p` / `s_eventually [lo:hi] p` (16.12.13).
    Eventually {
        p: PropId,
        lo: u32,
        hi: Option<u32>,
        strong: bool,
    },
    /// `p until q` / `p s_until q` (16.12.12); `until_with` is built as
    /// `p until (p and q)`.
    Until { p: PropId, q: PropId, strong: bool },
    /// `accept_on`/`reject_on`/`sync_accept_on`/`sync_reject_on (cond) p`
    /// (16.12.14).
    Abort {
        cond: LeafId,
        p: PropId,
        mode: AbortMode,
    },
    /// Writes local variables at the start of `body`'s evaluation, in order, each
    /// value evaluated in the frame the earlier writes left (a property's local
    /// formals and declared locals with initialisers, 16.12.19).
    Let {
        writes: Vec<(LocalVarId, LeafId)>,
        body: PropId,
    },
    /// `@(clock) p` (16.13.2): `p` runs on `clock`, whatever clock the context
    /// had. Every operand of `p` that counts time (`nexttime`, `always`, `until`,
    /// a sequence's delays) counts ticks of `clock`.
    Clocked { clock: ClockId, p: PropId },
    /// An instance of a recursive property (16.12.17): evaluates `decl`'s body in
    /// the caller's frame with the listed slots rebound to the arguments, every
    /// one evaluated in the CALLER's frame first. Then `inits` (the instance's
    /// declared locals with initialisers, in declaration order) are written: each
    /// is evaluated in the caller's frame as the earlier `inits` left it, so that
    /// it reads the formals as the instance's actuals (which is what slang
    /// substitutes into an initialiser) and the declared locals it follows.
    Call {
        decl: DeclId,
        args: Vec<(LocalVarId, LeafId)>,
        inits: Vec<(LocalVarId, LeafId)>,
    },
}

/// A recursive property's body, entered through [`Prop::Call`].
#[derive(Clone, Debug, PartialEq, Eq)]
pub struct PropDecl {
    pub name: String,
    pub body: PropId,
}

/// A built property: the shared sequence automaton, the operator DAG and the
/// recursive declarations.
#[derive(Clone, Debug, PartialEq, Eq)]
pub struct PropertyIr {
    pub automaton: Automaton,
    pub props: Vec<Prop>,
    pub decls: Vec<PropDecl>,
    pub root: PropId,
    /// The `disable iff (cond)` of the property spec (16.12, T27): `root` is the
    /// property under it. `None` when the spec has no explicit clause. Only a
    /// top-level clause exists -- the builder rejects a nested one -- and the
    /// leaf is evaluated with CURRENT values (see [`Evaluator::attempt`]).
    pub disable: Option<LeafId>,
    /// Nodes whose 16.14.8 nonvacuity rule is not the one their shape says,
    /// because the builder expressed an operator through others (see
    /// [`NvRule`]). Empty for a hand-built property that has none.
    pub nv_rules: Vec<(PropId, NvRule)>,
}

/// An operator built from others whose nonvacuity rule (16.14.8) differs from
/// the derived shape's.
#[derive(Clone, Copy, Debug, PartialEq, Eq)]
pub enum NvRule {
    /// The [`Prop::Or`] of `not p or q` standing for `p implies q` (rule z): `p`
    /// must be true and nonvacuous, and `q` nonvacuous.
    Implies,
    /// The [`Prop::Until`] of `p until (p and q)` standing for `p until_with q`
    /// (rules x, y): only `p` can make the attempt nonvacuous.
    UntilWith,
}

impl PropertyIr {
    /// The special nonvacuity rule of node `id`, if it has one.
    pub fn nv_rule(&self, id: PropId) -> Option<NvRule> {
        self.nv_rules
            .iter()
            .find(|(p, _)| *p == id)
            .map(|(_, r)| *r)
    }

    /// Borrows `id`'s node (an id this IR's builder minted).
    pub fn prop(&self, id: PropId) -> &Prop {
        &self.props[id.0 as usize]
    }

    /// Whether the property contains a recursive instance ([`Prop::Call`]).
    pub fn is_recursive(&self) -> bool {
        self.props.iter().any(|p| matches!(p, Prop::Call { .. }))
    }
}

/// What a property's leaves are on a trace.
pub trait PropEnv {
    /// The value of `leaf` at `tick` with the thread's local-variable `frame`; a
    /// guard holds when nonzero. Called for real samples only.
    fn value(&self, leaf: LeafId, tick: u32, frame: &[Option<i64>]) -> Result<i64, TraceError>;

    /// Whether `label` selects the `case` selector at `tick`. The environment
    /// owns the comparison: 16.12.16 uses the case equality of 12.5 (`===`), under
    /// which an `x`/`z` selector matches no label that is not itself that value.
    fn case_match(
        &self,
        selector: LeafId,
        label: LeafId,
        tick: u32,
        frame: &[Option<i64>],
    ) -> Result<bool, TraceError>;

    /// The sampled value of the abort condition `leaf` at a time step STRICTLY
    /// BETWEEN tick `after` and tick `after + 1` (16.12.14: `accept_on` and
    /// `reject_on` are "evaluated at the granularity of the simulation time step",
    /// unlike the `sync_` forms). A trace that has no such steps -- the default --
    /// has none true.
    fn between(&self, _leaf: LeafId, _after: u32) -> Result<bool, TraceError> {
        Ok(false)
    }

    /// The tick lists of a multiclock property's clocks over the trace's
    /// positions (16.13), or `None` -- the default -- when every position is a
    /// tick of every clock, which is what a single-clocked property wants. With
    /// a timeline the positions are the trace's global steps and `value` is read
    /// at them; `between` is not consulted.
    fn timeline(&self) -> Option<&Timeline> {
        None
    }

    /// Local variables an attempt starts with already assigned: the values a
    /// procedural concurrent assertion captured when it was reached (16.14.6).
    fn initial_frame(&self) -> Vec<(LocalVarId, i64)> {
        Vec::new()
    }
}

/// The result of checking a property over a finite trace (F.5.3.2).
#[derive(Clone, Copy, Debug, PartialEq, Eq)]
pub enum Verdict {
    /// `w ⊭- A`: the weak verdict fails -- the property has definitely failed.
    Fails,
    /// `w ⊨- A` but `w ⊭+ A`: nothing has failed but something is still owed
    /// ("holds, but does not hold strongly", the evaluation is pending).
    Holds,
    /// `w ⊨+ A`: holds strongly.
    HoldsStrongly,
}

/// What an evaluation attempt of a property spec came to (16.12 `disable iff`).
#[derive(Clone, Copy, Debug, PartialEq, Eq)]
pub enum Disposition {
    /// The property failed (before any disabling).
    Fails,
    /// Nothing has failed and nothing is decided: the attempt is pending.
    Pending,
    /// The property holds strongly: it passed.
    Passes,
    /// The disable condition was true at some time step of the attempt while the
    /// property was still undecided: "a disabled evaluation of a property does not
    /// result in success or failure" (16.12).
    Disabled,
}

impl From<Verdict> for Disposition {
    fn from(v: Verdict) -> Self {
        match v {
            Verdict::Fails => Disposition::Fails,
            Verdict::Holds => Disposition::Pending,
            Verdict::HoldsStrongly => Disposition::Passes,
        }
    }
}

/// The evaluator: a property, the trace it is checked on and which strength a bare
/// sequence takes.
pub struct Evaluator<'a> {
    ir: &'a PropertyIr,
    env: &'a dyn PropEnv,
    implicit_strong: bool,
    /// Whether the trace is a prefix of a run that goes on (the live engine), see
    /// [`Evaluator::open_future`].
    open_future: bool,
    /// An upper bound on how many ticks any simple path of the sequence automaton
    /// can span, see [`Evaluator::horizon`].
    span: u32,
    /// The result of every [`Prop::Call`] evaluated so far, by what it depends on:
    /// the declaration, the start tick, the word, the local-variable frame the
    /// body starts with and the call depth (which decides where the unfolding is
    /// cut off). A recursive property reaches the same configuration along many
    /// paths (every match of an antecedent such as `x[->1]`, every abort point of
    /// an `accept_on` re-runs the property after it), so without this the number
    /// of evaluations grows exponentially with the depth of the unfolding.
    calls: RefCell<HashMap<CallKey, bool>>,
    /// The environment's [`Timeline`] cut to a word's real length, by that length
    /// (see [`Self::timeline_for`]).
    timelines: RefCell<HashMap<u32, Rc<Timeline>>>,
    /// Set while [`Self::calls`] collects: every sequence search then unions the
    /// subroutine calls its threads scheduled (16.11) into [`Self::call_sink`],
    /// and the operators that would stop at the first failing operand
    /// (`and`, `or`, `|->`) evaluate all of them, so the calls are those of every
    /// thread the property starts, not of the ones a verdict happened to need.
    exhaustive: Cell<bool>,
    /// Set while [`Evaluator::verdict`] decides "holds strongly": a weak sequence
    /// on the strong word then holds only once it has matched, see `weak_seq`.
    pending_until_match: Cell<bool>,
    call_sink: RefCell<Option<BTreeSet<CallEvent>>>,
    /// The live engine's incremental sequence evaluator, see
    /// [`Self::with_accel`]; `None` is the reference semantics, spelled out.
    accel: Option<&'a RefCell<Accel>>,
}

/// What the settled ticks of an `until` say, see [`Evaluator::skip_settled_until`].
enum Settled {
    Verdict(bool),
    Resume(u32),
}

/// What a [`Prop::Call`]'s result depends on, see the `calls` field of
/// [`Evaluator`].
type CallKey = (DeclId, u32, TailWord, Frame, u32, ClockId);

impl<'a> Evaluator<'a> {
    /// `implicit_strong` is whether a bare sequence property is strong (a `cover
    /// property` directive) or weak (`assert`/`assume`), 16.12.2.
    pub fn new(ir: &'a PropertyIr, env: &'a dyn PropEnv, implicit_strong: bool) -> Self {
        Self::new_with_span(ir, env, implicit_strong, automaton_span(&ir.automaton))
    }

    /// [`Self::new`] with the automaton's [`automaton_span`] already known (an
    /// engine builds one evaluator per evaluation).
    pub fn new_with_span(
        ir: &'a PropertyIr,
        env: &'a dyn PropEnv,
        implicit_strong: bool,
        span: u32,
    ) -> Self {
        Evaluator {
            ir,
            env,
            implicit_strong,
            open_future: false,
            span,
            calls: RefCell::new(HashMap::new()),
            timelines: RefCell::new(HashMap::new()),
            exhaustive: Cell::new(false),
            pending_until_match: Cell::new(false),
            call_sink: RefCell::new(None),
            accel: None,
        }
    }

    /// Answers the sequence searches of words with no explicit letters (`strong`
    /// and `weak` verdict words, which is what a live engine asks) from `accel`'s
    /// incremental state instead of replaying them. The accelerator declines
    /// what it does not model, and then the reference code below runs; the
    /// results are the reference's, which the engine's differential mode and
    /// this module's exhaustive test check.
    pub fn with_accel(mut self, accel: Option<&'a RefCell<Accel>>) -> Self {
        self.accel = accel;
        self
    }

    /// Reads the trace as a PREFIX of a run that is not over, which is what a live
    /// simulation has: the weak and strong verdicts then bracket every possible
    /// continuation, so `Fails` and `HoldsStrongly` are final and `Holds` means
    /// "undecided". Annex F's strong word `w⊥^ω` is the end of the run, where an
    /// antecedent that still needs a letter has no match and the implication is
    /// vacuously true (`a |=> b` holds strongly when `a` is the last letter). That is
    /// the right verdict for a run that ended and the wrong one for a decision
    /// taken in the middle of a run, so here an antecedent is matched on the DUAL
    /// word (`⊤` letters in the strong word, `⊥` in the weak one): it matches as
    /// eagerly as any continuation could make it in the strong word, as rarely in
    /// the weak one, and the consequent is judged on the word itself.
    pub fn open_future(mut self) -> Self {
        self.open_future = true;
        self
    }

    /// The clock the property starts on: the root context clock.
    fn root_clock(&self) -> ClockId {
        self.ir.automaton.entry_clock
    }

    /// The environment's timeline as `word` sees it: a position at or past
    /// `word.real` is a `⊤`/`⊥` letter, which is a tick of EVERY clock (see
    /// [`Timeline`]), so a word cut shorter than the trace needs the tick lists cut
    /// with it. `None` when the property is single-clocked.
    fn timeline_for(&self, word: &TailWord) -> Result<Option<Rc<Timeline>>, TraceError> {
        let Some(full) = self.env.timeline() else {
            return Ok(None);
        };
        if let Some(t) = self.timelines.borrow().get(&word.real) {
            return Ok(Some(Rc::clone(t)));
        }
        let cut = Rc::new(full.truncated(word.real));
        self.timelines
            .borrow_mut()
            .insert(word.real, Rc::clone(&cut));
        Ok(Some(cut))
    }

    /// The `k`-th tick of `dom` strictly after `from` on `word` (`k == 0`: `from`).
    fn after(&self, word: &TailWord, dom: ClockId, from: u32, k: u32) -> Result<u32, TraceError> {
        Ok(match self.timeline_for(word)? {
            Some(t) => t.kth_after(dom, from, k),
            None => from + k,
        })
    }

    /// The clock the property `id` starts on when that is evident from its own
    /// operators (a clocked sequence, `@(c) p`, `not`, an `and`/`or` whose
    /// operands agree); `fallback` otherwise.
    fn lead_clock(&self, id: PropId, fallback: ClockId) -> ClockId {
        match self.ir.prop(id) {
            Prop::Seq { seq, .. } => seq.clock,
            Prop::Clocked { clock, .. } => *clock,
            Prop::Not(p) => self.lead_clock(*p, fallback),
            Prop::Let { body, .. } => self.lead_clock(*body, fallback),
            Prop::And(a, b) | Prop::Or(a, b) => {
                let (x, y) = (self.lead_clock(*a, fallback), self.lead_clock(*b, fallback));
                if x == y { x } else { fallback }
            }
            _ => fallback,
        }
    }

    /// `pos` moved to the first tick of `dom` at or after it, folded into
    /// `extent` (every position from there on is the same letter).
    fn align(&self, word: &TailWord, dom: ClockId, pos: u32) -> Result<u32, TraceError> {
        let at = match self.timeline_for(word)? {
            Some(t) => t.next_tick(dom, pos),
            None => pos,
        };
        Ok(at.min(word.extent()))
    }

    /// The verdict of an evaluation attempt started at tick `start` of a trace of
    /// `len` samples.
    pub fn verdict(&self, len: u32, start: u32) -> Result<Verdict, TraceError> {
        let weak = self.holds(&TailWord::weak(len), start)?;
        if !weak {
            return Ok(Verdict::Fails);
        }
        self.pending_until_match.set(true);
        let strong = self.holds(&TailWord::strong(len), start);
        self.pending_until_match.set(false);
        Ok(if strong? {
            Verdict::HoldsStrongly
        } else {
            Verdict::Holds
        })
    }

    /// [`Self::verdict`] for the whole property spec, `disable iff` included
    /// (16.12): the attempt started at tick `start` of a trace of `len` samples.
    ///
    /// The disable condition is "true at anytime between the start of the attempt
    /// in the Observed region, inclusive, and the end of the evaluation attempt,
    /// inclusive". [`PropEnv::value`] of the disable leaf at tick `t` says whether
    /// it was true in the Observed region of tick `t`, and [`PropEnv::between`]
    /// whether it was true at some time step strictly between `t` and `t + 1`; both
    /// are CURRENT values (16.12: "not sampled"). Let `p` be the first such moment
    /// at or after the start; the attempt is judged on the letters before it -- the
    /// ones that came before the disabling, `w^{0,i-1}` -- as the Annex F neutral
    /// satisfaction of a top-level `disable iff` has it: failed if the weak completion of that prefix fails
    /// (the failure was decided before the disabling), passed if its strong
    /// completion holds, and DISABLED when it is neither (still pending).
    ///
    /// A condition true when the attempt starts disables it outright: Annex F
    /// excludes letter 0 from `0 < i`, but 16.12's prose is explicit that the window
    /// starts at the attempt's start, inclusive, and that is the clause that decides
    /// what an evaluation attempt is. A decided verdict is the same on every longer
    /// prefix (it does not depend on the continuation), so a disabling AFTER the
    /// property was decided changes nothing.
    pub fn attempt(&self, len: u32, start: u32) -> Result<Disposition, TraceError> {
        let Some(prefix) = self.disabling_prefix(len, start)? else {
            return Ok(self.verdict(len, start)?.into());
        };
        if prefix == start {
            return Ok(Disposition::Disabled);
        }
        Ok(match self.verdict(prefix, start)? {
            Verdict::Holds => Disposition::Disabled,
            decided => decided.into(),
        })
    }

    /// The number of letters (counted from tick 0) that precede the first moment at
    /// or after `start` the disable condition is true, see [`Self::attempt`]; `None`
    /// when there is no `disable iff` or it is never true on the `len` ticks.
    pub fn disabling_prefix(&self, len: u32, start: u32) -> Result<Option<u32>, TraceError> {
        let Some(cond) = self.ir.disable else {
            return Ok(None);
        };
        // The attempt's own captured values (16.14.6.1) are what a condition over
        // them reads; any other condition ignores the frame.
        let frame = self.initial_frame();
        for t in start..len {
            if self.env.value(cond, t, &frame)? != 0 {
                return Ok(Some(t));
            }
            if self.env.between(cond, t)? {
                return Ok(Some(t + 1));
            }
        }
        Ok(None)
    }

    /// The local-variable frame an attempt starts with: all unassigned, except
    /// the slots the environment pre-assigns ([`PropEnv::initial_frame`]).
    fn initial_frame(&self) -> Frame {
        let mut frame = vec![None; self.ir.automaton.local_vars.len()];
        for (var, value) in self.env.initial_frame() {
            frame[var.0 as usize] = Some(value);
        }
        frame
    }

    /// Whether the property holds on `word` from tick `start` (an evaluation
    /// attempt's start point), local variables unassigned save those the
    /// environment pre-assigns.
    pub fn holds(&self, word: &TailWord, start: u32) -> Result<bool, TraceError> {
        // What the environment says may differ from one call to the next.
        self.calls.borrow_mut().clear();
        let frame = self.initial_frame();
        self.sat(
            self.ir.root,
            word,
            start,
            &frame,
            0,
            self.root_clock(),
            false,
        )
    }

    /// Every nonempty match of the root sequence of a `cover sequence` (16.14.3)
    /// attempt started at tick `start`, over the `len` real samples of the trace,
    /// as `(end tick, the local-variable frame it matched with)`. Several matches
    /// may end on one tick (with different frames, or the same frame reached along
    /// different paths is one match): 16.14.3 counts every one. A match that would
    /// need a tick past the trace is not listed -- it is reported when that tick
    /// arrives. `NotASequence` for a root that is not a bare sequence.
    pub fn root_sequence_matches(&self, len: u32, start: u32) -> Result<Matches, TraceError> {
        let Prop::Seq { seq, .. } = self.ir.prop(self.ir.root) else {
            return Err(TraceError::NotASequence);
        };
        self.calls.borrow_mut().clear();
        let frame = self.initial_frame();
        self.matches(*seq, &TailWord::strong(len), start, &frame)
    }

    /// How deep a [`Prop::Call`] chain is followed (`k` of F.7's `π[k]`); an
    /// instance past it is `π[0]`, `1'b1`.
    ///
    /// Every recursive instance occurs after a positive time advance (16.12.17
    /// restriction 3), so a chain of calls advances the start tick by at least one
    /// each step, and past the trace (`extent`) every start tick is equivalent.
    /// What can still differ between two calls is which recursive declaration
    /// they enter and the local-variable arguments they pass. For a property with
    /// `c` recursive declarations and no argument that grows, the configuration
    /// `(declaration, tick clamped to extent)` repeats within `c * (extent + 1)`
    /// calls, after which the unfolding is periodic and `π[k]` no longer changes
    /// with `k` -- the limit below doubles that and adds slack. A recursion whose
    /// local arguments grow forever (a counter) has no such fixpoint; for it the
    /// verdict is that of this `k`, and the tests pin that `k` and `2k` agree on
    /// every property of the LRM's recursive examples.
    pub fn recursion_limit(&self, word: &TailWord) -> u32 {
        2 * (self.ir.decls.len() as u32).max(1) * (word.extent() + 2) + 4
    }

    /// The tick the sequence search runs to for a start tick `pos` on `word`: past
    /// the last tick that is not the constant tail, plus the longest a simple
    /// path of the automaton can span, so every distinct way a match can end has
    /// been tried.
    fn horizon(&self, word: &TailWord, pos: u32) -> u32 {
        word.extent().max(pos) + self.span + 1
    }

    /// Every nonempty match of `seq` started at `pos` with `frame`.
    fn matches(
        &self,
        seq: SeqRef,
        word: &TailWord,
        pos: u32,
        frame: &Frame,
    ) -> Result<Matches, TraceError> {
        if let Some(cell) = self.accel
            && word.mid.is_empty()
            && let Ok(mut accel) = cell.try_borrow_mut()
            && let Some(found) = accel.matches(
                &self.ir.automaton,
                self.env,
                seq.entry,
                word.real,
                word.tail_top,
                pos,
                frame,
            )
        {
            return Ok(found);
        }
        let eval = |leaf: LeafId, tick: u32, f: &[Option<i64>]| self.env.value(leaf, tick, f);
        let timeline = self.timeline_for(word)?;
        let (found, calls) = attempt_word_calls(
            &self.ir.automaton,
            seq.entry,
            frame,
            pos,
            word,
            self.horizon(word, pos),
            &eval,
            timeline.as_deref(),
            seq.clock,
        )?;
        if let Some(sink) = self.call_sink.borrow_mut().as_mut() {
            sink.extend(calls);
        }
        Ok(found.into_iter().collect())
    }

    /// Every subroutine call (16.11) a thread of the evaluation attempt started at
    /// tick `start` scheduled on the `len` samples of the trace, ascending by
    /// `(tick, call, args)`: "all subroutine calls attached to a sequence are
    /// executed at every end point of the sequence", whether or not the property
    /// those sequences are part of later holds.
    ///
    /// The attempt is judged on the letters before its `disable iff` (16.12): a
    /// call after the disabling is not the attempt's. The set depends only on
    /// the samples up to each call's own tick (a thread reaches a call edge by
    /// the letters before it), so an extension of the trace only ever ADDS
    /// calls -- which is what lets the engine report each once.
    ///
    /// Both completions of the word are run: the verdict calls the second only
    /// when the first holds, and the calls must not depend on the verdict.
    ///
    /// The calls are those the sequence searches find: they are exhaustive over
    /// `and`/`or`/`|->` operands (see [`Self::exhaustive`]), and a property that
    /// stops evaluating at a decision (`always`, `until`, ...) lists the calls of
    /// the evaluations that ran.
    pub fn scheduled_calls(&self, len: u32, start: u32) -> Result<Vec<CallEvent>, TraceError> {
        let eff = self.disabling_prefix(len, start)?.unwrap_or(len);
        *self.call_sink.borrow_mut() = Some(BTreeSet::new());
        self.exhaustive.set(true);
        let ran = self
            .holds(&TailWord::weak(eff), start)
            .and_then(|_| self.holds(&TailWord::strong(eff), start));
        self.exhaustive.set(false);
        let sink = self.call_sink.borrow_mut().take().unwrap_or_default();
        ran?;
        Ok(sink.into_iter().collect())
    }

    /// Whether a multiclock `cover sequence` attempt (16.13.1, 16.14.3) started at
    /// position `start` of a trace of `len` positions has reported every match it
    /// ever will: no thread of the root sequence can still be waiting for a
    /// position past the trace.
    ///
    /// A single-clock attempt is retired by [`Automaton::max_span`], a count of
    /// clock ticks. With several clocks the positions are the union of the clocks'
    /// ticks, and how many positions a `##N` or a clock change takes depends on the
    /// clock it waits for, so this follows the automaton on the timeline instead:
    /// the latest position each state is reachable at, taking every `##[m:n]` to its
    /// `n`-th tick and every clock change to its next tick of the new clock, guards
    /// ignored (so it only ever over-estimates). A step that needs a tick not in the
    /// trace yet, or an unbounded delay, leaves the attempt alive. `false` without
    /// a timeline (a single clock: use `max_span`).
    pub fn sequence_exhausted(&self, len: u32, start: u32) -> Result<bool, TraceError> {
        let Prop::Seq { seq, .. } = self.ir.prop(self.ir.root) else {
            return Err(TraceError::NotASequence);
        };
        let Some(tl) = self.env.timeline() else {
            return Ok(false);
        };
        let au = &self.ir.automaton;
        let first = tl.next_tick(seq.clock, start);
        let mut best: HashMap<(u32, ClockId), u32> = HashMap::new();
        let mut work = vec![((seq.entry.0, seq.clock), first)];
        while let Some(((state, dom), pos)) = work.pop() {
            if pos >= len {
                return Ok(false);
            }
            if best.get(&(state, dom)).is_some_and(|&b| b >= pos) {
                continue;
            }
            best.insert((state, dom), pos);
            for edge in &au.state(ThreadStateId(state)).edges {
                let target = edge.target.0;
                match &edge.label {
                    Transition::Delay { min, max } => {
                        let Some(max) = max else {
                            return Ok(false);
                        };
                        work.push(((target, dom), tl.kth_after(dom, pos, (*max).max(*min))));
                    }
                    Transition::ClockSync { to, strict } => {
                        let at = if *strict {
                            tl.kth_after(*to, pos, 1)
                        } else {
                            tl.next_tick(*to, pos)
                        };
                        work.push(((target, *to), at));
                    }
                    Transition::Match { .. } => {}
                    Transition::Epsilon
                    | Transition::Abort { .. }
                    | Transition::LocalVarWrite { .. }
                    | Transition::LocalVarCopy { .. }
                    | Transition::FirstMatchBegin { .. }
                    | Transition::FirstMatchEnd { .. }
                    | Transition::LocalVarStep { .. }
                    | Transition::SubroutineCall { .. }
                    | Transition::EndPoint { .. } => work.push(((target, dom), pos)),
                }
            }
        }
        Ok(true)
    }

    /// The calls (16.11) of the threads of `cover sequence`'s root sequence
    /// started at `start` (see [`Self::root_sequence_matches`]), over the `len`
    /// real samples, before the attempt's `disable iff` (16.12).
    pub fn sequence_calls(&self, len: u32, start: u32) -> Result<Vec<CallEvent>, TraceError> {
        let eff = self.disabling_prefix(len, start)?.unwrap_or(len);
        *self.call_sink.borrow_mut() = Some(BTreeSet::new());
        let ran = self.root_sequence_matches(eff, start);
        let sink = self.call_sink.borrow_mut().take().unwrap_or_default();
        ran?;
        Ok(sink.into_iter().collect())
    }

    /// A Boolean leaf at `tick`: a real sample's value, or the letter.
    fn boolean(
        &self,
        leaf: LeafId,
        word: &TailWord,
        tick: u32,
        frame: &Frame,
    ) -> Result<bool, TraceError> {
        match word.letter(tick) {
            Some(top) => Ok(top),
            None => Ok(self.env.value(leaf, tick, frame)? != 0),
        }
    }

    /// `strong(seq)` from `pos`.
    fn strong_seq(
        &self,
        seq: SeqRef,
        word: &TailWord,
        pos: u32,
        frame: &Frame,
    ) -> Result<bool, TraceError> {
        if let Some(cell) = self.accel
            && word.mid.is_empty()
            && let Ok(mut accel) = cell.try_borrow_mut()
            && let Some(found) = accel.strong(
                &self.ir.automaton,
                self.env,
                seq.entry,
                word.real,
                word.tail_top,
                pos,
                frame,
            )
        {
            return Ok(found);
        }
        Ok(!self.matches(seq, word, pos, frame)?.is_empty())
    }

    /// `weak(seq)` from `pos`: for every number of letters `n` past the start
    /// point, `w^{pos..n-1}⊤^ω` strongly satisfies `seq` (F.5.3.1).
    ///
    /// On a `⊤` tail a cut past the real and explicit letters is the word itself,
    /// so the cuts to try end there; on a `⊥` tail each longer cut adds a `⊥`
    /// letter before the `⊤`s, and a cut longer than the longest path a match can
    /// span from `pos` behaves like that one.
    fn weak_seq(
        &self,
        seq: SeqRef,
        word: &TailWord,
        pos: u32,
        frame: &Frame,
    ) -> Result<bool, TraceError> {
        // When deciding "holds strongly" (a PASS: `Evaluator::verdict`), a weak
        // sequence on the strong word (`⊥` tail, no explicit letters) holds exactly
        // when it has matched. Annex F's cuts are lenient
        // on an unbounded range: `a ##[1:$] b` over `[a]⊥^ω` is matched by every
        // cut `[a]⊥^k⊤^ω` (the `⊤` satisfies `b`), so it would hold strongly --
        // the attempt would PASS at its first tick, before `b` is ever true. The
        // LRM's own example (Table 40-3: `aundf: assert (on ##[1:$]
        // off)` "will not pass or fail") says such an attempt stays pending until
        // the sequence matches; a bounded sequence cannot tell the two apart (a
        // match needs real letters, the `⊥`s kill every Boolean), so this only
        // changes unbounded ranges, repetitions and goto/nonconsecutive forms.
        if self.pending_until_match.get() && !word.tail_top && word.mid.is_empty() {
            return self.strong_seq(seq, word, pos, frame);
        }
        if let Some(cell) = self.accel
            && word.mid.is_empty()
            && let Ok(mut accel) = cell.try_borrow_mut()
            && let Some(found) = accel.weak(
                &self.ir.automaton,
                self.env,
                seq.entry,
                word.real,
                word.tail_top,
                pos,
                frame,
            )
        {
            return Ok(found);
        }
        let ext = word.extent();
        let last = if word.tail_top {
            ext.max(pos + 1)
        } else {
            ext.max(pos) + self.span + 1
        };
        for n in pos + 1..=last {
            let cut = word.cut_then_top(n);
            if !self.strong_seq(seq, &cut, pos, frame)? {
                return Ok(false);
            }
        }
        Ok(true)
    }

    /// The position `prop` stands on when asked at `pos`, and the pending
    /// synchronization it hands on (see [`Self::sat`]'s `strict`).
    ///
    /// The pass-through operators hand the position on untouched; every other one
    /// stands on a tick of the clock it starts on. A position past `extent` is the
    /// one at it: every later tick carries the same letter.
    fn stand(
        &self,
        prop: &Prop,
        word: &TailWord,
        pos: u32,
        dom: ClockId,
        strict: bool,
    ) -> Result<(u32, bool), TraceError> {
        let through = pass_through(prop);
        let pos = if through {
            pos.min(word.extent())
        } else {
            let lead = match prop {
                Prop::Seq { seq, .. } => seq.clock,
                Prop::Implication { ante, .. } => ante.clock,
                // 16.13.7: a declaration assignment is performed at the earliest
                // tick of the body's leading clock, not of the context clock.
                Prop::Let { body, .. } => self.lead_clock(*body, dom),
                _ => dom,
            };
            if strict {
                self.after(word, lead, pos, 1)?.min(word.extent())
            } else {
                self.align(word, lead, pos)?
            }
        };
        // Only a pass-through operator hands the pending synchronization on.
        Ok((pos, strict && through))
    }

    /// The local-variable frame a [`Prop::Call`] body starts with: the caller's
    /// frame with the formals' slots rebound (every actual is evaluated in the
    /// caller's frame, before any slot is overwritten -- an actual may read the
    /// slot its own formal is about to take, `fibonacci1(b, a+b, ...)`).
    fn call_frame(
        &self,
        args: &[(LocalVarId, LeafId)],
        inits: &[(LocalVarId, LeafId)],
        word: &TailWord,
        pos: u32,
        frame: &Frame,
    ) -> Result<Frame, TraceError> {
        let mut f: Frame = frame.clone();
        for (var, leaf) in args {
            let raw = if word.letter(pos).is_some() {
                0
            } else {
                self.env.value(*leaf, pos, frame)?
            };
            f[var.0 as usize] = Some(self.ir.automaton.local_var(*var).cast(raw));
        }
        let mut seen: Frame = frame.clone();
        for (var, leaf) in inits {
            let raw = if word.letter(pos).is_some() {
                0
            } else {
                self.env.value(*leaf, pos, &seen)?
            };
            let v = Some(self.ir.automaton.local_var(*var).cast(raw));
            f[var.0 as usize] = v;
            seen[var.0 as usize] = v;
        }
        Ok(f)
    }

    /// `sat(prop, w, pos, frame)`: does `w^{pos..}` satisfy `prop` with the
    /// local-variable `frame` as input context. `dom` is the clock the context is
    /// running on (16.13.2): an evaluation point is a tick of it, so `pos` is moved
    /// to the first tick of `dom` at or after it, and every operator that counts
    /// time counts ticks of `dom`. A single-clocked property has every position a
    /// tick and this is the identity.
    ///
    /// `strict` is the pending synchronization of a nonoverlapped implication's
    /// consequent (16.13.2): "time is advanced from the end point of the match to
    /// the nearest STRICTLY future occurrence" of the clock the consequent starts
    /// on. It is carried down to wherever that clock is known -- through `not`,
    /// `and`, `or` and `@(c)`, which add no time of their own, so that each branch
    /// of `s0 |=> (@(c1) s1) and (@(c2) s2)` synchronizes to its own clock -- and
    /// consumed by the first operator that stands on a position.
    #[allow(clippy::too_many_arguments)]
    fn sat(
        &self,
        id: PropId,
        word: &TailWord,
        pos: u32,
        frame: &Frame,
        depth: u32,
        dom: ClockId,
        strict: bool,
    ) -> Result<bool, TraceError> {
        let prop = self.ir.prop(id);
        let (pos, strict) = self.stand(prop, word, pos, dom, strict)?;
        match prop {
            Prop::Seq { seq, strength } => {
                let strong = match strength {
                    Some(Strength::Strong) => true,
                    Some(Strength::Weak) => false,
                    None => self.implicit_strong,
                };
                if strong {
                    self.strong_seq(*seq, word, pos, frame)
                } else {
                    self.weak_seq(*seq, word, pos, frame)
                }
            }
            Prop::Not(p) => Ok(!self.sat(*p, &word.flip(), pos, frame, depth, dom, strict)?),
            Prop::And(a, b) => {
                let left = self.sat(*a, word, pos, frame, depth, dom, strict)?;
                if !left && !self.exhaustive.get() {
                    return Ok(false);
                }
                let right = self.sat(*b, word, pos, frame, depth, dom, strict)?;
                Ok(left && right)
            }
            Prop::Or(a, b) => {
                let left = self.sat(*a, word, pos, frame, depth, dom, strict)?;
                if left && !self.exhaustive.get() {
                    return Ok(true);
                }
                let right = self.sat(*b, word, pos, frame, depth, dom, strict)?;
                Ok(left || right)
            }
            Prop::If { cond, then, els } => {
                if self.boolean(*cond, word, pos, frame)? {
                    self.sat(*then, word, pos, frame, depth, dom, false)
                } else if let Some(e) = els {
                    self.sat(*e, word, pos, frame, depth, dom, false)
                } else {
                    Ok(true)
                }
            }
            Prop::Case {
                selector,
                arms,
                default,
            } => {
                for arm in arms {
                    if self.arm_selected(*selector, arm, word, pos, frame)? {
                        return self.sat(arm.body, word, pos, frame, depth, dom, false);
                    }
                }
                match default {
                    Some(d) => self.sat(*d, word, pos, frame, depth, dom, false),
                    None => Ok(true),
                }
            }
            Prop::Implication {
                ante,
                cons,
                overlapped,
            } => {
                // A consequent with a clock of its own is a `Clocked` node (or a
                // sequence stamped with one) and moves itself.
                //
                // `|->` evaluates the consequent at the end point, and the
                // consequent's own clock "awaits its nearest tick", at or after
                // it. `|=>` advances from the end point to the nearest STRICTLY
                // future tick of the clock the consequent starts on (16.13.2, the
                // `strict` flag of `sat`); with one clock that is the next tick,
                // `ante ##1 1` of F.3.4. Annex F's rewrite, read literally for a
                // multiclocked `|=>`, advances one tick of the ANTECEDENT's clock
                // and only then awaits the consequent clock: the two differ
                // exactly when a tick of the consequent's clock falls between the
                // end point and the next tick of the antecedent's. The prose of
                // 16.13.2, being specific to this construct, is what is
                // implemented.
                // A consequent that carries no clock of its own runs on the clock
                // of the context the implication stands in (`dom`), not on the one
                // the antecedent ended on: Annex F.5.1 rewrites `r |-> p` under `c`
                // to `T_s(r, c) |-> T_p(p, c)`, and 16.13.3's `@(c) w ##1 (x ##1
                // @(d) y) |=> z` clocks `z` at `c`.
                let on = ante.end_clock;
                let dual;
                let aw = if self.open_future {
                    dual = word.flip();
                    &dual
                } else {
                    word
                };
                // A failing consequent decides the implication; collecting calls
                // goes on, as the consequent's threads (16.11) are evaluated too.
                let mut holds = true;
                for (end, f) in self.matches(*ante, aw, pos, frame)? {
                    if !*overlapped {
                        // The `1` of `ante ##1 1` is a Boolean on the next tick of
                        // the antecedent's clock, which no `⊥` letter satisfies
                        // (F.5.3). A consequent that starts on another clock is
                        // synchronized to that clock's next tick instead (16.13.2),
                        // so it is that tick that must exist: the verdict of a
                        // failing consequent is then reported at ITS tick, not at
                        // the antecedent clock's next one.
                        let next = self.after(aw, self.lead_clock(*cons, on), end, 1)?;
                        if aw.letter(next) == Some(false) {
                            continue;
                        }
                    }
                    if !self.sat(*cons, word, end, &f, depth, dom, !*overlapped)? {
                        if !self.exhaustive.get() {
                            return Ok(false);
                        }
                        holds = false;
                    }
                }
                // An empty match of the antecedent triggers `|=>` at the start
                // point itself (16.12.7): `(empty ##1 1)` is `1` on that tick.
                if !overlapped
                    && ante.admits_empty
                    && aw.letter(pos) != Some(false)
                    && !self.sat(*cons, word, pos, frame, depth, dom, false)?
                {
                    holds = false;
                }
                Ok(holds)
            }
            Prop::Nexttime { p, n, .. } => {
                let to = self.after(word, dom, pos, *n)?;
                self.sat(*p, word, to, frame, depth, dom, false)
            }
            Prop::Always { p, lo, hi, .. } => {
                if let Some(found) =
                    self.scan_range(*p, word, pos, *lo, *hi, frame, depth, dom, false)
                {
                    return found.map(|failed| !failed);
                }
                for t in self.positions(word, dom, pos, *lo, *hi)? {
                    if !self.sat(*p, word, t, frame, depth, dom, false)? {
                        return Ok(false);
                    }
                }
                Ok(true)
            }
            Prop::Eventually { p, lo, hi, .. } => {
                if let Some(found) =
                    self.scan_range(*p, word, pos, *lo, *hi, frame, depth, dom, true)
                {
                    return found;
                }
                for t in self.positions(word, dom, pos, *lo, *hi)? {
                    if self.sat(*p, word, t, frame, depth, dom, false)? {
                        return Ok(true);
                    }
                }
                Ok(false)
            }
            Prop::Until { p, q, strong } => {
                // `∃j: q at j, p at every i < j` or `p at every i`; a start point
                // past `extent` is `extent`, so the scan ends there and, having
                // passed every `p`, a weak `until` holds forever on. The `i` and
                // `j` are ticks of `dom`.
                let mut t = pos;
                if let Some(decided) = self.skip_settled_until(*p, *q, word, pos, frame, depth, dom)
                {
                    match decided {
                        Settled::Verdict(v) => return Ok(v),
                        Settled::Resume(from) => t = from,
                    }
                }
                loop {
                    if self.sat(*q, word, t, frame, depth, dom, false)? {
                        return Ok(true);
                    }
                    if !self.sat(*p, word, t, frame, depth, dom, false)? {
                        return Ok(false);
                    }
                    if t >= word.extent() {
                        break;
                    }
                    t = self.align(word, dom, self.after(word, dom, t, 1)?)?;
                }
                Ok(!strong)
            }
            Prop::Clocked { clock, p } => self.sat(*p, word, pos, frame, depth, *clock, strict),
            Prop::Abort { cond, p, mode } => {
                self.abort(*cond, *p, *mode, word, pos, frame, depth, dom)
            }
            Prop::Let { writes, body } => {
                let mut f = frame.clone();
                for (var, leaf) in writes {
                    let raw = if word.letter(pos).is_some() {
                        0
                    } else {
                        self.env.value(*leaf, pos, &f)?
                    };
                    f[var.0 as usize] = Some(self.ir.automaton.local_var(*var).cast(raw));
                }
                self.sat(*body, word, pos, &f, depth, dom, false)
            }
            Prop::Call { decl, args, inits } => {
                if depth >= self.recursion_limit(word) {
                    // `π[0]` is the Boolean `1'b1`: true on every letter but `⊥`.
                    return Ok(word.letter(pos) != Some(false));
                }
                // The body runs in the caller's frame with the formals' slots
                // rebound: every actual is evaluated in the caller's frame, before
                // any slot is overwritten (an actual may read the slot its own
                // formal is about to take, `fibonacci1(b, a+b, ...)`).
                let f = self.call_frame(args, inits, word, pos, frame)?;
                let key = (*decl, pos, word.clone(), f, depth, dom);
                if let Some(&known) = self.calls.borrow().get(&key) {
                    return Ok(known);
                }
                let body = self.ir.decls[decl.0 as usize].body;
                let holds = self.sat(body, word, pos, &key.3, depth + 1, dom, false)?;
                self.calls.borrow_mut().insert(key, holds);
                Ok(holds)
            }
        }
    }

    /// Whether the evaluation attempt started at tick `start` of a trace of `len`
    /// samples is NONVACUOUS (16.14.8); together with a passing verdict it is a
    /// nonvacuous success.
    ///
    /// The attempt is judged on the letters it saw: those before the first moment
    /// the property spec's `disable iff` is true (rule ag: the condition holds in
    /// no time step of the attempt), all of them when it never is. The rules
    /// (a)-(af) are syntax-directed and live in [`Self::nv`], one arm per
    /// operator, next to [`Self::sat`]'s arm for the same operator.
    pub fn nonvacuous(&self, len: u32, start: u32) -> Result<bool, TraceError> {
        let end = self.disabling_prefix(len, start)?.unwrap_or(len);
        self.calls.borrow_mut().clear();
        let frame = self.initial_frame();
        self.nv(
            self.ir.root,
            &TailWord::strong(end),
            start,
            &frame,
            0,
            self.root_clock(),
            false,
        )
    }

    /// 16.14.8: is the evaluation attempt of `id` from `pos` nonvacuous? The
    /// arguments are [`Self::sat`]'s. A "clock event" of the rules is a real tick
    /// of `dom` of the word, never one of its `⊤`/`⊥` letters.
    #[allow(clippy::too_many_arguments)]
    fn nv(
        &self,
        id: PropId,
        word: &TailWord,
        pos: u32,
        frame: &Frame,
        depth: u32,
        dom: ClockId,
        strict: bool,
    ) -> Result<bool, TraceError> {
        let prop = self.ir.prop(id);
        let (pos, strict) = self.stand(prop, word, pos, dom, strict)?;
        let real = |t: u32| word.letter(t).is_none();
        match prop {
            // (a), (b), (c): a sequence, `strong(seq)` and `weak(seq)`.
            Prop::Seq { .. } => Ok(true),
            // (d)
            Prop::Not(p) => self.nv(*p, &word.flip(), pos, frame, depth, dom, strict),
            // (e), (f), (aa)
            Prop::And(a, b) => Ok(self.nv(*a, word, pos, frame, depth, dom, strict)?
                || self.nv(*b, word, pos, frame, depth, dom, strict)?),
            Prop::Or(a, b) => {
                if self.ir.nv_rule(id) == Some(NvRule::Implies) {
                    // (z): `not p or q` standing for `p implies q`.
                    let Prop::Not(p) = self.ir.prop(*a) else {
                        unreachable!("an `implies` node's left operand is the negation of `p`")
                    };
                    return Ok(self.sat(*p, word, pos, frame, depth, dom, strict)?
                        && self.nv(*p, word, pos, frame, depth, dom, strict)?
                        && self.nv(*b, word, pos, frame, depth, dom, strict)?);
                }
                Ok(self.nv(*a, word, pos, frame, depth, dom, strict)?
                    || self.nv(*b, word, pos, frame, depth, dom, strict)?)
            }
            // (g): the branch taken, and nothing at all for a missing `else`.
            Prop::If { cond, then, els } => {
                if self.boolean(*cond, word, pos, frame)? {
                    self.nv(*then, word, pos, frame, depth, dom, false)
                } else if let Some(e) = els {
                    self.nv(*e, word, pos, frame, depth, dom, false)
                } else {
                    Ok(false)
                }
            }
            // (af): the selected arm, the `default` when none is.
            Prop::Case {
                selector,
                arms,
                default,
            } => {
                for arm in arms {
                    if self.arm_selected(*selector, arm, word, pos, frame)? {
                        return self.nv(arm.body, word, pos, frame, depth, dom, false);
                    }
                }
                match default {
                    Some(d) => self.nv(*d, word, pos, frame, depth, dom, false),
                    None => Ok(false),
                }
            }
            // (h), (j), (k): a match of the antecedent with a nonvacuous
            // consequent attempt from its end point (the next clock event for the
            // nonoverlapped forms).
            Prop::Implication {
                ante,
                cons,
                overlapped,
            } => {
                let on = ante.end_clock;
                let dual;
                let aw = if self.open_future {
                    dual = word.flip();
                    &dual
                } else {
                    word
                };
                for (end, f) in self.matches(*ante, aw, pos, frame)? {
                    if !*overlapped {
                        let next = self.after(aw, self.lead_clock(*cons, on), end, 1)?;
                        if aw.letter(next) == Some(false) {
                            continue;
                        }
                    }
                    if self.nv(*cons, word, end, &f, depth, dom, !*overlapped)? {
                        return Ok(true);
                    }
                }
                Ok(!overlapped
                    && ante.admits_empty
                    && aw.letter(pos) != Some(false)
                    && self.nv(*cons, word, pos, frame, depth, dom, false)?)
            }
            // (l)-(o): the clock event `n` ticks on must exist.
            Prop::Nexttime { p, n, .. } => {
                let to = self.after(word, dom, pos, *n)?;
                Ok(real(to) && self.nv(*p, word, to, frame, depth, dom, false)?)
            }
            // (p)-(r): a clock event of the range where `p` is nonvacuous, `p`
            // not having failed before it.
            Prop::Always { p, lo, hi, .. } => {
                for t in self.positions(word, dom, pos, *lo, *hi)? {
                    if !real(t) {
                        break;
                    }
                    if self.nv(*p, word, t, frame, depth, dom, false)? {
                        return Ok(true);
                    }
                    if !self.sat(*p, word, t, frame, depth, dom, false)? {
                        return Ok(false);
                    }
                }
                Ok(false)
            }
            // (s)-(u): the same with `p` not having held before.
            Prop::Eventually { p, lo, hi, .. } => {
                for t in self.positions(word, dom, pos, *lo, *hi)? {
                    if !real(t) {
                        break;
                    }
                    if self.nv(*p, word, t, frame, depth, dom, false)? {
                        return Ok(true);
                    }
                    if self.sat(*p, word, t, frame, depth, dom, false)? {
                        return Ok(false);
                    }
                }
                Ok(false)
            }
            // (v), (w): a clock event where either operand is nonvacuous, `q` not
            // having held and `p` having held at every one before it; (x), (y)
            // (`until_with`): only `p` counts.
            Prop::Until { p, q, .. } => {
                let with = self.ir.nv_rule(id) == Some(NvRule::UntilWith);
                let mut t = pos;
                while real(t) {
                    if self.nv(*p, word, t, frame, depth, dom, false)?
                        || (!with && self.nv(*q, word, t, frame, depth, dom, false)?)
                    {
                        return Ok(true);
                    }
                    if self.sat(*q, word, t, frame, depth, dom, false)?
                        || !self.sat(*p, word, t, frame, depth, dom, false)?
                    {
                        return Ok(false);
                    }
                    t = self.align(word, dom, self.after(word, dom, t, 1)?)?;
                }
                Ok(false)
            }
            Prop::Clocked { clock, p } => self.nv(*p, word, pos, frame, depth, *clock, strict),
            // (ab)-(ae): `p` nonvacuous and the condition true at no time step of
            // the attempt (at no clock event, for the `sync_` forms).
            Prop::Abort { cond, p, mode } => {
                if !self.nv(*p, word, pos, frame, depth, dom, false)? {
                    return Ok(false);
                }
                let sync = mode.is_sync();
                let timeline = self.timeline_for(word)?;
                for t in pos..word.real {
                    let looks = !sync || timeline.as_ref().is_none_or(|tl| tl.is_tick(dom, t));
                    if looks && self.boolean(*cond, word, t, frame)? {
                        return Ok(false);
                    }
                    if !sync && timeline.is_none() && self.env.between(*cond, t)? {
                        return Ok(false);
                    }
                }
                Ok(true)
            }
            Prop::Let { writes, body } => {
                let mut f = frame.clone();
                for (var, leaf) in writes {
                    let raw = if word.letter(pos).is_some() {
                        0
                    } else {
                        self.env.value(*leaf, pos, &f)?
                    };
                    f[var.0 as usize] = Some(self.ir.automaton.local_var(*var).cast(raw));
                }
                self.nv(*body, word, pos, &f, depth, dom, false)
            }
            // (i): the instance's body with the actuals substituted.
            Prop::Call { decl, args, inits } => {
                if depth >= self.recursion_limit(word) {
                    return Ok(false);
                }
                let f = self.call_frame(args, inits, word, pos, frame)?;
                let body = self.ir.decls[decl.0 as usize].body;
                self.nv(body, word, pos, &f, depth + 1, dom, false)
            }
        }
    }

    /// Whether the `case` arm is selected at `pos`: on a `⊤` letter every label
    /// holds, on `⊥` none does (the `if (selector === label)` chain of F.3.4.3
    /// evaluated at such a letter).
    fn arm_selected(
        &self,
        selector: LeafId,
        arm: &CaseArm,
        word: &TailWord,
        pos: u32,
        frame: &Frame,
    ) -> Result<bool, TraceError> {
        if let Some(top) = word.letter(pos) {
            return Ok(top);
        }
        for &label in &arm.labels {
            if self.env.case_match(selector, label, pos, frame)? {
                return Ok(true);
            }
        }
        Ok(false)
    }

    /// The distinct start points `always`/`eventually [lo:hi]` ranges over from
    /// `pos`: `pos+lo ..= pos+hi` (to the end for `$`), with every tick past
    /// `extent` folded into it.
    ///
    /// The range counts ticks of `dom` (16.13.2: a bounded `always [1:2]` on a
    /// clock is the next one and two ticks of THAT clock).
    fn positions(
        &self,
        word: &TailWord,
        dom: ClockId,
        pos: u32,
        lo: u32,
        hi: Option<u32>,
    ) -> Result<Vec<u32>, TraceError> {
        let ext = word.extent();
        let mut out = Vec::new();
        let mut k = lo;
        loop {
            let at = self.after(word, dom, pos, k)?;
            if at >= ext {
                out.push(ext);
                break;
            }
            out.push(at);
            if hi.is_some_and(|h| k >= h) {
                break;
            }
            k += 1;
        }
        Ok(out)
    }

    /// How far the verdicts of `id` are SETTLED on `word` (see [`Accel`]'s
    /// `Fin`): the window ticks `0..end` have a verdict no continuation of the
    /// trace and no choice of word can change, and they are in the accelerator's
    /// memo. `None` when the accelerator does not model `id` (several clocks, an
    /// unbounded lookahead, a local variable that is read, a word with explicit
    /// letters, ...), and the caller then runs the reference code.
    ///
    /// The memo is filled here, in tick order, with the verdicts the reference
    /// evaluation computes (`sat` of `id` at the tick, which is exactly what its
    /// loops ask), up to the last tick whose whole lookahead is real samples of
    /// `word`; one that is an error stops the filling, and the reference code
    /// then meets it where it would have.
    fn settled(
        &self,
        id: PropId,
        word: &TailWord,
        frame: &Frame,
        depth: u32,
        dom: ClockId,
    ) -> Option<u32> {
        let cell = self.accel?;
        if !word.mid.is_empty() || self.env.timeline().is_some() {
            return None;
        }
        let (reach, base) = {
            let accel = cell.try_borrow().ok()?;
            (accel.final_reach(id)?, accel.base())
        };
        // A tick `t` is settled when `t + reach` is a real tick.
        let limit = word.real.saturating_sub(reach);
        loop {
            let (next, blocked) = cell.try_borrow_mut().ok()?.final_next(id);
            let next_rel = u32::try_from(next - base).ok()?;
            if blocked || next_rel >= limit {
                return Some(next_rel.min(limit));
            }
            let verdict = self.sat(id, word, next_rel, frame, depth, dom, false);
            let mut accel = cell.try_borrow_mut().ok()?;
            accel.final_reach(id)?;
            accel.final_record(id, next, verdict.ok());
        }
    }

    /// Whether some tick of the range `always`/`eventually [lo:hi]` ranges over
    /// from `pos` has the verdict `stop_on` for `p`, found in the order, and with
    /// the errors, the reference loop over [`Self::positions`] has: the settled
    /// run of the range is read from the memo, and the rest evaluated.
    /// `None` declines (see [`Self::settled`]).
    #[allow(clippy::too_many_arguments)]
    fn scan_range(
        &self,
        p: PropId,
        word: &TailWord,
        pos: u32,
        lo: u32,
        hi: Option<u32>,
        frame: &Frame,
        depth: u32,
        dom: ClockId,
        stop_on: bool,
    ) -> Option<Result<bool, TraceError>> {
        let end = self.settled(p, word, frame, depth, dom)?;
        let cell = self.accel?;
        let first = pos.saturating_add(lo);
        let upper = hi.map_or(end, |h| end.min(pos.saturating_add(h).saturating_add(1)));
        let mut k = lo;
        if first < upper {
            let accel = cell.try_borrow().ok()?;
            let base = accel.base();
            let hit = accel.final_first(p, stop_on, base + u64::from(first));
            if hit.is_some_and(|t| t < base + u64::from(upper)) {
                return Some(Ok(true));
            }
            k = upper - pos;
        }
        let ext = word.extent();
        loop {
            if hi.is_some_and(|h| k > h) {
                return Some(Ok(false));
            }
            let at = pos + k;
            match self.sat(p, word, at.min(ext), frame, depth, dom, false) {
                Err(e) => return Some(Err(e)),
                Ok(v) if v == stop_on => return Some(Ok(true)),
                Ok(_) => {}
            }
            if at >= ext || hi.is_some_and(|h| k >= h) {
                return Some(Ok(false));
            }
            k += 1;
        }
    }

    /// The settled run of `p until q` from `pos`: the verdict when a settled tick
    /// decides it, else the tick the evaluation resumes at (every tick before
    /// it has `q` false and `p` true). `None` declines.
    #[allow(clippy::too_many_arguments)]
    fn skip_settled_until(
        &self,
        p: PropId,
        q: PropId,
        word: &TailWord,
        pos: u32,
        frame: &Frame,
        depth: u32,
        dom: ClockId,
    ) -> Option<Settled> {
        let ep = self.settled(p, word, frame, depth, dom)?;
        let eq = self.settled(q, word, frame, depth, dom)?;
        let end = ep.min(eq);
        if pos >= end {
            return None;
        }
        let accel = self.accel?.try_borrow().ok()?;
        let (from, to) = (accel.base() + u64::from(pos), accel.base() + u64::from(end));
        let q_true = accel.final_first(q, true, from).filter(|&t| t < to);
        let p_false = accel.final_first(p, false, from).filter(|&t| t < to);
        Some(match (q_true, p_false) {
            // `q` is tried before `p` on a tick.
            (Some(a), Some(b)) => Settled::Verdict(a <= b),
            (Some(_), None) => Settled::Verdict(true),
            (None, Some(_)) => Settled::Verdict(false),
            (None, None) => Settled::Resume(end),
        })
    }

    /// `accept_on`/`reject_on`/`sync_*` (16.12.14, F.5.6.1).
    #[allow(clippy::too_many_arguments)]
    fn abort(
        &self,
        cond: LeafId,
        p: PropId,
        mode: AbortMode,
        word: &TailWord,
        pos: u32,
        frame: &Frame,
        depth: u32,
        dom: ClockId,
    ) -> Result<bool, TraceError> {
        if mode.accepts() {
            self.accept_on(cond, mode.is_sync(), p, false, word, pos, frame, depth, dom)
        } else {
            // `reject_on(b) P` is `not accept_on(b) not P`.
            Ok(!self.accept_on(
                cond,
                mode.is_sync(),
                p,
                true,
                &word.flip(),
                pos,
                frame,
                depth,
                dom,
            )?)
        }
    }

    /// `accept_on(cond) p` (`not p` when `negated`) on `word` from `pos`: `p` holds
    /// on the whole word and the condition is never true, or for some abort
    /// point the word cut just before it and completed with `⊤` satisfies `p`.
    /// An abort point is a tick whose sampled condition is true and, unless
    /// `sync`, a time step between two ticks where it is.
    #[allow(clippy::too_many_arguments)]
    fn accept_on(
        &self,
        cond: LeafId,
        sync: bool,
        p: PropId,
        negated: bool,
        word: &TailWord,
        pos: u32,
        frame: &Frame,
        depth: u32,
        dom: ClockId,
    ) -> Result<bool, TraceError> {
        let inner = |w: &TailWord| -> Result<bool, TraceError> {
            if negated {
                Ok(!self.sat(p, &w.flip(), pos, frame, depth, dom, false)?)
            } else {
                self.sat(p, w, pos, frame, depth, dom, false)
            }
        };
        let timeline = self.timeline_for(word)?;
        let mut aborted = false;
        for t in pos..=word.extent() {
            // On a multiclock timeline the positions ARE the global steps: an
            // asynchronous condition is looked at on every one of them and a
            // synchronous one on the ticks of the property's clock. The `between`
            // steps do not exist there (every step is a position). When a
            // property spans several clocks this uses the clock the abort sits
            // on, not each operand's own -- see the module docs' approximation.
            let looks = !sync || timeline.as_ref().is_none_or(|tl| tl.is_tick(dom, t));
            if looks && self.boolean(cond, word, t, frame)? {
                aborted = true;
                if inner(&word.cut_then_top(t))? {
                    return Ok(true);
                }
            }
            if !sync && timeline.is_none() && t < word.real && self.env.between(cond, t)? {
                aborted = true;
                if inner(&word.cut_then_top(t + 1))? {
                    return Ok(true);
                }
            }
        }
        // A condition true on the constant tail is true at `extent` already.
        if aborted { Ok(false) } else { inner(word) }
    }
}

/// Whether `p` adds no position of its own: it evaluates its operands at the
/// position it is given, so a pending `|=>` synchronization (see
/// [`Evaluator::sat`]'s `strict`) passes through it to the operands.
fn pass_through(p: &Prop) -> bool {
    match p {
        Prop::Not(_) | Prop::And(..) | Prop::Or(..) | Prop::Clocked { .. } => true,
        Prop::Seq { .. }
        | Prop::If { .. }
        | Prop::Case { .. }
        | Prop::Implication { .. }
        | Prop::Nexttime { .. }
        | Prop::Always { .. }
        | Prop::Eventually { .. }
        | Prop::Until { .. }
        | Prop::Abort { .. }
        | Prop::Let { .. }
        | Prop::Call { .. } => false,
    }
}

/// What an automaton entry's sequence is, for the static legality checks of
/// 16.12.22.
#[derive(Clone, Copy, Debug, PartialEq, Eq)]
pub enum SequenceClass {
    /// No match at all, empty or not: `(1'b1) intersect (1'b1 ##1 1'b1)`.
    Never,
    /// Only the empty match: `1'b1[*0]`.
    EmptyOnly,
    /// At least one nonempty match; `also_empty` says whether the empty match is
    /// admitted too (`a[*0:2]`).
    NonEmpty { also_empty: bool },
}

/// Classifies the sequence entered at `seq` (16.12.22, F.5.5: nondegenerate iff
/// some nonempty word matches). A nonempty match is a path from the entry to a
/// state with a [`Transition::Match`] edge; the Boolean guards are treated as
/// satisfiable, which is what "some word" means for a Boolean expression, so
/// the result is a pure function of the automaton's graph.
///
/// `guard_never` names the leaves that can never hold (a constant-false
/// Boolean, judged on the leaf's own value -- `!e` for a negated leaf): an edge
/// guarded by one is not on any path.
pub fn classify_sequence(
    au: &Automaton,
    seq: SeqRef,
    guard_never: &dyn Fn(LeafId) -> bool,
) -> SequenceClass {
    let mut seen = vec![false; au.states.len()];
    let mut stack = vec![seq.entry];
    seen[seq.entry.0 as usize] = true;
    let mut accepting = false;
    while let Some(s) = stack.pop() {
        for e in &au.state(s).edges {
            if e.guard.is_some_and(guard_never) {
                continue;
            }
            if matches!(e.label, Transition::Match { .. }) {
                accepting = true;
                continue;
            }
            if !seen[e.target.0 as usize] {
                seen[e.target.0 as usize] = true;
                stack.push(e.target);
            }
        }
    }
    match (accepting, seq.admits_empty) {
        (true, also_empty) => SequenceClass::NonEmpty { also_empty },
        (false, true) => SequenceClass::EmptyOnly,
        (false, false) => SequenceClass::Never,
    }
}

#[cfg(test)]
mod tests {
    use super::*;
    use crate::sva::ir::LeafId;

    /// A property under construction over a hand-built automaton.
    struct B {
        au: Automaton,
        props: Vec<Prop>,
        decls: Vec<PropDecl>,
    }

    impl B {
        fn new() -> Self {
            B {
                au: Automaton::empty(),
                props: Vec::new(),
                decls: Vec::new(),
            }
        }

        fn prop(&mut self, p: Prop) -> PropId {
            self.props.push(p);
            PropId(self.props.len() as u32 - 1)
        }

        /// The sequence `l0 ##d1 l1 ##d2 l2 ...` of Boolean leaves.
        fn seq(&mut self, leaves: &[u32], delays: &[u32]) -> SeqRef {
            let ranges: Vec<(u32, Option<u32>)> = delays.iter().map(|&d| (d, Some(d))).collect();
            self.seq_r(leaves, &ranges)
        }

        /// The sequence `l0 ##[m1:n1] l1 ...` (`None` is `$`).
        fn seq_r(&mut self, leaves: &[u32], delays: &[(u32, Option<u32>)]) -> SeqRef {
            assert_eq!(leaves.len(), delays.len() + 1);
            let entry = self.au.new_state();
            let mut at = entry;
            for (i, l) in leaves.iter().enumerate() {
                let next = self.au.new_state();
                self.au
                    .add_edge(at, Some(LeafId(*l)), Transition::Epsilon, next);
                at = next;
                if let Some(&(min, max)) = delays.get(i) {
                    let next = self.au.new_state();
                    self.au
                        .add_edge(at, None, Transition::Delay { min, max }, next);
                    at = next;
                }
            }
            self.au.add_edge(
                at,
                None,
                Transition::Match {
                    actions: Vec::new(),
                },
                at,
            );
            SeqRef::single(entry, false)
        }

        fn leaf(&mut self, l: u32) -> SeqRef {
            self.seq(&[l], &[])
        }

        /// The Boolean leaf `l` as a property (a one-letter sequence).
        fn b(&mut self, l: u32, strength: Option<Strength>) -> PropId {
            let seq = self.leaf(l);
            self.prop(Prop::Seq { seq, strength })
        }

        fn not(&mut self, p: PropId) -> PropId {
            self.prop(Prop::Not(p))
        }

        fn finish(self, root: PropId) -> PropertyIr {
            PropertyIr {
                automaton: self.au,
                props: self.props,
                decls: self.decls,
                root,
                disable: None,
                nv_rules: Vec::new(),
            }
        }
    }

    /// Leaves as per-leaf boolean rows.
    struct Rows(Vec<Vec<bool>>);

    impl PropEnv for Rows {
        fn value(&self, leaf: LeafId, tick: u32, _: &[Option<i64>]) -> Result<i64, TraceError> {
            Ok(i64::from(self.0[leaf.0 as usize][tick as usize]))
        }
        fn case_match(
            &self,
            selector: LeafId,
            label: LeafId,
            tick: u32,
            f: &[Option<i64>],
        ) -> Result<bool, TraceError> {
            Ok(self.value(selector, tick, f)? == self.value(label, tick, f)?)
        }
    }

    fn rows(r: &[&str]) -> Rows {
        Rows(
            r.iter()
                .map(|s| s.chars().map(|c| c == '1').collect())
                .collect(),
        )
    }

    fn verdict(ir: &PropertyIr, env: &Rows, len: u32, start: u32, strong: bool) -> Verdict {
        Evaluator::new(ir, env, strong).verdict(len, start).unwrap()
    }

    /// 16.12.2: `p3` is `b ##1 c`; `a1: assert property (a |-> p3)` reads `p3` as
    /// weak, `c1: cover property (a #-# p3)` as strong.
    #[test]
    fn lrm_sequence_property_is_weak_in_assert_and_strong_in_cover() {
        // leaves: 0 = a, 1 = b, 2 = c
        let mut b = B::new();
        let a = b.leaf(0);
        let p3 = b.seq(&[1, 2], &[1]);
        let p3p = b.prop(Prop::Seq {
            seq: p3,
            strength: None,
        });
        let a1 = b.prop(Prop::Implication {
            ante: a,
            cons: p3p,
            overlapped: true,
        });
        let ir = b.finish(a1);
        // a false: true either way. b true then the trace ends: weak holds,
        // strong does not (assert only needs the weak reading).
        let end_after_b = rows(&["1", "1", "0"]);
        assert_eq!(
            verdict(&ir, &end_after_b, 1, 0, false),
            Verdict::Holds,
            "weak: `b` holds and there is no next tick"
        );
        // b true and c true at the next tick: holds strongly.
        let full = rows(&["11", "10", "01"]);
        assert_eq!(verdict(&ir, &full, 2, 0, false), Verdict::HoldsStrongly);
        // b true but c false at the next tick: fails.
        let bad = rows(&["11", "10", "00"]);
        assert_eq!(verdict(&ir, &bad, 2, 0, false), Verdict::Fails);
        // a false at the start: the implication is vacuously true.
        let vac = rows(&["0", "0", "0"]);
        assert_eq!(verdict(&ir, &vac, 1, 0, false), Verdict::HoldsStrongly);
        // b false at the start: fails regardless of the trace length.
        let nob = rows(&["1", "0", "1"]);
        assert_eq!(verdict(&ir, &nob, 1, 0, false), Verdict::Fails);
    }

    /// Every assignment of `leaves` boolean rows of `len` ticks.
    fn all_traces(leaves: usize, len: usize) -> Vec<Rows> {
        let bits = leaves * len;
        (0..1u32 << bits)
            .map(|m| {
                Rows(
                    (0..leaves)
                        .map(|l| (0..len).map(|t| m >> (l * len + t) & 1 == 1).collect())
                        .collect(),
                )
            })
            .collect()
    }

    /// The verdict of `root` over every trace of `leaves` signals of 0..=max_len ticks
    /// from every start tick, as a flat list.
    fn verdicts(ir: &PropertyIr, leaves: usize, max_len: usize, strong: bool) -> Vec<Verdict> {
        let mut out = Vec::new();
        for len in 1..=max_len {
            for env in all_traces(leaves, len) {
                for start in 0..len as u32 {
                    out.push(verdict(ir, &env, len as u32, start, strong));
                }
            }
        }
        out
    }

    /// 16.12.3: `not` switches strength. For `a ##[1:$] b` the weak sequence holds on
    /// the dual word (an unbounded delay is never refuted by a finite prefix),
    /// so `not (a ##[1:$] b)` fails on a trace that ends right after `a` -- the
    /// pitfall -- while `not strong(a ##[1:$] b)` only stays pending.
    #[test]
    fn lrm_not_of_a_weak_sequence_is_the_pitfall_and_strong_is_the_fix() {
        let mut b = B::new();
        let r = b.seq_r(&[0, 1], &[(1, None)]);
        let weak = b.prop(Prop::Seq {
            seq: r,
            strength: None,
        });
        let a1 = b.not(weak);
        let strong = b.prop(Prop::Seq {
            seq: r,
            strength: Some(Strength::Strong),
        });
        let a2 = b.not(strong);
        let mut ir1 = b.finish(a1);
        // a holds at the last tick of the trace, `b` never does.
        let env = rows(&["1", "0"]);
        assert_eq!(verdict(&ir1, &env, 1, 0, false), Verdict::Fails);
        ir1.root = a2;
        assert_eq!(verdict(&ir1, &env, 1, 0, false), Verdict::Holds);
        // With `b` seen after `a`, the strong sequence matched: `not` fails both ways.
        let env = rows(&["10", "01"]);
        assert_eq!(verdict(&ir1, &env, 2, 0, false), Verdict::Fails);
    }

    /// Table 40-3 (`aundf`): the weak `a ##[1:$] b` never fails on a finite prefix
    /// and does not hold STRONGLY until it matched, so its attempt is pending
    /// (not passed) while `b` has not been seen, and passes once it has.
    #[test]
    fn weak_unbounded_sequence_is_pending_until_it_matches() {
        let mut b = B::new();
        let r = b.seq_r(&[0, 1], &[(1, None)]);
        let weak = b.prop(Prop::Seq {
            seq: r,
            strength: None,
        });
        let ir = b.finish(weak);
        // Leaves 0 = a, 1 = b, one string per leaf: `a` at tick 0, `b` never.
        for (a, bb) in [("1", "0"), ("10", "00"), ("100", "000")] {
            let env = rows(&[a, bb]);
            assert_eq!(verdict(&ir, &env, a.len() as u32, 0, false), Verdict::Holds);
        }
        // `b` two ticks after `a`.
        let env = rows(&["100", "001"]);
        assert_eq!(verdict(&ir, &env, 3, 0, false), Verdict::HoldsStrongly);
    }

    /// Strength is the only thing `not` changes: `strong(R)` implies `weak(R)` on
    /// every trace, and `weak` fails only where `strong` does.
    #[test]
    fn strong_sequence_implies_weak_sequence() {
        let mut b = B::new();
        let r = b.seq_r(&[0, 1], &[(1, Some(2))]);
        let s = b.prop(Prop::Seq {
            seq: r,
            strength: Some(Strength::Strong),
        });
        let w = b.prop(Prop::Seq {
            seq: r,
            strength: Some(Strength::Weak),
        });
        let mut ir = b.finish(s);
        let strong = verdicts(&ir, 2, 4, false);
        ir.root = w;
        let weak = verdicts(&ir, 2, 4, false);
        assert_eq!(strong.len(), weak.len());
        for (s, w) in strong.iter().zip(&weak) {
            // strong: Fails or HoldsStrongly... a strong sequence is `Holds`
            // (pending) on a trace that cut it short, weak is too.
            assert!(
                *s != Verdict::HoldsStrongly || *w == Verdict::HoldsStrongly,
                "strong match on a trace the weak reading does not hold strongly"
            );
            assert!(*s == Verdict::Fails || *w != Verdict::Fails);
        }
    }

    /// 16.12.22 nondegeneracy, the LRM's three examples as automata.
    #[test]
    fn classify_sequence_lrm_examples() {
        let never = |_: LeafId| false;
        // (1'b1) intersect (1'b1 ##1 1'b1): no word matches -- built as an
        // entry whose only edges lead nowhere near a match.
        let mut au = Automaton::empty();
        let e = au.new_state();
        let dead = au.new_state();
        au.add_edge(e, Some(LeafId(0)), Transition::Epsilon, dead);
        let r = SeqRef::single(e, false);
        assert_eq!(classify_sequence(&au, r, &never), SequenceClass::Never);
        // 1'b1[*0]: only the empty match.
        let r = SeqRef::single(e, true);
        assert_eq!(classify_sequence(&au, r, &never), SequenceClass::EmptyOnly);
        // a[*0:2]: a nonempty match and the empty one.
        let mut b = B::new();
        let mut seq = b.leaf(0);
        seq.admits_empty = true;
        assert_eq!(
            classify_sequence(&b.au, seq, &never),
            SequenceClass::NonEmpty { also_empty: true }
        );
        // A match behind a leaf that can never hold is no match.
        let mut seq = b.leaf(1);
        assert_eq!(
            classify_sequence(&b.au, seq, &|l| l == LeafId(1)),
            SequenceClass::Never
        );
        seq.admits_empty = false;
        assert_eq!(
            classify_sequence(&b.au, seq, &never),
            SequenceClass::NonEmpty { also_empty: false }
        );
    }

    /// `s_nexttime p` is `not nexttime not p` (F.3.4.3), for every trace, start and
    /// offset; `nexttime[0]` is the alignment operator (16.12.10).
    #[test]
    fn nexttime_duality_and_alignment() {
        for n in 0..=2u32 {
            for strength in [Some(Strength::Weak), Some(Strength::Strong)] {
                let mut b = B::new();
                let p = b.b(0, strength);
                let snt = b.prop(Prop::Nexttime { p, n, strong: true });
                let np = b.not(p);
                let nn = b.prop(Prop::Nexttime {
                    p: np,
                    n,
                    strong: false,
                });
                let dual = b.not(nn);
                let mut ir = b.finish(snt);
                let a = verdicts(&ir, 1, 4, false);
                ir.root = dual;
                assert_eq!(a, verdicts(&ir, 1, 4, false), "n = {n}");
            }
        }
        // nexttime p needs the next tick: on a single-tick trace the weak
        // reading is satisfied, the strong one is only pending.
        let mut b = B::new();
        let p = b.b(0, Some(Strength::Strong));
        let nt = b.prop(Prop::Nexttime {
            p,
            n: 1,
            strong: false,
        });
        let ir = b.finish(nt);
        assert_eq!(verdict(&ir, &rows(&["0"]), 1, 0, false), Verdict::Holds);
        assert_eq!(
            verdict(&ir, &rows(&["01"]), 2, 0, false),
            Verdict::HoldsStrongly
        );
        assert_eq!(verdict(&ir, &rows(&["10"]), 2, 0, false), Verdict::Fails);
    }

    /// `s_eventually p` is `not always not p` and `always p` is `p until 0`.
    #[test]
    fn always_eventually_until_dualities() {
        let mut b = B::new();
        let p = b.b(0, Some(Strength::Weak));
        let seventually = b.prop(Prop::Eventually {
            p,
            lo: 0,
            hi: None,
            strong: true,
        });
        let np = b.not(p);
        let al = b.prop(Prop::Always {
            p: np,
            lo: 0,
            hi: None,
            strong: false,
        });
        let dual = b.not(al);
        let always = b.prop(Prop::Always {
            p,
            lo: 0,
            hi: None,
            strong: false,
        });
        let zero = b.b(1, Some(Strength::Weak));
        let until = b.prop(Prop::Until {
            p,
            q: zero,
            strong: false,
        });
        let mut ir = b.finish(seventually);
        let a = verdicts(&ir, 2, 3, false);
        ir.root = dual;
        assert_eq!(a, verdicts(&ir, 2, 3, false));
        // `until` with q the constant-0 leaf 1 only when leaf 1 is all-zero; compare
        // `always p` with `p until q` on the traces where q never holds.
        ir.root = always;
        let al = verdicts_with(&ir, 3);
        ir.root = until;
        let un = verdicts_with(&ir, 3);
        assert_eq!(al, un);
    }

    /// Verdicts over every `p` trace with `q` constant 0.
    fn verdicts_with(ir: &PropertyIr, max_len: usize) -> Vec<Verdict> {
        let mut out = Vec::new();
        for len in 1..=max_len {
            for env in all_traces(1, len) {
                let env = Rows(vec![env.0[0].clone(), vec![false; len]]);
                for start in 0..len as u32 {
                    out.push(verdict(ir, &env, len as u32, start, false));
                }
            }
        }
        out
    }

    /// 16.12.12: the four `until` forms on the LRM's `a`/`b` traces.
    #[test]
    fn until_family_truth_table() {
        // p until q: q at some tick j with p at all earlier ticks, or p always.
        let mut b = B::new();
        let p = b.b(0, Some(Strength::Weak));
        let q = b.b(1, Some(Strength::Weak));
        let u = b.prop(Prop::Until {
            p,
            q,
            strong: false,
        });
        let su = b.prop(Prop::Until { p, q, strong: true });
        let mut ir = b.finish(u);
        // a,a,a... never b: weak until holds (pending), strong until does not.
        let env = rows(&["111", "000"]);
        assert_eq!(verdict(&ir, &env, 3, 0, false), Verdict::Holds);
        ir.root = su;
        assert_eq!(verdict(&ir, &env, 3, 0, false), Verdict::Holds);
        // p fails before q: fails both.
        let env = rows(&["101", "001"]);
        assert_eq!(verdict(&ir, &env, 3, 0, false), Verdict::Fails);
        // q arrives while p still holds: holds strongly, even the strong form.
        let env = rows(&["110", "001"]);
        assert_eq!(verdict(&ir, &env, 3, 0, false), Verdict::HoldsStrongly);
        // q at the same tick p drops: `until` does not need p at the q tick.
        let env = rows(&["100", "010"]);
        assert_eq!(verdict(&ir, &env, 3, 0, false), Verdict::HoldsStrongly);
    }

    /// 16.12.14: the abort cut. `accept_on(a) p` succeeds if `a` becomes true
    /// during the evaluation even when `p` would fail afterwards; and an abort
    /// that is not reached leaves `p`'s verdict.
    #[test]
    fn accept_on_cuts_the_word_at_the_abort() {
        // p = strong(x ##1 y), abort cond = leaf 2.
        let mut b = B::new();
        let r = b.seq(&[0, 1], &[1]);
        let p = b.prop(Prop::Seq {
            seq: r,
            strength: Some(Strength::Strong),
        });
        let acc = b.prop(Prop::Abort {
            cond: LeafId(2),
            p,
            mode: AbortMode::SyncAccept,
        });
        let ir = b.finish(acc);
        // x then y: holds strongly regardless.
        assert_eq!(
            verdict(&ir, &rows(&["10", "01", "00"]), 2, 0, false),
            Verdict::HoldsStrongly
        );
        // the sequence fails at tick 1 (y low) but the abort fires at tick 1: the
        // word cut before tick 1 and completed by T lets `y` be true, so true.
        let env = rows(&["10", "00", "01"]);
        assert_eq!(verdict(&ir, &env, 2, 0, false), Verdict::HoldsStrongly);
        // the abort fires only after the sequence failed: cut at tick 2 still sees the
        // failure at tick 1.
        let env = rows(&["100", "000", "001"]);
        assert_eq!(verdict(&ir, &env, 3, 0, false), Verdict::Fails);
        // sync_reject_on is `not sync_accept_on not`: on the same trace it is false when
        // the abort fires before the property is decided, true if it never fires.
        let rej = {
            let mut b = B::new();
            let r = b.seq(&[0, 1], &[1]);
            let p = b.prop(Prop::Seq {
                seq: r,
                strength: Some(Strength::Strong),
            });
            let rej = b.prop(Prop::Abort {
                cond: LeafId(2),
                p,
                mode: AbortMode::SyncReject,
            });
            b.finish(rej)
        };
        let env = rows(&["10", "01", "01"]);
        assert_eq!(verdict(&rej, &env, 2, 0, false), Verdict::Fails);
        let env = rows(&["10", "01", "00"]);
        assert_eq!(verdict(&rej, &env, 2, 0, false), Verdict::HoldsStrongly);
    }

    /// 16.12.14: an abort and the end of the evaluation at the same tick: the abort
    /// wins; the outermost of two nested aborts wins a tie.
    #[test]
    fn abort_wins_a_tie_and_the_outermost_nested_abort_wins() {
        // p1 = strong(x), decided at tick 0. a (leaf 1) fires at tick 0 too.
        let mut b = B::new();
        let x = b.b(0, Some(Strength::Strong));
        let acc = b.prop(Prop::Abort {
            cond: LeafId(1),
            p: x,
            mode: AbortMode::SyncAccept,
        });
        let rej = b.prop(Prop::Abort {
            cond: LeafId(1),
            p: x,
            mode: AbortMode::SyncReject,
        });
        // x is false but the abort fires at tick 0 along with it: accept wins (true),
        // reject wins (false).
        let env = rows(&["0", "1"]);
        let mut ir = b.finish(acc);
        assert_eq!(verdict(&ir, &env, 1, 0, false), Verdict::HoldsStrongly);
        ir.root = rej;
        assert_eq!(verdict(&ir, &env, 1, 0, false), Verdict::Fails);
        // x true at tick 0 with the abort too: reject_on still fails (the abort takes
        // precedence), accept_on holds.
        let env = rows(&["1", "1"]);
        assert_eq!(verdict(&ir, &env, 1, 0, false), Verdict::Fails);
        // nested accept_on(a) reject_on(b) p1: a and b at the same tick -> succeeds;
        // b before a -> fails.
        let mut b = B::new();
        // p1 = strong(x ##5 x) is still being evaluated through all three ticks.
        let r = b.seq(&[0, 0], &[5]);
        let p1 = b.prop(Prop::Seq {
            seq: r,
            strength: Some(Strength::Strong),
        });
        let inner = b.prop(Prop::Abort {
            cond: LeafId(2),
            p: p1,
            mode: AbortMode::SyncReject,
        });
        let outer = b.prop(Prop::Abort {
            cond: LeafId(1),
            p: inner,
            mode: AbortMode::SyncAccept,
        });
        let ir = b.finish(outer);
        // leaves: 0 = x (always true), 1 = a, 2 = b
        let same = rows(&["111", "001", "001"]);
        assert_eq!(verdict(&ir, &same, 3, 0, false), Verdict::HoldsStrongly);
        let b_first = rows(&["111", "001", "010"]);
        assert_eq!(verdict(&ir, &b_first, 3, 0, false), Verdict::Fails);
        // a before b: the outer abort already accepted.
        let a_first = rows(&["111", "010", "001"]);
        assert_eq!(verdict(&ir, &a_first, 3, 0, false), Verdict::HoldsStrongly);
    }

    /// 16.12.14: `async` aborts also see conditions between ticks; the sync forms do
    /// not. The three formulations of the LRM example agree on tick-aligned traces,
    /// and only the async form reacts to a pulse between ticks.
    #[test]
    fn async_abort_sees_between_ticks_and_sync_does_not() {
        struct Between(Rows, Vec<u32>);
        impl PropEnv for Between {
            fn value(&self, l: LeafId, t: u32, f: &[Option<i64>]) -> Result<i64, TraceError> {
                self.0.value(l, t, f)
            }
            fn case_match(
                &self,
                s: LeafId,
                l: LeafId,
                t: u32,
                f: &[Option<i64>],
            ) -> Result<bool, TraceError> {
                self.0.case_match(s, l, t, f)
            }
            fn between(&self, leaf: LeafId, after: u32) -> Result<bool, TraceError> {
                Ok(leaf == LeafId(1) && self.1.contains(&after))
            }
        }
        let build = |mode| {
            let mut b = B::new();
            let r = b.seq(&[0, 2], &[1]);
            let p = b.prop(Prop::Seq {
                seq: r,
                strength: Some(Strength::Strong),
            });
            let r = b.prop(Prop::Abort {
                cond: LeafId(1),
                p,
                mode,
            });
            b.finish(r)
        };
        // x ##1 y with y never true; the abort pulses between tick 0 and tick 1 only.
        let fails = Between(rows(&["10", "00", "00"]), vec![0]);
        let ev =
            |ir: &PropertyIr, env: &Between| Evaluator::new(ir, env, false).verdict(2, 0).unwrap();
        // accept_on takes the pulse (the cut before tick 1 leaves `y` to the T tail);
        // sync_accept_on never samples it and `y` fails.
        assert_eq!(
            ev(&build(AbortMode::Accept), &fails),
            Verdict::HoldsStrongly
        );
        assert_eq!(ev(&build(AbortMode::SyncAccept), &fails), Verdict::Fails);
        // x ##1 y holds; the same pulse rejects it asynchronously, not synchronously.
        let holds = Between(rows(&["10", "00", "01"]), vec![0]);
        assert_eq!(ev(&build(AbortMode::Reject), &holds), Verdict::Fails);
        assert_eq!(
            ev(&build(AbortMode::SyncReject), &holds),
            Verdict::HoldsStrongly
        );
    }

    /// `if`/`case` on the two-valued letters: `⊤` takes the first arm, `⊥` the default.
    #[test]
    fn if_and_case_follow_the_condition() {
        let mut b = B::new();
        let t = b.b(1, Some(Strength::Strong));
        let e = b.b(2, Some(Strength::Strong));
        let i = b.prop(Prop::If {
            cond: LeafId(0),
            then: t,
            els: Some(e),
        });
        let ir = b.finish(i);
        assert_eq!(
            verdict(&ir, &rows(&["1", "1", "0"]), 1, 0, false),
            Verdict::HoldsStrongly
        );
        assert_eq!(
            verdict(&ir, &rows(&["0", "1", "0"]), 1, 0, false),
            Verdict::Fails
        );
        // case (l0) l1: p1; l2: p2; default: p3
        let mut b = B::new();
        let p1 = b.b(3, Some(Strength::Strong));
        let p2 = b.b(4, Some(Strength::Strong));
        let p3 = b.b(5, Some(Strength::Strong));
        let c = b.prop(Prop::Case {
            selector: LeafId(0),
            arms: vec![
                CaseArm {
                    labels: vec![LeafId(1)],
                    body: p1,
                },
                CaseArm {
                    labels: vec![LeafId(2)],
                    body: p2,
                },
            ],
            default: Some(p3),
        });
        let ir = b.finish(c);
        // selector equals label 2 only: p2.
        let env = rows(&["1", "0", "1", "0", "1", "0"]);
        assert_eq!(verdict(&ir, &env, 1, 0, false), Verdict::HoldsStrongly);
        // equals none: default p3 (selector 1, labels 0 and 0).
        let env = rows(&["1", "0", "0", "1", "1", "0"]);
        assert_eq!(verdict(&ir, &env, 1, 0, false), Verdict::Fails);
    }

    // ---- multiclock (16.13; sva T28) -------------------------------------------

    /// Leaf rows over the global steps of a trace, plus the tick lists of its
    /// clocks: `ClockId(c)` ticks at the steps where `ticks[c]` has a `1`.
    struct Multi {
        rows: Rows,
        timeline: Timeline,
    }

    impl PropEnv for Multi {
        fn value(&self, leaf: LeafId, tick: u32, f: &[Option<i64>]) -> Result<i64, TraceError> {
            self.rows.value(leaf, tick, f)
        }
        fn case_match(
            &self,
            selector: LeafId,
            label: LeafId,
            tick: u32,
            f: &[Option<i64>],
        ) -> Result<bool, TraceError> {
            self.rows.case_match(selector, label, tick, f)
        }
        fn timeline(&self) -> Option<&Timeline> {
            Some(&self.timeline)
        }
    }

    fn multi(leaves: &[&str], clocks: &[&str]) -> Multi {
        let bits: Vec<Vec<bool>> = clocks
            .iter()
            .map(|s| s.chars().map(|c| c == '1').collect())
            .collect();
        let refs: Vec<&[bool]> = bits.iter().map(Vec::as_slice).collect();
        Multi {
            rows: rows(leaves),
            timeline: Timeline::from_rows(&refs),
        }
    }

    fn multi_verdict(ir: &PropertyIr, env: &Multi) -> Verdict {
        Evaluator::new(ir, env, false)
            .verdict(env.timeline.real(), 0)
            .unwrap()
    }

    impl B {
        /// The one-letter sequence `leaf` on `clock`.
        fn leaf_on(&mut self, l: u32, clock: u32) -> SeqRef {
            let mut s = self.leaf(l);
            s.clock = ClockId(clock);
            s.end_clock = ClockId(clock);
            s
        }

        /// `l0 ##d @(clock to) l1`: the cross-clock synchronisation of 16.13.1.
        fn seq_sync(&mut self, l0: u32, l1: u32, to: u32, strict: bool) -> SeqRef {
            let entry = self.au.new_state();
            let s1 = self.au.new_state();
            let s2 = self.au.new_state();
            let s3 = self.au.new_state();
            self.au
                .add_edge(entry, Some(LeafId(l0)), Transition::Epsilon, s1);
            self.au.add_edge(
                s1,
                None,
                Transition::ClockSync {
                    to: ClockId(to),
                    strict,
                },
                s2,
            );
            self.au
                .add_edge(s2, Some(LeafId(l1)), Transition::Epsilon, s3);
            self.au.add_edge(
                s3,
                None,
                Transition::Match {
                    actions: Vec::new(),
                },
                s3,
            );
            SeqRef {
                entry,
                admits_empty: false,
                clock: ClockId(0),
                end_clock: ClockId(to),
            }
        }
    }

    /// 16.13.2: `@(clk) a |-> @(clk1) b` (clk = ClockId 0, clk1 = ClockId 1). The
    /// consequent starts at the nearest tick of clk1 at or after the end of the
    /// antecedent.
    #[test]
    fn overlapped_implication_awaits_the_nearest_tick_of_the_consequent_clock() {
        let mut b = B::new();
        let a = b.leaf_on(0, 0);
        let cons = b.leaf_on(1, 1);
        let c = b.prop(Prop::Seq {
            seq: cons,
            strength: Some(Strength::Strong),
        });
        let c = b.prop(Prop::Clocked {
            clock: ClockId(1),
            p: c,
        });
        let root = b.prop(Prop::Implication {
            ante: a,
            cons: c,
            overlapped: true,
        });
        let ir = b.finish(root);
        // clk ticks at 0 and 2, clk1 at 1 and 3; `a` holds at 0.
        let clocks = ["1010", "0101"];
        // b at clk1's first tick (step 1): holds.
        let env = multi(&["1000", "0100"], &clocks);
        assert_eq!(multi_verdict(&ir, &env), Verdict::HoldsStrongly);
        // b only at clk1's second tick (step 3): the consequent is checked at
        // step 1 and fails.
        let env = multi(&["1000", "0001"], &clocks);
        assert_eq!(multi_verdict(&ir, &env), Verdict::Fails);
        // b true at a step that is no tick of clk1 does not count.
        let env = multi(&["1000", "1010"], &clocks);
        assert_eq!(multi_verdict(&ir, &env), Verdict::Fails);
    }

    /// 16.13.2: `|=>` moves to the nearest STRICTLY LATER tick of the consequent's
    /// clock. Annex F's rewrite (`ante ##1 1 |-> cons`) advances one tick of the
    /// ANTECEDENT's clock first; the two differ when a clk1 tick falls between the
    /// end of the antecedent and the next clk tick, and the prose of 16.13.2 is the
    /// reading pinned here: `b` false at step 1 (the strictly later clk1 tick) fails
    /// even though it holds at step 2, which the rewrite would have checked.
    #[test]
    fn non_overlapped_implication_moves_to_the_strictly_later_consequent_tick() {
        let mut b = B::new();
        let a = b.leaf_on(0, 0);
        let cons = b.leaf_on(1, 1);
        let c = b.prop(Prop::Seq {
            seq: cons,
            strength: Some(Strength::Strong),
        });
        let c = b.prop(Prop::Clocked {
            clock: ClockId(1),
            p: c,
        });
        let root = b.prop(Prop::Implication {
            ante: a,
            cons: c,
            overlapped: false,
        });
        let ir = b.finish(root);
        // clk ticks at 0 and 2, clk1 at every step.
        let clocks = ["1010", "1111"];
        let env = multi(&["1000", "0100"], &clocks);
        assert_eq!(multi_verdict(&ir, &env), Verdict::HoldsStrongly);
        let env = multi(&["1000", "0010"], &clocks);
        assert_eq!(
            multi_verdict(&ir, &env),
            Verdict::Fails,
            "the consequent is checked at step 1, the next clk1 tick after the antecedent"
        );
        // clk1's tick at the end point itself (step 0) is not "strictly later":
        let env = multi(&["1000", "1000"], &clocks);
        assert_eq!(multi_verdict(&ir, &env), Verdict::Fails);
    }

    /// 16.13.1: `a ##1 @(clk1) b` waits for the first tick of clk1 strictly after
    /// the tick `a` matched at; `##0` allows the same step.
    #[test]
    fn cross_clock_delay_synchronises_to_the_other_clock() {
        let clocks = ["10100", "01011"];
        let mut b = B::new();
        let s = b.seq_sync(0, 1, 1, true);
        let root = b.prop(Prop::Seq {
            seq: s,
            strength: Some(Strength::Strong),
        });
        let ir = b.finish(root);
        // `a` at step 0; clk1's first tick strictly after is step 1.
        let env = multi(&["10000", "01000"], &clocks);
        assert_eq!(multi_verdict(&ir, &env), Verdict::HoldsStrongly);
        // `b` at step 3 (a later clk1 tick) does not match: the sync is to the
        // NEAREST tick.
        let env = multi(&["10000", "00010"], &clocks);
        assert_eq!(multi_verdict(&ir, &env), Verdict::Fails);
        // A non-strict (`##0`) sync with both clocks ticking at step 0 stays there.
        let clocks = ["1010", "1101"];
        let mut b = B::new();
        let s = b.seq_sync(0, 1, 1, false);
        let root = b.prop(Prop::Seq {
            seq: s,
            strength: Some(Strength::Strong),
        });
        let ir = b.finish(root);
        let env = multi(&["1000", "1000"], &clocks);
        assert_eq!(multi_verdict(&ir, &env), Verdict::HoldsStrongly);
    }

    mod calls;
    mod incremental;
    mod nonvacuity;
}