diff options
Diffstat (limited to 'tests/fstar/betree/Betree.Clauses.fst')
| -rw-r--r-- | tests/fstar/betree/Betree.Clauses.fst | 40 |
1 files changed, 25 insertions, 15 deletions
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 |