Isekai is a verifiable computation framework that allows to work with several programming languages and verifiable computation systems while using a single code-to-circuit module. Our aim is to make zero-knowledge proofs accessible to mainstream programmers. Specifically:
-
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. This is because isekai supports more features of regular programming languages than any other project we know of, without using a domain specific language.
Isekai is being developed by Sikoba Research 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.
To find out more, please consult the isekai Medium posts or contact us at isekai at protonmail dot com. There is also a (slightly outdated) isekai Technical documentation from July 2019.
The initial development of isekai until version 1.0 has been made possible by the support of Fantom Foundation. We are now looking for new sponsors and partners for the months ahead. Our goal is to make isekai a community project and to keep it free and open source.
Here is our tentative "to do" list for the coming months.
Additional language features:
Integer division and modulo✅ DONE (13-DEC-19)!Array look-up and dynamic storage optimisations✅ DONE (13-DEC-19)!Native field operations for efficient cryptgraphic primitives implementation✅ DONE (20-DEC-19)!- Floating point operations
LLVM support improvements:
- full function call
- new LLVM instructions: bitcast, memcpy, memset
- global/static variables
Support for additional ZKP systems :
- Fractal
- Plonk
- Marlin
- Starks
LLVM Frontends :
- C/C++ (i.e integrating Clang into isekai)
- Rust
- Crystal
More long-term goals:
- WebAssembly frontend
- TinyRAM
- add FHE library
- add MPC library
- python, java frontends
- Domain-specific functions
Isekai is a tool for zero-knowledge applications. It currently parses a C/C++ program and outputs the arithmetic and/or boolean circuit representing the expression equivalent to the input program. Support for more languages will be added in the future. isekai uses libclang to parse the C program, so most of the preprocessor (including the includes) is available. Then isekai generates an arithmetic representation and converts it to a rank-1 constraints system. Isekai can prove and verify the program execution using several ZKP libraries (libsnak, bulletproof and libiop). isekai is written using crystal programming language allowing for a strong type safety and it is compiled to a native executable, ensuring maximum efficiency in parsing.
This version is fullfilling our goals for a tool integrating several standard programming languages with several ZKP schemes.
isekai now supports LLVM bitcode! This means in theory that you can compile any language to work with isekai as long as you have an LLVM frontend for it. In practise we have successfully tested C and C++ through LLVM. With the support of LLVM comes many improvements; pointers, arrays, function call and many other C features are supported, and of course, also C++. Another feature we are proud to deliver is the support of Bulletproof zero-knowledge scheme. One major advantage of this scheme is that proofs do not need a trusted setup. This does not come for free unfortunately as it has impact on performances. Nevertheless, with isekai you can now easily compare with zk-snarks by simply changing the scheme! We believe isekai is the first project that can handle multiple languages and multiple zero-knowledge proof systems.
isekai can be easily tested on Windows using Ubuntu for windows. This Medium post indicates how to do it.
Start by cloning isekai to a local directory. We recommend to retrieve also the the submodules:
$ git clone --recurse-submodules https://github.com/sikoba/isekai.git
The project is written in Crystal language. Follow the Official instructions for instructions how to install Crystal lang.
Make sure to install the recommended packages, even though only libgmp-dev is actually required for isekai.
Then install the following additional packages required by isekai:
$ sudo apt install clang-7
$ sudo apt install libclang-7-dev
$ sudo apt-get install libprocps-dev
$ shards install
The project depends on several libclang patches which are not yet merged in the libclang (https://www.mail-archive.com/cfe-commits@cs.uiuc.edu/msg95414.html, http://lists.llvm.org/pipermail/cfe-commits/Week-of-Mon-20140428/104048.html)
Applying the patch is done from the docker subdirectory:
$ cd docker/
$ cp bin/libclang.so.gz /tmp/libclang.so.gz
$ gzip -d /tmp/libclang.so.gz
$ sudo cp /tmp/libclang.so /usr/lib/x86_64-linux-gnu/libclang-7.so.1
$ sudo cp /tmp/libclang.so /usr/lib/libclang.so.7
$ cd ..
The project comes with the Makefile and in order to compile the project, running make will be enough. That will create the isekai binary file in the current directory. To run tests make test should be used.
Alternatively, crystal build src/isekai.cr or crystal test can be used.
$ make
$ make test
The result of make test should end with something resembling this:
...
Finished in 800.85 milliseconds
9 examples, 0 failures, 0 errors, 0 pending
libsnarc is a library which provides a C-wrapper over libsnark and libiop. The library is already included so you do not need to compile it. However, we have noticed errors on some systems, which are fixed by recompiling the library. Please make sure you retrieved the submodules recursively before compiling this library.
$ sudo apt-get install libsodium-dev
$ cd lib/libsnarc
$ mkdir build
$ cd build & cmake ..
$ make
After having built libsnarc, you need to (re-)build isekai :
go to isekai main directory
$ make --always-make
(Also check the "Some tests with isekai" section of the above-mentioned Medium post)
Isekai can generate a proof of the execution of a C function. The C function must have one of the following signature:
void outsource(struct Input *input, struct NzikInput * nzik, struct Output *output);
void outsource(struct Input *input, struct Output *output);
void outsource(struct NzikInput * nzik, struct Output *output);
Input and Output are public parameters and NzikInput are the private parameters (zero-knowledge). Inputs and NzikInputs can be provided in an additional file, by putting each value one per line. This input file must have the same name as the C program file, with an additional ‘.in’ extension. For instance, if the function is implemented in my_C_prog.c, the inputs must be provided in my_C_prog.c.in
Basically, you first generates the constraints system with --r1cs option, then with this r1cs you can create a proof using --prove option, and finally verify the proof using the --verif option. The ZKP scheme to use can be specified with the --scheme option.
In order to use LLVM with isekai, you simply provide the LLVM bitcode file instead of the C source code. Please note that LLVM is now the recommended way to use with isekai. The C frontend of isekai will not be maintained but will be probably replaced using the LLVM one. For instance, use the following commands to use LLVM frontend with C source code:
clang -DISEKAI_C_PARSER=0 -O0 -c -emit-llvm my_C_prog.c
./isekai --r1cs=output_file.j1 my_C_prog.bc
The inputs should have the .in extension as explained above. In this example it means you should have also the file my_C_prog.bc.in next to my_C_prog.bc Isekai also generate the assignments in the file output_file.j1.in. It adds ‘.in’ to the filename provided in the r1cs option to get a file for the assignments. Note that existing files are overwritten by isekai. Isekai automatically uses the inputs provided in my_C_prog.bc.in if it exists. If not, isekai assumes all the inputs are 0.
To generate (and verify) a proof with libsnark:
./isekai --prove=my_snark output_file.j1
If the verification pass, this command will generate json files of the proof (my_snark.p) and trusted setup (my_snark.s). Of course in real life, you should not generate a proof and the trusted setup at the same time!
A verifier can verify the proof with the following command:
./isekai --verif=my_snark output_file.j1.in
A verifier should not know the private inputs (NzikInput) so you should remove the ‘witnesses’ part from the input file before giving it to the verifier. Two different ZKP schemes from libsnark are supported and can be specified with the --scheme option, refer to the ZKP scheme section below for more information. If the scheme option is not set, it will use libsnark by default.
In order to use Bulletproof instead of libsnark, you need to specify the dalek scheme;
./isekai --scheme=dalek --r1cs=output_file.j1 my_C_prog.bc
./isekai --scheme=dalek --prove=my_proof output_file.j1
./isekai --verif=my_proof output_file.j1
As you can see, the verification requires (for now) the .j1 file (and also the public inputs), contrary to libsnark. Please note that although very similar, the r1cs generated for libsnark and bulletproof are not compatible, this is why you need to specify the scheme when generating it.
isekai is the most versatile ZKP project that we know of, regarding high-level programming languages supported features:
- full C/C++ pre-processing support
- include files (header files)
- Integer operations:
- Arithmetic: + , - , * , / , %
- Binary: and, or, not, xor, left/right shift
- Comparisons: < , > , <=, >=, ==, !=
- Control flow graphs from C99 code, without goto, break, continue and return statements
- Inline function calls
- Loops with constant (or provided maximum) iterations
- Arrays
- Pointers
However there are still some limitations:
- Function calls must be in-lined
- No support for dynamic pointers, as well as:
- Dynamic arrays
- Dynamic allocations
- Pointers created from a constant
- Source code must be in one file (except for include files)
- Global/static variables are not supported
- No floating point types
- Entry point must have C name mangling
With isekai 1.0 we now support more ZKP schemes, the --scheme option can be used with the following values.
| Scheme option | Type |
|---|---|
| bctv14a | zk-snark |
| groth16 | zk-snark |
| dalek | bulletproof |
| ligero | iop |
| aurora | iop |