vest_lib/combinators/bits/
mod.rs

1//! Byte-aligned bitfield specification and proof combinator.
2/// Correctness proofs for this combinator.
3pub mod proof;
4/// Specification trait implementations for this combinator.
5pub mod spec;
6
7use crate::core::spec::{PredFnSpec, SpecByteLen};
8use vstd::prelude::*;
9
10verus! {
11
12#[verifier::reject_recursive_types(Tuple)]
13#[verifier::reject_recursive_types(Nominal)]
14/// Packs a tuple of logical bitfield values into one fixed-width integer representation.
15///
16/// Generated Vest bitfield formats use the functions stored here to unpack the
17/// wire integer, validate the structural tuple, construct the public nominal
18/// value, and perform the inverse operation during serialization.
19pub struct Bits<Repr: SpecByteLen, Tuple, Nominal> {
20    /// Integer format that reads and writes the complete bitfield word.
21    pub repr: Repr,
22    /// Splits the representation into its structural field tuple.
23    pub unpack: spec_fn(Repr::T) -> Tuple,
24    /// Packs the structural field tuple into the representation.
25    pub pack: spec_fn(Tuple) -> Repr::T,
26    /// Predicate enforcing field widths and reserved-bit constraints.
27    pub refinement: PredFnSpec<Tuple>,
28    /// Constructs the public nominal value from structural fields.
29    pub ctor: spec_fn(Tuple) -> Nominal,
30    /// Projects a public nominal value back to structural fields.
31    pub dtor: spec_fn(Nominal) -> Tuple,
32    /// Additional consistency predicate for nominal values.
33    pub consistent: PredFnSpec<Nominal>,
34}
35
36} // verus!
vest_lib/combinators/bits/mod.rs

vest_lib/combinators/bits/
mod.rs
