Skip to main content

AdmitsUniqueVal

vest_lib::core::spec

Trait AdmitsUniqueVal 

Source 
pub trait AdmitsUniqueVal: Consistency {
    // Required method
    proof fn lemma_unique_consistent_val(&self, v1: Self::Val, v2: Self::Val);
}
Expand description

Combinators whose consistency admits at most one value.

Used by e.g., crate::combinators::Preceded and crate::combinators::Terminated to recover non-malleability when the discarded side is not checked explicitly.

Required Methods§

Source

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

ensures
self.consistent(v1) && self.consistent(v2) ==> v1 == v2,

Any two consistent values must be equal.

Implementors§