diff --git a/prover/src/auto_storage.rs b/prover/src/auto_storage.rs index a28bcd498..49707cb4c 100644 --- a/prover/src/auto_storage.rs +++ b/prover/src/auto_storage.rs @@ -34,9 +34,9 @@ use stark::prover::table_parallelism; use stark::storage_mode::StorageMode; use sysinfo::System; -const GOLDILOCKS_BYTES: u64 = 8; -const CUBIC_EXT_BYTES: u64 = 24; -const KECCAK_NODE_BYTES: u64 = 32; +pub(crate) const GOLDILOCKS_BYTES: u64 = 8; +pub(crate) const CUBIC_EXT_BYTES: u64 = 24; +pub(crate) const KECCAK_NODE_BYTES: u64 = 32; const LOG_STRUCT_BYTES: u64 = 40; const MEMORY_CELL_BYTES: u64 = 32; const INSTRUCTION_MAP_BYTES_PER_ROW: u64 = 32; @@ -283,7 +283,7 @@ pub fn peak_bytes(lengths: &TableLengths, blowup_factor: u8, table_parallelism: /// `Disk` if `estimated` exceeds `available` minus a safety margin, else /// `Ram`. Defaults to `Disk` when `available` is `None`. -fn select_storage_mode(estimated: u64, available: Option) -> StorageMode { +pub(crate) fn select_storage_mode(estimated: u64, available: Option) -> StorageMode { let Some(available) = available else { log::warn!("Auto disk-spill: sysinfo could not read system memory, defaulting to Disk."); return StorageMode::Disk; @@ -307,96 +307,3 @@ fn available_ram_bytes() -> Option { Some(sys.available_memory()) } } - -#[cfg(test)] -mod tests { - use super::*; - - const GB: u64 = 1_000_000_000; - /// Larger than the table count, so every table lands in the top-k and the - /// per-table delta in `peak_bytes_per_table_increment_is_exact` is purely - /// additive. - const ALL_TABLES: usize = 1_000; - - fn empty_lengths() -> TableLengths { - TableLengths::default() - } - - /// Adding rows to a single chunked table must increase `peak_bytes` by - /// exactly the per-row contribution from the formula in the module doc. - /// Verifies the per-table breakdown is exact rather than averaged. - #[test] - fn peak_bytes_per_table_increment_is_exact() { - let blowup = 2u8; - let b = blowup as u64; - - let baseline = peak_bytes(&empty_lengths(), blowup, ALL_TABLES); - - let mut lengths = empty_lengths(); - lengths.cpu_padded_rows = 4; - let bumped = peak_bytes(&lengths, blowup, ALL_TABLES); - - let cpu_main = CPU_COLS as u64; - let cpu_aux = cpu_buses().len().div_ceil(2) as u64; - let per_row_persistent = cpu_main * GOLDILOCKS_BYTES * (1 + b) - + cpu_aux * CUBIC_EXT_BYTES * (1 + b) - + 2 * b * KECCAK_NODE_BYTES // main Merkle (1 tree) - + 2 * b * KECCAK_NODE_BYTES; // aux Merkle - let per_row_transient = b * CUBIC_EXT_BYTES // constraint_evaluations - + 2 * b * CUBIC_EXT_BYTES // composition LDE (2 parts, d=2) - + b * KECCAK_NODE_BYTES // composition Merkle (PairKeccak) - + b * CUBIC_EXT_BYTES // FRI evals (geometric ≈ 1) - + b * KECCAK_NODE_BYTES; // FRI Merkle (geometric ≈ 1) - let per_row_domain = (3 + 2 * b) * GOLDILOCKS_BYTES; - - // CPU adds 4 rows of persistent + transient (top-k by ALL_TABLES) + - // its 4-row Domain entry (a fresh unique key not previously present). - assert_eq!( - bumped - baseline, - 4 * (per_row_persistent + per_row_transient + per_row_domain) - ); - } - - /// Higher blowup_factor should produce a strictly larger estimate. - #[test] - fn peak_bytes_scales_with_blowup() { - let lengths = empty_lengths(); - let two = peak_bytes(&lengths, 2, ALL_TABLES); - let four = peak_bytes(&lengths, 4, ALL_TABLES); - let eight = peak_bytes(&lengths, 8, ALL_TABLES); - assert!(two < four); - assert!(four < eight); - } - - /// Lower table_parallelism caps the transient sum to fewer tables, so the - /// estimate must be monotone in `k`. - #[test] - fn peak_bytes_monotone_in_table_parallelism() { - let lengths = empty_lengths(); - let k1 = peak_bytes(&lengths, 2, 1); - let k4 = peak_bytes(&lengths, 2, 4); - let k_all = peak_bytes(&lengths, 2, ALL_TABLES); - assert!(k1 < k4); - assert!(k4 <= k_all); - } - - #[test] - fn select_ram_when_estimate_below_threshold() { - // 10 GB estimated, 32 GB available → threshold 28.8 GB → Ram. - let mode = select_storage_mode(10 * GB, Some(32 * GB)); - assert_eq!(mode, StorageMode::Ram); - } - - #[test] - fn select_disk_when_estimate_exceeds_threshold() { - // 30 GB estimated, 32 GB available → threshold 28.8 GB → Disk. - let mode = select_storage_mode(30 * GB, Some(32 * GB)); - assert_eq!(mode, StorageMode::Disk); - } - - #[test] - fn unknown_available_defaults_to_disk() { - let mode = select_storage_mode(peak_bytes(&empty_lengths(), 2, ALL_TABLES), None); - assert_eq!(mode, StorageMode::Disk); - } -} diff --git a/prover/src/constraints/templates.rs b/prover/src/constraints/templates.rs index 09237145f..fc3df4825 100644 --- a/prover/src/constraints/templates.rs +++ b/prover/src/constraints/templates.rs @@ -509,16 +509,3 @@ pub fn new_is_bit_constraints( (constraints, constraint_idx_start + value_cols.len()) } - -#[cfg(test)] -mod tests { - use super::*; - use crate::tables::types::GoldilocksField; - - #[test] - fn test_inv_shift_32_is_correct() { - let inv = FieldElement::::from(INV_SHIFT_32); - let shift = FieldElement::::from(SHIFT_32); - assert_eq!(inv * shift, FieldElement::one()); - } -} diff --git a/prover/src/tables/decode.rs b/prover/src/tables/decode.rs index 913867b59..de7250e94 100644 --- a/prover/src/tables/decode.rs +++ b/prover/src/tables/decode.rs @@ -422,81 +422,3 @@ fn build_decode_table( TraceTable::new_main(data, cols::NUM_COLUMNS, 1) } - -#[cfg(test)] -mod tests { - use super::*; - use executor::elf::Segment; - - #[test] - fn test_tables_from_elf_single_executable_segment() { - // ADDI x1, x0, 42 (opcode: 0x02a00093) - // ADDI x2, x1, 10 (opcode: 0x00a08113) - let elf = Elf { - entry_point: 0x1000, - data: vec![Segment { - base_addr: 0x1000, - values: vec![0x02a00093, 0x00a08113], - is_executable: true, - }], - }; - - let tables = tables_from_elf(&elf).unwrap(); - - // Check DECODE table - assert_eq!(tables.pc_to_row.len(), 3); // 2 instructions + CPU padding - assert!(tables.pc_to_row.contains_key(&0x1000)); - assert!(tables.pc_to_row.contains_key(&0x1004)); - assert!( - tables - .pc_to_row - .contains_key(&super::super::cpu::CPU_PADDING_PC) - ); - } - - #[test] - fn test_tables_from_elf_mixed_segments() { - // Executable segment with instructions - // Data segment with data (not included in DECODE) - let elf = Elf { - entry_point: 0x1000, - data: vec![ - Segment { - base_addr: 0x1000, - values: vec![0x02a00093], // ADDI instruction - is_executable: true, - }, - Segment { - base_addr: 0x2000, - values: vec![0xDEADBEEF, 0xCAFEBABE], // Data - is_executable: false, - }, - ], - }; - - let tables = tables_from_elf(&elf).unwrap(); - - // DECODE: only executable segment (1 instruction + CPU padding) - assert_eq!(tables.pc_to_row.len(), 2); - assert!(tables.pc_to_row.contains_key(&0x1000)); - assert!(!tables.pc_to_row.contains_key(&0x2000)); // Data not in decode - } - - #[test] - fn test_tables_from_elf_empty() { - let elf = Elf { - entry_point: 0x1000, - data: vec![], - }; - - let tables = tables_from_elf(&elf).unwrap(); - - // DECODE: only CPU padding entry - assert_eq!(tables.pc_to_row.len(), 1); - assert!( - tables - .pc_to_row - .contains_key(&super::super::cpu::CPU_PADDING_PC) - ); - } -} diff --git a/prover/src/tables/keccak_rnd.rs b/prover/src/tables/keccak_rnd.rs index 75e174463..a808670e1 100644 --- a/prover/src/tables/keccak_rnd.rs +++ b/prover/src/tables/keccak_rnd.rs @@ -934,62 +934,3 @@ pub fn create_constraints( } (constraints, idx) } - -#[cfg(test)] -mod tests { - use super::*; - use executor::vm::instruction::execution::keccak_f1600; - - /// pi is a spec virtual variable. Verify the inlined expression - /// (rot_left[sx,sy,l_byte] + rot_right[sx,sy,r_byte]) matches the byte of - /// rho(theta) for a non-trivial state. Uses mu=0 padding rows as a trivial - /// sanity check (all zeros), then a non-zero-input round as the real test. - #[test] - fn test_pi_virtual_matches_rotate() { - // Use a non-zero input so theta_lanes are non-trivial. - let input = [0x0102030405060708u64; 25]; - let mut output = input; - keccak_f1600(&mut output); - let op = KeccakRoundOperation { - timestamp: 42, - input, - output, - }; - let trace = generate_keccak_rnd_trace(&[op]); - let base = 0; - - // Recompute theta for round 0 in u64 to compare against virtual pi. - let mut c = [0u64; 5]; - for x in 0..5 { - c[x] = input[x] ^ input[x + 5] ^ input[x + 10] ^ input[x + 15] ^ input[x + 20]; - } - let mut d = [0u64; 5]; - for x in 0..5 { - d[x] = c[(x + 4) % 5] ^ c[(x + 1) % 5].rotate_left(1); - } - let mut theta_lanes = [0u64; 25]; - for x in 0..5 { - for y in 0..5 { - theta_lanes[x + 5 * y] = input[x + 5 * y] ^ d[x]; - } - } - - for x in 0..5 { - for y in 0..5 { - let sx = (x + 3 * y) % 5; - let sy = x; - let rotated = theta_lanes[sx + 5 * sy].rotate_left(KECCAK_RHO[sx][sy]); - for z in 0..8 { - let (l_col, r_col) = cols::pi_src_cols(x, y, z); - let virtual_pi = - &trace.main_table.data[base + l_col] + &trace.main_table.data[base + r_col]; - let expected = FE::from((rotated >> (z * 8)) & 0xFF); - assert_eq!( - virtual_pi, expected, - "virtual pi mismatch at ({x},{y},{z}): sx={sx}, sy={sy}" - ); - } - } - } - } -} diff --git a/prover/src/tables/load.rs b/prover/src/tables/load.rs index 7be191849..32c945a41 100644 --- a/prover/src/tables/load.rs +++ b/prover/src/tables/load.rs @@ -605,68 +605,3 @@ pub fn constraints() constraints } - -#[cfg(test)] -mod tests { - use super::*; - - #[test] - fn test_load_trace_generation() { - // Load 4 bytes, sign-extend - let ops = vec![ - LoadOperation::new( - 0x1000, - 100, - 4, - true, - [0x12, 0x34, 0x56, 0x78, 0xFF, 0xFF, 0xFF, 0xFF], - ), - LoadOperation::new( - 0x2000, - 200, - 1, - false, - [0x42, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00], - ), - ]; - - let trace = generate_load_trace(&ops); - assert_eq!(trace.num_cols(), cols::NUM_COLUMNS); - assert!(trace.num_rows() >= 2); - } - - #[test] - fn test_read_flags() { - // "Exactly N" semantics per spec - let op1 = LoadOperation::new(0, 0, 1, false, [0; 8]); - assert_eq!(op1.read_flags(), (false, false, false)); // no flags for 1 byte - - let op2 = LoadOperation::new(0, 0, 2, false, [0; 8]); - assert_eq!(op2.read_flags(), (true, false, false)); // read2 only - - let op4 = LoadOperation::new(0, 0, 4, false, [0; 8]); - assert_eq!(op4.read_flags(), (false, true, false)); // read4 only - - let op8 = LoadOperation::new(0, 0, 8, false, [0; 8]); - assert_eq!(op8.read_flags(), (false, false, true)); // read8 only - } - - #[test] - fn test_sign_bit_extraction() { - // Byte with MSB set - let op1 = LoadOperation::new(0, 0, 1, true, [0x80, 0, 0, 0, 0, 0, 0, 0]); - assert!(op1.compute_sign_bit()); - - // Byte without MSB set - let op2 = LoadOperation::new(0, 0, 1, true, [0x7F, 0, 0, 0, 0, 0, 0, 0]); - assert!(!op2.compute_sign_bit()); - - // Halfword with MSB set - let op3 = LoadOperation::new(0, 0, 2, true, [0x00, 0x80, 0, 0, 0, 0, 0, 0]); - assert!(op3.compute_sign_bit()); - - // Word with MSB set - let op4 = LoadOperation::new(0, 0, 4, true, [0, 0, 0, 0x80, 0, 0, 0, 0]); - assert!(op4.compute_sign_bit()); - } -} diff --git a/prover/src/tables/memw.rs b/prover/src/tables/memw.rs index c3bc34b26..7bf75741a 100644 --- a/prover/src/tables/memw.rs +++ b/prover/src/tables/memw.rs @@ -965,81 +965,3 @@ pub fn constraints() constraints } - -#[cfg(test)] -mod tests { - use super::*; - - #[test] - fn test_memw_trace_generation() { - let ops = vec![ - MemwOperation::new(false, 0x1000, [1, 2, 3, 4, 5, 6, 7, 8], 100, 8, false) - .with_old([0; 8], [50; 8]), - MemwOperation::new(true, 5, [42, 0, 0, 0, 0, 0, 0, 0], 200, 1, true) - .with_old([10, 0, 0, 0, 0, 0, 0, 0], [150, 0, 0, 0, 0, 0, 0, 0]), - ]; - - let trace = generate_memw_trace(&ops); - assert_eq!(trace.num_cols(), cols::NUM_COLUMNS); - assert!(trace.num_rows() >= 2); - } - - #[test] - fn test_write_flags() { - let op1 = MemwOperation::new(false, 0, [0; 8], 0, 1, false); - assert_eq!(op1.write_flags(), (false, false, false)); - - let op2 = MemwOperation::new(false, 0, [0; 8], 0, 2, false); - assert_eq!(op2.write_flags(), (true, false, false)); - - let op4 = MemwOperation::new(false, 0, [0; 8], 0, 4, false); - assert_eq!(op4.write_flags(), (false, true, false)); - - let op8 = MemwOperation::new(false, 0, [0; 8], 0, 8, false); - assert_eq!(op8.write_flags(), (false, false, true)); - } - - #[test] - fn test_carry_flags() { - // Address 0xFFFF_FFFF should carry when adding 1 - let op = - MemwOperation::new(false, 0xFFFF_FFFF, [0; 8], 100, 8, false).with_old([0; 8], [50; 8]); - let trace = generate_memw_trace(&[op]); - - // All 7 carry flags should be 1 since 0xFFFF_FFFF + i >= 2^32 for i >= 1 - for i in 0..7 { - let val = trace.get_main(0, cols::CARRY[i]); - assert_eq!(*val, FE::one(), "carry[{i}] should be 1"); - } - - // Address 0x0000_0000 should not carry - let op2 = - MemwOperation::new(false, 0x0000_0000, [0; 8], 100, 8, false).with_old([0; 8], [50; 8]); - let trace2 = generate_memw_trace(&[op2]); - for i in 0..7 { - let val = trace2.get_main(0, cols::CARRY[i]); - assert_eq!(*val, FE::zero(), "carry[{i}] should be 0"); - } - - // Address 0xFFFF_FFFE with width=8 exercises mixed per-byte carry bits: - // carry[0]=0 (0xFFFF_FFFE+1 = 0xFFFF_FFFF < 2^32) - // carry[1..6]=1 (0xFFFF_FFFE+2..8 >= 2^32) - let op3 = - MemwOperation::new(false, 0xFFFF_FFFE, [0; 8], 100, 8, false).with_old([0; 8], [50; 8]); - let trace3 = generate_memw_trace(&[op3]); - let val0 = trace3.get_main(0, cols::CARRY[0]); - assert_eq!( - *val0, - FE::zero(), - "carry[0] should be 0 for base 0xFFFF_FFFE" - ); - for i in 1..7 { - let val = trace3.get_main(0, cols::CARRY[i]); - assert_eq!( - *val, - FE::one(), - "carry[{i}] should be 1 for base 0xFFFF_FFFE" - ); - } - } -} diff --git a/prover/src/tables/memw_aligned.rs b/prover/src/tables/memw_aligned.rs index 43b97ce11..f61c66679 100644 --- a/prover/src/tables/memw_aligned.rs +++ b/prover/src/tables/memw_aligned.rs @@ -731,33 +731,3 @@ pub fn constraints() IsBitConstraint::unconditional(cols::MU_WRITE, 3).boxed(), ] } - -#[cfg(test)] -mod tests { - use super::*; - - #[test] - fn test_memw_aligned_trace_generation() { - let ops = vec![ - MemwOperation::new(true, 4, [42, 0, 0, 0, 0, 0, 0, 0], 100, 2, true) - .with_old([42, 0, 0, 0, 0, 0, 0, 0], [50, 50, 0, 0, 0, 0, 0, 0]), - MemwOperation::new(false, 0x1000, [1, 2, 3, 4, 0, 0, 0, 0], 200, 4, false) - .with_old([0; 8], [100; 8]), - ]; - - let trace = generate_memw_aligned_trace(&ops); - assert_eq!(trace.num_cols(), cols::NUM_COLUMNS); - assert!(trace.num_rows() >= 2); - - // Check address decomposition for op[1]: addr = 0x1000 - // base_address[0] (low half) = 0x1000 - // base_address[1] (mid half) = 0 - // base_address[2] (high word) = 0 - assert_eq!( - *trace.get_main(1, cols::BASE_ADDRESS[0]), - FE::from(0x1000u64) - ); - assert_eq!(*trace.get_main(1, cols::BASE_ADDRESS[1]), FE::from(0u64)); - assert_eq!(*trace.get_main(1, cols::BASE_ADDRESS[2]), FE::from(0u64)); - } -} diff --git a/prover/src/tables/memw_register.rs b/prover/src/tables/memw_register.rs index 08930a41e..599fe7ed5 100644 --- a/prover/src/tables/memw_register.rs +++ b/prover/src/tables/memw_register.rs @@ -412,86 +412,3 @@ pub fn constraints() MemwRegisterMuSumIsBit::new(2).boxed(), ] } - -#[cfg(test)] -mod tests { - use super::*; - - #[test] - fn test_memw_register_trace_generation() { - // Create a simple register op (reg x1 = address 1, so base_address = 2) - let ops = vec![ - MemwOperation::new( - true, // is_register - 2, // base_address = 2 * register_index (reg x1) - [42, 7, 0, 0, 0, 0, 0, 0], - 100, - 2, // width = 2 words (registers are DWordWL) - true, - ) - .with_old([10, 3, 0, 0, 0, 0, 0, 0], [50, 50, 0, 0, 0, 0, 0, 0]), - ]; - - let trace = generate_memw_register_trace(&ops); - assert_eq!(trace.num_cols(), cols::NUM_COLUMNS); - assert!(trace.num_rows() >= 4); // minimum 4 rows - - // ADDRESS = base_address / 2 = 2 / 2 = 1 - assert_eq!(*trace.get_main(0, cols::ADDRESS), FE::from(1u64)); - - // TIMESTAMP split - assert_eq!(*trace.get_main(0, cols::TIMESTAMP_0), FE::from(100u64)); - assert_eq!(*trace.get_main(0, cols::TIMESTAMP_1), FE::from(0u64)); - - // Values - assert_eq!(*trace.get_main(0, cols::VAL_0), FE::from(42u64)); - assert_eq!(*trace.get_main(0, cols::VAL_1), FE::from(7u64)); - - // Old values - assert_eq!(*trace.get_main(0, cols::OLD_0), FE::from(10u64)); - assert_eq!(*trace.get_main(0, cols::OLD_1), FE::from(3u64)); - - // Old timestamp lo - assert_eq!(*trace.get_main(0, cols::OLD_TIMESTAMP_LO), FE::from(50u64)); - - // Multiplicity: is_read = true => MU_READ=1, MU_WRITE=0 - assert_eq!(*trace.get_main(0, cols::MU_READ), FE::from(1u64)); - assert_eq!(*trace.get_main(0, cols::MU_WRITE), FE::from(0u64)); - } - - #[test] - fn test_memw_register_trace_generation_write_op() { - // Write op: is_read = false => MU_WRITE=1, MU_READ=0 - let ops = vec![ - MemwOperation::new( - true, // is_register - 4, // base_address = 2 * register_index (reg x2) - [99, 55, 0, 0, 0, 0, 0, 0], - 200, - 2, // width = 2 words - false, // is_read = false (write) - ) - .with_old([11, 22, 0, 0, 0, 0, 0, 0], [180, 180, 0, 0, 0, 0, 0, 0]), - ]; - - let trace = generate_memw_register_trace(&ops); - - // ADDRESS = base_address / 2 = 4 / 2 = 2 - assert_eq!(*trace.get_main(0, cols::ADDRESS), FE::from(2u64)); - - // Values - assert_eq!(*trace.get_main(0, cols::VAL_0), FE::from(99u64)); - assert_eq!(*trace.get_main(0, cols::VAL_1), FE::from(55u64)); - - // Old values - assert_eq!(*trace.get_main(0, cols::OLD_0), FE::from(11u64)); - assert_eq!(*trace.get_main(0, cols::OLD_1), FE::from(22u64)); - - // Old timestamp lo - assert_eq!(*trace.get_main(0, cols::OLD_TIMESTAMP_LO), FE::from(180u64)); - - // Multiplicity: is_read = false => MU_WRITE=1, MU_READ=0 - assert_eq!(*trace.get_main(0, cols::MU_READ), FE::from(0u64)); - assert_eq!(*trace.get_main(0, cols::MU_WRITE), FE::from(1u64)); - } -} diff --git a/prover/src/tables/page.rs b/prover/src/tables/page.rs index 475ab5279..ecade24d3 100644 --- a/prover/src/tables/page.rs +++ b/prover/src/tables/page.rs @@ -430,111 +430,3 @@ pub fn offset_in_page(addr: u64, page_size: usize) -> usize { ); (addr & (page_size as u64 - 1)) as usize } - -#[cfg(test)] -mod tests { - use super::*; - - #[test] - fn test_page_base_for_address() { - let page_size = 4096; - assert_eq!(page_base_for_address(0x1000, page_size), 0x1000); - assert_eq!(page_base_for_address(0x1001, page_size), 0x1000); - assert_eq!(page_base_for_address(0x1FFF, page_size), 0x1000); - assert_eq!(page_base_for_address(0x2000, page_size), 0x2000); - } - - #[test] - fn test_offset_in_page() { - let page_size = 4096; - assert_eq!(offset_in_page(0x1000, page_size), 0); - assert_eq!(offset_in_page(0x1001, page_size), 1); - assert_eq!(offset_in_page(0x1FFF, page_size), 4095); - assert_eq!(offset_in_page(0x2000, page_size), 0); - } - - #[test] - fn test_generate_page_trace_zero_init() { - let config = PageConfig::zero_init(0x1000, 16); // Small page for testing - let final_state = FinalStateMap::new(); - - let trace = generate_page_trace(&config, &final_state); - - assert_eq!(trace.num_rows(), 16); - - // Check first row (address is virtual: 0x1000 + offset) - assert_eq!(*trace.main_table.get(0, cols::OFFSET), FE::zero()); - assert_eq!(*trace.main_table.get(0, cols::INIT), FE::zero()); - assert_eq!(*trace.main_table.get(0, cols::FINI), FE::zero()); - assert_eq!(*trace.main_table.get(0, cols::TIMESTAMP_LO), FE::zero()); - - // Check last row (address is virtual: 0x1000 + 15 = 0x100F) - assert_eq!(*trace.main_table.get(15, cols::OFFSET), FE::from(15u64)); - assert_eq!(*trace.main_table.get(15, cols::INIT), FE::zero()); - } - - #[test] - fn test_generate_page_trace_with_data() { - let data = vec![0x01, 0x02, 0x03, 0x04]; - let config = PageConfig::with_data(0x2000, 16, data); - let final_state = FinalStateMap::new(); - - let trace = generate_page_trace(&config, &final_state); - - // Check initial values from data - assert_eq!(*trace.main_table.get(0, cols::INIT), FE::from(0x01u64)); - assert_eq!(*trace.main_table.get(1, cols::INIT), FE::from(0x02u64)); - assert_eq!(*trace.main_table.get(2, cols::INIT), FE::from(0x03u64)); - assert_eq!(*trace.main_table.get(3, cols::INIT), FE::from(0x04u64)); - // Rest should be zero (padding) - assert_eq!(*trace.main_table.get(4, cols::INIT), FE::zero()); - - // Without accesses, fini should equal init - assert_eq!(*trace.main_table.get(0, cols::FINI), FE::from(0x01u64)); - } - - #[test] - fn test_generate_page_trace_with_accesses() { - let data = vec![0xAA, 0xBB]; - let config = PageConfig::with_data(0x3000, 16, data); - - let mut final_state = FinalStateMap::new(); - // Address 0x3000 was written with value 0xFF at timestamp 100 - final_state.insert( - 0x3000, - FinalByteState { - timestamp: 100, - value: 0xFF, - }, - ); - - let trace = generate_page_trace(&config, &final_state); - - // Row 0: address 0x3000 - was accessed - assert_eq!(*trace.main_table.get(0, cols::INIT), FE::from(0xAAu64)); - assert_eq!(*trace.main_table.get(0, cols::FINI), FE::from(0xFFu64)); - assert_eq!( - *trace.main_table.get(0, cols::TIMESTAMP_LO), - FE::from(100u64) - ); - - // Row 1: address 0x3001 - not accessed, fini = init - assert_eq!(*trace.main_table.get(1, cols::INIT), FE::from(0xBBu64)); - assert_eq!(*trace.main_table.get(1, cols::FINI), FE::from(0xBBu64)); - assert_eq!(*trace.main_table.get(1, cols::TIMESTAMP_LO), FE::zero()); - } - - #[test] - fn test_bus_interactions() { - let interactions = bus_interactions(0x1000); // page_base - assert_eq!(interactions.len(), 3); // C1+C2 (batched ARE_BYTES), C3, C4 - } - - #[test] - fn test_bus_interactions_high_address() { - // Test with high address like stack region - let stack_page = STACK_TOP & !(DEFAULT_PAGE_SIZE as u64 - 1); - let interactions = bus_interactions(stack_page); - assert_eq!(interactions.len(), 3); - } -} diff --git a/prover/src/tables/register.rs b/prover/src/tables/register.rs index 976b40444..3ff181dbc 100644 --- a/prover/src/tables/register.rs +++ b/prover/src/tables/register.rs @@ -347,89 +347,3 @@ pub fn register_word_addresses(reg_idx: u8) -> Vec { } } } - -#[cfg(test)] -mod tests { - use super::*; - - #[test] - fn test_register_base_address() { - assert_eq!(register_base_address(0), 0); - assert_eq!(register_base_address(1), 2); - assert_eq!(register_base_address(2), 4); - assert_eq!(register_base_address(31), 62); - assert_eq!(register_base_address(254), 508); - assert_eq!(register_base_address(255), 510); - } - - #[test] - fn test_generate_register_trace_empty() { - let entry_point = 0x1000u64; - let final_state = FinalRegisterStateMap::new(); - let trace = generate_register_trace(&final_state, entry_point); - - // Should have power-of-2 rows >= 67 (x0-x31, x254, x255) - assert!(trace.num_rows() >= NUM_REGISTER_ADDRESSES); - assert!(trace.num_rows().is_power_of_two()); - - // Check first row (address 0, never accessed): timestamp defaults to 1 - // per spec/memory.typ so that REG-C1/REG-C2 cancel on the bus. - assert_eq!(*trace.main_table.get(0, cols::OFFSET), FE::zero()); - assert_eq!(*trace.main_table.get(0, cols::INIT), FE::zero()); - assert_eq!(*trace.main_table.get(0, cols::FINI), FE::zero()); - assert_eq!(*trace.main_table.get(0, cols::TIMESTAMP_LO), FE::from(1u64)); - - // Check x254 row (row 64 = addr 508) - assert_eq!(*trace.main_table.get(64, cols::OFFSET), FE::from(508u64)); - assert_eq!(*trace.main_table.get(64, cols::INIT), FE::zero()); - assert_eq!(*trace.main_table.get(64, cols::FINI), FE::zero()); - - // Check x255 rows (row 65 = addr 510, row 66 = addr 511) - assert_eq!(*trace.main_table.get(65, cols::OFFSET), FE::from(510u64)); - assert_eq!( - *trace.main_table.get(65, cols::INIT), - FE::from(entry_point & 0xFFFF_FFFF) - ); - assert_eq!( - *trace.main_table.get(65, cols::FINI), - FE::from(entry_point & 0xFFFF_FFFF) - ); // fini=init when never accessed - assert_eq!(*trace.main_table.get(66, cols::OFFSET), FE::from(511u64)); - assert_eq!( - *trace.main_table.get(66, cols::INIT), - FE::from(entry_point >> 32) - ); - } - - #[test] - fn test_generate_register_trace_with_access() { - let entry_point = 0x1000u64; - let mut final_state = FinalRegisterStateMap::new(); - // Register x5 low Word was written with value 0x42 at timestamp 100 - let addr = register_base_address(5); // = 10 - final_state.insert( - addr, - FinalRegisterWordState { - timestamp: 100, - value: 0x42, - }, - ); - - let trace = generate_register_trace(&final_state, entry_point); - - // Row 10 (address 10) should have the final state - assert_eq!(*trace.main_table.get(10, cols::OFFSET), FE::from(10u64)); - assert_eq!(*trace.main_table.get(10, cols::INIT), FE::zero()); // init is always 0 - assert_eq!(*trace.main_table.get(10, cols::FINI), FE::from(0x42u64)); - assert_eq!( - *trace.main_table.get(10, cols::TIMESTAMP_LO), - FE::from(100u64) - ); - } - - #[test] - fn test_bus_interactions() { - let interactions = bus_interactions(); - assert_eq!(interactions.len(), 2); // C1, C2 - } -} diff --git a/prover/src/tables/trace_builder.rs b/prover/src/tables/trace_builder.rs index 5e787a700..76535484b 100644 --- a/prover/src/tables/trace_builder.rs +++ b/prover/src/tables/trace_builder.rs @@ -1043,7 +1043,7 @@ fn collect_bitwise_from_memw_aligned(ops: &[MemwOperation]) -> Vec bool { +pub(crate) fn is_register_op(op: &MemwOperation) -> bool { if !op.is_register || op.width != 2 { return false; } @@ -1671,7 +1671,7 @@ fn collect_bitwise_from_commit(commit_ops: &[CommitOperation]) -> Vec Vec { +pub(crate) fn collect_bitwise_from_keccak(keccak_ops: &[KeccakOperation]) -> Vec { use executor::vm::instruction::execution::{KECCAK_RC, KECCAK_RHO}; let mut ops = Vec::new(); @@ -3231,260 +3231,3 @@ impl Traces { Ok(traces) } } - -#[cfg(test)] -mod keccak_tests { - use super::*; - use crate::tables::keccak::cols as core_cols; - use crate::tables::keccak_rnd::cols as rnd_cols; - use crate::tables::types::FE; - use executor::vm::instruction::execution::keccak_f1600; - - fn make_keccak_ops() -> (KeccakOperation, KeccakRoundOperation) { - let input = [0u64; 25]; - let mut output = input; - keccak_f1600(&mut output); - let kop = KeccakOperation { - timestamp: 42, - state_addr: 0x1000, - input, - output, - }; - let rop = KeccakRoundOperation { - timestamp: 42, - input, - output, - }; - (kop, rop) - } - - #[test] - fn test_keccak_bitwise_ops_count() { - let (kop, _) = make_keccak_ops(); - let ops = collect_bitwise_from_keccak(&[kop]); - - let xor = ops - .iter() - .filter(|o| o.lookup_type == BitwiseOperationType::XorByte) - .count(); - let and = ops - .iter() - .filter(|o| o.lookup_type == BitwiseOperationType::AndByte) - .count(); - let are_bytes = ops - .iter() - .filter(|o| o.lookup_type == BitwiseOperationType::AreBytes) - .count(); - let hwsl = ops - .iter() - .filter(|o| o.lookup_type == BitwiseOperationType::Hwsl) - .count(); - let is_half = ops - .iter() - .filter(|o| o.lookup_type == BitwiseOperationType::IsHalf) - .count(); - - assert_eq!(xor, 24 * 608, "XorByte count"); - assert_eq!(and, 24 * 200 + 1, "AndByte count"); - // Cxz_right Byte→Bit (spec d75944ee): drops 40 ARE_BYTES per round. - // Spec emits one IS_BYTE template per byte; ops pair adjacent bytes - // into ARE_BYTES (20 cxz_left + 200 rho per round, 4 addr per call). - assert_eq!(are_bytes, 24 * 220 + 4, "AreBytes count"); - assert_eq!(hwsl, 24 * 120, "Hwsl count"); - assert_eq!(is_half, 100, "IsHalf count"); - assert_eq!(ops.len(), 105 + 24 * 1148, "Total bitwise ops"); - } - - #[test] - fn test_keccak_round_trace_matches_f1600() { - let (_, rop) = make_keccak_ops(); - let rnd_trace = keccak_rnd::generate_keccak_rnd_trace(&[rop]); - - let mut ref_state = [0u64; 25]; - for round in 0..24 { - let rc = executor::vm::instruction::execution::KECCAK_RC[round]; - let mut c = [0u64; 5]; - for x in 0..5 { - c[x] = ref_state[x] - ^ ref_state[x + 5] - ^ ref_state[x + 10] - ^ ref_state[x + 15] - ^ ref_state[x + 20]; - } - let mut d = [0u64; 5]; - for x in 0..5 { - d[x] = c[(x + 4) % 5] ^ c[(x + 1) % 5].rotate_left(1); - } - for i in 0..25 { - ref_state[i] ^= d[i % 5]; - } - let mut b = [0u64; 25]; - for x in 0..5 { - for y in 0..5 { - b[y + 5 * ((2 * x + 3 * y) % 5)] = ref_state[x + 5 * y] - .rotate_left(executor::vm::instruction::execution::KECCAK_RHO[x][y]); - } - } - for x in 0..5 { - for y in 0..5 { - ref_state[x + 5 * y] = - b[x + 5 * y] ^ (!b[(x + 1) % 5 + 5 * y] & b[(x + 2) % 5 + 5 * y]); - } - } - ref_state[0] ^= rc; - - let base = round * rnd_cols::NUM_COLUMNS; - for (lane, &lane_val) in ref_state.iter().enumerate() { - let x = lane % 5; - let y = lane / 5; - for byte_idx in 0..8 { - let expected = FE::from((lane_val >> (byte_idx * 8)) & 0xFF); - let col = if x == 0 && y == 0 { - rnd_cols::iota(byte_idx) - } else { - rnd_cols::chi(x, y, byte_idx) - }; - let trace_val = &rnd_trace.main_table.data[base + col]; - assert_eq!( - &expected, trace_val, - "Round {round} lane ({x},{y}) byte {byte_idx}" - ); - } - } - } - } - - #[test] - fn test_keccak_core_round_state_consistency() { - let (kop, rop) = make_keccak_ops(); - let core_trace = keccak::generate_keccak_trace(&[kop]); - let rnd_trace = keccak_rnd::generate_keccak_rnd_trace(&[rop]); - - // Round 0 start == core input_state - for x in 0..5 { - for y in 0..5 { - for b in 0..8 { - let core_val = &core_trace.main_table.data[core_cols::input_state(x, y, b)]; - let rnd_val = &rnd_trace.main_table.data[rnd_cols::start(x, y, b)]; - assert_eq!(core_val, rnd_val, "Round 0 start mismatch at ({x},{y},{b})"); - } - } - } - - // Round 23 out == core output_state - let rnd_base_23 = 23 * rnd_cols::NUM_COLUMNS; - for x in 0..5 { - for y in 0..5 { - for b in 0..8 { - let core_val = &core_trace.main_table.data[core_cols::output_state(x, y, b)]; - let rnd_val = if x == 0 && y == 0 { - &rnd_trace.main_table.data[rnd_base_23 + rnd_cols::iota(b)] - } else { - &rnd_trace.main_table.data[rnd_base_23 + rnd_cols::chi(x, y, b)] - }; - assert_eq!(core_val, rnd_val, "Round 23 out mismatch at ({x},{y},{b})"); - } - } - } - } - - #[test] - fn test_keccak_bus_interaction_counts() { - assert_eq!( - keccak::bus_interactions().len(), - 134, - "KECCAK core: 1 ECALL + 1 MEMW read_addr + 25 MEMW lanes + 100 IS_HALF + 1 AND_BYTE alignment + 4 ARE_BYTES addr pairs + 1 Keccak send + 1 Keccak recv" - ); - assert_eq!( - keccak_rnd::bus_interactions().len(), - 1151, - "KECCAK_RND: 3 IO + 440 theta + 300 rho + 400 chi + 8 iota \ - (Cxz_right Byte→Bit drops 40 ARE_BYTES per spec d75944ee; \ - ARE_BYTES sends are paired per spec ARE_BYTES interaction signature)" - ); - assert_eq!( - keccak_rc::bus_interactions().len(), - 1, - "KECCAK_RC: 1 receiver" - ); - } - - #[test] - fn test_keccak_column_counts() { - assert_eq!(core_cols::NUM_COLUMNS, 511, "KECCAK core columns"); - assert_eq!( - rnd_cols::NUM_COLUMNS, - 1480, - "KECCAK_RND columns (rnc/rbc inlined; pi virtual; Cxz_right Bit-typed)" - ); - assert_eq!(keccak_rc::cols::NUM_COLUMNS, 10, "KECCAK_RC columns"); - } - - #[test] - fn test_keccak_constraint_counts() { - let (core_constraints, _) = keccak::create_constraints(0); - assert_eq!( - core_constraints.len(), - 51, - "KECCAK core: 25 ADD pairs + no-overflow" - ); - - let (rnd_constraints, _) = keccak_rnd::create_constraints(0); - assert_eq!( - rnd_constraints.len(), - 20, - "KECCAK_RND: 20 IS_BIT(μ; Cxz_right_bit) per spec d75944ee" - ); - } -} - -#[cfg(test)] -mod routing_tests { - use super::*; - - fn make_register_op(timestamp: u64, old_timestamp: u64) -> MemwOperation { - MemwOperation::new(true, 2, [1, 0, 0, 0, 0, 0, 0, 0], timestamp, 2, false) - .with_old([0; 8], [old_timestamp, old_timestamp, 0, 0, 0, 0, 0, 0]) - } - - #[test] - fn test_is_register_op_delta_at_boundary_routes_in() { - // delta = 0x10000 = 2^16: spec allows this (IS_HALF[0xFFFF] is valid) - let op = make_register_op(0x10000, 0); - assert!(is_register_op(&op), "delta = 2^16 should route to MEMW_R"); - } - - #[test] - fn test_is_register_op_delta_above_boundary_falls_back() { - // delta = 0x10001: one above the IS_HALF range, must fall back to MEMW_A - let op = make_register_op(0x10001, 0); - assert!( - !is_register_op(&op), - "delta = 2^16 + 1 should fall back to MEMW_A" - ); - } - - #[test] - fn test_is_register_op_delta_one_routes_in() { - // delta = 1: minimum allowed value - let op = make_register_op(1, 0); - assert!(is_register_op(&op), "delta = 1 should route to MEMW_R"); - } - - #[test] - fn test_is_register_op_delta_zero_falls_back() { - // delta = 0: ts[0] not strictly greater than old_ts[0] - let op = make_register_op(5, 5); - assert!(!is_register_op(&op), "delta = 0 should not route to MEMW_R"); - } - - #[test] - fn test_is_register_op_upper_limb_mismatch_falls_back() { - // ts_hi != old_ts_hi: shared upper limb assumption violated - let op = make_register_op(0x1_0000_0001, 0x0_0000_0000); - assert!( - !is_register_op(&op), - "different upper limbs should fall back to MEMW_A" - ); - } -} diff --git a/prover/src/tests/auto_storage_tests.rs b/prover/src/tests/auto_storage_tests.rs new file mode 100644 index 000000000..5d976f81b --- /dev/null +++ b/prover/src/tests/auto_storage_tests.rs @@ -0,0 +1,97 @@ +//! Tests for storage-mode auto-selection. + +use crate::auto_storage::{ + CUBIC_EXT_BYTES, GOLDILOCKS_BYTES, KECCAK_NODE_BYTES, peak_bytes, select_storage_mode, +}; +use crate::tables::cpu::bus_interactions as cpu_buses; +use crate::tables::cpu::cols::NUM_COLUMNS as CPU_COLS; +use crate::tables::trace_builder::TableLengths; +use stark::storage_mode::StorageMode; + +const GB: u64 = 1_000_000_000; +/// Larger than the table count, so every table lands in the top-k and the +/// per-table delta in `peak_bytes_per_table_increment_is_exact` is purely +/// additive. +const ALL_TABLES: usize = 1_000; + +fn empty_lengths() -> TableLengths { + TableLengths::default() +} + +/// Adding rows to a single chunked table must increase `peak_bytes` by +/// exactly the per-row contribution from the formula in the module doc. +/// Verifies the per-table breakdown is exact rather than averaged. +#[test] +fn peak_bytes_per_table_increment_is_exact() { + let blowup = 2u8; + let b = blowup as u64; + + let baseline = peak_bytes(&empty_lengths(), blowup, ALL_TABLES); + + let mut lengths = empty_lengths(); + lengths.cpu_padded_rows = 4; + let bumped = peak_bytes(&lengths, blowup, ALL_TABLES); + + let cpu_main = CPU_COLS as u64; + let cpu_aux = cpu_buses().len().div_ceil(2) as u64; + let per_row_persistent = cpu_main * GOLDILOCKS_BYTES * (1 + b) + + cpu_aux * CUBIC_EXT_BYTES * (1 + b) + + 2 * b * KECCAK_NODE_BYTES // main Merkle (1 tree) + + 2 * b * KECCAK_NODE_BYTES; // aux Merkle + let per_row_transient = b * CUBIC_EXT_BYTES // constraint_evaluations + + 2 * b * CUBIC_EXT_BYTES // composition LDE (2 parts, d=2) + + b * KECCAK_NODE_BYTES // composition Merkle (PairKeccak) + + b * CUBIC_EXT_BYTES // FRI evals (geometric ≈ 1) + + b * KECCAK_NODE_BYTES; // FRI Merkle (geometric ≈ 1) + let per_row_domain = (3 + 2 * b) * GOLDILOCKS_BYTES; + + // CPU adds 4 rows of persistent + transient (top-k by ALL_TABLES) + + // its 4-row Domain entry (a fresh unique key not previously present). + assert_eq!( + bumped - baseline, + 4 * (per_row_persistent + per_row_transient + per_row_domain) + ); +} + +/// Higher blowup_factor should produce a strictly larger estimate. +#[test] +fn peak_bytes_scales_with_blowup() { + let lengths = empty_lengths(); + let two = peak_bytes(&lengths, 2, ALL_TABLES); + let four = peak_bytes(&lengths, 4, ALL_TABLES); + let eight = peak_bytes(&lengths, 8, ALL_TABLES); + assert!(two < four); + assert!(four < eight); +} + +/// Lower table_parallelism caps the transient sum to fewer tables, so the +/// estimate must be monotone in `k`. +#[test] +fn peak_bytes_monotone_in_table_parallelism() { + let lengths = empty_lengths(); + let k1 = peak_bytes(&lengths, 2, 1); + let k4 = peak_bytes(&lengths, 2, 4); + let k_all = peak_bytes(&lengths, 2, ALL_TABLES); + assert!(k1 < k4); + assert!(k4 <= k_all); +} + +#[test] +fn select_ram_when_estimate_below_threshold() { + // 10 GB estimated, 32 GB available → threshold 28.8 GB → Ram. + let mode = select_storage_mode(10 * GB, Some(32 * GB)); + assert_eq!(mode, StorageMode::Ram); +} + +#[test] +fn select_disk_when_estimate_exceeds_threshold() { + // 30 GB estimated, 32 GB available → threshold 28.8 GB → Disk. + let mode = select_storage_mode(30 * GB, Some(32 * GB)); + assert_eq!(mode, StorageMode::Disk); +} + +#[test] +fn unknown_available_defaults_to_disk() { + let mode = select_storage_mode(peak_bytes(&empty_lengths(), 2, ALL_TABLES), None); + assert_eq!(mode, StorageMode::Disk); +} diff --git a/prover/src/tests/decode_tests.rs b/prover/src/tests/decode_tests.rs index 8f61a1d74..c6a436c95 100644 --- a/prover/src/tests/decode_tests.rs +++ b/prover/src/tests/decode_tests.rs @@ -1,13 +1,13 @@ //! Tests for the DECODE table. -use executor::elf::Elf; +use executor::elf::{Elf, Segment}; use executor::vm::instruction::decoding::{ArithOp, Instruction}; use executor::vm::memory::U64HashMap; use math::field::element::FieldElement; use crate::tables::decode::{ DecodeEntry, bus_interactions, cols, generate_decode_trace, instructions_from_elf, - update_multiplicities, + tables_from_elf, update_multiplicities, }; use crate::tables::trace_builder::Traces; use crate::tables::types::{FE, packed_decode as bits}; @@ -1083,3 +1083,75 @@ fn test_decode_soundness_same_elf_accepted() { // With same ELF, verification should SUCCEED assert!(result, "Verifier with same ELF should ACCEPT the proof"); } + +#[test] +fn test_tables_from_elf_single_executable_segment() { + // ADDI x1, x0, 42 (opcode: 0x02a00093) + // ADDI x2, x1, 10 (opcode: 0x00a08113) + let elf = Elf { + entry_point: 0x1000, + data: vec![Segment { + base_addr: 0x1000, + values: vec![0x02a00093, 0x00a08113], + is_executable: true, + }], + }; + + let tables = tables_from_elf(&elf).unwrap(); + + // Check DECODE table + assert_eq!(tables.pc_to_row.len(), 3); // 2 instructions + CPU padding + assert!(tables.pc_to_row.contains_key(&0x1000)); + assert!(tables.pc_to_row.contains_key(&0x1004)); + assert!( + tables + .pc_to_row + .contains_key(&crate::tables::cpu::CPU_PADDING_PC) + ); +} + +#[test] +fn test_tables_from_elf_mixed_segments() { + // Executable segment with instructions + // Data segment with data (not included in DECODE) + let elf = Elf { + entry_point: 0x1000, + data: vec![ + Segment { + base_addr: 0x1000, + values: vec![0x02a00093], // ADDI instruction + is_executable: true, + }, + Segment { + base_addr: 0x2000, + values: vec![0xDEADBEEF, 0xCAFEBABE], // Data + is_executable: false, + }, + ], + }; + + let tables = tables_from_elf(&elf).unwrap(); + + // DECODE: only executable segment (1 instruction + CPU padding) + assert_eq!(tables.pc_to_row.len(), 2); + assert!(tables.pc_to_row.contains_key(&0x1000)); + assert!(!tables.pc_to_row.contains_key(&0x2000)); // Data not in decode +} + +#[test] +fn test_tables_from_elf_empty() { + let elf = Elf { + entry_point: 0x1000, + data: vec![], + }; + + let tables = tables_from_elf(&elf).unwrap(); + + // DECODE: only CPU padding entry + assert_eq!(tables.pc_to_row.len(), 1); + assert!( + tables + .pc_to_row + .contains_key(&crate::tables::cpu::CPU_PADDING_PC) + ); +} diff --git a/prover/src/tests/keccak_rnd_tests.rs b/prover/src/tests/keccak_rnd_tests.rs new file mode 100644 index 000000000..ce8f614c8 --- /dev/null +++ b/prover/src/tests/keccak_rnd_tests.rs @@ -0,0 +1,59 @@ +//! Tests for the KECCAK_RND table. + +use crate::tables::keccak_rnd::*; +use crate::tables::types::*; + +use executor::vm::instruction::execution::{KECCAK_RHO, keccak_f1600}; + +/// pi is a spec virtual variable. Verify the inlined expression +/// (rot_left[sx,sy,l_byte] + rot_right[sx,sy,r_byte]) matches the byte of +/// rho(theta) for a non-trivial state. Uses mu=0 padding rows as a trivial +/// sanity check (all zeros), then a non-zero-input round as the real test. +#[test] +fn test_pi_virtual_matches_rotate() { + // Use a non-zero input so theta_lanes are non-trivial. + let input = [0x0102030405060708u64; 25]; + let mut output = input; + keccak_f1600(&mut output); + let op = KeccakRoundOperation { + timestamp: 42, + input, + output, + }; + let trace = generate_keccak_rnd_trace(&[op]); + let base = 0; + + // Recompute theta for round 0 in u64 to compare against virtual pi. + let mut c = [0u64; 5]; + for x in 0..5 { + c[x] = input[x] ^ input[x + 5] ^ input[x + 10] ^ input[x + 15] ^ input[x + 20]; + } + let mut d = [0u64; 5]; + for x in 0..5 { + d[x] = c[(x + 4) % 5] ^ c[(x + 1) % 5].rotate_left(1); + } + let mut theta_lanes = [0u64; 25]; + for x in 0..5 { + for y in 0..5 { + theta_lanes[x + 5 * y] = input[x + 5 * y] ^ d[x]; + } + } + + for x in 0..5 { + for y in 0..5 { + let sx = (x + 3 * y) % 5; + let sy = x; + let rotated = theta_lanes[sx + 5 * sy].rotate_left(KECCAK_RHO[sx][sy]); + for z in 0..8 { + let (l_col, r_col) = cols::pi_src_cols(x, y, z); + let virtual_pi = + &trace.main_table.data[base + l_col] + &trace.main_table.data[base + r_col]; + let expected = FE::from((rotated >> (z * 8)) & 0xFF); + assert_eq!( + virtual_pi, expected, + "virtual pi mismatch at ({x},{y},{z}): sx={sx}, sy={sy}" + ); + } + } + } +} diff --git a/prover/src/tests/load_tests.rs b/prover/src/tests/load_tests.rs new file mode 100644 index 000000000..a85a7a920 --- /dev/null +++ b/prover/src/tests/load_tests.rs @@ -0,0 +1,63 @@ +//! Tests for the LOAD table. + +use crate::tables::load::*; + +#[test] +fn test_load_trace_generation() { + // Load 4 bytes, sign-extend + let ops = vec![ + LoadOperation::new( + 0x1000, + 100, + 4, + true, + [0x12, 0x34, 0x56, 0x78, 0xFF, 0xFF, 0xFF, 0xFF], + ), + LoadOperation::new( + 0x2000, + 200, + 1, + false, + [0x42, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00], + ), + ]; + + let trace = generate_load_trace(&ops); + assert_eq!(trace.num_cols(), cols::NUM_COLUMNS); + assert!(trace.num_rows() >= 2); +} + +#[test] +fn test_read_flags() { + // "Exactly N" semantics per spec + let op1 = LoadOperation::new(0, 0, 1, false, [0; 8]); + assert_eq!(op1.read_flags(), (false, false, false)); // no flags for 1 byte + + let op2 = LoadOperation::new(0, 0, 2, false, [0; 8]); + assert_eq!(op2.read_flags(), (true, false, false)); // read2 only + + let op4 = LoadOperation::new(0, 0, 4, false, [0; 8]); + assert_eq!(op4.read_flags(), (false, true, false)); // read4 only + + let op8 = LoadOperation::new(0, 0, 8, false, [0; 8]); + assert_eq!(op8.read_flags(), (false, false, true)); // read8 only +} + +#[test] +fn test_sign_bit_extraction() { + // Byte with MSB set + let op1 = LoadOperation::new(0, 0, 1, true, [0x80, 0, 0, 0, 0, 0, 0, 0]); + assert!(op1.compute_sign_bit()); + + // Byte without MSB set + let op2 = LoadOperation::new(0, 0, 1, true, [0x7F, 0, 0, 0, 0, 0, 0, 0]); + assert!(!op2.compute_sign_bit()); + + // Halfword with MSB set + let op3 = LoadOperation::new(0, 0, 2, true, [0x00, 0x80, 0, 0, 0, 0, 0, 0]); + assert!(op3.compute_sign_bit()); + + // Word with MSB set + let op4 = LoadOperation::new(0, 0, 4, true, [0, 0, 0, 0x80, 0, 0, 0, 0]); + assert!(op4.compute_sign_bit()); +} diff --git a/prover/src/tests/memw_aligned_tests.rs b/prover/src/tests/memw_aligned_tests.rs new file mode 100644 index 000000000..49ac8cc5c --- /dev/null +++ b/prover/src/tests/memw_aligned_tests.rs @@ -0,0 +1,30 @@ +//! Tests for the MEMW_A (aligned memory word) table. + +use crate::tables::memw::MemwOperation; +use crate::tables::memw_aligned::*; +use crate::tables::types::*; + +#[test] +fn test_memw_aligned_trace_generation() { + let ops = vec![ + MemwOperation::new(true, 4, [42, 0, 0, 0, 0, 0, 0, 0], 100, 2, true) + .with_old([42, 0, 0, 0, 0, 0, 0, 0], [50, 50, 0, 0, 0, 0, 0, 0]), + MemwOperation::new(false, 0x1000, [1, 2, 3, 4, 0, 0, 0, 0], 200, 4, false) + .with_old([0; 8], [100; 8]), + ]; + + let trace = generate_memw_aligned_trace(&ops); + assert_eq!(trace.num_cols(), cols::NUM_COLUMNS); + assert!(trace.num_rows() >= 2); + + // Check address decomposition for op[1]: addr = 0x1000 + // base_address[0] (low half) = 0x1000 + // base_address[1] (mid half) = 0 + // base_address[2] (high word) = 0 + assert_eq!( + *trace.get_main(1, cols::BASE_ADDRESS[0]), + FE::from(0x1000u64) + ); + assert_eq!(*trace.get_main(1, cols::BASE_ADDRESS[1]), FE::from(0u64)); + assert_eq!(*trace.get_main(1, cols::BASE_ADDRESS[2]), FE::from(0u64)); +} diff --git a/prover/src/tests/memw_register_tests.rs b/prover/src/tests/memw_register_tests.rs new file mode 100644 index 000000000..56b8a372c --- /dev/null +++ b/prover/src/tests/memw_register_tests.rs @@ -0,0 +1,83 @@ +//! Tests for the MEMW_R (register memory word) table. + +use crate::tables::memw::MemwOperation; +use crate::tables::memw_register::*; +use crate::tables::types::*; + +#[test] +fn test_memw_register_trace_generation() { + // Create a simple register op (reg x1 = address 1, so base_address = 2) + let ops = vec![ + MemwOperation::new( + true, // is_register + 2, // base_address = 2 * register_index (reg x1) + [42, 7, 0, 0, 0, 0, 0, 0], + 100, + 2, // width = 2 words (registers are DWordWL) + true, + ) + .with_old([10, 3, 0, 0, 0, 0, 0, 0], [50, 50, 0, 0, 0, 0, 0, 0]), + ]; + + let trace = generate_memw_register_trace(&ops); + assert_eq!(trace.num_cols(), cols::NUM_COLUMNS); + assert!(trace.num_rows() >= 4); // minimum 4 rows + + // ADDRESS = base_address / 2 = 2 / 2 = 1 + assert_eq!(*trace.get_main(0, cols::ADDRESS), FE::from(1u64)); + + // TIMESTAMP split + assert_eq!(*trace.get_main(0, cols::TIMESTAMP_0), FE::from(100u64)); + assert_eq!(*trace.get_main(0, cols::TIMESTAMP_1), FE::from(0u64)); + + // Values + assert_eq!(*trace.get_main(0, cols::VAL_0), FE::from(42u64)); + assert_eq!(*trace.get_main(0, cols::VAL_1), FE::from(7u64)); + + // Old values + assert_eq!(*trace.get_main(0, cols::OLD_0), FE::from(10u64)); + assert_eq!(*trace.get_main(0, cols::OLD_1), FE::from(3u64)); + + // Old timestamp lo + assert_eq!(*trace.get_main(0, cols::OLD_TIMESTAMP_LO), FE::from(50u64)); + + // Multiplicity: is_read = true => MU_READ=1, MU_WRITE=0 + assert_eq!(*trace.get_main(0, cols::MU_READ), FE::from(1u64)); + assert_eq!(*trace.get_main(0, cols::MU_WRITE), FE::from(0u64)); +} + +#[test] +fn test_memw_register_trace_generation_write_op() { + // Write op: is_read = false => MU_WRITE=1, MU_READ=0 + let ops = vec![ + MemwOperation::new( + true, // is_register + 4, // base_address = 2 * register_index (reg x2) + [99, 55, 0, 0, 0, 0, 0, 0], + 200, + 2, // width = 2 words + false, // is_read = false (write) + ) + .with_old([11, 22, 0, 0, 0, 0, 0, 0], [180, 180, 0, 0, 0, 0, 0, 0]), + ]; + + let trace = generate_memw_register_trace(&ops); + + // ADDRESS = base_address / 2 = 4 / 2 = 2 + assert_eq!(*trace.get_main(0, cols::ADDRESS), FE::from(2u64)); + + // Values + assert_eq!(*trace.get_main(0, cols::VAL_0), FE::from(99u64)); + assert_eq!(*trace.get_main(0, cols::VAL_1), FE::from(55u64)); + + // Old values + assert_eq!(*trace.get_main(0, cols::OLD_0), FE::from(11u64)); + assert_eq!(*trace.get_main(0, cols::OLD_1), FE::from(22u64)); + + // Old timestamp lo + assert_eq!(*trace.get_main(0, cols::OLD_TIMESTAMP_LO), FE::from(180u64)); + + // Multiplicity: is_read = false => MU_WRITE=1, MU_READ=0 + assert_eq!(*trace.get_main(0, cols::MU_READ), FE::from(0u64)); + assert_eq!(*trace.get_main(0, cols::MU_WRITE), FE::from(1u64)); +} diff --git a/prover/src/tests/memw_tests.rs b/prover/src/tests/memw_tests.rs new file mode 100644 index 000000000..e6830efad --- /dev/null +++ b/prover/src/tests/memw_tests.rs @@ -0,0 +1,77 @@ +//! Tests for the MEMW table. + +use crate::tables::memw::*; +use crate::tables::types::*; + +#[test] +fn test_memw_trace_generation() { + let ops = vec![ + MemwOperation::new(false, 0x1000, [1, 2, 3, 4, 5, 6, 7, 8], 100, 8, false) + .with_old([0; 8], [50; 8]), + MemwOperation::new(true, 5, [42, 0, 0, 0, 0, 0, 0, 0], 200, 1, true) + .with_old([10, 0, 0, 0, 0, 0, 0, 0], [150, 0, 0, 0, 0, 0, 0, 0]), + ]; + + let trace = generate_memw_trace(&ops); + assert_eq!(trace.num_cols(), cols::NUM_COLUMNS); + assert!(trace.num_rows() >= 2); +} + +#[test] +fn test_write_flags() { + let op1 = MemwOperation::new(false, 0, [0; 8], 0, 1, false); + assert_eq!(op1.write_flags(), (false, false, false)); + + let op2 = MemwOperation::new(false, 0, [0; 8], 0, 2, false); + assert_eq!(op2.write_flags(), (true, false, false)); + + let op4 = MemwOperation::new(false, 0, [0; 8], 0, 4, false); + assert_eq!(op4.write_flags(), (false, true, false)); + + let op8 = MemwOperation::new(false, 0, [0; 8], 0, 8, false); + assert_eq!(op8.write_flags(), (false, false, true)); +} + +#[test] +fn test_carry_flags() { + // Address 0xFFFF_FFFF should carry when adding 1 + let op = + MemwOperation::new(false, 0xFFFF_FFFF, [0; 8], 100, 8, false).with_old([0; 8], [50; 8]); + let trace = generate_memw_trace(&[op]); + + // All 7 carry flags should be 1 since 0xFFFF_FFFF + i >= 2^32 for i >= 1 + for i in 0..7 { + let val = trace.get_main(0, cols::CARRY[i]); + assert_eq!(*val, FE::one(), "carry[{i}] should be 1"); + } + + // Address 0x0000_0000 should not carry + let op2 = + MemwOperation::new(false, 0x0000_0000, [0; 8], 100, 8, false).with_old([0; 8], [50; 8]); + let trace2 = generate_memw_trace(&[op2]); + for i in 0..7 { + let val = trace2.get_main(0, cols::CARRY[i]); + assert_eq!(*val, FE::zero(), "carry[{i}] should be 0"); + } + + // Address 0xFFFF_FFFE with width=8 exercises mixed per-byte carry bits: + // carry[0]=0 (0xFFFF_FFFE+1 = 0xFFFF_FFFF < 2^32) + // carry[1..6]=1 (0xFFFF_FFFE+2..8 >= 2^32) + let op3 = + MemwOperation::new(false, 0xFFFF_FFFE, [0; 8], 100, 8, false).with_old([0; 8], [50; 8]); + let trace3 = generate_memw_trace(&[op3]); + let val0 = trace3.get_main(0, cols::CARRY[0]); + assert_eq!( + *val0, + FE::zero(), + "carry[0] should be 0 for base 0xFFFF_FFFE" + ); + for i in 1..7 { + let val = trace3.get_main(0, cols::CARRY[i]); + assert_eq!( + *val, + FE::one(), + "carry[{i}] should be 1 for base 0xFFFF_FFFE" + ); + } +} diff --git a/prover/src/tests/mod.rs b/prover/src/tests/mod.rs index 91a92ad46..4fcdba7f4 100644 --- a/prover/src/tests/mod.rs +++ b/prover/src/tests/mod.rs @@ -1,3 +1,5 @@ +#[cfg(all(test, feature = "disk-spill"))] +pub mod auto_storage_tests; #[cfg(test)] pub mod bitwise_bus_tests; #[cfg(test)] @@ -23,14 +25,30 @@ pub mod disk_spill_tests; #[cfg(test)] pub mod dvrm_tests; #[cfg(test)] +pub mod keccak_rnd_tests; +#[cfg(test)] +pub mod load_tests; +#[cfg(test)] pub mod lt_bus_tests; #[cfg(test)] pub mod lt_tests; #[cfg(test)] +pub mod memw_aligned_tests; +#[cfg(test)] +pub mod memw_register_tests; +#[cfg(test)] +pub mod memw_tests; +#[cfg(test)] pub mod mul_tests; #[cfg(test)] +pub mod page_tests; +#[cfg(test)] pub mod prove_elfs_tests; #[cfg(test)] +pub mod register_tests; +#[cfg(test)] pub mod statement_tests; #[cfg(test)] +pub mod templates_tests; +#[cfg(test)] pub mod trace_builder_tests; diff --git a/prover/src/tests/page_tests.rs b/prover/src/tests/page_tests.rs new file mode 100644 index 000000000..23978c123 --- /dev/null +++ b/prover/src/tests/page_tests.rs @@ -0,0 +1,107 @@ +//! Tests for the PAGE table. + +use crate::tables::page::*; +use crate::tables::types::*; + +#[test] +fn test_page_base_for_address() { + let page_size = 4096; + assert_eq!(page_base_for_address(0x1000, page_size), 0x1000); + assert_eq!(page_base_for_address(0x1001, page_size), 0x1000); + assert_eq!(page_base_for_address(0x1FFF, page_size), 0x1000); + assert_eq!(page_base_for_address(0x2000, page_size), 0x2000); +} + +#[test] +fn test_offset_in_page() { + let page_size = 4096; + assert_eq!(offset_in_page(0x1000, page_size), 0); + assert_eq!(offset_in_page(0x1001, page_size), 1); + assert_eq!(offset_in_page(0x1FFF, page_size), 4095); + assert_eq!(offset_in_page(0x2000, page_size), 0); +} + +#[test] +fn test_generate_page_trace_zero_init() { + let config = PageConfig::zero_init(0x1000, 16); // Small page for testing + let final_state = FinalStateMap::new(); + + let trace = generate_page_trace(&config, &final_state); + + assert_eq!(trace.num_rows(), 16); + + // Check first row (address is virtual: 0x1000 + offset) + assert_eq!(*trace.main_table.get(0, cols::OFFSET), FE::zero()); + assert_eq!(*trace.main_table.get(0, cols::INIT), FE::zero()); + assert_eq!(*trace.main_table.get(0, cols::FINI), FE::zero()); + assert_eq!(*trace.main_table.get(0, cols::TIMESTAMP_LO), FE::zero()); + + // Check last row (address is virtual: 0x1000 + 15 = 0x100F) + assert_eq!(*trace.main_table.get(15, cols::OFFSET), FE::from(15u64)); + assert_eq!(*trace.main_table.get(15, cols::INIT), FE::zero()); +} + +#[test] +fn test_generate_page_trace_with_data() { + let data = vec![0x01, 0x02, 0x03, 0x04]; + let config = PageConfig::with_data(0x2000, 16, data); + let final_state = FinalStateMap::new(); + + let trace = generate_page_trace(&config, &final_state); + + // Check initial values from data + assert_eq!(*trace.main_table.get(0, cols::INIT), FE::from(0x01u64)); + assert_eq!(*trace.main_table.get(1, cols::INIT), FE::from(0x02u64)); + assert_eq!(*trace.main_table.get(2, cols::INIT), FE::from(0x03u64)); + assert_eq!(*trace.main_table.get(3, cols::INIT), FE::from(0x04u64)); + // Rest should be zero (padding) + assert_eq!(*trace.main_table.get(4, cols::INIT), FE::zero()); + + // Without accesses, fini should equal init + assert_eq!(*trace.main_table.get(0, cols::FINI), FE::from(0x01u64)); +} + +#[test] +fn test_generate_page_trace_with_accesses() { + let data = vec![0xAA, 0xBB]; + let config = PageConfig::with_data(0x3000, 16, data); + + let mut final_state = FinalStateMap::new(); + // Address 0x3000 was written with value 0xFF at timestamp 100 + final_state.insert( + 0x3000, + FinalByteState { + timestamp: 100, + value: 0xFF, + }, + ); + + let trace = generate_page_trace(&config, &final_state); + + // Row 0: address 0x3000 - was accessed + assert_eq!(*trace.main_table.get(0, cols::INIT), FE::from(0xAAu64)); + assert_eq!(*trace.main_table.get(0, cols::FINI), FE::from(0xFFu64)); + assert_eq!( + *trace.main_table.get(0, cols::TIMESTAMP_LO), + FE::from(100u64) + ); + + // Row 1: address 0x3001 - not accessed, fini = init + assert_eq!(*trace.main_table.get(1, cols::INIT), FE::from(0xBBu64)); + assert_eq!(*trace.main_table.get(1, cols::FINI), FE::from(0xBBu64)); + assert_eq!(*trace.main_table.get(1, cols::TIMESTAMP_LO), FE::zero()); +} + +#[test] +fn test_bus_interactions() { + let interactions = bus_interactions(0x1000); // page_base + assert_eq!(interactions.len(), 3); // C1+C2 (batched ARE_BYTES), C3, C4 +} + +#[test] +fn test_bus_interactions_high_address() { + // Test with high address like stack region + let stack_page = STACK_TOP & !(DEFAULT_PAGE_SIZE as u64 - 1); + let interactions = bus_interactions(stack_page); + assert_eq!(interactions.len(), 3); +} diff --git a/prover/src/tests/register_tests.rs b/prover/src/tests/register_tests.rs new file mode 100644 index 000000000..1baa55eda --- /dev/null +++ b/prover/src/tests/register_tests.rs @@ -0,0 +1,85 @@ +//! Tests for the REGISTER table. + +use crate::tables::register::*; +use crate::tables::types::*; + +#[test] +fn test_register_base_address() { + assert_eq!(register_base_address(0), 0); + assert_eq!(register_base_address(1), 2); + assert_eq!(register_base_address(2), 4); + assert_eq!(register_base_address(31), 62); + assert_eq!(register_base_address(254), 508); + assert_eq!(register_base_address(255), 510); +} + +#[test] +fn test_generate_register_trace_empty() { + let entry_point = 0x1000u64; + let final_state = FinalRegisterStateMap::new(); + let trace = generate_register_trace(&final_state, entry_point); + + // Should have power-of-2 rows >= 67 (x0-x31, x254, x255) + assert!(trace.num_rows() >= NUM_REGISTER_ADDRESSES); + assert!(trace.num_rows().is_power_of_two()); + + // Check first row (address 0, never accessed): timestamp defaults to 1 + // per spec/memory.typ so that REG-C1/REG-C2 cancel on the bus. + assert_eq!(*trace.main_table.get(0, cols::OFFSET), FE::zero()); + assert_eq!(*trace.main_table.get(0, cols::INIT), FE::zero()); + assert_eq!(*trace.main_table.get(0, cols::FINI), FE::zero()); + assert_eq!(*trace.main_table.get(0, cols::TIMESTAMP_LO), FE::from(1u64)); + + // Check x254 row (row 64 = addr 508) + assert_eq!(*trace.main_table.get(64, cols::OFFSET), FE::from(508u64)); + assert_eq!(*trace.main_table.get(64, cols::INIT), FE::zero()); + assert_eq!(*trace.main_table.get(64, cols::FINI), FE::zero()); + + // Check x255 rows (row 65 = addr 510, row 66 = addr 511) + assert_eq!(*trace.main_table.get(65, cols::OFFSET), FE::from(510u64)); + assert_eq!( + *trace.main_table.get(65, cols::INIT), + FE::from(entry_point & 0xFFFF_FFFF) + ); + assert_eq!( + *trace.main_table.get(65, cols::FINI), + FE::from(entry_point & 0xFFFF_FFFF) + ); // fini=init when never accessed + assert_eq!(*trace.main_table.get(66, cols::OFFSET), FE::from(511u64)); + assert_eq!( + *trace.main_table.get(66, cols::INIT), + FE::from(entry_point >> 32) + ); +} + +#[test] +fn test_generate_register_trace_with_access() { + let entry_point = 0x1000u64; + let mut final_state = FinalRegisterStateMap::new(); + // Register x5 low Word was written with value 0x42 at timestamp 100 + let addr = register_base_address(5); // = 10 + final_state.insert( + addr, + FinalRegisterWordState { + timestamp: 100, + value: 0x42, + }, + ); + + let trace = generate_register_trace(&final_state, entry_point); + + // Row 10 (address 10) should have the final state + assert_eq!(*trace.main_table.get(10, cols::OFFSET), FE::from(10u64)); + assert_eq!(*trace.main_table.get(10, cols::INIT), FE::zero()); // init is always 0 + assert_eq!(*trace.main_table.get(10, cols::FINI), FE::from(0x42u64)); + assert_eq!( + *trace.main_table.get(10, cols::TIMESTAMP_LO), + FE::from(100u64) + ); +} + +#[test] +fn test_bus_interactions() { + let interactions = bus_interactions(); + assert_eq!(interactions.len(), 2); // C1, C2 +} diff --git a/prover/src/tests/templates_tests.rs b/prover/src/tests/templates_tests.rs new file mode 100644 index 000000000..709ab1313 --- /dev/null +++ b/prover/src/tests/templates_tests.rs @@ -0,0 +1,12 @@ +//! Tests for constraint templates. + +use crate::constraints::templates::*; +use crate::tables::types::GoldilocksField; +use math::field::element::FieldElement; + +#[test] +fn test_inv_shift_32_is_correct() { + let inv = FieldElement::::from(INV_SHIFT_32); + let shift = FieldElement::::from(SHIFT_32); + assert_eq!(inv * shift, FieldElement::one()); +} diff --git a/prover/src/tests/trace_builder_tests.rs b/prover/src/tests/trace_builder_tests.rs index 0e54f353c..199ce71db 100644 --- a/prover/src/tests/trace_builder_tests.rs +++ b/prover/src/tests/trace_builder_tests.rs @@ -562,3 +562,263 @@ fn test_lt_generates_bitwise_lookups() { "IS_HALF lookup for lhs_sub_rhs[0] should have non-zero multiplicity" ); } + +mod keccak_tests { + use crate::tables::bitwise::BitwiseOperationType; + use crate::tables::keccak::cols as core_cols; + use crate::tables::keccak::{self, KeccakOperation}; + use crate::tables::keccak_rc; + use crate::tables::keccak_rnd::cols as rnd_cols; + use crate::tables::keccak_rnd::{self, KeccakRoundOperation}; + use crate::tables::trace_builder::*; + use crate::tables::types::FE; + use executor::vm::instruction::execution::keccak_f1600; + + fn make_keccak_ops() -> (KeccakOperation, KeccakRoundOperation) { + let input = [0u64; 25]; + let mut output = input; + keccak_f1600(&mut output); + let kop = KeccakOperation { + timestamp: 42, + state_addr: 0x1000, + input, + output, + }; + let rop = KeccakRoundOperation { + timestamp: 42, + input, + output, + }; + (kop, rop) + } + + #[test] + fn test_keccak_bitwise_ops_count() { + let (kop, _) = make_keccak_ops(); + let ops = collect_bitwise_from_keccak(&[kop]); + + let xor = ops + .iter() + .filter(|o| o.lookup_type == BitwiseOperationType::XorByte) + .count(); + let and = ops + .iter() + .filter(|o| o.lookup_type == BitwiseOperationType::AndByte) + .count(); + let are_bytes = ops + .iter() + .filter(|o| o.lookup_type == BitwiseOperationType::AreBytes) + .count(); + let hwsl = ops + .iter() + .filter(|o| o.lookup_type == BitwiseOperationType::Hwsl) + .count(); + let is_half = ops + .iter() + .filter(|o| o.lookup_type == BitwiseOperationType::IsHalf) + .count(); + + assert_eq!(xor, 24 * 608, "XorByte count"); + assert_eq!(and, 24 * 200 + 1, "AndByte count"); + // Cxz_right Byte→Bit (spec d75944ee): drops 40 ARE_BYTES per round. + // Spec emits one IS_BYTE template per byte; ops pair adjacent bytes + // into ARE_BYTES (20 cxz_left + 200 rho per round, 4 addr per call). + assert_eq!(are_bytes, 24 * 220 + 4, "AreBytes count"); + assert_eq!(hwsl, 24 * 120, "Hwsl count"); + assert_eq!(is_half, 100, "IsHalf count"); + assert_eq!(ops.len(), 105 + 24 * 1148, "Total bitwise ops"); + } + + #[test] + fn test_keccak_round_trace_matches_f1600() { + let (_, rop) = make_keccak_ops(); + let rnd_trace = keccak_rnd::generate_keccak_rnd_trace(&[rop]); + + let mut ref_state = [0u64; 25]; + for round in 0..24 { + let rc = executor::vm::instruction::execution::KECCAK_RC[round]; + let mut c = [0u64; 5]; + for x in 0..5 { + c[x] = ref_state[x] + ^ ref_state[x + 5] + ^ ref_state[x + 10] + ^ ref_state[x + 15] + ^ ref_state[x + 20]; + } + let mut d = [0u64; 5]; + for x in 0..5 { + d[x] = c[(x + 4) % 5] ^ c[(x + 1) % 5].rotate_left(1); + } + for i in 0..25 { + ref_state[i] ^= d[i % 5]; + } + let mut b = [0u64; 25]; + for x in 0..5 { + for y in 0..5 { + b[y + 5 * ((2 * x + 3 * y) % 5)] = ref_state[x + 5 * y] + .rotate_left(executor::vm::instruction::execution::KECCAK_RHO[x][y]); + } + } + for x in 0..5 { + for y in 0..5 { + ref_state[x + 5 * y] = + b[x + 5 * y] ^ (!b[(x + 1) % 5 + 5 * y] & b[(x + 2) % 5 + 5 * y]); + } + } + ref_state[0] ^= rc; + + let base = round * rnd_cols::NUM_COLUMNS; + for (lane, &lane_val) in ref_state.iter().enumerate() { + let x = lane % 5; + let y = lane / 5; + for byte_idx in 0..8 { + let expected = FE::from((lane_val >> (byte_idx * 8)) & 0xFF); + let col = if x == 0 && y == 0 { + rnd_cols::iota(byte_idx) + } else { + rnd_cols::chi(x, y, byte_idx) + }; + let trace_val = &rnd_trace.main_table.data[base + col]; + assert_eq!( + &expected, trace_val, + "Round {round} lane ({x},{y}) byte {byte_idx}" + ); + } + } + } + } + + #[test] + fn test_keccak_core_round_state_consistency() { + let (kop, rop) = make_keccak_ops(); + let core_trace = keccak::generate_keccak_trace(&[kop]); + let rnd_trace = keccak_rnd::generate_keccak_rnd_trace(&[rop]); + + // Round 0 start == core input_state + for x in 0..5 { + for y in 0..5 { + for b in 0..8 { + let core_val = &core_trace.main_table.data[core_cols::input_state(x, y, b)]; + let rnd_val = &rnd_trace.main_table.data[rnd_cols::start(x, y, b)]; + assert_eq!(core_val, rnd_val, "Round 0 start mismatch at ({x},{y},{b})"); + } + } + } + + // Round 23 out == core output_state + let rnd_base_23 = 23 * rnd_cols::NUM_COLUMNS; + for x in 0..5 { + for y in 0..5 { + for b in 0..8 { + let core_val = &core_trace.main_table.data[core_cols::output_state(x, y, b)]; + let rnd_val = if x == 0 && y == 0 { + &rnd_trace.main_table.data[rnd_base_23 + rnd_cols::iota(b)] + } else { + &rnd_trace.main_table.data[rnd_base_23 + rnd_cols::chi(x, y, b)] + }; + assert_eq!(core_val, rnd_val, "Round 23 out mismatch at ({x},{y},{b})"); + } + } + } + } + + #[test] + fn test_keccak_bus_interaction_counts() { + assert_eq!( + keccak::bus_interactions().len(), + 134, + "KECCAK core: 1 ECALL + 1 MEMW read_addr + 25 MEMW lanes + 100 IS_HALF + 1 AND_BYTE alignment + 4 ARE_BYTES addr pairs + 1 Keccak send + 1 Keccak recv" + ); + assert_eq!( + keccak_rnd::bus_interactions().len(), + 1151, + "KECCAK_RND: 3 IO + 440 theta + 300 rho + 400 chi + 8 iota \ + (Cxz_right Byte→Bit drops 40 ARE_BYTES per spec d75944ee; \ + ARE_BYTES sends are paired per spec ARE_BYTES interaction signature)" + ); + assert_eq!( + keccak_rc::bus_interactions().len(), + 1, + "KECCAK_RC: 1 receiver" + ); + } + + #[test] + fn test_keccak_column_counts() { + assert_eq!(core_cols::NUM_COLUMNS, 511, "KECCAK core columns"); + assert_eq!( + rnd_cols::NUM_COLUMNS, + 1480, + "KECCAK_RND columns (rnc/rbc inlined; pi virtual; Cxz_right Bit-typed)" + ); + assert_eq!(keccak_rc::cols::NUM_COLUMNS, 10, "KECCAK_RC columns"); + } + + #[test] + fn test_keccak_constraint_counts() { + let (core_constraints, _) = keccak::create_constraints(0); + assert_eq!( + core_constraints.len(), + 51, + "KECCAK core: 25 ADD pairs + no-overflow" + ); + + let (rnd_constraints, _) = keccak_rnd::create_constraints(0); + assert_eq!( + rnd_constraints.len(), + 20, + "KECCAK_RND: 20 IS_BIT(μ; Cxz_right_bit) per spec d75944ee" + ); + } +} + +mod routing_tests { + use crate::tables::memw::MemwOperation; + use crate::tables::trace_builder::*; + + fn make_register_op(timestamp: u64, old_timestamp: u64) -> MemwOperation { + MemwOperation::new(true, 2, [1, 0, 0, 0, 0, 0, 0, 0], timestamp, 2, false) + .with_old([0; 8], [old_timestamp, old_timestamp, 0, 0, 0, 0, 0, 0]) + } + + #[test] + fn test_is_register_op_delta_at_boundary_routes_in() { + // delta = 0x10000 = 2^16: spec allows this (IS_HALF[0xFFFF] is valid) + let op = make_register_op(0x10000, 0); + assert!(is_register_op(&op), "delta = 2^16 should route to MEMW_R"); + } + + #[test] + fn test_is_register_op_delta_above_boundary_falls_back() { + // delta = 0x10001: one above the IS_HALF range, must fall back to MEMW_A + let op = make_register_op(0x10001, 0); + assert!( + !is_register_op(&op), + "delta = 2^16 + 1 should fall back to MEMW_A" + ); + } + + #[test] + fn test_is_register_op_delta_one_routes_in() { + // delta = 1: minimum allowed value + let op = make_register_op(1, 0); + assert!(is_register_op(&op), "delta = 1 should route to MEMW_R"); + } + + #[test] + fn test_is_register_op_delta_zero_falls_back() { + // delta = 0: ts[0] not strictly greater than old_ts[0] + let op = make_register_op(5, 5); + assert!(!is_register_op(&op), "delta = 0 should not route to MEMW_R"); + } + + #[test] + fn test_is_register_op_upper_limb_mismatch_falls_back() { + // ts_hi != old_ts_hi: shared upper limb assumption violated + let op = make_register_op(0x1_0000_0001, 0x0_0000_0000); + assert!( + !is_register_op(&op), + "different upper limbs should fall back to MEMW_A" + ); + } +}