Trait SpecByteLen 

pub trait SpecByteLen {
    type T;

    // Required method
    spec fn byte_len(&self, v: Self::T) -> nat;
}

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

Required Associated Types

type T

The type of values whose byte length is being computed.

Required Methods

spec fn byte_len(&self, v: Self::T) -> nat

Returns the number of bytes v occupies when serialized.

Implementations on Foreign Types

impl<S: SpecByteLen> SpecByteLen for &S

open spec fn byte_len(&self, v: Self::T) -> nat

{ (*self).byte_len(v) }

type T = <S as SpecByteLen>::T

Implementors

impl SpecByteLen for BerEndFmt

type T = ()

impl SpecByteLen for Integer8Fmt

type T = i8

impl SpecByteLen for Integer16Fmt

type T = i16

impl SpecByteLen for BerLengthFmt

type T = BerLength

impl SpecByteLen for BmpStringFmt

type T = BmpStringSpec

impl SpecByteLen for EnumeratedFmt

type T = int

impl SpecByteLen for Ia5StringFmt

type T = Ia5StringSpec

impl SpecByteLen for IntegerFmt

type T = int

impl SpecByteLen for ObjectIdentifierFmt

type T = ObjectIdentifierSpec

impl SpecByteLen for PrintableStringFmt

type T = PrintableStringSpec

impl SpecByteLen for TagFmt

type T = Tag

impl SpecByteLen for TeletexStringFmt

type T = TeletexStringSpec

impl SpecByteLen for UniversalStringFmt

type T = Seq<char>

impl SpecByteLen for Utf8StringFmt

type T = Seq<char>

impl SpecByteLen for CborInitialFmt

type T = CborInitial

impl SpecByteLen for Empty

type T = ()

impl SpecByteLen for Void

type T = ExecNever

impl SpecByteLen for I8

type T = i8

impl SpecByteLen for I16Be

type T = i16

impl SpecByteLen for I16Le

type T = i16

impl SpecByteLen for I32Be

type T = i32

impl SpecByteLen for I32Le

type T = i32

impl SpecByteLen for I64Be

type T = i64

impl SpecByteLen for I64Le

type T = i64

impl SpecByteLen for Eof

type T = ()

impl SpecByteLen for Tail

type T = Seq<u8>

impl SpecByteLen for U8

type T = u8

impl SpecByteLen for U16Be

type T = u16

impl SpecByteLen for U16Le

type T = u16

impl SpecByteLen for U24Be

type T = u32

impl SpecByteLen for U24Le

type T = u32

impl SpecByteLen for U32Be

type T = u32

impl SpecByteLen for U32Le

type T = u32

impl SpecByteLen for U64Be

type T = u64

impl SpecByteLen for U64Le

type T = u64

impl<A, B> SpecByteLen for Sum<A, B>

where A: SpecByteLen, B: SpecByteLen,

type T = Sum<<A as SpecByteLen>::T, <B as SpecByteLen>::T>

impl<A, B> SpecByteLen for Choice<A, B>

where A: SpecByteLen, B: SpecByteLen,

type T = Sum<<A as SpecByteLen>::T, <B as SpecByteLen>::T>

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

where A: SpecByteLen, B: SpecByteLen,

type T = (<A as SpecByteLen>::T, <B as SpecByteLen>::T)

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

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

type T = (<A as SpecByteLen>::T, <<B as SpecMap>::Output as SpecByteLen>::T)

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

where A: SpecByteLen, B: SpecByteLen,

type T = <B as SpecByteLen>::T

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

where A: SpecByteLen, B: SpecByteLen,

type T = <A as SpecByteLen>::T

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

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

type T = <A as SpecByteLen>::T

impl<A, Then: SpecByteLen> SpecByteLen for AndThen<A, Then>

type T = <Then as SpecByteLen>::T

impl<A: SpecByteLen> SpecByteLen for Star<A>

type T = Seq<<A as SpecByteLen>::T>

impl<A: SpecByteLen, B: SpecByteLen> SpecByteLen for Optional<A, B>

