concolic_core/

lib.rs

//! The architecture-neutral half of the concolic pipeline.
//!
//! Every item in this crate is stated over **traces, decisions and reports**.
//! None names an instruction set, a register, a syscall number, or a cell
//! layout. A frontend (an ISA, a bytecode VM, a symbolic runtime, ...) supplies:
//!
//! - a deterministic concrete reference run ([`Frontend::run`]),
//! - a symbolic walk forced along a concrete branch log ([`Frontend::walk`]),
//! - the flip query at one decision ([`Frontend::flip`]),
//! - the symbolic surface's names in a model, and how to apply them
//!   ([`Frontend::model_inputs`], [`Frontend::apply_inputs`]).
//!
//! Everything else - the frontier, the budgets, the verification predicate
//! ("same sites, same directions, opposite at the flipped site"), the seven
//! flip outcomes and the report - is fixed here. A path only counts when the
//! frontend's own reference engine re-ran the model and agreed; a `Sat` model
//! alone is never a witness.

use std::collections::BTreeSet;

use smtlite::{Model, Solution};

/// One decision in a concrete trace: the site and the direction taken.
///
/// Operand **values** are deliberately absent. A changed input necessarily
/// changes the operands of earlier comparisons that still go the same way, so a
/// verification predicate that compared whole records would reject genuine
/// flips. Sites and directions are the path.
#[derive(Clone, Copy, Debug, PartialEq, Eq)]
pub struct BranchRec {
    /// The decision site (an address in every frontend so far).
    pub site: u64,
    /// Whether the branch was taken.
    pub taken: bool,
}

/// What an attempted flip actually reached.
#[derive(Clone, Copy, Debug, Default, PartialEq, Eq, PartialOrd, Ord)]
pub enum FlipOutcome {
    /// The reference engine took the opposite side at the same site, with the
    /// same prefix decisions, and the resulting path was new.
    Verified,
    /// The flip query was UNSAT under the path prefix: no input flips it here.
    ProvenUnflippable,
    /// The solver hit a bound before a verdict.
    SolverUnknown,
    /// No verification run was spent, or no query was built. The loop records a
    /// walk that cannot replay the path as a gap instead of inventing a
    /// per-decision record; this value is the honest default for a consumer
    /// that records an attempt it could not pose.
    #[default]
    NotPosed,
    /// The flipped run failed at the engine level.
    RunFailed,
    /// The run failed to reproduce the walked prefix and take the opposite
    /// side at this decision: its log was too short, diverged before the
    /// decision, reached a different site, or took the same side. The walker
    /// and the engine disagree.
    Unconfirmed,
    /// The run did take the opposite side, but the path was already seen.
    AlreadyExplored,
}

/// One flip attempt, in decision order.
#[derive(Clone, Debug, Default)]
pub struct FlipRec {
    /// The site the attempt was posed at.
    pub at: u64,
    /// The model's bindings over the frontend's symbolic surface, as opaque
    /// name/value pairs.
    pub input: Vec<(String, u64)>,
    /// Whether the reference engine verified the flip onto a new path.
    pub verified: bool,
    /// The structured outcome.
    pub outcome: FlipOutcome,
}

/// A property query's outcome (the same algebra every frontend's engine uses).
#[derive(Clone, Copy, Debug, Default, PartialEq, Eq, PartialOrd, Ord)]
pub enum PropertyOutcome {
    /// Sat model, applied and re-run: the concrete readback violates the invariant.
    Confirmed,
    /// UNSAT under the path formula: no reaching input violates it.
    Proven,
    /// The solver hit a bound.
    SolverUnknown,
    /// No verification run was spent, or no query was built.
    #[default]
    NotPosed,
    /// The verification re-run trapped, or failed at the engine level, so there
    /// is no post-state to judge.
    RunFailed,
    /// The model was applied, the run completed, and it did not violate.
    Unreproduced,
}

/// One property-directed query on one walked path.
#[derive(Clone, Debug, Default)]
pub struct PropertyRec {
    /// The assertion's label.
    pub label: String,
    /// What the query reached.
    pub outcome: PropertyOutcome,
    /// The observed operands on a confirmed violation.
    pub violation: Option<(u64, u64)>,
    /// The applied input, when a model was re-run.
    pub input: Vec<(String, u64)>,
}

/// A sink reached on a walked path. The `kind` and argument names are the
/// frontend's vocabulary; the ledger treats them as opaque labels.
#[derive(Clone, Debug, Default)]
pub struct SinkRec {
    /// The call site.
    pub site: u64,
    /// The sink class. The frontend chooses these labels; the ledger treats
    /// them as opaque strings (e.g. `transfer`, `log`, `call`).
    pub kind: String,
    /// Argument names and their concrete values on the walked path.
    pub args: Vec<(String, u64)>,
}

/// The outcome of one concrete reference run.
#[derive(Clone, Debug, Default)]
pub struct RunResult {
    /// The program's own return value, when it returned.
    pub result: Option<i64>,
    /// The trap text, when the run trapped instead of returning.
    pub trapped: Option<String>,
    /// The decisions the run made, in order.
    pub log: Vec<BranchRec>,
    /// Sinks reached. The loop does not read this field; it reports the sinks
    /// its own walks found through [`Frontend::walk_sinks`].
    pub sinks: Vec<SinkRec>,
}

