Trait ByteLen 

pub trait ByteLen<T>
where
    Self: SpecByteLen<T = T::V>,
    T: DeepView + ?Sized,
{
    // Required method
    exec fn length(&self, v: &T) -> len : usize;

    // Provided method
    open spec fn exec_inv(&self) -> bool { ... }
}

Computes the exact serialized length of a value already known to fit usize.

Unlike Prepare, this operation does not check the format’s consistency predicate. Use Prepare::prepare for untrusted or newly constructed values.

Required Methods

exec fn length(&self, v: &T) -> len : usize

requires

self.exec_inv(),

self.byte_len(v.deep_view()) <= usize::MAX,

ensures

len == self.byte_len(v.deep_view()),

Returns the exact number of bytes produced by serialization.

Provided Methods

open spec fn exec_inv(&self) -> bool

{ true }

Extra invariant required by the executable length implementation.

Implementations on Foreign Types

impl<T, S> ByteLen<T> for &S

where T: DeepView + ?Sized, S: ByteLen<T>,

open spec fn exec_inv(&self) -> bool

{ (*self).exec_inv() }

exec fn length(&self, v: &T) -> len : usize

Implementors

impl ByteLen<BerLength> for BerLengthFmt

impl ByteLen<i8> for Integer8Fmt

impl ByteLen<i8> for I8

impl ByteLen<i16> for Integer16Fmt

impl ByteLen<i16> for I16Be

impl ByteLen<i16> for I16Le

impl ByteLen<i32> for I32Be

impl ByteLen<i32> for I32Le

impl ByteLen<i64> for I64Be

impl ByteLen<i64> for I64Le

impl ByteLen<u8> for U8

impl ByteLen<u16> for U16Be

impl ByteLen<u16> for U16Le

impl ByteLen<u32> for U24Be

impl ByteLen<u32> for U24Le

impl ByteLen<u32> for U32Be

impl ByteLen<u32> for U32Le

impl ByteLen<u64> for U64Be

impl ByteLen<u64> for U64Le

impl ByteLen<()> for BerEndFmt

impl ByteLen<()> for Empty

impl ByteLen<()> for Eof

impl ByteLen<BitStringOwned> for BitStringFmt<false>

Available on crate feature alloc only.

impl ByteLen<BmpString> for BmpStringFmt

Available on crate feature alloc only.

impl ByteLen<Ia5StringOwned> for Ia5StringFmt

Available on crate feature alloc only.

impl ByteLen<ObjectIdentifier> for ObjectIdentifierFmt

Available on crate feature alloc only.

impl ByteLen<PrintableStringOwned> for PrintableStringFmt

Available on crate feature alloc only.

impl ByteLen<Tag> for TagFmt

impl ByteLen<TeletexStringOwned> for TeletexStringFmt

Available on crate feature alloc only.

impl ByteLen<CborInitial> for CborInitialFmt

impl ByteLen<ExecNever> for Void

impl ByteLen<String> for UniversalStringFmt

Available on crate feature alloc only.

impl ByteLen<String> for Utf8StringFmt

Available on crate feature alloc only.

impl ByteLen<[u8]> for Tail

impl<'a, const DER: bool> ByteLen<Any<'a>> for AnyFmt<DER>

impl<'a, const DER: bool> ByteLen<Real<'a, DER>> for RealFmt<DER>

impl<'i> ByteLen<&'i str> for Utf8StringFmt

impl<'i> ByteLen<&'i [u8]> for Tail

impl<'i> ByteLen<Integer<'i>> for EnumeratedFmt

impl<'i> ByteLen<Integer<'i>> for IntegerFmt

impl<'i> ByteLen<Ia5String<'i>> for Ia5StringFmt

impl<'i> ByteLen<PrintableString<'i>> for PrintableStringFmt

impl<'i> ByteLen<TeletexString<'i>> for TeletexStringFmt

impl<'i, Len: AsLen> ByteLen<&'i [u8]> for Varied<Len>

impl<'i, const DER: bool> ByteLen<BitString<'i, DER>> for BitStringFmt<DER>

impl<'i, const DER: bool> ByteLen<GeneralizedTime<'i>> for GeneralizedTimeFmt<DER>

impl<'i, const DET: bool, const LIMIT: usize> ByteLen<CborValue<'i>> for CborFmt<DET, LIMIT>

impl<'i, const N: usize> ByteLen<&'i [u8]> for Fixed<N>

impl<A, AST> ByteLen<Option<AST>> for OptionalEnd<A>

where A: ByteLen<AST>, AST: DeepView,

impl<A, AVal, B, BVal, const CHECK: bool> ByteLen<BVal> for Preceded<A, AVal, B, CHECK>

