STARK - SNARK recursive proofs

The point of this library is to combine the SNARK and STARK computation arguments of knowledge, namely the Winterfell library for the generation of STARKs and the Circom language, combined with the Groth16 protocol for SNARKs.

They allow the combinaison of advantages of both proof systems:

Groth16 (SNARK): constant-time proofs, constant-time verification, etc.
Winterfell: flexibility of the AIR construct

🗝️ Powers of tau phase 1 transcript

Before anything, a powers of tau phase 1 transcript must be placed in the root of the workspace, named final.ptau.

You can download the ones from the Hermez ceremony here. Hopefully this link will not die.

⚙️ Example Executables

A few example crates are provided as proof-of-concept and usage examples, located in the examples folder.

sum : Computation of the sum of integers from 0 to n.

Each crate contains three executables:

compile: generates and compile Circom code, and generates the circuit-specific keys.
This must be run once before the the other two executables, and every time the proof options are changed.
prove: generate a STARK - SNARK recursive proof.
verify: verify the previously generated proof.

Therefore, the complete execution of the example sum is as follows:

cargo build --release -p example-sum
cargo run --release -p example-sum --bin compile
cargo run --release -p example-sum --bin prove
cargo run --release -p example-sum --bin verify

🪛 Implementing an algorithm

Click to show/hide

This example is available fully-functional in the examples/sum folder.

Define a constant instance of WinterCircomProofOptions, using its new method (see the documentation of this method for what the arguments correspond to).

const PROOF_OPTIONS: WinterCircomProofOptions<2> =
   WinterCircomProofOptions::new(128, 2, 3, [1, 1], 32, 8, 0, 8, 128);

Implement WinterPublicInputs.

use serde::{ser::SerializeTuple, Serialize};
use winter_circom_prover::winterfell::math::fields::f256::BaseElement;

#[derive(Clone, Default)]
pub struct PublicInputs {
    pub start: BaseElement,
    pub start: BaseElement,
}

impl WinterPublicInputs for PublicInputs {
    const NUM_PUB_INPUTS: usize = 2;
}

impl Serialize for PublicInputs {
    fn serialize<S>(&self, serializer: S) -> Result<S::Ok, S::Error>
    where
        S: serde::Serializer,
    {
        let mut state  = serializer.serialize_tuple(2)?;
        state.serialize_element(&self.start)?;
        state.serialize_element(&self.end)?;
        state.end()
    }
}

impl Serializable for PublicInputs {
    fn write_into<W: ByteWriter>(&self, target: &mut W) {
        target.write(self.start);
        target.write(self.result);
    }
}

Implement Winterfell Air trait. See their documentation for instructions.
While writing methods, make sure to use the [WinterCircomProofOptions] constant you previously defined, instead of hard coded values.
Also implement the Default trait for your Air implementation.

use winter_circom_prover::{winterfell::{
    math::{fields::f256::BaseElement, FieldElement},
    Air, AirContext, Assertion, EvaluationFrame, FieldExtension, HashFunction,
    ProofOptions, TraceInfo}};

pub struct WorkAir {
    context: AirContext<BaseElement>,
    start: BaseElement,
    result: BaseElement,
}

impl Air for WorkAir {
    type BaseField = BaseElement;
    type PublicInputs = PublicInputs;

    fn new(trace_info: TraceInfo, pub_inputs: PublicInputs, options: ProofOptions) -> Self {
        let degrees = PROOF_OPTIONS.transition_constraint_degrees();

        let num_assertions = PROOF_OPTIONS.num_assertions();

        WorkAir {
            context: AirContext::new(trace_info, degrees, num_assertions, options),
            start: pub_inputs.start,
            result: pub_inputs.result,
        }
    }

    fn evaluate_transition<E: FieldElement + From<Self::BaseField>>(
        &self,
        frame: &EvaluationFrame<E>,
        _periodic_values: &[E],
        result: &mut [E],
    ) {
        let current = &frame.current();
        let next = &frame.next();

        result[0] = next[0] - (current[0] + E::ONE);
        result[1] = next[1] - (current[1] + current[0] + E::ONE);
    }

    fn get_assertions(&self) -> Vec<Assertion<Self::BaseField>> {
        let last_step = self.trace_length() - 1;
        vec![
            Assertion::single(0, 0, self.start),
            Assertion::single(1, 0, self.start),
            Assertion::single(1, last_step, self.result),
        ]
    }

