Boolean-not
Formalization and verification of a circuit
for boolean negation.
Given a field element x representing a boolean
(i.e. such that the field element is either 0 or 1;
see boolean-assert),
its negation y is obtained via a constraint of the form
which defines y to be 1 if x is 0, or 0 if x is 1.
Thus, y is boolean (0 or 1) if x is.
Subtopics
- Boolean-not-spec
- Specification of the circuit.
- Boolean-not-circuit
- Construction of the circuit.
- Boolean-not-correctness
- Correctness of the circuit.
- Boolean-not-lifting
- Lifting of the circuit to a predicate.
