Skip to main content

SpecSerializer

Trait SpecSerializer 

Source
pub trait SpecSerializer {
    type SVal;

    // Required method
    spec fn spec_serialize(&self, v: Self::SVal) -> Seq<u8>;
}
Expand description

Serializer specification.

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

Required Associated Types§

Source

type SVal

The type of values to be serialized.

Required Methods§

Source

spec fn spec_serialize(&self, v: Self::SVal) -> Seq<u8>

Serializes v into a fresh byte sequence.

Implementations on Foreign Types§

Source§

impl<S: SpecSerializer> SpecSerializer for &S

Source§

open spec fn spec_serialize(&self, v: Self::SVal) -> Seq<u8>

{ (*self).spec_serialize(v) }
Source§

type SVal = <S as SpecSerializer>::SVal

Implementors§

Source§

impl SpecSerializer for BerEndFmt

Source§

impl SpecSerializer for Integer8Fmt

Source§

impl SpecSerializer for Integer16Fmt

Source§

impl SpecSerializer for BerLengthFmt

Source§

impl SpecSerializer for BmpStringFmt

Source§

impl SpecSerializer for EnumeratedFmt

Source§

type SVal = int

Source§

impl SpecSerializer for Ia5StringFmt

Source§

impl SpecSerializer for IntegerFmt

Source§

type SVal = int

Source§

impl SpecSerializer for ObjectIdentifierFmt

Source§

impl SpecSerializer for PrintableStringFmt

Source§

impl SpecSerializer for TagFmt

Source§

impl SpecSerializer for TeletexStringFmt

Source§

impl SpecSerializer for UniversalStringFmt

Source§

type SVal = Seq<char>

Source§

impl SpecSerializer for Utf8StringFmt

Source§

type SVal = Seq<char>

Source§

impl SpecSerializer for CborInitialFmt

Source§

impl SpecSerializer for Empty

Source§

impl SpecSerializer for Void

Source§

impl SpecSerializer for I8

Source§

impl SpecSerializer for I16Be

Source§

impl SpecSerializer for I16Le

Source§

impl SpecSerializer for I32Be

Source§

impl SpecSerializer for I32Le

Source§

impl SpecSerializer for I64Be

Source§

impl SpecSerializer for I64Le

Source§

impl SpecSerializer for Eof

Source§

impl SpecSerializer for Tail

Source§

type SVal = Seq<u8>

Source§

impl SpecSerializer for U8

Source§

impl SpecSerializer for U16Be

Source§

impl SpecSerializer for U16Le

Source§

impl SpecSerializer for U24Be

Source§

impl SpecSerializer for U24Le

Source§

impl SpecSerializer for U32Be

Source§

impl SpecSerializer for U32Le

Source§

impl SpecSerializer for U64Be

Source§

impl SpecSerializer for U64Le

Source§

impl<A> SpecSerializer for Opt<A>
where A: SpecSerializer,

Source§

impl<A> SpecSerializer for Star<A>
where A: SpecSerializer,

Source§

type SVal = Seq<<A as SpecSerializer>::SVal>

Source§

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

Source§

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

Source§

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

Source§

impl<A, B> SpecSerializer for Bind<A, B>
where A: SpecSerializer, B: SpecMap<Input = A::SVal>, B::Output: SpecSerializer,

Source§

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

Source§

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

Source§

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

Source§

type SVal = (<A as SpecSerializer>::SVal, (<B as SpecSerializer>::SVal, (<C as SpecSerializer>::SVal, <D as SpecSerializer>::SVal)))

Source§

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

Source§

type SVal = (<A as SpecSerializer>::SVal, (<B as SpecSerializer>::SVal, (<C as SpecSerializer>::SVal, (<D as SpecSerializer>::SVal, <E as SpecSerializer>::SVal))))

Source§

impl<A, B, const CHECK: bool> SpecSerializer for Preceded<A, A::SVal, B, CHECK>

Source§

impl<A, B, const CHECK: bool> SpecSerializer for Terminated<A, B, B::SVal, CHECK>

Source§

impl<A, Pred> SpecSerializer for Refined<A, Pred>
where A: SpecSerializer, Pred: SpecPred<A::SVal>,

Source§

impl<A, Then> SpecSerializer for AndThen<A, Then>
where A: SpecSerializer<SVal = Seq<u8>>, Then: SpecSerializer,

Source§

type SVal = <Then as SpecSerializer>::SVal

Source§

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

Source§

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

Source§

type SVal = (Seq<<A as SpecSerializer>::SVal>, <B as SpecSerializer>::SVal)

Source§

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

Source§

type SVal = <C as SpecByteLen>::T

Source§

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

Source§

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

Source§

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

Source§

type SVal = <C as SpecByteLen>::T

Source§

impl<C: SpecSerializer> SpecSerializer for SetOfFmt<C>

Source§

type SVal = Seq<<C as SpecSerializer>::SVal>

Source§

impl<C: SpecSerializer> SpecSerializer for OptionalEnd<C>

Source§

impl<C: SpecSerializer> SpecSerializer for RepeatTillEnd<C>

Source§

