Coder Social home page Coder Social logo

winterfell's Introduction

Winterfell 🐺

A STARK prover and verifier for arbitrary computations.

WARNING: This is a research project. It has not been audited and may contain bugs and security flaws. This implementation is NOT ready for production use.

Overview

A STARK is a novel proof-of-computation scheme to create efficiently verifiable proofs of the correct execution of a computation. The scheme was developed by Eli Ben-Sasson, Michael Riabzev et al. at Technion - Israel Institute of Technology. STARKs do not require an initial trusted setup, and rely on very few cryptographic assumptions. See references for more info.

The aim of this project is to build a feature-rich, easy to use, and highly performant STARK prover which can generate integrity proofs for very large computations. STARK proof generation process is massively parallelizable, however, it also requires lots of RAM. For very large computations, amount of RAM available on a single machine may not be sufficient to efficiently generate a proof. Therefore, our final goal is to efficiently distribute proof generation across many machines.

Status and features

Winterfell is a fully-functional, multi-threaded STARK prover and verifier with the following nice properties:

A simple interface. The library provides a relatively simple interface for describing general computations. See usage for a quick tutorial, air crate for the description of the interface, and examples crate for a few real-world examples.

Randomized AIR support. The library supports multi-stage trace commitments, which enables support for randomized AIR. This greatly increases the expressivity of AIR constraints, and enables, among other things, multiset and permutation checks similar to the ones available in PLONKish systems.

Multi-threaded proof generation. When compiled with concurrent feature enabled, the proof generation process will run in multiple threads. The library also supports concurrent construction of execution trace tables. The performance section showcases the benefits of multi-threading.

Configurable fields. Both the base and the extension field for proof generation can be chosen dynamically. This simplifies fine-tuning of proof generation for specific performance and security targets. See math crate for description of currently available fields.

Configurable hash functions. The library allows dynamic selection of hash functions used in the STARK protocol. Currently, BLAKE3 and SHA3 hash functions are supported, and support for arithmetization-friendly hash function (e.g. Rescue) is planned.

WebAssembly support. The library is written in pure Rust and can be compiled to WebAssembly. The std standard library is enabled as feature by default for both prover and verifier crates. For WASM targets, one can compile with default features disabled by using --no-default-features flag.

Planned features

Over time, we hope extend the library with additional features:

Distributed prover. Distributed proof generation is the main priority of this project, and we hope to release an update containing it soon.

Perfect zero-knowledge. The current implementation provides succinct proofs but NOT perfect zero-knowledge. This means that, in its current form, the library may not be suitable for use cases where proofs must not leak any info about secret inputs.

Project structure

The project is organized into several crates like so:

Crate Description
examples Contains examples of generating/verifying proofs for several toy and real-world computations.
prover Contains an implementation of a STARK prover which can be used to generate computational integrity proofs.
verifier Contains an implementation of a STARK verifier which can verify proofs generated by the Winterfell prover.
winterfell Re-exports prover and verifier crates as a single create for simplified dependency management.
air Contains components needed to describe arbitrary computations in a STARK-specific format.
fri Contains implementation of a FRI prover and verifier. These are used internally by the STARK prover and verifier.
math Contains modules with math operations needed in STARK proof generation/verification. These include: finite field arithmetic, polynomial arithmetic, and FFTs.
crypto Contains modules with cryptographic operations needed in STARK proof generation/verification. Specifically: hash functions and Merkle trees.
utils Contains a set of utility traits, functions, and macros used throughout the library.

Usage

Generating STARK proofs for a computation is a relatively complicated process. This library aims to abstract away most of the complexity, however, the users are still expected to provide descriptions of their computations in a STARK-specific format. This format is called algebraic intermediate representation, or AIR, for short.

This library contains several higher-level constructs which make defining AIRs for computations a little easier, and there are also examples of AIRs for several computations available in the examples crate. However, the best way to understand the STARK proof generation process is to go through a trivial example from start to finish.

First, we'll need to pick a computation for which we'll be generating and verifying STARK proofs. To keep things simple, we'll use the following:

use winterfell::math::{fields::f128::BaseElement, FieldElement};

fn do_work(start: BaseElement, n: usize) -> BaseElement {
    let mut result = start;
    for _ in 1..n {
        result = result.exp(3) + BaseElement::new(42);
    }
    result
}

This computation starts with an element in a finite field and then, for the specified number of steps, cubes the element and adds value 42 to it.

Suppose, we run this computation for a million steps and get some result. Using STARKs we can prove that we did the work correctly without requiring any verifying party to re-execute the computation. Here is how to do it.

First, we need to define an execution trace for our computation. This trace should capture the state of the computation at every step of its execution. In our case, the trace is just a single column of intermediate values after each execution of the loop. For example, if we start with value 3 and run the computation for 1,048,576 (same as 220) steps, the execution trace will look like this:

Step State
0 3
1 69
2 328551
3 35465687262668193
4 237280320818395402166933071684267763523
...
1,048,575 247770943907079986105389697876176586605

To record the trace, we'll use the TraceTable struct provided by the library. The function below, is just a modified version of the do_work() function which records every intermediate state of the computation in the TraceTable struct:

use winterfell::{
    math::{fields::f128::BaseElement, FieldElement},
    TraceTable,
};

pub fn build_do_work_trace(start: BaseElement, n: usize) -> TraceTable<BaseElement> {
    // Instantiate the trace with a given width and length; this will allocate all
    // required memory for the trace
    let trace_width = 1;
    let mut trace = TraceTable::new(trace_width, n);

    // Fill the trace with data; the first closure initializes the first state of the
    // computation; the second closure computes the next state of the computation based
    // on its current state.
    trace.fill(
        |state| {
            state[0] = start;
        },
        |_, state| {
            state[0] = state[0].exp(3u32.into()) + BaseElement::new(42);
        },
    );

    trace
}

Next, we need to define algebraic intermediate representation (AIR) for our computation. This process is usually called arithmetization. We do this by implementing the Air trait. At the high level, the code below does three things:

  1. Defines what the public inputs for our computation should look like. These inputs are called "public" because they must be known to both, the prover and the verifier.
  2. Defines a transition function with a single transition constraint. This transition constraint must evaluate to zero for all valid state transitions, and to non-zero for any invalid state transition. The degree of this constraint is 3 (see more about constraint degrees here).
  3. Define two assertions against an execution trace of our computation. These assertions tie a specific set of public inputs to a specific execution trace (see more about assertions here).

For more information about arithmetization see air crate, and here is the actual code:

use winterfell::{
    math::{fields::f128::BaseElement, FieldElement, ToElements},
    Air, AirContext, Assertion, ByteWriter, EvaluationFrame, ProofOptions, TraceInfo,
    TransitionConstraintDegree,
};

// Public inputs for our computation will consist of the starting value and the end result.
pub struct PublicInputs {
    start: BaseElement,
    result: BaseElement,
}

// We need to describe how public inputs can be converted to field elements.
impl ToElements<BaseElement> for PublicInputs {
    fn to_elements(&self) -> Vec<BaseElement> {
        vec![self.start, self.result]
    }
}

// For a specific instance of our computation, we'll keep track of the public inputs and
// the computation's context which we'll build in the constructor. The context is used
// internally by the Winterfell prover/verifier when interpreting this AIR.
pub struct WorkAir {
    context: AirContext<BaseElement>,
    start: BaseElement,
    result: BaseElement,
}

impl Air for WorkAir {
    // First, we'll specify which finite field to use for our computation, and also how
    // the public inputs must look like.
    type BaseField = BaseElement;
    type PublicInputs = PublicInputs;

