Merge pull request #31 from AeneasVerif/son_lean_backend

Improve the Lean backend

3 files changed, 99 insertions, 81 deletions

diff --git a/tests/fstar/hashmap/Hashmap.Funs.fst b/tests/fstar/hashmap/Hashmap.Funs.fst
index 44ad7463..950f1490 100644
--- a/tests/fstar/hashmap/Hashmap.Funs.fst
+++ b/tests/fstar/hashmap/Hashmap.Funs.fst
@@ -7,11 +7,11 @@ include Hashmap.Clauses
 
 #set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
 
-(** [hashmap::hash_key] *)
+(** [hashmap::hash_key]: forward function *)
 let hash_key_fwd (k : usize) : result usize =
   Return k
 
-(** [hashmap::HashMap::{0}::allocate_slots] *)
+(** [hashmap::HashMap::{0}::allocate_slots]: loop 0: forward function *)
 let rec hash_map_allocate_slots_loop_fwd
   (t : Type0) (slots : vec (list_t t)) (n : usize) :
   Tot (result (vec (list_t t)))
@@ -24,12 +24,12 @@ let rec hash_map_allocate_slots_loop_fwd
     hash_map_allocate_slots_loop_fwd t slots0 n0
   else Return slots
 
-(** [hashmap::HashMap::{0}::allocate_slots] *)
+(** [hashmap::HashMap::{0}::allocate_slots]: forward function *)
 let hash_map_allocate_slots_fwd
   (t : Type0) (slots : vec (list_t t)) (n : usize) : result (vec (list_t t)) =
   hash_map_allocate_slots_loop_fwd t slots n
 
-(** [hashmap::HashMap::{0}::new_with_capacity] *)
+(** [hashmap::HashMap::{0}::new_with_capacity]: forward function *)
 let hash_map_new_with_capacity_fwd
   (t : Type0) (capacity : usize) (max_load_dividend : usize)
   (max_load_divisor : usize) :
@@ -47,11 +47,12 @@ let hash_map_new_with_capacity_fwd
       hash_map_slots = slots
     }
 
-(** [hashmap::HashMap::{0}::new] *)
+(** [hashmap::HashMap::{0}::new]: forward function *)
 let hash_map_new_fwd (t : Type0) : result (hash_map_t t) =
   hash_map_new_with_capacity_fwd t 32 4 5
 
-(** [hashmap::HashMap::{0}::clear] *)
+(** [hashmap::HashMap::{0}::clear]: loop 0: merged forward/backward function
+    (there is a single backward function, and the forward function returns ()) *)
 let rec hash_map_clear_loop_fwd_back
   (t : Type0) (slots : vec (list_t t)) (i : usize) :
   Tot (result (vec (list_t t)))
@@ -65,17 +66,18 @@ let rec hash_map_clear_loop_fwd_back
     hash_map_clear_loop_fwd_back t slots0 i1
   else Return slots
 
-(** [hashmap::HashMap::{0}::clear] *)
+(** [hashmap::HashMap::{0}::clear]: merged forward/backward function
+    (there is a single backward function, and the forward function returns ()) *)
 let hash_map_clear_fwd_back
   (t : Type0) (self : hash_map_t t) : result (hash_map_t t) =
   let* v = hash_map_clear_loop_fwd_back t self.hash_map_slots 0 in
   Return { self with hash_map_num_entries = 0; hash_map_slots = v }
 
-(** [hashmap::HashMap::{0}::len] *)
+(** [hashmap::HashMap::{0}::len]: forward function *)
 let hash_map_len_fwd (t : Type0) (self : hash_map_t t) : result usize =
   Return self.hash_map_num_entries
 
-(** [hashmap::HashMap::{0}::insert_in_list] *)
+(** [hashmap::HashMap::{0}::insert_in_list]: loop 0: forward function *)
 let rec hash_map_insert_in_list_loop_fwd
   (t : Type0) (key : usize) (value : t) (ls : list_t t) :
   Tot (result bool)
@@ -89,12 +91,12 @@ let rec hash_map_insert_in_list_loop_fwd
   | ListNil -> Return true
   end
 
-(** [hashmap::HashMap::{0}::insert_in_list] *)
+(** [hashmap::HashMap::{0}::insert_in_list]: forward function *)
 let hash_map_insert_in_list_fwd
   (t : Type0) (key : usize) (value : t) (ls : list_t t) : result bool =
   hash_map_insert_in_list_loop_fwd t key value ls
 
-(** [hashmap::HashMap::{0}::insert_in_list] *)
+(** [hashmap::HashMap::{0}::insert_in_list]: loop 0: backward function 0 *)
 let rec hash_map_insert_in_list_loop_back
   (t : Type0) (key : usize) (value : t) (ls : list_t t) :
   Tot (result (list_t t))