type SVal = Seq<<C as SpecSerializer>::SVal>

Source§

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

Source§

type SVal = Seq<<C as SpecSerializer>::SVal>

Source§

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

Source§

type SVal = <Content as SpecParser>::PVal

Source§

impl<F> SpecSerializer for ImplicitlyTaggedFmt<F>

Source§

impl<Field, Rest, const DER: bool> SpecSerializer for DefaultedFmt<Field, Field::SVal, Rest, DER>
where Field: SpecByteLen + SpecSerializer<SVal = Field::T>, Rest: SpecByteLen + SpecSerializer<SVal = Rest::T>,

Source§

type SVal = (<Field as SpecSerializer>::SVal, <Rest as SpecSerializer>::SVal)

Source§

impl<Head, Tail> SpecSerializer for Implicit<Head, Tail>
where Head: SpecSerializer, Tail: DepCombinator<Key = Head::SVal>, Tail::Body: SpecSerializer<SVal = Tail::Val>,

Source§

type SVal = <Tail as DepCombinator>::Val

Source§

impl<Inner> SpecSerializer for Const<Inner, Inner::SVal>
where Inner: SpecSerializer,

Source§

type SVal = <Inner as SpecSerializer>::SVal

Source§

impl<Inner, M> SpecSerializer for Mapped<Inner, M>
where Inner: SpecSerializer, M: SpecMapper<In = Inner::SVal>,

Source§

type SVal = <M as SpecMapper>::Out

Source§

impl<Inner, M> SpecSerializer for TryMap<Inner, M>
where Inner: SpecSerializer, M: SpecMapper<In = Inner::SVal>,

Source§

type SVal = <M as SpecMapper>::Out

Source§

impl<Inner, M, MRev> SpecSerializer for Mapped<Inner, BiMap<M, MRev>>
where Inner: SpecSerializer, M: SpecMap<Input = Inner::SVal>, MRev: SpecMap<Input = M::Output, Output = M::Input>,

Source§

type SVal = <M as SpecMap>::Output

Source§

impl<Inner: SpecSerializer> SpecSerializer for Cond<Inner>

Source§

type SVal = <Inner as SpecSerializer>::SVal

Source§

impl<Inner: SpecSerializer> SpecSerializer for Named<Inner>

Source§

type SVal = <Inner as SpecSerializer>::SVal

Source§

impl<Inner: SpecSerializer> SpecSerializer for Ref<Inner>

Source§

type SVal = <Inner as SpecSerializer>::SVal

Source§

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

Source§

type SVal = <Inner as SpecSerializer>::SVal

Source§

impl<Inner: SpecSerializer, Out> SpecSerializer for Mapped<Inner, FnSpec<(Out,), Inner::SVal>>

Source§

type SVal = Out

Source§

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

Source§

type SVal = Seq<u8>

Source§

impl<Of, Tg> SpecSerializer for SuffixTagged<Of, Tg, Tg::T>
where Tg: SpecByteLen + SpecSerializer<SVal = Tg::T>, Of: SpecSerializer,

Source§

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

Source§

type SVal = <T as DeepView>::V

Source§

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

Source§

type SVal = (<P1 as SpecSerializer>::SVal, <P2 as SpecSerializer>::SVal)

Source§

impl<Repr, Tuple, Nominal> SpecSerializer for Bits<Repr, Tuple, Nominal>
where Repr: SpecByteLen + SpecSerializer<SVal = Repr::T>,

Source§

type SVal = Nominal

Source§

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

Source§

type SVal = <Blen as SpecByteLen>::T

Source§

impl<T> SpecSerializer for BundledSpecs<T>

Source§

type SVal = T

Source§

impl<T> SpecSerializer for SerializerFnSpec<T>

Source§

type SVal = T

Source§

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

Source§

impl<Tg, Of> SpecSerializer for PrefixTagged<Tg, Tg::T, Of>
where Tg: SpecByteLen + SpecSerializer<SVal = Tg::T>, Of: SpecSerializer,

Source§

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

Source§

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

Source§

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

Source§

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

Source§

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

Source§

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

Source§

type SVal = nat

Source§

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

Source§

type SVal = Seq<u8>

Source§

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

Source§

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

Source§

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

Source§

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

Source§

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

Source§

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

Source§

type SVal = Seq<u8>

Source§

impl<const LIMIT: usize, Body, Param> SpecSerializer for FixWith<LIMIT, Body, Param>
where Body: SpecRecBody, Param: DeepView<V = Body::Param>,

Source§

type SVal = <Body as SpecRecBody>::T

Source§

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

Source§

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

Source§

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

Source§

type SVal = nat

Source§

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

Source§

type SVal = Seq<u8>

Source§

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

Source§

type SVal = Seq<u8>

Source§

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

Source§

type SVal = Seq<<C as SpecSerializer>::SVal>

Source§

impl<const NONDETERMINISTIC: bool, A, B> SpecSerializer for Alt<A, B, NONDETERMINISTIC>
where A: SpecSerializer + Consistency<Val = A::SVal>, B: SpecSerializer<SVal = A::SVal> + Consistency<Val = B::SVal>,