1
0
Fork 0
mirror of synced 2025-09-23 12:18:44 +00:00

change syntax in core and stdlib tests

This commit is contained in:
dark64 2022-04-07 16:04:40 +02:00
parent 16f2b4c3ac
commit 2b9c1e8854
324 changed files with 3390 additions and 3228 deletions

View file

@ -1,2 +1,3 @@
def main(field a, field b) -> field: def main(field a, field b) -> field {
return 3*a+(b+a)**2 return 3*a+(b+a)**2;
}

View file

@ -0,0 +1,3 @@
def main(field a) -> field {
return a == 1 ? 1 : 0;
}

View file

@ -0,0 +1,3 @@
def main(field a) -> field {
return a == 1 ? 1 : 0;
}

View file

@ -1,2 +0,0 @@
def main(field a) -> field:
return if a == 1 then 1 else 0 fi

View file

@ -1,2 +0,0 @@
def main(field a) -> field:
return if a == 1 then 1 else 0 fi

View file

@ -1,3 +1,4 @@
def main(field[2][2] a) -> field[2][2]: def main(field[2][2] a) -> field[2][2] {
a[1][1] = 42 a[1][1] = 42;
return a return a;
}

View file

@ -1,14 +1,16 @@
import "utils/casts/u32_to_field" as to_field import "utils/casts/u32_to_field" as to_field;
// Binomial Coeffizient, n!/(k!*(n-k)!). // Binomial Coeffizient, n!/(k!*(n-k)!).
def fac(field x) -> field: def fac(field x) -> field {
field f = 1 field f = 1;
field counter = 0 field counter = 0;
for u32 i in 1..100 do for u32 i in 1..100 {
f = if counter == x then f else f * to_field(i) fi f = counter == x ? f : f * to_field(i);
counter = if counter == x then counter else counter + 1 fi counter = counter == x ? counter : counter + 1;
endfor }
return f return f;
}
def main(field n, field k) -> field: def main(field n, field k) -> field {
return fac(n)/(fac(k)*fac(n-k)) return fac(n)/(fac(k)*fac(n-k));
}

View file

@ -1,3 +1,4 @@
def main(field a, field b): def main(field a, field b) {
assert(a == b) assert(a == b);
return return;
}

View file

@ -1,2 +1,3 @@
def main(private field[3] a, private field b, private field[4] c) -> (field, field[3], field[4]): def main(private field[3] a, private field b, private field[4] c) -> (field, field[3], field[4]) {
return b, a, c return b, a, c;
}

View file

@ -1,3 +1,4 @@
// only using add, no need to flatten // only using add, no need to flatten
def main(field a, field b) -> field: def main(field a, field b) -> field {
return a + b return a + b:
}

View file

@ -1,2 +1,3 @@
def main(field a, field b, field c) -> field: def main(field a, field b, field c) -> field {
return a * b * c return a * b * c;
}

View file

@ -1,7 +1,9 @@
def wtax(field debt, field wealth) -> field: def wtax(field debt, field wealth) -> field {
field x = if wealth < debt then 0 else (wealth-debt) fi field x = wealth < debt ? 0 : (wealth - debt);
return x return x;
}
def main(field debt, field wealth) -> field: def main(field debt, field wealth) -> field {
field tax = wtax(debt,wealth) field tax = wtax(debt, wealth);
return tax return tax;
}

View file

