diff options
author | Son HO | 2023-11-22 15:06:43 +0100 |
---|---|---|
committer | GitHub | 2023-11-22 15:06:43 +0100 |
commit | bacf3f5f6f5f6a9aa650d5ae8d12a132fd747039 (patch) | |
tree | 9953d7af1fe406cdc750030a43a5e4d6245cd763 /tests/fstar/betree | |
parent | 587f1ebc0178acb19029d3fc9a729c197082aba7 (diff) | |
parent | 01cfd899119174ef7c5941c99dd251711f4ee701 (diff) |
Merge pull request #45 from AeneasVerif/son_merge_types
Big cleanup
Diffstat (limited to '')
-rw-r--r-- | tests/fstar/betree/BetreeMain.Clauses.Template.fst | 47 | ||||
-rw-r--r-- | tests/fstar/betree/BetreeMain.Clauses.fst | 2 | ||||
-rw-r--r-- | tests/fstar/betree/BetreeMain.Funs.fst | 202 | ||||
-rw-r--r-- | tests/fstar/betree/BetreeMain.Opaque.fsti | 15 | ||||
-rw-r--r-- | tests/fstar/betree/BetreeMain.Types.fsti | 27 | ||||
-rw-r--r-- | tests/fstar/betree/Primitives.fst | 88 | ||||
-rw-r--r-- | tests/fstar/betree_back_stateful/BetreeMain.Clauses.Template.fst | 47 | ||||
-rw-r--r-- | tests/fstar/betree_back_stateful/BetreeMain.Clauses.fst | 2 | ||||
-rw-r--r-- | tests/fstar/betree_back_stateful/BetreeMain.Funs.fst | 220 | ||||
-rw-r--r-- | tests/fstar/betree_back_stateful/BetreeMain.Opaque.fsti | 15 | ||||
-rw-r--r-- | tests/fstar/betree_back_stateful/BetreeMain.Types.fsti | 27 | ||||
-rw-r--r-- | tests/fstar/betree_back_stateful/Primitives.fst | 88 |
12 files changed, 480 insertions, 300 deletions
diff --git a/tests/fstar/betree/BetreeMain.Clauses.Template.fst b/tests/fstar/betree/BetreeMain.Clauses.Template.fst index 8722f0bf..4ae29302 100644 --- a/tests/fstar/betree/BetreeMain.Clauses.Template.fst +++ b/tests/fstar/betree/BetreeMain.Clauses.Template.fst @@ -6,94 +6,109 @@ 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 + Source: 'src/betree.rs', lines 276:4-276:24 *) 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 + Source: 'src/betree.rs', lines 284:4-284:51 *) 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 + Source: 'src/betree.rs', lines 339:4-339:73 *) 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 + Source: 'src/betree.rs', lines 789:4-792:34 *) 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 + Source: 'src/betree.rs', lines 819:4-819:90 *) 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 + Source: 'src/betree.rs', lines 636:4-636:80 *) 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 + Source: 'src/betree.rs', lines 395:4-395:63 *) 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 + Source: 'src/betree.rs', lines 709:4-709:58 *) 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 + Source: 'src/betree.rs', lines 674:4-674:77 *) 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 + Source: 'src/betree.rs', lines 689:4-692:34 *) 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 + Source: 'src/betree.rs', lines 502:4-505:5 *) 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 + Source: 'src/betree.rs', lines 653:4-656:32 *) 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 + Source: 'src/betree.rs', lines 444:4-447:5 *) 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 + Source: 'src/betree.rs', lines 410:4-415:26 *) 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 + Source: 'src/betree.rs', lines 588:4-593:5 *) 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..537ec32e 100644 --- a/tests/fstar/betree/BetreeMain.Funs.fst +++ b/tests/fstar/betree/BetreeMain.Funs.fst @@ -8,14 +8,16 @@ include BetreeMain.Clauses #set-options "--z3rlimit 50 --fuel 1 --ifuel 1" -(** [betree_main::betree::load_internal_node]: forward function *) +(** [betree_main::betree::load_internal_node]: forward function + Source: 'src/betree.rs', lines 36:0-36:52 *) let betree_load_internal_node (id : u64) (st : state) : result (state & (betree_List_t (u64 & betree_Message_t))) = betree_utils_load_internal_node id st -(** [betree_main::betree::store_internal_node]: forward function *) +(** [betree_main::betree::store_internal_node]: forward function + Source: 'src/betree.rs', lines 41:0-41:60 *) let betree_store_internal_node (id : u64) (content : betree_List_t (u64 & betree_Message_t)) (st : state) : result (state & unit) @@ -23,12 +25,14 @@ let betree_store_internal_node let* (st0, _) = betree_utils_store_internal_node id content st in Return (st0, ()) -(** [betree_main::betree::load_leaf_node]: forward function *) +(** [betree_main::betree::load_leaf_node]: forward function + Source: 'src/betree.rs', lines 46:0-46:44 *) let betree_load_leaf_node (id : u64) (st : state) : result (state & (betree_List_t (u64 & u64))) = betree_utils_load_leaf_node id st -(** [betree_main::betree::store_leaf_node]: forward function *) +(** [betree_main::betree::store_leaf_node]: forward function + Source: 'src/betree.rs', lines 51:0-51:52 *) let betree_store_leaf_node (id : u64) (content : betree_List_t (u64 & u64)) (st : state) : result (state & unit) @@ -36,29 +40,35 @@ let betree_store_leaf_node let* (st0, _) = betree_utils_store_leaf_node id content st in Return (st0, ()) -(** [betree_main::betree::fresh_node_id]: forward function *) +(** [betree_main::betree::fresh_node_id]: forward function + Source: 'src/betree.rs', lines 55:0-55:48 *) let betree_fresh_node_id (counter : u64) : result u64 = let* _ = u64_add counter 1 in Return counter -(** [betree_main::betree::fresh_node_id]: backward function 0 *) +(** [betree_main::betree::fresh_node_id]: backward function 0 + Source: 'src/betree.rs', lines 55:0-55:48 *) 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 + Source: 'src/betree.rs', lines 206:4-206:20 *) 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 + Source: 'src/betree.rs', lines 210:4-210:36 *) 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 + Source: 'src/betree.rs', lines 210:4-210:36 *) 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 } -(** [betree_main::betree::upsert_update]: forward function *) +(** [betree_main::betree::upsert_update]: forward function + Source: 'src/betree.rs', lines 234:0-234:70 *) let betree_upsert_update (prev : option u64) (st : betree_UpsertFunState_t) : result u64 = begin match prev with @@ -77,7 +87,8 @@ 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 + Source: 'src/betree.rs', lines 276:4-276:24 *) let rec betree_List_len (t : Type0) (self : betree_List_t t) : Tot (result u64) (decreases (betree_List_len_decreases t self)) @@ -87,7 +98,8 @@ 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 + Source: 'src/betree.rs', lines 284:4-284:51 *) let rec betree_List_split_at (t : Type0) (self : betree_List_t t) (n : u64) : Tot (result ((betree_List_t t) & (betree_List_t t))) @@ -106,15 +118,17 @@ let rec betree_List_split_at | Betree_List_Nil -> Fail Failure end -(** [betree_main::betree::List::{1}::push_front]: merged forward/backward function - (there is a single backward function, and the forward function returns ()) *) +(** [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 ()) + Source: 'src/betree.rs', lines 299:4-299:34 *) let betree_List_push_front (t : Type0) (self : betree_List_t t) (x : t) : result (betree_List_t t) = let tl = core_mem_replace (betree_List_t t) self Betree_List_Nil in 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 + Source: 'src/betree.rs', lines 306:4-306:32 *) 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 +136,8 @@ 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 + Source: 'src/betree.rs', lines 306:4-306:32 *) 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 +146,29 @@ 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 + Source: 'src/betree.rs', lines 318:4-318:22 *) let betree_List_hd (t : Type0) (self : betree_List_t t) : result t = begin match self with | Betree_List_Cons hd 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 + Source: 'src/betree.rs', lines 327:4-327:44 *) +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 + Source: 'src/betree.rs', lines 339:4-339:73 *) +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 +176,15 @@ 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 + Source: 'src/betree.rs', lines 359:4-364:17 *) let betree_Leaf_split (self : betree_Leaf_t) (content : betree_List_t (u64 & u64)) (params : betree_Params_t) (node_id_cnt : betree_NodeIdCounter_t) @@ -185,7 +204,8 @@ 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 + Source: 'src/betree.rs', lines 359:4-364:17 *) 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 +222,8 @@ 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 + Source: 'src/betree.rs', lines 789:4-792:34 *) let rec betree_Node_lookup_first_message_for_key (key : u64) (msgs : betree_List_t (u64 & betree_Message_t)) : Tot (result (betree_List_t (u64 & betree_Message_t))) @@ -217,7 +238,8 @@ 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 + Source: 'src/betree.rs', lines 789:4-792:34 *) 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 +258,15 @@ 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 + Source: 'src/betree.rs', lines 819:4-819:90 *) let rec betree_Node_apply_upserts (msgs : betree_List_t (u64 & betree_Message_t)) (prev : option u64) (key : u64) (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 +286,15 @@ 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 + Source: 'src/betree.rs', lines 819:4-819:90 *) 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 +312,8 @@ 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 + Source: 'src/betree.rs', lines 636:4-636:80 *) let rec betree_Node_lookup_in_bindings (key : u64) (bindings : betree_List_t (u64 & u64)) : Tot (result (option u64)) @@ -303,7 +328,8 @@ 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 + Source: 'src/betree.rs', lines 395:4-395:63 *) let rec betree_Internal_lookup_in_children (self : betree_Internal_t) (key : u64) (st : state) : Tot (result (state & (option u64))) @@ -313,7 +339,8 @@ 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 + Source: 'src/betree.rs', lines 395:4-395:63 *) and betree_Internal_lookup_in_children_back (self : betree_Internal_t) (key : u64) (st : state) : Tot (result betree_Internal_t) @@ -327,7 +354,8 @@ 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 + Source: 'src/betree.rs', lines 709:4-709:58 *) and betree_Node_lookup (self : betree_Node_t) (key : u64) (st : state) : Tot (result (state & (option u64))) @@ -386,7 +414,8 @@ 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 + Source: 'src/betree.rs', lines 709:4-709:58 *) and betree_Node_lookup_back (self : betree_Node_t) (key : u64) (st : state) : Tot (result betree_Node_t) @@ -445,8 +474,9 @@ and betree_Node_lookup_back Return (Betree_Node_Leaf node) 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 ()) *) +(** [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 ()) + Source: 'src/betree.rs', lines 674:4-674:77 *) let rec betree_Node_filter_messages_for_key (key : u64) (msgs : betree_List_t (u64 & betree_Message_t)) : Tot (result (betree_List_t (u64 & betree_Message_t))) @@ -465,7 +495,8 @@ 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 + Source: 'src/betree.rs', lines 689:4-692:34 *) let rec betree_Node_lookup_first_message_after_key (key : u64) (msgs : betree_List_t (u64 & betree_Message_t)) : Tot (result (betree_List_t (u64 & betree_Message_t))) @@ -480,7 +511,8 @@ 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 + Source: 'src/betree.rs', lines 689:4-692:34 *) 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,15 +531,16 @@ 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 - (there is a single backward function, and the forward function returns ()) *) +(** [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 ()) + Source: 'src/betree.rs', lines 521:4-521:89 *) let betree_Node_apply_to_internal (msgs : betree_List_t (u64 & betree_Message_t)) (key : u64) (new_msg : betree_Message_t) : result (betree_List_t (u64 & betree_Message_t)) = let* 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,8 +591,9 @@ 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 - (there is a single backward function, and the forward function returns ()) *) +(** [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 ()) + Source: 'src/betree.rs', lines 502:4-505:5 *) let rec betree_Node_apply_messages_to_internal (msgs : betree_List_t (u64 & betree_Message_t)) (new_msgs : betree_List_t (u64 & betree_Message_t)) : @@ -574,7 +608,8 @@ 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 + Source: 'src/betree.rs', lines 653:4-656:32 *) let rec betree_Node_lookup_mut_in_bindings (key : u64) (bindings : betree_List_t (u64 & u64)) : Tot (result (betree_List_t (u64 & u64))) @@ -589,7 +624,8 @@ 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 + Source: 'src/betree.rs', lines 653:4-656:32 *) let rec betree_Node_lookup_mut_in_bindings_back (key : u64) (bindings : betree_List_t (u64 & u64)) (ret : betree_List_t (u64 & u64)) : @@ -607,15 +643,16 @@ 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 - (there is a single backward function, and the forward function returns ()) *) +(** [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 ()) + Source: 'src/betree.rs', lines 460:4-460:87 *) let betree_Node_apply_to_leaf (bindings : betree_List_t (u64 & u64)) (key : u64) (new_msg : betree_Message_t) : result (betree_List_t (u64 & u64)) = let* 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,8 +684,9 @@ 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 - (there is a single backward function, and the forward function returns ()) *) +(** [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 ()) + Source: 'src/betree.rs', lines 444:4-447:5 *) let rec betree_Node_apply_messages_to_leaf (bindings : betree_List_t (u64 & u64)) (new_msgs : betree_List_t (u64 & betree_Message_t)) : @@ -663,7 +701,8 @@ 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 + Source: 'src/betree.rs', lines 410:4-415:26 *) let rec betree_Internal_flush (self : betree_Internal_t) (params : betree_Params_t) (node_id_cnt : betree_NodeIdCounter_t) @@ -672,7 +711,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 +742,8 @@ 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 + Source: 'src/betree.rs', lines 410:4-415:26 *) and betree_Internal_flush_back (self : betree_Internal_t) (params : betree_Params_t) (node_id_cnt : betree_NodeIdCounter_t) @@ -711,7 +752,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 +778,8 @@ 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 + Source: 'src/betree.rs', lines 588:4-593:5 *) and betree_Node_apply_messages (self : betree_Node_t) (params : betree_Params_t) (node_id_cnt : betree_NodeIdCounter_t) @@ -776,7 +819,8 @@ 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 + Source: 'src/betree.rs', lines 588:4-593:5 *) and betree_Node_apply_messages_back (self : betree_Node_t) (params : betree_Params_t) (node_id_cnt : betree_NodeIdCounter_t) @@ -819,7 +863,8 @@ 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 + Source: 'src/betree.rs', lines 576:4-582:5 *) let betree_Node_apply (self : betree_Node_t) (params : betree_Params_t) (node_id_cnt : betree_NodeIdCounter_t) (key : u64) @@ -835,7 +880,8 @@ 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 + Source: 'src/betree.rs', lines 576:4-582:5 *) let betree_Node_apply_back (self : betree_Node_t) (params : betree_Params_t) (node_id_cnt : betree_NodeIdCounter_t) (key : u64) @@ -846,7 +892,8 @@ 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 + Source: 'src/betree.rs', lines 849:4-849:60 *) let betree_BeTree_new (min_flush_size : u64) (split_size : u64) (st : state) : result (state & betree_BeTree_t) @@ -862,7 +909,8 @@ 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 + Source: 'src/betree.rs', lines 868:4-868:47 *) let betree_BeTree_apply (self : betree_BeTree_t) (key : u64) (msg : betree_Message_t) (st : state) : result (state & unit) @@ -873,7 +921,8 @@ 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 + Source: 'src/betree.rs', lines 868:4-868:47 *) let betree_BeTree_apply_back (self : betree_BeTree_t) (key : u64) (msg : betree_Message_t) (st : state) : result betree_BeTree_t @@ -882,7 +931,8 @@ 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 + Source: 'src/betree.rs', lines 874:4-874:52 *) let betree_BeTree_insert (self : betree_BeTree_t) (key : u64) (value : u64) (st : state) : result (state & unit) @@ -893,26 +943,30 @@ 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 + Source: 'src/betree.rs', lines 874:4-874:52 *) 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 + Source: 'src/betree.rs', lines 880:4-880:38 *) 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 + Source: 'src/betree.rs', lines 880:4-880:38 *) 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 + Source: 'src/betree.rs', lines 886:4-886:59 *) let betree_BeTree_upsert (self : betree_BeTree_t) (key : u64) (upd : betree_UpsertFunState_t) (st : state) : @@ -923,7 +977,8 @@ 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 + Source: 'src/betree.rs', lines 886:4-886:59 *) let betree_BeTree_upsert_back (self : betree_BeTree_t) (key : u64) (upd : betree_UpsertFunState_t) (st : state) : @@ -931,20 +986,23 @@ 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 + Source: 'src/betree.rs', lines 895:4-895:62 *) let betree_BeTree_lookup (self : betree_BeTree_t) (key : u64) (st : state) : result (state & (option u64)) = betree_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 + Source: 'src/betree.rs', lines 895:4-895:62 *) 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 Return { self with root = n } -(** [betree_main::main]: forward function *) +(** [betree_main::main]: forward function + Source: 'src/betree_main.rs', lines 5:0-5:9 *) let main : result unit = Return () diff --git a/tests/fstar/betree/BetreeMain.Opaque.fsti b/tests/fstar/betree/BetreeMain.Opaque.fsti index c5d0a814..b89c8718 100644 --- a/tests/fstar/betree/BetreeMain.Opaque.fsti +++ b/tests/fstar/betree/BetreeMain.Opaque.fsti @@ -6,25 +6,30 @@ include BetreeMain.Types #set-options "--z3rlimit 50 --fuel 1 --ifuel 1" -(** [betree_main::betree_utils::load_internal_node]: forward function *) +(** [betree_main::betree_utils::load_internal_node]: forward function + Source: 'src/betree_utils.rs', lines 98:0-98:63 *) val betree_utils_load_internal_node : u64 -> state -> result (state & (betree_List_t (u64 & betree_Message_t))) -(** [betree_main::betree_utils::store_internal_node]: forward function *) +(** [betree_main::betree_utils::store_internal_node]: forward function + Source: 'src/betree_utils.rs', lines 115:0-115:71 *) val betree_utils_store_internal_node : u64 -> betree_List_t (u64 & betree_Message_t) -> state -> result (state & unit) -(** [betree_main::betree_utils::load_leaf_node]: forward function *) +(** [betree_main::betree_utils::load_leaf_node]: forward function + Source: 'src/betree_utils.rs', lines 132:0-132:55 *) val betree_utils_load_leaf_node : u64 -> state -> result (state & (betree_List_t (u64 & u64))) -(** [betree_main::betree_utils::store_leaf_node]: forward function *) +(** [betree_main::betree_utils::store_leaf_node]: forward function + Source: 'src/betree_utils.rs', lines 145:0-145:63 *) 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 + Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/option.rs', lines 932:4-932:34 *) val core_option_Option_unwrap (t : Type0) : option t -> state -> result (state & t) diff --git a/tests/fstar/betree/BetreeMain.Types.fsti b/tests/fstar/betree/BetreeMain.Types.fsti index 9320f6b7..a098ec19 100644 --- a/tests/fstar/betree/BetreeMain.Types.fsti +++ b/tests/fstar/betree/BetreeMain.Types.fsti @@ -5,43 +5,52 @@ open Primitives #set-options "--z3rlimit 50 --fuel 1 --ifuel 1" -(** [betree_main::betree::List] *) +(** [betree_main::betree::List] + Source: 'src/betree.rs', lines 17:0-17:23 *) type betree_List_t (t : Type0) = | Betree_List_Cons : t -> betree_List_t t -> betree_List_t t | Betree_List_Nil : betree_List_t t -(** [betree_main::betree::UpsertFunState] *) +(** [betree_main::betree::UpsertFunState] + Source: 'src/betree.rs', lines 63:0-63:23 *) type betree_UpsertFunState_t = | Betree_UpsertFunState_Add : u64 -> betree_UpsertFunState_t | Betree_UpsertFunState_Sub : u64 -> betree_UpsertFunState_t -(** [betree_main::betree::Message] *) +(** [betree_main::betree::Message] + Source: 'src/betree.rs', lines 69:0-69:23 *) type betree_Message_t = | Betree_Message_Insert : u64 -> betree_Message_t | Betree_Message_Delete : betree_Message_t | Betree_Message_Upsert : betree_UpsertFunState_t -> betree_Message_t -(** [betree_main::betree::Leaf] *) +(** [betree_main::betree::Leaf] + Source: 'src/betree.rs', lines 167:0-167:11 *) type betree_Leaf_t = { id : u64; size : u64; } -(** [betree_main::betree::Internal] *) +(** [betree_main::betree::Internal] + Source: 'src/betree.rs', lines 156:0-156:15 *) type betree_Internal_t = { id : u64; pivot : u64; left : betree_Node_t; right : betree_Node_t; } -(** [betree_main::betree::Node] *) +(** [betree_main::betree::Node] + Source: 'src/betree.rs', lines 179:0-179:9 *) and betree_Node_t = | Betree_Node_Internal : betree_Internal_t -> betree_Node_t | Betree_Node_Leaf : betree_Leaf_t -> betree_Node_t -(** [betree_main::betree::Params] *) +(** [betree_main::betree::Params] + Source: 'src/betree.rs', lines 187:0-187:13 *) type betree_Params_t = { min_flush_size : u64; split_size : u64; } -(** [betree_main::betree::NodeIdCounter] *) +(** [betree_main::betree::NodeIdCounter] + Source: 'src/betree.rs', lines 201:0-201:20 *) type betree_NodeIdCounter_t = { next_node_id : u64; } -(** [betree_main::betree::BeTree] *) +(** [betree_main::betree::BeTree] + Source: 'src/betree.rs', lines 218:0-218:17 *) type betree_BeTree_t = { params : betree_Params_t; diff --git a/tests/fstar/betree/Primitives.fst b/tests/fstar/betree/Primitives.fst index 3297803c..94322ead 100644 --- a/tests/fstar/betree/Primitives.fst +++ b/tests/fstar/betree/Primitives.fst @@ -351,14 +351,14 @@ let alloc_boxed_Box_deref_mut (t : Type0) (x : t) : result t = Return x let alloc_boxed_Box_deref_mut_back (t : Type) (_ : t) (x : t) : result t = Return x // Trait instance -let alloc_boxed_Box_coreOpsDerefInst (self : Type0) : core_ops_deref_Deref self = { +let alloc_boxed_Box_coreopsDerefInst (self : Type0) : core_ops_deref_Deref self = { target = self; deref = alloc_boxed_Box_deref self; } // Trait instance -let alloc_boxed_Box_coreOpsDerefMutInst (self : Type0) : core_ops_deref_DerefMut self = { - derefInst = alloc_boxed_Box_coreOpsDerefInst self; +let alloc_boxed_Box_coreopsDerefMutInst (self : Type0) : core_ops_deref_DerefMut self = { + derefInst = alloc_boxed_Box_coreopsDerefInst self; deref_mut = alloc_boxed_Box_deref_mut self; deref_mut_back = alloc_boxed_Box_deref_mut_back self; } @@ -483,23 +483,23 @@ let core_slice_index_Slice_index | Some x -> Return x // [core::slice::index::Range:::get]: forward function -let core_slice_index_Range_get (t : Type0) (i : core_ops_range_Range usize) (s : slice t) : +let core_slice_index_RangeUsize_get (t : Type0) (i : core_ops_range_Range usize) (s : slice t) : result (option (slice t)) = admit () // TODO // [core::slice::index::Range::get_mut]: forward function -let core_slice_index_Range_get_mut +let core_slice_index_RangeUsize_get_mut (t : Type0) : core_ops_range_Range usize → slice t → result (option (slice t)) = admit () // TODO // [core::slice::index::Range::get_mut]: backward function 0 -let core_slice_index_Range_get_mut_back +let core_slice_index_RangeUsize_get_mut_back (t : Type0) : core_ops_range_Range usize → slice t → option (slice t) → result (slice t) = admit () // TODO // [core::slice::index::Range::get_unchecked]: forward function -let core_slice_index_Range_get_unchecked +let core_slice_index_RangeUsize_get_unchecked (t : Type0) : core_ops_range_Range usize → const_raw_ptr (slice t) → result (const_raw_ptr (slice t)) = // Don't know what the model should be - for now we always fail to make @@ -507,7 +507,7 @@ let core_slice_index_Range_get_unchecked fun _ _ -> Fail Failure // [core::slice::index::Range::get_unchecked_mut]: forward function -let core_slice_index_Range_get_unchecked_mut +let core_slice_index_RangeUsize_get_unchecked_mut (t : Type0) : core_ops_range_Range usize → mut_raw_ptr (slice t) → result (mut_raw_ptr (slice t)) = // Don't know what the model should be - for now we always fail to make @@ -515,17 +515,17 @@ let core_slice_index_Range_get_unchecked_mut fun _ _ -> Fail Failure // [core::slice::index::Range::index]: forward function -let core_slice_index_Range_index +let core_slice_index_RangeUsize_index (t : Type0) : core_ops_range_Range usize → slice t → result (slice t) = admit () // TODO // [core::slice::index::Range::index_mut]: forward function -let core_slice_index_Range_index_mut +let core_slice_index_RangeUsize_index_mut (t : Type0) : core_ops_range_Range usize → slice t → result (slice t) = admit () // TODO // [core::slice::index::Range::index_mut]: backward function 0 -let core_slice_index_Range_index_mut_back +let core_slice_index_RangeUsize_index_mut_back (t : Type0) : core_ops_range_Range usize → slice t → slice t → result (slice t) = admit () // TODO @@ -559,44 +559,44 @@ let core_array_Array_index_mut_back (a : array t n) (i : idx) (x : inst.indexInst.output) : result (array t n) = admit () // TODO -// Trait implementation: [core::slice::index::[T]] -let core_slice_index_Slice_coreopsindexIndexInst (t idx : Type0) - (inst : core_slice_index_SliceIndex idx (slice t)) : - core_ops_index_Index (slice t) idx = { - output = inst.output; - index = core_slice_index_Slice_index t idx inst; -} - // Trait implementation: [core::slice::index::private_slice_index::Range] -let core_slice_index_private_slice_index_Range_coresliceindexprivate_slice_indexSealedInst +let core_slice_index_private_slice_index_SealedRangeUsizeInst : core_slice_index_private_slice_index_Sealed (core_ops_range_Range usize) = () // Trait implementation: [core::slice::index::Range] -let core_slice_index_Range_coresliceindexSliceIndexInst (t : Type0) : +let core_slice_index_SliceIndexRangeUsizeSliceTInst (t : Type0) : core_slice_index_SliceIndex (core_ops_range_Range usize) (slice t) = { - sealedInst = core_slice_index_private_slice_index_Range_coresliceindexprivate_slice_indexSealedInst; + sealedInst = core_slice_index_private_slice_index_SealedRangeUsizeInst; output = slice t; - get = core_slice_index_Range_get t; - get_mut = core_slice_index_Range_get_mut t; - get_mut_back = core_slice_index_Range_get_mut_back t; - get_unchecked = core_slice_index_Range_get_unchecked t; - get_unchecked_mut = core_slice_index_Range_get_unchecked_mut t; - index = core_slice_index_Range_index t; - index_mut = core_slice_index_Range_index_mut t; - index_mut_back = core_slice_index_Range_index_mut_back t; + get = core_slice_index_RangeUsize_get t; + get_mut = core_slice_index_RangeUsize_get_mut t; + get_mut_back = core_slice_index_RangeUsize_get_mut_back t; + get_unchecked = core_slice_index_RangeUsize_get_unchecked t; + get_unchecked_mut = core_slice_index_RangeUsize_get_unchecked_mut t; + index = core_slice_index_RangeUsize_index t; + index_mut = core_slice_index_RangeUsize_index_mut t; + index_mut_back = core_slice_index_RangeUsize_index_mut_back t; +} + +// Trait implementation: [core::slice::index::[T]] +let core_ops_index_IndexSliceTIInst (t idx : Type0) + (inst : core_slice_index_SliceIndex idx (slice t)) : + core_ops_index_Index (slice t) idx = { + output = inst.output; + index = core_slice_index_Slice_index t idx inst; } // Trait implementation: [core::slice::index::[T]] -let core_slice_index_Slice_coreopsindexIndexMutInst (t idx : Type0) +let core_ops_index_IndexMutSliceTIInst (t idx : Type0) (inst : core_slice_index_SliceIndex idx (slice t)) : core_ops_index_IndexMut (slice t) idx = { - indexInst = core_slice_index_Slice_coreopsindexIndexInst t idx inst; + indexInst = core_ops_index_IndexSliceTIInst t idx inst; index_mut = core_slice_index_Slice_index_mut t idx inst; index_mut_back = core_slice_index_Slice_index_mut_back t idx inst; } // Trait implementation: [core::array::[T; N]] -let core_array_Array_coreopsindexIndexInst (t idx : Type0) (n : usize) +let core_ops_index_IndexArrayInst (t idx : Type0) (n : usize) (inst : core_ops_index_Index (slice t) idx) : core_ops_index_Index (array t n) idx = { output = inst.output; @@ -604,10 +604,10 @@ let core_array_Array_coreopsindexIndexInst (t idx : Type0) (n : usize) } // Trait implementation: [core::array::[T; N]] -let core_array_Array_coreopsindexIndexMutInst (t idx : Type0) (n : usize) +let core_ops_index_IndexMutArrayIInst (t idx : Type0) (n : usize) (inst : core_ops_index_IndexMut (slice t) idx) : core_ops_index_IndexMut (array t n) idx = { - indexInst = core_array_Array_coreopsindexIndexInst t idx n inst.indexInst; + indexInst = core_ops_index_IndexArrayInst t idx n inst.indexInst; index_mut = core_array_Array_index_mut t idx n inst; index_mut_back = core_array_Array_index_mut_back t idx n inst; } @@ -651,13 +651,13 @@ let core_slice_index_usize_index_mut_back admit () // TODO // Trait implementation: [core::slice::index::private_slice_index::usize] -let core_slice_index_private_slice_index_usize_coresliceindexprivate_slice_indexSealedInst +let core_slice_index_private_slice_index_SealedUsizeInst : core_slice_index_private_slice_index_Sealed usize = () // Trait implementation: [core::slice::index::usize] -let core_slice_index_usize_coresliceindexSliceIndexInst (t : Type0) : +let core_slice_index_SliceIndexUsizeSliceTInst (t : Type0) : core_slice_index_SliceIndex usize (slice t) = { - sealedInst = core_slice_index_private_slice_index_usize_coresliceindexprivate_slice_indexSealedInst; + sealedInst = core_slice_index_private_slice_index_SealedUsizeInst; output = t; get = core_slice_index_usize_get t; get_mut = core_slice_index_usize_get_mut t; @@ -706,24 +706,24 @@ let alloc_vec_Vec_coreopsindexIndexMutInst (t idx : Type0) let alloc_vec_Vec_index_eq (#a : Type0) (v : alloc_vec_Vec a) (i : usize) : Lemma ( - alloc_vec_Vec_index a usize (core_slice_index_usize_coresliceindexSliceIndexInst a) v i == + alloc_vec_Vec_index a usize (core_slice_index_SliceIndexUsizeSliceTInst a) v i == alloc_vec_Vec_index_usize v i) - [SMTPat (alloc_vec_Vec_index a usize (core_slice_index_usize_coresliceindexSliceIndexInst a) v i)] + [SMTPat (alloc_vec_Vec_index a usize (core_slice_index_SliceIndexUsizeSliceTInst a) v i)] = admit() let alloc_vec_Vec_index_mut_eq (#a : Type0) (v : alloc_vec_Vec a) (i : usize) : Lemma ( - alloc_vec_Vec_index_mut a usize (core_slice_index_usize_coresliceindexSliceIndexInst a) v i == + alloc_vec_Vec_index_mut a usize (core_slice_index_SliceIndexUsizeSliceTInst a) v i == alloc_vec_Vec_index_usize v i) - [SMTPat (alloc_vec_Vec_index_mut a usize (core_slice_index_usize_coresliceindexSliceIndexInst a) v i)] + [SMTPat (alloc_vec_Vec_index_mut a usize (core_slice_index_SliceIndexUsizeSliceTInst a) v i)] = admit() let alloc_vec_Vec_index_mut_back_eq (#a : Type0) (v : alloc_vec_Vec a) (i : usize) (x : a) : Lemma ( - alloc_vec_Vec_index_mut_back a usize (core_slice_index_usize_coresliceindexSliceIndexInst a) v i x == + alloc_vec_Vec_index_mut_back a usize (core_slice_index_SliceIndexUsizeSliceTInst a) v i x == alloc_vec_Vec_update_usize v i x) - [SMTPat (alloc_vec_Vec_index_mut_back a usize (core_slice_index_usize_coresliceindexSliceIndexInst a) v i x)] + [SMTPat (alloc_vec_Vec_index_mut_back a usize (core_slice_index_SliceIndexUsizeSliceTInst a) v i x)] = admit() diff --git a/tests/fstar/betree_back_stateful/BetreeMain.Clauses.Template.fst b/tests/fstar/betree_back_stateful/BetreeMain.Clauses.Template.fst index 8722f0bf..4ae29302 100644 --- a/tests/fstar/betree_back_stateful/BetreeMain.Clauses.Template.fst +++ b/tests/fstar/betree_back_stateful/BetreeMain.Clauses.Template.fst @@ -6,94 +6,109 @@ 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 + Source: 'src/betree.rs', lines 276:4-276:24 *) 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 + Source: 'src/betree.rs', lines 284:4-284:51 *) 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 + Source: 'src/betree.rs', lines 339:4-339:73 *) 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 + Source: 'src/betree.rs', lines 789:4-792:34 *) 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 + Source: 'src/betree.rs', lines 819:4-819:90 *) 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 + Source: 'src/betree.rs', lines 636:4-636:80 *) 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 + Source: 'src/betree.rs', lines 395:4-395:63 *) 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 + Source: 'src/betree.rs', lines 709:4-709:58 *) 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 + Source: 'src/betree.rs', lines 674:4-674:77 *) 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 + Source: 'src/betree.rs', lines 689:4-692:34 *) 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 + Source: 'src/betree.rs', lines 502:4-505:5 *) 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 + Source: 'src/betree.rs', lines 653:4-656:32 *) 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 + Source: 'src/betree.rs', lines 444:4-447:5 *) 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 + Source: 'src/betree.rs', lines 410:4-415:26 *) 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 + Source: 'src/betree.rs', lines 588:4-593:5 *) 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..a2586431 100644 --- a/tests/fstar/betree_back_stateful/BetreeMain.Funs.fst +++ b/tests/fstar/betree_back_stateful/BetreeMain.Funs.fst @@ -8,14 +8,16 @@ include BetreeMain.Clauses #set-options "--z3rlimit 50 --fuel 1 --ifuel 1" -(** [betree_main::betree::load_internal_node]: forward function *) +(** [betree_main::betree::load_internal_node]: forward function + Source: 'src/betree.rs', lines 36:0-36:52 *) let betree_load_internal_node (id : u64) (st : state) : result (state & (betree_List_t (u64 & betree_Message_t))) = betree_utils_load_internal_node id st -(** [betree_main::betree::store_internal_node]: forward function *) +(** [betree_main::betree::store_internal_node]: forward function + Source: 'src/betree.rs', lines 41:0-41:60 *) let betree_store_internal_node (id : u64) (content : betree_List_t (u64 & betree_Message_t)) (st : state) : result (state & unit) @@ -23,12 +25,14 @@ let betree_store_internal_node let* (st0, _) = betree_utils_store_internal_node id content st in Return (st0, ()) -(** [betree_main::betree::load_leaf_node]: forward function *) +(** [betree_main::betree::load_leaf_node]: forward function + Source: 'src/betree.rs', lines 46:0-46:44 *) let betree_load_leaf_node (id : u64) (st : state) : result (state & (betree_List_t (u64 & u64))) = betree_utils_load_leaf_node id st -(** [betree_main::betree::store_leaf_node]: forward function *) +(** [betree_main::betree::store_leaf_node]: forward function + Source: 'src/betree.rs', lines 51:0-51:52 *) let betree_store_leaf_node (id : u64) (content : betree_List_t (u64 & u64)) (st : state) : result (state & unit) @@ -36,29 +40,35 @@ let betree_store_leaf_node let* (st0, _) = betree_utils_store_leaf_node id content st in Return (st0, ()) -(** [betree_main::betree::fresh_node_id]: forward function *) +(** [betree_main::betree::fresh_node_id]: forward function + Source: 'src/betree.rs', lines 55:0-55:48 *) let betree_fresh_node_id (counter : u64) : result u64 = let* _ = u64_add counter 1 in Return counter -(** [betree_main::betree::fresh_node_id]: backward function 0 *) +(** [betree_main::betree::fresh_node_id]: backward function 0 + Source: 'src/betree.rs', lines 55:0-55:48 *) 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 + Source: 'src/betree.rs', lines 206:4-206:20 *) 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 + Source: 'src/betree.rs', lines 210:4-210:36 *) 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 + Source: 'src/betree.rs', lines 210:4-210:36 *) 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 } -(** [betree_main::betree::upsert_update]: forward function *) +(** [betree_main::betree::upsert_update]: forward function + Source: 'src/betree.rs', lines 234:0-234:70 *) let betree_upsert_update (prev : option u64) (st : betree_UpsertFunState_t) : result u64 = begin match prev with @@ -77,7 +87,8 @@ 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 + Source: 'src/betree.rs', lines 276:4-276:24 *) let rec betree_List_len (t : Type0) (self : betree_List_t t) : Tot (result u64) (decreases (betree_List_len_decreases t self)) @@ -87,7 +98,8 @@ 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 + Source: 'src/betree.rs', lines 284:4-284:51 *) let rec betree_List_split_at (t : Type0) (self : betree_List_t t) (n : u64) : Tot (result ((betree_List_t t) & (betree_List_t t))) @@ -106,15 +118,17 @@ let rec betree_List_split_at | Betree_List_Nil -> Fail Failure end -(** [betree_main::betree::List::{1}::push_front]: merged forward/backward function - (there is a single backward function, and the forward function returns ()) *) +(** [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 ()) + Source: 'src/betree.rs', lines 299:4-299:34 *) let betree_List_push_front (t : Type0) (self : betree_List_t t) (x : t) : result (betree_List_t t) = let tl = core_mem_replace (betree_List_t t) self Betree_List_Nil in 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 + Source: 'src/betree.rs', lines 306:4-306:32 *) 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 +136,8 @@ 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 + Source: 'src/betree.rs', lines 306:4-306:32 *) 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 +146,29 @@ 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 + Source: 'src/betree.rs', lines 318:4-318:22 *) let betree_List_hd (t : Type0) (self : betree_List_t t) : result t = begin match self with | Betree_List_Cons hd 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 + Source: 'src/betree.rs', lines 327:4-327:44 *) +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 + Source: 'src/betree.rs', lines 339:4-339:73 *) +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 +176,15 @@ 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 + Source: 'src/betree.rs', lines 359:4-364:17 *) let betree_Leaf_split (self : betree_Leaf_t) (content : betree_List_t (u64 & u64)) (params : betree_Params_t) (node_id_cnt : betree_NodeIdCounter_t) @@ -185,7 +204,8 @@ 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 + Source: 'src/betree.rs', lines 359:4-364:17 *) 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 +222,8 @@ 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 + Source: 'src/betree.rs', lines 359:4-364:17 *) 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 +240,8 @@ 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 + Source: 'src/betree.rs', lines 359:4-364:17 *) 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 +259,8 @@ 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 + Source: 'src/betree.rs', lines 789:4-792:34 *) let rec betree_Node_lookup_first_message_for_key (key : u64) (msgs : betree_List_t (u64 & betree_Message_t)) : Tot (result (betree_List_t (u64 & betree_Message_t))) @@ -252,7 +275,8 @@ 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 + Source: 'src/betree.rs', lines 789:4-792:34 *) 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 +295,15 @@ 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 + Source: 'src/betree.rs', lines 819:4-819:90 *) let rec betree_Node_apply_upserts (msgs : betree_List_t (u64 & betree_Message_t)) (prev : option u64) (key : u64) (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 +323,15 @@ 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 + Source: 'src/betree.rs', lines 819:4-819:90 *) 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 +351,8 @@ 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 + Source: 'src/betree.rs', lines 636:4-636:80 *) let rec betree_Node_lookup_in_bindings (key : u64) (bindings : betree_List_t (u64 & u64)) : Tot (result (option u64)) @@ -340,7 +367,8 @@ 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 + Source: 'src/betree.rs', lines 395:4-395:63 *) let rec betree_Internal_lookup_in_children (self : betree_Internal_t) (key : u64) (st : state) : Tot (result (state & (option u64))) @@ -350,7 +378,8 @@ 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 + Source: 'src/betree.rs', lines 395:4-395:63 *) 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 +393,8 @@ 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 + Source: 'src/betree.rs', lines 709:4-709:58 *) and betree_Node_lookup (self : betree_Node_t) (key : u64) (st : state) : Tot (result (state & (option u64))) @@ -424,7 +454,8 @@ 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 + Source: 'src/betree.rs', lines 709:4-709:58 *) and betree_Node_lookup_back (self : betree_Node_t) (key : u64) (st : state) (st0 : state) : Tot (result (state & betree_Node_t)) @@ -486,8 +517,9 @@ 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 - (there is a single backward function, and the forward function returns ()) *) +(** [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 ()) + Source: 'src/betree.rs', lines 674:4-674:77 *) let rec betree_Node_filter_messages_for_key (key : u64) (msgs : betree_List_t (u64 & betree_Message_t)) : Tot (result (betree_List_t (u64 & betree_Message_t))) @@ -506,7 +538,8 @@ 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 + Source: 'src/betree.rs', lines 689:4-692:34 *) let rec betree_Node_lookup_first_message_after_key (key : u64) (msgs : betree_List_t (u64 & betree_Message_t)) : Tot (result (betree_List_t (u64 & betree_Message_t))) @@ -521,7 +554,8 @@ 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 + Source: 'src/betree.rs', lines 689:4-692:34 *) 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,15 +574,16 @@ 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 - (there is a single backward function, and the forward function returns ()) *) +(** [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 ()) + Source: 'src/betree.rs', lines 521:4-521:89 *) let betree_Node_apply_to_internal (msgs : betree_List_t (u64 & betree_Message_t)) (key : u64) (new_msg : betree_Message_t) : result (betree_List_t (u64 & betree_Message_t)) = let* 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,8 +634,9 @@ 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 - (there is a single backward function, and the forward function returns ()) *) +(** [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 ()) + Source: 'src/betree.rs', lines 502:4-505:5 *) let rec betree_Node_apply_messages_to_internal (msgs : betree_List_t (u64 & betree_Message_t)) (new_msgs : betree_List_t (u64 & betree_Message_t)) : @@ -615,7 +651,8 @@ 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 + Source: 'src/betree.rs', lines 653:4-656:32 *) let rec betree_Node_lookup_mut_in_bindings (key : u64) (bindings : betree_List_t (u64 & u64)) : Tot (result (betree_List_t (u64 & u64))) @@ -630,7 +667,8 @@ 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 + Source: 'src/betree.rs', lines 653:4-656:32 *) let rec betree_Node_lookup_mut_in_bindings_back (key : u64) (bindings : betree_List_t (u64 & u64)) (ret : betree_List_t (u64 & u64)) : @@ -648,15 +686,16 @@ 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 - (there is a single backward function, and the forward function returns ()) *) +(** [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 ()) + Source: 'src/betree.rs', lines 460:4-460:87 *) let betree_Node_apply_to_leaf (bindings : betree_List_t (u64 & u64)) (key : u64) (new_msg : betree_Message_t) : result (betree_List_t (u64 & u64)) = let* 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,8 +727,9 @@ 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 - (there is a single backward function, and the forward function returns ()) *) +(** [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 ()) + Source: 'src/betree.rs', lines 444:4-447:5 *) let rec betree_Node_apply_messages_to_leaf (bindings : betree_List_t (u64 & u64)) (new_msgs : betree_List_t (u64 & betree_Message_t)) : @@ -704,7 +744,8 @@ 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 + Source: 'src/betree.rs', lines 410:4-415:26 *) let rec betree_Internal_flush (self : betree_Internal_t) (params : betree_Params_t) (node_id_cnt : betree_NodeIdCounter_t) @@ -713,7 +754,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 +794,8 @@ 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 + Source: 'src/betree.rs', lines 410:4-415:26 *) and betree_Internal_flush_back'a (self : betree_Internal_t) (params : betree_Params_t) (node_id_cnt : betree_NodeIdCounter_t) @@ -762,7 +805,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 +845,8 @@ 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 + Source: 'src/betree.rs', lines 410:4-415:26 *) and betree_Internal_flush_back1 (self : betree_Internal_t) (params : betree_Params_t) (node_id_cnt : betree_NodeIdCounter_t) @@ -811,7 +856,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 +896,8 @@ 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 + Source: 'src/betree.rs', lines 588:4-593:5 *) and betree_Node_apply_messages (self : betree_Node_t) (params : betree_Params_t) (node_id_cnt : betree_NodeIdCounter_t) @@ -891,7 +938,8 @@ 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 + Source: 'src/betree.rs', lines 588:4-593:5 *) and betree_Node_apply_messages_back'a (self : betree_Node_t) (params : betree_Params_t) (node_id_cnt : betree_NodeIdCounter_t) @@ -937,7 +985,8 @@ 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 + Source: 'src/betree.rs', lines 588:4-593:5 *) and betree_Node_apply_messages_back1 (self : betree_Node_t) (params : betree_Params_t) (node_id_cnt : betree_NodeIdCounter_t) @@ -979,7 +1028,8 @@ 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 + Source: 'src/betree.rs', lines 576:4-582:5 *) let betree_Node_apply (self : betree_Node_t) (params : betree_Params_t) (node_id_cnt : betree_NodeIdCounter_t) (key : u64) @@ -996,7 +1046,8 @@ 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 + Source: 'src/betree.rs', lines 576:4-582:5 *) let betree_Node_apply_back'a (self : betree_Node_t) (params : betree_Params_t) (node_id_cnt : betree_NodeIdCounter_t) (key : u64) @@ -1015,7 +1066,8 @@ 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 + Source: 'src/betree.rs', lines 576:4-582:5 *) let betree_Node_apply_back1 (self : betree_Node_t) (params : betree_Params_t) (node_id_cnt : betree_NodeIdCounter_t) (key : u64) @@ -1034,7 +1086,8 @@ 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 + Source: 'src/betree.rs', lines 849:4-849:60 *) let betree_BeTree_new (min_flush_size : u64) (split_size : u64) (st : state) : result (state & betree_BeTree_t) @@ -1050,7 +1103,8 @@ 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 + Source: 'src/betree.rs', lines 868:4-868:47 *) let betree_BeTree_apply (self : betree_BeTree_t) (key : u64) (msg : betree_Message_t) (st : state) : result (state & unit) @@ -1062,7 +1116,8 @@ 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 + Source: 'src/betree.rs', lines 868:4-868:47 *) let betree_BeTree_apply_back (self : betree_BeTree_t) (key : u64) (msg : betree_Message_t) (st : state) (st0 : state) : @@ -1078,7 +1133,8 @@ 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 + Source: 'src/betree.rs', lines 874:4-874:52 *) let betree_BeTree_insert (self : betree_BeTree_t) (key : u64) (value : u64) (st : state) : result (state & unit) @@ -1089,7 +1145,8 @@ 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 + Source: 'src/betree.rs', lines 874:4-874:52 *) let betree_BeTree_insert_back (self : betree_BeTree_t) (key : u64) (value : u64) (st : state) (st0 : state) : @@ -1101,7 +1158,8 @@ 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 + Source: 'src/betree.rs', lines 880:4-880:38 *) 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 +1167,8 @@ 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 + Source: 'src/betree.rs', lines 880:4-880:38 *) let betree_BeTree_delete_back (self : betree_BeTree_t) (key : u64) (st : state) (st0 : state) : result (state & betree_BeTree_t) @@ -1119,7 +1178,8 @@ 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 + Source: 'src/betree.rs', lines 886:4-886:59 *) let betree_BeTree_upsert (self : betree_BeTree_t) (key : u64) (upd : betree_UpsertFunState_t) (st : state) : @@ -1131,7 +1191,8 @@ 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 + Source: 'src/betree.rs', lines 886:4-886:59 *) let betree_BeTree_upsert_back (self : betree_BeTree_t) (key : u64) (upd : betree_UpsertFunState_t) (st : state) (st0 : state) : @@ -1143,14 +1204,16 @@ 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 + Source: 'src/betree.rs', lines 895:4-895:62 *) let betree_BeTree_lookup (self : betree_BeTree_t) (key : u64) (st : state) : result (state & (option u64)) = betree_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 + Source: 'src/betree.rs', lines 895:4-895:62 *) let betree_BeTree_lookup_back (self : betree_BeTree_t) (key : u64) (st : state) (st0 : state) : result (state & betree_BeTree_t) @@ -1158,7 +1221,8 @@ let betree_BeTree_lookup_back let* (st1, n) = betree_Node_lookup_back self.root key st st0 in Return (st1, { self with root = n }) -(** [betree_main::main]: forward function *) +(** [betree_main::main]: forward function + Source: 'src/betree_main.rs', lines 5:0-5:9 *) let main : result unit = Return () diff --git a/tests/fstar/betree_back_stateful/BetreeMain.Opaque.fsti b/tests/fstar/betree_back_stateful/BetreeMain.Opaque.fsti index c5d0a814..b89c8718 100644 --- a/tests/fstar/betree_back_stateful/BetreeMain.Opaque.fsti +++ b/tests/fstar/betree_back_stateful/BetreeMain.Opaque.fsti @@ -6,25 +6,30 @@ include BetreeMain.Types #set-options "--z3rlimit 50 --fuel 1 --ifuel 1" -(** [betree_main::betree_utils::load_internal_node]: forward function *) +(** [betree_main::betree_utils::load_internal_node]: forward function + Source: 'src/betree_utils.rs', lines 98:0-98:63 *) val betree_utils_load_internal_node : u64 -> state -> result (state & (betree_List_t (u64 & betree_Message_t))) -(** [betree_main::betree_utils::store_internal_node]: forward function *) +(** [betree_main::betree_utils::store_internal_node]: forward function + Source: 'src/betree_utils.rs', lines 115:0-115:71 *) val betree_utils_store_internal_node : u64 -> betree_List_t (u64 & betree_Message_t) -> state -> result (state & unit) -(** [betree_main::betree_utils::load_leaf_node]: forward function *) +(** [betree_main::betree_utils::load_leaf_node]: forward function + Source: 'src/betree_utils.rs', lines 132:0-132:55 *) val betree_utils_load_leaf_node : u64 -> state -> result (state & (betree_List_t (u64 & u64))) -(** [betree_main::betree_utils::store_leaf_node]: forward function *) +(** [betree_main::betree_utils::store_leaf_node]: forward function + Source: 'src/betree_utils.rs', lines 145:0-145:63 *) 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 + Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/option.rs', lines 932:4-932:34 *) val core_option_Option_unwrap (t : Type0) : option t -> state -> result (state & t) diff --git a/tests/fstar/betree_back_stateful/BetreeMain.Types.fsti b/tests/fstar/betree_back_stateful/BetreeMain.Types.fsti index 9320f6b7..a098ec19 100644 --- a/tests/fstar/betree_back_stateful/BetreeMain.Types.fsti +++ b/tests/fstar/betree_back_stateful/BetreeMain.Types.fsti @@ -5,43 +5,52 @@ open Primitives #set-options "--z3rlimit 50 --fuel 1 --ifuel 1" -(** [betree_main::betree::List] *) +(** [betree_main::betree::List] + Source: 'src/betree.rs', lines 17:0-17:23 *) type betree_List_t (t : Type0) = | Betree_List_Cons : t -> betree_List_t t -> betree_List_t t | Betree_List_Nil : betree_List_t t -(** [betree_main::betree::UpsertFunState] *) +(** [betree_main::betree::UpsertFunState] + Source: 'src/betree.rs', lines 63:0-63:23 *) type betree_UpsertFunState_t = | Betree_UpsertFunState_Add : u64 -> betree_UpsertFunState_t | Betree_UpsertFunState_Sub : u64 -> betree_UpsertFunState_t -(** [betree_main::betree::Message] *) +(** [betree_main::betree::Message] + Source: 'src/betree.rs', lines 69:0-69:23 *) type betree_Message_t = | Betree_Message_Insert : u64 -> betree_Message_t | Betree_Message_Delete : betree_Message_t | Betree_Message_Upsert : betree_UpsertFunState_t -> betree_Message_t -(** [betree_main::betree::Leaf] *) +(** [betree_main::betree::Leaf] + Source: 'src/betree.rs', lines 167:0-167:11 *) type betree_Leaf_t = { id : u64; size : u64; } -(** [betree_main::betree::Internal] *) +(** [betree_main::betree::Internal] + Source: 'src/betree.rs', lines 156:0-156:15 *) type betree_Internal_t = { id : u64; pivot : u64; left : betree_Node_t; right : betree_Node_t; } -(** [betree_main::betree::Node] *) +(** [betree_main::betree::Node] + Source: 'src/betree.rs', lines 179:0-179:9 *) and betree_Node_t = | Betree_Node_Internal : betree_Internal_t -> betree_Node_t | Betree_Node_Leaf : betree_Leaf_t -> betree_Node_t -(** [betree_main::betree::Params] *) +(** [betree_main::betree::Params] + Source: 'src/betree.rs', lines 187:0-187:13 *) type betree_Params_t = { min_flush_size : u64; split_size : u64; } -(** [betree_main::betree::NodeIdCounter] *) +(** [betree_main::betree::NodeIdCounter] + Source: 'src/betree.rs', lines 201:0-201:20 *) type betree_NodeIdCounter_t = { next_node_id : u64; } -(** [betree_main::betree::BeTree] *) +(** [betree_main::betree::BeTree] + Source: 'src/betree.rs', lines 218:0-218:17 *) type betree_BeTree_t = { params : betree_Params_t; diff --git a/tests/fstar/betree_back_stateful/Primitives.fst b/tests/fstar/betree_back_stateful/Primitives.fst index 3297803c..94322ead 100644 --- a/tests/fstar/betree_back_stateful/Primitives.fst +++ b/tests/fstar/betree_back_stateful/Primitives.fst @@ -351,14 +351,14 @@ let alloc_boxed_Box_deref_mut (t : Type0) (x : t) : result t = Return x let alloc_boxed_Box_deref_mut_back (t : Type) (_ : t) (x : t) : result t = Return x // Trait instance -let alloc_boxed_Box_coreOpsDerefInst (self : Type0) : core_ops_deref_Deref self = { +let alloc_boxed_Box_coreopsDerefInst (self : Type0) : core_ops_deref_Deref self = { target = self; deref = alloc_boxed_Box_deref self; } // Trait instance -let alloc_boxed_Box_coreOpsDerefMutInst (self : Type0) : core_ops_deref_DerefMut self = { - derefInst = alloc_boxed_Box_coreOpsDerefInst self; +let alloc_boxed_Box_coreopsDerefMutInst (self : Type0) : core_ops_deref_DerefMut self = { + derefInst = alloc_boxed_Box_coreopsDerefInst self; deref_mut = alloc_boxed_Box_deref_mut self; deref_mut_back = alloc_boxed_Box_deref_mut_back self; } @@ -483,23 +483,23 @@ let core_slice_index_Slice_index | Some x -> Return x // [core::slice::index::Range:::get]: forward function -let core_slice_index_Range_get (t : Type0) (i : core_ops_range_Range usize) (s : slice t) : +let core_slice_index_RangeUsize_get (t : Type0) (i : core_ops_range_Range usize) (s : slice t) : result (option (slice t)) = admit () // TODO // [core::slice::index::Range::get_mut]: forward function -let core_slice_index_Range_get_mut +let core_slice_index_RangeUsize_get_mut (t : Type0) : core_ops_range_Range usize → slice t → result (option (slice t)) = admit () // TODO // [core::slice::index::Range::get_mut]: backward function 0 -let core_slice_index_Range_get_mut_back +let core_slice_index_RangeUsize_get_mut_back (t : Type0) : core_ops_range_Range usize → slice t → option (slice t) → result (slice t) = admit () // TODO // [core::slice::index::Range::get_unchecked]: forward function -let core_slice_index_Range_get_unchecked +let core_slice_index_RangeUsize_get_unchecked (t : Type0) : core_ops_range_Range usize → const_raw_ptr (slice t) → result (const_raw_ptr (slice t)) = // Don't know what the model should be - for now we always fail to make @@ -507,7 +507,7 @@ let core_slice_index_Range_get_unchecked fun _ _ -> Fail Failure // [core::slice::index::Range::get_unchecked_mut]: forward function -let core_slice_index_Range_get_unchecked_mut +let core_slice_index_RangeUsize_get_unchecked_mut (t : Type0) : core_ops_range_Range usize → mut_raw_ptr (slice t) → result (mut_raw_ptr (slice t)) = // Don't know what the model should be - for now we always fail to make @@ -515,17 +515,17 @@ let core_slice_index_Range_get_unchecked_mut fun _ _ -> Fail Failure // [core::slice::index::Range::index]: forward function -let core_slice_index_Range_index +let core_slice_index_RangeUsize_index (t : Type0) : core_ops_range_Range usize → slice t → result (slice t) = admit () // TODO // [core::slice::index::Range::index_mut]: forward function -let core_slice_index_Range_index_mut +let core_slice_index_RangeUsize_index_mut (t : Type0) : core_ops_range_Range usize → slice t → result (slice t) = admit () // TODO // [core::slice::index::Range::index_mut]: backward function 0 -let core_slice_index_Range_index_mut_back +let core_slice_index_RangeUsize_index_mut_back (t : Type0) : core_ops_range_Range usize → slice t → slice t → result (slice t) = admit () // TODO @@ -559,44 +559,44 @@ let core_array_Array_index_mut_back (a : array t n) (i : idx) (x : inst.indexInst.output) : result (array t n) = admit () // TODO -// Trait implementation: [core::slice::index::[T]] -let core_slice_index_Slice_coreopsindexIndexInst (t idx : Type0) - (inst : core_slice_index_SliceIndex idx (slice t)) : - core_ops_index_Index (slice t) idx = { - output = inst.output; - index = core_slice_index_Slice_index t idx inst; -} - // Trait implementation: [core::slice::index::private_slice_index::Range] -let core_slice_index_private_slice_index_Range_coresliceindexprivate_slice_indexSealedInst +let core_slice_index_private_slice_index_SealedRangeUsizeInst : core_slice_index_private_slice_index_Sealed (core_ops_range_Range usize) = () // Trait implementation: [core::slice::index::Range] -let core_slice_index_Range_coresliceindexSliceIndexInst (t : Type0) : +let core_slice_index_SliceIndexRangeUsizeSliceTInst (t : Type0) : core_slice_index_SliceIndex (core_ops_range_Range usize) (slice t) = { - sealedInst = core_slice_index_private_slice_index_Range_coresliceindexprivate_slice_indexSealedInst; + sealedInst = core_slice_index_private_slice_index_SealedRangeUsizeInst; output = slice t; - get = core_slice_index_Range_get t; - get_mut = core_slice_index_Range_get_mut t; - get_mut_back = core_slice_index_Range_get_mut_back t; - get_unchecked = core_slice_index_Range_get_unchecked t; - get_unchecked_mut = core_slice_index_Range_get_unchecked_mut t; - index = core_slice_index_Range_index t; - index_mut = core_slice_index_Range_index_mut t; - index_mut_back = core_slice_index_Range_index_mut_back t; + get = core_slice_index_RangeUsize_get t; + get_mut = core_slice_index_RangeUsize_get_mut t; + get_mut_back = core_slice_index_RangeUsize_get_mut_back t; + get_unchecked = core_slice_index_RangeUsize_get_unchecked t; + get_unchecked_mut = core_slice_index_RangeUsize_get_unchecked_mut t; + index = core_slice_index_RangeUsize_index t; + index_mut = core_slice_index_RangeUsize_index_mut t; + index_mut_back = core_slice_index_RangeUsize_index_mut_back t; +} + +// Trait implementation: [core::slice::index::[T]] +let core_ops_index_IndexSliceTIInst (t idx : Type0) + (inst : core_slice_index_SliceIndex idx (slice t)) : + core_ops_index_Index (slice t) idx = { + output = inst.output; + index = core_slice_index_Slice_index t idx inst; } // Trait implementation: [core::slice::index::[T]] -let core_slice_index_Slice_coreopsindexIndexMutInst (t idx : Type0) +let core_ops_index_IndexMutSliceTIInst (t idx : Type0) (inst : core_slice_index_SliceIndex idx (slice t)) : core_ops_index_IndexMut (slice t) idx = { - indexInst = core_slice_index_Slice_coreopsindexIndexInst t idx inst; + indexInst = core_ops_index_IndexSliceTIInst t idx inst; index_mut = core_slice_index_Slice_index_mut t idx inst; index_mut_back = core_slice_index_Slice_index_mut_back t idx inst; } // Trait implementation: [core::array::[T; N]] -let core_array_Array_coreopsindexIndexInst (t idx : Type0) (n : usize) +let core_ops_index_IndexArrayInst (t idx : Type0) (n : usize) (inst : core_ops_index_Index (slice t) idx) : core_ops_index_Index (array t n) idx = { output = inst.output; @@ -604,10 +604,10 @@ let core_array_Array_coreopsindexIndexInst (t idx : Type0) (n : usize) } // Trait implementation: [core::array::[T; N]] -let core_array_Array_coreopsindexIndexMutInst (t idx : Type0) (n : usize) +let core_ops_index_IndexMutArrayIInst (t idx : Type0) (n : usize) (inst : core_ops_index_IndexMut (slice t) idx) : core_ops_index_IndexMut (array t n) idx = { - indexInst = core_array_Array_coreopsindexIndexInst t idx n inst.indexInst; + indexInst = core_ops_index_IndexArrayInst t idx n inst.indexInst; index_mut = core_array_Array_index_mut t idx n inst; index_mut_back = core_array_Array_index_mut_back t idx n inst; } @@ -651,13 +651,13 @@ let core_slice_index_usize_index_mut_back admit () // TODO // Trait implementation: [core::slice::index::private_slice_index::usize] -let core_slice_index_private_slice_index_usize_coresliceindexprivate_slice_indexSealedInst +let core_slice_index_private_slice_index_SealedUsizeInst : core_slice_index_private_slice_index_Sealed usize = () // Trait implementation: [core::slice::index::usize] -let core_slice_index_usize_coresliceindexSliceIndexInst (t : Type0) : +let core_slice_index_SliceIndexUsizeSliceTInst (t : Type0) : core_slice_index_SliceIndex usize (slice t) = { - sealedInst = core_slice_index_private_slice_index_usize_coresliceindexprivate_slice_indexSealedInst; + sealedInst = core_slice_index_private_slice_index_SealedUsizeInst; output = t; get = core_slice_index_usize_get t; get_mut = core_slice_index_usize_get_mut t; @@ -706,24 +706,24 @@ let alloc_vec_Vec_coreopsindexIndexMutInst (t idx : Type0) let alloc_vec_Vec_index_eq (#a : Type0) (v : alloc_vec_Vec a) (i : usize) : Lemma ( - alloc_vec_Vec_index a usize (core_slice_index_usize_coresliceindexSliceIndexInst a) v i == + alloc_vec_Vec_index a usize (core_slice_index_SliceIndexUsizeSliceTInst a) v i == alloc_vec_Vec_index_usize v i) - [SMTPat (alloc_vec_Vec_index a usize (core_slice_index_usize_coresliceindexSliceIndexInst a) v i)] + [SMTPat (alloc_vec_Vec_index a usize (core_slice_index_SliceIndexUsizeSliceTInst a) v i)] = admit() let alloc_vec_Vec_index_mut_eq (#a : Type0) (v : alloc_vec_Vec a) (i : usize) : Lemma ( - alloc_vec_Vec_index_mut a usize (core_slice_index_usize_coresliceindexSliceIndexInst a) v i == + alloc_vec_Vec_index_mut a usize (core_slice_index_SliceIndexUsizeSliceTInst a) v i == alloc_vec_Vec_index_usize v i) - [SMTPat (alloc_vec_Vec_index_mut a usize (core_slice_index_usize_coresliceindexSliceIndexInst a) v i)] + [SMTPat (alloc_vec_Vec_index_mut a usize (core_slice_index_SliceIndexUsizeSliceTInst a) v i)] = admit() let alloc_vec_Vec_index_mut_back_eq (#a : Type0) (v : alloc_vec_Vec a) (i : usize) (x : a) : Lemma ( - alloc_vec_Vec_index_mut_back a usize (core_slice_index_usize_coresliceindexSliceIndexInst a) v i x == + alloc_vec_Vec_index_mut_back a usize (core_slice_index_SliceIndexUsizeSliceTInst a) v i x == alloc_vec_Vec_update_usize v i x) - [SMTPat (alloc_vec_Vec_index_mut_back a usize (core_slice_index_usize_coresliceindexSliceIndexInst a) v i x)] + [SMTPat (alloc_vec_Vec_index_mut_back a usize (core_slice_index_SliceIndexUsizeSliceTInst a) v i x)] = admit() |