		Search-engine friendly clone of the ACL2 documentation.

Prime-field-constraint-systems

A library for PFCS (Prime Field Constraint Systems).

The notion of PFCS is introduced by this library; it is not an existing notion that this library formalizes. We use the acronym `PFCS' for both singular (`System') and plural (`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 PFCS stems from zero-knowledge proofs, but there may be more general applications. PFCS generalize R1CS (Rank-1 Constraint Systems), which are used in zero-knowledge proofs, in two ways:

Constraints in PFCS are not limited to the R1CS form (i.e. equality between a product of two linear polynomials and a linear polynomial). They 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, PFCS generalize R1CS, and likely (or eventually) other forms of constraints used in zero-knowledge proofs, e.g. PLONK. The richer representation also supports more elaborate transformations of the constraints.
Constraints in PFCS 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 (R1CS or others), and supports more modular verification, analysis, transformation, and synthesis.

Currently this library contains an abstract syntax of PFCS, some operations on the abstract syntax, and a semantics expressed as a shallow embedding; see the documentation of these artifacts for more information. It also includes some examples. It is expected that this library will be extended with more artifacts related to PFCS.

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 some more general form of constraints.

This library makes use of the prime fields library and is related to the R1CS library in the community books.

Subtopics

Proof-support: Proof support for PFCS.
Semantics: Semantics of PFCS.
Abstract-syntax: Abstract syntax of PFCS.
Well-formedness: Well-formedness of PFCS.
Abstract-syntax-operations: Operations on the abstract syntax of PFCS.