fix: lookup verification fail (#58)

* chore: impl proof recursion * chore: impl proof recursion * chore: impl proof recursion * chore: debug recursive proof * chore: remove dead code * fix: verify * fix: verify * fix: verify * fix: verify * fix: verify * fix: verify * chore: stash * chore: stash * chore: stash * chore: stash * chore: stash * chore: stash * chore: stash * chore: stash * chore: stash * chore: stash-no * chore: stash * chore: stash * chore: stash-no * chore: remove dead code * feat: MFHI, MTHI, MFLO and MTLO. * fix: COMBINED_OPS. * fix: lookup * fix: memory lookup * change data in memory op to LE * fix: slt. * fix: mem timstamp lookup * fix: mem timstamp lookup * fix: mem timstamp lookup * fix: mem timstamp lookup * fix: mem timstamp lookup * fix: mem timstamp lookup * fix index for code * fix: mem lookup * fix: mem lookup --------- Co-authored-by: 0xBlakeee <148928866+0xblakeee@users.noreply.github.com> Co-authored-by: Angell Li <angell.l@zkm.io>
zkMIPS · Dec 22, 2023 · 4c12bb5 · 4c12bb5
1 parent e0bef35
commit 4c12bb5
Show file tree

Hide file tree

Showing 37 changed files with 2,909 additions and 541 deletions.
diff --git a/Cargo.toml b/Cargo.toml
@@ -28,6 +28,7 @@ static_assertions = "1.1.0"
 keccak-hash = "0.10.0"
 byteorder = "1.5.0"
 hex = "0.4"
+hashbrown = { version = "0.14.0", default-features = false, features = ["ahash", "serde"] } # NOTE: When upgrading, see `ahash` dependency.
 lazy_static = "1.4.0"
 
 elf = { version = "0.7", default-features = false }

diff --git a/output/segment0 b/output/segment0
diff --git a/output/segment1 b/output/segment1
diff --git a/src/all_stark.rs b/src/all_stark.rs
@@ -196,7 +196,8 @@ fn ctl_memory<F: Field>() -> CrossTableLookup<F> {
         .chain(keccak_sponge_reads)
         .collect();
     */
-    let all_lookers = cpu_memory_gp_ops.collect();
+    //let all_lookers = iter::once(cpu_memory_code_read)
+    let all_lookers = [].into_iter().chain(cpu_memory_gp_ops).collect();
     let memory_looked = TableWithColumns::new(
         Table::Memory,
         memory_stark::ctl_data(),

diff --git a/src/arithmetic/addcy.rs b/src/arithmetic/addcy.rs
@@ -38,11 +38,17 @@ pub(crate) fn generate<F: PrimeField64>(lv: &mut [F], filter: usize, left_in: u3
             u32_to_array(&mut lv[AUX_INPUT_REGISTER_0], cy as u32);
             u32_to_array(&mut lv[OUTPUT_REGISTER], result);
         }
-        IS_SUB => {
+        IS_SUB | IS_SUBU => {
             let (diff, cy) = left_in.overflowing_sub(right_in);
             u32_to_array(&mut lv[AUX_INPUT_REGISTER_0], cy as u32);
             u32_to_array(&mut lv[OUTPUT_REGISTER], diff);
         }
+        IS_ADDU | IS_ADDIU => {
+            // FIXME: add constraints
+            let (result, cy) = left_in.overflowing_add(right_in);
+            u32_to_array(&mut lv[AUX_INPUT_REGISTER_0], cy as u32);
+            u32_to_array(&mut lv[OUTPUT_REGISTER], result);
+        }
         _ => panic!("unexpected operation filter"),
     };
 }

diff --git a/src/arithmetic/arithmetic_stark.rs b/src/arithmetic/arithmetic_stark.rs
@@ -16,7 +16,7 @@ use super::shift;
 use crate::all_stark::Table;
 use crate::arithmetic::columns::{RANGE_COUNTER, RC_FREQUENCIES, SHARED_COLS};
 //use crate::arithmetic::{addcy, byte, columns, divmod, modular, mul, Operation};
-use crate::arithmetic::{addcy, columns, div, lui, mul, mult, slt, sra, Operation};
+use crate::arithmetic::{addcy, columns, div, lo_hi, lui, mul, mult, slt, sra, Operation};
 use crate::constraint_consumer::{ConstraintConsumer, RecursiveConstraintConsumer};
 use crate::cross_table_lookup::{Column, TableWithColumns};
 use crate::evaluation_frame::{StarkEvaluationFrame, StarkFrame};
@@ -55,6 +55,7 @@ fn cpu_arith_data_link<F: Field>(
             res.push(Column::linear_combination([(c0, F::ONE), (c1, limb_base)]));
         }
     }
+
     res
 }
 
