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

---
 compiler/InterpreterLoops.ml                       | 40 ++++++++++++++++++++--
 compiler/InterpreterUtils.ml                       |  3 ++
 tests/coq/hashmap/Hashmap_Funs.v                   | 12 +++----
 tests/coq/hashmap_on_disk/HashmapMain_Funs.v       | 12 +++----
 tests/coq/misc/Loops.v                             |  8 ++---
 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 +++---
 15 files changed, 103 insertions(+), 64 deletions(-)

diff --git a/compiler/InterpreterLoops.ml b/compiler/InterpreterLoops.ml
index 11bc7a07..544bface 100644
--- a/compiler/InterpreterLoops.ml
+++ b/compiler/InterpreterLoops.ml
@@ -4106,9 +4106,45 @@ let compute_fp_ctx_symbolic_values (ctx : C.eval_ctx) (fp_ctx : C.eval_ctx) :
       sids_to_values
   in
 
-  (* The value ids should be listed in increasing order *)
+  (* List the input symbolic values in proper order.
+
+     We explore the environment, and order the symbolic values in the order
+     in which they are found - this way, the symbolic values found in a
+     variable [x] which appears before [y] are listed first, for instance.
+  *)
   let input_svalues =
-    List.map snd (V.SymbolicValueId.Map.bindings sids_to_values)
+    let found_sids = ref V.SymbolicValueId.Set.empty in
+    let ordered_sids = ref [] in
+
+    let visitor =
+      object (self : 'self)
+        inherit [_] C.iter_env
+
+        (** We lookup the shared values *)
+        method! visit_SharedBorrow env bid =
+          let open InterpreterBorrowsCore in
+          let v =
+            match snd (lookup_loan ek_all bid fp_ctx) with
+            | Concrete (V.SharedLoan (_, v)) -> v
+            | Abstract (V.ASharedLoan (_, v, _)) -> v
+            | _ -> raise (Failure "Unreachable")
+          in
+          self#visit_typed_value env v
+
+        method! visit_symbolic_value_id _ id =
+          if not (V.SymbolicValueId.Set.mem id !found_sids) then (
+            found_sids := V.SymbolicValueId.Set.add id !found_sids;
+            ordered_sids := id :: !ordered_sids)
+      end
+    in
+
+    (* TODO: why do we have to put a boolean here for the typechecker to be happy?
+       Is it because we use a similar visitor with booleans above?? *)
+    List.iter (visitor#visit_env_elem true) (List.rev fp_ctx.env);
+
+    List.filter_map
+      (fun id -> V.SymbolicValueId.Map.find_opt id sids_to_values)
+      (List.rev !ordered_sids)
   in
 
   log#ldebug
diff --git a/compiler/InterpreterUtils.ml b/compiler/InterpreterUtils.ml
index d60ddfe6..a50bb7ac 100644
--- a/compiler/InterpreterUtils.ml
+++ b/compiler/InterpreterUtils.ml
@@ -143,12 +143,15 @@ let remove_borrow_from_asb (bid : V.BorrowId.id)
     TODO: change the name "abstract"
  *)
 type ('a, 'b) concrete_or_abs = Concrete of 'a | Abstract of 'b
+[@@deriving show]
 
 (** Generic loan content: concrete or abstract *)
 type g_loan_content = (V.loan_content, V.aloan_content) concrete_or_abs
+[@@deriving show]
 
 (** Generic borrow content: concrete or abstract *)
 type g_borrow_content = (V.borrow_content, V.aborrow_content) concrete_or_abs
+[@@deriving show]
 
 type abs_or_var_id =
   | AbsId of V.AbstractionId.id
diff --git a/tests/coq/hashmap/Hashmap_Funs.v b/tests/coq/hashmap/Hashmap_Funs.v
index 1cbff379..9c65fb46 100644
--- a/tests/coq/hashmap/Hashmap_Funs.v
+++ b/tests/coq/hashmap/Hashmap_Funs.v
@@ -332,7 +332,7 @@ Definition hash_map_get_fwd
 
 (** [hashmap::HashMap::{0}::get_mut_in_list] *)
 Fixpoint hash_map_get_mut_in_list_loop_fwd
-  (T : Type) (n : nat) (key : usize) (ls : List_t T) : result T :=
+  (T : Type) (n : nat) (ls : List_t T) (key : usize) : result T :=
   match n with
   | O => Fail_ OutOfFuel
   | S n0 =>
@@ -340,7 +340,7 @@ Fixpoint hash_map_get_mut_in_list_loop_fwd
     | ListCons ckey cvalue tl =>
       if ckey s= key
       then Return cvalue
-      else hash_map_get_mut_in_list_loop_fwd T n0 key tl
+      else hash_map_get_mut_in_list_loop_fwd T n0 tl key
     | ListNil => Fail_ Failure
     end
   end
@@ -349,12 +349,12 @@ Fixpoint hash_map_get_mut_in_list_loop_fwd
 (** [hashmap::HashMap::{0}::get_mut_in_list] *)
 Definition hash_map_get_mut_in_list_fwd
   (T : Type) (n : nat) (ls : List_t T) (key : usize) : result T :=
-  hash_map_get_mut_in_list_loop_fwd T n key ls
+  hash_map_get_mut_in_list_loop_fwd T n ls key
 .
 
 (** [hashmap::HashMap::{0}::get_mut_in_list] *)
 Fixpoint hash_map_get_mut_in_list_loop_back
-  (T : Type) (n : nat) (key : usize) (ls : List_t T) (ret : T) :
+  (T : Type) (n : nat) (ls : List_t T) (key : usize) (ret : T) :
   result (List_t T)
   :=
   match n with
@@ -365,7 +365,7 @@ Fixpoint hash_map_get_mut_in_list_loop_back
       if ckey s= key
       then Return (ListCons ckey ret tl)
       else (
-        l <- hash_map_get_mut_in_list_loop_back T n0 key tl ret;
+        l <- hash_map_get_mut_in_list_loop_back T n0 tl key ret;
         Return (ListCons ckey cvalue l))
     | ListNil => Fail_ Failure
     end
@@ -377,7 +377,7 @@ Definition hash_map_get_mut_in_list_back
   (T : Type) (n : nat) (ls : List_t T) (key : usize) (ret : T) :
   result (List_t T)
   :=
-  hash_map_get_mut_in_list_loop_back T n key ls ret
+  hash_map_get_mut_in_list_loop_back T n ls key ret
 .
 
 (** [hashmap::HashMap::{0}::get_mut] *)
diff --git a/tests/coq/hashmap_on_disk/HashmapMain_Funs.v b/tests/coq/hashmap_on_disk/HashmapMain_Funs.v
index 2a8ab5b5..94a9e6a5 100644
--- a/tests/coq/hashmap_on_disk/HashmapMain_Funs.v
+++ b/tests/coq/hashmap_on_disk/HashmapMain_Funs.v
@@ -358,7 +358,7 @@ Definition hashmap_hash_map_get_fwd
 
 (** [hashmap_main::hashmap::HashMap::{0}::get_mut_in_list] *)
 Fixpoint hashmap_hash_map_get_mut_in_list_loop_fwd
-  (T : Type) (n : nat) (key : usize) (ls : Hashmap_list_t T) : result T :=
+  (T : Type) (n : nat) (ls : Hashmap_list_t T) (key : usize) : result T :=
   match n with
   | O => Fail_ OutOfFuel
   | S n0 =>
@@ -366,7 +366,7 @@ Fixpoint hashmap_hash_map_get_mut_in_list_loop_fwd
     | HashmapListCons ckey cvalue tl =>
       if ckey s= key
       then Return cvalue
-      else hashmap_hash_map_get_mut_in_list_loop_fwd T n0 key tl
+      else hashmap_hash_map_get_mut_in_list_loop_fwd T n0 tl key
     | HashmapListNil => Fail_ Failure
     end
   end
@@ -375,12 +375,12 @@ Fixpoint hashmap_hash_map_get_mut_in_list_loop_fwd
 (** [hashmap_main::hashmap::HashMap::{0}::get_mut_in_list] *)
 Definition hashmap_hash_map_get_mut_in_list_fwd
   (T : Type) (n : nat) (ls : Hashmap_list_t T) (key : usize) : result T :=
-  hashmap_hash_map_get_mut_in_list_loop_fwd T n key ls
+  hashmap_hash_map_get_mut_in_list_loop_fwd T n ls key
 .
 
 (** [hashmap_main::hashmap::HashMap::{0}::get_mut_in_list] *)
 Fixpoint hashmap_hash_map_get_mut_in_list_loop_back
-  (T : Type) (n : nat) (key : usize) (ls : Hashmap_list_t T) (ret : T) :
+  (T : Type) (n : nat) (ls : Hashmap_list_t T) (key : usize) (ret : T) :
   result (Hashmap_list_t T)
   :=
   match n with
@@ -391,7 +391,7 @@ Fixpoint hashmap_hash_map_get_mut_in_list_loop_back
       if ckey s= key
       then Return (HashmapListCons ckey ret tl)
       else (
-        l <- hashmap_hash_map_get_mut_in_list_loop_back T n0 key tl ret;
+        l <- hashmap_hash_map_get_mut_in_list_loop_back T n0 tl key ret;
         Return (HashmapListCons ckey cvalue l))
     | HashmapListNil => Fail_ Failure
     end
@@ -403,7 +403,7 @@ Definition hashmap_hash_map_get_mut_in_list_back
   (T : Type) (n : nat) (ls : Hashmap_list_t T) (key : usize) (ret : T) :
   result (Hashmap_list_t T)
   :=
-  hashmap_hash_map_get_mut_in_list_loop_back T n key ls ret
+  hashmap_hash_map_get_mut_in_list_loop_back T n ls key ret
 .
 
 (** [hashmap_main::hashmap::HashMap::{0}::get_mut] *)
diff --git a/tests/coq/misc/Loops.v b/tests/coq/misc/Loops.v
index 4fbb7da0..9d416bb0 100644
--- a/tests/coq/misc/Loops.v
+++ b/tests/coq/misc/Loops.v
@@ -235,16 +235,16 @@ Definition get_elem_mut_back
 
 (** [loops::get_elem_shared] *)
 Fixpoint get_elem_shared_loop_fwd
-  (n : nat) (x : usize) (slots : vec (List_t usize)) (ls : List_t usize)
+  (n : nat) (slots : vec (List_t usize)) (x : usize) (ls : List_t usize)
   (ls0 : List_t usize) :
   result usize
   :=
   match n with
   | O => Fail_ OutOfFuel
   | S n0 =>
-    match ls0 with
+    match ls with
     | ListCons y tl =>
-      if y s= x then Return y else get_elem_shared_loop_fwd n0 x slots ls tl
+      if y s= x then Return y else get_elem_shared_loop_fwd n0 slots x tl ls0
     | ListNil => Fail_ Failure
     end
   end
@@ -254,7 +254,7 @@ Fixpoint get_elem_shared_loop_fwd
 Definition get_elem_shared_fwd
   (n : nat) (slots : vec (List_t usize)) (x : usize) : result usize :=
   l <- vec_index_fwd (List_t usize) slots (0%usize);
-  get_elem_shared_loop_fwd n x slots l l
+  get_elem_shared_loop_fwd n slots x l l
 .
 
 (** [loops::id_mut] *)
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