Merge branch 'master' into logic-ops

scroll-tech · Sep 18, 2024 · 0b54570 · 0b54570
2 parents 305af7c + ec51621
commit 0b54570
Show file tree

Hide file tree

Showing 6 changed files with 155 additions and 226 deletions.
diff --git a/ceno_zkvm/benches/riscv_add.rs b/ceno_zkvm/benches/riscv_add.rs
@@ -3,7 +3,7 @@ use std::time::{Duration, Instant};
 use ark_std::test_rng;
 use ceno_zkvm::{
     self,
-    instructions::{riscv::addsub::AddInstruction, Instruction},
+    instructions::{riscv::arith::AddInstruction, Instruction},
     scheme::prover::ZKVMProver,
     structs::{ZKVMConstraintSystem, ZKVMFixedTraces},
 };

diff --git a/ceno_zkvm/examples/riscv_add.rs b/ceno_zkvm/examples/riscv_add.rs
@@ -2,7 +2,7 @@ use std::time::Instant;
 
 use ark_std::test_rng;
 use ceno_zkvm::{
-    instructions::riscv::addsub::AddInstruction, scheme::prover::ZKVMProver,
+    instructions::riscv::arith::AddInstruction, scheme::prover::ZKVMProver,
     tables::ProgramTableCircuit,
 };
 use clap::Parser;

diff --git a/ceno_zkvm/src/instructions/riscv.rs b/ceno_zkvm/src/instructions/riscv.rs
@@ -1,11 +1,10 @@
 use ceno_emul::InsnKind;
 
-pub mod addsub;
+pub mod arith;
 pub mod blt;
 pub mod config;
 pub mod constants;
 pub mod logic;
-pub mod mul;
 
 mod r_insn;
 

diff --git a/ceno_zkvm/src/instructions/riscv/addsub.rs → ceno_zkvm/src/instructions/riscv/arith.rs b/ceno_zkvm/src/instructions/riscv/addsub.rs → ceno_zkvm/src/instructions/riscv/arith.rs
@@ -35,6 +35,12 @@ impl RIVInstruction for SubOp {
 }
 pub type SubInstruction<E> = ArithInstruction<E, SubOp>;
 
+pub struct MulOp;
+impl RIVInstruction for MulOp {
+    const INST_KIND: InsnKind = InsnKind::MUL;
+}
+pub type MulInstruction<E> = ArithInstruction<E, MulOp>;
+
 impl<E: ExtensionField, I: RIVInstruction> Instruction<E> for ArithInstruction<E, I> {
     type InstructionConfig = ArithConfig<E>;
 
@@ -68,6 +74,15 @@ impl<E: ExtensionField, I: RIVInstruction> Instruction<E> for ArithInstruction<E
                 (rs1_read, rs2_read, rd_written)
             }
 
+            InsnKind::MUL => {
+                // rs1_read * rs2_read = rd_written
+                let mut rs1_read = UInt::new_unchecked(|| "rs1_read", circuit_builder)?;
+                let mut rs2_read = UInt::new_unchecked(|| "rs2_read", circuit_builder)?;
+                let rd_written =
+                    rs1_read.mul(|| "rd_written", circuit_builder, &mut rs2_read, true)?;
+                (rs1_read, rs2_read, rd_written)
+            }
+
             _ => unreachable!("Unsupported instruction kind"),
         };
 
@@ -135,6 +150,29 @@ impl<E: ExtensionField, I: RIVInstruction> Instruction<E> for ArithInstruction<E
                 );
             }
 
+            InsnKind::MUL => {
+                // rs1_read * rs2_read = rd_written
+                let rs1_read = Value::new_unchecked(step.rs1().unwrap().value);
+                let rd_written = Value::new_unchecked(step.rd().unwrap().value.after);
+
+                config
+                    .rs1_read
+                    .assign_limbs(instance, rs1_read.u16_fields());
+
+                let (_, carries) = rs1_read.mul(&rs2_read, lk_multiplicity, true);
+
+                config
+                    .rd_written
+                    .assign_limbs(instance, rd_written.u16_fields());
+                config.rd_written.assign_carries(
+                    instance,
+                    carries
+                        .into_iter()
+                        .map(|carry| E::BaseField::from(carry as u64))
+                        .collect_vec(),
+                );
+            }
+
             _ => unreachable!("Unsupported instruction kind"),
         };
 
