diff options
Diffstat (limited to '')
| -rw-r--r-- | Makefile | 12 | ||||
| -rw-r--r-- | compiler/Extract.ml | 29 | ||||
| -rw-r--r-- | tests/coq/betree/BetreeMain__Funs.v | 1394 | ||||
| -rw-r--r-- | tests/coq/betree/BetreeMain__Opaque.v | 38 | ||||
| -rw-r--r-- | tests/coq/betree/BetreeMain__Types.v | 117 | ||||
| -rw-r--r-- | tests/coq/betree/Makefile | 22 | ||||
| -rw-r--r-- | tests/coq/betree/Primitives.v | 482 | ||||
| -rw-r--r-- | tests/coq/betree/_CoqProject | 9 | ||||
| -rw-r--r-- | tests/coq/misc/PoloniusList.v | 41 | ||||
| -rw-r--r-- | tests/coq/misc/_CoqProject | 3 |
10 files changed, 2132 insertions, 15 deletions
@@ -130,10 +130,12 @@ tcoq-hashmap_main: OPTIONS += -use-fuel transp-polonius_list: OPTIONS += -test-units -test-trans-units -no-split-files -no-state transp-polonius_list: SUBDIR:=misc tfstarp-polonius_list: OPTIONS += +tcoqp-polonius_list: OPTIONS += trans-constants: OPTIONS += -test-units -test-trans-units -no-split-files -no-state trans-constants: SUBDIR:=misc tfstar-constants: OPTIONS += +tcoq-constants: OPTIONS += trans-external: OPTIONS += trans-external: SUBDIR:=misc @@ -143,6 +145,7 @@ BETREE_FSTAR_OPTIONS = -decreases-clauses -template-clauses transp-betree_main: OPTIONS += -backward-no-state-update transp-betree_main: SUBDIR:=betree tfstarp-betree_main: OPTIONS += $(BETREE_FSTAR_OPTIONS) +tcoqp-betree_main: OPTIONS += -use-fuel # Additional test on the betree: translate it without `-backward-no-state-update`. # This generates very ugly code, but is good to test the translation. @@ -184,7 +187,7 @@ trans-%: gen-llbc-% tfstar-% tcoq-% .PHONY: transp-% transp-%: CHARON_TEST_DIR = $(CHARON_TESTS_POLONIUS_DIR) transp-%: FILE = $* -transp-%: gen-llbcp-% tfstarp-% +transp-%: gen-llbcp-% tfstarp-% tcoqp-% echo "# Test $* done" .PHONY: tfstar-% @@ -206,6 +209,13 @@ tcoq-%: BACKEND_SUBDIR := coq tcoq-%: $(AENEAS_CMD) +# "p" stands for "Polonius" +.PHONY: tcoqp-% +tcoqp-%: OPTIONS += -backend coq +tcoqp-%: BACKEND_SUBDIR := coq +tcoqp-%: + $(AENEAS_CMD) + # Nix .PHONY: nix nix: diff --git a/compiler/Extract.ml b/compiler/Extract.ml index 6cd1462e..950e4026 100644 --- a/compiler/Extract.ml +++ b/compiler/Extract.ml @@ -674,23 +674,26 @@ let extract_type_decl_variant (ctx : extraction_ctx) (fmt : F.formatter) extraction_ctx = (* Open the field box *) F.pp_open_box fmt ctx.indent_incr; - (* Print the field names + (* Print the field names, if the backend accepts it. * [ x :] * Note that when printing fields, we register the field names as * *variables*: they don't need to be unique at the top level. *) let ctx = - match f.field_name with - | None -> ctx - | Some field_name -> - let var_id = VarId.of_int (FieldId.to_int fid) in - let field_name = - ctx.fmt.var_basename ctx.names_map.names_set (Some field_name) - f.field_ty - in - let ctx, field_name = ctx_add_var field_name var_id ctx in - F.pp_print_string fmt (field_name ^ " :"); - F.pp_print_space fmt (); - ctx + match !backend with + | FStar -> ( + match f.field_name with + | None -> ctx + | Some field_name -> + let var_id = VarId.of_int (FieldId.to_int fid) in + let field_name = + ctx.fmt.var_basename ctx.names_map.names_set (Some field_name) + f.field_ty + in + let ctx, field_name = ctx_add_var field_name var_id ctx in + F.pp_print_string fmt (field_name ^ " :"); + F.pp_print_space fmt (); + ctx) + | Coq -> ctx in (* Print the field type *) extract_ty ctx fmt false f.field_ty; diff --git a/tests/coq/betree/BetreeMain__Funs.v b/tests/coq/betree/BetreeMain__Funs.v new file mode 100644 index 00000000..a8bb9b74 --- /dev/null +++ b/tests/coq/betree/BetreeMain__Funs.v @@ -0,0 +1,1394 @@ +(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *) +(** [betree_main]: function definitions *) +Require Import Primitives. +Import Primitives. +Require Import Coq.ZArith.ZArith. +Local Open Scope Primitives_scope. +Require Export BetreeMain__Types . +Import BetreeMain__Types . +Require Export BetreeMain__Opaque . +Import BetreeMain__Opaque . +Module BetreeMain__Funs . + +(** [betree_main::betree::load_internal_node] *) +Definition betree_load_internal_node_fwd + (id : u64) (st : state) : + result (state * (Betree_list_t (u64 * Betree_message_t))) + := + p <- betree_utils_load_internal_node_fwd id st; + let (st0, l) := p in + Return (st0, l) + . + +(** [betree_main::betree::store_internal_node] *) +Definition betree_store_internal_node_fwd + (id : u64) (content : Betree_list_t (u64 * Betree_message_t)) (st : state) : + result (state * unit) + := + p <- betree_utils_store_internal_node_fwd id content st; + let (st0, _) := p in + Return (st0, tt) + . + +(** [betree_main::betree::load_leaf_node] *) +Definition betree_load_leaf_node_fwd + (id : u64) (st : state) : result (state * (Betree_list_t (u64 * u64))) := + p <- betree_utils_load_leaf_node_fwd id st; + let (st0, l) := p in + Return (st0, l) + . + +(** [betree_main::betree::store_leaf_node] *) +Definition betree_store_leaf_node_fwd + (id : u64) (content : Betree_list_t (u64 * u64)) (st : state) : + result (state * unit) + := + p <- betree_utils_store_leaf_node_fwd id content st; + let (st0, _) := p in + Return (st0, tt) + . + +(** [betree_main::betree::fresh_node_id] *) +Definition betree_fresh_node_id_fwd (counter : u64) : result u64 := + i <- u64_add counter 1 %u64; let _ := i in Return counter . + +(** [betree_main::betree::fresh_node_id] *) +Definition betree_fresh_node_id_back (counter : u64) : result u64 := + counter0 <- u64_add counter 1 %u64; Return counter0 . + +(** [betree_main::betree::NodeIdCounter::{0}::new] *) +Definition betree_node_id_counter_new_fwd : result Betree_node_id_counter_t := + Return (mkBetree_node_id_counter_t (0 %u64)) . + +(** [betree_main::betree::NodeIdCounter::{0}::fresh_id] *) +Definition betree_node_id_counter_fresh_id_fwd + (self : Betree_node_id_counter_t) : result u64 := + match self with + | mkBetree_node_id_counter_t id => + i <- u64_add id 1 %u64; let _ := i in Return id + end + . + +(** [betree_main::betree::NodeIdCounter::{0}::fresh_id] *) +Definition betree_node_id_counter_fresh_id_back + (self : Betree_node_id_counter_t) : result Betree_node_id_counter_t := + match self with + | mkBetree_node_id_counter_t id => + i <- u64_add id 1 %u64; Return (mkBetree_node_id_counter_t i) + end + . + +(** [core::num::u64::{10}::MAX] *) +Definition core_num_u64_max_body : result u64 := + Return (18446744073709551615 %u64) + . +Definition core_num_u64_max_c : u64 := core_num_u64_max_body%global . + +(** [betree_main::betree::upsert_update] *) +Definition betree_upsert_update_fwd + (prev : option u64) (st : Betree_upsert_fun_state_t) : result u64 := + match prev with + | None => + match st with + | BetreeUpsertFunStateAdd v => Return v + | BetreeUpsertFunStateSub i => Return (0 %u64) + end + | Some prev0 => + match st with + | BetreeUpsertFunStateAdd v => + margin <- u64_sub core_num_u64_max_c prev0; + if margin s>= v + then (i <- u64_add prev0 v; Return i) + else Return core_num_u64_max_c + | BetreeUpsertFunStateSub v => + if prev0 s>= v then (i <- u64_sub prev0 v; Return i) else Return (0 %u64) + end + end + . + +(** [betree_main::betree::List::{1}::len] *) +Fixpoint betree_list_len_fwd + (T : Type) (n : nat) (self : Betree_list_t T) : result u64 := + match n with + | O => Fail_ OutOfFuel + | S n0 => + match self with + | BetreeListCons t tl => + i <- betree_list_len_fwd T n0 tl; i0 <- u64_add 1 %u64 i; Return i0 + | BetreeListNil => Return (0 %u64) + end + end + . + +(** [betree_main::betree::List::{1}::split_at] *) +Fixpoint betree_list_split_at_fwd + (T : Type) (n : nat) (self : Betree_list_t T) (n0 : u64) : + result ((Betree_list_t T) * (Betree_list_t T)) + := + match n with + | O => Fail_ OutOfFuel + | S n1 => + if n0 s= 0 %u64 + then Return (BetreeListNil, self) + else + match self with + | BetreeListCons hd tl => + i <- u64_sub n0 1 %u64; + p <- betree_list_split_at_fwd T n1 tl i; + let (ls0, ls1) := p in + let l := ls0 in + Return (BetreeListCons hd l, ls1) + | BetreeListNil => Fail_ Failure + end + end + . + +(** [betree_main::betree::List::{1}::push_front] *) +Definition betree_list_push_front_fwd_back + (T : Type) (self : Betree_list_t T) (x : T) : result (Betree_list_t T) := + let tl := mem_replace_fwd (Betree_list_t T) self BetreeListNil in + let l := tl in + Return (BetreeListCons x l) + . + +(** [betree_main::betree::List::{1}::pop_front] *) +Definition betree_list_pop_front_fwd + (T : Type) (self : Betree_list_t T) : result T := + let ls := mem_replace_fwd (Betree_list_t T) self BetreeListNil in + match ls with + | BetreeListCons x tl => Return x + | BetreeListNil => Fail_ Failure + end + . + +(** [betree_main::betree::List::{1}::pop_front] *) +Definition betree_list_pop_front_back + (T : Type) (self : Betree_list_t T) : result (Betree_list_t T) := + let ls := mem_replace_fwd (Betree_list_t T) self BetreeListNil in + match ls with + | BetreeListCons x tl => Return tl + | BetreeListNil => Fail_ Failure + end + . + +(** [betree_main::betree::List::{1}::hd] *) +Definition betree_list_hd_fwd (T : Type) (self : Betree_list_t T) : result T := + match self with + | BetreeListCons hd l => Return hd + | BetreeListNil => Fail_ Failure + end + . + +(** [betree_main::betree::List::{2}::head_has_key] *) +Definition betree_list_head_has_key_fwd + (T : Type) (self : Betree_list_t (u64 * T)) (key : u64) : result bool := + match self with + | BetreeListCons hd l => let (i, _) := hd in Return (i s= key) + | BetreeListNil => Return false + end + . + +(** [betree_main::betree::List::{2}::partition_at_pivot] *) +Fixpoint betree_list_partition_at_pivot_fwd + (T : Type) (n : nat) (self : Betree_list_t (u64 * T)) (pivot : u64) : + result ((Betree_list_t (u64 * T)) * (Betree_list_t (u64 * T))) + := + match n with + | O => Fail_ OutOfFuel + | S n0 => + match self with + | BetreeListCons hd tl => + let (i, t) := hd in + if i s>= pivot + then Return (BetreeListNil, BetreeListCons (i, t) tl) + else ( + p <- betree_list_partition_at_pivot_fwd T n0 tl pivot; + let (ls0, ls1) := p in + let l := ls0 in + Return (BetreeListCons (i, t) l, ls1)) + | BetreeListNil => Return (BetreeListNil, BetreeListNil) + end + end + . + +(** [betree_main::betree::Leaf::{3}::split] *) +Definition betree_leaf_split_fwd + (n : nat) (self : Betree_leaf_t) (content : Betree_list_t (u64 * u64)) + (params : Betree_params_t) (node_id_cnt : Betree_node_id_counter_t) + (st : state) : + result (state * Betree_internal_t) + := + match n with + | O => Fail_ OutOfFuel + | S n0 => + match params with + | mkBetree_params_t i i0 => + p <- betree_list_split_at_fwd (u64 * u64) n0 content i0; + let (content0, content1) := p in + p0 <- betree_list_hd_fwd (u64 * u64) content1; + let (pivot, _) := p0 in + id0 <- betree_node_id_counter_fresh_id_fwd node_id_cnt; + node_id_cnt0 <- betree_node_id_counter_fresh_id_back node_id_cnt; + id1 <- betree_node_id_counter_fresh_id_fwd node_id_cnt0; + p1 <- betree_store_leaf_node_fwd id0 content0 st; + let (st0, _) := p1 in + p2 <- betree_store_leaf_node_fwd id1 content1 st0; + let (st1, _) := p2 in + match self with + | mkBetree_leaf_t i1 i2 => + let n1 := BetreeNodeLeaf (mkBetree_leaf_t id0 i0) in + let n2 := BetreeNodeLeaf (mkBetree_leaf_t id1 i0) in + Return (st1, mkBetree_internal_t i1 pivot n1 n2) + end + end + end + . + +(** [betree_main::betree::Leaf::{3}::split] *) +Definition betree_leaf_split_back + (n : nat) (self : Betree_leaf_t) (content : Betree_list_t (u64 * u64)) + (params : Betree_params_t) (node_id_cnt : Betree_node_id_counter_t) + (st : state) : + result Betree_node_id_counter_t + := + match n with + | O => Fail_ OutOfFuel + | S n0 => + match params with + | mkBetree_params_t i i0 => + p <- betree_list_split_at_fwd (u64 * u64) n0 content i0; + let (content0, content1) := p in + p0 <- betree_list_hd_fwd (u64 * u64) content1; + let _ := p0 in + id0 <- betree_node_id_counter_fresh_id_fwd node_id_cnt; + node_id_cnt0 <- betree_node_id_counter_fresh_id_back node_id_cnt; + id1 <- betree_node_id_counter_fresh_id_fwd node_id_cnt0; + p1 <- betree_store_leaf_node_fwd id0 content0 st; + let (st0, _) := p1 in + p2 <- betree_store_leaf_node_fwd id1 content1 st0; + let (_, _) := p2 in + match self with + | mkBetree_leaf_t i1 i2 => + node_id_cnt1 <- betree_node_id_counter_fresh_id_back node_id_cnt0; + Return node_id_cnt1 + end + end + end + . + +(** [betree_main::betree::Node::{5}::lookup_in_bindings] *) +Fixpoint betree_node_lookup_in_bindings_fwd + (n : nat) (key : u64) (bindings : Betree_list_t (u64 * u64)) : + result (option u64) + := + match n with + | O => Fail_ OutOfFuel + | S n0 => + match bindings with + | BetreeListCons hd tl => + let (i, i0) := hd in + if i s= key + then Return (Some i0) + else + if i s> key + then Return None + else (opt <- betree_node_lookup_in_bindings_fwd n0 key tl; Return opt) + | BetreeListNil => Return None + end + end + . + +(** [betree_main::betree::Node::{5}::lookup_first_message_for_key] *) +Fixpoint betree_node_lookup_first_message_for_key_fwd + (n : nat) (key : u64) (msgs : Betree_list_t (u64 * Betree_message_t)) : + result (Betree_list_t (u64 * Betree_message_t)) + := + match n with + | O => Fail_ OutOfFuel + | S n0 => + match msgs with + | BetreeListCons x next_msgs => + let (i, m) := x in + if i s>= key + then Return (BetreeListCons (i, m) next_msgs) + else ( + l <- betree_node_lookup_first_message_for_key_fwd n0 key next_msgs; + Return l) + | BetreeListNil => Return BetreeListNil + end + end + . + +(** [betree_main::betree::Node::{5}::lookup_first_message_for_key] *) +Fixpoint betree_node_lookup_first_message_for_key_back + (n : nat) (key : u64) (msgs : Betree_list_t (u64 * Betree_message_t)) + (ret : Betree_list_t (u64 * Betree_message_t)) : + result (Betree_list_t (u64 * Betree_message_t)) + := + match n with + | O => Fail_ OutOfFuel + | S n0 => + match msgs with + | BetreeListCons x next_msgs => + let (i, m) := x in + if i s>= key + then Return ret + else ( + next_msgs0 <- + betree_node_lookup_first_message_for_key_back n0 key next_msgs ret; + Return (BetreeListCons (i, m) next_msgs0)) + | BetreeListNil => Return ret + end + end + . + +(** [betree_main::betree::Node::{5}::apply_upserts] *) +Fixpoint betree_node_apply_upserts_fwd + (n : nat) (msgs : Betree_list_t (u64 * Betree_message_t)) (prev : option u64) + (key : u64) (st : state) : + result (state * u64) + := + match n with + | O => Fail_ OutOfFuel + | S n0 => + b <- betree_list_head_has_key_fwd Betree_message_t msgs key; + if b + then ( + msg <- betree_list_pop_front_fwd (u64 * Betree_message_t) msgs; + let (_, m) := msg in + match m with + | BetreeMessageInsert i => Fail_ Failure + | BetreeMessageDelete => Fail_ Failure + | BetreeMessageUpsert s => + v <- betree_upsert_update_fwd prev s; + msgs0 <- betree_list_pop_front_back (u64 * Betree_message_t) msgs; + p <- betree_node_apply_upserts_fwd n0 msgs0 (Some v) key st; + let (st0, i) := p in + Return (st0, i) + end) + else ( + p <- core_option_option_unwrap_fwd u64 prev st; + let (st0, v) := p in + l <- + betree_list_push_front_fwd_back (u64 * Betree_message_t) msgs (key, + BetreeMessageInsert v); + let _ := l in + Return (st0, v)) + end + . + +(** [betree_main::betree::Node::{5}::apply_upserts] *) +Fixpoint betree_node_apply_upserts_back + (n : nat) (msgs : Betree_list_t (u64 * Betree_message_t)) (prev : option u64) + (key : u64) (st : state) : + result (Betree_list_t (u64 * Betree_message_t)) + := + match n with + | O => Fail_ OutOfFuel + | S n0 => + b <- betree_list_head_has_key_fwd Betree_message_t msgs key; + if b + then ( + msg <- betree_list_pop_front_fwd (u64 * Betree_message_t) msgs; + let (_, m) := msg in + match m with + | BetreeMessageInsert i => Fail_ Failure + | BetreeMessageDelete => Fail_ Failure + | BetreeMessageUpsert s => + v <- betree_upsert_update_fwd prev s; + msgs0 <- betree_list_pop_front_back (u64 * Betree_message_t) msgs; + msgs1 <- betree_node_apply_upserts_back n0 msgs0 (Some v) key st; + Return msgs1 + end) + else ( + p <- core_option_option_unwrap_fwd u64 prev st; + let (_, v) := p in + msgs0 <- + betree_list_push_front_fwd_back (u64 * Betree_message_t) msgs (key, + BetreeMessageInsert v); + Return msgs0) + end + . + +(** [betree_main::betree::Node::{5}::lookup] *) +Fixpoint betree_node_lookup_fwd + (n : nat) (self : Betree_node_t) (key : u64) (st : state) : + result (state * (option u64)) + := + match n with + | O => Fail_ OutOfFuel + | S n0 => + match self with + | BetreeNodeInternal node => + match node with + | mkBetree_internal_t i i0 n1 n2 => + p <- betree_load_internal_node_fwd i st; + let (st0, msgs) := p in + pending <- betree_node_lookup_first_message_for_key_fwd n0 key msgs; + match pending with + | BetreeListCons p0 l => + let (k, msg) := p0 in + if k s<> key + then ( + p1 <- + betree_internal_lookup_in_children_fwd n0 (mkBetree_internal_t i + i0 n1 n2) key st0; + let (st1, opt) := p1 in + l0 <- + betree_node_lookup_first_message_for_key_back n0 key msgs + (BetreeListCons (k, msg) l); + let _ := l0 in + Return (st1, opt)) + else + match msg with + | BetreeMessageInsert v => + l0 <- + betree_node_lookup_first_message_for_key_back n0 key msgs + (BetreeListCons (k, BetreeMessageInsert v) l); + let _ := l0 in + Return (st0, Some v) + | BetreeMessageDelete => + l0 <- + betree_node_lookup_first_message_for_key_back n0 key msgs + (BetreeListCons (k, BetreeMessageDelete) l); + let _ := l0 in + Return (st0, None) + | BetreeMessageUpsert ufs => + p1 <- + betree_internal_lookup_in_children_fwd n0 (mkBetree_internal_t + i i0 n1 n2) key st0; + let (st1, v) := p1 in + p2 <- + betree_node_apply_upserts_fwd n0 (BetreeListCons (k, + BetreeMessageUpsert ufs) l) v key st1; + let (st2, v0) := p2 in + node0 <- + betree_internal_lookup_in_children_back n0 (mkBetree_internal_t + i i0 n1 n2) key st0; + match node0 with + | mkBetree_internal_t i1 i2 n3 n4 => + pending0 <- + betree_node_apply_upserts_back n0 (BetreeListCons (k, + BetreeMessageUpsert ufs) l) v key st1; + msgs0 <- + betree_node_lookup_first_message_for_key_back n0 key msgs + pending0; + p3 <- betree_store_internal_node_fwd i1 msgs0 st2; + let (st3, _) := p3 in + Return (st3, Some v0) + end + end + | BetreeListNil => + p0 <- + betree_internal_lookup_in_children_fwd n0 (mkBetree_internal_t i i0 + n1 n2) key st0; + let (st1, opt) := p0 in + l <- + betree_node_lookup_first_message_for_key_back n0 key msgs + BetreeListNil; + let _ := l in + Return (st1, opt) + end + end + | BetreeNodeLeaf node => + match node with + | mkBetree_leaf_t i i0 => + p <- betree_load_leaf_node_fwd i st; + let (st0, bindings) := p in + opt <- betree_node_lookup_in_bindings_fwd n0 key bindings; + Return (st0, opt) + end + end + end + +(** [betree_main::betree::Node::{5}::lookup] *) +with betree_node_lookup_back + (n : nat) (self : Betree_node_t) (key : u64) (st : state) : + result Betree_node_t + := + match n with + | O => Fail_ OutOfFuel + | S n0 => + match self with + | BetreeNodeInternal node => + match node with + | mkBetree_internal_t i i0 n1 n2 => + p <- betree_load_internal_node_fwd i st; + let (st0, msgs) := p in + pending <- betree_node_lookup_first_message_for_key_fwd n0 key msgs; + match pending with + | BetreeListCons p0 l => + let (k, msg) := p0 in + if k s<> key + then ( + l0 <- + betree_node_lookup_first_message_for_key_back n0 key msgs + (BetreeListCons (k, msg) l); + let _ := l0 in + node0 <- + betree_internal_lookup_in_children_back n0 (mkBetree_internal_t i + i0 n1 n2) key st0; + Return (BetreeNodeInternal node0)) + else + match msg with + | BetreeMessageInsert v => + l0 <- + betree_node_lookup_first_message_for_key_back n0 key msgs + (BetreeListCons (k, BetreeMessageInsert v) l); + let _ := l0 in + Return (BetreeNodeInternal (mkBetree_internal_t i i0 n1 n2)) + | BetreeMessageDelete => + l0 <- + betree_node_lookup_first_message_for_key_back n0 key msgs + (BetreeListCons (k, BetreeMessageDelete) l); + let _ := l0 in + Return (BetreeNodeInternal (mkBetree_internal_t i i0 n1 n2)) + | BetreeMessageUpsert ufs => + p1 <- + betree_internal_lookup_in_children_fwd n0 (mkBetree_internal_t + i i0 n1 n2) key st0; + let (st1, v) := p1 in + p2 <- + betree_node_apply_upserts_fwd n0 (BetreeListCons (k, + BetreeMessageUpsert ufs) l) v key st1; + let (st2, _) := p2 in + node0 <- + betree_internal_lookup_in_children_back n0 (mkBetree_internal_t + i i0 n1 n2) key st0; + match node0 with + | mkBetree_internal_t i1 i2 n3 n4 => + pending0 <- + betree_node_apply_upserts_back n0 (BetreeListCons (k, + BetreeMessageUpsert ufs) l) v key st1; + msgs0 <- + betree_node_lookup_first_message_for_key_back n0 key msgs + pending0; + p3 <- betree_store_internal_node_fwd i1 msgs0 st2; + let (_, _) := p3 in + Return (BetreeNodeInternal (mkBetree_internal_t i1 i2 n3 n4)) + end + end + | BetreeListNil => + l <- + betree_node_lookup_first_message_for_key_back n0 key msgs + BetreeListNil; + let _ := l in + node0 <- + betree_internal_lookup_in_children_back n0 (mkBetree_internal_t i + i0 n1 n2) key st0; + Return (BetreeNodeInternal node0) + end + end + | BetreeNodeLeaf node => + match node with + | mkBetree_leaf_t i i0 => + p <- betree_load_leaf_node_fwd i st; + let (_, bindings) := p in + opt <- betree_node_lookup_in_bindings_fwd n0 key bindings; + let _ := opt in + Return (BetreeNodeLeaf (mkBetree_leaf_t i i0)) + end + end + end + +(** [betree_main::betree::Internal::{4}::lookup_in_children] *) +with betree_internal_lookup_in_children_fwd + (n : nat) (self : Betree_internal_t) (key : u64) (st : state) : + result (state * (option u64)) + := + match n with + | O => Fail_ OutOfFuel + | S n0 => + match self with + | mkBetree_internal_t i i0 n1 n2 => + if key s< i0 + then ( + p <- betree_node_lookup_fwd n0 n1 key st; + let (st0, opt) := p in + Return (st0, opt)) + else ( + p <- betree_node_lookup_fwd n0 n2 key st; + let (st0, opt) := p in + Return (st0, opt)) + end + end + +(** [betree_main::betree::Internal::{4}::lookup_in_children] *) +with betree_internal_lookup_in_children_back + (n : nat) (self : Betree_internal_t) (key : u64) (st : state) : + result Betree_internal_t + := + match n with + | O => Fail_ OutOfFuel + | S n0 => + match self with + | mkBetree_internal_t i i0 n1 n2 => + if key s< i0 + then ( + n3 <- betree_node_lookup_back n0 n1 key st; + Return (mkBetree_internal_t i i0 n3 n2)) + else ( + n3 <- betree_node_lookup_back n0 n2 key st; + Return (mkBetree_internal_t i i0 n1 n3)) + end + end + . + +(** [betree_main::betree::Node::{5}::lookup_mut_in_bindings] *) +Fixpoint betree_node_lookup_mut_in_bindings_fwd + (n : nat) (key : u64) (bindings : Betree_list_t (u64 * u64)) : + result (Betree_list_t (u64 * u64)) + := + match n with + | O => Fail_ OutOfFuel + | S n0 => + match bindings with + | BetreeListCons hd tl => + let (i, i0) := hd in + if i s>= key + then Return (BetreeListCons (i, i0) tl) + else (l <- betree_node_lookup_mut_in_bindings_fwd n0 key tl; Return l) + | BetreeListNil => Return BetreeListNil + end + end + . + +(** [betree_main::betree::Node::{5}::lookup_mut_in_bindings] *) +Fixpoint betree_node_lookup_mut_in_bindings_back + (n : nat) (key : u64) (bindings : Betree_list_t (u64 * u64)) + (ret : Betree_list_t (u64 * u64)) : + result (Betree_list_t (u64 * u64)) + := + match n with + | O => Fail_ OutOfFuel + | S n0 => + match bindings with + | BetreeListCons hd tl => + let (i, i0) := hd in + if i s>= key + then Return ret + else ( + tl0 <- betree_node_lookup_mut_in_bindings_back n0 key tl ret; + Return (BetreeListCons (i, i0) tl0)) + | BetreeListNil => Return ret + end + end + . + +(** [betree_main::betree::Node::{5}::apply_to_leaf] *) +Definition betree_node_apply_to_leaf_fwd_back + (n : nat) (bindings : Betree_list_t (u64 * u64)) (key : u64) + (new_msg : Betree_message_t) : + result (Betree_list_t (u64 * u64)) + := + match n with + | O => Fail_ OutOfFuel + | S n0 => + bindings0 <- betree_node_lookup_mut_in_bindings_fwd n0 key bindings; + b <- betree_list_head_has_key_fwd u64 bindings0 key; + if b + then ( + hd <- betree_list_pop_front_fwd (u64 * u64) bindings0; + match new_msg with + | BetreeMessageInsert v => + bindings1 <- betree_list_pop_front_back (u64 * u64) bindings0; + bindings2 <- + betree_list_push_front_fwd_back (u64 * u64) bindings1 (key, v); + bindings3 <- + betree_node_lookup_mut_in_bindings_back n0 key bindings bindings2; + Return bindings3 + | BetreeMessageDelete => + bindings1 <- betree_list_pop_front_back (u64 * u64) bindings0; + bindings2 <- + betree_node_lookup_mut_in_bindings_back n0 key bindings bindings1; + Return bindings2 + | BetreeMessageUpsert s => + let (_, i) := hd in + v <- betree_upsert_update_fwd (Some i) s; + bindings1 <- betree_list_pop_front_back (u64 * u64) bindings0; + bindings2 <- + betree_list_push_front_fwd_back (u64 * u64) bindings1 (key, v); + bindings3 <- + betree_node_lookup_mut_in_bindings_back n0 key bindings bindings2; + Return bindings3 + end) + else + match new_msg with + | BetreeMessageInsert v => + bindings1 <- + betree_list_push_front_fwd_back (u64 * u64) bindings0 (key, v); + bindings2 <- + betree_node_lookup_mut_in_bindings_back n0 key bindings bindings1; + Return bindings2 + | BetreeMessageDelete => + bindings1 <- + betree_node_lookup_mut_in_bindings_back n0 key bindings bindings0; + Return bindings1 + | BetreeMessageUpsert s => + v <- betree_upsert_update_fwd None s; + bindings1 <- + betree_list_push_front_fwd_back (u64 * u64) bindings0 (key, v); + bindings2 <- + betree_node_lookup_mut_in_bindings_back n0 key bindings bindings1; + Return bindings2 + end + end + . + +(** [betree_main::betree::Node::{5}::apply_messages_to_leaf] *) +Fixpoint betree_node_apply_messages_to_leaf_fwd_back + (n : nat) (bindings : Betree_list_t (u64 * u64)) + (new_msgs : Betree_list_t (u64 * Betree_message_t)) : + result (Betree_list_t (u64 * u64)) + := + match n with + | O => Fail_ OutOfFuel + | S n0 => + match new_msgs with + | BetreeListCons new_msg new_msgs_tl => + let (i, m) := new_msg in + bindings0 <- betree_node_apply_to_leaf_fwd_back n0 bindings i m; + bindings1 <- + betree_node_apply_messages_to_leaf_fwd_back n0 bindings0 new_msgs_tl; + Return bindings1 + | BetreeListNil => Return bindings + end + end + . + +(** [betree_main::betree::Node::{5}::filter_messages_for_key] *) +Fixpoint betree_node_filter_messages_for_key_fwd_back + (n : nat) (key : u64) (msgs : Betree_list_t (u64 * Betree_message_t)) : + result (Betree_list_t (u64 * Betree_message_t)) + := + match n with + | O => Fail_ OutOfFuel + | S n0 => + match msgs with + | BetreeListCons p l => + let (k, m) := p in + if k s= key + then ( + msgs0 <- + betree_list_pop_front_back (u64 * Betree_message_t) (BetreeListCons + (k, m) l); + msgs1 <- betree_node_filter_messages_for_key_fwd_back n0 key msgs0; + Return msgs1) + else Return (BetreeListCons (k, m) l) + | BetreeListNil => Return BetreeListNil + end + end + . + +(** [betree_main::betree::Node::{5}::lookup_first_message_after_key] *) +Fixpoint betree_node_lookup_first_message_after_key_fwd + (n : nat) (key : u64) (msgs : Betree_list_t (u64 * Betree_message_t)) : + result (Betree_list_t (u64 * Betree_message_t)) + := + match n with + | O => Fail_ OutOfFuel + | S n0 => + match msgs with + | BetreeListCons p next_msgs => + let (k, m) := p in + if k s= key + then ( + l <- betree_node_lookup_first_message_after_key_fwd n0 key next_msgs; + Return l) + else Return (BetreeListCons (k, m) next_msgs) + | BetreeListNil => Return BetreeListNil + end + end + . + +(** [betree_main::betree::Node::{5}::lookup_first_message_after_key] *) +Fixpoint betree_node_lookup_first_message_after_key_back + (n : nat) (key : u64) (msgs : Betree_list_t (u64 * Betree_message_t)) + (ret : Betree_list_t (u64 * Betree_message_t)) : + result (Betree_list_t (u64 * Betree_message_t)) + := + match n with + | O => Fail_ OutOfFuel + | S n0 => + match msgs with + | BetreeListCons p next_msgs => + let (k, m) := p in + if k s= key + then ( + next_msgs0 <- + betree_node_lookup_first_message_after_key_back n0 key next_msgs ret; + Return (BetreeListCons (k, m) next_msgs0)) + else Return ret + | BetreeListNil => Return ret + end + end + . + +(** [betree_main::betree::Node::{5}::apply_to_internal] *) +Definition betree_node_apply_to_internal_fwd_back + (n : nat) (msgs : Betree_list_t (u64 * Betree_message_t)) (key : u64) + (new_msg : Betree_message_t) : + result (Betree_list_t (u64 * Betree_message_t)) + := + match n with + | O => Fail_ OutOfFuel + | S n0 => + msgs0 <- betree_node_lookup_first_message_for_key_fwd n0 key msgs; + b <- betree_list_head_has_key_fwd Betree_message_t msgs0 key; + if b + then + match new_msg with + | BetreeMessageInsert i => + msgs1 <- betree_node_filter_messages_for_key_fwd_back n0 key msgs0; + msgs2 <- + betree_list_push_front_fwd_back (u64 * Betree_message_t) msgs1 (key, + BetreeMessageInsert i); + msgs3 <- + betree_node_lookup_first_message_for_key_back n0 key msgs msgs2; + Return msgs3 + | BetreeMessageDelete => + msgs1 <- betree_node_filter_messages_for_key_fwd_back n0 key msgs0; + msgs2 <- + betree_list_push_front_fwd_back (u64 * Betree_message_t) msgs1 (key, + BetreeMessageDelete); + msgs3 <- + betree_node_lookup_first_message_for_key_back n0 key msgs msgs2; + Return msgs3 + | BetreeMessageUpsert s => + p <- betree_list_hd_fwd (u64 * Betree_message_t) msgs0; + let (_, m) := p in + match m with + | BetreeMessageInsert prev => + v <- betree_upsert_update_fwd (Some prev) s; + msgs1 <- betree_list_pop_front_back (u64 * Betree_message_t) msgs0; + msgs2 <- + betree_list_push_front_fwd_back (u64 * Betree_message_t) msgs1 + (key, BetreeMessageInsert v); + msgs3 <- + betree_node_lookup_first_message_for_key_back n0 key msgs msgs2; + Return msgs3 + | BetreeMessageDelete => + v <- betree_upsert_update_fwd None s; + msgs1 <- betree_list_pop_front_back (u64 * Betree_message_t) msgs0; + msgs2 <- + betree_list_push_front_fwd_back (u64 * Betree_message_t) msgs1 + (key, BetreeMessageInsert v); + msgs3 <- + betree_node_lookup_first_message_for_key_back n0 key msgs msgs2; + Return msgs3 + | BetreeMessageUpsert ufs => + msgs1 <- betree_node_lookup_first_message_after_key_fwd n0 key msgs0; + msgs2 <- + betree_list_push_front_fwd_back (u64 * Betree_message_t) msgs1 + (key, BetreeMessageUpsert s); + msgs3 <- + betree_node_lookup_first_message_after_key_back n0 key msgs0 msgs2; + msgs4 <- + betree_node_lookup_first_message_for_key_back n0 key msgs msgs3; + Return msgs4 + end + end + else ( + msgs1 <- + betree_list_push_front_fwd_back (u64 * Betree_message_t) msgs0 (key, + new_msg); + msgs2 <- betree_node_lookup_first_message_for_key_back n0 key msgs msgs1; + Return msgs2) + end + . + +(** [betree_main::betree::Node::{5}::apply_messages_to_internal] *) +Fixpoint betree_node_apply_messages_to_internal_fwd_back + (n : nat) (msgs : Betree_list_t (u64 * Betree_message_t)) + (new_msgs : Betree_list_t (u64 * Betree_message_t)) : + result (Betree_list_t (u64 * Betree_message_t)) + := + match n with + | O => Fail_ OutOfFuel + | S n0 => + match new_msgs with + | BetreeListCons new_msg new_msgs_tl => + let (i, m) := new_msg in + msgs0 <- betree_node_apply_to_internal_fwd_back n0 msgs i m; + msgs1 <- + betree_node_apply_messages_to_internal_fwd_back n0 msgs0 new_msgs_tl; + Return msgs1 + | BetreeListNil => Return msgs + end + end + . + +(** [betree_main::betree::Node::{5}::apply_messages] *) +Fixpoint betree_node_apply_messages_fwd + (n : nat) (self : Betree_node_t) (params : Betree_params_t) + (node_id_cnt : Betree_node_id_counter_t) + (msgs : Betree_list_t (u64 * Betree_message_t)) (st : state) : + result (state * unit) + := + match n with + | O => Fail_ OutOfFuel + | S n0 => + match self with + | BetreeNodeInternal node => + match node with + | mkBetree_internal_t i i0 n1 n2 => + p <- betree_load_internal_node_fwd i st; + let (st0, content) := p in + content0 <- + betree_node_apply_messages_to_internal_fwd_back n0 content msgs; + num_msgs <- betree_list_len_fwd (u64 * Betree_message_t) n0 content0; + match params with + | mkBetree_params_t i1 i2 => + if num_msgs s>= i1 + then ( + p0 <- + betree_internal_flush_fwd n0 (mkBetree_internal_t i i0 n1 n2) + (mkBetree_params_t i1 i2) node_id_cnt content0 st0; + let (st1, content1) := p0 in + p1 <- + betree_internal_flush_back n0 (mkBetree_internal_t i i0 n1 n2) + (mkBetree_params_t i1 i2) node_id_cnt content0 st0; + let (node0, _) := p1 in + match node0 with + | mkBetree_internal_t i3 i4 n3 n4 => + p2 <- betree_store_internal_node_fwd i3 content1 st1; + let (st2, _) := p2 in + Return (st2, tt) + end) + else ( + p0 <- betree_store_internal_node_fwd i content0 st0; + let (st1, _) := p0 in + Return (st1, tt)) + end + end + | BetreeNodeLeaf node => + match node with + | mkBetree_leaf_t i i0 => + p <- betree_load_leaf_node_fwd i st; + let (st0, content) := p in + content0 <- + betree_node_apply_messages_to_leaf_fwd_back n0 content msgs; + len <- betree_list_len_fwd (u64 * u64) n0 content0; + match params with + | mkBetree_params_t i1 i2 => + i3 <- u64_mul 2 %u64 i2; + if len s>= i3 + then ( + p0 <- + betree_leaf_split_fwd n0 (mkBetree_leaf_t i i0) content0 + (mkBetree_params_t i1 i2) node_id_cnt st0; + let (st1, _) := p0 in + p1 <- betree_store_leaf_node_fwd i BetreeListNil st1; + let (st2, _) := p1 in + Return (st2, tt)) + else ( + p0 <- betree_store_leaf_node_fwd i content0 st0; + let (st1, _) := p0 in + Return (st1, tt)) + end + end + end + end + +(** [betree_main::betree::Node::{5}::apply_messages] *) +with betree_node_apply_messages_back + (n : nat) (self : Betree_node_t) (params : Betree_params_t) + (node_id_cnt : Betree_node_id_counter_t) + (msgs : Betree_list_t (u64 * Betree_message_t)) (st : state) : + result (Betree_node_t * Betree_node_id_counter_t) + := + match n with + | O => Fail_ OutOfFuel + | S n0 => + match self with + | BetreeNodeInternal node => + match node with + | mkBetree_internal_t i i0 n1 n2 => + p <- betree_load_internal_node_fwd i st; + let (st0, content) := p in + content0 <- + betree_node_apply_messages_to_internal_fwd_back n0 content msgs; + num_msgs <- betree_list_len_fwd (u64 * Betree_message_t) n0 content0; + match params with + | mkBetree_params_t i1 i2 => + if num_msgs s>= i1 + then ( + p0 <- + betree_internal_flush_fwd n0 (mkBetree_internal_t i i0 n1 n2) + (mkBetree_params_t i1 i2) node_id_cnt content0 st0; + let (st1, content1) := p0 in + p1 <- + betree_internal_flush_back n0 (mkBetree_internal_t i i0 n1 n2) + (mkBetree_params_t i1 i2) node_id_cnt content0 st0; + let (node0, node_id_cnt0) := p1 in + match node0 with + | mkBetree_internal_t i3 i4 n3 n4 => + p2 <- betree_store_internal_node_fwd i3 content1 st1; + let (_, _) := p2 in + Return (BetreeNodeInternal (mkBetree_internal_t i3 i4 n3 n4), + node_id_cnt0) + end) + else ( + p0 <- betree_store_internal_node_fwd i content0 st0; + let (_, _) := p0 in + Return (BetreeNodeInternal (mkBetree_internal_t i i0 n1 n2), + node_id_cnt)) + end + end + | BetreeNodeLeaf node => + match node with + | mkBetree_leaf_t i i0 => + p <- betree_load_leaf_node_fwd i st; + let (st0, content) := p in + content0 <- + betree_node_apply_messages_to_leaf_fwd_back n0 content msgs; + len <- betree_list_len_fwd (u64 * u64) n0 content0; + match params with + | mkBetree_params_t i1 i2 => + i3 <- u64_mul 2 %u64 i2; + if len s>= i3 + then ( + p0 <- + betree_leaf_split_fwd n0 (mkBetree_leaf_t i i0) content0 + (mkBetree_params_t i1 i2) node_id_cnt st0; + let (st1, new_node) := p0 in + p1 <- betree_store_leaf_node_fwd i BetreeListNil st1; + let (_, _) := p1 in + node_id_cnt0 <- + betree_leaf_split_back n0 (mkBetree_leaf_t i i0) content0 + (mkBetree_params_t i1 i2) node_id_cnt st0; + Return (BetreeNodeInternal new_node, node_id_cnt0)) + else ( + p0 <- betree_store_leaf_node_fwd i content0 st0; + let (_, _) := p0 in + Return (BetreeNodeLeaf (mkBetree_leaf_t i len), node_id_cnt)) + end + end + end + end + +(** [betree_main::betree::Internal::{4}::flush] *) +with betree_internal_flush_fwd + (n : nat) (self : Betree_internal_t) (params : Betree_params_t) + (node_id_cnt : Betree_node_id_counter_t) + (content : Betree_list_t (u64 * Betree_message_t)) (st : state) : + result (state * (Betree_list_t (u64 * Betree_message_t))) + := + match n with + | O => Fail_ OutOfFuel + | S n0 => + match self with + | mkBetree_internal_t i i0 n1 n2 => + p <- betree_list_partition_at_pivot_fwd Betree_message_t n0 content i0; + let (msgs_left, msgs_right) := p in + len_left <- betree_list_len_fwd (u64 * Betree_message_t) n0 msgs_left; + match params with + | mkBetree_params_t i1 i2 => + if len_left s>= i1 + then ( + p0 <- + betree_node_apply_messages_fwd n0 n1 (mkBetree_params_t i1 i2) + node_id_cnt msgs_left st; + let (st0, _) := p0 in + p1 <- + betree_node_apply_messages_back n0 n1 (mkBetree_params_t i1 i2) + node_id_cnt msgs_left st; + let (_, node_id_cnt0) := p1 in + len_right <- + betree_list_len_fwd (u64 * Betree_message_t) n0 msgs_right; + if len_right s>= i1 + then ( + p2 <- + betree_node_apply_messages_fwd n0 n2 (mkBetree_params_t i1 i2) + node_id_cnt0 msgs_right st0; + let (st1, _) := p2 in + p3 <- + betree_node_apply_messages_back n0 n2 (mkBetree_params_t i1 i2) + node_id_cnt0 msgs_right st0; + let (_, _) := p3 in + Return (st1, BetreeListNil)) + else Return (st0, msgs_right)) + else ( + p0 <- + betree_node_apply_messages_fwd n0 n2 (mkBetree_params_t i1 i2) + node_id_cnt msgs_right st; + let (st0, _) := p0 in + p1 <- + betree_node_apply_messages_back n0 n2 (mkBetree_params_t i1 i2) + node_id_cnt msgs_right st; + let (_, _) := p1 in + Return (st0, msgs_left)) + end + end + end + +(** [betree_main::betree::Internal::{4}::flush] *) +with betree_internal_flush_back + (n : nat) (self : Betree_internal_t) (params : Betree_params_t) + (node_id_cnt : Betree_node_id_counter_t) + (content : Betree_list_t (u64 * Betree_message_t)) (st : state) : + result (Betree_internal_t * Betree_node_id_counter_t) + := + match n with + | O => Fail_ OutOfFuel + | S n0 => + match self with + | mkBetree_internal_t i i0 n1 n2 => + p <- betree_list_partition_at_pivot_fwd Betree_message_t n0 content i0; + let (msgs_left, msgs_right) := p in + len_left <- betree_list_len_fwd (u64 * Betree_message_t) n0 msgs_left; + match params with + | mkBetree_params_t i1 i2 => + if len_left s>= i1 + then ( + p0 <- + betree_node_apply_messages_fwd n0 n1 (mkBetree_params_t i1 i2) + node_id_cnt msgs_left st; + let (st0, _) := p0 in + p1 <- + betree_node_apply_messages_back n0 n1 (mkBetree_params_t i1 i2) + node_id_cnt msgs_left st; + let (n3, node_id_cnt0) := p1 in + len_right <- + betree_list_len_fwd (u64 * Betree_message_t) n0 msgs_right; + if len_right s>= i1 + then ( + p2 <- + betree_node_apply_messages_back n0 n2 (mkBetree_params_t i1 i2) + node_id_cnt0 msgs_right st0; + let (n4, node_id_cnt1) := p2 in + Return (mkBetree_internal_t i i0 n3 n4, node_id_cnt1)) + else Return (mkBetree_internal_t i i0 n3 n2, node_id_cnt0)) + else ( + p0 <- + betree_node_apply_messages_back n0 n2 (mkBetree_params_t i1 i2) + node_id_cnt msgs_right st; + let (n3, node_id_cnt0) := p0 in + Return (mkBetree_internal_t i i0 n1 n3, node_id_cnt0)) + end + end + end + . + +(** [betree_main::betree::Node::{5}::apply] *) +Definition betree_node_apply_fwd + (n : nat) (self : Betree_node_t) (params : Betree_params_t) + (node_id_cnt : Betree_node_id_counter_t) (key : u64) + (new_msg : Betree_message_t) (st : state) : + result (state * unit) + := + match n with + | O => Fail_ OutOfFuel + | S n0 => + let l := BetreeListNil in + p <- + betree_node_apply_messages_fwd n0 self params node_id_cnt (BetreeListCons + (key, new_msg) l) st; + let (st0, _) := p in + p0 <- + betree_node_apply_messages_back n0 self params node_id_cnt + (BetreeListCons (key, new_msg) l) st; + let (_, _) := p0 in + Return (st0, tt) + end + . + +(** [betree_main::betree::Node::{5}::apply] *) +Definition betree_node_apply_back + (n : nat) (self : Betree_node_t) (params : Betree_params_t) + (node_id_cnt : Betree_node_id_counter_t) (key : u64) + (new_msg : Betree_message_t) (st : state) : + result (Betree_node_t * Betree_node_id_counter_t) + := + match n with + | O => Fail_ OutOfFuel + | S n0 => + let l := BetreeListNil in + p <- + betree_node_apply_messages_back n0 self params node_id_cnt + (BetreeListCons (key, new_msg) l) st; + let (self0, node_id_cnt0) := p in + Return (self0, node_id_cnt0) + end + . + +(** [betree_main::betree::BeTree::{6}::new] *) +Definition betree_be_tree_new_fwd + (min_flush_size : u64) (split_size : u64) (st : state) : + result (state * Betree_be_tree_t) + := + node_id_cnt <- betree_node_id_counter_new_fwd; + id <- betree_node_id_counter_fresh_id_fwd node_id_cnt; + p <- betree_store_leaf_node_fwd id BetreeListNil st; + let (st0, _) := p in + node_id_cnt0 <- betree_node_id_counter_fresh_id_back node_id_cnt; + Return (st0, mkBetree_be_tree_t (mkBetree_params_t min_flush_size split_size) + node_id_cnt0 (BetreeNodeLeaf (mkBetree_leaf_t id (0 %u64)))) + . + +(** [betree_main::betree::BeTree::{6}::apply] *) +Definition betree_be_tree_apply_fwd + (n : nat) (self : Betree_be_tree_t) (key : u64) (msg : Betree_message_t) + (st : state) : + result (state * unit) + := + match n with + | O => Fail_ OutOfFuel + | S n0 => + match self with + | mkBetree_be_tree_t p nic n1 => + p0 <- betree_node_apply_fwd n0 n1 p nic key msg st; + let (st0, _) := p0 in + p1 <- betree_node_apply_back n0 n1 p nic key msg st; + let (_, _) := p1 in + Return (st0, tt) + end + end + . + +(** [betree_main::betree::BeTree::{6}::apply] *) +Definition betree_be_tree_apply_back + (n : nat) (self : Betree_be_tree_t) (key : u64) (msg : Betree_message_t) + (st : state) : + result Betree_be_tree_t + := + match n with + | O => Fail_ OutOfFuel + | S n0 => + match self with + | mkBetree_be_tree_t p nic n1 => + p0 <- betree_node_apply_back n0 n1 p nic key msg st; + let (n2, nic0) := p0 in + Return (mkBetree_be_tree_t p nic0 n2) + end + end + . + +(** [betree_main::betree::BeTree::{6}::insert] *) +Definition betree_be_tree_insert_fwd + (n : nat) (self : Betree_be_tree_t) (key : u64) (value : u64) (st : state) : + result (state * unit) + := + match n with + | O => Fail_ OutOfFuel + | S n0 => + p <- betree_be_tree_apply_fwd n0 self key (BetreeMessageInsert value) st; + let (st0, _) := p in + bt <- betree_be_tree_apply_back n0 self key (BetreeMessageInsert value) st; + let _ := bt in + Return (st0, tt) + end + . + +(** [betree_main::betree::BeTree::{6}::insert] *) +Definition betree_be_tree_insert_back + (n : nat) (self : Betree_be_tree_t) (key : u64) (value : u64) (st : state) : + result Betree_be_tree_t + := + match n with + | O => Fail_ OutOfFuel + | S n0 => + self0 <- + betree_be_tree_apply_back n0 self key (BetreeMessageInsert value) st; + Return self0 + end + . + +(** [betree_main::betree::BeTree::{6}::delete] *) +Definition betree_be_tree_delete_fwd + (n : nat) (self : Betree_be_tree_t) (key : u64) (st : state) : + result (state * unit) + := + match n with + | O => Fail_ OutOfFuel + | S n0 => + p <- betree_be_tree_apply_fwd n0 self key BetreeMessageDelete st; + let (st0, _) := p in + bt <- betree_be_tree_apply_back n0 self key BetreeMessageDelete st; + let _ := bt in + Return (st0, tt) + end + . + +(** [betree_main::betree::BeTree::{6}::delete] *) +Definition betree_be_tree_delete_back + (n : nat) (self : Betree_be_tree_t) (key : u64) (st : state) : + result Betree_be_tree_t + := + match n with + | O => Fail_ OutOfFuel + | S n0 => + self0 <- betree_be_tree_apply_back n0 self key BetreeMessageDelete st; + Return self0 + end + . + +(** [betree_main::betree::BeTree::{6}::upsert] *) +Definition betree_be_tree_upsert_fwd + (n : nat) (self : Betree_be_tree_t) (key : u64) + (upd : Betree_upsert_fun_state_t) (st : state) : + result (state * unit) + := + match n with + | O => Fail_ OutOfFuel + | S n0 => + p <- betree_be_tree_apply_fwd n0 self key (BetreeMessageUpsert upd) st; + let (st0, _) := p in + bt <- betree_be_tree_apply_back n0 self key (BetreeMessageUpsert upd) st; + let _ := bt in + Return (st0, tt) + end + . + +(** [betree_main::betree::BeTree::{6}::upsert] *) +Definition betree_be_tree_upsert_back + (n : nat) (self : Betree_be_tree_t) (key : u64) + (upd : Betree_upsert_fun_state_t) (st : state) : + result Betree_be_tree_t + := + match n with + | O => Fail_ OutOfFuel + | S n0 => + self0 <- + betree_be_tree_apply_back n0 self key (BetreeMessageUpsert upd) st; + Return self0 + end + . + +(** [betree_main::betree::BeTree::{6}::lookup] *) +Definition betree_be_tree_lookup_fwd + (n : nat) (self : Betree_be_tree_t) (key : u64) (st : state) : + result (state * (option u64)) + := + match n with + | O => Fail_ OutOfFuel + | S n0 => + match self with + | mkBetree_be_tree_t p nic n1 => + p0 <- betree_node_lookup_fwd n0 n1 key st; + let (st0, opt) := p0 in + Return (st0, opt) + end + end + . + +(** [betree_main::betree::BeTree::{6}::lookup] *) +Definition betree_be_tree_lookup_back + (n : nat) (self : Betree_be_tree_t) (key : u64) (st : state) : + result Betree_be_tree_t + := + match n with + | O => Fail_ OutOfFuel + | S n0 => + match self with + | mkBetree_be_tree_t p nic n1 => + n2 <- betree_node_lookup_back n0 n1 key st; + Return (mkBetree_be_tree_t p nic n2) + end + end + . + +(** [betree_main::main] *) +Definition main_fwd : result unit := Return tt . + +End BetreeMain__Funs . diff --git a/tests/coq/betree/BetreeMain__Opaque.v b/tests/coq/betree/BetreeMain__Opaque.v new file mode 100644 index 00000000..95d4b7c0 --- /dev/null +++ b/tests/coq/betree/BetreeMain__Opaque.v @@ -0,0 +1,38 @@ +(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *) +(** [betree_main]: opaque function definitions *) +Require Import Primitives. +Import Primitives. +Require Import Coq.ZArith.ZArith. +Local Open Scope Primitives_scope. +Require Export BetreeMain__Types . +Import BetreeMain__Types . +Module BetreeMain__Opaque . + +(** [betree_main::betree_utils::load_internal_node] *) +Axiom betree_utils_load_internal_node_fwd + : u64 -> state -> result (state * (Betree_list_t (u64 * Betree_message_t))) + . + +(** [betree_main::betree_utils::store_internal_node] *) +Axiom betree_utils_store_internal_node_fwd + : + u64 -> Betree_list_t (u64 * Betree_message_t) -> state -> result (state * + unit) + . + +(** [betree_main::betree_utils::load_leaf_node] *) +Axiom betree_utils_load_leaf_node_fwd + : u64 -> state -> result (state * (Betree_list_t (u64 * u64))) + . + +(** [betree_main::betree_utils::store_leaf_node] *) +Axiom betree_utils_store_leaf_node_fwd + : u64 -> Betree_list_t (u64 * u64) -> state -> result (state * unit) + . + +(** [core::option::Option::{0}::unwrap] *) +Axiom core_option_option_unwrap_fwd : + forall(T : Type) , option T -> state -> result (state * T) + . + +End BetreeMain__Opaque . diff --git a/tests/coq/betree/BetreeMain__Types.v b/tests/coq/betree/BetreeMain__Types.v new file mode 100644 index 00000000..7660a367 --- /dev/null +++ b/tests/coq/betree/BetreeMain__Types.v @@ -0,0 +1,117 @@ +(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *) +(** [betree_main]: type definitions *) +Require Import Primitives. +Import Primitives. +Require Import Coq.ZArith.ZArith. +Local Open Scope Primitives_scope. +Module BetreeMain__Types . + +(** [betree_main::betree::List] *) +Inductive Betree_list_t (T : Type) := +| BetreeListCons : T -> Betree_list_t T -> Betree_list_t T +| BetreeListNil : Betree_list_t T +. + +Arguments BetreeListCons {T} _ _ . +Arguments BetreeListNil {T} . + +(** [betree_main::betree::UpsertFunState] *) +Inductive Betree_upsert_fun_state_t := +| BetreeUpsertFunStateAdd : u64 -> Betree_upsert_fun_state_t +| BetreeUpsertFunStateSub : u64 -> Betree_upsert_fun_state_t +. + +Arguments BetreeUpsertFunStateAdd _ . +Arguments BetreeUpsertFunStateSub _ . + +(** [betree_main::betree::Message] *) +Inductive Betree_message_t := +| BetreeMessageInsert : u64 -> Betree_message_t +| BetreeMessageDelete : Betree_message_t +| BetreeMessageUpsert : Betree_upsert_fun_state_t -> Betree_message_t +. + +Arguments BetreeMessageInsert _ . +Arguments BetreeMessageDelete . +Arguments BetreeMessageUpsert _ . + +(** [betree_main::betree::Leaf] *) +Record Betree_leaf_t := +mkBetree_leaf_t +{ + Betree_leaf_id : u64; Betree_leaf_size : u64; +} +. + +Arguments mkBetree_leaf_t _ _ . +Arguments Betree_leaf_id . +Arguments Betree_leaf_size . + +(** [betree_main::betree::Node] *) +Inductive Betree_node_t := +| BetreeNodeInternal : Betree_internal_t -> Betree_node_t +| BetreeNodeLeaf : Betree_leaf_t -> Betree_node_t + +(** [betree_main::betree::Internal] *) +with Betree_internal_t := +| mkBetree_internal_t : + u64 -> + u64 -> + Betree_node_t -> + Betree_node_t -> + Betree_internal_t +. + +Arguments BetreeNodeInternal _ . +Arguments BetreeNodeLeaf _ . + +Arguments mkBetree_internal_t _ _ _ _ . + +(** [betree_main::betree::Params] *) +Record Betree_params_t := +mkBetree_params_t +{ + Betree_params_min_flush_size : u64; Betree_params_split_size : u64; +} +. + +Arguments mkBetree_params_t _ _ . +Arguments Betree_params_min_flush_size . +Arguments Betree_params_split_size . + +(** [betree_main::betree::NodeIdCounter] *) +Record Betree_node_id_counter_t := +mkBetree_node_id_counter_t +{ + Betree_node_id_counter_next_node_id : u64; +} +. + +Arguments mkBetree_node_id_counter_t _ . +Arguments Betree_node_id_counter_next_node_id . + +(** [betree_main::betree::BeTree] *) +Record Betree_be_tree_t := +mkBetree_be_tree_t +{ + Betree_be_tree_params : Betree_params_t; + Betree_be_tree_node_id_cnt : Betree_node_id_counter_t; + Betree_be_tree_root : Betree_node_t; +} +. + +Arguments mkBetree_be_tree_t _ _ _ . +Arguments Betree_be_tree_params . +Arguments Betree_be_tree_node_id_cnt . +Arguments Betree_be_tree_root . + +(** [core::num::u64::{10}::MAX] *) +Definition core_num_u64_max_body : result u64 := + Return (18446744073709551615 %u64) + . +Definition core_num_u64_max_c : u64 := core_num_u64_max_body%global . + +(** The state type used in the state-error monad *) +Axiom state : Type. + +End BetreeMain__Types . diff --git a/tests/coq/betree/Makefile b/tests/coq/betree/Makefile new file mode 100644 index 00000000..ff1ccd39 --- /dev/null +++ b/tests/coq/betree/Makefile @@ -0,0 +1,22 @@ +# Makefile originally taken from coq-club + +%: Makefile.coq phony + +make -f Makefile.coq $@ + +all: Makefile.coq + +make -f Makefile.coq all + +clean: Makefile.coq + +make -f Makefile.coq clean + rm -f Makefile.coq + +Makefile.coq: _CoqProject Makefile + coq_makefile -f _CoqProject | sed 's/$$(COQCHK) $$(COQCHKFLAGS) $$(COQLIBS)/$$(COQCHK) $$(COQCHKFLAGS) $$(subst -Q,-R,$$(COQLIBS))/' > Makefile.coq + +_CoqProject: ; + +Makefile: ; + +phony: ; + +.PHONY: all clean phony diff --git a/tests/coq/betree/Primitives.v b/tests/coq/betree/Primitives.v new file mode 100644 index 00000000..9a97d6c7 --- /dev/null +++ b/tests/coq/betree/Primitives.v @@ -0,0 +1,482 @@ +Require Import Lia. +Require Coq.Strings.Ascii. +Require Coq.Strings.String. +Require Import Coq.Program.Equality. +Require Import Coq.ZArith.ZArith. +Require Import Coq.ZArith.Znat. +Require Import List. +Import ListNotations. + +Module Primitives. + + (* TODO: use more *) +Declare Scope Primitives_scope. + +(*** Result *) + +Inductive error := + | Failure + | OutOfFuel. + +Inductive result A := + | Return : A -> result A + | Fail_ : error -> result A. + +Arguments Return {_} a. +Arguments Fail_ {_}. + +Definition bind {A B} (m: result A) (f: A -> result B) : result B := + match m with + | Fail_ e => Fail_ e + | Return x => f x + end. + +Definition return_ {A: Type} (x: A) : result A := Return x. +Definition fail_ {A: Type} (e: error) : result A := Fail_ e. + +Notation "x <- c1 ; c2" := (bind c1 (fun x => c2)) + (at level 61, c1 at next level, right associativity). + +(** Monadic assert *) +Definition massert (b: bool) : result unit := + if b then Return tt else Fail_ Failure. + +(** Normalize and unwrap a successful result (used for globals) *) +Definition eval_result_refl {A} {x} (a: result A) (p: a = Return x) : A := + match a as r return (r = Return x -> A) with + | Return a' => fun _ => a' + | Fail_ e => fun p' => + False_rect _ (eq_ind (Fail_ e) + (fun e : result A => + match e with + | Return _ => False + | Fail_ e => True + end) + I (Return x) p') + end p. + +Notation "x %global" := (eval_result_refl x eq_refl) (at level 40). +Notation "x %return" := (eval_result_refl x eq_refl) (at level 40). + +(* Sanity check *) +Check (if true then Return (1 + 2) else Fail_ Failure)%global = 3. + +(*** Misc *) + + +Definition string := Coq.Strings.String.string. +Definition char := Coq.Strings.Ascii.ascii. +Definition char_of_byte := Coq.Strings.Ascii.ascii_of_byte. + +Definition mem_replace_fwd (a : Type) (x : a) (y : a) : a := x . +Definition mem_replace_back (a : Type) (x : a) (y : a) : a := y . + +(*** Scalars *) + +Definition i8_min : Z := -128%Z. +Definition i8_max : Z := 127%Z. +Definition i16_min : Z := -32768%Z. +Definition i16_max : Z := 32767%Z. +Definition i32_min : Z := -2147483648%Z. +Definition i32_max : Z := 2147483647%Z. +Definition i64_min : Z := -9223372036854775808%Z. +Definition i64_max : Z := 9223372036854775807%Z. +Definition i128_min : Z := -170141183460469231731687303715884105728%Z. +Definition i128_max : Z := 170141183460469231731687303715884105727%Z. +Definition u8_min : Z := 0%Z. +Definition u8_max : Z := 255%Z. +Definition u16_min : Z := 0%Z. +Definition u16_max : Z := 65535%Z. +Definition u32_min : Z := 0%Z. +Definition u32_max : Z := 4294967295%Z. +Definition u64_min : Z := 0%Z. +Definition u64_max : Z := 18446744073709551615%Z. +Definition u128_min : Z := 0%Z. +Definition u128_max : Z := 340282366920938463463374607431768211455%Z. + +(** The bounds of [isize] and [usize] vary with the architecture. *) +Axiom isize_min : Z. +Axiom isize_max : Z. +Definition usize_min : Z := 0%Z. +Axiom usize_max : Z. + +Open Scope Z_scope. + +(** We provide those lemmas to reason about the bounds of [isize] and [usize] *) +Axiom isize_min_bound : isize_min <= i32_min. +Axiom isize_max_bound : i32_max <= isize_max. +Axiom usize_max_bound : u32_max <= usize_max. + +Inductive scalar_ty := + | Isize + | I8 + | I16 + | I32 + | I64 + | I128 + | Usize + | U8 + | U16 + | U32 + | U64 + | U128 +. + +Definition scalar_min (ty: scalar_ty) : Z := + match ty with + | Isize => isize_min + | I8 => i8_min + | I16 => i16_min + | I32 => i32_min + | I64 => i64_min + | I128 => i128_min + | Usize => usize_min + | U8 => u8_min + | U16 => u16_min + | U32 => u32_min + | U64 => u64_min + | U128 => u128_min +end. + +Definition scalar_max (ty: scalar_ty) : Z := + match ty with + | Isize => isize_max + | I8 => i8_max + | I16 => i16_max + | I32 => i32_max + | I64 => i64_max + | I128 => i128_max + | Usize => usize_max + | U8 => u8_max + | U16 => u16_max + | U32 => u32_max + | U64 => u64_max + | U128 => u128_max +end. + +(** We use the following conservative bounds to make sure we can compute bound + checks in most situations *) +Definition scalar_min_cons (ty: scalar_ty) : Z := + match ty with + | Isize => i32_min + | Usize => u32_min + | _ => scalar_min ty +end. + +Definition scalar_max_cons (ty: scalar_ty) : Z := + match ty with + | Isize => i32_max + | Usize => u32_max + | _ => scalar_max ty +end. + +Lemma scalar_min_cons_valid : forall ty, scalar_min ty <= scalar_min_cons ty . +Proof. + destruct ty; unfold scalar_min_cons, scalar_min; try lia. + - pose isize_min_bound; lia. + - apply Z.le_refl. +Qed. + +Lemma scalar_max_cons_valid : forall ty, scalar_max ty >= scalar_max_cons ty . +Proof. + destruct ty; unfold scalar_max_cons, scalar_max; try lia. + - pose isize_max_bound; lia. + - pose usize_max_bound. lia. +Qed. + +Definition scalar (ty: scalar_ty) : Type := + { x: Z | scalar_min ty <= x <= scalar_max ty }. + +Definition to_Z {ty} (x: scalar ty) : Z := proj1_sig x. + +(** Bounds checks: we start by using the conservative bounds, to make sure we + can compute in most situations, then we use the real bounds (for [isize] + and [usize]). *) +Definition scalar_ge_min (ty: scalar_ty) (x: Z) : bool := + Z.leb (scalar_min_cons ty) x || Z.leb (scalar_min ty) x. + +Definition scalar_le_max (ty: scalar_ty) (x: Z) : bool := + Z.leb x (scalar_max_cons ty) || Z.leb x (scalar_max ty). + +Lemma scalar_ge_min_valid (ty: scalar_ty) (x: Z) : + scalar_ge_min ty x = true -> scalar_min ty <= x . +Proof. + unfold scalar_ge_min. + pose (scalar_min_cons_valid ty). + lia. +Qed. + +Lemma scalar_le_max_valid (ty: scalar_ty) (x: Z) : + scalar_le_max ty x = true -> x <= scalar_max ty . +Proof. + unfold scalar_le_max. + pose (scalar_max_cons_valid ty). + lia. +Qed. + +Definition scalar_in_bounds (ty: scalar_ty) (x: Z) : bool := + scalar_ge_min ty x && scalar_le_max ty x . + +Lemma scalar_in_bounds_valid (ty: scalar_ty) (x: Z) : + scalar_in_bounds ty x = true -> scalar_min ty <= x <= scalar_max ty . +Proof. + unfold scalar_in_bounds. + intros H. + destruct (scalar_ge_min ty x) eqn:Hmin. + - destruct (scalar_le_max ty x) eqn:Hmax. + + pose (scalar_ge_min_valid ty x Hmin). + pose (scalar_le_max_valid ty x Hmax). + lia. + + inversion H. + - inversion H. +Qed. + +Import Sumbool. + +Definition mk_scalar (ty: scalar_ty) (x: Z) : result (scalar ty) := + match sumbool_of_bool (scalar_in_bounds ty x) with + | left H => Return (exist _ x (scalar_in_bounds_valid _ _ H)) + | right _ => Fail_ Failure + end. + +Definition scalar_add {ty} (x y: scalar ty) : result (scalar ty) := mk_scalar ty (to_Z x + to_Z y). + +Definition scalar_sub {ty} (x y: scalar ty) : result (scalar ty) := mk_scalar ty (to_Z x - to_Z y). + +Definition scalar_mul {ty} (x y: scalar ty) : result (scalar ty) := mk_scalar ty (to_Z x * to_Z y). + +Definition scalar_div {ty} (x y: scalar ty) : result (scalar ty) := + if to_Z y =? 0 then Fail_ Failure else + mk_scalar ty (to_Z x / to_Z y). + +Definition scalar_rem {ty} (x y: scalar ty) : result (scalar ty) := mk_scalar ty (Z.rem (to_Z x) (to_Z y)). + +Definition scalar_neg {ty} (x: scalar ty) : result (scalar ty) := mk_scalar ty (-(to_Z x)). + +(** Cast an integer from a [src_ty] to a [tgt_ty] *) +(* TODO: check the semantics of casts in Rust *) +Definition scalar_cast (src_ty tgt_ty : scalar_ty) (x : scalar src_ty) : result (scalar tgt_ty) := + mk_scalar tgt_ty (to_Z x). + +(** Comparisons *) +Print Z.leb . + +Definition scalar_leb {ty : scalar_ty} (x : scalar ty) (y : scalar ty) : bool := + Z.leb (to_Z x) (to_Z y) . + +Definition scalar_ltb {ty : scalar_ty} (x : scalar ty) (y : scalar ty) : bool := + Z.ltb (to_Z x) (to_Z y) . + +Definition scalar_geb {ty : scalar_ty} (x : scalar ty) (y : scalar ty) : bool := + Z.geb (to_Z x) (to_Z y) . + +Definition scalar_gtb {ty : scalar_ty} (x : scalar ty) (y : scalar ty) : bool := + Z.gtb (to_Z x) (to_Z y) . + +Definition scalar_eqb {ty : scalar_ty} (x : scalar ty) (y : scalar ty) : bool := + Z.eqb (to_Z x) (to_Z y) . + +Definition scalar_neqb {ty : scalar_ty} (x : scalar ty) (y : scalar ty) : bool := + negb (Z.eqb (to_Z x) (to_Z y)) . + + +(** The scalar types *) +Definition isize := scalar Isize. +Definition i8 := scalar I8. +Definition i16 := scalar I16. +Definition i32 := scalar I32. +Definition i64 := scalar I64. +Definition i128 := scalar I128. +Definition usize := scalar Usize. +Definition u8 := scalar U8. +Definition u16 := scalar U16. +Definition u32 := scalar U32. +Definition u64 := scalar U64. +Definition u128 := scalar U128. + +(** Negaion *) +Definition isize_neg := @scalar_neg Isize. +Definition i8_neg := @scalar_neg I8. +Definition i16_neg := @scalar_neg I16. +Definition i32_neg := @scalar_neg I32. +Definition i64_neg := @scalar_neg I64. +Definition i128_neg := @scalar_neg I128. + +(** Division *) +Definition isize_div := @scalar_div Isize. +Definition i8_div := @scalar_div I8. +Definition i16_div := @scalar_div I16. +Definition i32_div := @scalar_div I32. +Definition i64_div := @scalar_div I64. +Definition i128_div := @scalar_div I128. +Definition usize_div := @scalar_div Usize. +Definition u8_div := @scalar_div U8. +Definition u16_div := @scalar_div U16. +Definition u32_div := @scalar_div U32. +Definition u64_div := @scalar_div U64. +Definition u128_div := @scalar_div U128. + +(** Remainder *) +Definition isize_rem := @scalar_rem Isize. +Definition i8_rem := @scalar_rem I8. +Definition i16_rem := @scalar_rem I16. +Definition i32_rem := @scalar_rem I32. +Definition i64_rem := @scalar_rem I64. +Definition i128_rem := @scalar_rem I128. +Definition usize_rem := @scalar_rem Usize. +Definition u8_rem := @scalar_rem U8. +Definition u16_rem := @scalar_rem U16. +Definition u32_rem := @scalar_rem U32. +Definition u64_rem := @scalar_rem U64. +Definition u128_rem := @scalar_rem U128. + +(** Addition *) +Definition isize_add := @scalar_add Isize. +Definition i8_add := @scalar_add I8. +Definition i16_add := @scalar_add I16. +Definition i32_add := @scalar_add I32. +Definition i64_add := @scalar_add I64. +Definition i128_add := @scalar_add I128. +Definition usize_add := @scalar_add Usize. +Definition u8_add := @scalar_add U8. +Definition u16_add := @scalar_add U16. +Definition u32_add := @scalar_add U32. +Definition u64_add := @scalar_add U64. +Definition u128_add := @scalar_add U128. + +(** Substraction *) +Definition isize_sub := @scalar_sub Isize. +Definition i8_sub := @scalar_sub I8. +Definition i16_sub := @scalar_sub I16. +Definition i32_sub := @scalar_sub I32. +Definition i64_sub := @scalar_sub I64. +Definition i128_sub := @scalar_sub I128. +Definition usize_sub := @scalar_sub Usize. +Definition u8_sub := @scalar_sub U8. +Definition u16_sub := @scalar_sub U16. +Definition u32_sub := @scalar_sub U32. +Definition u64_sub := @scalar_sub U64. +Definition u128_sub := @scalar_sub U128. + +(** Multiplication *) +Definition isize_mul := @scalar_mul Isize. +Definition i8_mul := @scalar_mul I8. +Definition i16_mul := @scalar_mul I16. +Definition i32_mul := @scalar_mul I32. +Definition i64_mul := @scalar_mul I64. +Definition i128_mul := @scalar_mul I128. +Definition usize_mul := @scalar_mul Usize. +Definition u8_mul := @scalar_mul U8. +Definition u16_mul := @scalar_mul U16. +Definition u32_mul := @scalar_mul U32. +Definition u64_mul := @scalar_mul U64. +Definition u128_mul := @scalar_mul U128. + +(** Small utility *) +Definition usize_to_nat (x: usize) : nat := Z.to_nat (to_Z x). + +(** Notations *) +Notation "x %isize" := ((mk_scalar Isize x)%return) (at level 9). +Notation "x %i8" := ((mk_scalar I8 x)%return) (at level 9). +Notation "x %i16" := ((mk_scalar I16 x)%return) (at level 9). +Notation "x %i32" := ((mk_scalar I32 x)%return) (at level 9). +Notation "x %i64" := ((mk_scalar I64 x)%return) (at level 9). +Notation "x %i128" := ((mk_scalar I128 x)%return) (at level 9). +Notation "x %usize" := ((mk_scalar Usize x)%return) (at level 9). +Notation "x %u8" := ((mk_scalar U8 x)%return) (at level 9). +Notation "x %u16" := ((mk_scalar U16 x)%return) (at level 9). +Notation "x %u32" := ((mk_scalar U32 x)%return) (at level 9). +Notation "x %u64" := ((mk_scalar U64 x)%return) (at level 9). +Notation "x %u128" := ((mk_scalar U128 x)%return) (at level 9). + +Notation "x s= y" := (scalar_eqb x y) (at level 80) : Primitives_scope. +Notation "x s<> y" := (scalar_neqb x y) (at level 80) : Primitives_scope. +Notation "x s<= y" := (scalar_leb x y) (at level 80) : Primitives_scope. +Notation "x s< y" := (scalar_ltb x y) (at level 80) : Primitives_scope. +Notation "x s>= y" := (scalar_geb x y) (at level 80) : Primitives_scope. +Notation "x s> y" := (scalar_gtb x y) (at level 80) : Primitives_scope. + +(*** Vectors *) + +Definition vec T := { l: list T | Z.of_nat (length l) <= usize_max }. + +Definition vec_to_list {T: Type} (v: vec T) : list T := proj1_sig v. + +Definition vec_length {T: Type} (v: vec T) : Z := Z.of_nat (length (vec_to_list v)). + +Lemma le_0_usize_max : 0 <= usize_max. +Proof. + pose (H := usize_max_bound). + unfold u32_max in H. + lia. +Qed. + +Definition vec_new (T: Type) : vec T := (exist _ [] le_0_usize_max). + +Lemma vec_len_in_usize {T} (v: vec T) : usize_min <= vec_length v <= usize_max. +Proof. + unfold vec_length, usize_min. + split. + - lia. + - apply (proj2_sig v). +Qed. + +Definition vec_len (T: Type) (v: vec T) : usize := + exist _ (vec_length v) (vec_len_in_usize v). + +Fixpoint list_update {A} (l: list A) (n: nat) (a: A) + : list A := + match l with + | [] => [] + | x :: t => match n with + | 0%nat => a :: t + | S m => x :: (list_update t m a) +end end. + +Definition vec_bind {A B} (v: vec A) (f: list A -> result (list B)) : result (vec B) := + l <- f (vec_to_list v) ; + match sumbool_of_bool (scalar_le_max Usize (Z.of_nat (length l))) with + | left H => Return (exist _ l (scalar_le_max_valid _ _ H)) + | right _ => Fail_ Failure + end. + +(* The **forward** function shouldn't be used *) +Definition vec_push_fwd (T: Type) (v: vec T) (x: T) : unit := tt. + +Definition vec_push_back (T: Type) (v: vec T) (x: T) : result (vec T) := + vec_bind v (fun l => Return (l ++ [x])). + +(* The **forward** function shouldn't be used *) +Definition vec_insert_fwd (T: Type) (v: vec T) (i: usize) (x: T) : result unit := + if to_Z i <? vec_length v then Return tt else Fail_ Failure. + +Definition vec_insert_back (T: Type) (v: vec T) (i: usize) (x: T) : result (vec T) := + vec_bind v (fun l => + if to_Z i <? Z.of_nat (length l) + then Return (list_update l (usize_to_nat i) x) + else Fail_ Failure). + +(* The **backward** function shouldn't be used *) +Definition vec_index_fwd (T: Type) (v: vec T) (i: usize) : result T := + match nth_error (vec_to_list v) (usize_to_nat i) with + | Some n => Return n + | None => Fail_ Failure + end. + +Definition vec_index_back (T: Type) (v: vec T) (i: usize) (x: T) : result unit := + if to_Z i <? vec_length v then Return tt else Fail_ Failure. + +(* The **backward** function shouldn't be used *) +Definition vec_index_mut_fwd (T: Type) (v: vec T) (i: usize) : result T := + match nth_error (vec_to_list v) (usize_to_nat i) with + | Some n => Return n + | None => Fail_ Failure + end. + +Definition vec_index_mut_back (T: Type) (v: vec T) (i: usize) (x: T) : result (vec T) := + vec_bind v (fun l => + if to_Z i <? Z.of_nat (length l) + then Return (list_update l (usize_to_nat i) x) + else Fail_ Failure). + +End Primitives. diff --git a/tests/coq/betree/_CoqProject b/tests/coq/betree/_CoqProject new file mode 100644 index 00000000..5e08a7a6 --- /dev/null +++ b/tests/coq/betree/_CoqProject @@ -0,0 +1,9 @@ +-R . Lib +-arg -w +-arg all + +Primitives.v + +BetreeMain__Funs.v +BetreeMain__Opaque.v +BetreeMain__Types.v
\ No newline at end of file diff --git a/tests/coq/misc/PoloniusList.v b/tests/coq/misc/PoloniusList.v new file mode 100644 index 00000000..6d6ea537 --- /dev/null +++ b/tests/coq/misc/PoloniusList.v @@ -0,0 +1,41 @@ +(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *) +(** [polonius_list] *) +Require Import Primitives. +Import Primitives. +Require Import Coq.ZArith.ZArith. +Local Open Scope Primitives_scope. +Module PoloniusList . + +(** [polonius_list::List] *) +Inductive List_t (T : Type) := +| ListCons : T -> List_t T -> List_t T +| ListNil : List_t T +. + +Arguments ListCons {T} _ _ . +Arguments ListNil {T} . + +(** [polonius_list::get_list_at_x] *) +Fixpoint get_list_at_x_fwd (ls : List_t u32) (x : u32) : result (List_t u32) := + match ls with + | ListCons hd tl => + if hd s= x + then Return (ListCons hd tl) + else (l <- get_list_at_x_fwd tl x; Return l) + | ListNil => Return ListNil + end + . + +(** [polonius_list::get_list_at_x] *) +Fixpoint get_list_at_x_back + (ls : List_t u32) (x : u32) (ret : List_t u32) : result (List_t u32) := + match ls with + | ListCons hd tl => + if hd s= x + then Return ret + else (tl0 <- get_list_at_x_back tl x ret; Return (ListCons hd tl0)) + | ListNil => Return ret + end + . + +End PoloniusList . diff --git a/tests/coq/misc/_CoqProject b/tests/coq/misc/_CoqProject index 7f4981fa..16fcaf44 100644 --- a/tests/coq/misc/_CoqProject +++ b/tests/coq/misc/_CoqProject @@ -9,4 +9,5 @@ External__Funs.v External__Opaque.v External__Types.v NoNestedBorrows.v -Paper.v
\ No newline at end of file +Paper.v +PoloniusList.v
\ No newline at end of file |