@@ -64,28 +65,33 @@ pub fn ctl_arithmetic_rows<F: Field>() -> TableWithColumns<F> {
     // the CTL will enforce that the reconstructed opcode value
     // from the opcode bits matches.
     // FIXME: opcode = op + 2^6 * func
-    const COMBINED_OPS: [(usize, u32); 21] = [
+    const COMBINED_OPS: [(usize, u32); 18] = [
         (columns::IS_ADD, 0b000000 + 0b100000 * (1 << 6)),
         (columns::IS_ADDU, 0b000000 + 0b100001 * (1 << 6)),
-        (columns::IS_ADDI, 0b001000 + 0b000000 * (1 << 6)),
-        (columns::IS_ADDIU, 0b001001 + 0b000000 * (1 << 6)),
+        //(columns::IS_ADDI, 0b001000 + 0b000000 * (1 << 6)),
+        //(columns::IS_ADDIU, 0b001001 + 0b000000 * (1 << 6)),
         (columns::IS_SUB, 0b000000 + 0b100010 * (1 << 6)),
         (columns::IS_SUBU, 0b000000 + 0b100011 * (1 << 6)),
         (columns::IS_MULT, 0b000000 + 0b011000 * (1 << 6)),
         (columns::IS_MULTU, 0b000000 + 0b011001 * (1 << 6)),
+        (columns::IS_MUL, 0b011100 + 0b000010 * (1 << 6)),
         (columns::IS_DIV, 0b000000 + 0b011010 * (1 << 6)),
         (columns::IS_DIVU, 0b000000 + 0b011011 * (1 << 6)),
         (columns::IS_SLLV, 0b000000 + 0b000100 * (1 << 6)),
         (columns::IS_SRLV, 0b000000 + 0b000110 * (1 << 6)),
         (columns::IS_SRAV, 0b000000 + 0b000111 * (1 << 6)),
-        (columns::IS_SLL, 0b000000 + 0b000000 * (1 << 6)),
-        (columns::IS_SRL, 0b000000 + 0b000010 * (1 << 6)),
-        (columns::IS_SRA, 0b000000 + 0b000011 * (1 << 6)),
+        //(columns::IS_SLL, 0b000000 + 0b000000 * (1 << 6)),
+        //(columns::IS_SRL, 0b000000 + 0b000010 * (1 << 6)),
+        //(columns::IS_SRA, 0b000000 + 0b000011 * (1 << 6)),
         (columns::IS_SLT, 0b000000 + 0b101010 * (1 << 6)),
         (columns::IS_SLTU, 0b000000 + 0b101011 * (1 << 6)),
-        (columns::IS_SLTI, 0b001010 + 0b000000 * (1 << 6)),
-        (columns::IS_SLTIU, 0b001011 + 0b000000 * (1 << 6)),
-        (columns::IS_LUI, 0b001111 + 0b000000 * (1 << 6)),
+        // (columns::IS_SLTI, 0b001010 + 0b000000 * (1 << 6)),
+        // (columns::IS_SLTIU, 0b001011 + 0b000000 * (1 << 6)),
+        // (columns::IS_LUI, 0b001111 + 0b000000 * (1 << 6)),
+        (columns::IS_MFHI, 0b000000 + 0b010000 * (1 << 6)),
+        (columns::IS_MTHI, 0b000000 + 0b010001 * (1 << 6)),
+        (columns::IS_MFLO, 0b000000 + 0b010010 * (1 << 6)),
+        (columns::IS_MTLO, 0b000000 + 0b010011 * (1 << 6)),
     ];
 
     const REGISTER_MAP: [Range<usize>; 3] = [
@@ -222,6 +228,7 @@ impl<F: RichField + Extendable<D>, const D: usize> Stark<F, D> for ArithmeticSta
         //byte::eval_packed(lv, yield_constr);
         shift::eval_packed_generic(lv, nv, yield_constr);
         sra::eval_packed_generic(lv, nv, yield_constr);
+        lo_hi::eval_packed_generic(lv, yield_constr);
     }
 
     fn eval_ext_circuit(
@@ -259,6 +266,7 @@ impl<F: RichField + Extendable<D>, const D: usize> Stark<F, D> for ArithmeticSta
         //byte::eval_ext_circuit(builder, lv, yield_constr);
         shift::eval_ext_circuit(builder, lv, nv, yield_constr);
         sra::eval_ext_circuit(builder, lv, nv, yield_constr);
+        lo_hi::eval_ext_circuit(builder, lv, yield_constr);
     }
 
     fn constraint_degree(&self) -> usize {

diff --git a/src/arithmetic/columns.rs b/src/arithmetic/columns.rs
@@ -44,8 +44,12 @@ pub(crate) const IS_SLTU: usize = IS_SLT + 1;
 pub(crate) const IS_SLTI: usize = IS_SLTU + 1;
 pub(crate) const IS_SLTIU: usize = IS_SLTI + 1;
 pub(crate) const IS_LUI: usize = IS_SLTIU + 1;
+pub(crate) const IS_MFHI: usize = IS_LUI + 1;
+pub(crate) const IS_MTHI: usize = IS_MFHI + 1;
+pub(crate) const IS_MFLO: usize = IS_MTHI + 1;
+pub(crate) const IS_MTLO: usize = IS_MFLO + 1;
 
-pub(crate) const START_SHARED_COLS: usize = IS_LUI + 1;
+pub(crate) const START_SHARED_COLS: usize = IS_MTLO + 1;
 
 /// Within the Arithmetic Unit, there are shared columns which can be
 /// used by any arithmetic circuit, depending on which one is active

diff --git a/src/arithmetic/lo_hi.rs b/src/arithmetic/lo_hi.rs
@@ -0,0 +1,133 @@
+//! Support for EVM instructions MFHI, MTHI, MHLO, MTLO
+
+use plonky2::field::extension::Extendable;
+use plonky2::field::packed::PackedField;
+use plonky2::field::types::PrimeField64;
+use plonky2::hash::hash_types::RichField;
+use plonky2::iop::ext_target::ExtensionTarget;
+use plonky2::plonk::circuit_builder::CircuitBuilder;
+
+use crate::arithmetic::columns::*;
+use crate::arithmetic::utils::u32_to_array;
+use crate::constraint_consumer::{ConstraintConsumer, RecursiveConstraintConsumer};
+
+/// Generate row for MFHI, MTHI, MHLO, and MTLO operations.
+pub(crate) fn generate<F: PrimeField64>(lv: &mut [F], filter: usize, input: u32, result: u32) {
+    u32_to_array(&mut lv[INPUT_REGISTER_0], input);
+
+    match filter {
+        IS_MFHI | IS_MTHI | IS_MFLO | IS_MTLO => {
+            u32_to_array(&mut lv[OUTPUT_REGISTER], result);
+        }
+        _ => panic!("unexpected operation filter"),
+    };
+}
+pub fn eval_packed_generic<P: PackedField>(
+    lv: &[P; NUM_ARITH_COLUMNS],
+    yield_constr: &mut ConstraintConsumer<P>,
+) {
+    let filter = lv[IS_MFHI] + lv[IS_MTHI] + lv[IS_MFLO] + lv[IS_MTLO];
+
+    let input = &lv[INPUT_REGISTER_0];
+    let output = &lv[OUTPUT_REGISTER];
+    for (input, output) in input.iter().zip(output) {
+        yield_constr.constraint(filter * (*input - *output));
+    }
+}
+
+pub fn eval_ext_circuit<F: RichField + Extendable<D>, const D: usize>(
+    builder: &mut CircuitBuilder<F, D>,
+    lv: &[ExtensionTarget<D>; NUM_ARITH_COLUMNS],
+    yield_constr: &mut RecursiveConstraintConsumer<F, D>,
+) {
+    let filter = builder.add_many_extension([lv[IS_MFHI], lv[IS_MTHI], lv[IS_MFLO], lv[IS_MTLO]]);
+
+    let input = &lv[INPUT_REGISTER_0];
+    let output = &lv[OUTPUT_REGISTER];
+    for (input, output) in input.iter().zip(output) {
+        let sub = builder.sub_extension(*input, *output);
+        let t = builder.mul_extension(filter, sub);
+        yield_constr.constraint(builder, t);
+    }
+}
+
+#[cfg(test)]
+mod tests {
+    use plonky2::field::goldilocks_field::GoldilocksField;
+    use plonky2::field::types::{Field, Sample};
+    use rand::{Rng, SeedableRng};
+    use rand_chacha::ChaCha8Rng;
+
+    use super::*;
+    use crate::arithmetic::columns::NUM_ARITH_COLUMNS;
+    use crate::constraint_consumer::ConstraintConsumer;
+
+    const OPS: [usize; 4] = [IS_MFHI, IS_MTHI, IS_MFLO, IS_MTLO];
+    #[test]
+    fn generate_eval_consistency_not_lo_hi() {
+        type F = GoldilocksField;
+
+        let mut rng = ChaCha8Rng::seed_from_u64(0x6feb51b7ec230f25);
+        let mut lv = [F::default(); NUM_ARITH_COLUMNS].map(|_| F::sample(&mut rng));
+
+        // if the operation filters are all zero, then the constraints
+        // should be met even if all values are garbage.
+        OPS.map(|i| lv[i] = F::ZERO);
+
+        let mut constrant_consumer = ConstraintConsumer::new(
+            vec![GoldilocksField(2), GoldilocksField(3), GoldilocksField(5)],
+            F::ONE,
+            F::ONE,
+            F::ONE,
+        );
+        eval_packed_generic(&lv, &mut constrant_consumer);
+        for &acc in &constrant_consumer.constraint_accs {
+            assert_eq!(acc, F::ZERO);
+        }
+    }
+
+    #[test]
+    fn generate_eval_consistency_addcy() {
+        type F = GoldilocksField;
+
+        let mut rng = ChaCha8Rng::seed_from_u64(0x6feb51b7ec230f25);
+        const N_ITERS: usize = 1000;
+
+        for _ in 0..N_ITERS {
+            for op_filter in OPS {
+                // set entire row to random 16-bit values
+                let mut lv = [F::default(); NUM_ARITH_COLUMNS]
+                    .map(|_| F::from_canonical_u16(rng.gen::<u16>()));
+
+                // set operation filter and ensure all constraints are
+                // satisfied. We have to explicitly set the other
+                // operation filters to zero since all are treated by
+                // the call.
+                OPS.map(|i| lv[i] = F::ZERO);
+                lv[op_filter] = F::ONE;
+
+                let input = rng.gen::<u32>();
+
+                generate(&mut lv, op_filter, input, input);
+
+                let mut constrant_consumer = ConstraintConsumer::new(
+                    vec![GoldilocksField(2), GoldilocksField(3), GoldilocksField(5)],
+                    F::ONE,
+                    F::ONE,
+                    F::ONE,
+                );
+                eval_packed_generic(&lv, &mut constrant_consumer);
+                for &acc in &constrant_consumer.constraint_accs {
+                    assert_eq!(acc, F::ZERO);
+                }
+
+                let mut expected_limbs = [F::ZERO; N_LIMBS];
+                u32_to_array(&mut expected_limbs, input);
+                assert!(expected_limbs
+                    .iter()
+                    .zip(&lv[OUTPUT_REGISTER])
+                    .all(|(x, y)| x == y));
+            }
+        }
+    }
+}
diff --git a/src/arithmetic/mod.rs b/src/arithmetic/mod.rs
@@ -2,6 +2,7 @@ pub mod addcy;
 pub mod arithmetic_stark;
 pub mod columns;
 pub mod div;
+pub mod lo_hi;
 pub mod lui;
 pub mod mul;
 pub mod mult;
@@ -37,6 +38,10 @@ pub(crate) enum BinaryOperator {
     SLTI,
     SLTIU,
     LUI,
+    MFHI,
+    MTHI,
+    MFLO,
+    MTLO,
 }
 
 impl BinaryOperator {
@@ -120,6 +125,10 @@ impl BinaryOperator {
                 ((input0 as i32) % (input1 as i32)) as u32, // hi
             ),
             BinaryOperator::DIVU => (input0 / input1, input0 % input1), //lo,hi
+            BinaryOperator::MFHI
+            | BinaryOperator::MTHI
+            | BinaryOperator::MFLO
+            | BinaryOperator::MTLO => (input0, 0),
         }
     }
 
@@ -147,6 +156,10 @@ impl BinaryOperator {
             BinaryOperator::SLTU => columns::IS_SLTU,
             BinaryOperator::SLT => columns::IS_SLT,
             BinaryOperator::LUI => columns::IS_LUI,
+            BinaryOperator::MFHI => columns::IS_MFHI,
+            BinaryOperator::MTHI => columns::IS_MTHI,
+            BinaryOperator::MFLO => columns::IS_MFLO,
+            BinaryOperator::MTLO => columns::IS_MTLO,
         }
     }
 }
