-- 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 ())