|
|
|---|
|
|
|
|---|
A library for PFCSes (Prime Field Constraint Systems).
The notion of PFCS (Prime Field Constraint System) is introduced by this library; it is not an existing notion that this library formalizes. We write `PFCS' for the singular `Prime Field Constraint System', and`PFCSes' for the plural `Prime Field Constraint Systems'.
A PFCS is a system of constraints over a prime field; the constraints include variables that range over a prime field. The motivation for PFCSes stems from zero-knowledge proofs, but there may be more general applications. PFCSes generalize R1CSes (Rank-1 Constraint Systems), which are used in zero-knowledge proofs, in two ways:
Currently this library contains a concrete syntax of PFCSes and with a parser to CSTs (concrete syntax trees), an abstract syntax of PFCSes with operations on the abstract syntax trees and with an abstractor from CSTs to ASTs (abstract syntax trees), a notion of well-formedness, a semantics defined as a deep embedding, a parser interface functions to generate abstract syntax from strings written in the concrete syntax, some tools to support proofs about PFCSes, and a lifter to turn abstract syntax into shallowly embedded PFCSes; see the documentation of these artifacts for more information. The library also includes a characterization of PFCSes that only use R!CS constraints, and a translator from R1CSes to PFCSes. This library also includes some examples. This library is a work in progress; it is expected that it will be extended with more artifacts related to PFCSes.
Some of the concepts in this library are more general than prime fields. Thus, it may be possible to generalize some parts of this library to even more general form of constraints.
This library makes use of the prime fields library and is related to the R1CS library, both in the community books.