pub trait EquivSerializers: SpecSerializer + SpecSerializerDps<SValue = Self::SVal> {
// Required method
proof fn lemma_serialize_equiv_on_empty(&self, v: Self::SVal);
// Provided method
open spec fn equiv_inv(&self) -> bool { ... }
}Expand description
DPS ↔ non-DPS serializer equivalence on the empty buffer.
Sufficient for deriving SPRoundTrip from SPRoundTripDps.
Required Methods§
Sourceproof fn lemma_serialize_equiv_on_empty(&self, v: Self::SVal)
proof fn lemma_serialize_equiv_on_empty(&self, v: Self::SVal)
requires
self.equiv_inv(),self.spec_serialize_dps(v, seq![]) == self.spec_serialize(v),spec_serialize_dps(v, []) == spec_serialize(v).