Introduction

Vest generates secure, performant parsers and serializers for binary data formats, formally verified in Verus. It provides a concise format DSL for non-experts, as well as a combinator library for experts who want to build formats directly in Verus.

Given a high-level format description, Vest automatically emits efficient, idiomatic Rust that is memory-safe, arithmetically safe, panic-free, and terminating on any input. More importantly, Vest parsers and serializers are proven to satisfy a suite of desirable security properties, making them immune to entire classes of attacks that historically plague unverified, hand-written code.

With Vest, we have built the first production-grade formally verified ASN.1 library (supporting both DER and BER, which we leverage to implement the first verified CMS codec), and a verified prototype for both general and deterministic CBOR.

Who this is for

Vest is for anyone who needs to parse or serialize binary data formats, especially when correctness and security are critical. This includes: network security protocols such as TLS and IKE, which parse handshake messages and serialize authenticated responses; cryptographic message formats such as X.509 and CMS, which encode certificates, signed objects, keys, and algorithm parameters; executable and secure-update formats carrying code alongside authenticated metadata; and RPC and distributed-systems frameworks, which marshal typed application objects onto wire formats such as Protocol Buffers.

Vest is still a research tool. It does not cover every format in the wild, and its current features and limitations are documented.

As of now, this book covers the nitty-gritty of the DSL and the ASN.1 compiler. We are working on a guide to the underlying combinator library, as well as a more complete support for CBOR.

Choose your path

The project repository holds the source code for the combinator library, the DSL compiler, the ASN.1 library and frontend, and the CBOR codec.

Getting started

This tutorial shows how to install Vest, define a simple tag-length-value (TLV) format in the DSL, compile it to Rust, parse a message in that format, and serialize a value according to the format.

Install

Prerequisites: a stable Rust toolchain with cargo and rustc on your PATH.

cargo install vest

That puts the vest compiler on your PATH. In the crate that will hold the generated code, add the following dependencies to Cargo.toml:

cargo add vest_lib
cargo add vstd@=0.0.0-2026-08-23-0033 --no-default-features

which gives you:

[dependencies]
vest_lib = "0.2"
vstd = { version = "=0.0.0-2026-08-23-0033", default-features = false }

Generated modules refer to vstd directly, so it has to be a direct dependency even when you are only compiling and running the executable Rust. The version has to be exact (we’ll try to keep this doc up to date as much as possible): Verus and vstd move quickly, and each Vest release tracks one release of each.

vest_lib has three configurations — the default std, alloc alone for no_std with a heap, and neither for core-only. See Feature configurations.

Describe a format

Let’s define a simple Tag-length-value (TLV) format in the Vest DSL, which is the shape underneath most network protocols. A tag says what follows, a length delimits it, and the body is interpreted according to the tag.

Create msg.vest:

msg_type = enum {
  Msg1 = 1,
  Msg2 = 2,
  Msg3 = 3,
}

msg1 = { a: u8, b: u16, c: [u8; 3], data: Tail, }
msg2 = { a: u8, b: u16, c: u32, }
msg3 = { data: [u8; 6], }

msg = {
  @tag: msg_type,
  @len: u16,
  content: [u8; @len] >>= choose(@tag) {
    Msg1 => msg1,
    Msg2 => msg2,
    Msg3 => msg3,
  },
}

The syntax is mostly self-explanatory, akin to those of Rust. There are a few things to notice inside the msg definition:

• @tag and @len are field dependencies. The @ prefix lets later fields refer to them. They are still ordinary fields of the generated struct, and of course still bytes on the wire. @ only signals that they are used in later format expressions.
• [u8; @len] carves out exactly len bytes.
• >>= choose(@tag) then reparses that region with the format chosen by tag. Because the region is bounded first, a body that tries to read past its length would fail. We will see what it means for serialization shortly.

Integers are little-endian by default. Add !BIG_ENDIAN at the top of the file to switch to big-endian.

Generate Rust

$ vest msg.vest -o src/msg.rs
📜 Parsing the vest file...
🔨 Elaborating the AST...
🔍 Type checking...
📝 Generating the verus file...
👏 Done!

Without -o, the compiler writes next to the input and replaces its extension, so msg.vest becomes msg.rs. The generated module is a normal Rust file, so you can mod msg; it and use it like any other module.

See here for how to automate this process in build.rs so that the generated code is always up to date.

The DSL compiler emits one value type per definition, plus a zero-sized format type carrying the parser, serializer, and proofs:

pub enum MsgType { Msg1 = 1, Msg2 = 2, Msg3 = 3 }

pub struct Msg1<'i> { pub a: u8, pub b: u16, pub c: &'i [u8], pub data: &'i [u8] }
pub struct Msg2      { pub a: u8, pub b: u16, pub c: u32 }
pub struct Msg3<'i>  { pub data: &'i [u8] }

pub enum MsgContent<'i> { Msg1(Msg1<'i>), Msg2(Msg2), Msg3(Msg3<'i>) }

pub struct Msg<'i> {
    pub tag: MsgType,
    pub len: u16,
    pub content: MsgContent<'i>,
}

pub struct MsgFmt;   // the format: parser + serializer + proofs

// ... specifications, proofs, and executable APIs

Checking the proofs (highly recommended)

Technically, you do not need to install Verus to use Vest, especially if you are working with unverified Rust and just want to parse and serialize things more safely. However, Vest-generated code comes with specifications and proofs that establish the correctness and security of the parser and serializer. It is therefore highly recommended to use Verus to automatically check the proofs (rather than trusting the DSL compiler) to ensure that the generated code indeed satisfies the desired properties.

Each Vest release tracks one exact Verus release, recorded in verus.json. Follow the Verus installation instructions and match that version, or let the script in the Vest repository install it for you:

git clone https://github.com/secure-foundations/vest.git
./vest/scripts/install-verus.sh
export PATH="$PWD/vest/.verus:$PATH"

Then verify your crate, the one holding the generated module:

cd my-project
cargo verus verify

Verus checks every specification and proof in src/msg.rs, so a successful run means that the guarantees hold for your format and the generated parser and serializer.

Parse

use vest_lib::core::exec::{Parser, Prepare, SerializerExt};
use crate::msg::*;

let wire: &[u8] = &[
    0x02,                               // tag = Msg2
    0x07, 0x00,                         // len = 7
    0xAA,                               // a
    0xBB, 0xCC,                         // b
    0xDD, 0xEE, 0xFF, 0x11,             // c
];

let (consumed, msg) = MsgFmt.parse(&wire).unwrap();
assert_eq!(consumed, 10);
assert_eq!(msg.tag, MsgType::Msg2);
assert_eq!(msg.len, 7);
assert!(matches!(msg.content, MsgContent::Msg2(_)));

parse returns the parsed value and how many bytes it consumed, so a caller reading a stream knows where the next message begins (it does not mandate that the input slice end exactly at the message boundary). The msg value in the example copies and re-interprets the wire bytes because msg2 only contains fixed-size integers (where “zero-copy” pointers to the input buffer would be even less efficient). For larger payloads, Vest uses borrowed slices to avoid unnecessary copies/allocations.

