groth16

A from-scratch implementation of the Groth16 zk-SNARK in Rust, written to understand the protocol end to end rather than to be used in production.

Everything below the elliptic-curve arithmetic is implemented here: the R1CS-to-QAP reduction, the FFT over a finite field, Lagrange basis evaluation, the trusted setup, the prover and the verifier. Curve operations and pairings come from bls12_381, group, ff and pairing.

Layout

Module	Contents
src/groth16	R1CS interface, QAP reduction, setup, prove, verify
src/fourier	Radix-2 FFT — one version over a prime field, one over Complex32

How it works

A circuit is supplied through the R1CS trait rather than a concrete matrix type, so any representation can be plugged in:

pub trait R1CS<F: Field> {
    fn get_n(&self) -> usize;                        // number of constraints
    fn get_m(&self) -> usize;                        // number of variables, excluding the constant 1
    fn get(&self, c: Column, i: usize, j: usize) -> F;  // entry of matrix U, V or W
}

The full assignment vector has length m + 1 and is laid out as [1, public inputs..., witness...]. The number of constraints n must be a power of two, because the QAP domain is built from the n-th roots of unity.

The pipeline is the standard one. Each column of U, V and W is treated as the evaluation vector of a polynomial over the domain {1, ω, ω², …, ω^(n-1)}; an inverse FFT recovers its coefficients; the polynomials are evaluated at the secret point τ during setup. verify_r1cs is available separately to check an assignment directly, which is useful when debugging a new circuit.

The FFT domain is derived from the field's two-adicity: F::ROOT_OF_UNITY is squared F::S - log2(n) times to obtain a primitive n-th root of unity. This is why n must be a power of two and cannot exceed 2^F::S.

Computing the quotient polynomial

h(x) = (u(x)·v(x) − w(x)) / t(x) where t(x) = xⁿ − 1 is the vanishing polynomial of the domain. Evaluating this directly at a domain point gives 0/0, since both numerator and denominator vanish there. The implementation applies L'Hôpital's rule instead, evaluating

h(ωⁱ) = (u'·v + u·v' − w')(ωⁱ) / t'(ωⁱ)

and uses t'(x) = n·x^(n-1), so t'(ωⁱ) = n·ω^(-i). The derivatives are taken on the coefficient form and transformed back with a forward FFT, so no polynomial division is needed anywhere.

Usage

use bls12_381::Bls12;

let (pk, vk) = setup::<Bls12, _>(&r1cs, num_public_inputs, rng.clone());
let proof    = prove::<Bls12, _>(&r1cs, pk, assignment, num_public_inputs, rng.clone());
assert!(verify::<Bls12>(vk, public_inputs, proof));

src/groth16/mod.rs contains a worked example as a test: a four-constraint circuit proving that w3 = x1·x2 + x3·x4, with the assignment vector spelled out variable by variable.

Build

cargo test

The test suite covers the primitive roots, polynomial differentiation, the equivalence between Lagrange-basis and FFT evaluation, pairing bilinearity, and one end-to-end setup → prove → verify run.

Status and limitations

This is a study implementation. It is not suitable for any real use:

• Not audited, and not written with side channels in mind — no constant-time guarantees.
• setup samples the trapdoor (τ, α, β, γ, δ) in process and drops it. Real deployments require a multi-party ceremony; here the toxic waste is simply in memory.
• LagrangeBaseEvaluation::get_value recomputes the barycentric weights on every call, making it O(n) per basis polynomial. Fine for small circuits, quadratic overall.
• There is no circuit front end. Constraint matrices must be written by hand or generated by something else.