chore!: Rename Arithmetic opcode to AssertZero

acvm-repo/acir/acir_docs.md

@@ -6,9 +6,9 @@
 ## Introduction
 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 uses 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.
 
 ## Abstract Circuit Intermediate Representation
 ACIR stands for abstract circuit intermediate representation:
@@ -32,7 +32,7 @@
 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 assignement + 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.
@@ -43,7 +43,7 @@
 
 *Remark*: 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.
 
 *Remark*: 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 assignements and their 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.
 
 
 ## ACIR Reference
@@ -55,22 +55,22 @@
 
 Finally, some opcodes will have a predicate, whose value is 0 or 1. Its purpose is to nullify the opcode when the value is 0, so that it has no effect. Note that removing the opcode is not a solution because this modifies the circuit (the circuit being mainly the list of the opcodes). 
 
-*Remark*: Opcodes operate on witnesses, but we will see that some opcode work on Arithmetic expressions of witnesses. We call an arithmetic expression a linear combination of witnesses and/or products of two witnesses (and also a constant term). A single witness is a (simple) arithmetic expression, and conversly, an arithmetic expression can be turned into a single witness using an arithmetic opcode (see below). So basically, using witnesses or arithmetic expressions is equivalent, but the latter can avoid the creation of witness in some cases.
+*Remark*: Opcodes operate on witnesses, but we will see that some opcode work on expressions of witnesses. We call an expression a linear combination of witnesses and/or products of two witnesses (and also 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 (see below). So basically, using witnesses or expressions is equivalent, but the latter can avoid the creation of witness in some cases.
 
-### Arithmetic opcode
-An arithmetic opcode adds the constraint that P(w) = 0, where w=(w_1,..w_n) is a tuple of n witnesses, and P is a multi-variate polynomial of total degree at most 2.
+### AssertZero opcode
+An AssertZero opcode adds the constraint that P(w) = 0, where w=(w_1,..w_n) is a tuple of n witnesses, and P is a multi-variate polynomial of total degree at most 2.
 The coefficients ${q_M}_{i,j}, q_i,q_c$ of the polynomial are known values which define the opcode.
-A general expression of arithmetic opcode is the following: $\sum_{i,j} {q_M}_{i,j}w_iw_j + \sum_i q_iw_i +q_c = 0$
+A general expression of assert-zero opcode is the following: $\sum_{i,j} {q_M}_{i,j}w_iw_j + \sum_i q_iw_i +q_c = 0$
 
-An arithmetic opcode can be used to:
+An assert-zero opcode can be used to:
 - **express a constraint** on witnesses; for instance to express that a witness $w$ is a boolean, you can add the opcode:  $w*w-w=0$
 - or, to **compute the value** of an arithmetic operation of some inputs. For instance, to multiply two witnesses $x$ and $y$, you would use the opcode $z-x*y=0$, which would constraint $z$ to be $x*y$.
 
 
 The solver expects that at most one witness is not known when executing the opcode.
 
 ### BlackBoxFuncCall opcode
-These opcodes represent a specific computation. Even if any computation can be done using only arithmetic opcodes, it is not always efficient. Some proving systems, and in particular the proving system from Aztec, can implement several computations more efficiently using for instance look-up tables. The BlackBoxFuncCall opcode is used to ask the proving system to handle the computation by itself.
+These opcodes represent a specific computation. Even if any computation can be done using only assert-zero opcodes, it is not always efficient. Some proving systems, and in particular the proving system from Aztec, can implement several computations more efficiently using for instance look-up tables. The BlackBoxFuncCall opcode is used to ask the proving system to handle the computation by itself.
 All black box functions takes as input a tuple (witness, num_bits), where num_bits is a constant representing the bit size of the input witness, and they have one or several witnesses as output.
 Some more advanced computations assume that the proving system has an 'embedded curve'. It is a curve that cycle with the main curve of the proving system, i.e the scalar field of the embedded curve is the base field of the main one, and vice-versa. The curves used by the proving system are dependent on the proving system (and/or its configuration). Aztec's Barretenberg uses BN254 as the main curve and Grumpkin as the embedded curve.
 
@@ -91,11 +91,11 @@
 
 **SHA256**: computes sha256 of the inputs
 - inputs are a byte array, i.e a vector of (FieldElement, 8)
 - output is a byte array of len 32, i.e a vector of 32 (FieldElement, 8), constrainted to be the sha256 of the inputs.
 
 **Blake2s**: computes the Blake2s hash of the inputs, as specified in https://tools.ietf.org/html/rfc7693
 - inputs are a byte array, i.e a vector of (FieldElement, 8)
 - output is a byte array of length 32, i.e a vector of 32 (FieldElement, 8), constrainted to be the blake2s of the inputs.
 
 
 **SchnorrVerify**: Verify a Schnorr signature over the embedded curve
@@ -114,7 +114,7 @@
 - output: 2 witnesses representing the x,y coordinates of the resulting Grumpkin point
 - domain separator: a constant public value (a field element) that you can use so that the commitment also depends on the domain separator. Noir uses 0 as domain separator.
 
 The backend should handle proper conversion between the inputs being ACIR field elements and the scalar field of the embedded curve. In the case of Aztec's Barretenberg, the latter is bigger than the ACIR field so it is straightforward. The Peredersen generators are managed by the proving system.
 
 
 **PedersenHash**: Computes a Pedersen commitments of the inputs and their number, using generators of the embedded curve
@@ -163,7 +163,7 @@
 - verification_key: Vector of (FieldElement, 254) representing the verification key of the circuit being verified
 - public_inputs: Vector of (FieldElement, 254)  representing the public inputs corresponding to the proof being verified
 - key_hash: one (FieldElement, 254). It should be the hash of the verification key. Barretenberg expects the Pedersen hash of the verification key
 - input_aggregation_object: an optional vector of (FieldElement, 254). It is a blob of data specific to the proving sytem.
 - output_aggregation_object: Some witnesses returned by the function, representing some data internal to the proving system.
 
 This black box function does not fully verify a proof, what it does is verifying that the key_hash is indeed a hash of verification_key, allowing the user to use the verification key as private inputs and only have the key_hash as public input, which is more performant.
@@ -179,8 +179,8 @@
 - bytecode: assembly code representing the computation to perform within this opcode. The noir assembly specification is not part of this document.
 - predicate: an arithmetic expression that disable the opcode when it is null.
 
 Let's see an example with euclidian division.
-The normal way to compute a/b, where a and b are 8-bits integers, is to implement Euclid algorithm which computes in a loop (or recursively) modulos of the kind 'a mod b'. Doing this computation requires a lot of steps to be properly implemented in ACIR, especially the loop with a condition. However, euclidian division can be easily constrained with one arithmetic opcode: a = bq+r, assuming q is 8 bits and r<b. Since these assumptions can easily written with a few range opcodes, euclidian division can in fact be implemented with a small number of opcodes.
+The normal way to compute a/b, where a and b are 8-bits integers, is to implement Euclid algorithm which computes in a loop (or recursively) modulos of the kind 'a mod b'. Doing this computation requires a lot of steps to be properly implemented in ACIR, especially the loop with a condition. However, euclidian division can be easily constrained with one assert-zero opcode: a = bq+r, assuming q is 8 bits and r<b. Since these assumptions can easily written with a few range opcodes, euclidian division can in fact be implemented with a small number of opcodes.
 
 However, in order to write these opcodes we need the result of the division which are the witness q and r. But from the constraint a=bq+r, how can the solver figure out how to solve q and r with only one equation? This is where brillig/unconstrained function come into action. We simply define a function that performs the usual Euclid algorithm to compute q and r from a and b. Since Brillig opcode does not generate constraint, it won't be provided to the proving system but simply used by the solver to compute the values of q and r.
 

acvm-repo/acir/codegen/acir.cpp

@@ -767,12 +767,12 @@ namespace Circuit {
 
     struct Opcode {
 
-        struct Arithmetic {
+        struct AssertZero {
             Circuit::Expression value;
 
-            friend bool operator==(const Arithmetic&, const Arithmetic&);
+            friend bool operator==(const AssertZero&, const AssertZero&);
             std::vector<uint8_t> bincodeSerialize() const;
-            static Arithmetic bincodeDeserialize(std::vector<uint8_t>);
+            static AssertZero bincodeDeserialize(std::vector<uint8_t>);
         };
 
         struct BlackBoxFuncCall {
@@ -818,7 +818,7 @@ namespace Circuit {
             static MemoryInit bincodeDeserialize(std::vector<uint8_t>);
         };
 
-        std::variant<Arithmetic, BlackBoxFuncCall, Directive, Brillig, MemoryOp, MemoryInit> value;
+        std::variant<AssertZero, BlackBoxFuncCall, Directive, Brillig, MemoryOp, MemoryInit> value;
 
         friend bool operator==(const Opcode&, const Opcode&);
         std::vector<uint8_t> bincodeSerialize() const;
@@ -4268,20 +4268,20 @@ Circuit::Opcode serde::Deserializable<Circuit::Opcode>::deserialize(Deserializer
 
 namespace Circuit {
 
-    inline bool operator==(const Opcode::Arithmetic &lhs, const Opcode::Arithmetic &rhs) {
+    inline bool operator==(const Opcode::AssertZero &lhs, const Opcode::AssertZero &rhs) {
         if (!(lhs.value == rhs.value)) { return false; }
         return true;
     }
 
-    inline std::vector<uint8_t> Opcode::Arithmetic::bincodeSerialize() const {
+    inline std::vector<uint8_t> Opcode::AssertZero::bincodeSerialize() const {
         auto serializer = serde::BincodeSerializer();
-        serde::Serializable<Opcode::Arithmetic>::serialize(*this, serializer);
+        serde::Serializable<Opcode::AssertZero>::serialize(*this, serializer);
         return std::move(serializer).bytes();
     }
 
-    inline Opcode::Arithmetic Opcode::Arithmetic::bincodeDeserialize(std::vector<uint8_t> input) {
+    inline Opcode::AssertZero Opcode::AssertZero::bincodeDeserialize(std::vector<uint8_t> input) {
         auto deserializer = serde::BincodeDeserializer(input);
-        auto value = serde::Deserializable<Opcode::Arithmetic>::deserialize(deserializer);
+        auto value = serde::Deserializable<Opcode::AssertZero>::deserialize(deserializer);
         if (deserializer.get_buffer_offset() < input.size()) {
             throw serde::deserialization_error("Some input bytes were not read");
         }
@@ -4292,14 +4292,14 @@ namespace Circuit {
 
 template <>
 template <typename Serializer>
-void serde::Serializable<Circuit::Opcode::Arithmetic>::serialize(const Circuit::Opcode::Arithmetic &obj, Serializer &serializer) {
+void serde::Serializable<Circuit::Opcode::AssertZero>::serialize(const Circuit::Opcode::AssertZero &obj, Serializer &serializer) {
     serde::Serializable<decltype(obj.value)>::serialize(obj.value, serializer);
 }
 
 template <>
 template <typename Deserializer>
-Circuit::Opcode::Arithmetic serde::Deserializable<Circuit::Opcode::Arithmetic>::deserialize(Deserializer &deserializer) {
-    Circuit::Opcode::Arithmetic obj;
+Circuit::Opcode::AssertZero serde::Deserializable<Circuit::Opcode::AssertZero>::deserialize(Deserializer &deserializer) {
+    Circuit::Opcode::AssertZero obj;
     obj.value = serde::Deserializable<decltype(obj.value)>::deserialize(deserializer);
     return obj;
 }

acvm-repo/acir/src/circuit/mod.rs

@@ -277,7 +277,7 @@ mod tests {
         let circuit = Circuit {
             current_witness_index: 0,
             opcodes: vec![
-                Opcode::Arithmetic(crate::native_types::Expression {
+                Opcode::AssertZero(crate::native_types::Expression {
                     mul_terms: vec![],
                     linear_combinations: vec![],
                     q_c: FieldElement::from(8u128),

acvm-repo/acir/src/circuit/opcodes.rs

@@ -13,7 +13,7 @@ pub use memory_operation::{BlockId, MemOp};
 
 #[derive(Clone, PartialEq, Eq, Serialize, Deserialize)]
 pub enum Opcode {
-    Arithmetic(Expression),
+    AssertZero(Expression),
     /// Calls to "gadgets" which rely on backends implementing support for specialized constraints.
     ///
     /// Often used for exposing more efficient implementations of SNARK-unfriendly computations.  
@@ -36,7 +36,7 @@ pub enum Opcode {
 impl std::fmt::Display for Opcode {
     fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
         match self {
-            Opcode::Arithmetic(expr) => {
+            Opcode::AssertZero(expr) => {
                 write!(f, "EXPR [ ")?;
                 for i in &expr.mul_terms {
                     write!(f, "({}, _{}, _{}) ", i.0, i.1.witness_index(), i.2.witness_index())?;

acvm-repo/acir/src/native_types/expression/mod.rs

@@ -8,15 +8,15 @@ mod ordering;
 
 // In the addition polynomial
 // We can have arbitrary fan-in/out, so we need more than wL,wR and wO
-// When looking at the arithmetic opcode for the quotient polynomial in standard plonk
+// When looking at the assert-zero opcode for the quotient polynomial in standard plonk
 // You can think of it as fan-in 2 and fan out-1 , or you can think of it as fan-in 1 and fan-out 2
 //
 // In the multiplication polynomial
 // XXX: If we allow the degree of the quotient polynomial to be arbitrary, then we will need a vector of wire values
 #[derive(Clone, Debug, PartialEq, Eq, Serialize, Deserialize, Hash)]
 pub struct Expression {
     // To avoid having to create intermediate variables pre-optimization
-    // We collect all of the multiplication terms in the arithmetic opcode
+    // We collect all of the multiplication terms in the assert-zero opcode
     // A multiplication term if of the form q_M * wL * wR
     // Hence this vector represents the following sum: q_M1 * wL1 * wR1 + q_M2 * wL2 * wR2 + .. +
     pub mul_terms: Vec<(FieldElement, Witness, Witness)>,
@@ -42,7 +42,7 @@ impl std::fmt::Display for Expression {
         if let Some(witness) = self.to_witness() {
             write!(f, "x{}", witness.witness_index())
         } else {
-            write!(f, "%{:?}%", crate::circuit::opcodes::Opcode::Arithmetic(self.clone()))
+            write!(f, "%{:?}%", crate::circuit::opcodes::Opcode::AssertZero(self.clone()))
         }
     }
 }
@@ -178,7 +178,13 @@ impl Expression {
         self.linear_combinations.sort_by(|a, b| a.1.cmp(&b.1));
     }
 
-    /// Checks if this polynomial can fit into one arithmetic identity
+    /// Checks if this expression can fit into one arithmetic identity
+    /// TODO: This needs to be reworded, arithmetic identity only makes sense in the context
+    /// TODO of PLONK, whereas we want expressions to be generic.
+    /// TODO: We just need to reword it to say exactly what its doing and
+    /// TODO then reference the fact that this is what plonk will accept.
+    /// TODO alternatively, we can define arithmetic identity in the context of expressions
+    /// TODO and then reference that.
     pub fn fits_in_one_identity(&self, width: usize) -> bool {
         // A Polynomial with more than one mul term cannot fit into one opcode
         if self.mul_terms.len() > 1 {

acvm-repo/acir/tests/test_program_serialization.rs

@@ -24,7 +24,7 @@ use brillig::{HeapArray, RegisterIndex, RegisterOrMemory};
 
 #[test]
 fn addition_circuit() {
-    let addition = Opcode::Arithmetic(Expression {
+    let addition = Opcode::AssertZero(Expression {
         mul_terms: Vec::new(),
         linear_combinations: vec![
             (FieldElement::one(), Witness(1)),

acvm-repo/acvm/src/compiler/optimizers/mod.rs

@@ -31,8 +31,8 @@ pub(super) fn optimize_internal(acir: Circuit) -> (Circuit, Vec<usize>) {
         .opcodes
         .into_iter()
         .map(|opcode| {
-            if let Opcode::Arithmetic(arith_expr) = opcode {
-                Opcode::Arithmetic(GeneralOptimizer::optimize(arith_expr))
+            if let Opcode::AssertZero(arith_expr) = opcode {
+                Opcode::AssertZero(GeneralOptimizer::optimize(arith_expr))
             } else {
                 opcode
             }

acvm-repo/acvm/src/compiler/optimizers/redundant_range.rs

@@ -132,7 +132,7 @@ fn extract_range_opcode(opcode: &Opcode) -> Option<(Witness, u32)> {
 
 fn optimized_range_opcode(witness: Witness, num_bits: u32) -> Opcode {
     if num_bits == 1 {
-        Opcode::Arithmetic(Expression {
+        Opcode::AssertZero(Expression {
             mul_terms: vec![(FieldElement::one(), witness, witness)],
             linear_combinations: vec![(-FieldElement::one(), witness)],
             q_c: FieldElement::zero(),
@@ -234,13 +234,13 @@ mod tests {
     #[test]
     fn non_range_opcodes() {
         // The optimizer should not remove or change non-range opcodes
-        // The four Arithmetic opcodes should remain unchanged.
+        // The four AssertZero opcodes should remain unchanged.
         let mut circuit = test_circuit(vec![(Witness(1), 16), (Witness(1), 16)]);
 
-        circuit.opcodes.push(Opcode::Arithmetic(Expression::default()));
-        circuit.opcodes.push(Opcode::Arithmetic(Expression::default()));
-        circuit.opcodes.push(Opcode::Arithmetic(Expression::default()));
-        circuit.opcodes.push(Opcode::Arithmetic(Expression::default()));
+        circuit.opcodes.push(Opcode::AssertZero(Expression::default()));
+        circuit.opcodes.push(Opcode::AssertZero(Expression::default()));
+        circuit.opcodes.push(Opcode::AssertZero(Expression::default()));
+        circuit.opcodes.push(Opcode::AssertZero(Expression::default()));
         let acir_opcode_positions = circuit.opcodes.iter().enumerate().map(|(i, _)| i).collect();
         let optimizer = RangeOptimizer::new(circuit);
         let (optimized_circuit, _) = optimizer.replace_redundant_ranges(acir_opcode_positions);

acvm-repo/acvm/src/compiler/transformers/csat.rs

@@ -62,7 +62,7 @@ impl CSatTransformer {
     }
 
     // Still missing dead witness optimization.
-    // To do this, we will need the whole set of arithmetic opcodes
+    // To do this, we will need the whole set of assert-zero opcodes
     // I think it can also be done before the local optimization seen here, as dead variables will come from the user
     pub(crate) fn transform(
         &mut self,
@@ -84,7 +84,7 @@ impl CSatTransformer {
         opcode
     }
 
-    // This optimization will search for combinations of terms which can be represented in a single arithmetic opcode
+    // This optimization will search for combinations of terms which can be represented in a single assert-zero opcode
     // Case 1 : qM * wL * wR + qL * wL + qR * wR + qO * wO + qC
     // This polynomial does not require any further optimizations, it can be safely represented in one opcode
     // ie a polynomial with 1 mul(bi-variate) term and 3 (univariate) terms where 2 of those terms match the bivariate term
@@ -93,13 +93,13 @@ impl CSatTransformer {
     //
     //
     // Case 2: qM * wL * wR + qL * wL + qR * wR + qO * wO + qC + qM2 * wL2 * wR2 + qL * wL2 + qR * wR2 + qO * wO2 + qC2
-    // This polynomial cannot be represented using one arithmetic opcode.
+    // This polynomial cannot be represented using one assert-zero opcode.
     //
     // This algorithm will first extract the first full opcode(if possible):
     // t = qM * wL * wR + qL * wL + qR * wR + qO * wO + qC
     //
     // The polynomial now looks like so t + qM2 * wL2 * wR2 + qL * wL2 + qR * wR2 + qO * wO2 + qC2
-    // This polynomial cannot be represented using one arithmetic opcode.
+    // This polynomial cannot be represented using one assert-zero opcode.
     //
     // This algorithm will then extract the second full opcode(if possible):
     // t2 = qM2 * wL2 * wR2 + qL * wL2 + qR * wR2 + qO * wO2 + qC2
@@ -121,7 +121,7 @@ impl CSatTransformer {
         // If the opcode only has one mul term, then this algorithm cannot optimize it any further
         // Either it can be represented in a single arithmetic equation or it's fan-in is too large and we need intermediate variables for those
         // large-fan-in optimization is not this algorithms purpose.
-        // If the opcode has 0 mul terms, then it is an add opcode and similarly it can either fit into a single arithmetic opcode or it has a large fan-in
+        // If the opcode has 0 mul terms, then it is an add opcode and similarly it can either fit into a single assert-zero opcode or it has a large fan-in
         if opcode.mul_terms.len() <= 1 {
             return opcode;
         }
@@ -194,7 +194,7 @@ impl CSatTransformer {
                         }
                     }
 
-                    // Now we have used up 2 spaces in our arithmetic opcode. The width now dictates, how many more we can add
+                    // Now we have used up 2 spaces in our assert-zero opcode. The width now dictates, how many more we can add
                     let mut remaining_space = self.width - 2 - 1; // We minus 1 because we need an extra space to contain the intermediate variable
                                                                   // Keep adding terms until we have no more left, or we reach the width
                     let mut remaining_linear_terms =
@@ -325,7 +325,7 @@ impl CSatTransformer {
         // Then use intermediate variables again to squash the fan-in, so that it can fit into the appropriate width
 
         // First check if this polynomial actually needs a partial opcode optimization
-        // There is the chance that it fits perfectly within the arithmetic opcode
+        // There is the chance that it fits perfectly within the assert-zero opcode
         if opcode.fits_in_one_identity(self.width) {
             return opcode;
         }