diff options
Diffstat (limited to 'tests/lean/betree/BetreeMain')
| -rw-r--r-- | tests/lean/betree/BetreeMain/Clauses/Template.lean | 185 | ||||
| -rw-r--r-- | tests/lean/betree/BetreeMain/Funs.lean | 1222 | ||||
| -rw-r--r-- | tests/lean/betree/BetreeMain/Opaque.lean | 33 | ||||
| -rw-r--r-- | tests/lean/betree/BetreeMain/Types.lean | 61 |
4 files changed, 1501 insertions, 0 deletions
diff --git a/tests/lean/betree/BetreeMain/Clauses/Template.lean b/tests/lean/betree/BetreeMain/Clauses/Template.lean new file mode 100644 index 00000000..1d18174e --- /dev/null +++ b/tests/lean/betree/BetreeMain/Clauses/Template.lean @@ -0,0 +1,185 @@ +-- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS +-- [betree_main]: templates for the decreases clauses +import Base.Primitives +import BetreeMain.Types + +/- [betree_main::betree::List::{1}::len]: termination measure -/ +@[simp] +def betree_list_len_terminates (T : Type) (self : betree_list_t T) := self + +/- [betree_main::betree::List::{1}::len]: decreases_by tactic -/ +syntax "betree_list_len_decreases" term+ : tactic +macro_rules +| `(tactic| betree_list_len_decreases $self) =>`(tactic| sorry) + +/- [betree_main::betree::List::{1}::split_at]: termination measure -/ +@[simp] +def betree_list_split_at_terminates (T : Type) (self : betree_list_t T) + (n : UInt64) := + (self, n) + +/- [betree_main::betree::List::{1}::split_at]: decreases_by tactic -/ +syntax "betree_list_split_at_decreases" term+ : tactic +macro_rules +| `(tactic| betree_list_split_at_decreases $self $n) =>`(tactic| sorry) + +/- [betree_main::betree::List::{2}::partition_at_pivot]: termination measure -/ +@[simp] +def betree_list_partition_at_pivot_terminates (T : Type) + (self : betree_list_t (UInt64 × T)) (pivot : UInt64) := + (self, pivot) + +/- [betree_main::betree::List::{2}::partition_at_pivot]: decreases_by tactic -/ +syntax "betree_list_partition_at_pivot_decreases" term+ : tactic +macro_rules +| `(tactic| betree_list_partition_at_pivot_decreases $self $pivot) => + `(tactic| sorry) + +/- [betree_main::betree::Node::{5}::lookup_in_bindings]: termination measure -/ +@[simp] +def betree_node_lookup_in_bindings_terminates (key : UInt64) + (bindings : betree_list_t (UInt64 × UInt64)) := + (key, bindings) + +/- [betree_main::betree::Node::{5}::lookup_in_bindings]: decreases_by tactic -/ +syntax "betree_node_lookup_in_bindings_decreases" term+ : tactic +macro_rules +| `(tactic| betree_node_lookup_in_bindings_decreases $key $bindings) => + `(tactic| sorry) + +/- [betree_main::betree::Node::{5}::lookup_first_message_for_key]: termination measure -/ +@[simp] +def betree_node_lookup_first_message_for_key_terminates (key : UInt64) + (msgs : betree_list_t (UInt64 × betree_message_t)) := + (key, msgs) + +/- [betree_main::betree::Node::{5}::lookup_first_message_for_key]: decreases_by tactic -/ +syntax "betree_node_lookup_first_message_for_key_decreases" term+ : tactic +macro_rules +| `(tactic| betree_node_lookup_first_message_for_key_decreases $key $msgs) => + `(tactic| sorry) + +/- [betree_main::betree::Node::{5}::apply_upserts]: termination measure -/ +@[simp] +def betree_node_apply_upserts_terminates + (msgs : betree_list_t (UInt64 × betree_message_t)) (prev : Option UInt64) + (key : UInt64) (st : State) := + (msgs, prev, key, st) + +/- [betree_main::betree::Node::{5}::apply_upserts]: decreases_by tactic -/ +syntax "betree_node_apply_upserts_decreases" term+ : tactic +macro_rules +| `(tactic| betree_node_apply_upserts_decreases $msgs $prev $key $st) => + `(tactic| sorry) + +/- [betree_main::betree::Node::{5}::lookup]: termination measure -/ +@[simp] +def betree_node_lookup_terminates (self : betree_node_t) (key : UInt64) + (st : State) := + (self, key, st) + +/- [betree_main::betree::Node::{5}::lookup]: decreases_by tactic -/ +syntax "betree_node_lookup_decreases" term+ : tactic +macro_rules +| `(tactic| betree_node_lookup_decreases $self $key $st) =>`(tactic| sorry) + +/- [betree_main::betree::Internal::{4}::lookup_in_children]: termination measure -/ +@[simp] +def betree_internal_lookup_in_children_terminates (self : betree_internal_t) + (key : UInt64) (st : State) := + (self, key, st) + +/- [betree_main::betree::Internal::{4}::lookup_in_children]: decreases_by tactic -/ +syntax "betree_internal_lookup_in_children_decreases" term+ : tactic +macro_rules +| `(tactic| betree_internal_lookup_in_children_decreases $self $key $st) => + `(tactic| sorry) + +/- [betree_main::betree::Node::{5}::lookup_mut_in_bindings]: termination measure -/ +@[simp] +def betree_node_lookup_mut_in_bindings_terminates (key : UInt64) + (bindings : betree_list_t (UInt64 × UInt64)) := + (key, bindings) + +/- [betree_main::betree::Node::{5}::lookup_mut_in_bindings]: decreases_by tactic -/ +syntax "betree_node_lookup_mut_in_bindings_decreases" term+ : tactic +macro_rules +| `(tactic| betree_node_lookup_mut_in_bindings_decreases $key $bindings) => + `(tactic| sorry) + +/- [betree_main::betree::Node::{5}::apply_messages_to_leaf]: termination measure -/ +@[simp] +def betree_node_apply_messages_to_leaf_terminates + (bindings : betree_list_t (UInt64 × UInt64)) + (new_msgs : betree_list_t (UInt64 × betree_message_t)) := + (bindings, new_msgs) + +/- [betree_main::betree::Node::{5}::apply_messages_to_leaf]: decreases_by tactic -/ +syntax "betree_node_apply_messages_to_leaf_decreases" term+ : tactic +macro_rules +| `(tactic| betree_node_apply_messages_to_leaf_decreases $bindings +$new_msgs) =>`(tactic| sorry) + +/- [betree_main::betree::Node::{5}::filter_messages_for_key]: termination measure -/ +@[simp] +def betree_node_filter_messages_for_key_terminates (key : UInt64) + (msgs : betree_list_t (UInt64 × betree_message_t)) := + (key, msgs) + +/- [betree_main::betree::Node::{5}::filter_messages_for_key]: decreases_by tactic -/ +syntax "betree_node_filter_messages_for_key_decreases" term+ : tactic +macro_rules +| `(tactic| betree_node_filter_messages_for_key_decreases $key $msgs) => + `(tactic| sorry) + +/- [betree_main::betree::Node::{5}::lookup_first_message_after_key]: termination measure -/ +@[simp] +def betree_node_lookup_first_message_after_key_terminates (key : UInt64) + (msgs : betree_list_t (UInt64 × betree_message_t)) := + (key, msgs) + +/- [betree_main::betree::Node::{5}::lookup_first_message_after_key]: decreases_by tactic -/ +syntax "betree_node_lookup_first_message_after_key_decreases" term+ : tactic +macro_rules +| `(tactic| betree_node_lookup_first_message_after_key_decreases $key $msgs) => + `(tactic| sorry) + +/- [betree_main::betree::Node::{5}::apply_messages_to_internal]: termination measure -/ +@[simp] +def betree_node_apply_messages_to_internal_terminates + (msgs : betree_list_t (UInt64 × betree_message_t)) + (new_msgs : betree_list_t (UInt64 × betree_message_t)) := + (msgs, new_msgs) + +/- [betree_main::betree::Node::{5}::apply_messages_to_internal]: decreases_by tactic -/ +syntax "betree_node_apply_messages_to_internal_decreases" term+ : tactic +macro_rules +| `(tactic| betree_node_apply_messages_to_internal_decreases $msgs +$new_msgs) =>`(tactic| sorry) + +/- [betree_main::betree::Node::{5}::apply_messages]: termination measure -/ +@[simp] +def betree_node_apply_messages_terminates (self : betree_node_t) + (params : betree_params_t) (node_id_cnt : betree_node_id_counter_t) + (msgs : betree_list_t (UInt64 × betree_message_t)) (st : State) := + (self, params, node_id_cnt, msgs, st) + +/- [betree_main::betree::Node::{5}::apply_messages]: decreases_by tactic -/ +syntax "betree_node_apply_messages_decreases" term+ : tactic +macro_rules +| `(tactic| betree_node_apply_messages_decreases $self $params $node_id_cnt +$msgs $st) =>`(tactic| sorry) + +/- [betree_main::betree::Internal::{4}::flush]: termination measure -/ +@[simp] +def betree_internal_flush_terminates (self : betree_internal_t) + (params : betree_params_t) (node_id_cnt : betree_node_id_counter_t) + (content : betree_list_t (UInt64 × betree_message_t)) (st : State) := + (self, params, node_id_cnt, content, st) + +/- [betree_main::betree::Internal::{4}::flush]: decreases_by tactic -/ +syntax "betree_internal_flush_decreases" term+ : tactic +macro_rules +| `(tactic| betree_internal_flush_decreases $self $params $node_id_cnt $content +$st) =>`(tactic| sorry) + diff --git a/tests/lean/betree/BetreeMain/Funs.lean b/tests/lean/betree/BetreeMain/Funs.lean new file mode 100644 index 00000000..e40ca4ca --- /dev/null +++ b/tests/lean/betree/BetreeMain/Funs.lean @@ -0,0 +1,1222 @@ +-- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS +-- [betree_main]: function definitions +import Base.Primitives +import BetreeMain.Types +import BetreeMain.Opaque +import BetreeMain.Clauses.Clauses + +section variable (opaque_defs: OpaqueDefs) + +/- [betree_main::betree::load_internal_node] -/ +def betree_load_internal_node_fwd + (id : UInt64) (st : State) : + Result (State × (betree_list_t (UInt64 × betree_message_t))) + := + opaque_defs.betree_utils_load_internal_node_fwd id st + +/- [betree_main::betree::store_internal_node] -/ +def betree_store_internal_node_fwd + (id : UInt64) (content : betree_list_t (UInt64 × betree_message_t)) + (st : State) : + Result (State × Unit) + := + do + let (st0, _) ← + opaque_defs.betree_utils_store_internal_node_fwd id content st + Result.ret (st0, ()) + +/- [betree_main::betree::load_leaf_node] -/ +def betree_load_leaf_node_fwd + (id : UInt64) (st : State) : + Result (State × (betree_list_t (UInt64 × UInt64))) + := + opaque_defs.betree_utils_load_leaf_node_fwd id st + +/- [betree_main::betree::store_leaf_node] -/ +def betree_store_leaf_node_fwd + (id : UInt64) (content : betree_list_t (UInt64 × UInt64)) (st : State) : + Result (State × Unit) + := + do + let (st0, _) ← opaque_defs.betree_utils_store_leaf_node_fwd id content st + Result.ret (st0, ()) + +/- [betree_main::betree::fresh_node_id] -/ +def betree_fresh_node_id_fwd (counter : UInt64) : Result UInt64 := + do + let _ ← UInt64.checked_add counter (UInt64.ofNatCore 1 (by intlit)) + Result.ret counter + +/- [betree_main::betree::fresh_node_id] -/ +def betree_fresh_node_id_back (counter : UInt64) : Result UInt64 := + UInt64.checked_add counter (UInt64.ofNatCore 1 (by intlit)) + +/- [betree_main::betree::NodeIdCounter::{0}::new] -/ +def betree_node_id_counter_new_fwd : Result betree_node_id_counter_t := + Result.ret + { betree_node_id_counter_next_node_id := (UInt64.ofNatCore 0 (by intlit)) } + +/- [betree_main::betree::NodeIdCounter::{0}::fresh_id] -/ +def betree_node_id_counter_fresh_id_fwd + (self : betree_node_id_counter_t) : Result UInt64 := + do + let _ ← UInt64.checked_add self.betree_node_id_counter_next_node_id + (UInt64.ofNatCore 1 (by intlit)) + Result.ret self.betree_node_id_counter_next_node_id + +/- [betree_main::betree::NodeIdCounter::{0}::fresh_id] -/ +def betree_node_id_counter_fresh_id_back + (self : betree_node_id_counter_t) : Result betree_node_id_counter_t := + do + let i ← UInt64.checked_add self.betree_node_id_counter_next_node_id + (UInt64.ofNatCore 1 (by intlit)) + Result.ret { betree_node_id_counter_next_node_id := i } + +/- [core::num::u64::{10}::MAX] -/ +def core_num_u64_max_body : Result UInt64 := + Result.ret (UInt64.ofNatCore 18446744073709551615 (by intlit)) +def core_num_u64_max_c : UInt64 := eval_global core_num_u64_max_body (by simp) + +/- [betree_main::betree::upsert_update] -/ +def betree_upsert_update_fwd + (prev : Option UInt64) (st : betree_upsert_fun_state_t) : Result UInt64 := + match h: prev with + | Option.none => + match h: st with + | betree_upsert_fun_state_t.BetreeUpsertFunStateAdd v => Result.ret v + | betree_upsert_fun_state_t.BetreeUpsertFunStateSub i => + Result.ret (UInt64.ofNatCore 0 (by intlit)) + | Option.some prev0 => + match h: st with + | betree_upsert_fun_state_t.BetreeUpsertFunStateAdd v => + do + let margin ← UInt64.checked_sub core_num_u64_max_c prev0 + if h: margin >= v + then UInt64.checked_add prev0 v + else Result.ret core_num_u64_max_c + | betree_upsert_fun_state_t.BetreeUpsertFunStateSub v => + if h: prev0 >= v + then UInt64.checked_sub prev0 v + else Result.ret (UInt64.ofNatCore 0 (by intlit)) + +/- [betree_main::betree::List::{1}::len] -/ +def betree_list_len_fwd + (T : Type) (self : betree_list_t T) : (Result UInt64) := + match h: self with + | betree_list_t.BetreeListCons t tl => + do + let i ← betree_list_len_fwd T tl + UInt64.checked_add (UInt64.ofNatCore 1 (by intlit)) i + | betree_list_t.BetreeListNil => Result.ret (UInt64.ofNatCore 0 (by intlit)) +termination_by betree_list_len_fwd self => betree_list_len_terminates T self +decreasing_by betree_list_len_decreases self + +/- [betree_main::betree::List::{1}::split_at] -/ +def betree_list_split_at_fwd + (T : Type) (self : betree_list_t T) (n : UInt64) : + (Result ((betree_list_t T) × (betree_list_t T))) + := + if h: n = (UInt64.ofNatCore 0 (by intlit)) + then Result.ret (betree_list_t.BetreeListNil, self) + else + match h: self with + | betree_list_t.BetreeListCons hd tl => + do + let i ← UInt64.checked_sub n (UInt64.ofNatCore 1 (by intlit)) + let p ← betree_list_split_at_fwd T tl i + let (ls0, ls1) := p + let l := ls0 + Result.ret (betree_list_t.BetreeListCons hd l, ls1) + | betree_list_t.BetreeListNil => Result.fail Error.panic +termination_by betree_list_split_at_fwd self n => + betree_list_split_at_terminates T self n +decreasing_by betree_list_split_at_decreases self n + +/- [betree_main::betree::List::{1}::push_front] -/ +def betree_list_push_front_fwd_back + (T : Type) (self : betree_list_t T) (x : T) : Result (betree_list_t T) := + let tl := mem_replace_fwd (betree_list_t T) self betree_list_t.BetreeListNil + let l := tl + Result.ret (betree_list_t.BetreeListCons x l) + +/- [betree_main::betree::List::{1}::pop_front] -/ +def betree_list_pop_front_fwd (T : Type) (self : betree_list_t T) : Result T := + let ls := mem_replace_fwd (betree_list_t T) self betree_list_t.BetreeListNil + match h: ls with + | betree_list_t.BetreeListCons x tl => Result.ret x + | betree_list_t.BetreeListNil => Result.fail Error.panic + +/- [betree_main::betree::List::{1}::pop_front] -/ +def betree_list_pop_front_back + (T : Type) (self : betree_list_t T) : Result (betree_list_t T) := + let ls := mem_replace_fwd (betree_list_t T) self betree_list_t.BetreeListNil + match h: ls with + | betree_list_t.BetreeListCons x tl => Result.ret tl + | betree_list_t.BetreeListNil => Result.fail Error.panic + +/- [betree_main::betree::List::{1}::hd] -/ +def betree_list_hd_fwd (T : Type) (self : betree_list_t T) : Result T := + match h: self with + | betree_list_t.BetreeListCons hd l => Result.ret hd + | betree_list_t.BetreeListNil => Result.fail Error.panic + +/- [betree_main::betree::List::{2}::head_has_key] -/ +def betree_list_head_has_key_fwd + (T : Type) (self : betree_list_t (UInt64 × T)) (key : UInt64) : + Result Bool + := + match h: self with + | betree_list_t.BetreeListCons hd l => let (i, _) := hd + Result.ret (i = key) + | betree_list_t.BetreeListNil => Result.ret false + +/- [betree_main::betree::List::{2}::partition_at_pivot] -/ +def betree_list_partition_at_pivot_fwd + (T : Type) (self : betree_list_t (UInt64 × T)) (pivot : UInt64) : + (Result ((betree_list_t (UInt64 × T)) × (betree_list_t (UInt64 × T)))) + := + match h: self with + | betree_list_t.BetreeListCons hd tl => + let (i, t) := hd + if h: i >= pivot + then + Result.ret (betree_list_t.BetreeListNil, betree_list_t.BetreeListCons (i, + t) tl) + else + do + let p ← betree_list_partition_at_pivot_fwd T tl pivot + let (ls0, ls1) := p + let l := ls0 + Result.ret (betree_list_t.BetreeListCons (i, t) l, ls1) + | betree_list_t.BetreeListNil => + Result.ret (betree_list_t.BetreeListNil, betree_list_t.BetreeListNil) +termination_by betree_list_partition_at_pivot_fwd self pivot => + betree_list_partition_at_pivot_terminates T self pivot +decreasing_by betree_list_partition_at_pivot_decreases self pivot + +/- [betree_main::betree::Leaf::{3}::split] -/ +def betree_leaf_split_fwd + (self : betree_leaf_t) (content : betree_list_t (UInt64 × UInt64)) + (params : betree_params_t) (node_id_cnt : betree_node_id_counter_t) + (st : State) : + Result (State × betree_internal_t) + := + do + let p ← + betree_list_split_at_fwd (UInt64 × UInt64) content + params.betree_params_split_size + let (content0, content1) := p + let p0 ← betree_list_hd_fwd (UInt64 × UInt64) content1 + let (pivot, _) := p0 + let id0 ← betree_node_id_counter_fresh_id_fwd node_id_cnt + let node_id_cnt0 ← betree_node_id_counter_fresh_id_back node_id_cnt + let id1 ← betree_node_id_counter_fresh_id_fwd node_id_cnt0 + let (st0, _) ← betree_store_leaf_node_fwd id0 content0 st + let (st1, _) ← betree_store_leaf_node_fwd id1 content1 st0 + let n := betree_node_t.BetreeNodeLeaf + { + betree_leaf_id := id0, + betree_leaf_size := params.betree_params_split_size + } + let n0 := betree_node_t.BetreeNodeLeaf + { + betree_leaf_id := id1, + betree_leaf_size := params.betree_params_split_size + } + Result.ret (st1, + { + betree_internal_id := self.betree_leaf_id, + betree_internal_pivot := pivot, + betree_internal_left := n, + betree_internal_right := n0 + }) + +/- [betree_main::betree::Leaf::{3}::split] -/ +def betree_leaf_split_back + (self : betree_leaf_t) (content : betree_list_t (UInt64 × UInt64)) + (params : betree_params_t) (node_id_cnt : betree_node_id_counter_t) + (st : State) : + Result betree_node_id_counter_t + := + do + let p ← + betree_list_split_at_fwd (UInt64 × UInt64) content + params.betree_params_split_size + let (content0, content1) := p + let _ ← betree_list_hd_fwd (UInt64 × UInt64) content1 + let id0 ← betree_node_id_counter_fresh_id_fwd node_id_cnt + let node_id_cnt0 ← betree_node_id_counter_fresh_id_back node_id_cnt + let id1 ← betree_node_id_counter_fresh_id_fwd node_id_cnt0 + let (st0, _) ← betree_store_leaf_node_fwd id0 content0 st + let _ ← betree_store_leaf_node_fwd id1 content1 st0 + betree_node_id_counter_fresh_id_back node_id_cnt0 + +/- [betree_main::betree::Node::{5}::lookup_in_bindings] -/ +def betree_node_lookup_in_bindings_fwd + (key : UInt64) (bindings : betree_list_t (UInt64 × UInt64)) : + (Result (Option UInt64)) + := + match h: bindings with + | betree_list_t.BetreeListCons hd tl => + let (i, i0) := hd + if h: i = key + then Result.ret (Option.some i0) + else + if h: i > key + then Result.ret Option.none + else betree_node_lookup_in_bindings_fwd key tl + | betree_list_t.BetreeListNil => Result.ret Option.none +termination_by betree_node_lookup_in_bindings_fwd key bindings => + betree_node_lookup_in_bindings_terminates key bindings +decreasing_by betree_node_lookup_in_bindings_decreases key bindings + +/- [betree_main::betree::Node::{5}::lookup_first_message_for_key] -/ +def betree_node_lookup_first_message_for_key_fwd + (key : UInt64) (msgs : betree_list_t (UInt64 × betree_message_t)) : + (Result (betree_list_t (UInt64 × betree_message_t))) + := + match h: msgs with + | betree_list_t.BetreeListCons x next_msgs => + let (i, m) := x + if h: i >= key + then Result.ret (betree_list_t.BetreeListCons (i, m) next_msgs) + else betree_node_lookup_first_message_for_key_fwd key next_msgs + | betree_list_t.BetreeListNil => Result.ret betree_list_t.BetreeListNil +termination_by betree_node_lookup_first_message_for_key_fwd key msgs => + betree_node_lookup_first_message_for_key_terminates key msgs +decreasing_by betree_node_lookup_first_message_for_key_decreases key msgs + +/- [betree_main::betree::Node::{5}::lookup_first_message_for_key] -/ +def betree_node_lookup_first_message_for_key_back + (key : UInt64) (msgs : betree_list_t (UInt64 × betree_message_t)) + (ret0 : betree_list_t (UInt64 × betree_message_t)) : + (Result (betree_list_t (UInt64 × betree_message_t))) + := + match h: msgs with + | betree_list_t.BetreeListCons x next_msgs => + let (i, m) := x + if h: i >= key + then Result.ret ret0 + else + do + let next_msgs0 ← + betree_node_lookup_first_message_for_key_back key next_msgs ret0 + Result.ret (betree_list_t.BetreeListCons (i, m) next_msgs0) + | betree_list_t.BetreeListNil => Result.ret ret0 +termination_by betree_node_lookup_first_message_for_key_back key msgs ret0 => + betree_node_lookup_first_message_for_key_terminates key msgs +decreasing_by betree_node_lookup_first_message_for_key_decreases key msgs + +/- [betree_main::betree::Node::{5}::apply_upserts] -/ +def betree_node_apply_upserts_fwd + (msgs : betree_list_t (UInt64 × betree_message_t)) (prev : Option UInt64) + (key : UInt64) (st : State) : + (Result (State × UInt64)) + := + do + let b ← betree_list_head_has_key_fwd betree_message_t msgs key + if h: b + then + do + let msg ← betree_list_pop_front_fwd (UInt64 × betree_message_t) msgs + let (_, m) := msg + match h: m with + | betree_message_t.BetreeMessageInsert i => Result.fail Error.panic + | betree_message_t.BetreeMessageDelete => Result.fail Error.panic + | betree_message_t.BetreeMessageUpsert s => + do + let v ← betree_upsert_update_fwd prev s + let msgs0 ← + betree_list_pop_front_back (UInt64 × betree_message_t) msgs + betree_node_apply_upserts_fwd msgs0 (Option.some v) key st + else + do + let (st0, v) ← + opaque_defs.core_option_option_unwrap_fwd UInt64 prev st + let _ ← + betree_list_push_front_fwd_back (UInt64 × betree_message_t) msgs + (key, betree_message_t.BetreeMessageInsert v) + Result.ret (st0, v) +termination_by betree_node_apply_upserts_fwd msgs prev key st => + betree_node_apply_upserts_terminates msgs prev key st +decreasing_by betree_node_apply_upserts_decreases msgs prev key st + +/- [betree_main::betree::Node::{5}::apply_upserts] -/ +def betree_node_apply_upserts_back + (msgs : betree_list_t (UInt64 × betree_message_t)) (prev : Option UInt64) + (key : UInt64) (st : State) : + (Result (betree_list_t (UInt64 × betree_message_t))) + := + do + let b ← betree_list_head_has_key_fwd betree_message_t msgs key + if h: b + then + do + let msg ← betree_list_pop_front_fwd (UInt64 × betree_message_t) msgs + let (_, m) := msg + match h: m with + | betree_message_t.BetreeMessageInsert i => Result.fail Error.panic + | betree_message_t.BetreeMessageDelete => Result.fail Error.panic + | betree_message_t.BetreeMessageUpsert s => + do + let v ← betree_upsert_update_fwd prev s + let msgs0 ← + betree_list_pop_front_back (UInt64 × betree_message_t) msgs + betree_node_apply_upserts_back msgs0 (Option.some v) key st + else + do + let (_, v) ← opaque_defs.core_option_option_unwrap_fwd UInt64 prev st + betree_list_push_front_fwd_back (UInt64 × betree_message_t) msgs (key, + betree_message_t.BetreeMessageInsert v) +termination_by betree_node_apply_upserts_back msgs prev key st => + betree_node_apply_upserts_terminates msgs prev key st +decreasing_by betree_node_apply_upserts_decreases msgs prev key st + +/- [betree_main::betree::Node::{5}::lookup] -/ +mutual def betree_node_lookup_fwd + (self : betree_node_t) (key : UInt64) (st : State) : + (Result (State × (Option UInt64))) + := + match h: self with + | betree_node_t.BetreeNodeInternal node => + do + let (st0, msgs) ← + betree_load_internal_node_fwd node.betree_internal_id st + let pending ← betree_node_lookup_first_message_for_key_fwd key msgs + match h: pending with + | betree_list_t.BetreeListCons p l => + let (k, msg) := p + if h: k != key + then + do + let (st1, opt) ← + betree_internal_lookup_in_children_fwd node key st0 + let _ ← + betree_node_lookup_first_message_for_key_back key msgs + (betree_list_t.BetreeListCons (k, msg) l) + Result.ret (st1, opt) + else + match h: msg with + | betree_message_t.BetreeMessageInsert v => + do + let _ ← + betree_node_lookup_first_message_for_key_back key msgs + (betree_list_t.BetreeListCons (k, + betree_message_t.BetreeMessageInsert v) l) + Result.ret (st0, Option.some v) + | betree_message_t.BetreeMessageDelete => + do + let _ ← + betree_node_lookup_first_message_for_key_back key msgs + (betree_list_t.BetreeListCons (k, + betree_message_t.BetreeMessageDelete) l) + Result.ret (st0, Option.none) + | betree_message_t.BetreeMessageUpsert ufs => + do + let (st1, v) ← + betree_internal_lookup_in_children_fwd node key st0 + let (st2, v0) ← + betree_node_apply_upserts_fwd (betree_list_t.BetreeListCons (k, + betree_message_t.BetreeMessageUpsert ufs) l) v key st1 + let node0 ← + betree_internal_lookup_in_children_back node key st0 + let pending0 ← + betree_node_apply_upserts_back (betree_list_t.BetreeListCons + (k, betree_message_t.BetreeMessageUpsert ufs) l) v key st1 + let msgs0 ← + betree_node_lookup_first_message_for_key_back key msgs pending0 + let (st3, _) ← + betree_store_internal_node_fwd node0.betree_internal_id msgs0 + st2 + Result.ret (st3, Option.some v0) + | betree_list_t.BetreeListNil => + do + let (st1, opt) ← + betree_internal_lookup_in_children_fwd node key st0 + let _ ← + betree_node_lookup_first_message_for_key_back key msgs + betree_list_t.BetreeListNil + Result.ret (st1, opt) + | betree_node_t.BetreeNodeLeaf node => + do + let (st0, bindings) ← betree_load_leaf_node_fwd node.betree_leaf_id st + let opt ← betree_node_lookup_in_bindings_fwd key bindings + Result.ret (st0, opt) +termination_by betree_node_lookup_fwd self key st => + betree_node_lookup_terminates self key st +decreasing_by betree_node_lookup_decreases self key st + +/- [betree_main::betree::Node::{5}::lookup] -/ +def betree_node_lookup_back + (self : betree_node_t) (key : UInt64) (st : State) : + (Result betree_node_t) + := + match h: self with + | betree_node_t.BetreeNodeInternal node => + do + let (st0, msgs) ← + betree_load_internal_node_fwd node.betree_internal_id st + let pending ← betree_node_lookup_first_message_for_key_fwd key msgs + match h: pending with + | betree_list_t.BetreeListCons p l => + let (k, msg) := p + if h: k != key + then + do + let _ ← + betree_node_lookup_first_message_for_key_back key msgs + (betree_list_t.BetreeListCons (k, msg) l) + let node0 ← betree_internal_lookup_in_children_back node key st0 + Result.ret (betree_node_t.BetreeNodeInternal node0) + else + match h: msg with + | betree_message_t.BetreeMessageInsert v => + do + let _ ← + betree_node_lookup_first_message_for_key_back key msgs + (betree_list_t.BetreeListCons (k, + betree_message_t.BetreeMessageInsert v) l) + Result.ret (betree_node_t.BetreeNodeInternal node) + | betree_message_t.BetreeMessageDelete => + do + let _ ← + betree_node_lookup_first_message_for_key_back key msgs + (betree_list_t.BetreeListCons (k, + betree_message_t.BetreeMessageDelete) l) + Result.ret (betree_node_t.BetreeNodeInternal node) + | betree_message_t.BetreeMessageUpsert ufs => + do + let (st1, v) ← + betree_internal_lookup_in_children_fwd node key st0 + let (st2, _) ← + betree_node_apply_upserts_fwd (betree_list_t.BetreeListCons (k, + betree_message_t.BetreeMessageUpsert ufs) l) v key st1 + let node0 ← + betree_internal_lookup_in_children_back node key st0 + let pending0 ← + betree_node_apply_upserts_back (betree_list_t.BetreeListCons + (k, betree_message_t.BetreeMessageUpsert ufs) l) v key st1 + let msgs0 ← + betree_node_lookup_first_message_for_key_back key msgs pending0 + let _ ← + betree_store_internal_node_fwd node0.betree_internal_id msgs0 + st2 + Result.ret (betree_node_t.BetreeNodeInternal node0) + | betree_list_t.BetreeListNil => + do + let _ ← + betree_node_lookup_first_message_for_key_back key msgs + betree_list_t.BetreeListNil + let node0 ← betree_internal_lookup_in_children_back node key st0 + Result.ret (betree_node_t.BetreeNodeInternal node0) + | betree_node_t.BetreeNodeLeaf node => + do + let (_, bindings) ← betree_load_leaf_node_fwd node.betree_leaf_id st + let _ ← betree_node_lookup_in_bindings_fwd key bindings + Result.ret (betree_node_t.BetreeNodeLeaf node) +termination_by betree_node_lookup_back self key st => + betree_node_lookup_terminates self key st +decreasing_by betree_node_lookup_decreases self key st + +/- [betree_main::betree::Internal::{4}::lookup_in_children] -/ +def betree_internal_lookup_in_children_fwd + (self : betree_internal_t) (key : UInt64) (st : State) : + (Result (State × (Option UInt64))) + := + if h: key < self.betree_internal_pivot + then betree_node_lookup_fwd self.betree_internal_left key st + else betree_node_lookup_fwd self.betree_internal_right key st +termination_by betree_internal_lookup_in_children_fwd self key st => + betree_internal_lookup_in_children_terminates self key st +decreasing_by betree_internal_lookup_in_children_decreases self key st + +/- [betree_main::betree::Internal::{4}::lookup_in_children] -/ +def betree_internal_lookup_in_children_back + (self : betree_internal_t) (key : UInt64) (st : State) : + (Result betree_internal_t) + := + if h: key < self.betree_internal_pivot + then + do + let n ← betree_node_lookup_back self.betree_internal_left key st + Result.ret + { + betree_internal_id := self.betree_internal_id, + betree_internal_pivot := self.betree_internal_pivot, + betree_internal_left := n, + betree_internal_right := self.betree_internal_right + } + else + do + let n ← betree_node_lookup_back self.betree_internal_right key st + Result.ret + { + betree_internal_id := self.betree_internal_id, + betree_internal_pivot := self.betree_internal_pivot, + betree_internal_left := self.betree_internal_left, + betree_internal_right := n + } +termination_by betree_internal_lookup_in_children_back self key st => + betree_internal_lookup_in_children_terminates self key st +decreasing_by betree_internal_lookup_in_children_decreases self key st + +/- [betree_main::betree::Node::{5}::lookup_mut_in_bindings] -/ +def betree_node_lookup_mut_in_bindings_fwd + (key : UInt64) (bindings : betree_list_t (UInt64 × UInt64)) : + (Result (betree_list_t (UInt64 × UInt64))) + := + match h: bindings with + | betree_list_t.BetreeListCons hd tl => + let (i, i0) := hd + if h: i >= key + then Result.ret (betree_list_t.BetreeListCons (i, i0) tl) + else betree_node_lookup_mut_in_bindings_fwd key tl + | betree_list_t.BetreeListNil => Result.ret betree_list_t.BetreeListNil +termination_by betree_node_lookup_mut_in_bindings_fwd key bindings => + betree_node_lookup_mut_in_bindings_terminates key bindings +decreasing_by betree_node_lookup_mut_in_bindings_decreases key bindings + +/- [betree_main::betree::Node::{5}::lookup_mut_in_bindings] -/ +def betree_node_lookup_mut_in_bindings_back + (key : UInt64) (bindings : betree_list_t (UInt64 × UInt64)) + (ret0 : betree_list_t (UInt64 × UInt64)) : + (Result (betree_list_t (UInt64 × UInt64))) + := + match h: bindings with + | betree_list_t.BetreeListCons hd tl => + let (i, i0) := hd + if h: i >= key + then Result.ret ret0 + else + do + let tl0 ← betree_node_lookup_mut_in_bindings_back key tl ret0 + Result.ret (betree_list_t.BetreeListCons (i, i0) tl0) + | betree_list_t.BetreeListNil => Result.ret ret0 +termination_by betree_node_lookup_mut_in_bindings_back key bindings ret0 => + betree_node_lookup_mut_in_bindings_terminates key bindings +decreasing_by betree_node_lookup_mut_in_bindings_decreases key bindings + +/- [betree_main::betree::Node::{5}::apply_to_leaf] -/ +def betree_node_apply_to_leaf_fwd_back + (bindings : betree_list_t (UInt64 × UInt64)) (key : UInt64) + (new_msg : betree_message_t) : + Result (betree_list_t (UInt64 × UInt64)) + := + do + let bindings0 ← betree_node_lookup_mut_in_bindings_fwd key bindings + let b ← betree_list_head_has_key_fwd UInt64 bindings0 key + if h: b + then + do + let hd ← betree_list_pop_front_fwd (UInt64 × UInt64) bindings0 + match h: new_msg with + | betree_message_t.BetreeMessageInsert v => + do + let bindings1 ← + betree_list_pop_front_back (UInt64 × UInt64) bindings0 + let bindings2 ← + betree_list_push_front_fwd_back (UInt64 × UInt64) bindings1 + (key, v) + betree_node_lookup_mut_in_bindings_back key bindings bindings2 + | betree_message_t.BetreeMessageDelete => + do + let bindings1 ← + betree_list_pop_front_back (UInt64 × UInt64) bindings0 + betree_node_lookup_mut_in_bindings_back key bindings bindings1 + | betree_message_t.BetreeMessageUpsert s => + do + let (_, i) := hd + let v ← betree_upsert_update_fwd (Option.some i) s + let bindings1 ← + betree_list_pop_front_back (UInt64 × UInt64) bindings0 + let bindings2 ← + betree_list_push_front_fwd_back (UInt64 × UInt64) bindings1 + (key, v) + betree_node_lookup_mut_in_bindings_back key bindings bindings2 + else + match h: new_msg with + | betree_message_t.BetreeMessageInsert v => + do + let bindings1 ← + betree_list_push_front_fwd_back (UInt64 × UInt64) bindings0 (key, + v) + betree_node_lookup_mut_in_bindings_back key bindings bindings1 + | betree_message_t.BetreeMessageDelete => + betree_node_lookup_mut_in_bindings_back key bindings bindings0 + | betree_message_t.BetreeMessageUpsert s => + do + let v ← betree_upsert_update_fwd Option.none s + let bindings1 ← + betree_list_push_front_fwd_back (UInt64 × UInt64) bindings0 (key, + v) + betree_node_lookup_mut_in_bindings_back key bindings bindings1 + +/- [betree_main::betree::Node::{5}::apply_messages_to_leaf] -/ +def betree_node_apply_messages_to_leaf_fwd_back + (bindings : betree_list_t (UInt64 × UInt64)) + (new_msgs : betree_list_t (UInt64 × betree_message_t)) : + (Result (betree_list_t (UInt64 × UInt64))) + := + match h: new_msgs with + | betree_list_t.BetreeListCons new_msg new_msgs_tl => + do + let (i, m) := new_msg + let bindings0 ← betree_node_apply_to_leaf_fwd_back bindings i m + betree_node_apply_messages_to_leaf_fwd_back bindings0 new_msgs_tl + | betree_list_t.BetreeListNil => Result.ret bindings +termination_by betree_node_apply_messages_to_leaf_fwd_back bindings new_msgs => + betree_node_apply_messages_to_leaf_terminates bindings new_msgs +decreasing_by betree_node_apply_messages_to_leaf_decreases bindings new_msgs + +/- [betree_main::betree::Node::{5}::filter_messages_for_key] -/ +def betree_node_filter_messages_for_key_fwd_back + (key : UInt64) (msgs : betree_list_t (UInt64 × betree_message_t)) : + (Result (betree_list_t (UInt64 × betree_message_t))) + := + match h: msgs with + | betree_list_t.BetreeListCons p l => + let (k, m) := p + if h: k = key + then + do + let msgs0 ← + betree_list_pop_front_back (UInt64 × betree_message_t) + (betree_list_t.BetreeListCons (k, m) l) + betree_node_filter_messages_for_key_fwd_back key msgs0 + else Result.ret (betree_list_t.BetreeListCons (k, m) l) + | betree_list_t.BetreeListNil => Result.ret betree_list_t.BetreeListNil +termination_by betree_node_filter_messages_for_key_fwd_back key msgs => + betree_node_filter_messages_for_key_terminates key msgs +decreasing_by betree_node_filter_messages_for_key_decreases key msgs + +/- [betree_main::betree::Node::{5}::lookup_first_message_after_key] -/ +def betree_node_lookup_first_message_after_key_fwd + (key : UInt64) (msgs : betree_list_t (UInt64 × betree_message_t)) : + (Result (betree_list_t (UInt64 × betree_message_t))) + := + match h: msgs with + | betree_list_t.BetreeListCons p next_msgs => + let (k, m) := p + if h: k = key + then betree_node_lookup_first_message_after_key_fwd key next_msgs + else Result.ret (betree_list_t.BetreeListCons (k, m) next_msgs) + | betree_list_t.BetreeListNil => Result.ret betree_list_t.BetreeListNil +termination_by betree_node_lookup_first_message_after_key_fwd key msgs => + betree_node_lookup_first_message_after_key_terminates key msgs +decreasing_by betree_node_lookup_first_message_after_key_decreases key msgs + +/- [betree_main::betree::Node::{5}::lookup_first_message_after_key] -/ +def betree_node_lookup_first_message_after_key_back + (key : UInt64) (msgs : betree_list_t (UInt64 × betree_message_t)) + (ret0 : betree_list_t (UInt64 × betree_message_t)) : + (Result (betree_list_t (UInt64 × betree_message_t))) + := + match h: msgs with + | betree_list_t.BetreeListCons p next_msgs => + let (k, m) := p + if h: k = key + then + do + let next_msgs0 ← + betree_node_lookup_first_message_after_key_back key next_msgs ret0 + Result.ret (betree_list_t.BetreeListCons (k, m) next_msgs0) + else Result.ret ret0 + | betree_list_t.BetreeListNil => Result.ret ret0 +termination_by betree_node_lookup_first_message_after_key_back key msgs ret0 => + betree_node_lookup_first_message_after_key_terminates key msgs +decreasing_by betree_node_lookup_first_message_after_key_decreases key msgs + +/- [betree_main::betree::Node::{5}::apply_to_internal] -/ +def betree_node_apply_to_internal_fwd_back + (msgs : betree_list_t (UInt64 × betree_message_t)) (key : UInt64) + (new_msg : betree_message_t) : + Result (betree_list_t (UInt64 × betree_message_t)) + := + do + let msgs0 ← betree_node_lookup_first_message_for_key_fwd key msgs + let b ← betree_list_head_has_key_fwd betree_message_t msgs0 key + if h: b + then + match h: new_msg with + | betree_message_t.BetreeMessageInsert i => + do + let msgs1 ← betree_node_filter_messages_for_key_fwd_back key msgs0 + let msgs2 ← + betree_list_push_front_fwd_back (UInt64 × betree_message_t) msgs1 + (key, betree_message_t.BetreeMessageInsert i) + betree_node_lookup_first_message_for_key_back key msgs msgs2 + | betree_message_t.BetreeMessageDelete => + do + let msgs1 ← betree_node_filter_messages_for_key_fwd_back key msgs0 + let msgs2 ← + betree_list_push_front_fwd_back (UInt64 × betree_message_t) msgs1 + (key, betree_message_t.BetreeMessageDelete) + betree_node_lookup_first_message_for_key_back key msgs msgs2 + | betree_message_t.BetreeMessageUpsert s => + do + let p ← betree_list_hd_fwd (UInt64 × betree_message_t) msgs0 + let (_, m) := p + match h: m with + | betree_message_t.BetreeMessageInsert prev => + do + let v ← betree_upsert_update_fwd (Option.some prev) s + let msgs1 ← + betree_list_pop_front_back (UInt64 × betree_message_t) msgs0 + let msgs2 ← + betree_list_push_front_fwd_back (UInt64 × betree_message_t) + msgs1 (key, betree_message_t.BetreeMessageInsert v) + betree_node_lookup_first_message_for_key_back key msgs msgs2 + | betree_message_t.BetreeMessageDelete => + do + let v ← betree_upsert_update_fwd Option.none s + let msgs1 ← + betree_list_pop_front_back (UInt64 × betree_message_t) msgs0 + let msgs2 ← + betree_list_push_front_fwd_back (UInt64 × betree_message_t) + msgs1 (key, betree_message_t.BetreeMessageInsert v) + betree_node_lookup_first_message_for_key_back key msgs msgs2 + | betree_message_t.BetreeMessageUpsert ufs => + do + let msgs1 ← + betree_node_lookup_first_message_after_key_fwd key msgs0 + let msgs2 ← + betree_list_push_front_fwd_back (UInt64 × betree_message_t) + msgs1 (key, betree_message_t.BetreeMessageUpsert s) + let msgs3 ← + betree_node_lookup_first_message_after_key_back key msgs0 msgs2 + betree_node_lookup_first_message_for_key_back key msgs msgs3 + else + do + let msgs1 ← + betree_list_push_front_fwd_back (UInt64 × betree_message_t) msgs0 + (key, new_msg) + betree_node_lookup_first_message_for_key_back key msgs msgs1 + +/- [betree_main::betree::Node::{5}::apply_messages_to_internal] -/ +def betree_node_apply_messages_to_internal_fwd_back + (msgs : betree_list_t (UInt64 × betree_message_t)) + (new_msgs : betree_list_t (UInt64 × betree_message_t)) : + (Result (betree_list_t (UInt64 × betree_message_t))) + := + match h: new_msgs with + | betree_list_t.BetreeListCons new_msg new_msgs_tl => + do + let (i, m) := new_msg + let msgs0 ← betree_node_apply_to_internal_fwd_back msgs i m + betree_node_apply_messages_to_internal_fwd_back msgs0 new_msgs_tl + | betree_list_t.BetreeListNil => Result.ret msgs +termination_by betree_node_apply_messages_to_internal_fwd_back msgs new_msgs => + betree_node_apply_messages_to_internal_terminates msgs new_msgs +decreasing_by betree_node_apply_messages_to_internal_decreases msgs new_msgs + +/- [betree_main::betree::Node::{5}::apply_messages] -/ +mutual def betree_node_apply_messages_fwd + (self : betree_node_t) (params : betree_params_t) + (node_id_cnt : betree_node_id_counter_t) + (msgs : betree_list_t (UInt64 × betree_message_t)) (st : State) : + (Result (State × Unit)) + := + match h: self with + | betree_node_t.BetreeNodeInternal node => + do + let (st0, content) ← + betree_load_internal_node_fwd node.betree_internal_id st + let content0 ← + betree_node_apply_messages_to_internal_fwd_back content msgs + let num_msgs ← + betree_list_len_fwd (UInt64 × betree_message_t) content0 + if h: num_msgs >= params.betree_params_min_flush_size + then + do + let (st1, content1) ← + betree_internal_flush_fwd node params node_id_cnt content0 st0 + let (node0, _) ← + betree_internal_flush_back node params node_id_cnt content0 st0 + let (st2, _) ← + betree_store_internal_node_fwd node0.betree_internal_id content1 + st1 + Result.ret (st2, ()) + else + do + let (st1, _) ← + betree_store_internal_node_fwd node.betree_internal_id content0 st0 + Result.ret (st1, ()) + | betree_node_t.BetreeNodeLeaf node => + do + let (st0, content) ← betree_load_leaf_node_fwd node.betree_leaf_id st + let content0 ← betree_node_apply_messages_to_leaf_fwd_back content msgs + let len ← betree_list_len_fwd (UInt64 × UInt64) content0 + let i ← UInt64.checked_mul (UInt64.ofNatCore 2 (by intlit)) + params.betree_params_split_size + if h: len >= i + then + do + let (st1, _) ← + betree_leaf_split_fwd node content0 params node_id_cnt st0 + let (st2, _) ← + betree_store_leaf_node_fwd node.betree_leaf_id + betree_list_t.BetreeListNil st1 + Result.ret (st2, ()) + else + do + let (st1, _) ← + betree_store_leaf_node_fwd node.betree_leaf_id content0 st0 + Result.ret (st1, ()) +termination_by betree_node_apply_messages_fwd self params node_id_cnt msgs st + => + betree_node_apply_messages_terminates self params node_id_cnt msgs st +decreasing_by + betree_node_apply_messages_decreases self params node_id_cnt msgs st + +/- [betree_main::betree::Node::{5}::apply_messages] -/ +def betree_node_apply_messages_back + (self : betree_node_t) (params : betree_params_t) + (node_id_cnt : betree_node_id_counter_t) + (msgs : betree_list_t (UInt64 × betree_message_t)) (st : State) : + (Result (betree_node_t × betree_node_id_counter_t)) + := + match h: self with + | betree_node_t.BetreeNodeInternal node => + do + let (st0, content) ← + betree_load_internal_node_fwd node.betree_internal_id st + let content0 ← + betree_node_apply_messages_to_internal_fwd_back content msgs + let num_msgs ← + betree_list_len_fwd (UInt64 × betree_message_t) content0 + if h: num_msgs >= params.betree_params_min_flush_size + then + do + let (st1, content1) ← + betree_internal_flush_fwd node params node_id_cnt content0 st0 + let (node0, node_id_cnt0) ← + betree_internal_flush_back node params node_id_cnt content0 st0 + let _ ← + betree_store_internal_node_fwd node0.betree_internal_id content1 + st1 + Result.ret (betree_node_t.BetreeNodeInternal node0, node_id_cnt0) + else + do + let _ ← + betree_store_internal_node_fwd node.betree_internal_id content0 st0 + Result.ret (betree_node_t.BetreeNodeInternal node, node_id_cnt) + | betree_node_t.BetreeNodeLeaf node => + do + let (st0, content) ← betree_load_leaf_node_fwd node.betree_leaf_id st + let content0 ← betree_node_apply_messages_to_leaf_fwd_back content msgs + let len ← betree_list_len_fwd (UInt64 × UInt64) content0 + let i ← UInt64.checked_mul (UInt64.ofNatCore 2 (by intlit)) + params.betree_params_split_size + if h: len >= i + then + do + let (st1, new_node) ← + betree_leaf_split_fwd node content0 params node_id_cnt st0 + let _ ← + betree_store_leaf_node_fwd node.betree_leaf_id + betree_list_t.BetreeListNil st1 + let node_id_cnt0 ← + betree_leaf_split_back node content0 params node_id_cnt st0 + Result.ret (betree_node_t.BetreeNodeInternal new_node, node_id_cnt0) + else + do + let _ ← betree_store_leaf_node_fwd node.betree_leaf_id content0 st0 + Result.ret (betree_node_t.BetreeNodeLeaf + { betree_leaf_id := node.betree_leaf_id, betree_leaf_size := len }, + node_id_cnt) +termination_by betree_node_apply_messages_back self params node_id_cnt msgs st + => + betree_node_apply_messages_terminates self params node_id_cnt msgs st +decreasing_by + betree_node_apply_messages_decreases self params node_id_cnt msgs st + +/- [betree_main::betree::Internal::{4}::flush] -/ +def betree_internal_flush_fwd + (self : betree_internal_t) (params : betree_params_t) + (node_id_cnt : betree_node_id_counter_t) + (content : betree_list_t (UInt64 × betree_message_t)) (st : State) : + (Result (State × (betree_list_t (UInt64 × betree_message_t)))) + := + do + let p ← + betree_list_partition_at_pivot_fwd betree_message_t content + self.betree_internal_pivot + let (msgs_left, msgs_right) := p + let len_left ← betree_list_len_fwd (UInt64 × betree_message_t) msgs_left + if h: len_left >= params.betree_params_min_flush_size + then + do + let (st0, _) ← + betree_node_apply_messages_fwd self.betree_internal_left params + node_id_cnt msgs_left st + let (_, node_id_cnt0) ← + betree_node_apply_messages_back self.betree_internal_left params + node_id_cnt msgs_left st + let len_right ← + betree_list_len_fwd (UInt64 × betree_message_t) msgs_right + if h: len_right >= params.betree_params_min_flush_size + then + do + let (st1, _) ← + betree_node_apply_messages_fwd self.betree_internal_right params + node_id_cnt0 msgs_right st0 + let _ ← + betree_node_apply_messages_back self.betree_internal_right params + node_id_cnt0 msgs_right st0 + Result.ret (st1, betree_list_t.BetreeListNil) + else Result.ret (st0, msgs_right) + else + do + let (st0, _) ← + betree_node_apply_messages_fwd self.betree_internal_right params + node_id_cnt msgs_right st + let _ ← + betree_node_apply_messages_back self.betree_internal_right params + node_id_cnt msgs_right st + Result.ret (st0, msgs_left) +termination_by betree_internal_flush_fwd self params node_id_cnt content st => + betree_internal_flush_terminates self params node_id_cnt content st +decreasing_by + betree_internal_flush_decreases self params node_id_cnt content st + +/- [betree_main::betree::Internal::{4}::flush] -/ +def betree_internal_flush_back + (self : betree_internal_t) (params : betree_params_t) + (node_id_cnt : betree_node_id_counter_t) + (content : betree_list_t (UInt64 × betree_message_t)) (st : State) : + (Result (betree_internal_t × betree_node_id_counter_t)) + := + do + let p ← + betree_list_partition_at_pivot_fwd betree_message_t content + self.betree_internal_pivot + let (msgs_left, msgs_right) := p + let len_left ← betree_list_len_fwd (UInt64 × betree_message_t) msgs_left + if h: len_left >= params.betree_params_min_flush_size + then + do + let (st0, _) ← + betree_node_apply_messages_fwd self.betree_internal_left params + node_id_cnt msgs_left st + let (n, node_id_cnt0) ← + betree_node_apply_messages_back self.betree_internal_left params + node_id_cnt msgs_left st + let len_right ← + betree_list_len_fwd (UInt64 × betree_message_t) msgs_right + if h: len_right >= params.betree_params_min_flush_size + then + do + let (n0, node_id_cnt1) ← + betree_node_apply_messages_back self.betree_internal_right params + node_id_cnt0 msgs_right st0 + Result.ret + ({ + betree_internal_id := self.betree_internal_id, + betree_internal_pivot := self.betree_internal_pivot, + betree_internal_left := n, + betree_internal_right := n0 + }, node_id_cnt1) + else + Result.ret + ({ + betree_internal_id := self.betree_internal_id, + betree_internal_pivot := self.betree_internal_pivot, + betree_internal_left := n, + betree_internal_right := self.betree_internal_right + }, node_id_cnt0) + else + do + let (n, node_id_cnt0) ← + betree_node_apply_messages_back self.betree_internal_right params + node_id_cnt msgs_right st + Result.ret + ({ + betree_internal_id := self.betree_internal_id, + betree_internal_pivot := self.betree_internal_pivot, + betree_internal_left := self.betree_internal_left, + betree_internal_right := n + }, node_id_cnt0) +termination_by betree_internal_flush_back self params node_id_cnt content st => + betree_internal_flush_terminates self params node_id_cnt content st +decreasing_by + betree_internal_flush_decreases self params node_id_cnt content st + +/- [betree_main::betree::Node::{5}::apply] -/ +def betree_node_apply_fwd + (self : betree_node_t) (params : betree_params_t) + (node_id_cnt : betree_node_id_counter_t) (key : UInt64) + (new_msg : betree_message_t) (st : State) : + Result (State × Unit) + := + do + let l := betree_list_t.BetreeListNil + let (st0, _) ← + betree_node_apply_messages_fwd self params node_id_cnt + (betree_list_t.BetreeListCons (key, new_msg) l) st + let _ ← + betree_node_apply_messages_back self params node_id_cnt + (betree_list_t.BetreeListCons (key, new_msg) l) st + Result.ret (st0, ()) + +/- [betree_main::betree::Node::{5}::apply] -/ +def betree_node_apply_back + (self : betree_node_t) (params : betree_params_t) + (node_id_cnt : betree_node_id_counter_t) (key : UInt64) + (new_msg : betree_message_t) (st : State) : + Result (betree_node_t × betree_node_id_counter_t) + := + let l := betree_list_t.BetreeListNil + betree_node_apply_messages_back self params node_id_cnt + (betree_list_t.BetreeListCons (key, new_msg) l) st + +/- [betree_main::betree::BeTree::{6}::new] -/ +def betree_be_tree_new_fwd + (min_flush_size : UInt64) (split_size : UInt64) (st : State) : + Result (State × betree_be_tree_t) + := + do + let node_id_cnt ← betree_node_id_counter_new_fwd + let id ← betree_node_id_counter_fresh_id_fwd node_id_cnt + let (st0, _) ← + betree_store_leaf_node_fwd id betree_list_t.BetreeListNil st + let node_id_cnt0 ← betree_node_id_counter_fresh_id_back node_id_cnt + Result.ret (st0, + { + betree_be_tree_params := { + betree_params_min_flush_size := min_flush_size, + betree_params_split_size := split_size + }, + betree_be_tree_node_id_cnt := node_id_cnt0, + betree_be_tree_root := (betree_node_t.BetreeNodeLeaf + { + betree_leaf_id := id, + betree_leaf_size := (UInt64.ofNatCore 0 (by intlit)) + }) + }) + +/- [betree_main::betree::BeTree::{6}::apply] -/ +def betree_be_tree_apply_fwd + (self : betree_be_tree_t) (key : UInt64) (msg : betree_message_t) + (st : State) : + Result (State × Unit) + := + do + let (st0, _) ← + betree_node_apply_fwd self.betree_be_tree_root self.betree_be_tree_params + self.betree_be_tree_node_id_cnt key msg st + let _ ← + betree_node_apply_back self.betree_be_tree_root + self.betree_be_tree_params self.betree_be_tree_node_id_cnt key msg st + Result.ret (st0, ()) + +/- [betree_main::betree::BeTree::{6}::apply] -/ +def betree_be_tree_apply_back + (self : betree_be_tree_t) (key : UInt64) (msg : betree_message_t) + (st : State) : + Result betree_be_tree_t + := + do + let (n, nic) ← + betree_node_apply_back self.betree_be_tree_root + self.betree_be_tree_params self.betree_be_tree_node_id_cnt key msg st + Result.ret + { + betree_be_tree_params := self.betree_be_tree_params, + betree_be_tree_node_id_cnt := nic, + betree_be_tree_root := n + } + +/- [betree_main::betree::BeTree::{6}::insert] -/ +def betree_be_tree_insert_fwd + (self : betree_be_tree_t) (key : UInt64) (value : UInt64) (st : State) : + Result (State × Unit) + := + do + let (st0, _) ← + betree_be_tree_apply_fwd self key (betree_message_t.BetreeMessageInsert + value) st + let _ ← + betree_be_tree_apply_back self key (betree_message_t.BetreeMessageInsert + value) st + Result.ret (st0, ()) + +/- [betree_main::betree::BeTree::{6}::insert] -/ +def betree_be_tree_insert_back + (self : betree_be_tree_t) (key : UInt64) (value : UInt64) (st : State) : + Result betree_be_tree_t + := + betree_be_tree_apply_back self key (betree_message_t.BetreeMessageInsert + value) st + +/- [betree_main::betree::BeTree::{6}::delete] -/ +def betree_be_tree_delete_fwd + (self : betree_be_tree_t) (key : UInt64) (st : State) : + Result (State × Unit) + := + do + let (st0, _) ← + betree_be_tree_apply_fwd self key betree_message_t.BetreeMessageDelete st + let _ ← + betree_be_tree_apply_back self key betree_message_t.BetreeMessageDelete + st + Result.ret (st0, ()) + +/- [betree_main::betree::BeTree::{6}::delete] -/ +def betree_be_tree_delete_back + (self : betree_be_tree_t) (key : UInt64) (st : State) : + Result betree_be_tree_t + := + betree_be_tree_apply_back self key betree_message_t.BetreeMessageDelete st + +/- [betree_main::betree::BeTree::{6}::upsert] -/ +def betree_be_tree_upsert_fwd + (self : betree_be_tree_t) (key : UInt64) (upd : betree_upsert_fun_state_t) + (st : State) : + Result (State × Unit) + := + do + let (st0, _) ← + betree_be_tree_apply_fwd self key (betree_message_t.BetreeMessageUpsert + upd) st + let _ ← + betree_be_tree_apply_back self key (betree_message_t.BetreeMessageUpsert + upd) st + Result.ret (st0, ()) + +/- [betree_main::betree::BeTree::{6}::upsert] -/ +def betree_be_tree_upsert_back + (self : betree_be_tree_t) (key : UInt64) (upd : betree_upsert_fun_state_t) + (st : State) : + Result betree_be_tree_t + := + betree_be_tree_apply_back self key (betree_message_t.BetreeMessageUpsert upd) + st + +/- [betree_main::betree::BeTree::{6}::lookup] -/ +def betree_be_tree_lookup_fwd + (self : betree_be_tree_t) (key : UInt64) (st : State) : + Result (State × (Option UInt64)) + := + betree_node_lookup_fwd self.betree_be_tree_root key st + +/- [betree_main::betree::BeTree::{6}::lookup] -/ +def betree_be_tree_lookup_back + (self : betree_be_tree_t) (key : UInt64) (st : State) : + Result betree_be_tree_t + := + do + let n ← betree_node_lookup_back self.betree_be_tree_root key st + Result.ret + { + betree_be_tree_params := self.betree_be_tree_params, + betree_be_tree_node_id_cnt := self.betree_be_tree_node_id_cnt, + betree_be_tree_root := n + } + +/- [betree_main::main] -/ +def main_fwd : Result Unit := + Result.ret () + +/- Unit test for [betree_main::main] -/ +#assert (main_fwd == .ret ()) + diff --git a/tests/lean/betree/BetreeMain/Opaque.lean b/tests/lean/betree/BetreeMain/Opaque.lean new file mode 100644 index 00000000..b3db37c2 --- /dev/null +++ b/tests/lean/betree/BetreeMain/Opaque.lean @@ -0,0 +1,33 @@ +-- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS +-- [betree_main]: opaque function definitions +import Base.Primitives +import BetreeMain.Types + +structure OpaqueDefs where + + /- [betree_main::betree_utils::load_internal_node] -/ + betree_utils_load_internal_node_fwd + : + UInt64 -> State -> Result (State × (betree_list_t (UInt64 × + betree_message_t))) + + /- [betree_main::betree_utils::store_internal_node] -/ + betree_utils_store_internal_node_fwd + : + UInt64 -> betree_list_t (UInt64 × betree_message_t) -> State -> Result + (State × Unit) + + /- [betree_main::betree_utils::load_leaf_node] -/ + betree_utils_load_leaf_node_fwd + : UInt64 -> State -> Result (State × (betree_list_t (UInt64 × UInt64))) + + /- [betree_main::betree_utils::store_leaf_node] -/ + betree_utils_store_leaf_node_fwd + : + UInt64 -> betree_list_t (UInt64 × UInt64) -> State -> Result (State × + Unit) + + /- [core::option::Option::{0}::unwrap] -/ + core_option_option_unwrap_fwd + (T : Type) : Option T -> State -> Result (State × T) + diff --git a/tests/lean/betree/BetreeMain/Types.lean b/tests/lean/betree/BetreeMain/Types.lean new file mode 100644 index 00000000..2726e1f0 --- /dev/null +++ b/tests/lean/betree/BetreeMain/Types.lean @@ -0,0 +1,61 @@ +-- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS +-- [betree_main]: type definitions +import Base.Primitives + +/- [betree_main::betree::List] -/ +inductive betree_list_t (T : Type) := +| BetreeListCons : T -> betree_list_t T -> betree_list_t T +| BetreeListNil : betree_list_t T + +/- [betree_main::betree::UpsertFunState] -/ +inductive betree_upsert_fun_state_t := +| BetreeUpsertFunStateAdd : UInt64 -> betree_upsert_fun_state_t +| BetreeUpsertFunStateSub : UInt64 -> betree_upsert_fun_state_t + +/- [betree_main::betree::Message] -/ +inductive betree_message_t := +| BetreeMessageInsert : UInt64 -> betree_message_t +| BetreeMessageDelete : betree_message_t +| BetreeMessageUpsert : betree_upsert_fun_state_t -> betree_message_t + +/- [betree_main::betree::Leaf] -/ +structure betree_leaf_t where + + betree_leaf_id : UInt64 betree_leaf_size : UInt64 + + +/- [betree_main::betree::Node] -/ +mutual inductive betree_node_t := +| BetreeNodeInternal : betree_internal_t -> betree_node_t +| BetreeNodeLeaf : betree_leaf_t -> betree_node_t + +/- [betree_main::betree::Internal] -/ +inductive betree_internal_t := + + betree_internal_id : UInt64 + betree_internal_pivot : UInt64 + betree_internal_left : betree_node_t + betree_internal_right : betree_node_t + + +/- [betree_main::betree::Params] -/ +structure betree_params_t where + + betree_params_min_flush_size : UInt64 betree_params_split_size : UInt64 + + +/- [betree_main::betree::NodeIdCounter] -/ +structure betree_node_id_counter_t where + + betree_node_id_counter_next_node_id : UInt64 + + +/- [betree_main::betree::BeTree] -/ +structure betree_be_tree_t where + + betree_be_tree_params : betree_params_t + betree_be_tree_node_id_cnt : betree_node_id_counter_t + betree_be_tree_root : betree_node_t + +/- The state type used in the state-error monad -/ axiom State : Type + |