feat(avm)!: Derive is_infinite flag from point coordinates (#22564)

### Update

Will also close [Foundation AVM Issue
13](https://linear.app/aztec-foundation/issue/AVM-13/enforce-canonical-point-at-infinity-representation)

Note that this is currently being used as a base for removing the flag
from AVM's point representation ([Foundation AVM Issue
14](https://linear.app/aztec-foundation/issue/AVM-14/remove-is-inf-flag-from-avm-ec-point-representation)):

- ~#22745 (in merge
train)
- #23342 (ACIR
changes from #23155 for removing `inf`)
- #22564 <-- here
- #22921 ✅ 
- #22795 ✅ 
- #22945 ✅ 
- #23031 ✅ 


**Everything in this branch has been reviewed**, see above PRs for
individual work ⬆️


### [OLD] Overview

Will close
[AVM-248](https://linear.app/aztec-labs/issue/AVM-248/enforce-canonical-point-at-infinity-representation)

As a kind of stopgap before removing the `is_infinite` flag completely
from the AVM
([AVM-266](https://linear.app/aztec-labs/issue/AVM-266/remove-is-inf-flag-from-ec-point-representation)),
we now follow Noir behaviour more closely by deriving `is_inf` from
coordinates inside the circuits ( `(x, y) == (0, 0) ? is_inf == true`).
This replaces previous logic remapping points to (0, 0) from `is_inf`.

This method relies on the on curve check (for `(0, 0) ==> is_inf `) and
some new relations enforcing coordinates (for `is_inf ==> (0, 0)`)
rather than (more expensive) error handling. However this does mean that
the former will fail with an on curve error whereas the latter will
simply fail a relation.

Author: MirandaWood

avm-transpiler/src/procedures/msm.rs

@@ -1,11 +1,11 @@
 pub(crate) const MSM_ASSEMBLY: &str = "
                 ; We are passed three pointers and one usize.
-                ; d0 points to the points. Points are represented by (x: Field, y: Field). The point at infinity is (0, 0).
+                ; d0 points to the points. Points are represented by (x: Field, y: Field).
                 ; d1 points to the scalars. Scalars are represented by (lo: Field, hi: Field) both range checked to 128 bits.
                 ; d2 contains the number of points.
                 ; d3 points to the result. The result is a point.
                 ADD d3, /*the reserved register 'one_usize'*/ $2, d4; Compute the pointer to the result y.
-                ; Initialize the msm result: point at infinity (0, 0)
+                ; Initialize the msm result: point at infinity
                 SET i3, 0 ff
                 SET i4, 0 ff
                 ; Loop globals

avm-transpiler/src/transpile.rs

@@ -1285,7 +1285,7 @@ fn handle_black_box_function(
             result,
         } => avm_instrs.push(AvmInstruction {
             opcode: AvmOpcode::ECADD,
-            // The result (SIXTH operand) is indirect (addressing mode).
+            // The result (FOURTH operand) is indirect (addressing mode).
             addressing_mode: Some(
                 AddressingModeBuilder::default()
                     .direct_operand(p1_x_offset)

barretenberg/cpp/pil/vm2/bytecode/address_derivation.pil

@@ -30,7 +30,7 @@ include "../scalar_mul.pil";
  *               as an independent 'destination' trace which is purely responsible for address
  *               computation.
  *               This means we assume all public keys are not the point at infinity, and so use
- *               precomputed.zero to represent each key's is_infinity flag (see TODO(#7529)).
+ *               precomputed.zero to represent each key's is_infinity flag (see TODO(#7529) and PR #22462).
  *
  * USAGE: To enforce that an address is correctly derived from all preimage members
  *        (adapted from #[ADDRESS_DERIVATION] in contract_instance_retrieval.pil):
@@ -184,7 +184,9 @@ namespace address_derivation;
     // 3. Computation of public keys hash
     pol commit public_keys_hash;
 
-    // TODO(#7529): Remove all the 0s for is_infinity when removed from public_keys.nr
+    // TODO(#AVM-266): Remove infinity flags from point representation. Note that we may still need to use
+    // precomputed.zero in the hash preimages until address derivation removes them:
+    // TODO(#7529)/TODO(F-553): Remove all the 0s for is_infinity when removed from public_keys.nr
     // https://github.com/AztecProtocol/aztec-packages/issues/7529
     // TODO(#14031): Compress keys in public_keys_hash
     // https://github.com/AztecProtocol/aztec-packages/issues/14031
@@ -312,11 +314,11 @@ namespace address_derivation;
     sel {
         preaddress_public_key_x, preaddress_public_key_y, precomputed.zero,
         incoming_viewing_key_x, incoming_viewing_key_y, precomputed.zero,
-        address, address_y, precomputed.zero
+        address, address_y
     } in ecc.sel {
         ecc.p_x, ecc.p_y, ecc.p_is_inf,
         ecc.q_x, ecc.q_y, ecc.q_is_inf,
-        ecc.r_x, ecc.r_y, ecc.r_is_inf
+        ecc.r_x, ecc.r_y
     };
 
     // Note: We can safely assume the address point is not infinity since that would imply either

barretenberg/cpp/pil/vm2/ecc.pil

@@ -2,23 +2,32 @@
 /**
  * This subtrace supports point addition over the Grumpkin curve.
  * Given two points, P & Q, this trace computes R = P + Q.
- * PRECONDITIONS: The only assumption here is that the inputs P & Q are points on the Grumpkin curve (note that the Point at Infinity = (0, 0) is considered on the curve):
- * Grumpkin Curve Eqn in SW form:  Y^2 = X^3 − 17.
+ * PRECONDITIONS: This trace assumes that the inputs P & Q are points on the Grumpkin curve and infinity points are correctly
+ * flagged with p_is_inf and/or q_is_inf (note that the Point at Infinity = (0, 0) is considered on the curve):
+ *      Grumpkin Curve Eqn in SW form:  Y^2 = X^3 − 17.
  * Note: Grumpkin forms a 2-cycle with BN254, i.e the base field of one is the scalar field of the other and vice-versa.
  *
  * USAGE: This is a non-memory aware subtrace used to constrain point addition as defined above. Each point can be looked up
  *        by coordinates (lookup as defined in ecc_mem.pil):
  *        #[INPUT_OUTPUT_ECC_ADD]
  *        sel_should_exec {
- *          p_x_n, p_y_n, p_is_inf, // Point P
- *          q_x_n, q_y_n, q_is_inf, // Point Q
- *          res_x, res_y, res_is_inf // Point R
+ *          p_x_n, p_y_n, // Point P
+ *          p_is_inf, // P == O
+ *          q_x_n, q_y_n, // Point Q
+ *          q_is_inf, // Q == O
+ *          res_x, res_y // Point R
  *        } in ecc.sel {
- *          ecc.p_x, ecc.p_y, ecc.p_is_inf, // Point P
- *          ecc.q_x, ecc.q_y, ecc.q_is_inf, // Point Q
- *          ecc.r_x, ecc.r_y, ecc.r_is_inf // Point R
+ *          ecc.p_x, ecc.p_y, // Point P
+ *          ecc.p_is_inf, // P == O
+ *          ecc.q_x, ecc.q_y,, // Point Q
+ *          ecc.q_is_inf, // Q == O
+ *          ecc.r_x, ecc.r_y // Point R
  *        };
  *
+ * NOTE: For now, the calling trace MUST constrain that p_is_inf, q_is_inf above are correct. This is so if we have a calling
+ *       trace in which we know inf would never be an input we can simply use precomputed.zero and avoid wasting gates on deriving is_inf.
+ *       This follows the same logic for points being on the curve.
+ *
  * TRACE SHAPE: 1 single row per computation (P + Q = R).
  *
  * INTERACTIONS: This subtrace is looked up by:
@@ -37,11 +46,11 @@ namespace ecc;
     // We perform point addition over our Short Weierstrass (SW) curve with 3 cases outlined in the last section ('Assign Result').
     // The notation will be as follows:
     //    P + Q = R where:
-    //      P = (p_x, p_y, p_is_inf), Q = (q_x, q_y, q_is_inf), R = (r_x, r_y, r_is_inf),
+    //      P = (p_x, p_y), Q = (q_x, q_y), R = (r_x, r_y),
     //    where the coordinates satisfy:
     //      y^2 = x^3 - 17 (unless is_inf is true).
     // The point at infinity, O, does not have valid coordinates (a property of SW curves). We represent it as:
-    //    O = (0, 0, true).
+    //    O = (0, 0).
     //    Note: this is NOT enforced here for inputs, see ecc_mem.pil for example of constraining.
     //
 
@@ -70,20 +79,20 @@ namespace ecc;
     // Point P in affine form
     pol commit p_x;
     pol commit p_y;
+    // Must be constrained by the calling trace:
     pol commit p_is_inf; // @boolean
     p_is_inf * (1 - p_is_inf) = 0;
 
     // Point Q in affine form
     pol commit q_x;
     pol commit q_y;
+    // Must be constrained by the calling trace:
     pol commit q_is_inf; // @boolean
     q_is_inf * (1 - q_is_inf) = 0;
 
     // Resulting Point R in affine form
     pol commit r_x;
     pol commit r_y;
-    pol commit r_is_inf; // @boolean
-    r_is_inf * (1 - r_is_inf) = 0;
 
     // Check x coordinates, i.e. p_x == q_x
     pol commit x_match; // @boolean
@@ -147,9 +156,9 @@ namespace ecc;
     //    If P != Q where x_match, this implies p_y == -q_y <==> P == -Q (INVERSE_PRED == true):
     //      R := O
     //    If P == O:
-    //      R := Q (r_x := q_x, r_y := q_y, r_is_inf = q_is_inf)
+    //      R := Q (r_x := q_x, r_y := q_y)
     //    Vice versa, if Q == O:
-    //      R := P (r_x := p_x, r_y := p_y, r_is_inf = p_is_inf)
+    //      R := P (r_x := p_x, r_y := p_y)
     //
 
     pol INVERSE_PRED = x_match * (1 - y_match);
@@ -182,6 +191,4 @@ namespace ecc;
     sel * (r_x - (EITHER_INF * (p_is_inf * q_x + q_is_inf * p_x)) - result_infinity * INFINITY_X - use_computed_result * COMPUTED_R_X) = 0;
     #[OUTPUT_Y_COORD]
     sel * (r_y - (EITHER_INF * (p_is_inf * q_y + q_is_inf * p_y)) - result_infinity * INFINITY_Y - use_computed_result * COMPUTED_R_Y) = 0;
-    #[OUTPUT_INF_FLAG]
-    sel * (r_is_inf - result_infinity) = 0;