Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Add support for ZoKrates with curly brackets (wip) #211

Merged
merged 28 commits into from
Feb 12, 2025
Merged
Show file tree
Hide file tree
Changes from 14 commits
Commits
Show all changes
28 commits
Select commit Hold shift + click to select a range
26f3e65
Add boilerplate code for a new Zokrates frontend (curcly brackets)
StefanosChaliasos Oct 30, 2024
bb5f2c5
Update the Zokrates standard library and pest to the newer version (c…
StefanosChaliasos Oct 30, 2024
a13a18e
Update tests and examples for ZoKratesCurly
StefanosChaliasos Oct 30, 2024
ce9ddbf
Implement the ZSharpCurlyFE
StefanosChaliasos Oct 30, 2024
95e58e3
Apply fmt
StefanosChaliasos Oct 30, 2024
cdbc804
Add zcxi in Cargo.toml
StefanosChaliasos Oct 30, 2024
1121700
Fix linting errors
StefanosChaliasos Oct 30, 2024
33f0075
Correctly implement tuple for zsharpcurly
StefanosChaliasos Nov 7, 2024
11aba74
Update error message for MPC support
StefanosChaliasos Nov 7, 2024
3309a0d
Apply fmt
StefanosChaliasos Nov 7, 2024
b2c08da
Remove commented out code
StefanosChaliasos Nov 7, 2024
9981366
Fix linting error
StefanosChaliasos Nov 7, 2024
36497e1
Fix script for processing zcx tests
StefanosChaliasos Dec 13, 2024
79e1d94
Handle assembly assignments and constraints
StefanosChaliasos Dec 13, 2024
788fb51
Remove deprecated comment
StefanosChaliasos Dec 13, 2024
7f284b6
Add support for AssignConstrain (<==)
StefanosChaliasos Dec 13, 2024
2629341
Remove print stmts
StefanosChaliasos Dec 13, 2024
3a32dcb
Add support for field_to_bool_unsafe
StefanosChaliasos Jan 21, 2025
f442e2b
Uncomment tests and fmt changes
StefanosChaliasos Jan 21, 2025
8ece447
Fix field_to_bool_unsafe and some linting errors
StefanosChaliasos Jan 23, 2025
94db4be
Fix type alias issue in type checking
StefanosChaliasos Jan 23, 2025
2704df6
Apply fmt
StefanosChaliasos Jan 23, 2025
51b8bf2
Fix linting errors
StefanosChaliasos Jan 23, 2025
d4a1644
Fix linting errors
StefanosChaliasos Jan 23, 2025
354d0fe
fmt changes
StefanosChaliasos Jan 23, 2025
78499d9
README: rm circom, add pointer to old implementation
alex-ozdemir Feb 6, 2025
7836f55
Fix the build (#221)
alex-ozdemir Feb 10, 2025
0ffdcb5
Extend input declarations in Z# to support structs (#219)
lorenzorota Feb 11, 2025
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
The table of contents is too big for display.
Diff view
Diff view
  •  
  •  
  •  
223 changes: 168 additions & 55 deletions Cargo.lock

Large diffs are not rendered by default.

7 changes: 7 additions & 0 deletions Cargo.toml
Original file line number Diff line number Diff line change
Expand Up @@ -20,6 +20,8 @@ rsmt2 = { version = "0.14", optional = true }
ieee754 = { version = "0.2", optional = true}
zokrates_parser = { path = "third_party/ZoKrates/zokrates_parser", optional = true }
zokrates_pest_ast = { path = "third_party/ZoKrates/zokrates_pest_ast", optional = true }
zokrates_curly_parser = { package = "zokrates_parser", path = "third_party/ZoKratesCurly/zokrates_parser", optional = true }
zokrates_curly_pest_ast = { package = "zokrates_pest_ast", path = "third_party/ZoKratesCurly/zokrates_pest_ast", optional = true }
typed-arena = { version = "2.0", optional = true }
log = "0.4"
thiserror = "1.0"
Expand Down Expand Up @@ -65,6 +67,7 @@ default = []
# frontends
c = ["lang-c"]
zok = ["smt", "zokrates_parser", "zokrates_pest_ast", "typed-arena", "petgraph"]
zokc = ["smt", "zokrates_curly_parser", "zokrates_curly_pest_ast", "typed-arena", "petgraph"]
datalog = ["pest", "pest-ast", "pest_derive", "from-pest", "lazy_static"]
# backends
smt = ["rsmt2", "ieee754"]
Expand All @@ -90,6 +93,10 @@ required-features = ["bellman", "poly"]
name = "zxi"
required-features = ["smt", "zok"]

[[example]]
name = "zcxi"
required-features = ["smt", "zokc"]

[[example]]
name = "zxc"
required-features = ["smt", "zok"]
Expand Down
1 change: 1 addition & 0 deletions driver.py
Original file line number Diff line number Diff line change
Expand Up @@ -16,6 +16,7 @@
"r1cs",
"smt",
"zok",
"zokc",
"datalog",
"bellman",
"spartan",
Expand Down
3 changes: 3 additions & 0 deletions examples/ZoKratesCurly/mpc/unit_tests/2pc_millionaires.zok
Original file line number Diff line number Diff line change
@@ -0,0 +1,3 @@
def main(private u32 a, private u32 b) -> bool {
return a < b;
}
11 changes: 11 additions & 0 deletions examples/ZoKratesCurly/mpc/unit_tests/2pc_structs.zok
Original file line number Diff line number Diff line change
@@ -0,0 +1,11 @@
struct Pt {
u32 x;
u32 y;
}

def main(private u32 a, private u32 b) -> u32 {
Pt c = Pt {x: 0, y: 1};
c.x = a;
c.y = b;
return c.y + c.x;
}
Original file line number Diff line number Diff line change
@@ -0,0 +1,3 @@
def main(private u32 a, private u32 b) -> u32 {
return a + b;
}
Original file line number Diff line number Diff line change
@@ -0,0 +1,3 @@
def main(private u32 a, private u32 b) -> bool {
return a == b;
}
Original file line number Diff line number Diff line change
@@ -0,0 +1,3 @@
def main(private u32 a, private u32 b) -> bool {
return a >= b;
}
Original file line number Diff line number Diff line change
@@ -0,0 +1,3 @@
def main(private u32 a, private u32 b) -> bool {
return a > b;
}
Original file line number Diff line number Diff line change
@@ -0,0 +1,3 @@
def main(private u32 a, private u32 b) -> bool {
return a <= b;
}
Original file line number Diff line number Diff line change
@@ -0,0 +1,3 @@
def main(private u32 a, private u32 b) -> bool {
return a < b;
}
Original file line number Diff line number Diff line change
@@ -0,0 +1,3 @@
def main(private u32 a, private u32 b) -> u32 {
return a * b;
}
Original file line number Diff line number Diff line change
@@ -0,0 +1,3 @@
def main(private u32 a, private u32 b, u32 v) -> u32 {
return a * b + v;
}
Original file line number Diff line number Diff line change
@@ -0,0 +1,3 @@
def main(private u32 a, private u32 b) -> u32 {
return a - b;
}
Original file line number Diff line number Diff line change
@@ -0,0 +1,3 @@
def main(private u32 a, private u32 b) -> u32[2] {
return [a, b];
}
Original file line number Diff line number Diff line change
@@ -0,0 +1,4 @@
def main(private u32 a, private u32 b) -> u32 {
u32[2] c = [a, b];
return c[0] + c[1];
}
Original file line number Diff line number Diff line change
@@ -0,0 +1,3 @@
def main(private u32 a, private u32 b) -> u32 {
return a & b;
}
Original file line number Diff line number Diff line change
@@ -0,0 +1,3 @@
def main(private u32 a, private u32 b) -> u32 {
return a | b;
}
Original file line number Diff line number Diff line change
@@ -0,0 +1,3 @@
def main(private u32 a, private u32 b) -> u32 {
return a ^ b;
}
Original file line number Diff line number Diff line change
@@ -0,0 +1,3 @@
def main(private bool a, private bool b) -> bool {
return a && b;
}
Original file line number Diff line number Diff line change
@@ -0,0 +1,3 @@
def main(private bool a, private bool b) -> bool {
return a == b;
}
Original file line number Diff line number Diff line change
@@ -0,0 +1,3 @@
def main(private bool a, private bool b) -> bool {
return a || b;
}
Original file line number Diff line number Diff line change
@@ -0,0 +1,4 @@
def main(private u32 a, private u32 b) -> u32 {
u32 c = 1;
return a + b + c;
}
Original file line number Diff line number Diff line change
@@ -0,0 +1,4 @@
def main(private bool a, private bool b) -> bool {
bool c = true;
return a == c;
}
Original file line number Diff line number Diff line change
@@ -0,0 +1,7 @@
def add(u32 a, u32 b) -> u32 {
return a + b;
}

def main(private u32 a, private u32 b) -> u32 {
return add(a, b) + add(a, b);
}
Original file line number Diff line number Diff line change
@@ -0,0 +1,7 @@
def sub(u32 b, u32 a) -> u32 {
return a - b;
}

def main(private u32 a, private u32 b) -> u32 {
return sub(b, a);
}
Original file line number Diff line number Diff line change
@@ -0,0 +1,3 @@
def main(private u32 a, private u32 b, public bool sel) -> u32 {
return if sel { a } else { b };
}
Original file line number Diff line number Diff line change
@@ -0,0 +1,3 @@
def main(private bool a, private bool b, public bool sel) -> bool {
return if sel { a } else { b };
}
Original file line number Diff line number Diff line change
@@ -0,0 +1,3 @@
def main(private u32 a, private u32 b, public bool sel) -> u32 {
return if sel { a } else { b };
}
Original file line number Diff line number Diff line change
@@ -0,0 +1,6 @@
def main(private u32 a, private u32 b) -> u32 {
for u32 i in 0..4 {
a = a + b;
}
return a;
}
Original file line number Diff line number Diff line change
@@ -0,0 +1,7 @@
def main(private u32 a, private u32 b) -> u32 {
u32 mut res = 0x00000000;
for u32 i in 0..5 {
res = res + i;
}
return res;
}
Original file line number Diff line number Diff line change
@@ -0,0 +1,3 @@
def main(private u32 a, private u32 b, private u32 c) -> u32 {
return a + b + c;
}
Original file line number Diff line number Diff line change
@@ -0,0 +1,3 @@
def main(private bool a, private bool b, private bool c) -> bool {
return a && b && c;
}
4 changes: 4 additions & 0 deletions examples/ZoKratesCurly/mpc/unit_tests/shift_tests/2pc_lhs.zok
Original file line number Diff line number Diff line change
@@ -0,0 +1,4 @@
def main(private u32 a, private u32 b) -> u32 {
u32 c = 0x00000001;
return a << c;
}
4 changes: 4 additions & 0 deletions examples/ZoKratesCurly/mpc/unit_tests/shift_tests/2pc_rhs.zok
Original file line number Diff line number Diff line change
@@ -0,0 +1,4 @@
def main(private u32 a, private u32 b) -> u32 {
u32 c = 0x00000001;
return a >> c;
}
3 changes: 3 additions & 0 deletions examples/ZoKratesCurly/opt/3_plus_opt.zok
Original file line number Diff line number Diff line change
@@ -0,0 +1,3 @@
def main(private u8 x) -> u8 {
return x + x + x;
}
3 changes: 3 additions & 0 deletions examples/ZoKratesCurly/opt/id_opt.zok
Original file line number Diff line number Diff line change
@@ -0,0 +1,3 @@
def main(private u8 x) -> u8 {
return x;
}
12 changes: 12 additions & 0 deletions examples/ZoKratesCurly/opt/log.zok
Original file line number Diff line number Diff line change
@@ -0,0 +1,12 @@
def u8log2(u8 x) -> u8 {
u8 mut acc = 0x00;
for field i in 0..8 {
acc = acc + if x != 0x00 { 0x01 } else { 0x00 };
x = x >> 1;
}
return acc;
}

def main(private u8 x) -> u8 {
return x + u8log2(x);
}
12 changes: 12 additions & 0 deletions examples/ZoKratesCurly/opt/log16.zok
Original file line number Diff line number Diff line change
@@ -0,0 +1,12 @@
def u16log2(x: u16) -> u16 {
u16 mut acc = 0x0000;
for field i in 0..16 {
acc = acc + if x != 0x0000 { 0x0001 } else { 0x0000 };
x = x >> 1;
}
return acc;
}

def main(private x: u16) -> u16 {
return x + u16log2(x);
}
3 changes: 3 additions & 0 deletions examples/ZoKratesCurly/opt/mult_opt.zok
Original file line number Diff line number Diff line change
@@ -0,0 +1,3 @@
def main(private u8 x, private u8 y) -> u8 {
return x * y;
}
3 changes: 3 additions & 0 deletions examples/ZoKratesCurly/opt/plus_3_opt.zok
Original file line number Diff line number Diff line change
@@ -0,0 +1,3 @@
def main(private u8 x) -> u8 {
return 0x03 + x;
}
3 changes: 3 additions & 0 deletions examples/ZoKratesCurly/opt/times_2_opt.zok
Original file line number Diff line number Diff line change
@@ -0,0 +1,3 @@
def main(private u8 x) -> u8 {
return 0x02 * x;
}
3 changes: 3 additions & 0 deletions examples/ZoKratesCurly/opt/times_2_u32_opt.zok
Original file line number Diff line number Diff line change
@@ -0,0 +1,3 @@
def main(private u32 x) -> u32 {
return 0x00000002 * x;
}
3 changes: 3 additions & 0 deletions examples/ZoKratesCurly/opt/times_3_opt.zok
Original file line number Diff line number Diff line change
@@ -0,0 +1,3 @@
def main(private u8 x) -> u8 {
return 0x03 * x;
}
7 changes: 7 additions & 0 deletions examples/ZoKratesCurly/pf/2024_05_24_benny_bug.zok.pin
Original file line number Diff line number Diff line change
@@ -0,0 +1,7 @@
(set_default_modulus 52435875175126190479447740508185965837690552500527637822603658699938581184513
(let (
(x #f6)
) false ; ignored
))


7 changes: 7 additions & 0 deletions examples/ZoKratesCurly/pf/2024_05_24_benny_bug.zok.vin
Original file line number Diff line number Diff line change
@@ -0,0 +1,7 @@
(set_default_modulus 52435875175126190479447740508185965837690552500527637822603658699938581184513
(let (
(x #f6)
(return #f0)
) false ; ignored
))

6 changes: 6 additions & 0 deletions examples/ZoKratesCurly/pf/2024_05_31_benny_bug.zok.pin
Original file line number Diff line number Diff line change
@@ -0,0 +1,6 @@
(set_default_modulus 52435875175126190479447740508185965837690552500527637822603658699938581184513
(let (
(x #f6)
) false ; ignored
))

7 changes: 7 additions & 0 deletions examples/ZoKratesCurly/pf/2024_05_31_benny_bug.zok.vin
Original file line number Diff line number Diff line change
@@ -0,0 +1,7 @@
(set_default_modulus 52435875175126190479447740508185965837690552500527637822603658699938581184513
(let (
(x #f6)
(return #f6)
) false ; ignored
))

23 changes: 23 additions & 0 deletions examples/ZoKratesCurly/pf/2024_06_02_chad_bug.zok
Original file line number Diff line number Diff line change
@@ -0,0 +1,23 @@
struct BigNat_init_quotient<Qm1, Lp1> {
field[Qm1][Lp1] limbs;
field last_limb;
}

struct BigNat_init<N, Lp1> {
field[N][Lp1] limbs;
}
struct BigNatModMult_init<Qm1, Lp1, ZG, CL> {
BigNat_init_quotient<Qm1, Lp1> quotient_init;
BigNat_init<ZG, CL> carry_init;
}

const u32 Qm1 = 7;
const u32 Lp1 = 4;
const u32 ZG = 2;
const u32 CL = 5;

def main(private BigNatModMult_init<Qm1,Lp1,ZG,CL>[1] intermediate_mod) -> bool {
BigNat_init<ZG, CL> carry = intermediate_mod[0].carry_init;
assert(carry.limbs[0][0] == 1);
return true;
}
19 changes: 19 additions & 0 deletions examples/ZoKratesCurly/pf/2024_07_01_chad_bug_wit.zok
Original file line number Diff line number Diff line change
@@ -0,0 +1,19 @@
def unsafe_baz<M>(field input) -> field[M] {
return [input; M];
}

def foo<M>(field input) -> field[M] {
unsafe witness field[M] inputs = unsafe_baz::<M>(input);
assert(inputs[0] == input);
return inputs;
}

def bar<N, M>(field[N][M] input) -> field[M] {
return foo::<M>(input[0][0]);
}

def main(field[8] a) -> bool {
field[8] x = bar::<2, 8>([a, a]);
field[8] y = bar::<2, 8>([x, a]);
return true;
}
3 changes: 3 additions & 0 deletions examples/ZoKratesCurly/pf/3_plus.zok
Original file line number Diff line number Diff line change
@@ -0,0 +1,3 @@
def main(private u8 x) -> u8 {
return x + x + x;
}
5 changes: 5 additions & 0 deletions examples/ZoKratesCurly/pf/3_plus.zok.pin
Original file line number Diff line number Diff line change
@@ -0,0 +1,5 @@
(let (
(x #x04)
)
false
)
6 changes: 6 additions & 0 deletions examples/ZoKratesCurly/pf/3_plus.zok.vin
Original file line number Diff line number Diff line change
@@ -0,0 +1,6 @@
(let (
(return #x0c)
)
false
)

15 changes: 15 additions & 0 deletions examples/ZoKratesCurly/pf/arr_str_arr_str.zok
Original file line number Diff line number Diff line change
@@ -0,0 +1,15 @@
struct Pt {
field x;
field y;
}

struct Pts {
Pt[2] pts;
}

def main(private field y) -> field {
Pt p1 = Pt {x: 2, y: y};
Pt p2 = Pt {x: y, y: 2};
Pts[1] pts = [Pts { pts: [p1, p2] }];
return pts[0].pts[0].y * pts[0].pts[1].x;
}
Loading
Loading