Custom frontends

The sumcheck and GKR crates of StateSync-GKR do not depend on its sparse-Merkle compiler, so a frontend of your own can prove other layered arithmetic computations with the same core. This guide lists what such a frontend must supply, walks through a complete program that proves several instances of an arithmetic relation with one proof, and states what the engine fixes and what it leaves to you.

Before you begin#

• Read How GKR works. It explains the layer identity, the per-layer sumcheck, the transcript and the two residual input claims, and it shows the smallest possible use of the core. This guide builds a complete frontend on those ideas.
• Use the statesync-gkr dependency described in Installation. The core is reached through statesync_gkr::gkr for circuits, the GKR prover and verifier and the wiring oracles, statesync_gkr::primitives for the field types and the transcript, and statesync_gkr::sumcheck.

What a frontend supplies#

The sparse-Merkle facade performs every row of this table for its three operations. Its conveniences, such as PreparedSync, the binding of a proof to a SyncRequest and the inner-proof-v1 codec, apply only to its own circuits.

Describe the circuit#

A LayeredCircuit lists its layers from the output layer, layers[0], down to the layer that reads the input vector. A layer has 2^width_bits wires and the input vector has 2^input_width_bits entries; unused wires stay zero. A Lin gate adds coeff * a to its output wire, a Mul gate adds coeff * a * b and a Pow3 gate adds coeff * a^3, where a and b are wires of the layer below.

• Each gate reads only the layer directly below it. A value needed several layers higher must be carried up by a Lin gate with coefficient 1 in each intermediate layer.
• Lin and Pow3 take one input, so set in2 equal to in1. compiler::validate_unary_gates reports a violation as CompileError::NonUnaryGate.
• Gates that write to the same output wire add up, so addition needs no gate kind of its own. Constants go in the layer's consts list as (wire, value) pairs.
• Every wire index must lie inside its layer. evaluate_circuit returns CircuitError::WireOutOfRange otherwise.

The circuit representation and its gate semantics belong to the interfaces that the current release line keeps fixed; see Versioning.

Lay out circuits with the builder#

Assigning wires and carrying values through layers by hand is error-prone. compiler::builder::Builder takes a graph of arithmetic nodes and lays it out for you: it gives every node a level, inserts copy gates for values that skip levels and places the outputs you list, in that order, on the output layer.

The builder is the layout helper of the sparse-Merkle compiler, published as a public module. It is not a compiler for programs, and it is not one of the interfaces that the release line keeps fixed.

For a computation repeated over many instances, wrap each instance in scope(family, block) with one family label and consecutive block numbers, and build every instance with the same code so that their nodes line up slot for slot. The builder then places the family's blocks at a power-of-two stride from an aligned position in every layer, which is the layout that DerivedRegularWiring evaluates in closed form. Inputs keep the positions you give them, so lay out each instance's inputs at a power-of-two stride as well.

The hints only propose groups. DerivedRegularWiring::derive checks every proposed group gate by gate and keeps whatever does not fit on an exact sparse path, so a wrong or missing hint costs verification time. The derivation is designed so that its evaluations equal those of TableWiring on the same circuit; the repository's tests check this on its compiled circuits, and the example below verifies with both oracles. stats() reports how many gates the closed form covers.

Generate the witness#

gkr::evaluate_circuit(&circuit, &inputs) computes every layer and returns a CircuitWitness whose layer_values[0] holds the outputs and whose last entry is the input vector. inputs must have exactly 2^input_width_bits entries, otherwise the call returns CircuitError::InputWidthMismatch. gkr::prove expects this witness for the same circuit and does not check it.

Choose the output claim#

The verifier passes its own claimed outputs to gkr::verify; the proof does not carry them. Two conventions are common:

claimed_outputs must have one entry per wire of layers[0]. Any other length makes gkr::verify return GkrError::ShapeMismatch.

Bind the statement in the transcript#

gkr::prove and gkr::verify draw every challenge from the transcript you pass in, and they absorb nothing about your circuit or your statement themselves. Before calling either, absorb the same values in the same order on both sides:

1. A domain tag of your own, passed to Transcript::new. The sparse-Merkle frontend uses statesync-gkr/v0.1; a tag of your own keeps the transcripts of different frontends apart.
2. The circuit identity. The sparse-Merkle frontend absorbs its circuit's shape and full circuit commitment, but wrap::commitment::full_circuit_commitment takes sparse-Merkle parameters, so define your own binding. The example below absorbs every structural value of the circuit; a large circuit can absorb a digest computed once instead.
3. The statement: everything the verifier uses to discharge the input claims.
4. The claimed outputs.