@ -16,10 +16,11 @@ use zokrates_fs_resolver::FileSystemResolver;
#[test] #[test]
fn lt_field() { fn lt_field() {
let source = r#" let source = r#"
def main(private field a, private field b): def main(private field a, private field b) {
field x = if a < b then 3333 else 4444 fi field x = a < b ? 3333 : 4444;
assert(x == 3333) assert(x == 3333);
return return;
}
"# "#
.to_string(); .to_string();
@ -51,10 +52,11 @@ fn lt_field() {
#[test] #[test]
fn lt_uint() { fn lt_uint() {
let source = r#" let source = r#"
def main(private u32 a, private u32 b): def main(private u32 a, private u32 b) {
field x = if a < b then 3333 else 4444 fi field x = a < b ? 3333 : 4444;
assert(x == 3333) assert(x == 3333);
return return;
}
"# "#
.to_string(); .to_string();
@ -86,12 +88,13 @@ fn lt_uint() {
#[test] #[test]
fn unpack256() { fn unpack256() {
let source = r#" let source = r#"
import "utils/pack/bool/unpack256" import "utils/pack/bool/unpack256";
def main(private field a): def main(private field a) {
bool[256] bits = unpack256(a) bool[256] bits = unpack256(a);
assert(bits[255]) assert(bits[255]);
return return;
}
"# "#
.to_string(); .to_string();
@ -129,12 +132,13 @@ fn unpack256() {
#[test] #[test]
fn unpack256_unchecked() { fn unpack256_unchecked() {
let source = r#" let source = r#"
import "utils/pack/bool/nonStrictUnpack256" import "utils/pack/bool/nonStrictUnpack256";
def main(private field a): def main(private field a) {
bool[256] bits = nonStrictUnpack256(a) bool[256] bits = nonStrictUnpack256(a);
assert(bits[255]) assert(bits[255]);
return return;
}
"# "#
.to_string(); .to_string();

View file

@ -1,2 +1,3 @@
def main(field a, field b) -> field: def main(field a, field b) -> field {
return a + b return a + b;
}

View file

@ -1,5 +1,5 @@
{ {
"entry_point": "./tests/tests/array_if.zok", "entry_point": "./tests/tests/array_conditional.zok",
"curves": ["Bn128", "Bls12_381", "Bls12_377", "Bw6_761"], "curves": ["Bn128", "Bls12_381", "Bls12_377", "Bw6_761"],
"tests": [ "tests": [
{ {

View file

@ -0,0 +1,3 @@
def main(field[2] a, field[2] b, field condition) -> field[2] {
return condition == 1 ? a : b;
}

View file

@ -1,2 +0,0 @@
def main(field[2] a, field[2] b, field condition) -> field[2]:
return if condition == 1 then a else b fi

View file

@ -1,7 +1,6 @@
import "utils/pack/bool/nonStrictUnpack256.zok" as unpack256 import "utils/pack/bool/nonStrictUnpack256.zok" as unpack256;
def main(field[2] inputs) -> (bool[512]): def main(field[2] inputs) -> (bool[512]) {
bool[512] preimage512 = [...unpack256(inputs[0]), ...unpack256(inputs[1])];
bool[512] preimage512 = [...unpack256(inputs[0]), ...unpack256(inputs[1])] return preimage512;
}
return preimage512

View file

@ -1,2 +1,3 @@
def main(bool[3] a) -> (bool[3]): def main(bool[3] a) -> (bool[3]) {
return a return a;
}

View file

@ -1,2 +1,3 @@
def main(field[3] array, u32 index) -> field: def main(field[3] array, u32 index) -> field {
return array[index] return array[index];
}

View file

@ -1,3 +1,4 @@
def main(field[2] a): def main(field[2] a) {
assert(a == [1, 2]) assert(a == [1, 2]);
return return;
}

View file

@ -1,3 +1,4 @@
def main(field a): def main(field a) {
assert(a == 1) assert(a == 1);
return return;
}

View file

@ -1,2 +1,3 @@
def main(bool a, bool b) -> bool: def main(bool a, bool b) -> bool {
return a == b return a == b;
}

View file

@ -1,4 +1,5 @@
// `a < b` should be flattened a single time, even if 1000 elements are assigned conditionally // `a < b` should be flattened a single time, even if 1000 elements are assigned conditionally
def main(field a, field b) -> field[1000]: def main(field a, field b) -> field[1000] {
return if a < b then [0f; 1000] else [1; 1000] fi return a < b ? [0f; 1000] : [1; 1000];
}

View file

@ -1,9 +1,10 @@
from "field" import FIELD_MAX from "field" import FIELD_MAX;
// /!\ should be called with a = 0 // /!\ should be called with a = 0
// as `|a - FIELD_MAX| < 2**(N-2)` the comparison should succeed // as `|a - FIELD_MAX| < 2**(N-2)` the comparison should succeed
def main(field a) -> bool: def main(field a) -> bool {
field p = FIELD_MAX + a field p = FIELD_MAX + a;
// we added a = 0 to prevent the condition to be evaluated at compile time // we added a = 0 to prevent the condition to be evaluated at compile time
return a < p return a < p;
}

View file

@ -1,11 +1,13 @@
struct Foo { struct Foo {
bool[2] a bool[2] a;
field b field b;
} }
def f(bool a, field b, Foo c, field[2] d) -> (Foo, field): def f(bool a, field b, Foo c, field[2] d) -> (Foo, field) {
return Foo { a: [a, a], b: d[0] }, if c.a[0] then b + c.b else d[1] fi return Foo { a: [a, a], b: d[0] }, c.a[0] ? b + c.b : d[1];
}
def main(bool a, field b, Foo c, field[2] d) -> (Foo, field): def main(bool a, field b, Foo c, field[2] d) -> (Foo, field) {
Foo e, field f = f(a, b, c, d) Foo e, field f = f(a, b, c, d);
return e, f return e, f;
}

View file

@ -1,5 +1,6 @@
const u32 N = 2 const u32 N = 2;
const field[N] ARRAY = [1, 2] const field[N] ARRAY = [1, 2];
def main() -> field[N]: def main() -> field[N] {
return ARRAY return ARRAY;
}

View file

@ -1,5 +1,6 @@
const u32 SIZE = 2 const u32 SIZE = 2;
def main(field[SIZE] a) -> field[SIZE]: def main(field[SIZE] a) -> field[SIZE] {
field[SIZE] b = a field[SIZE] b = a;
return b return b;
}

View file

@ -1,4 +1,5 @@
const bool BOOLEAN = true const bool BOOLEAN = true;
def main() -> bool: def main() -> bool {
return BOOLEAN return BOOLEAN;
}

View file

@ -1,4 +1,5 @@
const field ONE = 1 const field ONE = 1;
def main() -> field: def main() -> field {
return ONE return ONE;
}

View file

@ -1,4 +1,6 @@
from "./origin.zok" import foo from "./origin.zok" import foo;
def main():
assert(foo([1, 1])) def main() {
return assert(foo([1, 1]));
return;
}

View file

@ -1,3 +1,5 @@
const u32 N = 1 + 1 const u32 N = 1 + 1;
def foo(field[N] a) -> bool:
return true def foo(field[N] a) -> bool {
return true;
}

View file

@ -1,5 +1,6 @@
from "./b" import SIZE_WORDS from "./b" import SIZE_WORDS;
def main(field[SIZE_WORDS] a): def main(field[SIZE_WORDS] a) {
assert(a == [0; SIZE_WORDS]) assert(a == [0; SIZE_WORDS]);
return return;
}

View file

@ -1,2 +1,2 @@
const u32 SIZE_BYTES = 136 const u32 SIZE_BYTES = 136;
const u32 SIZE_WORDS = SIZE_BYTES/8 const u32 SIZE_WORDS = SIZE_BYTES / 8;

View file

@ -1,2 +1,2 @@
const u32 SIZE_BYTES = 136 const u32 SIZE_BYTES = 136;
const u32 SIZE_WORDS = SIZE_BYTES/8 const u32 SIZE_WORDS = SIZE_BYTES / 8;

View file

@ -1,5 +1,6 @@
from "./a" import SIZE_WORDS from "./a" import SIZE_WORDS;
def main(field[SIZE_WORDS] a): def main(field[SIZE_WORDS] a) {
assert(a == [0; SIZE_WORDS]) assert(a == [0; SIZE_WORDS]);
return return;
}

View file

@ -1,4 +1,5 @@
from "./b" import B from "./b" import B;
def main(): def main() {
return return;
}

View file

@ -1,2 +1,2 @@
const field A = 1 const field A = 1;
const field B = A + 1 const field B = A + 1;

View file

@ -1,2 +1,2 @@
const field A = 1 const field A = 1;
const field B = A + 1 const field B = A + 1;

View file

@ -1,4 +1,5 @@
from "./a" import B from "./a" import B;
def main(): def main() {
return return;
}

View file

@ -1,15 +1,16 @@
const u32 N = 2 const u32 N = 2;
const bool B = true const bool B = true;
struct Foo { struct Foo {
field[N] a field[N] a;
bool b bool b;
} }
const Foo[N] F = [ const Foo[N] F = [
Foo { a: [1, 2], b: B }, Foo { a: [1, 2], b: B },
Foo { a: [3, 4], b: !B } Foo { a: [3, 4], b: !B }
] ];
def main() -> Foo[N]: def main() -> Foo[N] {
return F return F;
}

View file

@ -1,6 +1,7 @@
const field A = 2 const field A = 2;
const field B = 2 const field B = 2;
const field[2] ARRAY = [A * 2, B * 2] const field[2] ARRAY = [A * 2, B * 2];
def main() -> field: def main() -> field {
return ARRAY[0] + ARRAY[1] return ARRAY[0] + ARRAY[1];
}

View file

@ -1,5 +1,6 @@
const u32 TWO = 2 const u32 TWO = 2;
const u32 FOUR = TWO * TWO const u32 FOUR = TWO * TWO;
def main() -> field[FOUR]: def main() -> field[FOUR] {
return [42; FOUR] return [42; FOUR];
}

View file

@ -1,8 +1,8 @@
const u32 N = 2 const u32 N = 2;
struct State { struct State {
field[N] a field[N] a;
field[N][N] b field[N][N] b;
} }
const State STATE = State { const State STATE = State {
@ -10,5 +10,6 @@ const State STATE = State {
b: [[3, 4], [5, 6]] b: [[3, 4], [5, 6]]
} }
def main() -> State: def main() -> State {
return STATE return STATE;
}

View file

@ -1,4 +1,5 @@
const u32 ONE = 0x00000001 const u32 ONE = 0x00000001;
def main() -> u32: def main() -> u32 {
return ONE return ONE;
}

View file

@ -1,10 +1,11 @@
import "utils/casts/u32_to_field" as to_field import "utils/casts/u32_to_field" as to_field;
def main(field x) -> field: def main(field x) -> field {
field f = 1 field f = 1;
field counter = 0 field counter = 0;
for u32 i in 1..5 do for u32 i in 1..5 {
f = if counter == x then f else f * to_field(i) fi f = counter == x ? f : f * to_field(i);
counter = if counter == x then counter else counter + 1 fi counter = counter == x ? counter : counter + 1;
endfor }
return f return f;
}

View file

@ -1,7 +1,9 @@
def id<N>() -> u32: def id<N>() -> u32 {
return N return N;
}
def main(): def main() {
assert(id::<5>() == 5) assert(id::<5>() == 5);
assert(id::<6>() == 6) assert(id::<6>() == 6);
return return;
}

View file

@ -1,8 +1,11 @@
def foo<T>(field[T] b) -> field: def foo<T>(field[T] b) -> field {
return 1 return 1;
}
def bar<T>(field[T] b) -> field: def bar<T>(field[T] b) -> field {
return foo(b) return foo(b);
}
def main(field[3] a) -> field: def main(field[3] a) -> field {
return foo(a) + bar(a) return foo(a) + bar(a);
}

View file

@ -1,5 +1,6 @@
from "EMBED" import unpack from "EMBED" import unpack;
def main(field x): def main(field x) {
bool[1] bits = unpack(x) bool[1] bits = unpack(x);
return return;
}

View file

@ -1,6 +1,8 @@
def foo<T>(field[T] b) -> field[T]: def foo<T>(field[T] b) -> field[T] {
return b return b;
}
def main(field[3] a) -> field[3]: def main(field[3] a) -> field[3] {
field[3] res = foo(a) field[3] res = foo(a);
return res return res;
}

View file

@ -1,10 +1,13 @@
def foo<N>(field[N] x) -> field[N]: def foo<N>(field[N] x) -> field[N] {
return x return x;
}
def bar<N>(field[N] x) -> field[N]: def bar<N>(field[N] x) -> field[N] {
field[N] r = x field[N] r = x;
return r return r;
}
def main(field[3] x) -> field[2]: def main(field[3] x) -> field[2] {
field[2] z = foo(x)[0..2] field[2] z = foo(x)[0..2];
return bar(z) return bar(z);
}

View file

@ -1,2 +1,3 @@
def foo() -> field: def foo() -> field {
return 1 return 1;
}

View file

@ -1,4 +1,5 @@
from "./dep/foo" import foo as bar from "./dep/foo" import foo as bar;
def foo() -> field: def foo() -> field {
return 2 + bar() return 2 + bar();
}

View file

@ -1,4 +1,5 @@
from "./dep/foo" import foo from "./dep/foo" import foo;
def main() -> field: def main() -> field {
return foo() return foo();
}

View file

@ -1,2 +1,3 @@
def main(field e) -> bool: def main(field e) -> bool {
return e <= 42 return e <= 42;
}

View file

@ -1,5 +1,7 @@
def rotl32<N>(u32 x) -> u32: def rotl32<N>(u32 x) -> u32 {
return ((x << N) | (x >> (32 - N))) return ((x << N) | (x >> (32 - N)));
}
def main(u32 i) -> u32: def main(u32 i) -> u32 {
return rotl32::<2>(i) return rotl32::<2>(i);
}

View file

@ -1,9 +1,11 @@
import "utils/casts/u32_to_bits" as to_bits import "utils/casts/u32_to_bits" as to_bits;
import "utils/casts/u32_from_bits" as from_bits import "utils/casts/u32_from_bits" as from_bits;
def rotl32<N>(u32 e) -> u32: def rotl32<N>(u32 e) -> u32 {
bool[32] b = to_bits(e) bool[32] b = to_bits(e);
return from_bits([...b[N..], ...b[..N]]) return from_bits([...b[N..], ...b[..N]]);
}
def main(u32 i) -> u32: def main(u32 i) -> u32 {
return rotl32::<2>(i) return rotl32::<2>(i);
}

View file

@ -1,3 +1,4 @@
def dep(field a) -> field: // this costs 2 constraints per call def dep(field a) -> field { // this costs 2 constraints per call
field res = a ** 4 field res = a ** 4;
return res return res;
}

View file

@ -1,14 +1,16 @@
from "./dep.zok" import dep as dep from "./dep.zok" import dep as dep;
def local(field a) -> field: // this costs 3 constraints per call def local(field a) -> field { // this costs 3 constraints per call
field res = a ** 8 field res = a ** 8;
return res // currently expressions in the return statement don't get memoized return res; // currently expressions in the return statement don't get memoized
}
def main(field a): def main(field a) {
// calling a local function many times with the same arg should cost only once // calling a local function many times with the same arg should cost only once
assert(local(a) + local(a) + local(a) + local(a) + local(a) == 5 * (a ** 8)) assert(local(a) + local(a) + local(a) + local(a) + local(a) == 5 * (a ** 8));
// calling an imported function many times with the same arg should cost only once // calling an imported function many times with the same arg should cost only once
assert(dep(a) + dep(a) + dep(a) + dep(a) + dep(a) == 5 * (a ** 4)) assert(dep(a) + dep(a) + dep(a) + dep(a) + dep(a) == 5 * (a ** 4));
return return;
}

View file

@ -1,10 +1,12 @@
def foo(field[1] a) -> field: def foo(field[1] a) -> field {
return a[0] return a[0];
}
def main(): def main() {
field[1] a = [1] field[1] a = [1];
field b = foo(a) field b = foo(a);
a[0] = 0 a[0] = 0;
field c = foo(a) field c = foo(a);
assert(c == 0) assert(c == 0);
return return;
}

View file

@ -1,43 +1,45 @@
from "utils/pack/bool/unpack.zok" import main as unpack from "utils/pack/bool/unpack.zok" import main as unpack;
from "utils/casts/u32_to_bits" import main as u32_to_bits from "utils/casts/u32_to_bits" import main as u32_to_bits;
from "field" import FIELD_MAX, FIELD_SIZE_IN_BITS from "field" import FIELD_MAX, FIELD_SIZE_IN_BITS;
// this comparison works for any N smaller than the field size, which is the case in practice // this comparison works for any N smaller than the field size, which is the case in practice
def le<N>(bool[N] a_bits, bool[N] c_bits) -> bool: def le<N>(bool[N] a_bits, bool[N] c_bits) -> bool {
bool size_unknown = false;
u32 verified_conditions = 0; // `and(conditions) == (sum(conditions) == len(conditions))`, here we initialize `sum(conditions)`
bool size_unknown = false size_unknown = true;
u32 verified_conditions = 0 // `and(conditions) == (sum(conditions) == len(conditions))`, here we initialize `sum(conditions)` for u32 i in 0..N {
verified_conditions = verified_conditions + c_bits[i] || (!size_unknown || !a_bits[i]) ? 1 : 0;
size_unknown = c_bits[i] ? size_unknown && a_bits[i] : size_unknown; // this is actually not required in the last round
}
size_unknown = true return verified_conditions == N; // this checks that all conditions were verified
}
for u32 i in 0..N do
verified_conditions = verified_conditions + if c_bits[i] || (!size_unknown || !a_bits[i]) then 1 else 0 fi
size_unknown = if c_bits[i] then size_unknown && a_bits[i] else size_unknown fi // this is actually not required in the last round
endfor
return verified_conditions == N // this checks that all conditions were verified
// this instantiates comparison starting from field elements // this instantiates comparison starting from field elements
def le<N>(field a, field c) -> bool: def le<N>(field a, field c) -> bool {
bool[N] MAX_BITS = unpack::<N>(FIELD_MAX) bool[N] MAX_BITS = unpack::<N>(FIELD_MAX);
bool[N] a_bits = unpack(a) bool[N] a_bits = unpack(a);
assert(le(a_bits, MAX_BITS)) assert(le(a_bits, MAX_BITS));
bool[N] c_bits = unpack(c) bool[N] c_bits = unpack(c);
assert(le(c_bits, MAX_BITS)) assert(le(c_bits, MAX_BITS));
return le(a_bits, c_bits) return le(a_bits, c_bits);
}
// this instanciates comparison starting from u32 // this instanciates comparison starting from u32
def le(u32 a, u32 c) -> bool: def le(u32 a, u32 c) -> bool {
bool[32] a_bits = u32_to_bits(a) bool[32] a_bits = u32_to_bits(a);
bool[32] c_bits = u32_to_bits(c) bool[32] c_bits = u32_to_bits(c);
return le(a_bits, c_bits) return le(a_bits, c_bits);
}
def main(field a, u32 b) -> (bool, bool): def main(field a, u32 b) -> (bool, bool) {
field c = 42 field c = 42;
u32 d = 42 u32 d = 42;
return le::<FIELD_SIZE_IN_BITS>(a, c), le(b, d) return le::<FIELD_SIZE_IN_BITS>(a, c), le(b, d);
}

View file

@ -1,15 +1,16 @@
def main(field x, field y, u8 z, u8 t) -> (field[4], u8[4]): def main(field x, field y, u8 z, u8 t) -> (field[4], u8[4]) {
field a = -y // should parse to neg field a = -y; // should parse to neg
field b = x - y // should parse to sub field b = x - y; // should parse to sub
field c = x + - y // should parse to add(neg) field c = x + - y; // should parse to add(neg)
field d = x - + y // should parse to sub(pos) field d = x - + y; // should parse to sub(pos)
u8 e = -t // should parse to neg u8 e = -t; // should parse to neg
u8 f = z - t // should parse to sub u8 f = z - t; // should parse to sub
u8 g = z + - t // should parse to add(neg) u8 g = z + - t; // should parse to add(neg)
u8 h = z - + t // should parse to sub(pos) u8 h = z - + t; // should parse to sub(pos)
assert(-0x00 == 0x00) assert(-0x00 == 0x00);
assert(-0f == 0) assert(-0f == 0);
return [a, b, c, d], [e, f, g, h] return [a, b, c, d], [e, f, g, h];
}

View file

@ -1,27 +1,28 @@
def main(field[4] values) -> (field, field, field): def main(field[4] values) -> (field, field, field) {
field res0 = 1 field res0 = 1;
field res1 = 0 field res1 = 0;
u32 counter = 0 u32 counter = 0;
for u32 i in 0..4 do for u32 i in 0..4 {
for u32 j in i..4 do for u32 j in i..4 {
counter = counter + 1 counter = counter + 1;
res0 = res0 * (values[i] + values[j]) res0 = res0 * (values[i] + values[j]);
endfor }
endfor }
for u32 i in 0..counter do for u32 i in 0..counter {
res1 = res1 + 1 res1 = res1 + 1;
endfor }
field res2 = 0 field res2 = 0;
u32 i = 0 u32 i = 0;
for u32 i in i..5 do for u32 i in i..5 {
i = 5 i = 5;
for u32 i in 0..i do for u32 i in 0..i {
res2 = res2 + 1 res2 = res2 + 1;
endfor }
endfor }
return res0, res1, res2 return res0, res1, res2;
}

View file

@ -1,10 +1,11 @@
def throwing_bound<N>(u32 x) -> u32: def throwing_bound<N>(u32 x) -> u32 {
assert(x == N) assert(x == N);
return 1 return 1;
}
// this compiles: the conditional, even though it can throw, has a constant compile-time value of `1` // this compiles: the conditional, even though it can throw, has a constant compile-time value of `1`
// However, the assertions are still checked at runtime, which leads to panics without branch isolation. // However, the assertions are still checked at runtime, which leads to panics without branch isolation.
def main(u32 x): def main(u32 x) {
for u32 i in 0..if x == 0 then throwing_bound::<0>(x) else throwing_bound::<1>(x) fi do for u32 i in 0..x == 0 ? throwing_bound::<0>(x) : throwing_bound::<1>(x) {}
endfor return;
return }

View file

@ -1,34 +1,16 @@
def check<N>(bool[N] conditions, bool[N] expected) -> bool[3]: def check<N>(bool[N] conditions, bool[N] expected) -> bool[3] {
assert(conditions == expected) assert(conditions == expected);
return conditions return conditions;
}
def main(bool[3] conditions) -> bool[3]: def main(bool[3] conditions) -> bool[3] {
return if conditions[0] then\ return conditions[0] ? \
if conditions[1] then\ conditions[1] ? \
if conditions[2] then\ conditions[2] ? check(conditions, [true, true, true]) : check(conditions, [true, true, false]) : \
check(conditions, [true, true, true])\ conditions[2] ? check(conditions, [true, false, true]) : \
else\ check(conditions, [true, false, false]) : \
check(conditions, [true, true, false])\ conditions[1] ? \
fi\ conditions[2] ? check(conditions, [false, true, true]) : check(conditions, [false, true, false]) : \
else\ conditions[2] ? check(conditions, [false, false, true]) : \
if conditions[2] then\ check(conditions, [false, false, false]);
check(conditions, [true, false, true])\ }
else\
check(conditions, [true, false, false])\
fi\
fi\
else\
if conditions[1] then\
if conditions[2] then\
check(conditions, [false, true, true])\
else\
check(conditions, [false, true, false])\
fi\
else\
if conditions[2] then\
check(conditions, [false, false, true])\
else\
check(conditions, [false, false, false])\
fi\
fi\
fi

View file

@ -1,2 +1,3 @@
def main(field x) -> field: def main(field x) -> field {
return if x == 0 then 0 else 1/x fi return x == 0 ? 0 : 1/x;
}

View file

@ -1,9 +1,10 @@
def throwing_bound<N>(u32 x) -> u32: def throwing_bound<N>(u32 x) -> u32 {
assert(x == N) assert(x == N);
return 1 return 1;
}
// Even if the bound is constant at compile time, it can throw at runtime // Even if the bound is constant at compile time, it can throw at runtime
def main(u32 x): def main(u32 x) {
for u32 i in 0..throwing_bound::<1>(x) do for u32 i in 0..throwing_bound::<1>(x) {}
endfor return;
return }

View file

@ -1,31 +1,38 @@
def zero(field x) -> field: def zero(field x) -> field {
assert(x == 0) assert(x == 0);
return 0 return 0;
}
def inverse(field x) -> field: def inverse(field x) -> field {
assert(x != 0) assert(x != 0);
return 1/x return 1/x;
}
def yes(bool x) -> bool: def yes(bool x) -> bool {
assert(x) assert(x);
return x return x;
}
def no(bool x) -> bool: def no(bool x) -> bool {
assert(!x) assert(!x);
return x return x;
}
def ones(field[2] a) -> field[2]: def ones(field[2] a) -> field[2] {
assert(a == [1, 1]) assert(a == [1, 1]);
return a return a;
}
def twos(field[2] a) -> field[2]: def twos(field[2] a) -> field[2] {
assert(a == [2, 2]) assert(a == [2, 2]);
return a return a;
}
def main(bool condition, field[2] a, field x) -> (bool, field[2], field): def main(bool condition, field[2] a, field x) -> (bool, field[2], field) {
// first branch asserts that `condition` is true, second branch asserts that `condition` is false. This should never throw. // first branch asserts that `condition` is true, second branch asserts that `condition` is false. This should never throw.
// first branch asserts that all elements in `a` are 1, 2 in the second branch. This should throw only if `a` is neither ones or zeroes // first branch asserts that all elements in `a` are 1, 2 in the second branch. This should throw only if `a` is neither ones or zeroes
// first branch asserts that `x` is zero and returns it, second branch asserts that `x` isn't 0 and returns its inverse (which internally generates a failing assert if x is 0). This should never throw // first branch asserts that `x` is zero and returns it, second branch asserts that `x` isn't 0 and returns its inverse (which internally generates a failing assert if x is 0). This should never throw
return if condition then yes(condition) else no(condition) fi,\ return condition ? yes(condition) : no(condition), \
if condition then ones(a) else twos(a) fi,\ condition ? ones(a) : twos(a), \
if x == 0 then zero(x) else inverse(x) fi x == 0 ? zero(x) : inverse(x);
}

View file

@ -1,18 +1,22 @@
struct Foo { struct Foo {
field a field a;
} }
def mutate(field a) -> field: def mutate(field a) -> field {
a = a + 1 a = a + 1;
return a return a;
}
def mutate(Foo f) -> Foo: def mutate(Foo f) -> Foo {
f.a = f.a + 1 f.a = f.a + 1;
return f return f;
}
def mutate(field[1] f) -> field[1]: def mutate(field[1] f) -> field[1] {
f[0] = f[0] + 1 f[0] = f[0] + 1;
return f return f;
}
def main(field[1] f, Foo g, field h) -> (field[1], field[1], Foo, Foo, field, field): def main(field[1] f, Foo g, field h) -> (field[1], field[1], Foo, Foo, field, field) {
return mutate(f), f, mutate(g), g, mutate(h), h return mutate(f), f, mutate(g), g, mutate(h), h;
}

View file

@ -1,21 +1,22 @@
def main(): def main() {
assert(9 == 1 + 2 * 2 ** 2) // Checks precedence of arithmetic operators (expecting transitive behaviour) assert(9 == 1 + 2 * 2 ** 2); // checks precedence of arithmetic operators (expecting transitive behaviour)
assert(9 == 2 ** 2 * 2 + 1) assert(9 == 2 ** 2 * 2 + 1);
assert(7 == 2 ** 2 * 2 - 1) assert(7 == 2 ** 2 * 2 - 1);
assert(3 == 2 ** 2 / 2 + 1) assert(3 == 2 ** 2 / 2 + 1);
field a = if 3f == 2f ** 2 / 2 + 1 && true then 1 else 0 fi // combines arithmetic with boolean operators field a = 3f == 2f ** 2 / 2 + 1 && true ? 1 : 0; // combines arithmetic with boolean operators
field b = if 3f == 3f && 4f < 5f then 1 else 0 fi // checks precedence of boolean operators field b = 3f == 3f && 4f < 5f ? 1 : 0; // checks precedence of boolean operators
field c = if 4f < 5f && 3f == 3f then 1 else 0 fi field c = 4f < 5f && 3f == 3f ? 1 : 0;
field d = if 4f > 5f && 2f >= 1f || 1f == 1f then 1 else 0 fi field d = 4f > 5f && 2f >= 1f || 1f == 1f ? 1 : 0;
field e = if 2f >= 1f && 4f > 5f || 1f == 1f then 1 else 0 fi field e = 2f >= 1f && 4f > 5f || 1f == 1f ? 1 : 0;
field f = if 1f < 2f && false || 4f < 5f && 2f >= 1f then 1 else 0 fi field f = 1f < 2f && false || 4f < 5f && 2f >= 1f ? 1 : 0;
assert(0x00 ^ 0x00 == 0x00) assert(0x00 ^ 0x00 == 0x00);
assert(0 - 2 ** 2 == -4) assert(0 - 2 ** 2 == -4);
assert(-2**2 == -4) assert(-2**2 == -4);
//check if all statements have evalutated to true //check if all statements have evaluated to true
assert(a * b * c * d * e * f == 1) assert(a * b * c * d * e * f == 1);
return return;
}

View file

@ -1,2 +1,3 @@
def main(field x) -> bool[5]: def main(field x) -> bool[5] {
return [x < 0, x < 1, x < 255, x < 0 - 1, x - 2 > 0 - 2] return [x < 0, x < 1, x < 255, x < 0 - 1, x - 2 > 0 - 2];
}

View file

@ -1,3 +1,4 @@
def main(field x): def main(field x) {
assert(x >= 2) assert(x >= 2);
return return;
}

View file

@ -1,3 +1,4 @@
def main(field x): def main(field x) {
assert(x > 2) assert(x > 2);
return return;
}

View file

@ -1,5 +1,6 @@
from "field" import FIELD_MAX from "field" import FIELD_MAX;
def main(field x): def main(field x) {
assert(x > FIELD_MAX - 1) assert(x > FIELD_MAX - 1);
return return;
}

View file

@ -1,3 +1,4 @@
def main(field x): def main(field x) {
assert(x <= 2) assert(x <= 2);
return return;
}

View file

@ -1,3 +1,4 @@
def main(field x): def main(field x) {
assert(x < 2) assert(x < 2);
return return;
}

View file

@ -1,5 +1,6 @@
from "field" import FIELD_MAX from "field" import FIELD_MAX;
def main(field x): def main(field x) {
assert(x < FIELD_MAX - 1) assert(x < FIELD_MAX - 1);
return return;
}

View file

@ -1,5 +1,7 @@
def rotr32<N>(u32 x) -> u32: def rotr32<N>(u32 x) -> u32 {
return (x >> N) | (x << (32 - N)) return (x >> N) | (x << (32 - N));
}
def main(u32 i) -> u32: def main(u32 i) -> u32 {
return rotr32::<2>(i) return rotr32::<2>(i);
}

View file

@ -1,9 +1,11 @@
import "utils/casts/u32_to_bits" as to_bits import "utils/casts/u32_to_bits" as to_bits;
import "utils/casts/u32_from_bits" as from_bits import "utils/casts/u32_from_bits" as from_bits;
def rotr32<N>(u32 e) -> u32: def rotr32<N>(u32 e) -> u32 {
bool[32] b = to_bits(e) bool[32] b = to_bits(e);
return from_bits([...b[32-N..], ...b[..32-N]]) return from_bits([...b[32-N..], ...b[..32-N]]);
}
def main(u32 i) -> u32: def main(u32 i) -> u32 {
return rotr32::<2>(i) return rotr32::<2>(i);
}

View file

@ -1,6 +1,8 @@
def foo() -> field: def foo() -> field {
return 42 return 42;
}
def main(): def main() {
field a = foo() field a = foo();
return return;
}

View file

@ -3,8 +3,9 @@ from "EMBED" import snark_verify_bls12_377
// Verifies a proof with 1 public input (0 inputs + 1 output) // Verifies a proof with 1 public input (0 inputs + 1 output)
// Circuit used in this test: // Circuit used in this test:
// //
// def main() -> field: // def main() -> field {
// return 1 // return 1;
// }
// //
// Save the circuit as "circuit.zok" and run the following commands (in order): // Save the circuit as "circuit.zok" and run the following commands (in order):
// $ zokrates compile -i ./circuit.zok -c bls12_377 // $ zokrates compile -i ./circuit.zok -c bls12_377
@ -30,6 +31,7 @@ from "EMBED" import snark_verify_bls12_377
// Save this script as "flatten.js" and run the following command: // Save this script as "flatten.js" and run the following command:
// $ node flatten.js proof.json verification.key // $ node flatten.js proof.json verification.key
def main(private field[8] proof, private field[1] inputs, private field[20] vk) -> bool: def main(private field[8] proof, private field[1] inputs, private field[20] vk) -> bool {
bool result = snark_verify_bls12_377(inputs, proof, vk) bool result = snark_verify_bls12_377(inputs, proof, vk);
return result return result;
}

View file

@ -3,8 +3,9 @@ from "EMBED" import snark_verify_bls12_377
// Verifies a proof with 2 public inputs (1 input + 1 output) // Verifies a proof with 2 public inputs (1 input + 1 output)
// Circuit used in this test: // Circuit used in this test:
// //
// def main(field a) -> field: // def main(field a) -> field {
// return a * a // return a * a;
// }
// //
// Save the circuit as "circuit.zok" and run the following commands (in order): // Save the circuit as "circuit.zok" and run the following commands (in order):
// $ zokrates compile -i ./circuit.zok -c bls12_377 // $ zokrates compile -i ./circuit.zok -c bls12_377
@ -30,6 +31,7 @@ from "EMBED" import snark_verify_bls12_377
// Save this script as "flatten.js" and run the following command: // Save this script as "flatten.js" and run the following command:
// $ node flatten.js proof.json verification.key // $ node flatten.js proof.json verification.key
def main(private field[8] proof, private field[2] inputs, private field[22] vk) -> bool: def main(private field[8] proof, private field[2] inputs, private field[22] vk) -> bool {
bool result = snark_verify_bls12_377(inputs, proof, vk) bool result = snark_verify_bls12_377(inputs, proof, vk);
return result return result;
}

View file

@ -3,12 +3,13 @@ from "EMBED" import snark_verify_bls12_377
// Verifies a proof with 5 public inputs (4 inputs + 1 output) // Verifies a proof with 5 public inputs (4 inputs + 1 output)
// Circuit used in this test: // Circuit used in this test:
// //
// def main(field[4] a) -> field: // def main(field[4] a) -> field {
// field out = 0 // field out = 0;
// for u32 i in 0..4 do // for u32 i in 0..4 {
// out = out + a[i] // out = out + a[i];
// endfor // }
// return out // return out;
// }
// //
// Save the circuit as "circuit.zok" and run the following commands (in order): // Save the circuit as "circuit.zok" and run the following commands (in order):
// $ zokrates compile -i ./circuit.zok -c bls12_377 // $ zokrates compile -i ./circuit.zok -c bls12_377
@ -34,6 +35,7 @@ from "EMBED" import snark_verify_bls12_377
// Save this script as "flatten.js" and run the following command: // Save this script as "flatten.js" and run the following command:
// $ node flatten.js proof.json verification.key // $ node flatten.js proof.json verification.key
def main(private field[8] proof, private field[5] inputs, private field[28] vk) -> bool: def main(private field[8] proof, private field[5] inputs, private field[28] vk) -> bool {
bool result = snark_verify_bls12_377(inputs, proof, vk) bool result = snark_verify_bls12_377(inputs, proof, vk);
return result return result;
}

View file

@ -1,6 +1,7 @@
from "EMBED" import unpack from "EMBED" import unpack;
from "field" import FIELD_SIZE_IN_BITS from "field" import FIELD_SIZE_IN_BITS;
def main(field a) -> bool[FIELD_SIZE_IN_BITS]: def main(field a) -> bool[FIELD_SIZE_IN_BITS] {
bool[FIELD_SIZE_IN_BITS] b = unpack(a) bool[FIELD_SIZE_IN_BITS] b = unpack(a);
return b return b;
}

View file

@ -1,2 +1,3 @@
def main(field[3] a, field[3] b, field c) -> (field[9]): def main(field[3] a, field[3] b, field c) -> (field[9]) {
return [...a[..2], ...b[1..], ...a[..], ...b[1..2], c] return [...a[..2], ...b[1..], ...a[..], ...b[1..2], c];
}

View file

@ -1,8 +1,9 @@
struct State { struct State {
u32[16] memory u32[16] memory;
} }
def main(): def main() {
State s = State { memory: [0; 16] } State s = State { memory: [0; 16] };
s.memory[0] = 0x00000001 s.memory[0] = 0x00000001;
return return;
}

View file

@ -1,7 +1,8 @@
struct A { struct A {
field a field a;
bool b bool b;
} }
def main(A a) -> (A): def main(A a) -> (A) {
return a return a;
}

View file

@ -1,9 +1,10 @@
struct Foo { struct Foo {
field b field b;
bool a bool a;
} }
// this tests the abi, checking that the fields of a `Foo` instance get encoded in the right order // this tests the abi, checking that the fields of a `Foo` instance get encoded in the right order
// if the the encoder reverses `a` and `b`, the boolean check ends up being done on the field value, which would fail // if the the encoder reverses `a` and `b`, the boolean check ends up being done on the field value, which would fail
def main(Foo f): def main(Foo f) {
return return;
}

View file

@ -1,5 +1,4 @@
def main(bool a, bool b) -> field: def main(bool a, bool b) -> field {
field x = a ? 1 : b ? 2 : 3 // (a ? 1 : (b ? 2 : 3)) field x = a ? 1 : b ? 2 : 3; // (a ? 1 : (b ? 2 : 3))
field y = if a then 1 else if b then 2 else 3 fi fi return x;
assert(x == y) }
return x

View file

@ -1,4 +1,5 @@
def main(): def main() {
(u32[16],) s = ([0; 16],) (u32[16],) s = ([0; 16],);
s.0[0] = 0x00000001 s.0[0] = 0x00000001;
return return;
}

View file

@ -1,4 +1,5 @@
// this tests the abi, checking that the fields of a (field, bool) instance get encoded in the right order // this tests the abi, checking that the fields of a (field, bool) instance get encoded in the right order
// if the the encoder reverses `0` and `1`, the boolean check ends up being done on the field value, which would fail // if the the encoder reverses `0` and `1`, the boolean check ends up being done on the field value, which would fail
def main((field, bool) f): def main((field, bool) f) {
return return;
}

View file

@ -1,4 +1,5 @@
def main(() a) -> (()): def main(() a) -> (()) {
() b = () () b = ();
assert(a == b) assert(a == b);
return a return a;
}

View file

@ -1,2 +1,3 @@
def main((field, bool,) a) -> ((field, bool,)): def main((field, bool,) a) -> ((field, bool,)) {
return a return a;
}

View file

@ -1,7 +1,8 @@
// 32 constraints for input constraining // 32 constraints for input constraining
def main(u32 a) -> u32: def main(u32 a) -> u32 {
u32 res = 0x00000000 u32 res = 0x00000000;
for u32 i in 0..10 do for u32 i in 0..10 {
res = res + a res = res + a;
endfor }
return res // 42 constraints (decomposing on 42 bits) return res; // 42 constraints (decomposing on 42 bits)
}

Some files were not shown because too many files have changed in this diff Show more