diff options
Diffstat (limited to 'tests')
27 files changed, 1042 insertions, 456 deletions
diff --git a/tests/coq/betree/Betree_Funs.v b/tests/coq/betree/Betree_Funs.v index b965d423..1c6092ba 100644 --- a/tests/coq/betree/Betree_Funs.v +++ b/tests/coq/betree/Betree_Funs.v @@ -88,45 +88,85 @@ Definition betree_upsert_update end . +(** [betree::betree::{betree::betree::List<T>#1}::len]: loop 0: + Source: 'src/betree.rs', lines 276:4-284:5 *) +Fixpoint betree_List_len_loop + (T : Type) (n : nat) (self : betree_List_t T) (len : u64) : result u64 := + match n with + | O => Fail_ OutOfFuel + | S n1 => + match self with + | Betree_List_Cons _ tl => + len1 <- u64_add len 1%u64; betree_List_len_loop T n1 tl len1 + | Betree_List_Nil => Ok len + end + end +. + (** [betree::betree::{betree::betree::List<T>#1}::len]: Source: 'src/betree.rs', lines 276:4-276:24 *) -Fixpoint betree_List_len +Definition betree_List_len (T : Type) (n : nat) (self : betree_List_t T) : result u64 := + betree_List_len_loop T n self 0%u64 +. + +(** [betree::betree::{betree::betree::List<T>#1}::reverse]: loop 0: + Source: 'src/betree.rs', lines 304:4-312:5 *) +Fixpoint betree_List_reverse_loop + (T : Type) (n : nat) (self : betree_List_t T) (out : betree_List_t T) : + result (betree_List_t T) + := match n with | O => Fail_ OutOfFuel | S n1 => match self with - | Betree_List_Cons _ tl => i <- betree_List_len T n1 tl; u64_add 1%u64 i - | Betree_List_Nil => Ok 0%u64 + | Betree_List_Cons hd tl => + betree_List_reverse_loop T n1 tl (Betree_List_Cons hd out) + | Betree_List_Nil => Ok out end end . -(** [betree::betree::{betree::betree::List<T>#1}::split_at]: - Source: 'src/betree.rs', lines 284:4-284:51 *) -Fixpoint betree_List_split_at - (T : Type) (n : nat) (self : betree_List_t T) (n1 : u64) : +(** [betree::betree::{betree::betree::List<T>#1}::reverse]: + Source: 'src/betree.rs', lines 304:4-304:32 *) +Definition betree_List_reverse + (T : Type) (n : nat) (self : betree_List_t T) : result (betree_List_t T) := + betree_List_reverse_loop T n self Betree_List_Nil +. + +(** [betree::betree::{betree::betree::List<T>#1}::split_at]: loop 0: + Source: 'src/betree.rs', lines 287:4-302:5 *) +Fixpoint betree_List_split_at_loop + (T : Type) (n : nat) (n1 : u64) (beg : betree_List_t T) + (self : betree_List_t T) : result ((betree_List_t T) * (betree_List_t T)) := match n with | O => Fail_ OutOfFuel | S n2 => - if n1 s= 0%u64 - then Ok (Betree_List_Nil, self) - else + if n1 s> 0%u64 + then match self with | Betree_List_Cons hd tl => - i <- u64_sub n1 1%u64; - p <- betree_List_split_at T n2 tl i; - let (ls0, ls1) := p in - Ok (Betree_List_Cons hd ls0, ls1) + n3 <- u64_sub n1 1%u64; + betree_List_split_at_loop T n2 n3 (Betree_List_Cons hd beg) tl | Betree_List_Nil => Fail_ Failure end + else (l <- betree_List_reverse T n2 beg; Ok (l, self)) end . +(** [betree::betree::{betree::betree::List<T>#1}::split_at]: + Source: 'src/betree.rs', lines 287:4-287:55 *) +Definition betree_List_split_at + (T : Type) (n : nat) (self : betree_List_t T) (n1 : u64) : + result ((betree_List_t T) * (betree_List_t T)) + := + betree_List_split_at_loop T n n1 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 *) Definition betree_List_push_front (T : Type) (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 @@ -134,7 +174,7 @@ Definition betree_List_push_front . (** [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 *) Definition betree_List_pop_front (T : Type) (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 @@ -145,7 +185,7 @@ Definition betree_List_pop_front . (** [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 *) Definition betree_List_hd (T : Type) (self : betree_List_t T) : result T := match self with | Betree_List_Cons hd _ => Ok hd @@ -154,7 +194,7 @@ Definition betree_List_hd (T : Type) (self : betree_List_t T) : result T := . (** [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 *) Definition betree_ListPairU64T_head_has_key (T : Type) (self : betree_List_t (u64 * T)) (key : u64) : result bool := match self with @@ -163,10 +203,11 @@ Definition betree_ListPairU64T_head_has_key end . -(** [betree::betree::{betree::betree::List<(u64, T)>#2}::partition_at_pivot]: - Source: 'src/betree.rs', lines 339:4-339:73 *) -Fixpoint betree_ListPairU64T_partition_at_pivot - (T : Type) (n : nat) (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 *) +Fixpoint betree_ListPairU64T_partition_at_pivot_loop + (T : Type) (n : nat) (pivot : u64) (beg : betree_List_t (u64 * T)) + (end1 : betree_List_t (u64 * T)) (self : betree_List_t (u64 * T)) : result ((betree_List_t (u64 * T)) * (betree_List_t (u64 * T))) := match n with @@ -176,18 +217,32 @@ Fixpoint betree_ListPairU64T_partition_at_pivot | Betree_List_Cons hd tl => let (i, t) := hd in if i s>= pivot - then Ok (Betree_List_Nil, Betree_List_Cons (i, t) tl) - else ( - p <- betree_ListPairU64T_partition_at_pivot T n1 tl pivot; - let (ls0, ls1) := p in - Ok (Betree_List_Cons (i, t) ls0, ls1)) - | Betree_List_Nil => Ok (Betree_List_Nil, Betree_List_Nil) + then + betree_ListPairU64T_partition_at_pivot_loop T n1 pivot beg + (Betree_List_Cons (i, t) end1) tl + else + betree_ListPairU64T_partition_at_pivot_loop T n1 pivot + (Betree_List_Cons (i, t) beg) end1 tl + | Betree_List_Nil => + l <- betree_List_reverse (u64 * T) n1 beg; + l1 <- betree_List_reverse (u64 * T) n1 end1; + Ok (l, l1) end end . +(** [betree::betree::{betree::betree::List<(u64, T)>#2}::partition_at_pivot]: + Source: 'src/betree.rs', lines 355:4-355:73 *) +Definition betree_ListPairU64T_partition_at_pivot + (T : Type) (n : nat) (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 n 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 *) Definition betree_Leaf_split (n : nat) (self : betree_Leaf_t) (content : betree_List_t (u64 * u64)) (params : betree_Params_t) (node_id_cnt : betree_NodeIdCounter_t) @@ -222,9 +277,9 @@ Definition betree_Leaf_split node_id_cnt2)) . -(** [betree::betree::{betree::betree::Node#5}::lookup_first_message_for_key]: - Source: 'src/betree.rs', lines 789:4-792:34 *) -Fixpoint 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 *) +Fixpoint betree_Node_lookup_first_message_for_key_loop (n : nat) (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)))) @@ -238,21 +293,30 @@ Fixpoint betree_Node_lookup_first_message_for_key if i s>= key then Ok (Betree_List_Cons (i, m) next_msgs, Ok) else ( - p <- betree_Node_lookup_first_message_for_key n1 key next_msgs; - let (l, lookup_first_message_for_key_back) := p in - let back := + p <- betree_Node_lookup_first_message_for_key_loop n1 key next_msgs; + let (l, back) := p in + let back1 := fun (ret : betree_List_t (u64 * betree_Message_t)) => - next_msgs1 <- lookup_first_message_for_key_back ret; - Ok (Betree_List_Cons (i, m) next_msgs1) in - Ok (l, back)) + next_msgs1 <- back ret; Ok (Betree_List_Cons (i, m) next_msgs1) in + Ok (l, back1)) | Betree_List_Nil => Ok (Betree_List_Nil, Ok) end end . -(** [betree::betree::{betree::betree::Node#5}::lookup_in_bindings]: - Source: 'src/betree.rs', lines 636:4-636:80 *) -Fixpoint 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 *) +Definition betree_Node_lookup_first_message_for_key + (n : nat) (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 n key msgs +. + +(** [betree::betree::{betree::betree::Node#5}::lookup_in_bindings]: loop 0: + Source: 'src/betree.rs', lines 649:4-660:5 *) +Fixpoint betree_Node_lookup_in_bindings_loop (n : nat) (key : u64) (bindings : betree_List_t (u64 * u64)) : result (option u64) := @@ -265,15 +329,26 @@ Fixpoint betree_Node_lookup_in_bindings if i s= key then Ok (Some i1) else - if i s> key then Ok None else betree_Node_lookup_in_bindings n1 key tl + if i s> key + then Ok None + else betree_Node_lookup_in_bindings_loop n1 key tl | Betree_List_Nil => Ok None end end . -(** [betree::betree::{betree::betree::Node#5}::apply_upserts]: - Source: 'src/betree.rs', lines 819:4-819:90 *) -Fixpoint betree_Node_apply_upserts +(** [betree::betree::{betree::betree::Node#5}::lookup_in_bindings]: + Source: 'src/betree.rs', lines 649:4-649:84 *) +Definition betree_Node_lookup_in_bindings + (n : nat) (key : u64) (bindings : betree_List_t (u64 * u64)) : + result (option u64) + := + betree_Node_lookup_in_bindings_loop n key bindings +. + +(** [betree::betree::{betree::betree::Node#5}::apply_upserts]: loop 0: + Source: 'src/betree.rs', lines 820:4-844:5 *) +Fixpoint betree_Node_apply_upserts_loop (n : nat) (msgs : betree_List_t (u64 * betree_Message_t)) (prev : option u64) (key : u64) : result (u64 * (betree_List_t (u64 * betree_Message_t))) @@ -292,7 +367,7 @@ Fixpoint betree_Node_apply_upserts | Betree_Message_Delete => Fail_ Failure | Betree_Message_Upsert s => v <- betree_upsert_update prev s; - betree_Node_apply_upserts n1 msgs1 (Some v) key + betree_Node_apply_upserts_loop n1 msgs1 (Some v) key end) else ( v <- core_option_Option_unwrap u64 prev; @@ -303,8 +378,18 @@ Fixpoint betree_Node_apply_upserts end . +(** [betree::betree::{betree::betree::Node#5}::apply_upserts]: + Source: 'src/betree.rs', lines 820:4-820:94 *) +Definition betree_Node_apply_upserts + (n : nat) (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 n 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 *) Fixpoint betree_Internal_lookup_in_children (n : nat) (self : betree_Internal_t) (key : u64) (st : state) : result (state * ((option u64) * betree_Internal_t)) @@ -328,7 +413,7 @@ Fixpoint betree_Internal_lookup_in_children end (** [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 *) with betree_Node_lookup (n : nat) (self : betree_Node_t) (key : u64) (st : state) : result (state * ((option u64) * betree_Node_t)) @@ -394,9 +479,9 @@ with betree_Node_lookup end . -(** [betree::betree::{betree::betree::Node#5}::filter_messages_for_key]: - Source: 'src/betree.rs', lines 674:4-674:77 *) -Fixpoint 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 *) +Fixpoint betree_Node_filter_messages_for_key_loop (n : nat) (key : u64) (msgs : betree_List_t (u64 * betree_Message_t)) : result (betree_List_t (u64 * betree_Message_t)) := @@ -412,16 +497,25 @@ Fixpoint betree_Node_filter_messages_for_key betree_List_pop_front (u64 * betree_Message_t) (Betree_List_Cons (k, m) l); let (_, msgs1) := p1 in - betree_Node_filter_messages_for_key n1 key msgs1) + betree_Node_filter_messages_for_key_loop n1 key msgs1) else Ok (Betree_List_Cons (k, m) l) | Betree_List_Nil => Ok Betree_List_Nil end end . -(** [betree::betree::{betree::betree::Node#5}::lookup_first_message_after_key]: - Source: 'src/betree.rs', lines 689:4-692:34 *) -Fixpoint 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 *) +Definition betree_Node_filter_messages_for_key + (n : nat) (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 n key msgs +. + +(** [betree::betree::{betree::betree::Node#5}::lookup_first_message_after_key]: loop 0: + Source: 'src/betree.rs', lines 694:4-706:5 *) +Fixpoint betree_Node_lookup_first_message_after_key_loop (n : nat) (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)))) @@ -434,21 +528,30 @@ Fixpoint betree_Node_lookup_first_message_after_key let (k, m) := p in if k s= key then ( - p1 <- betree_Node_lookup_first_message_after_key n1 key next_msgs; - let (l, lookup_first_message_after_key_back) := p1 in - let back := + p1 <- betree_Node_lookup_first_message_after_key_loop n1 key next_msgs; + let (l, back) := p1 in + let back1 := fun (ret : betree_List_t (u64 * betree_Message_t)) => - next_msgs1 <- lookup_first_message_after_key_back ret; - Ok (Betree_List_Cons (k, m) next_msgs1) in - Ok (l, back)) + next_msgs1 <- back ret; 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 end . +(** [betree::betree::{betree::betree::Node#5}::lookup_first_message_after_key]: + Source: 'src/betree.rs', lines 694:4-697:34 *) +Definition betree_Node_lookup_first_message_after_key + (n : nat) (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 n 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 *) Definition betree_Node_apply_to_internal (n : nat) (msgs : betree_List_t (u64 * betree_Message_t)) (key : u64) (new_msg : betree_Message_t) : @@ -508,9 +611,9 @@ Definition betree_Node_apply_to_internal 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 *) -Fixpoint 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 *) +Fixpoint betree_Node_apply_messages_to_internal_loop (n : nat) (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)) @@ -522,15 +625,25 @@ Fixpoint betree_Node_apply_messages_to_internal | Betree_List_Cons new_msg new_msgs_tl => let (i, m) := new_msg in msgs1 <- betree_Node_apply_to_internal n1 msgs i m; - betree_Node_apply_messages_to_internal n1 msgs1 new_msgs_tl + betree_Node_apply_messages_to_internal_loop n1 msgs1 new_msgs_tl | Betree_List_Nil => Ok msgs end end . -(** [betree::betree::{betree::betree::Node#5}::lookup_mut_in_bindings]: - Source: 'src/betree.rs', lines 653:4-656:32 *) -Fixpoint 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 *) +Definition betree_Node_apply_messages_to_internal + (n : nat) (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 n msgs new_msgs +. + +(** [betree::betree::{betree::betree::Node#5}::lookup_mut_in_bindings]: loop 0: + Source: 'src/betree.rs', lines 664:4-677:5 *) +Fixpoint betree_Node_lookup_mut_in_bindings_loop (n : nat) (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)))) @@ -544,20 +657,29 @@ Fixpoint betree_Node_lookup_mut_in_bindings if i s>= key then Ok (Betree_List_Cons (i, i1) tl, Ok) else ( - p <- betree_Node_lookup_mut_in_bindings n1 key tl; - let (l, lookup_mut_in_bindings_back) := p in - let back := + p <- betree_Node_lookup_mut_in_bindings_loop n1 key tl; + let (l, back) := p in + let back1 := fun (ret : betree_List_t (u64 * u64)) => - tl1 <- lookup_mut_in_bindings_back ret; - Ok (Betree_List_Cons (i, i1) tl1) in - Ok (l, back)) + tl1 <- back ret; Ok (Betree_List_Cons (i, i1) tl1) in + Ok (l, back1)) | Betree_List_Nil => Ok (Betree_List_Nil, Ok) end end . +(** [betree::betree::{betree::betree::Node#5}::lookup_mut_in_bindings]: + Source: 'src/betree.rs', lines 664:4-667:32 *) +Definition betree_Node_lookup_mut_in_bindings + (n : nat) (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 n 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 *) Definition betree_Node_apply_to_leaf (n : nat) (bindings : betree_List_t (u64 * u64)) (key : u64) (new_msg : betree_Message_t) : @@ -594,9 +716,9 @@ Definition betree_Node_apply_to_leaf end . -(** [betree::betree::{betree::betree::Node#5}::apply_messages_to_leaf]: - Source: 'src/betree.rs', lines 444:4-447:5 *) -Fixpoint 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 *) +Fixpoint betree_Node_apply_messages_to_leaf_loop (n : nat) (bindings : betree_List_t (u64 * u64)) (new_msgs : betree_List_t (u64 * betree_Message_t)) : result (betree_List_t (u64 * u64)) @@ -608,14 +730,24 @@ Fixpoint betree_Node_apply_messages_to_leaf | Betree_List_Cons new_msg new_msgs_tl => let (i, m) := new_msg in bindings1 <- betree_Node_apply_to_leaf n1 bindings i m; - betree_Node_apply_messages_to_leaf n1 bindings1 new_msgs_tl + betree_Node_apply_messages_to_leaf_loop n1 bindings1 new_msgs_tl | Betree_List_Nil => Ok bindings end end . +(** [betree::betree::{betree::betree::Node#5}::apply_messages_to_leaf]: + Source: 'src/betree.rs', lines 463:4-466:5 *) +Definition betree_Node_apply_messages_to_leaf + (n : nat) (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 n 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 *) Fixpoint betree_Internal_flush (n : nat) (self : betree_Internal_t) (params : betree_Params_t) (node_id_cnt : betree_NodeIdCounter_t) @@ -665,7 +797,7 @@ Fixpoint betree_Internal_flush end (** [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 *) with betree_Node_apply_messages (n : nat) (self : betree_Node_t) (params : betree_Params_t) (node_id_cnt : betree_NodeIdCounter_t) @@ -721,7 +853,7 @@ with betree_Node_apply_messages . (** [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 *) Definition betree_Node_apply (n : nat) (self : betree_Node_t) (params : betree_Params_t) (node_id_cnt : betree_NodeIdCounter_t) (key : u64) @@ -737,7 +869,7 @@ Definition betree_Node_apply . (** [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 *) Definition betree_BeTree_new (min_flush_size : u64) (split_size : u64) (st : state) : result (state * betree_BeTree_t) @@ -762,7 +894,7 @@ Definition 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 *) Definition betree_BeTree_apply (n : nat) (self : betree_BeTree_t) (key : u64) (msg : betree_Message_t) (st : state) : @@ -782,7 +914,7 @@ Definition betree_BeTree_apply . (** [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 *) Definition betree_BeTree_insert (n : nat) (self : betree_BeTree_t) (key : u64) (value : u64) (st : state) : result (state * betree_BeTree_t) @@ -791,7 +923,7 @@ Definition betree_BeTree_insert . (** [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 *) Definition betree_BeTree_delete (n : nat) (self : betree_BeTree_t) (key : u64) (st : state) : result (state * betree_BeTree_t) @@ -800,7 +932,7 @@ Definition betree_BeTree_delete . (** [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 *) Definition betree_BeTree_upsert (n : nat) (self : betree_BeTree_t) (key : u64) (upd : betree_UpsertFunState_t) (st : state) : @@ -810,7 +942,7 @@ Definition betree_BeTree_upsert . (** [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 *) Definition betree_BeTree_lookup (n : nat) (self : betree_BeTree_t) (key : u64) (st : state) : result (state * ((option u64) * betree_BeTree_t)) 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)) diff --git a/tests/lean/Betree/Funs.lean b/tests/lean/Betree/Funs.lean index 8612ccbc..7d8b4714 100644 --- a/tests/lean/Betree/Funs.lean +++ b/tests/lean/Betree/Funs.lean @@ -79,42 +79,74 @@ def betree.upsert_update then prev1 - v else Result.ok 0#u64 +/- [betree::betree::{betree::betree::List<T>#1}::len]: loop 0: + Source: 'src/betree.rs', lines 276:4-284:5 -/ +divergent def betree.List.len_loop + (T : Type) (self : betree.List T) (len : U64) : Result U64 := + match self with + | betree.List.Cons _ tl => + do + let len1 ← len + 1#u64 + betree.List.len_loop T tl len1 + | betree.List.Nil => Result.ok len + /- [betree::betree::{betree::betree::List<T>#1}::len]: Source: 'src/betree.rs', lines 276:4-276:24 -/ -divergent def betree.List.len (T : Type) (self : betree.List T) : Result U64 := +def betree.List.len (T : Type) (self : betree.List T) : Result U64 := + betree.List.len_loop T self 0#u64 + +/- [betree::betree::{betree::betree::List<T>#1}::reverse]: loop 0: + Source: 'src/betree.rs', lines 304:4-312:5 -/ +divergent def betree.List.reverse_loop + (T : Type) (self : betree.List T) (out : betree.List T) : + Result (betree.List T) + := match self with - | betree.List.Cons _ tl => do - let i ← betree.List.len T tl - 1#u64 + i - | betree.List.Nil => Result.ok 0#u64 - -/- [betree::betree::{betree::betree::List<T>#1}::split_at]: - Source: 'src/betree.rs', lines 284:4-284:51 -/ -divergent def betree.List.split_at - (T : Type) (self : betree.List T) (n : U64) : + | betree.List.Cons hd tl => + betree.List.reverse_loop T tl (betree.List.Cons hd out) + | betree.List.Nil => Result.ok out + +/- [betree::betree::{betree::betree::List<T>#1}::reverse]: + Source: 'src/betree.rs', lines 304:4-304:32 -/ +def betree.List.reverse + (T : Type) (self : betree.List T) : Result (betree.List 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 -/ +divergent def betree.List.split_at_loop + (T : Type) (n : U64) (beg : betree.List T) (self : betree.List T) : Result ((betree.List T) × (betree.List T)) := - if n = 0#u64 - then Result.ok (betree.List.Nil, self) - else + if n > 0#u64 + then match self with | betree.List.Cons hd tl => do - let i ← n - 1#u64 - let p ← betree.List.split_at T tl i - let (ls0, ls1) := p - Result.ok (betree.List.Cons hd ls0, ls1) + let n1 ← n - 1#u64 + betree.List.split_at_loop T n1 (betree.List.Cons hd beg) tl | betree.List.Nil => Result.fail .panic + else do + let l ← betree.List.reverse T beg + Result.ok (l, self) + +/- [betree::betree::{betree::betree::List<T>#1}::split_at]: + Source: 'src/betree.rs', lines 287:4-287:55 -/ +def betree.List.split_at + (T : Type) (self : betree.List T) (n : U64) : + Result ((betree.List T) × (betree.List 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 -/ def betree.List.push_front (T : Type) (self : betree.List T) (x : T) : Result (betree.List T) := let (tl, _) := core.mem.replace (betree.List T) self betree.List.Nil Result.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 -/ def betree.List.pop_front (T : Type) (self : betree.List T) : Result (T × (betree.List T)) := let (ls, _) := core.mem.replace (betree.List T) self betree.List.Nil @@ -123,14 +155,14 @@ def betree.List.pop_front | betree.List.Nil => Result.fail .panic /- [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 -/ def betree.List.hd (T : Type) (self : betree.List T) : Result T := match self with | betree.List.Cons hd _ => Result.ok hd | betree.List.Nil => Result.fail .panic /- [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 -/ def betree.ListPairU64T.head_has_key (T : Type) (self : betree.List (U64 × T)) (key : U64) : Result Bool := match self with @@ -138,26 +170,40 @@ def betree.ListPairU64T.head_has_key Result.ok (i = key) | betree.List.Nil => Result.ok false -/- [betree::betree::{betree::betree::List<(u64, T)>#2}::partition_at_pivot]: - Source: 'src/betree.rs', lines 339:4-339:73 -/ -divergent def betree.ListPairU64T.partition_at_pivot - (T : Type) (self : betree.List (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 -/ +divergent def betree.ListPairU64T.partition_at_pivot_loop + (T : Type) (pivot : U64) (beg : betree.List (U64 × T)) + (end1 : betree.List (U64 × T)) (self : betree.List (U64 × T)) : Result ((betree.List (U64 × T)) × (betree.List (U64 × T))) := match self with | betree.List.Cons hd tl => let (i, t) := hd if i >= pivot - then Result.ok (betree.List.Nil, betree.List.Cons (i, t) tl) + then + betree.ListPairU64T.partition_at_pivot_loop T pivot beg (betree.List.Cons + (i, t) end1) tl else - do - let p ← betree.ListPairU64T.partition_at_pivot T tl pivot - let (ls0, ls1) := p - Result.ok (betree.List.Cons (i, t) ls0, ls1) - | betree.List.Nil => Result.ok (betree.List.Nil, betree.List.Nil) + betree.ListPairU64T.partition_at_pivot_loop T pivot (betree.List.Cons (i, + t) beg) end1 tl + | betree.List.Nil => + do + let l ← betree.List.reverse (U64 × T) beg + let l1 ← betree.List.reverse (U64 × T) end1 + Result.ok (l, l1) + +/- [betree::betree::{betree::betree::List<(u64, T)>#2}::partition_at_pivot]: + Source: 'src/betree.rs', lines 355:4-355:73 -/ +def betree.ListPairU64T.partition_at_pivot + (T : Type) (self : betree.List (U64 × T)) (pivot : U64) : + Result ((betree.List (U64 × T)) × (betree.List (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 -/ def betree.Leaf.split (self : betree.Leaf) (content : betree.List (U64 × U64)) (params : betree.Params) (node_id_cnt : betree.NodeIdCounter) (st : State) : @@ -176,9 +222,9 @@ def betree.Leaf.split let n1 := betree.Node.Leaf { id := id1, size := params.split_size } Result.ok (st2, (betree.Internal.mk self.id pivot n n1, node_id_cnt2)) -/- [betree::betree::{betree::betree::Node#5}::lookup_first_message_for_key]: - Source: 'src/betree.rs', lines 789:4-792:34 -/ -divergent def 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 -/ +divergent def betree.Node.lookup_first_message_for_key_loop (key : U64) (msgs : betree.List (U64 × betree.Message)) : Result ((betree.List (U64 × betree.Message)) × (betree.List (U64 × betree.Message) → Result (betree.List (U64 × betree.Message)))) @@ -190,19 +236,28 @@ divergent def betree.Node.lookup_first_message_for_key then Result.ok (betree.List.Cons (i, m) next_msgs, Result.ok) else do - let (l, lookup_first_message_for_key_back) ← - betree.Node.lookup_first_message_for_key key next_msgs - let back := + let (l, back) ← + betree.Node.lookup_first_message_for_key_loop key next_msgs + let back1 := fun ret => do - let next_msgs1 ← lookup_first_message_for_key_back ret + let next_msgs1 ← back ret Result.ok (betree.List.Cons (i, m) next_msgs1) - Result.ok (l, back) + Result.ok (l, back1) | betree.List.Nil => Result.ok (betree.List.Nil, Result.ok) -/- [betree::betree::{betree::betree::Node#5}::lookup_in_bindings]: - Source: 'src/betree.rs', lines 636:4-636:80 -/ -divergent def 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 -/ +def betree.Node.lookup_first_message_for_key + (key : U64) (msgs : betree.List (U64 × betree.Message)) : + Result ((betree.List (U64 × betree.Message)) × (betree.List (U64 × + betree.Message) → Result (betree.List (U64 × betree.Message)))) + := + 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 -/ +divergent def betree.Node.lookup_in_bindings_loop (key : U64) (bindings : betree.List (U64 × U64)) : Result (Option U64) := match bindings with | betree.List.Cons hd tl => @@ -212,12 +267,18 @@ divergent def betree.Node.lookup_in_bindings else if i > key then Result.ok none - else betree.Node.lookup_in_bindings key tl + else betree.Node.lookup_in_bindings_loop key tl | betree.List.Nil => Result.ok none -/- [betree::betree::{betree::betree::Node#5}::apply_upserts]: - Source: 'src/betree.rs', lines 819:4-819:90 -/ -divergent def betree.Node.apply_upserts +/- [betree::betree::{betree::betree::Node#5}::lookup_in_bindings]: + Source: 'src/betree.rs', lines 649:4-649:84 -/ +def betree.Node.lookup_in_bindings + (key : U64) (bindings : betree.List (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 -/ +divergent def betree.Node.apply_upserts_loop (msgs : betree.List (U64 × betree.Message)) (prev : Option U64) (key : U64) : Result (U64 × (betree.List (U64 × betree.Message))) @@ -235,7 +296,7 @@ divergent def betree.Node.apply_upserts | betree.Message.Upsert s => do let v ← betree.upsert_update prev s - betree.Node.apply_upserts msgs1 (some v) key + betree.Node.apply_upserts_loop msgs1 (some v) key else do let v ← core.option.Option.unwrap U64 prev @@ -244,8 +305,17 @@ divergent def betree.Node.apply_upserts betree.Message.Insert v) Result.ok (v, msgs1) +/- [betree::betree::{betree::betree::Node#5}::apply_upserts]: + Source: 'src/betree.rs', lines 820:4-820:94 -/ +def betree.Node.apply_upserts + (msgs : betree.List (U64 × betree.Message)) (prev : Option U64) (key : U64) + : + Result (U64 × (betree.List (U64 × betree.Message))) + := + 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 -/ mutual divergent def betree.Internal.lookup_in_children (self : betree.Internal) (key : U64) (st : State) : Result (State × ((Option U64) × betree.Internal)) @@ -261,7 +331,7 @@ mutual divergent def betree.Internal.lookup_in_children Result.ok (st1, (o, betree.Internal.mk self.id self.pivot self.left 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 -/ divergent def betree.Node.lookup (self : betree.Node) (key : U64) (st : State) : Result (State × ((Option U64) × betree.Node)) @@ -320,9 +390,9 @@ divergent def betree.Node.lookup end -/- [betree::betree::{betree::betree::Node#5}::filter_messages_for_key]: - Source: 'src/betree.rs', lines 674:4-674:77 -/ -divergent def 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 -/ +divergent def betree.Node.filter_messages_for_key_loop (key : U64) (msgs : betree.List (U64 × betree.Message)) : Result (betree.List (U64 × betree.Message)) := @@ -335,13 +405,21 @@ divergent def betree.Node.filter_messages_for_key let (_, msgs1) ← betree.List.pop_front (U64 × betree.Message) (betree.List.Cons (k, m) l) - betree.Node.filter_messages_for_key key msgs1 + betree.Node.filter_messages_for_key_loop key msgs1 else Result.ok (betree.List.Cons (k, m) l) | betree.List.Nil => Result.ok betree.List.Nil -/- [betree::betree::{betree::betree::Node#5}::lookup_first_message_after_key]: - Source: 'src/betree.rs', lines 689:4-692:34 -/ -divergent def 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 -/ +def betree.Node.filter_messages_for_key + (key : U64) (msgs : betree.List (U64 × betree.Message)) : + Result (betree.List (U64 × betree.Message)) + := + 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 -/ +divergent def betree.Node.lookup_first_message_after_key_loop (key : U64) (msgs : betree.List (U64 × betree.Message)) : Result ((betree.List (U64 × betree.Message)) × (betree.List (U64 × betree.Message) → Result (betree.List (U64 × betree.Message)))) @@ -352,19 +430,28 @@ divergent def betree.Node.lookup_first_message_after_key if k = key then do - let (l, lookup_first_message_after_key_back) ← - betree.Node.lookup_first_message_after_key key next_msgs - let back := + let (l, back) ← + betree.Node.lookup_first_message_after_key_loop key next_msgs + let back1 := fun ret => do - let next_msgs1 ← lookup_first_message_after_key_back ret + let next_msgs1 ← back ret Result.ok (betree.List.Cons (k, m) next_msgs1) - Result.ok (l, back) + Result.ok (l, back1) else Result.ok (betree.List.Cons (k, m) next_msgs, Result.ok) | betree.List.Nil => Result.ok (betree.List.Nil, Result.ok) +/- [betree::betree::{betree::betree::Node#5}::lookup_first_message_after_key]: + Source: 'src/betree.rs', lines 694:4-697:34 -/ +def betree.Node.lookup_first_message_after_key + (key : U64) (msgs : betree.List (U64 × betree.Message)) : + Result ((betree.List (U64 × betree.Message)) × (betree.List (U64 × + betree.Message) → Result (betree.List (U64 × betree.Message)))) + := + 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 -/ def betree.Node.apply_to_internal (msgs : betree.List (U64 × betree.Message)) (key : U64) (new_msg : betree.Message) : @@ -427,9 +514,9 @@ def betree.Node.apply_to_internal betree.List.push_front (U64 × betree.Message) msgs1 (key, new_msg) 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 -/ -divergent def 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 -/ +divergent def betree.Node.apply_messages_to_internal_loop (msgs : betree.List (U64 × betree.Message)) (new_msgs : betree.List (U64 × betree.Message)) : Result (betree.List (U64 × betree.Message)) @@ -439,12 +526,21 @@ divergent def betree.Node.apply_messages_to_internal do let (i, m) := new_msg let msgs1 ← betree.Node.apply_to_internal msgs i m - betree.Node.apply_messages_to_internal msgs1 new_msgs_tl + betree.Node.apply_messages_to_internal_loop msgs1 new_msgs_tl | betree.List.Nil => Result.ok msgs -/- [betree::betree::{betree::betree::Node#5}::lookup_mut_in_bindings]: - Source: 'src/betree.rs', lines 653:4-656:32 -/ -divergent def 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 -/ +def betree.Node.apply_messages_to_internal + (msgs : betree.List (U64 × betree.Message)) + (new_msgs : betree.List (U64 × betree.Message)) : + Result (betree.List (U64 × betree.Message)) + := + 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 -/ +divergent def betree.Node.lookup_mut_in_bindings_loop (key : U64) (bindings : betree.List (U64 × U64)) : Result ((betree.List (U64 × U64)) × (betree.List (U64 × U64) → Result (betree.List (U64 × U64)))) @@ -456,18 +552,26 @@ divergent def betree.Node.lookup_mut_in_bindings then Result.ok (betree.List.Cons (i, i1) tl, Result.ok) else do - let (l, lookup_mut_in_bindings_back) ← - betree.Node.lookup_mut_in_bindings key tl - let back := + let (l, back) ← betree.Node.lookup_mut_in_bindings_loop key tl + let back1 := fun ret => do - let tl1 ← lookup_mut_in_bindings_back ret + let tl1 ← back ret Result.ok (betree.List.Cons (i, i1) tl1) - Result.ok (l, back) + Result.ok (l, back1) | betree.List.Nil => Result.ok (betree.List.Nil, Result.ok) +/- [betree::betree::{betree::betree::Node#5}::lookup_mut_in_bindings]: + Source: 'src/betree.rs', lines 664:4-667:32 -/ +def betree.Node.lookup_mut_in_bindings + (key : U64) (bindings : betree.List (U64 × U64)) : + Result ((betree.List (U64 × U64)) × (betree.List (U64 × U64) → Result + (betree.List (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 -/ def betree.Node.apply_to_leaf (bindings : betree.List (U64 × U64)) (key : U64) (new_msg : betree.Message) : @@ -506,9 +610,9 @@ def betree.Node.apply_to_leaf let bindings2 ← betree.List.push_front (U64 × U64) bindings1 (key, v) lookup_mut_in_bindings_back bindings2 -/- [betree::betree::{betree::betree::Node#5}::apply_messages_to_leaf]: - Source: 'src/betree.rs', lines 444:4-447:5 -/ -divergent def 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 -/ +divergent def betree.Node.apply_messages_to_leaf_loop (bindings : betree.List (U64 × U64)) (new_msgs : betree.List (U64 × betree.Message)) : Result (betree.List (U64 × U64)) @@ -518,11 +622,20 @@ divergent def betree.Node.apply_messages_to_leaf do let (i, m) := new_msg let bindings1 ← betree.Node.apply_to_leaf bindings i m - betree.Node.apply_messages_to_leaf bindings1 new_msgs_tl + betree.Node.apply_messages_to_leaf_loop bindings1 new_msgs_tl | betree.List.Nil => Result.ok bindings +/- [betree::betree::{betree::betree::Node#5}::apply_messages_to_leaf]: + Source: 'src/betree.rs', lines 463:4-466:5 -/ +def betree.Node.apply_messages_to_leaf + (bindings : betree.List (U64 × U64)) + (new_msgs : betree.List (U64 × betree.Message)) : + Result (betree.List (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 -/ mutual divergent def betree.Internal.flush (self : betree.Internal) (params : betree.Params) (node_id_cnt : betree.NodeIdCounter) @@ -563,7 +676,7 @@ mutual divergent def betree.Internal.flush self.left 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 -/ divergent def betree.Node.apply_messages (self : betree.Node) (params : betree.Params) (node_id_cnt : betree.NodeIdCounter) @@ -610,7 +723,7 @@ divergent def 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 -/ def betree.Node.apply (self : betree.Node) (params : betree.Params) (node_id_cnt : betree.NodeIdCounter) (key : U64) (new_msg : betree.Message) @@ -625,7 +738,7 @@ def betree.Node.apply Result.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 -/ def betree.BeTree.new (min_flush_size : U64) (split_size : U64) (st : State) : Result (State × betree.BeTree) @@ -642,7 +755,7 @@ def 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 -/ def betree.BeTree.apply (self : betree.BeTree) (key : U64) (msg : betree.Message) (st : State) : Result (State × betree.BeTree) @@ -654,7 +767,7 @@ def betree.BeTree.apply Result.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 -/ def betree.BeTree.insert (self : betree.BeTree) (key : U64) (value : U64) (st : State) : Result (State × betree.BeTree) @@ -662,7 +775,7 @@ def 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 -/ def betree.BeTree.delete (self : betree.BeTree) (key : U64) (st : State) : Result (State × betree.BeTree) @@ -670,7 +783,7 @@ def 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 -/ def betree.BeTree.upsert (self : betree.BeTree) (key : U64) (upd : betree.UpsertFunState) (st : State) : @@ -679,7 +792,7 @@ def 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 -/ def betree.BeTree.lookup (self : betree.BeTree) (key : U64) (st : State) : Result (State × ((Option U64) × betree.BeTree)) diff --git a/tests/src/betree/aeneas-test-options b/tests/src/betree/aeneas-test-options index c71e01df..5a1e4180 100644 --- a/tests/src/betree/aeneas-test-options +++ b/tests/src/betree/aeneas-test-options @@ -1,4 +1,4 @@ charon-args=--polonius --opaque=betree_utils -aeneas-args=-backward-no-state-update -test-trans-units -state -split-files +[!borrow-check] aeneas-args=-backward-no-state-update -test-trans-units -state -split-files [coq] aeneas-args=-use-fuel [fstar] aeneas-args=-decreases-clauses -template-clauses diff --git a/tests/src/betree/src/betree.rs b/tests/src/betree/src/betree.rs index 12f2847d..8ba07824 100644 --- a/tests/src/betree/src/betree.rs +++ b/tests/src/betree/src/betree.rs @@ -274,25 +274,41 @@ pub fn upsert_update(prev: Option<Value>, st: UpsertFunState) -> Value { impl<T> List<T> { fn len(&self) -> u64 { - match self { - List::Nil => 0, - List::Cons(_, tl) => 1 + tl.len(), + let mut l = self; + let mut len = 0; + while let List::Cons(_, tl) = l { + len += 1; + l = tl; } + len } /// Split a list at a given length - fn split_at(self, n: u64) -> (List<T>, List<T>) { - if n == 0 { - (List::Nil, self) - } else { - match self { + fn split_at(self, mut n: u64) -> (List<T>, List<T>) { + let mut beg = List::Nil; + let mut end = self; + while n > 0 { + match end { List::Nil => unreachable!(), - List::Cons(hd, tl) => { - let (ls0, ls1) = tl.split_at(n - 1); - (List::Cons(hd, Box::new(ls0)), ls1) + List::Cons(hd, mut tl) => { + n -= 1; + end = *tl; + *tl = beg; + beg = List::Cons(hd, tl); } } } + (beg.reverse(), end) + } + + fn reverse(mut self) -> Self { + let mut out = List::Nil; + while let List::Cons(hd, mut tl) = self { + self = *tl; + *tl = out; + out = List::Cons(hd, tl); + } + out } /// Push an element at the front of the list. @@ -337,17 +353,20 @@ impl<T> Map<Key, T> { /// Note that the bindings in the map are supposed to be sorted in /// order of increasing keys. fn partition_at_pivot(self, pivot: Key) -> (Map<Key, T>, Map<Key, T>) { - match self { - List::Nil => (List::Nil, List::Nil), - List::Cons(hd, tl) => { - if hd.0 >= pivot { - (List::Nil, List::Cons(hd, tl)) - } else { - let (ls0, ls1) = tl.partition_at_pivot(pivot); - (List::Cons(hd, Box::new(ls0)), ls1) - } + let mut beg = List::Nil; + let mut end = List::Nil; + let mut curr = self; + while let List::Cons(hd, mut tl) = curr { + curr = *tl; + if hd.0 >= pivot { + *tl = end; + end = List::Cons(hd, tl); + } else { + *tl = beg; + beg = List::Cons(hd, tl); } } + (beg.reverse(), end.reverse()) } } @@ -443,14 +462,11 @@ impl Node { /// Apply a list of message to ourselves: leaf node case fn apply_messages_to_leaf<'a>( bindings: &'a mut Map<Key, Value>, - new_msgs: List<(Key, Message)>, + mut new_msgs: List<(Key, Message)>, ) { - match new_msgs { - List::Nil => (), - List::Cons(new_msg, new_msgs_tl) => { - Node::apply_to_leaf(bindings, new_msg.0, new_msg.1); - Node::apply_messages_to_leaf(bindings, *new_msgs_tl); - } + while let List::Cons(new_msg, new_msgs_tl) = new_msgs { + Node::apply_to_leaf(bindings, new_msg.0, new_msg.1); + new_msgs = *new_msgs_tl; } } @@ -501,14 +517,11 @@ impl Node { /// Apply a list of message to ourselves: internal node case fn apply_messages_to_internal<'a>( msgs: &'a mut Map<Key, Message>, - new_msgs: List<(Key, Message)>, + mut new_msgs: List<(Key, Message)>, ) { - match new_msgs { - List::Nil => (), - List::Cons(new_msg, new_msgs_tl) => { - Node::apply_to_internal(msgs, new_msg.0, new_msg.1); - Node::apply_messages_to_internal(msgs, *new_msgs_tl); - } + while let List::Cons(new_msg, new_msgs_tl) = new_msgs { + Node::apply_to_internal(msgs, new_msg.0, new_msg.1); + new_msgs = *new_msgs_tl; } } @@ -633,38 +646,34 @@ impl Node { /// Lookup a value in a list of bindings. /// Note that the values should be stored in order of increasing key. - fn lookup_in_bindings(key: Key, bindings: &Map<Key, Value>) -> Option<Value> { - match bindings { - List::Nil => Option::None, - List::Cons(hd, tl) => { - if hd.0 == key { - Option::Some(hd.1) - } else if hd.0 > key { - Option::None - } else { - Node::lookup_in_bindings(key, tl) - } + fn lookup_in_bindings(key: Key, mut bindings: &Map<Key, Value>) -> Option<Value> { + while let List::Cons(hd, tl) = bindings { + if hd.0 == key { + return Option::Some(hd.1); + } else if hd.0 > key { + return Option::None; + } else { + bindings = tl; } } + Option::None } /// Lookup a value in a list of bindings, and return a borrow to the position /// where the value is (or should be inserted, if the key is not in the bindings). fn lookup_mut_in_bindings<'a>( key: Key, - bindings: &'a mut Map<Key, Value>, + mut bindings: &'a mut Map<Key, Value>, ) -> &'a mut Map<Key, Value> { - match bindings { - List::Nil => bindings, - List::Cons(hd, tl) => { - // This requires Polonius - if hd.0 >= key { - bindings - } else { - Node::lookup_mut_in_bindings(key, tl) - } + while let List::Cons(hd, tl) = bindings { + // This requires Polonius + if hd.0 >= key { + break; + } else { + bindings = tl; } } + bindings } /// Filter all the messages which concern [key]. @@ -672,34 +681,28 @@ impl Node { /// Note that the stack of messages must start with a message for [key]: /// we stop filtering at the first message which is not about [key]. fn filter_messages_for_key<'a>(key: Key, msgs: &'a mut Map<Key, Message>) { - match msgs { - List::Nil => (), - List::Cons((k, _), _) => { - if *k == key { - msgs.pop_front(); - Node::filter_messages_for_key(key, msgs); - } else { - // Stop - () - } + while let List::Cons((k, _), _) = msgs { + if *k == key { + msgs.pop_front(); + } else { + // Stop + break; } } } fn lookup_first_message_after_key<'a>( key: Key, - msgs: &'a mut Map<Key, Message>, + mut msgs: &'a mut Map<Key, Message>, ) -> &'a mut Map<Key, Message> { - match msgs { - List::Nil => msgs, - List::Cons((k, _), next_msgs) => { - if *k == key { - Node::lookup_first_message_after_key(key, next_msgs) - } else { - msgs - } + while let List::Cons((k, _), next_msgs) = msgs { + if *k == key { + msgs = next_msgs; + } else { + break; } } + return msgs; } /// Returns the value bound to a key. @@ -788,24 +791,22 @@ impl Node { /// of the list). fn lookup_first_message_for_key<'a>( key: Key, - msgs: &'a mut Map<Key, Message>, + mut msgs: &'a mut Map<Key, Message>, ) -> &'a mut Map<Key, Message> { - match msgs { - List::Nil => msgs, - List::Cons(x, next_msgs) => { - // Rk.: we need Polonius here - // We wouldn't need Polonius if directly called the proper - // function to make the modifications here (because we wouldn't - // need to return anything). However, it would not be very - // idiomatic, especially with regards to the fact that we will - // rewrite everything with loops at some point. - if x.0 >= key { - msgs - } else { - Node::lookup_first_message_for_key(key, next_msgs) - } + while let List::Cons(x, next_msgs) = msgs { + // Rk.: we need Polonius here + // We wouldn't need Polonius if directly called the proper + // function to make the modifications here (because we wouldn't + // need to return anything). However, it would not be very + // idiomatic, especially with regards to the fact that we will + // rewrite everything with loops at some point. + if x.0 >= key { + return msgs; + } else { + msgs = next_msgs; } } + msgs } /// Apply the upserts from the current messages stack to a looked up value. @@ -816,8 +817,8 @@ impl Node { /// Note that if there are no more upserts to apply, then the value must be /// `Some`. Also note that we use the invariant that in the message stack, /// upsert messages are sorted from the first to the last to apply. - fn apply_upserts(msgs: &mut Map<Key, Message>, prev: Option<Value>, key: Key) -> Value { - if msgs.head_has_key(key) { + fn apply_upserts(msgs: &mut Map<Key, Message>, mut prev: Option<Value>, key: Key) -> Value { + while msgs.head_has_key(key) { // Pop the front message. // Note that it *must* be an upsert. let msg = msgs.pop_front(); @@ -825,9 +826,8 @@ impl Node { Message::Upsert(s) => { // Apply the update let v = upsert_update(prev, s); - let prev = Option::Some(v); + prev = Option::Some(v); // Continue - Node::apply_upserts(msgs, prev, key) } _ => { // Unreachable: we can only have [Upsert] messages @@ -835,13 +835,12 @@ impl Node { unreachable!(); } } - } else { - // We applied all the upsert messages: simply put an [Insert] - // message and return the value. - let v = prev.unwrap(); - msgs.push_front((key, Message::Insert(v))); - return v; } + // We applied all the upsert messages: simply put an [Insert] + // message and return the value. + let v = prev.unwrap(); + msgs.push_front((key, Message::Insert(v))); + v } } diff --git a/tests/src/bitwise.rs b/tests/src/bitwise.rs index fda8eff3..be12cea0 100644 --- a/tests/src/bitwise.rs +++ b/tests/src/bitwise.rs @@ -1,4 +1,4 @@ -//@ aeneas-args=-test-trans-units +//@ [!borrow-check] aeneas-args=-test-trans-units //@ [coq,fstar] subdir=misc //! Exercise the bitwise operations diff --git a/tests/src/borrow-check-negative.borrow-check.out b/tests/src/borrow-check-negative.borrow-check.out new file mode 100644 index 00000000..dc9dd5a7 --- /dev/null +++ b/tests/src/borrow-check-negative.borrow-check.out @@ -0,0 +1,15 @@ +[[92mInfo[39m ] Imported: tests/llbc/borrow_check_negative.llbc +[[91mError[39m] Can not apply a projection to the ⊥ value +Source: 'tests/src/borrow-check-negative.rs', lines 17:4-24:1 +[[91mError[39m] Can't end abstraction 8 as it is set as non-endable +Source: 'tests/src/borrow-check-negative.rs', lines 26:0-26:76 +[[91mError[39m] Can not apply a projection to the ⊥ value +Source: 'tests/src/borrow-check-negative.rs', lines 37:4-41:1 +[[91mError[39m] Can not apply a projection to the ⊥ value +Source: 'tests/src/borrow-check-negative.rs', lines 47:4-50:1 +[[91mError[39m] Can not apply a projection to the ⊥ value +Source: 'tests/src/borrow-check-negative.rs', lines 60:4-64:1 +[[91mError[39m] Can not apply a projection to the ⊥ value +Source: 'tests/src/borrow-check-negative.rs', lines 71:4-79:1 +[[91mError[39m] Can not apply a projection to the ⊥ value +Source: 'tests/src/borrow-check-negative.rs', lines 87:4-90:1 diff --git a/tests/src/borrow-check-negative.rs b/tests/src/borrow-check-negative.rs new file mode 100644 index 00000000..697546dd --- /dev/null +++ b/tests/src/borrow-check-negative.rs @@ -0,0 +1,90 @@ +//@ [!borrow-check] skip +//@ [borrow-check] known-failure +// Some negative tests for borrow checking + +// This succeeds +fn choose<'a, T>(b: bool, x: &'a mut T, y: &'a mut T) -> &'a mut T { + if b { + x + } else { + y + } +} + +pub fn choose_test() { + let mut x = 0; + let mut y = 0; + let z = choose(true, &mut x, &mut y); + *z += 1; + assert!(*z == 1); + // drop(z) + assert!(x == 1); + assert!(y == 0); + assert!(*z == 1); // z is not valid anymore +} + +fn choose_wrong<'a, 'b, T>(b: bool, x: &'a mut T, y: &'b mut T) -> &'a mut T { + if b { + x + } else { + y // Expected lifetime 'a + } +} + +fn test_mut1(b: bool) { + let mut x = 0; + let mut y = 1; + let z = if b { &mut x } else { &mut y }; + *z += 1; + assert!(x >= 0); + *z += 1; // z is not valid anymore +} + +#[allow(unused_assignments)] +fn test_mut2(b: bool) { + let mut x = 0; + let mut y = 1; + let z = if b { &x } else { &y }; + x += 1; + assert!(*z == 0); // z is not valid anymore +} + +fn test_move1<T>(x: T) -> T { + let _ = x; + return x; // x has been moved +} + +pub fn refs_test1() { + let mut x = 0; + let mut px = &mut x; + let ppx = &mut px; + **ppx = 1; + assert!(x == 1); + assert!(**ppx == 1); // ppx has ended +} + +pub fn refs_test2() { + let mut x = 0; + let mut y = 1; + let mut px = &mut x; + let py = &mut y; + let ppx = &mut px; + *ppx = py; + **ppx = 2; + assert!(*px == 2); + assert!(x == 0); + assert!(*py == 2); + assert!(y == 2); + assert!(**ppx == 2); // ppx has ended +} + +pub fn test_box1() { + use std::ops::Deref; + use std::ops::DerefMut; + let mut b: Box<i32> = Box::new(0); + let x0 = b.deref_mut(); + *x0 = 1; + let x1 = b.deref(); + assert!(*x1 == 1); + assert!(*x0 == 1); // x0 has ended +} diff --git a/tests/src/constants.rs b/tests/src/constants.rs index ac24dcd4..71d7c557 100644 --- a/tests/src/constants.rs +++ b/tests/src/constants.rs @@ -1,5 +1,5 @@ //@ charon-args=--no-code-duplication -//@ aeneas-args=-test-trans-units +//@ [!borrow-check] aeneas-args=-test-trans-units //@ [coq,fstar] subdir=misc //! Tests with constants diff --git a/tests/src/external.rs b/tests/src/external.rs index baea76e4..00acdb0b 100644 --- a/tests/src/external.rs +++ b/tests/src/external.rs @@ -1,6 +1,6 @@ //@ charon-args=--no-code-duplication -//@ aeneas-args=-state -split-files -//@ aeneas-args=-test-trans-units +//@ [!borrow-check] aeneas-args=-state -split-files +//@ [!borrow-check] aeneas-args=-test-trans-units //@ [coq,fstar] subdir=misc //! This module uses external types and functions diff --git a/tests/src/hashmap.rs b/tests/src/hashmap.rs index 19832a84..7dda2404 100644 --- a/tests/src/hashmap.rs +++ b/tests/src/hashmap.rs @@ -1,5 +1,5 @@ //@ charon-args=--opaque=utils -//@ aeneas-args=-state -split-files +//@ [!borrow-check] aeneas-args=-state -split-files //@ [coq] aeneas-args=-use-fuel //@ [fstar] aeneas-args=-decreases-clauses -template-clauses //@ [lean] aeneas-args=-no-gen-lib-entry diff --git a/tests/src/loops-borrow-check-fail.borrow-check.out b/tests/src/loops-borrow-check-fail.borrow-check.out new file mode 100644 index 00000000..34eb75f8 --- /dev/null +++ b/tests/src/loops-borrow-check-fail.borrow-check.out @@ -0,0 +1,5 @@ +[[92mInfo[39m ] Imported: tests/llbc/loops_borrow_check_fail.llbc +[[91mError[39m] Can not apply a projection to the ⊥ value +Source: 'tests/src/loops-borrow-check-fail.rs', lines 7:4-12:1 +[[91mError[39m] Can not apply a projection to the ⊥ value +Source: 'tests/src/loops-borrow-check-fail.rs', lines 17:4-21:1 diff --git a/tests/src/loops-borrow-check-fail.rs b/tests/src/loops-borrow-check-fail.rs new file mode 100644 index 00000000..24be052c --- /dev/null +++ b/tests/src/loops-borrow-check-fail.rs @@ -0,0 +1,21 @@ +//@ [!borrow-check] skip +//@ [borrow-check] known-failure + +// We need to use the general rules for joining the loans +fn loop_reborrow_mut() { + let mut x = 0; + let mut px = &mut x; + while *px > 0 { + x += 1; + px = &mut x; + } +} + +// We need to imrpove [prepare_ashared_loans] +fn iter_local_shared_borrow() { + let mut x = 0; + let mut p = &x; + loop { + p = &(*p); + } +} diff --git a/tests/src/loops-borrow-check-negative.borrow-check.out b/tests/src/loops-borrow-check-negative.borrow-check.out new file mode 100644 index 00000000..093d8b8a --- /dev/null +++ b/tests/src/loops-borrow-check-negative.borrow-check.out @@ -0,0 +1,3 @@ +[[92mInfo[39m ] Imported: tests/llbc/loops_borrow_check_negative.llbc +[[91mError[39m] Can't end abstraction 16 as it is set as non-endable +Source: 'tests/src/loops-borrow-check-negative.rs', lines 18:0-18:66 diff --git a/tests/src/loops-borrow-check-negative.rs b/tests/src/loops-borrow-check-negative.rs new file mode 100644 index 00000000..3386d581 --- /dev/null +++ b/tests/src/loops-borrow-check-negative.rs @@ -0,0 +1,28 @@ +//@ [!borrow-check] skip +//@ [borrow-check] known-failure + +// This succeeds +fn loop_a<'a>(a: &'a mut u32, b: &'a mut u32) -> &'a mut u32 { + let mut x = 0; + while x > 0 { + x += 1; + } + if x > 0 { + a + } else { + b + } +} + +// This fails +fn loop_a_b<'a, 'b>(a: &'a mut u32, b: &'b mut u32) -> &'a mut u32 { + let mut x = 0; + while x > 0 { + x += 1; + } + if x > 0 { + a + } else { + b // Expect lifetime 'a + } +} diff --git a/tests/src/loops-borrow-check.rs b/tests/src/loops-borrow-check.rs new file mode 100644 index 00000000..ab300b37 --- /dev/null +++ b/tests/src/loops-borrow-check.rs @@ -0,0 +1,10 @@ +//@ [!borrow-check] skip + +fn iter_local_mut_borrow() { + let mut x = 0; + let mut p = &mut x; + loop { + p = &mut (*p); + *p += 1; + } +} diff --git a/tests/src/mutually-recursive-traits.lean.out b/tests/src/mutually-recursive-traits.lean.out index 6d638644..e2ed3abc 100644 --- a/tests/src/mutually-recursive-traits.lean.out +++ b/tests/src/mutually-recursive-traits.lean.out @@ -1,17 +1,17 @@ [[92mInfo[39m ] Imported: tests/llbc/mutually_recursive_traits.llbc -[[91mError[39m] In file Translate.ml, line 812: +[[91mError[39m] In file Translate.ml, line 813: Mutually recursive trait declarations are not supported Uncaught exception: (Failure - "In file Translate.ml, line 812:\ - \nIn file Translate.ml, line 812:\ + "In file Translate.ml, line 813:\ + \nIn file Translate.ml, line 813:\ \nMutually recursive trait declarations are not supported") Raised at Aeneas__Errors.craise_opt_span in file "Errors.ml", line 46, characters 4-76 Called from Stdlib__List.iter in file "list.ml", line 110, characters 12-15 -Called from Aeneas__Translate.extract_definitions in file "Translate.ml", line 835, characters 2-52 -Called from Aeneas__Translate.extract_file in file "Translate.ml", line 953, characters 2-36 -Called from Aeneas__Translate.translate_crate in file "Translate.ml", line 1501, characters 5-42 -Called from Dune__exe__Main in file "Main.ml", line 276, characters 9-61 +Called from Aeneas__Translate.extract_definitions in file "Translate.ml", line 836, characters 2-52 +Called from Aeneas__Translate.extract_file in file "Translate.ml", line 954, characters 2-36 +Called from Aeneas__Translate.translate_crate in file "Translate.ml", line 1503, characters 5-42 +Called from Dune__exe__Main in file "Main.ml", line 314, characters 14-66 diff --git a/tests/src/mutually-recursive-traits.rs b/tests/src/mutually-recursive-traits.rs index 351763b2..9bc4ca63 100644 --- a/tests/src/mutually-recursive-traits.rs +++ b/tests/src/mutually-recursive-traits.rs @@ -1,6 +1,6 @@ //@ [lean] known-failure -//@ [coq,fstar] skip -//@ subdir=misc +//@ [!lean] skip +//@ [lean] subdir=misc pub trait Trait1 { type T: Trait2; } diff --git a/tests/src/no_nested_borrows.rs b/tests/src/no_nested_borrows.rs index 6d3074ef..11c4a695 100644 --- a/tests/src/no_nested_borrows.rs +++ b/tests/src/no_nested_borrows.rs @@ -1,5 +1,5 @@ //@ charon-args=--no-code-duplication -//@ aeneas-args=-test-trans-units +//@ [!borrow-check] aeneas-args=-test-trans-units //@ [coq,fstar] subdir=misc //! This module doesn't contain **functions which use nested borrows in their //! signatures**, and doesn't contain functions with loops. diff --git a/tests/src/paper.rs b/tests/src/paper.rs index 6a4a7c31..d9fb1032 100644 --- a/tests/src/paper.rs +++ b/tests/src/paper.rs @@ -1,5 +1,5 @@ //@ charon-args=--no-code-duplication -//@ aeneas-args=-test-trans-units +//@ [!borrow-check] aeneas-args=-test-trans-units //@ [coq,fstar] subdir=misc //! The examples from the ICFP submission, all in one place. diff --git a/tests/src/polonius_list.rs b/tests/src/polonius_list.rs index b029ad02..084441aa 100644 --- a/tests/src/polonius_list.rs +++ b/tests/src/polonius_list.rs @@ -1,5 +1,5 @@ //@ charon-args=--polonius -//@ aeneas-args=-test-trans-units +//@ [!borrow-check] aeneas-args=-test-trans-units //@ [coq,fstar] subdir=misc #![allow(dead_code)] diff --git a/tests/src/string-chars.rs b/tests/src/string-chars.rs index f8490e76..9fd91752 100644 --- a/tests/src/string-chars.rs +++ b/tests/src/string-chars.rs @@ -1,5 +1,5 @@ //@ [lean] known-failure -//@ [coq,fstar] skip +//@ [!lean] skip //@ no-check-output fn main() { let s = "hello"; diff --git a/tests/test_runner/Backend.ml b/tests/test_runner/Backend.ml index d21a46fc..819081a2 100644 --- a/tests/test_runner/Backend.ml +++ b/tests/test_runner/Backend.ml @@ -1,15 +1,24 @@ (*** Define the backends we support as an enum *) -type t = Coq | Lean | FStar | HOL4 [@@deriving ord, sexp] +type t = + | Coq + | Lean + | FStar + | HOL4 + | BorrowCheck + (** Borrow check: no backend. + We use this when we only want to borrow-check the program *) +[@@deriving ord, sexp] (* TODO: reactivate HOL4 once traits are parameterized by their associated types *) -let all = [ Coq; Lean; FStar ] +let all = [ Coq; Lean; FStar; BorrowCheck ] let of_string = function | "coq" -> Coq | "lean" -> Lean | "fstar" -> FStar | "hol4" -> HOL4 + | "borrow-check" -> BorrowCheck | backend -> failwith ("Unknown backend: `" ^ backend ^ "`") let to_string = function @@ -17,6 +26,11 @@ let to_string = function | Lean -> "lean" | FStar -> "fstar" | HOL4 -> "hol4" + | BorrowCheck -> "borrow-check" + +let to_command = function + | BorrowCheck -> [ "-borrow-check" ] + | x -> [ "-backend"; to_string x ] module Map = struct (* Hack to be able to include things from the parent module with the same names *) diff --git a/tests/test_runner/Input.ml b/tests/test_runner/Input.ml index 960ffe8d..e35be96f 100644 --- a/tests/test_runner/Input.ml +++ b/tests/test_runner/Input.ml @@ -7,7 +7,7 @@ type action = Normal | Skip | KnownFailure type per_backend = { action : action; aeneas_options : string list; - subdir : string; + subdir : string option; (* Whether to store the command output to a file. Only available for known-failure tests. *) check_output : bool; } @@ -22,8 +22,11 @@ type t = { } (* The default subdirectory in which to store the outputs. *) -let default_subdir backend test_name = - match backend with Backend.Lean -> "." | _ -> test_name +let default_subdir backend test_name : string option = + match backend with + | Backend.Lean -> Some "." + | Backend.BorrowCheck -> None + | _ -> Some test_name (* Parse lines that start `//@`. Each of them modifies the options we use for the test. Supported comments: @@ -39,14 +42,21 @@ let default_subdir backend test_name = let apply_special_comment comment input = let comment = String.trim comment in (* Parse the backends if any *) - let re = Re.compile (Re.Pcre.re "^\\[([a-zA-Z,]+)\\](.*)$") in + let re = Re.compile (Re.Pcre.re "^\\[(!)?([a-zA-Z,-]+)\\](.*)$") in let comment, (backends : Backend.t list) = match Re.exec_opt re comment with | Some groups -> - let backends = Re.Group.get groups 1 in + let exclude = Re.Group.get_opt groups 1 <> None in + let backends = Re.Group.get groups 2 in let backends = String.split_on_char ',' backends in let backends = List.map Backend.of_string backends in - let rest = Re.Group.get groups 2 in + let rest = Re.Group.get groups 3 in + (* If [exclude]: we take all the backends *but* the list provided. *) + let backends = + if exclude then + List.filter (fun x -> not (List.mem x backends)) Backend.all + else backends + in (String.trim rest, backends) | None -> (comment, Backend.all) in @@ -83,9 +93,9 @@ let apply_special_comment comment input = let args = String.split_on_char ' ' args in per_backend (fun x -> { x with aeneas_options = List.append x.aeneas_options args }) - else if Option.is_some subdir then - let subdir = Option.get subdir in - per_backend (fun x -> { x with subdir }) + else if Option.is_some subdir then ( + assert (not (List.mem Backend.BorrowCheck backends)); + per_backend (fun x -> { x with subdir })) else failwith ("Unrecognized special comment: `" ^ comment ^ "`") (* Given a path to a rust file or crate, gather the details and options about how to build the test. *) diff --git a/tests/test_runner/run_test.ml b/tests/test_runner/run_test.ml index c17c17be..0c3426c5 100644 --- a/tests/test_runner/run_test.ml +++ b/tests/test_runner/run_test.ml @@ -50,25 +50,35 @@ end (* Run Aeneas on a specific input with the given options *) let run_aeneas (env : runner_env) (case : Input.t) (backend : Backend.t) = let backend_str = Backend.to_string backend in + let backend_command = Backend.to_command backend in let input_file = concat_path [ env.llbc_dir; case.name ] ^ ".llbc" in let output_file = Filename.remove_extension case.path ^ "." ^ backend_str ^ ".out" in + let per_backend = Backend.Map.find backend case.per_backend in let subdir = per_backend.subdir in let check_output = per_backend.check_output in let aeneas_options = per_backend.aeneas_options in let action = per_backend.action in - let dest_dir = concat_path [ env.dest_dir; backend_str; subdir ] in + (* No destination directory if we borrow-check *) + let dest_command = + match backend with + | Backend.BorrowCheck -> [] + | _ -> + let subdir = match subdir with None -> [] | Some x -> [ x ] in + [ "-dest"; concat_path ([ env.dest_dir; backend_str ] @ subdir) ] + in (* Build the command *) - let args = - [ env.aeneas_path; input_file; "-dest"; dest_dir; "-backend"; backend_str ] - in + let args = [ env.aeneas_path; input_file ] @ dest_command @ backend_command in + (* If we target a specific backend and the test is known to fail, we abort + on error so as not to generate any files *) let abort_on_error = match action with | Skip | Normal -> [] - | KnownFailure -> [ "-abort-on-error" ] + | KnownFailure -> + if backend = Backend.BorrowCheck then [] else [ "-abort-on-error" ] in let args = List.concat [ args; aeneas_options; abort_on_error ] in let cmd = Command.make args in |