From 1951b6fac6ea0d4cf2a3943a6a7d9126dc7b488a Mon Sep 17 00:00:00 2001 From: Marco Eilers Date: Sat, 17 Feb 2024 00:33:23 +0100 Subject: [PATCH 1/2] 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__"] } } } From b07add959a9b7a547b53c3afd96cbd70650b4839 Mon Sep 17 00:00:00 2001 From: Marco Eilers Date: Sun, 18 Feb 2024 13:59:52 +0100 Subject: [PATCH 2/2] Better sum and sorted definitions --- src/nagini_translation/resources/bool.sil | 23 ++++++++--- .../verification/test_sum_sorted.py | 38 +++++++++++++++++++ 2 files changed, 55 insertions(+), 6 deletions(-) create mode 100644 tests/functional/verification/test_sum_sorted.py diff --git a/src/nagini_translation/resources/bool.sil b/src/nagini_translation/resources/bool.sil index f0b10125..212db54e 100644 --- a/src/nagini_translation/resources/bool.sil +++ b/src/nagini_translation/resources/bool.sil @@ -197,19 +197,26 @@ method sorted(r: Ref) returns (rs: Ref) 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)) + ensures result == __sum(__seq_ref_to_seq_int(r.list_acc)) -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))) +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$] { @@ -226,4 +233,8 @@ domain __SumHelper[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) + } } diff --git a/tests/functional/verification/test_sum_sorted.py b/tests/functional/verification/test_sum_sorted.py new file mode 100644 index 00000000..ab74cb24 --- /dev/null +++ b/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])))