Boolean-xor
Formalization and verification of a circuit
for boolean exclusive disjunction.
Given two field elements x and y representing booleans
(i.e. such that each field element is either 0 or 1;
see boolean-assert),
their exclusive disjunction z is obtained via
a constraint of the form
which is equivalent to
which defines z to be
1 if x is 1 and y is 0,
1 if x is 0 and y is 1,
0 if x and y are both 1, and
0 if x and y are both 0.
Thus, z is boolean (0 or 1) if both x and y are.
Subtopics
- Boolean-xor-correctness
- Correctness of the circuit.
- Boolean-xor-spec
- Specification of the circuit.
- Boolean-xor-circuit
- Construction of the circuit.
- Boolean-xor-lifting
- Lifting of the circuit to a predicate.
