From 3fdda8e30889167cbd355d26ebf7685f279b5132 Mon Sep 17 00:00:00 2001 From: svv232 Date: Mon, 18 Nov 2024 14:38:21 -0500 Subject: [PATCH 01/63] add elf parser test --- o1vm/tests/test_riscv_elf.rs | 17 +++++++++++++++++ 1 file changed, 17 insertions(+) diff --git a/o1vm/tests/test_riscv_elf.rs b/o1vm/tests/test_riscv_elf.rs index f6cf008924..d6918dc01b 100644 --- a/o1vm/tests/test_riscv_elf.rs +++ b/o1vm/tests/test_riscv_elf.rs @@ -5,6 +5,23 @@ use o1vm::interpreters::riscv32i::{ PAGE_SIZE, }; +#[test] +// This test is used to check that the elf loader is working correctly. +// We must export the code used in this test in a function that can be called by +// the o1vm at load time. +fn test_correctly_parsing_elf() { + let curr_dir = std::env::current_dir().unwrap(); + let path = curr_dir.join(std::path::PathBuf::from( + "resources/programs/riscv32i/fibonacci", + )); + let state = o1vm::elf_loader::parse_riscv32i(&path).unwrap(); + // This is the output we get by running objdump -d fibonacci + assert_eq!(state.pc, 69932); + + assert_eq!(state.memory.len(), 1); + assert_eq!(state.memory[0].index, 17); +} + #[test] // Checking an instruction can be converted into a string. // It is mostly because we would want to use it to debug or write better error From 370e0994f9ee0a48cd25b8ba4c63cee14c53cb5b Mon Sep 17 00:00:00 2001 From: Danny Willems Date: Wed, 20 Nov 2024 14:52:07 +0100 Subject: [PATCH 02/63] o1vm/riscv32: introduce tests checking the number of instructions In the meantime, set the correct current value. --- o1vm/src/interpreters/riscv32im/mod.rs | 9 ++++-- o1vm/src/interpreters/riscv32im/tests.rs | 36 ++++++++++++++++++++++++ 2 files changed, 42 insertions(+), 3 deletions(-) create mode 100644 o1vm/src/interpreters/riscv32im/tests.rs diff --git a/o1vm/src/interpreters/riscv32im/mod.rs b/o1vm/src/interpreters/riscv32im/mod.rs index 5b78cb702b..59c855694b 100644 --- a/o1vm/src/interpreters/riscv32im/mod.rs +++ b/o1vm/src/interpreters/riscv32im/mod.rs @@ -4,12 +4,12 @@ pub const SCRATCH_SIZE: usize = 80; /// Number of instructions in the ISA -// FIXME: the value might not be correct. It will be updated when the -// interpreter is fully implemented. -pub const INSTRUCTION_SET_SIZE: usize = 40; +pub const INSTRUCTION_SET_SIZE: usize = 48; + pub const PAGE_ADDRESS_SIZE: u32 = 12; pub const PAGE_SIZE: u32 = 1 << PAGE_ADDRESS_SIZE; pub const PAGE_ADDRESS_MASK: u32 = PAGE_SIZE - 1; + /// List all columns used by the interpreter pub mod column; @@ -21,3 +21,6 @@ pub mod interpreter; pub mod registers; pub mod witness; + +#[cfg(test)] +mod tests; diff --git a/o1vm/src/interpreters/riscv32im/tests.rs b/o1vm/src/interpreters/riscv32im/tests.rs new file mode 100644 index 0000000000..6409c486aa --- /dev/null +++ b/o1vm/src/interpreters/riscv32im/tests.rs @@ -0,0 +1,36 @@ +use crate::interpreters::riscv32im::{ + constraints, + interpreter::{ + IInstruction, MInstruction, RInstruction, SBInstruction, SInstruction, SyscallInstruction, + UInstruction, UJInstruction, + }, +}; +use mina_curves::pasta::Fp; +use strum::EnumCount; + +#[test] +// Sanity check that we have as many selector as we have instructions +fn test_regression_selectors_for_instructions() { + let mips_con_env = constraints::Env::::default(); + let constraints = mips_con_env.get_selector_constraints(); + assert_eq!( + // We substract 1 as we have one boolean check per sel + // and 1 constraint to check that one and only one + // sel is activated + constraints.len() - 1, + // This should match the list in + // crate::interpreters::riscv32im::interpreter::Instruction + RInstruction::COUNT + + IInstruction::COUNT + + SInstruction::COUNT + + SBInstruction::COUNT + + UInstruction::COUNT + + UJInstruction::COUNT + + SyscallInstruction::COUNT + + MInstruction::COUNT + ); + // All instructions are degree 1 or 2. + constraints + .iter() + .for_each(|c| assert!(c.degree(1, 0) == 2 || c.degree(1, 0) == 1)); +} From 124d8be36023f95fdd64e0d00897b2a12e62b8ad Mon Sep 17 00:00:00 2001 From: Mikhail Volkhov Date: Wed, 20 Nov 2024 15:51:59 +0000 Subject: [PATCH 03/63] Rename xi into polyscale --- poly-commitment/src/commitment.rs | 14 +++++++------- poly-commitment/src/kzg.rs | 6 +++--- 2 files changed, 10 insertions(+), 10 deletions(-) diff --git a/poly-commitment/src/commitment.rs b/poly-commitment/src/commitment.rs index ba4d180134..f756e5b110 100644 --- a/poly-commitment/src/commitment.rs +++ b/poly-commitment/src/commitment.rs @@ -511,7 +511,7 @@ pub fn combined_inner_product( // final combined evaluation result let mut res = F::zero(); // polyscale^i - let mut xi_i = F::one(); + let mut polyscale_i = F::one(); for evals_tr in polys.iter().filter(|evals_tr| !evals_tr[0].is_empty()) { // Transpose the evaluations. @@ -523,7 +523,7 @@ pub fn combined_inner_product( // Iterating over the polynomial segments. // Each segment gets its own polyscale^i, each segment element j is multiplied by evalscale^j. - // Given that xi_i = polyscale^i0 at this point, after this loop we have: + // Given that polyscale_i = polyscale^i0 at this point, after this loop we have: // // res += Σ polyscale^{i0+i} ( Σ evals_tr[j][i] * evalscale^j ) // i j @@ -531,8 +531,8 @@ pub fn combined_inner_product( for eval in &evals { // p_i(evalscale) let term = DensePolynomial::::eval_polynomial(eval, *evalscale); - res += &(xi_i * term); - xi_i *= polyscale; + res += &(polyscale_i * term); + polyscale_i *= polyscale; } } res @@ -607,16 +607,16 @@ pub fn combine_commitments( rand_base: G::ScalarField, ) { // will contain the power of polyscale - let mut xi_i = G::ScalarField::one(); + let mut polyscale_i = G::ScalarField::one(); for Evaluation { commitment, .. } in evaluations.iter().filter(|x| !x.commitment.is_empty()) { // iterating over the polynomial segments for comm_ch in &commitment.chunks { - scalars.push(rand_base * xi_i); + scalars.push(rand_base * polyscale_i); points.push(*comm_ch); // compute next power of polyscale - xi_i *= polyscale; + polyscale_i *= polyscale; } } } diff --git a/poly-commitment/src/kzg.rs b/poly-commitment/src/kzg.rs index 9a448b4207..8d4d8ed7c6 100644 --- a/poly-commitment/src/kzg.rs +++ b/poly-commitment/src/kzg.rs @@ -55,7 +55,7 @@ pub fn combine_evaluations( evaluations: &Vec>, polyscale: G::ScalarField, ) -> Vec { - let mut xi_i = G::ScalarField::one(); + let mut polyscale_i = G::ScalarField::one(); let mut acc = { let num_evals = if !evaluations.is_empty() { evaluations[0].evaluations.len() @@ -74,9 +74,9 @@ pub fn combine_evaluations( for chunk_idx in 0..evaluations[0].len() { // supposes that all evaluations are of the same size for eval_pt_idx in 0..evaluations.len() { - acc[eval_pt_idx] += evaluations[eval_pt_idx][chunk_idx] * xi_i; + acc[eval_pt_idx] += evaluations[eval_pt_idx][chunk_idx] * polyscale_i; } - xi_i *= polyscale; + polyscale_i *= polyscale; } } From 761d053ce4984115384143b2d2abd0dc83dd0e20 Mon Sep 17 00:00:00 2001 From: Mikhail Volkhov Date: Wed, 20 Nov 2024 16:18:56 +0000 Subject: [PATCH 04/63] Variable names in combine_polys: get rid of omegas --- poly-commitment/src/ipa.rs | 41 ++++++++++++++++++++++---------------- 1 file changed, 24 insertions(+), 17 deletions(-) diff --git a/poly-commitment/src/ipa.rs b/poly-commitment/src/ipa.rs index af4e439818..aeea83c584 100644 --- a/poly-commitment/src/ipa.rs +++ b/poly-commitment/src/ipa.rs @@ -103,10 +103,10 @@ impl<'a, F: Field> ScaledChunkedPolynomial { /// Example: /// Given the three polynomials `p1(X)`, and `p3(X)` in coefficients /// forms, p2(X) in evaluation form, -/// and the scaling factor `s`, the result will be the polynomial: +/// and the scaling factor `polyscale`, the result will be the polynomial: /// /// ```text -/// p1(X) + s * i_fft(chunks(p2))(X) + s^2 p3(X) +/// p1(X) + polyscale * i_fft(chunks(p2))(X) + polyscale^2 p3(X) /// ``` /// /// Additional complexity is added to handle chunks. @@ -140,16 +140,19 @@ pub fn combine_polys>( vec![G::ScalarField::zero(); degree] }; - let mut omega = G::ScalarField::zero(); - let mut scale = G::ScalarField::one(); + // Will contain ∑ comm_chunk * polyscale^i + let mut combined_comm = G::ScalarField::zero(); + + // Will contain polyscale^i + let mut polyscale_to_i = G::ScalarField::one(); // Iterating over polynomials in the batch. - // Note that `omegas` are given as `PolyComm`. They are + // Note that the chunks in the commitment `p_i_comm` are given as `PolyComm`. They are // evaluations. // We do modify two different structures depending on the form of the // polynomial we are currently processing: `plnm` and `plnm_evals_part`. // We do need to treat both forms separately. - for (p_i, omegas) in plnms { + for (p_i, p_i_comm) in plnms { match p_i { // Here we scale the polynomial in evaluations forms // Note that based on the check above, sub_domain.size() always give @@ -161,11 +164,11 @@ pub fn combine_polys>( .par_iter_mut() .enumerate() .for_each(|(i, x)| { - *x += scale * evals[i * stride]; + *x += polyscale_to_i * evals[i * stride]; }); - for chunk in omegas.into_iter() { - omega += &(*chunk * scale); - scale *= &polyscale; + for comm_chunk in p_i_comm.into_iter() { + combined_comm += &(*comm_chunk * polyscale_to_i); + polyscale_to_i *= &polyscale; } } @@ -173,13 +176,13 @@ pub fn combine_polys>( DensePolynomialOrEvaluations::DensePolynomial(p_i) => { let mut offset = 0; // iterating over chunks of the polynomial - for chunk in omegas.into_iter() { + for comm_chunk in p_i_comm.into_iter() { let segment = &p_i.coeffs[std::cmp::min(offset, p_i.coeffs.len()) ..std::cmp::min(offset + srs_length, p_i.coeffs.len())]; - plnm_coefficients.add_poly(scale, segment); + plnm_coefficients.add_poly(polyscale_to_i, segment); - omega += &(*chunk * scale); - scale *= &polyscale; + combined_comm += &(*comm_chunk * polyscale_to_i); + polyscale_to_i *= &polyscale; offset += srs_length; } } @@ -191,7 +194,7 @@ pub fn combine_polys>( // plnm will be our final combined polynomial. We first treat the // polynomials in coefficients forms, which is simply scaling the // coefficients and add them. - let mut plnm = plnm_coefficients.to_dense_polynomial(); + let mut combined_plnm = plnm_coefficients.to_dense_polynomial(); if !plnm_evals_part.is_empty() { // n is the number of evaluations, which is a multiple of the @@ -202,13 +205,13 @@ pub fn combine_polys>( // equiv to divceil, but unstable in rust < 1.73. let num_chunks = n / max_poly_size + if n % max_poly_size == 0 { 0 } else { 1 }; // Interpolation on the whole domain, i.e. it can be d2, d4, etc. - plnm += &Evaluations::from_vec_and_domain(plnm_evals_part, D::new(n).unwrap()) + combined_plnm += &Evaluations::from_vec_and_domain(plnm_evals_part, D::new(n).unwrap()) .interpolate() .to_chunked_polynomial(num_chunks, max_poly_size) .linearize(polyscale); } - (plnm, omega) + (combined_plnm, combined_comm) } #[serde_as] @@ -744,6 +747,10 @@ impl SRS { let mut g = self.g.clone(); g.extend(vec![G::zero(); padding]); + // Combines polynomials roughly as follows: p(X) := ∑_i polyscale^i p_i(X) + // + // `blinding_factor` is a combined set of commitments that are + // paired with polynomials in `plnms`. let (p, blinding_factor) = combine_polys::(plnms, polyscale, self.g.len()); // The initial evaluation vector for polynomial commitment b_init is not From aad3200dbbdcd47254b5187bec004475c04fb15b Mon Sep 17 00:00:00 2001 From: Danny Willems Date: Thu, 21 Nov 2024 09:31:19 +0100 Subject: [PATCH 05/63] o1vm/mips: remove inverse_or_zero from interpreter trait --- o1vm/src/interpreters/mips/constraints.rs | 10 +--------- o1vm/src/interpreters/mips/interpreter.rs | 15 --------------- o1vm/src/interpreters/mips/witness.rs | 14 -------------- 3 files changed, 1 insertion(+), 38 deletions(-) diff --git a/o1vm/src/interpreters/mips/constraints.rs b/o1vm/src/interpreters/mips/constraints.rs index ea02390fd1..94369c890b 100644 --- a/o1vm/src/interpreters/mips/constraints.rs +++ b/o1vm/src/interpreters/mips/constraints.rs @@ -220,7 +220,7 @@ impl InterpreterEnv for Env { }; let x_inv_or_zero = { let pos = self.alloc_scratch(); - unsafe { self.inverse_or_zero(x, pos) } + self.variable(pos) }; // If x = 0, then res = 1 and x_inv_or_zero = 0 // If x <> 0, then res = 0 and x_inv_or_zero = x^(-1) @@ -229,14 +229,6 @@ impl InterpreterEnv for Env { res } - unsafe fn inverse_or_zero( - &mut self, - _x: &Self::Variable, - position: Self::Position, - ) -> Self::Variable { - self.variable(position) - } - fn equal(&mut self, x: &Self::Variable, y: &Self::Variable) -> Self::Variable { self.is_zero(&(x.clone() - y.clone())) } diff --git a/o1vm/src/interpreters/mips/interpreter.rs b/o1vm/src/interpreters/mips/interpreter.rs index 5ace8fb260..8bf4f61d2e 100644 --- a/o1vm/src/interpreters/mips/interpreter.rs +++ b/o1vm/src/interpreters/mips/interpreter.rs @@ -683,21 +683,6 @@ pub trait InterpreterEnv { /// `x`. unsafe fn test_zero(&mut self, x: &Self::Variable, position: Self::Position) -> Self::Variable; - /// Returns `x^(-1)`, or `0` if `x` is `0`, storing the result in `position`. - /// - /// # Safety - /// - /// There are no constraints on the returned value; callers must assert the relationship with - /// `x`. - /// - /// The value returned may be a placeholder; callers should be careful not to depend directly - /// on the value stored in the variable. - unsafe fn inverse_or_zero( - &mut self, - x: &Self::Variable, - position: Self::Position, - ) -> Self::Variable; - fn is_zero(&mut self, x: &Self::Variable) -> Self::Variable; /// Returns 1 if `x` is equal to `y`, or 0 otherwise, storing the result in `position`. diff --git a/o1vm/src/interpreters/mips/witness.rs b/o1vm/src/interpreters/mips/witness.rs index 684178ca29..ca0b98e1ef 100644 --- a/o1vm/src/interpreters/mips/witness.rs +++ b/o1vm/src/interpreters/mips/witness.rs @@ -312,20 +312,6 @@ impl InterpreterEnv for Env Self::Variable { - if *x == 0 { - self.write_column(position, 0); - 0 - } else { - self.write_field_column(position, Fp::from(*x).inverse().unwrap()); - 1 // Placeholder value - } - } - fn is_zero(&mut self, x: &Self::Variable) -> Self::Variable { // write the result let pos = self.alloc_scratch(); From e800dcfe9baaa88b0362e46d15e5baa38c596c40 Mon Sep 17 00:00:00 2001 From: Mikhail Volkhov Date: Wed, 20 Nov 2024 16:30:56 +0000 Subject: [PATCH 06/63] Move combine_polys and related structs into utils.rs --- ivc/src/prover.rs | 2 +- kimchi/src/prover.rs | 2 +- msm/src/prover.rs | 2 +- o1vm/src/pickles/prover.rs | 3 +- poly-commitment/benches/ipa.rs | 4 +- poly-commitment/src/ipa.rs | 194 +----------------------- poly-commitment/src/kzg.rs | 5 +- poly-commitment/src/lib.rs | 3 +- poly-commitment/src/utils.rs | 186 +++++++++++++++++++++++ poly-commitment/tests/batch_15_wires.rs | 3 +- poly-commitment/tests/commitment.rs | 3 +- poly-commitment/tests/ipa_commitment.rs | 6 +- poly-commitment/tests/kzg.rs | 6 +- 13 files changed, 214 insertions(+), 205 deletions(-) create mode 100644 poly-commitment/src/utils.rs diff --git a/ivc/src/prover.rs b/ivc/src/prover.rs index f123612d9c..719b2a8f61 100644 --- a/ivc/src/prover.rs +++ b/ivc/src/prover.rs @@ -31,8 +31,8 @@ use mina_poseidon::{sponge::ScalarChallenge, FqSponge}; use o1_utils::ExtendedDensePolynomial; use poly_commitment::{ commitment::{absorb_commitment, CommitmentCurve, PolyComm}, - ipa::DensePolynomialOrEvaluations, kzg::{KZGProof, PairingSRS}, + utils::DensePolynomialOrEvaluations, OpenProof, SRS, }; use rand::{CryptoRng, RngCore}; diff --git a/kimchi/src/prover.rs b/kimchi/src/prover.rs index 9156aee482..755592ca60 100644 --- a/kimchi/src/prover.rs +++ b/kimchi/src/prover.rs @@ -46,7 +46,7 @@ use poly_commitment::{ commitment::{ absorb_commitment, b_poly_coefficients, BlindedCommitment, CommitmentCurve, PolyComm, }, - ipa::DensePolynomialOrEvaluations, + utils::DensePolynomialOrEvaluations, OpenProof, SRS as _, }; use rand_core::{CryptoRng, RngCore}; diff --git a/msm/src/prover.rs b/msm/src/prover.rs index 138005a3e2..53cab9b287 100644 --- a/msm/src/prover.rs +++ b/msm/src/prover.rs @@ -30,7 +30,7 @@ use mina_poseidon::{sponge::ScalarChallenge, FqSponge}; use o1_utils::ExtendedDensePolynomial; use poly_commitment::{ commitment::{absorb_commitment, PolyComm}, - ipa::DensePolynomialOrEvaluations, + utils::DensePolynomialOrEvaluations, OpenProof, SRS, }; use rand::{CryptoRng, RngCore}; diff --git a/o1vm/src/pickles/prover.rs b/o1vm/src/pickles/prover.rs index 2f40787546..8978952d35 100644 --- a/o1vm/src/pickles/prover.rs +++ b/o1vm/src/pickles/prover.rs @@ -18,7 +18,8 @@ use mina_poseidon::{sponge::ScalarChallenge, FqSponge}; use o1_utils::ExtendedDensePolynomial; use poly_commitment::{ commitment::{absorb_commitment, PolyComm}, - ipa::{DensePolynomialOrEvaluations, OpeningProof, SRS}, + ipa::{OpeningProof, SRS}, + utils::DensePolynomialOrEvaluations, OpenProof as _, SRS as _, }; use rand::{CryptoRng, RngCore}; diff --git a/poly-commitment/benches/ipa.rs b/poly-commitment/benches/ipa.rs index 76c0cd3ea9..6c2abe5ef2 100644 --- a/poly-commitment/benches/ipa.rs +++ b/poly-commitment/benches/ipa.rs @@ -5,9 +5,7 @@ use groupmap::GroupMap; use mina_curves::pasta::{Fp, Vesta, VestaParameters}; use mina_poseidon::{constants::PlonkSpongeConstantsKimchi, sponge::DefaultFqSponge, FqSponge}; use poly_commitment::{ - commitment::CommitmentCurve, - ipa::{DensePolynomialOrEvaluations, SRS}, - PolyComm, SRS as _, + commitment::CommitmentCurve, ipa::SRS, utils::DensePolynomialOrEvaluations, PolyComm, SRS as _, }; fn benchmark_ipa_open(c: &mut Criterion) { diff --git a/poly-commitment/src/ipa.rs b/poly-commitment/src/ipa.rs index aeea83c584..c56fc2d13e 100644 --- a/poly-commitment/src/ipa.rs +++ b/poly-commitment/src/ipa.rs @@ -5,18 +5,18 @@ use crate::{ commitment::{ - b_poly, b_poly_coefficients, combine_commitments, shift_scalar, BatchEvaluationProof, - CommitmentCurve, *, + b_poly, b_poly_coefficients, combine_commitments, shift_scalar, squeeze_challenge, + squeeze_prechallenge, BatchEvaluationProof, CommitmentCurve, EndoCurve, }, error::CommitmentError, hash_map_cache::HashMapCache, + utils::combine_polys, BlindedCommitment, PolyComm, PolynomialsToCombine, SRS as SRSTrait, }; use ark_ec::{AffineRepr, CurveGroup, VariableBaseMSM}; -use ark_ff::{BigInteger, FftField, Field, One, PrimeField, UniformRand, Zero}; +use ark_ff::{BigInteger, Field, One, PrimeField, UniformRand, Zero}; use ark_poly::{ - univariate::DensePolynomial, DenseUVPolynomial, EvaluationDomain, Evaluations, - Radix2EvaluationDomain as D, + univariate::DensePolynomial, EvaluationDomain, Evaluations, Radix2EvaluationDomain as D, }; use ark_serialize::{CanonicalDeserialize, CanonicalSerialize}; use blake2::{Blake2b512, Digest}; @@ -24,7 +24,7 @@ use groupmap::GroupMap; use mina_poseidon::{sponge::ScalarChallenge, FqSponge}; use o1_utils::{ field_helpers::{inner_prod, pows}, - math, ExtendedDensePolynomial, + math, }; use rand::{CryptoRng, RngCore}; use rayon::prelude::*; @@ -32,188 +32,6 @@ use serde::{Deserialize, Serialize}; use serde_with::serde_as; use std::{cmp::min, iter::Iterator, ops::AddAssign}; -/// A formal sum of the form -/// `s_0 * p_0 + ... s_n * p_n` -/// where each `s_i` is a scalar and each `p_i` is a polynomial. -/// The parameter `P` is expected to be the coefficients of the polynomial -/// `p_i`, even though we could treat it as the evaluations. -/// -/// This hypothesis is important if `to_dense_polynomial` is called. -#[derive(Default)] -struct ScaledChunkedPolynomial(Vec<(F, P)>); - -/// Represent a polynomial either with its coefficients or its evaluations -pub enum DensePolynomialOrEvaluations<'a, F: FftField, D: EvaluationDomain> { - /// Polynomial represented by its coefficients - DensePolynomial(&'a DensePolynomial), - /// Polynomial represented by its evaluations over a domain D - Evaluations(&'a Evaluations, D), -} - -impl ScaledChunkedPolynomial { - fn add_poly(&mut self, scale: F, p: P) { - self.0.push((scale, p)) - } -} - -impl<'a, F: Field> ScaledChunkedPolynomial { - /// Compute the resulting scaled polynomial. - /// Example: - /// Given the two polynomials `1 + 2X` and `3 + 4X`, and the scaling - /// factors `2` and `3`, the result is the polynomial `11 + 16X`. - /// ```text - /// 2 * [1, 2] + 3 * [3, 4] = [2, 4] + [9, 12] = [11, 16] - /// ``` - fn to_dense_polynomial(&self) -> DensePolynomial { - // Note: using a reference to avoid reallocation of the result. - let mut res = DensePolynomial::::zero(); - - let scaled: Vec<_> = self - .0 - .par_iter() - .map(|(scale, segment)| { - let scale = *scale; - // We simply scale each coefficients. - // It is simply because DensePolynomial doesn't have a method - // `scale`. - let v = segment.par_iter().map(|x| scale * *x).collect(); - DensePolynomial::from_coefficients_vec(v) - }) - .collect(); - - for p in scaled { - res += &p; - } - - res - } -} - -/// Combine the polynomials using a scalar (`polyscale`), creating a single -/// unified polynomial to open. This function also accepts polynomials in -/// evaluations form. In this case it applies an IFFT, and, if necessarry, -/// applies chunking to it (ie. split it in multiple polynomials of -/// degree less than the SRS size). -/// Parameters: -/// - plnms: vector of polynomials, either in evaluations or coefficients form. -/// The order of the output follows the order of this structure. -/// - polyscale: scalar to combine the polynomials, which will be scaled based -/// on the number of polynomials to combine. -/// -/// Example: -/// Given the three polynomials `p1(X)`, and `p3(X)` in coefficients -/// forms, p2(X) in evaluation form, -/// and the scaling factor `polyscale`, the result will be the polynomial: -/// -/// ```text -/// p1(X) + polyscale * i_fft(chunks(p2))(X) + polyscale^2 p3(X) -/// ``` -/// -/// Additional complexity is added to handle chunks. -// TODO: move into utils? It is useful for multiple PCS -pub fn combine_polys>( - plnms: PolynomialsToCombine, - polyscale: G::ScalarField, - srs_length: usize, -) -> (DensePolynomial, G::ScalarField) { - // Initialising the output for the combined coefficients forms - let mut plnm_coefficients = - ScaledChunkedPolynomial::::default(); - // Initialising the output for the combined evaluations forms - let mut plnm_evals_part = { - // For now just check that all the evaluation polynomials are the same - // degree so that we can do just a single FFT. - // If/when we change this, we can add more complicated code to handle - // different degrees. - let degree = plnms - .iter() - .fold(None, |acc, (p, _)| match p { - DensePolynomialOrEvaluations::DensePolynomial(_) => acc, - DensePolynomialOrEvaluations::Evaluations(_, d) => { - if let Some(n) = acc { - assert_eq!(n, d.size()); - } - Some(d.size()) - } - }) - .unwrap_or(0); - vec![G::ScalarField::zero(); degree] - }; - - // Will contain ∑ comm_chunk * polyscale^i - let mut combined_comm = G::ScalarField::zero(); - - // Will contain polyscale^i - let mut polyscale_to_i = G::ScalarField::one(); - - // Iterating over polynomials in the batch. - // Note that the chunks in the commitment `p_i_comm` are given as `PolyComm`. They are - // evaluations. - // We do modify two different structures depending on the form of the - // polynomial we are currently processing: `plnm` and `plnm_evals_part`. - // We do need to treat both forms separately. - for (p_i, p_i_comm) in plnms { - match p_i { - // Here we scale the polynomial in evaluations forms - // Note that based on the check above, sub_domain.size() always give - // the same value - DensePolynomialOrEvaluations::Evaluations(evals_i, sub_domain) => { - let stride = evals_i.evals.len() / sub_domain.size(); - let evals = &evals_i.evals; - plnm_evals_part - .par_iter_mut() - .enumerate() - .for_each(|(i, x)| { - *x += polyscale_to_i * evals[i * stride]; - }); - for comm_chunk in p_i_comm.into_iter() { - combined_comm += &(*comm_chunk * polyscale_to_i); - polyscale_to_i *= &polyscale; - } - } - - // Here we scale the polynomial in coefficient forms - DensePolynomialOrEvaluations::DensePolynomial(p_i) => { - let mut offset = 0; - // iterating over chunks of the polynomial - for comm_chunk in p_i_comm.into_iter() { - let segment = &p_i.coeffs[std::cmp::min(offset, p_i.coeffs.len()) - ..std::cmp::min(offset + srs_length, p_i.coeffs.len())]; - plnm_coefficients.add_poly(polyscale_to_i, segment); - - combined_comm += &(*comm_chunk * polyscale_to_i); - polyscale_to_i *= &polyscale; - offset += srs_length; - } - } - } - } - - // Now, we will combine both evaluations and coefficients forms - - // plnm will be our final combined polynomial. We first treat the - // polynomials in coefficients forms, which is simply scaling the - // coefficients and add them. - let mut combined_plnm = plnm_coefficients.to_dense_polynomial(); - - if !plnm_evals_part.is_empty() { - // n is the number of evaluations, which is a multiple of the - // domain size. - // We treat now each chunk. - let n = plnm_evals_part.len(); - let max_poly_size = srs_length; - // equiv to divceil, but unstable in rust < 1.73. - let num_chunks = n / max_poly_size + if n % max_poly_size == 0 { 0 } else { 1 }; - // Interpolation on the whole domain, i.e. it can be d2, d4, etc. - combined_plnm += &Evaluations::from_vec_and_domain(plnm_evals_part, D::new(n).unwrap()) - .interpolate() - .to_chunked_polynomial(num_chunks, max_poly_size) - .linearize(polyscale); - } - - (combined_plnm, combined_comm) -} - #[serde_as] #[derive(Debug, Clone, Default, Serialize, Deserialize)] #[serde(bound = "G: CanonicalDeserialize + CanonicalSerialize")] diff --git a/poly-commitment/src/kzg.rs b/poly-commitment/src/kzg.rs index 8d4d8ed7c6..958b2b494c 100644 --- a/poly-commitment/src/kzg.rs +++ b/poly-commitment/src/kzg.rs @@ -10,9 +10,8 @@ //! parameter. use crate::{ - commitment::*, - ipa::{combine_polys, SRS}, - CommitmentError, PolynomialsToCombine, SRS as SRSTrait, + commitment::*, ipa::SRS, utils::combine_polys, CommitmentError, PolynomialsToCombine, + SRS as SRSTrait, }; use ark_ec::{pairing::Pairing, AffineRepr, VariableBaseMSM}; diff --git a/poly-commitment/src/lib.rs b/poly-commitment/src/lib.rs index d6389a4203..9037a0a6ae 100644 --- a/poly-commitment/src/lib.rs +++ b/poly-commitment/src/lib.rs @@ -4,6 +4,7 @@ pub mod error; pub mod hash_map_cache; pub mod ipa; pub mod kzg; +pub mod utils; // Exposing property based tests for the SRS trait pub mod pbt_srs; @@ -13,7 +14,7 @@ pub use commitment::PolyComm; use crate::{ commitment::{BatchEvaluationProof, BlindedCommitment, CommitmentCurve}, error::CommitmentError, - ipa::DensePolynomialOrEvaluations, + utils::DensePolynomialOrEvaluations, }; use ark_ec::AffineRepr; use ark_ff::UniformRand; diff --git a/poly-commitment/src/utils.rs b/poly-commitment/src/utils.rs new file mode 100644 index 0000000000..4dea685144 --- /dev/null +++ b/poly-commitment/src/utils.rs @@ -0,0 +1,186 @@ +use crate::{commitment::CommitmentCurve, PolynomialsToCombine}; +use ark_ff::{FftField, Field, One, Zero}; +use ark_poly::{univariate::DensePolynomial, DenseUVPolynomial, EvaluationDomain, Evaluations}; +use o1_utils::ExtendedDensePolynomial; +use rayon::prelude::*; + +/// Represent a polynomial either with its coefficients or its evaluations +pub enum DensePolynomialOrEvaluations<'a, F: FftField, D: EvaluationDomain> { + /// Polynomial represented by its coefficients + DensePolynomial(&'a DensePolynomial), + /// Polynomial represented by its evaluations over a domain D + Evaluations(&'a Evaluations, D), +} + +/// A formal sum of the form +/// `s_0 * p_0 + ... s_n * p_n` +/// where each `s_i` is a scalar and each `p_i` is a polynomial. +/// The parameter `P` is expected to be the coefficients of the polynomial +/// `p_i`, even though we could treat it as the evaluations. +/// +/// This hypothesis is important if `to_dense_polynomial` is called. +#[derive(Default)] +struct ScaledChunkedPolynomial(Vec<(F, P)>); + +impl ScaledChunkedPolynomial { + fn add_poly(&mut self, scale: F, p: P) { + self.0.push((scale, p)) + } +} + +impl<'a, F: Field> ScaledChunkedPolynomial { + /// Compute the resulting scaled polynomial. + /// Example: + /// Given the two polynomials `1 + 2X` and `3 + 4X`, and the scaling + /// factors `2` and `3`, the result is the polynomial `11 + 16X`. + /// ```text + /// 2 * [1, 2] + 3 * [3, 4] = [2, 4] + [9, 12] = [11, 16] + /// ``` + fn to_dense_polynomial(&self) -> DensePolynomial { + // Note: using a reference to avoid reallocation of the result. + let mut res = DensePolynomial::::zero(); + + let scaled: Vec<_> = self + .0 + .par_iter() + .map(|(scale, segment)| { + let scale = *scale; + // We simply scale each coefficients. + // It is simply because DensePolynomial doesn't have a method + // `scale`. + let v = segment.par_iter().map(|x| scale * *x).collect(); + DensePolynomial::from_coefficients_vec(v) + }) + .collect(); + + for p in scaled { + res += &p; + } + + res + } +} + +/// Combine the polynomials using a scalar (`polyscale`), creating a single +/// unified polynomial to open. This function also accepts polynomials in +/// evaluations form. In this case it applies an IFFT, and, if necessarry, +/// applies chunking to it (ie. split it in multiple polynomials of +/// degree less than the SRS size). +/// Parameters: +/// - plnms: vector of polynomials, either in evaluations or coefficients form. +/// The order of the output follows the order of this structure. +/// - polyscale: scalar to combine the polynomials, which will be scaled based +/// on the number of polynomials to combine. +/// +/// Example: +/// Given the three polynomials `p1(X)`, and `p3(X)` in coefficients +/// forms, p2(X) in evaluation form, +/// and the scaling factor `polyscale`, the result will be the polynomial: +/// +/// ```text +/// p1(X) + polyscale * i_fft(chunks(p2))(X) + polyscale^2 p3(X) +/// ``` +/// +/// Additional complexity is added to handle chunks. +pub fn combine_polys>( + plnms: PolynomialsToCombine, + polyscale: G::ScalarField, + srs_length: usize, +) -> (DensePolynomial, G::ScalarField) { + // Initialising the output for the combined coefficients forms + let mut plnm_coefficients = + ScaledChunkedPolynomial::::default(); + // Initialising the output for the combined evaluations forms + let mut plnm_evals_part = { + // For now just check that all the evaluation polynomials are the same + // degree so that we can do just a single FFT. + // If/when we change this, we can add more complicated code to handle + // different degrees. + let degree = plnms + .iter() + .fold(None, |acc, (p, _)| match p { + DensePolynomialOrEvaluations::DensePolynomial(_) => acc, + DensePolynomialOrEvaluations::Evaluations(_, d) => { + if let Some(n) = acc { + assert_eq!(n, d.size()); + } + Some(d.size()) + } + }) + .unwrap_or(0); + vec![G::ScalarField::zero(); degree] + }; + + // Will contain ∑ comm_chunk * polyscale^i + let mut combined_comm = G::ScalarField::zero(); + + // Will contain polyscale^i + let mut polyscale_to_i = G::ScalarField::one(); + + // Iterating over polynomials in the batch. + // Note that the chunks in the commitment `p_i_comm` are given as `PolyComm`. They are + // evaluations. + // We do modify two different structures depending on the form of the + // polynomial we are currently processing: `plnm` and `plnm_evals_part`. + // We do need to treat both forms separately. + for (p_i, p_i_comm) in plnms { + match p_i { + // Here we scale the polynomial in evaluations forms + // Note that based on the check above, sub_domain.size() always give + // the same value + DensePolynomialOrEvaluations::Evaluations(evals_i, sub_domain) => { + let stride = evals_i.evals.len() / sub_domain.size(); + let evals = &evals_i.evals; + plnm_evals_part + .par_iter_mut() + .enumerate() + .for_each(|(i, x)| { + *x += polyscale_to_i * evals[i * stride]; + }); + for comm_chunk in p_i_comm.into_iter() { + combined_comm += &(*comm_chunk * polyscale_to_i); + polyscale_to_i *= &polyscale; + } + } + + // Here we scale the polynomial in coefficient forms + DensePolynomialOrEvaluations::DensePolynomial(p_i) => { + let mut offset = 0; + // iterating over chunks of the polynomial + for comm_chunk in p_i_comm.into_iter() { + let segment = &p_i.coeffs[std::cmp::min(offset, p_i.coeffs.len()) + ..std::cmp::min(offset + srs_length, p_i.coeffs.len())]; + plnm_coefficients.add_poly(polyscale_to_i, segment); + + combined_comm += &(*comm_chunk * polyscale_to_i); + polyscale_to_i *= &polyscale; + offset += srs_length; + } + } + } + } + + // Now, we will combine both evaluations and coefficients forms + + // plnm will be our final combined polynomial. We first treat the + // polynomials in coefficients forms, which is simply scaling the + // coefficients and add them. + let mut combined_plnm = plnm_coefficients.to_dense_polynomial(); + + if !plnm_evals_part.is_empty() { + // n is the number of evaluations, which is a multiple of the + // domain size. + // We treat now each chunk. + let n = plnm_evals_part.len(); + let max_poly_size = srs_length; + // equiv to divceil, but unstable in rust < 1.73. + let num_chunks = n / max_poly_size + if n % max_poly_size == 0 { 0 } else { 1 }; + // Interpolation on the whole domain, i.e. it can be d2, d4, etc. + combined_plnm += &Evaluations::from_vec_and_domain(plnm_evals_part, D::new(n).unwrap()) + .interpolate() + .to_chunked_polynomial(num_chunks, max_poly_size) + .linearize(polyscale); + } + + (combined_plnm, combined_comm) +} diff --git a/poly-commitment/tests/batch_15_wires.rs b/poly-commitment/tests/batch_15_wires.rs index 0efbc27170..eafeba8f5b 100644 --- a/poly-commitment/tests/batch_15_wires.rs +++ b/poly-commitment/tests/batch_15_wires.rs @@ -12,7 +12,8 @@ use mina_poseidon::{ use o1_utils::ExtendedDensePolynomial as _; use poly_commitment::{ commitment::{combined_inner_product, BatchEvaluationProof, CommitmentCurve, Evaluation}, - ipa::{DensePolynomialOrEvaluations, SRS}, + ipa::SRS, + utils::DensePolynomialOrEvaluations, SRS as _, }; use rand::Rng; diff --git a/poly-commitment/tests/commitment.rs b/poly-commitment/tests/commitment.rs index dac48427c4..b22b1e9853 100644 --- a/poly-commitment/tests/commitment.rs +++ b/poly-commitment/tests/commitment.rs @@ -14,7 +14,8 @@ use poly_commitment::{ combined_inner_product, BatchEvaluationProof, BlindedCommitment, CommitmentCurve, Evaluation, PolyComm, }, - ipa::{DensePolynomialOrEvaluations, OpeningProof, SRS}, + ipa::{OpeningProof, SRS}, + utils::DensePolynomialOrEvaluations, SRS as _, }; use rand::{CryptoRng, Rng, SeedableRng}; diff --git a/poly-commitment/tests/ipa_commitment.rs b/poly-commitment/tests/ipa_commitment.rs index 9bf96a1c06..bbab4def03 100644 --- a/poly-commitment/tests/ipa_commitment.rs +++ b/poly-commitment/tests/ipa_commitment.rs @@ -11,8 +11,10 @@ use mina_poseidon::{ use o1_utils::ExtendedDensePolynomial; use poly_commitment::{ commitment::{combined_inner_product, BatchEvaluationProof, CommitmentCurve, Evaluation}, - ipa::{DensePolynomialOrEvaluations, SRS}, - pbt_srs, PolyComm, SRS as _, + ipa::SRS, + pbt_srs, + utils::DensePolynomialOrEvaluations, + PolyComm, SRS as _, }; use rand::Rng; use std::array; diff --git a/poly-commitment/tests/kzg.rs b/poly-commitment/tests/kzg.rs index 682b5eb9f8..0b553fa1fb 100644 --- a/poly-commitment/tests/kzg.rs +++ b/poly-commitment/tests/kzg.rs @@ -9,9 +9,11 @@ use ark_serialize::{CanonicalDeserialize, CanonicalSerialize}; use mina_curves::pasta::{Fp, Vesta as VestaG}; use poly_commitment::{ commitment::Evaluation, - ipa::{DensePolynomialOrEvaluations, SRS}, + ipa::SRS, kzg::{combine_evaluations, KZGProof, PairingSRS}, - pbt_srs, PolyComm, SRS as _, + pbt_srs, + utils::DensePolynomialOrEvaluations, + PolyComm, SRS as _, }; #[test] From 42002f8cb12274678ed48ada1c8facda25d5329c Mon Sep 17 00:00:00 2001 From: Mikhail Volkhov Date: Wed, 20 Nov 2024 16:48:32 +0000 Subject: [PATCH 07/63] Rename erroneous d1_size into num_chunks in prover --- kimchi/src/prover.rs | 14 +++++++------- msm/src/prover.rs | 8 ++++---- 2 files changed, 11 insertions(+), 11 deletions(-) diff --git a/kimchi/src/prover.rs b/kimchi/src/prover.rs index 755592ca60..b135d20836 100644 --- a/kimchi/src/prover.rs +++ b/kimchi/src/prover.rs @@ -1238,8 +1238,12 @@ where //~ 1. Create a list of all polynomials that will require evaluations //~ (and evaluation proofs) in the protocol. //~ First, include the previous challenges, in case we are in a recursive prover. - let non_hiding = |d1_size: usize| PolyComm { - chunks: vec![G::ScalarField::zero(); d1_size], + let non_hiding = |n_chunks: usize| PolyComm { + chunks: vec![G::ScalarField::zero(); n_chunks], + }; + + let fixed_hiding = |n_chunks: usize| PolyComm { + chunks: vec![G::ScalarField::one(); n_chunks], }; let coefficients_form = DensePolynomialOrEvaluations::DensePolynomial; @@ -1247,13 +1251,9 @@ where let mut polynomials = polys .iter() - .map(|(p, d1_size)| (coefficients_form(p), non_hiding(*d1_size))) + .map(|(p, n_chunks)| (coefficients_form(p), non_hiding(*n_chunks))) .collect::>(); - let fixed_hiding = |d1_size: usize| PolyComm { - chunks: vec![G::ScalarField::one(); d1_size], - }; - //~ 1. Then, include: //~~ * the negated public polynomial //~~ * the ft polynomial diff --git a/msm/src/prover.rs b/msm/src/prover.rs index 53cab9b287..2ea2534da2 100644 --- a/msm/src/prover.rs +++ b/msm/src/prover.rs @@ -490,11 +490,11 @@ where let u = u_chal.to_field(endo_r); let coefficients_form = DensePolynomialOrEvaluations::DensePolynomial; - let non_hiding = |d1_size| PolyComm { - chunks: vec![G::ScalarField::zero(); d1_size], + let non_hiding = |n_chunks| PolyComm { + chunks: vec![G::ScalarField::zero(); n_chunks], }; - let hiding = |d1_size| PolyComm { - chunks: vec![G::ScalarField::one(); d1_size], + let hiding = |n_chunks| PolyComm { + chunks: vec![G::ScalarField::one(); n_chunks], }; // Gathering all polynomials to use in the opening proof From 0ba848267cb52edd9c4c61403337682d9355e262 Mon Sep 17 00:00:00 2001 From: Mikhail Volkhov Date: Wed, 20 Nov 2024 16:53:53 +0000 Subject: [PATCH 08/63] More comments on ipa#open --- poly-commitment/src/ipa.rs | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) diff --git a/poly-commitment/src/ipa.rs b/poly-commitment/src/ipa.rs index c56fc2d13e..77b98c99a1 100644 --- a/poly-commitment/src/ipa.rs +++ b/poly-commitment/src/ipa.rs @@ -568,15 +568,17 @@ impl SRS { // Combines polynomials roughly as follows: p(X) := ∑_i polyscale^i p_i(X) // // `blinding_factor` is a combined set of commitments that are - // paired with polynomials in `plnms`. + // paired with polynomials in `plnms`. In kimchi, these input commitments + // are blinders, so often `[G::ScalarField::one(); num_chunks]` or zeroes. let (p, blinding_factor) = combine_polys::(plnms, polyscale, self.g.len()); // The initial evaluation vector for polynomial commitment b_init is not - // just the powers of a single point as in the original IPA, but rather - // a vector of linearly combined powers with `evalscale` as recombiner. + // just the powers of a single point as in the original IPA (1,ζ,ζ^2,...) + // + // but rather a vector of linearly combined powers with `evalscale` as recombiner. // // b_init[j] = Σ_i evalscale^i elm_i^j - // = ζ^j + evalscale * ζ^j ω^j (in the specific case of opening) + // = ζ^j + evalscale * ζ^j ω^j (in the specific case of challenges (ζ,ζω)) let b_init = { // randomise/scale the eval powers let mut scale = G::ScalarField::one(); From d694a2270452d2ad00e128b28d07eeeb401a22fd Mon Sep 17 00:00:00 2001 From: Mikhail Volkhov Date: Wed, 20 Nov 2024 17:58:28 +0000 Subject: [PATCH 09/63] Improve combine_poly docs --- poly-commitment/src/utils.rs | 13 +++++++++---- 1 file changed, 9 insertions(+), 4 deletions(-) diff --git a/poly-commitment/src/utils.rs b/poly-commitment/src/utils.rs index 4dea685144..fc43883aff 100644 --- a/poly-commitment/src/utils.rs +++ b/poly-commitment/src/utils.rs @@ -66,11 +66,16 @@ impl<'a, F: Field> ScaledChunkedPolynomial { /// evaluations form. In this case it applies an IFFT, and, if necessarry, /// applies chunking to it (ie. split it in multiple polynomials of /// degree less than the SRS size). +/// /// Parameters: -/// - plnms: vector of polynomials, either in evaluations or coefficients form. -/// The order of the output follows the order of this structure. -/// - polyscale: scalar to combine the polynomials, which will be scaled based -/// on the number of polynomials to combine. +/// - `plnms`: vector of polynomials, either in evaluations or coefficients form, together with +/// a set of scalars representing their blinders. +/// - `polyscale`: scalar to combine the polynomials, which will be scaled based on the number of +/// polynomials to combine. +/// +/// Output: +/// - `combined_poly`: combined polynomial. The order of the output follows the order of `plnms`. +/// - `combined_comm`: combined scalars representing the blinder commitment. /// /// Example: /// Given the three polynomials `p1(X)`, and `p3(X)` in coefficients From b3ef6eab6fdc0cee34c3de2ddeb14012c2dd2bc1 Mon Sep 17 00:00:00 2001 From: Mikhail Volkhov Date: Wed, 20 Nov 2024 17:59:08 +0000 Subject: [PATCH 10/63] Improve docs for PolynomialsToCombine --- poly-commitment/src/lib.rs | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/poly-commitment/src/lib.rs b/poly-commitment/src/lib.rs index 9037a0a6ae..06e546a9e7 100644 --- a/poly-commitment/src/lib.rs +++ b/poly-commitment/src/lib.rs @@ -169,8 +169,9 @@ pub trait SRS: Clone + Sized { } #[allow(type_alias_bounds)] -/// Simply an alias to represent a polynomial with its commitment, possibly with -/// a blinder. +/// An alias to represent a polynomial (in either coefficient or +/// evaluation form), with a set of *scalar field* elements that +/// represent the exponent of its blinder. // TODO: add a string to name the polynomial type PolynomialsToCombine<'a, G: CommitmentCurve, D: EvaluationDomain> = &'a [( DensePolynomialOrEvaluations<'a, G::ScalarField, D>, From 654266619ec4660f11b8c4256dd7d5849a9fef11 Mon Sep 17 00:00:00 2001 From: Mikhail Volkhov Date: Wed, 20 Nov 2024 17:59:40 +0000 Subject: [PATCH 11/63] Improve docs for IPA, improve some variable names --- poly-commitment/src/ipa.rs | 55 +++++++++++++++++++++++++------------- 1 file changed, 36 insertions(+), 19 deletions(-) diff --git a/poly-commitment/src/ipa.rs b/poly-commitment/src/ipa.rs index 77b98c99a1..d68216f67c 100644 --- a/poly-commitment/src/ipa.rs +++ b/poly-commitment/src/ipa.rs @@ -183,8 +183,8 @@ impl SRS { { sponge.absorb_fr(&[shift_scalar::(*combined_inner_product)]); - let t = sponge.challenge_fq(); - let u: G = { + let u_base: G = { + let t = sponge.challenge_fq(); let (x, y) = group_map.to_group(t); G::of_coordinates(x, y) }; @@ -240,7 +240,7 @@ impl SRS { // TERM // -rand_base_i * (z1 * b0 * U) scalars.push(neg_rand_base_i * (opening.z1 * b0)); - points.push(u); + points.push(u_base); // TERM // rand_base_i c_i Q_i @@ -269,7 +269,7 @@ impl SRS { ); scalars.push(rand_base_i_c_i * *combined_inner_product); - points.push(u); + points.push(u_base); scalars.push(rand_base_i); points.push(opening.delta); @@ -569,7 +569,7 @@ impl SRS { // // `blinding_factor` is a combined set of commitments that are // paired with polynomials in `plnms`. In kimchi, these input commitments - // are blinders, so often `[G::ScalarField::one(); num_chunks]` or zeroes. + // are poly com blinders, so often `[G::ScalarField::one(); num_chunks]` or zeroes. let (p, blinding_factor) = combine_polys::(plnms, polyscale, self.g.len()); // The initial evaluation vector for polynomial commitment b_init is not @@ -579,6 +579,13 @@ impl SRS { // // b_init[j] = Σ_i evalscale^i elm_i^j // = ζ^j + evalscale * ζ^j ω^j (in the specific case of challenges (ζ,ζω)) + // + // So in our case b_init is the following vector: + // 1 + evalscale + // ζ + evalscale * ζ ω + // ζ^2 + evalscale * (ζ ω)^2 + // ζ^3 + evalscale * (ζ ω)^3 + // ... let b_init = { // randomise/scale the eval powers let mut scale = G::ScalarField::one(); @@ -593,7 +600,7 @@ impl SRS { res }; - // Combined polynomial p, evaluated at the combined point b_init. + // Combined polynomial p(X) evaluated at the combined eval point b_init. let combined_inner_product = p .coeffs .iter() @@ -610,8 +617,9 @@ impl SRS { // See the `shift_scalar`` doc. sponge.absorb_fr(&[shift_scalar::(combined_inner_product)]); - let t = sponge.challenge_fq(); - let u: G = { + // Generate another randomisation base U; our commitments will be w.r.t bases {G_i},H,U. + let u_base: G = { + let t = sponge.challenge_fq(); let (x, y) = group_map.to_group(t); G::of_coordinates(x, y) }; @@ -645,7 +653,7 @@ impl SRS { // Pedersen commitment to a_lo,rand_l, let l = G::Group::msm_bigint( - &[g_lo, &[self.h, u]].concat(), + &[g_lo, &[self.h, u_base]].concat(), &[a_hi, &[rand_l, inner_prod(a_hi, b_lo)]] .concat() .iter() @@ -655,7 +663,7 @@ impl SRS { .into_affine(); let r = G::Group::msm_bigint( - &[g_hi, &[self.h, u]].concat(), + &[g_hi, &[self.h, u_base]].concat(), &[a_lo, &[rand_r, inner_prod(a_lo, b_hi)]] .concat() .iter() @@ -670,7 +678,9 @@ impl SRS { sponge.absorb_g(&[l]); sponge.absorb_g(&[r]); - // Round #i challenges + // Round #i challenges; + // - not to be confused with "u_base" + // - not to be confused with "u" as "polyscale" let u_pre = squeeze_prechallenge(&mut sponge); let u = u_pre.to_field(&endo_r); let u_inv = u.inverse().unwrap(); @@ -716,11 +726,15 @@ impl SRS { let b0 = b[0]; let g0 = g[0]; - // Schnorr/Sigma-protocol part - - // r_prime = blinding_factor + \sum_i (rand_l[i] * (u[i]^{-1}) + rand_r * u[i]) - // where u is a vector of folding challenges, and rand_l/rand_r are - // intermediate L/R blinders + // Compute r_prime, a folded blinder. It combines blinders on + // each individual step of the IPA folding process together + // with the final blinding_factor of the polynomial. + // + // r_prime := ∑_i (rand_l[i] * u[i]^{-1} + rand_r * u[i]) + // + blinding_factor + // + // where u is a vector of folding challenges, and rand_l/rand_r are + // intermediate L/R blinders. let r_prime = blinders .iter() .zip(chals.iter().zip(chal_invs.iter())) @@ -730,13 +744,16 @@ impl SRS { let d = ::rand(rng); let r_delta = ::rand(rng); - // delta = (g0 + u*b0)*d + h*r_delta - let delta = ((g0.into_group() + (u.mul(b0))).into_affine().mul(d) + self.h.mul(r_delta)) - .into_affine(); + // Compute delta, the commitment + // delta = G0^d * U_base^{b0*d} * H^r_delta (as a group element, in multiplicative notation) + let delta = ((g0.into_group() + (u_base.mul(b0))).into_affine().mul(d) + + self.h.mul(r_delta)) + .into_affine(); sponge.absorb_g(&[delta]); let c = ScalarChallenge(sponge.challenge()).to_field(&endo_r); + // (?) Schnorr-like responses showing the knowledge of r_prime and a0. let z1 = a0 * c + d; let z2 = r_prime * c + r_delta; From b48338f3ba2862bd2cc88ccc010ed722825f5bd9 Mon Sep 17 00:00:00 2001 From: Danny Willems Date: Thu, 21 Nov 2024 19:31:01 +0100 Subject: [PATCH 12/63] Revert "add elf parser test" This reverts commit 3fdda8e30889167cbd355d26ebf7685f279b5132. --- o1vm/tests/test_riscv_elf.rs | 17 ----------------- 1 file changed, 17 deletions(-) diff --git a/o1vm/tests/test_riscv_elf.rs b/o1vm/tests/test_riscv_elf.rs index a2669d9926..7b278a3a8e 100644 --- a/o1vm/tests/test_riscv_elf.rs +++ b/o1vm/tests/test_riscv_elf.rs @@ -5,23 +5,6 @@ use o1vm::interpreters::riscv32im::{ PAGE_SIZE, }; -#[test] -// This test is used to check that the elf loader is working correctly. -// We must export the code used in this test in a function that can be called by -// the o1vm at load time. -fn test_correctly_parsing_elf() { - let curr_dir = std::env::current_dir().unwrap(); - let path = curr_dir.join(std::path::PathBuf::from( - "resources/programs/riscv32i/fibonacci", - )); - let state = o1vm::elf_loader::parse_riscv32i(&path).unwrap(); - // This is the output we get by running objdump -d fibonacci - assert_eq!(state.pc, 69932); - - assert_eq!(state.memory.len(), 1); - assert_eq!(state.memory[0].index, 17); -} - #[test] // Checking an instruction can be converted into a string. // It is mostly because we would want to use it to debug or write better error From d9371ea1a6830792f8e862868ec4079bc775ed2e Mon Sep 17 00:00:00 2001 From: Danny Willems Date: Wed, 20 Nov 2024 16:21:01 +0100 Subject: [PATCH 13/63] o1vm/riscv32: implement mul_hi_signed --- o1vm/src/interpreters/riscv32im/constraints.rs | 9 +++++++++ o1vm/src/interpreters/riscv32im/interpreter.rs | 14 ++++++++++++++ o1vm/src/interpreters/riscv32im/witness.rs | 15 +++++++++++++++ 3 files changed, 38 insertions(+) diff --git a/o1vm/src/interpreters/riscv32im/constraints.rs b/o1vm/src/interpreters/riscv32im/constraints.rs index c8b7bec2c2..11dee8a230 100644 --- a/o1vm/src/interpreters/riscv32im/constraints.rs +++ b/o1vm/src/interpreters/riscv32im/constraints.rs @@ -327,6 +327,15 @@ impl InterpreterEnv for Env { (self.variable(position_hi), self.variable(position_lo)) } + unsafe fn mul_hi_signed( + &mut self, + _x: &Self::Variable, + _y: &Self::Variable, + position: Self::Position, + ) -> Self::Variable { + self.variable(position) + } + unsafe fn mul_hi_lo( &mut self, _x: &Self::Variable, diff --git a/o1vm/src/interpreters/riscv32im/interpreter.rs b/o1vm/src/interpreters/riscv32im/interpreter.rs index 6eeaa28623..1e41918b20 100644 --- a/o1vm/src/interpreters/riscv32im/interpreter.rs +++ b/o1vm/src/interpreters/riscv32im/interpreter.rs @@ -1201,6 +1201,20 @@ pub trait InterpreterEnv { position: Self::Position, ) -> Self::Variable; + /// Returns `((x * y) >> 32`, storing the results in `position`. + /// + /// # Safety + /// + /// There are no constraints on the returned values; callers must manually add constraints to + /// ensure that the pair of returned values correspond to the given values `x` and `y`, and + /// that they fall within the desired range. + unsafe fn mul_hi_signed( + &mut self, + x: &Self::Variable, + y: &Self::Variable, + position: Self::Position, + ) -> Self::Variable; + /// Returns `((x * y) >> 32, (x * y) & ((1 << 32) - 1))`, storing the results in `position_hi` /// and `position_lo` respectively. /// diff --git a/o1vm/src/interpreters/riscv32im/witness.rs b/o1vm/src/interpreters/riscv32im/witness.rs index 1fbe44552b..b0d2adccda 100644 --- a/o1vm/src/interpreters/riscv32im/witness.rs +++ b/o1vm/src/interpreters/riscv32im/witness.rs @@ -441,6 +441,21 @@ impl InterpreterEnv for Env { res } + unsafe fn mul_hi_signed( + &mut self, + x: &Self::Variable, + y: &Self::Variable, + position: Self::Position, + ) -> Self::Variable { + let x: u32 = (*x).try_into().unwrap(); + let y: u32 = (*y).try_into().unwrap(); + let res = (((x as i32) as i64) * ((y as i32) as i64)) as u64; + let res = (res >> 32) as u32; + let res = res as u64; + self.write_column(position, res); + res + } + unsafe fn mul_hi_lo_signed( &mut self, x: &Self::Variable, From 1e918140dafaa89c721f47928a0341b952740363 Mon Sep 17 00:00:00 2001 From: Sai Vegasena Date: Thu, 21 Nov 2024 20:08:34 +0100 Subject: [PATCH 14/63] o1vm/riscv32im: simplify mul_hi_signed --- o1vm/src/interpreters/riscv32im/witness.rs | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/o1vm/src/interpreters/riscv32im/witness.rs b/o1vm/src/interpreters/riscv32im/witness.rs index b0d2adccda..0418852ae9 100644 --- a/o1vm/src/interpreters/riscv32im/witness.rs +++ b/o1vm/src/interpreters/riscv32im/witness.rs @@ -447,10 +447,10 @@ impl InterpreterEnv for Env { y: &Self::Variable, position: Self::Position, ) -> Self::Variable { - let x: u32 = (*x).try_into().unwrap(); - let y: u32 = (*y).try_into().unwrap(); - let res = (((x as i32) as i64) * ((y as i32) as i64)) as u64; - let res = (res >> 32) as u32; + let x: i32 = (*x).try_into().unwrap(); + let y: i32 = (*y).try_into().unwrap(); + let res = (x as i64) * (y as i64); + let res = (res >> 32) as i32; let res = res as u64; self.write_column(position, res); res From 7f2d2fe67ee2e48ec3a4756d3e75d8743f2fd62d Mon Sep 17 00:00:00 2001 From: Danny Willems Date: Thu, 21 Nov 2024 08:56:11 +0100 Subject: [PATCH 15/63] o1vm/mips: introduce scratch_state_inverse These fields will be used to keep track of the elements that should be inverted while generating the proof. --- o1vm/src/interpreters/mips/tests_helpers.rs | 4 ++++ o1vm/src/interpreters/mips/witness.rs | 11 +++++++++++ 2 files changed, 15 insertions(+) diff --git a/o1vm/src/interpreters/mips/tests_helpers.rs b/o1vm/src/interpreters/mips/tests_helpers.rs index 0ad73ab3cc..f07b260e21 100644 --- a/o1vm/src/interpreters/mips/tests_helpers.rs +++ b/o1vm/src/interpreters/mips/tests_helpers.rs @@ -13,6 +13,8 @@ use std::{fs, path::PathBuf}; // FIXME: we should parametrize the tests with different fields. use ark_bn254::Fr as Fp; +use super::witness::SCRATCH_SIZE_INVERSE; + const PAGE_INDEX_EXECUTABLE_MEMORY: u32 = 1; pub(crate) struct OnDiskPreImageOracle; @@ -87,7 +89,9 @@ where registers: Registers::default(), registers_write_index: Registers::default(), scratch_state_idx: 0, + scratch_state_idx_inverse: 0, scratch_state: [Fp::from(0); SCRATCH_SIZE], + scratch_state_inverse: [Fp::from(0); SCRATCH_SIZE_INVERSE], selector: crate::interpreters::mips::column::N_MIPS_SEL_COLS, halt: false, // Keccak related diff --git a/o1vm/src/interpreters/mips/witness.rs b/o1vm/src/interpreters/mips/witness.rs index ca0b98e1ef..c3936b38ce 100644 --- a/o1vm/src/interpreters/mips/witness.rs +++ b/o1vm/src/interpreters/mips/witness.rs @@ -50,10 +50,17 @@ pub const NUM_INSTRUCTION_LOOKUP_TERMS: usize = 5; pub const NUM_LOOKUP_TERMS: usize = NUM_GLOBAL_LOOKUP_TERMS + NUM_DECODING_LOOKUP_TERMS + NUM_INSTRUCTION_LOOKUP_TERMS; // TODO: Delete and use a vector instead +// FIXME: since the introduction of the scratch size inverse, the value below +// can be decreased. It implies to change the offsets defined in [column]. At +// the moment, it incurs an overhead we could avoid as some columns are zeroes. // MIPS + hash_counter + byte_counter + eof + num_bytes_read + chunk + bytes // + length + has_n_bytes + chunk_bytes + preimage pub const SCRATCH_SIZE: usize = 98; +/// Number of columns used by the MIPS interpreter to keep values to be +/// inverted. +pub const SCRATCH_SIZE_INVERSE: usize = 12; + #[derive(Clone, Default)] pub struct SyscallEnv { pub last_hint: Option>, @@ -81,7 +88,9 @@ pub struct Env { pub registers: Registers, pub registers_write_index: Registers, pub scratch_state_idx: usize, + pub scratch_state_idx_inverse: usize, pub scratch_state: [Fp; SCRATCH_SIZE], + pub scratch_state_inverse: [Fp; SCRATCH_SIZE_INVERSE], pub halt: bool, pub syscall_env: SyscallEnv, pub selector: usize, @@ -878,7 +887,9 @@ impl Env { registers: initial_registers.clone(), registers_write_index: Registers::default(), scratch_state_idx: 0, + scratch_state_idx_inverse: 0, scratch_state: fresh_scratch_state(), + scratch_state_inverse: fresh_scratch_state(), halt: state.exited, syscall_env, selector, From ff73fa22bded511d015a8c1d48585b63cad0dc8e Mon Sep 17 00:00:00 2001 From: Danny Willems Date: Thu, 21 Nov 2024 09:05:27 +0100 Subject: [PATCH 16/63] o1vm/MIPS: intro a new column to keep track of values to be inverted --- o1vm/src/interpreters/mips/column.rs | 19 +++++++++++++++---- o1vm/src/interpreters/mips/constraints.rs | 8 ++++++++ o1vm/src/interpreters/mips/interpreter.rs | 2 ++ o1vm/src/interpreters/mips/witness.rs | 7 +++++++ 4 files changed, 32 insertions(+), 4 deletions(-) diff --git a/o1vm/src/interpreters/mips/column.rs b/o1vm/src/interpreters/mips/column.rs index 1b2acfc830..d6e018b0b0 100644 --- a/o1vm/src/interpreters/mips/column.rs +++ b/o1vm/src/interpreters/mips/column.rs @@ -9,7 +9,7 @@ use kimchi_msm::{ use std::ops::{Index, IndexMut}; use strum::EnumCount; -use super::{ITypeInstruction, JTypeInstruction, RTypeInstruction}; +use super::{witness::SCRATCH_SIZE_INVERSE, ITypeInstruction, JTypeInstruction, RTypeInstruction}; /// The number of hashes performed so far in the block pub(crate) const MIPS_HASH_COUNTER_OFF: usize = 80; @@ -50,6 +50,9 @@ pub const N_MIPS_COLS: usize = N_MIPS_REL_COLS + N_MIPS_SEL_COLS; pub enum ColumnAlias { // Can be seen as the abstract indexed variable X_{i} ScratchState(usize), + // A column whose value needs to be inverted in the final witness. + // We're keeping a separate column to perform a batch inversion at the end. + ScratchStateInverse(usize), InstructionCounter, Selector(usize), } @@ -66,8 +69,12 @@ impl From for usize { assert!(i < SCRATCH_SIZE); i } - ColumnAlias::InstructionCounter => SCRATCH_SIZE, - ColumnAlias::Selector(s) => SCRATCH_SIZE + 1 + s, + ColumnAlias::ScratchStateInverse(i) => { + assert!(i < SCRATCH_SIZE_INVERSE); + SCRATCH_SIZE + i + } + ColumnAlias::InstructionCounter => SCRATCH_SIZE + SCRATCH_SIZE_INVERSE, + ColumnAlias::Selector(s) => SCRATCH_SIZE + SCRATCH_SIZE_INVERSE + 1 + s, } } } @@ -138,7 +145,11 @@ impl ColumnIndexer for ColumnAlias { assert!(ss < SCRATCH_SIZE); Column::Relation(ss) } - Self::InstructionCounter => Column::Relation(SCRATCH_SIZE), + Self::ScratchStateInverse(ss) => { + assert!(ss < SCRATCH_SIZE_INVERSE); + Column::Relation(SCRATCH_SIZE + ss) + } + Self::InstructionCounter => Column::Relation(SCRATCH_SIZE + SCRATCH_SIZE_INVERSE), // TODO: what happens with error? It does not have a corresponding alias Self::Selector(s) => { assert!(s < N_MIPS_SEL_COLS); diff --git a/o1vm/src/interpreters/mips/constraints.rs b/o1vm/src/interpreters/mips/constraints.rs index 94369c890b..fa047f199a 100644 --- a/o1vm/src/interpreters/mips/constraints.rs +++ b/o1vm/src/interpreters/mips/constraints.rs @@ -25,6 +25,7 @@ use super::column::N_MIPS_SEL_COLS; /// The environment keeping the constraints between the different polynomials pub struct Env { scratch_state_idx: usize, + scratch_state_idx_inverse: usize, /// A list of constraints, which are multi-variate polynomials over a field, /// represented using the expression framework of `kimchi`. constraints: Vec>, @@ -37,6 +38,7 @@ impl Default for Env { fn default() -> Self { Self { scratch_state_idx: 0, + scratch_state_idx_inverse: 0, constraints: Vec::new(), lookups: Vec::new(), selector: None, @@ -62,6 +64,12 @@ impl InterpreterEnv for Env { MIPSColumn::ScratchState(scratch_idx) } + fn alloc_scratch_inverse(&mut self) -> Self::Position { + let scratch_idx = self.scratch_state_idx_inverse; + self.scratch_state_idx_inverse += 1; + MIPSColumn::ScratchStateInverse(scratch_idx) + } + type Variable = E; fn variable(&self, column: Self::Position) -> Self::Variable { diff --git a/o1vm/src/interpreters/mips/interpreter.rs b/o1vm/src/interpreters/mips/interpreter.rs index 8bf4f61d2e..d10b28eca2 100644 --- a/o1vm/src/interpreters/mips/interpreter.rs +++ b/o1vm/src/interpreters/mips/interpreter.rs @@ -172,6 +172,8 @@ pub trait InterpreterEnv { /// [crate::interpreters::mips::witness::SCRATCH_SIZE] fn alloc_scratch(&mut self) -> Self::Position; + fn alloc_scratch_inverse(&mut self) -> Self::Position; + type Variable: Clone + std::ops::Add + std::ops::Sub diff --git a/o1vm/src/interpreters/mips/witness.rs b/o1vm/src/interpreters/mips/witness.rs index c3936b38ce..1ea7e74a6e 100644 --- a/o1vm/src/interpreters/mips/witness.rs +++ b/o1vm/src/interpreters/mips/witness.rs @@ -115,6 +115,12 @@ impl InterpreterEnv for Env Self::Position { + let scratch_idx = self.scratch_state_idx_inverse; + self.scratch_state_idx_inverse += 1; + Column::ScratchStateInverse(scratch_idx) + } + type Variable = u64; fn variable(&self, _column: Self::Position) -> Self::Variable { @@ -915,6 +921,7 @@ impl Env { pub fn write_field_column(&mut self, column: Column, value: Fp) { match column { Column::ScratchState(idx) => self.scratch_state[idx] = value, + Column::ScratchStateInverse(idx) => self.scratch_state_inverse[idx] = value, Column::InstructionCounter => panic!("Cannot overwrite the column {:?}", column), Column::Selector(s) => self.selector = s, } From 52d5cd9f0248d4e16538840475240cca5365fa42 Mon Sep 17 00:00:00 2001 From: Danny Willems Date: Thu, 21 Nov 2024 09:11:08 +0100 Subject: [PATCH 17/63] o1vm/mips/witness: introduce and call reset_scratch_state_inverse --- o1vm/src/interpreters/mips/tests.rs | 1 + o1vm/src/interpreters/mips/witness.rs | 6 ++++++ 2 files changed, 7 insertions(+) diff --git a/o1vm/src/interpreters/mips/tests.rs b/o1vm/src/interpreters/mips/tests.rs index 3056fae7cd..1b212077d1 100644 --- a/o1vm/src/interpreters/mips/tests.rs +++ b/o1vm/src/interpreters/mips/tests.rs @@ -114,6 +114,7 @@ mod rtype { // that condition would generate an infinite loop instead) while dummy_env.registers.preimage_offset < total_length { dummy_env.reset_scratch_state(); + dummy_env.reset_scratch_state_inverse(); // Set maximum number of bytes to read in this call dummy_env.registers[6] = rng.gen_range(1..=4); diff --git a/o1vm/src/interpreters/mips/witness.rs b/o1vm/src/interpreters/mips/witness.rs index 1ea7e74a6e..6e2b950300 100644 --- a/o1vm/src/interpreters/mips/witness.rs +++ b/o1vm/src/interpreters/mips/witness.rs @@ -914,6 +914,11 @@ impl Env { self.selector = N_MIPS_SEL_COLS; } + pub fn reset_scratch_state_inverse(&mut self) { + self.scratch_state_idx_inverse = 0; + self.scratch_state_inverse = fresh_scratch_state(); + } + pub fn write_column(&mut self, column: Column, value: u64) { self.write_field_column(column, value.into()) } @@ -1156,6 +1161,7 @@ impl Env { start: &Start, ) -> Instruction { self.reset_scratch_state(); + self.reset_scratch_state_inverse(); let (opcode, _instruction) = self.decode_instruction(); self.pp_info(&config.info_at, metadata, start); From f108bf27bb257535971cf7e9446ae52117e10261 Mon Sep 17 00:00:00 2001 From: Danny Willems Date: Thu, 21 Nov 2024 09:11:39 +0100 Subject: [PATCH 18/63] o1vm/mips/constraints: reset scratch state idx inverse --- o1vm/src/interpreters/mips/constraints.rs | 1 + 1 file changed, 1 insertion(+) diff --git a/o1vm/src/interpreters/mips/constraints.rs b/o1vm/src/interpreters/mips/constraints.rs index fa047f199a..7e97317bbd 100644 --- a/o1vm/src/interpreters/mips/constraints.rs +++ b/o1vm/src/interpreters/mips/constraints.rs @@ -631,6 +631,7 @@ impl InterpreterEnv for Env { fn reset(&mut self) { self.scratch_state_idx = 0; + self.scratch_state_idx_inverse = 0; self.constraints.clear(); self.lookups.clear(); self.selector = None; From 8f37429fa304a226dac4863b6dd8e0e1ff7a4b18 Mon Sep 17 00:00:00 2001 From: Danny Willems Date: Thu, 21 Nov 2024 10:43:18 +0100 Subject: [PATCH 19/63] o1vm/mips: introduce scratch_inverse in the proof --- o1vm/src/pickles/proof.rs | 7 ++++++- o1vm/src/pickles/prover.rs | 33 +++++++++++++++++++++++++++++++++ o1vm/src/pickles/tests.rs | 1 + o1vm/src/pickles/verifier.rs | 11 +++++++++++ 4 files changed, 51 insertions(+), 1 deletion(-) diff --git a/o1vm/src/pickles/proof.rs b/o1vm/src/pickles/proof.rs index e3548cdbfe..d98d04113c 100644 --- a/o1vm/src/pickles/proof.rs +++ b/o1vm/src/pickles/proof.rs @@ -1,10 +1,14 @@ use kimchi::{curve::KimchiCurve, proof::PointEvaluations}; use poly_commitment::{ipa::OpeningProof, PolyComm}; -use crate::interpreters::mips::{column::N_MIPS_SEL_COLS, witness::SCRATCH_SIZE}; +use crate::interpreters::mips::{ + column::N_MIPS_SEL_COLS, + witness::{SCRATCH_SIZE, SCRATCH_SIZE_INVERSE}, +}; pub struct WitnessColumns { pub scratch: [G; SCRATCH_SIZE], + pub scratch_inverse: [G; SCRATCH_SIZE_INVERSE], pub instruction_counter: G, pub error: G, pub selector: S, @@ -19,6 +23,7 @@ impl ProofInputs { ProofInputs { evaluations: WitnessColumns { scratch: std::array::from_fn(|_| Vec::with_capacity(domain_size)), + scratch_inverse: std::array::from_fn(|_| Vec::with_capacity(domain_size)), instruction_counter: Vec::with_capacity(domain_size), error: Vec::with_capacity(domain_size), selector: Vec::with_capacity(domain_size), diff --git a/o1vm/src/pickles/prover.rs b/o1vm/src/pickles/prover.rs index 2f40787546..dc0ac2dd08 100644 --- a/o1vm/src/pickles/prover.rs +++ b/o1vm/src/pickles/prover.rs @@ -84,6 +84,7 @@ where > = { let WitnessColumns { scratch, + scratch_inverse, instruction_counter, error, selector, @@ -110,9 +111,17 @@ where }; // Doing in parallel let scratch = scratch.into_par_iter().map(eval_col).collect::>(); + let scratch_inverse = scratch_inverse + .into_par_iter() + .map(|mut evals| { + ark_ff::batch_inversion(&mut evals); + eval_col(evals) + }) + .collect::>(); let selector = selector.into_par_iter().map(eval_col).collect::>(); WitnessColumns { scratch: scratch.try_into().unwrap(), + scratch_inverse: scratch_inverse.try_into().unwrap(), instruction_counter: eval_col(instruction_counter), error: eval_col(error.clone()), selector: selector.try_into().unwrap(), @@ -123,6 +132,7 @@ where let commitments: WitnessColumns, [PolyComm; N_MIPS_SEL_COLS]> = { let WitnessColumns { scratch, + scratch_inverse, instruction_counter, error, selector, @@ -139,9 +149,11 @@ where }; // Doing in parallel let scratch = scratch.par_iter().map(comm).collect::>(); + let scratch_inverse = scratch_inverse.par_iter().map(comm).collect::>(); let selector = selector.par_iter().map(comm).collect::>(); WitnessColumns { scratch: scratch.try_into().unwrap(), + scratch_inverse: scratch_inverse.try_into().unwrap(), instruction_counter: comm(instruction_counter), error: comm(error), selector: selector.try_into().unwrap(), @@ -156,6 +168,7 @@ where let evaluations_d8 = { let WitnessColumns { scratch, + scratch_inverse, instruction_counter, error, selector, @@ -164,9 +177,14 @@ where |poly: &DensePolynomial| poly.evaluate_over_domain_by_ref(domain.d8); // Doing in parallel let scratch = scratch.into_par_iter().map(eval_d8).collect::>(); + let scratch_inverse = scratch_inverse + .into_par_iter() + .map(eval_d8) + .collect::>(); let selector = selector.into_par_iter().map(eval_d8).collect::>(); WitnessColumns { scratch: scratch.try_into().unwrap(), + scratch_inverse: scratch_inverse.try_into().unwrap(), instruction_counter: eval_d8(instruction_counter), error: eval_d8(error), selector: selector.try_into().unwrap(), @@ -178,6 +196,9 @@ where for comm in commitments.scratch.iter() { absorb_commitment(&mut fq_sponge, comm) } + for comm in commitments.scratch_inverse.iter() { + absorb_commitment(&mut fq_sponge, comm) + } absorb_commitment(&mut fq_sponge, &commitments.instruction_counter); absorb_commitment(&mut fq_sponge, &commitments.error); for comm in commitments.selector.iter() { @@ -291,15 +312,18 @@ where let evals = |point| { let WitnessColumns { scratch, + scratch_inverse, instruction_counter, error, selector, } = &polys; let eval = |poly: &DensePolynomial| poly.evaluate(point); let scratch = scratch.par_iter().map(eval).collect::>(); + let scratch_inverse = scratch_inverse.par_iter().map(eval).collect::>(); let selector = selector.par_iter().map(eval).collect::>(); WitnessColumns { scratch: scratch.try_into().unwrap(), + scratch_inverse: scratch_inverse.try_into().unwrap(), instruction_counter: eval(instruction_counter), error: eval(error), selector: selector.try_into().unwrap(), @@ -342,6 +366,14 @@ where fr_sponge.absorb(zeta_eval); fr_sponge.absorb(zeta_omega_eval); } + for (zeta_eval, zeta_omega_eval) in zeta_evaluations + .scratch_inverse + .iter() + .zip(zeta_omega_evaluations.scratch_inverse.iter()) + { + fr_sponge.absorb(zeta_eval); + fr_sponge.absorb(zeta_omega_eval); + } fr_sponge.absorb(&zeta_evaluations.instruction_counter); fr_sponge.absorb(&zeta_omega_evaluations.instruction_counter); fr_sponge.absorb(&zeta_evaluations.error); @@ -367,6 +399,7 @@ where //////////////////////////////////////////////////////////////////////////// let mut polynomials: Vec<_> = polys.scratch.into_iter().collect(); + polynomials.extend(polys.scratch_inverse); polynomials.push(polys.instruction_counter); polynomials.push(polys.error); polynomials.extend(polys.selector); diff --git a/o1vm/src/pickles/tests.rs b/o1vm/src/pickles/tests.rs index f19c610400..474a42c44a 100644 --- a/o1vm/src/pickles/tests.rs +++ b/o1vm/src/pickles/tests.rs @@ -63,6 +63,7 @@ fn test_small_circuit() { let proof_input = ProofInputs:: { evaluations: WitnessColumns { scratch: std::array::from_fn(|_| zero_to_n_minus_one(8)), + scratch_inverse: std::array::from_fn(|_| zero_to_n_minus_one(8)), instruction_counter: zero_to_n_minus_one(8) .into_iter() .map(|x| x + Fq::one()) diff --git a/o1vm/src/pickles/verifier.rs b/o1vm/src/pickles/verifier.rs index 9057a89802..fbbaa912eb 100644 --- a/o1vm/src/pickles/verifier.rs +++ b/o1vm/src/pickles/verifier.rs @@ -96,6 +96,9 @@ where for comm in commitments.scratch.iter() { absorb_commitment(&mut fq_sponge, comm) } + for comm in commitments.scratch_inverse.iter() { + absorb_commitment(&mut fq_sponge, comm) + } absorb_commitment(&mut fq_sponge, &commitments.instruction_counter); absorb_commitment(&mut fq_sponge, &commitments.error); for comm in commitments.selector.iter() { @@ -137,6 +140,14 @@ where fr_sponge.absorb(zeta_eval); fr_sponge.absorb(zeta_omega_eval); } + for (zeta_eval, zeta_omega_eval) in zeta_evaluations + .scratch_inverse + .iter() + .zip(zeta_omega_evaluations.scratch_inverse.iter()) + { + fr_sponge.absorb(zeta_eval); + fr_sponge.absorb(zeta_omega_eval); + } fr_sponge.absorb(&zeta_evaluations.instruction_counter); fr_sponge.absorb(&zeta_omega_evaluations.instruction_counter); fr_sponge.absorb(&zeta_evaluations.error); From acc02530028d717ce96f7be6eb987497774a3dbd Mon Sep 17 00:00:00 2001 From: Danny Willems Date: Thu, 21 Nov 2024 11:01:11 +0100 Subject: [PATCH 20/63] o1vm/mips: use alloc_scratch_inverse for the inverse --- o1vm/src/interpreters/mips/witness.rs | 20 ++++++++++---------- 1 file changed, 10 insertions(+), 10 deletions(-) diff --git a/o1vm/src/interpreters/mips/witness.rs b/o1vm/src/interpreters/mips/witness.rs index 6e2b950300..04bbf6c021 100644 --- a/o1vm/src/interpreters/mips/witness.rs +++ b/o1vm/src/interpreters/mips/witness.rs @@ -333,13 +333,13 @@ impl InterpreterEnv for Env InterpreterEnv for Env Date: Thu, 21 Nov 2024 13:59:43 +0100 Subject: [PATCH 21/63] o1vm/column: increase the total number of columns incl. inverses --- o1vm/src/interpreters/mips/column.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/o1vm/src/interpreters/mips/column.rs b/o1vm/src/interpreters/mips/column.rs index d6e018b0b0..b42b23cafd 100644 --- a/o1vm/src/interpreters/mips/column.rs +++ b/o1vm/src/interpreters/mips/column.rs @@ -35,7 +35,7 @@ pub(crate) const MIPS_CHUNK_BYTES_LEN: usize = 4; pub(crate) const MIPS_PREIMAGE_KEY: usize = 97; /// The number of columns used for relation witness in the MIPS circuit -pub const N_MIPS_REL_COLS: usize = SCRATCH_SIZE + 2; +pub const N_MIPS_REL_COLS: usize = SCRATCH_SIZE + SCRATCH_SIZE_INVERSE + 2; /// The number of witness columns used to store the instruction selectors. pub const N_MIPS_SEL_COLS: usize = From dcf661cc6f752004bf596a011821ea1884d91f0a Mon Sep 17 00:00:00 2001 From: Danny Willems Date: Thu, 21 Nov 2024 14:00:32 +0100 Subject: [PATCH 22/63] o1vm/column: add error message when assert is false --- o1vm/src/interpreters/mips/column.rs | 22 +++++++++++++++++++--- 1 file changed, 19 insertions(+), 3 deletions(-) diff --git a/o1vm/src/interpreters/mips/column.rs b/o1vm/src/interpreters/mips/column.rs index b42b23cafd..ea4f55e9d4 100644 --- a/o1vm/src/interpreters/mips/column.rs +++ b/o1vm/src/interpreters/mips/column.rs @@ -139,20 +139,36 @@ impl IndexMut for MIPSWitness { impl ColumnIndexer for ColumnAlias { const N_COL: usize = N_MIPS_COLS; + fn to_column(self) -> Column { match self { Self::ScratchState(ss) => { - assert!(ss < SCRATCH_SIZE); + assert!( + ss < SCRATCH_SIZE, + "The maximum index is {}, got {}", + SCRATCH_SIZE, + ss + ); Column::Relation(ss) } Self::ScratchStateInverse(ss) => { - assert!(ss < SCRATCH_SIZE_INVERSE); + assert!( + ss < SCRATCH_SIZE_INVERSE, + "The maximum index is {}, got {}", + SCRATCH_SIZE_INVERSE, + ss + ); Column::Relation(SCRATCH_SIZE + ss) } Self::InstructionCounter => Column::Relation(SCRATCH_SIZE + SCRATCH_SIZE_INVERSE), // TODO: what happens with error? It does not have a corresponding alias Self::Selector(s) => { - assert!(s < N_MIPS_SEL_COLS); + assert!( + s < N_MIPS_SEL_COLS, + "The maximum index is {}, got {}", + N_MIPS_SEL_COLS, + s + ); Column::DynamicSelector(s) } } From ac0380be78cd3f6b45b1ec763bcd72153e497044 Mon Sep 17 00:00:00 2001 From: Danny Willems Date: Thu, 21 Nov 2024 14:01:16 +0100 Subject: [PATCH 23/63] o1vm/mips: simplify by removing unused variable --- o1vm/src/interpreters/mips/witness.rs | 15 ++++++--------- 1 file changed, 6 insertions(+), 9 deletions(-) diff --git a/o1vm/src/interpreters/mips/witness.rs b/o1vm/src/interpreters/mips/witness.rs index 04bbf6c021..ee170bbc0f 100644 --- a/o1vm/src/interpreters/mips/witness.rs +++ b/o1vm/src/interpreters/mips/witness.rs @@ -354,15 +354,12 @@ impl InterpreterEnv for Env Date: Thu, 21 Nov 2024 14:02:21 +0100 Subject: [PATCH 24/63] o1vm/pickles: improve error message when panicking when picking col --- o1vm/src/pickles/column_env.rs | 16 ++++++++++++---- 1 file changed, 12 insertions(+), 4 deletions(-) diff --git a/o1vm/src/pickles/column_env.rs b/o1vm/src/pickles/column_env.rs index c66f68160f..d333533a39 100644 --- a/o1vm/src/pickles/column_env.rs +++ b/o1vm/src/pickles/column_env.rs @@ -3,7 +3,10 @@ use ark_poly::{Evaluations, Radix2EvaluationDomain}; use kimchi_msm::columns::Column; use crate::{ - interpreters::mips::{column::N_MIPS_SEL_COLS, witness::SCRATCH_SIZE}, + interpreters::mips::{ + column::N_MIPS_SEL_COLS, + witness::{SCRATCH_SIZE, SCRATCH_SIZE_INVERSE}, + }, pickles::proof::WitnessColumns, }; use kimchi::circuits::{ @@ -60,19 +63,24 @@ impl WitnessColumns { let res = &self.error; Some(res) } else { - panic!("We should not have that many relation columns"); + panic!("We should not have that many relation columns. We have {} columns and index {} was given", SCRATCH_SIZE + SCRATCH_SIZE_INVERSE + 2, i); } } Column::DynamicSelector(i) => { assert!( i < N_MIPS_SEL_COLS, - "We do not have that many dynamic selector columns" + "We do not have that many dynamic selector columns. We have {} columns and index {} was given", + N_MIPS_SEL_COLS, + i ); let res = &self.selector[i]; Some(res) } _ => { - panic!("We should not have any other type of columns") + panic!( + "We should not have any other type of columns. The column {:?} was given", + col + ); } } } From c65b14a6a02c188d237f77dfdc1646f69ae77f24 Mon Sep 17 00:00:00 2001 From: Danny Willems Date: Thu, 21 Nov 2024 14:03:58 +0100 Subject: [PATCH 25/63] o1vm/pickles: incl scratch_size_inverse selection in get_all_columns --- o1vm/src/pickles/column_env.rs | 12 ++++++++---- 1 file changed, 8 insertions(+), 4 deletions(-) diff --git a/o1vm/src/pickles/column_env.rs b/o1vm/src/pickles/column_env.rs index d333533a39..8e8b027b08 100644 --- a/o1vm/src/pickles/column_env.rs +++ b/o1vm/src/pickles/column_env.rs @@ -39,8 +39,9 @@ pub struct ColumnEnvironment<'a, F: FftField> { } pub fn get_all_columns() -> Vec { - let mut cols = Vec::::with_capacity(SCRATCH_SIZE + 2 + N_MIPS_SEL_COLS); - for i in 0..SCRATCH_SIZE + 2 { + let mut cols = + Vec::::with_capacity(SCRATCH_SIZE + SCRATCH_SIZE_INVERSE + 2 + N_MIPS_SEL_COLS); + for i in 0..SCRATCH_SIZE + SCRATCH_SIZE_INVERSE + 2 { cols.push(Column::Relation(i)); } for i in 0..N_MIPS_SEL_COLS { @@ -56,10 +57,13 @@ impl WitnessColumns { if i < SCRATCH_SIZE { let res = &self.scratch[i]; Some(res) - } else if i == SCRATCH_SIZE { + } else if i < SCRATCH_SIZE + SCRATCH_SIZE_INVERSE { + let res = &self.scratch_inverse[i - SCRATCH_SIZE]; + Some(res) + } else if i == SCRATCH_SIZE + SCRATCH_SIZE_INVERSE { let res = &self.instruction_counter; Some(res) - } else if i == SCRATCH_SIZE + 1 { + } else if i == SCRATCH_SIZE + SCRATCH_SIZE_INVERSE + 1 { let res = &self.error; Some(res) } else { From 3071eabb9d181498a708a5a96359136f985b3ac0 Mon Sep 17 00:00:00 2001 From: Danny Willems Date: Thu, 21 Nov 2024 14:34:20 +0100 Subject: [PATCH 26/63] o1vm/pickles: regtest reg. arkworks batch inversion Checking as a regression tests that the batch inversion works with zeroes --- o1vm/src/pickles/tests.rs | 30 +++++++++++++++++++++++++++++- 1 file changed, 29 insertions(+), 1 deletion(-) diff --git a/o1vm/src/pickles/tests.rs b/o1vm/src/pickles/tests.rs index 474a42c44a..0c772d1d91 100644 --- a/o1vm/src/pickles/tests.rs +++ b/o1vm/src/pickles/tests.rs @@ -11,7 +11,7 @@ use crate::{ }, pickles::{verifier::verify, MAXIMUM_DEGREE_CONSTRAINTS, TOTAL_NUMBER_OF_CONSTRAINTS}, }; -use ark_ff::{One, Zero}; +use ark_ff::{Field, One, UniformRand, Zero}; use kimchi::circuits::{domains::EvaluationDomains, expr::Expr, gate::CurrOrNext}; use kimchi_msm::{columns::Column, expr::E}; use log::debug; @@ -101,3 +101,31 @@ fn test_small_circuit() { ); assert!(verif, "Verification fails"); } + +#[test] +fn test_arkworks_batch_inversion_with_only_zeroes() { + let input = vec![Fq::zero(); 8]; + let exp_output = vec![Fq::zero(); 8]; + let mut output = input.clone(); + ark_ff::batch_inversion::(&mut output); + assert_eq!(output, exp_output); +} + +#[test] +fn test_arkworks_batch_inversion_with_zeroes_and_ones() { + let input: Vec = vec![Fq::zero(), Fq::one(), Fq::zero()]; + let exp_output: Vec = vec![Fq::zero(), Fq::one(), Fq::zero()]; + let mut output: Vec = input.clone(); + ark_ff::batch_inversion::(&mut output); + assert_eq!(output, exp_output); +} + +#[test] +fn test_arkworks_batch_inversion_with_zeroes_and_random() { + let mut rng = o1_utils::tests::make_test_rng(None); + let input: Vec = vec![Fq::zero(), Fq::rand(&mut rng), Fq::one()]; + let exp_output: Vec = vec![Fq::zero(), input[1].inverse().unwrap(), Fq::one()]; + let mut output: Vec = input.clone(); + ark_ff::batch_inversion::(&mut output); + assert_eq!(output, exp_output); +} From f4b52a7578725c27d7534f990d15d08260ccf48d Mon Sep 17 00:00:00 2001 From: Danny Willems Date: Thu, 21 Nov 2024 14:49:54 +0100 Subject: [PATCH 27/63] o1vm/pickles: add scratch_state_inverse in the proof inputs --- o1vm/src/pickles/main.rs | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/o1vm/src/pickles/main.rs b/o1vm/src/pickles/main.rs index f60ae5948f..5083d7d58d 100644 --- a/o1vm/src/pickles/main.rs +++ b/o1vm/src/pickles/main.rs @@ -105,6 +105,13 @@ pub fn main() -> ExitCode { { scratch_chunk.push(*scratch); } + for (scratch, scratch_chunk) in mips_wit_env + .scratch_state_inverse + .iter() + .zip(curr_proof_inputs.evaluations.scratch_inverse.iter_mut()) + { + scratch_chunk.push(*scratch); + } curr_proof_inputs .evaluations .instruction_counter From be87dce544b90e512d328c8895a98ee0265686f8 Mon Sep 17 00:00:00 2001 From: Danny Willems Date: Thu, 21 Nov 2024 14:52:24 +0100 Subject: [PATCH 28/63] o1vm/mips: allocate correctly the inverse column --- o1vm/src/interpreters/mips/constraints.rs | 2 +- o1vm/src/interpreters/mips/witness.rs | 13 ++++++------- 2 files changed, 7 insertions(+), 8 deletions(-) diff --git a/o1vm/src/interpreters/mips/constraints.rs b/o1vm/src/interpreters/mips/constraints.rs index 7e97317bbd..cb46508b9b 100644 --- a/o1vm/src/interpreters/mips/constraints.rs +++ b/o1vm/src/interpreters/mips/constraints.rs @@ -227,7 +227,7 @@ impl InterpreterEnv for Env { unsafe { self.test_zero(x, pos) } }; let x_inv_or_zero = { - let pos = self.alloc_scratch(); + let pos = self.alloc_scratch_inverse(); self.variable(pos) }; // If x = 0, then res = 1 and x_inv_or_zero = 0 diff --git a/o1vm/src/interpreters/mips/witness.rs b/o1vm/src/interpreters/mips/witness.rs index ee170bbc0f..38eba183bb 100644 --- a/o1vm/src/interpreters/mips/witness.rs +++ b/o1vm/src/interpreters/mips/witness.rs @@ -329,15 +329,15 @@ impl InterpreterEnv for Env Self::Variable { // write the result - let pos = self.alloc_scratch(); - let res = if *x == 0 { 1 } else { 0 }; - self.write_column(pos, res); + let res = { + let pos = self.alloc_scratch(); + unsafe { self.test_zero(x, pos) } + }; // write the non deterministic advice inv_or_zero + let pos = self.alloc_scratch_inverse(); if *x == 0 { - let pos = self.alloc_scratch(); self.write_field_column(pos, Fp::zero()); } else { - let pos = self.alloc_scratch_inverse(); self.write_field_column(pos, Fp::from(*x)); }; // return the result @@ -354,11 +354,10 @@ impl InterpreterEnv for Env Date: Thu, 21 Nov 2024 17:24:11 +0100 Subject: [PATCH 29/63] o1vm/mips: fix tests related to the new inverse scratch state --- o1vm/src/interpreters/mips/column.rs | 4 +++- o1vm/src/pickles/tests.rs | 9 ++++++--- 2 files changed, 9 insertions(+), 4 deletions(-) diff --git a/o1vm/src/interpreters/mips/column.rs b/o1vm/src/interpreters/mips/column.rs index ea4f55e9d4..88cd6cc68a 100644 --- a/o1vm/src/interpreters/mips/column.rs +++ b/o1vm/src/interpreters/mips/column.rs @@ -9,7 +9,9 @@ use kimchi_msm::{ use std::ops::{Index, IndexMut}; use strum::EnumCount; -use super::{witness::SCRATCH_SIZE_INVERSE, ITypeInstruction, JTypeInstruction, RTypeInstruction}; +pub use super::{ + witness::SCRATCH_SIZE_INVERSE, ITypeInstruction, JTypeInstruction, RTypeInstruction, +}; /// The number of hashes performed so far in the block pub(crate) const MIPS_HASH_COUNTER_OFF: usize = 80; diff --git a/o1vm/src/pickles/tests.rs b/o1vm/src/pickles/tests.rs index 0c772d1d91..e5c80f8f4b 100644 --- a/o1vm/src/pickles/tests.rs +++ b/o1vm/src/pickles/tests.rs @@ -7,7 +7,10 @@ use super::{ }; use crate::{ interpreters::mips::{ - constraints as mips_constraints, interpreter, interpreter::InterpreterEnv, Instruction, + column::SCRATCH_SIZE_INVERSE, + constraints as mips_constraints, + interpreter::{self, InterpreterEnv}, + Instruction, }, pickles::{verifier::verify, MAXIMUM_DEGREE_CONSTRAINTS, TOTAL_NUMBER_OF_CONSTRAINTS}, }; @@ -63,7 +66,7 @@ fn test_small_circuit() { let proof_input = ProofInputs:: { evaluations: WitnessColumns { scratch: std::array::from_fn(|_| zero_to_n_minus_one(8)), - scratch_inverse: std::array::from_fn(|_| zero_to_n_minus_one(8)), + scratch_inverse: std::array::from_fn(|_| (0..8).map(|_| Fq::zero()).collect()), instruction_counter: zero_to_n_minus_one(8) .into_iter() .map(|x| x + Fq::one()) @@ -75,7 +78,7 @@ fn test_small_circuit() { }, }; let mut expr = Expr::zero(); - for i in 0..SCRATCH_SIZE + 2 { + for i in 0..SCRATCH_SIZE + SCRATCH_SIZE_INVERSE + 2 { expr += Expr::cell(Column::Relation(i), CurrOrNext::Curr); } let mut rng = make_test_rng(None); From bc42b0286d2dd5dede90d822d0774181359f40fc Mon Sep 17 00:00:00 2001 From: Danny Willems Date: Thu, 21 Nov 2024 15:42:21 +0100 Subject: [PATCH 30/63] o1vm/mips: rewrite offsets reg. column index in scratch state In addition to that, moving the values SCRATCH_SIZE and SCRATCH_SIZE_INVERSE into column.rs --- o1vm/src/interpreters/mips/column.rs | 36 ++++++++++++--------- o1vm/src/interpreters/mips/constraints.rs | 4 +-- o1vm/src/interpreters/mips/interpreter.rs | 4 +-- o1vm/src/interpreters/mips/tests_helpers.rs | 4 +-- o1vm/src/interpreters/mips/witness.rs | 12 +------ o1vm/src/legacy/main.rs | 4 +-- o1vm/src/legacy/tests.rs | 3 +- o1vm/src/pickles/column_env.rs | 5 +-- o1vm/src/pickles/proof.rs | 5 +-- o1vm/src/pickles/tests.rs | 2 +- 10 files changed, 33 insertions(+), 46 deletions(-) diff --git a/o1vm/src/interpreters/mips/column.rs b/o1vm/src/interpreters/mips/column.rs index 88cd6cc68a..9a8060bb9d 100644 --- a/o1vm/src/interpreters/mips/column.rs +++ b/o1vm/src/interpreters/mips/column.rs @@ -1,7 +1,4 @@ -use crate::interpreters::mips::{ - witness::SCRATCH_SIZE, - Instruction::{self, IType, JType, RType}, -}; +use crate::interpreters::mips::Instruction::{self, IType, JType, RType}; use kimchi_msm::{ columns::{Column, ColumnIndexer}, witness::Witness, @@ -9,32 +6,39 @@ use kimchi_msm::{ use std::ops::{Index, IndexMut}; use strum::EnumCount; -pub use super::{ - witness::SCRATCH_SIZE_INVERSE, ITypeInstruction, JTypeInstruction, RTypeInstruction, -}; +use super::{ITypeInstruction, JTypeInstruction, RTypeInstruction}; +pub(crate) const SCRATCH_SIZE_WITHOUT_KECCAK: usize = 80; /// The number of hashes performed so far in the block -pub(crate) const MIPS_HASH_COUNTER_OFF: usize = 80; +pub(crate) const MIPS_HASH_COUNTER_OFF: usize = SCRATCH_SIZE_WITHOUT_KECCAK; /// The number of bytes of the preimage that have been read so far in this hash -pub(crate) const MIPS_BYTE_COUNTER_OFF: usize = 81; +pub(crate) const MIPS_BYTE_COUNTER_OFF: usize = SCRATCH_SIZE_WITHOUT_KECCAK + 1; /// A flag indicating whether the preimage has been read fully or not -pub(crate) const MIPS_END_OF_PREIMAGE_OFF: usize = 82; +pub(crate) const MIPS_END_OF_PREIMAGE_OFF: usize = SCRATCH_SIZE_WITHOUT_KECCAK + 2; /// The number of preimage bytes processed in this step -pub(crate) const MIPS_NUM_BYTES_READ_OFF: usize = 83; +pub(crate) const MIPS_NUM_BYTES_READ_OFF: usize = SCRATCH_SIZE_WITHOUT_KECCAK + 3; /// The at most 4-byte chunk of the preimage that has been read in this step. /// Contains a field element of at most 4 bytes. -pub(crate) const MIPS_PREIMAGE_CHUNK_OFF: usize = 84; +pub(crate) const MIPS_PREIMAGE_CHUNK_OFF: usize = SCRATCH_SIZE_WITHOUT_KECCAK + 4; /// The at most 4-bytes of the preimage that are currently being processed /// Consists of 4 field elements of at most 1 byte each. -pub(crate) const MIPS_PREIMAGE_BYTES_OFF: usize = 85; +pub(crate) const MIPS_PREIMAGE_BYTES_OFF: usize = SCRATCH_SIZE_WITHOUT_KECCAK + 5; /// The at most 4-bytes of the length that are currently being processed -pub(crate) const MIPS_LENGTH_BYTES_OFF: usize = 89; +pub(crate) const MIPS_LENGTH_BYTES_OFF: usize = SCRATCH_SIZE_WITHOUT_KECCAK + 5 + 4; /// Flags indicating whether at least N bytes have been processed in this step -pub(crate) const MIPS_HAS_N_BYTES_OFF: usize = 93; +pub(crate) const MIPS_HAS_N_BYTES_OFF: usize = SCRATCH_SIZE_WITHOUT_KECCAK + 5 + 4 + 4; /// The maximum size of a chunk (4 bytes) pub(crate) const MIPS_CHUNK_BYTES_LEN: usize = 4; /// The location of the preimage key as a field element of 248bits -pub(crate) const MIPS_PREIMAGE_KEY: usize = 97; +pub(crate) const MIPS_PREIMAGE_KEY: usize = SCRATCH_SIZE_WITHOUT_KECCAK + 5 + 4 + 4 + 4; + +// MIPS + hash_counter + byte_counter + eof + num_bytes_read + chunk + bytes +// + length + has_n_bytes + chunk_bytes + preimage +pub const SCRATCH_SIZE: usize = SCRATCH_SIZE_WITHOUT_KECCAK + 5 + 4 + 4 + 4 + 1; + +/// Number of columns used by the MIPS interpreter to keep values to be +/// inverted. +pub const SCRATCH_SIZE_INVERSE: usize = 12; /// The number of columns used for relation witness in the MIPS circuit pub const N_MIPS_REL_COLS: usize = SCRATCH_SIZE + SCRATCH_SIZE_INVERSE + 2; diff --git a/o1vm/src/interpreters/mips/constraints.rs b/o1vm/src/interpreters/mips/constraints.rs index cb46508b9b..279cb0a6c1 100644 --- a/o1vm/src/interpreters/mips/constraints.rs +++ b/o1vm/src/interpreters/mips/constraints.rs @@ -54,10 +54,10 @@ impl InterpreterEnv for Env { // Use one of the available columns. It won't create a new column every time // this function is called. The number of columns is defined upfront by - // crate::mips::witness::SCRATCH_SIZE. + // crate::interpreters::mips::column::SCRATCH_SIZE. fn alloc_scratch(&mut self) -> Self::Position { // All columns are implemented using a simple index, and a name is given - // to the index. See crate::SCRATCH_SIZE for the maximum number of + // to the index. See crate::interpreters::mips::column::SCRATCH_SIZE for the maximum number of // columns the circuit can use. let scratch_idx = self.scratch_state_idx; self.scratch_state_idx += 1; diff --git a/o1vm/src/interpreters/mips/interpreter.rs b/o1vm/src/interpreters/mips/interpreter.rs index d10b28eca2..0ea55c67ea 100644 --- a/o1vm/src/interpreters/mips/interpreter.rs +++ b/o1vm/src/interpreters/mips/interpreter.rs @@ -166,10 +166,10 @@ pub trait InterpreterEnv { /// The variables are "freed" after each step/instruction. /// The variable allocation can be seen as an allocation on a stack that is /// popped after each step execution. - /// At the moment, [crate::interpreters::mips::witness::SCRATCH_SIZE - 46] + /// At the moment, [crate::interpreters::mips::column::SCRATCH_SIZE - 46] /// elements can be allocated. If more temporary variables are required for /// an instruction, increase the value - /// [crate::interpreters::mips::witness::SCRATCH_SIZE] + /// [crate::interpreters::mips::column::SCRATCH_SIZE] fn alloc_scratch(&mut self) -> Self::Position; fn alloc_scratch_inverse(&mut self) -> Self::Position; diff --git a/o1vm/src/interpreters/mips/tests_helpers.rs b/o1vm/src/interpreters/mips/tests_helpers.rs index f07b260e21..1682196588 100644 --- a/o1vm/src/interpreters/mips/tests_helpers.rs +++ b/o1vm/src/interpreters/mips/tests_helpers.rs @@ -3,7 +3,7 @@ use crate::{ interpreters::mips::{ interpreter::{debugging::InstructionParts, InterpreterEnv}, registers::Registers, - witness::{Env as WEnv, SyscallEnv, SCRATCH_SIZE}, + witness::{Env as WEnv, SyscallEnv}, }, preimage_oracle::PreImageOracleT, }; @@ -13,7 +13,7 @@ use std::{fs, path::PathBuf}; // FIXME: we should parametrize the tests with different fields. use ark_bn254::Fr as Fp; -use super::witness::SCRATCH_SIZE_INVERSE; +use super::column::{SCRATCH_SIZE, SCRATCH_SIZE_INVERSE}; const PAGE_INDEX_EXECUTABLE_MEMORY: u32 = 1; diff --git a/o1vm/src/interpreters/mips/witness.rs b/o1vm/src/interpreters/mips/witness.rs index 38eba183bb..991b946c8d 100644 --- a/o1vm/src/interpreters/mips/witness.rs +++ b/o1vm/src/interpreters/mips/witness.rs @@ -1,4 +1,4 @@ -use super::column::N_MIPS_SEL_COLS; +use super::column::{N_MIPS_SEL_COLS, SCRATCH_SIZE, SCRATCH_SIZE_INVERSE}; use crate::{ cannon::{ Hint, Meta, Page, Start, State, StepFrequency, VmConfiguration, PAGE_ADDRESS_MASK, @@ -50,16 +50,6 @@ pub const NUM_INSTRUCTION_LOOKUP_TERMS: usize = 5; pub const NUM_LOOKUP_TERMS: usize = NUM_GLOBAL_LOOKUP_TERMS + NUM_DECODING_LOOKUP_TERMS + NUM_INSTRUCTION_LOOKUP_TERMS; // TODO: Delete and use a vector instead -// FIXME: since the introduction of the scratch size inverse, the value below -// can be decreased. It implies to change the offsets defined in [column]. At -// the moment, it incurs an overhead we could avoid as some columns are zeroes. -// MIPS + hash_counter + byte_counter + eof + num_bytes_read + chunk + bytes -// + length + has_n_bytes + chunk_bytes + preimage -pub const SCRATCH_SIZE: usize = 98; - -/// Number of columns used by the MIPS interpreter to keep values to be -/// inverted. -pub const SCRATCH_SIZE_INVERSE: usize = 12; #[derive(Clone, Default)] pub struct SyscallEnv { diff --git a/o1vm/src/legacy/main.rs b/o1vm/src/legacy/main.rs index 767f1e0e41..749f5722b6 100644 --- a/o1vm/src/legacy/main.rs +++ b/o1vm/src/legacy/main.rs @@ -12,10 +12,10 @@ use o1vm::{ environment::KeccakEnv, }, mips::{ - column::{N_MIPS_COLS, N_MIPS_REL_COLS, N_MIPS_SEL_COLS}, + column::{N_MIPS_COLS, N_MIPS_REL_COLS, N_MIPS_SEL_COLS, SCRATCH_SIZE}, constraints as mips_constraints, interpreter::Instruction, - witness::{self as mips_witness, SCRATCH_SIZE}, + witness::{self as mips_witness}, }, }, legacy::{ diff --git a/o1vm/src/legacy/tests.rs b/o1vm/src/legacy/tests.rs index 30dc417929..bce2990d86 100644 --- a/o1vm/src/legacy/tests.rs +++ b/o1vm/src/legacy/tests.rs @@ -1,9 +1,8 @@ use crate::{ interpreters::mips::{ - column::N_MIPS_REL_COLS, + column::{N_MIPS_REL_COLS, SCRATCH_SIZE}, constraints::Env as CEnv, interpreter::{debugging::InstructionParts, interpret_itype}, - witness::SCRATCH_SIZE, ITypeInstruction, }, legacy::{ diff --git a/o1vm/src/pickles/column_env.rs b/o1vm/src/pickles/column_env.rs index 8e8b027b08..61f72d05e1 100644 --- a/o1vm/src/pickles/column_env.rs +++ b/o1vm/src/pickles/column_env.rs @@ -3,10 +3,7 @@ use ark_poly::{Evaluations, Radix2EvaluationDomain}; use kimchi_msm::columns::Column; use crate::{ - interpreters::mips::{ - column::N_MIPS_SEL_COLS, - witness::{SCRATCH_SIZE, SCRATCH_SIZE_INVERSE}, - }, + interpreters::mips::column::{N_MIPS_SEL_COLS, SCRATCH_SIZE, SCRATCH_SIZE_INVERSE}, pickles::proof::WitnessColumns, }; use kimchi::circuits::{ diff --git a/o1vm/src/pickles/proof.rs b/o1vm/src/pickles/proof.rs index d98d04113c..40529a3409 100644 --- a/o1vm/src/pickles/proof.rs +++ b/o1vm/src/pickles/proof.rs @@ -1,10 +1,7 @@ use kimchi::{curve::KimchiCurve, proof::PointEvaluations}; use poly_commitment::{ipa::OpeningProof, PolyComm}; -use crate::interpreters::mips::{ - column::N_MIPS_SEL_COLS, - witness::{SCRATCH_SIZE, SCRATCH_SIZE_INVERSE}, -}; +use crate::interpreters::mips::column::{N_MIPS_SEL_COLS, SCRATCH_SIZE, SCRATCH_SIZE_INVERSE}; pub struct WitnessColumns { pub scratch: [G; SCRATCH_SIZE], diff --git a/o1vm/src/pickles/tests.rs b/o1vm/src/pickles/tests.rs index e5c80f8f4b..b4bb102dc7 100644 --- a/o1vm/src/pickles/tests.rs +++ b/o1vm/src/pickles/tests.rs @@ -1,7 +1,7 @@ use std::time::Instant; use super::{ - super::interpreters::mips::witness::SCRATCH_SIZE, + super::interpreters::mips::column::SCRATCH_SIZE, proof::{ProofInputs, WitnessColumns}, prover::prove, }; From 796267d3fc0e2f86d21a3aa1b0bf058234651aed Mon Sep 17 00:00:00 2001 From: Danny Willems Date: Thu, 21 Nov 2024 17:11:31 +0100 Subject: [PATCH 31/63] o1vm/mips: decreasing actual scratch state size by 40% It seems that most of the state was empty. --- o1vm/src/interpreters/mips/column.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/o1vm/src/interpreters/mips/column.rs b/o1vm/src/interpreters/mips/column.rs index 9a8060bb9d..cd895198b7 100644 --- a/o1vm/src/interpreters/mips/column.rs +++ b/o1vm/src/interpreters/mips/column.rs @@ -8,7 +8,7 @@ use strum::EnumCount; use super::{ITypeInstruction, JTypeInstruction, RTypeInstruction}; -pub(crate) const SCRATCH_SIZE_WITHOUT_KECCAK: usize = 80; +pub(crate) const SCRATCH_SIZE_WITHOUT_KECCAK: usize = 45; /// The number of hashes performed so far in the block pub(crate) const MIPS_HASH_COUNTER_OFF: usize = SCRATCH_SIZE_WITHOUT_KECCAK; /// The number of bytes of the preimage that have been read so far in this hash From ebcd6bb5bfd09720c9a6c28ddae34ea4f593d45b Mon Sep 17 00:00:00 2001 From: Danny Willems Date: Wed, 20 Nov 2024 16:22:33 +0100 Subject: [PATCH 32/63] o1vm/riscv32: implement mul_lo_signed --- o1vm/src/interpreters/riscv32im/constraints.rs | 9 +++++++++ o1vm/src/interpreters/riscv32im/interpreter.rs | 14 ++++++++++++++ o1vm/src/interpreters/riscv32im/witness.rs | 15 +++++++++++++++ 3 files changed, 38 insertions(+) diff --git a/o1vm/src/interpreters/riscv32im/constraints.rs b/o1vm/src/interpreters/riscv32im/constraints.rs index 11dee8a230..82b9cd5105 100644 --- a/o1vm/src/interpreters/riscv32im/constraints.rs +++ b/o1vm/src/interpreters/riscv32im/constraints.rs @@ -336,6 +336,15 @@ impl InterpreterEnv for Env { self.variable(position) } + unsafe fn mul_lo_signed( + &mut self, + _x: &Self::Variable, + _y: &Self::Variable, + position: Self::Position, + ) -> Self::Variable { + self.variable(position) + } + unsafe fn mul_hi_lo( &mut self, _x: &Self::Variable, diff --git a/o1vm/src/interpreters/riscv32im/interpreter.rs b/o1vm/src/interpreters/riscv32im/interpreter.rs index 1e41918b20..2cd83827a1 100644 --- a/o1vm/src/interpreters/riscv32im/interpreter.rs +++ b/o1vm/src/interpreters/riscv32im/interpreter.rs @@ -1215,6 +1215,20 @@ pub trait InterpreterEnv { position: Self::Position, ) -> Self::Variable; + /// Returns `(x * y) & ((1 << 32) - 1))`, storing the results in `position` + /// + /// # Safety + /// + /// There are no constraints on the returned values; callers must manually add constraints to + /// ensure that the pair of returned values correspond to the given values `x` and `y`, and + /// that they fall within the desired range. + unsafe fn mul_lo_signed( + &mut self, + x: &Self::Variable, + y: &Self::Variable, + position: Self::Position, + ) -> Self::Variable; + /// Returns `((x * y) >> 32, (x * y) & ((1 << 32) - 1))`, storing the results in `position_hi` /// and `position_lo` respectively. /// diff --git a/o1vm/src/interpreters/riscv32im/witness.rs b/o1vm/src/interpreters/riscv32im/witness.rs index 0418852ae9..658048bf99 100644 --- a/o1vm/src/interpreters/riscv32im/witness.rs +++ b/o1vm/src/interpreters/riscv32im/witness.rs @@ -456,6 +456,21 @@ impl InterpreterEnv for Env { res } + unsafe fn mul_lo_signed( + &mut self, + x: &Self::Variable, + y: &Self::Variable, + position: Self::Position, + ) -> Self::Variable { + let x: u32 = (*x).try_into().unwrap(); + let y: u32 = (*y).try_into().unwrap(); + let res = (((x as i32) as i64) * ((y as i32) as i64)) as u64; + let res = (res & ((1 << 32) - 1)) as u32; + let res = res as u64; + self.write_column(position, res); + res + } + unsafe fn mul_hi_lo_signed( &mut self, x: &Self::Variable, From 95098af4c18c79cc880f1e2da0dd76399b470423 Mon Sep 17 00:00:00 2001 From: Danny Willems Date: Mon, 25 Nov 2024 10:46:42 +0100 Subject: [PATCH 33/63] o1vm/riscv32im: simplify mul_lo_signed implementation --- o1vm/src/interpreters/riscv32im/witness.rs | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/o1vm/src/interpreters/riscv32im/witness.rs b/o1vm/src/interpreters/riscv32im/witness.rs index 658048bf99..3484ad0a10 100644 --- a/o1vm/src/interpreters/riscv32im/witness.rs +++ b/o1vm/src/interpreters/riscv32im/witness.rs @@ -462,9 +462,9 @@ impl InterpreterEnv for Env { y: &Self::Variable, position: Self::Position, ) -> Self::Variable { - let x: u32 = (*x).try_into().unwrap(); - let y: u32 = (*y).try_into().unwrap(); - let res = (((x as i32) as i64) * ((y as i32) as i64)) as u64; + let x: i32 = (*x).try_into().unwrap(); + let y: i32 = (*y).try_into().unwrap(); + let res = ((x as i64) * (y as i64)) as u64; let res = (res & ((1 << 32) - 1)) as u32; let res = res as u64; self.write_column(position, res); From b86aa1f422c8add255e5ee96a8cd9bd55a836474 Mon Sep 17 00:00:00 2001 From: svv232 Date: Mon, 25 Nov 2024 09:36:10 -0500 Subject: [PATCH 34/63] implementation for load half instruction for riscvi32 --- .../src/interpreters/riscv32im/interpreter.rs | 20 ++++++++++++++++++- 1 file changed, 19 insertions(+), 1 deletion(-) diff --git a/o1vm/src/interpreters/riscv32im/interpreter.rs b/o1vm/src/interpreters/riscv32im/interpreter.rs index 1e41918b20..f71d522789 100644 --- a/o1vm/src/interpreters/riscv32im/interpreter.rs +++ b/o1vm/src/interpreters/riscv32im/interpreter.rs @@ -1652,7 +1652,25 @@ pub fn interpret_itype(env: &mut Env, instr: IInstruction) unimplemented!("LoadByte") } IInstruction::LoadHalf => { - unimplemented!("LoadHalf") + // lh: x[rd] = sext(M[x[rs1] + sext(offset)][15:0]) + let local_rs1 = env.read_register(&rs1); + let local_imm = env.sign_extend(&imm, 12); + let address = { + let address_scratch = env.alloc_scratch(); + let overflow_scratch = env.alloc_scratch(); + let (address, _overflow) = unsafe { + env.add_witness(&local_rs1, &local_imm, address_scratch, overflow_scratch) + }; + address + }; + // Add a range check here for address + let v0 = env.read_memory(&address); + let v1 = env.read_memory(&(address.clone() + Env::constant(1))); + let value = (v0 * Env::constant(1 << 8)) + v1; + let value = env.sign_extend(&value, 16); + env.write_register(&rd, value); + env.set_instruction_pointer(next_instruction_pointer.clone()); + env.set_next_instruction_pointer(next_instruction_pointer + Env::constant(4u32)); } IInstruction::LoadWord => { // lw: x[rd] = sext(M[x[rs1] + sext(offset)][31:0]) From 22459284276ce76f5dfc1acb24b861a3958c2056 Mon Sep 17 00:00:00 2001 From: svv232 Date: Mon, 25 Nov 2024 09:38:35 -0500 Subject: [PATCH 35/63] implementation for load byte in riscv32im --- o1vm/src/interpreters/riscv32im/interpreter.rs | 18 +++++++++++++++++- 1 file changed, 17 insertions(+), 1 deletion(-) diff --git a/o1vm/src/interpreters/riscv32im/interpreter.rs b/o1vm/src/interpreters/riscv32im/interpreter.rs index f71d522789..1639dc8985 100644 --- a/o1vm/src/interpreters/riscv32im/interpreter.rs +++ b/o1vm/src/interpreters/riscv32im/interpreter.rs @@ -1649,7 +1649,23 @@ pub fn interpret_itype(env: &mut Env, instr: IInstruction) match instr { IInstruction::LoadByte => { - unimplemented!("LoadByte") + // lb: x[rd] = sext(M[x[rs1] + sext(offset)][7:0]) + let local_rs1 = env.read_register(&rs1); + let local_imm = env.sign_extend(&imm, 12); + let address = { + let address_scratch = env.alloc_scratch(); + let overflow_scratch = env.alloc_scratch(); + let (address, _overflow) = unsafe { + env.add_witness(&local_rs1, &local_imm, address_scratch, overflow_scratch) + }; + address + }; + // Add a range check here for address + let value = env.read_memory(&address); + let value = env.sign_extend(&value, 8); + env.write_register(&rd, value); + env.set_instruction_pointer(next_instruction_pointer.clone()); + env.set_next_instruction_pointer(next_instruction_pointer + Env::constant(4u32)); } IInstruction::LoadHalf => { // lh: x[rd] = sext(M[x[rs1] + sext(offset)][15:0]) From b89ce1cf4519a8cafd2f5561ab573a116553a2f1 Mon Sep 17 00:00:00 2001 From: svv232 Date: Mon, 25 Nov 2024 09:43:20 -0500 Subject: [PATCH 36/63] implementation for load byte unsigned riscv32im --- o1vm/src/interpreters/riscv32im/interpreter.rs | 17 ++++++++++++++++- 1 file changed, 16 insertions(+), 1 deletion(-) diff --git a/o1vm/src/interpreters/riscv32im/interpreter.rs b/o1vm/src/interpreters/riscv32im/interpreter.rs index 1639dc8985..64e27edfa3 100644 --- a/o1vm/src/interpreters/riscv32im/interpreter.rs +++ b/o1vm/src/interpreters/riscv32im/interpreter.rs @@ -1714,7 +1714,22 @@ pub fn interpret_itype(env: &mut Env, instr: IInstruction) env.set_next_instruction_pointer(next_instruction_pointer + Env::constant(4u32)); } IInstruction::LoadByteUnsigned => { - unimplemented!("LoadByteUnsigned") + //lbu: x[rd] = M[x[rs1] + sext(offset)][7:0] + let local_rs1 = env.read_register(&rs1); + let local_imm = env.sign_extend(&imm, 12); + let address = { + let address_scratch = env.alloc_scratch(); + let overflow_scratch = env.alloc_scratch(); + let (address, _overflow) = unsafe { + env.add_witness(&local_rs1, &local_imm, address_scratch, overflow_scratch) + }; + address + }; + // lhu: Add a range check here for address + let value = env.read_memory(&address); + env.write_register(&rd, value); + env.set_instruction_pointer(next_instruction_pointer.clone()); + env.set_next_instruction_pointer(next_instruction_pointer + Env::constant(4u32)); } IInstruction::LoadHalfUnsigned => { unimplemented!("LoadHalfUnsigned") From 83e423ad15ffc45ba4c731dae8c199d4f5ba74f1 Mon Sep 17 00:00:00 2001 From: svv232 Date: Mon, 25 Nov 2024 09:48:55 -0500 Subject: [PATCH 37/63] implementation for load half unsigned riscv32im --- .../src/interpreters/riscv32im/interpreter.rs | 19 ++++++++++++++++++- 1 file changed, 18 insertions(+), 1 deletion(-) diff --git a/o1vm/src/interpreters/riscv32im/interpreter.rs b/o1vm/src/interpreters/riscv32im/interpreter.rs index 64e27edfa3..5fe7535c60 100644 --- a/o1vm/src/interpreters/riscv32im/interpreter.rs +++ b/o1vm/src/interpreters/riscv32im/interpreter.rs @@ -1732,7 +1732,24 @@ pub fn interpret_itype(env: &mut Env, instr: IInstruction) env.set_next_instruction_pointer(next_instruction_pointer + Env::constant(4u32)); } IInstruction::LoadHalfUnsigned => { - unimplemented!("LoadHalfUnsigned") + // lhu: x[rd] = M[x[rs1] + sext(offset)][15:0] + let local_rs1 = env.read_register(&rs1); + let local_imm = env.sign_extend(&imm, 12); + let address = { + let address_scratch = env.alloc_scratch(); + let overflow_scratch = env.alloc_scratch(); + let (address, _overflow) = unsafe { + env.add_witness(&local_rs1, &local_imm, address_scratch, overflow_scratch) + }; + address + }; + // Add a range check here for address + let v0 = env.read_memory(&address); + let v1 = env.read_memory(&(address.clone() + Env::constant(1))); + let value = (v0 * Env::constant(1 << 8)) + v1; + env.write_register(&rd, value); + env.set_instruction_pointer(next_instruction_pointer.clone()); + env.set_next_instruction_pointer(next_instruction_pointer + Env::constant(4u32)); } IInstruction::ShiftLeftLogicalImmediate => { unimplemented!("ShiftLeftLogicalImmediate") From ba54734692ad33ecb7a4627efe0fd53b7f372896 Mon Sep 17 00:00:00 2001 From: Danny Willems Date: Wed, 20 Nov 2024 16:23:37 +0100 Subject: [PATCH 38/63] o1vm/riscv32: implement mul_hi --- o1vm/src/interpreters/riscv32im/constraints.rs | 9 +++++++++ o1vm/src/interpreters/riscv32im/interpreter.rs | 14 ++++++++++++++ o1vm/src/interpreters/riscv32im/witness.rs | 15 +++++++++++++++ 3 files changed, 38 insertions(+) diff --git a/o1vm/src/interpreters/riscv32im/constraints.rs b/o1vm/src/interpreters/riscv32im/constraints.rs index 82b9cd5105..ef1496ae80 100644 --- a/o1vm/src/interpreters/riscv32im/constraints.rs +++ b/o1vm/src/interpreters/riscv32im/constraints.rs @@ -345,6 +345,15 @@ impl InterpreterEnv for Env { self.variable(position) } + unsafe fn mul_hi( + &mut self, + _x: &Self::Variable, + _y: &Self::Variable, + position: Self::Position, + ) -> Self::Variable { + self.variable(position) + } + unsafe fn mul_hi_lo( &mut self, _x: &Self::Variable, diff --git a/o1vm/src/interpreters/riscv32im/interpreter.rs b/o1vm/src/interpreters/riscv32im/interpreter.rs index 2cd83827a1..905efe547f 100644 --- a/o1vm/src/interpreters/riscv32im/interpreter.rs +++ b/o1vm/src/interpreters/riscv32im/interpreter.rs @@ -1245,6 +1245,20 @@ pub trait InterpreterEnv { position_lo: Self::Position, ) -> (Self::Variable, Self::Variable); + /// Returns `((x * y) >> 32`, storing the results in `position`. + /// + /// # Safety + /// + /// There are no constraints on the returned values; callers must manually add constraints to + /// ensure that the pair of returned values correspond to the given values `x` and `y`, and + /// that they fall within the desired range. + unsafe fn mul_hi( + &mut self, + x: &Self::Variable, + y: &Self::Variable, + position: Self::Position, + ) -> Self::Variable; + /// Returns `((x * y) >> 32, (x * y) & ((1 << 32) - 1))`, storing the results in `position_hi` /// and `position_lo` respectively. /// diff --git a/o1vm/src/interpreters/riscv32im/witness.rs b/o1vm/src/interpreters/riscv32im/witness.rs index 3484ad0a10..fa919adb16 100644 --- a/o1vm/src/interpreters/riscv32im/witness.rs +++ b/o1vm/src/interpreters/riscv32im/witness.rs @@ -490,6 +490,21 @@ impl InterpreterEnv for Env { (hi, lo) } + unsafe fn mul_hi( + &mut self, + x: &Self::Variable, + y: &Self::Variable, + position: Self::Position, + ) -> Self::Variable { + let x: u32 = (*x).try_into().unwrap(); + let y: u32 = (*y).try_into().unwrap(); + let res = (x as u64) * (y as u64); + let res = (res >> 32) as u32; + let res = res as u64; + self.write_column(position, res); + res + } + unsafe fn mul_hi_lo( &mut self, x: &Self::Variable, From 840066e8613d15a3bd7cfeab8c88ba8aece0eb8f Mon Sep 17 00:00:00 2001 From: Danny Willems Date: Wed, 20 Nov 2024 16:24:28 +0100 Subject: [PATCH 39/63] o1vm/riscv32: implement mul_lo --- o1vm/src/interpreters/riscv32im/constraints.rs | 9 +++++++++ o1vm/src/interpreters/riscv32im/interpreter.rs | 14 ++++++++++++++ o1vm/src/interpreters/riscv32im/witness.rs | 15 +++++++++++++++ 3 files changed, 38 insertions(+) diff --git a/o1vm/src/interpreters/riscv32im/constraints.rs b/o1vm/src/interpreters/riscv32im/constraints.rs index ef1496ae80..e173e8fecb 100644 --- a/o1vm/src/interpreters/riscv32im/constraints.rs +++ b/o1vm/src/interpreters/riscv32im/constraints.rs @@ -354,6 +354,15 @@ impl InterpreterEnv for Env { self.variable(position) } + unsafe fn mul_lo( + &mut self, + _x: &Self::Variable, + _y: &Self::Variable, + position: Self::Position, + ) -> Self::Variable { + self.variable(position) + } + unsafe fn mul_hi_lo( &mut self, _x: &Self::Variable, diff --git a/o1vm/src/interpreters/riscv32im/interpreter.rs b/o1vm/src/interpreters/riscv32im/interpreter.rs index 905efe547f..0633895a46 100644 --- a/o1vm/src/interpreters/riscv32im/interpreter.rs +++ b/o1vm/src/interpreters/riscv32im/interpreter.rs @@ -1259,6 +1259,20 @@ pub trait InterpreterEnv { position: Self::Position, ) -> Self::Variable; + /// Returns `(x * y) & ((1 << 32) - 1))`, storing the results in `position`. + /// + /// # Safety + /// + /// There are no constraints on the returned values; callers must manually add constraints to + /// ensure that the pair of returned values correspond to the given values `x` and `y`, and + /// that they fall within the desired range. + unsafe fn mul_lo( + &mut self, + x: &Self::Variable, + y: &Self::Variable, + position: Self::Position, + ) -> Self::Variable; + /// Returns `((x * y) >> 32, (x * y) & ((1 << 32) - 1))`, storing the results in `position_hi` /// and `position_lo` respectively. /// diff --git a/o1vm/src/interpreters/riscv32im/witness.rs b/o1vm/src/interpreters/riscv32im/witness.rs index fa919adb16..e358051512 100644 --- a/o1vm/src/interpreters/riscv32im/witness.rs +++ b/o1vm/src/interpreters/riscv32im/witness.rs @@ -505,6 +505,21 @@ impl InterpreterEnv for Env { res } + unsafe fn mul_lo( + &mut self, + x: &Self::Variable, + y: &Self::Variable, + position: Self::Position, + ) -> Self::Variable { + let x: u32 = (*x).try_into().unwrap(); + let y: u32 = (*y).try_into().unwrap(); + let res = (x as u64) * (y as u64); + let res = (res & ((1 << 32) - 1)) as u32; + let res = res as u64; + self.write_column(position, res); + res + } + unsafe fn mul_hi_lo( &mut self, x: &Self::Variable, From 4d833a21d54529aa8406bd74370e196ab8662444 Mon Sep 17 00:00:00 2001 From: Danny Willems Date: Wed, 20 Nov 2024 16:26:54 +0100 Subject: [PATCH 40/63] o1vm/riscv32: implement M type instruction Mul --- o1vm/src/interpreters/riscv32im/interpreter.rs | 14 ++++++++++++-- 1 file changed, 12 insertions(+), 2 deletions(-) diff --git a/o1vm/src/interpreters/riscv32im/interpreter.rs b/o1vm/src/interpreters/riscv32im/interpreter.rs index 0633895a46..3ad530280c 100644 --- a/o1vm/src/interpreters/riscv32im/interpreter.rs +++ b/o1vm/src/interpreters/riscv32im/interpreter.rs @@ -2089,7 +2089,7 @@ pub fn interpret_syscall(env: &mut Env, _instr: SyscallInst /// [here](https://www.cs.cornell.edu/courses/cs3410/2024fa/assignments/cpusim/riscv-instructions.pdf) pub fn interpret_mtype(env: &mut Env, instr: MInstruction) { let instruction_pointer = env.get_instruction_pointer(); - let _next_instruction_pointer = env.get_next_instruction_pointer(); + let next_instruction_pointer = env.get_next_instruction_pointer(); let instruction = { let v0 = env.read_memory(&instruction_pointer); @@ -2160,7 +2160,17 @@ pub fn interpret_mtype(env: &mut Env, instr: MInstruction) match instr { MInstruction::Mul => { - unimplemented!("Mul") + let rs1 = env.read_register(&rs1); + let rs2 = env.read_register(&rs2); + // FIXME: constrain + let res = { + let pos = env.alloc_scratch(); + unsafe { env.mul_lo_signed(&rs1, &rs2, pos) } + }; + env.write_register(&rd, res); + + env.set_instruction_pointer(next_instruction_pointer.clone()); + env.set_next_instruction_pointer(next_instruction_pointer + Env::constant(4u32)); } MInstruction::Mulh => { unimplemented!("Mulh") From 93afc08c23c615005589282136d4a90e2b08e0b0 Mon Sep 17 00:00:00 2001 From: Danny Willems Date: Wed, 20 Nov 2024 16:28:03 +0100 Subject: [PATCH 41/63] o1vm/riscv32: implement mulh --- o1vm/src/interpreters/riscv32im/interpreter.rs | 12 +++++++++++- 1 file changed, 11 insertions(+), 1 deletion(-) diff --git a/o1vm/src/interpreters/riscv32im/interpreter.rs b/o1vm/src/interpreters/riscv32im/interpreter.rs index ec959f514d..96a15a9130 100644 --- a/o1vm/src/interpreters/riscv32im/interpreter.rs +++ b/o1vm/src/interpreters/riscv32im/interpreter.rs @@ -2222,7 +2222,17 @@ pub fn interpret_mtype(env: &mut Env, instr: MInstruction) env.set_next_instruction_pointer(next_instruction_pointer + Env::constant(4u32)); } MInstruction::Mulh => { - unimplemented!("Mulh") + let rs1 = env.read_register(&rs1); + let rs2 = env.read_register(&rs2); + // FIXME: constrain + let res = { + let pos = env.alloc_scratch(); + unsafe { env.mul_hi_signed(&rs1, &rs2, pos) } + }; + env.write_register(&rd, res); + + env.set_instruction_pointer(next_instruction_pointer.clone()); + env.set_next_instruction_pointer(next_instruction_pointer + Env::constant(4u32)); } MInstruction::Mulhsu => { unimplemented!("Mulhsu") From e752cac243d2827994467cb4dcc8fb89e09de95e Mon Sep 17 00:00:00 2001 From: Danny Willems Date: Wed, 20 Nov 2024 16:30:38 +0100 Subject: [PATCH 42/63] o1vm/riscv32: implement Mulhu --- o1vm/src/interpreters/riscv32im/interpreter.rs | 12 +++++++++++- 1 file changed, 11 insertions(+), 1 deletion(-) diff --git a/o1vm/src/interpreters/riscv32im/interpreter.rs b/o1vm/src/interpreters/riscv32im/interpreter.rs index 96a15a9130..721a4de4aa 100644 --- a/o1vm/src/interpreters/riscv32im/interpreter.rs +++ b/o1vm/src/interpreters/riscv32im/interpreter.rs @@ -2238,7 +2238,17 @@ pub fn interpret_mtype(env: &mut Env, instr: MInstruction) unimplemented!("Mulhsu") } MInstruction::Mulhu => { - unimplemented!("Mulhu") + let rs1 = env.read_register(&rs1); + let rs2 = env.read_register(&rs2); + // FIXME: constrain + let res = { + let pos = env.alloc_scratch(); + unsafe { env.mul_hi(&rs1, &rs2, pos) } + }; + env.write_register(&rd, res); + + env.set_instruction_pointer(next_instruction_pointer.clone()); + env.set_next_instruction_pointer(next_instruction_pointer + Env::constant(4u32)); } MInstruction::Div => { unimplemented!("Div") From 4641725fc3dd6eec122f44c23463d9452b07e553 Mon Sep 17 00:00:00 2001 From: Danny Willems Date: Wed, 20 Nov 2024 16:34:33 +0100 Subject: [PATCH 43/63] o1vm/riscv32: remove unused mul_hi_lo_signed The method is splitted in two different methods, comparetively to MIPS. --- .../src/interpreters/riscv32im/constraints.rs | 10 ---------- .../src/interpreters/riscv32im/interpreter.rs | 16 ---------------- o1vm/src/interpreters/riscv32im/witness.rs | 19 ------------------- 3 files changed, 45 deletions(-) diff --git a/o1vm/src/interpreters/riscv32im/constraints.rs b/o1vm/src/interpreters/riscv32im/constraints.rs index e173e8fecb..21d7ca1fce 100644 --- a/o1vm/src/interpreters/riscv32im/constraints.rs +++ b/o1vm/src/interpreters/riscv32im/constraints.rs @@ -317,16 +317,6 @@ impl InterpreterEnv for Env { self.variable(position) } - unsafe fn mul_hi_lo_signed( - &mut self, - _x: &Self::Variable, - _y: &Self::Variable, - position_hi: Self::Position, - position_lo: Self::Position, - ) -> (Self::Variable, Self::Variable) { - (self.variable(position_hi), self.variable(position_lo)) - } - unsafe fn mul_hi_signed( &mut self, _x: &Self::Variable, diff --git a/o1vm/src/interpreters/riscv32im/interpreter.rs b/o1vm/src/interpreters/riscv32im/interpreter.rs index 721a4de4aa..82d3b73c8d 100644 --- a/o1vm/src/interpreters/riscv32im/interpreter.rs +++ b/o1vm/src/interpreters/riscv32im/interpreter.rs @@ -1229,22 +1229,6 @@ pub trait InterpreterEnv { position: Self::Position, ) -> Self::Variable; - /// Returns `((x * y) >> 32, (x * y) & ((1 << 32) - 1))`, storing the results in `position_hi` - /// and `position_lo` respectively. - /// - /// # Safety - /// - /// There are no constraints on the returned values; callers must manually add constraints to - /// ensure that the pair of returned values correspond to the given values `x` and `y`, and - /// that they fall within the desired range. - unsafe fn mul_hi_lo_signed( - &mut self, - x: &Self::Variable, - y: &Self::Variable, - position_hi: Self::Position, - position_lo: Self::Position, - ) -> (Self::Variable, Self::Variable); - /// Returns `((x * y) >> 32`, storing the results in `position`. /// /// # Safety diff --git a/o1vm/src/interpreters/riscv32im/witness.rs b/o1vm/src/interpreters/riscv32im/witness.rs index e358051512..24cc710f46 100644 --- a/o1vm/src/interpreters/riscv32im/witness.rs +++ b/o1vm/src/interpreters/riscv32im/witness.rs @@ -471,25 +471,6 @@ impl InterpreterEnv for Env { res } - unsafe fn mul_hi_lo_signed( - &mut self, - x: &Self::Variable, - y: &Self::Variable, - position_hi: Self::Position, - position_lo: Self::Position, - ) -> (Self::Variable, Self::Variable) { - let x: u32 = (*x).try_into().unwrap(); - let y: u32 = (*y).try_into().unwrap(); - let mul = (((x as i32) as i64) * ((y as i32) as i64)) as u64; - let hi = (mul >> 32) as u32; - let lo = (mul & ((1 << 32) - 1)) as u32; - let hi = hi as u64; - let lo = lo as u64; - self.write_column(position_hi, hi); - self.write_column(position_lo, lo); - (hi, lo) - } - unsafe fn mul_hi( &mut self, x: &Self::Variable, From f07b581dee5bffd18d0cc352feebba283f079994 Mon Sep 17 00:00:00 2001 From: Danny Willems Date: Wed, 20 Nov 2024 16:36:28 +0100 Subject: [PATCH 44/63] o1vm/riscv32: remove unused mul_hi_lo. Like mul_hi_lo_signed, the method is splitted in two different methods: mul_hi and mul_lo. --- .../src/interpreters/riscv32im/constraints.rs | 10 ---------- .../src/interpreters/riscv32im/interpreter.rs | 16 ---------------- o1vm/src/interpreters/riscv32im/witness.rs | 19 ------------------- 3 files changed, 45 deletions(-) diff --git a/o1vm/src/interpreters/riscv32im/constraints.rs b/o1vm/src/interpreters/riscv32im/constraints.rs index 21d7ca1fce..c270bee34a 100644 --- a/o1vm/src/interpreters/riscv32im/constraints.rs +++ b/o1vm/src/interpreters/riscv32im/constraints.rs @@ -353,16 +353,6 @@ impl InterpreterEnv for Env { self.variable(position) } - unsafe fn mul_hi_lo( - &mut self, - _x: &Self::Variable, - _y: &Self::Variable, - position_hi: Self::Position, - position_lo: Self::Position, - ) -> (Self::Variable, Self::Variable) { - (self.variable(position_hi), self.variable(position_lo)) - } - unsafe fn divmod_signed( &mut self, _x: &Self::Variable, diff --git a/o1vm/src/interpreters/riscv32im/interpreter.rs b/o1vm/src/interpreters/riscv32im/interpreter.rs index 82d3b73c8d..cb399f8c61 100644 --- a/o1vm/src/interpreters/riscv32im/interpreter.rs +++ b/o1vm/src/interpreters/riscv32im/interpreter.rs @@ -1257,22 +1257,6 @@ pub trait InterpreterEnv { position: Self::Position, ) -> Self::Variable; - /// Returns `((x * y) >> 32, (x * y) & ((1 << 32) - 1))`, storing the results in `position_hi` - /// and `position_lo` respectively. - /// - /// # Safety - /// - /// There are no constraints on the returned values; callers must manually add constraints to - /// ensure that the pair of returned values correspond to the given values `x` and `y`, and - /// that they fall within the desired range. - unsafe fn mul_hi_lo( - &mut self, - x: &Self::Variable, - y: &Self::Variable, - position_hi: Self::Position, - position_lo: Self::Position, - ) -> (Self::Variable, Self::Variable); - /// Returns `(x / y, x % y)`, storing the results in `position_quotient` and /// `position_remainder` respectively. /// diff --git a/o1vm/src/interpreters/riscv32im/witness.rs b/o1vm/src/interpreters/riscv32im/witness.rs index 24cc710f46..10d6508721 100644 --- a/o1vm/src/interpreters/riscv32im/witness.rs +++ b/o1vm/src/interpreters/riscv32im/witness.rs @@ -501,25 +501,6 @@ impl InterpreterEnv for Env { res } - unsafe fn mul_hi_lo( - &mut self, - x: &Self::Variable, - y: &Self::Variable, - position_hi: Self::Position, - position_lo: Self::Position, - ) -> (Self::Variable, Self::Variable) { - let x: u32 = (*x).try_into().unwrap(); - let y: u32 = (*y).try_into().unwrap(); - let mul = (x as u64) * (y as u64); - let hi = (mul >> 32) as u32; - let lo = (mul & ((1 << 32) - 1)) as u32; - let hi = hi as u64; - let lo = lo as u64; - self.write_column(position_hi, hi); - self.write_column(position_lo, lo); - (hi, lo) - } - unsafe fn divmod_signed( &mut self, x: &Self::Variable, From 3815c8a5f69c7d9a748c30c830bdf9bde2f05664 Mon Sep 17 00:00:00 2001 From: Danny Willems Date: Wed, 20 Nov 2024 16:42:28 +0100 Subject: [PATCH 45/63] o1vm/riscv32: implement div_signed --- o1vm/src/interpreters/riscv32im/constraints.rs | 9 +++++++++ o1vm/src/interpreters/riscv32im/interpreter.rs | 14 ++++++++++++++ o1vm/src/interpreters/riscv32im/witness.rs | 14 ++++++++++++++ 3 files changed, 37 insertions(+) diff --git a/o1vm/src/interpreters/riscv32im/constraints.rs b/o1vm/src/interpreters/riscv32im/constraints.rs index c270bee34a..5f8236aed7 100644 --- a/o1vm/src/interpreters/riscv32im/constraints.rs +++ b/o1vm/src/interpreters/riscv32im/constraints.rs @@ -344,6 +344,15 @@ impl InterpreterEnv for Env { self.variable(position) } + unsafe fn div_signed( + &mut self, + _x: &Self::Variable, + _y: &Self::Variable, + position: Self::Position, + ) -> Self::Variable { + self.variable(position) + } + unsafe fn mul_lo( &mut self, _x: &Self::Variable, diff --git a/o1vm/src/interpreters/riscv32im/interpreter.rs b/o1vm/src/interpreters/riscv32im/interpreter.rs index df9dd7176e..036107a200 100644 --- a/o1vm/src/interpreters/riscv32im/interpreter.rs +++ b/o1vm/src/interpreters/riscv32im/interpreter.rs @@ -1257,6 +1257,20 @@ pub trait InterpreterEnv { position: Self::Position, ) -> Self::Variable; + /// Returns `x / y`, storing the results in `position`. + /// + /// # Safety + /// + /// There are no constraints on the returned values; callers must manually add constraints to + /// ensure that the pair of returned values correspond to the given values `x` and `y`, and + /// that they fall within the desired range. + unsafe fn div_signed( + &mut self, + x: &Self::Variable, + y: &Self::Variable, + position: Self::Position, + ) -> Self::Variable; + /// Returns `(x / y, x % y)`, storing the results in `position_quotient` and /// `position_remainder` respectively. /// diff --git a/o1vm/src/interpreters/riscv32im/witness.rs b/o1vm/src/interpreters/riscv32im/witness.rs index 10d6508721..8b29db4f63 100644 --- a/o1vm/src/interpreters/riscv32im/witness.rs +++ b/o1vm/src/interpreters/riscv32im/witness.rs @@ -486,6 +486,20 @@ impl InterpreterEnv for Env { res } + unsafe fn div_signed( + &mut self, + x: &Self::Variable, + y: &Self::Variable, + position: Self::Position, + ) -> Self::Variable { + let x: u32 = (*x).try_into().unwrap(); + let y: u32 = (*y).try_into().unwrap(); + let res = ((x as i32) / (y as i32)) as u32; + let res = res as u64; + self.write_column(position, res); + res + } + unsafe fn mul_lo( &mut self, x: &Self::Variable, From bb6f118d49fd5fa9b61550e1798d6760a38d6c00 Mon Sep 17 00:00:00 2001 From: Danny Willems Date: Mon, 25 Nov 2024 10:53:12 +0100 Subject: [PATCH 46/63] o1vm/riscv32im: simplify div_signed --- o1vm/src/interpreters/riscv32im/witness.rs | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/o1vm/src/interpreters/riscv32im/witness.rs b/o1vm/src/interpreters/riscv32im/witness.rs index 8b29db4f63..895ab46e1c 100644 --- a/o1vm/src/interpreters/riscv32im/witness.rs +++ b/o1vm/src/interpreters/riscv32im/witness.rs @@ -492,9 +492,9 @@ impl InterpreterEnv for Env { y: &Self::Variable, position: Self::Position, ) -> Self::Variable { - let x: u32 = (*x).try_into().unwrap(); - let y: u32 = (*y).try_into().unwrap(); - let res = ((x as i32) / (y as i32)) as u32; + let x: i32 = (*x).try_into().unwrap(); + let y: i32 = (*y).try_into().unwrap(); + let res = (x / y) as u32; let res = res as u64; self.write_column(position, res); res From 7367e4b86bfdd08903ffd5ec4e27bb7be7731eff Mon Sep 17 00:00:00 2001 From: Danny Willems Date: Wed, 20 Nov 2024 16:43:33 +0100 Subject: [PATCH 47/63] o1vm/riscv32: implement M type instruction div --- o1vm/src/interpreters/riscv32im/interpreter.rs | 12 +++++++++++- 1 file changed, 11 insertions(+), 1 deletion(-) diff --git a/o1vm/src/interpreters/riscv32im/interpreter.rs b/o1vm/src/interpreters/riscv32im/interpreter.rs index 036107a200..438abaa065 100644 --- a/o1vm/src/interpreters/riscv32im/interpreter.rs +++ b/o1vm/src/interpreters/riscv32im/interpreter.rs @@ -2250,7 +2250,17 @@ pub fn interpret_mtype(env: &mut Env, instr: MInstruction) env.set_next_instruction_pointer(next_instruction_pointer + Env::constant(4u32)); } MInstruction::Div => { - unimplemented!("Div") + let rs1 = env.read_register(&rs1); + let rs2 = env.read_register(&rs2); + // FIXME: constrain + let res = { + let pos = env.alloc_scratch(); + unsafe { env.div_signed(&rs1, &rs2, pos) } + }; + env.write_register(&rd, res); + + env.set_instruction_pointer(next_instruction_pointer.clone()); + env.set_next_instruction_pointer(next_instruction_pointer + Env::constant(4u32)); } MInstruction::Divu => { unimplemented!("Divu") From 0ad5fea2a06952e9f1c5dcf10bd08ef9404fcad1 Mon Sep 17 00:00:00 2001 From: Danny Willems Date: Wed, 20 Nov 2024 16:47:06 +0100 Subject: [PATCH 48/63] o1vm/riscv32: implement mod_signed It will be used to implement MInstruction::Rem in a follow-up PR. --- o1vm/src/interpreters/riscv32im/constraints.rs | 9 +++++++++ o1vm/src/interpreters/riscv32im/interpreter.rs | 14 ++++++++++++++ o1vm/src/interpreters/riscv32im/witness.rs | 14 ++++++++++++++ 3 files changed, 37 insertions(+) diff --git a/o1vm/src/interpreters/riscv32im/constraints.rs b/o1vm/src/interpreters/riscv32im/constraints.rs index 5f8236aed7..67bfa46fea 100644 --- a/o1vm/src/interpreters/riscv32im/constraints.rs +++ b/o1vm/src/interpreters/riscv32im/constraints.rs @@ -353,6 +353,15 @@ impl InterpreterEnv for Env { self.variable(position) } + unsafe fn mod_signed( + &mut self, + _x: &Self::Variable, + _y: &Self::Variable, + position: Self::Position, + ) -> Self::Variable { + self.variable(position) + } + unsafe fn mul_lo( &mut self, _x: &Self::Variable, diff --git a/o1vm/src/interpreters/riscv32im/interpreter.rs b/o1vm/src/interpreters/riscv32im/interpreter.rs index 438abaa065..7e0826abad 100644 --- a/o1vm/src/interpreters/riscv32im/interpreter.rs +++ b/o1vm/src/interpreters/riscv32im/interpreter.rs @@ -1271,6 +1271,20 @@ pub trait InterpreterEnv { position: Self::Position, ) -> Self::Variable; + /// Returns `x % y`, storing the results in `position`. + /// + /// # Safety + /// + /// There are no constraints on the returned values; callers must manually add constraints to + /// ensure that the pair of returned values correspond to the given values `x` and `y`, and + /// that they fall within the desired range. + unsafe fn mod_signed( + &mut self, + x: &Self::Variable, + y: &Self::Variable, + position: Self::Position, + ) -> Self::Variable; + /// Returns `(x / y, x % y)`, storing the results in `position_quotient` and /// `position_remainder` respectively. /// diff --git a/o1vm/src/interpreters/riscv32im/witness.rs b/o1vm/src/interpreters/riscv32im/witness.rs index 895ab46e1c..6c87d64b8e 100644 --- a/o1vm/src/interpreters/riscv32im/witness.rs +++ b/o1vm/src/interpreters/riscv32im/witness.rs @@ -515,6 +515,20 @@ impl InterpreterEnv for Env { res } + unsafe fn mod_signed( + &mut self, + x: &Self::Variable, + y: &Self::Variable, + position: Self::Position, + ) -> Self::Variable { + let x: u32 = (*x).try_into().unwrap(); + let y: u32 = (*y).try_into().unwrap(); + let res = ((x as i32) % (y as i32)) as u32; + let res = res as u64; + self.write_column(position, res); + res + } + unsafe fn divmod_signed( &mut self, x: &Self::Variable, From 4e0220dbd6c09aaff3578d8f8a3f322674f4c9f4 Mon Sep 17 00:00:00 2001 From: Danny Willems Date: Mon, 25 Nov 2024 10:57:40 +0100 Subject: [PATCH 49/63] o1vm/riscv32im: simplify mod_signed --- o1vm/src/interpreters/riscv32im/witness.rs | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/o1vm/src/interpreters/riscv32im/witness.rs b/o1vm/src/interpreters/riscv32im/witness.rs index 6c87d64b8e..bb0e0cf6c5 100644 --- a/o1vm/src/interpreters/riscv32im/witness.rs +++ b/o1vm/src/interpreters/riscv32im/witness.rs @@ -521,9 +521,9 @@ impl InterpreterEnv for Env { y: &Self::Variable, position: Self::Position, ) -> Self::Variable { - let x: u32 = (*x).try_into().unwrap(); - let y: u32 = (*y).try_into().unwrap(); - let res = ((x as i32) % (y as i32)) as u32; + let x: i32 = (*x).try_into().unwrap(); + let y: i32 = (*y).try_into().unwrap(); + let res = (x % y) as u32; let res = res as u64; self.write_column(position, res); res From 77a50c46fa2c2a4feb16d81cab098bda86207d6d Mon Sep 17 00:00:00 2001 From: Danny Willems Date: Wed, 20 Nov 2024 16:49:00 +0100 Subject: [PATCH 50/63] o1vm/riscv32: remove unused divmod_signed As for mul_hi_lo(_signed), the method is splitted. --- o1vm/src/interpreters/riscv32im/constraints.rs | 13 ------------- o1vm/src/interpreters/riscv32im/interpreter.rs | 16 ---------------- o1vm/src/interpreters/riscv32im/witness.rs | 18 ------------------ 3 files changed, 47 deletions(-) diff --git a/o1vm/src/interpreters/riscv32im/constraints.rs b/o1vm/src/interpreters/riscv32im/constraints.rs index 67bfa46fea..cf154f1cca 100644 --- a/o1vm/src/interpreters/riscv32im/constraints.rs +++ b/o1vm/src/interpreters/riscv32im/constraints.rs @@ -371,19 +371,6 @@ impl InterpreterEnv for Env { self.variable(position) } - unsafe fn divmod_signed( - &mut self, - _x: &Self::Variable, - _y: &Self::Variable, - position_quotient: Self::Position, - position_remainder: Self::Position, - ) -> (Self::Variable, Self::Variable) { - ( - self.variable(position_quotient), - self.variable(position_remainder), - ) - } - unsafe fn divmod( &mut self, _x: &Self::Variable, diff --git a/o1vm/src/interpreters/riscv32im/interpreter.rs b/o1vm/src/interpreters/riscv32im/interpreter.rs index 7e0826abad..bec354f46e 100644 --- a/o1vm/src/interpreters/riscv32im/interpreter.rs +++ b/o1vm/src/interpreters/riscv32im/interpreter.rs @@ -1285,22 +1285,6 @@ pub trait InterpreterEnv { position: Self::Position, ) -> Self::Variable; - /// Returns `(x / y, x % y)`, storing the results in `position_quotient` and - /// `position_remainder` respectively. - /// - /// # Safety - /// - /// There are no constraints on the returned values; callers must manually add constraints to - /// ensure that the pair of returned values correspond to the given values `x` and `y`, and - /// that they fall within the desired range. - unsafe fn divmod_signed( - &mut self, - x: &Self::Variable, - y: &Self::Variable, - position_quotient: Self::Position, - position_remainder: Self::Position, - ) -> (Self::Variable, Self::Variable); - /// Returns `(x / y, x % y)`, storing the results in `position_quotient` and /// `position_remainder` respectively. /// diff --git a/o1vm/src/interpreters/riscv32im/witness.rs b/o1vm/src/interpreters/riscv32im/witness.rs index bb0e0cf6c5..a2e169b76c 100644 --- a/o1vm/src/interpreters/riscv32im/witness.rs +++ b/o1vm/src/interpreters/riscv32im/witness.rs @@ -529,24 +529,6 @@ impl InterpreterEnv for Env { res } - unsafe fn divmod_signed( - &mut self, - x: &Self::Variable, - y: &Self::Variable, - position_quotient: Self::Position, - position_remainder: Self::Position, - ) -> (Self::Variable, Self::Variable) { - let x: u32 = (*x).try_into().unwrap(); - let y: u32 = (*y).try_into().unwrap(); - let q = ((x as i32) / (y as i32)) as u32; - let r = ((x as i32) % (y as i32)) as u32; - let q = q as u64; - let r = r as u64; - self.write_column(position_quotient, q); - self.write_column(position_remainder, r); - (q, r) - } - unsafe fn divmod( &mut self, x: &Self::Variable, From deedbff6e1496f94adf57a766de90a949d8f3426 Mon Sep 17 00:00:00 2001 From: Danny Willems Date: Wed, 20 Nov 2024 16:51:28 +0100 Subject: [PATCH 51/63] o1vm/riscv32: implement M type instruction Rem --- o1vm/src/interpreters/riscv32im/interpreter.rs | 12 +++++++++++- 1 file changed, 11 insertions(+), 1 deletion(-) diff --git a/o1vm/src/interpreters/riscv32im/interpreter.rs b/o1vm/src/interpreters/riscv32im/interpreter.rs index bec354f46e..87fe1861e7 100644 --- a/o1vm/src/interpreters/riscv32im/interpreter.rs +++ b/o1vm/src/interpreters/riscv32im/interpreter.rs @@ -2264,7 +2264,17 @@ pub fn interpret_mtype(env: &mut Env, instr: MInstruction) unimplemented!("Divu") } MInstruction::Rem => { - unimplemented!("Rem") + let rs1 = env.read_register(&rs1); + let rs2 = env.read_register(&rs2); + // FIXME: constrain + let res = { + let pos = env.alloc_scratch(); + unsafe { env.mod_signed(&rs1, &rs2, pos) } + }; + env.write_register(&rd, res); + + env.set_instruction_pointer(next_instruction_pointer.clone()); + env.set_next_instruction_pointer(next_instruction_pointer + Env::constant(4u32)); } MInstruction::Remu => { unimplemented!("Remu") From 85639cae3edeef7cd92f6ba2fe7aa6eaac1713a2 Mon Sep 17 00:00:00 2001 From: Danny Willems Date: Wed, 20 Nov 2024 16:55:11 +0100 Subject: [PATCH 52/63] o1vm/riscv32: implement div for unsigned 32bits Will be used to implement MInstruction::Divu --- o1vm/src/interpreters/riscv32im/constraints.rs | 9 +++++++++ o1vm/src/interpreters/riscv32im/interpreter.rs | 14 ++++++++++++++ o1vm/src/interpreters/riscv32im/witness.rs | 14 ++++++++++++++ 3 files changed, 37 insertions(+) diff --git a/o1vm/src/interpreters/riscv32im/constraints.rs b/o1vm/src/interpreters/riscv32im/constraints.rs index cf154f1cca..41084472d1 100644 --- a/o1vm/src/interpreters/riscv32im/constraints.rs +++ b/o1vm/src/interpreters/riscv32im/constraints.rs @@ -362,6 +362,15 @@ impl InterpreterEnv for Env { self.variable(position) } + unsafe fn div( + &mut self, + _x: &Self::Variable, + _y: &Self::Variable, + position: Self::Position, + ) -> Self::Variable { + self.variable(position) + } + unsafe fn mul_lo( &mut self, _x: &Self::Variable, diff --git a/o1vm/src/interpreters/riscv32im/interpreter.rs b/o1vm/src/interpreters/riscv32im/interpreter.rs index 87fe1861e7..be39806fbc 100644 --- a/o1vm/src/interpreters/riscv32im/interpreter.rs +++ b/o1vm/src/interpreters/riscv32im/interpreter.rs @@ -1285,6 +1285,20 @@ pub trait InterpreterEnv { position: Self::Position, ) -> Self::Variable; + /// Returns `x / y`, storing the results in `position`. + /// + /// # Safety + /// + /// There are no constraints on the returned values; callers must manually add constraints to + /// ensure that the pair of returned values correspond to the given values `x` and `y`, and + /// that they fall within the desired range. + unsafe fn div( + &mut self, + x: &Self::Variable, + y: &Self::Variable, + position: Self::Position, + ) -> Self::Variable; + /// Returns `(x / y, x % y)`, storing the results in `position_quotient` and /// `position_remainder` respectively. /// diff --git a/o1vm/src/interpreters/riscv32im/witness.rs b/o1vm/src/interpreters/riscv32im/witness.rs index a2e169b76c..d29b3d863e 100644 --- a/o1vm/src/interpreters/riscv32im/witness.rs +++ b/o1vm/src/interpreters/riscv32im/witness.rs @@ -529,6 +529,20 @@ impl InterpreterEnv for Env { res } + unsafe fn div( + &mut self, + x: &Self::Variable, + y: &Self::Variable, + position: Self::Position, + ) -> Self::Variable { + let x: u32 = (*x).try_into().unwrap(); + let y: u32 = (*y).try_into().unwrap(); + let res = x / y; + let res = res as u64; + self.write_column(position, res); + res + } + unsafe fn divmod( &mut self, x: &Self::Variable, From c9207b8ea3bbda2cde7ea9c6b7147ea9d04e9805 Mon Sep 17 00:00:00 2001 From: Danny Willems Date: Wed, 20 Nov 2024 16:57:29 +0100 Subject: [PATCH 53/63] o1vm/riscv32: implement mod_ It will be used to implement MInstruction::Remu in a follow-up PR. --- o1vm/src/interpreters/riscv32im/constraints.rs | 9 +++++++++ o1vm/src/interpreters/riscv32im/interpreter.rs | 14 ++++++++++++++ o1vm/src/interpreters/riscv32im/witness.rs | 14 ++++++++++++++ 3 files changed, 37 insertions(+) diff --git a/o1vm/src/interpreters/riscv32im/constraints.rs b/o1vm/src/interpreters/riscv32im/constraints.rs index 41084472d1..1713346ab4 100644 --- a/o1vm/src/interpreters/riscv32im/constraints.rs +++ b/o1vm/src/interpreters/riscv32im/constraints.rs @@ -371,6 +371,15 @@ impl InterpreterEnv for Env { self.variable(position) } + unsafe fn mod_( + &mut self, + _x: &Self::Variable, + _y: &Self::Variable, + position: Self::Position, + ) -> Self::Variable { + self.variable(position) + } + unsafe fn mul_lo( &mut self, _x: &Self::Variable, diff --git a/o1vm/src/interpreters/riscv32im/interpreter.rs b/o1vm/src/interpreters/riscv32im/interpreter.rs index be39806fbc..3f9a60f645 100644 --- a/o1vm/src/interpreters/riscv32im/interpreter.rs +++ b/o1vm/src/interpreters/riscv32im/interpreter.rs @@ -1299,6 +1299,20 @@ pub trait InterpreterEnv { position: Self::Position, ) -> Self::Variable; + /// Returns `x % y`, storing the results in `position`. + /// + /// # Safety + /// + /// There are no constraints on the returned values; callers must manually add constraints to + /// ensure that the pair of returned values correspond to the given values `x` and `y`, and + /// that they fall within the desired range. + unsafe fn mod_( + &mut self, + x: &Self::Variable, + y: &Self::Variable, + position: Self::Position, + ) -> Self::Variable; + /// Returns `(x / y, x % y)`, storing the results in `position_quotient` and /// `position_remainder` respectively. /// diff --git a/o1vm/src/interpreters/riscv32im/witness.rs b/o1vm/src/interpreters/riscv32im/witness.rs index d29b3d863e..06a9bc00ac 100644 --- a/o1vm/src/interpreters/riscv32im/witness.rs +++ b/o1vm/src/interpreters/riscv32im/witness.rs @@ -543,6 +543,20 @@ impl InterpreterEnv for Env { res } + unsafe fn mod_( + &mut self, + x: &Self::Variable, + y: &Self::Variable, + position: Self::Position, + ) -> Self::Variable { + let x: u32 = (*x).try_into().unwrap(); + let y: u32 = (*y).try_into().unwrap(); + let res = x % y; + let res = res as u64; + self.write_column(position, res); + res + } + unsafe fn divmod( &mut self, x: &Self::Variable, From 517924f0015fa80ce1e5516ee7cc75fa63eb25c0 Mon Sep 17 00:00:00 2001 From: Danny Willems Date: Mon, 25 Nov 2024 10:56:05 +0100 Subject: [PATCH 54/63] o1vm/riscv32im: rename mod_ in mod_unsigned for readability --- o1vm/src/interpreters/riscv32im/constraints.rs | 2 +- o1vm/src/interpreters/riscv32im/interpreter.rs | 2 +- o1vm/src/interpreters/riscv32im/witness.rs | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) diff --git a/o1vm/src/interpreters/riscv32im/constraints.rs b/o1vm/src/interpreters/riscv32im/constraints.rs index 1713346ab4..9fbdb8fbc8 100644 --- a/o1vm/src/interpreters/riscv32im/constraints.rs +++ b/o1vm/src/interpreters/riscv32im/constraints.rs @@ -371,7 +371,7 @@ impl InterpreterEnv for Env { self.variable(position) } - unsafe fn mod_( + unsafe fn mod_unsigned( &mut self, _x: &Self::Variable, _y: &Self::Variable, diff --git a/o1vm/src/interpreters/riscv32im/interpreter.rs b/o1vm/src/interpreters/riscv32im/interpreter.rs index 3f9a60f645..0222924c78 100644 --- a/o1vm/src/interpreters/riscv32im/interpreter.rs +++ b/o1vm/src/interpreters/riscv32im/interpreter.rs @@ -1306,7 +1306,7 @@ pub trait InterpreterEnv { /// There are no constraints on the returned values; callers must manually add constraints to /// ensure that the pair of returned values correspond to the given values `x` and `y`, and /// that they fall within the desired range. - unsafe fn mod_( + unsafe fn mod_unsigned( &mut self, x: &Self::Variable, y: &Self::Variable, diff --git a/o1vm/src/interpreters/riscv32im/witness.rs b/o1vm/src/interpreters/riscv32im/witness.rs index 06a9bc00ac..8a1502c6ea 100644 --- a/o1vm/src/interpreters/riscv32im/witness.rs +++ b/o1vm/src/interpreters/riscv32im/witness.rs @@ -543,7 +543,7 @@ impl InterpreterEnv for Env { res } - unsafe fn mod_( + unsafe fn mod_unsigned( &mut self, x: &Self::Variable, y: &Self::Variable, From 7482d1b4d356a6f4c906836535742387c6deb3cc Mon Sep 17 00:00:00 2001 From: Danny Willems Date: Wed, 20 Nov 2024 16:59:21 +0100 Subject: [PATCH 55/63] o1vm/riscv32: remove unused divmod As for mul_hi_lo(_signed), the method is splitted as there are individual instructions for div and mod. --- o1vm/src/interpreters/riscv32im/constraints.rs | 13 ------------- o1vm/src/interpreters/riscv32im/interpreter.rs | 16 ---------------- o1vm/src/interpreters/riscv32im/witness.rs | 18 ------------------ 3 files changed, 47 deletions(-) diff --git a/o1vm/src/interpreters/riscv32im/constraints.rs b/o1vm/src/interpreters/riscv32im/constraints.rs index 9fbdb8fbc8..2b02d708eb 100644 --- a/o1vm/src/interpreters/riscv32im/constraints.rs +++ b/o1vm/src/interpreters/riscv32im/constraints.rs @@ -389,19 +389,6 @@ impl InterpreterEnv for Env { self.variable(position) } - unsafe fn divmod( - &mut self, - _x: &Self::Variable, - _y: &Self::Variable, - position_quotient: Self::Position, - position_remainder: Self::Position, - ) -> (Self::Variable, Self::Variable) { - ( - self.variable(position_quotient), - self.variable(position_remainder), - ) - } - unsafe fn count_leading_zeros( &mut self, _x: &Self::Variable, diff --git a/o1vm/src/interpreters/riscv32im/interpreter.rs b/o1vm/src/interpreters/riscv32im/interpreter.rs index 0222924c78..c7a5e3bc17 100644 --- a/o1vm/src/interpreters/riscv32im/interpreter.rs +++ b/o1vm/src/interpreters/riscv32im/interpreter.rs @@ -1313,22 +1313,6 @@ pub trait InterpreterEnv { position: Self::Position, ) -> Self::Variable; - /// Returns `(x / y, x % y)`, storing the results in `position_quotient` and - /// `position_remainder` respectively. - /// - /// # Safety - /// - /// There are no constraints on the returned values; callers must manually add constraints to - /// ensure that the pair of returned values correspond to the given values `x` and `y`, and - /// that they fall within the desired range. - unsafe fn divmod( - &mut self, - x: &Self::Variable, - y: &Self::Variable, - position_quotient: Self::Position, - position_remainder: Self::Position, - ) -> (Self::Variable, Self::Variable); - /// Returns the number of leading 0s in `x`, storing the result in `position`. /// /// # Safety diff --git a/o1vm/src/interpreters/riscv32im/witness.rs b/o1vm/src/interpreters/riscv32im/witness.rs index 8a1502c6ea..61d2868886 100644 --- a/o1vm/src/interpreters/riscv32im/witness.rs +++ b/o1vm/src/interpreters/riscv32im/witness.rs @@ -557,24 +557,6 @@ impl InterpreterEnv for Env { res } - unsafe fn divmod( - &mut self, - x: &Self::Variable, - y: &Self::Variable, - position_quotient: Self::Position, - position_remainder: Self::Position, - ) -> (Self::Variable, Self::Variable) { - let x: u32 = (*x).try_into().unwrap(); - let y: u32 = (*y).try_into().unwrap(); - let q = x / y; - let r = x % y; - let q = q as u64; - let r = r as u64; - self.write_column(position_quotient, q); - self.write_column(position_remainder, r); - (q, r) - } - unsafe fn count_leading_zeros( &mut self, x: &Self::Variable, From 3dd7fe66ba9044856b8b41ed71ead2a4f63c9706 Mon Sep 17 00:00:00 2001 From: Mikhail Volkhov Date: Tue, 3 Dec 2024 11:40:49 +0000 Subject: [PATCH 56/63] Change comment notation to additive --- poly-commitment/src/ipa.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/poly-commitment/src/ipa.rs b/poly-commitment/src/ipa.rs index d68216f67c..17c561bb3d 100644 --- a/poly-commitment/src/ipa.rs +++ b/poly-commitment/src/ipa.rs @@ -745,7 +745,7 @@ impl SRS { let r_delta = ::rand(rng); // Compute delta, the commitment - // delta = G0^d * U_base^{b0*d} * H^r_delta (as a group element, in multiplicative notation) + // delta = [d] G0 + [b0*d] U_base + [r_delta] H^r (as a group element, in additive notation) let delta = ((g0.into_group() + (u_base.mul(b0))).into_affine().mul(d) + self.h.mul(r_delta)) .into_affine(); From 2e4d75418562c1964e1959eb4cb9f2b90b32719e Mon Sep 17 00:00:00 2001 From: Mikhail Volkhov Date: Tue, 3 Dec 2024 11:44:33 +0000 Subject: [PATCH 57/63] Rename d1_size to n_chunks in IVC prover --- ivc/src/prover.rs | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/ivc/src/prover.rs b/ivc/src/prover.rs index 719b2a8f61..8e318ad7a7 100644 --- a/ivc/src/prover.rs +++ b/ivc/src/prover.rs @@ -437,11 +437,11 @@ where let u = u_chal.to_field(endo_r); let coefficients_form = DensePolynomialOrEvaluations::DensePolynomial; - let non_hiding = |d1_size| PolyComm { - chunks: vec![Fp::zero(); d1_size], + let non_hiding = |n_chunks| PolyComm { + chunks: vec![Fp::zero(); n_chunks], }; - let hiding = |d1_size| PolyComm { - chunks: vec![Fp::one(); d1_size], + let hiding = |n_chunks| PolyComm { + chunks: vec![Fp::one(); n_chunks], }; // Gathering all polynomials_to_open to use in the opening proof From e08400805ac9c27353a5c244d4bcf7be7c038b55 Mon Sep 17 00:00:00 2001 From: Danny Willems Date: Wed, 20 Nov 2024 17:03:05 +0100 Subject: [PATCH 58/63] o1vm/riscv32: implement M type instruction divu --- o1vm/src/interpreters/riscv32im/interpreter.rs | 12 +++++++++++- 1 file changed, 11 insertions(+), 1 deletion(-) diff --git a/o1vm/src/interpreters/riscv32im/interpreter.rs b/o1vm/src/interpreters/riscv32im/interpreter.rs index c7a5e3bc17..d0e6630e07 100644 --- a/o1vm/src/interpreters/riscv32im/interpreter.rs +++ b/o1vm/src/interpreters/riscv32im/interpreter.rs @@ -2273,7 +2273,17 @@ pub fn interpret_mtype(env: &mut Env, instr: MInstruction) env.set_next_instruction_pointer(next_instruction_pointer + Env::constant(4u32)); } MInstruction::Divu => { - unimplemented!("Divu") + let rs1 = env.read_register(&rs1); + let rs2 = env.read_register(&rs2); + // FIXME: constrain + let res = { + let pos = env.alloc_scratch(); + unsafe { env.div(&rs1, &rs2, pos) } + }; + env.write_register(&rd, res); + + env.set_instruction_pointer(next_instruction_pointer.clone()); + env.set_next_instruction_pointer(next_instruction_pointer + Env::constant(4u32)); } MInstruction::Rem => { let rs1 = env.read_register(&rs1); From 4c5bff90bafd0f2fc984d01cb0a3d90a32fa904a Mon Sep 17 00:00:00 2001 From: Danny Willems Date: Wed, 20 Nov 2024 17:04:21 +0100 Subject: [PATCH 59/63] o1vm/riscv32: implement M type instruction Remu --- o1vm/src/interpreters/riscv32im/interpreter.rs | 12 +++++++++++- 1 file changed, 11 insertions(+), 1 deletion(-) diff --git a/o1vm/src/interpreters/riscv32im/interpreter.rs b/o1vm/src/interpreters/riscv32im/interpreter.rs index d0e6630e07..1797dde93e 100644 --- a/o1vm/src/interpreters/riscv32im/interpreter.rs +++ b/o1vm/src/interpreters/riscv32im/interpreter.rs @@ -2299,7 +2299,17 @@ pub fn interpret_mtype(env: &mut Env, instr: MInstruction) env.set_next_instruction_pointer(next_instruction_pointer + Env::constant(4u32)); } MInstruction::Remu => { - unimplemented!("Remu") + let rs1 = env.read_register(&rs1); + let rs2 = env.read_register(&rs2); + // FIXME: constrain + let res = { + let pos = env.alloc_scratch(); + unsafe { env.mod_unsigned(&rs1, &rs2, pos) } + }; + env.write_register(&rd, res); + + env.set_instruction_pointer(next_instruction_pointer.clone()); + env.set_next_instruction_pointer(next_instruction_pointer + Env::constant(4u32)); } } } From 1708293192548d66f1f3d9ad7f1cced7df0ab9af Mon Sep 17 00:00:00 2001 From: Danny Willems Date: Wed, 20 Nov 2024 17:14:02 +0100 Subject: [PATCH 60/63] o1vm/riscv32: implement mul_hi_signed_unsigned to be used for Mulhsu --- o1vm/src/interpreters/riscv32im/constraints.rs | 9 +++++++++ o1vm/src/interpreters/riscv32im/interpreter.rs | 14 ++++++++++++++ o1vm/src/interpreters/riscv32im/witness.rs | 15 +++++++++++++++ 3 files changed, 38 insertions(+) diff --git a/o1vm/src/interpreters/riscv32im/constraints.rs b/o1vm/src/interpreters/riscv32im/constraints.rs index 2b02d708eb..ba1633e1a7 100644 --- a/o1vm/src/interpreters/riscv32im/constraints.rs +++ b/o1vm/src/interpreters/riscv32im/constraints.rs @@ -344,6 +344,15 @@ impl InterpreterEnv for Env { self.variable(position) } + unsafe fn mul_hi_signed_unsigned( + &mut self, + _x: &Self::Variable, + _y: &Self::Variable, + position: Self::Position, + ) -> Self::Variable { + self.variable(position) + } + unsafe fn div_signed( &mut self, _x: &Self::Variable, diff --git a/o1vm/src/interpreters/riscv32im/interpreter.rs b/o1vm/src/interpreters/riscv32im/interpreter.rs index 1797dde93e..59fa7a6bd2 100644 --- a/o1vm/src/interpreters/riscv32im/interpreter.rs +++ b/o1vm/src/interpreters/riscv32im/interpreter.rs @@ -1257,6 +1257,20 @@ pub trait InterpreterEnv { position: Self::Position, ) -> Self::Variable; + /// Returns `((x * y) >> 32`, storing the results in `position`. + /// + /// # Safety + /// + /// There are no constraints on the returned values; callers must manually add constraints to + /// ensure that the pair of returned values correspond to the given values `x` and `y`, and + /// that they fall within the desired range. + unsafe fn mul_hi_signed_unsigned( + &mut self, + x: &Self::Variable, + y: &Self::Variable, + position: Self::Position, + ) -> Self::Variable; + /// Returns `x / y`, storing the results in `position`. /// /// # Safety diff --git a/o1vm/src/interpreters/riscv32im/witness.rs b/o1vm/src/interpreters/riscv32im/witness.rs index 61d2868886..e9a976ca13 100644 --- a/o1vm/src/interpreters/riscv32im/witness.rs +++ b/o1vm/src/interpreters/riscv32im/witness.rs @@ -486,6 +486,21 @@ impl InterpreterEnv for Env { res } + unsafe fn mul_hi_signed_unsigned( + &mut self, + x: &Self::Variable, + y: &Self::Variable, + position: Self::Position, + ) -> Self::Variable { + let x: u32 = (*x).try_into().unwrap(); + let y: u32 = (*y).try_into().unwrap(); + let res = (((x as i32) as i64) * (y as i64)) as u64; + let res = (res >> 32) as u32; + let res = res as u64; + self.write_column(position, res); + res + } + unsafe fn div_signed( &mut self, x: &Self::Variable, From 277cec86f478a800ed3b169e9ef2a6041bd34d96 Mon Sep 17 00:00:00 2001 From: Danny Willems Date: Wed, 20 Nov 2024 17:16:14 +0100 Subject: [PATCH 61/63] o1vm/riscv32: implement M type instruction Mulhsu --- o1vm/src/interpreters/riscv32im/interpreter.rs | 12 +++++++++++- 1 file changed, 11 insertions(+), 1 deletion(-) diff --git a/o1vm/src/interpreters/riscv32im/interpreter.rs b/o1vm/src/interpreters/riscv32im/interpreter.rs index 59fa7a6bd2..b657699967 100644 --- a/o1vm/src/interpreters/riscv32im/interpreter.rs +++ b/o1vm/src/interpreters/riscv32im/interpreter.rs @@ -2258,7 +2258,17 @@ pub fn interpret_mtype(env: &mut Env, instr: MInstruction) env.set_next_instruction_pointer(next_instruction_pointer + Env::constant(4u32)); } MInstruction::Mulhsu => { - unimplemented!("Mulhsu") + let rs1 = env.read_register(&rs1); + let rs2 = env.read_register(&rs2); + // FIXME: constrain + let res = { + let pos = env.alloc_scratch(); + unsafe { env.mul_hi_signed_unsigned(&rs1, &rs2, pos) } + }; + env.write_register(&rd, res); + + env.set_instruction_pointer(next_instruction_pointer.clone()); + env.set_next_instruction_pointer(next_instruction_pointer + Env::constant(4u32)); } MInstruction::Mulhu => { let rs1 = env.read_register(&rs1); From 54edc550095010a9eeda7132e78acaeaeb413022 Mon Sep 17 00:00:00 2001 From: Danny Willems Date: Mon, 25 Nov 2024 11:10:35 +0100 Subject: [PATCH 62/63] o1vm/riscv32im: improve documentation reg. semantic of op --- o1vm/src/interpreters/riscv32im/interpreter.rs | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/o1vm/src/interpreters/riscv32im/interpreter.rs b/o1vm/src/interpreters/riscv32im/interpreter.rs index b657699967..f13e3aa68e 100644 --- a/o1vm/src/interpreters/riscv32im/interpreter.rs +++ b/o1vm/src/interpreters/riscv32im/interpreter.rs @@ -20,6 +20,14 @@ //! and copied in this file for offline reference. //! If you are the author of the above documentations and would like to add or //! modify the credits, please open a pull request. +//! +//! For each instruction, we provide the format, description, and the +//! semantic in pseudo-code of the instruction. +//! When `signed` is mentioned in the pseudo-code, it means that the +//! operation is performed as a signed operation (i.e. signed(v) where `v` is a +//! 32 bits value means that `v` must be interpreted as a i32 value in Rust, the +//! most significant bit being the sign - 1 for negative, 0 for positive). +//! By default, unsigned operations are performed. use super::registers::{REGISTER_CURRENT_IP, REGISTER_HEAP_POINTER, REGISTER_NEXT_IP}; use crate::lookups::{Lookup, LookupTableIDs}; From 964cfeb7ad91aa21475cd0c8784b94800ac7b952 Mon Sep 17 00:00:00 2001 From: Danny Willems Date: Mon, 25 Nov 2024 11:11:00 +0100 Subject: [PATCH 63/63] o1vm/riscv32im: add semantic for MInstruction --- o1vm/src/interpreters/riscv32im/interpreter.rs | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/o1vm/src/interpreters/riscv32im/interpreter.rs b/o1vm/src/interpreters/riscv32im/interpreter.rs index f13e3aa68e..0bc94d1c7e 100644 --- a/o1vm/src/interpreters/riscv32im/interpreter.rs +++ b/o1vm/src/interpreters/riscv32im/interpreter.rs @@ -2240,6 +2240,7 @@ pub fn interpret_mtype(env: &mut Env, instr: MInstruction) match instr { MInstruction::Mul => { + // x[rd] = x[rs1] * x[rs2] let rs1 = env.read_register(&rs1); let rs2 = env.read_register(&rs2); // FIXME: constrain @@ -2253,6 +2254,7 @@ pub fn interpret_mtype(env: &mut Env, instr: MInstruction) env.set_next_instruction_pointer(next_instruction_pointer + Env::constant(4u32)); } MInstruction::Mulh => { + // x[rd] = (signed(x[rs1]) * signed(x[rs2])) >> 32 let rs1 = env.read_register(&rs1); let rs2 = env.read_register(&rs2); // FIXME: constrain @@ -2266,6 +2268,7 @@ pub fn interpret_mtype(env: &mut Env, instr: MInstruction) env.set_next_instruction_pointer(next_instruction_pointer + Env::constant(4u32)); } MInstruction::Mulhsu => { + // x[rd] = (signed(x[rs1]) * x[rs2]) >> 32 let rs1 = env.read_register(&rs1); let rs2 = env.read_register(&rs2); // FIXME: constrain @@ -2279,6 +2282,7 @@ pub fn interpret_mtype(env: &mut Env, instr: MInstruction) env.set_next_instruction_pointer(next_instruction_pointer + Env::constant(4u32)); } MInstruction::Mulhu => { + // x[rd] = (x[rs1] * x[rs2]) >> 32 let rs1 = env.read_register(&rs1); let rs2 = env.read_register(&rs2); // FIXME: constrain @@ -2292,6 +2296,7 @@ pub fn interpret_mtype(env: &mut Env, instr: MInstruction) env.set_next_instruction_pointer(next_instruction_pointer + Env::constant(4u32)); } MInstruction::Div => { + // x[rd] = signed(x[rs1]) / signed(x[rs2]) let rs1 = env.read_register(&rs1); let rs2 = env.read_register(&rs2); // FIXME: constrain @@ -2305,6 +2310,7 @@ pub fn interpret_mtype(env: &mut Env, instr: MInstruction) env.set_next_instruction_pointer(next_instruction_pointer + Env::constant(4u32)); } MInstruction::Divu => { + // x[rd] = x[rs1] / x[rs2] let rs1 = env.read_register(&rs1); let rs2 = env.read_register(&rs2); // FIXME: constrain @@ -2318,6 +2324,7 @@ pub fn interpret_mtype(env: &mut Env, instr: MInstruction) env.set_next_instruction_pointer(next_instruction_pointer + Env::constant(4u32)); } MInstruction::Rem => { + // x[rd] = signed(x[rs1]) % signed(x[rs2]) let rs1 = env.read_register(&rs1); let rs2 = env.read_register(&rs2); // FIXME: constrain @@ -2331,6 +2338,7 @@ pub fn interpret_mtype(env: &mut Env, instr: MInstruction) env.set_next_instruction_pointer(next_instruction_pointer + Env::constant(4u32)); } MInstruction::Remu => { + // x[rd] = x[rs1] % x[rs2] let rs1 = env.read_register(&rs1); let rs2 = env.read_register(&rs2); // FIXME: constrain