@@ -110,12 +112,13 @@ let rec hash_map_insert_in_list_loop_back
   | ListNil -> let l = ListNil in Return (ListCons key value l)
   end
 
-(** [hashmap::HashMap::{0}::insert_in_list] *)
+(** [hashmap::HashMap::{0}::insert_in_list]: backward function 0 *)
 let hash_map_insert_in_list_back
   (t : Type0) (key : usize) (value : t) (ls : list_t t) : result (list_t t) =
   hash_map_insert_in_list_loop_back t key value ls
 
-(** [hashmap::HashMap::{0}::insert_no_resize] *)
+(** [hashmap::HashMap::{0}::insert_no_resize]: merged forward/backward function
+    (there is a single backward function, and the forward function returns ()) *)
 let hash_map_insert_no_resize_fwd_back
   (t : Type0) (self : hash_map_t t) (key : usize) (value : t) :
   result (hash_map_t t)
@@ -140,7 +143,8 @@ let hash_map_insert_no_resize_fwd_back
 let core_num_u32_max_body : result u32 = Return 4294967295
 let core_num_u32_max_c : u32 = eval_global core_num_u32_max_body
 
-(** [hashmap::HashMap::{0}::move_elements_from_list] *)
+(** [hashmap::HashMap::{0}::move_elements_from_list]: loop 0: merged forward/backward function
+    (there is a single backward function, and the forward function returns ()) *)
 let rec hash_map_move_elements_from_list_loop_fwd_back
   (t : Type0) (ntable : hash_map_t t) (ls : list_t t) :
   Tot (result (hash_map_t t))
@@ -153,12 +157,14 @@ let rec hash_map_move_elements_from_list_loop_fwd_back
   | ListNil -> Return ntable
   end
 
-(** [hashmap::HashMap::{0}::move_elements_from_list] *)
+(** [hashmap::HashMap::{0}::move_elements_from_list]: merged forward/backward function
+    (there is a single backward function, and the forward function returns ()) *)
 let hash_map_move_elements_from_list_fwd_back
   (t : Type0) (ntable : hash_map_t t) (ls : list_t t) : result (hash_map_t t) =
   hash_map_move_elements_from_list_loop_fwd_back t ntable ls
 
-(** [hashmap::HashMap::{0}::move_elements] *)
+(** [hashmap::HashMap::{0}::move_elements]: loop 0: merged forward/backward function
+    (there is a single backward function, and the forward function returns ()) *)
 let rec hash_map_move_elements_loop_fwd_back
   (t : Type0) (ntable : hash_map_t t) (slots : vec (list_t t)) (i : usize) :
   Tot (result ((hash_map_t t) & (vec (list_t t))))
@@ -176,14 +182,16 @@ let rec hash_map_move_elements_loop_fwd_back
     hash_map_move_elements_loop_fwd_back t ntable0 slots0 i1
   else Return (ntable, slots)
 
-(** [hashmap::HashMap::{0}::move_elements] *)
+(** [hashmap::HashMap::{0}::move_elements]: merged forward/backward function
+    (there is a single backward function, and the forward function returns ()) *)
 let hash_map_move_elements_fwd_back
   (t : Type0) (ntable : hash_map_t t) (slots : vec (list_t t)) (i : usize) :
   result ((hash_map_t t) & (vec (list_t t)))
   =
   hash_map_move_elements_loop_fwd_back t ntable slots i
 
-(** [hashmap::HashMap::{0}::try_resize] *)
+(** [hashmap::HashMap::{0}::try_resize]: merged forward/backward function
+    (there is a single backward function, and the forward function returns ()) *)
 let hash_map_try_resize_fwd_back
   (t : Type0) (self : hash_map_t t) : result (hash_map_t t) =
   let* max_usize = scalar_cast U32 Usize core_num_u32_max_c in
@@ -206,7 +214,8 @@ let hash_map_try_resize_fwd_back
       }
   else Return { self with hash_map_max_load_factor = (i, i0) }
 
-(** [hashmap::HashMap::{0}::insert] *)
+(** [hashmap::HashMap::{0}::insert]: merged forward/backward function
+    (there is a single backward function, and the forward function returns ()) *)
 let hash_map_insert_fwd_back
   (t : Type0) (self : hash_map_t t) (key : usize) (value : t) :
   result (hash_map_t t)
@@ -217,7 +226,7 @@ let hash_map_insert_fwd_back
   then hash_map_try_resize_fwd_back t self0
   else Return self0
 
-(** [hashmap::HashMap::{0}::contains_key_in_list] *)
+(** [hashmap::HashMap::{0}::contains_key_in_list]: loop 0: forward function *)
 let rec hash_map_contains_key_in_list_loop_fwd
   (t : Type0) (key : usize) (ls : list_t t) :
   Tot (result bool)
@@ -231,12 +240,12 @@ let rec hash_map_contains_key_in_list_loop_fwd
   | ListNil -> Return false
   end
 
