concolic-core 0.1.0

//! 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 (SBF, x86-64, RV32IM, AArch64, ...) 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 in this workspace).
    pub site: u64,
    /// Whether the branch was taken.
    pub taken: bool,
}

/// What an attempted flip actually reached (§7.1 of the LACUNA account).
#[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 query was built (the walk could not replay the path or force the branch).
    /// The default is the honest one: nothing was posed.
    #[default]
    NotPosed,
    /// The flipped run failed at the engine level.
    RunFailed,
    /// The run completed but did not flip: 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 symbolic surface (`in!...` names).
    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 the SBF frontend 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 run failed at the engine level.
    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 (e.g. `cpi`, `transfer`, `ecall`, `syscall`).
    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.
    pub sinks: Vec<SinkRec>,
}

/// The session report - the architecture-neutral subset of the engine report
/// that the diagnosis layer reads.
#[derive(Clone, Debug, Default)]
pub struct Report {
    /// The base run's result, when it returned.
    pub result: Option<i64>,
    /// Concrete runs spent.
    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 from the frontend.
    pub gaps: Vec<String>,
    /// The frontier emptied inside the budgets.
    pub exhausted: bool,
}

/// The budgets a session ran under.
#[derive(Clone, Copy, Debug, PartialEq, Eq)]
pub struct Opts {
    /// Hard cap on concrete runs.
    pub max_runs: usize,
    /// Hard cap on verified flips.
    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 four obligations are exactly the soundness contract: `run` is
/// deterministic, `walk` is a sound over-approximation of `run`'s prefix, and
/// `model_inputs`/`apply_inputs` round-trip a model onto a runnable seed.
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 lift 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 opcode, 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()
    }
}

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<Vec<bool>> = BTreeSet::new();

    let first = match frontend.run(base) {
        Ok(r) => r,
        Err(e) => {
            report.gaps.push(format!("run failed: {e}"));
            return report;
        }
    };
    report.runs = 1;
    report.result = first.result;
    let mut frontier = vec![Pending { seed: base.clone(), run: first }];

    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 path: Vec<bool> = item.run.log.iter().map(|b| b.taken).collect();
        if !seen.insert(path) {
            continue;
        }
        let Some(mut walk) = frontend.walk(&item.seed, &item.run.log) else {
            report
                .gaps
                .push("walk could not replay the concrete path".to_string());
            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 SBF
        // engine records.
        let (mut spent, mut flipped) = (0usize, 0usize);
        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
            {
                break;
            }
            let a = attempt(frontend, &item.seed, &item.run.log, &mut walk, i, &seen);
            spent += usize::from(a.ran);
            flipped += usize::from(a.verified);
            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 = true;
    report
}

fn attempt<F: Frontend>(
    frontend: &F,
    seed: &F::Seed,
    log: &[BranchRec],
    walk: &mut F::Walk,
    i: usize,
    seen: &BTreeSet<Vec<bool>>,
) -> 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: Vec<bool> = child_run.log.iter().map(|b| b.taken).collect();
    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;

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

    struct Walk {
        solver: smtlite::Solver,
        x: smtlite::Bv,
        conds: Vec<smtlite::Bv>,
        taken: Vec<bool>,
        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("in!x", 8);
            let mut conds = Vec::new();
            let mut taken = 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);
            }
            Some(Walk { solver, x, conds, taken, 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 {
            let _ = walk;
            [0x100, 0x200][i]
        }

        fn model_inputs(&self, model: &Model, _walk: &Self::Walk) -> Vec<(String, u64)> {
            model.get("in!x").map(|v| vec![("in!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) }
        }
    }

    #[test]
    fn the_loop_verifies_a_real_flip_and_proves_the_unreachable_one() {
        let r = explore(&Toy, &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);
    }
}