diff options
author | Son Ho | 2023-11-21 11:50:44 +0100 |
---|---|---|
committer | Son Ho | 2023-11-21 11:50:44 +0100 |
commit | 753f7e72f87f5282aee60ad5ada47efeb42625e9 (patch) | |
tree | 85805dddd48eacaaac9f482c4c969469e92d73f9 /tests/fstar | |
parent | 46ab0fc047c69d14e52415bd8b76be167771cd58 (diff) |
Regenerate the betree files
Diffstat (limited to 'tests/fstar')
-rw-r--r-- | tests/fstar/betree/BetreeMain.Clauses.Template.fst | 32 | ||||
-rw-r--r-- | tests/fstar/betree/BetreeMain.Clauses.fst | 2 | ||||
-rw-r--r-- | tests/fstar/betree/BetreeMain.Funs.fst | 118 | ||||
-rw-r--r-- | tests/fstar/betree/BetreeMain.Opaque.fsti | 2 | ||||
-rw-r--r-- | tests/fstar/betree_back_stateful/BetreeMain.Clauses.Template.fst | 32 | ||||
-rw-r--r-- | tests/fstar/betree_back_stateful/BetreeMain.Clauses.fst | 2 | ||||
-rw-r--r-- | tests/fstar/betree_back_stateful/BetreeMain.Funs.fst | 131 | ||||
-rw-r--r-- | tests/fstar/betree_back_stateful/BetreeMain.Opaque.fsti | 2 |
8 files changed, 163 insertions, 158 deletions
diff --git a/tests/fstar/betree/BetreeMain.Clauses.Template.fst b/tests/fstar/betree/BetreeMain.Clauses.Template.fst index 8722f0bf..4d16d8d3 100644 --- a/tests/fstar/betree/BetreeMain.Clauses.Template.fst +++ b/tests/fstar/betree/BetreeMain.Clauses.Template.fst @@ -6,94 +6,94 @@ open BetreeMain.Types #set-options "--z3rlimit 50 --fuel 1 --ifuel 1" -(** [betree_main::betree::List::{1}::len]: decreases clause *) +(** [betree_main::betree::{betree_main::betree::List<T>#1}::len]: decreases clause *) unfold let betree_List_len_decreases (t : Type0) (self : betree_List_t t) : nat = admit () -(** [betree_main::betree::List::{1}::split_at]: decreases clause *) +(** [betree_main::betree::{betree_main::betree::List<T>#1}::split_at]: decreases clause *) unfold let betree_List_split_at_decreases (t : Type0) (self : betree_List_t t) (n : u64) : nat = admit () -(** [betree_main::betree::List::{2}::partition_at_pivot]: decreases clause *) +(** [betree_main::betree::{betree_main::betree::List<(u64, T)>#2}::partition_at_pivot]: decreases clause *) unfold -let betree_List_partition_at_pivot_decreases (t : Type0) +let betree_ListTupleU64T_partition_at_pivot_decreases (t : Type0) (self : betree_List_t (u64 & t)) (pivot : u64) : nat = admit () -(** [betree_main::betree::Node::{5}::lookup_first_message_for_key]: decreases clause *) +(** [betree_main::betree::{betree_main::betree::Node#5}::lookup_first_message_for_key]: decreases clause *) unfold let betree_Node_lookup_first_message_for_key_decreases (key : u64) (msgs : betree_List_t (u64 & betree_Message_t)) : nat = admit () -(** [betree_main::betree::Node::{5}::apply_upserts]: decreases clause *) +(** [betree_main::betree::{betree_main::betree::Node#5}::apply_upserts]: decreases clause *) unfold let betree_Node_apply_upserts_decreases (msgs : betree_List_t (u64 & betree_Message_t)) (prev : option u64) (key : u64) (st : state) : nat = admit () -(** [betree_main::betree::Node::{5}::lookup_in_bindings]: decreases clause *) +(** [betree_main::betree::{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::Internal::{4}::lookup_in_children]: decreases clause *) +(** [betree_main::betree::{betree_main::betree::Internal#4}::lookup_in_children]: decreases clause *) unfold let betree_Internal_lookup_in_children_decreases (self : betree_Internal_t) (key : u64) (st : state) : nat = admit () -(** [betree_main::betree::Node::{5}::lookup]: decreases clause *) +(** [betree_main::betree::{betree_main::betree::Node#5}::lookup]: decreases clause *) unfold 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 *) +(** [betree_main::betree::{betree_main::betree::Node#5}::filter_messages_for_key]: decreases clause *) unfold let betree_Node_filter_messages_for_key_decreases (key : u64) (msgs : betree_List_t (u64 & betree_Message_t)) : nat = admit () -(** [betree_main::betree::Node::{5}::lookup_first_message_after_key]: decreases clause *) +(** [betree_main::betree::{betree_main::betree::Node#5}::lookup_first_message_after_key]: decreases clause *) unfold let betree_Node_lookup_first_message_after_key_decreases (key : u64) (msgs : betree_List_t (u64 & betree_Message_t)) : nat = admit () -(** [betree_main::betree::Node::{5}::apply_messages_to_internal]: decreases clause *) +(** [betree_main::betree::{betree_main::betree::Node#5}::apply_messages_to_internal]: decreases clause *) unfold let betree_Node_apply_messages_to_internal_decreases (msgs : betree_List_t (u64 & betree_Message_t)) (new_msgs : betree_List_t (u64 & betree_Message_t)) : nat = admit () -(** [betree_main::betree::Node::{5}::lookup_mut_in_bindings]: decreases clause *) +(** [betree_main::betree::{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::{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 *) +(** [betree_main::betree::{betree_main::betree::Internal#4}::flush]: decreases clause *) unfold let betree_Internal_flush_decreases (self : betree_Internal_t) (params : betree_Params_t) (node_id_cnt : betree_NodeIdCounter_t) (content : betree_List_t (u64 & betree_Message_t)) (st : state) : nat = admit () -(** [betree_main::betree::Node::{5}::apply_messages]: decreases clause *) +(** [betree_main::betree::{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_NodeIdCounter_t) diff --git a/tests/fstar/betree/BetreeMain.Clauses.fst b/tests/fstar/betree/BetreeMain.Clauses.fst index cda7b920..21f953d1 100644 --- a/tests/fstar/betree/BetreeMain.Clauses.fst +++ b/tests/fstar/betree/BetreeMain.Clauses.fst @@ -114,7 +114,7 @@ let betree_List_split_at_decreases (t : Type0) (self : betree_List_t t) (** [betree_main::betree::List::{2}::partition_at_pivot]: decreases clause *) unfold -let betree_List_partition_at_pivot_decreases (t : Type0) +let betree_ListTupleU64T_partition_at_pivot_decreases (t : Type0) (self : betree_List_t (u64 & t)) (pivot : u64) : betree_List_t (u64 & t) = self diff --git a/tests/fstar/betree/BetreeMain.Funs.fst b/tests/fstar/betree/BetreeMain.Funs.fst index d2bf5c7c..2ccbac60 100644 --- a/tests/fstar/betree/BetreeMain.Funs.fst +++ b/tests/fstar/betree/BetreeMain.Funs.fst @@ -44,16 +44,16 @@ let betree_fresh_node_id (counter : u64) : result u64 = let betree_fresh_node_id_back (counter : u64) : result u64 = u64_add counter 1 -(** [betree_main::betree::NodeIdCounter::{0}::new]: forward function *) +(** [betree_main::betree::{betree_main::betree::NodeIdCounter}::new]: forward function *) let betree_NodeIdCounter_new : result betree_NodeIdCounter_t = Return { next_node_id = 0 } -(** [betree_main::betree::NodeIdCounter::{0}::fresh_id]: forward function *) +(** [betree_main::betree::{betree_main::betree::NodeIdCounter}::fresh_id]: forward function *) let betree_NodeIdCounter_fresh_id (self : betree_NodeIdCounter_t) : result u64 = let* _ = u64_add self.next_node_id 1 in Return self.next_node_id -(** [betree_main::betree::NodeIdCounter::{0}::fresh_id]: backward function 0 *) +(** [betree_main::betree::{betree_main::betree::NodeIdCounter}::fresh_id]: backward function 0 *) let betree_NodeIdCounter_fresh_id_back (self : betree_NodeIdCounter_t) : result betree_NodeIdCounter_t = let* i = u64_add self.next_node_id 1 in Return { next_node_id = i } @@ -77,7 +77,7 @@ let betree_upsert_update end end -(** [betree_main::betree::List::{1}::len]: forward function *) +(** [betree_main::betree::{betree_main::betree::List<T>#1}::len]: forward function *) let rec betree_List_len (t : Type0) (self : betree_List_t t) : Tot (result u64) (decreases (betree_List_len_decreases t self)) @@ -87,7 +87,7 @@ let rec betree_List_len | Betree_List_Nil -> Return 0 end -(** [betree_main::betree::List::{1}::split_at]: forward function *) +(** [betree_main::betree::{betree_main::betree::List<T>#1}::split_at]: forward function *) let rec betree_List_split_at (t : Type0) (self : betree_List_t t) (n : u64) : Tot (result ((betree_List_t t) & (betree_List_t t))) @@ -106,7 +106,7 @@ let rec betree_List_split_at | Betree_List_Nil -> Fail Failure end -(** [betree_main::betree::List::{1}::push_front]: merged forward/backward function +(** [betree_main::betree::{betree_main::betree::List<T>#1}::push_front]: merged forward/backward function (there is a single backward function, and the forward function returns ()) *) let betree_List_push_front (t : Type0) (self : betree_List_t t) (x : t) : result (betree_List_t t) = @@ -114,7 +114,7 @@ let betree_List_push_front let l = tl in Return (Betree_List_Cons x l) -(** [betree_main::betree::List::{1}::pop_front]: forward function *) +(** [betree_main::betree::{betree_main::betree::List<T>#1}::pop_front]: forward function *) let betree_List_pop_front (t : Type0) (self : betree_List_t t) : result t = let ls = core_mem_replace (betree_List_t t) self Betree_List_Nil in begin match ls with @@ -122,7 +122,7 @@ let betree_List_pop_front (t : Type0) (self : betree_List_t t) : result t = | Betree_List_Nil -> Fail Failure end -(** [betree_main::betree::List::{1}::pop_front]: backward function 0 *) +(** [betree_main::betree::{betree_main::betree::List<T>#1}::pop_front]: backward function 0 *) let betree_List_pop_front_back (t : Type0) (self : betree_List_t t) : result (betree_List_t t) = let ls = core_mem_replace (betree_List_t t) self Betree_List_Nil in @@ -131,26 +131,26 @@ let betree_List_pop_front_back | Betree_List_Nil -> Fail Failure end -(** [betree_main::betree::List::{1}::hd]: forward function *) +(** [betree_main::betree::{betree_main::betree::List<T>#1}::hd]: forward function *) let betree_List_hd (t : Type0) (self : betree_List_t t) : result t = begin match self with | Betree_List_Cons hd l -> Return hd | Betree_List_Nil -> Fail Failure end -(** [betree_main::betree::List::{2}::head_has_key]: forward function *) -let betree_List_head_has_key +(** [betree_main::betree::{betree_main::betree::List<(u64, T)>#2}::head_has_key]: forward function *) +let betree_ListTupleU64T_head_has_key (t : Type0) (self : betree_List_t (u64 & t)) (key : u64) : result bool = begin match self with | Betree_List_Cons hd l -> let (i, _) = hd in Return (i = key) | Betree_List_Nil -> Return false end -(** [betree_main::betree::List::{2}::partition_at_pivot]: forward function *) -let rec betree_List_partition_at_pivot +(** [betree_main::betree::{betree_main::betree::List<(u64, T)>#2}::partition_at_pivot]: forward function *) +let rec betree_ListTupleU64T_partition_at_pivot (t : Type0) (self : betree_List_t (u64 & t)) (pivot : u64) : Tot (result ((betree_List_t (u64 & t)) & (betree_List_t (u64 & t)))) - (decreases (betree_List_partition_at_pivot_decreases t self pivot)) + (decreases (betree_ListTupleU64T_partition_at_pivot_decreases t self pivot)) = begin match self with | Betree_List_Cons hd tl -> @@ -158,14 +158,14 @@ let rec betree_List_partition_at_pivot if i >= pivot then Return (Betree_List_Nil, Betree_List_Cons (i, x) tl) else - let* p = betree_List_partition_at_pivot t tl pivot in + let* p = betree_ListTupleU64T_partition_at_pivot t tl pivot in let (ls0, ls1) = p in let l = ls0 in Return (Betree_List_Cons (i, x) l, ls1) | Betree_List_Nil -> Return (Betree_List_Nil, Betree_List_Nil) end -(** [betree_main::betree::Leaf::{3}::split]: forward function *) +(** [betree_main::betree::{betree_main::betree::Leaf#3}::split]: forward function *) let betree_Leaf_split (self : betree_Leaf_t) (content : betree_List_t (u64 & u64)) (params : betree_Params_t) (node_id_cnt : betree_NodeIdCounter_t) @@ -185,7 +185,7 @@ let betree_Leaf_split let n0 = Betree_Node_Leaf { id = id1; size = params.split_size } in Return (st1, { id = self.id; pivot = pivot; left = n; right = n0 }) -(** [betree_main::betree::Leaf::{3}::split]: backward function 2 *) +(** [betree_main::betree::{betree_main::betree::Leaf#3}::split]: backward function 2 *) let betree_Leaf_split_back (self : betree_Leaf_t) (content : betree_List_t (u64 & u64)) (params : betree_Params_t) (node_id_cnt : betree_NodeIdCounter_t) @@ -202,7 +202,7 @@ let betree_Leaf_split_back let* _ = betree_store_leaf_node id1 content1 st0 in betree_NodeIdCounter_fresh_id_back node_id_cnt0 -(** [betree_main::betree::Node::{5}::lookup_first_message_for_key]: forward function *) +(** [betree_main::betree::{betree_main::betree::Node#5}::lookup_first_message_for_key]: forward function *) let rec betree_Node_lookup_first_message_for_key (key : u64) (msgs : betree_List_t (u64 & betree_Message_t)) : Tot (result (betree_List_t (u64 & betree_Message_t))) @@ -217,7 +217,7 @@ let rec betree_Node_lookup_first_message_for_key | Betree_List_Nil -> Return Betree_List_Nil end -(** [betree_main::betree::Node::{5}::lookup_first_message_for_key]: backward function 0 *) +(** [betree_main::betree::{betree_main::betree::Node#5}::lookup_first_message_for_key]: backward function 0 *) let rec betree_Node_lookup_first_message_for_key_back (key : u64) (msgs : betree_List_t (u64 & betree_Message_t)) (ret : betree_List_t (u64 & betree_Message_t)) : @@ -236,14 +236,14 @@ let rec betree_Node_lookup_first_message_for_key_back | Betree_List_Nil -> Return ret end -(** [betree_main::betree::Node::{5}::apply_upserts]: forward function *) +(** [betree_main::betree::{betree_main::betree::Node#5}::apply_upserts]: forward function *) let rec betree_Node_apply_upserts (msgs : betree_List_t (u64 & betree_Message_t)) (prev : option u64) (key : u64) (st : state) : Tot (result (state & u64)) (decreases (betree_Node_apply_upserts_decreases msgs prev key st)) = - let* b = betree_List_head_has_key betree_Message_t msgs key in + let* b = betree_ListTupleU64T_head_has_key betree_Message_t msgs key in if b then let* msg = betree_List_pop_front (u64 & betree_Message_t) msgs in @@ -263,14 +263,14 @@ let rec betree_Node_apply_upserts Betree_Message_Insert v) in Return (st0, v) -(** [betree_main::betree::Node::{5}::apply_upserts]: backward function 0 *) +(** [betree_main::betree::{betree_main::betree::Node#5}::apply_upserts]: backward function 0 *) let rec betree_Node_apply_upserts_back (msgs : betree_List_t (u64 & betree_Message_t)) (prev : option u64) (key : u64) (st : state) : Tot (result (betree_List_t (u64 & betree_Message_t))) (decreases (betree_Node_apply_upserts_decreases msgs prev key st)) = - let* b = betree_List_head_has_key betree_Message_t msgs key in + let* b = betree_ListTupleU64T_head_has_key betree_Message_t msgs key in if b then let* msg = betree_List_pop_front (u64 & betree_Message_t) msgs in @@ -288,7 +288,7 @@ let rec betree_Node_apply_upserts_back betree_List_push_front (u64 & betree_Message_t) msgs (key, Betree_Message_Insert v) -(** [betree_main::betree::Node::{5}::lookup_in_bindings]: forward function *) +(** [betree_main::betree::{betree_main::betree::Node#5}::lookup_in_bindings]: forward function *) let rec betree_Node_lookup_in_bindings (key : u64) (bindings : betree_List_t (u64 & u64)) : Tot (result (option u64)) @@ -303,7 +303,7 @@ let rec betree_Node_lookup_in_bindings | Betree_List_Nil -> Return None end -(** [betree_main::betree::Internal::{4}::lookup_in_children]: forward function *) +(** [betree_main::betree::{betree_main::betree::Internal#4}::lookup_in_children]: forward function *) let rec betree_Internal_lookup_in_children (self : betree_Internal_t) (key : u64) (st : state) : Tot (result (state & (option u64))) @@ -313,7 +313,7 @@ let rec betree_Internal_lookup_in_children then betree_Node_lookup self.left key st else betree_Node_lookup self.right key st -(** [betree_main::betree::Internal::{4}::lookup_in_children]: backward function 0 *) +(** [betree_main::betree::{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) @@ -327,7 +327,7 @@ and betree_Internal_lookup_in_children_back let* n = betree_Node_lookup_back self.right key st in Return { self with right = n } -(** [betree_main::betree::Node::{5}::lookup]: forward function *) +(** [betree_main::betree::{betree_main::betree::Node#5}::lookup]: forward function *) and betree_Node_lookup (self : betree_Node_t) (key : u64) (st : state) : Tot (result (state & (option u64))) @@ -386,7 +386,7 @@ and betree_Node_lookup Return (st0, o) end -(** [betree_main::betree::Node::{5}::lookup]: backward function 0 *) +(** [betree_main::betree::{betree_main::betree::Node#5}::lookup]: backward function 0 *) and betree_Node_lookup_back (self : betree_Node_t) (key : u64) (st : state) : Tot (result betree_Node_t) @@ -445,7 +445,7 @@ and betree_Node_lookup_back Return (Betree_Node_Leaf node) end -(** [betree_main::betree::Node::{5}::filter_messages_for_key]: merged forward/backward function +(** [betree_main::betree::{betree_main::betree::Node#5}::filter_messages_for_key]: merged forward/backward function (there is a single backward function, and the forward function returns ()) *) let rec betree_Node_filter_messages_for_key (key : u64) (msgs : betree_List_t (u64 & betree_Message_t)) : @@ -465,7 +465,7 @@ let rec betree_Node_filter_messages_for_key | Betree_List_Nil -> Return Betree_List_Nil end -(** [betree_main::betree::Node::{5}::lookup_first_message_after_key]: forward function *) +(** [betree_main::betree::{betree_main::betree::Node#5}::lookup_first_message_after_key]: forward function *) let rec betree_Node_lookup_first_message_after_key (key : u64) (msgs : betree_List_t (u64 & betree_Message_t)) : Tot (result (betree_List_t (u64 & betree_Message_t))) @@ -480,7 +480,7 @@ let rec betree_Node_lookup_first_message_after_key | Betree_List_Nil -> Return Betree_List_Nil end -(** [betree_main::betree::Node::{5}::lookup_first_message_after_key]: backward function 0 *) +(** [betree_main::betree::{betree_main::betree::Node#5}::lookup_first_message_after_key]: backward function 0 *) let rec betree_Node_lookup_first_message_after_key_back (key : u64) (msgs : betree_List_t (u64 & betree_Message_t)) (ret : betree_List_t (u64 & betree_Message_t)) : @@ -499,7 +499,7 @@ let rec betree_Node_lookup_first_message_after_key_back | Betree_List_Nil -> Return ret end -(** [betree_main::betree::Node::{5}::apply_to_internal]: merged forward/backward function +(** [betree_main::betree::{betree_main::betree::Node#5}::apply_to_internal]: merged forward/backward function (there is a single backward function, and the forward function returns ()) *) let betree_Node_apply_to_internal (msgs : betree_List_t (u64 & betree_Message_t)) (key : u64) @@ -507,7 +507,7 @@ let betree_Node_apply_to_internal result (betree_List_t (u64 & betree_Message_t)) = let* msgs0 = betree_Node_lookup_first_message_for_key key msgs in - let* b = betree_List_head_has_key betree_Message_t msgs0 key in + let* b = betree_ListTupleU64T_head_has_key betree_Message_t msgs0 key in if b then begin match new_msg with @@ -558,7 +558,7 @@ let betree_Node_apply_to_internal betree_List_push_front (u64 & betree_Message_t) msgs0 (key, new_msg) in betree_Node_lookup_first_message_for_key_back key msgs msgs1 -(** [betree_main::betree::Node::{5}::apply_messages_to_internal]: merged forward/backward function +(** [betree_main::betree::{betree_main::betree::Node#5}::apply_messages_to_internal]: merged forward/backward function (there is a single backward function, and the forward function returns ()) *) let rec betree_Node_apply_messages_to_internal (msgs : betree_List_t (u64 & betree_Message_t)) @@ -574,7 +574,7 @@ let rec betree_Node_apply_messages_to_internal | Betree_List_Nil -> Return msgs end -(** [betree_main::betree::Node::{5}::lookup_mut_in_bindings]: forward function *) +(** [betree_main::betree::{betree_main::betree::Node#5}::lookup_mut_in_bindings]: forward function *) let rec betree_Node_lookup_mut_in_bindings (key : u64) (bindings : betree_List_t (u64 & u64)) : Tot (result (betree_List_t (u64 & u64))) @@ -589,7 +589,7 @@ let rec betree_Node_lookup_mut_in_bindings | Betree_List_Nil -> Return Betree_List_Nil end -(** [betree_main::betree::Node::{5}::lookup_mut_in_bindings]: backward function 0 *) +(** [betree_main::betree::{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)) : @@ -607,7 +607,7 @@ let rec betree_Node_lookup_mut_in_bindings_back | Betree_List_Nil -> Return ret end -(** [betree_main::betree::Node::{5}::apply_to_leaf]: merged forward/backward function +(** [betree_main::betree::{betree_main::betree::Node#5}::apply_to_leaf]: merged forward/backward function (there is a single backward function, and the forward function returns ()) *) let betree_Node_apply_to_leaf (bindings : betree_List_t (u64 & u64)) (key : u64) @@ -615,7 +615,7 @@ let betree_Node_apply_to_leaf result (betree_List_t (u64 & u64)) = let* bindings0 = betree_Node_lookup_mut_in_bindings key bindings in - let* b = betree_List_head_has_key u64 bindings0 key in + let* b = betree_ListTupleU64T_head_has_key u64 bindings0 key in if b then let* hd = betree_List_pop_front (u64 & u64) bindings0 in @@ -647,7 +647,7 @@ let betree_Node_apply_to_leaf betree_Node_lookup_mut_in_bindings_back key bindings bindings1 end -(** [betree_main::betree::Node::{5}::apply_messages_to_leaf]: merged forward/backward function +(** [betree_main::betree::{betree_main::betree::Node#5}::apply_messages_to_leaf]: merged forward/backward function (there is a single backward function, and the forward function returns ()) *) let rec betree_Node_apply_messages_to_leaf (bindings : betree_List_t (u64 & u64)) @@ -663,7 +663,7 @@ let rec betree_Node_apply_messages_to_leaf | Betree_List_Nil -> Return bindings end -(** [betree_main::betree::Internal::{4}::flush]: forward function *) +(** [betree_main::betree::{betree_main::betree::Internal#4}::flush]: forward function *) let rec betree_Internal_flush (self : betree_Internal_t) (params : betree_Params_t) (node_id_cnt : betree_NodeIdCounter_t) @@ -672,7 +672,8 @@ let rec betree_Internal_flush (decreases ( betree_Internal_flush_decreases self params node_id_cnt content st)) = - let* p = betree_List_partition_at_pivot betree_Message_t content self.pivot + let* p = + betree_ListTupleU64T_partition_at_pivot betree_Message_t content self.pivot in let (msgs_left, msgs_right) = p in let* len_left = betree_List_len (u64 & betree_Message_t) msgs_left in @@ -702,7 +703,7 @@ let rec betree_Internal_flush st in Return (st0, msgs_left) -(** [betree_main::betree::Internal::{4}::flush]: backward function 0 *) +(** [betree_main::betree::{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_NodeIdCounter_t) @@ -711,7 +712,8 @@ and betree_Internal_flush_back (decreases ( betree_Internal_flush_decreases self params node_id_cnt content st)) = - let* p = betree_List_partition_at_pivot betree_Message_t content self.pivot + let* p = + betree_ListTupleU64T_partition_at_pivot betree_Message_t content self.pivot in let (msgs_left, msgs_right) = p in let* len_left = betree_List_len (u64 & betree_Message_t) msgs_left in @@ -736,7 +738,7 @@ and betree_Internal_flush_back st in Return ({ self with right = n }, node_id_cnt0) -(** [betree_main::betree::Node::{5}::apply_messages]: forward function *) +(** [betree_main::betree::{betree_main::betree::Node#5}::apply_messages]: forward function *) and betree_Node_apply_messages (self : betree_Node_t) (params : betree_Params_t) (node_id_cnt : betree_NodeIdCounter_t) @@ -776,7 +778,7 @@ and betree_Node_apply_messages Return (st1, ()) end -(** [betree_main::betree::Node::{5}::apply_messages]: backward function 0 *) +(** [betree_main::betree::{betree_main::betree::Node#5}::apply_messages]: backward function 0 *) and betree_Node_apply_messages_back (self : betree_Node_t) (params : betree_Params_t) (node_id_cnt : betree_NodeIdCounter_t) @@ -819,7 +821,7 @@ and betree_Node_apply_messages_back Return (Betree_Node_Leaf { node with size = len }, node_id_cnt) end -(** [betree_main::betree::Node::{5}::apply]: forward function *) +(** [betree_main::betree::{betree_main::betree::Node#5}::apply]: forward function *) let betree_Node_apply (self : betree_Node_t) (params : betree_Params_t) (node_id_cnt : betree_NodeIdCounter_t) (key : u64) @@ -835,7 +837,7 @@ let betree_Node_apply (key, new_msg) l) st in Return (st0, ()) -(** [betree_main::betree::Node::{5}::apply]: backward function 0 *) +(** [betree_main::betree::{betree_main::betree::Node#5}::apply]: backward function 0 *) let betree_Node_apply_back (self : betree_Node_t) (params : betree_Params_t) (node_id_cnt : betree_NodeIdCounter_t) (key : u64) @@ -846,7 +848,7 @@ let betree_Node_apply_back betree_Node_apply_messages_back self params node_id_cnt (Betree_List_Cons (key, new_msg) l) st -(** [betree_main::betree::BeTree::{6}::new]: forward function *) +(** [betree_main::betree::{betree_main::betree::BeTree#6}::new]: forward function *) let betree_BeTree_new (min_flush_size : u64) (split_size : u64) (st : state) : result (state & betree_BeTree_t) @@ -862,7 +864,7 @@ let betree_BeTree_new root = (Betree_Node_Leaf { id = id; size = 0 }) }) -(** [betree_main::betree::BeTree::{6}::apply]: forward function *) +(** [betree_main::betree::{betree_main::betree::BeTree#6}::apply]: forward function *) let betree_BeTree_apply (self : betree_BeTree_t) (key : u64) (msg : betree_Message_t) (st : state) : result (state & unit) @@ -873,7 +875,7 @@ let betree_BeTree_apply betree_Node_apply_back self.root self.params self.node_id_cnt key msg st in Return (st0, ()) -(** [betree_main::betree::BeTree::{6}::apply]: backward function 0 *) +(** [betree_main::betree::{betree_main::betree::BeTree#6}::apply]: backward function 0 *) let betree_BeTree_apply_back (self : betree_BeTree_t) (key : u64) (msg : betree_Message_t) (st : state) : result betree_BeTree_t @@ -882,7 +884,7 @@ let betree_BeTree_apply_back betree_Node_apply_back self.root self.params self.node_id_cnt key msg st in Return { self with node_id_cnt = nic; root = n } -(** [betree_main::betree::BeTree::{6}::insert]: forward function *) +(** [betree_main::betree::{betree_main::betree::BeTree#6}::insert]: forward function *) let betree_BeTree_insert (self : betree_BeTree_t) (key : u64) (value : u64) (st : state) : result (state & unit) @@ -893,26 +895,26 @@ let betree_BeTree_insert in Return (st0, ()) -(** [betree_main::betree::BeTree::{6}::insert]: backward function 0 *) +(** [betree_main::betree::{betree_main::betree::BeTree#6}::insert]: backward function 0 *) let betree_BeTree_insert_back (self : betree_BeTree_t) (key : u64) (value : u64) (st : state) : result betree_BeTree_t = betree_BeTree_apply_back self key (Betree_Message_Insert value) st -(** [betree_main::betree::BeTree::{6}::delete]: forward function *) +(** [betree_main::betree::{betree_main::betree::BeTree#6}::delete]: forward function *) let betree_BeTree_delete (self : betree_BeTree_t) (key : u64) (st : state) : result (state & unit) = let* (st0, _) = betree_BeTree_apply self key Betree_Message_Delete st in let* _ = betree_BeTree_apply_back self key Betree_Message_Delete st in Return (st0, ()) -(** [betree_main::betree::BeTree::{6}::delete]: backward function 0 *) +(** [betree_main::betree::{betree_main::betree::BeTree#6}::delete]: backward function 0 *) let betree_BeTree_delete_back (self : betree_BeTree_t) (key : u64) (st : state) : result betree_BeTree_t = betree_BeTree_apply_back self key Betree_Message_Delete st -(** [betree_main::betree::BeTree::{6}::upsert]: forward function *) +(** [betree_main::betree::{betree_main::betree::BeTree#6}::upsert]: forward function *) let betree_BeTree_upsert (self : betree_BeTree_t) (key : u64) (upd : betree_UpsertFunState_t) (st : state) : @@ -923,7 +925,7 @@ let betree_BeTree_upsert let* _ = betree_BeTree_apply_back self key (Betree_Message_Upsert upd) st in Return (st0, ()) -(** [betree_main::betree::BeTree::{6}::upsert]: backward function 0 *) +(** [betree_main::betree::{betree_main::betree::BeTree#6}::upsert]: backward function 0 *) let betree_BeTree_upsert_back (self : betree_BeTree_t) (key : u64) (upd : betree_UpsertFunState_t) (st : state) : @@ -931,14 +933,14 @@ let betree_BeTree_upsert_back = betree_BeTree_apply_back self key (Betree_Message_Upsert upd) st -(** [betree_main::betree::BeTree::{6}::lookup]: forward function *) +(** [betree_main::betree::{betree_main::betree::BeTree#6}::lookup]: forward function *) let betree_BeTree_lookup (self : betree_BeTree_t) (key : u64) (st : state) : result (state & (option u64)) = betree_Node_lookup self.root key st -(** [betree_main::betree::BeTree::{6}::lookup]: backward function 0 *) +(** [betree_main::betree::{betree_main::betree::BeTree#6}::lookup]: backward function 0 *) let betree_BeTree_lookup_back (self : betree_BeTree_t) (key : u64) (st : state) : result betree_BeTree_t = let* n = betree_Node_lookup_back self.root key st in diff --git a/tests/fstar/betree/BetreeMain.Opaque.fsti b/tests/fstar/betree/BetreeMain.Opaque.fsti index c5d0a814..23d2e60e 100644 --- a/tests/fstar/betree/BetreeMain.Opaque.fsti +++ b/tests/fstar/betree/BetreeMain.Opaque.fsti @@ -24,7 +24,7 @@ val betree_utils_load_leaf_node val betree_utils_store_leaf_node : u64 -> betree_List_t (u64 & u64) -> state -> result (state & unit) -(** [core::option::Option::{0}::unwrap]: forward function *) +(** [core::option::{core::option::Option<T>}::unwrap]: forward function *) val core_option_Option_unwrap (t : Type0) : option t -> state -> result (state & t) diff --git a/tests/fstar/betree_back_stateful/BetreeMain.Clauses.Template.fst b/tests/fstar/betree_back_stateful/BetreeMain.Clauses.Template.fst index 8722f0bf..4d16d8d3 100644 --- a/tests/fstar/betree_back_stateful/BetreeMain.Clauses.Template.fst +++ b/tests/fstar/betree_back_stateful/BetreeMain.Clauses.Template.fst @@ -6,94 +6,94 @@ open BetreeMain.Types #set-options "--z3rlimit 50 --fuel 1 --ifuel 1" -(** [betree_main::betree::List::{1}::len]: decreases clause *) +(** [betree_main::betree::{betree_main::betree::List<T>#1}::len]: decreases clause *) unfold let betree_List_len_decreases (t : Type0) (self : betree_List_t t) : nat = admit () -(** [betree_main::betree::List::{1}::split_at]: decreases clause *) +(** [betree_main::betree::{betree_main::betree::List<T>#1}::split_at]: decreases clause *) unfold let betree_List_split_at_decreases (t : Type0) (self : betree_List_t t) (n : u64) : nat = admit () -(** [betree_main::betree::List::{2}::partition_at_pivot]: decreases clause *) +(** [betree_main::betree::{betree_main::betree::List<(u64, T)>#2}::partition_at_pivot]: decreases clause *) unfold -let betree_List_partition_at_pivot_decreases (t : Type0) +let betree_ListTupleU64T_partition_at_pivot_decreases (t : Type0) (self : betree_List_t (u64 & t)) (pivot : u64) : nat = admit () -(** [betree_main::betree::Node::{5}::lookup_first_message_for_key]: decreases clause *) +(** [betree_main::betree::{betree_main::betree::Node#5}::lookup_first_message_for_key]: decreases clause *) unfold let betree_Node_lookup_first_message_for_key_decreases (key : u64) (msgs : betree_List_t (u64 & betree_Message_t)) : nat = admit () -(** [betree_main::betree::Node::{5}::apply_upserts]: decreases clause *) +(** [betree_main::betree::{betree_main::betree::Node#5}::apply_upserts]: decreases clause *) unfold let betree_Node_apply_upserts_decreases (msgs : betree_List_t (u64 & betree_Message_t)) (prev : option u64) (key : u64) (st : state) : nat = admit () -(** [betree_main::betree::Node::{5}::lookup_in_bindings]: decreases clause *) +(** [betree_main::betree::{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::Internal::{4}::lookup_in_children]: decreases clause *) +(** [betree_main::betree::{betree_main::betree::Internal#4}::lookup_in_children]: decreases clause *) unfold let betree_Internal_lookup_in_children_decreases (self : betree_Internal_t) (key : u64) (st : state) : nat = admit () -(** [betree_main::betree::Node::{5}::lookup]: decreases clause *) +(** [betree_main::betree::{betree_main::betree::Node#5}::lookup]: decreases clause *) unfold 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 *) +(** [betree_main::betree::{betree_main::betree::Node#5}::filter_messages_for_key]: decreases clause *) unfold let betree_Node_filter_messages_for_key_decreases (key : u64) (msgs : betree_List_t (u64 & betree_Message_t)) : nat = admit () -(** [betree_main::betree::Node::{5}::lookup_first_message_after_key]: decreases clause *) +(** [betree_main::betree::{betree_main::betree::Node#5}::lookup_first_message_after_key]: decreases clause *) unfold let betree_Node_lookup_first_message_after_key_decreases (key : u64) (msgs : betree_List_t (u64 & betree_Message_t)) : nat = admit () -(** [betree_main::betree::Node::{5}::apply_messages_to_internal]: decreases clause *) +(** [betree_main::betree::{betree_main::betree::Node#5}::apply_messages_to_internal]: decreases clause *) unfold let betree_Node_apply_messages_to_internal_decreases (msgs : betree_List_t (u64 & betree_Message_t)) (new_msgs : betree_List_t (u64 & betree_Message_t)) : nat = admit () -(** [betree_main::betree::Node::{5}::lookup_mut_in_bindings]: decreases clause *) +(** [betree_main::betree::{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::{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 *) +(** [betree_main::betree::{betree_main::betree::Internal#4}::flush]: decreases clause *) unfold let betree_Internal_flush_decreases (self : betree_Internal_t) (params : betree_Params_t) (node_id_cnt : betree_NodeIdCounter_t) (content : betree_List_t (u64 & betree_Message_t)) (st : state) : nat = admit () -(** [betree_main::betree::Node::{5}::apply_messages]: decreases clause *) +(** [betree_main::betree::{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_NodeIdCounter_t) diff --git a/tests/fstar/betree_back_stateful/BetreeMain.Clauses.fst b/tests/fstar/betree_back_stateful/BetreeMain.Clauses.fst index cda7b920..21f953d1 100644 --- a/tests/fstar/betree_back_stateful/BetreeMain.Clauses.fst +++ b/tests/fstar/betree_back_stateful/BetreeMain.Clauses.fst @@ -114,7 +114,7 @@ let betree_List_split_at_decreases (t : Type0) (self : betree_List_t t) (** [betree_main::betree::List::{2}::partition_at_pivot]: decreases clause *) unfold -let betree_List_partition_at_pivot_decreases (t : Type0) +let betree_ListTupleU64T_partition_at_pivot_decreases (t : Type0) (self : betree_List_t (u64 & t)) (pivot : u64) : betree_List_t (u64 & t) = self diff --git a/tests/fstar/betree_back_stateful/BetreeMain.Funs.fst b/tests/fstar/betree_back_stateful/BetreeMain.Funs.fst index 08c4f615..b46ca0a0 100644 --- a/tests/fstar/betree_back_stateful/BetreeMain.Funs.fst +++ b/tests/fstar/betree_back_stateful/BetreeMain.Funs.fst @@ -44,16 +44,16 @@ let betree_fresh_node_id (counter : u64) : result u64 = let betree_fresh_node_id_back (counter : u64) : result u64 = u64_add counter 1 -(** [betree_main::betree::NodeIdCounter::{0}::new]: forward function *) +(** [betree_main::betree::{betree_main::betree::NodeIdCounter}::new]: forward function *) let betree_NodeIdCounter_new : result betree_NodeIdCounter_t = Return { next_node_id = 0 } -(** [betree_main::betree::NodeIdCounter::{0}::fresh_id]: forward function *) +(** [betree_main::betree::{betree_main::betree::NodeIdCounter}::fresh_id]: forward function *) let betree_NodeIdCounter_fresh_id (self : betree_NodeIdCounter_t) : result u64 = let* _ = u64_add self.next_node_id 1 in Return self.next_node_id -(** [betree_main::betree::NodeIdCounter::{0}::fresh_id]: backward function 0 *) +(** [betree_main::betree::{betree_main::betree::NodeIdCounter}::fresh_id]: backward function 0 *) let betree_NodeIdCounter_fresh_id_back (self : betree_NodeIdCounter_t) : result betree_NodeIdCounter_t = let* i = u64_add self.next_node_id 1 in Return { next_node_id = i } @@ -77,7 +77,7 @@ let betree_upsert_update end end -(** [betree_main::betree::List::{1}::len]: forward function *) +(** [betree_main::betree::{betree_main::betree::List<T>#1}::len]: forward function *) let rec betree_List_len (t : Type0) (self : betree_List_t t) : Tot (result u64) (decreases (betree_List_len_decreases t self)) @@ -87,7 +87,7 @@ let rec betree_List_len | Betree_List_Nil -> Return 0 end -(** [betree_main::betree::List::{1}::split_at]: forward function *) +(** [betree_main::betree::{betree_main::betree::List<T>#1}::split_at]: forward function *) let rec betree_List_split_at (t : Type0) (self : betree_List_t t) (n : u64) : Tot (result ((betree_List_t t) & (betree_List_t t))) @@ -106,7 +106,7 @@ let rec betree_List_split_at | Betree_List_Nil -> Fail Failure end -(** [betree_main::betree::List::{1}::push_front]: merged forward/backward function +(** [betree_main::betree::{betree_main::betree::List<T>#1}::push_front]: merged forward/backward function (there is a single backward function, and the forward function returns ()) *) let betree_List_push_front (t : Type0) (self : betree_List_t t) (x : t) : result (betree_List_t t) = @@ -114,7 +114,7 @@ let betree_List_push_front let l = tl in Return (Betree_List_Cons x l) -(** [betree_main::betree::List::{1}::pop_front]: forward function *) +(** [betree_main::betree::{betree_main::betree::List<T>#1}::pop_front]: forward function *) let betree_List_pop_front (t : Type0) (self : betree_List_t t) : result t = let ls = core_mem_replace (betree_List_t t) self Betree_List_Nil in begin match ls with @@ -122,7 +122,7 @@ let betree_List_pop_front (t : Type0) (self : betree_List_t t) : result t = | Betree_List_Nil -> Fail Failure end -(** [betree_main::betree::List::{1}::pop_front]: backward function 0 *) +(** [betree_main::betree::{betree_main::betree::List<T>#1}::pop_front]: backward function 0 *) let betree_List_pop_front_back (t : Type0) (self : betree_List_t t) : result (betree_List_t t) = let ls = core_mem_replace (betree_List_t t) self Betree_List_Nil in @@ -131,26 +131,26 @@ let betree_List_pop_front_back | Betree_List_Nil -> Fail Failure end -(** [betree_main::betree::List::{1}::hd]: forward function *) +(** [betree_main::betree::{betree_main::betree::List<T>#1}::hd]: forward function *) let betree_List_hd (t : Type0) (self : betree_List_t t) : result t = begin match self with | Betree_List_Cons hd l -> Return hd | Betree_List_Nil -> Fail Failure end -(** [betree_main::betree::List::{2}::head_has_key]: forward function *) -let betree_List_head_has_key +(** [betree_main::betree::{betree_main::betree::List<(u64, T)>#2}::head_has_key]: forward function *) +let betree_ListTupleU64T_head_has_key (t : Type0) (self : betree_List_t (u64 & t)) (key : u64) : result bool = begin match self with | Betree_List_Cons hd l -> let (i, _) = hd in Return (i = key) | Betree_List_Nil -> Return false end -(** [betree_main::betree::List::{2}::partition_at_pivot]: forward function *) -let rec betree_List_partition_at_pivot +(** [betree_main::betree::{betree_main::betree::List<(u64, T)>#2}::partition_at_pivot]: forward function *) +let rec betree_ListTupleU64T_partition_at_pivot (t : Type0) (self : betree_List_t (u64 & t)) (pivot : u64) : Tot (result ((betree_List_t (u64 & t)) & (betree_List_t (u64 & t)))) - (decreases (betree_List_partition_at_pivot_decreases t self pivot)) + (decreases (betree_ListTupleU64T_partition_at_pivot_decreases t self pivot)) = begin match self with | Betree_List_Cons hd tl -> @@ -158,14 +158,14 @@ let rec betree_List_partition_at_pivot if i >= pivot then Return (Betree_List_Nil, Betree_List_Cons (i, x) tl) else - let* p = betree_List_partition_at_pivot t tl pivot in + let* p = betree_ListTupleU64T_partition_at_pivot t tl pivot in let (ls0, ls1) = p in let l = ls0 in Return (Betree_List_Cons (i, x) l, ls1) | Betree_List_Nil -> Return (Betree_List_Nil, Betree_List_Nil) end -(** [betree_main::betree::Leaf::{3}::split]: forward function *) +(** [betree_main::betree::{betree_main::betree::Leaf#3}::split]: forward function *) let betree_Leaf_split (self : betree_Leaf_t) (content : betree_List_t (u64 & u64)) (params : betree_Params_t) (node_id_cnt : betree_NodeIdCounter_t) @@ -185,7 +185,7 @@ let betree_Leaf_split let n0 = Betree_Node_Leaf { id = id1; size = params.split_size } in Return (st1, { id = self.id; pivot = pivot; left = n; right = n0 }) -(** [betree_main::betree::Leaf::{3}::split]: backward function 0 *) +(** [betree_main::betree::{betree_main::betree::Leaf#3}::split]: backward function 0 *) let betree_Leaf_split_back0 (self : betree_Leaf_t) (content : betree_List_t (u64 & u64)) (params : betree_Params_t) (node_id_cnt : betree_NodeIdCounter_t) @@ -202,7 +202,7 @@ let betree_Leaf_split_back0 let* _ = betree_store_leaf_node id1 content1 st1 in Return (st0, ()) -(** [betree_main::betree::Leaf::{3}::split]: backward function 1 *) +(** [betree_main::betree::{betree_main::betree::Leaf#3}::split]: backward function 1 *) let betree_Leaf_split_back1 (self : betree_Leaf_t) (content : betree_List_t (u64 & u64)) (params : betree_Params_t) (node_id_cnt : betree_NodeIdCounter_t) @@ -219,7 +219,7 @@ let betree_Leaf_split_back1 let* _ = betree_store_leaf_node id1 content1 st1 in Return (st0, ()) -(** [betree_main::betree::Leaf::{3}::split]: backward function 2 *) +(** [betree_main::betree::{betree_main::betree::Leaf#3}::split]: backward function 2 *) let betree_Leaf_split_back2 (self : betree_Leaf_t) (content : betree_List_t (u64 & u64)) (params : betree_Params_t) (node_id_cnt : betree_NodeIdCounter_t) @@ -237,7 +237,7 @@ let betree_Leaf_split_back2 let* node_id_cnt1 = betree_NodeIdCounter_fresh_id_back node_id_cnt0 in Return (st0, node_id_cnt1) -(** [betree_main::betree::Node::{5}::lookup_first_message_for_key]: forward function *) +(** [betree_main::betree::{betree_main::betree::Node#5}::lookup_first_message_for_key]: forward function *) let rec betree_Node_lookup_first_message_for_key (key : u64) (msgs : betree_List_t (u64 & betree_Message_t)) : Tot (result (betree_List_t (u64 & betree_Message_t))) @@ -252,7 +252,7 @@ let rec betree_Node_lookup_first_message_for_key | Betree_List_Nil -> Return Betree_List_Nil end -(** [betree_main::betree::Node::{5}::lookup_first_message_for_key]: backward function 0 *) +(** [betree_main::betree::{betree_main::betree::Node#5}::lookup_first_message_for_key]: backward function 0 *) let rec betree_Node_lookup_first_message_for_key_back (key : u64) (msgs : betree_List_t (u64 & betree_Message_t)) (ret : betree_List_t (u64 & betree_Message_t)) : @@ -271,14 +271,14 @@ let rec betree_Node_lookup_first_message_for_key_back | Betree_List_Nil -> Return ret end -(** [betree_main::betree::Node::{5}::apply_upserts]: forward function *) +(** [betree_main::betree::{betree_main::betree::Node#5}::apply_upserts]: forward function *) let rec betree_Node_apply_upserts (msgs : betree_List_t (u64 & betree_Message_t)) (prev : option u64) (key : u64) (st : state) : Tot (result (state & u64)) (decreases (betree_Node_apply_upserts_decreases msgs prev key st)) = - let* b = betree_List_head_has_key betree_Message_t msgs key in + let* b = betree_ListTupleU64T_head_has_key betree_Message_t msgs key in if b then let* msg = betree_List_pop_front (u64 & betree_Message_t) msgs in @@ -298,14 +298,14 @@ let rec betree_Node_apply_upserts Betree_Message_Insert v) in Return (st0, v) -(** [betree_main::betree::Node::{5}::apply_upserts]: backward function 0 *) +(** [betree_main::betree::{betree_main::betree::Node#5}::apply_upserts]: backward function 0 *) let rec betree_Node_apply_upserts_back (msgs : betree_List_t (u64 & betree_Message_t)) (prev : option u64) (key : u64) (st : state) (st0 : state) : Tot (result (state & (betree_List_t (u64 & betree_Message_t)))) (decreases (betree_Node_apply_upserts_decreases msgs prev key st)) = - let* b = betree_List_head_has_key betree_Message_t msgs key in + let* b = betree_ListTupleU64T_head_has_key betree_Message_t msgs key in if b then let* msg = betree_List_pop_front (u64 & betree_Message_t) msgs in @@ -325,7 +325,7 @@ let rec betree_Node_apply_upserts_back Betree_Message_Insert v) in Return (st0, msgs0) -(** [betree_main::betree::Node::{5}::lookup_in_bindings]: forward function *) +(** [betree_main::betree::{betree_main::betree::Node#5}::lookup_in_bindings]: forward function *) let rec betree_Node_lookup_in_bindings (key : u64) (bindings : betree_List_t (u64 & u64)) : Tot (result (option u64)) @@ -340,7 +340,7 @@ let rec betree_Node_lookup_in_bindings | Betree_List_Nil -> Return None end -(** [betree_main::betree::Internal::{4}::lookup_in_children]: forward function *) +(** [betree_main::betree::{betree_main::betree::Internal#4}::lookup_in_children]: forward function *) let rec betree_Internal_lookup_in_children (self : betree_Internal_t) (key : u64) (st : state) : Tot (result (state & (option u64))) @@ -350,7 +350,7 @@ let rec betree_Internal_lookup_in_children then betree_Node_lookup self.left key st else betree_Node_lookup self.right key st -(** [betree_main::betree::Internal::{4}::lookup_in_children]: backward function 0 *) +(** [betree_main::betree::{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)) @@ -364,7 +364,7 @@ and betree_Internal_lookup_in_children_back let* (st1, n) = betree_Node_lookup_back self.right key st st0 in Return (st1, { self with right = n }) -(** [betree_main::betree::Node::{5}::lookup]: forward function *) +(** [betree_main::betree::{betree_main::betree::Node#5}::lookup]: forward function *) and betree_Node_lookup (self : betree_Node_t) (key : u64) (st : state) : Tot (result (state & (option u64))) @@ -424,7 +424,7 @@ and betree_Node_lookup Return (st0, o) end -(** [betree_main::betree::Node::{5}::lookup]: backward function 0 *) +(** [betree_main::betree::{betree_main::betree::Node#5}::lookup]: backward function 0 *) and betree_Node_lookup_back (self : betree_Node_t) (key : u64) (st : state) (st0 : state) : Tot (result (state & betree_Node_t)) @@ -486,7 +486,7 @@ and betree_Node_lookup_back Return (st0, Betree_Node_Leaf node) end -(** [betree_main::betree::Node::{5}::filter_messages_for_key]: merged forward/backward function +(** [betree_main::betree::{betree_main::betree::Node#5}::filter_messages_for_key]: merged forward/backward function (there is a single backward function, and the forward function returns ()) *) let rec betree_Node_filter_messages_for_key (key : u64) (msgs : betree_List_t (u64 & betree_Message_t)) : @@ -506,7 +506,7 @@ let rec betree_Node_filter_messages_for_key | Betree_List_Nil -> Return Betree_List_Nil end -(** [betree_main::betree::Node::{5}::lookup_first_message_after_key]: forward function *) +(** [betree_main::betree::{betree_main::betree::Node#5}::lookup_first_message_after_key]: forward function *) let rec betree_Node_lookup_first_message_after_key (key : u64) (msgs : betree_List_t (u64 & betree_Message_t)) : Tot (result (betree_List_t (u64 & betree_Message_t))) @@ -521,7 +521,7 @@ let rec betree_Node_lookup_first_message_after_key | Betree_List_Nil -> Return Betree_List_Nil end -(** [betree_main::betree::Node::{5}::lookup_first_message_after_key]: backward function 0 *) +(** [betree_main::betree::{betree_main::betree::Node#5}::lookup_first_message_after_key]: backward function 0 *) let rec betree_Node_lookup_first_message_after_key_back (key : u64) (msgs : betree_List_t (u64 & betree_Message_t)) (ret : betree_List_t (u64 & betree_Message_t)) : @@ -540,7 +540,7 @@ let rec betree_Node_lookup_first_message_after_key_back | Betree_List_Nil -> Return ret end -(** [betree_main::betree::Node::{5}::apply_to_internal]: merged forward/backward function +(** [betree_main::betree::{betree_main::betree::Node#5}::apply_to_internal]: merged forward/backward function (there is a single backward function, and the forward function returns ()) *) let betree_Node_apply_to_internal (msgs : betree_List_t (u64 & betree_Message_t)) (key : u64) @@ -548,7 +548,7 @@ let betree_Node_apply_to_internal result (betree_List_t (u64 & betree_Message_t)) = let* msgs0 = betree_Node_lookup_first_message_for_key key msgs in - let* b = betree_List_head_has_key betree_Message_t msgs0 key in + let* b = betree_ListTupleU64T_head_has_key betree_Message_t msgs0 key in if b then begin match new_msg with @@ -599,7 +599,7 @@ let betree_Node_apply_to_internal betree_List_push_front (u64 & betree_Message_t) msgs0 (key, new_msg) in betree_Node_lookup_first_message_for_key_back key msgs msgs1 -(** [betree_main::betree::Node::{5}::apply_messages_to_internal]: merged forward/backward function +(** [betree_main::betree::{betree_main::betree::Node#5}::apply_messages_to_internal]: merged forward/backward function (there is a single backward function, and the forward function returns ()) *) let rec betree_Node_apply_messages_to_internal (msgs : betree_List_t (u64 & betree_Message_t)) @@ -615,7 +615,7 @@ let rec betree_Node_apply_messages_to_internal | Betree_List_Nil -> Return msgs end -(** [betree_main::betree::Node::{5}::lookup_mut_in_bindings]: forward function *) +(** [betree_main::betree::{betree_main::betree::Node#5}::lookup_mut_in_bindings]: forward function *) let rec betree_Node_lookup_mut_in_bindings (key : u64) (bindings : betree_List_t (u64 & u64)) : Tot (result (betree_List_t (u64 & u64))) @@ -630,7 +630,7 @@ let rec betree_Node_lookup_mut_in_bindings | Betree_List_Nil -> Return Betree_List_Nil end -(** [betree_main::betree::Node::{5}::lookup_mut_in_bindings]: backward function 0 *) +(** [betree_main::betree::{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)) : @@ -648,7 +648,7 @@ let rec betree_Node_lookup_mut_in_bindings_back | Betree_List_Nil -> Return ret end -(** [betree_main::betree::Node::{5}::apply_to_leaf]: merged forward/backward function +(** [betree_main::betree::{betree_main::betree::Node#5}::apply_to_leaf]: merged forward/backward function (there is a single backward function, and the forward function returns ()) *) let betree_Node_apply_to_leaf (bindings : betree_List_t (u64 & u64)) (key : u64) @@ -656,7 +656,7 @@ let betree_Node_apply_to_leaf result (betree_List_t (u64 & u64)) = let* bindings0 = betree_Node_lookup_mut_in_bindings key bindings in - let* b = betree_List_head_has_key u64 bindings0 key in + let* b = betree_ListTupleU64T_head_has_key u64 bindings0 key in if b then let* hd = betree_List_pop_front (u64 & u64) bindings0 in @@ -688,7 +688,7 @@ let betree_Node_apply_to_leaf betree_Node_lookup_mut_in_bindings_back key bindings bindings1 end -(** [betree_main::betree::Node::{5}::apply_messages_to_leaf]: merged forward/backward function +(** [betree_main::betree::{betree_main::betree::Node#5}::apply_messages_to_leaf]: merged forward/backward function (there is a single backward function, and the forward function returns ()) *) let rec betree_Node_apply_messages_to_leaf (bindings : betree_List_t (u64 & u64)) @@ -704,7 +704,7 @@ let rec betree_Node_apply_messages_to_leaf | Betree_List_Nil -> Return bindings end -(** [betree_main::betree::Internal::{4}::flush]: forward function *) +(** [betree_main::betree::{betree_main::betree::Internal#4}::flush]: forward function *) let rec betree_Internal_flush (self : betree_Internal_t) (params : betree_Params_t) (node_id_cnt : betree_NodeIdCounter_t) @@ -713,7 +713,8 @@ let rec betree_Internal_flush (decreases ( betree_Internal_flush_decreases self params node_id_cnt content st)) = - let* p = betree_List_partition_at_pivot betree_Message_t content self.pivot + let* p = + betree_ListTupleU64T_partition_at_pivot betree_Message_t content self.pivot in let (msgs_left, msgs_right) = p in let* len_left = betree_List_len (u64 & betree_Message_t) msgs_left in @@ -752,7 +753,7 @@ let rec betree_Internal_flush st st1 in Return (st2, msgs_left) -(** [betree_main::betree::Internal::{4}::flush]: backward function 0 *) +(** [betree_main::betree::{betree_main::betree::Internal#4}::flush]: backward function 0 *) and betree_Internal_flush_back'a (self : betree_Internal_t) (params : betree_Params_t) (node_id_cnt : betree_NodeIdCounter_t) @@ -762,7 +763,8 @@ and betree_Internal_flush_back'a (decreases ( betree_Internal_flush_decreases self params node_id_cnt content st)) = - let* p = betree_List_partition_at_pivot betree_Message_t content self.pivot + let* p = + betree_ListTupleU64T_partition_at_pivot betree_Message_t content self.pivot in let (msgs_left, msgs_right) = p in let* len_left = betree_List_len (u64 & betree_Message_t) msgs_left in @@ -801,7 +803,7 @@ and betree_Internal_flush_back'a st st2 in Return (st0, ({ self with right = n }, node_id_cnt0)) -(** [betree_main::betree::Internal::{4}::flush]: backward function 1 *) +(** [betree_main::betree::{betree_main::betree::Internal#4}::flush]: backward function 1 *) and betree_Internal_flush_back1 (self : betree_Internal_t) (params : betree_Params_t) (node_id_cnt : betree_NodeIdCounter_t) @@ -811,7 +813,8 @@ and betree_Internal_flush_back1 (decreases ( betree_Internal_flush_decreases self params node_id_cnt content st)) = - let* p = betree_List_partition_at_pivot betree_Message_t content self.pivot + let* p = + betree_ListTupleU64T_partition_at_pivot betree_Message_t content self.pivot in let (msgs_left, msgs_right) = p in let* len_left = betree_List_len (u64 & betree_Message_t) msgs_left in @@ -850,7 +853,7 @@ and betree_Internal_flush_back1 st st2 in Return (st0, ()) -(** [betree_main::betree::Node::{5}::apply_messages]: forward function *) +(** [betree_main::betree::{betree_main::betree::Node#5}::apply_messages]: forward function *) and betree_Node_apply_messages (self : betree_Node_t) (params : betree_Params_t) (node_id_cnt : betree_NodeIdCounter_t) @@ -891,7 +894,7 @@ and betree_Node_apply_messages Return (st1, ()) end -(** [betree_main::betree::Node::{5}::apply_messages]: backward function 0 *) +(** [betree_main::betree::{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_NodeIdCounter_t) @@ -937,7 +940,7 @@ and betree_Node_apply_messages_back'a Return (st0, (Betree_Node_Leaf { node with size = len }, node_id_cnt)) end -(** [betree_main::betree::Node::{5}::apply_messages]: backward function 1 *) +(** [betree_main::betree::{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_NodeIdCounter_t) @@ -979,7 +982,7 @@ and betree_Node_apply_messages_back1 let* _ = betree_store_leaf_node node.id content0 st1 in Return (st0, ()) end -(** [betree_main::betree::Node::{5}::apply]: forward function *) +(** [betree_main::betree::{betree_main::betree::Node#5}::apply]: forward function *) let betree_Node_apply (self : betree_Node_t) (params : betree_Params_t) (node_id_cnt : betree_NodeIdCounter_t) (key : u64) @@ -996,7 +999,7 @@ let betree_Node_apply betree_Node_apply_messages_back1 self params node_id_cnt (Betree_List_Cons (key, new_msg) l) st st1 -(** [betree_main::betree::Node::{5}::apply]: backward function 0 *) +(** [betree_main::betree::{betree_main::betree::Node#5}::apply]: backward function 0 *) let betree_Node_apply_back'a (self : betree_Node_t) (params : betree_Params_t) (node_id_cnt : betree_NodeIdCounter_t) (key : u64) @@ -1015,7 +1018,7 @@ let betree_Node_apply_back'a (key, new_msg) l) st st2 in Return (st0, (self0, node_id_cnt0)) -(** [betree_main::betree::Node::{5}::apply]: backward function 1 *) +(** [betree_main::betree::{betree_main::betree::Node#5}::apply]: backward function 1 *) let betree_Node_apply_back1 (self : betree_Node_t) (params : betree_Params_t) (node_id_cnt : betree_NodeIdCounter_t) (key : u64) @@ -1034,7 +1037,7 @@ let betree_Node_apply_back1 (key, new_msg) l) st st2 in Return (st0, ()) -(** [betree_main::betree::BeTree::{6}::new]: forward function *) +(** [betree_main::betree::{betree_main::betree::BeTree#6}::new]: forward function *) let betree_BeTree_new (min_flush_size : u64) (split_size : u64) (st : state) : result (state & betree_BeTree_t) @@ -1050,7 +1053,7 @@ let betree_BeTree_new root = (Betree_Node_Leaf { id = id; size = 0 }) }) -(** [betree_main::betree::BeTree::{6}::apply]: forward function *) +(** [betree_main::betree::{betree_main::betree::BeTree#6}::apply]: forward function *) let betree_BeTree_apply (self : betree_BeTree_t) (key : u64) (msg : betree_Message_t) (st : state) : result (state & unit) @@ -1062,7 +1065,7 @@ let betree_BeTree_apply st0 in betree_Node_apply_back1 self.root self.params self.node_id_cnt key msg st st1 -(** [betree_main::betree::BeTree::{6}::apply]: backward function 0 *) +(** [betree_main::betree::{betree_main::betree::BeTree#6}::apply]: backward function 0 *) let betree_BeTree_apply_back (self : betree_BeTree_t) (key : u64) (msg : betree_Message_t) (st : state) (st0 : state) : @@ -1078,7 +1081,7 @@ let betree_BeTree_apply_back st2 in Return (st0, { self with node_id_cnt = nic; root = n }) -(** [betree_main::betree::BeTree::{6}::insert]: forward function *) +(** [betree_main::betree::{betree_main::betree::BeTree#6}::insert]: forward function *) let betree_BeTree_insert (self : betree_BeTree_t) (key : u64) (value : u64) (st : state) : result (state & unit) @@ -1089,7 +1092,7 @@ let betree_BeTree_insert betree_BeTree_apply_back self key (Betree_Message_Insert value) st st0 in Return (st1, ()) -(** [betree_main::betree::BeTree::{6}::insert]: backward function 0 *) +(** [betree_main::betree::{betree_main::betree::BeTree#6}::insert]: backward function 0 *) let betree_BeTree_insert_back (self : betree_BeTree_t) (key : u64) (value : u64) (st : state) (st0 : state) : @@ -1101,7 +1104,7 @@ let betree_BeTree_insert_back betree_BeTree_apply_back self key (Betree_Message_Insert value) st st1 in Return (st0, self0) -(** [betree_main::betree::BeTree::{6}::delete]: forward function *) +(** [betree_main::betree::{betree_main::betree::BeTree#6}::delete]: forward function *) let betree_BeTree_delete (self : betree_BeTree_t) (key : u64) (st : state) : result (state & unit) = let* (st0, _) = betree_BeTree_apply self key Betree_Message_Delete st in @@ -1109,7 +1112,7 @@ let betree_BeTree_delete betree_BeTree_apply_back self key Betree_Message_Delete st st0 in Return (st1, ()) -(** [betree_main::betree::BeTree::{6}::delete]: backward function 0 *) +(** [betree_main::betree::{betree_main::betree::BeTree#6}::delete]: backward function 0 *) let betree_BeTree_delete_back (self : betree_BeTree_t) (key : u64) (st : state) (st0 : state) : result (state & betree_BeTree_t) @@ -1119,7 +1122,7 @@ let betree_BeTree_delete_back betree_BeTree_apply_back self key Betree_Message_Delete st st1 in Return (st0, self0) -(** [betree_main::betree::BeTree::{6}::upsert]: forward function *) +(** [betree_main::betree::{betree_main::betree::BeTree#6}::upsert]: forward function *) let betree_BeTree_upsert (self : betree_BeTree_t) (key : u64) (upd : betree_UpsertFunState_t) (st : state) : @@ -1131,7 +1134,7 @@ let betree_BeTree_upsert betree_BeTree_apply_back self key (Betree_Message_Upsert upd) st st0 in Return (st1, ()) -(** [betree_main::betree::BeTree::{6}::upsert]: backward function 0 *) +(** [betree_main::betree::{betree_main::betree::BeTree#6}::upsert]: backward function 0 *) let betree_BeTree_upsert_back (self : betree_BeTree_t) (key : u64) (upd : betree_UpsertFunState_t) (st : state) (st0 : state) : @@ -1143,14 +1146,14 @@ let betree_BeTree_upsert_back betree_BeTree_apply_back self key (Betree_Message_Upsert upd) st st1 in Return (st0, self0) -(** [betree_main::betree::BeTree::{6}::lookup]: forward function *) +(** [betree_main::betree::{betree_main::betree::BeTree#6}::lookup]: forward function *) let betree_BeTree_lookup (self : betree_BeTree_t) (key : u64) (st : state) : result (state & (option u64)) = betree_Node_lookup self.root key st -(** [betree_main::betree::BeTree::{6}::lookup]: backward function 0 *) +(** [betree_main::betree::{betree_main::betree::BeTree#6}::lookup]: backward function 0 *) let betree_BeTree_lookup_back (self : betree_BeTree_t) (key : u64) (st : state) (st0 : state) : result (state & betree_BeTree_t) diff --git a/tests/fstar/betree_back_stateful/BetreeMain.Opaque.fsti b/tests/fstar/betree_back_stateful/BetreeMain.Opaque.fsti index c5d0a814..23d2e60e 100644 --- a/tests/fstar/betree_back_stateful/BetreeMain.Opaque.fsti +++ b/tests/fstar/betree_back_stateful/BetreeMain.Opaque.fsti @@ -24,7 +24,7 @@ val betree_utils_load_leaf_node val betree_utils_store_leaf_node : u64 -> betree_List_t (u64 & u64) -> state -> result (state & unit) -(** [core::option::Option::{0}::unwrap]: forward function *) +(** [core::option::{core::option::Option<T>}::unwrap]: forward function *) val core_option_Option_unwrap (t : Type0) : option t -> state -> result (state & t) |