diff --git a/src/interface/WireConformance.idr b/src/interface/WireConformance.idr index a553443..d7d5349 100644 --- a/src/interface/WireConformance.idr +++ b/src/interface/WireConformance.idr @@ -1,36 +1,35 @@ -- SPDX-License-Identifier: PMPL-1.0-or-later -- Copyright (c) 2026 Jonathan D.A. Jewell -||| 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 diff --git a/src/interface/WireDecode.idr b/src/interface/WireDecode.idr index ae09b83..6740dbb 100644 --- a/src/interface/WireDecode.idr +++ b/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) diff --git a/src/interface/parse/WIRE-FORMAT.adoc b/src/interface/parse/WIRE-FORMAT.adoc index 617749a..0c0e00b 100644 --- a/src/interface/parse/WIRE-FORMAT.adoc +++ b/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` then `list`. +`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`. + == Statement (field order = the `Grammar.idr` record) `list`, `Source`, `option` (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 diff --git a/src/interface/parse/src/lib.rs b/src/interface/parse/src/lib.rs index 5df1023..9a75985 100644 --- a/src/interface/parse/src/lib.rs +++ b/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 { diff --git a/src/interface/parse/src/schema.rs b/src/interface/parse/src/schema.rs new file mode 100644 index 0000000..46762c5 --- /dev/null +++ b/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) + +//! 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), + TRecord(Vec<(String, VqlType)>), + TOctad, + TNull(Box), + TAny, + TKnows(Agent, Box), + TBelieves(Agent, Box), + TCommonKnowledge(Box), +} + +/// `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, +} + +/// `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, +} diff --git a/src/interface/parse/src/wire.rs b/src/interface/parse/src/wire.rs index 1578248..106397e 100644 --- a/src/interface/parse/src/wire.rs +++ b/src/interface/parse/src/wire.rs @@ -12,8 +12,12 @@ //! counts, every malformed input a typed [`WireError`]. use crate::ast::*; +use crate::schema::{FieldDef, ModalitySchema, OctadSchema, VqlType}; const MAGIC: [u8; 4] = *b"VCLW"; +/// Distinct magic for the P5c `OctadSchema` stream so a schema/statement +/// mix-up is a hard `BadMagic`, never a silent mis-parse. +const SCHEMA_MAGIC: [u8; 4] = *b"VCLS"; const VERSION: u16 = 1; /// Total decode failure (never a panic). @@ -843,3 +847,176 @@ fn dec_stmt(d: &mut D) -> Result { requested_level, }) } + +// ── P5c: OctadSchema codec (schema marshalling for the recompute tier) + +fn enc_vqltype(t: &VqlType, o: &mut Vec) { + match t { + VqlType::TString => put_u8(o, 0), + VqlType::TInt => put_u8(o, 1), + VqlType::TFloat => put_u8(o, 2), + VqlType::TBool => put_u8(o, 3), + VqlType::TBytes => put_u8(o, 4), + VqlType::TVector(n) => { + put_u8(o, 5); + put_u64(o, *n); + } + VqlType::TTimestamp => put_u8(o, 6), + VqlType::THash => put_u8(o, 7), + VqlType::TList(inner) => { + put_u8(o, 8); + enc_vqltype(inner, o); + } + VqlType::TRecord(fields) => { + put_u8(o, 9); + put_len(o, fields.len()); + for (name, fty) in fields { + put_str(o, name); + enc_vqltype(fty, o); + } + } + VqlType::TOctad => put_u8(o, 10), + VqlType::TNull(inner) => { + put_u8(o, 11); + enc_vqltype(inner, o); + } + VqlType::TAny => put_u8(o, 12), + VqlType::TKnows(a, inner) => { + put_u8(o, 13); + enc_agent(a, o); + enc_vqltype(inner, o); + } + VqlType::TBelieves(a, inner) => { + put_u8(o, 14); + enc_agent(a, o); + enc_vqltype(inner, o); + } + VqlType::TCommonKnowledge(inner) => { + put_u8(o, 15); + enc_vqltype(inner, o); + } + } +} + +fn enc_fielddef(f: &FieldDef, o: &mut Vec) { + put_str(o, &f.name); + enc_vqltype(&f.ty, o); + put_bool(o, f.nullable); + put_bool(o, f.indexed); +} + +fn enc_modschema(m: &ModalitySchema, o: &mut Vec) { + enc_modality(&m.modality, o); + put_len(o, m.fields.len()); + for fd in &m.fields { + enc_fielddef(fd, o); + } +} + +/// Serialise an `OctadSchema` to the v1 `VCLS` wire stream. Total. +pub fn to_wire_schema(s: &OctadSchema) -> Vec { + let mut o = Vec::new(); + o.extend_from_slice(&SCHEMA_MAGIC); + o.extend_from_slice(&VERSION.to_le_bytes()); + enc_modschema(&s.graph, &mut o); + enc_modschema(&s.vector, &mut o); + enc_modschema(&s.tensor, &mut o); + enc_modschema(&s.semantic, &mut o); + enc_modschema(&s.document, &mut o); + enc_modschema(&s.temporal, &mut o); + enc_modschema(&s.provenance, &mut o); + enc_modschema(&s.spatial, &mut o); + o +} + +fn dec_vqltype(d: &mut D) -> Result { + match d.u8()? { + 0 => Ok(VqlType::TString), + 1 => Ok(VqlType::TInt), + 2 => Ok(VqlType::TFloat), + 3 => Ok(VqlType::TBool), + 4 => Ok(VqlType::TBytes), + 5 => Ok(VqlType::TVector(d.u64()?)), + 6 => Ok(VqlType::TTimestamp), + 7 => Ok(VqlType::THash), + 8 => Ok(VqlType::TList(Box::new(dec_vqltype(d)?))), + 9 => { + let fields = d.vec(|dd| { + let name = dd.string()?; + let fty = dec_vqltype(dd)?; + Ok((name, fty)) + })?; + Ok(VqlType::TRecord(fields)) + } + 10 => Ok(VqlType::TOctad), + 11 => Ok(VqlType::TNull(Box::new(dec_vqltype(d)?))), + 12 => Ok(VqlType::TAny), + 13 => { + let a = dec_agent(d)?; + Ok(VqlType::TKnows(a, Box::new(dec_vqltype(d)?))) + } + 14 => { + let a = dec_agent(d)?; + Ok(VqlType::TBelieves(a, Box::new(dec_vqltype(d)?))) + } + 15 => Ok(VqlType::TCommonKnowledge(Box::new(dec_vqltype(d)?))), + t => Err(WireError::BadTag { + ty: "VqlType", + tag: t, + }), + } +} + +fn dec_fielddef(d: &mut D) -> Result { + let name = d.string()?; + let ty = dec_vqltype(d)?; + let nullable = d.boolean()?; + let indexed = d.boolean()?; + Ok(FieldDef { + name, + ty, + nullable, + indexed, + }) +} + +fn dec_modschema(d: &mut D) -> Result { + let modality = dec_modality(d)?; + let fields = d.vec(dec_fielddef)?; + Ok(ModalitySchema { modality, fields }) +} + +/// Decode a v1 `VCLS` wire stream into an `OctadSchema`. Total: every +/// input yields `Ok`/`Err`, never a panic (same contract as +/// [`from_wire`]). +pub fn from_wire_schema(input: &[u8]) -> Result { + let mut d = D { b: input, pos: 0 }; + if d.take(4)? != SCHEMA_MAGIC { + return Err(WireError::BadMagic); + } + let ver = d.u16()?; + if ver != VERSION { + return Err(WireError::BadVersion(ver)); + } + let graph = dec_modschema(&mut d)?; + let vector = dec_modschema(&mut d)?; + let tensor = dec_modschema(&mut d)?; + let semantic = dec_modschema(&mut d)?; + let document = dec_modschema(&mut d)?; + let temporal = dec_modschema(&mut d)?; + let provenance = dec_modschema(&mut d)?; + let spatial = dec_modschema(&mut d)?; + if d.pos != d.b.len() { + return Err(WireError::TrailingBytes); + } + Ok(OctadSchema { + graph, + vector, + tensor, + semantic, + document, + temporal, + provenance, + spatial, + }) +} diff --git a/src/interface/parse/tests/conformance_emit.rs b/src/interface/parse/tests/conformance_emit.rs index eae0e56..9e3a8ce 100644 --- a/src/interface/parse/tests/conformance_emit.rs +++ b/src/interface/parse/tests/conformance_emit.rs @@ -22,7 +22,8 @@ #![allow(clippy::unwrap_used, clippy::expect_used, clippy::panic)] use vcltotal_parse::ast::*; -use vcltotal_parse::to_wire; +use vcltotal_parse::schema::*; +use vcltotal_parse::{to_wire, to_wire_schema}; fn line(name: &str, s: &Statement) { let b = to_wire(s); @@ -30,6 +31,53 @@ fn line(name: &str, s: &Statement) { println!("{name} = [{body}]"); } +fn line_schema(name: &str, s: &OctadSchema) { + let b = to_wire_schema(s); + let body = b.iter().map(u8::to_string).collect::>().join(","); + println!("{name} = [{body}]"); +} + +/// Minimal P5c schema fixture: exercises empty + non-empty field +/// lists, all 8 modality slots in record order, bools, and a recursive +/// `VqlType` (`TList`) plus `TVector(Nat)`. +fn sch1() -> OctadSchema { + let m = |modality, fields| ModalitySchema { modality, fields }; + OctadSchema { + graph: m( + Modality::Graph, + vec![FieldDef { + name: "id".to_string(), + ty: VqlType::TString, + nullable: true, + indexed: false, + }], + ), + vector: m( + Modality::Vector, + vec![FieldDef { + name: "emb".to_string(), + ty: VqlType::TVector(4), + nullable: false, + indexed: true, + }], + ), + tensor: m(Modality::Tensor, vec![]), + semantic: m(Modality::Semantic, vec![]), + document: m( + Modality::Document, + vec![FieldDef { + name: "tags".to_string(), + ty: VqlType::TList(Box::new(VqlType::TString)), + nullable: false, + indexed: false, + }], + ), + temporal: m(Modality::Temporal, vec![]), + provenance: m(Modality::Provenance, vec![]), + spatial: m(Modality::Spatial, vec![]), + } +} + fn f1() -> Statement { Statement { select_items: vec![SelectItem::Star], @@ -117,6 +165,7 @@ fn emit() { line("golden1", &f1()); line("golden2", &f2()); line("golden3", &f3()); + line_schema("goldenS1", &sch1()); } /// Self-check: every fixture round-trips through the Rust codec, so the @@ -127,4 +176,8 @@ fn fixtures_roundtrip() { for s in [f1(), f2(), f3()] { assert_eq!(vcltotal_parse::from_wire(&to_wire(&s)).unwrap(), s); } + assert_eq!( + vcltotal_parse::from_wire_schema(&to_wire_schema(&sch1())).unwrap(), + sch1() + ); }