Trait SpecSerializerDps 

pub trait SpecSerializerDps {
    type SValue;

    // Required method
    spec fn spec_serialize_dps(&self, v: Self::SValue, obuf: Seq<u8>) -> Seq<u8>;
}

Destination-passing style (DPS) serializer specification.

See crate::core::proof::EquivSerializers for its relationship to SpecSerializer.

Required Associated Types

type SValue

The type of values to be serialized.

Required Methods

spec fn spec_serialize_dps(&self, v: Self::SValue, obuf: Seq<u8>) -> Seq<u8>

Serializes v by prepending its encoding onto obuf.

Dyn Compatibility

This trait is dyn compatible.

In older versions of Rust, dyn compatibility was called "object safety".

Implementors

impl SpecSerializerDps for BerEndFmt

type SValue = ()

impl SpecSerializerDps for BerLengthFmt

type SValue = BerLength

impl SpecSerializerDps for BmpStringFmt

type SValue = BmpStringSpec

impl SpecSerializerDps for CborInitialFmt

type SValue = CborInitial

impl SpecSerializerDps for Empty

type SValue = ()

impl SpecSerializerDps for EnumeratedFmt

type SValue = int

impl SpecSerializerDps for Eof

type SValue = ()

impl SpecSerializerDps for I8

type SValue = i8

impl SpecSerializerDps for I16Be

type SValue = i16

impl SpecSerializerDps for I16Le

type SValue = i16

impl SpecSerializerDps for I32Be

type SValue = i32

impl SpecSerializerDps for I32Le

type SValue = i32

impl SpecSerializerDps for I64Be

type SValue = i64

impl SpecSerializerDps for I64Le

type SValue = i64

impl SpecSerializerDps for Ia5StringFmt

type SValue = Ia5StringSpec

impl SpecSerializerDps for Integer8Fmt

type SValue = i8

impl SpecSerializerDps for Integer16Fmt

type SValue = i16

impl SpecSerializerDps for IntegerFmt

type SValue = int

impl SpecSerializerDps for ObjectIdentifierFmt

type SValue = ObjectIdentifierSpec

impl SpecSerializerDps for PrintableStringFmt

type SValue = PrintableStringSpec

impl SpecSerializerDps for TagFmt

type SValue = Tag

impl SpecSerializerDps for Tail

type SValue = Seq<u8>

impl SpecSerializerDps for TeletexStringFmt

type SValue = TeletexStringSpec

impl SpecSerializerDps for U8

type SValue = u8

impl SpecSerializerDps for U16Be

type SValue = u16

impl SpecSerializerDps for U16Le

type SValue = u16

impl SpecSerializerDps for U24Be

type SValue = u32

impl SpecSerializerDps for U24Le

type SValue = u32

impl SpecSerializerDps for U32Be

type SValue = u32

impl SpecSerializerDps for U32Le

type SValue = u32

impl SpecSerializerDps for U64Be

type SValue = u64

impl SpecSerializerDps for U64Le

type SValue = u64

impl SpecSerializerDps for UniversalStringFmt

type SValue = Seq<char>

impl SpecSerializerDps for Utf8StringFmt

type SValue = Seq<char>

impl SpecSerializerDps for Void

type SValue = ExecNever

impl<A, B, C, D, E> SpecSerializerDps for Permute5<A, B, C, D, E>

where A: SpecSerializerDps, B: SpecSerializerDps, C: SpecSerializerDps, D: SpecSerializerDps, E: SpecSerializerDps,

type SValue = (<A as SpecSerializerDps>::SValue, (<B as SpecSerializerDps>::SValue, (<C as SpecSerializerDps>::SValue, (<D as SpecSerializerDps>::SValue, <E as SpecSerializerDps>::SValue))))

impl<A, B, C, D> SpecSerializerDps for Permute4<A, B, C, D>

where A: SpecSerializerDps, B: SpecSerializerDps, C: SpecSerializerDps, D: SpecSerializerDps,