Serialize (and beyond)

Serializing in Vest is two steps. The standard way is to call prepare first, which dynamically checks that the value is valid (we will see what that means) and returns the exact wire length of the serialized representation. Then you allocate a buffer of that length and call serialize to write into it. This two-step process allows Vest to serialize without failing, nor allocating memory during serialization.

Using the msg value from the parse example:

let len = MsgFmt.prepare(&msg).unwrap();
let mut output = vec![0u8; len];
MsgFmt.serialize(&msg, &mut output);
assert_eq!(output.as_slice(), wire);

Now build a new msg from scratch:

let msg = Msg {
    tag: MsgType::Msg2,
    len: 7, // u8 + u16 + u32 = 1 + 2 + 4 = 7
    content: MsgContent::Msg2(Msg2 { a: 0xAA, b: 0xBBCC, c: 0xDDEEFF11 }),
};

let len = MsgFmt.prepare(&msg).unwrap();   // 10

A wrong len is rejected by prepare:

let bad = Msg {
    tag: MsgType::Msg2,
    len: 99, // wrong length for the content
    content: MsgContent::Msg2(Msg2 { a: 0xAA, b: 0xBBCC, c: 0xDDEEFF11 }),
};

assert!(MsgFmt.prepare(&bad).is_err());

This would produce an error like:

PreSerializeError { kind: NotCompliant(LengthInconsistent), .. }

This is the field dependency being enforced in the other direction. Unlike for parsing, where @len determines how many bytes to read subsequently, a dependency like @len is a constraint the value must satisfy before serialization, and prepare is where that is checked.

What was proven

The generated module carries proofs that, among other things, parsing/serializing is memory and arithmetically safe, panic-free, and terminating; and that a successful parse reconstructs the original serialized value and consumes exactly as many bytes as the value would serialize to. See What Vest proves for a complete list of properties.

Where next

• Language reference — every format construct, and the current limitations.
• Generated Rust Code — the full shape of what comes out of the compiler.
• Troubleshooting — what the common errors mean.
• ASN.1 frontend — generate DER or BER from an ASN.1 module instead of writing a .vest file.

What Vest proves

Binary parsers and serializers are a classic source of security vulnerabilities, due to the conflicting goals of high performance and adherence to complex binary formats. The most common implementation mistakes are:

• Memory safety issues, such as use-after-free, double-free, and out-of-bounds accesses
• Arithmetic issues, such as integer overflow and underflow
• Improper Input Validation
• Deserialization of Untrusted Data
• Uncontrolled Resource Consumption
• Uncontrolled Recursion

There are also more subtle issues that root in the format itself, such as:

• Format confusion. It occurs when objects from different semantic domains, or distinct objects from the same semantic domain are encoded with the same byte representation. In this case, a parser fundamentally cannot distinguish between the two objects, making it vulnerable to cross-protocol attacks.
• Format malleability. It occurs when a single object can be encoded in multiple ways, and a parser accepts all of them. In this case, a parser can be tricked into accepting a modified input that is semantically equivalent to the original, but would yield completely different hash values or signatures. This is a common source of signature forgery or transaction malleability attacks.

Vest’s answer is to formally prove the absence of these vulnerabilities, for each format you define, without asking you to write proofs.

This page describes Vest’s formal guarantees in plain words. For the formal definitions, see the core specs in vest_lib.

Safety, for every format

These hold for every format Vest generates.

• Memory safety. Parsers and serializers are written in safe Rust, so Rust’s ownership and borrowing rules rule out use-after-free and double-free. Verus adds proofs that there are no out-of-bounds accesses.
• Arithmetic safety. No integer overflow or underflow, including in length/offset calculations — the classic place where a hand-written parser goes wrong.
• Termination and panic freedom. Parsing and serializing terminate and never panic, on any input.

Correctness and security

These are the properties that prevent format confusion and malleability. Most, but not every format can satisfy all of them, and Vest is explicit about which properties hold for which formats.

• Parser soundness. If parsing succeeds, the result is a valid instance of the format, and the number of bytes consumed is exactly the formally specified wire length of that instance.
• Parser completeness. Every valid instance of the format can be successfully parsed from its byte representation.
• Parser non-malleability. Each value has a unique byte representation accepted by the parser. Modifying or truncating an accepted input changes the outcome — it fails, or yields a different value.
• Parser non-extensibility. Appending bytes to an accepted input does not change what was already parsed.
• Parser productivity. A successful parse consumes at least one byte, making “progress” on the input.
• Serializer non-ambiguity. Two distinct valid values never serialize to the same bytes.
• Round trips. Together, for unambiguous, non-malleable formats, parsing and serializing are mutual inverses: parse-then-serialize reproduces the consumed bytes, and serialize-then-parse recovers the value.

When a format cannot be non-malleable

While non-malleability is the gold standard in cryptographic systems, it violates Postel’s law: be conservative in what you do; be liberal in what you accept. Many foundational security standards explicitly rely on malleability for backwards-compatibility, extensibility, and interoperability. Concise Binary Object Representation (CBOR) permits multiple valid encodings and separately defines deterministic serialization as required; Cryptographic Message Syntax (CMS) permits the malleable Basic Encoding Rules (BER) for many structures and requires Distinguished Encoding Rules (DER) only at particular authenticated boundaries; and Internet Key Exchange (IKE) allows flexible ordering of payloads and defines explicit rules for ignoring payloads to preserve forward compatibility.

In Vest, malleable formats are explicitly marked (those that do not carry the NonMalleable proof trait or only carry it conditionally), so you cannot accidentally rely on uniqueness that is not there. The practical consequence is that if your application needs byte-faithful round trips (e.g., verifying a signature over the bytes you parsed), add NonMalleable as a requirement (trait bound) to your format.

The DSL currently only accepts and produces non-malleable formats, and we are working on bringing malleable features into the DSL securely.

Vest’s Trusted Computing Base (TCB)

The guarantees above rely on the correctness of the following components:

• rustc, the Rust compiler;
• Verus and the Z3 solver;
• vstd, Verus’s trusted standard-library specification;
• top-level theorem statements in vest_lib.

Vest also says nothing about whether your format is the right format. That it parses/serializes safely and securely does not mean it matches the RFC you are reading. For now, we recommend testing your format against real-world corpora. In the future, we hope to provide an automated testing framework that checks a format against its RFC or other authoritative specification, and flags any discrepancies.

Vest language reference

Overview

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 .vest file).
• The DSL does not support declaring “trusted”/“external” formats that are implemented in Rust/Verus and used in the DSL.

File structure and lexical rules

A .vest file is a sequence of top-level definitions in any order: format definitions, constant definitions, macro definitions, and at most one byte-order (endianness) directive.

Identifiers and reserved words

Identifiers start with a letter or _ and continue with letters, digits, or _. Format names, field names, and enum variants all use this form.

These words are reserved and cannot be used as identifiers:

macro   const   enum   choose   wrap
Option  Vec     Tail   Nothing  Never
btc_varint      uleb128

