Skip to content
Open
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
101 changes: 4 additions & 97 deletions prover/src/auto_storage.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down Expand Up @@ -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<u64>) -> StorageMode {
pub(crate) fn select_storage_mode(estimated: u64, available: Option<u64>) -> StorageMode {
let Some(available) = available else {
log::warn!("Auto disk-spill: sysinfo could not read system memory, defaulting to Disk.");
return StorageMode::Disk;
Expand All @@ -307,96 +307,3 @@ fn available_ram_bytes() -> Option<u64> {
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);
}
}
13 changes: 0 additions & 13 deletions prover/src/constraints/templates.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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::<GoldilocksField>::from(INV_SHIFT_32);
let shift = FieldElement::<GoldilocksField>::from(SHIFT_32);
assert_eq!(inv * shift, FieldElement::one());
}
}
78 changes: 0 additions & 78 deletions prover/src/tables/decode.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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)
);
}
}
59 changes: 0 additions & 59 deletions prover/src/tables/keccak_rnd.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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}"
);
}
}
}
}
}
65 changes: 0 additions & 65 deletions prover/src/tables/load.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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());
}
}
Loading
Loading