/// The session report - the architecture-neutral subset of the engine report
/// that a consumer (a diagnosis layer, a CI gate, a notebook) reads.
#[derive(Clone, Debug, Default)]
pub struct Report {
    /// The base run's result, when it returned.
    pub result: Option<i64>,
    /// Concrete runs attempted, including attempts that failed at the engine
    /// level.
    pub runs: usize,
    /// Flips the reference engine verified.
    pub flips_verified: usize,
    /// Sinks reached.
    pub sinks: Vec<SinkRec>,
    /// Property queries posed.
    pub properties: Vec<PropertyRec>,
    /// Every flip attempt.
    pub flips: Vec<FlipRec>,
    /// Gap notes, verbatim: the frontend's own walk notes plus the loop's own
    /// limit notes (`run failed: ...`, `run trapped: ...`, `walk could not
    /// replay ...`, `solver Unknown at ...`).
    pub gaps: Vec<String>,
    /// The frontier emptied with no work left undone. A session whose budget
    /// cut the decision loop short, refused a property verification, or could
    /// not walk a discovered path is NOT exhausted, even if every path it did
    /// process was processed to the end.
    pub exhausted: bool,
}

/// The budgets a session ran under.
#[derive(Clone, Copy, Debug, PartialEq, Eq)]
pub struct Opts {
    /// Cap on concrete runs. The base run is always attempted (a report always
    /// says what it tried); every later attempt is refused once `runs` reaches
    /// this value.
    pub max_runs: usize,
    /// Cap on verified flips. Reaching it ends the search.
    pub max_flips: usize,
}

impl Default for Opts {
    fn default() -> Self {
        Self {
            max_runs: 64,
            max_flips: 32,
        }
    }
}

/// What a frontend must provide for the loop to run.
///
/// The obligations are the soundness contract: `run` is deterministic, `walk`
/// is a sound over-approximation of `run`'s prefix, `flip` poses the query at a
/// real decision and `site` names it, and `model_inputs`/`apply_inputs`
/// round-trip a model onto a runnable seed.
///
/// Two further preconditions the loop relies on but cannot check:
///
/// - a `Some(walk)` must expose at least `log.len()` decisions: the loop
///   indexes `site` and `flip` over `0..log.len()`, so a shorter walk is a
///   frontend bug that will surface as a panic inside the frontend, not as a
///   gap;
/// - every seed in one session must share the same symbolic surface, because
///   a path is identified by its `(site, taken)` decisions alone. Across
///   different frontends or different input surfaces, call [`explore`]
///   separately.
pub trait Frontend {
    /// The seed: the initial state, with its base concrete assignment.
    type Seed: Clone;
    /// The symbolic walk, owning whatever solver state the frontend keeps.
    type Walk;

    /// Run the reference engine concretely. Determinism is the frontend's
    /// obligation; an engine-level failure is `Err`, not a trap.
    fn run(&self, seed: &Self::Seed) -> Result<RunResult, String>;

    /// Replay the concrete log symbolically. `None` when the walk cannot force
    /// the path (a replay or frontend limitation); the caller records that fact.
    fn walk(&self, seed: &Self::Seed, log: &[BranchRec]) -> Option<Self::Walk>;

    /// Pose the flip query at decision `i` of the forced walk.
    fn flip(&self, walk: &mut Self::Walk, i: usize) -> Solution;

    /// The decision site at index `i` of the walk.
    fn site(&self, walk: &Self::Walk, i: usize) -> u64;

    /// The model's bindings over the symbolic surface.
    fn model_inputs(&self, model: &Model, walk: &Self::Walk) -> Vec<(String, u64)>;

    /// Apply those bindings to a child seed.
    fn apply_inputs(&self, seed: &Self::Seed, inputs: &[(String, u64)]) -> Self::Seed;

    /// Gap notes the walk itself recorded (unsupported instruction, replay
    /// drift, ...).
    fn walk_gaps(&self, _walk: &Self::Walk) -> Vec<String> {
        Vec::new()
    }

    /// Sinks reached on the walked path.
    fn walk_sinks(&self, _walk: &Self::Walk) -> Vec<SinkRec> {
        Vec::new()
    }

    // -- optional property surface -------------------------------------------

    /// The property-query labels this frontend poses at the end of a walked
    /// path. Empty by default.
    ///
    /// A property query asks the end-state question `path AND NOT invariant`,
    /// so a violation on a straight-line path with no decision to flip is
    /// still expressible. A frontend with no property surface leaves this
    /// empty and its property ledger stays empty.
    ///
    /// Queries are posed only on paths whose reference run completed. When
    /// the run trapped, the loop records every declared label as
    /// [`PropertyOutcome::NotPosed`]: there is no post-state to read, so the
    /// question is vacuous rather than refused, and the ledger still shows
    /// that the frontend declared it.
    fn properties(&self, _walk: &Self::Walk) -> Vec<String> {
        Vec::new()
    }

    /// Pose `label` over the walked path: `path AND NOT invariant`.
    ///
    /// `Unsat` is a local negative under this path's assumptions. `Sat` is a
    /// candidate, never a finding - the loop re-runs its model and asks
    /// [`Frontend::property_violated`] before believing it.
    fn check_property(&self, _walk: &mut Self::Walk, _label: &str) -> Solution {
        Solution::Unknown
    }

    /// Read the verification re-run's post-state for `label`. `Some((observed,
    /// required))` only when the run completed and its concrete readback
    /// violates the property. Called only on a run that did not trap.
    fn property_violated(&self, _run: &RunResult, _label: &str) -> Option<(u64, u64)> {
        None
    }
}

