Regenerate the files

8 files changed, 350 insertions, 175 deletions

diff --git a/tests/fstar/betree/BetreeMain.Clauses.Template.fst b/tests/fstar/betree/BetreeMain.Clauses.Template.fst
index 4d16d8d3..4ae29302 100644
--- a/tests/fstar/betree/BetreeMain.Clauses.Template.fst
+++ b/tests/fstar/betree/BetreeMain.Clauses.Template.fst
@@ -6,94 +6,109 @@ open BetreeMain.Types
 
 #set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
 
-(** [betree_main::betree::{betree_main::betree::List<T>#1}::len]: decreases clause *)
+(** [betree_main::betree::{betree_main::betree::List<T>#1}::len]: decreases clause
+    Source: 'src/betree.rs', lines 276:4-276:24 *)
 unfold
 let betree_List_len_decreases (t : Type0) (self : betree_List_t t) : nat =
   admit ()
 
-(** [betree_main::betree::{betree_main::betree::List<T>#1}::split_at]: decreases clause *)
+(** [betree_main::betree::{betree_main::betree::List<T>#1}::split_at]: decreases clause
+    Source: 'src/betree.rs', lines 284:4-284:51 *)
 unfold
 let betree_List_split_at_decreases (t : Type0) (self : betree_List_t t)
   (n : u64) : nat =
   admit ()
 
-(** [betree_main::betree::{betree_main::betree::List<(u64, T)>#2}::partition_at_pivot]: decreases clause *)
+(** [betree_main::betree::{betree_main::betree::List<(u64, T)>#2}::partition_at_pivot]: decreases clause
+    Source: 'src/betree.rs', lines 339:4-339:73 *)
 unfold
 let betree_ListTupleU64T_partition_at_pivot_decreases (t : Type0)
   (self : betree_List_t (u64 & t)) (pivot : u64) : nat =
   admit ()
 
-(** [betree_main::betree::{betree_main::betree::Node#5}::lookup_first_message_for_key]: decreases clause *)
+(** [betree_main::betree::{betree_main::betree::Node#5}::lookup_first_message_for_key]: decreases clause
+    Source: 'src/betree.rs', lines 789:4-792:34 *)
 unfold
 let betree_Node_lookup_first_message_for_key_decreases (key : u64)
   (msgs : betree_List_t (u64 & betree_Message_t)) : nat =
   admit ()
 
-(** [betree_main::betree::{betree_main::betree::Node#5}::apply_upserts]: decreases clause *)
+(** [betree_main::betree::{betree_main::betree::Node#5}::apply_upserts]: decreases clause
+    Source: 'src/betree.rs', lines 819:4-819:90 *)
 unfold
 let betree_Node_apply_upserts_decreases
   (msgs : betree_List_t (u64 & betree_Message_t)) (prev : option u64)
   (key : u64) (st : state) : nat =
   admit ()
 
-(** [betree_main::betree::{betree_main::betree::Node#5}::lookup_in_bindings]: decreases clause *)
+(** [betree_main::betree::{betree_main::betree::Node#5}::lookup_in_bindings]: decreases clause
+    Source: 'src/betree.rs', lines 636:4-636:80 *)
 unfold
 let betree_Node_lookup_in_bindings_decreases (key : u64)
   (bindings : betree_List_t (u64 & u64)) : nat =
   admit ()
 
-(** [betree_main::betree::{betree_main::betree::Internal#4}::lookup_in_children]: decreases clause *)
+(** [betree_main::betree::{betree_main::betree::Internal#4}::lookup_in_children]: decreases clause
+    Source: 'src/betree.rs', lines 395:4-395:63 *)
 unfold
 let betree_Internal_lookup_in_children_decreases (self : betree_Internal_t)
   (key : u64) (st : state) : nat =
   admit ()
 
-(** [betree_main::betree::{betree_main::betree::Node#5}::lookup]: decreases clause *)
+(** [betree_main::betree::{betree_main::betree::Node#5}::lookup]: decreases clause
+    Source: 'src/betree.rs', lines 709:4-709:58 *)
 unfold
 let betree_Node_lookup_decreases (self : betree_Node_t) (key : u64)
   (st : state) : nat =
   admit ()
 
-(** [betree_main::betree::{betree_main::betree::Node#5}::filter_messages_for_key]: decreases clause *)
+(** [betree_main::betree::{betree_main::betree::Node#5}::filter_messages_for_key]: decreases clause
+    Source: 'src/betree.rs', lines 674:4-674:77 *)
 unfold
 let betree_Node_filter_messages_for_key_decreases (key : u64)
   (msgs : betree_List_t (u64 & betree_Message_t)) : nat =
   admit ()
 
-(** [betree_main::betree::{betree_main::betree::Node#5}::lookup_first_message_after_key]: decreases clause *)
+(** [betree_main::betree::{betree_main::betree::Node#5}::lookup_first_message_after_key]: decreases clause
+    Source: 'src/betree.rs', lines 689:4-692:34 *)
 unfold
 let betree_Node_lookup_first_message_after_key_decreases (key : u64)
   (msgs : betree_List_t (u64 & betree_Message_t)) : nat =
   admit ()
 
-(** [betree_main::betree::{betree_main::betree::Node#5}::apply_messages_to_internal]: decreases clause *)
+(** [betree_main::betree::{betree_main::betree::Node#5}::apply_messages_to_internal]: decreases clause
+    Source: 'src/betree.rs', lines 502:4-505:5 *)
 unfold
 let betree_Node_apply_messages_to_internal_decreases
   (msgs : betree_List_t (u64 & betree_Message_t))
   (new_msgs : betree_List_t (u64 & betree_Message_t)) : nat =
   admit ()
 
-(** [betree_main::betree::{betree_main::betree::Node#5}::lookup_mut_in_bindings]: decreases clause *)
+(** [betree_main::betree::{betree_main::betree::Node#5}::lookup_mut_in_bindings]: decreases clause
+    Source: 'src/betree.rs', lines 653:4-656:32 *)
 unfold
 let betree_Node_lookup_mut_in_bindings_decreases (key : u64)
   (bindings : betree_List_t (u64 & u64)) : nat =
   admit ()
 
-(** [betree_main::betree::{betree_main::betree::Node#5}::apply_messages_to_leaf]: decreases clause *)
+(** [betree_main::betree::{betree_main::betree::Node#5}::apply_messages_to_leaf]: decreases clause
+    Source: 'src/betree.rs', lines 444:4-447:5 *)
 unfold
 let betree_Node_apply_messages_to_leaf_decreases
   (bindings : betree_List_t (u64 & u64))
   (new_msgs : betree_List_t (u64 & betree_Message_t)) : nat =
   admit ()
 
-(** [betree_main::betree::{betree_main::betree::Internal#4}::flush]: decreases clause *)
+(** [betree_main::betree::{betree_main::betree::Internal#4}::flush]: decreases clause
+    Source: 'src/betree.rs', lines 410:4-415:26 *)
 unfold
 let betree_Internal_flush_decreases (self : betree_Internal_t)
   (params : betree_Params_t) (node_id_cnt : betree_NodeIdCounter_t)
   (content : betree_List_t (u64 & betree_Message_t)) (st : state) : nat =
   admit ()
 
-(** [betree_main::betree::{betree_main::betree::Node#5}::apply_messages]: decreases clause *)
+(** [betree_main::betree::{betree_main::betree::Node#5}::apply_messages]: decreases clause
+    Source: 'src/betree.rs', lines 588:4-593:5 *)
 unfold
 let betree_Node_apply_messages_decreases (self : betree_Node_t)
   (params : betree_Params_t) (node_id_cnt : betree_NodeIdCounter_t)
diff --git a/tests/fstar/betree/BetreeMain.Funs.fst b/tests/fstar/betree/BetreeMain.Funs.fst
index 2ccbac60..537ec32e 100644
--- a/tests/fstar/betree/BetreeMain.Funs.fst
+++ b/tests/fstar/betree/BetreeMain.Funs.fst
@@ -8,14 +8,16 @@ include BetreeMain.Clauses
 
 #set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
 
-(** [betree_main::betree::load_internal_node]: forward function *)
+(** [betree_main::betree::load_internal_node]: forward function
+    Source: 'src/betree.rs', lines 36:0-36:52 *)
 let betree_load_internal_node
   (id : u64) (st : state) :
   result (state & (betree_List_t (u64 & betree_Message_t)))
   =
   betree_utils_load_internal_node id st
 
-(** [betree_main::betree::store_internal_node]: forward function *)
+(** [betree_main::betree::store_internal_node]: forward function
+    Source: 'src/betree.rs', lines 41:0-41:60 *)
 let betree_store_internal_node
   (id : u64) (content : betree_List_t (u64 & betree_Message_t)) (st : state) :
   result (state & unit)
@@ -23,12 +25,14 @@ let betree_store_internal_node
   let* (st0, _) = betree_utils_store_internal_node id content st in
   Return (st0, ())
 
-(** [betree_main::betree::load_leaf_node]: forward function *)
+(** [betree_main::betree::load_leaf_node]: forward function
+    Source: 'src/betree.rs', lines 46:0-46:44 *)
 let betree_load_leaf_node
   (id : u64) (st : state) : result (state & (betree_List_t (u64 & u64))) =
   betree_utils_load_leaf_node id st
 
-(** [betree_main::betree::store_leaf_node]: forward function *)
+(** [betree_main::betree::store_leaf_node]: forward function
+    Source: 'src/betree.rs', lines 51:0-51:52 *)
 let betree_store_leaf_node
   (id : u64) (content : betree_List_t (u64 & u64)) (st : state) :
   result (state & unit)
@@ -36,29 +40,35 @@ let betree_store_leaf_node
   let* (st0, _) = betree_utils_store_leaf_node id content st in
   Return (st0, ())
 
-(** [betree_main::betree::fresh_node_id]: forward function *)
+(** [betree_main::betree::fresh_node_id]: forward function
+    Source: 'src/betree.rs', lines 55:0-55:48 *)
 let betree_fresh_node_id (counter : u64) : result u64 =
   let* _ = u64_add counter 1 in Return counter
 
-(** [betree_main::betree::fresh_node_id]: backward function 0 *)
+(** [betree_main::betree::fresh_node_id]: backward function 0
+    Source: 'src/betree.rs', lines 55:0-55:48 *)
 let betree_fresh_node_id_back (counter : u64) : result u64 =
   u64_add counter 1
 
-(** [betree_main::betree::{betree_main::betree::NodeIdCounter}::new]: forward function *)
+(** [betree_main::betree::{betree_main::betree::NodeIdCounter}::new]: forward function
+    Source: 'src/betree.rs', lines 206:4-206:20 *)
 let betree_NodeIdCounter_new : result betree_NodeIdCounter_t =
   Return { next_node_id = 0 }
 
-(** [betree_main::betree::{betree_main::betree::NodeIdCounter}::fresh_id]: forward function *)
+(** [betree_main::betree::{betree_main::betree::NodeIdCounter}::fresh_id]: forward function
+    Source: 'src/betree.rs', lines 210:4-210:36 *)
 let betree_NodeIdCounter_fresh_id
   (self : betree_NodeIdCounter_t) : result u64 =
   let* _ = u64_add self.next_node_id 1 in Return self.next_node_id
 
-(** [betree_main::betree::{betree_main::betree::NodeIdCounter}::fresh_id]: backward function 0 *)
+(** [betree_main::betree::{betree_main::betree::NodeIdCounter}::fresh_id]: backward function 0
+    Source: 'src/betree.rs', lines 210:4-210:36 *)
 let betree_NodeIdCounter_fresh_id_back
   (self : betree_NodeIdCounter_t) : result betree_NodeIdCounter_t =
   let* i = u64_add self.next_node_id 1 in Return { next_node_id = i }
 
-(** [betree_main::betree::upsert_update]: forward function *)
+(** [betree_main::betree::upsert_update]: forward function
+    Source: 'src/betree.rs', lines 234:0-234:70 *)
 let betree_upsert_update
   (prev : option u64) (st : betree_UpsertFunState_t) : result u64 =
   begin match prev with
@@ -77,7 +87,8 @@ let betree_upsert_update
     end
   end
 
-(** [betree_main::betree::{betree_main::betree::List<T>#1}::len]: forward function *)
+(** [betree_main::betree::{betree_main::betree::List<T>#1}::len]: forward function
+    Source: 'src/betree.rs', lines 276:4-276:24 *)
 let rec betree_List_len
   (t : Type0) (self : betree_List_t t) :
   Tot (result u64) (decreases (betree_List_len_decreases t self))
@@ -87,7 +98,8 @@ let rec betree_List_len
   | Betree_List_Nil -> Return 0
   end
 
-(** [betree_main::betree::{betree_main::betree::List<T>#1}::split_at]: forward function *)
+(** [betree_main::betree::{betree_main::betree::List<T>#1}::split_at]: forward function
+    Source: 'src/betree.rs', lines 284:4-284:51 *)
 let rec betree_List_split_at
   (t : Type0) (self : betree_List_t t) (n : u64) :
   Tot (result ((betree_List_t t) & (betree_List_t t)))
@@ -107,14 +119,16 @@ let rec betree_List_split_at
     end
 
 (** [betree_main::betree::{betree_main::betree::List<T>#1}::push_front]: merged forward/backward function
-    (there is a single backward function, and the forward function returns ()) *)
+    (there is a single backward function, and the forward function returns ())
+    Source: 'src/betree.rs', lines 299:4-299:34 *)
 let betree_List_push_front
   (t : Type0) (self : betree_List_t t) (x : t) : result (betree_List_t t) =
   let tl = core_mem_replace (betree_List_t t) self Betree_List_Nil in
   let l = tl in
   Return (Betree_List_Cons x l)
 
-(** [betree_main::betree::{betree_main::betree::List<T>#1}::pop_front]: forward function *)
+(** [betree_main::betree::{betree_main::betree::List<T>#1}::pop_front]: forward function
+    Source: 'src/betree.rs', lines 306:4-306:32 *)
 let betree_List_pop_front (t : Type0) (self : betree_List_t t) : result t =
   let ls = core_mem_replace (betree_List_t t) self Betree_List_Nil in
   begin match ls with
@@ -122,7 +136,8 @@ let betree_List_pop_front (t : Type0) (self : betree_List_t t) : result t =
   | Betree_List_Nil -> Fail Failure
   end
 
-(** [betree_main::betree::{betree_main::betree::List<T>#1}::pop_front]: backward function 0 *)
+(** [betree_main::betree::{betree_main::betree::List<T>#1}::pop_front]: backward function 0
+    Source: 'src/betree.rs', lines 306:4-306:32 *)
 let betree_List_pop_front_back
   (t : Type0) (self : betree_List_t t) : result (betree_List_t t) =
   let ls = core_mem_replace (betree_List_t t) self Betree_List_Nil in
@@ -131,14 +146,16 @@ let betree_List_pop_front_back
   | Betree_List_Nil -> Fail Failure
   end
 
-(** [betree_main::betree::{betree_main::betree::List<T>#1}::hd]: forward function *)
+(** [betree_main::betree::{betree_main::betree::List<T>#1}::hd]: forward function
+    Source: 'src/betree.rs', lines 318:4-318:22 *)
 let betree_List_hd (t : Type0) (self : betree_List_t t) : result t =
   begin match self with
   | Betree_List_Cons hd l -> Return hd
   | Betree_List_Nil -> Fail Failure
   end
 
-(** [betree_main::betree::{betree_main::betree::List<(u64, T)>#2}::head_has_key]: forward function *)
+(** [betree_main::betree::{betree_main::betree::List<(u64, T)>#2}::head_has_key]: forward function
+    Source: 'src/betree.rs', lines 327:4-327:44 *)
 let betree_ListTupleU64T_head_has_key
   (t : Type0) (self : betree_List_t (u64 & t)) (key : u64) : result bool =
   begin match self with
@@ -146,7 +163,8 @@ let betree_ListTupleU64T_head_has_key
   | Betree_List_Nil -> Return false
   end
 
-(** [betree_main::betree::{betree_main::betree::List<(u64, T)>#2}::partition_at_pivot]: forward function *)
+(** [betree_main::betree::{betree_main::betree::List<(u64, T)>#2}::partition_at_pivot]: forward function
+    Source: 'src/betree.rs', lines 339:4-339:73 *)
 let rec betree_ListTupleU64T_partition_at_pivot
   (t : Type0) (self : betree_List_t (u64 & t)) (pivot : u64) :
   Tot (result ((betree_List_t (u64 & t)) & (betree_List_t (u64 & t))))
@@ -165,7 +183,8 @@ let rec betree_ListTupleU64T_partition_at_pivot
   | Betree_List_Nil -> Return (Betree_List_Nil, Betree_List_Nil)
   end
 
-(** [betree_main::betree::{betree_main::betree::Leaf#3}::split]: forward function *)
+(** [betree_main::betree::{betree_main::betree::Leaf#3}::split]: forward function
+    Source: 'src/betree.rs', lines 359:4-364:17 *)
 let betree_Leaf_split
   (self : betree_Leaf_t) (content : betree_List_t (u64 & u64))
   (params : betree_Params_t) (node_id_cnt : betree_NodeIdCounter_t)
@@ -185,7 +204,8 @@ let betree_Leaf_split
   let n0 = Betree_Node_Leaf { id = id1; size = params.split_size } in
   Return (st1, { id = self.id; pivot = pivot; left = n; right = n0 })
 
-(** [betree_main::betree::{betree_main::betree::Leaf#3}::split]: backward function 2 *)
+(** [betree_main::betree::{betree_main::betree::Leaf#3}::split]: backward function 2
+    Source: 'src/betree.rs', lines 359:4-364:17 *)
 let betree_Leaf_split_back
   (self : betree_Leaf_t) (content : betree_List_t (u64 & u64))
   (params : betree_Params_t) (node_id_cnt : betree_NodeIdCounter_t)
@@ -202,7 +222,8 @@ let betree_Leaf_split_back
   let* _ = betree_store_leaf_node id1 content1 st0 in
   betree_NodeIdCounter_fresh_id_back node_id_cnt0
 
-(** [betree_main::betree::{betree_main::betree::Node#5}::lookup_first_message_for_key]: forward function *)
+(** [betree_main::betree::{betree_main::betree::Node#5}::lookup_first_message_for_key]: forward function
+    Source: 'src/betree.rs', lines 789:4-792:34 *)
 let rec betree_Node_lookup_first_message_for_key
   (key : u64) (msgs : betree_List_t (u64 & betree_Message_t)) :
   Tot (result (betree_List_t (u64 & betree_Message_t)))
@@ -217,7 +238,8 @@ let rec betree_Node_lookup_first_message_for_key
   | Betree_List_Nil -> Return Betree_List_Nil
   end
 
-(** [betree_main::betree::{betree_main::betree::Node#5}::lookup_first_message_for_key]: backward function 0 *)
+(** [betree_main::betree::{betree_main::betree::Node#5}::lookup_first_message_for_key]: backward function 0
+    Source: 'src/betree.rs', lines 789:4-792:34 *)
 let rec betree_Node_lookup_first_message_for_key_back
   (key : u64) (msgs : betree_List_t (u64 & betree_Message_t))
   (ret : betree_List_t (u64 & betree_Message_t)) :
@@ -236,7 +258,8 @@ let rec betree_Node_lookup_first_message_for_key_back
   | Betree_List_Nil -> Return ret
   end
 
-(** [betree_main::betree::{betree_main::betree::Node#5}::apply_upserts]: forward function *)
+(** [betree_main::betree::{betree_main::betree::Node#5}::apply_upserts]: forward function
+    Source: 'src/betree.rs', lines 819:4-819:90 *)
 let rec betree_Node_apply_upserts
   (msgs : betree_List_t (u64 & betree_Message_t)) (prev : option u64)
   (key : u64) (st : state) :
@@ -263,7 +286,8 @@ let rec betree_Node_apply_upserts
         Betree_Message_Insert v) in
     Return (st0, v)
 
-(** [betree_main::betree::{betree_main::betree::Node#5}::apply_upserts]: backward function 0 *)
+(** [betree_main::betree::{betree_main::betree::Node#5}::apply_upserts]: backward function 0
+    Source: 'src/betree.rs', lines 819:4-819:90 *)
 let rec betree_Node_apply_upserts_back
   (msgs : betree_List_t (u64 & betree_Message_t)) (prev : option u64)
   (key : u64) (st : state) :
@@ -288,7 +312,8 @@ let rec betree_Node_apply_upserts_back
     betree_List_push_front (u64 & betree_Message_t) msgs (key,
       Betree_Message_Insert v)
 
-(** [betree_main::betree::{betree_main::betree::Node#5}::lookup_in_bindings]: forward function *)
+(** [betree_main::betree::{betree_main::betree::Node#5}::lookup_in_bindings]: forward function
+    Source: 'src/betree.rs', lines 636:4-636:80 *)
 let rec betree_Node_lookup_in_bindings
   (key : u64) (bindings : betree_List_t (u64 & u64)) :
   Tot (result (option u64))
@@ -303,7 +328,8 @@ let rec betree_Node_lookup_in_bindings
   | Betree_List_Nil -> Return None
   end
 
-(** [betree_main::betree::{betree_main::betree::Internal#4}::lookup_in_children]: forward function *)
+(** [betree_main::betree::{betree_main::betree::Internal#4}::lookup_in_children]: forward function
+    Source: 'src/betree.rs', lines 395:4-395:63 *)
 let rec betree_Internal_lookup_in_children
   (self : betree_Internal_t) (key : u64) (st : state) :
   Tot (result (state & (option u64)))
@@ -313,7 +339,8 @@ let rec betree_Internal_lookup_in_children
   then betree_Node_lookup self.left key st
   else betree_Node_lookup self.right key st
 
-(** [betree_main::betree::{betree_main::betree::Internal#4}::lookup_in_children]: backward function 0 *)
+(** [betree_main::betree::{betree_main::betree::Internal#4}::lookup_in_children]: backward function 0
+    Source: 'src/betree.rs', lines 395:4-395:63 *)
 and betree_Internal_lookup_in_children_back
   (self : betree_Internal_t) (key : u64) (st : state) :
   Tot (result betree_Internal_t)
@@ -327,7 +354,8 @@ and betree_Internal_lookup_in_children_back
     let* n = betree_Node_lookup_back self.right key st in
     Return { self with right = n }
 
-(** [betree_main::betree::{betree_main::betree::Node#5}::lookup]: forward function *)
+(** [betree_main::betree::{betree_main::betree::Node#5}::lookup]: forward function
+    Source: 'src/betree.rs', lines 709:4-709:58 *)
 and betree_Node_lookup
   (self : betree_Node_t) (key : u64) (st : state) :
   Tot (result (state & (option u64)))
@@ -386,7 +414,8 @@ and betree_Node_lookup
     Return (st0, o)
   end
 
-(** [betree_main::betree::{betree_main::betree::Node#5}::lookup]: backward function 0 *)
+(** [betree_main::betree::{betree_main::betree::Node#5}::lookup]: backward function 0
+    Source: 'src/betree.rs', lines 709:4-709:58 *)
 and betree_Node_lookup_back
   (self : betree_Node_t) (key : u64) (st : state) :
   Tot (result betree_Node_t)
@@ -446,7 +475,8 @@ and betree_Node_lookup_back
   end
 
 (** [betree_main::betree::{betree_main::betree::Node#5}::filter_messages_for_key]: merged forward/backward function
-    (there is a single backward function, and the forward function returns ()) *)
+    (there is a single backward function, and the forward function returns ())
+    Source: 'src/betree.rs', lines 674:4-674:77 *)
 let rec betree_Node_filter_messages_for_key
   (key : u64) (msgs : betree_List_t (u64 & betree_Message_t)) :
   Tot (result (betree_List_t (u64 & betree_Message_t)))
@@ -465,7 +495,8 @@ let rec betree_Node_filter_messages_for_key
   | Betree_List_Nil -> Return Betree_List_Nil
   end
 
-(** [betree_main::betree::{betree_main::betree::Node#5}::lookup_first_message_after_key]: forward function *)
+(** [betree_main::betree::{betree_main::betree::Node#5}::lookup_first_message_after_key]: forward function
+    Source: 'src/betree.rs', lines 689:4-692:34 *)
 let rec betree_Node_lookup_first_message_after_key
   (key : u64) (msgs : betree_List_t (u64 & betree_Message_t)) :
   Tot (result (betree_List_t (u64 & betree_Message_t)))
@@ -480,7 +511,8 @@ let rec betree_Node_lookup_first_message_after_key
   | Betree_List_Nil -> Return Betree_List_Nil
   end
 
-(** [betree_main::betree::{betree_main::betree::Node#5}::lookup_first_message_after_key]: backward function 0 *)
+(** [betree_main::betree::{betree_main::betree::Node#5}::lookup_first_message_after_key]: backward function 0
+    Source: 'src/betree.rs', lines 689:4-692:34 *)
 let rec betree_Node_lookup_first_message_after_key_back
   (key : u64) (msgs : betree_List_t (u64 & betree_Message_t))
   (ret : betree_List_t (u64 & betree_Message_t)) :
@@ -500,7 +532,8 @@ let rec betree_Node_lookup_first_message_after_key_back
   end
 
 (** [betree_main::betree::{betree_main::betree::Node#5}::apply_to_internal]: merged forward/backward function
-    (there is a single backward function, and the forward function returns ()) *)
+    (there is a single backward function, and the forward function returns ())
+    Source: 'src/betree.rs', lines 521:4-521:89 *)
 let betree_Node_apply_to_internal
   (msgs : betree_List_t (u64 & betree_Message_t)) (key : u64)
   (new_msg : betree_Message_t) :
@@ -559,7 +592,8 @@ let betree_Node_apply_to_internal
     betree_Node_lookup_first_message_for_key_back key msgs msgs1
 
 (** [betree_main::betree::{betree_main::betree::Node#5}::apply_messages_to_internal]: merged forward/backward function
-    (there is a single backward function, and the forward function returns ()) *)
+    (there is a single backward function, and the forward function returns ())
+    Source: 'src/betree.rs', lines 502:4-505:5 *)
 let rec betree_Node_apply_messages_to_internal
   (msgs : betree_List_t (u64 & betree_Message_t))
   (new_msgs : betree_List_t (u64 & betree_Message_t)) :
@@ -574,7 +608,8 @@ let rec betree_Node_apply_messages_to_internal
   | Betree_List_Nil -> Return msgs
   end
 
-(** [betree_main::betree::{betree_main::betree::Node#5}::lookup_mut_in_bindings]: forward function *)
+(** [betree_main::betree::{betree_main::betree::Node#5}::lookup_mut_in_bindings]: forward function
+    Source: 'src/betree.rs', lines 653:4-656:32 *)
 let rec betree_Node_lookup_mut_in_bindings
   (key : u64) (bindings : betree_List_t (u64 & u64)) :
   Tot (result (betree_List_t (u64 & u64)))
@@ -589,7 +624,8 @@ let rec betree_Node_lookup_mut_in_bindings
   | Betree_List_Nil -> Return Betree_List_Nil
   end
 
-(** [betree_main::betree::{betree_main::betree::Node#5}::lookup_mut_in_bindings]: backward function 0 *)
+(** [betree_main::betree::{betree_main::betree::Node#5}::lookup_mut_in_bindings]: backward function 0
+    Source: 'src/betree.rs', lines 653:4-656:32 *)
 let rec betree_Node_lookup_mut_in_bindings_back
   (key : u64) (bindings : betree_List_t (u64 & u64))
   (ret : betree_List_t (u64 & u64)) :
@@ -608,7 +644,8 @@ let rec betree_Node_lookup_mut_in_bindings_back
   end
 
 (** [betree_main::betree::{betree_main::betree::Node#5}::apply_to_leaf]: merged forward/backward function
-    (there is a single backward function, and the forward function returns ()) *)
+    (there is a single backward function, and the forward function returns ())
+    Source: 'src/betree.rs', lines 460:4-460:87 *)
 let betree_Node_apply_to_leaf
   (bindings : betree_List_t (u64 & u64)) (key : u64)
   (new_msg : betree_Message_t) :
@@ -648,7 +685,8 @@ let betree_Node_apply_to_leaf
     end
 
 (** [betree_main::betree::{betree_main::betree::Node#5}::apply_messages_to_leaf]: merged forward/backward function
-    (there is a single backward function, and the forward function returns ()) *)
+    (there is a single backward function, and the forward function returns ())
+    Source: 'src/betree.rs', lines 444:4-447:5 *)
 let rec betree_Node_apply_messages_to_leaf
   (bindings : betree_List_t (u64 & u64))
   (new_msgs : betree_List_t (u64 & betree_Message_t)) :
@@ -663,7 +701,8 @@ let rec betree_Node_apply_messages_to_leaf
   | Betree_List_Nil -> Return bindings
   end
 
-(** [betree_main::betree::{betree_main::betree::Internal#4}::flush]: forward function *)
+(** [betree_main::betree::{betree_main::betree::Internal#4}::flush]: forward function
+    Source: 'src/betree.rs', lines 410:4-415:26 *)
 let rec betree_Internal_flush
   (self : betree_Internal_t) (params : betree_Params_t)
   (node_id_cnt : betree_NodeIdCounter_t)
@@ -703,7 +742,8 @@ let rec betree_Internal_flush
         st in
     Return (st0, msgs_left)
 
-(** [betree_main::betree::{betree_main::betree::Internal#4}::flush]: backward function 0 *)
+(** [betree_main::betree::{betree_main::betree::Internal#4}::flush]: backward function 0
+    Source: 'src/betree.rs', lines 410:4-415:26 *)
 and betree_Internal_flush_back
   (self : betree_Internal_t) (params : betree_Params_t)
   (node_id_cnt : betree_NodeIdCounter_t)
@@ -738,7 +778,8 @@ and betree_Internal_flush_back
         st in
     Return ({ self with right = n }, node_id_cnt0)
 
-(** [betree_main::betree::{betree_main::betree::Node#5}::apply_messages]: forward function *)
+(** [betree_main::betree::{betree_main::betree::Node#5}::apply_messages]: forward function
+    Source: 'src/betree.rs', lines 588:4-593:5 *)
 and betree_Node_apply_messages
   (self : betree_Node_t) (params : betree_Params_t)
   (node_id_cnt : betree_NodeIdCounter_t)
@@ -778,7 +819,8 @@ and betree_Node_apply_messages
       Return (st1, ())
   end
 
-(** [betree_main::betree::{betree_main::betree::Node#5}::apply_messages]: backward function 0 *)
+(** [betree_main::betree::{betree_main::betree::Node#5}::apply_messages]: backward function 0
+    Source: 'src/betree.rs', lines 588:4-593:5 *)
 and betree_Node_apply_messages_back
   (self : betree_Node_t) (params : betree_Params_t)
   (node_id_cnt : betree_NodeIdCounter_t)
@@ -821,7 +863,8 @@ and betree_Node_apply_messages_back
       Return (Betree_Node_Leaf { node with size = len }, node_id_cnt)
   end
 
-(** [betree_main::betree::{betree_main::betree::Node#5}::apply]: forward function *)
+(** [betree_main::betree::{betree_main::betree::Node#5}::apply]: forward function
+    Source: 'src/betree.rs', lines 576:4-582:5 *)
 let betree_Node_apply
   (self : betree_Node_t) (params : betree_Params_t)
   (node_id_cnt : betree_NodeIdCounter_t) (key : u64)
@@ -837,7 +880,8 @@ let betree_Node_apply
       (key, new_msg) l) st in
   Return (st0, ())
 
-(** [betree_main::betree::{betree_main::betree::Node#5}::apply]: backward function 0 *)
+(** [betree_main::betree::{betree_main::betree::Node#5}::apply]: backward function 0
+    Source: 'src/betree.rs', lines 576:4-582:5 *)
 let betree_Node_apply_back
   (self : betree_Node_t) (params : betree_Params_t)
   (node_id_cnt : betree_NodeIdCounter_t) (key : u64)
@@ -848,7 +892,8 @@ let betree_Node_apply_back
   betree_Node_apply_messages_back self params node_id_cnt (Betree_List_Cons
     (key, new_msg) l) st
 
-(** [betree_main::betree::{betree_main::betree::BeTree#6}::new]: forward function *)
+(** [betree_main::betree::{betree_main::betree::BeTree#6}::new]: forward function
+    Source: 'src/betree.rs', lines 849:4-849:60 *)
 let betree_BeTree_new
   (min_flush_size : u64) (split_size : u64) (st : state) :
   result (state & betree_BeTree_t)
@@ -864,7 +909,8 @@ let betree_BeTree_new
       root = (Betree_Node_Leaf { id = id; size = 0 })
     })
 
-(** [betree_main::betree::{betree_main::betree::BeTree#6}::apply]: forward function *)
+(** [betree_main::betree::{betree_main::betree::BeTree#6}::apply]: forward function
+    Source: 'src/betree.rs', lines 868:4-868:47 *)
 let betree_BeTree_apply
   (self : betree_BeTree_t) (key : u64) (msg : betree_Message_t) (st : state) :
   result (state & unit)
@@ -875,7 +921,8 @@ let betree_BeTree_apply
     betree_Node_apply_back self.root self.params self.node_id_cnt key msg st in
   Return (st0, ())
 
-(** [betree_main::betree::{betree_main::betree::BeTree#6}::apply]: backward function 0 *)
+(** [betree_main::betree::{betree_main::betree::BeTree#6}::apply]: backward function 0
+    Source: 'src/betree.rs', lines 868:4-868:47 *)
 let betree_BeTree_apply_back
   (self : betree_BeTree_t) (key : u64) (msg : betree_Message_t) (st : state) :
   result betree_BeTree_t
@@ -884,7 +931,8 @@ let betree_BeTree_apply_back
     betree_Node_apply_back self.root self.params self.node_id_cnt key msg st in
   Return { self with node_id_cnt = nic; root = n }
 
-(** [betree_main::betree::{betree_main::betree::BeTree#6}::insert]: forward function *)
+(** [betree_main::betree::{betree_main::betree::BeTree#6}::insert]: forward function
+    Source: 'src/betree.rs', lines 874:4-874:52 *)
 let betree_BeTree_insert
   (self : betree_BeTree_t) (key : u64) (value : u64) (st : state) :
   result (state & unit)
@@ -895,26 +943,30 @@ let betree_BeTree_insert
     in
   Return (st0, ())
 
-(** [betree_main::betree::{betree_main::betree::BeTree#6}::insert]: backward function 0 *)
+(** [betree_main::betree::{betree_main::betree::BeTree#6}::insert]: backward function 0
+    Source: 'src/betree.rs', lines 874:4-874:52 *)
 let betree_BeTree_insert_back
   (self : betree_BeTree_t) (key : u64) (value : u64) (st : state) :
   result betree_BeTree_t
   =
   betree_BeTree_apply_back self key (Betree_Message_Insert value) st
 
-(** [betree_main::betree::{betree_main::betree::BeTree#6}::delete]: forward function *)
+(** [betree_main::betree::{betree_main::betree::BeTree#6}::delete]: forward function
+    Source: 'src/betree.rs', lines 880:4-880:38 *)
 let betree_BeTree_delete
   (self : betree_BeTree_t) (key : u64) (st : state) : result (state & unit) =
   let* (st0, _) = betree_BeTree_apply self key Betree_Message_Delete st in
   let* _ = betree_BeTree_apply_back self key Betree_Message_Delete st in
   Return (st0, ())
 
-(** [betree_main::betree::{betree_main::betree::BeTree#6}::delete]: backward function 0 *)
+(** [betree_main::betree::{betree_main::betree::BeTree#6}::delete]: backward function 0
+    Source: 'src/betree.rs', lines 880:4-880:38 *)
 let betree_BeTree_delete_back
   (self : betree_BeTree_t) (key : u64) (st : state) : result betree_BeTree_t =
   betree_BeTree_apply_back self key Betree_Message_Delete st
 
-(** [betree_main::betree::{betree_main::betree::BeTree#6}::upsert]: forward function *)
+(** [betree_main::betree::{betree_main::betree::BeTree#6}::upsert]: forward function
+    Source: 'src/betree.rs', lines 886:4-886:59 *)
 let betree_BeTree_upsert
   (self : betree_BeTree_t) (key : u64) (upd : betree_UpsertFunState_t)
   (st : state) :
@@ -925,7 +977,8 @@ let betree_BeTree_upsert
   let* _ = betree_BeTree_apply_back self key (Betree_Message_Upsert upd) st in
   Return (st0, ())
 
-(** [betree_main::betree::{betree_main::betree::BeTree#6}::upsert]: backward function 0 *)
+(** [betree_main::betree::{betree_main::betree::BeTree#6}::upsert]: backward function 0
+    Source: 'src/betree.rs', lines 886:4-886:59 *)
 let betree_BeTree_upsert_back
   (self : betree_BeTree_t) (key : u64) (upd : betree_UpsertFunState_t)
   (st : state) :
@@ -933,20 +986,23 @@ let betree_BeTree_upsert_back
   =
   betree_BeTree_apply_back self key (Betree_Message_Upsert upd) st
 
-(** [betree_main::betree::{betree_main::betree::BeTree#6}::lookup]: forward function *)
+(** [betree_main::betree::{betree_main::betree::BeTree#6}::lookup]: forward function
+    Source: 'src/betree.rs', lines 895:4-895:62 *)
 let betree_BeTree_lookup
   (self : betree_BeTree_t) (key : u64) (st : state) :
   result (state & (option u64))
   =
   betree_Node_lookup self.root key st
 
-(** [betree_main::betree::{betree_main::betree::BeTree#6}::lookup]: backward function 0 *)
+(** [betree_main::betree::{betree_main::betree::BeTree#6}::lookup]: backward function 0
+    Source: 'src/betree.rs', lines 895:4-895:62 *)
 let betree_BeTree_lookup_back
   (self : betree_BeTree_t) (key : u64) (st : state) : result betree_BeTree_t =
   let* n = betree_Node_lookup_back self.root key st in
   Return { self with root = n }
 
-(** [betree_main::main]: forward function *)
+(** [betree_main::main]: forward function
+    Source: 'src/betree_main.rs', lines 5:0-5:9 *)
 let main : result unit =
   Return ()
 
diff --git a/tests/fstar/betree/BetreeMain.Opaque.fsti b/tests/fstar/betree/BetreeMain.Opaque.fsti
index 23d2e60e..b89c8718 100644
--- a/tests/fstar/betree/BetreeMain.Opaque.fsti
+++ b/tests/fstar/betree/BetreeMain.Opaque.fsti
@@ -6,25 +6,30 @@ include BetreeMain.Types
 
 #set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
 
-(** [betree_main::betree_utils::load_internal_node]: forward function *)
+(** [betree_main::betree_utils::load_internal_node]: forward function
+    Source: 'src/betree_utils.rs', lines 98:0-98:63 *)
 val betree_utils_load_internal_node
   : u64 -> state -> result (state & (betree_List_t (u64 & betree_Message_t)))
 
-(** [betree_main::betree_utils::store_internal_node]: forward function *)
+(** [betree_main::betree_utils::store_internal_node]: forward function
+    Source: 'src/betree_utils.rs', lines 115:0-115:71 *)
 val betree_utils_store_internal_node
   :
   u64 -> betree_List_t (u64 & betree_Message_t) -> state -> result (state &
     unit)
 
-(** [betree_main::betree_utils::load_leaf_node]: forward function *)
+(** [betree_main::betree_utils::load_leaf_node]: forward function
+    Source: 'src/betree_utils.rs', lines 132:0-132:55 *)
 val betree_utils_load_leaf_node
   : u64 -> state -> result (state & (betree_List_t (u64 & u64)))
 
-(** [betree_main::betree_utils::store_leaf_node]: forward function *)
+(** [betree_main::betree_utils::store_leaf_node]: forward function
+    Source: 'src/betree_utils.rs', lines 145:0-145:63 *)
 val betree_utils_store_leaf_node
   : u64 -> betree_List_t (u64 & u64) -> state -> result (state & unit)
 
-(** [core::option::{core::option::Option<T>}::unwrap]: forward function *)
+(** [core::option::{core::option::Option<T>}::unwrap]: forward function
+    Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/option.rs', lines 932:4-932:34 *)
 val core_option_Option_unwrap
   (t : Type0) : option t -> state -> result (state & t)
 
diff --git a/tests/fstar/betree/BetreeMain.Types.fsti b/tests/fstar/betree/BetreeMain.Types.fsti
index 9320f6b7..a098ec19 100644
--- a/tests/fstar/betree/BetreeMain.Types.fsti
+++ b/tests/fstar/betree/BetreeMain.Types.fsti
@@ -5,43 +5,52 @@ open Primitives
 
 #set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
 
-(** [betree_main::betree::List] *)
+(** [betree_main::betree::List]
+    Source: 'src/betree.rs', lines 17:0-17:23 *)
 type betree_List_t (t : Type0) =
 | Betree_List_Cons : t -> betree_List_t t -> betree_List_t t
 | Betree_List_Nil : betree_List_t t
 
-(** [betree_main::betree::UpsertFunState] *)
+(** [betree_main::betree::UpsertFunState]
+    Source: 'src/betree.rs', lines 63:0-63:23 *)
 type betree_UpsertFunState_t =
 | Betree_UpsertFunState_Add : u64 -> betree_UpsertFunState_t
 | Betree_UpsertFunState_Sub : u64 -> betree_UpsertFunState_t
 
-(** [betree_main::betree::Message] *)
+(** [betree_main::betree::Message]
+    Source: 'src/betree.rs', lines 69:0-69:23 *)
 type betree_Message_t =
 | Betree_Message_Insert : u64 -> betree_Message_t
 | Betree_Message_Delete : betree_Message_t
 | Betree_Message_Upsert : betree_UpsertFunState_t -> betree_Message_t
 
-(** [betree_main::betree::Leaf] *)
+(** [betree_main::betree::Leaf]
+    Source: 'src/betree.rs', lines 167:0-167:11 *)
 type betree_Leaf_t = { id : u64; size : u64; }
 
-(** [betree_main::betree::Internal] *)
+(** [betree_main::betree::Internal]
+    Source: 'src/betree.rs', lines 156:0-156:15 *)
 type betree_Internal_t =
 {
   id : u64; pivot : u64; left : betree_Node_t; right : betree_Node_t;
 }
 
-(** [betree_main::betree::Node] *)
+(** [betree_main::betree::Node]
+    Source: 'src/betree.rs', lines 179:0-179:9 *)
 and betree_Node_t =
 | Betree_Node_Internal : betree_Internal_t -> betree_Node_t
 | Betree_Node_Leaf : betree_Leaf_t -> betree_Node_t
 
-(** [betree_main::betree::Params] *)
+(** [betree_main::betree::Params]
+    Source: 'src/betree.rs', lines 187:0-187:13 *)
 type betree_Params_t = { min_flush_size : u64; split_size : u64; }
 
-(** [betree_main::betree::NodeIdCounter] *)
+(** [betree_main::betree::NodeIdCounter]
+    Source: 'src/betree.rs', lines 201:0-201:20 *)
 type betree_NodeIdCounter_t = { next_node_id : u64; }
 
-(** [betree_main::betree::BeTree] *)
+(** [betree_main::betree::BeTree]
+    Source: 'src/betree.rs', lines 218:0-218:17 *)
 type betree_BeTree_t =
 {
   params : betree_Params_t;
diff --git a/tests/fstar/betree_back_stateful/BetreeMain.Clauses.Template.fst b/tests/fstar/betree_back_stateful/BetreeMain.Clauses.Template.fst
index 4d16d8d3..4ae29302 100644
--- a/tests/fstar/betree_back_stateful/BetreeMain.Clauses.Template.fst
+++ b/tests/fstar/betree_back_stateful/BetreeMain.Clauses.Template.fst
@@ -6,94 +6,109 @@ open BetreeMain.Types
 
 #set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
 
-(** [betree_main::betree::{betree_main::betree::List<T>#1}::len]: decreases clause *)
+(** [betree_main::betree::{betree_main::betree::List<T>#1}::len]: decreases clause
+    Source: 'src/betree.rs', lines 276:4-276:24 *)
 unfold
 let betree_List_len_decreases (t : Type0) (self : betree_List_t t) : nat =
   admit ()
 
-(** [betree_main::betree::{betree_main::betree::List<T>#1}::split_at]: decreases clause *)
+(** [betree_main::betree::{betree_main::betree::List<T>#1}::split_at]: decreases clause
+    Source: 'src/betree.rs', lines 284:4-284:51 *)
 unfold
 let betree_List_split_at_decreases (t : Type0) (self : betree_List_t t)
   (n : u64) : nat =
   admit ()
 
-(** [betree_main::betree::{betree_main::betree::List<(u64, T)>#2}::partition_at_pivot]: decreases clause *)
+(** [betree_main::betree::{betree_main::betree::List<(u64, T)>#2}::partition_at_pivot]: decreases clause
+    Source: 'src/betree.rs', lines 339:4-339:73 *)
 unfold
 let betree_ListTupleU64T_partition_at_pivot_decreases (t : Type0)
   (self : betree_List_t (u64 & t)) (pivot : u64) : nat =
   admit ()
 
-(** [betree_main::betree::{betree_main::betree::Node#5}::lookup_first_message_for_key]: decreases clause *)
+(** [betree_main::betree::{betree_main::betree::Node#5}::lookup_first_message_for_key]: decreases clause
+    Source: 'src/betree.rs', lines 789:4-792:34 *)
 unfold
 let betree_Node_lookup_first_message_for_key_decreases (key : u64)
   (msgs : betree_List_t (u64 & betree_Message_t)) : nat =
   admit ()
 
-(** [betree_main::betree::{betree_main::betree::Node#5}::apply_upserts]: decreases clause *)
+(** [betree_main::betree::{betree_main::betree::Node#5}::apply_upserts]: decreases clause
+    Source: 'src/betree.rs', lines 819:4-819:90 *)
 unfold
 let betree_Node_apply_upserts_decreases
   (msgs : betree_List_t (u64 & betree_Message_t)) (prev : option u64)
   (key : u64) (st : state) : nat =
   admit ()
 
-(** [betree_main::betree::{betree_main::betree::Node#5}::lookup_in_bindings]: decreases clause *)
+(** [betree_main::betree::{betree_main::betree::Node#5}::lookup_in_bindings]: decreases clause
+    Source: 'src/betree.rs', lines 636:4-636:80 *)
 unfold
 let betree_Node_lookup_in_bindings_decreases (key : u64)
   (bindings : betree_List_t (u64 & u64)) : nat =
   admit ()
 
-(** [betree_main::betree::{betree_main::betree::Internal#4}::lookup_in_children]: decreases clause *)
+(** [betree_main::betree::{betree_main::betree::Internal#4}::lookup_in_children]: decreases clause
+    Source: 'src/betree.rs', lines 395:4-395:63 *)
 unfold
 let betree_Internal_lookup_in_children_decreases (self : betree_Internal_t)
   (key : u64) (st : state) : nat =
   admit ()
 
-(** [betree_main::betree::{betree_main::betree::Node#5}::lookup]: decreases clause *)
+(** [betree_main::betree::{betree_main::betree::Node#5}::lookup]: decreases clause
+    Source: 'src/betree.rs', lines 709:4-709:58 *)
 unfold
 let betree_Node_lookup_decreases (self : betree_Node_t) (key : u64)
   (st : state) : nat =
   admit ()
 
-(** [betree_main::betree::{betree_main::betree::Node#5}::filter_messages_for_key]: decreases clause *)
+(** [betree_main::betree::{betree_main::betree::Node#5}::filter_messages_for_key]: decreases clause
+    Source: 'src/betree.rs', lines 674:4-674:77 *)
 unfold
 let betree_Node_filter_messages_for_key_decreases (key : u64)
   (msgs : betree_List_t (u64 & betree_Message_t)) : nat =
   admit ()
 
-(** [betree_main::betree::{betree_main::betree::Node#5}::lookup_first_message_after_key]: decreases clause *)
+(** [betree_main::betree::{betree_main::betree::Node#5}::lookup_first_message_after_key]: decreases clause
+    Source: 'src/betree.rs', lines 689:4-692:34 *)
 unfold
 let betree_Node_lookup_first_message_after_key_decreases (key : u64)
   (msgs : betree_List_t (u64 & betree_Message_t)) : nat =
   admit ()
 
-(** [betree_main::betree::{betree_main::betree::Node#5}::apply_messages_to_internal]: decreases clause *)
+(** [betree_main::betree::{betree_main::betree::Node#5}::apply_messages_to_internal]: decreases clause
+    Source: 'src/betree.rs', lines 502:4-505:5 *)
 unfold
 let betree_Node_apply_messages_to_internal_decreases
   (msgs : betree_List_t (u64 & betree_Message_t))
   (new_msgs : betree_List_t (u64 & betree_Message_t)) : nat =
   admit ()
 
-(** [betree_main::betree::{betree_main::betree::Node#5}::lookup_mut_in_bindings]: decreases clause *)
+(** [betree_main::betree::{betree_main::betree::Node#5}::lookup_mut_in_bindings]: decreases clause
+    Source: 'src/betree.rs', lines 653:4-656:32 *)
 unfold
 let betree_Node_lookup_mut_in_bindings_decreases (key : u64)
   (bindings : betree_List_t (u64 & u64)) : nat =
   admit ()
 
-(** [betree_main::betree::{betree_main::betree::Node#5}::apply_messages_to_leaf]: decreases clause *)
+(** [betree_main::betree::{betree_main::betree::Node#5}::apply_messages_to_leaf]: decreases clause
+    Source: 'src/betree.rs', lines 444:4-447:5 *)
 unfold
 let betree_Node_apply_messages_to_leaf_decreases
   (bindings : betree_List_t (u64 & u64))
   (new_msgs : betree_List_t (u64 & betree_Message_t)) : nat =
   admit ()
 
-(** [betree_main::betree::{betree_main::betree::Internal#4}::flush]: decreases clause *)
+(** [betree_main::betree::{betree_main::betree::Internal#4}::flush]: decreases clause
+    Source: 'src/betree.rs', lines 410:4-415:26 *)
 unfold
 let betree_Internal_flush_decreases (self : betree_Internal_t)
   (params : betree_Params_t) (node_id_cnt : betree_NodeIdCounter_t)
   (content : betree_List_t (u64 & betree_Message_t)) (st : state) : nat =
   admit ()
 
-(** [betree_main::betree::{betree_main::betree::Node#5}::apply_messages]: decreases clause *)
+(** [betree_main::betree::{betree_main::betree::Node#5}::apply_messages]: decreases clause
+    Source: 'src/betree.rs', lines 588:4-593:5 *)
 unfold
 let betree_Node_apply_messages_decreases (self : betree_Node_t)
   (params : betree_Params_t) (node_id_cnt : betree_NodeIdCounter_t)
diff --git a/tests/fstar/betree_back_stateful/BetreeMain.Funs.fst b/tests/fstar/betree_back_stateful/BetreeMain.Funs.fst
index b46ca0a0..a2586431 100644
--- a/tests/fstar/betree_back_stateful/BetreeMain.Funs.fst
+++ b/tests/fstar/betree_back_stateful/BetreeMain.Funs.fst
@@ -8,14 +8,16 @@ include BetreeMain.Clauses
 
 #set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
 
-(** [betree_main::betree::load_internal_node]: forward function *)
+(** [betree_main::betree::load_internal_node]: forward function
+    Source: 'src/betree.rs', lines 36:0-36:52 *)
 let betree_load_internal_node
   (id : u64) (st : state) :
   result (state & (betree_List_t (u64 & betree_Message_t)))
   =
   betree_utils_load_internal_node id st
 
-(** [betree_main::betree::store_internal_node]: forward function *)
+(** [betree_main::betree::store_internal_node]: forward function
+    Source: 'src/betree.rs', lines 41:0-41:60 *)
 let betree_store_internal_node
   (id : u64) (content : betree_List_t (u64 & betree_Message_t)) (st : state) :
   result (state & unit)
@@ -23,12 +25,14 @@ let betree_store_internal_node
   let* (st0, _) = betree_utils_store_internal_node id content st in
   Return (st0, ())
 
-(** [betree_main::betree::load_leaf_node]: forward function *)
+(** [betree_main::betree::load_leaf_node]: forward function
+    Source: 'src/betree.rs', lines 46:0-46:44 *)
 let betree_load_leaf_node
   (id : u64) (st : state) : result (state & (betree_List_t (u64 & u64))) =
   betree_utils_load_leaf_node id st
 
-(** [betree_main::betree::store_leaf_node]: forward function *)
+(** [betree_main::betree::store_leaf_node]: forward function
+    Source: 'src/betree.rs', lines 51:0-51:52 *)
 let betree_store_leaf_node
   (id : u64) (content : betree_List_t (u64 & u64)) (st : state) :
   result (state & unit)
@@ -36,29 +40,35 @@ let betree_store_leaf_node
   let* (st0, _) = betree_utils_store_leaf_node id content st in
   Return (st0, ())
 
-(** [betree_main::betree::fresh_node_id]: forward function *)
+(** [betree_main::betree::fresh_node_id]: forward function
+    Source: 'src/betree.rs', lines 55:0-55:48 *)
 let betree_fresh_node_id (counter : u64) : result u64 =
   let* _ = u64_add counter 1 in Return counter
 
-(** [betree_main::betree::fresh_node_id]: backward function 0 *)
+(** [betree_main::betree::fresh_node_id]: backward function 0
+    Source: 'src/betree.rs', lines 55:0-55:48 *)
 let betree_fresh_node_id_back (counter : u64) : result u64 =
   u64_add counter 1
 
-(** [betree_main::betree::{betree_main::betree::NodeIdCounter}::new]: forward function *)
+(** [betree_main::betree::{betree_main::betree::NodeIdCounter}::new]: forward function
+    Source: 'src/betree.rs', lines 206:4-206:20 *)
 let betree_NodeIdCounter_new : result betree_NodeIdCounter_t =
   Return { next_node_id = 0 }
 
-(** [betree_main::betree::{betree_main::betree::NodeIdCounter}::fresh_id]: forward function *)
+(** [betree_main::betree::{betree_main::betree::NodeIdCounter}::fresh_id]: forward function
+    Source: 'src/betree.rs', lines 210:4-210:36 *)
 let betree_NodeIdCounter_fresh_id
   (self : betree_NodeIdCounter_t) : result u64 =
   let* _ = u64_add self.next_node_id 1 in Return self.next_node_id
 
-(** [betree_main::betree::{betree_main::betree::NodeIdCounter}::fresh_id]: backward function 0 *)
+(** [betree_main::betree::{betree_main::betree::NodeIdCounter}::fresh_id]: backward function 0
+    Source: 'src/betree.rs', lines 210:4-210:36 *)
 let betree_NodeIdCounter_fresh_id_back
   (self : betree_NodeIdCounter_t) : result betree_NodeIdCounter_t =
   let* i = u64_add self.next_node_id 1 in Return { next_node_id = i }
 
-(** [betree_main::betree::upsert_update]: forward function *)
+(** [betree_main::betree::upsert_update]: forward function
+    Source: 'src/betree.rs', lines 234:0-234:70 *)
 let betree_upsert_update
   (prev : option u64) (st : betree_UpsertFunState_t) : result u64 =
   begin match prev with
@@ -77,7 +87,8 @@ let betree_upsert_update
     end
   end
 
-(** [betree_main::betree::{betree_main::betree::List<T>#1}::len]: forward function *)
+(** [betree_main::betree::{betree_main::betree::List<T>#1}::len]: forward function
+    Source: 'src/betree.rs', lines 276:4-276:24 *)
 let rec betree_List_len
   (t : Type0) (self : betree_List_t t) :
   Tot (result u64) (decreases (betree_List_len_decreases t self))
@@ -87,7 +98,8 @@ let rec betree_List_len
   | Betree_List_Nil -> Return 0
   end
 
-(** [betree_main::betree::{betree_main::betree::List<T>#1}::split_at]: forward function *)
+(** [betree_main::betree::{betree_main::betree::List<T>#1}::split_at]: forward function
+    Source: 'src/betree.rs', lines 284:4-284:51 *)
 let rec betree_List_split_at
   (t : Type0) (self : betree_List_t t) (n : u64) :
   Tot (result ((betree_List_t t) & (betree_List_t t)))
@@ -107,14 +119,16 @@ let rec betree_List_split_at
     end
 
 (** [betree_main::betree::{betree_main::betree::List<T>#1}::push_front]: merged forward/backward function
-    (there is a single backward function, and the forward function returns ()) *)
+    (there is a single backward function, and the forward function returns ())
+    Source: 'src/betree.rs', lines 299:4-299:34 *)
 let betree_List_push_front
   (t : Type0) (self : betree_List_t t) (x : t) : result (betree_List_t t) =
   let tl = core_mem_replace (betree_List_t t) self Betree_List_Nil in
   let l = tl in
   Return (Betree_List_Cons x l)
 
-(** [betree_main::betree::{betree_main::betree::List<T>#1}::pop_front]: forward function *)
+(** [betree_main::betree::{betree_main::betree::List<T>#1}::pop_front]: forward function
+    Source: 'src/betree.rs', lines 306:4-306:32 *)
 let betree_List_pop_front (t : Type0) (self : betree_List_t t) : result t =
   let ls = core_mem_replace (betree_List_t t) self Betree_List_Nil in
   begin match ls with
@@ -122,7 +136,8 @@ let betree_List_pop_front (t : Type0) (self : betree_List_t t) : result t =
   | Betree_List_Nil -> Fail Failure
   end
 
-(** [betree_main::betree::{betree_main::betree::List<T>#1}::pop_front]: backward function 0 *)
+(** [betree_main::betree::{betree_main::betree::List<T>#1}::pop_front]: backward function 0
+    Source: 'src/betree.rs', lines 306:4-306:32 *)
 let betree_List_pop_front_back
   (t : Type0) (self : betree_List_t t) : result (betree_List_t t) =
   let ls = core_mem_replace (betree_List_t t) self Betree_List_Nil in
@@ -131,14 +146,16 @@ let betree_List_pop_front_back
   | Betree_List_Nil -> Fail Failure
   end
 
-(** [betree_main::betree::{betree_main::betree::List<T>#1}::hd]: forward function *)
+(** [betree_main::betree::{betree_main::betree::List<T>#1}::hd]: forward function
+    Source: 'src/betree.rs', lines 318:4-318:22 *)
 let betree_List_hd (t : Type0) (self : betree_List_t t) : result t =
   begin match self with
   | Betree_List_Cons hd l -> Return hd
   | Betree_List_Nil -> Fail Failure
   end
 
-(** [betree_main::betree::{betree_main::betree::List<(u64, T)>#2}::head_has_key]: forward function *)
+(** [betree_main::betree::{betree_main::betree::List<(u64, T)>#2}::head_has_key]: forward function
+    Source: 'src/betree.rs', lines 327:4-327:44 *)
 let betree_ListTupleU64T_head_has_key
   (t : Type0) (self : betree_List_t (u64 & t)) (key : u64) : result bool =
   begin match self with
@@ -146,7 +163,8 @@ let betree_ListTupleU64T_head_has_key
   | Betree_List_Nil -> Return false
   end
 
-(** [betree_main::betree::{betree_main::betree::List<(u64, T)>#2}::partition_at_pivot]: forward function *)
+(** [betree_main::betree::{betree_main::betree::List<(u64, T)>#2}::partition_at_pivot]: forward function
+    Source: 'src/betree.rs', lines 339:4-339:73 *)
 let rec betree_ListTupleU64T_partition_at_pivot
   (t : Type0) (self : betree_List_t (u64 & t)) (pivot : u64) :
   Tot (result ((betree_List_t (u64 & t)) & (betree_List_t (u64 & t))))
@@ -165,7 +183,8 @@ let rec betree_ListTupleU64T_partition_at_pivot
   | Betree_List_Nil -> Return (Betree_List_Nil, Betree_List_Nil)
   end
 
-(** [betree_main::betree::{betree_main::betree::Leaf#3}::split]: forward function *)
+(** [betree_main::betree::{betree_main::betree::Leaf#3}::split]: forward function
+    Source: 'src/betree.rs', lines 359:4-364:17 *)
 let betree_Leaf_split
   (self : betree_Leaf_t) (content : betree_List_t (u64 & u64))
   (params : betree_Params_t) (node_id_cnt : betree_NodeIdCounter_t)
@@ -185,7 +204,8 @@ let betree_Leaf_split
   let n0 = Betree_Node_Leaf { id = id1; size = params.split_size } in
   Return (st1, { id = self.id; pivot = pivot; left = n; right = n0 })
 
-(** [betree_main::betree::{betree_main::betree::Leaf#3}::split]: backward function 0 *)
+(** [betree_main::betree::{betree_main::betree::Leaf#3}::split]: backward function 0
+    Source: 'src/betree.rs', lines 359:4-364:17 *)
 let betree_Leaf_split_back0
   (self : betree_Leaf_t) (content : betree_List_t (u64 & u64))
   (params : betree_Params_t) (node_id_cnt : betree_NodeIdCounter_t)
@@ -202,7 +222,8 @@ let betree_Leaf_split_back0
   let* _ = betree_store_leaf_node id1 content1 st1 in
   Return (st0, ())
 
-(** [betree_main::betree::{betree_main::betree::Leaf#3}::split]: backward function 1 *)
+(** [betree_main::betree::{betree_main::betree::Leaf#3}::split]: backward function 1
+    Source: 'src/betree.rs', lines 359:4-364:17 *)
 let betree_Leaf_split_back1
   (self : betree_Leaf_t) (content : betree_List_t (u64 & u64))
   (params : betree_Params_t) (node_id_cnt : betree_NodeIdCounter_t)
@@ -219,7 +240,8 @@ let betree_Leaf_split_back1
   let* _ = betree_store_leaf_node id1 content1 st1 in
   Return (st0, ())
 
-(** [betree_main::betree::{betree_main::betree::Leaf#3}::split]: backward function 2 *)
+(** [betree_main::betree::{betree_main::betree::Leaf#3}::split]: backward function 2
+    Source: 'src/betree.rs', lines 359:4-364:17 *)
 let betree_Leaf_split_back2
   (self : betree_Leaf_t) (content : betree_List_t (u64 & u64))
   (params : betree_Params_t) (node_id_cnt : betree_NodeIdCounter_t)
@@ -237,7 +259,8 @@ let betree_Leaf_split_back2
   let* node_id_cnt1 = betree_NodeIdCounter_fresh_id_back node_id_cnt0 in
   Return (st0, node_id_cnt1)
 
-(** [betree_main::betree::{betree_main::betree::Node#5}::lookup_first_message_for_key]: forward function *)
+(** [betree_main::betree::{betree_main::betree::Node#5}::lookup_first_message_for_key]: forward function
+    Source: 'src/betree.rs', lines 789:4-792:34 *)
 let rec betree_Node_lookup_first_message_for_key
   (key : u64) (msgs : betree_List_t (u64 & betree_Message_t)) :
   Tot (result (betree_List_t (u64 & betree_Message_t)))
@@ -252,7 +275,8 @@ let rec betree_Node_lookup_first_message_for_key
   | Betree_List_Nil -> Return Betree_List_Nil
   end
 
-(** [betree_main::betree::{betree_main::betree::Node#5}::lookup_first_message_for_key]: backward function 0 *)
+(** [betree_main::betree::{betree_main::betree::Node#5}::lookup_first_message_for_key]: backward function 0
+    Source: 'src/betree.rs', lines 789:4-792:34 *)
 let rec betree_Node_lookup_first_message_for_key_back
   (key : u64) (msgs : betree_List_t (u64 & betree_Message_t))
   (ret : betree_List_t (u64 & betree_Message_t)) :
@@ -271,7 +295,8 @@ let rec betree_Node_lookup_first_message_for_key_back
   | Betree_List_Nil -> Return ret
   end
 
-(** [betree_main::betree::{betree_main::betree::Node#5}::apply_upserts]: forward function *)
+(** [betree_main::betree::{betree_main::betree::Node#5}::apply_upserts]: forward function
+    Source: 'src/betree.rs', lines 819:4-819:90 *)
 let rec betree_Node_apply_upserts
   (msgs : betree_List_t (u64 & betree_Message_t)) (prev : option u64)
   (key : u64) (st : state) :
@@ -298,7 +323,8 @@ let rec betree_Node_apply_upserts
         Betree_Message_Insert v) in
     Return (st0, v)
 
-(** [betree_main::betree::{betree_main::betree::Node#5}::apply_upserts]: backward function 0 *)
+(** [betree_main::betree::{betree_main::betree::Node#5}::apply_upserts]: backward function 0
+    Source: 'src/betree.rs', lines 819:4-819:90 *)
 let rec betree_Node_apply_upserts_back
   (msgs : betree_List_t (u64 & betree_Message_t)) (prev : option u64)
   (key : u64) (st : state) (st0 : state) :
@@ -325,7 +351,8 @@ let rec betree_Node_apply_upserts_back
         Betree_Message_Insert v) in
     Return (st0, msgs0)
 
-(** [betree_main::betree::{betree_main::betree::Node#5}::lookup_in_bindings]: forward function *)
+(** [betree_main::betree::{betree_main::betree::Node#5}::lookup_in_bindings]: forward function
+    Source: 'src/betree.rs', lines 636:4-636:80 *)
 let rec betree_Node_lookup_in_bindings
   (key : u64) (bindings : betree_List_t (u64 & u64)) :
   Tot (result (option u64))
@@ -340,7 +367,8 @@ let rec betree_Node_lookup_in_bindings
   | Betree_List_Nil -> Return None
   end
 
-(** [betree_main::betree::{betree_main::betree::Internal#4}::lookup_in_children]: forward function *)
+(** [betree_main::betree::{betree_main::betree::Internal#4}::lookup_in_children]: forward function
+    Source: 'src/betree.rs', lines 395:4-395:63 *)
 let rec betree_Internal_lookup_in_children
   (self : betree_Internal_t) (key : u64) (st : state) :
   Tot (result (state & (option u64)))
@@ -350,7 +378,8 @@ let rec betree_Internal_lookup_in_children
   then betree_Node_lookup self.left key st
   else betree_Node_lookup self.right key st
 
-(** [betree_main::betree::{betree_main::betree::Internal#4}::lookup_in_children]: backward function 0 *)
+(** [betree_main::betree::{betree_main::betree::Internal#4}::lookup_in_children]: backward function 0
+    Source: 'src/betree.rs', lines 395:4-395:63 *)
 and betree_Internal_lookup_in_children_back
   (self : betree_Internal_t) (key : u64) (st : state) (st0 : state) :
   Tot (result (state & betree_Internal_t))
@@ -364,7 +393,8 @@ and betree_Internal_lookup_in_children_back
     let* (st1, n) = betree_Node_lookup_back self.right key st st0 in
     Return (st1, { self with right = n })
 
-(** [betree_main::betree::{betree_main::betree::Node#5}::lookup]: forward function *)
+(** [betree_main::betree::{betree_main::betree::Node#5}::lookup]: forward function
+    Source: 'src/betree.rs', lines 709:4-709:58 *)
 and betree_Node_lookup
   (self : betree_Node_t) (key : u64) (st : state) :
   Tot (result (state & (option u64)))
@@ -424,7 +454,8 @@ and betree_Node_lookup
     Return (st0, o)
   end
 
-(** [betree_main::betree::{betree_main::betree::Node#5}::lookup]: backward function 0 *)
+(** [betree_main::betree::{betree_main::betree::Node#5}::lookup]: backward function 0
+    Source: 'src/betree.rs', lines 709:4-709:58 *)
 and betree_Node_lookup_back
   (self : betree_Node_t) (key : u64) (st : state) (st0 : state) :
   Tot (result (state & betree_Node_t))
@@ -487,7 +518,8 @@ and betree_Node_lookup_back
   end
 
 (** [betree_main::betree::{betree_main::betree::Node#5}::filter_messages_for_key]: merged forward/backward function
-    (there is a single backward function, and the forward function returns ()) *)
+    (there is a single backward function, and the forward function returns ())
+    Source: 'src/betree.rs', lines 674:4-674:77 *)
 let rec betree_Node_filter_messages_for_key
   (key : u64) (msgs : betree_List_t (u64 & betree_Message_t)) :
   Tot (result (betree_List_t (u64 & betree_Message_t)))
@@ -506,7 +538,8 @@ let rec betree_Node_filter_messages_for_key
   | Betree_List_Nil -> Return Betree_List_Nil
   end
 
-(** [betree_main::betree::{betree_main::betree::Node#5}::lookup_first_message_after_key]: forward function *)
+(** [betree_main::betree::{betree_main::betree::Node#5}::lookup_first_message_after_key]: forward function
+    Source: 'src/betree.rs', lines 689:4-692:34 *)
 let rec betree_Node_lookup_first_message_after_key
   (key : u64) (msgs : betree_List_t (u64 & betree_Message_t)) :
   Tot (result (betree_List_t (u64 & betree_Message_t)))
@@ -521,7 +554,8 @@ let rec betree_Node_lookup_first_message_after_key
   | Betree_List_Nil -> Return Betree_List_Nil
   end
 
-(** [betree_main::betree::{betree_main::betree::Node#5}::lookup_first_message_after_key]: backward function 0 *)
+(** [betree_main::betree::{betree_main::betree::Node#5}::lookup_first_message_after_key]: backward function 0
+    Source: 'src/betree.rs', lines 689:4-692:34 *)
 let rec betree_Node_lookup_first_message_after_key_back
   (key : u64) (msgs : betree_List_t (u64 & betree_Message_t))
   (ret : betree_List_t (u64 & betree_Message_t)) :
@@ -541,7 +575,8 @@ let rec betree_Node_lookup_first_message_after_key_back
   end
 
 (** [betree_main::betree::{betree_main::betree::Node#5}::apply_to_internal]: merged forward/backward function
-    (there is a single backward function, and the forward function returns ()) *)
+    (there is a single backward function, and the forward function returns ())
+    Source: 'src/betree.rs', lines 521:4-521:89 *)
 let betree_Node_apply_to_internal
   (msgs : betree_List_t (u64 & betree_Message_t)) (key : u64)
   (new_msg : betree_Message_t) :
@@ -600,7 +635,8 @@ let betree_Node_apply_to_internal
     betree_Node_lookup_first_message_for_key_back key msgs msgs1
 
 (** [betree_main::betree::{betree_main::betree::Node#5}::apply_messages_to_internal]: merged forward/backward function
-    (there is a single backward function, and the forward function returns ()) *)
+    (there is a single backward function, and the forward function returns ())
+    Source: 'src/betree.rs', lines 502:4-505:5 *)
 let rec betree_Node_apply_messages_to_internal
   (msgs : betree_List_t (u64 & betree_Message_t))
   (new_msgs : betree_List_t (u64 & betree_Message_t)) :
@@ -615,7 +651,8 @@ let rec betree_Node_apply_messages_to_internal
   | Betree_List_Nil -> Return msgs
   end
 
-(** [betree_main::betree::{betree_main::betree::Node#5}::lookup_mut_in_bindings]: forward function *)
+(** [betree_main::betree::{betree_main::betree::Node#5}::lookup_mut_in_bindings]: forward function
+    Source: 'src/betree.rs', lines 653:4-656:32 *)
 let rec betree_Node_lookup_mut_in_bindings
   (key : u64) (bindings : betree_List_t (u64 & u64)) :
   Tot (result (betree_List_t (u64 & u64)))
@@ -630,7 +667,8 @@ let rec betree_Node_lookup_mut_in_bindings
   | Betree_List_Nil -> Return Betree_List_Nil
   end
 
-(** [betree_main::betree::{betree_main::betree::Node#5}::lookup_mut_in_bindings]: backward function 0 *)
+(** [betree_main::betree::{betree_main::betree::Node#5}::lookup_mut_in_bindings]: backward function 0
+    Source: 'src/betree.rs', lines 653:4-656:32 *)
 let rec betree_Node_lookup_mut_in_bindings_back
   (key : u64) (bindings : betree_List_t (u64 & u64))
   (ret : betree_List_t (u64 & u64)) :
@@ -649,7 +687,8 @@ let rec betree_Node_lookup_mut_in_bindings_back
   end
 
 (** [betree_main::betree::{betree_main::betree::Node#5}::apply_to_leaf]: merged forward/backward function
-    (there is a single backward function, and the forward function returns ()) *)
+    (there is a single backward function, and the forward function returns ())
+    Source: 'src/betree.rs', lines 460:4-460:87 *)
 let betree_Node_apply_to_leaf
   (bindings : betree_List_t (u64 & u64)) (key : u64)
   (new_msg : betree_Message_t) :
@@ -689,7 +728,8 @@ let betree_Node_apply_to_leaf
     end
 
 (** [betree_main::betree::{betree_main::betree::Node#5}::apply_messages_to_leaf]: merged forward/backward function
-    (there is a single backward function, and the forward function returns ()) *)
+    (there is a single backward function, and the forward function returns ())
+    Source: 'src/betree.rs', lines 444:4-447:5 *)
 let rec betree_Node_apply_messages_to_leaf
   (bindings : betree_List_t (u64 & u64))
   (new_msgs : betree_List_t (u64 & betree_Message_t)) :
@@ -704,7 +744,8 @@ let rec betree_Node_apply_messages_to_leaf
   | Betree_List_Nil -> Return bindings
   end
 
-(** [betree_main::betree::{betree_main::betree::Internal#4}::flush]: forward function *)
+(** [betree_main::betree::{betree_main::betree::Internal#4}::flush]: forward function
+    Source: 'src/betree.rs', lines 410:4-415:26 *)
 let rec betree_Internal_flush
   (self : betree_Internal_t) (params : betree_Params_t)
   (node_id_cnt : betree_NodeIdCounter_t)
@@ -753,7 +794,8 @@ let rec betree_Internal_flush
         st st1 in
     Return (st2, msgs_left)
 
-(** [betree_main::betree::{betree_main::betree::Internal#4}::flush]: backward function 0 *)
+(** [betree_main::betree::{betree_main::betree::Internal#4}::flush]: backward function 0
+    Source: 'src/betree.rs', lines 410:4-415:26 *)
 and betree_Internal_flush_back'a
   (self : betree_Internal_t) (params : betree_Params_t)
   (node_id_cnt : betree_NodeIdCounter_t)
@@ -803,7 +845,8 @@ and betree_Internal_flush_back'a
         st st2 in
     Return (st0, ({ self with right = n }, node_id_cnt0))
 
-(** [betree_main::betree::{betree_main::betree::Internal#4}::flush]: backward function 1 *)
+(** [betree_main::betree::{betree_main::betree::Internal#4}::flush]: backward function 1
+    Source: 'src/betree.rs', lines 410:4-415:26 *)
 and betree_Internal_flush_back1
   (self : betree_Internal_t) (params : betree_Params_t)
   (node_id_cnt : betree_NodeIdCounter_t)
@@ -853,7 +896,8 @@ and betree_Internal_flush_back1
         st st2 in
     Return (st0, ())
 
-(** [betree_main::betree::{betree_main::betree::Node#5}::apply_messages]: forward function *)
+(** [betree_main::betree::{betree_main::betree::Node#5}::apply_messages]: forward function
+    Source: 'src/betree.rs', lines 588:4-593:5 *)
 and betree_Node_apply_messages
   (self : betree_Node_t) (params : betree_Params_t)
   (node_id_cnt : betree_NodeIdCounter_t)
@@ -894,7 +938,8 @@ and betree_Node_apply_messages
       Return (st1, ())
   end
 
-(** [betree_main::betree::{betree_main::betree::Node#5}::apply_messages]: backward function 0 *)
+(** [betree_main::betree::{betree_main::betree::Node#5}::apply_messages]: backward function 0
+    Source: 'src/betree.rs', lines 588:4-593:5 *)
 and betree_Node_apply_messages_back'a
   (self : betree_Node_t) (params : betree_Params_t)
   (node_id_cnt : betree_NodeIdCounter_t)
@@ -940,7 +985,8 @@ and betree_Node_apply_messages_back'a
       Return (st0, (Betree_Node_Leaf { node with size = len }, node_id_cnt))
   end
 
-(** [betree_main::betree::{betree_main::betree::Node#5}::apply_messages]: backward function 1 *)
+(** [betree_main::betree::{betree_main::betree::Node#5}::apply_messages]: backward function 1
+    Source: 'src/betree.rs', lines 588:4-593:5 *)
 and betree_Node_apply_messages_back1
   (self : betree_Node_t) (params : betree_Params_t)
   (node_id_cnt : betree_NodeIdCounter_t)
@@ -982,7 +1028,8 @@ and betree_Node_apply_messages_back1
       let* _ = betree_store_leaf_node node.id content0 st1 in Return (st0, ())
   end
 
-(** [betree_main::betree::{betree_main::betree::Node#5}::apply]: forward function *)
+(** [betree_main::betree::{betree_main::betree::Node#5}::apply]: forward function
+    Source: 'src/betree.rs', lines 576:4-582:5 *)
 let betree_Node_apply
   (self : betree_Node_t) (params : betree_Params_t)
   (node_id_cnt : betree_NodeIdCounter_t) (key : u64)
@@ -999,7 +1046,8 @@ let betree_Node_apply
   betree_Node_apply_messages_back1 self params node_id_cnt (Betree_List_Cons
     (key, new_msg) l) st st1
 
-(** [betree_main::betree::{betree_main::betree::Node#5}::apply]: backward function 0 *)
+(** [betree_main::betree::{betree_main::betree::Node#5}::apply]: backward function 0
+    Source: 'src/betree.rs', lines 576:4-582:5 *)
 let betree_Node_apply_back'a
   (self : betree_Node_t) (params : betree_Params_t)
   (node_id_cnt : betree_NodeIdCounter_t) (key : u64)
@@ -1018,7 +1066,8 @@ let betree_Node_apply_back'a
       (key, new_msg) l) st st2 in
   Return (st0, (self0, node_id_cnt0))
 
-(** [betree_main::betree::{betree_main::betree::Node#5}::apply]: backward function 1 *)
+(** [betree_main::betree::{betree_main::betree::Node#5}::apply]: backward function 1
+    Source: 'src/betree.rs', lines 576:4-582:5 *)
 let betree_Node_apply_back1
   (self : betree_Node_t) (params : betree_Params_t)
   (node_id_cnt : betree_NodeIdCounter_t) (key : u64)
@@ -1037,7 +1086,8 @@ let betree_Node_apply_back1
       (key, new_msg) l) st st2 in
   Return (st0, ())
 
-(** [betree_main::betree::{betree_main::betree::BeTree#6}::new]: forward function *)
+(** [betree_main::betree::{betree_main::betree::BeTree#6}::new]: forward function
+    Source: 'src/betree.rs', lines 849:4-849:60 *)
 let betree_BeTree_new
   (min_flush_size : u64) (split_size : u64) (st : state) :
   result (state & betree_BeTree_t)
@@ -1053,7 +1103,8 @@ let betree_BeTree_new
       root = (Betree_Node_Leaf { id = id; size = 0 })
     })
 
-(** [betree_main::betree::{betree_main::betree::BeTree#6}::apply]: forward function *)
+(** [betree_main::betree::{betree_main::betree::BeTree#6}::apply]: forward function
+    Source: 'src/betree.rs', lines 868:4-868:47 *)
 let betree_BeTree_apply
   (self : betree_BeTree_t) (key : u64) (msg : betree_Message_t) (st : state) :
   result (state & unit)
@@ -1065,7 +1116,8 @@ let betree_BeTree_apply
       st0 in
   betree_Node_apply_back1 self.root self.params self.node_id_cnt key msg st st1
 
-(** [betree_main::betree::{betree_main::betree::BeTree#6}::apply]: backward function 0 *)
+(** [betree_main::betree::{betree_main::betree::BeTree#6}::apply]: backward function 0
+    Source: 'src/betree.rs', lines 868:4-868:47 *)
 let betree_BeTree_apply_back
   (self : betree_BeTree_t) (key : u64) (msg : betree_Message_t) (st : state)
   (st0 : state) :
@@ -1081,7 +1133,8 @@ let betree_BeTree_apply_back
       st2 in
   Return (st0, { self with node_id_cnt = nic; root = n })
 
-(** [betree_main::betree::{betree_main::betree::BeTree#6}::insert]: forward function *)
+(** [betree_main::betree::{betree_main::betree::BeTree#6}::insert]: forward function
+    Source: 'src/betree.rs', lines 874:4-874:52 *)
 let betree_BeTree_insert
   (self : betree_BeTree_t) (key : u64) (value : u64) (st : state) :
   result (state & unit)
@@ -1092,7 +1145,8 @@ let betree_BeTree_insert
     betree_BeTree_apply_back self key (Betree_Message_Insert value) st st0 in
   Return (st1, ())
 
-(** [betree_main::betree::{betree_main::betree::BeTree#6}::insert]: backward function 0 *)
+(** [betree_main::betree::{betree_main::betree::BeTree#6}::insert]: backward function 0
+    Source: 'src/betree.rs', lines 874:4-874:52 *)
 let betree_BeTree_insert_back
   (self : betree_BeTree_t) (key : u64) (value : u64) (st : state) (st0 : state)
   :
@@ -1104,7 +1158,8 @@ let betree_BeTree_insert_back
     betree_BeTree_apply_back self key (Betree_Message_Insert value) st st1 in
   Return (st0, self0)
 
-(** [betree_main::betree::{betree_main::betree::BeTree#6}::delete]: forward function *)
+(** [betree_main::betree::{betree_main::betree::BeTree#6}::delete]: forward function
+    Source: 'src/betree.rs', lines 880:4-880:38 *)
 let betree_BeTree_delete
   (self : betree_BeTree_t) (key : u64) (st : state) : result (state & unit) =
   let* (st0, _) = betree_BeTree_apply self key Betree_Message_Delete st in
@@ -1112,7 +1167,8 @@ let betree_BeTree_delete
     betree_BeTree_apply_back self key Betree_Message_Delete st st0 in
   Return (st1, ())
 
-(** [betree_main::betree::{betree_main::betree::BeTree#6}::delete]: backward function 0 *)
+(** [betree_main::betree::{betree_main::betree::BeTree#6}::delete]: backward function 0
+    Source: 'src/betree.rs', lines 880:4-880:38 *)
 let betree_BeTree_delete_back
   (self : betree_BeTree_t) (key : u64) (st : state) (st0 : state) :
   result (state & betree_BeTree_t)
@@ -1122,7 +1178,8 @@ let betree_BeTree_delete_back
     betree_BeTree_apply_back self key Betree_Message_Delete st st1 in
   Return (st0, self0)
 
-(** [betree_main::betree::{betree_main::betree::BeTree#6}::upsert]: forward function *)
+(** [betree_main::betree::{betree_main::betree::BeTree#6}::upsert]: forward function
+    Source: 'src/betree.rs', lines 886:4-886:59 *)
 let betree_BeTree_upsert
   (self : betree_BeTree_t) (key : u64) (upd : betree_UpsertFunState_t)
   (st : state) :
@@ -1134,7 +1191,8 @@ let betree_BeTree_upsert
     betree_BeTree_apply_back self key (Betree_Message_Upsert upd) st st0 in
   Return (st1, ())
 
-(** [betree_main::betree::{betree_main::betree::BeTree#6}::upsert]: backward function 0 *)
+(** [betree_main::betree::{betree_main::betree::BeTree#6}::upsert]: backward function 0
+    Source: 'src/betree.rs', lines 886:4-886:59 *)
 let betree_BeTree_upsert_back
   (self : betree_BeTree_t) (key : u64) (upd : betree_UpsertFunState_t)
   (st : state) (st0 : state) :
@@ -1146,14 +1204,16 @@ let betree_BeTree_upsert_back
     betree_BeTree_apply_back self key (Betree_Message_Upsert upd) st st1 in
   Return (st0, self0)
 
-(** [betree_main::betree::{betree_main::betree::BeTree#6}::lookup]: forward function *)
+(** [betree_main::betree::{betree_main::betree::BeTree#6}::lookup]: forward function
+    Source: 'src/betree.rs', lines 895:4-895:62 *)
 let betree_BeTree_lookup
   (self : betree_BeTree_t) (key : u64) (st : state) :
   result (state & (option u64))
   =
   betree_Node_lookup self.root key st
 
-(** [betree_main::betree::{betree_main::betree::BeTree#6}::lookup]: backward function 0 *)
+(** [betree_main::betree::{betree_main::betree::BeTree#6}::lookup]: backward function 0
+    Source: 'src/betree.rs', lines 895:4-895:62 *)
 let betree_BeTree_lookup_back
   (self : betree_BeTree_t) (key : u64) (st : state) (st0 : state) :
   result (state & betree_BeTree_t)
@@ -1161,7 +1221,8 @@ let betree_BeTree_lookup_back
   let* (st1, n) = betree_Node_lookup_back self.root key st st0 in
   Return (st1, { self with root = n })
 
-(** [betree_main::main]: forward function *)
+(** [betree_main::main]: forward function
+    Source: 'src/betree_main.rs', lines 5:0-5:9 *)
 let main : result unit =
   Return ()
 
diff --git a/tests/fstar/betree_back_stateful/BetreeMain.Opaque.fsti b/tests/fstar/betree_back_stateful/BetreeMain.Opaque.fsti
index 23d2e60e..b89c8718 100644
--- a/tests/fstar/betree_back_stateful/BetreeMain.Opaque.fsti
+++ b/tests/fstar/betree_back_stateful/BetreeMain.Opaque.fsti
@@ -6,25 +6,30 @@ include BetreeMain.Types
 
 #set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
 
-(** [betree_main::betree_utils::load_internal_node]: forward function *)
+(** [betree_main::betree_utils::load_internal_node]: forward function
+    Source: 'src/betree_utils.rs', lines 98:0-98:63 *)
 val betree_utils_load_internal_node
   : u64 -> state -> result (state & (betree_List_t (u64 & betree_Message_t)))
 
-(** [betree_main::betree_utils::store_internal_node]: forward function *)
+(** [betree_main::betree_utils::store_internal_node]: forward function
+    Source: 'src/betree_utils.rs', lines 115:0-115:71 *)
 val betree_utils_store_internal_node
   :
   u64 -> betree_List_t (u64 & betree_Message_t) -> state -> result (state &
     unit)
 
-(** [betree_main::betree_utils::load_leaf_node]: forward function *)
+(** [betree_main::betree_utils::load_leaf_node]: forward function
+    Source: 'src/betree_utils.rs', lines 132:0-132:55 *)
 val betree_utils_load_leaf_node
   : u64 -> state -> result (state & (betree_List_t (u64 & u64)))
 
-(** [betree_main::betree_utils::store_leaf_node]: forward function *)
+(** [betree_main::betree_utils::store_leaf_node]: forward function
+    Source: 'src/betree_utils.rs', lines 145:0-145:63 *)
 val betree_utils_store_leaf_node
   : u64 -> betree_List_t (u64 & u64) -> state -> result (state & unit)
 
-(** [core::option::{core::option::Option<T>}::unwrap]: forward function *)
+(** [core::option::{core::option::Option<T>}::unwrap]: forward function
+    Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/option.rs', lines 932:4-932:34 *)
 val core_option_Option_unwrap
   (t : Type0) : option t -> state -> result (state & t)
 
diff --git a/tests/fstar/betree_back_stateful/BetreeMain.Types.fsti b/tests/fstar/betree_back_stateful/BetreeMain.Types.fsti
index 9320f6b7..a098ec19 100644
--- a/tests/fstar/betree_back_stateful/BetreeMain.Types.fsti
+++ b/tests/fstar/betree_back_stateful/BetreeMain.Types.fsti
@@ -5,43 +5,52 @@ open Primitives
 
 #set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
 
-(** [betree_main::betree::List] *)
+(** [betree_main::betree::List]
+    Source: 'src/betree.rs', lines 17:0-17:23 *)
 type betree_List_t (t : Type0) =
 | Betree_List_Cons : t -> betree_List_t t -> betree_List_t t
 | Betree_List_Nil : betree_List_t t
 
-(** [betree_main::betree::UpsertFunState] *)
+(** [betree_main::betree::UpsertFunState]
+    Source: 'src/betree.rs', lines 63:0-63:23 *)
 type betree_UpsertFunState_t =
 | Betree_UpsertFunState_Add : u64 -> betree_UpsertFunState_t
 | Betree_UpsertFunState_Sub : u64 -> betree_UpsertFunState_t
 
-(** [betree_main::betree::Message] *)
+(** [betree_main::betree::Message]
+    Source: 'src/betree.rs', lines 69:0-69:23 *)
 type betree_Message_t =
 | Betree_Message_Insert : u64 -> betree_Message_t
 | Betree_Message_Delete : betree_Message_t
 | Betree_Message_Upsert : betree_UpsertFunState_t -> betree_Message_t
 
-(** [betree_main::betree::Leaf] *)
+(** [betree_main::betree::Leaf]
+    Source: 'src/betree.rs', lines 167:0-167:11 *)
 type betree_Leaf_t = { id : u64; size : u64; }
 
-(** [betree_main::betree::Internal] *)
+(** [betree_main::betree::Internal]
+    Source: 'src/betree.rs', lines 156:0-156:15 *)
 type betree_Internal_t =
 {
   id : u64; pivot : u64; left : betree_Node_t; right : betree_Node_t;
 }
 
-(** [betree_main::betree::Node] *)
+(** [betree_main::betree::Node]
+    Source: 'src/betree.rs', lines 179:0-179:9 *)
 and betree_Node_t =
 | Betree_Node_Internal : betree_Internal_t -> betree_Node_t
 | Betree_Node_Leaf : betree_Leaf_t -> betree_Node_t
 
-(** [betree_main::betree::Params] *)
+(** [betree_main::betree::Params]
+    Source: 'src/betree.rs', lines 187:0-187:13 *)
 type betree_Params_t = { min_flush_size : u64; split_size : u64; }
 
-(** [betree_main::betree::NodeIdCounter] *)
+(** [betree_main::betree::NodeIdCounter]
+    Source: 'src/betree.rs', lines 201:0-201:20 *)
 type betree_NodeIdCounter_t = { next_node_id : u64; }
 
-(** [betree_main::betree::BeTree] *)
+(** [betree_main::betree::BeTree]
+    Source: 'src/betree.rs', lines 218:0-218:17 *)
 type betree_BeTree_t =
 {
   params : betree_Params_t;