Prove the ~30 external_body codec/CRC bodies with ordeal (upgrade proptest → certificate)

[avrabe]

relay's source literally documents where Verus/Z3 can't do bit-level proofs — ~30 #[verifier::external_body] hatches with comments like "would require bit-vector lemmas Verus' default integer theory cannot discharge" / "pinned by proptest" (relay-ccsds/src/sensor_wire.rs:239, relay-nid/src/bitpack.rs, relay-mavlink/src/frame.rs, CRCs in relay-mavlink/src/crc.rs, relay-cs/src/engine.rs). Relates to #4, #253.

Proposal: use ordeal prove_equiv for encode/decode round-trip and CRC-16/32 per-step equivalence — an unbounded, certificate-checked upgrade from "trust the unit test" on safety-critical flight wire codecs.

Enablers: byte-layout to/from_le_bytes + native 16-bit width — ordeal roadmap pulseengine/ordeal#64 (v0.10.0) — and the equivalence toolkit pulseengine/ordeal#66 (v0.12.0). Boundary: codec/CRC per-step is QF_BV; falcon EKF/mixer (f32/f64) is FP theory and scheduling/liveness is temporal — both OUT of ordeal, stay on FP/Gale/loom.

[avrabe]

+1 with fresh motivating data from v1.117 (today): the PARAM-P03 parameter-persistence layer (relay-param persist.rs, lands in PR shortly) hit exactly this wall. The record codec is CRC-32-guarded, and Kani/CBMC could not carry ANY nondet through the CRC: a fully-nondet 96-byte image ran >28 CPU-min without terminating, and even a single nondet byte at a nondet position ran >20 CPU-min (killed both). Same class as relay-traj (#260).

Current assurance (documented in relay-param/plain/src/kani_proofs.rs): compositional (the loader's only store mutation is the K01-proven bounded set) + an exhaustive concrete all-positions corruption sweep + proptests. Honest, but the CRC step-equivalence itself is test-pinned — exactly the "trust the unit test" gap this issue names.

Please add to the scope list: relay-param/plain/src/persist.rs — crc32 per-step equivalence + record encode/decode round-trip (pure byte-layout QF_BV, no FP — squarely inside ordeal's boundary). It would let us re-state the PARAM-K03/K04 properties we had to remove as unbounded certificates.

Rivet artifact for this lands when the enablers ship (ordeal#64 v0.10 byte-layout + #66 v0.12 equivalence toolkit) — until then the kani_proofs.rs rationale block is the traceable pointer.

🤖 Generated with Claude Code

[avrabe]

Accepted into scope — relay-param/plain/src/persist.rs (CRC-32 per-step equivalence + record encode/decode round-trip) is added to the FEAT-010 target list, and the PARAM-P03 data is a perfect motivator: Kani/CBMC can't carry nondet through a CRC (your >28 CPU-min / >20 CPU-min kills) is precisely the wall a certificate-checked QF_BV prove_equiv walks around, because it proves the algebraic step-equivalence rather than enumerating.

Covered by the enablers you named: ordeal#64 (v0.10.0 — byte-layout to/from_le_bytes + 16-bit) then ordeal#66 (v0.12.0 — the equivalence toolkit / prove_valid). That lets you re-state the removed PARAM-K03/K04 properties as unbounded certificates. The kani_proofs.rs rationale block is the right traceable pointer until the rivet artifact lands. Boundary stays clean: CRC/codec byte-layout is QF_BV; nothing FP here.