From bf2db29c9a023a7883d9d29419713c97703d3467 Mon Sep 17 00:00:00 2001 From: marcbeunardeau88 Date: Mon, 27 Jan 2025 10:00:47 +0100 Subject: [PATCH 1/2] o1vm/lookup: add lookup prover until alpha --- o1vm/src/pickles/lookup_prover.rs | 140 ++++++++++++++++++++++++++++++ o1vm/src/pickles/mod.rs | 3 + 2 files changed, 143 insertions(+) create mode 100644 o1vm/src/pickles/lookup_prover.rs diff --git a/o1vm/src/pickles/lookup_prover.rs b/o1vm/src/pickles/lookup_prover.rs new file mode 100644 index 0000000000..8b2648be8b --- /dev/null +++ b/o1vm/src/pickles/lookup_prover.rs @@ -0,0 +1,140 @@ +use crate::E; +use ark_ff::{One, PrimeField, Zero}; +use ark_poly::{Evaluations, Radix2EvaluationDomain}; +use core::iter::Once; +use kimchi::{circuits::domains::EvaluationDomains, curve::KimchiCurve}; +use mina_poseidon::FqSponge; +use poly_commitment::{commitment::absorb_commitment, ipa::SRS, SRS as _}; +//TODO Parralelize +//use rayon::prelude::*; +use std::iter::Chain; + +/// This prover takes one Public Input and one Public Output +/// It then proves that the sum 1/(beta + table) = PI - PO +/// where the table term are term from fixed lookup or RAMLookup + +pub struct AuxiliaryProofInput { + wires: Vec>, + arity: Vec>, + beta_challenge: F, + gamma_challenge: F, +} +pub struct ColumnEnv { + wires: Vec, + inverses: Vec, + acc: X, +} + +impl IntoIterator for ColumnEnv { + type Item = X; + type IntoIter = Chain< + Chain< as IntoIterator>::IntoIter, as IntoIterator>::IntoIter>, + as IntoIterator>::IntoIter, + >; + fn into_iter(self) -> Self::IntoIter { + self.wires + .into_iter() + .chain(self.inverses) + .chain(std::iter::once(self.acc)) + } +} + +pub struct AllColumns { + cols: ColumnEnv, + t_1: X, + t_2: X, +} +pub struct Eval { + zeta: AllColumns, + zeta_omega: AllColumns, +} + +pub struct Proof { + //placeholder + a: G::ScalarField, +} + +pub fn aux_prove + Clone>( + input: AuxiliaryProofInput, + srs: &SRS, + domain: EvaluationDomains, + mut fq_sponge: EFqSponge, + constraints: &[E], +) -> { + let AuxiliaryProofInput { + wires, + arity, + beta_challenge, + gamma_challenge, + } = input; + //Compute how many inverse wires we need to define pad function accordingly + let nb_inv_wires = arity + .iter() + .max_by(|a, b| a.len().cmp(&b.len())) + .unwrap() + .len(); + let pad = |mut vec: Vec| { + vec.append(&mut vec![G::ScalarField::zero(); nb_inv_wires]); + vec + }; + + // compute the 1/beta+sum_i gamma^i value_i for each lookup term + // The inversions is commputed in batch in the end + let mut inverses: Vec> = wires + .iter() + .zip(arity) + .map(|(inner_vec, arity)| { + arity + .into_iter() + .map(|arity| { + // TODO don't recompute gamma powers everytime + let (res, _) = inner_vec.iter().take(arity).fold( + (beta_challenge, G::ScalarField::one()), + |(acc, gamma_i), x| (acc + gamma_i * x, gamma_i * gamma_challenge), + ); + res + }) + .collect() + }) + .map(pad) + .collect(); + //perform the inversion + inverses + .iter_mut() + .for_each(|inner_vec| ark_ff::batch_inversion(inner_vec)); + // compute the accumulator + let mut partial_sum = G::ScalarField::zero(); + let mut acc = vec![]; + for inner in inverses.iter_mut() { + for x in inner.iter_mut() { + partial_sum += *x; + acc.push(partial_sum) + } + } + let columns = ColumnEnv { + wires, + inverses, + acc, + }; + //interpolating + let eval_col = |evals: Vec| { + Evaluations::>::from_vec_and_domain( + evals, domain.d1, + ) + .interpolate() + }; + let columns_poly = columns.into_iter().map(eval_col); + // commiting + let columns_com = columns_poly + .into_iter() + .map(|poly| srs.commit_non_hiding(&poly, 1)); + + // abosrbing commit + // TODO don't absorb the wires which already have been + columns_com + .into_iter() + .for_each(|com| absorb_commitment(&mut fq_sponge, &com)); + + // Constraints combiner + let alpha: G::ScalarField = fq_sponge.challenge(); +} diff --git a/o1vm/src/pickles/mod.rs b/o1vm/src/pickles/mod.rs index b557473fe3..906e9f444a 100644 --- a/o1vm/src/pickles/mod.rs +++ b/o1vm/src/pickles/mod.rs @@ -17,6 +17,9 @@ pub mod proof; pub mod prover; pub mod verifier; +///Lookup related modules +pub mod lookup_prover; + /// Maximum degree of the constraints. /// It does include the additional degree induced by the multiplication of the /// selectors. From d41ef489b54504a346cd30607f2d09b655436f37 Mon Sep 17 00:00:00 2001 From: marcbeunardeau88 Date: Wed, 5 Feb 2025 14:52:36 +0100 Subject: [PATCH 2/2] o1vm/lookup_prover: to remove, make clippy happy --- o1vm/src/pickles/lookup_prover.rs | 18 +++++++++--------- 1 file changed, 9 insertions(+), 9 deletions(-) diff --git a/o1vm/src/pickles/lookup_prover.rs b/o1vm/src/pickles/lookup_prover.rs index 8b2648be8b..a43aa9f159 100644 --- a/o1vm/src/pickles/lookup_prover.rs +++ b/o1vm/src/pickles/lookup_prover.rs @@ -40,18 +40,18 @@ impl IntoIterator for ColumnEnv { } pub struct AllColumns { - cols: ColumnEnv, - t_1: X, - t_2: X, + _cols: ColumnEnv, + _t_1: X, + _t_2: X, } pub struct Eval { - zeta: AllColumns, - zeta_omega: AllColumns, + _zeta: AllColumns, + _zeta_omega: AllColumns, } pub struct Proof { //placeholder - a: G::ScalarField, + _a: G::ScalarField, } pub fn aux_prove + Clone>( @@ -59,8 +59,8 @@ pub fn aux_prove, domain: EvaluationDomains, mut fq_sponge: EFqSponge, - constraints: &[E], -) -> { + _constraints: &[E], +) { let AuxiliaryProofInput { wires, arity, @@ -136,5 +136,5 @@ pub fn aux_prove