Skip to content

Commit

Permalink
Feat/#367 SLTI (#453)
Browse files Browse the repository at this point in the history 
To close #367 

Co-authored-by: sm.wu <[email protected]>
  • Loading branch information
@KimiWu123 @hero78119
KimiWu123 and hero78119 authored Oct 28, 2024
1 parent 79bb73b commit 7471ae5
Show file tree
Hide file tree
Showing 9 changed files with 283 additions and 73 deletions.
22 changes: 0 additions & 22 deletions ceno_emul/src/rv32im.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -218,28 +218,6 @@ impl DecodedInstruction {
}
}

#[allow(dead_code)]
pub fn from_raw(kind: InsnKind, rs1: u32, rs2: u32, rd: u32) -> Self {
// limit the range of inputs
let rs2 = rs2 & 0x1f; // 5bits mask
let rs1 = rs1 & 0x1f;
let rd = rd & 0x1f;
let func7 = kind.codes().func7;
let func3 = kind.codes().func3;
let opcode = kind.codes().opcode;
let insn = func7 << 25 | rs2 << 20 | rs1 << 15 | func3 << 12 | rd << 7 | opcode;
Self {
insn,
top_bit: func7 | 0x80,
func7,
rs2,
rs1,
func3,
rd,
opcode,
}
}

pub fn encoded(&self) -> u32 {
self.insn
}
Expand Down
25 changes: 17 additions & 8 deletions ceno_zkvm/src/gadgets/is_lt.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -109,11 +109,23 @@ impl IsLtConfig {
lhs: u64,
rhs: u64,
) -> Result<(), ZKVMError> {
let is_lt = lhs < rhs;
set_val!(instance, self.is_lt, is_lt as u64);
set_val!(instance, self.is_lt, (lhs < rhs) as u64);
self.config.assign_instance(instance, lkm, lhs, rhs)?;
Ok(())
}

pub fn assign_instance_signed<F: SmallField>(
&self,
instance: &mut [MaybeUninit<F>],
lkm: &mut LkMultiplicity,
lhs: SWord,
rhs: SWord,
) -> Result<(), ZKVMError> {
set_val!(instance, self.is_lt, (lhs < rhs) as u64);
self.config
.assign_instance_signed(instance, lkm, lhs, rhs)?;
Ok(())
}
}

#[derive(Debug, Clone)]
Expand Down Expand Up @@ -337,12 +349,9 @@ impl InnerSignedLtConfig {
1,
)?;

// Convert two's complement representation into field arithmetic.
// Example: 0xFFFF_FFFF = 2^32 - 1 --> shift --> -1
let neg_shift = -Expression::Constant((1_u64 << 32).into());
let lhs_value = lhs.value() + is_lhs_neg.expr() * neg_shift.clone();
let rhs_value = rhs.value() + is_rhs_neg.expr() * neg_shift;

