2 KiB
Bounded symbolic soundness contract
Model relation
Let C_k be the concrete executions within the configured loop/call bound and
let E_k be fold's encoded executions. For an over-approximated encoding, the
required relation is C_k ⊆ E_k: every bounded concrete execution has an
encoded counterpart, while the encoding may admit additional executions.
Typed bit-vector operations are exact where the source width and signedness are known. Unknown calls, unsupported nodes and types, loop havoc, and timeouts are not exact; they must be recorded in the encoding precision context.
UNSAT results
If E_k ∧ H is UNSAT, no execution in C_k can satisfy hazard H. This is the
safe direction of proof under over-approximation and is used for bounded
unreachability and invariant checks.
The conclusion remains bounded: it says nothing about executions beyond the configured loop/call bound or translation units and binaries outside the scan.
SAT results
If E_k ∧ H is SAT, the model is a candidate hazard witness. It corresponds to
a bounded concrete execution only when the encoding that supports the query is
exact. A SAT model from an over-approximated encoding may be spurious.
Accordingly, the confidence contract is:
proved: an exact bounded model established the property (SAT for a hazard witness, or UNSAT for a negated invariant);latent: the intra-procedural model is exact, but a caller/environment obligation remains undischarged;heuristic: an unsupported or over-approximated operation contributes to the result;concrete-witness: a sanitizer/runtime failure was strictly correlated with the predicted hazard.
Detectors must propagate the sink-time encoding precision into evidence and
must not label an over-approximated SAT result proved.
Exact fragment
For loop-free, call-free functions whose used operations and types are fully encoded, the bounded model can be exact. Exactness is a per-query property, not a blanket property of every integer-only function or every 64-bit encoding.