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(),

Dyn Compatibility§

This trait is dyn compatible.

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

Implementors§