Skip to main content

LeafNonMalleable

vest_lib::core::proof

Trait LeafNonMalleable 

Source 
pub trait LeafNonMalleable:
    Leaf
    + SoundParser
    + NonMalleable {
    // Required method
    proof fn nonmal_leaf_inv(&self);
}
Expand description

Similar to Leaf, but also includes the parser soundness and non-malleability properties.

Required Methods§

Source

proof fn nonmal_leaf_inv(&self)

ensures
self.unambiguous(),
self.safe_inv(),
self.sound_inv(),
self.nonmal_inv(),
self.serialize_inv(),
self.serialize_dps_inv(),
self.equiv_general_inv(),

Implementors§