Integer type names are also reserved: any u or i followed by digits, so u8, u16, u3, i32 and so on are unavailable as names.

The following identifier forms have extra syntax:

Comments

Only line comments exist:

// this is a comment

There is no block comment syntax (/* ... */).

Byte order

!BIG_ENDIAN

or

!LITTLE_ENDIAN

Note:

• Little-endian is the default. A file with no directive is little-endian.
• The directive is file-global, wherever it appears. Putting !BIG_ENDIAN on the last line still applies it to every definition in the file.

Byte order applies only where it is meaningful: multi-byte integers. It does not affect u8, byte arrays, or an 8-bit bits block.

Integer literals

There are three forms, usable anywhere a constant integer is expected — enum values, constraints, constant fields, array lengths:

Similar to Rust, enum values may carry a type suffix that fixes the underlying representation:

kind = enum { A = 0u16, B = 1u16, }

Constant arrays

Byte-array constants take either a string or a list form, and the list form has a repeat shorthand:

const MAGIC: [u8; 4] = "vest"
const ZEROS: [u8; 4] = [0; 4]
const BYTES: [u8; 3] = [0x01, 0x02, 0x03]

Whitespace

Whitespace, including newlines, is insignificant. Fields and enum variants are comma-terminated — including the last one:

msg = {
    a: u8,
    b: u16,     // trailing comma required
}

Vim and Neovim highlighting

The repository includes vest/vest.vim. Copy it to ~/.vim/syntax/vest.vim (or ~/.config/nvim/syntax/vest.vim) and add this to your Vim configuration:

autocmd BufRead,BufNewFile *.vest setfiletype vest

Primitive formats

Primitive formats are the leaves from which larger formats are composed.

Unsigned integers

A fixed-width big- or little-endian integer.

!BIG_ENDIAN

header = {
    kind: u8,
    length: u16,
    sequence: u24,
    timestamp: u32,
    nonce: u64,
}

u8, u16, u24, u32, and u64 are supported. Multi-byte integers follow the file’s byte order. The generated Rust types are the matching unsigned integer types, except that u24 is represented as u32 (with proper value constraints specified in Verus).

Parsing. Reads exactly the declared number of bytes and interprets them in the specified byte order. Fewer bytes remaining than the width is a parse error.

Preparation and serialization. Preparation always succeeds and reports the fixed width. Serialization writes that many bytes in the same byte order.

Signed counterparts are supported in the vest_lib backend, but not yet exposed in the DSL (currently rejected during type checking, but we plan to support them soon). Widths other than the five listed above are rejected too. See bitfields for ways to specify bit-sized integers inside a bits block.

Variable-width integers

btc_varint is Bitcoin’s CompactSize unsigned integer and maps to u64 in Rust. The encoding is one byte for small values and a tagged 3-, 5-, or 9-byte form otherwise, so its width depends on the value.

input = {
    flags: u8,
}

transaction_prefix = {
    @input_count: btc_varint, // 1, 3, 5, or 9 bytes
    inputs: [input; @input_count],
}

Parsing. Reads the leading tag byte, then the remaining bytes according to the tag. Interprets the result as a u64. Only the shortest encoding of a value is accepted — a value padded into a wider form is rejected, which is what keeps the format non-malleable.

Preparation and serialization. Preparation reports the width of the shortest encoding for that value. Serialization writes exactly that form.

The vest_lib backend also supports other variable-length integers such as uleb128, base128 (VLQ), and base256. We plan to expose them in the DSL soon.

Bytes and arrays

[u8; length] is a run of raw bytes of a known length, mapping to a Rust byte slice (&[u8]) to avoid unnecessary copying.

digest = [u8; 32]

Parsing. Takes exactly length bytes and borrows them from the input.

Preparation and serialization. Preparation checks that the slice is exactly length bytes long and reports that length; a slice of any other size is an error. Serialization copies the bytes through unchanged.

For non-byte elements, [format; count] is a repeated format, and a constant count produces a Rust array:

words = [u16; 8]

Lengths and counts may also use runtime dependencies and arithmetic; see Structures and dependencies, and Collections for the repetition semantics.

Tail, Nothing, and Never

payload = {
    header: u16,
    rest: Tail,
}

empty = Nothing
reject = Never("this branch is reserved")

Tail can be used to “under-specify” a format, leaving the rest of the input uninterpreted. Nothing can be used as the “do-nothing” branch of a choice; Never marks a branch that must never be taken, and gives the resulting parse error a message you choose. See Choices.

Refinements

A refinement narrows an existing format to a subset of its values. The wire encoding and the Rust type are unchanged, only the set of accepted values shrinks.

Parsing. Parses the underlying format, then tests the predicate. A value outside the refinement is a parse error.

Preparation and serialization. Preparation tests the same predicate on the value and fails if it does not hold. Length and serialization are those of the underlying format.

The predicate is therefore enforced in both directions.

Integer constraints

constrained = {
    exact: u8 | 7,
    range: u16 | 1..1024,
    lower_bounded: u32 | 1..,
    upper_bounded: u16 | ..4096,
    selected: u8 | {1, 4, 9},
    except: u8 | !{0, 255},
}

Vest ranges include both supplied endpoints: 1..1024 accepts 1 through 1024. Either endpoint may be omitted. A set uses braces and commas; prefixing a constraint with ! takes its complement. Values and range endpoints must fit the underlying integer type.

Enum constraints

Named enum formats can be restricted by variant:

kind = enum {
    Request = 1,
    Response = 2,
    Error = 3,
}

messages = {
    request: kind | Request,
    not_error: kind | !Error,
    terminal: kind | {Response, Error},
}

Every named variant must belong to the referenced enum. The generated field still has type Kind; the refinement changes only which values are consistent with the format.

Structures and dependencies

A struct is a fixed sequence of fields laid out back to back on the wire (without padding). The DSL generates a Rust struct with the same field names, in the same order (though Rust may add padding for alignment or reorder fields for better layout).

record = {
    kind: u8,
    flags: u16,
    payload: [u8; 8],
}

Every field is followed by a comma, including the last one.

Parsing. Parses each field in definition order. The bytes consumed are the sum of the fields’ wire lengths. The parsed value is Record { kind, flags, payload }.

Preparation and serialization. Preparation prepares each field, adds up the lengths with an overflow check, and fails if any field fails. Serialization writes the fields in the same order, back to back.

Dependency fields

Prefix a field name with @ to let later fields refer to its value:

packet = {
    @length: u16,
    payload: [u8; @length],
}

The generated value is Packet { length, payload }. The @ field is present on the wire and in the Rust value.

Parsing. @length is parsed like any other field; its value is then in scope, so [u8; @length] knows how many bytes to take.

Preparation and serialization. The direction reverses: @length is now a consistency requirement. Preparation checks that the payload really is length bytes and fails otherwise. Serialization then writes both fields normally.

A dependency may refer only to a preceding field or a format parameter. Dotted field access is supported for nested structs:

header = {
    kind: u8,
    payload_length: u32,
}

