Merge branch 'master' into c_frontend

scripts/dependencies_arch.sh

@@ -1,2 +1,2 @@
 set -xe
-pacman -S cvc4 coinor-cbc
+pacman -S cvc4 coin-or-cbc

scripts/dependencies_macos_homebrew.sh

@@ -0,0 +1,9 @@
+set -xe
+
+# breaks on M1 processors for now
+# https://github.com/coin-or-tools/homebrew-coinor/issues/62
+brew tap coin-or-tools/coinor
+brew install coin-or-tools/coinor/cbc
+
+brew tap cvc4/cvc4
+brew install cvc4/cvc4/cvc4

scripts/zokrates_test.zsh

@@ -56,3 +56,5 @@ pf_test str_arr_str
 pf_test arr_str_arr_str
 pf_test var_idx_arr_str_arr_str
 pf_test mm
+
+scripts/zx_tests/run_tests.sh

scripts/zx_tests/array_eq.zx

@@ -0,0 +1,4 @@
+def main() -> bool:
+    bool a = [4u32; 4u32] == [5u32; 4u32]
+    bool b = [4u32; 4u32] != [5u32; 4u32]
+    return a || b

scripts/zx_tests/array_eq.zxf

@@ -0,0 +1,4 @@
+def main() -> bool:
+    bool a = [4u32; 4u32] == [5u32; 5u32]
+    bool b = [4u32; 4u32] != [5u32; 4u32]
+    return a || b

scripts/zx_tests/array_eq_2.zxf

@@ -0,0 +1,4 @@
+def main() -> bool:
+    bool a = [4u32; 4u32] == [5u32; 4u32]
+    bool b = [4u32; 4u32] != [5u32; 5u32]
+    return a || b

scripts/zx_tests/array_oob_read.zxf

@@ -0,0 +1,3 @@
+def main() -> u32:
+    u32[3] a = [1, 2, 3]
+    return a[3]

scripts/zx_tests/array_oob_write.zxf

@@ -0,0 +1,4 @@
+def main() -> u32:
+    u32[3] a = [1, 2, 3]
+    a[3] = 4
+    return a[0]

scripts/zx_tests/array_read_write.zx

@@ -0,0 +1,5 @@
+def main() -> u32:
+    u32[4] a = [1, 2, 3, 4]
+    a[2] = 5
+    assert(a[2] == 5)
+    return a[2]

scripts/zx_tests/bit_order.zx

@@ -0,0 +1,103 @@
+import "utils/casts/u8_to_bits"
+import "utils/casts/u8_from_bits"
+import "utils/casts/u8_to_field"
+import "utils/casts/field_to_u8"
+
+import "utils/casts/u16_to_bits"
+import "utils/casts/u16_from_bits"
+import "utils/casts/u16_to_field"
+import "utils/casts/field_to_u16"
+
+import "utils/casts/u32_to_bits"
+import "utils/casts/u32_from_bits"
+import "utils/casts/u32_to_field"
+import "utils/casts/field_to_u32"
+
+import "utils/casts/u64_to_bits"
+import "utils/casts/u64_from_bits"
+import "utils/casts/u64_to_field"
+import "utils/casts/field_to_u64"
+
+import "utils/pack/bool/unpack"
+import "utils/pack/bool/pack"
+
+def main() -> bool:
+    // check for msb0 bit order
+    u8 i1 = 128
+    bool[8] o1 = u8_to_bits(i1)
+    assert(o1[0])
+    assert(!o1[7])
+
+    u16 i2 = 32768
+    bool[16] o2 = u16_to_bits(i2)
+    assert(o2[0])
+    assert(!o2[15])
+
+    u32 i3 = 2147483648
+    bool[32] o3 = u32_to_bits(i3)
+    assert(o3[0])
+    assert(!o3[31])
+
+    u64 i4 = 9223372036854775808
+    bool[64] o4 = u64_to_bits(i4)
+    assert(o4[0])
+    assert(!o4[63])
+
+    // u8 -> field -> bits -> u8
+    u8 t1_0 = 42
+    field t1_1 = u8_to_field(t1_0)
+    bool[8] t1_2 = unpack(t1_1)
+    u8 t1_3 = u8_from_bits(t1_2)
+    assert(t1_0 == t1_3)
+
+    // XXX(TODO) pack builtin
+    // u8 -> bits -> field -> u8
+    u8 t2_0 = 77
+    bool[8] t2_1 = u8_to_bits(t2_0)
+    field t2_2 = pack(t2_1)
+    u8 t2_3 = field_to_u8(t2_2)
+    assert(t2_0 == t2_3)
+
+    // u16 -> field -> bits -> u16
+    u16 t3_0 = 46971
+    field t3_1 = u16_to_field(t3_0)
+    bool[16] t3_2 = unpack(t3_1)
+    u16 t3_3 = u16_from_bits(t3_2)
+    assert(t3_0 == t3_3)
+
+    // u16 -> bits -> field -> u16
+    u16 t4_0 = 63336
+    bool[16] t4_1 = u16_to_bits(t4_0)
+    field t4_2 = pack(t4_1)
+    u16 t4_3 = field_to_u16(t4_2)
+    assert(t4_0 == t4_3)
+
+    // u32 -> field -> bits -> u32
+    u32 t5_0 = 2652390681
+    field t5_1 = u32_to_field(t5_0)
+    bool[32] t5_2 = unpack(t5_1)
+    u32 t5_3 = u32_from_bits(t5_2)
+    assert(t5_0 == t5_3)
+
+    // u32 -> bits -> field -> u32
+    u32 t6_0 = 1173684415
+    bool[32] t6_1 = u32_to_bits(t6_0)
+    field t6_2 = pack(t6_1)
+    u32 t6_3 = field_to_u32(t6_2)
+    assert(t6_0 == t6_3)
+
+    // u64 -> field -> bits -> u64
+    u64 t7_0 = 18312416462297086083
+    field t7_1 = u64_to_field(t7_0)
+    bool[64] t7_2 = unpack(t7_1)
+    u64 t7_3 = u64_from_bits(t7_2)
+    assert(t7_0 == t7_3)
+
+    // u64 -> bits -> field -> u64
+    u64 t8_0 = 4047977501435466453
+    bool[64] t8_1 = u64_to_bits(t8_0)
+    field t8_2 = pack(t8_1)
+    u64 t8_3 = field_to_u64(t8_2)
+    assert(t8_0 == t8_3)
+
+    return true

