diff options
Diffstat (limited to 'tests')
| -rw-r--r-- | tests/coq/betree/BetreeMain_Funs.v | 785 | ||||
| -rw-r--r-- | tests/coq/betree/BetreeMain_Types.v | 29 | ||||
| -rw-r--r-- | tests/coq/betree/_CoqProject | 6 | ||||
| -rw-r--r-- | tests/coq/hashmap/Hashmap_Funs.v | 196 | ||||
| -rw-r--r-- | tests/coq/hashmap/_CoqProject | 4 | ||||
| -rw-r--r-- | tests/coq/hashmap_on_disk/HashmapMain_Funs.v | 228 | ||||
| -rw-r--r-- | tests/coq/hashmap_on_disk/_CoqProject | 6 | ||||
| -rw-r--r-- | tests/coq/misc/Constants.v | 4 | ||||
| -rw-r--r-- | tests/coq/misc/NoNestedBorrows.v | 43 | ||||
| -rw-r--r-- | tests/coq/misc/_CoqProject | 6 |
10 files changed, 612 insertions, 695 deletions
diff --git a/tests/coq/betree/BetreeMain_Funs.v b/tests/coq/betree/BetreeMain_Funs.v index 3129614c..d60ef718 100644 --- a/tests/coq/betree/BetreeMain_Funs.v +++ b/tests/coq/betree/BetreeMain_Funs.v @@ -66,19 +66,16 @@ Definition betree_node_id_counter_new_fwd : result Betree_node_id_counter_t := (** [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 + i <- u64_add self.(Betree_node_id_counter_next_node_id) 1%u64; + let _ := i in + Return self.(Betree_node_id_counter_next_node_id) . (** [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 + i <- u64_add self.(Betree_node_id_counter_next_node_id) 1%u64; + Return (mkBetree_node_id_counter_t i) . (** [core::num::u64::{10}::MAX] *) @@ -224,26 +221,24 @@ Definition betree_leaf_split_fwd 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 + p <- + betree_list_split_at_fwd (u64 * u64) n0 content + params.(Betree_params_split_size); + 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 + let n1 := BetreeNodeLeaf (mkBetree_leaf_t id0 + params.(Betree_params_split_size)) in + let n2 := BetreeNodeLeaf (mkBetree_leaf_t id1 + params.(Betree_params_split_size)) in + Return (st1, mkBetree_internal_t self.(Betree_leaf_id) pivot n1 n2) end . @@ -257,25 +252,21 @@ Definition betree_leaf_split_back 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 + p <- + betree_list_split_at_fwd (u64 * u64) n0 content + params.(Betree_params_split_size); + 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 + node_id_cnt1 <- betree_node_id_counter_fresh_id_back node_id_cnt0; + Return node_id_cnt1 end . @@ -423,84 +414,69 @@ Fixpoint betree_node_lookup_fwd | 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 + p <- betree_load_internal_node_fwd node.(Betree_internal_id) 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 node 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, msg) l); + (BetreeListCons (k, BetreeMessageInsert v) 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 + 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 node 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 node key st0; + 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 node0.(Betree_internal_id) msgs0 + st2; + let (st3, _) := p3 in + Return (st3, Some v0) + end + | BetreeListNil => + p0 <- betree_internal_lookup_in_children_fwd n0 node 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 | 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 + p <- betree_load_leaf_node_fwd node.(Betree_leaf_id) st; + let (st0, bindings) := p in + opt <- betree_node_lookup_in_bindings_fwd n0 key bindings; + Return (st0, opt) end end @@ -514,83 +490,68 @@ with betree_node_lookup_back | 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 ( + p <- betree_load_internal_node_fwd node.(Betree_internal_id) 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 node 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, msg) l); + (BetreeListCons (k, BetreeMessageInsert v) 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 + Return (BetreeNodeInternal node) + | BetreeMessageDelete => + l0 <- + betree_node_lookup_first_message_for_key_back n0 key msgs + (BetreeListCons (k, BetreeMessageDelete) l); + let _ := l0 in + Return (BetreeNodeInternal node) + | BetreeMessageUpsert ufs => + p1 <- betree_internal_lookup_in_children_fwd n0 node 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 node key st0; + 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 node0.(Betree_internal_id) msgs0 + st2; + let (_, _) := p3 in + Return (BetreeNodeInternal node0) + 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 node key st0; + Return (BetreeNodeInternal node0) 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 + p <- betree_load_leaf_node_fwd node.(Betree_leaf_id) st; + let (_, bindings) := p in + opt <- betree_node_lookup_in_bindings_fwd n0 key bindings; + let _ := opt in + Return (BetreeNodeLeaf node) end end @@ -602,18 +563,15 @@ with betree_internal_lookup_in_children_fwd 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 + if key s< self.(Betree_internal_pivot) + then ( + p <- betree_node_lookup_fwd n0 self.(Betree_internal_left) key st; + let (st0, opt) := p in + Return (st0, opt)) + else ( + p <- betree_node_lookup_fwd n0 self.(Betree_internal_right) key st; + let (st0, opt) := p in + Return (st0, opt)) end (** [betree_main::betree::Internal::{4}::lookup_in_children] *) @@ -624,16 +582,15 @@ with betree_internal_lookup_in_children_back 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 + if key s< self.(Betree_internal_pivot) + then ( + n1 <- betree_node_lookup_back n0 self.(Betree_internal_left) key st; + Return (mkBetree_internal_t self.(Betree_internal_id) + self.(Betree_internal_pivot) n1 self.(Betree_internal_right))) + else ( + n1 <- betree_node_lookup_back n0 self.(Betree_internal_right) key st; + Return (mkBetree_internal_t self.(Betree_internal_id) + self.(Betree_internal_pivot) self.(Betree_internal_left) n1)) end . @@ -933,63 +890,47 @@ Fixpoint betree_node_apply_messages_fwd | 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 + p <- betree_load_internal_node_fwd node.(Betree_internal_id) 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; + if num_msgs s>= params.(Betree_params_min_flush_size) + then ( + p0 <- + betree_internal_flush_fwd n0 node params node_id_cnt content0 st0; + let (st1, content1) := p0 in + p1 <- + betree_internal_flush_back n0 node params node_id_cnt content0 st0; + let (node0, _) := p1 in + p2 <- + betree_store_internal_node_fwd node0.(Betree_internal_id) content1 + st1; + let (st2, _) := p2 in + Return (st2, tt)) + else ( + p0 <- + betree_store_internal_node_fwd node.(Betree_internal_id) content0 st0; + let (st1, _) := p0 in + Return (st1, tt)) | 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 + p <- betree_load_leaf_node_fwd node.(Betree_leaf_id) 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; + i <- u64_mul 2%u64 params.(Betree_params_split_size); + if len s>= i + then ( + p0 <- betree_leaf_split_fwd n0 node content0 params node_id_cnt st0; + let (st1, _) := p0 in + p1 <- + betree_store_leaf_node_fwd node.(Betree_leaf_id) BetreeListNil st1; + let (st2, _) := p1 in + Return (st2, tt)) + else ( + p0 <- betree_store_leaf_node_fwd node.(Betree_leaf_id) content0 st0; + let (st1, _) := p0 in + Return (st1, tt)) end end @@ -1005,68 +946,50 @@ with betree_node_apply_messages_back | 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 + p <- betree_load_internal_node_fwd node.(Betree_internal_id) 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; + if num_msgs s>= params.(Betree_params_min_flush_size) + then ( + p0 <- + betree_internal_flush_fwd n0 node params node_id_cnt content0 st0; + let (st1, content1) := p0 in + p1 <- + betree_internal_flush_back n0 node params node_id_cnt content0 st0; + let (node0, node_id_cnt0) := p1 in + p2 <- + betree_store_internal_node_fwd node0.(Betree_internal_id) content1 + st1; + let (_, _) := p2 in + Return (BetreeNodeInternal node0, node_id_cnt0)) + else ( + p0 <- + betree_store_internal_node_fwd node.(Betree_internal_id) content0 st0; + let (_, _) := p0 in + Return (BetreeNodeInternal node, node_id_cnt)) | 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 + p <- betree_load_leaf_node_fwd node.(Betree_leaf_id) 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; + i <- u64_mul 2%u64 params.(Betree_params_split_size); + if len s>= i + then ( + p0 <- betree_leaf_split_fwd n0 node content0 params node_id_cnt st0; + let (st1, new_node) := p0 in + p1 <- + betree_store_leaf_node_fwd node.(Betree_leaf_id) BetreeListNil st1; + let (_, _) := p1 in + node_id_cnt0 <- + betree_leaf_split_back n0 node content0 params node_id_cnt st0; + Return (BetreeNodeInternal new_node, node_id_cnt0)) + else ( + p0 <- betree_store_leaf_node_fwd node.(Betree_leaf_id) content0 st0; + let (_, _) := p0 in + Return (BetreeNodeLeaf (mkBetree_leaf_t node.(Betree_leaf_id) len), + node_id_cnt)) end end @@ -1080,49 +1003,44 @@ with betree_internal_flush_fwd 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 + p <- + betree_list_partition_at_pivot_fwd Betree_message_t n0 content + self.(Betree_internal_pivot); + let (msgs_left, msgs_right) := p in + len_left <- betree_list_len_fwd (u64 * Betree_message_t) n0 msgs_left; + if len_left s>= params.(Betree_params_min_flush_size) + then ( + p0 <- + betree_node_apply_messages_fwd n0 self.(Betree_internal_left) params + node_id_cnt msgs_left st; + let (st0, _) := p0 in + p1 <- + betree_node_apply_messages_back n0 self.(Betree_internal_left) params + node_id_cnt msgs_left st; + let (_, node_id_cnt0) := p1 in + len_right <- betree_list_len_fwd (u64 * Betree_message_t) n0 msgs_right; + if len_right s>= params.(Betree_params_min_flush_size) + then ( + p2 <- + betree_node_apply_messages_fwd n0 self.(Betree_internal_right) params + node_id_cnt0 msgs_right st0; + let (st1, _) := p2 in + p3 <- + betree_node_apply_messages_back n0 self.(Betree_internal_right) + params 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 self.(Betree_internal_right) params + node_id_cnt msgs_right st; + let (st0, _) := p0 in + p1 <- + betree_node_apply_messages_back n0 self.(Betree_internal_right) params + node_id_cnt msgs_right st; + let (_, _) := p1 in + Return (st0, msgs_left)) end (** [betree_main::betree::Internal::{4}::flush] *) @@ -1135,41 +1053,42 @@ with betree_internal_flush_back 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 + p <- + betree_list_partition_at_pivot_fwd Betree_message_t n0 content + self.(Betree_internal_pivot); + let (msgs_left, msgs_right) := p in + len_left <- betree_list_len_fwd (u64 * Betree_message_t) n0 msgs_left; + if len_left s>= params.(Betree_params_min_flush_size) + then ( + p0 <- + betree_node_apply_messages_fwd n0 self.(Betree_internal_left) params + node_id_cnt msgs_left st; + let (st0, _) := p0 in + p1 <- + betree_node_apply_messages_back n0 self.(Betree_internal_left) params + node_id_cnt msgs_left st; + let (n1, node_id_cnt0) := p1 in + len_right <- betree_list_len_fwd (u64 * Betree_message_t) n0 msgs_right; + if len_right s>= params.(Betree_params_min_flush_size) + then ( + p2 <- + betree_node_apply_messages_back n0 self.(Betree_internal_right) + params node_id_cnt0 msgs_right st0; + let (n2, node_id_cnt1) := p2 in + Return (mkBetree_internal_t self.(Betree_internal_id) + self.(Betree_internal_pivot) n1 n2, node_id_cnt1)) + else + Return (mkBetree_internal_t self.(Betree_internal_id) + self.(Betree_internal_pivot) n1 self.(Betree_internal_right), + node_id_cnt0)) + else ( + p0 <- + betree_node_apply_messages_back n0 self.(Betree_internal_right) params + node_id_cnt msgs_right st; + let (n1, node_id_cnt0) := p0 in + Return (mkBetree_internal_t self.(Betree_internal_id) + self.(Betree_internal_pivot) self.(Betree_internal_left) n1, + node_id_cnt0)) end . @@ -1238,14 +1157,17 @@ Definition betree_be_tree_apply_fwd 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 + p <- + betree_node_apply_fwd n0 self.(Betree_be_tree_root) + self.(Betree_be_tree_params) self.(Betree_be_tree_node_id_cnt) key msg + st; + let (st0, _) := p in + p0 <- + betree_node_apply_back n0 self.(Betree_be_tree_root) + self.(Betree_be_tree_params) self.(Betree_be_tree_node_id_cnt) key msg + st; + let (_, _) := p0 in + Return (st0, tt) end . @@ -1258,12 +1180,12 @@ Definition betree_be_tree_apply_back 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 + p <- + betree_node_apply_back n0 self.(Betree_be_tree_root) + self.(Betree_be_tree_params) self.(Betree_be_tree_node_id_cnt) key msg + st; + let (n1, nic) := p in + Return (mkBetree_be_tree_t self.(Betree_be_tree_params) nic n1) end . @@ -1366,12 +1288,9 @@ Definition betree_be_tree_lookup_fwd 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 + p <- betree_node_lookup_fwd n0 self.(Betree_be_tree_root) key st; + let (st0, opt) := p in + Return (st0, opt) end . @@ -1383,11 +1302,9 @@ Definition betree_be_tree_lookup_back 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 + n1 <- betree_node_lookup_back n0 self.(Betree_be_tree_root) key st; + Return (mkBetree_be_tree_t self.(Betree_be_tree_params) + self.(Betree_be_tree_node_id_cnt) n1) end . diff --git a/tests/coq/betree/BetreeMain_Types.v b/tests/coq/betree/BetreeMain_Types.v index 672b2ebd..d02289de 100644 --- a/tests/coq/betree/BetreeMain_Types.v +++ b/tests/coq/betree/BetreeMain_Types.v @@ -50,6 +50,35 @@ with Betree_internal_t := Betree_internal_t . +Definition Betree_internal_id (x : Betree_internal_t) := + match x with | mkBetree_internal_t x0 _ _ _ => x0 end +. + +Notation "x1 .(Betree_internal_id)" := (Betree_internal_id x1) (at level 9). + +Definition Betree_internal_pivot (x : Betree_internal_t) := + match x with | mkBetree_internal_t _ x0 _ _ => x0 end +. + +Notation "x1 .(Betree_internal_pivot)" := (Betree_internal_pivot x1) + (at level 9) +. + +Definition Betree_internal_left (x : Betree_internal_t) := + match x with | mkBetree_internal_t _ _ x0 _ => x0 end +. + +Notation "x1 .(Betree_internal_left)" := (Betree_internal_left x1) (at level 9) +. + +Definition Betree_internal_right (x : Betree_internal_t) := + match x with | mkBetree_internal_t _ _ _ x0 => x0 end +. + +Notation "x1 .(Betree_internal_right)" := (Betree_internal_right x1) + (at level 9) +. + (** [betree_main::betree::Params] *) Record Betree_params_t := mkBetree_params_t { diff --git a/tests/coq/betree/_CoqProject b/tests/coq/betree/_CoqProject index 5e08a7a6..3cf45746 100644 --- a/tests/coq/betree/_CoqProject +++ b/tests/coq/betree/_CoqProject @@ -4,6 +4,6 @@ Primitives.v -BetreeMain__Funs.v -BetreeMain__Opaque.v -BetreeMain__Types.v
\ No newline at end of file +BetreeMain_Funs.v +BetreeMain_Opaque.v +BetreeMain_Types.v
\ No newline at end of file diff --git a/tests/coq/hashmap/Hashmap_Funs.v b/tests/coq/hashmap/Hashmap_Funs.v index 912b7fe2..d12ee1b9 100644 --- a/tests/coq/hashmap/Hashmap_Funs.v +++ b/tests/coq/hashmap/Hashmap_Funs.v @@ -82,17 +82,15 @@ Definition hash_map_clear_fwd_back match n with | O => Fail_ OutOfFuel | S n0 => - match self with - | mkHash_map_t i p i0 v => - v0 <- hash_map_clear_slots_fwd_back T n0 v (0%usize); - Return (mkHash_map_t (0%usize) p i0 v0) - end + v <- hash_map_clear_slots_fwd_back T n0 self.(Hash_map_slots) (0%usize); + Return (mkHash_map_t (0%usize) self.(Hash_map_max_load_factor) + self.(Hash_map_max_load) v) end . (** [hashmap::HashMap::{0}::len] *) Definition hash_map_len_fwd (T : Type) (self : Hash_map_t T) : result usize := - match self with | mkHash_map_t i p i0 v => Return i end + Return self.(Hash_map_num_entries) . (** [hashmap::HashMap::{0}::insert_in_list] *) @@ -142,23 +140,22 @@ Definition hash_map_insert_no_resize_fwd_back | O => Fail_ OutOfFuel | S n0 => hash <- hash_key_fwd key; - match self with - | mkHash_map_t i p i0 v => - let i1 := vec_len (List_t T) v in - hash_mod <- usize_rem hash i1; - l <- vec_index_mut_fwd (List_t T) v hash_mod; - inserted <- hash_map_insert_in_list_fwd T n0 key value l; - if inserted - then ( - i2 <- usize_add i 1%usize; - l0 <- hash_map_insert_in_list_back T n0 key value l; - v0 <- vec_index_mut_back (List_t T) v hash_mod l0; - Return (mkHash_map_t i2 p i0 v0)) - else ( - l0 <- hash_map_insert_in_list_back T n0 key value l; - v0 <- vec_index_mut_back (List_t T) v hash_mod l0; - Return (mkHash_map_t i p i0 v0)) - end + let i := vec_len (List_t T) self.(Hash_map_slots) in + hash_mod <- usize_rem hash i; + l <- vec_index_mut_fwd (List_t T) self.(Hash_map_slots) hash_mod; + inserted <- hash_map_insert_in_list_fwd T n0 key value l; + if inserted + then ( + i0 <- usize_add self.(Hash_map_num_entries) 1%usize; + l0 <- hash_map_insert_in_list_back T n0 key value l; + v <- vec_index_mut_back (List_t T) self.(Hash_map_slots) hash_mod l0; + Return (mkHash_map_t i0 self.(Hash_map_max_load_factor) + self.(Hash_map_max_load) v)) + else ( + l0 <- hash_map_insert_in_list_back T n0 key value l; + v <- vec_index_mut_back (List_t T) self.(Hash_map_slots) hash_mod l0; + Return (mkHash_map_t self.(Hash_map_num_entries) + self.(Hash_map_max_load_factor) self.(Hash_map_max_load) v)) end . @@ -216,23 +213,23 @@ Definition hash_map_try_resize_fwd_back | O => Fail_ OutOfFuel | S n0 => max_usize <- scalar_cast U32 Usize core_num_u32_max_c; - match self with - | mkHash_map_t i p i0 v => - let capacity := vec_len (List_t T) v in - n1 <- usize_div max_usize 2%usize; - let (i1, i2) := p in - i3 <- usize_div n1 i1; - if capacity s<= i3 - then ( - i4 <- usize_mul capacity 2%usize; - ntable <- hash_map_new_with_capacity_fwd T n0 i4 i1 i2; - p0 <- hash_map_move_elements_fwd_back T n0 ntable v (0%usize); - let (ntable0, _) := p0 in - match ntable0 with - | mkHash_map_t i5 p1 i6 v0 => Return (mkHash_map_t i (i1, i2) i6 v0) - end) - else Return (mkHash_map_t i (i1, i2) i0 v) - end + let capacity := vec_len (List_t T) self.(Hash_map_slots) in + n1 <- usize_div max_usize 2%usize; + let (i, i0) := self.(Hash_map_max_load_factor) in + i1 <- usize_div n1 i; + if capacity s<= i1 + then ( + i2 <- usize_mul capacity 2%usize; + ntable <- hash_map_new_with_capacity_fwd T n0 i2 i i0; + p <- + hash_map_move_elements_fwd_back T n0 ntable self.(Hash_map_slots) + (0%usize); + let (ntable0, _) := p in + Return (mkHash_map_t self.(Hash_map_num_entries) (i, i0) + ntable0.(Hash_map_max_load) ntable0.(Hash_map_slots))) + else + Return (mkHash_map_t self.(Hash_map_num_entries) (i, i0) + self.(Hash_map_max_load) self.(Hash_map_slots)) end . @@ -246,14 +243,9 @@ Definition hash_map_insert_fwd_back | S n0 => self0 <- hash_map_insert_no_resize_fwd_back T n0 self key value; i <- hash_map_len_fwd T self0; - match self0 with - | mkHash_map_t i0 p i1 v => - if i s> i1 - then ( - self1 <- hash_map_try_resize_fwd_back T n0 (mkHash_map_t i0 p i1 v); - Return self1) - else Return (mkHash_map_t i0 p i1 v) - end + if i s> self0.(Hash_map_max_load) + then (self1 <- hash_map_try_resize_fwd_back T n0 self0; Return self1) + else Return self0 end . @@ -280,14 +272,11 @@ Definition hash_map_contains_key_fwd | O => Fail_ OutOfFuel | S n0 => hash <- hash_key_fwd key; - match self with - | mkHash_map_t i p i0 v => - let i1 := vec_len (List_t T) v in - hash_mod <- usize_rem hash i1; - l <- vec_index_fwd (List_t T) v hash_mod; - b <- hash_map_contains_key_in_list_fwd T n0 key l; - Return b - end + let i := vec_len (List_t T) self.(Hash_map_slots) in + hash_mod <- usize_rem hash i; + l <- vec_index_fwd (List_t T) self.(Hash_map_slots) hash_mod; + b <- hash_map_contains_key_in_list_fwd T n0 key l; + Return b end . @@ -314,14 +303,11 @@ Definition hash_map_get_fwd | O => Fail_ OutOfFuel | S n0 => hash <- hash_key_fwd key; - match self with - | mkHash_map_t i p i0 v => - let i1 := vec_len (List_t T) v in - hash_mod <- usize_rem hash i1; - l <- vec_index_fwd (List_t T) v hash_mod; - t <- hash_map_get_in_list_fwd T n0 key l; - Return t - end + let i := vec_len (List_t T) self.(Hash_map_slots) in + hash_mod <- usize_rem hash i; + l <- vec_index_fwd (List_t T) self.(Hash_map_slots) hash_mod; + t <- hash_map_get_in_list_fwd T n0 key l; + Return t end . @@ -368,14 +354,11 @@ Definition hash_map_get_mut_fwd | O => Fail_ OutOfFuel | S n0 => hash <- hash_key_fwd key; - match self with - | mkHash_map_t i p i0 v => - let i1 := vec_len (List_t T) v in - hash_mod <- usize_rem hash i1; - l <- vec_index_mut_fwd (List_t T) v hash_mod; - t <- hash_map_get_mut_in_list_fwd T n0 key l; - Return t - end + let i := vec_len (List_t T) self.(Hash_map_slots) in + hash_mod <- usize_rem hash i; + l <- vec_index_mut_fwd (List_t T) self.(Hash_map_slots) hash_mod; + t <- hash_map_get_mut_in_list_fwd T n0 key l; + Return t end . @@ -388,15 +371,13 @@ Definition hash_map_get_mut_back | O => Fail_ OutOfFuel | S n0 => hash <- hash_key_fwd key; - match self with - | mkHash_map_t i p i0 v => - let i1 := vec_len (List_t T) v in - hash_mod <- usize_rem hash i1; - l <- vec_index_mut_fwd (List_t T) v hash_mod; - l0 <- hash_map_get_mut_in_list_back T n0 key l ret; - v0 <- vec_index_mut_back (List_t T) v hash_mod l0; - Return (mkHash_map_t i p i0 v0) - end + let i := vec_len (List_t T) self.(Hash_map_slots) in + hash_mod <- usize_rem hash i; + l <- vec_index_mut_fwd (List_t T) self.(Hash_map_slots) hash_mod; + l0 <- hash_map_get_mut_in_list_back T n0 key l ret; + v <- vec_index_mut_back (List_t T) self.(Hash_map_slots) hash_mod l0; + Return (mkHash_map_t self.(Hash_map_num_entries) + self.(Hash_map_max_load_factor) self.(Hash_map_max_load) v) end . @@ -453,16 +434,16 @@ Definition hash_map_remove_fwd | O => Fail_ OutOfFuel | S n0 => hash <- hash_key_fwd key; - match self with - | mkHash_map_t i p i0 v => - let i1 := vec_len (List_t T) v in - hash_mod <- usize_rem hash i1; - l <- vec_index_mut_fwd (List_t T) v hash_mod; - x <- hash_map_remove_from_list_fwd T n0 key l; - match x with - | None => Return None - | Some x0 => i2 <- usize_sub i 1%usize; let _ := i2 in Return (Some x0) - end + let i := vec_len (List_t T) self.(Hash_map_slots) in + hash_mod <- usize_rem hash i; + l <- vec_index_mut_fwd (List_t T) self.(Hash_map_slots) hash_mod; + x <- hash_map_remove_from_list_fwd T n0 key l; + match x with + | None => Return None + | Some x0 => + i0 <- usize_sub self.(Hash_map_num_entries) 1%usize; + let _ := i0 in + Return (Some x0) end end . @@ -476,23 +457,22 @@ Definition hash_map_remove_back | O => Fail_ OutOfFuel | S n0 => hash <- hash_key_fwd key; - match self with - | mkHash_map_t i p i0 v => - let i1 := vec_len (List_t T) v in - hash_mod <- usize_rem hash i1; - l <- vec_index_mut_fwd (List_t T) v hash_mod; - x <- hash_map_remove_from_list_fwd T n0 key l; - match x with - | None => - l0 <- hash_map_remove_from_list_back T n0 key l; - v0 <- vec_index_mut_back (List_t T) v hash_mod l0; - Return (mkHash_map_t i p i0 v0) - | Some x0 => - i2 <- usize_sub i 1%usize; - l0 <- hash_map_remove_from_list_back T n0 key l; - v0 <- vec_index_mut_back (List_t T) v hash_mod l0; - Return (mkHash_map_t i2 p i0 v0) - end + let i := vec_len (List_t T) self.(Hash_map_slots) in + hash_mod <- usize_rem hash i; + l <- vec_index_mut_fwd (List_t T) self.(Hash_map_slots) hash_mod; + x <- hash_map_remove_from_list_fwd T n0 key l; + match x with + | None => + l0 <- hash_map_remove_from_list_back T n0 key l; + v <- vec_index_mut_back (List_t T) self.(Hash_map_slots) hash_mod l0; + Return (mkHash_map_t self.(Hash_map_num_entries) + self.(Hash_map_max_load_factor) self.(Hash_map_max_load) v) + | Some x0 => + i0 <- usize_sub self.(Hash_map_num_entries) 1%usize; + l0 <- hash_map_remove_from_list_back T n0 key l; + v <- vec_index_mut_back (List_t T) self.(Hash_map_slots) hash_mod l0; + Return (mkHash_map_t i0 self.(Hash_map_max_load_factor) + self.(Hash_map_max_load) v) end end . diff --git a/tests/coq/hashmap/_CoqProject b/tests/coq/hashmap/_CoqProject index 2aa6b46c..94708adc 100644 --- a/tests/coq/hashmap/_CoqProject +++ b/tests/coq/hashmap/_CoqProject @@ -4,5 +4,5 @@ Primitives.v -Hashmap__Types.v -Hashmap__Funs.v
\ No newline at end of file +Hashmap_Types.v +Hashmap_Funs.v
\ No newline at end of file diff --git a/tests/coq/hashmap_on_disk/HashmapMain_Funs.v b/tests/coq/hashmap_on_disk/HashmapMain_Funs.v index b4351dc3..94a390df 100644 --- a/tests/coq/hashmap_on_disk/HashmapMain_Funs.v +++ b/tests/coq/hashmap_on_disk/HashmapMain_Funs.v @@ -89,18 +89,19 @@ Definition hashmap_hash_map_clear_fwd_back match n with | O => Fail_ OutOfFuel | S n0 => - match self with - | mkHashmap_hash_map_t i p i0 v => - v0 <- hashmap_hash_map_clear_slots_fwd_back T n0 v (0%usize); - Return (mkHashmap_hash_map_t (0%usize) p i0 v0) - end + v <- + hashmap_hash_map_clear_slots_fwd_back T n0 self.(Hashmap_hash_map_slots) + (0%usize); + Return (mkHashmap_hash_map_t (0%usize) + self.(Hashmap_hash_map_max_load_factor) self.(Hashmap_hash_map_max_load) + v) end . (** [hashmap_main::hashmap::HashMap::{0}::len] *) Definition hashmap_hash_map_len_fwd (T : Type) (self : Hashmap_hash_map_t T) : result usize := - match self with | mkHashmap_hash_map_t i p i0 v => Return i end + Return self.(Hashmap_hash_map_num_entries) . (** [hashmap_main::hashmap::HashMap::{0}::insert_in_list] *) @@ -153,23 +154,29 @@ Definition hashmap_hash_map_insert_no_resize_fwd_back | O => Fail_ OutOfFuel | S n0 => hash <- hashmap_hash_key_fwd key; - match self with - | mkHashmap_hash_map_t i p i0 v => - let i1 := vec_len (Hashmap_list_t T) v in - hash_mod <- usize_rem hash i1; - l <- vec_index_mut_fwd (Hashmap_list_t T) v hash_mod; - inserted <- hashmap_hash_map_insert_in_list_fwd T n0 key value l; - if inserted - then ( - i2 <- usize_add i 1%usize; - l0 <- hashmap_hash_map_insert_in_list_back T n0 key value l; - v0 <- vec_index_mut_back (Hashmap_list_t T) v hash_mod l0; - Return (mkHashmap_hash_map_t i2 p i0 v0)) - else ( - l0 <- hashmap_hash_map_insert_in_list_back T n0 key value l; - v0 <- vec_index_mut_back (Hashmap_list_t T) v hash_mod l0; - Return (mkHashmap_hash_map_t i p i0 v0)) - end + let i := vec_len (Hashmap_list_t T) self.(Hashmap_hash_map_slots) in + hash_mod <- usize_rem hash i; + l <- + vec_index_mut_fwd (Hashmap_list_t T) self.(Hashmap_hash_map_slots) + hash_mod; + inserted <- hashmap_hash_map_insert_in_list_fwd T n0 key value l; + if inserted + then ( + i0 <- usize_add self.(Hashmap_hash_map_num_entries) 1%usize; + l0 <- hashmap_hash_map_insert_in_list_back T n0 key value l; + v <- + vec_index_mut_back (Hashmap_list_t T) self.(Hashmap_hash_map_slots) + hash_mod l0; + Return (mkHashmap_hash_map_t i0 self.(Hashmap_hash_map_max_load_factor) + self.(Hashmap_hash_map_max_load) v)) + else ( + l0 <- hashmap_hash_map_insert_in_list_back T n0 key value l; + v <- + vec_index_mut_back (Hashmap_list_t T) self.(Hashmap_hash_map_slots) + hash_mod l0; + Return (mkHashmap_hash_map_t self.(Hashmap_hash_map_num_entries) + self.(Hashmap_hash_map_max_load_factor) + self.(Hashmap_hash_map_max_load) v)) end . @@ -232,24 +239,23 @@ Definition hashmap_hash_map_try_resize_fwd_back | O => Fail_ OutOfFuel | S n0 => max_usize <- scalar_cast U32 Usize core_num_u32_max_c; - match self with - | mkHashmap_hash_map_t i p i0 v => - let capacity := vec_len (Hashmap_list_t T) v in - n1 <- usize_div max_usize 2%usize; - let (i1, i2) := p in - i3 <- usize_div n1 i1; - if capacity s<= i3 - then ( - i4 <- usize_mul capacity 2%usize; - ntable <- hashmap_hash_map_new_with_capacity_fwd T n0 i4 i1 i2; - p0 <- hashmap_hash_map_move_elements_fwd_back T n0 ntable v (0%usize); - let (ntable0, _) := p0 in - match ntable0 with - | mkHashmap_hash_map_t i5 p1 i6 v0 => - Return (mkHashmap_hash_map_t i (i1, i2) i6 v0) - end) - else Return (mkHashmap_hash_map_t i (i1, i2) i0 v) - end + let capacity := vec_len (Hashmap_list_t T) self.(Hashmap_hash_map_slots) in + n1 <- usize_div max_usize 2%usize; + let (i, i0) := self.(Hashmap_hash_map_max_load_factor) in + i1 <- usize_div n1 i; + if capacity s<= i1 + then ( + i2 <- usize_mul capacity 2%usize; + ntable <- hashmap_hash_map_new_with_capacity_fwd T n0 i2 i i0; + p <- + hashmap_hash_map_move_elements_fwd_back T n0 ntable + self.(Hashmap_hash_map_slots) (0%usize); + let (ntable0, _) := p in + Return (mkHashmap_hash_map_t self.(Hashmap_hash_map_num_entries) (i, i0) + ntable0.(Hashmap_hash_map_max_load) ntable0.(Hashmap_hash_map_slots))) + else + Return (mkHashmap_hash_map_t self.(Hashmap_hash_map_num_entries) (i, i0) + self.(Hashmap_hash_map_max_load) self.(Hashmap_hash_map_slots)) end . @@ -264,16 +270,10 @@ Definition hashmap_hash_map_insert_fwd_back | S n0 => self0 <- hashmap_hash_map_insert_no_resize_fwd_back T n0 self key value; i <- hashmap_hash_map_len_fwd T self0; - match self0 with - | mkHashmap_hash_map_t i0 p i1 v => - if i s> i1 - then ( - self1 <- - hashmap_hash_map_try_resize_fwd_back T n0 (mkHashmap_hash_map_t i0 p - i1 v); - Return self1) - else Return (mkHashmap_hash_map_t i0 p i1 v) - end + if i s> self0.(Hashmap_hash_map_max_load) + then ( + self1 <- hashmap_hash_map_try_resize_fwd_back T n0 self0; Return self1) + else Return self0 end . @@ -303,14 +303,12 @@ Definition hashmap_hash_map_contains_key_fwd | O => Fail_ OutOfFuel | S n0 => hash <- hashmap_hash_key_fwd key; - match self with - | mkHashmap_hash_map_t i p i0 v => - let i1 := vec_len (Hashmap_list_t T) v in - hash_mod <- usize_rem hash i1; - l <- vec_index_fwd (Hashmap_list_t T) v hash_mod; - b <- hashmap_hash_map_contains_key_in_list_fwd T n0 key l; - Return b - end + let i := vec_len (Hashmap_list_t T) self.(Hashmap_hash_map_slots) in + hash_mod <- usize_rem hash i; + l <- + vec_index_fwd (Hashmap_list_t T) self.(Hashmap_hash_map_slots) hash_mod; + b <- hashmap_hash_map_contains_key_in_list_fwd T n0 key l; + Return b end . @@ -339,14 +337,12 @@ Definition hashmap_hash_map_get_fwd | O => Fail_ OutOfFuel | S n0 => hash <- hashmap_hash_key_fwd key; - match self with - | mkHashmap_hash_map_t i p i0 v => - let i1 := vec_len (Hashmap_list_t T) v in - hash_mod <- usize_rem hash i1; - l <- vec_index_fwd (Hashmap_list_t T) v hash_mod; - t <- hashmap_hash_map_get_in_list_fwd T n0 key l; - Return t - end + let i := vec_len (Hashmap_list_t T) self.(Hashmap_hash_map_slots) in + hash_mod <- usize_rem hash i; + l <- + vec_index_fwd (Hashmap_list_t T) self.(Hashmap_hash_map_slots) hash_mod; + t <- hashmap_hash_map_get_in_list_fwd T n0 key l; + Return t end . @@ -395,14 +391,13 @@ Definition hashmap_hash_map_get_mut_fwd | O => Fail_ OutOfFuel | S n0 => hash <- hashmap_hash_key_fwd key; - match self with - | mkHashmap_hash_map_t i p i0 v => - let i1 := vec_len (Hashmap_list_t T) v in - hash_mod <- usize_rem hash i1; - l <- vec_index_mut_fwd (Hashmap_list_t T) v hash_mod; - t <- hashmap_hash_map_get_mut_in_list_fwd T n0 key l; - Return t - end + let i := vec_len (Hashmap_list_t T) self.(Hashmap_hash_map_slots) in + hash_mod <- usize_rem hash i; + l <- + vec_index_mut_fwd (Hashmap_list_t T) self.(Hashmap_hash_map_slots) + hash_mod; + t <- hashmap_hash_map_get_mut_in_list_fwd T n0 key l; + Return t end . @@ -415,15 +410,18 @@ Definition hashmap_hash_map_get_mut_back | O => Fail_ OutOfFuel | S n0 => hash <- hashmap_hash_key_fwd key; - match self with - | mkHashmap_hash_map_t i p i0 v => - let i1 := vec_len (Hashmap_list_t T) v in - hash_mod <- usize_rem hash i1; - l <- vec_index_mut_fwd (Hashmap_list_t T) v hash_mod; - l0 <- hashmap_hash_map_get_mut_in_list_back T n0 key l ret; - v0 <- vec_index_mut_back (Hashmap_list_t T) v hash_mod l0; - Return (mkHashmap_hash_map_t i p i0 v0) - end + let i := vec_len (Hashmap_list_t T) self.(Hashmap_hash_map_slots) in + hash_mod <- usize_rem hash i; + l <- + vec_index_mut_fwd (Hashmap_list_t T) self.(Hashmap_hash_map_slots) + hash_mod; + l0 <- hashmap_hash_map_get_mut_in_list_back T n0 key l ret; + v <- + vec_index_mut_back (Hashmap_list_t T) self.(Hashmap_hash_map_slots) + hash_mod l0; + Return (mkHashmap_hash_map_t self.(Hashmap_hash_map_num_entries) + self.(Hashmap_hash_map_max_load_factor) self.(Hashmap_hash_map_max_load) + v) end . @@ -489,16 +487,18 @@ Definition hashmap_hash_map_remove_fwd | O => Fail_ OutOfFuel | S n0 => hash <- hashmap_hash_key_fwd key; - match self with - | mkHashmap_hash_map_t i p i0 v => - let i1 := vec_len (Hashmap_list_t T) v in - hash_mod <- usize_rem hash i1; - l <- vec_index_mut_fwd (Hashmap_list_t T) v hash_mod; - x <- hashmap_hash_map_remove_from_list_fwd T n0 key l; - match x with - | None => Return None - | Some x0 => i2 <- usize_sub i 1%usize; let _ := i2 in Return (Some x0) - end + let i := vec_len (Hashmap_list_t T) self.(Hashmap_hash_map_slots) in + hash_mod <- usize_rem hash i; + l <- + vec_index_mut_fwd (Hashmap_list_t T) self.(Hashmap_hash_map_slots) + hash_mod; + x <- hashmap_hash_map_remove_from_list_fwd T n0 key l; + match x with + | None => Return None + | Some x0 => + i0 <- usize_sub self.(Hashmap_hash_map_num_entries) 1%usize; + let _ := i0 in + Return (Some x0) end end . @@ -512,23 +512,29 @@ Definition hashmap_hash_map_remove_back | O => Fail_ OutOfFuel | S n0 => hash <- hashmap_hash_key_fwd key; - match self with - | mkHashmap_hash_map_t i p i0 v => - let i1 := vec_len (Hashmap_list_t T) v in - hash_mod <- usize_rem hash i1; - l <- vec_index_mut_fwd (Hashmap_list_t T) v hash_mod; - x <- hashmap_hash_map_remove_from_list_fwd T n0 key l; - match x with - | None => - l0 <- hashmap_hash_map_remove_from_list_back T n0 key l; - v0 <- vec_index_mut_back (Hashmap_list_t T) v hash_mod l0; - Return (mkHashmap_hash_map_t i p i0 v0) - | Some x0 => - i2 <- usize_sub i 1%usize; - l0 <- hashmap_hash_map_remove_from_list_back T n0 key l; - v0 <- vec_index_mut_back (Hashmap_list_t T) v hash_mod l0; - Return (mkHashmap_hash_map_t i2 p i0 v0) - end + let i := vec_len (Hashmap_list_t T) self.(Hashmap_hash_map_slots) in + hash_mod <- usize_rem hash i; + l <- + vec_index_mut_fwd (Hashmap_list_t T) self.(Hashmap_hash_map_slots) + hash_mod; + x <- hashmap_hash_map_remove_from_list_fwd T n0 key l; + match x with + | None => + l0 <- hashmap_hash_map_remove_from_list_back T n0 key l; + v <- + vec_index_mut_back (Hashmap_list_t T) self.(Hashmap_hash_map_slots) + hash_mod l0; + Return (mkHashmap_hash_map_t self.(Hashmap_hash_map_num_entries) + self.(Hashmap_hash_map_max_load_factor) + self.(Hashmap_hash_map_max_load) v) + | Some x0 => + i0 <- usize_sub self.(Hashmap_hash_map_num_entries) 1%usize; + l0 <- hashmap_hash_map_remove_from_list_back T n0 key l; + v <- + vec_index_mut_back (Hashmap_list_t T) self.(Hashmap_hash_map_slots) + hash_mod l0; + Return (mkHashmap_hash_map_t i0 self.(Hashmap_hash_map_max_load_factor) + self.(Hashmap_hash_map_max_load) v) end end . diff --git a/tests/coq/hashmap_on_disk/_CoqProject b/tests/coq/hashmap_on_disk/_CoqProject index 10e247ae..95b82c41 100644 --- a/tests/coq/hashmap_on_disk/_CoqProject +++ b/tests/coq/hashmap_on_disk/_CoqProject @@ -4,6 +4,6 @@ Primitives.v -HashmapMain__Funs.v -HashmapMain__Opaque.v -HashmapMain__Types.v
\ No newline at end of file +HashmapMain_Funs.v +HashmapMain_Opaque.v +HashmapMain_Types.v
\ No newline at end of file diff --git a/tests/coq/misc/Constants.v b/tests/coq/misc/Constants.v index c9ec0daf..7d3e5a34 100644 --- a/tests/coq/misc/Constants.v +++ b/tests/coq/misc/Constants.v @@ -86,9 +86,7 @@ Definition y_body : result (Wrap_t i32) := Definition y_c : Wrap_t i32 := y_body%global. (** [constants::unwrap_y] *) -Definition unwrap_y_fwd : result i32 := - match y_c with | mkWrap_t i => Return i end -. +Definition unwrap_y_fwd : result i32 := Return y_c.(Wrap_val). (** [constants::YVAL] *) Definition yval_body : result i32 := i <- unwrap_y_fwd; Return i. diff --git a/tests/coq/misc/NoNestedBorrows.v b/tests/coq/misc/NoNestedBorrows.v index 7c5212b2..a5f6126b 100644 --- a/tests/coq/misc/NoNestedBorrows.v +++ b/tests/coq/misc/NoNestedBorrows.v @@ -460,37 +460,24 @@ Definition new_pair1_fwd : result (Struct_with_pair_t u32 u32) := (** [no_nested_borrows::test_constants] *) Definition test_constants_fwd : result unit := swt <- new_tuple1_fwd; - match swt with - | mkStruct_with_tuple_t p => - let (i, _) := p in - if negb (i s= 1%u32) + let (i, _) := swt.(Struct_with_tuple_p) in + if negb (i s= 1%u32) + then Fail_ Failure + else ( + swt0 <- new_tuple2_fwd; + let (i0, _) := swt0.(Struct_with_tuple_p) in + if negb (i0 s= 1%i16) then Fail_ Failure else ( - swt0 <- new_tuple2_fwd; - match swt0 with - | mkStruct_with_tuple_t p0 => - let (i0, _) := p0 in - if negb (i0 s= 1%i16) + swt1 <- new_tuple3_fwd; + let (i1, _) := swt1.(Struct_with_tuple_p) in + if negb (i1 s= 1%u64) + then Fail_ Failure + else ( + swp <- new_pair1_fwd; + if negb (swp.(Struct_with_pair_p).(Pair_x) s= 1%u32) then Fail_ Failure - else ( - swt1 <- new_tuple3_fwd; - match swt1 with - | mkStruct_with_tuple_t p1 => - let (i1, _) := p1 in - if negb (i1 s= 1%u64) - then Fail_ Failure - else ( - swp <- new_pair1_fwd; - match swp with - | mkStruct_with_pair_t p2 => - match p2 with - | mkPair_t i2 i3 => - if negb (i2 s= 1%u32) then Fail_ Failure else Return tt - end - end) - end) - end) - end + else Return tt))) . (** Unit test for [no_nested_borrows::test_constants] *) diff --git a/tests/coq/misc/_CoqProject b/tests/coq/misc/_CoqProject index 16fcaf44..b8590272 100644 --- a/tests/coq/misc/_CoqProject +++ b/tests/coq/misc/_CoqProject @@ -5,9 +5,9 @@ Primitives.v Constants.v -External__Funs.v -External__Opaque.v -External__Types.v +External_Funs.v +External_Opaque.v +External_Types.v NoNestedBorrows.v Paper.v PoloniusList.v
\ No newline at end of file |