diff options
Diffstat (limited to 'tests/fstar/betree_back_stateful')
| -rw-r--r-- | tests/fstar/betree_back_stateful/BetreeMain.Funs.fst | 128 | ||||
| -rw-r--r-- | tests/fstar/betree_back_stateful/BetreeMain.Opaque.fsti | 12 |
2 files changed, 73 insertions, 67 deletions
diff --git a/tests/fstar/betree_back_stateful/BetreeMain.Funs.fst b/tests/fstar/betree_back_stateful/BetreeMain.Funs.fst index c70bef08..12402fb4 100644 --- a/tests/fstar/betree_back_stateful/BetreeMain.Funs.fst +++ b/tests/fstar/betree_back_stateful/BetreeMain.Funs.fst @@ -8,14 +8,14 @@ include BetreeMain.Clauses #set-options "--z3rlimit 50 --fuel 1 --ifuel 1" -(** [betree_main::betree::load_internal_node] *) +(** [betree_main::betree::load_internal_node]: forward function *) let betree_load_internal_node_fwd (id : u64) (st : state) : result (state & (betree_list_t (u64 & betree_message_t))) = betree_utils_load_internal_node_fwd id st -(** [betree_main::betree::store_internal_node] *) +(** [betree_main::betree::store_internal_node]: forward function *) let betree_store_internal_node_fwd (id : u64) (content : betree_list_t (u64 & betree_message_t)) (st : state) : result (state & unit) @@ -23,12 +23,12 @@ let betree_store_internal_node_fwd let* (st0, _) = betree_utils_store_internal_node_fwd id content st in Return (st0, ()) -(** [betree_main::betree::load_leaf_node] *) +(** [betree_main::betree::load_leaf_node]: forward function *) let betree_load_leaf_node_fwd (id : u64) (st : state) : result (state & (betree_list_t (u64 & u64))) = betree_utils_load_leaf_node_fwd id st -(** [betree_main::betree::store_leaf_node] *) +(** [betree_main::betree::store_leaf_node]: forward function *) let betree_store_leaf_node_fwd (id : u64) (content : betree_list_t (u64 & u64)) (st : state) : result (state & unit) @@ -36,25 +36,25 @@ let betree_store_leaf_node_fwd let* (st0, _) = betree_utils_store_leaf_node_fwd id content st in Return (st0, ()) -(** [betree_main::betree::fresh_node_id] *) +(** [betree_main::betree::fresh_node_id]: forward function *) let betree_fresh_node_id_fwd (counter : u64) : result u64 = let* _ = u64_add counter 1 in Return counter -(** [betree_main::betree::fresh_node_id] *) +(** [betree_main::betree::fresh_node_id]: backward function 0 *) let betree_fresh_node_id_back (counter : u64) : result u64 = u64_add counter 1 -(** [betree_main::betree::NodeIdCounter::{0}::new] *) +(** [betree_main::betree::NodeIdCounter::{0}::new]: forward function *) let betree_node_id_counter_new_fwd : result betree_node_id_counter_t = Return { betree_node_id_counter_next_node_id = 0 } -(** [betree_main::betree::NodeIdCounter::{0}::fresh_id] *) +(** [betree_main::betree::NodeIdCounter::{0}::fresh_id]: forward function *) let betree_node_id_counter_fresh_id_fwd (self : betree_node_id_counter_t) : result u64 = let* _ = u64_add self.betree_node_id_counter_next_node_id 1 in Return self.betree_node_id_counter_next_node_id -(** [betree_main::betree::NodeIdCounter::{0}::fresh_id] *) +(** [betree_main::betree::NodeIdCounter::{0}::fresh_id]: backward function 0 *) let betree_node_id_counter_fresh_id_back (self : betree_node_id_counter_t) : result betree_node_id_counter_t = let* i = u64_add self.betree_node_id_counter_next_node_id 1 in @@ -64,7 +64,7 @@ let betree_node_id_counter_fresh_id_back let core_num_u64_max_body : result u64 = Return 18446744073709551615 let core_num_u64_max_c : u64 = eval_global core_num_u64_max_body -(** [betree_main::betree::upsert_update] *) +(** [betree_main::betree::upsert_update]: forward function *) let betree_upsert_update_fwd (prev : option u64) (st : betree_upsert_fun_state_t) : result u64 = begin match prev with @@ -83,7 +83,7 @@ let betree_upsert_update_fwd end end -(** [betree_main::betree::List::{1}::len] *) +(** [betree_main::betree::List::{1}::len]: forward function *) let rec betree_list_len_fwd (t : Type0) (self : betree_list_t t) : Tot (result u64) (decreases (betree_list_len_decreases t self)) @@ -93,7 +93,7 @@ let rec betree_list_len_fwd | BetreeListNil -> Return 0 end -(** [betree_main::betree::List::{1}::split_at] *) +(** [betree_main::betree::List::{1}::split_at]: forward function *) let rec betree_list_split_at_fwd (t : Type0) (self : betree_list_t t) (n : u64) : Tot (result ((betree_list_t t) & (betree_list_t t))) @@ -112,14 +112,15 @@ let rec betree_list_split_at_fwd | BetreeListNil -> Fail Failure end -(** [betree_main::betree::List::{1}::push_front] *) +(** [betree_main::betree::List::{1}::push_front]: merged forward/backward function + (there is a single backward function, and the forward function returns ()) *) let betree_list_push_front_fwd_back (t : Type0) (self : betree_list_t t) (x : t) : result (betree_list_t t) = let tl = mem_replace_fwd (betree_list_t t) self BetreeListNil in let l = tl in Return (BetreeListCons x l) -(** [betree_main::betree::List::{1}::pop_front] *) +(** [betree_main::betree::List::{1}::pop_front]: forward function *) let betree_list_pop_front_fwd (t : Type0) (self : betree_list_t t) : result t = let ls = mem_replace_fwd (betree_list_t t) self BetreeListNil in begin match ls with @@ -127,7 +128,7 @@ let betree_list_pop_front_fwd (t : Type0) (self : betree_list_t t) : result t = | BetreeListNil -> Fail Failure end -(** [betree_main::betree::List::{1}::pop_front] *) +(** [betree_main::betree::List::{1}::pop_front]: backward function 0 *) let betree_list_pop_front_back (t : Type0) (self : betree_list_t t) : result (betree_list_t t) = let ls = mem_replace_fwd (betree_list_t t) self BetreeListNil in @@ -136,14 +137,14 @@ let betree_list_pop_front_back | BetreeListNil -> Fail Failure end -(** [betree_main::betree::List::{1}::hd] *) +(** [betree_main::betree::List::{1}::hd]: forward function *) let betree_list_hd_fwd (t : Type0) (self : betree_list_t t) : result t = begin match self with | BetreeListCons hd l -> Return hd | BetreeListNil -> Fail Failure end -(** [betree_main::betree::List::{2}::head_has_key] *) +(** [betree_main::betree::List::{2}::head_has_key]: forward function *) let betree_list_head_has_key_fwd (t : Type0) (self : betree_list_t (u64 & t)) (key : u64) : result bool = begin match self with @@ -151,7 +152,7 @@ let betree_list_head_has_key_fwd | BetreeListNil -> Return false end -(** [betree_main::betree::List::{2}::partition_at_pivot] *) +(** [betree_main::betree::List::{2}::partition_at_pivot]: forward function *) let rec betree_list_partition_at_pivot_fwd (t : Type0) (self : betree_list_t (u64 & t)) (pivot : u64) : Tot (result ((betree_list_t (u64 & t)) & (betree_list_t (u64 & t)))) @@ -170,7 +171,7 @@ let rec betree_list_partition_at_pivot_fwd | BetreeListNil -> Return (BetreeListNil, BetreeListNil) end -(** [betree_main::betree::Leaf::{3}::split] *) +(** [betree_main::betree::Leaf::{3}::split]: forward function *) let betree_leaf_split_fwd (self : betree_leaf_t) (content : betree_list_t (u64 & u64)) (params : betree_params_t) (node_id_cnt : betree_node_id_counter_t) @@ -202,7 +203,7 @@ let betree_leaf_split_fwd betree_internal_right = n0 }) -(** [betree_main::betree::Leaf::{3}::split] *) +(** [betree_main::betree::Leaf::{3}::split]: backward function 0 *) let betree_leaf_split_back0 (self : betree_leaf_t) (content : betree_list_t (u64 & u64)) (params : betree_params_t) (node_id_cnt : betree_node_id_counter_t) @@ -221,7 +222,7 @@ let betree_leaf_split_back0 let* _ = betree_store_leaf_node_fwd id1 content1 st1 in Return (st0, ()) -(** [betree_main::betree::Leaf::{3}::split] *) +(** [betree_main::betree::Leaf::{3}::split]: backward function 1 *) let betree_leaf_split_back1 (self : betree_leaf_t) (content : betree_list_t (u64 & u64)) (params : betree_params_t) (node_id_cnt : betree_node_id_counter_t) @@ -240,7 +241,7 @@ let betree_leaf_split_back1 let* _ = betree_store_leaf_node_fwd id1 content1 st1 in Return (st0, ()) -(** [betree_main::betree::Leaf::{3}::split] *) +(** [betree_main::betree::Leaf::{3}::split]: backward function 2 *) let betree_leaf_split_back2 (self : betree_leaf_t) (content : betree_list_t (u64 & u64)) (params : betree_params_t) (node_id_cnt : betree_node_id_counter_t) @@ -260,7 +261,7 @@ let betree_leaf_split_back2 let* node_id_cnt1 = betree_node_id_counter_fresh_id_back node_id_cnt0 in Return (st0, node_id_cnt1) -(** [betree_main::betree::Node::{5}::lookup_in_bindings] *) +(** [betree_main::betree::Node::{5}::lookup_in_bindings]: forward function *) let rec betree_node_lookup_in_bindings_fwd (key : u64) (bindings : betree_list_t (u64 & u64)) : Tot (result (option u64)) @@ -278,7 +279,7 @@ let rec betree_node_lookup_in_bindings_fwd | BetreeListNil -> Return None end -(** [betree_main::betree::Node::{5}::lookup_first_message_for_key] *) +(** [betree_main::betree::Node::{5}::lookup_first_message_for_key]: forward function *) let rec betree_node_lookup_first_message_for_key_fwd (key : u64) (msgs : betree_list_t (u64 & betree_message_t)) : Tot (result (betree_list_t (u64 & betree_message_t))) @@ -293,7 +294,7 @@ let rec betree_node_lookup_first_message_for_key_fwd | BetreeListNil -> Return BetreeListNil end -(** [betree_main::betree::Node::{5}::lookup_first_message_for_key] *) +(** [betree_main::betree::Node::{5}::lookup_first_message_for_key]: backward function 0 *) 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)) : @@ -312,7 +313,7 @@ let rec betree_node_lookup_first_message_for_key_back | BetreeListNil -> Return ret end -(** [betree_main::betree::Node::{5}::apply_upserts] *) +(** [betree_main::betree::Node::{5}::apply_upserts]: forward function *) let rec betree_node_apply_upserts_fwd (msgs : betree_list_t (u64 & betree_message_t)) (prev : option u64) (key : u64) (st : state) : @@ -339,7 +340,7 @@ let rec betree_node_apply_upserts_fwd BetreeMessageInsert v) in Return (st0, v) -(** [betree_main::betree::Node::{5}::apply_upserts] *) +(** [betree_main::betree::Node::{5}::apply_upserts]: backward function 0 *) let rec betree_node_apply_upserts_back (msgs : betree_list_t (u64 & betree_message_t)) (prev : option u64) (key : u64) (st : state) (st0 : state) : @@ -366,7 +367,7 @@ let rec betree_node_apply_upserts_back BetreeMessageInsert v) in Return (st0, msgs0) -(** [betree_main::betree::Node::{5}::lookup] *) +(** [betree_main::betree::Node::{5}::lookup]: forward function *) let rec betree_node_lookup_fwd (self : betree_node_t) (key : u64) (st : state) : Tot (result (state & (option u64))) @@ -430,7 +431,7 @@ let rec betree_node_lookup_fwd Return (st0, opt) end -(** [betree_main::betree::Node::{5}::lookup] *) +(** [betree_main::betree::Node::{5}::lookup]: backward function 0 *) and betree_node_lookup_back (self : betree_node_t) (key : u64) (st : state) (st0 : state) : Tot (result (state & betree_node_t)) @@ -495,7 +496,7 @@ and betree_node_lookup_back Return (st0, BetreeNodeLeaf node) end -(** [betree_main::betree::Internal::{4}::lookup_in_children] *) +(** [betree_main::betree::Internal::{4}::lookup_in_children]: forward function *) and betree_internal_lookup_in_children_fwd (self : betree_internal_t) (key : u64) (st : state) : Tot (result (state & (option u64))) @@ -505,7 +506,7 @@ and betree_internal_lookup_in_children_fwd then betree_node_lookup_fwd self.betree_internal_left key st else betree_node_lookup_fwd self.betree_internal_right key st -(** [betree_main::betree::Internal::{4}::lookup_in_children] *) +(** [betree_main::betree::Internal::{4}::lookup_in_children]: backward function 0 *) and betree_internal_lookup_in_children_back (self : betree_internal_t) (key : u64) (st : state) (st0 : state) : Tot (result (state & betree_internal_t)) @@ -521,7 +522,7 @@ and betree_internal_lookup_in_children_back betree_node_lookup_back self.betree_internal_right key st st0 in Return (st1, { self with betree_internal_right = n }) -(** [betree_main::betree::Node::{5}::lookup_mut_in_bindings] *) +(** [betree_main::betree::Node::{5}::lookup_mut_in_bindings]: forward function *) let rec betree_node_lookup_mut_in_bindings_fwd (key : u64) (bindings : betree_list_t (u64 & u64)) : Tot (result (betree_list_t (u64 & u64))) @@ -536,7 +537,7 @@ let rec betree_node_lookup_mut_in_bindings_fwd | BetreeListNil -> Return BetreeListNil end -(** [betree_main::betree::Node::{5}::lookup_mut_in_bindings] *) +(** [betree_main::betree::Node::{5}::lookup_mut_in_bindings]: backward function 0 *) let rec betree_node_lookup_mut_in_bindings_back (key : u64) (bindings : betree_list_t (u64 & u64)) (ret : betree_list_t (u64 & u64)) : @@ -554,7 +555,8 @@ let rec betree_node_lookup_mut_in_bindings_back | BetreeListNil -> Return ret end -(** [betree_main::betree::Node::{5}::apply_to_leaf] *) +(** [betree_main::betree::Node::{5}::apply_to_leaf]: merged forward/backward function + (there is a single backward function, and the forward function returns ()) *) let betree_node_apply_to_leaf_fwd_back (bindings : betree_list_t (u64 & u64)) (key : u64) (new_msg : betree_message_t) : @@ -597,7 +599,8 @@ let betree_node_apply_to_leaf_fwd_back betree_node_lookup_mut_in_bindings_back key bindings bindings1 end -(** [betree_main::betree::Node::{5}::apply_messages_to_leaf] *) +(** [betree_main::betree::Node::{5}::apply_messages_to_leaf]: merged forward/backward function + (there is a single backward function, and the forward function returns ()) *) let rec betree_node_apply_messages_to_leaf_fwd_back (bindings : betree_list_t (u64 & u64)) (new_msgs : betree_list_t (u64 & betree_message_t)) : @@ -612,7 +615,8 @@ let rec betree_node_apply_messages_to_leaf_fwd_back | BetreeListNil -> Return bindings end -(** [betree_main::betree::Node::{5}::filter_messages_for_key] *) +(** [betree_main::betree::Node::{5}::filter_messages_for_key]: merged forward/backward function + (there is a single backward function, and the forward function returns ()) *) let rec betree_node_filter_messages_for_key_fwd_back (key : u64) (msgs : betree_list_t (u64 & betree_message_t)) : Tot (result (betree_list_t (u64 & betree_message_t))) @@ -631,7 +635,7 @@ let rec betree_node_filter_messages_for_key_fwd_back | BetreeListNil -> Return BetreeListNil end -(** [betree_main::betree::Node::{5}::lookup_first_message_after_key] *) +(** [betree_main::betree::Node::{5}::lookup_first_message_after_key]: forward function *) let rec betree_node_lookup_first_message_after_key_fwd (key : u64) (msgs : betree_list_t (u64 & betree_message_t)) : Tot (result (betree_list_t (u64 & betree_message_t))) @@ -646,7 +650,7 @@ let rec betree_node_lookup_first_message_after_key_fwd | BetreeListNil -> Return BetreeListNil end -(** [betree_main::betree::Node::{5}::lookup_first_message_after_key] *) +(** [betree_main::betree::Node::{5}::lookup_first_message_after_key]: backward function 0 *) 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)) : @@ -665,7 +669,8 @@ let rec betree_node_lookup_first_message_after_key_back | BetreeListNil -> Return ret end -(** [betree_main::betree::Node::{5}::apply_to_internal] *) +(** [betree_main::betree::Node::{5}::apply_to_internal]: merged forward/backward function + (there is a single backward function, and the forward function returns ()) *) let betree_node_apply_to_internal_fwd_back (msgs : betree_list_t (u64 & betree_message_t)) (key : u64) (new_msg : betree_message_t) : @@ -725,7 +730,8 @@ let betree_node_apply_to_internal_fwd_back new_msg) in betree_node_lookup_first_message_for_key_back key msgs msgs1 -(** [betree_main::betree::Node::{5}::apply_messages_to_internal] *) +(** [betree_main::betree::Node::{5}::apply_messages_to_internal]: merged forward/backward function + (there is a single backward function, and the forward function returns ()) *) let rec betree_node_apply_messages_to_internal_fwd_back (msgs : betree_list_t (u64 & betree_message_t)) (new_msgs : betree_list_t (u64 & betree_message_t)) : @@ -740,7 +746,7 @@ let rec betree_node_apply_messages_to_internal_fwd_back | BetreeListNil -> Return msgs end -(** [betree_main::betree::Node::{5}::apply_messages] *) +(** [betree_main::betree::Node::{5}::apply_messages]: forward function *) let rec betree_node_apply_messages_fwd (self : betree_node_t) (params : betree_params_t) (node_id_cnt : betree_node_id_counter_t) @@ -788,7 +794,7 @@ let rec betree_node_apply_messages_fwd Return (st1, ()) end -(** [betree_main::betree::Node::{5}::apply_messages] *) +(** [betree_main::betree::Node::{5}::apply_messages]: backward function 0 *) and betree_node_apply_messages_back'a (self : betree_node_t) (params : betree_params_t) (node_id_cnt : betree_node_id_counter_t) @@ -840,7 +846,7 @@ and betree_node_apply_messages_back'a node_id_cnt)) end -(** [betree_main::betree::Node::{5}::apply_messages] *) +(** [betree_main::betree::Node::{5}::apply_messages]: backward function 1 *) and betree_node_apply_messages_back1 (self : betree_node_t) (params : betree_params_t) (node_id_cnt : betree_node_id_counter_t) @@ -889,7 +895,7 @@ and betree_node_apply_messages_back1 Return (st0, ()) end -(** [betree_main::betree::Internal::{4}::flush] *) +(** [betree_main::betree::Internal::{4}::flush]: forward function *) and betree_internal_flush_fwd (self : betree_internal_t) (params : betree_params_t) (node_id_cnt : betree_node_id_counter_t) @@ -940,7 +946,7 @@ and betree_internal_flush_fwd node_id_cnt msgs_right st st1 in Return (st2, msgs_left) -(** [betree_main::betree::Internal::{4}::flush] *) +(** [betree_main::betree::Internal::{4}::flush]: backward function 0 *) and betree_internal_flush_back'a (self : betree_internal_t) (params : betree_params_t) (node_id_cnt : betree_node_id_counter_t) @@ -994,7 +1000,7 @@ and betree_internal_flush_back'a node_id_cnt msgs_right st st2 in Return (st0, ({ self with betree_internal_right = n }, node_id_cnt0)) -(** [betree_main::betree::Internal::{4}::flush] *) +(** [betree_main::betree::Internal::{4}::flush]: backward function 1 *) and betree_internal_flush_back1 (self : betree_internal_t) (params : betree_params_t) (node_id_cnt : betree_node_id_counter_t) @@ -1046,7 +1052,7 @@ and betree_internal_flush_back1 node_id_cnt msgs_right st st2 in Return (st0, ()) -(** [betree_main::betree::Node::{5}::apply] *) +(** [betree_main::betree::Node::{5}::apply]: forward function *) let betree_node_apply_fwd (self : betree_node_t) (params : betree_params_t) (node_id_cnt : betree_node_id_counter_t) (key : u64) @@ -1063,7 +1069,7 @@ let betree_node_apply_fwd betree_node_apply_messages_back1 self params node_id_cnt (BetreeListCons (key, new_msg) l) st st1 -(** [betree_main::betree::Node::{5}::apply] *) +(** [betree_main::betree::Node::{5}::apply]: backward function 0 *) let betree_node_apply_back'a (self : betree_node_t) (params : betree_params_t) (node_id_cnt : betree_node_id_counter_t) (key : u64) @@ -1082,7 +1088,7 @@ let betree_node_apply_back'a (key, new_msg) l) st st2 in Return (st0, (self0, node_id_cnt0)) -(** [betree_main::betree::Node::{5}::apply] *) +(** [betree_main::betree::Node::{5}::apply]: backward function 1 *) let betree_node_apply_back1 (self : betree_node_t) (params : betree_params_t) (node_id_cnt : betree_node_id_counter_t) (key : u64) @@ -1101,7 +1107,7 @@ let betree_node_apply_back1 (key, new_msg) l) st st2 in Return (st0, ()) -(** [betree_main::betree::BeTree::{6}::new] *) +(** [betree_main::betree::BeTree::{6}::new]: forward function *) let betree_be_tree_new_fwd (min_flush_size : u64) (split_size : u64) (st : state) : result (state & betree_be_tree_t) @@ -1122,7 +1128,7 @@ let betree_be_tree_new_fwd (BetreeNodeLeaf { betree_leaf_id = id; betree_leaf_size = 0 }) }) -(** [betree_main::betree::BeTree::{6}::apply] *) +(** [betree_main::betree::BeTree::{6}::apply]: forward function *) let betree_be_tree_apply_fwd (self : betree_be_tree_t) (key : u64) (msg : betree_message_t) (st : state) : result (state & unit) @@ -1137,7 +1143,7 @@ let betree_be_tree_apply_fwd betree_node_apply_back1 self.betree_be_tree_root self.betree_be_tree_params self.betree_be_tree_node_id_cnt key msg st st1 -(** [betree_main::betree::BeTree::{6}::apply] *) +(** [betree_main::betree::BeTree::{6}::apply]: backward function 0 *) let betree_be_tree_apply_back (self : betree_be_tree_t) (key : u64) (msg : betree_message_t) (st : state) (st0 : state) : @@ -1156,7 +1162,7 @@ let betree_be_tree_apply_back Return (st0, { self with betree_be_tree_node_id_cnt = nic; betree_be_tree_root = n }) -(** [betree_main::betree::BeTree::{6}::insert] *) +(** [betree_main::betree::BeTree::{6}::insert]: forward function *) let betree_be_tree_insert_fwd (self : betree_be_tree_t) (key : u64) (value : u64) (st : state) : result (state & unit) @@ -1167,7 +1173,7 @@ let betree_be_tree_insert_fwd betree_be_tree_apply_back self key (BetreeMessageInsert value) st st0 in Return (st1, ()) -(** [betree_main::betree::BeTree::{6}::insert] *) +(** [betree_main::betree::BeTree::{6}::insert]: backward function 0 *) let betree_be_tree_insert_back (self : betree_be_tree_t) (key : u64) (value : u64) (st : state) (st0 : state) : @@ -1179,7 +1185,7 @@ let betree_be_tree_insert_back betree_be_tree_apply_back self key (BetreeMessageInsert value) st st1 in Return (st0, self0) -(** [betree_main::betree::BeTree::{6}::delete] *) +(** [betree_main::betree::BeTree::{6}::delete]: forward function *) let betree_be_tree_delete_fwd (self : betree_be_tree_t) (key : u64) (st : state) : result (state & unit) = let* (st0, _) = betree_be_tree_apply_fwd self key BetreeMessageDelete st in @@ -1187,7 +1193,7 @@ let betree_be_tree_delete_fwd in Return (st1, ()) -(** [betree_main::betree::BeTree::{6}::delete] *) +(** [betree_main::betree::BeTree::{6}::delete]: backward function 0 *) let betree_be_tree_delete_back (self : betree_be_tree_t) (key : u64) (st : state) (st0 : state) : result (state & betree_be_tree_t) @@ -1197,7 +1203,7 @@ let betree_be_tree_delete_back betree_be_tree_apply_back self key BetreeMessageDelete st st1 in Return (st0, self0) -(** [betree_main::betree::BeTree::{6}::upsert] *) +(** [betree_main::betree::BeTree::{6}::upsert]: forward function *) let betree_be_tree_upsert_fwd (self : betree_be_tree_t) (key : u64) (upd : betree_upsert_fun_state_t) (st : state) : @@ -1209,7 +1215,7 @@ let betree_be_tree_upsert_fwd betree_be_tree_apply_back self key (BetreeMessageUpsert upd) st st0 in Return (st1, ()) -(** [betree_main::betree::BeTree::{6}::upsert] *) +(** [betree_main::betree::BeTree::{6}::upsert]: backward function 0 *) let betree_be_tree_upsert_back (self : betree_be_tree_t) (key : u64) (upd : betree_upsert_fun_state_t) (st : state) (st0 : state) : @@ -1221,14 +1227,14 @@ let betree_be_tree_upsert_back betree_be_tree_apply_back self key (BetreeMessageUpsert upd) st st1 in Return (st0, self0) -(** [betree_main::betree::BeTree::{6}::lookup] *) +(** [betree_main::betree::BeTree::{6}::lookup]: forward function *) let betree_be_tree_lookup_fwd (self : betree_be_tree_t) (key : u64) (st : state) : result (state & (option u64)) = betree_node_lookup_fwd self.betree_be_tree_root key st -(** [betree_main::betree::BeTree::{6}::lookup] *) +(** [betree_main::betree::BeTree::{6}::lookup]: backward function 0 *) let betree_be_tree_lookup_back (self : betree_be_tree_t) (key : u64) (st : state) (st0 : state) : result (state & betree_be_tree_t) @@ -1237,7 +1243,7 @@ let betree_be_tree_lookup_back in Return (st1, { self with betree_be_tree_root = n }) -(** [betree_main::main] *) +(** [betree_main::main]: forward function *) let main_fwd : result unit = Return () diff --git a/tests/fstar/betree_back_stateful/BetreeMain.Opaque.fsti b/tests/fstar/betree_back_stateful/BetreeMain.Opaque.fsti index dc49601a..c33cf225 100644 --- a/tests/fstar/betree_back_stateful/BetreeMain.Opaque.fsti +++ b/tests/fstar/betree_back_stateful/BetreeMain.Opaque.fsti @@ -1,30 +1,30 @@ (** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *) -(** [betree_main]: opaque function definitions *) +(** [betree_main]: external function declarations *) module BetreeMain.Opaque open Primitives include BetreeMain.Types #set-options "--z3rlimit 50 --fuel 1 --ifuel 1" -(** [betree_main::betree_utils::load_internal_node] *) +(** [betree_main::betree_utils::load_internal_node]: forward function *) val betree_utils_load_internal_node_fwd : u64 -> state -> result (state & (betree_list_t (u64 & betree_message_t))) -(** [betree_main::betree_utils::store_internal_node] *) +(** [betree_main::betree_utils::store_internal_node]: forward function *) val betree_utils_store_internal_node_fwd : u64 -> betree_list_t (u64 & betree_message_t) -> state -> result (state & unit) -(** [betree_main::betree_utils::load_leaf_node] *) +(** [betree_main::betree_utils::load_leaf_node]: forward function *) val betree_utils_load_leaf_node_fwd : u64 -> state -> result (state & (betree_list_t (u64 & u64))) -(** [betree_main::betree_utils::store_leaf_node] *) +(** [betree_main::betree_utils::store_leaf_node]: forward function *) val betree_utils_store_leaf_node_fwd : u64 -> betree_list_t (u64 & u64) -> state -> result (state & unit) -(** [core::option::Option::{0}::unwrap] *) +(** [core::option::Option::{0}::unwrap]: forward function *) val core_option_option_unwrap_fwd (t : Type0) : option t -> state -> result (state & t) |