From c2b4bfbde553151737c7788f0797bf804dd05188 Mon Sep 17 00:00:00 2001 From: Morgan Thomas Date: Fri, 5 Apr 2024 19:13:56 -0400 Subject: [PATCH 01/23] wip: static data chip: using a preprocessed trace --- static_data/src/columns.rs | 25 +++++++++++++++++++------ static_data/src/lib.rs | 26 ++++++++------------------ static_data/src/stark.rs | 38 +++++++++++++++++++++----------------- 3 files changed, 48 insertions(+), 41 deletions(-) diff --git a/static_data/src/columns.rs b/static_data/src/columns.rs index 8c7e519..5ff965e 100644 --- a/static_data/src/columns.rs +++ b/static_data/src/columns.rs @@ -4,8 +4,21 @@ use valida_derive::AlignedBorrow; use valida_machine::Word; use valida_util::indices_arr; -#[derive(AlignedBorrow, Default)] pub struct StaticDataCols { + // Not used for anything, just present because of the assumption that each chip has a column in its trace + pub dummy: T, +} + +pub const NUM_STATIC_DATA_COLS: usize = size_of::>(); +pub const STATIC_DATA_COL_MAP: StaticDataCols = make_col_map(); + +const fn make_col_map() -> StaticDataCols { + let indices_arr = indices_arr::(); + unsafe { transmute::<[usize; NUM_STATIC_DATA_COLS], StaticDataCols>(indices_arr) } +} + +#[derive(AlignedBorrow, Default)] +pub struct StaticDataPreprocessedCols { /// Memory address pub addr: T, @@ -16,10 +29,10 @@ pub struct StaticDataCols { pub is_real: T, } -pub const NUM_STATIC_DATA_COLS: usize = size_of::>(); -pub const STATIC_DATA_COL_MAP: StaticDataCols = make_col_map(); +pub const NUM_STATIC_DATA_PREPROCESSED_COLS: usize = size_of::>(); +pub const STATIC_DATA_PREPROCESSED_COL_MAP: StaticDataPreprocessedCols = make_preprocessed_col_map(); -const fn make_col_map() -> StaticDataCols { - let indices_arr = indices_arr::(); - unsafe { transmute::<[usize; NUM_STATIC_DATA_COLS], StaticDataCols>(indices_arr) } +const fn make_preprocessed_col_map() -> StaticDataPreprocessedCols { + let indices_arr = indices_arr::(); + unsafe { transmute::<[usize; NUM_STATIC_DATA_PREPROCESSED_COLS], StaticDataPreprocessedCols>(indices_arr) } } diff --git a/static_data/src/lib.rs b/static_data/src/lib.rs index 81eb39c..dc17577 100644 --- a/static_data/src/lib.rs +++ b/static_data/src/lib.rs @@ -2,7 +2,7 @@ extern crate alloc; -use crate::columns::{NUM_STATIC_DATA_COLS, STATIC_DATA_COL_MAP}; +use crate::columns::{NUM_STATIC_DATA_COLS, NUM_STATIC_DATA_PREPROCESSED_COLS, STATIC_DATA_PREPROCESSED_COL_MAP}; use alloc::collections::BTreeMap; use alloc::vec; use alloc::vec::Vec; @@ -10,8 +10,8 @@ use p3_air::VirtualPairCol; use p3_field::{AbstractField, Field}; use p3_matrix::dense::RowMajorMatrix; use valida_bus::MachineWithMemBus; -use valida_machine::{BusArgument, Chip, Interaction, Machine, StarkConfig, Word}; -use valida_memory::{MachineWithMemoryChip, MemoryChip}; +use valida_machine::{Chip, Interaction, StarkConfig, Word}; +use valida_memory::{MachineWithMemoryChip}; pub mod columns; pub mod stark; @@ -52,25 +52,15 @@ where M: MachineWithMemBus, SC: StarkConfig, { - fn generate_trace(&self, machine: &M) -> RowMajorMatrix { - let mut rows = self.cells.iter() - .map(|(addr, value)| { - let mut row: Vec = vec![SC::Val::from_canonical_u32(*addr)]; - row.extend(value.0.into_iter().map(SC::Val::from_canonical_u8).collect::>()); - row - }) - .flatten() - .collect::>(); - rows.resize(rows.len().next_power_of_two() * NUM_STATIC_DATA_COLS, SC::Val::zero()); - RowMajorMatrix::new(rows, NUM_STATIC_DATA_COLS) + fn generate_trace(&self, _machine: &M) -> RowMajorMatrix { + RowMajorMatrix::new(vec![SC::Val::zero(); self.cells.len().next_power_of_two()], NUM_STATIC_DATA_COLS) } fn global_sends(&self, machine: &M) -> Vec> { - // return vec![]; // TODO - let addr = VirtualPairCol::single_main(STATIC_DATA_COL_MAP.addr); - let value = STATIC_DATA_COL_MAP.value.0.map(VirtualPairCol::single_main); + let addr = VirtualPairCol::single_preprocessed(STATIC_DATA_PREPROCESSED_COL_MAP.addr); + let value = STATIC_DATA_PREPROCESSED_COL_MAP.value.0.map(VirtualPairCol::single_preprocessed); let is_read = VirtualPairCol::constant(SC::Val::zero()); - let is_real = VirtualPairCol::single_main(STATIC_DATA_COL_MAP.is_real); + let is_real = VirtualPairCol::single_preprocessed(STATIC_DATA_PREPROCESSED_COL_MAP.is_real); let is_static_initial = VirtualPairCol::constant(SC::Val::one()); let clk = VirtualPairCol::constant(SC::Val::zero()); let mut fields = vec![is_read, clk, addr, is_static_initial]; diff --git a/static_data/src/stark.rs b/static_data/src/stark.rs index 05cdd1f..bca6b4a 100644 --- a/static_data/src/stark.rs +++ b/static_data/src/stark.rs @@ -1,35 +1,39 @@ -use crate::columns::{StaticDataCols, NUM_STATIC_DATA_COLS}; +use crate::columns::{StaticDataPreprocessedCols, NUM_STATIC_DATA_PREPROCESSED_COLS, NUM_STATIC_DATA_COLS}; use crate::StaticDataChip; +use alloc::vec::Vec; +use alloc::vec; use core::borrow::Borrow; use p3_air::{Air, AirBuilder, BaseAir}; use p3_field::AbstractField; use p3_matrix::MatrixRowSlices; +use p3_matrix::dense::RowMajorMatrix; -impl BaseAir for StaticDataChip { +impl BaseAir for StaticDataChip { fn width(&self) -> usize { NUM_STATIC_DATA_COLS } + + fn preprocessed_trace(&self) -> Option> { + let mut rows = self.cells.iter() + .map(|(addr, value)| { + let mut row: Vec = vec![F::from_canonical_u32(*addr)]; + row.extend(value.0.into_iter().map(F::from_canonical_u8).collect::>()); + row.push(F::one()); + row + }) + .flatten() + .collect::>(); + rows.resize(rows.len().next_power_of_two() * NUM_STATIC_DATA_PREPROCESSED_COLS, F::zero()); + Some(RowMajorMatrix::new(rows, NUM_STATIC_DATA_PREPROCESSED_COLS)) + } } impl Air for StaticDataChip where AB: AirBuilder, { - fn eval(&self, builder: &mut AB) { - self.eval_main(builder); - } -} - -impl StaticDataChip { - fn eval_main(&self, builder: &mut AB) { - // ensure that addresses are sequentially increasing, in order to ensure internal consistency of static data trace - let main = builder.main(); - let local: &StaticDataCols = main.row_slice(0).borrow(); - let next: &StaticDataCols = main.row_slice(1).borrow(); - builder - .when_transition() - .when(local.is_real * next.is_real) - .assert_eq(next.addr, local.addr + AB::Expr::one()); + fn eval(&self, _builder: &mut AB) { + // Nothing to do here } } From 1d9ecf91dd53b3e73770dcff0ff9e77367ba410d Mon Sep 17 00:00:00 2001 From: Morgan Thomas Date: Sat, 6 Apr 2024 13:36:05 -0400 Subject: [PATCH 02/23] wip: preprocessed traces --- cpu/src/lib.rs | 1 - derive/src/lib.rs | 17 +- machine/src/chip.rs | 1 - machine/src/proof.rs | 2 +- machine/src/symbolic/symbolic_builder.rs | 1 - memory/src/lib.rs | 254 +++++++++++------------ static_data/src/lib.rs | 3 +- static_data/src/stark.rs | 4 +- 8 files changed, 137 insertions(+), 146 deletions(-) diff --git a/cpu/src/lib.rs b/cpu/src/lib.rs index cbbcd89..c18cbdc 100644 --- a/cpu/src/lib.rs +++ b/cpu/src/lib.rs @@ -7,7 +7,6 @@ use alloc::format; use alloc::vec; use alloc::vec::Vec; use core::iter; -use core::marker::Sync; use core::mem::transmute; use valida_bus::{MachineWithGeneralBus, MachineWithMemBus, MachineWithProgramBus}; use valida_machine::{ diff --git a/derive/src/lib.rs b/derive/src/lib.rs index ba8dc38..d707f34 100644 --- a/derive/src/lib.rs +++ b/derive/src/lib.rs @@ -368,8 +368,7 @@ fn prove_method(chips: &[&Field]) -> TokenStream2 { let zeta_exp_quotient_degree: [Vec; #num_chips] = log_quotient_degrees.map(|log_deg| vec![zeta.exp_power_of_2(log_deg)]); let prover_data_and_points = [ - // TODO: Causes some errors, probably related to the fact that not all chips have preprocessed traces? - // (&preprocessed_data, zeta_and_next.as_slice()), + (&preprocessed_data, zeta_and_next.as_slice()), (&main_data, zeta_and_next.as_slice()), (&perm_data, zeta_and_next.as_slice()), ("ient_data, zeta_exp_quotient_degree.as_slice()), @@ -377,28 +376,26 @@ fn prove_method(chips: &[&Field]) -> TokenStream2 { let (openings, opening_proof) = pcs.open_multi_batches( &prover_data_and_points, &mut challenger); - // TODO: add preprocessed openings - let [main_openings, perm_openings, quotient_openings] = - openings.try_into().expect("Should have 3 rounds of openings"); + let [preprocessed_openings, main_openings, perm_openings, quotient_openings] = + openings.try_into().expect("Should have 4 rounds of openings"); let commitments = Commitments { + preprocessed_trace: preprocessed_commit, main_trace: main_commit, perm_trace: perm_commit, quotient_chunks: quotient_commit, }; - - // TODO: add preprocessed openings let chip_proofs = log_degrees .iter() + .zip(preprocessed_openings) .zip(main_openings) .zip(perm_openings) .zip(quotient_openings) .zip(perm_traces) - .map(|((((log_degree, main), perm), quotient), perm_trace)| { - // TODO: add preprocessed openings + .map(|(((((log_degree, preprocessed), main), perm), quotient), perm_trace)| { let [preprocessed_local, preprocessed_next] = - [vec![], vec![]]; + preprocessed.try_into().expect("Should have 2 openings"); let [main_local, main_next] = main.try_into().expect("Should have 2 openings"); let [perm_local, perm_next] = perm.try_into().expect("Should have 2 openings"); diff --git a/machine/src/chip.rs b/machine/src/chip.rs index afd6e09..8c97e8f 100644 --- a/machine/src/chip.rs +++ b/machine/src/chip.rs @@ -2,7 +2,6 @@ use crate::folding_builder::VerifierConstraintFolder; use crate::Machine; use crate::__internal::{DebugConstraintBuilder, ProverConstraintFolder}; use alloc::vec; -use alloc::vec::Vec; use crate::config::StarkConfig; use crate::symbolic::symbolic_builder::SymbolicAirBuilder; diff --git a/machine/src/proof.rs b/machine/src/proof.rs index db8ec34..8b3b064 100644 --- a/machine/src/proof.rs +++ b/machine/src/proof.rs @@ -1,5 +1,4 @@ use crate::config::StarkConfig; -use alloc::vec::Vec; use p3_commit::Pcs; use p3_matrix::dense::RowMajorMatrix; use serde::de::DeserializeOwned; @@ -20,6 +19,7 @@ pub struct MachineProof { #[derive(Serialize, Deserialize)] pub struct Commitments { + pub preprocessed_trace: Com, pub main_trace: Com, pub perm_trace: Com, pub quotient_chunks: Com, diff --git a/machine/src/symbolic/symbolic_builder.rs b/machine/src/symbolic/symbolic_builder.rs index da9c374..f9333d4 100644 --- a/machine/src/symbolic/symbolic_builder.rs +++ b/machine/src/symbolic/symbolic_builder.rs @@ -1,5 +1,4 @@ use alloc::vec; -use alloc::vec::Vec; use crate::config::StarkConfig; use crate::{Machine, ValidaAirBuilder}; diff --git a/memory/src/lib.rs b/memory/src/lib.rs index d10e2b1..492029b 100644 --- a/memory/src/lib.rs +++ b/memory/src/lib.rs @@ -14,7 +14,7 @@ use p3_maybe_rayon::prelude::*; use valida_bus::MachineWithMemBus; use valida_machine::StarkConfig; use valida_machine::{Chip, Interaction, Machine, Word}; -use valida_util::batch_multiplicative_inverse_allowing_zero; +// use valida_util::batch_multiplicative_inverse_allowing_zero; pub mod columns; pub mod stark; @@ -249,130 +249,130 @@ impl MemoryChip { row } - fn insert_dummy_reads(ops: &mut Vec<(u32, Operation)>) { - if ops.is_empty() { - return; - } - - let table_len = ops.len() as u32; - let mut dummy_ops = Vec::new(); - for (op1, op2) in ops.iter().zip(ops.iter().skip(1)) { - let addr_diff = op2.1.get_address() - op1.1.get_address(); - if addr_diff != 0 { - // Add dummy reads when addr_diff is greater than the number of operations - if addr_diff > table_len { - let num_dummy_ops = addr_diff / table_len; - for i in 0..num_dummy_ops { - let dummy_op_clk = op1.0; - let dummy_op_addr = op1.1.get_address() + table_len * (i + 1); - let dummy_op_value = op1.1.get_value(); - dummy_ops.push(( - dummy_op_clk, - Operation::DummyRead(dummy_op_addr, dummy_op_value), - )); - } - } else { - continue; - } - } else { - let clk_diff = op2.0 - op1.0; - if clk_diff > table_len { - let num_dummy_ops = clk_diff / table_len; - for j in 0..num_dummy_ops { - let dummy_op_clk = op1.0 + table_len * (j + 1); - let dummy_op_addr = op1.1.get_address(); - let dummy_op_value = op1.1.get_value(); - dummy_ops.push(( - dummy_op_clk, - Operation::DummyRead(dummy_op_addr, dummy_op_value), - )); - } - } - } - } - - // TODO: Track number of operations at a given address instead of recounting here - for (clk, dummy_op) in dummy_ops.iter() { - let idx_addr = ops.binary_search_by_key(&dummy_op.get_address(), |(_, dummy_op)| { - dummy_op.get_address() - }); - if let Ok(idx_addr) = idx_addr { - ops.insert(idx_addr, (*clk, dummy_op.clone())); - let num_ops = ops[idx_addr..] - .iter() - .take_while(|(_, op2)| dummy_op.get_address() == op2.get_address()) - .count(); - let idx_clk = - ops[idx_addr..(idx_addr + num_ops)].partition_point(|(clk2, _)| clk2 < clk); - ops.insert(idx_addr + idx_clk, (*clk, *dummy_op)); - } else if let Err(idx_addr) = idx_addr { - ops.insert(idx_addr, (*clk, dummy_op.clone())); - } - } - - // Pad the end of the table with dummy reads (to the next power of two) - let num_dummy_ops = ops.len().next_power_of_two() - ops.len(); - let dummy_op_clk = ops.last().unwrap().0; - let dummy_op_addr = ops.last().unwrap().1.get_address(); - let dummy_op_value = ops.last().unwrap().1.get_value(); - for _ in 0..num_dummy_ops { - ops.push(( - dummy_op_clk, - Operation::DummyRead(dummy_op_addr, dummy_op_value), - )); - } - - // Resort (TODO: this shouldn't be necessary if `insert_dummy_reads` is - // implemented correctly...) - ops.sort_by_key(|(clk, op)| (op.get_address(), *clk)); - } - - fn compute_address_diffs( - &self, - ops: Vec<(u32, Operation)>, - rows: &mut Vec<[F; NUM_MEM_COLS]>, - ) { - if ops.is_empty() { - return; - } - - let i0 = self.static_data.len(); - - // Compute `diff` and `counter_mult` - let mut diff = vec![F::zero(); rows.len()]; - let mut mult = vec![F::zero(); rows.len()]; - for i in 0..(ops.len() - 1) { - let addr = ops[i].1.get_address(); - let addr_next = ops[i + 1].1.get_address(); - let value = if addr_next != addr { - addr_next - addr - } else { - let clk = ops[i].0; - let clk_next = ops[i + 1].0; - clk_next - clk - }; - diff[i] = F::from_canonical_u32(value); - mult[value as usize] += F::one(); - } - - // Compute `diff_inv` - let diff_inv = batch_multiplicative_inverse_allowing_zero(diff.clone()); - - // Set trace values - for i in 0..(ops.len() - 1) { - rows[i0 + i][MEM_COL_MAP.diff] = diff[i]; - rows[i0 + i][MEM_COL_MAP.diff_inv] = diff_inv[i]; - rows[i0 + i][MEM_COL_MAP.counter_mult] = mult[i]; - - let addr = ops[i].1.get_address(); - let addr_next = ops[i + 1].1.get_address(); - if addr_next - addr != 0 { - rows[i0 + i][MEM_COL_MAP.addr_not_equal] = F::one(); - } - } - - // The first row should have a zero-valued diff, which is "sent" to the local - // range check bus. We need to account for that value on the receiving end here. - rows[0][MEM_COL_MAP.counter_mult] += F::one(); - } + // fn insert_dummy_reads(ops: &mut Vec<(u32, Operation)>) { + // if ops.is_empty() { + // return; + // } + + // let table_len = ops.len() as u32; + // let mut dummy_ops = Vec::new(); + // for (op1, op2) in ops.iter().zip(ops.iter().skip(1)) { + // let addr_diff = op2.1.get_address() - op1.1.get_address(); + // if addr_diff != 0 { + // // Add dummy reads when addr_diff is greater than the number of operations + // if addr_diff > table_len { + // let num_dummy_ops = addr_diff / table_len; + // for i in 0..num_dummy_ops { + // let dummy_op_clk = op1.0; + // let dummy_op_addr = op1.1.get_address() + table_len * (i + 1); + // let dummy_op_value = op1.1.get_value(); + // dummy_ops.push(( + // dummy_op_clk, + // Operation::DummyRead(dummy_op_addr, dummy_op_value), + // )); + // } + // } else { + // continue; + // } + // } else { + // let clk_diff = op2.0 - op1.0; + // if clk_diff > table_len { + // let num_dummy_ops = clk_diff / table_len; + // for j in 0..num_dummy_ops { + // let dummy_op_clk = op1.0 + table_len * (j + 1); + // let dummy_op_addr = op1.1.get_address(); + // let dummy_op_value = op1.1.get_value(); + // dummy_ops.push(( + // dummy_op_clk, + // Operation::DummyRead(dummy_op_addr, dummy_op_value), + // )); + // } + // } + // } + // } + + // // TODO: Track number of operations at a given address instead of recounting here + // for (clk, dummy_op) in dummy_ops.iter() { + // let idx_addr = ops.binary_search_by_key(&dummy_op.get_address(), |(_, dummy_op)| { + // dummy_op.get_address() + // }); + // if let Ok(idx_addr) = idx_addr { + // ops.insert(idx_addr, (*clk, dummy_op.clone())); + // let num_ops = ops[idx_addr..] + // .iter() + // .take_while(|(_, op2)| dummy_op.get_address() == op2.get_address()) + // .count(); + // let idx_clk = + // ops[idx_addr..(idx_addr + num_ops)].partition_point(|(clk2, _)| clk2 < clk); + // ops.insert(idx_addr + idx_clk, (*clk, *dummy_op)); + // } else if let Err(idx_addr) = idx_addr { + // ops.insert(idx_addr, (*clk, dummy_op.clone())); + // } + // } + + // // Pad the end of the table with dummy reads (to the next power of two) + // let num_dummy_ops = ops.len().next_power_of_two() - ops.len(); + // let dummy_op_clk = ops.last().unwrap().0; + // let dummy_op_addr = ops.last().unwrap().1.get_address(); + // let dummy_op_value = ops.last().unwrap().1.get_value(); + // for _ in 0..num_dummy_ops { + // ops.push(( + // dummy_op_clk, + // Operation::DummyRead(dummy_op_addr, dummy_op_value), + // )); + // } + + // // Resort (TODO: this shouldn't be necessary if `insert_dummy_reads` is + // // implemented correctly...) + // ops.sort_by_key(|(clk, op)| (op.get_address(), *clk)); + // } + + // fn compute_address_diffs( + // &self, + // ops: Vec<(u32, Operation)>, + // rows: &mut Vec<[F; NUM_MEM_COLS]>, + // ) { + // if ops.is_empty() { + // return; + // } + + // let i0 = self.static_data.len(); + + // // Compute `diff` and `counter_mult` + // let mut diff = vec![F::zero(); rows.len()]; + // let mut mult = vec![F::zero(); rows.len()]; + // for i in 0..(ops.len() - 1) { + // let addr = ops[i].1.get_address(); + // let addr_next = ops[i + 1].1.get_address(); + // let value = if addr_next != addr { + // addr_next - addr + // } else { + // let clk = ops[i].0; + // let clk_next = ops[i + 1].0; + // clk_next - clk + // }; + // diff[i] = F::from_canonical_u32(value); + // mult[value as usize] += F::one(); + // } + + // // Compute `diff_inv` + // let diff_inv = batch_multiplicative_inverse_allowing_zero(diff.clone()); + + // // Set trace values + // for i in 0..(ops.len() - 1) { + // rows[i0 + i][MEM_COL_MAP.diff] = diff[i]; + // rows[i0 + i][MEM_COL_MAP.diff_inv] = diff_inv[i]; + // rows[i0 + i][MEM_COL_MAP.counter_mult] = mult[i]; + + // let addr = ops[i].1.get_address(); + // let addr_next = ops[i + 1].1.get_address(); + // if addr_next - addr != 0 { + // rows[i0 + i][MEM_COL_MAP.addr_not_equal] = F::one(); + // } + // } + + // // The first row should have a zero-valued diff, which is "sent" to the local + // // range check bus. We need to account for that value on the receiving end here. + // rows[0][MEM_COL_MAP.counter_mult] += F::one(); + // } } diff --git a/static_data/src/lib.rs b/static_data/src/lib.rs index 9494923..b0be9a3 100644 --- a/static_data/src/lib.rs +++ b/static_data/src/lib.rs @@ -2,11 +2,10 @@ extern crate alloc; -use crate::columns::{NUM_STATIC_DATA_COLS, NUM_STATIC_DATA_PREPROCESSED_COLS, STATIC_DATA_PREPROCESSED_COL_MAP}; +use crate::columns::{NUM_STATIC_DATA_COLS, STATIC_DATA_PREPROCESSED_COL_MAP}; use alloc::collections::BTreeMap; use alloc::vec; use alloc::vec::Vec; -use core::mem::transmute; use p3_air::VirtualPairCol; use p3_field::{AbstractField, Field}; use p3_matrix::dense::RowMajorMatrix; diff --git a/static_data/src/stark.rs b/static_data/src/stark.rs index bca6b4a..759f66d 100644 --- a/static_data/src/stark.rs +++ b/static_data/src/stark.rs @@ -1,12 +1,10 @@ -use crate::columns::{StaticDataPreprocessedCols, NUM_STATIC_DATA_PREPROCESSED_COLS, NUM_STATIC_DATA_COLS}; +use crate::columns::{NUM_STATIC_DATA_PREPROCESSED_COLS, NUM_STATIC_DATA_COLS}; use crate::StaticDataChip; use alloc::vec::Vec; use alloc::vec; -use core::borrow::Borrow; use p3_air::{Air, AirBuilder, BaseAir}; use p3_field::AbstractField; -use p3_matrix::MatrixRowSlices; use p3_matrix::dense::RowMajorMatrix; impl BaseAir for StaticDataChip { From f9f6bacda38a4516365dd7f295a6c710c851980d Mon Sep 17 00:00:00 2001 From: Morgan Thomas Date: Sat, 6 Apr 2024 14:42:28 -0400 Subject: [PATCH 03/23] issue/143: duplicate basic crate --- Cargo.lock | 42 +++ Cargo.toml | 1 + basic_macro/Cargo.toml | 63 ++++ basic_macro/src/bin/test_prover.rs | 263 +++++++++++++ basic_macro/src/bin/valida.rs | 157 ++++++++ basic_macro/src/lib.rs | 352 ++++++++++++++++++ .../tests/programs/assembly/fibonacci.val | 38 ++ .../tests/programs/assembly/subtraction.val | 7 + .../tests/programs/binary/fibonacci.bin | Bin 0 -> 720 bytes .../tests/programs/binary/subtraction.bin | Bin 0 -> 120 bytes basic_macro/tests/test_interpreter.rs | 43 +++ basic_macro/tests/test_prover.rs | 262 +++++++++++++ basic_macro/tests/test_static_data.rs | 113 ++++++ 13 files changed, 1341 insertions(+) create mode 100644 basic_macro/Cargo.toml create mode 100644 basic_macro/src/bin/test_prover.rs create mode 100644 basic_macro/src/bin/valida.rs create mode 100644 basic_macro/src/lib.rs create mode 100644 basic_macro/tests/programs/assembly/fibonacci.val create mode 100644 basic_macro/tests/programs/assembly/subtraction.val create mode 100644 basic_macro/tests/programs/binary/fibonacci.bin create mode 100644 basic_macro/tests/programs/binary/subtraction.bin create mode 100644 basic_macro/tests/test_interpreter.rs create mode 100644 basic_macro/tests/test_prover.rs create mode 100644 basic_macro/tests/test_static_data.rs diff --git a/Cargo.lock b/Cargo.lock index c57a567..b2d5a86 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -1082,6 +1082,48 @@ dependencies = [ "valida-static-data", ] +[[package]] +name = "valida-basic-macro" +version = "0.1.0" +dependencies = [ + "byteorder", + "ciborium", + "clap", + "p3-air", + "p3-baby-bear", + "p3-challenger", + "p3-commit", + "p3-dft", + "p3-field", + "p3-fri", + "p3-goldilocks", + "p3-keccak", + "p3-matrix", + "p3-maybe-rayon", + "p3-mds", + "p3-merkle-tree", + "p3-poseidon", + "p3-symmetric", + "p3-uni-stark", + "p3-util", + "rand", + "rand_pcg", + "rand_seeder", + "tracing", + "valida-alu-u32", + "valida-assembler", + "valida-bus", + "valida-cpu", + "valida-derive", + "valida-machine", + "valida-memory", + "valida-opcodes", + "valida-output", + "valida-program", + "valida-range", + "valida-static-data", +] + [[package]] name = "valida-bus" version = "0.1.0" diff --git a/Cargo.toml b/Cargo.toml index c91bac6..a59aeb3 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -4,6 +4,7 @@ members = [ "assembler", "alu_u32", "basic", + "basic_macro", "bus", "cpu", "derive", diff --git a/basic_macro/Cargo.toml b/basic_macro/Cargo.toml new file mode 100644 index 0000000..3b2e095 --- /dev/null +++ b/basic_macro/Cargo.toml @@ -0,0 +1,63 @@ +[package] +name = "valida-basic-macro" +version = "0.1.0" +edition = "2021" +license = "MIT OR Apache-2.0" + +[[bin]] +name = "valida_macro" +path = "src/bin/valida.rs" + +[[bin]] +name = "test_prover_macro" +path = "src/bin/test_prover.rs" + +[dependencies] +byteorder = "1.4.3" +ciborium = "0.2.2" +clap = { version = "4.3.19", features = ["derive"] } +rand = "0.8.5" +rand_pcg = "0.3.1" +rand_seeder = "0.2.3" +tracing = "0.1.37" +valida-alu-u32 = { path = "../alu_u32" } +valida-assembler = { path = "../assembler" } +valida-bus = { path = "../bus" } +valida-cpu = { path = "../cpu" } +valida-derive = { path = "../derive" } +valida-machine = { path = "../machine" } +valida-memory = { path = "../memory" } +valida-opcodes = { path = "../opcodes" } +valida-output = { path = "../output" } +valida-program = { path = "../program" } +valida-range = { path = "../range" } +valida-static-data = { path = "../static_data" } +p3-baby-bear = { workspace = true } +p3-field = { workspace = true } +p3-maybe-rayon = { workspace = true } +p3-util = { workspace = true } +p3-goldilocks = { workspace = true } +p3-uni-stark = { workspace = true } +p3-commit = { workspace = true } +p3-air = { workspace = true } +p3-matrix = { workspace = true } +p3-challenger = { workspace = true } +p3-dft = { workspace = true } +p3-fri = { workspace = true } +p3-keccak = { workspace = true } +p3-mds = { workspace = true } +p3-merkle-tree = { workspace = true } +p3-poseidon = { workspace = true } +p3-symmetric = { workspace = true } + +[dev-dependencies] +ciborium = "0.2.2" +p3-challenger = { workspace = true } +p3-dft = { workspace = true } +p3-field = { workspace = true } +p3-fri = { workspace = true } +p3-keccak = { workspace = true } +p3-mds = { workspace = true } +p3-merkle-tree = { workspace = true } +p3-poseidon = { workspace = true } +p3-symmetric = { workspace = true } diff --git a/basic_macro/src/bin/test_prover.rs b/basic_macro/src/bin/test_prover.rs new file mode 100644 index 0000000..27116fb --- /dev/null +++ b/basic_macro/src/bin/test_prover.rs @@ -0,0 +1,263 @@ +extern crate core; + +use p3_baby_bear::BabyBear; +use p3_fri::{TwoAdicFriPcs, TwoAdicFriPcsConfig}; +use valida_alu_u32::add::Add32Instruction; +use valida_basic_macro::BasicMachine; +use valida_cpu::{ + BeqInstruction, BneInstruction, Imm32Instruction, JalInstruction, JalvInstruction, + MachineWithCpuChip, StopInstruction, +}; +use valida_machine::{ + FixedAdviceProvider, Instruction, InstructionWord, Machine, MachineProof, Operands, ProgramROM, +}; + +use valida_opcodes::BYTES_PER_INSTR; +use valida_program::MachineWithProgramChip; + +use p3_challenger::DuplexChallenger; +use p3_dft::Radix2Bowers; +use p3_field::extension::BinomialExtensionField; +use p3_field::Field; +use p3_fri::FriConfig; +use p3_keccak::Keccak256Hash; +use p3_mds::coset_mds::CosetMds; +use p3_merkle_tree::FieldMerkleTreeMmcs; +use p3_poseidon::Poseidon; +use p3_symmetric::{CompressionFunctionFromHasher, SerializingHasher32}; +use rand::thread_rng; +use valida_machine::StarkConfigImpl; +use valida_machine::__internal::p3_commit::ExtensionMmcs; + +fn main() { + prove_fibonacci() +} + +fn prove_fibonacci() { + let mut program = vec![]; + + // Label locations + let bytes_per_instr = BYTES_PER_INSTR as i32; + let fib_bb0 = 8 * bytes_per_instr; + let fib_bb0_1 = 13 * bytes_per_instr; + let fib_bb0_2 = 15 * bytes_per_instr; + let fib_bb0_3 = 19 * bytes_per_instr; + let fib_bb0_4 = 21 * bytes_per_instr; + + //main: ; @main + //; %bb.0: + // imm32 -4(fp), 0, 0, 0, 0 + // imm32 -8(fp), 0, 0, 0, 100 + // addi -16(fp), -8(fp), 0 + // imm32 -20(fp), 0, 0, 0, 28 + // jal -28(fp), fib, -28 + // addi -12(fp), -24(fp), 0 + // addi 4(fp), -12(fp), 0 + // exit + //... + program.extend([ + InstructionWord { + opcode: , Val>>::OPCODE, + operands: Operands([-4, 0, 0, 0, 0]), + }, + InstructionWord { + opcode: , Val>>::OPCODE, + operands: Operands([-8, 0, 0, 0, 100]), + }, + InstructionWord { + opcode: , Val>>::OPCODE, + operands: Operands([-16, -8, 0, 0, 1]), + }, + InstructionWord { + opcode: , Val>>::OPCODE, + operands: Operands([-20, 0, 0, 0, 28]), + }, + InstructionWord { + opcode: , Val>>::OPCODE, + operands: Operands([-28, fib_bb0, -28, 0, 0]), + }, + InstructionWord { + opcode: , Val>>::OPCODE, + operands: Operands([-12, -24, 0, 0, 1]), + }, + InstructionWord { + opcode: , Val>>::OPCODE, + operands: Operands([4, -12, 0, 0, 1]), + }, + InstructionWord { + opcode: , Val>>::OPCODE, + operands: Operands::default(), + }, + ]); + + //fib: ; @fib + //; %bb.0: + // addi -4(fp), 12(fp), 0 + // imm32 -8(fp), 0, 0, 0, 0 + // imm32 -12(fp), 0, 0, 0, 1 + // imm32 -16(fp), 0, 0, 0, 0 + // beq .LBB0_1, 0(fp), 0(fp) + program.extend([ + InstructionWord { + opcode: , Val>>::OPCODE, + operands: Operands([-4, 12, 0, 0, 1]), + }, + InstructionWord { + opcode: , Val>>::OPCODE, + operands: Operands([-8, 0, 0, 0, 0]), + }, + InstructionWord { + opcode: , Val>>::OPCODE, + operands: Operands([-12, 0, 0, 0, 1]), + }, + InstructionWord { + opcode: , Val>>::OPCODE, + operands: Operands([-16, 0, 0, 0, 0]), + }, + InstructionWord { + opcode: , Val>>::OPCODE, + operands: Operands([fib_bb0_1, 0, 0, 0, 0]), + }, + ]); + + //.LBB0_1: + // bne .LBB0_2, -16(fp), -4(fp) + // beq .LBB0_4, 0(fp), 0(fp) + program.extend([ + InstructionWord { + opcode: , Val>>::OPCODE, + operands: Operands([fib_bb0_2, -16, -4, 0, 0]), + }, + InstructionWord { + opcode: , Val>>::OPCODE, + operands: Operands([fib_bb0_4, 0, 0, 0, 0]), + }, + ]); + + //; %bb.2: + // add -20(fp), -8(fp), -12(fp) + // addi -8(fp), -12(fp), 0 + // addi -12(fp), -20(fp), 0 + // beq .LBB0_3, 0(fp), 0(fp) + program.extend([ + InstructionWord { + opcode: , Val>>::OPCODE, + operands: Operands([-20, -8, -12, 0, 0]), + }, + InstructionWord { + opcode: , Val>>::OPCODE, + operands: Operands([-8, -12, 0, 0, 1]), + }, + InstructionWord { + opcode: , Val>>::OPCODE, + operands: Operands([-12, -20, 0, 0, 1]), + }, + InstructionWord { + opcode: , Val>>::OPCODE, + operands: Operands([fib_bb0_3, 0, 0, 0, 0]), + }, + ]); + + //; %bb.3: + // addi -16(fp), -16(fp), 1 + // beq .LBB0_1, 0(fp), 0(fp) + program.extend([ + InstructionWord { + opcode: , Val>>::OPCODE, + operands: Operands([-16, -16, 1, 0, 1]), + }, + InstructionWord { + opcode: , Val>>::OPCODE, + operands: Operands([fib_bb0_1, 0, 0, 0, 0]), + }, + ]); + + //.LBB0_4: + // addi 4(fp), -8(fp), 0 + // jalv -4(fp), 0(fp), 8(fp) + program.extend([ + InstructionWord { + opcode: , Val>>::OPCODE, + operands: Operands([4, -8, 0, 0, 1]), + }, + InstructionWord { + opcode: , Val>>::OPCODE, + operands: Operands([-4, 0, 8, 0, 0]), + }, + ]); + + let mut machine = BasicMachine::::default(); + let rom = ProgramROM::new(program); + machine.program_mut().set_program_rom(&rom); + machine.cpu_mut().fp = 0x1000; + machine.cpu_mut().save_register_state(); // TODO: Initial register state should be saved + // automatically by the machine, not manually here + machine.run(&rom, &mut FixedAdviceProvider::empty()); + + type Val = BabyBear; + type Challenge = BinomialExtensionField; + type PackedChallenge = BinomialExtensionField<::Packing, 5>; + + type Mds16 = CosetMds; + let mds16 = Mds16::default(); + + type Perm16 = Poseidon; + let perm16 = Perm16::new_from_rng(4, 22, mds16, &mut thread_rng()); // TODO: Use deterministic RNG + + type MyHash = SerializingHasher32; + let hash = MyHash::new(Keccak256Hash {}); + + type MyCompress = CompressionFunctionFromHasher; + let compress = MyCompress::new(hash); + + type ValMmcs = FieldMerkleTreeMmcs; + let val_mmcs = ValMmcs::new(hash, compress); + + type ChallengeMmcs = ExtensionMmcs; + let challenge_mmcs = ChallengeMmcs::new(val_mmcs.clone()); + + type Dft = Radix2Bowers; + let dft = Dft::default(); + + type Challenger = DuplexChallenger; + + type MyFriConfig = TwoAdicFriPcsConfig; + let fri_config = FriConfig { + log_blowup: 1, + num_queries: 40, + proof_of_work_bits: 8, + mmcs: challenge_mmcs, + }; + + type Pcs = TwoAdicFriPcs; + type MyConfig = StarkConfigImpl; + + let pcs = Pcs::new(fri_config, dft, val_mmcs); + + let challenger = Challenger::new(perm16); + let config = MyConfig::new(pcs, challenger); + let proof = machine.prove(&config); + + let mut bytes = vec![]; + ciborium::into_writer(&proof, &mut bytes).expect("serialization failed"); + println!("Proof size: {} bytes", bytes.len()); + let deserialized_proof: MachineProof = + ciborium::from_reader(bytes.as_slice()).expect("deserialization failed"); + + machine + .verify(&config, &proof) + .expect("verification failed"); + machine + .verify(&config, &deserialized_proof) + .expect("verification failed"); + + // assert_eq!(machine.cpu().clock, 192); + // assert_eq!(machine.cpu().operations.len(), 192); + // assert_eq!(machine.mem().operations.values().flatten().count(), 401); + // assert_eq!(machine.add_u32().operations.len(), 105); + + // assert_eq!( + // *machine.mem().cells.get(&(0x1000 + 4)).unwrap(), // Return value + // Word([0, 1, 37, 17,]) // 25th fibonacci number (75025) + // ); +} diff --git a/basic_macro/src/bin/valida.rs b/basic_macro/src/bin/valida.rs new file mode 100644 index 0000000..a7b2eb2 --- /dev/null +++ b/basic_macro/src/bin/valida.rs @@ -0,0 +1,157 @@ +use clap::Parser; +use std::fs::File; +use std::io::{stdout, Write}; + +use valida_basic_macro::BasicMachine; + +use p3_baby_bear::BabyBear; + +use p3_fri::{FriConfig, TwoAdicFriPcs, TwoAdicFriPcsConfig}; +use valida_cpu::MachineWithCpuChip; +use valida_machine::{Machine, MachineProof, ProgramROM, StdinAdviceProvider}; + +use valida_program::MachineWithProgramChip; + +use p3_challenger::DuplexChallenger; +use p3_dft::Radix2DitParallel; +use p3_field::extension::BinomialExtensionField; +use p3_field::Field; +use p3_keccak::Keccak256Hash; +use p3_mds::coset_mds::CosetMds; +use p3_merkle_tree::FieldMerkleTreeMmcs; +use p3_poseidon::Poseidon; +use p3_symmetric::{CompressionFunctionFromHasher, SerializingHasher32}; +use rand_pcg::Pcg64; +use rand_seeder::Seeder; +use valida_machine::StarkConfigImpl; +use valida_machine::__internal::p3_commit::ExtensionMmcs; +use valida_output::MachineWithOutputChip; + +#[derive(Parser)] +struct Args { + /// Command option either "run" or "prove" or "verify" + #[arg(name = "Action Option")] + action: String, + + /// Program binary file + #[arg(name = "PROGRAM FILE")] + program: String, + + /// The output file for run or prove, or the input file for verify + #[arg(name = "ACTION FILE")] + action_file: String, + + /// Stack height (which is also the initial frame pointer value) + #[arg(long, default_value = "16777216")] + stack_height: u32, +} + +fn main() { + let args = Args::parse(); + + let mut machine = BasicMachine::::default(); + let rom = match ProgramROM::from_file(&args.program) { + Ok(contents) => contents, + Err(e) => panic!("Failure to load file: {}. {}", &args.program, e), + }; + machine.program_mut().set_program_rom(&rom); + machine.cpu_mut().fp = args.stack_height; + machine.cpu_mut().save_register_state(); + + // Run the program + machine.run(&rom, &mut StdinAdviceProvider); + + type Val = BabyBear; + type Challenge = BinomialExtensionField; + type PackedChallenge = BinomialExtensionField<::Packing, 5>; + + type Mds16 = CosetMds; + let mds16 = Mds16::default(); + + type Perm16 = Poseidon; + let mut rng: Pcg64 = Seeder::from("validia seed").make_rng(); + let perm16 = Perm16::new_from_rng(4, 22, mds16, &mut rng); + + type MyHash = SerializingHasher32; + let hash = MyHash::new(Keccak256Hash {}); + + type MyCompress = CompressionFunctionFromHasher; + let compress = MyCompress::new(hash); + + type ValMmcs = FieldMerkleTreeMmcs; + let val_mmcs = ValMmcs::new(hash, compress); + + type ChallengeMmcs = ExtensionMmcs; + let challenge_mmcs = ChallengeMmcs::new(val_mmcs.clone()); + + type Dft = Radix2DitParallel; + let dft = Dft::default(); + + type Challenger = DuplexChallenger; + + type MyFriConfig = TwoAdicFriPcsConfig; + let fri_config = FriConfig { + log_blowup: 1, + num_queries: 40, + proof_of_work_bits: 8, + mmcs: challenge_mmcs, + }; + + type Pcs = TwoAdicFriPcs; + type MyConfig = StarkConfigImpl; + + let pcs = Pcs::new(fri_config, dft, val_mmcs); + + let challenger = Challenger::new(perm16); + let config = MyConfig::new(pcs, challenger); + + if args.action == "run" { + let mut action_file; + match File::create(args.action_file) { + Ok(file) => { + action_file = file; + } + Err(e) => { + stdout().write(e.to_string().as_bytes()).unwrap(); + return (); + } + } + action_file.write_all(&machine.output().bytes()).unwrap(); + } else if args.action == "prove" { + let mut action_file; + match File::create(args.action_file) { + Ok(file) => { + action_file = file; + } + Err(e) => { + stdout().write(e.to_string().as_bytes()).unwrap(); + return (); + } + } + let proof = machine.prove(&config); + debug_assert!(machine.verify(&config, &proof).is_ok()); + let mut bytes = vec![]; + ciborium::into_writer(&proof, &mut bytes).expect("Proof serialization failed"); + action_file.write(&bytes).expect("Writing proof failed"); + stdout().write("Proof successful\n".as_bytes()).unwrap(); + } else if args.action == "verify" { + let bytes = std::fs::read(args.action_file).expect("File reading failed"); + let proof: MachineProof = + ciborium::from_reader(bytes.as_slice()).expect("Proof deserialization failed"); + let verification_result = machine.verify(&config, &proof); + match verification_result { + Ok(_) => { + stdout().write("Proof verified\n".as_bytes()).unwrap(); + } + Err(_) => { + stdout() + .write("Proof verification failed\n".as_bytes()) + .unwrap(); + } + } + } else { + stdout() + .write("Action name unrecognized".as_bytes()) + .unwrap(); + } +} diff --git a/basic_macro/src/lib.rs b/basic_macro/src/lib.rs new file mode 100644 index 0000000..6c07d93 --- /dev/null +++ b/basic_macro/src/lib.rs @@ -0,0 +1,352 @@ +#![no_std] +#![allow(unused)] + +extern crate alloc; + +use alloc::vec::Vec; +use core::marker::PhantomData; +use p3_air::Air; +use p3_commit::{Pcs, UnivariatePcs, UnivariatePcsWithLde}; +use p3_field::PrimeField32; +use p3_field::{extension::BinomialExtensionField, TwoAdicField}; +use p3_matrix::dense::RowMajorMatrix; +use p3_maybe_rayon::*; +use p3_util::log2_ceil_usize; +use valida_alu_u32::{ + add::{Add32Chip, Add32Instruction, MachineWithAdd32Chip}, + bitwise::{ + And32Instruction, Bitwise32Chip, MachineWithBitwise32Chip, Or32Instruction, + Xor32Instruction, + }, + com::{Com32Chip, Eq32Instruction, MachineWithCom32Chip, Ne32Instruction}, + div::{Div32Chip, Div32Instruction, MachineWithDiv32Chip, SDiv32Instruction}, + lt::{Lt32Chip, Lt32Instruction, Lte32Instruction, MachineWithLt32Chip}, + mul::{ + MachineWithMul32Chip, Mul32Chip, Mul32Instruction, Mulhs32Instruction, Mulhu32Instruction, + }, + shift::{ + MachineWithShift32Chip, Shift32Chip, Shl32Instruction, Shr32Instruction, Sra32Instruction, + }, + sub::{MachineWithSub32Chip, Sub32Chip, Sub32Instruction}, +}; +use valida_bus::{ + MachineWithGeneralBus, MachineWithMemBus, MachineWithProgramBus, MachineWithRangeBus8, +}; +use valida_cpu::{ + BeqInstruction, BneInstruction, Imm32Instruction, JalInstruction, JalvInstruction, + Load32Instruction, LoadFpInstruction, ReadAdviceInstruction, StopInstruction, + Store32Instruction, +}; +use valida_cpu::{CpuChip, MachineWithCpuChip}; +use valida_derive::Machine; +use valida_machine::{ + AdviceProvider, BusArgument, Chip, ChipProof, Instruction, Machine, MachineProof, ProgramROM, + ValidaAirBuilder, +}; +use valida_memory::{MachineWithMemoryChip, MemoryChip}; +use valida_output::{MachineWithOutputChip, OutputChip, WriteInstruction}; +use valida_program::{MachineWithProgramChip, ProgramChip}; +use valida_range::{MachineWithRangeChip, RangeCheckerChip}; +use valida_static_data::{MachineWithStaticDataChip, StaticDataChip}; + +use p3_maybe_rayon::prelude::*; +use valida_machine::StarkConfig; + +#[derive(Machine, Default)] +#[machine_fields(F)] +pub struct BasicMachine { + // Core instructions + #[instruction] + load32: Load32Instruction, + + #[instruction] + store32: Store32Instruction, + + #[instruction] + jal: JalInstruction, + + #[instruction] + jalv: JalvInstruction, + + #[instruction] + beq: BeqInstruction, + + #[instruction] + bne: BneInstruction, + + #[instruction] + imm32: Imm32Instruction, + + #[instruction] + stop: StopInstruction, + + #[instruction] + loadfp: LoadFpInstruction, + + // ALU instructions + #[instruction(add_u32)] + add32: Add32Instruction, + + #[instruction(sub_u32)] + sub32: Sub32Instruction, + + #[instruction(mul_u32)] + mul32: Mul32Instruction, + + #[instruction(mul_u32)] + mulhs32: Mulhs32Instruction, + + #[instruction(mul_u32)] + mulhu32: Mulhu32Instruction, + + #[instruction(div_u32)] + div32: Div32Instruction, + + #[instruction(div_u32)] + sdiv32: SDiv32Instruction, + + #[instruction(shift_u32)] + shl32: Shl32Instruction, + + #[instruction(shift_u32)] + shr32: Shr32Instruction, + + #[instruction(shift_u32)] + sra32: Sra32Instruction, + + #[instruction(lt_u32)] + lt32: Lt32Instruction, + + #[instruction(lt_u32)] + lte32: Lte32Instruction, + + #[instruction(bitwise_u32)] + and32: And32Instruction, + + #[instruction(bitwise_u32)] + or32: Or32Instruction, + + #[instruction(bitwise_u32)] + xor32: Xor32Instruction, + + #[instruction(com_u32)] + ne32: Ne32Instruction, + + #[instruction(com_u32)] + eq32: Eq32Instruction, + + // Input/output instructions + #[instruction] + read: ReadAdviceInstruction, + + #[instruction(output)] + write: WriteInstruction, + + #[chip] + cpu: CpuChip, + + #[chip] + program: ProgramChip, + + #[chip] + mem: MemoryChip, + + #[chip] + add_u32: Add32Chip, + + #[chip] + sub_u32: Sub32Chip, + + #[chip] + mul_u32: Mul32Chip, + + #[chip] + div_u32: Div32Chip, + + #[chip] + shift_u32: Shift32Chip, + + #[chip] + lt_u32: Lt32Chip, + + #[chip] + com_u32: Com32Chip, + + #[chip] + bitwise_u32: Bitwise32Chip, + + #[chip] + output: OutputChip, + + #[chip] + range: RangeCheckerChip<256>, + + #[chip] + #[static_data_chip] + static_data: StaticDataChip, + + _phantom_sc: PhantomData F>, +} + +impl MachineWithGeneralBus for BasicMachine { + fn general_bus(&self) -> BusArgument { + BusArgument::Global(0) + } +} + +impl MachineWithProgramBus for BasicMachine { + fn program_bus(&self) -> BusArgument { + BusArgument::Global(1) + } +} + +impl MachineWithMemBus for BasicMachine { + fn mem_bus(&self) -> BusArgument { + BusArgument::Global(2) + } +} + +impl MachineWithRangeBus8 for BasicMachine { + fn range_bus(&self) -> BusArgument { + BusArgument::Global(3) + } +} + +impl MachineWithCpuChip for BasicMachine { + fn cpu(&self) -> &CpuChip { + &self.cpu + } + + fn cpu_mut(&mut self) -> &mut CpuChip { + &mut self.cpu + } +} + +impl MachineWithProgramChip for BasicMachine { + fn program(&self) -> &ProgramChip { + &self.program + } + + fn program_mut(&mut self) -> &mut ProgramChip { + &mut self.program + } +} + +impl MachineWithMemoryChip for BasicMachine { + fn mem(&self) -> &MemoryChip { + &self.mem + } + + fn mem_mut(&mut self) -> &mut MemoryChip { + &mut self.mem + } +} + +impl MachineWithAdd32Chip for BasicMachine { + fn add_u32(&self) -> &Add32Chip { + &self.add_u32 + } + + fn add_u32_mut(&mut self) -> &mut Add32Chip { + &mut self.add_u32 + } +} + +impl MachineWithSub32Chip for BasicMachine { + fn sub_u32(&self) -> &Sub32Chip { + &self.sub_u32 + } + + fn sub_u32_mut(&mut self) -> &mut Sub32Chip { + &mut self.sub_u32 + } +} + +impl MachineWithMul32Chip for BasicMachine { + fn mul_u32(&self) -> &Mul32Chip { + &self.mul_u32 + } + + fn mul_u32_mut(&mut self) -> &mut Mul32Chip { + &mut self.mul_u32 + } +} + +impl MachineWithDiv32Chip for BasicMachine { + fn div_u32(&self) -> &Div32Chip { + &self.div_u32 + } + + fn div_u32_mut(&mut self) -> &mut Div32Chip { + &mut self.div_u32 + } +} + +impl MachineWithBitwise32Chip for BasicMachine { + fn bitwise_u32(&self) -> &Bitwise32Chip { + &self.bitwise_u32 + } + + fn bitwise_u32_mut(&mut self) -> &mut Bitwise32Chip { + &mut self.bitwise_u32 + } +} + +impl MachineWithLt32Chip for BasicMachine { + fn lt_u32(&self) -> &Lt32Chip { + &self.lt_u32 + } + + fn lt_u32_mut(&mut self) -> &mut Lt32Chip { + &mut self.lt_u32 + } +} +impl MachineWithCom32Chip for BasicMachine { + fn com_u32(&self) -> &Com32Chip { + &self.com_u32 + } + + fn com_u32_mut(&mut self) -> &mut Com32Chip { + &mut self.com_u32 + } +} + +impl MachineWithShift32Chip for BasicMachine { + fn shift_u32(&self) -> &Shift32Chip { + &self.shift_u32 + } + + fn shift_u32_mut(&mut self) -> &mut Shift32Chip { + &mut self.shift_u32 + } +} + +impl MachineWithOutputChip for BasicMachine { + fn output(&self) -> &OutputChip { + &self.output + } + + fn output_mut(&mut self) -> &mut OutputChip { + &mut self.output + } +} + +impl MachineWithRangeChip for BasicMachine { + fn range(&self) -> &RangeCheckerChip<256> { + &self.range + } + + fn range_mut(&mut self) -> &mut RangeCheckerChip<256> { + &mut self.range + } +} + +impl MachineWithStaticDataChip for BasicMachine { + fn static_data(&self) -> &StaticDataChip { + &self.static_data + } + + fn static_data_mut(&mut self) -> &mut StaticDataChip { + &mut self.static_data + } +} diff --git a/basic_macro/tests/programs/assembly/fibonacci.val b/basic_macro/tests/programs/assembly/fibonacci.val new file mode 100644 index 0000000..7caf938 --- /dev/null +++ b/basic_macro/tests/programs/assembly/fibonacci.val @@ -0,0 +1,38 @@ +main: + imm32 -4(fp), 0, 0, 0, 0 + ; Read the fibonacci number count from input + advread -8 + addi -16(fp), -8(fp), 0 + imm32 -20(fp), 0, 0, 0, 28 + jal -28(fp), fib, -28 + addi -12(fp), -24(fp), 0 + addi 4(fp), -12(fp), 0 + ; Write the result to output + write 0, 4, 0, 0, 1 + divi 4, 4, 256 + write 0, 4, 0, 0, 1 + divi 4, 4, 256 + write 0, 4, 0, 0, 1 + divi 4, 4, 256 + write 0, 4, 0, 0, 1 + stop +fib: + addi -4(fp), 12(fp), 0 + imm32 -8(fp), 0, 0, 0, 0 + imm32 -12(fp), 0, 0, 0, 1 + imm32 -16(fp), 0, 0, 0, 0 + beq .LBB0_1, 0(fp), 0(fp) +.LBB0_1: + bne .LBB0_2, -16(fp), -4(fp) + beq .LBB0_4, 0(fp), 0(fp) +.LBB0_2: + add -20(fp), -8(fp), -12(fp) + addi -8(fp), -12(fp), 0 + addi -12(fp), -20(fp), 0 + beq .LBB0_3, 0(fp), 0(fp) +.LBB0_3: + addi -16(fp), -16(fp), 1 + beq .LBB0_1, 0(fp), 0(fp) +.LBB0_4: + addi 4(fp), -8(fp), 0 + jalv -4(fp), 0(fp), 8(fp) diff --git a/basic_macro/tests/programs/assembly/subtraction.val b/basic_macro/tests/programs/assembly/subtraction.val new file mode 100644 index 0000000..7a57c10 --- /dev/null +++ b/basic_macro/tests/programs/assembly/subtraction.val @@ -0,0 +1,7 @@ +main: + ; TODO: Test different classes of input + imm32 0(fp), 0, 0, 0, 12 + imm32 -4(fp), 0, 0, 0, 5 + sub 4(fp), 0(fp), -4(fp) + write 0, 4(fp), 0, 0, 1 + stop diff --git a/basic_macro/tests/programs/binary/fibonacci.bin b/basic_macro/tests/programs/binary/fibonacci.bin new file mode 100644 index 0000000000000000000000000000000000000000..36ef4ce1e864da0d06452f632dafd3bedb436f36 GIT binary patch literal 720 zcmc(cu?hk)5JV%Mo`PT_7UCz|XC3(C78Vv378XLB7qT!e_Abor?aL&$w;4+*?^>(U zS8RK=P=49^toota8Jh@)65@aeV~_xY@d&j5 literal 0 HcmV?d00001 diff --git a/basic_macro/tests/test_interpreter.rs b/basic_macro/tests/test_interpreter.rs new file mode 100644 index 0000000..12af4a9 --- /dev/null +++ b/basic_macro/tests/test_interpreter.rs @@ -0,0 +1,43 @@ +use p3_baby_bear::BabyBear; +use std::fs::read_to_string; +use valida_assembler::assemble; +use valida_basic_macro::BasicMachine; +use valida_cpu::MachineWithCpuChip; +use valida_machine::{FixedAdviceProvider, Machine, ProgramROM}; +use valida_output::MachineWithOutputChip; +use valida_program::MachineWithProgramChip; + +#[test] +fn run_fibonacci() { + let mut machine = BasicMachine::::default(); + let asm_path = "tests/programs/assembly/fibonacci.val"; + let asm = read_to_string(asm_path).expect("Failed to read asm"); + let rom = ProgramROM::from_machine_code(&assemble(&asm).unwrap()); + machine.program_mut().set_program_rom(&rom); + machine.cpu_mut().fp = 16777216; // default stack height + machine.cpu_mut().save_register_state(); + + let fib_number = 25; + // Put the desired fib number in the advice tape. + let mut advice = FixedAdviceProvider::new(vec![fib_number]); + + // Run the program + machine.run(&rom, &mut advice); + let output = machine.output().bytes(); + assert_eq!(output.len(), 4); + let actual_result = u32::from_le_bytes(output.try_into().unwrap()); + + let expected_result = fibonacci(fib_number); + assert_eq!(actual_result, expected_result); +} + +fn fibonacci(n: u8) -> u32 { + let mut a = 0u32; + let mut b = 1u32; + for _ in 0..n { + let temp = a; + a = b; + (b, _) = temp.overflowing_add(b); + } + a +} diff --git a/basic_macro/tests/test_prover.rs b/basic_macro/tests/test_prover.rs new file mode 100644 index 0000000..0a1a0ca --- /dev/null +++ b/basic_macro/tests/test_prover.rs @@ -0,0 +1,262 @@ +extern crate core; + +use p3_baby_bear::BabyBear; +use p3_fri::{TwoAdicFriPcs, TwoAdicFriPcsConfig}; +use valida_alu_u32::add::{Add32Instruction, MachineWithAdd32Chip}; +use valida_basic_macro::BasicMachine; +use valida_cpu::{ + BeqInstruction, BneInstruction, Imm32Instruction, JalInstruction, JalvInstruction, + MachineWithCpuChip, StopInstruction, +}; +use valida_machine::{ + FixedAdviceProvider, Instruction, InstructionWord, Machine, MachineProof, Operands, ProgramROM, + Word, +}; + +use valida_memory::MachineWithMemoryChip; +use valida_opcodes::BYTES_PER_INSTR; +use valida_program::MachineWithProgramChip; + +use p3_challenger::DuplexChallenger; +use p3_dft::Radix2Bowers; +use p3_field::extension::BinomialExtensionField; +use p3_field::Field; +use p3_fri::FriConfig; +use p3_keccak::Keccak256Hash; +use p3_mds::coset_mds::CosetMds; +use p3_merkle_tree::FieldMerkleTreeMmcs; +use p3_poseidon::Poseidon; +use p3_symmetric::{CompressionFunctionFromHasher, SerializingHasher32}; +use rand::thread_rng; +use valida_machine::StarkConfigImpl; +use valida_machine::__internal::p3_commit::ExtensionMmcs; + +#[test] +fn prove_fibonacci() { + let mut program = vec![]; + + // Label locations + let bytes_per_instr = BYTES_PER_INSTR as i32; + let fib_bb0 = 8 * bytes_per_instr; + let fib_bb0_1 = 13 * bytes_per_instr; + let fib_bb0_2 = 15 * bytes_per_instr; + let fib_bb0_3 = 19 * bytes_per_instr; + let fib_bb0_4 = 21 * bytes_per_instr; + + //main: ; @main + //; %bb.0: + // imm32 -4(fp), 0, 0, 0, 0 + // imm32 -8(fp), 0, 0, 0, 10 + // addi -16(fp), -8(fp), 0 + // imm32 -20(fp), 0, 0, 0, 28 + // jal -28(fp), fib, -28 + // addi -12(fp), -24(fp), 0 + // addi 4(fp), -12(fp), 0 + // exit + //... + program.extend([ + InstructionWord { + opcode: , Val>>::OPCODE, + operands: Operands([-4, 0, 0, 0, 0]), + }, + InstructionWord { + opcode: , Val>>::OPCODE, + operands: Operands([-8, 0, 0, 0, 25]), + }, + InstructionWord { + opcode: , Val>>::OPCODE, + operands: Operands([-16, -8, 0, 0, 1]), + }, + InstructionWord { + opcode: , Val>>::OPCODE, + operands: Operands([-20, 0, 0, 0, 28]), + }, + InstructionWord { + opcode: , Val>>::OPCODE, + operands: Operands([-28, fib_bb0, -28, 0, 0]), + }, + InstructionWord { + opcode: , Val>>::OPCODE, + operands: Operands([-12, -24, 0, 0, 1]), + }, + InstructionWord { + opcode: , Val>>::OPCODE, + operands: Operands([4, -12, 0, 0, 1]), + }, + InstructionWord { + opcode: , Val>>::OPCODE, + operands: Operands::default(), + }, + ]); + + //fib: ; @fib + //; %bb.0: + // addi -4(fp), 12(fp), 0 + // imm32 -8(fp), 0, 0, 0, 0 + // imm32 -12(fp), 0, 0, 0, 1 + // imm32 -16(fp), 0, 0, 0, 0 + // beq .LBB0_1, 0(fp), 0(fp) + program.extend([ + InstructionWord { + opcode: , Val>>::OPCODE, + operands: Operands([-4, 12, 0, 0, 1]), + }, + InstructionWord { + opcode: , Val>>::OPCODE, + operands: Operands([-8, 0, 0, 0, 0]), + }, + InstructionWord { + opcode: , Val>>::OPCODE, + operands: Operands([-12, 0, 0, 0, 1]), + }, + InstructionWord { + opcode: , Val>>::OPCODE, + operands: Operands([-16, 0, 0, 0, 0]), + }, + InstructionWord { + opcode: , Val>>::OPCODE, + operands: Operands([fib_bb0_1, 0, 0, 0, 0]), + }, + ]); + + //.LBB0_1: + // bne .LBB0_2, -16(fp), -4(fp) + // beq .LBB0_4, 0(fp), 0(fp) + program.extend([ + InstructionWord { + opcode: , Val>>::OPCODE, + operands: Operands([fib_bb0_2, -16, -4, 0, 0]), + }, + InstructionWord { + opcode: , Val>>::OPCODE, + operands: Operands([fib_bb0_4, 0, 0, 0, 0]), + }, + ]); + + //; %bb.2: + // add -20(fp), -8(fp), -12(fp) + // addi -8(fp), -12(fp), 0 + // addi -12(fp), -20(fp), 0 + // beq .LBB0_3, 0(fp), 0(fp) + program.extend([ + InstructionWord { + opcode: , Val>>::OPCODE, + operands: Operands([-20, -8, -12, 0, 0]), + }, + InstructionWord { + opcode: , Val>>::OPCODE, + operands: Operands([-8, -12, 0, 0, 1]), + }, + InstructionWord { + opcode: , Val>>::OPCODE, + operands: Operands([-12, -20, 0, 0, 1]), + }, + InstructionWord { + opcode: , Val>>::OPCODE, + operands: Operands([fib_bb0_3, 0, 0, 0, 0]), + }, + ]); + + //; %bb.3: + // addi -16(fp), -16(fp), 1 + // beq .LBB0_1, 0(fp), 0(fp) + program.extend([ + InstructionWord { + opcode: , Val>>::OPCODE, + operands: Operands([-16, -16, 1, 0, 1]), + }, + InstructionWord { + opcode: , Val>>::OPCODE, + operands: Operands([fib_bb0_1, 0, 0, 0, 0]), + }, + ]); + + //.LBB0_4: + // addi 4(fp), -8(fp), 0 + // jalv -4(fp), 0(fp), 8(fp) + program.extend([ + InstructionWord { + opcode: , Val>>::OPCODE, + operands: Operands([4, -8, 0, 0, 1]), + }, + InstructionWord { + opcode: , Val>>::OPCODE, + operands: Operands([-4, 0, 8, 0, 0]), + }, + ]); + + let mut machine = BasicMachine::::default(); + let rom = ProgramROM::new(program); + machine.program_mut().set_program_rom(&rom); + machine.cpu_mut().fp = 0x1000; + machine.cpu_mut().save_register_state(); // TODO: Initial register state should be saved + // automatically by the machine, not manually here + machine.run(&rom, &mut FixedAdviceProvider::empty()); + + type Val = BabyBear; + type Challenge = BinomialExtensionField; + type PackedChallenge = BinomialExtensionField<::Packing, 5>; + + type Mds16 = CosetMds; + let mds16 = Mds16::default(); + + type Perm16 = Poseidon; + let perm16 = Perm16::new_from_rng(4, 22, mds16, &mut thread_rng()); // TODO: Use deterministic RNG + + type MyHash = SerializingHasher32; + let hash = MyHash::new(Keccak256Hash {}); + + type MyCompress = CompressionFunctionFromHasher; + let compress = MyCompress::new(hash); + + type ValMmcs = FieldMerkleTreeMmcs; + let val_mmcs = ValMmcs::new(hash, compress); + + type ChallengeMmcs = ExtensionMmcs; + let challenge_mmcs = ChallengeMmcs::new(val_mmcs.clone()); + + type Dft = Radix2Bowers; + let dft = Dft::default(); + + type Challenger = DuplexChallenger; + + type MyFriConfig = TwoAdicFriPcsConfig; + let fri_config = FriConfig { + log_blowup: 1, + num_queries: 40, + proof_of_work_bits: 8, + mmcs: challenge_mmcs, + }; + + type Pcs = TwoAdicFriPcs; + type MyConfig = StarkConfigImpl; + + let pcs = Pcs::new(fri_config, dft, val_mmcs); + + let challenger = Challenger::new(perm16); + let config = MyConfig::new(pcs, challenger); + let proof = machine.prove(&config); + + let mut bytes = vec![]; + ciborium::into_writer(&proof, &mut bytes).expect("serialization failed"); + println!("Proof size: {} bytes", bytes.len()); + let deserialized_proof: MachineProof = + ciborium::from_reader(bytes.as_slice()).expect("deserialization failed"); + + machine + .verify(&config, &proof) + .expect("verification failed"); + machine + .verify(&config, &deserialized_proof) + .expect("verification failed"); + + assert_eq!(machine.cpu().clock, 192); + assert_eq!(machine.cpu().operations.len(), 192); + assert_eq!(machine.mem().operations.values().flatten().count(), 401); + assert_eq!(machine.add_u32().operations.len(), 105); + + assert_eq!( + *machine.mem().cells.get(&(0x1000 + 4)).unwrap(), // Return value + Word([0, 1, 37, 17,]) // 25th fibonacci number (75025) + ); +} diff --git a/basic_macro/tests/test_static_data.rs b/basic_macro/tests/test_static_data.rs new file mode 100644 index 0000000..6d63046 --- /dev/null +++ b/basic_macro/tests/test_static_data.rs @@ -0,0 +1,113 @@ +extern crate core; + +use p3_baby_bear::BabyBear; +use p3_fri::{TwoAdicFriPcs, TwoAdicFriPcsConfig}; +use valida_basic_macro::BasicMachine; +use valida_cpu::{ + BneInstruction, Imm32Instruction, Load32Instruction, MachineWithCpuChip, StopInstruction, +}; +use valida_machine::{ + FixedAdviceProvider, Instruction, InstructionWord, Machine, Operands, ProgramROM, Word, +}; + +use valida_program::MachineWithProgramChip; +use valida_static_data::MachineWithStaticDataChip; + +use p3_challenger::DuplexChallenger; +use p3_dft::Radix2Bowers; +use p3_field::extension::BinomialExtensionField; +use p3_field::Field; +use p3_fri::FriConfig; +use p3_keccak::Keccak256Hash; +use p3_mds::coset_mds::CosetMds; +use p3_merkle_tree::FieldMerkleTreeMmcs; +use p3_poseidon::Poseidon; +use p3_symmetric::{CompressionFunctionFromHasher, SerializingHasher32}; +use rand::thread_rng; +use valida_machine::StarkConfigImpl; +use valida_machine::__internal::p3_commit::ExtensionMmcs; + +#[test] +fn prove_static_data() { + // _start: + // imm32 0(fp), 0, 0, 0, 0x10 + // load32 -4(fp), 0(fp), 0, 0, 0 + // bnei _start, 0(fp), 0x25, 0, 1 // infinite loop unless static value is loaded + // stop + let program = vec![ + InstructionWord { + opcode: , Val>>::OPCODE, + operands: Operands([0, 0, 0, 0, 0x10]), + }, + InstructionWord { + opcode: , Val>>::OPCODE, + operands: Operands([-4, 0, 0, 0, 0]), + }, + InstructionWord { + opcode: , Val>>::OPCODE, + operands: Operands([0, -4, 0x25, 0, 1]), + }, + InstructionWord { + opcode: , Val>>::OPCODE, + operands: Operands::default(), + }, + ]; + + let mut machine = BasicMachine::::default(); + let rom = ProgramROM::new(program); + machine.static_data_mut().write(0x10, Word([0, 0, 0, 0x25])); + machine.static_data_mut().write(0x14, Word([0, 0, 0, 0x32])); + machine.program_mut().set_program_rom(&rom); + machine.cpu_mut().fp = 0x1000; + machine.cpu_mut().save_register_state(); // TODO: Initial register state should be saved + // automatically by the machine, not manually here + + machine.run(&rom, &mut FixedAdviceProvider::empty()); + + type Val = BabyBear; + type Challenge = BinomialExtensionField; + type PackedChallenge = BinomialExtensionField<::Packing, 5>; + + type Mds16 = CosetMds; + let mds16 = Mds16::default(); + + type Perm16 = Poseidon; + let perm16 = Perm16::new_from_rng(4, 22, mds16, &mut thread_rng()); // TODO: Use deterministic RNG + + type MyHash = SerializingHasher32; + let hash = MyHash::new(Keccak256Hash {}); + + type MyCompress = CompressionFunctionFromHasher; + let compress = MyCompress::new(hash); + + type ValMmcs = FieldMerkleTreeMmcs; + let val_mmcs = ValMmcs::new(hash, compress); + + type ChallengeMmcs = ExtensionMmcs; + let challenge_mmcs = ChallengeMmcs::new(val_mmcs.clone()); + + type Dft = Radix2Bowers; + let dft = Dft::default(); + + type Challenger = DuplexChallenger; + + type MyFriConfig = TwoAdicFriPcsConfig; + let fri_config = FriConfig { + log_blowup: 1, + num_queries: 40, + proof_of_work_bits: 8, + mmcs: challenge_mmcs, + }; + + type Pcs = TwoAdicFriPcs; + type MyConfig = StarkConfigImpl; + + let pcs = Pcs::new(fri_config, dft, val_mmcs); + + let challenger = Challenger::new(perm16); + let config = MyConfig::new(pcs, challenger); + let proof = machine.prove(&config); + machine + .verify(&config, &proof) + .expect("verification failed"); +} From 7bb573fa554df305f03bd96acd5a5b3d8e7cce95 Mon Sep 17 00:00:00 2001 From: Morgan Thomas Date: Sat, 6 Apr 2024 14:52:10 -0400 Subject: [PATCH 04/23] issue/143: remove macros from basic machine --- basic/src/lib.rs | 109 +++++++++++------------------------------------ 1 file changed, 25 insertions(+), 84 deletions(-) diff --git a/basic/src/lib.rs b/basic/src/lib.rs index 6c07d93..3e07a68 100644 --- a/basic/src/lib.rs +++ b/basic/src/lib.rs @@ -38,7 +38,6 @@ use valida_cpu::{ Store32Instruction, }; use valida_cpu::{CpuChip, MachineWithCpuChip}; -use valida_derive::Machine; use valida_machine::{ AdviceProvider, BusArgument, Chip, ChipProof, Instruction, Machine, MachineProof, ProgramROM, ValidaAirBuilder, @@ -52,142 +51,84 @@ use valida_static_data::{MachineWithStaticDataChip, StaticDataChip}; use p3_maybe_rayon::prelude::*; use valida_machine::StarkConfig; -#[derive(Machine, Default)] -#[machine_fields(F)] +#[derive(Default)] pub struct BasicMachine { // Core instructions - #[instruction] load32: Load32Instruction, - - #[instruction] store32: Store32Instruction, - - #[instruction] jal: JalInstruction, - - #[instruction] jalv: JalvInstruction, - - #[instruction] beq: BeqInstruction, - - #[instruction] bne: BneInstruction, - - #[instruction] imm32: Imm32Instruction, - - #[instruction] stop: StopInstruction, - - #[instruction] loadfp: LoadFpInstruction, // ALU instructions - #[instruction(add_u32)] add32: Add32Instruction, - - #[instruction(sub_u32)] sub32: Sub32Instruction, - - #[instruction(mul_u32)] mul32: Mul32Instruction, - - #[instruction(mul_u32)] mulhs32: Mulhs32Instruction, - - #[instruction(mul_u32)] mulhu32: Mulhu32Instruction, - - #[instruction(div_u32)] div32: Div32Instruction, - - #[instruction(div_u32)] sdiv32: SDiv32Instruction, - - #[instruction(shift_u32)] shl32: Shl32Instruction, - - #[instruction(shift_u32)] shr32: Shr32Instruction, - - #[instruction(shift_u32)] sra32: Sra32Instruction, - - #[instruction(lt_u32)] lt32: Lt32Instruction, - - #[instruction(lt_u32)] lte32: Lte32Instruction, - - #[instruction(bitwise_u32)] and32: And32Instruction, - - #[instruction(bitwise_u32)] or32: Or32Instruction, - - #[instruction(bitwise_u32)] xor32: Xor32Instruction, - - #[instruction(com_u32)] ne32: Ne32Instruction, - - #[instruction(com_u32)] eq32: Eq32Instruction, // Input/output instructions - #[instruction] read: ReadAdviceInstruction, - - #[instruction(output)] write: WriteInstruction, - #[chip] + // Chips cpu: CpuChip, - - #[chip] program: ProgramChip, - - #[chip] mem: MemoryChip, - - #[chip] add_u32: Add32Chip, - - #[chip] sub_u32: Sub32Chip, - - #[chip] mul_u32: Mul32Chip, - - #[chip] div_u32: Div32Chip, - - #[chip] shift_u32: Shift32Chip, - - #[chip] lt_u32: Lt32Chip, - - #[chip] com_u32: Com32Chip, - - #[chip] bitwise_u32: Bitwise32Chip, - - #[chip] output: OutputChip, - - #[chip] range: RangeCheckerChip<256>, - - #[chip] - #[static_data_chip] static_data: StaticDataChip, _phantom_sc: PhantomData F>, } +impl Machine for BasicMachine { + fn run(&mut self, program: &ProgramROM, advice: &mut Adv) + where + Adv: AdviceProvider + { + todo!() + } + + fn prove(&self, config: &SC) -> MachineProof + where + SC: StarkConfig + { + todo!() + } + + fn verify(&self, config: &SC, proof: &MachineProof) -> Result<(), ()> + where + SC: StarkConfig + { + todo!() + } +} + impl MachineWithGeneralBus for BasicMachine { fn general_bus(&self) -> BusArgument { BusArgument::Global(0) From c13fadf83e5b1d1b3279c4854bb5e6cc787efc6f Mon Sep 17 00:00:00 2001 From: Morgan Thomas Date: Sat, 6 Apr 2024 14:57:19 -0400 Subject: [PATCH 05/23] issue/143: wip: de-macroify run --- basic/src/lib.rs | 79 +++++++++++++++++++++++++++++++++++++++++++++++- 1 file changed, 78 insertions(+), 1 deletion(-) diff --git a/basic/src/lib.rs b/basic/src/lib.rs index 3e07a68..65b3195 100644 --- a/basic/src/lib.rs +++ b/basic/src/lib.rs @@ -111,7 +111,84 @@ impl Machine for BasicMachine { where Adv: AdviceProvider { - todo!() + self.initialize_memory(); + + loop { + // Fetch + let pc = self.cpu().pc; + let instruction = program.get_instruction(pc); + let opcode = instruction.opcode; + let ops = instruction.operands; + + // Execute + match opcode { + >::OPCODE => + Load32Instruction::execute_with_advice::(self, ops, advice), + >::OPCODE => + Store32Instruction::execute_with_advice::(self, ops, advice), + >::OPCODE => + JalInstruction::execute_with_advice::(self, ops, advice), + >::OPCODE => + JalvInstruction::execute_with_advice::(self, ops, advice), + >::OPCODE => + BeqInstruction::execute_with_advice::(self, ops, advice), + >::OPCODE => + BneInstruction::execute_with_advice::(self, ops, advice), + >::OPCODE => + Imm32Instruction::execute_with_advice::(self, ops, advice), + >::OPCODE => + StopInstruction::execute_with_advice::(self, ops, advice), + >::OPCODE => + LoadFpInstruction::execute_with_advice::(self, ops, advice), + >::OPCODE => + Sub32Instruction::execute_with_advice::(self, ops, advice), + >::OPCODE => + Mul32Instruction::execute_with_advice::(self, ops, advice), + >::OPCODE => + Mulhs32Instruction::execute_with_advice::(self, ops, advice), + >::OPCODE => + Mulhu32Instruction::execute_with_advice::(self, ops, advice), + >::OPCODE => + Div32Instruction::execute_with_advice::(self, ops, advice), + >::OPCODE => + SDiv32Instruction::execute_with_advice::(self, ops, advice), + >::OPCODE => + Shl32Instruction::execute_with_advice::(self, ops, advice), + >::OPCODE => + Shr32Instruction::execute_with_advice::(self, ops, advice), + >::OPCODE => + Lt32Instruction::execute_with_advice::(self, ops, advice), + >::OPCODE => + Lte32Instruction::execute_with_advice::(self, ops, advice), + >::OPCODE => + And32Instruction::execute_with_advice::(self, ops, advice), + >::OPCODE => + Or32Instruction::execute_with_advice::(self, ops, advice), + >::OPCODE => + Xor32Instruction::execute_with_advice::(self, ops, advice), + >::OPCODE => + Ne32Instruction::execute_with_advice::(self, ops, advice), + >::OPCODE => + Eq32Instruction::execute_with_advice::(self, ops, advice), + >::OPCODE => + ReadAdviceInstruction::execute_with_advice::(self, ops, advice), + >::OPCODE => + WriteInstruction::execute_with_advice::(self, ops, advice), + _ => panic!("Unrecognized opcode: {}", opcode), + }; + self.read_word(pc as usize); + + // A STOP instruction signals the end of the program + if opcode == >::OPCODE { + break; + } + } + + // Record padded STOP instructions + let n = self.cpu().clock.next_power_of_two() - self.cpu().clock; + for _ in 0..n { + self.read_word(self.cpu().pc as usize); + } } fn prove(&self, config: &SC) -> MachineProof From ac02d955ac543638a2cc03cd01a9e682e82d873d Mon Sep 17 00:00:00 2001 From: Morgan Thomas Date: Sat, 6 Apr 2024 15:09:48 -0400 Subject: [PATCH 06/23] issue/143: wip: de-macroify prove --- basic/src/lib.rs | 439 +++++++++++++++++++++++++++++++++++++++++++++- derive/src/lib.rs | 4 +- 2 files changed, 436 insertions(+), 7 deletions(-) diff --git a/basic/src/lib.rs b/basic/src/lib.rs index 65b3195..69030b3 100644 --- a/basic/src/lib.rs +++ b/basic/src/lib.rs @@ -3,15 +3,18 @@ extern crate alloc; +use alloc::boxed::Box; +use alloc::vec; use alloc::vec::Vec; use core::marker::PhantomData; use p3_air::Air; use p3_commit::{Pcs, UnivariatePcs, UnivariatePcsWithLde}; -use p3_field::PrimeField32; +use p3_field::{AbstractField, PrimeField32}; use p3_field::{extension::BinomialExtensionField, TwoAdicField}; +use p3_matrix::{Matrix, MatrixRowSlices}; use p3_matrix::dense::RowMajorMatrix; use p3_maybe_rayon::*; -use p3_util::log2_ceil_usize; +use p3_util::{log2_ceil_usize, log2_strict_usize}; use valida_alu_u32::{ add::{Add32Chip, Add32Instruction, MachineWithAdd32Chip}, bitwise::{ @@ -39,9 +42,11 @@ use valida_cpu::{ }; use valida_cpu::{CpuChip, MachineWithCpuChip}; use valida_machine::{ - AdviceProvider, BusArgument, Chip, ChipProof, Instruction, Machine, MachineProof, ProgramROM, - ValidaAirBuilder, + AdviceProvider, BusArgument, Commitments, Chip, ChipProof, Instruction, Machine, MachineProof, OpenedValues, ProgramROM, + ValidaAirBuilder, generate_permutation_trace }; +use valida_machine::__internal::{get_log_quotient_degree, quotient, check_constraints, check_cumulative_sums}; +use valida_machine::__internal::p3_challenger::{CanObserve, FieldChallenger}; use valida_memory::{MachineWithMemoryChip, MemoryChip}; use valida_output::{MachineWithOutputChip, OutputChip, WriteInstruction}; use valida_program::{MachineWithProgramChip, ProgramChip}; @@ -106,6 +111,8 @@ pub struct BasicMachine { _phantom_sc: PhantomData F>, } +const NUM_CHIPS: usize = 14; + impl Machine for BasicMachine { fn run(&mut self, program: &ProgramROM, advice: &mut Adv) where @@ -195,7 +202,429 @@ impl Machine for BasicMachine { where SC: StarkConfig { - todo!() + let mut chips: [Box<&dyn Chip>; NUM_CHIPS] = [ + Box::new(self.cpu()), + Box::new(self.program()), + Box::new(self.mem()), + Box::new(self.add_u32()), + Box::new(self.sub_u32()), + Box::new(self.mul_u32()), + Box::new(self.div_u32()), + Box::new(self.shift_u32()), + Box::new(self.lt_u32()), + Box::new(self.com_u32()), + Box::new(self.bitwise_u32()), + Box::new(self.output()), + Box::new(self.range()), + Box::new(self.static_data()), + ]; + + let log_quotient_degrees: [usize; NUM_CHIPS] = [ + get_log_quotient_degree::(self, self.cpu()), + get_log_quotient_degree::(self, self.program()), + get_log_quotient_degree::(self, self.mem()), + get_log_quotient_degree::(self, self.add_u32()), + get_log_quotient_degree::(self, self.sub_u32()), + get_log_quotient_degree::(self, self.mul_u32()), + get_log_quotient_degree::(self, self.div_u32()), + get_log_quotient_degree::(self, self.shift_u32()), + get_log_quotient_degree::(self, self.lt_u32()), + get_log_quotient_degree::(self, self.com_u32()), + get_log_quotient_degree::(self, self.bitwise_u32()), + get_log_quotient_degree::(self, self.output()), + get_log_quotient_degree::(self, self.range()), + get_log_quotient_degree::(self, self.static_data()), + ]; + + let mut challenger = config.challenger(); + // TODO: Seed challenger with digest of all constraints & trace lengths. + let pcs = config.pcs(); + + let preprocessed_traces: Vec> = + tracing::info_span!("generate preprocessed traces") + .in_scope(|| + chips.par_iter() + .flat_map(|chip| chip.preprocessed_trace()) + .collect::>() + ); + + let (preprocessed_commit, preprocessed_data) = + tracing::info_span!("commit to preprocessed traces") + .in_scope(|| pcs.commit_batches(preprocessed_traces.to_vec())); + challenger.observe(preprocessed_commit.clone()); + let mut preprocessed_trace_ldes = pcs.get_ldes(&preprocessed_data); + + let main_traces: [RowMajorMatrix; NUM_CHIPS] = + tracing::info_span!("generate main trace") + .in_scope(|| + chips.par_iter() + .map(|chip| chip.generate_trace(self)) + .collect::>() + .try_into().unwrap() + ); + + let degrees: [usize; NUM_CHIPS] = main_traces.iter() + .map(|trace| trace.height()) + .collect::>() + .try_into().unwrap(); + let log_degrees = degrees.map(|d| log2_strict_usize(d)); + let g_subgroups = log_degrees.map(|log_deg| SC::Val::two_adic_generator(log_deg)); + + let (main_commit, main_data) = tracing::info_span!("commit to main traces") + .in_scope(|| pcs.commit_batches(main_traces.to_vec())); + challenger.observe(main_commit.clone()); + let mut main_trace_ldes = pcs.get_ldes(&main_data); + + let mut perm_challenges = Vec::new(); + for _ in 0..3 { + perm_challenges.push(challenger.sample_ext_element()); + } + + let perm_traces = tracing::info_span!("generate permutation traces") + .in_scope(|| + chips.into_par_iter().enumerate().map(|(i, chip)| { + generate_permutation_trace(self, *chip, &main_traces[i], perm_challenges.clone()) + }).collect::>() + ); + + let cumulative_sums = perm_traces.iter() + .map(|trace| trace.row_slice(trace.height() - 1).last().unwrap().clone()) + .collect::>(); + + let (perm_commit, perm_data) = tracing::info_span!("commit to permutation traces") + .in_scope(|| { + let flattened_perm_traces = perm_traces.iter() + .map(|trace| trace.flatten_to_base()) + .collect::>(); + pcs.commit_batches(flattened_perm_traces) + }); + challenger.observe(perm_commit.clone()); + let mut perm_trace_ldes = pcs.get_ldes(&perm_data); + + let alpha: SC::Challenge = challenger.sample_ext_element(); + + let mut quotients: Vec> = vec![]; + + let mut i: usize = 0; + + let chip = self.cpu(); + #[cfg(debug_assertions)] + check_constraints::(self, chip, &main_traces[i], &perm_traces[i], &perm_challenges); + quotients.push(quotient( + self, + config, + chip, + log_degrees[i], + None::>, + main_trace_ldes.remove(0), + perm_trace_ldes.remove(0), + cumulative_sums[i], + &perm_challenges, + alpha + )); + i += 1; + + let chip = self.program(); + #[cfg(debug_assertions)] + check_constraints::(self, chip, &main_traces[i], &perm_traces[i], &perm_challenges); + quotients.push(quotient( + self, + config, + chip, + log_degrees[i], + Some(preprocessed_trace_ldes.remove(0)), + main_trace_ldes.remove(0), + perm_trace_ldes.remove(0), + cumulative_sums[i], + &perm_challenges, + alpha + )); + i += 1; + + let chip = self.mem(); + #[cfg(debug_assertions)] + check_constraints::(self, chip, &main_traces[i], &perm_traces[i], &perm_challenges); + quotients.push(quotient( + self, + config, + chip, + log_degrees[i], + None::>, + main_trace_ldes.remove(0), + perm_trace_ldes.remove(0), + cumulative_sums[i], + &perm_challenges, + alpha + )); + i += 1; + + let chip = self.add_u32(); + #[cfg(debug_assertions)] + check_constraints::(self, chip, &main_traces[i], &perm_traces[i], &perm_challenges); + quotients.push(quotient( + self, + config, + chip, + log_degrees[i], + None::>, + main_trace_ldes.remove(0), + perm_trace_ldes.remove(0), + cumulative_sums[i], + &perm_challenges, + alpha + )); + i += 1; + + let chip = self.sub_u32(); + #[cfg(debug_assertions)] + check_constraints::(self, chip, &main_traces[i], &perm_traces[i], &perm_challenges); + quotients.push(quotient( + self, + config, + chip, + log_degrees[i], + None::>, + main_trace_ldes.remove(0), + perm_trace_ldes.remove(0), + cumulative_sums[i], + &perm_challenges, + alpha + )); + i += 1; + + let chip = self.mul_u32(); + #[cfg(debug_assertions)] + check_constraints::(self, chip, &main_traces[i], &perm_traces[i], &perm_challenges); + quotients.push(quotient( + self, + config, + chip, + log_degrees[i], + None::>, + main_trace_ldes.remove(0), + perm_trace_ldes.remove(0), + cumulative_sums[i], + &perm_challenges, + alpha + )); + i += 1; + + let chip = self.div_u32(); + #[cfg(debug_assertions)] + check_constraints::(self, chip, &main_traces[i], &perm_traces[i], &perm_challenges); + quotients.push(quotient( + self, + config, + chip, + log_degrees[i], + None::>, + main_trace_ldes.remove(0), + perm_trace_ldes.remove(0), + cumulative_sums[i], + &perm_challenges, + alpha + )); + i += 1; + + let chip = self.shift_u32(); + #[cfg(debug_assertions)] + check_constraints::(self, chip, &main_traces[i], &perm_traces[i], &perm_challenges); + quotients.push(quotient( + self, + config, + chip, + log_degrees[i], + None::>, + main_trace_ldes.remove(0), + perm_trace_ldes.remove(0), + cumulative_sums[i], + &perm_challenges, + alpha + )); + i += 1; + + let chip = self.lt_u32(); + #[cfg(debug_assertions)] + check_constraints::(self, chip, &main_traces[i], &perm_traces[i], &perm_challenges); + quotients.push(quotient( + self, + config, + chip, + log_degrees[i], + None::>, + main_trace_ldes.remove(0), + perm_trace_ldes.remove(0), + cumulative_sums[i], + &perm_challenges, + alpha + )); + i += 1; + + let chip = self.com_u32(); + #[cfg(debug_assertions)] + check_constraints::(self, chip, &main_traces[i], &perm_traces[i], &perm_challenges); + quotients.push(quotient( + self, + config, + chip, + log_degrees[i], + None::>, + main_trace_ldes.remove(0), + perm_trace_ldes.remove(0), + cumulative_sums[i], + &perm_challenges, + alpha + )); + i += 1; + + let chip = self.bitwise_u32(); + #[cfg(debug_assertions)] + check_constraints::(self, chip, &main_traces[i], &perm_traces[i], &perm_challenges); + quotients.push(quotient( + self, + config, + chip, + log_degrees[i], + None::>, + main_trace_ldes.remove(0), + perm_trace_ldes.remove(0), + cumulative_sums[i], + &perm_challenges, + alpha + )); + i += 1; + + let chip = self.output(); + #[cfg(debug_assertions)] + check_constraints::(self, chip, &main_traces[i], &perm_traces[i], &perm_challenges); + quotients.push(quotient( + self, + config, + chip, + log_degrees[i], + None::>, + main_trace_ldes.remove(0), + perm_trace_ldes.remove(0), + cumulative_sums[i], + &perm_challenges, + alpha + )); + i += 1; + + let chip = self.range(); + #[cfg(debug_assertions)] + check_constraints::(self, chip, &main_traces[i], &perm_traces[i], &perm_challenges); + quotients.push(quotient( + self, + config, + chip, + log_degrees[i], + Some(preprocessed_trace_ldes.remove(0)), + main_trace_ldes.remove(0), + perm_trace_ldes.remove(0), + cumulative_sums[i], + &perm_challenges, + alpha + )); + i += 1; + + let chip = self.static_data(); + #[cfg(debug_assertions)] + check_constraints::(self, chip, &main_traces[i], &perm_traces[i], &perm_challenges); + quotients.push(quotient( + self, + config, + chip, + log_degrees[i], + Some(preprocessed_trace_ldes.remove(0)), + main_trace_ldes.remove(0), + perm_trace_ldes.remove(0), + cumulative_sums[i], + &perm_challenges, + alpha + )); + i += 1; + + assert_eq!(quotients.len(), NUM_CHIPS); + assert_eq!(log_quotient_degrees.len(), NUM_CHIPS); + let coset_shifts = tracing::debug_span!("coset shift").in_scope(|| { + let pcs_coset_shift = pcs.coset_shift(); + log_quotient_degrees.map(|log_d| pcs_coset_shift.exp_power_of_2(log_d)) + }); + assert_eq!(coset_shifts.len(), NUM_CHIPS); + let (quotient_commit, quotient_data) = tracing::info_span!("commit to quotient chunks") + .in_scope(|| pcs.commit_shifted_batches(quotients.to_vec(), &coset_shifts)); + + challenger.observe(quotient_commit.clone()); + + #[cfg(debug_assertions)] + check_cumulative_sums(&perm_traces[..]); + + let zeta: SC::Challenge = challenger.sample_ext_element(); + let zeta_and_next: [Vec; NUM_CHIPS] = + g_subgroups.map(|g| vec![zeta, zeta * g]); + let zeta_exp_quotient_degree: [Vec; NUM_CHIPS] = + log_quotient_degrees.map(|log_deg| vec![zeta.exp_power_of_2(log_deg)]); + let prover_data_and_points = [ + // TODO: Causes some errors, probably related to the fact that not all chips have preprocessed traces? + // (&preprocessed_data, zeta_and_next.as_slice()), + (&main_data, zeta_and_next.as_slice()), + (&perm_data, zeta_and_next.as_slice()), + ("ient_data, zeta_exp_quotient_degree.as_slice()), + ]; + let (openings, opening_proof) = pcs.open_multi_batches( + &prover_data_and_points, &mut challenger); + + // TODO: add preprocessed openings + let [main_openings, perm_openings, quotient_openings] = + openings.try_into().expect("Should have 3 rounds of openings"); + + let commitments = Commitments { + main_trace: main_commit, + perm_trace: perm_commit, + quotient_chunks: quotient_commit, + }; + + // TODO: add preprocessed openings + let chip_proofs = log_degrees + .iter() + .zip(main_openings) + .zip(perm_openings) + .zip(quotient_openings) + .zip(perm_traces) + .map(|((((log_degree, main), perm), quotient), perm_trace)| { + // TODO: add preprocessed openings + let [preprocessed_local, preprocessed_next] = + [vec![], vec![]]; + + let [main_local, main_next] = main.try_into().expect("Should have 2 openings"); + let [perm_local, perm_next] = perm.try_into().expect("Should have 2 openings"); + let [quotient_chunks] = quotient.try_into().expect("Should have 1 opening"); + + let opened_values = OpenedValues { + preprocessed_local, + preprocessed_next, + trace_local: main_local, + trace_next: main_next, + permutation_local: perm_local, + permutation_next: perm_next, + quotient_chunks, + }; + + let cumulative_sum = perm_trace.row_slice(perm_trace.height() - 1).last().unwrap().clone(); + ChipProof { + log_degree: *log_degree, + opened_values, + cumulative_sum, + } + }) + .collect::>(); + + MachineProof { + commitments, + opening_proof, + chip_proofs, + } } fn verify(&self, config: &SC, proof: &MachineProof) -> Result<(), ()> diff --git a/derive/src/lib.rs b/derive/src/lib.rs index ba8dc38..680fad4 100644 --- a/derive/src/lib.rs +++ b/derive/src/lib.rs @@ -250,7 +250,7 @@ fn prove_method(chips: &[&Field]) -> TokenStream2 { preprocessed_trace_lde, main_trace_ldes.remove(0), perm_trace_ldes.remove(0), - cummulative_sums[#i], + cumulative_sums[#i], &perm_challenges, alpha, )); @@ -329,7 +329,7 @@ fn prove_method(chips: &[&Field]) -> TokenStream2 { }).collect::>() ); - let cummulative_sums = perm_traces.iter() + let cumulative_sums = perm_traces.iter() .map(|trace| trace.row_slice(trace.height() - 1).last().unwrap().clone()) .collect::>(); From 5c90dd1cfb305db2ec50397479b086b0879bedd3 Mon Sep 17 00:00:00 2001 From: Morgan Thomas Date: Sat, 6 Apr 2024 19:18:54 -0400 Subject: [PATCH 07/23] issue/143: wip: de-macroify verify --- basic/src/lib.rs | 386 +++++++++++++++++++++++++++++++++++++++++++++- derive/src/lib.rs | 18 +-- 2 files changed, 390 insertions(+), 14 deletions(-) diff --git a/basic/src/lib.rs b/basic/src/lib.rs index 69030b3..c4a6bf4 100644 --- a/basic/src/lib.rs +++ b/basic/src/lib.rs @@ -4,14 +4,15 @@ extern crate alloc; use alloc::boxed::Box; +use alloc::format; use alloc::vec; use alloc::vec::Vec; use core::marker::PhantomData; use p3_air::Air; use p3_commit::{Pcs, UnivariatePcs, UnivariatePcsWithLde}; -use p3_field::{AbstractField, PrimeField32}; +use p3_field::{AbstractField, AbstractExtensionField, PrimeField32}; use p3_field::{extension::BinomialExtensionField, TwoAdicField}; -use p3_matrix::{Matrix, MatrixRowSlices}; +use p3_matrix::{Matrix, Dimensions, MatrixRowSlices}; use p3_matrix::dense::RowMajorMatrix; use p3_maybe_rayon::*; use p3_util::{log2_ceil_usize, log2_strict_usize}; @@ -43,7 +44,7 @@ use valida_cpu::{ use valida_cpu::{CpuChip, MachineWithCpuChip}; use valida_machine::{ AdviceProvider, BusArgument, Commitments, Chip, ChipProof, Instruction, Machine, MachineProof, OpenedValues, ProgramROM, - ValidaAirBuilder, generate_permutation_trace + ValidaAirBuilder, generate_permutation_trace, verify_constraints }; use valida_machine::__internal::{get_log_quotient_degree, quotient, check_constraints, check_cumulative_sums}; use valida_machine::__internal::p3_challenger::{CanObserve, FieldChallenger}; @@ -631,7 +632,384 @@ impl Machine for BasicMachine { where SC: StarkConfig { - todo!() + let mut chips: [Box<&dyn Chip>; NUM_CHIPS] = [ + Box::new(self.cpu()), + Box::new(self.program()), + Box::new(self.mem()), + Box::new(self.add_u32()), + Box::new(self.sub_u32()), + Box::new(self.mul_u32()), + Box::new(self.div_u32()), + Box::new(self.shift_u32()), + Box::new(self.lt_u32()), + Box::new(self.com_u32()), + Box::new(self.bitwise_u32()), + Box::new(self.output()), + Box::new(self.range()), + Box::new(self.static_data()), + ]; + + let log_quotient_degrees: [usize; NUM_CHIPS] = [ + get_log_quotient_degree::(self, self.cpu()), + get_log_quotient_degree::(self, self.program()), + get_log_quotient_degree::(self, self.mem()), + get_log_quotient_degree::(self, self.add_u32()), + get_log_quotient_degree::(self, self.sub_u32()), + get_log_quotient_degree::(self, self.mul_u32()), + get_log_quotient_degree::(self, self.div_u32()), + get_log_quotient_degree::(self, self.shift_u32()), + get_log_quotient_degree::(self, self.lt_u32()), + get_log_quotient_degree::(self, self.com_u32()), + get_log_quotient_degree::(self, self.bitwise_u32()), + get_log_quotient_degree::(self, self.output()), + get_log_quotient_degree::(self, self.range()), + get_log_quotient_degree::(self, self.static_data()), + ]; + + let mut challenger = config.challenger(); + // TODO: Seed challenger with digest of all constraints & trace lengths. + let pcs = config.pcs(); + + let chips_interactions = chips + .iter() + .map(|chip| chip.all_interactions(self)) + .collect::>(); + + let dims = &[ + chips + .iter() + .zip(proof.chip_proofs.iter()) + .map(|(chip, chip_proof)| Dimensions { + width: chip.trace_width(), + height: 1 << chip_proof.log_degree, + }) + .collect::>(), + chips_interactions.iter() + .zip(proof.chip_proofs.iter()) + .map(|(interactions, chip_proof)| Dimensions { + width: (interactions.len() + 1) * SC::Challenge::D, + height: 1 << chip_proof.log_degree, + }) + .collect::>(), + proof.chip_proofs.iter() + .zip(log_quotient_degrees) + .map(|(chip_proof, log_quotient_deg)| Dimensions { + width: log_quotient_deg << SC::Challenge::D, + height: 1 << chip_proof.log_degree, + }) + .collect::>(), + ]; + + // Get the generators of the trace subgroups for each chip. + let g_subgroups: [SC::Val; NUM_CHIPS] = proof.chip_proofs + .iter() + .map(|chip_proof| SC::Val::two_adic_generator(chip_proof.log_degree)) + .collect::>().try_into().unwrap(); + + // TODO: maybe avoid cloning opened values (not sure if possible) + let mut main_values = vec![]; + let mut perm_values = vec![]; + let mut quotient_values = vec![]; + + for chip_proof in proof.chip_proofs.iter() { + let OpenedValues { + preprocessed_local, + preprocessed_next, + trace_local, + trace_next, + permutation_local, + permutation_next, + quotient_chunks, + } = &chip_proof.opened_values; + + main_values.push(vec![trace_local.clone(), trace_next.clone()]); + perm_values.push(vec![permutation_local.clone(), permutation_next.clone()]); + quotient_values.push(vec![quotient_chunks.clone()]); + } + + let chips_opening_values = vec![main_values, perm_values, quotient_values]; + + // Observe commitments and get challenges. + let Commitments { + main_trace, + perm_trace, + quotient_chunks, + } = &proof.commitments; + + // Compute the commitments to preprocessed traces (TODO: avoid in the future) + let preprocessed_traces: Vec> = + tracing::info_span!("generate preprocessed traces") + .in_scope(|| + chips.par_iter() + .flat_map(|chip| chip.preprocessed_trace()) + .collect::>() + ); + + let (preprocessed_commit, preprocessed_data) = + tracing::info_span!("commit to preprocessed traces") + .in_scope(|| pcs.commit_batches(preprocessed_traces.to_vec())); + + challenger.observe(preprocessed_commit.clone()); + + challenger.observe(main_trace.clone()); + + let mut perm_challenges = Vec::new(); + for _ in 0..3 { + perm_challenges.push(challenger.sample_ext_element::()); + } + + challenger.observe(perm_trace.clone()); + + let alpha = challenger.sample_ext_element::(); + + challenger.observe(quotient_chunks.clone()); + + // Verify the opening proof. + let zeta: SC::Challenge = challenger.sample_ext_element(); + let zeta_and_next: [Vec; NUM_CHIPS] = + g_subgroups.map(|g| vec![zeta, zeta * g]); + let zeta_exp_quotient_degree: [Vec; NUM_CHIPS] = + log_quotient_degrees.map(|log_deg| vec![zeta.exp_power_of_2(log_deg)]); + pcs + .verify_multi_batches( + &[ + // TODO: add preprocessed trace + (main_trace.clone(), zeta_and_next.as_slice()), + (perm_trace.clone(), zeta_and_next.as_slice()), + (quotient_chunks.clone(), zeta_exp_quotient_degree.as_slice()), + ], + dims, + chips_opening_values, + &proof.opening_proof, + &mut challenger, + ) + .map_err(|_| ())?; + + // Verify the constraints. + let mut i = 0; + + let chip = self.cpu(); + verify_constraints::( + self, + chip, + &proof.chip_proofs[i].opened_values, + proof.chip_proofs[i].cumulative_sum, + proof.chip_proofs[i].log_degree, + g_subgroups[i], + zeta, + alpha, + &perm_challenges + ).expect(&format!("Failed to verify constraints on chip {}", i)); + i += 1; + + let chip = self.program(); + verify_constraints::( + self, + chip, + &proof.chip_proofs[i].opened_values, + proof.chip_proofs[i].cumulative_sum, + proof.chip_proofs[i].log_degree, + g_subgroups[i], + zeta, + alpha, + &perm_challenges + ).expect(&format!("Failed to verify constraints on chip {}", i)); + i += 1; + + let chip = self.mem(); + verify_constraints::( + self, + chip, + &proof.chip_proofs[i].opened_values, + proof.chip_proofs[i].cumulative_sum, + proof.chip_proofs[i].log_degree, + g_subgroups[i], + zeta, + alpha, + &perm_challenges + ).expect(&format!("Failed to verify constraints on chip {}", i)); + i += 1; + + let chip = self.add_u32(); + verify_constraints::( + self, + chip, + &proof.chip_proofs[i].opened_values, + proof.chip_proofs[i].cumulative_sum, + proof.chip_proofs[i].log_degree, + g_subgroups[i], + zeta, + alpha, + &perm_challenges + ).expect(&format!("Failed to verify constraints on chip {}", i)); + i += 1; + + let chip = self.sub_u32(); + verify_constraints::( + self, + chip, + &proof.chip_proofs[i].opened_values, + proof.chip_proofs[i].cumulative_sum, + proof.chip_proofs[i].log_degree, + g_subgroups[i], + zeta, + alpha, + &perm_challenges + ).expect(&format!("Failed to verify constraints on chip {}", i)); + i += 1; + + let chip = self.mul_u32(); + verify_constraints::( + self, + chip, + &proof.chip_proofs[i].opened_values, + proof.chip_proofs[i].cumulative_sum, + proof.chip_proofs[i].log_degree, + g_subgroups[i], + zeta, + alpha, + &perm_challenges + ).expect(&format!("Failed to verify constraints on chip {}", i)); + i += 1; + + let chip = self.div_u32(); + verify_constraints::( + self, + chip, + &proof.chip_proofs[i].opened_values, + proof.chip_proofs[i].cumulative_sum, + proof.chip_proofs[i].log_degree, + g_subgroups[i], + zeta, + alpha, + &perm_challenges + ).expect(&format!("Failed to verify constraints on chip {}", i)); + i += 1; + + let chip = self.div_u32(); + verify_constraints::( + self, + chip, + &proof.chip_proofs[i].opened_values, + proof.chip_proofs[i].cumulative_sum, + proof.chip_proofs[i].log_degree, + g_subgroups[i], + zeta, + alpha, + &perm_challenges + ).expect(&format!("Failed to verify constraints on chip {}", i)); + i += 1; + + let chip = self.shift_u32(); + verify_constraints::( + self, + chip, + &proof.chip_proofs[i].opened_values, + proof.chip_proofs[i].cumulative_sum, + proof.chip_proofs[i].log_degree, + g_subgroups[i], + zeta, + alpha, + &perm_challenges + ).expect(&format!("Failed to verify constraints on chip {}", i)); + i += 1; + + let chip = self.lt_u32(); + verify_constraints::( + self, + chip, + &proof.chip_proofs[i].opened_values, + proof.chip_proofs[i].cumulative_sum, + proof.chip_proofs[i].log_degree, + g_subgroups[i], + zeta, + alpha, + &perm_challenges + ).expect(&format!("Failed to verify constraints on chip {}", i)); + i += 1; + + let chip = self.com_u32(); + verify_constraints::( + self, + chip, + &proof.chip_proofs[i].opened_values, + proof.chip_proofs[i].cumulative_sum, + proof.chip_proofs[i].log_degree, + g_subgroups[i], + zeta, + alpha, + &perm_challenges + ).expect(&format!("Failed to verify constraints on chip {}", i)); + i += 1; + + let chip = self.bitwise_u32(); + verify_constraints::( + self, + chip, + &proof.chip_proofs[i].opened_values, + proof.chip_proofs[i].cumulative_sum, + proof.chip_proofs[i].log_degree, + g_subgroups[i], + zeta, + alpha, + &perm_challenges + ).expect(&format!("Failed to verify constraints on chip {}", i)); + i += 1; + + let chip = self.output(); + verify_constraints::( + self, + chip, + &proof.chip_proofs[i].opened_values, + proof.chip_proofs[i].cumulative_sum, + proof.chip_proofs[i].log_degree, + g_subgroups[i], + zeta, + alpha, + &perm_challenges + ).expect(&format!("Failed to verify constraints on chip {}", i)); + i += 1; + + let chip = self.range(); + verify_constraints::( + self, + chip, + &proof.chip_proofs[i].opened_values, + proof.chip_proofs[i].cumulative_sum, + proof.chip_proofs[i].log_degree, + g_subgroups[i], + zeta, + alpha, + &perm_challenges + ).expect(&format!("Failed to verify constraints on chip {}", i)); + i += 1; + + let chip = self.static_data(); + verify_constraints::( + self, + chip, + &proof.chip_proofs[i].opened_values, + proof.chip_proofs[i].cumulative_sum, + proof.chip_proofs[i].log_degree, + g_subgroups[i], + zeta, + alpha, + &perm_challenges + ).expect(&format!("Failed to verify constraints on chip {}", i)); + i += 1; + + // Verify that the cumulative_sum sums add up to zero. + let sum: SC::Challenge = proof + .chip_proofs + .iter() + .map(|chip_proof| chip_proof.cumulative_sum) + .sum(); + + if sum != SC::Challenge::zero() { + return Err(()); + } + + Ok(()) } } diff --git a/derive/src/lib.rs b/derive/src/lib.rs index 680fad4..ec8ba45 100644 --- a/derive/src/lib.rs +++ b/derive/src/lib.rs @@ -534,7 +534,7 @@ fn verify_method(chips: &[&Field]) -> TokenStream2 { ]; // Get the generators of the trace subgroups for each chip. - let g_subgroups :[SC::Val ; #num_chips] = proof.chip_proofs + let g_subgroups: [SC::Val; #num_chips] = proof.chip_proofs .iter() .map(|chip_proof| SC::Val::two_adic_generator(chip_proof.log_degree)) .collect::>().try_into().unwrap(); @@ -562,7 +562,6 @@ fn verify_method(chips: &[&Field]) -> TokenStream2 { let chips_opening_values = vec![main_values, perm_values, quotient_values]; - // Observe commitments and get challenges. let Commitments { main_trace, @@ -570,7 +569,6 @@ fn verify_method(chips: &[&Field]) -> TokenStream2 { quotient_chunks, } = &proof.commitments; - // Compute the commitments to preprocessed traces (TODO: avoid in the future) let preprocessed_traces: Vec> = tracing::info_span!("generate preprocessed traces") @@ -586,7 +584,6 @@ fn verify_method(chips: &[&Field]) -> TokenStream2 { challenger.observe(preprocessed_commit.clone()); - // challenger.observe(preprocessed_commit.clone()); challenger.observe(main_trace.clone()); let mut perm_challenges = Vec::new(); @@ -600,15 +597,16 @@ fn verify_method(chips: &[&Field]) -> TokenStream2 { challenger.observe(quotient_chunks.clone()); - // Verify the openning proof. - let zeta: SC::Challenge = challenger.sample_ext_element(); - let zeta_and_next: [Vec; #num_chips] = - g_subgroups.map(|g| vec![zeta, zeta * g]); - let zeta_exp_quotient_degree: [Vec; #num_chips] = - log_quotient_degrees.map(|log_deg| vec![zeta.exp_power_of_2(log_deg)]); + // Verify the opening proof. + let zeta: SC::Challenge = challenger.sample_ext_element(); + let zeta_and_next: [Vec; #num_chips] = + g_subgroups.map(|g| vec![zeta, zeta * g]); + let zeta_exp_quotient_degree: [Vec; #num_chips] = + log_quotient_degrees.map(|log_deg| vec![zeta.exp_power_of_2(log_deg)]); pcs .verify_multi_batches( &[ + // TODO: add preprocessed trace (main_trace.clone(), zeta_and_next.as_slice()), (perm_trace.clone(), zeta_and_next.as_slice()), (quotient_chunks.clone(), zeta_exp_quotient_degree.as_slice()), From b71d2aea62797b0c248d65d9036b7eef6e378250 Mon Sep 17 00:00:00 2001 From: Morgan Thomas Date: Sat, 6 Apr 2024 19:44:47 -0400 Subject: [PATCH 08/23] issue/143: bugfixes --- basic/src/lib.rs | 18 +++--------------- 1 file changed, 3 insertions(+), 15 deletions(-) diff --git a/basic/src/lib.rs b/basic/src/lib.rs index c4a6bf4..5ad3fd5 100644 --- a/basic/src/lib.rs +++ b/basic/src/lib.rs @@ -148,6 +148,8 @@ impl Machine for BasicMachine { StopInstruction::execute_with_advice::(self, ops, advice), >::OPCODE => LoadFpInstruction::execute_with_advice::(self, ops, advice), + >::OPCODE => + Add32Instruction::execute_with_advice::(self, ops, advice), >::OPCODE => Sub32Instruction::execute_with_advice::(self, ops, advice), >::OPCODE => @@ -537,7 +539,7 @@ impl Machine for BasicMachine { config, chip, log_degrees[i], - Some(preprocessed_trace_ldes.remove(0)), + None::>, main_trace_ldes.remove(0), perm_trace_ldes.remove(0), cumulative_sums[i], @@ -886,20 +888,6 @@ impl Machine for BasicMachine { ).expect(&format!("Failed to verify constraints on chip {}", i)); i += 1; - let chip = self.div_u32(); - verify_constraints::( - self, - chip, - &proof.chip_proofs[i].opened_values, - proof.chip_proofs[i].cumulative_sum, - proof.chip_proofs[i].log_degree, - g_subgroups[i], - zeta, - alpha, - &perm_challenges - ).expect(&format!("Failed to verify constraints on chip {}", i)); - i += 1; - let chip = self.shift_u32(); verify_constraints::( self, From 1c51e9c4a683f13f3598c6dfa02f84f0365544b0 Mon Sep 17 00:00:00 2001 From: Morgan Thomas Date: Sat, 6 Apr 2024 19:49:02 -0400 Subject: [PATCH 09/23] issue/143: cargo fmt --- basic/src/lib.rs | 505 ++++++++++++++++++++++++++++++----------------- 1 file changed, 327 insertions(+), 178 deletions(-) diff --git a/basic/src/lib.rs b/basic/src/lib.rs index 5ad3fd5..050c13d 100644 --- a/basic/src/lib.rs +++ b/basic/src/lib.rs @@ -10,10 +10,10 @@ use alloc::vec::Vec; use core::marker::PhantomData; use p3_air::Air; use p3_commit::{Pcs, UnivariatePcs, UnivariatePcsWithLde}; -use p3_field::{AbstractField, AbstractExtensionField, PrimeField32}; use p3_field::{extension::BinomialExtensionField, TwoAdicField}; -use p3_matrix::{Matrix, Dimensions, MatrixRowSlices}; +use p3_field::{AbstractExtensionField, AbstractField, PrimeField32}; use p3_matrix::dense::RowMajorMatrix; +use p3_matrix::{Dimensions, Matrix, MatrixRowSlices}; use p3_maybe_rayon::*; use p3_util::{log2_ceil_usize, log2_strict_usize}; use valida_alu_u32::{ @@ -42,12 +42,14 @@ use valida_cpu::{ Store32Instruction, }; use valida_cpu::{CpuChip, MachineWithCpuChip}; +use valida_machine::__internal::p3_challenger::{CanObserve, FieldChallenger}; +use valida_machine::__internal::{ + check_constraints, check_cumulative_sums, get_log_quotient_degree, quotient, +}; use valida_machine::{ - AdviceProvider, BusArgument, Commitments, Chip, ChipProof, Instruction, Machine, MachineProof, OpenedValues, ProgramROM, - ValidaAirBuilder, generate_permutation_trace, verify_constraints + generate_permutation_trace, verify_constraints, AdviceProvider, BusArgument, Chip, ChipProof, + Commitments, Instruction, Machine, MachineProof, OpenedValues, ProgramROM, ValidaAirBuilder, }; -use valida_machine::__internal::{get_log_quotient_degree, quotient, check_constraints, check_cumulative_sums}; -use valida_machine::__internal::p3_challenger::{CanObserve, FieldChallenger}; use valida_memory::{MachineWithMemoryChip, MemoryChip}; use valida_output::{MachineWithOutputChip, OutputChip, WriteInstruction}; use valida_program::{MachineWithProgramChip, ProgramChip}; @@ -117,7 +119,7 @@ const NUM_CHIPS: usize = 14; impl Machine for BasicMachine { fn run(&mut self, program: &ProgramROM, advice: &mut Adv) where - Adv: AdviceProvider + Adv: AdviceProvider, { self.initialize_memory(); @@ -130,60 +132,87 @@ impl Machine for BasicMachine { // Execute match opcode { - >::OPCODE => - Load32Instruction::execute_with_advice::(self, ops, advice), - >::OPCODE => - Store32Instruction::execute_with_advice::(self, ops, advice), - >::OPCODE => - JalInstruction::execute_with_advice::(self, ops, advice), - >::OPCODE => - JalvInstruction::execute_with_advice::(self, ops, advice), - >::OPCODE => - BeqInstruction::execute_with_advice::(self, ops, advice), - >::OPCODE => - BneInstruction::execute_with_advice::(self, ops, advice), - >::OPCODE => - Imm32Instruction::execute_with_advice::(self, ops, advice), - >::OPCODE => - StopInstruction::execute_with_advice::(self, ops, advice), - >::OPCODE => - LoadFpInstruction::execute_with_advice::(self, ops, advice), - >::OPCODE => - Add32Instruction::execute_with_advice::(self, ops, advice), - >::OPCODE => - Sub32Instruction::execute_with_advice::(self, ops, advice), - >::OPCODE => - Mul32Instruction::execute_with_advice::(self, ops, advice), - >::OPCODE => - Mulhs32Instruction::execute_with_advice::(self, ops, advice), - >::OPCODE => - Mulhu32Instruction::execute_with_advice::(self, ops, advice), - >::OPCODE => - Div32Instruction::execute_with_advice::(self, ops, advice), - >::OPCODE => - SDiv32Instruction::execute_with_advice::(self, ops, advice), - >::OPCODE => - Shl32Instruction::execute_with_advice::(self, ops, advice), - >::OPCODE => - Shr32Instruction::execute_with_advice::(self, ops, advice), - >::OPCODE => - Lt32Instruction::execute_with_advice::(self, ops, advice), - >::OPCODE => - Lte32Instruction::execute_with_advice::(self, ops, advice), - >::OPCODE => - And32Instruction::execute_with_advice::(self, ops, advice), - >::OPCODE => - Or32Instruction::execute_with_advice::(self, ops, advice), - >::OPCODE => - Xor32Instruction::execute_with_advice::(self, ops, advice), - >::OPCODE => - Ne32Instruction::execute_with_advice::(self, ops, advice), - >::OPCODE => - Eq32Instruction::execute_with_advice::(self, ops, advice), - >::OPCODE => - ReadAdviceInstruction::execute_with_advice::(self, ops, advice), - >::OPCODE => - WriteInstruction::execute_with_advice::(self, ops, advice), + >::OPCODE => { + Load32Instruction::execute_with_advice::(self, ops, advice) + } + >::OPCODE => { + Store32Instruction::execute_with_advice::(self, ops, advice) + } + >::OPCODE => { + JalInstruction::execute_with_advice::(self, ops, advice) + } + >::OPCODE => { + JalvInstruction::execute_with_advice::(self, ops, advice) + } + >::OPCODE => { + BeqInstruction::execute_with_advice::(self, ops, advice) + } + >::OPCODE => { + BneInstruction::execute_with_advice::(self, ops, advice) + } + >::OPCODE => { + Imm32Instruction::execute_with_advice::(self, ops, advice) + } + >::OPCODE => { + StopInstruction::execute_with_advice::(self, ops, advice) + } + >::OPCODE => { + LoadFpInstruction::execute_with_advice::(self, ops, advice) + } + >::OPCODE => { + Add32Instruction::execute_with_advice::(self, ops, advice) + } + >::OPCODE => { + Sub32Instruction::execute_with_advice::(self, ops, advice) + } + >::OPCODE => { + Mul32Instruction::execute_with_advice::(self, ops, advice) + } + >::OPCODE => { + Mulhs32Instruction::execute_with_advice::(self, ops, advice) + } + >::OPCODE => { + Mulhu32Instruction::execute_with_advice::(self, ops, advice) + } + >::OPCODE => { + Div32Instruction::execute_with_advice::(self, ops, advice) + } + >::OPCODE => { + SDiv32Instruction::execute_with_advice::(self, ops, advice) + } + >::OPCODE => { + Shl32Instruction::execute_with_advice::(self, ops, advice) + } + >::OPCODE => { + Shr32Instruction::execute_with_advice::(self, ops, advice) + } + >::OPCODE => { + Lt32Instruction::execute_with_advice::(self, ops, advice) + } + >::OPCODE => { + Lte32Instruction::execute_with_advice::(self, ops, advice) + } + >::OPCODE => { + And32Instruction::execute_with_advice::(self, ops, advice) + } + >::OPCODE => { + Or32Instruction::execute_with_advice::(self, ops, advice) + } + >::OPCODE => { + Xor32Instruction::execute_with_advice::(self, ops, advice) + } + >::OPCODE => { + Ne32Instruction::execute_with_advice::(self, ops, advice) + } + >::OPCODE => { + Eq32Instruction::execute_with_advice::(self, ops, advice) + } + >::OPCODE => { + ReadAdviceInstruction::execute_with_advice::(self, ops, advice) + } + >::OPCODE => { + WriteInstruction::execute_with_advice::(self, ops, advice) + } _ => panic!("Unrecognized opcode: {}", opcode), }; self.read_word(pc as usize); @@ -203,7 +232,7 @@ impl Machine for BasicMachine { fn prove(&self, config: &SC) -> MachineProof where - SC: StarkConfig + SC: StarkConfig, { let mut chips: [Box<&dyn Chip>; NUM_CHIPS] = [ Box::new(self.cpu()), @@ -244,12 +273,12 @@ impl Machine for BasicMachine { let pcs = config.pcs(); let preprocessed_traces: Vec> = - tracing::info_span!("generate preprocessed traces") - .in_scope(|| - chips.par_iter() - .flat_map(|chip| chip.preprocessed_trace()) - .collect::>() - ); + tracing::info_span!("generate preprocessed traces").in_scope(|| { + chips + .par_iter() + .flat_map(|chip| chip.preprocessed_trace()) + .collect::>() + }); let (preprocessed_commit, preprocessed_data) = tracing::info_span!("commit to preprocessed traces") @@ -258,18 +287,21 @@ impl Machine for BasicMachine { let mut preprocessed_trace_ldes = pcs.get_ldes(&preprocessed_data); let main_traces: [RowMajorMatrix; NUM_CHIPS] = - tracing::info_span!("generate main trace") - .in_scope(|| - chips.par_iter() - .map(|chip| chip.generate_trace(self)) - .collect::>() - .try_into().unwrap() - ); - - let degrees: [usize; NUM_CHIPS] = main_traces.iter() + tracing::info_span!("generate main trace").in_scope(|| { + chips + .par_iter() + .map(|chip| chip.generate_trace(self)) + .collect::>() + .try_into() + .unwrap() + }); + + let degrees: [usize; NUM_CHIPS] = main_traces + .iter() .map(|trace| trace.height()) .collect::>() - .try_into().unwrap(); + .try_into() + .unwrap(); let log_degrees = degrees.map(|d| log2_strict_usize(d)); let g_subgroups = log_degrees.map(|log_deg| SC::Val::two_adic_generator(log_deg)); @@ -283,20 +315,30 @@ impl Machine for BasicMachine { perm_challenges.push(challenger.sample_ext_element()); } - let perm_traces = tracing::info_span!("generate permutation traces") - .in_scope(|| - chips.into_par_iter().enumerate().map(|(i, chip)| { - generate_permutation_trace(self, *chip, &main_traces[i], perm_challenges.clone()) - }).collect::>() - ); + let perm_traces = tracing::info_span!("generate permutation traces").in_scope(|| { + chips + .into_par_iter() + .enumerate() + .map(|(i, chip)| { + generate_permutation_trace( + self, + *chip, + &main_traces[i], + perm_challenges.clone(), + ) + }) + .collect::>() + }); - let cumulative_sums = perm_traces.iter() + let cumulative_sums = perm_traces + .iter() .map(|trace| trace.row_slice(trace.height() - 1).last().unwrap().clone()) .collect::>(); let (perm_commit, perm_data) = tracing::info_span!("commit to permutation traces") .in_scope(|| { - let flattened_perm_traces = perm_traces.iter() + let flattened_perm_traces = perm_traces + .iter() .map(|trace| trace.flatten_to_base()) .collect::>(); pcs.commit_batches(flattened_perm_traces) @@ -312,7 +354,13 @@ impl Machine for BasicMachine { let chip = self.cpu(); #[cfg(debug_assertions)] - check_constraints::(self, chip, &main_traces[i], &perm_traces[i], &perm_challenges); + check_constraints::( + self, + chip, + &main_traces[i], + &perm_traces[i], + &perm_challenges, + ); quotients.push(quotient( self, config, @@ -323,13 +371,19 @@ impl Machine for BasicMachine { perm_trace_ldes.remove(0), cumulative_sums[i], &perm_challenges, - alpha + alpha, )); i += 1; let chip = self.program(); #[cfg(debug_assertions)] - check_constraints::(self, chip, &main_traces[i], &perm_traces[i], &perm_challenges); + check_constraints::( + self, + chip, + &main_traces[i], + &perm_traces[i], + &perm_challenges, + ); quotients.push(quotient( self, config, @@ -340,13 +394,19 @@ impl Machine for BasicMachine { perm_trace_ldes.remove(0), cumulative_sums[i], &perm_challenges, - alpha + alpha, )); i += 1; let chip = self.mem(); #[cfg(debug_assertions)] - check_constraints::(self, chip, &main_traces[i], &perm_traces[i], &perm_challenges); + check_constraints::( + self, + chip, + &main_traces[i], + &perm_traces[i], + &perm_challenges, + ); quotients.push(quotient( self, config, @@ -357,13 +417,19 @@ impl Machine for BasicMachine { perm_trace_ldes.remove(0), cumulative_sums[i], &perm_challenges, - alpha + alpha, )); i += 1; let chip = self.add_u32(); #[cfg(debug_assertions)] - check_constraints::(self, chip, &main_traces[i], &perm_traces[i], &perm_challenges); + check_constraints::( + self, + chip, + &main_traces[i], + &perm_traces[i], + &perm_challenges, + ); quotients.push(quotient( self, config, @@ -374,13 +440,19 @@ impl Machine for BasicMachine { perm_trace_ldes.remove(0), cumulative_sums[i], &perm_challenges, - alpha + alpha, )); i += 1; let chip = self.sub_u32(); #[cfg(debug_assertions)] - check_constraints::(self, chip, &main_traces[i], &perm_traces[i], &perm_challenges); + check_constraints::( + self, + chip, + &main_traces[i], + &perm_traces[i], + &perm_challenges, + ); quotients.push(quotient( self, config, @@ -391,13 +463,19 @@ impl Machine for BasicMachine { perm_trace_ldes.remove(0), cumulative_sums[i], &perm_challenges, - alpha + alpha, )); i += 1; let chip = self.mul_u32(); #[cfg(debug_assertions)] - check_constraints::(self, chip, &main_traces[i], &perm_traces[i], &perm_challenges); + check_constraints::( + self, + chip, + &main_traces[i], + &perm_traces[i], + &perm_challenges, + ); quotients.push(quotient( self, config, @@ -408,13 +486,19 @@ impl Machine for BasicMachine { perm_trace_ldes.remove(0), cumulative_sums[i], &perm_challenges, - alpha + alpha, )); i += 1; let chip = self.div_u32(); #[cfg(debug_assertions)] - check_constraints::(self, chip, &main_traces[i], &perm_traces[i], &perm_challenges); + check_constraints::( + self, + chip, + &main_traces[i], + &perm_traces[i], + &perm_challenges, + ); quotients.push(quotient( self, config, @@ -425,13 +509,19 @@ impl Machine for BasicMachine { perm_trace_ldes.remove(0), cumulative_sums[i], &perm_challenges, - alpha + alpha, )); i += 1; let chip = self.shift_u32(); #[cfg(debug_assertions)] - check_constraints::(self, chip, &main_traces[i], &perm_traces[i], &perm_challenges); + check_constraints::( + self, + chip, + &main_traces[i], + &perm_traces[i], + &perm_challenges, + ); quotients.push(quotient( self, config, @@ -442,13 +532,19 @@ impl Machine for BasicMachine { perm_trace_ldes.remove(0), cumulative_sums[i], &perm_challenges, - alpha + alpha, )); i += 1; let chip = self.lt_u32(); #[cfg(debug_assertions)] - check_constraints::(self, chip, &main_traces[i], &perm_traces[i], &perm_challenges); + check_constraints::( + self, + chip, + &main_traces[i], + &perm_traces[i], + &perm_challenges, + ); quotients.push(quotient( self, config, @@ -459,13 +555,19 @@ impl Machine for BasicMachine { perm_trace_ldes.remove(0), cumulative_sums[i], &perm_challenges, - alpha + alpha, )); i += 1; let chip = self.com_u32(); #[cfg(debug_assertions)] - check_constraints::(self, chip, &main_traces[i], &perm_traces[i], &perm_challenges); + check_constraints::( + self, + chip, + &main_traces[i], + &perm_traces[i], + &perm_challenges, + ); quotients.push(quotient( self, config, @@ -476,13 +578,19 @@ impl Machine for BasicMachine { perm_trace_ldes.remove(0), cumulative_sums[i], &perm_challenges, - alpha + alpha, )); i += 1; let chip = self.bitwise_u32(); #[cfg(debug_assertions)] - check_constraints::(self, chip, &main_traces[i], &perm_traces[i], &perm_challenges); + check_constraints::( + self, + chip, + &main_traces[i], + &perm_traces[i], + &perm_challenges, + ); quotients.push(quotient( self, config, @@ -493,13 +601,19 @@ impl Machine for BasicMachine { perm_trace_ldes.remove(0), cumulative_sums[i], &perm_challenges, - alpha + alpha, )); i += 1; let chip = self.output(); #[cfg(debug_assertions)] - check_constraints::(self, chip, &main_traces[i], &perm_traces[i], &perm_challenges); + check_constraints::( + self, + chip, + &main_traces[i], + &perm_traces[i], + &perm_challenges, + ); quotients.push(quotient( self, config, @@ -510,13 +624,19 @@ impl Machine for BasicMachine { perm_trace_ldes.remove(0), cumulative_sums[i], &perm_challenges, - alpha + alpha, )); i += 1; let chip = self.range(); #[cfg(debug_assertions)] - check_constraints::(self, chip, &main_traces[i], &perm_traces[i], &perm_challenges); + check_constraints::( + self, + chip, + &main_traces[i], + &perm_traces[i], + &perm_challenges, + ); quotients.push(quotient( self, config, @@ -527,24 +647,30 @@ impl Machine for BasicMachine { perm_trace_ldes.remove(0), cumulative_sums[i], &perm_challenges, - alpha + alpha, )); i += 1; let chip = self.static_data(); #[cfg(debug_assertions)] - check_constraints::(self, chip, &main_traces[i], &perm_traces[i], &perm_challenges); + check_constraints::( + self, + chip, + &main_traces[i], + &perm_traces[i], + &perm_challenges, + ); quotients.push(quotient( self, config, chip, log_degrees[i], - None::>, + None::>, main_trace_ldes.remove(0), perm_trace_ldes.remove(0), cumulative_sums[i], &perm_challenges, - alpha + alpha, )); i += 1; @@ -575,12 +701,13 @@ impl Machine for BasicMachine { (&perm_data, zeta_and_next.as_slice()), ("ient_data, zeta_exp_quotient_degree.as_slice()), ]; - let (openings, opening_proof) = pcs.open_multi_batches( - &prover_data_and_points, &mut challenger); + let (openings, opening_proof) = + pcs.open_multi_batches(&prover_data_and_points, &mut challenger); // TODO: add preprocessed openings - let [main_openings, perm_openings, quotient_openings] = - openings.try_into().expect("Should have 3 rounds of openings"); + let [main_openings, perm_openings, quotient_openings] = openings + .try_into() + .expect("Should have 3 rounds of openings"); let commitments = Commitments { main_trace: main_commit, @@ -595,10 +722,9 @@ impl Machine for BasicMachine { .zip(perm_openings) .zip(quotient_openings) .zip(perm_traces) - .map(|((((log_degree, main), perm), quotient), perm_trace)| { + .map(|((((log_degree, main), perm), quotient), perm_trace)| { // TODO: add preprocessed openings - let [preprocessed_local, preprocessed_next] = - [vec![], vec![]]; + let [preprocessed_local, preprocessed_next] = [vec![], vec![]]; let [main_local, main_next] = main.try_into().expect("Should have 2 openings"); let [perm_local, perm_next] = perm.try_into().expect("Should have 2 openings"); @@ -614,7 +740,11 @@ impl Machine for BasicMachine { quotient_chunks, }; - let cumulative_sum = perm_trace.row_slice(perm_trace.height() - 1).last().unwrap().clone(); + let cumulative_sum = perm_trace + .row_slice(perm_trace.height() - 1) + .last() + .unwrap() + .clone(); ChipProof { log_degree: *log_degree, opened_values, @@ -632,7 +762,7 @@ impl Machine for BasicMachine { fn verify(&self, config: &SC, proof: &MachineProof) -> Result<(), ()> where - SC: StarkConfig + SC: StarkConfig, { let mut chips: [Box<&dyn Chip>; NUM_CHIPS] = [ Box::new(self.cpu()), @@ -673,9 +803,9 @@ impl Machine for BasicMachine { let pcs = config.pcs(); let chips_interactions = chips - .iter() - .map(|chip| chip.all_interactions(self)) - .collect::>(); + .iter() + .map(|chip| chip.all_interactions(self)) + .collect::>(); let dims = &[ chips @@ -686,14 +816,17 @@ impl Machine for BasicMachine { height: 1 << chip_proof.log_degree, }) .collect::>(), - chips_interactions.iter() - .zip(proof.chip_proofs.iter()) + chips_interactions + .iter() + .zip(proof.chip_proofs.iter()) .map(|(interactions, chip_proof)| Dimensions { width: (interactions.len() + 1) * SC::Challenge::D, height: 1 << chip_proof.log_degree, }) .collect::>(), - proof.chip_proofs.iter() + proof + .chip_proofs + .iter() .zip(log_quotient_degrees) .map(|(chip_proof, log_quotient_deg)| Dimensions { width: log_quotient_deg << SC::Challenge::D, @@ -703,10 +836,13 @@ impl Machine for BasicMachine { ]; // Get the generators of the trace subgroups for each chip. - let g_subgroups: [SC::Val; NUM_CHIPS] = proof.chip_proofs + let g_subgroups: [SC::Val; NUM_CHIPS] = proof + .chip_proofs .iter() .map(|chip_proof| SC::Val::two_adic_generator(chip_proof.log_degree)) - .collect::>().try_into().unwrap(); + .collect::>() + .try_into() + .unwrap(); // TODO: maybe avoid cloning opened values (not sure if possible) let mut main_values = vec![]; @@ -740,12 +876,12 @@ impl Machine for BasicMachine { // Compute the commitments to preprocessed traces (TODO: avoid in the future) let preprocessed_traces: Vec> = - tracing::info_span!("generate preprocessed traces") - .in_scope(|| - chips.par_iter() + tracing::info_span!("generate preprocessed traces").in_scope(|| { + chips + .par_iter() .flat_map(|chip| chip.preprocessed_trace()) .collect::>() - ); + }); let (preprocessed_commit, preprocessed_data) = tracing::info_span!("commit to preprocessed traces") @@ -772,20 +908,19 @@ impl Machine for BasicMachine { g_subgroups.map(|g| vec![zeta, zeta * g]); let zeta_exp_quotient_degree: [Vec; NUM_CHIPS] = log_quotient_degrees.map(|log_deg| vec![zeta.exp_power_of_2(log_deg)]); - pcs - .verify_multi_batches( - &[ - // TODO: add preprocessed trace - (main_trace.clone(), zeta_and_next.as_slice()), - (perm_trace.clone(), zeta_and_next.as_slice()), - (quotient_chunks.clone(), zeta_exp_quotient_degree.as_slice()), - ], - dims, - chips_opening_values, - &proof.opening_proof, - &mut challenger, - ) - .map_err(|_| ())?; + pcs.verify_multi_batches( + &[ + // TODO: add preprocessed trace + (main_trace.clone(), zeta_and_next.as_slice()), + (perm_trace.clone(), zeta_and_next.as_slice()), + (quotient_chunks.clone(), zeta_exp_quotient_degree.as_slice()), + ], + dims, + chips_opening_values, + &proof.opening_proof, + &mut challenger, + ) + .map_err(|_| ())?; // Verify the constraints. let mut i = 0; @@ -800,8 +935,9 @@ impl Machine for BasicMachine { g_subgroups[i], zeta, alpha, - &perm_challenges - ).expect(&format!("Failed to verify constraints on chip {}", i)); + &perm_challenges, + ) + .expect(&format!("Failed to verify constraints on chip {}", i)); i += 1; let chip = self.program(); @@ -814,8 +950,9 @@ impl Machine for BasicMachine { g_subgroups[i], zeta, alpha, - &perm_challenges - ).expect(&format!("Failed to verify constraints on chip {}", i)); + &perm_challenges, + ) + .expect(&format!("Failed to verify constraints on chip {}", i)); i += 1; let chip = self.mem(); @@ -828,8 +965,9 @@ impl Machine for BasicMachine { g_subgroups[i], zeta, alpha, - &perm_challenges - ).expect(&format!("Failed to verify constraints on chip {}", i)); + &perm_challenges, + ) + .expect(&format!("Failed to verify constraints on chip {}", i)); i += 1; let chip = self.add_u32(); @@ -842,8 +980,9 @@ impl Machine for BasicMachine { g_subgroups[i], zeta, alpha, - &perm_challenges - ).expect(&format!("Failed to verify constraints on chip {}", i)); + &perm_challenges, + ) + .expect(&format!("Failed to verify constraints on chip {}", i)); i += 1; let chip = self.sub_u32(); @@ -856,8 +995,9 @@ impl Machine for BasicMachine { g_subgroups[i], zeta, alpha, - &perm_challenges - ).expect(&format!("Failed to verify constraints on chip {}", i)); + &perm_challenges, + ) + .expect(&format!("Failed to verify constraints on chip {}", i)); i += 1; let chip = self.mul_u32(); @@ -870,8 +1010,9 @@ impl Machine for BasicMachine { g_subgroups[i], zeta, alpha, - &perm_challenges - ).expect(&format!("Failed to verify constraints on chip {}", i)); + &perm_challenges, + ) + .expect(&format!("Failed to verify constraints on chip {}", i)); i += 1; let chip = self.div_u32(); @@ -884,8 +1025,9 @@ impl Machine for BasicMachine { g_subgroups[i], zeta, alpha, - &perm_challenges - ).expect(&format!("Failed to verify constraints on chip {}", i)); + &perm_challenges, + ) + .expect(&format!("Failed to verify constraints on chip {}", i)); i += 1; let chip = self.shift_u32(); @@ -898,8 +1040,9 @@ impl Machine for BasicMachine { g_subgroups[i], zeta, alpha, - &perm_challenges - ).expect(&format!("Failed to verify constraints on chip {}", i)); + &perm_challenges, + ) + .expect(&format!("Failed to verify constraints on chip {}", i)); i += 1; let chip = self.lt_u32(); @@ -912,8 +1055,9 @@ impl Machine for BasicMachine { g_subgroups[i], zeta, alpha, - &perm_challenges - ).expect(&format!("Failed to verify constraints on chip {}", i)); + &perm_challenges, + ) + .expect(&format!("Failed to verify constraints on chip {}", i)); i += 1; let chip = self.com_u32(); @@ -926,8 +1070,9 @@ impl Machine for BasicMachine { g_subgroups[i], zeta, alpha, - &perm_challenges - ).expect(&format!("Failed to verify constraints on chip {}", i)); + &perm_challenges, + ) + .expect(&format!("Failed to verify constraints on chip {}", i)); i += 1; let chip = self.bitwise_u32(); @@ -940,8 +1085,9 @@ impl Machine for BasicMachine { g_subgroups[i], zeta, alpha, - &perm_challenges - ).expect(&format!("Failed to verify constraints on chip {}", i)); + &perm_challenges, + ) + .expect(&format!("Failed to verify constraints on chip {}", i)); i += 1; let chip = self.output(); @@ -954,8 +1100,9 @@ impl Machine for BasicMachine { g_subgroups[i], zeta, alpha, - &perm_challenges - ).expect(&format!("Failed to verify constraints on chip {}", i)); + &perm_challenges, + ) + .expect(&format!("Failed to verify constraints on chip {}", i)); i += 1; let chip = self.range(); @@ -968,8 +1115,9 @@ impl Machine for BasicMachine { g_subgroups[i], zeta, alpha, - &perm_challenges - ).expect(&format!("Failed to verify constraints on chip {}", i)); + &perm_challenges, + ) + .expect(&format!("Failed to verify constraints on chip {}", i)); i += 1; let chip = self.static_data(); @@ -982,8 +1130,9 @@ impl Machine for BasicMachine { g_subgroups[i], zeta, alpha, - &perm_challenges - ).expect(&format!("Failed to verify constraints on chip {}", i)); + &perm_challenges, + ) + .expect(&format!("Failed to verify constraints on chip {}", i)); i += 1; // Verify that the cumulative_sum sums add up to zero. From 4e16400ea5397f5bbc976a14517a455aff39f94e Mon Sep 17 00:00:00 2001 From: Morgan Thomas Date: Sat, 6 Apr 2024 19:53:30 -0400 Subject: [PATCH 10/23] issue/143: remove no_std from basic_macro lib (is breaking ci?) --- basic_macro/src/lib.rs | 1 - 1 file changed, 1 deletion(-) diff --git a/basic_macro/src/lib.rs b/basic_macro/src/lib.rs index 6c07d93..e7522e0 100644 --- a/basic_macro/src/lib.rs +++ b/basic_macro/src/lib.rs @@ -1,4 +1,3 @@ -#![no_std] #![allow(unused)] extern crate alloc; From 8314901fe373675abe750f9340f82dbf94913729 Mon Sep 17 00:00:00 2001 From: Morgan Thomas Date: Tue, 9 Apr 2024 12:05:10 -0400 Subject: [PATCH 11/23] issue/143: fix merge --- Cargo.lock | 486 +++++++++++++++++++++++++++++++++++++++- basic/src/bin/valida.rs | 47 ++-- basic/src/lib.rs | 203 +++++++++-------- basic_macro/src/lib.rs | 2 +- derive/src/lib.rs | 43 +--- machine/src/machine.rs | 5 +- 6 files changed, 621 insertions(+), 165 deletions(-) diff --git a/Cargo.lock b/Cargo.lock index f1b1caa..81874cc 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -11,6 +11,21 @@ dependencies = [ "memchr", ] +[[package]] +name = "android-tzdata" +version = "0.1.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "e999941b234f3131b00bc13c22d06e8c5ff726d1b6318ac7eb276997bbb4fef0" + +[[package]] +name = "android_system_properties" +version = "0.1.5" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "819e7219dbd41043ac279b19830f2efc897156490d7fd6ea916720117ee66311" +dependencies = [ + "libc", +] + [[package]] name = "anes" version = "0.1.6" @@ -52,7 +67,7 @@ version = "1.0.2" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "e28923312444cdd728e4738b3f9c9cac739500909bb3d3c94b43551b16517648" dependencies = [ - "windows-sys", + "windows-sys 0.52.0", ] [[package]] @@ -62,7 +77,7 @@ source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "1cd54b81ec8d6180e24654d0b371ad22fc3dd083b6ff8ba325b72e00c87660a7" dependencies = [ "anstyle", - "windows-sys", + "windows-sys 0.52.0", ] [[package]] @@ -71,6 +86,21 @@ version = "1.1.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "d468802bab17cbc0cc575e9b053f41e72aa36bfa6b7f55e3529ffa43161b97fa" +[[package]] +name = "bitflags" +version = "1.3.2" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "bef38d45163c2f1dde094a7dfd33ccf595c92905c8f8f4fdc18d06fb1037718a" + +[[package]] +name = "bitflags" +version = "2.5.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "cf4b9d6a944f767f8e5e0db018570623c85f3d925ac718db4e06d0187adb21c1" +dependencies = [ + "serde", +] + [[package]] name = "block-buffer" version = "0.10.4" @@ -98,12 +128,31 @@ version = "0.3.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "37b2a672a2cb129a2e41c10b1224bb368f9f37a2b16b612598138befd7b37eb5" +[[package]] +name = "cc" +version = "1.0.92" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "2678b2e3449475e95b0aa6f9b506a28e61b3dc8996592b983695e8ebb58a8b41" + [[package]] name = "cfg-if" version = "1.0.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "baf1de4339761588bc0619e3cbc0120ee582ebb74b53b4efbf79117bd2da40fd" +[[package]] +name = "chrono" +version = "0.4.37" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "8a0d04d43504c61aa6c7531f1871dd0d418d91130162063b789da00fd7057a5e" +dependencies = [ + "android-tzdata", + "iana-time-zone", + "num-traits", + "serde", + "windows-targets 0.52.4", +] + [[package]] name = "ciborium" version = "0.2.2" @@ -177,6 +226,12 @@ version = "1.0.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "acbf1af155f9b9ef647e42cdc158db4b64a1b61f743629225fde6f3e0be2a7c7" +[[package]] +name = "core-foundation-sys" +version = "0.8.6" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "06ea2b9bc92be3c2baa9334a323ebca2d6f074ff852cd1d7b11064035cd3868f" + [[package]] name = "cpufeatures" version = "0.2.12" @@ -222,6 +277,28 @@ dependencies = [ "itertools 0.10.5", ] +[[package]] +name = "crossbeam" +version = "0.8.4" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "1137cd7e7fc0fb5d3c5a8678be38ec56e819125d8d7907411fe24ccb943faca8" +dependencies = [ + "crossbeam-channel", + "crossbeam-deque", + "crossbeam-epoch", + "crossbeam-queue", + "crossbeam-utils", +] + +[[package]] +name = "crossbeam-channel" +version = "0.5.12" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "ab3db02a9c5b5121e1e42fbdb1aeb65f5e02624cc58c43f2884c6ccac0b82f95" +dependencies = [ + "crossbeam-utils", +] + [[package]] name = "crossbeam-deque" version = "0.8.5" @@ -241,12 +318,47 @@ dependencies = [ "crossbeam-utils", ] +[[package]] +name = "crossbeam-queue" +version = "0.3.11" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "df0346b5d5e76ac2fe4e327c5fd1118d6be7c51dfb18f9b7922923f287471e35" +dependencies = [ + "crossbeam-utils", +] + [[package]] name = "crossbeam-utils" version = "0.8.19" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "248e3bacc7dc6baa3b21e405ee045c3047101a49145e7e9eca583ab4c2ca5345" +[[package]] +name = "crossterm" +version = "0.27.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "f476fe445d41c9e991fd07515a6f463074b782242ccf4a5b7b1d1012e70824df" +dependencies = [ + "bitflags 2.5.0", + "crossterm_winapi", + "libc", + "mio", + "parking_lot", + "serde", + "signal-hook", + "signal-hook-mio", + "winapi", +] + +[[package]] +name = "crossterm_winapi" +version = "0.9.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "acdd7c62a3665c7f6830a51635d9ac9b23ed385797f70a83bb8bafe9c572ab2b" +dependencies = [ + "winapi", +] + [[package]] name = "crunchy" version = "0.2.2" @@ -285,6 +397,27 @@ version = "0.7.4" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "4445909572dbd556c457c849c4ca58623d84b27c8fff1e74b0b4227d8b90d17b" +[[package]] +name = "errno" +version = "0.3.8" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "a258e46cdc063eb8519c00b9fc845fc47bcfca4130e2f08e88665ceda8474245" +dependencies = [ + "libc", + "windows-sys 0.52.0", +] + +[[package]] +name = "fd-lock" +version = "3.0.13" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "ef033ed5e9bad94e55838ca0ca906db0e043f517adda0c8b79c7a8c66c93c1b5" +dependencies = [ + "cfg-if", + "rustix", + "windows-sys 0.48.0", +] + [[package]] name = "generic-array" version = "0.14.7" @@ -328,6 +461,29 @@ version = "0.3.9" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "d231dfb89cfffdbc30e7fc41579ed6066ad03abda9e567ccafae602b97ec5024" +[[package]] +name = "iana-time-zone" +version = "0.1.60" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "e7ffbb5a1b541ea2561f8c41c087286cc091e21e556a4f09a8f6cbf17b69b141" +dependencies = [ + "android_system_properties", + "core-foundation-sys", + "iana-time-zone-haiku", + "js-sys", + "wasm-bindgen", + "windows-core", +] + +[[package]] +name = "iana-time-zone-haiku" +version = "0.1.2" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "f31827a206f56af32e590ba56d5d2d085f558508192593743f16b2306495269f" +dependencies = [ + "cc", +] + [[package]] name = "is-terminal" version = "0.4.12" @@ -336,7 +492,7 @@ checksum = "f23ff5ef2b80d608d61efee834934d862cd92461afc0560dedf493e4c033738b" dependencies = [ "hermit-abi", "libc", - "windows-sys", + "windows-sys 0.52.0", ] [[package]] @@ -378,6 +534,22 @@ version = "0.2.153" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "9c198f91728a82281a64e1f4f9eeb25d82cb32a5de251c6bd1b5154d63a8e7bd" +[[package]] +name = "linux-raw-sys" +version = "0.4.13" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "01cda141df6706de531b6c46c3a33ecca755538219bd484262fa09410c13539c" + +[[package]] +name = "lock_api" +version = "0.4.11" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "3c168f8615b12bc01f9c17e2eb0cc07dcae1940121185446edc3744920e8ef45" +dependencies = [ + "autocfg", + "scopeguard", +] + [[package]] name = "log" version = "0.4.21" @@ -390,6 +562,27 @@ version = "2.7.1" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "523dc4f511e55ab87b694dc30d0f820d60906ef06413f93d4d7a1385599cc149" +[[package]] +name = "mio" +version = "0.8.11" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "a4a650543ca06a924e8b371db273b2756685faae30f8487da1b56505a8f78b0c" +dependencies = [ + "libc", + "log", + "wasi", + "windows-sys 0.48.0", +] + +[[package]] +name = "nu-ansi-term" +version = "0.50.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "dd2800e1520bdc966782168a627aa5d1ad92e33b984bf7c7615d31280c83ff14" +dependencies = [ + "windows-sys 0.48.0", +] + [[package]] name = "num-traits" version = "0.2.18" @@ -633,6 +826,29 @@ dependencies = [ "serde", ] +[[package]] +name = "parking_lot" +version = "0.12.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "3742b2c103b9f06bc9fff0a37ff4912935851bee6d36f3c02bcc755bcfec228f" +dependencies = [ + "lock_api", + "parking_lot_core", +] + +[[package]] +name = "parking_lot_core" +version = "0.9.9" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "4c42a9226546d68acdd9c0a280d17ce19bfe27a46bf68784e4066115788d008e" +dependencies = [ + "cfg-if", + "libc", + "redox_syscall", + "smallvec", + "windows-targets 0.48.5", +] + [[package]] name = "pest" version = "2.7.8" @@ -804,6 +1020,51 @@ dependencies = [ "crossbeam-utils", ] +[[package]] +name = "redox_syscall" +version = "0.4.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "4722d768eff46b75989dd134e5c353f0d6296e5aaa3132e776cbdb56be7731aa" +dependencies = [ + "bitflags 1.3.2", +] + +[[package]] +name = "reedline" +version = "0.30.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "413a9fa6a5d8c937d3ae1e975bfb6a918bb0b6cdfae6a10416218c837a31b8fc" +dependencies = [ + "chrono", + "crossbeam", + "crossterm", + "fd-lock", + "itertools 0.12.1", + "nu-ansi-term", + "serde", + "strip-ansi-escapes", + "strum", + "strum_macros", + "thiserror", + "unicode-segmentation", + "unicode-width", +] + +[[package]] +name = "reedline-repl-rs" +version = "1.1.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "28f19046a23d5c9f988b6677868024009a60e82676d5cd3b4c52d7557db680eb" +dependencies = [ + "clap", + "crossterm", + "nu-ansi-term", + "reedline", + "regex", + "winapi-util", + "yansi", +] + [[package]] name = "regex" version = "1.10.3" @@ -833,6 +1094,25 @@ version = "0.8.2" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "c08c74e62047bb2de4ff487b251e4a92e24f48745648451635cec7d591162d9f" +[[package]] +name = "rustix" +version = "0.38.32" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "65e04861e65f21776e67888bfbea442b3642beaa0138fdb1dd7a84a52dffdb89" +dependencies = [ + "bitflags 2.5.0", + "errno", + "libc", + "linux-raw-sys", + "windows-sys 0.52.0", +] + +[[package]] +name = "rustversion" +version = "1.0.15" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "80af6f9131f277a45a3fba6ce8e2258037bb0477a67e610d3c1fe046ab31de47" + [[package]] name = "ryu" version = "1.0.17" @@ -848,6 +1128,12 @@ dependencies = [ "winapi-util", ] +[[package]] +name = "scopeguard" +version = "1.2.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "94143f37725109f92c262ed2cf5e59bce7498c01bcc1502d7b9afe439a4e9f49" + [[package]] name = "serde" version = "1.0.197" @@ -890,12 +1176,76 @@ dependencies = [ "digest", ] +[[package]] +name = "signal-hook" +version = "0.3.17" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "8621587d4798caf8eb44879d42e56b9a93ea5dcd315a6487c357130095b62801" +dependencies = [ + "libc", + "signal-hook-registry", +] + +[[package]] +name = "signal-hook-mio" +version = "0.2.3" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "29ad2e15f37ec9a6cc544097b78a1ec90001e9f71b81338ca39f430adaca99af" +dependencies = [ + "libc", + "mio", + "signal-hook", +] + +[[package]] +name = "signal-hook-registry" +version = "1.4.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "d8229b473baa5980ac72ef434c4415e70c4b5e71b423043adb4ba059f89c99a1" +dependencies = [ + "libc", +] + +[[package]] +name = "smallvec" +version = "1.13.2" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "3c5e1a9a646d36c3599cd173a41282daf47c44583ad367b8e6837255952e5c67" + +[[package]] +name = "strip-ansi-escapes" +version = "0.2.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "55ff8ef943b384c414f54aefa961dd2bd853add74ec75e7ac74cf91dba62bcfa" +dependencies = [ + "vte", +] + [[package]] name = "strsim" version = "0.11.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "5ee073c9e4cd00e28217186dbe12796d692868f432bf2e97ee73bed0c56dfa01" +[[package]] +name = "strum" +version = "0.25.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "290d54ea6f91c969195bdbcd7442c8c2a2ba87da8bf60a7ee86a235d4bc1e125" + +[[package]] +name = "strum_macros" +version = "0.25.3" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "23dc1fa9ac9c169a78ba62f0b841814b7abae11bdd047b9c58f893439e309ea0" +dependencies = [ + "heck", + "proc-macro2", + "quote", + "rustversion", + "syn 2.0.52", +] + [[package]] name = "syn" version = "1.0.109" @@ -1006,6 +1356,18 @@ version = "1.0.12" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "3354b9ac3fae1ff6755cb6db53683adb661634f67557942dea4facebec0fee4b" +[[package]] +name = "unicode-segmentation" +version = "1.11.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "d4c87d22b6e3f4a18d4d40ef354e97c90fcb14dd91d7dc0aa9d8a1172ebf7202" + +[[package]] +name = "unicode-width" +version = "0.1.11" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "e51733f11c9c4f72aa0c160008246859e340b00807569a0da0e7a1079b27ba85" + [[package]] name = "utf8parse" version = "0.2.1" @@ -1073,6 +1435,7 @@ dependencies = [ "rand", "rand_pcg", "rand_seeder", + "reedline-repl-rs", "tracing", "valida-alu-u32", "valida-assembler", @@ -1324,6 +1687,26 @@ version = "0.9.4" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "49874b5167b65d7193b8aba1567f5c7d93d001cafc34600cee003eda787e483f" +[[package]] +name = "vte" +version = "0.11.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "f5022b5fbf9407086c180e9557be968742d839e68346af7792b8592489732197" +dependencies = [ + "utf8parse", + "vte_generate_state_changes", +] + +[[package]] +name = "vte_generate_state_changes" +version = "0.1.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "d257817081c7dffcdbab24b9e62d2def62e2ff7d00b1c20062551e6cccc145ff" +dependencies = [ + "proc-macro2", + "quote", +] + [[package]] name = "walkdir" version = "2.5.0" @@ -1435,13 +1818,46 @@ version = "0.4.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "712e227841d057c1ee1cd2fb22fa7e5a5461ae8e48fa2ca79ec42cfc1931183f" +[[package]] +name = "windows-core" +version = "0.52.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "33ab640c8d7e35bf8ba19b884ba838ceb4fba93a4e8c65a9059d08afcfc683d9" +dependencies = [ + "windows-targets 0.52.4", +] + +[[package]] +name = "windows-sys" +version = "0.48.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "677d2418bec65e3338edb076e806bc1ec15693c5d0104683f2efe857f61056a9" +dependencies = [ + "windows-targets 0.48.5", +] + [[package]] name = "windows-sys" version = "0.52.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "282be5f36a8ce781fad8c8ae18fa3f9beff57ec1b52cb3de0789201425d9a33d" dependencies = [ - "windows-targets", + "windows-targets 0.52.4", +] + +[[package]] +name = "windows-targets" +version = "0.48.5" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "9a2fa6e2155d7247be68c096456083145c183cbbbc2764150dda45a87197940c" +dependencies = [ + "windows_aarch64_gnullvm 0.48.5", + "windows_aarch64_msvc 0.48.5", + "windows_i686_gnu 0.48.5", + "windows_i686_msvc 0.48.5", + "windows_x86_64_gnu 0.48.5", + "windows_x86_64_gnullvm 0.48.5", + "windows_x86_64_msvc 0.48.5", ] [[package]] @@ -1450,53 +1866,101 @@ version = "0.52.4" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "7dd37b7e5ab9018759f893a1952c9420d060016fc19a472b4bb20d1bdd694d1b" dependencies = [ - "windows_aarch64_gnullvm", - "windows_aarch64_msvc", - "windows_i686_gnu", - "windows_i686_msvc", - "windows_x86_64_gnu", - "windows_x86_64_gnullvm", - "windows_x86_64_msvc", + "windows_aarch64_gnullvm 0.52.4", + "windows_aarch64_msvc 0.52.4", + "windows_i686_gnu 0.52.4", + "windows_i686_msvc 0.52.4", + "windows_x86_64_gnu 0.52.4", + "windows_x86_64_gnullvm 0.52.4", + "windows_x86_64_msvc 0.52.4", ] +[[package]] +name = "windows_aarch64_gnullvm" +version = "0.48.5" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "2b38e32f0abccf9987a4e3079dfb67dcd799fb61361e53e2882c3cbaf0d905d8" + [[package]] name = "windows_aarch64_gnullvm" version = "0.52.4" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "bcf46cf4c365c6f2d1cc93ce535f2c8b244591df96ceee75d8e83deb70a9cac9" +[[package]] +name = "windows_aarch64_msvc" +version = "0.48.5" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "dc35310971f3b2dbbf3f0690a219f40e2d9afcf64f9ab7cc1be722937c26b4bc" + [[package]] name = "windows_aarch64_msvc" version = "0.52.4" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "da9f259dd3bcf6990b55bffd094c4f7235817ba4ceebde8e6d11cd0c5633b675" +[[package]] +name = "windows_i686_gnu" +version = "0.48.5" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "a75915e7def60c94dcef72200b9a8e58e5091744960da64ec734a6c6e9b3743e" + [[package]] name = "windows_i686_gnu" version = "0.52.4" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "b474d8268f99e0995f25b9f095bc7434632601028cf86590aea5c8a5cb7801d3" +[[package]] +name = "windows_i686_msvc" +version = "0.48.5" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "8f55c233f70c4b27f66c523580f78f1004e8b5a8b659e05a4eb49d4166cca406" + [[package]] name = "windows_i686_msvc" version = "0.52.4" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "1515e9a29e5bed743cb4415a9ecf5dfca648ce85ee42e15873c3cd8610ff8e02" +[[package]] +name = "windows_x86_64_gnu" +version = "0.48.5" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "53d40abd2583d23e4718fddf1ebec84dbff8381c07cae67ff7768bbf19c6718e" + [[package]] name = "windows_x86_64_gnu" version = "0.52.4" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "5eee091590e89cc02ad514ffe3ead9eb6b660aedca2183455434b93546371a03" +[[package]] +name = "windows_x86_64_gnullvm" +version = "0.48.5" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "0b7b52767868a23d5bab768e390dc5f5c55825b6d30b86c844ff2dc7414044cc" + [[package]] name = "windows_x86_64_gnullvm" version = "0.52.4" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "77ca79f2451b49fa9e2af39f0747fe999fcda4f5e241b2898624dca97a1f2177" +[[package]] +name = "windows_x86_64_msvc" +version = "0.48.5" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "ed94fce61571a4006852b7389a063ab983c02eb1bb37b47f8272ce92d06d9538" + [[package]] name = "windows_x86_64_msvc" version = "0.52.4" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "32b752e52a2da0ddfbdbcc6fceadfeede4c939ed16d13e648833a61dfb611ed8" + +[[package]] +name = "yansi" +version = "1.0.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "cfe53a6657fd280eaa890a3bc59152892ffa3e30101319d168b781ed6529b049" diff --git a/basic/src/bin/valida.rs b/basic/src/bin/valida.rs index 0687f3b..b616ace 100644 --- a/basic/src/bin/valida.rs +++ b/basic/src/bin/valida.rs @@ -9,7 +9,7 @@ use p3_baby_bear::BabyBear; use p3_fri::{FriConfig, TwoAdicFriPcs, TwoAdicFriPcsConfig}; use valida_cpu::MachineWithCpuChip; -use valida_machine::{Machine, MachineProof, ProgramROM, StdinAdviceProvider}; +use valida_machine::{Machine, MachineProof, ProgramROM, StdinAdviceProvider, StoppingFlag}; use valida_memory::MachineWithMemoryChip; use valida_elf::{load_executable_file, Program}; @@ -34,7 +34,7 @@ use valida_output::MachineWithOutputChip; use reedline_repl_rs::clap::{Arg, ArgMatches, Command}; use reedline_repl_rs::{Repl, Result}; -#[derive(Parser)] +#[derive(Parser, Clone)] struct Args { /// Command option either "run" or "prove" or "verify" or "interactive" #[arg(name = "Action Option")] @@ -53,23 +53,23 @@ struct Args { stack_height: u32, } -struct Context<'a> { +struct Context { machine_: BasicMachine, - args_: &'a Args, + args_: Args, breakpoints_: Vec, - stopped_: bool, + stopped_: StoppingFlag, last_fp_: u32, recorded_current_fp_: u32, last_fp_size_: u32, } -impl Context<'_> { +impl Context { fn new(args: &Args) -> Context { let mut context = Context { machine_: BasicMachine::::default(), - args_: args.clone(), + args_: (*args).clone(), breakpoints_: Vec::new(), - stopped_: false, + stopped_: StoppingFlag::DidNotStop, last_fp_: args.stack_height, recorded_current_fp_: args.stack_height, last_fp_size_: 0, @@ -87,10 +87,10 @@ impl Context<'_> { context } - fn step(&mut self) -> (bool, u32) { + fn step(&mut self) -> (StoppingFlag, u32) { // do not execute if already stopped - if self.stopped_ { - return (true, 0); + if self.stopped_ == StoppingFlag::DidStop { + return (StoppingFlag::DidStop, 0); } let state = self.machine_.step(&mut StdinAdviceProvider); let pc = self.machine_.cpu().pc; @@ -109,22 +109,23 @@ impl Context<'_> { } } -fn init_context(args: ArgMatches, context: &mut Context) -> Result> { +fn init_context(_args: ArgMatches, _context: &mut Context) -> Result> { Ok(Some(String::from("created machine"))) } -fn status(args: ArgMatches, context: &mut Context) -> Result> { +fn status(_args: ArgMatches, context: &mut Context) -> Result> { // construct machine status let mut status = String::new(); status.push_str("FP: "); status.push_str(&context.machine_.cpu().fp.to_string()); status.push_str(", PC: "); status.push_str(&context.machine_.cpu().pc.to_string()); - status.push_str(if context.stopped_ { - ", Stopped" - } else { - ", Running" - }); + status.push_str( + match context.stopped_ { + StoppingFlag::DidStop => ", Stopped", + StoppingFlag::DidNotStop => ", Running", + } + ); Ok(Some(status)) } @@ -204,11 +205,11 @@ fn set_bp(args: ArgMatches, context: &mut Context) -> Result> { Ok(Some(message)) } -fn run_until(args: ArgMatches, context: &mut Context) -> Result> { +fn run_until(_args: ArgMatches, context: &mut Context) -> Result> { let mut message = String::new(); loop { let (stop, pc) = context.step(); - if stop { + if stop == StoppingFlag::DidStop { message.push_str("Execution stopped"); break; } @@ -221,10 +222,10 @@ fn run_until(args: ArgMatches, context: &mut Context) -> Result> Ok(Some(message)) } -fn step(args: ArgMatches, context: &mut Context) -> Result> { +fn step(_args: ArgMatches, context: &mut Context) -> Result> { let (stop, _) = context.step(); - if stop { - context.stopped_ = true; + if stop == StoppingFlag::DidStop { + context.stopped_ = StoppingFlag::DidStop; Ok(Some(String::from("Execution stopped"))) } else { Ok(None) diff --git a/basic/src/lib.rs b/basic/src/lib.rs index c414bd5..1b2d44d 100644 --- a/basic/src/lib.rs +++ b/basic/src/lib.rs @@ -47,7 +47,7 @@ use valida_machine::__internal::{ }; use valida_machine::{ generate_permutation_trace, verify_constraints, AdviceProvider, BusArgument, Chip, ChipProof, - Commitments, Instruction, Machine, MachineProof, OpenedValues, ProgramROM, ValidaAirBuilder, + Commitments, Instruction, Machine, MachineProof, OpenedValues, ProgramROM, StoppingFlag, ValidaAirBuilder, }; use valida_memory::{MachineWithMemoryChip, MemoryChip}; use valida_output::{MachineWithOutputChip, OutputChip, WriteInstruction}; @@ -123,101 +123,8 @@ impl Machine for BasicMachine { self.initialize_memory(); loop { - // Fetch - let pc = self.cpu().pc; - let instruction = program.get_instruction(pc); - let opcode = instruction.opcode; - let ops = instruction.operands; - - // Execute - match opcode { - >::OPCODE => { - Load32Instruction::execute_with_advice::(self, ops, advice) - } - >::OPCODE => { - Store32Instruction::execute_with_advice::(self, ops, advice) - } - >::OPCODE => { - JalInstruction::execute_with_advice::(self, ops, advice) - } - >::OPCODE => { - JalvInstruction::execute_with_advice::(self, ops, advice) - } - >::OPCODE => { - BeqInstruction::execute_with_advice::(self, ops, advice) - } - >::OPCODE => { - BneInstruction::execute_with_advice::(self, ops, advice) - } - >::OPCODE => { - Imm32Instruction::execute_with_advice::(self, ops, advice) - } - >::OPCODE => { - StopInstruction::execute_with_advice::(self, ops, advice) - } - >::OPCODE => { - LoadFpInstruction::execute_with_advice::(self, ops, advice) - } - >::OPCODE => { - Add32Instruction::execute_with_advice::(self, ops, advice) - } - >::OPCODE => { - Sub32Instruction::execute_with_advice::(self, ops, advice) - } - >::OPCODE => { - Mul32Instruction::execute_with_advice::(self, ops, advice) - } - >::OPCODE => { - Mulhs32Instruction::execute_with_advice::(self, ops, advice) - } - >::OPCODE => { - Mulhu32Instruction::execute_with_advice::(self, ops, advice) - } - >::OPCODE => { - Div32Instruction::execute_with_advice::(self, ops, advice) - } - >::OPCODE => { - SDiv32Instruction::execute_with_advice::(self, ops, advice) - } - >::OPCODE => { - Shl32Instruction::execute_with_advice::(self, ops, advice) - } - >::OPCODE => { - Shr32Instruction::execute_with_advice::(self, ops, advice) - } - >::OPCODE => { - Lt32Instruction::execute_with_advice::(self, ops, advice) - } - >::OPCODE => { - Lte32Instruction::execute_with_advice::(self, ops, advice) - } - >::OPCODE => { - And32Instruction::execute_with_advice::(self, ops, advice) - } - >::OPCODE => { - Or32Instruction::execute_with_advice::(self, ops, advice) - } - >::OPCODE => { - Xor32Instruction::execute_with_advice::(self, ops, advice) - } - >::OPCODE => { - Ne32Instruction::execute_with_advice::(self, ops, advice) - } - >::OPCODE => { - Eq32Instruction::execute_with_advice::(self, ops, advice) - } - >::OPCODE => { - ReadAdviceInstruction::execute_with_advice::(self, ops, advice) - } - >::OPCODE => { - WriteInstruction::execute_with_advice::(self, ops, advice) - } - _ => panic!("Unrecognized opcode: {}", opcode), - }; - self.read_word(pc as usize); - - // A STOP instruction signals the end of the program - if opcode == >::OPCODE { + let step_did_stop = self.step(advice); + if step_did_stop == StoppingFlag::DidStop { break; } } @@ -1147,6 +1054,110 @@ impl Machine for BasicMachine { Ok(()) } + + fn step(&mut self, advice: &mut Adv) -> StoppingFlag + where Adv: AdviceProvider + { + // Fetch + let pc = self.cpu().pc; + let instruction = self.program.program_rom.get_instruction(pc); + let opcode = instruction.opcode; + let ops = instruction.operands; + + // Execute + match opcode { + >::OPCODE => { + Load32Instruction::execute_with_advice::(self, ops, advice) + } + >::OPCODE => { + Store32Instruction::execute_with_advice::(self, ops, advice) + } + >::OPCODE => { + JalInstruction::execute_with_advice::(self, ops, advice) + } + >::OPCODE => { + JalvInstruction::execute_with_advice::(self, ops, advice) + } + >::OPCODE => { + BeqInstruction::execute_with_advice::(self, ops, advice) + } + >::OPCODE => { + BneInstruction::execute_with_advice::(self, ops, advice) + } + >::OPCODE => { + Imm32Instruction::execute_with_advice::(self, ops, advice) + } + >::OPCODE => { + StopInstruction::execute_with_advice::(self, ops, advice) + } + >::OPCODE => { + LoadFpInstruction::execute_with_advice::(self, ops, advice) + } + >::OPCODE => { + Add32Instruction::execute_with_advice::(self, ops, advice) + } + >::OPCODE => { + Sub32Instruction::execute_with_advice::(self, ops, advice) + } + >::OPCODE => { + Mul32Instruction::execute_with_advice::(self, ops, advice) + } + >::OPCODE => { + Mulhs32Instruction::execute_with_advice::(self, ops, advice) + } + >::OPCODE => { + Mulhu32Instruction::execute_with_advice::(self, ops, advice) + } + >::OPCODE => { + Div32Instruction::execute_with_advice::(self, ops, advice) + } + >::OPCODE => { + SDiv32Instruction::execute_with_advice::(self, ops, advice) + } + >::OPCODE => { + Shl32Instruction::execute_with_advice::(self, ops, advice) + } + >::OPCODE => { + Shr32Instruction::execute_with_advice::(self, ops, advice) + } + >::OPCODE => { + Lt32Instruction::execute_with_advice::(self, ops, advice) + } + >::OPCODE => { + Lte32Instruction::execute_with_advice::(self, ops, advice) + } + >::OPCODE => { + And32Instruction::execute_with_advice::(self, ops, advice) + } + >::OPCODE => { + Or32Instruction::execute_with_advice::(self, ops, advice) + } + >::OPCODE => { + Xor32Instruction::execute_with_advice::(self, ops, advice) + } + >::OPCODE => { + Ne32Instruction::execute_with_advice::(self, ops, advice) + } + >::OPCODE => { + Eq32Instruction::execute_with_advice::(self, ops, advice) + } + >::OPCODE => { + ReadAdviceInstruction::execute_with_advice::(self, ops, advice) + } + >::OPCODE => { + WriteInstruction::execute_with_advice::(self, ops, advice) + } + _ => panic!("Unrecognized opcode: {}", opcode), + }; + self.read_word(pc as usize); + + // A STOP instruction signals the end of the program + if opcode == >::OPCODE { + StoppingFlag::DidStop + } else { + StoppingFlag::DidNotStop + } + } } impl MachineWithGeneralBus for BasicMachine { diff --git a/basic_macro/src/lib.rs b/basic_macro/src/lib.rs index e7522e0..8d2b44e 100644 --- a/basic_macro/src/lib.rs +++ b/basic_macro/src/lib.rs @@ -40,7 +40,7 @@ use valida_cpu::{CpuChip, MachineWithCpuChip}; use valida_derive::Machine; use valida_machine::{ AdviceProvider, BusArgument, Chip, ChipProof, Instruction, Machine, MachineProof, ProgramROM, - ValidaAirBuilder, + StoppingFlag, ValidaAirBuilder, }; use valida_memory::{MachineWithMemoryChip, MemoryChip}; use valida_output::{MachineWithOutputChip, OutputChip, WriteInstruction}; diff --git a/derive/src/lib.rs b/derive/src/lib.rs index d369160..13d9782 100644 --- a/derive/src/lib.rs +++ b/derive/src/lib.rs @@ -149,18 +149,6 @@ fn run_method( let name = &machine.ident; let (_, ty_generics, _) = machine.generics.split_for_impl(); - let opcode_arms = instructions - .iter() - .map(|inst| { - let ty = &inst.ty; - quote! { - // TODO: Self instead of #name #ty_generics? - <#ty as Instruction<#name #ty_generics, #val>>::OPCODE => - #ty::execute_with_advice::(self, ops, advice), - } - }) - .collect::(); - let init_static_data: TokenStream2 = match static_data_chip { Some(_static_data_chip) => quote! { self.initialize_memory(); @@ -173,25 +161,10 @@ fn run_method( #init_static_data loop { - // Fetch - let pc = self.cpu().pc; - let instruction = program.get_instruction(pc); - let opcode = instruction.opcode; - let ops = instruction.operands; - - // Execute - std::println!("trace: pc = {:?}, instruction = {:?}, ops = {:?}", pc, instruction, ops); - match opcode { - #opcode_arms - _ => panic!("Unrecognized opcode: {}", opcode), - }; - self.read_word(pc as usize); - - //let stop = self.step(&program, &mut advice); - // A STOP instruction signals the end of the program - if opcode == >::OPCODE { - break; - } + let step_did_stop = self.step(advice); + if step_did_stop == StoppingFlag::DidStop { + break; + } } // Record padded STOP instructions @@ -221,7 +194,7 @@ fn step_method(machine: &syn::DeriveInput, instructions: &[&Field], val: &Ident) .collect::(); quote! { - fn step(&mut self, advice: &mut Adv) -> bool { + fn step(&mut self, advice: &mut Adv) -> StoppingFlag { let pc = self.cpu().pc; let instruction = self.program.program_rom.get_instruction(pc); let opcode = instruction.opcode; @@ -234,7 +207,11 @@ fn step_method(machine: &syn::DeriveInput, instructions: &[&Field], val: &Ident) }; self.read_word(pc as usize); - opcode == >::OPCODE + if opcode == >::OPCODE { + StoppingFlag::DidStop + } else { + StoppingFlag::DidNotStop + } } } } diff --git a/machine/src/machine.rs b/machine/src/machine.rs index 70d6412..1b23f17 100644 --- a/machine/src/machine.rs +++ b/machine/src/machine.rs @@ -4,12 +4,15 @@ use crate::proof::MachineProof; use crate::AdviceProvider; use p3_field::Field; +#[derive(PartialEq, Eq)] +pub enum StoppingFlag { DidStop, DidNotStop } + pub trait Machine: Sync { fn run(&mut self, program: &ProgramROM, advice: &mut Adv) where Adv: AdviceProvider; - fn step(&mut self, advice: &mut Adv) -> bool + fn step(&mut self, advice: &mut Adv) -> StoppingFlag where Adv: AdviceProvider; From 125b33bb1ceae74730c93d4c79bfb123416390d3 Mon Sep 17 00:00:00 2001 From: Morgan Thomas Date: Tue, 9 Apr 2024 12:17:46 -0400 Subject: [PATCH 12/23] issue/143: cargo fmt --- basic/src/bin/valida.rs | 10 ++++------ basic/src/lib.rs | 6 ++++-- machine/src/machine.rs | 5 ++++- 3 files changed, 12 insertions(+), 9 deletions(-) diff --git a/basic/src/bin/valida.rs b/basic/src/bin/valida.rs index b616ace..062224e 100644 --- a/basic/src/bin/valida.rs +++ b/basic/src/bin/valida.rs @@ -120,12 +120,10 @@ fn status(_args: ArgMatches, context: &mut Context) -> Result> { status.push_str(&context.machine_.cpu().fp.to_string()); status.push_str(", PC: "); status.push_str(&context.machine_.cpu().pc.to_string()); - status.push_str( - match context.stopped_ { - StoppingFlag::DidStop => ", Stopped", - StoppingFlag::DidNotStop => ", Running", - } - ); + status.push_str(match context.stopped_ { + StoppingFlag::DidStop => ", Stopped", + StoppingFlag::DidNotStop => ", Running", + }); Ok(Some(status)) } diff --git a/basic/src/lib.rs b/basic/src/lib.rs index 1b2d44d..35168ea 100644 --- a/basic/src/lib.rs +++ b/basic/src/lib.rs @@ -47,7 +47,8 @@ use valida_machine::__internal::{ }; use valida_machine::{ generate_permutation_trace, verify_constraints, AdviceProvider, BusArgument, Chip, ChipProof, - Commitments, Instruction, Machine, MachineProof, OpenedValues, ProgramROM, StoppingFlag, ValidaAirBuilder, + Commitments, Instruction, Machine, MachineProof, OpenedValues, ProgramROM, StoppingFlag, + ValidaAirBuilder, }; use valida_memory::{MachineWithMemoryChip, MemoryChip}; use valida_output::{MachineWithOutputChip, OutputChip, WriteInstruction}; @@ -1056,7 +1057,8 @@ impl Machine for BasicMachine { } fn step(&mut self, advice: &mut Adv) -> StoppingFlag - where Adv: AdviceProvider + where + Adv: AdviceProvider, { // Fetch let pc = self.cpu().pc; diff --git a/machine/src/machine.rs b/machine/src/machine.rs index 1b23f17..8122dbf 100644 --- a/machine/src/machine.rs +++ b/machine/src/machine.rs @@ -5,7 +5,10 @@ use crate::AdviceProvider; use p3_field::Field; #[derive(PartialEq, Eq)] -pub enum StoppingFlag { DidStop, DidNotStop } +pub enum StoppingFlag { + DidStop, + DidNotStop, +} pub trait Machine: Sync { fn run(&mut self, program: &ProgramROM, advice: &mut Adv) From d61efe8d5c9047c2479ea9d7f5a3382cc862c7c8 Mon Sep 17 00:00:00 2001 From: Morgan Thomas Date: Tue, 9 Apr 2024 12:52:45 -0400 Subject: [PATCH 13/23] issue/140: fix merge of morgan/issue/143 --- Cargo.lock | 42 ------------------------------------------ Cargo.toml | 2 +- basic/src/lib.rs | 22 ++++++++++++---------- 3 files changed, 13 insertions(+), 53 deletions(-) diff --git a/Cargo.lock b/Cargo.lock index 81874cc..540e91c 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -1452,48 +1452,6 @@ dependencies = [ "valida-static-data", ] -[[package]] -name = "valida-basic-macro" -version = "0.1.0" -dependencies = [ - "byteorder", - "ciborium", - "clap", - "p3-air", - "p3-baby-bear", - "p3-challenger", - "p3-commit", - "p3-dft", - "p3-field", - "p3-fri", - "p3-goldilocks", - "p3-keccak", - "p3-matrix", - "p3-maybe-rayon", - "p3-mds", - "p3-merkle-tree", - "p3-poseidon", - "p3-symmetric", - "p3-uni-stark", - "p3-util", - "rand", - "rand_pcg", - "rand_seeder", - "tracing", - "valida-alu-u32", - "valida-assembler", - "valida-bus", - "valida-cpu", - "valida-derive", - "valida-machine", - "valida-memory", - "valida-opcodes", - "valida-output", - "valida-program", - "valida-range", - "valida-static-data", -] - [[package]] name = "valida-bus" version = "0.1.0" diff --git a/Cargo.toml b/Cargo.toml index ff8210b..88e7f02 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -4,7 +4,7 @@ members = [ "assembler", "alu_u32", "basic", - "basic_macro", + # "basic_macro", "bus", "cpu", "derive", diff --git a/basic/src/lib.rs b/basic/src/lib.rs index 35168ea..e5f1b75 100644 --- a/basic/src/lib.rs +++ b/basic/src/lib.rs @@ -602,8 +602,7 @@ impl Machine for BasicMachine { let zeta_exp_quotient_degree: [Vec; NUM_CHIPS] = log_quotient_degrees.map(|log_deg| vec![zeta.exp_power_of_2(log_deg)]); let prover_data_and_points = [ - // TODO: Causes some errors, probably related to the fact that not all chips have preprocessed traces? - // (&preprocessed_data, zeta_and_next.as_slice()), + (&preprocessed_data, zeta_and_next.as_slice()), (&main_data, zeta_and_next.as_slice()), (&perm_data, zeta_and_next.as_slice()), ("ient_data, zeta_exp_quotient_degree.as_slice()), @@ -612,27 +611,27 @@ impl Machine for BasicMachine { pcs.open_multi_batches(&prover_data_and_points, &mut challenger); // TODO: add preprocessed openings - let [main_openings, perm_openings, quotient_openings] = openings + let [preprocessed_openings, main_openings, perm_openings, quotient_openings] = openings .try_into() .expect("Should have 3 rounds of openings"); let commitments = Commitments { + preprocessed_trace: preprocessed_commit, main_trace: main_commit, perm_trace: perm_commit, quotient_chunks: quotient_commit, }; - // TODO: add preprocessed openings let chip_proofs = log_degrees .iter() + .zip(preprocessed_openings) .zip(main_openings) .zip(perm_openings) .zip(quotient_openings) .zip(perm_traces) - .map(|((((log_degree, main), perm), quotient), perm_trace)| { - // TODO: add preprocessed openings - let [preprocessed_local, preprocessed_next] = [vec![], vec![]]; - + .map(|(((((log_degree, preprocessed), main), perm), quotient), perm_trace)| { + let [preprocessed_local, preprocessed_next] = + preprocessed.try_into().expect("Should have 2 openings"); let [main_local, main_next] = main.try_into().expect("Should have 2 openings"); let [perm_local, perm_next] = perm.try_into().expect("Should have 2 openings"); let [quotient_chunks] = quotient.try_into().expect("Should have 1 opening"); @@ -752,6 +751,7 @@ impl Machine for BasicMachine { .unwrap(); // TODO: maybe avoid cloning opened values (not sure if possible) + let mut preprocessed_values = vec![]; let mut main_values = vec![]; let mut perm_values = vec![]; let mut quotient_values = vec![]; @@ -767,15 +767,17 @@ impl Machine for BasicMachine { quotient_chunks, } = &chip_proof.opened_values; + preprocessed_values.push(vec![preprocessed_local.clone(), preprocessed_next.clone()]); main_values.push(vec![trace_local.clone(), trace_next.clone()]); perm_values.push(vec![permutation_local.clone(), permutation_next.clone()]); quotient_values.push(vec![quotient_chunks.clone()]); } - let chips_opening_values = vec![main_values, perm_values, quotient_values]; + let chips_opening_values = vec![preprocessed_values, main_values, perm_values, quotient_values]; // Observe commitments and get challenges. let Commitments { + preprocessed_trace, main_trace, perm_trace, quotient_chunks, @@ -817,7 +819,7 @@ impl Machine for BasicMachine { log_quotient_degrees.map(|log_deg| vec![zeta.exp_power_of_2(log_deg)]); pcs.verify_multi_batches( &[ - // TODO: add preprocessed trace + (preprocessed_trace.clone(), zeta_and_next.as_slice()), (main_trace.clone(), zeta_and_next.as_slice()), (perm_trace.clone(), zeta_and_next.as_slice()), (quotient_chunks.clone(), zeta_exp_quotient_degree.as_slice()), From 15c4c2f15fb2ccbfb11fb86073d3b44ef5e6105e Mon Sep 17 00:00:00 2001 From: Morgan Thomas Date: Tue, 9 Apr 2024 19:07:08 -0400 Subject: [PATCH 14/23] issue/140: wip: bugfix static data chip --- Cargo.lock | 19 ------------------- basic/src/lib.rs | 3 +-- static_data/src/columns.rs | 10 ++++++++-- static_data/src/lib.rs | 22 +++++++++++++++------- static_data/src/stark.rs | 2 +- 5 files changed, 25 insertions(+), 31 deletions(-) diff --git a/Cargo.lock b/Cargo.lock index 540e91c..969a2fa 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -607,7 +607,6 @@ checksum = "0ab1bc2a289d34bd04a330323ac98a1b4bc82c9d9fcb1e66b63caa84da26b575" [[package]] name = "p3-air" version = "0.1.0" -source = "git+https://github.com/valida-xyz/Plonky3.git?branch=valida-main#3c89583157f5186148674543c91160be0a734c8e" dependencies = [ "p3-field", "p3-matrix", @@ -616,7 +615,6 @@ dependencies = [ [[package]] name = "p3-baby-bear" version = "0.1.0" -source = "git+https://github.com/valida-xyz/Plonky3.git?branch=valida-main#3c89583157f5186148674543c91160be0a734c8e" dependencies = [ "p3-field", "rand", @@ -626,7 +624,6 @@ dependencies = [ [[package]] name = "p3-challenger" version = "0.1.0" -source = "git+https://github.com/valida-xyz/Plonky3.git?branch=valida-main#3c89583157f5186148674543c91160be0a734c8e" dependencies = [ "p3-field", "p3-maybe-rayon", @@ -637,7 +634,6 @@ dependencies = [ [[package]] name = "p3-commit" version = "0.1.0" -source = "git+https://github.com/valida-xyz/Plonky3.git?branch=valida-main#3c89583157f5186148674543c91160be0a734c8e" dependencies = [ "p3-challenger", "p3-field", @@ -648,7 +644,6 @@ dependencies = [ [[package]] name = "p3-dft" version = "0.1.0" -source = "git+https://github.com/valida-xyz/Plonky3.git?branch=valida-main#3c89583157f5186148674543c91160be0a734c8e" dependencies = [ "p3-field", "p3-matrix", @@ -659,7 +654,6 @@ dependencies = [ [[package]] name = "p3-field" version = "0.1.0" -source = "git+https://github.com/valida-xyz/Plonky3.git?branch=valida-main#3c89583157f5186148674543c91160be0a734c8e" dependencies = [ "itertools 0.12.1", "p3-util", @@ -670,7 +664,6 @@ dependencies = [ [[package]] name = "p3-fri" version = "0.1.0" -source = "git+https://github.com/valida-xyz/Plonky3.git?branch=valida-main#3c89583157f5186148674543c91160be0a734c8e" dependencies = [ "itertools 0.12.1", "p3-challenger", @@ -688,7 +681,6 @@ dependencies = [ [[package]] name = "p3-goldilocks" version = "0.1.0" -source = "git+https://github.com/valida-xyz/Plonky3.git?branch=valida-main#3c89583157f5186148674543c91160be0a734c8e" dependencies = [ "p3-field", "p3-util", @@ -699,7 +691,6 @@ dependencies = [ [[package]] name = "p3-interpolation" version = "0.1.0" -source = "git+https://github.com/valida-xyz/Plonky3.git?branch=valida-main#3c89583157f5186148674543c91160be0a734c8e" dependencies = [ "p3-field", "p3-matrix", @@ -710,7 +701,6 @@ dependencies = [ [[package]] name = "p3-keccak" version = "0.1.0" -source = "git+https://github.com/valida-xyz/Plonky3.git?branch=valida-main#3c89583157f5186148674543c91160be0a734c8e" dependencies = [ "p3-symmetric", "tiny-keccak", @@ -719,7 +709,6 @@ dependencies = [ [[package]] name = "p3-matrix" version = "0.1.0" -source = "git+https://github.com/valida-xyz/Plonky3.git?branch=valida-main#3c89583157f5186148674543c91160be0a734c8e" dependencies = [ "p3-field", "p3-maybe-rayon", @@ -730,12 +719,10 @@ dependencies = [ [[package]] name = "p3-maybe-rayon" version = "0.1.0" -source = "git+https://github.com/valida-xyz/Plonky3.git?branch=valida-main#3c89583157f5186148674543c91160be0a734c8e" [[package]] name = "p3-mds" version = "0.1.0" -source = "git+https://github.com/valida-xyz/Plonky3.git?branch=valida-main#3c89583157f5186148674543c91160be0a734c8e" dependencies = [ "p3-baby-bear", "p3-dft", @@ -751,7 +738,6 @@ dependencies = [ [[package]] name = "p3-merkle-tree" version = "0.1.0" -source = "git+https://github.com/valida-xyz/Plonky3.git?branch=valida-main#3c89583157f5186148674543c91160be0a734c8e" dependencies = [ "itertools 0.12.1", "p3-commit", @@ -767,7 +753,6 @@ dependencies = [ [[package]] name = "p3-mersenne-31" version = "0.1.0" -source = "git+https://github.com/valida-xyz/Plonky3.git?branch=valida-main#3c89583157f5186148674543c91160be0a734c8e" dependencies = [ "criterion", "itertools 0.12.1", @@ -783,7 +768,6 @@ dependencies = [ [[package]] name = "p3-poseidon" version = "0.1.0" -source = "git+https://github.com/valida-xyz/Plonky3.git?branch=valida-main#3c89583157f5186148674543c91160be0a734c8e" dependencies = [ "p3-field", "p3-mds", @@ -794,7 +778,6 @@ dependencies = [ [[package]] name = "p3-symmetric" version = "0.1.0" -source = "git+https://github.com/valida-xyz/Plonky3.git?branch=valida-main#3c89583157f5186148674543c91160be0a734c8e" dependencies = [ "itertools 0.12.1", "p3-field", @@ -803,7 +786,6 @@ dependencies = [ [[package]] name = "p3-uni-stark" version = "0.1.0" -source = "git+https://github.com/valida-xyz/Plonky3.git?branch=valida-main#3c89583157f5186148674543c91160be0a734c8e" dependencies = [ "itertools 0.12.1", "p3-air", @@ -821,7 +803,6 @@ dependencies = [ [[package]] name = "p3-util" version = "0.1.0" -source = "git+https://github.com/valida-xyz/Plonky3.git?branch=valida-main#3c89583157f5186148674543c91160be0a734c8e" dependencies = [ "serde", ] diff --git a/basic/src/lib.rs b/basic/src/lib.rs index e5f1b75..e226696 100644 --- a/basic/src/lib.rs +++ b/basic/src/lib.rs @@ -610,7 +610,6 @@ impl Machine for BasicMachine { let (openings, opening_proof) = pcs.open_multi_batches(&prover_data_and_points, &mut challenger); - // TODO: add preprocessed openings let [preprocessed_openings, main_openings, perm_openings, quotient_openings] = openings .try_into() .expect("Should have 3 rounds of openings"); @@ -624,7 +623,7 @@ impl Machine for BasicMachine { let chip_proofs = log_degrees .iter() - .zip(preprocessed_openings) + .zip(preprocessed_openings) // TODO: add empties so that the zips don't truncate .zip(main_openings) .zip(perm_openings) .zip(quotient_openings) diff --git a/static_data/src/columns.rs b/static_data/src/columns.rs index 5ff965e..f3a6dd2 100644 --- a/static_data/src/columns.rs +++ b/static_data/src/columns.rs @@ -5,8 +5,14 @@ use valida_machine::Word; use valida_util::indices_arr; pub struct StaticDataCols { - // Not used for anything, just present because of the assumption that each chip has a column in its trace - pub dummy: T, + /// Memory address + pub addr: T, + + /// Memory cell + pub value: Word, + + /// Whether this row represents a real (address, value) pair + pub is_real: T, } pub const NUM_STATIC_DATA_COLS: usize = size_of::>(); diff --git a/static_data/src/lib.rs b/static_data/src/lib.rs index e7defb8..47d9cb9 100644 --- a/static_data/src/lib.rs +++ b/static_data/src/lib.rs @@ -1,8 +1,6 @@ -#![no_std] - extern crate alloc; -use crate::columns::{NUM_STATIC_DATA_COLS, STATIC_DATA_PREPROCESSED_COL_MAP}; +use crate::columns::{NUM_STATIC_DATA_COLS, STATIC_DATA_COL_MAP}; use alloc::collections::BTreeMap; use alloc::vec; use alloc::vec::Vec; @@ -57,14 +55,24 @@ where SC: StarkConfig, { fn generate_trace(&self, _machine: &M) -> RowMajorMatrix { - RowMajorMatrix::new(vec![SC::Val::zero(); self.cells.len().next_power_of_two()], NUM_STATIC_DATA_COLS) + let mut rows = self.cells.iter() + .map(|(addr, value)| { + let mut row: Vec = vec![SC::Val::from_canonical_u32(*addr)]; + row.extend(value.0.into_iter().map(SC::Val::from_canonical_u8).collect::>()); + row.push(SC::Val::one()); + row + }) + .flatten() + .collect::>(); + rows.resize(rows.len().next_power_of_two() * NUM_STATIC_DATA_COLS, SC::Val::zero()); + RowMajorMatrix::new(rows, NUM_STATIC_DATA_COLS) } fn global_sends(&self, machine: &M) -> Vec> { - let addr = VirtualPairCol::single_preprocessed(STATIC_DATA_PREPROCESSED_COL_MAP.addr); - let value = STATIC_DATA_PREPROCESSED_COL_MAP.value.0.map(VirtualPairCol::single_preprocessed); + let addr = VirtualPairCol::single_main(STATIC_DATA_COL_MAP.addr); + let value = STATIC_DATA_COL_MAP.value.0.map(VirtualPairCol::single_main); let is_read = VirtualPairCol::constant(SC::Val::zero()); - let is_real = VirtualPairCol::single_preprocessed(STATIC_DATA_PREPROCESSED_COL_MAP.is_real); + let is_real = VirtualPairCol::single_main(STATIC_DATA_COL_MAP.is_real); let is_static_initial = VirtualPairCol::constant(SC::Val::one()); let clk = VirtualPairCol::constant(SC::Val::zero()); let mut fields = vec![is_read, clk, addr, is_static_initial]; diff --git a/static_data/src/stark.rs b/static_data/src/stark.rs index 759f66d..43d24ea 100644 --- a/static_data/src/stark.rs +++ b/static_data/src/stark.rs @@ -32,6 +32,6 @@ where AB: AirBuilder, { fn eval(&self, _builder: &mut AB) { - // Nothing to do here + // TODO: check equality of main trace with preprocessed trace } } From 28c147a17dc029ceb8a72e5f80f1dff9cecfdeb6 Mon Sep 17 00:00:00 2001 From: Morgan Thomas Date: Wed, 10 Apr 2024 19:54:21 -0400 Subject: [PATCH 15/23] issue/140: wip: bugfix static data chip --- alu_u32/src/add/stark.rs | 4 ++-- alu_u32/src/bitwise/stark.rs | 2 +- alu_u32/src/com/stark.rs | 2 +- alu_u32/src/div/stark.rs | 4 ++-- alu_u32/src/lt/stark.rs | 2 +- alu_u32/src/mul/stark.rs | 2 +- alu_u32/src/shift/stark.rs | 2 +- alu_u32/src/sub/stark.rs | 2 +- basic/src/lib.rs | 6 +++--- cpu/src/stark.rs | 2 +- machine/src/check_constraints.rs | 13 +++---------- machine/src/chip.rs | 13 +++---------- memory/src/stark.rs | 3 ++- native_field/src/stark.rs | 2 +- output/src/stark.rs | 4 ++-- program/src/stark.rs | 5 ++--- range/src/stark.rs | 4 ++-- static_data/src/stark.rs | 4 ++-- 18 files changed, 31 insertions(+), 45 deletions(-) diff --git a/alu_u32/src/add/stark.rs b/alu_u32/src/add/stark.rs index 58b3950..1a370af 100644 --- a/alu_u32/src/add/stark.rs +++ b/alu_u32/src/add/stark.rs @@ -4,10 +4,10 @@ use core::borrow::Borrow; use crate::add::columns::NUM_ADD_COLS; use p3_air::{Air, AirBuilder, BaseAir}; -use p3_field::PrimeField; +use p3_field::{AbstractField, PrimeField}; use p3_matrix::MatrixRowSlices; -impl BaseAir for Add32Chip { +impl BaseAir for Add32Chip { fn width(&self) -> usize { NUM_ADD_COLS } diff --git a/alu_u32/src/bitwise/stark.rs b/alu_u32/src/bitwise/stark.rs index b628bb6..73a831f 100644 --- a/alu_u32/src/bitwise/stark.rs +++ b/alu_u32/src/bitwise/stark.rs @@ -8,7 +8,7 @@ use p3_air::{Air, AirBuilder, BaseAir}; use p3_field::AbstractField; use p3_matrix::MatrixRowSlices; -impl BaseAir for Bitwise32Chip { +impl BaseAir for Bitwise32Chip { fn width(&self) -> usize { NUM_BITWISE_COLS } diff --git a/alu_u32/src/com/stark.rs b/alu_u32/src/com/stark.rs index 9ce1357..b5b29c8 100644 --- a/alu_u32/src/com/stark.rs +++ b/alu_u32/src/com/stark.rs @@ -7,7 +7,7 @@ use p3_air::{Air, AirBuilder, BaseAir}; use p3_field::AbstractField; use p3_matrix::MatrixRowSlices; -impl BaseAir for Com32Chip { +impl BaseAir for Com32Chip { fn width(&self) -> usize { NUM_COM_COLS } diff --git a/alu_u32/src/div/stark.rs b/alu_u32/src/div/stark.rs index f61ae82..f151dc3 100644 --- a/alu_u32/src/div/stark.rs +++ b/alu_u32/src/div/stark.rs @@ -2,9 +2,9 @@ use super::Div32Chip; use crate::div::columns::NUM_DIV_COLS; use p3_air::{Air, AirBuilder, BaseAir}; -use p3_field::PrimeField; +use p3_field::{AbstractField, PrimeField}; -impl BaseAir for Div32Chip { +impl BaseAir for Div32Chip { fn width(&self) -> usize { NUM_DIV_COLS } diff --git a/alu_u32/src/lt/stark.rs b/alu_u32/src/lt/stark.rs index 2180ce5..bc0a2b8 100644 --- a/alu_u32/src/lt/stark.rs +++ b/alu_u32/src/lt/stark.rs @@ -7,7 +7,7 @@ use p3_air::{Air, AirBuilder, BaseAir}; use p3_field::AbstractField; use p3_matrix::MatrixRowSlices; -impl BaseAir for Lt32Chip { +impl BaseAir for Lt32Chip { fn width(&self) -> usize { NUM_LT_COLS } diff --git a/alu_u32/src/mul/stark.rs b/alu_u32/src/mul/stark.rs index 38376d2..92d899e 100644 --- a/alu_u32/src/mul/stark.rs +++ b/alu_u32/src/mul/stark.rs @@ -9,7 +9,7 @@ use p3_air::{Air, AirBuilder, BaseAir}; use p3_field::{AbstractField, PrimeField}; use p3_matrix::MatrixRowSlices; -impl BaseAir for Mul32Chip { +impl BaseAir for Mul32Chip { fn width(&self) -> usize { NUM_MUL_COLS } diff --git a/alu_u32/src/shift/stark.rs b/alu_u32/src/shift/stark.rs index b25d05a..b7a366c 100644 --- a/alu_u32/src/shift/stark.rs +++ b/alu_u32/src/shift/stark.rs @@ -7,7 +7,7 @@ use p3_air::{Air, AirBuilder, BaseAir}; use p3_field::AbstractField; use p3_matrix::MatrixRowSlices; -impl BaseAir for Shift32Chip { +impl BaseAir for Shift32Chip { fn width(&self) -> usize { NUM_SHIFT_COLS } diff --git a/alu_u32/src/sub/stark.rs b/alu_u32/src/sub/stark.rs index b0bd008..d62b9cf 100644 --- a/alu_u32/src/sub/stark.rs +++ b/alu_u32/src/sub/stark.rs @@ -7,7 +7,7 @@ use p3_air::{Air, AirBuilder, BaseAir}; use p3_field::{AbstractField, PrimeField}; use p3_matrix::MatrixRowSlices; -impl BaseAir for Sub32Chip { +impl BaseAir for Sub32Chip { fn width(&self) -> usize { NUM_SUB_COLS } diff --git a/basic/src/lib.rs b/basic/src/lib.rs index e226696..6f51be0 100644 --- a/basic/src/lib.rs +++ b/basic/src/lib.rs @@ -183,7 +183,7 @@ impl Machine for BasicMachine { tracing::info_span!("generate preprocessed traces").in_scope(|| { chips .par_iter() - .flat_map(|chip| chip.preprocessed_trace()) + .map(|chip| chip.preprocessed_trace()) .collect::>() }); @@ -623,7 +623,7 @@ impl Machine for BasicMachine { let chip_proofs = log_degrees .iter() - .zip(preprocessed_openings) // TODO: add empties so that the zips don't truncate + .zip(preprocessed_openings) .zip(main_openings) .zip(perm_openings) .zip(quotient_openings) @@ -787,7 +787,7 @@ impl Machine for BasicMachine { tracing::info_span!("generate preprocessed traces").in_scope(|| { chips .par_iter() - .flat_map(|chip| chip.preprocessed_trace()) + .map(|chip| chip.preprocessed_trace()) .collect::>() }); diff --git a/cpu/src/stark.rs b/cpu/src/stark.rs index 425267b..e79795c 100644 --- a/cpu/src/stark.rs +++ b/cpu/src/stark.rs @@ -8,7 +8,7 @@ use p3_field::{AbstractField, PrimeField}; use p3_matrix::MatrixRowSlices; use valida_opcodes::BYTES_PER_INSTR; -impl BaseAir for CpuChip { +impl BaseAir for CpuChip { fn width(&self) -> usize { NUM_CPU_COLS } diff --git a/machine/src/check_constraints.rs b/machine/src/check_constraints.rs index 97ecb3e..ac4ca7b 100644 --- a/machine/src/check_constraints.rs +++ b/machine/src/check_constraints.rs @@ -29,6 +29,7 @@ pub fn check_constraints( } let preprocessed = air.preprocessed_trace(); + let preprocessed_height = preprocessed.height(); let cumulative_sum = *perm.row_slice(perm.height() - 1).last().unwrap(); @@ -38,16 +39,8 @@ pub fn check_constraints( let main_local = main.row_slice(i); let main_next = main.row_slice(i_next); - let preprocessed_local = if preprocessed.is_some() { - preprocessed.as_ref().unwrap().row_slice(i) - } else { - &[] - }; - let preprocessed_next = if preprocessed.is_some() { - preprocessed.as_ref().unwrap().row_slice(i_next) - } else { - &[] - }; + let preprocessed_local = preprocessed.row_slice(i % preprocessed_height); + let preprocessed_next = preprocessed.row_slice(i_next % preprocessed_height); let perm_local = perm.row_slice(i); let perm_next = perm.row_slice(i_next); diff --git a/machine/src/chip.rs b/machine/src/chip.rs index 8c97e8f..baa8f8f 100644 --- a/machine/src/chip.rs +++ b/machine/src/chip.rs @@ -132,6 +132,7 @@ where let betas = random_elements[2].powers(); let preprocessed = chip.preprocessed_trace(); + let preprocessed_height = preprocessed.height(); // Compute the reciprocal columns // @@ -153,11 +154,7 @@ where } else { alphas_global[interaction.argument_index()] }; - let preprocessed_row = if preprocessed.is_some() { - preprocessed.as_ref().unwrap().row_slice(n) - } else { - &[] - }; + let preprocessed_row = preprocessed.row_slice(n % preprocessed_height); row[m] = reduce_row( main_row, preprocessed_row, @@ -179,11 +176,7 @@ where if n > 0 { phi[n] = phi[n - 1]; } - let preprocessed_row = if preprocessed.is_some() { - preprocessed.as_ref().unwrap().row_slice(n) - } else { - &[] - }; + let preprocessed_row = preprocessed.row_slice(n % preprocessed_height); for (m, (interaction, interaction_type)) in all_interactions.iter().enumerate() { let mult = interaction .count diff --git a/memory/src/stark.rs b/memory/src/stark.rs index cac818b..b3ae75e 100644 --- a/memory/src/stark.rs +++ b/memory/src/stark.rs @@ -2,8 +2,9 @@ use crate::columns::NUM_MEM_COLS; use crate::MemoryChip; use p3_air::{Air, AirBuilder, BaseAir}; +use p3_field::AbstractField; -impl BaseAir for MemoryChip { +impl BaseAir for MemoryChip { fn width(&self) -> usize { NUM_MEM_COLS } diff --git a/native_field/src/stark.rs b/native_field/src/stark.rs index 08ceadf..0fcf64f 100644 --- a/native_field/src/stark.rs +++ b/native_field/src/stark.rs @@ -7,7 +7,7 @@ use p3_air::{Air, AirBuilder, BaseAir}; use p3_field::{AbstractField, PrimeField}; use p3_matrix::MatrixRowSlices; -impl BaseAir for NativeFieldChip { +impl BaseAir for NativeFieldChip { fn width(&self) -> usize { NUM_NATIVE_FIELD_COLS } diff --git a/output/src/stark.rs b/output/src/stark.rs index 22110ce..6846c63 100644 --- a/output/src/stark.rs +++ b/output/src/stark.rs @@ -4,10 +4,10 @@ use core::borrow::Borrow; use valida_opcodes::WRITE; use p3_air::{Air, AirBuilder, BaseAir}; -use p3_field::PrimeField; +use p3_field::{AbstractField, PrimeField}; use p3_matrix::MatrixRowSlices; -impl BaseAir for OutputChip { +impl BaseAir for OutputChip { fn width(&self) -> usize { NUM_OUTPUT_COLS } diff --git a/program/src/stark.rs b/program/src/stark.rs index e846857..c1c4811 100644 --- a/program/src/stark.rs +++ b/program/src/stark.rs @@ -19,7 +19,7 @@ impl BaseAir for ProgramChip { NUM_PROGRAM_COLS } - fn preprocessed_trace(&self) -> Option> { + fn preprocessed_trace(&self) -> RowMajorMatrix { // Pad the ROM to a power of two. let mut rom = self.program_rom.0.clone(); let n = rom.len(); @@ -35,7 +35,6 @@ impl BaseAir for ProgramChip { row }) .collect(); - let trace = RowMajorMatrix::new(flattened, NUM_PREPROCESSED_COLS); - Some(trace) + RowMajorMatrix::new(flattened, NUM_PREPROCESSED_COLS) } } diff --git a/range/src/stark.rs b/range/src/stark.rs index e9164d6..4102392 100644 --- a/range/src/stark.rs +++ b/range/src/stark.rs @@ -19,8 +19,8 @@ impl BaseAir for RangeCheckerChip { NUM_RANGE_COLS } - fn preprocessed_trace(&self) -> Option> { + fn preprocessed_trace(&self) -> RowMajorMatrix { let column = (0..MAX).map(F::from_canonical_u32).collect(); - Some(RowMajorMatrix::new_col(column)) + RowMajorMatrix::new_col(column) } } diff --git a/static_data/src/stark.rs b/static_data/src/stark.rs index 43d24ea..e8f57cc 100644 --- a/static_data/src/stark.rs +++ b/static_data/src/stark.rs @@ -12,7 +12,7 @@ impl BaseAir for StaticDataChip { NUM_STATIC_DATA_COLS } - fn preprocessed_trace(&self) -> Option> { + fn preprocessed_trace(&self) -> RowMajorMatrix { let mut rows = self.cells.iter() .map(|(addr, value)| { let mut row: Vec = vec![F::from_canonical_u32(*addr)]; @@ -23,7 +23,7 @@ impl BaseAir for StaticDataChip { .flatten() .collect::>(); rows.resize(rows.len().next_power_of_two() * NUM_STATIC_DATA_PREPROCESSED_COLS, F::zero()); - Some(RowMajorMatrix::new(rows, NUM_STATIC_DATA_PREPROCESSED_COLS)) + RowMajorMatrix::new(rows, NUM_STATIC_DATA_PREPROCESSED_COLS) } } From f115fe8a756638140edd288949b0fe7cc56eb39e Mon Sep 17 00:00:00 2001 From: Morgan Thomas Date: Wed, 10 Apr 2024 20:20:59 -0400 Subject: [PATCH 16/23] issue/140: more specific failures to verify --- basic/src/lib.rs | 8 ++++---- machine/src/machine.rs | 8 +++++++- 2 files changed, 11 insertions(+), 5 deletions(-) diff --git a/basic/src/lib.rs b/basic/src/lib.rs index 6f51be0..fd07183 100644 --- a/basic/src/lib.rs +++ b/basic/src/lib.rs @@ -48,7 +48,7 @@ use valida_machine::__internal::{ use valida_machine::{ generate_permutation_trace, verify_constraints, AdviceProvider, BusArgument, Chip, ChipProof, Commitments, Instruction, Machine, MachineProof, OpenedValues, ProgramROM, StoppingFlag, - ValidaAirBuilder, + ValidaAirBuilder, FailureReason, }; use valida_memory::{MachineWithMemoryChip, MemoryChip}; use valida_output::{MachineWithOutputChip, OutputChip, WriteInstruction}; @@ -665,7 +665,7 @@ impl Machine for BasicMachine { } } - fn verify(&self, config: &SC, proof: &MachineProof) -> Result<(), ()> + fn verify(&self, config: &SC, proof: &MachineProof) -> Result<(), FailureReason> where SC: StarkConfig, { @@ -828,7 +828,7 @@ impl Machine for BasicMachine { &proof.opening_proof, &mut challenger, ) - .map_err(|_| ())?; + .map_err(|_| FailureReason::FailureToVerifyMultiOpening)?; // Verify the constraints. let mut i = 0; @@ -1051,7 +1051,7 @@ impl Machine for BasicMachine { .sum(); if sum != SC::Challenge::zero() { - return Err(()); + return Err(FailureReason::CumulativeSumNonZero); } Ok(()) diff --git a/machine/src/machine.rs b/machine/src/machine.rs index 8122dbf..d7b1731 100644 --- a/machine/src/machine.rs +++ b/machine/src/machine.rs @@ -10,6 +10,12 @@ pub enum StoppingFlag { DidNotStop, } +#[derive(Debug)] +pub enum FailureReason { + CumulativeSumNonZero, + FailureToVerifyMultiOpening, +} + pub trait Machine: Sync { fn run(&mut self, program: &ProgramROM, advice: &mut Adv) where @@ -23,7 +29,7 @@ pub trait Machine: Sync { where SC: StarkConfig; - fn verify(&self, config: &SC, proof: &MachineProof) -> Result<(), ()> + fn verify(&self, config: &SC, proof: &MachineProof) -> Result<(), FailureReason> where SC: StarkConfig; } From 77fae7bcdbc674406f639bad20bd6e4693f24d63 Mon Sep 17 00:00:00 2001 From: Morgan Thomas Date: Thu, 11 Apr 2024 17:43:26 -0400 Subject: [PATCH 17/23] issue/140: wip: bugfix preprocessed stuff --- basic/src/lib.rs | 25 ++++++++++++++++--------- machine/src/config.rs | 1 + machine/src/machine.rs | 8 +++++--- 3 files changed, 22 insertions(+), 12 deletions(-) diff --git a/basic/src/lib.rs b/basic/src/lib.rs index fd07183..6a4318c 100644 --- a/basic/src/lib.rs +++ b/basic/src/lib.rs @@ -179,7 +179,7 @@ impl Machine for BasicMachine { // TODO: Seed challenger with digest of all constraints & trace lengths. let pcs = config.pcs(); - let preprocessed_traces: Vec> = + let mut preprocessed_traces: Vec> = tracing::info_span!("generate preprocessed traces").in_scope(|| { chips .par_iter() @@ -187,12 +187,6 @@ impl Machine for BasicMachine { .collect::>() }); - let (preprocessed_commit, preprocessed_data) = - tracing::info_span!("commit to preprocessed traces") - .in_scope(|| pcs.commit_batches(preprocessed_traces.to_vec())); - challenger.observe(preprocessed_commit.clone()); - let mut preprocessed_trace_ldes = pcs.get_ldes(&preprocessed_data); - let main_traces: [RowMajorMatrix; NUM_CHIPS] = tracing::info_span!("generate main trace").in_scope(|| { chips @@ -203,6 +197,18 @@ impl Machine for BasicMachine { .unwrap() }); + for (preprocessed_trace, main_trace) in preprocessed_traces.iter_mut().zip(main_traces.iter()) { + let w = preprocessed_trace.width(); + preprocessed_trace.values.resize(preprocessed_trace.width() * main_trace.height(), + SC::Val::zero()); + } + + let (preprocessed_commit, preprocessed_data) = + tracing::info_span!("commit to preprocessed traces") + .in_scope(|| pcs.commit_batches(preprocessed_traces.to_vec())); + challenger.observe(preprocessed_commit.clone()); + let mut preprocessed_trace_ldes = pcs.get_ldes(&preprocessed_data); + let degrees: [usize; NUM_CHIPS] = main_traces .iter() .map(|trace| trace.height()) @@ -665,7 +671,8 @@ impl Machine for BasicMachine { } } - fn verify(&self, config: &SC, proof: &MachineProof) -> Result<(), FailureReason> + fn verify(&self, config: &SC, proof: &MachineProof) + -> Result<(), FailureReason> where SC: StarkConfig, { @@ -828,7 +835,7 @@ impl Machine for BasicMachine { &proof.opening_proof, &mut challenger, ) - .map_err(|_| FailureReason::FailureToVerifyMultiOpening)?; + .map_err(FailureReason::FailureToVerifyMultiOpening)?; // Verify the constraints. let mut i = 0; diff --git a/machine/src/config.rs b/machine/src/config.rs index fbc5676..a2b74e4 100644 --- a/machine/src/config.rs +++ b/machine/src/config.rs @@ -30,6 +30,7 @@ pub trait StarkConfig { fn challenger(&self) -> Self::Challenger; } +#[derive(Debug)] pub struct StarkConfigImpl { pcs: Pcs, init_challenger: Challenger, diff --git a/machine/src/machine.rs b/machine/src/machine.rs index d7b1731..0f9a0e3 100644 --- a/machine/src/machine.rs +++ b/machine/src/machine.rs @@ -2,7 +2,9 @@ use crate::config::StarkConfig; use crate::program::ProgramROM; use crate::proof::MachineProof; use crate::AdviceProvider; +use p3_commit::Pcs; use p3_field::Field; +use p3_matrix::dense::RowMajorMatrix; #[derive(PartialEq, Eq)] pub enum StoppingFlag { @@ -11,9 +13,9 @@ pub enum StoppingFlag { } #[derive(Debug)] -pub enum FailureReason { +pub enum FailureReason { CumulativeSumNonZero, - FailureToVerifyMultiOpening, + FailureToVerifyMultiOpening(<::Pcs as Pcs>>::Error), } pub trait Machine: Sync { @@ -29,7 +31,7 @@ pub trait Machine: Sync { where SC: StarkConfig; - fn verify(&self, config: &SC, proof: &MachineProof) -> Result<(), FailureReason> + fn verify(&self, config: &SC, proof: &MachineProof) -> Result<(), FailureReason> where SC: StarkConfig; } From 11c2bedd3746225fa9db3c98e389649c7c787fd2 Mon Sep 17 00:00:00 2001 From: Morgan Thomas Date: Thu, 11 Apr 2024 18:09:44 -0400 Subject: [PATCH 18/23] issue/140: wip: bugfix preprocessed stuff --- basic/src/lib.rs | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) diff --git a/basic/src/lib.rs b/basic/src/lib.rs index 6a4318c..6576d6d 100644 --- a/basic/src/lib.rs +++ b/basic/src/lib.rs @@ -198,9 +198,7 @@ impl Machine for BasicMachine { }); for (preprocessed_trace, main_trace) in preprocessed_traces.iter_mut().zip(main_traces.iter()) { - let w = preprocessed_trace.width(); - preprocessed_trace.values.resize(preprocessed_trace.width() * main_trace.height(), - SC::Val::zero()); + preprocessed_trace.expand_to_height(main_trace.height()); } let (preprocessed_commit, preprocessed_data) = @@ -790,7 +788,7 @@ impl Machine for BasicMachine { } = &proof.commitments; // Compute the commitments to preprocessed traces (TODO: avoid in the future) - let preprocessed_traces: Vec> = + let mut preprocessed_traces: Vec> = tracing::info_span!("generate preprocessed traces").in_scope(|| { chips .par_iter() @@ -798,6 +796,10 @@ impl Machine for BasicMachine { .collect::>() }); + for (preprocessed_trace, dim) in preprocessed_traces.iter_mut().zip(dims[0].iter()) { + preprocessed_trace.expand_to_height(dim.height); + } + let (preprocessed_commit, preprocessed_data) = tracing::info_span!("commit to preprocessed traces") .in_scope(|| pcs.commit_batches(preprocessed_traces.to_vec())); From 35ce1c003a996aa8a0aa671672e41b30c6f6b62d Mon Sep 17 00:00:00 2001 From: Morgan Thomas Date: Thu, 11 Apr 2024 20:40:32 -0400 Subject: [PATCH 19/23] issue/140: wip: bugfix preprocessed stuff --- basic/src/lib.rs | 54 ++++++++++++++++++++++++++++++++++-------------- 1 file changed, 38 insertions(+), 16 deletions(-) diff --git a/basic/src/lib.rs b/basic/src/lib.rs index 6576d6d..be8d24c 100644 --- a/basic/src/lib.rs +++ b/basic/src/lib.rs @@ -717,7 +717,7 @@ impl Machine for BasicMachine { .map(|chip| chip.all_interactions(self)) .collect::>(); - let dims = &[ + let main_trace_dims = chips .iter() .zip(proof.chip_proofs.iter()) @@ -725,7 +725,33 @@ impl Machine for BasicMachine { width: chip.trace_width(), height: 1 << chip_proof.log_degree, }) - .collect::>(), + .collect::>(); + + // Compute the preprocessed traces (TODO: avoid in the future) + let mut preprocessed_traces: Vec> = + tracing::info_span!("generate preprocessed traces").in_scope(|| { + chips + .par_iter() + .map(|chip| chip.preprocessed_trace()) + .collect::>() + }); + + for (preprocessed_trace, dim) in preprocessed_traces.iter_mut().zip(main_trace_dims.iter()) { + preprocessed_trace.expand_to_height(dim.height); + } + + let preprocessed_trace_dims = + chips + .iter() + .zip(proof.chip_proofs.iter()) + .zip(preprocessed_traces.iter()) + .map(|((chip, chip_proof), preprocessed_trace)| Dimensions { + width: preprocessed_trace.width(), + height: 1 << chip_proof.log_degree, + }) + .collect::>(); + + let permutation_trace_dims = chips_interactions .iter() .zip(proof.chip_proofs.iter()) @@ -733,7 +759,9 @@ impl Machine for BasicMachine { width: (interactions.len() + 1) * SC::Challenge::D, height: 1 << chip_proof.log_degree, }) - .collect::>(), + .collect::>(); + + let quotient_dims = proof .chip_proofs .iter() @@ -742,7 +770,13 @@ impl Machine for BasicMachine { width: log_quotient_deg << SC::Challenge::D, height: 1 << chip_proof.log_degree, }) - .collect::>(), + .collect::>(); + + let dims = &[ + preprocessed_trace_dims, + main_trace_dims, + permutation_trace_dims, + quotient_dims, ]; // Get the generators of the trace subgroups for each chip. @@ -788,18 +822,6 @@ impl Machine for BasicMachine { } = &proof.commitments; // Compute the commitments to preprocessed traces (TODO: avoid in the future) - let mut preprocessed_traces: Vec> = - tracing::info_span!("generate preprocessed traces").in_scope(|| { - chips - .par_iter() - .map(|chip| chip.preprocessed_trace()) - .collect::>() - }); - - for (preprocessed_trace, dim) in preprocessed_traces.iter_mut().zip(dims[0].iter()) { - preprocessed_trace.expand_to_height(dim.height); - } - let (preprocessed_commit, preprocessed_data) = tracing::info_span!("commit to preprocessed traces") .in_scope(|| pcs.commit_batches(preprocessed_traces.to_vec())); From 0cadb44589ff17e20fb5ee7608d669fb3449e791 Mon Sep 17 00:00:00 2001 From: Morgan Thomas Date: Thu, 11 Apr 2024 21:04:21 -0400 Subject: [PATCH 20/23] issue/140: wip: bugfix preprocessed stuff --- basic/src/lib.rs | 30 +++++++++++++-------------- machine/src/quotient.rs | 45 +++++++++++++++++------------------------ 2 files changed, 34 insertions(+), 41 deletions(-) diff --git a/basic/src/lib.rs b/basic/src/lib.rs index be8d24c..d66db6b 100644 --- a/basic/src/lib.rs +++ b/basic/src/lib.rs @@ -277,7 +277,7 @@ impl Machine for BasicMachine { config, chip, log_degrees[i], - None::>, + preprocessed_trace_ldes.remove(0), main_trace_ldes.remove(0), perm_trace_ldes.remove(0), cumulative_sums[i], @@ -300,7 +300,7 @@ impl Machine for BasicMachine { config, chip, log_degrees[i], - Some(preprocessed_trace_ldes.remove(0)), + preprocessed_trace_ldes.remove(0), main_trace_ldes.remove(0), perm_trace_ldes.remove(0), cumulative_sums[i], @@ -323,7 +323,7 @@ impl Machine for BasicMachine { config, chip, log_degrees[i], - None::>, + preprocessed_trace_ldes.remove(0), main_trace_ldes.remove(0), perm_trace_ldes.remove(0), cumulative_sums[i], @@ -346,7 +346,7 @@ impl Machine for BasicMachine { config, chip, log_degrees[i], - None::>, + preprocessed_trace_ldes.remove(0), main_trace_ldes.remove(0), perm_trace_ldes.remove(0), cumulative_sums[i], @@ -369,7 +369,7 @@ impl Machine for BasicMachine { config, chip, log_degrees[i], - None::>, + preprocessed_trace_ldes.remove(0), main_trace_ldes.remove(0), perm_trace_ldes.remove(0), cumulative_sums[i], @@ -392,7 +392,7 @@ impl Machine for BasicMachine { config, chip, log_degrees[i], - None::>, + preprocessed_trace_ldes.remove(0), main_trace_ldes.remove(0), perm_trace_ldes.remove(0), cumulative_sums[i], @@ -415,7 +415,7 @@ impl Machine for BasicMachine { config, chip, log_degrees[i], - None::>, + preprocessed_trace_ldes.remove(0), main_trace_ldes.remove(0), perm_trace_ldes.remove(0), cumulative_sums[i], @@ -438,7 +438,7 @@ impl Machine for BasicMachine { config, chip, log_degrees[i], - None::>, + preprocessed_trace_ldes.remove(0), main_trace_ldes.remove(0), perm_trace_ldes.remove(0), cumulative_sums[i], @@ -461,7 +461,7 @@ impl Machine for BasicMachine { config, chip, log_degrees[i], - None::>, + preprocessed_trace_ldes.remove(0), main_trace_ldes.remove(0), perm_trace_ldes.remove(0), cumulative_sums[i], @@ -484,7 +484,7 @@ impl Machine for BasicMachine { config, chip, log_degrees[i], - None::>, + preprocessed_trace_ldes.remove(0), main_trace_ldes.remove(0), perm_trace_ldes.remove(0), cumulative_sums[i], @@ -507,7 +507,7 @@ impl Machine for BasicMachine { config, chip, log_degrees[i], - None::>, + preprocessed_trace_ldes.remove(0), main_trace_ldes.remove(0), perm_trace_ldes.remove(0), cumulative_sums[i], @@ -530,7 +530,7 @@ impl Machine for BasicMachine { config, chip, log_degrees[i], - None::>, + preprocessed_trace_ldes.remove(0), main_trace_ldes.remove(0), perm_trace_ldes.remove(0), cumulative_sums[i], @@ -553,7 +553,7 @@ impl Machine for BasicMachine { config, chip, log_degrees[i], - Some(preprocessed_trace_ldes.remove(0)), + preprocessed_trace_ldes.remove(0), main_trace_ldes.remove(0), perm_trace_ldes.remove(0), cumulative_sums[i], @@ -576,7 +576,7 @@ impl Machine for BasicMachine { config, chip, log_degrees[i], - None::>, + preprocessed_trace_ldes.remove(0), main_trace_ldes.remove(0), perm_trace_ldes.remove(0), cumulative_sums[i], @@ -616,7 +616,7 @@ impl Machine for BasicMachine { let [preprocessed_openings, main_openings, perm_openings, quotient_openings] = openings .try_into() - .expect("Should have 3 rounds of openings"); + .expect("Should have 4 rounds of openings"); let commitments = Commitments { preprocessed_trace: preprocessed_commit, diff --git a/machine/src/quotient.rs b/machine/src/quotient.rs index c7b1ead..eb7b9b3 100644 --- a/machine/src/quotient.rs +++ b/machine/src/quotient.rs @@ -20,7 +20,7 @@ pub fn quotient( config: &SC, air: &A, log_degree: usize, - preprocessed_trace_lde: Option, + preprocessed_trace_lde: PreprocessedTraceLde, main_trace_lde: MainTraceLde, perm_trace_lde: PermTraceLde, cumulative_sum: SC::Challenge, @@ -40,7 +40,7 @@ where let log_stride_for_quotient = pcs.log_blowup() - log_quotient_degree; let preprocessed_trace_lde_for_quotient = - preprocessed_trace_lde.map(|lde| lde.vertically_strided(1 << log_stride_for_quotient, 0)); + preprocessed_trace_lde.vertically_strided(1 << log_stride_for_quotient, 0); let main_trace_lde_for_quotient = main_trace_lde.vertically_strided(1 << log_stride_for_quotient, 0); let perm_trace_lde_for_quotient = @@ -74,7 +74,7 @@ fn quotient_values( air: &A, log_degree: usize, log_quotient_degree: usize, - preprocessed_trace_lde: Option, + preprocessed_trace_lde: PreprocessedTraceLde, main_trace_lde: MainTraceLde, perm_trace_lde: PermTraceLde, cumulative_sum: SC::Challenge, @@ -130,29 +130,22 @@ where let is_first_row = *SC::PackedVal::from_slice(&lagrange_first_evals[i_range.clone()]); let is_last_row = *SC::PackedVal::from_slice(&lagrange_last_evals[i_range]); - let (preprocessed_local, preprocessed_next): (Vec<_>, Vec<_>) = - match &preprocessed_trace_lde { - Some(lde) => { - let local = (0..lde.width()) - .map(|col| { - SC::PackedVal::from_fn(|offset| { - let row = wrap(i_local_start + offset); - lde.get(row, col) - }) - }) - .collect(); - let next = (0..lde.width()) - .map(|col| { - SC::PackedVal::from_fn(|offset| { - let row = wrap(i_next_start + offset); - lde.get(row, col) - }) - }) - .collect(); - (local, next) - } - None => (vec![], vec![]), - }; + let preprocessed_local: Vec<_> = (0..preprocessed_trace_lde.width()) + .map(|col| { + SC::PackedVal::from_fn(|offset| { + let row = wrap(i_local_start + offset); + preprocessed_trace_lde.get(row, col) + }) + }) + .collect(); + let preprocessed_next: Vec<_> = (0..preprocessed_trace_lde.width()) + .map(|col| { + SC::PackedVal::from_fn(|offset| { + let row = wrap(i_next_start + offset); + preprocessed_trace_lde.get(row, col) + }) + }) + .collect(); let main_local: Vec<_> = (0..main_trace_lde.width()) .map(|col| { From c1a47a09f40a242ea4cc89e3d96ba5ec0b07d7a4 Mon Sep 17 00:00:00 2001 From: Morgan Thomas Date: Thu, 11 Apr 2024 21:09:36 -0400 Subject: [PATCH 21/23] issue/140: wip: bugfix preprocessed stuff --- basic/src/lib.rs | 14 ++++++++++++++ machine/src/check_constraints.rs | 7 ++++--- 2 files changed, 18 insertions(+), 3 deletions(-) diff --git a/basic/src/lib.rs b/basic/src/lib.rs index d66db6b..b51478d 100644 --- a/basic/src/lib.rs +++ b/basic/src/lib.rs @@ -268,6 +268,7 @@ impl Machine for BasicMachine { check_constraints::( self, chip, + &preprocessed_traces[i], &main_traces[i], &perm_traces[i], &perm_challenges, @@ -291,6 +292,7 @@ impl Machine for BasicMachine { check_constraints::( self, chip, + &preprocessed_traces[i], &main_traces[i], &perm_traces[i], &perm_challenges, @@ -314,6 +316,7 @@ impl Machine for BasicMachine { check_constraints::( self, chip, + &preprocessed_traces[i], &main_traces[i], &perm_traces[i], &perm_challenges, @@ -337,6 +340,7 @@ impl Machine for BasicMachine { check_constraints::( self, chip, + &preprocessed_traces[i], &main_traces[i], &perm_traces[i], &perm_challenges, @@ -360,6 +364,7 @@ impl Machine for BasicMachine { check_constraints::( self, chip, + &preprocessed_traces[i], &main_traces[i], &perm_traces[i], &perm_challenges, @@ -383,6 +388,7 @@ impl Machine for BasicMachine { check_constraints::( self, chip, + &preprocessed_traces[i], &main_traces[i], &perm_traces[i], &perm_challenges, @@ -406,6 +412,7 @@ impl Machine for BasicMachine { check_constraints::( self, chip, + &preprocessed_traces[i], &main_traces[i], &perm_traces[i], &perm_challenges, @@ -429,6 +436,7 @@ impl Machine for BasicMachine { check_constraints::( self, chip, + &preprocessed_traces[i], &main_traces[i], &perm_traces[i], &perm_challenges, @@ -452,6 +460,7 @@ impl Machine for BasicMachine { check_constraints::( self, chip, + &preprocessed_traces[i], &main_traces[i], &perm_traces[i], &perm_challenges, @@ -475,6 +484,7 @@ impl Machine for BasicMachine { check_constraints::( self, chip, + &preprocessed_traces[i], &main_traces[i], &perm_traces[i], &perm_challenges, @@ -498,6 +508,7 @@ impl Machine for BasicMachine { check_constraints::( self, chip, + &preprocessed_traces[i], &main_traces[i], &perm_traces[i], &perm_challenges, @@ -521,6 +532,7 @@ impl Machine for BasicMachine { check_constraints::( self, chip, + &preprocessed_traces[i], &main_traces[i], &perm_traces[i], &perm_challenges, @@ -544,6 +556,7 @@ impl Machine for BasicMachine { check_constraints::( self, chip, + &preprocessed_traces[i], &main_traces[i], &perm_traces[i], &perm_challenges, @@ -567,6 +580,7 @@ impl Machine for BasicMachine { check_constraints::( self, chip, + &preprocessed_traces[i], &main_traces[i], &perm_traces[i], &perm_challenges, diff --git a/machine/src/check_constraints.rs b/machine/src/check_constraints.rs index ac4ca7b..a14c6db 100644 --- a/machine/src/check_constraints.rs +++ b/machine/src/check_constraints.rs @@ -14,6 +14,7 @@ use p3_maybe_rayon::prelude::*; pub fn check_constraints( machine: &M, air: &A, + preprocessed: &RowMajorMatrix, main: &RowMajorMatrix, perm: &RowMajorMatrix, perm_challenges: &[SC::Challenge], @@ -28,8 +29,8 @@ pub fn check_constraints( return; } - let preprocessed = air.preprocessed_trace(); let preprocessed_height = preprocessed.height(); + assert_eq!(height, preprocessed_height); let cumulative_sum = *perm.row_slice(perm.height() - 1).last().unwrap(); @@ -39,8 +40,8 @@ pub fn check_constraints( let main_local = main.row_slice(i); let main_next = main.row_slice(i_next); - let preprocessed_local = preprocessed.row_slice(i % preprocessed_height); - let preprocessed_next = preprocessed.row_slice(i_next % preprocessed_height); + let preprocessed_local = preprocessed.row_slice(i); + let preprocessed_next = preprocessed.row_slice(i_next); let perm_local = perm.row_slice(i); let perm_next = perm.row_slice(i_next); From 6dc45113bb2e279e882d0fff144162c5fb4cc2a8 Mon Sep 17 00:00:00 2001 From: Morgan Thomas Date: Sat, 13 Apr 2024 20:28:06 -0400 Subject: [PATCH 22/23] issue/140: add a redundant check of the preprocessed commitment (for more helpful errors when this happens) --- basic/src/lib.rs | 1 + 1 file changed, 1 insertion(+) diff --git a/basic/src/lib.rs b/basic/src/lib.rs index b51478d..06a0f07 100644 --- a/basic/src/lib.rs +++ b/basic/src/lib.rs @@ -839,6 +839,7 @@ impl Machine for BasicMachine { let (preprocessed_commit, preprocessed_data) = tracing::info_span!("commit to preprocessed traces") .in_scope(|| pcs.commit_batches(preprocessed_traces.to_vec())); + assert_eq!(preprocessed_commit, proof.commitments.preprocessed_trace); challenger.observe(preprocessed_commit.clone()); From c0a0abe692198afbb0b4dbeae82a48bb00a2ea40 Mon Sep 17 00:00:00 2001 From: Morgan Thomas Date: Mon, 15 Apr 2024 13:38:11 -0400 Subject: [PATCH 23/23] issue/140: wip: un-batch the opening proofs to figure out which one is the problem --- basic/src/lib.rs | 27 +++++++++++++++++++++------ machine/src/proof.rs | 11 ++++++++++- 2 files changed, 31 insertions(+), 7 deletions(-) diff --git a/basic/src/lib.rs b/basic/src/lib.rs index 06a0f07..fb434d5 100644 --- a/basic/src/lib.rs +++ b/basic/src/lib.rs @@ -625,12 +625,27 @@ impl Machine for BasicMachine { (&perm_data, zeta_and_next.as_slice()), ("ient_data, zeta_exp_quotient_degree.as_slice()), ]; - let (openings, opening_proof) = - pcs.open_multi_batches(&prover_data_and_points, &mut challenger); - - let [preprocessed_openings, main_openings, perm_openings, quotient_openings] = openings - .try_into() - .expect("Should have 4 rounds of openings"); + // let (openings, opening_proof) = + // pcs.open_multi_batches(&prover_data_and_points, &mut challenger); + + let (preprocessed_openings, preprocessed_opening_proof) = + pcs.open_multi_batches(&[(&preprocessed_data, zeta_and_next.as_slice())], + &mut challenger); + let [preprocessed_openings] = preprocessed_openings.try_into().expect("Should have 1 round opening"); + + let (main_openings, main_opening_proof) = + pcs.open_multi_batches(&[(&main_data, zeta_and_next.as_slice())], + &mut challenger); + let [main_openings] = main_openings.try_into().expect("Should have 1 round opening"); + + let (perm_openings, perm_opening_proof) = + pcs.open_multi_batches(&[(&perm_data, zeta_and_next.as_slice())], + &mut challenger); + let [perm_openings] = perm_openings.try_into().expect("Should have 1 round opening"); + + // let [preprocessed_openings, main_openings, perm_openings, quotient_openings] = openings + // .try_into() + // .expect("Should have 4 rounds of openings"); let commitments = Commitments { preprocessed_trace: preprocessed_commit, diff --git a/machine/src/proof.rs b/machine/src/proof.rs index 8b3b064..5cf0d54 100644 --- a/machine/src/proof.rs +++ b/machine/src/proof.rs @@ -13,10 +13,19 @@ type PcsProof = <::Pcs as Pcs, ValMat>>::Proo #[serde(bound = "SC::Challenge: Serialize + DeserializeOwned")] pub struct MachineProof { pub commitments: Commitments>, - pub opening_proof: PcsProof, + pub opening_proofs: OpeningProofs, pub chip_proofs: Vec>, } +#[derive(Serialize, Deserialize)] +#[serde(bound = "SC::Challenge: Serialize + DeserializeOwned")] +pub struct OpeningProofs { + pub preprocessed: PcsProof, + pub main: PcsProof, + pub perm: PcsProof, + pub quotient: PcsProof, +} + #[derive(Serialize, Deserialize)] pub struct Commitments { pub preprocessed_trace: Com,