Skip to content

Commit

Permalink
Merge pull request #2924 from o1-labs/arrabbiata/main-works-ci
Browse files Browse the repository at this point in the history 
CI/Arrabbiata: make the main file running for continuous testing
  • Loading branch information
@dannywillems
dannywillems authored Jan 8, 2025
2 parents c61f2ff + 08a5e40 commit d760a9a
Show file tree
Hide file tree
Showing 7 changed files with 199 additions and 57 deletions.
2 changes: 1 addition & 1 deletion arrabbiata/README.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -67,7 +67,7 @@ environment variable `RUST_LOG=debug`.
### Run tests

```
cargo nextest run --all-features --release --nocapture -p arrabiata
cargo nextest run --all-features --release --nocapture -p arrabbiata
```

### Registry of zkApps
Expand Down
181 changes: 136 additions & 45 deletions arrabbiata/src/interpreter.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -28,6 +28,8 @@
//! - [Handle the combinaison of constraints](#handle-the-combinaison-of-constraints)
//! - [Permutation argument](#permutation-argument)
//! - [Fiat-Shamir challenges](#fiat-shamir-challenges)
//! - [Folding](#folding)
//! - [Message passing](#message-passing)
//!
//! ## Gadgets implemented
//!
Expand All @@ -37,9 +39,9 @@
//! particular additions and scalar multiplications.
//!
//! To reduce the number of operations, we consider the affine coordinates.
//! As a reminder, here the equations to compute the addition of two different
//! points `P1 = (X1, Y1)` and `P2 = (X2, Y2)`. Let define `P3 = (X3, Y3) = P1 +
//! P2`.
//! As a reminder, here are the equations to compute the addition of two
//! different points `P1 = (X1, Y1)` and `P2 = (X2, Y2)`. Let define `P3 = (X3,
//! Y3) = P1 + P2`.
//!
//! ```text
//! - λ = (Y1 - Y2) / (X1 - X2)
Expand Down Expand Up @@ -67,9 +69,9 @@
//! For given inputs (x1, y1) and (x2, y2), the layout will be as follow:
//!
//! ```text
//! | C1 | C2 | C3 | C4 | C5 | C6 | C7 | C8 | C9 | C10 | C11 | C12 | C13 | C14 | C15 | C16 | C17 |
//! | -- | -- | -- | -- | -- | -- | -- | -- | -- | --- | --- | --- | --- | --- | --- | --- | --- |
//! | x1 | y1 | x2 | y2 | b0 | λ | x3 | y3 | | | | | | | | | |
//! | C1 | C2 | C3 | C4 | C5 | C6 | C7 | C8 | C9 | C10 | C11 | C12 | C13 | C14 | C15 |
//! | -- | -- | -- | -- | -- | -- | -- | -- | -- | --- | --- | --- | --- | --- | --- |
//! | x1 | y1 | x2 | y2 | b0 | λ | x3 | y3 | | | | | | | |
//! ```
//!
//! where `b0` is equal two `1` if the points are the same, and `0` otherwise.
Expand Down Expand Up @@ -115,33 +117,12 @@
//!
//! #### Gadget layout
//!
//! We start with the assumption that 17 columns are available for the whole
//! circuit, and we can support constraints up to degree 5.
//! Therefore, we can compute 4 full rounds per row if we rely on the
//! permutation argument, or 5 full rounds per row if we use the "next row".
//!
//! We provide two implementations of the Poseidon hash function. The first one
//! does not use the "next row" and is limited to 4 full rounds per row. The
//! second one uses the "next row" and can compute 5 full rounds per row.
//! The second implementation is more efficient as it allows to compute one
//! additional round per row.
//! For the second implementation, the permutation argument will only be
//! activated on the first and last group of 5 rounds.
//!
//! The layout for the one not using the "next row" is as follow (4 full rounds):
//! ```text
//! | C1 | C2 | C3 | C4 | C5 | C6 | C7 | C8 | C9 | C10 | C11 | C12 | C13 | C14 | C15 |
//! | -- | -- | -- | -- | -- | -- | -- | -- | -- | --- | --- | --- | --- | --- | --- |
//! | x | y | z | a1 | a2 | a3 | b1 | b2 | b3 | c1 | c2 | c3 | o1 | o2 | o3 |
//! ```
//! where (x, y, z) is the input of the current step, (o1, o2, o3) is the
//! output, and the other values are intermediary values. And we have the following equalities:
//! ```text
//! (a1, a2, a3) = PoseidonRound(x, y, z)
//! (b1, b2, b3) = PoseidonRound(a1, a2, a3)
//! (c1, c2, c3) = PoseidonRound(b1, b2, b3)
//! (o1, o2, o3) = PoseidonRound(c1, c2, c3)
//! ```
//! We start with the assumption that [crate::NUMBER_OF_COLUMNS] columns are
//! available for the whole circuit, and we can support constraints up to degree
//! [crate::MAX_DEGREE].
//! Therefore, we can compute 5 full rounds per row by using the "next row"
//! (i.e. adding an evaluation point at ζω). An implementation is provided in
//! the gadget [crate::columns::Gadget::Poseidon].
//!
//! The layout for the one using the "next row" is as follow (5 full rounds):
//! ```text
Expand All @@ -161,7 +142,7 @@
//! (o1, o2, o3) = PoseidonRound(d1, d2, d3)
//! ```
//!
//! For both implementations, round constants are passed as public inputs. As a
//! Round constants are passed as public inputs. As a
//! reminder, public inputs are simply additional columns known by the prover
//! and verifier.
//! Also, the elements to absorb are added to the initial state at the beginning
Expand All @@ -176,7 +157,7 @@
//!
//! We will consider a basic implementation using the "next row". The
//! accumulators will be saved on the "next row". The decomposition of the
//! scalar will be incrementally on each row.
//! scalar will be incremental on each row.
//! The scalar used for the scalar multiplication will be fetched using the
//! permutation argument (FIXME: to be implemented).
//! More than one bit can be decomposed at the same time, and we could reduce
Expand All @@ -199,8 +180,8 @@
//! We have the following layout:
//!
//! ```text
//! | C1 | C2 | C3 | C4 | C5 | C7 | C7 | C8 | C9 | C10 | C11 | C12 | C13 | C14 | C15 | C16 | C17 |
//! | -- | ----- | ------------- | ------------- | --------- | -- | -------------- | -------------- | -- | --- | -------- | --- | --- | --- | --- | --- | --- |
//! | C1 | C2 | C3 | C4 | C5 | C7 | C7 | C8 | C9 | C10 | C11 | C12 | C13 | C14 | C15 |
//! | -- | ----- | ------------- | ------------- | --------- | -- | -------------- | -------------- | -- | --- | -------- | --- | --- | --- | --- |
//! | o_x | o_y | double_tmp_x | double_tmp_y | r_i | λ | res_plus_tmp_x | res_plus_tmp_y | λ' | b |
//! | o'_x | o'_y | double_tmp'_x | double_tmp'_y | r_(i+1) |
//! ```
Expand All @@ -224,8 +205,8 @@
//!
//! Using this technique requires us a folding scheme that handles degree
//! `5 + 1` constraints, as the challenge will be considered as a variable.
//! The reader can refer to the folding library available in this monorepo for
//! more contexts.
//! The reader can refer to this [HackMD
//! document](https://hackmd.io/@dannywillems/Syo5MBq90) for more details.
//!
//! ## Permutation argument
//!
Expand Down Expand Up @@ -297,11 +278,13 @@
//! ## Fiat-Shamir challenges
//!
//! The challenges sent by the verifier must also be simulated by the IVC
//! circuit.
//! circuit. It is done by passing "messages" as public inputs to the next
//! instances. Diagrams recapitulating the messages that must be passed are
//! available in the section [Message passing](#message-passing).
//!
//! For a step `i + 1`, the challenges of the step `i` must be computed by the
//! verifier, and check that it corresponds to the ones received as a public
//! input.
//! verifier in the circuit, and check that it corresponds to the ones received
//! as a public input.
//!
//! TBD/FIXME: specify. Might require foreign field arithmetic.
//!
Expand All @@ -319,8 +302,8 @@
//! This computation depends on the constraints, and in particular on the
//! monomials describing the constraints.
//! The computation of the cross-terms and the error terms happen after the
//! witness has been built and the different arguments like the permutation or
//! lookup have been done. Therefore, the interpreter must provide a method to
//! witness has been built and the different arguments like the permutation and
//! lookups have been done. Therefore, the interpreter must provide a method to
//! compute it, and the constraints should be passed as an argument.
//!
//! When computing the cross-terms, we must compute the contribution of each
Expand All @@ -337,6 +320,115 @@
//! implementing the trait [MVPoly](mvpoly::MVPoly) and the method
//! [compute_cross_terms](mvpoly::MVPoly::compute_cross_terms) can be used from
//! there.
//!
//! ## Message passing
//!
//! The message passing is a crucial part of the IVC scheme. The messages are
//! mostly commitments and challenges that must be passed from one step to
//! another, and by "jumping" between curves. In the implementation,
//! the messages are kept in an "application environment", located in the
//! "witness environment". The structure [crate::witness::Env] is used to keep
//! track of the messages that must be passed.
//! Each step starts with an "application state" and end with another that are
//! accumuated. The final state is passed through a "digest" to the next
//! instance. The digest is performed using a hash function (see [Hash -
//! Poseidon](#hash---poseidon)). We often use the term "sponge" to refer to the
//! hash function or the state of the hash function.
//!
//! The sponge state will be forked at different steps, to provide a
//! consistent state between the different instances and the different curves.
//! The challenges will be computed using the sponge state after hashing the
//! appropriate values from the appropriate initial state, and be kept in the
//! environment.
//!
//! In the diagram below, each object subscripted by `(p, n)` (resp. `(q, n)`)
//! means that they are related to the instance `n` whose circuit is defined in
//! the field `Fp` (resp. `Fq`), the scalar field of Vesta (resp. Pallas).
//!
//! In addition to that, we use
//! - `w_(p, n)` for the witness.
//! - `W_(p, n)` for the aggregated witness.
//! - `C_(p, n)` for the commitment to the witness `w_(p, n)`.
//! - `acc_(p, n)` for the accumulated commitments to the aggregated witness
//! `W_(p, n)`.
//! - `α_(p, n)` for the challenge used to combine constraints.
//! - `β_(p, n)` and `γ_(p, n)` for the challenge used to for the
//! permutation argument.
//! - `r_(p, n)` for the challenge used for the accumulation of the
//! - `t_(p, n, i)` for the evaluations of the cross-terms of degree `i`.
//! - `Ct_(p, n, i)` for the commitments to the cross-terms of degree `i`.
//! witness/commitments.
//! - `u_(p, n)` for the challenge used to homogenize the constraints.
//! - `o_(p, n)` for the final digest of the application state.
//!
//! Here a diagram (FIXME: this is not complete) that shows the messages that
//! must be passed:
//!
//! ```text
//! +------------------------------------------+ +------------------------+
//! | Instance n | | Instance n + 2 |
//! | (witness w_(p, n)) | | (witness W_(p, n + 1)) |
//! | ---------- | | ---------- |
//! | Vesta | | Vesta |
//! | (scalar field = Fp) | | (scalar field = Fp) |
//! | (base field = Fq) | | (base field = Fq) |
//! | (Sponge over Fq) | | (Sponge over Fq) |
//! | | | |
//! | Generate as output | | Generate as output |
//! | ------------------ | | ------------------ |
//! | Challenges: | | Challenges: |
//! | - α_(p, n) | | - α_(p, n + 1) |
//! | - β_(p, n) | | - β_(p, n + 1) |
//! | - γ_(p, n) | | - γ_(p, n + 1) |
//! | - r_(p, n) | | - r_(p, n + 1) |
//! | - u_(p, n) | | - u_(p, n + 1) |
//! | Commitments: | | (...) |
//! | - Cross-terms (`Ct_(p, n)`) | +------------------------+
//! | - Witness columns (`w_(p, n)`) | ^
//! | Fiat-Shamir: | |
//! | - digest of all messages read until | |
//! | now -> `o_(p, n)` | |
//! | | |
//! | Receive in PI | |
//! | -------------- | |
//! | - Commitments to w_(p, (n - 1)) | |
//! | - Final digest of the application | |
//! | state at instance (n - 1) | |
//! | (o_(q, n - 1)). | |
//! | - Final digest of the application | |
//! | state at instance (n - 2) | |
//! | (o_(p, n - 1)). | |
//! | | |
//! | Responsibility | |
//! | -------------- | |
//! | - Verify FS challenges (α_(q, n - 1), | |
//! | β_(q, n - 1), γ_(q, n - 1), | |
//! | r_(q, n - 1), u_(q, n - 1) | |
//! | (i.e. challenges of instance n - 1) | |
//! | from o_(q, n - 1) | |
//! | - Aggregate witness columns w_(p, n) | |
//! | into W_(p, n). | |
//! | - Aggregate error terms | |
//! | from instance n - 2 with cross terms of | |
//! | instance n - 2 | |
//! +------------------------------------------+ |
//! | |
//! | |
//! | +----------------------------+ |
//! | | Instance n + 1 | |
//! | | (witness w_(q, n)) | |
//! | | -------------- | |
//! | | Pallas | |
//! | | (scalar field = Fq) | |
//! |-----------> | (base field = Fp) |--------------
//! | (Sponge over Fp) |
//! TODO: define msgs | | TODO: define msgs
//! format to pass | TODO | format to pass
//! IO | | IO
//! | |
//! | |
//! +----------------------------+
//! ```
use crate::{
columns::Gadget, curve::PlonkSpongeConstants, MAXIMUM_FIELD_SIZE_IN_BITS, NUMBER_OF_COLUMNS,
Expand Down Expand Up @@ -925,7 +1017,6 @@ pub fn run_ivc<E: InterpreterEnv>(env: &mut E, instr: Instruction) {
state.iter().enumerate().for_each(|(i, x)| {
unsafe { env.save_poseidon_state(x.clone(), i) };
});
env.reset();
};
state
});
Expand Down
14 changes: 10 additions & 4 deletions arrabbiata/src/lib.rs
View file
Original file line number Diff line number Diff line change
@@ -1,3 +1,5 @@
use curve::PlonkSpongeConstants;
use mina_poseidon::constants::SpongeConstants;
use strum::EnumCount as _;

