pub trait NonTailFmt: SpecByteLen + SpecSerializerDps<SValue = Self::T> {
// Required methods
proof fn lemma_serialize_dps_prepend(&self, v: Self::SValue, obuf: Seq<u8>);
proof fn lemma_serialize_dps_len(&self, v: Self::SValue, obuf: Seq<u8>);
// Provided method
open spec fn serialize_dps_inv(&self) -> bool { ... }
}Expand description
A non-tail format combinator would allow for things to be serialized after itself.
§Notable formats that are not non-tail (i.e., tail formats)
Required Methods§
Sourceproof fn lemma_serialize_dps_prepend(&self, v: Self::SValue, obuf: Seq<u8>)
proof fn lemma_serialize_dps_prepend(&self, v: Self::SValue, obuf: Seq<u8>)
requires
self.serialize_dps_inv(),exists |new_buf: Seq<u8>| self.spec_serialize_dps(v, obuf) == new_buf + obuf,The serializer prepends to obuf (so it will leave obuf intact, no truncation, corruption, etc.).
Another way to think about this is that the format allows for trailing bytes after itself, whereas a tail format would only allow for leading bytes before itself.
Sourceproof fn lemma_serialize_dps_len(&self, v: Self::SValue, obuf: Seq<u8>)
proof fn lemma_serialize_dps_len(&self, v: Self::SValue, obuf: Seq<u8>)
requires
self.serialize_dps_inv(),self.spec_serialize_dps(v, obuf).len() - obuf.len() == self.byte_len(v),number of bytes prepended equals byte_len(v).
Provided Methods§
Sourceopen spec fn serialize_dps_inv(&self) -> bool
open spec fn serialize_dps_inv(&self) -> bool
{ true }Optional invariant for DPS serializer proofs.