/// A path's identity: every decision's site and direction, in order.
///
/// Directions alone are not an identity. Two runs can take the same side of
/// the same number of decisions and still be different paths when the
/// decision *sites* differ (an indirect branch, a dispatch table, a virtual
/// call), so a key made of `taken` bits alone would discard the second path
/// as already explored.
type PathKey = Vec<(u64, bool)>;

fn path_key(log: &[BranchRec]) -> PathKey {
    log.iter().map(|b| (b.site, b.taken)).collect()
}

struct Pending<S> {
    seed: S,
    run: RunResult,
}

struct Attempt<S> {
    rec: FlipRec,
    verified: bool,
    ran: bool,
    gap: Option<String>,
    child: Option<Pending<S>>,
}

/// Explore the frontend's entry point from `base` inside the budgets.
///
/// The loop is the DART/CUTE shape: run, replay the path symbolically, pose a
/// flip query at every decision (deepest first), apply a model, re-run, verify.
/// A verified flip pushes the child path onto the frontier; the frontier
/// emptying inside the budgets sets `exhausted`.
#[must_use]
pub fn explore<F: Frontend>(frontend: &F, base: &F::Seed, opts: &Opts) -> Report {
    let mut report = Report::default();
    let mut seen: BTreeSet<PathKey> = BTreeSet::new();

    // `runs` counts attempts, not successes: a report always says what it
    // tried, including a base run the engine could not perform.
    report.runs = 1;
    let first = match frontend.run(base) {
        Ok(r) => r,
        Err(e) => {
            report.gaps.push(format!("run failed: {e}"));
            return report;
        }
    };
    // A trapped run has no return value; the trap itself is the observation.
    if first.trapped.is_none() {
        report.result = first.result;
    }
    // `seen` holds every path the search has DISCOVERED - the base and every
    // verified child, whether or not it has been popped. A path sitting on the
    // frontier is already accounted for: checking only processed paths would
    // let a later flip claim the same child as new, enqueue it twice, and
    // inflate `flips_verified`.
    seen.insert(path_key(&first.log));
    let mut frontier = vec![Pending { seed: base.clone(), run: first }];

    // Set when work the search was supposed to do could not be done: a budget
    // refused a decision or a property verification, or a discovered path
    // could not be walked at all. The frontier can empty in that state, but
    // it did not empty *by completing the search*: remaining work was
    // refused or unanalysable, so the session is not exhausted.
    let mut incomplete = false;

    while let Some(item) = frontier.pop() {
        if report.runs >= opts.max_runs || report.flips_verified >= opts.max_flips {
            return report;
        }
        if let Some(t) = &item.run.trapped {
            report.gaps.push(format!("run trapped: {t}"));
        }
        let Some(mut walk) = frontend.walk(&item.seed, &item.run.log) else {
            // A discovered path was dropped unanalysed. That is recorded as a
            // gap AND it means the search did not complete: the frontier will
            // empty with this path's decisions never posed.
            report
                .gaps
                .push("walk could not replay the concrete path".to_string());
            incomplete = true;
            continue;
        };
        report.sinks.extend(frontend.walk_sinks(&walk));
        report.gaps.extend(frontend.walk_gaps(&walk));

        // Deepest decision first, with the budgets checked against what this
        // round has already spent - the same exact-cap discipline the
        // reference engines record.
        let (mut spent, mut flipped) = (0usize, 0usize);

        // Property-directed queries: the end-state question, posed on every
        // path the walker replayed. A verification run spent here counts
        // against the same budget as a flip's.
        for label in frontend.properties(&walk) {
            if item.run.trapped.is_some() {
                // There is no post-state to ask about, so the query is
                // vacuous rather than refused. Record the label as `NotPosed`
                // rather than dropping it: a ledger that omits a declared
                // query reads as "no property surface", which is a different
                // fact.
                report.properties.push(PropertyRec {
                    label,
                    ..PropertyRec::default()
                });
                continue;
            }
            let (rec, ran, skipped) = pose_property(
                frontend,
                &item.seed,
                &mut walk,
                &label,
                report.runs,
                opts,
            );
            report.runs += usize::from(ran);
            incomplete |= skipped;
            report.properties.push(rec);
        }
        let mut attempts = Vec::new();
        for i in (0..item.run.log.len()).rev() {
            if report.runs + spent >= opts.max_runs
                || report.flips_verified + flipped >= opts.max_flips
            {
                // Decisions remain unposed. The frontier may empty later, but
                // the search was cut short, not completed.
                incomplete = true;
                break;
            }
            let a = attempt(frontend, &item.seed, &item.run.log, &mut walk, i, &seen);
            spent += usize::from(a.ran);
            flipped += usize::from(a.verified);
            // Record the child's path immediately: a later attempt in this
            // same round must see it, or two flips can both call it new.
            if a.verified {
                if let Some(child) = &a.child {
                    seen.insert(path_key(&child.run.log));
                }
            }
            attempts.push(a);
        }

        for a in attempts {
            report.runs += usize::from(a.ran);
            if let Some(g) = a.gap {
                report.gaps.push(g);
            }
            report.flips.push(a.rec);
            if a.verified {
                report.flips_verified += 1;
                if let Some(child) = a.child {
                    frontier.push(child);
                }
            }
        }
    }
    report.exhausted = !incomplete;
    report
}

