Trait Serializer 

pub trait Serializer<Output, T>
where
    Output: OutputBuf,
    Self: SpecByteLen<T = T::V> + SpecSerializer<SVal = T::V> + Consistency<Val = T::V>,
    T: DeepView + ?Sized,
{
    // Required method
    exec fn serialize_into(&self, v: &T, obuf: &mut Output);

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

An executable serializer targeting Output.

Required Methods

exec fn serialize_into(&self, v: &T, obuf: &mut Output)

requires

self.exec_inv(),

self.consistent(v.deep_view()),

old(obuf).fits(self.byte_len(v.deep_view())),

ensures

final(obuf)@ == old(obuf)@ + self.spec_serialize(v.deep_view()),

forall |n| old(obuf).fits(self.byte_len(v.deep_view()) + n) <==> final(obuf).fits(n),

old(obuf).same_destination(final(obuf)),

Serializes the value v into the output buffer obuf by (logically) appending the serialized bytes to the end of obuf. This view has two main benefits:

1. It matches the specification of the serializer closely, which simplifies the proofs;
2. It is general enough to support both fixed-size (e.g., &mut [u8]) and growable (e.g., Vec<u8>) output buffers (see OutputBuf).

Preconditions

• The serializer’s execution invariant holds (mainly used for super::fns::FnSerializer, usually trivial for most combinators).
• The value v is compliant with the format specification.
• The output buffer has enough space to hold the serialized value.

Postconditions

• The output buffer’s contents are extended by the serialized value.
• The output buffer’s remaining capacity is reduced by the serialized value’s length.
• The output buffer’s destination remains the same.

Provided Methods

open spec fn exec_inv(&self) -> bool

{ true }

Implementations on Foreign Types

impl<Output, T, S> Serializer<Output, T> for &S

where Output: OutputBuf, T: DeepView + ?Sized, S: Serializer<Output, T>,

open spec fn exec_inv(&self) -> bool

{ (*self).exec_inv() }

exec fn serialize_into(&self, v: &T, obuf: &mut Output)

Implementors

impl<'a, Output: OutputBuf, const DER: bool> Serializer<Output, Any<'a>> for AnyFmt<DER>

impl<'a, Output: OutputBuf, const DER: bool> Serializer<Output, Real<'a, DER>> for RealFmt<DER>

impl<'i, Output: OutputBuf> Serializer<Output, &'i str> for Utf8StringFmt

impl<'i, Output: OutputBuf> Serializer<Output, &'i [u8]> for Tail

impl<'i, Output: OutputBuf> Serializer<Output, Integer<'i>> for EnumeratedFmt

impl<'i, Output: OutputBuf> Serializer<Output, Integer<'i>> for IntegerFmt

impl<'i, Output: OutputBuf> Serializer<Output, Ia5String<'i>> for Ia5StringFmt

impl<'i, Output: OutputBuf> Serializer<Output, PrintableString<'i>> for PrintableStringFmt

impl<'i, Output: OutputBuf> Serializer<Output, TeletexString<'i>> for TeletexStringFmt

impl<'i, Output: OutputBuf, Len: AsLen> Serializer<Output, &'i [u8]> for Varied<Len>

impl<'i, Output: OutputBuf, const DER: bool> Serializer<Output, BitString<'i, DER>> for BitStringFmt<DER>

impl<'i, Output: OutputBuf, const DER: bool> Serializer<Output, GeneralizedTime<'i>> for GeneralizedTimeFmt<DER>

impl<'i, Output: OutputBuf, const DET: bool, const LIMIT: usize> Serializer<Output, CborValue<'i>> for CborFmt<DET, LIMIT>

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

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

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

impl<Output, F, T> Serializer<Output, T> for ImplicitlyTaggedFmt<F>

where Output: OutputBuf, T: DeepView + ?Sized, F: Retaggable + Serializer<Output, T>,

impl<Output, Inner, T> Serializer<Output, &T> for Ref<Inner>

where Output: OutputBuf, T: DeepView + ?Sized, Inner: Serializer<Output, T>,

impl<Output, T, Spec, Exec> Serializer<Output, T> 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),

