Isekai Verifiable Computation Framework — An Introduction and Call for Partners
Isekai is a verifiable computation framework that will work with several programming languages and verifiable computation systems while using a single code-to-circuit module. Isekai is being developed by Sikoba Research using Crystal, with the support of Fantom Foundation. We seek to cooperate with researchers and developers who work on verifiable computation projects, as well as with blockchain projects that want to offer verifiable computation.
If you are interested to cooperate with us, or to find out more, please contact our CTO, Guillaume Drevon — gd at sikoba dot com.
What is verifiable computation?
Verifiable computation allows one to outsource the processing of some function or program to another computer, the worker, while being able to verify the result without having to redo the computation. As a result, the worker does not need to be trusted. Additionally, the worker may want to convince another verifier without disclosing the data being processed. To solve that problem, zero-knowledge verifiable computation, or ZK-verifiable computation, was introduced, which hides the input from the verifier. This uses zero-knowledge proofs, which is a method of proving to another party the knowledge of some data item without revealing the data item itself. For instance, you could produce the proof that you have the password for a specific account, without revealing your password.
Because the processing overhead of ZK-verifiable computation compared to non-ZK verifiable computation is negligible, research now focuses on the ZK variety. Therefore, the term verifiable computation generally denotes ZK-verifiable computation.
Early implementations of verifiable computation were extremely inefficient, with the verification taking orders of magnitude more time than the computation itself would have taken, had it not been outsourced. The main goal of current research is making verifiable computation practical by reducing verification time.
(In the future, the use of homomorphic encryption will make it possible to hide the data being processed even from the worker, which will allow for secure verifiable computation. However, that technology is still very far from being production-ready.)
Why Isekai?
There are already several verifiable computation libraries being developed, with different properties and unique capabilities, as described for example in the State of the Art in Verifiable Computation paper by Dmitry Khovratovich available on the Sikoba Research website. New implementations are also under development, but without any common standards in place benchmarking is near impossible and deciding which verifiable computation system to use is difficult.
This is where isekai comes in. Our intent is to provide a framework that will allow people to freely choose the programming language and verifiable computation system they want, allowing them to test multiple options without having to make difficult choices at the beginning of a project.
Many verifiable computation systems work by transforming a program into a system of constraints that are satisfied with the result of the program. The proof system then applies some cryptographic functions to this set of equations. This constraint system is easily derived from an arithmetic circuit representation of a program, which is independent of the programming language of the program itself, as well as of the proof system. We intend to come up with a dedicated generic format for a circuit representation, so that computations in any programming languages can be transformed into our circuit representation. Obviously, we will not support every feature of every programming language, indeed at the beginning we will support only integer calculus. We do, however, intend to add support for more and more features in the future.
From program to circuit
The input program is first converted to an internal representation, which in turn is transformed into a circuit representation. The idea is that when we want to support an additional programming language, only the transformation into the internal representation needs to be done. Since this representation is a direct result of parsing of the code, this step is much easier to do than converting directly to a circuit representation.
You can see these two building blocks in action below.
Currently we support only a limited subset of the C programming language. In the coming months, we will be adding support for other languages. The choice of languages supported will be based on feedback we get from the verifiable computing community.
From circuit to proof libraries
The language circuit and its execution trace will be the input to multiple proof systems, and a user can select the one that suits him well. Each proof system provides a proof of computational integrity for the circuit. The proofs, by default, are non-interactive, meaning that a verifier does not have to interact further with a prover to get convinced about the integrity. However, the proof systems we plan to support are quite different in features, concretely:
- The language circuit must be converted to an arithmetic or boolean circuit of some kind, with very limited set of operations and all variables from the same finite field. The field can be prime or binary.
- Some proof systems require a one-time additional setup for circuits (one or many) that is done by a trusted party.
- Proof size can be constant (big or small) or grow sublinearly of the circuit size.
- Verification time varies from constant to linear of the circuit size.
A typical lifecycle for the proof out of the language circuit is the following:
- The language circuit is converted to an arithmetic circuit.
- If needed, a trusted setup is performed to create a global circuit description (GCD), which is published so that proofs can be verified.
- The program is executed and its trace is recorded.
- The program trace is converted to an arithmetic trace.
- If needed, part of the arithmetic trace is published hidden in the form of cryptographic commitments.
- Proof generator takes the arithmetic trace and GCD and outputs a proof, which is sent to a verifier.
- The verifier checks the proof.
We plan to support the following proof systems:
- zkSNARKs: compact proofs, short verification time, trusted setup. Has the most developed ecosystem with a number of tools (libsnark, bellman) and compilers (tinyRAM, Zokrates) available. Used in Zcash.
- Bulletproofs: medium proofs, long verification time, no trusted setup. Used in Monero.
- zkSTARKs: medium proofs, short verification time, no trusted setup. Does not have a production-ready implementation. Not used yet.
- ZKBoo++: medium proofs, medium verification time, no trusted setup. Does not have a production-ready implementation. Not used yet.
All these proof systems can work with GCDs made of rank-1 constraints (R1CS), which are quadratic polynomials of a certain form.
Isekai project status
The code converting from C to the internal representation was completed in December/January and we just finished the conversion to circuit representation. A first version of the documentation is also done, so an important milestone has been reached.
The next steps, to be completed before the end of March, are:
- Isekai team meeting in Luxembourg on 16 and 17 February
- finalise documentation
- comprehensive testing and code review before a first official release
- research how additionnal languages can be supported (under way)
- convert arithmetic circuit to R1CS (some tests already done)
- integrate and test with a zkSNARK library
After that, possible topics will be:
- Support other languages, e.g. Python, Michelson…
- developing our own domain-specific language
- develop programming best-practices for efficiently verifiable code.
- circuit format specifications
- Add more features , e.g. function calls
- (we’re open to suggestions)
…
