ff_gt.pil

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 |
// +-----+-----+--------+--------------+--------------+------------+------------+------+------+------------+------------+--------+--------+-------------+-----+--------+---------------+
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;