framed = {
    @header: header,
    body: [u8; @header.payload_length],
}

Constant fields

A field whose value is fixed by the format — a magic number or version byte:

message = {
    const version: u8 = 1,
    const magic: [u8; 4] = "vest",
    body: Tail,
}

Parsing. Reads the field and requires it to equal the declared constant; anything else is a parse error.

Preparation and serialization. Constant fields are still present in the generated struct, so preparation rejects a caller value whose field differs, and serialization writes the declared bytes. Use wrap when framing constants should be absent from the value type entirely.

Top-level constants can name byte, integer, or enum constants for reuse:

const MAGIC: [u8; 4] = "vest"

message = {
    const magic: MAGIC,
    body: Tail,
}

Length expressions

Array and byte-string lengths support integer literals, dependencies, static format sizes, parentheses, and arithmetic:

header = {
    @total: u16 | 8..,
    flags: u8,
}

body(@header: header) = {
    payload: [u8; @header.total - |header|],
}

|format| is the static serialized size of a fixed-width named or primitive format. It is rejected for dynamically sized or parameter-dependent formats.

Parsing and preparation. The expression is evaluated the same way in both directions — to decide how many bytes to read, and to check how many bytes a value must occupy. The arithmetic is checked for overflow and underflow in the executable code (statically by Verus for parsing, and at runtime for preparation).

Enums

An enum is an integer on the wire with a name for each meaningful value. It corresponds to a Rust enum with the same discriminants. The generated Rust type is #[repr(uN)] where N is the backing width.

Closed enums

message_type = enum {
    Request = 1,
    Response = 2,
    Error = 3,
}

This emits a MessageType Rust enum. Values must be distinct and fit the inferred backing width.

Parsing. Reads the backing integer and maps it to a variant. Any other value is a parse error.

Preparation and serialization. Preparation always succeeds and reports the backing width. Serialization writes the variant’s discriminant as the backing integer.

Open enums

Add ... after the variants to preserve unknown values:

message_type = enum {
    Request = 1,
    Response = 2,
    ...
}

Parsing. A recognised value maps to its variant, and anything else is kept as Unknown(value).

Preparation and serialization. Same width as the closed form. Known variants serialize as before; Unknown(value) serializes as value.

Choosing the backing width

The backing width is what actually determines how many bytes appear on the wire. Without a suffix, Vest selects the smallest unsigned width containing every value. A suffix on any enumerator fixes the type; all supplied suffixes must agree:

wide_type = enum {
    Request = 1u16,
    Response = 2,
}

The supported executable backing widths are u8, u16, u24, u32, and u64.

Inside a bits block, a suffix such as 0u3 instead selects a three-bit enum. See Bit fields.

Choices

A choice is a format that can take one of several shapes. It generates a Rust enum, so the alternative that matched is recorded in the value. Vest has dependent choices, where an earlier field selects the branch, and non-dependent choices, where branches are tried in order.

Enum-dependent choices

kind = enum {
    Short = 1,
    Long = 2,
}

body(@kind: kind) = choose(@kind) {
    Short => u16,
    Long => u64,
}

Parsing. The dependency has already been parsed, so the branch is chosen directly — no backtracking, and no ambiguity about which arm applies.

Preparation and serialization. Preparation checks that the variant in your value matches the branch the dependency selects; a Long body under a Short tag is rejected before any bytes are written. It then prepares that branch. Serialization writes the selected branch only.

A closed enum choice must cover every declared variant unless it has a final wildcard. An open enum choice requires a final _ branch. Branch names must be unique and belong to the enum.

Integer-dependent choices

body(@kind: u8) = choose(@kind) {
    1 => u16,
    2..10 => u32,
    _ => Never("unknown body kind"),
}

Integer patterns use the same values and ranges as refinements. Explicit patterns must not overlap, and a final wildcard is mandatory because the integer domain is otherwise open. Semantics are as above: the dependency picks the arm, and the value must match that arm.

Byte-string-dependent choices

record = {
    @magic: [u8; 2],
    body: choose(@magic) {
        [0x01, 0x02] => u16,
        [0x03, 0x04] => u32,
        _ => Nothing,
    },
}

Every explicit byte pattern must have the same length as the dependency, and a final wildcard is required.

Non-dependent ordered choices

Without (@dependency), there is no tag to dispatch on, so the branches are distinguished by their own content:

small = choose {
    Tiny(u8 | 0..9),
    Medium(u8 | 10..100),
}

// or equivalently
small_arrow = choose {
    Tiny => u8 | 0..9,
    Medium => u8 | 10..100,
}

Parsing. Branches are attempted in source order and the first success wins. A failed attempt consumes nothing, so the next branch starts from the same position.

Preparation and serialization. Preparation checks whichever branch the value holds; serialization writes it.

Note that for non-dependent choices, the variant names (Tiny and Medium) are not part of the wire. In this case, Vest requires that the branches are non-overlapping, which is required for the parser to be able to unambiguously select the correct branch.

Wildcard rules

• _ may appear at most once and must be the final branch.
• Integer and byte-string choices require it.
• Open-enum choices require it.
• A closed-enum choice is normally written exhaustively, but a final _ is allowed to “catch all” other variants.

Collections

Fixed and dependency-sized arrays

A repetition of one format a known number of times.

fixed_words = [u16; 8]

counted = {
    @count: u16,
    words: [u32; @count],
}

A constant count generates a Rust array. A dependency-sized repetition generates a Vec, because its length is known only at runtime. [u8; length] is specialized to a borrowed byte slice.

Parsing. Parses the element format exactly count times, one after another.

Preparation and serialization. Preparation checks that the collection holds exactly count elements, prepares each element, and sums the lengths. Serialization writes the elements back to back.

Nested arrays are supported:

matrix = {
    @rows: u16,
    @columns: u16,
    cells: [[u8; @columns]; @rows],
}

Vec

A repetition with no count: zero or more occurrences of a format. The result is a Vec in Rust.

item = { value: u16, }

items = Vec<item>

Parsing. Repeats the element format until it errors (e.g., the input is exhausted).

Preparation and serialization. Preparation prepares every element and sums the lengths. Serialization writes the elements in order.

Because there is no count, the element must be productive — every successful element parse must consume at least one byte. Otherwise repetition could loop forever. Verus will check this property in the emitted Rust code and reject the format if productivity cannot be proven for the element format.

Option

Zero or one occurrence of a format.

tagged = wrap(u8 = 1, u16)
maybe_tagged = Option<tagged>

Parsing. Tries the inner format. On success the result is Some(v); on failure the result is None and no input is consumed, so parsing continues from the same position.

Preparation and serialization. Some(v) prepares and writes the inner format; None has length 0 and writes nothing.

Notes on Vec and Option

Because a Vec can be empty and an Option can be absent, the surrounding format must make their presence distinguishable from what follows — a tagged or otherwise disjoint inner format is the usual pattern. A chain of ambiguous Vec or Option fields will fail the generated unambiguity proof obligations.

>>=

left >>= right means “take the region left describes, then parse right against it.”

