vj_sim/sva/

engine.rs

//! The live driver of one concurrent assertion (16.14, plan T29): turns the
//! simulator's per-time-step observations into the trace the reference
//! [`Evaluator`] runs on, and reports every evaluation attempt the moment it is
//! decided.
//!
//! The engine is scheduler-agnostic. Its owner calls
//!
//! * [`Engine::fire`] once per time step, in the Observed region (the engine
//!   copes with being called more than once per step), and
//! * [`Engine::end_of_step`] at the end of every time step with a snapshot of
//!   the signals the assertion reads, which is the Preponed (sampled) value of
//!   the next step (16.5.1),
//!
//! and everything that touches simulator state is behind [`Host`].
//!
//! ## The trace
//!
//! A *position* is a time step in which a clock of the assertion ticked (with a
//! single clock that is exactly its ticks, so the evaluator's `Timeline` is not
//! needed; with several, the positions are the union of the clocks' steps and a
//! `Timeline` says which clock ticked where). A position holds the sampled
//! signal row of its step, the current value of the `disable iff` condition
//! observed in it (16.12: not sampled), and `btw`: whether a current-valued
//! condition (the disable condition, an asynchronous `accept_on`/`reject_on`
//! condition) was true at some time step strictly after it and before the next
//! position -- the evaluator's `PropEnv::between`.
//!
//! Evaluation is stateless: every pending attempt is re-run over the whole window
//! from its start whenever a position is appended, which is exactly how the
//! reference evaluator is specified (a decided verdict is stable under
//! extension). The window is cut at the earliest pending attempt's start, so a
//! property that decides quickly keeps a window of a few positions.
//!
//! ## Limitations (documented in the plan's report)
//!
//! * A clock edge is the net change of the clock signal over a time step: a
//!   pulse that begins and ends inside one step is invisible, and a clock
//!   changed in the Reactive region of a step is seen in the next.
//! * A `disable iff` that becomes true after an attempt was decided in the same
//!   time step does not retroactively undo the report.
//! * A local variable of at most 64 bits is a two-state `i64` (an `x`/`z` bit
//!   assigned to it reads as 0/1); a wider one is four-state, in 64-bit limbs
//!   ([`super::wide`]), as is a wide value an instance captures.

use super::incremental::{Accel, automaton_span};
use super::ir::{AbortMode, CallId, ClockId, LeafId, LocalVarId};
use super::property::{Disposition, Evaluator, Prop, PropEnv, PropertyIr};
use super::trace::{Timeline, TraceError};
use crate::sched::assert_control::Q_ALL;
use crate::sched::with_sva_leaf_time;

/// What a concurrent assertion statement is (16.14.1-16.14.5).
#[derive(Clone, Copy, Debug, PartialEq, Eq)]
pub enum AssertKind {
    /// `assert property`: failures and successes run the action block.
    Assert,
    /// `assume property`: checked as `assert` in simulation (16.14.2).
    Assume,
    /// `cover property`: counts and runs the pass statement per successful
    /// attempt (16.14.3).
    CoverProperty,
    /// `cover sequence`: counts and runs the pass statement per match.
    CoverSequence,
    /// `restrict property`: never checked in simulation (16.14.5).
    Restrict,
    /// The `expect` statement (16.17): a procedural blocking statement that
    /// starts one evaluation thread on the clocking event strictly after its
    /// own step and reports its single outcome. Judged as an `assert` is.
    Expect,
}

/// What a decided attempt did.
#[derive(Clone, Copy, Debug, PartialEq, Eq)]
pub enum EventKind {
    /// The attempt succeeded (a vacuous success included).
    Pass,
    /// The attempt failed.
    Fail,
    /// One match of a `cover sequence` (16.14.3: counted with multiplicity).
    Match,
    /// A subroutine call attached to a sequence (16.11) reached an end point:
    /// [`Event::call`] says which, with the arguments sampled there. Reported
    /// the moment the end point is seen, which is before the attempt's own
    /// outcome when that is decided in the same pass.
    Call,
}

/// One executed subroutine call (16.11), the payload of an [`EventKind::Call`].
#[derive(Clone, Debug, PartialEq, Eq)]
pub struct CallFire {
    pub call: CallId,
    /// Per actual argument, the value sampled at the end point: `None` for a
    /// `ref` argument (bound at call time) and for a constant the kernel that
    /// runs the call lowers itself ([`CallArg`](super::ir::CallArg)).
    pub args: Vec<Option<i64>>,
}

/// One reported attempt outcome.
#[derive(Clone, Debug, PartialEq, Eq)]
pub struct Event {
    pub kind: EventKind,
    /// The attempt's ordinal (0-based) among the attempts this engine started.
    pub attempt: u64,
    /// Whether the success was vacuous (16.14.8: the attempt was not nonvacuous).
    /// Always `false` for a failure and for a `cover sequence` match.
    pub vacuous: bool,
    /// The values the attempt's instance captured when it was queued (16.14.6.1;
    /// empty for a static assertion), which its action block reads.
    pub values: Vec<i64>,
    /// The tag the attempt's instance was activated with
    /// ([`Engine::activate_tagged`]; 0 for [`Engine::activate`] and for a static
    /// assertion): which blocked process an `expect` outcome unblocks.
    pub tag: u64,
    /// The call of an [`EventKind::Call`]; `None` for every other kind.
    pub call: Option<CallFire>,
    /// The `Q_*` action flags ([`crate::sched::assert_control`]) in force when the
    /// attempt started: an assertion already executing is not affected by a later
    /// `$assertpassoff`/`$assertfailoff`/... (20.11), so the report filter reads
    /// these, not the current ones.
    pub flags: u32,
    /// With [`EngineConfig::future`], for a verdict: the time step of the tick
    /// the verdict was reached at, the attempt's last assertion clock tick
    /// (16.9.4: the verdict is reported at the global clock tick after it, but
    /// the attempt's interval ends at that tick). `None` otherwise.
    pub time: Option<u64>,
}

/// How a stepped attempt's step ended (39.4.2).
#[derive(Clone, Copy, Debug, PartialEq, Eq)]
pub enum StepOutcome {
    /// The attempt progressed and is still pending.
    Pending,
    /// The attempt reached its accepting state.
    Accept,
    /// The attempt failed to progress.
    Fail,
}

/// One step of an attempt whose stepping VPI enabled (39.4.2, 39.5.2): the
/// progress the newest clock tick made.
#[derive(Clone, Debug, PartialEq, Eq)]
pub struct StepRecord {
    /// The attempt's ordinal.
    pub attempt: u64,
    /// How many of the attempt's ticks came before this one (0: its first).
    pub index: u64,
    /// The time step of the tick.
    pub time: u64,
    /// The leaves read at this tick that held, in read order, each once; for
    /// a [`StepOutcome::Fail`], the leaf the attempt failed on last.
    pub matched: Vec<LeafId>,
    pub outcome: StepOutcome,
}

/// Running counters (16.14.3 for covers; the attempt counter includes disabled
/// attempts, the others do not).
#[derive(Clone, Copy, Debug, Default, PartialEq, Eq)]
pub struct Stats {
    pub attempted: u64,
    /// Successes, vacuous ones included (at most one per attempt).
    pub passed: u64,
    /// Of `passed`, the ones that were vacuous successes (16.14.8: "succeeded
    /// because of vacuity").
    pub vacuous: u64,
    pub failed: u64,
    pub disabled: u64,
    pub matched: u64,
    /// Attempts discarded by a control action (39.5.2 `vpiAssertionKill`,
    /// `$assertkill`).
    pub killed: u64,
}