-(** [hashmap::HashMap::{0}::contains_key_in_list] *)
+(** [hashmap::HashMap::{0}::contains_key_in_list]: forward function *)
 let hash_map_contains_key_in_list_fwd
   (t : Type0) (key : usize) (ls : list_t t) : result bool =
   hash_map_contains_key_in_list_loop_fwd t key ls
 
-(** [hashmap::HashMap::{0}::contains_key] *)
+(** [hashmap::HashMap::{0}::contains_key]: forward function *)
 let hash_map_contains_key_fwd
   (t : Type0) (self : hash_map_t t) (key : usize) : result bool =
   let* hash = hash_key_fwd key in
@@ -245,7 +254,7 @@ let hash_map_contains_key_fwd
   let* l = vec_index_fwd (list_t t) self.hash_map_slots hash_mod in
   hash_map_contains_key_in_list_fwd t key l
 
-(** [hashmap::HashMap::{0}::get_in_list] *)
+(** [hashmap::HashMap::{0}::get_in_list]: loop 0: forward function *)
 let rec hash_map_get_in_list_loop_fwd
   (t : Type0) (key : usize) (ls : list_t t) :
   Tot (result t) (decreases (hash_map_get_in_list_loop_decreases t key ls))
@@ -258,12 +267,12 @@ let rec hash_map_get_in_list_loop_fwd
   | ListNil -> Fail Failure
   end
 
-(** [hashmap::HashMap::{0}::get_in_list] *)
+(** [hashmap::HashMap::{0}::get_in_list]: forward function *)
 let hash_map_get_in_list_fwd
   (t : Type0) (key : usize) (ls : list_t t) : result t =
   hash_map_get_in_list_loop_fwd t key ls
 
-(** [hashmap::HashMap::{0}::get] *)
+(** [hashmap::HashMap::{0}::get]: forward function *)
 let hash_map_get_fwd
   (t : Type0) (self : hash_map_t t) (key : usize) : result t =
   let* hash = hash_key_fwd key in
@@ -272,7 +281,7 @@ let hash_map_get_fwd
   let* l = vec_index_fwd (list_t t) self.hash_map_slots hash_mod in
   hash_map_get_in_list_fwd t key l
 
-(** [hashmap::HashMap::{0}::get_mut_in_list] *)
+(** [hashmap::HashMap::{0}::get_mut_in_list]: loop 0: forward function *)
 let rec hash_map_get_mut_in_list_loop_fwd
   (t : Type0) (ls : list_t t) (key : usize) :
   Tot (result t) (decreases (hash_map_get_mut_in_list_loop_decreases t ls key))
@@ -285,12 +294,12 @@ let rec hash_map_get_mut_in_list_loop_fwd
   | ListNil -> Fail Failure
   end
 
-(** [hashmap::HashMap::{0}::get_mut_in_list] *)
+(** [hashmap::HashMap::{0}::get_mut_in_list]: forward function *)
 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 ls key
 
-(** [hashmap::HashMap::{0}::get_mut_in_list] *)
+(** [hashmap::HashMap::{0}::get_mut_in_list]: loop 0: backward function 0 *)
 let rec hash_map_get_mut_in_list_loop_back
   (t : Type0) (ls : list_t t) (key : usize) (ret : t) :
   Tot (result (list_t t))
@@ -306,12 +315,12 @@ let rec hash_map_get_mut_in_list_loop_back
   | ListNil -> Fail Failure
   end
 
-(** [hashmap::HashMap::{0}::get_mut_in_list] *)
+(** [hashmap::HashMap::{0}::get_mut_in_list]: backward function 0 *)
 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 ls key ret
 
-(** [hashmap::HashMap::{0}::get_mut] *)
+(** [hashmap::HashMap::{0}::get_mut]: forward function *)
 let hash_map_get_mut_fwd
   (t : Type0) (self : hash_map_t t) (key : usize) : result t =
   let* hash = hash_key_fwd key in
@@ -320,7 +329,7 @@ let hash_map_get_mut_fwd
   let* l = vec_index_mut_fwd (list_t t) self.hash_map_slots hash_mod in
   hash_map_get_mut_in_list_fwd t l key
 
-(** [hashmap::HashMap::{0}::get_mut] *)
+(** [hashmap::HashMap::{0}::get_mut]: backward function 0 *)
 let hash_map_get_mut_back
   (t : Type0) (self : hash_map_t t) (key : usize) (ret : t) :
   result (hash_map_t t)
@@ -333,7 +342,7 @@ let hash_map_get_mut_back
   let* v = vec_index_mut_back (list_t t) self.hash_map_slots hash_mod l0 in
   Return { self with hash_map_slots = v }
 
-(** [hashmap::HashMap::{0}::remove_from_list] *)
+(** [hashmap::HashMap::{0}::remove_from_list]: loop 0: forward function *)
 let rec hash_map_remove_from_list_loop_fwd
   (t : Type0) (key : usize) (ls : list_t t) :
   Tot (result (option t))