impl<Output, T, const LIMIT: usize> Serializer<Output, T> for BerBitStringFmt<LIMIT>

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

impl<Output: OutputBuf> Serializer<Output, BerLength> for BerLengthFmt

impl<Output: OutputBuf> Serializer<Output, i8> for Integer8Fmt

impl<Output: OutputBuf> Serializer<Output, i8> for I8

impl<Output: OutputBuf> Serializer<Output, i16> for Integer16Fmt

impl<Output: OutputBuf> Serializer<Output, i16> for I16Be

impl<Output: OutputBuf> Serializer<Output, i16> for I16Le

impl<Output: OutputBuf> Serializer<Output, i32> for I32Be

impl<Output: OutputBuf> Serializer<Output, i32> for I32Le

impl<Output: OutputBuf> Serializer<Output, i64> for I64Be

impl<Output: OutputBuf> Serializer<Output, i64> for I64Le

impl<Output: OutputBuf> Serializer<Output, u8> for U8

impl<Output: OutputBuf> Serializer<Output, u16> for U16Be

impl<Output: OutputBuf> Serializer<Output, u16> for U16Le

impl<Output: OutputBuf> Serializer<Output, u32> for U24Be

impl<Output: OutputBuf> Serializer<Output, u32> for U24Le

impl<Output: OutputBuf> Serializer<Output, u32> for U32Be

impl<Output: OutputBuf> Serializer<Output, u32> for U32Le

impl<Output: OutputBuf> Serializer<Output, u64> for U64Be

impl<Output: OutputBuf> Serializer<Output, u64> for U64Le

impl<Output: OutputBuf> Serializer<Output, ()> for BerEndFmt

impl<Output: OutputBuf> Serializer<Output, ()> for Empty

impl<Output: OutputBuf> Serializer<Output, ()> for Eof

impl<Output: OutputBuf> Serializer<Output, BitStringOwned> for BitStringFmt<false>

Available on crate feature alloc only.

impl<Output: OutputBuf> Serializer<Output, BmpString> for BmpStringFmt

Available on crate feature alloc only.

impl<Output: OutputBuf> Serializer<Output, Ia5StringOwned> for Ia5StringFmt

Available on crate feature alloc only.

impl<Output: OutputBuf> Serializer<Output, ObjectIdentifier> for ObjectIdentifierFmt

Available on crate feature alloc only.

impl<Output: OutputBuf> Serializer<Output, PrintableStringOwned> for PrintableStringFmt

Available on crate feature alloc only.

impl<Output: OutputBuf> Serializer<Output, Tag> for TagFmt

impl<Output: OutputBuf> Serializer<Output, TeletexStringOwned> for TeletexStringFmt

Available on crate feature alloc only.

impl<Output: OutputBuf> Serializer<Output, CborInitial> for CborInitialFmt

impl<Output: OutputBuf> Serializer<Output, ExecNever> for Void

impl<Output: OutputBuf> Serializer<Output, String> for UniversalStringFmt

Available on crate feature alloc only.

impl<Output: OutputBuf> Serializer<Output, String> for Utf8StringFmt

Available on crate feature alloc only.

impl<Output: OutputBuf> Serializer<Output, [u8]> for Tail

impl<Output: OutputBuf, A, AVal, B, T, const CHECK: bool> Serializer<Output, T> for Preceded<A, AVal, B, CHECK>

where AVal: DeepView<V = AVal>, T: DeepView, A: Serializer<Output, AVal>, B: Serializer<Output, T>,

impl<Output: OutputBuf, A, B, BVal, T, const CHECK: bool> Serializer<Output, T> for Terminated<A, B, BVal, CHECK>

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

impl<Output: OutputBuf, A, B, C, D, E, TA, TB, TC, TD, TE> Serializer<Output, (TA, (TB, (TC, (TD, TE))))> for Permute5<A, B, C, D, E>

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

