pub trait SpecSerializerDps {
type SValue;
// Required method
spec fn spec_serialize_dps(&self, v: Self::SValue, obuf: Seq<u8>) -> Seq<u8>;
}Expand description
Destination-passing style (DPS) serializer specification.
See crate::core::proof::EquivSerializers for its relationship to SpecSerializer.
Required Associated Types§
Required Methods§
Sourcespec fn spec_serialize_dps(&self, v: Self::SValue, obuf: Seq<u8>) -> Seq<u8>
spec fn spec_serialize_dps(&self, v: Self::SValue, obuf: Seq<u8>) -> Seq<u8>
Serializes v by prepending its encoding onto obuf.