Skip to content

Commit 09a1808

Browse files
authored
Merge pull request #893 from Inversed-Tech/mihai/keccakf_integration
`keccakf` precompile + GKR-IOP integration
2 parents 6ef1b7c + a589775 commit 09a1808

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

43 files changed

+2852
-78
lines changed

Cargo.lock

Lines changed: 54 additions & 0 deletions
Some generated files are not rendered by default. Learn more about customizing how changed files appear on GitHub.

Cargo.toml

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -36,6 +36,7 @@ cfg-if = "1.0"
3636
criterion = { version = "0.5", features = ["html_reports"] }
3737
crossbeam-channel = "0.5"
3838
itertools = "0.13"
39+
ndarray = "*"
3940
num-bigint = { version = "0.4.6" }
4041
num-derive = "0.4"
4142
num-traits = "0.2"
@@ -60,7 +61,7 @@ rand_core = "0.6"
6061
rand_xorshift = "0.3"
6162
rayon = "1.10"
6263
secp = "0.4.1"
63-
serde = { version = "1.0", features = ["derive"] }
64+
serde = { version = "1.0", features = ["derive", "rc"] }
6465
serde_json = "1.0"
6566
strum = "0.26"
6667
strum_macros = "0.26"

ceno_emul/src/syscalls.rs

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -20,6 +20,10 @@ 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;
25+
26+
const GKR_OUTPUTS: usize = 0;
2327
}
2428