type T = (Option<<A as SpecByteLen>::T>, <B as SpecByteLen>::T)

impl<A: SpecByteLen, B: SpecByteLen> SpecByteLen for Repeat<A, B>

type T = (Seq<<A as SpecByteLen>::T>, <B as SpecByteLen>::T)

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

type T = (<A as SpecByteLen>::T, <B as SpecByteLen>::T)

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

type T = (<A as SpecByteLen>::T, (<B as SpecByteLen>::T, <C as SpecByteLen>::T))

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

type T = (<A as SpecByteLen>::T, (<B as SpecByteLen>::T, (<C as SpecByteLen>::T, <D as SpecByteLen>::T)))

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

type T = (<A as SpecByteLen>::T, (<B as SpecByteLen>::T, (<C as SpecByteLen>::T, (<D as SpecByteLen>::T, <E as SpecByteLen>::T))))

impl<C: SpecByteLen> SpecByteLen for SetOfFmt<C>

type T = Seq<<C as SpecByteLen>::T>

impl<C: SpecByteLen> SpecByteLen for OptionalEnd<C>

type T = Option<<C as SpecByteLen>::T>

impl<C: SpecByteLen> SpecByteLen for RepeatTillEnd<C>

type T = Seq<<C as SpecByteLen>::T>

impl<C: SpecByteLen, N: AsLen> SpecByteLen for RepeatN<C, N>

type T = Seq<<C as SpecByteLen>::T>

impl<C: SpecCombinator> SpecByteLen for BerSequenceFmt<C>

type T = <C as SpecByteLen>::T

impl<C: SpecCombinator> SpecByteLen for BerSequenceOfFmt<C>

type T = Seq<<C as SpecByteLen>::T>

impl<C: SpecCombinator, const LIMIT: usize> SpecByteLen for BerCharStringFmt<C, LIMIT>

type T = <C as SpecByteLen>::T

impl<Content: SpecCombinator, const DER: bool> SpecByteLen for ASN1Fmt<Content, DER>

type T = <Content as SpecParser>::PVal

impl<F> SpecByteLen for ImplicitlyTaggedFmt<F>

where F: Retaggable + SpecByteLen,

type T = <F as SpecByteLen>::T

impl<Field, Rest, const DER: bool> SpecByteLen for DefaultedFmt<Field, Field::T, Rest, DER>

where Field: SpecByteLen, Rest: SpecByteLen,

type T = (<Field as SpecByteLen>::T, <Rest as SpecByteLen>::T)

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

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

type T = <Tail as DepCombinator>::Val

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

where Inner: SpecByteLen,

type T = <Inner as SpecByteLen>::T

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

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

type T = <M as SpecMapper>::Out

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

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

type T = <M as SpecMapper>::Out

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

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

type T = <M as SpecMap>::Output

impl<Inner: SpecByteLen> SpecByteLen for Cond<Inner>

type T = <Inner as SpecByteLen>::T

impl<Inner: SpecByteLen> SpecByteLen for Named<Inner>

type T = <Inner as SpecByteLen>::T

impl<Inner: SpecByteLen> SpecByteLen for Opt<Inner>

type T = Option<<Inner as SpecByteLen>::T>

impl<Inner: SpecByteLen> SpecByteLen for Ref<Inner>

type T = <Inner as SpecByteLen>::T

impl<Inner: SpecByteLen, Len: AsLen> SpecByteLen for ExactLen<Inner, Len>

type T = <Inner as SpecByteLen>::T

impl<Len: AsLen> SpecByteLen for Varied<Len>

type T = Seq<u8>

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

where Tg: SpecByteLen, Of: SpecByteLen,

type T = <Of as SpecByteLen>::T

impl<Output, T, Spec, Exec> SpecByteLen for FnSerializer<Output, T, Spec, Exec>

where Output: OutputBuf, T: DeepView + ?Sized, Spec: SpecByteLen<T = T::V> + SpecSerializer<SVal = T::V> + Consistency<Val = T::V>, Exec: Fn(&T, &mut Output),

