Feat: add rw mismatch checkers and lookup checker in mock prover for zkvm

[kunxian-xia]

This PR is extracted from #526 and it aims to improve current mock prover to find out constraint errors in the zkvm setting.

• lookup errors.
• read / write not equal for global state
• read / write not equal for registers
• read / write not equal for memory

[naure]

How I understood that:

• The ram_type is given as an argument: purely debugging information.
• While it is still also the first field of the record: that's what isolates the tables from each other.

That could be highlighted somehow: doc, assert, ...

Otherwise the two values could be merged (record.insert(0, ram_type) or such), but that would downgrade it from Expression to constant only.

[naure]

Ok, I just realized that’s how it always was in the other methods (read_record, etc).

[hero78119]

👍 good point

Due to have urgent requirement to debug in example in release build, some workaround is fine, and we can make it better by isolated it into a specific features

Later, we can make those debug information toggle on/off by a specific feature e.g.

diff --git a/ceno_zkvm/src/circuit_builder.rs b/ceno_zkvm/src/circuit_builder.rs
index 92682a67..316fa4f9 100644
--- a/ceno_zkvm/src/circuit_builder.rs
+++ b/ceno_zkvm/src/circuit_builder.rs
@@ -386,7 +386,7 @@ impl<E: ExtensionField> ConstraintSystem<E> {
     pub fn read_record<NR: Into<String>, N: FnOnce() -> NR>(
         &mut self,
         name_fn: N,
-        ram_type: RAMType,
+        #[cfg(feature = "debug_lookup_failed")] ram_type: RAMType,
         record: Vec<Expression<E>>,
     ) -> Result<(), ZKVMError> {
         let rlc_record = self.rlc_chip_record(record.clone());
@@ -399,9 +399,12 @@ impl<E: ExtensionField> ConstraintSystem<E> {
         self.r_expressions.push(rlc_record);
         let path = self.ns.compute_path(name_fn().into());
         self.r_expressions_namespace_map.push(path);
-        // Since r_expression is RLC(record) and when we're debugging
-        // it's helpful to recover the value of record itself.
-        self.r_ram_types.push((ram_type, record));
+        #[cfg(feature = "debug_lookup_failed")]
+        {
+            // Since r_expression is RLC(record) and when we're debugging
+            // it's helpful to recover the value of record itself.
+            self.r_ram_types.push((ram_type, record));
+        }
         Ok(())
     }

related to #485

[naure]

No no I can live with that, I’ll suggest some name or documentation later.

[naure]

It's nice that there's no need to call this rlc_chip_record anymore.

[naure]

Too complicated; didn't review yet. But that doesn't hurt if the tests pass.