-
Notifications
You must be signed in to change notification settings - Fork 191
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
- Loading branch information
1 parent
7cc47a6
commit a4c2681
Showing
23 changed files
with
1,940 additions
and
272 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,144 @@ | ||
| include "../main.pil"; | ||
| include "../fixed/powers.pil"; | ||
|
|
||
| namespace range_check(256); | ||
| pol commit clk; | ||
|
|
||
| // Range check selector | ||
| pol commit sel_rng_chk; | ||
| sel_rng_chk * (1 - sel_rng_chk) = 0; | ||
|
|
||
| // Witnesses | ||
| // Value to range check | ||
| pol commit value; | ||
| // Number of bits to check against | ||
| pol commit rng_chk_bits; | ||
|
|
||
| // Bit Size Cols - lowest 16-bit multiple that is greater than value | ||
| // TODO: Maybe we can get rid of is_lte_u128 since it's implicit if we have sel_rng_chk and no other is_lte_x | ||
| pol commit is_lte_u16; | ||
| pol commit is_lte_u32; | ||
| pol commit is_lte_u48; | ||
| pol commit is_lte_u64; | ||
| pol commit is_lte_u80; | ||
| pol commit is_lte_u96; | ||
| pol commit is_lte_u112; | ||
| pol commit is_lte_u128; | ||
| is_lte_u16 * (1 - is_lte_u16) = 0; | ||
| is_lte_u32 * (1 - is_lte_u32) = 0; | ||
| is_lte_u48 * (1 - is_lte_u48) = 0; | ||
| is_lte_u64 * (1 - is_lte_u64) = 0; | ||
| is_lte_u80 * (1 - is_lte_u80) = 0; | ||
| is_lte_u96 * (1 - is_lte_u96) = 0; | ||
| is_lte_u112 * (1 - is_lte_u112) = 0; | ||
| is_lte_u128 * (1 - is_lte_u128) = 0; | ||
|
|
||
| // Mutual Exclusivity condition | ||
| is_lte_u16 + is_lte_u32 + is_lte_u48 + is_lte_u64 + is_lte_u80 + is_lte_u96 + is_lte_u112 + is_lte_u128 = sel_rng_chk; | ||
|
|
||
| // Eight 16-bit slice registers | ||
| pol commit u16_r0; | ||
| pol commit u16_r1; | ||
| pol commit u16_r2; | ||
| pol commit u16_r3; | ||
| pol commit u16_r4; | ||
| pol commit u16_r5; | ||
| pol commit u16_r6; | ||
| // This register has a (more expensive) set of constraint that enables dynamic range check of bit values between 0 and 16 bits | ||
| pol commit u16_r7; | ||
|
|
||
| // In each of these relations, the u16_r7 register contains the most significant 16 bits of value. | ||
| pol X_0 = is_lte_u16 * u16_r7; | ||
| pol X_1 = is_lte_u32 * (u16_r0 + u16_r7 * 2**16); | ||
| pol X_2 = is_lte_u48 * (u16_r0 + u16_r1 * 2**16 + u16_r7 * 2**32); | ||
| pol X_3 = is_lte_u64 * (u16_r0 + u16_r1 * 2**16 + u16_r2 * 2**32 + u16_r7 * 2**48); | ||
| pol X_4 = is_lte_u80 * (u16_r0 + u16_r1 * 2**16 + u16_r2 * 2**32 + u16_r3 * 2**48 + u16_r7 * 2**64); | ||
| 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); | ||
|
|
||
| // 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; | ||
|
|
||
| #[CHECK_RECOMPOSITION] | ||
| sel_rng_chk * (RESULT - value) = 0; | ||
|
|
||
| // The number of bits that form the dynamic range check is depending on the claimed lte value and the witness rng_chk_bits | ||
| // claimed is_lte_x | dyn_rng_chk_bits | ||
| // -----------------|----------------- | ||
| // is_lte_u16 | rng_chk_bits | ||
| // is_lte_u32 | rng_chk_bits - 16 | ||
| // is_lte_u48 | rng_chk_bits - 32 | ||
| // is_lte_u64 | rng_chk_bits - 48 | ||
| // is_lte_u80 | rng_chk_bits - 64 | ||
| // is_lte_u96 | rng_chk_bits - 80 | ||
| // is_lte_u112 | rng_chk_bits - 96 | ||
| // is_lte_u128 | rng_chk_bits - 112 | ||
|
|
||
| // The number of bits that need to be dynamically range checked. | ||
| pol commit dyn_rng_chk_bits; | ||
| // Valid values for dyn_rng_chk_bits are in the range [0, 16] | ||
| dyn_rng_chk_bits - (rng_chk_bits - (is_lte_u32 * 16) - (is_lte_u48 * 32) - (is_lte_u64 * 48) - (is_lte_u80 * 64) - (is_lte_u96 * 80) - (is_lte_u112 * 96) - (is_lte_u128 * 112)) = 0; | ||
|
|
||
| // To perform the dynamic range check we also need the value of 2^dyn_rng_chk_bits | ||
| pol commit dyn_rng_chk_pow_2; | ||
|
|
||
| // 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}; | ||
|
|
||
|
|
||
| // Now we need to perform the dynamic range check itself | ||
| // We check that u16_r7 < dyn_rng_chk_pow_2 ==> dyn_rng_chk_pow_2 - u16_r7 - 1 > 0 | ||
| pol commit dyn_diff; | ||
| sel_rng_chk * (dyn_diff - (dyn_rng_chk_pow_2 - u16_r7 - 1)) = 0; | ||
| // The value of dyn_diff has to be between [0, 2^16) | ||
| // To check we did not underflow we just range check it | ||
| #[LOOKUP_RNG_CHK_DIFF] | ||
| sel_rng_chk { dyn_diff } in main.sel_rng_16 { main.clk }; | ||
|
|
||
|
|
||
| // Lookup relations. | ||
| // We only need these relatiosn while we dont support pol in the LHS selector | ||
| pol commit sel_lookup_0; | ||
| pol commit sel_lookup_1; | ||
| pol commit sel_lookup_2; | ||
| pol commit sel_lookup_3; | ||
| pol commit sel_lookup_4; | ||
| pol commit sel_lookup_5; | ||
| pol commit sel_lookup_6; | ||
|
|
||
| // The lookups are cumulative - i.e. every value greater than 16 bits involve sel_lookup_0 | ||
| // Note that the lookup for the u16_r7 is always active (dynamic range check) | ||
| sel_lookup_0 - (is_lte_u32 + is_lte_u48 + is_lte_u64 + is_lte_u80 + is_lte_u96 + is_lte_u112 + is_lte_u128) = 0; | ||
| sel_lookup_1 - (is_lte_u48 + is_lte_u64 + is_lte_u80 + is_lte_u96 + is_lte_u112 + is_lte_u128) = 0; | ||
| sel_lookup_2 - (is_lte_u64 + is_lte_u80 + is_lte_u96 + is_lte_u112 + is_lte_u128) = 0; | ||
| sel_lookup_3 - (is_lte_u80 + is_lte_u96 + is_lte_u112 + is_lte_u128) = 0; | ||
| sel_lookup_4 - (is_lte_u96 + is_lte_u112 + is_lte_u128) = 0; | ||
| sel_lookup_5 - (is_lte_u112 + is_lte_u128) = 0; | ||
| sel_lookup_6 - is_lte_u128 = 0; | ||
|
|
||
| #[LOOKUP_RNG_CHK_0] | ||
| sel_lookup_0 { u16_r0 } in main.sel_rng_16 { main.clk }; | ||
|
|
||
| #[LOOKUP_RNG_CHK_1] | ||
| sel_lookup_1 { u16_r1 } in main.sel_rng_16 { main.clk }; | ||
|
|
||
| #[LOOKUP_RNG_CHK_2] | ||
| sel_lookup_2 { u16_r2 } in main.sel_rng_16 { main.clk }; | ||
|
|
||
| #[LOOKUP_RNG_CHK_3] | ||
| sel_lookup_3 { u16_r3 } in main.sel_rng_16 { main.clk }; | ||
|
|
||
| #[LOOKUP_RNG_CHK_4] | ||
| sel_lookup_4 { u16_r4 } in main.sel_rng_16 { main.clk }; | ||
|
|
||
| #[LOOKUP_RNG_CHK_5] | ||
| sel_lookup_5 { u16_r5 } in main.sel_rng_16 { main.clk }; | ||
|
|
||
| #[LOOKUP_RNG_CHK_6] | ||
| sel_lookup_6 { u16_r6 } in main.sel_rng_16 { main.clk }; | ||
|
|
||
| #[LOOKUP_RNG_CHK_7] | ||
| sel_rng_chk { u16_r7 } in main.sel_rng_16 { main.clk }; | ||
|
|
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Oops, something went wrong.