Support for sproll-evm proving (WIP)

ceno_emul/src/platform.rs

@@ -22,20 +22,14 @@ pub struct Platform {
 
 impl Display for Platform {
     fn fmt(&self, f: &mut Formatter) -> fmt::Result {
-        let prog_data: Option<Range<Addr>> = match (self.prog_data.first(), self.prog_data.last()) {
-            (Some(first), Some(last)) => Some(*first..*last),
-            _ => None,
+        let prog_data = match (self.prog_data.first(), self.prog_data.last()) {
+            (Some(first), Some(last)) => format!("{:#x?}", *first..*last),
+            _ => "-".to_string(),
         };
         write!(
             f,
-            "Platform {{ rom: {:?}, prog_data: {:?}, stack: {:?}, heap: {:?}, public_io: {:?}, hints: {:?}, unsafe_ecall_nop: {} }}",
-            self.rom,
-            prog_data,
-            self.stack,
-            self.heap,
-            self.public_io,
-            self.hints,
-            self.unsafe_ecall_nop
+            "Platform {{ rom: {:#x?}, prog_data: {prog_data}, stack: {:#x?}, heap: {:x?}, public_io: {:#x?}, hints: {:#x?}, unsafe_ecall_nop: {} }}",
+            self.rom, self.stack, self.heap, self.public_io, self.hints, self.unsafe_ecall_nop
         )
     }
 }

ceno_zkvm/src/bin/e2e.rs

@@ -115,7 +115,7 @@ fn main() {
     );
     tracing::info!("Running on platform {:?} {}", args.platform, platform);
     tracing::info!(
-        "Stack: {} bytes. Heap: {} bytes.",
+        "Stack: {:#x?} bytes. Heap: {:#x?} bytes.",
         args.stack_size,
         args.heap_size
     );

ceno_zkvm/src/e2e.rs

@@ -45,6 +45,7 @@ pub struct EmulationResult {
     pi: PublicValues<u32>,
 }
 
+// TODO(Matthias): handle hints properly.
 fn emulate_program(
     program: Arc<Program>,
     max_steps: usize,
@@ -574,8 +575,18 @@ fn debug_memory_ranges(vm: &VMState, mem_final: &[MemFinalRecord]) {
         format_segments(vm.platform(), handled_addrs.iter().copied())
     );
 
-    for addr in &accessed_addrs {
-        assert!(handled_addrs.contains(addr), "unhandled addr: {:?}", addr);
+    let unhandled: BTreeSet<_> = accessed_addrs
+        .iter()
+        .filter(|addr| !handled_addrs.contains(addr))
+        .collect();
+
+    // TODO(Matthias): this should be an assert, but it's currently broken, because our caller doesn't handle hints.
+    if !unhandled.is_empty() {
+        tracing::warn!(
+            "unhandled addr: {:?} to {:?}",
+            unhandled.first(),
+            unhandled.last()
+        );
     }
 }
 

ceno_zkvm/src/scheme/constants.rs

@@ -5,4 +5,5 @@ pub(crate) const SEL_DEGREE: usize = 2;
 pub const NUM_FANIN: usize = 2;
 pub const NUM_FANIN_LOGUP: usize = 2;
 
-pub const MAX_NUM_VARIABLES: usize = 24;
+// TODO(Matthias): what are the trade-offs for this value?
+pub const MAX_NUM_VARIABLES: usize = 27;