@@ -352,12 +361,12 @@ let rec hash_map_remove_from_list_loop_fwd
   | ListNil -> Return None
   end
 
-(** [hashmap::HashMap::{0}::remove_from_list] *)
+(** [hashmap::HashMap::{0}::remove_from_list]: forward function *)
 let hash_map_remove_from_list_fwd
   (t : Type0) (key : usize) (ls : list_t t) : result (option t) =
   hash_map_remove_from_list_loop_fwd t key ls
 
-(** [hashmap::HashMap::{0}::remove_from_list] *)
+(** [hashmap::HashMap::{0}::remove_from_list]: loop 0: backward function 1 *)
 let rec hash_map_remove_from_list_loop_back
   (t : Type0) (key : usize) (ls : list_t t) :
   Tot (result (list_t t))
@@ -378,12 +387,12 @@ let rec hash_map_remove_from_list_loop_back
   | ListNil -> Return ListNil
   end
 
-(** [hashmap::HashMap::{0}::remove_from_list] *)
+(** [hashmap::HashMap::{0}::remove_from_list]: backward function 1 *)
 let hash_map_remove_from_list_back
   (t : Type0) (key : usize) (ls : list_t t) : result (list_t t) =
   hash_map_remove_from_list_loop_back t key ls
 
-(** [hashmap::HashMap::{0}::remove] *)
+(** [hashmap::HashMap::{0}::remove]: forward function *)
 let hash_map_remove_fwd
   (t : Type0) (self : hash_map_t t) (key : usize) : result (option t) =
   let* hash = hash_key_fwd key in
@@ -397,7 +406,7 @@ let hash_map_remove_fwd
     let* _ = usize_sub self.hash_map_num_entries 1 in Return (Some x0)
   end
 
-(** [hashmap::HashMap::{0}::remove] *)
+(** [hashmap::HashMap::{0}::remove]: backward function 0 *)
 let hash_map_remove_back
   (t : Type0) (self : hash_map_t t) (key : usize) : result (hash_map_t t) =
   let* hash = hash_key_fwd key in
@@ -417,7 +426,7 @@ let hash_map_remove_back
     Return { self with hash_map_num_entries = i0; hash_map_slots = v }
   end
 
-(** [hashmap::test1] *)
+(** [hashmap::test1]: forward function *)
 let test1_fwd : result unit =
   let* hm = hash_map_new_fwd u64 in
   let* hm0 = hash_map_insert_fwd_back u64 hm 0 42 in
diff --git a/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst b/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst
index e8cd54c1..f6d9c8cf 100644
--- a/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst
+++ b/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst
@@ -8,11 +8,11 @@ include HashmapMain.Clauses
 
 #set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
 
-(** [hashmap_main::hashmap::hash_key] *)
+(** [hashmap_main::hashmap::hash_key]: forward function *)
 let hashmap_hash_key_fwd (k : usize) : result usize =
   Return k
 
-(** [hashmap_main::hashmap::HashMap::{0}::allocate_slots] *)
+(** [hashmap_main::hashmap::HashMap::{0}::allocate_slots]: loop 0: forward function *)
 let rec hashmap_hash_map_allocate_slots_loop_fwd
   (t : Type0) (slots : vec (hashmap_list_t t)) (n : usize) :
   Tot (result (vec (hashmap_list_t t)))
@@ -25,14 +25,14 @@ let rec hashmap_hash_map_allocate_slots_loop_fwd
     hashmap_hash_map_allocate_slots_loop_fwd t slots0 n0
   else Return slots
 
-(** [hashmap_main::hashmap::HashMap::{0}::allocate_slots] *)
+(** [hashmap_main::hashmap::HashMap::{0}::allocate_slots]: forward function *)
 let hashmap_hash_map_allocate_slots_fwd
   (t : Type0) (slots : vec (hashmap_list_t t)) (n : usize) :
   result (vec (hashmap_list_t t))
   =
   hashmap_hash_map_allocate_slots_loop_fwd t slots n
 
-(** [hashmap_main::hashmap::HashMap::{0}::new_with_capacity] *)
+(** [hashmap_main::hashmap::HashMap::{0}::new_with_capacity]: forward function *)
 let hashmap_hash_map_new_with_capacity_fwd
   (t : Type0) (capacity : usize) (max_load_dividend : usize)
   (max_load_divisor : usize) :
@@ -50,11 +50,12 @@ let hashmap_hash_map_new_with_capacity_fwd
       hashmap_hash_map_slots = slots
     }
 
-(** [hashmap_main::hashmap::HashMap::{0}::new] *)
+(** [hashmap_main::hashmap::HashMap::{0}::new]: forward function *)
 let hashmap_hash_map_new_fwd (t : Type0) : result (hashmap_hash_map_t t) =
   hashmap_hash_map_new_with_capacity_fwd t 32 4 5
 
