Merge pull request #36 from NethermindEth/ElijahVlasov/toy-amm-fix

ToyAMM fix

pyproject.toml

@@ -18,7 +18,7 @@ skip_gitignore = true
 
 [tool.poetry]
 name = "horus-compile"
-version = "0.0.6.2"
+version = "0.0.6.3"
 authors = ["Nethermind <[email protected]>"]
 description = "Use formally verified annotations in your Cairo code"
 classifiers = [

src/horus/compiler/type_checker.py

@@ -12,6 +12,7 @@
     TypeTuple,
 )
 from starkware.cairo.lang.compiler.ast.expr import (
+    ExprAssignment,
     ExprCast,
     ExprConst,
     ExprDeref,
@@ -292,6 +293,17 @@ def visit_ExprFuncCall(self, expr: ExprFuncCall):
                     ),
                 )
             )
+
+            new_args = []
+            for arg in rvalue.arguments.args:
+                assert isinstance(arg, ExprAssignment)
+                new_expr = self.visit(arg.expr)
+                new_args.append(dataclasses.replace(arg, expr=new_expr))
+
+            replaced.rvalue.arguments = dataclasses.replace(
+                replaced.rvalue.arguments, args=new_args
+            )
+
             return dataclasses.replace(
                 replaced,
                 rvalue=dataclasses.replace(

tests/golden/math.cairo

@@ -0,0 +1,65 @@
+// Verifies that a >= 0 (or more precisely 0 <= a < RANGE_CHECK_BOUND).
+// @post 0 <= a and a < 2**128
+func assert_nn{range_check_ptr}(a) {
+    %{
+        from starkware.cairo.common.math_utils import assert_integer
+        assert_integer(ids.a)
+        assert 0 <= ids.a % PRIME < range_check_builtin.bound, f'a = {ids.a} is out of range.'
+    %}
+    a = [range_check_ptr];
+    let range_check_ptr = range_check_ptr + 1;
+    return ();
+}
+
+// Verifies that a <= b (or more precisely 0 <= b - a < RANGE_CHECK_BOUND).
+// @post 0 <= b - a and b - a < 2**128
+func assert_le{range_check_ptr}(a, b) {
+    assert_nn(b - a);
+    return ();
+}
+
+// Verifies that 0 <= a <= b.
+//
+// Prover assumption: b < RANGE_CHECK_BOUND.
+//
+// This function is still sound without the prover assumptions. In that case, it is guaranteed
+// that a < RANGE_CHECK_BOUND and b < 2 * RANGE_CHECK_BOUND.
+// @pre b < 2**128
+// @post 0 <= a and a <= b
+func assert_nn_le{range_check_ptr}(a, b) {
+    assert_nn(a);
+    assert_le(a, b);
+    return ();
+}
+
+// Returns q and r such that:
+//  0 <= q < rc_bound, 0 <= r < div and value = q * div + r.
+//
+// Assumption: 0 < div <= PRIME / rc_bound.
+// Prover assumption: value / div < rc_bound.
+//
+// The value of div is restricted to make sure there is no overflow.
+// q * div + r < (q + 1) * div <= rc_bound * (PRIME / rc_bound) = PRIME.
+//
+// @pre 0 < div
+// @pre div <= 10633823966279326983230456482242756608
+// @pre value < 2**128 * div
+// @post 0 <= $Return.q and $Return.q <  2**128
+// @post 0 <= $Return.r and $Return.r < div
+// @post value == $Return.q * div + $Return.r
+func unsigned_div_rem{range_check_ptr}(value, div) -> (q: felt, r: felt) {
+    let r = [range_check_ptr];
+    let q = [range_check_ptr + 1];
+    let range_check_ptr = range_check_ptr + 2;
+    %{
+        from starkware.cairo.common.math_utils import assert_integer
+        assert_integer(ids.div)
+        assert 0 < ids.div <= PRIME // range_check_builtin.bound, \
+            f'div={hex(ids.div)} is out of the valid range.'
+        ids.q, ids.r = divmod(ids.value, ids.div)
+    %}
+    assert_le(r, div - 1);
+
+    assert value = q * div + r;
+    return (q, r);
+}

tests/golden/math.gold

@@ -0,0 +1,65 @@
+{
+  "invariants": {},
+  "specifications": {
+    "__main__.assert_le": {
+      "decls": {},
+      "logical_variables": {},
+      "post": [
+        "(let ((a!1 (<= 0 (- (memory (+ fp (- 3))) (memory (+ fp (- 4))))))",
+        "      (a!2 (> 340282366920938463463374607431768211456",
+        "              (- (memory (+ fp (- 3))) (memory (+ fp (- 4)))))))",
+        "  (and a!1 a!2))"
+      ],
+      "pre": [
+        "true"
+      ],
+      "storage_update": {}
+    },
+    "__main__.assert_nn": {
+      "decls": {},
+      "logical_variables": {},
+      "post": [
+        "(and (<= 0 (memory (+ fp (- 3))))",
+        "     (> 340282366920938463463374607431768211456 (memory (+ fp (- 3)))))"
+      ],
+      "pre": [
+        "true"
+      ],
+      "storage_update": {}
+    },
+    "__main__.assert_nn_le": {
+      "decls": {},
+      "logical_variables": {},
+      "post": [
+        "(and (<= 0 (memory (+ fp (- 4))))",
+        "     (<= (memory (+ fp (- 4))) (memory (+ fp (- 3)))))"
+      ],
+      "pre": [
+        "(> 340282366920938463463374607431768211456 (memory (+ fp (- 3))))"
+      ],
+      "storage_update": {}
+    },
+    "__main__.unsigned_div_rem": {
+      "decls": {},
+      "logical_variables": {},
+      "post": [
+        "(let ((a!1 (+ (* (memory (+ ap (- 2))) (memory (+ fp (- 3))))",
+        "              (memory (+ ap (- 1))))))",
+        "  (and (<= 0 (memory (+ ap (- 2))))",
+        "       (> 340282366920938463463374607431768211456 (memory (+ ap (- 2))))",
+        "       (<= 0 (memory (+ ap (- 1))))",
+        "       (< (memory (+ ap (- 1))) (memory (+ fp (- 3))))",
+        "       (= (memory (+ fp (- 4))) a!1)))"
+      ],
+      "pre": [
+        "(let ((a!1 (< (memory (+ fp (- 4)))",
+        "              (* 340282366920938463463374607431768211456 (memory (+ fp (- 3)))))))",
+        "  (and (< 0 (memory (+ fp (- 3))))",
+        "       (>= 10633823966279326983230456482242756608 (memory (+ fp (- 3))))",
+        "       a!1))"
+      ],
+      "storage_update": {}
+    }
+  },
+  "storage_vars": {}
+}