/// The simulator, as the engine sees it. Every method is infallible: a host
/// failure is a bug in the codegen, not a runtime condition.
pub trait Host {
    /// Whether `clock` ticked this time step, given the previous step's final
    /// signal row `prev` (an edge is the change from `prev` to now).
    fn clock_ticked(&self, clock: ClockId, prev: &[u128]) -> bool;
    /// The value of a Boolean or value leaf over the sampled `row`, with the
    /// local-variable `frame` of the thread evaluating it (every local variable
    /// the leaf reads is assigned in it).
    fn leaf(&self, leaf: LeafId, row: &[u128], frame: &[i64]) -> i64;
    /// Whether case `label` selects `selector` (12.5 case equality).
    fn case_pair(&self, selector: LeafId, label: LeafId, row: &[u128], frame: &[i64]) -> bool;
    /// The CURRENT value of a live leaf (see [`live_leaves`]) as a truth value.
    /// `sampled` is the position-shaped row of this time step with
    /// [`EngineConfig::live_history`] (the step's sampled row, then each clock's
    /// history, as of before this step's ticks), else empty.
    fn live(&self, leaf: LeafId, sampled: &[u128]) -> bool;
    /// [`Self::live`] of every leaf of `leaves`, appended to `out` in order. A
    /// host that pays a fixed cost per query (a signal snapshot) answers all of
    /// them with one.
    /// [`Self::live`] of a leaf that also reads captured values, `frame` being
    /// the local-variable frame holding them (16.14.6.1). A host without such
    /// leaves never gets asked.
    fn live_with(&self, leaf: LeafId, sampled: &[u128], frame: &[i64]) -> bool {
        let _ = frame;
        self.live(leaf, sampled)
    }
    fn live_all(&self, leaves: &[LeafId], sampled: &[u128], out: &mut Vec<bool>) {
        out.extend(leaves.iter().map(|&l| self.live(l, sampled)));
    }
}

/// Everything the engine needs to know about one assertion.
#[derive(Clone)]
pub struct EngineConfig {
    pub ir: PropertyIr,
    pub kind: AssertKind,
    /// The number of distinct clocks of the assertion.
    pub n_clocks: usize,
    /// Per leaf, the local variables its expression reads (each must be assigned
    /// when the leaf is evaluated, 16.10).
    pub leaf_reads: Vec<Vec<LocalVarId>>,
    /// Per leaf, the local variable a PLAIN assignment match item (`v = e`)
    /// writes: the kernel is handed its frame slot but the variable need not be
    /// assigned yet (the item is what assigns it).
    pub leaf_writes: Vec<Option<LocalVarId>>,
    /// A procedural concurrent assertion (16.14.6) instead of a static one: its
    /// attempts start only for instances queued with [`Engine::activate`], not
    /// at every tick.
    pub activated: bool,
    /// The automaton local-variable slot of each value an instance captures
    /// (`Engine::activate`'s `values`, same order). Assigned when the attempt
    /// starts, so the leaves that read the captured items find them.
    pub captured: Vec<LocalVarId>,
    /// The `disable iff` condition reads captured values AND signals (16.12,
    /// 16.14.6.1). The condition is not a constant of the attempt, nor a pure
    /// signal: the engine evaluates it against the live signals once per
    /// distinct tuple of captured values ([`Host::live_with`]) and each attempt
    /// reads the record of its own tuple.
    pub disable_mixed: bool,
    /// How many previous clock ticks' rows a position carries behind its own
    /// (0: just the row). The sampled value functions of an assertion read
    /// them (16.9.3): `$rose`/`$fell`/`$stable`/`$changed` the previous tick's,
    /// `$past(x, n)` the n-th previous. A position's row handed to
    /// [`Host::leaf`] is then `(1 + history_depth) * row_len` entries long, the
    /// tick's own sampled row first, then the row of the previous tick, then the
    /// one before it, and so on. Before the first tick the previous rows are the
    /// initial row (16.5.1: the default sampled value is the initial one). Only
    /// a single-clock assertion has such a history: with several clocks the
    /// positions are the union of the clocks' ticks, not any one clock's.
    pub history_depth: usize,
    /// How many clocks past the assertion's own [`EngineConfig::n_clocks`] the
    /// host also tells the ticks of (`Host::clock_ticked` is asked for clocks
    /// `n_clocks..n_clocks + hist_clocks` too). They have a history block in a
    /// position's row like any clock but start no attempt and make no position:
    /// they are the clocking events (`$past(x, 1, , @(posedge fclk))`), gated
    /// events (`$past(x, 2, en)`) and global clock (`$rose_gclk(x)`) of the sampled
    /// value functions that are not the clock of their own leaf (16.9.3, 16.9.4).
    pub hist_clocks: usize,
    /// The property calls a global clocking future sampled value function
    /// (16.9.4): a position's row carries, after its history, the sampled row of
    /// the NEXT tick of [`EngineConfig::future_clock`] (the global clock) strictly
    /// after the position's time step. A position is therefore held back until
    /// that tick arrives, so every verdict, and the action it runs, comes at the
    /// global clock tick that follows the attempt's end, as the LRM requires; the
    /// attempt's interval is unchanged.
    pub future: bool,
    /// With [`EngineConfig::future`]: the global clock, one of the assertion's
    /// clocks or one of its history-only ones.
    pub future_clock: u32,
    /// A live leaf (the `disable iff` condition, an asynchronous abort condition)
    /// reads sampled values: [`Host::live`] is handed the position-shaped row of
    /// the current time step, the step's sampled row followed by every clock's
    /// history (16.12, 16.9.3: `$sampled(x)` and `$rose(x, @ev)` in a disable
    /// condition are meaningful since the condition itself is not sampled).
    pub live_history: bool,
    /// A clocking event's `iff` condition calls a sampled value function
    /// (16.9.3: legal when explicitly clocked): [`Host::clock_ticked`] is handed
    /// the position-shaped row of the step ([`Engine::tick_row`]), the step's
    /// sampled row followed by every clock's history as of before this step's
    /// ticks, instead of the sampled row alone.
    pub tick_history: bool,
}

/// The leaves whose CURRENT value (not the sampled one) the engine records at
/// every time step: the `disable iff` condition and every asynchronous
/// `accept_on`/`reject_on` condition, in a deterministic order.
pub fn live_leaves(ir: &PropertyIr) -> Vec<LeafId> {
    let mut out: Vec<LeafId> = Vec::new();
    let mut add = |l: LeafId| {
        if !out.contains(&l) {
            out.push(l);
        }
    };
    if let Some(d) = ir.disable {
        add(d);
    }
    for p in &ir.props {
        if let Prop::Abort { cond, mode, .. } = p
            && matches!(mode, AbortMode::Accept | AbortMode::Reject)
        {
            add(*cond);
        }
    }
    out
}

/// Why an engine could not be built.
#[derive(Clone, Debug, PartialEq, Eq)]
pub struct EngineError(pub String);

impl std::fmt::Display for EngineError {
    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
        f.write_str(&self.0)
    }
}

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

#[derive(Clone)]
struct Pos {
    /// The time step of the position.
    time: u64,
    /// The sampled signal row of this step (the previous step's final values).
    row: Row,
    /// Which clock ticked at this step.
    ticked: smallvec::SmallVec<[bool; 4]>,
    /// The disable condition's current value, OR-ed over this step's firings.
    disable_cur: bool,
    /// Per live leaf: true at some step strictly after this position.
    btw: Vec<bool>,
    /// With [`EngineConfig::disable_mixed`], per distinct captured tuple (index
    /// into `Engine::mixed_tuples`; absent = false): the condition's current
    /// value at this position, and whether it was true at some step after it.
    mixed_cur: Vec<bool>,
    mixed_btw: Vec<bool>,
    /// The value of each frame-independent leaf over `row`, once asked for (empty
    /// until the first one; then one slot per leaf).
    vals: std::cell::RefCell<smallvec::SmallVec<[Option<i64>; 4]>>,
}

/// A position's sampled row: inline for the usual few words, so a position
/// (made per tick per assertion) costs no heap allocation.
type Row = smallvec::SmallVec<[u128; 8]>;

