**Background**

There are a number of compilers and tools for generating R1CS programs for use in zero-knowledge proofs. These tools are generally not formally verified, nor do they generate formal proofs, and it is unsettling to depend on the resulting R1CS for high-value or sensitive transactions. R1CS can be difficult to understand by a human. Additionally, people can write programs directly in R1CS, and those programs are also in need of formal verification.

**Current Status**

We have built an initial formal model of R1CS in the ACL2 theorem prover, and we have formalized a small number of R1CS gadgets. We have also developed prototype technology for lifting R1CS programs into a logical representation in ACL2. This enables people to prove things about the programs, such as functional correctness with respect to a specification written in ACL2.

The underlying technology is based on the ACL2 theorem prover and the Axe verification toolkit, which we have been using and developing for a number of years to verify Java bytecode implementations of cryptographic primitives and other code.

**Proposal**

We would like to improve this technology to handle more R1CS patterns, and to scale the technology so that it can verify larger R1CS programs such as SHA-256, elliptic curve arithmetic, and others.

Along the way, we will develop a standalone tool that can statically check most real-world R1CS programs for: unsatisfiability; unconstrained output variables; non-circuit-derived constructs; and constructs that introduce nondeterminism. Note that this tool will be sound but not complete; the tool will report "unknown" for some inputs.

**Benefits**

Besides the important work of verifying that R1CS circuits correctly implement specified functionality, and the standalone checker mentioned above, this work will enable future tools such as:

Equivalence checking, where an R1CS programmer can try out an optimization idea and get a quick answer on whether the optimized circuit is equivalent.

Automatic optimizer, a tool that applies verified optimization rules to make an equivalent circuit that is smaller. This would be based on our existing high-performance rewriter.

Started

6 months ago

Category

Developer tool

Funding

0.312 / 923 ZEC

Proposal didn’t get funded

Parse and Represent R1CS

Customize and scale Axe toolkit for R1CS

R1CS Static Checker

Larger R1CS Gadgets

Reward: **119.99 ZEC**