scripts/zx_tests/bool_to_bv.zx

@@ -0,0 +1,52 @@
+import "utils/casts/bool_array_to_u32_array"
+
+def main() -> u32:
+    bool[2] ones = [true, true]
+    bool[6] zeros = [false, false, false, false, false, false]
+
+    bool[8] byte0 = [...ones, ...zeros]     // 0xc0
+    bool[8] byte1 = [...zeros, ...ones]     // 0x03
+
+    bool[16] word0 = [...byte0, ...byte0]   // 0xc0c0
+    bool[16] word1 = [...byte0, ...byte1]   // 0xc003
+    bool[16] word2 = [...byte1, ...byte0]   // 0x03c0
+    bool[16] word3 = [...byte1, ...byte1]   // 0x0303
+
+    bool[32] dwrd0 = [...word0, ...word0]
+    bool[32] dwrd1 = [...word0, ...word1]
+    bool[32] dwrd2 = [...word0, ...word2]
+    bool[32] dwrd3 = [...word0, ...word3]
+    bool[32] dwrd4 = [...word1, ...word0]
+    bool[32] dwrd5 = [...word1, ...word1]
+    bool[32] dwrd6 = [...word1, ...word2]
+    bool[32] dwrd7 = [...word1, ...word3]
+    bool[32] dwrd8 = [...word2, ...word0]
+    bool[32] dwrd9 = [...word2, ...word1]
+    bool[32] dwrdA = [...word2, ...word2]
+    bool[32] dwrdB = [...word2, ...word3]
+    bool[32] dwrdC = [...word3, ...word0]
+    bool[32] dwrdD = [...word3, ...word1]
+    bool[32] dwrdE = [...word3, ...word2]
+    bool[32] dwrdF = [...word3, ...word3]
+
+    bool[16 * 32] foo = [...dwrd0, ...dwrd1, ...dwrd2, ...dwrd3, ...dwrd4, ...dwrd5, ...dwrd6, ...dwrd7, ...dwrd8, ...dwrd9, ...dwrdA, ...dwrdB, ...dwrdC, ...dwrdD, ...dwrdE, ...dwrdF ]
+    u32[16] a = bool_array_to_u32_array(foo)
+
+    assert(a[0] == 0xc0c0c0c0)
+    assert(a[1] == 0xc0c0c003)
+    assert(a[2] == 0xc0c003c0)
+    assert(a[3] == 0xc0c00303)
+    assert(a[4] == 0xc003c0c0)
+    assert(a[5] == 0xc003c003)
+    assert(a[6] == 0xc00303c0)
+    assert(a[7] == 0xc0030303)
+    assert(a[8] == 0x03c0c0c0)
+    assert(a[9] == 0x03c0c003)
+    assert(a[10] == 0x03c003c0)
+    assert(a[11] == 0x03c00303)
+    assert(a[12] == 0x0303c0c0)
+    assert(a[13] == 0x0303c003)
+    assert(a[14] == 0x030303c0)
+    assert(a[15] == 0x03030303)
+
+    return a[0]

