add lookup records for mockprover

ceno_zkvm/src/instructions/riscv/blt.rs

@@ -235,9 +235,12 @@ impl<E: ExtensionField> Instruction<E> for BltInstruction {
 mod test {
     use super::*;
     use ceno_emul::StepRecord;
+    use ff::Field;
     use goldilocks::GoldilocksExt2;
     use itertools::Itertools;
     use multilinear_extensions::mle::IntoMLEs;
+    use rand::rngs::OsRng;
+    use std::array;
 
     use crate::{circuit_builder::ConstraintSystem, scheme::mock_prover::MockProver};
 
@@ -257,17 +260,18 @@ mod test {
         )
         .unwrap();
 
-        MockProver::run(
+        let rng = OsRng;
+        let challenges: [GoldilocksExt2; 2] = array::from_fn(|_| GoldilocksExt2::random(rng));
+        MockProver::assert_satisfied(
             &mut circuit_builder,
             &raw_witin
                 .de_interleaving()
                 .into_mles()
                 .into_iter()
                 .map(|v| v.into())
                 .collect_vec(),
-            None,
-        )
-        .expect_err("lookup will fail");
+            Some(challenges),
+        );
         Ok(())
     }
 

ceno_zkvm/src/scheme/mock_prover.rs

@@ -266,6 +266,8 @@ impl<'a, E: ExtensionField> MockProver<E> {
         let mut table_vec = vec![];
         load_u5_table(&mut table_vec, cb, challenge);
         load_u16_table(&mut table_vec, cb, challenge);
+        load_and_table(&mut table_vec, cb, challenge);
+        load_ltu_table(&mut table_vec, cb, challenge);
 
         // Lookup expressions
         for (expr, name) in cb
@@ -350,6 +352,44 @@ pub fn load_u16_table<E: ExtensionField>(
     }
 }
 
+pub fn load_and_table<E: ExtensionField>(
+    t_vec: &mut Vec<E>,
+    cb: &CircuitBuilder<E>,
+    challenge: [E; 2],
+) {
+    for i in 0..(1 << 16) {
+        let a = i >> 8;
+        let b = i & 0xFF;
+        let c = a & b;
+        let rlc_record = cb.rlc_chip_record(vec![
+            Expression::Constant(E::BaseField::from(ROMType::And as u64)),
+            i.into(),
+            c.into(),
+        ]);
+        let rlc_record = eval_by_expr(&[], &challenge, &rlc_record);
+        t_vec.push(rlc_record);
+    }
+}
+
+pub fn load_ltu_table<E: ExtensionField>(
+    t_vec: &mut Vec<E>,
+    cb: &CircuitBuilder<E>,
+    challenge: [E; 2],
+) {
+    for i in 0..(1 << 16) {
+        let a = i >> 8;
+        let b = i & 0xFF;
+        let c = (a < b) as usize;
+        let rlc_record = cb.rlc_chip_record(vec![
+            Expression::Constant(E::BaseField::from(ROMType::Ltu as u64)),
+            i.into(),
+            c.into(),
+        ]);
+        let rlc_record = eval_by_expr(&[], &challenge, &rlc_record);
+        t_vec.push(rlc_record);
+    }
+}
+
 #[allow(unused_imports)]
 #[cfg(test)]
 mod tests {

ceno_zkvm/src/uint/arithmetic.rs

@@ -254,7 +254,7 @@ impl<const M: usize, E: ExtensionField> UInt<M, 8, E> {
         circuit_builder.lookup_and_byte(
             high_limb_no_msb.expr(),
             high_limb.clone(),
-            Expression::from(1 << 7),
+            Expression::from(0b0111_1111),
         )?;
 
         let inv_128 = F::from(128).invert().unwrap();