The corresponding Rust value type of the whole expression is the same as right’s.

Parsing. Extract a bounded region from the input defined by left, then parse right from that region. right must consume the region entirely — leftover bytes are an error.

Preparation and serialization. Preparation prepares right and requires its length to equal the region left declares. Serialization writes right’s bytes directly.

Currently, the left side must be [u8; length] or Tail. We’re working on generalizing this to any format that can be reinterpreted within a bounded region.

Bounding Vec with a length field

item = { value: u16, }

list = {
    @byte_length: u16,
    values: [u8; @byte_length] >>= Vec<item>,
}

Here, Vec<item> repeats until its region ([u8; @byte_length]) runs out. Because the region is exactly byte_length bytes, the repetition will eventually stop. Preparation checks that the items really do add up to byte_length.

Reinterpreting the remainder of a region

Tail names everything left in the enclosing region, which turns >>= into “reinterpret the remainder”:

item = { value: u16, }

items = Tail >>= Vec<item>

This is the idiom for a message that ends in an unknown number of records. It also composes: inside a format already bounded by a length field, Tail means the rest of that region, not the rest of the original input buffer.

Bit fields

bits { ... } describes several small unsigned fields packed into one fixed-width integer on the wire. The block as a whole is a single integer; the fields are slices of its bits. The DSL compiler exposes them as ordinary integer-typed Rust fields.

ipv4_first_byte = bits {
    version: u4,
    ihl: u4,
}

Fields are laid out from the most significant bit of the integer, in declaration order. The total width must be exactly 8, 16, 24, 32, or 64 bits; otherwise the compiler reports an invalid total width. Each individual width must be positive and no larger than 64.

Parsing. Reads the integer according to the specified byte order, then splits it into fields from the most significant bit down, and checks each field’s constraint.

Preparation and serialization. Preparation checks that each field fits its declared bit width and satisfies its constraint, and reports the integer’s width. Serialization packs the fields back into one integer and writes it in the specified byte order.

Cross-byte fields and byte order

!BIG_ENDIAN

packed = bits {
    prefix: u3,
    value: u10,
    suffix: u3,
}

Fields may straddle byte boundaries; only the integer as a whole is required to be byte aligned. Byte endianness controls how that multi-byte integer is decoded/encoded. It has no effect on abstract ordering of the fields, which is always from the most significant bit down. For example, the packed format above specifies a 16-bit integer with three bit fields.

| prefix (3 bits) |      value (10 bits)      | suffix (3 bits) |

In big-endian order, the first byte is the most significant, so the fields are encoded as follows:

|b00|b01|b02|b03|b04|b05|b06|b07|b08|b09|b10|b11|b12|b13|b14|b15|
 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
|   prefix  |                 value                 |   suffix  |

In little-endian order, the first byte is the least significant, so the fields are encoded as follows:

|b00|b01|b02|b03|b04|b05|b06|b07|b08|b09|b10|b11|b12|b13|b14|b15|
 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
|    value (low 5)  |  suffix   |   prefix  |   value (high 5)  |

Constraints and enums

Bit-sized integers use the ordinary refinement syntax, with the same two-way enforcement described in Refinements. Enum suffixes may select an exact bit width:

payload_kind = enum {
    Raw = 0u3,
    Words = 1u3,
    ...
}

header = bits {
    @kind: payload_kind,
    @count: u5 | 1..31,
    @length: u8,
}

packet = {
    @header: header,
    body: choose(@header.kind) {
        Raw => [u8; @header.length],
        Words => [u16; @header.count],
        _ => [u8; @header.length],
    },
}

Only unsigned integers and enums with unsigned bit-sized integer types are allowed as bit fields. Dependency fields and dotted access work exactly as in ordinary structures: @kind is unpacked while parsing the integer and is then in scope for later fields, and preparation enforces it as a constraint in the other direction.

Composition

Format aliases

A definition may directly reuse another format:

header = { kind: u8, length: u16, }
header_alias = header

The alias receives its own generated format name while using the referenced value type. Parsing, preparation, and serialization are those of the referenced format; the alias adds no wire bytes.

Framing with wrap

wrap surrounds a format with fixed bytes that carry no semantic information (e.g., a magic prefix, a terminator, or padding) and keeps them out of the value.

framed_word = wrap(
    u8 = 0xAA,
    u16,
    [u8; 2] = [0x0D, 0x0A]
)

The generated value type for framed_word is just u16.

Parsing. Recognizes the prefix constants, parses the inner format, then recognizes the suffix constants. A constant that does not match is a parse error. The framing bytes are consumed but discarded.

Preparation and serialization. Preparation reports the inner length plus the widths of all the constants. Serialization writes the prefix, the inner value, and the suffix.

This is the difference from a const structure field, which stays part of the generated struct and must be supplied by the caller during preparation and serialization.

wrap accepts any number of constant integer, byte-string, or enum formats before and after its one non-constant inner format.

Parameterized formats

payload(@length: u16) = [u8; @length]

packet = {
    @length: u16,
    body: payload(@length),
}

Parameters are values supplied by the enclosing format. They are not part of the generated value type.

Parsing and preparation. A parameter contributes no bytes of its own. It behaves exactly like a dependency but is required to be bound externally in the enclosing format.

When invoked, arguments must be @ dependencies in scope and must match the declared parameter format.

Macros

Macros substitute format arguments before type checking:

macro length_prefixed!(length_format, body_format) = {
    @length: length_format,
    body: [u8; @length] >>= body_format,
}

words = length_prefixed!(u16, Vec<u32>)

Macro arguments are format expressions. Macros are purely syntactic and have no semantics of their own. The expansion behaves exactly as if you had written it out.

Recursion

Named formats may refer to themselves directly or through other definitions:

list_kind = enum {
    Nil = 0,
    Cons = 1,
}

list = {
    @kind: list_kind,
    value: choose(@kind) {
        Nil => Nothing,
        Cons => {
            head: u8,
            tail: list,
        },
    },
}

The compiler finds strongly connected components (SCCs), so mutually recursive definitions are supported too. It emits owned Box links where Rust needs indirection in the value type.

Parsing. Recurses as the input demands, up to a fixed depth bound statically picked by the format. Exceeding the bound is a parse error.

Preparation and serialization. Preparation walks the value to the same bound, summing lengths, and fails if the value nests deeper than the format allows. Serialization traverses the value and writes the bytes in order.

Note

Though vest_lib defines a bounded fixpoint format combinator that can express arbitrary recursion, the compilation of recursive formats in Vest DSL is experimental: the implementation is incomplete and there is some engineering work remaining for a more robust support.

Construct-to-Rust mapping

A quick-lookup table from DSL construct to the Rust type it generates.

Names are converted to UpperCamelCase: msg_type becomes MsgType. Alongside each value type, the compiler emits a zero-sized format type — MsgTypeFmt — that carries the parser, serializer, and proofs. See Generated Rust Code for the full set of emitted names.

Generated Rust Code

Vest emits one user-facing value type and one format type for each named DSL definition. It also emits specification, proof, and executable helpers/trait implementations. The helpers are public to ease the codegen plumbing, but application code normally needs only the value and format types.