#[derive(Clone)]
struct Attempt {
    id: u64,
    /// Absolute index of the start position.
    start: u64,
    /// The first absolute position whose cover-sequence matches have not been
    /// counted for this attempt yet.
    from: u64,
    /// The captured values of an activated instance.
    values: Vec<i64>,
    /// The activation's tag (see [`Event::tag`]).
    tag: u64,
    /// The first absolute position whose subroutine calls (16.11) have not been
    /// reported yet. A call is a function of the samples up to its own tick, so
    /// a longer trace only adds calls at the new positions.
    called_from: u64,
    /// The action flags at the start (see [`Event::flags`]).
    flags: u32,
}

/// An activated instance waiting for the next leading clock event.
#[derive(Clone)]
struct Matured {
    /// The time step it matured in (an `expect` starts strictly after it).
    at: u64,
    tag: u64,
    values: Vec<i64>,
}

/// One assertion's runtime state. A clone evaluates a step without touching
/// the original (a trial run, e.g. a checker's solution attempt, 17.7.2).
#[derive(Clone)]
pub struct Engine {
    cfg: EngineConfig,
    live: Vec<LeafId>,
    disable_live: Option<usize>,
    /// With [`EngineConfig::disable_mixed`]: the distinct tuples of captured
    /// values the instances so far carried, and the condition's value for each
    /// at the current step.
    mixed_tuples: Vec<Vec<i64>>,
    mixed_now: Vec<bool>,
    /// The previous step's final signal row.
    last_end: Vec<u128>,
    /// The ordinals of the attempts the last [`Engine::fire`] found disabled
    /// (`disable iff`), which report no [`Event`], each with the time step of
    /// the tick it was found disabled at (global clocking future sampled value
    /// functions only, 39.4.2.1).
    disabled_now: Vec<(u64, Option<u64>)>,
    /// With [`EngineConfig::future`]: the positions (oldest first) with their
    /// time step and whether the entry clock ticked there, waiting for the next
    /// tick of the future clock for their next row.
    held: std::collections::VecDeque<(Pos, u64, bool)>,
    /// With [`EngineConfig::live_history`]: the position-shaped row live leaves
    /// were handed in the current step ([`Host::live`]), kept so a second
    /// `fire` of the step sees the history as of before its ticks too.
    live_row: Vec<u128>,
    /// Per clock (history-only ones last), the rows of its last
    /// `cfg.history_depth` ticks, the latest first (see
    /// [`EngineConfig::history_depth`]).
    history: Vec<std::collections::VecDeque<Vec<u128>>>,
    positions: Vec<Pos>,
    /// Absolute index of `positions[0]`.
    base: u64,
    attempts: Vec<Attempt>,
    next_attempt: u64,
    step_time: Option<u64>,
    /// With [`EngineConfig::future`]: `(attempt, time)` of the attempts started
    /// since the last [`Engine::take_started`] (the clock tick the attempt
    /// started at, not the global clock tick it was released at).
    started: Vec<(u64, u64)>,
    /// Whether the step `step_time` pushed a position.
    step_is_tick: bool,
    /// Whether the entry clock ticked in the step `step_time`.
    step_starts: bool,
    /// Instances that matured (16.14.6) and wait for the next leading clock
    /// event.
    matured: Vec<Matured>,
    /// Something changed since the last evaluation (a late activation).
    dirty: bool,
    stats: Stats,
    /// Cover sequence: the longest a match can end past its start.
    span: Option<u32>,
    /// Per sequence instance the end-point methods test: its clock and how many
    /// of its ticks to keep before the earliest pending attempt, so that the
    /// instance's attempts that end there are still in the window (`None`: every
    /// position, [`super::ir::Automaton::end_point_lookback`]).
    lookback: Vec<(ClockId, Option<u32>)>,
    /// Whether the automaton attaches subroutine calls (16.11).
    has_calls: bool,
    /// [`super::incremental::automaton_span`] of the property, which every
    /// evaluator needs.
    auto_span: u32,
    /// Buffers [`Engine::fire`] reuses from one call to the next.
    scratch_live: Vec<bool>,
    scratch_ticked: Vec<bool>,
    /// An emptied attempts buffer [`Self::judge_all`] reuses for its output.
    spare: std::cell::RefCell<Vec<Attempt>>,
    /// Whether new attempts start of the engine's own accord (`$asserton`, as
    /// against `$assertoff`/`$assertkill`, 20.11).
    checking: bool,
    /// The action flags new attempts start with (see [`Event::flags`]).
    flags: u32,
    /// The incremental sequence evaluator the judging asks first (see
    /// [`super::incremental`]); `None` for a shape it does not model.
    accel: Option<std::cell::RefCell<Accel>>,
    /// VPI tracing (39.4.2); empty unless a VPI library asks for it.
    tracing: Tracing,
}

/// What VPI asked the engine to trace, and what it traced (39.4.2).
#[derive(Clone, Default)]
struct Tracing {
    /// The attempts whose steps are reported, with the newest absolute
    /// position each one's steps were reported up to.
    stepped: std::collections::HashMap<u64, Option<u64>>,
    /// Whether a failure reports the leaf it failed on (`failExpr`).
    fail_leaf: bool,
    /// Whether every attempt started from now on is stepped
    /// ([`Engine::set_step_new`]).
    step_new: bool,
    steps: Vec<StepRecord>,
    fail_leaves: Vec<(u64, Option<LeafId>)>,
}

/// Whether every evaluation also runs the reference evaluator, without the
/// incremental one, and asserts that it reports the same events, counters and
/// pending attempts (`VJ_SVA_DIFF=1`/`0`; by default on in debug builds,
/// which is every test).
fn differential() -> bool {
    static MODE: std::sync::OnceLock<bool> = std::sync::OnceLock::new();
    *MODE.get_or_init(|| match std::env::var("VJ_SVA_DIFF").as_deref() {
        Ok("0") => false,
        Ok(_) => true,
        Err(_) => cfg!(debug_assertions),
    })
}

/// Whether the incremental evaluator is used at all (`VJ_SVA_ACCEL=0`
/// turns it off, leaving the reference evaluator alone).
fn accel_enabled() -> bool {
    static MODE: std::sync::OnceLock<bool> = std::sync::OnceLock::new();
    *MODE.get_or_init(|| std::env::var("VJ_SVA_ACCEL").as_deref() != Ok("0"))
}

/// What one judging of every attempt yields: the events, the counters, the
/// attempts still pending, and the attempts a `disable iff` cut short.
type Judged = Result<(Vec<Event>, Stats, Vec<Attempt>, Vec<(u64, Option<u64>)>), TraceError>;

/// Panics unless the two judgings agree on everything observable.
fn assert_same_outcome(fast: &Judged, oracle: &Judged) {
    match (fast, oracle) {
        (Ok((ev, st, keep, dis)), Ok((ev0, st0, keep0, dis0))) => {
            let key = |k: &[Attempt]| -> Vec<(u64, u64, u64, u64)> {
                k.iter()
                    .map(|a| (a.id, a.start, a.from, a.called_from))
                    .collect()
            };
            assert_eq!(ev, ev0, "incremental SVA evaluation diverged: events");
            assert_eq!(st, st0, "incremental SVA evaluation diverged: counters");
            assert_eq!(
                key(keep),
                key(keep0),
                "incremental SVA evaluation diverged: pending attempts"
            );
            assert_eq!(
                dis, dis0,
                "incremental SVA evaluation diverged: disabled attempts"
            );
        }
        (Err(e), Err(e0)) => assert_eq!(e, e0, "incremental SVA evaluation diverged: error"),
        (Ok(_), Err(e0)) => {
            panic!("incremental SVA evaluation succeeded where the reference failed: {e0:?}")
        }
        (Err(e), Ok(_)) => {
            panic!("incremental SVA evaluation failed where the reference succeeded: {e:?}")
        }
    }
}

impl Engine {
    /// The row this step's tick samples: the previous step's final values.
    pub fn sampled_row(&self) -> &[u128] {
        &self.last_end
    }

