Add Kani harnesses for crypto parsers (varint, DSSE envelope, signature verification)

[avrabe]

Part of the V&V coverage initiative.

Problem

sigil has a Lean proof of Ed25519 correctness (lean/Ed25519.lean, 203 lines) and Verus annotations on some crypto primitives. The parser surfaces — varint decoding in src/lib/src/wasm_module/varint.rs, DSSE envelope parsing, signature byte-layout validation — are where parser edge cases live, and these are not covered by the Lean theory (which operates on mathematical values, not byte slices).

Acceptance

• Kani harness for varint parser: round-trip encode/decode correctness + overflow rejection on 64-bit values
• Kani harness for DSSE envelope parser: malformed-envelope rejection, missing-field detection, untrusted-length bounds
• Kani harness for signature verification entry: length checks, format checks, error path closure
• Harnesses in src/lib/tests/kani_<parser>.rs or similar
• Traceability in rivet.yaml: link Kani harnesses to the Ed25519 Lean theorems (mathematical correctness) and DSSE spec requirements (parser correctness)
• CI gate via cargo kani

Notes

• varint is where 61 existing Kani uses already live — extend that pattern
• DSSE envelope format: treat untrusted input as kani::any_slice_of_array_that_is_nonempty()
• Matches the SymCrypt/Aeneas pattern: mathematical proof in Lean + parser proofs in Kani