Crate vest_lib 

Vest

vest_lib is a formally verified combinator library for parsing and serializing binary data. It is the backend of the Vest framework, which can automatically produce verified parsers and serializers from a high-level format description.

This document primarily serves as a reference for users who want to use the combinator library directly to achieve greater flexibility in the parsing and serialization process. For a more automated workflow, refer to the vest crate and some examples of using Vest DSL.

Formally Verified Parsing and Serialization

Vest leverages the Rust type system and Verus to formally verify the correctness and security of binary parsing and serialization. We exploit Rust’s borrowing, lifetime, and the powerful trait system to achieve high-performance without sacrificing safety, while Verus allows us to specify and prove key round-trip properties about our combinators.

These properties ensure mutual inversion of parsing and serialization, making them immune to parser malleability and format confusion attacks. See more in our USENIX Security ’25 paper.

Available Combinators

Vest provides a small yet expressive set of formally verified combinators for building parsers and serializers. Each combinator’s correctness properties are verified once and can be reused across complex compositions.

Combinator	Purpose
bytes::Fixed	Parse and serialize a fixed number of bytes (compile-time known)
bytes::Variable	Parse and serialize a dynamic number of bytes (runtime known)
U8/U16Le/U32Le/U64Le	Parse and serialize unsigned integers in little-endian format
U16Be/U32Be/U64Be	Parse and serialize unsigned integers in big-endian format
UnsignedLEB128	Parse and serialize unsigned integers using LEB128 variable-length encoding
BtcVarint	Parse and serialize unsigned integers using Bitcoin’s VarInt variable-length encoding
Pair	Sequentially compose two combinators, where the second might depend on the first’s output
Preceded	Sequentially compose two combinators, omitting the first’s output
Terminated	Sequentially compose two combinators, omitting the second’s output
Choice	Try two combinators in order
RepeatN	Repeat a combinator a fixed number of times
Repeat	Repeat a combinator until the end of input buffer
Refined	Refine parsed/serialized values with predicates
Mapped	Transform parsed/serialized values with infallible isomorphisms
TryMap	Transform parsed/serialized values with fallible isomorphisms
Cond	Conditionally apply a combinator based on a predicate
AndThen	Re-interpret bytes with (potentially nested) sub-combinators
Opt	Optionally apply a combinator
Success	Always succeeds and consumes nothing (unit combinator)
Fail	Always fails with a custom error message
End	Succeeds only at the end of input buffer
Tag	Match a specific value (useful for format markers)

Examples

Parsing and serializing a pair of bytes

use vest_lib::regular::bytes::Fixed;
use vest_lib::properties::Combinator;

// Define a combinator for parsing two consecutive fixed-size byte sequences
let pair_of_bytes = (Fixed::<1>, Fixed::<2>);

let input = &[0x10, 0x20, 0x30][..];
let (consumed, (a, b)) = <_ as Combinator<&[u8], Vec<u8>>>::parse(&pair_of_bytes, input)?;

let mut output = vec![0x00; 10];
let written = <_ as Combinator<&[u8], Vec<u8>>>::serialize(&pair_of_bytes, (&a, &b), &mut output, 0)?;

assert_eq!(written, consumed);
assert_eq!(&output[..written], &input[..consumed]);

Refining parsed values with predicates

use vest_lib::regular::uints::U8;
use vest_lib::regular::modifier::{Refined, Pred, SpecPred};
use vest_lib::properties::Combinator;
use vstd::prelude::*;

verus! {
    pub struct EvenU8;
    impl View for EvenU8 {
        type V = Self;
        open spec fn view(&self) -> Self::V { *self }
    }

    impl SpecPred<u8> for EvenU8 {
        open spec fn spec_apply(&self, i: &u8) -> bool {
            *i % 2 == 0
        }
    }

    impl Pred<u8> for EvenU8 {
        fn apply(&self, i: &u8) -> bool {
            *i % 2 == 0
        }
    }
}

// Create a refined combinator that only accepts even numbers
let even_u8 = Refined { inner: U8, predicate: EvenU8 };

// Serialize an even number
let mut output = vec![0x00; 10];
let written = <_ as Combinator<&[u8], Vec<u8>>>::serialize(&even_u8, &10u8, &mut output, 0)?;

// Parse it back - this succeeds because 10 is even
let (consumed, parsed) = <_ as Combinator<&[u8], Vec<u8>>>::parse(&even_u8, &output[..written])?;
assert_eq!(parsed, 10);

Modules

bitcoin

Combinators for Bitcoin formats.

buf_traits

Definitions for buffer traits that can be used as input and output for parsers and serializers, along with some implementations for commonly used buffers.

errors

Error types

properties

Definitions for parser and serializer combinators and their properties.

regular

Regular parser and serializer combinators.

utils

Utility functions and types.

Macros

inj_ord_choice_pat

Same as above but for patterns

inj_ord_choice_result

Maps x:Ti to ord_choice_result!(T1, …, Tn)

ord_choice

This macro constructs a nested OrdChoice combinator in the form of OrdChoice(…, OrdChoice(…, OrdChoice(…, …)))

ord_choice_result

Build a type for the result of ord_choice!

ord_choice_type

Build a type for the ord_choice! macro