fix: incorrect calc of surfeit related value in EmulatedFpVar

[yuxqiu]

Description

Currently, the following invariant is not maintained when computing num_of_additions_over_normal_form in sub_without_reduce and prod_of_num_of_additions in mul_without_reduce

• For AllocatedEmulatedFpVar, no limb has a value > (num_of_additions_over_normal_form + 1) * (2^{bits_per_limb} - 1).
• For AllocatedMulResultVar, no limb has a value > (prod_of_num_of_additions + 1) * (2^{bits_per_limb} - 1).

More specifically, these values are currently underestimated.

This will result in generating constraints in group_and_check_equality that can't be satisfied, since the surfeit value is used to determine how many limbs to put into a group. For example, in my overload, underestimating the surfeit value resulted in putting one more limb value in a group, which resulted in an overflow in let eqn_left = left_total_limb + pad_limb + &carry_in - right_total_limb; and made eqn_left. conditional_enforce_equal(&eqn_right, &Boolean::<BaseF>::TRUE) not satisfiable.

The patch also fixed the overhead! macro, which did not compute ceil(log2(x)) correctly.

Since it's not easy to create test cases that will trigger the constraint system to be unsatisfied, I've just added two tests to ensure that the above invariant is satisfied. Hopefully these two test cases will also help people contribute to this part of the library in the future by documenting the invariant used throughout the implementation.

A few more questions

1. I'm not sure why in post_add_reduce the reduction is only performed when 2 * params.bits_per_limb + surfeit + 1 >= BaseF::MODULUS_BIT_SIZE. I think that checking that params.bits_per_limb + some constant >= BaseF::MODULUS_BIT_SIZE is sufficient. This similar pattern is also present in sub_without_reduce. If there is no particular reason, I think we can fix it to accurately reflect the upper bounds of the bit size.

2. Currently, the add and add_constant implementations in AllocatedMulResultVar don't seem to reduce the results when prod_of_num_of_additions is large enough. This seems to be an issue that needs to be fixed.

---

Before we can merge this PR, please make sure that all the following items have been
checked off. If any of the checklist items are not applicable, please leave them but
write a little note why.

• Targeted PR against correct branch (master)
• Linked to Github issue with discussion and accepted design OR have an explanation in the PR that describes this work. (not applicable)
• Wrote unit tests
• Updated relevant documentation in the code
• Added a relevant changelog entry to the Pending section in CHANGELOG.md
• Re-reviewed Files changed in the Github PR explorer

[Pratyush]

Thank you for the PR! @weikengchen is the better reviewer for this

[Pratyush]

cc @weikengchen could you take a look at this.