Mod Builtin Constraints

lambdaclass / cairo-vm

cairo-vm is a Rust implementation of the Cairo VM. Cairo (CPU Algebraic Intermediate Representation) is a programming language for writing provable programs, where one party can prove to another that a certain computation was executed correctly without the need for this party to re-execute the same program.

Apache License 2.0

518 stars 148 forks source link

Right now, modulo builtin constraints are not always fulfilled.

Given a sub mod gate (for example: x3 = x2 - x1), then it must always be true that x3 + x1 - x2 = 0 or p.

Take, for example, x2 = p + 1 and x1 = 1. Our current implementation will calculate x3 = 0 as a result of the operation (x2 - x1) % p. The expected output is p, as it's the minimum value that meets the constraint (p + 1 - (p + 1) = 0). (the other possible value is 2p.

See https://github.com/starkware-libs/cairo-lang/pull/196 and cairo-lang implementation as reference.

lambdaclass / cairo-vm

Mod Builtin Constraints #1835