HackMD#4 - Home Edition
ZkpComRef: Interfaces, Formats and Interoperability
Please start by reading the editorial disclaimer to ensure proper expectations about the process.
Collaboration Instructions
This page was prepared for a breakout session during the ZKProof 4th workshop in order to receive concurrent/collaborative suggestions of content that may be useful for the "ZKProof Community Reference" (ZkpComRef).
Goal: this document will focus on expanding Section 3.4 on APIs and File Formats and Section 3.7 on Constraint-System Interoperability.
Content
Each contribution should be either self-contained or written within the context of the section (as an edit of the current subsections). The field is advancing fast, and more interesting solutions for interfacing between frontends and backends are being published, different formats (PLONK, R1CS, Circuits, etc.) are being built and more needs for interoperability exist.
Contributors are free to chose the relevant topics, either expanding on existing titles or adding new subsections. Here is a list of potential topics to be covered:
Examples of topics:
- Concrete / reference APIs for the different systems: can we build a generic API that would be used across the board in a "plug-and-play" manner? what would be the challenges?
- Backends APIs
- Frontend APIs
- Communication APIs
- Descriptions of file formats: what other formats exist (aside from R1CS) that can be used with ZK systems? For each maybe describe them, their mathematics, what are the (dis)advantages over others and how are they used in ZK proving systems?
- R1CS and different versions. There are other "light-weight" constraint systems that are similar to R1CS.
- Arithmetic and Boolean Circuits. The most common form of encoding computational statements is in circuit form.
- PLONK and Custom Gates. The PLONK encoding format comes with the advantage of defining custom gates that can compute functions in a "cheaper form".
- Expand on the Frontend-Backend interoperability section: what are some more advanced "features" that can be supported by such intermediate representations in the interoperability systems? What should be the scope of such systems (tooling, communication framework?)
- Textual vs binary representations
- Recursive composition of proofs: these can improve the performance and functionality ofZK proof systems in applications that deal with multi-stage computation or large amounts of data.
- Proof-carrying data (PCD) compliance predicates are constraint systems with additional conventions that determine theirsemantics, and for interoperability these conventions require precise specification.
- If we are to use different ZK systems for different parts of the composition, how are these interoperable?
- Extended forms of interoperability: Beyond interfacing between frontend and backend, there are other forms of interoperability (see Section 3.7)
- Proof interoperability
- Procedural interoperability
- Common reference string
Guidelines
What to include in the contribution:
Each contribution may have a different set of requirements or "titles", please try to think about the following questions when you write the contribution:
- What would be most relevant to discuss in the context of ZKProof and the ZkpComRef?
- How can you describe the topic in the simplest way without losing technical depth?
- How does the topic at hand fit within the larger picture of ZKP systems?
- Are there any efficiency trade-offs to keep in mind?
- What kind of adoption would be required in order for this topic to become a standard?
Add your contribution:
Email confirmation: After adding a contribution, please send a brief email to editors@zkproof.org to confirm your suggestion (mention the suggestion number and title).
Contribution #0: TEMPLATE VERSION
Do not edit or delete this template; instead, copy-paste its content inside one of the available suggestion placeholders below, and then edit it there.
Suggested by : Daniel Benarroch (daniel@qed-it.com)Example
Topic Description
what are you contributing about?
Specification
please say more, with technical details?
Considerations
how does this fit in the larger picture?
Contribution #1: PFCS (Prime Field Constraint System)
Suggested by : Alessandro Coglio (coglio@kestrel.edu, acoglio@aleo.org)Eric McCarthy (mccarthy@kestrel.edu, ericm@aleo.org)...
Topic Description
This is a possible generalization of R1CS and other constraint systems used in zero-knowledge proofs. The inspiring purpose is to facilitate formal proofs of correctness of R1CS with respect to higher-level specifications, but it may have broader uses.
Specification
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 generalizes R1CS 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.
This is a prototype formalization of PFCS in the ACL2 theorem prover: https://github.com/acl2/acl2/tree/master/books/kestrel/crypto/pfcs
This is the hyperlinked documentation generated from that code:
https://www.cs.utexas.edu/users/moore/acl2/manuals/current/manual/?topic=PFCS____PRIME-FIELD-CONSTRAINT-SYSTEMS
Considerations
This seems a fairly simple idea, and may overlap with other similar initiatives in zkinterface and elsewhere. The details may vary, but the main idea is to provide more structure.
Formal verification is facilitated by the additional structure in the same way as procedural decomposition facilitates traditional program verification.
Contribution #2: zkInterface
Suggested by : Eran Tromer...
(copy-paste here the template)
Contribution #3: SIEVE IR
Suggested by : Eran TromerKimberlee Model (kimee@stealthsoftwareinc.com)...
Not yet public, but we can start preparing.
(copy-paste here the template)
The SIEVE IR is a circuit based intermediate representation currently in progress within DARPA's SIEVE program. The IR is based on circuits, and is parameterizable along two axis.
- Gate set: Arithmetic or Boolean gate sets.
- Uniformity: non uniform is a list of gates for streaming. Uniformity (work in progress) uses nested scopes to convey structure.
The IR comes with three "resources" as the inputs to a proof system. The relation defines a circuit, while two input streams provide common inputs (instance) and prover inputs (short witness).
Contribution #4: ACIR (Abstract Circuit Intermediate Representation)
Suggested by : Kevname2
A uniform constraint system over proving systems and NP relation (R1CS and PLONK-CSAT).
It allows uniformity over any proving system by allowing for black box functions, and special opcodes which allow for prover provided values.
(copy-paste here the template)
Contribution #5: UltraPLONK
Suggested by : Eran Tromer
Format
To specify the constraint system used in PLONK in an abstract manner, we need to specify:
- The width
- The available custom constraints
One format which can be used to accomodate for custom constraints, is to view them as blackbox functions, where their functionality is known beforehand. This suggestion assumes the custom constraints are known along with their functionality.
The width is unbounded, which means that you can have any fan-in, fan-out configuration.
The available constraints are not theoretically bounded, so the format should accomodate for this.
A custom constraint can be seen as a polynomial identity which is encoded in this PLONK configuration.
The available custom constraints are accumulated into a quotient polynomial, where the degree of the quotient polynomial is a function of the degree of the highest polynomial identity.
(copy-paste here the template)
