Skip to main content

SPRoundTrip

vest_lib::core::proof

Trait SPRoundTrip 

Source 
pub trait SPRoundTrip
where
    Self: SpecByteLen + SpecParser<PVal = Self::T> + SpecSerializer<SVal = Self::T> + Consistency<Val = Self::T>,
{
    // Required method
    proof fn theorem_serialize_parse_roundtrip(&self, v: Self::T);

    // Provided method
    open spec fn sp_roundtrip_inv(&self) -> bool { ... }
}
Expand description

Serialize-parse roundtrip.

Serializing a consistent value and parsing the result recovers v, consuming the entire serialized buffer. Automatically derived for combinators implementing SPRoundTripDps + GoodSerializer + EquivSerializers.

§Note on user-defined combinators

User-defined combinators should prefer proving SPRoundTripDps to proving this trait. See the note on SPRoundTripDps for details.

Required Methods§

Source

proof fn theorem_serialize_parse_roundtrip(&self, v: Self::T)

requires
self.sp_roundtrip_inv(),
self.consistent(v),
ensures
({
    let bytes = self.spec_serialize(v);
    self.spec_parse(bytes) == Some((bytes.len() as int, v))
}),

Provided Methods§

Source

open spec fn sp_roundtrip_inv(&self) -> bool

{ true }

Implementors§