impl<Output: OutputBuf, A, B, C, D, TA, TB, TC, TD> Serializer<Output, (TA, (TB, (TC, TD)))> for Permute4<A, B, C, D>

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

impl<Output: OutputBuf, A, B, C, TA, TB, TC> Serializer<Output, (TA, (TB, TC))> for Permute3<A, B, C>

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

impl<Output: OutputBuf, A, B, TA, TB> Serializer<Output, (&[TA], TB)> for Repeat<A, B>

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

impl<Output: OutputBuf, A, B, TA, TB> Serializer<Output, (Option<TA>, TB)> for Optional<A, B>

where TA: DeepView, TB: DeepView, A: Serializer<Output, TA>, B: Serializer<Output, TB>,

impl<Output: OutputBuf, A, B, TA, TB> Serializer<Output, Sum<TA, TB>> for Sum<A, B>

where TA: DeepView, TB: DeepView, A: Serializer<Output, TA>, B: Serializer<Output, TB>,

impl<Output: OutputBuf, A, B, TA, TB> Serializer<Output, Sum<TA, TB>> for Choice<A, B>

where TA: DeepView, TB: DeepView, A: Serializer<Output, TA>, B: Serializer<Output, TB>,

impl<Output: OutputBuf, A, B, TA, TB> Serializer<Output, (TA, TB)> for Bind<A, B>

where TA: DeepView, TB: DeepView, A: Serializer<Output, TA>, B::O: Serializer<Output, TB>, B: MapRef<TA, Input = TA::V>,

impl<Output: OutputBuf, A, B, TA, TB> Serializer<Output, (TA, TB)> for Pair<A, B>

where TA: DeepView, TB: DeepView, A: Serializer<Output, TA>, B: Serializer<Output, TB>,

impl<Output: OutputBuf, A, PredFn, T> Serializer<Output, T> for Refined<A, PredFn>

where T: DeepView, A: Serializer<Output, T>, PredFn: SpecPred<T::V>,

impl<Output: OutputBuf, A, T> Serializer<Output, &[T]> for RepeatTillEnd<A>

where A: Serializer<Output, T> + Copy, T: DeepView,

impl<Output: OutputBuf, A, T> Serializer<Output, Option<T>> for Opt<A>

where T: DeepView, A: Serializer<Output, T>,

impl<Output: OutputBuf, A, T> Serializer<Output, Option<T>> for OptionalEnd<A>

where A: Serializer<Output, T>, T: DeepView,

impl<Output: OutputBuf, A, T> Serializer<Output, Vec<T>> for RepeatTillEnd<A>

where A: Serializer<Output, T> + Copy, T: DeepView,

Available on crate feature alloc only.

impl<Output: OutputBuf, C, Elem> Serializer<Output, [Elem]> for SetOfFmt<C>

where Elem: DeepView, C: SpecCombinator<T = <Elem as DeepView>::V> + Serializer<Output, Elem> + Copy,

impl<Output: OutputBuf, C, Elem> Serializer<Output, Vec<Elem>> for SetOfFmt<C>

where Elem: DeepView, C: SpecCombinator<T = <Elem as DeepView>::V> + Serializer<Output, Elem> + Copy,

Available on crate feature alloc only.

impl<Output: OutputBuf, C, T> Serializer<Output, &[T]> for BerSequenceOfFmt<C>

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

impl<Output: OutputBuf, C, T> Serializer<Output, Vec<T>> for BerSequenceOfFmt<C>

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

Available on crate feature alloc only.

impl<Output: OutputBuf, C, T> Serializer<Output, T> for BerSequenceFmt<C>

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

impl<Output: OutputBuf, Content, T, const DER: bool> Serializer<Output, T> for ASN1Fmt<Content, DER>

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

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

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

impl<Output: OutputBuf, Inner, M, MRev, T> Serializer<Output, 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> Serializer<Output, <MRev as Map<&'x T>>::O>,

