How GKR works

StateSync-GKR implements the GKR protocol and the sumcheck protocol from their published constructions, with a Libra-style sparse prover for each layer. This page builds the model you need to read the code: what is proved, how a claim travels from the outputs to the inputs, what the verifier must still check at the end, and why the production prover does not need memory that grows with the square of a layer's width.

The protocol in brief#

A prover claims that a layered arithmetic circuit, evaluated on some inputs, produces certain outputs. The verifier does not re-run the gates. It asks the prover to reduce a claim about the output layer to a claim about the layer below, and repeats this layer by layer. Each reduction is one run of the sumcheck protocol and ends in a claim about the next layer's values at a random point.

When the reduction reaches the input layer, the remaining claims are about the input vector itself, and whoever holds the inputs checks them directly. Intermediate layer values never appear in the proof as a whole: besides its sumcheck messages, each layer contributes two claimed evaluations of the layer below, and the next sumcheck holds the prover to them.

Layered circuits#

A layered circuit is a list of layers. Each wire of layer i is computed only from wires of layer i + 1, and the last layer reads from the input vector. In the engine, layers[0] is the output layer, and every layer stores width_bits, the base-2 logarithm of its wire count, because GKR indexes wires by bit strings.

The circuit representation in statesync_gkr::gkr has three weighted gate kinds and an additive constant vector per layer:

Every wire of layer i is therefore defined by one identity over the values V_{i+1} of the layer below:

V_i(z) = const_i(z)
       + sum over Lin  gates (out = z):  coeff * V_{i+1}(in1)
       + sum over Mul  gates (out = z):  coeff * V_{i+1}(in1) * V_{i+1}(in2)
       + sum over Pow3 gates (out = z):  coeff * V_{i+1}(in1)^3

Addition needs no gate of its own, because several Lin gates that write to the same output wire accumulate. The cube gate exists for Poseidon2, the hash this engine proves, whose S-box is x^3. Every layer has algebraic degree at most 3.

Multilinear extensions#

A layer with 2^s wires is a table of 2^s field values indexed by s-bit strings. Its multilinear extension (MLE) is the unique polynomial in s variables, of degree at most one in each variable, that equals the table on every bit string. The MLE can be evaluated at any point of a larger field. Two different tables agree at a random point only with small probability, so one evaluation at a random point works as a fingerprint of the whole table.

The circuit structure becomes polynomials in the same way. For each gate kind, a wiring predicate maps an output wire and its input wires to the coefficient of the gate that connects them, or to zero where no such gate exists. Single-input gates use one input index, Mul gates use two. The verifier needs the MLEs of these predicates, and of the constant vector, at random points. A WiringOracle implementation provides those evaluations; Circuits and layers describes the oracles the verifier can use.

Two engine conventions matter when you read the code. Variable 0 is the most significant bit of a wire index, and gkr::mle::mle_eval_base evaluates an MLE by folding one variable at a time. Circuit values are base-field elements, embedded into the challenge field before they are evaluated at a challenge point.

Sumcheck#

Sumcheck lets a verifier check a claim of the form "the sum of a polynomial g over all n-bit inputs equals C" while evaluating g only once, at a random point. It runs in n rounds:

1. The prover sends a univariate round polynomial: g with the earlier variables fixed to the challenges drawn so far, the current variable left free, and every later variable summed out.
2. The verifier checks that the polynomial's degree is within the bound and that its values at 0 and 1 add up to the running claim.
3. The verifier draws a random challenge r and replaces the running claim with the round polynomial evaluated at r.

After the last round the verifier holds a residual claim: g, evaluated at the point made of all the challenges, must equal the final running claim. In statesync_gkr::sumcheck, verify performs the per-round checks and returns this residual claim as a Subclaim { point, expected_eval }. It does not evaluate g itself; the caller discharges the subclaim. In GKR that caller is the layer reduction.

From the outputs to the inputs#

GKR chains one sumcheck per layer:

1. Output claim. The transcript yields a random point z0 over the output wires, and the verifier computes the MLE of the claimed outputs at z0. The SMT frontend always claims an all-zero output layer; Circuits and layers explains why.
2. Layer sumcheck. For layer i, the claim minus the layer's constant term becomes the claimed sum of one sumcheck over 2s variables, written (x, y), where s is width_bits of layer i + 1. The cube term makes each round polynomial at most degree 4, so the per-round bound LAYER_ROUND_DEGREE is 4. A selector term confines the single-input gates to y = 0, so one sumcheck covers all three gate kinds.
3. End check. The sumcheck ends at a random point (x*, y*). The prover sends eval_x and eval_y, its claimed values of the layer below at x* and at y*. The verifier evaluates the wiring MLEs at that point and checks that the sumcheck's residual claim equals the layer identity rebuilt from the two values.
4. Carry. The two values become the claims on the next layer, combined with a fresh challenge r: the point x* with coefficient 1 and the point y* with coefficient r.
5. Input claims. After the last layer the verifier returns an InputClaim with two points and two expected values. Whoever knows the inputs must evaluate the input MLE at both points and compare.

