|
|
|---|
|
|
|
|---|
Formalization and verification of a circuit for asserting that a field element is a boolean (i.e. 0 or 1).
Booleans are represented as field elements that are either 0 (for `false') or 1 (for `true'). This circuit constrains a variable to be either 0 or 1, via a single constrain of the form
which is satisfied iff