2529
/// 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_host/tests/test_elf.rs

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -231,7 +231,7 @@ fn test_ceno_rt_keccak() -> Result<()> {
231231
let steps = run(&mut state)?;
232232

233233
// Expect the program to have written successive states between Keccak permutations.
234-
const ITERATIONS: usize = 3;
234+
const ITERATIONS: usize = 4;
235235
let keccak_outs = sample_keccak_f(ITERATIONS);
236236

237237
let all_messages = read_all_messages(&state);

ceno_zkvm/Cargo.toml

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -19,9 +19,11 @@ serde_json.workspace = true
1919
base64 = "0.22"
2020
ceno_emul = { path = "../ceno_emul" }
2121
ff_ext = { path = "../ff_ext" }
22+
gkr_iop = { path = "../gkr_iop" }
2223
mpcs = { path = "../mpcs" }
2324
multilinear_extensions = { version = "0", path = "../multilinear_extensions" }
2425
p3 = { path = "../p3" }
26+
subprotocols = { path = "../subprotocols" }
2527
sumcheck = { version = "0", path = "../sumcheck" }
2628
transcript = { path = "../transcript" }
2729
witness = { path = "../witness" }

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/instructions.rs

Lines changed: 169 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,7 @@
11
use ceno_emul::StepRecord;
22
use ff_ext::ExtensionField;
3+
use gkr_iop::{ProtocolBuilder, ProtocolWitnessGenerator, gkr::GKRCircuitWitness};
4+
use itertools::Itertools;
35
use multilinear_extensions::util::max_usable_threads;
46
use rayon::{
57
iter::{IndexedParallelIterator, ParallelIterator},
@@ -67,3 +69,170 @@ pub trait Instruction<E: ExtensionField> {
6769
Ok((raw_witin, lk_multiplicity))
6870
}
6971
}
72+
73+
pub struct GKRinfo {
74+
pub and_lookups: usize,
75+
pub xor_lookups: usize,
76+
pub range_lookups: usize,
77+
pub aux_wits: usize,
78+
}
79+
80+
impl GKRinfo {
81+
fn lookup_total(&self) -> usize {
82+
self.and_lookups + self.xor_lookups + self.range_lookups
83+
}
84+
}
85+
86+
// Trait that should be implemented by opcodes which use the
87+
// GKR-IOP prover. Presently, such opcodes should also implement
88+
// the Instruction trait and in general methods of GKRIOPInstruction
89+
// will call corresponding methods of Instruction and do something extra
90+
// with respect to syncing state between GKR-IOP and old-style circuits/witnesses
91+
pub trait GKRIOPInstruction<E: ExtensionField>
92+
where
93+
Self: Instruction<E>,
94+
{
95+
type Layout: ProtocolWitnessGenerator<E> + ProtocolBuilder;
96+
97+
/// Similar to Instruction::construct_circuit; generally
98+
/// meant to extend InstructionConfig with GKR-specific
99+
/// fields
100+
#[allow(unused_variables)]
101+
fn construct_circuit_with_gkr_iop(
102+
cb: &mut CircuitBuilder<E>,
103+
) -> Result<Self::InstructionConfig, ZKVMError> {
104+
unimplemented!();
105+
}
106+
107+
/// Should generate phase1 witness for GKR from step records
108+
fn phase1_witness_from_steps(
109+
layout: &Self::Layout,
110+
steps: &[StepRecord],
111+
) -> Vec<Vec<E::BaseField>>;
112+
113+
/// Similar to Instruction::assign_instance, but with access to GKR lookups and wits
114+
fn assign_instance_with_gkr_iop(
115+
config: &Self::InstructionConfig,
116+
instance: &mut [E::BaseField],
117+
lk_multiplicity: &mut LkMultiplicity,
118+
step: &StepRecord,
119+
lookups: &[E::BaseField],
120+
aux_wits: &[E::BaseField],
121+
) -> Result<(), ZKVMError>;
122+
123+
/// Similar to Instruction::assign_instances, but with access to the GKR layout.
124+
#[allow(clippy::type_complexity)]
125+
fn assign_instances_with_gkr_iop(
126+
config: &Self::InstructionConfig,
127+
num_witin: usize,
128+
steps: Vec<StepRecord>,
129+
gkr_layout: &Self::Layout,
130+
) -> Result<
131+
(
132+
RowMajorMatrix<E::BaseField>,
133+
GKRCircuitWitness<E>,
134+
LkMultiplicity,
135+
),
136+
ZKVMError,
137+
> {
138+
let nthreads = max_usable_threads();
139+
let num_instance_per_batch = if steps.len() > 256 {
140+
steps.len().div_ceil(nthreads)
141+
} else {
142+
steps.len()
143+
}
144+
.max(1);
145+
let lk_multiplicity = LkMultiplicity::default();
146+
let mut raw_witin =
147+
RowMajorMatrix::<E::BaseField>::new(steps.len(), num_witin, Self::padding_strategy());
148+
let raw_witin_iter = raw_witin.par_batch_iter_mut(num_instance_per_batch);
149+
150+
let gkr_witness =
151+
gkr_layout.gkr_witness(&Self::phase1_witness_from_steps(gkr_layout, &steps), &[]);
152+
153+
let (lookups, aux_wits) = {
154+
// Extract lookups and auxiliary witnesses from GKR protocol
155+
// Here we assume that the gkr_witness's last layer is a convenience layer which holds
156+
// the output records for all instances; further, we assume that the last ```Self::lookup_count()```
157+
// elements of this layer are the lookup arguments.
158+
let mut lookups = vec![vec![]; steps.len()];
159+
let mut aux_wits: Vec<Vec<E::BaseField>> = vec![vec![]; steps.len()];
160+
let last_layer = gkr_witness.layers.last().unwrap().bases.clone();
161+
let len = last_layer.len();
162+
let lookup_total = Self::gkr_info().lookup_total();
163+
164+
let non_lookups = if len == 0 {
165+
0
166+
} else {
167+
assert!(len >= lookup_total);
168+
len - lookup_total
169+
};
170+
171+
for witness in last_layer.iter().skip(non_lookups) {
172+
for i in 0..witness.len() {
173+
lookups[i].push(witness[i]);
174+
}
175+
}
176+
177+
let n_layers = gkr_witness.layers.len();
178+
179+
for i in 0..steps.len() {
180+
// Omit last layer, which stores outputs and not real witnesses
181+
for layer in gkr_witness.layers[..n_layers - 1].iter() {
182+
for base in layer.bases.iter() {
183+
aux_wits[i].push(base[i]);
184+
}
185+
}
186+
}
187+
188+
(lookups, aux_wits)
189+
};
190+
191+
raw_witin_iter
192+
.zip(
193+
steps
194+
.iter()
195+
.enumerate()
196+
.collect_vec()
197+
.par_chunks(num_instance_per_batch),
198+
)
199+
.flat_map(|(instances, steps)| {
200+
let mut lk_multiplicity = lk_multiplicity.clone();
201+
instances
202+
.chunks_mut(num_witin)
203+
.zip(steps)
204+
.map(|(instance, (i, step))| {
205+
Self::assign_instance_with_gkr_iop(
206+
config,
207+
instance,
208+
&mut lk_multiplicity,
209+
step,
210+
&lookups[*i],
211+
&aux_wits[*i],
212+
)
213+
})
214+
.collect::<Vec<_>>()
215+
})
216+
.collect::<Result<(), ZKVMError>>()?;
217+
218+
raw_witin.padding_by_strategy();
219+
Ok((raw_witin, gkr_witness, lk_multiplicity))
220+
}
221+
222+
/// Lookup and witness counts used by GKR proof
223+
fn gkr_info() -> GKRinfo;
224+
225+
/// Returns corresponding column in RMM for the i-th
226+
/// output evaluation of the GKR proof
227+
#[allow(unused_variables)]
228+
fn output_evals_map(i: usize) -> usize {
229+
unimplemented!();
230+
}
231+
232+
/// Returns corresponding column in RMM for the i-th
233+
/// witness of the GKR proof
234+
#[allow(unused_variables)]
235+
fn witness_map(i: usize) -> usize {
236+
unimplemented!();
237+
}
238+
}

0 commit comments

Comments
 (0)