addi opcode (#260)

ceno_emul/src/rv32im.rs

@@ -326,7 +326,7 @@ impl DecodedInstruction {
         match self.codes() {
             InsnCodes { format: R, .. } => false,
             InsnCodes {
-                kind: SLLI | SRLI | SRAI,
+                kind: SLLI | SRLI | SRAI | ADDI,
                 ..
             } => false,
             _ => self.top_bit != 0,

ceno_zkvm/src/instructions/riscv.rs

@@ -1,6 +1,7 @@
 use ceno_emul::InsnKind;
 
 pub mod arith;
+pub mod arith_imm;
 pub mod blt;
 pub mod branch;
 pub mod config;

ceno_zkvm/src/instructions/riscv/arith_imm.rs

@@ -0,0 +1,179 @@
+use std::{marker::PhantomData, mem::MaybeUninit};
+
+use ceno_emul::StepRecord;
+use ff_ext::ExtensionField;
+
+use crate::{
+    circuit_builder::CircuitBuilder, error::ZKVMError, instructions::Instruction,
+    witness::LkMultiplicity, Value,
+};
+
+use super::{constants::UInt, i_insn::IInstructionConfig, RIVInstruction};
+
+pub struct AddiInstruction<E>(PhantomData<E>);
+
+impl<E> RIVInstruction for AddiInstruction<E> {
+    const INST_KIND: ceno_emul::InsnKind = ceno_emul::InsnKind::ADDI;
+}
+
+pub struct InstructionConfig<E: ExtensionField> {
+    i_insn: IInstructionConfig<E>,
+
+    rs1_read: UInt<E>,
+    imm: UInt<E>,
+    rd_written: UInt<E>,
+}
+
+impl<E: ExtensionField> Instruction<E> for AddiInstruction<E> {
+    type InstructionConfig = InstructionConfig<E>;
+
+    fn name() -> String {
+        format!("{:?}", Self::INST_KIND)
+    }
+
+    fn construct_circuit(
+        circuit_builder: &mut CircuitBuilder<E>,
+    ) -> Result<Self::InstructionConfig, ZKVMError> {
+        let rs1_read = UInt::new_unchecked(|| "rs1_read", circuit_builder)?;
+        let imm = UInt::new_unchecked(|| "imm", circuit_builder)?;
+        let rd_written = rs1_read.add(|| "rs1_read + imm", circuit_builder, &imm, true)?;
+
+        let i_insn = IInstructionConfig::<E>::construct_circuit(
+            circuit_builder,
+            Self::INST_KIND,
+            &imm.value(),
+            rs1_read.register_expr(),
+            rd_written.register_expr(),
+        )?;
+
+        Ok(InstructionConfig {
+            i_insn,
+            rs1_read,
+            imm,
+            rd_written,
+        })
+    }
+
+    fn assign_instance(
+        config: &Self::InstructionConfig,
+        instance: &mut [MaybeUninit<<E as ExtensionField>::BaseField>],
+        lk_multiplicity: &mut LkMultiplicity,
+        step: &StepRecord,
+    ) -> Result<(), ZKVMError> {
+        let rs1_read = Value::new_unchecked(step.rs1().unwrap().value);
+        let imm = Value::new(step.insn().imm_or_funct7(), lk_multiplicity);
+
+        let (result, carry) = rs1_read.add(&imm, lk_multiplicity, true);
+
+        config.rs1_read.assign_value(instance, rs1_read);
+        config.imm.assign_value(instance, imm);
+
+        config
+            .rd_written
+            .assign_limb_with_carry(instance, &(result, carry));
+
+        config
+            .i_insn
+            .assign_instance(instance, lk_multiplicity, step)?;
+
+        Ok(())
+    }
+}
+
+#[cfg(test)]
+mod test {
+    use ceno_emul::{Change, StepRecord};
+    use goldilocks::GoldilocksExt2;
+    use itertools::Itertools;
+    use multilinear_extensions::mle::IntoMLEs;
+
+    use crate::{
+        circuit_builder::{CircuitBuilder, ConstraintSystem},
+        instructions::Instruction,
+        scheme::mock_prover::{MockProver, MOCK_PC_ADDI, MOCK_PC_ADDI_SUB, MOCK_PROGRAM},
+    };
+
+    use super::AddiInstruction;
+
+    #[test]
+    fn test_opcode_addi() {
+        let mut cs = ConstraintSystem::<GoldilocksExt2>::new(|| "riscv");
+        let mut cb = CircuitBuilder::new(&mut cs);
+        let config = cb
+            .namespace(
+                || "addi",
+                |cb| {
+                    let config = AddiInstruction::<GoldilocksExt2>::construct_circuit(cb);
+                    Ok(config)
+                },
+            )
+            .unwrap()
+            .unwrap();
+
+        let (raw_witin, _) = AddiInstruction::<GoldilocksExt2>::assign_instances(
+            &config,
+            cb.cs.num_witin as usize,
+            vec![StepRecord::new_i_instruction(
+                3,
+                MOCK_PC_ADDI,
+                MOCK_PROGRAM[13],
+                1000,
+                Change::new(0, 1003),
+                0,
+            )],
+        )
+        .unwrap();
+
+        MockProver::assert_satisfied(
+            &cb,
+            &raw_witin
+                .de_interleaving()
+                .into_mles()
+                .into_iter()
+                .map(|v| v.into())
+                .collect_vec(),
+            None,
+        );
+    }
+
+    #[test]
+    fn test_opcode_addi_sub() {
+        let mut cs = ConstraintSystem::<GoldilocksExt2>::new(|| "riscv");
+        let mut cb = CircuitBuilder::new(&mut cs);
+        let config = cb
+            .namespace(
+                || "addi",
+                |cb| {
+                    let config = AddiInstruction::<GoldilocksExt2>::construct_circuit(cb);
+                    Ok(config)
+                },
+            )
+            .unwrap()
+            .unwrap();
+
+        let (raw_witin, _) = AddiInstruction::<GoldilocksExt2>::assign_instances(
+            &config,
+            cb.cs.num_witin as usize,
+            vec![StepRecord::new_i_instruction(
+                3,
+                MOCK_PC_ADDI_SUB,
+                MOCK_PROGRAM[14],
+                1000,
+                Change::new(0, 997),
+                0,
+            )],
+        )
+        .unwrap();
+
+        MockProver::assert_satisfied(
+            &cb,
+            &raw_witin
+                .de_interleaving()
+                .into_mles()
+                .into_iter()
+                .map(|v| v.into())
+                .collect_vec(),
+            Some([1.into(), 10000.into()]),
+        );
+    }
+}

ceno_zkvm/src/scheme/mock_prover.rs

@@ -33,6 +33,7 @@ pub const MOCK_RS2: u32 = 3;
 pub const MOCK_RD: u32 = 4;
 pub const MOCK_IMM_3: u32 = 3;
 pub const MOCK_IMM_31: u32 = 31;
+pub const MOCK_IMM_NEG3: u32 = 32 - 3;
 /// The program baked in the MockProver.
 /// TODO: Make this a parameter?
 #[allow(clippy::identity_op)]
@@ -68,6 +69,10 @@ pub const MOCK_PROGRAM: &[u32] = &[
     0x00 << 25 | MOCK_IMM_31 << 20 | MOCK_RS1 << 15 | 0x05 << 12 | MOCK_RD << 7 | 0x13,
     // sltu (0x00, 0x03, 0x33)
     0x00 << 25 | MOCK_RS2 << 20 | MOCK_RS1 << 15 | 0b011 << 12 | MOCK_RD << 7 | 0x33,
+    // addi x4, x2, 3
+    0x00 << 25 | MOCK_IMM_3 << 20 | MOCK_RS1 << 15 | 0x00 << 12 | MOCK_RD << 7 | 0x13,
+    // addi x4, x2, -3, correc this below
+    0b_1_111111 << 25 | MOCK_IMM_NEG3 << 20 | MOCK_RS1 << 15 | 0x00 << 12 | MOCK_RD << 7 | 0x13,
 ];
 // Addresses of particular instructions in the mock program.
 pub const MOCK_PC_ADD: ByteAddr = ByteAddr(CENO_PLATFORM.pc_start());
@@ -86,6 +91,8 @@ pub const MOCK_PC_DIVU: ByteAddr = ByteAddr(CENO_PLATFORM.pc_start() + 36);
 pub const MOCK_PC_SRLI: ByteAddr = ByteAddr(CENO_PLATFORM.pc_start() + 40);
 pub const MOCK_PC_SRLI_31: ByteAddr = ByteAddr(CENO_PLATFORM.pc_start() + 44);
 pub const MOCK_PC_SLTU: ByteAddr = ByteAddr(CENO_PLATFORM.pc_start() + 48);
+pub const MOCK_PC_ADDI: ByteAddr = ByteAddr(CENO_PLATFORM.pc_start() + 52);
+pub const MOCK_PC_ADDI_SUB: ByteAddr = ByteAddr(CENO_PLATFORM.pc_start() + 56);
 
 #[allow(clippy::enum_variant_names)]
 #[derive(Debug, PartialEq, Clone)]