/// Pose and discharge one property query.
///
/// Returns `(rec, ran, skipped)`: `ran` says whether a concrete verification
/// run was spent, and `skipped` says a satisfiable query went unanswered only
/// because the run budget refused its verification run.
///
/// The witness law is the same one the flip search obeys: a `Sat` model is a
/// candidate, and only the frontend's own re-run readback can confirm it. A
/// `Sat` model with no budget left for the re-run is `NotPosed`, not a
/// finding.
fn pose_property<F: Frontend>(
    frontend: &F,
    seed: &F::Seed,
    walk: &mut F::Walk,
    label: &str,
    runs_spent: usize,
    opts: &Opts,
) -> (PropertyRec, bool, bool) {
    let mut rec = PropertyRec {
        label: label.to_string(),
        outcome: PropertyOutcome::NotPosed,
        violation: None,
        input: Vec::new(),
    };
    match frontend.check_property(walk, label) {
        Solution::Unsat => rec.outcome = PropertyOutcome::Proven,
        Solution::Unknown => rec.outcome = PropertyOutcome::SolverUnknown,
        Solution::Sat(model) => {
            if runs_spent >= opts.max_runs {
                return (rec, false, true);
            }
            let inputs = frontend.model_inputs(&model, walk);
            let child_seed = frontend.apply_inputs(seed, &inputs);
            rec.input = inputs;
            // A run that trapped has no post-state for the invariant to be
            // read off; that is a failed verification, not a violation.
            match frontend.run(&child_seed) {
                Ok(run) if run.trapped.is_none() => {
                    match frontend.property_violated(&run, label) {
                        Some(violation) => {
                            rec.outcome = PropertyOutcome::Confirmed;
                            rec.violation = Some(violation);
                        }
                        None => rec.outcome = PropertyOutcome::Unreproduced,
                    }
                }
                _ => rec.outcome = PropertyOutcome::RunFailed,
            }
            return (rec, true, false);
        }
    }
    (rec, false, false)
}

fn attempt<F: Frontend>(
    frontend: &F,
    seed: &F::Seed,
    log: &[BranchRec],
    walk: &mut F::Walk,
    i: usize,
    seen: &BTreeSet<PathKey>,
) -> Attempt<F::Seed> {
    let at = frontend.site(walk, i);
    let solution = frontend.flip(walk, i);
    let Solution::Sat(m) = &solution else {
        let outcome = match solution {
            Solution::Unsat => FlipOutcome::ProvenUnflippable,
            Solution::Unknown => FlipOutcome::SolverUnknown,
            _ => FlipOutcome::NotPosed,
        };
        let gap = (outcome == FlipOutcome::SolverUnknown)
            .then(|| format!("solver Unknown at {at:#x}"));
        return Attempt {
            rec: FlipRec { at, input: Vec::new(), verified: false, outcome },
            verified: false,
            ran: false,
            gap,
            child: None,
        };
    };

    let inputs = frontend.model_inputs(m, walk);
    let child_seed = frontend.apply_inputs(seed, &inputs);
    let child_run = match frontend.run(&child_seed) {
        Ok(r) => r,
        Err(_) => {
            return Attempt {
                rec: FlipRec {
                    at,
                    input: inputs,
                    verified: false,
                    outcome: FlipOutcome::RunFailed,
                },
                verified: false,
                ran: true,
                gap: None,
                child: None,
            };
        }
    };

    // Verification: the SAME sites in the SAME directions up to decision `i`,
    // and the opposite direction at `i`. Operand values are not compared.
    let prefix_ok = child_run.log.len() > i
        && child_run.log[..i]
            .iter()
            .zip(&log[..i])
            .all(|(c, p)| c.site == p.site && c.taken == p.taken);
    let flipped =
        prefix_ok && child_run.log[i].site == log[i].site && child_run.log[i].taken != log[i].taken;

    let child_path = path_key(&child_run.log);
    let verified = flipped && !seen.contains(&child_path);
    let outcome = if verified {
        FlipOutcome::Verified
    } else if flipped {
        FlipOutcome::AlreadyExplored
    } else {
        FlipOutcome::Unconfirmed
    };

    Attempt {
        rec: FlipRec { at, input: inputs, verified, outcome },
        verified,
        ran: true,
        gap: None,
        child: verified.then_some(Pending { seed: child_seed, run: child_run }),
    }
}

#[cfg(test)]
mod tests {
    use super::*;

    /// A toy frontend: one symbolic byte `x`. The program branches on `x < 0x10`
    /// at site 0x100, then on `x == 0x42` at site 0x200. It exists to prove the
    /// loop and the verification predicate are independent of any real ISA.
    struct Toy {
        claim: Claim,
    }

    /// How the toy's property surface behaves.
    #[derive(Clone, Copy)]
    enum Claim {
        /// No property surface at all.
        None,
        /// The property `x != 3`, confirmed only by a re-run reading back 3.
        Witnessed,
        /// The property `x != 3`, but the frontend's readback always reports
        /// it as satisfied - the walker's term and the run disagree.
        Denied,
        /// Two queries on every completed path, so the second one meets the
        /// run budget edge if the first spends the last run.
        Pair,
    }

    #[derive(Clone)]
    struct Seed {
        x: u8,
    }

    struct Walk {
        solver: smtlite::Solver,
        x: smtlite::Bv,
        conds: Vec<smtlite::Bv>,
        taken: Vec<bool>,
        sites: Vec<u64>,
        path: Vec<smtlite::Bv>,
    }

    impl Frontend for Toy {
        type Seed = Seed;
        type Walk = Walk;

