Function kimchi_msm::ffa::interpreter::constrain_ff_addition_row
source · pub fn constrain_ff_addition_row<F: PrimeField, Env: ColAccessCap<F, FFAColumn> + LookupCap<F, FFAColumn, LookupTable>>(
env: &mut Env,
limb_num: usize
)
Expand description
Constraint for one row of FF addition:
- First: a_0 + b_0 - q * f_0 - r_0 - c_0 * 2^{15} = 0
- Intermediate: a_i + b_i - q * f_i - r_i - c_i * 2^{15} + c_{i-1} = 0
- Last (n=16): a_n + b_n - q * f_n - r_n + c_{n-1} = 0
q, c_i ∈ {-1,0,1} a_i, b_i, f_i, r_i ∈ [0,2^15)