type SValue = (<A as SpecSerializerDps>::SValue, (<B as SpecSerializerDps>::SValue, (<C as SpecSerializerDps>::SValue, <D as SpecSerializerDps>::SValue)))

impl<A, B, C> SpecSerializerDps for Permute3<A, B, C>

where A: SpecSerializerDps, B: SpecSerializerDps, C: SpecSerializerDps,

type SValue = (<A as SpecSerializerDps>::SValue, (<B as SpecSerializerDps>::SValue, <C as SpecSerializerDps>::SValue))

impl<A, B, const CHECK: bool> SpecSerializerDps for Preceded<A, A::SValue, B, CHECK>

where A: SpecSerializerDps, B: SpecSerializerDps,

type SValue = <B as SpecSerializerDps>::SValue

impl<A, B, const CHECK: bool> SpecSerializerDps for Terminated<A, B, B::SValue, CHECK>

where A: SpecSerializerDps, B: SpecSerializerDps,

type SValue = <A as SpecSerializerDps>::SValue

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

where A: SpecSerializerDps, B: SpecMap<Input = A::SValue>, B::Output: SpecSerializerDps,

type SValue = (<A as SpecSerializerDps>::SValue, <<B as SpecMap>::Output as SpecSerializerDps>::SValue)

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

where A: SpecSerializerDps, B: SpecSerializerDps,

type SValue = Sum<<A as SpecSerializerDps>::SValue, <B as SpecSerializerDps>::SValue>

impl<A, B> SpecSerializerDps for Pair<A, B>

where A: SpecSerializerDps, B: SpecSerializerDps,

type SValue = (<A as SpecSerializerDps>::SValue, <B as SpecSerializerDps>::SValue)

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

where A: SpecSerializerDps, B: SpecSerializerDps,

type SValue = (<A as SpecSerializerDps>::SValue, <B as SpecSerializerDps>::SValue)

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

where A: SpecSerializerDps, B: SpecSerializerDps,

type SValue = Sum<<A as SpecSerializerDps>::SValue, <B as SpecSerializerDps>::SValue>

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

where A: SpecSerializerDps, Pred: SpecPred<A::SValue>,

type SValue = <A as SpecSerializerDps>::SValue

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

where A: SpecSerializerDps<SValue = Seq<u8>>, Then: SpecSerializerDps,

type SValue = <Then as SpecSerializerDps>::SValue

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

type SValue = (Option<<A as SpecSerializerDps>::SValue>, <B as SpecSerializerDps>::SValue)

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

type SValue = (Seq<<A as SpecSerializerDps>::SValue>, <B as SpecSerializerDps>::SValue)

impl<A> SpecSerializerDps for Opt<A>

where A: SpecSerializerDps,

type SValue = Option<<A as SpecSerializerDps>::SValue>

impl<A> SpecSerializerDps for Star<A>

where A: SpecSerializerDps,

type SValue = Seq<<A as SpecSerializerDps>::SValue>

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

type SValue = <C as SpecByteLen>::T

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

type SValue = <C as SpecByteLen>::T

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

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

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

type SValue = Seq<<C as SpecSerializerDps>::SValue>

impl<C: SpecSerializerDps> SpecSerializerDps for OptionalEnd<C>

type SValue = Option<<C as SpecSerializerDps>::SValue>

impl<C: SpecSerializerDps> SpecSerializerDps for RepeatTillEnd<C>

type SValue = Seq<<C as SpecSerializerDps>::SValue>

impl<C: SpecSerializerDps> SpecSerializerDps for SetOfFmt<C>

type SValue = Seq<<C as SpecSerializerDps>::SValue>

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

type SValue = <Content as SpecParser>::PVal

impl<F> SpecSerializerDps for ImplicitlyTaggedFmt<F>

where F: Retaggable + SpecSerializerDps,

type SValue = <F as SpecSerializerDps>::SValue

impl<Field, Rest, const DER: bool> SpecSerializerDps for DefaultedFmt<Field, Field::SValue, Rest, DER>