        fn run(&self, seed: &Self::Seed) -> Result<RunResult, String> {
            let mut log = Vec::new();
            let x = seed.x;
            log.push(BranchRec { site: 0x100, taken: x < 0x10 });
            if x < 0x10 {
                log.push(BranchRec { site: 0x200, taken: x == 0x42 });
            }
            Ok(RunResult { result: Some(i64::from(x)), trapped: None, log, sinks: Vec::new() })
        }

        fn walk(&self, _seed: &Self::Seed, log: &[BranchRec]) -> Option<Self::Walk> {
            let mut solver = smtlite::Solver::new();
            let x = solver.var("x", 8);
            let mut conds = Vec::new();
            let mut taken = Vec::new();
            let mut sites = Vec::new();
            let mut path = Vec::new();
            for b in log {
                let cond = match b.site {
                    0x100 => x.ult(&smtlite::Bv::val(0x10, 8)),
                    0x200 => x.eq(&smtlite::Bv::val(0x42, 8)),
                    _ => return None,
                };
                path.push(if b.taken { cond.clone() } else { cond.not() });
                conds.push(cond);
                taken.push(b.taken);
                sites.push(b.site);
            }
            Some(Walk { solver, x, conds, taken, sites, path })
        }

        fn flip(&self, walk: &mut Self::Walk, i: usize) -> Solution {
            // Q_i = Phi_i AND NOT g_i: the prefix held, the branch forced the
            // other way. `g_i` is the direction the concrete run took.
            let g_i = if walk.taken[i] {
                walk.conds[i].not()
            } else {
                walk.conds[i].clone()
            };
            let mut assumptions = walk.path[..i].to_vec();
            assumptions.push(g_i);
            walk.solver.check_all(&assumptions)
        }

        fn site(&self, walk: &Self::Walk, i: usize) -> u64 {
            walk.sites[i]
        }

        fn model_inputs(&self, model: &Model, _walk: &Self::Walk) -> Vec<(String, u64)> {
            model.get("x").map(|v| vec![("x".to_string(), v)]).unwrap_or_default()
        }

        fn apply_inputs(&self, _seed: &Self::Seed, inputs: &[(String, u64)]) -> Self::Seed {
            Seed { x: inputs.first().map_or(0, |(_, v)| *v as u8) }
        }

        fn properties(&self, _walk: &Self::Walk) -> Vec<String> {
            match self.claim {
                Claim::None => Vec::new(),
                Claim::Witnessed | Claim::Denied => vec!["x != 3".to_string()],
                Claim::Pair => {
                    vec!["x != 3".to_string(), "x != 3 (second)".to_string()]
                }
            }
        }

        fn check_property(&self, walk: &mut Self::Walk, _label: &str) -> Solution {
            // `path AND NOT (x != 3)` - the end-state question.
            let mut assumptions = walk.path.clone();
            assumptions.push(walk.x.eq(&smtlite::Bv::val(3, 8)));
            walk.solver.check_all(&assumptions)
        }

        fn property_violated(&self, run: &RunResult, _label: &str) -> Option<(u64, u64)> {
            match self.claim {
                Claim::None | Claim::Denied => None,
                Claim::Witnessed | Claim::Pair => (run.result == Some(3)).then_some((3, 3)),
            }
        }
    }

    #[test]
    fn the_loop_verifies_a_real_flip_and_proves_the_unreachable_one() {
        let r = explore(
            &Toy { claim: Claim::None },
            &Seed { x: 0 },
            &Opts { max_runs: 64, max_flips: 32 },
        );
        // Base path: 0x100 taken, 0x200 not taken. The attempt at 0x200 asks
        // whether x < 0x10 AND x == 0x42 - UNSAT, a local negative. The
        // attempt at 0x100 is satisfiable, applied and re-run, and the
        // reference engine takes the other side: Verified. The child path's
        // own flip lands back on the base path: AlreadyExplored.
        assert_eq!(r.runs, 3, "flips={:?}", r.flips);
        assert_eq!(r.flips_verified, 1, "flips={:?}", r.flips);
        assert_eq!(
            r.flips.iter().map(|f| (f.at, f.outcome)).collect::<Vec<_>>(),
            vec![
                (0x200, FlipOutcome::ProvenUnflippable),
                (0x100, FlipOutcome::Verified),
                (0x100, FlipOutcome::AlreadyExplored),
            ]
        );
        assert!(r.exhausted);
    }

    /// Three independent decisions, one per symbolic byte: sites 0x100, 0x200
    /// and 0x300 each ask whether a distinct byte is below 0x10.
    ///
    /// A flip query constrains only the prefix and the flipped decision, so
    /// every later decision is free. A real model answers those with whatever
    /// bit pattern satisfies the solver first; this frontend pins them to
    /// 0x10 (`false`) so the regression is about the loop's bookkeeping, not
    /// about which completion a solver happens to choose.
    #[derive(Clone, Copy, Default)]
    struct Siblings {
        /// Every flip query hits a solver bound.
        stuck: bool,
        /// A run with `x >= 0x10` fails at the engine level.
        fail_high_x: bool,
        /// A run with `z >= 0x10` fails at the engine level. Because `z` is
        /// the last decision's byte, a failed deep flip leaves no child.
        fail_high_z: bool,
        /// The symbolic walk cannot replay any concrete path.
        walk_fails: bool,
    }

    #[derive(Clone)]
    struct SSeed {
        x: u8,
        y: u8,
        z: u8,
    }

