pub trait GoodSerializer: SpecByteLen + SpecSerializer<SVal = Self::T> {
// Required method
broadcast proof fn lemma_serialize_len(&self, v: Self::SVal);
// Provided method
open spec fn serialize_inv(&self) -> bool { ... }
}Expand description
A well-behaved serializer.
Required Methods§
Sourcebroadcast proof fn lemma_serialize_len(&self, v: Self::SVal)
broadcast proof fn lemma_serialize_len(&self, v: Self::SVal)
requires
self.serialize_inv(),self.spec_serialize(v).len() == self.byte_len(v),serialized byte sequence has the expected length.
Provided Methods§
Sourceopen spec fn serialize_inv(&self) -> bool
open spec fn serialize_inv(&self) -> bool
{ true }Optional invariant for serializer-length proofs.
Implementations on Foreign Types§
Source§impl<S: GoodSerializer> GoodSerializer for &S
impl<S: GoodSerializer> GoodSerializer for &S
Source§open spec fn serialize_inv(&self) -> bool
open spec fn serialize_inv(&self) -> bool
{ (*self).serialize_inv() }