#1084 follow up: verifier check on dynamic init table

ceno_emul/src/platform.rs

@@ -1,15 +1,15 @@
+use crate::addr::{Addr, RegIdx};
 use core::fmt::{self, Formatter};
 use once_cell::sync::Lazy;
+use serde::{Deserialize, Serialize};
 use std::{collections::BTreeSet, fmt::Display, ops::Range, sync::Arc};
 
-use crate::addr::{Addr, RegIdx};
-
 /// The Platform struct holds the parameters of the VM.
 /// It defines:
 /// - the layout of virtual memory,
 /// - special addresses, such as the initial PC,
 /// - codes of environment calls.
-#[derive(Clone, Debug)]
+#[derive(Clone, Debug, Serialize, Deserialize)]
 pub struct Platform {
     pub rom: Range<Addr>,
     pub prog_data: Arc<BTreeSet<Addr>>,
@@ -55,51 +55,43 @@ impl Display for Platform {
     }
 }
 
-/// alined with [`memory.x`]
-// ┌───────────────────────────── 0x4000_0000 (end of _sheap, or heap)
+/// aligned with [`memory.x`]
+// ┌───────────────────────────── 0x4000_0000 (stack top)
 // │
-// │   HEAP (128 MB, grows upward)
-// │   0x3800_0000 .. 0x4000_0000
+// │   STACK (256 MB window, grows downward)
+// │   0x3000_0000 .. 0x4000_0000
 // │
-// ├───────────────────────────── 0x3800_0000 (_sheap, align 0x800_0000)
-// │   RAM (128 MB)
-// │   0x3000_0000 .. 0x3800_0000
-// ├───────────────────────────── 0x3000_0000 (RAM base / hints end)
+// ├───────────────────────────── 0x3000_0000 (stack base / hints end)
 // │
 // │   HINTS (128 MB)
 // │   0x2800_0000 .. 0x3000_0000
 // │
-// │───────────────────────────── 0x2800_0000 (hint base / gap end)
+// │───────────────────────────── 0x2800_0000 (hint start / gap end)
 // │
 // │   [Reserved gap: 128 MB for debug I/O]
 // │   0x2000_0000 .. 0x2800_0000
-// │───────────────────────────── 0x2000_0000 (gap / stack end)
+// │───────────────────────────── 0x2000_0000 (gap / heap end)
 // │
-// │   STACK (≈128 MB, grows downward)
+// │   HEAP (128 MB, grows upward)
 // │   0x1800_0000 .. 0x2000_0000
 // │
-// ├───────────────────────────── 0x1800_0000 (stack base)
+// ├───────────────────────────── 0x1800_0000 (heap midpoint)
 // │
-// │   STACK (stack-only memory window, includes reserved low-address area
-// │   previously used for PUBLIC I/O)
+// │   RAM / DATA / BSS / HEAP
 // │   0x1000_0000 .. 0x2000_0000
 // │
-// ├───────────────────────────── 0x1000_0000 (stack base / rom end)
+// ├───────────────────────────── 0x1000_0000 (ram base / rom end)
 // │
 // │   ROM / TEXT / RODATA (128 MB)
 // │   0x0800_0000 .. 0x1000_0000
 // │
