vcl-ut #25 P5b (step 1): C-ABI wire codec for Statement

[hyperpolymath]

P5b (step 1) — C-ABI wire codec for Statement

The marshalling seam between the trusted Rust parser (P5a, #26) and the
Idris2 certifier. Stacked on #26 (base = the P5a branch); review/merge
#26 first.

What this adds (in the standalone vcltotal-parse crate)

• WIRE-FORMAT.adoc — normative spec: a deterministic, versioned,
  length-prefixed binary TLV ("VCLW" + u16 ver). Discriminants
  reuse Grammar.idr's *ToInt maps where they exist and
  Types.idr safetyLevelToInt, so the P5b-step-2 Idris2 decoder is
  a direct match. Chosen over CBOR: zero dependency / no extra trust
  surface, fully auditable, byte-exact.
• src/wire.rs — to_wire / from_wire for the full Statement
  AST, same SPARK-grade posture as the parser (crate lint-set):
  • to_wire: total, deterministic, canonical (one byte string per
    value).
  • from_wire: total — bounds-checked cursor, no panic, no
    unbounded pre-allocation from untrusted counts (anti-OOM), every
    malformed input a typed WireError.

Machine witnesses (tests/wire.rs, proptest 2048 cases)

• roundtrip: from_wire(to_wire(s)) == s over arbitrary
  Statements — the codec is a bijection on the Rust AST mirror.
• decoder_total_on_garbage / _with_valid_header: arbitrary bytes
  never panic — Ok/Err only (trusted-boundary totality).
• encoder_deterministic; golden vectors incl. bit-exact
  non-finite float preservation (inf structural, NaN by bits).

Verified (standalone, CI-faithful: --manifest-path … --locked)

cargo clippy --all-targets -- -D warnings clean (SPARK lint set);
cargo test 17/17 (6 lib + 5 parse + 6 wire); cargo fmt --check
clean. parse-gate CI applies (the crate is its own workspace root,
decoupled from the pre-existing parent-workspace external-path-dep
breakage).

Next (P5b step 2, separate PR)

The total Idris2 decoder of this identical byte format into
Grammar.idr's certified Statement (%default total, zero
proof-escape), with the golden vectors shared as cross-language
conformance fixtures — gated by the proof-corpus CI (now healthy after
#24's pinned-source idris2 build).

Refs #25.

🤖 Generated with Claude Code