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.

[Pratyush]

@yuxqiu Could you update the PR? @weikengchen could you take a look at this?

[yuxqiu]

@yuxqiu Could you update the PR? @weikengchen could you take a look at this?

Sure. It is done now.

[weikengchen]

Let me double check the formula...

[weikengchen]

can you find a test case that will fail or like provide calculations on why?

[weikengchen]

I think unless there is a case when the original implementation does fall short, we will not change the circuit---the arkworks-rs library has been used in a lot of projects, and if you want to change the circuit, it would just "force" a lot of the projects to fork the old circuit and continue to use it. Therefore, I still believe that you need to present a counterexample.

[yuxqiu]

I think unless there is a case when the original implementation does fall short, we will not change the circuit---the arkworks-rs library has been used in a lot of projects, and if you want to change the circuit, it would just "force" a lot of the projects to fork the old circuit and continue to use it. Therefore, I still believe that you need to present a counterexample.

That makes perfect sense. I’ll need a few days to prepare a test case and will get back to you once it’s ready.

[yuxqiu]

@weikengchen It’s all set for review now.

[weikengchen]

Great job. Let me take a look.

[Pratyush]

@weikengchen did you get a chance to look at this?

[weikengchen]

would be great to have someone else to take a careful look

[Pratyush]

hm @weikengchen who would be a good reviewer for this code? I am not familiar with this part of the codebase.