    struct SWalk {
        solver: smtlite::Solver,
        conds: Vec<smtlite::Bv>,
        taken: Vec<bool>,
        sites: Vec<u64>,
        path: Vec<smtlite::Bv>,
        /// The index `flip` was last asked about, so `model_inputs` knows
        /// which decisions the query did not constrain.
        last_flip: usize,
    }

    const SITE_VAR: [(u64, usize); 3] = [(0x100, 0), (0x200, 1), (0x300, 2)];

    impl Frontend for Siblings {
        type Seed = SSeed;
        type Walk = SWalk;

        fn run(&self, seed: &Self::Seed) -> Result<RunResult, String> {
            if (self.fail_high_x && seed.x >= 0x10)
                || (self.fail_high_z && seed.z >= 0x10)
            {
                return Err("the frontend refused this seed".to_string());
            }
            let log = vec![
                BranchRec { site: 0x100, taken: seed.x < 0x10 },
                BranchRec { site: 0x200, taken: seed.y < 0x10 },
                BranchRec { site: 0x300, taken: seed.z < 0x10 },
            ];
            Ok(RunResult { result: Some(0), trapped: None, log, sinks: Vec::new() })
        }

        fn walk(&self, _seed: &Self::Seed, log: &[BranchRec]) -> Option<Self::Walk> {
            if self.walk_fails {
                return None;
            }
            let mut solver = smtlite::Solver::new();
            let vars = [
                solver.var("x", 8),
                solver.var("y", 8),
                solver.var("z", 8),
            ];
            let mut conds = Vec::new();
            let mut taken = Vec::new();
            let mut sites = Vec::new();
            let mut path = Vec::new();
            for b in log {
                let k = SITE_VAR.iter().find(|(site, _)| *site == b.site)?.1;
                let cond = vars[k].ult(&smtlite::Bv::val(0x10, 8));
                path.push(if b.taken { cond.clone() } else { cond.not() });
                conds.push(cond);
                taken.push(b.taken);
                sites.push(b.site);
            }
            Some(SWalk { solver, conds, taken, sites, path, last_flip: 0 })
        }

        fn flip(&self, walk: &mut Self::Walk, i: usize) -> Solution {
            walk.last_flip = i;
            if self.stuck {
                return Solution::Unknown;
            }
            let g_i = if walk.taken[i] {
                walk.conds[i].not()
            } else {
                walk.conds[i].clone()
            };
            let mut assumptions = walk.path[..i].to_vec();
            assumptions.push(g_i);
            walk.solver.check_all(&assumptions)
        }

        fn site(&self, walk: &Self::Walk, i: usize) -> u64 {
            walk.sites[i]
        }

        fn model_inputs(&self, model: &Model, walk: &Self::Walk) -> Vec<(String, u64)> {
            // Decisions after the flipped one were not in the query. Fix them
            // to a legal completion (0x10) so the child's path is a pure
            // function of the query, not of the solver's assignment order.
            ["x", "y", "z"]
                .iter()
                .enumerate()
                .map(|(k, name)| {
                    let v = if k > walk.last_flip {
                        0x10
                    } else {
                        model.get(name).unwrap_or(0x10)
                    };
                    ((*name).to_string(), v)
                })
                .collect()
        }

        fn apply_inputs(&self, _seed: &Self::Seed, inputs: &[(String, u64)]) -> Self::Seed {
            let v = |name: &str| {
                inputs
                    .iter()
                    .find(|(n, _)| n == name)
                    .map_or(0, |(_, v)| *v as u8)
            };
            SSeed { x: v("x"), y: v("y"), z: v("z") }
        }
    }

    #[test]
    fn a_flip_onto_a_path_still_on_the_frontier_is_not_a_new_flip() {
        // The search discovers exactly eight paths: the base and seven
        // children. Some flips land on a path that is already discovered but
        // has not been popped yet; `verified` must mean "new path", so those
        // attempts are `AlreadyExplored`, not extra verifications. Tracking
        // only popped paths lets a later round verify the same child again
        // and inflate `flips_verified`.
        let r = explore(&Siblings::default(), &SSeed { x: 0, y: 0, z: 0 }, &Opts::default());
        assert!(r.exhausted);
        assert_eq!(7, r.flips_verified, "flips={:?}", r.flips);
        assert_eq!(
            7,
            r.flips.iter().filter(|f| f.verified).count(),
            "every counted verification must also be a verified record"
        );
    }

    #[test]
    fn a_budget_that_cuts_the_decision_loop_is_not_exhaustion() {
        // The base run and one verification exhaust `max_runs`; the shallower
        // decisions are never posed. The frontier will empty, but the search
        // was cut short, so `exhausted` must be false. A consumer that reads
        // `exhausted` alone must never see coverage that the budget refused.
        let r = explore(
            &Siblings::default(),
            &SSeed { x: 0, y: 0, z: 0 },
            &Opts { max_runs: 2, max_flips: 32 },
        );
        assert_eq!(r.runs, 2);
        assert_eq!(1, r.flips.len(), "flips={:?}", r.flips);
        assert!(!r.exhausted);
    }

    #[test]
    fn a_solver_bound_is_a_gap_and_an_unresolved_outcome() {
        // No verdict is not silence: every decision is recorded as
        // `SolverUnknown`, and the loop's own note is a gap. The frontier did
        // empty inside the budgets - the ledger, not the stop, carries the
        // unresolved fact.
        let r = explore(
            &Siblings { stuck: true, ..Siblings::default() },
            &SSeed { x: 0, y: 0, z: 0 },
            &Opts::default(),
        );
        assert_eq!(3, r.flips.len());
        assert!(r.flips.iter().all(|f| f.outcome == FlipOutcome::SolverUnknown));
        assert_eq!(3, r.gaps.iter().filter(|g| g.starts_with("solver Unknown at")).count());
        assert!(r.exhausted);
    }

