Track C: wohl-ota — verified dual-bank OTA state machine

[avrabe]

Summary

Phase 2 Track C. New crates/wohl-ota — the no_std core for over-the-air firmware update. Design-before-hardware: the state machine is proven correct in software first, then bolted onto a board later.

What's in it

Dual-bank update state machine over two slots (A/B), one Active, one Standby:

OtaState ::= Idle
           | Downloading { slot, bytes_received, total_bytes }
           | Verifying  { slot }
           | Ready      { slot }
           | Swapping

• OtaManifest (version, size, sha256, Ed25519 signature)
• Signature verification via a SignatureVerifier trait — no concrete crypto dependency; AlwaysAccept/AlwaysReject stubs for tests + Kani. Real Ed25519 is a later, isolated change.
• no_std, no_alloc — fixed arrays, no Vec.

Verification

• 4 Kani harnesses, all PASS (112 internal checks):
  • OTA-P01: Active slot is never a download destination
  • OTA-P02: swap only succeeds from Ready
  • OTA-P03: bytes_received never exceeds total_bytes
  • OTA-P04: no panic for any call sequence
• 11 unit tests + 4 proptests pass
• cargo +1.85.0 clippy --all-targets -- -D warnings + fmt clean

Open design questions (for reviewers)

• SignatureVerifier::verify takes the parsed &OtaManifest — should it take canonical &[u8] instead, to decouple the trait from the struct?
• Rollback currently flips active from Idle with no post-swap watchdog window — add a rollback-budget state?
• Swapping is modelled as instantaneous; real hardware has a power-loss window — add begin_swap/commit_swap for durability proofs?

Radio-agnostic — independent of the transport decisions (see #10).

🤖 Generated with Claude Code