some explainations about memory layout

Author: TomWambsgans

crates/lean_compiler/src/c_compile_final.rs

@@ -1,4 +1,4 @@
-use crate::{F, PUBLIC_INPUT_START, ZERO_VEC_PTR, ir::*, lang::*};
+use crate::{F, NONRESERVED_PROGRAM_INPUT_START, ZERO_VEC_PTR, ir::*, lang::*};
 use lean_vm::*;
 use p3_field::{PrimeCharacteristicRing, PrimeField32};
 use std::collections::BTreeMap;
@@ -395,7 +395,7 @@ fn count_real_instructions(instrs: &[IntermediateInstruction]) -> usize {
 fn eval_constant_value(constant: &ConstantValue, compiler: &Compiler) -> usize {
     match constant {
         ConstantValue::Scalar(scalar) => *scalar,
-        ConstantValue::PublicInputStart => PUBLIC_INPUT_START,
+        ConstantValue::PublicInputStart => NONRESERVED_PROGRAM_INPUT_START,
         ConstantValue::PointerToZeroVector => ZERO_VEC_PTR,
         ConstantValue::PointerToOneVector => ONE_VEC_PTR,
         ConstantValue::FunctionSize { function_name } => {

crates/lean_prover/tests/test_zkvm.rs

@@ -83,15 +83,15 @@ fn test_zk_vm_helper(program_str: &str) {
     const SECOND_POINT: usize = 2;
     const SECOND_N_VARS: usize = 7;
 
-    let mut public_input = (0..(1 << 13) - PUBLIC_INPUT_START)
+    let mut public_input = (0..(1 << 13) - NONRESERVED_PROGRAM_INPUT_START)
         .map(F::from_usize)
         .collect::<Vec<_>>();
 
     public_input[SECOND_POINT * (SECOND_N_VARS * DIMENSION).next_power_of_two()
         + SECOND_N_VARS * DIMENSION
-        - PUBLIC_INPUT_START
+        - NONRESERVED_PROGRAM_INPUT_START
         ..(SECOND_POINT + 1) * (SECOND_N_VARS * DIMENSION).next_power_of_two()
-            - PUBLIC_INPUT_START]
+            - NONRESERVED_PROGRAM_INPUT_START]
         .iter_mut()
         .for_each(|x| *x = F::ZERO);
 

crates/lean_vm/src/core/constants.rs

@@ -7,6 +7,23 @@ pub const LOG_VECTOR_LEN: usize = 3;
 /// Vector length (2^LOG_VECTOR_LEN)
 pub const VECTOR_LEN: usize = 1 << LOG_VECTOR_LEN;
 
+/// Maximum memory size for VM runner
+pub const MAX_RUNNER_MEMORY_SIZE: usize = 1 << 24;
+
+/// Memory layout:
+///
+/// [memory] = [public_data] [private_data]
+///       
+/// public_data: shared between prover and verifier
+/// private_data: witness, committed by the prover
+///
+/// [public_data] = [reserved_area] [program_input]
+///
+/// reserved_area: reserved for special constants (size = 48 field elements)
+/// program_input: the input of the program we want to prove
+///
+/// [reserved_area] = [00000000] [00000000] [10000000] [poseidon_16(0) (16 field elements)] [poseidon_24(0) (8 last field elements)]
+
 /// Convention: vectorized pointer of size 2, pointing to 16 zeros
 pub const ZERO_VEC_PTR: usize = 0;
 
@@ -19,8 +36,5 @@ pub const POSEIDON_16_NULL_HASH_PTR: usize = 3;
 /// Convention: vectorized pointer of size 1, = the last 8 elements of poseidon_24(0)
 pub const POSEIDON_24_NULL_HASH_PTR: usize = 5;
 
-/// Normal pointer to start of public input
-pub const PUBLIC_INPUT_START: usize = 6 * 8;
-
-/// Maximum memory size for VM runner
-pub const MAX_RUNNER_MEMORY_SIZE: usize = 1 << 24;
+/// Normal pointer to start of program input
+pub const NONRESERVED_PROGRAM_INPUT_START: usize = 6 * 8;

crates/lean_vm/src/execution/runner.rs

@@ -1,8 +1,8 @@
 //! VM execution runner
 
 use crate::core::{
-    DIMENSION, F, ONE_VEC_PTR, POSEIDON_16_NULL_HASH_PTR, POSEIDON_24_NULL_HASH_PTR,
-    PUBLIC_INPUT_START, VECTOR_LEN, ZERO_VEC_PTR,
+    DIMENSION, F, NONRESERVED_PROGRAM_INPUT_START, ONE_VEC_PTR, POSEIDON_16_NULL_HASH_PTR,
+    POSEIDON_24_NULL_HASH_PTR, VECTOR_LEN, ZERO_VEC_PTR,
 };
 use crate::diagnostics::{ExecutionResult, RunnerError};
 use crate::execution::{ExecutionHistory, Memory};
@@ -23,9 +23,11 @@ const STACK_TRACE_INSTRUCTIONS: usize = 5000;
 /// Build public memory with standard initialization
 pub fn build_public_memory(public_input: &[F]) -> Vec<F> {
     // padded to a power of two
-    let public_memory_len = (PUBLIC_INPUT_START + public_input.len()).next_power_of_two();
+    let public_memory_len =
+        (NONRESERVED_PROGRAM_INPUT_START + public_input.len()).next_power_of_two();
     let mut public_memory = F::zero_vec(public_memory_len);
-    public_memory[PUBLIC_INPUT_START..][..public_input.len()].copy_from_slice(public_input);
+    public_memory[NONRESERVED_PROGRAM_INPUT_START..][..public_input.len()]
+        .copy_from_slice(public_input);
 
     // "zero" vector
     let zero_start = ZERO_VEC_PTR * VECTOR_LEN;
@@ -157,7 +159,8 @@ fn execute_bytecode_helper(
     // set public memory
     let mut memory = Memory::new(build_public_memory(public_input));
 
-    let public_memory_size = (PUBLIC_INPUT_START + public_input.len()).next_power_of_two();
+    let public_memory_size =
+        (NONRESERVED_PROGRAM_INPUT_START + public_input.len()).next_power_of_two();
     let mut fp = public_memory_size;
 
     for (i, value) in private_input.iter().enumerate() {
@@ -320,7 +323,8 @@ fn execute_bytecode_helper(
     summary.push_str(&format!("MEMORY: {}\n", pretty_integer(memory.0.len())));
     summary.push('\n');
 
-    let runtime_memory_size = memory.0.len() - (PUBLIC_INPUT_START + public_input.len());
+    let runtime_memory_size =
+        memory.0.len() - (NONRESERVED_PROGRAM_INPUT_START + public_input.len());
     summary.push_str(&format!(
         "Bytecode size: {}\n",
         pretty_integer(bytecode.instructions.len())
@@ -342,7 +346,7 @@ fn execute_bytecode_helper(
     let used_memory_cells = memory
         .0
         .iter()
-        .skip(PUBLIC_INPUT_START + public_input.len())
+        .skip(NONRESERVED_PROGRAM_INPUT_START + public_input.len())
         .filter(|&&x| x.is_some())
         .count();
     summary.push_str(&format!(

crates/lean_vm/tests/test_lean_vm.rs

@@ -27,7 +27,7 @@ const MLE_N_VARS: usize = 1;
 
 // Ensure public input covers the highest index used (dot product arg1 slice).
 const MAX_MEMORY_INDEX: usize = DOT_ARG1_PTR + DOT_PRODUCT_LEN * DIMENSION - 1;
-const PUBLIC_INPUT_LEN: usize = MAX_MEMORY_INDEX - PUBLIC_INPUT_START + 1;
+const PUBLIC_INPUT_LEN: usize = MAX_MEMORY_INDEX - NONRESERVED_PROGRAM_INPUT_START + 1;
 
 const POSEIDON16_ARG_A_VALUES: [u64; VECTOR_LEN] = [1, 2, 3, 4, 5, 6, 7, 8];
 const POSEIDON16_ARG_B_VALUES: [u64; VECTOR_LEN] = [101, 102, 103, 104, 105, 106, 107, 108];
@@ -47,8 +47,8 @@ fn f(value: u64) -> F {
 }
 
 fn set_public_input_cell(public_input: &mut [F], memory_index: usize, value: F) {
-    assert!(memory_index >= PUBLIC_INPUT_START);
-    let idx = memory_index - PUBLIC_INPUT_START;
+    assert!(memory_index >= NONRESERVED_PROGRAM_INPUT_START);
+    let idx = memory_index - NONRESERVED_PROGRAM_INPUT_START;
     assert!(idx < public_input.len());
     public_input[idx] = value;
 }

crates/rec_aggregation/src/recursion.rs

@@ -127,7 +127,7 @@ pub fn run_whir_recursion_benchmark() {
 
     // to align the first merkle leaves (in base field) (required to appropriately call the precompile multilinear_eval)
     let mut proof_data_padding = (1 << first_folding_factor)
-        - ((PUBLIC_INPUT_START
+        - ((NONRESERVED_PROGRAM_INPUT_START
             + public_input.len()
             + {
                 // sumcheck polys

crates/rec_aggregation/src/xmss_aggregate.rs

@@ -224,7 +224,9 @@ pub fn run_xmss_benchmark(n_xmss: usize) {
     }
     public_input.insert(
         0,
-        F::from_usize((public_input.len() + 8 + PUBLIC_INPUT_START).next_power_of_two()),
+        F::from_usize(
+            (public_input.len() + 8 + NONRESERVED_PROGRAM_INPUT_START).next_power_of_two(),
+        ),
     );
     public_input.splice(1..1, F::zero_vec(7));