Crate concolic_core 

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.

Structs

BranchRec

One decision in a concrete trace: the site and the direction taken.

FlipRec

One flip attempt, in decision order.

Opts

The budgets a session ran under.

PropertyRec

One property-directed query on one walked path.

Report

The session report - the architecture-neutral subset of the engine report that the diagnosis layer reads.

RunResult

The outcome of one concrete reference run.

SinkRec

A sink reached on a walked path. The kind and argument names are the frontend’s vocabulary; the ledger treats them as opaque labels.

Enums

FlipOutcome

What an attempted flip actually reached (§7.1 of the LACUNA account).

PropertyOutcome

A property query’s outcome (the same algebra the SBF frontend uses).

Traits

Frontend

What a frontend must provide for the loop to run.

Functions

explore

Explore the frontend’s entry point from base inside the budgets.