# zkInterface: SIEVE Intermediate Representation (IR) Proposal

## Introduction

As part of the SIEVE program, TA1 and TA2 performers are required to interoperate by generating or consuming the same intermediate representation (IR) of zero-knowledge statements. This document contains a brief description of the zkInterface interoperability tool, and focuses on outlining the relevant and important features.

[zkInterface](https://github.com/QED-it/zkinterface) is the first such proposal, allowing TA1 performers to use the most suitable and convenient TA2 proving system, and viceversa, without having to implement every possible connection. Furthermore, zkInterface can facilitate the process of testing and evaluation (T&E) for the deliverables of different performers.

zkInterface was created as part of the [ZKProof Standardization effort](https://zkproof.org), where it quickly got traction becoming the standard tool for interoperability between frontends and backends.

## Resources

- **ZKProof Discussion Recording:** As a good introduction, [here is the recording](https://youtu.be/_d9d4K2P5dk) of the latest presentation (and discussion) at the [3rd ZKProof Workshop](https://zkproof.org/events/workshop3/).
- **Latest Version of the Specification:** The [latest version of the specification](https://docs.zkproof.org/pages/standards/accepted-workshop3/proposal-zkinterface.pdf) was last updated in early February for the workshop submissions.
- **GitHub Repo:** [Here is the official repository of zkInterface](https://github.com/QED-it/zkinterface).
- **WebAssembly Demo:** [Here you can find a browser demo using WebAssembly](https://qed-it.github.io/zkinterface-wasm-demo/).

For questions, comments, or if you are interested to use zkInterface, contact us at [e-mail], [e-mail] and [e-mail].

## Overview

zkInterface is a framework for enabling the interoperability of zero-knowledge proof systems by defining a standard file format for the intermediate representations used. The high-level goal is to enable decoupling of frontends from backends, allowing application writers to choose the frontend most convenient for their functional and development needs and combine it with the backend that best matches their performance and security needs. This includes communicating constraint systems, communicating variable assignments (for production of proofs), and also construction of constraint systems out of smaller building blocks (gadgets) possibly implemented by different authors and frameworks, as seen below

> In green you can see the frontends and backends implemented in zkInterface today.

zkInterface defines a standard format for both the statement and witness reductions, communicating the high-level statement and the variable assignments.

For the full specification, please see the latest version of the proposal.

### Desiderata

- Interoperability across frontend frameworks and programming languages.
- Ability to write \emph{gadgets} (reusable chunks of constraint systems) that can be consumed by different frontends and backends.
- Minimize copying and duplication of data.
- Support constraint system construction and witness reduction should be low (and in particular, linear) compared to a native implementation of the same gadgets in existing frameworks.
- Expose details of the backend's interface that are necessary for performance (e.g., constraint system representation and algebraic fields).
- Support all popular/important constraint system styles, starting with R1CS (implemented) and Boolean/arithmetic circuits (work in progress)

### A Calling Convention

zkInterface is first and foremost a standard file format to enable interoperability between different frameworks and languages (you can find the specific serialization in the [spec](https://docs.zkproof.org/pages/standards/accepted-workshop3/proposal-zkinterface.pdf)). This seralized format is, in fact, a special case of zkInterface's general mode of operation, which is as a _calling convention_ between producers and consumers of constraint systems and parts thereof. The standard specifies the protocol for communicating constraint systems, for communicating variable assignments (for production of proofs), and for constructing constraint systems out of smaller building blocks. The latter, in particular, require procedural composition (and thus a calling convention), as discussed below.

Thus, zkInterface is a procedural, purely functional interface for zero-knowledge systems that enables cross-language interoperability and offers the ability to abstractly craft a constraint system building from different gadgets, possibly written in different frameworks, by defining how data should be written and read. The interaction between caller and gadgets is based on exchanging messages. Messages are purely read-only data, which grants a great flexibility to implementations of gadgets and applications. The set of messages is defined by using the FlatBuffers interface definition language, which implies a precise data layout at the byte level. The specification of FlatBuffers can be found [here](https://google.github.io/flatbuffers/).

A simple special case is monolithic representation of a whole constraint system and its variable assignments. However, there are a need for more richer and more nuanced forms of interoperability:

- Precisely-specified statement semantics, variable representation and variable mapping
- Witness reduction, from high-level witnesses to variable assignments
- Gadgets interoperability, allowing components of constraint systems to be packaged in reusable and interoperable form
- Procedural interoperability, allowing execution of complex code to facilitate the above

For a full definition of the messages, channels and flows, see Section 2 in the [zkInterface specification](https://docs.zkproof.org/pages/standards/accepted-workshop3/proposal-zkinterface.pdf).

****

## Features

Most of the features below are not yet implemented into zkInterface, but we collect them below as these are the most interesting elements based on conversations with several performers for the SIEVE program.

Multiple paths for evolution and extensions of the standard are possible, thanks to the flexibility and backward-compatibility features of the encoding. The encoding is designed to require little to no data transformation, making it possible to implement the standard with minimal overhead in very large applications.

>Note that, except the first feature, the following are mostly work-in-progress. We welcome any feedback and comment that could contribute to the design of such features.

### 1. Declarative vs. Procedural

This is a core high-level feature, being the fundamental functionality of the framework. We believe that zkInterface can accelerate the adoption of zero-knowledge proofs because it will enable developers to use their prefered pair of systems of their projects, which will lower the barrier to entry and cost of development. Specifically for the SIEVE program, TA1 performers will be able to use the optimal TA2 proving system for their statement and framework.

**Declarative Operation**
In the declarative version of the statement (and witness) generation, zkInterface inputs gadgets written in a specific frontend and outputs a single constraint system, possibly as a fixed file, to be used in the given backend.

**Procedural Operation**
In the procedural setting, zkInterface can generate a constraint system (and witness) by composing gadgets written in different frontends. Different parts of an application may be written in different programming languages, and interoperate through messages. These parts may be linked and executed in a single process, calling functions, and exchanging messages through buffers of shared memory.

This approach enables _gadget interoperability_: exposing modular gadgets, including both their constraint system and associated witness reduction, for use by higher-level frameworks in the compiler/reduction pipeline. For example, libsnark offers a rich library of optimized R1CS gadgets, which developers of several front-end compilers would like to reuse in the context of their own constraint-system construction framework. Since the witness reduction is done anew (dynamically) every time a new proof is needed, it's necessary to support runtime invocation of the gadget provider's code. The calling convention serves this purpose, and is identical to the use used to convey the final constraint system to the cryptographic backend (i.e., the aforementioned serialized format).

In both cases, the message definition and flow are the same, which alludes to the simplicity of the interface design.

### 2. IR Languages Support

zkInterface's existing support and integrations are forthe R1CS constraint system style, which is the native language of many succinct ZK schemes, but is not optimal for some other proving systems nor sufficiently expressive expressive for some front-end optimizations. Thus, zkInterface is being extended to support additional constraint system styles, starting with arithmetic and boolean circuits.

These three constraint system styles (R1CS, arithmetic circuits and Boolean circuts) are similar enough that one can convert between these with acceptable overhead (for typical cases). Thus, we will also provide generic adapters that, for example, consume arithmetics circuit and produce R1CS, using the zkInterface calling convention on both sides. This will further facilitate mixing and matching TA1 frontends and TA2 backends, or at least rapidly prototyping such integration (and then optimize it "natively").

We can even extend zkInterface to allow hybrid circuits that use a mix of arithmetic and boolean operations (for the convenience for the TA1 frontend, that can then use the most natural style for the given computation). A generic zkInterface-based adapter can convert these statement into any backend's desired input language (algebraic constraints, SCALE, boolean circuits).

Further, prospective IR extensions could include custom gates for specifically defined languages such as for [PLONK](https://docs.zkproof.org/pages/standards/accepted-workshop3/proposal-turbo_plonk.pdf), or to include uniform constraint systems for which the prover takes advantage of structure within the statement encoding to improve the efficiency of the prover.

**Profile Definition**

While zkInterface's FlatBuffers-based definiton allows for easily extension to the aforementioned constraint system styles, it is crucial to precisely coordinate between producers (e.g., TA1 frontends) and (e.g., TA2 backends or or gadget authors), so that the former will deliver constraints the latter can process. This includes choice of finite field, topological constraints, gate sets, gate in/out-degree constaints, etc. We are thus defining *profiles* that specify all of these attributes. Frontends and backends can declare which profiles they support, and use zkInterface and its adapters to enforce profiles or (perhaps with some loss of efficiency convert between them.

We suggest the following initial profiles, to be supported by zkInterface and recommended to SIEVE performers as interoperable choices. We will also submit these to the ZKProof Standards process, to encourage their use in the wider ZK ecosystem.

| Attributes | R1CS-$GF_p$ | R1CS-$BN254$ | Arithmetic circuits | Boolean circuits | Char-2 circuits|
| -------- | -------- | -------- | -------- | -------| -------
| **Field** | Any large prime | order of BN254 | large prime | Bit / $GF_2$ | $GF_{2^k}$
| **Gate Set** | Bilinear | Bilinear | Field operations and constants | AND / OR / NOR / XOR | Field operations and constants
| **In-degree** | unlimited | unlimited | 2 | 2 | 2
| **Out-degree** | unlimited | unlimited | 1 | 1 | 1
| **Topology** | unconstrained | unconstrained | DAG | DAG | DAG
| **Constraint ordering** | Any | Any | Topological | Topological | Topological

### 3. Defining a Proving Framework

We seek to extend zkInterface beyond a serialized format and calling convention, to cover additional practical aspects of code integration and deployment at the ZK frontend-gadget-backend interfaces.

#### Linking, Deployment and Execution

Thus far zkInterface has focused on the "wire protocol", i.e., the serialization and calling convention. There is also the question of how the wiring is created. For example, how does the frontend find the backend and establish a bidirectional byte-level channel with it (for transferring the messages)? This could be done by reading and writing designated files, using TCP/IP or local sockets, using dynamic linking and in-memory transfers, by spawning and connecting to Docker containers, or by sharing buffers in a WebAssembly virtual machine. (Incidentally, this last one allows in-browser execution of ZK proving, as shown by our [WebAssembly demo](https://qed-it.github.io/zkinterface-wasm-demo/).)

Evaluators and deployers need to eventually make a concrete choice about how to establish this channel, and how to package the requisite code for easy deployment. Currently this is done ad hoc, which is not overly onerous since the hard part (the _content_ transferred over these channels) is taken care of by zkInterface; but it would be useful to standardize these aspects too.

Similar questions arise at the level of the [Gadget Libraries](#Gadget-Libraries) below.

#### Statement Validator and Proof Emulator

In addition to defining the structure and architecture of the end-to-end ZK system, zkInterface already has the functionality of verifying that a set of variables actually satisfy the given constraints. This will be extended from R1CS to the other profiles.

zkInterface could also be used to call an integrated proof emulator, which emits and consumes proofs placeholders instead of running the actual cryptographic prover. This can be used to (a) simulate the whole workflow of a TA1 application without incurring the actual ZK running times, and (b) estimate these running time using a performance model of the real backend prover.

#### Benchmarking Tooling

Finally, this kind of framework could make zkInterface useful for benchmarking purposes. Combined with a possible system for proof systems comparison (such as [the one submitted to ZKProof](https://docs.zkproof.org/pages/standards/accepted-workshop3/proposal-benchmarking.pdf)), zkInterface could facilitate precise benchmarking process of the TA2 backend performance on well-specified problems emanating from TA1.

### 4. Prospect: Breaking Down Statements

When working with very large statements, it is important, for modular and efficiency reasons, to optimize the statements and circuits at more granular levels. For example, one may want to reuse specific components of a statement, such as a hash function, one-time truth tables or random access memory. Or, one may want to decompose a statement into several fragments, and provem then in parallel or using different techniques. While beyond our immediately scope, we pose these here as potential extensions for which we would garner requirements from TA1 and TA2 performers.

#### Gadget Libraries

zkInterface is designed to allow creation of reusable gadgets (reusable constraint fragments and their associated witness reduction), but does not standardize their choice. There exist libraries of useful gadgets (e.g., in libsnark), and it would be useful to standardize these and create interface-compatible gadgets optimized for other constraint system styles. This would allow high-level TA1 code to rely on the existence of optimized gadgets for arithmetic, memory checking, etc., as a black box that gets instantiated for the specific TA2 backend they link against.

#### Streaming Statements

When dealing with very large statements, as in the SIEVE program, memory footprint can be a crucial bottleneck: the ZK witness data (e.g., program execution traces) may be too large to fit in memory, especially given the cryptographic representations' overhead. Thus, to enable scalable proof generation on memory-constrained machines, we will need provers and verifiers that consume their data as streams and process it on the fly.

zkInterface already has basic support for transferring constraints and variables in a chuncked fashion, and this can be further extended, e.g., by tracking variable dependencies and optimizing constraint orderings accordingly to minimize the requisite state, or by breaking down circuits into linked fragments (see below)

#### Proof Parallelization

Proof parallelization means that the prover algorithm is parallelized across different workers. In fact, not all backend systems are parallelizable, as some have in-series computations that need to be performed. However, for those that are able to parallelize, zkInterface could be extended to map the circuit into the different backend workers, making the connections between the variables and ensuring the integrity of the proving mechanism.

#### Proving with Multiple Proof Systems

Another prospective idea is breaking down constraint systems into linked fragments, each proven separately, potentially using a different proof system. This may be done for streaming-based scalability (see above), or to use proof systems that are optimized for certain tasks. For example, a statement may be best expressed in R1CS, except for its use of AES and SHA-3 hash invocations that are best handled by the Boolean-circuit or characteristic-2 profiles instead. These fragment proofs may be connected in parallel (e.g., by reasoning about the same commitments), or by recursive composition (e.g., Proof-Carrying Data). zkInterface can be extended to facilitate expressing such opportunities, as well as for writing optimizing adapters that find these opportunities automatically.