Skip to content

Commit 3cd65cb

Browse files
committed
add a MAX_MEMORY_SIZE, in order to use Dmitry's trick
1 parent 29d8302 commit 3cd65cb

File tree

3 files changed

+13
-6
lines changed

3 files changed

+13
-6
lines changed

crates/lean_prover/src/verify_execution.rs

Lines changed: 6 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -71,10 +71,13 @@ pub fn verify_execution(
7171
let n_cycles = 1 << log_n_cycles;
7272

7373
let public_memory = build_public_memory(public_input);
74-
let public_memory_len = public_memory.len();
7574

76-
let log_public_memory = log2_strict_usize(public_memory_len);
77-
let log_memory = log2_ceil_usize(public_memory_len + private_memory_len);
75+
if log2_ceil_usize(private_memory_len + private_memory_len) > MAX_MEMORY_SIZE {
76+
return Err(ProofError::InvalidProof);
77+
}
78+
79+
let log_public_memory = log2_strict_usize(public_memory.len());
80+
let log_memory = log2_ceil_usize(public_memory.len() + private_memory_len);
7881
let log_n_p16 = log2_ceil_usize(n_poseidons_16);
7982
let log_n_p24 = log2_ceil_usize(n_poseidons_24);
8083

crates/lean_vm/src/memory.rs

Lines changed: 6 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -5,7 +5,11 @@ use rayon::prelude::*;
55

66
use crate::*;
77

8-
pub(crate) const MAX_MEMORY_SIZE: usize = 1 << 24;
8+
pub const MAX_MEMORY_SIZE: usize = 1 << 29;
9+
10+
// For now, we restrict ourselves to executions where memory usage < 2^24 words.
11+
// But the VM supports theorically a memory of size MAX_MEMORY_SIZE = 2^29.
12+
pub(crate) const MAX_RUNNER_MEMORY_SIZE: usize = 1 << 24;
913

1014
#[derive(Debug, Clone, Default)]
1115
pub struct Memory(pub Vec<Option<F>>);
@@ -29,7 +33,7 @@ impl Memory {
2933

3034
pub fn set(&mut self, index: usize, value: F) -> Result<(), RunnerError> {
3135
if index >= self.0.len() {
32-
if index >= MAX_MEMORY_SIZE {
36+
if index >= MAX_RUNNER_MEMORY_SIZE {
3337
return Err(RunnerError::OutOfMemory);
3438
}
3539
self.0.resize(index + 1, None);

crates/lean_vm/src/runner.rs

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -101,7 +101,7 @@ pub fn execute_bytecode(
101101
bytecode,
102102
public_input,
103103
private_input,
104-
MAX_MEMORY_SIZE / 2,
104+
MAX_RUNNER_MEMORY_SIZE / 2,
105105
false,
106106
&mut std_out,
107107
&mut instruction_history,

0 commit comments

Comments
 (0)