claimed outputs  -> claim on layer 0 at z0
layer 0          -> sumcheck over (x, y) -> eval_x, eval_y about layer 1
layer 1          -> sumcheck over (x, y) -> eval_x, eval_y about layer 2
...
last layer       -> InputClaim: two points on the input vector
input owner      -> evaluates the input MLE at both points and compares

The proof is a GkrProof holding one LayerProof per layer, output layer first. A LayerProof contains the layer's sumcheck round polynomials and the two values eval_x and eval_y.

What the proof does not commit to#

GKR needs no commitment to intermediate layer values. Each layer enters the proof only through two evaluations, and the next sumcheck holds the prover to them. The verifier must still know the outputs, which are claimed, and must be able to evaluate the inputs.

The engine's full circuit commitment is a different object. It is a digest of the circuit's gates and constants, absorbed into the transcript so that a proof refers to one exact circuit. It carries no information about wire values.

The SMT verifier discharges the two input claims by rebuilding the input vector from the original request: the leaf, the sibling path, the key bits, the roots and the value digest. Rebuilding recomputes the leaf hash and every hash along the path, so the verifier needs the private witness. Separately, the inner proof has no zero-knowledge property: its sumcheck messages and layer evaluations are computed from the witness without masking. Trust boundaries describes what follows from this.

Fiat-Shamir and the transcript#

In the interactive protocol the verifier sends random challenges. The Fiat-Shamir transform replaces them with values derived from a hash of everything sent so far, so the prover can produce the whole proof alone. Prover and verifier replay the same sequence of observations. A change to any message changes every later challenge, and verification fails.

The engine's Transcript is a Poseidon2 duplex sponge over KoalaBear with width 16 and rate 8. A proof transcript observes, in this order:

