Skip to content

Commit 0b88154

Browse files
alex-ozdemiralex-ozdemir
authored
Implement ROM-checking based on Haboeck's lookup argument (#185)
1 parent 2ebd0a1 commit 0b88154

File tree

16 files changed

+526
-131
lines changed

16 files changed

+526
-131
lines changed

‎Cargo.toml

+1-1
Original file line numberDiff line numberDiff line change
@@ -64,7 +64,7 @@ approx = "0.5.0"
6464
default = []
6565
# frontends
6666
c = ["lang-c"]
67-
zok = ["zokrates_parser", "zokrates_pest_ast", "typed-arena", "petgraph"]
67+
zok = ["smt", "zokrates_parser", "zokrates_pest_ast", "typed-arena", "petgraph"]
6868
datalog = ["pest", "pest-ast", "pest_derive", "from-pest", "lazy_static"]
6969
# backends
7070
smt = ["rsmt2", "ieee754"]

‎circ_opt/README.md

+26
Original file line numberDiff line numberDiff line change
@@ -129,6 +129,16 @@ Options:
129129
- waksman: Use the AS-Waksman network
130130
- msh: Use the (keyed) multi-set hash
131131

132+
--ram-rom <ROM>
133+
ROM approach
134+
135+
[env: RAM_ROM=]
136+
[default: haboeck]
137+
138+
Possible values:
139+
- haboeck: Use Haboeck's argument
140+
- permute: Use permute-and-check
141+
132142
--fmt-use-default-field <USE_DEFAULT_FIELD>
133143
Which field to use
134144
@@ -210,6 +220,8 @@ Options:
210220
How to argue that indices are only repeated in blocks [env: RAM_INDEX=] [default: uniqueness] [possible values: sort, uniqueness]
211221
--ram-permutation <PERMUTATION>
212222
How to argue that indices are only repeated in blocks [env: RAM_PERMUTATION=] [default: msh] [possible values: waksman, msh]
223+
--ram-rom <ROM>
224+
ROM approach [env: RAM_ROM=] [default: haboeck] [possible values: haboeck, permute]
213225
--fmt-use-default-field <USE_DEFAULT_FIELD>
214226
Which field to use [env: FMT_USE_DEFAULT_FIELD=] [default: true] [possible values: true, false]
215227
--fmt-hide-field <HIDE_FIELD>
@@ -253,6 +265,7 @@ BinaryOpt {
253265
range: Sort,
254266
index: Uniqueness,
255267
permutation: Msh,
268+
rom: Haboeck,
256269
},
257270
fmt: FmtOpt {
258271
use_default_field: true,
@@ -298,6 +311,7 @@ BinaryOpt {
298311
range: Sort,
299312
index: Uniqueness,
300313
permutation: Msh,
314+
rom: Haboeck,
301315
},
302316
fmt: FmtOpt {
303317
use_default_field: true,
@@ -341,6 +355,7 @@ BinaryOpt {
341355
range: Sort,
342356
index: Uniqueness,
343357
permutation: Msh,
358+
rom: Haboeck,
344359
},
345360
fmt: FmtOpt {
346361
use_default_field: true,
@@ -384,6 +399,7 @@ BinaryOpt {
384399
range: Sort,
385400
index: Uniqueness,
386401
permutation: Msh,
402+
rom: Haboeck,
387403
},
388404
fmt: FmtOpt {
389405
use_default_field: true,
@@ -427,6 +443,7 @@ BinaryOpt {
427443
range: Sort,
428444
index: Uniqueness,
429445
permutation: Msh,
446+
rom: Haboeck,
430447
},
431448
fmt: FmtOpt {
432449
use_default_field: true,
@@ -470,6 +487,7 @@ BinaryOpt {
470487
range: Sort,
471488
index: Uniqueness,
472489
permutation: Msh,
490+
rom: Haboeck,
473491
},
474492
fmt: FmtOpt {
475493
use_default_field: true,
@@ -513,6 +531,7 @@ BinaryOpt {
513531
range: Sort,
514532
index: Uniqueness,
515533
permutation: Msh,
534+
rom: Haboeck,
516535
},
517536
fmt: FmtOpt {
518537
use_default_field: true,
@@ -556,6 +575,7 @@ BinaryOpt {
556575
range: Sort,
557576
index: Uniqueness,
558577
permutation: Msh,
578+
rom: Haboeck,
559579
},
560580
fmt: FmtOpt {
561581
use_default_field: true,
@@ -602,6 +622,7 @@ BinaryOpt {
602622
range: Sort,
603623
index: Uniqueness,
604624
permutation: Msh,
625+
rom: Haboeck,
605626
},
606627
fmt: FmtOpt {
607628
use_default_field: true,
@@ -646,6 +667,7 @@ BinaryOpt {
646667
range: Sort,
647668
index: Uniqueness,
648669
permutation: Msh,
670+
rom: Haboeck,
649671
},
650672
fmt: FmtOpt {
651673
use_default_field: true,
@@ -692,6 +714,7 @@ BinaryOpt {
692714
range: Sort,
693715
index: Uniqueness,
694716
permutation: Msh,
717+
rom: Haboeck,
695718
},
696719
fmt: FmtOpt {
697720
use_default_field: true,
@@ -736,6 +759,7 @@ BinaryOpt {
736759
range: Sort,
737760
index: Uniqueness,
738761
permutation: Msh,
762+
rom: Haboeck,
739763
},
740764
fmt: FmtOpt {
741765
use_default_field: true,
@@ -782,6 +806,7 @@ BinaryOpt {
782806
range: Sort,
783807
index: Uniqueness,
784808
permutation: Msh,
809+
rom: Haboeck,
785810
},
786811
fmt: FmtOpt {
787812
use_default_field: true,
@@ -826,6 +851,7 @@ BinaryOpt {
826851
range: Sort,
827852
index: Uniqueness,
828853
permutation: Msh,
854+
rom: Haboeck,
829855
},
830856
fmt: FmtOpt {
831857
use_default_field: true,

‎circ_opt/src/lib.rs

+23
Original file line numberDiff line numberDiff line change
@@ -239,6 +239,14 @@ pub struct RamOpt {
239239
default_value = "msh"
240240
)]
241241
pub permutation: PermutationStrategy,
242+
/// ROM approach
243+
#[arg(
244+
long = "ram-rom",
245+
env = "RAM_ROM",
246+
value_enum,
247+
default_value = "haboeck"
248+
)]
249+
pub rom: RomStrategy,
242250
}
243251

244252
#[derive(ValueEnum, Debug, PartialEq, Eq, Clone, Copy)]
@@ -286,6 +294,21 @@ impl Default for PermutationStrategy {
286294
}
287295
}
288296

297+
#[derive(ValueEnum, Debug, PartialEq, Eq, Clone, Copy)]
298+
/// How to argue that accesses have been permuted
299+
pub enum RomStrategy {
300+
/// Use Haboeck's argument
301+
Haboeck,
302+
/// Use permute-and-check
303+
Permute,
304+
}
305+
306+
impl Default for RomStrategy {
307+
fn default() -> Self {
308+
RomStrategy::Haboeck
309+
}
310+
}
311+
289312
/// Options for the prime field used
290313
#[derive(Args, Debug, Clone, PartialEq, Eq)]
291314
pub struct FmtOpt {

‎examples/ZoKrates/pf/mem/rom.zok

+22
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,22 @@
1+
const u32 VAL_LEN = 3
2+
const u32 RAM_LEN = 20
3+
const u32 ACCESSES = 400
4+
5+
struct Val {
6+
field x
7+
field y
8+
}
9+
10+
const transcript Val[RAM_LEN] array = [Val{x: 0, y: 0}, ...[Val{x: 10, y: 10}; RAM_LEN-1]]
11+
12+
def main(private field[ACCESSES] y) -> field:
13+
field result = 0
14+
15+
for u32 i in 0..ACCESSES do
16+
Val v = array[y[i]]
17+
result = result + v.x + v.y
18+
endfor
19+
return result
20+
21+
22+

‎scripts/ram_test.zsh

+12
Original file line numberDiff line numberDiff line change
@@ -50,6 +50,15 @@ function transcript_type_test {
5050
fi
5151
}
5252

53+
function cs_count_test {
54+
ex_name=$1
55+
cs_upper_bound=$2
56+
rm -rf P V pi
57+
output=$($BIN $ex_name r1cs --action count |& cat)
58+
n_constraints=$(echo "$output" | grep 'Final R1cs size:' | grep -Eo '\b[0-9]+\b')
59+
[[ $n_constraints -lt $cs_upper_bound ]] || (echo "Got $n_constraints, expected < $cs_upper_bound" && exit 1)
60+
}
61+
5362
transcript_count_test ./examples/ZoKrates/pf/mem/volatile.zok 1
5463
transcript_count_test ./examples/ZoKrates/pf/mem/two_level_ptr.zok 1
5564
transcript_count_test ./examples/ZoKrates/pf/mem/volatile_struct.zok 1
@@ -59,6 +68,9 @@ transcript_count_test ./examples/ZoKrates/pf/mem/arr_of_str_of_arr.zok 1
5968
transcript_type_test ./examples/ZoKrates/pf/mem/volatile_struct.zok "RAM"
6069
transcript_type_test ./examples/ZoKrates/pf/mem/two_level_ptr.zok "covering ROM"
6170

71+
# A=400; N=20; L=2; expected cost ~= N + A(L+1) = 1220
72+
cs_count_test ./examples/ZoKrates/pf/mem/rom.zok 1230
73+
6274
ram_test ./examples/ZoKrates/pf/mem/two_level_ptr.zok groth16 "--ram-permutation waksman --ram-index sort --ram-range bit-split"
6375
ram_test ./examples/ZoKrates/pf/mem/volatile.zok groth16 "--ram-permutation waksman --ram-index sort --ram-range bit-split"
6476
# waksman is broken for non-scalar array values

‎src/ir/opt/mem/ram.rs

+5-1
Original file line numberDiff line numberDiff line change
@@ -71,12 +71,13 @@ pub struct AccessCfg {
7171
split_times: bool,
7272
waksman: bool,
7373
covering_rom: bool,
74+
haboeck: bool,
7475
}
7576

7677
impl AccessCfg {
7778
/// Create a new configuration
7879
pub fn new(field: FieldT, opt: RamOpt, create: bool) -> Self {
79-
use circ_opt::{IndexStrategy, PermutationStrategy, RangeStrategy};
80+
use circ_opt::{IndexStrategy, PermutationStrategy, RangeStrategy, RomStrategy};
8081
Self {
8182
false_: bool_lit(false),
8283
true_: bool_lit(true),
@@ -88,6 +89,7 @@ impl AccessCfg {
8889
split_times: opt.range == RangeStrategy::BitSplit,
8990
waksman: opt.permutation == PermutationStrategy::Waksman,
9091
covering_rom: false,
92+
haboeck: opt.rom == RomStrategy::Haboeck,
9193
}
9294
}
9395
/// Create a default configuration, with this field.
@@ -103,6 +105,7 @@ impl AccessCfg {
103105
split_times: false,
104106
waksman: false,
105107
covering_rom: false,
108+
haboeck: true,
106109
}
107110
}
108111
/// Create a new default configuration
@@ -278,6 +281,7 @@ impl Access {
278281
}
279282
}
280283

284+
/// Serialize a value as field elements.
281285
fn val_to_field_elements(val: &Term, c: &AccessCfg, out: &mut Vec<Term>) {
282286
match check(val) {
283287
Sort::Field(_) | Sort::Bool | Sort::BitVector(_) => out.push(scalar_to_field(val, c)),

0 commit comments

Comments
 (0)