    #[test]
    fn a_failed_verification_run_is_recorded_and_counted() {
        // The model is applied and the reference engine fails. That spends a
        // run and is `RunFailed`; it is never folded into a flip.
        let r = explore(
            &Siblings { fail_high_x: true, ..Siblings::default() },
            &SSeed { x: 0, y: 0, z: 0 },
            &Opts::default(),
        );
        assert!(
            r.flips
                .iter()
                .any(|f| f.at == 0x100 && f.outcome == FlipOutcome::RunFailed && !f.verified),
            "flips={:?}",
            r.flips
        );
        assert_eq!(
            0,
            r.flips.iter().filter(|f| f.verified && f.at == 0x100).count(),
            "a run that failed at the engine level is not a verified flip"
        );
        assert!(r.exhausted);
    }

    #[test]
    fn a_budget_break_that_leaves_the_frontier_empty_is_not_exhaustion() {
        // The deepest flip spends the last run and FAILS, so it creates no
        // child. The shallower decision is never posed, the frontier is empty,
        // and only the inner-loop flag can record that the search was cut
        // short. Without it this report would claim exhaustion.
        let r = explore(
            &Siblings { fail_high_z: true, ..Siblings::default() },
            &SSeed { x: 0, y: 0, z: 0 },
            &Opts { max_runs: 2, max_flips: 32 },
        );
        assert_eq!(r.runs, 2);
        assert_eq!(1, r.flips.len(), "flips={:?}", r.flips);
        assert_eq!(FlipOutcome::RunFailed, r.flips[0].outcome);
        assert!(!r.exhausted);
    }

    /// A frontend with no decisions at all, but a property surface. It exists
    /// to isolate the property-budget precondition: with no decisions there is
    /// no attempt loop that could set the incomplete flag.
    struct NoDecisions;

    struct NWalk {
        solver: smtlite::Solver,
        x: smtlite::Bv,
    }

    impl Frontend for NoDecisions {
        type Seed = u8;
        type Walk = NWalk;

        fn run(&self, seed: &Self::Seed) -> Result<RunResult, String> {
            Ok(RunResult {
                result: Some(i64::from(*seed)),
                trapped: None,
                log: Vec::new(),
                sinks: Vec::new(),
            })
        }

        fn walk(&self, _seed: &Self::Seed, _log: &[BranchRec]) -> Option<Self::Walk> {
            let mut solver = smtlite::Solver::new();
            let x = solver.var("value", 8);
            Some(NWalk { solver, x })
        }

        fn flip(&self, _walk: &mut Self::Walk, _i: usize) -> Solution {
            Solution::Unknown
        }

        fn site(&self, _walk: &Self::Walk, _i: usize) -> u64 {
            0
        }

        fn model_inputs(&self, model: &Model, _walk: &Self::Walk) -> Vec<(String, u64)> {
            model
                .get("value")
                .map(|v| vec![("value".to_string(), v)])
                .unwrap_or_default()
        }

        fn apply_inputs(&self, _seed: &Self::Seed, inputs: &[(String, u64)]) -> Self::Seed {
            inputs.first().map_or(0, |(_, v)| *v as u8)
        }

        fn properties(&self, _walk: &Self::Walk) -> Vec<String> {
            vec!["p1".to_string(), "p2".to_string()]
        }

        fn check_property(&self, walk: &mut Self::Walk, _label: &str) -> Solution {
            let q = walk.x.eq(&smtlite::Bv::val(0, 8));
            walk.solver.check_all(&[q])
        }

        fn property_violated(&self, _run: &RunResult, _label: &str) -> Option<(u64, u64)> {
            None
        }
    }

    #[test]
    fn a_property_refused_its_verification_run_is_not_exhaustion() {
        // Two satisfiable queries, one run left after the base run. The first
        // query spends it; the second is recorded `NotPosed`. No decision was
        // even posed, so the frontier is empty - but a query went unanswered
        // for want of budget, and the report must not call that exhausted.
        let r = explore(&NoDecisions, &0, &Opts { max_runs: 2, max_flips: 32 });
        assert_eq!(r.runs, 2);
        assert_eq!(2, r.properties.len());
        assert_eq!(PropertyOutcome::Unreproduced, r.properties[0].outcome);
        assert_eq!(PropertyOutcome::NotPosed, r.properties[1].outcome);
        assert!(!r.exhausted);
    }

    #[test]
    fn a_path_whose_walk_fails_is_not_exhaustion() {
        // The path was discovered and its run completed, but it was dropped
        // unanalysed. The gap records the limitation; the stop must not claim
        // the search completed.
        let r = explore(
            &Siblings { walk_fails: true, ..Siblings::default() },
            &SSeed { x: 0, y: 0, z: 0 },
            &Opts::default(),
        );
        assert_eq!(r.runs, 1);
        assert!(r.flips.is_empty());
        assert_eq!(
            vec!["walk could not replay the concrete path".to_string()],
            r.gaps
        );
        assert!(!r.exhausted);
    }

    /// A frontend that traps on every run and declares one property label.
    struct Trapped;

    impl Frontend for Trapped {
        type Seed = u8;
        type Walk = smtlite::Solver;