scripts/zx_tests/double_generic.zx

@@ -0,0 +1,10 @@
+const u32[5] asdf = [1,2,3,4,5]
+
+def last<N>(u32[N] a) -> u32:
+    return a[N-1]
+
+def foo<N>(u32[N] a) -> u32:
+    return last([...a, ...a])
+
+def main() -> u32:
+    return foo([1,2,3])

scripts/zx_tests/double_generic_const.zx

@@ -0,0 +1,10 @@
+const u32[5] asdf = [1,2,3,4,5]
+
+def last<N>(u32[N] a) -> u32:
+    return a[N-1]
+
+def foo<N>(u32[N] a) -> u32:
+    return last([...a, ...a])
+
+def main() -> u32:
+    return foo(asdf)

scripts/zx_tests/field_cmp.zx

@@ -0,0 +1,18 @@
+def main() -> bool:
+    field a = 0
+    field b = -1
+    field c = 2
+    field d = 2
+    assert(b > a)
+    assert(b >= a)
+    assert(a < b)
+    assert(a <= b)
+    assert(c > a)
+    assert(c >= a)
+    assert(c < b)
+    assert(c <= b)
+    assert(d >= c)
+    assert(c <= d)
+    assert(c != b)
+    assert(c == d)
+    return true

scripts/zx_tests/field_mod.zx

@@ -0,0 +1,5 @@
+def main() -> bool:
+    field a = 12824923210
+    field b = 18423229
+    assert(a % b == 2355826)
+    return false

scripts/zx_tests/field_size.zx

@@ -0,0 +1,4 @@
+from "EMBED" import FIELD_SIZE_IN_BITS
+
+def main() -> u32:
+    return FIELD_SIZE_IN_BITS

scripts/zx_tests/inconsistent_array.zxf

@@ -0,0 +1,3 @@
+def main() -> u32:
+    u32[3][2] foo = [[1,2], [3,4], [5,6,7]]
+    return foo[0][0]

scripts/zx_tests/inline_array_const.zx

@@ -0,0 +1,6 @@
+const u32[3] A = [1, 2, 3]
+const u32[2][3] B = [A, A]
+const u32[1][2][3] C = [B]
+
+def main() -> u32[1][2][3]:
+    return C

scripts/zx_tests/inline_array_const_access.zx

@@ -0,0 +1,9 @@
+const u32[3] A = [1, 2, 3]
+const u32[2][3] B = [A, A]
+const u32[1][2][3] C = [B]
+
+def get_C() -> u32[1][2][3]:
+    return C
+
+def main() -> u32[3]:
+    return get_C()[0][1]

scripts/zx_tests/inline_array_const_access.zxf

@@ -0,0 +1,9 @@
+const u32[3] A = [1, 2, 3]
+const u32[2][3] B = [A, A]
+const u32[1][2][3] C = [B]
+
+def get_C() -> u32[1][2][3]:
+    return C
+
+def main() -> u32[3]:
+    return get_C()[1][1]

scripts/zx_tests/inline_expression_len.zx

@@ -0,0 +1,5 @@
+const u32[5] asdf = [1,2,3,4,5]
+
+def main() -> u32[4]:
+    u32[5] qwer = [1,2,3,4,5]
+    return [...asdf[1..3], 4, qwer[2]]

scripts/zx_tests/inline_expression_len.zxf

@@ -0,0 +1,5 @@
+const u32[5] asdf = [1,2,3,4,5]
+
+def main() -> u32[5]:
+    u32[5] qwer = [1,2,3,4,5]
+    return [...asdf[1..3], 4, qwer[2]]

scripts/zx_tests/inline_struct_generic.zx

@@ -0,0 +1,8 @@
+struct InlineTest<N> {
+    u32[N] x
+    field y
+}
+
+def main() -> InlineTest<4>:
+    InlineTest<4> foo = InlineTest { x: [1, 2, 3, 4], y: 1 }
+    return foo

scripts/zx_tests/inline_struct_generic.zxf

@@ -0,0 +1,8 @@
+struct InlineTest<N> {
+    u32[N] x
+    field y
+}
+
+def main() -> InlineTest<4>:
+    InlineTest<5> foo = InlineTest { x: [1, 2, 3, 4, 5], y: 1 }
+    return foo

scripts/zx_tests/inline_struct_generic_2.zxf

