Compiler crashes with "Sum check failed in Lt check" if subtraction inputs are proof inputs

[m1cm1c]

Description

I wrote a subtraction function. It works just fine if its inputs are compile-time constants. However, if they are supplied to the proof, the compiler crashes during witness computation.

Environment

• Compiler version: branch develop (commit 60f91894)
• Operating system: Manjaro

Steps to Reproduce

The following code compiles without issues and a witness can be computed:

/**
* Computes x - y. May overflow (mod p).
*/
def sub<N>(field[N] x, field[N] y) -> field[N]:
    field[N] z = [0; N]
    bool[N + 1] carry = [false; N + 1]
    for u32 i in 0..N do
        z[i] = x[i] - y[i] - (if carry[i] then 1 else 0 fi) // May overflow (mod p).
        carry[i + 1] = z[i] > x[i]
    endfor

    return z

def main() -> field[4]:
    field[4] f1 = [340282366920938463426481119284349108225, 0, 0, 0]
    field[4] f2 = [18446744073709551392, 18446744073709551613, 0, 0]
    field[4] r = sub(f1, f2)
    return r

$ zz compile -i no_bug.zok
Compiling no_bug.zok

Compiled code written to 'out'
Number of constraints: 4
$ zz compute-witness
Computing witness...
Witness file written to 'witness'

Now make the numbers inputs to the proof and the compiler crashes during witness computation:

/**
* Computes x - y. May overflow (mod p).
*/
def sub<N>(field[N] x, field[N] y) -> field[N]:
    field[N] z = [0; N]
    bool[N + 1] carry = [false; N + 1]
    for u32 i in 0..N do
        z[i] = x[i] - y[i] - (if carry[i] then 1 else 0 fi) // May overflow (mod p).
        carry[i + 1] = z[i] > x[i]
    endfor

    return z

def main(field[4] f1, field[4] f2) -> field[4]:
    field[4] r = sub(f1, f2)
    return r

$ zz compile -i bug.zok
Compiling bug.zok

Compiled code written to 'out'
Number of constraints: 4064
$ zz compute-witness -a 340282366920938463426481119284349108225 0 0 0 18446744073709551392 18446744073709551613 0 0
Computing witness...
Execution failed: Sum check failed in Lt check: expected 7237005577332262213973186563042994240829374041602535252466099000494570602495 to equal 21888242871839275222246405745257275088548364400416034343679757442502098944004

[Schaeff]

I reduced this to:

def main(field f1, field f2):
    bool lt = f1 - f2 > f1
    return

When you assign to the carry, you do a dynamic comparison (x < y where neither x nor y is constant), which sadly is not complete in ZoKrates now, see here. In particular, f1 - f2 ends up being a large number (because of an underflow) which is bigger than ~ p/2, which makes the comparison fail.

[Schaeff]

I had a look at the semantics of comparison operators in Circom, it may have a complete operator, in which case we could also use that.

[m1cm1c]

I was not aware of that restriction to comparison operators. Shall I close this issue because I used a comparison operator incorrectly?