For this definition:

message = {
    @length: u16,
    payload: [u8; @length],
}

the user-facing types are:

#[derive(Debug, PartialEq, Eq, Clone, Copy)]
pub struct Message<'i> {
    pub length: u16,
    pub payload: &'i [u8],
}

pub struct MessageFmt;

The shape of an emitted file

The whole module is a single verus! block behind a fixed use preamble, cut into five banner-delimited sections:

use vest_lib::combinators::*;            // fixed preamble, identical in every file
use vest_lib::core::exec::parser::*;
// ...
verus! {

// ============================================================
// Data Types
// ============================================================
// ============================================================
// Format Specifications
// ============================================================
// ============================================================
// Derived Parser, Serializer, Length, and Consistency Specifications
// ============================================================
// ============================================================
// Proven Format Properties
// ============================================================
// ============================================================
// Executable Implementations
// ============================================================

} // verus!

A file with nine definitions emits all nine value types, then all nine nominal format types, then all the derived specifications, and so on. Because the nominal format types (e.g., MessageFmt) are what the user actually interacts with, the last three sections are wrapped in private modules (derived_specs, derived_proofs, exec_impls).

Data Types

Per definition, alongside the Message shown above, Vest emits a nominal abstract value type (MessageSpec) and a structural representation (MessageInner), plus the DeepView impl that converts between the executable value and the abstract value. Additionally, Vest emits two empty structs (MessageForward and MessageReverse) to name the bijective conversion between the structural and nominal abstract value types.

#[verifier::ext_equal]
pub struct MessageSpec<T0 = u16, T1 = Seq<u8>> {   // abstract view of Message
    pub length: T0,
    pub payload: T1,
}

pub type MessageInner = (u16, Seq<u8>);           // what the combinator tree yields

impl<'i> DeepView for Message<'i> {               // exec value -> abstract value
    type V = MessageSpec;
    #[verifier::opaque]
    open spec fn deep_view(&self) -> Self::V { /* field-wise */ }
}

impl<T0, T1> MessageSpec<T0, T1> {                // abstract value <-> nested tuple
    #[verifier::opaque] pub open spec fn from_structural(input: (T0, T1)) -> Self { /* .. */ }
    #[verifier::opaque] pub open spec fn into_structural(self) -> (T0, T1) { /* .. */ }
    pub proof fn lemma_from_into(self) { /* .. */ }
    pub proof fn lemma_into_from(input: (T0, T1)) { /* .. */ }
}

// The bijection between the structural tuple and the nominal abstract value
#[doc(hidden)] pub struct MessageForward;
#[doc(hidden)] pub struct MessageReverse;

For a choose, the same set appears with enum instead of struct, and MessageInner becomes nested Sums rather than a nested tuple.

Format Specifications

This section is the format combinator representation (defined in vest_lib) of the DSL definition.

pub type MessageFmtSpec =
    Named<Mapped<Bind<U16Le, spec_fn(u16) -> Varied<u16>>, BiMap<MessageForward, MessageReverse>>>;

impl MessageFmt {
    pub open spec fn spec_inner() -> MessageFmtSpec {
        Named("message", Mapped {
            inner: Bind(U16Le, |length: u16| Varied(length)),
            mapper: BiMap(MessageForward, MessageReverse),
        })
    }
}

Note how each DSL construct has a corresponding shape in the combinator representation (@length: u16 becomes Bind(U16Le, |length: u16| ...), [u8; @length] becomes Varied(length), etc.). The Named wrapper is what gives the format a human-readable name for error reporting.

Derived Specifications

Because spec_inner() is a combinator tree composed of vest_lib format combinators, we can derive the formal specifications of the format from it.

impl SpecParser        for MessageFmt { type PVal   = MessageSpec; /* spec_parse */ }
impl Consistency       for MessageFmt { type Val    = MessageSpec; /* consistent */ }
impl SpecSerializer    for MessageFmt { type SVal   = MessageSpec; /* spec_serialize */ }
impl SpecByteLen       for MessageFmt { type T      = MessageSpec; /* byte_len */ }

Every method body is literally Self::spec_inner().<method name>(..). Most of them are marked #[verifier::opaque] so enclosing formats cannot see their inner definitions. This opacity is what keeps verification cost from exploding as formats grow in size and complexity.

Proven Format Properties

Likewise, the proofs of format properties are mostly derived from spec_inner().

broadcast use {
    vest_lib::combinators::disjoint::disjointness_lemmas,
    MessageSpec::lemma_from_into,
    MessageSpec::lemma_into_from,
};

impl SafeParser  for MessageFmt { /* .. */ }
impl Productive  for MessageFmt { /* .. */ }
impl SoundParser for MessageFmt { /* .. */ }
impl SPRoundTrip for MessageFmt { /* .. */ }
impl NonMalleable for MessageFmt { /* .. */ }
// ...plus more auxiliary proof traits, depending on the format

Each proof reveals the opaque specifications it needs, then hands off to the corresponding lemma on spec_inner(). disjointness_lemmas is a broadcast group of lemmas that compositionally establish the non-ambiguity of certain format combinators, which is a prerequisite for serialize-then-parse round trips.

Executable Implementations

Finally, the executable implementations of Parser, Serializer, and Prepare are emitted. Here, the implementations are not derived from spec_inner(); they are written in idiomatic imperative Rust to ensure performance and avoid unnecessary combinator overhead.

