openvm_circuit_primitives/bigint/
check_carry_to_zero.rs

Help
1use openvm_stark_backend::{
2    interaction::{BusIndex, InteractionBuilder},
3    p3_field::{Field, FieldAlgebra},
4};
5
6use super::{utils::range_check, OverflowInt};
7use crate::SubAir;
8
9pub struct CheckCarryToZeroCols<T> {
10    /// Carries for converting overflow limbs to canonical representation,
11    pub carries: Vec<T>,
12}
13
14#[derive(Clone, Debug)]
15pub struct CheckCarryToZeroSubAir {
16    // The number of bits for each limb (not overflowed). Example: 10.
17    pub limb_bits: usize,
18
19    pub range_checker_bus: BusIndex,
20    // The range checker decomp bits.
21    pub decomp: usize,
22}
23
24// max_overflow_bits: number of bits needed to represent the limbs of an expr / OverflowInt.
25// limb_bits: number of bits for each limb for a canonical representation, typically 8.
26pub fn get_carry_max_abs_and_bits(max_overflow_bits: usize, limb_bits: usize) -> (usize, usize) {
27    let carry_bits = max_overflow_bits - limb_bits;
28    let carry_min_value_abs = 1 << carry_bits;
29    let carry_abs_bits = carry_bits + 1;
30    (carry_min_value_abs, carry_abs_bits)
31}
32
33impl CheckCarryToZeroSubAir {
34    pub fn new(limb_bits: usize, range_checker_bus: BusIndex, decomp: usize) -> Self {
35        Self {
36            limb_bits,
37            range_checker_bus,
38            decomp,
39        }
40    }
41}
42
43impl<AB: InteractionBuilder> SubAir<AB> for CheckCarryToZeroSubAir {
44    /// `(expr, cols, is_valid)`
45    type AirContext<'a>
46        = (
47        OverflowInt<AB::Expr>,
48        CheckCarryToZeroCols<AB::Var>,
49        AB::Expr,
50    )
51    where
52        AB::Var: 'a,
53        AB::Expr: 'a,
54        AB: 'a;
55
56    /// Assumes that the parent chip has already asserted `is_valid` is to be boolean.
57    /// This is to avoid duplicating that constraint since this subair's eval method is
58    /// often called multiple times from the parent air.
59    fn eval<'a>(
60        &'a self,
61        builder: &'a mut AB,
62        (expr, cols, is_valid): (
63            OverflowInt<AB::Expr>,
64            CheckCarryToZeroCols<AB::Var>,
65            AB::Expr,
66        ),
67    ) where
68        AB::Var: 'a,
69        AB::Expr: 'a,
70    {
71        assert_eq!(expr.limbs.len(), cols.carries.len());
72        let (carry_min_value_abs, carry_abs_bits) =
73            get_carry_max_abs_and_bits(expr.max_overflow_bits, self.limb_bits);
74
75        // The carry is range checked to `[-2^(carry_abs_bits - 1), 2^(carry_abs_bits - 1))`.
76        // We assert that carry[i] * 2^limb_bits in the constraints below does not overflow.
77        // Worst case: carry[i] = -2^(carry_abs_bits - 1) so
78        //   |carry[i] * 2^limb_bits| <= 2^(carry_abs_bits - 1 + limb_bits)
79        // which has `carry_abs_bits + limb_bits` bits
80        // We constrain it to be < modulus_bits - 1 so that it is contained in [-p/2, p/2]
81        assert!(
82            carry_abs_bits + self.limb_bits < AB::F::bits() - 1,
83            "carry is too large"
84        );
85
86        // 1. Constrain the limbs size of carries.
87        for &carry in cols.carries.iter() {
88            range_check(
89                builder,
90                self.range_checker_bus,
91                self.decomp,
92                carry_abs_bits,
93                carry + AB::F::from_canonical_usize(carry_min_value_abs),
94                is_valid.clone(),
95            );
96        }
97
98        // 2. Constrain the carries and expr.
99        let mut previous_carry = AB::Expr::ZERO;
100        for (i, limb) in expr.limbs.iter().enumerate() {
101            builder.assert_eq(
102                limb.clone() + previous_carry.clone(),
103                cols.carries[i] * AB::F::from_canonical_usize(1 << self.limb_bits),
104            );
105            previous_carry = cols.carries[i].into();
106        }
107        // The last (highest) carry should be zero.
108        builder.assert_eq(previous_carry, AB::Expr::ZERO);
109    }
110}
openvm_circuit_primitives/bigint/check_carry_to_zero.rs

openvm_circuit_primitives/bigint/
check_carry_to_zero.rs
