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