bellpepper

A Rust library for expressing verifiable computation

Saravanan Vijayakumaran

Department of Electrical Engineering, IIT Bombay

February 4, 2024

bellpepper

A Rust library for expressing verifiable computation
Maintained by Lurk Lab
- https://github.com/lurk-lab/bellpepper
A fork of the bellperson library, which is itself a fork of the seminal bellman library
Verifiable computation = Computations which can be proved to give a certain output for a given input

Verifiable Computation

A prover wants to prove that a program F when run with input x gives an output y, i.e. y = F(x)
A verifier knows the program F and the IO values x,y
In some scenarios, the verifier cannot run the program F
- Due to resource constraints or insufficient info
- Example: Prover is a cloud provider and verifier is a user
The prover generates a proof \pi that y = F(x)
The proof \pi is easier to verify than re-running F

SNARKs

SNARK = Succinct Non-interactive Arguments of Knowledge
- Protocols that enable verifiable computation
- Succinct = Proofs are smaller than size of statement
- Non-interactive = A single message from prover to verifier
- Argument = Soundness only guaranteed for PPT provers
- Knowledge = Prover knows a witness (secret information)
zkSNARK = Zero-Knowledge SNARK

Arithmetic Circuits

To prove statements using SNARKs, they have to be expressed as arithmetic circuits
- Circuit variables are prime field elements
- Only addition and multiplication are allowed
Prime fields
- \mathbb{F}_p = \{0,1,\ldots,p-1\} where p is a prime
- Arithmetic modulo p
R1CS is one method for arithmetizing statements

Rank-1 Constraint Systems

Statement is represented using quadratic constraints \begin{align*} \left(a_0 + \sum_{i=1}^n a_i z_i \right) \cdot \left(b_0 + \sum_{i=1}^n b_i z_i \right) \\ = \left( c_0 + \sum_{i=1}^n c_i z_i\right) \end{align*}
The a_i, b_i, c_i values are determined by the statement
The z_i’s are values specific to the instance

Why Rank 1?

The LHS of a quadratic constraint can be written as \begin{align*} & \left(a_0 + \sum_{i=1}^n a_i z_i \right) \cdot \left(b_0 + \sum_{i=1}^n b_i z_i\right) \\ = & \langle \textbf{a}, (1,\textbf{z}) \rangle \cdot \langle \textbf{b}, (1,\textbf{z}) \rangle \\ = & \begin{bmatrix} 1 & \textbf{z} \end{bmatrix} \underbrace{\begin{bmatrix} a_0 \\ a_1 \\ \vdots \\ a_n \end{bmatrix} \begin{bmatrix} b_0 & b_1 & \cdots & b_n \end{bmatrix}}_{M} \begin{bmatrix} 1 \\ \textbf{z}^T \end{bmatrix} \end{align*}
The matrix M has rank one

SHA-256

Cryptographic Hash Functions

