HLL

High-Level languages for zkSNARKs, Fully-Homomorphic-Encryption and Multi-Party-Computation

zkSNARKs

High-Level Languages for zkSNARKs

Forms

QAP

Proving Systems

Technologies

Hyrax

Hyrax is a doubly-efficient (meaning, for both the prover and the verifier) zkSNARK which requires no trusted setup.

The source-code is available at: https://github.com/hyraxZK/hyraxZK

Hyrax uses Prover Worksheet as an intermediate form.

zkSNARKs

Bulletproofs

https://eprint.iacr.org/2017/1066.pdf

https://crypto.stanford.edu/bulletproofs/

Bulletproofs are short non-interactive zero-knowledge proofs that require no trusted setup. A bulletproof can be used to convince a verifier that an encrypted plaintext is well formed. For example, prove that an encrypted number is in a given range, without revealing anything else about the number. Compared to SNARKs, Bulletproofs require no trusted setup. However, verifying a bulletproof is more time consuming than verifying a SNARK proof.

Implemented in the following libraries:

Proving Systems

SONIC

https://github.com/zknuckles/sonic

Gro16

https://eprint.iacr.org/2016/260.pdf

GGPR13

GM17

Libraries

adjoint-io/bulletproofs

A Haskell library from Adjoint.io which implements range proofs, inner product range proofs, aggregate logarithmic proofs and subsequently arithmetic circuits using Bulletproofs.

dalek-cryptography

A pure-Rust implementation of Bulletproofs using Ristretto.

The fastest Bulletproofs implementation ever, featuring single and aggregated range proofs, strongly-typed multiparty computation, and a programmable constraint system API for proving arbitrary statements (under development).

This library implements Bulletproofs using Ristretto, using the ristretto255 implementation in [curve25519-dalek](https://doc.dalek.rs/curve25519_dalek/index.html). When using the parallel formulas in the curve25519-dalek AVX2 backend, it can verify 64-bit rangeproofs approximately twice as fast as the original libsecp256k1-based Bulletproofs implementation.

Compilers

CBMC-GC-2

CBMC-GC is a compiler for C programs in the context of secure two-party computation (STC). It compiles a C program that specifies a secure computation into a circuit which can be read in by an STC platform, which then performs the secure computation between two parties A and B:

Toolchain Overview

Languages

C

Compiled By:

SFDL

The ‘Secure Function Definition Language’ was defined by the FairPlay MPC project, it is compiled into the intermediate-form ‘SHDL’ - the ‘Secure Hardware Definition Language’ - where statements are decomposed into single-static-assignment circuit form operating on individual bits. The FairPlay compiler is not only well suited for MPC, but ebcause it compiles down to operations on individual bits it’s also well suited for general garbled circuits and fully-homomorphic-encryption.

Examples

program And {
	type Byte = Int<8>;
	type AliceInput = Byte;
	type BobInput = Byte;
	type AliceOutput = Byte; 
	type BobOutput = Byte; 
	type Input = struct {AliceInput alice,	BobInput bob};
	type Output = struct {AliceOutput alice, BobOutput bob};

	function Output output(Input input) {
           output.alice = (input.bob & input.alice);
           output.bob = (input.bob & input.alice);
	}
}

Circom

Verilog

Compiled By

The circuit_synthesis repository by TinyGarble includes a toolchain for compiling Verilog to netlist form supported by TinyGarble. This repository includes many examples.

Converted To

SCDL

Simple Circuit Description Language - simple functional language to describe circuits with a very basic implementation of a “compiler”.

Using single-line expressions in a somewhat functional style this semi-high-level language bridges the gap between high-level and low-level.

Example:

include "base.scdl"
  
input A : 2
input B : 2

func gt(X : 2, Y : 2) = \
  or(X[1]*not(Y[1]), eq(X[1], Y[1])*X[0]*not(Y[0]))

func out = gt(A, B)

Intermediate Formats

Intermediate forms are simplified low-level representations which require little to no complex parsing.

Pinocchio

https://github.com/Ethsnarks/ethsnarks-il/tree/master/cxx

Prover Worksheet

SHDL

andytoshi

SCD

An SCD file contains a compact description of a boolean circuit or a boolean circuit topology (a description with gate types are unspecified). Circuits are modeled closely after Foundations of garbled circuits by Bellare, Hoang and Roagaway, available from eprint.iacr.org. Here a circuit is a 6-tuple f = (n, m, q, A, B, G, O) where n, m, and q are integers representing the number of inputs, outputs, and gates in the circuit.

Consider a simple circuit implementing f(a_1,a_2,a_3) = (a_1 & a_2) | a_3. There are three inputs, one output, two gates, and five logical wires. We will add the extra dummy wire to make it six wires overall. An SCD representation of this circuit could be as follows: (3, 1, 2, [1,4], [2,3], [8, 14], [5]), indicating that there are 3 inputs, 1 output and 2 gates, the first inputs to the gates are 1 and 4, the second inputs are 2 and 3, the gate types are 8 = 1000 = AND, and 14 = 1110 = OR, and the output of the circuit is wire 5.

Bristol

This file format is suited for the representation of sequential binary circuits, where each wire represents a single bit.

To understand the format, each file consists of:

So for example:

2 1 3 4 5 XOR

corresponds to:

w5 = XOR(w3, w4)

Examples:

Converts to