summaryrefslogtreecommitdiff
path: root/tests/fstar
diff options
context:
space:
mode:
Diffstat (limited to 'tests/fstar')
-rw-r--r--tests/fstar/misc/Loops.Clauses.Template.fst51
-rw-r--r--tests/fstar/misc/Loops.Clauses.fst51
-rw-r--r--tests/fstar/misc/Loops.Funs.fst356
3 files changed, 446 insertions, 12 deletions
diff --git a/tests/fstar/misc/Loops.Clauses.Template.fst b/tests/fstar/misc/Loops.Clauses.Template.fst
index 3e44ef4f..cd29ca13 100644
--- a/tests/fstar/misc/Loops.Clauses.Template.fst
+++ b/tests/fstar/misc/Loops.Clauses.Template.fst
@@ -9,9 +9,14 @@ open Loops.Types
(** [loops::sum]: decreases clause *)
unfold let sum_decreases (max : u32) (i : u32) (s : u32) : nat = admit ()
-(** [loops::sum_with_borrows]: decreases clause *)
+(** [loops::sum_with_mut_borrows]: decreases clause *)
unfold
-let sum_with_borrows_decreases (max : u32) (mi : u32) (ms : u32) : nat =
+let sum_with_mut_borrows_decreases (max : u32) (mi : u32) (ms : u32) : nat =
+ admit ()
+
+(** [loops::sum_with_shared_borrows]: decreases clause *)
+unfold
+let sum_with_shared_borrows_decreases (max : u32) (i : u32) (s : u32) : nat =
admit ()
(** [loops::list_nth_mut_loop]: decreases clause *)
@@ -19,15 +24,57 @@ unfold
let list_nth_mut_loop_decreases (t : Type0) (ls : list_t t) (i : u32) : nat =
admit ()
+(** [loops::list_nth_shared_loop]: decreases clause *)
+unfold
+let list_nth_shared_loop_decreases (t : Type0) (ls : list_t t) (i : u32) : nat
+ =
+ admit ()
+
(** [loops::list_nth_mut_loop_pair]: decreases clause *)
unfold
let list_nth_mut_loop_pair_decreases (t : Type0) (l : list_t t) (l0 : list_t t)
(i : u32) : nat =
admit ()
+(** [loops::list_nth_shared_loop_pair]: decreases clause *)
+unfold
+let list_nth_shared_loop_pair_decreases (t : Type0) (l : list_t t)
+ (l0 : list_t t) (i : u32) : nat =
+ admit ()
+
(** [loops::list_nth_mut_loop_pair_merge]: decreases clause *)
unfold
let list_nth_mut_loop_pair_merge_decreases (t : Type0) (l : list_t t)
(l0 : list_t t) (i : u32) : nat =
admit ()
+(** [loops::list_nth_shared_loop_pair_merge]: decreases clause *)
+unfold
+let list_nth_shared_loop_pair_merge_decreases (t : Type0) (l : list_t t)
+ (l0 : list_t t) (i : u32) : nat =
+ admit ()
+
+(** [loops::list_nth_mut_shared_loop_pair]: decreases clause *)
+unfold
+let list_nth_mut_shared_loop_pair_decreases (t : Type0) (l : list_t t)
+ (l0 : list_t t) (i : u32) : nat =
+ admit ()
+
+(** [loops::list_nth_mut_shared_loop_pair_merge]: decreases clause *)
+unfold
+let list_nth_mut_shared_loop_pair_merge_decreases (t : Type0) (l : list_t t)
+ (l0 : list_t t) (i : u32) : nat =
+ admit ()
+
+(** [loops::list_nth_shared_mut_loop_pair]: decreases clause *)
+unfold
+let list_nth_shared_mut_loop_pair_decreases (t : Type0) (l : list_t t)
+ (l0 : list_t t) (i : u32) : nat =
+ admit ()
+
+(** [loops::list_nth_shared_mut_loop_pair_merge]: decreases clause *)
+unfold
+let list_nth_shared_mut_loop_pair_merge_decreases (t : Type0) (l : list_t t)
+ (l0 : list_t t) (i : u32) : nat =
+ admit ()
+
diff --git a/tests/fstar/misc/Loops.Clauses.fst b/tests/fstar/misc/Loops.Clauses.fst
index d315a4f0..9cf5db1f 100644
--- a/tests/fstar/misc/Loops.Clauses.fst
+++ b/tests/fstar/misc/Loops.Clauses.fst
@@ -9,25 +9,70 @@ open Loops.Types
unfold let sum_decreases (max : u32) (i : u32) (s : u32) : nat =
if i <= max then max - i else 0
+(** [loops::sum_with_mut_borrows]: decreases clause *)
+unfold
+let sum_with_mut_borrows_decreases (max : u32) (mi : u32) (ms : u32) : nat =
+ if max >= mi then max - mi else 0
-(** [loops::sum_with_borrows]: decreases clause *)
+(** [loops::sum_with_shared_borrows]: decreases clause *)
unfold
-let sum_with_borrows_decreases (max : u32) (mi : u32) (ms : u32) : nat =
- if mi <= max then max - mi else 0
+let sum_with_shared_borrows_decreases (max : u32) (i : u32) (s : u32) : nat =
+ if max >= i 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 =
i
+(** [loops::list_nth_shared_loop]: decreases clause *)
+unfold
+let list_nth_shared_loop_decreases (t : Type0) (ls : list_t t) (i : u32) : list_t t =
+ ls
+
(** [loops::list_nth_mut_loop_pair]: decreases clause *)
unfold
let list_nth_mut_loop_pair_decreases (t : Type0) (l : list_t t) (l0 : list_t t)
(i : u32) : nat =
i
+(** [loops::list_nth_shared_loop_pair]: decreases clause *)
+unfold
+let list_nth_shared_loop_pair_decreases (t : Type0) (l : list_t t)
+ (l0 : list_t t) (i : u32) : list_t t =
+ l
+
(** [loops::list_nth_mut_loop_pair_merge]: decreases clause *)
unfold
let list_nth_mut_loop_pair_merge_decreases (t : Type0) (l : list_t t)
(l0 : list_t t) (i : u32) : nat =
i
+
+(** [loops::list_nth_shared_loop_pair_merge]: decreases clause *)
+unfold
+let list_nth_shared_loop_pair_merge_decreases (t : Type0) (l : list_t t)
+ (l0 : list_t t) (i : u32) : list_t t =
+ l
+
+(** [loops::list_nth_mut_shared_loop_pair]: decreases clause *)
+unfold
+let list_nth_mut_shared_loop_pair_decreases (t : Type0) (l : list_t t)
+ (l0 : list_t t) (i : u32) : list_t t =
+ l
+
+(** [loops::list_nth_mut_shared_loop_pair_merge]: decreases clause *)
+unfold
+let list_nth_mut_shared_loop_pair_merge_decreases (t : Type0) (l : list_t t)
+ (l0 : list_t t) (i : u32) : list_t t =
+ l
+
+(** [loops::list_nth_shared_mut_loop_pair]: decreases clause *)
+unfold
+let list_nth_shared_mut_loop_pair_decreases (t : Type0) (l : list_t t)
+ (l0 : list_t t) (i : u32) : list_t t =
+ l
+
+(** [loops::list_nth_shared_mut_loop_pair_merge]: decreases clause *)
+unfold
+let list_nth_shared_mut_loop_pair_merge_decreases (t : Type0) (l : list_t t)
+ (l0 : list_t t) (i : u32) : list_t t =
+ l
diff --git a/tests/fstar/misc/Loops.Funs.fst b/tests/fstar/misc/Loops.Funs.fst
index 05d1f70f..ee8e95d2 100644
--- a/tests/fstar/misc/Loops.Funs.fst
+++ b/tests/fstar/misc/Loops.Funs.fst
@@ -27,10 +27,10 @@ let rec sum_loop_fwd
(** [loops::sum] *)
let sum_fwd (max : u32) : result u32 = sum_loop_fwd max 0 0
-(** [loops::sum_with_borrows] *)
-let rec sum_with_borrows_loop_fwd
+(** [loops::sum_with_mut_borrows] *)
+let rec sum_with_mut_borrows_loop_fwd
(max : u32) (mi : u32) (ms : u32) :
- Tot (result u32) (decreases (sum_with_borrows_decreases max mi ms))
+ Tot (result u32) (decreases (sum_with_mut_borrows_decreases max mi ms))
=
if mi < max
then
@@ -39,14 +39,35 @@ let rec sum_with_borrows_loop_fwd
| Return ms0 ->
begin match u32_add mi 1 with
| Fail e -> Fail e
- | Return mi0 -> sum_with_borrows_loop_fwd max mi0 ms0
+ | Return mi0 -> sum_with_mut_borrows_loop_fwd max mi0 ms0
end
end
else u32_mul ms 2
-(** [loops::sum_with_borrows] *)
-let sum_with_borrows_fwd (max : u32) : result u32 =
- sum_with_borrows_loop_fwd max 0 0
+(** [loops::sum_with_mut_borrows] *)
+let sum_with_mut_borrows_fwd (max : u32) : result u32 =
+ sum_with_mut_borrows_loop_fwd max 0 0
+
+(** [loops::sum_with_shared_borrows] *)
+let rec sum_with_shared_borrows_loop_fwd
+ (max : u32) (i : u32) (s : u32) :
+ Tot (result u32) (decreases (sum_with_shared_borrows_decreases max i s))
+ =
+ if i < max
+ then
+ begin match u32_add i 1 with
+ | Fail e -> Fail e
+ | Return i0 ->
+ begin match u32_add s i0 with
+ | Fail e -> Fail e
+ | Return s0 -> sum_with_shared_borrows_loop_fwd max i0 s0
+ end
+ end
+ else u32_mul s 2
+
+(** [loops::sum_with_shared_borrows] *)
+let sum_with_shared_borrows_fwd (max : u32) : result u32 =
+ sum_with_shared_borrows_loop_fwd max 0 0
(** [loops::list_nth_mut_loop] *)
let rec list_nth_mut_loop_loop_fwd
@@ -95,6 +116,27 @@ let list_nth_mut_loop_back
(t : Type0) (ls : list_t t) (i : u32) (ret : t) : result (list_t t) =
list_nth_mut_loop_loop_back t ls i ret
+(** [loops::list_nth_shared_loop] *)
+let rec list_nth_shared_loop_loop_fwd
+ (t : Type0) (ls : list_t t) (i : u32) :
+ Tot (result t) (decreases (list_nth_shared_loop_decreases t ls i))
+ =
+ begin match ls with
+ | ListCons x tl ->
+ if i = 0
+ then Return x
+ else
+ begin match u32_sub i 1 with
+ | Fail e -> Fail e
+ | Return i0 -> list_nth_shared_loop_loop_fwd t tl i0
+ end
+ | ListNil -> Fail Failure
+ end
+
+(** [loops::list_nth_shared_loop] *)
+let list_nth_shared_loop_fwd (t : Type0) (ls : list_t t) (i : u32) : result t =
+ list_nth_shared_loop_loop_fwd t ls i
+
(** [loops::list_nth_mut_loop_pair] *)
let rec list_nth_mut_loop_pair_loop_fwd
(t : Type0) (l : list_t t) (l0 : list_t t) (i : u32) :
@@ -187,6 +229,33 @@ let list_nth_mut_loop_pair_back'b
=
list_nth_mut_loop_pair_loop_back'b t ls0 ls1 i ret
+(** [loops::list_nth_shared_loop_pair] *)
+let rec list_nth_shared_loop_pair_loop_fwd
+ (t : Type0) (l : list_t t) (l0 : list_t t) (i : u32) :
+ Tot (result (t & t))
+ (decreases (list_nth_shared_loop_pair_decreases t l l0 i))
+ =
+ begin match l with
+ | ListCons x0 tl0 ->
+ begin match l0 with
+ | ListCons x1 tl1 ->
+ if i = 0
+ then Return (x0, x1)
+ else
+ begin match u32_sub i 1 with
+ | Fail e -> Fail e
+ | Return i0 -> list_nth_shared_loop_pair_loop_fwd t tl0 tl1 i0
+ end
+ | ListNil -> Fail Failure
+ end
+ | ListNil -> Fail Failure
+ end
+
+(** [loops::list_nth_shared_loop_pair] *)
+let list_nth_shared_loop_pair_fwd
+ (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) : result (t & t) =
+ list_nth_shared_loop_pair_loop_fwd t ls0 ls1 i
+
(** [loops::list_nth_mut_loop_pair_merge] *)
let rec list_nth_mut_loop_pair_merge_loop_fwd
(t : Type0) (l : list_t t) (l0 : list_t t) (i : u32) :
@@ -248,3 +317,276 @@ let list_nth_mut_loop_pair_merge_back
=
list_nth_mut_loop_pair_merge_loop_back t ls0 ls1 i ret
+(** [loops::list_nth_shared_loop_pair_merge] *)
+let rec list_nth_shared_loop_pair_merge_loop_fwd
+ (t : Type0) (l : list_t t) (l0 : list_t t) (i : u32) :
+ Tot (result (t & t))
+ (decreases (list_nth_shared_loop_pair_merge_decreases t l l0 i))
+ =
+ begin match l with
+ | ListCons x0 tl0 ->
+ begin match l0 with
+ | ListCons x1 tl1 ->
+ if i = 0
+ then Return (x0, x1)
+ else
+ begin match u32_sub i 1 with
+ | Fail e -> Fail e
+ | Return i0 -> list_nth_shared_loop_pair_merge_loop_fwd t tl0 tl1 i0
+ end
+ | ListNil -> Fail Failure
+ end
+ | ListNil -> Fail Failure
+ end
+
+(** [loops::list_nth_shared_loop_pair_merge] *)
+let list_nth_shared_loop_pair_merge_fwd
+ (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) : result (t & t) =
+ list_nth_shared_loop_pair_merge_loop_fwd t ls0 ls1 i
+
+(** [loops::list_nth_mut_shared_loop_pair] *)
+let rec list_nth_mut_shared_loop_pair_loop_fwd
+ (t : Type0) (l : list_t t) (l0 : list_t t) (i : u32) :
+ Tot (result (t & t))
+ (decreases (list_nth_mut_shared_loop_pair_decreases t l l0 i))
+ =
+ begin match l with
+ | ListCons x0 tl0 ->
+ begin match l0 with
+ | ListCons x1 tl1 ->
+ if i = 0
+ then Return (x0, x1)
+ else
+ begin match u32_sub i 1 with
+ | Fail e -> Fail e
+ | Return i0 -> list_nth_mut_shared_loop_pair_loop_fwd t tl0 tl1 i0
+ end
+ | ListNil -> Fail Failure
+ end
+ | ListNil -> Fail Failure
+ end
+
+(** [loops::list_nth_mut_shared_loop_pair] *)
+let list_nth_mut_shared_loop_pair_fwd
+ (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) : result (t & t) =
+ list_nth_mut_shared_loop_pair_loop_fwd t ls0 ls1 i
+
+(** [loops::list_nth_mut_shared_loop_pair] *)
+let rec list_nth_mut_shared_loop_pair_loop_back
+ (t : Type0) (l : list_t t) (l0 : list_t t) (i : u32) (ret : t) :
+ Tot (result (list_t t))
+ (decreases (list_nth_mut_shared_loop_pair_decreases t l l0 i))
+ =
+ begin match l with
+ | ListCons x0 tl0 ->
+ begin match l0 with
+ | ListCons x1 tl1 ->
+ if i = 0
+ then Return (ListCons ret tl0)
+ else
+ begin match u32_sub i 1 with
+ | Fail e -> Fail e
+ | Return i0 ->
+ begin match list_nth_mut_shared_loop_pair_loop_back t tl0 tl1 i0 ret
+ with
+ | Fail e -> Fail e
+ | Return l1 -> Return (ListCons x0 l1)
+ end
+ end
+ | ListNil -> Fail Failure
+ end
+ | ListNil -> Fail Failure
+ end
+
+(** [loops::list_nth_mut_shared_loop_pair] *)
+let list_nth_mut_shared_loop_pair_back
+ (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) (ret : t) :
+ result (list_t t)
+ =
+ list_nth_mut_shared_loop_pair_loop_back t ls0 ls1 i ret
+
+(** [loops::list_nth_mut_shared_loop_pair_merge] *)
+let rec list_nth_mut_shared_loop_pair_merge_loop_fwd
+ (t : Type0) (l : list_t t) (l0 : list_t t) (i : u32) :
+ Tot (result (t & t))
+ (decreases (list_nth_mut_shared_loop_pair_merge_decreases t l l0 i))
+ =
+ begin match l with
+ | ListCons x0 tl0 ->
+ begin match l0 with
+ | ListCons x1 tl1 ->
+ if i = 0
+ then Return (x0, x1)
+ else
+ begin match u32_sub i 1 with
+ | Fail e -> Fail e
+ | Return i0 ->
+ list_nth_mut_shared_loop_pair_merge_loop_fwd t tl0 tl1 i0
+ end
+ | ListNil -> Fail Failure
+ end
+ | ListNil -> Fail Failure
+ end
+
+(** [loops::list_nth_mut_shared_loop_pair_merge] *)
+let list_nth_mut_shared_loop_pair_merge_fwd
+ (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) : result (t & t) =
+ list_nth_mut_shared_loop_pair_merge_loop_fwd t ls0 ls1 i
+
+(** [loops::list_nth_mut_shared_loop_pair_merge] *)
+let rec list_nth_mut_shared_loop_pair_merge_loop_back
+ (t : Type0) (l : list_t t) (l0 : list_t t) (i : u32) (ret : t) :
+ Tot (result (list_t t))
+ (decreases (list_nth_mut_shared_loop_pair_merge_decreases t l l0 i))
+ =
+ begin match l with
+ | ListCons x0 tl0 ->
+ begin match l0 with
+ | ListCons x1 tl1 ->
+ if i = 0
+ then Return (ListCons ret tl0)
+ else
+ begin match u32_sub i 1 with
+ | Fail e -> Fail e
+ | Return i0 ->
+ begin match
+ list_nth_mut_shared_loop_pair_merge_loop_back t tl0 tl1 i0 ret with
+ | Fail e -> Fail e
+ | Return l1 -> Return (ListCons x0 l1)
+ end
+ end
+ | ListNil -> Fail Failure
+ end
+ | ListNil -> Fail Failure
+ end
+
+(** [loops::list_nth_mut_shared_loop_pair_merge] *)
+let list_nth_mut_shared_loop_pair_merge_back
+ (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) (ret : t) :
+ result (list_t t)
+ =
+ list_nth_mut_shared_loop_pair_merge_loop_back t ls0 ls1 i ret
+
+(** [loops::list_nth_shared_mut_loop_pair] *)
+let rec list_nth_shared_mut_loop_pair_loop_fwd
+ (t : Type0) (l : list_t t) (l0 : list_t t) (i : u32) :
+ Tot (result (t & t))
+ (decreases (list_nth_shared_mut_loop_pair_decreases t l l0 i))
+ =
+ begin match l with
+ | ListCons x0 tl0 ->
+ begin match l0 with
+ | ListCons x1 tl1 ->
+ if i = 0
+ then Return (x0, x1)
+ else
+ begin match u32_sub i 1 with
+ | Fail e -> Fail e
+ | Return i0 -> list_nth_shared_mut_loop_pair_loop_fwd t tl0 tl1 i0
+ end
+ | ListNil -> Fail Failure
+ end
+ | ListNil -> Fail Failure
+ end
+
+(** [loops::list_nth_shared_mut_loop_pair] *)
+let list_nth_shared_mut_loop_pair_fwd
+ (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) : result (t & t) =
+ list_nth_shared_mut_loop_pair_loop_fwd t ls0 ls1 i
+
+(** [loops::list_nth_shared_mut_loop_pair] *)
+let rec list_nth_shared_mut_loop_pair_loop_back
+ (t : Type0) (l : list_t t) (l0 : list_t t) (i : u32) (ret : t) :
+ Tot (result (list_t t))
+ (decreases (list_nth_shared_mut_loop_pair_decreases t l l0 i))
+ =
+ begin match l with
+ | ListCons x0 tl0 ->
+ begin match l0 with
+ | ListCons x1 tl1 ->
+ if i = 0
+ then Return (ListCons ret tl1)
+ else
+ begin match u32_sub i 1 with
+ | Fail e -> Fail e
+ | Return i0 ->
+ begin match list_nth_shared_mut_loop_pair_loop_back t tl0 tl1 i0 ret
+ with
+ | Fail e -> Fail e
+ | Return l1 -> Return (ListCons x1 l1)
+ end
+ end
+ | ListNil -> Fail Failure
+ end
+ | ListNil -> Fail Failure
+ end
+
+(** [loops::list_nth_shared_mut_loop_pair] *)
+let list_nth_shared_mut_loop_pair_back
+ (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) (ret : t) :
+ result (list_t t)
+ =
+ list_nth_shared_mut_loop_pair_loop_back t ls0 ls1 i ret
+
+(** [loops::list_nth_shared_mut_loop_pair_merge] *)
+let rec list_nth_shared_mut_loop_pair_merge_loop_fwd
+ (t : Type0) (l : list_t t) (l0 : list_t t) (i : u32) :
+ Tot (result (t & t))
+ (decreases (list_nth_shared_mut_loop_pair_merge_decreases t l l0 i))
+ =
+ begin match l with
+ | ListCons x0 tl0 ->
+ begin match l0 with
+ | ListCons x1 tl1 ->
+ if i = 0
+ then Return (x0, x1)
+ else
+ begin match u32_sub i 1 with
+ | Fail e -> Fail e
+ | Return i0 ->
+ list_nth_shared_mut_loop_pair_merge_loop_fwd t tl0 tl1 i0
+ end
+ | ListNil -> Fail Failure
+ end
+ | ListNil -> Fail Failure
+ end
+
+(** [loops::list_nth_shared_mut_loop_pair_merge] *)
+let list_nth_shared_mut_loop_pair_merge_fwd
+ (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) : result (t & t) =
+ list_nth_shared_mut_loop_pair_merge_loop_fwd t ls0 ls1 i
+
+(** [loops::list_nth_shared_mut_loop_pair_merge] *)
+let rec list_nth_shared_mut_loop_pair_merge_loop_back
+ (t : Type0) (l : list_t t) (l0 : list_t t) (i : u32) (ret : t) :
+ Tot (result (list_t t))
+ (decreases (list_nth_shared_mut_loop_pair_merge_decreases t l l0 i))
+ =
+ begin match l with
+ | ListCons x0 tl0 ->
+ begin match l0 with
+ | ListCons x1 tl1 ->
+ if i = 0
+ then Return (ListCons ret tl1)
+ else
+ begin match u32_sub i 1 with
+ | Fail e -> Fail e
+ | Return i0 ->
+ begin match
+ list_nth_shared_mut_loop_pair_merge_loop_back t tl0 tl1 i0 ret with
+ | Fail e -> Fail e
+ | Return l1 -> Return (ListCons x1 l1)
+ end
+ end
+ | ListNil -> Fail Failure
+ end
+ | ListNil -> Fail Failure
+ end
+
+(** [loops::list_nth_shared_mut_loop_pair_merge] *)
+let list_nth_shared_mut_loop_pair_merge_back
+ (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) (ret : t) :
+ result (list_t t)
+ =
+ list_nth_shared_mut_loop_pair_merge_loop_back t ls0 ls1 i ret
+
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-23 08:32:23 +0000