Absorb each count and index as one field element, and refuse a value at or above the field order instead of reducing it. The engine's own circuit commitment does the same, because a reduced value would absorb exactly like a different, smaller value.

A complete frontend#

The program below proves, with one proof, that four instances of the relation a * b + a^3 = c hold. Each instance becomes one residual output, a * b + a^3 - c, which must be zero. The verifier knows every input, builds the circuit itself and checks the proof with two different wiring oracles.

use std::process::ExitCode;

use statesync_gkr::compiler::builder::{Builder, TapKind};
use statesync_gkr::compiler::{is_accepting, validate_unary_gates};
use statesync_gkr::gkr::mle::mle_eval_base;
use statesync_gkr::gkr::wiring::TableWiring;
use statesync_gkr::gkr::{
    self, DerivedRegularWiring, GateKind, GkrProof, LayeredCircuit, WiringOracle, evaluate_circuit,
};
use statesync_gkr::primitives::Transcript;
use statesync_gkr::primitives::field::{
    BaseField, ChallengeField, PrimeCharacteristicRing, PrimeField32,
};

/// Domain tag of this frontend's transcripts.
const DOMAIN_TAG: &[u8] = b"example/mul-cube-check/v1";
/// Independent instances checked by one proof.
const INSTANCES: u32 = 4;
/// Input wires per instance: a, b, c and one unused wire, a power-of-two stride.
const STRIDE: u32 = 4;
/// Builder family label shared by every instance.
const FAMILY: u32 = 0;

/// One instance of the statement `a * b + a^3 = c`.
#[derive(Clone, Copy)]
struct Instance {
    a: u32,
    b: u32,
    c: u32,
}

/// The frontend: the circuit and the verifier's wiring oracle, built once.
struct MulCubeFrontend {
    circuit: LayeredCircuit<BaseField>,
    wiring: DerivedRegularWiring,
}

impl MulCubeFrontend {
    /// Lay out one residual output `a * b + a^3 - c` per instance.
    fn new() -> Result<Self, String> {
        let mut builder = Builder::new(INSTANCES * STRIDE);
        let mut residuals = Vec::new();
        for i in 0..INSTANCES {
            // Every instance is built by the same code inside its own block.
            builder.scope(FAMILY, i);
            let a = builder.input(i * STRIDE);
            let b = builder.input(i * STRIDE + 1);
            let c = builder.input(i * STRIDE + 2);
            let ab = builder.mul(a, b);
            let residual = builder.combine(
                vec![
                    (ab, BaseField::ONE, TapKind::Lin),
                    (a, BaseField::ONE, TapKind::Cube),
                    (c, -BaseField::ONE, TapKind::Lin),
                ],
                BaseField::ZERO,
            );
            residuals.push(residual);
        }
        builder.unscope();
        let (circuit, hints) = builder.build_with_hints(&residuals);
        validate_unary_gates(&circuit).map_err(|error| format!("invalid circuit: {error:?}"))?;
        let wiring = DerivedRegularWiring::derive(&circuit, &hints);
        Ok(Self { circuit, wiring })
    }

    /// The input vector: instance i at wires 4i to 4i + 2, every other wire zero.
    fn inputs(&self, instances: &[Instance]) -> Result<Vec<BaseField>, String> {
        if instances.len() != INSTANCES as usize {
            return Err(format!("expected {INSTANCES} instances, got {}", instances.len()));
        }
        let mut inputs = vec![BaseField::ZERO; 1usize << self.circuit.input_width_bits];
        for (i, instance) in instances.iter().enumerate() {
            let base = i * STRIDE as usize;
            inputs[base] = BaseField::from_u32(instance.a);
            inputs[base + 1] = BaseField::from_u32(instance.b);
            inputs[base + 2] = BaseField::from_u32(instance.c);
        }
        Ok(inputs)
    }

    /// Start a transcript: the domain tag, then the exact circuit, the statement
    /// and the claimed outputs. Prover and verifier absorb identical values.
    fn transcript(
        &self,
        inputs: &[BaseField],
        claimed_outputs: &[BaseField],
    ) -> Result<Transcript, String> {
        let mut transcript = Transcript::new(DOMAIN_TAG);
        observe_circuit(&mut transcript, &self.circuit)?;
        transcript.observe_many(inputs);
        transcript.observe_many(claimed_outputs);
        Ok(transcript)
    }

    /// Prove that every instance satisfies the relation.
    fn prove(&self, instances: &[Instance]) -> Result<GkrProof, String> {
        let inputs = self.inputs(instances)?;
        let witness = evaluate_circuit(&self.circuit, &inputs)
            .map_err(|error| format!("evaluation failed: {error:?}"))?;
        // Residual convention: the statement holds exactly when every output is zero.
        if !is_accepting(&witness) {
            return Err("the statement does not hold for these inputs".to_owned());
        }
        let mut transcript = self.transcript(&inputs, &witness.layer_values[0])?;
        Ok(gkr::prove(&self.circuit, &witness, &mut transcript))
    }

