Skip to content

Commit

Permalink
Common circuit for R-Instructions (#231)
Browse files Browse the repository at this point in the history
_Issues #121, #133, #134, #123, …_

Extract generic instruction handling out of the Add/Sub circuit.

---------

Co-authored-by: Aurélien Nicolas <[email protected]>
  • Loading branch information
naure and Aurélien Nicolas authored Sep 17, 2024
1 parent b300e9b commit 1637f4c
Show file tree
Hide file tree
Showing 11 changed files with 332 additions and 306 deletions.
2 changes: 2 additions & 0 deletions Cargo.lock

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

2 changes: 2 additions & 0 deletions ceno_emul/Cargo.toml
Original file line number Diff line number Diff line change
Expand Up @@ -6,6 +6,8 @@ license.workspace = true

[dependencies]
anyhow = { version = "1.0", default-features = false }
strum = "0.25.0"
strum_macros = "0.25.3"
tracing = { version = "0.1", default-features = false, features = [
"attributes",
] }
Expand Down
2 changes: 1 addition & 1 deletion ceno_emul/src/lib.rs
Original file line number Diff line number Diff line change
Expand Up @@ -11,7 +11,7 @@ mod vm_state;
pub use vm_state::VMState;

mod rv32im;
pub use rv32im::{DecodedInstruction, EmuContext, InsnCategory, InsnKind};
pub use rv32im::{DecodedInstruction, EmuContext, InsnCodes, InsnCategory, InsnKind};

mod elf;
pub use elf::Program;
30 changes: 23 additions & 7 deletions ceno_emul/src/rv32im.rs
Original file line number Diff line number Diff line change
Expand Up @@ -16,6 +16,7 @@

use anyhow::{anyhow, Result};
use std::sync::OnceLock;
use strum_macros::EnumIter;

use super::addr::{ByteAddr, RegIdx, Word, WordAddr, WORD_SIZE};

Expand Down Expand Up @@ -121,7 +122,7 @@ pub enum InsnCategory {
Invalid,
}

#[derive(Clone, Copy, Debug, PartialEq)]
#[derive(Clone, Copy, Debug, PartialEq, EnumIter)]
#[allow(clippy::upper_case_acronyms)]
pub enum InsnKind {
INVALID,
Expand Down Expand Up @@ -174,8 +175,14 @@ pub enum InsnKind {
MRET,
}

impl InsnKind {
pub const fn codes(self) -> InsnCodes {
RV32IM_ISA[self as usize]
}
}

#[derive(Clone, Copy, Debug)]
struct FastDecodeEntry {
pub struct InsnCodes {
pub kind: InsnKind,
category: InsnCategory,
pub opcode: u32,
Expand Down Expand Up @@ -269,8 +276,8 @@ const fn insn(
opcode: u32,
func3: i32,
func7: i32,
) -> FastDecodeEntry {
FastDecodeEntry {
) -> InsnCodes {
InsnCodes {
kind,
category,
opcode,
Expand All @@ -279,7 +286,7 @@ const fn insn(
}
}

type InstructionTable = [FastDecodeEntry; 48];
type InstructionTable = [InsnCodes; 48];
type FastInstructionTable = [u8; 1 << 10];

const RV32IM_ISA: InstructionTable = [
Expand Down Expand Up @@ -333,6 +340,15 @@ const RV32IM_ISA: InstructionTable = [
insn(InsnKind::MRET, InsnCategory::System, 0x73, 0x0, 0x18),
];

#[cfg(test)]
#[test]
fn test_isa_table() {
use strum::IntoEnumIterator;
for kind in InsnKind::iter() {
assert_eq!(kind.codes().kind, kind);
}
}

// RISC-V instruction are determined by 3 parts:
// - Opcode: 7 bits
// - Func3: 3 bits
Expand Down Expand Up @@ -373,7 +389,7 @@ impl FastDecodeTable {
((op_high << 5) | (func72bits << 3) | func3) as usize
}

fn add_insn(table: &mut FastInstructionTable, insn: &FastDecodeEntry, isa_idx: usize) {
fn add_insn(table: &mut FastInstructionTable, insn: &InsnCodes, isa_idx: usize) {
let op_high = insn.opcode >> 2;
if (insn.func3 as i32) < 0 {
for f3 in 0..8 {
Expand All @@ -392,7 +408,7 @@ impl FastDecodeTable {
}
}

fn lookup(&self, decoded: &DecodedInstruction) -> FastDecodeEntry {
fn lookup(&self, decoded: &DecodedInstruction) -> InsnCodes {
let isa_idx = self.table[Self::map10(decoded.opcode, decoded.func3, decoded.func7)];
RV32IM_ISA[isa_idx as usize]
}
Expand Down
10 changes: 5 additions & 5 deletions ceno_zkvm/src/chip_handler.rs
Original file line number Diff line number Diff line change
Expand Up @@ -18,23 +18,23 @@ pub trait GlobalStateRegisterMachineChipOperations<E: ExtensionField> {
}

pub trait RegisterChipOperations<E: ExtensionField, NR: Into<String>, N: FnOnce() -> NR> {
fn register_read<V: ToExpr<E, Output = Vec<Expression<E>>>>(
fn register_read(
&mut self,
name_fn: N,
register_id: &WitIn,
prev_ts: Expression<E>,
ts: Expression<E>,
values: &V,
values: &impl ToExpr<E, Output = Vec<Expression<E>>>,
) -> Result<(Expression<E>, ExprLtConfig), ZKVMError>;

#[allow(clippy::too_many_arguments)]
fn register_write<V: ToExpr<E, Output = Vec<Expression<E>>>>(
fn register_write(
&mut self,
name_fn: N,
register_id: &WitIn,
prev_ts: Expression<E>,
ts: Expression<E>,
prev_values: &V,
values: &V,
prev_values: &impl ToExpr<E, Output = Vec<Expression<E>>>,
values: &impl ToExpr<E, Output = Vec<Expression<E>>>,
) -> Result<(Expression<E>, ExprLtConfig), ZKVMError>;
}
10 changes: 5 additions & 5 deletions ceno_zkvm/src/chip_handler/register.rs
Original file line number Diff line number Diff line change
Expand Up @@ -13,13 +13,13 @@ use super::RegisterChipOperations;
impl<'a, E: ExtensionField, NR: Into<String>, N: FnOnce() -> NR> RegisterChipOperations<E, NR, N>
for CircuitBuilder<'a, E>
{
fn register_read<V: ToExpr<E, Output = Vec<Expression<E>>>>(
fn register_read(
&mut self,
name_fn: N,
register_id: &WitIn,
prev_ts: Expression<E>,
ts: Expression<E>,
values: &V,
values: &impl ToExpr<E, Output = Vec<Expression<E>>>,
) -> Result<(Expression<E>, ExprLtConfig), ZKVMError> {
self.namespace(name_fn, |cb| {
// READ (a, v, t)
Expand Down Expand Up @@ -58,14 +58,14 @@ impl<'a, E: ExtensionField, NR: Into<String>, N: FnOnce() -> NR> RegisterChipOpe
})
}

fn register_write<V: ToExpr<E, Output = Vec<Expression<E>>>>(
fn register_write(
&mut self,
name_fn: N,
register_id: &WitIn,
prev_ts: Expression<E>,
ts: Expression<E>,
prev_values: &V,
values: &V,
prev_values: &impl ToExpr<E, Output = Vec<Expression<E>>>,
values: &impl ToExpr<E, Output = Vec<Expression<E>>>,
) -> Result<(Expression<E>, ExprLtConfig), ZKVMError> {
self.namespace(name_fn, |cb| {
// READ (a, v, t)
Expand Down
10 changes: 4 additions & 6 deletions ceno_zkvm/src/instructions/riscv.rs
Original file line number Diff line number Diff line change
@@ -1,16 +1,14 @@
use constants::OpcodeType;
use ff_ext::ExtensionField;

use super::Instruction;
use ceno_emul::InsnKind;

pub mod addsub;
pub mod blt;
pub mod config;
pub mod constants;
mod r_insn;

#[cfg(test)]
mod test;

pub trait RIVInstruction<E: ExtensionField>: Instruction<E> {
const OPCODE_TYPE: OpcodeType;
pub trait RIVInstruction {
const INST_KIND: InsnKind;
}
Loading

0 comments on commit 1637f4c

Please sign in to comment.