where AVal: DeepView<V = AVal>, BVal: DeepView, A: ByteLen<AVal>, B: ByteLen<BVal>,

impl<A, B, AVal, BVal> ByteLen<(AVal, BVal)> for PairRev<A, B>

where AVal: DeepView, BVal: DeepView, A: ByteLen<AVal>, B: ByteLen<BVal>,

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

where T: DeepView, BVal: DeepView<V = BVal>, A: ByteLen<T>, B: ByteLen<BVal>,

impl<A, B, C, D, E, TA, TB, TC, TD, TE> ByteLen<(TA, (TB, (TC, (TD, TE))))> for Permute5<A, B, C, D, E>

where TA: DeepView, TB: DeepView, TC: DeepView, TD: DeepView, TE: DeepView, A: ByteLen<TA>, B: ByteLen<TB>, C: ByteLen<TC>, D: ByteLen<TD>, E: ByteLen<TE>,

impl<A, B, C, D, TA, TB, TC, TD> ByteLen<(TA, (TB, (TC, TD)))> for Permute4<A, B, C, D>

where TA: DeepView, TB: DeepView, TC: DeepView, TD: DeepView, A: ByteLen<TA>, B: ByteLen<TB>, C: ByteLen<TC>, D: ByteLen<TD>,

impl<A, B, C, TA, TB, TC> ByteLen<(TA, (TB, TC))> for Permute3<A, B, C>

where TA: DeepView, TB: DeepView, TC: DeepView, A: ByteLen<TA>, B: ByteLen<TB>, C: ByteLen<TC>,

impl<A, B, STA, STB> ByteLen<(STA, STB)> for Bind<A, B>

where STA: DeepView, STB: DeepView, A: ByteLen<STA>, B::O: ByteLen<STB>, B: MapRef<STA, Input = STA::V>,

impl<A, B, TA, TB> ByteLen<(&[TA], TB)> for Repeat<A, B>

where A: ByteLen<TA> + Copy, B: ByteLen<TB>, TA: DeepView, TB: DeepView,

impl<A, B, TA, TB> ByteLen<(Option<TA>, TB)> for Optional<A, B>

where TA: DeepView, TB: DeepView, A: ByteLen<TA>, B: ByteLen<TB>,

impl<A, B, TA, TB> ByteLen<Sum<TA, TB>> for Sum<A, B>

where TA: DeepView, TB: DeepView, A: ByteLen<TA>, B: ByteLen<TB>,

impl<A, B, TA, TB> ByteLen<Sum<TA, TB>> for Choice<A, B>

where TA: DeepView, TB: DeepView, A: ByteLen<TA>, B: ByteLen<TB>,

impl<A, B, TA, TB> ByteLen<(TA, TB)> for Pair<A, B>

where TA: DeepView, TB: DeepView, A: ByteLen<TA>, B: ByteLen<TB>,

impl<A, PredFn, T> ByteLen<T> for Refined<A, PredFn>

where T: DeepView, A: ByteLen<T>, PredFn: Pred<T>,

impl<A, T> ByteLen<&[T]> for RepeatTillEnd<A>

where A: ByteLen<T> + Copy, T: DeepView,

impl<A, T> ByteLen<Option<T>> for Opt<A>

where T: DeepView, A: ByteLen<T>,

impl<A, T> ByteLen<Vec<T>> for RepeatTillEnd<A>

where A: ByteLen<T> + Copy, T: DeepView,

Available on crate feature alloc only.

impl<A, Then, ThenST> ByteLen<ThenST> for AndThen<A, Then>

where ThenST: DeepView + ?Sized, Then: ByteLen<ThenST>,

impl<C, Elem> ByteLen<[Elem]> for SetOfFmt<C>

where C: SpecByteLen<T = <Elem as DeepView>::V> + ByteLen<Elem> + Copy, Elem: DeepView,

impl<C, Elem> ByteLen<Vec<Elem>> for SetOfFmt<C>

where C: SpecByteLen<T = <Elem as DeepView>::V> + ByteLen<Elem> + Copy, Elem: DeepView,

Available on crate feature alloc only.

impl<C, T> ByteLen<&[T]> for BerSequenceOfFmt<C>

where C: SpecCombinator + ByteLen<T> + Copy, T: DeepView,

impl<C, T> ByteLen<Vec<T>> for BerSequenceOfFmt<C>

where C: SpecCombinator + ByteLen<T> + Copy, T: DeepView,

Available on crate feature alloc only.

impl<C, T> ByteLen<T> for BerSequenceFmt<C>

where T: DeepView + ?Sized, C: SpecCombinator + ByteLen<T> + Copy,

