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

src/interface/WireConformance.idr

@@ -1,36 +1,35 @@
 -- 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)
+||| VCL-total Interface — Cross-language Wire Conformance (P5b/P5c)
 |||
-||| 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.
+||| Machine-checked proof that the certified Idris decoders
+||| (`WireDecode.fromWire` / `.fromWireSchema`) agree, byte-for-byte,
+||| with the trusted Rust encoder (`wire.rs` `to_wire`/
+||| `to_wire_schema`) 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.
+||| Each `goldenN`/`goldenSN` is the EXACT encoder image emitted by
+||| the Rust regeneration oracle
+||| `src/interface/parse/tests/conformance_emit.rs` (run that test with
+||| `--nocapture`; the literals are injected verbatim from its output,
+||| never hand-transcribed). `conformN`/`conformSN : from* goldenN =
+||| Right expectedN` 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 value. 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`).
+||| F1 minimal; F2 strings/ints/bools/agents/options/lists/nested
+||| comparison + every extension clause; F3 the float path (2.5);
+||| S1 (P5c) the `OctadSchema` path — 8 modality slots in record
+||| order, empty + non-empty field lists, bools, `TVector(Nat)`, and a
+||| recursive `VqlType` (`TList TString`).
 
 module VclTotal.Interface.WireConformance
 
 import VclTotal.ABI.Types
 import VclTotal.Core.Grammar
+import VclTotal.Core.Schema
 import VclTotal.Interface.WireDecode
 
 %default total
@@ -82,9 +81,7 @@ expected2 =
 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. ─────────
+-- ── F3: float path — WHERE 2.5 (exactly representable) ───────────────
 
 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]
@@ -99,3 +96,23 @@ expected3 =
 
 conform3 : fromWire WireConformance.golden3 = Right WireConformance.expected3
 conform3 = Refl
+
+-- ── S1 (P5c): OctadSchema path — 8 modality slots, VqlType recursion ─
+
+goldenS1 : List Bits8
+goldenS1 = [86,67,76,83,1,0,0,1,0,0,0,2,0,0,0,105,100,0,1,0,1,1,0,0,0,3,0,0,0,101,109,98,5,4,0,0,0,0,0,0,0,0,1,2,0,0,0,0,3,0,0,0,0,4,1,0,0,0,4,0,0,0,116,97,103,115,8,0,0,0,5,0,0,0,0,6,0,0,0,0,7,0,0,0,0]
+
+expectedS1 : OctadSchema
+expectedS1 =
+  MkOctadSchema
+    (MkModalitySchema Graph      [MkFieldDef "id" TString True False])
+    (MkModalitySchema Vector     [MkFieldDef "emb" (TVector 4) False True])
+    (MkModalitySchema Tensor     [])
+    (MkModalitySchema Semantic   [])
+    (MkModalitySchema Document   [MkFieldDef "tags" (TList TString) False False])
+    (MkModalitySchema Temporal   [])
+    (MkModalitySchema Provenance [])
+    (MkModalitySchema Spatial    [])
+
+conformS1 : fromWireSchema WireConformance.goldenS1 = Right WireConformance.expectedS1
+conformS1 = Refl

src/interface/WireDecode.idr

@@ -57,6 +57,7 @@ module VclTotal.Interface.WireDecode
 
 import VclTotal.ABI.Types
 import VclTotal.Core.Grammar
+import VclTotal.Core.Schema
 import Data.List
 
 %default total
@@ -641,3 +642,120 @@ fromWire input = do
   if ver /= 1 then Left BadVersion else Right ()
   (stmt, r2) <- decStmt (length input) r1
   if length r2 /= 0 then Left TrailingBytes else Right stmt
+
+-- ═══════════════════════════════════════════════════════════════════════
+-- P5c: OctadSchema decoder (schema marshalling for the recompute tier)
+--
+-- `VqlType` is recursive (TList/TNull/TRecord/TKnows/TBelieves/
+-- TCommonKnowledge nest VqlType), so its decoder is fuel-bounded
+-- exactly like `Expr`; the recursion-bearing record-field list is
+-- inlined into the same `mutual` block so the size-change analysis
+-- sees the fuel-decreasing edge directly. `VqlType` recursion is
+-- independent of `Statement`/`Expr` (it only nests `VqlType` and the
+-- non-recursive `Agent`), so this is its own block. Totality is
+-- structural, ZERO proof-escape, identical posture to the Statement
+-- decoder. The schema stream has its own magic (`VCLS`) so a
+-- schema/statement mix-up is a hard `BadMagic`.
+-- ═══════════════════════════════════════════════════════════════════════
+
+mutual
+  public export
+  decVqlType : Nat -> Parse VqlType
+  decVqlType Z     _   = Left OutOfFuel
+  decVqlType (S k) inp = do
+    (t, r0) <- byte inp
+    case t of
+      0  => Right (TString, r0)
+      1  => Right (TInt, r0)
+      2  => Right (TFloat, r0)
+      3  => Right (TBool, r0)
+      4  => Right (TBytes, r0)
+      5  => do (n, r) <- u64nat r0; Right (TVector n, r)
+      6  => Right (TTimestamp, r0)
+      7  => Right (THash, r0)
+      8  => do (v, r) <- decVqlType k r0; Right (TList v, r)
+      9  => do (fs, r) <- decVqlRecVec k r0; Right (TRecord fs, r)
+      10 => Right (TOctad, r0)
+      11 => do (v, r) <- decVqlType k r0; Right (TNull v, r)
+      12 => Right (TAny, r0)
+      13 => do (a, r1) <- decAgent r0
+               (v, r2) <- decVqlType k r1
+               Right (TKnows a v, r2)
+      14 => do (a, r1) <- decAgent r0
+               (v, r2) <- decVqlType k r1
+               Right (TBelieves a v, r2)
+      15 => do (v, r) <- decVqlType k r0; Right (TCommonKnowledge v, r)
+      x  => Left (BadTag "VqlType" x)
+
+  public export
+  decVqlRecN : Nat -> Nat -> Parse (List (String, VqlType))
+  decVqlRecN _    Z     i = Right ([], i)
+  decVqlRecN fuel (S c) i = do
+    (nm, i1)  <- vstring i
+    (vt, i2)  <- decVqlType fuel i1
+    (xs, i3)  <- decVqlRecN fuel c i2
+    Right ((nm, vt) :: xs, i3)
+
+  public export
+  decVqlRecVec : Nat -> Parse (List (String, VqlType))
+  decVqlRecVec fuel i = do
+    (n, r) <- u32count i
+    decVqlRecN fuel n r
+
+public export
+decFieldDef : Nat -> Parse FieldDef
+decFieldDef fuel inp = do
+  (nm, r1) <- vstring inp
+  (ty, r2) <- decVqlType fuel r1
+  (nl, r3) <- boolByte r2
+  (ix, r4) <- boolByte r3
+  Right (MkFieldDef nm ty nl ix, r4)
+
+public export
+decFieldDefsN : Nat -> Nat -> Parse (List FieldDef)
+decFieldDefsN _    Z     i = Right ([], i)
+decFieldDefsN fuel (S c) i = do
+  (x, i')   <- decFieldDef fuel i
+  (xs, i'') <- decFieldDefsN fuel c i'
+  Right (x :: xs, i'')
+
+public export
+decFieldDefVec : Nat -> Parse (List FieldDef)
+decFieldDefVec fuel i = do
+  (n, r) <- u32count i
+  decFieldDefsN fuel n r
+
+public export
+decModalitySchema : Nat -> Parse ModalitySchema
+decModalitySchema fuel inp = do
+  (m, r1)  <- decModality inp
+  (fs, r2) <- decFieldDefVec fuel r1
+  Right (MkModalitySchema m fs, r2)
+
+public export
+schemaMagic : List Bits8
+schemaMagic = [86, 67, 76, 83]   -- "VCLS"
+
+||| Decode a v1 `VCLS` wire stream into the certified `OctadSchema`.
+||| Total: every input yields `Right` or a typed `Left WireErr`, never
+||| a crash. Fuel is the input length (sound: every node costs >= 1
+||| discriminant byte). The 8 modality schemas are in `Schema.idr`
+||| record order; no count prefix (fixed arity).
+public export
+fromWireSchema : List Bits8 -> Either WireErr OctadSchema
+fromWireSchema input = do
+  (m, r0) <- takeN 4 input
+  if m /= schemaMagic then Left BadMagic else Right ()
+  (ver, r1) <- u16le r0
+  if ver /= 1 then Left BadVersion else Right ()
+  let f = length input
+  (gr, r2)  <- decModalitySchema f r1
+  (ve, r3)  <- decModalitySchema f r2
+  (te, r4)  <- decModalitySchema f r3
+  (se, r5)  <- decModalitySchema f r4
+  (do_, r6) <- decModalitySchema f r5
+  (tm, r7)  <- decModalitySchema f r6
+  (pr, r8)  <- decModalitySchema f r7
+  (sp, r9)  <- decModalitySchema f r8
+  if length r9 /= 0 then Left TrailingBytes
+    else Right (MkOctadSchema gr ve te se do_ tm pr sp)

src/interface/parse/WIRE-FORMAT.adoc

@@ -86,6 +86,20 @@ Defined here for v1 (no Idris int map existed; now normative):
 Composite: `FieldRef` = `modality` then `string` (field name).
 `EpistemicClause` = `list<agent>` then `list<EpistemicRequirement>`.
 
+`VqlType` (P5c — `Grammar.idr` `data VqlType`; recursive, so the
+decoder is fuel-bounded exactly like `Expr`). STABLE, append-only:
+
+* `TString` 0, `TInt` 1, `TFloat` 2, `TBool` 3, `TBytes` 4,
+  `TVector` 5 `u64` (dimension; Idris `Nat`), `TTimestamp` 6,
+  `THash` 7, `TList` 8 `vqltype`,
+  `TRecord` 9 `list<(string, vqltype)>`, `TOctad` 10,
+  `TNull` 11 `vqltype`, `TAny` 12, `TKnows` 13 `agent, vqltype`,
+  `TBelieves` 14 `agent, vqltype`, `TCommonKnowledge` 15 `vqltype`.
+
+Schema composites: `FieldDef` = `string` (name), `vqltype` (ty),
+`bool` (nullable), `bool` (indexed). `ModalitySchema` = `modality`
+then `list<FieldDef>`.
+
 == Statement (field order = the `Grammar.idr` record)
 
 `list<SelectItem>`, `Source`, `option<Expr>` (where),
@@ -99,6 +113,29 @@ Composite: `FieldRef` = `modality` then `string` (field name).
 After the final field the stream MUST be exhausted; trailing bytes =>
 `WireError::TrailingBytes`.
 
+== OctadSchema (P5c — schema marshalling)
+
+The recompute-PCC tier (see the transport note above) ships the
+`OctadSchema` alongside the `Statement` so the consumer can re-run the
+certified decider. This is a *separate* stream with its own header to
+make a schema/statement mix-up a hard `BadMagic`, not a silent
+mis-parse:
+
+Header: `56 43 4C 53` ("VCLS") then `u16` version (`01 00` for v1).
+
+Body — `OctadSchema` is the 8 modality schemas in `Grammar.idr`/
+`Schema.idr` record order (fixed arity, no count):
+
+`ModalitySchema` (graph), `ModalitySchema` (vector),
+`ModalitySchema` (tensor), `ModalitySchema` (semantic),
+`ModalitySchema` (document), `ModalitySchema` (temporal),
+`ModalitySchema` (provenance), `ModalitySchema` (spatial).
+
+After the 8th the stream MUST be exhausted (`TrailingBytes`
+otherwise). Same totality contract as the `Statement` decoder;
+`VqlType`'s recursion is fuel-bounded identically (every node ≥ 1
+discriminant byte).
+
 == Totality contract
 
 The decoder is *total*: bounds-checked, no panics, every malformed

src/interface/parse/src/lib.rs

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

src/interface/parse/src/schema.rs

@@ -0,0 +1,70 @@
+// SPDX-License-Identifier: PMPL-1.0-or-later
+// Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+
+//! Faithful Rust mirror of `src/core/Schema.idr`'s `OctadSchema`
+//! (and the `VqlType` it carries, from `src/core/Grammar.idr`).
+//!
+//! NOTE — why `VqlType` lives here and not in [`crate::ast`]: the
+//! parser deliberately omits `VqlType` because *parsing* establishes
+//! syntax only and never resolves types (see the `ast` module note).
+//! A *schema*, by contrast, IS a declaration of field types — `VqlType`
+//! is its payload, not dead data. Keeping it in this separate module
+//! preserves the parser's "syntax only" honesty while giving P5c the
+//! schema the certified decider needs to recompute the safety verdict.
+//! One-to-one with the Idris constructors so the wire codec is a
+//! structural map with no re-interpretation.
+
+use crate::ast::{Agent, Modality};
+
+/// `Grammar.idr`: `data VqlType`. Recursive (so its wire decoder is
+/// fuel-bounded, exactly like `Expr`).
+#[derive(Debug, Clone, PartialEq)]
+pub enum VqlType {
+    TString,
+    TInt,
+    TFloat,
+    TBool,
+    TBytes,
+    /// `TVector Nat` — fixed dimension (Idris `Nat`).
+    TVector(u64),
+    TTimestamp,
+    THash,
+    TList(Box<VqlType>),
+    TRecord(Vec<(String, VqlType)>),
+    TOctad,
+    TNull(Box<VqlType>),
+    TAny,
+    TKnows(Agent, Box<VqlType>),
+    TBelieves(Agent, Box<VqlType>),
+    TCommonKnowledge(Box<VqlType>),
+}
+
+/// `Schema.idr`: `record FieldDef`.
+#[derive(Debug, Clone, PartialEq)]
+pub struct FieldDef {
+    pub name: String,
+    pub ty: VqlType,
+    pub nullable: bool,
+    pub indexed: bool,
+}
+
+/// `Schema.idr`: `record ModalitySchema`.
+#[derive(Debug, Clone, PartialEq)]
+pub struct ModalitySchema {
+    pub modality: Modality,
+    pub fields: Vec<FieldDef>,
+}
+
+/// `Schema.idr`: `record OctadSchema` — the 8 modality schemas, in
+/// record order (fixed arity; no length prefix on the wire).
+#[derive(Debug, Clone, PartialEq)]
+pub struct OctadSchema {
+    pub graph: ModalitySchema,
+    pub vector: ModalitySchema,
+    pub tensor: ModalitySchema,
+    pub semantic: ModalitySchema,
+    pub document: ModalitySchema,
+    pub temporal: ModalitySchema,
+    pub provenance: ModalitySchema,
+    pub spatial: ModalitySchema,
+}