pub trait EquivSerializersGeneral: SpecSerializer + SpecSerializerDps<SValue = Self::SVal> {
// Required method
proof fn lemma_serialize_equiv(&self, v: Self::SVal, obuf: Seq<u8>);
// Provided method
open spec fn equiv_general_inv(&self) -> bool { ... }
}Expand description
Full DPS ↔ non-DPS serializer equivalence for any output buffer.
See EquivSerializers for the weaker empty-buffer variant.
Required Methods§
Sourceproof fn lemma_serialize_equiv(&self, v: Self::SVal, obuf: Seq<u8>)
proof fn lemma_serialize_equiv(&self, v: Self::SVal, obuf: Seq<u8>)
requires
self.equiv_general_inv(),self.spec_serialize_dps(v, obuf) == self.spec_serialize(v) + obuf,spec_serialize_dps(v, obuf) == spec_serialize(v) + obuf.
Provided Methods§
Sourceopen spec fn equiv_general_inv(&self) -> bool
open spec fn equiv_general_inv(&self) -> bool
{ true }