feat(avm)!: Remove is_infinite flag from AVM (PIL and EC points only) (#22795)

This branch includes the changes to remove the `is_infinite` flag from
our point representation and conceptually treating a point as infinite
iff its coordinates are `(0, 0)`.

It only contains logic changes within the AVM for the above and does not
touch the opcode - this is in a lower PR - so the **CI will probably
fail**.

Will close [Foundation AVM Issue
18](https://linear.app/aztec-foundation/issue/AVM-18/remove-is-inf-flag-from-resulting-ec-points-in-avm-circuits)

---

Stack:
- #22745
- #22564
- #22921
- `mw/avm-explore-remove-is-inf` <-- here
- #22945
- #23031

Author: MirandaWood

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

@@ -311,11 +311,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,27 +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.
  *
-* Note that once TODO(#AVM-266) is complete, is_inf will no longer be part of our point representation and we must either:
- *  - continue to rely on the 'calling' trace to inject a constrained is_inf, or
- *  - derive is_inf (<==> (X, Y) == (INFINITY_X, INFINITY_Y)) within this trace.
- *
  * 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:
@@ -41,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.
     //
 
@@ -74,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
@@ -151,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);
@@ -186,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;
 

barretenberg/cpp/pil/vm2/ecc_mem.pil

@@ -9,65 +9,52 @@ include "precomputed.pil";
  * Given two points, P & Q, this trace constrains that both exist on the Grumpkin curve
  * and the claimed result point, R = P + Q, is written to memory addresses within range.
  * A point exists on the curve if it satisfies the curve equation (SW form: Y^2 = X^3 − 17)
- * or is the point at infinity, represented by (X, Y) = (0, 0).
+ * or is the point at infinity, represented by (X, Y) = (INFINITY_X, INFINITY_Y) = (0, 0).
  * The reads of P and Q are handled by the registers in the execution trace. The correctness
  * of point addition is handled by the ECC subtrace.
  *
  * This trace writes the resulting embedded curve point to the addresses {dst,
- * dst + 1, and dst + 2 }. Embedded curve points consist of the tuple of types
- * {x: FF, y: FF, is_inf: U1 }.
+ * dst + 1 }. Embedded curve points consist of the tuple of types {x: FF, y: FF }.
  *
- * PRECONDITIONS: Input point coordinates have tag checked FF coordinates and U1 is_inf
- * flag (see Memory I/O below for details).
+ * PRECONDITIONS: Input point coordinates have tag checked FF coordinates (see Memory I/O
+ * below for details).
  *
  * USAGE: Dispatching lookup defined in execution.pil:
  *        #[DISPATCH_TO_ECC_ADD]
  *        sel_exec_dispatch_ecc_add {
  *          clk, context_id,
- *          register[0], register[1], register[2], // Point P
- *          register[3], register[4], register[5], // Point Q
- *          rop[6], // Dst address
+ *          register[0], register[1], // Point P
+ *          register[2], register[3], // Point Q
+ *          rop[4], // Dst address
  *          sel_opcode_error // Error
  *        } is ecc_add_mem.sel {
  *          ecc_add_mem.execution_clk, ecc_add_mem.space_id,
- *          ecc_add_mem.p_x, ecc_add_mem.p_y, ecc_add_mem.p_is_inf, // Point P
- *          ecc_add_mem.q_x, ecc_add_mem.q_y, ecc_add_mem.q_is_inf, // Point Q
+ *          ecc_add_mem.p_x, ecc_add_mem.p_y, // Point P
+ *          ecc_add_mem.q_x, ecc_add_mem.q_y, // Point Q
  *          ecc_add_mem.dst_addr[0], // Dst address
  *          ecc_add_mem.err // Error
  *        };
  *
  * Opcode operands (relevant in EXECUTION when interacting with this gadget):
  * - rop[0]: p_x_addr
  * - rop[1]: p_y_addr
- * - rop[2]: p_is_inf_addr (ignored)
- * - rop[3]: q_x_addr
- * - rop[4]: q_y_addr
- * - rop[5]: q_is_inf_addr (ignored)
- * - rop[6]: dst_addr
- *
- * Note: The values at p_is_inf_addr, q_is_inf_addr are ignored by this circuit and will be removed
- *      in TODO(#AVM-266). We instead derive whether the point is infinity by checking its coordinates
- *      for our standard representation of (0, 0). See below for details on infinity points.
+ * - rop[2]: q_x_addr
+ * - rop[3]: q_y_addr
+ * - rop[4]: dst_addr
  *
  * Memory I/O:
  * - register[0]: M[p_x_addr] aka p_x (x coordinate of point P - read from memory by EXECUTION)
  *     - p_x is tagged-checked by execution/registers to be FF based on instruction spec.
  * - register[1]: M[p_y_addr] aka p_y (y coordinate of point P - read from memory by EXECUTION)
  *     - p_y is tagged-checked by execution/registers to be FF based on instruction spec.
- * - register[2]: M[p_is_inf_addr] aka p_is_inf (boolean flag if P is the point at infinity - read from memory by EXECUTION)
- *     - Note: ignored by this circuit and will be removed in TODO(#AVM-266).
- * - register[3]: M[q_x_addr] aka q_x (x coordinate of point Q - read from memory by EXECUTION)
+ * - register[2]: M[q_x_addr] aka q_x (x coordinate of point Q - read from memory by EXECUTION)
  *     - q_x is tagged-checked by execution/registers to be FF based on instruction spec.
- * - register[4]: M[q_y_addr] aka q_y (y coordinate of point Q - read from memory by EXECUTION)
+ * - register[3]: M[q_y_addr] aka q_y (y coordinate of point Q - read from memory by EXECUTION)
  *     - q_y is tagged-checked by execution/registers to be FF based on instruction spec.
- * - register[5]: M[q_is_inf_addr] aka q_is_inf (boolean flag if Q is the point at infinity - read from memory by EXECUTION)
- *     - Note: ignored by this circuit and will be removed in TODO(#AVM-266).
- * - M[rop[6]]: M[dst_addr] aka res_x (x coordinate of the resulting point RES - written by this gadget)
+ * - M[rop[4]]: M[dst_addr] aka res_x (x coordinate of the resulting point RES - written by this gadget)
  *     - guaranteed by this gadget to be FF.
- * - M[rop[6]+1]: M[dst_offset+1] aka res_y (y coordinate of the resulting point RES - written by this gadget)
+ * - M[rop[4]+1]: M[dst_offset+1] aka res_y (y coordinate of the resulting point RES - written by this gadget)
  *     - guaranteed by this gadget to be FF.
- * - M[rop[6]+2]: M[dst_offset+2] aka res_is_inf (boolean flag if RES is the point at infinity - written by this gadget)
- *     - guaranteed by this gadget to be U1.
  *
  * ERROR HANDLING:
  * Two errors need to be handled as part of this trace,
@@ -84,30 +71,24 @@ include "precomputed.pil";
  *                                --> gt.pil
  * This subtrace is looked up by:
  * - execution.pil: To constrain the dispatch permutation for the ECADD opcode (#[DISPATCH_TO_ECC_ADD]). Includes memory
- *                  reads (register[0] to register[5]), the initial write address (rop[6]), and error flag (sel_opcode_error).
+ *                  reads (register[0] to register[3]), the initial write address (rop[4]), and error flag (sel_opcode_error).
  *
  * This subtrace looks up:
- * - memory.pil: To write the output point values (res_x, res_y, res_is_inf) to memory with standard write permutations
- *               (#[WRITE_MEM_i] for i = 0, 1, 2).
+ * - memory.pil: To write the output point values (res_x, res_y) to memory with standard write permutations
+ *               (#[WRITE_MEM_i] for i = 0, 1).
  * - ecc.pil: To retrieve the output point R as the result of adding the points P and Q read from memory
  *            (#[INPUT_OUTPUT_ECC_ADD]). See below for details on infinity points.
  * - gt.pil: To constrain that the maximum written memory address is within range (#[CHECK_DST_ADDR_IN_RANGE]).
  *
  * This subtrace is connected to the ECC subtrace via a lookup. ECC is used by other subtraces internally
  * (e.g. address derivation). Now that the is_inf flag has been removed from noir (noir-lang/noir/#11926/) we consider
- * a point to be infinity iff its coordinates are (0, 0); the noir standard representation.
+ * a point to be infinity iff its coordinates are (0, 0); the noir standard representation (see relations #[P/Q_INF_X/Y_CHECK]).
  *
  * Note that the point at infinity, O, does not have valid coordinates (a property of SW curves like Grumpkin). We represent it
  * as (0, 0) but any (ecc.INFINITY_X, ecc.INFINITY_Y) not satisfying the curve equation will be correctly handled in this trace.
  *
- * For now, we simply ignore any is_inf flags coming from memory (assigning and not reading the placeholder is_inf_), but
- * will eventually remove it from the operands TODO(#AVM-266).
- *
- * TODO(MW): Is ignoring i.e. leaving a memory operand unconstrained safe? Execution still reads them but will remove
- *  p/q_is_inf_ if so.
- *
- * Until #AVM-266, the ECC subtrace still requires a correctly constrained is_inf flag for each point. We derive it within
- * this circuit by enforcing (0, 0) <==> is_inf for input points P and Q:
+ * The ECC subtrace requires a correctly constrained is_inf flag for each point. We derive it within this circuit by enforcing
+ * (0, 0) <==> is_inf for input points P and Q:
  *  - (0, 0) ==> is_inf by #[P/Q_ON_CURVE_CHECK] (zero coordinates will fail this relation unless is_inf is set correctly).
  *  - is_inf ==> (0, 0) by #[P/Q_INF_X/Y_CHECK].
  * Resulting infinity points are guaranteed to be (0, 0) by the ECC subtrace (see #[OUTPUT_X_COORD] and #[OUTPUT_Y_COORD]).
@@ -123,18 +104,15 @@ namespace ecc_add_mem;
 
     pol commit execution_clk;
     pol commit space_id;
-    pol commit dst_addr[3];
+    pol commit dst_addr[2];
 
     // dst_addr[0] constrained by the permutation to execution
     #[WRITE_INCR_DST_ADDR]
     dst_addr[1] = sel * (dst_addr[0] + 1);
-    dst_addr[2] = sel * (dst_addr[0] + 2);
 
-    // TODO(#AVM-266): Remove p_is_inf_, q_is_inf_ (currently placeholders for #[DISPATCH_TO_ECC_ADD]).
-    pol commit p_x, p_y, p_is_inf_;
-    pol commit q_x, q_y, q_is_inf_;
+    pol commit p_x, p_y;
+    pol commit q_x, q_y;
 
-    // TODO(#AVM-266): Remove p_is_inf, q_is_inf entirely.
     // Needs to be committed columns as they are used in the lookups
     pol commit p_is_inf, q_is_inf; // constrained to be @boolean in the ecc subtrace (see #[INPUT_OUTPUT_ECC_ADD])
 
@@ -145,15 +123,15 @@ namespace ecc_add_mem;
 
     // Use the comparison gadget to check that the max addresses are within range
     // The comparison gadget provides the ability to test GreaterThan so we check
-    // dst_addr[2] > max_mem_addr
+    // dst_addr[1] > max_mem_addr
     pol commit max_mem_addr; // Column needed until we support constants in lookups
     sel * (max_mem_addr - constants.AVM_HIGHEST_MEM_ADDRESS) = 0;
 
     // Preconditions to `gt` gadget require both inputs to be bounded by 2^128.
-    // `dst_addr[2]` = dst_addr[0] + 2 where dst_addr[0] is an address (< 2^32), so dst_addr[2] < 2^33.
+    // `dst_addr[1]` = dst_addr[0] + 1 where dst_addr[0] is an address (< 2^32), so dst_addr[1] < 2^33.
     // `max_mem_addr` = AVM_HIGHEST_MEM_ADDRESS which is < 2^32.
     #[CHECK_DST_ADDR_IN_RANGE]
-    sel { dst_addr[2], max_mem_addr, sel_dst_out_of_range_err }
+    sel { dst_addr[1], max_mem_addr, sel_dst_out_of_range_err }
     in
     gt.sel_others { gt.input_a, gt.input_b, gt.res };
 
@@ -196,13 +174,11 @@ namespace ecc_add_mem;
     ///////////////////////////////////////////////////////////////////////
     // Dispatch inputs to ecc add and retrieve outputs
     ///////////////////////////////////////////////////////////////////////
-    pol commit res_x, res_y, res_is_inf; // res_is_inf is constrained to be @boolean in the ecc subtrace (see #[INPUT_OUTPUT_ECC_ADD])
+    pol commit res_x, res_y;
     pol commit sel_should_exec; // @boolean (by definition)
     sel_should_exec = sel * (1 - err);
 
-    // TODO(#AVM-266): Remove p_is_inf, q_is_inf entirely. For now, we ensure that the flag being set means that the coordinates
-    // are set to our infinity representation: (INFINITY_X, INFINITY_Y) = (0, 0). The reverse ((INFINITY_X, INFINITY_Y) ==> is_inf)
-    // is constrained by #[P/Q_ON_CURVE_CHECK]. Output infinities are already constrained to be (0, 0) in the subtrace.
+    // Constrains that the infinity flags required for the ecc trace have been set correctly:
     #[P_INF_X_CHECK]
     sel * p_is_inf * (p_x - ecc.INFINITY_X) = 0;
     #[P_INF_Y_CHECK]
@@ -217,12 +193,12 @@ namespace ecc_add_mem;
     sel_should_exec {
         p_x, p_y, p_is_inf,
         q_x, q_y, q_is_inf,
-        res_x, res_y, res_is_inf
+        res_x, res_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
     };
 
     ////////////////////////////////////////////////
@@ -243,12 +219,3 @@ namespace ecc_add_mem;
     memory.sel_ecc_write[1] {
         memory.clk, memory.space_id, memory.address, memory.value, memory.tag, memory.rw
     };
-
-    #[WRITE_MEM_2]
-    sel_should_exec {
-        execution_clk, space_id, dst_addr[2], res_is_inf, /*U1_mem_tag=1*/ sel_should_exec, /*rw=1*/ sel_should_exec
-    } is
-    memory.sel_ecc_write[2] {
-        memory.clk, memory.space_id, memory.address, memory.value, memory.tag, memory.rw
-    };
-

barretenberg/cpp/pil/vm2/execution.pil

@@ -1277,11 +1277,10 @@ sel_exec_dispatch_keccakf1600 {
 };
 
 // ECADD DISPATCHING
-// Each input point uses 3 registers:
-//  P = [x, y, is_inf] -> register[0..2], Q = [x, y, is_inf] -> register[3..5]
-// TODO(#AVM-266): Remove is_inf and use 2 registers per point (for now, the 3rd register is read but ignored).
+// Each input point uses 2 registers:
+//  P = [x, y] -> register[0..1], Q = [x, y] -> register[2..3]
 // The output point is written to memory internally inside the ecc_add_mem (ecc_mem.pil) trace, starting at:
-//  dst_addr[0] -> rop[6]
+//  dst_addr[0] -> rop[4]
 // Outputs (#[WRITE_MEM_x]) and memory write checks (#[CHECK_DST_ADDR_IN_RANGE]) are hence handled by the trace.
 
 #[DISPATCH_TO_ECC_ADD]
@@ -1291,13 +1290,11 @@ sel_exec_dispatch_ecc_add {
         // Point P
         register[0],
         register[1],
-        register[2],
         // Point Q
+        register[2],
         register[3],
-        register[4],
-        register[5],
         // Dst address
-        rop[6],
+        rop[4],
         // Error
         sel_opcode_error
 } is ecc_add_mem.sel {
@@ -1306,11 +1303,9 @@ sel_exec_dispatch_ecc_add {
         // Point P
         ecc_add_mem.p_x,
         ecc_add_mem.p_y,
-        ecc_add_mem.p_is_inf_,
         // Point Q
         ecc_add_mem.q_x,
         ecc_add_mem.q_y,
-        ecc_add_mem.q_is_inf_,
         // Dst address
         ecc_add_mem.dst_addr[0],
         // Error

barretenberg/cpp/pil/vm2/memory.pil

@@ -175,10 +175,9 @@ sel_sha256_op[6] * (1 - sel_sha256_op[6]) = 0;
 sel_sha256_op[7] * (1 - sel_sha256_op[7]) = 0;
 
 // Permutation selectors (ecc_mem.pil).
-pol commit sel_ecc_write[3]; // @boolean
+pol commit sel_ecc_write[2]; // @boolean
 sel_ecc_write[0] * (1 - sel_ecc_write[0]) = 0;
 sel_ecc_write[1] * (1 - sel_ecc_write[1]) = 0;
-sel_ecc_write[2] * (1 - sel_ecc_write[2]) = 0;
 
 // Permutation selectors (to_radix_mem.pil).
 pol commit sel_to_radix_write; // @boolean
@@ -212,7 +211,7 @@ sel = // Addressing.
     + sel_sha256_op[0] + sel_sha256_op[1] + sel_sha256_op[2] + sel_sha256_op[3]
     + sel_sha256_op[4] + sel_sha256_op[5] + sel_sha256_op[6] + sel_sha256_op[7]
     // ECC.
-    + sel_ecc_write[0] + sel_ecc_write[1] + sel_ecc_write[2]
+    + sel_ecc_write[0] + sel_ecc_write[1]
     // To Radix.
     + sel_to_radix_write;