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[0..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[0..n1] == buf2[0..n2],

Dyn Compatibility§

This trait is dyn compatible.

In older versions of Rust, dyn compatibility was called "object safety".

Implementors§