F433 deep-review findings and dispositions (2026-08-18)

1. C++ exceptions could escape selected C ABI entry points.
   Fixed: add/assume/observe/val/failed/terminate now catch at the ABI boundary.
2. QueryStore accepted an empty incremental proof policy during normalization.
   Fixed: all policy and import identities require exact lowercase SHA-256 text.
3. Realtime and ordinary CaDiCaL identities were checked too loosely downstream.
   Fixed: exact wrapper/native identity relation; truncation is rejected.
4. Saturating counter subtraction could hide a native counter rollback.
   Fixed: any counter below its session baseline fails closed.
5. Learned-clause native export and Python drain counts were not required equal.
   Fixed: QueryStore rejects incomplete learned-clause accounting.
6. The fake ABI ignored max_learned=0.
   Fixed: capacity zero now disables learned export exactly as the real bridge does.
7. The active-solve test used a fixed sleep and flaked under full LLVM 18 load.
   Fixed: an atomic solve-start handshake makes publication order deterministic.

After these fixes: focused 49+38, full Python 1242+291, LLVM 17/18 each 323
discovered with zero failure/unresolved, two real 512-case oracles with zero
mismatch, and two 64-round mechanism benchmarks with 64/64 native ACKs.