@@ -0,0 +1,9 @@
+struct InlineTest<N> {
+    u32[N] x
+    field y
+}
+
+const InlineTest<4> foo = InlineTest { x: [1, 2, 3, 4, 5], y: 1 }
+
+def main() -> InlineTest<4>:
+    return foo

scripts/zx_tests/inline_struct_generic_3.zxf

@@ -0,0 +1,8 @@
+struct InlineTest<N> {
+    u32[N] x
+    field y
+}
+
+def main() -> InlineTest<4>:
+    InlineTest<4> foo = InlineTest { x: [1, 2, 3, 4, 5], y: 1 }
+    return foo

scripts/zx_tests/inline_struct_generic_4.zxf

@@ -0,0 +1,8 @@
+struct InlineTest<N> {
+    u32[N] x
+    field y
+}
+
+def main() -> InlineTest<4>:
+    InlineTest<4> foo = MisspelledInlineTest { x: [1, 2, 3, 4], y: 1 }
+    return foo

scripts/zx_tests/inline_struct_generic_5.zxf

@@ -0,0 +1,9 @@
+struct InlineTest<N> {
+    u32[N] x
+    field y
+}
+
+const InlineTest<4> foo = MisspelledInlineTest { x: [1, 2, 3, 4], y: 1 }
+
+def main() -> InlineTest<4>:
+    return foo

scripts/zx_tests/inner_struct_generic.zx

@@ -0,0 +1,17 @@
+struct Foo<N> {
+    u32[N] a
+    u64 b
+}
+
+struct Bar<N> {
+    Foo<N> a
+    u64 b
+}
+
+const Bar<4> baz = Bar {
+    a: Foo { a: [1, 2, 3, 4], b: 0 },
+    b: 0
+}
+
+def main() -> Bar<4>:
+    return baz

scripts/zx_tests/inner_struct_generic.zxf

@@ -0,0 +1,17 @@
+struct Foo<N> {
+    u32[N] a
+    u64 b
+}
+
+struct Bar<N> {
+    Foo<N> a
+    u64 b
+}
+
+const Bar<4> baz = Bar {
+    a: Foo { a: [1, 2, 3], b: 0 },
+    b: 0
+}
+
+def main() -> Bar<4>:
+    return baz

scripts/zx_tests/literals.zx

@@ -0,0 +1,6 @@
+def main() -> bool:
+    assert(0xfa == 250)
+    assert(0xbeef == 48879)
+    assert(0xdeadbeef == 3735928559)
+    assert(0xc0ffee1111111111 == 13907095931411566865)
+    return true

scripts/zx_tests/redef_const.zxf

@@ -0,0 +1,5 @@
+const u32 A = 1
+const u32 A = 2
+
+def main() -> bool:
+    return false

scripts/zx_tests/redef_const_2.zxf

@@ -0,0 +1,6 @@
+from "EMBED" import FIELD_SIZE_IN_BITS as A
+
+const u32 A = 2
+
+def main() -> bool:
+    return false

scripts/zx_tests/redef_fn.zxf

@@ -0,0 +1,8 @@
+def foo() -> u32:
+    return 1
+
+def foo() -> u32:
+    return 2
+
+def main() -> u32:
+    return foo()

scripts/zx_tests/redef_import.zxf

@@ -0,0 +1,5 @@
+from "EMBED" import FIELD_SIZE_IN_BITS as A
+from "EMBED" import u16_to_bits as A
+
+def main() -> bool:
+    return false

scripts/zx_tests/redef_import_2.zxf

@@ -0,0 +1,5 @@
+import "EMBED"
+import "EMBED"
+
+def main() -> bool:
+    return false

scripts/zx_tests/redef_struct.zxf

@@ -0,0 +1,10 @@
+struct Foo {
+    u32 a
+}
+
+struct Foo {
+    u32 b
+}
+
+def main() -> bool:
+    return true

scripts/zx_tests/run_tests.sh

