From 1951b6fac6ea0d4cf2a3943a6a7d9126dc7b488a Mon Sep 17 00:00:00 2001
From: Marco Eilers <eilers.marco@googlemail.com>
Date: Sat, 17 Feb 2024 00:33:23 +0100
Subject: [PATCH] Basic sorted and sum

---
 src/nagini_translation/resources/bool.sil     | 41 ++++++++++++++++++-
 .../resources/preamble.index                  | 11 +++++
 2 files changed, 51 insertions(+), 1 deletion(-)

diff --git a/src/nagini_translation/resources/bool.sil b/src/nagini_translation/resources/bool.sil
index b3e4e0d9..f0b10125 100644
--- a/src/nagini_translation/resources/bool.sil
+++ b/src/nagini_translation/resources/bool.sil
@@ -187,4 +187,43 @@ function abs(a: Int): Int
 
 method print(r: Ref)
     requires Low(r)
-    requires LowEvent()
\ No newline at end of file
+    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 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)))
+
+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))
+
+function __seq_ref_to_seq_int(r: Ref): Seq[Int]
+    requires issubtype(typeof(r), list(int()))
+    requires acc(r.list_acc, 1/1000)
+    ensures |result| == |r.list_acc|
+    ensures forall i: Int :: { result[i] } i >= 0 && i < |result| ==>  result[i] == int___unbox__(list___getitem__(r, __prim__int___box__(i)))
+
+
+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)
+    }
+}
diff --git a/src/nagini_translation/resources/preamble.index b/src/nagini_translation/resources/preamble.index
index 67a8a7b7..19fae0e3 100644
--- a/src/nagini_translation/resources/preamble.index
+++ b/src/nagini_translation/resources/preamble.index
@@ -897,6 +897,11 @@
         "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": {
@@ -904,6 +909,12 @@
             "args": ["object"],
             "type": null,
             "MustTerminate": true
+        },
+        "sorted": {
+            "args": ["list"],
+            "type": "list",
+            "MustTerminate": true,
+            "requires": ["list___len__", "list___getitem__", "__prim__int___box__", "int___unbox__"]
         }
     }
 }