# 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 four
things:
- 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.
Everything else is fixed here: the frontier, the budgets, the verification predicate, the
seven flip outcomes, 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`, `NotPosed`, `RunFailed`, `Unconfirmed`, or `AlreadyExplored` - rather than
a bare count. 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".
```rust
use concolic_core::{BranchRec, FlipOutcome};
// A frontend returns the new trace; the core classifies what the flip reached.
let prefix = [BranchRec { site: 0x9000, taken: true }];
assert_eq!(prefix[0].site, 0x9000);
```
## License
Apache-2.0.