    fn context(&self) -> &AirContext<Self::BaseField> {
        &self.context
    }
}

impl Default for WorkAir {
    fn default() -> Self {
        WorkAir::new(
            TraceInfo::new(0, 0),
            PublicInputs::default(),
            ProofOptions::new(
                32,
                8,
                0,
                HashFunction::Poseidon,
                FieldExtension::None,
                8,
                128,
            ),
        )
    }
}

Implement the Winterfell Prover trait. See their documentation for instructions.
Also implement a method to build the trace.

use winter_circom_prover::winterfell::{
    math::{fields::f256::BaseElement, FieldElement},
    ProofOptions, Prover, Trace, TraceTable,
};

pub struct WorkProver {
    options: ProofOptions,
}

impl WorkProver {
    pub fn new(options: ProofOptions) -> Self {
        Self { options }
    }

    pub fn build_trace(&self, start: BaseElement, n: usize) -> TraceTable<BaseElement> {
        let trace_width = PROOF_OPTIONS.trace_width;
        let mut trace = TraceTable::new(trace_width, n);

        trace.fill(
            |state| {
                state[0] = start;
                state[1] = start;
            },
            |_, state| {
                state[0] += BaseElement::ONE;
                state[1] += state[0];
            },
        );

        trace
    }
}

impl Prover for WorkProver {
    type BaseField = BaseElement;
    type Air = WorkAir;
    type Trace = TraceTable<Self::BaseField>;

    fn get_pub_inputs(&self, trace: &Self::Trace) -> PublicInputs {
        let last_step = trace.length() - 1;
        PublicInputs {
            start: trace.get(0, 0),
            result: trace.get(1, last_step),
        }
    }

    fn options(&self) -> &ProofOptions {
        &self.options
    }
}

Define AIRTransitions and AIRAssertions Circom templates

Choose a circuit name, for instance: sum.

Create a file named <circuit_name>.circom in the circuits/air/ directory (replace <circuit-name> with the actual circuit name, naturally).

In this file, define two Circom templates:

AIRTransitions - template with a single array output. Hardcode the transition constrait degrees here. In this example, we defined PROOF_OPTIONS with [1, 1] as transition constraint degrees. The template defined below therefore returns [1, 1] as well.
AIRAssertions - template that replicates the get_assertions method of the Air implementation for Winterfell.

Copy the template below and replace the section between /* HERE YOUR ASSERTIONS HERE */ and /* -------------- */ with your own assertions.

For all i between 0 and num_assertions, define value[i], step[i] and register[i] such as the assertion is register[i] at step[i] equals value[i] (a register is a column of the trace).

pragma circom 2.0.0;

include "../utils.circom";

template AIRTransitions(trace_width) {
    signal output transition_degree[trace_width];

    transition_degree[0] <== 1;
    transition_degree[1] <== 1;
}

template AIRAssertions(
    num_assertions,
    num_public_inputs,
    trace_length,
    trace_width
) {
    signal input frame[2][trace_width];
    signal input g_trace;
    signal input public_inputs[num_public_inputs];
    signal input z;

    signal output out[num_assertions];
    signal output divisor_degree[num_assertions];

    signal numerator[num_assertions];
    signal value[num_assertions];
    signal output step[num_assertions];
    signal register[num_assertions];

    /* HERE YOUR ASSERTIONS HERE */

    value[0] <== public_inputs[0];
    step[0] <== 0;
    register[0] <== 0;

    value[1] <== public_inputs[0];
    step[1] <== 0;
    register[1] <== 1;

    value[2] <== public_inputs[1];
    step[2] <== trace_length - 1;
    register[2] <== 1;

    /* ------------------------------------- */

    // boundary constraints evaluation
    component pow[num_assertions];
    component sel[num_assertions];
    for (var i = 0; i < num_assertions; i++) {
        sel[i] = Selector(trace_width);
        for (var j = 0; j < trace_width; j++) {
            sel[i].in[j] <== frame[0][j];
        }
        sel[i].index <== register[i];

        out[i] <== sel[i].out - value[i];
        divisor_degree[i] <== 1;
    }
}

