summaryrefslogtreecommitdiff
path: root/tests/fstar
diff options
context:
space:
mode:
authorSon Ho2023-08-08 17:50:16 +0200
committerSon Ho2023-08-08 17:50:16 +0200
commit77f309cec8e2f119272640083bc3476e4121952c (patch)
tree79451f2f2b2d5e26ab0ad067b0bfe3c598f58a29 /tests/fstar
parent6cdbb77f2be6f349729e2fd075ca3c51e9365b4f (diff)
Regenerate the test files
Diffstat (limited to 'tests/fstar')
-rw-r--r--tests/fstar/betree/BetreeMain.Clauses.Template.fst46
-rw-r--r--tests/fstar/betree/BetreeMain.Funs.fst434
-rw-r--r--tests/fstar/betree/BetreeMain.Types.fsti12
-rw-r--r--tests/fstar/betree_back_stateful/BetreeMain.Clauses.Template.fst46
-rw-r--r--tests/fstar/betree_back_stateful/BetreeMain.Funs.fst556
-rw-r--r--tests/fstar/betree_back_stateful/BetreeMain.Types.fsti12
-rw-r--r--tests/fstar/misc/NoNestedBorrows.fst12
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