Skip to content

Commit 666276b

Browse files
author
Yoichi Hirai
authored
Use program memory checking in many chips (#369)
1 parent 369f6aa commit 666276b

File tree

14 files changed

+174
-54
lines changed

14 files changed

+174
-54
lines changed

‎prover/src/chips/add.rs‎

Lines changed: 7 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -132,7 +132,7 @@ impl MachineChip for AddChip {
132132
#[cfg(test)]
133133
mod test {
134134
use crate::{
135-
chips::{CpuChip, RegisterMemCheckChip},
135+
chips::{CpuChip, ProgramMemCheckChip, RegisterMemCheckChip},
136136
test_utils::assert_chip,
137137
trace::{
138138
preprocessed::PreprocessedBuilder, program::iter_program_steps,
@@ -142,6 +142,7 @@ mod test {
142142

143143
use super::*;
144144
use nexus_vm::{
145+
emulator::{Emulator, HarvardEmulator},
145146
riscv::{BasicBlock, BuiltinOpcode, Instruction, InstructionType, Opcode},
146147
trace::k_trace_direct,
147148
};
@@ -193,17 +194,19 @@ mod test {
193194

194195
#[test]
195196
fn test_k_trace_constrained_add_instructions() {
196-
type Chips = (CpuChip, AddChip, RegisterMemCheckChip);
197+
type Chips = (CpuChip, AddChip, RegisterMemCheckChip, ProgramMemCheckChip);
197198
let basic_block = setup_basic_block_ir();
198199
let k = 1;
199200

200201
// Get traces from VM K-Trace interface
201202
let vm_traces = k_trace_direct(&basic_block, k).expect("Failed to create trace");
203+
let emulator = HarvardEmulator::from_basic_blocks(&basic_block);
204+
let program_memory = emulator.get_program_memory();
202205

203206
// Trace circuit
204207
let mut traces = TracesBuilder::new(LOG_SIZE);
205208
let program_steps = iter_program_steps(&vm_traces, traces.num_rows());
206-
let program_trace = ProgramTraces::dummy(LOG_SIZE); // TODO: replace this dummy with real program
209+
let program_trace = ProgramTraces::new(LOG_SIZE, program_memory);
207210
let mut side_note = SideNote::new(&program_trace);
208211

209212
for (row_idx, program_step) in program_steps.enumerate() {
@@ -220,6 +223,6 @@ mod test {
220223
preprocessed_column.fill_is_first32();
221224
preprocessed_column.fill_row_idx();
222225
preprocessed_column.fill_timestamps();
223-
assert_chip::<Chips>(traces, Some(preprocessed_column), None);
226+
assert_chip::<Chips>(traces, Some(preprocessed_column), Some(program_trace));
224227
}
225228
}

‎prover/src/chips/auipc.rs‎

Lines changed: 11 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -107,13 +107,14 @@ impl MachineChip for AuipcChip {
107107
#[cfg(test)]
108108
mod test {
109109
use crate::{
110-
chips::{CpuChip, RegisterMemCheckChip},
110+
chips::{CpuChip, ProgramMemCheckChip, RegisterMemCheckChip},
111111
test_utils::assert_chip,
112112
trace::{program::iter_program_steps, program_trace::ProgramTraces, PreprocessedTraces},
113113
};
114114

115115
use super::*;
116116
use nexus_vm::{
117+
emulator::{Emulator, HarvardEmulator},
117118
riscv::{BasicBlock, BuiltinOpcode, Instruction, InstructionType, Opcode},
118119
trace::k_trace_direct,
119120
};
@@ -148,16 +149,23 @@ mod test {
148149

149150
#[test]
150151
fn test_k_trace_constrained_auipc_instructions() {
151-
type Chips = (CpuChip, AuipcChip, RegisterMemCheckChip);
152+
type Chips = (
153+
CpuChip,
154+
AuipcChip,
155+
ProgramMemCheckChip,
156+
RegisterMemCheckChip,
157+
);
152158
let basic_block = setup_basic_block_ir();
153159
let k = 1;
154160

155161
// Get traces from VM K-Trace interface
156162
let vm_traces = k_trace_direct(&basic_block, k).expect("Failed to create trace");
163+
let emulator = HarvardEmulator::from_basic_blocks(&basic_block);
164+
let program_memory = emulator.get_program_memory();
157165

158166
// Trace circuit
159167
let mut traces = TracesBuilder::new(LOG_SIZE);
160-
let program_traces = ProgramTraces::dummy(LOG_SIZE);
168+
let program_traces = ProgramTraces::new(LOG_SIZE, program_memory);
161169
let mut side_note = SideNote::new(&program_traces);
162170
let program_steps = iter_program_steps(&vm_traces, traces.num_rows());
163171

‎prover/src/chips/beq.rs‎

Lines changed: 15 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -263,7 +263,7 @@ impl MachineChip for BeqChip {
263263
#[cfg(test)]
264264
mod test {
265265
use crate::{
266-
chips::{AddChip, CpuChip, RegisterMemCheckChip, SubChip},
266+
chips::{AddChip, CpuChip, ProgramMemCheckChip, RegisterMemCheckChip, SubChip},
267267
test_utils::assert_chip,
268268
trace::{
269269
preprocessed::PreprocessedBuilder,
@@ -274,11 +274,12 @@ mod test {
274274

275275
use super::*;
276276
use nexus_vm::{
277+
emulator::{Emulator, HarvardEmulator},
277278
riscv::{BasicBlock, BuiltinOpcode, Instruction, InstructionType, Opcode},
278279
trace::k_trace_direct,
279280
};
280281

281-
const LOG_SIZE: u32 = PreprocessedBuilder::MIN_LOG_SIZE;
282+
const LOG_SIZE: u32 = 8; // PreprocessedBuilder::MIN_LOG_SIZE; makes the test more than a minute long.
282283

283284
#[rustfmt::skip]
284285
fn setup_basic_block_ir() -> Vec<BasicBlock> {
@@ -324,16 +325,25 @@ mod test {
324325

325326
#[test]
326327
fn test_k_trace_constrained_beq_instructions() {
327-
type Chips = (CpuChip, AddChip, SubChip, BeqChip, RegisterMemCheckChip);
328+
type Chips = (
329+
CpuChip,
330+
AddChip,
331+
SubChip,
332+
BeqChip,
333+
RegisterMemCheckChip,
334+
ProgramMemCheckChip,
335+
);
328336
let basic_block = setup_basic_block_ir();
329337
let k = 1;
330338

331339
// Get traces from VM K-Trace interface
332340
let vm_traces = k_trace_direct(&basic_block, k).expect("Failed to create trace");
341+
let emulator = HarvardEmulator::from_basic_blocks(&basic_block);
342+
let program_memory = emulator.get_program_memory();
333343

334344
// Trace circuit
335345
let mut traces = TracesBuilder::new(LOG_SIZE);
336-
let program_trace = program_trace::ProgramTraces::dummy(LOG_SIZE); // TODO: replace this dummy with real program trace
346+
let program_trace = program_trace::ProgramTraces::new(LOG_SIZE, program_memory);
337347
let mut side_note = SideNote::new(&program_trace);
338348
let program_steps = iter_program_steps(&vm_traces, traces.num_rows());
339349

@@ -353,6 +363,6 @@ mod test {
353363
preprocessed_column.fill_is_first32();
354364
preprocessed_column.fill_row_idx();
355365
preprocessed_column.fill_timestamps();
356-
assert_chip::<Chips>(traces, Some(preprocessed_column), None);
366+
assert_chip::<Chips>(traces, Some(preprocessed_column), Some(program_trace));
357367
}
358368
}

‎prover/src/chips/bge.rs‎

Lines changed: 8 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -215,13 +215,16 @@ impl MachineChip for BgeChip {
215215
#[cfg(test)]
216216
mod test {
217217
use crate::{
218-
chips::{AddChip, CpuChip, Range128Chip, RegisterMemCheckChip, SubChip},
218+
chips::{
219+
AddChip, CpuChip, ProgramMemCheckChip, Range128Chip, RegisterMemCheckChip, SubChip,
220+
},
219221
test_utils::assert_chip,
220222
trace::{program::iter_program_steps, program_trace::ProgramTraces, PreprocessedTraces},
221223
};
222224

223225
use super::*;
224226
use nexus_vm::{
227+
emulator::{Emulator, HarvardEmulator},
225228
riscv::{BasicBlock, BuiltinOpcode, Instruction, InstructionType, Opcode},
226229
trace::k_trace_direct,
227230
};
@@ -320,16 +323,19 @@ mod test {
320323
BgeChip,
321324
Range128Chip,
322325
RegisterMemCheckChip,
326+
ProgramMemCheckChip,
323327
);
324328
let basic_block = setup_basic_block_ir();
325329
let k = 1;
326330

327331
// Get traces from VM K-Trace interface
328332
let vm_traces = k_trace_direct(&basic_block, k).expect("Failed to create trace");
333+
let emulator = HarvardEmulator::from_basic_blocks(&basic_block);
334+
let program_memory = emulator.get_program_memory();
329335

330336
// Trace circuit
331337
let mut traces = TracesBuilder::new(LOG_SIZE);
332-
let program_traces = ProgramTraces::dummy(LOG_SIZE);
338+
let program_traces = ProgramTraces::new(LOG_SIZE, program_memory);
333339
let mut side_note = SideNote::new(&program_traces);
334340
let program_steps = iter_program_steps(&vm_traces, traces.num_rows());
335341

‎prover/src/chips/bgeu.rs‎

Lines changed: 15 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -155,7 +155,7 @@ impl MachineChip for BgeuChip {
155155
#[cfg(test)]
156156
mod test {
157157
use crate::{
158-
chips::{AddChip, CpuChip, RegisterMemCheckChip, SubChip},
158+
chips::{AddChip, CpuChip, ProgramMemCheckChip, RegisterMemCheckChip, SubChip},
159159
test_utils::assert_chip,
160160
trace::{
161161
preprocessed::PreprocessedBuilder, program::iter_program_steps,
@@ -165,11 +165,12 @@ mod test {
165165

166166
use super::*;
167167
use nexus_vm::{
168+
emulator::{Emulator, HarvardEmulator},
168169
riscv::{BasicBlock, BuiltinOpcode, Instruction, InstructionType, Opcode},
169170
trace::k_trace_direct,
170171
};
171172

172-
const LOG_SIZE: u32 = PreprocessedBuilder::MIN_LOG_SIZE;
173+
const LOG_SIZE: u32 = 8; // PreprocessedBuilder::MIN_LOG_SIZE makes the test more than a minute long
173174

174175
#[rustfmt::skip]
175176
fn setup_basic_block_ir() -> Vec<BasicBlock> {
@@ -237,16 +238,25 @@ mod test {
237238

238239
#[test]
239240
fn test_k_trace_constrained_bgeu_instructions() {
240-
type Chips = (CpuChip, AddChip, SubChip, BgeuChip, RegisterMemCheckChip);
241+
type Chips = (
242+
CpuChip,
243+
AddChip,
244+
SubChip,
245+
BgeuChip,
246+
RegisterMemCheckChip,
247+
ProgramMemCheckChip,
248+
);
241249
let basic_block = setup_basic_block_ir();
242250
let k = 1;
243251

244252
// Get traces from VM K-Trace interface
245253
let vm_traces = k_trace_direct(&basic_block, k).expect("Failed to create trace");
254+
let emulator = HarvardEmulator::from_basic_blocks(&basic_block);
255+
let program_memory = emulator.get_program_memory();
246256

247257
// Trace circuit
248258
let mut traces = TracesBuilder::new(LOG_SIZE);
249-
let program_trace = ProgramTraces::dummy(LOG_SIZE);
259+
let program_trace = ProgramTraces::new(LOG_SIZE, program_memory);
250260
let mut side_note = SideNote::new(&program_trace);
251261
let program_steps = iter_program_steps(&vm_traces, traces.num_rows());
252262

@@ -266,6 +276,6 @@ mod test {
266276
preprocessed_column.fill_is_first32();
267277
preprocessed_column.fill_row_idx();
268278
preprocessed_column.fill_timestamps();
269-
assert_chip::<Chips>(traces, Some(preprocessed_column), None);
279+
assert_chip::<Chips>(traces, Some(preprocessed_column), Some(program_trace));
270280
}
271281
}

‎prover/src/chips/bit_op.rs‎

Lines changed: 13 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -313,7 +313,7 @@ impl MachineChip for BitOpChip {
313313
#[cfg(test)]
314314
mod test {
315315
use crate::{
316-
chips::{AddChip, CpuChip, RegisterMemCheckChip},
316+
chips::{AddChip, CpuChip, ProgramMemCheckChip, RegisterMemCheckChip},
317317
test_utils::assert_chip,
318318
trace::preprocessed::PreprocessedBuilder,
319319
trace::program::iter_program_steps,
@@ -322,6 +322,7 @@ mod test {
322322
use super::*;
323323

324324
use nexus_vm::{
325+
emulator::{Emulator, HarvardEmulator},
325326
riscv::{BasicBlock, BuiltinOpcode, Instruction, InstructionType, Opcode},
326327
trace::k_trace_direct,
327328
};
@@ -354,16 +355,24 @@ mod test {
354355

355356
#[test]
356357
fn test_k_trace_values() {
357-
type Chips = (CpuChip, AddChip, BitOpChip, RegisterMemCheckChip);
358+
type Chips = (
359+
CpuChip,
360+
AddChip,
361+
BitOpChip,
362+
RegisterMemCheckChip,
363+
ProgramMemCheckChip,
364+
);
358365
let basic_block = setup_basic_block_ir();
359366
let k = 1;
360367

361368
// Get traces from VM K-Trace interface
362369
let vm_traces = k_trace_direct(&basic_block, k).expect("Failed to create trace");
370+
let emulator = HarvardEmulator::from_basic_blocks(&basic_block);
371+
let program_memory = emulator.get_program_memory();
363372

364373
let mut traces = TracesBuilder::new(LOG_SIZE);
365374
let program_steps = iter_program_steps(&vm_traces, traces.num_rows());
366-
let program_trace = ProgramTraces::dummy(LOG_SIZE);
375+
let program_trace = ProgramTraces::new(LOG_SIZE, program_memory);
367376
let mut side_note = SideNote::new(&program_trace);
368377

369378
for (row_idx, program_step) in program_steps.enumerate() {
@@ -398,6 +407,6 @@ mod test {
398407

399408
assert_eq!(output, 0b0110100);
400409

401-
assert_chip::<Chips>(traces, None, None);
410+
assert_chip::<Chips>(traces, None, Some(program_trace));
402411
}
403412
}

‎prover/src/chips/blt.rs‎

Lines changed: 9 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -214,13 +214,16 @@ impl MachineChip for BltChip {
214214
#[cfg(test)]
215215
mod test {
216216
use crate::{
217-
chips::{AddChip, CpuChip, Range128Chip, RegisterMemCheckChip, SubChip},
217+
chips::{
218+
AddChip, CpuChip, ProgramMemCheckChip, Range128Chip, RegisterMemCheckChip, SubChip,
219+
},
218220
test_utils::assert_chip,
219221
trace::{program::iter_program_steps, program_trace::ProgramTraces, PreprocessedTraces},
220222
};
221223

222224
use super::*;
223225
use nexus_vm::{
226+
emulator::{Emulator, HarvardEmulator},
224227
riscv::{BasicBlock, BuiltinOpcode, Instruction, InstructionType, Opcode},
225228
trace::k_trace_direct,
226229
};
@@ -300,16 +303,19 @@ mod test {
300303
BltChip,
301304
Range128Chip,
302305
RegisterMemCheckChip,
306+
ProgramMemCheckChip,
303307
);
304308
let basic_block = setup_basic_block_ir();
305309
let k = 1;
306310

307311
// Get traces from VM K-Trace interface
308312
let vm_traces = k_trace_direct(&basic_block, k).expect("Failed to create trace");
313+
let emulator = HarvardEmulator::from_basic_blocks(&basic_block);
314+
let program_memory = emulator.get_program_memory();
309315

310316
// Trace circuit
311317
let mut traces = TracesBuilder::new(LOG_SIZE);
312-
let program_traces = ProgramTraces::dummy(LOG_SIZE);
318+
let program_traces = ProgramTraces::new(LOG_SIZE, program_memory);
313319
let mut side_note = SideNote::new(&program_traces);
314320
let program_steps = iter_program_steps(&vm_traces, traces.num_rows());
315321

@@ -324,6 +330,6 @@ mod test {
324330
);
325331
}
326332

327-
assert_chip::<Chips>(traces, None, None);
333+
assert_chip::<Chips>(traces, None, Some(program_traces));
328334
}
329335
}

‎prover/src/chips/bltu.rs‎

Lines changed: 14 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -155,7 +155,7 @@ impl MachineChip for BltuChip {
155155
#[cfg(test)]
156156
mod test {
157157
use crate::{
158-
chips::{AddChip, CpuChip, RegisterMemCheckChip, SubChip},
158+
chips::{AddChip, CpuChip, ProgramMemCheckChip, RegisterMemCheckChip, SubChip},
159159
test_utils::assert_chip,
160160
trace::{
161161
preprocessed::PreprocessedBuilder, program::iter_program_steps,
@@ -165,6 +165,7 @@ mod test {
165165

166166
use super::*;
167167
use nexus_vm::{
168+
emulator::{Emulator, HarvardEmulator},
168169
riscv::{BasicBlock, BuiltinOpcode, Instruction, InstructionType, Opcode},
169170
trace::k_trace_direct,
170171
};
@@ -233,16 +234,25 @@ mod test {
233234

234235
#[test]
235236
fn test_k_trace_constrained_bltu_instructions() {
236-
type Chips = (CpuChip, AddChip, SubChip, BltuChip, RegisterMemCheckChip);
237+
type Chips = (
238+
CpuChip,
239+
AddChip,
240+
SubChip,
241+
BltuChip,
242+
RegisterMemCheckChip,
243+
ProgramMemCheckChip,
244+
);
237245
let basic_block = setup_basic_block_ir();
238246
let k = 1;
239247

240248
// Get traces from VM K-Trace interface
241249
let vm_traces = k_trace_direct(&basic_block, k).expect("Failed to create trace");
250+
let emulator = HarvardEmulator::from_basic_blocks(&basic_block);
251+
let program_memory = emulator.get_program_memory();
242252

243253
// Trace circuit
244254
let mut traces = TracesBuilder::new(LOG_SIZE);
245-
let program_trace = ProgramTraces::dummy(LOG_SIZE);
255+
let program_trace = ProgramTraces::new(LOG_SIZE, program_memory);
246256
let mut side_note = SideNote::new(&program_trace);
247257
let program_steps = iter_program_steps(&vm_traces, traces.num_rows());
248258

@@ -262,6 +272,6 @@ mod test {
262272
preprocessed_column.fill_is_first32();
263273
preprocessed_column.fill_row_idx();
264274
preprocessed_column.fill_timestamps();
265-
assert_chip::<Chips>(traces, Some(preprocessed_column), None);
275+
assert_chip::<Chips>(traces, Some(preprocessed_column), Some(program_trace));
266276
}
267277
}

0 commit comments

Comments
 (0)