Module spec 

Core specification traits for Vest combinators.

Re-exports

pub use crate::core::fns::ByteLenFnSpec;

pub use crate::core::fns::ParserFnSpec;

pub use crate::core::fns::SerializerDPSFnSpec;

pub use crate::core::fns::SerializerFnSpec;

Traits

AdmitsUniqueVal

Combinators whose consistency admits at most one value.

BytesCombinator

Marker for combinators whose corresponding values are raw bytes (Seq<u8>).

Consistency

Value well-formedness according to a format’s specification.

GoodSerializer

A well-behaved serializer.

MinMaxByteLen

Denotes the min/max byte length of a value w.r.t. a combinator’s format spec.

NonTailFmt

A non-tail format combinator would allow for things to be serialized after itself.

SafeParser

Parser safety.

SoundParser

Parser soundness.

SpecByteLen

Denotes the byte length of a value w.r.t. a combinator’s format spec.

SpecCombinator

Marker trait for all specification traits bundled together.

SpecParser

Parser specification.

SpecPred

Spec-level predicate abstraction.

SpecSerializer

Serializer specification.

SpecSerializerDps

Destination-passing style (DPS) serializer specification.

StaticByteLen

Static byte length for fixed-size combinators.

ValueByteLen

Like SpecByteLen, but the byte length can be computed from the value alone, without needing to refer to the combinator/format’s parameters or internal states (self).

Functions

disjoint_domains

disjoint_values

lemma_value_len_matches_byte_len

parser_fails_on

Type Aliases

PredFnSpec

A spec-level predicate function type alias.