more compiler tests

Author: TomWambsgans

crates/lean_compiler/tests/test_compiler.rs

@@ -274,3 +274,37 @@ def main():
    "#;
     compile_and_run(&ProgramSource::Raw(program.to_string()), &[], false);
 }
+
+#[test]
+#[rustfmt::skip]
+fn test_soundness_suite() {
+    #[allow(clippy::type_complexity)]
+    let cases: &[(&str, &[u32], &[(usize, u32)])] = &[
+        ("soundness_0", &[3, 6, 7, 10, 9, 20, 26, 1], &[(0, 4), (1, 7), (2, 8), (3, 11), (4, 10), (5, 21), (6, 27), (7, 0), (7, 2)]),
+        ("soundness_1", &[5, 10, 6, 7, 42, 9, 5, 4],  &[(0, 6), (1, 11), (2, 7), (3, 8), (4, 43), (5, 10), (6, 6), (7, 5)]),
+        ("soundness_2", &[3, 4, 5, 29, 7, 1, 17, 46], &[(0, 2), (1, 5), (2, 6), (3, 30), (4, 8), (5, 0), (5, 2), (6, 18), (7, 47)]),
+        ("soundness_3", &[4, 2, 14, 120, 5, 10, 50, 55], &[(0, 5), (1, 3), (2, 15), (3, 121), (4, 6), (5, 11), (6, 51), (7, 56)]),
+        ("soundness_4", &[5, 10, 10, 3, 4, 19, 20, 1], &[(0, 6), (1, 11), (2, 11), (3, 4), (4, 5), (5, 20), (6, 50), (7, 0), (7, 2)]),
+        ("soundness_5", &[3, 4, 7, 19, 49, 28, 1, 3],  &[(0, 4), (1, 5), (2, 8), (3, 20), (4, 50), (5, 29), (6, 0), (6, 2), (7, 4)]),
+    ];
+
+    let to_input = |v: &[u32]| v.iter().copied().map(F::new).collect::<Vec<_>>();
+
+    for &(name, valid, perturbations) in cases {
+        let path = format!("{}/{}.py", test_data_dir(), name);
+        let bytecode = compile_program(&ProgramSource::Filepath(path));
+
+        try_execute_bytecode(&bytecode, &to_input(valid), &ExecutionWitness::default(), false)
+            .unwrap_or_else(|err| panic!("{name}: valid input {valid:?} must succeed, got {err:?}"));
+
+        for &(idx, bad_value) in perturbations {
+            let mut input = valid.to_vec();
+            input[idx] = bad_value;
+            let res = try_execute_bytecode(&bytecode, &to_input(&input), &ExecutionWitness::default(), false);
+            assert!(
+                res.is_err(),
+                "{name}: perturbation p[{idx}]={bad_value} (input {input:?}) unexpectedly succeeded",
+            );
+        }
+    }
+}

crates/lean_compiler/tests/test_data/soundness_0.py

@@ -0,0 +1,39 @@
+from snark_lib import *
+
+
+def main():
+    p = 0
+    a = p[0]
+    b = p[1]
+    c = p[2]
+    d = p[3]
+    e = p[4]
+    f = p[5]
+    g = p[6]
+    h = p[7]
+
+    assert double(a) == b
+    assert square_plus_one(a) == d
+    assert a + c == 10
+    assert e < 10
+    assert f <= 20
+
+    acc: Mut = 0
+    for i in unroll(0, 4):
+        acc = acc + p[i]
+    assert acc == g
+
+    if h == 1:
+        assert a + b == 9
+    else:
+        assert a == 0
+    return
+
+
+@inline
+def double(x):
+    return x + x
+
+
+def square_plus_one(x):
+    return x * x + 1

crates/lean_compiler/tests/test_data/soundness_1.py

@@ -0,0 +1,36 @@
+from snark_lib import *
+
+
+def main():
+    p = 0
+    n = p[0]
+    sum_range = p[1]
+    x = p[2]
+    y = p[3]
+    prod_xy = p[4]
+    outer = p[5]
+    inner_bound = p[6]
+    v = p[7]
+
+    assert n == 5
+
+    s: Mut = 0
+    for i in range(0, 5):
+        s = s + i
+    assert s == sum_range
+
+    assert mul(x, y) == prod_xy
+
+    nested: Mut = 0
+    for i in unroll(0, 3):
+        for j in unroll(0, 3):
+            nested = nested + i * j
+    assert nested == outer
+
+    assert v < inner_bound
+    assert inner_bound == v + 1
+    return
+
+
+def mul(a, b):
+    return a * b

crates/lean_compiler/tests/test_data/soundness_2.py

