diff options
Diffstat (limited to '')
| -rw-r--r-- | tests/fstar/betree/Betree.Funs.fst (renamed from tests/fstar/betree/BetreeMain.Funs.fst) | 88 |
1 files changed, 44 insertions, 44 deletions
diff --git a/tests/fstar/betree/BetreeMain.Funs.fst b/tests/fstar/betree/Betree.Funs.fst index 9942ef68..07f561f5 100644 --- a/tests/fstar/betree/BetreeMain.Funs.fst +++ b/tests/fstar/betree/Betree.Funs.fst @@ -1,14 +1,14 @@ (** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *) -(** [betree_main]: function definitions *) -module BetreeMain.Funs +(** [betree]: function definitions *) +module Betree.Funs open Primitives -include BetreeMain.Types -include BetreeMain.FunsExternal -include BetreeMain.Clauses +include Betree.Types +include Betree.FunsExternal +include Betree.Clauses #set-options "--z3rlimit 50 --fuel 1 --ifuel 1" -(** [betree_main::betree::load_internal_node]: +(** [betree::betree::load_internal_node]: Source: 'src/betree.rs', lines 36:0-36:52 *) let betree_load_internal_node (id : u64) (st : state) : @@ -16,7 +16,7 @@ let betree_load_internal_node = betree_utils_load_internal_node id st -(** [betree_main::betree::store_internal_node]: +(** [betree::betree::store_internal_node]: 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) : @@ -24,13 +24,13 @@ let betree_store_internal_node = betree_utils_store_internal_node id content st -(** [betree_main::betree::load_leaf_node]: +(** [betree::betree::load_leaf_node]: 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]: +(** [betree::betree::store_leaf_node]: Source: 'src/betree.rs', lines 51:0-51:52 *) let betree_store_leaf_node (id : u64) (content : betree_List_t (u64 & u64)) (st : state) : @@ -38,24 +38,24 @@ let betree_store_leaf_node = betree_utils_store_leaf_node id content st -(** [betree_main::betree::fresh_node_id]: +(** [betree::betree::fresh_node_id]: Source: 'src/betree.rs', lines 55:0-55:48 *) let betree_fresh_node_id (counter : u64) : result (u64 & u64) = let* counter1 = u64_add counter 1 in Ok (counter, counter1) -(** [betree_main::betree::{betree_main::betree::NodeIdCounter}::new]: +(** [betree::betree::{betree::betree::NodeIdCounter}::new]: Source: 'src/betree.rs', lines 206:4-206:20 *) let betree_NodeIdCounter_new : result betree_NodeIdCounter_t = Ok { next_node_id = 0 } -(** [betree_main::betree::{betree_main::betree::NodeIdCounter}::fresh_id]: +(** [betree::betree::{betree::betree::NodeIdCounter}::fresh_id]: Source: 'src/betree.rs', lines 210:4-210:36 *) let betree_NodeIdCounter_fresh_id (self : betree_NodeIdCounter_t) : result (u64 & betree_NodeIdCounter_t) = let* i = u64_add self.next_node_id 1 in Ok (self.next_node_id, { next_node_id = i }) -(** [betree_main::betree::upsert_update]: +(** [betree::betree::upsert_update]: Source: 'src/betree.rs', lines 234:0-234:70 *) let betree_upsert_update (prev : option u64) (st : betree_UpsertFunState_t) : result u64 = @@ -75,7 +75,7 @@ let betree_upsert_update end end -(** [betree_main::betree::{betree_main::betree::List<T>#1}::len]: +(** [betree::betree::{betree::betree::List<T>#1}::len]: Source: 'src/betree.rs', lines 276:4-276:24 *) let rec betree_List_len (t : Type0) (self : betree_List_t t) : @@ -86,7 +86,7 @@ let rec betree_List_len | Betree_List_Nil -> Ok 0 end -(** [betree_main::betree::{betree_main::betree::List<T>#1}::split_at]: +(** [betree::betree::{betree::betree::List<T>#1}::split_at]: Source: 'src/betree.rs', lines 284:4-284:51 *) let rec betree_List_split_at (t : Type0) (self : betree_List_t t) (n : u64) : @@ -105,14 +105,14 @@ let rec betree_List_split_at | Betree_List_Nil -> Fail Failure end -(** [betree_main::betree::{betree_main::betree::List<T>#1}::push_front]: +(** [betree::betree::{betree::betree::List<T>#1}::push_front]: 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 Ok (Betree_List_Cons x tl) -(** [betree_main::betree::{betree_main::betree::List<T>#1}::pop_front]: +(** [betree::betree::{betree::betree::List<T>#1}::pop_front]: Source: 'src/betree.rs', lines 306:4-306:32 *) let betree_List_pop_front (t : Type0) (self : betree_List_t t) : result (t & (betree_List_t t)) = @@ -122,7 +122,7 @@ let betree_List_pop_front | Betree_List_Nil -> Fail Failure end -(** [betree_main::betree::{betree_main::betree::List<T>#1}::hd]: +(** [betree::betree::{betree::betree::List<T>#1}::hd]: 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 @@ -130,7 +130,7 @@ let betree_List_hd (t : Type0) (self : betree_List_t t) : result t = | Betree_List_Nil -> Fail Failure end -(** [betree_main::betree::{betree_main::betree::List<(u64, T)>#2}::head_has_key]: +(** [betree::betree::{betree::betree::List<(u64, T)>#2}::head_has_key]: Source: 'src/betree.rs', lines 327:4-327:44 *) let betree_ListPairU64T_head_has_key (t : Type0) (self : betree_List_t (u64 & t)) (key : u64) : result bool = @@ -139,7 +139,7 @@ let betree_ListPairU64T_head_has_key | Betree_List_Nil -> Ok false end -(** [betree_main::betree::{betree_main::betree::List<(u64, T)>#2}::partition_at_pivot]: +(** [betree::betree::{betree::betree::List<(u64, T)>#2}::partition_at_pivot]: Source: 'src/betree.rs', lines 339:4-339:73 *) let rec betree_ListPairU64T_partition_at_pivot (t : Type0) (self : betree_List_t (u64 & t)) (pivot : u64) : @@ -158,7 +158,7 @@ let rec betree_ListPairU64T_partition_at_pivot | Betree_List_Nil -> Ok (Betree_List_Nil, Betree_List_Nil) end -(** [betree_main::betree::{betree_main::betree::Leaf#3}::split]: +(** [betree::betree::{betree::betree::Leaf#3}::split]: Source: 'src/betree.rs', lines 359:4-364:17 *) let betree_Leaf_split (self : betree_Leaf_t) (content : betree_List_t (u64 & u64)) @@ -179,7 +179,7 @@ let betree_Leaf_split Ok (st2, ({ id = self.id; pivot = pivot; left = n; right = n1 }, node_id_cnt2)) -(** [betree_main::betree::{betree_main::betree::Node#5}::lookup_first_message_for_key]: +(** [betree::betree::{betree::betree::Node#5}::lookup_first_message_for_key]: 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)) : @@ -203,7 +203,7 @@ let rec betree_Node_lookup_first_message_for_key | Betree_List_Nil -> Ok (Betree_List_Nil, Ok) end -(** [betree_main::betree::{betree_main::betree::Node#5}::lookup_in_bindings]: +(** [betree::betree::{betree::betree::Node#5}::lookup_in_bindings]: Source: 'src/betree.rs', lines 636:4-636:80 *) let rec betree_Node_lookup_in_bindings (key : u64) (bindings : betree_List_t (u64 & u64)) : @@ -219,7 +219,7 @@ let rec betree_Node_lookup_in_bindings | Betree_List_Nil -> Ok None end -(** [betree_main::betree::{betree_main::betree::Node#5}::apply_upserts]: +(** [betree::betree::{betree::betree::Node#5}::apply_upserts]: 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) @@ -246,7 +246,7 @@ let rec betree_Node_apply_upserts Betree_Message_Insert v) in Ok (v, msgs1) -(** [betree_main::betree::{betree_main::betree::Internal#4}::lookup_in_children]: +(** [betree::betree::{betree::betree::Internal#4}::lookup_in_children]: Source: 'src/betree.rs', lines 395:4-395:63 *) let rec betree_Internal_lookup_in_children (self : betree_Internal_t) (key : u64) (st : state) : @@ -261,7 +261,7 @@ let rec betree_Internal_lookup_in_children let* (st1, (o, n)) = betree_Node_lookup self.right key st in Ok (st1, (o, { self with right = n })) -(** [betree_main::betree::{betree_main::betree::Node#5}::lookup]: +(** [betree::betree::{betree::betree::Node#5}::lookup]: Source: 'src/betree.rs', lines 709:4-709:58 *) and betree_Node_lookup (self : betree_Node_t) (key : u64) (st : state) : @@ -317,7 +317,7 @@ and betree_Node_lookup Ok (st1, (o, Betree_Node_Leaf node)) end -(** [betree_main::betree::{betree_main::betree::Node#5}::filter_messages_for_key]: +(** [betree::betree::{betree::betree::Node#5}::filter_messages_for_key]: 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)) : @@ -337,7 +337,7 @@ let rec betree_Node_filter_messages_for_key | Betree_List_Nil -> Ok Betree_List_Nil end -(** [betree_main::betree::{betree_main::betree::Node#5}::lookup_first_message_after_key]: +(** [betree::betree::{betree::betree::Node#5}::lookup_first_message_after_key]: 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)) : @@ -361,7 +361,7 @@ let rec betree_Node_lookup_first_message_after_key | Betree_List_Nil -> Ok (Betree_List_Nil, Ok) end -(** [betree_main::betree::{betree_main::betree::Node#5}::apply_to_internal]: +(** [betree::betree::{betree::betree::Node#5}::apply_to_internal]: 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) @@ -421,7 +421,7 @@ let betree_Node_apply_to_internal betree_List_push_front (u64 & betree_Message_t) msgs1 (key, new_msg) in lookup_first_message_for_key_back msgs2 -(** [betree_main::betree::{betree_main::betree::Node#5}::apply_messages_to_internal]: +(** [betree::betree::{betree::betree::Node#5}::apply_messages_to_internal]: 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)) @@ -437,7 +437,7 @@ let rec betree_Node_apply_messages_to_internal | Betree_List_Nil -> Ok msgs end -(** [betree_main::betree::{betree_main::betree::Node#5}::lookup_mut_in_bindings]: +(** [betree::betree::{betree::betree::Node#5}::lookup_mut_in_bindings]: 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)) : @@ -461,7 +461,7 @@ let rec betree_Node_lookup_mut_in_bindings | Betree_List_Nil -> Ok (Betree_List_Nil, Ok) end -(** [betree_main::betree::{betree_main::betree::Node#5}::apply_to_leaf]: +(** [betree::betree::{betree::betree::Node#5}::apply_to_leaf]: Source: 'src/betree.rs', lines 460:4-460:87 *) let betree_Node_apply_to_leaf (bindings : betree_List_t (u64 & u64)) (key : u64) @@ -497,7 +497,7 @@ let betree_Node_apply_to_leaf lookup_mut_in_bindings_back bindings2 end -(** [betree_main::betree::{betree_main::betree::Node#5}::apply_messages_to_leaf]: +(** [betree::betree::{betree::betree::Node#5}::apply_messages_to_leaf]: Source: 'src/betree.rs', lines 444:4-447:5 *) let rec betree_Node_apply_messages_to_leaf (bindings : betree_List_t (u64 & u64)) @@ -513,7 +513,7 @@ let rec betree_Node_apply_messages_to_leaf | Betree_List_Nil -> Ok bindings end -(** [betree_main::betree::{betree_main::betree::Internal#4}::flush]: +(** [betree::betree::{betree::betree::Internal#4}::flush]: Source: 'src/betree.rs', lines 410:4-415:26 *) let rec betree_Internal_flush (self : betree_Internal_t) (params : betree_Params_t) @@ -550,7 +550,7 @@ let rec betree_Internal_flush let (n, node_id_cnt1) = p1 in Ok (st1, (msgs_left, ({ self with right = n }, node_id_cnt1))) -(** [betree_main::betree::{betree_main::betree::Node#5}::apply_messages]: +(** [betree::betree::{betree::betree::Node#5}::apply_messages]: Source: 'src/betree.rs', lines 588:4-593:5 *) and betree_Node_apply_messages (self : betree_Node_t) (params : betree_Params_t) @@ -591,7 +591,7 @@ and betree_Node_apply_messages Ok (st2, (Betree_Node_Leaf { node with size = len }, node_id_cnt)) end -(** [betree_main::betree::{betree_main::betree::Node#5}::apply]: +(** [betree::betree::{betree::betree::Node#5}::apply]: Source: 'src/betree.rs', lines 576:4-582:5 *) let betree_Node_apply (self : betree_Node_t) (params : betree_Params_t) @@ -605,7 +605,7 @@ let betree_Node_apply let (self1, node_id_cnt1) = p in Ok (st1, (self1, node_id_cnt1)) -(** [betree_main::betree::{betree_main::betree::BeTree#6}::new]: +(** [betree::betree::{betree::betree::BeTree#6}::new]: Source: 'src/betree.rs', lines 849:4-849:60 *) let betree_BeTree_new (min_flush_size : u64) (split_size : u64) (st : state) : @@ -621,7 +621,7 @@ let betree_BeTree_new root = (Betree_Node_Leaf { id = id; size = 0 }) }) -(** [betree_main::betree::{betree_main::betree::BeTree#6}::apply]: +(** [betree::betree::{betree::betree::BeTree#6}::apply]: 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) : @@ -632,7 +632,7 @@ let betree_BeTree_apply let (n, nic) = p in Ok (st1, { self with node_id_cnt = nic; root = n }) -(** [betree_main::betree::{betree_main::betree::BeTree#6}::insert]: +(** [betree::betree::{betree::betree::BeTree#6}::insert]: Source: 'src/betree.rs', lines 874:4-874:52 *) let betree_BeTree_insert (self : betree_BeTree_t) (key : u64) (value : u64) (st : state) : @@ -640,7 +640,7 @@ let betree_BeTree_insert = betree_BeTree_apply self key (Betree_Message_Insert value) st -(** [betree_main::betree::{betree_main::betree::BeTree#6}::delete]: +(** [betree::betree::{betree::betree::BeTree#6}::delete]: Source: 'src/betree.rs', lines 880:4-880:38 *) let betree_BeTree_delete (self : betree_BeTree_t) (key : u64) (st : state) : @@ -648,7 +648,7 @@ let betree_BeTree_delete = betree_BeTree_apply self key Betree_Message_Delete st -(** [betree_main::betree::{betree_main::betree::BeTree#6}::upsert]: +(** [betree::betree::{betree::betree::BeTree#6}::upsert]: Source: 'src/betree.rs', lines 886:4-886:59 *) let betree_BeTree_upsert (self : betree_BeTree_t) (key : u64) (upd : betree_UpsertFunState_t) @@ -657,7 +657,7 @@ let betree_BeTree_upsert = betree_BeTree_apply self key (Betree_Message_Upsert upd) st -(** [betree_main::betree::{betree_main::betree::BeTree#6}::lookup]: +(** [betree::betree::{betree::betree::BeTree#6}::lookup]: Source: 'src/betree.rs', lines 895:4-895:62 *) let betree_BeTree_lookup (self : betree_BeTree_t) (key : u64) (st : state) : @@ -666,11 +666,11 @@ let betree_BeTree_lookup let* (st1, (o, n)) = betree_Node_lookup self.root key st in Ok (st1, (o, { self with root = n })) -(** [betree_main::main]: +(** [betree::main]: Source: 'src/main.rs', lines 4:0-4:9 *) let main : result unit = Ok () -(** Unit test for [betree_main::main] *) +(** Unit test for [betree::main] *) let _ = assert_norm (main = Ok ()) |