chore: add hint for insuffient K

DelphinusLab · Nov 13, 2023 · 1a6059e · 1a6059e
1 parent cccb83f
commit 1a6059e
Show file tree

Hide file tree

Showing 6 changed files with 83 additions and 51 deletions.
diff --git a/Cargo.lock b/Cargo.lock
diff --git a/Cargo.toml b/Cargo.toml
@@ -7,6 +7,7 @@ anyhow = { version = "1.0.68", features = ["backtrace"] }
 halo2aggregator-s = { git = "https://github.com/DelphinusLab/halo2aggregator-s.git", branch = "main", features = ["unsafe"] }
 halo2_proofs = { git = "https://github.com/DelphinusLab/halo2-gpu-specific.git", default-features = true }
 parity-wasm = { version = "0.42.0", features = ["sign_ext"] }
+thiserror = { version = "1.0.50" }
 wasmi = { path = "third-party/wasmi" }
 
 [profile.dev]

diff --git a/crates/zkwasm/Cargo.toml b/crates/zkwasm/Cargo.toml
@@ -30,6 +30,7 @@ anyhow.workspace = true
 halo2aggregator-s.workspace = true
 halo2_proofs.workspace = true
 parity-wasm.workspace = true
+thiserror.workspace = true
 wasmi.workspace = true
 
 # TODO put the host circuits into features

diff --git a/crates/zkwasm/src/circuits/rtable.rs b/crates/zkwasm/src/circuits/rtable.rs
@@ -18,6 +18,10 @@ use strum::IntoEnumIterator;
 
 const POW_OP: u64 = 4;
 
