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

The marshalling layer between the trusted Rust parser (P5a) and the
Idris2 certifier. Adds, in the standalone vcltotal-parse crate:

- WIRE-FORMAT.adoc: normative spec for a deterministic, versioned,
  length-prefixed binary TLV (magic "VCLW" + u16 ver). Discriminants
  reuse Grammar.idr's *ToInt maps where they exist (modality/agent/
  epReq/epistemicOp) and Types.idr safetyLevelToInt, so the P5b-step-2
  Idris2 decoder is a direct match. Chosen over CBOR: no 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
    (bijection on the Rust AST mirror).
  - decoder_total_on_garbage / _with_valid_header: arbitrary bytes
    never panic — Ok/Err only (trusted-boundary totality contract).
  - encoder_deterministic; golden vectors incl. bit-exact non-finite
    float preservation (inf structural, NaN by bits).

Verified standalone, CI-faithful (--manifest-path --locked):
clippy --all-targets -D warnings clean (SPARK lint set), 17/17 tests
(6 lib + 5 parse + 6 wire), fmt clean.

Step 2 (separate): the total Idris2 decoder of this identical format
into Grammar.idr's certified Statement, %default total, no proof
escape, with shared golden vectors for cross-language conformance —
gated by the proof-corpus CI (now healthy post-#24).

Stacked on the P5a branch. Refs #25.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

Author: hyperpolymath

src/interface/parse/WIRE-FORMAT.adoc

@@ -0,0 +1,98 @@
+= VCL-total Statement Wire Format v1 (P5b, vcl-ut#25)
+:toc:
+
+// SPDX-License-Identifier: PMPL-1.0-or-later
+// Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+
+The C-ABI marshalling format for a parsed `Statement`. The Rust
+encoder/decoder (`wire.rs`) is normative for v1; the P5b-step-2 Idris2
+decoder MUST decode this identical byte stream into `Grammar.idr`'s
+`Statement` (the certified type), proven total. Cross-language
+conformance is by shared golden vectors.
+
+Design: a deterministic, versioned, length-prefixed binary TLV.
+*Rationale:* no parser dependency / no extra trust surface (vs CBOR),
+fully auditable, byte-exact, total decode. This is the boundary the
+hypatia<->verisim seam crosses; it is specified, not improvised.
+
+== Conventions
+
+* All multi-byte integers are *little-endian, fixed width*.
+* `u8` = 1 byte; `u32` = 4 bytes; `u64`/`i64` = 8 bytes (`i64`
+  two's-complement); `f64` = 8 bytes IEEE-754 (`f64::to_bits`,
+  bit-exact — NaN/inf preserved).
+* `bool` = 1 byte, `0x00` false / `0x01` true (any other byte =>
+  `WireError::BadBool`).
+* `string` = `u32` byte length, then that many UTF-8 bytes.
+* `option<T>` = `0x00` (none) | `0x01` (some) then `T`.
+* `list<T>` = `u32` count, then that many `T`.
+* Every sum type = a `u8` *discriminant* then its payload in the field
+  order below. Unknown discriminant => `WireError::BadTag`.
+
+== Header
+
+`56 43 4C 57` ("VCLW") then `u16` version. v1 = `01 00`.
+Bad magic/version => `WireError::BadMagic` / `BadVersion`.
+
+== Discriminants (STABLE — never renumber; append only)
+
+Where `Grammar.idr` already defines an integer mapping it is reused so
+the Idris decoder is a direct match:
+
+* `Modality` — `modalityToInt`: Graph 0, Vector 1, Tensor 2,
+  Semantic 3, Document 4, Temporal 5, Provenance 6, Spatial 7.
+* `Agent` — `agentToInt` tag: Engine 0, Prover 1 `+string`,
+  Validator 2, User 3 `+string`, Federation 4.
+* `EpistemicOp` — `epistemicOpToInt`: Knows 0, Believes 1,
+  CommonKnowledge 2.
+* `EpistemicRequirement` — `epReqToInt`: Knows 0 `agent,expr`,
+  Believes 1 `agent,expr`, Common 2 `expr`, Entails 3
+  `agent,agent,expr`.
+* `SafetyLevel` — `safetyLevelToInt` (Types.idr): ParseSafe 0 …
+  EpistemicSafe 10.
+
+Defined here for v1 (no Idris int map existed; now normative):
+
+* `Literal`: Str 0 `string`, Int 1 `i64`, Float 2 `f64`, Bool 3
+  `bool`, Null 4, Vector 5 `list<f64>`.
+* `CompOp`: Eq 0, NotEq 1, Lt 2, Gt 3, LtEq 4, GtEq 5, Like 6, In 7.
+* `LogicOp`: And 0, Or 1, Not 2.
+* `AggFunc`: Count 0, Sum 1, Avg 2, Min 3, Max 4.
+* `Source`: Octad 0 `string`, Federation 1 `string`, Store 2 `string`.
+* `ProofClause`: Attached 0, Witness 1 `string`, Assert 2 `expr`.
+* `EffectDecl`: Read 0, Write 1, ReadWrite 2, Consume 3.
+* `VersionConstraint`: Latest 0, AtLeast 1 `u64`, Exact 2 `u64`,
+  Range 3 `u64,u64`.
+* `LinearAnnotation`: Unlimited 0, UseOnce 1, Bounded 2 `u64`.
+* `SelectItem`: Field 0 `fieldref`, Modality 1 `modality`,
+  Aggregate 2 `aggfunc,expr`, Star 3.
+* `Expr`: Field 0 `fieldref`, Literal 1 `literal`, Compare 2
+  `compop,expr,expr`, Logic 3 `logicop,expr,option<expr>`,
+  Aggregate 4 `aggfunc,expr`, Param 5 `string`, Star 6,
+  Subquery 7 `statement`, Epistemic 8 `epistemicop,agent,expr`,
+  Announce 9 `agent,expr,expr`.
+
+Composite: `FieldRef` = `modality` then `string` (field name).
+`EpistemicClause` = `list<agent>` then `list<EpistemicRequirement>`.
+
+== Statement (field order = the `Grammar.idr` record)
+
+`list<SelectItem>`, `Source`, `option<Expr>` (where),
+`list<FieldRef>` (group by), `option<Expr>` (having),
+`list<(FieldRef, bool)>` (order by; bool = ascending),
+`option<u64>` (limit), `option<u64>` (offset),
+`option<ProofClause>`, `option<EffectDecl>`,
+`option<VersionConstraint>`, `option<LinearAnnotation>`,
+`option<EpistemicClause>`, `SafetyLevel` (requested level).
+
+After the final field the stream MUST be exhausted; trailing bytes =>
+`WireError::TrailingBytes`.
+
+== Totality contract
+
+The decoder is *total*: bounds-checked, no panics, every malformed
+input a typed `WireError` (same SPARK-grade lint posture as the
+parser). `from_wire(to_wire(s)) == s` for every `Statement` (the
+round-trip proptest is the machine witness; bit-exact float preservation
+is pinned by a golden vector). `to_wire` is deterministic (canonical:
+exactly one byte string per value).

src/interface/parse/src/lib.rs

@@ -37,9 +37,11 @@
 pub mod ast;
 pub mod lexer;
 pub mod parser;
+pub mod wire;
 
 pub use ast::Statement;
 pub use parser::{parse, ParseError};
+pub use wire::{from_wire, to_wire, WireError};
 
 #[cfg(test)]
 mod tests {