# 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.