Function kimchi_msm::fec::interpreter::constrain_ec_addition

source · 
pub fn constrain_ec_addition<F: PrimeField, Ff: PrimeField, Env: ColAccessCap<F, FECColumn> + LookupCap<F, FECColumn, LookupTable<Ff>>>(
    env: &mut Env
)
Expand description

When P = (xP,yP) and Q = (xQ,yQ) are not negative of each other, thus function ensures

P + Q = R where

s = (yP - yQ) / (xP - xQ)

xR = s^2 - xP - xQ and yR = -yP + s(xP - xR)

Equations that we check:

  1. s (xP - xQ) - (yP - yQ) - q_1 f = 0
  2. xR - s^2 + xP + xQ - q_2 f = 0
  3. yR + yP - s (xP - xR) - q_3 f = 0

We will use several different “packing” format.

=== Limb equations

The standard (small limb) one, using 17 limbs of 15 bits each, is mostly helpful for range-checking the element, because 15-bit range checks are easy to perform. Additionally, this format is helpful for checking that the value is ∈ [0,f), where f is a foreign field modulus.

We will additionally use a “large limb” format, where each limb is 75 bits, so fitting exactly 5 small limbs. This format is effective for trusted values that we do not need to range check. Additionally, verifying equations on 75 bits is more effective in terms of minimising constraints.

Regarding our /concrete limb/ equations, they are different from the generic ones above in that they have carries. The carries are stored in a third format. Let us illustrate the design on the first equation of the three. Its concrete final form is as follows:

for i ∈ [0..2L-2]: \sum_{j,k < L | k+j = i} s_j (xP_k - xQ_k) - ((yP_i - yQ_i) if i < L else 0) - q_1_sign * \sum_{j,k < L | k+j = i} q_1_j f_k - (c_i * 2^B if i < 2L-2 else 0) + (c_{i-1} if i > 0 else 0) = 0

First, note that the equation has turned into 2L-2 equations. This is because the form of multiplication (and there are two multiplications here, s*(xP-xQ) and q*f) implies quadratic number of limb multiplications, but because our operations are modulo f, every single element except for q in this equation is in the field.

Instead of having one limb-multiplication per row (e.g. q_1_5*f_6), which would lead to quadratic number of constraints, and quadratic number of intermediate-representation columns, we “batch” all multiplications for degree $i$ in one constraint as above.

Second, note that the carries are non-uniform in the loop: for the first limb, we only subtract c_0*2^B, while for the last limb we only add the previous carry c_{2L-3}. This means that, as usual, the number of carries is one less than the number of limb-equations. In our case, every equation relies on 2L-2 “large” carries.

Finally, small remark is that for simplicity we carry the sign of q separately from its absolute value. Note that in the original generic equation s (xP - xQ) - (yP - yQ) - q_1 f = 0 that holds over the integers, the only value (except for f) that can actually be outside of the field range [0,f-1) is q_1. In fact, while every other value is strictly positive, q_1 can be actually negative. Carrying its sign separately greatly simplifies modelling limbs at the expense of just 3 extra columns per circuit. So q_1 limbs actually contains the absolute value of q_1, while q_1_sign is in {-1,1}.

=== Data layout

Now we are ready to present the data layout and to discuss the representation modes.

Let L := N_LIMBS_LARGE S := N_LIMBS_SMALL

variable offset length comment

xP: 0 L Always trusted, not range checked yP: 1L L Always trusted, not range checked xQ: 2L L Always trusted, not range checked yQ: 3L L Alawys trusted, not range checked f: 4L L Always trusted, not range checked xR: 5L S yR: 5L + 1S S s: 5L + 2S S q_1: 5L + 3S S q_2: 5L + 4S S q_3: 5L + 5S S q_2_sign: 5L + 6S 1 q_1_sign: 5L + 6S + 1 1 q_3_sign: 5L + 6S + 2 1 carry_1: 5L + 6S + 3 2S+2 carry_2: 5L + 8S + 5 2S+2 carry_3: 5L + 10S + 7 2S+2

As we said before, all elements that are either S small limbs or 1 are for range-checking. The only unusual part here is that the carries are represented in 2*S+2 limbs. Let us explain.

As we said, we need 2L-2 carries, which in 6. Because our operations contain not just one limb multiplication, but several limb multiplication and extra additions, our carries will /not/ fit into 75 bits. But we can prove (below) that they always fit into 79 limbs. Therefore, every large carry will be represented not by 5 15-bit chunks, but by 6 15-bit chunks. This gives us 6 bits * 6 carries = 36 chunks, and every 6th chunk is 4 bits only. This matches the 2S+2 = 36, since S = 17.

Note however since 79-bit carry is signed, we will store it as a list of [15 15 15 15 15 9]-bit limbs, where limbs are signed. E.g. 15-bit limbs are in [-2^14, 2^14-1]. This allows us to use 14abs range checks.

=== Ranges

Carries for our three equations have the following generic range form (inclusive over integers). Note that all three equations look exactly the same for i >= n except the carry from the previous limbs.

Eq1.

  • i ∈ [0,n-1]: c1_i ∈ [-((i+1)2^(b+1) - 2i - 3), (i+1)2^(b+1) - 2i - 3] (symmetric)
  • i ∈ [n,2n-2]: c1_i ∈ [-((2n-i-1)2^(b+1) - 2(2n-i) + 3), (2n-i-1)2^(b+1) - 2(2n-i) + 3] (symmetric)

Eq2.

  • i ∈ [0,n-1]: c2_i ∈ [-((i+1)2^(b+1) - 2i - 4), if i == 0 2^b else (i+1)*2^b - i]
  • i ∈ [n,2n-2]: c2_i ∈ [-((2n-i-1)2^(b+1) - 2(2n-i) + 3), (2n-i-1)2^(b+1) - 2(2n-i) + 3 - (if i == n { n-1 } else 0) ]

Eq3.

  • i ∈ [0,n-1]: c3_i ∈ [-((i+1)2^(b+1) - 2i - 4), (i+1)*2^b - i - 1]
  • i ∈ [n,2n-2]: c3_i ∈ [-((2n-i-1)2^(b+1) - 2(2n-i) + 3), (2n-i-1)2^(b+1) - 2(2n-i) + 3 - (if i == n { n-1 } else 0) ]

Absolute maximum values for all carries: Eq1.

  • Upper bound = -lower bound is achieved at i = n-1, n2^(b+1) - 2(n-1) - 3
    • (+-) 302231454903657293676535

Eq2 and Eq3:

  • Upper bound is achieved at i = n, (n-1)2^(b+1) - 2n + 3 - n -1
    • 226673591177742970257400
  • Lower bound is achieved at i = n-1, n2^(b+1) - 2(n-1) - 4
    • (-) 302231454903657293676534

As we can see, the values are about 2*n=8 times bigger than 2^b, so concretely 4 extra bits per carry will be enough. This implies that we can /definitely/ fit a large carry into 6 small limbs, since it has 15 “free” bits of which we will use 4 at most.

@volhovm: Soundness-wise I am not convinced that we need to enforce these more precise ranges as compared to enforcing just 4 bit more for the highest limb. Even checking that highest limb is 15 bits could be quite sound.