    // Here, we'll construct a new instance of our computation which is defined by 3 parameters:
    // starting value, number of steps, and the end result. Another way to think about it is
    // that an instance of our computation is a specific invocation of the do_work() function.
    fn new(trace_info: TraceInfo, pub_inputs: PublicInputs, options: ProofOptions) -> Self {
        // our execution trace should have only one column.
        assert_eq!(1, trace_info.width());

        // Our computation requires a single transition constraint. The constraint itself
        // is defined in the evaluate_transition() method below, but here we need to specify
        // the expected degree of the constraint. If the expected and actual degrees of the
        // constraints don't match, an error will be thrown in the debug mode, but in release
        // mode, an invalid proof will be generated which will not be accepted by any verifier.
        let degrees = vec![TransitionConstraintDegree::new(3)];

        // We also need to specify the exact number of assertions we will place against the
        // execution trace. This number must be the same as the number of items in a vector
        // returned from the get_assertions() method below.
        let num_assertions = 2;

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

    // In this method we'll define our transition constraints; a computation is considered to
    // be valid, if for all valid state transitions, transition constraints evaluate to all
    // zeros, and for any invalid transition, at least one constraint evaluates to a non-zero
    // value. The `frame` parameter will contain current and next states of the computation.
    fn evaluate_transition<E: FieldElement + From<Self::BaseField>>(
        &self,
        frame: &EvaluationFrame<E>,
        _periodic_values: &[E],
        result: &mut [E],
    ) {
        // First, we'll read the current state, and use it to compute the expected next state
        let current_state = &frame.current()[0];
        let next_state = current_state.exp(3u32.into()) + E::from(42u32);

        // Then, we'll subtract the expected next state from the actual next state; this will
        // evaluate to zero if and only if the expected and actual states are the same.
        result[0] = frame.next()[0] - next_state;
    }

    // Here, we'll define a set of assertions about the execution trace which must be satisfied
    // for the computation to be valid. Essentially, this ties computation's execution trace
    // to the public inputs.
    fn get_assertions(&self) -> Vec<Assertion<Self::BaseField>> {
        // for our computation to be valid, value in column 0 at step 0 must be equal to the
        // starting value, and at the last step it must be equal to the result.
        let last_step = self.trace_length() - 1;
        vec![
            Assertion::single(0, 0, self.start),
            Assertion::single(0, last_step, self.result),
        ]
    }

    // This is just boilerplate which is used by the Winterfell prover/verifier to retrieve
    // the context of the computation.
    fn context(&self) -> &AirContext<Self::BaseField> {
        &self.context
    }
}

Next, we need define our prover. This can be done by implementing [Prover] trait. The trait is pretty simple and has just a few required methods. Here is how our implementation could look like:

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

// Our prover needs to hold STARK protocol parameters which are specified via ProofOptions
// struct.
struct WorkProver {
    options: ProofOptions
}

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

// When implementing Prover trait we set the `Air` associated type to the AIR of the
// computation we defined previously, and set the `Trace` associated type to `TraceTable`
// struct as we don't need to define a custom trace for our computation.
impl Prover for WorkProver {
    type BaseField = BaseElement;
    type Air = WorkAir;
    type Trace = TraceTable<Self::BaseField>;
    type HashFn = Blake3_256<Self::BaseField>;

    // Our public inputs consist of the first and last value in the execution trace.
    fn get_pub_inputs(&self, trace: &Self::Trace) -> PublicInputs {
        let last_step = trace.length() - 1;
        PublicInputs {
            start: trace.get(0, 0),
            result: trace.get(0, last_step),
        }
    }

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

Now, we are finally ready to generate a STARK proof. The function below, will execute our computation, and will return the result together with the proof that the computation was executed correctly.

use winterfell::{
    math::{fields::f128::BaseElement, FieldElement},
    FieldExtension, HashFunction, ProofOptions, StarkProof,
};

pub fn prove_work() -> (BaseElement, StarkProof) {
    // We'll just hard-code the parameters here for this example.
    let start = BaseElement::new(3);
    let n = 1_048_576;

    // Build the execution trace and get the result from the last step.
    let trace = build_do_work_trace(start, n);
    let result = trace.get(0, n - 1);

    // Define proof options; these will be enough for ~96-bit security level.
    let options = ProofOptions::new(
        32, // number of queries
        8,  // blowup factor
        0,  // grinding factor
        FieldExtension::None,
        8,   // FRI folding factor
        128, // FRI max remainder length
    );

    // Instantiate the prover and generate the proof.
    let prover = WorkProver::new(options);
    let proof = prover.prove(trace).unwrap();

    (result, proof)
}

We can then give this proof (together with the public inputs) to anyone, and they can verify that we did in fact execute the computation and got the claimed result. They can do this like so:

pub fn verify_work(start: BaseElement, result: BaseElement, proof: StarkProof) {
    // The number of steps and options are encoded in the proof itself, so we
    // don't need to pass them explicitly to the verifier.
    let pub_inputs = PublicInputs { start, result };
    match winterfell::verify::<WorkAir, Blake3_256<Self::BaseField>>(proof, pub_inputs) {
        Ok(_) => println!("yay! all good!"),
        Err(_) => panic!("something went terribly wrong!"),
    }
}

That's all there is to it! As mentioned above, the examples crate contains examples of much more interesting computations (together with instructions on how to compile and run these examples). So, do check it out.

Performance

The Winterfell prover's performance depends on a large number of factors including the nature of the computation itself, efficiency of encoding the computation in AIR, proof generation parameters, hardware setup etc. Thus, the benchmarks below should be viewed as directional: they illustrate the general trends, but concrete numbers will be different for different computations, choices of parameters etc.

The computation we benchmark here is a chain of Rescue hash invocations (see examples for more info). The benchmarks were run on Intel Core i9-9980KH @ 2.4 GHz and 32 GB of RAM using all 8 cores.

Chain length Trace time 96 bit security 128 bit security R1CS equiv.
Proving time Proof size Proving time Proof size
210 0.1 sec 0.04 sec 51 KB 0.07 sec 102 KB 218 constr.
212 0.4 sec 0.14 sec 65 KB 0.25 sec 128 KB 220 constr.
214 1.4 sec 0.6 sec 80 KB 1 sec 156 KB 222 constr.
216 6 sec 2.5 sec 94 KB 4 sec 184 KB 224 constr.
218 24 sec 11 sec 112 KB 18 sec 216 KB 226 constr.
220 94 sec 50 sec 128 KB 89 sec 252 KB 228 constr.

A few remarks about these benchmarks:

  • Trace time is the time it takes to generate an execution trace for the computation. This time does not depend on the chosen security level. For this specific computation, trace generation must be sequential, and thus, cannot take advantage of multiple cores. However, for other computations, where execution trace can be generated in parallel, trace time would be much smaller in relation to the proving time (see below).
  • R1CS equiv. is a very rough estimate of how many R1CS constraints would be required for this computation. The assumption here is that a single invocation of Rescue hash function requires ~250 R1CS constraints.
  • Not included in the table, the time it takes to verify proofs in all benchmarks above is between 2 ms and 6 ms using a single CPU core.
  • As can be seen from the table, with STARKs, we can dynamically trade off proof size, proof security level, and proving time against each other.

Let's benchmark another example. This time our computation will consist of verifying many Lamport+ signatures (see example). This is a much more complicated computation. For comparison, execution trace for Rescue hash chain requires only 4 columns, but for Lamport+ signature verification we use 22 columns. The table below shows benchmarks for verifying different numbers of signatures on the same 8-core machine (at 123-bit security level).

# of signatures Trace time Proving time Prover RAM Proof size Verifier time
64 0.2 sec 1.2 sec 0.5 GB 110 KB 4.4 ms
128 0.4 sec 2.6 sec 1.0 GB 121 KB 4.4 ms
256 0.8 sec 5.3 sec 1.9 GB 132 KB 4.5 ms
512 1.6 sec 10.9 sec 3.8 GB 139 KB 4.9 ms
1024 3.2 sec 20.5 sec 7.6 GB 152 KB 5.9 ms

A few observations about these benchmarks:

