Field-div-checked
Formalization and verification of a circuit
for checked field division.
Given two field elements x and y,
their quotient z is obtained
by combining field-inv-checked and field-mul
to obtain the inverse of y and multiply it by x:
If y is 0, the circuit has no solution,
because field-inv-checked has no solution:
this is why this is `checked' field division.
Subtopics
- Field-div-checked-spec
- Specification of the circuit.
- Field-div-checked-circuit
- Construction of the circuit.
- Field-div-checked-lifting
- Lifting of the circuit to a predicate.
