feat(avm): Port field gt to vm2

barretenberg/cpp/pil/vm2/execution.pil

@@ -16,6 +16,7 @@ include "poseidon2_hash.pil";
 include "poseidon2_perm.pil";
 include "scalar_mul.pil";
 include "to_radix.pil";
+include "ff_gt.pil";
 
 namespace execution;
 

barretenberg/cpp/pil/vm2/ff_gt.pil

@@ -0,0 +1,218 @@
+include "./range_check.pil";
+
+// This module handles field gt
+// GT also enables us to support LT (by swapping the inputs of GT) and LTE (by negating the result of GT)
+// Lifecycle table:
+// +-----+-----+--------+--------------+--------------+------------+------------+------+------+------------+------------+--------+--------+-------------+-----+--------+---------------+
+// |  a  |  b  | result | a_hi (range) | a_lo (range) | p_sub_a_hi | p_sub_a_lo | b_hi | b_lo | p_sub_b_hi | p_sub_b_lo | res_hi | res_lo | cmp_rng_ctr | sel | sel_gt | sel_shift_rng |
+// +-----+-----+--------+--------------+--------------+------------+------------+------+------+------------+------------+--------+--------+-------------+-----+--------+---------------+
+// | 0   | 0   | 0      | 0            | 0            | 0          | 0          | 0    | 0    | 0          | 0          | 0      | 0      |           0 |   0 |      0 |             0 |
+// | 27  | 28  | 0      | 0            | 27           | x1         | x2         | 0    | 28   | y1         | y2         | 0      | 1      |           4 |   1 |      1 |             1 | <== lookup here
+// | unc | unc | unc    | x1           | x2           | 0          | 28         | y1   | y2   | 0          | 1          | unc    | unc    |           3 |   1 |      0 |             1 |
+// | unc | unc | unc    | 0            | 28           | y1         | y2         | 0    | 1    | unc        | unc        | unc    | unc    |           2 |   1 |      0 |             1 |
+// | unc | unc | unc    | y1           | y2           | 0          | 1          | unc  | unc  | unc        | unc        | unc    | unc    |           1 |   1 |      0 |             1 |
+// | unc | unc | unc    | 0            | 1            | unc        | unc        | unc  | unc  | unc        | unc        | unc    | unc    |           0 |   1 |      0 |             0 |
+// | 0   | 0   | 0      | 0            | 0            | 0          | 0          | 0    | 0    | 0          | 0          | 0      | 0      |           0 |   0 |      0 |             0 |
+// +-----+-----+--------+--------------+--------------+------------+------------+------+------+------------+------------+--------+--------+-------------+-----+--------+---------------+
+//
+// This trace should be looked up with the tuple (a,b,result,sel_gt)
+namespace ff_gt;
+    pol commit sel;
+    sel * (1 - sel) = 0;
+
+    #[skippable_if]
+    sel = 0;
+
+    // These are the i/o for the gadget
+    pol commit a;
+    pol commit b;
+    pol commit result;
+    (result * (1 - result)) = 0;
+
+    // Should be looked up based on this selector
+    // This will be off when doing the shifts for the remaning range constraints.
+    pol commit sel_gt;
+    sel_gt * (1 - sel_gt) = 0;
+
+    // TODO: Commited because lookups don't support constants
+    pol commit constant_128;
+    sel * (128 - constant_128) = 0;
+
+    pol POW_128 = 2 ** 128;
+    pol P_LO = 53438638232309528389504892708671455233; // Lower 128 bits of p
+    pol P_HI = 64323764613183177041862057485226039389; // Upper 128 bits of p
+
+    // ========= A DECOMPOSITION =========
+
+    pol commit a_lo;
+    pol commit a_hi;
+
+    #[A_DECOMPOSITION]
+    sel_gt * (a - (a_lo + POW_128 * a_hi)) = 0;
+
+    // We only do 2 range checks per row.
+    // We'll shift the other 8 range checks necessary in 4 rows after the sel_gt one.
+
+    #[A_LO_RANGE]
+    sel { a_lo, constant_128 }
+    in range_check.sel { range_check.value, range_check.rng_chk_bits };
+
+    #[A_HI_RANGE]
+    sel { a_hi, constant_128 }
+    in range_check.sel { range_check.value, range_check.rng_chk_bits };
+
+    pol commit p_a_borrow;
+    p_a_borrow * (1 - p_a_borrow) = 0;
+
+    pol commit p_sub_a_lo; // p_lo - a_lo
+    pol commit p_sub_a_hi; // p_hi - a_hi
+
+    #[P_SUB_A_LO]
+    sel_gt * (p_sub_a_lo - (P_LO - a_lo - 1 + p_a_borrow * POW_128)) = 0;
+    #[P_SUB_A_HI]
+    sel_gt * (p_sub_a_hi - (P_HI - a_hi - p_a_borrow)) = 0;
+
+    // ========= B DECOMPOSITION =========
+
+    pol commit b_lo;
+    pol commit b_hi;
+
+    #[B_DECOMPOSITION]
+    sel_gt * (b - (b_lo + POW_128 * b_hi)) = 0;
+
+    pol commit p_b_borrow;
+    p_b_borrow * (1 - p_b_borrow) = 0;
+
+    pol commit p_sub_b_lo;
+    pol commit p_sub_b_hi;
+
+    // Check that decomposition of b into lo and hi limbs do not overflow/underflow p.
+    // This is achieved by checking (p_lo > b_lo && p_hi >= b_hi) || (p_lo <= b_lo && b_hi > b_hi)
+    // First condition is if borrow = 0, second condition is if borrow = 1;
+    #[P_SUB_B_LO]
+    sel_gt * (p_sub_b_lo - (P_LO - b_lo - 1 + p_b_borrow * POW_128)) = 0;
+    #[P_SUB_B_HI]
+    sel_gt * (p_sub_b_hi - (P_HI - b_hi - p_b_borrow)) = 0;
+
+    // ========= GT OPERATION =========
+
+    pol commit borrow;
+
+    // Calculate the combined relation: (a - b - 1) * q + (b - a ) * (1-q)
+    // Check that (a > b) by checking (a_lo > b_lo && a_hi >= bhi) || (alo <= b_lo && a_hi > b_hi)
+    // First condition is if borrow = 0, second condition is if borrow = 1;
+    pol A_SUB_B_LO = a_lo - b_lo - 1 + borrow * POW_128;
+    pol A_SUB_B_HI = a_hi - b_hi - borrow;
+
+    // Check that (a <= b) by checking (b_lo >= a_lo && b_hi >= a_hi) || (b_lo < a_lo && b_hi > a_hi)
+    // First condition is if borrow = 0, second condition is if borrow = 1;
+    pol B_SUB_A_LO = b_lo - a_lo + borrow * POW_128;
+    pol B_SUB_A_HI = b_hi - a_hi - borrow;
+
+    pol IS_GT = sel_gt * result;
+    // When IS_GT = 1, we enforce the condition that a > b and thus a - b - 1 does not underflow.
+    // When IS_GT = 0, we enforce the condition that a <= b and thus b - a does not underflow.
+    // ========= Analysing res_lo and res_hi scenarios for LTE =================================
+    // (1) Assume a proof satisfies the constraints for LTE(x,y,1), i.e., x <= y
+    //     Therefore ia = x, ib = y and ic = 1.
+    //    (a) We do not swap the operands, so a = x and b = y,
+    //    (b) IS_GT = 1 - ic = 0
+    //    (c) res_lo = B_SUB_A_LO and res_hi = B_SUB_A_HI
+    //    (d) res_lo = y_lo - x_lo + borrow * 2**128 and res_hi = y_hi - x_hi - borrow.
+    //    (e) Due to 128-bit range checks on res_lo, res_hi, y_lo, x_lo, y_hi, x_hi, we
+    //        have the guarantee that res_lo >= 0 && res_hi >= 0. Furthermore, borrow is
+    //        boolean and so we have two cases to consider:
+    //         (i)  borrow == 0 ==> y_lo >= x_lo && y_hi >= x_hi
+    //         (ii) borrow == 1 ==> y_hi >= x_hi + 1 ==> y_hi > x_hi
+    //        This concludes the proof as for both cases, we must have: y >= x
+    //
+    // (2) Assume a proof satisfies the constraints for LTE(x,y,0), i.e. x > y.
+    //     Therefore ia = x, ib = y and ic = 0.
+    //    (a) We do not swap the operands, so a = x and b = y,
+    //    (b) IS_GT = 1 - ic = 1
+    //    (c) res_lo = A_SUB_B_LO and res_hi = A_SUB_B_HI
+    //    (d) res_lo = x_lo - y_lo - 1 + borrow * 2**128 and res_hi = x_hi - y_hi - borrow.
+    //    (e) Due to 128-bit range checks on res_lo, res_hi, y_lo, x_lo, y_hi, x_hi, we
+    //        have the guarantee that res_lo >= 0 && res_hi >= 0. Furthermore, borrow is
+    //        boolean and so we have two cases to consider:
+    //         (i)  borrow == 0 ==> x_lo > y_lo && x_hi >= y_hi
+    //         (ii) borrow == 1 ==> x_hi > y_hi
+    //        This concludes the proof as for both cases, we must have: x > y
+    //
+
+    // ========= Analysing res_lo and res_hi scenarios for LT ==================================
+    // (1) Assume a proof satisfies the constraints for LT(x,y,1), i.e. x < y.
+    //     Therefore ia = x, ib = y and ic = 1.
+    //    (a) We DO swap the operands, so a = y and b = x,
+    //    (b) IS_GT = ic = 1
+    //    (c) res_lo = A_SUB_B_LO and res_hi = A_SUB_B_HI, **remember we have swapped inputs**
+    //    (d) res_lo = y_lo - x_lo - 1 + borrow * 2**128 and res_hi = y_hi - x_hi - borrow.
+    //    (e) Due to 128-bit range checks on res_lo, res_hi, y_lo, x_lo, y_hi, x_hi, we
+    //        have the guarantee that res_lo >= 0 && res_hi >= 0. Furthermore, borrow is
+    //        boolean and so we have two cases to consider:
+    //         (i)  borrow == 0 ==> y_lo > x_lo && y_hi >= x_hi
+    //         (ii) borrow == 1 ==> y_hi > x_hi
+    //        This concludes the proof as for both cases, we must have: x < y
+    //
+    // (2) Assume a proof satisfies the constraint for LT(x,y,0), i.e. x >= y.
+    //     Therefore ia = x, ib = y and ic = 0.
+    //    (a) We DO swap the operands, so a = y and b = x,
+    //    (b) IS_GT = ic = 0
+    //    (c) res_lo = B_SUB_A_LO and res_hi = B_SUB_A_HI, **remember we have swapped inputs**
+    //    (d) res_lo = a_lo - y_lo + borrow * 2**128 and res_hi = a_hi - y_hi - borrow.
+    //    (e) Due to 128-bit range checks on res_lo, res_hi, y_lo, x_lo, y_hi, x_hi, we
+    //        have the guarantee that res_lo >= 0 && res_hi >= 0. Furthermore, borrow is
+    //        boolean and so we have two cases to consider:
+    //         (i)  borrow == 0 ==> x_lo >= y_lo && x_hi >= y_hi
+    //         (ii) borrow == 1 ==> x_hi > y_hi
+    //        This concludes the proof as for both cases, we must have: x >= y
+    pol commit res_lo;
+    pol commit res_hi;
+    #[RES_LO]
+    sel_gt * (res_lo - (A_SUB_B_LO * IS_GT + B_SUB_A_LO * (1 - IS_GT))) = 0;
+    #[RES_HI]
+    sel_gt * (res_hi - (A_SUB_B_HI * IS_GT + B_SUB_A_HI * (1 - IS_GT))) = 0;
+
+
+    // ========= SHIFTS FOR RANGE CHECKS =========
+
+    // Each call to GT requires 5x 256-bit range checks. We keep track of how many are left here.
+    pol commit cmp_rng_ctr;
+
+    // if this row is a comparison operation, the next range_check_remaining value is set to 5
+    #[SET_RNG_CTR]
+    sel_gt * (cmp_rng_ctr - 4) = 0;
+
+    // the number of range checks must decrement by 1 until it is equal to 0;
+    #[SUB_RNG_CTR]
+    cmp_rng_ctr * (cmp_rng_ctr - 1 - cmp_rng_ctr') = 0;
+
+    pol commit sel_shift_rng;
+    sel_shift_rng * (1 - sel_shift_rng) = 0;
+
+    pol commit cmp_rng_ctr_inv;
+
+    // sel_shift_rng = 1 when cmp_rng_ctr != 0 and sel_shift_rng = 0 when cmp_rng_ctr = 0;
+    #[RNG_CTR_NON_ZERO]
+    cmp_rng_ctr * ((1 - sel_shift_rng) * (1 -  cmp_rng_ctr_inv) +  cmp_rng_ctr_inv) - sel_shift_rng = 0;
+
+    // We shift the stuff that we have to range check to the left, so a_lo and a_hi (which are doing the range checks)
+    // receive the shifted values, two on every row.
+    #[SHIFT_0]
+    (a_lo' - p_sub_a_lo) * sel_shift_rng = 0;
+    (a_hi' - p_sub_a_hi) * sel_shift_rng = 0;
+    #[SHIFT_1]
+    (p_sub_a_lo' - b_lo) * sel_shift_rng = 0;
+    (p_sub_a_hi' - b_hi) * sel_shift_rng = 0;
+    #[SHIFT_2]
+    (b_lo' - p_sub_b_lo) * sel_shift_rng = 0;
+    (b_hi' - p_sub_b_hi) * sel_shift_rng = 0;
+    #[SHIFT_3]
+    (p_sub_b_lo' - res_lo) * sel_shift_rng = 0;
+    (p_sub_b_hi' - res_hi) * sel_shift_rng = 0;
+
+    // ========= SELECTOR =========
+    // Selector should be on on the whole 5 rows that are required for the gt operations + range checks.
+    // So if sel_gt is on, sel should be on, but also if the previous one had sel_shift_rng on.
+    #[SEL_CONSISTENCY]
+    sel_shift_rng + sel_gt' - sel' = 0;