summaryrefslogtreecommitdiff
path: root/tests/fstar
diff options
context:
space:
mode:
Diffstat (limited to 'tests/fstar')
-rw-r--r--tests/fstar/misc/Loops.Clauses.Template.fst3
-rw-r--r--tests/fstar/misc/Loops.Clauses.fst4
-rw-r--r--tests/fstar/misc/Loops.Funs.fst20
3 files changed, 27 insertions, 0 deletions
diff --git a/tests/fstar/misc/Loops.Clauses.Template.fst b/tests/fstar/misc/Loops.Clauses.Template.fst
index a898e9fb..79a9dc4e 100644
--- a/tests/fstar/misc/Loops.Clauses.Template.fst
+++ b/tests/fstar/misc/Loops.Clauses.Template.fst
@@ -6,6 +6,9 @@ open Loops.Types
#set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
+(** [loops::sum]: decreases clause *)
+unfold let sum_decreases (max : u32) (i : u32) (s : u32) : nat = admit ()
+
(** [loops::list_nth_mut_loop]: decreases clause *)
unfold
let list_nth_mut_loop_decreases (t : Type0) (ls : list_t t) (i : u32) : nat =
diff --git a/tests/fstar/misc/Loops.Clauses.fst b/tests/fstar/misc/Loops.Clauses.fst
index e09eda9a..2087f2e7 100644
--- a/tests/fstar/misc/Loops.Clauses.fst
+++ b/tests/fstar/misc/Loops.Clauses.fst
@@ -5,6 +5,10 @@ open Loops.Types
#set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
+(** [loops::sum]: decreases clause *)
+unfold let sum_decreases (max : u32) (i : u32) (s : u32) : nat =
+ if i <= max then max - i else 0
+
(** [loops::list_nth_mut_loop]: decreases clause *)
unfold
let list_nth_mut_loop_decreases (t : Type0) (ls : list_t t) (i : u32) : nat =
diff --git a/tests/fstar/misc/Loops.Funs.fst b/tests/fstar/misc/Loops.Funs.fst
index 870a2159..a2ae2563 100644
--- a/tests/fstar/misc/Loops.Funs.fst
+++ b/tests/fstar/misc/Loops.Funs.fst
@@ -7,6 +7,26 @@ include Loops.Clauses
#set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
+(** [loops::sum] *)
+let rec sum_loop0_fwd
+ (max : u32) (i : u32) (s : u32) :
+ Tot (result u32) (decreases (sum_decreases max i s))
+ =
+ if i < max
+ then
+ begin match u32_add s i with
+ | Fail e -> Fail e
+ | Return s0 ->
+ begin match u32_add i 1 with
+ | Fail e -> Fail e
+ | Return i0 -> sum_loop0_fwd max i0 s0
+ end
+ end
+ else u32_mul s 2
+
+(** [loops::sum] *)
+let sum_fwd (max : u32) : result u32 = sum_loop0_fwd max 0 0
+
(** [loops::list_nth_mut_loop] *)
let rec list_nth_mut_loop_loop0_fwd
(t : Type0) (ls : list_t t) (i : u32) :