    /// The row [`Host::clock_ticked`] reads (see [`EngineConfig::tick_history`]):
    /// the sampled row, or with a history-reading clocking event the position
    /// row.
    pub fn tick_row(&self) -> std::borrow::Cow<'_, [u128]> {
        if self.cfg.tick_history {
            std::borrow::Cow::Owned(self.position_row().into_vec())
        } else {
            std::borrow::Cow::Borrowed(&self.last_end)
        }
    }

    /// Overrides words of the sampled row with their current values: an active
    /// free checker variable's sampled value is its current one (17.7.2).
    pub fn set_sampled_words(&mut self, words: &[(usize, u128)]) {
        for &(i, w) in words {
            self.last_end[i] = w;
        }
    }

    pub fn new(cfg: EngineConfig, initial_row: Vec<u128>) -> Result<Self, EngineError> {
        let history = (0..(cfg.n_clocks + cfg.hist_clocks).max(1))
            .map(|_| std::iter::repeat_n(initial_row.clone(), cfg.history_depth).collect())
            .collect();
        let has_calls = cfg.ir.automaton.has_calls();
        if cfg.ir.automaton.end_points_have_calls() {
            return Err(EngineError(
                "a subroutine call (16.11) inside a sequence instance tested with `.triggered` or \
                 `.matched` is not executable: the instance's calls would have to run at its \
                 own end points, which the end-point status handoff does not carry"
                    .into(),
            ));
        }
        if has_calls && cfg.kind == AssertKind::Expect {
            return Err(EngineError(
                "a subroutine call (16.11) in the property of an `expect` statement is not \
                 executable: the statement blocks on its single outcome and the call would run \
                 in the Reactive region of a process that is still waiting for it"
                    .into(),
            ));
        }
        if has_calls && cfg.ir.props.iter().any(|p| matches!(p, Prop::Abort { .. })) {
            return Err(EngineError(
                "a subroutine call (16.11) in a property under `accept_on`/`reject_on` is not \
                 executable: the abort re-judges the attempt on a word cut at the abort, so \
                 which end points the calls ran at is not defined by the attempt alone"
                    .into(),
            ));
        }
        let mut live = live_leaves(&cfg.ir);
        // A `disable iff` condition over captured values (16.14.6.1) is a
        // constant of each attempt, judged per attempt, not recorded live.
        if let Some(d) = cfg.ir.disable
            && !cfg.leaf_reads[d.0 as usize].is_empty()
            && !cfg
                .ir
                .props
                .iter()
                .any(|p| matches!(p, Prop::Abort { cond, .. } if *cond == d))
        {
            live.retain(|&l| l != d);
        }
        let disable_live = cfg
            .ir
            .disable
            .and_then(|d| live.iter().position(|&l| l == d));
        let span = cfg.ir.automaton.max_span();
        let lookback = cfg.ir.automaton.end_point_lookback();
        let auto_span = automaton_span(&cfg.ir.automaton);
        let locals_read = cfg.leaf_reads.iter().any(|r| !r.is_empty());
        let accel = if accel_enabled() && !cfg.disable_mixed {
            Accel::new(&cfg.ir, cfg.n_clocks, has_calls, locals_read).map(std::cell::RefCell::new)
        } else {
            None
        };
        Ok(Engine {
            accel,
            tracing: Tracing::default(),
            lookback,
            cfg,
            live,
            disable_live,
            mixed_tuples: Vec::new(),
            mixed_now: Vec::new(),
            last_end: initial_row,
            disabled_now: Vec::new(),
            held: Default::default(),
            live_row: Vec::new(),
            history,
            positions: Vec::new(),
            base: 0,
            attempts: Vec::new(),
            next_attempt: 0,
            step_time: None,
            started: Vec::new(),
            step_is_tick: false,
            step_starts: false,
            matured: Vec::new(),
            dirty: false,
            stats: Stats::default(),
            span,
            has_calls,
            auto_span,
            scratch_live: Vec::new(),
            scratch_ticked: Vec::new(),
            spare: std::cell::RefCell::new(Vec::new()),
            checking: true,
            flags: Q_ALL,
        })
    }

    /// `$asserton`/`$assertoff` (20.11): whether a static assertion starts new
    /// attempts. A procedural one starts attempts only for instances that matured
    /// ([`Engine::activate`]); whether an instance is queued at all is decided
    /// where it is queued, so the flag does not hold back an instance already
    /// waiting for its clock.
    pub fn set_checking(&mut self, on: bool) {
        self.checking = on;
    }

    /// The action flags attempts started from now on carry (see
    /// [`Event::flags`]).
    pub fn set_action_flags(&mut self, flags: u32) {
        self.flags = flags;
    }

    /// `$assertkill` (20.11): aborts every executing attempt -- they report
    /// nothing and run no action -- and drops the matured instances still waiting
    /// to start. The statistics keep what they counted.
    pub fn kill(&mut self) {
        self.stats.killed += self.attempts.len() as u64;
        self.attempts.clear();
        self.matured.clear();
        self.trim();
    }

    pub fn kind(&self) -> AssertKind {
        self.cfg.kind
    }

    pub fn stats(&self) -> Stats {
        self.stats
    }

    /// The live leaves the host must be able to answer [`Host::live`] for.
    pub fn live_set(&self) -> &[LeafId] {
        &self.live
    }

    /// The signal row of the end of the time step that just finished: the
    /// sampled values of the next one.
    pub fn end_of_step(&mut self, row: Vec<u128>) {
        self.last_end = row;
    }

    /// [`Self::end_of_step`] that has `fill` write the row in place (over zeros),
    /// which saves the allocation of a row per step.
    pub fn end_of_step_with(&mut self, fill: impl FnOnce(&mut [u128])) {
        self.last_end.fill(0);
        fill(&mut self.last_end);
    }

    /// A procedural concurrent assertion instance matured in the Observed
    /// region of time step `now` (16.14.6), with the values it captured when the
    /// procedure reached it. When the leading clock ticked in this very step its
    /// attempt begins at once; otherwise the instance waits for the next tick.
    /// Call it before [`Engine::fire`] of the same step.
    pub fn activate(&mut self, now: u64, values: Vec<i64>) {
        self.activate_tagged(now, values, 0);
    }

    /// [`Engine::activate`] with a `tag` the attempt's [`Event`]s carry back.
    ///
    /// An [`AssertKind::Expect`] instance never starts in the step it was
    /// activated in, whether or not the leading clock ticked there: its first
    /// evaluation is on the *subsequent* clocking event (16.17).
    pub fn activate_tagged(&mut self, now: u64, values: Vec<i64>, tag: u64) {
        let strict = self.cfg.kind == AssertKind::Expect;
        self.register_tuple(&values);
        // A held position starts its instances when it is released.
        if !strict && !self.cfg.future && self.step_time == Some(now) && self.step_starts {
            self.start_attempt(values, tag);
            self.dirty = true;
        } else {
            self.matured.push(Matured {
                at: now,
                tag,
                values,
            });
        }
    }

    /// With [`EngineConfig::disable_mixed`]: makes `values` a tuple whose
    /// condition value the engine records from the next [`Engine::fire`] on.
    fn register_tuple(&mut self, values: &[i64]) {
        if self.cfg.disable_mixed && !self.mixed_tuples.iter().any(|t| t == values) {
            self.mixed_tuples.push(values.to_vec());
            self.dirty = true;
        }
    }

    /// The number of captured-value tuples whose `disable iff` value the engine
    /// records (see [`EngineConfig::disable_mixed`]); bounded by the live
    /// instances, which a long run's test observes.
    pub fn live_tuples(&self) -> usize {
        self.mixed_tuples.len()
    }

    /// Drops the tuples no instance can still ask about: the ones neither a
    /// pending attempt nor an instance waiting to start carries (16.14.6.1). A
    /// later instance with the same tuple registers it afresh, and it starts at
    /// the newest position, whose record it picks up on the next firing.
    fn prune_tuples(&mut self) {
        if self.mixed_tuples.is_empty() {
            return;
        }
        let keep: Vec<bool> = self
            .mixed_tuples
            .iter()
            .map(|t| {
                self.attempts.iter().any(|a| a.values == *t)
                    || self.matured.iter().any(|m| m.values == *t)
            })
            .collect();
        if keep.iter().all(|&k| k) {
            return;
        }
        let prune = |v: &mut Vec<bool>| {
            let mut i = 0;
            v.retain(|_| {
                let k = keep.get(i).copied().unwrap_or(true);
                i += 1;
                k
            });
        };
        let mut i = 0;
        self.mixed_tuples.retain(|_| {
            let k = keep[i];
            i += 1;
            k
        });
        prune(&mut self.mixed_now);
        for p in &mut self.positions {
            prune(&mut p.mixed_cur);
            prune(&mut p.mixed_btw);
        }
        for (p, _, _) in &mut self.held {
            prune(&mut p.mixed_cur);
            prune(&mut p.mixed_btw);
        }
    }

    /// Starts an attempt at the newest position.
    fn start_attempt(&mut self, values: Vec<i64>, tag: u64) {
        self.register_tuple(&values);
        let start = self.base + self.positions.len() as u64 - 1;
        self.attempts.push(Attempt {
            id: self.next_attempt,
            start,
            from: start,
            called_from: start,
            values,
            tag,
            flags: self.flags,
        });
        if self.cfg.future {
            let at = self.positions.last().map_or(0, |p| p.time);
            self.started.push((self.next_attempt, at));
        }
        if self.tracing.step_new {
            self.tracing.stepped.insert(self.next_attempt, None);
        }
        self.next_attempt += 1;
        self.stats.attempted += 1;
    }

    /// The Observed-region step at simulation time `now`. Returns the outcomes
    /// decided by it, in attempt-start order.
    /// Discards the attempt with ordinal `id` (VPI `vpiAssertionKill`, 39.5.2):
    /// it reports nothing; the assertion stays enabled. Whether it was pending.
    /// Turns step reporting for attempt `id` on or off (39.5.2
    /// `vpiAssertionEnableStep`/`vpiAssertionDisableStep`). Reported steps are
    /// collected by [`Engine::take_steps`].
    pub fn set_step(&mut self, id: u64, on: bool) {
        if on {
            self.tracing.stepped.entry(id).or_insert(None);
        } else {
            self.tracing.stepped.remove(&id);
        }
    }

    /// Whether every attempt that starts from now on has its steps reported
    /// (39.5.2: stepping requested for an attempt start time not reached
    /// yet). The caller turns it off again after the time step.
    pub fn set_step_new(&mut self, on: bool) {
        self.tracing.step_new = on;
    }

    /// Whether a failure records the leaf it failed on
    /// ([`Engine::take_fail_leaves`]).
    pub fn set_fail_leaf(&mut self, on: bool) {
        self.tracing.fail_leaf = on;
    }

    /// With [`EngineConfig::future`]: the start times of the attempts started
    /// since the last call, by attempt ordinal (empty otherwise).
    pub fn take_started(&mut self) -> Vec<(u64, u64)> {
        std::mem::take(&mut self.started)
    }

    /// The steps reported since the last call.
    pub fn take_steps(&mut self) -> Vec<StepRecord> {
        std::mem::take(&mut self.tracing.steps)
    }

    /// The failures reported since the last call with the leaf each failed on
    /// (`None` when it read none), by attempt ordinal.
    pub fn take_fail_leaves(&mut self) -> Vec<(u64, Option<LeafId>)> {
        std::mem::take(&mut self.tracing.fail_leaves)
    }

    pub fn kill_attempt(&mut self, id: u64) -> bool {
        let before = self.attempts.len();
        self.attempts.retain(|a| a.id != id);
        let killed = self.attempts.len() != before;
        if killed {
            self.stats.killed += (before - self.attempts.len()) as u64;
            self.trim();
        }
        killed
    }

    /// The ordinals of the attempts the last [`Engine::fire`] found disabled.
    pub fn disabled_attempts(&self) -> &[(u64, Option<u64>)] {
        &self.disabled_now
    }

    pub fn fire(&mut self, host: &dyn Host, now: u64) -> Result<Vec<Event>, TraceError> {
        self.disabled_now.clear();
        if self.cfg.kind == AssertKind::Restrict {
            return Ok(Vec::new());
        }
        let first = self.step_time != Some(now);
        self.step_time = Some(now);
        if first && self.cfg.live_history {
            // The step's sampled row and the histories as they are BEFORE this
            // step's ticks: a sampled value function reads strictly prior ticks.
            self.live_row = self.position_row().into_vec();
        }
        let mut live_now = std::mem::take(&mut self.scratch_live);
        live_now.clear();
        // The live values are read lazily: only a tick's position (its
        // `disable_cur`) or an attempt that can still start at or after the
        // newest position (its `btw` bits) ever consumes them, so a step in
        // which nothing is pending skips the signal snapshot they cost.
        let mut live_ready = false;
        let live_pending =
            !self.attempts.is_empty() || !self.held.is_empty() || !self.matured.is_empty();
        let mut pushed = false;
        let mut live_hit = false;
        self.mixed_now.clear();
        if self.cfg.disable_mixed
            && let Some(d) = self.cfg.ir.disable
        {
            // 16.12, 16.14.6.1: the condition over the live signals and each
            // tuple of captured values.
            let mut frame = vec![0i64; self.cfg.ir.automaton.local_vars.len()];
            for t in &self.mixed_tuples {
                for (slot, v) in self.cfg.captured.iter().zip(t) {
                    frame[slot.0 as usize] = *v;
                }
                self.mixed_now
                    .push(host.live_with(d, &self.live_row, &frame));
            }
        }
        let mut ticked = std::mem::take(&mut self.scratch_ticked);
        if first {
            self.step_is_tick = false;
            self.step_starts = false;
            ticked.clear();
            let tick_row = self.tick_row();
            ticked.extend(
                (0..self.cfg.n_clocks + self.cfg.hist_clocks)
                    .map(|c| host.clock_ticked(ClockId(c as u32), &tick_row)),
            );
            drop(tick_row);
            if ticked.iter().any(|&t| t) {
                // A position is a tick of one of the assertion's own clocks; the
                // tick of a history-only clock just records its row.
                let own = &ticked[..self.cfg.n_clocks];
                let entry = self.cfg.ir.automaton.entry_clock.0 as usize;
                let starts = own.get(entry).copied().unwrap_or(false);
                if !live_ready && !self.live.is_empty() {
                    host.live_all(&self.live, &self.live_row, &mut live_now);
                    live_ready = true;
                }
                let disable_cur = self.disable_live.is_some_and(|i| live_now[i]);
                // The position's row, then each clock's previous ticks' rows: a
                // sampled value function reads the history of its own clock
                // (16.9.3), which in a multiclock assertion is not the previous
                // position.
                let pos = own.iter().any(|&t| t).then(|| Pos {
                    time: now,
                    row: self.position_row(),
                    ticked: own.iter().copied().collect(),
                    disable_cur,
                    btw: vec![false; self.live.len()],
                    mixed_cur: self.mixed_now.clone(),
                    mixed_btw: Vec::new(),
                    vals: Default::default(),
                });
                if self.cfg.history_depth > 0 {
                    for (c, clock) in self.history.iter_mut().enumerate() {
                        if ticked.get(c).copied().unwrap_or(false) {
                            clock.push_front(self.last_end.clone());
                            clock.truncate(self.cfg.history_depth);
                        }
                    }
                }
                if pos.is_none() {
                    // No position here: the step is one between two positions.
                    if live_pending && !live_ready && !self.live.is_empty() {
                        host.live_all(&self.live, &self.live_row, &mut live_now);
                    }
                    live_hit |= self.record_between(&live_now);
                }
                if self.cfg.future
                    && ticked
                        .get(self.cfg.future_clock as usize)
                        .copied()
                        .unwrap_or(false)
                {
                    // This step's sampled row is the next row of every position
                    // held since an earlier step.
                    while let Some((mut prev, at, prev_starts)) = self.held.pop_front() {
                        prev.row.extend_from_slice(&self.last_end);
                        self.release(prev, at, prev_starts);
                        pushed = true;
                    }
                }
                if let Some(pos) = pos {
                    self.step_is_tick = true;
                    self.step_starts = starts;
                    if self.cfg.future {
                        self.held.push_back((pos, now, starts));
                    } else {
                        self.release(pos, now, starts);
                        pushed = true;
                    }
                }
            } else {
                if live_pending && !live_ready && !self.live.is_empty() {
                    host.live_all(&self.live, &self.live_row, &mut live_now);
                }
                live_hit |= self.record_between(&live_now);
            }
        } else if self.step_is_tick {
            if live_pending && !live_ready && !self.live.is_empty() {
                host.live_all(&self.live, &self.live_row, &mut live_now);
            }
            if let Some(i) = self.disable_live
                && live_now.get(i).copied().unwrap_or(false)
                && let Some(last) = self.newest_mut()
                && !last.disable_cur
            {
                last.disable_cur = true;
                live_hit = true;
            }
            let mixed = std::mem::take(&mut self.mixed_now);
            if let Some(last) = self.newest_mut() {
                for (i, &v) in mixed.iter().enumerate() {
                    if v && !last.mixed_cur.get(i).copied().unwrap_or(false) {
                        if last.mixed_cur.len() <= i {
                            last.mixed_cur.resize(i + 1, false);
                        }
                        last.mixed_cur[i] = true;
                        live_hit = true;
                    }
                }
            }
            self.mixed_now = mixed;
        } else {
            if live_pending && !live_ready && !self.live.is_empty() {
                host.live_all(&self.live, &self.live_row, &mut live_now);
            }
            live_hit |= self.record_between(&live_now);
        }
        self.scratch_live = live_now;
        self.scratch_ticked = ticked;
        if !pushed && !live_hit && !self.dirty {
            return Ok(Vec::new());
        }
        self.dirty = false;
        let events = self.evaluate(host)?;
        self.trim();
        Ok(events)
    }

    /// Appends the position of time step `at` to the window and starts the
    /// attempts that begin there.
    fn release(&mut self, pos: Pos, at: u64, starts: bool) {
        self.positions.push(pos);
        if !starts {
            return;
        }
        if self.cfg.activated {
            // An `expect` starts on a tick strictly after its activation; any
            // other instance on the first tick at or after it.
            let strict = self.cfg.kind == AssertKind::Expect;
            let (ready, later): (Vec<Matured>, Vec<Matured>) = std::mem::take(&mut self.matured)
                .into_iter()
                .partition(|m| if strict { m.at < at } else { m.at <= at });
            self.matured = later;
            for m in ready {
                self.start_attempt(m.values, m.tag);
            }
        } else if self.checking {
            self.start_attempt(Vec::new(), 0);
        }
    }

    /// The newest position: the last held one, or else the window's last.
    fn newest_mut(&mut self) -> Option<&mut Pos> {
        match self.held.back_mut() {
            Some((pos, _, _)) => Some(pos),
            None => self.positions.last_mut(),
        }
    }

    /// The row of a position made now: the step's sampled row, then every
    /// clock's history (see [`EngineConfig::history_depth`]).
    fn position_row(&self) -> Row {
        let mut row = Row::from_slice(&self.last_end);
        for clock in &self.history {
            for earlier in clock {
                row.extend_from_slice(earlier);
            }
        }
        row
    }

    fn record_between(&mut self, live_now: &[bool]) -> bool {
        let mixed = std::mem::take(&mut self.mixed_now);
        let Some(last) = self.newest_mut() else {
            self.mixed_now = mixed;
            return false;
        };
        let mut hit = false;
        for (i, &v) in live_now.iter().enumerate() {
            if v && !last.btw[i] {
                last.btw[i] = true;
                hit = true;
            }
        }
        for (i, &v) in mixed.iter().enumerate() {
            if v && !last.mixed_btw.get(i).copied().unwrap_or(false) {
                if last.mixed_btw.len() <= i {
                    last.mixed_btw.resize(i + 1, false);
                }
                last.mixed_btw[i] = true;
                hit = true;
            }
        }
        self.mixed_now = mixed;
        hit
    }

    /// Runs every pending attempt over the window; removes and reports the ones
    /// that are decided.
    fn evaluate(&mut self, host: &dyn Host) -> Result<Vec<Event>, TraceError> {
        if self.attempts.is_empty() {
            return Ok(Vec::new());
        }
        let len = self.positions.len() as u32;
        let timeline = if self.cfg.n_clocks > 1 {
            let ticks = (0..self.cfg.n_clocks)
                .map(|c| {
                    self.positions
                        .iter()
                        .enumerate()
                        .filter(|(_, p)| p.ticked[c])
                        .map(|(i, _)| i as u32)
                        .collect()
                })
                .collect();
            Some(Timeline::new(len, ticks)?)
        } else {
            None
        };
        let attempts = std::mem::take(&mut self.attempts);
        let oracle_input = (self.accel.is_some() && differential()).then(|| attempts.clone());
        if let Some(accel) = &self.accel {
            accel.borrow_mut().set_base(self.base);
        }
        let mut traced = Traced::default();
        let ran = self.judge_all(
            host,
            timeline.as_ref(),
            len,
            attempts,
            self.accel.as_ref(),
            Some(&mut traced),
        );
        if let Some(input) = oracle_input {
            let oracle = self.judge_all(host, timeline.as_ref(), len, input, None, None);
            assert_same_outcome(&ran, &oracle);
        }
        let (events, stats, keep, disabled) = ran?;
        self.record_traced(traced, len, &events);
        self.stats = stats;
        self.attempts = keep;
        self.disabled_now.extend(disabled);
        Ok(events)
    }

    /// Judges every attempt of `attempts` over the window of `len` positions: the
    /// events, the counters and the attempts still pending. `accel` is the
    /// incremental sequence evaluator the judging may use (`None`: the reference
    /// evaluator alone).
    fn judge_all(
        &self,
        host: &dyn Host,
        timeline: Option<&Timeline>,
        len: u32,
        attempts: Vec<Attempt>,
        accel: Option<&std::cell::RefCell<Accel>>,
        mut traced: Option<&mut Traced>,
    ) -> Judged {
        let strong = self.cfg.kind == AssertKind::CoverProperty;
        let mut events = Vec::new();
        let mut stats = self.stats;
        let mut keep = std::mem::take(&mut *self.spare.borrow_mut());
        keep.clear();
        let mut disabled = Vec::new();
        let env_for = |values: &[i64]| WindowEnv {
            host,
            positions: &self.positions,
            disable: self.cfg.ir.disable,
            live: &self.live,
            leaf_reads: &self.cfg.leaf_reads,
            leaf_writes: &self.cfg.leaf_writes,
            timeline,
            captured: &self.cfg.captured,
            values: values.to_vec(),
            mixed: self.cfg.disable_mixed.then_some(&self.mixed_tuples[..]),
            log: None,
        };
        let judge = Judge {
            kind: self.cfg.kind,
            span: self.span,
            multiclock: timeline.is_some(),
            has_calls: self.has_calls,
            base: self.base,
            len,
            times: if self.cfg.future {
                self.positions.iter().map(|p| p.time).collect()
            } else {
                Vec::new()
            },
        };
        // 39.4.2: an attempt VPI traces is judged on its own logging
        // environment by the reference evaluator, whose reads are its steps.
        let wants_trace =
            |att: &Attempt| self.tracing.fail_leaf || self.tracing.stepped.contains_key(&att.id);
        let (mut attempts, traced_atts): (Vec<Attempt>, Vec<Attempt>) = match traced.as_ref() {
            Some(_) if self.tracing.fail_leaf || !self.tracing.stepped.is_empty() => {
                attempts.into_iter().partition(|a| !wants_trace(a))
            }
            _ => (attempts, Vec::new()),
        };
        for att in traced_atts {
            let mut env = env_for(&att.values);
            env.log = Some(std::cell::RefCell::new(Vec::new()));
            let (id, start) = (att.id, att.start);
            {
                let ev = Evaluator::new_with_span(&self.cfg.ir, &env, strong, self.auto_span)
                    .open_future();
                judge.run(&ev, att, &mut events, &mut stats, &mut keep, &mut disabled)?;
            }
            if let (Some(t), Some(log)) = (traced.as_deref_mut(), env.log.take()) {
                t.logs.push((id, start, log.into_inner()));
            }
        }
        if self.cfg.captured.is_empty() {
            // Every attempt reads the same environment.
            let env = env_for(&[]);
            let ev = Evaluator::new_with_span(&self.cfg.ir, &env, strong, self.auto_span)
                .open_future()
                .with_accel(accel);
            for att in attempts.drain(..) {
                judge.run(&ev, att, &mut events, &mut stats, &mut keep, &mut disabled)?;
            }
        } else {
            // Each attempt starts with its own captured values.
            for att in attempts.drain(..) {
                let env = env_for(&att.values);
                let ev = Evaluator::new_with_span(&self.cfg.ir, &env, strong, self.auto_span)
                    .open_future()
                    .with_accel(accel);
                judge.run(&ev, att, &mut events, &mut stats, &mut keep, &mut disabled)?;
            }
        }
        // The emptied input buffer is the next judging's output buffer.
        *self.spare.borrow_mut() = attempts;
        Ok((events, stats, keep, disabled))
    }

    /// Drops the positions no pending attempt needs. An activated engine keeps
    /// the position of a tick step it is in: an instance can be activated after
    /// this step's [`Engine::fire`] -- a checker procedure runs in the Reactive
    /// region, after the Observed region this step's first `fire` ran in
    /// (17.7.3) -- and then starts its attempt at that position (16.14.6).
    fn trim(&mut self) {
        self.prune_tuples();
        let newest = if self.cfg.activated && self.step_starts && !self.positions.is_empty() {
            self.base + self.positions.len() as u64 - 1
        } else {
            self.base + self.positions.len() as u64
        };
        let keep_from = self
            .attempts
            .first()
            .map_or(newest, |a| a.start.min(newest));
        let mut keep_from = keep_from;
        for &(clock, span) in &self.lookback {
            let Some(n) = span else {
                // An unbounded instance: its every past start matters.
                keep_from = self.base;
                break;
            };
            let mut need = n + 1;
            let mut p = keep_from;
            while p > self.base && need > 0 {
                p -= 1;
                if self.positions[(p - self.base) as usize]
                    .ticked
                    .get(clock.0 as usize)
                    .copied()
                    .unwrap_or(true)
                {
                    need -= 1;
                }
            }
            keep_from = keep_from.min(p);
        }
        let drop_n = (keep_from - self.base) as usize;
        if drop_n == 0 {
            return;
        }
        self.positions.drain(..drop_n);
        self.base = keep_from;
        let base = self.base;
        if let Some(accel) = &self.accel {
            accel.borrow_mut().evict_before(base);
        }
    }
}