-// └───────────────────────────── 0x8000_0000 (rom base)
+// └───────────────────────────── 0x0800_0000 (rom base)
 pub static CENO_PLATFORM: Lazy<Platform> = Lazy::new(|| Platform {
     rom: 0x0800_0000..0x1000_0000,   // 128 MB
-    stack: 0x1000_0000..0x2000_4000, // stack grows downward, 0x4000 reserved for debug io.
-    // we make hints start from 0x2800_0000 thus reserve a 128MB gap for debug io
-    // at the end of stack
+    stack: 0x3000_0000..0x4000_4000, // stack grows downward, 0x4000 reserved for debug io.
     hints: 0x2800_0000..0x3000_0000, // 128 MB
-    // heap grows upward, reserved 128 MB for it
-    // the beginning of heap address got bss/sbss data
-    // and the real heap start from 0x3800_0000
-    heap: 0x3000_0000..0x4000_0000,
+    // heap grows upward in the low RAM window; .data/.bss live at its beginning.
+    heap: 0x1000_0000..0x2000_0000,
     unsafe_ecall_nop: false,
     prog_data: Arc::new(BTreeSet::new()),
     is_debug: false,

ceno_emul/src/tracer.rs

@@ -194,7 +194,7 @@ impl LatestAccesses {
         Self {
             store: DenseAddrSpace::new(
                 WordAddr::from(0u32),
-                ByteAddr::from(platform.heap.end).waddr(),
+                ByteAddr::from(platform.stack.end).waddr(),
             ),
             len: 0,
             #[cfg(any(test, debug_assertions))]

ceno_emul/src/vm_state.rs

@@ -66,7 +66,14 @@ impl<T: Tracer> VMState<T> {
             program: program.clone(),
             memory: DenseAddrSpace::new(
                 ByteAddr::from(platform.rom.start).waddr(),
-                ByteAddr::from(platform.heap.end).waddr(),
+                ByteAddr::from(
+                    platform
+                        .stack
+                        .end
+                        .max(platform.heap.end)
+                        .max(platform.hints.end),
+                )
+                .waddr(),
             ),
             registers: [0; VM_REG_COUNT],
             halt_state: None,

ceno_recursion/src/aggregation/mod.rs

@@ -2,8 +2,12 @@ use crate::zkvm_verifier::{
     binding::{E, F, ZKVMProofInput, ZKVMProofInputVariable},
     verifier::verify_zkvm_proof,
 };
+use ceno_emul::WORD_SIZE;
 use ceno_zkvm::{
-    instructions::riscv::constants::{END_PC_IDX, EXIT_CODE_IDX, INIT_PC_IDX},
+    instructions::riscv::constants::{
+        END_PC_IDX, EXIT_CODE_IDX, HEAP_LENGTH_IDX, HEAP_START_ADDR_IDX, HINT_LENGTH_IDX,
+        HINT_START_ADDR_IDX, INIT_PC_IDX,
+    },
     scheme::ZKVMProof,
     structs::ZKVMVerifyingKey,
 };
@@ -56,7 +60,7 @@ use openvm_stark_sdk::{
     openvm_stark_backend::keygen::types::MultiStarkVerifyingKey,
     p3_bn254_fr::Bn254Fr,
 };
-use p3::field::FieldAlgebra;
+use p3::field::{FieldAlgebra, PrimeField32};
 use serde::{Deserialize, Serialize};
 use std::{borrow::Borrow, sync::Arc, time::Instant};
 pub type RecPcs = Basefold<E, BasefoldRSParams>;
@@ -387,6 +391,49 @@ pub struct CenoLeafVmVerifierConfig {
 }
 
 impl CenoLeafVmVerifierConfig {
+    fn assert_felt_lt<C: Config<F = F>>(
+        builder: &mut Builder<C>,
+        lhs: Felt<C::F>,
+        rhs: Felt<C::F>,
+        max_bits: u32,
+    ) {
+        Self::check_felt_lt(builder, lhs, rhs, max_bits, true)
+    }
+
+    fn assert_felt_ge<C: Config<F = F>>(
+        builder: &mut Builder<C>,
+        lhs: Felt<C::F>,
+        rhs: Felt<C::F>,
+        max_bits: u32,
+    ) {
+        Self::check_felt_lt(builder, lhs, rhs, max_bits, false)
+    }
+
+    fn assert_felt_range<C: Config<F = F>>(
+        builder: &mut Builder<C>,
+        value: Felt<C::F>,
+        start: Felt<C::F>,
+        end: Felt<C::F>,
+        max_bits: u32,
+    ) {
+        Self::assert_felt_ge(builder, value, start, max_bits);
+        Self::assert_felt_lt(builder, value, end, max_bits);
+    }
+
+    fn check_felt_lt<C: Config<F = F>>(
+        builder: &mut Builder<C>,
+        lhs: Felt<C::F>,
+        rhs: Felt<C::F>,
+        max_bits: u32,
+        is_lt: bool,
+    ) {
+        let range: Felt<_> = builder.constant(C::F::from_canonical_u64(1u64 << max_bits));
+        let zero = builder.constant(F::ZERO);
+        let diff = builder.eval(lhs - rhs + if is_lt { range } else { zero });
+        let diff = builder.cast_felt_to_var(diff);
+        builder.range_check_var(diff, max_bits as usize);
+    }
+
     pub fn build_program(&self) -> Program<F> {
         let mut builder = Builder::<C>::default();
 
@@ -436,6 +483,97 @@ impl CenoLeafVmVerifierConfig {
                 builder.assign(&stark_pvs.public_values_commit[i], F::ZERO);
             }
 
+            assert!(
+                2 * self.vk.mem_state_verifier.heap.end < F::ORDER_U32,
+                "2 * {:x} >= {}",
+                self.vk.mem_state_verifier.heap.end,
+                F::ORDER_U32
+            );
+            assert!(
+                2 * self.vk.mem_state_verifier.hints.end < F::ORDER_U32,
+                "2 * {:x} >= {}",
+                self.vk.mem_state_verifier.hints.end,
+                F::ORDER_U32
+            );
+            fn bits_needed(x: u32) -> u32 {
+                if x == 0 { 1 } else { 32 - x.leading_zeros() }
+            }
+            let heap_max_bits = bits_needed(
+                self.vk.mem_state_verifier.heap.end - self.vk.mem_state_verifier.heap.start,
+            );
+            let hint_max_bits = bits_needed(
+                self.vk.mem_state_verifier.hints.end - self.vk.mem_state_verifier.hints.start,
+            );
+            let heap_min_start_addr = {
+                let v = builder.eval(Usize::from(self.vk.mem_state_verifier.heap.start as usize));
+                builder.unsafe_cast_var_to_felt(v)
+            };
+            let heap_max_end_addr = {
+                let v = builder.eval(Usize::from(self.vk.mem_state_verifier.heap.end as usize));
+                builder.unsafe_cast_var_to_felt(v)
+            };
+            let heap_max_addr_diff = {
+                let v = builder.eval(Usize::from(
+                    (self.vk.mem_state_verifier.heap.end - self.vk.mem_state_verifier.heap.start)
+                        as usize,
+                ));
+                builder.unsafe_cast_var_to_felt(v)
+            };
+            let hint_min_start_addr = {
+                let v = builder.eval(Usize::from(self.vk.mem_state_verifier.hints.start as usize));
+                builder.unsafe_cast_var_to_felt(v)
+            };
+            let hint_max_end_addr = {
+                let v = builder.eval(Usize::from(self.vk.mem_state_verifier.hints.end as usize));
+                builder.unsafe_cast_var_to_felt(v)
+            };
+            let hint_max_addr_diff = {
+                let v = builder.eval(Usize::from(
+                    (self.vk.mem_state_verifier.hints.end - self.vk.mem_state_verifier.hints.start)
+                        as usize,
+                ));
+                builder.unsafe_cast_var_to_felt(v)
+            };
+
+            let heap_start_addr = builder.get(pv, HEAP_START_ADDR_IDX);
+            let heap_length_words = builder.get(pv, HEAP_LENGTH_IDX);
+            let word_size = builder.constant::<Felt<_>>(F::from_canonical_usize(WORD_SIZE));
+            let heap_length = builder.eval(heap_length_words * word_size);
+            let heap_end_addr = builder.eval(heap_start_addr + heap_length);
+            let hint_start_addr = builder.get(pv, HINT_START_ADDR_IDX);
+            let hint_length_words = builder.get(pv, HINT_LENGTH_IDX);
+            let hint_length = builder.eval(hint_length_words * word_size);
+            let hint_end_addr = builder.eval(hint_start_addr + hint_length);
+
+            Self::assert_felt_range(
+                &mut builder,
+                heap_start_addr,
+                heap_min_start_addr,
+                heap_max_end_addr,
+                heap_max_bits,
+            );
+            Self::assert_felt_lt(
+                &mut builder,
+                heap_end_addr,
+                heap_max_end_addr,
+                heap_max_bits,
+            );
+            Self::assert_felt_lt(&mut builder, heap_length, heap_max_addr_diff, heap_max_bits);
+            Self::assert_felt_range(
+                &mut builder,
+                hint_start_addr,
+                hint_min_start_addr,
+                hint_max_end_addr,
+                hint_max_bits,
+            );
+            Self::assert_felt_lt(
+                &mut builder,
+                hint_end_addr,
+                hint_max_end_addr,
+                hint_max_bits,
+            );
+            Self::assert_felt_lt(&mut builder, hint_length, hint_max_addr_diff, hint_max_bits);
+
             // TODO: assign shard_ec_sum to stark_pvs.shard_ec_sum
 
             // builder

ceno_rt/ceno_link.x

@@ -21,11 +21,10 @@ SECTIONS
     *(.rodata .rodata.*);
   } > ROM
 
-
   .stack (NOLOAD) : ALIGN(4)
   {
     *(.stack .stack.*)
-  } > STACK_PUBIO
+  } > STACK
 
   /* Define a section for runtime-populated EEPROM-like HINTS data */
   .hints (NOLOAD) : ALIGN(4)
@@ -55,4 +54,5 @@ SECTIONS
     . = ALIGN(0x8000000);
     _sheap = .;
   } > RAM
+
 }

ceno_rt/memory.x

@@ -1,15 +1,15 @@
 MEMORY
 {
     ROM           (rx) : ORIGIN = 0x08000000, LENGTH = 128M
-    STACK_PUBIO   (rw) : ORIGIN = 0x10000000, LENGTH = 256M  /* Stack region */
+    RAM           (rw) : ORIGIN = 0x10000000, LENGTH = 256M   /* heap/data/bss */
     HINTS         (r)  : ORIGIN = 0x20000000, LENGTH = 256M  /* will shift hint to 0x28000000 with 128M to reserve gap*/
-    RAM           (rw) : ORIGIN = 0x30000000, LENGTH = 256M   /* heap/data/bss */
+    STACK         (rw) : ORIGIN = 0x30000000, LENGTH = 256M  /* stack-only region */
 }
 
 REGION_ALIAS("REGION_TEXT", ROM);
 REGION_ALIAS("REGION_RODATA", ROM);
 
-REGION_ALIAS("REGION_STACK", STACK_PUBIO);
+REGION_ALIAS("REGION_STACK", STACK);
 
 REGION_ALIAS("REGION_HINTS", HINTS);
 REGION_ALIAS("REGION_DATA", RAM);

ceno_rt/src/params.rs

@@ -1,4 +1,4 @@
 pub const WORD_SIZE: usize = 4;
 
 /// address defined in `memory.x` under RAM section.
-pub const INFO_OUT_ADDR: u32 = 0x2000_0000;
+pub const INFO_OUT_ADDR: u32 = 0x4000_0000;

ceno_zkvm/benches/fibonacci.rs

@@ -13,7 +13,10 @@ use criterion::*;
 use ff_ext::BabyBearExt4;
 use gkr_iop::cpu::default_backend_config;
 
-use ceno_zkvm::{e2e::MultiProver, scheme::verifier::ZKVMVerifier};
+use ceno_zkvm::{
+    e2e::MultiProver,
+    scheme::verifier::{RV32imMemStateConfig, ZKVMVerifier},
+};
 use mpcs::BasefoldDefault;
 use transcript::BasicTranscript;
 
@@ -69,7 +72,7 @@ fn fibonacci_prove(c: &mut Criterion) {
 
         println!("e2e proof {}", proof);
         let transcript = BasicTranscript::new(b"riscv");
-        let verifier = ZKVMVerifier::<E, Pcs>::new(vk);
+        let verifier = ZKVMVerifier::<E, Pcs, RV32imMemStateConfig>::new(vk);
         assert!(
             verifier
                 .verify_full_trace_proofs_halt(vec![proof], vec![transcript], false)

ceno_zkvm/benches/keccak.rs

@@ -8,7 +8,10 @@ use ceno_zkvm::{
     scheme::{create_backend, create_prover},
 };
 mod alloc;
-use ceno_zkvm::{e2e::MultiProver, scheme::verifier::ZKVMVerifier};
+use ceno_zkvm::{
+    e2e::MultiProver,
+    scheme::verifier::{RV32imMemStateConfig, ZKVMVerifier},
+};
 use criterion::*;
 use ff_ext::BabyBearExt4;
 use gkr_iop::cpu::default_backend_config;
@@ -66,7 +69,7 @@ fn keccak_prove(c: &mut Criterion) {
 
     println!("e2e proof {}", proof);
     let transcript = BasicTranscript::new(b"riscv");
-    let verifier = ZKVMVerifier::<E, Pcs>::new(vk);
+    let verifier = ZKVMVerifier::<E, Pcs, RV32imMemStateConfig>::new(vk);
     assert!(
         verifier
             .verify_full_trace_proofs_halt(vec![proof], vec![transcript], true)