All Projects → adjoint-io → Arithmetic Circuits

adjoint-io / Arithmetic Circuits

Licence: mit
Arithmetic circuits for zero knowledge proof systems

Programming Languages

haskell
3896 projects

Labels

Projects that are alternatives of or similar to Arithmetic Circuits

Smallerc
Simple C compiler
Stars: ✭ 986 (+1796.15%)
Mutual labels:  compiler
Bytenode
A minimalist bytecode compiler for Node.js
Stars: ✭ 1,012 (+1846.15%)
Mutual labels:  compiler
Patchouli Compiler
An Oberon-07 compiler for Intel 64 (AMD64) architecture
Stars: ✭ 46 (-11.54%)
Mutual labels:  compiler
Llvm Tutorial Standalone
DEPRECATED (Use: https://github.com/llvm-hs/llvm-hs-kaleidoscope )
Stars: ✭ 38 (-26.92%)
Mutual labels:  compiler
Mlml
self-hosted compiler for a subset of OCaml
Stars: ✭ 41 (-21.15%)
Mutual labels:  compiler
Jsx Lite
Write components once, run everywhere. Compiles to Vue, React, Solid, Angular, Svelte, and Liquid.
Stars: ✭ 1,015 (+1851.92%)
Mutual labels:  compiler
Compcert
The CompCert formally-verified C compiler
Stars: ✭ 984 (+1792.31%)
Mutual labels:  compiler
Cymbal
Yet another Rust implementation of the Monkey language from "Writing an Interpreter in Go" and "Writing a Compiler in Go"
Stars: ✭ 49 (-5.77%)
Mutual labels:  compiler
Antlr4 Calculator
Simple antlr4 calculator.
Stars: ✭ 40 (-23.08%)
Mutual labels:  compiler
Leekscript V2
A dynamically typed, compiled just-in-time programming language used in Leek Wars' AIs
Stars: ✭ 46 (-11.54%)
Mutual labels:  compiler
The Hack General Purpose Computer
Using HDL, from Boolean algebra and elementary logic gates to building a Central Processing Unit, a memory system, and a hardware platform, leading up to a 16-bit general-purpose computer. Then, implementing the modern software hierarchy designed to enable the translation and execution of object-based, high-level languages on a bare-bone computer hardware platform; Including Virtual machine,Compiler and Operating system.
Stars: ✭ 39 (-25%)
Mutual labels:  compiler
Nativejit
A C++ expression -> x64 JIT
Stars: ✭ 999 (+1821.15%)
Mutual labels:  compiler
Intrinsics Dude
Opensource Visual Studio extension for compiler instrinsics in C/C++
Stars: ✭ 44 (-15.38%)
Mutual labels:  compiler
Rascal
A simple Pascal interpreter written in rust.
Stars: ✭ 38 (-26.92%)
Mutual labels:  compiler
Min
Min: Crypto Token for Beautiful and Secure Code
Stars: ✭ 48 (-7.69%)
Mutual labels:  compiler
Mini Haskell
A self-hosting mini Haskell compiler with a mini C runtime.
Stars: ✭ 37 (-28.85%)
Mutual labels:  compiler
Shaderc
A collection of tools, libraries, and tests for Vulkan shader compilation.
Stars: ✭ 1,016 (+1853.85%)
Mutual labels:  compiler
Typhon
A virtual machine for Monte.
Stars: ✭ 49 (-5.77%)
Mutual labels:  compiler
Trck
Query engine for TrailDB
Stars: ✭ 48 (-7.69%)
Mutual labels:  compiler
U6a
Implementation of Unlambda, an esoteric programming language.
Stars: ✭ 46 (-11.54%)
Mutual labels:  compiler

Adjoint Logo

CircleCI

Arithmetic Circuits

An arithmetic circuit is a low-level representation of a program that consists of gates computing arithmetic operations of addition and multiplication, with wires connecting the gates.

This form allows us to express arbitrarily complex programs with a set of private inputs and public inputs whose execution can be publicly verified without revealing the private inputs. This construction relies on recent advances in zero-knowledge proving systems:

This library presents a low-level interface for building zkSNARK proving systems from higher-level compilers. This system depends on the following cryptographic dependenices.

Theory

Towers of Finite Fields

This library can build proof systems polymorphically over a variety of pairing friendly curves. By default we use the BN254 with an efficient implementation of the optimal Ate pairing.

The Barreto-Naehrig (BN) family of curves achieve high security and efficiency with pairings due to an optimum embedding degree and high 2-adicity. We have implemented the optimal Ate pairing over the BN254 curve we define and as:

The tower of finite fields we work with is defined as:

Arithmetic circuits

Arithmetic Circuit

An arithmetic circuit over a finite field is a directed acyclic graph with gates as vertices and wires and edges. It consists of a list of multiplication gates together with a set of linear consistency equations relating the inputs and outputs of the gates.

Let be a finite field and a map that takes arguments as inputs from and outputs l elements in . The function C is an arithmetic circuit if the value of the inputs that pass through wires to gates are only manipulated according to arithmetic operations + or x (allowing constant gates).

Let , , respectively denote the input, witness and output size and be the number of all inputs and outputs of the circuit A tuple , is said to be a valid assignment for an arithmetic circuit C if .

Quadratic Arithmetic Programs (QAP)

QAPs are encodings of arithmetic circuits that allow the prover to construct a proof of knowledge of a valid assignment for a given circuit .

A quadratic arithmetic program (QAP) contains three sets of polynomials in :

, ,

and a target polynomial .

In this setting, an assignment is valid for a circuit if and only if the target polynomial divides the polynomial:

Logical circuits can be written in terms of the addition, multiplication and negation operations.

DSL and Circuit Builder Monad

Any arithmetic circuit can be built using a domain specific language to construct circuits that lives inside Lang.hs.

type ExprM f a = State (ArithCircuit f, Int) a
execCircuitBuilder :: ExprM f a -> ArithCircuit f
-- | Binary arithmetic operations
add, sub, mul :: Expr Wire f f -> Expr Wire f f -> Expr Wire f f
-- | Binary logic operations
-- Have to use underscore or similar to avoid shadowing @[email protected] and @[email protected]
-- from Prelude/Protolude.
and_, or_, xor_ :: Expr Wire f Bool -> Expr Wire f Bool -> Expr Wire f Bool
-- | Negate expression
not_ :: Expr Wire f Bool -> Expr Wire f Bool
-- | Compare two expressions
eq :: Expr Wire f f -> Expr Wire f f -> Expr Wire f Bool
-- | Convert wire to expression
deref :: Wire -> Expr Wire f f
-- | Return compilation of expression into an intermediate wire
e :: Num f => Expr Wire f f -> ExprM f Wire
-- | Conditional statement on expressions
cond :: Expr Wire f Bool -> Expr Wire f ty -> Expr Wire f ty -> Expr Wire f ty
-- | Return compilation of expression into an output wire
ret :: Num f => Expr Wire f f -> ExprM f Wire

The following program represents the image of the arithmetic circuit above.

program :: ArithCircuit Fr
program = execCircuitBuilder (do
  i0 <- fmap deref input
  i1 <- fmap deref input
  i2 <- fmap deref input
  let r0 = mul i0 i1
      r1 = mul r0 (add i0 i2)
  ret r1)

The output of an arithmetic circuit can be converted to a DOT graph and save it as SVG.

dotOutput :: Text
dotOutput = arithCircuitToDot (execCircuitBuilder program)

Example

We'll keep taking the program constructed with our DSL as example and will use the library pairing that provides a field of points of the BN254 curve and precomputes primitive roots of unity for binary powers that divide .

import Protolude

import qualified Data.Map as Map
import Data.Pairing.BN254 (Fr, getRootOfUnity)

import Circuit.Arithmetic
import Circuit.Expr
import Circuit.Lang
import Fresh (evalFresh, fresh)
import QAP

program :: ArithCircuit Fr
program = execCircuitBuilder (do
  i0 <- fmap deref input
  i1 <- fmap deref input
  i2 <- fmap deref input
  let r0 = mul i0 i1
      r1 = mul r0 (add i0 i2)
  ret r1)

We need to generate the roots of the circuit to construct polynomials and that satisfy the divisibility property and encode the circuit to a QAP to allow the prover to construct a proof of a valid assignment.

We also need to give values to the three input wires to this arithmetic circuit.

roots :: [[Fr]]
roots = evalFresh (generateRoots (fmap (fromIntegral . (+ 1)) fresh) program)

qap :: QAP Fr
qap = arithCircuitToQAPFFT getRootOfUnity roots program

inputs :: Map.Map Int Fr
inputs = Map.fromList [(0, 7), (1, 5), (2, 4)]

A prover can now generate a valid assignment.

assignment :: QapSet Fr
assignment = generateAssignment program inputs

The verifier can check the divisibility property of by for the given circuit.

main :: IO ()
main = do
  if verifyAssignment qap assignment
    then putText "Valid assignment"
    else putText "Invalid assignment"

See Example.hs.

Disclaimer

This is experimental code meant for research-grade projects only. Please do not use this code in production until it has matured significantly.

License

Copyright (c) 2017-2020 Adjoint Inc.

Permission is hereby granted, free of charge, to any person obtaining a copy
of this software and associated documentation files (the "Software"), to deal
in the Software without restriction, including without limitation the rights
to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
copies of the Software, and to permit persons to whom the Software is
furnished to do so, subject to the following conditions:

The above copyright notice and this permission notice shall be included in all
copies or substantial portions of the Software.

THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF
MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT.
IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM,
DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR
OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE
OR OTHER DEALINGS IN THE SOFTWARE.
Note that the project description data, including the texts, logos, images, and/or trademarks, for each open source project belongs to its rightful owner. If you wish to add or remove any projects, please contact us at [email protected].