Module core 

Core specifications and correctness/security theorems for Vest combinators.

This module forms the foundation of the Vest combinator framework. It defines:

spec — Specification Family of Traits

• spec::SpecParser — parser specification
• spec::SpecSerializer — serializer specification
• spec::Consistency — value well-formedness against the format specification
• spec::SpecByteLen — byte length of serialized values
• spec::SpecSerializerDps — destination-passing style serializer specification for better composability
• spec::StaticByteLen — fixed byte length for static-size formats

These traits are designed to be as independent as possible such that they can be useful individually (e.g., applications that only need to specify parsing but not serialization, or vice versa). However, Vest combinators generally provide trait implementations for all of these traits, and the proofs in the proof module often rely on multiple, if not all, of these traits being implemented for the combinators in question.

proof — Proof Family of Traits

• proof::SPRoundTrip — serialize-parse roundtrip
• proof::SPRoundTripDps — serialize-parse roundtrip (the DPS variant, used mostly internally), which also carries the unambiguity side condition needed by roundtrip proofs
• proof::PSRoundTrip — parse-serialize roundtrip
• proof::NonMalleable — parser non-malleability
• proof::NoLookAhead — parser no-look-ahead property
• proof::Productive — parser productivity
• proof::NonAmbiguous — serializer non-ambiguity
• proof::EquivSerializers / proof::EquivSerializersGeneral — DPS ↔ non-DPS equivalence

Following the same philosophy as the specification traits, these proof traits are defined on top of a minimal set of specification traits, and crucially, they are not defined/dependent on each other. This way, combinators can implement only the proof traits that are relevant to their intended use cases (e.g., formats that accept non-canonical encodings may not be non-malleable, and thus would not implement proof::NonMalleable).

fns — Spec Function Combinators

Type aliases and trait implementations that allow plain Verus spec_fns to be used as combinators without defining new types.

Modules

exec

Executable parsing, validation, length calculation, and serialization.

fns

Type aliases and trait implementations allowing plain spec_fns to serve as combinators.

proof

Correctness and security proof traits for Vest combinators.

spec

Core specification traits for Vest combinators.