bellpepper-emulated: Add missing final carry check and fix limb count calculation

[avras]

I missed the final carry check in the limb-wise equality check code in crates/emulated/src/field_ops.rs:assert_limbs_equality_slow. Adding this check revealed another bug which was under-counting the number of new limbs in crates/emulated/src/field_element.rs:compact_limbs.

This PR fixed these bugs and updates the constraint counts (which have all increased). I am marking this PR as draft as I could not calculate the updated counts in the crates/bls12381/src/curves/pairing.rs. My machine ran out of RAM. If someone can tell me the updated values, I can add them.
EDIT: I got the updated number of constraints and variables from Github test failures.

Explanation

When two non-native field elements are equal, it is not necessary that their respective limbs will all be equal to each other. But they will be equal as big integers.

For example, suppose the limb width is 4 bits. The integer 100 can be written as $a = 6 \times 2^4 + 4$ and $b = 5 \times 2^4 +20$. The limbs of $a$ are $a_0=4, a_1=6$ and the limbs of $b$ are $b_0 = 20, b_1 =5$. There is no overflow in the limbs of $a$ while the limbs of $b$ have an overflow of 1 bit. The overflow allows the two different sets of limbs to represent the same integer. The difference of the limbs $a_0 - b_0 = -16$. This means that $-1$ has to be carried and added to the difference $a_1 - b_1 = 1$.

To prevent underflow, the carry is first calculated by adding an offset max_value. In the next limb, the shifted version of max_value given by max_value_shifted is deducted.

The pseudo-code for the limb-wise equality check is as follows:

max_limbs = max(a.num_limbs, b.num_limbs)
max_value = 1 << (num_bits_per_limb + num_carry_bits)
max_value_shifted = 1 << num_carry_bits
carry = 0

for i in 0..max_limbs:
    e[i] = max_value + carry

    if i < a.num_limbs:
        e[i] = e[i] + a[i]
    if i < b.num_limbs:
        e[i] = e[i] - b[i]

    if i > 0:
        e[i] = e[i] - max_value_shifted
    
    if least_significant_num_bits_per_limb(e[i]) != 0:
        exit with error

    carry = e[i] >> num_bits_per_limb

assert_is_equal(carry, max_value_shifted)

I missed the assert_is_equal check in the last line. A more detailed explanation can be found in Section 5.5 of the document at https://github.com/avras/bellpepper-gadgets/blob/emulated-overflow-fix/crates/emulated/docs/overflow.pdf.

I discovered the missing check while working out the overflow bounds. That requires some changes to emulated as well. But I wanted to restrict the fix in this PR to final carry check and correct limb count calculation.

[wwared]

Thank you for the investigation and fix!

To sanity check my understanding, in the pseudocode and in the pdf (caveat: I have not fully read it yet), should the least_significant_64_bits(e[i]) actually be something like least_significant_num_bits_per_limb_bits(e[i]) since the limbs are not necessarily 64 bits long? (I believe this is the case, since the pdf considers the limb_width = 64 case for simplicity, but I wanted to double check)

Also, I'm not sure where in the emulated code we currently handle the if least_significant_64_bits(e[i]) != 0: exit with error check, shouldn't there be some check on the least-significant-bits of diff_num to follow the pseudocode correctly? Reading the pdf (though I did not read it all yet), it seems like this is always true if qn = d, but that is precisely what this is aiming to check, so we need to perform this check. Am I misunderstanding something, e.g. is this check being made implicitly inside right_shift, or it's not necessary to be specified as a constraint, or would this be part of the follow-up changes to emulated and is unrelated to the fix in this PR?

Regarding the CI clippy failure, feel free to cherry-pick ff3e970 onto your branch (or run clippy --fix locally if you prefer). The clippy::useless_vec got turned on by default in the latest rust stable release.

[avras]

To sanity check my understanding, in the pseudocode and in the pdf (caveat: I have not fully read it yet), should the least_significant_64_bits(e[i]) actually be something like least_significant_num_bits_per_limb_bits(e[i]) since the limbs are not necessarily 64 bits long? (I believe this is the case, since the pdf considers the limb_width = 64 case for simplicity, but I wanted to double check)

Yes, you are right. It should be least_significant_num_bits_per_limb instead of least_significant_64_bits. If a compaction of limbs occurs, the num_bits_per_limb can be higher than the initial limb width (like 64). I have modified the pseudocode in the PR text. I will change it in the pdf as well.

Also, I'm not sure where in the emulated code we currently handle the if least_significant_64_bits(e[i]) != 0: exit with error check, shouldn't there be some check on the least-significant-bits of diff_num to follow the pseudocode correctly? Reading the pdf (though I did not read it all yet), it seems like this is always true if qn = d, but that is precisely what this is aiming to check, so we need to perform this check. Am I misunderstanding something, e.g. is this check being made implicitly inside right_shift, or it's not necessary to be specified as a constraint, or would this be part of the follow-up changes to emulated and is unrelated to the fix in this PR?

The check that the num_bits_per_limb least significant bits of diff_num are all zero bits is part of right_shift. We call right_shift with start_digit = num_bits_per_limb and end_digit = num_bits_per_limb + num_carry_bits + 1.

carry = Self::right_shift(
        &mut cs.namespace(|| format!("right shift to get carry {i}")),
        &diff_num,
        num_bits_per_limb,
        num_bits_per_limb + num_carry_bits + 1,
 )?;

In right_shift, we do the following

• The value of diff_num is decomposed into a little-endian bit vector v_bits
• A Boolean vector v_booleans is allocated using the v_bits[start_digit...end_digit]. This vector will have num_carry_bits + 1 elements.
• The bits in v_booleans are weighted by powers of 2 to get sum_higher_order_bits as
  sum_higher_order_bits = v_boolean[0] 2^(start_digit) + v_boolean[1] 2^(start_digit + 1) + ... + v_boolean[end_digit-start_digit-1] 2^(end_digit)
• The value of diff_num is checked to be equal to the value of sum_higher_order_bits here. If the any of the num_bits_per_limb least significant bits of diff_num are not zero, this check will fail.

Regarding the CI clippy failure, feel free to cherry-pick ff3e970 onto your branch (or run clippy --fix locally if you prefer). The clippy::useless_vec got turned on by default in the latest rust stable release.

Thanks for the clippy fix. I have added it to the PR.

[wwared]

In right_shift, we do the following [...]

Thanks for the explanation! I noticed that we were skipping the first start_digit bits when doing the weighted sum, but I see now that the final comparison would indeed fail if any of those lower bits are set!

Thanks for the clippy fix. I have added it to the PR.

Sorry, I forgot to run cargo fmt after the clippy fix, you'll also need to apply 997030c. Once CI is passing I can re-approve the PR if necessary

[avras]

While replacing the 64 bits with limb_width in the pdf, I realized that the formula for number of limbs that can be combined was too conservative. I have made changes to the pdf. Please use the latest version for review. Thanks!

[avras]

While replacing the 64 bits with limb_width in the pdf, I realized that the formula for number of limbs that can be combined was too conservative. I have made changes to the pdf. Please use the latest version for review. Thanks!

@wwared Please re-approve this PR. I only added the cargo fmt commit. The above comment was a request to review the latest pdf which describes fixes to the overflow bounds. I will be submitting a separate PR for these fixes.