isekai 1.0 is now live!

We are proud to announce the release of isekai 1.0. In a nutshell:

isekai is the only tool to support 3 ZKP libraries and 5 proof systems: libsnark (Groth16 and BCTV14a), dalek (Bulletproofs) and libiop (Aurora and Ligero).

isekai is the first tool allowing programmers to take existing C or C++ code and generally require only slight modifications to make it compatible with isekai — we did it for sha256 as described in this post. This is because isekai supports more features of regular programming languages than any other project we know of, without using a domain specific language.

The isekai project can be found at https://github.com/sikoba/isekai

When we stated our ambitious goal to build a middleware that would help leverage zero-knowledge proofs by providing an interface to several proof systems and support standard high level programming languages, we knew the path would not be easy. In fact, six months ago I would probably not have bet that isekai 1.0 would be released before the end of 2019. So we’re obviously really happy about the progress we have made this year.

Let me take this opportunity to thank the Fantom Foundation for their continuing financial support —isekai development would not have been possible without Fantom. I’d like to also thank everybody who helped us on this project, in particular our cryptography advisor Dmitry Khovratovich and the Serotonin Syndrome team who did a fantastic job on the LLVM front-end.

Of course the journey is not over yet and there are still many points we would like to improve on. But for now, let’s review what we have achieved.

High-level programming language support

As you may know already, isekai is taking source code and input data, and it generates a zero-knowledge proof of execution of the computation described in the source code. Because we want to work with many programming languages, isekai is working with LLVM IR as input. In practice it means that you can take a C or C++ source code and compile it into LLVM bitcode using Clang for instance. This compilation step provides several benefits, such as C and C++ support, basic compiler optimisations and full pre-processor support. Regarding the compiler optimisations, we recommend to not go over level 2, level 0 being safer. This is because we do not support the entire LLVM instruction set (in particular we do not support floating point operations) and also because binary optimisations are not ZKP friendly.

isekai supports arrays, pointers, loops, function calls, integer operations (+,-,*,and.or,xor,left/right shift,<,>,==,..) and (partial) control flow. We don’t know of any other project being able to cover so many features of regular programming languages, i.e not using a dedicated domain specific language.

Of course, we have some limitations and we hope to implement these missing feature in the future, although there are already workarounds for many of them. Here are some of the current limitations:

• Function calls must be in-lined, meaning we cannot do recursion
• We do not support dynamic arrays (int a[n];) or dynamic allocations (malloc)
• Pointers cannot be created from a constant (int *p = 1453326; is it a feature? :)
• We cannot mix several source files together (all the code must be in the same source file)
• Global and static variables are not supported (one should use #define whenever possible instead)
• Floating points types and operations are no supported — but who needs these anyway? :-)
• The entry point for C++ source code must have extern “C” name mangling, this point currently prevents the usage other languages through LLVM (e.g. Rust)
• / and % operations, except if used with constant values

Choose your ZK proof scheme

Once you provide isekai with your program as LLVM bitcode, plus the input data of your program, isekai will generate a constraints system representing the execution of the program, which you can feed to the proof system of your choice.

We have integrated 5 proof systems, from 3 zkp libraries: libsnark (Groth16 and BCTV14a), dalek (Bulletproofs) and libiop (Aurora and Ligero). We believe isekai is the most versatile ZKP tool in terms of the number of supported proof systems.

Usage

Please refer to the isekai github for more detailed information. Installation should be straightforward although you might need to re-compile one library. isekai works on linux and has been tested successfully on Ubuntu 18.04. isekai also works fine with on the Ubuntu 18.04 Windows subsystem.

isekai is simple to use; just provide the LLVM bitcode and the input data and then isekai will generate the constraints system for you. You must specify which ZKP scheme you want to use though the ‘--scheme’ option. The possible values are: bctv14, groth16, dalek (for bulletproofs), ligero and aurora. From the constraints system (and its assignment, generated at the same time), isekai is then able to generate a proof. Of course, isekai can also verify a proof it has generated.

Here is for example a proof generation using Dalek (note that isekai also verifies the proof right after generating it):