Skip to main content

PSRoundTrip

vest_lib::core::proof

Trait PSRoundTrip 

Source 
pub trait PSRoundTrip
where
    Self: SpecByteLen + SpecParser<PVal = Self::T> + SpecSerializer<SVal = Self::T>,
{
    // Required method
    proof fn theorem_parse_serialize_roundtrip(&self, ibuf: Seq<u8>);

    // Provided methods
    open spec fn ps_roundtrip_inv(&self) -> bool { ... }
    fn corollary_parse_non_malleable(&self, buf1: Seq<u8>, buf2: Seq<u8>) { ... }
}
Expand description

Parse-serialize roundtrip.

Parsing a buffer and serializing the result reproduces the consumed bytes.

Automatically derived for combinators implementing SPRoundTrip + NonMalleable.

User-defined combinators can also prove this directly.

Required Methods§

Source

proof fn theorem_parse_serialize_roundtrip(&self, ibuf: Seq<u8>)

requires
self.ps_roundtrip_inv(),
ensures
self.spec_parse(ibuf) matches Some((n, v)) ==> self.spec_serialize(v) == ibuf.take(n),

Provided Methods§

Source

open spec fn ps_roundtrip_inv(&self) -> bool

{ true }
Source

proof fn corollary_parse_non_malleable(&self, buf1: Seq<u8>, buf2: Seq<u8>)

requires
self.ps_roundtrip_inv(),
ensures
self
    .spec_parse(
        buf1,
    ) matches Some(
    (n1, v1),
) ==> self
    .spec_parse(
        buf2,
    ) matches Some((n2, v2)) ==> v1 == v2 ==> buf1.take(n1) == buf2.take(n2),

Implementors§