diff --git a/circuits/src/cpu/generation.rs b/circuits/src/cpu/generation.rs index e4f9a62c0..98e02a3ab 100644 --- a/circuits/src/cpu/generation.rs +++ b/circuits/src/cpu/generation.rs @@ -73,7 +73,7 @@ pub fn generate_cpu_trace(record: &ExecutionRecord) -> Vec(record: &ExecutionRecord) -> Vec, const D: usize>( @@ -67,6 +68,8 @@ pub fn generate_traces, const D: usize>( let skeleton_rows = generate_cpu_skeleton_trace(record); let add_rows = ops::add::generate(record); let blt_taken_rows = ops::blt_taken::generate(record); + let store_word_rows = ops::sw::generate(&record.executed); + let load_word_rows = ops::lw::generate(&record.executed); let xor_rows = generate_xor_trace(&cpu_rows); let shift_amount_rows = generate_shift_amount_trace(&cpu_rows); let program_rows = generate_program_rom_trace(program); @@ -78,7 +81,6 @@ pub fn generate_traces, const D: usize>( let memory_zeroinit_rows = generate_memory_zero_init_trace(&record.executed, program); let halfword_memory_rows = generate_halfword_memory_trace(&record.executed); - let fullword_memory_rows = generate_fullword_memory_trace(&record.executed); let private_tape_rows = generate_private_tape_trace(&record.executed); let public_tape_rows = generate_public_tape_trace(&record.executed); let call_tape_rows = generate_call_tape_trace(&record.executed); @@ -95,7 +97,8 @@ pub fn generate_traces, const D: usize>( &memory_init, &memory_zeroinit_rows, &halfword_memory_rows, - &fullword_memory_rows, + &store_word_rows, + &load_word_rows, &private_tape_rows, &public_tape_rows, &call_tape_rows, @@ -112,6 +115,8 @@ pub fn generate_traces, const D: usize>( generate_register_trace( &cpu_rows, &add_rows, + &store_word_rows, + &load_word_rows, &blt_taken_rows, &poseiden2_sponge_rows, &private_tape_rows, @@ -128,6 +133,8 @@ pub fn generate_traces, const D: usize>( &cpu_rows, &add_rows, &blt_taken_rows, + &store_word_rows, + &load_word_rows, &memory_rows, ®ister_rows, ); @@ -136,6 +143,8 @@ pub fn generate_traces, const D: usize>( let rangecheck_u8_rows = generate_rangecheck_u8_trace(&rangecheck_rows, &memory_rows); let add_trace = ops::add::generate(record); let blt_trace = ops::blt_taken::generate(record); + let store_word_trace = ops::sw::generate(&record.executed); + let load_word_trace = ops::lw::generate(&record.executed); let tape_commitments_rows = generate_tape_commitments_trace(record); TableKindSetBuilder { @@ -150,7 +159,6 @@ pub fn generate_traces, const D: usize>( memory_zeroinit_stark: trace_rows_to_poly_values(memory_zeroinit_rows), rangecheck_u8_stark: trace_rows_to_poly_values(rangecheck_u8_rows), halfword_memory_stark: trace_rows_to_poly_values(halfword_memory_rows), - fullword_memory_stark: trace_rows_to_poly_values(fullword_memory_rows), private_tape_stark: trace_rows_to_poly_values(private_tape_rows), public_tape_stark: trace_rows_to_poly_values(public_tape_rows), call_tape_stark: trace_rows_to_poly_values(call_tape_rows), @@ -168,6 +176,8 @@ pub fn generate_traces, const D: usize>( cpu_skeleton_stark: trace_rows_to_poly_values(skeleton_rows), add_stark: trace_rows_to_poly_values(add_trace), blt_taken_stark: trace_rows_to_poly_values(blt_trace), + store_word_stark: trace_rows_to_poly_values(store_word_trace), + load_word_stark: trace_rows_to_poly_values(load_word_trace), tape_commitments_stark: trace_rows_to_poly_values(tape_commitments_rows), } .build() diff --git a/circuits/src/lib.rs b/circuits/src/lib.rs index db07c3cbc..c9460c53a 100644 --- a/circuits/src/lib.rs +++ b/circuits/src/lib.rs @@ -16,7 +16,6 @@ pub mod generation; pub mod linear_combination; pub mod linear_combination_typed; pub mod memory; -pub mod memory_fullword; pub mod memory_halfword; pub mod memory_zeroinit; pub mod memoryinit; diff --git a/circuits/src/memory/columns.rs b/circuits/src/memory/columns.rs index f2ea56ab8..72848d004 100644 --- a/circuits/src/memory/columns.rs +++ b/circuits/src/memory/columns.rs @@ -7,10 +7,11 @@ use plonky2::hash::poseidon2::Poseidon2Permutation; use crate::columns_view::{columns_view_impl, make_col_map}; use crate::cross_table_lookup::Column; -use crate::memory_fullword::columns::FullWordMemory; use crate::memory_halfword::columns::HalfWordMemory; use crate::memory_zeroinit::columns::MemoryZeroInit; use crate::memoryinit::columns::{MemoryInit, MemoryInitCtl}; +use crate::ops::lw::columns::LoadWord; +use crate::ops::sw::columns::StoreWord; use crate::poseidon2_output_bytes::columns::{Poseidon2OutputBytes, BYTES_COUNT}; use crate::poseidon2_sponge::columns::Poseidon2Sponge; use crate::rangecheck::columns::RangeCheckCtl; @@ -97,18 +98,35 @@ impl From<&HalfWordMemory> for Vec> { } } -impl From<&FullWordMemory> for Vec> { - fn from(val: &FullWordMemory) -> Self { - if (val.ops.is_load + val.ops.is_store).is_zero() { +impl From<&StoreWord> for Vec> { + fn from(val: &StoreWord) -> Self { + if (val.is_running).is_zero() { vec![] } else { - izip!(val.addrs, val.limbs) - .map(|(addr, value)| Memory { + izip!(0.., val.op1_limbs) + .map(|(i, limb)| Memory { clk: val.clk, - addr, + addr: val.address + F::from_canonical_u8(i), + value: limb, + is_store: F::ONE, + ..Default::default() + }) + .collect() + } + } +} + +impl From<&LoadWord> for Vec> { + fn from(val: &LoadWord) -> Self { + if (val.is_running).is_zero() { + vec![] + } else { + izip!(0.., val.dst_limbs) + .map(|(i, value)| Memory { + clk: val.clk, + addr: val.address + F::from_canonical_u8(i), value, - is_store: val.ops.is_store, - is_load: val.ops.is_load, + is_load: F::ONE, ..Default::default() }) .collect() diff --git a/circuits/src/memory/generation.rs b/circuits/src/memory/generation.rs index d6d7d4e98..09ee510f6 100644 --- a/circuits/src/memory/generation.rs +++ b/circuits/src/memory/generation.rs @@ -8,10 +8,11 @@ use plonky2::hash::hash_types::RichField; use crate::generation::MIN_TRACE_LENGTH; use crate::memory::columns::Memory; use crate::memory::trace::{get_memory_inst_addr, get_memory_inst_clk, get_memory_raw_value}; -use crate::memory_fullword::columns::FullWordMemory; use crate::memory_halfword::columns::HalfWordMemory; use crate::memory_zeroinit::columns::MemoryZeroInit; use crate::memoryinit::columns::MemoryInit; +use crate::ops::lw::columns::LoadWord; +use crate::ops::sw::columns::StoreWord; use crate::poseidon2_output_bytes::columns::Poseidon2OutputBytes; use crate::poseidon2_sponge::columns::Poseidon2Sponge; use crate::storage_device::columns::StorageDevice; @@ -115,12 +116,16 @@ pub fn transform_poseidon2_output_bytes( /// /// These need to be further interleaved with runtime memory trace generated /// from VM execution for final memory trace. -pub fn transform_fullword( - fullword_memory: &[FullWordMemory], +pub fn transform_sw( + store_word: &[StoreWord], ) -> impl Iterator> + '_ { - fullword_memory - .iter() - .flat_map(Into::>>::into) + store_word.iter().flat_map(Into::>>::into) +} + +pub fn transform_lw( + load_word: &[LoadWord], +) -> impl Iterator> + '_ { + load_word.iter().flat_map(Into::>>::into) } /// Generates Memory trace from a storage device table. @@ -153,7 +158,8 @@ pub fn generate_memory_trace( memory_init_rows: &[MemoryInit], memory_zeroinit_rows: &[MemoryZeroInit], halfword_memory_rows: &[HalfWordMemory], - fullword_memory_rows: &[FullWordMemory], + store_word_rows: &[StoreWord], + load_word_rows: &[LoadWord], private_tape_rows: &[StorageDevice], public_tape_rows: &[StorageDevice], call_tape_rows: &[StorageDevice], @@ -172,7 +178,8 @@ pub fn generate_memory_trace( transform_memory_zero_init(memory_zeroinit_rows), generate_memory_trace_from_execution(step_rows), transform_halfword(halfword_memory_rows), - transform_fullword(fullword_memory_rows), + transform_sw(store_word_rows), + transform_lw(load_word_rows), transform_storage(private_tape_rows), transform_storage(public_tape_rows), transform_storage(call_tape_rows), @@ -218,10 +225,10 @@ mod tests { use crate::memory::columns::Memory; use crate::memory::stark::MemoryStark; use crate::memory::test_utils::memory_trace_test_case; - use crate::memory_fullword::generation::generate_fullword_memory_trace; use crate::memory_halfword::generation::generate_halfword_memory_trace; use crate::memory_zeroinit::generation::generate_memory_zero_init_trace; use crate::memoryinit::generation::generate_memory_init_trace; + use crate::ops; use crate::poseidon2_output_bytes::generation::generate_poseidon2_output_bytes_trace; use crate::poseidon2_sponge::generation::generate_poseidon2_sponge_trace; use crate::stark::utils::trace_rows_to_poly_values; @@ -282,7 +289,9 @@ mod tests { let memory_zeroinit_rows = generate_memory_zero_init_trace(&record.executed, &program); let halfword_memory = generate_halfword_memory_trace(&record.executed); - let fullword_memory = generate_fullword_memory_trace(&record.executed); + let store_word_rows = ops::sw::generate(&record.executed); + let load_word_rows = ops::lw::generate(&record.executed + ); let private_tape_rows = generate_private_tape_trace(&record.executed); let public_tape_rows = generate_public_tape_trace(&record.executed); @@ -299,7 +308,8 @@ mod tests { &memory_init, &memory_zeroinit_rows, &halfword_memory, - &fullword_memory, + &store_word_rows, + &load_word_rows, &private_tape_rows, &public_tape_rows, &call_tape_rows, @@ -374,7 +384,8 @@ mod tests { let memory_zeroinit_rows = generate_memory_zero_init_trace(&[], &program); let halfword_memory = generate_halfword_memory_trace(&[]); - let fullword_memory = generate_fullword_memory_trace(&[]); + let store_word_rows = ops::sw::generate(&[]); + let load_word_rows = ops::lw::generate(&[]); let private_tape_rows = generate_private_tape_trace(&[]); let public_tape_rows = generate_public_tape_trace(&[]); let call_tape_rows = generate_call_tape_trace(&[]); @@ -390,7 +401,8 @@ mod tests { &memory_init, &memory_zeroinit_rows, &halfword_memory, - &fullword_memory, + &store_word_rows, + &load_word_rows, &private_tape_rows, &public_tape_rows, &call_tape_rows, diff --git a/circuits/src/memory_fullword/columns.rs b/circuits/src/memory_fullword/columns.rs deleted file mode 100644 index 223e4982e..000000000 --- a/circuits/src/memory_fullword/columns.rs +++ /dev/null @@ -1,81 +0,0 @@ -use core::ops::Add; - -use itertools::izip; - -use crate::columns_view::{columns_view_impl, make_col_map, NumberOfColumns}; -use crate::cross_table_lookup::ColumnWithTypedInput; -use crate::linear_combination::Column; -use crate::memory::columns::MemoryCtl; -use crate::stark::mozak_stark::{FullWordMemoryTable, TableWithTypedOutput}; - -/// Operations (one-hot encoded) -#[repr(C)] -#[derive(Clone, Copy, Eq, PartialEq, Debug, Default)] -pub struct Ops { - // One of `is_store`, `is_load` - // If none are `1`, it is a padding row - /// Binary filter column to represent a RISC-V SH operation. - pub is_store: T, - /// Binary filter column to represent a RISC-V LHU operation. - pub is_load: T, -} - -// TODO(roman): address_limbs & value columns can be optimized -// value == linear combination via range-check -// address_limbs also linear combination + forbid wrapping add -#[repr(C)] -#[derive(Clone, Copy, Eq, PartialEq, Debug)] -pub struct FullWordMemory { - /// Clock at memory access. - pub clk: T, - pub ops: Ops, - /// Memory addresses for the one byte limbs - pub addrs: [T; 4], - pub limbs: [T; 4], -} - -columns_view_impl!(FullWordMemory); -make_col_map!(FullWordMemory); - -impl> FullWordMemory { - pub fn is_executed(&self) -> T { - let ops = self.ops; - ops.is_load + ops.is_store - } -} - -/// Total number of columns. -pub const NUM_HW_MEM_COLS: usize = FullWordMemory::<()>::NUMBER_OF_COLUMNS; - -/// Columns containing the data which are looked from the CPU table into Memory -/// stark table. -#[must_use] -pub fn lookup_for_cpu() -> TableWithTypedOutput> { - FullWordMemoryTable::new( - MemoryCtl { - clk: COL_MAP.clk, - is_store: COL_MAP.ops.is_store, - is_load: COL_MAP.ops.is_load, - value: ColumnWithTypedInput::reduce_with_powers(COL_MAP.limbs, 1 << 8), - addr: COL_MAP.addrs[0], - }, - COL_MAP.is_executed(), - ) -} - -/// Lookup between fullword memory table -/// and Memory stark table. -pub fn lookup_for_memory_limb() -> impl Iterator>> { - izip!(COL_MAP.limbs, COL_MAP.addrs).map(|(value, addr)| { - FullWordMemoryTable::new( - MemoryCtl { - clk: COL_MAP.clk, - is_store: COL_MAP.ops.is_store, - is_load: COL_MAP.ops.is_load, - value, - addr, - }, - COL_MAP.is_executed(), - ) - }) -} diff --git a/circuits/src/memory_fullword/generation.rs b/circuits/src/memory_fullword/generation.rs deleted file mode 100644 index cc10aa940..000000000 --- a/circuits/src/memory_fullword/generation.rs +++ /dev/null @@ -1,241 +0,0 @@ -use itertools::Itertools; -use mozak_runner::instruction::Op; -use mozak_runner::vm::Row; -use plonky2::hash::hash_types::RichField; - -use crate::generation::MIN_TRACE_LENGTH; -use crate::memory::trace::get_memory_inst_clk; -use crate::memory_fullword::columns::{FullWordMemory, Ops}; - -/// Pad the memory trace to a power of 2. -#[must_use] -fn pad_mem_trace(mut trace: Vec>) -> Vec> { - trace.resize( - trace.len().next_power_of_two().max(MIN_TRACE_LENGTH), - FullWordMemory { - // Some columns need special treatment.. - ops: Ops::default(), - // .. and all other columns just have their last value duplicated. - ..trace.last().copied().unwrap_or_default() - }, - ); - trace -} - -/// Returns the rows with full word memory instructions. -pub fn filter_memory_trace(step_rows: &[Row]) -> impl Iterator> { - step_rows - .iter() - .filter(|row| matches!(row.instruction.op, Op::LW | Op::SW)) -} - -#[must_use] -pub fn generate_fullword_memory_trace( - step_rows: &[Row], -) -> Vec> { - pad_mem_trace( - filter_memory_trace(step_rows) - .map(|s| { - let op = s.instruction.op; - let base_addr = s.aux.mem.unwrap_or_default().addr; - let addrs = (0..4) - .map(|i| F::from_canonical_u32(base_addr.wrapping_add(i))) - .collect_vec() - .try_into() - .unwrap(); - let limbs = s - .aux - .dst_val - .to_le_bytes() - .into_iter() - .map(F::from_canonical_u8) - .collect_vec() - .try_into() - .unwrap(); - FullWordMemory { - clk: get_memory_inst_clk(s), - addrs, - ops: Ops { - is_store: F::from_bool(matches!(op, Op::SW)), - is_load: F::from_bool(matches!(op, Op::LW)), - }, - limbs, - } - }) - .collect_vec(), - ) -} -#[cfg(test)] -mod tests { - use mozak_runner::code; - use mozak_runner::elf::Program; - use mozak_runner::instruction::Op::{LW, SW}; - use mozak_runner::instruction::{Args, Instruction}; - use mozak_runner::vm::ExecutionRecord; - use plonky2::field::goldilocks_field::GoldilocksField; - - use crate::memory::generation::generate_memory_trace; - use crate::memory_fullword::generation::generate_fullword_memory_trace; - use crate::memory_halfword::generation::generate_halfword_memory_trace; - use crate::memory_zeroinit::generation::generate_memory_zero_init_trace; - use crate::memoryinit::generation::generate_memory_init_trace; - use crate::poseidon2_output_bytes::generation::generate_poseidon2_output_bytes_trace; - use crate::poseidon2_sponge::generation::generate_poseidon2_sponge_trace; - use crate::storage_device::generation::{ - generate_call_tape_trace, generate_cast_list_commitment_tape_trace, - generate_event_tape_trace, generate_events_commitment_tape_trace, - generate_private_tape_trace, generate_public_tape_trace, generate_self_prog_id_tape_trace, - }; - use crate::test_utils::prep_table; - - // TODO(Matthias): Consider unifying with the byte memory example? - #[must_use] - pub fn fullword_memory_trace_test_case( - repeats: usize, - ) -> (Program, ExecutionRecord) { - let new = Instruction::new; - let instructions = [ - new(SW, Args { - // addr = rs2 + imm, value = rs1-value - // store-full-word of address = 100, value 0x0a0b_0c0d - rs1: 1, - imm: 600, - ..Args::default() - }), - new(LW, Args { - // addr = rs2 + imm, value = rd-value - // load-full-word from address = 100 to reg-3, value of 0x0a0b_0c0d - rd: 3, - imm: 600, - ..Args::default() - }), - new(SW, Args { - // addr = rs2 + imm, value = rs1 - // store-full-word of address = 200, value 0x0102_0304 - rs1: 2, - imm: 700, - ..Args::default() - }), - new(LW, Args { - // addr = rs2 + imm, value = rd - // load-full-word from address = 200 to reg-4, value of 0x0102_0304 - rd: 4, - imm: 700, - ..Args::default() - }), - ]; - let code = std::iter::repeat(&instructions) - .take(repeats) - .flatten() - .copied() - .collect::>(); - let (program, record) = code::execute( - code, - &[ - (600, 0), - (601, 0), - (602, 0), - (603, 0), - (700, 0), - (701, 0), - (702, 0), - (703, 0), - ], - &[ - (1, 0x0a0b_0c0d), - (2, 0x0102_0304), - (3, 0xFFFF), - (4, 0x0000_FFFF), - ], - ); - - if repeats > 0 { - let state = &record.last_state; - assert_eq!(state.load_u32(600), 0x0a0b_0c0d); - assert_eq!(state.get_register_value(3), 0x0a0b_0c0d); - assert_eq!(state.load_u32(700), 0x0102_0304); - assert_eq!(state.get_register_value(4), 0x0102_0304); - } - (program, record) - } - - // This test simulates the scenario of a set of instructions - // which perform store byte (SB) and load byte unsigned (LBU) operations - // to memory and then checks if the memory trace is generated correctly. - #[test] - #[rustfmt::skip] - fn generate_full_memory_trace() { - let (program, record) = fullword_memory_trace_test_case(1); - - let memory_init = generate_memory_init_trace(&program); - let memory_zeroinit_rows = generate_memory_zero_init_trace(&record.executed, &program); - - let halfword_memory = generate_halfword_memory_trace(&record.executed); - let fullword_memory = generate_fullword_memory_trace(&record.executed); - let private_tape_rows = generate_private_tape_trace(&record.executed); - let public_tape_rows= generate_public_tape_trace(&record.executed); - let call_tape_rows = generate_call_tape_trace(&record.executed); - let event_tape_rows = generate_event_tape_trace(&record.executed); - let events_commitment_tape_rows = generate_events_commitment_tape_trace(&record.executed); - let cast_list_commitment_tape_rows = - generate_cast_list_commitment_tape_trace(&record.executed); - let self_prog_id_tape_rows = generate_self_prog_id_tape_trace(&record.executed); - let poseidon2_rows = generate_poseidon2_sponge_trace(&record.executed); - let poseidon2_output_bytes = generate_poseidon2_output_bytes_trace(&poseidon2_rows); - let trace = generate_memory_trace::( - &record.executed, - &memory_init, - &memory_zeroinit_rows, - &halfword_memory, - &fullword_memory, - &private_tape_rows, - &public_tape_rows, - &call_tape_rows, - &event_tape_rows, - &events_commitment_tape_rows, - &cast_list_commitment_tape_rows, - &self_prog_id_tape_rows, - &poseidon2_rows, - &poseidon2_output_bytes, - ); - let last = u64::from(u32::MAX); - assert_eq!( - trace, - prep_table(vec![ - //is_writable addr clk is_store, is_load, is_init value - [ 1, 0, 0, 0, 0, 1, 0], // Memory Init: 0 - [ 1, 600, 1, 0, 0, 1, 0], // Memory Init: 600 - [ 1, 600, 2, 1, 0, 0, 13], // Operations: 600 - [ 1, 600, 3, 0, 1, 0, 13], // Operations: 600 - [ 1, 601, 1, 0, 0, 1, 0], // Memory Init: 601 - [ 1, 601, 2, 1, 0, 0, 12], // Operations: 601 - [ 1, 601, 3, 0, 1, 0, 12], // Operations: 601 - [ 1, 602, 1, 0, 0, 1, 0], // Memory Init: 602 - [ 1, 602, 2, 1, 0, 0, 11], // Operations: 602 - [ 1, 602, 3, 0, 1, 0, 11], // Operations: 603 - [ 1, 603, 1, 0, 0, 1, 0], // Memory Init: 603 - [ 1, 603, 2, 1, 0, 0, 10], // Operations: 603 - [ 1, 603, 3, 0, 1, 0, 10], // Operations: 603 - [ 1, 700, 1, 0, 0, 1, 0], // Memory Init: 700 - [ 1, 700, 4, 1, 0, 0, 4], // Operations: 700 - [ 1, 700, 5, 0, 1, 0, 4], // Operations: 700 - [ 1, 701, 1, 0, 0, 1, 0], // Memory Init: 701 - [ 1, 701, 4, 1, 0, 0, 3], // Operations: 701 - [ 1, 701, 5, 0, 1, 0, 3], // Operations: 701 - [ 1, 702, 1, 0, 0, 1, 0], // Memory Init: 702 - [ 1, 702, 4, 1, 0, 0, 2], // Operations: 702 - [ 1, 702, 5, 0, 1, 0, 2], // Operations: 703 - [ 1, 703, 1, 0, 0, 1, 0], // Memory Init: 703 - [ 1, 703, 4, 1, 0, 0, 1], // Operations: 703 - [ 1, 703, 5, 0, 1, 0, 1], // Operations: 703 - [ 1, last, 0, 0, 0, 1, 0], // Memory Init: last - [ 1, last, 0, 0, 0, 0, 0], // padding - [ 1, last, 0, 0, 0, 0, 0], // padding - [ 1, last, 0, 0, 0, 0, 0], // padding - [ 1, last, 0, 0, 0, 0, 0], // padding - [ 1, last, 0, 0, 0, 0, 0], // padding - [ 1, last, 0, 0, 0, 0, 0], // padding - ]) - ); - } -} diff --git a/circuits/src/memory_fullword/mod.rs b/circuits/src/memory_fullword/mod.rs deleted file mode 100644 index dbb6f4019..000000000 --- a/circuits/src/memory_fullword/mod.rs +++ /dev/null @@ -1,8 +0,0 @@ -//! This module contains the **`Fullword-Memory` STARK Table**. -//! This Stark is used to store the VM Memory and -//! constrains the load and store operations by the CPU -//! using the CTL (cross table lookup) technique. - -pub mod columns; -pub mod generation; -pub mod stark; diff --git a/circuits/src/memory_fullword/stark.rs b/circuits/src/memory_fullword/stark.rs deleted file mode 100644 index 2f76c68fa..000000000 --- a/circuits/src/memory_fullword/stark.rs +++ /dev/null @@ -1,154 +0,0 @@ -use std::marker::PhantomData; - -use expr::{Expr, ExprBuilder, StarkFrameTyped}; -use itertools::izip; -use mozak_circuits_derive::StarkNameDisplay; -use plonky2::field::extension::{Extendable, FieldExtension}; -use plonky2::field::packed::PackedField; -use plonky2::hash::hash_types::RichField; -use plonky2::iop::ext_target::ExtensionTarget; -use plonky2::plonk::circuit_builder::CircuitBuilder; -use starky::constraint_consumer::{ConstraintConsumer, RecursiveConstraintConsumer}; -use starky::evaluation_frame::StarkFrame; -use starky::stark::Stark; - -use crate::columns_view::HasNamedColumns; -use crate::expr::{build_ext, build_packed, ConstraintBuilder}; -use crate::memory_fullword::columns::{FullWordMemory, NUM_HW_MEM_COLS}; -use crate::unstark::NoColumns; - -#[derive(Copy, Clone, Default, StarkNameDisplay)] -#[allow(clippy::module_name_repetitions)] -pub struct FullWordMemoryStark { - pub _f: PhantomData, -} - -impl HasNamedColumns for FullWordMemoryStark { - type Columns = FullWordMemory; -} - -const COLUMNS: usize = NUM_HW_MEM_COLS; -const PUBLIC_INPUTS: usize = 0; - -// Design description - https://docs.google.com/presentation/d/1J0BJd49BMQh3UR5TrOhe3k67plHxnohFtFVrMpDJ1oc/edit?usp=sharing -fn generate_constraints<'a, T: Copy>( - vars: &StarkFrameTyped>, NoColumns>>, -) -> ConstraintBuilder> { - let lv = vars.local_values; - let mut constraints = ConstraintBuilder::default(); - - constraints.always(lv.ops.is_store.is_binary()); - constraints.always(lv.ops.is_load.is_binary()); - constraints.always(lv.is_executed().is_binary()); - - // Check: the resulting sum is wrapped if necessary. - // As the result is range checked, this make the choice deterministic, - // even for a malicious prover. - for (i, addr) in izip!(0.., lv.addrs).skip(1) { - let target = lv.addrs[0] + i; - constraints.always(lv.is_executed() * (addr - target) * (addr + (1 << 32) - target)); - } - - constraints -} - -impl, const D: usize> Stark for FullWordMemoryStark { - type EvaluationFrame = StarkFrame - - where - FE: FieldExtension, - P: PackedField; - type EvaluationFrameTarget = - StarkFrame, ExtensionTarget, COLUMNS, PUBLIC_INPUTS>; - - // Design description - https://docs.google.com/presentation/d/1J0BJd49BMQh3UR5TrOhe3k67plHxnohFtFVrMpDJ1oc/edit?usp=sharing - fn eval_packed_generic( - &self, - vars: &Self::EvaluationFrame, - consumer: &mut ConstraintConsumer

, - ) where - FE: FieldExtension, - P: PackedField, { - let eb = ExprBuilder::default(); - let constraints = generate_constraints(&eb.to_typed_starkframe(vars)); - build_packed(constraints, consumer); - } - - fn eval_ext_circuit( - &self, - builder: &mut CircuitBuilder, - vars: &Self::EvaluationFrameTarget, - consumer: &mut RecursiveConstraintConsumer, - ) { - let eb = ExprBuilder::default(); - let constraints = generate_constraints(&eb.to_typed_starkframe(vars)); - build_ext(constraints, builder, consumer); - } - - fn constraint_degree(&self) -> usize { 3 } -} - -#[cfg(test)] -mod tests { - use mozak_runner::code; - use mozak_runner::instruction::{Args, Instruction, Op}; - use mozak_runner::test_utils::{u32_extra, u8_extra}; - use plonky2::plonk::config::Poseidon2GoldilocksConfig; - use proptest::prelude::ProptestConfig; - use proptest::proptest; - use starky::stark_testing::test_stark_circuit_constraints; - - use crate::memory_fullword::stark::FullWordMemoryStark; - use crate::stark::mozak_stark::MozakStark; - use crate::test_utils::{ProveAndVerify, D, F}; - - pub fn prove_mem_read_write(offset: u32, imm: u32, content: u8) { - let (program, record) = code::execute( - [ - Instruction { - op: Op::SW, - args: Args { - rs1: 1, - rs2: 2, - imm, - ..Args::default() - }, - }, - Instruction { - op: Op::LW, - args: Args { - rs2: 2, - imm, - ..Args::default() - }, - }, - ], - &[ - (imm.wrapping_add(offset), 0), - (imm.wrapping_add(offset).wrapping_add(1), 0), - (imm.wrapping_add(offset).wrapping_add(2), 0), - (imm.wrapping_add(offset).wrapping_add(3), 0), - ], - &[(1, content.into()), (2, offset)], - ); - - Stark::prove_and_verify(&program, &record).unwrap(); - } - proptest! { - #![proptest_config(ProptestConfig::with_cases(1))] - #[test] - fn prove_mem_read_write_mozak(offset in u32_extra(), imm in u32_extra(), content in u8_extra()) { - prove_mem_read_write::>(offset, imm, content); - } - } - - #[test] - fn test_circuit() -> anyhow::Result<()> { - type C = Poseidon2GoldilocksConfig; - type S = FullWordMemoryStark; - let stark = S::default(); - test_stark_circuit_constraints::(stark)?; - - Ok(()) - } -} diff --git a/circuits/src/memory_halfword/columns.rs b/circuits/src/memory_halfword/columns.rs index 9623d5830..fe6955408 100644 --- a/circuits/src/memory_halfword/columns.rs +++ b/circuits/src/memory_halfword/columns.rs @@ -9,9 +9,10 @@ use crate::memory::columns::MemoryCtl; use crate::stark::mozak_stark::{HalfWordMemoryTable, TableWithTypedOutput}; // use crate::stark::mozak_stark::{HalfWordMemoryTable, Table}; +columns_view_impl!(Ops); /// Operations (one-hot encoded) #[repr(C)] -#[derive(Clone, Copy, Eq, PartialEq, Debug, Default)] +#[derive(Clone, Copy, Eq, PartialEq, Debug)] pub struct Ops { // One of `is_store`, `is_load_u` // If none are `1`, it is a padding row diff --git a/circuits/src/memory_halfword/generation.rs b/circuits/src/memory_halfword/generation.rs index ecdb0d24b..ff0c5ead9 100644 --- a/circuits/src/memory_halfword/generation.rs +++ b/circuits/src/memory_halfword/generation.rs @@ -71,10 +71,10 @@ mod tests { use plonky2::field::goldilocks_field::GoldilocksField; use crate::memory::generation::generate_memory_trace; - use crate::memory_fullword::generation::generate_fullword_memory_trace; use crate::memory_halfword::generation::generate_halfword_memory_trace; use crate::memory_zeroinit::generation::generate_memory_zero_init_trace; use crate::memoryinit::generation::generate_memory_init_trace; + use crate::ops; use crate::poseidon2_output_bytes::generation::generate_poseidon2_output_bytes_trace; use crate::poseidon2_sponge::generation::generate_poseidon2_sponge_trace; use crate::storage_device::generation::{ @@ -162,7 +162,8 @@ mod tests { let memory_zeroinit_rows = generate_memory_zero_init_trace(&record.executed, &program); let halfword_memory = generate_halfword_memory_trace(&record.executed); - let fullword_memory = generate_fullword_memory_trace(&record.executed); + let store_word_rows = ops::sw::generate(&record.executed); + let load_word_rows = ops::lw::generate(&record.executed); let private_tape_rows = generate_private_tape_trace(&record.executed); let public_tape_rows = generate_public_tape_trace(&record.executed); let call_tape_rows = generate_call_tape_trace(&record.executed); @@ -179,7 +180,8 @@ mod tests { &memory_init, &memory_zeroinit_rows, &halfword_memory, - &fullword_memory, + &store_word_rows, + &load_word_rows, &private_tape_rows, &public_tape_rows, &call_tape_rows, diff --git a/circuits/src/ops/add/mod.rs b/circuits/src/ops/add/mod.rs index 2d9a71c53..4dc534988 100644 --- a/circuits/src/ops/add/mod.rs +++ b/circuits/src/ops/add/mod.rs @@ -15,16 +15,10 @@ pub mod columns { #[repr(C)] #[derive(Clone, Copy, Eq, PartialEq, Debug)] pub struct Instruction { - /// The original instruction (+ `imm_value`) used for program - /// cross-table-lookup. pub pc: T, - /// Selects the register to use as source for `rs1` pub rs1_selected: T, - /// Selects the register to use as source for `rs2` pub rs2_selected: T, - /// Selects the register to use as destination for `rd` pub rd_selected: T, - /// Special immediate value used for code constants pub imm_value: T, } diff --git a/circuits/src/ops/lw/mod.rs b/circuits/src/ops/lw/mod.rs new file mode 100644 index 000000000..f5f18bc10 --- /dev/null +++ b/circuits/src/ops/lw/mod.rs @@ -0,0 +1,191 @@ +pub mod stark; + +pub mod columns { + + use crate::columns_view::{columns_view_impl, make_col_map}; + use crate::cpu_skeleton::columns::CpuSkeletonCtl; + use crate::linear_combination::Column; + use crate::linear_combination_typed::ColumnWithTypedInput; + use crate::memory::columns::MemoryCtl; + use crate::program::columns::ProgramRom; + use crate::rangecheck::columns::RangeCheckCtl; + use crate::register::RegisterCtl; + use crate::stark::mozak_stark::{LoadWordTable, TableWithTypedOutput}; + + columns_view_impl!(Instruction); + #[repr(C)] + #[derive(Clone, Copy, Eq, PartialEq, Debug)] + pub struct Instruction { + pub pc: T, + pub rs2_selected: T, + pub rd_selected: T, + pub imm_value: T, + } + + make_col_map!(LoadWord); + columns_view_impl!(LoadWord); + #[repr(C)] + #[derive(Clone, Copy, Eq, PartialEq, Debug)] + pub struct LoadWord { + pub inst: Instruction, + pub clk: T, + pub op2_value: T, + pub dst_limbs: [T; 4], + // Extra column, so we can do CTL, like range check and memory. + pub address: T, + + pub is_running: T, + } + + #[must_use] + pub fn register_looking() -> Vec>> { + let is_read = ColumnWithTypedInput::constant(1); + let is_write = ColumnWithTypedInput::constant(2); + + vec![ + LoadWordTable::new( + RegisterCtl { + clk: COL_MAP.clk, + op: is_read, + addr: COL_MAP.inst.rs2_selected, + value: COL_MAP.op2_value, + }, + COL_MAP.is_running, + ), + LoadWordTable::new( + RegisterCtl { + clk: COL_MAP.clk, + op: is_write, + addr: COL_MAP.inst.rd_selected, + value: ColumnWithTypedInput::reduce_with_powers(COL_MAP.dst_limbs, 1 << 8), + }, + COL_MAP.is_running, + ), + ] + } + + #[must_use] + pub fn rangecheck_looking() -> Vec>> { + vec![LoadWordTable::new( + RangeCheckCtl(COL_MAP.address), + COL_MAP.is_running, + )] + } + + #[must_use] + pub fn lookup_for_skeleton() -> TableWithTypedOutput> { + LoadWordTable::new( + CpuSkeletonCtl { + clk: COL_MAP.clk, + pc: COL_MAP.inst.pc, + new_pc: COL_MAP.inst.pc + 4, + will_halt: ColumnWithTypedInput::constant(0), + }, + COL_MAP.is_running, + ) + } + + #[must_use] + pub fn lookup_for_program_rom() -> TableWithTypedOutput> { + let inst = COL_MAP.inst; + LoadWordTable::new( + ProgramRom { + pc: inst.pc, + // Combine columns into a single column. + // - ops: This is an internal opcode, not the opcode from RISC-V, and can fit within + // 5 bits. + // - is_op1_signed and is_op2_signed: These fields occupy 1 bit each. + // - rs1_select, rs2_select, and rd_select: These fields require 5 bits each. + // - imm_value: This field requires 32 bits. + // Therefore, the total bit requirement is 5 * 6 + 32 = 62 bits, which is less than + // the size of the Goldilocks field. + // Note: The imm_value field, having more than 5 bits, must be positioned as the + // last column in the list to ensure the correct functioning of + // 'reduce_with_powers'. + inst_data: ColumnWithTypedInput::reduce_with_powers( + [ + // TODO: don't hard-code Ops like this. + ColumnWithTypedInput::constant(21), + // TODO: use a struct here to name the components, and make IntoIterator, + // like we do with our stark tables. + ColumnWithTypedInput::constant(0), + ColumnWithTypedInput::constant(0), + ColumnWithTypedInput::constant(0), + inst.rs2_selected, + inst.rd_selected, + inst.imm_value, + ], + 1 << 5, + ), + }, + COL_MAP.is_running, + ) + } + + /// Lookup between Store Word memory table + /// and Memory stark table. + #[must_use] + pub fn lookup_for_memory_limb() -> Vec>> { + (0..4) + .map(|limb_index| { + LoadWordTable::new( + MemoryCtl { + clk: COL_MAP.clk, + is_store: ColumnWithTypedInput::constant(0), + is_load: ColumnWithTypedInput::constant(1), + value: COL_MAP.dst_limbs[limb_index], + addr: COL_MAP.address + i64::try_from(limb_index).unwrap(), + }, + COL_MAP.is_running, + ) + }) + .collect() + } +} + +use columns::{Instruction, LoadWord}; +use mozak_runner::instruction::Op; +use mozak_runner::vm::Row; +use plonky2::hash::hash_types::RichField; + +use crate::utils::pad_trace_with_default; + +#[must_use] +pub fn generate(executed: &[Row]) -> Vec> { + let mut trace: Vec> = vec![]; + for Row { + state, + instruction: inst, + aux, + } in executed + { + if let Op::LW = inst.op { + let rs2_selected = inst.args.rs2; + let rd_selected = inst.args.rd; + let op2_value = state.get_register_value(rs2_selected); + let imm_value = inst.args.imm; + let address = aux.mem.unwrap().addr; + let dst_value = aux.mem.unwrap().raw_value; + let dst_value_from_aux = aux.dst_val; + assert_eq!(dst_value, dst_value_from_aux); + assert_eq!(address, op2_value.wrapping_add(imm_value)); + let dst_limbs = aux.dst_val.to_le_bytes().map(u32::from); + let row = LoadWord { + inst: Instruction { + pc: state.get_pc(), + rs2_selected: u32::from(rs2_selected), + rd_selected: u32::from(rd_selected), + imm_value, + }, + clk: u32::try_from(state.clk).unwrap(), + op2_value, + address, + dst_limbs, + is_running: 1, + } + .map(F::from_canonical_u32); + trace.push(row); + } + } + pad_trace_with_default(trace) +} diff --git a/circuits/src/ops/lw/stark.rs b/circuits/src/ops/lw/stark.rs new file mode 100644 index 000000000..cb1033c84 --- /dev/null +++ b/circuits/src/ops/lw/stark.rs @@ -0,0 +1,82 @@ +use std::marker::PhantomData; + +use expr::{Expr, ExprBuilder, StarkFrameTyped}; +use mozak_circuits_derive::StarkNameDisplay; +use plonky2::field::extension::{Extendable, FieldExtension}; +use plonky2::field::packed::PackedField; +use plonky2::hash::hash_types::RichField; +use plonky2::iop::ext_target::ExtensionTarget; +use plonky2::plonk::circuit_builder::CircuitBuilder; +use starky::constraint_consumer::{ConstraintConsumer, RecursiveConstraintConsumer}; +use starky::evaluation_frame::StarkFrame; +use starky::stark::Stark; + +use super::columns::LoadWord; +use crate::columns_view::{HasNamedColumns, NumberOfColumns}; +use crate::expr::{build_ext, build_packed, ConstraintBuilder}; +use crate::unstark::NoColumns; + +#[derive(Copy, Clone, Default, StarkNameDisplay)] +#[allow(clippy::module_name_repetitions)] +pub struct LoadWordStark { + pub _f: PhantomData, +} + +impl HasNamedColumns for LoadWordStark { + type Columns = LoadWord; +} + +const COLUMNS: usize = LoadWord::<()>::NUMBER_OF_COLUMNS; +const PUBLIC_INPUTS: usize = 0; + +fn generate_constraints<'a, T: Copy>( + vars: &StarkFrameTyped>, NoColumns>>, +) -> ConstraintBuilder> { + let lv = vars.local_values; + let mut constraints = ConstraintBuilder::default(); + + let address_overflowing = lv.op2_value + lv.inst.imm_value; + let wrapped = address_overflowing - (1 << 32); + + // Check: the resulting sum is wrapped if necessary. + // As the result is range checked, this make the choice deterministic, + // even for a malicious prover. + constraints.always((lv.address - address_overflowing) * (lv.address - wrapped)); + + constraints +} + +impl, const D: usize> Stark for LoadWordStark { + type EvaluationFrame = StarkFrame + + where + FE: FieldExtension, + P: PackedField; + type EvaluationFrameTarget = + StarkFrame, ExtensionTarget, COLUMNS, PUBLIC_INPUTS>; + + fn eval_packed_generic( + &self, + vars: &Self::EvaluationFrame, + constraint_consumer: &mut ConstraintConsumer

, + ) where + FE: FieldExtension, + P: PackedField, { + let expr_builder = ExprBuilder::default(); + let constraints = generate_constraints(&expr_builder.to_typed_starkframe(vars)); + build_packed(constraints, constraint_consumer); + } + + fn eval_ext_circuit( + &self, + circuit_builder: &mut CircuitBuilder, + vars: &Self::EvaluationFrameTarget, + constraint_consumer: &mut RecursiveConstraintConsumer, + ) { + let expr_builder = ExprBuilder::default(); + let constraints = generate_constraints(&expr_builder.to_typed_starkframe(vars)); + build_ext(constraints, circuit_builder, constraint_consumer); + } + + fn constraint_degree(&self) -> usize { 3 } +} diff --git a/circuits/src/ops/mod.rs b/circuits/src/ops/mod.rs index 2dee7e7a5..62a920e94 100644 --- a/circuits/src/ops/mod.rs +++ b/circuits/src/ops/mod.rs @@ -1,2 +1,4 @@ pub mod add; pub mod blt_taken; +pub mod lw; +pub mod sw; diff --git a/circuits/src/ops/sw/mod.rs b/circuits/src/ops/sw/mod.rs new file mode 100644 index 000000000..2222e8060 --- /dev/null +++ b/circuits/src/ops/sw/mod.rs @@ -0,0 +1,194 @@ +pub mod stark; + +pub mod columns { + + use crate::columns_view::{columns_view_impl, make_col_map}; + use crate::cpu_skeleton::columns::CpuSkeletonCtl; + use crate::linear_combination::Column; + use crate::linear_combination_typed::ColumnWithTypedInput; + use crate::memory::columns::MemoryCtl; + use crate::program::columns::ProgramRom; + use crate::rangecheck::columns::RangeCheckCtl; + // use crate::rangecheck::columns::RangeCheckCtl; + use crate::register::RegisterCtl; + use crate::stark::mozak_stark::{StoreWordTable, TableWithTypedOutput}; + + columns_view_impl!(Instruction); + #[repr(C)] + #[derive(Clone, Copy, Eq, PartialEq, Debug)] + pub struct Instruction { + /// The original instruction (+ `imm_value`) used for program + /// cross-table-lookup. + pub pc: T, + /// Selects the register to use as source for `rs1` + pub rs1_selected: T, + /// Selects the register to use as source for `rs2` + pub rs2_selected: T, + /// Special immediate value used for code constants + pub imm_value: T, + } + + make_col_map!(StoreWord); + columns_view_impl!(StoreWord); + #[repr(C)] + #[derive(Clone, Copy, Eq, PartialEq, Debug)] + pub struct StoreWord { + pub inst: Instruction, + pub clk: T, + pub op1_limbs: [T; 4], + pub op2_value: T, + // Extra column, so we can do CTL, like range check and memory. + pub address: T, + + pub is_running: T, + } + + #[must_use] + pub fn register_looking() -> Vec>> { + let is_read = ColumnWithTypedInput::constant(1); + + vec![ + StoreWordTable::new( + RegisterCtl { + clk: COL_MAP.clk, + op: is_read, + addr: COL_MAP.inst.rs1_selected, + value: ColumnWithTypedInput::reduce_with_powers(COL_MAP.op1_limbs, 1 << 8), + }, + COL_MAP.is_running, + ), + StoreWordTable::new( + RegisterCtl { + clk: COL_MAP.clk, + op: is_read, + addr: COL_MAP.inst.rs2_selected, + value: COL_MAP.op2_value, + }, + COL_MAP.is_running, + ), + ] + } + + #[must_use] + pub fn rangecheck_looking() -> Vec>> { + vec![StoreWordTable::new( + RangeCheckCtl(COL_MAP.address), + COL_MAP.is_running, + )] + } + + #[must_use] + pub fn lookup_for_skeleton() -> TableWithTypedOutput> { + StoreWordTable::new( + CpuSkeletonCtl { + clk: COL_MAP.clk, + pc: COL_MAP.inst.pc, + new_pc: COL_MAP.inst.pc + 4, + will_halt: ColumnWithTypedInput::constant(0), + }, + COL_MAP.is_running, + ) + } + + #[must_use] + pub fn lookup_for_program_rom() -> TableWithTypedOutput> { + let inst = COL_MAP.inst; + StoreWordTable::new( + ProgramRom { + pc: inst.pc, + // Combine columns into a single column. + // - ops: This is an internal opcode, not the opcode from RISC-V, and can fit within + // 5 bits. + // - is_op1_signed and is_op2_signed: These fields occupy 1 bit each. + // - rs1_select, rs2_select, and rd_select: These fields require 5 bits each. + // - imm_value: This field requires 32 bits. + // Therefore, the total bit requirement is 5 * 6 + 32 = 62 bits, which is less than + // the size of the Goldilocks field. + // Note: The imm_value field, having more than 5 bits, must be positioned as the + // last column in the list to ensure the correct functioning of + // 'reduce_with_powers'. + inst_data: ColumnWithTypedInput::reduce_with_powers( + [ + // TODO: don't hard-code opcode like this. + ColumnWithTypedInput::constant(18), + // TODO: use a struct here to name the components, and make IntoIterator, + // like we do with our stark tables. + ColumnWithTypedInput::constant(0), + ColumnWithTypedInput::constant(0), + inst.rs1_selected, + inst.rs2_selected, + ColumnWithTypedInput::constant(0), + inst.imm_value, + ], + 1 << 5, + ), + }, + COL_MAP.is_running, + ) + } + + /// Lookup between Store Word memory table + /// and Memory stark table. + #[must_use] + pub fn lookup_for_memory_limb() -> Vec>> { + (0..4) + .map(|limb_index| { + StoreWordTable::new( + MemoryCtl { + clk: COL_MAP.clk, + is_store: ColumnWithTypedInput::constant(1), + is_load: ColumnWithTypedInput::constant(0), + value: COL_MAP.op1_limbs[limb_index], + addr: COL_MAP.address + i64::try_from(limb_index).unwrap(), + }, + COL_MAP.is_running, + ) + }) + .collect() + } +} + +use columns::{Instruction, StoreWord}; +use mozak_runner::instruction::Op; +use mozak_runner::vm::Row; +use plonky2::hash::hash_types::RichField; + +use crate::utils::pad_trace_with_default; + +#[must_use] +pub fn generate(executed: &[Row]) -> Vec> { + let mut trace: Vec> = vec![]; + for Row { + state, + instruction: inst, + aux, + } in executed + { + if let Op::SW = inst.op { + let rs1_selected = inst.args.rs1; + let rs2_selected = inst.args.rs2; + let op1_value = state.get_register_value(rs1_selected); + let op2_value = state.get_register_value(rs2_selected); + let imm_value = inst.args.imm; + let address = aux.mem.unwrap().addr; + assert_eq!(address, op2_value.wrapping_add(imm_value)); + let op1_limbs = op1_value.to_le_bytes().map(u32::from); + let row = StoreWord { + inst: Instruction { + pc: state.get_pc(), + rs1_selected: u32::from(rs1_selected), + rs2_selected: u32::from(rs2_selected), + imm_value, + }, + clk: u32::try_from(state.clk).unwrap(), + op1_limbs, + op2_value, + address, + is_running: 1, + } + .map(F::from_canonical_u32); + trace.push(row); + } + } + pad_trace_with_default(trace) +} diff --git a/circuits/src/ops/sw/stark.rs b/circuits/src/ops/sw/stark.rs new file mode 100644 index 000000000..a9d17cfc4 --- /dev/null +++ b/circuits/src/ops/sw/stark.rs @@ -0,0 +1,80 @@ +use std::marker::PhantomData; + +use expr::{Expr, ExprBuilder, StarkFrameTyped}; +use mozak_circuits_derive::StarkNameDisplay; +use plonky2::field::extension::{Extendable, FieldExtension}; +use plonky2::field::packed::PackedField; +use plonky2::hash::hash_types::RichField; +use plonky2::iop::ext_target::ExtensionTarget; +use plonky2::plonk::circuit_builder::CircuitBuilder; +use starky::constraint_consumer::{ConstraintConsumer, RecursiveConstraintConsumer}; +use starky::evaluation_frame::StarkFrame; +use starky::stark::Stark; + +use super::columns::StoreWord; +use crate::columns_view::{HasNamedColumns, NumberOfColumns}; +use crate::expr::{build_ext, build_packed, ConstraintBuilder}; +use crate::unstark::NoColumns; + +#[derive(Copy, Clone, Default, StarkNameDisplay)] +#[allow(clippy::module_name_repetitions)] +pub struct StoreWordStark { + pub _f: PhantomData, +} + +impl HasNamedColumns for StoreWordStark { + type Columns = StoreWord; +} + +const COLUMNS: usize = StoreWord::<()>::NUMBER_OF_COLUMNS; +const PUBLIC_INPUTS: usize = 0; + +fn generate_constraints<'a, T: Copy>( + vars: &StarkFrameTyped>, NoColumns>>, +) -> ConstraintBuilder> { + let lv = vars.local_values; + let mut constraints = ConstraintBuilder::default(); + let address_overflowing = lv.op2_value + lv.inst.imm_value; + let wrapped = address_overflowing - (1 << 32); + + // Check: the resulting sum is wrapped if necessary. + // As the result is range checked, this make the choice deterministic, + // even for a malicious prover. + constraints.always((lv.address - address_overflowing) * (lv.address - wrapped)); + constraints +} + +impl, const D: usize> Stark for StoreWordStark { + type EvaluationFrame = StarkFrame + + where + FE: FieldExtension, + P: PackedField; + type EvaluationFrameTarget = + StarkFrame, ExtensionTarget, COLUMNS, PUBLIC_INPUTS>; + + fn eval_packed_generic( + &self, + vars: &Self::EvaluationFrame, + constraint_consumer: &mut ConstraintConsumer

, + ) where + FE: FieldExtension, + P: PackedField, { + let expr_builder = ExprBuilder::default(); + let constraints = generate_constraints(&expr_builder.to_typed_starkframe(vars)); + build_packed(constraints, constraint_consumer); + } + + fn eval_ext_circuit( + &self, + circuit_builder: &mut CircuitBuilder, + vars: &Self::EvaluationFrameTarget, + constraint_consumer: &mut RecursiveConstraintConsumer, + ) { + let expr_builder = ExprBuilder::default(); + let constraints = generate_constraints(&expr_builder.to_typed_starkframe(vars)); + build_ext(constraints, circuit_builder, constraint_consumer); + } + + fn constraint_degree(&self) -> usize { 3 } +} diff --git a/circuits/src/poseidon2_sponge/columns.rs b/circuits/src/poseidon2_sponge/columns.rs index b7250cf6e..ad5f3bf1b 100644 --- a/circuits/src/poseidon2_sponge/columns.rs +++ b/circuits/src/poseidon2_sponge/columns.rs @@ -17,7 +17,7 @@ use crate::register::RegisterCtl; use crate::stark::mozak_stark::{Poseidon2SpongeTable, TableWithTypedOutput}; #[repr(C)] -#[derive(Clone, Copy, Eq, PartialEq, Debug, Default)] +#[derive(Clone, Copy, Eq, PartialEq, Debug)] pub struct Ops { pub is_init_permute: T, pub is_permute: T, diff --git a/circuits/src/rangecheck/generation.rs b/circuits/src/rangecheck/generation.rs index d13a88f42..d8b6ddb68 100644 --- a/circuits/src/rangecheck/generation.rs +++ b/circuits/src/rangecheck/generation.rs @@ -7,6 +7,8 @@ use crate::cpu::columns::CpuState; use crate::memory::columns::Memory; use crate::ops::add::columns::Add; use crate::ops::blt_taken::columns::BltTaken; +use crate::ops::lw::columns::LoadWord; +use crate::ops::sw::columns::StoreWord; use crate::rangecheck::columns::RangeCheckColumnsView; use crate::register::general::columns::Register; use crate::stark::mozak_stark::{Lookups, RangecheckTable, Table, TableKind}; @@ -53,6 +55,8 @@ pub(crate) fn generate_rangecheck_trace( cpu_trace: &[CpuState], add_trace: &[Add], blt_taken_trace: &[BltTaken], + store_word_trace: &[StoreWord], + load_word_trace: &[LoadWord], memory_trace: &[Memory], register_trace: &[Register], ) -> Vec> { @@ -67,6 +71,8 @@ pub(crate) fn generate_rangecheck_trace( TableKind::Register => extract_with_mul(register_trace, &looking_table), TableKind::Add => extract_with_mul(add_trace, &looking_table), TableKind::BltTaken => extract_with_mul(blt_taken_trace, &looking_table), + TableKind::StoreWord => extract_with_mul(store_word_trace, &looking_table), + TableKind::LoadWord => extract_with_mul(load_word_trace, &looking_table), // We are trying to build the RangeCheck table, so we have to ignore it here. TableKind::RangeCheck => vec![], other => unimplemented!("Can't range check {other:#?} tables"), @@ -99,7 +105,6 @@ mod tests { use crate::cpu::generation::generate_cpu_trace; use crate::generation::MIN_TRACE_LENGTH; use crate::memory::generation::generate_memory_trace; - use crate::memory_fullword::generation::generate_fullword_memory_trace; use crate::memory_halfword::generation::generate_halfword_memory_trace; use crate::memory_zeroinit::generation::generate_memory_zero_init_trace; use crate::memoryinit::generation::generate_memory_init_trace; @@ -132,13 +137,14 @@ mod tests { let cpu_rows = generate_cpu_trace::(&record); let add_rows = ops::add::generate(&record); + let store_word_rows = ops::sw::generate(&record.executed); + let load_word_rows = ops::lw::generate(&record.executed); let blt_rows = blt_taken::generate(&record); let memory_init = generate_memory_init_trace(&program); let memory_zeroinit_rows = generate_memory_zero_init_trace(&record.executed, &program); let halfword_memory = generate_halfword_memory_trace(&record.executed); - let fullword_memory = generate_fullword_memory_trace(&record.executed); let private_tape_rows = generate_private_tape_trace(&record.executed); let public_tape_rows = generate_public_tape_trace(&record.executed); let call_tape_rows = generate_call_tape_trace(&record.executed); @@ -154,7 +160,8 @@ mod tests { &memory_init, &memory_zeroinit_rows, &halfword_memory, - &fullword_memory, + &store_word_rows, + &load_word_rows, &private_tape_rows, &public_tape_rows, &call_tape_rows, @@ -169,6 +176,8 @@ mod tests { let (_, _, register_rows) = generate_register_trace( &cpu_rows, &add_rows, + &store_word_rows, + &load_word_rows, &blt_rows, &poseidon2_sponge_trace, &private_tape_rows, @@ -184,6 +193,8 @@ mod tests { &cpu_rows, &add_rows, &blt_rows, + &store_word_rows, + &load_word_rows, &memory_rows, ®ister_rows, ); diff --git a/circuits/src/rangecheck_u8/generation.rs b/circuits/src/rangecheck_u8/generation.rs index b04cc383a..f4e5ed737 100644 --- a/circuits/src/rangecheck_u8/generation.rs +++ b/circuits/src/rangecheck_u8/generation.rs @@ -46,7 +46,6 @@ mod tests { use super::*; use crate::cpu::generation::generate_cpu_trace; use crate::memory::generation::generate_memory_trace; - use crate::memory_fullword::generation::generate_fullword_memory_trace; use crate::memory_halfword::generation::generate_halfword_memory_trace; use crate::memory_zeroinit::generation::generate_memory_zero_init_trace; use crate::memoryinit::generation::generate_memory_init_trace; @@ -80,13 +79,14 @@ mod tests { let cpu_rows = generate_cpu_trace::(&record); let add_rows = ops::add::generate(&record); + let store_word_rows = ops::sw::generate(&record.executed); + let load_word_rows = ops::lw::generate(&record.executed); let blt_rows = ops::blt_taken::generate(&record); let memory_init = generate_memory_init_trace(&program); let memory_zeroinit_rows = generate_memory_zero_init_trace(&record.executed, &program); let halfword_memory = generate_halfword_memory_trace(&record.executed); - let fullword_memory = generate_fullword_memory_trace(&record.executed); let private_tape = generate_private_tape_trace(&record.executed); let public_tape = generate_public_tape_trace(&record.executed); let call_tape_rows = generate_call_tape_trace(&record.executed); @@ -102,7 +102,8 @@ mod tests { &memory_init, &memory_zeroinit_rows, &halfword_memory, - &fullword_memory, + &store_word_rows, + &load_word_rows, &private_tape, &public_tape, &call_tape_rows, @@ -117,6 +118,8 @@ mod tests { let (_, _, register_rows) = generate_register_trace( &cpu_rows, &add_rows, + &store_word_rows, + &load_word_rows, &blt_rows, &poseidon2_sponge_trace, &private_tape, @@ -132,6 +135,8 @@ mod tests { &cpu_rows, &add_rows, &blt_rows, + &store_word_rows, + &load_word_rows, &memory_rows, ®ister_rows, ); diff --git a/circuits/src/register/generation.rs b/circuits/src/register/generation.rs index 696f29cc0..2079c050d 100644 --- a/circuits/src/register/generation.rs +++ b/circuits/src/register/generation.rs @@ -83,10 +83,13 @@ where /// 3) pad with dummy rows (`is_used` == 0) to ensure that trace is a power of /// 2. #[allow(clippy::type_complexity)] +// TODO(Matthias): rework the args, perhaps pass table kind with Option or so? #[allow(clippy::too_many_arguments)] pub fn generate_register_trace( cpu_trace: &[CpuState], add_trace: &[ops::add::columns::Add], + store_word_trace: &[ops::sw::columns::StoreWord], + load_word_trace: &[ops::lw::columns::LoadWord], blt_trace: &[ops::blt_taken::columns::BltTaken], poseidon2_sponge: &[Poseidon2Sponge], mem_private: &[StorageDevice], @@ -110,6 +113,8 @@ pub fn generate_register_trace( TableKind::Cpu => extract(cpu_trace, &looking_table), TableKind::Add => extract(add_trace, &looking_table), TableKind::BltTaken => extract(blt_trace, &looking_table), + TableKind::StoreWord => extract(store_word_trace, &looking_table), + TableKind::LoadWord => extract(load_word_trace, &looking_table), TableKind::StorageDevicePrivate => extract(mem_private, &looking_table), TableKind::StorageDevicePublic => extract(mem_public, &looking_table), TableKind::CallTape => extract(mem_call_tape, &looking_table), @@ -223,6 +228,8 @@ mod tests { let cpu_rows = generate_cpu_trace::(&record); let add_rows = ops::add::generate(&record); + let store_word_rows = ops::sw::generate(&record.executed); + let load_word_rows = ops::lw::generate(&record.executed); let blt_rows = ops::blt_taken::generate(&record); let private_tape = generate_private_tape_trace(&record.executed); let public_tape = generate_public_tape_trace(&record.executed); @@ -239,6 +246,8 @@ mod tests { let (_, _, trace) = generate_register_trace( &cpu_rows, &add_rows, + &store_word_rows, + &load_word_rows, &blt_rows, &poseidon2_sponge_trace, &private_tape, diff --git a/circuits/src/stark/mozak_stark.rs b/circuits/src/stark/mozak_stark.rs index 847534a94..bfca0c0d5 100644 --- a/circuits/src/stark/mozak_stark.rs +++ b/circuits/src/stark/mozak_stark.rs @@ -25,8 +25,6 @@ use crate::cross_table_lookup::{ }; use crate::memory::columns::{Memory, MemoryCtl}; use crate::memory::stark::MemoryStark; -use crate::memory_fullword::columns::FullWordMemory; -use crate::memory_fullword::stark::FullWordMemoryStark; use crate::memory_halfword::columns::HalfWordMemory; use crate::memory_halfword::stark::HalfWordMemoryStark; use crate::memory_zeroinit::columns::MemoryZeroInit; @@ -37,7 +35,10 @@ use crate::ops::add::columns::Add; use crate::ops::add::stark::AddStark; use crate::ops::blt_taken::columns::BltTaken; use crate::ops::blt_taken::stark::BltTakenStark; -use crate::ops::{add, blt_taken}; +use crate::ops::lw::columns::LoadWord; +use crate::ops::lw::stark::LoadWordStark; +use crate::ops::sw::columns::StoreWord; +use crate::ops::sw::stark::StoreWordStark; use crate::poseidon2::columns::{Poseidon2State, Poseidon2StateCtl}; use crate::poseidon2::stark::Poseidon2_12Stark; use crate::poseidon2_output_bytes::columns::{Poseidon2OutputBytes, Poseidon2OutputBytesCtl}; @@ -69,12 +70,12 @@ use crate::tape_commitments::stark::TapeCommitmentsStark; use crate::xor::columns::{XorColumnsView, XorView}; use crate::xor::stark::XorStark; use crate::{ - bitshift, cpu, cpu_skeleton, memory, memory_fullword, memory_halfword, memory_zeroinit, - memoryinit, ops, poseidon2_output_bytes, poseidon2_sponge, program, program_multiplicities, - rangecheck, register, storage_device, xor, + bitshift, cpu, cpu_skeleton, memory, memory_halfword, memory_zeroinit, memoryinit, ops, + poseidon2_output_bytes, poseidon2_sponge, program, program_multiplicities, rangecheck, + register, storage_device, xor, }; -const NUM_CROSS_TABLE_LOOKUP: usize = 18; +const NUM_CROSS_TABLE_LOOKUP: usize = 17; const NUM_PUBLIC_SUB_TABLES: usize = 2; const NUM_PUBLIC_TABLES: usize = 2; pub const PUBLIC_TABLE_KINDS: [TableKind; NUM_PUBLIC_TABLES] = @@ -113,8 +114,6 @@ pub struct MozakStark, const D: usize> { pub rangecheck_u8_stark: RangeCheckU8Stark, #[StarkSet(stark_kind = "HalfWordMemory")] pub halfword_memory_stark: HalfWordMemoryStark, - #[StarkSet(stark_kind = "FullWordMemory")] - pub fullword_memory_stark: FullWordMemoryStark, #[StarkSet(stark_kind = "StorageDevicePrivate")] pub private_tape_stark: StorageDeviceStark, #[StarkSet(stark_kind = "StorageDevicePublic")] @@ -153,6 +152,10 @@ pub struct MozakStark, const D: usize> { pub add_stark: AddStark, #[StarkSet(stark_kind = "BltTaken")] pub blt_taken_stark: BltTakenStark, + #[StarkSet(stark_kind = "StoreWord")] + pub store_word_stark: StoreWordStark, + #[StarkSet(stark_kind = "LoadWord")] + pub load_word_stark: LoadWordStark, #[StarkSet(stark_kind = "TapeCommitments")] pub tape_commitments_stark: TapeCommitmentsStark, pub cross_table_lookups: [CrossTableLookup; NUM_CROSS_TABLE_LOOKUP], @@ -335,7 +338,6 @@ macro_rules! mozak_stark_helpers { } #[allow(unused_imports)] pub(crate) use all_starks_par; - }; } @@ -429,7 +431,6 @@ impl, const D: usize> Default for MozakStark memory_zeroinit_stark: MemoryZeroInitStark::default(), rangecheck_u8_stark: RangeCheckU8Stark::default(), halfword_memory_stark: HalfWordMemoryStark::default(), - fullword_memory_stark: FullWordMemoryStark::default(), register_init_stark: RegisterInitStark::default(), register_stark: RegisterStark::default(), register_zero_read_stark: RegisterZeroReadStark::default(), @@ -447,6 +448,8 @@ impl, const D: usize> Default for MozakStark cpu_skeleton_stark: CpuSkeletonStark::default(), add_stark: AddStark::default(), blt_taken_stark: BltTakenStark::default(), + store_word_stark: StoreWordStark::default(), + load_word_stark: LoadWordStark::default(), tape_commitments_stark: TapeCommitmentsStark::default(), // These tables contain only descriptions of the tables. @@ -461,7 +464,6 @@ impl, const D: usize> Default for MozakStark MemoryInitMemoryTable::lookups(), RangeCheckU8LookupTable::lookups(), HalfWordMemoryCpuTable::lookups(), - FullWordMemoryCpuTable::lookups(), RegisterLookups::lookups(), StorageDeviceToCpuTable::lookups(), Poseidon2SpongeCpuTable::lookups(), @@ -608,11 +610,6 @@ table_impl!( TableKind::HalfWordMemory, HalfWordMemory ); -table_impl!( - FullWordMemoryTable, - TableKind::FullWordMemory, - FullWordMemory -); table_impl!(RegisterInitTable, TableKind::RegisterInit, RegisterInit); table_impl!(RegisterTable, TableKind::Register, Register); table_impl!( @@ -671,6 +668,8 @@ table_impl!( table_impl!(SkeletonTable, TableKind::CpuSkeleton, CpuSkeleton); table_impl!(AddTable, TableKind::Add, Add); table_impl!(BltTakenTable, TableKind::BltTaken, BltTaken); +table_impl!(StoreWordTable, TableKind::StoreWord, StoreWord); +table_impl!(LoadWordTable, TableKind::LoadWord, LoadWord); pub trait Lookups { type Row: IntoIterator; @@ -690,6 +689,8 @@ impl Lookups for CpuToSkeletonTable { cpu::columns::lookup_for_skeleton(), ops::add::columns::lookup_for_skeleton(), ops::blt_taken::columns::lookup_for_skeleton(), + ops::sw::columns::lookup_for_skeleton(), + ops::lw::columns::lookup_for_skeleton(), ], vec![cpu_skeleton::columns::lookup_for_cpu()], ) @@ -708,6 +709,9 @@ impl Lookups for RangecheckTable { memory::columns::rangecheck_looking(), cpu::columns::rangecheck_looking(), ops::add::columns::rangecheck_looking(), + ops::sw::columns::rangecheck_looking(), + // TODO(Matthias): + ops::lw::columns::rangecheck_looking(), register, ] .collect(); @@ -746,7 +750,8 @@ impl Lookups for IntoMemoryTable { TableKind::SelfProgIdTape, ] .map(storage_device::columns::lookup_for_memory), - memory_fullword::columns::lookup_for_memory_limb(), + ops::sw::columns::lookup_for_memory_limb(), + ops::lw::columns::lookup_for_memory_limb(), memory_halfword::columns::lookup_for_memory_limb(), poseidon2_sponge::columns::lookup_for_input_memory(), poseidon2_output_bytes::columns::lookup_for_output_memory(), @@ -792,8 +797,10 @@ impl Lookups for InnerCpuTable { fn lookups_with_typed_output() -> CrossTableLookupWithTypedOutput { CrossTableLookupWithTypedOutput::new( vec![ - add::columns::lookup_for_program_rom(), - blt_taken::columns::lookup_for_program_rom(), + ops::add::columns::lookup_for_program_rom(), + ops::blt_taken::columns::lookup_for_program_rom(), + ops::sw::columns::lookup_for_program_rom(), + ops::lw::columns::lookup_for_program_rom(), cpu::columns::lookup_for_program_rom(), ], vec![program_multiplicities::columns::lookup_for_cpu()], @@ -841,19 +848,6 @@ impl Lookups for HalfWordMemoryCpuTable { } } -pub struct FullWordMemoryCpuTable; - -impl Lookups for FullWordMemoryCpuTable { - type Row = MemoryCtl; - - fn lookups_with_typed_output() -> CrossTableLookupWithTypedOutput { - CrossTableLookupWithTypedOutput::new( - vec![cpu::columns::lookup_for_fullword_memory()], - vec![memory_fullword::columns::lookup_for_cpu()], - ) - } -} - pub struct RegisterLookups; impl Lookups for RegisterLookups { @@ -865,6 +859,8 @@ impl Lookups for RegisterLookups { crate::cpu::columns::register_looking(), ops::add::columns::register_looking(), ops::blt_taken::columns::register_looking(), + ops::sw::columns::register_looking(), + ops::lw::columns::register_looking(), crate::storage_device::columns::register_looking(), crate::poseidon2_sponge::columns::register_looking(), vec![crate::register::init::columns::lookup_for_register()], diff --git a/circuits/src/storage_device/columns.rs b/circuits/src/storage_device/columns.rs index 281531b11..da72aed24 100644 --- a/circuits/src/storage_device/columns.rs +++ b/circuits/src/storage_device/columns.rs @@ -15,7 +15,7 @@ use crate::tape_commitments::columns::TapeCommitmentCTL; /// Operations (one-hot encoded) #[repr(C)] -#[derive(Clone, Copy, Eq, PartialEq, Debug, Default)] +#[derive(Clone, Copy, Eq, PartialEq, Debug)] pub struct Ops { /// Binary filter column to represent a RISC-V SB operation. pub is_memory_store: T, diff --git a/circuits/src/test_utils.rs b/circuits/src/test_utils.rs index 55325065e..a3886c799 100644 --- a/circuits/src/test_utils.rs +++ b/circuits/src/test_utils.rs @@ -27,8 +27,6 @@ use crate::cpu::generation::generate_cpu_trace; use crate::cpu::stark::CpuStark; use crate::memory::generation::generate_memory_trace; use crate::memory::stark::MemoryStark; -use crate::memory_fullword::generation::generate_fullword_memory_trace; -use crate::memory_fullword::stark::FullWordMemoryStark; use crate::memory_halfword::generation::generate_halfword_memory_trace; use crate::memory_halfword::stark::HalfWordMemoryStark; use crate::memory_zeroinit::generation::generate_memory_zero_init_trace; @@ -150,13 +148,14 @@ impl ProveAndVerify for RangeCheckStark { let stark = S::default(); let cpu_trace = generate_cpu_trace(record); let add_trace = ops::add::generate(record); + let store_word_rows = ops::sw::generate(&record.executed); + let load_word_rows = ops::lw::generate(&record.executed); let blt_trace = ops::blt_taken::generate(record); let memory_init = generate_memory_init_trace(program); let memory_zeroinit_rows = generate_memory_zero_init_trace(&record.executed, program); let halfword_memory = generate_halfword_memory_trace(&record.executed); - let fullword_memory = generate_fullword_memory_trace(&record.executed); let private_tape = generate_private_tape_trace(&record.executed); let public_tape = generate_public_tape_trace(&record.executed); let call_tape_rows = generate_call_tape_trace(&record.executed); @@ -172,7 +171,8 @@ impl ProveAndVerify for RangeCheckStark { &memory_init, &memory_zeroinit_rows, &halfword_memory, - &fullword_memory, + &store_word_rows, + &load_word_rows, &private_tape, &public_tape, &call_tape_rows, @@ -187,6 +187,8 @@ impl ProveAndVerify for RangeCheckStark { let (_, _, register_trace) = generate_register_trace( &cpu_trace, &add_trace, + &store_word_rows, + &load_word_rows, &blt_trace, &poseidon2_sponge_trace, &private_tape, @@ -202,6 +204,8 @@ impl ProveAndVerify for RangeCheckStark { &cpu_trace, &add_trace, &blt_trace, + &store_word_rows, + &load_word_rows, &memory_trace, ®ister_trace, )); @@ -249,7 +253,8 @@ impl ProveAndVerify for MemoryStark { let memory_zeroinit_rows = generate_memory_zero_init_trace(&record.executed, program); let halfword_memory = generate_halfword_memory_trace(&record.executed); - let fullword_memory = generate_fullword_memory_trace(&record.executed); + let store_word_rows = ops::sw::generate(&record.executed); + let load_word_rows = ops::lw::generate(&record.executed); let private_tape = generate_private_tape_trace(&record.executed); let public_tape = generate_public_tape_trace(&record.executed); let call_tape_rows = generate_call_tape_trace(&record.executed); @@ -265,7 +270,8 @@ impl ProveAndVerify for MemoryStark { &memory_init, &memory_zeroinit_rows, &halfword_memory, - &fullword_memory, + &store_word_rows, + &load_word_rows, &private_tape, &public_tape, &call_tape_rows, @@ -308,26 +314,6 @@ impl ProveAndVerify for HalfWordMemoryStark { } } -impl ProveAndVerify for FullWordMemoryStark { - fn prove_and_verify(_program: &Program, record: &ExecutionRecord) -> Result<()> { - type S = FullWordMemoryStark; - let config = fast_test_config(); - - let stark = S::default(); - let trace_poly_values = - trace_rows_to_poly_values(generate_fullword_memory_trace(&record.executed)); - let proof = prove_table::( - stark, - &config, - trace_poly_values, - &[], - &mut TimingTree::default(), - )?; - - verify_stark_proof(stark, proof, &config) - } -} - impl ProveAndVerify for StorageDeviceStark { fn prove_and_verify(_program: &Program, record: &ExecutionRecord) -> Result<()> { type S = StorageDeviceStark; @@ -397,6 +383,8 @@ impl ProveAndVerify for RegisterStark { let stark = S::default(); let cpu_trace = generate_cpu_trace(record); let add_trace = ops::add::generate(record); + let store_word_rows = ops::sw::generate(&record.executed); + let load_word_rows = ops::lw::generate(&record.executed); let blt_trace = ops::blt_taken::generate(record); let private_tape = generate_private_tape_trace(&record.executed); let public_tape = generate_public_tape_trace(&record.executed); @@ -412,6 +400,8 @@ impl ProveAndVerify for RegisterStark { let (_, _, trace) = generate_register_trace( &cpu_trace, &add_trace, + &store_word_rows, + &load_word_rows, &blt_trace, &poseidon2_sponge_rows, &private_tape, diff --git a/cli/src/cli_benches/benches.rs b/cli/src/cli_benches/benches.rs index 05ca63a50..8406876c6 100644 --- a/cli/src/cli_benches/benches.rs +++ b/cli/src/cli_benches/benches.rs @@ -3,6 +3,7 @@ use std::time::Duration; use anyhow::Result; use clap::{Args as Args_, Subcommand}; +use super::memory::MemoryBench; use super::nop::NopBench; use super::omni::OmniBench; use super::poseidon2::Poseidon2Bench; @@ -39,6 +40,9 @@ pub(crate) trait Bench { #[derive(PartialEq, Debug, Subcommand, Clone)] pub enum BenchFunction { + MemoryBench { + iterations: u32, + }, XorBench { iterations: u32, }, @@ -72,6 +76,7 @@ impl BenchArgs { BenchFunction::Poseidon2Bench { input_len } => Poseidon2Bench.bench(input_len), BenchFunction::SortBench { n } => SortBench.bench(n), BenchFunction::SortBenchRecursive { n } => SortBenchRecursive.bench(n), + BenchFunction::MemoryBench { iterations } => MemoryBench.bench(iterations), BenchFunction::BatchStarksSortBench { n } => BatchStarksSortBench.bench(n), } } diff --git a/cli/src/cli_benches/memory.rs b/cli/src/cli_benches/memory.rs new file mode 100644 index 000000000..dd29386c6 --- /dev/null +++ b/cli/src/cli_benches/memory.rs @@ -0,0 +1,88 @@ +use anyhow::Result; +use mozak_circuits::test_utils::{prove_and_verify_mozak_stark, F}; +use mozak_runner::code; +use mozak_runner::elf::Program; +use mozak_runner::instruction::{Args, Instruction, Op}; +use mozak_runner::vm::ExecutionRecord; +use starky::config::StarkConfig; + +use super::benches::Bench; + +// Stick some byte and word (and half-word?) memory operations in a big old +// loop. Do some randomisation? +// +// Code it up in Rust? Or as assembly? +// +// just use two counters. Outer counter, and inner counter. +// +// r1: counter +// r3: memory value +// + +pub fn memory_execute((program, record): (Program, ExecutionRecord)) -> Result<()> { + prove_and_verify_mozak_stark(&program, &record, &StarkConfig::standard_fast_config()) +} + +pub fn memory_prepare(iterations: u32) -> (Program, ExecutionRecord) { + let instructions = [ + Instruction { + op: Op::SW, + args: Args { + rs1: 1, + rs2: 1, + imm: 0xDEAD_BEEF, + ..Args::default() + }, + }, + Instruction { + op: Op::LW, + args: Args { + rd: 1, + rs2: 1, + imm: 0xDEAD_BEEF, + ..Args::default() + }, + }, + Instruction { + op: Op::ADD, + args: Args { + rd: 1, + rs1: 1, + imm: 1_u32.wrapping_neg(), + ..Args::default() + }, + }, + Instruction { + op: Op::BLTU, + args: Args { + rs1: 0, + rs2: 1, + imm: 0, + ..Args::default() + }, + }, + ]; + code::execute(instructions, &[], &[(1, iterations)]) +} + +pub(crate) struct MemoryBench; + +impl Bench for MemoryBench { + type Args = u32; + type Prepared = (Program, ExecutionRecord); + + fn prepare(&self, args: &Self::Args) -> Self::Prepared { memory_prepare(*args) } + + fn execute(&self, prepared: Self::Prepared) -> Result<()> { memory_execute(prepared) } +} + +#[cfg(test)] +mod tests { + use super::{memory_execute, memory_prepare}; + + #[test] + fn test_memory_bench() -> anyhow::Result<()> { + let iterations = 10; + memory_execute(memory_prepare(iterations)) + } +} diff --git a/cli/src/cli_benches/mod.rs b/cli/src/cli_benches/mod.rs index 354332982..06208c99e 100644 --- a/cli/src/cli_benches/mod.rs +++ b/cli/src/cli_benches/mod.rs @@ -1,4 +1,5 @@ pub mod benches; +pub mod memory; pub mod nop; pub mod omni; pub mod poseidon2; diff --git a/cli/src/cli_benches/omni.rs b/cli/src/cli_benches/omni.rs index 3573abd43..131cd052c 100644 --- a/cli/src/cli_benches/omni.rs +++ b/cli/src/cli_benches/omni.rs @@ -130,7 +130,6 @@ pub fn omni_prepare(iterations: u32) -> (Program, ExecutionRecord) { op: Op::LW, args: Args { rd: 4, - rs1: 1, rs2: 2, ..Args::default() }, @@ -165,7 +164,6 @@ pub fn omni_prepare(iterations: u32) -> (Program, ExecutionRecord) { Instruction { op: Op::SW, args: Args { - rd: 4, rs1: 1, rs2: 2, ..Args::default() diff --git a/runner/src/state.rs b/runner/src/state.rs index 06d1d93df..4cadb7b52 100644 --- a/runner/src/state.rs +++ b/runner/src/state.rs @@ -214,6 +214,7 @@ pub struct Aux { pub op2_raw: u32, pub poseidon2: Option>, pub storage_device_entry: Option, + pub branch_taken: Option, } #[derive(Default, Clone)] @@ -325,14 +326,23 @@ impl State { pub fn branch_op(self, data: &Args, op: fn(u32, u32) -> bool) -> (Aux, Self) { let op1 = self.get_register_value(data.rs1); let op2 = self.get_register_value(data.rs2); - ( - Aux::default(), - if op(op1, op2) { - self.set_pc(data.imm) - } else { - self.bump_pc() - }, - ) + if op(op1, op2) { + ( + Aux { + branch_taken: Some(true), + ..Default::default() + }, + self.set_pc(data.imm), + ) + } else { + ( + Aux { + branch_taken: Some(false), + ..Default::default() + }, + self.bump_pc(), + ) + } } }