impl<C, T, const LIMIT: usize> ByteLen<T> for BerCharStringFmt<C, LIMIT>

where T: DeepView + ?Sized, C: SpecCombinator + Copy + GoodSerializer + ByteLen<T>,

impl<Content, T, const DER: bool> ByteLen<T> for ASN1Fmt<Content, DER>

where T: DeepView + ?Sized, Content: SpecCombinator + ByteLen<T>,

impl<F, T> ByteLen<T> for ImplicitlyTaggedFmt<F>

where T: DeepView + ?Sized, F: Retaggable + ByteLen<T>,

impl<Field, Default, Rest, R, const DER: bool> ByteLen<(Default, R)> for DefaultedFmt<Field, Default, Rest, DER>

where Field: SpecByteLen<T = Default> + ByteLen<Default>, Rest: SpecByteLen<T = R::V> + ByteLen<R>, Default: DeepView<V = Default> + PartialEq + Structural + Copy, R: DeepView,

impl<Inner, M, MRev, T> ByteLen<T> for Mapped<Inner, BiMap<M, MRev>>

where T: DeepView, M: SpecMap<Input = MRev::Output, Output = T::V>, MRev: SpecMap<Input = T::V> + for<'x> Map<&'x T>, Inner: for<'x> ByteLen<<MRev as Map<&'x T>>::O>,

impl<Inner, N, T> ByteLen<[T]> for RepeatN<Inner, N>

where Inner: ByteLen<T>, T: DeepView, N: AsLen,

impl<Inner, T> ByteLen<&T> for Ref<Inner>

where T: DeepView + ?Sized, Inner: ByteLen<T>,

impl<Inner, T> ByteLen<[T]> for Star<Inner>

where Inner: ByteLen<T>, T: DeepView,

impl<Inner, T, const N: usize> ByteLen<[T; N]> for Array<N, Inner>

where Inner: ByteLen<T>, T: DeepView,

impl<Inner, V, T> ByteLen<T> for Const<Inner, V>

where T: DeepView<V = V>, Inner: SpecByteLen<T = V> + ByteLen<T>,

impl<Len, Inner, InnerST> ByteLen<InnerST> for ExactLen<Inner, Len>

where Len: AsLen, InnerST: DeepView + ?Sized, Inner: ByteLen<InnerST>,

impl<Len: AsLen> ByteLen<[u8]> for Varied<Len>

impl<Of, TagVal, Tg, T> ByteLen<T> for SuffixTagged<Of, Tg, TagVal>

where Tg: SpecByteLen<T = TagVal> + ByteLen<TagVal>, TagVal: DeepView<V = TagVal> + PartialEq + Structural + Copy, T: DeepView, Of: ByteLen<T>,

impl<P1, P2, T1, T2> ByteLen<(T1, T2)> for Permute2<P1, P2>

where T1: DeepView, T2: DeepView, P1: ByteLen<T1>, P2: ByteLen<T2>,

impl<T, Inner> ByteLen<T> for Cond<Inner>

where T: DeepView, Inner: ByteLen<T>,

impl<T, Inner> ByteLen<T> for Named<Inner>

where T: DeepView, Inner: ByteLen<T>,

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

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

impl<T, const LIMIT: usize> ByteLen<T> for BerBitStringFmt<LIMIT>

where T: DeepView<V = BitStringSpec> + ?Sized, ASN1Fmt<BitStringFmt<BER>, BER>: ByteLen<T>,

impl<Tg, TagVal, Of, T> ByteLen<T> for PrefixTagged<Tg, TagVal, Of>

where Tg: SpecByteLen<T = TagVal> + ByteLen<TagVal>, TagVal: DeepView<V = TagVal> + PartialEq + Structural + Copy, T: DeepView, Of: ByteLen<T>,

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

impl<const DER: bool> ByteLen<usize> for LengthFmt<DER>

impl<const DER: bool> ByteLen<AnyOwned> for AnyFmt<DER>

Available on crate feature alloc only.

impl<const DER: bool> ByteLen<UtcTime> for UtcTimeFmt<DER>

impl<const DET: bool> ByteLen<CborHead> for CborHeadFmt<DET>

impl<const LIMIT: usize> ByteLen<AnyOwned> for BerAnyFmt<LIMIT>

Available on crate feature alloc only.

impl<const LIMIT: usize> ByteLen<Vec<u8>> for BerOctetStringFmt<LIMIT>

Available on crate feature alloc only.

impl<const LIMIT: usize> ByteLen<[u8]> for BerOctetStringFmt<LIMIT>

impl<const MINIMAL: bool> ByteLen<u64> for Base128Fmt<MINIMAL>

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

impl<const N: usize> ByteLen<[u8]> for Fixed<N>