Vest language reference
Overview
| Topic | Covers |
|---|---|
| File structure and lexical rules | definitions, comments, names, literals, and byte order |
| Primitive formats | integers, byte strings, Tail, Nothing, and Never |
| Refinements | integer and enum constraints |
| Structures and dependencies | fields, dependencies, constants, and length expressions |
| Enums | closed, open, typed, and bit-sized enums |
| Choices | dependent dispatch and ordered alternatives |
| Collections | arrays, Vec, and Option |
>>= | reinterpretation of a bounded byte region as another format |
| Bit fields | bits blocks, bit-sized fields, and bit-level refinements |
| Composition | format aliases, wrap, parameters, and macros |
| Recursion | self-recursive formats and mutually recursive formats |
How each construct is described
Every format construct is given as what it means on the wire, plus how it behaves under Vest’s three core executable APIs:
- parse reads bytes and returns a value together with the number of bytes consumed;
- prepare checks that a value is consistent with the format (its dependencies, constants, and refinement constraints all hold) and returns the exact number of bytes it will occupy;
- serialize writes a prepared value into a caller-owned buffer of exactly that size, without failing or allocating.
The generated Rust code guide explains the Rust types, format types, executable APIs, and specs/proofs that the compiler emits for each construct. The construct-to-Rust table provides a quick reference for the DSL constructs and their corresponding Rust types.
Limitations
- The DSL does not support polymorphic or “higher-kinded” formats that take other formats as parameters.
- The DSL does not support arbitrary semantic transformations or parsing actions on the data.
- The DSL does not support expressing backward dependencies (e.g., a field that depends on a later field like footers).
- The DSL does not have a module/namespace system (so you cannot “import” a format from another
.vestfile). - The DSL does not support declaring “trusted”/“external” formats that are implemented in Rust/Verus and used in the DSL.