Skip to content

Commit 3ba1be4

Browse files
alex-ozdemiralex-ozdemir
authored
array v->k lookups, membership assertions, and witness computation in Z# (#186)
* draft: rev-lookup, in-array, witness * lint * sparse examples * fmt
1 parent 41361e4 commit 3ba1be4

Some content is hidden

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

41 files changed

+1114
-305
lines changed

‎Cargo.toml

+1-1
Original file line numberDiff line numberDiff line change
@@ -61,7 +61,7 @@ bls12_381 = "0.7"
6161
approx = "0.5.0"
6262

6363
[features]
64-
default = []
64+
default = ["bellman", "r1cs", "poly", "smt", "zok"]
6565
# frontends
6666
c = ["lang-c"]
6767
zok = ["smt", "zokrates_parser", "zokrates_pest_ast", "typed-arena", "petgraph"]

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

+10
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
from "EMBED" import value_in_array
2+
3+
// square map
4+
const field[6] SQUARES = [0, 1, 4, 9, 16, 25]
5+
6+
def main(private field y) -> field:
7+
assert(value_in_array(y, SQUARES))
8+
assert(value_in_array(y * y, SQUARES))
9+
assert(value_in_array(y * 4, SQUARES))
10+
return y

‎examples/ZoKrates/pf/mem/in_array.zok.pin

