goto

During a proof, due to case distinctions, the proof tree may contain several open goals (unsolved leafs). This rule allows you to change the current working goal:

goto n.

where n must be an integer between $1$ and the number of open goals.

simplify

This rule has no additional arguments:

simplify.

It simplifies the current working goal. Internally, it performs an abstraction of the system of equations to get rid of $\forall$ and $\sum$ symbols, obtaining abstracted Laurent polynomials. Later, it uses Gröbner Basis reductions to simplify these abstracted Laurent polynomials. Finally, it undoes the abstraction, obtaining a simplified system of equations which is equivalent to the original one. This algorithm also unifies the index variable names.
We show a small example of simplification: $$ \begin{array}{ll} \exists j_{1}. & \\ \sigma + \left( \sum_{j_{3} \not \in \{ j_{1}\}} \rho_{j_{1}}\cdot \rho'_{j_{3}} \right)= 0 & \land \\ \forall j_{2}\not \in \{ j_{1} \}. \rho_{j_{1}}\cdot \rho'_{j_{2}} = 0 & \\ \end{array} \hspace{1cm} \longrightarrow \hspace{1cm} \begin{array}{ll} \exists i. & \\ \sigma = 0 & \land \\ \forall j\not \in \{ i \}. \rho_{i}\cdot \rho'_{j} = 0 & \\ \end{array} $$

contradiction

This rule is used when a contradiction was found.

contradiction.

Every contradiction can be reduced to $1=0$ or $0\neq 0$. If the current goal has been simplified to a contradiction, this rule removes the goal from the goals list. Otherwise, an error message will be shown while applying the rule. If it was the last goal, this command finishes the proof.

coeff

This rule exploits the fact that if a polynomial is equal to zero, then when interpreting the polynomial as a polynomial over uniform variables, the coefficients for all monomials must be zero. The rule could be summarized as follows: $$ \begin{array}{ll} \dots & \land \\ {\cal E} = 0 & \land\\ \dots & \\ \end{array} \ \ \ \ \ \ \longrightarrow \ \ \ \ \ \ \begin{array}{ll} \dots & \land\\ {\cal E} = 0 & \land\\ \forall i_{1},\dots,i_{k}. {\sf Coeff}_{\cal M}({\cal E}) = 0 & \land\\ \dots \\ \end{array} $$ It introduces a new equation, where the monomial ${\cal M}$ depends on index variables $i_{1},\dots,i_{k}$ and the expression ${\cal E}$ does not contain any of these index variables. The syntax is the following:

coeff (M) n.

where $M$ is a monomial (containing only uniform variables) and n is an integer corresponding to the equation number in the system of equations.

extract_coeffs

This rule has no additional arguments:

extract_coeffs.

It applies the previous rule to all possible equalities and all possible (and relevant) monomials.

simp_Coeff

This rule is part of the simplify routine. It simplifies coeff expressions in the natural way. A simple example of its behaviour is the following: $$ \begin{array}{lll} 1. & a\cdot X + b\cdot Y + c\cdot X\cdot Y = 0 & \\ \end{array} $$ we apply coeff (X*Y) 1. and we get, $$ \begin{array}{lll} 1. & a\cdot X + b\cdot Y + c\cdot X\cdot Y = 0 & \land \\ 2. & {\sf Coeff}_{X\cdot Y}(a\cdot X + b\cdot Y + c\cdot X\cdot Y) = 0 & \\ \end{array} $$ after simp_Coeff. we get $$ \begin{array}{lll} 1. & a\cdot X + b\cdot Y + c\cdot X\cdot Y = 0 & \land \\ 2. & c = 0 & \\ \end{array} $$ In practice, this rule is more complicated due to the fact that the adversary may be adaptive. As explained above, we distinguish between uniform variables and handle variables. All variables in the experiment, but Oracle inputs, are uniform variables. However, Oracle inputs must be instantiated (possibly in an adaptive way) by the adversary. Oracle input variables (handle variables) and depend at the same time on other handle variables (corresponding to earlier queries to the Oracle) and uniform variables. They ultimately depend only on uniform variables, but, since the number of queries is not fixed, these relation is not bounded.
Despite this issue, in some cases it is possible to prove that a particular handle variable does not contain certain monomial. When this happens, it is possible to simplify a Coeff to $0$.

case_distinction

This rule is used to perform case distinctions on the parameters. The syntax is:

case_distinction p.

where $p$ is a parameter.

• If it is a non-indexed parameter or an indexed parameter whose index is existentially quantified, the current goal is divided into two different goals, where one of them includes the equation $p = 0$ and the other one includes the equation $p \neq 0$.
• If it is an indexed parameter whose index is not existentially quantified, the current goal is divided into two different goals, where one of them includes the equation $\forall i. p_{i} = 0$ and the other one includes the equation $p_{i^{*}} \neq 0$ where $i^{*}$ is a new existentially quantified index variable.

split_in_factors

The syntax is:

split_in_factors n.

where $n$ is an integer, corresponding to the number of an equality equation. If the left hand side of these equality (the right hand side is $0$) can be expressed as the product of more than one term, i.e. ${\cal E} = 0$ can be expressed as ${\cal E_{1}}\cdot {\cal E_{2}}\cdots {\cal E}_{k} = 0$, then the current goal is divided into $k$ goals where the $i$-th new goal replaces the mentioned equation by ${\cal E}_{i} = 0$.

divide_by_param

The syntax is:

divide_by_param p.

where $p$ is a parameter.
Under the assumption that a parameter is not null, we can divide by it. Therefore, to apply this rule for parameter $p$, the equation $p \neq 0$ must appear in the system. This rule applies division by $p$ in all equations where $p$ is a common factor of every term. (All the rules are designed to avoid dealing with negative degree parameters).

assure_Laurent

The syntax is:

assure_Laurent n.

where $n$ corresponds to an equation number. This rule exploits the fact that a handle variable must be a Laurent polynomial on uniform variables to derive new equations on the parameters.
As an example, let $X,Y$ be uniform variables and let $M$ be a handle variable. Let $\sigma$ be a parameter. The equation $X\cdot M + \sigma\cdot Y \cdot M + \sigma - 1 = 0$ is equivalent to $$ M = \frac{1-\sigma}{X+\sigma \cdot Y} $$ and asuming that $M$ must be a Laurent polynomial, we can derive new equations on $\sigma$. In particular, in this case we have $\sigma = 0 \ \lor \ \sigma = 1$. Otherwise $M$ is a rational expression different from a Laurent polynomial.