AVM: MUL u128 is not properly constrained

[jeanmon]

In alu.pil, the following variable
pol PRODUCT = a_lo * b_lo + (1 - u1_tag) * (LIMB_BITS_POW * partial_prod_lo + MAX_BITS_POW * (partial_prod_hi + a_hi * b_hi));
might overflow the field when operand type is u128. Namely, a_hi and b_hi are of size 64 bits and MAX_BITS_POW=2^128.
Note that modifications of PRODUCT might affect division relation as well.