vcl-ut #25 P5c (step 1): certified OctadSchema wire codec + cross-language conformance

[hyperpolymath]

P5c (step 1) — certified OctadSchema wire codec + cross-language conformance

The recompute-PCC tier (the typed-wasm objective, per the two-tier
boundary model in VERIFICATION-STANCE.adoc) ships the OctadSchema
alongside the Statement so the consumer can re-run the certified
decider. This adds the schema half of the marshalling — certified
and conformance-proven — and closes the previously-OWED "C-ABI
Statement/OctadSchema marshalling" item for the decode/schema
direction.

Stacked on #29 (P5b step 2): WireDecode/WIRE-FORMAT.adoc aren't on
main yet. Base is the #29 branch; rebase to main once #29 merges.

Wire format (WIRE-FORMAT.adoc)

• 16 VqlType discriminants (STABLE, append-only) — recursive, so the
  decoder is fuel-bounded exactly like Expr.
• FieldDef/ModalitySchema composites; OctadSchema = 8 modality
  schemas in Schema.idr record order (fixed arity, no count).
• Distinct VCLS magic ⇒ schema/statement mix-up is a hard
  BadMagic, never a silent mis-parse.

Rust (trusted encoder)

• New schema module: faithful mirror of Schema.idr OctadSchema +
  Grammar.idr VqlType, with a documented note on why VqlType
  lives here and not in ast (a schema is type declarations; the
  parser's "syntax only" honesty is preserved by the module split).
• to_wire_schema/from_wire_schema — same SPARK posture (total,
  bounds-checked, no panic).

Idris (certified decoder, in the CI-gated corpus)

• WireDecode: decVqlType (fuel-bounded mutual block, recursive
  TRecord field-list inlined so size-change sees the decreasing
  edge), decFieldDef/decModalitySchema, fromWireSchema.
  %default total, ZERO proof-escape.
• WireConformance: conformS1 : fromWireSchema goldenS1 = Right expectedS1 by Refl — the schema decoder is proven
  byte-for-byte conformant with the Rust to_wire_schema encoder at
  compile time. S1 exercises all 8 modality slots, empty + non-empty
  field lists, bools, TVector(Nat), and recursive VqlType
  (TList TString).
• conformance_emit.rs regeneration oracle extended (schema fixture +
  round-trip self-check); golden bytes injected verbatim, never
  hand-transcribed.

Verified locally

• Corpus idris2 0.8.0 --build exit 0 — 12 modules (WireDecode
  4/12, WireConformance 5/12).
• CI proof-escape audit: OK: zero proof-escape symbols outside comments (the new code is in the audited file list).
• parse-gate equivalent: cargo clippy --all-targets --locked -D warnings clean, cargo test --locked green (incl. schema
  round-trip self-check), cargo fmt --check clean.

Where this sits in P5c

P5c = recompute-certified-decider over typed-wasm. This is step 1
(schema marshalling, the data both tiers need). Next: AffineScript
wire decoder + decision-core port → typed-wasm, the three-way
conformance harness (Idris-decider verdict == typed-wasm-decider
verdict), transport plumbing with the C/Zig fail-closed attestation
fallback, and the stance flip + ADR.

Refs #25.

🤖 Generated with Claude Code