kimchi_msm/ffa/
interpreter.rs

1use crate::{
2    circuit_design::{ColAccessCap, ColWriteCap, LookupCap},
3    ffa::{columns::FFAColumn, lookups::LookupTable},
4    serialization::interpreter::{limb_decompose_biguint, limb_decompose_ff},
5    LIMB_BITSIZE, N_LIMBS,
6};
7use ark_ff::PrimeField;
8use num_bigint::BigUint;
9use num_integer::Integer;
10use o1_utils::field_helpers::FieldHelpers;
11
12// For now this function does not /compute/ anything, although it could.
13/// Constraint for one row of FF addition:
14///
15/// - First:        a_0 + b_0 - q * f_0 - r_0 - c_0 * 2^{15} = 0
16/// - Intermediate: a_i + b_i - q * f_i - r_i - c_i * 2^{15} + c_{i-1} = 0
17/// - Last (n=16):  a_n + b_n - q * f_n - r_n                + c_{n-1} = 0
18///
19/// q, c_i ∈ {-1,0,1}
20/// a_i, b_i, f_i, r_i ∈ [0,2^15)
21pub fn constrain_ff_addition_row<
22    F: PrimeField,
23    Env: ColAccessCap<F, FFAColumn> + LookupCap<F, FFAColumn, LookupTable>,
24>(
25    env: &mut Env,
26    limb_num: usize,
27) {
28    let a: Env::Variable = Env::read_column(env, FFAColumn::InputA(limb_num));
29    let b: Env::Variable = Env::read_column(env, FFAColumn::InputB(limb_num));
30    let f: Env::Variable = Env::read_column(env, FFAColumn::ModulusF(limb_num));
31    let r: Env::Variable = Env::read_column(env, FFAColumn::Remainder(limb_num));
32    let q: Env::Variable = Env::read_column(env, FFAColumn::Quotient);
33    env.lookup(LookupTable::RangeCheck15, vec![a.clone()]);
34    env.lookup(LookupTable::RangeCheck15, vec![b.clone()]);
35    env.lookup(LookupTable::RangeCheck15, vec![f.clone()]);
36    env.lookup(LookupTable::RangeCheck15, vec![r.clone()]);
37    env.lookup(LookupTable::RangeCheck1BitSigned, vec![q.clone()]);
38    let constraint = if limb_num == 0 {
39        let limb_size = Env::constant(From::from((1 << LIMB_BITSIZE) as u64));
40        let c0: Env::Variable = Env::read_column(env, FFAColumn::Carry(limb_num));
41        env.lookup(LookupTable::RangeCheck1BitSigned, vec![c0.clone()]);
42        a + b - q * f - r - c0 * limb_size
43    } else if limb_num < N_LIMBS - 1 {
44        let limb_size = Env::constant(From::from((1 << LIMB_BITSIZE) as u64));
45        let c_prev: Env::Variable = Env::read_column(env, FFAColumn::Carry(limb_num - 1));
46        let c_cur: Env::Variable = Env::read_column(env, FFAColumn::Carry(limb_num));
47        env.lookup(LookupTable::RangeCheck1BitSigned, vec![c_prev.clone()]);
48        env.lookup(LookupTable::RangeCheck1BitSigned, vec![c_cur.clone()]);
49        a + b - q * f - r - c_cur * limb_size + c_prev
50    } else {
51        let c_prev: Env::Variable = Env::read_column(env, FFAColumn::Carry(limb_num - 1));
52        env.lookup(LookupTable::RangeCheck1BitSigned, vec![c_prev.clone()]);
53        a + b - q * f - r + c_prev
54    };
55    env.assert_zero(constraint);
56}
57
58pub fn constrain_ff_addition<
59    F: PrimeField,
60    Env: ColAccessCap<F, FFAColumn> + LookupCap<F, FFAColumn, LookupTable>,
61>(
62    env: &mut Env,
63) {
64    for limb_i in 0..N_LIMBS {
65        constrain_ff_addition_row(env, limb_i);
66    }
67}
68
69pub fn ff_addition_circuit<
70    F: PrimeField,
71    Ff: PrimeField,
72    Env: ColAccessCap<F, FFAColumn> + ColWriteCap<F, FFAColumn> + LookupCap<F, FFAColumn, LookupTable>,
73>(
74    env: &mut Env,
75    a: Ff,
76    b: Ff,
77) {
78    let f_bigint: BigUint = TryFrom::try_from(Ff::MODULUS).unwrap();
79
80    let a_limbs: [F; N_LIMBS] = limb_decompose_ff::<F, Ff, LIMB_BITSIZE, N_LIMBS>(&a);
81    let b_limbs: [F; N_LIMBS] = limb_decompose_ff::<F, Ff, LIMB_BITSIZE, N_LIMBS>(&b);
82    let f_limbs: [F; N_LIMBS] =
83        limb_decompose_biguint::<F, LIMB_BITSIZE, N_LIMBS>(f_bigint.clone());
84    a_limbs.iter().enumerate().for_each(|(i, var)| {
85        env.write_column(FFAColumn::InputA(i), &Env::constant(*var));
86    });
87    b_limbs.iter().enumerate().for_each(|(i, var)| {
88        env.write_column(FFAColumn::InputB(i), &Env::constant(*var));
89    });
90    f_limbs.iter().enumerate().for_each(|(i, var)| {
91        env.write_column(FFAColumn::ModulusF(i), &Env::constant(*var));
92    });
93
94    let a_bigint = FieldHelpers::to_biguint(&a);
95    let b_bigint = FieldHelpers::to_biguint(&b);
96
97    // TODO FIXME this computation must be done over BigInts, not BigUInts
98    // q can be -1! But only in subtraction, so for now we don't care.
99    // for now with addition only q ∈ {0,1}
100    let (q_bigint, r_bigint) = (a_bigint + b_bigint).div_rem(&f_bigint);
101    let r_limbs: [F; N_LIMBS] = limb_decompose_biguint::<F, LIMB_BITSIZE, N_LIMBS>(r_bigint);
102    // We expect just one limb.
103    let q: F = limb_decompose_biguint::<F, LIMB_BITSIZE, N_LIMBS>(q_bigint)[0];
104
105    env.write_column(FFAColumn::Quotient, &Env::constant(q));
106    r_limbs.iter().enumerate().for_each(|(i, var)| {
107        env.write_column(FFAColumn::Remainder(i), &Env::constant(*var));
108    });
109
110    let limb_size: F = From::from((1 << LIMB_BITSIZE) as u64);
111    let mut carry: F = From::from(0u64);
112    for limb_i in 0..N_LIMBS {
113        let res = a_limbs[limb_i] + b_limbs[limb_i] - q * f_limbs[limb_i] - r_limbs[limb_i] + carry;
114        let newcarry: F = if res == limb_size {
115            // Overflow
116            F::one()
117        } else if res == -limb_size {
118            // Underflow
119            F::zero() - F::one()
120        } else if res.is_zero() {
121            // Neither overflow nor overflow, the transcendent way of being
122            F::zero()
123        } else {
124            panic!("Computed carry is not -1,0,1, impossible: limb number {limb_i:?}")
125        };
126        // Last carry should be zero, otherwise we record it
127        if limb_i < N_LIMBS - 1 {
128            env.write_column(FFAColumn::Carry(limb_i), &Env::constant(newcarry));
129            carry = newcarry;
130        } else {
131            // should this be in circiut?
132            assert!(newcarry.is_zero());
133        }
134        constrain_ff_addition_row(env, limb_i);
135    }
136}
kimchi_msm/ffa/interpreter.rs

kimchi_msm/ffa/
interpreter.rs
