Field-if
Formalization and verification of a circuit
for field ternary conditional.
Given a field element x representing a boolean
(i.e. such that it is either 0 or 1; see boolean-assert),
and given two field elements y and z,
the result w of the ternary conditional
with test x, `then' branch y, and `else' branch z,
is obtained via a constraint of the form
which works as follows:
if x is 0, we have w - z = 0, i.e. w = z;
if x is 1, we have y - z = w - z, i.e. w = y.
This circuit has the same form as boolean-if.
Subtopics
- Field-if-spec
- Specification of the circuit.
- Field-if-correctness
- Correctness of the circuit.
- Field-if-circuit
- Construction of the circuit.
- Field-if-lifting
- Lifting of the circuit to a predicate.
