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

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):
@@ -181,7 +181,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
@@ -309,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,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;
 

barretenberg/cpp/pil/vm2/ecc_mem.pil

@@ -8,67 +8,60 @@ include "precomputed.pil";
  * This handles the memory writes when the ECADD opcode is executed by user code.
  * 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) = (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
- * - rop[3]: q_x_addr
- * - rop[4]: q_y_addr
- * - rop[5]: q_is_inf_addr
- * - rop[6]: dst_addr
+ * - 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)
- *     - p_is_inf is tagged-checked by execution/registers to be U1 based on instruction spec.
- * - 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)
- *     - q_is_inf is tagged-checked by execution/registers to be U1 based on instruction spec.
- * - 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,
  * (1) DST_OUT_OF_BOUNDS_ACCESS: If the writes would access a memory address outside
  *     of the max AVM memory address (AVM_HIGHEST_MEM_ADDRESS).
  * (2) POINT_NOT_ON_CURVE: If either of the inputs (embedded curve points) do not
- *     satisfy the Grumpkin curve equation (SW form: Y^2 = X^3 − 17)
+ *     exist on the Grumpkin curve.
  *
  * TRACE SHAPE: This subtrace writes the values within 1 single row (i.e. 3 output columns)
  *
@@ -78,19 +71,27 @@ 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). We re-map any input infinity points to (0, 0)
- * so ECC correctly manages edge cases. Resulting infinity points are guaranteed to be (0, 0) by the
- * ECC subtrace (see #[OUTPUT_X_COORD] and #[OUTPUT_Y_COORD]).
+ * 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 (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.
+ *
+ * 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]).
  */
 
 namespace ecc_add_mem;
@@ -103,16 +104,17 @@ 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);
 
-    // p_is_inf, q_is_inf are constrained to be @boolean in the ecc subtrace (see #[INPUT_OUTPUT_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;
+
+    // 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])
 
     ////////////////////////////////////////////////
     // Error Handling - Out of Range Memory Access
@@ -121,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 };
 
@@ -142,6 +144,8 @@ namespace ecc_add_mem;
     pol commit sel_q_not_on_curve_err; // @boolean
     sel_q_not_on_curve_err * (1 - sel_q_not_on_curve_err) = 0;
 
+    // Note: The below additionally constrains that (X, Y) == (INFINITY_X, INFINITY_Y) ==> is_inf. See above description.
+
     // Y^2 = X^3 − 17, re-formulate to Y^2 - (X^3 - 17) = 0
     pol commit p_is_on_curve_eqn; // Needs to be committed to reduce relation degrees
     pol P_X3 = p_x * p_x * p_x;
@@ -170,32 +174,31 @@ 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);
 
-    // Needs to be committed columns as they are used in the lookups
-    pol commit p_x_n, p_y_n;
-    pol commit q_x_n, q_y_n;
-
-    // We re-map input infinity points to (0, 0) for ecc.pil. Output infinities are already constrained to be (0, 0) in the subtrace.
-    // Note that we cannot use p_x, p_y, etc. because they are read from memory in execution's #[DISPATCH_TO_ECC_ADD].
-    sel_should_exec * (p_x_n - (1 - p_is_inf) * p_x - p_is_inf * ecc.INFINITY_X) = 0;
-    sel_should_exec * (p_y_n - (1 - p_is_inf) * p_y - p_is_inf * ecc.INFINITY_Y) = 0;
-    sel_should_exec * (q_x_n - (1 - q_is_inf) * q_x - q_is_inf * ecc.INFINITY_X) = 0;
-    sel_should_exec * (q_y_n - (1 - q_is_inf) * q_y - q_is_inf * ecc.INFINITY_Y) = 0;
+    // 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]
+    sel * p_is_inf * (p_y - ecc.INFINITY_Y) = 0;
+    #[Q_INF_X_CHECK]
+    sel * q_is_inf * (q_x - ecc.INFINITY_X) = 0;
+    #[Q_INF_Y_CHECK]
+    sel * q_is_inf * (q_y - ecc.INFINITY_Y) = 0;
 
 
     #[INPUT_OUTPUT_ECC_ADD]
     sel_should_exec {
-        p_x_n, p_y_n, p_is_inf,
-        q_x_n, q_y_n, q_is_inf,
-        res_x, res_y, res_is_inf
+        p_x, p_y, p_is_inf,
+        q_x, q_y, q_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
     };
 
     ////////////////////////////////////////////////
@@ -216,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
-    };
-