kiln's math/runtime core has concrete QF_BV obligations: integer op semantics (kiln-math/src/ops.rs — i32_div_s MIN/-1 trap, i32_shl shift-mask, wrap/extend), duplicated ASIL logic (kiln-math/src/safety.rs), and effective-address overflow/bounds trap logic (kiln-runtime/src/stackless/engine.rs, kiln-foundation/src/linear_memory.rs — note pop_atomic_address uses wrapping_add+guard). Relates to the certified-oracle thesis #401/#413.
Proposal: use ordeal prove_equiv to prove the wrapping/masking bodies and trap predicates bit-exact, and checked_add().is_none() ⟺ sum ≥ 2^64 on the hot memory path — a certificate-checked oracle complementing external-interpreter differential testing, Z3-free.
Enablers: signed bvsdiv/bvsrem/bvurem + 16-bit width — ordeal roadmap pulseengine/ordeal#64 (v0.10.0) — + toolkit pulseengine/ordeal#66 (v0.12.0). Boundary: integer/trap logic is QF_BV; trunc_f* is FP (OUT); SafeMemoryHandler checksum/Seq<u8> integrity uses UF+quantifiers (OUT, stays in Verus).
kiln's math/runtime core has concrete QF_BV obligations: integer op semantics (
kiln-math/src/ops.rs—i32_div_sMIN/-1 trap,i32_shlshift-mask, wrap/extend), duplicated ASIL logic (kiln-math/src/safety.rs), and effective-address overflow/bounds trap logic (kiln-runtime/src/stackless/engine.rs,kiln-foundation/src/linear_memory.rs— notepop_atomic_addressuseswrapping_add+guard). Relates to the certified-oracle thesis #401/#413.Proposal: use ordeal
prove_equivto prove the wrapping/masking bodies and trap predicates bit-exact, andchecked_add().is_none() ⟺ sum ≥ 2^64on the hot memory path — a certificate-checked oracle complementing external-interpreter differential testing, Z3-free.Enablers: signed
bvsdiv/bvsrem/bvurem+ 16-bit width — ordeal roadmap pulseengine/ordeal#64 (v0.10.0) — + toolkit pulseengine/ordeal#66 (v0.12.0). Boundary: integer/trap logic is QF_BV;trunc_f*is FP (OUT);SafeMemoryHandlerchecksum/Seq<u8>integrity uses UF+quantifiers (OUT, stays in Verus).