vcl-ut #25 P5b (step 2): certified Idris wire decoder + cross-language Refl conformance

.github/workflows/proof-corpus.yml

@@ -64,7 +64,8 @@ jobs:
                  src/core/Levels.idr src/core/Checker.idr \
                  src/core/Composition.idr src/core/Epistemic.idr \
                  src/interface/abi/Types.idr src/interface/abi/Layout.idr \
-                 src/interface/abi/LayoutProofs.idr"
+                 src/interface/abi/LayoutProofs.idr \
+                 src/interface/WireDecode.idr src/interface/WireConformance.idr"
           if grep -nE '\b(believe_me|really_believe_me|assert_total|assert_smaller|idris_crash|postulate|sorry)\b' \
                $files | grep -vE ':\s*(--|\|\|\|)' ; then
             echo "::error::proof-escape symbol found in the Phase-1 corpus"

CHANGELOG.md

@@ -12,13 +12,14 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 
 ### Verified
 
-**VclTotal proof corpus — Phase 0→4 remediation** (2026-05-18/19,
-hyperpolymath/standards#124). The `src/core/**` Idris2 corpus, which at
+**VclTotal proof corpus — Phase 0→4 remediation + Phase 5 boundary
+reinforcement** (2026-05-18/19, hyperpolymath/standards#124,
+hyperpolymath/vcl-ut#25). The `src/core/**` Idris2 corpus, which at
 Phase 0 did not compile and had never been machine-checked, is now
 CI-gated and green:
 
 - `verification/proofs/vclut-core.ipkg` builds clean under idris2 0.8.0
-  (`idris2 --build`, exit 0, `%default total`) as **10 modules**, with
+  (`idris2 --build`, exit 0, `%default total`) as **12 modules**, with
   **zero proof-escape symbols** (no `believe_me`/`postulate`/`assert_*`/
   `idris_crash`/`sorry`), enforced by `.github/workflows/proof-corpus.yml`.
 - Phase 1 (#21): corpus resurrection — `ABI.Types`/`Grammar` repaired,
@@ -33,6 +34,26 @@ CI-gated and green:
   bounds) + L6–L10 `composeJoin` closure (`l6..l9Compose`,
   `epiStructJoin`); L10 acyclicity carried by the explicit
   `JoinSideCondition` (provably non-closed, not faked).
+- Phase 5 / vcl-ut#25 (boundary reinforcement): trusted Rust/SPARK-grade
+  parser (P5a, #26) + deterministic versioned wire codec (P5b step 1,
+  #28); **P5b step 2 (this change)** — `VclTotal.Interface.WireDecode`,
+  a total (`%default total`, zero proof-escape) decoder of the v1 wire
+  format into the certified `Statement`, recursion bounded by an
+  input-length fuel `Nat`; `VclTotal.Interface.WireConformance` proves
+  it byte-for-byte conformant with the Rust `to_wire` encoder by `Refl`
+  on golden fixtures (regeneration oracle:
+  `src/interface/parse/tests/conformance_emit.rs`). The C-ABI
+  `Statement` marshalling *decode* side is now certified. Disclosed:
+  the NaN *payload* is not preserved across the Idris `Double` boundary
+  (finite + infinite values bit-exact; Rust proptest remains the
+  exhaustive float witness). OWED: **P5c — typed-wasm PCC transport**
+  (proof term + checker kernel the consumer re-runs; *re-checkable*,
+  TCB = checker kernel; the estate-aligned objective — the `ffi/zig`
+  fail-closed shim is retained only as the C-ABI attestation
+  *fallback*, not the endpoint); **P5d** — the signed-attestation
+  fallback contract for C-only consumers. Re-checkable transport is
+  impossible only over a C ABI, not over typed-wasm (two-tier boundary
+  model: `verification/proofs/VERIFICATION-STANCE.adoc`).
 
 `verification/proofs/VERIFICATION-STANCE.adoc` is the authoritative,
 precisely-scoped catalogue (residual OWED items disclosed, not masked).

PROOF-NEEDS.md

@@ -6,8 +6,8 @@
 - **LOC**: ~8,000
 - **Languages**: Rust, ReScript, Idris2, Zig
 - **Existing ABI proofs**: `src/interface/abi/*.idr` + domain-specific Idris2: `src/core/Checker.idr`, `Grammar.idr`, `Levels.idr`, `Schema.idr`, `Composition.idr`
-- **Machine-verified**: the full `VclTotal` proof corpus — `verification/proofs/vclut-core.ipkg` builds clean under idris2 0.8.0 (`idris2 --build`, exit 0, `%default total`, **zero proof-escape symbols**, CI-gated by `.github/workflows/proof-corpus.yml`) as **10 modules** (`ABI.{Types,Layout,LayoutProofs}` + `Core.{Grammar,Schema,Decide,Levels,Checker,Composition,Epistemic}`), plus the self-contained `verification/proofs/SafetyL4Model.idr` (`--check`, exit 0). Phases 1–3 are on `origin/main` (PRs #21/#22/#23); Phase 4 (`LayoutProofs` + L6–L10 `composeJoin` closure) is **PR #24**, pending merge.
-- **Status (Phase 0 → 4 RESOLVED, honestly)**: the Phase-0 blockers are fixed, not faked — the corpus compiles and is machine-checked; `ABI.Types`/`Grammar` errors repaired; **L2/L3/L5 de-vacuized** (Phase 2, evidence-carrying predicates over `Core.Decide`); all ten levels carry `checkLevelNSound` and `Checker.certifyAt`/`certifyRequested` assemble a genuine dependent `SafetyCertificate` (Phase 3); the Zig FFI is no longer a fabricating stub — it is **fail-closed** with a proof-gated `Checker.certifiedLevel` mint (Phase 3d). Remaining honest gaps are precisely scoped (FFI proof-transport, string→`Statement` parser, L3 subquery/heuristic scoping, L9/L10 predicate depth, the additive↔ceil `alignUp` sliver). `verification/proofs/VERIFICATION-STANCE.adoc` is the authoritative, proof-backed catalogue and takes precedence over this file.
+- **Machine-verified**: the full `VclTotal` proof corpus — `verification/proofs/vclut-core.ipkg` builds clean under idris2 0.8.0 (`idris2 --build`, exit 0, `%default total`, **zero proof-escape symbols**, CI-gated by `.github/workflows/proof-corpus.yml`) as **12 modules** (`ABI.{Types,Layout,LayoutProofs}` + `Core.{Grammar,Schema,Decide,Levels,Checker,Composition,Epistemic}` + `Interface.{WireDecode,WireConformance}`), plus the self-contained `verification/proofs/SafetyL4Model.idr` (`--check`, exit 0). Phases 1–4 are on `origin/main` (PRs #21/#22/#23/#24); Phase 5 / vcl-ut#25 (trusted Rust parser P5a #26, wire codec P5b-step-1 #28, **certified Idris wire decoder + cross-language `Refl` conformance** P5b-step-2) reinforces the FFI boundary.
+- **Status (Phase 0 → 4 RESOLVED, honestly; Phase 5 boundary reinforcement in progress)**: the Phase-0 blockers are fixed, not faked — the corpus compiles and is machine-checked; `ABI.Types`/`Grammar` errors repaired; **L2/L3/L5 de-vacuized** (Phase 2, evidence-carrying predicates over `Core.Decide`); all ten levels carry `checkLevelNSound` and `Checker.certifyAt`/`certifyRequested` assemble a genuine dependent `SafetyCertificate` (Phase 3); the Zig FFI is no longer a fabricating stub — it is **fail-closed** with a proof-gated `Checker.certifiedLevel` mint (Phase 3d). **Phase 5 (vcl-ut#25)**: a trusted Rust/SPARK-grade parser + a deterministic versioned wire codec exist, and the *decode* side of the C-ABI `Statement` marshalling is now **certified** — `VclTotal.Interface.WireDecode` is a total (zero-escape) decoder proven byte-for-byte conformant with the Rust encoder by `Refl` (`WireConformance`). Remaining honest gaps are precisely scoped (P5c = typed-wasm PCC proof-transport — proof term + checker kernel the consumer re-runs, *re-checkable*, the estate-aligned objective; the C-ABI/Zig shim retained only as the fail-closed attestation fallback; P5d = signed-attestation *fallback* contract for C-only consumers; plus L3 subquery/heuristic scoping; L9/L10 predicate depth; the additive↔ceil `alignUp` sliver; the disclosed NaN-payload limitation of the Idris `Double` boundary). Re-checkable transport is impossible *only* over a C ABI, not over the estate's typed-wasm target. `verification/proofs/VERIFICATION-STANCE.adoc` is the authoritative, proof-backed catalogue and takes precedence over this file.
 
 ## What Needs Proving
 
@@ -44,6 +44,23 @@
 - The *trusted* boundary parser is the Rust/SPARK-grade
   `src/interface/parse` crate (`vcltotal-parse`, P5a of vcl-ut#25),
   which mirrors `Grammar.idr` and feeds the certifier across the C-ABI.
+  Its `wire.rs` codec (P5b step 1) serialises the parsed `Statement`
+  to a deterministic versioned binary format
+  (`src/interface/parse/WIRE-FORMAT.adoc`).
+- The *certified* receiver of that format is
+  `VclTotal.Interface.WireDecode` (P5b step 2): a total, zero-escape
+  Idris decoder into the certified `Statement`, proven byte-for-byte
+  conformant with the Rust encoder by `Refl` in
+  `VclTotal.Interface.WireConformance`. The marshalling seam's *decode*
+  side is therefore now machine-verified. **P5c** (the estate-aligned
+  objective): transport the certificate over the **typed-wasm** target
+  as a proof term + a small checker kernel the consumer re-runs —
+  proof-carrying code, *re-checkable*, TCB = checker kernel + typed-wasm
+  verifier (re-checkable transport is impossible only over a C ABI; the
+  `ffi/zig` fail-closed shim is retained only as the C-ABI attestation
+  fallback). **P5d** (fallback tier): the signed-attestation contract
+  for consumers reachable only over C. Both OWED; see the two-tier
+  boundary model in `verification/proofs/VERIFICATION-STANCE.adoc`.
 - Optional future work: prove the ReScript frontend faithfully tracks
   the Idris2 grammar (low priority; it is a convenience frontend, not a
   trust anchor).

src/interface/WireConformance.idr

@@ -0,0 +1,101 @@
+-- SPDX-License-Identifier: PMPL-1.0-or-later
+-- Copyright (c) 2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
+
+||| VCL-total Interface — Cross-language Wire Conformance (P5b step 2)
+|||
+||| Machine-checked proof that the certified Idris decoder
+||| (`VclTotal.Interface.WireDecode.fromWire`) agrees, byte-for-byte,
+||| with the trusted Rust encoder (`src/interface/parse/src/wire.rs`
+||| `to_wire`) on shared golden fixtures.
+|||
+||| Each `goldenN` is the EXACT `to_wire` image emitted by the Rust
+||| regeneration oracle `src/interface/parse/tests/conformance_emit.rs`
+||| (run that test with `--nocapture` to re-derive these literals; the
+||| literals below are injected verbatim from its output, never
+||| hand-transcribed). The corresponding
+||| `conformN : fromWire goldenN = Right expectedN` is proved by `Refl`:
+||| the corpus build only succeeds if the total decoder, evaluated at
+||| compile time on the Rust bytes, reduces to exactly the expected
+||| certified `Statement`. This is WIRE-FORMAT.adoc's conformance
+||| contract discharged as a proof, not a runtime test — no
+||| proof-escape, %default total.
+|||
+||| Fixtures: F1 minimal; F2 exercises strings / ints / bools / agents /
+||| options / lists / a nested comparison expression and every extension
+||| clause; F3 the float path with the exactly-representable `2.5`
+||| (arbitrary-`f64` bit-exactness — incl. the NaN payload, which the
+||| Idris `Double` boundary does NOT preserve, by disclosure — is the
+||| Rust proptest's job: `wire.rs::golden_bit_exact_floats`).
+
+module VclTotal.Interface.WireConformance
+
+import VclTotal.ABI.Types
+import VclTotal.Core.Grammar
+import VclTotal.Interface.WireDecode
+
+%default total
+
+-- ── F1: minimal — SELECT * FROM STORE "main", level SchemaBound ──────
+
+golden1 : List Bits8
+golden1 = [86,67,76,87,1,0,1,0,0,0,3,2,4,0,0,0,109,97,105,110,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,1]
+
+expected1 : Statement
+expected1 =
+  MkStatement [SelStar] (SrcStore "main")
+    Nothing [] Nothing [] Nothing Nothing
+    Nothing Nothing Nothing Nothing Nothing
+    SchemaBound
+
+conform1 : fromWire WireConformance.golden1 = Right WireConformance.expected1
+conform1 = Refl
+
+-- ── F2: strings/ints/bools/agents/options/lists/nested expr + every
+--       extension clause; level EpistemicSafe ─────────────────────────
+
+golden2 : List Bits8
+golden2 = [86,67,76,87,1,0,2,0,0,0,0,0,2,0,0,0,105,100,3,0,6,0,0,0,117,117,105,100,45,49,1,2,0,0,1,1,0,0,0,120,1,1,7,0,0,0,0,0,0,0,0,0,0,0,0,1,0,0,0,5,1,0,0,0,116,1,1,10,0,0,0,0,0,0,0,0,1,1,1,0,0,0,119,1,2,1,1,3,0,0,0,0,0,0,0,1,1,1,2,0,0,0,0,1,5,0,0,0,108,101,97,110,52,1,0,0,0,0,0,1,3,1,10]
+
+expected2 : Statement
+expected2 =
+  MkStatement
+    [SelField (MkFieldRef Graph "id"), SelStar]
+    (SrcOctad "uuid-1")
+    (Just (ECompare Eq
+             (EField (MkFieldRef Vector "x") TAny)
+             (ELiteral (LitInt 7) TAny)
+             TAny))
+    []
+    Nothing
+    [(MkFieldRef Temporal "t", True)]
+    (Just 10)
+    Nothing
+    (Just (ProofWitness "w"))
+    (Just EffReadWrite)
+    (Just (VerAtLeast 3))
+    (Just LinUseOnce)
+    (Just (EpClause
+             [AgEngine, AgProver "lean4"]
+             [EpReqKnows AgEngine (ELiteral (LitBool True) TAny)]))
+    EpistemicSafe
+
+conform2 : fromWire WireConformance.golden2 = Right WireConformance.expected2
+conform2 = Refl
+
+-- ── F3: float path — WHERE 2.5 (exactly representable), level
+--       ParseSafe. Witnesses the IEEE-754 reconstruction reduces to
+--       the identical primitive `Double` under the evaluator. ─────────
+
+golden3 : List Bits8
+golden3 = [86,67,76,87,1,0,1,0,0,0,3,2,1,0,0,0,115,1,1,2,0,0,0,0,0,0,4,64,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0]
+
+expected3 : Statement
+expected3 =
+  MkStatement [SelStar] (SrcStore "s")
+    (Just (ELiteral (LitFloat 2.5) TAny))
+    [] Nothing [] Nothing Nothing
+    Nothing Nothing Nothing Nothing Nothing
+    ParseSafe
+
+conform3 : fromWire WireConformance.golden3 = Right WireConformance.expected3
+conform3 = Refl