@@ -232,7 +245,12 @@ fn binary_op_to_rows<F: PrimeField64>(
     row[op.row_filter()] = F::ONE;
 
     match op {
-        BinaryOperator::ADD | BinaryOperator::SUB | BinaryOperator::ADDI => {
+        BinaryOperator::ADD
+        | BinaryOperator::SUB
+        | BinaryOperator::ADDI
+        | BinaryOperator::ADDIU
+        | BinaryOperator::ADDU
+        | BinaryOperator::SUBU => {
             addcy::generate(&mut row, op.row_filter(), input0, input1);
             (row, None)
         }
@@ -284,7 +302,12 @@ fn binary_op_to_rows<F: PrimeField64>(
             sra::generate(&mut row, &mut nv, op.row_filter(), input1, input0, result0);
             (row, Some(nv))
         }
-
-        _ => (row, None),
+        BinaryOperator::MFHI
+        | BinaryOperator::MTHI
+        | BinaryOperator::MFLO
+        | BinaryOperator::MTLO => {
+            lo_hi::generate(&mut row, op.row_filter(), input0, result0);
+            (row, None)
+        }
     }
 }
diff --git a/src/arithmetic/slt.rs b/src/arithmetic/slt.rs
@@ -34,14 +34,14 @@ pub(crate) fn generate<F: PrimeField64>(
             }
 
             u32_to_array(&mut lv[AUX_INPUT_REGISTER_0], diff);
-            u32_to_array(&mut lv[AUX_INPUT_REGISTER_1], rd);
-            u32_to_array(&mut lv[OUTPUT_REGISTER], cy_val);
+            u32_to_array(&mut lv[AUX_INPUT_REGISTER_1], cy_val);
+            u32_to_array(&mut lv[OUTPUT_REGISTER], rd);
         }
         IS_SLTU | IS_SLTIU => {
             let (diff, cy) = left_in.overflowing_sub(right_in);
             u32_to_array(&mut lv[AUX_INPUT_REGISTER_0], diff);
-            u32_to_array(&mut lv[AUX_INPUT_REGISTER_1], rd);
-            u32_to_array(&mut lv[OUTPUT_REGISTER], cy as u32);
+            u32_to_array(&mut lv[AUX_INPUT_REGISTER_1], cy as u32);
+            u32_to_array(&mut lv[OUTPUT_REGISTER], rd);
         }
         _ => panic!("unexpected operation filter"),
     };
@@ -65,7 +65,7 @@ pub fn eval_packed_generic<P: PackedField>(
     let aux = &lv[AUX_INPUT_REGISTER_0];
     let rd = &lv[AUX_INPUT_REGISTER_1];
 
-    eval_packed_generic_slt(yield_constr, is_lt, is_sign, in1, aux, in0, out, rd);
+    eval_packed_generic_slt(yield_constr, is_lt, is_sign, in1, aux, in0, rd, out);
 }
 
 pub(crate) fn eval_packed_generic_slt<P: PackedField>(
@@ -137,8 +137,8 @@ pub fn eval_ext_circuit<F: RichField + Extendable<D>, const D: usize>(
         in1,
         aux,
         in0,
-        out,
         rd,
+        out,
     );
 }