  • Trace time and prover RAM (RAM consumed by the prover during proof generation) grow pretty much linearly with the size of the computation.
  • Proving time grows very slightly faster than linearly with the size of the computation.
  • Proof size and verifier time grow much slower than linearly (actually logarithmically) with the size of the computation.

Another difference between this example and Rescue hash chain is that we can generate execution trace for each signature verification independently, and thus, we can build the entire trace in parallel using multiple threads. In general, Winterfell prover performance scales nearly linearly with every additional CPU core. This is because nearly all steps of STARK proof generation process can be parallelized. The table below illustrates this relationship on the example of verifying 1024 Lamport+ signatures (at 123-bit security level). This time, our benchmark machine is AMD EPYC 7003 with 64 CPU cores.

Threads Trace time Proving time Total time (trace + proving) Improvement
1 28 sec 127 sec 155 sec 1x
2 14 sec 64 sec 78 sec 2x
4 6.7 sec 33 sec 39.7 sec 3.9x
8 3.8 sec 17 sec 20.8 sec 7.5x
16 2 sec 10.3 sec 12.3 sec 12.6x
32 1 sec 6 sec 7 sec 22.1x
64 0.6 sec 3.8 sec 4.4 sec 35.2x

References

If you are interested in learning how STARKs work under the hood, here are a few links to get you started. From the standpoint of this library, arithmetization is by far the most important concept to understand.

Vitalik Buterin's blog series on zk-STARKs:

Alan Szepieniec's STARK tutorial:

StarkWare's STARK Math blog series:

License

This project is MIT licensed.

Acknowledgements

The original codebase was developed by Irakliy Khaburzaniya (@irakliyk) with contributions from François Garillot (@huitseeker), Kevin Lewi (@kevinlewi), Konstantinos Chalkias (@kchalkias), and Jasleen Malvai (@Jasleen1).

winterfell's People

Contributors

0xkanekiken avatar abhi3700 avatar al-kindi-0 avatar andrewmilson avatar armfazh avatar eigmax avatar frisitano avatar grjte avatar hackaugusto avatar irakliyk avatar itzmeanjan avatar jasleen1 avatar jimpo avatar kchalkias avatar matthiasgoergens avatar nashtare avatar plafer avatar vlopes11 avatar

Stargazers

 avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar

Watchers

 avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar

winterfell's Issues

More efficient remainder verification in FRI

Currently, the last step in FRI verification is https://github.com/novifinancial/winterfell/blob/e43b75d365e03a71288ede25a6c2c9d9dc021a4d/fri/src/verifier/mod.rs#L307-L319

This is inefficient in, at least, two ways:

  1. The commitment to the remainder is a Merkle tree. This is inefficient because we don't really use the property of vector-commitment that a Merkle tree provides in the above implementation and we can in fact get away with the weaker notion of set-commitment, provided the set is composed of elements of the form (position,remainder[position]).
  2. Combined with the previous point, the verifier can, instead of checking that remainder[position] == evaluation, just compute the set commitment to (position,evaluations[position]) and then check that the two set-commitments are equal. This assumes that the queries at the initial layer are drawn in such a way so as the last folded positions span the range [0, remainder.len() - 1] . I assume this is already implemented in Winterfell but I haven't checked.

As for the set-commitment, a sequential hash of remainder[i] for $i$ in increasing order might be sufficient.

Potential vulnerability if not checking proof security level

This issue was brought up by Quan Thoi Minh Nguyen from Google.

The core of the issue is how we define the verifier interface here. Basically, the verifier accepts a StarkProof as an input and StarkProof struct contains ProofOptions struct. In turn, ProofOptions contains a bunch of protocol parameters which, in the end, define the security level of the proof. This setup could allow a potential attacker to send a fake proof at a very low security level (e.g., just a few bits), and the verifier would accept this proof.

So, it is up to the users of this library to make sure they check security level of the proof before passing it to the verify() function. While this works, it is probably not ideal as people might forget that this needs to be done leading to unintended concequences.

I can think of 3 ways of changing the verifier interface to make this type of bugs less likely.

Option 1: return security level from the verify() function

We could change the signature of the verify() function to something like this:

pub fn verify<AIR: Air, HashFn: ElementHasher<BaseField = AIR::BaseField>>(
    proof: StarkProof,
    pub_inputs: AIR::PublicInputs,
) -> Result<u32, VerifierError>

Where the returned u32 would specify the security level of the verified proof.

Option 2: pass ProofOptions struct separately

We could change the signature of the verify() function to something like this:

pub fn verify<AIR: Air, HashFn: ElementHasher<BaseField = AIR::BaseField>>(
    proof: StarkProof,
    options: ProofOptions,
    pub_inputs: AIR::PublicInputs,
) -> Result<(), VerifierError>

This would also require the we remove ProofOptions from StarkProof.

Option 3: specify minimum security level

We could change the signature of the verify() function to something like this:

pub fn verify<AIR: Air, HashFn: ElementHasher<BaseField = AIR::BaseField>>(
    proof: StarkProof,
    pub_inputs: AIR::PublicInputs,
    min_security_level: u32,
) -> Result<(), VerifierError>

My thinking is that option 1 is not really explicit enough and the return value could be ignored by the caller just as easily. Option 2 makes the interface less ergonomic and difficult to use, in my opinion. So, my preference would be with option 3 - but would love to know if others think differently.

[crypto] Rescue hash function

Implementing high-performance version of Rescue hash function would be the first step towards recursive STARKs. Target performance should be 100K+ hashes (64B -> 32B) per second.

To achieve such level of performance, we would need to implement Rescue in a small (~64-bit) field. Description of Rescue hash function can be found here:

Potential parameters (for ~128-bit security level) could be:

