From 7d4d6db73397c6fbaeff9cf01760fd4830cf08be Mon Sep 17 00:00:00 2001 From: Mikhail Volkhov Date: Thu, 16 May 2024 14:30:19 +0100 Subject: [PATCH 1/9] [#2231] Add BlockSel columns into IVC --- ivc/src/ivc/columns.rs | 76 ++++++++++++++++++++++++++---------------- 1 file changed, 47 insertions(+), 29 deletions(-) diff --git a/ivc/src/ivc/columns.rs b/ivc/src/ivc/columns.rs index 313030bb63..e675ecfc1e 100644 --- a/ivc/src/ivc/columns.rs +++ b/ivc/src/ivc/columns.rs @@ -151,6 +151,9 @@ pub type IVCPoseidonColumn = PoseidonColumn Column { match self { + IVCColumn::BlockSel(i) => { + assert!(i < 2 * N_BLOCKS); + Column::FixedSelector(i) + } + IVCColumn::Block1Input(i) => { assert!(i < 2 * N_LIMBS_SMALL); - Column::Relation(i) + Column::Relation(N_BLOCKS + i) } IVCColumn::Block1InputRepacked75(i) => { assert!(i < 2 * N_LIMBS_LARGE); - Column::Relation(2 * N_LIMBS_SMALL + i) + Column::Relation(N_BLOCKS + 2 * N_LIMBS_SMALL + i) } IVCColumn::Block1InputRepacked150(i) => { assert!(i < 2 * N_LIMBS_XLARGE); - Column::Relation(2 * N_LIMBS_SMALL + 2 * N_LIMBS_LARGE + i) + Column::Relation(N_BLOCKS + 2 * N_LIMBS_SMALL + 2 * N_LIMBS_LARGE + i) } IVCColumn::Block2Hash(poseidon_col) => poseidon_col.to_column(), - IVCColumn::Block3ConstPhi => Column::Relation(0), - IVCColumn::Block3ConstR => Column::Relation(1), - IVCColumn::Block3PhiPow => Column::Relation(2), - IVCColumn::Block3PhiPowR => Column::Relation(3), - IVCColumn::Block3PhiPowR2 => Column::Relation(4), - IVCColumn::Block3PhiPowR3 => Column::Relation(5), + IVCColumn::Block3ConstPhi => Column::Relation(N_BLOCKS), + IVCColumn::Block3ConstR => Column::Relation(N_BLOCKS + 1), + IVCColumn::Block3PhiPow => Column::Relation(N_BLOCKS + 2), + IVCColumn::Block3PhiPowR => Column::Relation(N_BLOCKS + 3), + IVCColumn::Block3PhiPowR2 => Column::Relation(N_BLOCKS + 4), + IVCColumn::Block3PhiPowR3 => Column::Relation(N_BLOCKS + 5), IVCColumn::Block3PhiPowLimbs(i) => { assert!(i < N_LIMBS_SMALL); - Column::Relation(6 + i) + Column::Relation(N_BLOCKS + 6 + i) } IVCColumn::Block3PhiPowRLimbs(i) => { assert!(i < N_LIMBS_SMALL); - Column::Relation(6 + N_LIMBS_SMALL + i) + Column::Relation(N_BLOCKS + 6 + N_LIMBS_SMALL + i) } IVCColumn::Block3PhiPowR2Limbs(i) => { assert!(i < N_LIMBS_SMALL); - Column::Relation(6 + 2 * N_LIMBS_SMALL + i) + Column::Relation(N_BLOCKS + 6 + 2 * N_LIMBS_SMALL + i) } IVCColumn::Block3PhiPowR3Limbs(i) => { assert!(i < N_LIMBS_SMALL); - Column::Relation(6 + 3 * N_LIMBS_SMALL + i) + Column::Relation(N_BLOCKS + 6 + 3 * N_LIMBS_SMALL + i) } IVCColumn::Block4Input1(i) => { assert!(i < 2 * N_LIMBS_LARGE); - Column::Relation(i) + Column::Relation(N_BLOCKS + i) } - IVCColumn::Block4Coeff => Column::Relation(8), - IVCColumn::Block4Input2AccessTime => Column::Relation(9), + IVCColumn::Block4Coeff => Column::Relation(N_BLOCKS + 8), + IVCColumn::Block4Input2AccessTime => Column::Relation(N_BLOCKS + 9), IVCColumn::Block4Input2(i) => { assert!(i < 2 * N_LIMBS_LARGE); - Column::Relation(10 + i) + Column::Relation(N_BLOCKS + 10 + i) + } + IVCColumn::Block4ECAddInter(fec_inter) => { + fec_inter.to_column().add_rel_offset(N_BLOCKS + 18) } - IVCColumn::Block4ECAddInter(fec_inter) => fec_inter.to_column().add_rel_offset(18), IVCColumn::Block4OutputRaw(fec_output) => fec_output .to_column() - .add_rel_offset(18 + FECColumnInter::N_COL), + .add_rel_offset(N_BLOCKS + 18 + FECColumnInter::N_COL), IVCColumn::Block4OutputAccessTime => { - Column::Relation(18 + FECColumnInter::N_COL + FECColumnOutput::N_COL) + Column::Relation(N_BLOCKS + 18 + FECColumnInter::N_COL + FECColumnOutput::N_COL) } IVCColumn::Block4OutputRepacked(i) => { assert!(i < 2 * N_LIMBS_LARGE); - Column::Relation(18 + FECColumnInter::N_COL + FECColumnOutput::N_COL + 1 + i) + Column::Relation( + N_BLOCKS + 18 + FECColumnInter::N_COL + FECColumnOutput::N_COL + 1 + i, + ) } - IVCColumn::Block5ConstHr => Column::Relation(0), - IVCColumn::Block5ConstR => Column::Relation(1), - IVCColumn::Block5ChalLeft => Column::Relation(2), - IVCColumn::Block5ChalRight => Column::Relation(3), - IVCColumn::Block5ChalOutput => Column::Relation(4), + IVCColumn::Block5ConstHr => Column::Relation(N_BLOCKS), + IVCColumn::Block5ConstR => Column::Relation(N_BLOCKS + 1), + IVCColumn::Block5ChalLeft => Column::Relation(N_BLOCKS + 2), + IVCColumn::Block5ChalRight => Column::Relation(N_BLOCKS + 3), + IVCColumn::Block5ChalOutput => Column::Relation(N_BLOCKS + 4), - IVCColumn::Block6ConstR => Column::Relation(0), - IVCColumn::Block6ULeft => Column::Relation(1), - IVCColumn::Block6UOutput => Column::Relation(2), + IVCColumn::Block6ConstR => Column::Relation(N_BLOCKS), + IVCColumn::Block6ULeft => Column::Relation(N_BLOCKS + 1), + IVCColumn::Block6UOutput => Column::Relation(N_BLOCKS + 2), } } } From 4b6821b08d3557e0fdb9336244a32f3aaf413601 Mon Sep 17 00:00:00 2001 From: Mikhail Volkhov Date: Thu, 16 May 2024 16:20:37 +0100 Subject: [PATCH 2/9] [#2231] Implement simple set_assert_mapper --- ivc/src/ivc/columns.rs | 6 ++-- ivc/src/ivc/interpreter.rs | 40 +++++++++++++++++++++++++- msm/src/circuit_design/capabilities.rs | 5 ++++ msm/src/circuit_design/composition.rs | 12 ++++++++ msm/src/circuit_design/constraints.rs | 22 +++++++------- msm/src/circuit_design/witness.rs | 10 ++++++- 6 files changed, 80 insertions(+), 15 deletions(-) diff --git a/ivc/src/ivc/columns.rs b/ivc/src/ivc/columns.rs index e675ecfc1e..415c814b44 100644 --- a/ivc/src/ivc/columns.rs +++ b/ivc/src/ivc/columns.rs @@ -6,6 +6,9 @@ use kimchi_msm::{ serialization::interpreter::{N_LIMBS_LARGE, N_LIMBS_SMALL}, }; +/// Number of blocks in the circuit. +pub const N_BLOCKS: usize = 6; + pub const IVC_POSEIDON_STATE_SIZE: usize = 3; pub const IVC_POSEIDON_NB_FULL_ROUND: usize = 55; @@ -286,9 +289,6 @@ pub enum IVCColumn { Block6UOutput, } -/// Number of blocks in the circuit. -const N_BLOCKS: usize = 6; - impl ColumnIndexer for IVCColumn { // This should be // const N_COL: usize = std::cmp::max(IVCPoseidonColumn::N_COL, FECColumn::N_COL); diff --git a/ivc/src/ivc/interpreter.rs b/ivc/src/ivc/interpreter.rs index b993e397fe..5da353329c 100644 --- a/ivc/src/ivc/interpreter.rs +++ b/ivc/src/ivc/interpreter.rs @@ -3,7 +3,8 @@ use crate::{ ivc::{ columns::{ - IVCColumn, IVCFECLens, IVCHashLens, IVC_POSEIDON_NB_FULL_ROUND, IVC_POSEIDON_STATE_SIZE, + IVCColumn, IVCFECLens, IVCHashLens, IVC_POSEIDON_NB_FULL_ROUND, + IVC_POSEIDON_STATE_SIZE, N_BLOCKS, }, lookups::{IVCFECLookupLens, IVCLookupTable}, }, @@ -913,6 +914,43 @@ where { } +/// This function generates constraitns for the whole IVC circuit. +pub fn constrain_selectors(env: &mut Env) +where + F: PrimeField, + Env: ColAccessCap, +{ + for i in 0..N_BLOCKS { + // Each selector must have value either 0 or 1. + let sel = env.read_column(IVCColumn::BlockSel(i)); + env.assert_zero(sel.clone() * (sel.clone() - Env::constant(F::from(1u64)))); + } +} + +/// This function generates constraitns for the whole IVC circuit. +pub fn constrain_ivc(env: &mut Env) +where + F: PrimeField, + Ff: PrimeField, + Env: ColAccessCap + LookupCap>, +{ + constrain_selectors(env); + + env.set_assert_mapper(env.read_column(IVCColumn::BlockSel(0))); + constrain_inputs(env); + // TODO hashes + env.set_assert_mapper(env.read_column(IVCColumn::BlockSel(2))); + constrain_ecadds(env); + env.set_assert_mapper(env.read_column(IVCColumn::BlockSel(3))); + constrain_scalars(env); + env.set_assert_mapper(env.read_column(IVCColumn::BlockSel(4))); + constrain_challenges(env); + env.set_assert_mapper(env.read_column(IVCColumn::BlockSel(5))); + constrain_u(env); + + env.set_assert_mapper(Env::constant(F::one())); +} + /// Instantiates the IVC circuit for folding. L is relaxed (folded) /// instance, and R is strict (new) instance that is being relaxed at /// this step. `N_COL_TOTAL` is the total number of columnsfor IVC + APP. diff --git a/msm/src/circuit_design/capabilities.rs b/msm/src/circuit_design/capabilities.rs index 0fe144178b..07487bd8b3 100644 --- a/msm/src/circuit_design/capabilities.rs +++ b/msm/src/circuit_design/capabilities.rs @@ -22,6 +22,11 @@ pub trait ColAccessCap { /// Asserts that the value is zero. fn assert_zero(&mut self, cst: Self::Variable); + // TODO we need mapper: Box Self::Variable> + /// Sets an assert predicate `f(X)` such that when assert_zero is + /// called on x, it will actually perform `assert_zero(f(x))`. + fn set_assert_mapper(&mut self, mapper: Self::Variable); + /// Reads value from a column position. fn read_column(&self, col: CIx) -> Self::Variable; diff --git a/msm/src/circuit_design/composition.rs b/msm/src/circuit_design/composition.rs index 1e8ab9a353..c586b98f51 100644 --- a/msm/src/circuit_design/composition.rs +++ b/msm/src/circuit_design/composition.rs @@ -183,6 +183,10 @@ impl< self.env.assert_zero(cst); } + fn set_assert_mapper(&mut self, mapper: Self::Variable) { + self.env.set_assert_mapper(mapper); + } + fn constant(value: F) -> Self::Variable { Env1::constant(value) } @@ -235,6 +239,10 @@ impl< self.0.assert_zero(cst); } + fn set_assert_mapper(&mut self, mapper: Self::Variable) { + self.0.set_assert_mapper(mapper); + } + fn constant(value: F) -> Self::Variable { Env1::constant(value) } @@ -281,6 +289,10 @@ impl<'a, F: PrimeField, CIx1: ColumnIndexer, Env1: ColAccessCap, L> Col self.0.env.assert_zero(cst); } + fn set_assert_mapper(&mut self, mapper: Self::Variable) { + self.0.env.set_assert_mapper(mapper); + } + fn constant(value: F) -> Self::Variable { Env1::constant(value) } diff --git a/msm/src/circuit_design/constraints.rs b/msm/src/circuit_design/constraints.rs index 4a29b3155c..f792d6d1b5 100644 --- a/msm/src/circuit_design/constraints.rs +++ b/msm/src/circuit_design/constraints.rs @@ -17,17 +17,20 @@ pub struct ConstraintBuilderEnv { /// The index can be used to differentiate the constraints used by different /// calls to the interpreter function, and let the callers ordered them for /// folding for instance. - pub constraints: Vec<(usize, Expr, Column>)>, - pub constrain_index: usize, + pub constraints: Vec, Column>>, pub lookups: BTreeMap, LT>>>, + pub assert_mapper: E, } impl ConstraintBuilderEnv { pub fn create() -> Self { + let const_one = Expr::Atom(ExprInner::Constant(ConstantExpr::from( + ConstantTerm::Literal(F::one()), + ))); Self { constraints: vec![], - constrain_index: 0, lookups: BTreeMap::new(), + assert_mapper: const_one, } } } @@ -40,9 +43,11 @@ impl ColAccessCap fn assert_zero(&mut self, cst: Self::Variable) { // FIXME: We should enforce that we add the same expression // Maybe we could have a digest of the expression - let index = self.constrain_index; - self.constraints.push((index, cst)); - self.constrain_index += 1; + self.constraints.push(self.assert_mapper.clone() * cst); + } + + fn set_assert_mapper(&mut self, mapper: Self::Variable) { + self.assert_mapper = mapper; } fn read_column(&self, position: CIx) -> Self::Variable { @@ -91,10 +96,7 @@ impl LookupCap impl ConstraintBuilderEnv { /// Get constraints related to the application logic itself. pub fn get_relation_constraints(&self) -> Vec> { - self.constraints - .iter() - .map(|(_, cst)| cst.clone()) - .collect() + self.constraints.clone() } /// Get constraints related to the lookup argument. diff --git a/msm/src/circuit_design/witness.rs b/msm/src/circuit_design/witness.rs index 2f28a8d6d3..ff9bc170c3 100644 --- a/msm/src/circuit_design/witness.rs +++ b/msm/src/circuit_design/witness.rs @@ -43,6 +43,9 @@ pub struct WitnessBuilderEnv< /// value for row #j of the selector #i. pub fixed_selectors: Vec>, + /// Function used to map assertions. + pub assert_mapper: F, + // A Phantom Data for CIx -- right now WitnessBUilderEnv does not // depend on CIx, but in the future (with associated generics // enabled?) it might be convenient to put all the `NT_COL` (and @@ -67,7 +70,11 @@ impl< type Variable = F; fn assert_zero(&mut self, cst: Self::Variable) { - assert_eq!(cst, F::zero()); + assert_eq!(self.assert_mapper * cst, F::zero()); + } + + fn set_assert_mapper(&mut self, mapper: Self::Variable) { + self.assert_mapper = mapper; } fn constant(value: F) -> Self::Variable { @@ -301,6 +308,7 @@ impl< lookups: vec![lookups_row], fixed_selectors, phantom_cix: PhantomData, + assert_mapper: F::one(), } } From 30c9950a4aad71c7d7d1ab8cc93af22377c4450d Mon Sep 17 00:00:00 2001 From: Mikhail Volkhov Date: Thu, 16 May 2024 16:29:17 +0100 Subject: [PATCH 3/9] [#2231] Add write_sel for block functions --- ivc/src/ivc/interpreter.rs | 39 +++++++++++++++++++++++++++++++++++++- 1 file changed, 38 insertions(+), 1 deletion(-) diff --git a/ivc/src/ivc/interpreter.rs b/ivc/src/ivc/interpreter.rs index 5da353329c..b9c8c8e4c7 100644 --- a/ivc/src/ivc/interpreter.rs +++ b/ivc/src/ivc/interpreter.rs @@ -914,6 +914,43 @@ where { } +/// Builds selectors for the IVC circuit. +pub fn build_selectors( + domain_size: usize, +) -> [Vec; N_BLOCKS] +where + F: PrimeField, +{ + let mut selectors: [Vec; N_BLOCKS] = std::array::from_fn(|_| vec![F::zero(); domain_size]); + let mut cur_row = 0; + for _i in 0..3 * N_COL_TOTAL { + selectors[0][cur_row] = F::one(); + cur_row += 1; + } + for _i in 0..6 * N_COL_TOTAL + 2 { + selectors[1][cur_row] = F::one(); + cur_row += 1; + } + for _i in 0..N_COL_TOTAL + 1 { + selectors[2][cur_row] = F::one(); + cur_row += 1; + } + for _i in 0..(35 * N_COL_TOTAL + 5) { + selectors[3][cur_row] = F::one(); + cur_row += 1; + } + for _i in 0..CHAL_LEN { + selectors[4][cur_row] = F::one(); + cur_row += 1; + } + for _i in 0..1 { + selectors[5][cur_row] = F::one(); + cur_row += 1; + } + + selectors +} + /// This function generates constraitns for the whole IVC circuit. pub fn constrain_selectors(env: &mut Env) where @@ -938,7 +975,7 @@ where env.set_assert_mapper(env.read_column(IVCColumn::BlockSel(0))); constrain_inputs(env); - // TODO hashes + // TODO FIXME add constraints for hashes env.set_assert_mapper(env.read_column(IVCColumn::BlockSel(2))); constrain_ecadds(env); env.set_assert_mapper(env.read_column(IVCColumn::BlockSel(3))); From ca75363647ee828fb5345b5d1f74a6023991b305 Mon Sep 17 00:00:00 2001 From: Mikhail Volkhov Date: Thu, 16 May 2024 17:01:57 +0100 Subject: [PATCH 4/9] [#2231] Add completeness test w/ selectors --- ivc/src/ivc/interpreter.rs | 4 +- ivc/src/ivc/lookups.rs | 9 +++ ivc/src/ivc/mod.rs | 94 +++++++++++++++++++++++++++++-- msm/src/circuit_design/witness.rs | 8 ++- msm/src/test/test_circuit/mod.rs | 2 +- 5 files changed, 107 insertions(+), 10 deletions(-) diff --git a/ivc/src/ivc/interpreter.rs b/ivc/src/ivc/interpreter.rs index b9c8c8e4c7..8f8e235fdf 100644 --- a/ivc/src/ivc/interpreter.rs +++ b/ivc/src/ivc/interpreter.rs @@ -915,7 +915,7 @@ where } /// Builds selectors for the IVC circuit. -pub fn build_selectors( +pub fn build_selectors( domain_size: usize, ) -> [Vec; N_BLOCKS] where @@ -939,7 +939,7 @@ where selectors[3][cur_row] = F::one(); cur_row += 1; } - for _i in 0..CHAL_LEN { + for _i in 0..N_CHALS { selectors[4][cur_row] = F::one(); cur_row += 1; } diff --git a/ivc/src/ivc/lookups.rs b/ivc/src/ivc/lookups.rs index b798a29615..5a9fdd7e7b 100644 --- a/ivc/src/ivc/lookups.rs +++ b/ivc/src/ivc/lookups.rs @@ -52,6 +52,15 @@ impl LookupTableID for IVCLookupTable { } } +impl IVCLookupTable { + /// Provides a full list of entries for the given table. + pub fn entries(&self, domain_d1_size: u64) -> Vec { + match self { + Self::SerLookupTable(lt) => lt.entries(domain_d1_size), + } + } +} + pub struct IVCFECLookupLens(pub PhantomData); impl MPrism for IVCFECLookupLens { diff --git a/ivc/src/ivc/mod.rs b/ivc/src/ivc/mod.rs index c837cdc98f..891fd8ee1f 100644 --- a/ivc/src/ivc/mod.rs +++ b/ivc/src/ivc/mod.rs @@ -7,18 +7,32 @@ mod tests { use crate::{ ivc::{ - columns::{IVCColumn, IVC_POSEIDON_NB_FULL_ROUND, IVC_POSEIDON_STATE_SIZE}, - interpreter::ivc_circuit, + columns::{IVCColumn, IVC_POSEIDON_NB_FULL_ROUND, IVC_POSEIDON_STATE_SIZE, N_BLOCKS}, + interpreter::{build_selectors, constrain_ivc, ivc_circuit}, lookups::IVCLookupTable, }, poseidon::{interpreter::PoseidonParams, params::static_params}, }; use ark_ff::{UniformRand, Zero}; - use kimchi_msm::{circuit_design::WitnessBuilderEnv, columns::ColumnIndexer, Ff1, Fp}; + use kimchi::circuits::domains::EvaluationDomains; + use kimchi_msm::{ + circuit_design::{ConstraintBuilderEnv, WitnessBuilderEnv}, + columns::ColumnIndexer, + logup::LookupTableID, + precomputed_srs::get_bn254_srs, + prover::prove, + verifier::verify, + witness::Witness, + BaseSponge, Ff1, Fp, OpeningProof, ScalarSponge, BN254, + }; + use poly_commitment::pairing_proof::PairingSRS; use rand::{CryptoRng, RngCore}; + use std::collections::BTreeMap; // Test number - pub const TEST_N_COL_TOTAL: usize = 50; + pub const TEST_N_COL_TOTAL: usize = 2 * IVCColumn::N_COL; + // Absolutely no idea. + pub const TEST_N_CHALS: usize = 200; pub const TEST_DOMAIN_SIZE: usize = 1 << 15; #[derive(Clone)] @@ -48,7 +62,10 @@ mod tests { } } - fn build_ivc_circuit(rng: &mut RNG) -> IVCWitnessBuilderEnv { + fn build_ivc_circuit( + rng: &mut RNG, + domain_size: usize, + ) -> IVCWitnessBuilderEnv { let mut witness_env = IVCWitnessBuilderEnv::create(); // To support less rows than domain_size we need to have selectors. @@ -73,6 +90,10 @@ mod tests { ) }); + let fixed_selectors: [Vec; N_BLOCKS] = + build_selectors::<_, TEST_N_COL_TOTAL, TEST_N_CHALS>(domain_size); + witness_env.set_fixed_selectors(fixed_selectors.to_vec()); + // TODO add nonzero E/T values. ivc_circuit::<_, _, _, _, TEST_N_COL_TOTAL>( &mut witness_env, @@ -94,6 +115,67 @@ mod tests { /// Tests if building the IVC circuit succeeds. pub fn test_ivc_circuit() { let mut rng = o1_utils::tests::make_test_rng(); - build_ivc_circuit(&mut rng); + build_ivc_circuit(&mut rng, 1 << 8); + } + + #[test] + fn test_completeness_ivc() { + let mut rng = o1_utils::tests::make_test_rng(); + + let domain_size = 1 << 15; + let domain = EvaluationDomains::::create(domain_size).unwrap(); + + let srs: PairingSRS = get_bn254_srs(domain); + + let mut lookup_tables_data = BTreeMap::new(); + for table_id in IVCLookupTable::::all_variants().into_iter() { + lookup_tables_data.insert(table_id, table_id.entries(domain.d1.size)); + } + let witness_env = build_ivc_circuit::<_>(&mut rng, domain_size); + let mut proof_inputs = witness_env.get_proof_inputs(domain, lookup_tables_data); + // Don't use lookups for now + proof_inputs.logups = vec![]; + + let mut constraint_env = ConstraintBuilderEnv::>::create(); + constrain_ivc::(&mut constraint_env); + // Don't use lookups for now + let constraints = constraint_env.get_relation_constraints(); + + // generate the proof + let proof = prove::< + _, + OpeningProof, + BaseSponge, + ScalarSponge, + _, + { IVCColumn::N_COL }, + { IVCColumn::N_COL - N_BLOCKS }, + 0, + N_BLOCKS, + IVCLookupTable, + >(domain, &srs, &constraints, proof_inputs, &mut rng) + .unwrap(); + + // verify the proof + let verifies = verify::< + _, + OpeningProof, + BaseSponge, + ScalarSponge, + { IVCColumn::N_COL }, + { IVCColumn::N_COL - N_BLOCKS }, + 0, + N_BLOCKS, + 0, + IVCLookupTable, + >( + domain, + &srs, + &constraints, + &proof, + Witness::zero_vec(domain_size), + ); + + assert!(verifies); } } diff --git a/msm/src/circuit_design/witness.rs b/msm/src/circuit_design/witness.rs index ff9bc170c3..3b74852beb 100644 --- a/msm/src/circuit_design/witness.rs +++ b/msm/src/circuit_design/witness.rs @@ -314,7 +314,7 @@ impl< /// Sets a fixed selector, the vector of length equal to the /// domain size (circuit height). - pub fn set_fixed_selector(&mut self, sel: CIx, sel_values: Vec) { + pub fn set_fixed_selector_cix(&mut self, sel: CIx, sel_values: Vec) { if let Column::FixedSelector(i) = sel.to_column() { self.fixed_selectors[i] = sel_values; } else { @@ -322,6 +322,12 @@ impl< } } + /// Sets all fixed selectors directly. Each item in `selectors` is + /// a vector of `domain_size` length. + pub fn set_fixed_selectors(&mut self, selectors: Vec>) { + self.fixed_selectors = selectors + } + /// Generates proof inputs, repacking/collecting internal witness builder state. pub fn get_proof_inputs( &self, diff --git a/msm/src/test/test_circuit/mod.rs b/msm/src/test/test_circuit/mod.rs index d7a274e388..2b30b79a0a 100644 --- a/msm/src/test/test_circuit/mod.rs +++ b/msm/src/test/test_circuit/mod.rs @@ -45,7 +45,7 @@ mod tests { fixed_sel.push(Fp::from(i as u64)); } - witness_env.set_fixed_selector(TestColumn::FixedE, fixed_sel); + witness_env.set_fixed_selector_cix(TestColumn::FixedE, fixed_sel); for row_i in 0..domain_size { let a: Fp = ::rand(rng); From 1847b26cb6efb4ef84b149700b41a1a4c9498965 Mon Sep 17 00:00:00 2001 From: Mikhail Volkhov Date: Fri, 17 May 2024 13:08:05 +0100 Subject: [PATCH 5/9] [#2231] Make IVC interpreter work in completeness test --- ivc/src/ivc/columns.rs | 7 ++- ivc/src/ivc/interpreter.rs | 61 +++++++++++++------------ ivc/src/ivc/mod.rs | 65 +++++++++++++++++---------- msm/src/circuit_design/composition.rs | 59 +++++++++++++++++++++++- msm/src/circuit_design/witness.rs | 33 ++++++++++---- 5 files changed, 160 insertions(+), 65 deletions(-) diff --git a/ivc/src/ivc/columns.rs b/ivc/src/ivc/columns.rs index 415c814b44..e8987ebe84 100644 --- a/ivc/src/ivc/columns.rs +++ b/ivc/src/ivc/columns.rs @@ -293,7 +293,8 @@ impl ColumnIndexer for IVCColumn { // This should be // const N_COL: usize = std::cmp::max(IVCPoseidonColumn::N_COL, FECColumn::N_COL); // which is runtime-only expression..? - const N_COL: usize = IVCPoseidonColumn::N_COL; + // 333 is not enough + const N_COL: usize = 400; fn to_column(self) -> Column { match self { @@ -315,7 +316,9 @@ impl ColumnIndexer for IVCColumn { Column::Relation(N_BLOCKS + 2 * N_LIMBS_SMALL + 2 * N_LIMBS_LARGE + i) } - IVCColumn::Block2Hash(poseidon_col) => poseidon_col.to_column(), + IVCColumn::Block2Hash(poseidon_col) => { + poseidon_col.to_column().add_rel_offset(N_BLOCKS) + } IVCColumn::Block3ConstPhi => Column::Relation(N_BLOCKS), IVCColumn::Block3ConstR => Column::Relation(N_BLOCKS + 1), diff --git a/ivc/src/ivc/interpreter.rs b/ivc/src/ivc/interpreter.rs index 8f8e235fdf..c6b66ab397 100644 --- a/ivc/src/ivc/interpreter.rs +++ b/ivc/src/ivc/interpreter.rs @@ -185,7 +185,7 @@ where pub fn write_inputs_row( env: &mut Env, - target_comms: [(Ff, Ff); N_COL_TOTAL], + target_comms: &[(Ff, Ff); N_COL_TOTAL], row_num_local: usize, ) -> (Vec, Vec, Vec) where @@ -246,11 +246,11 @@ where #[allow(clippy::type_complexity)] pub fn process_inputs( env: &mut Env, - comms: [[(Ff, Ff); N_COL_TOTAL]; 3], + comms: [Box<[(Ff, Ff); N_COL_TOTAL]>; 3], ) -> ( - [[[F; 2 * N_LIMBS_SMALL]; N_COL_TOTAL]; 3], - [[[F; 2 * N_LIMBS_LARGE]; N_COL_TOTAL]; 3], - [[[F; 2 * N_LIMBS_XLARGE]; N_COL_TOTAL]; 3], + Box<[[[F; 2 * N_LIMBS_SMALL]; N_COL_TOTAL]; 3]>, + Box<[[[F; 2 * N_LIMBS_LARGE]; N_COL_TOTAL]; 3]>, + Box<[[[F; 2 * N_LIMBS_XLARGE]; N_COL_TOTAL]; 3]>, ) where F: PrimeField, @@ -264,11 +264,11 @@ where let row_num = env.curr_row(); let (target_comms, row_num_local, comtype) = if row_num < N_COL_TOTAL { - (comms[0], row_num, 0) + (&comms[0], row_num, 0) } else if row_num < 2 * N_COL_TOTAL { - (comms[1], row_num - N_COL_TOTAL, 1) + (&comms[1], row_num - N_COL_TOTAL, 1) } else { - (comms[2], row_num - 2 * N_COL_TOTAL, 2) + (&comms[2], row_num - 2 * N_COL_TOTAL, 2) }; let (limbs_small, limbs_large, limbs_xlarge) = @@ -287,20 +287,22 @@ where // Left-Right-Output for a given limb size. fn repack_output( input: [Vec>; 3], - ) -> [[[F; TWO_LIMB_SIZE]; N_COL_TOTAL]; 3] { - input - .into_iter() - .map(|vector: Vec>| { - vector - .into_iter() - .map(|subvec: Vec<_>| subvec.try_into().unwrap()) - .collect::>() - .try_into() - .unwrap() - }) - .collect::>() - .try_into() - .unwrap() + ) -> Box<[[[F; TWO_LIMB_SIZE]; N_COL_TOTAL]; 3]> { + Box::new( + input + .into_iter() + .map(|vector: Vec>| { + vector + .into_iter() + .map(|subvec: Vec<_>| subvec.try_into().unwrap()) + .collect::>() + .try_into() + .unwrap() + }) + .collect::>() + .try_into() + .unwrap(), + ) } ( @@ -917,14 +919,17 @@ where /// Builds selectors for the IVC circuit. pub fn build_selectors( domain_size: usize, -) -> [Vec; N_BLOCKS] +) -> Vec> where F: PrimeField, { - let mut selectors: [Vec; N_BLOCKS] = std::array::from_fn(|_| vec![F::zero(); domain_size]); + // 3*N + 6*N+2 + N+1 + 35*N + 5 + 1 + N_CHALS = + // 45N + 9 + N_CHALS + let mut selectors: Vec> = vec![vec![F::zero(); domain_size]; N_BLOCKS]; let mut cur_row = 0; for _i in 0..3 * N_COL_TOTAL { - selectors[0][cur_row] = F::one(); + //selectors[0][cur_row] = F::one(); + selectors[0][cur_row] = F::from(2u32); cur_row += 1; } for _i in 0..6 * N_COL_TOTAL + 2 { @@ -994,9 +999,9 @@ where #[allow(clippy::too_many_arguments)] pub fn ivc_circuit( env: &mut Env, - comms_left: [(Ff, Ff); N_COL_TOTAL], - comms_right: [(Ff, Ff); N_COL_TOTAL], - comms_out: [(Ff, Ff); N_COL_TOTAL], + comms_left: Box<[(Ff, Ff); N_COL_TOTAL]>, + comms_right: Box<[(Ff, Ff); N_COL_TOTAL]>, + comms_out: Box<[(Ff, Ff); N_COL_TOTAL]>, error_terms: [(Ff, Ff); 3], // E_L, E_R, E_O t_terms: [(Ff, Ff); 2], // T_0, T_1 u_l: F, // part of the relaxed instance. diff --git a/ivc/src/ivc/mod.rs b/ivc/src/ivc/mod.rs index 891fd8ee1f..e15730f2c5 100644 --- a/ivc/src/ivc/mod.rs +++ b/ivc/src/ivc/mod.rs @@ -16,10 +16,14 @@ mod tests { use ark_ff::{UniformRand, Zero}; use kimchi::circuits::domains::EvaluationDomains; use kimchi_msm::{ - circuit_design::{ConstraintBuilderEnv, WitnessBuilderEnv}, + circuit_design::{ + composition::{IdMPrism, MPrism}, + ConstraintBuilderEnv, SubEnvLookup, WitnessBuilderEnv, + }, columns::ColumnIndexer, logup::LookupTableID, precomputed_srs::get_bn254_srs, + proof::ProofInputs, prover::prove, verifier::verify, witness::Witness, @@ -27,10 +31,9 @@ mod tests { }; use poly_commitment::pairing_proof::PairingSRS; use rand::{CryptoRng, RngCore}; - use std::collections::BTreeMap; // Test number - pub const TEST_N_COL_TOTAL: usize = 2 * IVCColumn::N_COL; + pub const TEST_N_COL_TOTAL: usize = IVCColumn::N_COL + 50; // Absolutely no idea. pub const TEST_N_CHALS: usize = 200; pub const TEST_DOMAIN_SIZE: usize = 1 << 15; @@ -38,15 +41,17 @@ mod tests { #[derive(Clone)] pub struct PoseidonBN254Parameters; - type IVCWitnessBuilderEnv = WitnessBuilderEnv< + type IVCWitnessBuilderEnvRaw = WitnessBuilderEnv< Fp, IVCColumn, { ::N_COL }, { ::N_COL }, 0, 0, - IVCLookupTable, + LT, >; + //type IVCWitnessBuilderEnv = IVCWitnessBuilderEnvRaw>; + //type IVCWitnessBuilderEnvDummy = IVCWitnessBuilderEnvRaw; impl PoseidonParams for PoseidonBN254Parameters @@ -62,41 +67,46 @@ mod tests { } } - fn build_ivc_circuit( + fn build_ivc_circuit< + RNG: RngCore + CryptoRng, + LT: LookupTableID, + L: MPrism>, + >( rng: &mut RNG, domain_size: usize, - ) -> IVCWitnessBuilderEnv { - let mut witness_env = IVCWitnessBuilderEnv::create(); + lt_lens: L, + ) -> IVCWitnessBuilderEnvRaw { + let mut witness_env = IVCWitnessBuilderEnvRaw::::create(); // To support less rows than domain_size we need to have selectors. //let row_num = rng.gen_range(0..domain_size); - let comms_left: [_; TEST_N_COL_TOTAL] = core::array::from_fn(|_i| { + let comms_left: Box<[_; TEST_N_COL_TOTAL]> = Box::new(core::array::from_fn(|_i| { ( ::rand(rng), ::rand(rng), ) - }); - let comms_right: [_; TEST_N_COL_TOTAL] = core::array::from_fn(|_i| { + })); + let comms_right: Box<[_; TEST_N_COL_TOTAL]> = Box::new(core::array::from_fn(|_i| { ( ::rand(rng), ::rand(rng), ) - }); - let comms_output: [_; TEST_N_COL_TOTAL] = core::array::from_fn(|_i| { + })); + let comms_output: Box<[_; TEST_N_COL_TOTAL]> = Box::new(core::array::from_fn(|_i| { ( ::rand(rng), ::rand(rng), ) - }); + })); - let fixed_selectors: [Vec; N_BLOCKS] = + let fixed_selectors: Vec> = build_selectors::<_, TEST_N_COL_TOTAL, TEST_N_CHALS>(domain_size); witness_env.set_fixed_selectors(fixed_selectors.to_vec()); // TODO add nonzero E/T values. ivc_circuit::<_, _, _, _, TEST_N_COL_TOTAL>( - &mut witness_env, + &mut SubEnvLookup::new(&mut witness_env, lt_lens), comms_left, comms_right, comms_output, @@ -115,7 +125,11 @@ mod tests { /// Tests if building the IVC circuit succeeds. pub fn test_ivc_circuit() { let mut rng = o1_utils::tests::make_test_rng(); - build_ivc_circuit(&mut rng, 1 << 8); + build_ivc_circuit::<_, IVCLookupTable, _>( + &mut rng, + 1 << 8, + IdMPrism::>::default(), + ); } #[test] @@ -127,14 +141,17 @@ mod tests { let srs: PairingSRS = get_bn254_srs(domain); - let mut lookup_tables_data = BTreeMap::new(); - for table_id in IVCLookupTable::::all_variants().into_iter() { - lookup_tables_data.insert(table_id, table_id.entries(domain.d1.size)); - } - let witness_env = build_ivc_circuit::<_>(&mut rng, domain_size); - let mut proof_inputs = witness_env.get_proof_inputs(domain, lookup_tables_data); + let witness_env = build_ivc_circuit::<_, IVCLookupTable, _>( + &mut rng, + domain_size, + IdMPrism::>::default(), + ); // Don't use lookups for now - proof_inputs.logups = vec![]; + let rel_witness = witness_env.get_relation_witness(domain); + let proof_inputs = ProofInputs { + evaluations: rel_witness, + logups: vec![], + }; let mut constraint_env = ConstraintBuilderEnv::>::create(); constrain_ivc::(&mut constraint_env); diff --git a/msm/src/circuit_design/composition.rs b/msm/src/circuit_design/composition.rs index c586b98f51..c19fea7616 100644 --- a/msm/src/circuit_design/composition.rs +++ b/msm/src/circuit_design/composition.rs @@ -47,11 +47,14 @@ /// /// Similar "mapping" intuition applies to lookup tables. use crate::{ - circuit_design::capabilities::{ColAccessCap, ColWriteCap, HybridCopyCap, LookupCap}, + circuit_design::capabilities::{ + ColAccessCap, ColWriteCap, DirectWitnessCap, HybridCopyCap, LookupCap, MultiRowReadCap, + }, columns::ColumnIndexer, logup::LookupTableID, }; use ark_ff::PrimeField; +use std::marker::PhantomData; /// `MPrism` allows one to Something like a Prism, but for Maybe and not just any Applicative. /// @@ -70,6 +73,29 @@ pub trait MPrism { fn re_get(&self, target: Self::Target) -> Self::Source; } +/// Identity `MPrism` from any type `T` to itself. +#[derive(Clone, Copy, Debug)] +pub struct IdMPrism(pub PhantomData); + +impl Default for IdMPrism { + fn default() -> Self { + IdMPrism(PhantomData) + } +} + +impl MPrism for IdMPrism { + type Source = T; + type Target = T; + + fn traverse(&self, source: Self::Source) -> Option { + Some(source) + } + + fn re_get(&self, target: Self::Target) -> Self::Source { + target + } +} + pub struct ComposedMPrism { /// The left-hand side of the composition. lhs: LHS, @@ -123,7 +149,7 @@ where struct SubEnv<'a, F: PrimeField, CIx1: ColumnIndexer, Env1: ColAccessCap, L> { env: &'a mut Env1, lens: L, - phantom: core::marker::PhantomData<(F, CIx1)>, + phantom: PhantomData<(F, CIx1)>, } /// Sub environment with a lens that is mapping columns. @@ -347,3 +373,32 @@ impl< self.0.env.lookup(lookup_id, value) } } + +impl<'a, F: PrimeField, CIx: ColumnIndexer, Env1: MultiRowReadCap, L> + MultiRowReadCap for SubEnvLookup<'a, F, CIx, Env1, L> +{ + /// Read value from a (row,column) position. + fn read_row_column(&mut self, row: usize, col: CIx) -> Self::Variable { + self.0.env.read_row_column(row, col) + } + + /// Progresses to the next row. + fn next_row(&mut self) { + self.0.env.next_row(); + } + + /// Returns the current row. + fn curr_row(&self) -> usize { + self.0.env.curr_row() + } +} + +impl<'a, F: PrimeField, CIx: ColumnIndexer, Env1: DirectWitnessCap, L> + DirectWitnessCap for SubEnvLookup<'a, F, CIx, Env1, L> +{ + fn variable_to_field(value: Self::Variable) -> F { + Env1::variable_to_field(value) + } +} + +// TODO add traits for SubEnvColumn diff --git a/msm/src/circuit_design/witness.rs b/msm/src/circuit_design/witness.rs index 3b74852beb..dd6fb419de 100644 --- a/msm/src/circuit_design/witness.rs +++ b/msm/src/circuit_design/witness.rs @@ -328,13 +328,9 @@ impl< self.fixed_selectors = selectors } - /// Generates proof inputs, repacking/collecting internal witness builder state. - pub fn get_proof_inputs( - &self, - domain: EvaluationDomains, - lookup_tables_data: BTreeMap>, - ) -> ProofInputs { + pub fn get_relation_witness(&self, domain: EvaluationDomains) -> Witness> { let domain_size: usize = domain.d1.size as usize; + // Boxing to avoid stack overflow let mut witness: Box>> = Box::new(Witness { cols: Box::new(std::array::from_fn(|_| Vec::with_capacity(domain_size))), @@ -366,6 +362,15 @@ impl< witness.cols[N_REL + N_DSEL + i] = self.fixed_selectors[i].clone(); } + *witness + } + + pub fn get_logup_witness( + &self, + domain: EvaluationDomains, + lookup_tables_data: BTreeMap>, + ) -> Vec> { + let domain_size: usize = domain.d1.size as usize; // Building lookup values let mut lookup_tables: BTreeMap>>> = BTreeMap::new(); if !lookup_tables_data.is_empty() { @@ -412,7 +417,7 @@ impl< *(table.last_mut().unwrap()) = lookup_t.collect(); } - let logups: Vec> = lookup_tables + lookup_tables .iter() .filter_map(|(table_id, table)| { // Only add a table if it's used. Otherwise lookups fail. @@ -426,10 +431,20 @@ impl< None } }) - .collect(); + .collect() + } + + /// Generates proof inputs, repacking/collecting internal witness builder state. + pub fn get_proof_inputs( + &self, + domain: EvaluationDomains, + lookup_tables_data: BTreeMap>, + ) -> ProofInputs { + let evaluations = self.get_relation_witness(domain); + let logups = self.get_logup_witness(domain, lookup_tables_data); ProofInputs { - evaluations: *witness, + evaluations, logups, } } From d8cca45cc1444cc58948fed5bef29e2ea0f394a4 Mon Sep 17 00:00:00 2001 From: Mikhail Volkhov Date: Fri, 17 May 2024 17:25:57 +0100 Subject: [PATCH 6/9] [#2231] Generalise set_assert_mapper properly --- ivc/src/ivc/interpreter.rs | 25 +++++++++++++++++-------- ivc/src/ivc/mod.rs | 2 +- msm/src/circuit_design/capabilities.rs | 9 ++++++--- msm/src/circuit_design/composition.rs | 6 +++--- msm/src/circuit_design/constraints.rs | 11 ++++------- msm/src/circuit_design/witness.rs | 8 ++++---- 6 files changed, 35 insertions(+), 26 deletions(-) diff --git a/ivc/src/ivc/interpreter.rs b/ivc/src/ivc/interpreter.rs index c6b66ab397..899bbb55c2 100644 --- a/ivc/src/ivc/interpreter.rs +++ b/ivc/src/ivc/interpreter.rs @@ -928,8 +928,7 @@ where let mut selectors: Vec> = vec![vec![F::zero(); domain_size]; N_BLOCKS]; let mut cur_row = 0; for _i in 0..3 * N_COL_TOTAL { - //selectors[0][cur_row] = F::one(); - selectors[0][cur_row] = F::from(2u32); + selectors[0][cur_row] = F::one(); cur_row += 1; } for _i in 0..6 * N_COL_TOTAL + 2 { @@ -978,19 +977,29 @@ where { constrain_selectors(env); - env.set_assert_mapper(env.read_column(IVCColumn::BlockSel(0))); + let s0 = env.read_column(IVCColumn::BlockSel(0)); + env.set_assert_mapper(Box::new(move |x| s0.clone() * x)); constrain_inputs(env); + // TODO FIXME add constraints for hashes - env.set_assert_mapper(env.read_column(IVCColumn::BlockSel(2))); + + let s2 = env.read_column(IVCColumn::BlockSel(2)); + env.set_assert_mapper(Box::new(move |x| s2.clone() * x)); constrain_ecadds(env); - env.set_assert_mapper(env.read_column(IVCColumn::BlockSel(3))); + + let s3 = env.read_column(IVCColumn::BlockSel(3)); + env.set_assert_mapper(Box::new(move |x| s3.clone() * x)); constrain_scalars(env); - env.set_assert_mapper(env.read_column(IVCColumn::BlockSel(4))); + + let s4 = env.read_column(IVCColumn::BlockSel(4)); + env.set_assert_mapper(Box::new(move |x| s4.clone() * x)); constrain_challenges(env); - env.set_assert_mapper(env.read_column(IVCColumn::BlockSel(5))); + + let s5 = env.read_column(IVCColumn::BlockSel(5)); + env.set_assert_mapper(Box::new(move |x| s5.clone() * x)); constrain_u(env); - env.set_assert_mapper(Env::constant(F::one())); + env.set_assert_mapper(Box::new(move |x| x)); } /// Instantiates the IVC circuit for folding. L is relaxed (folded) diff --git a/ivc/src/ivc/mod.rs b/ivc/src/ivc/mod.rs index e15730f2c5..2776e04e73 100644 --- a/ivc/src/ivc/mod.rs +++ b/ivc/src/ivc/mod.rs @@ -127,7 +127,7 @@ mod tests { let mut rng = o1_utils::tests::make_test_rng(); build_ivc_circuit::<_, IVCLookupTable, _>( &mut rng, - 1 << 8, + 1 << 15, IdMPrism::>::default(), ); } diff --git a/msm/src/circuit_design/capabilities.rs b/msm/src/circuit_design/capabilities.rs index 07487bd8b3..c691f78bea 100644 --- a/msm/src/circuit_design/capabilities.rs +++ b/msm/src/circuit_design/capabilities.rs @@ -11,21 +11,24 @@ use ark_ff::PrimeField; /// Environment capability for accessing and reading columns. This is necessary for /// building constraints. pub trait ColAccessCap { + // NB: 'static here means that `Variable` does not contain any + // references witha a lifetime less than 'static. Which is true in + // our case. Necessary for `set_assert_mapper` type Variable: Clone + std::ops::Add + std::ops::Sub + std::ops::Mul + std::ops::Neg + From - + std::fmt::Debug; + + std::fmt::Debug + + 'static; /// Asserts that the value is zero. fn assert_zero(&mut self, cst: Self::Variable); - // TODO we need mapper: Box Self::Variable> /// Sets an assert predicate `f(X)` such that when assert_zero is /// called on x, it will actually perform `assert_zero(f(x))`. - fn set_assert_mapper(&mut self, mapper: Self::Variable); + fn set_assert_mapper(&mut self, mapper: Box Self::Variable>); /// Reads value from a column position. fn read_column(&self, col: CIx) -> Self::Variable; diff --git a/msm/src/circuit_design/composition.rs b/msm/src/circuit_design/composition.rs index c19fea7616..7bae628082 100644 --- a/msm/src/circuit_design/composition.rs +++ b/msm/src/circuit_design/composition.rs @@ -209,7 +209,7 @@ impl< self.env.assert_zero(cst); } - fn set_assert_mapper(&mut self, mapper: Self::Variable) { + fn set_assert_mapper(&mut self, mapper: Box Self::Variable>) { self.env.set_assert_mapper(mapper); } @@ -265,7 +265,7 @@ impl< self.0.assert_zero(cst); } - fn set_assert_mapper(&mut self, mapper: Self::Variable) { + fn set_assert_mapper(&mut self, mapper: Box Self::Variable>) { self.0.set_assert_mapper(mapper); } @@ -315,7 +315,7 @@ impl<'a, F: PrimeField, CIx1: ColumnIndexer, Env1: ColAccessCap, L> Col self.0.env.assert_zero(cst); } - fn set_assert_mapper(&mut self, mapper: Self::Variable) { + fn set_assert_mapper(&mut self, mapper: Box Self::Variable>) { self.0.env.set_assert_mapper(mapper); } diff --git a/msm/src/circuit_design/constraints.rs b/msm/src/circuit_design/constraints.rs index f792d6d1b5..9be6abc46f 100644 --- a/msm/src/circuit_design/constraints.rs +++ b/msm/src/circuit_design/constraints.rs @@ -19,18 +19,15 @@ pub struct ConstraintBuilderEnv { /// folding for instance. pub constraints: Vec, Column>>, pub lookups: BTreeMap, LT>>>, - pub assert_mapper: E, + pub assert_mapper: Box) -> E>, } impl ConstraintBuilderEnv { pub fn create() -> Self { - let const_one = Expr::Atom(ExprInner::Constant(ConstantExpr::from( - ConstantTerm::Literal(F::one()), - ))); Self { constraints: vec![], lookups: BTreeMap::new(), - assert_mapper: const_one, + assert_mapper: Box::new(|x| x), } } } @@ -43,10 +40,10 @@ impl ColAccessCap fn assert_zero(&mut self, cst: Self::Variable) { // FIXME: We should enforce that we add the same expression // Maybe we could have a digest of the expression - self.constraints.push(self.assert_mapper.clone() * cst); + self.constraints.push((self.assert_mapper)(cst)); } - fn set_assert_mapper(&mut self, mapper: Self::Variable) { + fn set_assert_mapper(&mut self, mapper: Box Self::Variable>) { self.assert_mapper = mapper; } diff --git a/msm/src/circuit_design/witness.rs b/msm/src/circuit_design/witness.rs index dd6fb419de..a53fbcc799 100644 --- a/msm/src/circuit_design/witness.rs +++ b/msm/src/circuit_design/witness.rs @@ -44,7 +44,7 @@ pub struct WitnessBuilderEnv< pub fixed_selectors: Vec>, /// Function used to map assertions. - pub assert_mapper: F, + pub assert_mapper: Box F>, // A Phantom Data for CIx -- right now WitnessBUilderEnv does not // depend on CIx, but in the future (with associated generics @@ -70,10 +70,10 @@ impl< type Variable = F; fn assert_zero(&mut self, cst: Self::Variable) { - assert_eq!(self.assert_mapper * cst, F::zero()); + assert_eq!((self.assert_mapper)(cst), F::zero()); } - fn set_assert_mapper(&mut self, mapper: Self::Variable) { + fn set_assert_mapper(&mut self, mapper: Box Self::Variable>) { self.assert_mapper = mapper; } @@ -308,7 +308,7 @@ impl< lookups: vec![lookups_row], fixed_selectors, phantom_cix: PhantomData, - assert_mapper: F::one(), + assert_mapper: Box::new(|x| x), } } From ed19c0456842a561449cfbe22bcec204a51ffcd2 Mon Sep 17 00:00:00 2001 From: Mikhail Volkhov Date: Tue, 28 May 2024 13:28:53 +0200 Subject: [PATCH 7/9] [#2231] Fix IVC column indexing --- ivc/src/ivc/columns.rs | 69 ++++++++++++++++++++---------------------- 1 file changed, 32 insertions(+), 37 deletions(-) diff --git a/ivc/src/ivc/columns.rs b/ivc/src/ivc/columns.rs index e8987ebe84..962524cf6f 100644 --- a/ivc/src/ivc/columns.rs +++ b/ivc/src/ivc/columns.rs @@ -299,84 +299,79 @@ impl ColumnIndexer for IVCColumn { fn to_column(self) -> Column { match self { IVCColumn::BlockSel(i) => { - assert!(i < 2 * N_BLOCKS); + assert!(i < N_BLOCKS); Column::FixedSelector(i) } IVCColumn::Block1Input(i) => { assert!(i < 2 * N_LIMBS_SMALL); - Column::Relation(N_BLOCKS + i) + Column::Relation(i) } IVCColumn::Block1InputRepacked75(i) => { assert!(i < 2 * N_LIMBS_LARGE); - Column::Relation(N_BLOCKS + 2 * N_LIMBS_SMALL + i) + Column::Relation(2 * N_LIMBS_SMALL + i) } IVCColumn::Block1InputRepacked150(i) => { assert!(i < 2 * N_LIMBS_XLARGE); - Column::Relation(N_BLOCKS + 2 * N_LIMBS_SMALL + 2 * N_LIMBS_LARGE + i) + Column::Relation(2 * N_LIMBS_SMALL + 2 * N_LIMBS_LARGE + i) } - IVCColumn::Block2Hash(poseidon_col) => { - poseidon_col.to_column().add_rel_offset(N_BLOCKS) - } + IVCColumn::Block2Hash(poseidon_col) => poseidon_col.to_column(), - IVCColumn::Block3ConstPhi => Column::Relation(N_BLOCKS), - IVCColumn::Block3ConstR => Column::Relation(N_BLOCKS + 1), - IVCColumn::Block3PhiPow => Column::Relation(N_BLOCKS + 2), - IVCColumn::Block3PhiPowR => Column::Relation(N_BLOCKS + 3), - IVCColumn::Block3PhiPowR2 => Column::Relation(N_BLOCKS + 4), - IVCColumn::Block3PhiPowR3 => Column::Relation(N_BLOCKS + 5), + IVCColumn::Block3ConstPhi => Column::Relation(0), + IVCColumn::Block3ConstR => Column::Relation(1), + IVCColumn::Block3PhiPow => Column::Relation(2), + IVCColumn::Block3PhiPowR => Column::Relation(3), + IVCColumn::Block3PhiPowR2 => Column::Relation(4), + IVCColumn::Block3PhiPowR3 => Column::Relation(5), IVCColumn::Block3PhiPowLimbs(i) => { assert!(i < N_LIMBS_SMALL); - Column::Relation(N_BLOCKS + 6 + i) + Column::Relation(6 + i) } IVCColumn::Block3PhiPowRLimbs(i) => { assert!(i < N_LIMBS_SMALL); - Column::Relation(N_BLOCKS + 6 + N_LIMBS_SMALL + i) + Column::Relation(6 + N_LIMBS_SMALL + i) } IVCColumn::Block3PhiPowR2Limbs(i) => { assert!(i < N_LIMBS_SMALL); - Column::Relation(N_BLOCKS + 6 + 2 * N_LIMBS_SMALL + i) + Column::Relation(6 + 2 * N_LIMBS_SMALL + i) } IVCColumn::Block3PhiPowR3Limbs(i) => { assert!(i < N_LIMBS_SMALL); - Column::Relation(N_BLOCKS + 6 + 3 * N_LIMBS_SMALL + i) + Column::Relation(6 + 3 * N_LIMBS_SMALL + i) } IVCColumn::Block4Input1(i) => { assert!(i < 2 * N_LIMBS_LARGE); - Column::Relation(N_BLOCKS + i) + Column::Relation(i) } - IVCColumn::Block4Coeff => Column::Relation(N_BLOCKS + 8), - IVCColumn::Block4Input2AccessTime => Column::Relation(N_BLOCKS + 9), + IVCColumn::Block4Coeff => Column::Relation(8), + IVCColumn::Block4Input2AccessTime => Column::Relation(9), IVCColumn::Block4Input2(i) => { assert!(i < 2 * N_LIMBS_LARGE); - Column::Relation(N_BLOCKS + 10 + i) - } - IVCColumn::Block4ECAddInter(fec_inter) => { - fec_inter.to_column().add_rel_offset(N_BLOCKS + 18) + Column::Relation(10 + i) } + IVCColumn::Block4ECAddInter(fec_inter) => fec_inter.to_column().add_rel_offset(18), IVCColumn::Block4OutputRaw(fec_output) => fec_output .to_column() - .add_rel_offset(N_BLOCKS + 18 + FECColumnInter::N_COL), + .add_rel_offset(18 + FECColumnInter::N_COL), IVCColumn::Block4OutputAccessTime => { - Column::Relation(N_BLOCKS + 18 + FECColumnInter::N_COL + FECColumnOutput::N_COL) + Column::Relation(18 + FECColumnInter::N_COL + FECColumnOutput::N_COL) } IVCColumn::Block4OutputRepacked(i) => { assert!(i < 2 * N_LIMBS_LARGE); - Column::Relation( - N_BLOCKS + 18 + FECColumnInter::N_COL + FECColumnOutput::N_COL + 1 + i, - ) + Column::Relation(18 + FECColumnInter::N_COL + FECColumnOutput::N_COL + 1 + i) } - IVCColumn::Block5ConstHr => Column::Relation(N_BLOCKS), - IVCColumn::Block5ConstR => Column::Relation(N_BLOCKS + 1), - IVCColumn::Block5ChalLeft => Column::Relation(N_BLOCKS + 2), - IVCColumn::Block5ChalRight => Column::Relation(N_BLOCKS + 3), - IVCColumn::Block5ChalOutput => Column::Relation(N_BLOCKS + 4), - IVCColumn::Block6ConstR => Column::Relation(N_BLOCKS), - IVCColumn::Block6ULeft => Column::Relation(N_BLOCKS + 1), - IVCColumn::Block6UOutput => Column::Relation(N_BLOCKS + 2), + IVCColumn::Block5ConstHr => Column::Relation(0), + IVCColumn::Block5ConstR => Column::Relation(1), + IVCColumn::Block5ChalLeft => Column::Relation(2), + IVCColumn::Block5ChalRight => Column::Relation(3), + IVCColumn::Block5ChalOutput => Column::Relation(4), + + IVCColumn::Block6ConstR => Column::Relation(0), + IVCColumn::Block6ULeft => Column::Relation(1), + IVCColumn::Block6UOutput => Column::Relation(2), } } } From 2dd268ff6ad08ffd33c9005cf0ed9f62a2897b49 Mon Sep 17 00:00:00 2001 From: Mikhail Volkhov Date: Tue, 28 May 2024 13:30:02 +0200 Subject: [PATCH 8/9] [#2231] Rename cur into curr --- ivc/src/ivc/interpreter.rs | 104 +++++++++++++++++++------------------ 1 file changed, 54 insertions(+), 50 deletions(-) diff --git a/ivc/src/ivc/interpreter.rs b/ivc/src/ivc/interpreter.rs index 899bbb55c2..3691ef4165 100644 --- a/ivc/src/ivc/interpreter.rs +++ b/ivc/src/ivc/interpreter.rs @@ -466,55 +466,59 @@ where F: PrimeField, Env: ColWriteCap, { - let phi_cur_power_f = phi_prev_power_f * phi_f; - let phi_cur_power_r_f = phi_prev_power_f * phi_f * r_f; - let phi_cur_power_r2_f = phi_prev_power_f * phi_f * r_f * r_f; - let phi_cur_power_r3_f = phi_prev_power_f * phi_f * r_f * r_f * r_f; + let phi_curr_power_f = phi_prev_power_f * phi_f; + let phi_curr_power_r_f = phi_prev_power_f * phi_f * r_f; + let phi_curr_power_r2_f = phi_prev_power_f * phi_f * r_f * r_f; + let phi_curr_power_r3_f = phi_prev_power_f * phi_f * r_f * r_f * r_f; env.write_column(IVCColumn::Block3ConstPhi, &Env::constant(phi_f)); env.write_column(IVCColumn::Block3ConstR, &Env::constant(r_f)); - env.write_column(IVCColumn::Block3PhiPow, &Env::constant(phi_cur_power_f)); - env.write_column(IVCColumn::Block3PhiPowR, &Env::constant(phi_cur_power_r_f)); + env.write_column(IVCColumn::Block3PhiPow, &Env::constant(phi_curr_power_f)); + env.write_column(IVCColumn::Block3PhiPowR, &Env::constant(phi_curr_power_r_f)); env.write_column( IVCColumn::Block3PhiPowR2, - &Env::constant(phi_cur_power_r2_f), + &Env::constant(phi_curr_power_r2_f), ); env.write_column( IVCColumn::Block3PhiPowR3, - &Env::constant(phi_cur_power_r3_f), + &Env::constant(phi_curr_power_r3_f), ); // TODO check that limb_decompose_ff works with - let phi_cur_power_f_limbs = - limb_decompose_ff::(&phi_cur_power_f); - write_column_array_const(env, &phi_cur_power_f_limbs, IVCColumn::Block3PhiPowLimbs); + let phi_curr_power_f_limbs = + limb_decompose_ff::(&phi_curr_power_f); + write_column_array_const(env, &phi_curr_power_f_limbs, IVCColumn::Block3PhiPowLimbs); - let phi_cur_power_r_f_limbs = - limb_decompose_ff::(&phi_cur_power_r_f); - write_column_array_const(env, &phi_cur_power_r_f_limbs, IVCColumn::Block3PhiPowRLimbs); + let phi_curr_power_r_f_limbs = + limb_decompose_ff::(&phi_curr_power_r_f); + write_column_array_const( + env, + &phi_curr_power_r_f_limbs, + IVCColumn::Block3PhiPowRLimbs, + ); - let phi_cur_power_r2_f_limbs = - limb_decompose_ff::(&phi_cur_power_r2_f); + let phi_curr_power_r2_f_limbs = + limb_decompose_ff::(&phi_curr_power_r2_f); write_column_array_const( env, - &phi_cur_power_r2_f_limbs, + &phi_curr_power_r2_f_limbs, IVCColumn::Block3PhiPowR2Limbs, ); - let phi_cur_power_r3_f_limbs = - limb_decompose_ff::(&phi_cur_power_r3_f); + let phi_curr_power_r3_f_limbs = + limb_decompose_ff::(&phi_curr_power_r3_f); write_column_array_const( env, - &phi_cur_power_r3_f_limbs, + &phi_curr_power_r3_f_limbs, IVCColumn::Block3PhiPowR3Limbs, ); ( - phi_cur_power_f, - phi_cur_power_f_limbs, - phi_cur_power_r_f_limbs, - phi_cur_power_r2_f_limbs, - phi_cur_power_r3_f_limbs, + phi_curr_power_f, + phi_curr_power_f_limbs, + phi_curr_power_r_f_limbs, + phi_curr_power_r2_f_limbs, + phi_curr_power_r3_f_limbs, ) } @@ -554,19 +558,19 @@ where for block_row_i in 0..N_COL_TOTAL + 1 { let ( phi_prev_power_f_new, - phi_cur_power_f_limbs, - phi_cur_power_r_f_limbs, - phi_cur_power_r2_f_limbs, - phi_cur_power_r3_f_limbs, + phi_curr_power_f_limbs, + phi_curr_power_r_f_limbs, + phi_curr_power_r2_f_limbs, + phi_curr_power_r3_f_limbs, ) = write_scalars_row(env, r, phi, phi_prev_power_f); phi_prev_power_f = phi_prev_power_f_new; - phi_limbs.push(phi_cur_power_f_limbs); - phi_r_limbs.push(phi_cur_power_r_f_limbs); + phi_limbs.push(phi_curr_power_f_limbs); + phi_r_limbs.push(phi_curr_power_r_f_limbs); if block_row_i == N_COL_TOTAL + 1 { - phi_np1_r2_limbs = phi_cur_power_r2_f_limbs; - phi_np1_r3_limbs = phi_cur_power_r3_f_limbs; + phi_np1_r2_limbs = phi_curr_power_r2_f_limbs; + phi_np1_r3_limbs = phi_curr_power_r3_f_limbs; } // Checking our constraints @@ -857,10 +861,10 @@ pub fn process_challenges( { let chal_num = chal_l.len(); - let mut cur_alpha_r_pow: F = F::one(); + let mut curr_alpha_r_pow: F = F::one(); for block_row_i in 0..chal_num { - cur_alpha_r_pow *= h_r; + curr_alpha_r_pow *= h_r; env.write_column(IVCColumn::Block5ConstHr, &Env::constant(h_r)); env.write_column(IVCColumn::Block5ConstR, &Env::constant(r)); @@ -868,10 +872,10 @@ pub fn process_challenges( IVCColumn::Block5ChalLeft, &Env::constant(chal_l[block_row_i]), ); - env.write_column(IVCColumn::Block5ChalRight, &Env::constant(cur_alpha_r_pow)); + env.write_column(IVCColumn::Block5ChalRight, &Env::constant(curr_alpha_r_pow)); env.write_column( IVCColumn::Block5ChalOutput, - &Env::constant(cur_alpha_r_pow * r + chal_l[block_row_i]), + &Env::constant(curr_alpha_r_pow * r + chal_l[block_row_i]), ); constrain_challenges(env); @@ -926,30 +930,30 @@ where // 3*N + 6*N+2 + N+1 + 35*N + 5 + 1 + N_CHALS = // 45N + 9 + N_CHALS let mut selectors: Vec> = vec![vec![F::zero(); domain_size]; N_BLOCKS]; - let mut cur_row = 0; + let mut curr_row = 0; for _i in 0..3 * N_COL_TOTAL { - selectors[0][cur_row] = F::one(); - cur_row += 1; + selectors[0][curr_row] = F::one(); + curr_row += 1; } for _i in 0..6 * N_COL_TOTAL + 2 { - selectors[1][cur_row] = F::one(); - cur_row += 1; + selectors[1][curr_row] = F::one(); + curr_row += 1; } for _i in 0..N_COL_TOTAL + 1 { - selectors[2][cur_row] = F::one(); - cur_row += 1; + selectors[2][curr_row] = F::one(); + curr_row += 1; } for _i in 0..(35 * N_COL_TOTAL + 5) { - selectors[3][cur_row] = F::one(); - cur_row += 1; + selectors[3][curr_row] = F::one(); + curr_row += 1; } for _i in 0..N_CHALS { - selectors[4][cur_row] = F::one(); - cur_row += 1; + selectors[4][curr_row] = F::one(); + curr_row += 1; } for _i in 0..1 { - selectors[5][cur_row] = F::one(); - cur_row += 1; + selectors[5][curr_row] = F::one(); + curr_row += 1; } selectors From 58e35d5f6bb51dd10cc9b7e1137931ea4a5a7b3a Mon Sep 17 00:00:00 2001 From: Mikhail Volkhov Date: Tue, 28 May 2024 13:40:20 +0200 Subject: [PATCH 9/9] [#2231] Cosmetics --- ivc/src/ivc/interpreter.rs | 2 +- msm/src/circuit_design/capabilities.rs | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/ivc/src/ivc/interpreter.rs b/ivc/src/ivc/interpreter.rs index 3691ef4165..7df8eca10d 100644 --- a/ivc/src/ivc/interpreter.rs +++ b/ivc/src/ivc/interpreter.rs @@ -968,7 +968,7 @@ where for i in 0..N_BLOCKS { // Each selector must have value either 0 or 1. let sel = env.read_column(IVCColumn::BlockSel(i)); - env.assert_zero(sel.clone() * (sel.clone() - Env::constant(F::from(1u64)))); + env.assert_zero(sel.clone() * (sel.clone() - Env::constant(F::one()))); } } diff --git a/msm/src/circuit_design/capabilities.rs b/msm/src/circuit_design/capabilities.rs index c691f78bea..0e97cd87e2 100644 --- a/msm/src/circuit_design/capabilities.rs +++ b/msm/src/circuit_design/capabilities.rs @@ -12,7 +12,7 @@ use ark_ff::PrimeField; /// building constraints. pub trait ColAccessCap { // NB: 'static here means that `Variable` does not contain any - // references witha a lifetime less than 'static. Which is true in + // references with a lifetime less than 'static. Which is true in // our case. Necessary for `set_assert_mapper` type Variable: Clone + std::ops::Add