impl<'i> Parser<&'i [u8]> for MessageFmt {
    type PT = Message<'i>;
    fn parse(&self, ibuf: &&'i [u8]) -> PResult<Self::PT> { /* .. */ }
}

impl<Output: OutputBuf, 'i> Serializer<Output, Message<'i>> for MessageFmt {
    fn serialize_into(&self, v: &Message<'i>, obuf: &mut Output) { /* .. */ }
}

impl<'i> Prepare<Message<'i>> for MessageFmt {
    fn prepare(&self, v: &Message<'i>) -> Result<usize, PreSerializeError> { /* .. */ }
}

parse walks the fields, advancing a cursor and propagating failure with ?, then assembles the value and asserts it matches spec_parse:

let (n1, length)  = U16Le.parse(&rest)?;
let rest          = rest.skip(n1);
let (n2, payload) = Varied(length).parse(&rest)?;
// ...
Ok((n1 + n2, Message { length, payload }))

serialize_into mirrors it — it traverses the value and writes each field directly in-place to the outbuf buffer. prepare similarly walks the value, checking that each field is valid and summing the lengths.

Calling it

use vest_lib::core::exec::{Parser, Prepare, SerializerExt};

let input: &[u8] = &[3, 0, b'a', b'b', b'c'];
let (consumed, message) = MessageFmt.parse(&input).unwrap();
assert_eq!(consumed, 5);
assert_eq!(message.payload, b"abc");

let length = MessageFmt.prepare(&message).unwrap();
let mut output = vec![0u8; length];
MessageFmt.serialize(&message, &mut output);

parse returns the consumed prefix length and the value; it need not consume the whole input unless the format says so. Errors carry a ParseErrorKind along with the static identifier provided to the Name combinator. When the alloc feature is enabled, the error also builds a trace of the enclosing formats, which is useful for debugging.

The SerializerExt trait provides two convenience methods for serializing values into a buffer: serialize and serialize_with_vec. serialize writes into an exactly sized slice and serialize_with_vec appends to a growable Vec<u8>. In both cases, the length of the buffer can be obtained from prepare to provably avoid (re)allocation.

Command-line interface

Synopsis

vest [OPTIONS] <VEST_FILE>

A successful run should print the following five stages and exit zero:

$ vest msg.vest -o src/msg.rs
📜 Parsing the vest file...
🔨 Elaborating the AST...
🔍 Type checking...
📝 Generating the verus file...
👏 Done!

Generating from build.rs

For a project that keeps its .vest schema under version control and regenerates the Rust code on change, we recommend a build.rs that calls the compiler. Add vest as a build dependency and use one of three entry points:

// build.rs
use std::error::Error;
use vest::compile_to;

fn main() -> Result<(), Box<dyn Error>> {
    println!("cargo::rerun-if-changed=src/msg.vest");
    compile_to("src/msg.vest", "src/msg.rs")?;
    Ok(())
}

All three report diagnostics to stderr and return Err on failure.

Troubleshooting

TODO. This page is not written yet.

It will cover the Vest DSL compiler, Verus verification, and runtime errors you are most likely to hit.

Using vest_lib

TODO. This page is not written yet.

Most applications should use the Vest DSL or the ASN.1 frontend, which generate parsers and serializers for you, composed with format combinators in vest_lib. This page will cover the case where you prefer writing them by hand: when a format is too complex to express in the DSL.

Until then, the combinators module documentation lists every primitive and higher-order format with its semantics and vest_dev/src/formats holds some handwritten examples that demonstrate how to use them.

Feature configurations

vest_lib has three supported configurations:

[dependencies]
vest_lib = { version = "0.2", default-features = false, features = ["alloc"] }

Vest and vest_lib must be used with the Verus and vstd versions this release pins. The Verus version is in verus.json and the vstd version is in the workspace Cargo.toml.

ASN.1 Compiler

vest_asn1 parses an ASN.1 module and emits verified formats backed by vest_lib::asn1. DER is the default; BER and definition-level rule overrides are available.

cargo run -p vest_asn1 -- schema.asn1 -o generated.rs
cargo run -p vest_asn1 -- --rules ber schema.asn1 -o generated_ber.rs

Similar to the Vest DSL, each supported ASN.1 definition becomes a user-facing Rust value type and a nominal format type whose specification, proof, and executable implementation are all derived from the inner combinator representation.

Start with the ASN.1 tutorial, then see the generated Rust code and the support table. The backend API is documented under vest_lib::asn1.

DER, BER, and rule overrides

--rules der or --rules ber authoritatively selects the module default. A definition override changes that definition and the transitive children it needs under the selected rule; parents remain under the module default.

cargo run -p vest_asn1 -- --rules ber \
  --der-definition SignedAttributes \
  --der-definition CertificateSet \
  schema.asn1 -o generated_mixed.rs

Every ASN.1 definition is emitted exactly once with one global rule. A BER definition may contain a DER child because a DER encoding is valid BER. However, a DER definition cannot depend on a BER definition without violating DER canonicality. Conflicting transitive overrides are rejected and require an explicit rule boundary.

ASN.1 tutorial

This walkthrough generates a small DER codec from an ASN.1 module and uses it to parse and serialize a message.

Define a module

Create message.asn1:

Message DEFINITIONS EXPLICIT TAGS ::= BEGIN
    Kind ::= ENUMERATED {
        request(0),
        response(1)
    }

    Packet ::= SEQUENCE {
        kind Kind,
        payload [0] IMPLICIT OCTET STRING (SIZE (1..32)) OPTIONAL
    }
END

Generate DER

vest_asn1 is currently a repository tool rather than a published crate:

cargo run -p vest_asn1 -- message.asn1 -o src/message.rs

DER is the default. Use --rules ber for BER, or definition overrides for a module with canonical DER substructures inside a BER envelope; see DER, BER, and rule overrides.

The generator emits Kind and Packet<'i> value types. Unlike the Vest DSL, their verified format values are KIND::Fmt and PACKET::Fmt (due to technical reasons mandated by the ASN.1 standard). Uppercase format names avoid collisions with the idiomatic Rust value names.

Parse and serialize

use vest_lib::core::exec::{Parser, Prepare, SerializerExt};
use crate::message::{Kind, PACKET};

let encoded: &[u8] = &[
    0x30, 0x07,             // SEQUENCE, seven content octets
    0x0a, 0x01, 0x00,       // Kind::Request
    0x80, 0x02, 0xaa, 0xbb, // [0] IMPLICIT OCTET STRING
];

let (consumed, packet) = PACKET::Fmt.parse(&encoded).unwrap();
assert_eq!(consumed, encoded.len());
assert_eq!(packet.kind, Kind::Request);
assert_eq!(packet.payload, Some(&[0xaa, 0xbb][..]));

let size = PACKET::Fmt.prepare(&packet).unwrap();
let mut output = vec![0u8; size];
PACKET::Fmt.serialize(&packet, &mut output);
assert_eq!(output, encoded);

DER string fields borrow from the input because their representation is contiguous. BER generated values may be owned when constructed, fragmented strings are concatenated.

What is checked

TODO. Discuss the proof obligations for format non-ambiguity, etc.

Generated Rust Code

An ASN.1 definition such as Packet becomes a Rust value type Packet and a verified nominal format type PACKET, used as PACKET::Fmt. The screaming-case format name avoids colliding with the idiomatic value name.

SEQUENCE and supported heterogeneous SET definitions become structs; CHOICE becomes an enum carrying the alternatives; and ENUMERATED becomes a closed typed enum. Anonymous composites receive deterministic private helper definitions. IMPLICIT tagging replaces the outer tag; untagged CHOICE and ANY have no single tag to replace, so the generator tags those explicitly.

The examples below come from the module in the tutorial:

Kind   ::= ENUMERATED { request(0), response(1) }
Packet ::= SEQUENCE {
    kind    Kind,
    payload [0] IMPLICIT OCTET STRING (SIZE (1..32)) OPTIONAL
}

The shape of an emitted file

Unlike a DSL-generated module, an ASN.1 module has no banner sections. It is one flat verus! block holding every definition’s types and schema, followed by one small private module per definition outside the block:

use vest_lib::asn1::der::{...};          // preamble selected by the encoding rules
verus! {

    // per definition: value type, abstract type, predicates, mappers,
    // combinator representations, and the nominal format type

} // verus!

mod __impl_kind   { use super::*; vest_lib::impl_der!(...); }
mod __impl_packet { use super::*; vest_lib::impl_der!(...); }

That last part is the biggest structural difference. Where the DSL writes out derived_specs, derived_proofs, and exec_impls explicitly, the ASN.1 backend emits one macro call per definition and lets vest_lib expand the specifications, proofs, and executable code.

Value and abstract types

This matches the DSL closely — a value type and a generic abstract type, bridged by DeepView:

pub struct Packet<'a> {
    pub kind: Kind,
    pub payload: Option<&'a [u8]>,
}

#[verifier::ext_equal]
pub struct PacketSpec<T0 = KindSpec, T1 = Option<Seq<u8>>> {
    pub kind: T0,
    pub payload: T1,
}

impl<'a> DeepView for Packet<'a> {
    type V = PacketSpec;
    #[verifier::opaque]
    open spec fn deep_view(&self) -> Self::V { /* field-wise */ }
}

For a definition whose value type is already Copy and structural — an ENUMERATED, for instance — there is no separate abstract type at all.

#[repr(i16)]
#[derive(Debug, Clone, Copy, PartialEq, Eq, StructuralEq)]
pub enum Kind { Request = 0, Response = 1 }

pub type KindSpec = Kind; // the abstract type is the same as the value type

impl DeepView for Kind { type V = Self; /* *self */ }

Predicates and mappers

ASN.1 constraints become named predicate structs used in both the specification and implementation, rather than the inline closures the DSL emits:

#[derive(Clone, Copy)]
pub struct KindPredicate;

impl SpecPred<i16> for KindPredicate { /* value == 0 || value == 1 */ }
impl Pred<i16>     for KindPredicate { /* the executable test */ }

ENUMERATED values are built on the verified i16 integer-content backend, which is why the predicate is over i16. Larger enumerations are currently not yet supported.

Mappers follow the DSL’s Forward/Reverse pattern, with one addition — they implement the executable Map as well as SpecMap.

pub struct KindForward;
pub struct KindReverse;

impl SpecMap for KindForward { /* .. */ }
impl SpecMap for KindReverse { /* .. */ }
impl Map<i16> for KindForward { /* executable */ }
impl Map<Kind> for KindReverse { /* executable */ }

The nominal format type

/// DER format for ASN.1 `Kind`.
type KIND__ = Mapped<Refined<Enumerated16TlvFmt, KindPredicate>, BiMap<KindForward, KindReverse>>;

#[derive(Clone, Copy)]
#[verifier::ext_equal]
pub struct KIND(pub Class, pub u64); // tag class, tag number

impl KIND {
    pub const Fmt: Self = Self(Class::Universal, 10u64);