/// The leaf reads of the attempts judged with tracing in one pass: per
/// attempt, `(tick, leaf, value)` in read order.
#[derive(Default)]
struct Traced {
    /// `(attempt, start position, reads)`.
    logs: Vec<(u64, u64, LeafLog)>,
}

/// A traced attempt's leaf reads: `(tick, leaf, value)` in read order.
type LeafLog = Vec<(u32, LeafId, i64)>;

impl Engine {
    /// Turns one pass's leaf reads into step records and failure leaves.
    fn record_traced(&mut self, traced: Traced, len: u32, events: &[Event]) {
        if len == 0 {
            return;
        }
        let newest = len - 1;
        let abs_newest = self.base + u64::from(newest);
        for (id, start, log) in traced.logs {
            let failed = events
                .iter()
                .any(|e| e.attempt == id && e.kind == EventKind::Fail);
            let passed = events
                .iter()
                .any(|e| e.attempt == id && e.kind == EventKind::Pass);
            // The leaf the failure was decided on: the last one read false at
            // the newest tick, else the last one read at all.
            let fail_leaf = log
                .iter()
                .rev()
                .find(|(t, _, v)| *t == newest && *v == 0)
                .or_else(|| log.last())
                .map(|&(_, l, _)| l);
            if failed && self.tracing.fail_leaf {
                self.tracing.fail_leaves.push((id, fail_leaf));
            }
            let Some(reported) = self.tracing.stepped.get_mut(&id) else {
                continue;
            };
            // One step per tick, however often the step is judged; an attempt
            // whose stepping was enabled after it started (in its first time
            // step) catches up from its start.
            let first = reported.map_or(start, |r| r + 1);
            if first > abs_newest {
                continue;
            }
            *reported = Some(abs_newest);
            let outcome = if failed {
                StepOutcome::Fail
            } else if passed {
                StepOutcome::Accept
            } else {
                StepOutcome::Pending
            };
            for abs in first.max(self.base)..=abs_newest {
                let tick = (abs - self.base) as u32;
                let last = abs == abs_newest;
                let mut matched: Vec<LeafId> = Vec::new();
                for &(t, l, v) in &log {
                    if t == tick && v != 0 && !matched.contains(&l) {
                        matched.push(l);
                    }
                }
                let outcome = if last { outcome } else { StepOutcome::Pending };
                if outcome == StepOutcome::Fail
                    && let Some(l) = fail_leaf
                {
                    matched.retain(|&m| m != l);
                    matched.push(l);
                }
                self.tracing.steps.push(StepRecord {
                    attempt: id,
                    index: abs - start,
                    time: self.positions[tick as usize].time,
                    matched,
                    outcome,
                });
            }
            if outcome != StepOutcome::Pending {
                self.tracing.stepped.remove(&id);
            }
        }
    }
}

