pub trait SPRoundTripDpswhere
Self: SpecByteLen + Consistency<Val = Self::T> + SpecParser<PVal = Self::T> + SpecSerializerDps<SValue = Self::T>,{
// Required method
proof fn theorem_serialize_dps_parse_roundtrip(&self, v: Self::T, obuf: Seq<u8>);
// Provided method
open spec fn unambiguous(&self) -> bool { ... }
}Expand description
Serialize-parse roundtrip (DPS).
Serializing a consistent value in DPS style and parsing the result recovers the
original value, consuming exactly byte_len(v) bytes.
This is a low-level trait. Individual combinators in the library prove this directly;
the higher-level property SPRoundTrip is derived via a blanket impl composing this with
GoodSerializer and EquivSerializers.
§Note on user-defined combinators
User-defined combinators should prefer proving this trait to proving SPRoundTrip, as
- it’s a stronger property and proving and implementing this trait would make Rust/Verus auto-derive a proof for
SPRoundTrip; - it makes the combinator composable with the rest of the library, which are all built on this stronger property.
Required Methods§
Sourceproof fn theorem_serialize_dps_parse_roundtrip(&self, v: Self::T, obuf: Seq<u8>)
proof fn theorem_serialize_dps_parse_roundtrip(&self, v: Self::T, obuf: Seq<u8>)
requires
self.unambiguous(),self.consistent(v),({
let ibuf = self.spec_serialize_dps(v, obuf);
let n = self.byte_len(v) as int;
self.spec_parse(ibuf) == Some((n, v))
}),Provided Methods§
Sourceopen spec fn unambiguous(&self) -> bool
open spec fn unambiguous(&self) -> bool
{ true }