Check if our inputs are malleable modulo the prime of the Field

[kevaundray]

Problem

Context

Imagine our prime is 7.

If the users program looks like:

fn main(x : Field, y : Field) {
 assert(x == y)
}

It's expected that if x = 2 and y = 2 the proof will verify to be true.

It is not quite expected that if x = 9 and y = 2 that the proof will also pass. Noting that 9 mod 7 == 2.

Issue

Without applying constraints, we cannot ensure that the inputs lie within the correct range [0,7). This can get extremely expensive because we would essentially need to take in bytes as input and then reconstruct each field in the circuit.

Is it an issue?

Technically this is how Field type operates as there is an equivalence relation. Since we don't allow it to done on < and >, this can only trip folks up when doing equality. The reason it is only on equality and not on < and > is because a Field has no ordering, just equality, so the compiler docs would need to clearly note that we are applying extra constraints on top of the definition of a Field in order to have "ordering". This extra constraint would be choosing a representative for each set, usually this is [0, p).

Happy Case

I think a test and documentation around this equality problem would be the best way forward.

Ideally we ask users to avoid using Field wherever possible, but since the proving systems are not fast enough right now, this is a massive performance hit.

Alternatives Considered

No response

Additional Context

No response

Would you like to submit a PR for this Issue?

No

Support Needs

No response

[kevaundray]

For honest users, the check when converting Toml inputs into witnesses is probably enough

[Savio-Sou]

we are applying extra constraints on top of the definition of a Field in order to have "ordering"

What would be the difference between unsigned integers and ordered Fields?

Or were you simply suggesting to document that as the reason of why Fields behave as they do?

[kevaundray]

we are applying extra constraints on top of the definition of a Field in order to have "ordering"

What would be the difference between unsigned integers and ordered Fields?

Or were you simply suggesting to document that as the reason of why Fields behave as they do?

unsigned integers usually mean modulo 2^{bit_size} while an ordered field is a set of numbers usually [0,p-1] ie its modulo p

[kevaundray]

Spoke with Ethan and next steps would be to check if the following compiles and issue warnings if so:

let x : u8 = 300
let x: Field = 9

[jfecher]

That should pass as the expected behavior is to do a modulo. This is why -1 as u8 == 255 currently.
I'm not sure why let x: Field = 9 would be problematic.

[Ethan-000]

tested this

use dep::std;
fn main() {
    let x:u8 = 300;
    std::println(x);
}

with output

"0x012c"
[modulo_overflow_test] Circuit witness successfully solved

[kevaundray]

That should pass as the expected behavior is to do a modulo. This is why -1 as u8 == 255 currently.
I'm not sure why let x: Field = 9 would be problematic.

Should note that with the as keyword it should pass but similar to Rust, the following would error:

fn main() {
    let a : u8 = 300;
}

Because 300 does not fit into a u8.

For

let x : Field = 9;

It was due to the same principal as the u8 example, assuming that the modulus is 7, then 9 does not fit within the valid range for a Fieldtoo

[TomAFrench]

Compare with #2858