From a0c58326c43a7a8026b3d4c158017bf126180e90 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Fri, 22 Dec 2023 23:23:30 +0100 Subject: Regenerate the test files and add the fstar-split tests --- tests/coq/betree/BetreeMain_Funs.v | 1052 ++++++++++++------------------------ 1 file changed, 340 insertions(+), 712 deletions(-) (limited to 'tests/coq/betree/BetreeMain_Funs.v') diff --git a/tests/coq/betree/BetreeMain_Funs.v b/tests/coq/betree/BetreeMain_Funs.v index a5dd4230..516bc7b7 100644 --- a/tests/coq/betree/BetreeMain_Funs.v +++ b/tests/coq/betree/BetreeMain_Funs.v @@ -12,7 +12,7 @@ Require Import BetreeMain_FunsExternal. Include BetreeMain_FunsExternal. Module BetreeMain_Funs. -(** [betree_main::betree::load_internal_node]: forward function +(** [betree_main::betree::load_internal_node]: Source: 'src/betree.rs', lines 36:0-36:52 *) Definition betree_load_internal_node (id : u64) (st : state) : @@ -21,70 +21,57 @@ Definition betree_load_internal_node betree_utils_load_internal_node id st . -(** [betree_main::betree::store_internal_node]: forward function +(** [betree_main::betree::store_internal_node]: Source: 'src/betree.rs', lines 41:0-41:60 *) Definition betree_store_internal_node (id : u64) (content : betree_List_t (u64 * betree_Message_t)) (st : state) : result (state * unit) := p <- betree_utils_store_internal_node id content st; - let (st0, _) := p in - Return (st0, tt) + let (st1, _) := p in + Return (st1, tt) . -(** [betree_main::betree::load_leaf_node]: forward function +(** [betree_main::betree::load_leaf_node]: Source: 'src/betree.rs', lines 46:0-46:44 *) Definition betree_load_leaf_node (id : u64) (st : state) : result (state * (betree_List_t (u64 * u64))) := betree_utils_load_leaf_node id st . -(** [betree_main::betree::store_leaf_node]: forward function +(** [betree_main::betree::store_leaf_node]: Source: 'src/betree.rs', lines 51:0-51:52 *) Definition betree_store_leaf_node (id : u64) (content : betree_List_t (u64 * u64)) (st : state) : result (state * unit) := p <- betree_utils_store_leaf_node id content st; - let (st0, _) := p in - Return (st0, tt) + let (st1, _) := p in + Return (st1, tt) . -(** [betree_main::betree::fresh_node_id]: forward function +(** [betree_main::betree::fresh_node_id]: Source: 'src/betree.rs', lines 55:0-55:48 *) -Definition betree_fresh_node_id (counter : u64) : result u64 := - _ <- u64_add counter 1%u64; Return counter +Definition betree_fresh_node_id (counter : u64) : result (u64 * u64) := + counter1 <- u64_add counter 1%u64; Return (counter, counter1) . -(** [betree_main::betree::fresh_node_id]: backward function 0 - Source: 'src/betree.rs', lines 55:0-55:48 *) -Definition betree_fresh_node_id_back (counter : u64) : result u64 := - u64_add counter 1%u64 -. - -(** [betree_main::betree::{betree_main::betree::NodeIdCounter}::new]: forward function +(** [betree_main::betree::{betree_main::betree::NodeIdCounter}::new]: Source: 'src/betree.rs', lines 206:4-206:20 *) Definition betree_NodeIdCounter_new : result betree_NodeIdCounter_t := Return {| betree_NodeIdCounter_next_node_id := 0%u64 |} . -(** [betree_main::betree::{betree_main::betree::NodeIdCounter}::fresh_id]: forward function +(** [betree_main::betree::{betree_main::betree::NodeIdCounter}::fresh_id]: Source: 'src/betree.rs', lines 210:4-210:36 *) Definition betree_NodeIdCounter_fresh_id - (self : betree_NodeIdCounter_t) : result u64 := - _ <- u64_add self.(betree_NodeIdCounter_next_node_id) 1%u64; - Return self.(betree_NodeIdCounter_next_node_id) -. - -(** [betree_main::betree::{betree_main::betree::NodeIdCounter}::fresh_id]: backward function 0 - Source: 'src/betree.rs', lines 210:4-210:36 *) -Definition betree_NodeIdCounter_fresh_id_back - (self : betree_NodeIdCounter_t) : result betree_NodeIdCounter_t := + (self : betree_NodeIdCounter_t) : result (u64 * betree_NodeIdCounter_t) := i <- u64_add self.(betree_NodeIdCounter_next_node_id) 1%u64; - Return {| betree_NodeIdCounter_next_node_id := i |} + Return (self.(betree_NodeIdCounter_next_node_id), + {| betree_NodeIdCounter_next_node_id := i |}) . -(** [betree_main::betree::upsert_update]: forward function +(** [betree_main::betree::upsert_update]: Source: 'src/betree.rs', lines 234:0-234:70 *) Definition betree_upsert_update (prev : option u64) (st : betree_UpsertFunState_t) : result u64 := @@ -92,49 +79,49 @@ Definition betree_upsert_update | None => match st with | Betree_UpsertFunState_Add v => Return v - | Betree_UpsertFunState_Sub i => Return 0%u64 + | Betree_UpsertFunState_Sub _ => Return 0%u64 end - | Some prev0 => + | Some prev1 => match st with | Betree_UpsertFunState_Add v => - margin <- u64_sub core_u64_max prev0; - if margin s>= v then u64_add prev0 v else Return core_u64_max + margin <- u64_sub core_u64_max prev1; + if margin s>= v then u64_add prev1 v else Return core_u64_max | Betree_UpsertFunState_Sub v => - if prev0 s>= v then u64_sub prev0 v else Return 0%u64 + if prev1 s>= v then u64_sub prev1 v else Return 0%u64 end end . -(** [betree_main::betree::{betree_main::betree::List#1}::len]: forward function +(** [betree_main::betree::{betree_main::betree::List#1}::len]: Source: 'src/betree.rs', lines 276:4-276:24 *) Fixpoint betree_List_len (T : Type) (n : nat) (self : betree_List_t T) : result u64 := match n with | O => Fail_ OutOfFuel - | S n0 => + | S n1 => match self with - | Betree_List_Cons t tl => i <- betree_List_len T n0 tl; u64_add 1%u64 i + | Betree_List_Cons _ tl => i <- betree_List_len T n1 tl; u64_add 1%u64 i | Betree_List_Nil => Return 0%u64 end end . -(** [betree_main::betree::{betree_main::betree::List#1}::split_at]: forward function +(** [betree_main::betree::{betree_main::betree::List#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) (n0 : u64) : + (T : Type) (n : nat) (self : betree_List_t T) (n1 : u64) : result ((betree_List_t T) * (betree_List_t T)) := match n with | O => Fail_ OutOfFuel - | S n1 => - if n0 s= 0%u64 + | S n2 => + if n1 s= 0%u64 then Return (Betree_List_Nil, self) else match self with | Betree_List_Cons hd tl => - i <- u64_sub n0 1%u64; - p <- betree_List_split_at T n1 tl i; + i <- u64_sub n1 1%u64; + p <- betree_List_split_at T n2 tl i; let (ls0, ls1) := p in let l := ls0 in Return (Betree_List_Cons hd l, ls1) @@ -143,58 +130,46 @@ Fixpoint betree_List_split_at end . -(** [betree_main::betree::{betree_main::betree::List#1}::push_front]: merged forward/backward function - (there is a single backward function, and the forward function returns ()) +(** [betree_main::betree::{betree_main::betree::List#1}::push_front]: Source: 'src/betree.rs', lines 299:4-299: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 + let (tl, _) := core_mem_replace (betree_List_t T) self Betree_List_Nil in let l := tl in Return (Betree_List_Cons x l) . -(** [betree_main::betree::{betree_main::betree::List#1}::pop_front]: forward function +(** [betree_main::betree::{betree_main::betree::List#1}::pop_front]: Source: 'src/betree.rs', lines 306:4-306:32 *) Definition betree_List_pop_front - (T : Type) (self : betree_List_t T) : result T := - let ls := core_mem_replace (betree_List_t T) self Betree_List_Nil in + (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 match ls with - | Betree_List_Cons x tl => Return x + | Betree_List_Cons x tl => Return (x, tl) | Betree_List_Nil => Fail_ Failure end . -(** [betree_main::betree::{betree_main::betree::List#1}::pop_front]: backward function 0 - Source: 'src/betree.rs', lines 306:4-306:32 *) -Definition betree_List_pop_front_back - (T : Type) (self : betree_List_t T) : result (betree_List_t T) := - let ls := core_mem_replace (betree_List_t T) self Betree_List_Nil in - match ls with - | Betree_List_Cons x tl => Return tl - | Betree_List_Nil => Fail_ Failure - end -. - -(** [betree_main::betree::{betree_main::betree::List#1}::hd]: forward function +(** [betree_main::betree::{betree_main::betree::List#1}::hd]: Source: 'src/betree.rs', lines 318:4-318:22 *) Definition betree_List_hd (T : Type) (self : betree_List_t T) : result T := match self with - | Betree_List_Cons hd l => Return hd + | Betree_List_Cons hd _ => Return hd | Betree_List_Nil => Fail_ Failure end . -(** [betree_main::betree::{betree_main::betree::List<(u64, T)>#2}::head_has_key]: forward function +(** [betree_main::betree::{betree_main::betree::List<(u64, T)>#2}::head_has_key]: Source: 'src/betree.rs', lines 327:4-327:44 *) Definition betree_ListTupleU64T_head_has_key (T : Type) (self : betree_List_t (u64 * T)) (key : u64) : result bool := match self with - | Betree_List_Cons hd l => let (i, _) := hd in Return (i s= key) + | Betree_List_Cons hd _ => let (i, _) := hd in Return (i s= key) | Betree_List_Nil => Return false end . -(** [betree_main::betree::{betree_main::betree::List<(u64, T)>#2}::partition_at_pivot]: forward function +(** [betree_main::betree::{betree_main::betree::List<(u64, T)>#2}::partition_at_pivot]: Source: 'src/betree.rs', lines 339:4-339:73 *) Fixpoint betree_ListTupleU64T_partition_at_pivot (T : Type) (n : nat) (self : betree_List_t (u64 * T)) (pivot : u64) : @@ -202,14 +177,14 @@ Fixpoint betree_ListTupleU64T_partition_at_pivot := match n with | O => Fail_ OutOfFuel - | S n0 => + | S n1 => match self with | Betree_List_Cons hd tl => let (i, t) := hd in if i s>= pivot then Return (Betree_List_Nil, Betree_List_Cons (i, t) tl) else ( - p <- betree_ListTupleU64T_partition_at_pivot T n0 tl pivot; + p <- betree_ListTupleU64T_partition_at_pivot T n1 tl pivot; let (ls0, ls1) := p in let l := ls0 in Return (Betree_List_Cons (i, t) l, ls1)) @@ -218,107 +193,76 @@ Fixpoint betree_ListTupleU64T_partition_at_pivot end . -(** [betree_main::betree::{betree_main::betree::Leaf#3}::split]: forward function +(** [betree_main::betree::{betree_main::betree::Leaf#3}::split]: Source: 'src/betree.rs', lines 359:4-364: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) (st : state) : - result (state * betree_Internal_t) + result (state * (betree_Internal_t * betree_NodeIdCounter_t)) := p <- betree_List_split_at (u64 * u64) n content params.(betree_Params_split_size); let (content0, content1) := p in - p0 <- betree_List_hd (u64 * u64) content1; - let (pivot, _) := p0 in - id0 <- betree_NodeIdCounter_fresh_id node_id_cnt; - node_id_cnt0 <- betree_NodeIdCounter_fresh_id_back node_id_cnt; - id1 <- betree_NodeIdCounter_fresh_id node_id_cnt0; - p1 <- betree_store_leaf_node id0 content0 st; - let (st0, _) := p1 in - p2 <- betree_store_leaf_node id1 content1 st0; - let (st1, _) := p2 in - let n0 := Betree_Node_Leaf + p1 <- betree_List_hd (u64 * u64) content1; + let (pivot, _) := p1 in + p2 <- betree_NodeIdCounter_fresh_id node_id_cnt; + let (id0, nic) := p2 in + p3 <- betree_NodeIdCounter_fresh_id nic; + let (id1, nic1) := p3 in + p4 <- betree_store_leaf_node id0 content0 st; + let (st1, _) := p4 in + p5 <- betree_store_leaf_node id1 content1 st1; + let (st2, _) := p5 in + let n1 := Betree_Node_Leaf {| betree_Leaf_id := id0; betree_Leaf_size := params.(betree_Params_split_size) |} in - let n1 := Betree_Node_Leaf + let n2 := Betree_Node_Leaf {| betree_Leaf_id := id1; betree_Leaf_size := params.(betree_Params_split_size) |} in - Return (st1, mkbetree_Internal_t self.(betree_Leaf_id) pivot n0 n1) + Return (st2, (mkbetree_Internal_t self.(betree_Leaf_id) pivot n1 n2, nic1)) . -(** [betree_main::betree::{betree_main::betree::Leaf#3}::split]: backward function 2 - Source: 'src/betree.rs', lines 359:4-364:17 *) -Definition betree_Leaf_split_back - (n : nat) (self : betree_Leaf_t) (content : betree_List_t (u64 * u64)) - (params : betree_Params_t) (node_id_cnt : betree_NodeIdCounter_t) - (st : state) : - result betree_NodeIdCounter_t - := - p <- - betree_List_split_at (u64 * u64) n content - params.(betree_Params_split_size); - let (content0, content1) := p in - _ <- betree_List_hd (u64 * u64) content1; - id0 <- betree_NodeIdCounter_fresh_id node_id_cnt; - node_id_cnt0 <- betree_NodeIdCounter_fresh_id_back node_id_cnt; - id1 <- betree_NodeIdCounter_fresh_id node_id_cnt0; - p0 <- betree_store_leaf_node id0 content0 st; - let (st0, _) := p0 in - _ <- betree_store_leaf_node id1 content1 st0; - betree_NodeIdCounter_fresh_id_back node_id_cnt0 -. - -(** [betree_main::betree::{betree_main::betree::Node#5}::lookup_first_message_for_key]: forward function +(** [betree_main::betree::{betree_main::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 (n : nat) (key : u64) (msgs : betree_List_t (u64 * betree_Message_t)) : - result (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)))) := match n with | O => Fail_ OutOfFuel - | S n0 => - match msgs with - | Betree_List_Cons x next_msgs => - let (i, m) := x in - if i s>= key - then Return (Betree_List_Cons (i, m) next_msgs) - else betree_Node_lookup_first_message_for_key n0 key next_msgs - | Betree_List_Nil => Return Betree_List_Nil - end - end -. - -(** [betree_main::betree::{betree_main::betree::Node#5}::lookup_first_message_for_key]: backward function 0 - Source: 'src/betree.rs', lines 789:4-792:34 *) -Fixpoint betree_Node_lookup_first_message_for_key_back - (n : nat) (key : u64) (msgs : betree_List_t (u64 * betree_Message_t)) - (ret : betree_List_t (u64 * betree_Message_t)) : - result (betree_List_t (u64 * betree_Message_t)) - := - match n with - | O => Fail_ OutOfFuel - | S n0 => + | S n1 => match msgs with | Betree_List_Cons x next_msgs => let (i, m) := x in if i s>= key - then Return ret + then + let back_'a := + fun (ret : betree_List_t (u64 * betree_Message_t)) => Return ret in + Return (Betree_List_Cons (i, m) next_msgs, back_'a) else ( - next_msgs0 <- - betree_Node_lookup_first_message_for_key_back n0 key next_msgs ret; - Return (Betree_List_Cons (i, m) next_msgs0)) - | Betree_List_Nil => Return ret + p <- betree_Node_lookup_first_message_for_key n1 key next_msgs; + let (l, lookup_first_message_for_key_back) := p in + let back_'a := + fun (ret : betree_List_t (u64 * betree_Message_t)) => + next_msgs1 <- lookup_first_message_for_key_back ret; + Return (Betree_List_Cons (i, m) next_msgs1) in + Return (l, back_'a)) + | Betree_List_Nil => + let back_'a := + fun (ret : betree_List_t (u64 * betree_Message_t)) => Return ret in + Return (Betree_List_Nil, back_'a) end end . -(** [betree_main::betree::{betree_main::betree::Node#5}::lookup_in_bindings]: forward function +(** [betree_main::betree::{betree_main::betree::Node#5}::lookup_in_bindings]: Source: 'src/betree.rs', lines 636:4-636:80 *) Fixpoint betree_Node_lookup_in_bindings (n : nat) (key : u64) (bindings : betree_List_t (u64 * u64)) : @@ -326,263 +270,146 @@ Fixpoint betree_Node_lookup_in_bindings := match n with | O => Fail_ OutOfFuel - | S n0 => + | S n1 => match bindings with | Betree_List_Cons hd tl => - let (i, i0) := hd in + let (i, i1) := hd in if i s= key - then Return (Some i0) + then Return (Some i1) else if i s> key then Return None - else betree_Node_lookup_in_bindings n0 key tl + else betree_Node_lookup_in_bindings n1 key tl | Betree_List_Nil => Return None end end . -(** [betree_main::betree::{betree_main::betree::Node#5}::apply_upserts]: forward function +(** [betree_main::betree::{betree_main::betree::Node#5}::apply_upserts]: Source: 'src/betree.rs', lines 819:4-819:90 *) Fixpoint betree_Node_apply_upserts (n : nat) (msgs : betree_List_t (u64 * betree_Message_t)) (prev : option u64) (key : u64) (st : state) : - result (state * u64) + result (state * (u64 * (betree_List_t (u64 * betree_Message_t)))) := match n with | O => Fail_ OutOfFuel - | S n0 => + | S n1 => b <- betree_ListTupleU64T_head_has_key betree_Message_t msgs key; if b then ( - msg <- betree_List_pop_front (u64 * betree_Message_t) msgs; + p <- betree_List_pop_front (u64 * betree_Message_t) msgs; + let (msg, l) := p in let (_, m) := msg in match m with - | Betree_Message_Insert i => Fail_ Failure + | Betree_Message_Insert _ => Fail_ Failure | Betree_Message_Delete => Fail_ Failure | Betree_Message_Upsert s => v <- betree_upsert_update prev s; - msgs0 <- betree_List_pop_front_back (u64 * betree_Message_t) msgs; - betree_Node_apply_upserts n0 msgs0 (Some v) key st + betree_Node_apply_upserts n1 l (Some v) key st end) else ( p <- core_option_Option_unwrap u64 prev st; - let (st0, v) := p in - _ <- + let (st1, v) := p in + l <- betree_List_push_front (u64 * betree_Message_t) msgs (key, Betree_Message_Insert v); - Return (st0, v)) - end -. - -(** [betree_main::betree::{betree_main::betree::Node#5}::apply_upserts]: backward function 0 - Source: 'src/betree.rs', lines 819:4-819:90 *) -Fixpoint betree_Node_apply_upserts_back - (n : nat) (msgs : betree_List_t (u64 * betree_Message_t)) (prev : option u64) - (key : u64) (st : state) : - result (betree_List_t (u64 * betree_Message_t)) - := - match n with - | O => Fail_ OutOfFuel - | S n0 => - b <- betree_ListTupleU64T_head_has_key betree_Message_t msgs key; - if b - then ( - msg <- betree_List_pop_front (u64 * betree_Message_t) msgs; - let (_, m) := msg in - match m with - | Betree_Message_Insert i => Fail_ Failure - | Betree_Message_Delete => Fail_ Failure - | Betree_Message_Upsert s => - v <- betree_upsert_update prev s; - msgs0 <- betree_List_pop_front_back (u64 * betree_Message_t) msgs; - betree_Node_apply_upserts_back n0 msgs0 (Some v) key st - end) - else ( - p <- core_option_Option_unwrap u64 prev st; - let (_, v) := p in - betree_List_push_front (u64 * betree_Message_t) msgs (key, - Betree_Message_Insert v)) + Return (st1, (v, l))) end . -(** [betree_main::betree::{betree_main::betree::Internal#4}::lookup_in_children]: forward function +(** [betree_main::betree::{betree_main::betree::Internal#4}::lookup_in_children]: Source: 'src/betree.rs', lines 395:4-395:63 *) Fixpoint betree_Internal_lookup_in_children (n : nat) (self : betree_Internal_t) (key : u64) (st : state) : - result (state * (option u64)) - := - match n with - | O => Fail_ OutOfFuel - | S n0 => - if key s< self.(betree_Internal_pivot) - then betree_Node_lookup n0 self.(betree_Internal_left) key st - else betree_Node_lookup n0 self.(betree_Internal_right) key st - end - -(** [betree_main::betree::{betree_main::betree::Internal#4}::lookup_in_children]: backward function 0 - Source: 'src/betree.rs', lines 395:4-395:63 *) -with betree_Internal_lookup_in_children_back - (n : nat) (self : betree_Internal_t) (key : u64) (st : state) : - result betree_Internal_t + result (state * ((option u64) * betree_Internal_t)) := match n with | O => Fail_ OutOfFuel - | S n0 => + | S n1 => if key s< self.(betree_Internal_pivot) then ( - n1 <- betree_Node_lookup_back n0 self.(betree_Internal_left) key st; - Return (mkbetree_Internal_t self.(betree_Internal_id) - self.(betree_Internal_pivot) n1 self.(betree_Internal_right))) + p <- betree_Node_lookup n1 self.(betree_Internal_left) key st; + let (st1, p1) := p in + let (o, n2) := p1 in + Return (st1, (o, mkbetree_Internal_t self.(betree_Internal_id) + self.(betree_Internal_pivot) n2 self.(betree_Internal_right)))) else ( - n1 <- betree_Node_lookup_back n0 self.(betree_Internal_right) key st; - Return (mkbetree_Internal_t self.(betree_Internal_id) - self.(betree_Internal_pivot) self.(betree_Internal_left) n1)) + p <- betree_Node_lookup n1 self.(betree_Internal_right) key st; + let (st1, p1) := p in + let (o, n2) := p1 in + Return (st1, (o, mkbetree_Internal_t self.(betree_Internal_id) + self.(betree_Internal_pivot) self.(betree_Internal_left) n2))) end -(** [betree_main::betree::{betree_main::betree::Node#5}::lookup]: forward function +(** [betree_main::betree::{betree_main::betree::Node#5}::lookup]: Source: 'src/betree.rs', lines 709:4-709:58 *) with betree_Node_lookup (n : nat) (self : betree_Node_t) (key : u64) (st : state) : - result (state * (option u64)) + result (state * ((option u64) * betree_Node_t)) := match n with | O => Fail_ OutOfFuel - | S n0 => - match self with - | Betree_Node_Internal node => - p <- betree_load_internal_node node.(betree_Internal_id) st; - let (st0, msgs) := p in - pending <- betree_Node_lookup_first_message_for_key n0 key msgs; - match pending with - | Betree_List_Cons p0 l => - let (k, msg) := p0 in - if k s<> key - then ( - p1 <- betree_Internal_lookup_in_children n0 node key st0; - let (st1, o) := p1 in - _ <- - betree_Node_lookup_first_message_for_key_back n0 key msgs - (Betree_List_Cons (k, msg) l); - Return (st1, o)) - else - match msg with - | Betree_Message_Insert v => - _ <- - betree_Node_lookup_first_message_for_key_back n0 key msgs - (Betree_List_Cons (k, Betree_Message_Insert v) l); - Return (st0, Some v) - | Betree_Message_Delete => - _ <- - betree_Node_lookup_first_message_for_key_back n0 key msgs - (Betree_List_Cons (k, Betree_Message_Delete) l); - Return (st0, None) - | Betree_Message_Upsert ufs => - p1 <- betree_Internal_lookup_in_children n0 node key st0; - let (st1, v) := p1 in - p2 <- - betree_Node_apply_upserts n0 (Betree_List_Cons (k, - Betree_Message_Upsert ufs) l) v key st1; - let (st2, v0) := p2 in - node0 <- betree_Internal_lookup_in_children_back n0 node key st0; - pending0 <- - betree_Node_apply_upserts_back n0 (Betree_List_Cons (k, - Betree_Message_Upsert ufs) l) v key st1; - msgs0 <- - betree_Node_lookup_first_message_for_key_back n0 key msgs - pending0; - p3 <- - betree_store_internal_node node0.(betree_Internal_id) msgs0 st2; - let (st3, _) := p3 in - Return (st3, Some v0) - end - | Betree_List_Nil => - p0 <- betree_Internal_lookup_in_children n0 node key st0; - let (st1, o) := p0 in - _ <- - betree_Node_lookup_first_message_for_key_back n0 key msgs - Betree_List_Nil; - Return (st1, o) - end - | Betree_Node_Leaf node => - p <- betree_load_leaf_node node.(betree_Leaf_id) st; - let (st0, bindings) := p in - o <- betree_Node_lookup_in_bindings n0 key bindings; - Return (st0, o) - end - end - -(** [betree_main::betree::{betree_main::betree::Node#5}::lookup]: backward function 0 - Source: 'src/betree.rs', lines 709:4-709:58 *) -with betree_Node_lookup_back - (n : nat) (self : betree_Node_t) (key : u64) (st : state) : - result betree_Node_t - := - match n with - | O => Fail_ OutOfFuel - | S n0 => + | S n1 => match self with | Betree_Node_Internal node => p <- betree_load_internal_node node.(betree_Internal_id) st; - let (st0, msgs) := p in - pending <- betree_Node_lookup_first_message_for_key n0 key msgs; + let (st1, msgs) := p in + p1 <- betree_Node_lookup_first_message_for_key n1 key msgs; + let (pending, lookup_first_message_for_key_back) := p1 in match pending with - | Betree_List_Cons p0 l => - let (k, msg) := p0 in + | Betree_List_Cons p2 l => + let (k, msg) := p2 in if k s<> key then ( - _ <- - betree_Node_lookup_first_message_for_key_back n0 key msgs - (Betree_List_Cons (k, msg) l); - node0 <- betree_Internal_lookup_in_children_back n0 node key st0; - Return (Betree_Node_Internal node0)) + p3 <- betree_Internal_lookup_in_children n1 node key st1; + let (st2, p4) := p3 in + let (o, i) := p4 in + _ <- lookup_first_message_for_key_back (Betree_List_Cons (k, msg) l); + Return (st2, (o, Betree_Node_Internal i))) else match msg with | Betree_Message_Insert v => _ <- - betree_Node_lookup_first_message_for_key_back n0 key msgs - (Betree_List_Cons (k, Betree_Message_Insert v) l); - Return (Betree_Node_Internal node) + lookup_first_message_for_key_back (Betree_List_Cons (k, + Betree_Message_Insert v) l); + Return (st1, (Some v, Betree_Node_Internal node)) | Betree_Message_Delete => _ <- - betree_Node_lookup_first_message_for_key_back n0 key msgs - (Betree_List_Cons (k, Betree_Message_Delete) l); - Return (Betree_Node_Internal node) + lookup_first_message_for_key_back (Betree_List_Cons (k, + Betree_Message_Delete) l); + Return (st1, (None, Betree_Node_Internal node)) | Betree_Message_Upsert ufs => - p1 <- betree_Internal_lookup_in_children n0 node key st0; - let (st1, v) := p1 in - p2 <- - betree_Node_apply_upserts n0 (Betree_List_Cons (k, - Betree_Message_Upsert ufs) l) v key st1; - let (st2, _) := p2 in - node0 <- betree_Internal_lookup_in_children_back n0 node key st0; - pending0 <- - betree_Node_apply_upserts_back n0 (Betree_List_Cons (k, - Betree_Message_Upsert ufs) l) v key st1; - msgs0 <- - betree_Node_lookup_first_message_for_key_back n0 key msgs - pending0; - _ <- - betree_store_internal_node node0.(betree_Internal_id) msgs0 st2; - Return (Betree_Node_Internal node0) + p3 <- betree_Internal_lookup_in_children n1 node key st1; + let (st2, p4) := p3 in + let (v, i) := p4 in + p5 <- + betree_Node_apply_upserts n1 (Betree_List_Cons (k, + Betree_Message_Upsert ufs) l) v key st2; + let (st3, p6) := p5 in + let (v1, l1) := p6 in + msgs1 <- lookup_first_message_for_key_back l1; + p7 <- betree_store_internal_node i.(betree_Internal_id) msgs1 st3; + let (st4, _) := p7 in + Return (st4, (Some v1, Betree_Node_Internal i)) end | Betree_List_Nil => - _ <- - betree_Node_lookup_first_message_for_key_back n0 key msgs - Betree_List_Nil; - node0 <- betree_Internal_lookup_in_children_back n0 node key st0; - Return (Betree_Node_Internal node0) + p2 <- betree_Internal_lookup_in_children n1 node key st1; + let (st2, p3) := p2 in + let (o, i) := p3 in + _ <- lookup_first_message_for_key_back Betree_List_Nil; + Return (st2, (o, Betree_Node_Internal i)) end | Betree_Node_Leaf node => p <- betree_load_leaf_node node.(betree_Leaf_id) st; - let (_, bindings) := p in - _ <- betree_Node_lookup_in_bindings n0 key bindings; - Return (Betree_Node_Leaf node) + let (st1, bindings) := p in + o <- betree_Node_lookup_in_bindings n1 key bindings; + Return (st1, (o, Betree_Node_Leaf node)) end end . -(** [betree_main::betree::{betree_main::betree::Node#5}::filter_messages_for_key]: merged forward/backward function - (there is a single backward function, and the forward function returns ()) +(** [betree_main::betree::{betree_main::betree::Node#5}::filter_messages_for_key]: Source: 'src/betree.rs', lines 674:4-674:77 *) Fixpoint betree_Node_filter_messages_for_key (n : nat) (key : u64) (msgs : betree_List_t (u64 * betree_Message_t)) : @@ -590,127 +417,118 @@ Fixpoint betree_Node_filter_messages_for_key := match n with | O => Fail_ OutOfFuel - | S n0 => + | S n1 => match msgs with | Betree_List_Cons p l => let (k, m) := p in if k s= key then ( - msgs0 <- - betree_List_pop_front_back (u64 * betree_Message_t) (Betree_List_Cons - (k, m) l); - betree_Node_filter_messages_for_key n0 key msgs0) + p1 <- + betree_List_pop_front (u64 * betree_Message_t) (Betree_List_Cons (k, + m) l); + let (_, l1) := p1 in + betree_Node_filter_messages_for_key n1 key l1) else Return (Betree_List_Cons (k, m) l) | Betree_List_Nil => Return Betree_List_Nil end end . -(** [betree_main::betree::{betree_main::betree::Node#5}::lookup_first_message_after_key]: forward function +(** [betree_main::betree::{betree_main::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 (n : nat) (key : u64) (msgs : betree_List_t (u64 * betree_Message_t)) : - result (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)))) := match n with | O => Fail_ OutOfFuel - | S n0 => - match msgs with - | Betree_List_Cons p next_msgs => - let (k, m) := p in - if k s= key - then betree_Node_lookup_first_message_after_key n0 key next_msgs - else Return (Betree_List_Cons (k, m) next_msgs) - | Betree_List_Nil => Return Betree_List_Nil - end - end -. - -(** [betree_main::betree::{betree_main::betree::Node#5}::lookup_first_message_after_key]: backward function 0 - Source: 'src/betree.rs', lines 689:4-692:34 *) -Fixpoint betree_Node_lookup_first_message_after_key_back - (n : nat) (key : u64) (msgs : betree_List_t (u64 * betree_Message_t)) - (ret : betree_List_t (u64 * betree_Message_t)) : - result (betree_List_t (u64 * betree_Message_t)) - := - match n with - | O => Fail_ OutOfFuel - | S n0 => + | S n1 => match msgs with | Betree_List_Cons p next_msgs => let (k, m) := p in if k s= key then ( - next_msgs0 <- - betree_Node_lookup_first_message_after_key_back n0 key next_msgs ret; - Return (Betree_List_Cons (k, m) next_msgs0)) - else Return ret - | Betree_List_Nil => Return ret + p1 <- betree_Node_lookup_first_message_after_key n1 key next_msgs; + let (l, lookup_first_message_after_key_back) := p1 in + let back_'a := + fun (ret : betree_List_t (u64 * betree_Message_t)) => + next_msgs1 <- lookup_first_message_after_key_back ret; + Return (Betree_List_Cons (k, m) next_msgs1) in + Return (l, back_'a)) + else + let back_'a := + fun (ret : betree_List_t (u64 * betree_Message_t)) => Return ret in + Return (Betree_List_Cons (k, m) next_msgs, back_'a) + | Betree_List_Nil => + let back_'a := + fun (ret : betree_List_t (u64 * betree_Message_t)) => Return ret in + Return (Betree_List_Nil, back_'a) end end . -(** [betree_main::betree::{betree_main::betree::Node#5}::apply_to_internal]: merged forward/backward function - (there is a single backward function, and the forward function returns ()) +(** [betree_main::betree::{betree_main::betree::Node#5}::apply_to_internal]: Source: 'src/betree.rs', lines 521:4-521:89 *) Definition betree_Node_apply_to_internal (n : nat) (msgs : betree_List_t (u64 * betree_Message_t)) (key : u64) (new_msg : betree_Message_t) : result (betree_List_t (u64 * betree_Message_t)) := - msgs0 <- betree_Node_lookup_first_message_for_key n key msgs; - b <- betree_ListTupleU64T_head_has_key betree_Message_t msgs0 key; + p <- betree_Node_lookup_first_message_for_key n key msgs; + let (msgs1, lookup_first_message_for_key_back) := p in + b <- betree_ListTupleU64T_head_has_key betree_Message_t msgs1 key; if b then match new_msg with | Betree_Message_Insert i => - msgs1 <- betree_Node_filter_messages_for_key n key msgs0; - msgs2 <- - betree_List_push_front (u64 * betree_Message_t) msgs1 (key, + l <- betree_Node_filter_messages_for_key n key msgs1; + l1 <- + betree_List_push_front (u64 * betree_Message_t) l (key, Betree_Message_Insert i); - betree_Node_lookup_first_message_for_key_back n key msgs msgs2 + lookup_first_message_for_key_back l1 | Betree_Message_Delete => - msgs1 <- betree_Node_filter_messages_for_key n key msgs0; - msgs2 <- - betree_List_push_front (u64 * betree_Message_t) msgs1 (key, + l <- betree_Node_filter_messages_for_key n key msgs1; + l1 <- + betree_List_push_front (u64 * betree_Message_t) l (key, Betree_Message_Delete); - betree_Node_lookup_first_message_for_key_back n key msgs msgs2 + lookup_first_message_for_key_back l1 | Betree_Message_Upsert s => - p <- betree_List_hd (u64 * betree_Message_t) msgs0; - let (_, m) := p in + p1 <- betree_List_hd (u64 * betree_Message_t) msgs1; + let (_, m) := p1 in match m with | Betree_Message_Insert prev => v <- betree_upsert_update (Some prev) s; - msgs1 <- betree_List_pop_front_back (u64 * betree_Message_t) msgs0; - msgs2 <- - betree_List_push_front (u64 * betree_Message_t) msgs1 (key, + p2 <- betree_List_pop_front (u64 * betree_Message_t) msgs1; + let (_, l) := p2 in + l1 <- + betree_List_push_front (u64 * betree_Message_t) l (key, Betree_Message_Insert v); - betree_Node_lookup_first_message_for_key_back n key msgs msgs2 + lookup_first_message_for_key_back l1 | Betree_Message_Delete => + p2 <- betree_List_pop_front (u64 * betree_Message_t) msgs1; + let (_, l) := p2 in v <- betree_upsert_update None s; - msgs1 <- betree_List_pop_front_back (u64 * betree_Message_t) msgs0; - msgs2 <- - betree_List_push_front (u64 * betree_Message_t) msgs1 (key, + l1 <- + betree_List_push_front (u64 * betree_Message_t) l (key, Betree_Message_Insert v); - betree_Node_lookup_first_message_for_key_back n key msgs msgs2 - | Betree_Message_Upsert ufs => - msgs1 <- betree_Node_lookup_first_message_after_key n key msgs0; - msgs2 <- - betree_List_push_front (u64 * betree_Message_t) msgs1 (key, + lookup_first_message_for_key_back l1 + | Betree_Message_Upsert _ => + p2 <- betree_Node_lookup_first_message_after_key n key msgs1; + let (msgs2, lookup_first_message_after_key_back) := p2 in + l <- + betree_List_push_front (u64 * betree_Message_t) msgs2 (key, Betree_Message_Upsert s); - msgs3 <- - betree_Node_lookup_first_message_after_key_back n key msgs0 msgs2; - betree_Node_lookup_first_message_for_key_back n key msgs msgs3 + msgs3 <- lookup_first_message_after_key_back l; + lookup_first_message_for_key_back msgs3 end end else ( - msgs1 <- - betree_List_push_front (u64 * betree_Message_t) msgs0 (key, new_msg); - betree_Node_lookup_first_message_for_key_back n key msgs msgs1) + l <- betree_List_push_front (u64 * betree_Message_t) msgs1 (key, new_msg); + lookup_first_message_for_key_back l) . -(** [betree_main::betree::{betree_main::betree::Node#5}::apply_messages_to_internal]: merged forward/backward function - (there is a single backward function, and the forward function returns ()) +(** [betree_main::betree::{betree_main::betree::Node#5}::apply_messages_to_internal]: Source: 'src/betree.rs', lines 502:4-505:5 *) Fixpoint betree_Node_apply_messages_to_internal (n : nat) (msgs : betree_List_t (u64 * betree_Message_t)) @@ -719,104 +537,88 @@ Fixpoint betree_Node_apply_messages_to_internal := match n with | O => Fail_ OutOfFuel - | S n0 => + | S n1 => match new_msgs with | Betree_List_Cons new_msg new_msgs_tl => let (i, m) := new_msg in - msgs0 <- betree_Node_apply_to_internal n0 msgs i m; - betree_Node_apply_messages_to_internal n0 msgs0 new_msgs_tl + l <- betree_Node_apply_to_internal n1 msgs i m; + betree_Node_apply_messages_to_internal n1 l new_msgs_tl | Betree_List_Nil => Return msgs end end . -(** [betree_main::betree::{betree_main::betree::Node#5}::lookup_mut_in_bindings]: forward function +(** [betree_main::betree::{betree_main::betree::Node#5}::lookup_mut_in_bindings]: Source: 'src/betree.rs', lines 653:4-656:32 *) Fixpoint betree_Node_lookup_mut_in_bindings (n : nat) (key : u64) (bindings : betree_List_t (u64 * u64)) : - result (betree_List_t (u64 * u64)) - := - match n with - | O => Fail_ OutOfFuel - | S n0 => - match bindings with - | Betree_List_Cons hd tl => - let (i, i0) := hd in - if i s>= key - then Return (Betree_List_Cons (i, i0) tl) - else betree_Node_lookup_mut_in_bindings n0 key tl - | Betree_List_Nil => Return Betree_List_Nil - end - end -. - -(** [betree_main::betree::{betree_main::betree::Node#5}::lookup_mut_in_bindings]: backward function 0 - Source: 'src/betree.rs', lines 653:4-656:32 *) -Fixpoint betree_Node_lookup_mut_in_bindings_back - (n : nat) (key : u64) (bindings : betree_List_t (u64 * u64)) - (ret : betree_List_t (u64 * u64)) : - result (betree_List_t (u64 * u64)) + result ((betree_List_t (u64 * u64)) * (betree_List_t (u64 * u64) -> result + (betree_List_t (u64 * u64)))) := match n with | O => Fail_ OutOfFuel - | S n0 => + | S n1 => match bindings with | Betree_List_Cons hd tl => - let (i, i0) := hd in + let (i, i1) := hd in if i s>= key - then Return ret + then + let back_'a := fun (ret : betree_List_t (u64 * u64)) => Return ret in + Return (Betree_List_Cons (i, i1) tl, back_'a) else ( - tl0 <- betree_Node_lookup_mut_in_bindings_back n0 key tl ret; - Return (Betree_List_Cons (i, i0) tl0)) - | Betree_List_Nil => Return ret + p <- betree_Node_lookup_mut_in_bindings n1 key tl; + let (l, lookup_mut_in_bindings_back) := p in + let back_'a := + fun (ret : betree_List_t (u64 * u64)) => + tl1 <- lookup_mut_in_bindings_back ret; + Return (Betree_List_Cons (i, i1) tl1) in + Return (l, back_'a)) + | Betree_List_Nil => + let back_'a := fun (ret : betree_List_t (u64 * u64)) => Return ret in + Return (Betree_List_Nil, back_'a) end end . -(** [betree_main::betree::{betree_main::betree::Node#5}::apply_to_leaf]: merged forward/backward function - (there is a single backward function, and the forward function returns ()) +(** [betree_main::betree::{betree_main::betree::Node#5}::apply_to_leaf]: Source: 'src/betree.rs', lines 460:4-460:87 *) Definition betree_Node_apply_to_leaf (n : nat) (bindings : betree_List_t (u64 * u64)) (key : u64) (new_msg : betree_Message_t) : result (betree_List_t (u64 * u64)) := - bindings0 <- betree_Node_lookup_mut_in_bindings n key bindings; - b <- betree_ListTupleU64T_head_has_key u64 bindings0 key; + p <- betree_Node_lookup_mut_in_bindings n key bindings; + let (bindings1, lookup_mut_in_bindings_back) := p in + b <- betree_ListTupleU64T_head_has_key u64 bindings1 key; if b then ( - hd <- betree_List_pop_front (u64 * u64) bindings0; + p1 <- betree_List_pop_front (u64 * u64) bindings1; + let (hd, l) := p1 in match new_msg with | Betree_Message_Insert v => - bindings1 <- betree_List_pop_front_back (u64 * u64) bindings0; - bindings2 <- betree_List_push_front (u64 * u64) bindings1 (key, v); - betree_Node_lookup_mut_in_bindings_back n key bindings bindings2 - | Betree_Message_Delete => - bindings1 <- betree_List_pop_front_back (u64 * u64) bindings0; - betree_Node_lookup_mut_in_bindings_back n key bindings bindings1 + l1 <- betree_List_push_front (u64 * u64) l (key, v); + lookup_mut_in_bindings_back l1 + | Betree_Message_Delete => lookup_mut_in_bindings_back l | Betree_Message_Upsert s => let (_, i) := hd in v <- betree_upsert_update (Some i) s; - bindings1 <- betree_List_pop_front_back (u64 * u64) bindings0; - bindings2 <- betree_List_push_front (u64 * u64) bindings1 (key, v); - betree_Node_lookup_mut_in_bindings_back n key bindings bindings2 + l1 <- betree_List_push_front (u64 * u64) l (key, v); + lookup_mut_in_bindings_back l1 end) else match new_msg with | Betree_Message_Insert v => - bindings1 <- betree_List_push_front (u64 * u64) bindings0 (key, v); - betree_Node_lookup_mut_in_bindings_back n key bindings bindings1 - | Betree_Message_Delete => - betree_Node_lookup_mut_in_bindings_back n key bindings bindings0 + l <- betree_List_push_front (u64 * u64) bindings1 (key, v); + lookup_mut_in_bindings_back l + | Betree_Message_Delete => lookup_mut_in_bindings_back bindings1 | Betree_Message_Upsert s => v <- betree_upsert_update None s; - bindings1 <- betree_List_push_front (u64 * u64) bindings0 (key, v); - betree_Node_lookup_mut_in_bindings_back n key bindings bindings1 + l <- betree_List_push_front (u64 * u64) bindings1 (key, v); + lookup_mut_in_bindings_back l end . -(** [betree_main::betree::{betree_main::betree::Node#5}::apply_messages_to_leaf]: merged forward/backward function - (there is a single backward function, and the forward function returns ()) +(** [betree_main::betree::{betree_main::betree::Node#5}::apply_messages_to_leaf]: Source: 'src/betree.rs', lines 444:4-447:5 *) Fixpoint betree_Node_apply_messages_to_leaf (n : nat) (bindings : betree_List_t (u64 * u64)) @@ -825,404 +627,230 @@ Fixpoint betree_Node_apply_messages_to_leaf := match n with | O => Fail_ OutOfFuel - | S n0 => + | S n1 => match new_msgs with | Betree_List_Cons new_msg new_msgs_tl => let (i, m) := new_msg in - bindings0 <- betree_Node_apply_to_leaf n0 bindings i m; - betree_Node_apply_messages_to_leaf n0 bindings0 new_msgs_tl + l <- betree_Node_apply_to_leaf n1 bindings i m; + betree_Node_apply_messages_to_leaf n1 l new_msgs_tl | Betree_List_Nil => Return bindings end end . -(** [betree_main::betree::{betree_main::betree::Internal#4}::flush]: forward function +(** [betree_main::betree::{betree_main::betree::Internal#4}::flush]: Source: 'src/betree.rs', lines 410:4-415:26 *) Fixpoint betree_Internal_flush (n : nat) (self : betree_Internal_t) (params : betree_Params_t) (node_id_cnt : betree_NodeIdCounter_t) (content : betree_List_t (u64 * betree_Message_t)) (st : state) : - result (state * (betree_List_t (u64 * betree_Message_t))) + result (state * ((betree_List_t (u64 * betree_Message_t)) * + (betree_Internal_t * betree_NodeIdCounter_t))) := match n with | O => Fail_ OutOfFuel - | S n0 => - p <- - betree_ListTupleU64T_partition_at_pivot betree_Message_t n0 content - self.(betree_Internal_pivot); - let (msgs_left, msgs_right) := p in - len_left <- betree_List_len (u64 * betree_Message_t) n0 msgs_left; - if len_left s>= params.(betree_Params_min_flush_size) - then ( - p0 <- - betree_Node_apply_messages n0 self.(betree_Internal_left) params - node_id_cnt msgs_left st; - let (st0, _) := p0 in - p1 <- - betree_Node_apply_messages_back n0 self.(betree_Internal_left) params - node_id_cnt msgs_left st; - let (_, node_id_cnt0) := p1 in - len_right <- betree_List_len (u64 * betree_Message_t) n0 msgs_right; - if len_right s>= params.(betree_Params_min_flush_size) - then ( - p2 <- - betree_Node_apply_messages n0 self.(betree_Internal_right) params - node_id_cnt0 msgs_right st0; - let (st1, _) := p2 in - _ <- - betree_Node_apply_messages_back n0 self.(betree_Internal_right) - params node_id_cnt0 msgs_right st0; - Return (st1, Betree_List_Nil)) - else Return (st0, msgs_right)) - else ( - p0 <- - betree_Node_apply_messages n0 self.(betree_Internal_right) params - node_id_cnt msgs_right st; - let (st0, _) := p0 in - _ <- - betree_Node_apply_messages_back n0 self.(betree_Internal_right) params - node_id_cnt msgs_right st; - Return (st0, msgs_left)) - end - -(** [betree_main::betree::{betree_main::betree::Internal#4}::flush]: backward function 0 - Source: 'src/betree.rs', lines 410:4-415:26 *) -with betree_Internal_flush_back - (n : nat) (self : betree_Internal_t) (params : betree_Params_t) - (node_id_cnt : betree_NodeIdCounter_t) - (content : betree_List_t (u64 * betree_Message_t)) (st : state) : - result (betree_Internal_t * betree_NodeIdCounter_t) - := - match n with - | O => Fail_ OutOfFuel - | S n0 => + | S n1 => p <- - betree_ListTupleU64T_partition_at_pivot betree_Message_t n0 content + betree_ListTupleU64T_partition_at_pivot betree_Message_t n1 content self.(betree_Internal_pivot); let (msgs_left, msgs_right) := p in - len_left <- betree_List_len (u64 * betree_Message_t) n0 msgs_left; + len_left <- betree_List_len (u64 * betree_Message_t) n1 msgs_left; if len_left s>= params.(betree_Params_min_flush_size) then ( - p0 <- - betree_Node_apply_messages n0 self.(betree_Internal_left) params - node_id_cnt msgs_left st; - let (st0, _) := p0 in p1 <- - betree_Node_apply_messages_back n0 self.(betree_Internal_left) params + betree_Node_apply_messages n1 self.(betree_Internal_left) params node_id_cnt msgs_left st; - let (n1, node_id_cnt0) := p1 in - len_right <- betree_List_len (u64 * betree_Message_t) n0 msgs_right; + let (st1, p2) := p1 in + let (n2, node_id_cnt1) := p2 in + len_right <- betree_List_len (u64 * betree_Message_t) n1 msgs_right; if len_right s>= params.(betree_Params_min_flush_size) then ( - p2 <- - betree_Node_apply_messages_back n0 self.(betree_Internal_right) - params node_id_cnt0 msgs_right st0; - let (n2, node_id_cnt1) := p2 in - Return (mkbetree_Internal_t self.(betree_Internal_id) - self.(betree_Internal_pivot) n1 n2, node_id_cnt1)) + p3 <- + betree_Node_apply_messages n1 self.(betree_Internal_right) params + node_id_cnt1 msgs_right st1; + let (st2, p4) := p3 in + let (n3, node_id_cnt2) := p4 in + Return (st2, (Betree_List_Nil, (mkbetree_Internal_t + self.(betree_Internal_id) self.(betree_Internal_pivot) n2 n3, + node_id_cnt2)))) else - Return (mkbetree_Internal_t self.(betree_Internal_id) - self.(betree_Internal_pivot) n1 self.(betree_Internal_right), - node_id_cnt0)) + Return (st1, (msgs_right, (mkbetree_Internal_t + self.(betree_Internal_id) self.(betree_Internal_pivot) n2 + self.(betree_Internal_right), node_id_cnt1)))) else ( - p0 <- - betree_Node_apply_messages_back n0 self.(betree_Internal_right) params + p1 <- + betree_Node_apply_messages n1 self.(betree_Internal_right) params node_id_cnt msgs_right st; - let (n1, node_id_cnt0) := p0 in - Return (mkbetree_Internal_t self.(betree_Internal_id) - self.(betree_Internal_pivot) self.(betree_Internal_left) n1, - node_id_cnt0)) + let (st1, p2) := p1 in + let (n2, node_id_cnt1) := p2 in + Return (st1, (msgs_left, (mkbetree_Internal_t self.(betree_Internal_id) + self.(betree_Internal_pivot) self.(betree_Internal_left) n2, + node_id_cnt1)))) end -(** [betree_main::betree::{betree_main::betree::Node#5}::apply_messages]: forward function +(** [betree_main::betree::{betree_main::betree::Node#5}::apply_messages]: Source: 'src/betree.rs', lines 588:4-593:5 *) with betree_Node_apply_messages (n : nat) (self : betree_Node_t) (params : betree_Params_t) (node_id_cnt : betree_NodeIdCounter_t) (msgs : betree_List_t (u64 * betree_Message_t)) (st : state) : - result (state * unit) + result (state * (betree_Node_t * betree_NodeIdCounter_t)) := match n with | O => Fail_ OutOfFuel - | S n0 => + | S n1 => match self with | Betree_Node_Internal node => p <- betree_load_internal_node node.(betree_Internal_id) st; - let (st0, content) := p in - content0 <- betree_Node_apply_messages_to_internal n0 content msgs; - num_msgs <- betree_List_len (u64 * betree_Message_t) n0 content0; + let (st1, content) := p in + l <- betree_Node_apply_messages_to_internal n1 content msgs; + num_msgs <- betree_List_len (u64 * betree_Message_t) n1 l; if num_msgs s>= params.(betree_Params_min_flush_size) then ( - p0 <- betree_Internal_flush n0 node params node_id_cnt content0 st0; - let (st1, content1) := p0 in - p1 <- - betree_Internal_flush_back n0 node params node_id_cnt content0 st0; - let (node0, _) := p1 in - p2 <- - betree_store_internal_node node0.(betree_Internal_id) content1 st1; - let (st2, _) := p2 in - Return (st2, tt)) + p1 <- betree_Internal_flush n1 node params node_id_cnt l st1; + let (st2, p2) := p1 in + let (content1, p3) := p2 in + let (node1, node_id_cnt1) := p3 in + p4 <- + betree_store_internal_node node1.(betree_Internal_id) content1 st2; + let (st3, _) := p4 in + Return (st3, (Betree_Node_Internal node1, node_id_cnt1))) else ( - p0 <- - betree_store_internal_node node.(betree_Internal_id) content0 st0; - let (st1, _) := p0 in - Return (st1, tt)) - | Betree_Node_Leaf node => - p <- betree_load_leaf_node node.(betree_Leaf_id) st; - let (st0, content) := p in - content0 <- betree_Node_apply_messages_to_leaf n0 content msgs; - len <- betree_List_len (u64 * u64) n0 content0; - i <- u64_mul 2%u64 params.(betree_Params_split_size); - if len s>= i - then ( - p0 <- betree_Leaf_split n0 node content0 params node_id_cnt st0; - let (st1, _) := p0 in - p1 <- betree_store_leaf_node node.(betree_Leaf_id) Betree_List_Nil st1; + p1 <- betree_store_internal_node node.(betree_Internal_id) l st1; let (st2, _) := p1 in - Return (st2, tt)) - else ( - p0 <- betree_store_leaf_node node.(betree_Leaf_id) content0 st0; - let (st1, _) := p0 in - Return (st1, tt)) - end - end - -(** [betree_main::betree::{betree_main::betree::Node#5}::apply_messages]: backward function 0 - Source: 'src/betree.rs', lines 588:4-593:5 *) -with betree_Node_apply_messages_back - (n : nat) (self : betree_Node_t) (params : betree_Params_t) - (node_id_cnt : betree_NodeIdCounter_t) - (msgs : betree_List_t (u64 * betree_Message_t)) (st : state) : - result (betree_Node_t * betree_NodeIdCounter_t) - := - match n with - | O => Fail_ OutOfFuel - | S n0 => - match self with - | Betree_Node_Internal node => - p <- betree_load_internal_node node.(betree_Internal_id) st; - let (st0, content) := p in - content0 <- betree_Node_apply_messages_to_internal n0 content msgs; - num_msgs <- betree_List_len (u64 * betree_Message_t) n0 content0; - if num_msgs s>= params.(betree_Params_min_flush_size) - then ( - p0 <- betree_Internal_flush n0 node params node_id_cnt content0 st0; - let (st1, content1) := p0 in - p1 <- - betree_Internal_flush_back n0 node params node_id_cnt content0 st0; - let (node0, node_id_cnt0) := p1 in - _ <- - betree_store_internal_node node0.(betree_Internal_id) content1 st1; - Return (Betree_Node_Internal node0, node_id_cnt0)) - else ( - _ <- betree_store_internal_node node.(betree_Internal_id) content0 st0; - Return (Betree_Node_Internal node, node_id_cnt)) + Return (st2, (Betree_Node_Internal node, node_id_cnt))) | Betree_Node_Leaf node => p <- betree_load_leaf_node node.(betree_Leaf_id) st; - let (st0, content) := p in - content0 <- betree_Node_apply_messages_to_leaf n0 content msgs; - len <- betree_List_len (u64 * u64) n0 content0; + let (st1, content) := p in + l <- betree_Node_apply_messages_to_leaf n1 content msgs; + len <- betree_List_len (u64 * u64) n1 l; i <- u64_mul 2%u64 params.(betree_Params_split_size); if len s>= i then ( - p0 <- betree_Leaf_split n0 node content0 params node_id_cnt st0; - let (st1, new_node) := p0 in - _ <- betree_store_leaf_node node.(betree_Leaf_id) Betree_List_Nil st1; - node_id_cnt0 <- - betree_Leaf_split_back n0 node content0 params node_id_cnt st0; - Return (Betree_Node_Internal new_node, node_id_cnt0)) + p1 <- betree_Leaf_split n1 node l params node_id_cnt st1; + let (st2, p2) := p1 in + let (new_node, nic) := p2 in + p3 <- betree_store_leaf_node node.(betree_Leaf_id) Betree_List_Nil st2; + let (st3, _) := p3 in + Return (st3, (Betree_Node_Internal new_node, nic))) else ( - _ <- betree_store_leaf_node node.(betree_Leaf_id) content0 st0; - Return (Betree_Node_Leaf + p1 <- betree_store_leaf_node node.(betree_Leaf_id) l st1; + let (st2, _) := p1 in + Return (st2, (Betree_Node_Leaf {| betree_Leaf_id := node.(betree_Leaf_id); betree_Leaf_size := len - |}, node_id_cnt)) + |}, node_id_cnt))) end end . -(** [betree_main::betree::{betree_main::betree::Node#5}::apply]: forward function +(** [betree_main::betree::{betree_main::betree::Node#5}::apply]: Source: 'src/betree.rs', lines 576:4-582:5 *) Definition betree_Node_apply (n : nat) (self : betree_Node_t) (params : betree_Params_t) (node_id_cnt : betree_NodeIdCounter_t) (key : u64) (new_msg : betree_Message_t) (st : state) : - result (state * unit) + result (state * (betree_Node_t * betree_NodeIdCounter_t)) := let l := Betree_List_Nil in p <- betree_Node_apply_messages n self params node_id_cnt (Betree_List_Cons (key, new_msg) l) st; - let (st0, _) := p in - _ <- - betree_Node_apply_messages_back n self params node_id_cnt (Betree_List_Cons - (key, new_msg) l) st; - Return (st0, tt) -. - -(** [betree_main::betree::{betree_main::betree::Node#5}::apply]: backward function 0 - Source: 'src/betree.rs', lines 576:4-582:5 *) -Definition betree_Node_apply_back - (n : nat) (self : betree_Node_t) (params : betree_Params_t) - (node_id_cnt : betree_NodeIdCounter_t) (key : u64) - (new_msg : betree_Message_t) (st : state) : - result (betree_Node_t * betree_NodeIdCounter_t) - := - let l := Betree_List_Nil in - betree_Node_apply_messages_back n self params node_id_cnt (Betree_List_Cons - (key, new_msg) l) st + let (st1, p1) := p in + let (self1, node_id_cnt1) := p1 in + Return (st1, (self1, node_id_cnt1)) . -(** [betree_main::betree::{betree_main::betree::BeTree#6}::new]: forward function +(** [betree_main::betree::{betree_main::betree::BeTree#6}::new]: Source: 'src/betree.rs', lines 849:4-849:60 *) Definition betree_BeTree_new (min_flush_size : u64) (split_size : u64) (st : state) : result (state * betree_BeTree_t) := node_id_cnt <- betree_NodeIdCounter_new; - id <- betree_NodeIdCounter_fresh_id node_id_cnt; - p <- betree_store_leaf_node id Betree_List_Nil st; - let (st0, _) := p in - node_id_cnt0 <- betree_NodeIdCounter_fresh_id_back node_id_cnt; - Return (st0, + p <- betree_NodeIdCounter_fresh_id node_id_cnt; + let (id, nic) := p in + p1 <- betree_store_leaf_node id Betree_List_Nil st; + let (st1, _) := p1 in + Return (st1, {| betree_BeTree_params := {| betree_Params_min_flush_size := min_flush_size; betree_Params_split_size := split_size |}; - betree_BeTree_node_id_cnt := node_id_cnt0; + betree_BeTree_node_id_cnt := nic; betree_BeTree_root := (Betree_Node_Leaf {| betree_Leaf_id := id; betree_Leaf_size := 0%u64 |}) |}) . -(** [betree_main::betree::{betree_main::betree::BeTree#6}::apply]: forward function +(** [betree_main::betree::{betree_main::betree::BeTree#6}::apply]: Source: 'src/betree.rs', lines 868:4-868:47 *) Definition betree_BeTree_apply (n : nat) (self : betree_BeTree_t) (key : u64) (msg : betree_Message_t) (st : state) : - result (state * unit) + result (state * betree_BeTree_t) := p <- betree_Node_apply n self.(betree_BeTree_root) self.(betree_BeTree_params) self.(betree_BeTree_node_id_cnt) key msg st; - let (st0, _) := p in - _ <- - betree_Node_apply_back n self.(betree_BeTree_root) - self.(betree_BeTree_params) self.(betree_BeTree_node_id_cnt) key msg st; - Return (st0, tt) -. - -(** [betree_main::betree::{betree_main::betree::BeTree#6}::apply]: backward function 0 - Source: 'src/betree.rs', lines 868:4-868:47 *) -Definition betree_BeTree_apply_back - (n : nat) (self : betree_BeTree_t) (key : u64) (msg : betree_Message_t) - (st : state) : - result betree_BeTree_t - := - p <- - betree_Node_apply_back n self.(betree_BeTree_root) - self.(betree_BeTree_params) self.(betree_BeTree_node_id_cnt) key msg st; - let (n0, nic) := p in - Return + let (st1, p1) := p in + let (n1, nic) := p1 in + Return (st1, {| betree_BeTree_params := self.(betree_BeTree_params); betree_BeTree_node_id_cnt := nic; - betree_BeTree_root := n0 - |} + betree_BeTree_root := n1 + |}) . -(** [betree_main::betree::{betree_main::betree::BeTree#6}::insert]: forward function +(** [betree_main::betree::{betree_main::betree::BeTree#6}::insert]: Source: 'src/betree.rs', lines 874:4-874:52 *) Definition betree_BeTree_insert (n : nat) (self : betree_BeTree_t) (key : u64) (value : u64) (st : state) : - result (state * unit) - := - p <- betree_BeTree_apply n self key (Betree_Message_Insert value) st; - let (st0, _) := p in - _ <- betree_BeTree_apply_back n self key (Betree_Message_Insert value) st; - Return (st0, tt) -. - -(** [betree_main::betree::{betree_main::betree::BeTree#6}::insert]: backward function 0 - Source: 'src/betree.rs', lines 874:4-874:52 *) -Definition betree_BeTree_insert_back - (n : nat) (self : betree_BeTree_t) (key : u64) (value : u64) (st : state) : - result betree_BeTree_t + result (state * betree_BeTree_t) := - betree_BeTree_apply_back n self key (Betree_Message_Insert value) st + betree_BeTree_apply n self key (Betree_Message_Insert value) st . -(** [betree_main::betree::{betree_main::betree::BeTree#6}::delete]: forward function +(** [betree_main::betree::{betree_main::betree::BeTree#6}::delete]: Source: 'src/betree.rs', lines 880:4-880:38 *) Definition betree_BeTree_delete (n : nat) (self : betree_BeTree_t) (key : u64) (st : state) : - result (state * unit) - := - p <- betree_BeTree_apply n self key Betree_Message_Delete st; - let (st0, _) := p in - _ <- betree_BeTree_apply_back n self key Betree_Message_Delete st; - Return (st0, tt) -. - -(** [betree_main::betree::{betree_main::betree::BeTree#6}::delete]: backward function 0 - Source: 'src/betree.rs', lines 880:4-880:38 *) -Definition betree_BeTree_delete_back - (n : nat) (self : betree_BeTree_t) (key : u64) (st : state) : - result betree_BeTree_t + result (state * betree_BeTree_t) := - betree_BeTree_apply_back n self key Betree_Message_Delete st + betree_BeTree_apply n self key Betree_Message_Delete st . -(** [betree_main::betree::{betree_main::betree::BeTree#6}::upsert]: forward function +(** [betree_main::betree::{betree_main::betree::BeTree#6}::upsert]: Source: 'src/betree.rs', lines 886:4-886:59 *) Definition betree_BeTree_upsert (n : nat) (self : betree_BeTree_t) (key : u64) (upd : betree_UpsertFunState_t) (st : state) : - result (state * unit) - := - p <- betree_BeTree_apply n self key (Betree_Message_Upsert upd) st; - let (st0, _) := p in - _ <- betree_BeTree_apply_back n self key (Betree_Message_Upsert upd) st; - Return (st0, tt) -. - -(** [betree_main::betree::{betree_main::betree::BeTree#6}::upsert]: backward function 0 - Source: 'src/betree.rs', lines 886:4-886:59 *) -Definition betree_BeTree_upsert_back - (n : nat) (self : betree_BeTree_t) (key : u64) - (upd : betree_UpsertFunState_t) (st : state) : - result betree_BeTree_t + result (state * betree_BeTree_t) := - betree_BeTree_apply_back n self key (Betree_Message_Upsert upd) st + betree_BeTree_apply n self key (Betree_Message_Upsert upd) st . -(** [betree_main::betree::{betree_main::betree::BeTree#6}::lookup]: forward function +(** [betree_main::betree::{betree_main::betree::BeTree#6}::lookup]: Source: 'src/betree.rs', lines 895:4-895:62 *) Definition betree_BeTree_lookup (n : nat) (self : betree_BeTree_t) (key : u64) (st : state) : - result (state * (option u64)) - := - betree_Node_lookup n self.(betree_BeTree_root) key st -. - -(** [betree_main::betree::{betree_main::betree::BeTree#6}::lookup]: backward function 0 - Source: 'src/betree.rs', lines 895:4-895:62 *) -Definition betree_BeTree_lookup_back - (n : nat) (self : betree_BeTree_t) (key : u64) (st : state) : - result betree_BeTree_t + result (state * ((option u64) * betree_BeTree_t)) := - n0 <- betree_Node_lookup_back n self.(betree_BeTree_root) key st; - Return + p <- betree_Node_lookup n self.(betree_BeTree_root) key st; + let (st1, p1) := p in + let (o, n1) := p1 in + Return (st1, (o, {| betree_BeTree_params := self.(betree_BeTree_params); betree_BeTree_node_id_cnt := self.(betree_BeTree_node_id_cnt); - betree_BeTree_root := n0 - |} + betree_BeTree_root := n1 + |})) . -(** [betree_main::main]: forward function +(** [betree_main::main]: Source: 'src/betree_main.rs', lines 5:0-5:9 *) Definition main : result unit := Return tt. -- cgit v1.2.3 From a4decc7654bc6f3301c0174124d21fdbc2dbc708 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Sat, 23 Dec 2023 00:59:55 +0100 Subject: Regenerate the files --- tests/coq/betree/BetreeMain_Funs.v | 40 ++++++++++---------------------------- 1 file changed, 10 insertions(+), 30 deletions(-) (limited to 'tests/coq/betree/BetreeMain_Funs.v') diff --git a/tests/coq/betree/BetreeMain_Funs.v b/tests/coq/betree/BetreeMain_Funs.v index 516bc7b7..cefab0f4 100644 --- a/tests/coq/betree/BetreeMain_Funs.v +++ b/tests/coq/betree/BetreeMain_Funs.v @@ -123,8 +123,7 @@ Fixpoint betree_List_split_at i <- u64_sub n1 1%u64; p <- betree_List_split_at T n2 tl i; let (ls0, ls1) := p in - let l := ls0 in - Return (Betree_List_Cons hd l, ls1) + Return (Betree_List_Cons hd ls0, ls1) | Betree_List_Nil => Fail_ Failure end end @@ -135,8 +134,7 @@ Fixpoint betree_List_split_at 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 - let l := tl in - Return (Betree_List_Cons x l) + Return (Betree_List_Cons x tl) . (** [betree_main::betree::{betree_main::betree::List#1}::pop_front]: @@ -186,8 +184,7 @@ Fixpoint betree_ListTupleU64T_partition_at_pivot else ( p <- betree_ListTupleU64T_partition_at_pivot T n1 tl pivot; let (ls0, ls1) := p in - let l := ls0 in - Return (Betree_List_Cons (i, t) l, ls1)) + Return (Betree_List_Cons (i, t) ls0, ls1)) | Betree_List_Nil => Return (Betree_List_Nil, Betree_List_Nil) end end @@ -242,10 +239,7 @@ Fixpoint betree_Node_lookup_first_message_for_key | Betree_List_Cons x next_msgs => let (i, m) := x in if i s>= key - then - let back_'a := - fun (ret : betree_List_t (u64 * betree_Message_t)) => Return ret in - Return (Betree_List_Cons (i, m) next_msgs, back_'a) + then Return (Betree_List_Cons (i, m) next_msgs, Return) else ( p <- betree_Node_lookup_first_message_for_key n1 key next_msgs; let (l, lookup_first_message_for_key_back) := p in @@ -254,10 +248,7 @@ Fixpoint betree_Node_lookup_first_message_for_key next_msgs1 <- lookup_first_message_for_key_back ret; Return (Betree_List_Cons (i, m) next_msgs1) in Return (l, back_'a)) - | Betree_List_Nil => - let back_'a := - fun (ret : betree_List_t (u64 * betree_Message_t)) => Return ret in - Return (Betree_List_Nil, back_'a) + | Betree_List_Nil => Return (Betree_List_Nil, Return) end end . @@ -456,14 +447,8 @@ Fixpoint betree_Node_lookup_first_message_after_key next_msgs1 <- lookup_first_message_after_key_back ret; Return (Betree_List_Cons (k, m) next_msgs1) in Return (l, back_'a)) - else - let back_'a := - fun (ret : betree_List_t (u64 * betree_Message_t)) => Return ret in - Return (Betree_List_Cons (k, m) next_msgs, back_'a) - | Betree_List_Nil => - let back_'a := - fun (ret : betree_List_t (u64 * betree_Message_t)) => Return ret in - Return (Betree_List_Nil, back_'a) + else Return (Betree_List_Cons (k, m) next_msgs, Return) + | Betree_List_Nil => Return (Betree_List_Nil, Return) end end . @@ -562,9 +547,7 @@ Fixpoint betree_Node_lookup_mut_in_bindings | Betree_List_Cons hd tl => let (i, i1) := hd in if i s>= key - then - let back_'a := fun (ret : betree_List_t (u64 * u64)) => Return ret in - Return (Betree_List_Cons (i, i1) tl, back_'a) + then Return (Betree_List_Cons (i, i1) tl, Return) else ( p <- betree_Node_lookup_mut_in_bindings n1 key tl; let (l, lookup_mut_in_bindings_back) := p in @@ -573,9 +556,7 @@ Fixpoint betree_Node_lookup_mut_in_bindings tl1 <- lookup_mut_in_bindings_back ret; Return (Betree_List_Cons (i, i1) tl1) in Return (l, back_'a)) - | Betree_List_Nil => - let back_'a := fun (ret : betree_List_t (u64 * u64)) => Return ret in - Return (Betree_List_Nil, back_'a) + | Betree_List_Nil => Return (Betree_List_Nil, Return) end end . @@ -751,10 +732,9 @@ Definition betree_Node_apply (new_msg : betree_Message_t) (st : state) : result (state * (betree_Node_t * betree_NodeIdCounter_t)) := - let l := Betree_List_Nil in p <- betree_Node_apply_messages n self params node_id_cnt (Betree_List_Cons - (key, new_msg) l) st; + (key, new_msg) Betree_List_Nil) st; let (st1, p1) := p in let (self1, node_id_cnt1) := p1 in Return (st1, (self1, node_id_cnt1)) -- cgit v1.2.3