acir

Module circuit

Source
Expand description

§The Abstract Circuit Intermediate Representation (ACIR)

The purpose of ACIR is to make the link between a generic proving system, such as Aztec’s Barretenberg, and a frontend, such as Noir, which describes user specific computations.

More precisely, Noir is a programming language for zero-knowledge proofs (ZKP) which allows users to write programs in an intuitive way using a high-level language close to Rust syntax. Noir is able to generate a proof of execution of a Noir program, using an external proving system. However, proving systems use specific low-level constrain-based languages. Similarly, frontends have their own internal representation in order to represent user programs.

The goal of ACIR is to provide a generic open-source intermediate representation close to proving system ‘languages’, but agnostic to a specific proving system, that can be used both by proving system as well as a target for frontends. So, at the end of the day, an ACIR program is just another representation of a program, dedicated to proving systems.

§ACIR

ACIR stands for Abstract Circuit Intermediate Representation:

  • abstract circuit: circuits are a simple computation model where basic computation units, named gates, are connected with wires. Data flows through the wires while gates compute output wires based on their input. More formally, they are directed acyclic graphs (DAG) where the vertices are the gates and the edges are the wires. Due to the immutability nature of the wires (their value does not change during an execution), they are well suited for describing computations for ZKPs. Furthermore, we do not lose any expressiveness when using a circuit as it is well known that any bounded computation can be translated into an arithmetic circuit (i.e a circuit with only addition and multiplication gates). The term abstract here simply means that we do not refer to an actual physical circuit (such as an electronic circuit). Furthermore, we will not exactly use the circuit model, but another model even better suited to ZKPs, the constraint model (see below).
  • intermediate representation: The ACIR representation is intermediate because it lies between a frontend and its proving system. ACIR bytecode makes the link between noir compiler output and the proving system backend input.

§The constraint model

The first step for generating a proof that a specific program was executed, is to execute this program. Since the proving system is going to handle ACIR programs, we need in fact to execute an ACIR program, using the user-supplied inputs.

In ACIR terminology, the gates are called opcodes and the wires are called partial witnesses. However, instead of connecting the opcodes together through wires, we create constraints: an opcode constraints together a set of wires. This constraint model trivially supersedes the circuit model. For instance, an addition gate output_wire = input_wire_1 + input_wire_2 can be expressed with the following arithmetic constraint: output_wire - (input_wire_1 + input_wire_2) = 0

§Solving

Because of these constraints, executing an ACIR program is called solving the witnesses. From the witnesses representing the inputs of the program, whose values are supplied by the user, we find out what the other witnesses should be by executing/solving the constraints one-by-one in the order they were defined.

For instance, if input_wire_1 and input_wire_2 values are supplied as 3 and 8, then we can solve the opcode output_wire - (input_wire_1 + input_wire_2) = 0 by saying that output_wire is 11.

In summary, the workflow is the following:

  1. user program -> (compilation) ACIR, a list of opcodes which constrain (partial) witnesses
  2. user inputs + ACIR -> (execution/solving) assign values to all the (partial) witnesses
  3. witness assignment + ACIR -> (proving system) proof

Although the ordering of opcode does not matter in theory, since a system of equations is not dependent on its ordering, in practice it matters a lot for the solving (i.e the performance of the execution). ACIR opcodes must be ordered so that each opcode can be resolved one after the other.

The values of the witnesses lie in the scalar field of the proving system. We will refer to it as FieldElement or ACIR field. The proving system needs the values of all the partial witnesses and all the constraints in order to generate a proof.

Note: The value of a partial witness is unique and fixed throughout a program execution, although in some rare cases, multiple values are possible for a same execution and witness (when there are several valid solutions to the constraints). Having multiple possible values for a witness may indicate that the circuit is not safe.

Note: Why do we use the term partial witnesses? It is because the proving system may create other constraints and witnesses (especially with BlackBoxFuncCall, see below). A proof refers to a full witness assignment and its constraints. ACIR opcodes and their partial witnesses are still an intermediate representation before getting the full list of constraints and witnesses. For the sake of simplicity, we will refer to witness instead of partial witness from now on.

Note: Opcodes operate on witnesses, but we will see that some opcodes work on expressions of witnesses. We call an expression a linear combination of witnesses and/or products of two witnesses (also with a constant term). A single witness is a (simple) expression, and conversely, an expression can be turned into a single witness using an assert-zero opcode. So basically, using witnesses or expressions is equivalent, but the latter can avoid the creation of witness in some cases.

§Documentation

For detailed documentation, visit https://noir-lang.github.io/noir/docs/acir/index.html. Native structures for representing ACIR

Re-exports§

Modules§

  • black_box_functions
    Black box functions are ACIR opcodes which rely on backends implementing support for specialized constraints. This makes certain zk-snark unfriendly computations cheaper than if they were implemented in more basic constraints.
  • brillig
    This module contains Brillig structures for integration within an ACIR circuit.
  • opcodes
    ACIR opcodes

Structs§

Enums§