        fn run(&self, _seed: &Self::Seed) -> Result<RunResult, String> {
            Ok(RunResult {
                result: None,
                trapped: Some("out of bounds memory access".to_string()),
                log: Vec::new(),
                sinks: Vec::new(),
            })
        }

        fn walk(&self, _seed: &Self::Seed, _log: &[BranchRec]) -> Option<Self::Walk> {
            Some(smtlite::Solver::new())
        }

        fn flip(&self, _walk: &mut Self::Walk, _i: usize) -> Solution {
            Solution::Unknown
        }

        fn site(&self, _walk: &Self::Walk, _i: usize) -> u64 {
            0
        }

        fn model_inputs(&self, _model: &Model, _walk: &Self::Walk) -> Vec<(String, u64)> {
            Vec::new()
        }

        fn apply_inputs(&self, _seed: &Self::Seed, _inputs: &[(String, u64)]) -> Self::Seed {
            0
        }

        fn properties(&self, _walk: &Self::Walk) -> Vec<String> {
            vec!["out <= 0x10".to_string()]
        }

        fn check_property(&self, _walk: &mut Self::Walk, _label: &str) -> Solution {
            Solution::Unknown
        }
    }

    #[test]
    fn a_trapped_path_declares_its_properties_as_not_posed() {
        // There is no post-state to ask an end-state question about, so the
        // query is vacuous. It must still appear in the ledger: dropping it
        // would make "declared but unaskable" indistinguishable from "the
        // frontend has no property surface".
        let r = explore(&Trapped, &0, &Opts::default());
        assert_eq!(1, r.properties.len());
        assert_eq!("out <= 0x10", r.properties[0].label);
        assert_eq!(PropertyOutcome::NotPosed, r.properties[0].outcome);
        assert_eq!(vec!["run trapped: out of bounds memory access".to_string()], r.gaps);
        // The trap is the program's observed behavior and every discovered
        // path was walked; refusing to ask a vacuous question is not skipped
        // work.
        assert!(r.exhausted);
    }

    #[test]
    fn path_identity_counts_sites_not_only_directions() {
        // An indirect branch: the same two directions, two different targets.
        let direct = [
            BranchRec { site: 0x100, taken: true },
            BranchRec { site: 0x200, taken: false },
        ];
        let indirect = [
            BranchRec { site: 0x100, taken: true },
            BranchRec { site: 0x300, taken: false },
        ];
        assert_eq!(
            direct.iter().map(|b| b.taken).collect::<Vec<_>>(),
            indirect.iter().map(|b| b.taken).collect::<Vec<_>>(),
            "the two runs take the same directions"
        );
        assert_ne!(
            path_key(&direct),
            path_key(&indirect),
            "but they are not the same path"
        );
    }

    #[test]
    fn a_property_is_confirmed_only_by_the_re_run() {
        let r = explore(
            &Toy { claim: Claim::Witnessed },
            &Seed { x: 0 },
            &Opts { max_runs: 64, max_flips: 32 },
        );
        // On the base path the solver finds x = 3 and the reference engine
        // re-runs that model; the readback is the witness, not the Sat answer.
        let confirmed = &r.properties[0];
        assert_eq!(confirmed.label, "x != 3");
        assert_eq!(confirmed.outcome, PropertyOutcome::Confirmed);
        assert_eq!(confirmed.violation, Some((3, 3)));
        assert_eq!(confirmed.input, vec![("x".to_string(), 3)]);
        // The flipped child path (x >= 0x10) is UNSAT for x == 3: a local
        // negative under its own assumptions, and no run is spent on it.
        assert_eq!(r.properties.len(), 2);
        assert_eq!(r.properties[1].outcome, PropertyOutcome::Proven);
        // base + property witness + verified flip + the child's own flip.
        assert_eq!(r.runs, 4, "flips={:?}", r.flips);
        assert_eq!(r.flips_verified, 1, "flips={:?}", r.flips);
        assert!(r.exhausted);
    }

    #[test]
    fn a_sat_model_without_a_violating_readback_is_unreproduced() {
        // The solver satisfies `x == 3`, the model is applied and re-run, but
        // this frontend's readback never reports the violation. The Sat answer
        // alone is not a finding: the ledger records the disagreement.
        let r = explore(
            &Toy { claim: Claim::Denied },
            &Seed { x: 0 },
            &Opts { max_runs: 64, max_flips: 32 },
        );
        assert_eq!(r.properties[0].outcome, PropertyOutcome::Unreproduced);
        assert_eq!(r.properties[0].violation, None);
        assert_eq!(r.properties[0].input, vec![("x".to_string(), 3)]);
    }

    #[test]
    fn a_sat_property_with_no_run_budget_is_not_posed() {
        // The first query spends the last remaining run; the second is
        // satisfiable but has no verification run behind it, so the witness
        // law records `NotPosed`, not a finding.
        let r = explore(
            &Toy { claim: Claim::Pair },
            &Seed { x: 0 },
            &Opts { max_runs: 2, max_flips: 32 },
        );
        assert_eq!(r.properties.len(), 2);
        assert_eq!(r.properties[0].outcome, PropertyOutcome::Confirmed);
        assert_eq!(r.properties[1].outcome, PropertyOutcome::NotPosed);
        assert_eq!(r.runs, 2, "the budget is a hard cap, not a target");
        // The frontier may be empty, but a satisfiable query was refused its
        // verification run. The search was cut short, so it is NOT exhausted.
        assert!(!r.exhausted);
    }
}