From f77e3f9cbe2ea7abeb4be815bdbf33d0c98076c2 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Mon, 27 May 2024 13:28:28 +0200 Subject: tests: Rename betree_main -> betree --- tests/fstar/betree/Betree.Funs.fst | 676 +++++++++++++++++++++++++++++++++++++ 1 file changed, 676 insertions(+) create mode 100644 tests/fstar/betree/Betree.Funs.fst (limited to 'tests/fstar/betree/Betree.Funs.fst') diff --git a/tests/fstar/betree/Betree.Funs.fst b/tests/fstar/betree/Betree.Funs.fst new file mode 100644 index 00000000..07f561f5 --- /dev/null +++ b/tests/fstar/betree/Betree.Funs.fst @@ -0,0 +1,676 @@ +(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *) +(** [betree]: function definitions *) +module Betree.Funs +open Primitives +include Betree.Types +include Betree.FunsExternal +include Betree.Clauses + +#set-options "--z3rlimit 50 --fuel 1 --ifuel 1" + +(** [betree::betree::load_internal_node]: + 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::betree::store_internal_node]: + 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) + = + betree_utils_store_internal_node id content st + +(** [betree::betree::load_leaf_node]: + 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::betree::store_leaf_node]: + 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) + = + betree_utils_store_leaf_node id content st + +(** [betree::betree::fresh_node_id]: + Source: 'src/betree.rs', lines 55:0-55:48 *) +let betree_fresh_node_id (counter : u64) : result (u64 & u64) = + let* counter1 = u64_add counter 1 in Ok (counter, counter1) + +(** [betree::betree::{betree::betree::NodeIdCounter}::new]: + Source: 'src/betree.rs', lines 206:4-206:20 *) +let betree_NodeIdCounter_new : result betree_NodeIdCounter_t = + Ok { next_node_id = 0 } + +(** [betree::betree::{betree::betree::NodeIdCounter}::fresh_id]: + Source: 'src/betree.rs', lines 210:4-210:36 *) +let betree_NodeIdCounter_fresh_id + (self : betree_NodeIdCounter_t) : result (u64 & betree_NodeIdCounter_t) = + let* i = u64_add self.next_node_id 1 in + Ok (self.next_node_id, { next_node_id = i }) + +(** [betree::betree::upsert_update]: + 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 -> Ok v + | Betree_UpsertFunState_Sub _ -> Ok 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 Ok core_u64_max + | Betree_UpsertFunState_Sub v -> + if prev1 >= v then u64_sub prev1 v else Ok 0 + end + end + +(** [betree::betree::{betree::betree::List#1}::len]: + 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 -> Ok 0 + end + +(** [betree::betree::{betree::betree::List#1}::split_at]: + 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 Ok (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 + Ok (Betree_List_Cons hd ls0, ls1) + | Betree_List_Nil -> Fail Failure + end + +(** [betree::betree::{betree::betree::List#1}::push_front]: + 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 + Ok (Betree_List_Cons x tl) + +(** [betree::betree::{betree::betree::List#1}::pop_front]: + Source: 'src/betree.rs', lines 306:4-306:32 *) +let betree_List_pop_front + (t : Type0) (self : betree_List_t t) : result (t & (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 x tl -> Ok (x, tl) + | Betree_List_Nil -> Fail Failure + end + +(** [betree::betree::{betree::betree::List#1}::hd]: + 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 _ -> Ok hd + | Betree_List_Nil -> Fail Failure + end + +(** [betree::betree::{betree::betree::List<(u64, T)>#2}::head_has_key]: + Source: 'src/betree.rs', lines 327:4-327:44 *) +let betree_ListPairU64T_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 Ok (i = key) + | Betree_List_Nil -> Ok false + end + +(** [betree::betree::{betree::betree::List<(u64, T)>#2}::partition_at_pivot]: + Source: 'src/betree.rs', lines 339:4-339:73 *) +let rec betree_ListPairU64T_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_ListPairU64T_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 Ok (Betree_List_Nil, Betree_List_Cons (i, x) tl) + else + let* p = betree_ListPairU64T_partition_at_pivot t tl pivot in + let (ls0, ls1) = p in + Ok (Betree_List_Cons (i, x) ls0, ls1) + | Betree_List_Nil -> Ok (Betree_List_Nil, Betree_List_Nil) + end + +(** [betree::betree::{betree::betree::Leaf#3}::split]: + 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 & betree_NodeIdCounter_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, node_id_cnt1) = betree_NodeIdCounter_fresh_id node_id_cnt in + let* (id1, node_id_cnt2) = 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 + Ok (st2, ({ id = self.id; pivot = pivot; left = n; right = n1 }, + node_id_cnt2)) + +(** [betree::betree::{betree::betree::Node#5}::lookup_first_message_for_key]: + 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)) & (betree_List_t (u64 & + betree_Message_t) -> 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 Ok (Betree_List_Cons (i, m) next_msgs, Ok) + else + let* (l, lookup_first_message_for_key_back) = + betree_Node_lookup_first_message_for_key key next_msgs in + let back = + fun ret -> + let* next_msgs1 = lookup_first_message_for_key_back ret in + Ok (Betree_List_Cons (i, m) next_msgs1) in + Ok (l, back) + | Betree_List_Nil -> Ok (Betree_List_Nil, Ok) + end + +(** [betree::betree::{betree::betree::Node#5}::lookup_in_bindings]: + 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 Ok (Some i1) + else if i > key then Ok None else betree_Node_lookup_in_bindings key tl + | Betree_List_Nil -> Ok None + end + +(** [betree::betree::{betree::betree::Node#5}::apply_upserts]: + 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) : + Tot (result (u64 & (betree_List_t (u64 & betree_Message_t)))) + (decreases (betree_Node_apply_upserts_decreases msgs prev key)) + = + let* b = betree_ListPairU64T_head_has_key betree_Message_t msgs key in + if b + then + let* (msg, msgs1) = 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 + betree_Node_apply_upserts msgs1 (Some v) key + end + else + let* v = core_option_Option_unwrap u64 prev in + let* msgs1 = + betree_List_push_front (u64 & betree_Message_t) msgs (key, + Betree_Message_Insert v) in + Ok (v, msgs1) + +(** [betree::betree::{betree::betree::Internal#4}::lookup_in_children]: + 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) & betree_Internal_t))) + (decreases (betree_Internal_lookup_in_children_decreases self key st)) + = + if key < self.pivot + then + let* (st1, (o, n)) = betree_Node_lookup self.left key st in + Ok (st1, (o, { self with left = n })) + else + let* (st1, (o, n)) = betree_Node_lookup self.right key st in + Ok (st1, (o, { self with right = n })) + +(** [betree::betree::{betree::betree::Node#5}::lookup]: + 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) & 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, lookup_first_message_for_key_back) = + 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, node1)) = + betree_Internal_lookup_in_children node key st1 in + let* _ = + lookup_first_message_for_key_back (Betree_List_Cons (k, msg) l) in + Ok (st2, (o, Betree_Node_Internal node1)) + else + begin match msg with + | Betree_Message_Insert v -> + let* _ = + lookup_first_message_for_key_back (Betree_List_Cons (k, + Betree_Message_Insert v) l) in + Ok (st1, (Some v, Betree_Node_Internal node)) + | Betree_Message_Delete -> + let* _ = + lookup_first_message_for_key_back (Betree_List_Cons (k, + Betree_Message_Delete) l) in + Ok (st1, (None, Betree_Node_Internal node)) + | Betree_Message_Upsert ufs -> + let* (st2, (v, node1)) = + betree_Internal_lookup_in_children node key st1 in + let* (v1, pending1) = + betree_Node_apply_upserts (Betree_List_Cons (k, + Betree_Message_Upsert ufs) l) v key in + let* msgs1 = lookup_first_message_for_key_back pending1 in + let* (st3, _) = betree_store_internal_node node1.id msgs1 st2 in + Ok (st3, (Some v1, Betree_Node_Internal node1)) + end + | Betree_List_Nil -> + let* (st2, (o, node1)) = betree_Internal_lookup_in_children node key st1 + in + let* _ = lookup_first_message_for_key_back Betree_List_Nil in + Ok (st2, (o, Betree_Node_Internal node1)) + 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 + Ok (st1, (o, Betree_Node_Leaf node)) + end + +(** [betree::betree::{betree::betree::Node#5}::filter_messages_for_key]: + 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 (u64 & betree_Message_t) (Betree_List_Cons (k, m) + l) in + betree_Node_filter_messages_for_key key msgs1 + else Ok (Betree_List_Cons (k, m) l) + | Betree_List_Nil -> Ok Betree_List_Nil + end + +(** [betree::betree::{betree::betree::Node#5}::lookup_first_message_after_key]: + 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)) & (betree_List_t (u64 & + betree_Message_t) -> 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* (l, lookup_first_message_after_key_back) = + betree_Node_lookup_first_message_after_key key next_msgs in + let back = + fun ret -> + let* next_msgs1 = lookup_first_message_after_key_back ret in + Ok (Betree_List_Cons (k, m) next_msgs1) in + Ok (l, back) + else Ok (Betree_List_Cons (k, m) next_msgs, Ok) + | Betree_List_Nil -> Ok (Betree_List_Nil, Ok) + end + +(** [betree::betree::{betree::betree::Node#5}::apply_to_internal]: + 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, lookup_first_message_for_key_back) = + betree_Node_lookup_first_message_for_key key msgs in + let* b = betree_ListPairU64T_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 + lookup_first_message_for_key_back 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 + lookup_first_message_for_key_back 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 (u64 & betree_Message_t) msgs1 + in + let* msgs3 = + betree_List_push_front (u64 & betree_Message_t) msgs2 (key, + Betree_Message_Insert v) in + lookup_first_message_for_key_back msgs3 + | Betree_Message_Delete -> + let* (_, msgs2) = betree_List_pop_front (u64 & betree_Message_t) msgs1 + in + let* v = betree_upsert_update None s in + let* msgs3 = + betree_List_push_front (u64 & betree_Message_t) msgs2 (key, + Betree_Message_Insert v) in + lookup_first_message_for_key_back msgs3 + | Betree_Message_Upsert _ -> + let* (msgs2, lookup_first_message_after_key_back) = + 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 = lookup_first_message_after_key_back msgs3 in + lookup_first_message_for_key_back msgs4 + end + end + else + let* msgs2 = + betree_List_push_front (u64 & betree_Message_t) msgs1 (key, new_msg) in + lookup_first_message_for_key_back msgs2 + +(** [betree::betree::{betree::betree::Node#5}::apply_messages_to_internal]: + 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 -> Ok msgs + end + +(** [betree::betree::{betree::betree::Node#5}::lookup_mut_in_bindings]: + 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)) & (betree_List_t (u64 & u64) -> + 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 Ok (Betree_List_Cons (i, i1) tl, Ok) + else + let* (l, lookup_mut_in_bindings_back) = + betree_Node_lookup_mut_in_bindings key tl in + let back = + fun ret -> + let* tl1 = lookup_mut_in_bindings_back ret in + Ok (Betree_List_Cons (i, i1) tl1) in + Ok (l, back) + | Betree_List_Nil -> Ok (Betree_List_Nil, Ok) + end + +(** [betree::betree::{betree::betree::Node#5}::apply_to_leaf]: + 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, lookup_mut_in_bindings_back) = + betree_Node_lookup_mut_in_bindings key bindings in + let* b = betree_ListPairU64T_head_has_key u64 bindings1 key in + if b + then + let* (hd, bindings2) = betree_List_pop_front (u64 & u64) bindings1 in + begin match new_msg with + | Betree_Message_Insert v -> + let* bindings3 = betree_List_push_front (u64 & u64) bindings2 (key, v) in + lookup_mut_in_bindings_back bindings3 + | Betree_Message_Delete -> lookup_mut_in_bindings_back bindings2 + | Betree_Message_Upsert s -> + let (_, i) = hd in + let* v = betree_upsert_update (Some i) s in + let* bindings3 = betree_List_push_front (u64 & u64) bindings2 (key, v) in + lookup_mut_in_bindings_back bindings3 + end + else + begin match new_msg with + | Betree_Message_Insert v -> + let* bindings2 = betree_List_push_front (u64 & u64) bindings1 (key, v) in + lookup_mut_in_bindings_back bindings2 + | Betree_Message_Delete -> lookup_mut_in_bindings_back 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 + lookup_mut_in_bindings_back bindings2 + end + +(** [betree::betree::{betree::betree::Node#5}::apply_messages_to_leaf]: + 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 -> Ok bindings + end + +(** [betree::betree::{betree::betree::Internal#4}::flush]: + 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)) & + (betree_Internal_t & betree_NodeIdCounter_t)))) + (decreases ( + betree_Internal_flush_decreases self params node_id_cnt content st)) + = + let* p = + betree_ListPairU64T_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, p1) = + betree_Node_apply_messages self.left params node_id_cnt msgs_left st in + let (n, node_id_cnt1) = p1 in + let* len_right = betree_List_len (u64 & betree_Message_t) msgs_right in + if len_right >= params.min_flush_size + then + let* (st2, p2) = + betree_Node_apply_messages self.right params node_id_cnt1 msgs_right + st1 in + let (n1, node_id_cnt2) = p2 in + Ok (st2, (Betree_List_Nil, ({ self with left = n; right = n1 }, + node_id_cnt2))) + else Ok (st1, (msgs_right, ({ self with left = n }, node_id_cnt1))) + else + let* (st1, p1) = + betree_Node_apply_messages self.right params node_id_cnt msgs_right st in + let (n, node_id_cnt1) = p1 in + Ok (st1, (msgs_left, ({ self with right = n }, node_id_cnt1))) + +(** [betree::betree::{betree::betree::Node#5}::apply_messages]: + 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 & (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, p)) = + betree_Internal_flush node params node_id_cnt content1 st1 in + let (node1, node_id_cnt1) = p in + let* (st3, _) = betree_store_internal_node node1.id content2 st2 in + Ok (st3, (Betree_Node_Internal node1, node_id_cnt1)) + else + let* (st2, _) = betree_store_internal_node node.id content1 st1 in + Ok (st2, (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, node_id_cnt1)) = + betree_Leaf_split node content1 params node_id_cnt st1 in + let* (st3, _) = betree_store_leaf_node node.id Betree_List_Nil st2 in + Ok (st3, (Betree_Node_Internal new_node, node_id_cnt1)) + else + let* (st2, _) = betree_store_leaf_node node.id content1 st1 in + Ok (st2, (Betree_Node_Leaf { node with size = len }, node_id_cnt)) + end + +(** [betree::betree::{betree::betree::Node#5}::apply]: + 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 & (betree_Node_t & betree_NodeIdCounter_t)) + = + let* (st1, p) = + betree_Node_apply_messages self params node_id_cnt (Betree_List_Cons (key, + new_msg) Betree_List_Nil) st in + let (self1, node_id_cnt1) = p in + Ok (st1, (self1, node_id_cnt1)) + +(** [betree::betree::{betree::betree::BeTree#6}::new]: + 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, node_id_cnt1) = betree_NodeIdCounter_fresh_id node_id_cnt in + let* (st1, _) = betree_store_leaf_node id Betree_List_Nil st in + Ok (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::betree::{betree::betree::BeTree#6}::apply]: + 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 & betree_BeTree_t) + = + let* (st1, p) = + betree_Node_apply self.root self.params self.node_id_cnt key msg st in + let (n, nic) = p in + Ok (st1, { self with node_id_cnt = nic; root = n }) + +(** [betree::betree::{betree::betree::BeTree#6}::insert]: + 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 & betree_BeTree_t) + = + betree_BeTree_apply self key (Betree_Message_Insert value) st + +(** [betree::betree::{betree::betree::BeTree#6}::delete]: + Source: 'src/betree.rs', lines 880:4-880:38 *) +let betree_BeTree_delete + (self : betree_BeTree_t) (key : u64) (st : state) : + result (state & betree_BeTree_t) + = + betree_BeTree_apply self key Betree_Message_Delete st + +(** [betree::betree::{betree::betree::BeTree#6}::upsert]: + 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 & betree_BeTree_t) + = + betree_BeTree_apply self key (Betree_Message_Upsert upd) st + +(** [betree::betree::{betree::betree::BeTree#6}::lookup]: + 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_BeTree_t)) + = + let* (st1, (o, n)) = betree_Node_lookup self.root key st in + Ok (st1, (o, { self with root = n })) + +(** [betree::main]: + Source: 'src/main.rs', lines 4:0-4:9 *) +let main : result unit = + Ok () + +(** Unit test for [betree::main] *) +let _ = assert_norm (main = Ok ()) + -- cgit v1.2.3