Trait StaticByteLen 

pub trait StaticByteLen: SpecByteLen + Consistency<Val = Self::T> {
    // Required methods
    spec fn static_byte_len() -> nat;
    proof fn lemma_static_len_matches_byte_len(&self, v: Self::T);
}

Static byte length for fixed-size combinators.

Required Methods

spec fn static_byte_len() -> nat

The statically known serialized length.

proof fn lemma_static_len_matches_byte_len(&self, v: Self::T)

requires

self.consistent(v),

ensures

self.byte_len(v) == Self::static_byte_len(),

Bridge between the dynamic byte-length view and the static one.

Dyn Compatibility

This trait is not dyn compatible.

In older versions of Rust, dyn compatibility was called "object safety", so this trait is not object safe.

Implementors

impl StaticByteLen for Empty

impl StaticByteLen for Void

impl StaticByteLen for I8

impl StaticByteLen for I16Be

impl StaticByteLen for I16Le

impl StaticByteLen for I32Be

impl StaticByteLen for I32Le

impl StaticByteLen for I64Be

impl StaticByteLen for I64Le

impl StaticByteLen for Eof

impl StaticByteLen for U8

impl StaticByteLen for U16Be

impl StaticByteLen for U16Le

impl StaticByteLen for U24Be

impl StaticByteLen for U24Le

impl StaticByteLen for U32Be

impl StaticByteLen for U32Le

impl StaticByteLen for U64Be

impl StaticByteLen for U64Le

impl<A, B> StaticByteLen for PairRev<A, B>

where A: StaticByteLen, B: StaticByteLen,

impl<A, B> StaticByteLen for Bind<A, B>

where A: StaticByteLen, B: SpecMap<Input = A::T>, B::Output: StaticByteLen,

impl<A, B, const CHECK: bool> StaticByteLen for Preceded<A, A::T, B, CHECK>

where A: StaticByteLen, B: StaticByteLen,

impl<A, B, const CHECK: bool> StaticByteLen for Terminated<A, B, B::T, CHECK>

where A: StaticByteLen, B: StaticByteLen,

impl<A, Pred> StaticByteLen for Refined<A, Pred>

where A: StaticByteLen, Pred: SpecPred<A::T>,

impl<A: StaticByteLen, B: StaticByteLen> StaticByteLen for Pair<A, B>

impl<A: StaticByteLen, B: StaticByteLen, C: StaticByteLen> StaticByteLen for Permute3<A, B, C>

impl<A: StaticByteLen, B: StaticByteLen, C: StaticByteLen, D: StaticByteLen> StaticByteLen for Permute4<A, B, C, D>

impl<A: StaticByteLen, B: StaticByteLen, C: StaticByteLen, D: StaticByteLen, E: StaticByteLen> StaticByteLen for Permute5<A, B, C, D, E>

impl<Head, Tail> StaticByteLen for Implicit<Head, Tail>

where Head: StaticByteLen, Tail: DepCombinator<Key = Head::T>, Tail::Body: StaticByteLen<T = Tail::Val>,

impl<Inner> StaticByteLen for Const<Inner, Inner::T>

where Inner: StaticByteLen,

impl<Inner, M> StaticByteLen for Mapped<Inner, M>

where Inner: StaticByteLen, M: SpecMapper<In = Inner::T>,

impl<Inner, M> StaticByteLen for TryMap<Inner, M>

where Inner: StaticByteLen, M: SpecMapper<In = Inner::T>,

impl<Inner, M, MRev> StaticByteLen for Mapped<Inner, BiMap<M, MRev>>

where Inner: StaticByteLen, M: SpecMap<Input = Inner::T>, MRev: SpecMap<Input = M::Output, Output = M::Input>,

impl<Inner: StaticByteLen> StaticByteLen for Cond<Inner>

impl<Inner: StaticByteLen> StaticByteLen for Named<Inner>

impl<Of, Tg> StaticByteLen for SuffixTagged<Of, Tg, Tg::T>

where Tg: StaticByteLen, Of: StaticByteLen,

impl<P1: StaticByteLen, P2: StaticByteLen> StaticByteLen for Permute2<P1, P2>

impl<Repr, Tuple, Nominal> StaticByteLen for Bits<Repr, Tuple, Nominal>

where Repr: StaticByteLen,

impl<T, C: StaticByteLen, const N: usize> StaticByteLen for Dispatch<T, C, N>

impl<Tg, Of> StaticByteLen for PrefixTagged<Tg, Tg::T, Of>

where Tg: StaticByteLen, Of: StaticByteLen,

impl<const DER: bool> StaticByteLen for BoolFmt<DER>

impl<const N: usize> StaticByteLen for Fixed<N>

impl<const N: usize> StaticByteLen for Const<Fixed<N>, [u8; N]>

impl<const N: usize, C: StaticByteLen> StaticByteLen for Array<N, C>