  • Filed size: ~64-bits
  • State width: 12 elements
  • S-box degree: 3, 5, or 7 (depends on the chose field)
  • Number of rounds: 7

We could also expose this implementation as two different variants: one with 4 field element output (~128 bit collision resistance) and 3 field element output (96-bit collision resistance). Although, it may be better to have a separate implementation for 96-bit version as that could be instantiated with a state width of 9 elements, and thus should be noticeably faster than the one using 12 elements.

Fix `--no-default-features` build

winter-utils is failing to build with --no-default-features for all targets.

Vec should be pulled from super, and not from prelude, as they will not be available by default under no-std.

merkle consistency proofs

It doesn't look like the merkle crate supports consistency proofs between two different trees, but it does support (batched) inclusion proofs for leaves. Would y'all be open to adding consistency proof support?

Does `Air::get_deep_composition_coefficients` assume that the proof is generated using an extension field?

This is not a real bug because I guess is at most generating an extra unused random coefficient.
https://github.com/novifinancial/winterfell/blob/10a5f5ad90592889fe977c505012cd9f2159fb23/air/src/air/mod.rs#L512
In this line 3 coefficients are sampled for each trace polynomial: \alpha_i for the trace opening to z, \beta_i for the opening to g*z, and \gamma_i for showing that the trace poly is defined over the base field. If we are not working over an extension field then we don't need to prove the third statement. I guess this is not a big problem because, at most, the extra coefficient never gets read.

Supporting RAPs

Hi,

First, this is a really nice project. Thank you!

Onto my question: the recent Cairo paper describes using Randomized AIRs with Preprocessing (RAPs) for Cairo's memory. While they don't describe in detail how they modify the STARK protocol, it appears to allow the prover to first commit to a set of trace columns, then use that commitment to generate randomness that can be used in an additional set of trace columns. The main use case here is that with such capability, local constraints (as in AIR) can be used to verify global properties (such as that one column is a permutation of another, which is what is done in Cairo's memory).

Is this of interest to anyone here? I'd really appreciate some pointers or advice on how the API for winterfell might be best modified to support this. Of course, if the modifications are of use to anyone here I'd be happy to contribute them.

Thanks and have a nice weekend

Migrate to new MerkleTree implementation

A new MerkleTree has already been implemented but it is not yet integrated into the rest of the library. Migrating to this new implementation will allow us to relax the condition that hash function output must be 32 bytes.

[FRI] First FRI layer handling

Right now, we include first FRI layer into the FRI proof. This is redundant as the verifier can compute the values for the first FRI layer directly from trace and constraint queries. Removing first FRI layer from the proof should reduce of proof size roughly by 15%.

However, we can do this only when perfect zero knowledge is not required. When we implement ability to turn on perfect zero knowledge (via #9), we would need to include first FRI layer queries into the FRI proof. So, it probably makes sense to address this issue once #9 has been addressed.

v0.7 release goals

For v0.7 release I'm thinking of adding the following to the library:

  • #180
  • #181
  • Add support for validity constraints (i.e., constraints which hold on every step of execution trace).
  • #206
  • #160

Suggestions/comments are welcome.

Field security origin?

In the conjectured security evaluation, we have:
let field_security = field_size - lde_domain_size.trailing_zeros();
( i.e. $\lambda \leq \log_2(\mathbb{K}) - \log_2(D)$ ) which bounds the security level of a given STARK proof by the bit size of the extension field on which we operate minus the bit size of the execution trace (after extension).
This conflicts with the conjectured security formulae given in EthSTARK paper, page 40, where for the field security we only consider the size of the extension field.

I was then wondering where this $- \log(D)$ was coming from? Would it have a link with the much more complex formula for proven security?

If that is the case, then wouldn't it make sense to stick to the "conjectured field security" estimate for the conjectured security level?

[FRI] Dynamic layer folding

Right now, we specify a single folding factor for all FRI layers. Out of supported folding factors (4, 8, 16), it seems like 8 results in the smallest proof in most situations. However, it might be possible to optimize this even further by using different folding factors across different layers. I wouldn't expect the impact to be huge - but getting something around 5% proof size reduction may be possible.

One way to go about this is to deterministically create a schedule of folding factors based on extended domain size, and field element size, and hash function digest size. This schedule can then be provided as an input to FRI prover/verifier.

Support custom implementations of Trace LDE

Currently, Trace LDE is implemented as a concrete struct (see here). It might be good to instead define as a trait and provide a default implementation (similar to what we did with RandomCoin recently). Making it a trait would make the structure more flexible and allow for custom implementations of Trace LDE which might be more suitable for various use cases (i.e., long-running provers where memory may not need to be allocated/de-allocated all the time, or provers which outsource LDE computations to hardware etc.).

The trait could look something like this:

pub trait TraceLde {
    type BaseField: StarkField;
    type HashFn: ElementHasher<BaseField = Self::BaseField>;

    /// Takes main trace columns as input, interpolates them into polynomials in coefficient form,
    /// evaluates the polynomials over the LDE domain, and commits to the polynomial evaluations.
    ///
    /// Returns a tuple containing the column polynomials in coefficient from and the commitment
    /// to the polynomial evaluations over the LDE domain.
    fn set_main_trace(
        main_trace: &ColMatrix<Self::BaseField>,
    ) -> (ColMatrix<Self::BaseField>, <Self::HashFn as Hasher>::Digest);

    /// Takes auxiliary trace segment columns as input, interpolates them into polynomials in
    /// coefficient form, evaluates the polynomials over the LDE domain, and commits to the
    /// polynomial evaluations.
    ///
    /// Returns a tuple containing the column polynomials in coefficient from and the commitment
    /// to the polynomial evaluations over the LDE domain.
    fn add_aux_segment<E: FieldElement<BaseField = Self::BaseField>>(
        aux_trace: &ColMatrix<E>,
    ) -> (ColMatrix<E>, <Self::HashFn as Hasher>::Digest);

    /// Reads current and next rows from the main trace segment into the specified frame.
    fn read_main_trace_frame_into(
        &self,
        lde_step: usize,
        frame: &mut EvaluationFrame<Self::BaseField>,
    );

    /// Reads current and next rows from the auxiliary trace segment into the specified frame.
    fn read_aux_trace_frame_into<E: FieldElement<BaseField = Self::BaseField>>(
        &self,
        lde_step: usize,
        frame: &mut EvaluationFrame<E>,
    );

    /// Returns trace table rows at the specified positions along with Merkle authentication paths
    /// from the commitment root to these rows.
    fn query(&self, positions: &[usize]) -> Vec<Queries>;

    /// Returns the number of rows in the execution trace.
    fn trace_len(&self) -> usize;

    /// Returns blowup factor which was used to extend original execution trace into trace LDE.
    fn blowup(&self) -> usize;
}

Creating an instances of TraceLde would be handled by the prover. To do this, we'd need to add the following to the Prover trait:

pub trait Prover {
    ...
    type TraceLde: TraceLde<BaseField = Self::BaseField>,

    fn new_trace_lde(&self, trace_info: &TraceInfo, blowup: usize) -> Self::TraceLde;
}

This structure can be further improved by abstracting away evaluations frame behind an associated and replacing read_* methods with some sort of a frame iterator (which would be helpful for #80). But I'm leaving this for a separate issue.

Build fails with concurrent feature

PR #124 broke the build using concurrent feature, by changing the scope of the fft_in_place function (originally in fft/serial module) to private, and moving it to the fft/fft_inputs module without updating the calls in the fft/concurrent module.

I think this already happened in the past that a change breaking builds with parallelization went unnoticed in the main branch, perhaps we should consider having a check in the CI?

Abstract away Merkle trees with VectorCommitment scheme

We currently make a hard assumption that for vector commitments (i.e., trace LDE commitment, constraint evaluation commitment, FRI layer commitments etc.) Merkle trees are used. It would be nice to abstract this assumption away and provide a way for the user to specify which vector commitment type to use.

This would help with such things as #38 and also would make #9 simpler as we could provide SaltedMerkleTree as one of the vector commitment types.

To make vector commitments fully generic, we could use something like this:

pub trait VectorCommitment: Sized {
    type Options;
    type Item: Clone + Serializable + Deserializable;
    type Commitment: Copy + Serializable + Deserializable;
    type Proof: Clone + Serializable + Deserializable;
    type MultiProof: Clone + Serializable + Deserializable;
    type Error: Debug;

    fn new(items: Vec<Self::Item>, options: Self::Options) -> Result<Self, Self::Error>;

    fn commitment(&self) -> Self::Commitment;

    fn open(&self, index: usize) -> Result<(Self::Item, Self::Proof), Self::Error>;
    fn open_many(&self, indexes: &[usize]) -> Result<(Vec<Self::Item>, Self::MultiProof), Self::Error>;

    fn verify(
        commitment: Self::Commitment,
        index: usize,
        item: Self::Item,
        proof: &Self::Proof
    ) -> Result<(), Self::Error>;

    fn verify_many(
        commitment: Self::Commitment,
        indexes: &[usize],
        items: &[Self::Item],
        proof: &Self::MultiProof
    ) -> Result<(), Self::Error>;
}

The first step for implementing this is probably to update our current MerkleTree implementation to comply with this interface.

Question about getting avoid of `panic` in the generated wasm binary

Hi there. I'm working on a blockchain-related project which uses winterfell and I need to compile my code to WebAssembly, so that it can be executed on an EVM-compatible runtime.

I found that the generated wasm binary imports core::panicking::panic somehow, even if panic = "abort" is enabled:

> wasm-dis wasm32-unknown-unknown/release/contract.wasm | grep "import.*panic"
 (import "env" "_ZN4core9panicking5panic17h6619a393253f8e08E" (func $_ZN4core9panicking5panic17h6619a393253f8e08E (param i32 i32 i32)))

And this function is called by $_ZN17compiler_builtins3int5shift4Ashl4ashl17h85b84ee9c80145b7E, which is called by $_ZN17compiler_builtins3int5shift9__ashlti317hbfcf8d3fd2119232E, which is called by $__ashlti3, which is called by $_ZN11winter_math5field6traits10StarkField17get_root_of_unity17hc9d7430c89370043E.

And here is $_ZN11winter_math5field6traits10StarkField17get_root_of_unity17hc9d7430c89370043E:
https://github.com/novifinancial/winterfell/blob/f89e6c1011a9e3f42667905e94b81265d8999dae/math/src/field/traits.rs#L218-L227

So I guess rustc has some internal checks to ensure that the shl operation doesn't overflow, which always call panic.

I made the following change, and the compiled wasm no longer imports panic.

- let power = Self::PositiveInteger::from(1u32) << (Self::TWO_ADICITY - n);
- Self::TWO_ADIC_ROOT_OF_UNITY.exp(power)
+ let power = 1u64 << (Self::TWO_ADICITY - n); // `TWO_ADICITY` is 39 in f62, and 40 in f128, so u64 is sufficient (?)
+ Self::TWO_ADIC_ROOT_OF_UNITY.exp(Self::PositiveInteger::from(power))

Since I am a beginner both to rust and winterfell, I am wondering whether my modified code works in the same way.

If it makes sense, I am willing to submit a pull request.

Proposal: Extending StarkField to any finite field with large 2-adicity

We currently only allow prime finite fields to implement the StarkField trait. However, I believe that the library would benefit greatly from relaxing this requirement to any finite field, given that they still have large 2-adicity.

In particular, I have in mind adding support for Mersenne prime fields, for the following reason:

  • really fast arithmetic (see for example alg. 1 in https://eprint.iacr.org/2020/665.pdf). Concrete comparison is available in the Virgo paper, table 1, where operations over $\mathbb{F}_p^2$ with $p = 2^{61} - 1$ are respectively 1.76x faster for addition and 1.13x slower (only) for multiplication, compared to $\mathbb{F}_2^{64}$.
  • quadratic extensions of Mersenne prime fields $\mathbb{F}_p$ always have 2-adicity $n$ for $n = \log_2(p)$
  • quadratic extensions of Mersenne prime fields can be defined as the complex field with modulus $X^2 + 1$, allowing efficient quadratic multiplication.

What's more, for Mersenne prime fields that would be of interesting size for STARKs:

  • $\mathbb{F}_{2^{127} - 1}^2$ would allow for up to 128 bits of security even in the proven security case (see #122, #151), without needing for extra extension.

  • The same field would allow support for FourQ) curve, adding efficient curve support for applications that may need it (I haven't done comparisons with ecgfp5 over f64 so I don't know by how much FourQ is more efficient).

  • Also the prime field $\mathbb{F}_{2^{127} - 1}$ can use $\alpha = 5$ for S-Boxes.

  • $\mathbb{F}_{2^{61} - 1}^2$ would probably be faster than the current f64, as the paper comparison was done over the binary field of same size. Unfortunately, the smallest $\alpha$ for S-Boxes is 17, which would require heavier arithmetization of hash functions for cells being exponentiated by $\alpha$, although this can be somehow alleviated (we could split the exponentiation of one cell over two cells with constraint degree 4 and 5).

  • $\mathbb{F}_{2^{31} - 1}^2$ would have base prime field elements fit in u32, which could come in handy if (or when) GPU support is added to Winterfell (which I believe, @irakliyk feel free to correct me on this, will come sooner or later, whether through generic libraries or dedicated ones), especially as GPU register sizes are 32 bits.

  • In addition, hashing throughput of algebraic hashes over the primefield $\mathbb{F}_{2^{31} - 1}$ should be higher than with larger fields. What's more, S-Boxes on this primefield can use $\alpha = 5$.

[FRI] Use Queries struct in FriProof

We should refactor FriProof struct to rely on Queries struct for internal representation of queries. This will unify serialization/deserialization approaches. But, it will also require moving Queries struct into utils crate, since fri crate does not depend on common crate.

Port Examples To Separate Repository.

Hi,

Could you port the examples folder to a different repository so it is easier to use. I am trying to use it and it has been a bit difficult to use. It would be much easier if you had a separate repository for examples.

A reference that has done this can be found here.

Thank you and thank you so much for the project. Very useful!

Custom evaluation frames

Some AIR constraints cannot be expressed as functions involving just two consecutive rows of trace registers. An example of such a constraint is found in the Cairo whitepaper, where a multi-set permutation check is used to ensure that memory is continuous and read-only. This constraint checks address-value pairs for four different pointer types (pc, dst, op0, op1). When these pointers are located in the same trace row, it is not possible to implement the required cumulative product step constraint for nontrivial programs, as memory accesses for more than one pointer type can occur in a single execution step and are not broken down into individual rows. Thus when we specify additional auxiliary columns for all of the various address-value pairs (regardless of pointer type, and sorted by address) there will be a mismatch in trace length. While sorted address-value columns could be constructed for each pointer type, and continuity constraints could be modified to ensure that memory accesses restricted to a specific pointer type are read-only, it does not appear possible to ensure that the same memory accesses across different pointer types also remain read-only. To solve this issue, the Cairo whitepaper introduces "virtual columns" and "subcolumns" (page 49) to allow for larger evaluation frames that effectively provide non-overlapping windows of the execution trace.

With the above in mind, a simple modification of the current frame implementation could allow for larger window sizes, and otherwise seek to keep the interface the same. We could split the current EvaluationFrame struct into an EvaluationFrame trait and ConsecutiveEvaluationFrame struct implementing this trait (similar to how ExecutionTrace was split in a previous pull request). The ConsecutiveEvaluationFrame (there is probably a better name) will have the same functionality as the current struct (it has a window size of 1), and remain in use for both the two OOD point evaluations and for AIR transition evaluations that only need the current and next row. Users that need a larger window for their transition function (e.g. the current 4 rows and next 4 rows) can create a custom struct satisfying the trait. It might also make sense to allow for the current and next functions to have differing windows sizes. I think at a minimum we will need to modify the evaluate_fragment function in ConstraintEvaluator and the read_main_trace_frame_into function in TraceLde.

When is distributed proving coming?

Our README says:

Therefore, our final goal is to efficiently distribute proof generation across many machines.

What's the current status of distributed proving? What are the plans?

Unable to compile examples

vadym@ubuntu:~/winterfell$ cargo build --release --manifest-path examples/Cargo.toml --features concurrent
  Downloaded crossbeam-epoch v0.9.5
  Downloaded memoffset v0.6.4
  Downloaded rayon-core v1.9.1
  Downloaded crossbeam-utils v0.8.5
  Downloaded rayon v1.5.1
  Downloaded crossbeam-deque v0.8.1
  Downloaded crossbeam-channel v0.5.1
  Downloaded 7 crates (423.1 KB) in 0.75s
   Compiling autocfg v1.0.1
   Compiling crossbeam-utils v0.8.5
   Compiling crossbeam-epoch v0.9.5
   Compiling scopeguard v1.1.0
   Compiling rayon-core v1.9.1
   Compiling either v1.6.1
   Compiling num_cpus v1.13.0
   Compiling structopt v0.3.25
   Compiling memoffset v0.6.4
   Compiling rayon v1.5.1
   Compiling crossbeam-channel v0.5.1
   Compiling crossbeam-deque v0.8.1
   Compiling winter-utils v0.2.0 (/home/vadym/winterfell/utils/core)
   Compiling winter-math v0.2.0 (/home/vadym/winterfell/math)
   Compiling winter-rand-utils v0.2.0 (/home/vadym/winterfell/utils/rand)
   Compiling winter-crypto v0.2.0 (/home/vadym/winterfell/crypto)
error[E0277]: `[B; N]` is not an iterator
  --> crypto/src/hash/rescue/mod.rs:23:27
   |
23 |     result.iter_mut().zip(tail).for_each(|(r, t)| *r *= t);
   |                           ^^^^
   |                           |
   |                           expected an implementor of trait `IntoIterator`
   |                           help: consider borrowing here: `&tail`
   |
   = note: the trait bound `[B; N]: IntoIterator` is not satisfied
   = note: required because of the requirements on the impl of `IntoIterator` for `[B; N]`

error[E0599]: the method `for_each` exists for struct `std::iter::Zip<std::slice::IterMut<'_, B>, [B; N]>`, but its trait bounds were not satisfied
  --> crypto/src/hash/rescue/mod.rs:23:33
   |
23 |     result.iter_mut().zip(tail).for_each(|(r, t)| *r *= t);
   |                                 ^^^^^^^^ method cannot be called on `std::iter::Zip<std::slice::IterMut<'_, B>, [B; N]>` due to unsatisfied trait bounds
   | 
  ::: /home/vadym/snap/rustup/common/rustup/toolchains/stable-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/iter/adapters/zip.rs:13:1
   |
13 | pub struct Zip<A, B> {
   | -------------------- doesn't satisfy `_: Iterator`
   |
   = note: the following trait bounds were not satisfied:
           `[B; N]: Iterator`
           which is required by `std::iter::Zip<std::slice::IterMut<'_, B>, [B; N]>: Iterator`
           `std::iter::Zip<std::slice::IterMut<'_, B>, [B; N]>: Iterator`
           which is required by `&mut std::iter::Zip<std::slice::IterMut<'_, B>, [B; N]>: Iterator`

error[E0277]: `[[winter_math::fields::f62::BaseElement; 12]; 12]` is not an iterator
   --> crypto/src/hash/rescue/rp62_248/mod.rs:262:27
    |
262 |     result.iter_mut().zip(MDS).for_each(|(r, mds_row)| {
    |                           ^^^
    |                           |
    |                           expected an implementor of trait `IntoIterator`
    |                           help: consider borrowing here: `&MDS`
    |
    = note: the trait bound `[[winter_math::fields::f62::BaseElement; 12]; 12]: IntoIterator` is not satisfied
    = note: required because of the requirements on the impl of `IntoIterator` for `[[winter_math::fields::f62::BaseElement; 12]; 12]`

error[E0599]: the method `for_each` exists for struct `std::iter::Zip<std::slice::IterMut<'_, winter_math::fields::f62::BaseElement>, [[winter_math::fields::f62::BaseElement; 12]; 12]>`, but its trait bounds were not satisfied
   --> crypto/src/hash/rescue/rp62_248/mod.rs:262:32
    |
262 |     result.iter_mut().zip(MDS).for_each(|(r, mds_row)| {
    |                                ^^^^^^^^ method cannot be called on `std::iter::Zip<std::slice::IterMut<'_, winter_math::fields::f62::BaseElement>, [[winter_math::fields::f62::BaseElement; 12]; 12]>` due to unsatisfied trait bounds
    | 
   ::: /home/vadym/snap/rustup/common/rustup/toolchains/stable-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/iter/adapters/zip.rs:13:1
    |
13  | pub struct Zip<A, B> {
    | -------------------- doesn't satisfy `_: Iterator`
    |
    = note: the following trait bounds were not satisfied:
            `[[winter_math::fields::f62::BaseElement; 12]; 12]: Iterator`
            which is required by `std::iter::Zip<std::slice::IterMut<'_, winter_math::fields::f62::BaseElement>, [[winter_math::fields::f62::BaseElement; 12]; 12]>: Iterator`
            `std::iter::Zip<std::slice::IterMut<'_, winter_math::fields::f62::BaseElement>, [[winter_math::fields::f62::BaseElement; 12]; 12]>: Iterator`
            which is required by `&mut std::iter::Zip<std::slice::IterMut<'_, winter_math::fields::f62::BaseElement>, [[winter_math::fields::f62::BaseElement; 12]; 12]>: Iterator`

error[E0277]: `[winter_math::fields::f62::BaseElement; 12]` is not an iterator
   --> crypto/src/hash/rescue/rp62_248/mod.rs:311:26
    |
311 |     state.iter_mut().zip(acc).for_each(|(s, a)| *s *= a);
    |                          ^^^
    |                          |
    |                          expected an implementor of trait `IntoIterator`
    |                          help: consider borrowing here: `&acc`
    |
    = note: the trait bound `[winter_math::fields::f62::BaseElement; 12]: IntoIterator` is not satisfied
    = note: required because of the requirements on the impl of `IntoIterator` for `[winter_math::fields::f62::BaseElement; 12]`

error[E0599]: the method `for_each` exists for struct `std::iter::Zip<std::slice::IterMut<'_, winter_math::fields::f62::BaseElement>, [winter_math::fields::f62::BaseElement; 12]>`, but its trait bounds were not satisfied
   --> crypto/src/hash/rescue/rp62_248/mod.rs:311:31
    |
311 |     state.iter_mut().zip(acc).for_each(|(s, a)| *s *= a);
    |                               ^^^^^^^^ method cannot be called on `std::iter::Zip<std::slice::IterMut<'_, winter_math::fields::f62::BaseElement>, [winter_math::fields::f62::BaseElement; 12]>` due to unsatisfied trait bounds
    | 
   ::: /home/vadym/snap/rustup/common/rustup/toolchains/stable-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/iter/adapters/zip.rs:13:1
    |
13  | pub struct Zip<A, B> {
    | -------------------- doesn't satisfy `_: Iterator`
    |
    = note: the following trait bounds were not satisfied:
            `[winter_math::fields::f62::BaseElement; 12]: Iterator`
            which is required by `std::iter::Zip<std::slice::IterMut<'_, winter_math::fields::f62::BaseElement>, [winter_math::fields::f62::BaseElement; 12]>: Iterator`
            `std::iter::Zip<std::slice::IterMut<'_, winter_math::fields::f62::BaseElement>, [winter_math::fields::f62::BaseElement; 12]>: Iterator`
            which is required by `&mut std::iter::Zip<std::slice::IterMut<'_, winter_math::fields::f62::BaseElement>, [winter_math::fields::f62::BaseElement; 12]>: Iterator`

error[E0277]: `[[winter_math::fields::f64::BaseElement; 12]; 12]` is not an iterator
   --> crypto/src/hash/rescue/rp64_256/mod.rs:262:27
    |
262 |     result.iter_mut().zip(MDS).for_each(|(r, mds_row)| {
    |                           ^^^
    |                           |
    |                           expected an implementor of trait `IntoIterator`
    |                           help: consider borrowing here: `&MDS`
    |
    = note: the trait bound `[[winter_math::fields::f64::BaseElement; 12]; 12]: IntoIterator` is not satisfied
    = note: required because of the requirements on the impl of `IntoIterator` for `[[winter_math::fields::f64::BaseElement; 12]; 12]`

error[E0599]: the method `for_each` exists for struct `std::iter::Zip<std::slice::IterMut<'_, winter_math::fields::f64::BaseElement>, [[winter_math::fields::f64::BaseElement; 12]; 12]>`, but its trait bounds were not satisfied
   --> crypto/src/hash/rescue/rp64_256/mod.rs:262:32
    |
262 |     result.iter_mut().zip(MDS).for_each(|(r, mds_row)| {
    |                                ^^^^^^^^ method cannot be called on `std::iter::Zip<std::slice::IterMut<'_, winter_math::fields::f64::BaseElement>, [[winter_math::fields::f64::BaseElement; 12]; 12]>` due to unsatisfied trait bounds
    | 
   ::: /home/vadym/snap/rustup/common/rustup/toolchains/stable-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/iter/adapters/zip.rs:13:1
    |
13  | pub struct Zip<A, B> {
    | -------------------- doesn't satisfy `_: Iterator`
    |
    = note: the following trait bounds were not satisfied:
            `[[winter_math::fields::f64::BaseElement; 12]; 12]: Iterator`
            which is required by `std::iter::Zip<std::slice::IterMut<'_, winter_math::fields::f64::BaseElement>, [[winter_math::fields::f64::BaseElement; 12]; 12]>: Iterator`
            `std::iter::Zip<std::slice::IterMut<'_, winter_math::fields::f64::BaseElement>, [[winter_math::fields::f64::BaseElement; 12]; 12]>: Iterator`
            which is required by `&mut std::iter::Zip<std::slice::IterMut<'_, winter_math::fields::f64::BaseElement>, [[winter_math::fields::f64::BaseElement; 12]; 12]>: Iterator`

error: aborting due to 8 previous errors

Some errors have detailed explanations: E0277, E0599.
For more information about an error, try `rustc --explain E0277`.
error: could not compile `winter-crypto`

To learn more, run the command again with --verbose.
vadym@ubuntu:~/winterfell$

v0.6 release goals

For v0.6 release I'm thinking of adding the following to the library:

  • #93
  • #80
  • #126
  • Abstract away Merkle trees behind VectorCommitment trait.
  • Add support for validity constraints (i.e., constraints which hold on every step of execution trace).
  • Enable custom logic for constraint evaluation in the prover.
  • Add full support for traces with more than 2 segments.

Suggestions/comments are welcome.

Optimization of Matrix struct

Currently, Matrix struct stores trace and polynomial evaluation data in a column-major order. This allows us to run LDE for each column independently, but presents challenges during constraint evaluation where we need to process two sequential rows. Thus, we spend some time reading rows from the trace by copying values from each column into an EvaluationFrame struct.

A better approach could be to store data in a Matrix in a row-major order. This has the following advantages:

  1. EvaluationFrame can just store pointers to rows in the trace - no need to move any data around.
  2. Running LDE and FFT over multiple columns in parallel will actually be faster - probably up to 20% faster than doing it column by column as we do now.

[math] Implement cubic field extensions

This will let us generate proofs at 128-bit security level even in small fields (e.g. ~64 bits).

For the 62-bit field we are currently using, the irreducible polynomial could be: x3 - x + 2. But this won't work for our 128-bit field. This is not a problem per se, because we don't need to do cubic extensions of 128-bit fields, but it might be a good idea to investigate approaches of tying extension fields to specific base field (rather than giving one generic implementation for all extensions of a given degree).

[crypto] Verkle tree commitments

Currently, the only commitment scheme supported by Winterfell is Merkle trees. We should investigate adding an additional commitment scheme: Verkle tree.

By using Verkle trees we could reduce proof sizes significantly (by like a factor of 6x - 8x) while giving up only post-quantum security. The big question is how would it affect proof generation time (e.g. how long it would take to construct a Verkle tree with 1M nodes?). Also, for performance and other reasons, we should probably use IPA-based Verkle trees (as opposed to KZG-based ones).

If the performance is acceptable, we should add Verkle tree commitments as one of dynamically configurable parameters - e.g. commitment_scheme with the type looking something like this:

pub enum CommitmentScheme {
    MerkleTree,
    VerkleTree,
}

Some references on Verkle trees:

Recursive proofs?

Does Winterfell support recursive proofs? Is there a simple way to write a circuit which takes as inputs and checks a zkSNARK generated for another circuit (or the same circuit)? Or how would you recommend going about doing this with Winterfell?

Composition's poly expected degree mismatch

Whenever there is a trace column with the same repeated entry, there's a mismatch on the expected degree of the composition poly as long as it is computed as constrain_degree*(trace_length -1) - divisor_degree here https://github.com/novifinancial/winterfell/blob/46dce1adf06dcb0778b546054e938f0144fc1288/prover/src/constraints/evaluation_table.rs#L440 and here https://github.com/novifinancial/winterfell/blob/46dce1adf06dcb0778b546054e938f0144fc1288/air/src/air/transition/degree.rs#L103
The problem seems to be the use of trace_length-1 instead of the actual colum degree.

Although seems to be only a problem for debugging, it is annoying because it is not the expected behaviour. I wonder if this problem might also happen when some trace columns are generated, for example, as the evaluations of the identity polynomial

v0.5 release goals

For v0.5 release I'm thinking of adding the following to the library:

  • #93
  • #80
  • Enable custom logic for constraint evaluation in the prover.
  • #52
  • Add full support for traces with more than 2 segments.

Suggestions/comments are welcome.

[crypto] Add hash function with small output

Currently supported hash functions (SHA3 and BLAKE3) produce 256-bit outputs. This is an overkill when for proofs which target security levels below 128 bits.

For example, for proofs targeting 100-bit security level, hash output of 200 bits should be sufficient (as we still get 100-bit collision resistance). Using such a hash function should reduce proof sizes by about 20%.

As the first step, we could add just a single hash function - e.g. BLAKE3 with 192-bit output (we could call it Blake3_192 to keep the naming consistent with Blake3_256 that we currently have).

Bug in f64 deserialization

Unless I should be using another method for serialization, deserialization of zero values in this field does not work due to their canonical representation. The code below will panic with the error message: InvalidValue("invalid field element: value 18446744069414584321 is greater than or equal to the field modulus")'

use winter_math::{fields::f64::BaseElement, StarkField};
use winter_utils::Deserializable;
use winter_utils::SliceReader;

let bytes = BaseElement::from(0u8).as_int().to_le_bytes();
let mut reader = SliceReader::new(&bytes);
BaseElement::read_batch_from(&mut reader, 1).unwrap();

The issue is the following line, which should be changed to a greater than inequality:

if value >= M {

Safer implementation of the uninit_vector function

pub unsafe fn uninit_vector<T>(length: usize) -> Vec<T> {
let mut vector = Vec::with_capacity(length);
vector.set_len(length);
vector
}

Hello, here's a safer implementation that uses std::mem::MaybeUninit to create an uninitialized Vec:

pub fn uninit_vector<T>(length: usize) -> Vec<T> { 
     let mut vector = Vec::with_capacity(length); 
     unsafe { 
         let data_ptr = vector.as_mut_ptr(); 
         std::ptr::write_bytes(data_ptr, 0, length); 
         vector.set_len(length); 
     } 
     return vector; 
 }

This implementation uses std::ptr::write_bytes to initialize each element in the vector. This ensures that all elements in the vector are properly initialized, avoiding potential memory safety issues.

[examples] Create an example of using small fields

Currently, all our examples are done in a 128-bit field. It would be good to create an example in a 62-bit field. There are a few options here - but I think signature aggregation would be one of the more interesting ones.

Fix bench runs in CI

These currently fail.

Also, would be good to not do an automatic bench run if a PR status is draft and do it only once the status changes from draft to read for review.

Implement perfect zero-knowledge

Proofs currently generated by the library leak info. This is not an issue when the primary use case for proofs is succinctness (e.g. light client, signature aggregation), but this is not desirable for use cases which need to hide private data (e.g. anon token, hash pre-image). Ideally, we should have an option to enable perfect zero-knowledge for proofs.

This will require the following changes:

  • Inject random values at the end of execution trace of each register.
  • Combine composition polynomial with a random low-degree polynomial before running it through FRI protocol.
  • Use salted Merkle commitment scheme for execution trace commitment.

Why execution trace length must be a power of 2?

With this restriction, if we have an 11 steps trace table, then we must pad it to length 16.

Then when implementing get_pub_inputs method of Prover, we just can not determine the last trace row from the trace table parameter. We still need another variable indicating the real length of the trace table, in the above example, which is 11, not 16.

`RandomCoin` as a trait

This issue aims to start a discussion on the merits of changing RandomCoin<B: StarkField, H: Hasher> from a struct to a trait. The reasons for this being that for some choices of H (specifically the ones based on the sponge construction) as well as of B (e.g. when it is the base field of the algebraic hasher H) seeding (which can be done with absorbing) and drawing random values (which can be done by squeezing) can be achieved in more efficient ways.

Javascript Bindings

Per the CI this command succeeds:

cargo build --no-default-features --features alloc --target wasm32-unknown-unknown --release

However, a build with wasm-pack` or neon might be easier to use.

Does anyone have any examples of this library being called from JavaScript?

Add Rescue Prime as a hash function option for prover/verifier

Rescue Prime hash function has been implemented as a part of #50. However, it is not yet integrated into the prover and verifier.

There is one challenging aspect here: RP62_248 works only in f62 field, however, prover and verifier expect the hash function to be generic over all fields. It would be nice if we could do some kind of "type narrowing" - e.g. if there is a mismatch between base field of AIR and hash function, a runtime error would be thrown, otherwise everything will work as expected. But I'm not sure if this is currently possible in Rust.

Question about TransitionConstraintDegree in examples

Hi, I am delighted to find the winterfell repository, it is helpful to me. I am trying to understand the examples you gave. I found the degree variable in the air.rs difficult to learn. As the documentation describes that all trace columns have degree of 1 and when multiplying trace columns together, the degree increases by 1. Further, if a constraint involves multiplication of one trace column and one periodic column, we should use with_cycles.

Here in merkle tree example. The first six terms all have a degree of 5.

let degrees = vec![
    TransitionConstraintDegree::with_cycles(5, vec![HASH_CYCLE_LEN]),
    TransitionConstraintDegree::with_cycles(5, vec![HASH_CYCLE_LEN]),
    TransitionConstraintDegree::with_cycles(5, vec![HASH_CYCLE_LEN]),
    TransitionConstraintDegree::with_cycles(5, vec![HASH_CYCLE_LEN]),
    TransitionConstraintDegree::with_cycles(5, vec![HASH_CYCLE_LEN]),
    TransitionConstraintDegree::with_cycles(5, vec![HASH_CYCLE_LEN]),
    TransitionConstraintDegree::new(2),
];

However, when I further looked evaluate_transition, I found there are rescue::enforce_round constraints which have degree of 3 for the above first six terms. And then there are the following constraints.

// when hash_flag = 0, make sure accumulated hash is placed in the right place in the hash
// state for the next round of hashing. Specifically: when index bit = 0 accumulated hash
// must go into registers [0, 1], and when index bit = 0, it must go into registers [2, 3]
let hash_init_flag = not(hash_flag);
let bit = next[6];
let not_bit = not(bit);
result.agg_constraint(0, hash_init_flag, not_bit * are_equal(current[0], next[0]));
result.agg_constraint(1, hash_init_flag, not_bit * are_equal(current[1], next[1]));
result.agg_constraint(2, hash_init_flag, bit * are_equal(current[0], next[2]));
result.agg_constraint(3, hash_init_flag, bit * are_equal(current[1], next[3]));

// make sure capacity registers of the hash state are reset to zeros
result.agg_constraint(4, hash_init_flag, is_zero(next[4]));
result.agg_constraint(5, hash_init_flag, is_zero(next[5]));

The hash_init_flag comes from a periodic column. not_bit and bit comes from a normal trace column. Take the first term as an example. The degree here is 3, and plus rescue::enforce_round constraints, the total degree should be 6.

result.agg_constraint(0, hash_init_flag, not_bit * are_equal(current[0], next[0]));
// hash_init_flag * not_bit * are_equal(current[0], next[0]);

I did not get how the degree 5 in code are determined.

In addition, the two terms below, each of them should have a degree of 4, then plus rescue::enforce_round constraints, the degree should be 7.

result.agg_constraint(2, hash_init_flag, bit * are_equal(current[0], next[2]));
result.agg_constraint(3, hash_init_flag, bit * are_equal(current[1], next[3]));

Can someone help me? appreciate.

A simple question about interpolate

When testing FFT, I try to interpolate a trace points and then evaluate as below.

        let points: Vec<u32> = (1..=4).collect();;
        let mut a: Vec<BaseElement> = points.iter().map(|e| BaseElement::from(e.clone()) ).collect();

        let inv_twiddles = get_inv_twiddles::<BaseElement>(points.len());
        println!("{:?}", points);
        fft::interpolate_poly(&mut a, &inv_twiddles);
        fft::evaluate_poly(&mut a, &inv_twiddles);
        
        let res : Vec<_> = a.iter().map(|e| { e.as_int() }).collect();
        println!("post {:?}", res);

output:

prev:   1, 2, 3, 4
post:   1, 4, 3, 2

I expect that the post suppose to be as same as the prev. Can you please help to explain how this happen?

[FRI] Implement custom folding factor

Currently, our implementation of degree-preserving projection folds evaluation domains by a factor of 4. Would be good to have the ability to dynamically change the folding factor between values of 4, 8, and 16 to see what impact this makes on prover performance, proof size etc.

[common] Custom proof serialization

We should implement custom serialization for StarkProof struct. The benefits of this are:

  1. Proof sizes should decrees by 5% or so.
  2. We can remove serde as a dependency from all crates.
  3. This will open up opportunities for future optimizations (e.g. custom-length hash function output).

This should be preceded by #5 and #6.

Recommend Projects

  • React photo React

    A declarative, efficient, and flexible JavaScript library for building user interfaces.

  • Vue.js photo Vue.js

    🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.

  • Typescript photo Typescript

    TypeScript is a superset of JavaScript that compiles to clean JavaScript output.

  • TensorFlow photo TensorFlow

    An Open Source Machine Learning Framework for Everyone

  • Django photo Django

    The Web framework for perfectionists with deadlines.

  • D3 photo D3

    Bring data to life with SVG, Canvas and HTML. 📊📈🎉

Recommend Topics

  • javascript

    JavaScript (JS) is a lightweight interpreted programming language with first-class functions.

  • web

    Some thing interesting about web. New door for the world.

  • server

    A server is a program made to process requests and deliver data to clients.

  • Machine learning

    Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.

  • Game

    Some thing interesting about game, make everyone happy.

Recommend Org

  • Facebook photo Facebook

    We are working to build community through open source technology. NB: members must have two-factor auth.

  • Microsoft photo Microsoft

    Open source projects and samples from Microsoft.

  • Google photo Google

    Google ❤️ Open Source for everyone.

  • D3 photo D3

    Data-Driven Documents codes.