where Field: SpecByteLen + SpecSerializerDps<SValue = Field::T>, Rest: SpecByteLen + SpecSerializerDps<SValue = Rest::T>,

type SValue = (<Field as SpecSerializerDps>::SValue, <Rest as SpecSerializerDps>::SValue)

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

where Head: SpecSerializerDps, Tail: DepCombinator<Key = Head::SValue>, Tail::Body: SpecSerializerDps<SValue = Tail::Val>,

type SValue = <Tail as DepCombinator>::Val

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

where Inner: SpecSerializerDps, M: SpecMap<Input = Inner::SValue>, MRev: SpecMap<Input = M::Output, Output = M::Input>,

type SValue = <M as SpecMap>::Output

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

where Inner: SpecSerializerDps, M: SpecMapper<In = Inner::SValue>,

type SValue = <M as SpecMapper>::Out

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

where Inner: SpecSerializerDps, M: SpecMapper<In = Inner::SValue>,

type SValue = <M as SpecMapper>::Out

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

type SValue = <Inner as SpecSerializerDps>::SValue

impl<Inner: SpecSerializerDps, Out> SpecSerializerDps for Mapped<Inner, FnSpec<(Out,), Inner::SValue>>

type SValue = Out

impl<Inner: SpecSerializerDps> SpecSerializerDps for Cond<Inner>

type SValue = <Inner as SpecSerializerDps>::SValue

impl<Inner: SpecSerializerDps> SpecSerializerDps for Named<Inner>

type SValue = <Inner as SpecSerializerDps>::SValue

impl<Inner: SpecSerializerDps> SpecSerializerDps for Ref<Inner>

type SValue = <Inner as SpecSerializerDps>::SValue

impl<Inner> SpecSerializerDps for Const<Inner, Inner::SValue>

where Inner: SpecSerializerDps,

type SValue = <Inner as SpecSerializerDps>::SValue

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

type SValue = Seq<u8>

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

where Tg: SpecByteLen + SpecSerializerDps<SValue = Tg::T>, Of: SpecSerializerDps,

type SValue = <Of as SpecSerializerDps>::SValue

impl<P1, P2> SpecSerializerDps for Permute2<P1, P2>

where P1: SpecSerializerDps, P2: SpecSerializerDps,

type SValue = (<P1 as SpecSerializerDps>::SValue, <P2 as SpecSerializerDps>::SValue)

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

where Repr: SpecByteLen + SpecSerializerDps<SValue = Repr::T>,

type SValue = Nominal

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

type SValue = <C as SpecSerializerDps>::SValue

impl<T> SpecSerializerDps for BundledSpecs<T>

type SValue = T

impl<T> SpecSerializerDps for SerializerDPSFnSpec<T>

type SValue = T

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

where Tg: SpecByteLen + SpecSerializerDps<SValue = Tg::T>, Of: SpecSerializerDps,

type SValue = <Of as SpecSerializerDps>::SValue

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

type SValue = AnySpec

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

type SValue = BitStringSpec

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

type SValue = bool

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

type SValue = GeneralizedTimeSpec

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

type SValue = usize

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

type SValue = nat

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

type SValue = Seq<u8>

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

type SValue = UtcTime

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

type SValue = CborValueSpec

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

type SValue = CborHead

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

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

type SValue = <Body as SpecRecBody>::T

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

type SValue = AnySpec

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

type SValue = BitStringSpec

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

type SValue = Seq<u8>

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

type SValue = nat

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

type SValue = u64

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

type SValue = u64

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

type SValue = Seq<<C as SpecSerializerDps>::SValue>

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

type SValue = Seq<u8>

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

type SValue = Seq<u8>

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

where A: SpecSerializerDps + Consistency<Val = A::SValue>, B: SpecSerializerDps<SValue = A::SValue> + Consistency<Val = B::SValue>,

type SValue = <A as SpecSerializerDps>::SValue