diff options
Diffstat (limited to '')
| -rw-r--r-- | tests/coq/betree/BetreeMain_Funs.v | 198 | ||||
| -rw-r--r-- | tests/coq/betree/BetreeMain_Opaque.v | 15 | ||||
| -rw-r--r-- | tests/coq/betree/BetreeMain_Types.v | 27 | ||||
| -rw-r--r-- | tests/coq/betree/Primitives.v | 88 |
4 files changed, 203 insertions, 125 deletions
diff --git a/tests/coq/betree/BetreeMain_Funs.v b/tests/coq/betree/BetreeMain_Funs.v index 261e8270..8e48b17d 100644 --- a/tests/coq/betree/BetreeMain_Funs.v +++ b/tests/coq/betree/BetreeMain_Funs.v @@ -12,7 +12,8 @@ Require Export BetreeMain_Opaque. Import BetreeMain_Opaque. Module BetreeMain_Funs. -(** [betree_main::betree::load_internal_node]: forward function *) +(** [betree_main::betree::load_internal_node]: forward function + Source: 'src/betree.rs', lines 36:0-36:52 *) Definition betree_load_internal_node (id : u64) (st : state) : result (state * (betree_List_t (u64 * betree_Message_t))) @@ -20,7 +21,8 @@ Definition betree_load_internal_node betree_utils_load_internal_node id st . -(** [betree_main::betree::store_internal_node]: forward function *) +(** [betree_main::betree::store_internal_node]: forward function + Source: 'src/betree.rs', lines 41:0-41:60 *) Definition betree_store_internal_node (id : u64) (content : betree_List_t (u64 * betree_Message_t)) (st : state) : result (state * unit) @@ -30,13 +32,15 @@ Definition betree_store_internal_node Return (st0, tt) . -(** [betree_main::betree::load_leaf_node]: forward function *) +(** [betree_main::betree::load_leaf_node]: forward function + Source: 'src/betree.rs', lines 46:0-46:44 *) Definition betree_load_leaf_node (id : u64) (st : state) : result (state * (betree_List_t (u64 * u64))) := betree_utils_load_leaf_node id st . -(** [betree_main::betree::store_leaf_node]: forward function *) +(** [betree_main::betree::store_leaf_node]: forward function + Source: 'src/betree.rs', lines 51:0-51:52 *) Definition betree_store_leaf_node (id : u64) (content : betree_List_t (u64 * u64)) (st : state) : result (state * unit) @@ -46,36 +50,42 @@ Definition betree_store_leaf_node Return (st0, tt) . -(** [betree_main::betree::fresh_node_id]: forward function *) +(** [betree_main::betree::fresh_node_id]: forward function + Source: 'src/betree.rs', lines 55:0-55:48 *) Definition betree_fresh_node_id (counter : u64) : result u64 := _ <- u64_add counter 1%u64; Return counter . -(** [betree_main::betree::fresh_node_id]: backward function 0 *) +(** [betree_main::betree::fresh_node_id]: backward function 0 + Source: 'src/betree.rs', lines 55:0-55:48 *) Definition betree_fresh_node_id_back (counter : u64) : result u64 := u64_add counter 1%u64 . -(** [betree_main::betree::NodeIdCounter::{0}::new]: forward function *) +(** [betree_main::betree::{betree_main::betree::NodeIdCounter}::new]: forward function + Source: 'src/betree.rs', lines 206:4-206:20 *) Definition betree_NodeIdCounter_new : result betree_NodeIdCounter_t := Return {| betree_NodeIdCounter_next_node_id := 0%u64 |} . -(** [betree_main::betree::NodeIdCounter::{0}::fresh_id]: forward function *) +(** [betree_main::betree::{betree_main::betree::NodeIdCounter}::fresh_id]: forward function + Source: 'src/betree.rs', lines 210:4-210:36 *) Definition betree_NodeIdCounter_fresh_id (self : betree_NodeIdCounter_t) : result u64 := _ <- u64_add self.(betree_NodeIdCounter_next_node_id) 1%u64; Return self.(betree_NodeIdCounter_next_node_id) . -(** [betree_main::betree::NodeIdCounter::{0}::fresh_id]: backward function 0 *) +(** [betree_main::betree::{betree_main::betree::NodeIdCounter}::fresh_id]: backward function 0 + Source: 'src/betree.rs', lines 210:4-210:36 *) Definition betree_NodeIdCounter_fresh_id_back (self : betree_NodeIdCounter_t) : result betree_NodeIdCounter_t := i <- u64_add self.(betree_NodeIdCounter_next_node_id) 1%u64; Return {| betree_NodeIdCounter_next_node_id := i |} . -(** [betree_main::betree::upsert_update]: forward function *) +(** [betree_main::betree::upsert_update]: forward function + Source: 'src/betree.rs', lines 234:0-234:70 *) Definition betree_upsert_update (prev : option u64) (st : betree_UpsertFunState_t) : result u64 := match prev with @@ -95,7 +105,8 @@ Definition betree_upsert_update end . -(** [betree_main::betree::List::{1}::len]: forward function *) +(** [betree_main::betree::{betree_main::betree::List<T>#1}::len]: forward function + Source: 'src/betree.rs', lines 276:4-276:24 *) Fixpoint betree_List_len (T : Type) (n : nat) (self : betree_List_t T) : result u64 := match n with @@ -108,7 +119,8 @@ Fixpoint betree_List_len end . -(** [betree_main::betree::List::{1}::split_at]: forward function *) +(** [betree_main::betree::{betree_main::betree::List<T>#1}::split_at]: forward function + Source: 'src/betree.rs', lines 284:4-284:51 *) Fixpoint betree_List_split_at (T : Type) (n : nat) (self : betree_List_t T) (n0 : u64) : result ((betree_List_t T) * (betree_List_t T)) @@ -131,8 +143,9 @@ Fixpoint betree_List_split_at end . -(** [betree_main::betree::List::{1}::push_front]: merged forward/backward function - (there is a single backward function, and the forward function returns ()) *) +(** [betree_main::betree::{betree_main::betree::List<T>#1}::push_front]: merged forward/backward function + (there is a single backward function, and the forward function returns ()) + Source: 'src/betree.rs', lines 299:4-299:34 *) Definition betree_List_push_front (T : Type) (self : betree_List_t T) (x : T) : result (betree_List_t T) := let tl := core_mem_replace (betree_List_t T) self Betree_List_Nil in @@ -140,7 +153,8 @@ Definition betree_List_push_front Return (Betree_List_Cons x l) . -(** [betree_main::betree::List::{1}::pop_front]: forward function *) +(** [betree_main::betree::{betree_main::betree::List<T>#1}::pop_front]: forward function + Source: 'src/betree.rs', lines 306:4-306:32 *) Definition betree_List_pop_front (T : Type) (self : betree_List_t T) : result T := let ls := core_mem_replace (betree_List_t T) self Betree_List_Nil in @@ -150,7 +164,8 @@ Definition betree_List_pop_front end . -(** [betree_main::betree::List::{1}::pop_front]: backward function 0 *) +(** [betree_main::betree::{betree_main::betree::List<T>#1}::pop_front]: backward function 0 + Source: 'src/betree.rs', lines 306:4-306:32 *) Definition betree_List_pop_front_back (T : Type) (self : betree_List_t T) : result (betree_List_t T) := let ls := core_mem_replace (betree_List_t T) self Betree_List_Nil in @@ -160,7 +175,8 @@ Definition betree_List_pop_front_back end . -(** [betree_main::betree::List::{1}::hd]: forward function *) +(** [betree_main::betree::{betree_main::betree::List<T>#1}::hd]: forward function + Source: 'src/betree.rs', lines 318:4-318:22 *) Definition betree_List_hd (T : Type) (self : betree_List_t T) : result T := match self with | Betree_List_Cons hd l => Return hd @@ -168,8 +184,9 @@ Definition betree_List_hd (T : Type) (self : betree_List_t T) : result T := end . -(** [betree_main::betree::List::{2}::head_has_key]: forward function *) -Definition betree_List_head_has_key +(** [betree_main::betree::{betree_main::betree::List<(u64, T)>#2}::head_has_key]: forward function + Source: 'src/betree.rs', lines 327:4-327:44 *) +Definition betree_ListTupleU64T_head_has_key (T : Type) (self : betree_List_t (u64 * T)) (key : u64) : result bool := match self with | Betree_List_Cons hd l => let (i, _) := hd in Return (i s= key) @@ -177,8 +194,9 @@ Definition betree_List_head_has_key end . -(** [betree_main::betree::List::{2}::partition_at_pivot]: forward function *) -Fixpoint betree_List_partition_at_pivot +(** [betree_main::betree::{betree_main::betree::List<(u64, T)>#2}::partition_at_pivot]: forward function + Source: 'src/betree.rs', lines 339:4-339:73 *) +Fixpoint betree_ListTupleU64T_partition_at_pivot (T : Type) (n : nat) (self : betree_List_t (u64 * T)) (pivot : u64) : result ((betree_List_t (u64 * T)) * (betree_List_t (u64 * T))) := @@ -191,7 +209,7 @@ Fixpoint betree_List_partition_at_pivot if i s>= pivot then Return (Betree_List_Nil, Betree_List_Cons (i, t) tl) else ( - p <- betree_List_partition_at_pivot T n0 tl pivot; + p <- betree_ListTupleU64T_partition_at_pivot T n0 tl pivot; let (ls0, ls1) := p in let l := ls0 in Return (Betree_List_Cons (i, t) l, ls1)) @@ -200,7 +218,8 @@ Fixpoint betree_List_partition_at_pivot end . -(** [betree_main::betree::Leaf::{3}::split]: forward function *) +(** [betree_main::betree::{betree_main::betree::Leaf#3}::split]: forward function + Source: 'src/betree.rs', lines 359:4-364:17 *) Definition betree_Leaf_split (n : nat) (self : betree_Leaf_t) (content : betree_List_t (u64 * u64)) (params : betree_Params_t) (node_id_cnt : betree_NodeIdCounter_t) @@ -233,7 +252,8 @@ Definition betree_Leaf_split Return (st1, mkbetree_Internal_t self.(betree_Leaf_id) pivot n0 n1) . -(** [betree_main::betree::Leaf::{3}::split]: backward function 2 *) +(** [betree_main::betree::{betree_main::betree::Leaf#3}::split]: backward function 2 + Source: 'src/betree.rs', lines 359:4-364:17 *) Definition betree_Leaf_split_back (n : nat) (self : betree_Leaf_t) (content : betree_List_t (u64 * u64)) (params : betree_Params_t) (node_id_cnt : betree_NodeIdCounter_t) @@ -254,7 +274,8 @@ Definition betree_Leaf_split_back betree_NodeIdCounter_fresh_id_back node_id_cnt0 . -(** [betree_main::betree::Node::{5}::lookup_first_message_for_key]: forward function *) +(** [betree_main::betree::{betree_main::betree::Node#5}::lookup_first_message_for_key]: forward function + Source: 'src/betree.rs', lines 789:4-792:34 *) Fixpoint betree_Node_lookup_first_message_for_key (n : nat) (key : u64) (msgs : betree_List_t (u64 * betree_Message_t)) : result (betree_List_t (u64 * betree_Message_t)) @@ -273,7 +294,8 @@ Fixpoint betree_Node_lookup_first_message_for_key end . -(** [betree_main::betree::Node::{5}::lookup_first_message_for_key]: backward function 0 *) +(** [betree_main::betree::{betree_main::betree::Node#5}::lookup_first_message_for_key]: backward function 0 + Source: 'src/betree.rs', lines 789:4-792:34 *) Fixpoint betree_Node_lookup_first_message_for_key_back (n : nat) (key : u64) (msgs : betree_List_t (u64 * betree_Message_t)) (ret : betree_List_t (u64 * betree_Message_t)) : @@ -296,7 +318,8 @@ Fixpoint betree_Node_lookup_first_message_for_key_back end . -(** [betree_main::betree::Node::{5}::apply_upserts]: forward function *) +(** [betree_main::betree::{betree_main::betree::Node#5}::apply_upserts]: forward function + Source: 'src/betree.rs', lines 819:4-819:90 *) Fixpoint betree_Node_apply_upserts (n : nat) (msgs : betree_List_t (u64 * betree_Message_t)) (prev : option u64) (key : u64) (st : state) : @@ -305,7 +328,7 @@ Fixpoint betree_Node_apply_upserts match n with | O => Fail_ OutOfFuel | S n0 => - b <- betree_List_head_has_key betree_Message_t msgs key; + b <- betree_ListTupleU64T_head_has_key betree_Message_t msgs key; if b then ( msg <- betree_List_pop_front (u64 * betree_Message_t) msgs; @@ -328,7 +351,8 @@ Fixpoint betree_Node_apply_upserts end . -(** [betree_main::betree::Node::{5}::apply_upserts]: backward function 0 *) +(** [betree_main::betree::{betree_main::betree::Node#5}::apply_upserts]: backward function 0 + Source: 'src/betree.rs', lines 819:4-819:90 *) Fixpoint betree_Node_apply_upserts_back (n : nat) (msgs : betree_List_t (u64 * betree_Message_t)) (prev : option u64) (key : u64) (st : state) : @@ -337,7 +361,7 @@ Fixpoint betree_Node_apply_upserts_back match n with | O => Fail_ OutOfFuel | S n0 => - b <- betree_List_head_has_key betree_Message_t msgs key; + b <- betree_ListTupleU64T_head_has_key betree_Message_t msgs key; if b then ( msg <- betree_List_pop_front (u64 * betree_Message_t) msgs; @@ -358,7 +382,8 @@ Fixpoint betree_Node_apply_upserts_back end . -(** [betree_main::betree::Node::{5}::lookup_in_bindings]: forward function *) +(** [betree_main::betree::{betree_main::betree::Node#5}::lookup_in_bindings]: forward function + Source: 'src/betree.rs', lines 636:4-636:80 *) Fixpoint betree_Node_lookup_in_bindings (n : nat) (key : u64) (bindings : betree_List_t (u64 * u64)) : result (option u64) @@ -380,7 +405,8 @@ Fixpoint betree_Node_lookup_in_bindings end . -(** [betree_main::betree::Internal::{4}::lookup_in_children]: forward function *) +(** [betree_main::betree::{betree_main::betree::Internal#4}::lookup_in_children]: forward function + Source: 'src/betree.rs', lines 395:4-395:63 *) Fixpoint betree_Internal_lookup_in_children (n : nat) (self : betree_Internal_t) (key : u64) (st : state) : result (state * (option u64)) @@ -393,7 +419,8 @@ Fixpoint betree_Internal_lookup_in_children else betree_Node_lookup n0 self.(betree_Internal_right) key st end -(** [betree_main::betree::Internal::{4}::lookup_in_children]: backward function 0 *) +(** [betree_main::betree::{betree_main::betree::Internal#4}::lookup_in_children]: backward function 0 + Source: 'src/betree.rs', lines 395:4-395:63 *) with betree_Internal_lookup_in_children_back (n : nat) (self : betree_Internal_t) (key : u64) (st : state) : result betree_Internal_t @@ -412,7 +439,8 @@ with betree_Internal_lookup_in_children_back self.(betree_Internal_pivot) self.(betree_Internal_left) n1)) end -(** [betree_main::betree::Node::{5}::lookup]: forward function *) +(** [betree_main::betree::{betree_main::betree::Node#5}::lookup]: forward function + Source: 'src/betree.rs', lines 709:4-709:58 *) with betree_Node_lookup (n : nat) (self : betree_Node_t) (key : u64) (st : state) : result (state * (option u64)) @@ -483,7 +511,8 @@ with betree_Node_lookup end end -(** [betree_main::betree::Node::{5}::lookup]: backward function 0 *) +(** [betree_main::betree::{betree_main::betree::Node#5}::lookup]: backward function 0 + Source: 'src/betree.rs', lines 709:4-709:58 *) with betree_Node_lookup_back (n : nat) (self : betree_Node_t) (key : u64) (st : state) : result betree_Node_t @@ -552,8 +581,9 @@ with betree_Node_lookup_back end . -(** [betree_main::betree::Node::{5}::filter_messages_for_key]: merged forward/backward function - (there is a single backward function, and the forward function returns ()) *) +(** [betree_main::betree::{betree_main::betree::Node#5}::filter_messages_for_key]: merged forward/backward function + (there is a single backward function, and the forward function returns ()) + Source: 'src/betree.rs', lines 674:4-674:77 *) Fixpoint betree_Node_filter_messages_for_key (n : nat) (key : u64) (msgs : betree_List_t (u64 * betree_Message_t)) : result (betree_List_t (u64 * betree_Message_t)) @@ -576,7 +606,8 @@ Fixpoint betree_Node_filter_messages_for_key end . -(** [betree_main::betree::Node::{5}::lookup_first_message_after_key]: forward function *) +(** [betree_main::betree::{betree_main::betree::Node#5}::lookup_first_message_after_key]: forward function + Source: 'src/betree.rs', lines 689:4-692:34 *) Fixpoint betree_Node_lookup_first_message_after_key (n : nat) (key : u64) (msgs : betree_List_t (u64 * betree_Message_t)) : result (betree_List_t (u64 * betree_Message_t)) @@ -595,7 +626,8 @@ Fixpoint betree_Node_lookup_first_message_after_key end . -(** [betree_main::betree::Node::{5}::lookup_first_message_after_key]: backward function 0 *) +(** [betree_main::betree::{betree_main::betree::Node#5}::lookup_first_message_after_key]: backward function 0 + Source: 'src/betree.rs', lines 689:4-692:34 *) Fixpoint betree_Node_lookup_first_message_after_key_back (n : nat) (key : u64) (msgs : betree_List_t (u64 * betree_Message_t)) (ret : betree_List_t (u64 * betree_Message_t)) : @@ -618,15 +650,16 @@ Fixpoint betree_Node_lookup_first_message_after_key_back end . -(** [betree_main::betree::Node::{5}::apply_to_internal]: merged forward/backward function - (there is a single backward function, and the forward function returns ()) *) +(** [betree_main::betree::{betree_main::betree::Node#5}::apply_to_internal]: merged forward/backward function + (there is a single backward function, and the forward function returns ()) + Source: 'src/betree.rs', lines 521:4-521:89 *) Definition betree_Node_apply_to_internal (n : nat) (msgs : betree_List_t (u64 * betree_Message_t)) (key : u64) (new_msg : betree_Message_t) : result (betree_List_t (u64 * betree_Message_t)) := msgs0 <- betree_Node_lookup_first_message_for_key n key msgs; - b <- betree_List_head_has_key betree_Message_t msgs0 key; + b <- betree_ListTupleU64T_head_has_key betree_Message_t msgs0 key; if b then match new_msg with @@ -676,8 +709,9 @@ Definition betree_Node_apply_to_internal betree_Node_lookup_first_message_for_key_back n key msgs msgs1) . -(** [betree_main::betree::Node::{5}::apply_messages_to_internal]: merged forward/backward function - (there is a single backward function, and the forward function returns ()) *) +(** [betree_main::betree::{betree_main::betree::Node#5}::apply_messages_to_internal]: merged forward/backward function + (there is a single backward function, and the forward function returns ()) + Source: 'src/betree.rs', lines 502:4-505:5 *) Fixpoint betree_Node_apply_messages_to_internal (n : nat) (msgs : betree_List_t (u64 * betree_Message_t)) (new_msgs : betree_List_t (u64 * betree_Message_t)) : @@ -696,7 +730,8 @@ Fixpoint betree_Node_apply_messages_to_internal end . -(** [betree_main::betree::Node::{5}::lookup_mut_in_bindings]: forward function *) +(** [betree_main::betree::{betree_main::betree::Node#5}::lookup_mut_in_bindings]: forward function + Source: 'src/betree.rs', lines 653:4-656:32 *) Fixpoint betree_Node_lookup_mut_in_bindings (n : nat) (key : u64) (bindings : betree_List_t (u64 * u64)) : result (betree_List_t (u64 * u64)) @@ -715,7 +750,8 @@ Fixpoint betree_Node_lookup_mut_in_bindings end . -(** [betree_main::betree::Node::{5}::lookup_mut_in_bindings]: backward function 0 *) +(** [betree_main::betree::{betree_main::betree::Node#5}::lookup_mut_in_bindings]: backward function 0 + Source: 'src/betree.rs', lines 653:4-656:32 *) Fixpoint betree_Node_lookup_mut_in_bindings_back (n : nat) (key : u64) (bindings : betree_List_t (u64 * u64)) (ret : betree_List_t (u64 * u64)) : @@ -737,15 +773,16 @@ Fixpoint betree_Node_lookup_mut_in_bindings_back end . -(** [betree_main::betree::Node::{5}::apply_to_leaf]: merged forward/backward function - (there is a single backward function, and the forward function returns ()) *) +(** [betree_main::betree::{betree_main::betree::Node#5}::apply_to_leaf]: merged forward/backward function + (there is a single backward function, and the forward function returns ()) + Source: 'src/betree.rs', lines 460:4-460:87 *) Definition betree_Node_apply_to_leaf (n : nat) (bindings : betree_List_t (u64 * u64)) (key : u64) (new_msg : betree_Message_t) : result (betree_List_t (u64 * u64)) := bindings0 <- betree_Node_lookup_mut_in_bindings n key bindings; - b <- betree_List_head_has_key u64 bindings0 key; + b <- betree_ListTupleU64T_head_has_key u64 bindings0 key; if b then ( hd <- betree_List_pop_front (u64 * u64) bindings0; @@ -778,8 +815,9 @@ Definition betree_Node_apply_to_leaf end . -(** [betree_main::betree::Node::{5}::apply_messages_to_leaf]: merged forward/backward function - (there is a single backward function, and the forward function returns ()) *) +(** [betree_main::betree::{betree_main::betree::Node#5}::apply_messages_to_leaf]: merged forward/backward function + (there is a single backward function, and the forward function returns ()) + Source: 'src/betree.rs', lines 444:4-447:5 *) Fixpoint betree_Node_apply_messages_to_leaf (n : nat) (bindings : betree_List_t (u64 * u64)) (new_msgs : betree_List_t (u64 * betree_Message_t)) : @@ -798,7 +836,8 @@ Fixpoint betree_Node_apply_messages_to_leaf end . -(** [betree_main::betree::Internal::{4}::flush]: forward function *) +(** [betree_main::betree::{betree_main::betree::Internal#4}::flush]: forward function + Source: 'src/betree.rs', lines 410:4-415:26 *) Fixpoint betree_Internal_flush (n : nat) (self : betree_Internal_t) (params : betree_Params_t) (node_id_cnt : betree_NodeIdCounter_t) @@ -809,7 +848,7 @@ Fixpoint betree_Internal_flush | O => Fail_ OutOfFuel | S n0 => p <- - betree_List_partition_at_pivot betree_Message_t n0 content + betree_ListTupleU64T_partition_at_pivot betree_Message_t n0 content self.(betree_Internal_pivot); let (msgs_left, msgs_right) := p in len_left <- betree_List_len (u64 * betree_Message_t) n0 msgs_left; @@ -846,7 +885,8 @@ Fixpoint betree_Internal_flush Return (st0, msgs_left)) end -(** [betree_main::betree::Internal::{4}::flush]: backward function 0 *) +(** [betree_main::betree::{betree_main::betree::Internal#4}::flush]: backward function 0 + Source: 'src/betree.rs', lines 410:4-415:26 *) with betree_Internal_flush_back (n : nat) (self : betree_Internal_t) (params : betree_Params_t) (node_id_cnt : betree_NodeIdCounter_t) @@ -857,7 +897,7 @@ with betree_Internal_flush_back | O => Fail_ OutOfFuel | S n0 => p <- - betree_List_partition_at_pivot betree_Message_t n0 content + betree_ListTupleU64T_partition_at_pivot betree_Message_t n0 content self.(betree_Internal_pivot); let (msgs_left, msgs_right) := p in len_left <- betree_List_len (u64 * betree_Message_t) n0 msgs_left; @@ -894,7 +934,8 @@ with betree_Internal_flush_back node_id_cnt0)) end -(** [betree_main::betree::Node::{5}::apply_messages]: forward function *) +(** [betree_main::betree::{betree_main::betree::Node#5}::apply_messages]: forward function + Source: 'src/betree.rs', lines 588:4-593:5 *) with betree_Node_apply_messages (n : nat) (self : betree_Node_t) (params : betree_Params_t) (node_id_cnt : betree_NodeIdCounter_t) @@ -946,7 +987,8 @@ with betree_Node_apply_messages end end -(** [betree_main::betree::Node::{5}::apply_messages]: backward function 0 *) +(** [betree_main::betree::{betree_main::betree::Node#5}::apply_messages]: backward function 0 + Source: 'src/betree.rs', lines 588:4-593:5 *) with betree_Node_apply_messages_back (n : nat) (self : betree_Node_t) (params : betree_Params_t) (node_id_cnt : betree_NodeIdCounter_t) @@ -998,7 +1040,8 @@ with betree_Node_apply_messages_back end . -(** [betree_main::betree::Node::{5}::apply]: forward function *) +(** [betree_main::betree::{betree_main::betree::Node#5}::apply]: forward function + Source: 'src/betree.rs', lines 576:4-582:5 *) Definition betree_Node_apply (n : nat) (self : betree_Node_t) (params : betree_Params_t) (node_id_cnt : betree_NodeIdCounter_t) (key : u64) @@ -1016,7 +1059,8 @@ Definition betree_Node_apply Return (st0, tt) . -(** [betree_main::betree::Node::{5}::apply]: backward function 0 *) +(** [betree_main::betree::{betree_main::betree::Node#5}::apply]: backward function 0 + Source: 'src/betree.rs', lines 576:4-582:5 *) Definition betree_Node_apply_back (n : nat) (self : betree_Node_t) (params : betree_Params_t) (node_id_cnt : betree_NodeIdCounter_t) (key : u64) @@ -1028,7 +1072,8 @@ Definition betree_Node_apply_back (key, new_msg) l) st . -(** [betree_main::betree::BeTree::{6}::new]: forward function *) +(** [betree_main::betree::{betree_main::betree::BeTree#6}::new]: forward function + Source: 'src/betree.rs', lines 849:4-849:60 *) Definition betree_BeTree_new (min_flush_size : u64) (split_size : u64) (st : state) : result (state * betree_BeTree_t) @@ -1052,7 +1097,8 @@ Definition betree_BeTree_new |}) . -(** [betree_main::betree::BeTree::{6}::apply]: forward function *) +(** [betree_main::betree::{betree_main::betree::BeTree#6}::apply]: forward function + Source: 'src/betree.rs', lines 868:4-868:47 *) Definition betree_BeTree_apply (n : nat) (self : betree_BeTree_t) (key : u64) (msg : betree_Message_t) (st : state) : @@ -1068,7 +1114,8 @@ Definition betree_BeTree_apply Return (st0, tt) . -(** [betree_main::betree::BeTree::{6}::apply]: backward function 0 *) +(** [betree_main::betree::{betree_main::betree::BeTree#6}::apply]: backward function 0 + Source: 'src/betree.rs', lines 868:4-868:47 *) Definition betree_BeTree_apply_back (n : nat) (self : betree_BeTree_t) (key : u64) (msg : betree_Message_t) (st : state) : @@ -1086,7 +1133,8 @@ Definition betree_BeTree_apply_back |} . -(** [betree_main::betree::BeTree::{6}::insert]: forward function *) +(** [betree_main::betree::{betree_main::betree::BeTree#6}::insert]: forward function + Source: 'src/betree.rs', lines 874:4-874:52 *) Definition betree_BeTree_insert (n : nat) (self : betree_BeTree_t) (key : u64) (value : u64) (st : state) : result (state * unit) @@ -1097,7 +1145,8 @@ Definition betree_BeTree_insert Return (st0, tt) . -(** [betree_main::betree::BeTree::{6}::insert]: backward function 0 *) +(** [betree_main::betree::{betree_main::betree::BeTree#6}::insert]: backward function 0 + Source: 'src/betree.rs', lines 874:4-874:52 *) Definition betree_BeTree_insert_back (n : nat) (self : betree_BeTree_t) (key : u64) (value : u64) (st : state) : result betree_BeTree_t @@ -1105,7 +1154,8 @@ Definition betree_BeTree_insert_back betree_BeTree_apply_back n self key (Betree_Message_Insert value) st . -(** [betree_main::betree::BeTree::{6}::delete]: forward function *) +(** [betree_main::betree::{betree_main::betree::BeTree#6}::delete]: forward function + Source: 'src/betree.rs', lines 880:4-880:38 *) Definition betree_BeTree_delete (n : nat) (self : betree_BeTree_t) (key : u64) (st : state) : result (state * unit) @@ -1116,7 +1166,8 @@ Definition betree_BeTree_delete Return (st0, tt) . -(** [betree_main::betree::BeTree::{6}::delete]: backward function 0 *) +(** [betree_main::betree::{betree_main::betree::BeTree#6}::delete]: backward function 0 + Source: 'src/betree.rs', lines 880:4-880:38 *) Definition betree_BeTree_delete_back (n : nat) (self : betree_BeTree_t) (key : u64) (st : state) : result betree_BeTree_t @@ -1124,7 +1175,8 @@ Definition betree_BeTree_delete_back betree_BeTree_apply_back n self key Betree_Message_Delete st . -(** [betree_main::betree::BeTree::{6}::upsert]: forward function *) +(** [betree_main::betree::{betree_main::betree::BeTree#6}::upsert]: forward function + Source: 'src/betree.rs', lines 886:4-886:59 *) Definition betree_BeTree_upsert (n : nat) (self : betree_BeTree_t) (key : u64) (upd : betree_UpsertFunState_t) (st : state) : @@ -1136,7 +1188,8 @@ Definition betree_BeTree_upsert Return (st0, tt) . -(** [betree_main::betree::BeTree::{6}::upsert]: backward function 0 *) +(** [betree_main::betree::{betree_main::betree::BeTree#6}::upsert]: backward function 0 + Source: 'src/betree.rs', lines 886:4-886:59 *) Definition betree_BeTree_upsert_back (n : nat) (self : betree_BeTree_t) (key : u64) (upd : betree_UpsertFunState_t) (st : state) : @@ -1145,7 +1198,8 @@ Definition betree_BeTree_upsert_back betree_BeTree_apply_back n self key (Betree_Message_Upsert upd) st . -(** [betree_main::betree::BeTree::{6}::lookup]: forward function *) +(** [betree_main::betree::{betree_main::betree::BeTree#6}::lookup]: forward function + Source: 'src/betree.rs', lines 895:4-895:62 *) Definition betree_BeTree_lookup (n : nat) (self : betree_BeTree_t) (key : u64) (st : state) : result (state * (option u64)) @@ -1153,7 +1207,8 @@ Definition betree_BeTree_lookup betree_Node_lookup n self.(betree_BeTree_root) key st . -(** [betree_main::betree::BeTree::{6}::lookup]: backward function 0 *) +(** [betree_main::betree::{betree_main::betree::BeTree#6}::lookup]: backward function 0 + Source: 'src/betree.rs', lines 895:4-895:62 *) Definition betree_BeTree_lookup_back (n : nat) (self : betree_BeTree_t) (key : u64) (st : state) : result betree_BeTree_t @@ -1167,7 +1222,8 @@ Definition betree_BeTree_lookup_back |} . -(** [betree_main::main]: forward function *) +(** [betree_main::main]: forward function + Source: 'src/betree_main.rs', lines 5:0-5:9 *) Definition main : result unit := Return tt. diff --git a/tests/coq/betree/BetreeMain_Opaque.v b/tests/coq/betree/BetreeMain_Opaque.v index eade90de..a065c8a3 100644 --- a/tests/coq/betree/BetreeMain_Opaque.v +++ b/tests/coq/betree/BetreeMain_Opaque.v @@ -10,29 +10,34 @@ Require Export BetreeMain_Types. Import BetreeMain_Types. Module BetreeMain_Opaque. -(** [betree_main::betree_utils::load_internal_node]: forward function *) +(** [betree_main::betree_utils::load_internal_node]: forward function + Source: 'src/betree_utils.rs', lines 98:0-98:63 *) Axiom betree_utils_load_internal_node : u64 -> state -> result (state * (betree_List_t (u64 * betree_Message_t))) . -(** [betree_main::betree_utils::store_internal_node]: forward function *) +(** [betree_main::betree_utils::store_internal_node]: forward function + Source: 'src/betree_utils.rs', lines 115:0-115:71 *) Axiom betree_utils_store_internal_node : u64 -> betree_List_t (u64 * betree_Message_t) -> state -> result (state * unit) . -(** [betree_main::betree_utils::load_leaf_node]: forward function *) +(** [betree_main::betree_utils::load_leaf_node]: forward function + Source: 'src/betree_utils.rs', lines 132:0-132:55 *) Axiom betree_utils_load_leaf_node : u64 -> state -> result (state * (betree_List_t (u64 * u64))) . -(** [betree_main::betree_utils::store_leaf_node]: forward function *) +(** [betree_main::betree_utils::store_leaf_node]: forward function + Source: 'src/betree_utils.rs', lines 145:0-145:63 *) Axiom betree_utils_store_leaf_node : u64 -> betree_List_t (u64 * u64) -> state -> result (state * unit) . -(** [core::option::Option::{0}::unwrap]: forward function *) +(** [core::option::{core::option::Option<T>}::unwrap]: forward function + Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/option.rs', lines 932:4-932:34 *) Axiom core_option_Option_unwrap : forall(T : Type), option T -> state -> result (state * T) . diff --git a/tests/coq/betree/BetreeMain_Types.v b/tests/coq/betree/BetreeMain_Types.v index 933a670c..b729d1c3 100644 --- a/tests/coq/betree/BetreeMain_Types.v +++ b/tests/coq/betree/BetreeMain_Types.v @@ -8,7 +8,8 @@ Import ListNotations. Local Open Scope Primitives_scope. Module BetreeMain_Types. -(** [betree_main::betree::List] *) +(** [betree_main::betree::List] + Source: 'src/betree.rs', lines 17:0-17:23 *) Inductive betree_List_t (T : Type) := | Betree_List_Cons : T -> betree_List_t T -> betree_List_t T | Betree_List_Nil : betree_List_t T @@ -17,27 +18,31 @@ Inductive betree_List_t (T : Type) := Arguments Betree_List_Cons { _ }. Arguments Betree_List_Nil { _ }. -(** [betree_main::betree::UpsertFunState] *) +(** [betree_main::betree::UpsertFunState] + Source: 'src/betree.rs', lines 63:0-63:23 *) Inductive betree_UpsertFunState_t := | Betree_UpsertFunState_Add : u64 -> betree_UpsertFunState_t | Betree_UpsertFunState_Sub : u64 -> betree_UpsertFunState_t . -(** [betree_main::betree::Message] *) +(** [betree_main::betree::Message] + Source: 'src/betree.rs', lines 69:0-69:23 *) Inductive betree_Message_t := | Betree_Message_Insert : u64 -> betree_Message_t | Betree_Message_Delete : betree_Message_t | Betree_Message_Upsert : betree_UpsertFunState_t -> betree_Message_t . -(** [betree_main::betree::Leaf] *) +(** [betree_main::betree::Leaf] + Source: 'src/betree.rs', lines 167:0-167:11 *) Record betree_Leaf_t := mkbetree_Leaf_t { betree_Leaf_id : u64; betree_Leaf_size : u64; } . -(** [betree_main::betree::Internal] *) +(** [betree_main::betree::Internal] + Source: 'src/betree.rs', lines 156:0-156:15 *) Inductive betree_Internal_t := | mkbetree_Internal_t : u64 -> @@ -46,7 +51,8 @@ Inductive betree_Internal_t := betree_Node_t -> betree_Internal_t -(** [betree_main::betree::Node] *) +(** [betree_main::betree::Node] + Source: 'src/betree.rs', lines 179:0-179:9 *) with betree_Node_t := | Betree_Node_Internal : betree_Internal_t -> betree_Node_t | Betree_Node_Leaf : betree_Leaf_t -> betree_Node_t @@ -81,21 +87,24 @@ Notation "x1 .(betree_Internal_right)" := (betree_Internal_right x1) (at level 9) . -(** [betree_main::betree::Params] *) +(** [betree_main::betree::Params] + Source: 'src/betree.rs', lines 187:0-187:13 *) Record betree_Params_t := mkbetree_Params_t { betree_Params_min_flush_size : u64; betree_Params_split_size : u64; } . -(** [betree_main::betree::NodeIdCounter] *) +(** [betree_main::betree::NodeIdCounter] + Source: 'src/betree.rs', lines 201:0-201:20 *) Record betree_NodeIdCounter_t := mkbetree_NodeIdCounter_t { betree_NodeIdCounter_next_node_id : u64; } . -(** [betree_main::betree::BeTree] *) +(** [betree_main::betree::BeTree] + Source: 'src/betree.rs', lines 218:0-218:17 *) Record betree_BeTree_t := mkbetree_BeTree_t { betree_BeTree_params : betree_Params_t; diff --git a/tests/coq/betree/Primitives.v b/tests/coq/betree/Primitives.v index 85e38f01..83f860b6 100644 --- a/tests/coq/betree/Primitives.v +++ b/tests/coq/betree/Primitives.v @@ -467,14 +467,14 @@ Definition alloc_boxed_Box_deref_mut (T : Type) (x : T) : result T := Return x. Definition alloc_boxed_Box_deref_mut_back (T : Type) (_ : T) (x : T) : result T := Return x. (* Trait instance *) -Definition alloc_boxed_Box_coreOpsDerefInst (Self : Type) : core_ops_deref_Deref Self := {| +Definition alloc_boxed_Box_coreopsDerefInst (Self : Type) : core_ops_deref_Deref Self := {| core_ops_deref_Deref_target := Self; core_ops_deref_Deref_deref := alloc_boxed_Box_deref Self; |}. (* Trait instance *) -Definition alloc_boxed_Box_coreOpsDerefMutInst (Self : Type) : core_ops_deref_DerefMut Self := {| - core_ops_deref_DerefMut_derefInst := alloc_boxed_Box_coreOpsDerefInst Self; +Definition alloc_boxed_Box_coreopsDerefMutInst (Self : Type) : core_ops_deref_DerefMut Self := {| + core_ops_deref_DerefMut_derefInst := alloc_boxed_Box_coreopsDerefInst Self; core_ops_deref_DerefMut_deref_mut := alloc_boxed_Box_deref_mut Self; core_ops_deref_DerefMut_deref_mut_back := alloc_boxed_Box_deref_mut_back Self; |}. @@ -576,7 +576,7 @@ Definition alloc_vec_Vec_insert (T: Type) (v: alloc_vec_Vec T) (i: usize) (x: T) else Fail_ Failure). (* Helper *) -Axiom alloc_vec_Vec_index_usize : forall {T : Type} (v : alloc_vec_Vec T) (i : usize) (x : T), result T. +Axiom alloc_vec_Vec_index_usize : forall {T : Type} (v : alloc_vec_Vec T) (i : usize), result T. (* Helper *) Axiom alloc_vec_Vec_update_usize : forall {T : Type} (v : alloc_vec_Vec T) (i : usize) (x : T), result (alloc_vec_Vec T). @@ -620,18 +620,18 @@ Definition core_slice_index_Slice_index end. (* [core::slice::index::Range:::get]: forward function *) -Axiom core_slice_index_Range_get : forall (T : Type) (i : core_ops_range_Range usize) (s : slice T), result (option (slice T)). +Axiom core_slice_index_RangeUsize_get : forall (T : Type) (i : core_ops_range_Range usize) (s : slice T), result (option (slice T)). (* [core::slice::index::Range::get_mut]: forward function *) -Axiom core_slice_index_Range_get_mut : +Axiom core_slice_index_RangeUsize_get_mut : forall (T : Type), core_ops_range_Range usize -> slice T -> result (option (slice T)). (* [core::slice::index::Range::get_mut]: backward function 0 *) -Axiom core_slice_index_Range_get_mut_back : +Axiom core_slice_index_RangeUsize_get_mut_back : forall (T : Type), core_ops_range_Range usize -> slice T -> option (slice T) -> result (slice T). (* [core::slice::index::Range::get_unchecked]: forward function *) -Definition core_slice_index_Range_get_unchecked +Definition core_slice_index_RangeUsize_get_unchecked (T : Type) : core_ops_range_Range usize -> const_raw_ptr (slice T) -> result (const_raw_ptr (slice T)) := (* Don't know what the model should be - for now we always fail to make @@ -639,7 +639,7 @@ Definition core_slice_index_Range_get_unchecked fun _ _ => Fail_ Failure. (* [core::slice::index::Range::get_unchecked_mut]: forward function *) -Definition core_slice_index_Range_get_unchecked_mut +Definition core_slice_index_RangeUsize_get_unchecked_mut (T : Type) : core_ops_range_Range usize -> mut_raw_ptr (slice T) -> result (mut_raw_ptr (slice T)) := (* Don't know what the model should be - for now we always fail to make @@ -647,15 +647,15 @@ Definition core_slice_index_Range_get_unchecked_mut fun _ _ => Fail_ Failure. (* [core::slice::index::Range::index]: forward function *) -Axiom core_slice_index_Range_index : +Axiom core_slice_index_RangeUsize_index : forall (T : Type), core_ops_range_Range usize -> slice T -> result (slice T). (* [core::slice::index::Range::index_mut]: forward function *) -Axiom core_slice_index_Range_index_mut : +Axiom core_slice_index_RangeUsize_index_mut : forall (T : Type), core_ops_range_Range usize -> slice T -> result (slice T). (* [core::slice::index::Range::index_mut]: backward function 0 *) -Axiom core_slice_index_Range_index_mut_back : +Axiom core_slice_index_RangeUsize_index_mut_back : forall (T : Type), core_ops_range_Range usize -> slice T -> slice T -> result (slice T). (* [core::slice::index::[T]::index_mut]: forward function *) @@ -683,44 +683,44 @@ Axiom core_array_Array_index_mut_back : forall (T Idx : Type) (N : usize) (inst : core_ops_index_IndexMut (slice T) Idx) (a : array T N) (i : Idx) (x : inst.(core_ops_index_IndexMut_indexInst).(core_ops_index_Index_Output)), result (array T N). -(* Trait implementation: [core::slice::index::[T]] *) -Definition core_slice_index_Slice_coreopsindexIndexInst (T Idx : Type) - (inst : core_slice_index_SliceIndex Idx (slice T)) : - core_ops_index_Index (slice T) Idx := {| - core_ops_index_Index_Output := inst.(core_slice_index_SliceIndex_Output); - core_ops_index_Index_index := core_slice_index_Slice_index T Idx inst; -|}. - (* Trait implementation: [core::slice::index::private_slice_index::Range] *) -Definition core_slice_index_private_slice_index_Range_coresliceindexprivate_slice_indexSealedInst +Definition core_slice_index_private_slice_index_SealedRangeUsizeInst : core_slice_index_private_slice_index_Sealed (core_ops_range_Range usize) := tt. (* Trait implementation: [core::slice::index::Range] *) -Definition core_slice_index_Range_coresliceindexSliceIndexInst (T : Type) : +Definition core_slice_index_SliceIndexRangeUsizeSliceTInst (T : Type) : core_slice_index_SliceIndex (core_ops_range_Range usize) (slice T) := {| - core_slice_index_SliceIndex_sealedInst := core_slice_index_private_slice_index_Range_coresliceindexprivate_slice_indexSealedInst; + core_slice_index_SliceIndex_sealedInst := core_slice_index_private_slice_index_SealedRangeUsizeInst; core_slice_index_SliceIndex_Output := slice T; - core_slice_index_SliceIndex_get := core_slice_index_Range_get T; - core_slice_index_SliceIndex_get_mut := core_slice_index_Range_get_mut T; - core_slice_index_SliceIndex_get_mut_back := core_slice_index_Range_get_mut_back T; - core_slice_index_SliceIndex_get_unchecked := core_slice_index_Range_get_unchecked T; - core_slice_index_SliceIndex_get_unchecked_mut := core_slice_index_Range_get_unchecked_mut T; - core_slice_index_SliceIndex_index := core_slice_index_Range_index T; - core_slice_index_SliceIndex_index_mut := core_slice_index_Range_index_mut T; - core_slice_index_SliceIndex_index_mut_back := core_slice_index_Range_index_mut_back T; + core_slice_index_SliceIndex_get := core_slice_index_RangeUsize_get T; + core_slice_index_SliceIndex_get_mut := core_slice_index_RangeUsize_get_mut T; + core_slice_index_SliceIndex_get_mut_back := core_slice_index_RangeUsize_get_mut_back T; + core_slice_index_SliceIndex_get_unchecked := core_slice_index_RangeUsize_get_unchecked T; + core_slice_index_SliceIndex_get_unchecked_mut := core_slice_index_RangeUsize_get_unchecked_mut T; + core_slice_index_SliceIndex_index := core_slice_index_RangeUsize_index T; + core_slice_index_SliceIndex_index_mut := core_slice_index_RangeUsize_index_mut T; + core_slice_index_SliceIndex_index_mut_back := core_slice_index_RangeUsize_index_mut_back T; +|}. + +(* Trait implementation: [core::slice::index::[T]] *) +Definition core_ops_index_IndexSliceTIInst (T Idx : Type) + (inst : core_slice_index_SliceIndex Idx (slice T)) : + core_ops_index_Index (slice T) Idx := {| + core_ops_index_Index_Output := inst.(core_slice_index_SliceIndex_Output); + core_ops_index_Index_index := core_slice_index_Slice_index T Idx inst; |}. (* Trait implementation: [core::slice::index::[T]] *) -Definition core_slice_index_Slice_coreopsindexIndexMutInst (T Idx : Type) +Definition core_ops_index_IndexMutSliceTIInst (T Idx : Type) (inst : core_slice_index_SliceIndex Idx (slice T)) : core_ops_index_IndexMut (slice T) Idx := {| - core_ops_index_IndexMut_indexInst := core_slice_index_Slice_coreopsindexIndexInst T Idx inst; + core_ops_index_IndexMut_indexInst := core_ops_index_IndexSliceTIInst T Idx inst; core_ops_index_IndexMut_index_mut := core_slice_index_Slice_index_mut T Idx inst; core_ops_index_IndexMut_index_mut_back := core_slice_index_Slice_index_mut_back T Idx inst; |}. (* Trait implementation: [core::array::[T; N]] *) -Definition core_array_Array_coreopsindexIndexInst (T Idx : Type) (N : usize) +Definition core_ops_index_IndexArrayInst (T Idx : Type) (N : usize) (inst : core_ops_index_Index (slice T) Idx) : core_ops_index_Index (array T N) Idx := {| core_ops_index_Index_Output := inst.(core_ops_index_Index_Output); @@ -728,10 +728,10 @@ Definition core_array_Array_coreopsindexIndexInst (T Idx : Type) (N : usize) |}. (* Trait implementation: [core::array::[T; N]] *) -Definition core_array_Array_coreopsindexIndexMutInst (T Idx : Type) (N : usize) +Definition core_ops_index_IndexMutArrayInst (T Idx : Type) (N : usize) (inst : core_ops_index_IndexMut (slice T) Idx) : core_ops_index_IndexMut (array T N) Idx := {| - core_ops_index_IndexMut_indexInst := core_array_Array_coreopsindexIndexInst T Idx N inst.(core_ops_index_IndexMut_indexInst); + core_ops_index_IndexMut_indexInst := core_ops_index_IndexArrayInst T Idx N inst.(core_ops_index_IndexMut_indexInst); core_ops_index_IndexMut_index_mut := core_array_Array_index_mut T Idx N inst; core_ops_index_IndexMut_index_mut_back := core_array_Array_index_mut_back T Idx N inst; |}. @@ -765,13 +765,13 @@ Axiom core_slice_index_usize_index_mut_back : forall (T : Type), usize -> slice T -> T -> result (slice T). (* Trait implementation: [core::slice::index::private_slice_index::usize] *) -Definition core_slice_index_private_slice_index_usize_coresliceindexprivate_slice_indexSealedInst +Definition core_slice_index_private_slice_index_SealedUsizeInst : core_slice_index_private_slice_index_Sealed usize := tt. (* Trait implementation: [core::slice::index::usize] *) -Definition core_slice_index_usize_coresliceindexSliceIndexInst (T : Type) : +Definition core_slice_index_SliceIndexUsizeSliceTInst (T : Type) : core_slice_index_SliceIndex usize (slice T) := {| - core_slice_index_SliceIndex_sealedInst := core_slice_index_private_slice_index_usize_coresliceindexprivate_slice_indexSealedInst; + core_slice_index_SliceIndex_sealedInst := core_slice_index_private_slice_index_SealedUsizeInst; core_slice_index_SliceIndex_Output := T; core_slice_index_SliceIndex_get := core_slice_index_usize_get T; core_slice_index_SliceIndex_get_mut := core_slice_index_usize_get_mut T; @@ -815,8 +815,16 @@ Definition alloc_vec_Vec_coreopsindexIndexMutInst (T Idx : Type) (*** Theorems *) +Axiom alloc_vec_Vec_index_eq : forall {a : Type} (v : alloc_vec_Vec a) (i : usize) (x : a), + alloc_vec_Vec_index a usize (core_slice_index_SliceIndexUsizeSliceTInst a) v i = + alloc_vec_Vec_index_usize v i. + +Axiom alloc_vec_Vec_index_mut_eq : forall {a : Type} (v : alloc_vec_Vec a) (i : usize) (x : a), + alloc_vec_Vec_index_mut a usize (core_slice_index_SliceIndexUsizeSliceTInst a) v i = + alloc_vec_Vec_index_usize v i. + Axiom alloc_vec_Vec_index_mut_back_eq : forall {a : Type} (v : alloc_vec_Vec a) (i : usize) (x : a), - alloc_vec_Vec_index_mut_back a usize (core_slice_index_usize_coresliceindexSliceIndexInst a) v i x = + alloc_vec_Vec_index_mut_back a usize (core_slice_index_SliceIndexUsizeSliceTInst a) v i x = alloc_vec_Vec_update_usize v i x. End Primitives. |