Boolean-neq
Formalization and verification of a circuit
for boolean non-equality.
Given two field elements x and y representing booleans
(i.e. such that each field element is either 0 or 1;
see boolean-assert),
the boolean-xor circuit can be also used
to set z to 0 or 1 depending on
whether x and y are equal or not:
Subtopics
- Boolean-neq-spec
- Specification of the circuit.
- Boolean-neq-correctness
- Correctness of the circuit.
- Boolean-neq-circuit
- Construction of the circuit.
- Boolean-neq-lifting
- Lifting of the circuit to a predicate.