@@ -149,14 +187,13 @@ mod test {
     use itertools::Itertools;
     use multilinear_extensions::mle::IntoMLEs;
 
+    use super::*;
     use crate::{
         circuit_builder::{CircuitBuilder, ConstraintSystem},
         instructions::Instruction,
-        scheme::mock_prover::{MockProver, MOCK_PC_ADD, MOCK_PC_SUB, MOCK_PROGRAM},
+        scheme::mock_prover::{MockProver, MOCK_PC_ADD, MOCK_PC_MUL, MOCK_PC_SUB, MOCK_PROGRAM},
     };
 
-    use super::{AddInstruction, SubInstruction};
-
     #[test]
     #[allow(clippy::option_map_unit_fn)]
     fn test_opcode_add() {
@@ -328,4 +365,115 @@ mod test {
             None,
         );
     }
+
+    #[test]
+    fn test_opcode_mul() {
+        let mut cs = ConstraintSystem::<GoldilocksExt2>::new(|| "riscv");
+        let mut cb = CircuitBuilder::new(&mut cs);
+        let config = cb
+            .namespace(|| "mul", |cb| Ok(MulInstruction::construct_circuit(cb)))
+            .unwrap()
+            .unwrap();
+
+        // values assignment
+        let (raw_witin, _) = MulInstruction::assign_instances(
+            &config,
+            cb.cs.num_witin as usize,
+            vec![StepRecord::new_r_instruction(
+                3,
+                MOCK_PC_MUL,
+                MOCK_PROGRAM[2],
+                11,
+                2,
+                Change::new(0, 22),
+                0,
+            )],
+        )
+        .unwrap();
+
+        MockProver::assert_satisfied(
+            &mut cb,
+            &raw_witin
+                .de_interleaving()
+                .into_mles()
+                .into_iter()
+                .map(|v| v.into())
+                .collect_vec(),
+            None,
+        );
+    }
+
+    #[test]
+    fn test_opcode_mul_overflow() {
+        let mut cs = ConstraintSystem::<GoldilocksExt2>::new(|| "riscv");
+        let mut cb = CircuitBuilder::new(&mut cs);
+        let config = cb
+            .namespace(|| "mul", |cb| Ok(MulInstruction::construct_circuit(cb)))
+            .unwrap()
+            .unwrap();
+
+        // values assignment
+        let (raw_witin, _) = MulInstruction::assign_instances(
+            &config,
+            cb.cs.num_witin as usize,
+            vec![StepRecord::new_r_instruction(
+                3,
+                MOCK_PC_MUL,
+                MOCK_PROGRAM[2],
+                u32::MAX / 2 + 1,
+                2,
+                Change::new(0, 0),
+                0,
+            )],
+        )
+        .unwrap();
+
+        MockProver::assert_satisfied(
+            &mut cb,
+            &raw_witin
+                .de_interleaving()
+                .into_mles()
+                .into_iter()
+                .map(|v| v.into())
+                .collect_vec(),
+            None,
+        );
+    }
+
+    #[test]
+    fn test_opcode_mul_overflow2() {
+        let mut cs = ConstraintSystem::<GoldilocksExt2>::new(|| "riscv");
+        let mut cb = CircuitBuilder::new(&mut cs);
+        let config = cb
+            .namespace(|| "mul", |cb| Ok(MulInstruction::construct_circuit(cb)))
+            .unwrap()
+            .unwrap();
+
+        // values assignment
+        let (raw_witin, _) = MulInstruction::assign_instances(
+            &config,
+            cb.cs.num_witin as usize,
+            vec![StepRecord::new_r_instruction(
+                3,
+                MOCK_PC_MUL,
+                MOCK_PROGRAM[2],
+                4294901760,
+                4294901760,
+                Change::new(0, 0),
+                0,
+            )],
+        )
+        .unwrap();
+
+        MockProver::assert_satisfied(
+            &mut cb,
+            &raw_witin
+                .de_interleaving()
+                .into_mles()
+                .into_iter()
+                .map(|v| v.into())
+                .collect_vec(),
+            None,
+        );
+    }
 }