/// What one evaluation pass needs to judge an attempt.
struct Judge {
    kind: AssertKind,
    span: Option<u32>,
    /// The assertion has several clocks (16.13): the window is a [`Timeline`].
    multiclock: bool,
    has_calls: bool,
    base: u64,
    len: u32,
    /// With [`EngineConfig::future`]: the time step of each position of the
    /// window, to date a verdict (see [`Event::time`]); empty otherwise.
    times: Vec<u64>,
}

impl Judge {
    /// With global clocking future sampled value functions: the time step of
    /// the first tick of the window the attempt starting at `rel` was decided
    /// at (16.9.4), found as the shortest prefix of the window that already
    /// decides it. `None` without them, or when only the whole window does.
    fn verdict_time(&self, ev: &Evaluator<'_>, rel: u32) -> Result<Option<u64>, TraceError> {
        if self.times.is_empty() {
            return Ok(None);
        }
        for l in rel + 1..self.len {
            if !matches!(ev.attempt(l, rel)?, Disposition::Pending) {
                return Ok(self.times.get(l as usize - 1).copied());
            }
        }
        Ok(self.times.get(self.len as usize - 1).copied())
    }

    /// With global clocking future sampled value functions: the time step of
    /// window tick `t` (the last tick when `t` is past the window), else `None`.
    fn tick_time(&self, t: u32) -> Option<u64> {
        self.times
            .get(t as usize)
            .or_else(|| self.times.last())
            .copied()
    }