Methods for deterministically mapping a long input string to a shorter output called a digest
Primary requirement is that it should be infeasible to find collisions, i.e. two distinct inputs having same digest
A collision is said to occur if h(x) = h(x') for x \neq x'
Cryptographic hash functions avoid collisions by defining a large co-domain

Co-Domain for 256-bit Output Length

SHA-256

SHA = Secure Hash Algorithm, 256-bit output length
Accepts bit strings of length upto 2^{64}-1
Announced in 2001 by NIST

Two Stages

Output calculation has two stages
- Preprocessing
- Hash Computation

Preprocessing

The input M is padded to a multiple of 512 bits
A 256-bit state variable H^{(0)} is set to \begin{align*} \begin{split} H_0^{(0)} = \texttt{0x6A09E667},& \quad H_1^{(0)} = \texttt{0xBB67AE85},\\ H_2^{(0)} = \texttt{0x3C6EF372},& \quad H_3^{(0)} = \texttt{0xA54FF53A},\\ H_4^{(0)} = \texttt{0x510E527F},& \quad H_5^{(0)} = \texttt{0x9B05688C},\\ H_6^{(0)} = \texttt{0x1F83D9AB},& \quad H_7^{(0)} = \texttt{0x5BE0CD19}. \end{split} \end{align*}
Derived from the square roots of the first eight primes
NUMS = Nothing Up My Sleeve

Hash Computation

A function f: \{0,1\}^{512} \times \{0,1\}^{256} \rightarrow \{0,1\}^{256} is used. It is called the compression function
Padded input is split into N 512-bit blocks M^{(1)}, M^{(2)}, \ldots, M^{(N)}
Given H^{(i-1)}, the next H^{(i)} is calculated as \begin{equation*} H^{(i)} = f(M^{(i)}, H^{(i-1)}), \quad 1 \le i \le N. \end{equation*}
H^{(N)} is the output of SHA-256 for input M

Building Blocks of f

U, V, W are 32-bit words
U \land V, U \lor V, U \oplus V denote bitwise AND, OR, XOR
U + V denotes integer sum modulo 2^{32}
\lnot U denotes bitwise complement
For 1 \le n \le 32, the shift right and rotate right operations \begin{align*} \textsf{SHR}^n(U) & = \underbrace{000 \cdots 000}_{n \textrm{ zeros}} u_0 u_1 \cdots u_{30-n} u_{31-n}, \\ \textsf{ROTR}^n(U) & = u_{31-n+1} u_{31-n+2} \cdots u_{30} u_{31} u_0 u_1 \cdots u_{30-n} u_{31-n}, \end{align*}

Building Blocks of f

Bitwise choice and majority functions \begin{align*} \textsf{Ch}(U,V,W) & = (U \land V) \oplus (\lnot U \land W), \\ \textsf{Maj}(U,V,W) & = (U \land V) \oplus (U \land W) \oplus (V \land W), \end{align*}
Let \begin{align*} \Sigma_0(U) & = \textsf{ROTR}^{2}(U) \oplus \textsf{ROTR}^{13}(U) \oplus \textsf{ROTR}^{22}(U) \\ \Sigma_1(U) & = \textsf{ROTR}^{6}(U) \oplus \textsf{ROTR}^{11}(U) \oplus \textsf{ROTR}^{25}(U) \\ \sigma_0(U) & = \textsf{ROTR}^{7}(U) \oplus \textsf{ROTR}^{18}(U) \oplus \textsf{SHR}^{3}(U) \\ \sigma_1(U) & = \textsf{ROTR}^{17}(U) \oplus \textsf{ROTR}^{19}(U) \oplus \textsf{SHR}^{10}(U) \end{align*}

f Calculation

Maintains internal state of 64 words \{W_j \mid j = 0,1,\ldots,63\}
Uses 64 constant words K_0, K_1, \ldots, K_{63} derived from the first 64 primes
f(M^{(i)}, H^{(i-1)}) proceeds as follows
1. Internal state initialization \begin{equation*} W_j = \begin{cases} M_j^{(i)} & 0 \le j \le 15, \\ \sigma_1(W_{j-2}) + W_{j-7} + \sigma_0(W_{j-15}) + W_{j-16} & 16 \le j \le 63. \end{cases} \end{equation*}
2. Initialize eight 32-bit words \begin{equation*} (A,B,C,D,E,F,G,H) = \left(H_0^{(i-1)}, H_1^{(i-1)}, \ldots, H_6^{(i-1)}, H_7^{(i-1)}\right). \end{equation*}
3. For j = 0,1,\ldots,63, iteratively update A,B,\ldots,H \begin{align*} \begin{split} & T_1 = H + \Sigma_1(E) + \textsf{Ch}(E,F,G) + K_j + W_j \\ & T_2 = \Sigma_0(A) + \textsf{Maj}(A,B,C) \\ & (A,B,C,D,E,F,G,H) = (T_1+T_2, A, B, C, D+T_1, E, F, G) \end{split} \end{align*}
4. Calculate H^{(i)} from H^{(i-1)} \begin{equation*} (H_0^{(i)}, H_1^{(i)}, \ldots, H_7^{(i)}) = \left(A+H_0^{(i-1)}, B+H_1^{(i-1)}, \ldots, H+H_7^{(i-1)}\right). \end{equation*}
Demo: https://sha256algorithm.com/

Sample SHA256 Output

Input                       Output

dec0   0525bd43e7ba2917ebb5ff4893961fa6e6a3b5ccadbffd9bc520882168945a71
dec1   0740174f35ff7cb50b8417bdc50be191f8c5e5daaf4c4bdb8498b1fe3aa41d0d
dec2   dabc08efd0d2ae280fc0177c978ab7c82542cc67d3acafb62cbd913b5b73cf72
dec3   a2b2c10ec26b94298e07e0273c319686721d6c7f285756fb4400b2bb9014ff4c
dec4   5076f2f9de8dbc00ebc6c72b3d207cd7b985b91f634026fd746fe07dc19993c3
dec5   884466e61bd01d5282386b758313b44a424b6d9d890255770393f267664c64f9
dec6   f37095c5192a84934ba69db9de48ad52051321fe64efc5bd95074eaaa66d08a4
dec7   aed0913ad1fedc68e621b23c895f5c2aa24db2cce1cb82ef123a92351ef081c3
dec8   8bac240a6fccbf8ead9a913d9e65f8394728e2cfeb36f745d1f0142f6e7fd0b6
dec9   99e9d59894056331a3ebe12870d9eb7b245a11707334a97dfad58de16eac977e

Observations

SHA-256 is complicated but can be computed easily
Difficult to invert
Difficult to find collisions

R1CS for SHA-256

Proving Knowledge of Preimage

Suppose we wanted to prove that we know the preimage of a SHA256 hash
Given a public y \in \{0,1\}^{256}, we claim to know x such that y = \text{SHA256}(x)
How can this statement be represented in a R1CS?

AND and OR Gates in R1CS

If z \in \mathbb{F}_p = \{0,1,\ldots,p-1\} satisfies z(1-z) = 0, then z \in \{0,1\}
Given z_1(1-z_1) = 0, z_2(1-z_2) = 0
- z_3 = z_1 \land z_2 is expressed as z_1z_2 = z_3
- z_3 = z_1 \lor z_2 is expressed as (1-z_1)\cdot(1-z_2) =1- z_3

XOR and NOT Gates in R1CS

Given z_1(1-z_1) = 0, z_2(1-z_2) = 0, we can express z_3 = z_1 \oplus z_2 as (z_1+z_1) \cdot z_2 = z_1 + z_2 - z_3.
- If z_2=0, then z_3 = z_1
- If z_2=1, then z_3 = 1-z_1
Given z_1(1-z_1) = 0, we can express z_2 = \lnot z_1 as (1-z_1) \cdot 1 = z_2.

Operations on 32-bit Words

A 32-bit word = Vector of 32 booleans
- U = [U_0, U_1, \ldots, U_{31}]
- Costs 32 constraints of the form x(1-x) = 0
SHA-256 involves operations like
- \textsf{Ch}(U,V,W) = (U \land V) \oplus (\lnot U \land W)
- \textsf{ROTR}^n(U) = Rotate right the U bits n times
- W = U +V \bmod 2^{32}

Addition Modulo 2^{32}

Suppose we want to calculate W = U +V \bmod 2^{32}
- Assume field size p \gg 2^{32}
Calculate field element u = \sum_{i=0}^{31} U_i \cdot 2^i
Calculate field element v = \sum_{i=0}^{31} V_i \cdot 2^i
Allocate 33 bits W = [W_0, W_1,\ldots,W_{32}]
Calculate field element w = \sum_{i=0}^{32} W_i \cdot 2^i
Check that w = u+v
Truncate W to 32 bits

Proving R1CS Instances

Collecting all the R1CS Constraints

We will have several constraints of the form (a_{j,0} + \sum_{i=1}^m a_{j,i} z_i)(b_{j,0} + \sum_{i=1}^m b_{j,i} z_i) = c_{j,0} + \sum_{i=1}^m c_{j,i} z_i where j=1,2,\ldots,n
Construct matrix A using [a_{j,0}, \ a_{j,1}, \ldots ,a_{j,m}] vectors
Similarly, construct B and C matrices
An R1CS instance can be expressed as A \mathbf{z} \odot B\mathbf{z} = C\mathbf{z} where \odot is the Hadamard product

Proof Systems for R1CS

Groth16 is a pairing-based SNARK that can prove R1CS instances
- Pro: Constant proof sizes
- Con: Involves a trusted setup
Spartan is a SNARK without trusted setup for proving R1CS instances
- Con: Proof size = O(\sqrt{n}) for a statement of size n
bellpepper circuits are provable using both Groth16 and Spartan

Incremental Verifiable Computation

Suppose the computation to be proved has this form
If F is expressible in R1CS, then the Nova folding scheme can be used to compress the computation
Nova folds all n steps into a single relaxed R1CS instance
bellpepper circuits can be proved using Nova

bellpepper

A Rust library for writing R1CS circuits
Repository: https://github.com/lurk-lab/bellpepper
Repo has two crates
- bellpepper-core
- bellpepper
Core functionality of bellperson was extracted into bellpepper-core

`bellpepper-core`

bellpepper-core/
├── benches
│   └── lc.rs
├── Cargo.toml
└── src
    ├── constraint_system.rs
    ├── gadgets
    │   ├── boolean.rs
    │   ├── mod.rs
    │   └── num.rs
    ├── lc.rs
    ├── lib.rs
    └── util_cs
        ├── mod.rs
        └── test_cs.rs

Variables

Inputs and Auxiliary Variables

Suppose we want to prove that x,y satisfy the equation y = x^3 + x+ 1
An R1CS instance for this statement
- x \times x = x_2
- x_2 \times x = x_3
- 1 \times (x_3 + x + 1) = y
x,y are the inputs and x_2, x_3 are auxiliary variables
Inputs are public, auxiliary variables can be kept private

Outputs are also Inputs

Suppose we want to prove that y = \text{SHA-256}(r \| x) where r \in \{0,1\}^{256} is a secret blinding factor
An R1CS instance for this statement will have x,y as input variables and r as an auxiliary variable
Even though y is an output of the hash function, it is an input to the verifiable computation
The SHA-256 computation involves many auxiliary variables, other than r

Variables

bellpepper-core/src/lc.rs

Index

/// Represents the index of either an input variable or
/// auxiliary variable.
pub enum Index {
    Input(usize),
    Aux(usize),
}

Variable

/// Represents a variable in our constraint system.
pub struct Variable(pub Index);

Linear Combinations

bellpepper-core/src/lc.rs

Indexer

struct Indexer<T> {
    values: Vec<(usize, T)>,
    /// Used to optimize consecutive operations
    last_inserted: Option<(usize, usize)>,
}

LinearCombination

pub struct LinearCombination<Scalar: PrimeField> {
    inputs: Indexer<Scalar>,
    aux: Indexer<Scalar>,
}

The PrimeField trait is defined in the ff crate

Test Constraint System

`ConstraintSystem` Trait

bellpepper-core/src/constraint_system.rs
Models an R1CS instance
alloc: Allocates an auxiliary variable
alloc_input: Allocates an input variable
enforce: Enforces an R1CS constraint between three linear combinations

`TestConstraintSystem`

Implements the ConstraintSystem trait for testing

pub struct TestConstraintSystem<Scalar: PrimeField> {
    named_objects: HashMap<String, NamedObject>,
    current_namespace: Vec<String>,
    constraints: Vec<(
        LinearCombination<Scalar>,
        LinearCombination<Scalar>,
        LinearCombination<Scalar>,
        String,
    )>,
    inputs: Vec<(Scalar, String)>,
    aux: Vec<(Scalar, String)>,
}

All variables and constraints have String labels for debugging

`TestConstraintSystem` Example

use bellpepper_core::{
    test_cs::TestConstraintSystem,
    ConstraintSystem
};
use pasta_curves::pallas::Scalar as Fq;

fn main() {
    let mut cs = TestConstraintSystem::<Fq>::new();
    let a = cs.alloc(|| "a var", || Ok(Fq::from(10u64))).unwrap();
    let b = cs.alloc(|| "b var", || Ok(Fq::from(4u64))).unwrap();
    let c = cs.alloc(|| "product", || Ok(Fq::from(40u64))).unwrap();

    cs.enforce(|| "mult",
        |lc| lc + a,
        |lc| lc + b,
        |lc| lc + c
    );
    assert!(cs.is_satisfied());
    assert_eq!(cs.num_constraints(), 1);
}

Field Elements

`AllocatedNum`

bellpepper-core/src/gadgets/num.rs

AllocatedNum

pub struct AllocatedNum<Scalar: PrimeField> {
    value: Option<Scalar>,
    variable: Variable,
}

Allows tracking the value of a variable in a computation

`AllocatedNum` Example

use bellpepper_core::{
    num::AllocatedNum,
    test_cs::TestConstraintSystem,
    ConstraintSystem
};
use pasta_curves::pallas::Scalar as Fq;

fn main() {
    let mut cs = TestConstraintSystem::<Fq>::new();

    let a = AllocatedNum::alloc(
        cs.namespace(|| "a"),
        || Ok(Fq::from(10u64))
    ).unwrap();
    
    let b = AllocatedNum::alloc(
        cs.namespace(|| "b"),
        || Ok(Fq::from(4u64))
    ).unwrap();
    
    let c = a.mul(&mut cs, &b).unwrap();

    assert!(c.get_value().unwrap() == Fq::from(40u64));
    assert!(cs.is_satisfied());
}

`Num`

In an R1CS constraint, there is no need to allocate a new variable for the sum of variables
- Suppose y = x_1 + x_2
- In any linear combination, y can be replaced with x_1+x_2

Num

pub struct Num<Scalar: PrimeField> {
    value: Option<Scalar>,
    lc: LinearCombination<Scalar>,
}

Num enables this behavior

Adding `Num`s

pub fn add(self, other: &Self) -> Self {
    let lc = self.lc + &other.lc;
    let value = match (self.value, other.value) {
        (Some(v1), Some(v2)) => {
            let mut tmp = v1;
            tmp.add_assign(&v2);
            Some(tmp)
        }
        (Some(v), None) | (None, Some(v)) => Some(v),
        (None, None) => None,
    };

    Num { value, lc }
}

Bits

`AllocatedBit`

bellpepper-core/src/gadgets/boolean.rs
Models a variable that can take only values 0 and 1

AllocatedBit

pub struct AllocatedBit {
    variable: Variable,
    value: Option<bool>,
}

Has and, xor, nor, and_not methods

`AllocatedBit::alloc`

/// Allocate a variable in the constraint system which can only be a
/// boolean value.
pub fn alloc<Scalar, CS>(mut cs: CS, value: Option<bool>) 
  -> Result<Self, SynthesisError>
where
    Scalar: PrimeField,
    CS: ConstraintSystem<Scalar>,
{
    let var = cs.alloc(
        || "boolean",
        || {
            if value.ok_or(SynthesisError::AssignmentMissing)? {
                Ok(Scalar::ONE)
            } else {
                Ok(Scalar::ZERO)
            }
        },
    )?;

    // Constrain: (1 - a) * a = 0
    // This constrains a to be either 0 or 1.
    cs.enforce(
        || "boolean constraint",
        |lc| lc + CS::one() - var,
        |lc| lc + var,
        |lc| lc,
    );

    Ok(AllocatedBit {
        variable: var,
        value,
    })
}

`Boolean`

Boolean

pub enum Boolean {
    /// Existential view of the boolean variable
    Is(AllocatedBit),
    /// Negated view of the boolean variable
    Not(AllocatedBit),
    /// Constant (not an allocated variable)
    Constant(bool),
}

When a bit is a known constant, not allocating it saves one R1CS constraint
The negated view also saves one R1CS constraint when the bit is complemented

`Boolean::not`

Method

/// Return a negated interpretation of this boolean.
pub fn not(&self) -> Self {
    match *self {
        Boolean::Constant(c) => Boolean::Constant(!c),
        Boolean::Is(ref v) => Boolean::Not(v.clone()),
        Boolean::Not(ref v) => Boolean::Is(v.clone()),
    }
}

A constant Boolean is mapped to another constant with complemented value
Is and Not are mapped to each other

`Boolean::and`

/// Perform AND over two boolean operands
pub fn and<'a, Scalar, CS>(cs: CS, a: &'a Self, b: &'a Self)
-> Result<Self, SynthesisError>
where
    Scalar: PrimeField,
    CS: ConstraintSystem<Scalar>,
{
  match (a, b) {
    // false AND x is always false
    (&Boolean::Constant(false), _)
      | (_, &Boolean::Constant(false)) => {
        Ok(Boolean::Constant(false))
    }

    // true AND x is always x
    (&Boolean::Constant(true), x) | (x, &Boolean::Constant(true)) =>
        Ok(x.clone()),

    // a AND (NOT b)
    (&Boolean::Is(ref is), &Boolean::Not(ref not))
       | (&Boolean::Not(ref not), &Boolean::Is(ref is)) => {
        Ok(Boolean::Is(AllocatedBit::and_not(cs, is, not)?))
    }

    // (NOT a) AND (NOT b) = a NOR b
    (Boolean::Not(a), Boolean::Not(b)) => 
        Ok(Boolean::Is(AllocatedBit::nor(cs, a, b)?)),

    // a AND b
    (Boolean::Is(a), Boolean::Is(b)) => 
        Ok(Boolean::Is(AllocatedBit::and(cs, a, b)?)),
  }
}

32-bit Integers

`UInt32`

Needed in the SHA-256 circuit

UInt32

pub struct UInt32 {
    // Least significant bit first
    bits: Vec<Boolean>,
    value: Option<u32>,
}

`UInt32::alloc`

/// Allocate a `UInt32` in the constraint system
pub fn alloc<Scalar, CS>(mut cs: CS, value: Option<u32>)
    -> Result<Self, SynthesisError>
where
    Scalar: PrimeField,
    CS: ConstraintSystem<Scalar>,
{
    let values = match value {
        Some(mut val) => {
            let mut v = Vec::with_capacity(32);

            for _ in 0..32 {
                v.push(Some(val & 1 == 1));
                val >>= 1;
            }

            v
        }
        None => vec![None; 32],
    };

    let bits = values
        .into_iter()
        .enumerate()
        .map(|(i, v)| {
            Ok(Boolean::from(AllocatedBit::alloc(
                cs.namespace(|| format!("allocated bit {}", i)),
                v,
            )?))
        })
        .collect::<Result<Vec<_>, SynthesisError>>()?;

    Ok(UInt32 { bits, value })
}

SHA-256 Circuit in bellpepper

Recall the SHA-256 Algorithm

Two stages
- Preprocessing
- Hash Computation
Preprocessing stage
- Given a message of length L
- Append a single 1 bit
- Append K zero bits such that L+1+K+64 is a multiple of 512
- Append L as a 64-bit big-endian integer
Relevant code

Hash Computation

Padded input is split into N 512-bit blocks M^{(1)}, \ldots, M^{(N)}
H^{(0)} is initialized to known constants
Given H^{(i-1)}, the next H^{(i)} is calculated as \begin{equation*} H^{(i)} = f(M^{(i)}, H^{(i-1)}), \quad 1 \le i \le N. \end{equation*}

Step 1 of Compression Function

The ith message block has sixteen 32-bit blocks
Internal state initialization \begin{equation*} W_j = \begin{cases} M_j^{(i)} & 0 \le j \le 15, \\ \sigma_1(W_{j-2}) + W_{j-7} + \sigma_0(W_{j-15}) + W_{j-16} & 16 \le j \le 63. \end{cases} \end{equation*}
Here \sigma_0(U) = \textsf{ROTR}^{7}(U) \oplus \textsf{ROTR}^{18}(U) \oplus \textsf{SHR}^{3}(U)\\ \sigma_1(U) = \textsf{ROTR}^{17}(U) \oplus \textsf{ROTR}^{19}(U) \oplus \textsf{SHR}^{10}(U)
Relevant code

Step 2 of Compression Function

Initialize eight 32-bit words \begin{align*} (A,B,C,D,E,F,G,H) = \left(H_0^{(i-1)}, H_1^{(i-1)}, \ldots, H_6^{(i-1)}, H_7^{(i-1)}\right). \end{align*}

Relevant code

let mut a = Maybe::Concrete(current_hash_value[0].clone());
let mut b = current_hash_value[1].clone();
let mut c = current_hash_value[2].clone();
let mut d = current_hash_value[3].clone();
let mut e = Maybe::Concrete(current_hash_value[4].clone());
let mut f = current_hash_value[5].clone();
let mut g = current_hash_value[6].clone();
let mut h = current_hash_value[7].clone();

`Maybe` enum

enum Maybe {
    Deferred(Vec<UInt32>),
    Concrete(UInt32),
}

impl Maybe {
    fn compute<Scalar, CS, M>(self, cs: M, others: &[UInt32])
      -> Result<UInt32, SynthesisError>
    where
        Scalar: PrimeField,
        CS: ConstraintSystem<Scalar>,
        M: ConstraintSystem<Scalar, Root = MultiEq<Scalar, CS>>,
    {
        Ok(match self {
            Maybe::Concrete(ref v) => return Ok(v.clone()),
            Maybe::Deferred(mut v) => {
                v.extend(others.iter().cloned());
                UInt32::addmany(cs, &v)?
            }
        })
    }
}

Relevant code

Step 3 of Compression Function

For j = 0,1,\ldots,63, iteratively update A,B,\ldots,H \begin{align*} \begin{split} & T_1 = H + \Sigma_1(E) + \textsf{Ch}(E,F,G) + K_j + W_j \\ & T_2 = \Sigma_0(A) + \textsf{Maj}(A,B,C) \\ & (A,B,C,D,E,F,G,H) = (T_1+T_2, A, B, C, D+T_1, E, F, G) \end{split} \end{align*}
Here \begin{align*} \Sigma_0(U) & = \textsf{ROTR}^{2}(U) \oplus \textsf{ROTR}^{13}(U) \oplus \textsf{ROTR}^{22}(U) \\ \Sigma_1(U) & = \textsf{ROTR}^{6}(U) \oplus \textsf{ROTR}^{11}(U) \oplus \textsf{ROTR}^{25}(U) \\ \textsf{Ch}(U,V,W) & = (U \land V) \oplus (\lnot U \land W), \\ \textsf{Maj}(U,V,W) & = (U \land V) \oplus (U \land W) \oplus (V \land W), \end{align*}
Relevant code

Step 4 of Compression Function

Calculate H^{(i)} from H^{(i-1)} \begin{equation*} (H_0^{(i)}, H_1^{(i)}, \ldots, H_7^{(i)}) = \hspace{12cm} \\ \left(A+H_0^{(i-1)}, B+H_1^{(i-1)}, \ldots, H+H_7^{(i-1)}\right). \end{equation*}
Relevant code

Writing and proving bellpepper circuits

`Circuit` trait

Your circuits have to implement the Circuit trait

pub trait Circuit<Scalar: PrimeField> {
    /// Synthesize the circuit into an R1CS instance
    fn synthesize<CS: ConstraintSystem<Scalar>>(self, cs: &mut CS)
        -> Result<(), SynthesisError>;
}

So they have to implement synthesize function
They can then be proved using the Groth16 or Spartan proof systems

Cubic circuit example

struct CubicCircuit<F: PrimeField> {
  _p: PhantomData<F>,
}

impl<F> Circuit<F> for CubicCircuit<F>
where
  F: PrimeField,
{
  fn synthesize<CS: ConstraintSystem<F>>(self, cs: &mut CS)
      -> Result<(), SynthesisError>
  {
    // Consider a cubic equation: `x^3 + x + 1 = y`
    let x = AllocatedNum::alloc(
        cs.namespace(|| "x"),
        || Ok(F::ONE + F::ONE)
    )?;
    let x_sq = x.square(cs.namespace(|| "x_sq"))?;
    let x_cu = x_sq.mul(cs.namespace(|| "x_cu"), &x)?;
    
    let y = AllocatedNum::alloc(cs.namespace(|| "y"), || {
      Ok(x_cu.get_value().unwrap() + x.get_value().unwrap() + F::ONE)
    })?;

    cs.enforce(
      || "y = x^3 + x + 1",
      |lc| lc + x_cu.get_variable() + x.get_variable() + CS::one(),
      |lc| lc + CS::one(),
      |lc| lc + y.get_variable(),
    );

    let _ = y.inputize(cs.namespace(|| "output"));

    Ok(())
  }
}

Demo

bellpepper-gadgets

https://github.com/lurk-lab/bellpepper-gadgets
Existing crates
- SHA1, SHA512, Keccak
- Non-native arithmetic
- Ed25519 curve operations
- Merkle proofs
More contributions welcome!

Resources

Slides: https://www.ee.iitb.ac.in/~sarva/bellpepper
Code: https://github.com/avras/bellpepper-tutorial-files
bellpepper: https://github.com/lurk-lab/bellpepper
Nova: https://github.com/Microsoft/Nova
Arecibo: https://github.com/lurk-lab/arecibo

bellpepper

bellpepper

Verifiable Computation

SNARKs

Arithmetic Circuits

Rank-1 Constraint Systems

Why Rank 1?

SHA-256

Cryptographic Hash Functions

Co-Domain for 256-bit Output Length

SHA-256

Two Stages

Preprocessing

Hash Computation

Building Blocks of f

Building Blocks of f

f Calculation

Sample SHA256 Output

Observations

R1CS for SHA-256

Proving Knowledge of Preimage

AND and OR Gates in R1CS

XOR and NOT Gates in R1CS

Operations on 32-bit Words

Addition Modulo 2^{32}

Proving R1CS Instances

Collecting all the R1CS Constraints

Proof Systems for R1CS

Incremental Verifiable Computation

bellpepper

bellpepper

bellpepper-core

Variables

Inputs and Auxiliary Variables

Outputs are also Inputs

Variables

Linear Combinations

Test Constraint System

ConstraintSystem Trait

TestConstraintSystem

TestConstraintSystem Example

Field Elements

AllocatedNum

AllocatedNum Example

Num

Adding Nums

Bits

AllocatedBit

AllocatedBit::alloc

Boolean

Boolean::not

Boolean::and

32-bit Integers

UInt32

UInt32::alloc

SHA-256 Circuit in bellpepper

Recall the SHA-256 Algorithm

Hash Computation

Step 1 of Compression Function

Step 2 of Compression Function

Maybe enum

Step 3 of Compression Function

Step 4 of Compression Function

Writing and proving bellpepper circuits

Circuit trait

Cubic circuit example

Demo

bellpepper-gadgets

Resources

`bellpepper-core`

`ConstraintSystem` Trait

`TestConstraintSystem`

`TestConstraintSystem` Example

`AllocatedNum`

`AllocatedNum` Example

`Num`

Adding `Num`s

`AllocatedBit`

`AllocatedBit::alloc`

`Boolean`

`Boolean::not`

`Boolean::and`

`UInt32`

`UInt32::alloc`

`Maybe` enum

`Circuit` trait