vest_lib/core/mod.rs
1//! Core specifications and correctness/security theorems for Vest combinators.
2//!
3//! This module forms the foundation of the Vest combinator framework. It defines:
4//!
5//! ## [`spec`] — Specification Family of Traits
6//!
7//! - [`spec::SpecParser`] — parser specification
8//! - [`spec::SpecSerializer`] — serializer specification
9//! - [`spec::Consistency`] — value well-formedness against the format specification
10//! - [`spec::SpecByteLen`] — byte length of serialized values
11//! - [`spec::SpecSerializerDps`] — destination-passing style serializer specification for better composability
12//! - [`spec::StaticByteLen`] — fixed byte length for static-size formats
13//!
14//! These traits are designed to be as independent as possible such that they can be useful individually
15//! (e.g., applications that only need to specify parsing but not serialization, or vice versa). However,
16//! Vest combinators generally provide trait implementations for all of these traits, and the proofs
17//! in the [`proof`] module often rely on multiple, if not all, of these traits being implemented
18//! for the combinators in question.
19//!
20//! ## [`proof`] — Proof Family of Traits
21//!
22//! - [`proof::SPRoundTrip`] — serialize-parse roundtrip
23//! - [`proof::SPRoundTripDps`] — serialize-parse roundtrip (the DPS variant, used mostly internally),
24//! which also carries the unambiguity side condition needed by roundtrip proofs
25//! - [`proof::PSRoundTrip`] — parse-serialize roundtrip
26//! - [`proof::NonMalleable`] — parser non-malleability
27//! - [`proof::NoLookAhead`] — parser no-look-ahead property
28//! - [`proof::Productive`] — parser productivity
29//! - [`proof::NonAmbiguous`] — serializer non-ambiguity
30//! - [`proof::EquivSerializers`] / [`proof::EquivSerializersGeneral`] — DPS ↔ non-DPS equivalence
31//!
32//! Following the same philosophy as the specification traits, these proof traits are defined on top of
33//! a *minimal* set of specification traits, and crucially, they are *not* defined/dependent on each other.
34//! This way, combinators can implement only the proof traits that are relevant to their intended use cases
35//! (e.g., formats that accept non-canonical encodings may not be non-malleable, and thus would not implement
36//! [`proof::NonMalleable`]).
37//!
38//! ## [`fns`] — Spec Function Combinators
39//!
40//! Type aliases and trait implementations that allow plain Verus `spec_fn`s
41//! to be used as combinators without defining new types.
42pub mod exec;
43pub mod fns;
44pub mod proof;
45pub mod spec;