-(** [hashmap_main::hashmap::HashMap::{0}::clear] *)
+(** [hashmap_main::hashmap::HashMap::{0}::clear]: loop 0: merged forward/backward function
+    (there is a single backward function, and the forward function returns ()) *)
 let rec hashmap_hash_map_clear_loop_fwd_back
   (t : Type0) (slots : vec (hashmap_list_t t)) (i : usize) :
   Tot (result (vec (hashmap_list_t t)))
@@ -69,7 +70,8 @@ let rec hashmap_hash_map_clear_loop_fwd_back
     hashmap_hash_map_clear_loop_fwd_back t slots0 i1
   else Return slots
 
-(** [hashmap_main::hashmap::HashMap::{0}::clear] *)
+(** [hashmap_main::hashmap::HashMap::{0}::clear]: merged forward/backward function
+    (there is a single backward function, and the forward function returns ()) *)
 let hashmap_hash_map_clear_fwd_back
   (t : Type0) (self : hashmap_hash_map_t t) : result (hashmap_hash_map_t t) =
   let* v = hashmap_hash_map_clear_loop_fwd_back t self.hashmap_hash_map_slots 0
@@ -77,12 +79,12 @@ let hashmap_hash_map_clear_fwd_back
   Return
     { self with hashmap_hash_map_num_entries = 0; hashmap_hash_map_slots = v }
 
-(** [hashmap_main::hashmap::HashMap::{0}::len] *)
+(** [hashmap_main::hashmap::HashMap::{0}::len]: forward function *)
 let hashmap_hash_map_len_fwd
   (t : Type0) (self : hashmap_hash_map_t t) : result usize =
   Return self.hashmap_hash_map_num_entries
 
-(** [hashmap_main::hashmap::HashMap::{0}::insert_in_list] *)
+(** [hashmap_main::hashmap::HashMap::{0}::insert_in_list]: loop 0: forward function *)
 let rec hashmap_hash_map_insert_in_list_loop_fwd
   (t : Type0) (key : usize) (value : t) (ls : hashmap_list_t t) :
   Tot (result bool)
@@ -96,12 +98,12 @@ let rec hashmap_hash_map_insert_in_list_loop_fwd
   | HashmapListNil -> Return true
   end
 
-(** [hashmap_main::hashmap::HashMap::{0}::insert_in_list] *)
+(** [hashmap_main::hashmap::HashMap::{0}::insert_in_list]: forward function *)
 let hashmap_hash_map_insert_in_list_fwd
   (t : Type0) (key : usize) (value : t) (ls : hashmap_list_t t) : result bool =
   hashmap_hash_map_insert_in_list_loop_fwd t key value ls
 
-(** [hashmap_main::hashmap::HashMap::{0}::insert_in_list] *)
+(** [hashmap_main::hashmap::HashMap::{0}::insert_in_list]: loop 0: backward function 0 *)
 let rec hashmap_hash_map_insert_in_list_loop_back
   (t : Type0) (key : usize) (value : t) (ls : hashmap_list_t t) :
   Tot (result (hashmap_list_t t))
@@ -118,14 +120,15 @@ let rec hashmap_hash_map_insert_in_list_loop_back
     let l = HashmapListNil in Return (HashmapListCons key value l)
   end
 
-(** [hashmap_main::hashmap::HashMap::{0}::insert_in_list] *)
+(** [hashmap_main::hashmap::HashMap::{0}::insert_in_list]: backward function 0 *)
 let hashmap_hash_map_insert_in_list_back
   (t : Type0) (key : usize) (value : t) (ls : hashmap_list_t t) :
   result (hashmap_list_t t)
   =
   hashmap_hash_map_insert_in_list_loop_back t key value ls
 
-(** [hashmap_main::hashmap::HashMap::{0}::insert_no_resize] *)
+(** [hashmap_main::hashmap::HashMap::{0}::insert_no_resize]: merged forward/backward function
+    (there is a single backward function, and the forward function returns ()) *)
 let hashmap_hash_map_insert_no_resize_fwd_back
   (t : Type0) (self : hashmap_hash_map_t t) (key : usize) (value : t) :
   result (hashmap_hash_map_t t)
@@ -158,7 +161,8 @@ let hashmap_hash_map_insert_no_resize_fwd_back
 let core_num_u32_max_body : result u32 = Return 4294967295
 let core_num_u32_max_c : u32 = eval_global core_num_u32_max_body
 
-(** [hashmap_main::hashmap::HashMap::{0}::move_elements_from_list] *)
+(** [hashmap_main::hashmap::HashMap::{0}::move_elements_from_list]: loop 0: merged forward/backward function
+    (there is a single backward function, and the forward function returns ()) *)
 let rec hashmap_hash_map_move_elements_from_list_loop_fwd_back
   (t : Type0) (ntable : hashmap_hash_map_t t) (ls : hashmap_list_t t) :
   Tot (result (hashmap_hash_map_t t))
