Skip to main content

Leaf

vest_lib::core::proof

Trait Leaf 

Source 
pub trait Leaf:
    SafeParser
    + GoodSerializer
    + NonTailFmt
    + SPRoundTripDps
    + EquivSerializersGeneral {
    // Required method
    proof fn leaf_inv(&self);
}
Expand description

This is a marker trait for combinators that are “leaves” in the combinator hierarchy.

A “leaf” combinator does not expose any non-trivial preconditions on its correctness and security properties.

Built-in combinators that are “leaves” include Fixed, Varied, U8/U16Le/U32Le, FixWith, Empty, and Void.

In addition, any derived/composed combinator proven to satisfy Leaf::leaf_inv can also be marked as a leaf combinator.

Required Methods§

Source

proof fn leaf_inv(&self)

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

Implementors§