    /// Verify a proof for a statement with the given wiring oracle.
    fn verify_with<W: WiringOracle<ChallengeField>>(
        &self,
        wiring: &W,
        instances: &[Instance],
        proof: &GkrProof,
    ) -> Result<(), String> {
        let inputs = self.inputs(instances)?;
        let output_bits = self
            .circuit
            .layers
            .first()
            .map(|layer| layer.width_bits)
            .ok_or_else(|| "the circuit has no layers".to_owned())?;
        // The verifier supplies its own claim: every residual is zero.
        let claimed_outputs = vec![BaseField::ZERO; 1usize << output_bits];
        let mut transcript = self.transcript(&inputs, &claimed_outputs)?;
        let claim = gkr::verify(&self.circuit, wiring, &claimed_outputs, proof, &mut transcript)
            .map_err(|error| format!("layer reduction rejected: {error:?}"))?;
        // Discharge both residual input claims against the inputs this verifier holds.
        if mle_eval_base(&inputs, &claim.point) != claim.expected_eval {
            return Err("the input claim at x* does not match".to_owned());
        }
        if mle_eval_base(&inputs, &claim.point_y) != claim.expected_eval_y {
            return Err("the input claim at y* does not match".to_owned());
        }
        Ok(())
    }
}

/// Absorb every structural value of the circuit, so a proof refers to this exact circuit.
fn observe_circuit(
    transcript: &mut Transcript,
    circuit: &LayeredCircuit<BaseField>,
) -> Result<(), String> {
    observe_count(transcript, circuit.input_width_bits)?;
    observe_count(transcript, circuit.layers.len())?;
    for layer in &circuit.layers {
        observe_count(transcript, layer.width_bits)?;
        observe_count(transcript, layer.gates.len())?;
        for gate in &layer.gates {
            let kind_tag: usize = match gate.kind {
                GateKind::Lin => 0,
                GateKind::Mul => 1,
                GateKind::Pow3 => 2,
            };
            observe_count(transcript, kind_tag)?;
            observe_count(transcript, gate.out as usize)?;
            observe_count(transcript, gate.in1 as usize)?;
            observe_count(transcript, gate.in2 as usize)?;
            transcript.observe_base(gate.coeff);
        }
        observe_count(transcript, layer.consts.len())?;
        for &(wire, value) in &layer.consts {
            observe_count(transcript, wire as usize)?;
            transcript.observe_base(value);
        }
    }
    Ok(())
}

/// Absorb a count or an index as one field element. A value at or above the
/// field order is refused instead of reduced, because reducing it would alias.
fn observe_count(transcript: &mut Transcript, value: usize) -> Result<(), String> {
    let small = u32::try_from(value)
        .ok()
        .filter(|candidate| *candidate < BaseField::ORDER_U32)
        .ok_or_else(|| format!("structural value {value} does not fit one field element"))?;
    transcript.observe_base(BaseField::from_u32(small));
    Ok(())
}

fn run() -> Result<(), String> {
    let frontend = MulCubeFrontend::new()?;
    let statement = [
        Instance { a: 2, b: 3, c: 14 },
        Instance { a: 3, b: 5, c: 42 },
        Instance { a: 4, b: 1, c: 68 },
        Instance { a: 5, b: 2, c: 135 },
    ];

    let mut proof = frontend.prove(&statement)?;
    // The derived oracle and the general table oracle must both accept.
    frontend.verify_with(&frontend.wiring, &statement, &proof)?;
    frontend.verify_with(&TableWiring::new(&frontend.circuit), &statement, &proof)?;
    println!("honest-proof=PASS");

    // 2 * 3 + 2^3 = 14, so c = 15 makes the first instance false.
    let mut other = statement;
    other[0].c = 15;
    if frontend.prove(&other).is_ok() {
        return Err("the prover accepted a false statement".to_owned());
    }
    println!("false-statement=REFUSED");

    // The honest proof must not verify for a different statement.
    if frontend.verify_with(&frontend.wiring, &other, &proof).is_ok() {
        return Err("the proof verified for another statement".to_owned());
    }
    println!("other-statement=REJECTED");

    // A modified proof must be rejected.
    let first_layer = proof
        .layer_proofs
        .first_mut()
        .ok_or_else(|| "the proof contains no layer proof".to_owned())?;
    first_layer.eval_x += ChallengeField::ONE;
    if frontend.verify_with(&frontend.wiring, &statement, &proof).is_ok() {
        return Err("the tampered proof was accepted".to_owned());
    }
    println!("tampered-proof=REJECTED");
    Ok(())
}