impl<Output: OutputBuf, Inner, N, T> Serializer<Output, [T]> for RepeatN<Inner, N>

where T: DeepView, Inner: Serializer<Output, T>, N: AsLen,

impl<Output: OutputBuf, Inner, T> Serializer<Output, [T]> for Star<Inner>

where T: DeepView, Inner: Serializer<Output, T>,

impl<Output: OutputBuf, Inner, T> Serializer<Output, T> for Cond<Inner>

where T: DeepView, Inner: Serializer<Output, T>,

impl<Output: OutputBuf, Inner, T> Serializer<Output, T> for Const<Inner, T>

where T: DeepView<V = T>, Inner: Serializer<Output, T>,

impl<Output: OutputBuf, Inner, T, const N: usize> Serializer<Output, [T; N]> for Array<N, Inner>

where T: DeepView, Inner: Serializer<Output, T>,

impl<Output: OutputBuf, Len, Inner, T> Serializer<Output, T> for ExactLen<Inner, Len>

where Len: AsLen, T: DeepView + ?Sized, Inner: Serializer<Output, T> + SpecByteLen<T = T::V>,

impl<Output: OutputBuf, Len: AsLen> Serializer<Output, [u8]> for Varied<Len>

impl<Output: OutputBuf, Of, Tg, TagVal, T> Serializer<Output, T> for SuffixTagged<Of, Tg, TagVal>

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

impl<Output: OutputBuf, P1, P2, T1, T2> Serializer<Output, (T1, T2)> for Permute2<P1, P2>

where T1: DeepView, T2: DeepView, P1: Serializer<Output, T1>, P2: Serializer<Output, T2>,

impl<Output: OutputBuf, T, Inner> Serializer<Output, T> for Named<Inner>

where T: DeepView, Inner: Serializer<Output, T>,

impl<Output: OutputBuf, T, const LIMIT: usize, Body, Param> Serializer<Output, T> for FixWith<LIMIT, Body, Param>

where T: DeepView<V = Body::T>, Param: DeepView<V = Body::Param>, Body: SerializerRecBody<Output, T, EP = Param>,

impl<Output: OutputBuf, Tg, TagVal, Of, T> Serializer<Output, T> for PrefixTagged<Tg, TagVal, Of>

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

impl<Output: OutputBuf, Then, T> Serializer<Output, T> for AndThen<Tail, Then>

where T: DeepView + ?Sized, Then: Serializer<Output, T>,

impl<Output: OutputBuf, const DER: bool> Serializer<Output, bool> for BoolFmt<DER>

impl<Output: OutputBuf, const DER: bool> Serializer<Output, usize> for LengthFmt<DER>

impl<Output: OutputBuf, const DER: bool> Serializer<Output, AnyOwned> for AnyFmt<DER>

Available on crate feature alloc only.

impl<Output: OutputBuf, const DER: bool> Serializer<Output, UtcTime> for UtcTimeFmt<DER>

impl<Output: OutputBuf, const DET: bool> Serializer<Output, CborHead> for CborHeadFmt<DET>

impl<Output: OutputBuf, const LIMIT: usize> Serializer<Output, AnyOwned> for BerAnyFmt<LIMIT>

Available on crate feature alloc only.

impl<Output: OutputBuf, const MINIMAL: bool> Serializer<Output, u64> for Base128Fmt<MINIMAL>

impl<Output: OutputBuf, const MINIMAL: bool> Serializer<Output, u64> for VarInt<MINIMAL>

impl<Output: OutputBuf, const N: usize> Serializer<Output, [u8; N]> for Fixed<N>

impl<Output: OutputBuf, const N: usize> Serializer<Output, [u8]> for Fixed<N>

impl<const LIMIT: usize, Output: OutputBuf> Serializer<Output, Vec<u8>> for BerOctetStringFmt<LIMIT>

Available on crate feature alloc only.

impl<const LIMIT: usize, Output: OutputBuf> Serializer<Output, [u8]> for BerOctetStringFmt<LIMIT>