		Search-engine friendly clone of the ACL2 documentation.

Projects

Pfcs

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:

Constraints in PFCSes are not limited to the R1CS form (i.e. equality between a product of two linear polynomials and a linear polynomial). PFCS constraints are equalities between any combinations of additions and multiplications (and perhaps more operations in the future); note that addition and multiplication suffice to describe arithmetic circuits. Thus, PFCSes generalize R1CSes, and likely (or eventually) other forms of constraints used in zero-knowledge proofs, e.g. PLONKs. The richer representation can also support more elaborate transformations of the constraints.
PFCS constraints may be hierarchically organized, by naming sets of them as relations with parameters, which may be referenced (i.e. ``called'') in the definition of other relations. This explicates the natural hierarchical structure of zero-knowledge gadgets (in R1CS or other form), and can supports more modular verification, analysis, transformation, and synthesis.

Currently this library contains a concrete syntax of PFCSes and a parser to CSTs (concrete syntax trees), an abstract syntax of PFCSes and an abstractor from CSTs to ASTs (abstract syntax trees), parser interface functions to generate ASTs from strings, some operations on the abstract syntax, a notion of well-formedness, a semantics expressed as a shallow embedding, a semantics expressed as a deep embedding, and some tools to support proofs about PFCSes; see the documentation of these artifacts for more information. 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.

Subtopics

Proof-support: Proof support for PFCSes.
Abstract-syntax: Abstract syntax of PFCSes.
R1cs-subset: R1CS subset of PFCSes.
Semantics: Semantics of PFCSes.
Abstract-syntax-operations: Operations on the abstract syntax of PFCSes.
Indexed-names: Indexed names for PFCS families.
Well-formedness: Well-formedness of PFCSes.
Concrete-syntax: Concrete syntax of PFCSes.
R1cs-bridge: Bridge between PFCSes and R1CSes.
Parser-interface: API functions for parsing PFCS specifications.