Currently, the divMod operation performs bitwise division. Under deterministic computational model, this is the only approach; with the new MonadCircuit interface, we can access the full power of circuit computational model to reduce the number of constraints dramatically.
The idea is: instead of "computing" divMod x y, we can "guess" the result d and m s.t. x = d * y + m and m < y. Outline of the algorithm:
compute witnesses for d and m;
range-constrain them so that values inside fit registers;
Currently, the
divModoperation performs bitwise division. Under deterministic computational model, this is the only approach; with the newMonadCircuitinterface, we can access the full power of circuit computational model to reduce the number of constraints dramatically. The idea is: instead of "computing"divMod x y, we can "guess" the resultdandms.t.x = d * y + mandm < y. Outline of the algorithm:dandm;ms.t.m < y;x = d * y + m.