Boolean-if
Formalization and verification of a circuit
for boolean ternary conditional.
Given three field elements x, y, and z representing booleans
(i.e. such that each field element is either 0 or 1;
see boolean-assert),
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.
Thus, w$ is a boolean if all of @($y and z are.
This circuit has the same form as field-if.
Subtopics
- Boolean-if-spec
- Specification of the circuit.
- Boolean-if-correctness
- Correctness of the circuit.
- Boolean-if-circuit
- Construction of the circuit.
- Boolean-if-lifting
- Lifting of the circuit to a predicate.
