|
|
|---|
|
|
|
|---|
Formalization and verification of a circuit for asserting that zero or more field elements are booleans (i.e. 0 or 1).
This is a family of PFCS relations of the form
boolean_assert_all[n](x[0], ..., x[n-1]) := {
boolean_assert(x[0]),
...
boolean_assert(x[n-1])
}where
Currently our PFCS library does not provide a concrete syntax for parameterized PFCS relations such as above. So we construct PFCS abstract syntax, which we lift ``manually'' (not via the lifter). Proofs of correctness are by induction, and cover all the infinitely many members of the family.