Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Dummy Circuit - Basic ECALL #369

Merged
merged 6 commits into from
Nov 8, 2024
Merged
Show file tree
Hide file tree
Changes from 5 commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
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, InsnCodes, InsnFormat, InsnKind};
pub use rv32im::{DecodedInstruction, EmuContext, InsnCategory, InsnCodes, InsnFormat, InsnKind};

mod elf;
pub use elf::Program;
Expand Down
3 changes: 3 additions & 0 deletions ceno_emul/src/platform.rs
Original file line number Diff line number Diff line change
Expand Up @@ -11,13 +11,16 @@ pub struct Platform {
pub rom_end: Addr,
pub ram_start: Addr,
pub ram_end: Addr,
/// If true, ecall instructions are no-op instead of trap. Testing only.
pub unsafe_ecall_nop: bool,
}

pub const CENO_PLATFORM: Platform = Platform {
rom_start: 0x2000_0000,
rom_end: 0x3000_0000 - 1,
ram_start: 0x8000_0000,
ram_end: 0xFFFF_FFFF,
unsafe_ecall_nop: false,
};

impl Platform {
Expand Down
4 changes: 2 additions & 2 deletions ceno_emul/src/rv32im.rs
Original file line number Diff line number Diff line change
Expand Up @@ -111,7 +111,7 @@ pub struct DecodedInstruction {
}

#[derive(Clone, Copy, Debug)]
enum InsnCategory {
pub enum InsnCategory {
Compute,
Branch,
Load,
Expand Down Expand Up @@ -196,7 +196,7 @@ impl InsnKind {
pub struct InsnCodes {
pub format: InsnFormat,
pub kind: InsnKind,
category: InsnCategory,
pub category: InsnCategory,
pub(crate) opcode: u32,
pub(crate) func3: u32,
pub(crate) func7: u32,
Expand Down
25 changes: 24 additions & 1 deletion ceno_emul/src/tracer.rs
Original file line number Diff line number Diff line change
@@ -1,8 +1,9 @@
use std::{collections::HashMap, fmt, mem};

use crate::{
CENO_PLATFORM, PC_STEP_SIZE,
CENO_PLATFORM, InsnKind, PC_STEP_SIZE,
addr::{ByteAddr, Cycle, RegIdx, Word, WordAddr},
encode_rv32,
rv32im::DecodedInstruction,
};

Expand Down Expand Up @@ -187,6 +188,28 @@ impl StepRecord {
)
}

/// Create a test record for an ECALL instruction that does NOP.
pub fn new_ecall_nop(
cycle: Cycle,
pc: ByteAddr,
ecall_id: Word,
previous_cycle: Cycle,
) -> StepRecord {
StepRecord {
cycle,
pc: Change::new(pc, pc + PC_STEP_SIZE),
insn_code: encode_rv32(InsnKind::EANY, 0, 0, 0, 0),
rs1: Some(ReadOp {
addr: CENO_PLATFORM.register_vma(CENO_PLATFORM.reg_ecall()).into(),
value: ecall_id,
previous_cycle,
}),
rs2: None,
rd: None,
memory_op: None,
}
}

#[allow(clippy::too_many_arguments)]
fn new_insn(
cycle: Cycle,
Expand Down
7 changes: 6 additions & 1 deletion ceno_emul/src/vm_state.rs
Original file line number Diff line number Diff line change
Expand Up @@ -2,7 +2,7 @@ use std::collections::HashMap;

use super::rv32im::EmuContext;
use crate::{
Program,
PC_STEP_SIZE, Program,
addr::{ByteAddr, RegIdx, Word, WordAddr},
platform::Platform,
rv32im::{DecodedInstruction, Emulator, TrapCause},
Expand Down Expand Up @@ -123,6 +123,11 @@ impl EmuContext for VMState {

self.halt();
Ok(true)
} else if self.platform.unsafe_ecall_nop {
// Treat unknown ecalls as NOP.
tracing::warn!("ecall ignored: syscall_id={}", function);
self.set_pc(ByteAddr(self.pc) + PC_STEP_SIZE);
Ok(true)
} else {
self.trap(TrapCause::EcallError)
}
Expand Down
1 change: 1 addition & 0 deletions ceno_zkvm/src/instructions/riscv.rs
Original file line number Diff line number Diff line change
Expand Up @@ -9,6 +9,7 @@ pub mod branch;
pub mod config;
pub mod constants;
pub mod divu;
pub mod dummy;
pub mod ecall;
pub mod jump;
pub mod logic;
Expand Down
19 changes: 19 additions & 0 deletions ceno_zkvm/src/instructions/riscv/divu.rs
Original file line number Diff line number Diff line change
Expand Up @@ -4,6 +4,7 @@ use ff_ext::ExtensionField;
use super::{
RIVInstruction,
constants::{UINT_LIMBS, UInt},
dummy::DummyInstruction,
r_insn::RInstructionConfig,
};
use crate::{
Expand Down Expand Up @@ -33,12 +34,30 @@ pub struct ArithConfig<E: ExtensionField> {

pub struct ArithInstruction<E, I>(PhantomData<(E, I)>);

pub struct DivOp;
impl RIVInstruction for DivOp {
const INST_KIND: InsnKind = InsnKind::DIV;
}
pub type DivDummy<E> = DummyInstruction<E, DivOp>; // TODO: implement DivInstruction.

pub struct DivUOp;
impl RIVInstruction for DivUOp {
const INST_KIND: InsnKind = InsnKind::DIVU;
}
pub type DivUInstruction<E> = ArithInstruction<E, DivUOp>;

pub struct RemOp;
impl RIVInstruction for RemOp {
const INST_KIND: InsnKind = InsnKind::REM;
}
pub type RemDummy<E> = DummyInstruction<E, RemOp>; // TODO: implement RemInstruction.

pub struct RemuOp;
impl RIVInstruction for RemuOp {
const INST_KIND: InsnKind = InsnKind::REMU;
}
pub type RemuDummy<E> = DummyInstruction<E, RemuOp>; // TODO: implement RemuInstruction.

impl<E: ExtensionField, I: RIVInstruction> Instruction<E> for ArithInstruction<E, I> {
type InstructionConfig = ArithConfig<E>;

Expand Down
236 changes: 236 additions & 0 deletions ceno_zkvm/src/instructions/riscv/dummy/dummy_circuit.rs
Original file line number Diff line number Diff line change
@@ -0,0 +1,236 @@
use std::marker::PhantomData;

use ceno_emul::{InsnCategory, InsnCodes, InsnFormat, InsnKind, StepRecord};
use ff_ext::ExtensionField;

use super::super::{
RIVInstruction,
constants::UInt,
insn_base::{ReadMEM, ReadRS1, ReadRS2, StateInOut, WriteMEM, WriteRD},
};
use crate::{
circuit_builder::CircuitBuilder,
error::ZKVMError,
expression::{ToExpr, WitIn},
instructions::Instruction,
set_val,
tables::InsnRecord,
uint::Value,
utils::i64_to_base,
witness::LkMultiplicity,
};
use core::mem::MaybeUninit;

/// DummyInstruction can handle any instruction and produce its side-effects.
pub struct DummyInstruction<E, I>(PhantomData<(E, I)>);

impl<E: ExtensionField, I: RIVInstruction> Instruction<E> for DummyInstruction<E, I> {
type InstructionConfig = DummyConfig<E>;

fn name() -> String {
format!("{:?}_DUMMY", I::INST_KIND)
}

fn construct_circuit(
circuit_builder: &mut CircuitBuilder<E>,
) -> Result<Self::InstructionConfig, ZKVMError> {
DummyConfig::construct_circuit(circuit_builder, I::INST_KIND.codes())
}

fn assign_instance(
config: &Self::InstructionConfig,
instance: &mut [MaybeUninit<<E as ExtensionField>::BaseField>],
lk_multiplicity: &mut LkMultiplicity,
step: &StepRecord,
) -> Result<(), ZKVMError> {
config.assign_instance(instance, lk_multiplicity, step)
}
}

#[derive(Debug)]
pub struct DummyConfig<E: ExtensionField> {
vm_state: StateInOut<E>,

rs1: Option<(ReadRS1<E>, UInt<E>)>,
rs2: Option<(ReadRS2<E>, UInt<E>)>,
rd: Option<(WriteRD<E>, UInt<E>)>,

mem_addr_val: Option<[WitIn; 3]>,
mem_read: Option<ReadMEM<E>>,
mem_write: Option<WriteMEM>,

imm: WitIn,
}

impl<E: ExtensionField> DummyConfig<E> {
fn construct_circuit(
circuit_builder: &mut CircuitBuilder<E>,
codes: InsnCodes,
) -> Result<Self, ZKVMError> {
let (with_rs1, with_rs2, with_rd) = match (codes.format, codes.kind) {
// ECALL reads its syscall_id, then do nothing.
(_, InsnKind::EANY) => (true, false, false),
// Regular instructions do what is implied by their format.
(InsnFormat::R, _) => (true, true, true),
(InsnFormat::I, _) => (true, false, true),
(InsnFormat::S, _) => (true, true, false),
(InsnFormat::B, _) => (true, true, false),
(InsnFormat::U, _) => (false, false, true),
(InsnFormat::J, _) => (false, false, true),
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Maybe we can get rid of them as opcodes that are not supported (i.e. DIV / REM / REMU) right now belong to the R category.

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Yes we have implemented almost everything in the mean time 😄 . Maybe there will be other use-cases: test, benchmarks, demos ?

};
let with_mem_write = matches!(codes.category, InsnCategory::Store);
let with_mem_read = matches!(codes.category, InsnCategory::Load);
let branching = matches!(codes.category, InsnCategory::Branch)
kunxian-xia marked this conversation as resolved.
Show resolved Hide resolved
|| matches!(codes.kind, InsnKind::JAL | InsnKind::JALR);

// State in and out
let vm_state = StateInOut::construct_circuit(circuit_builder, branching)?;

// Registers
let rs1 = if with_rs1 {
let rs1_read = UInt::new_unchecked(|| "rs1_read", circuit_builder)?;
let rs1_op =
ReadRS1::construct_circuit(circuit_builder, rs1_read.register_expr(), vm_state.ts)?;
Some((rs1_op, rs1_read))
} else {
None
};

let rs2 = if with_rs2 {
let rs2_read = UInt::new_unchecked(|| "rs2_read", circuit_builder)?;
let rs2_op =
ReadRS2::construct_circuit(circuit_builder, rs2_read.register_expr(), vm_state.ts)?;
Some((rs2_op, rs2_read))
} else {
None
};

let rd = if with_rd {
let rd_written = UInt::new_unchecked(|| "rd_written", circuit_builder)?;
let rd_op = WriteRD::construct_circuit(
circuit_builder,
rd_written.register_expr(),
vm_state.ts,
)?;
Some((rd_op, rd_written))
} else {
None
};

// Memory
let mem_addr_val = if with_mem_read || with_mem_write {
Some([
circuit_builder.create_witin(|| "mem_addr"),
circuit_builder.create_witin(|| "mem_before"),
circuit_builder.create_witin(|| "mem_after"),
])
} else {
None
};

let mem_read = if with_mem_read {
Some(ReadMEM::construct_circuit(
circuit_builder,
mem_addr_val.as_ref().unwrap()[0].expr(),
mem_addr_val.as_ref().unwrap()[1].expr(),
vm_state.ts,
)?)
} else {
None
};

let mem_write = if with_mem_write {
Some(WriteMEM::construct_circuit(
circuit_builder,
mem_addr_val.as_ref().unwrap()[0].expr(),
mem_addr_val.as_ref().unwrap()[1].expr(),
mem_addr_val.as_ref().unwrap()[2].expr(),
vm_state.ts,
)?)
} else {
None
};

// Fetch instruction

// The register IDs of ECALL is fixed, not encoded.
let rs1_id = match (&rs1, codes.kind) {
(None, _) | (_, InsnKind::EANY) => 0.into(),
(Some((r, _)), _) => r.id.expr(),
};

let imm = circuit_builder.create_witin(|| "imm");

circuit_builder.lk_fetch(&InsnRecord::new(
vm_state.pc.expr(),
codes.kind.into(),
rd.as_ref().map(|(r, _)| r.id.expr()),
rs1_id,
rs2.as_ref().map(|(r, _)| r.id.expr()).unwrap_or(0.into()),
imm.expr(),
))?;

Ok(DummyConfig {
vm_state,
rs1,
rs2,
rd,
mem_addr_val,
mem_read,
mem_write,
imm,
})
}

fn assign_instance(
&self,
instance: &mut [MaybeUninit<<E as ExtensionField>::BaseField>],
lk_multiplicity: &mut LkMultiplicity,
step: &StepRecord,
) -> Result<(), ZKVMError> {
// State in and out
self.vm_state.assign_instance(instance, step)?;

// Fetch instruction
lk_multiplicity.fetch(step.pc().before.0);

// Registers
if let Some((rs1_op, rs1_read)) = &self.rs1 {
naure marked this conversation as resolved.
Show resolved Hide resolved
rs1_op.assign_instance(instance, lk_multiplicity, step)?;

let rs1_val = Value::new_unchecked(step.rs1().expect("rs1 value").value);
rs1_read.assign_value(instance, rs1_val);
}
if let Some((rs2_op, rs2_read)) = &self.rs2 {
rs2_op.assign_instance(instance, lk_multiplicity, step)?;

let rs2_val = Value::new_unchecked(step.rs2().expect("rs2 value").value);
rs2_read.assign_value(instance, rs2_val);
}
if let Some((rd_op, rd_written)) = &self.rd {
rd_op.assign_instance(instance, lk_multiplicity, step)?;

let rd_val = Value::new_unchecked(step.rd().expect("rd value").value.after);
rd_written.assign_value(instance, rd_val);
}

// Memory
if let Some([mem_addr, mem_before, mem_after]) = &self.mem_addr_val {
let mem_op = step.memory_op().expect("memory operation");
set_val!(instance, mem_addr, u64::from(mem_op.addr));
set_val!(instance, mem_before, mem_op.value.before as u64);
set_val!(instance, mem_after, mem_op.value.after as u64);
}
if let Some(mem_read) = &self.mem_read {
mem_read.assign_instance(instance, lk_multiplicity, step)?;
}
if let Some(mem_write) = &self.mem_write {
mem_write.assign_instance::<E>(instance, lk_multiplicity, step)?;
}

let imm = i64_to_base::<E::BaseField>(InsnRecord::imm_internal(&step.insn()));
set_val!(instance, self.imm, imm);

Ok(())
}
}
Loading
Loading