summaryrefslogtreecommitdiff
path: root/tests/fstar/betree
diff options
context:
space:
mode:
Diffstat (limited to 'tests/fstar/betree')
-rw-r--r--tests/fstar/betree/Betree.Clauses.Template.fst65
-rw-r--r--tests/fstar/betree/Betree.Clauses.fst40
-rw-r--r--tests/fstar/betree/Betree.Funs.fst319
3 files changed, 280 insertions, 144 deletions
diff --git a/tests/fstar/betree/Betree.Clauses.Template.fst b/tests/fstar/betree/Betree.Clauses.Template.fst
index fad8c5ba..d3e07c7e 100644
--- a/tests/fstar/betree/Betree.Clauses.Template.fst
+++ b/tests/fstar/betree/Betree.Clauses.Template.fst
@@ -7,100 +7,109 @@ open Betree.Types
#set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
(** [betree::betree::{betree::betree::List<T>#1}::len]: decreases clause
- Source: 'src/betree.rs', lines 276:4-276:24 *)
+ Source: 'src/betree.rs', lines 276:4-284:5 *)
unfold
-let betree_List_len_decreases (t : Type0) (self : betree_List_t t) : nat =
+let betree_List_len_loop_decreases (t : Type0) (self : betree_List_t t)
+ (len : u64) : nat =
+ admit ()
+
+(** [betree::betree::{betree::betree::List<T>#1}::reverse]: decreases clause
+ Source: 'src/betree.rs', lines 304:4-312:5 *)
+unfold
+let betree_List_reverse_loop_decreases (t : Type0) (self : betree_List_t t)
+ (out : betree_List_t t) : nat =
admit ()
(** [betree::betree::{betree::betree::List<T>#1}::split_at]: decreases clause
- Source: 'src/betree.rs', lines 284:4-284:51 *)
+ Source: 'src/betree.rs', lines 287:4-302:5 *)
unfold
-let betree_List_split_at_decreases (t : Type0) (self : betree_List_t t)
- (n : u64) : nat =
+let betree_List_split_at_loop_decreases (t : Type0) (n : u64)
+ (beg : betree_List_t t) (self : betree_List_t t) : nat =
admit ()
(** [betree::betree::{betree::betree::List<(u64, T)>#2}::partition_at_pivot]: decreases clause
- Source: 'src/betree.rs', lines 339:4-339:73 *)
+ Source: 'src/betree.rs', lines 355:4-370:5 *)
unfold
-let betree_ListPairU64T_partition_at_pivot_decreases (t : Type0)
- (self : betree_List_t (u64 & t)) (pivot : u64) : nat =
+let betree_ListPairU64T_partition_at_pivot_loop_decreases (t : Type0)
+ (pivot : u64) (beg : betree_List_t (u64 & t))
+ (end1 : betree_List_t (u64 & t)) (self : betree_List_t (u64 & t)) : nat =
admit ()
(** [betree::betree::{betree::betree::Node#5}::lookup_first_message_for_key]: decreases clause
- Source: 'src/betree.rs', lines 789:4-792:34 *)
+ Source: 'src/betree.rs', lines 792:4-810:5 *)
unfold
-let betree_Node_lookup_first_message_for_key_decreases (key : u64)
+let betree_Node_lookup_first_message_for_key_loop_decreases (key : u64)
(msgs : betree_List_t (u64 & betree_Message_t)) : nat =
admit ()
(** [betree::betree::{betree::betree::Node#5}::lookup_in_bindings]: decreases clause
- Source: 'src/betree.rs', lines 636:4-636:80 *)
+ Source: 'src/betree.rs', lines 649:4-660:5 *)
unfold
-let betree_Node_lookup_in_bindings_decreases (key : u64)
+let betree_Node_lookup_in_bindings_loop_decreases (key : u64)
(bindings : betree_List_t (u64 & u64)) : nat =
admit ()
(** [betree::betree::{betree::betree::Node#5}::apply_upserts]: decreases clause
- Source: 'src/betree.rs', lines 819:4-819:90 *)
+ Source: 'src/betree.rs', lines 820:4-844:5 *)
unfold
-let betree_Node_apply_upserts_decreases
+let betree_Node_apply_upserts_loop_decreases
(msgs : betree_List_t (u64 & betree_Message_t)) (prev : option u64)
(key : u64) : nat =
admit ()
(** [betree::betree::{betree::betree::Internal#4}::lookup_in_children]: decreases clause
- Source: 'src/betree.rs', lines 395:4-395:63 *)
+ Source: 'src/betree.rs', lines 414:4-414:63 *)
unfold
let betree_Internal_lookup_in_children_decreases (self : betree_Internal_t)
(key : u64) (st : state) : nat =
admit ()
(** [betree::betree::{betree::betree::Node#5}::lookup]: decreases clause
- Source: 'src/betree.rs', lines 709:4-709:58 *)
+ Source: 'src/betree.rs', lines 712:4-712:58 *)
unfold
let betree_Node_lookup_decreases (self : betree_Node_t) (key : u64)
(st : state) : nat =
admit ()
(** [betree::betree::{betree::betree::Node#5}::filter_messages_for_key]: decreases clause
- Source: 'src/betree.rs', lines 674:4-674:77 *)
+ Source: 'src/betree.rs', lines 683:4-692:5 *)
unfold
-let betree_Node_filter_messages_for_key_decreases (key : u64)
+let betree_Node_filter_messages_for_key_loop_decreases (key : u64)
(msgs : betree_List_t (u64 & betree_Message_t)) : nat =
admit ()
(** [betree::betree::{betree::betree::Node#5}::lookup_first_message_after_key]: decreases clause
- Source: 'src/betree.rs', lines 689:4-692:34 *)
+ Source: 'src/betree.rs', lines 694:4-706:5 *)
unfold
-let betree_Node_lookup_first_message_after_key_decreases (key : u64)
+let betree_Node_lookup_first_message_after_key_loop_decreases (key : u64)
(msgs : betree_List_t (u64 & betree_Message_t)) : nat =
admit ()
(** [betree::betree::{betree::betree::Node#5}::apply_messages_to_internal]: decreases clause
- Source: 'src/betree.rs', lines 502:4-505:5 *)
+ Source: 'src/betree.rs', lines 518:4-526:5 *)
unfold
-let betree_Node_apply_messages_to_internal_decreases
+let betree_Node_apply_messages_to_internal_loop_decreases
(msgs : betree_List_t (u64 & betree_Message_t))
(new_msgs : betree_List_t (u64 & betree_Message_t)) : nat =
admit ()
(** [betree::betree::{betree::betree::Node#5}::lookup_mut_in_bindings]: decreases clause
- Source: 'src/betree.rs', lines 653:4-656:32 *)
+ Source: 'src/betree.rs', lines 664:4-677:5 *)
unfold
-let betree_Node_lookup_mut_in_bindings_decreases (key : u64)
+let betree_Node_lookup_mut_in_bindings_loop_decreases (key : u64)
(bindings : betree_List_t (u64 & u64)) : nat =
admit ()
(** [betree::betree::{betree::betree::Node#5}::apply_messages_to_leaf]: decreases clause
- Source: 'src/betree.rs', lines 444:4-447:5 *)
+ Source: 'src/betree.rs', lines 463:4-471:5 *)
unfold
-let betree_Node_apply_messages_to_leaf_decreases
+let betree_Node_apply_messages_to_leaf_loop_decreases
(bindings : betree_List_t (u64 & u64))
(new_msgs : betree_List_t (u64 & betree_Message_t)) : nat =
admit ()
(** [betree::betree::{betree::betree::Internal#4}::flush]: decreases clause
- Source: 'src/betree.rs', lines 410:4-415:26 *)
+ Source: 'src/betree.rs', lines 429:4-434:26 *)
unfold
let betree_Internal_flush_decreases (self : betree_Internal_t)
(params : betree_Params_t) (node_id_cnt : betree_NodeIdCounter_t)
@@ -108,7 +117,7 @@ let betree_Internal_flush_decreases (self : betree_Internal_t)
admit ()
(** [betree::betree::{betree::betree::Node#5}::apply_messages]: decreases clause
- Source: 'src/betree.rs', lines 588:4-593:5 *)
+ Source: 'src/betree.rs', lines 601:4-606: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/Betree.Clauses.fst b/tests/fstar/betree/Betree.Clauses.fst
index ae201cee..c50bf421 100644
--- a/tests/fstar/betree/Betree.Clauses.fst
+++ b/tests/fstar/betree/Betree.Clauses.fst
@@ -103,36 +103,46 @@ let wf_nat_pair_lem (p0 p1 : nat_pair) :
(** [betree_main::betree::List::{1}::len]: decreases clause *)
unfold
-let betree_List_len_decreases (t : Type0) (self : betree_List_t t) : betree_List_t t =
+let betree_List_len_loop_decreases (t : Type0) (self : betree_List_t t) (len : u64) : betree_List_t t =
self
-(** [betree_main::betree::List::{1}::split_at]: decreases clause *)
+(** [betree::betree::{betree::betree::List<T>#1}::reverse]: decreases clause
+ Source: 'src/betree.rs', lines 304:4-312:5 *)
unfold
-let betree_List_split_at_decreases (t : Type0) (self : betree_List_t t)
- (n : u64) : nat =
+let betree_List_reverse_loop_decreases (t : Type0) (self : betree_List_t t)
+ (out : betree_List_t t) =
+ self
+
+(** [betree::betree::{betree::betree::List<T>#1}::split_at]: decreases clause
+ Source: 'src/betree.rs', lines 287:4-302:5 *)
+unfold
+let betree_List_split_at_loop_decreases (t : Type0) (n : u64)
+ (beg : betree_List_t t) (self : betree_List_t t) : nat =
n
-(** [betree_main::betree::List::{2}::partition_at_pivot]: decreases clause *)
+(** [betree::betree::{betree::betree::List<(u64, T)>#2}::partition_at_pivot]: decreases clause
+ Source: 'src/betree.rs', lines 355:4-370:5 *)
unfold
-let betree_ListPairU64T_partition_at_pivot_decreases (t : Type0)
- (self : betree_List_t (u64 & t)) (pivot : u64) : betree_List_t (u64 & t) =
+let betree_ListPairU64T_partition_at_pivot_loop_decreases (t : Type0)
+ (pivot : u64) (beg : betree_List_t (u64 & t)) (end0 : betree_List_t (u64 & t))
+ (self : betree_List_t (u64 & t)) =
self
(** [betree_main::betree::Node::{5}::lookup_in_bindings]: decreases clause *)
unfold
-let betree_Node_lookup_in_bindings_decreases (key : u64)
+let betree_Node_lookup_in_bindings_loop_decreases (key : u64)
(bindings : betree_List_t (u64 & u64)) : betree_List_t (u64 & u64) =
bindings
(** [betree_main::betree::Node::{5}::lookup_first_message_for_key]: decreases clause *)
unfold
-let betree_Node_lookup_first_message_for_key_decreases (key : u64)
+let betree_Node_lookup_first_message_for_key_loop_decreases (key : u64)
(msgs : betree_List_t (u64 & betree_Message_t)) : betree_List_t (u64 & betree_Message_t) =
msgs
(** [betree_main::betree::Node::{5}::apply_upserts]: decreases clause *)
unfold
-let betree_Node_apply_upserts_decreases
+let betree_Node_apply_upserts_loop_decreases
(msgs : betree_List_t (u64 & betree_Message_t)) (prev : option u64)
(key : u64) : betree_List_t (u64 & betree_Message_t) =
msgs
@@ -151,29 +161,29 @@ let betree_Node_lookup_decreases (self : betree_Node_t) (key : u64)
(** [betree_main::betree::Node::{5}::lookup_mut_in_bindings]: decreases clause *)
unfold
-let betree_Node_lookup_mut_in_bindings_decreases (key : u64)
+let betree_Node_lookup_mut_in_bindings_loop_decreases (key : u64)
(bindings : betree_List_t (u64 & u64)) : betree_List_t (u64 & u64) =
bindings
unfold
-let betree_Node_apply_messages_to_leaf_decreases
+let betree_Node_apply_messages_to_leaf_loop_decreases
(bindings : betree_List_t (u64 & u64))
(new_msgs : betree_List_t (u64 & betree_Message_t)) : betree_List_t (u64 & betree_Message_t) =
new_msgs
(** [betree_main::betree::Node::{5}::filter_messages_for_key]: decreases clause *)
unfold
-let betree_Node_filter_messages_for_key_decreases (key : u64)
+let betree_Node_filter_messages_for_key_loop_decreases (key : u64)
(msgs : betree_List_t (u64 & betree_Message_t)) : betree_List_t (u64 & betree_Message_t) =
msgs
(** [betree_main::betree::Node::{5}::lookup_first_message_after_key]: decreases clause *)
unfold
-let betree_Node_lookup_first_message_after_key_decreases (key : u64)
+let betree_Node_lookup_first_message_after_key_loop_decreases (key : u64)
(msgs : betree_List_t (u64 & betree_Message_t)) : betree_List_t (u64 & betree_Message_t) =
msgs
-let betree_Node_apply_messages_to_internal_decreases
+let betree_Node_apply_messages_to_internal_loop_decreases
(msgs : betree_List_t (u64 & betree_Message_t))
(new_msgs : betree_List_t (u64 & betree_Message_t)) : betree_List_t (u64 & betree_Message_t) =
new_msgs
diff --git a/tests/fstar/betree/Betree.Funs.fst b/tests/fstar/betree/Betree.Funs.fst
index 07f561f5..de3ac13c 100644
--- a/tests/fstar/betree/Betree.Funs.fst
+++ b/tests/fstar/betree/Betree.Funs.fst
@@ -75,45 +75,76 @@ let betree_upsert_update
end
end
+(** [betree::betree::{betree::betree::List<T>#1}::len]: loop 0:
+ Source: 'src/betree.rs', lines 276:4-284:5 *)
+let rec betree_List_len_loop
+ (t : Type0) (self : betree_List_t t) (len : u64) :
+ Tot (result u64) (decreases (betree_List_len_loop_decreases t self len))
+ =
+ begin match self with
+ | Betree_List_Cons _ tl ->
+ let* len1 = u64_add len 1 in betree_List_len_loop t tl len1
+ | Betree_List_Nil -> Ok len
+ end
+
(** [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) :
- Tot (result u64) (decreases (betree_List_len_decreases t self))
+let betree_List_len (t : Type0) (self : betree_List_t t) : result u64 =
+ betree_List_len_loop t self 0
+
+(** [betree::betree::{betree::betree::List<T>#1}::reverse]: loop 0:
+ Source: 'src/betree.rs', lines 304:4-312:5 *)
+let rec betree_List_reverse_loop
+ (t : Type0) (self : betree_List_t t) (out : betree_List_t t) :
+ Tot (result (betree_List_t t))
+ (decreases (betree_List_reverse_loop_decreases t self out))
=
begin match self with
- | Betree_List_Cons _ tl -> let* i = betree_List_len t tl in u64_add 1 i
- | Betree_List_Nil -> Ok 0
+ | Betree_List_Cons hd tl ->
+ betree_List_reverse_loop t tl (Betree_List_Cons hd out)
+ | Betree_List_Nil -> Ok out
end
-(** [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) :
+(** [betree::betree::{betree::betree::List<T>#1}::reverse]:
+ Source: 'src/betree.rs', lines 304:4-304:32 *)
+let betree_List_reverse
+ (t : Type0) (self : betree_List_t t) : result (betree_List_t t) =
+ betree_List_reverse_loop t self Betree_List_Nil
+
+(** [betree::betree::{betree::betree::List<T>#1}::split_at]: loop 0:
+ Source: 'src/betree.rs', lines 287:4-302:5 *)
+let rec betree_List_split_at_loop
+ (t : Type0) (n : u64) (beg : betree_List_t t) (self : betree_List_t t) :
Tot (result ((betree_List_t t) & (betree_List_t t)))
- (decreases (betree_List_split_at_decreases t self n))
+ (decreases (betree_List_split_at_loop_decreases t n beg self))
=
- if n = 0
- then Ok (Betree_List_Nil, self)
- else
+ if n > 0
+ then
begin match self with
| Betree_List_Cons hd tl ->
- let* i = u64_sub n 1 in
- let* p = betree_List_split_at t tl i in
- let (ls0, ls1) = p in
- Ok (Betree_List_Cons hd ls0, ls1)
+ let* n1 = u64_sub n 1 in
+ betree_List_split_at_loop t n1 (Betree_List_Cons hd beg) tl
| Betree_List_Nil -> Fail Failure
end
+ else let* l = betree_List_reverse t beg in Ok (l, self)
+
+(** [betree::betree::{betree::betree::List<T>#1}::split_at]:
+ Source: 'src/betree.rs', lines 287:4-287:55 *)
+let betree_List_split_at
+ (t : Type0) (self : betree_List_t t) (n : u64) :
+ result ((betree_List_t t) & (betree_List_t t))
+ =
+ betree_List_split_at_loop t n Betree_List_Nil self
(** [betree::betree::{betree::betree::List<T>#1}::push_front]:
- Source: 'src/betree.rs', lines 299:4-299:34 *)
+ Source: 'src/betree.rs', lines 315:4-315: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::betree::{betree::betree::List<T>#1}::pop_front]:
- Source: 'src/betree.rs', lines 306:4-306:32 *)
+ Source: 'src/betree.rs', lines 322:4-322:32 *)
let betree_List_pop_front
(t : Type0) (self : betree_List_t t) : result (t & (betree_List_t t)) =
let (ls, _) = core_mem_replace (betree_List_t t) self Betree_List_Nil in
@@ -123,7 +154,7 @@ let betree_List_pop_front
end
(** [betree::betree::{betree::betree::List<T>#1}::hd]:
- Source: 'src/betree.rs', lines 318:4-318:22 *)
+ Source: 'src/betree.rs', lines 334:4-334:22 *)
let betree_List_hd (t : Type0) (self : betree_List_t t) : result t =
begin match self with
| Betree_List_Cons hd _ -> Ok hd
@@ -131,7 +162,7 @@ let betree_List_hd (t : Type0) (self : betree_List_t t) : result t =
end
(** [betree::betree::{betree::betree::List<(u64, T)>#2}::head_has_key]:
- Source: 'src/betree.rs', lines 327:4-327:44 *)
+ Source: 'src/betree.rs', lines 343:4-343:44 *)
let betree_ListPairU64T_head_has_key
(t : Type0) (self : betree_List_t (u64 & t)) (key : u64) : result bool =
begin match self with
@@ -139,27 +170,43 @@ let betree_ListPairU64T_head_has_key
| Betree_List_Nil -> Ok false
end
-(** [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) :
+(** [betree::betree::{betree::betree::List<(u64, T)>#2}::partition_at_pivot]: loop 0:
+ Source: 'src/betree.rs', lines 355:4-370:5 *)
+let rec betree_ListPairU64T_partition_at_pivot_loop
+ (t : Type0) (pivot : u64) (beg : betree_List_t (u64 & t))
+ (end1 : betree_List_t (u64 & t)) (self : betree_List_t (u64 & t)) :
Tot (result ((betree_List_t (u64 & t)) & (betree_List_t (u64 & t))))
- (decreases (betree_ListPairU64T_partition_at_pivot_decreases t self pivot))
+ (decreases (
+ betree_ListPairU64T_partition_at_pivot_loop_decreases t pivot beg end1
+ self))
=
begin match self with
| Betree_List_Cons hd tl ->
let (i, x) = hd in
if i >= pivot
- then Ok (Betree_List_Nil, Betree_List_Cons (i, x) tl)
+ then
+ betree_ListPairU64T_partition_at_pivot_loop t pivot beg (Betree_List_Cons
+ (i, x) end1) tl
else
- let* p = betree_ListPairU64T_partition_at_pivot t tl pivot in
- let (ls0, ls1) = p in
- Ok (Betree_List_Cons (i, x) ls0, ls1)
- | Betree_List_Nil -> Ok (Betree_List_Nil, Betree_List_Nil)
+ betree_ListPairU64T_partition_at_pivot_loop t pivot (Betree_List_Cons (i,
+ x) beg) end1 tl
+ | Betree_List_Nil ->
+ let* l = betree_List_reverse (u64 & t) beg in
+ let* l1 = betree_List_reverse (u64 & t) end1 in
+ Ok (l, l1)
end
+(** [betree::betree::{betree::betree::List<(u64, T)>#2}::partition_at_pivot]:
+ Source: 'src/betree.rs', lines 355:4-355:73 *)
+let betree_ListPairU64T_partition_at_pivot
+ (t : Type0) (self : betree_List_t (u64 & t)) (pivot : u64) :
+ result ((betree_List_t (u64 & t)) & (betree_List_t (u64 & t)))
+ =
+ betree_ListPairU64T_partition_at_pivot_loop t pivot Betree_List_Nil
+ Betree_List_Nil self
+
(** [betree::betree::{betree::betree::Leaf#3}::split]:
- Source: 'src/betree.rs', lines 359:4-364:17 *)
+ Source: 'src/betree.rs', lines 378:4-383: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)
@@ -179,13 +226,14 @@ let betree_Leaf_split
Ok (st2, ({ id = self.id; pivot = pivot; left = n; right = n1 },
node_id_cnt2))
-(** [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
+(** [betree::betree::{betree::betree::Node#5}::lookup_first_message_for_key]: loop 0:
+ Source: 'src/betree.rs', lines 792:4-810:5 *)
+let rec betree_Node_lookup_first_message_for_key_loop
(key : u64) (msgs : betree_List_t (u64 & betree_Message_t)) :
Tot (result ((betree_List_t (u64 & betree_Message_t)) & (betree_List_t (u64 &
betree_Message_t) -> result (betree_List_t (u64 & betree_Message_t)))))
- (decreases (betree_Node_lookup_first_message_for_key_decreases key msgs))
+ (decreases (
+ betree_Node_lookup_first_message_for_key_loop_decreases key msgs))
=
begin match msgs with
| Betree_List_Cons x next_msgs ->
@@ -193,39 +241,55 @@ let rec betree_Node_lookup_first_message_for_key
if i >= key
then Ok (Betree_List_Cons (i, m) next_msgs, Ok)
else
- let* (l, lookup_first_message_for_key_back) =
- betree_Node_lookup_first_message_for_key key next_msgs in
- let back =
+ let* (l, back) =
+ betree_Node_lookup_first_message_for_key_loop key next_msgs in
+ let back1 =
fun ret ->
- let* next_msgs1 = lookup_first_message_for_key_back ret in
- Ok (Betree_List_Cons (i, m) next_msgs1) in
- Ok (l, back)
+ let* next_msgs1 = back ret in Ok (Betree_List_Cons (i, m) next_msgs1)
+ in
+ Ok (l, back1)
| Betree_List_Nil -> Ok (Betree_List_Nil, Ok)
end
-(** [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
+(** [betree::betree::{betree::betree::Node#5}::lookup_first_message_for_key]:
+ Source: 'src/betree.rs', lines 792:4-795:34 *)
+let betree_Node_lookup_first_message_for_key
+ (key : u64) (msgs : betree_List_t (u64 & betree_Message_t)) :
+ result ((betree_List_t (u64 & betree_Message_t)) & (betree_List_t (u64 &
+ betree_Message_t) -> result (betree_List_t (u64 & betree_Message_t))))
+ =
+ betree_Node_lookup_first_message_for_key_loop key msgs
+
+(** [betree::betree::{betree::betree::Node#5}::lookup_in_bindings]: loop 0:
+ Source: 'src/betree.rs', lines 649:4-660:5 *)
+let rec betree_Node_lookup_in_bindings_loop
(key : u64) (bindings : betree_List_t (u64 & u64)) :
Tot (result (option u64))
- (decreases (betree_Node_lookup_in_bindings_decreases key bindings))
+ (decreases (betree_Node_lookup_in_bindings_loop_decreases key bindings))
=
begin match bindings with
| Betree_List_Cons hd tl ->
let (i, i1) = hd in
if i = key
then Ok (Some i1)
- else if i > key then Ok None else betree_Node_lookup_in_bindings key tl
+ else
+ if i > key then Ok None else betree_Node_lookup_in_bindings_loop key tl
| Betree_List_Nil -> Ok None
end
-(** [betree::betree::{betree::betree::Node#5}::apply_upserts]:
- Source: 'src/betree.rs', lines 819:4-819:90 *)
-let rec betree_Node_apply_upserts
+(** [betree::betree::{betree::betree::Node#5}::lookup_in_bindings]:
+ Source: 'src/betree.rs', lines 649:4-649:84 *)
+let betree_Node_lookup_in_bindings
+ (key : u64) (bindings : betree_List_t (u64 & u64)) : result (option u64) =
+ betree_Node_lookup_in_bindings_loop key bindings
+
+(** [betree::betree::{betree::betree::Node#5}::apply_upserts]: loop 0:
+ Source: 'src/betree.rs', lines 820:4-844:5 *)
+let rec betree_Node_apply_upserts_loop
(msgs : betree_List_t (u64 & betree_Message_t)) (prev : option u64)
(key : u64) :
Tot (result (u64 & (betree_List_t (u64 & betree_Message_t))))
- (decreases (betree_Node_apply_upserts_decreases msgs prev key))
+ (decreases (betree_Node_apply_upserts_loop_decreases msgs prev key))
=
let* b = betree_ListPairU64T_head_has_key betree_Message_t msgs key in
if b
@@ -237,7 +301,7 @@ let rec betree_Node_apply_upserts
| Betree_Message_Delete -> Fail Failure
| Betree_Message_Upsert s ->
let* v = betree_upsert_update prev s in
- betree_Node_apply_upserts msgs1 (Some v) key
+ betree_Node_apply_upserts_loop msgs1 (Some v) key
end
else
let* v = core_option_Option_unwrap u64 prev in
@@ -246,8 +310,17 @@ let rec betree_Node_apply_upserts
Betree_Message_Insert v) in
Ok (v, msgs1)
+(** [betree::betree::{betree::betree::Node#5}::apply_upserts]:
+ Source: 'src/betree.rs', lines 820:4-820:94 *)
+let betree_Node_apply_upserts
+ (msgs : betree_List_t (u64 & betree_Message_t)) (prev : option u64)
+ (key : u64) :
+ result (u64 & (betree_List_t (u64 & betree_Message_t)))
+ =
+ betree_Node_apply_upserts_loop msgs prev key
+
(** [betree::betree::{betree::betree::Internal#4}::lookup_in_children]:
- Source: 'src/betree.rs', lines 395:4-395:63 *)
+ Source: 'src/betree.rs', lines 414:4-414:63 *)
let rec betree_Internal_lookup_in_children
(self : betree_Internal_t) (key : u64) (st : state) :
Tot (result (state & ((option u64) & betree_Internal_t)))
@@ -262,7 +335,7 @@ let rec betree_Internal_lookup_in_children
Ok (st1, (o, { self with right = n }))
(** [betree::betree::{betree::betree::Node#5}::lookup]:
- Source: 'src/betree.rs', lines 709:4-709:58 *)
+ Source: 'src/betree.rs', lines 712:4-712:58 *)
and betree_Node_lookup
(self : betree_Node_t) (key : u64) (st : state) :
Tot (result (state & ((option u64) & betree_Node_t)))
@@ -317,12 +390,12 @@ and betree_Node_lookup
Ok (st1, (o, Betree_Node_Leaf node))
end
-(** [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
+(** [betree::betree::{betree::betree::Node#5}::filter_messages_for_key]: loop 0:
+ Source: 'src/betree.rs', lines 683:4-692:5 *)
+let rec betree_Node_filter_messages_for_key_loop
(key : u64) (msgs : betree_List_t (u64 & betree_Message_t)) :
Tot (result (betree_List_t (u64 & betree_Message_t)))
- (decreases (betree_Node_filter_messages_for_key_decreases key msgs))
+ (decreases (betree_Node_filter_messages_for_key_loop_decreases key msgs))
=
begin match msgs with
| Betree_List_Cons p l ->
@@ -332,37 +405,55 @@ let rec betree_Node_filter_messages_for_key
let* (_, msgs1) =
betree_List_pop_front (u64 & betree_Message_t) (Betree_List_Cons (k, m)
l) in
- betree_Node_filter_messages_for_key key msgs1
+ betree_Node_filter_messages_for_key_loop key msgs1
else Ok (Betree_List_Cons (k, m) l)
| Betree_List_Nil -> Ok Betree_List_Nil
end
-(** [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
+(** [betree::betree::{betree::betree::Node#5}::filter_messages_for_key]:
+ Source: 'src/betree.rs', lines 683:4-683:77 *)
+let betree_Node_filter_messages_for_key
+ (key : u64) (msgs : betree_List_t (u64 & betree_Message_t)) :
+ result (betree_List_t (u64 & betree_Message_t))
+ =
+ betree_Node_filter_messages_for_key_loop key msgs
+
+(** [betree::betree::{betree::betree::Node#5}::lookup_first_message_after_key]: loop 0:
+ Source: 'src/betree.rs', lines 694:4-706:5 *)
+let rec betree_Node_lookup_first_message_after_key_loop
(key : u64) (msgs : betree_List_t (u64 & betree_Message_t)) :
Tot (result ((betree_List_t (u64 & betree_Message_t)) & (betree_List_t (u64 &
betree_Message_t) -> result (betree_List_t (u64 & betree_Message_t)))))
- (decreases (betree_Node_lookup_first_message_after_key_decreases key msgs))
+ (decreases (
+ betree_Node_lookup_first_message_after_key_loop_decreases key msgs))
=
begin match msgs with
| Betree_List_Cons p next_msgs ->
let (k, m) = p in
if k = key
then
- let* (l, lookup_first_message_after_key_back) =
- betree_Node_lookup_first_message_after_key key next_msgs in
- let back =
+ let* (l, back) =
+ betree_Node_lookup_first_message_after_key_loop key next_msgs in
+ let back1 =
fun ret ->
- let* next_msgs1 = lookup_first_message_after_key_back ret in
- Ok (Betree_List_Cons (k, m) next_msgs1) in
- Ok (l, back)
+ let* next_msgs1 = back ret in Ok (Betree_List_Cons (k, m) next_msgs1)
+ in
+ Ok (l, back1)
else Ok (Betree_List_Cons (k, m) next_msgs, Ok)
| Betree_List_Nil -> Ok (Betree_List_Nil, Ok)
end
+(** [betree::betree::{betree::betree::Node#5}::lookup_first_message_after_key]:
+ Source: 'src/betree.rs', lines 694:4-697:34 *)
+let betree_Node_lookup_first_message_after_key
+ (key : u64) (msgs : betree_List_t (u64 & betree_Message_t)) :
+ result ((betree_List_t (u64 & betree_Message_t)) & (betree_List_t (u64 &
+ betree_Message_t) -> result (betree_List_t (u64 & betree_Message_t))))
+ =
+ betree_Node_lookup_first_message_after_key_loop key msgs
+
(** [betree::betree::{betree::betree::Node#5}::apply_to_internal]:
- Source: 'src/betree.rs', lines 521:4-521:89 *)
+ Source: 'src/betree.rs', lines 534:4-534:89 *)
let betree_Node_apply_to_internal
(msgs : betree_List_t (u64 & betree_Message_t)) (key : u64)
(new_msg : betree_Message_t) :
@@ -421,29 +512,39 @@ 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::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
+(** [betree::betree::{betree::betree::Node#5}::apply_messages_to_internal]: loop 0:
+ Source: 'src/betree.rs', lines 518:4-526:5 *)
+let rec betree_Node_apply_messages_to_internal_loop
(msgs : betree_List_t (u64 & betree_Message_t))
(new_msgs : betree_List_t (u64 & betree_Message_t)) :
Tot (result (betree_List_t (u64 & betree_Message_t)))
- (decreases (betree_Node_apply_messages_to_internal_decreases msgs new_msgs))
+ (decreases (
+ betree_Node_apply_messages_to_internal_loop_decreases msgs new_msgs))
=
begin match new_msgs with
| Betree_List_Cons new_msg new_msgs_tl ->
let (i, m) = new_msg in
let* msgs1 = betree_Node_apply_to_internal msgs i m in
- betree_Node_apply_messages_to_internal msgs1 new_msgs_tl
+ betree_Node_apply_messages_to_internal_loop msgs1 new_msgs_tl
| Betree_List_Nil -> Ok msgs
end
-(** [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
+(** [betree::betree::{betree::betree::Node#5}::apply_messages_to_internal]:
+ Source: 'src/betree.rs', lines 518:4-521:5 *)
+let betree_Node_apply_messages_to_internal
+ (msgs : betree_List_t (u64 & betree_Message_t))
+ (new_msgs : betree_List_t (u64 & betree_Message_t)) :
+ result (betree_List_t (u64 & betree_Message_t))
+ =
+ betree_Node_apply_messages_to_internal_loop msgs new_msgs
+
+(** [betree::betree::{betree::betree::Node#5}::lookup_mut_in_bindings]: loop 0:
+ Source: 'src/betree.rs', lines 664:4-677:5 *)
+let rec betree_Node_lookup_mut_in_bindings_loop
(key : u64) (bindings : betree_List_t (u64 & u64)) :
Tot (result ((betree_List_t (u64 & u64)) & (betree_List_t (u64 & u64) ->
result (betree_List_t (u64 & u64)))))
- (decreases (betree_Node_lookup_mut_in_bindings_decreases key bindings))
+ (decreases (betree_Node_lookup_mut_in_bindings_loop_decreases key bindings))
=
begin match bindings with
| Betree_List_Cons hd tl ->
@@ -451,18 +552,24 @@ let rec betree_Node_lookup_mut_in_bindings
if i >= key
then Ok (Betree_List_Cons (i, i1) tl, Ok)
else
- let* (l, lookup_mut_in_bindings_back) =
- betree_Node_lookup_mut_in_bindings key tl in
- let back =
- fun ret ->
- let* tl1 = lookup_mut_in_bindings_back ret in
- Ok (Betree_List_Cons (i, i1) tl1) in
- Ok (l, back)
+ let* (l, back) = betree_Node_lookup_mut_in_bindings_loop key tl in
+ let back1 =
+ fun ret -> let* tl1 = back ret in Ok (Betree_List_Cons (i, i1) tl1) in
+ Ok (l, back1)
| Betree_List_Nil -> Ok (Betree_List_Nil, Ok)
end
+(** [betree::betree::{betree::betree::Node#5}::lookup_mut_in_bindings]:
+ Source: 'src/betree.rs', lines 664:4-667:32 *)
+let betree_Node_lookup_mut_in_bindings
+ (key : u64) (bindings : betree_List_t (u64 & u64)) :
+ result ((betree_List_t (u64 & u64)) & (betree_List_t (u64 & u64) -> result
+ (betree_List_t (u64 & u64))))
+ =
+ betree_Node_lookup_mut_in_bindings_loop key bindings
+
(** [betree::betree::{betree::betree::Node#5}::apply_to_leaf]:
- Source: 'src/betree.rs', lines 460:4-460:87 *)
+ Source: 'src/betree.rs', lines 476:4-476:87 *)
let betree_Node_apply_to_leaf
(bindings : betree_List_t (u64 & u64)) (key : u64)
(new_msg : betree_Message_t) :
@@ -497,24 +604,34 @@ let betree_Node_apply_to_leaf
lookup_mut_in_bindings_back bindings2
end
-(** [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
+(** [betree::betree::{betree::betree::Node#5}::apply_messages_to_leaf]: loop 0:
+ Source: 'src/betree.rs', lines 463:4-471:5 *)
+let rec betree_Node_apply_messages_to_leaf_loop
(bindings : betree_List_t (u64 & u64))
(new_msgs : betree_List_t (u64 & betree_Message_t)) :
Tot (result (betree_List_t (u64 & u64)))
- (decreases (betree_Node_apply_messages_to_leaf_decreases bindings new_msgs))
+ (decreases (
+ betree_Node_apply_messages_to_leaf_loop_decreases bindings new_msgs))
=
begin match new_msgs with
| Betree_List_Cons new_msg new_msgs_tl ->
let (i, m) = new_msg in
let* bindings1 = betree_Node_apply_to_leaf bindings i m in
- betree_Node_apply_messages_to_leaf bindings1 new_msgs_tl
+ betree_Node_apply_messages_to_leaf_loop bindings1 new_msgs_tl
| Betree_List_Nil -> Ok bindings
end
+(** [betree::betree::{betree::betree::Node#5}::apply_messages_to_leaf]:
+ Source: 'src/betree.rs', lines 463:4-466:5 *)
+let betree_Node_apply_messages_to_leaf
+ (bindings : betree_List_t (u64 & u64))
+ (new_msgs : betree_List_t (u64 & betree_Message_t)) :
+ result (betree_List_t (u64 & u64))
+ =
+ betree_Node_apply_messages_to_leaf_loop bindings new_msgs
+
(** [betree::betree::{betree::betree::Internal#4}::flush]:
- Source: 'src/betree.rs', lines 410:4-415:26 *)
+ Source: 'src/betree.rs', lines 429:4-434:26 *)
let rec betree_Internal_flush
(self : betree_Internal_t) (params : betree_Params_t)
(node_id_cnt : betree_NodeIdCounter_t)
@@ -551,7 +668,7 @@ let rec betree_Internal_flush
Ok (st1, (msgs_left, ({ self with right = n }, node_id_cnt1)))
(** [betree::betree::{betree::betree::Node#5}::apply_messages]:
- Source: 'src/betree.rs', lines 588:4-593:5 *)
+ Source: 'src/betree.rs', lines 601:4-606:5 *)
and betree_Node_apply_messages
(self : betree_Node_t) (params : betree_Params_t)
(node_id_cnt : betree_NodeIdCounter_t)
@@ -592,7 +709,7 @@ and betree_Node_apply_messages
end
(** [betree::betree::{betree::betree::Node#5}::apply]:
- Source: 'src/betree.rs', lines 576:4-582:5 *)
+ Source: 'src/betree.rs', lines 589:4-595:5 *)
let betree_Node_apply
(self : betree_Node_t) (params : betree_Params_t)
(node_id_cnt : betree_NodeIdCounter_t) (key : u64)
@@ -606,7 +723,7 @@ let betree_Node_apply
Ok (st1, (self1, node_id_cnt1))
(** [betree::betree::{betree::betree::BeTree#6}::new]:
- Source: 'src/betree.rs', lines 849:4-849:60 *)
+ Source: 'src/betree.rs', lines 848:4-848:60 *)
let betree_BeTree_new
(min_flush_size : u64) (split_size : u64) (st : state) :
result (state & betree_BeTree_t)
@@ -622,7 +739,7 @@ let betree_BeTree_new
})
(** [betree::betree::{betree::betree::BeTree#6}::apply]:
- Source: 'src/betree.rs', lines 868:4-868:47 *)
+ Source: 'src/betree.rs', lines 867:4-867:47 *)
let betree_BeTree_apply
(self : betree_BeTree_t) (key : u64) (msg : betree_Message_t) (st : state) :
result (state & betree_BeTree_t)
@@ -633,7 +750,7 @@ let betree_BeTree_apply
Ok (st1, { self with node_id_cnt = nic; root = n })
(** [betree::betree::{betree::betree::BeTree#6}::insert]:
- Source: 'src/betree.rs', lines 874:4-874:52 *)
+ Source: 'src/betree.rs', lines 873:4-873:52 *)
let betree_BeTree_insert
(self : betree_BeTree_t) (key : u64) (value : u64) (st : state) :
result (state & betree_BeTree_t)
@@ -641,7 +758,7 @@ let betree_BeTree_insert
betree_BeTree_apply self key (Betree_Message_Insert value) st
(** [betree::betree::{betree::betree::BeTree#6}::delete]:
- Source: 'src/betree.rs', lines 880:4-880:38 *)
+ Source: 'src/betree.rs', lines 879:4-879:38 *)
let betree_BeTree_delete
(self : betree_BeTree_t) (key : u64) (st : state) :
result (state & betree_BeTree_t)
@@ -649,7 +766,7 @@ let betree_BeTree_delete
betree_BeTree_apply self key Betree_Message_Delete st
(** [betree::betree::{betree::betree::BeTree#6}::upsert]:
- Source: 'src/betree.rs', lines 886:4-886:59 *)
+ Source: 'src/betree.rs', lines 885:4-885:59 *)
let betree_BeTree_upsert
(self : betree_BeTree_t) (key : u64) (upd : betree_UpsertFunState_t)
(st : state) :
@@ -658,7 +775,7 @@ let betree_BeTree_upsert
betree_BeTree_apply self key (Betree_Message_Upsert upd) st
(** [betree::betree::{betree::betree::BeTree#6}::lookup]:
- Source: 'src/betree.rs', lines 895:4-895:62 *)
+ Source: 'src/betree.rs', lines 894:4-894:62 *)
let betree_BeTree_lookup
(self : betree_BeTree_t) (key : u64) (st : state) :
result (state & ((option u64) & betree_BeTree_t))
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-23 01:46:26 +0000