diff --git a/barretenberg/cpp/pil/avm/gadgets/range_check.pil b/barretenberg/cpp/pil/avm/gadgets/range_check.pil index d3d11168212..5121b67544d 100644 --- a/barretenberg/cpp/pil/avm/gadgets/range_check.pil +++ b/barretenberg/cpp/pil/avm/gadgets/range_check.pil @@ -60,10 +60,13 @@ namespace range_check(256); pol X_5 = is_lte_u96 * (u16_r0 + u16_r1 * 2**16 + u16_r2 * 2**32 + u16_r3 * 2**48 + u16_r4 * 2**64 + u16_r7 * 2**80); pol X_6 = is_lte_u112 * (u16_r0 + u16_r1 * 2**16 + u16_r2 * 2**32 + u16_r3 * 2**48 + u16_r4 * 2**64 + u16_r5 * 2**80 + u16_r7 * 2**96); pol X_7 = is_lte_u128 * (u16_r0 + u16_r1 * 2**16 + u16_r2 * 2**32 + u16_r3 * 2**48 + u16_r4 * 2**64 + u16_r5 * 2**80 + u16_r6 * 2**96 + u16_r7 * 2**112); + // NOTE: when doing a smaller range check (like is_lte_u48 which only uses u16_r0, u16_r1 and u16_r7), + // the values of inactive registers (u16_r2...6) are unconstrained // Since the is_lte_x are mutually exclusive, only one of the Xs will be non-zero pol RESULT = X_0 + X_1 + X_2 + X_3 + X_4 + X_5 + X_6 + X_7; + // Enforce that value can be derived from whichever slice registers are activated by an is_lte flag #[CHECK_RECOMPOSITION] sel_rng_chk * (RESULT - value) = 0; @@ -97,7 +100,7 @@ namespace range_check(256); // (b) u16_r7 is constrained by a 16-bit lookup table [0, 2^16 - 1] // 3) If the value of dyn_rng_chk_pow_2 > 2^16, i.e. dyn_rng_chk_bits is > 16, the condition (2a) will not hold // (a) [0, 2^16 - 1] = dyn_rng_chk_pow_2 - [0, 2^16 - 1] - 1 - // (b) from above, dyn_rng_check_pow_2 must be [0, 2^16] + // (b) from above, dyn_rng_check_pow_2 must be [0, 2^16] (remember from (1), dyn_rng_check_pow_2 is constrained to be a power of 2) // Some counter-examples // Assume a range check that the value 3 fits into 100 bits @@ -132,6 +135,7 @@ namespace range_check(256); // This lookup does 2 things (1) Indirectly range checks dyn_rng_chk_bits to not have underflowed and (2) Simplified calculation of 2^dyn_rng_chk_bits #[LOOKUP_RNG_CHK_POW_2] sel_rng_chk {dyn_rng_chk_bits, dyn_rng_chk_pow_2} in main.sel_rng_8 {main.clk, powers.power_of_2}; + // NOTE: `sel_rng_8` is chosen because it gives us rows [0, 256] which will give us all of the powers we need (plus many we don't need) // Now we need to perform the dynamic range check itself