openvm_rv32im_circuit/divrem/
core.rs

1use std::{
2    array,
3    borrow::{Borrow, BorrowMut},
4};
5
6use num_bigint::BigUint;
7use num_integer::Integer;
8use openvm_circuit::{
9    arch::*,
10    system::memory::{online::TracingMemory, MemoryAuxColsFactory},
11};
12use openvm_circuit_primitives::{
13    bitwise_op_lookup::{BitwiseOperationLookupBus, SharedBitwiseOperationLookupChip},
14    range_tuple::{RangeTupleCheckerBus, SharedRangeTupleCheckerChip},
15    utils::{not, select},
16    AlignedBytesBorrow, ColumnsAir, StructReflection, StructReflectionHelper,
17};
18use openvm_circuit_primitives_derive::AlignedBorrow;
19use openvm_instructions::{instruction::Instruction, program::DEFAULT_PC_STEP, LocalOpcode};
20use openvm_rv32im_transpiler::DivRemOpcode;
21use openvm_stark_backend::{
22    interaction::InteractionBuilder,
23    p3_air::{AirBuilder, BaseAir},
24    p3_field::{Field, PrimeCharacteristicRing, PrimeField32},
25    BaseAirWithPublicValues,
26};
27use strum::IntoEnumIterator;
28
29#[repr(C)]
30#[derive(AlignedBorrow, StructReflection)]
31pub struct DivRemCoreCols<T, const NUM_LIMBS: usize, const LIMB_BITS: usize> {
32    // b = c * q + r for some 0 <= |r| < |c| and sign(r) = sign(b) or r = 0.
33    pub b: [T; NUM_LIMBS],
34    pub c: [T; NUM_LIMBS],
35    pub q: [T; NUM_LIMBS],
36    pub r: [T; NUM_LIMBS],
37
38    // Flags to indicate special cases.
39    pub zero_divisor: T,
40    pub r_zero: T,
41
42    // Sign of b and c respectively, while q_sign = b_sign ^ c_sign if q is non-zero
43    // and is 0 otherwise. sign_xor = b_sign ^ c_sign always.
44    pub b_sign: T,
45    pub c_sign: T,
46    pub q_sign: T,
47    pub sign_xor: T,
48
49    // Auxiliary columns to constrain that zero_divisor = 1 if and only if c = 0.
50    pub c_sum_inv: T,
51    // Auxiliary columns to constrain that r_zero = 1 if and only if r = 0 and zero_divisor = 0.
52    pub r_sum_inv: T,
53
54    // Auxiliary columns to constrain that 0 <= |r| < |c|. When sign_xor == 1 we have
55    // r_prime = -r, and when sign_xor == 0 we have r_prime = r. Each r_inv[i] is the
56    // field inverse of r_prime[i] - 2^LIMB_BITS, ensures each r_prime[i] is in range.
57    pub r_prime: [T; NUM_LIMBS],
58    pub r_inv: [T; NUM_LIMBS],
59    pub lt_marker: [T; NUM_LIMBS],
60    pub lt_diff: T,
61
62    // Opcode flags
63    pub opcode_div_flag: T,
64    pub opcode_divu_flag: T,
65    pub opcode_rem_flag: T,
66    pub opcode_remu_flag: T,
67}
68
69#[derive(Copy, Clone, Debug, derive_new::new, ColumnsAir)]
70#[columns_via(DivRemCoreCols<u8, NUM_LIMBS, LIMB_BITS>)]
71pub struct DivRemCoreAir<const NUM_LIMBS: usize, const LIMB_BITS: usize> {
72    pub bitwise_lookup_bus: BitwiseOperationLookupBus,
73    pub range_tuple_bus: RangeTupleCheckerBus<2>,
74    offset: usize,
75}
76
77impl<F: Field, const NUM_LIMBS: usize, const LIMB_BITS: usize> BaseAir<F>
78    for DivRemCoreAir<NUM_LIMBS, LIMB_BITS>
79{
80    fn width(&self) -> usize {
81        DivRemCoreCols::<F, NUM_LIMBS, LIMB_BITS>::width()
82    }
83}
84impl<F: Field, const NUM_LIMBS: usize, const LIMB_BITS: usize> BaseAirWithPublicValues<F>
85    for DivRemCoreAir<NUM_LIMBS, LIMB_BITS>
86{
87}
88
89impl<AB, I, const NUM_LIMBS: usize, const LIMB_BITS: usize> VmCoreAir<AB, I>
90    for DivRemCoreAir<NUM_LIMBS, LIMB_BITS>
91where
92    AB: InteractionBuilder,
93    I: VmAdapterInterface<AB::Expr>,
94    I::Reads: From<[[AB::Expr; NUM_LIMBS]; 2]>,
95    I::Writes: From<[[AB::Expr; NUM_LIMBS]; 1]>,
96    I::ProcessedInstruction: From<MinimalInstruction<AB::Expr>>,
97{
98    fn eval(
99        &self,
100        builder: &mut AB,
101        local_core: &[AB::Var],
102        _from_pc: AB::Var,
103    ) -> AdapterAirContext<AB::Expr, I> {
104        let cols: &DivRemCoreCols<_, NUM_LIMBS, LIMB_BITS> = local_core.borrow();
105        let flags = [
106            cols.opcode_div_flag,
107            cols.opcode_divu_flag,
108            cols.opcode_rem_flag,
109            cols.opcode_remu_flag,
110        ];
111
112        let is_valid = flags.iter().fold(AB::Expr::ZERO, |acc, &flag| {
113            builder.assert_bool(flag);
114            acc + flag.into()
115        });
116        builder.assert_bool(is_valid.clone());
117
118        let b = &cols.b;
119        let c = &cols.c;
120        let q = &cols.q;
121        let r = &cols.r;
122
123        // Constrain that b = (c * q + r) % 2^{NUM_LIMBS * LIMB_BITS} and range checkeach element in
124        // q.
125        let b_ext = cols.b_sign * AB::F::from_u32((1 << LIMB_BITS) - 1);
126        let c_ext = cols.c_sign * AB::F::from_u32((1 << LIMB_BITS) - 1);
127        let carry_divide = AB::F::from_u32(1 << LIMB_BITS).inverse();
128        let mut carry: [AB::Expr; NUM_LIMBS] = array::from_fn(|_| AB::Expr::ZERO);
129
130        for i in 0..NUM_LIMBS {
131            let expected_limb = if i == 0 {
132                AB::Expr::ZERO
133            } else {
134                carry[i - 1].clone()
135            } + (0..=i).fold(r[i].into(), |ac, k| ac + (c[k] * q[i - k]));
136            carry[i] = (expected_limb - b[i]) * carry_divide;
137        }
138
139        for (q, carry) in q.iter().zip(carry.iter()) {
140            self.range_tuple_bus
141                .send(vec![(*q).into(), carry.clone()])
142                .eval(builder, is_valid.clone());
143        }
144
145        // Constrain that the upper limbs of b = c * q + r are all equal to b_ext and
146        // range check each element in r.
147        let q_ext = cols.q_sign * AB::F::from_u32((1 << LIMB_BITS) - 1);
148        let mut carry_ext: [AB::Expr; NUM_LIMBS] = array::from_fn(|_| AB::Expr::ZERO);
149
150        for j in 0..NUM_LIMBS {
151            let expected_limb = if j == 0 {
152                carry[NUM_LIMBS - 1].clone()
153            } else {
154                carry_ext[j - 1].clone()
155            } + ((j + 1)..NUM_LIMBS)
156                .fold(AB::Expr::ZERO, |acc, k| acc + (c[k] * q[NUM_LIMBS + j - k]))
157                + (0..(j + 1)).fold(AB::Expr::ZERO, |acc, k| {
158                    acc + (c[k] * q_ext.clone()) + (q[k] * c_ext.clone())
159                })
160                + (AB::Expr::ONE - cols.r_zero) * b_ext.clone();
161            // Technically there are ways to constrain that c * q is in range without
162            // using a range checker, but because we already have to range check each
163            // limb of r it requires no additional columns to also range check each
164            // carry_ext.
165            //
166            // Note that the sign of r is not equal to the sign of b only when r = 0.
167            // Flag column r_zero tracks this special case.
168            carry_ext[j] = (expected_limb - b_ext.clone()) * carry_divide;
169        }
170
171        for (r, carry) in r.iter().zip(carry_ext.iter()) {
172            self.range_tuple_bus
173                .send(vec![(*r).into(), carry.clone()])
174                .eval(builder, is_valid.clone());
175        }
176
177        // Handle special cases. We can have either at most one of a zero divisor,
178        // or a 0 remainder. Signed overflow falls under the latter.
179        let special_case = cols.zero_divisor + cols.r_zero;
180        builder.assert_bool(special_case.clone());
181
182        // Constrain that zero_divisor = 1 if and only if c = 0.
183        builder.assert_bool(cols.zero_divisor);
184        let mut when_zero_divisor = builder.when(cols.zero_divisor);
185        for i in 0..NUM_LIMBS {
186            when_zero_divisor.assert_zero(c[i]);
187            when_zero_divisor.assert_eq(q[i], AB::F::from_u32((1 << LIMB_BITS) - 1));
188        }
189        // c_sum is guaranteed to be non-zero if c is non-zero since we assume
190        // each limb of c to be within [0, 2^LIMB_BITS) already.
191        // To constrain that if c = 0 then zero_divisor = 1, we check that if zero_divisor = 0
192        // and is_valid = 1 then c_sum is non-zero using c_sum_inv.
193        let c_sum = c.iter().fold(AB::Expr::ZERO, |acc, c| acc + *c);
194        let valid_and_not_zero_divisor = is_valid.clone() - cols.zero_divisor;
195        builder.assert_bool(valid_and_not_zero_divisor.clone());
196        builder
197            .when(valid_and_not_zero_divisor)
198            .assert_one(c_sum * cols.c_sum_inv);
199
200        // Constrain that r_zero = 1 if and only if r = 0 and zero_divisor = 0.
201        builder.assert_bool(cols.r_zero);
202        r.iter()
203            .for_each(|r_i| builder.when(cols.r_zero).assert_zero(*r_i));
204        // To constrain that if r = 0 and zero_divisor = 0 then r_zero = 1, we check that
205        // if special_case = 0 and is_valid = 1 then r_sum is non-zero (using r_sum_inv).
206        let r_sum = r.iter().fold(AB::Expr::ZERO, |acc, r| acc + *r);
207        let valid_and_not_special_case = is_valid.clone() - special_case.clone();
208        builder.assert_bool(valid_and_not_special_case.clone());
209        builder
210            .when(valid_and_not_special_case)
211            .assert_one(r_sum * cols.r_sum_inv);
212
213        // Constrain the correctness of b_sign and c_sign. Note that we do not need to
214        // check that the sign of r is b_sign since we cannot have r_prime < c (or c < r_prime
215        // if c is negative) if this is not the case.
216        let signed = cols.opcode_div_flag + cols.opcode_rem_flag;
217
218        builder.assert_bool(cols.b_sign);
219        builder.assert_bool(cols.c_sign);
220        builder
221            .when(not::<AB::Expr>(signed.clone()))
222            .assert_zero(cols.b_sign);
223        builder
224            .when(not::<AB::Expr>(signed.clone()))
225            .assert_zero(cols.c_sign);
226        builder.assert_eq(
227            cols.b_sign + cols.c_sign - AB::Expr::from_u32(2) * cols.b_sign * cols.c_sign,
228            cols.sign_xor,
229        );
230
231        // To constrain the correctness of q_sign we make sure if q is non-zero then
232        // q_sign = b_sign ^ c_sign, and if q is zero then q_sign = 0.
233        // Note:
234        // - q_sum is guaranteed to be non-zero if q is non-zero since we've range checked each
235        // limb of q to be within [0, 2^LIMB_BITS) already.
236        // - If q is zero and q_ext satisfies the constraint
237        // sign_extend(b) = sign_extend(c) * sign_extend(q) + sign_extend(r), then q_sign must be 0.
238        // Thus, we do not need additional constraints in case q is zero.
239        let nonzero_q = q.iter().fold(AB::Expr::ZERO, |acc, q| acc + *q);
240        builder.assert_bool(cols.q_sign);
241        builder
242            .when(nonzero_q)
243            .when(not(cols.zero_divisor))
244            .assert_eq(cols.q_sign, cols.sign_xor);
245        builder
246            .when_ne(cols.q_sign, cols.sign_xor)
247            .when(not(cols.zero_divisor))
248            .assert_zero(cols.q_sign);
249
250        // Check that the signs of b and c are correct.
251        let sign_mask = AB::F::from_u32(1 << (LIMB_BITS - 1));
252        self.bitwise_lookup_bus
253            .send_range(
254                AB::Expr::from_u32(2) * (b[NUM_LIMBS - 1] - cols.b_sign * sign_mask),
255                AB::Expr::from_u32(2) * (c[NUM_LIMBS - 1] - cols.c_sign * sign_mask),
256            )
257            .eval(builder, signed.clone());
258
259        // Constrain that 0 <= |r| < |c| by checking that r_prime < c (unsigned LT). By
260        // definition, the sign of r must be b_sign. If c is negative then we want
261        // to constrain c < r_prime. If c is positive, then we want to constrain r_prime < c.
262        //
263        // Because we already constrain that r and q are correct for special cases,
264        // we skip the range check when special_case = 1.
265        let r_p = &cols.r_prime;
266        let mut carry_lt: [AB::Expr; NUM_LIMBS] = array::from_fn(|_| AB::Expr::ZERO);
267
268        for i in 0..NUM_LIMBS {
269            // When the signs of r (i.e. b) and c are the same, r_prime = r.
270            builder.when(not(cols.sign_xor)).assert_eq(r[i], r_p[i]);
271
272            // When the signs of r and c are different, r_prime = -r. To constrain this, we
273            // first ensure each r[i] + r_prime[i] + carry[i - 1] is in {0, 2^LIMB_BITS}, and
274            // that when the sum is 0 then r_prime[i] = 0 as well. Passing both constraints
275            // implies that 0 <= r_prime[i] <= 2^LIMB_BITS, and in order to ensure r_prime[i] !=
276            // 2^LIMB_BITS we check that r_prime[i] - 2^LIMB_BITS has an inverse in F.
277            let last_carry = if i > 0 {
278                carry_lt[i - 1].clone()
279            } else {
280                AB::Expr::ZERO
281            };
282            carry_lt[i] = (last_carry.clone() + r[i] + r_p[i]) * carry_divide;
283            builder.when(cols.sign_xor).assert_zero(
284                (carry_lt[i].clone() - last_carry) * (carry_lt[i].clone() - AB::Expr::ONE),
285            );
286            builder
287                .when(cols.sign_xor)
288                .assert_one((r_p[i] - AB::F::from_u32(1 << LIMB_BITS)) * cols.r_inv[i]);
289            builder
290                .when(cols.sign_xor)
291                .when(not::<AB::Expr>(carry_lt[i].clone()))
292                .assert_zero(r_p[i]);
293        }
294
295        let marker = &cols.lt_marker;
296        let mut prefix_sum = special_case.clone();
297
298        for i in (0..NUM_LIMBS).rev() {
299            let diff = r_p[i] * (AB::Expr::from_u8(2) * cols.c_sign - AB::Expr::ONE)
300                + c[i] * (AB::Expr::ONE - AB::Expr::from_u8(2) * cols.c_sign);
301            prefix_sum += marker[i].into();
302            builder.assert_bool(marker[i]);
303            builder.assert_zero(not::<AB::Expr>(prefix_sum.clone()) * diff.clone());
304            builder.when(marker[i]).assert_eq(cols.lt_diff, diff);
305        }
306        // - If r_prime != c, then prefix_sum = 1 so marker[i] must be 1 iff i is the first index
307        //   where diff != 0. Constrains that diff == lt_diff where lt_diff is non-zero.
308        // - If r_prime == c, then prefix_sum = 0. Here, prefix_sum cannot be 1 because all diff are
309        //   zero, making diff == lt_diff fails.
310
311        builder.when(is_valid.clone()).assert_one(prefix_sum);
312        // Range check to ensure lt_diff is non-zero.
313        self.bitwise_lookup_bus
314            .send_range(cols.lt_diff - AB::Expr::ONE, AB::F::ZERO)
315            .eval(builder, is_valid.clone() - special_case);
316
317        // Generate expected opcode and output a to pass to the adapter.
318        let expected_opcode = flags.iter().zip(DivRemOpcode::iter()).fold(
319            AB::Expr::ZERO,
320            |acc, (flag, local_opcode)| {
321                acc + (*flag).into() * AB::Expr::from_u8(local_opcode as u8)
322            },
323        ) + AB::Expr::from_usize(self.offset);
324
325        let is_div = cols.opcode_div_flag + cols.opcode_divu_flag;
326        let a = array::from_fn(|i| select(is_div.clone(), q[i], r[i]));
327
328        AdapterAirContext {
329            to_pc: None,
330            reads: [cols.b.map(Into::into), cols.c.map(Into::into)].into(),
331            writes: [a.map(Into::into)].into(),
332            instruction: MinimalInstruction {
333                is_valid,
334                opcode: expected_opcode,
335            }
336            .into(),
337        }
338    }
339
340    fn start_offset(&self) -> usize {
341        self.offset
342    }
343}
344
345#[derive(Debug, Eq, PartialEq)]
346#[repr(u8)]
347pub(super) enum DivRemCoreSpecialCase {
348    None,
349    ZeroDivisor,
350    SignedOverflow,
351}
352
353#[repr(C)]
354#[derive(AlignedBytesBorrow, Debug)]
355pub struct DivRemCoreRecord<const NUM_LIMBS: usize> {
356    pub b: [u8; NUM_LIMBS],
357    pub c: [u8; NUM_LIMBS],
358    pub local_opcode: u8,
359}
360
361#[derive(Clone, Copy, derive_new::new)]
362pub struct DivRemExecutor<A, const NUM_LIMBS: usize, const LIMB_BITS: usize> {
363    adapter: A,
364    pub offset: usize,
365}
366
367pub struct DivRemFiller<A, const NUM_LIMBS: usize, const LIMB_BITS: usize> {
368    adapter: A,
369    pub offset: usize,
370    pub bitwise_lookup_chip: SharedBitwiseOperationLookupChip<LIMB_BITS>,
371    pub range_tuple_chip: SharedRangeTupleCheckerChip<2>,
372}
373
374impl<A, const NUM_LIMBS: usize, const LIMB_BITS: usize> DivRemFiller<A, NUM_LIMBS, LIMB_BITS> {
375    pub fn new(
376        adapter: A,
377        bitwise_lookup_chip: SharedBitwiseOperationLookupChip<LIMB_BITS>,
378        range_tuple_chip: SharedRangeTupleCheckerChip<2>,
379        offset: usize,
380    ) -> Self {
381        // The RangeTupleChecker is used to range check (a[i], carry[i]) pairs where 0 <= i
382        // < 2 * NUM_LIMBS. a[i] must have LIMB_BITS bits and carry[i] is the sum of i + 1
383        // bytes (with LIMB_BITS bits). BitwiseOperationLookup is used to sign check bytes.
384        debug_assert!(
385            range_tuple_chip.sizes()[0] == 1 << LIMB_BITS,
386            "First element of RangeTupleChecker must have size {}",
387            1 << LIMB_BITS
388        );
389        debug_assert!(
390            range_tuple_chip.sizes()[1] >= (1 << LIMB_BITS) * 2 * NUM_LIMBS as u32,
391            "Second element of RangeTupleChecker must have size of at least {}",
392            (1 << LIMB_BITS) * 2 * NUM_LIMBS as u32
393        );
394
395        Self {
396            adapter,
397            offset,
398            bitwise_lookup_chip,
399            range_tuple_chip,
400        }
401    }
402}
403
404impl<F, A, RA, const NUM_LIMBS: usize, const LIMB_BITS: usize> PreflightExecutor<F, RA>
405    for DivRemExecutor<A, NUM_LIMBS, LIMB_BITS>
406where
407    F: PrimeField32,
408    A: 'static
409        + AdapterTraceExecutor<
410            F,
411            ReadData: Into<[[u8; NUM_LIMBS]; 2]>,
412            WriteData: From<[[u8; NUM_LIMBS]; 1]>,
413        >,
414    for<'buf> RA: RecordArena<
415        'buf,
416        EmptyAdapterCoreLayout<F, A>,
417        (A::RecordMut<'buf>, &'buf mut DivRemCoreRecord<NUM_LIMBS>),
418    >,
419{
420    fn get_opcode_name(&self, opcode: usize) -> String {
421        format!("{:?}", DivRemOpcode::from_usize(opcode - self.offset))
422    }
423
424    fn execute(
425        &self,
426        state: VmStateMut<F, TracingMemory, RA>,
427        instruction: &Instruction<F>,
428    ) -> Result<(), ExecutionError> {
429        let Instruction { opcode, .. } = instruction;
430
431        let (mut adapter_record, core_record) = state.ctx.alloc(EmptyAdapterCoreLayout::new());
432
433        A::start(*state.pc, state.memory, &mut adapter_record);
434
435        core_record.local_opcode = opcode.local_opcode_idx(self.offset) as u8;
436
437        let is_signed = core_record.local_opcode == DivRemOpcode::DIV as u8
438            || core_record.local_opcode == DivRemOpcode::REM as u8;
439        let is_div = core_record.local_opcode == DivRemOpcode::DIV as u8
440            || core_record.local_opcode == DivRemOpcode::DIVU as u8;
441
442        [core_record.b, core_record.c] = self
443            .adapter
444            .read(state.memory, instruction, &mut adapter_record)
445            .into();
446
447        let b = core_record.b.map(u32::from);
448        let c = core_record.c.map(u32::from);
449        let (q, r, _, _, _, _) = run_divrem::<NUM_LIMBS, LIMB_BITS>(is_signed, &b, &c);
450
451        let rd = if is_div {
452            q.map(|x| x as u8)
453        } else {
454            r.map(|x| x as u8)
455        };
456
457        self.adapter
458            .write(state.memory, instruction, [rd].into(), &mut adapter_record);
459
460        *state.pc = state.pc.wrapping_add(DEFAULT_PC_STEP);
461
462        Ok(())
463    }
464}
465
466impl<F, A, const NUM_LIMBS: usize, const LIMB_BITS: usize> TraceFiller<F>
467    for DivRemFiller<A, NUM_LIMBS, LIMB_BITS>
468where
469    F: PrimeField32,
470    A: 'static + AdapterTraceFiller<F>,
471{
472    fn fill_trace_row(&self, mem_helper: &MemoryAuxColsFactory<F>, row_slice: &mut [F]) {
473        // SAFETY: row_slice is guaranteed by the caller to have at least A::WIDTH +
474        // DivRemCoreCols::width() elements
475        let (adapter_row, mut core_row) = unsafe { row_slice.split_at_mut_unchecked(A::WIDTH) };
476        self.adapter.fill_trace_row(mem_helper, adapter_row);
477        // SAFETY: core_row contains a valid DivRemCoreRecord written by the executor
478        // during trace generation
479        let record: &DivRemCoreRecord<NUM_LIMBS> =
480            unsafe { get_record_from_slice(&mut core_row, ()) };
481        let core_row: &mut DivRemCoreCols<F, NUM_LIMBS, LIMB_BITS> = core_row.borrow_mut();
482
483        let opcode = DivRemOpcode::from_usize(record.local_opcode as usize);
484        let is_signed = opcode == DivRemOpcode::DIV || opcode == DivRemOpcode::REM;
485
486        let (q, r, b_sign, c_sign, q_sign, case) = run_divrem::<NUM_LIMBS, LIMB_BITS>(
487            is_signed,
488            &record.b.map(u32::from),
489            &record.c.map(u32::from),
490        );
491
492        let carries = run_mul_carries::<NUM_LIMBS, LIMB_BITS>(
493            is_signed,
494            &record.c.map(u32::from),
495            &q,
496            &r,
497            q_sign,
498        );
499        for i in 0..NUM_LIMBS {
500            self.range_tuple_chip.add_count(&[q[i], carries[i]]);
501            self.range_tuple_chip
502                .add_count(&[r[i], carries[i + NUM_LIMBS]]);
503        }
504
505        let sign_xor = b_sign ^ c_sign;
506        let r_prime = if sign_xor {
507            negate::<NUM_LIMBS, LIMB_BITS>(&r)
508        } else {
509            r
510        };
511        let r_zero = r.iter().all(|&v| v == 0) && case != DivRemCoreSpecialCase::ZeroDivisor;
512
513        if is_signed {
514            let b_sign_mask = if b_sign { 1 << (LIMB_BITS - 1) } else { 0 };
515            let c_sign_mask = if c_sign { 1 << (LIMB_BITS - 1) } else { 0 };
516            self.bitwise_lookup_chip.request_range(
517                (record.b[NUM_LIMBS - 1] as u32 - b_sign_mask) << 1,
518                (record.c[NUM_LIMBS - 1] as u32 - c_sign_mask) << 1,
519            );
520        }
521
522        // Write in a reverse order
523        core_row.opcode_remu_flag = F::from_bool(opcode == DivRemOpcode::REMU);
524        core_row.opcode_rem_flag = F::from_bool(opcode == DivRemOpcode::REM);
525        core_row.opcode_divu_flag = F::from_bool(opcode == DivRemOpcode::DIVU);
526        core_row.opcode_div_flag = F::from_bool(opcode == DivRemOpcode::DIV);
527
528        core_row.lt_diff = F::ZERO;
529        core_row.lt_marker = [F::ZERO; NUM_LIMBS];
530        if case == DivRemCoreSpecialCase::None && !r_zero {
531            let idx = run_sltu_diff_idx(&record.c.map(u32::from), &r_prime, c_sign);
532            let val = if c_sign {
533                r_prime[idx] - record.c[idx] as u32
534            } else {
535                record.c[idx] as u32 - r_prime[idx]
536            };
537            self.bitwise_lookup_chip.request_range(val - 1, 0);
538            core_row.lt_diff = F::from_u32(val);
539            core_row.lt_marker[idx] = F::ONE;
540        }
541
542        let r_prime_f = r_prime.map(F::from_u32);
543        core_row.r_inv = r_prime_f.map(|r| (r - F::from_u32(256)).inverse());
544        core_row.r_prime = r_prime_f;
545
546        let r_sum_f = r.iter().fold(F::ZERO, |acc, r| acc + F::from_u32(*r));
547        core_row.r_sum_inv = r_sum_f.try_inverse().unwrap_or(F::ZERO);
548
549        let c_sum_f = F::from_u32(record.c.iter().fold(0, |acc, c| acc + *c as u32));
550        core_row.c_sum_inv = c_sum_f.try_inverse().unwrap_or(F::ZERO);
551
552        core_row.sign_xor = F::from_bool(sign_xor);
553        core_row.q_sign = F::from_bool(q_sign);
554        core_row.c_sign = F::from_bool(c_sign);
555        core_row.b_sign = F::from_bool(b_sign);
556
557        core_row.r_zero = F::from_bool(r_zero);
558        core_row.zero_divisor = F::from_bool(case == DivRemCoreSpecialCase::ZeroDivisor);
559
560        core_row.r = r.map(F::from_u32);
561        core_row.q = q.map(F::from_u32);
562        core_row.c = record.c.map(F::from_u8);
563        core_row.b = record.b.map(F::from_u8);
564    }
565}
566
567// Returns (quotient, remainder, x_sign, y_sign, q_sign, case) where case = 0 for normal, 1
568// for zero divisor, and 2 for signed overflow
569#[inline(always)]
570pub(super) fn run_divrem<const NUM_LIMBS: usize, const LIMB_BITS: usize>(
571    signed: bool,
572    x: &[u32; NUM_LIMBS],
573    y: &[u32; NUM_LIMBS],
574) -> (
575    [u32; NUM_LIMBS],
576    [u32; NUM_LIMBS],
577    bool,
578    bool,
579    bool,
580    DivRemCoreSpecialCase,
581) {
582    let x_sign = signed && (x[NUM_LIMBS - 1] >> (LIMB_BITS - 1) == 1);
583    let y_sign = signed && (y[NUM_LIMBS - 1] >> (LIMB_BITS - 1) == 1);
584    let max_limb = (1 << LIMB_BITS) - 1;
585
586    let zero_divisor = y.iter().all(|val| *val == 0);
587    let overflow = x[NUM_LIMBS - 1] == 1 << (LIMB_BITS - 1)
588        && x[..(NUM_LIMBS - 1)].iter().all(|val| *val == 0)
589        && y.iter().all(|val| *val == max_limb)
590        && x_sign
591        && y_sign;
592
593    if zero_divisor {
594        return (
595            [max_limb; NUM_LIMBS],
596            *x,
597            x_sign,
598            y_sign,
599            signed,
600            DivRemCoreSpecialCase::ZeroDivisor,
601        );
602    } else if overflow {
603        return (
604            *x,
605            [0; NUM_LIMBS],
606            x_sign,
607            y_sign,
608            false,
609            DivRemCoreSpecialCase::SignedOverflow,
610        );
611    }
612
613    let x_abs = if x_sign {
614        negate::<NUM_LIMBS, LIMB_BITS>(x)
615    } else {
616        *x
617    };
618    let y_abs = if y_sign {
619        negate::<NUM_LIMBS, LIMB_BITS>(y)
620    } else {
621        *y
622    };
623
624    let x_big = limbs_to_biguint::<NUM_LIMBS, LIMB_BITS>(&x_abs);
625    let y_big = limbs_to_biguint::<NUM_LIMBS, LIMB_BITS>(&y_abs);
626    let q_big = x_big.clone() / y_big.clone();
627    let r_big = x_big.clone() % y_big.clone();
628
629    let q = if x_sign ^ y_sign {
630        negate::<NUM_LIMBS, LIMB_BITS>(&biguint_to_limbs::<NUM_LIMBS, LIMB_BITS>(&q_big))
631    } else {
632        biguint_to_limbs::<NUM_LIMBS, LIMB_BITS>(&q_big)
633    };
634    let q_sign = signed && (q[NUM_LIMBS - 1] >> (LIMB_BITS - 1) == 1);
635
636    // In C |q * y| <= |x|, which means if x is negative then r <= 0 and vice versa.
637    let r = if x_sign {
638        negate::<NUM_LIMBS, LIMB_BITS>(&biguint_to_limbs::<NUM_LIMBS, LIMB_BITS>(&r_big))
639    } else {
640        biguint_to_limbs::<NUM_LIMBS, LIMB_BITS>(&r_big)
641    };
642
643    (q, r, x_sign, y_sign, q_sign, DivRemCoreSpecialCase::None)
644}
645
646#[inline(always)]
647pub(super) fn run_sltu_diff_idx<const NUM_LIMBS: usize>(
648    x: &[u32; NUM_LIMBS],
649    y: &[u32; NUM_LIMBS],
650    cmp: bool,
651) -> usize {
652    for i in (0..NUM_LIMBS).rev() {
653        if x[i] != y[i] {
654            assert!((x[i] < y[i]) == cmp);
655            return i;
656        }
657    }
658    assert!(!cmp);
659    NUM_LIMBS
660}
661
662// returns carries of d * q + r
663#[inline(always)]
664pub(super) fn run_mul_carries<const NUM_LIMBS: usize, const LIMB_BITS: usize>(
665    signed: bool,
666    d: &[u32; NUM_LIMBS],
667    q: &[u32; NUM_LIMBS],
668    r: &[u32; NUM_LIMBS],
669    q_sign: bool,
670) -> Vec<u32> {
671    let mut carry = vec![0u32; 2 * NUM_LIMBS];
672    for i in 0..NUM_LIMBS {
673        let mut val = r[i] + if i > 0 { carry[i - 1] } else { 0 };
674        for j in 0..=i {
675            val += d[j] * q[i - j];
676        }
677        carry[i] = val >> LIMB_BITS;
678    }
679
680    let q_ext = if q_sign && signed {
681        (1 << LIMB_BITS) - 1
682    } else {
683        0
684    };
685    let d_ext =
686        (d[NUM_LIMBS - 1] >> (LIMB_BITS - 1)) * if signed { (1 << LIMB_BITS) - 1 } else { 0 };
687    let r_ext =
688        (r[NUM_LIMBS - 1] >> (LIMB_BITS - 1)) * if signed { (1 << LIMB_BITS) - 1 } else { 0 };
689    let mut d_prefix = 0;
690    let mut q_prefix = 0;
691
692    for i in 0..NUM_LIMBS {
693        d_prefix += d[i];
694        q_prefix += q[i];
695        let mut val = carry[NUM_LIMBS + i - 1] + d_prefix * q_ext + q_prefix * d_ext + r_ext;
696        for j in (i + 1)..NUM_LIMBS {
697            val += d[j] * q[NUM_LIMBS + i - j];
698        }
699        carry[NUM_LIMBS + i] = val >> LIMB_BITS;
700    }
701    carry
702}
703
704#[inline(always)]
705fn limbs_to_biguint<const NUM_LIMBS: usize, const LIMB_BITS: usize>(
706    x: &[u32; NUM_LIMBS],
707) -> BigUint {
708    let base = BigUint::new(vec![1 << LIMB_BITS]);
709    let mut res = BigUint::new(vec![0]);
710    for val in x.iter().rev() {
711        res *= base.clone();
712        res += BigUint::new(vec![*val]);
713    }
714    res
715}
716
717#[inline(always)]
718fn biguint_to_limbs<const NUM_LIMBS: usize, const LIMB_BITS: usize>(
719    x: &BigUint,
720) -> [u32; NUM_LIMBS] {
721    let mut res = [0; NUM_LIMBS];
722    let mut x = x.clone();
723    let base = BigUint::from(1u32 << LIMB_BITS);
724    for limb in res.iter_mut() {
725        let (quot, rem) = x.div_rem(&base);
726        *limb = rem.iter_u32_digits().next().unwrap_or(0);
727        x = quot;
728    }
729    debug_assert_eq!(x, BigUint::from(0u32));
730    res
731}
732
733#[inline(always)]
734fn negate<const NUM_LIMBS: usize, const LIMB_BITS: usize>(
735    x: &[u32; NUM_LIMBS],
736) -> [u32; NUM_LIMBS] {
737    let mut carry = 1;
738    array::from_fn(|i| {
739        let val = (1 << LIMB_BITS) + carry - 1 - x[i];
740        carry = val >> LIMB_BITS;
741        val % (1 << LIMB_BITS)
742    })
743}
openvm_rv32im_circuit/divrem/core.rs

openvm_rv32im_circuit/divrem/
core.rs