    /// Judges `att` on the window: reports it, drops it, or keeps it pending.
    fn run(
        &self,
        ev: &Evaluator<'_>,
        mut att: Attempt,
        events: &mut Vec<Event>,
        stats: &mut Stats,
        keep: &mut Vec<Attempt>,
        disabled: &mut Vec<(u64, Option<u64>)>,
    ) -> Result<(), TraceError> {
        let (len, kind) = (self.len, self.kind);
        let rel = (att.start - self.base) as u32;
        let event = |att: &Attempt, kind: EventKind| Event {
            kind,
            attempt: att.id,
            vacuous: false,
            values: att.values.clone(),
            tag: att.tag,
            call: None,
            flags: att.flags,
            time: None,
        };
        // 16.11: the calls attached to the sequences the attempt has run are
        // executed at their end points, ahead of the attempt's own report.
        if self.has_calls {
            let calls = match kind {
                AssertKind::CoverSequence => ev.sequence_calls(len, rel)?,
                AssertKind::Assert
                | AssertKind::Assume
                | AssertKind::CoverProperty
                | AssertKind::Expect => ev.scheduled_calls(len, rel)?,
                AssertKind::Restrict => unreachable!("a restrict property is never fired"),
            };
            for c in calls {
                if self.base + u64::from(c.tick) >= att.called_from {
                    events.push(Event {
                        call: Some(CallFire {
                            call: c.call,
                            args: c.args,
                        }),
                        ..event(&att, EventKind::Call)
                    });
                }
            }
            att.called_from = self.base + u64::from(len);
        }
        match kind {
            AssertKind::Assert
            | AssertKind::Assume
            | AssertKind::CoverProperty
            | AssertKind::Expect => {
                let report = kind != AssertKind::CoverProperty;
                match ev.attempt(len, rel)? {
                    Disposition::Pending => keep.push(att),
                    Disposition::Passes => {
                        // 16.14.8: a success that is not nonvacuous is a vacuous one.
                        let vacuous = !ev.nonvacuous(len, rel)?;
                        stats.passed += 1;
                        stats.vacuous += u64::from(vacuous);
                        events.push(Event {
                            vacuous,
                            time: self.verdict_time(ev, rel)?,
                            ..event(&att, EventKind::Pass)
                        });
                    }
                    Disposition::Fails => {
                        stats.failed += 1;
                        if report {
                            events.push(Event {
                                time: self.verdict_time(ev, rel)?,
                                ..event(&att, EventKind::Fail)
                            });
                        }
                    }
                    Disposition::Disabled => {
                        stats.disabled += 1;
                        let at = ev.disabling_prefix(len, rel)?;
                        disabled.push((att.id, at.and_then(|p| self.tick_time(p))));
                    }
                }
            }
            AssertKind::CoverSequence => {
                let disabled_at = ev.disabling_prefix(len, rel)?;
                let from = (att.from - self.base) as u32;
                for (end, _) in ev.root_sequence_matches(len, rel)? {
                    if end >= from && disabled_at.is_none_or(|p| end < p) {
                        stats.matched += 1;
                        events.push(Event {
                            time: self.tick_time(end),
                            ..event(&att, EventKind::Match)
                        });
                    }
                }
                att.from = self.base + u64::from(len);
                if let Some(p) = disabled_at {
                    stats.disabled += 1;
                    disabled.push((att.id, self.tick_time(p)));
                } else if self.multiclock {
                    // 16.13.1: positions are the union of the clocks' ticks, so the
                    // tick-count span says nothing; ask the timeline.
                    if !ev.sequence_exhausted(len, rel)? {
                        keep.push(att);
                    }
                } else if self.span.is_none_or(|s| len - 1 < rel.saturating_add(s)) {
                    keep.push(att);
                }
            }
            AssertKind::Restrict => unreachable!("a restrict property is never fired"),
        }
        Ok(())
    }
}

