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)