Field-div-unchecked
Formalization and verification of a circuit
for unchecked field division.
Given two field elements x and y,
such that y is not 0,
their quotient z is obtained via a constraint
This assumes y \neq 0,
in which case the constraint is equivalent to z = x / y.
If y = 0 and x \neq 0,
the constraint has no solution;
but if y = x = 0, the constraint is satisfied
and the result z is unconstrained.
Thus, this circuit must be used only if y is knownn to be non-zero
(e.g. as a postcondition for some previous operation);
this is why this is `unchecked' field division.
Because of the indeterminacy of z when x = y = 0,
this circuit cannot represent a deterministic computation
of z from x and y, unless y \neq 0.
Subtopics
- Field-div-unchecked-spec
- Specification of the circuit.
- Field-div-unchecked-circuit
- Field-div-checked-correctness
- Correctness of the circuit.
- Field-div-unchecked-lifting
- Lifting of the circuit to a predicate.