pub mod column_env;
Expand All @@ -21,13 +23,17 @@ pub const MAX_DEGREE: u64 = 5;
/// Requiring at least 2^16 to perform 16bits range checks.
pub const MIN_SRS_LOG2_SIZE: usize = 16;

/// The number of rows the IVC circuit requires.
// FIXME: that might change. We use a vertical layout for now.
pub const IVC_CIRCUIT_SIZE: usize = 1 << 13;

/// The maximum number of columns that can be used in the circuit.
pub const NUMBER_OF_COLUMNS: usize = 15;

/// The number of rows the IVC circuit requires.
// FIXME:
// We will increase the IVC circuit size step by step, while we are finishing
// the implementation.
// 1. We start by absorbing all the accumulators of each column.
pub const IVC_CIRCUIT_SIZE: usize =
(PlonkSpongeConstants::PERM_ROUNDS_FULL / 5) * NUMBER_OF_COLUMNS;

/// The maximum number of public inputs the circuit can use per row
/// We do have 15 for now as we want to compute 5 rounds of poseidon per row
/// using the gadget [crate::columns::Gadget::Poseidon]. In addition to
Expand Down
19 changes: 16 additions & 3 deletions arrabbiata/src/main.rs
View file
Original file line number Diff line number Diff line change
@@ -1,3 +1,9 @@
//! This file contains an entry point to run a zkApp written in Rust.
//! Until the first version is complete, this file will contain code that
//! will need to be moved later into the Arrabbiata library.
//! The end goal is to allow the end-user to simply select the zkApp they want,
//! specify the number of iterations, and keep this file relatively simple.
use arrabbiata::{
curve::PlonkSpongeConstants,
interpreter::{self, InterpreterEnv},
Expand Down Expand Up @@ -67,16 +73,23 @@ pub fn main() {
info!("Run iteration: {}/{}", env.current_iteration, n_iteration);

// Build the application circuit
info!("Running N iterations of the application circuit");
info!("Running {n_iteration_per_fold} iterations of the application circuit");
for _i in 0..n_iteration_per_fold {
interpreter::run_app(&mut env);
env.reset();
}

info!("Building the IVC circuit");
info!(
"Building the IVC circuit. A total number of {} rows will be filled from the witness row {}",
IVC_CIRCUIT_SIZE, env.current_row,
);
// Build the IVC circuit
for _i in 0..IVC_CIRCUIT_SIZE {
for i in 0..IVC_CIRCUIT_SIZE {
let instr = env.fetch_instruction();
debug!(
"Running IVC row {} (instruction = {:?}, witness row = {})",
i, instr, env.current_row
);
interpreter::run_ivc(&mut env, instr);
env.current_instruction = env.fetch_next_instruction();
env.reset();
Expand Down
5 changes: 2 additions & 3 deletions arrabbiata/src/witness.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -19,6 +19,8 @@ use crate::{
NUMBER_OF_VALUES_TO_ABSORB_PUBLIC_IO,
};

/// The first instruction in the IVC is the Poseidon permutation. It is used to
/// start hashing the public input.
pub const IVC_STARTING_INSTRUCTION: Instruction = Instruction::Poseidon(0);

/// An environment that can be shared between IVC instances.
Expand Down Expand Up @@ -990,9 +992,6 @@ impl<
/// z_(i + 1) = F(w_i, z_i)
/// ```
///
/// - We decompose the scalar `r`, the random combiner, into bits to compute
/// the MSM for the next step.
///
/// - We compute the MSM (verifier)
///
/// ```text
Expand Down
Loading

0 comments on commit d760a9a

Please sign in to comment.