remove POSEIDON_16_NULL_HASH_PTR from public input (move it to witness memory)

Author: TomWambsgans

.gitignore

@@ -1,5 +1,4 @@
 /target
 .vscode
 /docs/benchmark_graphs/.venv
-minimal_zkVM.synctex.gz
-.claude
+minimal_zkVM.synctex.gz

crates/lean_compiler/snark_lib.py

@@ -70,11 +70,10 @@ def pop(self):
 ZERO_VEC_PTR = 0
 SAMPLING_DOMAIN_SEPARATOR_PTR = 16
 ONE_EF_PTR = 24
-POSEIDON_16_NULL_HASH_PTR = 29
-REPEATED_ONES_PTR = 37
+REPEATED_ONES_PTR = 29
 NUM_REPEATED_ONES_IN_RESERVED_MEMORY = 16
-EQ_MLE_COEFFS_PTR = 53
-NONRESERVED_PROGRAM_INPUT_START = 60
+EQ_MLE_COEFFS_PTR = 45
+NONRESERVED_PROGRAM_INPUT_START = 50
 
 
 def poseidon16(left, right, output, mode):

crates/lean_compiler/src/parser/parsers/literal.rs

@@ -1,7 +1,7 @@
 use backend::*;
 use lean_vm::{
     EQ_MLE_COEFFS_PTR, NONRESERVED_PROGRAM_INPUT_START, NUM_REPEATED_ONES_IN_RESERVED_MEMORY, ONE_EF_PTR,
-    POSEIDON_16_NULL_HASH_PTR, REPEATED_ONES_PTR, SAMPLING_DOMAIN_SEPARATOR_PTR, ZERO_VEC_PTR,
+    REPEATED_ONES_PTR, SAMPLING_DOMAIN_SEPARATOR_PTR, ZERO_VEC_PTR,
 };
 
 use super::expression::ExpressionParser;
@@ -135,7 +135,6 @@ impl VarOrConstantParser {
                 NONRESERVED_PROGRAM_INPUT_START,
             ))),
             "ZERO_VEC_PTR" => Ok(SimpleExpr::Constant(ConstExpression::from(ZERO_VEC_PTR))),
