Skip to content

Commit ee54156

Browse files
committed
add lookups to DummyEcall (wip, Apr 10)
1 parent dd5ade7 commit ee54156

File tree

14 files changed

+165
-81
lines changed

14 files changed

+165
-81
lines changed

ceno_emul/src/syscalls.rs

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -20,6 +20,8 @@ pub trait SyscallSpec {
2020
const REG_OPS_COUNT: usize;
2121
const MEM_OPS_COUNT: usize;
2222
const CODE: u32;
23+
24+
const HAS_LOOKUPS: bool = false;
2325
}
2426

2527
/// Trace the inputs and effects of a syscall.

ceno_emul/src/syscalls/keccak_permute.rs

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -16,6 +16,7 @@ impl SyscallSpec for KeccakSpec {
1616
const REG_OPS_COUNT: usize = 2;
1717
const MEM_OPS_COUNT: usize = KECCAK_WORDS;
1818
const CODE: u32 = ceno_rt::syscalls::KECCAK_PERMUTE;
19+
const HAS_LOOKUPS: bool = true;
1920
}
2021

2122
/// Wrapper type for the keccak_permute argument that implements conversions

ceno_zkvm/benches/riscv_add.rs

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -95,6 +95,7 @@ fn bench_add(c: &mut Criterion) {
9595
"ADD",
9696
&prover.pk.pp,
9797
&circuit_pk,
98+
&None,
9899
polys.into_iter().map(|mle| mle.into()).collect_vec(),
99100
commit,
100101
&[],

ceno_zkvm/src/e2e.rs

Lines changed: 9 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -295,7 +295,7 @@ fn generate_fixed_traces<E: ExtensionField>(
295295
}
296296

297297
pub fn generate_witness<E: ExtensionField>(
298-
system_config: &ConstraintSystemConfig<E>,
298+
system_config: &mut ConstraintSystemConfig<E>,
299299
emul_result: EmulationResult,
300300
program: &Program,
301301
is_mock_proving: bool,
@@ -312,7 +312,7 @@ pub fn generate_witness<E: ExtensionField>(
312312
.unwrap();
313313
system_config
314314
.dummy_config
315-
.assign_opcode_circuit(&system_config.zkvm_cs, &mut zkvm_witness, dummy_records)
315+
.assign_opcode_circuit(&mut system_config.zkvm_cs, &mut zkvm_witness, dummy_records)
316316
.unwrap();
317317
zkvm_witness.finalize_lk_multiplicities(is_mock_proving);
318318

@@ -394,7 +394,7 @@ pub fn run_e2e_with_checkpoint<
394394
};
395395

396396
let program = Arc::new(program);
397-
let system_config = construct_configs::<E>(program_params);
397+
let mut system_config = construct_configs::<E>(program_params);
398398
let reg_init = system_config.mmu_config.initial_registers();
399399

400400
// IO is not used in this program, but it must have a particular size at the moment.
@@ -432,7 +432,7 @@ pub fn run_e2e_with_checkpoint<
432432
init_full_mem,
433433
platform,
434434
hints,
435-
&system_config,
435+
&mut system_config,
436436
pk,
437437
zkvm_fixed_traces,
438438
is_mock_proving,
@@ -451,11 +451,13 @@ pub fn run_e2e_with_checkpoint<
451451
if let Checkpoint::PrepWitnessGen = checkpoint {
452452
return (
453453
None,
454-
Box::new(move || _ = generate_witness(&system_config, emul_result, &program, false)),
454+
Box::new(move || {
455+
_ = generate_witness(&mut system_config, emul_result, &program, false)
456+
}),
455457
);
456458
}
457459

458-
let zkvm_witness = generate_witness(&system_config, emul_result, &program, is_mock_proving);
460+
let zkvm_witness = generate_witness(&mut system_config, emul_result, &program, is_mock_proving);
459461

460462
// proving
461463
let prover = ZKVMProver::new(pk);
@@ -496,7 +498,7 @@ pub fn run_e2e_proof<E: ExtensionField + LkMultiplicityKey, PCS: PolynomialCommi
496498
init_full_mem: InitMemState,
497499
platform: Platform,
498500
hints: Vec<u32>,
499-
system_config: &ConstraintSystemConfig<E>,
501+
system_config: &mut ConstraintSystemConfig<E>,
500502
pk: ZKVMProvingKey<E, PCS>,
501503
zkvm_fixed_traces: ZKVMFixedTraces<E>,
502504
is_mock_proving: bool,

ceno_zkvm/src/instructions.rs

Lines changed: 32 additions & 15 deletions
Original file line numberDiff line numberDiff line change
@@ -84,12 +84,12 @@ where
8484
instance: &mut [E::BaseField],
8585
lk_multiplicity: &mut LkMultiplicity,
8686
step: &StepRecord,
87-
lookups: Vec<E::BaseField>,
87+
lookups: &[E::BaseField],
8888
) -> Result<(), ZKVMError>;
8989

9090
fn phase1_witness_from_steps(
9191
layout: &Self::Layout,
92-
steps: Vec<StepRecord>,
92+
steps: &[StepRecord],
9393
) -> Vec<Vec<E::BaseField>>;
9494

9595
fn assign_instances_with_gkr_iop(
@@ -111,34 +111,51 @@ where
111111
let raw_witin_iter = raw_witin.par_batch_iter_mut(num_instance_per_batch);
112112

113113
let gkr_witness = gkr_layout.gkr_witness(
114-
&Self::phase1_witness_from_steps(gkr_layout, steps.clone()),
114+
&Self::phase1_witness_from_steps(gkr_layout, &steps),
115115
&vec![],
116116
);
117117

118-
let lookups = gkr_witness
119-
.layers
120-
.last()
121-
.unwrap()
122-
.bases
123-
.iter()
124-
.map(|instance| instance.into_iter().skip(100).collect_vec())
125-
.collect_vec();
118+
let lookups = {
119+
let mut lookups = vec![vec![]; steps.len()];
120+
for witness in gkr_witness
121+
.layers
122+
.last()
123+
.unwrap()
124+
.bases
125+
.iter()
126+
.skip(100)
127+
.cloned()
128+
{
129+
for i in 0..witness.len() {
130+
lookups[i].push(witness[i]);
131+
}
132+
}
133+
lookups
134+
};
135+
136+
// dbg!(&lookups);
126137

127138
raw_witin_iter
128-
.zip(steps.par_chunks(num_instance_per_batch))
139+
.zip(
140+
steps
141+
.iter()
142+
.enumerate()
143+
.collect_vec()
144+
.par_chunks(num_instance_per_batch),
145+
)
129146
.flat_map(|(instances, steps)| {
130147
let mut lk_multiplicity = lk_multiplicity.clone();
131148
instances
132149
.chunks_mut(num_witin)
133150
.zip(steps)
134-
.map(|(instance, step)| {
135-
let lookups = vec![];
151+
.map(|(instance, (i, step))| {
152+
// dbg!(i, step);
136153
Self::assign_instance_with_gkr_iop(
137154
config,
138155
instance,
139156
&mut lk_multiplicity,
140157
step,
141-
lookups,
158+
&lookups[*i],
142159
)
143160
})
144161
.collect::<Vec<_>>()

ceno_zkvm/src/instructions/riscv/dummy/dummy_ecall.rs

Lines changed: 49 additions & 33 deletions
Original file line numberDiff line numberDiff line change
@@ -79,34 +79,36 @@ impl<E: ExtensionField, S: SyscallSpec> Instruction<E> for LargeEcallDummy<E, S>
7979
.collect::<Result<Vec<_>, _>>()?;
8080

8181
// Temporarily set this to < 24 to avoid cb.num_witin overflow
82-
let active_rounds = 12;
82+
let active_rounds = 0;
8383

8484
let mut lookups = Vec::with_capacity(
8585
active_rounds
8686
* (3 * AND_LOOKUPS_PER_ROUND + 3 * XOR_LOOKUPS_PER_ROUND + RANGE_LOOKUPS_PER_ROUND),
8787
);
8888

89-
dbg!(lookups.capacity());
90-
91-
for round in 0..active_rounds {
92-
for i in 0..AND_LOOKUPS_PER_ROUND {
93-
let a = cb.create_witin(|| format!("and_lookup_{round}_{i}_a"));
94-
let b = cb.create_witin(|| format!("and_lookup_{round}_{i}_b"));
95-
let c = cb.create_witin(|| format!("and_lookup_{round}_{i}_c"));
96-
cb.lookup_and_byte(a.into(), b.into(), c.into())?;
97-
lookups.extend(vec![a, b, c]);
98-
}
99-
for i in 0..XOR_LOOKUPS_PER_ROUND {
100-
let a = cb.create_witin(|| format!("xor_lookup_{round}_{i}_a"));
101-
let b = cb.create_witin(|| format!("xor_lookup_{round}_{i}_b"));
102-
let c = cb.create_witin(|| format!("xor_lookup_{round}_{i}_c"));
103-
cb.lookup_xor_byte(a.into(), b.into(), c.into())?;
104-
lookups.extend(vec![a, b, c]);
105-
}
106-
for i in 0..RANGE_LOOKUPS_PER_ROUND {
107-
let wit = cb.create_witin(|| format!("range_lookup_{round}_{i}"));
108-
cb.assert_ux::<_, _, 16>(|| "nada", wit.into())?;
109-
lookups.push(wit);
89+
if S::HAS_LOOKUPS {
90+
dbg!(lookups.capacity());
91+
92+
for round in 0..active_rounds {
93+
for i in 0..AND_LOOKUPS_PER_ROUND {
94+
let a = cb.create_witin(|| format!("and_lookup_{round}_{i}_a"));
95+
let b = cb.create_witin(|| format!("and_lookup_{round}_{i}_b"));
96+
let c = cb.create_witin(|| format!("and_lookup_{round}_{i}_c"));
97+
cb.lookup_and_byte(a.into(), b.into(), c.into())?;
98+
lookups.extend(vec![a, b, c]);
99+
}
100+
for i in 0..XOR_LOOKUPS_PER_ROUND {
101+
let a = cb.create_witin(|| format!("xor_lookup_{round}_{i}_a"));
102+
let b = cb.create_witin(|| format!("xor_lookup_{round}_{i}_b"));
103+
let c = cb.create_witin(|| format!("xor_lookup_{round}_{i}_c"));
104+
cb.lookup_xor_byte(a.into(), b.into(), c.into())?;
105+
lookups.extend(vec![a, b, c]);
106+
}
107+
for i in 0..RANGE_LOOKUPS_PER_ROUND {
108+
let wit = cb.create_witin(|| format!("range_lookup_{round}_{i}"));
109+
cb.assert_ux::<_, _, 16>(|| "nada", wit.into())?;
110+
lookups.push(wit);
111+
}
110112
}
111113
}
112114

@@ -157,7 +159,7 @@ impl<E: ExtensionField> GKRIOPInstruction<E> for LargeEcallDummy<E, KeccakSpec>
157159

158160
fn phase1_witness_from_steps(
159161
layout: &Self::Layout,
160-
steps: Vec<StepRecord>,
162+
steps: &[StepRecord],
161163
) -> Vec<Vec<<E as ExtensionField>::BaseField>> {
162164
let instances = steps
163165
.iter()
@@ -181,33 +183,47 @@ impl<E: ExtensionField> GKRIOPInstruction<E> for LargeEcallDummy<E, KeccakSpec>
181183
instance: &mut [<E as ExtensionField>::BaseField],
182184
lk_multiplicity: &mut LkMultiplicity,
183185
step: &StepRecord,
184-
lookups: Vec<E::BaseField>,
186+
lookups: &[E::BaseField],
185187
) -> Result<(), ZKVMError> {
186188
Self::assign_instance(config, instance, lk_multiplicity, step)?;
187189

188-
let active_rounds = 12;
190+
let active_rounds = 0;
189191
let mut wit_iter = lookups.iter().map(|f| f.to_canonical_u64());
190192
let mut var_iter = config.lookups.iter();
191193

194+
dbg!(wit_iter.clone().count());
195+
dbg!(var_iter.clone().count());
196+
192197
let mut pop_arg = || -> u64 {
193198
let wit = wit_iter.next().unwrap();
194199
let var = var_iter.next().unwrap();
195-
set_val!(instance, var, wit);
200+
// set_val!(instance, var, wit);
201+
set_val!(instance, var, 0);
196202
wit
197203
};
198204

199-
for round in 0..active_rounds {
200-
for i in 0..AND_LOOKUPS_PER_ROUND {
201-
lk_multiplicity.lookup_and_byte(pop_arg(), pop_arg());
205+
for _round in 0..active_rounds {
206+
for _i in 0..AND_LOOKUPS_PER_ROUND {
207+
// lk_multiplicity.lookup_and_byte(pop_arg(), pop_arg());
208+
lk_multiplicity.lookup_and_byte(0, 0);
209+
pop_arg();
210+
pop_arg();
211+
pop_arg();
202212
}
203-
for i in 0..XOR_LOOKUPS_PER_ROUND {
204-
lk_multiplicity.lookup_xor_byte(pop_arg(), pop_arg());
213+
for _i in 0..XOR_LOOKUPS_PER_ROUND {
214+
lk_multiplicity.lookup_xor_byte(0, 0);
215+
pop_arg();
216+
pop_arg();
217+
pop_arg();
205218
}
206-
for i in 0..RANGE_LOOKUPS_PER_ROUND {
207-
lk_multiplicity.assert_ux::<16>(pop_arg());
219+
for _i in 0..RANGE_LOOKUPS_PER_ROUND {
220+
lk_multiplicity.assert_ux::<16>(0);
221+
pop_arg();
208222
}
209223
}
210224

225+
assert!(var_iter.next().is_none());
226+
211227
Ok(())
212228
}
213229
}

ceno_zkvm/src/instructions/riscv/rv32im.rs

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -524,7 +524,7 @@ impl<E: ExtensionField> DummyExtraConfig<E> {
524524

525525
pub fn assign_opcode_circuit(
526526
&self,
527-
cs: &ZKVMConstraintSystem<E>,
527+
cs: &mut ZKVMConstraintSystem<E>,
528528
witness: &mut ZKVMWitnesses<E>,
529529
steps: GroupedSteps,
530530
) -> Result<(), ZKVMError> {
@@ -562,7 +562,7 @@ impl<E: ExtensionField> DummyExtraConfig<E> {
562562
}
563563
}
564564

565-
witness.assign_keccakf_circuit(&cs, &self.keccak_config, keccak_steps)?;
565+
witness.assign_keccakf_circuit(cs, &self.keccak_config, keccak_steps)?;
566566

567567
witness.assign_opcode_circuit::<LargeEcallDummy<E, Secp256k1AddSpec>>(
568568
cs,

ceno_zkvm/src/scheme/prover.rs

Lines changed: 6 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -181,7 +181,8 @@ impl<E: ExtensionField, PCS: PolynomialCommitmentScheme<E>> ZKVMProver<E, PCS> {
181181
&& cs.w_table_expressions.is_empty();
182182

183183
if *circuit_name == <LargeEcallDummy<E, KeccakSpec> as Instruction<E>>::name() {
184-
unimplemented!("keccak impl wip");
184+
// unimplemented!("keccak impl wip");
185+
()
185186
} else if is_opcode_circuit {
186187
tracing::debug!(
187188
"opcode circuit {} has {} witnesses, {} reads, {} writes, {} lookups",
@@ -278,10 +279,10 @@ impl<E: ExtensionField, PCS: PolynomialCommitmentScheme<E>> ZKVMProver<E, PCS> {
278279
let log2_num_instances = ceil_log2(next_pow2_instances);
279280
let (chip_record_alpha, _) = (challenges[0], challenges[1]);
280281

281-
if let Some(gkr_iop_pk) = gkr_iop_pk {
282-
let mut gkr_iop_pk = gkr_iop_pk.clone();
283-
unimplemented!("cannot fully handle GKRIOP component yet")
284-
}
282+
// if let Some(gkr_iop_pk) = gkr_iop_pk {
283+
// let mut gkr_iop_pk = gkr_iop_pk.clone();
284+
// unimplemented!("cannot fully handle GKRIOP component yet")
285+
// }
285286

286287
// sanity check
287288
assert_eq!(witnesses.len(), cs.num_witin as usize);

ceno_zkvm/src/scheme/tests.rs

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -139,6 +139,7 @@ fn test_rw_lk_expression_combination() {
139139
name.as_str(),
140140
&prover.pk.pp,
141141
prover.pk.circuit_pks.get(&name).unwrap(),
142+
&None,
142143
wits_in,
143144
commit,
144145
&[],

ceno_zkvm/src/structs.rs

Lines changed: 16 additions & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -2,7 +2,7 @@ use crate::{
22
circuit_builder::{CircuitBuilder, ConstraintSystem},
33
error::ZKVMError,
44
expression::Expression,
5-
instructions::{Instruction, riscv::dummy::LargeEcallDummy},
5+
instructions::{GKRIOPInstruction, Instruction, riscv::dummy::LargeEcallDummy},
66
state::StateCircuit,
77
tables::{RMMCollections, TableCircuit},
88
witness::LkMultiplicity,
@@ -365,25 +365,28 @@ impl<E: ExtensionField> ZKVMWitnesses<E> {
365365

366366
pub fn assign_keccakf_circuit(
367367
&mut self,
368-
css: &ZKVMConstraintSystem<E>,
368+
// TODO: do without mutability requirement
369+
css: &mut ZKVMConstraintSystem<E>,
369370
config: &<LargeEcallDummy<E, KeccakSpec> as Instruction<E>>::InstructionConfig,
370371
records: Vec<StepRecord>,
371372
) -> Result<(), ZKVMError> {
372373
// Ugly copy paste from assign_opcode_circuit, but we need to use the row major matrix
373374
let cs = css
374375
.get_cs(&LargeEcallDummy::<E, KeccakSpec>::name())
375376
.unwrap();
376-
let (witness, logup_multiplicity) = LargeEcallDummy::<E, KeccakSpec>::assign_instances(
377-
config,
378-
cs.num_witin as usize,
379-
records,
380-
)?;
381-
382-
// Intercept row-major matrix, convert into KeccakTrace and obtain phase1_wit
383-
self.keccak_phase1wit = css
384-
.keccak_gkr_iop
385-
.layout
386-
.phase1_witness(KeccakTrace::from(witness.clone()));
377+
let (witness, logup_multiplicity) =
378+
LargeEcallDummy::<E, KeccakSpec>::assign_instances_with_gkr_iop(
379+
config,
380+
cs.num_witin as usize,
381+
records,
382+
&mut css.keccak_gkr_iop.layout,
383+
)?;
384+
385+
// // Intercept row-major matrix, convert into KeccakTrace and obtain phase1_wit
386+
// self.keccak_phase1wit = css
387+
// .keccak_gkr_iop
388+
// .layout
389+
// .phase1_witness(KeccakTrace::from(witness.clone()));
387390

388391
assert!(
389392
self.witnesses_opcodes

0 commit comments

Comments
 (0)