1. the domain tag statesync-gkr/v0.1, one field element per byte;
2. the circuit shape (operation tag, tree depth, input width in bits, layer count, and each layer's width in bits, gate count and constant count), followed by the full circuit commitment;
3. the public inputs: old_root, new_root, op_kind_tag, the low and high 32-bit halves of asset_id, and value_digest;
4. the claimed output values, after which the output point z0 is drawn;
5. for each layer, every sumcheck round's polynomial coefficients, each followed by one challenge, then eval_x and eval_y, then, if another layer follows, one carry challenge.

Each extension-field challenge is assembled from four base-field outputs of the sponge. The machine-checked soundness bound is stated for uniformly random challenges; applying it to this deterministic transcript requires a Fiat-Shamir argument that the repository does not contain. See Formal verification.

KoalaBear and the degree-four extension#

Circuit values, digests and the absorbed public-input values are elements of the KoalaBear prime field, p = 2^31 - 2^24 + 1 = 2130706433 (BaseField). Verifier challenges come from the degree-four binomial extension F_p[X] / (X^4 - 3) (ChallengeField, with CHALLENGE_EXT_DEGREE equal to 4).

The extension exists for the soundness arithmetic. In one sumcheck round, a cheating prover gets through with probability at most the round degree divided by the size of the field the challenge comes from. With about 2^31 elements the base field is too small for that bound to stay negligible across many rounds. The extension field has p^4 elements, about 2^124. That figure is the size of the challenge field; it is not a measured or proven security level of the executable verifier.

Poseidon2#

The engine uses one Poseidon2 permutation over KoalaBear for in-circuit hashing, the transcript and the circuit commitment: width 16, S-box x^3, 4 initial external rounds, 20 internal rounds and 4 final external rounds, with the round constants published in Plonky3 0.4.3.

Inside the circuit, the compiler emits each permutation gate by gate as 29 layers: one initial linear layer and one layer per round. The native reference primitives::poseidon2_arith::permute wraps the production permutation, and the test suite cross-checks the compiled gates against it. Plonky3 supplies the field, permutation and challenger code. The sumcheck, GKR assembly, SMT compiler, sparse prover and wiring oracles are implemented in this repository.

Sparse layer reduction#

To answer the sumcheck of one layer, the prover needs an oracle that produces round polynomials of the layer polynomial over (x, y) and binds one variable per round.

The engine keeps a direct version as a test-only reference, DenseLayerOracle. It materializes six factor tables over the full (x, y) hypercube: the linear and cube predicates, the values of the layer below indexed by x and by y, the y = 0 selector, and the multiplication predicate. Each table has 2^(2s) entries, so memory grows with the square of the layer's input width.

The production oracle, SparseLayerOracle, uses Libra-style two-phase sparse booking. Three of the six factors depend only on x, two depend only on y, and the multiplication predicate is nonzero only where a Mul gate exists. Writing the sum over (x, y) as a sum over x of a sum over y removes the quadratic tables:

• Phase 1 binds x. The oracle keeps four tables of 2^s entries over x. One of them is a booking table that holds, for each x, the sum over y of the multiplication predicate times the value at y. It is accumulated directly from the list of Mul gates.
• Phase 2 binds y. With x fixed at x*, the x-only factors collapse to three scalars, and the oracle builds three tables of 2^s entries over y.

Dense reference   six tables over (x, y), 2^(2s) entries each
Sparse oracle     phase 1: four tables over x, 2^s entries each
                  phase 2: three tables over y, 2^s entries each
                  plus the list of Mul gates

For a layer with n_in input wires, n_out output wires and m multiplication gates, the sparse oracle's auxiliary memory is O(n_out + n_in + m), and no table over (x, y) is allocated. The regrouping uses only the distributivity and commutativity of field arithmetic, so both oracles emit bit-identical round polynomials. They share one prover driver and one transcript order, and the test suite compares whole proofs from both.

In a two-layer mixed circuit of width 4,096, measured against the engine's own test-only Dense reference, whole-process peak RSS was 89.46 times lower and additional requested allocation was 3,242.41 times lower. The two figures come from separate measurement boundaries of one internal comparison; neither compares StateSync-GKR with other GKR implementations. Benchmark results gives the conditions.

Where each step lives#

The sumcheck and protocol crates do not depend on the SMT compiler, so another arithmetic frontend can use them directly. See Custom frontends.

See it in code#

The program below uses only the generic layers. It builds a two-layer circuit with all three gate kinds, proves its evaluation, verifies the proof with the general table oracle, and discharges both input claims. A real frontend also absorbs its circuit identity and public statement into the transcript before proving; the SMT frontend does this for you.

use statesync_gkr::gkr::mle::mle_eval_base;
use statesync_gkr::gkr::wiring::TableWiring;
use statesync_gkr::gkr::{self, Gate, GateKind, Layer, LayeredCircuit, evaluate_circuit};
use statesync_gkr::primitives::Transcript;
use statesync_gkr::primitives::field::{BaseField, PrimeCharacteristicRing};

fn gate(kind: GateKind, out: u32, in1: u32, in2: u32) -> Gate<BaseField> {
    Gate {
        kind,
        out,
        in1,
        in2,
        coeff: BaseField::ONE,
    }
}

fn main() -> Result<(), String> {
    // Layer 1 (two wires): [in0 * in1, in2^3].
    let layer1 = Layer {
        width_bits: 1,
        gates: vec![gate(GateKind::Mul, 0, 0, 1), gate(GateKind::Pow3, 1, 2, 2)],
        consts: Vec::new(),
    };
    // Layer 0, the output layer (two wires): [w0 + w1, w0].
    let layer0 = Layer {
        width_bits: 1,
        gates: vec![
            gate(GateKind::Lin, 0, 0, 0),
            gate(GateKind::Lin, 0, 1, 1),
            gate(GateKind::Lin, 1, 0, 0),
        ],
        consts: Vec::new(),
    };
    let circuit = LayeredCircuit {
        layers: vec![layer0, layer1],
        input_width_bits: 2,
    };
    let inputs = [3u32, 5, 7, 11].map(BaseField::from_u32);

    // Prover: evaluate every layer, bind the claimed outputs, prove.
    let witness = evaluate_circuit(&circuit, &inputs)
        .map_err(|error| format!("evaluation failed: {error:?}"))?;
    let outputs = witness.layer_values[0].clone();
    let mut prover_transcript = Transcript::new(b"example/gkr");
    prover_transcript.observe_many(&outputs);
    let proof = gkr::prove(&circuit, &witness, &mut prover_transcript);

    // Verifier: replay the same observations, then run every layer reduction.
    let wiring = TableWiring::new(&circuit);
    let mut verifier_transcript = Transcript::new(b"example/gkr");
    verifier_transcript.observe_many(&outputs);
    let claim = gkr::verify(&circuit, &wiring, &outputs, &proof, &mut verifier_transcript)
        .map_err(|error| format!("proof rejected: {error:?}"))?;

    // The input owner discharges both residual claims.
    let x_ok = mle_eval_base(&inputs, &claim.point) == claim.expected_eval;
    let y_ok = mle_eval_base(&inputs, &claim.point_y) == claim.expected_eval_y;
    if !(x_ok && y_ok) {
        return Err("an input claim does not match the inputs".to_owned());
    }
    println!("outputs={outputs:?} accepted");
    Ok(())
}

Skipping the last two checks would leave the proof unverified: gkr::verify returning Ok only means that every layer reduction was consistent, down to two claims about the inputs.

Next steps#

• Sparse Merkle state defines the statements the SMT frontend proves.
• Circuits and layers shows how an SMT operation becomes a layered circuit.
• Proof lifecycle follows one request through preparation, proving, encoding and verification.
• API reference lists every public item named on this page.