Enum StatementTree 

pub enum StatementTree {
    Leaf(Expr),
    And(Vec<StatementTree>),
    Or(Vec<StatementTree>),
    Thresh(usize, Vec<StatementTree>),
}

The statements in the ZKP form a tree. The leaves are basic statements of various kinds; for example, equations or inequalities about Scalars and Points. The interior nodes are combiners: And, Or, or Thresh (with a given constant threshold). A leaf is true if the basic statement it contains is true. An And node is true if all of its children are true. An Or node is true if at least one of its children is true. A Thresh node (with threshold k) is true if at least k of its children are true.

Variants

Leaf(Expr)

And(Vec<StatementTree>)

Or(Vec<StatementTree>)

Thresh(usize, Vec<StatementTree>)

Implementations

impl StatementTree

pub fn parse(expr: &Expr) -> Result<Self>

Parse an Expr (which may contain nested AND, OR, or THRESH) into a StatementTree. For example, the Expr obtained from:

parse_quote! {
   AND (
       C = c*B + r*A,
       D = d*B + s*A,
       OR (
           AND (
               C = c0*B + r0*A,
               D = d0*B + s0*A,
               c0 = d0,
           ),
           AND (
               C = c1*B + r1*A,
               D = d1*B + s1*A,
               c1 = d1 + 1,
           ),
       )
   )
}

would yield a StatementTree::And containing a 3-element vector. The first two elements are StatementTree::Leaf, and the third is StatementTree::Or containing a 2-element vector. Each element is an StatementTree::And with a vector containing 3 StatementTree::Leafs.

Note that AND, OR, and THRESH in the expression are case-insensitive.

pub fn parse_andlist(exprlist: &[Expr]) -> Result<Self>

A convenience function that takes a list of Exprs, and returns the StatementTree that implicitly puts AND around the Exprs. This is useful because a common thing to do is to just write a list of Exprs in the top-level macro invocation, having the semantics of “all of these must be true”.

pub fn leaves(&self) -> Vec<&Expr>

Return a vector of references to all of the leaf expressions in the StatementTree

pub fn leaves_mut(&mut self) -> Vec<&mut Expr>

Return a vector of mutable references to all of the leaf expressions in the StatementTree

pub fn leaves_st_mut(&mut self) -> Vec<&mut StatementTree>

Return a vector of mutable references to all of the leaves in the StatementTree

pub fn check_disjunction_invariant(&self, vars: &VarDict) -> Result<()>

Verify whether the StatementTree satisfies the disjunction invariant.

A disjunction node is an Or or Thresh node in the StatementTree.

A disjunction branch is a subtree rooted at a non-disjunction node that is the child of a disjunction node or at the root of the StatementTree.

The disjunction invariant is that a private variable (which is necessarily a Scalar since there are no private Point variables) that appears in a disjunction branch cannot also appear outside of that disjunction branch.

For example, if all of the lowercase variables are private Scalars, the StatementTree created from:

   AND (
       C = c*B + r*A,
       D = d*B + s*A,
       OR (
           AND (
               C = c0*B + r0*A,
               D = d0*B + s0*A,
               c0 = d0,
           ),
           AND (
               C = c1*B + r1*A,
               D = d1*B + s1*A,
               c1 = d1 + 1,
           ),
       )
   )

satisfies the disjunction invariant, but

   AND (
       C = c*B + r*A,
       D = d*B + s*A,
       OR (
           AND (
               D = d0*B + s0*A,
               c = d0,
           ),
           AND (
               C = c1*B + r1*A,
               D = d1*B + s1*A,
               c1 = d1 + 1,
           ),
       )
   )

does not, because c appears in the first child of the OR and also outside of the OR entirely. Indeed, the reason to write the first expression above rather than the more natural

   AND (
       C = c*B + r*A,
       D = d*B + s*A,
       OR (
           c = d,
           c = d + 1,
       )
   )

is exactly that the invariant must be satisfied.

If you don’t know that your StatementTree already satisfies the invariant, call enforce_disjunction_invariant, which will transform the StatementTree so that it does (and also call this check_disjunction_invariant function as a sanity check).

pub fn for_each_disjunction_branch( &mut self, closure: &mut dyn FnMut(&mut StatementTree, &[usize]) -> Result<()>, ) -> Result<()>

Call the supplied closure for each disjunction branch of the given StatementTree (including the root, if the root is a non-disjunction node).

The calls are in preorder traversal (parents before children). The given closure will be called with the root of each disjunction branch as well as a slice of usize indicating the path through the StatementTree to that disjunction branch. The disjunction branch at the root has path []. The disjunction branch rooted at, say, the 2nd child of an Or node in the root disjunction branch will have path [2]. The disjunction branch rooted at the 1st child of an Or node in that disjunction branch will have path [2,1], and so on.

Abort and return Err if any call to the closure returns Err.

pub fn for_each_disjunction_branch_leaf( &mut self, closure: &mut dyn FnMut(&mut StatementTree) -> Result<()>, ) -> Result<()>

Call the supplied closure for each StatementTree::Leaf of the given disjunction branch.

Abort and return Err if any call to the closure returns Err.

pub fn disjunction_branch_priv_scalars( &mut self, vars: &VarDict, ) -> HashSet<Ident>

Produce a HashSet of the private Scalars that appear in any leaf of the given disjunction branch.

pub fn flatten_ands(&mut self)

Flatten nested And nodes in a StatementTree.

The underlying sigma-proofs crate can share Scalars across statements that are direct children of the same And node, but not in nested And nodes.

So a StatementTree like this:

   AND (
       C = x*B + r*A,
       AND (
           D = x*B + s*A,
           E = x*B + t*A,
       ),
   )

Needs to be flattened to:

   AND (
       C = x*B + r*A,
       D = x*B + s*A,
       E = x*B + t*A,
   )

pub fn leaf_true() -> StatementTree

Produce a StatementTree that represents the constant true

pub fn is_leaf_true(&self) -> bool

Test if the given StatementTree represents the constant true

pub fn dump(&self)

Trait Implementations

impl Clone for StatementTree

fn clone(&self) -> StatementTree

Returns a duplicate of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl Debug for StatementTree

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl PartialEq for StatementTree

fn eq(&self, other: &StatementTree) -> bool

Tests for self and other values to be equal, and is used by ==.

fn ne(&self, other: &Rhs) -> bool

Tests for !=. The default implementation is almost always sufficient, and should not be overridden without very good reason.

impl Eq for StatementTree

impl StructuralPartialEq for StatementTree