Trait StaticByteLen 

pub trait StaticByteLen: SpecByteLen + Consistency<Val = Self::T> {
    // Required methods
    spec fn static_byte_len() -> nat;
    broadcast 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.

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

requires

self.consistent(v),

ensures

#[trigger] 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".

Implementations on Foreign Types

impl<S: StaticByteLen> StaticByteLen for &S

open spec fn static_byte_len() -> nat

{ S::static_byte_len() }

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

Implementors

impl StaticByteLen for Empty

impl StaticByteLen for Eof

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 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 StaticByteLen for Void

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, B> StaticByteLen for Bind<A, B>

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

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

where A: StaticByteLen, B: StaticByteLen,

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

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

impl<A, Then> StaticByteLen for AndThen<A, Then>

where A: BytesCombinator + StaticByteLen, Then: Consistency + SpecByteLen<T = Then::Val>,

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

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

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

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

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

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

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, 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: StaticByteLen, Len: AsLen> StaticByteLen for ExactLen<Inner, Len>

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

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

impl<Inner: StaticByteLen> StaticByteLen for Ref<Inner>

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

where Inner: StaticByteLen,

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, C: StaticByteLen> StaticByteLen for Array<N, C>

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

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