fn main() -> ExitCode {
    match run() {
        Ok(()) => ExitCode::SUCCESS,
        Err(error) => {
            eprintln!("custom-frontend=FAIL: {error}");
            ExitCode::FAILURE
        }
    }
}

Running it prints:

honest-proof=PASS
false-statement=REFUSED
other-statement=REJECTED
tampered-proof=REJECTED

How the program uses the core:

• MulCubeFrontend::new builds one residual output per instance, all in one family. The builder produces two layers: the products together with copies of a and c, and the output layer, where combine adds the product, the cube of a and -c into one wire per instance. The verifier builds this circuit and its wiring oracle itself, never from data that arrives with a proof.
• transcript absorbs the domain tag, the circuit, the whole input vector and the claimed outputs, in that order, on both sides.
• The prover refuses a statement whose residuals are not all zero, because is_accepting rejects the witness before any proving work starts.
• verify_with accepts the honest proof with the derived oracle and with TableWiring. Verifying with both during development checks your layout; in production, one oracle is enough.
• The honest proof is rejected for a changed statement, and a proof with one changed layer evaluation is rejected.

Discharge the residual input claims#

gkr::verify returning Ok(InputClaim) means only that every layer reduction was consistent, down to two claims about the input vector. Acceptance needs both comparisons that verify_with makes: the multilinear extension of the inputs at claim.point must equal claim.expected_eval, and at claim.point_y it must equal claim.expected_eval_y.

• Check point_y as well as point, even when the layer next to the inputs has no Mul gate. The second check costs one more evaluation.
• mle_eval_base folds the entire input vector, so the verifier must hold every input. The engine contains no commitment scheme for input vectors. A verifier that should not hold the inputs needs a separate mechanism that yields trustworthy evaluations of the input at both points, and that mechanism is outside StateSync-GKR and outside its evidence.

Pick a wiring oracle#

gkr::verify evaluates the oracle you pass and does not compare it with circuit. Build the oracle from the verifier's own copy of the circuit, and check a custom implementation against TableWiring on the same circuit before relying on it.

What is fixed#

The sumcheck crate on its own is generic over F: Field. Its verify returns a Subclaim, and the caller must evaluate the summed polynomial at subclaim.point and compare the result with subclaim.expected_eval; as with GKR, Ok alone is not acceptance. Running the core over another field, extension or hash is a new implementation and verification task, and the existing evidence does not carry over to it (Configuration).

What is not included#

• A compiler from programs to circuits. The builder lays out arithmetic graphs that you write.
• A runtime choice of field, extension or hash.
• A commitment scheme for input vectors.
• A proof codec for custom circuits. inner-proof-v1 carries the sparse-Merkle circuit identity (operation tag, tree depth, leaf bound and strategy) and its decoder rejects other values, so it cannot describe another circuit.
• Preparation, request binding and encoding conveniences for custom circuits.

GkrProof has public fields and no serialization of its own. If you define a format, follow the rules of inner-proof-v1: version every axis, carry your circuit identity and your statement, encode each field element canonically and reject values at or above p, give every round polynomial exactly LAYER_ROUND_DEGREE + 1 coefficients and reject any other count, and reject trailing bytes. The in-memory verifier bounds a round polynomial's degree by its coefficient count and also accepts shorter coefficient vectors, so a fixed count in your format is what keeps every absorbed message the same width (Wire format).

Assurance scope#

• The formal results and the published measurements apply to the engine's own circuits: the sparse-Merkle frontend and the generic two-layer circuits of the memory study. See Trust boundaries.
• Your circuit, transcript conventions, input binding and proof format are new work that needs its own review. Formal verification describes what the existing model results cover.

Checklist#

• Lin and Pow3 gates have in2 equal to in1, and validate_unary_gates passes.
• The input vector has exactly 2^input_width_bits entries.
• Prover and verifier absorb the same domain tag, circuit identity, statement and claimed outputs, in the same order, before proving and verifying.
• Structural values are refused, not reduced, when they reach the field order.
• The verifier builds its circuit and wiring oracle from its own description, never from data received with a proof.
• Both residual input claims are checked before a proof counts as accepted.
• Any serialization fixes five coefficients per round polynomial and rejects trailing bytes.

Next steps#

• How GKR works: the protocol behind each step on this page.
• Circuits and layers: how the sparse-Merkle compiler uses the same representation.
• API reference: signatures of the gkr, sumcheck and compiler::builder items.
• Errors: GkrError, SumcheckError, CircuitError and CompileError.