/// The window as a [`PropEnv`].
struct WindowEnv<'a> {
    host: &'a dyn Host,
    positions: &'a [Pos],
    disable: Option<LeafId>,
    live: &'a [LeafId],
    leaf_reads: &'a [Vec<LocalVarId>],
    leaf_writes: &'a [Option<LocalVarId>],
    timeline: Option<&'a Timeline>,
    /// The local-variable slots an instance's captured values are assigned to,
    /// and the values of the attempt being judged.
    captured: &'a [LocalVarId],
    values: Vec<i64>,
    /// With [`EngineConfig::disable_mixed`]: the tuples the condition is
    /// recorded for; the attempt reads the record of its own `values`.
    mixed: Option<&'a [Vec<i64>]>,
    /// When the attempt is traced (39.4.2): every leaf read, `(tick, leaf,
    /// value)`, in order.
    log: Option<std::cell::RefCell<Vec<(u32, LeafId, i64)>>>,
}

impl WindowEnv<'_> {
    fn note(&self, tick: u32, leaf: LeafId, v: i64) {
        if let Some(log) = &self.log {
            log.borrow_mut().push((tick, leaf, v));
        }
    }

    /// `frame` as the host's two-state frame, after checking that every local
    /// variable the leaves read is assigned.
    fn host_frame(&self, leaves: &[LeafId], frame: &[Option<i64>]) -> Result<Vec<i64>, TraceError> {
        for l in leaves {
            for v in &self.leaf_reads[l.0 as usize] {
                if frame.get(v.0 as usize).copied().flatten().is_none() {
                    return Err(TraceError::UnassignedRead(*v));
                }
            }
        }
        Ok(frame.iter().map(|v| v.unwrap_or(0)).collect())
    }

    /// The record index of this attempt's captured tuple, with a mixed
    /// `disable iff` condition (see [`EngineConfig::disable_mixed`]).
    fn mixed_index(&self) -> Option<usize> {
        self.mixed?.iter().position(|t| *t == self.values)
    }

    fn reads_locals(&self, leaf: LeafId) -> bool {
        !self.leaf_reads[leaf.0 as usize].is_empty() || self.leaf_writes[leaf.0 as usize].is_some()
    }
}

impl WindowEnv<'_> {
    fn value_of(&self, leaf: LeafId, tick: u32, frame: &[Option<i64>]) -> Result<i64, TraceError> {
        let pos = &self.positions[tick as usize];
        if Some(leaf) == self.disable
            && let Some(i) = self.mixed_index()
        {
            return Ok(i64::from(pos.mixed_cur.get(i).copied().unwrap_or(false)));
        }
        if Some(leaf) == self.disable && !self.reads_locals(leaf) {
            return Ok(i64::from(pos.disable_cur));
        }
        if !self.reads_locals(leaf) {
            let slot = leaf.0 as usize;
            if let Some(Some(v)) = pos.vals.borrow().get(slot) {
                return Ok(*v);
            }
            let v = with_sva_leaf_time(pos.time, || self.host.leaf(leaf, &pos.row, &[]));
            let mut vals = pos.vals.borrow_mut();
            if vals.is_empty() {
                vals.resize(self.leaf_reads.len(), None);
            }
            vals[slot] = Some(v);
            return Ok(v);
        }
        let f = self.host_frame(&[leaf], frame)?;
        Ok(with_sva_leaf_time(pos.time, || {
            self.host.leaf(leaf, &pos.row, &f)
        }))
    }
}

impl PropEnv for WindowEnv<'_> {
    fn value(&self, leaf: LeafId, tick: u32, frame: &[Option<i64>]) -> Result<i64, TraceError> {
        let v = self.value_of(leaf, tick, frame)?;
        if Some(leaf) != self.disable {
            self.note(tick, leaf, v);
        }
        Ok(v)
    }

    fn case_match(
        &self,
        selector: LeafId,
        label: LeafId,
        tick: u32,
        frame: &[Option<i64>],
    ) -> Result<bool, TraceError> {
        let f = self.host_frame(&[selector, label], frame)?;
        let m = self
            .host
            .case_pair(selector, label, &self.positions[tick as usize].row, &f);
        self.note(tick, selector, 1);
        self.note(tick, label, i64::from(m));
        Ok(m)
    }

    fn between(&self, leaf: LeafId, after: u32) -> Result<bool, TraceError> {
        if Some(leaf) == self.disable
            && let Some(i) = self.mixed_index()
        {
            return Ok(self.positions[after as usize]
                .mixed_btw
                .get(i)
                .copied()
                .unwrap_or(false));
        }
        let Some(i) = self.live.iter().position(|&l| l == leaf) else {
            return Ok(false);
        };
        Ok(self.positions[after as usize].btw[i])
    }

    fn timeline(&self) -> Option<&Timeline> {
        self.timeline
    }

    fn initial_frame(&self) -> Vec<(LocalVarId, i64)> {
        self.captured
            .iter()
            .copied()
            .zip(self.values.iter().copied())
            .collect()
    }
}

#[cfg(test)]
mod tests;