+pub fn maximal_common_range() -> u32 {
+    (1u32 << (zkwasm_k() - 1)) - 1
+}
+
 /*
  * | Comment   | Op  | left(u8) | right                       | result   |
  * | --------- | --- | -------- | --------------------------- | -------- |
@@ -163,11 +167,11 @@ impl<F: FieldExt> RangeTableChip<F> {
         layouter.assign_table(
             || "common range table",
             |mut table| {
-                for i in 0..(1 << (zkwasm_k() - 1)) {
+                for i in 0..=maximal_common_range() {
                     table.assign_cell(
                         || "range table",
                         self.config.common_range_col,
-                        i,
+                        i as usize,
                         || Ok(F::from(i as u64)),
                     )?;
                 }

diff --git a/crates/zkwasm/src/circuits/test_circuit/mod.rs b/crates/zkwasm/src/circuits/test_circuit/mod.rs
@@ -210,7 +210,15 @@ impl<F: FieldExt> Circuit<F> for TestCircuit<F> {
                             &self.tables.execution_tables.etable,
                             &memory_writing_table,
                         )
-                    );
+                    )
+                    .map_err(|err| match err {
+                        crate::circuits::utils::table_entry::Error::CircuitSizeNotEnough => {
+                            // TODO: maybe put K in self
+                            Error::NotEnoughRowsAvailable {
+                                current_k: zkwasm_k(),
+                            }
+                        }
+                    })?;
 
                     let etable_permutation_cells = exec_with_profile!(
                         || "Assign etable",

diff --git a/crates/zkwasm/src/circuits/utils/table_entry.rs b/crates/zkwasm/src/circuits/utils/table_entry.rs
@@ -1,3 +1,4 @@
+use log::error;
 use serde::Serialize;
 use specs::etable::EventTable;
 use specs::etable::EventTableEntry;
@@ -10,10 +11,17 @@ use std::collections::BTreeMap;
 use std::env;
 use std::io::Write;
 use std::path::PathBuf;
+use thiserror::Error;
 
-use crate::circuits::config::zkwasm_k;
+use crate::circuits::rtable::maximal_common_range;
 use crate::runtime::memory_event_of_step;
 
+#[derive(Error, Debug)]
+pub enum Error {
+    #[error("Failed to lookup memory writing in MemoryWritingTable. It is usually because K is insufficient for the execution, please increase K and try again.")]
+    CircuitSizeNotEnough,
+}
+
 #[derive(Clone, Debug, Serialize)]
 pub(in crate::circuits) struct MemoryWritingEntry {
     index: usize,
@@ -32,7 +40,7 @@ pub struct MemoryWritingTable(pub(in crate::circuits) Vec<MemoryWritingEntry>);
 
 impl From<MTable> for MemoryWritingTable {
     fn from(value: MTable) -> Self {
-        let maximal_eid = (1u32 << (zkwasm_k() - 1)) - 1;
+        let maximal_eid = maximal_common_range();
         let mut index = 0;
 
         let mut entries: Vec<MemoryWritingEntry> = value
@@ -128,58 +136,67 @@ impl EventTableWithMemoryInfo {
     pub(in crate::circuits) fn new(
         event_table: &EventTable,
         memory_writing_table: &MemoryWritingTable,
-    ) -> Self {
+    ) -> Result<Self, Error> {
         let lookup = memory_writing_table.build_lookup_mapping();
 
-        let lookup_mtable_eid = |(eid, ltype, offset, is_writing)| {
+        let lookup_mtable_eid = |(eid, ltype, offset, is_writing)| -> Result<(u32, u32), Error> {
             let records = lookup.get(&(ltype, offset)).unwrap();
 
+            // The MemoryWritingTable uses maximal_common_range as maximal end eid, hence
+            // searching will be failed if eid exceeds maximal_common_range.
+            if eid > maximal_common_range() {
+                return Err(Error::CircuitSizeNotEnough);
+            }
+
             if is_writing {
-                let idx = records
-                    .binary_search_by(|(start_eid, _)| start_eid.cmp(eid))
-                    .unwrap();
-                records[idx]
+                let idx = records.binary_search_by(|(start_eid, _)| start_eid.cmp(&eid));
+
+                Ok(records[idx.unwrap()])
             } else {
-                let idx = records
-                    .binary_search_by(|(start_eid, end_eid)| {
-                        if eid <= start_eid {
-                            Ordering::Greater
-                        } else if eid > end_eid {
-                            Ordering::Less
-                        } else {
-                            Ordering::Equal
-                        }
-                    })
-                    .unwrap();
-                records[idx]
+                let idx = records.binary_search_by(|(start_eid, end_eid)| {
+                    if eid <= *start_eid {
+                        Ordering::Greater
+                    } else if eid > *end_eid {
+                        Ordering::Less
+                    } else {
+                        Ordering::Equal
+                    }
+                });
+
+                idx.map(|idx| records[idx])
+                    .map_err(|_| Error::CircuitSizeNotEnough)
             }
         };
 
-        EventTableWithMemoryInfo(
-            event_table
-                .entries()
-                .iter()
-                .map(|eentry| EventTableEntryWithMemoryInfo {
-                    eentry: eentry.clone(),
-                    memory_rw_entires: memory_event_of_step(eentry, &mut 1)
-                        .iter()
-                        .map(|mentry| {
-                            let (start_eid, end_eid) = lookup_mtable_eid((
-                                &eentry.eid,
-                                mentry.ltype,
-                                mentry.offset,
-                                mentry.atype == AccessType::Write,
-                            ));
-
-                            MemoryRWEntry {
-                                entry: mentry.clone(),
-                                start_eid,
-                                end_eid,
-                            }
+        let entries = event_table
+            .entries()
+            .iter()
+            .map(|eentry| {
+                let memory_rw_entires = memory_event_of_step(eentry, &mut 1)
+                    .into_iter()
+                    .map(|mentry| {
+                        let (start_eid, end_eid) = lookup_mtable_eid((
+                            eentry.eid,
+                            mentry.ltype,
+                            mentry.offset,
+                            mentry.atype == AccessType::Write,
+                        ))?;
+
+                        Ok(MemoryRWEntry {
+                            entry: mentry.clone(),
+                            start_eid,
+                            end_eid,
                         })
-                        .collect(),
+                    })
+                    .collect::<Result<_, _>>()?;
+
+                Ok(EventTableEntryWithMemoryInfo {
+                    eentry: eentry.clone(),
+                    memory_rw_entires,
                 })
-                .collect(),
-        )
+            })
+            .collect::<Result<_, _>>()?;
+
+        Ok(EventTableWithMemoryInfo(entries))
     }
 }