// Convert to field arithmetic.
let lhs_value = lhs.to_field_expr(is_lhs_neg.expr());
let rhs_value = rhs.to_field_expr(is_rhs_neg.expr());
let config = InnerLtConfig::construct_circuit(
cb,
format!("{name} (lhs < rhs)"),
Expand Down
3 changes: 3 additions & 0 deletions ceno_zkvm/src/instructions/riscv.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -17,6 +17,7 @@ pub mod mulh;
pub mod shift;
pub mod shift_imm;
pub mod slt;
pub mod slti;
pub mod sltu;

mod b_insn;
Expand All @@ -33,6 +34,8 @@ mod memory;
mod s_insn;
#[cfg(test)]
mod test;
#[cfg(test)]
mod test_utils;

pub trait RIVInstruction {
const INST_KIND: InsnKind;
Expand Down
15 changes: 3 additions & 12 deletions ceno_zkvm/src/instructions/riscv/arith_imm.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -88,21 +88,12 @@ mod test {

use crate::{
circuit_builder::{CircuitBuilder, ConstraintSystem},
instructions::Instruction,
instructions::{Instruction, riscv::test_utils::imm_i},
scheme::mock_prover::{MOCK_PC_START, MockProver},
};

use super::AddiInstruction;

fn imm(imm: i32) -> u32 {
// imm is 12 bits in B-type
const IMM_MAX: i32 = 2i32.pow(12);
if imm.is_negative() {
(IMM_MAX + imm) as u32
} else {
imm as u32
}
}
#[test]
fn test_opcode_addi() {
let mut cs = ConstraintSystem::<GoldilocksExt2>::new(|| "riscv");
Expand All @@ -118,7 +109,7 @@ mod test {
.unwrap()
.unwrap();

let insn_code = encode_rv32(InsnKind::ADDI, 2, 0, 4, imm(3));
let insn_code = encode_rv32(InsnKind::ADDI, 2, 0, 4, imm_i(3));
let (raw_witin, lkm) = AddiInstruction::<GoldilocksExt2>::assign_instances(
&config,
cb.cs.num_witin as usize,
Expand Down Expand Up @@ -162,7 +153,7 @@ mod test {
.unwrap()
.unwrap();

let insn_code = encode_rv32(InsnKind::ADDI, 2, 0, 4, imm(-3));
let insn_code = encode_rv32(InsnKind::ADDI, 2, 0, 4, imm_i(-3));
let (raw_witin, lkm) = AddiInstruction::<GoldilocksExt2>::assign_instances(
&config,
cb.cs.num_witin as usize,
Expand Down
24 changes: 7 additions & 17 deletions ceno_zkvm/src/instructions/riscv/branch/test.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -7,23 +7,13 @@ use super::*;
use crate::{
circuit_builder::{CircuitBuilder, ConstraintSystem},
error::ZKVMError,
instructions::Instruction,
instructions::{Instruction, riscv::test_utils::imm_b},
scheme::mock_prover::{MOCK_PC_START, MockProver},
};

const A: Word = 0xbead1010;
const B: Word = 0xef552020;

fn imm(imm: i32) -> u32 {
// imm is 13 bits in B-type
const IMM_MAX: i32 = 2i32.pow(13);
if imm.is_negative() {
(IMM_MAX + imm) as u32
} else {
imm as u32
}
}

#[test]
fn test_opcode_beq() {
impl_opcode_beq(false);
Expand All @@ -44,7 +34,7 @@ fn impl_opcode_beq(equal: bool) {
.unwrap()
.unwrap();

let insn_code = encode_rv32(InsnKind::BEQ, 2, 3, 0, imm(8));
let insn_code = encode_rv32(InsnKind::BEQ, 2, 3, 0, imm_b(8));
let pc_offset = if equal { 8 } else { PC_STEP_SIZE };
let (raw_witin, lkm) =
BeqInstruction::assign_instances(&config, cb.cs.num_witin as usize, vec![
Expand Down Expand Up @@ -93,7 +83,7 @@ fn impl_opcode_bne(equal: bool) {
.unwrap()
.unwrap();

let insn_code = encode_rv32(InsnKind::BNE, 2, 3, 0, imm(8));
let insn_code = encode_rv32(InsnKind::BNE, 2, 3, 0, imm_b(8));
let pc_offset = if equal { PC_STEP_SIZE } else { 8 };
let (raw_witin, lkm) =
BneInstruction::assign_instances(&config, cb.cs.num_witin as usize, vec![
Expand Down Expand Up @@ -145,7 +135,7 @@ fn impl_bltu_circuit(taken: bool, a: u32, b: u32) -> Result<(), ZKVMError> {
MOCK_PC_START + PC_STEP_SIZE
};

let insn_code = encode_rv32(InsnKind::BLTU, 2, 3, 0, imm(-8));
let insn_code = encode_rv32(InsnKind::BLTU, 2, 3, 0, imm_b(-8));
println!("{:#b}", insn_code);
let (raw_witin, lkm) =
BltuInstruction::assign_instances(&config, circuit_builder.cs.num_witin as usize, vec![
Expand Down Expand Up @@ -198,7 +188,7 @@ fn impl_bgeu_circuit(taken: bool, a: u32, b: u32) -> Result<(), ZKVMError> {
MOCK_PC_START + PC_STEP_SIZE
};

let insn_code = encode_rv32(InsnKind::BGEU, 2, 3, 0, imm(-8));
let insn_code = encode_rv32(InsnKind::BGEU, 2, 3, 0, imm_b(-8));
let (raw_witin, lkm) =
BgeuInstruction::assign_instances(&config, circuit_builder.cs.num_witin as usize, vec![
StepRecord::new_b_instruction(
Expand Down Expand Up @@ -251,7 +241,7 @@ fn impl_blt_circuit(taken: bool, a: i32, b: i32) -> Result<(), ZKVMError> {
MOCK_PC_START + PC_STEP_SIZE
};

let insn_code = encode_rv32(InsnKind::BLT, 2, 3, 0, imm(-8));
let insn_code = encode_rv32(InsnKind::BLT, 2, 3, 0, imm_b(-8));
let (raw_witin, lkm) =
BltInstruction::assign_instances(&config, circuit_builder.cs.num_witin as usize, vec![
StepRecord::new_b_instruction(
Expand Down Expand Up @@ -304,7 +294,7 @@ fn impl_bge_circuit(taken: bool, a: i32, b: i32) -> Result<(), ZKVMError> {
MOCK_PC_START + PC_STEP_SIZE
};

let insn_code = encode_rv32(InsnKind::BGE, 2, 3, 0, imm(-8));
let insn_code = encode_rv32(InsnKind::BGE, 2, 3, 0, imm_b(-8));
let (raw_witin, lkm) =
BgeInstruction::assign_instances(&config, circuit_builder.cs.num_witin as usize, vec![
StepRecord::new_b_instruction(
Expand Down
18 changes: 4 additions & 14 deletions ceno_zkvm/src/instructions/riscv/jump/test.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -5,21 +5,15 @@ use multilinear_extensions::mle::IntoMLEs;

use crate::{
circuit_builder::{CircuitBuilder, ConstraintSystem},
instructions::Instruction,
instructions::{
Instruction,
riscv::test_utils::{imm_j, imm_u},
},
scheme::mock_prover::{MOCK_PC_START, MockProver},
};

use super::{AuipcInstruction, JalInstruction, JalrInstruction, LuiInstruction};

fn imm_j(imm: i32) -> u32 {
// imm is 21 bits in J-type
const IMM_MAX: i32 = 2i32.pow(21);
if imm.is_negative() {
(IMM_MAX + imm) as u32
} else {
imm as u32
}
}
#[test]
fn test_opcode_jal() {
let mut cs = ConstraintSystem::<GoldilocksExt2>::new(|| "riscv");
Expand Down Expand Up @@ -113,10 +107,6 @@ fn test_opcode_jalr() {
);
}

fn imm_u(imm: u32) -> u32 {
// valid imm is imm[12:31] in U-type
imm << 12
}
#[test]
fn test_opcode_lui() {
let mut cs = ConstraintSystem::<GoldilocksExt2>::new(|| "riscv");
Expand Down
Loading

0 comments on commit 7471ae5

Please sign in to comment.