@@ -172,14 +176,16 @@ let rec hashmap_hash_map_move_elements_from_list_loop_fwd_back
   | HashmapListNil -> Return ntable
   end
 
-(** [hashmap_main::hashmap::HashMap::{0}::move_elements_from_list] *)
+(** [hashmap_main::hashmap::HashMap::{0}::move_elements_from_list]: merged forward/backward function
+    (there is a single backward function, and the forward function returns ()) *)
 let hashmap_hash_map_move_elements_from_list_fwd_back
   (t : Type0) (ntable : hashmap_hash_map_t t) (ls : hashmap_list_t t) :
   result (hashmap_hash_map_t t)
   =
   hashmap_hash_map_move_elements_from_list_loop_fwd_back t ntable ls
 
-(** [hashmap_main::hashmap::HashMap::{0}::move_elements] *)
+(** [hashmap_main::hashmap::HashMap::{0}::move_elements]: loop 0: merged forward/backward function
+    (there is a single backward function, and the forward function returns ()) *)
 let rec hashmap_hash_map_move_elements_loop_fwd_back
   (t : Type0) (ntable : hashmap_hash_map_t t) (slots : vec (hashmap_list_t t))
   (i : usize) :
@@ -199,7 +205,8 @@ let rec hashmap_hash_map_move_elements_loop_fwd_back
     hashmap_hash_map_move_elements_loop_fwd_back t ntable0 slots0 i1
   else Return (ntable, slots)
 
-(** [hashmap_main::hashmap::HashMap::{0}::move_elements] *)
+(** [hashmap_main::hashmap::HashMap::{0}::move_elements]: merged forward/backward function
+    (there is a single backward function, and the forward function returns ()) *)
 let hashmap_hash_map_move_elements_fwd_back
   (t : Type0) (ntable : hashmap_hash_map_t t) (slots : vec (hashmap_list_t t))
   (i : usize) :
@@ -207,7 +214,8 @@ let hashmap_hash_map_move_elements_fwd_back
   =
   hashmap_hash_map_move_elements_loop_fwd_back t ntable slots i
 
-(** [hashmap_main::hashmap::HashMap::{0}::try_resize] *)
+(** [hashmap_main::hashmap::HashMap::{0}::try_resize]: merged forward/backward function
+    (there is a single backward function, and the forward function returns ()) *)
 let hashmap_hash_map_try_resize_fwd_back
   (t : Type0) (self : hashmap_hash_map_t t) : result (hashmap_hash_map_t t) =
   let* max_usize = scalar_cast U32 Usize core_num_u32_max_c in
@@ -231,7 +239,8 @@ let hashmap_hash_map_try_resize_fwd_back
       }
   else Return { self with hashmap_hash_map_max_load_factor = (i, i0) }
 
-(** [hashmap_main::hashmap::HashMap::{0}::insert] *)
+(** [hashmap_main::hashmap::HashMap::{0}::insert]: merged forward/backward function
+    (there is a single backward function, and the forward function returns ()) *)
 let hashmap_hash_map_insert_fwd_back
   (t : Type0) (self : hashmap_hash_map_t t) (key : usize) (value : t) :
   result (hashmap_hash_map_t t)
@@ -242,7 +251,7 @@ let hashmap_hash_map_insert_fwd_back
   then hashmap_hash_map_try_resize_fwd_back t self0
   else Return self0
 
-(** [hashmap_main::hashmap::HashMap::{0}::contains_key_in_list] *)
+(** [hashmap_main::hashmap::HashMap::{0}::contains_key_in_list]: loop 0: forward function *)
 let rec hashmap_hash_map_contains_key_in_list_loop_fwd
   (t : Type0) (key : usize) (ls : hashmap_list_t t) :
   Tot (result bool)
@@ -256,12 +265,12 @@ let rec hashmap_hash_map_contains_key_in_list_loop_fwd
   | HashmapListNil -> Return false
   end
 
-(** [hashmap_main::hashmap::HashMap::{0}::contains_key_in_list] *)
+(** [hashmap_main::hashmap::HashMap::{0}::contains_key_in_list]: forward function *)
 let hashmap_hash_map_contains_key_in_list_fwd
   (t : Type0) (key : usize) (ls : hashmap_list_t t) : result bool =
   hashmap_hash_map_contains_key_in_list_loop_fwd t key ls
 
-(** [hashmap_main::hashmap::HashMap::{0}::contains_key] *)
+(** [hashmap_main::hashmap::HashMap::{0}::contains_key]: forward function *)
 let hashmap_hash_map_contains_key_fwd
   (t : Type0) (self : hashmap_hash_map_t t) (key : usize) : result bool =
   let* hash = hashmap_hash_key_fwd key in
