Field-div-flagged
Formalization and verification of a circuit
for flagged field division.
This is not yet implemented in snarkVM.
Given two field elements x and y,
the constraints
work as follows:
if y \neq 0,
the second constraint becomes e = 0,
the first constraint becomes w = 1 / y,
the third constraint becomes z = x w = x / y,
and the fourth constraint disappears;
if y = 0,
the second constraint disappears,
the first constraint becomes e = 1,
the third constraint becomes y = 0,
and the fourth constraint becomes z = 0.
In other words,
e is an error flag,
signaling whether the division of x by y
is defined (0) or not (1):
if the error flag is 0, x is the quotient of x and y;
if the error flag is 1, z is totalized to be 0,
and w can be anything.
Note the similarity with field-inv-flagged.
Subtopics
- Field-div-flagged-correctness
- Correctness of the circuit.
- Field-div-flagged-spec
- Specification of the circuit.
- Field-div-flagged-circuit
- Construction of the circuit.
- Field-div-flagged-lifting
- Lifting of the circuit to a predicate.
