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