type T = <T as DeepView>::V

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

type T = (<P1 as SpecByteLen>::T, <P2 as SpecByteLen>::T)

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

where Repr: SpecByteLen,

type T = Nominal

impl<SpecP, Cnstcy, Blen> SpecByteLen for ParserSpecs<SpecP, Cnstcy, Blen>

where Blen: SpecByteLen, SpecP: SpecParser<PVal = Blen::T>, Cnstcy: Consistency<Val = Blen::T>,

type T = <Blen as SpecByteLen>::T

impl<SpecS, Blen> SpecByteLen for SerializerSpecs<SpecS, Blen>

where Blen: SpecByteLen, SpecS: SpecSerializer<SVal = Blen::T>,

type T = <Blen as SpecByteLen>::T

impl<T> SpecByteLen for BundledSpecs<T>

type T = T

impl<T> SpecByteLen for ByteLenFnSpec<T>

type T = T

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

type T = <C as SpecByteLen>::T

impl<T, Spec, Exec> SpecByteLen for FnByteLen<T, Spec, Exec>

where T: DeepView + ?Sized, Spec: SpecByteLen<T = T::V> + Consistency<Val = T::V>, Exec: Fn(&T) -> usize,

type T = <T as DeepView>::V

impl<T, Spec, Exec> SpecByteLen for FnPrepare<T, Spec, Exec>

where T: DeepView + ?Sized, Spec: SpecByteLen<T = T::V> + Consistency<Val = T::V>, Exec: Fn(&T) -> Result<usize, PreSerializeError>,

type T = <T as DeepView>::V

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

where Tg: SpecByteLen, Of: SpecByteLen,

type T = <Of as SpecByteLen>::T

impl<const DER: bool> SpecByteLen for AnyFmt<DER>

type T = AnySpec

impl<const DER: bool> SpecByteLen for BitStringFmt<DER>

type T = BitStringSpec

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

type T = bool

impl<const DER: bool> SpecByteLen for GeneralizedTimeFmt<DER>

type T = GeneralizedTimeSpec

impl<const DER: bool> SpecByteLen for LengthFmt<DER>

type T = usize

impl<const DER: bool> SpecByteLen for NatLengthFmt<DER>

type T = nat

impl<const DER: bool> SpecByteLen for RealFmt<DER>

type T = Seq<u8>

impl<const DER: bool> SpecByteLen for UtcTimeFmt<DER>

type T = UtcTime

impl<const DET: bool> SpecByteLen for CborHeadFmt<DET>

type T = CborHead

impl<const DET: bool, const LIMIT: usize> SpecByteLen for CborFmt<DET, LIMIT>

type T = CborValueSpec

impl<const LIMIT: usize> SpecByteLen for BerAnyFmt<LIMIT>

type T = AnySpec

impl<const LIMIT: usize> SpecByteLen for BerBitStringFmt<LIMIT>

type T = BitStringSpec

impl<const LIMIT: usize> SpecByteLen for BerOctetStringFmt<LIMIT>

type T = Seq<u8>

impl<const LIMIT: usize, Body, Param> SpecByteLen for FixWith<LIMIT, Body, Param>

where Body: SpecRecBody, Param: DeepView<V = Body::Param>,

type T = <Body as SpecRecBody>::T

impl<const MINIMAL: bool> SpecByteLen for Base128Fmt<MINIMAL>

type T = u64

impl<const MINIMAL: bool> SpecByteLen for VarInt<MINIMAL>

type T = u64

impl<const MINIMAL: bool, const N: usize> SpecByteLen for ULeb128<MINIMAL, N>

type T = nat

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

type T = Seq<u8>

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

type T = Seq<u8>

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

type T = Seq<<C as SpecByteLen>::T>

impl<const NONDETERMINISTIC: bool, A, B> SpecByteLen for Alt<A, B, NONDETERMINISTIC>

where A: SpecByteLen + Consistency<Val = A::T>, B: SpecByteLen<T = A::T> + Consistency<Val = B::T>,

type T = <A as SpecByteLen>::T