Skip to main content

ACIR OpCodes

The Aztec Noir DSL provides an intuitive, rust-like language that is saved to .nr files. Noir circuits are meant to emulate traditional code as closely as possible. Under the hood, however, .nr files are translated into an intermediate representation (IR) called the ACIR (abstract circuit intermediate representation). The IR provides all the necessary information to generate a constraint system in any language.

Examining the ACIR​

For the following demonstration, we will use the "hello world" circuit generated by running nargo new hello_world. The easiest way to manually examine the ACIR is to run any nargo command with the acir print flag. 

# in the newly created "./hello_world" folder
nargo compile --print-acir

which outputs

Compiled ACIR for main:
current witness index : 11
public parameters indices : []
return value indices : []
BLACKBOX::RANGE [(_1, num_bits: 32)] [ ]
BLACKBOX::RANGE [(_2, num_bits: 32)] [ ]
BLACKBOX::RANGE [(_3, num_bits: 32)] [ ]
DIR::QUOTIENT (out : _%EXPR [ (1, _1) (-1, _2) 2³² ]%,  (_5, %EXPR [ 2³² ]%), _4)
BLACKBOX::RANGE [(_4, num_bits: 32)] [ ]
EXPR [ (1, _5, _5) (-1, _5) 0 ]
EXPR [ (-1, _1) (1, _2) (1, _10) -2³² ]
EXPR [ (1, _4) (2³², _5) (-1, _10) 0 ]
EXPR [ (-1, _3) (1, _4) (-1, _6) 0 ]
DIR::INVERT (_6, out: _7) 
EXPR [ (1, _6, _7) (-1, _8) 0 ]
EXPR [ (1, _6, _8) (-1, _6) 0 ]
EXPR [ (1, _8) 0 ]

OpCodes​

OpCodes are how we shape the constraint system. There are three main types of OpCodes present in the ACIR:

  • Expressions
  • Black Box Functions
  • Directives

The values given for witnesses in the ACIR are indexes that can be used to look up and assign the true values later, when proofs are actually being made. Doing this allows us to shape a constraint system that is agnostic to the inputs.

Expressions​

Expressions are simple, and the ACVM is capable of computing the expected values for witnesses. We simply need to assign these values inside the proof system's backend.

There are three types of terms in our expressions: linear, multiplicative, and constant. Coefficients are printed only as numbers themselves (-1, 2³², etc) while witnesses are prefixed with "_" (_4, _5, etc).

  • Linear term (coefficient * variable): (1, _4), (2³², _5), etc
  • Multiplicative term (coefficient variable_a variable_b): (1, _6, _7), (1, _6, _8), etc
  • Constant term: 0, _4, etc

Say we want to prove 5x + 6y == 1, or 5x + 6y - 1 == 0. This expression becomes EXPR [(5, _1), (6, _2) -1 ].

This explanation is paraphrased from kevayndray, with more detail and their loose connection to plonk arithmetization here.

Black Box Functions​

Black Box Functions are much more complex than expressions. Functionality like hashing, elliptic curve operations, and proof recursion will generally make use of efficiency optimizations in the underlying proving system (perhaps using custom gates or lookup arguments).

Take SHA256 black box opcode (not yet implemented in Halo2 Backend):

SHA256 {
    inputs: Vec<FunctionInput>,
    outputs: Vec<Witness>,
},

Here, the ACIR would provide an opcode that looks something like BLACKBOX::SHA256 [(_1, num_bits: 8), (_2, num_bits: 8)] [ (_3,...,_34)]. Here, witness inputs and outputs are provided, and the ACVM backend is responsible for constraining the proper computation to reach the outputs from the inputs. Your backend will create further interstitial witness values inside the black box, however only the input and output of the black box function is tracked by the ACIR.

Directives​

Directives are unconstrained operations that are handled by the ACVM witness generator. The witness map generated by the ACVM will handle directive opcodes for you.