Skip to main content

NonAmbiguous

vest_lib::core::proof

Trait NonAmbiguous 

Source 
pub trait NonAmbiguous
where
    Self: Consistency + SpecSerializer<SVal = Self::Val>,
{
    // Required method
    proof fn lemma_serialize_injective(&self, v1: Self::Val, v2: Self::Val);

    // Provided methods
    open spec fn nonamb_inv(&self) -> bool { ... }
    fn corollary_serialize_injective_contrapositive(
        &self,
        v1: Self::Val,
        v2: Self::Val,
    ) { ... }
}
Expand description

Serializer unambiguity (injectivity on consistent values).

Two different consistent values cannot serialize to the same bytes. This rules out ambiguity in the value-to-wire direction and follows automatically from SPRoundTrip.

Required Methods§

Source

proof fn lemma_serialize_injective(&self, v1: Self::Val, v2: Self::Val)

requires
self.nonamb_inv(),
self.consistent(v1),
self.consistent(v2),
ensures
self.spec_serialize(v1) == self.spec_serialize(v2) ==> v1 == v2,

Proves that equal serializations imply equal values.

Provided Methods§

Source

open spec fn nonamb_inv(&self) -> bool

{ true }

Side conditions needed by the injectivity proof.

Source

proof fn corollary_serialize_injective_contrapositive( &self, v1: Self::Val, v2: Self::Val, )

requires
self.nonamb_inv(),
self.consistent(v1),
self.consistent(v2),
ensures
v1 != v2 ==> self.spec_serialize(v1) != self.spec_serialize(v2),

Equivalent contrapositive: distinct values have distinct serializations.

Implementors§