Skip to content

Commit 76b3647

Browse files
authored
feat: Incremental aggregation ohbender (#5)
## What ❔ * Added keccak_32 implementation that can run on reduced machine * In universal verifier - added option to combine 2 proofs with same verification keys together (and their 'public input' will be the keccak of the inputs) * added flatten-two command in CLI that combines 2 proofs together. * added CI to test this case. ## Why ❔ This allows us to implement 'ohbender' - where we would merge the current proof with the previous one - therefore creating a 'chained' proof, which can be snark-wrapped once.
1 parent efd6c72 commit 76b3647

File tree

14 files changed

+419
-23
lines changed

14 files changed

+419
-23
lines changed

.dockerignore

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -17,6 +17,7 @@ tools/verifier/target
1717
!non_determinism_source
1818
!poseidon2
1919
!prover
20+
!reduced_keccak
2021
!risc_v_simulator
2122
!riscv_common
2223
!trace_holder

.github/workflows/ci.yml

Lines changed: 32 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -361,6 +361,38 @@ jobs:
361361
run: ./cli verify --proof recursion_proofs/reduced_proof_0.json
362362

363363

364+
# Test incremental proofs.
365+
oh_bender:
366+
name: oh_bender_incremental_proofs
367+
runs-on: [matterlabs-ci-runner-c3d]
368+
needs: [build_cli_no_verifiers_512, build_verifier]
369+
370+
steps:
371+
- uses: actions/checkout@v3
372+
- uses: actions/download-artifact@v4
373+
with:
374+
name: cli_512
375+
- uses: actions/download-artifact@v4
376+
with:
377+
name: verifier
378+
379+
- name: Display structure of downloaded files
380+
run: ls -R
381+
- name: Set permissions
382+
run: chmod +x ./cli
383+
384+
- name: Create output
385+
run: mkdir output
386+
387+
388+
- name: Create basic fibonacci proof
389+
run: ./cli prove --bin examples/basic_fibonacci/app.bin --until final-recursion --output-dir output
390+
- name: Flatten 2 basic fibonacci proofs
391+
run: ./cli flatten-two --first-metadata output/metadata.json --second-metadata output/metadata.json --output-file output/proof_merged_flatten.json
392+
- name: Run
393+
run: ./cli run --bin app.bin --input-file output/proof_merged_flatten.json --cycles 20000000 --machine reduced --expected-results 890242439,3543186763,4251668155,4029038820,912219460,64639318,3267867168,290530290
394+
395+
364396
full_recursion:
365397
name: full_recursion
366398
runs-on: [matterlabs-ci-runner-c3d]

Cargo.toml

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -43,6 +43,7 @@ members = [
4343
"verifier_common",
4444
"poseidon2",
4545
"non_determinism_source",
46+
"reduced_keccak",
4647
"risc_v_simulator",
4748
"execution_utils",
4849
"circuit_defs/blake2_with_compression",
@@ -74,6 +75,7 @@ default-members = [
7475
"non_determinism_source",
7576
"poseidon2",
7677
"prover",
78+
"reduced_keccak",
7779
"risc_v_simulator",
7880
"tools/cli",
7981
"tools/generator",

reduced_keccak/Cargo.toml

Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
[package]
2+
name = "reduced_keccak"
3+
4+
version.workspace = true
5+
edition.workspace = true
6+
authors.workspace = true
7+
homepage.workspace = true
8+
repository.workspace = true
9+
license.workspace = true
10+
keywords.workspace = true
11+
categories.workspace = true

reduced_keccak/src/lib.rs

Lines changed: 275 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,275 @@
1+
#![no_std]
2+
3+
// Keccak-256 implementation for RV32, using u32 words.
4+
// This is a special implementation that can be run on our reduced machine
5+
// therefore it can run as part of recursion flow.
6+
// WARNING: this api is little-endian based (both inputs and outputs).
7+
8+
/// Keccak parameters for Keccak-256
9+
const LANES: usize = 25; // 5×5 lanes
10+
const RATE_BITS: usize = 1088;
11+
const CAP_BITS: usize = 512;
12+
const RATE_LANES: usize = RATE_BITS / 64; // = 17 lanes per block
13+
const RATE_WORDS: usize = RATE_BITS / 32; // = 34 u32 words per block
14+
15+
/// A Keccak-256 sponge with u32-word inputs/outputs, for RV32. No heap allocations.
16+
pub struct Keccak32 {
17+
state: [u64; LANES], // internal 64-bit lanes
18+
buffer: [u32; RATE_WORDS], // fixed-size input buffer
19+
buf_len: usize, // how many words are buffered
20+
}
21+
22+
impl Keccak32 {
23+
/// Initialize a new Keccak-256 hasher.
24+
pub fn new() -> Self {
25+
assert!(
26+
RATE_BITS + CAP_BITS == 1600,
27+
"rate+capacity must equal 1600 bits"
28+
);
29+
Keccak32 {
30+
state: [0u64; LANES],
31+
buffer: [0u32; RATE_WORDS],
32+
buf_len: 0,
33+
}
34+
}
35+
36+
/// Absorb a slice of u32 words (little-endian).
37+
pub fn update(&mut self, input: &[u32]) {
38+
let mut in_off = 0;
39+
let mut rem = self.buf_len;
40+
41+
// 1) Fill the current buffer to a full block, if partially filled
42+
if rem > 0 {
43+
let needed = RATE_WORDS - rem;
44+
let take = needed.min(input.len());
45+
for i in 0..take {
46+
self.buffer[rem + i] = input[in_off + i];
47+
}
48+
rem += take;
49+
in_off += take;
50+
if rem == RATE_WORDS {
51+
// buffer now full → absorb
52+
let mut lanes = [0u64; RATE_LANES];
53+
for i in 0..RATE_LANES {
54+
let lo = self.buffer[2 * i] as u64;
55+
let hi = self.buffer[2 * i + 1] as u64;
56+
lanes[i] = lo | (hi << 32);
57+
}
58+
self.absorb_block(&lanes);
59+
rem = 0; // buffer is now empty
60+
}
61+
}
62+
63+
// 2) Absorb all full blocks directly from remaining input
64+
while input.len().saturating_sub(in_off) >= RATE_WORDS {
65+
let mut lanes = [0u64; RATE_LANES];
66+
for i in 0..RATE_LANES {
67+
let lo = input[in_off + 2 * i] as u64;
68+
let hi = input[in_off + 2 * i + 1] as u64;
69+
lanes[i] = lo | (hi << 32);
70+
}
71+
self.absorb_block(&lanes);
72+
in_off += RATE_WORDS;
73+
}
74+
75+
// 3) Buffer any leftover words
76+
let take = input.len().saturating_sub(in_off);
77+
for i in 0..take {
78+
self.buffer[rem + i] = input[in_off + i];
79+
}
80+
rem += take;
81+
self.buf_len = rem;
82+
}
83+
84+
/// Finalize and return 8 u32 words (32 bytes) of output.
85+
pub fn finalize(mut self) -> [u32; 8] {
86+
// Multi-rate pad10*1 on u32-word boundary
87+
let rem = self.buf_len;
88+
let mut lanes = [0u64; RATE_LANES];
89+
// fill lanes from buffer
90+
for i in 0..(rem / 2) {
91+
let lo = self.buffer[2 * i] as u64;
92+
let hi = self.buffer[2 * i + 1] as u64;
93+
lanes[i] = lo | (hi << 32);
94+
}
95+
if rem % 2 == 1 {
96+
lanes[rem / 2] = self.buffer[rem - 1] as u64;
97+
}
98+
// pad bit right after last word
99+
let lane_idx = rem / 2;
100+
let bit_pos = (rem % 2) * 32;
101+
lanes[lane_idx] |= 1u64 << bit_pos;
102+
// final pad bit at end of block
103+
lanes[RATE_LANES - 1] |= 1u64 << 63;
104+
self.absorb_block(&lanes);
105+
106+
// Squeeze out 8 words
107+
let mut out = [0u32; 8];
108+
let mut cnt = 0;
109+
loop {
110+
for i in 0..RATE_LANES {
111+
if cnt < 8 {
112+
out[cnt] = (self.state[i] & 0xFFFF_FFFF) as u32;
113+
cnt += 1;
114+
}
115+
if cnt < 8 {
116+
out[cnt] = (self.state[i] >> 32) as u32;
117+
cnt += 1;
118+
}
119+
if cnt >= 8 {
120+
break;
121+
}
122+
}
123+
if cnt >= 8 {
124+
break;
125+
}
126+
keccak_f(&mut self.state);
127+
}
128+
out
129+
}
130+
131+
/// XOR lanes into state and run the permutation.
132+
fn absorb_block(&mut self, lanes: &[u64; RATE_LANES]) {
133+
for i in 0..RATE_LANES {
134+
self.state[i] ^= lanes[i];
135+
}
136+
keccak_f(&mut self.state);
137+
}
138+
}
139+
140+
/// Convenience: hash u32-word slice to 8-word (32-byte) digest
141+
pub fn keccak256_words(input: &[u32]) -> [u32; 8] {
142+
let mut hasher = Keccak32::new();
143+
hasher.update(input);
144+
hasher.finalize()
145+
}
146+
147+
/// The 24-round permutation Keccak-f[1600].
148+
fn keccak_f(state: &mut [u64; 25]) {
149+
for round in 0..24 {
150+
// Theta step
151+
let mut c = [0u64; 5];
152+
for x in 0..5 {
153+
c[x] = state[x] ^ state[x + 5] ^ state[x + 10] ^ state[x + 15] ^ state[x + 20];
154+
}
155+
let mut d = [0u64; 5];
156+
for x in 0..5 {
157+
d[x] = c[(x + 4) % 5] ^ c[(x + 1) % 5].rotate_left(1);
158+
}
159+
for x in 0..5 {
160+
for y in 0..5 {
161+
state[x + 5 * y] ^= d[x];
162+
}
163+
}
164+
165+
// Rho and Pi steps combined
166+
let mut b = [0u64; 25];
167+
for x in 0..5 {
168+
for y in 0..5 {
169+
let idx = x + 5 * y;
170+
let new_x = y;
171+
let new_y = (2 * x + 3 * y) % 5;
172+
let new_idx = new_x + 5 * new_y;
173+
b[new_idx] = state[idx].rotate_left(RHO_OFFSETS[idx]);
174+
}
175+
}
176+
177+
// Chi step
178+
for x in 0..5 {
179+
for y in 0..5 {
180+
let idx = x + 5 * y;
181+
state[idx] = b[idx] ^ ((!b[((x + 1) % 5) + 5 * y]) & b[((x + 2) % 5) + 5 * y]);
182+
}
183+
}
184+
185+
// Iota step
186+
state[0] ^= ROUND_CONSTANTS[round];
187+
}
188+
}
189+
190+
/// Rotation offsets for Rho step.
191+
const RHO_OFFSETS: [u32; 25] = [
192+
0, 1, 62, 28, 27, 36, 44, 6, 55, 20, 3, 10, 43, 25, 39, 41, 45, 15, 21, 8, 18, 2, 61, 56, 14,
193+
];
194+
195+
/// Round constants for the Iota step.
196+
const ROUND_CONSTANTS: [u64; 24] = [
197+
0x0000000000000001,
198+
0x0000000000008082,
199+
0x800000000000808A,
200+
0x8000000080008000,
201+
0x000000000000808B,
202+
0x0000000080000001,
203+
0x8000000080008081,
204+
0x8000000000008009,
205+
0x000000000000008A,
206+
0x0000000000000088,
207+
0x0000000080008009,
208+
0x000000008000000A,
209+
0x000000008000808B,
210+
0x800000000000008B,
211+
0x8000000000008089,
212+
0x8000000000008003,
213+
0x8000000000008002,
214+
0x8000000000000080,
215+
0x000000000000800A,
216+
0x800000008000000A,
217+
0x8000000080008081,
218+
0x8000000000008080,
219+
0x0000000080000001,
220+
0x8000000080008008,
221+
];
222+
223+
#[cfg(test)]
224+
mod tests {
225+
use super::*;
226+
227+
fn reverse_endianness(input: &[u32; 8]) -> [u32; 8] {
228+
let mut result = [0u32; 8];
229+
for i in 0..8 {
230+
result[i] = input[i].swap_bytes();
231+
}
232+
result
233+
}
234+
235+
#[test]
236+
fn test_keccak256_words() {
237+
// Test vector 1: Empty input
238+
let input = [];
239+
let expected: [u32; 8] = [
240+
0xc5d2_4601,
241+
0x86f7_233c,
242+
0x927e_7db2,
243+
0xdcc7_03c0,
244+
0xe500_b653,
245+
0xca82_273b,
246+
0x7bfa_d804,
247+
0x5d85_a470,
248+
];
249+
250+
assert_eq!(reverse_endianness(&keccak256_words(&input)), expected);
251+
252+
// Test vector 2: "16777216" - in little endian, so 0x00000001
253+
let input = [16777216];
254+
let expected = [
255+
0x51f81bcd, 0xfc324a0d, 0xff2b5bec, 0x9d92e21c, 0xbebc4d5e, 0x29d3a3d3, 0x0de3e03f,
256+
0xbeab8d7f,
257+
];
258+
259+
assert_eq!(
260+
reverse_endianness(&keccak256_words(&input)),
261+
expected,
262+
"Assertion failed! Expected: {:x?}, Got: {:x?}",
263+
expected,
264+
reverse_endianness(&keccak256_words(&input))
265+
);
266+
267+
// Test vector 3: "1, 2, 3" - in little endian, so 0x01000000 02000000 03000000
268+
let input = [1, 2, 3];
269+
let expected = [
270+
0x9186e459, 0xff7edfa5, 0xacc87375, 0x3676278c, 0xc4c65f18, 0x3513b583, 0x46230c03,
271+
0x1fd46cad,
272+
];
273+
assert_eq!(reverse_endianness(&keccak256_words(&input)), expected);
274+
}
275+
}

0 commit comments

Comments
 (0)