Trait Frontend 

pub trait Frontend {
    type Seed: Clone;
    type Walk;

    // Required methods
    fn run(&self, seed: &Self::Seed) -> Result<RunResult, String>;
    fn walk(&self, seed: &Self::Seed, log: &[BranchRec]) -> Option<Self::Walk>;
    fn flip(&self, walk: &mut Self::Walk, i: usize) -> Solution;
    fn site(&self, walk: &Self::Walk, i: usize) -> u64;
    fn model_inputs(
        &self,
        model: &Model,
        walk: &Self::Walk,
    ) -> Vec<(String, u64)>;
    fn apply_inputs(
        &self,
        seed: &Self::Seed,
        inputs: &[(String, u64)],
    ) -> Self::Seed;

    // Provided methods
    fn walk_gaps(&self, _walk: &Self::Walk) -> Vec<String> { ... }
    fn walk_sinks(&self, _walk: &Self::Walk) -> Vec<SinkRec> { ... }
    fn properties(&self, _walk: &Self::Walk) -> Vec<String> { ... }
    fn check_property(&self, _walk: &mut Self::Walk, _label: &str) -> Solution { ... }
    fn property_violated(
        &self,
        _run: &RunResult,
        _label: &str,
    ) -> Option<(u64, u64)> { ... }
}

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.

Required Associated Types

type Seed: Clone

The seed: the initial state, with its base concrete assignment.

type Walk

The symbolic walk, owning whatever solver state the frontend keeps.

Required Methods

fn run(&self, seed: &Self::Seed) -> Result<RunResult, String>

Run the reference engine concretely. Determinism is the frontend’s obligation; an engine-level failure is Err, not a trap.

fn walk(&self, seed: &Self::Seed, log: &[BranchRec]) -> Option<Self::Walk>

Replay the concrete log symbolically. None when the walk cannot force the path (a replay or frontend limitation); the caller records that fact.

fn flip(&self, walk: &mut Self::Walk, i: usize) -> Solution

Pose the flip query at decision i of the forced walk.

fn site(&self, walk: &Self::Walk, i: usize) -> u64

The decision site at index i of the walk.

fn model_inputs(&self, model: &Model, walk: &Self::Walk) -> Vec<(String, u64)>

The model’s bindings over the symbolic surface.

fn apply_inputs( &self, seed: &Self::Seed, inputs: &[(String, u64)], ) -> Self::Seed

Apply those bindings to a child seed.

Provided Methods

fn walk_gaps(&self, _walk: &Self::Walk) -> Vec<String>

Gap notes the walk itself recorded (unsupported instruction, replay drift, …).

fn walk_sinks(&self, _walk: &Self::Walk) -> Vec<SinkRec>

Sinks reached on the walked path.

fn properties(&self, _walk: &Self::Walk) -> Vec<String>

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 check_property(&self, _walk: &mut Self::Walk, _label: &str) -> Solution

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 property_violated( &self, _run: &RunResult, _label: &str, ) -> Option<(u64, u64)>

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.

Dyn Compatibility

This trait is dyn compatible.

In older versions of Rust, dyn compatibility was called "object safety".

Implementors