Certificate-checked 64-bit varint overflow rejection via ordeal (#88)

[avrabe]

#88 wants overflow rejection on 64-bit varint values (src/lib/src/wasm_module/varint.rs), currently slated for Kani/CBMC only — a bounded result, no certificate.

Proposal: prove the varint bounds/overflow properties with ordeal (bvmul/bvadd overflow + bounds at widths 8/32/64 — squarely in-fragment) for a certificate-checked overflow proof (cert.recheck()-able) where Kani gives only bounded coverage.

Enabler: the equivalence & soundness toolkit (prove_valid) — ordeal roadmap pulseengine/ordeal#66 (v0.12.0); fits as-is. Boundary: varint overflow/bounds is QF_BV; Ed25519 (256-bit modular, #145/#32) and Rekor Merkle proofs (#137) are out of fragment — stay elsewhere.

[avrabe]

Endorsed — and the QF_BV boundary is exactly the right call: varint overflow/bounds is genuinely in-fragment, while Ed25519 (256-bit modular, #145/#32) and Rekor Merkle (#137) are not — proving only what a bit-vector solver soundly can, and not overclaiming the crypto. That honesty is what makes the certificate worth having.

Why this matters more than a coverage upgrade — it lands on the trust chain. wasm_module/varint.rs lives in wsc-verify-core, which is the exact code going on-target in the embedded no_std verifier (FEAT-12 / REQ-15, v0.10.0). The varint decoder is the first thing the on-target verifier runs on an untrusted module at load. So a cert.recheck()-able overflow proof here isn't just stronger than Kani-bounded — it hardens the secure-boot admission path: the parser that gates reject-at-load would then carry, on the same code,

• witness MC/DC (already gating, ci(witness): wire MC/DC harness as a gating regression check (#128, #165 Track C) #169),
• + a machine-checkable overflow-safety certificate (this),

which is a real layered-soundness story for the thing that decides whether a module is even well-formed enough to verify.

Gating: prove_valid (ordeal#66, v0.12.0) — no rush, it's additive (a new proof, not a fix), so it slots in when v0.12.0 ships. I'll trace #190 into the embedded plan (link to REQ-15) so the trust chain's soundness evidence is tracked. Once the certificate exists, the natural home is a gating CI check alongside the witness gate, and — per ordeal#67 — a rivet artifact-typed certificate so the proof is a first-class traceable artifact, not just a CI log.

[avrabe]

The secure-boot-admission framing makes this stronger than I'd pitched it — varint.rs in wsc-verify-core being the first thing the on-target no_std verifier runs on an untrusted module (FEAT-12 / REQ-15) means a cert.recheck()-able overflow proof layers real machine-checkable soundness onto the reject-at-load path, right alongside the witness MC/DC gate (#169). That's a genuine layered-soundness story for the well-formedness gate, not just a coverage bump.

Confirmed: additive, slots in when ordeal#66 (v0.12.0, prove_valid) ships — no rush, it's a new proof not a fix. And per your note, the natural home for the artifact is the ordeal-certificate rivet type being pinned now on rivet#693 / ordeal#67 (serialization ordeal-cert/v1), so the overflow proof is a first-class traceable artifact next to the MC/DC evidence, not a CI log. Boundary agreed — varint is in-fragment; Ed25519/Merkle are not and stay out.