# What formal verification of R1CS circuits proves

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.

3 Likes

This page https://github.com/acl2/acl2/tree/master/books/kestrel/crypto/r1cs contains some information about R1CS proof tools and methods based on the ACL2 theorem prover. The tools are in that directory, which is part of the ACL2+libraries open-source repository.

3 Likes