Skip to content

Commit

Permalink
chore: add a couple of comments in the AVM range check gadget (#11402)
Browse files Browse the repository at this point in the history
  • Loading branch information
dbanks12 authored Jan 22, 2025
1 parent 6b0106c commit f1fd2d1
Showing 1 changed file with 5 additions and 1 deletion.
6 changes: 5 additions & 1 deletion barretenberg/cpp/pil/avm/gadgets/range_check.pil
Original file line number Diff line number Diff line change
Expand Up @@ -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;

Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down

0 comments on commit f1fd2d1

Please sign in to comment.