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> { ... }
}

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.

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 lift 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 opcode, replay drift, …).

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

Sinks reached on the walked path.

Dyn Compatibility

This trait is dyn compatible.

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

Implementors