@@ -271,7 +280,7 @@ let hashmap_hash_map_contains_key_fwd
     vec_index_fwd (hashmap_list_t t) self.hashmap_hash_map_slots hash_mod in
   hashmap_hash_map_contains_key_in_list_fwd t key l
 
-(** [hashmap_main::hashmap::HashMap::{0}::get_in_list] *)
+(** [hashmap_main::hashmap::HashMap::{0}::get_in_list]: loop 0: forward function *)
 let rec hashmap_hash_map_get_in_list_loop_fwd
   (t : Type0) (key : usize) (ls : hashmap_list_t t) :
   Tot (result t)
@@ -285,12 +294,12 @@ let rec hashmap_hash_map_get_in_list_loop_fwd
   | HashmapListNil -> Fail Failure
   end
 
-(** [hashmap_main::hashmap::HashMap::{0}::get_in_list] *)
+(** [hashmap_main::hashmap::HashMap::{0}::get_in_list]: forward function *)
 let hashmap_hash_map_get_in_list_fwd
   (t : Type0) (key : usize) (ls : hashmap_list_t t) : result t =
   hashmap_hash_map_get_in_list_loop_fwd t key ls
 
-(** [hashmap_main::hashmap::HashMap::{0}::get] *)
+(** [hashmap_main::hashmap::HashMap::{0}::get]: forward function *)
 let hashmap_hash_map_get_fwd
   (t : Type0) (self : hashmap_hash_map_t t) (key : usize) : result t =
   let* hash = hashmap_hash_key_fwd key in
@@ -300,7 +309,7 @@ let hashmap_hash_map_get_fwd
     vec_index_fwd (hashmap_list_t t) self.hashmap_hash_map_slots hash_mod in
   hashmap_hash_map_get_in_list_fwd t key l
 
-(** [hashmap_main::hashmap::HashMap::{0}::get_mut_in_list] *)
+(** [hashmap_main::hashmap::HashMap::{0}::get_mut_in_list]: loop 0: forward function *)
 let rec hashmap_hash_map_get_mut_in_list_loop_fwd
   (t : Type0) (ls : hashmap_list_t t) (key : usize) :
   Tot (result t)
@@ -314,12 +323,12 @@ let rec hashmap_hash_map_get_mut_in_list_loop_fwd
   | HashmapListNil -> Fail Failure
   end
 
-(** [hashmap_main::hashmap::HashMap::{0}::get_mut_in_list] *)
+(** [hashmap_main::hashmap::HashMap::{0}::get_mut_in_list]: forward function *)
 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 ls key
 
-(** [hashmap_main::hashmap::HashMap::{0}::get_mut_in_list] *)
+(** [hashmap_main::hashmap::HashMap::{0}::get_mut_in_list]: loop 0: backward function 0 *)
 let rec hashmap_hash_map_get_mut_in_list_loop_back
   (t : Type0) (ls : hashmap_list_t t) (key : usize) (ret : t) :
   Tot (result (hashmap_list_t t))
@@ -335,14 +344,14 @@ let rec hashmap_hash_map_get_mut_in_list_loop_back
   | HashmapListNil -> Fail Failure
   end
 
-(** [hashmap_main::hashmap::HashMap::{0}::get_mut_in_list] *)
+(** [hashmap_main::hashmap::HashMap::{0}::get_mut_in_list]: backward function 0 *)
 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 ls key ret
 
-(** [hashmap_main::hashmap::HashMap::{0}::get_mut] *)
+(** [hashmap_main::hashmap::HashMap::{0}::get_mut]: forward function *)
 let hashmap_hash_map_get_mut_fwd
   (t : Type0) (self : hashmap_hash_map_t t) (key : usize) : result t =
   let* hash = hashmap_hash_key_fwd key in
@@ -353,7 +362,7 @@ let hashmap_hash_map_get_mut_fwd
     in
   hashmap_hash_map_get_mut_in_list_fwd t l key
 
-(** [hashmap_main::hashmap::HashMap::{0}::get_mut] *)
+(** [hashmap_main::hashmap::HashMap::{0}::get_mut]: backward function 0 *)
 let hashmap_hash_map_get_mut_back
   (t : Type0) (self : hashmap_hash_map_t t) (key : usize) (ret : t) :
   result (hashmap_hash_map_t t)
@@ -370,7 +379,7 @@ let hashmap_hash_map_get_mut_back
       l0 in
   Return { self with hashmap_hash_map_slots = v }
 
-(** [hashmap_main::hashmap::HashMap::{0}::remove_from_list] *)
+(** [hashmap_main::hashmap::HashMap::{0}::remove_from_list]: loop 0: forward function *)
 let rec hashmap_hash_map_remove_from_list_loop_fwd
   (t : Type0) (key : usize) (ls : hashmap_list_t t) :
   Tot (result (option t))
@@ -391,12 +400,12 @@ let rec hashmap_hash_map_remove_from_list_loop_fwd
   | HashmapListNil -> Return None
   end
 
