From d9cc59b2d27095a7880b4e30332dc954da704ecf Mon Sep 17 00:00:00 2001
From: Matthias Goergens <matthias.goergens@gmail.com>
Date: Mon, 9 Dec 2024 19:48:23 +0800
Subject: [PATCH] Check: is `DynVolatileRamTable::max_len` broken?

---
 ceno_zkvm/src/tables/ram.rs             | 9 +++++++++
 ceno_zkvm/src/tables/ram/ram_circuit.rs | 7 ++++++-
 2 files changed, 15 insertions(+), 1 deletion(-)

diff --git a/ceno_zkvm/src/tables/ram.rs b/ceno_zkvm/src/tables/ram.rs
index 2c45294e4..ff0c23e1f 100644
--- a/ceno_zkvm/src/tables/ram.rs
+++ b/ceno_zkvm/src/tables/ram.rs
@@ -31,6 +31,15 @@ impl DynVolatileRamTable for DynMemTable {
     }
 }
 
+#[test]
+fn test_dyn_mem_table() {
+    let mut params = ProgramParams::default();
+    params.platform.ram.start = 0;
+    params.platform.ram.end = 100;
+    let max_len_bytes = 4 * DynMemTable::max_len(&params);
+    assert_eq!(max_len_bytes, 128);
+}
+
 pub type DynMemCircuit<E> = DynVolatileRamCircuit<E, DynMemTable>;
 
 #[derive(Clone)]
diff --git a/ceno_zkvm/src/tables/ram/ram_circuit.rs b/ceno_zkvm/src/tables/ram/ram_circuit.rs
index 234ff7799..99269c1ed 100644
--- a/ceno_zkvm/src/tables/ram/ram_circuit.rs
+++ b/ceno_zkvm/src/tables/ram/ram_circuit.rs
@@ -163,7 +163,12 @@ pub trait DynVolatileRamTable {
     fn max_len(params: &ProgramParams) -> usize {
         let max_size =
             (Self::end_addr(params) - Self::offset_addr(params)).div_ceil(WORD_SIZE as u32) as Addr;
-        1 << (u32::BITS - 1 - max_size.leading_zeros()) // prev_power_of_2
+        let max_len = 1 << (u32::BITS - 1 - max_size.leading_zeros()); // prev_power_of_2
+        assert!(
+            max_size as usize <= max_len,
+            "Did not round up {max_size} correctly, got {max_len}, which is smaller."
+        );
+        max_len
     }
 
     fn addr(params: &ProgramParams, entry_index: usize) -> Addr {