Define executables for compilation, proving and verifying.

See cargo documentation for how to define multiple binaries in a single cargo crate.

All functions are called with a string argument, which should be the circuit name chosen in the previous step.

Compile executable

use winter_circom_prover::{circom_compile, utils::{LoggingLevel, WinterCircomError}};

fn main() -> Result<(), WinterCircomError> {
    circom_compile::<WorkProver, 2>(PROOF_OPTIONS, "sum", LoggingLevel::Default)
}

Prove executable

use winter_circom_prover::{
    circom_prove,
    utils::{LoggingLevel, WinterCircomError},
    winterfell::math::{fields::f256::BaseElement, FieldElement},
};

fn main() -> Result<(), WinterCircomError> {
    // parameters
    let start = BaseElement::ONE;

    // build proof
    let options = PROOF_OPTIONS.get_proof_options();
    let prover = WorkProver::new(options.clone());
    let trace = prover.build_trace(start, PROOF_OPTIONS.trace_length);

    circom_prove(prover, trace, "sum", LoggingLevel::Default)
}

Verify executable

use winter_circom_prover::{
    check_ood_frame, circom_verify,
    utils::{LoggingLevel, WinterCircomError},
};

fn main() -> Result<(), WinterCircomError> {
    check_ood_frame::<WorkAir>("sum");
    circom_verify("sum", LoggingLevel::Verbose)?;

    Ok(())
}

📖 Library

This repo provides a library for the easy generation of STARK - SNARK recursive proofs.

The main components of its API are:

The circom_compile function, for generating a Circom circuit capable of verifying a Winterfell proof, compiling it and generating circuit-specific keys.
The circom_prove function, for generating a SNARK - Groth16 proof of the verification of the Winterfell proof.
The circom_verify function, for verifying the proof generated by the previous function.

Completeness and soundness

The completeness and soundness of arguments of knowledge generated by this crate naturally depends on the completeness and soundness of those generated by the Winterfell library and the Circom language, using the Groth16 protocol.

The generated proofs are complete and sound, assuming the following:

n * lde_blowup_factor < 2^253 where n is the length of the trace.
The Poseidon hash function is used to generate the Winterfell proof.
No field extensions are used.

The generated proofs are composed of a Groth16 proof and a set of public inputs, which are the out-of-domain (OOD) trace frame and the OOD constraint evaluations.

Out-of-domain consistency check

To preserve the flexibility of STARKs compared to the constrained arithmetization of STARKs and especially the Groth16 protocol, the out-of-domain (OOD) consistency check, which requires the evaluations of a user-defined arbitrary function, is done alongside the Circom verification circuit.

The fact that the out-of-domain trace frame and constraint evaluations are consistent is therefore not guaranteed by the Groth16 proof. This is why this crate provides a [check_ood_frame] function, that must be used alongside the [circom_verify] function and which takes the Groth16 public inputs and performs the OOD consistency check.

The [check_ood_frame] verifies that the the OOD trace frame and constraint evaluations correspond to one-another, using the transition constraints defined by the user in their implementation of the Air trait. On top of that, the OOD trace frame is used to reseed the pseudo-random generator. Therefore, modifying the OOD trace frame given as public input to the Groth16 verifier will result in the generation of different query positions, which will result in the failure of Merkle tree commitment checks, with probability at least (1 / trace_width * lde_domain_size) ^ num_queries (the probability that all picked query positions are the same).

This means that verifying the Groth16 proof and the OOD consistency guarantees that the proof is correct. We refer you to the Winterfell and Circom documentations for more details about their respective soundness.

🚀 To-Do

Add support for Winterfell's cyclic assertions.
Implement additional proof-of-concept examples.
Add support for global public inputs, alongside the OOD trace frame and constraint evaluations.
Automate generation of AIRTransitions and AIRAssertions templates.

⚠️ Disclaimer

This library is a research project, has not been audited for safety and should not be used in production.

The circuit-specific keys, generated by the compile executable, do not contain contributions and are therefore unsafe to use in production.

⚖️ License

This work is licensed under the MIT License.

The Winterfell library is licensed under the MIT License.

The Circom and SnarkJS libraries are both licensed under the GNU General Public License v3.0 (see here and here respectively).

victorcolomb / stark-snark-recursive-proofs Goto Github PK