diff options
Diffstat (limited to 'tests/fstar')
| -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 | ||||
| -rw-r--r-- | tests/fstar/betree_back_stateful/BetreeMain.Clauses.Template.fst | 46 | ||||
| -rw-r--r-- | tests/fstar/betree_back_stateful/BetreeMain.Funs.fst | 556 | ||||
| -rw-r--r-- | tests/fstar/betree_back_stateful/BetreeMain.Types.fsti | 12 | ||||
| -rw-r--r-- | tests/fstar/misc/NoNestedBorrows.fst | 12 |
7 files changed, 559 insertions, 559 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 = { diff --git a/tests/fstar/betree_back_stateful/BetreeMain.Clauses.Template.fst b/tests/fstar/betree_back_stateful/BetreeMain.Clauses.Template.fst index 5a9776ab..823df03a 100644 --- a/tests/fstar/betree_back_stateful/BetreeMain.Clauses.Template.fst +++ b/tests/fstar/betree_back_stateful/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_back_stateful/BetreeMain.Funs.fst b/tests/fstar/betree_back_stateful/BetreeMain.Funs.fst index 12402fb4..be8ac438 100644 --- a/tests/fstar/betree_back_stateful/BetreeMain.Funs.fst +++ b/tests/fstar/betree_back_stateful/BetreeMain.Funs.fst @@ -261,24 +261,6 @@ 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]: 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)) : @@ -367,8 +349,52 @@ let rec betree_node_apply_upserts_back BetreeMessageInsert v) in Return (st0, msgs0) +(** [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) (st0 : state) : + Tot (result (state & betree_internal_t)) + (decreases (betree_internal_lookup_in_children_decreases self key st)) + = + if key < self.betree_internal_pivot + then + let* (st1, n) = + betree_node_lookup_back self.betree_internal_left key st st0 in + Return (st1, { self with betree_internal_left = n }) + else + let* (st1, n) = + 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]: 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)) @@ -496,125 +522,6 @@ and betree_node_lookup_back Return (st0, 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) (st0 : state) : - Tot (result (state & betree_internal_t)) - (decreases (betree_internal_lookup_in_children_decreases self key st)) - = - if key < self.betree_internal_pivot - then - let* (st1, n) = - betree_node_lookup_back self.betree_internal_left key st st0 in - Return (st1, { self with betree_internal_left = n }) - else - let* (st1, n) = - 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]: 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 @@ -746,157 +653,101 @@ let rec betree_node_apply_messages_to_internal_fwd_back | BetreeListNil -> Return msgs end -(** [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) - (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)) +(** [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 self with - | BetreeNodeInternal node -> - let* (st0, content) = - betree_load_internal_node_fwd node.betree_internal_id st in - let* content0 = - betree_node_apply_messages_to_internal_fwd_back content msgs in - let* num_msgs = betree_list_len_fwd (u64 & betree_message_t) content0 in - if num_msgs >= params.betree_params_min_flush_size - then - let* (st1, content1) = - betree_internal_flush_fwd node params node_id_cnt content0 st0 in - let* (st2, (node0, _)) = - betree_internal_flush_back'a node params node_id_cnt content0 st0 st1 - in - let* (st3, _) = - betree_store_internal_node_fwd node0.betree_internal_id content1 st2 in - Return (st3, ()) - else - let* (st1, _) = - betree_store_internal_node_fwd node.betree_internal_id content0 st0 in - Return (st1, ()) - | BetreeNodeLeaf node -> - let* (st0, content) = betree_load_leaf_node_fwd node.betree_leaf_id st in - let* content0 = betree_node_apply_messages_to_leaf_fwd_back content msgs in - let* len = betree_list_len_fwd (u64 & u64) content0 in - let* i = u64_mul 2 params.betree_params_split_size in - if len >= i - then - let* (st1, _) = - betree_leaf_split_fwd node content0 params node_id_cnt st0 in - let* (st2, _) = - betree_store_leaf_node_fwd node.betree_leaf_id BetreeListNil st1 in - betree_leaf_split_back0 node content0 params node_id_cnt st0 st2 - else - let* (st1, _) = - betree_store_leaf_node_fwd node.betree_leaf_id content0 st0 in - Return (st1, ()) + 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}::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) - (msgs : betree_list_t (u64 & betree_message_t)) (st : state) (st0 : state) : - Tot (result (state & (betree_node_t & betree_node_id_counter_t))) - (decreases ( - betree_node_apply_messages_decreases self params node_id_cnt msgs st)) +(** [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 self with - | BetreeNodeInternal node -> - let* (st1, content) = - betree_load_internal_node_fwd node.betree_internal_id st in - let* content0 = - betree_node_apply_messages_to_internal_fwd_back content msgs in - let* num_msgs = betree_list_len_fwd (u64 & betree_message_t) content0 in - if num_msgs >= params.betree_params_min_flush_size - then - let* (st2, content1) = - betree_internal_flush_fwd node params node_id_cnt content0 st1 in - let* (st3, (node0, node_id_cnt0)) = - betree_internal_flush_back'a node params node_id_cnt content0 st1 st2 - in - let* _ = - betree_store_internal_node_fwd node0.betree_internal_id content1 st3 in - Return (st0, (BetreeNodeInternal node0, node_id_cnt0)) - else - let* _ = - betree_store_internal_node_fwd node.betree_internal_id content0 st1 in - Return (st0, (BetreeNodeInternal node, node_id_cnt)) - | BetreeNodeLeaf node -> - let* (st1, content) = betree_load_leaf_node_fwd node.betree_leaf_id st in - let* content0 = betree_node_apply_messages_to_leaf_fwd_back content msgs in - let* len = betree_list_len_fwd (u64 & u64) content0 in - let* i = u64_mul 2 params.betree_params_split_size in - if len >= i - then - let* (st2, new_node) = - betree_leaf_split_fwd node content0 params node_id_cnt st1 in - let* (st3, _) = - betree_store_leaf_node_fwd node.betree_leaf_id BetreeListNil st2 in - let* _ = betree_leaf_split_back0 node content0 params node_id_cnt st1 st3 - in - let* (st4, node_id_cnt0) = - betree_leaf_split_back2 node content0 params node_id_cnt st1 st0 in - Return (st4, (BetreeNodeInternal new_node, node_id_cnt0)) + begin match bindings with + | BetreeListCons hd tl -> + let (i, i0) = hd in + if i >= key + then Return ret else - let* _ = betree_store_leaf_node_fwd node.betree_leaf_id content0 st1 in - Return (st0, (BetreeNodeLeaf { node with betree_leaf_size = len }, - node_id_cnt)) + 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_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) - (msgs : betree_list_t (u64 & betree_message_t)) (st : state) (st0 : state) : - Tot (result (state & unit)) - (decreases ( - betree_node_apply_messages_decreases self params node_id_cnt msgs st)) +(** [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)) = - begin match self with - | BetreeNodeInternal node -> - let* (st1, content) = - betree_load_internal_node_fwd node.betree_internal_id st in - let* content0 = - betree_node_apply_messages_to_internal_fwd_back content msgs in - let* num_msgs = betree_list_len_fwd (u64 & betree_message_t) content0 in - if num_msgs >= params.betree_params_min_flush_size - then - let* (st2, content1) = - betree_internal_flush_fwd node params node_id_cnt content0 st1 in - let* (st3, (node0, _)) = - betree_internal_flush_back'a node params node_id_cnt content0 st1 st2 - in - let* _ = - betree_store_internal_node_fwd node0.betree_internal_id content1 st3 in - betree_internal_flush_back1 node params node_id_cnt content0 st1 st0 - else - let* _ = - betree_store_internal_node_fwd node.betree_internal_id content0 st1 in - Return (st0, ()) - | BetreeNodeLeaf node -> - let* (st1, content) = betree_load_leaf_node_fwd node.betree_leaf_id st in - let* content0 = betree_node_apply_messages_to_leaf_fwd_back content msgs in - let* len = betree_list_len_fwd (u64 & u64) content0 in - let* i = u64_mul 2 params.betree_params_split_size in - if len >= i - then - let* (st2, _) = - betree_leaf_split_fwd node content0 params node_id_cnt st1 in - let* (st3, _) = - betree_store_leaf_node_fwd node.betree_leaf_id BetreeListNil st2 in - let* _ = betree_leaf_split_back0 node content0 params node_id_cnt st1 st3 - in - betree_leaf_split_back1 node content0 params node_id_cnt st1 st0 - else - let* _ = betree_store_leaf_node_fwd node.betree_leaf_id content0 st1 in - Return (st0, ()) + 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 *) -and betree_internal_flush_fwd +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) : @@ -1052,6 +903,155 @@ and betree_internal_flush_back1 node_id_cnt msgs_right st st2 in Return (st0, ()) +(** [betree_main::betree::Node::{5}::apply_messages]: forward function *) +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) : + Tot (result (state & unit)) + (decreases ( + betree_node_apply_messages_decreases self params node_id_cnt msgs st)) + = + begin match self with + | BetreeNodeInternal node -> + let* (st0, content) = + betree_load_internal_node_fwd node.betree_internal_id st in + let* content0 = + betree_node_apply_messages_to_internal_fwd_back content msgs in + let* num_msgs = betree_list_len_fwd (u64 & betree_message_t) content0 in + if num_msgs >= params.betree_params_min_flush_size + then + let* (st1, content1) = + betree_internal_flush_fwd node params node_id_cnt content0 st0 in + let* (st2, (node0, _)) = + betree_internal_flush_back'a node params node_id_cnt content0 st0 st1 + in + let* (st3, _) = + betree_store_internal_node_fwd node0.betree_internal_id content1 st2 in + Return (st3, ()) + else + let* (st1, _) = + betree_store_internal_node_fwd node.betree_internal_id content0 st0 in + Return (st1, ()) + | BetreeNodeLeaf node -> + let* (st0, content) = betree_load_leaf_node_fwd node.betree_leaf_id st in + let* content0 = betree_node_apply_messages_to_leaf_fwd_back content msgs in + let* len = betree_list_len_fwd (u64 & u64) content0 in + let* i = u64_mul 2 params.betree_params_split_size in + if len >= i + then + let* (st1, _) = + betree_leaf_split_fwd node content0 params node_id_cnt st0 in + let* (st2, _) = + betree_store_leaf_node_fwd node.betree_leaf_id BetreeListNil st1 in + betree_leaf_split_back0 node content0 params node_id_cnt st0 st2 + else + let* (st1, _) = + betree_store_leaf_node_fwd node.betree_leaf_id content0 st0 in + Return (st1, ()) + end + +(** [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) + (msgs : betree_list_t (u64 & betree_message_t)) (st : state) (st0 : state) : + Tot (result (state & (betree_node_t & betree_node_id_counter_t))) + (decreases ( + betree_node_apply_messages_decreases self params node_id_cnt msgs st)) + = + begin match self with + | BetreeNodeInternal node -> + let* (st1, content) = + betree_load_internal_node_fwd node.betree_internal_id st in + let* content0 = + betree_node_apply_messages_to_internal_fwd_back content msgs in + let* num_msgs = betree_list_len_fwd (u64 & betree_message_t) content0 in + if num_msgs >= params.betree_params_min_flush_size + then + let* (st2, content1) = + betree_internal_flush_fwd node params node_id_cnt content0 st1 in + let* (st3, (node0, node_id_cnt0)) = + betree_internal_flush_back'a node params node_id_cnt content0 st1 st2 + in + let* _ = + betree_store_internal_node_fwd node0.betree_internal_id content1 st3 in + Return (st0, (BetreeNodeInternal node0, node_id_cnt0)) + else + let* _ = + betree_store_internal_node_fwd node.betree_internal_id content0 st1 in + Return (st0, (BetreeNodeInternal node, node_id_cnt)) + | BetreeNodeLeaf node -> + let* (st1, content) = betree_load_leaf_node_fwd node.betree_leaf_id st in + let* content0 = betree_node_apply_messages_to_leaf_fwd_back content msgs in + let* len = betree_list_len_fwd (u64 & u64) content0 in + let* i = u64_mul 2 params.betree_params_split_size in + if len >= i + then + let* (st2, new_node) = + betree_leaf_split_fwd node content0 params node_id_cnt st1 in + let* (st3, _) = + betree_store_leaf_node_fwd node.betree_leaf_id BetreeListNil st2 in + let* _ = betree_leaf_split_back0 node content0 params node_id_cnt st1 st3 + in + let* (st4, node_id_cnt0) = + betree_leaf_split_back2 node content0 params node_id_cnt st1 st0 in + Return (st4, (BetreeNodeInternal new_node, node_id_cnt0)) + else + let* _ = betree_store_leaf_node_fwd node.betree_leaf_id content0 st1 in + Return (st0, (BetreeNodeLeaf { node with betree_leaf_size = len }, + node_id_cnt)) + end + +(** [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) + (msgs : betree_list_t (u64 & betree_message_t)) (st : state) (st0 : state) : + Tot (result (state & unit)) + (decreases ( + betree_node_apply_messages_decreases self params node_id_cnt msgs st)) + = + begin match self with + | BetreeNodeInternal node -> + let* (st1, content) = + betree_load_internal_node_fwd node.betree_internal_id st in + let* content0 = + betree_node_apply_messages_to_internal_fwd_back content msgs in + let* num_msgs = betree_list_len_fwd (u64 & betree_message_t) content0 in + if num_msgs >= params.betree_params_min_flush_size + then + let* (st2, content1) = + betree_internal_flush_fwd node params node_id_cnt content0 st1 in + let* (st3, (node0, _)) = + betree_internal_flush_back'a node params node_id_cnt content0 st1 st2 + in + let* _ = + betree_store_internal_node_fwd node0.betree_internal_id content1 st3 in + betree_internal_flush_back1 node params node_id_cnt content0 st1 st0 + else + let* _ = + betree_store_internal_node_fwd node.betree_internal_id content0 st1 in + Return (st0, ()) + | BetreeNodeLeaf node -> + let* (st1, content) = betree_load_leaf_node_fwd node.betree_leaf_id st in + let* content0 = betree_node_apply_messages_to_leaf_fwd_back content msgs in + let* len = betree_list_len_fwd (u64 & u64) content0 in + let* i = u64_mul 2 params.betree_params_split_size in + if len >= i + then + let* (st2, _) = + betree_leaf_split_fwd node content0 params node_id_cnt st1 in + let* (st3, _) = + betree_store_leaf_node_fwd node.betree_leaf_id BetreeListNil st2 in + let* _ = betree_leaf_split_back0 node content0 params node_id_cnt st1 st3 + in + betree_leaf_split_back1 node content0 params node_id_cnt st1 st0 + else + let* _ = betree_store_leaf_node_fwd node.betree_leaf_id content0 st1 in + Return (st0, ()) + end + (** [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_back_stateful/BetreeMain.Types.fsti b/tests/fstar/betree_back_stateful/BetreeMain.Types.fsti index aad9cb43..a937c726 100644 --- a/tests/fstar/betree_back_stateful/BetreeMain.Types.fsti +++ b/tests/fstar/betree_back_stateful/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 = { diff --git a/tests/fstar/misc/NoNestedBorrows.fst b/tests/fstar/misc/NoNestedBorrows.fst index d790bfa9..2cdd6e21 100644 --- a/tests/fstar/misc/NoNestedBorrows.fst +++ b/tests/fstar/misc/NoNestedBorrows.fst @@ -202,16 +202,16 @@ let _ = assert_norm (choose_test_fwd = Return ()) let test_char_fwd : result char = Return 'a' -(** [no_nested_borrows::NodeElem] *) -type node_elem_t (t : Type0) = -| NodeElemCons : tree_t t -> node_elem_t t -> node_elem_t t -| NodeElemNil : node_elem_t t - (** [no_nested_borrows::Tree] *) -and tree_t (t : Type0) = +type tree_t (t : Type0) = | TreeLeaf : t -> tree_t t | TreeNode : t -> node_elem_t t -> tree_t t -> tree_t t +(** [no_nested_borrows::NodeElem] *) +and node_elem_t (t : Type0) = +| NodeElemCons : tree_t t -> node_elem_t t -> node_elem_t t +| NodeElemNil : node_elem_t t + (** [no_nested_borrows::list_length]: forward function *) let rec list_length_fwd (t : Type0) (l : list_t t) : result u32 = begin match l with |