isekai technical documentation released!
We have just published the first version of the isekai technical documentation in our GitHub repository. This document explains how to use isekai, how it works under the hood and how we want to it to evolve. Here is a summary of its contents.
isekai is a framework for zero-knowledge proof (ZKP) applications, built with the support of the Fantom Foundation. It aims to provide easy-to-use interfaces to several zero-knowledge proof implementations for programs written by mainstream software engineers, i.e. those who do not specialise in verifiable computation or ZKP. In a nutshell: using isekai, you can generate a proof that you have executed a computer program (that’s the “verifiable computation” part) without providing all the inputs of that computation (that’s the “zero knowledge“ part).
The documentation explains the architecture of isekai and how it is designed to be flexible so that we can easily improve on our three main goals: programming language support, programming language features and zero-knowledge proof schemes.
Usage
The “Usage” section details how to generate a proof of simple C programs. Most of this was already covered in our “First steps with isekai on Windows” article.
Architecture
The four main components of isekai are presented:
- The “frontend”, which parses C code and transforms it into the intermediate form (expression graph)
- The “backend”, which takes the expression graph produced by the frontend and produces either an arithmetic or boolean circuit
- The “reducer”, which takes an arithmetic circuit and produces R1CS
- The “prover”, which takes R1CS and generates a proof of execution
This modular architecture allows for a simple workflow that follows a waterfall pattern.
It has been designed to facilitate:
- the support of additional programming languages for the input source code
- the integration of several zero-knowledge proof libraries
- the implementation of common high-level programming language features
Frontend
isekai takes the source code of a computer program and transforms it into a representation suitable for zero-knowledge proof systems. In order to be as independent as possible of programming language, the frontend starts by transforming the source code into an abstract syntax tree (AST) and then transforms it into an intermediate representation that is not dependent on the programming language of the input source code. This transformation is similar to the work done by compilers, and we plan to support the LLVM compiler, which will make adding new languages much easier.
The documentation provides an example of an AST for a simple C program and discusses the internals of the collapser and the frontend parser.
Backend
The backend transforms the internal representation into an arithmetic circuit. An arithmetic circuit is a DAG (directed acyclic graph) whose vertices (gates) are operators, each one having several (0…n) inputs and outputs, represented by the edges of the graph. In theory, an arithmetic circuit is a graph with only addition and multiplication gates. However, we do use additional types of gates so that more programming language features can be supported. In the future, we would like to add more gates to cover even more features. One example would be a division gate that divides two integers. The features currently supported are derived from the gates: addition, multiplication, equality and bit-decomposition. Several gates can be combined to form a feature. For instance, comparing two integers is done by subtracting them and then getting the bit representation of the result and checking the sign bit. Finally, each instruction from the internal representation directly corresponds to some predefined set of gates that we call the Bus.
All of the elements involved in the procedure of generating the circuit are discussed in detail: the Bus, Trace, FieldOp, Wire and Board.
The circuit is generated by the backend as a text file containing the circuit data. The documentation describes the format of arithmetic circuits and the available gates.
Reducer
The arithmetic circuit is then transformed into a system of equations, which is more suitable for zero-knowledge proofs. isekai is currently using an external library for this step, but we plan to use our own implementation. That way, it will be easier to support additional types of gates.
Prover
Proofs (and verifications) can easily be obtained from the equation system discussed in the previous step.
Zero-knowledge proof schemes are an active research area, and there are already many different zero-knowledge proof schemes and implementations in existence, each with their own pros and cons. However, few tools have been developed that are aimed at interfacing with these existing implementations and providing simple interfaces. This is why we at Sikoba Research decided not to work on yet another implementation of ZKP and why we are using external zero-knowledge libraries in order to produce proofs. So far, we support zk-snark thanks to the libsnark library, but we are looking to support other zero-knowledge proof schemes.
