From af929939c44116cdfd5faa845273d0f032d761bf Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Sat, 7 Jan 2023 17:21:27 +0100
Subject: Improve the order of the loop input parameters

---
 tests/fstar/hashmap/Hashmap.Clauses.Template.fst   |  4 ++--
 tests/fstar/hashmap/Hashmap.Clauses.fst            |  4 ++--
 tests/fstar/hashmap/Hashmap.Funs.fst               | 16 ++++++-------
 tests/fstar/hashmap/Hashmap.Properties.fst         | 28 +++++++++++-----------
 .../HashmapMain.Clauses.Template.fst               |  4 ++--
 .../fstar/hashmap_on_disk/HashmapMain.Clauses.fst  |  4 ++--
 tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst   | 16 ++++++-------
 tests/fstar/misc/Loops.Clauses.Template.fst        |  2 +-
 tests/fstar/misc/Loops.Clauses.fst                 |  4 ++--
 tests/fstar/misc/Loops.Funs.fst                    | 10 ++++----
 10 files changed, 46 insertions(+), 46 deletions(-)

(limited to 'tests/fstar')

diff --git a/tests/fstar/hashmap/Hashmap.Clauses.Template.fst b/tests/fstar/hashmap/Hashmap.Clauses.Template.fst
index 3e51c6f1..ce86071c 100644
--- a/tests/fstar/hashmap/Hashmap.Clauses.Template.fst
+++ b/tests/fstar/hashmap/Hashmap.Clauses.Template.fst
@@ -54,8 +54,8 @@ let hash_map_get_in_list_decreases (t : Type0) (key : usize) (ls : list_t t) :
 
 (** [hashmap::HashMap::{0}::get_mut_in_list]: decreases clause *)
 unfold
-let hash_map_get_mut_in_list_decreases (t : Type0) (key : usize)
-  (ls : list_t t) : nat =
+let hash_map_get_mut_in_list_decreases (t : Type0) (ls : list_t t)
+  (key : usize) : nat =
   admit ()
 
 (** [hashmap::HashMap::{0}::remove_from_list]: decreases clause *)
diff --git a/tests/fstar/hashmap/Hashmap.Clauses.fst b/tests/fstar/hashmap/Hashmap.Clauses.fst
index 4f3e37e9..2a9c0242 100644
--- a/tests/fstar/hashmap/Hashmap.Clauses.fst
+++ b/tests/fstar/hashmap/Hashmap.Clauses.fst
@@ -49,8 +49,8 @@ let hash_map_get_in_list_decreases (t : Type0) (key : usize) (ls : list_t t) :
 
 (** [hashmap::HashMap::get_mut_in_list]: decreases clause *)
 unfold
-let hash_map_get_mut_in_list_decreases (t : Type0) (key : usize)
-  (ls : list_t t) : list_t t =
+let hash_map_get_mut_in_list_decreases (t : Type0) (ls : list_t t)
+  (key : usize) : list_t t =
   ls
 
 (** [hashmap::HashMap::remove_from_list]: decreases clause *)
diff --git a/tests/fstar/hashmap/Hashmap.Funs.fst b/tests/fstar/hashmap/Hashmap.Funs.fst
index 81b253ad..14cea9cb 100644
--- a/tests/fstar/hashmap/Hashmap.Funs.fst
+++ b/tests/fstar/hashmap/Hashmap.Funs.fst
@@ -384,34 +384,34 @@ let hash_map_get_fwd
 
 (** [hashmap::HashMap::{0}::get_mut_in_list] *)
 let rec hash_map_get_mut_in_list_loop_fwd
-  (t : Type0) (key : usize) (ls : list_t t) :
-  Tot (result t) (decreases (hash_map_get_mut_in_list_decreases t key ls))
+  (t : Type0) (ls : list_t t) (key : usize) :
+  Tot (result t) (decreases (hash_map_get_mut_in_list_decreases t ls key))
   =
   begin match ls with
   | ListCons ckey cvalue tl ->
     if ckey = key
     then Return cvalue
-    else hash_map_get_mut_in_list_loop_fwd t key tl
+    else hash_map_get_mut_in_list_loop_fwd t tl key
   | ListNil -> Fail Failure
   end
 
 (** [hashmap::HashMap::{0}::get_mut_in_list] *)
 let hash_map_get_mut_in_list_fwd
   (t : Type0) (ls : list_t t) (key : usize) : result t =
-  hash_map_get_mut_in_list_loop_fwd t key ls
+  hash_map_get_mut_in_list_loop_fwd t ls key
 
 (** [hashmap::HashMap::{0}::get_mut_in_list] *)
 let rec hash_map_get_mut_in_list_loop_back
-  (t : Type0) (key : usize) (ls : list_t t) (ret : t) :
+  (t : Type0) (ls : list_t t) (key : usize) (ret : t) :
   Tot (result (list_t t))
