openvm_circuit_primitives/bigint/
check_carry_mod_to_zero.rs

Help
1use itertools::Itertools;
2use num_bigint::BigUint;
3use openvm_stark_backend::{
4    interaction::{BusIndex, InteractionBuilder},
5    p3_field::FieldAlgebra,
6};
7
8use super::{
9    check_carry_to_zero::{CheckCarryToZeroCols, CheckCarryToZeroSubAir},
10    utils::{big_uint_to_limbs, range_check},
11    OverflowInt,
12};
13use crate::SubAir;
14
15#[derive(Clone)]
16pub struct CheckCarryModToZeroCols<T> {
17    /// Carries for converting the remainder to canonical form
18    pub carries: Vec<T>,
19
20    // We will check that expr - quotient * modulus = 0, which imples expr is 0 mod modulus.
21    // quotient can be negative, and this means there is no unique way to represent it as limbs but it's fine.
22    // Each limb will be range-checked to be in [-2^limb_bits, 2^limb_bits).
23    pub quotient: Vec<T>,
24}
25
26#[derive(Clone, Debug)]
27pub struct CheckCarryModToZeroSubAir {
28    pub modulus_limbs: Vec<usize>,
29
30    pub check_carry_to_zero: CheckCarryToZeroSubAir,
31}
32
33impl CheckCarryModToZeroSubAir {
34    pub fn new(
35        modulus: BigUint,
36        limb_bits: usize,
37        range_checker_bus: BusIndex,
38        decomp: usize,
39    ) -> Self {
40        let check_carry_to_zero = CheckCarryToZeroSubAir::new(limb_bits, range_checker_bus, decomp);
41        let modulus_limbs = big_uint_to_limbs(&modulus, limb_bits);
42        Self {
43            modulus_limbs,
44            check_carry_to_zero,
45        }
46    }
47}
48
49impl<AB: InteractionBuilder> SubAir<AB> for CheckCarryModToZeroSubAir {
50    /// `(expr, cols, is_valid)`
51    type AirContext<'a>
52        = (
53        OverflowInt<AB::Expr>,
54        CheckCarryModToZeroCols<AB::Var>,
55        AB::Expr,
56    )
57    where
58        AB::Var: 'a,
59        AB::Expr: 'a,
60        AB: 'a;
61
62    /// Assumes that the parent chip has already asserted `is_valid` is to be boolean.
63    /// This is to avoid duplicating that constraint since this subair's eval method is
64    /// often called multiple times from the parent air.
65    fn eval<'a>(
66        &'a self,
67        builder: &'a mut AB,
68        (expr, cols, is_valid): (
69            OverflowInt<AB::Expr>,
70            CheckCarryModToZeroCols<AB::Var>,
71            AB::Expr,
72        ),
73    ) where
74        AB::Var: 'a,
75        AB::Expr: 'a,
76    {
77        let CheckCarryModToZeroCols { quotient, carries } = cols;
78        let q_offset = AB::F::from_canonical_usize(1 << self.check_carry_to_zero.limb_bits);
79        for &q in quotient.iter() {
80            range_check(
81                builder,
82                self.check_carry_to_zero.range_checker_bus,
83                self.check_carry_to_zero.decomp,
84                self.check_carry_to_zero.limb_bits + 1,
85                q + q_offset,
86                is_valid.clone(),
87            );
88        }
89        let limb_bits = self.check_carry_to_zero.limb_bits;
90        let q_limbs = quotient.iter().map(|&x| x.into()).collect();
91        let overflow_q = OverflowInt::<AB::Expr>::from_canonical_signed_limbs(q_limbs, limb_bits);
92        let p_limbs = self
93            .modulus_limbs
94            .iter()
95            .map(|&x| AB::Expr::from_canonical_usize(x))
96            .collect_vec();
97        let overflow_p =
98            OverflowInt::from_canonical_unsigned_limbs(p_limbs, self.check_carry_to_zero.limb_bits);
99
100        let expr = expr - overflow_q * overflow_p;
101        self.check_carry_to_zero
102            .eval(builder, (expr, CheckCarryToZeroCols { carries }, is_valid));
103    }
104}
openvm_circuit_primitives/bigint/check_carry_mod_to_zero.rs

openvm_circuit_primitives/bigint/
check_carry_mod_to_zero.rs
