Underconstrained div and mod

[emmorais]

When we compute div and mod we use the non-deterministic equation a = b.div + mod, and we constraint mod < b. However, in the field we can easily (if non-zero b) compute div = (a - mod)*inv(b), then an attacker could choose any mod he wants, and set div as before. What is wrong? We also need to check div and mod are u64, and this check is lacking in the old circuit.

Implement a gadget that attests correct u64 range showing a non-deterministic 64-bit decomposition.

[emmorais]

This must also be fixed in the old circuit.

[huitseeker]

See #664

[arthurpaulino]

No longer relevant in LEM