+6
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,6 @@
1+
(set_default_modulus 52435875175126190479447740508185965837690552500527637822603658699938581184513
2+
(let (
3+
(y #f4)
4+
) false ; ignored
5+
))
6+

‎examples/ZoKrates/pf/mem/in_array.zok.vin

+5
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,5 @@
1+
(set_default_modulus 52435875175126190479447740508185965837690552500527637822603658699938581184513
2+
(let (
3+
(return #f4)
4+
) false ; ignored
5+
))

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

+10
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
from "EMBED" import reverse_lookup
2+
3+
// Inputs: 0 1 2 3
4+
// Outputs: 3 0 1 2
5+
const transcript field[4] ROTATION = [3, 0, 1, 2]
6+
7+
def main(private field y, private field z) -> field:
8+
field dy = reverse_lookup(ROTATION, y)
9+
field dz = reverse_lookup(ROTATION, z)
10+
return dz * dy

‎examples/ZoKrates/pf/mem/reverse_lookup.zok.pin

+7
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,7 @@
1+
(set_default_modulus 52435875175126190479447740508185965837690552500527637822603658699938581184513
2+
(let (
3+
(y #f0)
4+
(z #f2)
5+
) false ; ignored
6+
))
7+

‎examples/ZoKrates/pf/mem/reverse_lookup.zok.vin

+7
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,7 @@
1+
(set_default_modulus 52435875175126190479447740508185965837690552500527637822603658699938581184513
2+
(let (
3+
(return #f3)
4+
) false ; ignored
5+
))
6+
7+

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

+32
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,32 @@
1+
// dense to sparse
2+
// Inputs: 00 01 10 11
3+
// Outputs: 0000 0001 0100 0101
4+
const transcript field[4] DENSE_TO_SPARSE = [0f, 1f, 4f, 5f]
5+
6+
from "EMBED" import unpack, value_in_array, reverse_lookup
7+
8+
def split_sparse_bits<N>(field x) -> field[2]:
9+
bool[2*N] bits = unpack(x)
10+
field even = 0
11+
field odd = 0
12+
for u32 i in 0..N do
13+
even = even + 4 ** i * (if bits[2*N-1-(2*i)] then 1 else 0 fi)
14+
odd = odd + 4 ** i * (if bits[2*N-1-(2*i+1)] then 1 else 0 fi)
15+
endfor
16+
return [even, odd]
17+
18+
19+
//do a bitwise AND.
20+
def main(private field x, private field y) -> field:
21+
field sy = DENSE_TO_SPARSE[y]
22+
field sx = DENSE_TO_SPARSE[x]
23+
unsafe witness field[2] split = split_sparse_bits::<2>(sx + sy)
24+
field even = split[0]
25+
field odd = split[1]
26+
assert(value_in_array(even, DENSE_TO_SPARSE))
27+
field odd_dense = reverse_lookup(DENSE_TO_SPARSE, odd)
28+
assert(sx + sy == 2 * odd + even)
29+
return odd_dense
30+
31+
32+

‎examples/ZoKrates/pf/mem/small_sparse.zok.pin

+7
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,7 @@
1+
(set_default_modulus 52435875175126190479447740508185965837690552500527637822603658699938581184513
2+
(let (
3+
(x #f3)
4+
(y #f3)
5+
) false ; ignored
6+
))
7+

‎examples/ZoKrates/pf/mem/small_sparse.zok.vin

+6
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,6 @@
1+
(set_default_modulus 52435875175126190479447740508185965837690552500527637822603658699938581184513
2+
(let (
3+
(return #f3)
4+
) false ; ignored
5+
))
6+

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

+118
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,118 @@
1+
// Examples of different SHA-esque operations being performed using sparse form
2+
// and lookup arguments
3+
4+
5+
// python -c "b=8;dtos=lambda d: sum(4**i*int(b) for i, b in enumerate(bin(d)[2:][::-1]));print(f'const transcript field[{2**b}] D_TO_S_{b} = [', ', '.join(str(dtos(i)) for i in range(2**b)), ']', sep='')"
6+
const transcript field[256] D_TO_S_8 = [0, 1, 4, 5, 16, 17, 20, 21, 64, 65, 68, 69, 80, 81, 84, 85, 256, 257, 260, 261, 272, 273, 276, 277, 320, 321, 324, 325, 336, 337, 340, 341, 1024, 1025, 1028, 1029, 1040, 1041, 1044, 1045, 1088, 1089, 1092, 1093, 1104, 1105, 1108, 1109, 1280, 1281, 1284, 1285, 1296, 1297, 1300, 1301, 1344, 1345, 1348, 1349, 1360, 1361, 1364, 1365, 4096, 4097, 4100, 4101, 4112, 4113, 4116, 4117, 4160, 4161, 4164, 4165, 4176, 4177, 4180, 4181, 4352, 4353, 4356, 4357, 4368, 4369, 4372, 4373, 4416, 4417, 4420, 4421, 4432, 4433, 4436, 4437, 5120, 5121, 5124, 5125, 5136, 5137, 5140, 5141, 5184, 5185, 5188, 5189, 5200, 5201, 5204, 5205, 5376, 5377, 5380, 5381, 5392, 5393, 5396, 5397, 5440, 5441, 5444, 5445, 5456, 5457, 5460, 5461, 16384, 16385, 16388, 16389, 16400, 16401, 16404, 16405, 16448, 16449, 16452, 16453, 16464, 16465, 16468, 16469, 16640, 16641, 16644, 16645, 16656, 16657, 16660, 16661, 16704, 16705, 16708, 16709, 16720, 16721, 16724, 16725, 17408, 17409, 17412, 17413, 17424, 17425, 17428, 17429, 17472, 17473, 17476, 17477, 17488, 17489, 17492, 17493, 17664, 17665, 17668, 17669, 17680, 17681, 17684, 17685, 17728, 17729, 17732, 17733, 17744, 17745, 17748, 17749, 20480, 20481, 20484, 20485, 20496, 20497, 20500, 20501, 20544, 20545, 20548, 20549, 20560, 20561, 20564, 20565, 20736, 20737, 20740, 20741, 20752, 20753, 20756, 20757, 20800, 20801, 20804, 20805, 20816, 20817, 20820, 20821, 21504, 21505, 21508, 21509, 21520, 21521, 21524, 21525, 21568, 21569, 21572, 21573, 21584, 21585, 21588, 21589, 21760, 21761, 21764, 21765, 21776, 21777, 21780, 21781, 21824, 21825, 21828, 21829, 21840, 21841, 21844, 21845]
7+
8+
const transcript field[8] D_TO_S_3 = [0, 1, 4, 5, 16, 17, 20, 21]
9+
10+
const transcript field[8] D_3 = [0, 1, 2, 3, 4, 5, 6, 7]
11+
12+
// python -c "b=8;dtos=lambda d: sum(4**i*int(b) for i, b in enumerate(bin(d)[2:][::-1]));print(f'const field S_ONES_{b} = {dtos(2**b-1)}');print(f'const field D_ONES_{b} = {2**b-1}')"
13+
const field S_ONES_8 = 21845
14+
const field D_ONES_8 = 255
15+
16+
from "EMBED" import unpack, value_in_array, reverse_lookup, fits_in_bits
17+
18+
// split a number into (unchecked) high and low bits
19+
def unsafe_split<LOW_BITS,HIGH_BITS>(field x) -> field[2]:
20+
bool[LOW_BITS+HIGH_BITS] bits = unpack(x)
21+
field low = 0
22+
field high = 0
23+
for u32 i in 0..LOW_BITS do
24+
low = low + 2 ** i * (if bits[LOW_BITS+HIGH_BITS-1-i] then 1 else 0 fi)
25+
endfor
26+
for u32 i in LOW_BITS..HIGH_BITS do
27+
high = high + 2 ** i * (if bits[LOW_BITS+HIGH_BITS-1-i] then 1 else 0 fi)
28+
endfor
29+
return [low, high]
30+
31+
// split a 2N bit number into (unchecked) even and odd bits (in sparse form)
32+
def unsafe_separate_sparse<N>(field x) -> field[2]:
33+
bool[2*N] bits = unpack(x)
34+
field even = 0
35+
field odd = 0
36+
for u32 i in 0..N do
37+
even = even + 4 ** i * (if bits[2*N-1-(2*i)] then 1 else 0 fi)
38+
odd = odd + 4 ** i * (if bits[2*N-1-(2*i+1)] then 1 else 0 fi)
39+
endfor
40+
return [even, odd]
41+
42+
struct Dual {
43+
field s
44+
field d
45+
}
46+
47+
// convert a dense 8-bit value to dual form; ensures the value fits in 8 bits.
48+
def dense_to_dual_8(field x) -> Dual:
49+
field s = D_TO_S_8[x]
50+
return Dual {s: s, d: x}
51+
52+
// get the even bits of a 16-bit value in dual form; ensures the value fits in 16 bits.
53+
def split_even_dual_8(field x) -> Dual:
54+
unsafe witness field[2] split = unsafe_separate_sparse::<8>(x)
55+
field even = split[0]
56+
field odd = split[1]
57+
assert(x == 2 * odd + even)
58+
field even_d = reverse_lookup(D_TO_S_8, even)
59+
assert(value_in_array(odd, D_TO_S_8))
60+
return Dual { s: even, d: even_d }
61+
62+
// get the odd bits of a 16-bit value in dual form; ensures the value fits in 16 bits.
63+
def split_odd_dual_8(field x) -> Dual:
64+
unsafe witness field[2] split = unsafe_separate_sparse::<8>(x)
65+
field even = split[0]
66+
field odd = split[1]
67+
assert(x == 2 * odd + even)
68+
field odd_d = reverse_lookup(D_TO_S_8, odd)
69+
assert(value_in_array(even, D_TO_S_8))
70+
return Dual { s: odd, d: odd_d }
71+
72+
// get the even and odd bits of a 16-bit value in dual form; ensures the value fits in 16 bits.
73+
def split_both_dual_8(field x) -> Dual[2]:
74+
unsafe witness field[2] split = unsafe_separate_sparse::<8>(x)
75+
field even = split[0]
76+
field odd = split[1]
77+
field odd_d = reverse_lookup(D_TO_S_8, odd)
78+
field even_d = reverse_lookup(D_TO_S_8, even)
79+
return [Dual { s: even, d: even_d }, Dual { s: odd, d: odd_d }]
80+
81+
def and_8(Dual x, Dual y) -> Dual:
82+
return split_odd_dual_8(x.s + y.s)
83+
84+
def maj_8(Dual x, Dual y, Dual z) -> Dual:
85+
return split_odd_dual_8(x.s + y.s + z.s)
86+
87+
def xor_8(Dual x, Dual y, Dual z) -> Dual:
88+
return split_even_dual_8(x.s + y.s + z.s)
89+
90+
def not_8(Dual x) -> Dual:
91+
return Dual { s: S_ONES_8 - x.s, d: D_ONES_8 - x.d }
92+
93+
def or_8(Dual x, Dual y) -> Dual:
94+
return not_8(and_8(not_8(x), not_8(y)))
95+
96+
// split s into 8 low bits and 3 high bits, and return the low bits
97+
// in dual form.
98+
def normalize_sum_8(field s) -> Dual:
99+
unsafe witness field[2] split = unsafe_split::<8, 3>(s)
100+
field low = split[0]
101+
field high = split[1]
102+
assert(value_in_array(high, D_3))
103+
return dense_to_dual_8(low)
104+
105+
//do a bitwise AND.
106+
def main(private field dense_x, private field dense_y) -> field:
107+
Dual z = dense_to_dual_8(0)
108+
Dual x = dense_to_dual_8(dense_x) // 10001000 (136)
109+
Dual y = dense_to_dual_8(dense_y) // 10000001 (129)
110+
Dual a = and_8(x, y) // 10000000
111+
Dual b = or_8(x, y) // 10001001
112+
Dual c = xor_8(x, y, z) // 00001001
113+
Dual d = maj_8(x, y, c) // 10001001
114+
Dual s = normalize_sum_8(d.d + c.d + b.d + a.d) // 10011011 (128+27=155)
115+
return s.d
116+
117+
118+

‎examples/ZoKrates/pf/mem/sparse.zok.pin

+7
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,7 @@
1+
(set_default_modulus 52435875175126190479447740508185965837690552500527637822603658699938581184513
2+
(let (
3+
(dense_x #f136)
4+
(dense_y #f129)
5+
) false ; ignored
6+
))
7+

‎examples/ZoKrates/pf/mem/sparse.zok.vin

+6
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,6 @@
1+
(set_default_modulus 52435875175126190479447740508185965837690552500527637822603658699938581184513
2+
(let (
3+
(return #f155)
4+
) false ; ignored
5+
))
6+

‎examples/circ.rs

+2
Original file line numberDiff line numberDiff line change
@@ -261,6 +261,7 @@ fn main() {
261261
Mode::Proof | Mode::ProofOfHighValue(_) => {
262262
let mut opts = Vec::new();
263263

264+
opts.push(Opt::DeskolemizeWitnesses);
264265
opts.push(Opt::ScalarizeVars);
265266
opts.push(Opt::Flatten);
266267
opts.push(Opt::Sha);
@@ -270,6 +271,7 @@ fn main() {
270271
opts.push(Opt::ConstantFold(Box::new([])));
271272
opts.push(Opt::Obliv);
272273
// The obliv elim pass produces more tuples, that must be eliminated
274+
opts.push(Opt::SetMembership);
273275
opts.push(Opt::PersistentRam);
274276
opts.push(Opt::VolatileRam);
275277
opts.push(Opt::SkolemizeChallenges);

‎scripts/ram_test.zsh

+6-1
Original file line numberDiff line numberDiff line change
@@ -8,7 +8,7 @@ disable -r time
88
# cargo build --features "zok smt bellman" --example circ --example zk
99

1010
MODE=release
11-
MODE=debug
11+
# MODE=debug
1212
BIN=./target/$MODE/examples/circ
1313
ZK_BIN=./target/$MODE/examples/zk
1414

@@ -82,6 +82,11 @@ ram_test ./examples/ZoKrates/pf/mem/volatile.zok mirage ""
8282
ram_test ./examples/ZoKrates/pf/mem/volatile_struct.zok mirage ""
8383
ram_test ./examples/ZoKrates/pf/mem/arr_of_str.zok mirage ""
8484
ram_test ./examples/ZoKrates/pf/mem/arr_of_str_of_arr.zok mirage ""
85+
ram_test ./examples/ZoKrates/pf/mem/in_array.zok mirage ""
86+
ram_test ./examples/ZoKrates/pf/mem/small_sparse.zok mirage ""
87+
ram_test ./examples/ZoKrates/pf/mem/reverse_lookup.zok mirage ""
88+
ram_test ./examples/ZoKrates/pf/mem/sparse.zok mirage ""
89+
8590

8691
# challenges
8792
ram_test ./examples/ZoKrates/pf/chall/simple.zok mirage ""

0 commit comments

Comments
 (0)