|
|
|---|
|
|
|
|---|
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. 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.