Skip to content

Commit 47f5577

Browse files
hero78119hero78119
committed
left-over: mock prover
1 parent 5d8d86a commit 47f5577

File tree

7 files changed

+299
-159
lines changed

7 files changed

+299
-159
lines changed

‎ceno_zkvm/src/instructions/riscv.rs‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -51,6 +51,6 @@ pub trait RIVInstruction {
5151
pub use arith::{AddInstruction, SubInstruction};
5252
pub use jump::{JalInstruction, JalrInstruction};
5353
pub use memory::{
54-
LbInstruction, LbuInstruction, LhInstruction, LhuInstruction, LwInstruction, SbInstruction,
55-
ShInstruction, SwInstruction,
54+
LbInstruction, LbuInstruction, LhInstruction, LhuInstruction, LoadStoreWordInstruction,
55+
SbInstruction, ShInstruction,
5656
};

‎ceno_zkvm/src/instructions/riscv/insn_base.rs‎

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -117,7 +117,7 @@ impl<E: ExtensionField> ReadRS1<E> {
117117
let id = circuit_builder.create_witin(|| "rs1_id");
118118
let prev_ts = circuit_builder.create_witin(|| "prev_rs1_ts");
119119
circuit_builder
120-
.conditional_rw_selector(is_enable, |circuit_builder| {
120+
.region_selector(is_enable, |circuit_builder| {
121121
let (_, lt_cfg) = circuit_builder.register_read(
122122
|| "read_rs1",
123123
id,
@@ -212,7 +212,7 @@ impl<E: ExtensionField> ReadRS2<E> {
212212
let id = circuit_builder.create_witin(|| "rs2_id");
213213
let prev_ts = circuit_builder.create_witin(|| "prev_rs2_ts");
214214
circuit_builder
215-
.conditional_rw_selector(is_enable, |circuit_builder| {
215+
.region_selector(is_enable, |circuit_builder| {
216216
let (_, lt_cfg) = circuit_builder.register_read(
217217
|| "read_rs2",
218218
id,
@@ -311,7 +311,7 @@ impl<E: ExtensionField> WriteRD<E> {
311311
let prev_ts = circuit_builder.create_witin(|| "prev_rd_ts");
312312
let prev_value = UInt::new_unchecked(|| "prev_rd_value", circuit_builder)?;
313313
circuit_builder
314-
.conditional_rw_selector(is_enable, |circuit_builder| {
314+
.region_selector(is_enable, |circuit_builder| {
315315
let (_, lt_cfg) = circuit_builder.register_write(
316316
|| "write_rd",
317317
id,

‎ceno_zkvm/src/instructions/riscv/memory.rs‎

Lines changed: 1 addition & 14 deletions
Original file line numberDiff line numberDiff line change
@@ -19,21 +19,14 @@ use crate::instructions::riscv::RIVInstruction;
1919
pub use crate::instructions::riscv::memory::load::LoadInstruction;
2020
#[cfg(feature = "u16limb_circuit")]
2121
pub use crate::instructions::riscv::memory::load_v2::LoadInstruction;
22+
pub use crate::instructions::riscv::memory::loadstorew_v2::LoadStoreWordInstruction;
2223
#[cfg(not(feature = "u16limb_circuit"))]
2324
pub use crate::instructions::riscv::memory::store::StoreInstruction;
2425
#[cfg(feature = "u16limb_circuit")]
2526
pub use crate::instructions::riscv::memory::store_v2::StoreInstruction;
2627

2728
use ceno_emul::InsnKind;
2829

29-
pub struct LwOp;
30-
31-
impl RIVInstruction for LwOp {
32-
const INST_KIND: InsnKind = InsnKind::LW;
33-
}
34-
35-
pub type LwInstruction<E> = LoadInstruction<E, LwOp>;
36-
3730
pub struct LhOp;
3831
impl RIVInstruction for LhOp {
3932
const INST_KIND: InsnKind = InsnKind::LH;
@@ -58,12 +51,6 @@ impl RIVInstruction for LbuOp {
5851
}
5952
pub type LbuInstruction<E> = LoadInstruction<E, LbuOp>;
6053

61-
pub struct SWOp;
62-
impl RIVInstruction for SWOp {
63-
const INST_KIND: InsnKind = InsnKind::SW;
64-
}
65-
pub type SwInstruction<E> = StoreInstruction<E, SWOp, 2>;
66-
6754
pub struct SHOp;
6855
impl RIVInstruction for SHOp {
6956
const INST_KIND: InsnKind = InsnKind::SH;

‎ceno_zkvm/src/instructions/riscv/memory/loadstorew_v2.rs‎

Lines changed: 9 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -7,7 +7,6 @@ use crate::{
77
instructions::{
88
Instruction,
99
riscv::{
10-
RIVInstruction,
1110
constants::{MEM_BITS, UInt},
1211
insn_base::{MemAddr, RWMEM, ReadRS1, ReadRS2, StateInOut, WriteRD},
1312
},
@@ -17,7 +16,7 @@ use crate::{
1716
witness::LkMultiplicity,
1817
};
1918
use ceno_emul::{
20-
ByteAddr,
19+
ByteAddr, InsnKind,
2120
InsnKind::{LW, SW},
2221
StepRecord,
2322
};
@@ -48,12 +47,17 @@ pub struct LoadStoreWordConfig<E: ExtensionField> {
4847
mem_rw: RWMEM,
4948
}
5049

51-
pub struct LoadStoreWordInstruction<E, I>(PhantomData<(E, I)>);
52-
impl<E: ExtensionField, I: RIVInstruction> Instruction<E> for LoadStoreWordInstruction<E, I> {
50+
pub struct LoadStoreWordInstruction<E>(PhantomData<E>);
51+
impl<E: ExtensionField> Instruction<E> for LoadStoreWordInstruction<E> {
5352
type InstructionConfig = LoadStoreWordConfig<E>;
53+
type InsnType = InsnKind;
54+
55+
fn inst_kinds() -> &'static [Self::InsnType] {
56+
&[InsnKind::LW, InsnKind::SW]
57+
}
5458

5559
fn name() -> String {
56-
format!("{:?}", I::INST_KIND)
60+
format!("{:?}_{:?}", InsnKind::LW, InsnKind::SW)
5761
}
5862

5963
fn construct_circuit(

‎ceno_zkvm/src/instructions/riscv/memory/test.rs‎

Lines changed: 134 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,5 @@
1+
#[cfg(feature = "u16limb_circuit")]
2+
use crate::instructions::riscv::memory::LoadStoreWordInstruction;
13
use crate::{
24
Value,
35
circuit_builder::{CircuitBuilder, ConstraintSystem},
@@ -7,16 +9,15 @@ use crate::{
79
riscv::{
810
LbInstruction, LbuInstruction, LhInstruction, LhuInstruction, RIVInstruction,
911
constants::UInt,
10-
memory::{
11-
LbOp, LbuOp, LhOp, LhuOp, LwInstruction, LwOp, SBOp, SHOp, SWOp, SbInstruction,
12-
ShInstruction, SwInstruction,
13-
},
12+
memory::{LbOp, LbuOp, LhOp, LhuOp, SBOp, SHOp, SbInstruction, ShInstruction},
1413
},
1514
},
1615
scheme::mock_prover::{MOCK_PC_START, MockProver},
1716
structs::ProgramParams,
1817
};
19-
use ceno_emul::{ByteAddr, Change, InsnKind, ReadOp, StepRecord, Word, WriteOp, encode_rv32};
18+
use ceno_emul::{
19+
ByteAddr, Change, InsnKind, InsnKind::SW, ReadOp, StepRecord, Word, WriteOp, encode_rv32,
20+
};
2021
#[cfg(feature = "u16limb_circuit")]
2122
use ff_ext::BabyBearExt4;
2223
use ff_ext::{ExtensionField, GoldilocksExt2};
@@ -139,6 +140,100 @@ fn impl_opcode_store<E: ExtensionField + Hash, I: RIVInstruction, Inst: Instruct
139140
MockProver::assert_satisfied_raw(&cb, raw_witin, &[insn_code], None, Some(lkm));
140141
}
141142

143+
#[cfg(feature = "u16limb_circuit")]
144+
fn impl_opcode_store_word_dynamic<E: ExtensionField + Hash, Inst: Instruction<E>>(
145+
imm: i32,
146+
is_load: bool,
147+
) {
148+
let mut cs = ConstraintSystem::<E>::new(|| "riscv");
149+
let mut cb = CircuitBuilder::new(&mut cs);
150+
let config = cb
151+
.namespace(
152+
|| Inst::name(),
153+
|cb| {
154+
let config = Inst::construct_circuit(cb, &ProgramParams::default());
155+
Ok(config)
156+
},
157+
)
158+
.unwrap()
159+
.unwrap();
160+
161+
let insn_kind = if is_load { InsnKind::LW } else { SW };
162+
let insn_code = encode_rv32(insn_kind, 2, 3, 0, imm);
163+
let rs1_word = Word::from(0x4000000_u32);
164+
let unaligned_addr = ByteAddr::from(rs1_word.wrapping_add_signed(imm));
165+
166+
if is_load {
167+
let mem_value = 0x40302010;
168+
let prev_rd_word = Word::from(0x12345678_u32);
169+
let new_rd_word = load(mem_value, InsnKind::LW, unaligned_addr.shift());
170+
let rd_change = Change {
171+
before: prev_rd_word,
172+
after: new_rd_word,
173+
};
174+
let (raw_witin, lkm) = Inst::assign_instances(
175+
&config,
176+
&mut ShardContext::default(),
177+
cb.cs.num_witin as usize,
178+
cb.cs.num_structural_witin as usize,
179+
&[StepRecord::new_im_instruction(
180+
12,
181+
MOCK_PC_START,
182+
insn_code,
183+
rs1_word,
184+
rd_change,
185+
ReadOp {
186+
addr: unaligned_addr.waddr(),
187+
value: mem_value,
188+
previous_cycle: 4,
189+
},
190+
8,
191+
)],
192+
)
193+
.unwrap();
194+
MockProver::assert_satisfied_raw(&cb, raw_witin, &[insn_code], None, Some(lkm));
195+
} else {
196+
let prev_mem_value = 0x40302010;
197+
let rs2_word = Word::from(0x12345678_u32);
198+
let new_mem_value = sw(prev_mem_value, rs2_word);
199+
let (raw_witin, lkm) = Inst::assign_instances(
200+
&config,
201+
&mut ShardContext::default(),
202+
cb.cs.num_witin as usize,
203+
cb.cs.num_structural_witin as usize,
204+
&[StepRecord::new_s_instruction(
205+
12,
206+
MOCK_PC_START,
207+
insn_code,
208+
rs1_word,
209+
rs2_word,
210+
WriteOp {
211+
addr: unaligned_addr.waddr(),
212+
value: Change {
213+
before: prev_mem_value,
214+
after: new_mem_value,
215+
},
216+
previous_cycle: 4,
217+
},
218+
8,
219+
)],
220+
)
221+
.unwrap();
222+
223+
let expected_mem_written =
224+
UInt::from_const_unchecked(Value::new_unchecked(new_mem_value).as_u16_limbs().to_vec());
225+
let mem_written_expr = cb.get_debug_expr(DebugIndex::MemWrite as usize)[0].clone();
226+
cb.require_equal(
227+
|| "assert_mem_written",
228+
mem_written_expr,
229+
expected_mem_written.value(),
230+
)
231+
.unwrap();
232+
233+
MockProver::assert_satisfied_raw(&cb, raw_witin, &[insn_code], None, Some(lkm));
234+
}
235+
}
236+
142237
fn impl_opcode_load<E: ExtensionField + Hash, I: RIVInstruction, Inst: Instruction<E>>(imm: i32) {
143238
let mut cs = ConstraintSystem::<E>::new(|| "riscv");
144239
let mut cb = CircuitBuilder::new(&mut cs);
@@ -196,11 +291,40 @@ fn impl_opcode_sh(imm: i32) {
196291
impl_opcode_store::<GoldilocksExt2, SHOp, ShInstruction<GoldilocksExt2>>(imm)
197292
}
198293

294+
#[cfg(not(feature = "u16limb_circuit"))]
199295
fn impl_opcode_sw(imm: i32) {
200296
assert_eq!(imm & 0x03, 0);
201297
impl_opcode_store::<GoldilocksExt2, SWOp, SwInstruction<GoldilocksExt2>>(imm)
202298
}
203299

300+
#[cfg(feature = "u16limb_circuit")]
301+
fn impl_opcode_sw(imm: i32) {
302+
assert_eq!(imm & 0x03, 0);
303+
impl_opcode_store_word_dynamic::<GoldilocksExt2, LoadStoreWordInstruction<GoldilocksExt2>>(
304+
imm, false,
305+
);
306+
}
307+
308+
#[cfg(feature = "u16limb_circuit")]
309+
fn impl_opcode_sw_u16(imm: i32) {
310+
impl_opcode_store_word_dynamic::<BabyBearExt4, LoadStoreWordInstruction<BabyBearExt4>>(
311+
imm, false,
312+
);
313+
}
314+
315+
fn impl_opcode_lw(imm: i32) {
316+
assert_eq!(imm & 0x03, 0);
317+
impl_opcode_store_word_dynamic::<GoldilocksExt2, LoadStoreWordInstruction<GoldilocksExt2>>(
318+
imm, true,
319+
);
320+
}
321+
322+
fn impl_opcode_lw_u16(imm: i32) {
323+
impl_opcode_store_word_dynamic::<BabyBearExt4, LoadStoreWordInstruction<BabyBearExt4>>(
324+
imm, true,
325+
);
326+
}
327+
204328
#[test]
205329
fn test_sb() {
206330
let cases = vec![(0,), (5,), (10,), (15,), (-4,), (-3,), (-2,), (-1,)];
@@ -230,7 +354,7 @@ fn test_sw() {
230354
for &(imm,) in &cases {
231355
impl_opcode_sw(imm);
232356
#[cfg(feature = "u16limb_circuit")]
233-
impl_opcode_sw(imm);
357+
impl_opcode_sw_u16(imm);
234358
}
235359
}
236360

@@ -319,8 +443,9 @@ fn test_lw() {
319443
let cases = vec![(0,), (4,), (-4,)];
320444

321445
for &(imm,) in &cases {
322-
impl_opcode_load::<GoldilocksExt2, LwOp, LwInstruction<GoldilocksExt2>>(imm);
323-
#[cfg(feature = "u16limb_circuit")]
324-
impl_opcode_load::<BabyBearExt4, LwOp, LwInstruction<BabyBearExt4>>(imm);
446+
{
447+
impl_opcode_lw(imm);
448+
impl_opcode_lw_u16(imm);
449+
}
325450
}
326451
}

0 commit comments

Comments
 (0)