feat: WIP quick pil changes exploring removing is inf (no opcode changes yet)

Author: MirandaWood

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

@@ -307,6 +307,7 @@ namespace address_derivation;
 
     // Enforces address_point = preaddress_public_key + incoming_viewing_key on Grumpkin, and that
     // address = address_point.x.
+    // TODO(MW): Remove result_infinity?
     #[ADDRESS_ECADD]
     sel {
         preaddress_public_key_x, preaddress_public_key_y, precomputed.zero,
@@ -315,7 +316,7 @@ namespace address_derivation;
     } 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, ecc.result_infinity
     };
 
     // Note: We can safely assume the address point is not infinity since that would imply either

barretenberg/cpp/pil/vm2/ecc.pil

@@ -6,23 +6,32 @@
  * 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:
+ *
+ * MW NOTE: USING APPROACH 1 BELOW:
+ * 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
  *        };
  *
+ * MW 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.
+ *
  * TRACE SHAPE: 1 single row per computation (P + Q = R).
  *
  * INTERACTIONS: This subtrace is looked up by:
@@ -41,11 +50,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 +83,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 +160,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 +195,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

@@ -24,50 +24,38 @@ include "precomputed.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,11 +72,11 @@ 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]).
@@ -103,9 +91,7 @@ include "precomputed.pil";
  * 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.
- *
+ * MW NOTE: Still using p_is_inf, q_is_inf just as flags to tell ecc.pil how to treat the points.
  * 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:
  *  - (0, 0) ==> is_inf by #[P/Q_ON_CURVE_CHECK] (zero coordinates will fail this relation unless is_inf is set correctly).
@@ -123,17 +109,16 @@ 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;
 
+    // MW NOTE: Still using p_is_inf, q_is_inf just as flags to tell ecc.pil how to treat the points.
     // 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 +130,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,10 +181,14 @@ 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);
 
+    // MW NOTE: Still using p_is_inf, q_is_inf just as flags to tell ecc.pil how to treat the points.
+    // MW NOTE: Output inifinities - in ecc.pil, if result_infinity, then r_x = INFINITY_X = 0, r_y = INFINITY_Y = 0.
+    // Sufficient to just lookup res_x, res_y here?
+
     // 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.
@@ -217,12 +206,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
     };
 
     ////////////////////////////////////////////////
@@ -244,11 +233,11 @@ namespace ecc_add_mem;
         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
-    };
+    // #[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/scalar_mul.pil

@@ -175,11 +175,12 @@ namespace scalar_mul;
     end * (temp_y - point_y) = 0;
     end * (temp_inf - point_inf) = 0;
 
+    // TODO(MW): Remove result_infinity?
     #[DOUBLE]
     sel_not_end { temp_x, temp_y, temp_inf, temp_x', temp_y', temp_inf', sel_not_end /* = 1 */ }
     in
     ecc.sel
-        { ecc.r_x, ecc.r_y, ecc.r_is_inf, ecc.p_x, ecc.p_y, ecc.p_is_inf, ecc.double_op };
+        { ecc.r_x, ecc.r_y, ecc.result_infinity, ecc.p_x, ecc.p_y, ecc.p_is_inf, ecc.double_op };
 
     ///////////////////////////////
     // Result Computation
@@ -203,11 +204,12 @@ namespace scalar_mul;
     SHOULD_PASS * (res_y - res_y') = 0;
     SHOULD_PASS * (res_inf - res_inf') = 0;
 
+    // TODO(MW): Remove result_infinity?
     #[ADD]
     should_add { res_x, res_y, res_inf, res_x', res_y', res_inf', temp_x, temp_y, temp_inf }
     in
     ecc.sel
-        { ecc.r_x, ecc.r_y, ecc.r_is_inf, 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.result_infinity, ecc.p_x, ecc.p_y, ecc.p_is_inf, ecc.q_x, ecc.q_y, ecc.q_is_inf };