Module exec 

Executable parsing, validation, length calculation, and serialization.

Application code normally uses the following trait methods:

• Parser::parse consumes an input prefix and produces a structured value;
• Prepare::prepare validates a value against the format specification and computes its exact wire length;
• SerializerExt::serialize writes into an exactly sized slice without allocation.

InputBuf and OutputBuf let combinators share implementations across different buffer types.

Re-exports

pub use error::ParseError;

pub use error::ParseErrorKind;

pub use input::InputBuf;

pub use input::InputSlice;

pub use output::OutputBuf;

pub use output::OutputSlice;

pub use parser::PResult;

pub use parser::Parser;

pub use serializer::ByteLen;

pub use serializer::ComplianceErrorKind;

pub use serializer::PreSerializeError;

pub use serializer::Prepare;

pub use serializer::Serializer;

pub use serializer::SerializerExt;

Modules

bridge_lemmas

Bridges executable invariants through common combinator wrappers.

error

Runtime parse errors.

fns

Executable fn traits.

input

Input abstractions for executable parsers.

output

Output abstractions for executable serializers.

parser

Executable parser traits.

serializer

Executable serializer traits.

Functions

_verus_external_fn_specification_1__60__32__91_T_93__32_as_32_PartialEq_32__60__32__91_U_93__32__62__32__62__32__58__58__32_eq^⚠

bytes_eq