summaryrefslogtreecommitdiff
path: root/tests/fstar/betree
diff options
context:
space:
mode:
Diffstat (limited to 'tests/fstar/betree')
-rw-r--r--tests/fstar/betree/BetreeMain.Clauses.Template.fst14
-rw-r--r--tests/fstar/betree/BetreeMain.Funs.fst32
2 files changed, 23 insertions, 23 deletions
diff --git a/tests/fstar/betree/BetreeMain.Clauses.Template.fst b/tests/fstar/betree/BetreeMain.Clauses.Template.fst
index 4ae29302..537705c5 100644
--- a/tests/fstar/betree/BetreeMain.Clauses.Template.fst
+++ b/tests/fstar/betree/BetreeMain.Clauses.Template.fst
@@ -33,6 +33,13 @@ let betree_Node_lookup_first_message_for_key_decreases (key : u64)
(msgs : betree_List_t (u64 & betree_Message_t)) : nat =
admit ()
+(** [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::{betree_main::betree::Node#5}::apply_upserts]: decreases clause
Source: 'src/betree.rs', lines 819:4-819:90 *)
unfold
@@ -41,13 +48,6 @@ let betree_Node_apply_upserts_decreases
(key : u64) (st : state) : nat =
admit ()
-(** [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::{betree_main::betree::Internal#4}::lookup_in_children]: decreases clause
Source: 'src/betree.rs', lines 395:4-395:63 *)
unfold
diff --git a/tests/fstar/betree/BetreeMain.Funs.fst b/tests/fstar/betree/BetreeMain.Funs.fst
index fef8a8e1..f844b0ec 100644
--- a/tests/fstar/betree/BetreeMain.Funs.fst
+++ b/tests/fstar/betree/BetreeMain.Funs.fst
@@ -258,6 +258,22 @@ let rec betree_Node_lookup_first_message_for_key_back
| Betree_List_Nil -> Return ret
end
+(** [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))
+ (decreases (betree_Node_lookup_in_bindings_decreases key bindings))
+ =
+ begin match bindings with
+ | Betree_List_Cons hd tl ->
+ let (i, i0) = hd in
+ if i = key
+ then Return (Some i0)
+ else if i > key then Return None else betree_Node_lookup_in_bindings key tl
+ | Betree_List_Nil -> Return None
+ end
+
(** [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
@@ -312,22 +328,6 @@ let rec betree_Node_apply_upserts_back
betree_List_push_front (u64 & betree_Message_t) msgs (key,
Betree_Message_Insert v)
-(** [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))
- (decreases (betree_Node_lookup_in_bindings_decreases key bindings))
- =
- begin match bindings with
- | Betree_List_Cons hd tl ->
- let (i, i0) = hd in
- if i = key
- then Return (Some i0)
- else if i > key then Return None else betree_Node_lookup_in_bindings key tl
- | Betree_List_Nil -> Return None
- end
-
(** [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