summaryrefslogtreecommitdiff
path: root/tests/betree
diff options
context:
space:
mode:
Diffstat (limited to 'tests/betree')
-rw-r--r--tests/betree/BetreeMain.Clauses.Template.fst28
-rw-r--r--tests/betree/BetreeMain.Funs.fst356
-rw-r--r--tests/betree/BetreeMain.Types.fsti16
-rw-r--r--tests/betree/Primitives.fst3
4 files changed, 209 insertions, 194 deletions
diff --git a/tests/betree/BetreeMain.Clauses.Template.fst b/tests/betree/BetreeMain.Clauses.Template.fst
index eb26276c..c2412775 100644
--- a/tests/betree/BetreeMain.Clauses.Template.fst
+++ b/tests/betree/BetreeMain.Clauses.Template.fst
@@ -6,6 +6,10 @@ open BetreeMain.Types
#set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
+(** [core::num::u64::{9}::MAX] *)
+let core_num_u64_max_body : result u64 = Return 18446744073709551615
+let core_num_u64_max_c : u64 = eval_global core_num_u64_max_body
+
(** [betree_main::betree::List::{1}::len]: decreases clause *)
unfold
let betree_list_len_decreases (t : Type0) (self : betree_list_t t) : nat =
@@ -42,18 +46,18 @@ let betree_node_apply_upserts_decreases
(key : u64) (st : state) : nat =
admit ()
-(** [betree_main::betree::Internal::{4}::lookup_in_children]: decreases clause *)
-unfold
-let betree_internal_lookup_in_children_decreases (self : betree_internal_t)
- (key : u64) (st : state) : nat =
- admit ()
-
(** [betree_main::betree::Node::{5}::lookup]: decreases clause *)
unfold
let betree_node_lookup_decreases (self : betree_node_t) (key : u64)
(st : state) : nat =
admit ()
+(** [betree_main::betree::Internal::{4}::lookup_in_children]: decreases clause *)
+unfold
+let betree_internal_lookup_in_children_decreases (self : betree_internal_t)
+ (key : u64) (st : state) : nat =
+ admit ()
+
(** [betree_main::betree::Node::{5}::lookup_mut_in_bindings]: decreases clause *)
unfold
let betree_node_lookup_mut_in_bindings_decreases (key : u64)
@@ -86,17 +90,17 @@ let betree_node_apply_messages_to_internal_decreases
(new_msgs : betree_list_t (u64 & betree_message_t)) : nat =
admit ()
-(** [betree_main::betree::Internal::{4}::flush]: decreases clause *)
+(** [betree_main::betree::Node::{5}::apply_messages]: decreases clause *)
unfold
-let betree_internal_flush_decreases (self : betree_internal_t)
+let betree_node_apply_messages_decreases (self : betree_node_t)
(params : betree_params_t) (node_id_cnt : betree_node_id_counter_t)
- (content : betree_list_t (u64 & betree_message_t)) (st : state) : nat =
+ (msgs : betree_list_t (u64 & betree_message_t)) (st : state) : nat =
admit ()
-(** [betree_main::betree::Node::{5}::apply_messages]: decreases clause *)
+(** [betree_main::betree::Internal::{4}::flush]: decreases clause *)
unfold
-let betree_node_apply_messages_decreases (self : betree_node_t)
+let betree_internal_flush_decreases (self : betree_internal_t)
(params : betree_params_t) (node_id_cnt : betree_node_id_counter_t)
- (msgs : betree_list_t (u64 & betree_message_t)) (st : state) : nat =
+ (content : betree_list_t (u64 & betree_message_t)) (st : state) : nat =
admit ()
diff --git a/tests/betree/BetreeMain.Funs.fst b/tests/betree/BetreeMain.Funs.fst
index 9b960ce5..e80e96a6 100644
--- a/tests/betree/BetreeMain.Funs.fst
+++ b/tests/betree/BetreeMain.Funs.fst
@@ -80,6 +80,10 @@ let betree_node_id_counter_fresh_id_back
| Return i -> Return (Mkbetree_node_id_counter_t i)
end
+(** [core::num::u64::{9}::MAX] *)
+let core_num_u64_max_body : result u64 = Return 18446744073709551615
+let core_num_u64_max_c : u64 = eval_global core_num_u64_max_body
+
(** [betree_main::betree::upsert_update] *)
let betree_upsert_update_fwd
(prev : option u64) (st : betree_upsert_fun_state_t) : result u64 =
@@ -92,7 +96,7 @@ let betree_upsert_update_fwd
| Some prev0 ->
begin match st with
| BetreeUpsertFunStateAdd v ->
- begin match u64_sub 18446744073709551615 prev0 with
+ begin match u64_sub core_num_u64_max_c prev0 with
| Fail -> Fail
| Return margin ->
if margin >= v
@@ -101,7 +105,7 @@ let betree_upsert_update_fwd
| Fail -> Fail
| Return i -> Return i
end
- else Return 18446744073709551615
+ else Return core_num_u64_max_c
end
| BetreeUpsertFunStateSub v ->
if prev0 >= v
@@ -468,48 +472,8 @@ let rec betree_node_apply_upserts_back
end
end
-(** [betree_main::betree::Internal::{4}::lookup_in_children] *)
-let rec betree_internal_lookup_in_children_fwd
- (self : betree_internal_t) (key : u64) (st : state) :
- Tot (result (state & (option u64)))
- (decreases (betree_internal_lookup_in_children_decreases self key st))
- =
- if key < self.betree_internal_pivot
- then
- begin match betree_node_lookup_fwd self.betree_internal_left key st with
- | Fail -> Fail
- | Return (st0, opt) -> Return (st0, opt)
- end
- else
- begin match betree_node_lookup_fwd self.betree_internal_right key st with
- | Fail -> Fail
- | Return (st0, opt) -> Return (st0, opt)
- end
-
-(** [betree_main::betree::Internal::{4}::lookup_in_children] *)
-and betree_internal_lookup_in_children_back
- (self : betree_internal_t) (key : u64) (st : state) :
- Tot (result betree_internal_t)
- (decreases (betree_internal_lookup_in_children_decreases self key st))
- =
- if key < self.betree_internal_pivot
- then
- begin match betree_node_lookup_back self.betree_internal_left key st with
- | Fail -> Fail
- | Return n ->
- Return (Mkbetree_internal_t self.betree_internal_id
- self.betree_internal_pivot n self.betree_internal_right)
- end
- else
- begin match betree_node_lookup_back self.betree_internal_right key st with
- | Fail -> Fail
- | Return n ->
- Return (Mkbetree_internal_t self.betree_internal_id
- self.betree_internal_pivot self.betree_internal_left n)
- end
-
(** [betree_main::betree::Node::{5}::lookup] *)
-and betree_node_lookup_fwd
+let rec betree_node_lookup_fwd
(self : betree_node_t) (key : u64) (st : state) :
Tot (result (state & (option u64)))
(decreases (betree_node_lookup_decreases self key st))
@@ -723,6 +687,46 @@ and betree_node_lookup_back
end
end
+(** [betree_main::betree::Internal::{4}::lookup_in_children] *)
+and betree_internal_lookup_in_children_fwd
+ (self : betree_internal_t) (key : u64) (st : state) :
+ Tot (result (state & (option u64)))
+ (decreases (betree_internal_lookup_in_children_decreases self key st))
+ =
+ if key < self.betree_internal_pivot
+ then
+ begin match betree_node_lookup_fwd self.betree_internal_left key st with
+ | Fail -> Fail
+ | Return (st0, opt) -> Return (st0, opt)
+ end
+ else
+ begin match betree_node_lookup_fwd self.betree_internal_right key st with
+ | Fail -> Fail
+ | Return (st0, opt) -> Return (st0, opt)
+ end
+
+(** [betree_main::betree::Internal::{4}::lookup_in_children] *)
+and betree_internal_lookup_in_children_back
+ (self : betree_internal_t) (key : u64) (st : state) :
+ Tot (result betree_internal_t)
+ (decreases (betree_internal_lookup_in_children_decreases self key st))
+ =
+ if key < self.betree_internal_pivot
+ then
+ begin match betree_node_lookup_back self.betree_internal_left key st with
+ | Fail -> Fail
+ | Return n ->
+ Return (Mkbetree_internal_t self.betree_internal_id
+ self.betree_internal_pivot n self.betree_internal_right)
+ end
+ else
+ begin match betree_node_lookup_back self.betree_internal_right key st with
+ | Fail -> Fail
+ | Return n ->
+ Return (Mkbetree_internal_t self.betree_internal_id
+ self.betree_internal_pivot self.betree_internal_left n)
+ end
+
(** [betree_main::betree::Node::{5}::lookup_mut_in_bindings] *)
let rec betree_node_lookup_mut_in_bindings_fwd
(key : u64) (bindings : betree_list_t (u64 & u64)) :
@@ -1128,140 +1132,8 @@ let rec betree_node_apply_messages_to_internal_fwd_back
| BetreeListNil -> Return msgs
end
-(** [betree_main::betree::Internal::{4}::flush] *)
-let rec betree_internal_flush_fwd
- (self : betree_internal_t) (params : betree_params_t)
- (node_id_cnt : betree_node_id_counter_t)
- (content : betree_list_t (u64 & betree_message_t)) (st : state) :
- Tot (result (state & (betree_list_t (u64 & betree_message_t))))
- (decreases (betree_internal_flush_decreases self params node_id_cnt content
- st))
- =
- begin match
- betree_list_partition_at_pivot_fwd betree_message_t content
- self.betree_internal_pivot with
- | Fail -> Fail
- | Return p ->
- let (msgs_left, msgs_right) = p in
- begin match betree_list_len_fwd (u64 & betree_message_t) msgs_left with
- | Fail -> Fail
- | Return len_left ->
- if len_left >= params.betree_params_min_flush_size
- then
- begin match
- betree_node_apply_messages_fwd self.betree_internal_left params
- node_id_cnt msgs_left st with
- | Fail -> Fail
- | Return (st0, _) ->
- begin match
- betree_node_apply_messages_back self.betree_internal_left params
- node_id_cnt msgs_left st with
- | Fail -> Fail
- | Return (_, node_id_cnt0) ->
- begin match betree_list_len_fwd (u64 & betree_message_t) msgs_right
- with
- | Fail -> Fail
- | Return len_right ->
- if len_right >= params.betree_params_min_flush_size
- then
- begin match
- betree_node_apply_messages_fwd self.betree_internal_right
- params node_id_cnt0 msgs_right st0 with
- | Fail -> Fail
- | Return (st1, _) ->
- begin match
- betree_node_apply_messages_back self.betree_internal_right
- params node_id_cnt0 msgs_right st0 with
- | Fail -> Fail
- | Return (_, _) -> Return (st1, BetreeListNil)
- end
- end
- else Return (st0, msgs_right)
- end
- end
- end
- else
- begin match
- betree_node_apply_messages_fwd self.betree_internal_right params
- node_id_cnt msgs_right st with
- | Fail -> Fail
- | Return (st0, _) ->
- begin match
- betree_node_apply_messages_back self.betree_internal_right params
- node_id_cnt msgs_right st with
- | Fail -> Fail
- | Return (_, _) -> Return (st0, msgs_left)
- end
- end
- end
- end
-
-(** [betree_main::betree::Internal::{4}::flush] *)
-and betree_internal_flush_back
- (self : betree_internal_t) (params : betree_params_t)
- (node_id_cnt : betree_node_id_counter_t)
- (content : betree_list_t (u64 & betree_message_t)) (st : state) :
- Tot (result (betree_internal_t & betree_node_id_counter_t))
- (decreases (betree_internal_flush_decreases self params node_id_cnt content
- st))
- =
- begin match
- betree_list_partition_at_pivot_fwd betree_message_t content
- self.betree_internal_pivot with
- | Fail -> Fail
- | Return p ->
- let (msgs_left, msgs_right) = p in
- begin match betree_list_len_fwd (u64 & betree_message_t) msgs_left with
- | Fail -> Fail
- | Return len_left ->
- if len_left >= params.betree_params_min_flush_size
- then
- begin match
- betree_node_apply_messages_fwd self.betree_internal_left params
- node_id_cnt msgs_left st with
- | Fail -> Fail
- | Return (st0, _) ->
- begin match
- betree_node_apply_messages_back self.betree_internal_left params
- node_id_cnt msgs_left st with
- | Fail -> Fail
- | Return (n, node_id_cnt0) ->
- begin match betree_list_len_fwd (u64 & betree_message_t) msgs_right
- with
- | Fail -> Fail
- | Return len_right ->
- if len_right >= params.betree_params_min_flush_size
- then
- begin match
- betree_node_apply_messages_back self.betree_internal_right
- params node_id_cnt0 msgs_right st0 with
- | Fail -> Fail
- | Return (n0, node_id_cnt1) ->
- Return (Mkbetree_internal_t self.betree_internal_id
- self.betree_internal_pivot n n0, node_id_cnt1)
- end
- else
- Return (Mkbetree_internal_t self.betree_internal_id
- self.betree_internal_pivot n self.betree_internal_right,
- node_id_cnt0)
- end
- end
- end
- else
- begin match
- betree_node_apply_messages_back self.betree_internal_right params
- node_id_cnt msgs_right st with
- | Fail -> Fail
- | Return (n, node_id_cnt0) ->
- Return (Mkbetree_internal_t self.betree_internal_id
- self.betree_internal_pivot self.betree_internal_left n,
- node_id_cnt0)
- end
- end
- end
-
(** [betree_main::betree::Node::{5}::apply_messages] *)
-and betree_node_apply_messages_fwd
+let rec betree_node_apply_messages_fwd
(self : betree_node_t) (params : betree_params_t)
(node_id_cnt : betree_node_id_counter_t)
(msgs : betree_list_t (u64 & betree_message_t)) (st : state) :
@@ -1450,6 +1322,138 @@ and betree_node_apply_messages_back
end
end
+(** [betree_main::betree::Internal::{4}::flush] *)
+and betree_internal_flush_fwd
+ (self : betree_internal_t) (params : betree_params_t)
+ (node_id_cnt : betree_node_id_counter_t)
+ (content : betree_list_t (u64 & betree_message_t)) (st : state) :
+ Tot (result (state & (betree_list_t (u64 & betree_message_t))))
+ (decreases (betree_internal_flush_decreases self params node_id_cnt content
+ st))
+ =
+ begin match
+ betree_list_partition_at_pivot_fwd betree_message_t content
+ self.betree_internal_pivot with
+ | Fail -> Fail
+ | Return p ->
+ let (msgs_left, msgs_right) = p in
+ begin match betree_list_len_fwd (u64 & betree_message_t) msgs_left with
+ | Fail -> Fail
+ | Return len_left ->
+ if len_left >= params.betree_params_min_flush_size
+ then
+ begin match
+ betree_node_apply_messages_fwd self.betree_internal_left params
+ node_id_cnt msgs_left st with
+ | Fail -> Fail
+ | Return (st0, _) ->
+ begin match
+ betree_node_apply_messages_back self.betree_internal_left params
+ node_id_cnt msgs_left st with
+ | Fail -> Fail
+ | Return (_, node_id_cnt0) ->
+ begin match betree_list_len_fwd (u64 & betree_message_t) msgs_right
+ with
+ | Fail -> Fail
+ | Return len_right ->
+ if len_right >= params.betree_params_min_flush_size
+ then
+ begin match
+ betree_node_apply_messages_fwd self.betree_internal_right
+ params node_id_cnt0 msgs_right st0 with
+ | Fail -> Fail
+ | Return (st1, _) ->
+ begin match
+ betree_node_apply_messages_back self.betree_internal_right
+ params node_id_cnt0 msgs_right st0 with
+ | Fail -> Fail
+ | Return (_, _) -> Return (st1, BetreeListNil)
+ end
+ end
+ else Return (st0, msgs_right)
+ end
+ end
+ end
+ else
+ begin match
+ betree_node_apply_messages_fwd self.betree_internal_right params
+ node_id_cnt msgs_right st with
+ | Fail -> Fail
+ | Return (st0, _) ->
+ begin match
+ betree_node_apply_messages_back self.betree_internal_right params
+ node_id_cnt msgs_right st with
+ | Fail -> Fail
+ | Return (_, _) -> Return (st0, msgs_left)
+ end
+ end
+ end
+ end
+
+(** [betree_main::betree::Internal::{4}::flush] *)
+and betree_internal_flush_back
+ (self : betree_internal_t) (params : betree_params_t)
+ (node_id_cnt : betree_node_id_counter_t)
+ (content : betree_list_t (u64 & betree_message_t)) (st : state) :
+ Tot (result (betree_internal_t & betree_node_id_counter_t))
+ (decreases (betree_internal_flush_decreases self params node_id_cnt content
+ st))
+ =
+ begin match
+ betree_list_partition_at_pivot_fwd betree_message_t content
+ self.betree_internal_pivot with
+ | Fail -> Fail
+ | Return p ->
+ let (msgs_left, msgs_right) = p in
+ begin match betree_list_len_fwd (u64 & betree_message_t) msgs_left with
+ | Fail -> Fail
+ | Return len_left ->
+ if len_left >= params.betree_params_min_flush_size
+ then
+ begin match
+ betree_node_apply_messages_fwd self.betree_internal_left params
+ node_id_cnt msgs_left st with
+ | Fail -> Fail
+ | Return (st0, _) ->
+ begin match
+ betree_node_apply_messages_back self.betree_internal_left params
+ node_id_cnt msgs_left st with
+ | Fail -> Fail
+ | Return (n, node_id_cnt0) ->
+ begin match betree_list_len_fwd (u64 & betree_message_t) msgs_right
+ with
+ | Fail -> Fail
+ | Return len_right ->
+ if len_right >= params.betree_params_min_flush_size
+ then
+ begin match
+ betree_node_apply_messages_back self.betree_internal_right
+ params node_id_cnt0 msgs_right st0 with
+ | Fail -> Fail
+ | Return (n0, node_id_cnt1) ->
+ Return (Mkbetree_internal_t self.betree_internal_id
+ self.betree_internal_pivot n n0, node_id_cnt1)
+ end
+ else
+ Return (Mkbetree_internal_t self.betree_internal_id
+ self.betree_internal_pivot n self.betree_internal_right,
+ node_id_cnt0)
+ end
+ end
+ end
+ else
+ begin match
+ betree_node_apply_messages_back self.betree_internal_right params
+ node_id_cnt msgs_right st with
+ | Fail -> Fail
+ | Return (n, node_id_cnt0) ->
+ Return (Mkbetree_internal_t self.betree_internal_id
+ self.betree_internal_pivot self.betree_internal_left n,
+ node_id_cnt0)
+ end
+ end
+ end
+
(** [betree_main::betree::Node::{5}::apply] *)
let betree_node_apply_fwd
(self : betree_node_t) (params : betree_params_t)
diff --git a/tests/betree/BetreeMain.Types.fsti b/tests/betree/BetreeMain.Types.fsti
index a937c726..f0ca1d9e 100644
--- a/tests/betree/BetreeMain.Types.fsti
+++ b/tests/betree/BetreeMain.Types.fsti
@@ -24,8 +24,13 @@ type betree_message_t =
(** [betree_main::betree::Leaf] *)
type betree_leaf_t = { betree_leaf_id : u64; betree_leaf_size : u64; }
+(** [betree_main::betree::Node] *)
+type betree_node_t =
+| BetreeNodeInternal : betree_internal_t -> betree_node_t
+| BetreeNodeLeaf : betree_leaf_t -> betree_node_t
+
(** [betree_main::betree::Internal] *)
-type betree_internal_t =
+and betree_internal_t =
{
betree_internal_id : u64;
betree_internal_pivot : u64;
@@ -33,11 +38,6 @@ type betree_internal_t =
betree_internal_right : betree_node_t;
}
-(** [betree_main::betree::Node] *)
-and betree_node_t =
-| BetreeNodeInternal : betree_internal_t -> betree_node_t
-| BetreeNodeLeaf : betree_leaf_t -> betree_node_t
-
(** [betree_main::betree::Params] *)
type betree_params_t =
{
@@ -55,6 +55,10 @@ type betree_be_tree_t =
betree_be_tree_root : betree_node_t;
}
+(** [core::num::u64::{9}::MAX] *)
+let core_num_u64_max_body : result u64 = Return 18446744073709551615
+let core_num_u64_max_c : u64 = eval_global core_num_u64_max_body
+
(** The state type used in the state-error monad *)
val state : Type0
diff --git a/tests/betree/Primitives.fst b/tests/betree/Primitives.fst
index fe351f3a..b44fe9d1 100644
--- a/tests/betree/Primitives.fst
+++ b/tests/betree/Primitives.fst
@@ -34,6 +34,9 @@ let bind (#a #b : Type0) (m : result a) (f : a -> result b) : result b =
// Monadic assert(...)
let massert (b:bool) : result unit = if b then Return () else Fail
+// Normalize and unwrap a successful result (used for globals).
+let eval_global (#a : Type0) (x : result a{Return? (normalize_term x)}) : a = Return?.v x
+
(*** Misc *)
type char = FStar.Char.char
type string = string