diff options
Diffstat (limited to '')
| -rw-r--r-- | tests/fstar-split/betree/BetreeMain.Funs.fst | 1006 |
1 files changed, 0 insertions, 1006 deletions
diff --git a/tests/fstar-split/betree/BetreeMain.Funs.fst b/tests/fstar-split/betree/BetreeMain.Funs.fst deleted file mode 100644 index 33133236..00000000 --- a/tests/fstar-split/betree/BetreeMain.Funs.fst +++ /dev/null @@ -1,1006 +0,0 @@ -(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *) -(** [betree_main]: function definitions *) -module BetreeMain.Funs -open Primitives -include BetreeMain.Types -include BetreeMain.FunsExternal -include BetreeMain.Clauses - -#set-options "--z3rlimit 50 --fuel 1 --ifuel 1" - -(** [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 - 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) - = - let* (st1, _) = betree_utils_store_internal_node id content st in - Return (st1, ()) - -(** [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 - 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) - = - let* (st1, _) = betree_utils_store_leaf_node id content st in - Return (st1, ()) - -(** [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 - 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 - 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 - 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 - 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 - 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 - | None -> - begin match st with - | Betree_UpsertFunState_Add v -> Return v - | Betree_UpsertFunState_Sub _ -> Return 0 - end - | Some prev1 -> - begin match st with - | Betree_UpsertFunState_Add v -> - let* margin = u64_sub core_u64_max prev1 in - if margin >= v then u64_add prev1 v else Return core_u64_max - | Betree_UpsertFunState_Sub v -> - if prev1 >= v then u64_sub prev1 v else Return 0 - end - end - -(** [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)) - = - begin match self with - | Betree_List_Cons _ tl -> let* i = betree_List_len t tl in u64_add 1 i - | Betree_List_Nil -> Return 0 - end - -(** [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))) - (decreases (betree_List_split_at_decreases t self n)) - = - if n = 0 - then Return (Betree_List_Nil, self) - else - begin match self with - | Betree_List_Cons hd tl -> - let* i = u64_sub n 1 in - let* p = betree_List_split_at t tl i in - let (ls0, ls1) = p in - Return (Betree_List_Cons hd ls0, ls1) - | Betree_List_Nil -> Fail Failure - 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 ()) - 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 - Return (Betree_List_Cons x tl) - -(** [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 - | Betree_List_Cons x _ -> Return x - | Betree_List_Nil -> Fail Failure - end - -(** [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 - begin match ls with - | Betree_List_Cons _ tl -> Return tl - | Betree_List_Nil -> Fail Failure - end - -(** [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 _ -> Return hd - | Betree_List_Nil -> Fail Failure - end - -(** [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 - | Betree_List_Cons hd _ -> let (i, _) = hd in Return (i = key) - | Betree_List_Nil -> Return false - end - -(** [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)))) - (decreases (betree_ListTupleU64T_partition_at_pivot_decreases t self pivot)) - = - begin match self with - | Betree_List_Cons hd tl -> - let (i, x) = hd in - if i >= pivot - then Return (Betree_List_Nil, Betree_List_Cons (i, x) tl) - else - let* p = betree_ListTupleU64T_partition_at_pivot t tl pivot in - let (ls0, ls1) = p in - Return (Betree_List_Cons (i, x) ls0, ls1) - | Betree_List_Nil -> Return (Betree_List_Nil, Betree_List_Nil) - end - -(** [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) - (st : state) : - result (state & betree_Internal_t) - = - let* p = betree_List_split_at (u64 & u64) content params.split_size in - let (content0, content1) = p in - let* p1 = betree_List_hd (u64 & u64) content1 in - let (pivot, _) = p1 in - let* id0 = betree_NodeIdCounter_fresh_id node_id_cnt in - let* node_id_cnt1 = betree_NodeIdCounter_fresh_id_back node_id_cnt in - let* id1 = betree_NodeIdCounter_fresh_id node_id_cnt1 in - let* (st1, _) = betree_store_leaf_node id0 content0 st in - let* (st2, _) = betree_store_leaf_node id1 content1 st1 in - let n = Betree_Node_Leaf { id = id0; size = params.split_size } in - let n1 = Betree_Node_Leaf { id = id1; size = params.split_size } in - Return (st2, { id = self.id; pivot = pivot; left = n; right = n1 }) - -(** [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) - (st : state) : - result betree_NodeIdCounter_t - = - let* p = betree_List_split_at (u64 & u64) content params.split_size in - let (content0, content1) = p in - let* _ = betree_List_hd (u64 & u64) content1 in - let* id0 = betree_NodeIdCounter_fresh_id node_id_cnt in - let* node_id_cnt1 = betree_NodeIdCounter_fresh_id_back node_id_cnt in - let* id1 = betree_NodeIdCounter_fresh_id node_id_cnt1 in - let* (st1, _) = betree_store_leaf_node id0 content0 st in - let* _ = betree_store_leaf_node id1 content1 st1 in - betree_NodeIdCounter_fresh_id_back node_id_cnt1 - -(** [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))) - (decreases (betree_Node_lookup_first_message_for_key_decreases key msgs)) - = - begin match msgs with - | Betree_List_Cons x next_msgs -> - let (i, m) = x in - if i >= key - then Return (Betree_List_Cons (i, m) next_msgs) - else betree_Node_lookup_first_message_for_key key next_msgs - | Betree_List_Nil -> Return Betree_List_Nil - end - -(** [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)) : - Tot (result (betree_List_t (u64 & betree_Message_t))) - (decreases (betree_Node_lookup_first_message_for_key_decreases key msgs)) - = - begin match msgs with - | Betree_List_Cons x next_msgs -> - let (i, m) = x in - if i >= key - then Return ret - else - let* next_msgs1 = - betree_Node_lookup_first_message_for_key_back key next_msgs ret in - Return (Betree_List_Cons (i, m) next_msgs1) - | Betree_List_Nil -> Return ret - end - -(** [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)) - (decreases (betree_Node_lookup_in_bindings_decreases key bindings)) - = - begin match bindings with - | Betree_List_Cons hd tl -> - let (i, i1) = hd in - if i = key - then Return (Some i1) - else if i > key then Return None else betree_Node_lookup_in_bindings key tl - | Betree_List_Nil -> Return None - end - -(** [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) : - Tot (result (state & u64)) - (decreases (betree_Node_apply_upserts_decreases msgs prev key st)) - = - let* b = betree_ListTupleU64T_head_has_key betree_Message_t msgs key in - if b - then - let* msg = betree_List_pop_front (u64 & betree_Message_t) msgs in - let (_, m) = msg in - begin match m with - | Betree_Message_Insert _ -> Fail Failure - | Betree_Message_Delete -> Fail Failure - | Betree_Message_Upsert s -> - let* v = betree_upsert_update prev s in - let* msgs1 = betree_List_pop_front_back (u64 & betree_Message_t) msgs in - betree_Node_apply_upserts msgs1 (Some v) key st - end - else - let* (st1, v) = core_option_Option_unwrap u64 prev st in - let* _ = - betree_List_push_front (u64 & betree_Message_t) msgs (key, - Betree_Message_Insert v) in - Return (st1, v) - -(** [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) : - Tot (result (betree_List_t (u64 & betree_Message_t))) - (decreases (betree_Node_apply_upserts_decreases msgs prev key st)) - = - let* b = betree_ListTupleU64T_head_has_key betree_Message_t msgs key in - if b - then - let* msg = betree_List_pop_front (u64 & betree_Message_t) msgs in - let (_, m) = msg in - begin match m with - | Betree_Message_Insert _ -> Fail Failure - | Betree_Message_Delete -> Fail Failure - | Betree_Message_Upsert s -> - let* v = betree_upsert_update prev s in - let* msgs1 = betree_List_pop_front_back (u64 & betree_Message_t) msgs in - betree_Node_apply_upserts_back msgs1 (Some v) key st - end - else - let* (_, v) = core_option_Option_unwrap u64 prev st in - betree_List_push_front (u64 & betree_Message_t) msgs (key, - Betree_Message_Insert v) - -(** [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))) - (decreases (betree_Internal_lookup_in_children_decreases self key st)) - = - if key < self.pivot - 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 - 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) - (decreases (betree_Internal_lookup_in_children_decreases self key st)) - = - if key < self.pivot - then - let* n = betree_Node_lookup_back self.left key st in - Return { self with left = n } - else - 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 - 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))) - (decreases (betree_Node_lookup_decreases self key st)) - = - begin match self with - | Betree_Node_Internal node -> - let* (st1, msgs) = betree_load_internal_node node.id st in - let* pending = betree_Node_lookup_first_message_for_key key msgs in - begin match pending with - | Betree_List_Cons p l -> - let (k, msg) = p in - if k <> key - then - let* (st2, o) = betree_Internal_lookup_in_children node key st1 in - let* _ = - betree_Node_lookup_first_message_for_key_back key msgs - (Betree_List_Cons (k, msg) l) in - Return (st2, o) - else - begin match msg with - | Betree_Message_Insert v -> - let* _ = - betree_Node_lookup_first_message_for_key_back key msgs - (Betree_List_Cons (k, Betree_Message_Insert v) l) in - Return (st1, Some v) - | Betree_Message_Delete -> - let* _ = - betree_Node_lookup_first_message_for_key_back key msgs - (Betree_List_Cons (k, Betree_Message_Delete) l) in - Return (st1, None) - | Betree_Message_Upsert ufs -> - let* (st2, v) = betree_Internal_lookup_in_children node key st1 in - let* (st3, v1) = - betree_Node_apply_upserts (Betree_List_Cons (k, - Betree_Message_Upsert ufs) l) v key st2 in - let* node1 = betree_Internal_lookup_in_children_back node key st1 in - let* pending1 = - betree_Node_apply_upserts_back (Betree_List_Cons (k, - Betree_Message_Upsert ufs) l) v key st2 in - let* msgs1 = - betree_Node_lookup_first_message_for_key_back key msgs pending1 in - let* (st4, _) = betree_store_internal_node node1.id msgs1 st3 in - Return (st4, Some v1) - end - | Betree_List_Nil -> - let* (st2, o) = betree_Internal_lookup_in_children node key st1 in - let* _ = - betree_Node_lookup_first_message_for_key_back key msgs Betree_List_Nil - in - Return (st2, o) - end - | Betree_Node_Leaf node -> - let* (st1, bindings) = betree_load_leaf_node node.id st in - let* o = betree_Node_lookup_in_bindings key bindings in - Return (st1, o) - end - -(** [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) - (decreases (betree_Node_lookup_decreases self key st)) - = - begin match self with - | Betree_Node_Internal node -> - let* (st1, msgs) = betree_load_internal_node node.id st in - let* pending = betree_Node_lookup_first_message_for_key key msgs in - begin match pending with - | Betree_List_Cons p l -> - let (k, msg) = p in - if k <> key - then - let* _ = - betree_Node_lookup_first_message_for_key_back key msgs - (Betree_List_Cons (k, msg) l) in - let* node1 = betree_Internal_lookup_in_children_back node key st1 in - Return (Betree_Node_Internal node1) - else - begin match msg with - | Betree_Message_Insert v -> - let* _ = - betree_Node_lookup_first_message_for_key_back key msgs - (Betree_List_Cons (k, Betree_Message_Insert v) l) in - Return (Betree_Node_Internal node) - | Betree_Message_Delete -> - let* _ = - betree_Node_lookup_first_message_for_key_back key msgs - (Betree_List_Cons (k, Betree_Message_Delete) l) in - Return (Betree_Node_Internal node) - | Betree_Message_Upsert ufs -> - let* (st2, v) = betree_Internal_lookup_in_children node key st1 in - let* (st3, _) = - betree_Node_apply_upserts (Betree_List_Cons (k, - Betree_Message_Upsert ufs) l) v key st2 in - let* node1 = betree_Internal_lookup_in_children_back node key st1 in - let* pending1 = - betree_Node_apply_upserts_back (Betree_List_Cons (k, - Betree_Message_Upsert ufs) l) v key st2 in - let* msgs1 = - betree_Node_lookup_first_message_for_key_back key msgs pending1 in - let* _ = betree_store_internal_node node1.id msgs1 st3 in - Return (Betree_Node_Internal node1) - end - | Betree_List_Nil -> - let* _ = - betree_Node_lookup_first_message_for_key_back key msgs Betree_List_Nil - in - let* node1 = betree_Internal_lookup_in_children_back node key st1 in - Return (Betree_Node_Internal node1) - end - | Betree_Node_Leaf node -> - let* (_, bindings) = betree_load_leaf_node node.id st in - let* _ = betree_Node_lookup_in_bindings key bindings in - Return (Betree_Node_Leaf node) - 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 ()) - 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))) - (decreases (betree_Node_filter_messages_for_key_decreases key msgs)) - = - begin match msgs with - | Betree_List_Cons p l -> - let (k, m) = p in - if k = key - then - let* msgs1 = - betree_List_pop_front_back (u64 & betree_Message_t) (Betree_List_Cons - (k, m) l) in - betree_Node_filter_messages_for_key key msgs1 - else Return (Betree_List_Cons (k, m) l) - | Betree_List_Nil -> Return Betree_List_Nil - end - -(** [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))) - (decreases (betree_Node_lookup_first_message_after_key_decreases key msgs)) - = - begin match msgs with - | Betree_List_Cons p next_msgs -> - let (k, m) = p in - if k = key - then betree_Node_lookup_first_message_after_key key next_msgs - else Return (Betree_List_Cons (k, m) next_msgs) - | Betree_List_Nil -> Return Betree_List_Nil - end - -(** [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)) : - Tot (result (betree_List_t (u64 & betree_Message_t))) - (decreases (betree_Node_lookup_first_message_after_key_decreases key msgs)) - = - begin match msgs with - | Betree_List_Cons p next_msgs -> - let (k, m) = p in - if k = key - then - let* next_msgs1 = - betree_Node_lookup_first_message_after_key_back key next_msgs ret in - Return (Betree_List_Cons (k, m) next_msgs1) - else Return ret - | Betree_List_Nil -> Return ret - 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 ()) - 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) : - result (betree_List_t (u64 & betree_Message_t)) - = - let* msgs1 = betree_Node_lookup_first_message_for_key key msgs in - let* b = betree_ListTupleU64T_head_has_key betree_Message_t msgs1 key in - if b - then - begin match new_msg with - | Betree_Message_Insert i -> - let* msgs2 = betree_Node_filter_messages_for_key key msgs1 in - let* msgs3 = - betree_List_push_front (u64 & betree_Message_t) msgs2 (key, - Betree_Message_Insert i) in - betree_Node_lookup_first_message_for_key_back key msgs msgs3 - | Betree_Message_Delete -> - let* msgs2 = betree_Node_filter_messages_for_key key msgs1 in - let* msgs3 = - betree_List_push_front (u64 & betree_Message_t) msgs2 (key, - Betree_Message_Delete) in - betree_Node_lookup_first_message_for_key_back key msgs msgs3 - | Betree_Message_Upsert s -> - let* p = betree_List_hd (u64 & betree_Message_t) msgs1 in - let (_, m) = p in - begin match m with - | Betree_Message_Insert prev -> - let* v = betree_upsert_update (Some prev) s in - let* msgs2 = betree_List_pop_front_back (u64 & betree_Message_t) msgs1 - in - let* msgs3 = - betree_List_push_front (u64 & betree_Message_t) msgs2 (key, - Betree_Message_Insert v) in - betree_Node_lookup_first_message_for_key_back key msgs msgs3 - | Betree_Message_Delete -> - let* v = betree_upsert_update None s in - let* msgs2 = betree_List_pop_front_back (u64 & betree_Message_t) msgs1 - in - let* msgs3 = - betree_List_push_front (u64 & betree_Message_t) msgs2 (key, - Betree_Message_Insert v) in - betree_Node_lookup_first_message_for_key_back key msgs msgs3 - | Betree_Message_Upsert _ -> - let* msgs2 = betree_Node_lookup_first_message_after_key key msgs1 in - let* msgs3 = - betree_List_push_front (u64 & betree_Message_t) msgs2 (key, - Betree_Message_Upsert s) in - let* msgs4 = - betree_Node_lookup_first_message_after_key_back key msgs1 msgs3 in - betree_Node_lookup_first_message_for_key_back key msgs msgs4 - end - end - else - let* msgs2 = - betree_List_push_front (u64 & betree_Message_t) msgs1 (key, new_msg) in - betree_Node_lookup_first_message_for_key_back key msgs msgs2 - -(** [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 ()) - 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)) : - Tot (result (betree_List_t (u64 & betree_Message_t))) - (decreases (betree_Node_apply_messages_to_internal_decreases msgs new_msgs)) - = - begin match new_msgs with - | Betree_List_Cons new_msg new_msgs_tl -> - let (i, m) = new_msg in - let* msgs1 = betree_Node_apply_to_internal msgs i m in - betree_Node_apply_messages_to_internal msgs1 new_msgs_tl - | Betree_List_Nil -> Return msgs - end - -(** [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))) - (decreases (betree_Node_lookup_mut_in_bindings_decreases key bindings)) - = - begin match bindings with - | Betree_List_Cons hd tl -> - let (i, i1) = hd in - if i >= key - then Return (Betree_List_Cons (i, i1) tl) - else betree_Node_lookup_mut_in_bindings key tl - | Betree_List_Nil -> Return Betree_List_Nil - end - -(** [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)) : - Tot (result (betree_List_t (u64 & u64))) - (decreases (betree_Node_lookup_mut_in_bindings_decreases key bindings)) - = - begin match bindings with - | Betree_List_Cons hd tl -> - let (i, i1) = hd in - if i >= key - then Return ret - else - let* tl1 = betree_Node_lookup_mut_in_bindings_back key tl ret in - Return (Betree_List_Cons (i, i1) tl1) - | Betree_List_Nil -> Return ret - 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 ()) - 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) : - result (betree_List_t (u64 & u64)) - = - let* bindings1 = betree_Node_lookup_mut_in_bindings key bindings in - let* b = betree_ListTupleU64T_head_has_key u64 bindings1 key in - if b - then - let* hd = betree_List_pop_front (u64 & u64) bindings1 in - begin match new_msg with - | Betree_Message_Insert v -> - let* bindings2 = betree_List_pop_front_back (u64 & u64) bindings1 in - let* bindings3 = betree_List_push_front (u64 & u64) bindings2 (key, v) in - betree_Node_lookup_mut_in_bindings_back key bindings bindings3 - | Betree_Message_Delete -> - let* bindings2 = betree_List_pop_front_back (u64 & u64) bindings1 in - betree_Node_lookup_mut_in_bindings_back key bindings bindings2 - | Betree_Message_Upsert s -> - let (_, i) = hd in - let* v = betree_upsert_update (Some i) s in - let* bindings2 = betree_List_pop_front_back (u64 & u64) bindings1 in - let* bindings3 = betree_List_push_front (u64 & u64) bindings2 (key, v) in - betree_Node_lookup_mut_in_bindings_back key bindings bindings3 - end - else - begin match new_msg with - | Betree_Message_Insert v -> - let* bindings2 = betree_List_push_front (u64 & u64) bindings1 (key, v) in - betree_Node_lookup_mut_in_bindings_back key bindings bindings2 - | Betree_Message_Delete -> - betree_Node_lookup_mut_in_bindings_back key bindings bindings1 - | Betree_Message_Upsert s -> - let* v = betree_upsert_update None s in - let* bindings2 = betree_List_push_front (u64 & u64) bindings1 (key, v) in - betree_Node_lookup_mut_in_bindings_back key bindings bindings2 - 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 ()) - 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)) : - Tot (result (betree_List_t (u64 & u64))) - (decreases (betree_Node_apply_messages_to_leaf_decreases bindings new_msgs)) - = - begin match new_msgs with - | Betree_List_Cons new_msg new_msgs_tl -> - let (i, m) = new_msg in - let* bindings1 = betree_Node_apply_to_leaf bindings i m in - betree_Node_apply_messages_to_leaf bindings1 new_msgs_tl - | Betree_List_Nil -> Return bindings - end - -(** [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) - (content : betree_List_t (u64 & betree_Message_t)) (st : state) : - Tot (result (state & (betree_List_t (u64 & betree_Message_t)))) - (decreases ( - betree_Internal_flush_decreases self params node_id_cnt content st)) - = - let* p = - betree_ListTupleU64T_partition_at_pivot betree_Message_t content self.pivot - in - let (msgs_left, msgs_right) = p in - let* len_left = betree_List_len (u64 & betree_Message_t) msgs_left in - if len_left >= params.min_flush_size - then - let* (st1, _) = - betree_Node_apply_messages self.left params node_id_cnt msgs_left st in - let* (_, node_id_cnt1) = - betree_Node_apply_messages_back self.left params node_id_cnt msgs_left st - in - let* len_right = betree_List_len (u64 & betree_Message_t) msgs_right in - if len_right >= params.min_flush_size - then - let* (st2, _) = - betree_Node_apply_messages self.right params node_id_cnt1 msgs_right - st1 in - let* _ = - betree_Node_apply_messages_back self.right params node_id_cnt1 - msgs_right st1 in - Return (st2, Betree_List_Nil) - else Return (st1, msgs_right) - else - let* (st1, _) = - betree_Node_apply_messages self.right params node_id_cnt msgs_right st in - let* _ = - betree_Node_apply_messages_back self.right params node_id_cnt msgs_right - st in - Return (st1, msgs_left) - -(** [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) - (content : betree_List_t (u64 & betree_Message_t)) (st : state) : - Tot (result (betree_Internal_t & betree_NodeIdCounter_t)) - (decreases ( - betree_Internal_flush_decreases self params node_id_cnt content st)) - = - let* p = - betree_ListTupleU64T_partition_at_pivot betree_Message_t content self.pivot - in - let (msgs_left, msgs_right) = p in - let* len_left = betree_List_len (u64 & betree_Message_t) msgs_left in - if len_left >= params.min_flush_size - then - let* (st1, _) = - betree_Node_apply_messages self.left params node_id_cnt msgs_left st in - let* (n, node_id_cnt1) = - betree_Node_apply_messages_back self.left params node_id_cnt msgs_left st - in - let* len_right = betree_List_len (u64 & betree_Message_t) msgs_right in - if len_right >= params.min_flush_size - then - let* (n1, node_id_cnt2) = - betree_Node_apply_messages_back self.right params node_id_cnt1 - msgs_right st1 in - Return ({ self with left = n; right = n1 }, node_id_cnt2) - else Return ({ self with left = n }, node_id_cnt1) - else - let* (n, node_id_cnt1) = - betree_Node_apply_messages_back self.right params node_id_cnt msgs_right - st in - Return ({ self with right = n }, node_id_cnt1) - -(** [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) - (msgs : betree_List_t (u64 & betree_Message_t)) (st : state) : - Tot (result (state & unit)) - (decreases ( - betree_Node_apply_messages_decreases self params node_id_cnt msgs st)) - = - begin match self with - | Betree_Node_Internal node -> - let* (st1, content) = betree_load_internal_node node.id st in - let* content1 = betree_Node_apply_messages_to_internal content msgs in - let* num_msgs = betree_List_len (u64 & betree_Message_t) content1 in - if num_msgs >= params.min_flush_size - then - let* (st2, content2) = - betree_Internal_flush node params node_id_cnt content1 st1 in - let* (node1, _) = - betree_Internal_flush_back node params node_id_cnt content1 st1 in - let* (st3, _) = betree_store_internal_node node1.id content2 st2 in - Return (st3, ()) - else - let* (st2, _) = betree_store_internal_node node.id content1 st1 in - Return (st2, ()) - | Betree_Node_Leaf node -> - let* (st1, content) = betree_load_leaf_node node.id st in - let* content1 = betree_Node_apply_messages_to_leaf content msgs in - let* len = betree_List_len (u64 & u64) content1 in - let* i = u64_mul 2 params.split_size in - if len >= i - then - let* (st2, _) = betree_Leaf_split node content1 params node_id_cnt st1 in - let* (st3, _) = betree_store_leaf_node node.id Betree_List_Nil st2 in - Return (st3, ()) - else - let* (st2, _) = betree_store_leaf_node node.id content1 st1 in - Return (st2, ()) - end - -(** [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) - (msgs : betree_List_t (u64 & betree_Message_t)) (st : state) : - Tot (result (betree_Node_t & betree_NodeIdCounter_t)) - (decreases ( - betree_Node_apply_messages_decreases self params node_id_cnt msgs st)) - = - begin match self with - | Betree_Node_Internal node -> - let* (st1, content) = betree_load_internal_node node.id st in - let* content1 = betree_Node_apply_messages_to_internal content msgs in - let* num_msgs = betree_List_len (u64 & betree_Message_t) content1 in - if num_msgs >= params.min_flush_size - then - let* (st2, content2) = - betree_Internal_flush node params node_id_cnt content1 st1 in - let* (node1, node_id_cnt1) = - betree_Internal_flush_back node params node_id_cnt content1 st1 in - let* _ = betree_store_internal_node node1.id content2 st2 in - Return (Betree_Node_Internal node1, node_id_cnt1) - else - let* _ = betree_store_internal_node node.id content1 st1 in - Return (Betree_Node_Internal node, node_id_cnt) - | Betree_Node_Leaf node -> - let* (st1, content) = betree_load_leaf_node node.id st in - let* content1 = betree_Node_apply_messages_to_leaf content msgs in - let* len = betree_List_len (u64 & u64) content1 in - let* i = u64_mul 2 params.split_size in - if len >= i - then - let* (st2, new_node) = - betree_Leaf_split node content1 params node_id_cnt st1 in - let* _ = betree_store_leaf_node node.id Betree_List_Nil st2 in - let* node_id_cnt1 = - betree_Leaf_split_back node content1 params node_id_cnt st1 in - Return (Betree_Node_Internal new_node, node_id_cnt1) - else - let* _ = betree_store_leaf_node node.id content1 st1 in - Return (Betree_Node_Leaf { node with size = len }, node_id_cnt) - end - -(** [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) - (new_msg : betree_Message_t) (st : state) : - result (state & unit) - = - let* (st1, _) = - betree_Node_apply_messages self params node_id_cnt (Betree_List_Cons (key, - new_msg) Betree_List_Nil) st in - let* _ = - betree_Node_apply_messages_back self params node_id_cnt (Betree_List_Cons - (key, new_msg) Betree_List_Nil) st in - Return (st1, ()) - -(** [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) - (new_msg : betree_Message_t) (st : state) : - result (betree_Node_t & betree_NodeIdCounter_t) - = - betree_Node_apply_messages_back self params node_id_cnt (Betree_List_Cons - (key, new_msg) Betree_List_Nil) st - -(** [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) - = - let* node_id_cnt = betree_NodeIdCounter_new in - let* id = betree_NodeIdCounter_fresh_id node_id_cnt in - let* (st1, _) = betree_store_leaf_node id Betree_List_Nil st in - let* node_id_cnt1 = betree_NodeIdCounter_fresh_id_back node_id_cnt in - Return (st1, - { - params = { min_flush_size = min_flush_size; split_size = split_size }; - node_id_cnt = node_id_cnt1; - root = (Betree_Node_Leaf { id = id; size = 0 }) - }) - -(** [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) - = - let* (st1, _) = - betree_Node_apply self.root self.params self.node_id_cnt key msg st in - let* _ = - betree_Node_apply_back self.root self.params self.node_id_cnt key msg st in - Return (st1, ()) - -(** [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 - = - let* (n, nic) = - 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 - 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) - = - let* (st1, _) = betree_BeTree_apply self key (Betree_Message_Insert value) st - in - let* _ = betree_BeTree_apply_back self key (Betree_Message_Insert value) st - in - Return (st1, ()) - -(** [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 - 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* (st1, _) = betree_BeTree_apply self key Betree_Message_Delete st in - let* _ = betree_BeTree_apply_back self key Betree_Message_Delete st in - Return (st1, ()) - -(** [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 - 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) : - result (state & unit) - = - let* (st1, _) = betree_BeTree_apply self key (Betree_Message_Upsert upd) st - in - let* _ = betree_BeTree_apply_back self key (Betree_Message_Upsert upd) st in - Return (st1, ()) - -(** [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) : - result betree_BeTree_t - = - betree_BeTree_apply_back self key (Betree_Message_Upsert upd) st - -(** [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 - 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 - Source: 'src/betree_main.rs', lines 5:0-5:9 *) -let main : result unit = - Return () - -(** Unit test for [betree_main::main] *) -let _ = assert_norm (main = Return ()) - |