|
| 1 | +//! The Abstract Circuit Intermediate Representation (ACIR) |
| 2 | +//! |
| 3 | +//! The purpose of ACIR is to make the link between a generic proving system, such |
| 4 | +//! as Aztec's Barretenberg, and a frontend, such as Noir, which describes user |
| 5 | +//! specific computations. |
| 6 | +//! |
| 7 | +//! More precisely, Noir is a programming language for zero-knowledge proofs (ZKP) |
| 8 | +//! which allows users to write programs in an intuitive way using a high-level |
| 9 | +//! language close to Rust syntax. Noir is able to generate a proof of execution of |
| 10 | +//! a Noir program, using an external proving system. However, proving systems use |
| 11 | +//! specific low-level constrain-based languages. Similarly, frontends have their |
| 12 | +//! own internal representation in order to represent user programs. |
| 13 | +//! |
| 14 | +//! The goal of ACIR is to provide a generic open-source intermediate |
| 15 | +//! representation close to proving system 'languages', but agnostic to a specific |
| 16 | +//! proving system, that can be used both by proving system as well as a target for |
| 17 | +//! frontends. So, at the end of the day, an ACIR program is just another |
| 18 | +//! representation of a program, dedicated to proving systems. |
| 19 | +//! |
| 20 | +//! ## Abstract Circuit Intermediate Representation |
| 21 | +//! ACIR stands for abstract circuit intermediate representation: |
| 22 | +//! - **abstract circuit**: circuits are a simple computation model where basic |
| 23 | +//! computation units, named gates, are connected with wires. Data flows |
| 24 | +//! through the wires while gates compute output wires based on their input. |
| 25 | +//! More formally, they are directed acyclic graphs (DAG) where the vertices |
| 26 | +//! are the gates and the edges are the wires. Due to the immutability nature |
| 27 | +//! of the wires (their value does not change during an execution), they are |
| 28 | +//! well suited for describing computations for ZKPs. Furthermore, we do not |
| 29 | +//! lose any expressiveness when using a circuit as it is well known that any |
| 30 | +//! bounded computation can be translated into an arithmetic circuit (i.e a |
| 31 | +//! circuit with only addition and multiplication gates). |
| 32 | +//! The term abstract here simply means that we do not refer to an actual physical |
| 33 | +//! circuit (such as an electronic circuit). Furthermore, we will not exactly use |
| 34 | +//! the circuit model, but another model even better suited to ZKPs, the constraint |
| 35 | +//! model (see below). |
| 36 | +//! - **intermediate representation**: The ACIR representation is intermediate |
| 37 | +//! because it lies between a frontend and its proving system. ACIR bytecode makes |
| 38 | +//! the link between noir compiler output and the proving system backend input. |
| 39 | +//! |
| 40 | +//! ## The constraint model |
| 41 | +//! |
| 42 | +//! The first step for generating a proof that a specific program was executed, is |
| 43 | +//! to execute this program. Since the proving system is going to handle ACIR |
| 44 | +//! programs, we need in fact to execute an ACIR program, using the user-supplied |
| 45 | +//! inputs. |
| 46 | +//! |
| 47 | +//! In ACIR terminology, the gates are called opcodes and the wires are called |
| 48 | +//! partial witnesses. However, instead of connecting the opcodes together through |
| 49 | +//! wires, we create constraints: an opcode constraints together a set of wires. |
| 50 | +//! This constraint model trivially supersedes the circuit model. For instance, an |
| 51 | +//! addition gate `output_wire = input_wire_1 + input_wire_2` can be expressed with |
| 52 | +//! the following arithmetic constraint: |
| 53 | +//! `output_wire - (input_wire_1 + input_wire_2) = 0` |
| 54 | +//! |
| 55 | +//! ## Solving |
| 56 | +//! |
| 57 | +//! Because of these constraints, executing an ACIR program is called solving the |
| 58 | +//! witnesses. From the witnesses representing the inputs of the program, whose |
| 59 | +//! values are supplied by the user, we find out what the other witnesses should be |
| 60 | +//! by executing/solving the constraints one-by-one in the order they were defined. |
| 61 | +//! |
| 62 | +//! For instance, if `input_wire_1` and `input_wire_2` values are supplied as `3` and |
| 63 | +//! `8`, then we can solve the opcode |
| 64 | +//! `output_wire - (input_wire_1 + input_wire_2) = 0` by saying that `output_wire` is |
| 65 | +//! `11`. |
| 66 | +//! |
| 67 | +//! In summary, the workflow is the following: |
| 68 | +//! 1. user program -> (compilation) ACIR, a list of opcodes which constrain |
| 69 | +//! (partial) witnesses |
| 70 | +//! 2. user inputs + ACIR -> (execution/solving) assign values to all the |
| 71 | +//! (partial) witnesses |
| 72 | +//! 3. witness assignment + ACIR -> (proving system) proof |
| 73 | +//! |
| 74 | +//! Although the ordering of opcode does not matter in theory, since a system of |
| 75 | +//! equations is not dependent on its ordering, in practice it matters a lot for the |
| 76 | +//! solving (i.e the performance of the execution). ACIR opcodes **must be ordered** |
| 77 | +//! so that each opcode can be resolved one after the other. |
| 78 | +//! |
| 79 | +//! The values of the witnesses lie in the scalar field of the proving system. We |
| 80 | +//! will refer to it as `FieldElement` or ACIR field. The proving system needs the |
| 81 | +//! values of all the partial witnesses and all the constraints in order to generate |
| 82 | +//! a proof. |
| 83 | +//! |
| 84 | +//! _Remark_: The value of a partial witness is unique and fixed throughout a program |
| 85 | +//! execution, although in some rare cases, multiple values are possible for a |
| 86 | +//! same execution and witness (when there are several valid solutions to the |
| 87 | +//! constraints). Having multiple possible values for a witness may indicate that |
| 88 | +//! the circuit is not safe. |
| 89 | +//! |
| 90 | +//! _Remark_: Why do we use the term partial witnesses? It is because the proving |
| 91 | +//! system may create other constraints and witnesses (especially with |
| 92 | +//! `BlackBoxFuncCall`, see below). A proof refers to a full witness assignments |
| 93 | +//! and their constraints. ACIR opcodes and their partial witnesses are still an |
| 94 | +//! intermediate representation before getting the full list of constraints and |
| 95 | +//! witnesses. For the sake of simplicity, we will refer to witness instead of |
| 96 | +//! partial witness from now on. |
| 97 | +
|
1 | 98 | #![cfg_attr(not(test), forbid(unsafe_code))] // `std::env::set_var` is used in tests.
|
2 | 99 | #![warn(unreachable_pub)]
|
3 | 100 | #![warn(clippy::semicolon_if_nothing_returned)]
|
4 | 101 | #![cfg_attr(not(test), warn(unused_crate_dependencies, unused_extern_crates))]
|
5 | 102 |
|
6 |
| -// Arbitrary Circuit Intermediate Representation |
7 |
| - |
8 | 103 | pub mod circuit;
|
9 | 104 | pub mod native_types;
|
10 | 105 | mod proto;
|
|
0 commit comments