Field-inv-checked
Formalization and verification of a circuit
for checked field inversion.
Given a field element x different from 0,
its inverse y is obtained via a constraint of the form
which is equivalent to y = 1 / x if x \neq 0.
If x is 0, the constraint has no solution:
this is why this is `checked' field inversion.
Subtopics
- Field-inv-checked-spec
- Specification of the circuit.
- Field-inv-checked-circuit
- Construction of the circuit.
- Field-inv-checked-lifting
- Lifting of the circuit to a predicate.
