@@ -39,7 +39,7 @@ sel = 0;
3939pol commit cf;
4040
4141// Generic helper column
42- // Current use: EQ (inverse of a-b) & DIV (remainder)
42+ // Current use: EQ (inverse of a-b), DIV (remainder), and SHL (2**ib )
4343pol commit helper1;
4444
4545// maximum bits the number can hold (i.e. 8 for a u8):
@@ -95,7 +95,7 @@ execution.sel_execute_alu {
9595
9696// IS_FF CHECKING
9797
98- pol CHECK_TAG_FF = sel_op_div + sel_op_fdiv + sel_op_lt + sel_op_lte + sel_op_not;
98+ pol CHECK_TAG_FF = sel_op_div + sel_op_fdiv + sel_op_lt + sel_op_lte + sel_op_not + sel_shift_ops ;
9999// We prove that sel_is_ff == 1 <==> ia_tag == MEM_TAG_FF
100100pol TAG_FF_DIFF = ia_tag - constants.MEM_TAG_FF;
101101pol commit tag_ff_diff_inv;
@@ -113,7 +113,7 @@ CHECK_TAG_U128 * (TAG_U128_DIFF * (sel_is_u128 * (1 - tag_u128_diff_inv) + tag_u
113113
114114// TAG CHECKING
115115
116- pol EXPECTED_C_TAG = (sel_op_add + sel_op_sub + sel_op_mul + sel_op_div + sel_op_truncate + sel_op_shr + sel_op_shl ) * ia_tag + (sel_op_eq + sel_op_lt + sel_op_lte) * constants.MEM_TAG_U1 + sel_op_fdiv * constants.MEM_TAG_FF;
116+ pol EXPECTED_C_TAG = (sel_op_add + sel_op_sub + sel_op_mul + sel_op_div + sel_op_truncate + sel_shift_ops ) * ia_tag + (sel_op_eq + sel_op_lt + sel_op_lte) * constants.MEM_TAG_U1 + sel_op_fdiv * constants.MEM_TAG_FF;
117117
118118// The tag of c is generated by the opcode and is never wrong.
119119// Gating with (1 - sel_tag_err) is necessary because when an error occurs, we have to set the tag to 0,
@@ -125,22 +125,22 @@ pol commit sel_tag_err;
125125sel_tag_err * (1 - sel_tag_err) = 0;
126126
127127// Tag errors currently have cases:
128- // 1. Input tagged as a field for NOT or DIV operations or non-field for FDIV operation
128+ // 1. Input tagged as a field for NOT, DIV, or shift operations or non-field for FDIV operation
129129// 2. Mismatched tags for inputs a and b for all opcodes apart from TRUNC
130130// 1 is handled by checking FF_TAG_ERR in TAG_ERR_CHECK and 2 is handled in AB_TAGS_CHECK.
131- pol FF_TAG_ERR = (sel_op_div + sel_op_not) * sel_is_ff + sel_op_fdiv * IS_NOT_FF;
131+ pol FF_TAG_ERR = (sel_op_div + sel_op_not + sel_shift_ops ) * sel_is_ff + sel_op_fdiv * IS_NOT_FF;
132132pol commit sel_ab_tag_mismatch;
133133sel_ab_tag_mismatch * (1 - sel_ab_tag_mismatch) = 0;
134134
135- // TODO(MW): It's technically possible to have BOTH cases be true if we perform a DIV with FF ib and integer ia,
135+ // TODO(MW): It's technically possible to have BOTH cases be true if we perform a DIV or shift with FF ib and integer ia,
136136// so for now I take sel_ab_tag_mismatch * FF_TAG_ERR.
137137#[TAG_ERR_CHECK]
138138sel_tag_err = sel_ab_tag_mismatch + FF_TAG_ERR - sel_ab_tag_mismatch * FF_TAG_ERR;
139139
140140// For NOT opcode, an error occurs if the tag of a is FF. In this case, tracegen will set
141141// b's tag as 0 which, while it would currently pass the checks below, is not a tag inequality we
142142// want to throw with sel_ab_tag_mismatch:
143- pol CHECK_AB_TAGS = 1 - sel_op_not * sel_is_ff - sel_op_truncate - sel_op_shr - sel_op_shl; // note: shifts are temporary, they should be subject to AB checks
143+ pol CHECK_AB_TAGS = 1 - sel_op_not * sel_is_ff - sel_op_truncate;
144144pol AB_TAGS_EQ = 1 - sel_ab_tag_mismatch;
145145pol commit ab_tags_diff_inv;
146146// Prove that sel_ab_tag_mismatch = 1 <==> we have a disallowed inequality between the tags:
@@ -150,6 +150,52 @@ CHECK_AB_TAGS * ( (ia_tag - ib_tag) * ( AB_TAGS_EQ * (1 - ab_tags_diff_inv) + ab
150150#[TAG_MAX_BITS_VALUE]
151151sel { ia_tag, max_bits, max_value } in precomputed.sel_tag_parameters { precomputed.clk, precomputed.tag_max_bits, precomputed.tag_max_value };
152152
153+ // BIT DECOMPOSITION
154+
155+ // We use the below to prove correct decomposition of limbs. Currently used by MUL, DIV, SHL, and SHR.
156+ pol commit sel_decompose_a;
157+ // #[OP_ID_CHECK] ensures selectors are mutually exclusive:
158+ sel_decompose_a = sel_mul_div_u128 + sel_shift_ops * IS_NOT_FF;
159+ // Currently, sel_decompose_b would just equal sel_mul_div_u128, so no need for another column.
160+ pol commit a_lo, a_hi, b_lo, b_hi;
161+ pol TWO_POW_64 = 2 ** 64;
162+
163+ // Reusing columns for decomposition (#[OP_ID_CHECK] ensures selectors are mutually exclusive):
164+ pol DECOMPOSED_A = ((sel_mul_u128 + sel_shift_ops_no_overflow) * ia) + (sel_shift_ops - sel_shift_ops_no_overflow) * (ib - max_bits) + (sel_is_u128 * sel_op_div * (1 - sel_tag_err) * ic);
165+ pol DECOMPOSED_B = ib;
166+ // For MUL and DIV, we decompose into 64 bit limbs. For shifts, we have one limb of b bits and one limb of max_bits - b bits.
167+ pol LIMB_SIZE = sel_mul_div_u128 * TWO_POW_64 + sel_shift_ops * two_pow_shift_lo_bits;
168+
169+ #[A_DECOMPOSITION]
170+ sel_decompose_a * (DECOMPOSED_A - (a_lo + LIMB_SIZE * a_hi)) = 0;
171+ #[B_DECOMPOSITION]
172+ sel_mul_div_u128 * (DECOMPOSED_B - (b_lo + LIMB_SIZE * b_hi)) = 0;
173+
174+ // Note: the only current use for decomposition of b has 64 bit limbs, so no need for b_lo/hi_bits.
175+ pol commit a_lo_bits, a_hi_bits;
176+ // TODO: Once lookups support expression in tuple, we can inline constant_64 into the lookup.
177+ // Note: only currently used for MUL/DIV u128, so gated by sel_mul_div_u128:
178+ pol commit constant_64;
179+ sel_mul_div_u128 * (64 - constant_64) = 0;
180+
181+ #[A_LO_BITS]
182+ a_lo_bits - sel_mul_div_u128 * constant_64 - sel_shift_ops * shift_lo_bits = 0;
183+
184+ #[A_HI_BITS]
185+ a_hi_bits - sel_mul_div_u128 * constant_64 - sel_shift_ops * SHIFT_HI_BITS = 0;
186+
187+ #[RANGE_CHECK_DECOMPOSITION_A_LO]
188+ sel_decompose_a { a_lo, a_lo_bits } in range_check.sel { range_check.value, range_check.rng_chk_bits };
189+
190+ #[RANGE_CHECK_DECOMPOSITION_A_HI]
191+ sel_decompose_a { a_hi, a_hi_bits } in range_check.sel { range_check.value, range_check.rng_chk_bits };
192+
193+ #[RANGE_CHECK_DECOMPOSITION_B_LO]
194+ sel_mul_div_u128 { b_lo, constant_64 } in range_check.sel { range_check.value, range_check.rng_chk_bits };
195+
196+ #[RANGE_CHECK_DECOMPOSITION_B_HI]
197+ sel_mul_div_u128 { b_hi, constant_64 } in range_check.sel { range_check.value, range_check.rng_chk_bits };
198+
153199
154200// ADD
155201
@@ -194,21 +240,6 @@ sel_mul_u128 = sel_is_u128 * sel_op_mul;
194240// a * b_l + a_l * b_h * 2^64 = (cf * 2^64 + c_hi) * 2^128 + c
195241// => no need for a_h in final relation
196242
197- pol commit a_lo;
198- pol commit a_hi;
199- pol commit b_lo;
200- pol commit b_hi;
201- pol TWO_POW_64 = 2 ** 64;
202-
203- // Reusing columns for decomposition (#[OP_ID_CHECK] ensures selectors are mutually exclusive):
204- pol DECOMPOSED_A = (sel_mul_u128 * ia) + (sel_is_u128 * sel_op_div * (1 - sel_tag_err) * ic);
205- pol DECOMPOSED_B = ib;
206-
207- #[A_DECOMPOSITION]
208- sel_mul_div_u128 * (DECOMPOSED_A - (a_lo + TWO_POW_64 * a_hi)) = 0;
209- #[B_DECOMPOSITION]
210- sel_mul_div_u128 * (DECOMPOSED_B - (b_lo + TWO_POW_64 * b_hi)) = 0;
211-
212243#[ALU_MUL_U128]
213244sel_mul_u128 * (1 - sel_tag_err)
214245 * (
@@ -217,23 +248,6 @@ sel_mul_u128 * (1 - sel_tag_err)
217248 - (max_value + 1) * (cf * TWO_POW_64 + c_hi) // c_hi * 2^128 + (cf ? 2^192 : 0)
218249 ) = 0;
219250
220- // TODO: Once lookups support expression in tuple, we can inline constant_64 into the lookup.
221- // Note: only used for MUL/DIV u128, so gated by sel_mul_div_u128
222- pol commit constant_64;
223- sel_mul_div_u128 * (64 - constant_64) = 0;
224-
225- #[RANGE_CHECK_MUL_U128_A_LO]
226- sel_mul_div_u128 { a_lo, constant_64 } in range_check.sel { range_check.value, range_check.rng_chk_bits };
227-
228- #[RANGE_CHECK_MUL_U128_A_HI]
229- sel_mul_div_u128 { a_hi, constant_64 } in range_check.sel { range_check.value, range_check.rng_chk_bits };
230-
231- #[RANGE_CHECK_MUL_U128_B_LO]
232- sel_mul_div_u128 { b_lo, constant_64 } in range_check.sel { range_check.value, range_check.rng_chk_bits };
233-
234- #[RANGE_CHECK_MUL_U128_B_HI]
235- sel_mul_div_u128 { b_hi, constant_64 } in range_check.sel { range_check.value, range_check.rng_chk_bits };
236-
237251// No need to range_check c_hi for cases other than u128 because we know a and b's size from the tags and have looked
238252// up max_value. i.e. we cannot provide a malicious c, c_hi such that a + b - c_hi * 2^n = c passes for n < 128.
239253// No need to range_check c_lo = ic because the memory write will ensure ic <= max_value.
@@ -392,6 +406,87 @@ sel_op_not * (1 - sel_op_not) = 0;
392406#[NOT_OP_MAIN]
393407sel_op_not * (1 - sel_tag_err) * (ia + ib - max_value) = 0;
394408
409+ // SHIFTS - Taken from vm1:
410+ // Given (1) an input a, within the range [0, 2**128-1],
411+ // (2) a value s, the amount of bits to shift a by (stored in ib),
412+ // (3) and a memory tag, mem_tag that supports a maximum of t bits (stored in max_bits).
413+ // Split input a into Big Endian hi and lo limbs, (we re-use the a_hi and a_lo columns we used for the MUL/DIV u128 operators)
414+ // a_hi and a_lo, and the number of bits represented by the memory tag, t.
415+ // If we are shifting by more than the bit length represented by the memory tag, the result is trivially zero.
416+
417+ // SHL
418+
419+ // === Steps when performing SHL
420+ // (1) Prove the correct decomposition: a_hi * 2**(t-s) + a_lo = a ---> see #[A_DECOMPOSITION]
421+ // (2) Range check a_hi < 2**s && a_lo < 2**(t-s) ---> see #[RANGE_CHECK_DECOMPOSITION_A_LO/HI]
422+ // (3) Return a_lo * 2**s ---> see #[ALU_SHL]
423+ //
424+ // <-- s bits --> | <-- (t-s) bits -->
425+ // ------------------|-------------------
426+ // | a_hi | a_lo | --> a
427+ // --------------------------------------
428+ //
429+ // Use of helper1 for SHL:
430+ // We have: s (=ib), t (=max_bits), 2**(t-s) (=two_pow_shift_lo_bits), and 2**t (=max_value + 1)
431+ // We want: 2**s (=2**ib), ideally without another precomputed.power_of_2 lookup
432+ // Injecting 2**s (=helper1), we can check that 2**t == 2**(t-s) * 2**s:
433+ #[SHL_TWO_POW_SHIFT]
434+ sel_op_shl * sel_shift_ops_no_overflow * (1 - sel_tag_err) * (max_value + 1 - two_pow_shift_lo_bits * helper1) = 0;
435+
436+ #[ALU_SHL]
437+ sel_op_shl * (1 - sel_tag_err) * (ic - sel_shift_ops_no_overflow * a_lo * helper1 ) = 0;
438+
439+ // SHR
440+
441+ // === Steps when performing SHR
442+ // (1) Prove the correct decomposition: a_hi * 2**s + a_lo = a ---> see #[A_DECOMPOSITION]
443+ // (2) Range check a_hi < 2**(t-s) && a_lo < 2**s ---> see #[RANGE_CHECK_DECOMPOSITION_A_LO/HI]
444+ // (3) Return a_hi ---> see #[ALU_SHR]
445+ //
446+ // <--(t-s) bits --> | <-- s bits -->
447+ // -------------------|-------------------
448+ // | a_hi | a_lo | --> a
449+ // ---------------------------------------
450+
451+ #[ALU_SHR]
452+ sel_op_shr * (1 - sel_tag_err) * (ic - sel_shift_ops_no_overflow * a_hi) = 0;
453+
454+ // SHL & SHR - Shared relations:
455+
456+ pol commit sel_shift_ops;
457+ // sel_op_shl || sel_op_shr:
458+ sel_shift_ops = sel_op_shl + sel_op_shr;
459+
460+ pol commit sel_shift_ops_no_overflow;
461+ // sel_shift_ops_no_overflow = 1 ==> sel_shift_ops = 1:
462+ sel_shift_ops_no_overflow * (1 - sel_shift_ops) = 0;
463+ // (sel_op_shl || sel_op_shr) & b < max_bits: see below* for constraining.
464+ pol SHIFT_OVERFLOW = sel_shift_ops * (1 - sel_shift_ops_no_overflow);
465+
466+ // The bit size of the lo limb used by the shift:
467+ pol commit shift_lo_bits;
468+ pol commit two_pow_shift_lo_bits;
469+
470+ // *For SHL and SHR, when the shift (b) > max_bits we want SHIFT_OVERFLOW == 1 and c == 0:
471+ // SHL: a_lo_bits = max_bits - b -> will underflow
472+ // SHR: a_hi_bits = max_bits - b -> will underflow
473+ // so instead set a_lo = b - max_bits and shift_lo_bits = max_bits for both SHL and SHR (see DECOMPOSED_A) and reuse the range check
474+ // RANGE_CHECK_DECOMPOSITION_A_LO to prove that b > max_bits <==> SHIFT_OVERFLOW = 1 <==> c = 0.
475+ // Note: sel_decompose_a is gated by IS_NOT_FF, so no gating for the FF tag error case is required below.
476+
477+ #[SHIFTS_LO_BITS]
478+ shift_lo_bits
479+ - sel_shift_ops_no_overflow * (sel_op_shl * (max_bits - ib) + sel_op_shr * ib)
480+ - SHIFT_OVERFLOW * max_bits
481+ = 0;
482+
483+ // Set shift_hi_bits = max_bits in the overflow case, so RANGE_CHECK_DECOMPOSITION_A_HI passes. Since we set c == 0 in this case,
484+ // we don't need to constrain that a_hi is within a certain limb size.
485+ pol SHIFT_HI_BITS = max_bits - sel_shift_ops_no_overflow * shift_lo_bits;
486+
487+ #[SHIFTS_TWO_POW]
488+ sel_shift_ops_no_overflow { shift_lo_bits, two_pow_shift_lo_bits } in precomputed.sel_range_8 { precomputed.clk, precomputed.power_of_2 };
489+
395490// TRUNCATE (ALU part for opcodes CAST and SET)
396491// Input of truncation value is sent to ia, destination tag in ia_tag and output is computed as ic.
397492// We have one dispatching lookup from execution specific to CAST and another one for SET, as
0 commit comments