@@ -0,0 +1,28 @@
+#!/bin/bash
+
+TESTDIR=$(dirname -- "$0")
+ZXI=${TESTDIR}/../../target/release/examples/zxi
+error=0
+
+echo Running zx should-pass tests:
+for i in ${TESTDIR}/*.zx; do
+    ${ZXI} "$i" &>/dev/null
+    if [ "$?" != "0" ]; then
+        echo "[failure: should-pass] $i"
+        error=1
+    fi
+done
+echo Done.
+echo
+
+echo Running zx should-fail tests:
+for i in ${TESTDIR}/*.zxf; do
+    ${ZXI} "$i" &>/dev/null
+    if [ "$?" == "0" ]; then
+        echo "[failure: should-fail] $i"
+        error=1
+    fi
+done
+echo Done.
+
+exit $error

scripts/zx_tests/signed_remainder.zx

@@ -0,0 +1,21 @@
+from "field" import s_divisible, s_remainder
+
+def main() -> bool:
+    field q = 4
+
+    field a = -2048
+    assert((a % q) != 0)
+    assert(s_divisible(a, q))
+    assert(s_remainder(a, q) == 0)
+
+    field b = 2048
+    assert((b % q) == 0)
+    assert(s_divisible(b, q))
+    assert(s_remainder(b, q) == 0)
+
+    field c = -2049
+    assert((c % 2) == 0)
+    assert(!s_divisible(c, q))
+    assert(s_remainder(c, q) == 3)
+
+    return true

scripts/zx_tests/simple_loop.zx

@@ -0,0 +1,7 @@
+def main() -> bool:
+    u32 total = 0
+    for u32 j in 0..7 do
+        total = total + j
+    endfor
+    assert(total == 21)
+    return true

scripts/zx_tests/single_generic.zx

@@ -0,0 +1,5 @@
+def last<N>(u32[N] a) -> u32:
+    return a[N-1]
+
+def main() -> u32:
+    return last([1u32,2,3])

scripts/zx_tests/single_generic_2.zx

@@ -0,0 +1,6 @@
+def dbl<N,NN>(u32[N] a) -> u32[NN]:
+    // XXX NN is unconstrained! this is a weird and annoying thing
+    return [...a,...a]
+
+def main() -> u32[6]:
+    return dbl([1u32,2,3])

scripts/zx_tests/single_generic_2.zxf

@@ -0,0 +1,6 @@
+def dbl<N,NN>(u32[N] a) -> u32[NN]:
+    // XXX NN is unconstrained! this is a weird and annoying thing
+    return [...a,...a]
+
+def main() -> u32[5]:
+    return dbl([1u32,2,3])

scripts/zx_tests/single_generic_3.zx

@@ -0,0 +1,5 @@
+def last<N>(u32[N] a) -> u32:
+    return a[N-1]
+
+def main() -> u32:
+    return last([1u32, 2, ...[3u32, 4, 5]])

scripts/zx_tests/single_generic_const.zx

@@ -0,0 +1,7 @@
+const u32[5] asdf = [1,2,3,4,5]
+
+def last<N>(u32[N] a) -> u32:
+    return a[N-1]
+
+def main() -> u32:
+    return last(asdf)

scripts/zx_tests/single_generic_const_2.zx

@@ -0,0 +1,7 @@
+const u32[5] asdf = [1,2,3,4,5]
+
+def dbl<N,NN>(u32[N] a) -> u32[NN]:
+    return [...a,...a]
+
+def main() -> u32[10]:
+    return dbl(asdf)

scripts/zx_tests/single_generic_const_2.zxf

@@ -0,0 +1,7 @@
+const u32[5] asdf = [1,2,3,4,5]
+
+def dbl<N,NN>(u32[N] a) -> u32[NN]:
+    return [...a,...a]
+
+def main() -> u32[6]:
+    return dbl(asdf)

scripts/zx_tests/struct_eq.zx

@@ -0,0 +1,22 @@
+struct Bar {
+    u8 d
+    u16 e
+}
+
+struct Foo {
+    u32[7] a
+    field b
+    u64 c
+    Bar d
+}
+
+def main() -> Foo:
+    Bar w = Bar { d: 0, e: 0 }
+    assert(w == w)
+
+    Foo x = Foo { a: [7; 7], b: 1, c: 0, d: w }
+    Foo y = Foo { a: [8; 7], b: 0, c: 1, d: w }
+
+    assert(x != y)
+    assert(!(x == y))
+    return x

scripts/zx_tests/struct_eq.zxf

@@ -0,0 +1,18 @@
+struct Bar {
+    u8 d
+    u16 e
+}
+
+struct Foo {
+    u32[7] a
+    field b
+    u64 c
+    Bar d
+}
+
+def main() -> bool:
+    Bar w = Bar { d: 0, e: 0 }
+    Foo x = Foo { a: [7; 7], b: 1, c: 0, d: w }
+    assert(x != w)
+    assert(!(x == y))
+    return x == y || x != y

scripts/zx_tests/struct_read_write.zx

@@ -0,0 +1,12 @@
+struct Foo {
+    u32 a
+    u8 b
+}
+
+def main() -> u8:
+    Foo bar = Foo { a: 1, b: 2 }
+    assert(bar.a == 1)
+    assert(bar.b == 2)
+    bar.a = 2
+    assert(bar.a == 2)
+    return bar.b