diff options
Diffstat (limited to 'tests/fstar/betree')
| -rw-r--r-- | tests/fstar/betree/BetreeMain.Clauses.Template.fst | 46 | ||||
| -rw-r--r-- | tests/fstar/betree/BetreeMain.Funs.fst | 434 | ||||
| -rw-r--r-- | tests/fstar/betree/BetreeMain.Types.fsti | 12 |
3 files changed, 246 insertions, 246 deletions
diff --git a/tests/fstar/betree/BetreeMain.Clauses.Template.fst b/tests/fstar/betree/BetreeMain.Clauses.Template.fst index 5a9776ab..823df03a 100644 --- a/tests/fstar/betree/BetreeMain.Clauses.Template.fst +++ b/tests/fstar/betree/BetreeMain.Clauses.Template.fst @@ -23,12 +23,6 @@ let betree_list_partition_at_pivot_decreases (t : Type0) (self : betree_list_t (u64 & t)) (pivot : u64) : nat = admit () -(** [betree_main::betree::Node::{5}::lookup_in_bindings]: decreases clause *) -unfold -let betree_node_lookup_in_bindings_decreases (key : u64) - (bindings : betree_list_t (u64 & u64)) : nat = - admit () - (** [betree_main::betree::Node::{5}::lookup_first_message_for_key]: decreases clause *) unfold let betree_node_lookup_first_message_for_key_decreases (key : u64) @@ -42,10 +36,10 @@ let betree_node_apply_upserts_decreases (key : u64) (st : state) : nat = admit () -(** [betree_main::betree::Node::{5}::lookup]: decreases clause *) +(** [betree_main::betree::Node::{5}::lookup_in_bindings]: decreases clause *) unfold -let betree_node_lookup_decreases (self : betree_node_t) (key : u64) - (st : state) : nat = +let betree_node_lookup_in_bindings_decreases (key : u64) + (bindings : betree_list_t (u64 & u64)) : nat = admit () (** [betree_main::betree::Internal::{4}::lookup_in_children]: decreases clause *) @@ -54,17 +48,10 @@ let betree_internal_lookup_in_children_decreases (self : betree_internal_t) (key : u64) (st : state) : nat = admit () -(** [betree_main::betree::Node::{5}::lookup_mut_in_bindings]: decreases clause *) -unfold -let betree_node_lookup_mut_in_bindings_decreases (key : u64) - (bindings : betree_list_t (u64 & u64)) : nat = - admit () - -(** [betree_main::betree::Node::{5}::apply_messages_to_leaf]: decreases clause *) +(** [betree_main::betree::Node::{5}::lookup]: decreases clause *) 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 = +let betree_node_lookup_decreases (self : betree_node_t) (key : u64) + (st : state) : nat = admit () (** [betree_main::betree::Node::{5}::filter_messages_for_key]: decreases clause *) @@ -86,11 +73,17 @@ let betree_node_apply_messages_to_internal_decreases (new_msgs : betree_list_t (u64 & betree_message_t)) : nat = admit () -(** [betree_main::betree::Node::{5}::apply_messages]: decreases clause *) +(** [betree_main::betree::Node::{5}::lookup_mut_in_bindings]: decreases clause *) unfold -let betree_node_apply_messages_decreases (self : betree_node_t) - (params : betree_params_t) (node_id_cnt : betree_node_id_counter_t) - (msgs : betree_list_t (u64 & betree_message_t)) (st : state) : nat = +let betree_node_lookup_mut_in_bindings_decreases (key : u64) + (bindings : betree_list_t (u64 & u64)) : nat = + admit () + +(** [betree_main::betree::Node::{5}::apply_messages_to_leaf]: decreases clause *) +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::Internal::{4}::flush]: decreases clause *) @@ -100,3 +93,10 @@ let betree_internal_flush_decreases (self : betree_internal_t) (content : betree_list_t (u64 & betree_message_t)) (st : state) : nat = admit () +(** [betree_main::betree::Node::{5}::apply_messages]: decreases clause *) +unfold +let betree_node_apply_messages_decreases (self : betree_node_t) + (params : betree_params_t) (node_id_cnt : betree_node_id_counter_t) + (msgs : betree_list_t (u64 & betree_message_t)) (st : state) : nat = + admit () + diff --git a/tests/fstar/betree/BetreeMain.Funs.fst b/tests/fstar/betree/BetreeMain.Funs.fst index f1bc1191..bd4e37d4 100644 --- a/tests/fstar/betree/BetreeMain.Funs.fst +++ b/tests/fstar/betree/BetreeMain.Funs.fst @@ -222,24 +222,6 @@ let betree_leaf_split_back let* _ = betree_store_leaf_node_fwd id1 content1 st0 in betree_node_id_counter_fresh_id_back node_id_cnt0 -(** [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)) - (decreases (betree_node_lookup_in_bindings_decreases key bindings)) - = - begin match bindings with - | BetreeListCons hd tl -> - let (i, i0) = hd in - if i = key - then Return (Some i0) - else - if i > key - then Return None - else betree_node_lookup_in_bindings_fwd key tl - | BetreeListNil -> Return None - end - (** [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)) : @@ -326,8 +308,50 @@ let rec betree_node_apply_upserts_back betree_list_push_front_fwd_back (u64 & betree_message_t) msgs (key, BetreeMessageInsert v) +(** [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)) + (decreases (betree_node_lookup_in_bindings_decreases key bindings)) + = + begin match bindings with + | BetreeListCons hd tl -> + let (i, i0) = hd in + if i = key + then Return (Some i0) + else + if i > key + then Return None + else betree_node_lookup_in_bindings_fwd key tl + | BetreeListNil -> Return None + end + +(** [betree_main::betree::Internal::{4}::lookup_in_children]: forward function *) +let rec betree_internal_lookup_in_children_fwd + (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.betree_internal_pivot + 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]: backward function 0 *) +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.betree_internal_pivot + then + let* n = betree_node_lookup_back self.betree_internal_left key st in + Return { self with betree_internal_left = n } + else + let* n = betree_node_lookup_back self.betree_internal_right key st in + Return { self with betree_internal_right = n } + (** [betree_main::betree::Node::{5}::lookup]: forward function *) -let rec betree_node_lookup_fwd +and betree_node_lookup_fwd (self : betree_node_t) (key : u64) (st : state) : Tot (result (state & (option u64))) (decreases (betree_node_lookup_decreases self key st)) @@ -451,123 +475,6 @@ and betree_node_lookup_back Return (BetreeNodeLeaf node) end -(** [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))) - (decreases (betree_internal_lookup_in_children_decreases self key st)) - = - if key < self.betree_internal_pivot - 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]: backward function 0 *) -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.betree_internal_pivot - then - let* n = betree_node_lookup_back self.betree_internal_left key st in - Return { self with betree_internal_left = n } - else - let* n = betree_node_lookup_back self.betree_internal_right key st in - Return { self with betree_internal_right = n } - -(** [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))) - (decreases (betree_node_lookup_mut_in_bindings_decreases key bindings)) - = - begin match bindings with - | BetreeListCons hd tl -> - let (i, i0) = hd in - if i >= key - then Return (BetreeListCons (i, i0) tl) - else betree_node_lookup_mut_in_bindings_fwd key tl - | BetreeListNil -> Return BetreeListNil - end - -(** [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)) : - Tot (result (betree_list_t (u64 & u64))) - (decreases (betree_node_lookup_mut_in_bindings_decreases key bindings)) - = - begin match bindings with - | BetreeListCons hd tl -> - let (i, i0) = hd in - if i >= key - then Return ret - else - let* tl0 = betree_node_lookup_mut_in_bindings_back key tl ret in - Return (BetreeListCons (i, i0) tl0) - | BetreeListNil -> Return ret - end - -(** [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) : - result (betree_list_t (u64 & u64)) - = - let* bindings0 = betree_node_lookup_mut_in_bindings_fwd key bindings in - let* b = betree_list_head_has_key_fwd u64 bindings0 key in - if b - then - let* hd = betree_list_pop_front_fwd (u64 & u64) bindings0 in - begin match new_msg with - | BetreeMessageInsert v -> - let* bindings1 = betree_list_pop_front_back (u64 & u64) bindings0 in - let* bindings2 = - betree_list_push_front_fwd_back (u64 & u64) bindings1 (key, v) in - betree_node_lookup_mut_in_bindings_back key bindings bindings2 - | BetreeMessageDelete -> - let* bindings1 = betree_list_pop_front_back (u64 & u64) bindings0 in - betree_node_lookup_mut_in_bindings_back key bindings bindings1 - | BetreeMessageUpsert s -> - let (_, i) = hd in - let* v = betree_upsert_update_fwd (Some i) s in - let* bindings1 = betree_list_pop_front_back (u64 & u64) bindings0 in - let* bindings2 = - betree_list_push_front_fwd_back (u64 & u64) bindings1 (key, v) in - betree_node_lookup_mut_in_bindings_back key bindings bindings2 - end - else - begin match new_msg with - | BetreeMessageInsert v -> - let* bindings1 = - betree_list_push_front_fwd_back (u64 & u64) bindings0 (key, v) in - betree_node_lookup_mut_in_bindings_back key bindings bindings1 - | BetreeMessageDelete -> - betree_node_lookup_mut_in_bindings_back key bindings bindings0 - | BetreeMessageUpsert s -> - let* v = betree_upsert_update_fwd None s in - let* bindings1 = - betree_list_push_front_fwd_back (u64 & u64) bindings0 (key, v) in - betree_node_lookup_mut_in_bindings_back key bindings bindings1 - end - -(** [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)) : - Tot (result (betree_list_t (u64 & u64))) - (decreases (betree_node_apply_messages_to_leaf_decreases bindings new_msgs)) - = - begin match new_msgs with - | BetreeListCons new_msg new_msgs_tl -> - let (i, m) = new_msg in - let* bindings0 = betree_node_apply_to_leaf_fwd_back bindings i m in - betree_node_apply_messages_to_leaf_fwd_back bindings0 new_msgs_tl - | BetreeListNil -> Return bindings - end - (** [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 @@ -699,8 +606,181 @@ let rec betree_node_apply_messages_to_internal_fwd_back | BetreeListNil -> Return msgs end +(** [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))) + (decreases (betree_node_lookup_mut_in_bindings_decreases key bindings)) + = + begin match bindings with + | BetreeListCons hd tl -> + let (i, i0) = hd in + if i >= key + then Return (BetreeListCons (i, i0) tl) + else betree_node_lookup_mut_in_bindings_fwd key tl + | BetreeListNil -> Return BetreeListNil + end + +(** [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)) : + Tot (result (betree_list_t (u64 & u64))) + (decreases (betree_node_lookup_mut_in_bindings_decreases key bindings)) + = + begin match bindings with + | BetreeListCons hd tl -> + let (i, i0) = hd in + if i >= key + then Return ret + else + let* tl0 = betree_node_lookup_mut_in_bindings_back key tl ret in + Return (BetreeListCons (i, i0) tl0) + | BetreeListNil -> Return ret + end + +(** [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) : + result (betree_list_t (u64 & u64)) + = + let* bindings0 = betree_node_lookup_mut_in_bindings_fwd key bindings in + let* b = betree_list_head_has_key_fwd u64 bindings0 key in + if b + then + let* hd = betree_list_pop_front_fwd (u64 & u64) bindings0 in + begin match new_msg with + | BetreeMessageInsert v -> + let* bindings1 = betree_list_pop_front_back (u64 & u64) bindings0 in + let* bindings2 = + betree_list_push_front_fwd_back (u64 & u64) bindings1 (key, v) in + betree_node_lookup_mut_in_bindings_back key bindings bindings2 + | BetreeMessageDelete -> + let* bindings1 = betree_list_pop_front_back (u64 & u64) bindings0 in + betree_node_lookup_mut_in_bindings_back key bindings bindings1 + | BetreeMessageUpsert s -> + let (_, i) = hd in + let* v = betree_upsert_update_fwd (Some i) s in + let* bindings1 = betree_list_pop_front_back (u64 & u64) bindings0 in + let* bindings2 = + betree_list_push_front_fwd_back (u64 & u64) bindings1 (key, v) in + betree_node_lookup_mut_in_bindings_back key bindings bindings2 + end + else + begin match new_msg with + | BetreeMessageInsert v -> + let* bindings1 = + betree_list_push_front_fwd_back (u64 & u64) bindings0 (key, v) in + betree_node_lookup_mut_in_bindings_back key bindings bindings1 + | BetreeMessageDelete -> + betree_node_lookup_mut_in_bindings_back key bindings bindings0 + | BetreeMessageUpsert s -> + let* v = betree_upsert_update_fwd None s in + let* bindings1 = + betree_list_push_front_fwd_back (u64 & u64) bindings0 (key, v) in + betree_node_lookup_mut_in_bindings_back key bindings bindings1 + end + +(** [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)) : + Tot (result (betree_list_t (u64 & u64))) + (decreases (betree_node_apply_messages_to_leaf_decreases bindings new_msgs)) + = + begin match new_msgs with + | BetreeListCons new_msg new_msgs_tl -> + let (i, m) = new_msg in + let* bindings0 = betree_node_apply_to_leaf_fwd_back bindings i m in + betree_node_apply_messages_to_leaf_fwd_back bindings0 new_msgs_tl + | BetreeListNil -> Return bindings + end + +(** [betree_main::betree::Internal::{4}::flush]: forward function *) +let rec betree_internal_flush_fwd + (self : betree_internal_t) (params : betree_params_t) + (node_id_cnt : betree_node_id_counter_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_list_partition_at_pivot_fwd betree_message_t content + self.betree_internal_pivot in + let (msgs_left, msgs_right) = p in + let* len_left = betree_list_len_fwd (u64 & betree_message_t) msgs_left in + if len_left >= params.betree_params_min_flush_size + then + let* (st0, _) = + betree_node_apply_messages_fwd self.betree_internal_left params + node_id_cnt msgs_left st in + let* (_, node_id_cnt0) = + betree_node_apply_messages_back self.betree_internal_left params + node_id_cnt msgs_left st in + let* len_right = betree_list_len_fwd (u64 & betree_message_t) msgs_right in + if len_right >= params.betree_params_min_flush_size + then + let* (st1, _) = + betree_node_apply_messages_fwd self.betree_internal_right params + node_id_cnt0 msgs_right st0 in + let* _ = + betree_node_apply_messages_back self.betree_internal_right params + node_id_cnt0 msgs_right st0 in + Return (st1, BetreeListNil) + else Return (st0, msgs_right) + else + let* (st0, _) = + betree_node_apply_messages_fwd self.betree_internal_right params + node_id_cnt msgs_right st in + let* _ = + betree_node_apply_messages_back self.betree_internal_right params + node_id_cnt msgs_right st in + Return (st0, msgs_left) + +(** [betree_main::betree::Internal::{4}::flush]: backward function 0 *) +and betree_internal_flush_back + (self : betree_internal_t) (params : betree_params_t) + (node_id_cnt : betree_node_id_counter_t) + (content : betree_list_t (u64 & betree_message_t)) (st : state) : + Tot (result (betree_internal_t & betree_node_id_counter_t)) + (decreases ( + betree_internal_flush_decreases self params node_id_cnt content st)) + = + let* p = + betree_list_partition_at_pivot_fwd betree_message_t content + self.betree_internal_pivot in + let (msgs_left, msgs_right) = p in + let* len_left = betree_list_len_fwd (u64 & betree_message_t) msgs_left in + if len_left >= params.betree_params_min_flush_size + then + let* (st0, _) = + betree_node_apply_messages_fwd self.betree_internal_left params + node_id_cnt msgs_left st in + let* (n, node_id_cnt0) = + betree_node_apply_messages_back self.betree_internal_left params + node_id_cnt msgs_left st in + let* len_right = betree_list_len_fwd (u64 & betree_message_t) msgs_right in + if len_right >= params.betree_params_min_flush_size + then + let* (n0, node_id_cnt1) = + betree_node_apply_messages_back self.betree_internal_right params + node_id_cnt0 msgs_right st0 in + Return + ({ self with betree_internal_left = n; betree_internal_right = n0 }, + node_id_cnt1) + else Return ({ self with betree_internal_left = n }, node_id_cnt0) + else + let* (n, node_id_cnt0) = + betree_node_apply_messages_back self.betree_internal_right params + node_id_cnt msgs_right st in + Return ({ self with betree_internal_right = n }, node_id_cnt0) + (** [betree_main::betree::Node::{5}::apply_messages]: forward function *) -let rec betree_node_apply_messages_fwd +and betree_node_apply_messages_fwd (self : betree_node_t) (params : betree_params_t) (node_id_cnt : betree_node_id_counter_t) (msgs : betree_list_t (u64 & betree_message_t)) (st : state) : @@ -794,86 +874,6 @@ and betree_node_apply_messages_back Return (BetreeNodeLeaf { node with betree_leaf_size = len }, node_id_cnt) end -(** [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) - (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_list_partition_at_pivot_fwd betree_message_t content - self.betree_internal_pivot in - let (msgs_left, msgs_right) = p in - let* len_left = betree_list_len_fwd (u64 & betree_message_t) msgs_left in - if len_left >= params.betree_params_min_flush_size - then - let* (st0, _) = - betree_node_apply_messages_fwd self.betree_internal_left params - node_id_cnt msgs_left st in - let* (_, node_id_cnt0) = - betree_node_apply_messages_back self.betree_internal_left params - node_id_cnt msgs_left st in - let* len_right = betree_list_len_fwd (u64 & betree_message_t) msgs_right in - if len_right >= params.betree_params_min_flush_size - then - let* (st1, _) = - betree_node_apply_messages_fwd self.betree_internal_right params - node_id_cnt0 msgs_right st0 in - let* _ = - betree_node_apply_messages_back self.betree_internal_right params - node_id_cnt0 msgs_right st0 in - Return (st1, BetreeListNil) - else Return (st0, msgs_right) - else - let* (st0, _) = - betree_node_apply_messages_fwd self.betree_internal_right params - node_id_cnt msgs_right st in - let* _ = - betree_node_apply_messages_back self.betree_internal_right params - node_id_cnt msgs_right st in - Return (st0, msgs_left) - -(** [betree_main::betree::Internal::{4}::flush]: backward function 0 *) -and betree_internal_flush_back - (self : betree_internal_t) (params : betree_params_t) - (node_id_cnt : betree_node_id_counter_t) - (content : betree_list_t (u64 & betree_message_t)) (st : state) : - Tot (result (betree_internal_t & betree_node_id_counter_t)) - (decreases ( - betree_internal_flush_decreases self params node_id_cnt content st)) - = - let* p = - betree_list_partition_at_pivot_fwd betree_message_t content - self.betree_internal_pivot in - let (msgs_left, msgs_right) = p in - let* len_left = betree_list_len_fwd (u64 & betree_message_t) msgs_left in - if len_left >= params.betree_params_min_flush_size - then - let* (st0, _) = - betree_node_apply_messages_fwd self.betree_internal_left params - node_id_cnt msgs_left st in - let* (n, node_id_cnt0) = - betree_node_apply_messages_back self.betree_internal_left params - node_id_cnt msgs_left st in - let* len_right = betree_list_len_fwd (u64 & betree_message_t) msgs_right in - if len_right >= params.betree_params_min_flush_size - then - let* (n0, node_id_cnt1) = - betree_node_apply_messages_back self.betree_internal_right params - node_id_cnt0 msgs_right st0 in - Return - ({ self with betree_internal_left = n; betree_internal_right = n0 }, - node_id_cnt1) - else Return ({ self with betree_internal_left = n }, node_id_cnt0) - else - let* (n, node_id_cnt0) = - betree_node_apply_messages_back self.betree_internal_right params - node_id_cnt msgs_right st in - Return ({ self with betree_internal_right = n }, node_id_cnt0) - (** [betree_main::betree::Node::{5}::apply]: forward function *) let betree_node_apply_fwd (self : betree_node_t) (params : betree_params_t) diff --git a/tests/fstar/betree/BetreeMain.Types.fsti b/tests/fstar/betree/BetreeMain.Types.fsti index aad9cb43..a937c726 100644 --- a/tests/fstar/betree/BetreeMain.Types.fsti +++ b/tests/fstar/betree/BetreeMain.Types.fsti @@ -24,13 +24,8 @@ type betree_message_t = (** [betree_main::betree::Leaf] *) type betree_leaf_t = { betree_leaf_id : u64; betree_leaf_size : u64; } -(** [betree_main::betree::Node] *) -type betree_node_t = -| BetreeNodeInternal : betree_internal_t -> betree_node_t -| BetreeNodeLeaf : betree_leaf_t -> betree_node_t - (** [betree_main::betree::Internal] *) -and betree_internal_t = +type betree_internal_t = { betree_internal_id : u64; betree_internal_pivot : u64; @@ -38,6 +33,11 @@ and betree_internal_t = betree_internal_right : betree_node_t; } +(** [betree_main::betree::Node] *) +and betree_node_t = +| BetreeNodeInternal : betree_internal_t -> betree_node_t +| BetreeNodeLeaf : betree_leaf_t -> betree_node_t + (** [betree_main::betree::Params] *) type betree_params_t = { |