concolic-core

The architecture-neutral half of a concolic-execution 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 memory layout. A frontend supplies:

• a deterministic concrete reference run;
• a symbolic walk forced along a concrete branch log;
• the flip query at one decision;
• the symbolic surface's names in a model, and how to apply them.

Optionally it also supplies a property surface: the labels to pose as end-state queries, the query itself, and the readback that decides whether a re-run violated the property. Without one, the property ledger is simply empty.

Everything else is fixed here: the frontier, the budgets, the verification predicate, the flip and property outcome algebras, and the report contract.

The verification law

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.

The predicate is same decision sites, same directions as the walked prefix, opposite at exactly the flipped site. Operand values are deliberately excluded from the path: a changed input necessarily moves the operands of earlier comparisons that still go the same way, so a predicate comparing whole records rejects genuine flips.

The flip ledger

An attempted flip ends in one structured outcome - Verified, ProvenUnflippable, SolverUnknown, RunFailed, Unconfirmed, or AlreadyExplored - rather than a bare count. (NotPosed is the honest default for a consumer's own record of an attempt it could not pose; the loop spends no run and builds no query in that case, so its own records never carry it.) A count of failed attempts is not a diagnosis; the structured outcome is what separates "the solver proved this fixed" from "the walker and the run disagreed".

Report::exhausted means the frontier emptied with no work left undone. If a budget refused a decision or a property verification, or a discovered path could not be walked, the report says not exhausted even when the frontier happens to empty: the remaining work was skipped, not completed.

The property ledger

A property query asks path AND NOT invariant at the end of a walked path, so a straight-line violation with no decision to flip is still expressible. Queries are posed only on paths whose reference run completed; on a trapped path every declared label is recorded as NotPosed (there is no post-state to read), so the ledger stays total. The same witness law applies:

• Unsat is a local negative under the path's assumptions (Proven);
• a Sat model is a candidate, and only the reference engine's own re-run readback can confirm it (Confirmed), deny it (Unreproduced), or fail to return (RunFailed);
• a query with no run budget left for its verification run is NotPosed - nothing was observed, so nothing is claimed.

License

Apache-2.0.