    #[verifier::allow_in_spec]
    pub const fn schema() -> KIND__
        returns (Mapped { inner: Refined(ENUMERATED16, KindPredicate),
                          mapper: BiMap(KindForward, KindReverse) }),
    { /* the same representation */ }

    proof fn lemma_schema_unambiguous(&self) { /* .. */ }
}

Several things differ from the DSL here.

The format type is always parametric. MessageFmt in a DSL module is a zero-sized struct. KIND is a tuple struct holding the effective tag class and number, so an IMPLICIT tag can replace the outer tag without rebuilding the format. KIND::Fmt is the associated constant carrying the definition’s own tag — Class::Universal, 10 for ENUMERATED, 16 for SEQUENCE, etc.

schema() is dual spec-exec. The DSL’s spec_inner() is pub open spec fn — specification only. schema() here is a const fn marked #[verifier::allow_in_spec] with a returns clause, so the same definition serves both worlds (there are valid reasons for the DSL to separate them, such as to allow for more flexible executable implementations).

lemma_schema_unambiguous has no DSL counterpart. It proves the ASN.1 schema unambiguous (needed for serialize-then-parse roundtrip) by leveraging a sound over-approximation of each ASN.1 combinator’s parsing domain. On the other hand, the DSL’s constructs disambiguate themselves largely by construction, so the DSL does not need to emit this lemma.

Specifications, proofs, and executable code

Everything else arrives from one macro invocation, placed outside verus!:

mod __impl_packet {
    use super::*;
    vest_lib::impl_der!(
        tagged_exact(true),   // this definition contributes an outer tag
        borrowed,             // the value type borrows from the input
        PACKET, PACKET__,     // nominal type and its combinator type alias
        PacketSpec, Packet,   // abstract and executable value types
        PacketForward, PacketReverse
    );
}

impl_der! (or impl_ber! under BER) expands to the same code the DSL emits explicitly — derived spec trait impls (SpecParser, SpecSerializer, SpecByteLen, Consistency) and derived proof trait impls (SafeParser, SoundParser, Productive, NonTailFmt, GoodSerializer, NonMalleable, etc.). Additionally, it also expands to the executable trait impls (Parser, Prepare, Serializer).

Calling it

Calling the parser, serializer, and the prepare methods is almost identical in shape to DSL-generated code, except that the format value is the ::Fmt constant:

use vest_lib::core::exec::{Parser, Prepare, SerializerExt};

let (consumed, packet) = PACKET::Fmt.parse(&encoded).unwrap();

let size = PACKET::Fmt.prepare(&packet).unwrap();
let mut output = vec![0u8; size];
PACKET::Fmt.serialize(&packet, &mut output);

Supported ASN.1 and limitations

What vest_asn1 accepts today. Anything listed as not supported is rejected by the compiler with an error.

Primitive types

Constructed types

Tagging

Components and constraints

Module-level

Additional notes

SET OF ordering. DER requires the values to be sorted by their complete DER TLV encoding. The generated prepare rejects an unsorted vector without allocating, so sorting is the caller’s job (the provided comparison abstraction is non-allocating so sorting should be efficient as well). Duplicate encodings are allowed. BER SET OF imposes no canonical order and preserves schema order on output.

Heterogeneous SET. BER lets a SET carry its components in any order, so a BER parser would have to accept every permutation of the fields. DER instead fixes them in ascending tag order. vest_asn1 currently emits SET only under DER, and only when the schema already lists the fields in canonical order. The vest_lib backend supports a group of Permute combinators that can be used to implement BER SET, but the generator does not yet emit them.

Borrowing and alloc. DER strings are contiguous, so their value types borrow from the input. BER strings may arrive fragmented across constructed encodings and are flattened into owned values, which is why BER modules need the alloc feature where the equivalent DER module may not. BMPString and UniversalString are always owned, since their wire form is not UTF-8.

High tag numbers and disjointness. CHOICE, OPTIONAL, and DEFAULT need alternatives/adjacent fields to be provably disjoint. The generated proof covers the 256 possible leading identifier octets: tags 0 through 30 are exact, but all high-tag-number forms sharing a class and constructed bit collapse onto one bit. Two such tags cannot be proven disjoint from their later tag-number octets alone, so a schema that distinguishes alternatives only by high tag numbers is conservatively rejected.

General and deterministic CBOR

TODO. This page is not written yet.

vest_lib::cbor is a verified prototype codec for the RFC 8949 generic data model, covering both general well-formed CBOR and the deterministic profile. This page will cover the value model, the borrowing and allocation behaviour, and which parts of the deterministic profile are enforced today.

Until then, the cbor module documentation describes the formats and their proof interfaces.