-  (decreases (hash_map_get_mut_in_list_decreases t key ls))
+  (decreases (hash_map_get_mut_in_list_decreases t ls key))
   =
   begin match ls with
   | ListCons ckey cvalue tl ->
     if ckey = key
     then Return (ListCons ckey ret tl)
     else
-      begin match hash_map_get_mut_in_list_loop_back t key tl ret with
+      begin match hash_map_get_mut_in_list_loop_back t tl key ret with
       | Fail e -> Fail e
       | Return l -> Return (ListCons ckey cvalue l)
       end
@@ -421,7 +421,7 @@ let rec hash_map_get_mut_in_list_loop_back
 (** [hashmap::HashMap::{0}::get_mut_in_list] *)
 let hash_map_get_mut_in_list_back
   (t : Type0) (ls : list_t t) (key : usize) (ret : t) : result (list_t t) =
-  hash_map_get_mut_in_list_loop_back t key ls ret
+  hash_map_get_mut_in_list_loop_back t ls key ret
 
 (** [hashmap::HashMap::{0}::get_mut] *)
 let hash_map_get_mut_fwd
diff --git a/tests/fstar/hashmap/Hashmap.Properties.fst b/tests/fstar/hashmap/Hashmap.Properties.fst
index 724ca741..e1d0a541 100644
--- a/tests/fstar/hashmap/Hashmap.Properties.fst
+++ b/tests/fstar/hashmap/Hashmap.Properties.fst
@@ -2704,16 +2704,16 @@ let hash_map_get_fwd_lem #t self key = hash_map_get_fwd_lem_aux #t self key
 (**** get_mut_in_list'fwd *)
 
 val hash_map_get_mut_in_list_loop_fwd_lem
-  (#t : Type0) (key : usize) (ls : list_t t) :
+  (#t : Type0) (ls : list_t t) (key : usize) :
   Lemma
   (ensures (
-    match hash_map_get_mut_in_list_loop_fwd t key ls, slot_t_find_s key ls with
+    match hash_map_get_mut_in_list_loop_fwd t ls key, slot_t_find_s key ls with
     | Fail _, None -> True
     | Return x, Some x' -> x == x'
     | _ -> False))
 
 #push-options "--fuel 1"
-let rec hash_map_get_mut_in_list_loop_fwd_lem #t key ls =
+let rec hash_map_get_mut_in_list_loop_fwd_lem #t ls key =
   begin match ls with
   | ListCons ckey cvalue ls0 ->
     let b = ckey = key in
@@ -2721,8 +2721,8 @@ let rec hash_map_get_mut_in_list_loop_fwd_lem #t key ls =
     then ()
     else
       begin
-      hash_map_get_mut_in_list_loop_fwd_lem key ls0;
-      match hash_map_get_mut_in_list_loop_fwd t key ls0 with
+      hash_map_get_mut_in_list_loop_fwd_lem ls0 key;
+      match hash_map_get_mut_in_list_loop_fwd t ls0 key with
       | Fail _ -> ()
       | Return x -> ()
       end
@@ -2754,8 +2754,8 @@ let hash_map_get_mut_fwd_lem_aux #t self key =
       | Fail _ -> ()
       | Return l ->
         begin
-        hash_map_get_mut_in_list_loop_fwd_lem key l;
-        match hash_map_get_mut_in_list_loop_fwd t key l with
+        hash_map_get_mut_in_list_loop_fwd_lem l key;
+        match hash_map_get_mut_in_list_loop_fwd t l key with
         | Fail _ -> ()
         | Return x -> ()
         end
@@ -2771,17 +2771,17 @@ let hash_map_get_mut_fwd_lem #t self key =
 (**** get_mut_in_list'back *)
 
 val hash_map_get_mut_in_list_loop_back_lem
-  (#t : Type0) (key : usize) (ls : list_t t) (ret : t) :
+  (#t : Type0) (ls : list_t t) (key : usize) (ret : t) :
   Lemma
   (requires (Some? (slot_t_find_s key ls)))
   (ensures (
-    match hash_map_get_mut_in_list_loop_back t key ls ret with
+    match hash_map_get_mut_in_list_loop_back t ls key ret with
     | Fail _ -> False
     | Return ls' -> list_t_v ls' == find_update (same_key key) (list_t_v ls) (key,ret)
     | _ -> False))
 
 #push-options "--fuel 1"
-let rec hash_map_get_mut_in_list_loop_back_lem #t key ls ret =
+let rec hash_map_get_mut_in_list_loop_back_lem #t ls key ret =
   begin match ls with
   | ListCons ckey cvalue ls0 ->
     let b = ckey = key in
@@ -2789,8 +2789,8 @@ let rec hash_map_get_mut_in_list_loop_back_lem #t key ls ret =
     then let ls1 = ListCons ckey ret ls0 in ()
     else
       begin
-      hash_map_get_mut_in_list_loop_back_lem key ls0 ret;
-      match hash_map_get_mut_in_list_loop_back t key ls0 ret with
+      hash_map_get_mut_in_list_loop_back_lem ls0 key ret;
+      match hash_map_get_mut_in_list_loop_back t ls0 key ret with
       | Fail _ -> ()
       | Return l -> let ls1 = ListCons ckey cvalue l in ()
       end
@@ -2828,8 +2828,8 @@ let hash_map_get_mut_back_lem_refin #t self key ret =
       | Fail _ -> ()
       | Return l ->
         begin
-        hash_map_get_mut_in_list_loop_back_lem key l ret;
-        match hash_map_get_mut_in_list_loop_back t key l ret with
+        hash_map_get_mut_in_list_loop_back_lem l key ret;
+        match hash_map_get_mut_in_list_loop_back t l key ret with
         | Fail _ -> ()
         | Return l0 ->
           begin match vec_index_mut_back (list_t t) v hash_mod l0 with
diff --git a/tests/fstar/hashmap_on_disk/HashmapMain.Clauses.Template.fst b/tests/fstar/hashmap_on_disk/HashmapMain.Clauses.Template.fst
index 55685114..871de28a 100644
--- a/tests/fstar/hashmap_on_disk/HashmapMain.Clauses.Template.fst
+++ b/tests/fstar/hashmap_on_disk/HashmapMain.Clauses.Template.fst
@@ -55,8 +55,8 @@ let hashmap_hash_map_get_in_list_decreases (t : Type0) (key : usize)
 
 (** [hashmap_main::hashmap::HashMap::{0}::get_mut_in_list]: decreases clause *)
 unfold
-let hashmap_hash_map_get_mut_in_list_decreases (t : Type0) (key : usize)
-  (ls : hashmap_list_t t) : nat =
+let hashmap_hash_map_get_mut_in_list_decreases (t : Type0)
+  (ls : hashmap_list_t t) (key : usize) : nat =
   admit ()
 
 (** [hashmap_main::hashmap::HashMap::{0}::remove_from_list]: decreases clause *)
diff --git a/tests/fstar/hashmap_on_disk/HashmapMain.Clauses.fst b/tests/fstar/hashmap_on_disk/HashmapMain.Clauses.fst
index b864e32a..8afe2523 100644
--- a/tests/fstar/hashmap_on_disk/HashmapMain.Clauses.fst
+++ b/tests/fstar/hashmap_on_disk/HashmapMain.Clauses.fst
@@ -49,8 +49,8 @@ let hashmap_hash_map_get_in_list_decreases (t : Type0) (key : usize) (ls : hashm
 
 (** [hashmap::HashMap::get_mut_in_list]: decreases clause *)
 unfold
-let hashmap_hash_map_get_mut_in_list_decreases (t : Type0) (key : usize)
-  (ls : hashmap_list_t t) : hashmap_list_t t =
+let hashmap_hash_map_get_mut_in_list_decreases (t : Type0)
+  (ls : hashmap_list_t t) (key : usize) : hashmap_list_t t =
   ls
 
 (** [hashmap::HashMap::remove_from_list]: decreases clause *)
diff --git a/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst b/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst
index fdbf1404..42ee2a17 100644
--- a/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst
+++ b/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst
@@ -410,35 +410,35 @@ let hashmap_hash_map_get_fwd
 
 (** [hashmap_main::hashmap::HashMap::{0}::get_mut_in_list] *)
 let rec hashmap_hash_map_get_mut_in_list_loop_fwd
-  (t : Type0) (key : usize) (ls : hashmap_list_t t) :
+  (t : Type0) (ls : hashmap_list_t t) (key : usize) :
   Tot (result t)
-  (decreases (hashmap_hash_map_get_mut_in_list_decreases t key ls))
+  (decreases (hashmap_hash_map_get_mut_in_list_decreases t ls key))
   =
   begin match ls with
   | HashmapListCons ckey cvalue tl ->
     if ckey = key
     then Return cvalue
-    else hashmap_hash_map_get_mut_in_list_loop_fwd t key tl
+    else hashmap_hash_map_get_mut_in_list_loop_fwd t tl key
   | HashmapListNil -> Fail Failure
   end
 
 (** [hashmap_main::hashmap::HashMap::{0}::get_mut_in_list] *)
 let hashmap_hash_map_get_mut_in_list_fwd
   (t : Type0) (ls : hashmap_list_t t) (key : usize) : result t =
-  hashmap_hash_map_get_mut_in_list_loop_fwd t key ls
+  hashmap_hash_map_get_mut_in_list_loop_fwd t ls key
 
 (** [hashmap_main::hashmap::HashMap::{0}::get_mut_in_list] *)
 let rec hashmap_hash_map_get_mut_in_list_loop_back
-  (t : Type0) (key : usize) (ls : hashmap_list_t t) (ret : t) :
+  (t : Type0) (ls : hashmap_list_t t) (key : usize) (ret : t) :
   Tot (result (hashmap_list_t t))
-  (decreases (hashmap_hash_map_get_mut_in_list_decreases t key ls))
+  (decreases (hashmap_hash_map_get_mut_in_list_decreases t ls key))
   =
   begin match ls with
   | HashmapListCons ckey cvalue tl ->
     if ckey = key
     then Return (HashmapListCons ckey ret tl)
     else
-      begin match hashmap_hash_map_get_mut_in_list_loop_back t key tl ret with
+      begin match hashmap_hash_map_get_mut_in_list_loop_back t tl key ret with
       | Fail e -> Fail e
       | Return l -> Return (HashmapListCons ckey cvalue l)
       end
@@ -450,7 +450,7 @@ let hashmap_hash_map_get_mut_in_list_back
   (t : Type0) (ls : hashmap_list_t t) (key : usize) (ret : t) :
   result (hashmap_list_t t)
   =
-  hashmap_hash_map_get_mut_in_list_loop_back t key ls ret
+  hashmap_hash_map_get_mut_in_list_loop_back t ls key ret
 
 (** [hashmap_main::hashmap::HashMap::{0}::get_mut] *)
 let hashmap_hash_map_get_mut_fwd
diff --git a/tests/fstar/misc/Loops.Clauses.Template.fst b/tests/fstar/misc/Loops.Clauses.Template.fst
index 1b141d64..8cdc6e2c 100644
--- a/tests/fstar/misc/Loops.Clauses.Template.fst
+++ b/tests/fstar/misc/Loops.Clauses.Template.fst
@@ -42,7 +42,7 @@ let get_elem_mut_decreases (x : usize) (ls : list_t usize) : nat = admit ()
 
 (** [loops::get_elem_shared]: decreases clause *)
 unfold
-let get_elem_shared_decreases (x : usize) (slots : vec (list_t usize))
+let get_elem_shared_decreases (slots : vec (list_t usize)) (x : usize)
   (ls : list_t usize) (ls0 : list_t usize) : nat =
   admit ()
 
diff --git a/tests/fstar/misc/Loops.Clauses.fst b/tests/fstar/misc/Loops.Clauses.fst
index 57849896..a03f0302 100644
--- a/tests/fstar/misc/Loops.Clauses.fst
+++ b/tests/fstar/misc/Loops.Clauses.fst
@@ -43,8 +43,8 @@ let get_elem_mut_decreases (x : usize) (ls : list_t usize) : list_t usize = ls
 
 (** [loops::get_elem_shared]: decreases clause *)
 unfold
-let get_elem_shared_decreases (x : usize) (v : vec (list_t usize))
-  (l : list_t usize) (ls : list_t usize) : list_t usize =
+let get_elem_shared_decreases (slots : vec (list_t usize)) (x : usize)
+  (ls : list_t usize) (ls0 : list_t usize) : list_t usize =
   ls
 
 (** [loops::list_nth_mut_loop_with_id]: decreases clause *)
diff --git a/tests/fstar/misc/Loops.Funs.fst b/tests/fstar/misc/Loops.Funs.fst
index ca918e35..e8fb89e9 100644
--- a/tests/fstar/misc/Loops.Funs.fst
+++ b/tests/fstar/misc/Loops.Funs.fst
@@ -222,13 +222,13 @@ let get_elem_mut_back
 
 (** [loops::get_elem_shared] *)
 let rec get_elem_shared_loop_fwd
-  (x : usize) (slots : vec (list_t usize)) (ls : list_t usize)
+  (slots : vec (list_t usize)) (x : usize) (ls : list_t usize)
   (ls0 : list_t usize) :
-  Tot (result usize) (decreases (get_elem_shared_decreases x slots ls ls0))
+  Tot (result usize) (decreases (get_elem_shared_decreases slots x ls ls0))
   =
-  begin match ls0 with
+  begin match ls with
   | ListCons y tl ->
-    if y = x then Return y else get_elem_shared_loop_fwd x slots ls tl
+    if y = x then Return y else get_elem_shared_loop_fwd slots x tl ls0
   | ListNil -> Fail Failure
   end
 
@@ -237,7 +237,7 @@ let get_elem_shared_fwd
   (slots : vec (list_t usize)) (x : usize) : result usize =
   begin match vec_index_fwd (list_t usize) slots 0 with
   | Fail e -> Fail e
-  | Return l -> get_elem_shared_loop_fwd x slots l l
+  | Return l -> get_elem_shared_loop_fwd slots x l l
   end
 
 (** [loops::id_mut] *)
-- 
cgit v1.2.3