From fa6dcd3ebbdc7a508157ff2a12f91e70d2012a86 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Tue, 15 Nov 2022 15:25:47 +0100 Subject: Change the name of the generated Coq modules --- tests/coq/betree/BetreeMain_Funs.v | 1397 +++++++++++++++++++++++++++++++++ tests/coq/betree/BetreeMain_Opaque.v | 38 + tests/coq/betree/BetreeMain_Types.v | 85 ++ tests/coq/betree/BetreeMain__Funs.v | 1397 --------------------------------- tests/coq/betree/BetreeMain__Opaque.v | 38 - tests/coq/betree/BetreeMain__Types.v | 85 -- 6 files changed, 1520 insertions(+), 1520 deletions(-) create mode 100644 tests/coq/betree/BetreeMain_Funs.v create mode 100644 tests/coq/betree/BetreeMain_Opaque.v create mode 100644 tests/coq/betree/BetreeMain_Types.v delete mode 100644 tests/coq/betree/BetreeMain__Funs.v delete mode 100644 tests/coq/betree/BetreeMain__Opaque.v delete mode 100644 tests/coq/betree/BetreeMain__Types.v (limited to 'tests/coq/betree') diff --git a/tests/coq/betree/BetreeMain_Funs.v b/tests/coq/betree/BetreeMain_Funs.v new file mode 100644 index 00000000..3129614c --- /dev/null +++ b/tests/coq/betree/BetreeMain_Funs.v @@ -0,0 +1,1397 @@ +(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *) +(** [betree_main]: function definitions *) +Require Import Primitives. +Import Primitives. +Require Import Coq.ZArith.ZArith. +Local Open Scope Primitives_scope. +Require Export BetreeMain_Types. +Import BetreeMain_Types. +Require Export BetreeMain_Opaque. +Import BetreeMain_Opaque. +Module BetreeMain_Funs. + +(** [betree_main::betree::load_internal_node] *) +Definition betree_load_internal_node_fwd + (id : u64) (st : state) : + result (state * (Betree_list_t (u64 * Betree_message_t))) + := + p <- betree_utils_load_internal_node_fwd id st; + let (st0, l) := p in + Return (st0, l) +. + +(** [betree_main::betree::store_internal_node] *) +Definition betree_store_internal_node_fwd + (id : u64) (content : Betree_list_t (u64 * Betree_message_t)) (st : state) : + result (state * unit) + := + p <- betree_utils_store_internal_node_fwd id content st; + let (st0, _) := p in + Return (st0, tt) +. + +(** [betree_main::betree::load_leaf_node] *) +Definition betree_load_leaf_node_fwd + (id : u64) (st : state) : result (state * (Betree_list_t (u64 * u64))) := + p <- betree_utils_load_leaf_node_fwd id st; + let (st0, l) := p in + Return (st0, l) +. + +(** [betree_main::betree::store_leaf_node] *) +Definition betree_store_leaf_node_fwd + (id : u64) (content : Betree_list_t (u64 * u64)) (st : state) : + result (state * unit) + := + p <- betree_utils_store_leaf_node_fwd id content st; + let (st0, _) := p in + Return (st0, tt) +. + +(** [betree_main::betree::fresh_node_id] *) +Definition betree_fresh_node_id_fwd (counter : u64) : result u64 := + i <- u64_add counter 1%u64; let _ := i in Return counter +. + +(** [betree_main::betree::fresh_node_id] *) +Definition betree_fresh_node_id_back (counter : u64) : result u64 := + counter0 <- u64_add counter 1%u64; Return counter0 +. + +(** [betree_main::betree::NodeIdCounter::{0}::new] *) +Definition betree_node_id_counter_new_fwd : result Betree_node_id_counter_t := + Return (mkBetree_node_id_counter_t (0%u64)) +. + +(** [betree_main::betree::NodeIdCounter::{0}::fresh_id] *) +Definition betree_node_id_counter_fresh_id_fwd + (self : Betree_node_id_counter_t) : result u64 := + match self with + | mkBetree_node_id_counter_t id => + i <- u64_add id 1%u64; let _ := i in Return id + end +. + +(** [betree_main::betree::NodeIdCounter::{0}::fresh_id] *) +Definition betree_node_id_counter_fresh_id_back + (self : Betree_node_id_counter_t) : result Betree_node_id_counter_t := + match self with + | mkBetree_node_id_counter_t id => + i <- u64_add id 1%u64; Return (mkBetree_node_id_counter_t i) + end +. + +(** [core::num::u64::{10}::MAX] *) +Definition core_num_u64_max_body : result u64 := + Return (18446744073709551615%u64) +. +Definition core_num_u64_max_c : u64 := core_num_u64_max_body%global. + +(** [betree_main::betree::upsert_update] *) +Definition betree_upsert_update_fwd + (prev : option u64) (st : Betree_upsert_fun_state_t) : result u64 := + match prev with + | None => + match st with + | BetreeUpsertFunStateAdd v => Return v + | BetreeUpsertFunStateSub i => Return (0%u64) + end + | Some prev0 => + match st with + | BetreeUpsertFunStateAdd v => + margin <- u64_sub core_num_u64_max_c prev0; + if margin s>= v + then (i <- u64_add prev0 v; Return i) + else Return core_num_u64_max_c + | BetreeUpsertFunStateSub v => + if prev0 s>= v then (i <- u64_sub prev0 v; Return i) else Return (0%u64) + end + end +. + +(** [betree_main::betree::List::{1}::len] *) +Fixpoint betree_list_len_fwd + (T : Type) (n : nat) (self : Betree_list_t T) : result u64 := + match n with + | O => Fail_ OutOfFuel + | S n0 => + match self with + | BetreeListCons t tl => + i <- betree_list_len_fwd T n0 tl; i0 <- u64_add 1%u64 i; Return i0 + | BetreeListNil => Return (0%u64) + end + end +. + +(** [betree_main::betree::List::{1}::split_at] *) +Fixpoint betree_list_split_at_fwd + (T : Type) (n : nat) (self : Betree_list_t T) (n0 : u64) : + result ((Betree_list_t T) * (Betree_list_t T)) + := + match n with + | O => Fail_ OutOfFuel + | S n1 => + if n0 s= 0%u64 + then Return (BetreeListNil, self) + else + match self with + | BetreeListCons hd tl => + i <- u64_sub n0 1%u64; + p <- betree_list_split_at_fwd T n1 tl i; + let (ls0, ls1) := p in + let l := ls0 in + Return (BetreeListCons hd l, ls1) + | BetreeListNil => Fail_ Failure + end + end +. + +(** [betree_main::betree::List::{1}::push_front] *) +Definition 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 BetreeListNil in + let l := tl in + Return (BetreeListCons x l) +. + +(** [betree_main::betree::List::{1}::pop_front] *) +Definition betree_list_pop_front_fwd + (T : Type) (self : Betree_list_t T) : result T := + let ls := mem_replace_fwd (Betree_list_t T) self BetreeListNil in + match ls with + | BetreeListCons x tl => Return x + | BetreeListNil => Fail_ Failure + end +. + +(** [betree_main::betree::List::{1}::pop_front] *) +Definition 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 BetreeListNil in + match ls with + | BetreeListCons x tl => Return tl + | BetreeListNil => Fail_ Failure + end +. + +(** [betree_main::betree::List::{1}::hd] *) +Definition betree_list_hd_fwd (T : Type) (self : Betree_list_t T) : result T := + match self with + | BetreeListCons hd l => Return hd + | BetreeListNil => Fail_ Failure + end +. + +(** [betree_main::betree::List::{2}::head_has_key] *) +Definition betree_list_head_has_key_fwd + (T : Type) (self : Betree_list_t (u64 * T)) (key : u64) : result bool := + match self with + | BetreeListCons hd l => let (i, _) := hd in Return (i s= key) + | BetreeListNil => Return false + end +. + +(** [betree_main::betree::List::{2}::partition_at_pivot] *) +Fixpoint betree_list_partition_at_pivot_fwd + (T : Type) (n : nat) (self : Betree_list_t (u64 * T)) (pivot : u64) : + result ((Betree_list_t (u64 * T)) * (Betree_list_t (u64 * T))) + := + match n with + | O => Fail_ OutOfFuel + | S n0 => + match self with + | BetreeListCons hd tl => + let (i, t) := hd in + if i s>= pivot + then Return (BetreeListNil, BetreeListCons (i, t) tl) + else ( + p <- betree_list_partition_at_pivot_fwd T n0 tl pivot; + let (ls0, ls1) := p in + let l := ls0 in + Return (BetreeListCons (i, t) l, ls1)) + | BetreeListNil => Return (BetreeListNil, BetreeListNil) + end + end +. + +(** [betree_main::betree::Leaf::{3}::split] *) +Definition betree_leaf_split_fwd + (n : nat) (self : Betree_leaf_t) (content : Betree_list_t (u64 * u64)) + (params : Betree_params_t) (node_id_cnt : Betree_node_id_counter_t) + (st : state) : + result (state * Betree_internal_t) + := + match n with + | O => Fail_ OutOfFuel + | S n0 => + match params with + | mkBetree_params_t i i0 => + p <- betree_list_split_at_fwd (u64 * u64) n0 content i0; + let (content0, content1) := p in + p0 <- betree_list_hd_fwd (u64 * u64) content1; + let (pivot, _) := p0 in + id0 <- betree_node_id_counter_fresh_id_fwd node_id_cnt; + node_id_cnt0 <- betree_node_id_counter_fresh_id_back node_id_cnt; + id1 <- betree_node_id_counter_fresh_id_fwd node_id_cnt0; + p1 <- betree_store_leaf_node_fwd id0 content0 st; + let (st0, _) := p1 in + p2 <- betree_store_leaf_node_fwd id1 content1 st0; + let (st1, _) := p2 in + match self with + | mkBetree_leaf_t i1 i2 => + let n1 := BetreeNodeLeaf (mkBetree_leaf_t id0 i0) in + let n2 := BetreeNodeLeaf (mkBetree_leaf_t id1 i0) in + Return (st1, mkBetree_internal_t i1 pivot n1 n2) + end + end + end +. + +(** [betree_main::betree::Leaf::{3}::split] *) +Definition betree_leaf_split_back + (n : nat) (self : Betree_leaf_t) (content : Betree_list_t (u64 * u64)) + (params : Betree_params_t) (node_id_cnt : Betree_node_id_counter_t) + (st : state) : + result Betree_node_id_counter_t + := + match n with + | O => Fail_ OutOfFuel + | S n0 => + match params with + | mkBetree_params_t i i0 => + p <- betree_list_split_at_fwd (u64 * u64) n0 content i0; + let (content0, content1) := p in + p0 <- betree_list_hd_fwd (u64 * u64) content1; + let _ := p0 in + id0 <- betree_node_id_counter_fresh_id_fwd node_id_cnt; + node_id_cnt0 <- betree_node_id_counter_fresh_id_back node_id_cnt; + id1 <- betree_node_id_counter_fresh_id_fwd node_id_cnt0; + p1 <- betree_store_leaf_node_fwd id0 content0 st; + let (st0, _) := p1 in + p2 <- betree_store_leaf_node_fwd id1 content1 st0; + let (_, _) := p2 in + match self with + | mkBetree_leaf_t i1 i2 => + node_id_cnt1 <- betree_node_id_counter_fresh_id_back node_id_cnt0; + Return node_id_cnt1 + end + end + end +. + +(** [betree_main::betree::Node::{5}::lookup_in_bindings] *) +Fixpoint betree_node_lookup_in_bindings_fwd + (n : nat) (key : u64) (bindings : Betree_list_t (u64 * u64)) : + result (option u64) + := + match n with + | O => Fail_ OutOfFuel + | S n0 => + match bindings with + | BetreeListCons hd tl => + let (i, i0) := hd in + if i s= key + then Return (Some i0) + else + if i s> key + then Return None + else (opt <- betree_node_lookup_in_bindings_fwd n0 key tl; Return opt) + | BetreeListNil => Return None + end + end +. + +(** [betree_main::betree::Node::{5}::lookup_first_message_for_key] *) +Fixpoint betree_node_lookup_first_message_for_key_fwd + (n : nat) (key : u64) (msgs : Betree_list_t (u64 * Betree_message_t)) : + result (Betree_list_t (u64 * Betree_message_t)) + := + match n with + | O => Fail_ OutOfFuel + | S n0 => + match msgs with + | BetreeListCons x next_msgs => + let (i, m) := x in + if i s>= key + then Return (BetreeListCons (i, m) next_msgs) + else ( + l <- betree_node_lookup_first_message_for_key_fwd n0 key next_msgs; + Return l) + | BetreeListNil => Return BetreeListNil + end + end +. + +(** [betree_main::betree::Node::{5}::lookup_first_message_for_key] *) +Fixpoint betree_node_lookup_first_message_for_key_back + (n : nat) (key : u64) (msgs : Betree_list_t (u64 * Betree_message_t)) + (ret : Betree_list_t (u64 * Betree_message_t)) : + result (Betree_list_t (u64 * Betree_message_t)) + := + match n with + | O => Fail_ OutOfFuel + | S n0 => + match msgs with + | BetreeListCons x next_msgs => + let (i, m) := x in + if i s>= key + then Return ret + else ( + next_msgs0 <- + betree_node_lookup_first_message_for_key_back n0 key next_msgs ret; + Return (BetreeListCons (i, m) next_msgs0)) + | BetreeListNil => Return ret + end + end +. + +(** [betree_main::betree::Node::{5}::apply_upserts] *) +Fixpoint betree_node_apply_upserts_fwd + (n : nat) (msgs : Betree_list_t (u64 * Betree_message_t)) (prev : option u64) + (key : u64) (st : state) : + result (state * u64) + := + match n with + | O => Fail_ OutOfFuel + | S n0 => + b <- betree_list_head_has_key_fwd Betree_message_t msgs key; + if b + then ( + msg <- betree_list_pop_front_fwd (u64 * Betree_message_t) msgs; + let (_, m) := msg in + match m with + | BetreeMessageInsert i => Fail_ Failure + | BetreeMessageDelete => Fail_ Failure + | BetreeMessageUpsert s => + v <- betree_upsert_update_fwd prev s; + msgs0 <- betree_list_pop_front_back (u64 * Betree_message_t) msgs; + p <- betree_node_apply_upserts_fwd n0 msgs0 (Some v) key st; + let (st0, i) := p in + Return (st0, i) + end) + else ( + p <- core_option_option_unwrap_fwd u64 prev st; + let (st0, v) := p in + l <- + betree_list_push_front_fwd_back (u64 * Betree_message_t) msgs (key, + BetreeMessageInsert v); + let _ := l in + Return (st0, v)) + end +. + +(** [betree_main::betree::Node::{5}::apply_upserts] *) +Fixpoint betree_node_apply_upserts_back + (n : nat) (msgs : Betree_list_t (u64 * Betree_message_t)) (prev : option u64) + (key : u64) (st : state) : + result (Betree_list_t (u64 * Betree_message_t)) + := + match n with + | O => Fail_ OutOfFuel + | S n0 => + b <- betree_list_head_has_key_fwd Betree_message_t msgs key; + if b + then ( + msg <- betree_list_pop_front_fwd (u64 * Betree_message_t) msgs; + let (_, m) := msg in + match m with + | BetreeMessageInsert i => Fail_ Failure + | BetreeMessageDelete => Fail_ Failure + | BetreeMessageUpsert s => + v <- betree_upsert_update_fwd prev s; + msgs0 <- betree_list_pop_front_back (u64 * Betree_message_t) msgs; + msgs1 <- betree_node_apply_upserts_back n0 msgs0 (Some v) key st; + Return msgs1 + end) + else ( + p <- core_option_option_unwrap_fwd u64 prev st; + let (_, v) := p in + msgs0 <- + betree_list_push_front_fwd_back (u64 * Betree_message_t) msgs (key, + BetreeMessageInsert v); + Return msgs0) + end +. + +(** [betree_main::betree::Node::{5}::lookup] *) +Fixpoint betree_node_lookup_fwd + (n : nat) (self : Betree_node_t) (key : u64) (st : state) : + result (state * (option u64)) + := + match n with + | O => Fail_ OutOfFuel + | S n0 => + match self with + | BetreeNodeInternal node => + match node with + | mkBetree_internal_t i i0 n1 n2 => + p <- betree_load_internal_node_fwd i st; + let (st0, msgs) := p in + pending <- betree_node_lookup_first_message_for_key_fwd n0 key msgs; + match pending with + | BetreeListCons p0 l => + let (k, msg) := p0 in + if k s<> key + then ( + p1 <- + betree_internal_lookup_in_children_fwd n0 (mkBetree_internal_t i + i0 n1 n2) key st0; + let (st1, opt) := p1 in + l0 <- + betree_node_lookup_first_message_for_key_back n0 key msgs + (BetreeListCons (k, msg) l); + let _ := l0 in + Return (st1, opt)) + else + match msg with + | BetreeMessageInsert v => + l0 <- + betree_node_lookup_first_message_for_key_back n0 key msgs + (BetreeListCons (k, BetreeMessageInsert v) l); + let _ := l0 in + Return (st0, Some v) + | BetreeMessageDelete => + l0 <- + betree_node_lookup_first_message_for_key_back n0 key msgs + (BetreeListCons (k, BetreeMessageDelete) l); + let _ := l0 in + Return (st0, None) + | BetreeMessageUpsert ufs => + p1 <- + betree_internal_lookup_in_children_fwd n0 (mkBetree_internal_t + i i0 n1 n2) key st0; + let (st1, v) := p1 in + p2 <- + betree_node_apply_upserts_fwd n0 (BetreeListCons (k, + BetreeMessageUpsert ufs) l) v key st1; + let (st2, v0) := p2 in + node0 <- + betree_internal_lookup_in_children_back n0 (mkBetree_internal_t + i i0 n1 n2) key st0; + match node0 with + | mkBetree_internal_t i1 i2 n3 n4 => + pending0 <- + betree_node_apply_upserts_back n0 (BetreeListCons (k, + BetreeMessageUpsert ufs) l) v key st1; + msgs0 <- + betree_node_lookup_first_message_for_key_back n0 key msgs + pending0; + p3 <- betree_store_internal_node_fwd i1 msgs0 st2; + let (st3, _) := p3 in + Return (st3, Some v0) + end + end + | BetreeListNil => + p0 <- + betree_internal_lookup_in_children_fwd n0 (mkBetree_internal_t i i0 + n1 n2) key st0; + let (st1, opt) := p0 in + l <- + betree_node_lookup_first_message_for_key_back n0 key msgs + BetreeListNil; + let _ := l in + Return (st1, opt) + end + end + | BetreeNodeLeaf node => + match node with + | mkBetree_leaf_t i i0 => + p <- betree_load_leaf_node_fwd i st; + let (st0, bindings) := p in + opt <- betree_node_lookup_in_bindings_fwd n0 key bindings; + Return (st0, opt) + end + end + end + +(** [betree_main::betree::Node::{5}::lookup] *) +with betree_node_lookup_back + (n : nat) (self : Betree_node_t) (key : u64) (st : state) : + result Betree_node_t + := + match n with + | O => Fail_ OutOfFuel + | S n0 => + match self with + | BetreeNodeInternal node => + match node with + | mkBetree_internal_t i i0 n1 n2 => + p <- betree_load_internal_node_fwd i st; + let (st0, msgs) := p in + pending <- betree_node_lookup_first_message_for_key_fwd n0 key msgs; + match pending with + | BetreeListCons p0 l => + let (k, msg) := p0 in + if k s<> key + then ( + l0 <- + betree_node_lookup_first_message_for_key_back n0 key msgs + (BetreeListCons (k, msg) l); + let _ := l0 in + node0 <- + betree_internal_lookup_in_children_back n0 (mkBetree_internal_t i + i0 n1 n2) key st0; + Return (BetreeNodeInternal node0)) + else + match msg with + | BetreeMessageInsert v => + l0 <- + betree_node_lookup_first_message_for_key_back n0 key msgs + (BetreeListCons (k, BetreeMessageInsert v) l); + let _ := l0 in + Return (BetreeNodeInternal (mkBetree_internal_t i i0 n1 n2)) + | BetreeMessageDelete => + l0 <- + betree_node_lookup_first_message_for_key_back n0 key msgs + (BetreeListCons (k, BetreeMessageDelete) l); + let _ := l0 in + Return (BetreeNodeInternal (mkBetree_internal_t i i0 n1 n2)) + | BetreeMessageUpsert ufs => + p1 <- + betree_internal_lookup_in_children_fwd n0 (mkBetree_internal_t + i i0 n1 n2) key st0; + let (st1, v) := p1 in + p2 <- + betree_node_apply_upserts_fwd n0 (BetreeListCons (k, + BetreeMessageUpsert ufs) l) v key st1; + let (st2, _) := p2 in + node0 <- + betree_internal_lookup_in_children_back n0 (mkBetree_internal_t + i i0 n1 n2) key st0; + match node0 with + | mkBetree_internal_t i1 i2 n3 n4 => + pending0 <- + betree_node_apply_upserts_back n0 (BetreeListCons (k, + BetreeMessageUpsert ufs) l) v key st1; + msgs0 <- + betree_node_lookup_first_message_for_key_back n0 key msgs + pending0; + p3 <- betree_store_internal_node_fwd i1 msgs0 st2; + let (_, _) := p3 in + Return (BetreeNodeInternal (mkBetree_internal_t i1 i2 n3 n4)) + end + end + | BetreeListNil => + l <- + betree_node_lookup_first_message_for_key_back n0 key msgs + BetreeListNil; + let _ := l in + node0 <- + betree_internal_lookup_in_children_back n0 (mkBetree_internal_t i + i0 n1 n2) key st0; + Return (BetreeNodeInternal node0) + end + end + | BetreeNodeLeaf node => + match node with + | mkBetree_leaf_t i i0 => + p <- betree_load_leaf_node_fwd i st; + let (_, bindings) := p in + opt <- betree_node_lookup_in_bindings_fwd n0 key bindings; + let _ := opt in + Return (BetreeNodeLeaf (mkBetree_leaf_t i i0)) + end + end + end + +(** [betree_main::betree::Internal::{4}::lookup_in_children] *) +with betree_internal_lookup_in_children_fwd + (n : nat) (self : Betree_internal_t) (key : u64) (st : state) : + result (state * (option u64)) + := + match n with + | O => Fail_ OutOfFuel + | S n0 => + match self with + | mkBetree_internal_t i i0 n1 n2 => + if key s< i0 + then ( + p <- betree_node_lookup_fwd n0 n1 key st; + let (st0, opt) := p in + Return (st0, opt)) + else ( + p <- betree_node_lookup_fwd n0 n2 key st; + let (st0, opt) := p in + Return (st0, opt)) + end + end + +(** [betree_main::betree::Internal::{4}::lookup_in_children] *) +with betree_internal_lookup_in_children_back + (n : nat) (self : Betree_internal_t) (key : u64) (st : state) : + result Betree_internal_t + := + match n with + | O => Fail_ OutOfFuel + | S n0 => + match self with + | mkBetree_internal_t i i0 n1 n2 => + if key s< i0 + then ( + n3 <- betree_node_lookup_back n0 n1 key st; + Return (mkBetree_internal_t i i0 n3 n2)) + else ( + n3 <- betree_node_lookup_back n0 n2 key st; + Return (mkBetree_internal_t i i0 n1 n3)) + end + end +. + +(** [betree_main::betree::Node::{5}::lookup_mut_in_bindings] *) +Fixpoint betree_node_lookup_mut_in_bindings_fwd + (n : nat) (key : u64) (bindings : Betree_list_t (u64 * u64)) : + result (Betree_list_t (u64 * u64)) + := + match n with + | O => Fail_ OutOfFuel + | S n0 => + match bindings with + | BetreeListCons hd tl => + let (i, i0) := hd in + if i s>= key + then Return (BetreeListCons (i, i0) tl) + else (l <- betree_node_lookup_mut_in_bindings_fwd n0 key tl; Return l) + | BetreeListNil => Return BetreeListNil + end + end +. + +(** [betree_main::betree::Node::{5}::lookup_mut_in_bindings] *) +Fixpoint betree_node_lookup_mut_in_bindings_back + (n : nat) (key : u64) (bindings : Betree_list_t (u64 * u64)) + (ret : Betree_list_t (u64 * u64)) : + result (Betree_list_t (u64 * u64)) + := + match n with + | O => Fail_ OutOfFuel + | S n0 => + match bindings with + | BetreeListCons hd tl => + let (i, i0) := hd in + if i s>= key + then Return ret + else ( + tl0 <- betree_node_lookup_mut_in_bindings_back n0 key tl ret; + Return (BetreeListCons (i, i0) tl0)) + | BetreeListNil => Return ret + end + end +. + +(** [betree_main::betree::Node::{5}::apply_to_leaf] *) +Definition betree_node_apply_to_leaf_fwd_back + (n : nat) (bindings : Betree_list_t (u64 * u64)) (key : u64) + (new_msg : Betree_message_t) : + result (Betree_list_t (u64 * u64)) + := + match n with + | O => Fail_ OutOfFuel + | S n0 => + bindings0 <- betree_node_lookup_mut_in_bindings_fwd n0 key bindings; + b <- betree_list_head_has_key_fwd u64 bindings0 key; + if b + then ( + hd <- betree_list_pop_front_fwd (u64 * u64) bindings0; + match new_msg with + | BetreeMessageInsert v => + bindings1 <- betree_list_pop_front_back (u64 * u64) bindings0; + bindings2 <- + betree_list_push_front_fwd_back (u64 * u64) bindings1 (key, v); + bindings3 <- + betree_node_lookup_mut_in_bindings_back n0 key bindings bindings2; + Return bindings3 + | BetreeMessageDelete => + bindings1 <- betree_list_pop_front_back (u64 * u64) bindings0; + bindings2 <- + betree_node_lookup_mut_in_bindings_back n0 key bindings bindings1; + Return bindings2 + | BetreeMessageUpsert s => + let (_, i) := hd in + v <- betree_upsert_update_fwd (Some i) s; + bindings1 <- betree_list_pop_front_back (u64 * u64) bindings0; + bindings2 <- + betree_list_push_front_fwd_back (u64 * u64) bindings1 (key, v); + bindings3 <- + betree_node_lookup_mut_in_bindings_back n0 key bindings bindings2; + Return bindings3 + end) + else + match new_msg with + | BetreeMessageInsert v => + bindings1 <- + betree_list_push_front_fwd_back (u64 * u64) bindings0 (key, v); + bindings2 <- + betree_node_lookup_mut_in_bindings_back n0 key bindings bindings1; + Return bindings2 + | BetreeMessageDelete => + bindings1 <- + betree_node_lookup_mut_in_bindings_back n0 key bindings bindings0; + Return bindings1 + | BetreeMessageUpsert s => + v <- betree_upsert_update_fwd None s; + bindings1 <- + betree_list_push_front_fwd_back (u64 * u64) bindings0 (key, v); + bindings2 <- + betree_node_lookup_mut_in_bindings_back n0 key bindings bindings1; + Return bindings2 + end + end +. + +(** [betree_main::betree::Node::{5}::apply_messages_to_leaf] *) +Fixpoint betree_node_apply_messages_to_leaf_fwd_back + (n : nat) (bindings : Betree_list_t (u64 * u64)) + (new_msgs : Betree_list_t (u64 * Betree_message_t)) : + result (Betree_list_t (u64 * u64)) + := + match n with + | O => Fail_ OutOfFuel + | S n0 => + match new_msgs with + | BetreeListCons new_msg new_msgs_tl => + let (i, m) := new_msg in + bindings0 <- betree_node_apply_to_leaf_fwd_back n0 bindings i m; + bindings1 <- + betree_node_apply_messages_to_leaf_fwd_back n0 bindings0 new_msgs_tl; + Return bindings1 + | BetreeListNil => Return bindings + end + end +. + +(** [betree_main::betree::Node::{5}::filter_messages_for_key] *) +Fixpoint betree_node_filter_messages_for_key_fwd_back + (n : nat) (key : u64) (msgs : Betree_list_t (u64 * Betree_message_t)) : + result (Betree_list_t (u64 * Betree_message_t)) + := + match n with + | O => Fail_ OutOfFuel + | S n0 => + match msgs with + | BetreeListCons p l => + let (k, m) := p in + if k s= key + then ( + msgs0 <- + betree_list_pop_front_back (u64 * Betree_message_t) (BetreeListCons + (k, m) l); + msgs1 <- betree_node_filter_messages_for_key_fwd_back n0 key msgs0; + Return msgs1) + else Return (BetreeListCons (k, m) l) + | BetreeListNil => Return BetreeListNil + end + end +. + +(** [betree_main::betree::Node::{5}::lookup_first_message_after_key] *) +Fixpoint betree_node_lookup_first_message_after_key_fwd + (n : nat) (key : u64) (msgs : Betree_list_t (u64 * Betree_message_t)) : + result (Betree_list_t (u64 * Betree_message_t)) + := + match n with + | O => Fail_ OutOfFuel + | S n0 => + match msgs with + | BetreeListCons p next_msgs => + let (k, m) := p in + if k s= key + then ( + l <- betree_node_lookup_first_message_after_key_fwd n0 key next_msgs; + Return l) + else Return (BetreeListCons (k, m) next_msgs) + | BetreeListNil => Return BetreeListNil + end + end +. + +(** [betree_main::betree::Node::{5}::lookup_first_message_after_key] *) +Fixpoint betree_node_lookup_first_message_after_key_back + (n : nat) (key : u64) (msgs : Betree_list_t (u64 * Betree_message_t)) + (ret : Betree_list_t (u64 * Betree_message_t)) : + result (Betree_list_t (u64 * Betree_message_t)) + := + match n with + | O => Fail_ OutOfFuel + | S n0 => + match msgs with + | BetreeListCons p next_msgs => + let (k, m) := p in + if k s= key + then ( + next_msgs0 <- + betree_node_lookup_first_message_after_key_back n0 key next_msgs ret; + Return (BetreeListCons (k, m) next_msgs0)) + else Return ret + | BetreeListNil => Return ret + end + end +. + +(** [betree_main::betree::Node::{5}::apply_to_internal] *) +Definition betree_node_apply_to_internal_fwd_back + (n : nat) (msgs : Betree_list_t (u64 * Betree_message_t)) (key : u64) + (new_msg : Betree_message_t) : + result (Betree_list_t (u64 * Betree_message_t)) + := + match n with + | O => Fail_ OutOfFuel + | S n0 => + msgs0 <- betree_node_lookup_first_message_for_key_fwd n0 key msgs; + b <- betree_list_head_has_key_fwd Betree_message_t msgs0 key; + if b + then + match new_msg with + | BetreeMessageInsert i => + msgs1 <- betree_node_filter_messages_for_key_fwd_back n0 key msgs0; + msgs2 <- + betree_list_push_front_fwd_back (u64 * Betree_message_t) msgs1 (key, + BetreeMessageInsert i); + msgs3 <- + betree_node_lookup_first_message_for_key_back n0 key msgs msgs2; + Return msgs3 + | BetreeMessageDelete => + msgs1 <- betree_node_filter_messages_for_key_fwd_back n0 key msgs0; + msgs2 <- + betree_list_push_front_fwd_back (u64 * Betree_message_t) msgs1 (key, + BetreeMessageDelete); + msgs3 <- + betree_node_lookup_first_message_for_key_back n0 key msgs msgs2; + Return msgs3 + | BetreeMessageUpsert s => + p <- betree_list_hd_fwd (u64 * Betree_message_t) msgs0; + let (_, m) := p in + match m with + | BetreeMessageInsert prev => + v <- betree_upsert_update_fwd (Some prev) s; + msgs1 <- betree_list_pop_front_back (u64 * Betree_message_t) msgs0; + msgs2 <- + betree_list_push_front_fwd_back (u64 * Betree_message_t) msgs1 + (key, BetreeMessageInsert v); + msgs3 <- + betree_node_lookup_first_message_for_key_back n0 key msgs msgs2; + Return msgs3 + | BetreeMessageDelete => + v <- betree_upsert_update_fwd None s; + msgs1 <- betree_list_pop_front_back (u64 * Betree_message_t) msgs0; + msgs2 <- + betree_list_push_front_fwd_back (u64 * Betree_message_t) msgs1 + (key, BetreeMessageInsert v); + msgs3 <- + betree_node_lookup_first_message_for_key_back n0 key msgs msgs2; + Return msgs3 + | BetreeMessageUpsert ufs => + msgs1 <- betree_node_lookup_first_message_after_key_fwd n0 key msgs0; + msgs2 <- + betree_list_push_front_fwd_back (u64 * Betree_message_t) msgs1 + (key, BetreeMessageUpsert s); + msgs3 <- + betree_node_lookup_first_message_after_key_back n0 key msgs0 msgs2; + msgs4 <- + betree_node_lookup_first_message_for_key_back n0 key msgs msgs3; + Return msgs4 + end + end + else ( + msgs1 <- + betree_list_push_front_fwd_back (u64 * Betree_message_t) msgs0 (key, + new_msg); + msgs2 <- betree_node_lookup_first_message_for_key_back n0 key msgs msgs1; + Return msgs2) + end +. + +(** [betree_main::betree::Node::{5}::apply_messages_to_internal] *) +Fixpoint betree_node_apply_messages_to_internal_fwd_back + (n : nat) (msgs : Betree_list_t (u64 * Betree_message_t)) + (new_msgs : Betree_list_t (u64 * Betree_message_t)) : + result (Betree_list_t (u64 * Betree_message_t)) + := + match n with + | O => Fail_ OutOfFuel + | S n0 => + match new_msgs with + | BetreeListCons new_msg new_msgs_tl => + let (i, m) := new_msg in + msgs0 <- betree_node_apply_to_internal_fwd_back n0 msgs i m; + msgs1 <- + betree_node_apply_messages_to_internal_fwd_back n0 msgs0 new_msgs_tl; + Return msgs1 + | BetreeListNil => Return msgs + end + end +. + +(** [betree_main::betree::Node::{5}::apply_messages] *) +Fixpoint betree_node_apply_messages_fwd + (n : nat) (self : Betree_node_t) (params : Betree_params_t) + (node_id_cnt : Betree_node_id_counter_t) + (msgs : Betree_list_t (u64 * Betree_message_t)) (st : state) : + result (state * unit) + := + match n with + | O => Fail_ OutOfFuel + | S n0 => + match self with + | BetreeNodeInternal node => + match node with + | mkBetree_internal_t i i0 n1 n2 => + p <- betree_load_internal_node_fwd i st; + let (st0, content) := p in + content0 <- + betree_node_apply_messages_to_internal_fwd_back n0 content msgs; + num_msgs <- betree_list_len_fwd (u64 * Betree_message_t) n0 content0; + match params with + | mkBetree_params_t i1 i2 => + if num_msgs s>= i1 + then ( + p0 <- + betree_internal_flush_fwd n0 (mkBetree_internal_t i i0 n1 n2) + (mkBetree_params_t i1 i2) node_id_cnt content0 st0; + let (st1, content1) := p0 in + p1 <- + betree_internal_flush_back n0 (mkBetree_internal_t i i0 n1 n2) + (mkBetree_params_t i1 i2) node_id_cnt content0 st0; + let (node0, _) := p1 in + match node0 with + | mkBetree_internal_t i3 i4 n3 n4 => + p2 <- betree_store_internal_node_fwd i3 content1 st1; + let (st2, _) := p2 in + Return (st2, tt) + end) + else ( + p0 <- betree_store_internal_node_fwd i content0 st0; + let (st1, _) := p0 in + Return (st1, tt)) + end + end + | BetreeNodeLeaf node => + match node with + | mkBetree_leaf_t i i0 => + p <- betree_load_leaf_node_fwd i st; + let (st0, content) := p in + content0 <- + betree_node_apply_messages_to_leaf_fwd_back n0 content msgs; + len <- betree_list_len_fwd (u64 * u64) n0 content0; + match params with + | mkBetree_params_t i1 i2 => + i3 <- u64_mul 2%u64 i2; + if len s>= i3 + then ( + p0 <- + betree_leaf_split_fwd n0 (mkBetree_leaf_t i i0) content0 + (mkBetree_params_t i1 i2) node_id_cnt st0; + let (st1, _) := p0 in + p1 <- betree_store_leaf_node_fwd i BetreeListNil st1; + let (st2, _) := p1 in + Return (st2, tt)) + else ( + p0 <- betree_store_leaf_node_fwd i content0 st0; + let (st1, _) := p0 in + Return (st1, tt)) + end + end + end + end + +(** [betree_main::betree::Node::{5}::apply_messages] *) +with betree_node_apply_messages_back + (n : nat) (self : Betree_node_t) (params : Betree_params_t) + (node_id_cnt : Betree_node_id_counter_t) + (msgs : Betree_list_t (u64 * Betree_message_t)) (st : state) : + result (Betree_node_t * Betree_node_id_counter_t) + := + match n with + | O => Fail_ OutOfFuel + | S n0 => + match self with + | BetreeNodeInternal node => + match node with + | mkBetree_internal_t i i0 n1 n2 => + p <- betree_load_internal_node_fwd i st; + let (st0, content) := p in + content0 <- + betree_node_apply_messages_to_internal_fwd_back n0 content msgs; + num_msgs <- betree_list_len_fwd (u64 * Betree_message_t) n0 content0; + match params with + | mkBetree_params_t i1 i2 => + if num_msgs s>= i1 + then ( + p0 <- + betree_internal_flush_fwd n0 (mkBetree_internal_t i i0 n1 n2) + (mkBetree_params_t i1 i2) node_id_cnt content0 st0; + let (st1, content1) := p0 in + p1 <- + betree_internal_flush_back n0 (mkBetree_internal_t i i0 n1 n2) + (mkBetree_params_t i1 i2) node_id_cnt content0 st0; + let (node0, node_id_cnt0) := p1 in + match node0 with + | mkBetree_internal_t i3 i4 n3 n4 => + p2 <- betree_store_internal_node_fwd i3 content1 st1; + let (_, _) := p2 in + Return (BetreeNodeInternal (mkBetree_internal_t i3 i4 n3 n4), + node_id_cnt0) + end) + else ( + p0 <- betree_store_internal_node_fwd i content0 st0; + let (_, _) := p0 in + Return (BetreeNodeInternal (mkBetree_internal_t i i0 n1 n2), + node_id_cnt)) + end + end + | BetreeNodeLeaf node => + match node with + | mkBetree_leaf_t i i0 => + p <- betree_load_leaf_node_fwd i st; + let (st0, content) := p in + content0 <- + betree_node_apply_messages_to_leaf_fwd_back n0 content msgs; + len <- betree_list_len_fwd (u64 * u64) n0 content0; + match params with + | mkBetree_params_t i1 i2 => + i3 <- u64_mul 2%u64 i2; + if len s>= i3 + then ( + p0 <- + betree_leaf_split_fwd n0 (mkBetree_leaf_t i i0) content0 + (mkBetree_params_t i1 i2) node_id_cnt st0; + let (st1, new_node) := p0 in + p1 <- betree_store_leaf_node_fwd i BetreeListNil st1; + let (_, _) := p1 in + node_id_cnt0 <- + betree_leaf_split_back n0 (mkBetree_leaf_t i i0) content0 + (mkBetree_params_t i1 i2) node_id_cnt st0; + Return (BetreeNodeInternal new_node, node_id_cnt0)) + else ( + p0 <- betree_store_leaf_node_fwd i content0 st0; + let (_, _) := p0 in + Return (BetreeNodeLeaf (mkBetree_leaf_t i len), node_id_cnt)) + end + end + end + end + +(** [betree_main::betree::Internal::{4}::flush] *) +with betree_internal_flush_fwd + (n : nat) (self : Betree_internal_t) (params : Betree_params_t) + (node_id_cnt : Betree_node_id_counter_t) + (content : Betree_list_t (u64 * Betree_message_t)) (st : state) : + result (state * (Betree_list_t (u64 * Betree_message_t))) + := + match n with + | O => Fail_ OutOfFuel + | S n0 => + match self with + | mkBetree_internal_t i i0 n1 n2 => + p <- betree_list_partition_at_pivot_fwd Betree_message_t n0 content i0; + let (msgs_left, msgs_right) := p in + len_left <- betree_list_len_fwd (u64 * Betree_message_t) n0 msgs_left; + match params with + | mkBetree_params_t i1 i2 => + if len_left s>= i1 + then ( + p0 <- + betree_node_apply_messages_fwd n0 n1 (mkBetree_params_t i1 i2) + node_id_cnt msgs_left st; + let (st0, _) := p0 in + p1 <- + betree_node_apply_messages_back n0 n1 (mkBetree_params_t i1 i2) + node_id_cnt msgs_left st; + let (_, node_id_cnt0) := p1 in + len_right <- + betree_list_len_fwd (u64 * Betree_message_t) n0 msgs_right; + if len_right s>= i1 + then ( + p2 <- + betree_node_apply_messages_fwd n0 n2 (mkBetree_params_t i1 i2) + node_id_cnt0 msgs_right st0; + let (st1, _) := p2 in + p3 <- + betree_node_apply_messages_back n0 n2 (mkBetree_params_t i1 i2) + node_id_cnt0 msgs_right st0; + let (_, _) := p3 in + Return (st1, BetreeListNil)) + else Return (st0, msgs_right)) + else ( + p0 <- + betree_node_apply_messages_fwd n0 n2 (mkBetree_params_t i1 i2) + node_id_cnt msgs_right st; + let (st0, _) := p0 in + p1 <- + betree_node_apply_messages_back n0 n2 (mkBetree_params_t i1 i2) + node_id_cnt msgs_right st; + let (_, _) := p1 in + Return (st0, msgs_left)) + end + end + end + +(** [betree_main::betree::Internal::{4}::flush] *) +with betree_internal_flush_back + (n : nat) (self : Betree_internal_t) (params : Betree_params_t) + (node_id_cnt : Betree_node_id_counter_t) + (content : Betree_list_t (u64 * Betree_message_t)) (st : state) : + result (Betree_internal_t * Betree_node_id_counter_t) + := + match n with + | O => Fail_ OutOfFuel + | S n0 => + match self with + | mkBetree_internal_t i i0 n1 n2 => + p <- betree_list_partition_at_pivot_fwd Betree_message_t n0 content i0; + let (msgs_left, msgs_right) := p in + len_left <- betree_list_len_fwd (u64 * Betree_message_t) n0 msgs_left; + match params with + | mkBetree_params_t i1 i2 => + if len_left s>= i1 + then ( + p0 <- + betree_node_apply_messages_fwd n0 n1 (mkBetree_params_t i1 i2) + node_id_cnt msgs_left st; + let (st0, _) := p0 in + p1 <- + betree_node_apply_messages_back n0 n1 (mkBetree_params_t i1 i2) + node_id_cnt msgs_left st; + let (n3, node_id_cnt0) := p1 in + len_right <- + betree_list_len_fwd (u64 * Betree_message_t) n0 msgs_right; + if len_right s>= i1 + then ( + p2 <- + betree_node_apply_messages_back n0 n2 (mkBetree_params_t i1 i2) + node_id_cnt0 msgs_right st0; + let (n4, node_id_cnt1) := p2 in + Return (mkBetree_internal_t i i0 n3 n4, node_id_cnt1)) + else Return (mkBetree_internal_t i i0 n3 n2, node_id_cnt0)) + else ( + p0 <- + betree_node_apply_messages_back n0 n2 (mkBetree_params_t i1 i2) + node_id_cnt msgs_right st; + let (n3, node_id_cnt0) := p0 in + Return (mkBetree_internal_t i i0 n1 n3, node_id_cnt0)) + end + end + end +. + +(** [betree_main::betree::Node::{5}::apply] *) +Definition betree_node_apply_fwd + (n : nat) (self : Betree_node_t) (params : Betree_params_t) + (node_id_cnt : Betree_node_id_counter_t) (key : u64) + (new_msg : Betree_message_t) (st : state) : + result (state * unit) + := + match n with + | O => Fail_ OutOfFuel + | S n0 => + let l := BetreeListNil in + p <- + betree_node_apply_messages_fwd n0 self params node_id_cnt (BetreeListCons + (key, new_msg) l) st; + let (st0, _) := p in + p0 <- + betree_node_apply_messages_back n0 self params node_id_cnt + (BetreeListCons (key, new_msg) l) st; + let (_, _) := p0 in + Return (st0, tt) + end +. + +(** [betree_main::betree::Node::{5}::apply] *) +Definition betree_node_apply_back + (n : nat) (self : Betree_node_t) (params : Betree_params_t) + (node_id_cnt : Betree_node_id_counter_t) (key : u64) + (new_msg : Betree_message_t) (st : state) : + result (Betree_node_t * Betree_node_id_counter_t) + := + match n with + | O => Fail_ OutOfFuel + | S n0 => + let l := BetreeListNil in + p <- + betree_node_apply_messages_back n0 self params node_id_cnt + (BetreeListCons (key, new_msg) l) st; + let (self0, node_id_cnt0) := p in + Return (self0, node_id_cnt0) + end +. + +(** [betree_main::betree::BeTree::{6}::new] *) +Definition betree_be_tree_new_fwd + (min_flush_size : u64) (split_size : u64) (st : state) : + result (state * Betree_be_tree_t) + := + node_id_cnt <- betree_node_id_counter_new_fwd; + id <- betree_node_id_counter_fresh_id_fwd node_id_cnt; + p <- betree_store_leaf_node_fwd id BetreeListNil st; + let (st0, _) := p in + node_id_cnt0 <- betree_node_id_counter_fresh_id_back node_id_cnt; + Return (st0, mkBetree_be_tree_t (mkBetree_params_t min_flush_size split_size) + node_id_cnt0 (BetreeNodeLeaf (mkBetree_leaf_t id (0%u64)))) +. + +(** [betree_main::betree::BeTree::{6}::apply] *) +Definition betree_be_tree_apply_fwd + (n : nat) (self : Betree_be_tree_t) (key : u64) (msg : Betree_message_t) + (st : state) : + result (state * unit) + := + match n with + | O => Fail_ OutOfFuel + | S n0 => + match self with + | mkBetree_be_tree_t p nic n1 => + p0 <- betree_node_apply_fwd n0 n1 p nic key msg st; + let (st0, _) := p0 in + p1 <- betree_node_apply_back n0 n1 p nic key msg st; + let (_, _) := p1 in + Return (st0, tt) + end + end +. + +(** [betree_main::betree::BeTree::{6}::apply] *) +Definition betree_be_tree_apply_back + (n : nat) (self : Betree_be_tree_t) (key : u64) (msg : Betree_message_t) + (st : state) : + result Betree_be_tree_t + := + match n with + | O => Fail_ OutOfFuel + | S n0 => + match self with + | mkBetree_be_tree_t p nic n1 => + p0 <- betree_node_apply_back n0 n1 p nic key msg st; + let (n2, nic0) := p0 in + Return (mkBetree_be_tree_t p nic0 n2) + end + end +. + +(** [betree_main::betree::BeTree::{6}::insert] *) +Definition betree_be_tree_insert_fwd + (n : nat) (self : Betree_be_tree_t) (key : u64) (value : u64) (st : state) : + result (state * unit) + := + match n with + | O => Fail_ OutOfFuel + | S n0 => + p <- betree_be_tree_apply_fwd n0 self key (BetreeMessageInsert value) st; + let (st0, _) := p in + bt <- betree_be_tree_apply_back n0 self key (BetreeMessageInsert value) st; + let _ := bt in + Return (st0, tt) + end +. + +(** [betree_main::betree::BeTree::{6}::insert] *) +Definition betree_be_tree_insert_back + (n : nat) (self : Betree_be_tree_t) (key : u64) (value : u64) (st : state) : + result Betree_be_tree_t + := + match n with + | O => Fail_ OutOfFuel + | S n0 => + self0 <- + betree_be_tree_apply_back n0 self key (BetreeMessageInsert value) st; + Return self0 + end +. + +(** [betree_main::betree::BeTree::{6}::delete] *) +Definition betree_be_tree_delete_fwd + (n : nat) (self : Betree_be_tree_t) (key : u64) (st : state) : + result (state * unit) + := + match n with + | O => Fail_ OutOfFuel + | S n0 => + p <- betree_be_tree_apply_fwd n0 self key BetreeMessageDelete st; + let (st0, _) := p in + bt <- betree_be_tree_apply_back n0 self key BetreeMessageDelete st; + let _ := bt in + Return (st0, tt) + end +. + +(** [betree_main::betree::BeTree::{6}::delete] *) +Definition betree_be_tree_delete_back + (n : nat) (self : Betree_be_tree_t) (key : u64) (st : state) : + result Betree_be_tree_t + := + match n with + | O => Fail_ OutOfFuel + | S n0 => + self0 <- betree_be_tree_apply_back n0 self key BetreeMessageDelete st; + Return self0 + end +. + +(** [betree_main::betree::BeTree::{6}::upsert] *) +Definition betree_be_tree_upsert_fwd + (n : nat) (self : Betree_be_tree_t) (key : u64) + (upd : Betree_upsert_fun_state_t) (st : state) : + result (state * unit) + := + match n with + | O => Fail_ OutOfFuel + | S n0 => + p <- betree_be_tree_apply_fwd n0 self key (BetreeMessageUpsert upd) st; + let (st0, _) := p in + bt <- betree_be_tree_apply_back n0 self key (BetreeMessageUpsert upd) st; + let _ := bt in + Return (st0, tt) + end +. + +(** [betree_main::betree::BeTree::{6}::upsert] *) +Definition betree_be_tree_upsert_back + (n : nat) (self : Betree_be_tree_t) (key : u64) + (upd : Betree_upsert_fun_state_t) (st : state) : + result Betree_be_tree_t + := + match n with + | O => Fail_ OutOfFuel + | S n0 => + self0 <- + betree_be_tree_apply_back n0 self key (BetreeMessageUpsert upd) st; + Return self0 + end +. + +(** [betree_main::betree::BeTree::{6}::lookup] *) +Definition betree_be_tree_lookup_fwd + (n : nat) (self : Betree_be_tree_t) (key : u64) (st : state) : + result (state * (option u64)) + := + match n with + | O => Fail_ OutOfFuel + | S n0 => + match self with + | mkBetree_be_tree_t p nic n1 => + p0 <- betree_node_lookup_fwd n0 n1 key st; + let (st0, opt) := p0 in + Return (st0, opt) + end + end +. + +(** [betree_main::betree::BeTree::{6}::lookup] *) +Definition betree_be_tree_lookup_back + (n : nat) (self : Betree_be_tree_t) (key : u64) (st : state) : + result Betree_be_tree_t + := + match n with + | O => Fail_ OutOfFuel + | S n0 => + match self with + | mkBetree_be_tree_t p nic n1 => + n2 <- betree_node_lookup_back n0 n1 key st; + Return (mkBetree_be_tree_t p nic n2) + end + end +. + +(** [betree_main::main] *) +Definition main_fwd : result unit := Return tt. + +End BetreeMain_Funs . diff --git a/tests/coq/betree/BetreeMain_Opaque.v b/tests/coq/betree/BetreeMain_Opaque.v new file mode 100644 index 00000000..08ab530a --- /dev/null +++ b/tests/coq/betree/BetreeMain_Opaque.v @@ -0,0 +1,38 @@ +(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *) +(** [betree_main]: opaque function definitions *) +Require Import Primitives. +Import Primitives. +Require Import Coq.ZArith.ZArith. +Local Open Scope Primitives_scope. +Require Export BetreeMain_Types. +Import BetreeMain_Types. +Module BetreeMain_Opaque. + +(** [betree_main::betree_utils::load_internal_node] *) +Axiom betree_utils_load_internal_node_fwd + : u64 -> state -> result (state * (Betree_list_t (u64 * Betree_message_t))) +. + +(** [betree_main::betree_utils::store_internal_node] *) +Axiom betree_utils_store_internal_node_fwd + : + u64 -> Betree_list_t (u64 * Betree_message_t) -> state -> result (state * + unit) +. + +(** [betree_main::betree_utils::load_leaf_node] *) +Axiom betree_utils_load_leaf_node_fwd + : u64 -> state -> result (state * (Betree_list_t (u64 * u64))) +. + +(** [betree_main::betree_utils::store_leaf_node] *) +Axiom betree_utils_store_leaf_node_fwd + : u64 -> Betree_list_t (u64 * u64) -> state -> result (state * unit) +. + +(** [core::option::Option::{0}::unwrap] *) +Axiom core_option_option_unwrap_fwd : + forall(T : Type), option T -> state -> result (state * T) +. + +End BetreeMain_Opaque . diff --git a/tests/coq/betree/BetreeMain_Types.v b/tests/coq/betree/BetreeMain_Types.v new file mode 100644 index 00000000..672b2ebd --- /dev/null +++ b/tests/coq/betree/BetreeMain_Types.v @@ -0,0 +1,85 @@ +(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *) +(** [betree_main]: type definitions *) +Require Import Primitives. +Import Primitives. +Require Import Coq.ZArith.ZArith. +Local Open Scope Primitives_scope. +Module BetreeMain_Types. + +(** [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 +. + +Arguments BetreeListCons {T} _ _. +Arguments BetreeListNil {T}. + +(** [betree_main::betree::UpsertFunState] *) +Inductive Betree_upsert_fun_state_t := +| BetreeUpsertFunStateAdd : u64 -> Betree_upsert_fun_state_t +| BetreeUpsertFunStateSub : u64 -> Betree_upsert_fun_state_t +. + +(** [betree_main::betree::Message] *) +Inductive Betree_message_t := +| BetreeMessageInsert : u64 -> Betree_message_t +| BetreeMessageDelete : Betree_message_t +| BetreeMessageUpsert : Betree_upsert_fun_state_t -> Betree_message_t +. + +(** [betree_main::betree::Leaf] *) +Record Betree_leaf_t := +mkBetree_leaf_t { + Betree_leaf_id : u64; Betree_leaf_size : u64; +} +. + +(** [betree_main::betree::Node] *) +Inductive Betree_node_t := +| BetreeNodeInternal : Betree_internal_t -> Betree_node_t +| BetreeNodeLeaf : Betree_leaf_t -> Betree_node_t + +(** [betree_main::betree::Internal] *) +with Betree_internal_t := +| mkBetree_internal_t : + u64 -> + u64 -> + Betree_node_t -> + Betree_node_t -> + Betree_internal_t +. + +(** [betree_main::betree::Params] *) +Record Betree_params_t := +mkBetree_params_t { + Betree_params_min_flush_size : u64; Betree_params_split_size : u64; +} +. + +(** [betree_main::betree::NodeIdCounter] *) +Record Betree_node_id_counter_t := +mkBetree_node_id_counter_t { + Betree_node_id_counter_next_node_id : u64; +} +. + +(** [betree_main::betree::BeTree] *) +Record Betree_be_tree_t := +mkBetree_be_tree_t { + 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; +} +. + +(** [core::num::u64::{10}::MAX] *) +Definition core_num_u64_max_body : result u64 := + Return (18446744073709551615%u64) +. +Definition core_num_u64_max_c : u64 := core_num_u64_max_body%global. + +(** The state type used in the state-error monad *) +Axiom state : Type. + +End BetreeMain_Types . diff --git a/tests/coq/betree/BetreeMain__Funs.v b/tests/coq/betree/BetreeMain__Funs.v deleted file mode 100644 index 3ce86f6b..00000000 --- a/tests/coq/betree/BetreeMain__Funs.v +++ /dev/null @@ -1,1397 +0,0 @@ -(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *) -(** [betree_main]: function definitions *) -Require Import Primitives. -Import Primitives. -Require Import Coq.ZArith.ZArith. -Local Open Scope Primitives_scope. -Require Export BetreeMain__Types. -Import BetreeMain__Types. -Require Export BetreeMain__Opaque. -Import BetreeMain__Opaque. -Module BetreeMain__Funs. - -(** [betree_main::betree::load_internal_node] *) -Definition betree_load_internal_node_fwd - (id : u64) (st : state) : - result (state * (Betree_list_t (u64 * Betree_message_t))) - := - p <- betree_utils_load_internal_node_fwd id st; - let (st0, l) := p in - Return (st0, l) -. - -(** [betree_main::betree::store_internal_node] *) -Definition betree_store_internal_node_fwd - (id : u64) (content : Betree_list_t (u64 * Betree_message_t)) (st : state) : - result (state * unit) - := - p <- betree_utils_store_internal_node_fwd id content st; - let (st0, _) := p in - Return (st0, tt) -. - -(** [betree_main::betree::load_leaf_node] *) -Definition betree_load_leaf_node_fwd - (id : u64) (st : state) : result (state * (Betree_list_t (u64 * u64))) := - p <- betree_utils_load_leaf_node_fwd id st; - let (st0, l) := p in - Return (st0, l) -. - -(** [betree_main::betree::store_leaf_node] *) -Definition betree_store_leaf_node_fwd - (id : u64) (content : Betree_list_t (u64 * u64)) (st : state) : - result (state * unit) - := - p <- betree_utils_store_leaf_node_fwd id content st; - let (st0, _) := p in - Return (st0, tt) -. - -(** [betree_main::betree::fresh_node_id] *) -Definition betree_fresh_node_id_fwd (counter : u64) : result u64 := - i <- u64_add counter 1%u64; let _ := i in Return counter -. - -(** [betree_main::betree::fresh_node_id] *) -Definition betree_fresh_node_id_back (counter : u64) : result u64 := - counter0 <- u64_add counter 1%u64; Return counter0 -. - -(** [betree_main::betree::NodeIdCounter::{0}::new] *) -Definition betree_node_id_counter_new_fwd : result Betree_node_id_counter_t := - Return (mkBetree_node_id_counter_t (0%u64)) -. - -(** [betree_main::betree::NodeIdCounter::{0}::fresh_id] *) -Definition betree_node_id_counter_fresh_id_fwd - (self : Betree_node_id_counter_t) : result u64 := - match self with - | mkBetree_node_id_counter_t id => - i <- u64_add id 1%u64; let _ := i in Return id - end -. - -(** [betree_main::betree::NodeIdCounter::{0}::fresh_id] *) -Definition betree_node_id_counter_fresh_id_back - (self : Betree_node_id_counter_t) : result Betree_node_id_counter_t := - match self with - | mkBetree_node_id_counter_t id => - i <- u64_add id 1%u64; Return (mkBetree_node_id_counter_t i) - end -. - -(** [core::num::u64::{10}::MAX] *) -Definition core_num_u64_max_body : result u64 := - Return (18446744073709551615%u64) -. -Definition core_num_u64_max_c : u64 := core_num_u64_max_body%global. - -(** [betree_main::betree::upsert_update] *) -Definition betree_upsert_update_fwd - (prev : option u64) (st : Betree_upsert_fun_state_t) : result u64 := - match prev with - | None => - match st with - | BetreeUpsertFunStateAdd v => Return v - | BetreeUpsertFunStateSub i => Return (0%u64) - end - | Some prev0 => - match st with - | BetreeUpsertFunStateAdd v => - margin <- u64_sub core_num_u64_max_c prev0; - if margin s>= v - then (i <- u64_add prev0 v; Return i) - else Return core_num_u64_max_c - | BetreeUpsertFunStateSub v => - if prev0 s>= v then (i <- u64_sub prev0 v; Return i) else Return (0%u64) - end - end -. - -(** [betree_main::betree::List::{1}::len] *) -Fixpoint betree_list_len_fwd - (T : Type) (n : nat) (self : Betree_list_t T) : result u64 := - match n with - | O => Fail_ OutOfFuel - | S n0 => - match self with - | BetreeListCons t tl => - i <- betree_list_len_fwd T n0 tl; i0 <- u64_add 1%u64 i; Return i0 - | BetreeListNil => Return (0%u64) - end - end -. - -(** [betree_main::betree::List::{1}::split_at] *) -Fixpoint betree_list_split_at_fwd - (T : Type) (n : nat) (self : Betree_list_t T) (n0 : u64) : - result ((Betree_list_t T) * (Betree_list_t T)) - := - match n with - | O => Fail_ OutOfFuel - | S n1 => - if n0 s= 0%u64 - then Return (BetreeListNil, self) - else - match self with - | BetreeListCons hd tl => - i <- u64_sub n0 1%u64; - p <- betree_list_split_at_fwd T n1 tl i; - let (ls0, ls1) := p in - let l := ls0 in - Return (BetreeListCons hd l, ls1) - | BetreeListNil => Fail_ Failure - end - end -. - -(** [betree_main::betree::List::{1}::push_front] *) -Definition 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 BetreeListNil in - let l := tl in - Return (BetreeListCons x l) -. - -(** [betree_main::betree::List::{1}::pop_front] *) -Definition betree_list_pop_front_fwd - (T : Type) (self : Betree_list_t T) : result T := - let ls := mem_replace_fwd (Betree_list_t T) self BetreeListNil in - match ls with - | BetreeListCons x tl => Return x - | BetreeListNil => Fail_ Failure - end -. - -(** [betree_main::betree::List::{1}::pop_front] *) -Definition 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 BetreeListNil in - match ls with - | BetreeListCons x tl => Return tl - | BetreeListNil => Fail_ Failure - end -. - -(** [betree_main::betree::List::{1}::hd] *) -Definition betree_list_hd_fwd (T : Type) (self : Betree_list_t T) : result T := - match self with - | BetreeListCons hd l => Return hd - | BetreeListNil => Fail_ Failure - end -. - -(** [betree_main::betree::List::{2}::head_has_key] *) -Definition betree_list_head_has_key_fwd - (T : Type) (self : Betree_list_t (u64 * T)) (key : u64) : result bool := - match self with - | BetreeListCons hd l => let (i, _) := hd in Return (i s= key) - | BetreeListNil => Return false - end -. - -(** [betree_main::betree::List::{2}::partition_at_pivot] *) -Fixpoint betree_list_partition_at_pivot_fwd - (T : Type) (n : nat) (self : Betree_list_t (u64 * T)) (pivot : u64) : - result ((Betree_list_t (u64 * T)) * (Betree_list_t (u64 * T))) - := - match n with - | O => Fail_ OutOfFuel - | S n0 => - match self with - | BetreeListCons hd tl => - let (i, t) := hd in - if i s>= pivot - then Return (BetreeListNil, BetreeListCons (i, t) tl) - else ( - p <- betree_list_partition_at_pivot_fwd T n0 tl pivot; - let (ls0, ls1) := p in - let l := ls0 in - Return (BetreeListCons (i, t) l, ls1)) - | BetreeListNil => Return (BetreeListNil, BetreeListNil) - end - end -. - -(** [betree_main::betree::Leaf::{3}::split] *) -Definition betree_leaf_split_fwd - (n : nat) (self : Betree_leaf_t) (content : Betree_list_t (u64 * u64)) - (params : Betree_params_t) (node_id_cnt : Betree_node_id_counter_t) - (st : state) : - result (state * Betree_internal_t) - := - match n with - | O => Fail_ OutOfFuel - | S n0 => - match params with - | mkBetree_params_t i i0 => - p <- betree_list_split_at_fwd (u64 * u64) n0 content i0; - let (content0, content1) := p in - p0 <- betree_list_hd_fwd (u64 * u64) content1; - let (pivot, _) := p0 in - id0 <- betree_node_id_counter_fresh_id_fwd node_id_cnt; - node_id_cnt0 <- betree_node_id_counter_fresh_id_back node_id_cnt; - id1 <- betree_node_id_counter_fresh_id_fwd node_id_cnt0; - p1 <- betree_store_leaf_node_fwd id0 content0 st; - let (st0, _) := p1 in - p2 <- betree_store_leaf_node_fwd id1 content1 st0; - let (st1, _) := p2 in - match self with - | mkBetree_leaf_t i1 i2 => - let n1 := BetreeNodeLeaf (mkBetree_leaf_t id0 i0) in - let n2 := BetreeNodeLeaf (mkBetree_leaf_t id1 i0) in - Return (st1, mkBetree_internal_t i1 pivot n1 n2) - end - end - end -. - -(** [betree_main::betree::Leaf::{3}::split] *) -Definition betree_leaf_split_back - (n : nat) (self : Betree_leaf_t) (content : Betree_list_t (u64 * u64)) - (params : Betree_params_t) (node_id_cnt : Betree_node_id_counter_t) - (st : state) : - result Betree_node_id_counter_t - := - match n with - | O => Fail_ OutOfFuel - | S n0 => - match params with - | mkBetree_params_t i i0 => - p <- betree_list_split_at_fwd (u64 * u64) n0 content i0; - let (content0, content1) := p in - p0 <- betree_list_hd_fwd (u64 * u64) content1; - let _ := p0 in - id0 <- betree_node_id_counter_fresh_id_fwd node_id_cnt; - node_id_cnt0 <- betree_node_id_counter_fresh_id_back node_id_cnt; - id1 <- betree_node_id_counter_fresh_id_fwd node_id_cnt0; - p1 <- betree_store_leaf_node_fwd id0 content0 st; - let (st0, _) := p1 in - p2 <- betree_store_leaf_node_fwd id1 content1 st0; - let (_, _) := p2 in - match self with - | mkBetree_leaf_t i1 i2 => - node_id_cnt1 <- betree_node_id_counter_fresh_id_back node_id_cnt0; - Return node_id_cnt1 - end - end - end -. - -(** [betree_main::betree::Node::{5}::lookup_in_bindings] *) -Fixpoint betree_node_lookup_in_bindings_fwd - (n : nat) (key : u64) (bindings : Betree_list_t (u64 * u64)) : - result (option u64) - := - match n with - | O => Fail_ OutOfFuel - | S n0 => - match bindings with - | BetreeListCons hd tl => - let (i, i0) := hd in - if i s= key - then Return (Some i0) - else - if i s> key - then Return None - else (opt <- betree_node_lookup_in_bindings_fwd n0 key tl; Return opt) - | BetreeListNil => Return None - end - end -. - -(** [betree_main::betree::Node::{5}::lookup_first_message_for_key] *) -Fixpoint betree_node_lookup_first_message_for_key_fwd - (n : nat) (key : u64) (msgs : Betree_list_t (u64 * Betree_message_t)) : - result (Betree_list_t (u64 * Betree_message_t)) - := - match n with - | O => Fail_ OutOfFuel - | S n0 => - match msgs with - | BetreeListCons x next_msgs => - let (i, m) := x in - if i s>= key - then Return (BetreeListCons (i, m) next_msgs) - else ( - l <- betree_node_lookup_first_message_for_key_fwd n0 key next_msgs; - Return l) - | BetreeListNil => Return BetreeListNil - end - end -. - -(** [betree_main::betree::Node::{5}::lookup_first_message_for_key] *) -Fixpoint betree_node_lookup_first_message_for_key_back - (n : nat) (key : u64) (msgs : Betree_list_t (u64 * Betree_message_t)) - (ret : Betree_list_t (u64 * Betree_message_t)) : - result (Betree_list_t (u64 * Betree_message_t)) - := - match n with - | O => Fail_ OutOfFuel - | S n0 => - match msgs with - | BetreeListCons x next_msgs => - let (i, m) := x in - if i s>= key - then Return ret - else ( - next_msgs0 <- - betree_node_lookup_first_message_for_key_back n0 key next_msgs ret; - Return (BetreeListCons (i, m) next_msgs0)) - | BetreeListNil => Return ret - end - end -. - -(** [betree_main::betree::Node::{5}::apply_upserts] *) -Fixpoint betree_node_apply_upserts_fwd - (n : nat) (msgs : Betree_list_t (u64 * Betree_message_t)) (prev : option u64) - (key : u64) (st : state) : - result (state * u64) - := - match n with - | O => Fail_ OutOfFuel - | S n0 => - b <- betree_list_head_has_key_fwd Betree_message_t msgs key; - if b - then ( - msg <- betree_list_pop_front_fwd (u64 * Betree_message_t) msgs; - let (_, m) := msg in - match m with - | BetreeMessageInsert i => Fail_ Failure - | BetreeMessageDelete => Fail_ Failure - | BetreeMessageUpsert s => - v <- betree_upsert_update_fwd prev s; - msgs0 <- betree_list_pop_front_back (u64 * Betree_message_t) msgs; - p <- betree_node_apply_upserts_fwd n0 msgs0 (Some v) key st; - let (st0, i) := p in - Return (st0, i) - end) - else ( - p <- core_option_option_unwrap_fwd u64 prev st; - let (st0, v) := p in - l <- - betree_list_push_front_fwd_back (u64 * Betree_message_t) msgs (key, - BetreeMessageInsert v); - let _ := l in - Return (st0, v)) - end -. - -(** [betree_main::betree::Node::{5}::apply_upserts] *) -Fixpoint betree_node_apply_upserts_back - (n : nat) (msgs : Betree_list_t (u64 * Betree_message_t)) (prev : option u64) - (key : u64) (st : state) : - result (Betree_list_t (u64 * Betree_message_t)) - := - match n with - | O => Fail_ OutOfFuel - | S n0 => - b <- betree_list_head_has_key_fwd Betree_message_t msgs key; - if b - then ( - msg <- betree_list_pop_front_fwd (u64 * Betree_message_t) msgs; - let (_, m) := msg in - match m with - | BetreeMessageInsert i => Fail_ Failure - | BetreeMessageDelete => Fail_ Failure - | BetreeMessageUpsert s => - v <- betree_upsert_update_fwd prev s; - msgs0 <- betree_list_pop_front_back (u64 * Betree_message_t) msgs; - msgs1 <- betree_node_apply_upserts_back n0 msgs0 (Some v) key st; - Return msgs1 - end) - else ( - p <- core_option_option_unwrap_fwd u64 prev st; - let (_, v) := p in - msgs0 <- - betree_list_push_front_fwd_back (u64 * Betree_message_t) msgs (key, - BetreeMessageInsert v); - Return msgs0) - end -. - -(** [betree_main::betree::Node::{5}::lookup] *) -Fixpoint betree_node_lookup_fwd - (n : nat) (self : Betree_node_t) (key : u64) (st : state) : - result (state * (option u64)) - := - match n with - | O => Fail_ OutOfFuel - | S n0 => - match self with - | BetreeNodeInternal node => - match node with - | mkBetree_internal_t i i0 n1 n2 => - p <- betree_load_internal_node_fwd i st; - let (st0, msgs) := p in - pending <- betree_node_lookup_first_message_for_key_fwd n0 key msgs; - match pending with - | BetreeListCons p0 l => - let (k, msg) := p0 in - if k s<> key - then ( - p1 <- - betree_internal_lookup_in_children_fwd n0 (mkBetree_internal_t i - i0 n1 n2) key st0; - let (st1, opt) := p1 in - l0 <- - betree_node_lookup_first_message_for_key_back n0 key msgs - (BetreeListCons (k, msg) l); - let _ := l0 in - Return (st1, opt)) - else - match msg with - | BetreeMessageInsert v => - l0 <- - betree_node_lookup_first_message_for_key_back n0 key msgs - (BetreeListCons (k, BetreeMessageInsert v) l); - let _ := l0 in - Return (st0, Some v) - | BetreeMessageDelete => - l0 <- - betree_node_lookup_first_message_for_key_back n0 key msgs - (BetreeListCons (k, BetreeMessageDelete) l); - let _ := l0 in - Return (st0, None) - | BetreeMessageUpsert ufs => - p1 <- - betree_internal_lookup_in_children_fwd n0 (mkBetree_internal_t - i i0 n1 n2) key st0; - let (st1, v) := p1 in - p2 <- - betree_node_apply_upserts_fwd n0 (BetreeListCons (k, - BetreeMessageUpsert ufs) l) v key st1; - let (st2, v0) := p2 in - node0 <- - betree_internal_lookup_in_children_back n0 (mkBetree_internal_t - i i0 n1 n2) key st0; - match node0 with - | mkBetree_internal_t i1 i2 n3 n4 => - pending0 <- - betree_node_apply_upserts_back n0 (BetreeListCons (k, - BetreeMessageUpsert ufs) l) v key st1; - msgs0 <- - betree_node_lookup_first_message_for_key_back n0 key msgs - pending0; - p3 <- betree_store_internal_node_fwd i1 msgs0 st2; - let (st3, _) := p3 in - Return (st3, Some v0) - end - end - | BetreeListNil => - p0 <- - betree_internal_lookup_in_children_fwd n0 (mkBetree_internal_t i i0 - n1 n2) key st0; - let (st1, opt) := p0 in - l <- - betree_node_lookup_first_message_for_key_back n0 key msgs - BetreeListNil; - let _ := l in - Return (st1, opt) - end - end - | BetreeNodeLeaf node => - match node with - | mkBetree_leaf_t i i0 => - p <- betree_load_leaf_node_fwd i st; - let (st0, bindings) := p in - opt <- betree_node_lookup_in_bindings_fwd n0 key bindings; - Return (st0, opt) - end - end - end - -(** [betree_main::betree::Node::{5}::lookup] *) -with betree_node_lookup_back - (n : nat) (self : Betree_node_t) (key : u64) (st : state) : - result Betree_node_t - := - match n with - | O => Fail_ OutOfFuel - | S n0 => - match self with - | BetreeNodeInternal node => - match node with - | mkBetree_internal_t i i0 n1 n2 => - p <- betree_load_internal_node_fwd i st; - let (st0, msgs) := p in - pending <- betree_node_lookup_first_message_for_key_fwd n0 key msgs; - match pending with - | BetreeListCons p0 l => - let (k, msg) := p0 in - if k s<> key - then ( - l0 <- - betree_node_lookup_first_message_for_key_back n0 key msgs - (BetreeListCons (k, msg) l); - let _ := l0 in - node0 <- - betree_internal_lookup_in_children_back n0 (mkBetree_internal_t i - i0 n1 n2) key st0; - Return (BetreeNodeInternal node0)) - else - match msg with - | BetreeMessageInsert v => - l0 <- - betree_node_lookup_first_message_for_key_back n0 key msgs - (BetreeListCons (k, BetreeMessageInsert v) l); - let _ := l0 in - Return (BetreeNodeInternal (mkBetree_internal_t i i0 n1 n2)) - | BetreeMessageDelete => - l0 <- - betree_node_lookup_first_message_for_key_back n0 key msgs - (BetreeListCons (k, BetreeMessageDelete) l); - let _ := l0 in - Return (BetreeNodeInternal (mkBetree_internal_t i i0 n1 n2)) - | BetreeMessageUpsert ufs => - p1 <- - betree_internal_lookup_in_children_fwd n0 (mkBetree_internal_t - i i0 n1 n2) key st0; - let (st1, v) := p1 in - p2 <- - betree_node_apply_upserts_fwd n0 (BetreeListCons (k, - BetreeMessageUpsert ufs) l) v key st1; - let (st2, _) := p2 in - node0 <- - betree_internal_lookup_in_children_back n0 (mkBetree_internal_t - i i0 n1 n2) key st0; - match node0 with - | mkBetree_internal_t i1 i2 n3 n4 => - pending0 <- - betree_node_apply_upserts_back n0 (BetreeListCons (k, - BetreeMessageUpsert ufs) l) v key st1; - msgs0 <- - betree_node_lookup_first_message_for_key_back n0 key msgs - pending0; - p3 <- betree_store_internal_node_fwd i1 msgs0 st2; - let (_, _) := p3 in - Return (BetreeNodeInternal (mkBetree_internal_t i1 i2 n3 n4)) - end - end - | BetreeListNil => - l <- - betree_node_lookup_first_message_for_key_back n0 key msgs - BetreeListNil; - let _ := l in - node0 <- - betree_internal_lookup_in_children_back n0 (mkBetree_internal_t i - i0 n1 n2) key st0; - Return (BetreeNodeInternal node0) - end - end - | BetreeNodeLeaf node => - match node with - | mkBetree_leaf_t i i0 => - p <- betree_load_leaf_node_fwd i st; - let (_, bindings) := p in - opt <- betree_node_lookup_in_bindings_fwd n0 key bindings; - let _ := opt in - Return (BetreeNodeLeaf (mkBetree_leaf_t i i0)) - end - end - end - -(** [betree_main::betree::Internal::{4}::lookup_in_children] *) -with betree_internal_lookup_in_children_fwd - (n : nat) (self : Betree_internal_t) (key : u64) (st : state) : - result (state * (option u64)) - := - match n with - | O => Fail_ OutOfFuel - | S n0 => - match self with - | mkBetree_internal_t i i0 n1 n2 => - if key s< i0 - then ( - p <- betree_node_lookup_fwd n0 n1 key st; - let (st0, opt) := p in - Return (st0, opt)) - else ( - p <- betree_node_lookup_fwd n0 n2 key st; - let (st0, opt) := p in - Return (st0, opt)) - end - end - -(** [betree_main::betree::Internal::{4}::lookup_in_children] *) -with betree_internal_lookup_in_children_back - (n : nat) (self : Betree_internal_t) (key : u64) (st : state) : - result Betree_internal_t - := - match n with - | O => Fail_ OutOfFuel - | S n0 => - match self with - | mkBetree_internal_t i i0 n1 n2 => - if key s< i0 - then ( - n3 <- betree_node_lookup_back n0 n1 key st; - Return (mkBetree_internal_t i i0 n3 n2)) - else ( - n3 <- betree_node_lookup_back n0 n2 key st; - Return (mkBetree_internal_t i i0 n1 n3)) - end - end -. - -(** [betree_main::betree::Node::{5}::lookup_mut_in_bindings] *) -Fixpoint betree_node_lookup_mut_in_bindings_fwd - (n : nat) (key : u64) (bindings : Betree_list_t (u64 * u64)) : - result (Betree_list_t (u64 * u64)) - := - match n with - | O => Fail_ OutOfFuel - | S n0 => - match bindings with - | BetreeListCons hd tl => - let (i, i0) := hd in - if i s>= key - then Return (BetreeListCons (i, i0) tl) - else (l <- betree_node_lookup_mut_in_bindings_fwd n0 key tl; Return l) - | BetreeListNil => Return BetreeListNil - end - end -. - -(** [betree_main::betree::Node::{5}::lookup_mut_in_bindings] *) -Fixpoint betree_node_lookup_mut_in_bindings_back - (n : nat) (key : u64) (bindings : Betree_list_t (u64 * u64)) - (ret : Betree_list_t (u64 * u64)) : - result (Betree_list_t (u64 * u64)) - := - match n with - | O => Fail_ OutOfFuel - | S n0 => - match bindings with - | BetreeListCons hd tl => - let (i, i0) := hd in - if i s>= key - then Return ret - else ( - tl0 <- betree_node_lookup_mut_in_bindings_back n0 key tl ret; - Return (BetreeListCons (i, i0) tl0)) - | BetreeListNil => Return ret - end - end -. - -(** [betree_main::betree::Node::{5}::apply_to_leaf] *) -Definition betree_node_apply_to_leaf_fwd_back - (n : nat) (bindings : Betree_list_t (u64 * u64)) (key : u64) - (new_msg : Betree_message_t) : - result (Betree_list_t (u64 * u64)) - := - match n with - | O => Fail_ OutOfFuel - | S n0 => - bindings0 <- betree_node_lookup_mut_in_bindings_fwd n0 key bindings; - b <- betree_list_head_has_key_fwd u64 bindings0 key; - if b - then ( - hd <- betree_list_pop_front_fwd (u64 * u64) bindings0; - match new_msg with - | BetreeMessageInsert v => - bindings1 <- betree_list_pop_front_back (u64 * u64) bindings0; - bindings2 <- - betree_list_push_front_fwd_back (u64 * u64) bindings1 (key, v); - bindings3 <- - betree_node_lookup_mut_in_bindings_back n0 key bindings bindings2; - Return bindings3 - | BetreeMessageDelete => - bindings1 <- betree_list_pop_front_back (u64 * u64) bindings0; - bindings2 <- - betree_node_lookup_mut_in_bindings_back n0 key bindings bindings1; - Return bindings2 - | BetreeMessageUpsert s => - let (_, i) := hd in - v <- betree_upsert_update_fwd (Some i) s; - bindings1 <- betree_list_pop_front_back (u64 * u64) bindings0; - bindings2 <- - betree_list_push_front_fwd_back (u64 * u64) bindings1 (key, v); - bindings3 <- - betree_node_lookup_mut_in_bindings_back n0 key bindings bindings2; - Return bindings3 - end) - else - match new_msg with - | BetreeMessageInsert v => - bindings1 <- - betree_list_push_front_fwd_back (u64 * u64) bindings0 (key, v); - bindings2 <- - betree_node_lookup_mut_in_bindings_back n0 key bindings bindings1; - Return bindings2 - | BetreeMessageDelete => - bindings1 <- - betree_node_lookup_mut_in_bindings_back n0 key bindings bindings0; - Return bindings1 - | BetreeMessageUpsert s => - v <- betree_upsert_update_fwd None s; - bindings1 <- - betree_list_push_front_fwd_back (u64 * u64) bindings0 (key, v); - bindings2 <- - betree_node_lookup_mut_in_bindings_back n0 key bindings bindings1; - Return bindings2 - end - end -. - -(** [betree_main::betree::Node::{5}::apply_messages_to_leaf] *) -Fixpoint betree_node_apply_messages_to_leaf_fwd_back - (n : nat) (bindings : Betree_list_t (u64 * u64)) - (new_msgs : Betree_list_t (u64 * Betree_message_t)) : - result (Betree_list_t (u64 * u64)) - := - match n with - | O => Fail_ OutOfFuel - | S n0 => - match new_msgs with - | BetreeListCons new_msg new_msgs_tl => - let (i, m) := new_msg in - bindings0 <- betree_node_apply_to_leaf_fwd_back n0 bindings i m; - bindings1 <- - betree_node_apply_messages_to_leaf_fwd_back n0 bindings0 new_msgs_tl; - Return bindings1 - | BetreeListNil => Return bindings - end - end -. - -(** [betree_main::betree::Node::{5}::filter_messages_for_key] *) -Fixpoint betree_node_filter_messages_for_key_fwd_back - (n : nat) (key : u64) (msgs : Betree_list_t (u64 * Betree_message_t)) : - result (Betree_list_t (u64 * Betree_message_t)) - := - match n with - | O => Fail_ OutOfFuel - | S n0 => - match msgs with - | BetreeListCons p l => - let (k, m) := p in - if k s= key - then ( - msgs0 <- - betree_list_pop_front_back (u64 * Betree_message_t) (BetreeListCons - (k, m) l); - msgs1 <- betree_node_filter_messages_for_key_fwd_back n0 key msgs0; - Return msgs1) - else Return (BetreeListCons (k, m) l) - | BetreeListNil => Return BetreeListNil - end - end -. - -(** [betree_main::betree::Node::{5}::lookup_first_message_after_key] *) -Fixpoint betree_node_lookup_first_message_after_key_fwd - (n : nat) (key : u64) (msgs : Betree_list_t (u64 * Betree_message_t)) : - result (Betree_list_t (u64 * Betree_message_t)) - := - match n with - | O => Fail_ OutOfFuel - | S n0 => - match msgs with - | BetreeListCons p next_msgs => - let (k, m) := p in - if k s= key - then ( - l <- betree_node_lookup_first_message_after_key_fwd n0 key next_msgs; - Return l) - else Return (BetreeListCons (k, m) next_msgs) - | BetreeListNil => Return BetreeListNil - end - end -. - -(** [betree_main::betree::Node::{5}::lookup_first_message_after_key] *) -Fixpoint betree_node_lookup_first_message_after_key_back - (n : nat) (key : u64) (msgs : Betree_list_t (u64 * Betree_message_t)) - (ret : Betree_list_t (u64 * Betree_message_t)) : - result (Betree_list_t (u64 * Betree_message_t)) - := - match n with - | O => Fail_ OutOfFuel - | S n0 => - match msgs with - | BetreeListCons p next_msgs => - let (k, m) := p in - if k s= key - then ( - next_msgs0 <- - betree_node_lookup_first_message_after_key_back n0 key next_msgs ret; - Return (BetreeListCons (k, m) next_msgs0)) - else Return ret - | BetreeListNil => Return ret - end - end -. - -(** [betree_main::betree::Node::{5}::apply_to_internal] *) -Definition betree_node_apply_to_internal_fwd_back - (n : nat) (msgs : Betree_list_t (u64 * Betree_message_t)) (key : u64) - (new_msg : Betree_message_t) : - result (Betree_list_t (u64 * Betree_message_t)) - := - match n with - | O => Fail_ OutOfFuel - | S n0 => - msgs0 <- betree_node_lookup_first_message_for_key_fwd n0 key msgs; - b <- betree_list_head_has_key_fwd Betree_message_t msgs0 key; - if b - then - match new_msg with - | BetreeMessageInsert i => - msgs1 <- betree_node_filter_messages_for_key_fwd_back n0 key msgs0; - msgs2 <- - betree_list_push_front_fwd_back (u64 * Betree_message_t) msgs1 (key, - BetreeMessageInsert i); - msgs3 <- - betree_node_lookup_first_message_for_key_back n0 key msgs msgs2; - Return msgs3 - | BetreeMessageDelete => - msgs1 <- betree_node_filter_messages_for_key_fwd_back n0 key msgs0; - msgs2 <- - betree_list_push_front_fwd_back (u64 * Betree_message_t) msgs1 (key, - BetreeMessageDelete); - msgs3 <- - betree_node_lookup_first_message_for_key_back n0 key msgs msgs2; - Return msgs3 - | BetreeMessageUpsert s => - p <- betree_list_hd_fwd (u64 * Betree_message_t) msgs0; - let (_, m) := p in - match m with - | BetreeMessageInsert prev => - v <- betree_upsert_update_fwd (Some prev) s; - msgs1 <- betree_list_pop_front_back (u64 * Betree_message_t) msgs0; - msgs2 <- - betree_list_push_front_fwd_back (u64 * Betree_message_t) msgs1 - (key, BetreeMessageInsert v); - msgs3 <- - betree_node_lookup_first_message_for_key_back n0 key msgs msgs2; - Return msgs3 - | BetreeMessageDelete => - v <- betree_upsert_update_fwd None s; - msgs1 <- betree_list_pop_front_back (u64 * Betree_message_t) msgs0; - msgs2 <- - betree_list_push_front_fwd_back (u64 * Betree_message_t) msgs1 - (key, BetreeMessageInsert v); - msgs3 <- - betree_node_lookup_first_message_for_key_back n0 key msgs msgs2; - Return msgs3 - | BetreeMessageUpsert ufs => - msgs1 <- betree_node_lookup_first_message_after_key_fwd n0 key msgs0; - msgs2 <- - betree_list_push_front_fwd_back (u64 * Betree_message_t) msgs1 - (key, BetreeMessageUpsert s); - msgs3 <- - betree_node_lookup_first_message_after_key_back n0 key msgs0 msgs2; - msgs4 <- - betree_node_lookup_first_message_for_key_back n0 key msgs msgs3; - Return msgs4 - end - end - else ( - msgs1 <- - betree_list_push_front_fwd_back (u64 * Betree_message_t) msgs0 (key, - new_msg); - msgs2 <- betree_node_lookup_first_message_for_key_back n0 key msgs msgs1; - Return msgs2) - end -. - -(** [betree_main::betree::Node::{5}::apply_messages_to_internal] *) -Fixpoint betree_node_apply_messages_to_internal_fwd_back - (n : nat) (msgs : Betree_list_t (u64 * Betree_message_t)) - (new_msgs : Betree_list_t (u64 * Betree_message_t)) : - result (Betree_list_t (u64 * Betree_message_t)) - := - match n with - | O => Fail_ OutOfFuel - | S n0 => - match new_msgs with - | BetreeListCons new_msg new_msgs_tl => - let (i, m) := new_msg in - msgs0 <- betree_node_apply_to_internal_fwd_back n0 msgs i m; - msgs1 <- - betree_node_apply_messages_to_internal_fwd_back n0 msgs0 new_msgs_tl; - Return msgs1 - | BetreeListNil => Return msgs - end - end -. - -(** [betree_main::betree::Node::{5}::apply_messages] *) -Fixpoint betree_node_apply_messages_fwd - (n : nat) (self : Betree_node_t) (params : Betree_params_t) - (node_id_cnt : Betree_node_id_counter_t) - (msgs : Betree_list_t (u64 * Betree_message_t)) (st : state) : - result (state * unit) - := - match n with - | O => Fail_ OutOfFuel - | S n0 => - match self with - | BetreeNodeInternal node => - match node with - | mkBetree_internal_t i i0 n1 n2 => - p <- betree_load_internal_node_fwd i st; - let (st0, content) := p in - content0 <- - betree_node_apply_messages_to_internal_fwd_back n0 content msgs; - num_msgs <- betree_list_len_fwd (u64 * Betree_message_t) n0 content0; - match params with - | mkBetree_params_t i1 i2 => - if num_msgs s>= i1 - then ( - p0 <- - betree_internal_flush_fwd n0 (mkBetree_internal_t i i0 n1 n2) - (mkBetree_params_t i1 i2) node_id_cnt content0 st0; - let (st1, content1) := p0 in - p1 <- - betree_internal_flush_back n0 (mkBetree_internal_t i i0 n1 n2) - (mkBetree_params_t i1 i2) node_id_cnt content0 st0; - let (node0, _) := p1 in - match node0 with - | mkBetree_internal_t i3 i4 n3 n4 => - p2 <- betree_store_internal_node_fwd i3 content1 st1; - let (st2, _) := p2 in - Return (st2, tt) - end) - else ( - p0 <- betree_store_internal_node_fwd i content0 st0; - let (st1, _) := p0 in - Return (st1, tt)) - end - end - | BetreeNodeLeaf node => - match node with - | mkBetree_leaf_t i i0 => - p <- betree_load_leaf_node_fwd i st; - let (st0, content) := p in - content0 <- - betree_node_apply_messages_to_leaf_fwd_back n0 content msgs; - len <- betree_list_len_fwd (u64 * u64) n0 content0; - match params with - | mkBetree_params_t i1 i2 => - i3 <- u64_mul 2%u64 i2; - if len s>= i3 - then ( - p0 <- - betree_leaf_split_fwd n0 (mkBetree_leaf_t i i0) content0 - (mkBetree_params_t i1 i2) node_id_cnt st0; - let (st1, _) := p0 in - p1 <- betree_store_leaf_node_fwd i BetreeListNil st1; - let (st2, _) := p1 in - Return (st2, tt)) - else ( - p0 <- betree_store_leaf_node_fwd i content0 st0; - let (st1, _) := p0 in - Return (st1, tt)) - end - end - end - end - -(** [betree_main::betree::Node::{5}::apply_messages] *) -with betree_node_apply_messages_back - (n : nat) (self : Betree_node_t) (params : Betree_params_t) - (node_id_cnt : Betree_node_id_counter_t) - (msgs : Betree_list_t (u64 * Betree_message_t)) (st : state) : - result (Betree_node_t * Betree_node_id_counter_t) - := - match n with - | O => Fail_ OutOfFuel - | S n0 => - match self with - | BetreeNodeInternal node => - match node with - | mkBetree_internal_t i i0 n1 n2 => - p <- betree_load_internal_node_fwd i st; - let (st0, content) := p in - content0 <- - betree_node_apply_messages_to_internal_fwd_back n0 content msgs; - num_msgs <- betree_list_len_fwd (u64 * Betree_message_t) n0 content0; - match params with - | mkBetree_params_t i1 i2 => - if num_msgs s>= i1 - then ( - p0 <- - betree_internal_flush_fwd n0 (mkBetree_internal_t i i0 n1 n2) - (mkBetree_params_t i1 i2) node_id_cnt content0 st0; - let (st1, content1) := p0 in - p1 <- - betree_internal_flush_back n0 (mkBetree_internal_t i i0 n1 n2) - (mkBetree_params_t i1 i2) node_id_cnt content0 st0; - let (node0, node_id_cnt0) := p1 in - match node0 with - | mkBetree_internal_t i3 i4 n3 n4 => - p2 <- betree_store_internal_node_fwd i3 content1 st1; - let (_, _) := p2 in - Return (BetreeNodeInternal (mkBetree_internal_t i3 i4 n3 n4), - node_id_cnt0) - end) - else ( - p0 <- betree_store_internal_node_fwd i content0 st0; - let (_, _) := p0 in - Return (BetreeNodeInternal (mkBetree_internal_t i i0 n1 n2), - node_id_cnt)) - end - end - | BetreeNodeLeaf node => - match node with - | mkBetree_leaf_t i i0 => - p <- betree_load_leaf_node_fwd i st; - let (st0, content) := p in - content0 <- - betree_node_apply_messages_to_leaf_fwd_back n0 content msgs; - len <- betree_list_len_fwd (u64 * u64) n0 content0; - match params with - | mkBetree_params_t i1 i2 => - i3 <- u64_mul 2%u64 i2; - if len s>= i3 - then ( - p0 <- - betree_leaf_split_fwd n0 (mkBetree_leaf_t i i0) content0 - (mkBetree_params_t i1 i2) node_id_cnt st0; - let (st1, new_node) := p0 in - p1 <- betree_store_leaf_node_fwd i BetreeListNil st1; - let (_, _) := p1 in - node_id_cnt0 <- - betree_leaf_split_back n0 (mkBetree_leaf_t i i0) content0 - (mkBetree_params_t i1 i2) node_id_cnt st0; - Return (BetreeNodeInternal new_node, node_id_cnt0)) - else ( - p0 <- betree_store_leaf_node_fwd i content0 st0; - let (_, _) := p0 in - Return (BetreeNodeLeaf (mkBetree_leaf_t i len), node_id_cnt)) - end - end - end - end - -(** [betree_main::betree::Internal::{4}::flush] *) -with betree_internal_flush_fwd - (n : nat) (self : Betree_internal_t) (params : Betree_params_t) - (node_id_cnt : Betree_node_id_counter_t) - (content : Betree_list_t (u64 * Betree_message_t)) (st : state) : - result (state * (Betree_list_t (u64 * Betree_message_t))) - := - match n with - | O => Fail_ OutOfFuel - | S n0 => - match self with - | mkBetree_internal_t i i0 n1 n2 => - p <- betree_list_partition_at_pivot_fwd Betree_message_t n0 content i0; - let (msgs_left, msgs_right) := p in - len_left <- betree_list_len_fwd (u64 * Betree_message_t) n0 msgs_left; - match params with - | mkBetree_params_t i1 i2 => - if len_left s>= i1 - then ( - p0 <- - betree_node_apply_messages_fwd n0 n1 (mkBetree_params_t i1 i2) - node_id_cnt msgs_left st; - let (st0, _) := p0 in - p1 <- - betree_node_apply_messages_back n0 n1 (mkBetree_params_t i1 i2) - node_id_cnt msgs_left st; - let (_, node_id_cnt0) := p1 in - len_right <- - betree_list_len_fwd (u64 * Betree_message_t) n0 msgs_right; - if len_right s>= i1 - then ( - p2 <- - betree_node_apply_messages_fwd n0 n2 (mkBetree_params_t i1 i2) - node_id_cnt0 msgs_right st0; - let (st1, _) := p2 in - p3 <- - betree_node_apply_messages_back n0 n2 (mkBetree_params_t i1 i2) - node_id_cnt0 msgs_right st0; - let (_, _) := p3 in - Return (st1, BetreeListNil)) - else Return (st0, msgs_right)) - else ( - p0 <- - betree_node_apply_messages_fwd n0 n2 (mkBetree_params_t i1 i2) - node_id_cnt msgs_right st; - let (st0, _) := p0 in - p1 <- - betree_node_apply_messages_back n0 n2 (mkBetree_params_t i1 i2) - node_id_cnt msgs_right st; - let (_, _) := p1 in - Return (st0, msgs_left)) - end - end - end - -(** [betree_main::betree::Internal::{4}::flush] *) -with betree_internal_flush_back - (n : nat) (self : Betree_internal_t) (params : Betree_params_t) - (node_id_cnt : Betree_node_id_counter_t) - (content : Betree_list_t (u64 * Betree_message_t)) (st : state) : - result (Betree_internal_t * Betree_node_id_counter_t) - := - match n with - | O => Fail_ OutOfFuel - | S n0 => - match self with - | mkBetree_internal_t i i0 n1 n2 => - p <- betree_list_partition_at_pivot_fwd Betree_message_t n0 content i0; - let (msgs_left, msgs_right) := p in - len_left <- betree_list_len_fwd (u64 * Betree_message_t) n0 msgs_left; - match params with - | mkBetree_params_t i1 i2 => - if len_left s>= i1 - then ( - p0 <- - betree_node_apply_messages_fwd n0 n1 (mkBetree_params_t i1 i2) - node_id_cnt msgs_left st; - let (st0, _) := p0 in - p1 <- - betree_node_apply_messages_back n0 n1 (mkBetree_params_t i1 i2) - node_id_cnt msgs_left st; - let (n3, node_id_cnt0) := p1 in - len_right <- - betree_list_len_fwd (u64 * Betree_message_t) n0 msgs_right; - if len_right s>= i1 - then ( - p2 <- - betree_node_apply_messages_back n0 n2 (mkBetree_params_t i1 i2) - node_id_cnt0 msgs_right st0; - let (n4, node_id_cnt1) := p2 in - Return (mkBetree_internal_t i i0 n3 n4, node_id_cnt1)) - else Return (mkBetree_internal_t i i0 n3 n2, node_id_cnt0)) - else ( - p0 <- - betree_node_apply_messages_back n0 n2 (mkBetree_params_t i1 i2) - node_id_cnt msgs_right st; - let (n3, node_id_cnt0) := p0 in - Return (mkBetree_internal_t i i0 n1 n3, node_id_cnt0)) - end - end - end -. - -(** [betree_main::betree::Node::{5}::apply] *) -Definition betree_node_apply_fwd - (n : nat) (self : Betree_node_t) (params : Betree_params_t) - (node_id_cnt : Betree_node_id_counter_t) (key : u64) - (new_msg : Betree_message_t) (st : state) : - result (state * unit) - := - match n with - | O => Fail_ OutOfFuel - | S n0 => - let l := BetreeListNil in - p <- - betree_node_apply_messages_fwd n0 self params node_id_cnt (BetreeListCons - (key, new_msg) l) st; - let (st0, _) := p in - p0 <- - betree_node_apply_messages_back n0 self params node_id_cnt - (BetreeListCons (key, new_msg) l) st; - let (_, _) := p0 in - Return (st0, tt) - end -. - -(** [betree_main::betree::Node::{5}::apply] *) -Definition betree_node_apply_back - (n : nat) (self : Betree_node_t) (params : Betree_params_t) - (node_id_cnt : Betree_node_id_counter_t) (key : u64) - (new_msg : Betree_message_t) (st : state) : - result (Betree_node_t * Betree_node_id_counter_t) - := - match n with - | O => Fail_ OutOfFuel - | S n0 => - let l := BetreeListNil in - p <- - betree_node_apply_messages_back n0 self params node_id_cnt - (BetreeListCons (key, new_msg) l) st; - let (self0, node_id_cnt0) := p in - Return (self0, node_id_cnt0) - end -. - -(** [betree_main::betree::BeTree::{6}::new] *) -Definition betree_be_tree_new_fwd - (min_flush_size : u64) (split_size : u64) (st : state) : - result (state * Betree_be_tree_t) - := - node_id_cnt <- betree_node_id_counter_new_fwd; - id <- betree_node_id_counter_fresh_id_fwd node_id_cnt; - p <- betree_store_leaf_node_fwd id BetreeListNil st; - let (st0, _) := p in - node_id_cnt0 <- betree_node_id_counter_fresh_id_back node_id_cnt; - Return (st0, mkBetree_be_tree_t (mkBetree_params_t min_flush_size split_size) - node_id_cnt0 (BetreeNodeLeaf (mkBetree_leaf_t id (0%u64)))) -. - -(** [betree_main::betree::BeTree::{6}::apply] *) -Definition betree_be_tree_apply_fwd - (n : nat) (self : Betree_be_tree_t) (key : u64) (msg : Betree_message_t) - (st : state) : - result (state * unit) - := - match n with - | O => Fail_ OutOfFuel - | S n0 => - match self with - | mkBetree_be_tree_t p nic n1 => - p0 <- betree_node_apply_fwd n0 n1 p nic key msg st; - let (st0, _) := p0 in - p1 <- betree_node_apply_back n0 n1 p nic key msg st; - let (_, _) := p1 in - Return (st0, tt) - end - end -. - -(** [betree_main::betree::BeTree::{6}::apply] *) -Definition betree_be_tree_apply_back - (n : nat) (self : Betree_be_tree_t) (key : u64) (msg : Betree_message_t) - (st : state) : - result Betree_be_tree_t - := - match n with - | O => Fail_ OutOfFuel - | S n0 => - match self with - | mkBetree_be_tree_t p nic n1 => - p0 <- betree_node_apply_back n0 n1 p nic key msg st; - let (n2, nic0) := p0 in - Return (mkBetree_be_tree_t p nic0 n2) - end - end -. - -(** [betree_main::betree::BeTree::{6}::insert] *) -Definition betree_be_tree_insert_fwd - (n : nat) (self : Betree_be_tree_t) (key : u64) (value : u64) (st : state) : - result (state * unit) - := - match n with - | O => Fail_ OutOfFuel - | S n0 => - p <- betree_be_tree_apply_fwd n0 self key (BetreeMessageInsert value) st; - let (st0, _) := p in - bt <- betree_be_tree_apply_back n0 self key (BetreeMessageInsert value) st; - let _ := bt in - Return (st0, tt) - end -. - -(** [betree_main::betree::BeTree::{6}::insert] *) -Definition betree_be_tree_insert_back - (n : nat) (self : Betree_be_tree_t) (key : u64) (value : u64) (st : state) : - result Betree_be_tree_t - := - match n with - | O => Fail_ OutOfFuel - | S n0 => - self0 <- - betree_be_tree_apply_back n0 self key (BetreeMessageInsert value) st; - Return self0 - end -. - -(** [betree_main::betree::BeTree::{6}::delete] *) -Definition betree_be_tree_delete_fwd - (n : nat) (self : Betree_be_tree_t) (key : u64) (st : state) : - result (state * unit) - := - match n with - | O => Fail_ OutOfFuel - | S n0 => - p <- betree_be_tree_apply_fwd n0 self key BetreeMessageDelete st; - let (st0, _) := p in - bt <- betree_be_tree_apply_back n0 self key BetreeMessageDelete st; - let _ := bt in - Return (st0, tt) - end -. - -(** [betree_main::betree::BeTree::{6}::delete] *) -Definition betree_be_tree_delete_back - (n : nat) (self : Betree_be_tree_t) (key : u64) (st : state) : - result Betree_be_tree_t - := - match n with - | O => Fail_ OutOfFuel - | S n0 => - self0 <- betree_be_tree_apply_back n0 self key BetreeMessageDelete st; - Return self0 - end -. - -(** [betree_main::betree::BeTree::{6}::upsert] *) -Definition betree_be_tree_upsert_fwd - (n : nat) (self : Betree_be_tree_t) (key : u64) - (upd : Betree_upsert_fun_state_t) (st : state) : - result (state * unit) - := - match n with - | O => Fail_ OutOfFuel - | S n0 => - p <- betree_be_tree_apply_fwd n0 self key (BetreeMessageUpsert upd) st; - let (st0, _) := p in - bt <- betree_be_tree_apply_back n0 self key (BetreeMessageUpsert upd) st; - let _ := bt in - Return (st0, tt) - end -. - -(** [betree_main::betree::BeTree::{6}::upsert] *) -Definition betree_be_tree_upsert_back - (n : nat) (self : Betree_be_tree_t) (key : u64) - (upd : Betree_upsert_fun_state_t) (st : state) : - result Betree_be_tree_t - := - match n with - | O => Fail_ OutOfFuel - | S n0 => - self0 <- - betree_be_tree_apply_back n0 self key (BetreeMessageUpsert upd) st; - Return self0 - end -. - -(** [betree_main::betree::BeTree::{6}::lookup] *) -Definition betree_be_tree_lookup_fwd - (n : nat) (self : Betree_be_tree_t) (key : u64) (st : state) : - result (state * (option u64)) - := - match n with - | O => Fail_ OutOfFuel - | S n0 => - match self with - | mkBetree_be_tree_t p nic n1 => - p0 <- betree_node_lookup_fwd n0 n1 key st; - let (st0, opt) := p0 in - Return (st0, opt) - end - end -. - -(** [betree_main::betree::BeTree::{6}::lookup] *) -Definition betree_be_tree_lookup_back - (n : nat) (self : Betree_be_tree_t) (key : u64) (st : state) : - result Betree_be_tree_t - := - match n with - | O => Fail_ OutOfFuel - | S n0 => - match self with - | mkBetree_be_tree_t p nic n1 => - n2 <- betree_node_lookup_back n0 n1 key st; - Return (mkBetree_be_tree_t p nic n2) - end - end -. - -(** [betree_main::main] *) -Definition main_fwd : result unit := Return tt. - -End BetreeMain__Funs . diff --git a/tests/coq/betree/BetreeMain__Opaque.v b/tests/coq/betree/BetreeMain__Opaque.v deleted file mode 100644 index cbd8cfb3..00000000 --- a/tests/coq/betree/BetreeMain__Opaque.v +++ /dev/null @@ -1,38 +0,0 @@ -(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *) -(** [betree_main]: opaque function definitions *) -Require Import Primitives. -Import Primitives. -Require Import Coq.ZArith.ZArith. -Local Open Scope Primitives_scope. -Require Export BetreeMain__Types. -Import BetreeMain__Types. -Module BetreeMain__Opaque. - -(** [betree_main::betree_utils::load_internal_node] *) -Axiom betree_utils_load_internal_node_fwd - : u64 -> state -> result (state * (Betree_list_t (u64 * Betree_message_t))) -. - -(** [betree_main::betree_utils::store_internal_node] *) -Axiom betree_utils_store_internal_node_fwd - : - u64 -> Betree_list_t (u64 * Betree_message_t) -> state -> result (state * - unit) -. - -(** [betree_main::betree_utils::load_leaf_node] *) -Axiom betree_utils_load_leaf_node_fwd - : u64 -> state -> result (state * (Betree_list_t (u64 * u64))) -. - -(** [betree_main::betree_utils::store_leaf_node] *) -Axiom betree_utils_store_leaf_node_fwd - : u64 -> Betree_list_t (u64 * u64) -> state -> result (state * unit) -. - -(** [core::option::Option::{0}::unwrap] *) -Axiom core_option_option_unwrap_fwd : - forall(T : Type), option T -> state -> result (state * T) -. - -End BetreeMain__Opaque . diff --git a/tests/coq/betree/BetreeMain__Types.v b/tests/coq/betree/BetreeMain__Types.v deleted file mode 100644 index 2ed0d324..00000000 --- a/tests/coq/betree/BetreeMain__Types.v +++ /dev/null @@ -1,85 +0,0 @@ -(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *) -(** [betree_main]: type definitions *) -Require Import Primitives. -Import Primitives. -Require Import Coq.ZArith.ZArith. -Local Open Scope Primitives_scope. -Module BetreeMain__Types. - -(** [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 -. - -Arguments BetreeListCons {T} _ _. -Arguments BetreeListNil {T}. - -(** [betree_main::betree::UpsertFunState] *) -Inductive Betree_upsert_fun_state_t := -| BetreeUpsertFunStateAdd : u64 -> Betree_upsert_fun_state_t -| BetreeUpsertFunStateSub : u64 -> Betree_upsert_fun_state_t -. - -(** [betree_main::betree::Message] *) -Inductive Betree_message_t := -| BetreeMessageInsert : u64 -> Betree_message_t -| BetreeMessageDelete : Betree_message_t -| BetreeMessageUpsert : Betree_upsert_fun_state_t -> Betree_message_t -. - -(** [betree_main::betree::Leaf] *) -Record Betree_leaf_t := -mkBetree_leaf_t { - Betree_leaf_id : u64; Betree_leaf_size : u64; -} -. - -(** [betree_main::betree::Node] *) -Inductive Betree_node_t := -| BetreeNodeInternal : Betree_internal_t -> Betree_node_t -| BetreeNodeLeaf : Betree_leaf_t -> Betree_node_t - -(** [betree_main::betree::Internal] *) -with Betree_internal_t := -| mkBetree_internal_t : - u64 -> - u64 -> - Betree_node_t -> - Betree_node_t -> - Betree_internal_t -. - -(** [betree_main::betree::Params] *) -Record Betree_params_t := -mkBetree_params_t { - Betree_params_min_flush_size : u64; Betree_params_split_size : u64; -} -. - -(** [betree_main::betree::NodeIdCounter] *) -Record Betree_node_id_counter_t := -mkBetree_node_id_counter_t { - Betree_node_id_counter_next_node_id : u64; -} -. - -(** [betree_main::betree::BeTree] *) -Record Betree_be_tree_t := -mkBetree_be_tree_t { - 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; -} -. - -(** [core::num::u64::{10}::MAX] *) -Definition core_num_u64_max_body : result u64 := - Return (18446744073709551615%u64) -. -Definition core_num_u64_max_c : u64 := core_num_u64_max_body%global. - -(** The state type used in the state-error monad *) -Axiom state : Type. - -End BetreeMain__Types . -- cgit v1.2.3