Sorted and sum

src/nagini_translation/resources/bool.sil

@@ -187,4 +187,54 @@ function abs(a: Int): Int
 
 method print(r: Ref)
     requires Low(r)
-    requires LowEvent()
+    requires LowEvent()
+
+method sorted(r: Ref) returns (rs: Ref)
+    requires issubtype(typeof(r), list(int()))
+    requires acc(r.list_acc, 1/1000)
+    ensures issubtype(typeof(rs), list(int()))
+    ensures acc(r.list_acc, 1/1000)
+    ensures acc(rs.list_acc)
+    ensures list___len__(rs) == list___len__(r)
+    ensures __toMS(r.list_acc) == __toMS(rs.list_acc)
+    ensures sum(r) == sum(rs)
+    ensures forall i1: Int, i2: Int :: { rs.list_acc[i1], rs.list_acc[i2] } i1 >= 0 && i1 < i2 && i2 < list___len__(rs) ==>
+            int___unbox__(list___getitem__(rs, __prim__int___box__(i1))) <= int___unbox__(list___getitem__(rs, __prim__int___box__(i2)))
+    ensures list___len__(r) == 1 ==> rs.list_acc == r.list_acc
+    ensures list___len__(r) > 1 ==> forall i: Int :: { r.list_acc[i] } i >= 0 && i < list___len__(r) ==> int___unbox__(list___getitem__(r, __prim__int___box__(i))) >= int___unbox__(list___getitem__(rs, __prim__int___box__(0)))
+    ensures list___len__(r) > 1 ==> forall i: Int :: { r.list_acc[i] } i >= 0 && i < list___len__(r) ==> int___unbox__(list___getitem__(r, __prim__int___box__(i))) <= int___unbox__(list___getitem__(rs, __prim__int___box__(list___len__(r) - 1)))
+
+
+function sum(r: Ref): Int
+    requires issubtype(typeof(r), list(int()))
+    requires acc(r.list_acc, 1/1000)
+    ensures result == __sum(__seq_ref_to_seq_int(r.list_acc))
+
+function __seq_ref_to_seq_int(sr: Seq[Ref]): Seq[Int]
+    ensures |result| == |sr|
+    ensures forall i: Int :: { result[i] } i >= 0 && i < |result| && issubtype(typeof(sr[i]), int()) ==>  result[i] == int___unbox__(sr[i])
+    ensures sr == Seq() ==> result == Seq()
+    ensures forall r: Ref :: {__seq_ref_to_seq_int(Seq(r))} issubtype(typeof(r), int()) ==> __seq_ref_to_seq_int(Seq(r)) == Seq(int___unbox__(r))
+    ensures forall sr1: Seq[Ref], sr2: Seq[Ref] :: {__seq_ref_to_seq_int(sr1 ++ sr2)} __seq_ref_to_seq_int(sr1 ++ sr2) == __seq_ref_to_seq_int(sr1) ++ __seq_ref_to_seq_int(sr2)
+    decreases _
+
+
+domain __SumHelper[T$] {
+    function __sum(s: Seq[Int]): Int
+
+    axiom __sum_def_1 {
+        __sum(Seq[Int]()) == 0
+    }
+
+    axiom __sum_def_2 {
+        forall __t: Int :: { __sum(Seq(__t)) } __sum(Seq(__t)) == __t
+    }
+
+    axiom __sum_def_3 {
+        forall __ss1: Seq[Int], __ss2: Seq[Int] :: { __sum(__ss1 ++ __ss2) } __sum(__ss1 ++ __ss2) == __sum(__ss1) + __sum(__ss2)
+    }
+
+    axiom __sum_def_4 {
+        forall __ss1: Seq[Int], __ss2: Seq[Int] :: { __sum(__ss1), __sum(__ss2) } __toMS(__ss1) == __toMS(__ss2) ==> __sum(__ss1) == __sum(__ss2)
+    }
+}

src/nagini_translation/resources/preamble.index

@@ -897,13 +897,24 @@
         "abs": {
             "args": ["__prim__int"],
             "type": "__prim__int"
+        },
+        "sum": {
+            "args": ["list"],
+            "type": "__prim__int",
+            "requires": ["__seq_ref_to_seq_int", "int___unbox__", "__prim__int___box__", "list___getitem__"]
         }
     },
     "methods": {
         "print": {
             "args": ["object"],
             "type": null,
             "MustTerminate": true
+        },
+        "sorted": {
+            "args": ["list"],
+            "type": "list",
+            "MustTerminate": true,
+            "requires": ["list___len__", "list___getitem__", "__prim__int___box__", "int___unbox__"]
         }
     }
 }

tests/functional/verification/test_sum_sorted.py

@@ -0,0 +1,38 @@
+# Any copyright is dedicated to the Public Domain.
+# http://creativecommons.org/publicdomain/zero/1.0/
+
+from nagini_contracts.contracts import *
+from typing import List
+
+
+def sum_sorted_test() -> None:
+    l = [3, 2]
+    l2 = sorted(l)
+    l3 = sum(l)
+    l4 = sorted([2])
+    Assert(l3 == 5)
+    Assert(l2[0] <= l2[1])
+    Assert(l4[0] == 2)
+    Assert(sum(l) == sum(l2))
+    Assert(l[0] >= l2[0])
+    #:: ExpectedOutput(assert.failed:assertion.false)
+    Assert(False)
+
+
+def sum_test(l1: List[int], l2: List[int]) -> None:
+    Requires(list_pred(l1) and list_pred(l2))
+    s3 = sum(l1) + sum(l2)
+    l3 = l1 + l2
+    Assert(s3 == sum(l3))
+    if len(l1) > 0:
+        #:: ExpectedOutput(assert.failed:assertion.false)
+        Assert(sum(l1) > 0)
+
+
+def sorted_test(l1: List[int], l2: List[int]) -> None:
+    Requires(list_pred(l1) and list_pred(l2))
+    l3 = sorted(l1)
+    Assert(l3 is not l2)
+    Assert(Forall(int, lambda i: Implies(i >= 0 and i < len(l3) - 1, l3[i] <= l3[i + 1])))
+    #:: ExpectedOutput(assert.failed:assertion.false)
+    Assert(Forall(int, lambda i: Implies(i >= 0 and i < len(l3) - 1, l3[i] < l3[i + 1])))