-            "POSEIDON_16_NULL_HASH_PTR" => Ok(SimpleExpr::Constant(ConstExpression::from(POSEIDON_16_NULL_HASH_PTR))),
             "ONE_EF_PTR" => Ok(SimpleExpr::Constant(ConstExpression::from(ONE_EF_PTR))),
             "REPEATED_ONES_PTR" => Ok(SimpleExpr::Constant(ConstExpression::from(REPEATED_ONES_PTR))),
             "NUM_REPEATED_ONES_IN_RESERVED_MEMORY" => Ok(SimpleExpr::Constant(ConstExpression::from(

crates/lean_prover/src/lib.rs

@@ -25,7 +25,7 @@ pub const WHIR_SUBSEQUENT_FOLDING_FACTOR: usize = 5;
 pub const RS_DOMAIN_INITIAL_REDUCTION_FACTOR: usize = 5;
 
 pub const SNARK_DOMAIN_SEP: [F; 8] = F::new_array([
-    459434519, 297494976, 1722838545, 1130849508, 622859451, 1840279103, 16871075, 1399912153,
+    130704175, 1303721200, 493664240, 1035493700, 2063844858, 1410214009, 1938905908, 1696767928,
 ]);
 
 pub fn default_whir_config(starting_log_inv_rate: usize) -> WhirConfigBuilder {

crates/lean_prover/src/trace_gen.rs

@@ -1,7 +1,7 @@
 use backend::*;
 use lean_vm::*;
 use std::{array, collections::BTreeMap, iter::repeat_n};
-use utils::{ToUsize, transposed_par_iter_mut};
+use utils::{ToUsize, get_poseidon_16_of_zero, transposed_par_iter_mut};
 
 #[derive(Debug)]
 pub struct ExecutionTrace {
@@ -92,8 +92,13 @@ pub fn get_execution_trace(bytecode: &Bytecode, execution_result: ExecutionResul
         });
 
     let mut memory_padded = memory.0.par_iter().map(|&v| v.unwrap_or(F::ZERO)).collect::<Vec<F>>();
+
+    // Write poseidon(0) at the end of used memory for poseidon table padding rows
+    let null_poseidon_16_hash_ptr = memory_padded.len();
+    memory_padded.extend_from_slice(get_poseidon_16_of_zero());
+
     // IMPORTANT: memory size should always be >= number of VM cycles
-    let padded_memory_len = (memory.0.len().max(n_cycles).max(1 << MIN_LOG_N_ROWS_PER_TABLE)).next_power_of_two();
+    let padded_memory_len = (memory_padded.len().max(n_cycles).max(1 << MIN_LOG_N_ROWS_PER_TABLE)).next_power_of_two();
     memory_padded.resize(padded_memory_len, F::ZERO);
 
     let ExecutionResult { mut traces, .. } = execution_result;
@@ -113,7 +118,7 @@ pub fn get_execution_trace(bytecode: &Bytecode, execution_result: ExecutionResul
         },
     );
     for table in traces.keys().copied().collect::<Vec<_>>() {
-        pad_table(&table, &mut traces);
+        pad_table(&table, &mut traces, null_poseidon_16_hash_ptr);
     }
 
     ExecutionTrace {
@@ -124,7 +129,7 @@ pub fn get_execution_trace(bytecode: &Bytecode, execution_result: ExecutionResul
     }
 }
 
-fn pad_table(table: &Table, traces: &mut BTreeMap<Table, TableTrace>) {
+fn pad_table(table: &Table, traces: &mut BTreeMap<Table, TableTrace>, null_hash_ptr: usize) {
     let trace = traces.get_mut(table).unwrap();
     let h = trace.base[0].len();
     trace
@@ -136,7 +141,11 @@ fn pad_table(table: &Table, traces: &mut BTreeMap<Table, TableTrace>) {
     trace.non_padded_n_rows = h;
     trace.log_n_rows = log2_ceil_usize(h + 1).max(MIN_LOG_N_ROWS_PER_TABLE);
     let padding_len = (1 << trace.log_n_rows) - h;
-    let padding_row = table.padding_row();
+    let padding_row = if *table == Table::poseidon16() {
+        default_poseidon_row(null_hash_ptr)
+    } else {
+        table.padding_row()
+    };
     trace.base.par_iter_mut().enumerate().for_each(|(i, col)| {
         col.extend(repeat_n(padding_row[i], padding_len));
     });

crates/lean_vm/src/core/constants.rs

@@ -40,10 +40,10 @@ pub const ENDING_PC: usize = 0;
 ///
 /// [public_data] = [reserved_area] [program_input]
 ///
-/// reserved_area: reserved for special constants (size = 48 field elements)
+/// reserved_area: reserved for special constants (size = 40 field elements)
 /// program_input: the input of the program we want to prove
 ///
-/// [reserved_area] = [00000000] [00000000] [10000000] [10000] [poseidon_16(0) (8 FE)] [111..111 (16 FE)] [2 -1 -1 1]
+/// [reserved_area] = [00000000] [00000000] [10000000] [10000] [111..111 (16 FE)] [2 -1 -1 1]
 ///
 /// pointing to 16 zeros
 pub const ZERO_VEC_PTR: usize = 0;
@@ -54,12 +54,9 @@ pub const SAMPLING_DOMAIN_SEPARATOR_PTR: usize = ZERO_VEC_PTR + 2 * DIGEST_LEN;
 /// pointing to [10000] (the multiplicative identity of EF, as DIMENSION base field elements)
 pub const ONE_EF_PTR: usize = SAMPLING_DOMAIN_SEPARATOR_PTR + DIGEST_LEN;
 
-/// pointing to the 8 elements of poseidon_16(0)
-pub const POSEIDON_16_NULL_HASH_PTR: usize = ONE_EF_PTR + DIMENSION;
-
 /// POINTING TO 111..111 (`NUM_REPEATED_ONES_IN_RESERVED_MEMORY` times)
 pub const NUM_REPEATED_ONES_IN_RESERVED_MEMORY: usize = 16;
-pub const REPEATED_ONES_PTR: usize = POSEIDON_16_NULL_HASH_PTR + DIGEST_LEN;
+pub const REPEATED_ONES_PTR: usize = ONE_EF_PTR + DIMENSION;
 
 /// [2, -1, -1, 1] is useful to compute (xy + (1-x)(1-y)) = 2xy - x - y + 1 = dot_product([xy, x, y, 1], [2, -1, -1, 1])
 pub const EQ_MLE_COEFFS_LEN: usize = 4;

crates/lean_vm/src/execution/runner.rs

@@ -1,6 +1,6 @@
 //! VM execution runner
 
-use crate::core::{DIGEST_LEN, DIMENSION, F, NONRESERVED_PROGRAM_INPUT_START, POSEIDON_16_NULL_HASH_PTR, ZERO_VEC_PTR};
+use crate::core::{DIGEST_LEN, DIMENSION, F, NONRESERVED_PROGRAM_INPUT_START, ZERO_VEC_PTR};
 use crate::diagnostics::{ExecutionMetadata, ExecutionResult, MemoryProfile, RunnerError};
 use crate::execution::{ExecutionHistory, Memory};
 use crate::isa::Bytecode;
@@ -12,7 +12,7 @@ use crate::{
 };
 use backend::*;
 use std::collections::{BTreeMap, BTreeSet};
-use utils::{ToUsize, get_poseidon_16_of_zero};
+use utils::ToUsize;
 use xmss::Poseidon16History;
 
 #[derive(Debug)]
@@ -60,7 +60,6 @@ pub fn build_public_memory(non_reserved_public_input: &[F]) -> Vec<F> {
     // ONE in the extension field = [1, 0, 0, 0, 0]
     public_memory[ONE_EF_PTR] = F::ONE;
 
-    public_memory[POSEIDON_16_NULL_HASH_PTR..][..DIGEST_LEN].copy_from_slice(get_poseidon_16_of_zero());
     public_memory[REPEATED_ONES_PTR..][..NUM_REPEATED_ONES_IN_RESERVED_MEMORY].fill(F::ONE);
 
     public_memory[EQ_MLE_COEFFS_PTR..][..EQ_MLE_COEFFS_LEN].copy_from_slice(&[F::TWO, F::NEG_ONE, F::NEG_ONE, F::ONE]);

crates/lean_vm/src/tables/poseidon_16/mod.rs

@@ -1,11 +1,11 @@
 use std::any::TypeId;
 
-use crate::{tables::poseidon_16::trace_gen::default_poseidon_row, *};
+use crate::*;
 use backend::*;
 use utils::{ToUsize, poseidon16_compress};
 
 mod trace_gen;
-pub use trace_gen::fill_trace_poseidon_16;
+pub use trace_gen::{default_poseidon_row, fill_trace_poseidon_16};
 
 pub(super) const WIDTH: usize = 16;
 const HALF_INITIAL_FULL_ROUNDS: usize = KOALABEAR_RC16_EXTERNAL_INITIAL.len() / 2;
@@ -65,7 +65,8 @@ impl<const BUS: bool> TableT for Poseidon16Precompile<BUS> {
     }
 
     fn padding_row(&self) -> Vec<F> {
-        default_poseidon_row()
+        // depends on null_poseidon_16_hash_ptr (cf lean_prover/trace_gen.rs)
+        unreachable!()
     }
 
     #[inline(always)]

crates/lean_vm/src/tables/poseidon_16/trace_gen.rs

@@ -1,7 +1,7 @@
 use tracing::instrument;
 
 use crate::{
-    F, POSEIDON_16_NULL_HASH_PTR, ZERO_VEC_PTR,
+    F, ZERO_VEC_PTR,
     tables::{Poseidon2Cols, WIDTH, num_cols_poseidon_16},
 };
 use backend::*;
@@ -41,7 +41,7 @@ pub fn fill_trace_poseidon_16(trace: &mut [Vec<F>]) {
     }
 }
 
-pub fn default_poseidon_row() -> Vec<F> {
+pub fn default_poseidon_row(null_hash_ptr: usize) -> Vec<F> {
     let mut row = vec![F::ZERO; num_cols_poseidon_16()];
     let ptrs: [*mut F; num_cols_poseidon_16()] = std::array::from_fn(|i| unsafe { row.as_mut_ptr().add(i) });
 
@@ -50,7 +50,7 @@ pub fn default_poseidon_row() -> Vec<F> {
     *perm.flag = F::ZERO;
     *perm.index_a = F::from_usize(ZERO_VEC_PTR);
     *perm.index_b = F::from_usize(ZERO_VEC_PTR);
-    *perm.index_res = F::from_usize(POSEIDON_16_NULL_HASH_PTR);
+    *perm.index_res = F::from_usize(null_hash_ptr);
 
     generate_trace_rows_for_perm(perm);
     row

src/prove_poseidons.rs

@@ -2,8 +2,7 @@ use air::{check_air_validity, prove_air, verify_air};
 use backend::*;
 use lean_vm::{
     EF, ExtraDataForBuses, F, POSEIDON_16_COL_A, POSEIDON_16_COL_B, POSEIDON_16_COL_FLAG, POSEIDON_16_COL_INPUT_START,
-    POSEIDON_16_COL_RES, POSEIDON_16_NULL_HASH_PTR, Poseidon16Precompile, ZERO_VEC_PTR, fill_trace_poseidon_16,
-    num_cols_poseidon_16,
+    POSEIDON_16_COL_RES, Poseidon16Precompile, ZERO_VEC_PTR, fill_trace_poseidon_16, num_cols_poseidon_16,
 };
 use rand::{Rng, SeedableRng, rngs::StdRng};
 use utils::{
@@ -29,7 +28,7 @@ pub fn benchmark_prove_poseidon_16(log_n_rows: usize, tracing: bool) {
         *t = (0..n_rows).map(|_| rng.random()).collect();
     }
     trace[POSEIDON_16_COL_FLAG] = (0..n_rows).map(|_| F::ONE).collect();
-    trace[POSEIDON_16_COL_RES] = (0..n_rows).map(|_| F::from_usize(POSEIDON_16_NULL_HASH_PTR)).collect();
+    trace[POSEIDON_16_COL_RES] = (0..n_rows).map(|_| F::ZERO).collect(); // useless
     trace[POSEIDON_16_COL_A] = (0..n_rows).map(|_| F::from_usize(ZERO_VEC_PTR)).collect();
     trace[POSEIDON_16_COL_B] = (0..n_rows).map(|_| F::from_usize(ZERO_VEC_PTR)).collect();
     fill_trace_poseidon_16(&mut trace);