Skip to content

WIRE-FORMAT.adoc

Latest commit

 

History

History
184 lines (151 loc) · 8.4 KB

WIRE-FORMAT.adoc

File metadata and controls

184 lines (151 loc) · 8.4 KB
Raw

VCL-total Statement Wire Format v1 (P5b, vcl-ut#25)

Table of Contents

The Statement marshalling format. 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 byte representation of the Statement that crosses the hypatia<→verisim seam; it is specified, not improvised.

Note
 This format is transport-agnostic. It is the marshalling payload over the C-ABI fallback tier (trusted-certifier attestation, P5d) and the proof-term payload over the estate’s typed-wasm target, where it rides with a checker kernel the consumer re-runs (proof-carrying code — re-checkable, TCB = checker kernel; the P5c objective). Re-checkable transport is impossible only over a C ABI, not over typed-wasm; see the two-tier boundary model in verification/proofs/VERIFICATION-STANCE.adoc ("What is NOT proven"), the authoritative catalogue.

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>.

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), 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.

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 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).

Certified decoder + cross-language conformance (P5b step 2)

This format is no longer Rust-only. VclTotal.Interface.WireDecode (src/interface/WireDecode.idr, in the CI-gated proof corpus verification/proofs/vclut-core.ipkg) is a second, independent decoder of this exact byte stream into Grammar.idr’s certified `Statement. It is machine-checked %default total with zero proof-escape (no believe_me/postulate/assert_*/idris_crash/ sorry): the same trusted-boundary totality contract as the Rust from_wire, but discharged by the type-checker rather than asserted — recursion is bounded by an input-length fuel Nat (sound because every node costs >= 1 discriminant byte).

Cross-language conformance is a proof, not a test: src/interface/parse/tests/conformance_emit.rs is the regeneration oracle (emits the exact to_wire image of fixed Statement`s); `VclTotal.Interface.WireConformance embeds those bytes verbatim and proves fromWire goldenN = Right expectedN by Refl. The corpus build fails unless the Idris decoder, evaluated at compile time on the Rust encoder’s bytes, reduces to exactly the expected certified Statement. Fixtures cover the minimal case, the full clause/agent/nested-expression surface, and the float path.

Disclosed limitation — NaN payload

Idris2 0.8.0 has no pure, bit-exact Bits64 → Double. The certified decoder reconstructs finite values (incl. subnormals and f64::MIN/ MAX) and both infinities bit-exactly by exact power-of-two scaling. A NaN bit-pattern decodes to a NaN; the NaN payload is NOT preserved across the Idris Double boundary. This is disclosed, not papered over: every consumer still agrees "this is NaN" (the semantically meaningful invariant), and exhaustive bit-exact float preservation — including the NaN payload — remains witnessed on the Rust side by wire.rs::golden_bit_exact_floats. The omitted VqlType slots are filled TAny (the grammar’s documented "unresolved type before type checking"; the 10-level checker resolves them at Level 2+) — faithful, not a shortcut.