Crate vest_lib 

vest_lib

vest_lib is Vest’s format combinator library verified in Verus. A format in Vest is organized in three layers:

• pure parsing, serialization, byte-length, and consistency specifications in core::spec;
• executable parsing and serialization APIs in core::exec; and
• correctness and security theorems in core::proof.

Where to start

• core includes Vest’s core specs as well as the runtime API and buffer abstractions.
• combinators documents all the primitive and higher-order formats.
• asn1 contains modular DER and BER formats.
• cbor provides generic CBOR formats for both general and deterministic profiles.
• primitives contains reusable variable-width integer formats.

See the Vest guide for more background and gentle introductions.

Modules

asn1

Verified ASN.1 contents, tag-length-value wrappers, and schema combinators.

cbor

Concise Binary Object Representation (CBOR) formats.

combinators

Combinators for composing binary data formats.

core

Core specifications and correctness/security theorems for Vest combinators.

macros

Utility macros.

primitives

Verified variable-width integer formats built from the core combinators.

Macros

impl_ber

Implements the verified BER traits and executable APIs for a generated nominal format.

impl_der

Implements the verified DER traits and executable APIs for a generated nominal format.

with_deep_view

Defines paired executable/spec nominal value types and corresponding DeepView and SpecMapper impls.

with_deep_view_and_mapper

Defines paired executable/spec nominal value types and corresponding DeepView and SpecMapper impls.

Type Aliases

Never

An uninhabitable type used to represent impossible values (e.g., in combinators::Void).