-(** [hashmap_main::hashmap::HashMap::{0}::remove_from_list] *)
+(** [hashmap_main::hashmap::HashMap::{0}::remove_from_list]: forward function *)
 let hashmap_hash_map_remove_from_list_fwd
   (t : Type0) (key : usize) (ls : hashmap_list_t t) : result (option t) =
   hashmap_hash_map_remove_from_list_loop_fwd t key ls
 
-(** [hashmap_main::hashmap::HashMap::{0}::remove_from_list] *)
+(** [hashmap_main::hashmap::HashMap::{0}::remove_from_list]: loop 0: backward function 1 *)
 let rec hashmap_hash_map_remove_from_list_loop_back
   (t : Type0) (key : usize) (ls : hashmap_list_t t) :
   Tot (result (hashmap_list_t t))
@@ -419,14 +428,14 @@ let rec hashmap_hash_map_remove_from_list_loop_back
   | HashmapListNil -> Return HashmapListNil
   end
 
-(** [hashmap_main::hashmap::HashMap::{0}::remove_from_list] *)
+(** [hashmap_main::hashmap::HashMap::{0}::remove_from_list]: backward function 1 *)
 let hashmap_hash_map_remove_from_list_back
   (t : Type0) (key : usize) (ls : hashmap_list_t t) :
   result (hashmap_list_t t)
   =
   hashmap_hash_map_remove_from_list_loop_back t key ls
 
-(** [hashmap_main::hashmap::HashMap::{0}::remove] *)
+(** [hashmap_main::hashmap::HashMap::{0}::remove]: forward function *)
 let hashmap_hash_map_remove_fwd
   (t : Type0) (self : hashmap_hash_map_t t) (key : usize) : result (option t) =
   let* hash = hashmap_hash_key_fwd key in
@@ -442,7 +451,7 @@ let hashmap_hash_map_remove_fwd
     let* _ = usize_sub self.hashmap_hash_map_num_entries 1 in Return (Some x0)
   end
 
-(** [hashmap_main::hashmap::HashMap::{0}::remove] *)
+(** [hashmap_main::hashmap::HashMap::{0}::remove]: backward function 0 *)
 let hashmap_hash_map_remove_back
   (t : Type0) (self : hashmap_hash_map_t t) (key : usize) :
   result (hashmap_hash_map_t t)
@@ -472,7 +481,7 @@ let hashmap_hash_map_remove_back
       }
   end
 
-(** [hashmap_main::hashmap::test1] *)
+(** [hashmap_main::hashmap::test1]: forward function *)
 let hashmap_test1_fwd : result unit =
   let* hm = hashmap_hash_map_new_fwd u64 in
   let* hm0 = hashmap_hash_map_insert_fwd_back u64 hm 0 42 in
@@ -511,7 +520,7 @@ let hashmap_test1_fwd : result unit =
 (** Unit test for [hashmap_main::hashmap::test1] *)
 let _ = assert_norm (hashmap_test1_fwd = Return ())
 
-(** [hashmap_main::insert_on_disk] *)
+(** [hashmap_main::insert_on_disk]: forward function *)
 let insert_on_disk_fwd
   (key : usize) (value : u64) (st : state) : result (state & unit) =
   let* (st0, hm) = hashmap_utils_deserialize_fwd st in
@@ -519,7 +528,7 @@ let insert_on_disk_fwd
   let* (st1, _) = hashmap_utils_serialize_fwd hm0 st0 in
   Return (st1, ())
 
-(** [hashmap_main::main] *)
+(** [hashmap_main::main]: forward function *)
 let main_fwd : result unit =
   Return ()
 
diff --git a/tests/fstar/hashmap_on_disk/HashmapMain.Opaque.fsti b/tests/fstar/hashmap_on_disk/HashmapMain.Opaque.fsti
index 6e54ea10..78a6c3ba 100644
--- a/tests/fstar/hashmap_on_disk/HashmapMain.Opaque.fsti
+++ b/tests/fstar/hashmap_on_disk/HashmapMain.Opaque.fsti
@@ -1,16 +1,16 @@
 (** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
-(** [hashmap_main]: opaque function definitions *)
+(** [hashmap_main]: external function declarations *)
 module HashmapMain.Opaque
 open Primitives
 include HashmapMain.Types
 
 #set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
 
-(** [hashmap_main::hashmap_utils::deserialize] *)
+(** [hashmap_main::hashmap_utils::deserialize]: forward function *)
 val hashmap_utils_deserialize_fwd
   : state -> result (state & (hashmap_hash_map_t u64))
 
-(** [hashmap_main::hashmap_utils::serialize] *)
+(** [hashmap_main::hashmap_utils::serialize]: forward function *)
 val hashmap_utils_serialize_fwd
   : hashmap_hash_map_t u64 -> state -> result (state & unit)