template EnforceMaxBits(n) { assert(n < 254); // Number of bits in the finite field signal input in; // REASON: Num2Bits constrains in to be representable by `n` bits signal output {maxbits} out; out.maxbits = n; Num2Bits(n)(in); out <== in; } // Add two numbers, ensuring that the resut does not overflow template AddMaxBits(){ signal input {maxbits} a; signal input {maxbits} b; // REASON: log(a + b) <= log(2*max(a, b)) = 1 + max(log(a), log(b)) signal output {maxbits} c; c.maxbits = max(a.maxbits, b.maxbits) + 1 assert(c.maxbits < 254); c <== a + b; } // Multiply two numbers, ensuring that the resut does not overflow template MulMaxBits(){ signal input {maxbits} a; signal input {maxbits} b; // REASON: log(a * b) = log(a) + log(b) signal output {maxbits} c; c.maxbits = a.maxbits +…