@@ -0,0 +1,58 @@
+from snark_lib import *
+
+
+def main():
+    p = 0
+    mode = p[0]
+    x = p[1]
+    y = p[2]
+    expected = p[3]
+    secondary = p[4]
+    flag = p[5]
+    offset = p[6]
+    total = p[7]
+
+    computed: Imu
+    match mode:
+        case 0:
+            computed = add_op(x, y)
+        case 1:
+            computed = sub_op(x, y)
+        case 2:
+            computed = mul_op(x, y)
+        case 3:
+            computed = combined(x, y)
+    assert computed == expected
+
+    adjusted: Imu
+    if flag == 0:
+        adjusted = bump(secondary, 1)
+    elif flag == 1:
+        adjusted = bump(secondary, 10)
+    else:
+        adjusted = bump(secondary, 100)
+    assert adjusted == offset
+
+    assert total == expected + offset
+    return
+
+
+def add_op(a, b):
+    return a + b
+
+
+def sub_op(a, b):
+    return a - b
+
+
+def mul_op(a, b):
+    return a * b
+
+
+def combined(a, b):
+    return mul_op(a, b) + add_op(a, b)
+
+
+@inline
+def bump(v, k):
+    return v + k

crates/lean_compiler/tests/test_data/soundness_3.py

@@ -0,0 +1,40 @@
+from snark_lib import *
+
+
+def main():
+    p = 0
+    n = p[0]
+    seed = p[1]
+    sum_expected = p[2]
+    prod_expected = p[3]
+    max_val = p[4]
+    upper = p[5]
+    w = p[6]
+    expected_final = p[7]
+
+    assert n == 4
+
+    arr = Array(4)
+    for i in unroll(0, 4):
+        arr[i] = seed + i
+
+    s: Mut = 0
+    for i in range(0, 4):
+        s = s + arr[i]
+    assert s == sum_expected
+
+    prod: Mut = 1
+    for i in unroll(0, 4):
+        prod = times(prod, arr[i])
+    assert prod == prod_expected
+
+    assert max_val < upper
+    assert upper <= 100
+    assert upper == max_val + 5
+    assert w + max_val == expected_final
+    return
+
+
+@inline
+def times(a, b):
+    return a * b

crates/lean_compiler/tests/test_data/soundness_4.py

@@ -0,0 +1,54 @@
+from snark_lib import *
+
+
+def main():
+    p = 0
+    n = p[0]
+    expected_sum_pos = p[1]
+    expected_sum_neg = p[2]
+    x = p[3]
+    y = p[4]
+    expected_pipeline = p[5]
+    threshold = p[6]
+    threshold_check = p[7]
+
+    assert n == 5
+
+    markers = Array(5)
+    for i in unroll(0, 5):
+        markers[i] = i
+
+    sum_pos: Mut = 0
+    sum_neg: Mut = 0
+    for i in range(0, 5):
+        m = markers[i]
+        if m == 0:
+            sum_neg = sum_neg + 10
+        else:
+            sum_pos = sum_pos + m
+    assert sum_pos == expected_sum_pos
+    assert sum_neg == expected_sum_neg
+
+    assert pipeline(x, y) == expected_pipeline
+
+    if threshold_check == 1:
+        assert threshold < 50
+    else:
+        assert threshold == 0
+
+    assert threshold_check * (1 - threshold_check) == 0
+    return
+
+
+@inline
+def pipeline(a, b):
+    return wrapper(a, b) + a
+
+
+def wrapper(a, b):
+    return inner(a, b) + b
+
+
+@inline
+def inner(a, b):
+    return a * b

crates/lean_compiler/tests/test_data/soundness_5.py

@@ -0,0 +1,63 @@
+from snark_lib import *
+
+
+def main():
+    p = 0
+    seed = p[0]
+    n = p[1]
+    last_write = p[2]
+    match_tally = p[3]
+    pipeline_squared = p[4]
+    paired = p[5]
+    flag = p[6]
+    alt = p[7]
+
+    assert n == 4
+
+    counter: Mut = 0
+    for i in range(0, 4):
+        counter = 2 * i + 1
+    assert counter == last_write
+
+    acc: Mut = seed
+    for i in range(0, 4):
+        match i:
+            case 0:
+                acc = acc + 1
+            case 1:
+                acc = acc + 3
+            case 2:
+                acc = acc + 5
+            case 3:
+                acc = acc + 7
+    assert acc == match_tally
+
+    assert sqr_via_pipeline(seed + n) == pipeline_squared
+
+    assert paired_sum(seed, n) == paired
+
+    chosen: Imu
+    if flag == 1:
+        chosen = seed
+    else:
+        chosen = seed * 2
+    assert chosen == alt
+
+    assert flag * (1 - flag) == 0
+    return
+
+
+@inline
+def sqr_via_pipeline(x):
+    return mul_boxed(x, x)
+
+
+def mul_boxed(a, b):
+    return a * b
+
+
+def paired_sum(a, b):
+    total: Mut = 0
+    for i in range(0, 4):
+        total = total + a + b
+    return total