Boolean-assert-true
Formalization and verification of a circuit
for asserting that a boolean is true.
Given a field element x representing a boolean
(i.e. such that the field element is either 0 or 1;
see boolean-assert),
this circuit constrains it to be `true`, i.e. to be 1,
via a single 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.
This could be a more general to assert that a field element is 1.
We may replace this circuit with that one at some point.
Subtopics
- Boolean-assert-true-circuit
- Construction of the circuit.
- Boolean-assert-true-spec
- Specification of the circuit.
- Boolean-assert-true-correctness
- Correctness of the circuit.
- Boolean-assert-true-lifting
- Lifting of the circuit to a predicate.
