An R1CS circuit is a set of constraints over a set of variables. Some variables are designated as ‘input variables’, others as ‘output variables’, and the remaining ones we can call ‘auxiliary variables’. For simplicity, let us assume one input variable x, one output variable y, and one auxiliary variable a; the generalization to multiple ones of each category is straightforward.
Logically, a circuit defines a predicate
R(x,y,a)
over the variables. The predicate is true exactly for the values that satisfy all the constraints of the circuit, and false for the other values.
By existentially quantifying the auxiliary variable(s), we obtain an input/output predicate for the circuit
IO(x,y) := [exists a. R(x,y,a)]
This predicate is true exactly for the the input and output values that satisfy all the circuit constraints, for some auxiliary value.
A circuit is typically meant to represent a certain computation from the inputs to the outputs, e.g. a hash function, or a Leo program. Logically, this computation can be represented as a function
y = F(x)
This function can be regarded as the specification for the circuit. It could be a high-level specification written in a theorem prover. Or it could be the mathematical function denoted by a Leo program (more precisely, its main function) according to the Leo operational semantics.
Formally verifying that the circuit satisfies the specification F amounts to proving
forall x,y. [y = F(x)] <==> IO(x,y)
That is, saying that F computes y from x is equivalent to saying that x and y satisfy the circuit constraints (for some a).
The equivalence consists of two parts, examined below.
The ‘if’ part of the equivalence is
forall x,y. IO(x,y) ==> [y = F(x)]
which says that if x and y are part of the I/O relation of the circuit, then y is the output of F on x. That is, when the circuit relates an output to an input, the output is consistent with F on the same input. This property implies, in particular, the functionality of the input/output relation, namely that there is at most one output y for each input x: if both IO(x,y1) and IO(x,y2) hold, the above property implies y1 = F(x) and y2 = F(x), and thus y1 = y2.
Expanding the definition of IO and turning the existential over the antecedent into a universal over the implication, the ‘if’ part of the equivalence can be stated as
forall x,y,a. R(x,y,a) ==> [y = F(x)]
which says that every solution of the constraints of the circuit must have the output consistent with F.
Roughly speaking, the ‘if’ part of the equivalence says that the circuit calculates the right thing, when it calculates something.
The ‘only if’ part of the equivalence is
forall x,y. [y = F(x)] ==> IO(x,y)
which says that if y is the output of F on x, then y and x are part of the input/output relation of the circuit. That is, when the function F computes an output from an input, the input and output values must satisfy the constraints of the circuit (for some value a).
Expanding the definition of IO and substituting F(x) for y, the ‘only if’ part of the equivalence can be stated as
forall x. exists a. R(x,F(x),a)
which says that for every input there must be a choice of a that satisfies all the circuit constraints when the output is the one of the function.
Roughly speaking, the ‘only if’ part of the equivalence says that the circuit always calculates something, i.e. it never fails on an input.
The equivalence, and consequently its ‘if’ and ‘only if’ parts, can be weakened by adding a precondition on the input x. That is, just like in program verification, sometimes we only care about some of the possible input values, not all of them. If P is the precondition predicate, the weaker equivalence has the form
forall x. P(x) ==> [forall y. [y = F(x)] <==> IO(x,y)]
Our main formal verification goal for Leo is that the generated R1CS circuit is correct with respect to the function defined by the Leo program.