diff options
Diffstat (limited to 'tests/fstar')
| -rw-r--r-- | tests/fstar/betree/BetreeMain.Funs.fst | 421 | ||||
| -rw-r--r-- | tests/fstar/betree/Primitives.fst | 32 | ||||
| -rw-r--r-- | tests/fstar/betree_back_stateful/BetreeMain.Funs.fst | 551 | ||||
| -rw-r--r-- | tests/fstar/betree_back_stateful/Primitives.fst | 32 | ||||
| -rw-r--r-- | tests/fstar/hashmap/Hashmap.Funs.fst | 200 | ||||
| -rw-r--r-- | tests/fstar/hashmap/Hashmap.Properties.fst | 260 | ||||
| -rw-r--r-- | tests/fstar/hashmap/Hashmap.Properties.fsti | 20 | ||||
| -rw-r--r-- | tests/fstar/hashmap/Primitives.fst | 32 | ||||
| -rw-r--r-- | tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst | 206 | ||||
| -rw-r--r-- | tests/fstar/hashmap_on_disk/HashmapMain.Properties.fst | 8 | ||||
| -rw-r--r-- | tests/fstar/hashmap_on_disk/Primitives.fst | 32 | ||||
| -rw-r--r-- | tests/fstar/misc/Constants.fst | 38 | ||||
| -rw-r--r-- | tests/fstar/misc/External.Funs.fst | 41 | ||||
| -rw-r--r-- | tests/fstar/misc/NoNestedBorrows.fst | 155 | ||||
| -rw-r--r-- | tests/fstar/misc/Paper.fst | 53 | ||||
| -rw-r--r-- | tests/fstar/misc/PoloniusList.fst | 4 | ||||
| -rw-r--r-- | tests/fstar/misc/Primitives.fst | 32 |
17 files changed, 1088 insertions, 1029 deletions
diff --git a/tests/fstar/betree/BetreeMain.Funs.fst b/tests/fstar/betree/BetreeMain.Funs.fst index 8cb5eb41..f6045dfd 100644 --- a/tests/fstar/betree/BetreeMain.Funs.fst +++ b/tests/fstar/betree/BetreeMain.Funs.fst @@ -14,7 +14,7 @@ let betree_load_internal_node_fwd result (state & (betree_list_t (u64 & betree_message_t))) = begin match betree_utils_load_internal_node_fwd id st with - | Fail -> Fail + | Fail e -> Fail e | Return (st0, l) -> Return (st0, l) end @@ -24,7 +24,7 @@ let betree_store_internal_node_fwd result (state & unit) = begin match betree_utils_store_internal_node_fwd id content st with - | Fail -> Fail + | Fail e -> Fail e | Return (st0, _) -> Return (st0, ()) end @@ -32,7 +32,7 @@ let betree_store_internal_node_fwd let betree_load_leaf_node_fwd (id : u64) (st : state) : result (state & (betree_list_t (u64 & u64))) = begin match betree_utils_load_leaf_node_fwd id st with - | Fail -> Fail + | Fail e -> Fail e | Return (st0, l) -> Return (st0, l) end @@ -42,21 +42,21 @@ let betree_store_leaf_node_fwd result (state & unit) = begin match betree_utils_store_leaf_node_fwd id content st with - | Fail -> Fail + | Fail e -> Fail e | Return (st0, _) -> Return (st0, ()) end (** [betree_main::betree::fresh_node_id] *) let betree_fresh_node_id_fwd (counter : u64) : result u64 = begin match u64_add counter 1 with - | Fail -> Fail + | Fail e -> Fail e | Return _ -> Return counter end (** [betree_main::betree::fresh_node_id] *) let betree_fresh_node_id_back (counter : u64) : result u64 = begin match u64_add counter 1 with - | Fail -> Fail + | Fail e -> Fail e | Return counter0 -> Return counter0 end @@ -68,7 +68,7 @@ let betree_node_id_counter_new_fwd : result betree_node_id_counter_t = let betree_node_id_counter_fresh_id_fwd (self : betree_node_id_counter_t) : result u64 = begin match u64_add self.betree_node_id_counter_next_node_id 1 with - | Fail -> Fail + | Fail e -> Fail e | Return _ -> Return self.betree_node_id_counter_next_node_id end @@ -76,7 +76,7 @@ let betree_node_id_counter_fresh_id_fwd let betree_node_id_counter_fresh_id_back (self : betree_node_id_counter_t) : result betree_node_id_counter_t = begin match u64_add self.betree_node_id_counter_next_node_id 1 with - | Fail -> Fail + | Fail e -> Fail e | Return i -> Return (Mkbetree_node_id_counter_t i) end @@ -97,12 +97,12 @@ let betree_upsert_update_fwd begin match st with | BetreeUpsertFunStateAdd v -> begin match u64_sub core_num_u64_max_c prev0 with - | Fail -> Fail + | Fail e -> Fail e | Return margin -> if margin >= v then begin match u64_add prev0 v with - | Fail -> Fail + | Fail e -> Fail e | Return i -> Return i end else Return core_num_u64_max_c @@ -111,7 +111,7 @@ let betree_upsert_update_fwd if prev0 >= v then begin match u64_sub prev0 v with - | Fail -> Fail + | Fail e -> Fail e | Return i -> Return i end else Return 0 @@ -126,9 +126,12 @@ let rec betree_list_len_fwd begin match self with | BetreeListCons x tl -> begin match betree_list_len_fwd t tl with - | Fail -> Fail + | Fail e -> Fail e | Return i -> - begin match u64_add 1 i with | Fail -> Fail | Return i0 -> Return i0 end + begin match u64_add 1 i with + | Fail e -> Fail e + | Return i0 -> Return i0 + end end | BetreeListNil -> Return 0 end @@ -145,17 +148,17 @@ let rec betree_list_split_at_fwd begin match self with | BetreeListCons hd tl -> begin match u64_sub n 1 with - | Fail -> Fail + | Fail e -> Fail e | Return i -> begin match betree_list_split_at_fwd t tl i with - | Fail -> Fail + | Fail e -> Fail e | Return p -> let (ls0, ls1) = p in let l = ls0 in Return (BetreeListCons hd l, ls1) end end - | BetreeListNil -> Fail + | BetreeListNil -> Fail Failure end (** [betree_main::betree::List::{1}::push_front] *) @@ -170,7 +173,7 @@ let betree_list_pop_front_fwd (t : Type0) (self : betree_list_t t) : result t = let ls = mem_replace_fwd (betree_list_t t) self BetreeListNil in begin match ls with | BetreeListCons x tl -> Return x - | BetreeListNil -> Fail + | BetreeListNil -> Fail Failure end (** [betree_main::betree::List::{1}::pop_front] *) @@ -179,14 +182,14 @@ let betree_list_pop_front_back let ls = mem_replace_fwd (betree_list_t t) self BetreeListNil in begin match ls with | BetreeListCons x tl -> Return tl - | BetreeListNil -> Fail + | BetreeListNil -> Fail Failure end (** [betree_main::betree::List::{1}::hd] *) let betree_list_hd_fwd (t : Type0) (self : betree_list_t t) : result t = begin match self with | BetreeListCons hd l -> Return hd - | BetreeListNil -> Fail + | BetreeListNil -> Fail Failure end (** [betree_main::betree::List::{2}::head_has_key] *) @@ -210,7 +213,7 @@ let rec betree_list_partition_at_pivot_fwd then Return (BetreeListNil, BetreeListCons (i, x) tl) else begin match betree_list_partition_at_pivot_fwd t tl pivot with - | Fail -> Fail + | Fail e -> Fail e | Return p -> let (ls0, ls1) = p in let l = ls0 in @@ -229,27 +232,27 @@ let betree_leaf_split_fwd begin match betree_list_split_at_fwd (u64 & u64) content params.betree_params_split_size with - | Fail -> Fail + | Fail e -> Fail e | Return p -> let (content0, content1) = p in begin match betree_list_hd_fwd (u64 & u64) content1 with - | Fail -> Fail + | Fail e -> Fail e | Return p0 -> let (pivot, _) = p0 in begin match betree_node_id_counter_fresh_id_fwd node_id_cnt with - | Fail -> Fail + | Fail e -> Fail e | Return id0 -> begin match betree_node_id_counter_fresh_id_back node_id_cnt with - | Fail -> Fail + | Fail e -> Fail e | Return node_id_cnt0 -> begin match betree_node_id_counter_fresh_id_fwd node_id_cnt0 with - | Fail -> Fail + | Fail e -> Fail e | Return id1 -> begin match betree_store_leaf_node_fwd id0 content0 st with - | Fail -> Fail + | Fail e -> Fail e | Return (st0, _) -> begin match betree_store_leaf_node_fwd id1 content1 st0 with - | Fail -> Fail + | Fail e -> Fail e | Return (st1, _) -> let n = BetreeNodeLeaf (Mkbetree_leaf_t id0 params.betree_params_split_size) in @@ -275,30 +278,30 @@ let betree_leaf_split_back begin match betree_list_split_at_fwd (u64 & u64) content params.betree_params_split_size with - | Fail -> Fail + | Fail e -> Fail e | Return p -> let (content0, content1) = p in begin match betree_list_hd_fwd (u64 & u64) content1 with - | Fail -> Fail + | Fail e -> Fail e | Return _ -> begin match betree_node_id_counter_fresh_id_fwd node_id_cnt with - | Fail -> Fail + | Fail e -> Fail e | Return id0 -> begin match betree_node_id_counter_fresh_id_back node_id_cnt with - | Fail -> Fail + | Fail e -> Fail e | Return node_id_cnt0 -> begin match betree_node_id_counter_fresh_id_fwd node_id_cnt0 with - | Fail -> Fail + | Fail e -> Fail e | Return id1 -> begin match betree_store_leaf_node_fwd id0 content0 st with - | Fail -> Fail + | Fail e -> Fail e | Return (st0, _) -> begin match betree_store_leaf_node_fwd id1 content1 st0 with - | Fail -> Fail + | Fail e -> Fail e | Return (_, _) -> begin match betree_node_id_counter_fresh_id_back node_id_cnt0 with - | Fail -> Fail + | Fail e -> Fail e | Return node_id_cnt1 -> Return node_id_cnt1 end end @@ -325,7 +328,7 @@ let rec betree_node_lookup_in_bindings_fwd then Return None else begin match betree_node_lookup_in_bindings_fwd key tl with - | Fail -> Fail + | Fail e -> Fail e | Return opt -> Return opt end | BetreeListNil -> Return None @@ -345,7 +348,7 @@ let rec betree_node_lookup_first_message_for_key_fwd else begin match betree_node_lookup_first_message_for_key_fwd key next_msgs with - | Fail -> Fail + | Fail e -> Fail e | Return l -> Return l end | BetreeListNil -> Return BetreeListNil @@ -366,7 +369,7 @@ let rec betree_node_lookup_first_message_for_key_back else begin match betree_node_lookup_first_message_for_key_back key next_msgs ret with - | Fail -> Fail + | Fail e -> Fail e | Return next_msgs0 -> Return (BetreeListCons (i, m) next_msgs0) end | BetreeListNil -> Return ret @@ -380,28 +383,28 @@ let rec betree_node_apply_upserts_fwd (decreases (betree_node_apply_upserts_decreases msgs prev key st)) = begin match betree_list_head_has_key_fwd betree_message_t msgs key with - | Fail -> Fail + | Fail e -> Fail e | Return b -> if b then begin match betree_list_pop_front_fwd (u64 & betree_message_t) msgs with - | Fail -> Fail + | Fail e -> Fail e | Return msg -> let (_, m) = msg in begin match m with - | BetreeMessageInsert i -> Fail - | BetreeMessageDelete -> Fail + | BetreeMessageInsert i -> Fail Failure + | BetreeMessageDelete -> Fail Failure | BetreeMessageUpsert s -> begin match betree_upsert_update_fwd prev s with - | Fail -> Fail + | Fail e -> Fail e | Return v -> begin match betree_list_pop_front_back (u64 & betree_message_t) msgs with - | Fail -> Fail + | Fail e -> Fail e | Return msgs0 -> begin match betree_node_apply_upserts_fwd msgs0 (Some v) key st with - | Fail -> Fail + | Fail e -> Fail e | Return (st0, i) -> Return (st0, i) end end @@ -410,12 +413,12 @@ let rec betree_node_apply_upserts_fwd end else begin match core_option_option_unwrap_fwd u64 prev st with - | Fail -> Fail + | Fail e -> Fail e | Return (st0, v) -> begin match betree_list_push_front_fwd_back (u64 & betree_message_t) msgs (key, BetreeMessageInsert v) with - | Fail -> Fail + | Fail e -> Fail e | Return _ -> Return (st0, v) end end @@ -429,28 +432,28 @@ let rec betree_node_apply_upserts_back (decreases (betree_node_apply_upserts_decreases msgs prev key st)) = begin match betree_list_head_has_key_fwd betree_message_t msgs key with - | Fail -> Fail + | Fail e -> Fail e | Return b -> if b then begin match betree_list_pop_front_fwd (u64 & betree_message_t) msgs with - | Fail -> Fail + | Fail e -> Fail e | Return msg -> let (_, m) = msg in begin match m with - | BetreeMessageInsert i -> Fail - | BetreeMessageDelete -> Fail + | BetreeMessageInsert i -> Fail Failure + | BetreeMessageDelete -> Fail Failure | BetreeMessageUpsert s -> begin match betree_upsert_update_fwd prev s with - | Fail -> Fail + | Fail e -> Fail e | Return v -> begin match betree_list_pop_front_back (u64 & betree_message_t) msgs with - | Fail -> Fail + | Fail e -> Fail e | Return msgs0 -> begin match betree_node_apply_upserts_back msgs0 (Some v) key st with - | Fail -> Fail + | Fail e -> Fail e | Return msgs1 -> Return msgs1 end end @@ -459,12 +462,12 @@ let rec betree_node_apply_upserts_back end else begin match core_option_option_unwrap_fwd u64 prev st with - | Fail -> Fail + | Fail e -> Fail e | Return (_, v) -> begin match betree_list_push_front_fwd_back (u64 & betree_message_t) msgs (key, BetreeMessageInsert v) with - | Fail -> Fail + | Fail e -> Fail e | Return msgs0 -> Return msgs0 end end @@ -479,10 +482,10 @@ let rec betree_node_lookup_fwd begin match self with | BetreeNodeInternal node -> begin match betree_load_internal_node_fwd node.betree_internal_id st with - | Fail -> Fail + | Fail e -> Fail e | Return (st0, msgs) -> begin match betree_node_lookup_first_message_for_key_fwd key msgs with - | Fail -> Fail + | Fail e -> Fail e | Return pending -> begin match pending with | BetreeListCons p l -> @@ -491,12 +494,12 @@ let rec betree_node_lookup_fwd then begin match betree_internal_lookup_in_children_fwd node key st0 with - | Fail -> Fail + | Fail e -> Fail e | Return (st1, opt) -> begin match betree_node_lookup_first_message_for_key_back key msgs (BetreeListCons (k, msg) l) with - | Fail -> Fail + | Fail e -> Fail e | Return _ -> Return (st1, opt) end end @@ -506,44 +509,44 @@ let rec betree_node_lookup_fwd begin match betree_node_lookup_first_message_for_key_back key msgs (BetreeListCons (k, BetreeMessageInsert v) l) with - | Fail -> Fail + | Fail e -> Fail e | Return _ -> Return (st0, Some v) end | BetreeMessageDelete -> begin match betree_node_lookup_first_message_for_key_back key msgs (BetreeListCons (k, BetreeMessageDelete) l) with - | Fail -> Fail + | Fail e -> Fail e | Return _ -> Return (st0, None) end | BetreeMessageUpsert ufs -> begin match betree_internal_lookup_in_children_fwd node key st0 with - | Fail -> Fail + | Fail e -> Fail e | Return (st1, v) -> begin match betree_node_apply_upserts_fwd (BetreeListCons (k, BetreeMessageUpsert ufs) l) v key st1 with - | Fail -> Fail + | Fail e -> Fail e | Return (st2, v0) -> begin match betree_internal_lookup_in_children_back node key st0 with - | Fail -> Fail + | Fail e -> Fail e | Return node0 -> begin match betree_node_apply_upserts_back (BetreeListCons (k, BetreeMessageUpsert ufs) l) v key st1 with - | Fail -> Fail + | Fail e -> Fail e | Return pending0 -> begin match betree_node_lookup_first_message_for_key_back key msgs pending0 with - | Fail -> Fail + | Fail e -> Fail e | Return msgs0 -> begin match betree_store_internal_node_fwd node0.betree_internal_id msgs0 st2 with - | Fail -> Fail + | Fail e -> Fail e | Return (st3, _) -> Return (st3, Some v0) end end @@ -554,12 +557,12 @@ let rec betree_node_lookup_fwd end | BetreeListNil -> begin match betree_internal_lookup_in_children_fwd node key st0 with - | Fail -> Fail + | Fail e -> Fail e | Return (st1, opt) -> begin match betree_node_lookup_first_message_for_key_back key msgs BetreeListNil with - | Fail -> Fail + | Fail e -> Fail e | Return _ -> Return (st1, opt) end end @@ -568,10 +571,10 @@ let rec betree_node_lookup_fwd end | BetreeNodeLeaf node -> begin match betree_load_leaf_node_fwd node.betree_leaf_id st with - | Fail -> Fail + | Fail e -> Fail e | Return (st0, bindings) -> begin match betree_node_lookup_in_bindings_fwd key bindings with - | Fail -> Fail + | Fail e -> Fail e | Return opt -> Return (st0, opt) end end @@ -586,10 +589,10 @@ and betree_node_lookup_back begin match self with | BetreeNodeInternal node -> begin match betree_load_internal_node_fwd node.betree_internal_id st with - | Fail -> Fail + | Fail e -> Fail e | Return (st0, msgs) -> begin match betree_node_lookup_first_message_for_key_fwd key msgs with - | Fail -> Fail + | Fail e -> Fail e | Return pending -> begin match pending with | BetreeListCons p l -> @@ -599,11 +602,11 @@ and betree_node_lookup_back begin match betree_node_lookup_first_message_for_key_back key msgs (BetreeListCons (k, msg) l) with - | Fail -> Fail + | Fail e -> Fail e | Return _ -> begin match betree_internal_lookup_in_children_back node key st0 with - | Fail -> Fail + | Fail e -> Fail e | Return node0 -> Return (BetreeNodeInternal node0) end end @@ -613,44 +616,44 @@ and betree_node_lookup_back begin match betree_node_lookup_first_message_for_key_back key msgs (BetreeListCons (k, BetreeMessageInsert v) l) with - | Fail -> Fail + | Fail e -> Fail e | Return _ -> Return (BetreeNodeInternal node) end | BetreeMessageDelete -> begin match betree_node_lookup_first_message_for_key_back key msgs (BetreeListCons (k, BetreeMessageDelete) l) with - | Fail -> Fail + | Fail e -> Fail e | Return _ -> Return (BetreeNodeInternal node) end | BetreeMessageUpsert ufs -> begin match betree_internal_lookup_in_children_fwd node key st0 with - | Fail -> Fail + | Fail e -> Fail e | Return (st1, v) -> begin match betree_node_apply_upserts_fwd (BetreeListCons (k, BetreeMessageUpsert ufs) l) v key st1 with - | Fail -> Fail + | Fail e -> Fail e | Return (st2, _) -> begin match betree_internal_lookup_in_children_back node key st0 with - | Fail -> Fail + | Fail e -> Fail e | Return node0 -> begin match betree_node_apply_upserts_back (BetreeListCons (k, BetreeMessageUpsert ufs) l) v key st1 with - | Fail -> Fail + | Fail e -> Fail e | Return pending0 -> begin match betree_node_lookup_first_message_for_key_back key msgs pending0 with - | Fail -> Fail + | Fail e -> Fail e | Return msgs0 -> begin match betree_store_internal_node_fwd node0.betree_internal_id msgs0 st2 with - | Fail -> Fail + | Fail e -> Fail e | Return (_, _) -> Return (BetreeNodeInternal node0) end end @@ -663,11 +666,11 @@ and betree_node_lookup_back begin match betree_node_lookup_first_message_for_key_back key msgs BetreeListNil with - | Fail -> Fail + | Fail e -> Fail e | Return _ -> begin match betree_internal_lookup_in_children_back node key st0 with - | Fail -> Fail + | Fail e -> Fail e | Return node0 -> Return (BetreeNodeInternal node0) end end @@ -676,10 +679,10 @@ and betree_node_lookup_back end | BetreeNodeLeaf node -> begin match betree_load_leaf_node_fwd node.betree_leaf_id st with - | Fail -> Fail + | Fail e -> Fail e | Return (_, bindings) -> begin match betree_node_lookup_in_bindings_fwd key bindings with - | Fail -> Fail + | Fail e -> Fail e | Return _ -> Return (BetreeNodeLeaf node) end end @@ -694,12 +697,12 @@ and betree_internal_lookup_in_children_fwd if key < self.betree_internal_pivot then begin match betree_node_lookup_fwd self.betree_internal_left key st with - | Fail -> Fail + | Fail e -> Fail e | Return (st0, opt) -> Return (st0, opt) end else begin match betree_node_lookup_fwd self.betree_internal_right key st with - | Fail -> Fail + | Fail e -> Fail e | Return (st0, opt) -> Return (st0, opt) end @@ -712,14 +715,14 @@ and betree_internal_lookup_in_children_back if key < self.betree_internal_pivot then begin match betree_node_lookup_back self.betree_internal_left key st with - | Fail -> Fail + | Fail e -> Fail e | Return n -> Return (Mkbetree_internal_t self.betree_internal_id self.betree_internal_pivot n self.betree_internal_right) end else begin match betree_node_lookup_back self.betree_internal_right key st with - | Fail -> Fail + | Fail e -> Fail e | Return n -> Return (Mkbetree_internal_t self.betree_internal_id self.betree_internal_pivot self.betree_internal_left n) @@ -738,7 +741,7 @@ let rec betree_node_lookup_mut_in_bindings_fwd then Return (BetreeListCons (i, i0) tl) else begin match betree_node_lookup_mut_in_bindings_fwd key tl with - | Fail -> Fail + | Fail e -> Fail e | Return l -> Return l end | BetreeListNil -> Return BetreeListNil @@ -758,7 +761,7 @@ let rec betree_node_lookup_mut_in_bindings_back then Return ret else begin match betree_node_lookup_mut_in_bindings_back key tl ret with - | Fail -> Fail + | Fail e -> Fail e | Return tl0 -> Return (BetreeListCons (i, i0) tl0) end | BetreeListNil -> Return ret @@ -771,62 +774,62 @@ let betree_node_apply_to_leaf_fwd_back result (betree_list_t (u64 & u64)) = begin match betree_node_lookup_mut_in_bindings_fwd key bindings with - | Fail -> Fail + | Fail e -> Fail e | Return bindings0 -> begin match betree_list_head_has_key_fwd u64 bindings0 key with - | Fail -> Fail + | Fail e -> Fail e | Return b -> if b then begin match betree_list_pop_front_fwd (u64 & u64) bindings0 with - | Fail -> Fail + | Fail e -> Fail e | Return hd -> begin match new_msg with | BetreeMessageInsert v -> begin match betree_list_pop_front_back (u64 & u64) bindings0 with - | Fail -> Fail + | Fail e -> Fail e | Return bindings1 -> begin match betree_list_push_front_fwd_back (u64 & u64) bindings1 (key, v) with - | Fail -> Fail + | Fail e -> Fail e | Return bindings2 -> begin match betree_node_lookup_mut_in_bindings_back key bindings bindings2 with - | Fail -> Fail + | Fail e -> Fail e | Return bindings3 -> Return bindings3 end end end | BetreeMessageDelete -> begin match betree_list_pop_front_back (u64 & u64) bindings0 with - | Fail -> Fail + | Fail e -> Fail e | Return bindings1 -> begin match betree_node_lookup_mut_in_bindings_back key bindings bindings1 with - | Fail -> Fail + | Fail e -> Fail e | Return bindings2 -> Return bindings2 end end | BetreeMessageUpsert s -> let (_, i) = hd in begin match betree_upsert_update_fwd (Some i) s with - | Fail -> Fail + | Fail e -> Fail e | Return v -> begin match betree_list_pop_front_back (u64 & u64) bindings0 with - | Fail -> Fail + | Fail e -> Fail e | Return bindings1 -> begin match betree_list_push_front_fwd_back (u64 & u64) bindings1 (key, v) with - | Fail -> Fail + | Fail e -> Fail e | Return bindings2 -> begin match betree_node_lookup_mut_in_bindings_back key bindings bindings2 with - | Fail -> Fail + | Fail e -> Fail e | Return bindings3 -> Return bindings3 end end @@ -839,34 +842,34 @@ let betree_node_apply_to_leaf_fwd_back | BetreeMessageInsert v -> begin match betree_list_push_front_fwd_back (u64 & u64) bindings0 (key, v) with - | Fail -> Fail + | Fail e -> Fail e | Return bindings1 -> begin match betree_node_lookup_mut_in_bindings_back key bindings bindings1 with - | Fail -> Fail + | Fail e -> Fail e | Return bindings2 -> Return bindings2 end end | BetreeMessageDelete -> begin match betree_node_lookup_mut_in_bindings_back key bindings bindings0 with - | Fail -> Fail + | Fail e -> Fail e | Return bindings1 -> Return bindings1 end | BetreeMessageUpsert s -> begin match betree_upsert_update_fwd None s with - | Fail -> Fail + | Fail e -> Fail e | Return v -> begin match betree_list_push_front_fwd_back (u64 & u64) bindings0 (key, v) with - | Fail -> Fail + | Fail e -> Fail e | Return bindings1 -> begin match betree_node_lookup_mut_in_bindings_back key bindings bindings1 with - | Fail -> Fail + | Fail e -> Fail e | Return bindings2 -> Return bindings2 end end @@ -886,11 +889,11 @@ let rec betree_node_apply_messages_to_leaf_fwd_back | BetreeListCons new_msg new_msgs_tl -> let (i, m) = new_msg in begin match betree_node_apply_to_leaf_fwd_back bindings i m with - | Fail -> Fail + | Fail e -> Fail e | Return bindings0 -> begin match betree_node_apply_messages_to_leaf_fwd_back bindings0 new_msgs_tl with - | Fail -> Fail + | Fail e -> Fail e | Return bindings1 -> Return bindings1 end end @@ -911,10 +914,10 @@ let rec betree_node_filter_messages_for_key_fwd_back begin match betree_list_pop_front_back (u64 & betree_message_t) (BetreeListCons (k, m) l) with - | Fail -> Fail + | Fail e -> Fail e | Return msgs0 -> begin match betree_node_filter_messages_for_key_fwd_back key msgs0 with - | Fail -> Fail + | Fail e -> Fail e | Return msgs1 -> Return msgs1 end end @@ -935,7 +938,7 @@ let rec betree_node_lookup_first_message_after_key_fwd then begin match betree_node_lookup_first_message_after_key_fwd key next_msgs with - | Fail -> Fail + | Fail e -> Fail e | Return l -> Return l end else Return (BetreeListCons (k, m) next_msgs) @@ -956,7 +959,7 @@ let rec betree_node_lookup_first_message_after_key_back then begin match betree_node_lookup_first_message_after_key_back key next_msgs ret with - | Fail -> Fail + | Fail e -> Fail e | Return next_msgs0 -> Return (BetreeListCons (k, m) next_msgs0) end else Return ret @@ -970,10 +973,10 @@ let betree_node_apply_to_internal_fwd_back result (betree_list_t (u64 & betree_message_t)) = begin match betree_node_lookup_first_message_for_key_fwd key msgs with - | Fail -> Fail + | Fail e -> Fail e | Return msgs0 -> begin match betree_list_head_has_key_fwd betree_message_t msgs0 key with - | Fail -> Fail + | Fail e -> Fail e | Return b -> if b then @@ -981,17 +984,17 @@ let betree_node_apply_to_internal_fwd_back | BetreeMessageInsert i -> begin match betree_node_filter_messages_for_key_fwd_back key msgs0 with - | Fail -> Fail + | Fail e -> Fail e | Return msgs1 -> begin match betree_list_push_front_fwd_back (u64 & betree_message_t) msgs1 (key, BetreeMessageInsert i) with - | Fail -> Fail + | Fail e -> Fail e | Return msgs2 -> begin match betree_node_lookup_first_message_for_key_back key msgs msgs2 with - | Fail -> Fail + | Fail e -> Fail e | Return msgs3 -> Return msgs3 end end @@ -999,45 +1002,45 @@ let betree_node_apply_to_internal_fwd_back | BetreeMessageDelete -> begin match betree_node_filter_messages_for_key_fwd_back key msgs0 with - | Fail -> Fail + | Fail e -> Fail e | Return msgs1 -> begin match betree_list_push_front_fwd_back (u64 & betree_message_t) msgs1 (key, BetreeMessageDelete) with - | Fail -> Fail + | Fail e -> Fail e | Return msgs2 -> begin match betree_node_lookup_first_message_for_key_back key msgs msgs2 with - | Fail -> Fail + | Fail e -> Fail e | Return msgs3 -> Return msgs3 end end end | BetreeMessageUpsert s -> begin match betree_list_hd_fwd (u64 & betree_message_t) msgs0 with - | Fail -> Fail + | Fail e -> Fail e | Return p -> let (_, m) = p in begin match m with | BetreeMessageInsert prev -> begin match betree_upsert_update_fwd (Some prev) s with - | Fail -> Fail + | Fail e -> Fail e | Return v -> begin match betree_list_pop_front_back (u64 & betree_message_t) msgs0 with - | Fail -> Fail + | Fail e -> Fail e | Return msgs1 -> begin match betree_list_push_front_fwd_back (u64 & betree_message_t) msgs1 (key, BetreeMessageInsert v) with - | Fail -> Fail + | Fail e -> Fail e | Return msgs2 -> begin match betree_node_lookup_first_message_for_key_back key msgs msgs2 with - | Fail -> Fail + | Fail e -> Fail e | Return msgs3 -> Return msgs3 end end @@ -1045,22 +1048,22 @@ let betree_node_apply_to_internal_fwd_back end | BetreeMessageDelete -> begin match betree_upsert_update_fwd None s with - | Fail -> Fail + | Fail e -> Fail e | Return v -> begin match betree_list_pop_front_back (u64 & betree_message_t) msgs0 with - | Fail -> Fail + | Fail e -> Fail e | Return msgs1 -> begin match betree_list_push_front_fwd_back (u64 & betree_message_t) msgs1 (key, BetreeMessageInsert v) with - | Fail -> Fail + | Fail e -> Fail e | Return msgs2 -> begin match betree_node_lookup_first_message_for_key_back key msgs msgs2 with - | Fail -> Fail + | Fail e -> Fail e | Return msgs3 -> Return msgs3 end end @@ -1069,22 +1072,22 @@ let betree_node_apply_to_internal_fwd_back | BetreeMessageUpsert ufs -> begin match betree_node_lookup_first_message_after_key_fwd key msgs0 with - | Fail -> Fail + | Fail e -> Fail e | Return msgs1 -> begin match betree_list_push_front_fwd_back (u64 & betree_message_t) msgs1 (key, BetreeMessageUpsert s) with - | Fail -> Fail + | Fail e -> Fail e | Return msgs2 -> begin match betree_node_lookup_first_message_after_key_back key msgs0 msgs2 with - | Fail -> Fail + | Fail e -> Fail e | Return msgs3 -> begin match betree_node_lookup_first_message_for_key_back key msgs msgs3 with - | Fail -> Fail + | Fail e -> Fail e | Return msgs4 -> Return msgs4 end end @@ -1097,11 +1100,11 @@ let betree_node_apply_to_internal_fwd_back begin match betree_list_push_front_fwd_back (u64 & betree_message_t) msgs0 (key, new_msg) with - | Fail -> Fail + | Fail e -> Fail e | Return msgs1 -> begin match betree_node_lookup_first_message_for_key_back key msgs msgs1 with - | Fail -> Fail + | Fail e -> Fail e | Return msgs2 -> Return msgs2 end end @@ -1119,11 +1122,11 @@ let rec betree_node_apply_messages_to_internal_fwd_back | BetreeListCons new_msg new_msgs_tl -> let (i, m) = new_msg in begin match betree_node_apply_to_internal_fwd_back msgs i m with - | Fail -> Fail + | Fail e -> Fail e | Return msgs0 -> begin match betree_node_apply_messages_to_internal_fwd_back msgs0 new_msgs_tl with - | Fail -> Fail + | Fail e -> Fail e | Return msgs1 -> Return msgs1 end end @@ -1142,31 +1145,31 @@ let rec betree_node_apply_messages_fwd begin match self with | BetreeNodeInternal node -> begin match betree_load_internal_node_fwd node.betree_internal_id st with - | Fail -> Fail + | Fail e -> Fail e | Return (st0, content) -> begin match betree_node_apply_messages_to_internal_fwd_back content msgs with - | Fail -> Fail + | Fail e -> Fail e | Return content0 -> begin match betree_list_len_fwd (u64 & betree_message_t) content0 with - | Fail -> Fail + | Fail e -> Fail e | Return num_msgs -> if num_msgs >= params.betree_params_min_flush_size then begin match betree_internal_flush_fwd node params node_id_cnt content0 st0 with - | Fail -> Fail + | Fail e -> Fail e | Return (st1, content1) -> begin match betree_internal_flush_back node params node_id_cnt content0 st0 with - | Fail -> Fail + | Fail e -> Fail e | Return (node0, _) -> begin match betree_store_internal_node_fwd node0.betree_internal_id content1 st1 with - | Fail -> Fail + | Fail e -> Fail e | Return (st2, _) -> Return (st2, ()) end end @@ -1175,7 +1178,7 @@ let rec betree_node_apply_messages_fwd begin match betree_store_internal_node_fwd node.betree_internal_id content0 st0 with - | Fail -> Fail + | Fail e -> Fail e | Return (st1, _) -> Return (st1, ()) end end @@ -1183,27 +1186,27 @@ let rec betree_node_apply_messages_fwd end | BetreeNodeLeaf node -> begin match betree_load_leaf_node_fwd node.betree_leaf_id st with - | Fail -> Fail + | Fail e -> Fail e | Return (st0, content) -> begin match betree_node_apply_messages_to_leaf_fwd_back content msgs with - | Fail -> Fail + | Fail e -> Fail e | Return content0 -> begin match betree_list_len_fwd (u64 & u64) content0 with - | Fail -> Fail + | Fail e -> Fail e | Return len -> begin match u64_mul 2 params.betree_params_split_size with - | Fail -> Fail + | Fail e -> Fail e | Return i -> if len >= i then begin match betree_leaf_split_fwd node content0 params node_id_cnt st0 with - | Fail -> Fail + | Fail e -> Fail e | Return (st1, _) -> begin match betree_store_leaf_node_fwd node.betree_leaf_id BetreeListNil st1 with - | Fail -> Fail + | Fail e -> Fail e | Return (st2, _) -> Return (st2, ()) end end @@ -1211,7 +1214,7 @@ let rec betree_node_apply_messages_fwd begin match betree_store_leaf_node_fwd node.betree_leaf_id content0 st0 with - | Fail -> Fail + | Fail e -> Fail e | Return (st1, _) -> Return (st1, ()) end end @@ -1232,31 +1235,31 @@ and betree_node_apply_messages_back begin match self with | BetreeNodeInternal node -> begin match betree_load_internal_node_fwd node.betree_internal_id st with - | Fail -> Fail + | Fail e -> Fail e | Return (st0, content) -> begin match betree_node_apply_messages_to_internal_fwd_back content msgs with - | Fail -> Fail + | Fail e -> Fail e | Return content0 -> begin match betree_list_len_fwd (u64 & betree_message_t) content0 with - | Fail -> Fail + | Fail e -> Fail e | Return num_msgs -> if num_msgs >= params.betree_params_min_flush_size then begin match betree_internal_flush_fwd node params node_id_cnt content0 st0 with - | Fail -> Fail + | Fail e -> Fail e | Return (st1, content1) -> begin match betree_internal_flush_back node params node_id_cnt content0 st0 with - | Fail -> Fail + | Fail e -> Fail e | Return (node0, node_id_cnt0) -> begin match betree_store_internal_node_fwd node0.betree_internal_id content1 st1 with - | Fail -> Fail + | Fail e -> Fail e | Return (_, _) -> Return (BetreeNodeInternal node0, node_id_cnt0) end @@ -1266,7 +1269,7 @@ and betree_node_apply_messages_back begin match betree_store_internal_node_fwd node.betree_internal_id content0 st0 with - | Fail -> Fail + | Fail e -> Fail e | Return (_, _) -> Return (BetreeNodeInternal node, node_id_cnt) end end @@ -1274,32 +1277,32 @@ and betree_node_apply_messages_back end | BetreeNodeLeaf node -> begin match betree_load_leaf_node_fwd node.betree_leaf_id st with - | Fail -> Fail + | Fail e -> Fail e | Return (st0, content) -> begin match betree_node_apply_messages_to_leaf_fwd_back content msgs with - | Fail -> Fail + | Fail e -> Fail e | Return content0 -> begin match betree_list_len_fwd (u64 & u64) content0 with - | Fail -> Fail + | Fail e -> Fail e | Return len -> begin match u64_mul 2 params.betree_params_split_size with - | Fail -> Fail + | Fail e -> Fail e | Return i -> if len >= i then begin match betree_leaf_split_fwd node content0 params node_id_cnt st0 with - | Fail -> Fail + | Fail e -> Fail e | Return (st1, new_node) -> begin match betree_store_leaf_node_fwd node.betree_leaf_id BetreeListNil st1 with - | Fail -> Fail + | Fail e -> Fail e | Return (_, _) -> begin match betree_leaf_split_back node content0 params node_id_cnt st0 with - | Fail -> Fail + | Fail e -> Fail e | Return node_id_cnt0 -> Return (BetreeNodeInternal new_node, node_id_cnt0) end @@ -1309,7 +1312,7 @@ and betree_node_apply_messages_back begin match betree_store_leaf_node_fwd node.betree_leaf_id content0 st0 with - | Fail -> Fail + | Fail e -> Fail e | Return (_, _) -> Return (BetreeNodeLeaf (Mkbetree_leaf_t node.betree_leaf_id len), node_id_cnt) @@ -1332,39 +1335,39 @@ and betree_internal_flush_fwd begin match betree_list_partition_at_pivot_fwd betree_message_t content self.betree_internal_pivot with - | Fail -> Fail + | Fail e -> Fail e | Return p -> let (msgs_left, msgs_right) = p in begin match betree_list_len_fwd (u64 & betree_message_t) msgs_left with - | Fail -> Fail + | Fail e -> Fail e | Return len_left -> if len_left >= params.betree_params_min_flush_size then begin match betree_node_apply_messages_fwd self.betree_internal_left params node_id_cnt msgs_left st with - | Fail -> Fail + | Fail e -> Fail e | Return (st0, _) -> begin match betree_node_apply_messages_back self.betree_internal_left params node_id_cnt msgs_left st with - | Fail -> Fail + | Fail e -> Fail e | Return (_, node_id_cnt0) -> begin match betree_list_len_fwd (u64 & betree_message_t) msgs_right with - | Fail -> Fail + | Fail e -> Fail e | Return len_right -> if len_right >= params.betree_params_min_flush_size then begin match betree_node_apply_messages_fwd self.betree_internal_right params node_id_cnt0 msgs_right st0 with - | Fail -> Fail + | Fail e -> Fail e | Return (st1, _) -> begin match betree_node_apply_messages_back self.betree_internal_right params node_id_cnt0 msgs_right st0 with - | Fail -> Fail + | Fail e -> Fail e | Return (_, _) -> Return (st1, BetreeListNil) end end @@ -1376,12 +1379,12 @@ and betree_internal_flush_fwd begin match betree_node_apply_messages_fwd self.betree_internal_right params node_id_cnt msgs_right st with - | Fail -> Fail + | Fail e -> Fail e | Return (st0, _) -> begin match betree_node_apply_messages_back self.betree_internal_right params node_id_cnt msgs_right st with - | Fail -> Fail + | Fail e -> Fail e | Return (_, _) -> Return (st0, msgs_left) end end @@ -1400,34 +1403,34 @@ and betree_internal_flush_back begin match betree_list_partition_at_pivot_fwd betree_message_t content self.betree_internal_pivot with - | Fail -> Fail + | Fail e -> Fail e | Return p -> let (msgs_left, msgs_right) = p in begin match betree_list_len_fwd (u64 & betree_message_t) msgs_left with - | Fail -> Fail + | Fail e -> Fail e | Return len_left -> if len_left >= params.betree_params_min_flush_size then begin match betree_node_apply_messages_fwd self.betree_internal_left params node_id_cnt msgs_left st with - | Fail -> Fail + | Fail e -> Fail e | Return (st0, _) -> begin match betree_node_apply_messages_back self.betree_internal_left params node_id_cnt msgs_left st with - | Fail -> Fail + | Fail e -> Fail e | Return (n, node_id_cnt0) -> begin match betree_list_len_fwd (u64 & betree_message_t) msgs_right with - | Fail -> Fail + | Fail e -> Fail e | Return len_right -> if len_right >= params.betree_params_min_flush_size then begin match betree_node_apply_messages_back self.betree_internal_right params node_id_cnt0 msgs_right st0 with - | Fail -> Fail + | Fail e -> Fail e | Return (n0, node_id_cnt1) -> Return (Mkbetree_internal_t self.betree_internal_id self.betree_internal_pivot n n0, node_id_cnt1) @@ -1443,7 +1446,7 @@ and betree_internal_flush_back begin match betree_node_apply_messages_back self.betree_internal_right params node_id_cnt msgs_right st with - | Fail -> Fail + | Fail e -> Fail e | Return (n, node_id_cnt0) -> Return (Mkbetree_internal_t self.betree_internal_id self.betree_internal_pivot self.betree_internal_left n, @@ -1463,12 +1466,12 @@ let betree_node_apply_fwd begin match betree_node_apply_messages_fwd self params node_id_cnt (BetreeListCons (key, new_msg) l) st with - | Fail -> Fail + | Fail e -> Fail e | Return (st0, _) -> begin match betree_node_apply_messages_back self params node_id_cnt (BetreeListCons (key, new_msg) l) st with - | Fail -> Fail + | Fail e -> Fail e | Return (_, _) -> Return (st0, ()) end end @@ -1484,7 +1487,7 @@ let betree_node_apply_back begin match betree_node_apply_messages_back self params node_id_cnt (BetreeListCons (key, new_msg) l) st with - | Fail -> Fail + | Fail e -> Fail e | Return (self0, node_id_cnt0) -> Return (self0, node_id_cnt0) end @@ -1494,16 +1497,16 @@ let betree_be_tree_new_fwd result (state & betree_be_tree_t) = begin match betree_node_id_counter_new_fwd with - | Fail -> Fail + | Fail e -> Fail e | Return node_id_cnt -> begin match betree_node_id_counter_fresh_id_fwd node_id_cnt with - | Fail -> Fail + | Fail e -> Fail e | Return id -> begin match betree_store_leaf_node_fwd id BetreeListNil st with - | Fail -> Fail + | Fail e -> Fail e | Return (st0, _) -> begin match betree_node_id_counter_fresh_id_back node_id_cnt with - | Fail -> Fail + | Fail e -> Fail e | Return node_id_cnt0 -> Return (st0, Mkbetree_be_tree_t (Mkbetree_params_t min_flush_size split_size) node_id_cnt0 (BetreeNodeLeaf (Mkbetree_leaf_t id 0))) @@ -1520,13 +1523,13 @@ let betree_be_tree_apply_fwd begin match betree_node_apply_fwd self.betree_be_tree_root self.betree_be_tree_params self.betree_be_tree_node_id_cnt key msg st with - | Fail -> Fail + | Fail e -> Fail e | Return (st0, _) -> begin match betree_node_apply_back self.betree_be_tree_root self.betree_be_tree_params self.betree_be_tree_node_id_cnt key msg st with - | Fail -> Fail + | Fail e -> Fail e | Return (_, _) -> Return (st0, ()) end end @@ -1539,7 +1542,7 @@ let betree_be_tree_apply_back begin match betree_node_apply_back self.betree_be_tree_root self.betree_be_tree_params self.betree_be_tree_node_id_cnt key msg st with - | Fail -> Fail + | Fail e -> Fail e | Return (n, nic) -> Return (Mkbetree_be_tree_t self.betree_be_tree_params nic n) end @@ -1551,11 +1554,11 @@ let betree_be_tree_insert_fwd = begin match betree_be_tree_apply_fwd self key (BetreeMessageInsert value) st with - | Fail -> Fail + | Fail e -> Fail e | Return (st0, _) -> begin match betree_be_tree_apply_back self key (BetreeMessageInsert value) st with - | Fail -> Fail + | Fail e -> Fail e | Return _ -> Return (st0, ()) end end @@ -1567,7 +1570,7 @@ let betree_be_tree_insert_back = begin match betree_be_tree_apply_back self key (BetreeMessageInsert value) st with - | Fail -> Fail + | Fail e -> Fail e | Return self0 -> Return self0 end @@ -1575,10 +1578,10 @@ let betree_be_tree_insert_back let betree_be_tree_delete_fwd (self : betree_be_tree_t) (key : u64) (st : state) : result (state & unit) = begin match betree_be_tree_apply_fwd self key BetreeMessageDelete st with - | Fail -> Fail + | Fail e -> Fail e | Return (st0, _) -> begin match betree_be_tree_apply_back self key BetreeMessageDelete st with - | Fail -> Fail + | Fail e -> Fail e | Return _ -> Return (st0, ()) end end @@ -1589,7 +1592,7 @@ let betree_be_tree_delete_back result betree_be_tree_t = begin match betree_be_tree_apply_back self key BetreeMessageDelete st with - | Fail -> Fail + | Fail e -> Fail e | Return self0 -> Return self0 end @@ -1601,11 +1604,11 @@ let betree_be_tree_upsert_fwd = begin match betree_be_tree_apply_fwd self key (BetreeMessageUpsert upd) st with - | Fail -> Fail + | Fail e -> Fail e | Return (st0, _) -> begin match betree_be_tree_apply_back self key (BetreeMessageUpsert upd) st with - | Fail -> Fail + | Fail e -> Fail e | Return _ -> Return (st0, ()) end end @@ -1618,7 +1621,7 @@ let betree_be_tree_upsert_back = begin match betree_be_tree_apply_back self key (BetreeMessageUpsert upd) st with - | Fail -> Fail + | Fail e -> Fail e | Return self0 -> Return self0 end @@ -1628,7 +1631,7 @@ let betree_be_tree_lookup_fwd result (state & (option u64)) = begin match betree_node_lookup_fwd self.betree_be_tree_root key st with - | Fail -> Fail + | Fail e -> Fail e | Return (st0, opt) -> Return (st0, opt) end @@ -1638,7 +1641,7 @@ let betree_be_tree_lookup_back result betree_be_tree_t = begin match betree_node_lookup_back self.betree_be_tree_root key st with - | Fail -> Fail + | Fail e -> Fail e | Return n -> Return (Mkbetree_be_tree_t self.betree_be_tree_params self.betree_be_tree_node_id_cnt n) diff --git a/tests/fstar/betree/Primitives.fst b/tests/fstar/betree/Primitives.fst index 96138e46..82622656 100644 --- a/tests/fstar/betree/Primitives.fst +++ b/tests/fstar/betree/Primitives.fst @@ -18,9 +18,13 @@ let rec list_update #a ls i x = #pop-options (*** Result *) +type error : Type0 = +| Failure +| OutOfFuel + type result (a : Type0) : Type0 = | Return : v:a -> result a -| Fail : result a +| Fail : e:error -> result a // Monadic bind and return. // Re-definining those allows us to customize the result of the monadic notations @@ -29,10 +33,10 @@ let return (#a : Type0) (x:a) : result a = Return x let bind (#a #b : Type0) (m : result a) (f : a -> result b) : result b = match m with | Return x -> f x - | Fail -> Fail + | Fail e -> Fail e // Monadic assert(...) -let massert (b:bool) : result unit = if b then Return () else Fail +let massert (b:bool) : result unit = if b then Return () else Fail Failure // Normalize and unwrap a successful result (used for globals). let eval_global (#a : Type0) (x : result a{Return? (normalize_term x)}) : a = Return?.v x @@ -119,12 +123,12 @@ let scalar_max (ty : scalar_ty) : int = type scalar (ty : scalar_ty) : eqtype = x:int{scalar_min ty <= x && x <= scalar_max ty} let mk_scalar (ty : scalar_ty) (x : int) : result (scalar ty) = - if scalar_min ty <= x && scalar_max ty >= x then Return x else Fail + if scalar_min ty <= x && scalar_max ty >= x then Return x else Fail Failure let scalar_neg (#ty : scalar_ty) (x : scalar ty) : result (scalar ty) = mk_scalar ty (-x) let scalar_div (#ty : scalar_ty) (x : scalar ty) (y : scalar ty) : result (scalar ty) = - if y <> 0 then mk_scalar ty (x / y) else Fail + if y <> 0 then mk_scalar ty (x / y) else Fail Failure /// The remainder operation let int_rem (x : int) (y : int{y <> 0}) : int = @@ -137,7 +141,7 @@ let _ = assert_norm(int_rem 1 (-2) = 1) let _ = assert_norm(int_rem (-1) (-2) = -1) let scalar_rem (#ty : scalar_ty) (x : scalar ty) (y : scalar ty) : result (scalar ty) = - if y <> 0 then mk_scalar ty (int_rem x y) else Fail + if y <> 0 then mk_scalar ty (int_rem x y) else Fail Failure let scalar_add (#ty : scalar_ty) (x : scalar ty) (y : scalar ty) : result (scalar ty) = mk_scalar ty (x + y) @@ -258,7 +262,7 @@ let vec_push_back (a : Type0) (v : vec a) (x : a) : (requires True) (ensures (fun res -> match res with - | Fail -> True + | Fail e -> e == Failure | Return v' -> length v' = length v + 1)) = if length v < usize_max then begin (**) assert_norm(length [x] == 1); @@ -266,22 +270,22 @@ let vec_push_back (a : Type0) (v : vec a) (x : a) : (**) assert(length (append v [x]) = length v + 1); Return (append v [x]) end - else Fail + else Fail Failure // The **forward** function shouldn't be used let vec_insert_fwd (a : Type0) (v : vec a) (i : usize) (x : a) : result unit = - if i < length v then Return () else Fail + if i < length v then Return () else Fail Failure let vec_insert_back (a : Type0) (v : vec a) (i : usize) (x : a) : result (vec a) = - if i < length v then Return (list_update v i x) else Fail + if i < length v then Return (list_update v i x) else Fail Failure // The **backward** function shouldn't be used let vec_index_fwd (a : Type0) (v : vec a) (i : usize) : result a = - if i < length v then Return (index v i) else Fail + if i < length v then Return (index v i) else Fail Failure let vec_index_back (a : Type0) (v : vec a) (i : usize) (x : a) : result unit = - if i < length v then Return () else Fail + if i < length v then Return () else Fail Failure let vec_index_mut_fwd (a : Type0) (v : vec a) (i : usize) : result a = - if i < length v then Return (index v i) else Fail + if i < length v then Return (index v i) else Fail Failure let vec_index_mut_back (a : Type0) (v : vec a) (i : usize) (nx : a) : result (vec a) = - if i < length v then Return (list_update v i nx) else Fail + if i < length v then Return (list_update v i nx) else Fail Failure diff --git a/tests/fstar/betree_back_stateful/BetreeMain.Funs.fst b/tests/fstar/betree_back_stateful/BetreeMain.Funs.fst index eebed6e6..6a2b7c09 100644 --- a/tests/fstar/betree_back_stateful/BetreeMain.Funs.fst +++ b/tests/fstar/betree_back_stateful/BetreeMain.Funs.fst @@ -14,7 +14,7 @@ let betree_load_internal_node_fwd result (state & (betree_list_t (u64 & betree_message_t))) = begin match betree_utils_load_internal_node_fwd id st with - | Fail -> Fail + | Fail e -> Fail e | Return (st0, l) -> Return (st0, l) end @@ -24,7 +24,7 @@ let betree_store_internal_node_fwd result (state & unit) = begin match betree_utils_store_internal_node_fwd id content st with - | Fail -> Fail + | Fail e -> Fail e | Return (st0, _) -> Return (st0, ()) end @@ -32,7 +32,7 @@ let betree_store_internal_node_fwd let betree_load_leaf_node_fwd (id : u64) (st : state) : result (state & (betree_list_t (u64 & u64))) = begin match betree_utils_load_leaf_node_fwd id st with - | Fail -> Fail + | Fail e -> Fail e | Return (st0, l) -> Return (st0, l) end @@ -42,21 +42,21 @@ let betree_store_leaf_node_fwd result (state & unit) = begin match betree_utils_store_leaf_node_fwd id content st with - | Fail -> Fail + | Fail e -> Fail e | Return (st0, _) -> Return (st0, ()) end (** [betree_main::betree::fresh_node_id] *) let betree_fresh_node_id_fwd (counter : u64) : result u64 = begin match u64_add counter 1 with - | Fail -> Fail + | Fail e -> Fail e | Return _ -> Return counter end (** [betree_main::betree::fresh_node_id] *) let betree_fresh_node_id_back (counter : u64) : result u64 = begin match u64_add counter 1 with - | Fail -> Fail + | Fail e -> Fail e | Return counter0 -> Return counter0 end @@ -68,7 +68,7 @@ let betree_node_id_counter_new_fwd : result betree_node_id_counter_t = let betree_node_id_counter_fresh_id_fwd (self : betree_node_id_counter_t) : result u64 = begin match u64_add self.betree_node_id_counter_next_node_id 1 with - | Fail -> Fail + | Fail e -> Fail e | Return _ -> Return self.betree_node_id_counter_next_node_id end @@ -76,7 +76,7 @@ let betree_node_id_counter_fresh_id_fwd let betree_node_id_counter_fresh_id_back (self : betree_node_id_counter_t) : result betree_node_id_counter_t = begin match u64_add self.betree_node_id_counter_next_node_id 1 with - | Fail -> Fail + | Fail e -> Fail e | Return i -> Return (Mkbetree_node_id_counter_t i) end @@ -97,12 +97,12 @@ let betree_upsert_update_fwd begin match st with | BetreeUpsertFunStateAdd v -> begin match u64_sub core_num_u64_max_c prev0 with - | Fail -> Fail + | Fail e -> Fail e | Return margin -> if margin >= v then begin match u64_add prev0 v with - | Fail -> Fail + | Fail e -> Fail e | Return i -> Return i end else Return core_num_u64_max_c @@ -111,7 +111,7 @@ let betree_upsert_update_fwd if prev0 >= v then begin match u64_sub prev0 v with - | Fail -> Fail + | Fail e -> Fail e | Return i -> Return i end else Return 0 @@ -126,9 +126,12 @@ let rec betree_list_len_fwd begin match self with | BetreeListCons x tl -> begin match betree_list_len_fwd t tl with - | Fail -> Fail + | Fail e -> Fail e | Return i -> - begin match u64_add 1 i with | Fail -> Fail | Return i0 -> Return i0 end + begin match u64_add 1 i with + | Fail e -> Fail e + | Return i0 -> Return i0 + end end | BetreeListNil -> Return 0 end @@ -145,17 +148,17 @@ let rec betree_list_split_at_fwd begin match self with | BetreeListCons hd tl -> begin match u64_sub n 1 with - | Fail -> Fail + | Fail e -> Fail e | Return i -> begin match betree_list_split_at_fwd t tl i with - | Fail -> Fail + | Fail e -> Fail e | Return p -> let (ls0, ls1) = p in let l = ls0 in Return (BetreeListCons hd l, ls1) end end - | BetreeListNil -> Fail + | BetreeListNil -> Fail Failure end (** [betree_main::betree::List::{1}::push_front] *) @@ -170,7 +173,7 @@ let betree_list_pop_front_fwd (t : Type0) (self : betree_list_t t) : result t = let ls = mem_replace_fwd (betree_list_t t) self BetreeListNil in begin match ls with | BetreeListCons x tl -> Return x - | BetreeListNil -> Fail + | BetreeListNil -> Fail Failure end (** [betree_main::betree::List::{1}::pop_front] *) @@ -179,14 +182,14 @@ let betree_list_pop_front_back let ls = mem_replace_fwd (betree_list_t t) self BetreeListNil in begin match ls with | BetreeListCons x tl -> Return tl - | BetreeListNil -> Fail + | BetreeListNil -> Fail Failure end (** [betree_main::betree::List::{1}::hd] *) let betree_list_hd_fwd (t : Type0) (self : betree_list_t t) : result t = begin match self with | BetreeListCons hd l -> Return hd - | BetreeListNil -> Fail + | BetreeListNil -> Fail Failure end (** [betree_main::betree::List::{2}::head_has_key] *) @@ -210,7 +213,7 @@ let rec betree_list_partition_at_pivot_fwd then Return (BetreeListNil, BetreeListCons (i, x) tl) else begin match betree_list_partition_at_pivot_fwd t tl pivot with - | Fail -> Fail + | Fail e -> Fail e | Return p -> let (ls0, ls1) = p in let l = ls0 in @@ -229,27 +232,27 @@ let betree_leaf_split_fwd begin match betree_list_split_at_fwd (u64 & u64) content params.betree_params_split_size with - | Fail -> Fail + | Fail e -> Fail e | Return p -> let (content0, content1) = p in begin match betree_list_hd_fwd (u64 & u64) content1 with - | Fail -> Fail + | Fail e -> Fail e | Return p0 -> let (pivot, _) = p0 in begin match betree_node_id_counter_fresh_id_fwd node_id_cnt with - | Fail -> Fail + | Fail e -> Fail e | Return id0 -> begin match betree_node_id_counter_fresh_id_back node_id_cnt with - | Fail -> Fail + | Fail e -> Fail e | Return node_id_cnt0 -> begin match betree_node_id_counter_fresh_id_fwd node_id_cnt0 with - | Fail -> Fail + | Fail e -> Fail e | Return id1 -> begin match betree_store_leaf_node_fwd id0 content0 st with - | Fail -> Fail + | Fail e -> Fail e | Return (st0, _) -> begin match betree_store_leaf_node_fwd id1 content1 st0 with - | Fail -> Fail + | Fail e -> Fail e | Return (st1, _) -> let n = BetreeNodeLeaf (Mkbetree_leaf_t id0 params.betree_params_split_size) in @@ -275,26 +278,26 @@ let betree_leaf_split_back0 begin match betree_list_split_at_fwd (u64 & u64) content params.betree_params_split_size with - | Fail -> Fail + | Fail e -> Fail e | Return p -> let (content0, content1) = p in begin match betree_list_hd_fwd (u64 & u64) content1 with - | Fail -> Fail + | Fail e -> Fail e | Return _ -> begin match betree_node_id_counter_fresh_id_fwd node_id_cnt with - | Fail -> Fail + | Fail e -> Fail e | Return id0 -> begin match betree_node_id_counter_fresh_id_back node_id_cnt with - | Fail -> Fail + | Fail e -> Fail e | Return node_id_cnt0 -> begin match betree_node_id_counter_fresh_id_fwd node_id_cnt0 with - | Fail -> Fail + | Fail e -> Fail e | Return id1 -> begin match betree_store_leaf_node_fwd id0 content0 st with - | Fail -> Fail + | Fail e -> Fail e | Return (st1, _) -> begin match betree_store_leaf_node_fwd id1 content1 st1 with - | Fail -> Fail + | Fail e -> Fail e | Return (_, _) -> Return (st0, ()) end end @@ -314,26 +317,26 @@ let betree_leaf_split_back1 begin match betree_list_split_at_fwd (u64 & u64) content params.betree_params_split_size with - | Fail -> Fail + | Fail e -> Fail e | Return p -> let (content0, content1) = p in begin match betree_list_hd_fwd (u64 & u64) content1 with - | Fail -> Fail + | Fail e -> Fail e | Return _ -> begin match betree_node_id_counter_fresh_id_fwd node_id_cnt with - | Fail -> Fail + | Fail e -> Fail e | Return id0 -> begin match betree_node_id_counter_fresh_id_back node_id_cnt with - | Fail -> Fail + | Fail e -> Fail e | Return node_id_cnt0 -> begin match betree_node_id_counter_fresh_id_fwd node_id_cnt0 with - | Fail -> Fail + | Fail e -> Fail e | Return id1 -> begin match betree_store_leaf_node_fwd id0 content0 st with - | Fail -> Fail + | Fail e -> Fail e | Return (st1, _) -> begin match betree_store_leaf_node_fwd id1 content1 st1 with - | Fail -> Fail + | Fail e -> Fail e | Return (_, _) -> Return (st0, ()) end end @@ -353,30 +356,30 @@ let betree_leaf_split_back2 begin match betree_list_split_at_fwd (u64 & u64) content params.betree_params_split_size with - | Fail -> Fail + | Fail e -> Fail e | Return p -> let (content0, content1) = p in begin match betree_list_hd_fwd (u64 & u64) content1 with - | Fail -> Fail + | Fail e -> Fail e | Return _ -> begin match betree_node_id_counter_fresh_id_fwd node_id_cnt with - | Fail -> Fail + | Fail e -> Fail e | Return id0 -> begin match betree_node_id_counter_fresh_id_back node_id_cnt with - | Fail -> Fail + | Fail e -> Fail e | Return node_id_cnt0 -> begin match betree_node_id_counter_fresh_id_fwd node_id_cnt0 with - | Fail -> Fail + | Fail e -> Fail e | Return id1 -> begin match betree_store_leaf_node_fwd id0 content0 st with - | Fail -> Fail + | Fail e -> Fail e | Return (st1, _) -> begin match betree_store_leaf_node_fwd id1 content1 st1 with - | Fail -> Fail + | Fail e -> Fail e | Return (_, _) -> begin match betree_node_id_counter_fresh_id_back node_id_cnt0 with - | Fail -> Fail + | Fail e -> Fail e | Return node_id_cnt1 -> Return (st0, node_id_cnt1) end end @@ -403,7 +406,7 @@ let rec betree_node_lookup_in_bindings_fwd then Return None else begin match betree_node_lookup_in_bindings_fwd key tl with - | Fail -> Fail + | Fail e -> Fail e | Return opt -> Return opt end | BetreeListNil -> Return None @@ -423,7 +426,7 @@ let rec betree_node_lookup_first_message_for_key_fwd else begin match betree_node_lookup_first_message_for_key_fwd key next_msgs with - | Fail -> Fail + | Fail e -> Fail e | Return l -> Return l end | BetreeListNil -> Return BetreeListNil @@ -444,7 +447,7 @@ let rec betree_node_lookup_first_message_for_key_back else begin match betree_node_lookup_first_message_for_key_back key next_msgs ret with - | Fail -> Fail + | Fail e -> Fail e | Return next_msgs0 -> Return (BetreeListCons (i, m) next_msgs0) end | BetreeListNil -> Return ret @@ -458,28 +461,28 @@ let rec betree_node_apply_upserts_fwd (decreases (betree_node_apply_upserts_decreases msgs prev key st)) = begin match betree_list_head_has_key_fwd betree_message_t msgs key with - | Fail -> Fail + | Fail e -> Fail e | Return b -> if b then begin match betree_list_pop_front_fwd (u64 & betree_message_t) msgs with - | Fail -> Fail + | Fail e -> Fail e | Return msg -> let (_, m) = msg in begin match m with - | BetreeMessageInsert i -> Fail - | BetreeMessageDelete -> Fail + | BetreeMessageInsert i -> Fail Failure + | BetreeMessageDelete -> Fail Failure | BetreeMessageUpsert s -> begin match betree_upsert_update_fwd prev s with - | Fail -> Fail + | Fail e -> Fail e | Return v -> begin match betree_list_pop_front_back (u64 & betree_message_t) msgs with - | Fail -> Fail + | Fail e -> Fail e | Return msgs0 -> begin match betree_node_apply_upserts_fwd msgs0 (Some v) key st with - | Fail -> Fail + | Fail e -> Fail e | Return (st0, i) -> Return (st0, i) end end @@ -488,12 +491,12 @@ let rec betree_node_apply_upserts_fwd end else begin match core_option_option_unwrap_fwd u64 prev st with - | Fail -> Fail + | Fail e -> Fail e | Return (st0, v) -> begin match betree_list_push_front_fwd_back (u64 & betree_message_t) msgs (key, BetreeMessageInsert v) with - | Fail -> Fail + | Fail e -> Fail e | Return _ -> Return (st0, v) end end @@ -507,28 +510,28 @@ let rec betree_node_apply_upserts_back (decreases (betree_node_apply_upserts_decreases msgs prev key st)) = begin match betree_list_head_has_key_fwd betree_message_t msgs key with - | Fail -> Fail + | Fail e -> Fail e | Return b -> if b then begin match betree_list_pop_front_fwd (u64 & betree_message_t) msgs with - | Fail -> Fail + | Fail e -> Fail e | Return msg -> let (_, m) = msg in begin match m with - | BetreeMessageInsert i -> Fail - | BetreeMessageDelete -> Fail + | BetreeMessageInsert i -> Fail Failure + | BetreeMessageDelete -> Fail Failure | BetreeMessageUpsert s -> begin match betree_upsert_update_fwd prev s with - | Fail -> Fail + | Fail e -> Fail e | Return v -> begin match betree_list_pop_front_back (u64 & betree_message_t) msgs with - | Fail -> Fail + | Fail e -> Fail e | Return msgs0 -> begin match betree_node_apply_upserts_back msgs0 (Some v) key st st0 with - | Fail -> Fail + | Fail e -> Fail e | Return (st1, msgs1) -> Return (st1, msgs1) end end @@ -537,12 +540,12 @@ let rec betree_node_apply_upserts_back end else begin match core_option_option_unwrap_fwd u64 prev st with - | Fail -> Fail + | Fail e -> Fail e | Return (_, v) -> begin match betree_list_push_front_fwd_back (u64 & betree_message_t) msgs (key, BetreeMessageInsert v) with - | Fail -> Fail + | Fail e -> Fail e | Return msgs0 -> Return (st0, msgs0) end end @@ -557,10 +560,10 @@ let rec betree_node_lookup_fwd begin match self with | BetreeNodeInternal node -> begin match betree_load_internal_node_fwd node.betree_internal_id st with - | Fail -> Fail + | Fail e -> Fail e | Return (st0, msgs) -> begin match betree_node_lookup_first_message_for_key_fwd key msgs with - | Fail -> Fail + | Fail e -> Fail e | Return pending -> begin match pending with | BetreeListCons p l -> @@ -569,12 +572,12 @@ let rec betree_node_lookup_fwd then begin match betree_internal_lookup_in_children_fwd node key st0 with - | Fail -> Fail + | Fail e -> Fail e | Return (st1, opt) -> begin match betree_node_lookup_first_message_for_key_back key msgs (BetreeListCons (k, msg) l) with - | Fail -> Fail + | Fail e -> Fail e | Return _ -> Return (st1, opt) end end @@ -584,45 +587,45 @@ let rec betree_node_lookup_fwd begin match betree_node_lookup_first_message_for_key_back key msgs (BetreeListCons (k, BetreeMessageInsert v) l) with - | Fail -> Fail + | Fail e -> Fail e | Return _ -> Return (st0, Some v) end | BetreeMessageDelete -> begin match betree_node_lookup_first_message_for_key_back key msgs (BetreeListCons (k, BetreeMessageDelete) l) with - | Fail -> Fail + | Fail e -> Fail e | Return _ -> Return (st0, None) end | BetreeMessageUpsert ufs -> begin match betree_internal_lookup_in_children_fwd node key st0 with - | Fail -> Fail + | Fail e -> Fail e | Return (st1, v) -> begin match betree_node_apply_upserts_fwd (BetreeListCons (k, BetreeMessageUpsert ufs) l) v key st1 with - | Fail -> Fail + | Fail e -> Fail e | Return (st2, v0) -> begin match betree_internal_lookup_in_children_back node key st0 st2 with - | Fail -> Fail + | Fail e -> Fail e | Return (st3, node0) -> begin match betree_node_apply_upserts_back (BetreeListCons (k, BetreeMessageUpsert ufs) l) v key st1 st3 with - | Fail -> Fail + | Fail e -> Fail e | Return (st4, pending0) -> begin match betree_node_lookup_first_message_for_key_back key msgs pending0 with - | Fail -> Fail + | Fail e -> Fail e | Return msgs0 -> begin match betree_store_internal_node_fwd node0.betree_internal_id msgs0 st4 with - | Fail -> Fail + | Fail e -> Fail e | Return (st5, _) -> Return (st5, Some v0) end end @@ -633,12 +636,12 @@ let rec betree_node_lookup_fwd end | BetreeListNil -> begin match betree_internal_lookup_in_children_fwd node key st0 with - | Fail -> Fail + | Fail e -> Fail e | Return (st1, opt) -> begin match betree_node_lookup_first_message_for_key_back key msgs BetreeListNil with - | Fail -> Fail + | Fail e -> Fail e | Return _ -> Return (st1, opt) end end @@ -647,10 +650,10 @@ let rec betree_node_lookup_fwd end | BetreeNodeLeaf node -> begin match betree_load_leaf_node_fwd node.betree_leaf_id st with - | Fail -> Fail + | Fail e -> Fail e | Return (st0, bindings) -> begin match betree_node_lookup_in_bindings_fwd key bindings with - | Fail -> Fail + | Fail e -> Fail e | Return opt -> Return (st0, opt) end end @@ -665,10 +668,10 @@ and betree_node_lookup_back begin match self with | BetreeNodeInternal node -> begin match betree_load_internal_node_fwd node.betree_internal_id st with - | Fail -> Fail + | Fail e -> Fail e | Return (st1, msgs) -> begin match betree_node_lookup_first_message_for_key_fwd key msgs with - | Fail -> Fail + | Fail e -> Fail e | Return pending -> begin match pending with | BetreeListCons p l -> @@ -678,11 +681,11 @@ and betree_node_lookup_back begin match betree_node_lookup_first_message_for_key_back key msgs (BetreeListCons (k, msg) l) with - | Fail -> Fail + | Fail e -> Fail e | Return _ -> begin match betree_internal_lookup_in_children_back node key st1 st0 with - | Fail -> Fail + | Fail e -> Fail e | Return (st2, node0) -> Return (st2, BetreeNodeInternal node0) end end @@ -692,45 +695,45 @@ and betree_node_lookup_back begin match betree_node_lookup_first_message_for_key_back key msgs (BetreeListCons (k, BetreeMessageInsert v) l) with - | Fail -> Fail + | Fail e -> Fail e | Return _ -> Return (st0, BetreeNodeInternal node) end | BetreeMessageDelete -> begin match betree_node_lookup_first_message_for_key_back key msgs (BetreeListCons (k, BetreeMessageDelete) l) with - | Fail -> Fail + | Fail e -> Fail e | Return _ -> Return (st0, BetreeNodeInternal node) end | BetreeMessageUpsert ufs -> begin match betree_internal_lookup_in_children_fwd node key st1 with - | Fail -> Fail + | Fail e -> Fail e | Return (st2, v) -> begin match betree_node_apply_upserts_fwd (BetreeListCons (k, BetreeMessageUpsert ufs) l) v key st2 with - | Fail -> Fail + | Fail e -> Fail e | Return (st3, _) -> begin match betree_internal_lookup_in_children_back node key st1 st3 with - | Fail -> Fail + | Fail e -> Fail e | Return (st4, node0) -> begin match betree_node_apply_upserts_back (BetreeListCons (k, BetreeMessageUpsert ufs) l) v key st2 st4 with - | Fail -> Fail + | Fail e -> Fail e | Return (st5, pending0) -> begin match betree_node_lookup_first_message_for_key_back key msgs pending0 with - | Fail -> Fail + | Fail e -> Fail e | Return msgs0 -> begin match betree_store_internal_node_fwd node0.betree_internal_id msgs0 st5 with - | Fail -> Fail + | Fail e -> Fail e | Return (_, _) -> Return (st0, BetreeNodeInternal node0) end @@ -744,11 +747,11 @@ and betree_node_lookup_back begin match betree_node_lookup_first_message_for_key_back key msgs BetreeListNil with - | Fail -> Fail + | Fail e -> Fail e | Return _ -> begin match betree_internal_lookup_in_children_back node key st1 st0 with - | Fail -> Fail + | Fail e -> Fail e | Return (st2, node0) -> Return (st2, BetreeNodeInternal node0) end end @@ -757,10 +760,10 @@ and betree_node_lookup_back end | BetreeNodeLeaf node -> begin match betree_load_leaf_node_fwd node.betree_leaf_id st with - | Fail -> Fail + | Fail e -> Fail e | Return (_, bindings) -> begin match betree_node_lookup_in_bindings_fwd key bindings with - | Fail -> Fail + | Fail e -> Fail e | Return _ -> Return (st0, BetreeNodeLeaf node) end end @@ -775,12 +778,12 @@ and betree_internal_lookup_in_children_fwd if key < self.betree_internal_pivot then begin match betree_node_lookup_fwd self.betree_internal_left key st with - | Fail -> Fail + | Fail e -> Fail e | Return (st0, opt) -> Return (st0, opt) end else begin match betree_node_lookup_fwd self.betree_internal_right key st with - | Fail -> Fail + | Fail e -> Fail e | Return (st0, opt) -> Return (st0, opt) end @@ -794,7 +797,7 @@ and betree_internal_lookup_in_children_back then begin match betree_node_lookup_back self.betree_internal_left key st st0 with - | Fail -> Fail + | Fail e -> Fail e | Return (st1, n) -> Return (st1, Mkbetree_internal_t self.betree_internal_id self.betree_internal_pivot n self.betree_internal_right) @@ -802,7 +805,7 @@ and betree_internal_lookup_in_children_back else begin match betree_node_lookup_back self.betree_internal_right key st st0 with - | Fail -> Fail + | Fail e -> Fail e | Return (st1, n) -> Return (st1, Mkbetree_internal_t self.betree_internal_id self.betree_internal_pivot self.betree_internal_left n) @@ -821,7 +824,7 @@ let rec betree_node_lookup_mut_in_bindings_fwd then Return (BetreeListCons (i, i0) tl) else begin match betree_node_lookup_mut_in_bindings_fwd key tl with - | Fail -> Fail + | Fail e -> Fail e | Return l -> Return l end | BetreeListNil -> Return BetreeListNil @@ -841,7 +844,7 @@ let rec betree_node_lookup_mut_in_bindings_back then Return ret else begin match betree_node_lookup_mut_in_bindings_back key tl ret with - | Fail -> Fail + | Fail e -> Fail e | Return tl0 -> Return (BetreeListCons (i, i0) tl0) end | BetreeListNil -> Return ret @@ -854,62 +857,62 @@ let betree_node_apply_to_leaf_fwd_back result (betree_list_t (u64 & u64)) = begin match betree_node_lookup_mut_in_bindings_fwd key bindings with - | Fail -> Fail + | Fail e -> Fail e | Return bindings0 -> begin match betree_list_head_has_key_fwd u64 bindings0 key with - | Fail -> Fail + | Fail e -> Fail e | Return b -> if b then begin match betree_list_pop_front_fwd (u64 & u64) bindings0 with - | Fail -> Fail + | Fail e -> Fail e | Return hd -> begin match new_msg with | BetreeMessageInsert v -> begin match betree_list_pop_front_back (u64 & u64) bindings0 with - | Fail -> Fail + | Fail e -> Fail e | Return bindings1 -> begin match betree_list_push_front_fwd_back (u64 & u64) bindings1 (key, v) with - | Fail -> Fail + | Fail e -> Fail e | Return bindings2 -> begin match betree_node_lookup_mut_in_bindings_back key bindings bindings2 with - | Fail -> Fail + | Fail e -> Fail e | Return bindings3 -> Return bindings3 end end end | BetreeMessageDelete -> begin match betree_list_pop_front_back (u64 & u64) bindings0 with - | Fail -> Fail + | Fail e -> Fail e | Return bindings1 -> begin match betree_node_lookup_mut_in_bindings_back key bindings bindings1 with - | Fail -> Fail + | Fail e -> Fail e | Return bindings2 -> Return bindings2 end end | BetreeMessageUpsert s -> let (_, i) = hd in begin match betree_upsert_update_fwd (Some i) s with - | Fail -> Fail + | Fail e -> Fail e | Return v -> begin match betree_list_pop_front_back (u64 & u64) bindings0 with - | Fail -> Fail + | Fail e -> Fail e | Return bindings1 -> begin match betree_list_push_front_fwd_back (u64 & u64) bindings1 (key, v) with - | Fail -> Fail + | Fail e -> Fail e | Return bindings2 -> begin match betree_node_lookup_mut_in_bindings_back key bindings bindings2 with - | Fail -> Fail + | Fail e -> Fail e | Return bindings3 -> Return bindings3 end end @@ -922,34 +925,34 @@ let betree_node_apply_to_leaf_fwd_back | BetreeMessageInsert v -> begin match betree_list_push_front_fwd_back (u64 & u64) bindings0 (key, v) with - | Fail -> Fail + | Fail e -> Fail e | Return bindings1 -> begin match betree_node_lookup_mut_in_bindings_back key bindings bindings1 with - | Fail -> Fail + | Fail e -> Fail e | Return bindings2 -> Return bindings2 end end | BetreeMessageDelete -> begin match betree_node_lookup_mut_in_bindings_back key bindings bindings0 with - | Fail -> Fail + | Fail e -> Fail e | Return bindings1 -> Return bindings1 end | BetreeMessageUpsert s -> begin match betree_upsert_update_fwd None s with - | Fail -> Fail + | Fail e -> Fail e | Return v -> begin match betree_list_push_front_fwd_back (u64 & u64) bindings0 (key, v) with - | Fail -> Fail + | Fail e -> Fail e | Return bindings1 -> begin match betree_node_lookup_mut_in_bindings_back key bindings bindings1 with - | Fail -> Fail + | Fail e -> Fail e | Return bindings2 -> Return bindings2 end end @@ -969,11 +972,11 @@ let rec betree_node_apply_messages_to_leaf_fwd_back | BetreeListCons new_msg new_msgs_tl -> let (i, m) = new_msg in begin match betree_node_apply_to_leaf_fwd_back bindings i m with - | Fail -> Fail + | Fail e -> Fail e | Return bindings0 -> begin match betree_node_apply_messages_to_leaf_fwd_back bindings0 new_msgs_tl with - | Fail -> Fail + | Fail e -> Fail e | Return bindings1 -> Return bindings1 end end @@ -994,10 +997,10 @@ let rec betree_node_filter_messages_for_key_fwd_back begin match betree_list_pop_front_back (u64 & betree_message_t) (BetreeListCons (k, m) l) with - | Fail -> Fail + | Fail e -> Fail e | Return msgs0 -> begin match betree_node_filter_messages_for_key_fwd_back key msgs0 with - | Fail -> Fail + | Fail e -> Fail e | Return msgs1 -> Return msgs1 end end @@ -1018,7 +1021,7 @@ let rec betree_node_lookup_first_message_after_key_fwd then begin match betree_node_lookup_first_message_after_key_fwd key next_msgs with - | Fail -> Fail + | Fail e -> Fail e | Return l -> Return l end else Return (BetreeListCons (k, m) next_msgs) @@ -1039,7 +1042,7 @@ let rec betree_node_lookup_first_message_after_key_back then begin match betree_node_lookup_first_message_after_key_back key next_msgs ret with - | Fail -> Fail + | Fail e -> Fail e | Return next_msgs0 -> Return (BetreeListCons (k, m) next_msgs0) end else Return ret @@ -1053,10 +1056,10 @@ let betree_node_apply_to_internal_fwd_back result (betree_list_t (u64 & betree_message_t)) = begin match betree_node_lookup_first_message_for_key_fwd key msgs with - | Fail -> Fail + | Fail e -> Fail e | Return msgs0 -> begin match betree_list_head_has_key_fwd betree_message_t msgs0 key with - | Fail -> Fail + | Fail e -> Fail e | Return b -> if b then @@ -1064,17 +1067,17 @@ let betree_node_apply_to_internal_fwd_back | BetreeMessageInsert i -> begin match betree_node_filter_messages_for_key_fwd_back key msgs0 with - | Fail -> Fail + | Fail e -> Fail e | Return msgs1 -> begin match betree_list_push_front_fwd_back (u64 & betree_message_t) msgs1 (key, BetreeMessageInsert i) with - | Fail -> Fail + | Fail e -> Fail e | Return msgs2 -> begin match betree_node_lookup_first_message_for_key_back key msgs msgs2 with - | Fail -> Fail + | Fail e -> Fail e | Return msgs3 -> Return msgs3 end end @@ -1082,45 +1085,45 @@ let betree_node_apply_to_internal_fwd_back | BetreeMessageDelete -> begin match betree_node_filter_messages_for_key_fwd_back key msgs0 with - | Fail -> Fail + | Fail e -> Fail e | Return msgs1 -> begin match betree_list_push_front_fwd_back (u64 & betree_message_t) msgs1 (key, BetreeMessageDelete) with - | Fail -> Fail + | Fail e -> Fail e | Return msgs2 -> begin match betree_node_lookup_first_message_for_key_back key msgs msgs2 with - | Fail -> Fail + | Fail e -> Fail e | Return msgs3 -> Return msgs3 end end end | BetreeMessageUpsert s -> begin match betree_list_hd_fwd (u64 & betree_message_t) msgs0 with - | Fail -> Fail + | Fail e -> Fail e | Return p -> let (_, m) = p in begin match m with | BetreeMessageInsert prev -> begin match betree_upsert_update_fwd (Some prev) s with - | Fail -> Fail + | Fail e -> Fail e | Return v -> begin match betree_list_pop_front_back (u64 & betree_message_t) msgs0 with - | Fail -> Fail + | Fail e -> Fail e | Return msgs1 -> begin match betree_list_push_front_fwd_back (u64 & betree_message_t) msgs1 (key, BetreeMessageInsert v) with - | Fail -> Fail + | Fail e -> Fail e | Return msgs2 -> begin match betree_node_lookup_first_message_for_key_back key msgs msgs2 with - | Fail -> Fail + | Fail e -> Fail e | Return msgs3 -> Return msgs3 end end @@ -1128,22 +1131,22 @@ let betree_node_apply_to_internal_fwd_back end | BetreeMessageDelete -> begin match betree_upsert_update_fwd None s with - | Fail -> Fail + | Fail e -> Fail e | Return v -> begin match betree_list_pop_front_back (u64 & betree_message_t) msgs0 with - | Fail -> Fail + | Fail e -> Fail e | Return msgs1 -> begin match betree_list_push_front_fwd_back (u64 & betree_message_t) msgs1 (key, BetreeMessageInsert v) with - | Fail -> Fail + | Fail e -> Fail e | Return msgs2 -> begin match betree_node_lookup_first_message_for_key_back key msgs msgs2 with - | Fail -> Fail + | Fail e -> Fail e | Return msgs3 -> Return msgs3 end end @@ -1152,22 +1155,22 @@ let betree_node_apply_to_internal_fwd_back | BetreeMessageUpsert ufs -> begin match betree_node_lookup_first_message_after_key_fwd key msgs0 with - | Fail -> Fail + | Fail e -> Fail e | Return msgs1 -> begin match betree_list_push_front_fwd_back (u64 & betree_message_t) msgs1 (key, BetreeMessageUpsert s) with - | Fail -> Fail + | Fail e -> Fail e | Return msgs2 -> begin match betree_node_lookup_first_message_after_key_back key msgs0 msgs2 with - | Fail -> Fail + | Fail e -> Fail e | Return msgs3 -> begin match betree_node_lookup_first_message_for_key_back key msgs msgs3 with - | Fail -> Fail + | Fail e -> Fail e | Return msgs4 -> Return msgs4 end end @@ -1180,11 +1183,11 @@ let betree_node_apply_to_internal_fwd_back begin match betree_list_push_front_fwd_back (u64 & betree_message_t) msgs0 (key, new_msg) with - | Fail -> Fail + | Fail e -> Fail e | Return msgs1 -> begin match betree_node_lookup_first_message_for_key_back key msgs msgs1 with - | Fail -> Fail + | Fail e -> Fail e | Return msgs2 -> Return msgs2 end end @@ -1202,11 +1205,11 @@ let rec betree_node_apply_messages_to_internal_fwd_back | BetreeListCons new_msg new_msgs_tl -> let (i, m) = new_msg in begin match betree_node_apply_to_internal_fwd_back msgs i m with - | Fail -> Fail + | Fail e -> Fail e | Return msgs0 -> begin match betree_node_apply_messages_to_internal_fwd_back msgs0 new_msgs_tl with - | Fail -> Fail + | Fail e -> Fail e | Return msgs1 -> Return msgs1 end end @@ -1225,31 +1228,31 @@ let rec betree_node_apply_messages_fwd begin match self with | BetreeNodeInternal node -> begin match betree_load_internal_node_fwd node.betree_internal_id st with - | Fail -> Fail + | Fail e -> Fail e | Return (st0, content) -> begin match betree_node_apply_messages_to_internal_fwd_back content msgs with - | Fail -> Fail + | Fail e -> Fail e | Return content0 -> begin match betree_list_len_fwd (u64 & betree_message_t) content0 with - | Fail -> Fail + | Fail e -> Fail e | Return num_msgs -> if num_msgs >= params.betree_params_min_flush_size then begin match betree_internal_flush_fwd node params node_id_cnt content0 st0 with - | Fail -> Fail + | Fail e -> Fail e | Return (st1, content1) -> begin match betree_internal_flush_back'a node params node_id_cnt content0 st0 st1 with - | Fail -> Fail + | Fail e -> Fail e | Return (st2, (node0, _)) -> begin match betree_store_internal_node_fwd node0.betree_internal_id content1 st2 with - | Fail -> Fail + | Fail e -> Fail e | Return (st3, _) -> Return (st3, ()) end end @@ -1258,7 +1261,7 @@ let rec betree_node_apply_messages_fwd begin match betree_store_internal_node_fwd node.betree_internal_id content0 st0 with - | Fail -> Fail + | Fail e -> Fail e | Return (st1, _) -> Return (st1, ()) end end @@ -1266,32 +1269,32 @@ let rec betree_node_apply_messages_fwd end | BetreeNodeLeaf node -> begin match betree_load_leaf_node_fwd node.betree_leaf_id st with - | Fail -> Fail + | Fail e -> Fail e | Return (st0, content) -> begin match betree_node_apply_messages_to_leaf_fwd_back content msgs with - | Fail -> Fail + | Fail e -> Fail e | Return content0 -> begin match betree_list_len_fwd (u64 & u64) content0 with - | Fail -> Fail + | Fail e -> Fail e | Return len -> begin match u64_mul 2 params.betree_params_split_size with - | Fail -> Fail + | Fail e -> Fail e | Return i -> if len >= i then begin match betree_leaf_split_fwd node content0 params node_id_cnt st0 with - | Fail -> Fail + | Fail e -> Fail e | Return (st1, _) -> begin match betree_store_leaf_node_fwd node.betree_leaf_id BetreeListNil st1 with - | Fail -> Fail + | Fail e -> Fail e | Return (st2, _) -> begin match betree_leaf_split_back0 node content0 params node_id_cnt st0 st2 with - | Fail -> Fail + | Fail e -> Fail e | Return (st3, ()) -> Return (st3, ()) end end @@ -1300,7 +1303,7 @@ let rec betree_node_apply_messages_fwd begin match betree_store_leaf_node_fwd node.betree_leaf_id content0 st0 with - | Fail -> Fail + | Fail e -> Fail e | Return (st1, _) -> Return (st1, ()) end end @@ -1321,31 +1324,31 @@ and betree_node_apply_messages_back'a begin match self with | BetreeNodeInternal node -> begin match betree_load_internal_node_fwd node.betree_internal_id st with - | Fail -> Fail + | Fail e -> Fail e | Return (st1, content) -> begin match betree_node_apply_messages_to_internal_fwd_back content msgs with - | Fail -> Fail + | Fail e -> Fail e | Return content0 -> begin match betree_list_len_fwd (u64 & betree_message_t) content0 with - | Fail -> Fail + | Fail e -> Fail e | Return num_msgs -> if num_msgs >= params.betree_params_min_flush_size then begin match betree_internal_flush_fwd node params node_id_cnt content0 st1 with - | Fail -> Fail + | Fail e -> Fail e | Return (st2, content1) -> begin match betree_internal_flush_back'a node params node_id_cnt content0 st1 st2 with - | Fail -> Fail + | Fail e -> Fail e | Return (st3, (node0, node_id_cnt0)) -> begin match betree_store_internal_node_fwd node0.betree_internal_id content1 st3 with - | Fail -> Fail + | Fail e -> Fail e | Return (_, _) -> Return (st0, (BetreeNodeInternal node0, node_id_cnt0)) end @@ -1355,7 +1358,7 @@ and betree_node_apply_messages_back'a begin match betree_store_internal_node_fwd node.betree_internal_id content0 st1 with - | Fail -> Fail + | Fail e -> Fail e | Return (_, _) -> Return (st0, (BetreeNodeInternal node, node_id_cnt)) end @@ -1364,37 +1367,37 @@ and betree_node_apply_messages_back'a end | BetreeNodeLeaf node -> begin match betree_load_leaf_node_fwd node.betree_leaf_id st with - | Fail -> Fail + | Fail e -> Fail e | Return (st1, content) -> begin match betree_node_apply_messages_to_leaf_fwd_back content msgs with - | Fail -> Fail + | Fail e -> Fail e | Return content0 -> begin match betree_list_len_fwd (u64 & u64) content0 with - | Fail -> Fail + | Fail e -> Fail e | Return len -> begin match u64_mul 2 params.betree_params_split_size with - | Fail -> Fail + | Fail e -> Fail e | Return i -> if len >= i then begin match betree_leaf_split_fwd node content0 params node_id_cnt st1 with - | Fail -> Fail + | Fail e -> Fail e | Return (st2, new_node) -> begin match betree_store_leaf_node_fwd node.betree_leaf_id BetreeListNil st2 with - | Fail -> Fail + | Fail e -> Fail e | Return (st3, _) -> begin match betree_leaf_split_back0 node content0 params node_id_cnt st1 st3 with - | Fail -> Fail + | Fail e -> Fail e | Return (_, ()) -> begin match betree_leaf_split_back2 node content0 params node_id_cnt st1 st0 with - | Fail -> Fail + | Fail e -> Fail e | Return (st4, node_id_cnt0) -> Return (st4, (BetreeNodeInternal new_node, node_id_cnt0)) end @@ -1405,7 +1408,7 @@ and betree_node_apply_messages_back'a begin match betree_store_leaf_node_fwd node.betree_leaf_id content0 st1 with - | Fail -> Fail + | Fail e -> Fail e | Return (_, _) -> Return (st0, (BetreeNodeLeaf (Mkbetree_leaf_t node.betree_leaf_id len), node_id_cnt)) @@ -1428,36 +1431,36 @@ and betree_node_apply_messages_back1 begin match self with | BetreeNodeInternal node -> begin match betree_load_internal_node_fwd node.betree_internal_id st with - | Fail -> Fail + | Fail e -> Fail e | Return (st1, content) -> begin match betree_node_apply_messages_to_internal_fwd_back content msgs with - | Fail -> Fail + | Fail e -> Fail e | Return content0 -> begin match betree_list_len_fwd (u64 & betree_message_t) content0 with - | Fail -> Fail + | Fail e -> Fail e | Return num_msgs -> if num_msgs >= params.betree_params_min_flush_size then begin match betree_internal_flush_fwd node params node_id_cnt content0 st1 with - | Fail -> Fail + | Fail e -> Fail e | Return (st2, content1) -> begin match betree_internal_flush_back'a node params node_id_cnt content0 st1 st2 with - | Fail -> Fail + | Fail e -> Fail e | Return (st3, (node0, _)) -> begin match betree_store_internal_node_fwd node0.betree_internal_id content1 st3 with - | Fail -> Fail + | Fail e -> Fail e | Return (_, _) -> begin match betree_internal_flush_back1 node params node_id_cnt content0 st1 st0 with - | Fail -> Fail + | Fail e -> Fail e | Return (st4, ()) -> Return (st4, ()) end end @@ -1467,7 +1470,7 @@ and betree_node_apply_messages_back1 begin match betree_store_internal_node_fwd node.betree_internal_id content0 st1 with - | Fail -> Fail + | Fail e -> Fail e | Return (_, _) -> Return (st0, ()) end end @@ -1475,37 +1478,37 @@ and betree_node_apply_messages_back1 end | BetreeNodeLeaf node -> begin match betree_load_leaf_node_fwd node.betree_leaf_id st with - | Fail -> Fail + | Fail e -> Fail e | Return (st1, content) -> begin match betree_node_apply_messages_to_leaf_fwd_back content msgs with - | Fail -> Fail + | Fail e -> Fail e | Return content0 -> begin match betree_list_len_fwd (u64 & u64) content0 with - | Fail -> Fail + | Fail e -> Fail e | Return len -> begin match u64_mul 2 params.betree_params_split_size with - | Fail -> Fail + | Fail e -> Fail e | Return i -> if len >= i then begin match betree_leaf_split_fwd node content0 params node_id_cnt st1 with - | Fail -> Fail + | Fail e -> Fail e | Return (st2, _) -> begin match betree_store_leaf_node_fwd node.betree_leaf_id BetreeListNil st2 with - | Fail -> Fail + | Fail e -> Fail e | Return (st3, _) -> begin match betree_leaf_split_back0 node content0 params node_id_cnt st1 st3 with - | Fail -> Fail + | Fail e -> Fail e | Return (_, ()) -> begin match betree_leaf_split_back1 node content0 params node_id_cnt st1 st0 with - | Fail -> Fail + | Fail e -> Fail e | Return (st4, ()) -> Return (st4, ()) end end @@ -1515,7 +1518,7 @@ and betree_node_apply_messages_back1 begin match betree_store_leaf_node_fwd node.betree_leaf_id content0 st1 with - | Fail -> Fail + | Fail e -> Fail e | Return (_, _) -> Return (st0, ()) end end @@ -1536,51 +1539,51 @@ and betree_internal_flush_fwd begin match betree_list_partition_at_pivot_fwd betree_message_t content self.betree_internal_pivot with - | Fail -> Fail + | Fail e -> Fail e | Return p -> let (msgs_left, msgs_right) = p in begin match betree_list_len_fwd (u64 & betree_message_t) msgs_left with - | Fail -> Fail + | Fail e -> Fail e | Return len_left -> if len_left >= params.betree_params_min_flush_size then begin match betree_node_apply_messages_fwd self.betree_internal_left params node_id_cnt msgs_left st with - | Fail -> Fail + | Fail e -> Fail e | Return (st0, _) -> begin match betree_node_apply_messages_back'a self.betree_internal_left params node_id_cnt msgs_left st st0 with - | Fail -> Fail + | Fail e -> Fail e | Return (st1, (_, node_id_cnt0)) -> begin match betree_node_apply_messages_back1 self.betree_internal_left params node_id_cnt msgs_left st st1 with - | Fail -> Fail + | Fail e -> Fail e | Return (st2, ()) -> begin match betree_list_len_fwd (u64 & betree_message_t) msgs_right with - | Fail -> Fail + | Fail e -> Fail e | Return len_right -> if len_right >= params.betree_params_min_flush_size then begin match betree_node_apply_messages_fwd self.betree_internal_right params node_id_cnt0 msgs_right st2 with - | Fail -> Fail + | Fail e -> Fail e | Return (st3, _) -> begin match betree_node_apply_messages_back'a self.betree_internal_right params node_id_cnt0 msgs_right st2 st3 with - | Fail -> Fail + | Fail e -> Fail e | Return (st4, (_, _)) -> begin match betree_node_apply_messages_back1 self.betree_internal_right params node_id_cnt0 msgs_right st2 st4 with - | Fail -> Fail + | Fail e -> Fail e | Return (st5, ()) -> Return (st5, BetreeListNil) end end @@ -1594,17 +1597,17 @@ and betree_internal_flush_fwd begin match betree_node_apply_messages_fwd self.betree_internal_right params node_id_cnt msgs_right st with - | Fail -> Fail + | Fail e -> Fail e | Return (st0, _) -> begin match betree_node_apply_messages_back'a self.betree_internal_right params node_id_cnt msgs_right st st0 with - | Fail -> Fail + | Fail e -> Fail e | Return (st1, (_, _)) -> begin match betree_node_apply_messages_back1 self.betree_internal_right params node_id_cnt msgs_right st st1 with - | Fail -> Fail + | Fail e -> Fail e | Return (st2, ()) -> Return (st2, msgs_left) end end @@ -1624,51 +1627,51 @@ and betree_internal_flush_back'a begin match betree_list_partition_at_pivot_fwd betree_message_t content self.betree_internal_pivot with - | Fail -> Fail + | Fail e -> Fail e | Return p -> let (msgs_left, msgs_right) = p in begin match betree_list_len_fwd (u64 & betree_message_t) msgs_left with - | Fail -> Fail + | Fail e -> Fail e | Return len_left -> if len_left >= params.betree_params_min_flush_size then begin match betree_node_apply_messages_fwd self.betree_internal_left params node_id_cnt msgs_left st with - | Fail -> Fail + | Fail e -> Fail e | Return (st1, _) -> begin match betree_node_apply_messages_back'a self.betree_internal_left params node_id_cnt msgs_left st st1 with - | Fail -> Fail + | Fail e -> Fail e | Return (st2, (n, node_id_cnt0)) -> begin match betree_node_apply_messages_back1 self.betree_internal_left params node_id_cnt msgs_left st st2 with - | Fail -> Fail + | Fail e -> Fail e | Return (st3, ()) -> begin match betree_list_len_fwd (u64 & betree_message_t) msgs_right with - | Fail -> Fail + | Fail e -> Fail e | Return len_right -> if len_right >= params.betree_params_min_flush_size then begin match betree_node_apply_messages_fwd self.betree_internal_right params node_id_cnt0 msgs_right st3 with - | Fail -> Fail + | Fail e -> Fail e | Return (st4, _) -> begin match betree_node_apply_messages_back'a self.betree_internal_right params node_id_cnt0 msgs_right st3 st4 with - | Fail -> Fail + | Fail e -> Fail e | Return (st5, (n0, node_id_cnt1)) -> begin match betree_node_apply_messages_back1 self.betree_internal_right params node_id_cnt0 msgs_right st3 st5 with - | Fail -> Fail + | Fail e -> Fail e | Return (_, ()) -> Return (st0, (Mkbetree_internal_t self.betree_internal_id self.betree_internal_pivot n @@ -1688,17 +1691,17 @@ and betree_internal_flush_back'a begin match betree_node_apply_messages_fwd self.betree_internal_right params node_id_cnt msgs_right st with - | Fail -> Fail + | Fail e -> Fail e | Return (st1, _) -> begin match betree_node_apply_messages_back'a self.betree_internal_right params node_id_cnt msgs_right st st1 with - | Fail -> Fail + | Fail e -> Fail e | Return (st2, (n, node_id_cnt0)) -> begin match betree_node_apply_messages_back1 self.betree_internal_right params node_id_cnt msgs_right st st2 with - | Fail -> Fail + | Fail e -> Fail e | Return (_, ()) -> Return (st0, (Mkbetree_internal_t self.betree_internal_id self.betree_internal_pivot self.betree_internal_left n, @@ -1721,51 +1724,51 @@ and betree_internal_flush_back1 begin match betree_list_partition_at_pivot_fwd betree_message_t content self.betree_internal_pivot with - | Fail -> Fail + | Fail e -> Fail e | Return p -> let (msgs_left, msgs_right) = p in begin match betree_list_len_fwd (u64 & betree_message_t) msgs_left with - | Fail -> Fail + | Fail e -> Fail e | Return len_left -> if len_left >= params.betree_params_min_flush_size then begin match betree_node_apply_messages_fwd self.betree_internal_left params node_id_cnt msgs_left st with - | Fail -> Fail + | Fail e -> Fail e | Return (st1, _) -> begin match betree_node_apply_messages_back'a self.betree_internal_left params node_id_cnt msgs_left st st1 with - | Fail -> Fail + | Fail e -> Fail e | Return (st2, (_, node_id_cnt0)) -> begin match betree_node_apply_messages_back1 self.betree_internal_left params node_id_cnt msgs_left st st2 with - | Fail -> Fail + | Fail e -> Fail e | Return (st3, ()) -> begin match betree_list_len_fwd (u64 & betree_message_t) msgs_right with - | Fail -> Fail + | Fail e -> Fail e | Return len_right -> if len_right >= params.betree_params_min_flush_size then begin match betree_node_apply_messages_fwd self.betree_internal_right params node_id_cnt0 msgs_right st3 with - | Fail -> Fail + | Fail e -> Fail e | Return (st4, _) -> begin match betree_node_apply_messages_back'a self.betree_internal_right params node_id_cnt0 msgs_right st3 st4 with - | Fail -> Fail + | Fail e -> Fail e | Return (st5, (_, _)) -> begin match betree_node_apply_messages_back1 self.betree_internal_right params node_id_cnt0 msgs_right st3 st5 with - | Fail -> Fail + | Fail e -> Fail e | Return (_, ()) -> Return (st0, ()) end end @@ -1779,17 +1782,17 @@ and betree_internal_flush_back1 begin match betree_node_apply_messages_fwd self.betree_internal_right params node_id_cnt msgs_right st with - | Fail -> Fail + | Fail e -> Fail e | Return (st1, _) -> begin match betree_node_apply_messages_back'a self.betree_internal_right params node_id_cnt msgs_right st st1 with - | Fail -> Fail + | Fail e -> Fail e | Return (st2, (_, _)) -> begin match betree_node_apply_messages_back1 self.betree_internal_right params node_id_cnt msgs_right st st2 with - | Fail -> Fail + | Fail e -> Fail e | Return (_, ()) -> Return (st0, ()) end end @@ -1808,17 +1811,17 @@ let betree_node_apply_fwd begin match betree_node_apply_messages_fwd self params node_id_cnt (BetreeListCons (key, new_msg) l) st with - | Fail -> Fail + | Fail e -> Fail e | Return (st0, _) -> begin match betree_node_apply_messages_back'a self params node_id_cnt (BetreeListCons (key, new_msg) l) st st0 with - | Fail -> Fail + | Fail e -> Fail e | Return (st1, (_, _)) -> begin match betree_node_apply_messages_back1 self params node_id_cnt (BetreeListCons (key, new_msg) l) st st1 with - | Fail -> Fail + | Fail e -> Fail e | Return (st2, ()) -> Return (st2, ()) end end @@ -1835,17 +1838,17 @@ let betree_node_apply_back'a begin match betree_node_apply_messages_fwd self params node_id_cnt (BetreeListCons (key, new_msg) l) st with - | Fail -> Fail + | Fail e -> Fail e | Return (st1, _) -> begin match betree_node_apply_messages_back'a self params node_id_cnt (BetreeListCons (key, new_msg) l) st st1 with - | Fail -> Fail + | Fail e -> Fail e | Return (st2, (self0, node_id_cnt0)) -> begin match betree_node_apply_messages_back1 self params node_id_cnt (BetreeListCons (key, new_msg) l) st st2 with - | Fail -> Fail + | Fail e -> Fail e | Return (_, ()) -> Return (st0, (self0, node_id_cnt0)) end end @@ -1862,17 +1865,17 @@ let betree_node_apply_back1 begin match betree_node_apply_messages_fwd self params node_id_cnt (BetreeListCons (key, new_msg) l) st with - | Fail -> Fail + | Fail e -> Fail e | Return (st1, _) -> begin match betree_node_apply_messages_back'a self params node_id_cnt (BetreeListCons (key, new_msg) l) st st1 with - | Fail -> Fail + | Fail e -> Fail e | Return (st2, (_, _)) -> begin match betree_node_apply_messages_back1 self params node_id_cnt (BetreeListCons (key, new_msg) l) st st2 with - | Fail -> Fail + | Fail e -> Fail e | Return (_, ()) -> Return (st0, ()) end end @@ -1884,16 +1887,16 @@ let betree_be_tree_new_fwd result (state & betree_be_tree_t) = begin match betree_node_id_counter_new_fwd with - | Fail -> Fail + | Fail e -> Fail e | Return node_id_cnt -> begin match betree_node_id_counter_fresh_id_fwd node_id_cnt with - | Fail -> Fail + | Fail e -> Fail e | Return id -> begin match betree_store_leaf_node_fwd id BetreeListNil st with - | Fail -> Fail + | Fail e -> Fail e | Return (st0, _) -> begin match betree_node_id_counter_fresh_id_back node_id_cnt with - | Fail -> Fail + | Fail e -> Fail e | Return node_id_cnt0 -> Return (st0, Mkbetree_be_tree_t (Mkbetree_params_t min_flush_size split_size) node_id_cnt0 (BetreeNodeLeaf (Mkbetree_leaf_t id 0))) @@ -1910,19 +1913,19 @@ let betree_be_tree_apply_fwd begin match betree_node_apply_fwd self.betree_be_tree_root self.betree_be_tree_params self.betree_be_tree_node_id_cnt key msg st with - | Fail -> Fail + | Fail e -> Fail e | Return (st0, _) -> begin match betree_node_apply_back'a self.betree_be_tree_root self.betree_be_tree_params self.betree_be_tree_node_id_cnt key msg st st0 with - | Fail -> Fail + | Fail e -> Fail e | Return (st1, (_, _)) -> begin match betree_node_apply_back1 self.betree_be_tree_root self.betree_be_tree_params self.betree_be_tree_node_id_cnt key msg st st1 with - | Fail -> Fail + | Fail e -> Fail e | Return (st2, ()) -> Return (st2, ()) end end @@ -1937,19 +1940,19 @@ let betree_be_tree_apply_back begin match betree_node_apply_fwd self.betree_be_tree_root self.betree_be_tree_params self.betree_be_tree_node_id_cnt key msg st with - | Fail -> Fail + | Fail e -> Fail e | Return (st1, _) -> begin match betree_node_apply_back'a self.betree_be_tree_root self.betree_be_tree_params self.betree_be_tree_node_id_cnt key msg st st1 with - | Fail -> Fail + | Fail e -> Fail e | Return (st2, (n, nic)) -> begin match betree_node_apply_back1 self.betree_be_tree_root self.betree_be_tree_params self.betree_be_tree_node_id_cnt key msg st st2 with - | Fail -> Fail + | Fail e -> Fail e | Return (_, ()) -> Return (st0, Mkbetree_be_tree_t self.betree_be_tree_params nic n) end @@ -1963,12 +1966,12 @@ let betree_be_tree_insert_fwd = begin match betree_be_tree_apply_fwd self key (BetreeMessageInsert value) st with - | Fail -> Fail + | Fail e -> Fail e | Return (st0, _) -> begin match betree_be_tree_apply_back self key (BetreeMessageInsert value) st st0 with - | Fail -> Fail + | Fail e -> Fail e | Return (st1, _) -> Return (st1, ()) end end @@ -1981,12 +1984,12 @@ let betree_be_tree_insert_back = begin match betree_be_tree_apply_fwd self key (BetreeMessageInsert value) st with - | Fail -> Fail + | Fail e -> Fail e | Return (st1, _) -> begin match betree_be_tree_apply_back self key (BetreeMessageInsert value) st st1 with - | Fail -> Fail + | Fail e -> Fail e | Return (_, self0) -> Return (st0, self0) end end @@ -1995,11 +1998,11 @@ let betree_be_tree_insert_back let betree_be_tree_delete_fwd (self : betree_be_tree_t) (key : u64) (st : state) : result (state & unit) = begin match betree_be_tree_apply_fwd self key BetreeMessageDelete st with - | Fail -> Fail + | Fail e -> Fail e | Return (st0, _) -> begin match betree_be_tree_apply_back self key BetreeMessageDelete st st0 with - | Fail -> Fail + | Fail e -> Fail e | Return (st1, _) -> Return (st1, ()) end end @@ -2010,11 +2013,11 @@ let betree_be_tree_delete_back result (state & betree_be_tree_t) = begin match betree_be_tree_apply_fwd self key BetreeMessageDelete st with - | Fail -> Fail + | Fail e -> Fail e | Return (st1, _) -> begin match betree_be_tree_apply_back self key BetreeMessageDelete st st1 with - | Fail -> Fail + | Fail e -> Fail e | Return (_, self0) -> Return (st0, self0) end end @@ -2027,11 +2030,11 @@ let betree_be_tree_upsert_fwd = begin match betree_be_tree_apply_fwd self key (BetreeMessageUpsert upd) st with - | Fail -> Fail + | Fail e -> Fail e | Return (st0, _) -> begin match betree_be_tree_apply_back self key (BetreeMessageUpsert upd) st st0 with - | Fail -> Fail + | Fail e -> Fail e | Return (st1, _) -> Return (st1, ()) end end @@ -2044,11 +2047,11 @@ let betree_be_tree_upsert_back = begin match betree_be_tree_apply_fwd self key (BetreeMessageUpsert upd) st with - | Fail -> Fail + | Fail e -> Fail e | Return (st1, _) -> begin match betree_be_tree_apply_back self key (BetreeMessageUpsert upd) st st1 with - | Fail -> Fail + | Fail e -> Fail e | Return (_, self0) -> Return (st0, self0) end end @@ -2059,7 +2062,7 @@ let betree_be_tree_lookup_fwd result (state & (option u64)) = begin match betree_node_lookup_fwd self.betree_be_tree_root key st with - | Fail -> Fail + | Fail e -> Fail e | Return (st0, opt) -> Return (st0, opt) end @@ -2069,7 +2072,7 @@ let betree_be_tree_lookup_back result (state & betree_be_tree_t) = begin match betree_node_lookup_back self.betree_be_tree_root key st st0 with - | Fail -> Fail + | Fail e -> Fail e | Return (st1, n) -> Return (st1, Mkbetree_be_tree_t self.betree_be_tree_params self.betree_be_tree_node_id_cnt n) diff --git a/tests/fstar/betree_back_stateful/Primitives.fst b/tests/fstar/betree_back_stateful/Primitives.fst index 96138e46..82622656 100644 --- a/tests/fstar/betree_back_stateful/Primitives.fst +++ b/tests/fstar/betree_back_stateful/Primitives.fst @@ -18,9 +18,13 @@ let rec list_update #a ls i x = #pop-options (*** Result *) +type error : Type0 = +| Failure +| OutOfFuel + type result (a : Type0) : Type0 = | Return : v:a -> result a -| Fail : result a +| Fail : e:error -> result a // Monadic bind and return. // Re-definining those allows us to customize the result of the monadic notations @@ -29,10 +33,10 @@ let return (#a : Type0) (x:a) : result a = Return x let bind (#a #b : Type0) (m : result a) (f : a -> result b) : result b = match m with | Return x -> f x - | Fail -> Fail + | Fail e -> Fail e // Monadic assert(...) -let massert (b:bool) : result unit = if b then Return () else Fail +let massert (b:bool) : result unit = if b then Return () else Fail Failure // Normalize and unwrap a successful result (used for globals). let eval_global (#a : Type0) (x : result a{Return? (normalize_term x)}) : a = Return?.v x @@ -119,12 +123,12 @@ let scalar_max (ty : scalar_ty) : int = type scalar (ty : scalar_ty) : eqtype = x:int{scalar_min ty <= x && x <= scalar_max ty} let mk_scalar (ty : scalar_ty) (x : int) : result (scalar ty) = - if scalar_min ty <= x && scalar_max ty >= x then Return x else Fail + if scalar_min ty <= x && scalar_max ty >= x then Return x else Fail Failure let scalar_neg (#ty : scalar_ty) (x : scalar ty) : result (scalar ty) = mk_scalar ty (-x) let scalar_div (#ty : scalar_ty) (x : scalar ty) (y : scalar ty) : result (scalar ty) = - if y <> 0 then mk_scalar ty (x / y) else Fail + if y <> 0 then mk_scalar ty (x / y) else Fail Failure /// The remainder operation let int_rem (x : int) (y : int{y <> 0}) : int = @@ -137,7 +141,7 @@ let _ = assert_norm(int_rem 1 (-2) = 1) let _ = assert_norm(int_rem (-1) (-2) = -1) let scalar_rem (#ty : scalar_ty) (x : scalar ty) (y : scalar ty) : result (scalar ty) = - if y <> 0 then mk_scalar ty (int_rem x y) else Fail + if y <> 0 then mk_scalar ty (int_rem x y) else Fail Failure let scalar_add (#ty : scalar_ty) (x : scalar ty) (y : scalar ty) : result (scalar ty) = mk_scalar ty (x + y) @@ -258,7 +262,7 @@ let vec_push_back (a : Type0) (v : vec a) (x : a) : (requires True) (ensures (fun res -> match res with - | Fail -> True + | Fail e -> e == Failure | Return v' -> length v' = length v + 1)) = if length v < usize_max then begin (**) assert_norm(length [x] == 1); @@ -266,22 +270,22 @@ let vec_push_back (a : Type0) (v : vec a) (x : a) : (**) assert(length (append v [x]) = length v + 1); Return (append v [x]) end - else Fail + else Fail Failure // The **forward** function shouldn't be used let vec_insert_fwd (a : Type0) (v : vec a) (i : usize) (x : a) : result unit = - if i < length v then Return () else Fail + if i < length v then Return () else Fail Failure let vec_insert_back (a : Type0) (v : vec a) (i : usize) (x : a) : result (vec a) = - if i < length v then Return (list_update v i x) else Fail + if i < length v then Return (list_update v i x) else Fail Failure // The **backward** function shouldn't be used let vec_index_fwd (a : Type0) (v : vec a) (i : usize) : result a = - if i < length v then Return (index v i) else Fail + if i < length v then Return (index v i) else Fail Failure let vec_index_back (a : Type0) (v : vec a) (i : usize) (x : a) : result unit = - if i < length v then Return () else Fail + if i < length v then Return () else Fail Failure let vec_index_mut_fwd (a : Type0) (v : vec a) (i : usize) : result a = - if i < length v then Return (index v i) else Fail + if i < length v then Return (index v i) else Fail Failure let vec_index_mut_back (a : Type0) (v : vec a) (i : usize) (nx : a) : result (vec a) = - if i < length v then Return (list_update v i nx) else Fail + if i < length v then Return (list_update v i nx) else Fail Failure diff --git a/tests/fstar/hashmap/Hashmap.Funs.fst b/tests/fstar/hashmap/Hashmap.Funs.fst index 6e67fca4..e3ae587f 100644 --- a/tests/fstar/hashmap/Hashmap.Funs.fst +++ b/tests/fstar/hashmap/Hashmap.Funs.fst @@ -20,13 +20,13 @@ let rec hash_map_allocate_slots_fwd then Return slots else begin match vec_push_back (list_t t) slots ListNil with - | Fail -> Fail + | Fail e -> Fail e | Return slots0 -> begin match usize_sub n 1 with - | Fail -> Fail + | Fail e -> Fail e | Return i -> begin match hash_map_allocate_slots_fwd t slots0 i with - | Fail -> Fail + | Fail e -> Fail e | Return v -> Return v end end @@ -40,13 +40,13 @@ let hash_map_new_with_capacity_fwd = let v = vec_new (list_t t) in begin match hash_map_allocate_slots_fwd t v capacity with - | Fail -> Fail + | Fail e -> Fail e | Return slots -> begin match usize_mul capacity max_load_dividend with - | Fail -> Fail + | Fail e -> Fail e | Return i -> begin match usize_div i max_load_divisor with - | Fail -> Fail + | Fail e -> Fail e | Return i0 -> Return (Mkhash_map_t 0 (max_load_dividend, max_load_divisor) i0 slots) end @@ -56,7 +56,7 @@ let hash_map_new_with_capacity_fwd (** [hashmap::HashMap::{0}::new] *) let hash_map_new_fwd (t : Type0) : result (hash_map_t t) = begin match hash_map_new_with_capacity_fwd t 32 4 5 with - | Fail -> Fail + | Fail e -> Fail e | Return hm -> Return hm end @@ -70,13 +70,13 @@ let rec hash_map_clear_slots_fwd_back if i < i0 then begin match vec_index_mut_back (list_t t) slots i ListNil with - | Fail -> Fail + | Fail e -> Fail e | Return slots0 -> begin match usize_add i 1 with - | Fail -> Fail + | Fail e -> Fail e | Return i1 -> begin match hash_map_clear_slots_fwd_back t slots0 i1 with - | Fail -> Fail + | Fail e -> Fail e | Return slots1 -> Return slots1 end end @@ -87,7 +87,7 @@ let rec hash_map_clear_slots_fwd_back let hash_map_clear_fwd_back (t : Type0) (self : hash_map_t t) : result (hash_map_t t) = begin match hash_map_clear_slots_fwd_back t self.hash_map_slots 0 with - | Fail -> Fail + | Fail e -> Fail e | Return v -> Return (Mkhash_map_t 0 self.hash_map_max_load_factor self.hash_map_max_load v) @@ -109,7 +109,7 @@ let rec hash_map_insert_in_list_fwd then Return false else begin match hash_map_insert_in_list_fwd t key value ls0 with - | Fail -> Fail + | Fail e -> Fail e | Return b -> Return b end | ListNil -> Return true @@ -127,7 +127,7 @@ let rec hash_map_insert_in_list_back then Return (ListCons ckey value ls0) else begin match hash_map_insert_in_list_back t key value ls0 with - | Fail -> Fail + | Fail e -> Fail e | Return ls1 -> Return (ListCons ckey cvalue ls1) end | ListNil -> let l = ListNil in Return (ListCons key value l) @@ -139,31 +139,31 @@ let hash_map_insert_no_resize_fwd_back result (hash_map_t t) = begin match hash_key_fwd key with - | Fail -> Fail + | Fail e -> Fail e | Return hash -> let i = vec_len (list_t t) self.hash_map_slots in begin match usize_rem hash i with - | Fail -> Fail + | Fail e -> Fail e | Return hash_mod -> begin match vec_index_mut_fwd (list_t t) self.hash_map_slots hash_mod with - | Fail -> Fail + | Fail e -> Fail e | Return l -> begin match hash_map_insert_in_list_fwd t key value l with - | Fail -> Fail + | Fail e -> Fail e | Return inserted -> if inserted then begin match usize_add self.hash_map_num_entries 1 with - | Fail -> Fail + | Fail e -> Fail e | Return i0 -> begin match hash_map_insert_in_list_back t key value l with - | Fail -> Fail + | Fail e -> Fail e | Return l0 -> begin match vec_index_mut_back (list_t t) self.hash_map_slots hash_mod l0 with - | Fail -> Fail + | Fail e -> Fail e | Return v -> Return (Mkhash_map_t i0 self.hash_map_max_load_factor self.hash_map_max_load v) @@ -172,12 +172,12 @@ let hash_map_insert_no_resize_fwd_back end else begin match hash_map_insert_in_list_back t key value l with - | Fail -> Fail + | Fail e -> Fail e | Return l0 -> begin match vec_index_mut_back (list_t t) self.hash_map_slots hash_mod l0 with - | Fail -> Fail + | Fail e -> Fail e | Return v -> Return (Mkhash_map_t self.hash_map_num_entries self.hash_map_max_load_factor self.hash_map_max_load v) @@ -201,10 +201,10 @@ let rec hash_map_move_elements_from_list_fwd_back begin match ls with | ListCons k v tl -> begin match hash_map_insert_no_resize_fwd_back t ntable k v with - | Fail -> Fail + | Fail e -> Fail e | Return ntable0 -> begin match hash_map_move_elements_from_list_fwd_back t ntable0 tl with - | Fail -> Fail + | Fail e -> Fail e | Return ntable1 -> Return ntable1 end end @@ -221,22 +221,22 @@ let rec hash_map_move_elements_fwd_back if i < i0 then begin match vec_index_mut_fwd (list_t t) slots i with - | Fail -> Fail + | Fail e -> Fail e | Return l -> let ls = mem_replace_fwd (list_t t) l ListNil in begin match hash_map_move_elements_from_list_fwd_back t ntable ls with - | Fail -> Fail + | Fail e -> Fail e | Return ntable0 -> let l0 = mem_replace_back (list_t t) l ListNil in begin match vec_index_mut_back (list_t t) slots i l0 with - | Fail -> Fail + | Fail e -> Fail e | Return slots0 -> begin match usize_add i 1 with - | Fail -> Fail + | Fail e -> Fail e | Return i1 -> begin match hash_map_move_elements_fwd_back t ntable0 slots0 i1 with - | Fail -> Fail + | Fail e -> Fail e | Return (ntable1, slots1) -> Return (ntable1, slots1) end end @@ -249,28 +249,28 @@ let rec hash_map_move_elements_fwd_back let hash_map_try_resize_fwd_back (t : Type0) (self : hash_map_t t) : result (hash_map_t t) = begin match scalar_cast U32 Usize core_num_u32_max_c with - | Fail -> Fail + | Fail e -> Fail e | Return max_usize -> let capacity = vec_len (list_t t) self.hash_map_slots in begin match usize_div max_usize 2 with - | Fail -> Fail + | Fail e -> Fail e | Return n1 -> let (i, i0) = self.hash_map_max_load_factor in begin match usize_div n1 i with - | Fail -> Fail + | Fail e -> Fail e | Return i1 -> if capacity <= i1 then begin match usize_mul capacity 2 with - | Fail -> Fail + | Fail e -> Fail e | Return i2 -> begin match hash_map_new_with_capacity_fwd t i2 i i0 with - | Fail -> Fail + | Fail e -> Fail e | Return ntable -> begin match hash_map_move_elements_fwd_back t ntable self.hash_map_slots 0 with - | Fail -> Fail + | Fail e -> Fail e | Return (ntable0, _) -> Return (Mkhash_map_t self.hash_map_num_entries (i, i0) ntable0.hash_map_max_load ntable0.hash_map_slots) @@ -290,15 +290,15 @@ let hash_map_insert_fwd_back result (hash_map_t t) = begin match hash_map_insert_no_resize_fwd_back t self key value with - | Fail -> Fail + | Fail e -> Fail e | Return self0 -> begin match hash_map_len_fwd t self0 with - | Fail -> Fail + | Fail e -> Fail e | Return i -> if i > self0.hash_map_max_load then begin match hash_map_try_resize_fwd_back t self0 with - | Fail -> Fail + | Fail e -> Fail e | Return self1 -> Return self1 end else Return self0 @@ -317,7 +317,7 @@ let rec hash_map_contains_key_in_list_fwd then Return true else begin match hash_map_contains_key_in_list_fwd t key ls0 with - | Fail -> Fail + | Fail e -> Fail e | Return b -> Return b end | ListNil -> Return false @@ -327,17 +327,17 @@ let rec hash_map_contains_key_in_list_fwd let hash_map_contains_key_fwd (t : Type0) (self : hash_map_t t) (key : usize) : result bool = begin match hash_key_fwd key with - | Fail -> Fail + | Fail e -> Fail e | Return hash -> let i = vec_len (list_t t) self.hash_map_slots in begin match usize_rem hash i with - | Fail -> Fail + | Fail e -> Fail e | Return hash_mod -> begin match vec_index_fwd (list_t t) self.hash_map_slots hash_mod with - | Fail -> Fail + | Fail e -> Fail e | Return l -> begin match hash_map_contains_key_in_list_fwd t key l with - | Fail -> Fail + | Fail e -> Fail e | Return b -> Return b end end @@ -355,27 +355,27 @@ let rec hash_map_get_in_list_fwd then Return cvalue else begin match hash_map_get_in_list_fwd t key ls0 with - | Fail -> Fail + | Fail e -> Fail e | Return x -> Return x end - | ListNil -> Fail + | ListNil -> Fail Failure end (** [hashmap::HashMap::{0}::get] *) let hash_map_get_fwd (t : Type0) (self : hash_map_t t) (key : usize) : result t = begin match hash_key_fwd key with - | Fail -> Fail + | Fail e -> Fail e | Return hash -> let i = vec_len (list_t t) self.hash_map_slots in begin match usize_rem hash i with - | Fail -> Fail + | Fail e -> Fail e | Return hash_mod -> begin match vec_index_fwd (list_t t) self.hash_map_slots hash_mod with - | Fail -> Fail + | Fail e -> Fail e | Return l -> begin match hash_map_get_in_list_fwd t key l with - | Fail -> Fail + | Fail e -> Fail e | Return x -> Return x end end @@ -393,10 +393,10 @@ let rec hash_map_get_mut_in_list_fwd then Return cvalue else begin match hash_map_get_mut_in_list_fwd t key ls0 with - | Fail -> Fail + | Fail e -> Fail e | Return x -> Return x end - | ListNil -> Fail + | ListNil -> Fail Failure end (** [hashmap::HashMap::{0}::get_mut_in_list] *) @@ -411,28 +411,28 @@ let rec hash_map_get_mut_in_list_back then Return (ListCons ckey ret ls0) else begin match hash_map_get_mut_in_list_back t key ls0 ret with - | Fail -> Fail + | Fail e -> Fail e | Return ls1 -> Return (ListCons ckey cvalue ls1) end - | ListNil -> Fail + | ListNil -> Fail Failure end (** [hashmap::HashMap::{0}::get_mut] *) let hash_map_get_mut_fwd (t : Type0) (self : hash_map_t t) (key : usize) : result t = begin match hash_key_fwd key with - | Fail -> Fail + | Fail e -> Fail e | Return hash -> let i = vec_len (list_t t) self.hash_map_slots in begin match usize_rem hash i with - | Fail -> Fail + | Fail e -> Fail e | Return hash_mod -> begin match vec_index_mut_fwd (list_t t) self.hash_map_slots hash_mod with - | Fail -> Fail + | Fail e -> Fail e | Return l -> begin match hash_map_get_mut_in_list_fwd t key l with - | Fail -> Fail + | Fail e -> Fail e | Return x -> Return x end end @@ -445,22 +445,22 @@ let hash_map_get_mut_back result (hash_map_t t) = begin match hash_key_fwd key with - | Fail -> Fail + | Fail e -> Fail e | Return hash -> let i = vec_len (list_t t) self.hash_map_slots in begin match usize_rem hash i with - | Fail -> Fail + | Fail e -> Fail e | Return hash_mod -> begin match vec_index_mut_fwd (list_t t) self.hash_map_slots hash_mod with - | Fail -> Fail + | Fail e -> Fail e | Return l -> begin match hash_map_get_mut_in_list_back t key l ret with - | Fail -> Fail + | Fail e -> Fail e | Return l0 -> begin match vec_index_mut_back (list_t t) self.hash_map_slots hash_mod l0 with - | Fail -> Fail + | Fail e -> Fail e | Return v -> Return (Mkhash_map_t self.hash_map_num_entries self.hash_map_max_load_factor self.hash_map_max_load v) @@ -483,11 +483,11 @@ let rec hash_map_remove_from_list_fwd let mv_ls = mem_replace_fwd (list_t t) (ListCons ckey x tl) ListNil in begin match mv_ls with | ListCons i cvalue tl0 -> Return (Some cvalue) - | ListNil -> Fail + | ListNil -> Fail Failure end else begin match hash_map_remove_from_list_fwd t key tl with - | Fail -> Fail + | Fail e -> Fail e | Return opt -> Return opt end | ListNil -> Return None @@ -506,11 +506,11 @@ let rec hash_map_remove_from_list_back let mv_ls = mem_replace_fwd (list_t t) (ListCons ckey x tl) ListNil in begin match mv_ls with | ListCons i cvalue tl0 -> Return tl0 - | ListNil -> Fail + | ListNil -> Fail Failure end else begin match hash_map_remove_from_list_back t key tl with - | Fail -> Fail + | Fail e -> Fail e | Return tl0 -> Return (ListCons ckey x tl0) end | ListNil -> Return ListNil @@ -520,24 +520,24 @@ let rec hash_map_remove_from_list_back let hash_map_remove_fwd (t : Type0) (self : hash_map_t t) (key : usize) : result (option t) = begin match hash_key_fwd key with - | Fail -> Fail + | Fail e -> Fail e | Return hash -> let i = vec_len (list_t t) self.hash_map_slots in begin match usize_rem hash i with - | Fail -> Fail + | Fail e -> Fail e | Return hash_mod -> begin match vec_index_mut_fwd (list_t t) self.hash_map_slots hash_mod with - | Fail -> Fail + | Fail e -> Fail e | Return l -> begin match hash_map_remove_from_list_fwd t key l with - | Fail -> Fail + | Fail e -> Fail e | Return x -> begin match x with | None -> Return None | Some x0 -> begin match usize_sub self.hash_map_num_entries 1 with - | Fail -> Fail + | Fail e -> Fail e | Return _ -> Return (Some x0) end end @@ -550,28 +550,28 @@ let hash_map_remove_fwd let hash_map_remove_back (t : Type0) (self : hash_map_t t) (key : usize) : result (hash_map_t t) = begin match hash_key_fwd key with - | Fail -> Fail + | Fail e -> Fail e | Return hash -> let i = vec_len (list_t t) self.hash_map_slots in begin match usize_rem hash i with - | Fail -> Fail + | Fail e -> Fail e | Return hash_mod -> begin match vec_index_mut_fwd (list_t t) self.hash_map_slots hash_mod with - | Fail -> Fail + | Fail e -> Fail e | Return l -> begin match hash_map_remove_from_list_fwd t key l with - | Fail -> Fail + | Fail e -> Fail e | Return x -> begin match x with | None -> begin match hash_map_remove_from_list_back t key l with - | Fail -> Fail + | Fail e -> Fail e | Return l0 -> begin match vec_index_mut_back (list_t t) self.hash_map_slots hash_mod l0 with - | Fail -> Fail + | Fail e -> Fail e | Return v -> Return (Mkhash_map_t self.hash_map_num_entries self.hash_map_max_load_factor self.hash_map_max_load v) @@ -579,15 +579,15 @@ let hash_map_remove_back end | Some x0 -> begin match usize_sub self.hash_map_num_entries 1 with - | Fail -> Fail + | Fail e -> Fail e | Return i0 -> begin match hash_map_remove_from_list_back t key l with - | Fail -> Fail + | Fail e -> Fail e | Return l0 -> begin match vec_index_mut_back (list_t t) self.hash_map_slots hash_mod l0 with - | Fail -> Fail + | Fail e -> Fail e | Return v -> Return (Mkhash_map_t i0 self.hash_map_max_load_factor self.hash_map_max_load v) @@ -603,65 +603,65 @@ let hash_map_remove_back (** [hashmap::test1] *) let test1_fwd : result unit = begin match hash_map_new_fwd u64 with - | Fail -> Fail + | Fail e -> Fail e | Return hm -> begin match hash_map_insert_fwd_back u64 hm 0 42 with - | Fail -> Fail + | Fail e -> Fail e | Return hm0 -> begin match hash_map_insert_fwd_back u64 hm0 128 18 with - | Fail -> Fail + | Fail e -> Fail e | Return hm1 -> begin match hash_map_insert_fwd_back u64 hm1 1024 138 with - | Fail -> Fail + | Fail e -> Fail e | Return hm2 -> begin match hash_map_insert_fwd_back u64 hm2 1056 256 with - | Fail -> Fail + | Fail e -> Fail e | Return hm3 -> begin match hash_map_get_fwd u64 hm3 128 with - | Fail -> Fail + | Fail e -> Fail e | Return i -> if not (i = 18) - then Fail + then Fail Failure else begin match hash_map_get_mut_back u64 hm3 1024 56 with - | Fail -> Fail + | Fail e -> Fail e | Return hm4 -> begin match hash_map_get_fwd u64 hm4 1024 with - | Fail -> Fail + | Fail e -> Fail e | Return i0 -> if not (i0 = 56) - then Fail + then Fail Failure else begin match hash_map_remove_fwd u64 hm4 1024 with - | Fail -> Fail + | Fail e -> Fail e | Return x -> begin match x with - | None -> Fail + | None -> Fail Failure | Some x0 -> if not (x0 = 56) - then Fail + then Fail Failure else begin match hash_map_remove_back u64 hm4 1024 with - | Fail -> Fail + | Fail e -> Fail e | Return hm5 -> begin match hash_map_get_fwd u64 hm5 0 with - | Fail -> Fail + | Fail e -> Fail e | Return i1 -> if not (i1 = 42) - then Fail + then Fail Failure else begin match hash_map_get_fwd u64 hm5 128 with - | Fail -> Fail + | Fail e -> Fail e | Return i2 -> if not (i2 = 18) - then Fail + then Fail Failure else begin match hash_map_get_fwd u64 hm5 1056 with - | Fail -> Fail + | Fail e -> Fail e | Return i3 -> if not (i3 = 256) - then Fail + then Fail Failure else Return () end end diff --git a/tests/fstar/hashmap/Hashmap.Properties.fst b/tests/fstar/hashmap/Hashmap.Properties.fst index 21a46c73..0713dc7c 100644 --- a/tests/fstar/hashmap/Hashmap.Properties.fst +++ b/tests/fstar/hashmap/Hashmap.Properties.fst @@ -502,7 +502,7 @@ val hash_map_allocate_slots_fwd_lem (requires (length slots + n <= usize_max)) (ensures ( match hash_map_allocate_slots_fwd t slots n with - | Fail -> False + | Fail _ -> False | Return slots' -> length slots' = length slots + n /\ // We leave the already allocated slots unchanged @@ -517,14 +517,14 @@ let rec hash_map_allocate_slots_fwd_lem t slots n = | 0 -> () | _ -> begin match vec_push_back (list_t t) slots ListNil with - | Fail -> () + | Fail _ -> () | Return slots1 -> begin match usize_sub n 1 with - | Fail -> () + | Fail _ -> () | Return i -> hash_map_allocate_slots_fwd_lem t slots1 i; begin match hash_map_allocate_slots_fwd t slots1 i with - | Fail -> () + | Fail _ -> () | Return slots2 -> assert(length slots1 = length slots + 1); assert(slots1 == slots @ [ListNil]); // Triggers patterns @@ -550,7 +550,7 @@ val hash_map_new_with_capacity_fwd_lem capacity * max_load_dividend <= usize_max)) (ensures ( match hash_map_new_with_capacity_fwd t capacity max_load_dividend max_load_divisor with - | Fail -> False + | Fail _ -> False | Return hm -> // The hash map invariant is satisfied hash_map_t_inv hm /\ @@ -574,13 +574,13 @@ let hash_map_new_with_capacity_fwd_lem (t : Type0) (capacity : usize) assert(length v = 0); hash_map_allocate_slots_fwd_lem t v capacity; begin match hash_map_allocate_slots_fwd t v capacity with - | Fail -> assert(False) + | Fail _ -> assert(False) | Return v0 -> begin match usize_mul capacity max_load_dividend with - | Fail -> assert(False) + | Fail _ -> assert(False) | Return i -> begin match usize_div i max_load_divisor with - | Fail -> assert(False) + | Fail _ -> assert(False) | Return i0 -> let hm = Mkhash_map_t 0 (max_load_dividend, max_load_divisor) i0 v0 in slots_t_all_nil_inv_lem v0; @@ -597,7 +597,7 @@ val hash_map_new_fwd_lem_aux (t : Type0) : Lemma (ensures ( match hash_map_new_fwd t with - | Fail -> False + | Fail _ -> False | Return hm -> // The hash map invariant is satisfied hash_map_t_inv hm /\ @@ -610,7 +610,7 @@ val hash_map_new_fwd_lem_aux (t : Type0) : let hash_map_new_fwd_lem_aux t = hash_map_new_with_capacity_fwd_lem t 32 4 5; match hash_map_new_with_capacity_fwd t 32 4 5 with - | Fail -> () + | Fail _ -> () | Return hm -> () #pop-options @@ -625,7 +625,7 @@ let rec hash_map_clear_slots_fwd_back_lem Lemma (ensures ( match hash_map_clear_slots_fwd_back t slots i with - | Fail -> False + | Fail _ -> False | Return slots' -> // The length is preserved length slots' == length slots /\ @@ -640,14 +640,14 @@ let rec hash_map_clear_slots_fwd_back_lem if b then begin match vec_index_mut_back (list_t t) slots i ListNil with - | Fail -> () + | Fail _ -> () | Return v -> begin match usize_add i 1 with - | Fail -> () + | Fail _ -> () | Return i1 -> hash_map_clear_slots_fwd_back_lem t v i1; begin match hash_map_clear_slots_fwd_back t v i1 with - | Fail -> () + | Fail _ -> () | Return slots1 -> assert(length slots1 == length slots); assert(forall (j:nat{i+1 <= j /\ j < length slots}). index slots1 j == ListNil); @@ -666,7 +666,7 @@ val hash_map_clear_fwd_back_lem_aux (requires (hash_map_t_base_inv self)) (ensures ( match hash_map_clear_fwd_back t self with - | Fail -> False + | Fail _ -> False | Return hm -> // The hash map invariant is satisfied hash_map_t_base_inv hm /\ @@ -685,7 +685,7 @@ let hash_map_clear_fwd_back_lem_aux #t self = let v = self.hash_map_slots in hash_map_clear_slots_fwd_back_lem t v 0; begin match hash_map_clear_slots_fwd_back t v 0 with - | Fail -> () + | Fail _ -> () | Return slots1 -> slots_t_al_v_all_nil_is_empty_lem slots1; let hm1 = Mkhash_map_t 0 p i slots1 in @@ -714,7 +714,7 @@ val hash_map_insert_in_list_fwd_lem Lemma (ensures ( match hash_map_insert_in_list_fwd t key value ls with - | Fail -> False + | Fail _ -> False | Return b -> b <==> (slot_t_find_s key ls == None))) (decreases (hash_map_insert_in_list_decreases t key value ls)) @@ -730,7 +730,7 @@ let rec hash_map_insert_in_list_fwd_lem t key value ls = begin hash_map_insert_in_list_fwd_lem t key value ls0; match hash_map_insert_in_list_fwd t key value ls0 with - | Fail -> () + | Fail _ -> () | Return b0 -> () end | ListNil -> @@ -769,7 +769,7 @@ val hash_map_insert_in_list_back_lem_append_s slot_t_find_s key ls == None)) (ensures ( match hash_map_insert_in_list_back t key value ls with - | Fail -> False + | Fail _ -> False | Return ls' -> list_t_v ls' == list_t_v ls @ [(key,value)])) (decreases (hash_map_insert_in_list_decreases t key value ls)) @@ -785,7 +785,7 @@ let rec hash_map_insert_in_list_back_lem_append_s t key value ls = begin hash_map_insert_in_list_back_lem_append_s t key value ls0; match hash_map_insert_in_list_back t key value ls0 with - | Fail -> () + | Fail _ -> () | Return l -> () end | ListNil -> () @@ -800,7 +800,7 @@ val hash_map_insert_in_list_back_lem_update_s Some? (find (same_key key) (list_t_v ls)))) (ensures ( match hash_map_insert_in_list_back t key value ls with - | Fail -> False + | Fail _ -> False | Return ls' -> list_t_v ls' == find_update (same_key key) (list_t_v ls) (key,value))) (decreases (hash_map_insert_in_list_decreases t key value ls)) @@ -816,7 +816,7 @@ let rec hash_map_insert_in_list_back_lem_update_s t key value ls = begin hash_map_insert_in_list_back_lem_update_s t key value ls0; match hash_map_insert_in_list_back t key value ls0 with - | Fail -> () + | Fail _ -> () | Return l -> () end | ListNil -> () @@ -829,7 +829,7 @@ val hash_map_insert_in_list_back_lem_s Lemma (ensures ( match hash_map_insert_in_list_back t key value ls with - | Fail -> False + | Fail _ -> False | Return ls' -> list_t_v ls' == hash_map_insert_in_list_s key value (list_t_v ls))) @@ -924,7 +924,7 @@ val hash_map_insert_in_list_back_lem_append slot_t_find_s key ls == None)) (ensures ( match hash_map_insert_in_list_back t key value ls with - | Fail -> False + | Fail _ -> False | Return ls' -> list_t_v ls' == list_t_v ls @ [(key,value)] /\ // The invariant is preserved @@ -1044,7 +1044,7 @@ val hash_map_insert_in_list_back_lem_update Some? (slot_t_find_s key ls))) (ensures ( match hash_map_insert_in_list_back t key value ls with - | Fail -> False + | Fail _ -> False | Return ls' -> let als = list_t_v ls in list_t_v ls' == find_update (same_key key) als (key,value) /\ @@ -1096,7 +1096,7 @@ val hash_map_insert_in_list_back_lem (requires (slot_t_inv len (hash_mod_key key len) ls)) (ensures ( match hash_map_insert_in_list_back t key value ls with - | Fail -> False + | Fail _ -> False | Return ls' -> // The invariant is preserved slot_t_inv len (hash_mod_key key len) ls' /\ @@ -1145,7 +1145,7 @@ let hash_map_insert_no_resize_s result (hash_map_s t) = // Check if the table is saturated (too many entries, and we need to insert one) let num_entries = length (flatten hm) in - if None? (hash_map_s_find hm key) && num_entries = usize_max then Fail + if None? (hash_map_s_find hm key) && num_entries = usize_max then Fail Failure else Return (hash_map_insert_no_fail_s hm key value) /// Prove that [hash_map_insert_no_resize_s] is refined by @@ -1161,7 +1161,7 @@ val hash_map_insert_no_resize_fwd_back_lem_s match hash_map_insert_no_resize_fwd_back t self key value, hash_map_insert_no_resize_s (hash_map_t_v self) key value with - | Fail, Fail -> True + | Fail _, Fail _ -> True | Return hm, Return hm_v -> hash_map_t_base_inv hm /\ hash_map_t_same_params hm self /\ @@ -1172,7 +1172,7 @@ val hash_map_insert_no_resize_fwd_back_lem_s let hash_map_insert_no_resize_fwd_back_lem_s t self key value = begin match hash_key_fwd key with - | Fail -> () + | Fail _ -> () | Return i -> let i0 = self.hash_map_num_entries in let p = self.hash_map_max_load_factor in @@ -1181,31 +1181,31 @@ let hash_map_insert_no_resize_fwd_back_lem_s t self key value = let i2 = vec_len (list_t t) v in let len = length v in begin match usize_rem i i2 with - | Fail -> () + | Fail _ -> () | Return hash_mod -> begin match vec_index_mut_fwd (list_t t) v hash_mod with - | Fail -> () + | Fail _ -> () | Return l -> begin // Checking that: list_t_v (index ...) == index (hash_map_t_v ...) ... assert(list_t_v l == index (hash_map_t_v self) hash_mod); hash_map_insert_in_list_fwd_lem t key value l; match hash_map_insert_in_list_fwd t key value l with - | Fail -> () + | Fail _ -> () | Return b -> assert(b = None? (slot_s_find key (list_t_v l))); hash_map_insert_in_list_back_lem t len key value l; if b then begin match usize_add i0 1 with - | Fail -> () + | Fail _ -> () | Return i3 -> begin match hash_map_insert_in_list_back t key value l with - | Fail -> () + | Fail _ -> () | Return l0 -> begin match vec_index_mut_back (list_t t) v hash_mod l0 with - | Fail -> () + | Fail _ -> () | Return v0 -> let self_v = hash_map_t_v self in let hm = Mkhash_map_t i3 p i1 v0 in @@ -1221,10 +1221,10 @@ let hash_map_insert_no_resize_fwd_back_lem_s t self key value = else begin match hash_map_insert_in_list_back t key value l with - | Fail -> () + | Fail _ -> () | Return l0 -> begin match vec_index_mut_back (list_t t) v hash_mod l0 with - | Fail -> () + | Fail _ -> () | Return v0 -> let self_v = hash_map_t_v self in let hm = Mkhash_map_t i0 p i1 v0 in @@ -1285,7 +1285,7 @@ val hash_map_insert_no_resize_s_lem (requires (hash_map_s_inv hm)) (ensures ( match hash_map_insert_no_resize_s hm key value with - | Fail -> + | Fail _ -> // Can fail only if we need to create a new binding in // an already saturated map hash_map_s_len hm = usize_max /\ @@ -1308,7 +1308,7 @@ val hash_map_insert_no_resize_s_get_same_lem Lemma (requires (hash_map_s_inv hm)) (ensures ( match hash_map_insert_no_resize_s hm key value with - | Fail -> True + | Fail _ -> True | Return hm' -> hash_map_s_find hm' key == Some value)) @@ -1330,7 +1330,7 @@ val hash_map_insert_no_resize_s_get_diff_lem Lemma (requires (hash_map_s_inv hm)) (ensures ( match hash_map_insert_no_resize_s hm key value with - | Fail -> True + | Fail _ -> True | Return hm' -> hash_map_s_find hm' key' == hash_map_s_find hm key')) @@ -1364,7 +1364,7 @@ let hash_map_insert_no_resize_s_get_diff_lem #t hm key value key' = type result_hash_map_s_nes (t : Type0) : Type0 = res:result (hash_map_s t) { match res with - | Fail -> True + | Fail _ -> True | Return hm -> is_pos_usize (length hm) } @@ -1378,7 +1378,7 @@ let rec hash_map_move_elements_from_list_s | [] -> Return hm | (key, value) :: ls' -> match hash_map_insert_no_resize_s hm key value with - | Fail -> Fail + | Fail e -> Fail e | Return hm' -> hash_map_move_elements_from_list_s hm' ls' @@ -1390,7 +1390,7 @@ val hash_map_move_elements_from_list_fwd_back_lem match hash_map_move_elements_from_list_fwd_back t ntable ls, hash_map_move_elements_from_list_s (hash_map_t_v ntable) (slot_t_v ls) with - | Fail, Fail -> True + | Fail _, Fail _ -> True | Return hm', Return hm_v -> hash_map_t_base_inv hm' /\ hash_map_t_v hm' == hm_v /\ @@ -1407,13 +1407,13 @@ let rec hash_map_move_elements_from_list_fwd_back_lem t ntable ls = let (_,_) :: tl_v = ls_v in hash_map_insert_no_resize_fwd_back_lem_s t ntable k v; begin match hash_map_insert_no_resize_fwd_back t ntable k v with - | Fail -> () + | Fail _ -> () | Return h -> let h_v = Return?.v (hash_map_insert_no_resize_s (hash_map_t_v ntable) k v) in assert(hash_map_t_v h == h_v); hash_map_move_elements_from_list_fwd_back_lem t h tl; begin match hash_map_move_elements_from_list_fwd_back t h tl with - | Fail -> () + | Fail _ -> () | Return h0 -> () end end @@ -1450,7 +1450,7 @@ let rec hash_map_move_elements_s_simpl (requires (True)) (ensures (fun res -> match res, hash_map_move_elements_fwd_back t ntable slots i with - | Fail, Fail -> True + | Fail _, Fail _ -> True | Return (ntable1, slots1), Return (ntable2, slots2) -> ntable1 == ntable2 /\ slots1 == slots2 @@ -1461,7 +1461,7 @@ let rec hash_map_move_elements_s_simpl then let slot = index slots i in begin match hash_map_move_elements_from_list_fwd_back t ntable slot with - | Fail -> Fail + | Fail e -> Fail e | Return hm' -> let slots' = list_update slots i ListNil in hash_map_move_elements_s_simpl t hm' slots' (i+1) @@ -1487,7 +1487,7 @@ let rec hash_map_move_elements_s begin let slot = index slots i in match hash_map_move_elements_from_list_s hm slot with - | Fail -> Fail + | Fail e -> Fail e | Return hm' -> let slots' = list_update slots i [] in hash_map_move_elements_s hm' slots' (i+1) @@ -1504,7 +1504,7 @@ val hash_map_move_elements_fwd_back_lem_refin match hash_map_move_elements_fwd_back t ntable slots i, hash_map_move_elements_s (hash_map_t_v ntable) (slots_t_v slots) i with - | Fail, Fail -> True // We will prove later that this is not possible + | Fail _, Fail _ -> True // We will prove later that this is not possible | Return (ntable', _), Return ntable'_v -> hash_map_t_base_inv ntable' /\ hash_map_t_v ntable' == ntable'_v /\ @@ -1567,27 +1567,27 @@ let rec hash_map_move_elements_fwd_back_lem_refin t ntable slots i = if b then begin match vec_index_mut_fwd (list_t t) slots i with - | Fail -> () + | Fail _ -> () | Return l -> let l0 = mem_replace_fwd (list_t t) l ListNil in assert(l0 == l); hash_map_move_elements_from_list_fwd_back_lem t ntable l0; begin match hash_map_move_elements_from_list_fwd_back t ntable l0 with - | Fail -> () + | Fail _ -> () | Return h -> let l1 = mem_replace_back (list_t t) l ListNil in assert(l1 == ListNil); assert(slot_t_v #t ListNil == []); // THIS IS IMPORTANT begin match vec_index_mut_back (list_t t) slots i l1 with - | Fail -> () + | Fail _ -> () | Return v -> begin match usize_add i 1 with - | Fail -> () + | Fail _ -> () | Return i1 -> hash_map_move_elements_fwd_back_lem_refin t h v i1; begin match hash_map_move_elements_fwd_back t h v i1 with - | Fail -> - assert(hash_map_move_elements_fwd_back t ntable slots i == Fail); + | Fail _ -> + assert(Fail? (hash_map_move_elements_fwd_back t ntable slots i)); () | Return (ntable', v0) -> () end @@ -1617,7 +1617,7 @@ let rec hash_map_move_elements_s_flat | [] -> Return ntable | (k,v) :: slots' -> match hash_map_insert_no_resize_s ntable k v with - | Fail -> Fail + | Fail e -> Fail e | Return ntable' -> hash_map_move_elements_s_flat ntable' slots' @@ -1718,7 +1718,7 @@ let rec hash_map_move_elements_from_list_s_as_flat_lem #t hm ls = | [] -> () | (key, value) :: ls' -> match hash_map_insert_no_resize_s hm key value with - | Fail -> () + | Fail _ -> () | Return hm' -> hash_map_move_elements_from_list_s_as_flat_lem hm' ls' #pop-options @@ -1728,7 +1728,7 @@ let hash_map_move_elements_s_flat_comp (#t : Type0) (hm : hash_map_s_nes t) (slot0 slot1 : slot_s t) : Tot (result_hash_map_s_nes t) = match hash_map_move_elements_s_flat hm slot0 with - | Fail -> Fail + | Fail e -> Fail e | Return hm1 -> hash_map_move_elements_s_flat hm1 slot1 /// High-level desc: @@ -1740,7 +1740,7 @@ val hash_map_move_elements_s_flat_append_lem match hash_map_move_elements_s_flat_comp hm slot0 slot1, hash_map_move_elements_s_flat hm (slot0 @ slot1) with - | Fail, Fail -> True + | Fail _, Fail _ -> True | Return hm1, Return hm2 -> hm1 == hm2 | _ -> False)) (decreases (slot0)) @@ -1751,7 +1751,7 @@ let rec hash_map_move_elements_s_flat_append_lem #t hm slot0 slot1 = | [] -> () | (k,v) :: slot0' -> match hash_map_insert_no_resize_s hm k v with - | Fail -> () + | Fail _ -> () | Return hm' -> hash_map_move_elements_s_flat_append_lem hm' slot0' slot1 #pop-options @@ -1784,7 +1784,7 @@ val hash_map_move_elements_s_lem_refin_flat match hash_map_move_elements_s hm slots i, hash_map_move_elements_s_flat hm (flatten_i slots i) with - | Fail, Fail -> True + | Fail _, Fail _ -> True | Return hm, Return hm' -> hm == hm' | _ -> False)) (decreases (length slots - i)) @@ -1797,10 +1797,10 @@ let rec hash_map_move_elements_s_lem_refin_flat #t hm slots i = let slot = index slots i in hash_map_move_elements_from_list_s_as_flat_lem hm slot; match hash_map_move_elements_from_list_s hm slot with - | Fail -> + | Fail _ -> assert(flatten_i slots i == slot @ flatten_i slots (i+1)); hash_map_move_elements_s_flat_append_lem hm slot (flatten_i slots (i+1)); - assert(hash_map_move_elements_s_flat hm (flatten_i slots i) == Fail) + assert(Fail? (hash_map_move_elements_s_flat hm (flatten_i slots i))) | Return hm' -> let slots' = list_update slots i [] in flatten_i_same_suffix slots slots' (i+1); @@ -1859,7 +1859,7 @@ val hash_map_move_elements_s_flat_lem hash_map_s_len hm + length al <= usize_max)) (ensures ( match hash_map_move_elements_s_flat hm al with - | Fail -> False // We can't fail + | Fail _ -> False // We can't fail | Return hm' -> // The invariant is preserved hash_map_s_inv hm' /\ @@ -1876,7 +1876,7 @@ let rec hash_map_move_elements_s_flat_lem #t hm al = | (k,v) :: al' -> hash_map_insert_no_resize_s_lem hm k v; match hash_map_insert_no_resize_s hm k v with - | Fail -> () + | Fail _ -> () | Return hm' -> assert(hash_map_s_inv hm'); assert(assoc_list_inv al'); @@ -2211,7 +2211,7 @@ let hash_map_move_elements_fwd_back_lem t ntable slots = match hash_map_move_elements_fwd_back t ntable slots 0, hash_map_move_elements_s ntable_v slots_v 0 with - | Fail, Fail -> () + | Fail _, Fail _ -> () | Return (ntable', _), Return ntable'_v -> assert(hash_map_t_base_inv ntable'); assert(hash_map_t_v ntable' == ntable'_v) @@ -2222,7 +2222,7 @@ let hash_map_move_elements_fwd_back_lem t ntable slots = match hash_map_move_elements_s ntable_v slots_v 0, hash_map_move_elements_s_flat ntable_v (flatten_i slots_v 0) with - | Fail, Fail -> () + | Fail _, Fail _ -> () | Return hm, Return hm' -> assert(hm == hm') | _ -> assert(False) end; @@ -2258,10 +2258,10 @@ let hash_map_try_resize_s_simpl if capacity <= (usize_max / 2) / divid then let ncapacity : usize = capacity * 2 in begin match hash_map_new_with_capacity_fwd t ncapacity divid divis with - | Fail -> Fail + | Fail e -> Fail e | Return ntable -> match hash_map_move_elements_fwd_back t ntable hm.hash_map_slots 0 with - | Fail -> Fail + | Fail e -> Fail e | Return (ntable', _) -> let hm = { hm with hash_map_slots = ntable'.hash_map_slots; @@ -2294,7 +2294,7 @@ val hash_map_try_resize_fwd_back_lem_refin match hash_map_try_resize_fwd_back t self, hash_map_try_resize_s_simpl self with - | Fail, Fail -> True + | Fail _, Fail _ -> True | Return hm1, Return hm2 -> hm1 == hm2 | _ -> False)) @@ -2420,7 +2420,7 @@ val hash_map_try_resize_s_simpl_lem (#t : Type0) (hm : hash_map_t t) : )) (ensures ( match hash_map_try_resize_s_simpl hm with - | Fail -> False + | Fail _ -> False | Return hm' -> // The full invariant is now satisfied (the full invariant is "base // invariant" + the map is not overloaded (or can't be resized because @@ -2442,7 +2442,7 @@ let hash_map_try_resize_s_simpl_lem #t hm = new_max_load_lem (hash_map_t_len_s hm) capacity divid divis; hash_map_new_with_capacity_fwd_lem t ncapacity divid divis; match hash_map_new_with_capacity_fwd t ncapacity divid divis with - | Fail -> () + | Fail _ -> () | Return ntable -> let slots = hm.hash_map_slots in let al = flatten (slots_t_v slots) in @@ -2461,7 +2461,7 @@ let hash_map_try_resize_s_simpl_lem #t hm = assert(forall (k:key). hash_map_t_find_s ntable k == None); hash_map_move_elements_fwd_back_lem t ntable hm.hash_map_slots; match hash_map_move_elements_fwd_back t ntable hm.hash_map_slots 0 with - | Fail -> () + | Fail _ -> () | Return (ntable', _) -> hash_map_is_assoc_list_lem hm; assert(hash_map_is_assoc_list hm (hash_map_t_al_v hm)); @@ -2502,7 +2502,7 @@ val hash_map_try_resize_fwd_back_lem (#t : Type0) (hm : hash_map_t t) : length hm.hash_map_slots * 2 * dividend > usize_max))) (ensures ( match hash_map_try_resize_fwd_back t hm with - | Fail -> False + | Fail _ -> False | Return hm' -> // The full invariant is now satisfied (the full invariant is "base // invariant" + the map is not overloaded (or can't be resized because @@ -2525,7 +2525,7 @@ let hash_map_insert_s (#t : Type0) (self : hash_map_t t) (key : usize) (value : t) : result (hash_map_t t) = match hash_map_insert_no_resize_fwd_back t self key value with - | Fail -> Fail + | Fail e -> Fail e | Return hm' -> if hash_map_t_len_s hm' > hm'.hash_map_max_load then hash_map_try_resize_fwd_back t hm' @@ -2538,7 +2538,7 @@ val hash_map_insert_fwd_back_lem_refin match hash_map_insert_fwd_back t self key value, hash_map_insert_s self key value with - | Fail, Fail -> True + | Fail _, Fail _ -> True | Return hm1, Return hm2 -> hm1 == hm2 | _ -> False)) @@ -2563,7 +2563,7 @@ val hash_map_insert_fwd_back_lem_aux Lemma (requires (hash_map_t_inv self)) (ensures ( match hash_map_insert_fwd_back t self key value with - | Fail -> + | Fail _ -> // We can fail only if: // - the key is not in the map and we need to add it // - we are already saturated @@ -2585,7 +2585,7 @@ let hash_map_insert_fwd_back_lem_aux #t self key value = hash_map_insert_no_resize_fwd_back_lem_s t self key value; hash_map_insert_no_resize_s_lem (hash_map_t_v self) key value; match hash_map_insert_no_resize_fwd_back t self key value with - | Fail -> () + | Fail _ -> () | Return hm' -> // Expanding the post of [hash_map_insert_no_resize_fwd_back_lem_s] let self_v = hash_map_t_v self in @@ -2634,7 +2634,7 @@ val hash_map_contains_key_in_list_fwd_lem Lemma (ensures ( match hash_map_contains_key_in_list_fwd t key ls with - | Fail -> False + | Fail _ -> False | Return b -> b = Some? (slot_t_find_s key ls))) @@ -2650,7 +2650,7 @@ let rec hash_map_contains_key_in_list_fwd_lem #t key ls = begin hash_map_contains_key_in_list_fwd_lem key ls0; match hash_map_contains_key_in_list_fwd t key ls0 with - | Fail -> () + | Fail _ -> () | Return b0 -> () end | ListNil -> () @@ -2663,24 +2663,24 @@ val hash_map_contains_key_fwd_lem_aux Lemma (ensures ( match hash_map_contains_key_fwd t self key with - | Fail -> False + | Fail _ -> False | Return b -> b = Some? (hash_map_t_find_s self key))) let hash_map_contains_key_fwd_lem_aux #t self key = begin match hash_key_fwd key with - | Fail -> () + | Fail _ -> () | Return i -> let v = self.hash_map_slots in let i0 = vec_len (list_t t) v in begin match usize_rem i i0 with - | Fail -> () + | Fail _ -> () | Return hash_mod -> begin match vec_index_fwd (list_t t) v hash_mod with - | Fail -> () + | Fail _ -> () | Return l -> hash_map_contains_key_in_list_fwd_lem key l; begin match hash_map_contains_key_in_list_fwd t key l with - | Fail -> () + | Fail _ -> () | Return b -> () end end @@ -2700,7 +2700,7 @@ val hash_map_get_in_list_fwd_lem Lemma (ensures ( match hash_map_get_in_list_fwd t key ls, slot_t_find_s key ls with - | Fail, None -> True + | Fail _, None -> True | Return x, Some x' -> x == x' | _ -> False)) @@ -2715,7 +2715,7 @@ let rec hash_map_get_in_list_fwd_lem #t key ls = begin hash_map_get_in_list_fwd_lem key ls0; match hash_map_get_in_list_fwd t key ls0 with - | Fail -> () + | Fail _ -> () | Return x -> () end | ListNil -> () @@ -2729,26 +2729,26 @@ val hash_map_get_fwd_lem_aux Lemma (ensures ( match hash_map_get_fwd t self key, hash_map_t_find_s self key with - | Fail, None -> True + | Fail _, None -> True | Return x, Some x' -> x == x' | _ -> False)) let hash_map_get_fwd_lem_aux #t self key = begin match hash_key_fwd key with - | Fail -> () + | Fail _ -> () | Return i -> let v = self.hash_map_slots in let i0 = vec_len (list_t t) v in begin match usize_rem i i0 with - | Fail -> () + | Fail _ -> () | Return hash_mod -> begin match vec_index_fwd (list_t t) v hash_mod with - | Fail -> () + | Fail _ -> () | Return l -> begin hash_map_get_in_list_fwd_lem key l; match hash_map_get_in_list_fwd t key l with - | Fail -> () + | Fail _ -> () | Return x -> () end end @@ -2768,7 +2768,7 @@ val hash_map_get_mut_in_list_fwd_lem Lemma (ensures ( match hash_map_get_mut_in_list_fwd t key ls, slot_t_find_s key ls with - | Fail, None -> True + | Fail _, None -> True | Return x, Some x' -> x == x' | _ -> False)) @@ -2783,7 +2783,7 @@ let rec hash_map_get_mut_in_list_fwd_lem #t key ls = begin hash_map_get_mut_in_list_fwd_lem key ls0; match hash_map_get_mut_in_list_fwd t key ls0 with - | Fail -> () + | Fail _ -> () | Return x -> () end | ListNil -> () @@ -2797,26 +2797,26 @@ val hash_map_get_mut_fwd_lem_aux Lemma (ensures ( match hash_map_get_mut_fwd t self key, hash_map_t_find_s self key with - | Fail, None -> True + | Fail _, None -> True | Return x, Some x' -> x == x' | _ -> False)) let hash_map_get_mut_fwd_lem_aux #t self key = begin match hash_key_fwd key with - | Fail -> () + | Fail _ -> () | Return i -> let v = self.hash_map_slots in let i0 = vec_len (list_t t) v in begin match usize_rem i i0 with - | Fail -> () + | Fail _ -> () | Return hash_mod -> begin match vec_index_fwd (list_t t) v hash_mod with - | Fail -> () + | Fail _ -> () | Return l -> begin hash_map_get_mut_in_list_fwd_lem key l; match hash_map_get_mut_in_list_fwd t key l with - | Fail -> () + | Fail _ -> () | Return x -> () end end @@ -2836,7 +2836,7 @@ val hash_map_get_mut_in_list_back_lem (requires (Some? (slot_t_find_s key ls))) (ensures ( match hash_map_get_mut_in_list_back t key ls ret with - | Fail -> False + | Fail _ -> False | Return ls' -> list_t_v ls' == find_update (same_key key) (list_t_v ls) (key,ret) | _ -> False)) @@ -2851,7 +2851,7 @@ let rec hash_map_get_mut_in_list_back_lem #t key ls ret = begin hash_map_get_mut_in_list_back_lem key ls0 ret; match hash_map_get_mut_in_list_back t key ls0 ret with - | Fail -> () + | Fail _ -> () | Return l -> let ls1 = ListCons ckey cvalue l in () end | ListNil -> () @@ -2868,13 +2868,13 @@ val hash_map_get_mut_back_lem_refin (requires (Some? (hash_map_t_find_s self key))) (ensures ( match hash_map_get_mut_back t self key ret with - | Fail -> False + | Fail _ -> False | Return hm' -> hash_map_t_v hm' == hash_map_insert_no_fail_s (hash_map_t_v self) key ret)) let hash_map_get_mut_back_lem_refin #t self key ret = begin match hash_key_fwd key with - | Fail -> () + | Fail _ -> () | Return i -> let i0 = self.hash_map_num_entries in let p = self.hash_map_max_load_factor in @@ -2882,18 +2882,18 @@ let hash_map_get_mut_back_lem_refin #t self key ret = let v = self.hash_map_slots in let i2 = vec_len (list_t t) v in begin match usize_rem i i2 with - | Fail -> () + | Fail _ -> () | Return hash_mod -> begin match vec_index_mut_fwd (list_t t) v hash_mod with - | Fail -> () + | Fail _ -> () | Return l -> begin hash_map_get_mut_in_list_back_lem key l ret; match hash_map_get_mut_in_list_back t key l ret with - | Fail -> () + | Fail _ -> () | Return l0 -> begin match vec_index_mut_back (list_t t) v hash_mod l0 with - | Fail -> () + | Fail _ -> () | Return v0 -> let self0 = Mkhash_map_t i0 p i1 v0 in () end end @@ -2911,7 +2911,7 @@ val hash_map_get_mut_back_lem_aux Some? (hash_map_t_find_s hm key))) (ensures ( match hash_map_get_mut_back t hm key ret with - | Fail -> False + | Fail _ -> False | Return hm' -> // Functional spec hash_map_t_v hm' == hash_map_insert_no_fail_s (hash_map_t_v hm) key ret /\ @@ -2928,7 +2928,7 @@ let hash_map_get_mut_back_lem_aux #t hm key ret = let hm_v = hash_map_t_v hm in hash_map_get_mut_back_lem_refin hm key ret; match hash_map_get_mut_back t hm key ret with - | Fail -> assert(False) + | Fail _ -> assert(False) | Return hm' -> hash_map_insert_no_fail_s_lem hm_v key ret @@ -2942,7 +2942,7 @@ val hash_map_remove_from_list_fwd_lem Lemma (ensures ( match hash_map_remove_from_list_fwd t key ls with - | Fail -> False + | Fail _ -> False | Return opt_x -> opt_x == slot_t_find_s key ls /\ (Some? opt_x ==> length (slot_t_v ls) > 0))) @@ -2963,7 +2963,7 @@ let rec hash_map_remove_from_list_fwd_lem #t key ls = begin hash_map_remove_from_list_fwd_lem key tl; match hash_map_remove_from_list_fwd t key tl with - | Fail -> () + | Fail _ -> () | Return opt -> () end | ListNil -> () @@ -2979,26 +2979,26 @@ val hash_map_remove_fwd_lem_aux hash_map_t_inv self)) (ensures ( match hash_map_remove_fwd t self key with - | Fail -> False + | Fail _ -> False | Return opt_x -> opt_x == hash_map_t_find_s self key)) let hash_map_remove_fwd_lem_aux #t self key = begin match hash_key_fwd key with - | Fail -> () + | Fail _ -> () | Return i -> let i0 = self.hash_map_num_entries in let v = self.hash_map_slots in let i1 = vec_len (list_t t) v in begin match usize_rem i i1 with - | Fail -> () + | Fail _ -> () | Return hash_mod -> begin match vec_index_mut_fwd (list_t t) v hash_mod with - | Fail -> () + | Fail _ -> () | Return l -> begin hash_map_remove_from_list_fwd_lem key l; match hash_map_remove_from_list_fwd t key l with - | Fail -> () + | Fail _ -> () | Return x -> begin match x with | None -> () @@ -3008,7 +3008,7 @@ let hash_map_remove_fwd_lem_aux #t self key = assert(length (list_t_v #t l) > 0); length_flatten_index (hash_map_t_v self) hash_mod; match usize_sub i0 1 with - | Fail -> () + | Fail _ -> () | Return _ -> () end end @@ -3036,7 +3036,7 @@ val hash_map_remove_from_list_back_lem_refin Lemma (ensures ( match hash_map_remove_from_list_back t key ls with - | Fail -> False + | Fail _ -> False | Return ls' -> list_t_v ls' == hash_map_remove_from_list_s key (list_t_v ls) /\ // The length is decremented, iff the key was in the slot @@ -3062,7 +3062,7 @@ let rec hash_map_remove_from_list_back_lem_refin #t key ls = begin hash_map_remove_from_list_back_lem_refin key tl; match hash_map_remove_from_list_back t key tl with - | Fail -> () + | Fail _ -> () | Return l -> let ls0 = ListCons ckey x l in () end | ListNil -> () @@ -3089,7 +3089,7 @@ val hash_map_remove_back_lem_refin hash_map_t_inv self)) (ensures ( match hash_map_remove_back t self key with - | Fail -> False + | Fail _ -> False | Return hm' -> hash_map_t_same_params hm' self /\ hash_map_t_v hm' == hash_map_remove_s (hash_map_t_v self) key /\ @@ -3102,7 +3102,7 @@ val hash_map_remove_back_lem_refin let hash_map_remove_back_lem_refin #t self key = begin match hash_key_fwd key with - | Fail -> () + | Fail _ -> () | Return i -> let i0 = self.hash_map_num_entries in let p = self.hash_map_max_load_factor in @@ -3110,27 +3110,27 @@ let hash_map_remove_back_lem_refin #t self key = let v = self.hash_map_slots in let i2 = vec_len (list_t t) v in begin match usize_rem i i2 with - | Fail -> () + | Fail _ -> () | Return hash_mod -> begin match vec_index_mut_fwd (list_t t) v hash_mod with - | Fail -> () + | Fail _ -> () | Return l -> begin hash_map_remove_from_list_fwd_lem key l; match hash_map_remove_from_list_fwd t key l with - | Fail -> () + | Fail _ -> () | Return x -> begin match x with | None -> begin hash_map_remove_from_list_back_lem_refin key l; match hash_map_remove_from_list_back t key l with - | Fail -> () + | Fail _ -> () | Return l0 -> begin length_flatten_update (slots_t_v v) hash_mod (list_t_v l0); match vec_index_mut_back (list_t t) v hash_mod l0 with - | Fail -> () + | Fail _ -> () | Return v0 -> () end end @@ -3140,17 +3140,17 @@ let hash_map_remove_back_lem_refin #t self key = assert(length (list_t_v #t l) > 0); length_flatten_index (hash_map_t_v self) hash_mod; match usize_sub i0 1 with - | Fail -> () + | Fail _ -> () | Return i3 -> begin hash_map_remove_from_list_back_lem_refin key l; match hash_map_remove_from_list_back t key l with - | Fail -> () + | Fail _ -> () | Return l0 -> begin length_flatten_update (slots_t_v v) hash_mod (list_t_v l0); match vec_index_mut_back (list_t t) v hash_mod l0 with - | Fail -> () + | Fail _ -> () | Return v0 -> () end end @@ -3224,7 +3224,7 @@ val hash_map_remove_back_lem_aux (requires (hash_map_t_inv self)) (ensures ( match hash_map_remove_back t self key with - | Fail -> False + | Fail _ -> False | Return hm' -> hash_map_t_inv self /\ hash_map_t_same_params hm' self /\ diff --git a/tests/fstar/hashmap/Hashmap.Properties.fsti b/tests/fstar/hashmap/Hashmap.Properties.fsti index 756ae687..0a4f0134 100644 --- a/tests/fstar/hashmap/Hashmap.Properties.fsti +++ b/tests/fstar/hashmap/Hashmap.Properties.fsti @@ -67,7 +67,7 @@ val hash_map_new_fwd_lem (t : Type0) : Lemma (ensures ( match hash_map_new_fwd t with - | Fail -> False + | Fail _ -> False | Return hm -> // The hash map invariant is satisfied hash_map_t_inv hm /\ @@ -85,7 +85,7 @@ val hash_map_clear_fwd_back_lem (requires (hash_map_t_inv self)) (ensures ( match hash_map_clear_fwd_back t self with - | Fail -> False + | Fail _ -> False | Return hm -> // The hash map invariant is satisfied hash_map_t_inv hm /\ @@ -102,7 +102,7 @@ val hash_map_len_fwd_lem (#t : Type0) (self : hash_map_t t) : (requires (hash_map_t_inv self)) (ensures ( match hash_map_len_fwd t self with - | Fail -> False + | Fail _ -> False | Return l -> l = len_s self)) @@ -120,7 +120,7 @@ val hash_map_insert_fwd_back_lem (requires (hash_map_t_inv self)) (ensures ( match hash_map_insert_fwd_back t self key value with - | Fail -> + | Fail _ -> // We can fail only if: // - the key is not in the map and we thus need to add it None? (find_s self key) /\ @@ -151,7 +151,7 @@ val hash_map_contains_key_fwd_lem (requires (hash_map_t_inv self)) (ensures ( match hash_map_contains_key_fwd t self key with - | Fail -> False + | Fail _ -> False | Return b -> b = Some? (find_s self key))) (**** [get'fwd] *) @@ -163,7 +163,7 @@ val hash_map_get_fwd_lem (requires (hash_map_t_inv self)) (ensures ( match hash_map_get_fwd t self key, find_s self key with - | Fail, None -> True + | Fail _, None -> True | Return x, Some x' -> x == x' | _ -> False)) @@ -181,7 +181,7 @@ val hash_map_get_mut_fwd_lem (requires (hash_map_t_inv self)) (ensures ( match hash_map_get_mut_fwd t self key, find_s self key with - | Fail, None -> True + | Fail _, None -> True | Return x, Some x' -> x == x' | _ -> False)) @@ -211,7 +211,7 @@ val hash_map_get_mut_back_lem Some? (find_s hm key))) (ensures ( match hash_map_get_mut_back t hm key ret with - | Fail -> False // Can't fail + | Fail _ -> False // Can't fail | Return hm' -> // The invariant is preserved hash_map_t_inv hm' /\ @@ -234,7 +234,7 @@ val hash_map_remove_fwd_lem (requires (hash_map_t_inv self)) (ensures ( match hash_map_remove_fwd t self key with - | Fail -> False + | Fail _ -> False | Return opt_x -> opt_x == find_s self key)) @@ -249,7 +249,7 @@ val hash_map_remove_back_lem (requires (hash_map_t_inv self)) (ensures ( match hash_map_remove_back t self key with - | Fail -> False + | Fail _ -> False | Return hm' -> // The invariant is preserved hash_map_t_inv self /\ diff --git a/tests/fstar/hashmap/Primitives.fst b/tests/fstar/hashmap/Primitives.fst index 96138e46..82622656 100644 --- a/tests/fstar/hashmap/Primitives.fst +++ b/tests/fstar/hashmap/Primitives.fst @@ -18,9 +18,13 @@ let rec list_update #a ls i x = #pop-options (*** Result *) +type error : Type0 = +| Failure +| OutOfFuel + type result (a : Type0) : Type0 = | Return : v:a -> result a -| Fail : result a +| Fail : e:error -> result a // Monadic bind and return. // Re-definining those allows us to customize the result of the monadic notations @@ -29,10 +33,10 @@ let return (#a : Type0) (x:a) : result a = Return x let bind (#a #b : Type0) (m : result a) (f : a -> result b) : result b = match m with | Return x -> f x - | Fail -> Fail + | Fail e -> Fail e // Monadic assert(...) -let massert (b:bool) : result unit = if b then Return () else Fail +let massert (b:bool) : result unit = if b then Return () else Fail Failure // Normalize and unwrap a successful result (used for globals). let eval_global (#a : Type0) (x : result a{Return? (normalize_term x)}) : a = Return?.v x @@ -119,12 +123,12 @@ let scalar_max (ty : scalar_ty) : int = type scalar (ty : scalar_ty) : eqtype = x:int{scalar_min ty <= x && x <= scalar_max ty} let mk_scalar (ty : scalar_ty) (x : int) : result (scalar ty) = - if scalar_min ty <= x && scalar_max ty >= x then Return x else Fail + if scalar_min ty <= x && scalar_max ty >= x then Return x else Fail Failure let scalar_neg (#ty : scalar_ty) (x : scalar ty) : result (scalar ty) = mk_scalar ty (-x) let scalar_div (#ty : scalar_ty) (x : scalar ty) (y : scalar ty) : result (scalar ty) = - if y <> 0 then mk_scalar ty (x / y) else Fail + if y <> 0 then mk_scalar ty (x / y) else Fail Failure /// The remainder operation let int_rem (x : int) (y : int{y <> 0}) : int = @@ -137,7 +141,7 @@ let _ = assert_norm(int_rem 1 (-2) = 1) let _ = assert_norm(int_rem (-1) (-2) = -1) let scalar_rem (#ty : scalar_ty) (x : scalar ty) (y : scalar ty) : result (scalar ty) = - if y <> 0 then mk_scalar ty (int_rem x y) else Fail + if y <> 0 then mk_scalar ty (int_rem x y) else Fail Failure let scalar_add (#ty : scalar_ty) (x : scalar ty) (y : scalar ty) : result (scalar ty) = mk_scalar ty (x + y) @@ -258,7 +262,7 @@ let vec_push_back (a : Type0) (v : vec a) (x : a) : (requires True) (ensures (fun res -> match res with - | Fail -> True + | Fail e -> e == Failure | Return v' -> length v' = length v + 1)) = if length v < usize_max then begin (**) assert_norm(length [x] == 1); @@ -266,22 +270,22 @@ let vec_push_back (a : Type0) (v : vec a) (x : a) : (**) assert(length (append v [x]) = length v + 1); Return (append v [x]) end - else Fail + else Fail Failure // The **forward** function shouldn't be used let vec_insert_fwd (a : Type0) (v : vec a) (i : usize) (x : a) : result unit = - if i < length v then Return () else Fail + if i < length v then Return () else Fail Failure let vec_insert_back (a : Type0) (v : vec a) (i : usize) (x : a) : result (vec a) = - if i < length v then Return (list_update v i x) else Fail + if i < length v then Return (list_update v i x) else Fail Failure // The **backward** function shouldn't be used let vec_index_fwd (a : Type0) (v : vec a) (i : usize) : result a = - if i < length v then Return (index v i) else Fail + if i < length v then Return (index v i) else Fail Failure let vec_index_back (a : Type0) (v : vec a) (i : usize) (x : a) : result unit = - if i < length v then Return () else Fail + if i < length v then Return () else Fail Failure let vec_index_mut_fwd (a : Type0) (v : vec a) (i : usize) : result a = - if i < length v then Return (index v i) else Fail + if i < length v then Return (index v i) else Fail Failure let vec_index_mut_back (a : Type0) (v : vec a) (i : usize) (nx : a) : result (vec a) = - if i < length v then Return (list_update v i nx) else Fail + if i < length v then Return (list_update v i nx) else Fail Failure diff --git a/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst b/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst index 82b44dbd..d6da4562 100644 --- a/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst +++ b/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst @@ -21,13 +21,13 @@ let rec hashmap_hash_map_allocate_slots_fwd then Return slots else begin match vec_push_back (hashmap_list_t t) slots HashmapListNil with - | Fail -> Fail + | Fail e -> Fail e | Return slots0 -> begin match usize_sub n 1 with - | Fail -> Fail + | Fail e -> Fail e | Return i -> begin match hashmap_hash_map_allocate_slots_fwd t slots0 i with - | Fail -> Fail + | Fail e -> Fail e | Return v -> Return v end end @@ -41,13 +41,13 @@ let hashmap_hash_map_new_with_capacity_fwd = let v = vec_new (hashmap_list_t t) in begin match hashmap_hash_map_allocate_slots_fwd t v capacity with - | Fail -> Fail + | Fail e -> Fail e | Return slots -> begin match usize_mul capacity max_load_dividend with - | Fail -> Fail + | Fail e -> Fail e | Return i -> begin match usize_div i max_load_divisor with - | Fail -> Fail + | Fail e -> Fail e | Return i0 -> Return (Mkhashmap_hash_map_t 0 (max_load_dividend, max_load_divisor) i0 slots) @@ -58,7 +58,7 @@ let hashmap_hash_map_new_with_capacity_fwd (** [hashmap_main::hashmap::HashMap::{0}::new] *) let hashmap_hash_map_new_fwd (t : Type0) : result (hashmap_hash_map_t t) = begin match hashmap_hash_map_new_with_capacity_fwd t 32 4 5 with - | Fail -> Fail + | Fail e -> Fail e | Return hm -> Return hm end @@ -73,13 +73,13 @@ let rec hashmap_hash_map_clear_slots_fwd_back then begin match vec_index_mut_back (hashmap_list_t t) slots i HashmapListNil with - | Fail -> Fail + | Fail e -> Fail e | Return slots0 -> begin match usize_add i 1 with - | Fail -> Fail + | Fail e -> Fail e | Return i1 -> begin match hashmap_hash_map_clear_slots_fwd_back t slots0 i1 with - | Fail -> Fail + | Fail e -> Fail e | Return slots1 -> Return slots1 end end @@ -91,7 +91,7 @@ let hashmap_hash_map_clear_fwd_back (t : Type0) (self : hashmap_hash_map_t t) : result (hashmap_hash_map_t t) = begin match hashmap_hash_map_clear_slots_fwd_back t self.hashmap_hash_map_slots 0 with - | Fail -> Fail + | Fail e -> Fail e | Return v -> Return (Mkhashmap_hash_map_t 0 self.hashmap_hash_map_max_load_factor self.hashmap_hash_map_max_load v) @@ -114,7 +114,7 @@ let rec hashmap_hash_map_insert_in_list_fwd then Return false else begin match hashmap_hash_map_insert_in_list_fwd t key value ls0 with - | Fail -> Fail + | Fail e -> Fail e | Return b -> Return b end | HashmapListNil -> Return true @@ -132,7 +132,7 @@ let rec hashmap_hash_map_insert_in_list_back then Return (HashmapListCons ckey value ls0) else begin match hashmap_hash_map_insert_in_list_back t key value ls0 with - | Fail -> Fail + | Fail e -> Fail e | Return ls1 -> Return (HashmapListCons ckey cvalue ls1) end | HashmapListNil -> @@ -145,33 +145,33 @@ let hashmap_hash_map_insert_no_resize_fwd_back result (hashmap_hash_map_t t) = begin match hashmap_hash_key_fwd key with - | Fail -> Fail + | Fail e -> Fail e | Return hash -> let i = vec_len (hashmap_list_t t) self.hashmap_hash_map_slots in begin match usize_rem hash i with - | Fail -> Fail + | Fail e -> Fail e | Return hash_mod -> begin match vec_index_mut_fwd (hashmap_list_t t) self.hashmap_hash_map_slots hash_mod with - | Fail -> Fail + | Fail e -> Fail e | Return l -> begin match hashmap_hash_map_insert_in_list_fwd t key value l with - | Fail -> Fail + | Fail e -> Fail e | Return inserted -> if inserted then begin match usize_add self.hashmap_hash_map_num_entries 1 with - | Fail -> Fail + | Fail e -> Fail e | Return i0 -> begin match hashmap_hash_map_insert_in_list_back t key value l with - | Fail -> Fail + | Fail e -> Fail e | Return l0 -> begin match vec_index_mut_back (hashmap_list_t t) self.hashmap_hash_map_slots hash_mod l0 with - | Fail -> Fail + | Fail e -> Fail e | Return v -> Return (Mkhashmap_hash_map_t i0 self.hashmap_hash_map_max_load_factor @@ -181,12 +181,12 @@ let hashmap_hash_map_insert_no_resize_fwd_back end else begin match hashmap_hash_map_insert_in_list_back t key value l with - | Fail -> Fail + | Fail e -> Fail e | Return l0 -> begin match vec_index_mut_back (hashmap_list_t t) self.hashmap_hash_map_slots hash_mod l0 with - | Fail -> Fail + | Fail e -> Fail e | Return v -> Return (Mkhashmap_hash_map_t self.hashmap_hash_map_num_entries self.hashmap_hash_map_max_load_factor @@ -211,11 +211,11 @@ let rec hashmap_hash_map_move_elements_from_list_fwd_back begin match ls with | HashmapListCons k v tl -> begin match hashmap_hash_map_insert_no_resize_fwd_back t ntable k v with - | Fail -> Fail + | Fail e -> Fail e | Return ntable0 -> begin match hashmap_hash_map_move_elements_from_list_fwd_back t ntable0 tl with - | Fail -> Fail + | Fail e -> Fail e | Return ntable1 -> Return ntable1 end end @@ -233,23 +233,23 @@ let rec hashmap_hash_map_move_elements_fwd_back if i < i0 then begin match vec_index_mut_fwd (hashmap_list_t t) slots i with - | Fail -> Fail + | Fail e -> Fail e | Return l -> let ls = mem_replace_fwd (hashmap_list_t t) l HashmapListNil in begin match hashmap_hash_map_move_elements_from_list_fwd_back t ntable ls with - | Fail -> Fail + | Fail e -> Fail e | Return ntable0 -> let l0 = mem_replace_back (hashmap_list_t t) l HashmapListNil in begin match vec_index_mut_back (hashmap_list_t t) slots i l0 with - | Fail -> Fail + | Fail e -> Fail e | Return slots0 -> begin match usize_add i 1 with - | Fail -> Fail + | Fail e -> Fail e | Return i1 -> begin match hashmap_hash_map_move_elements_fwd_back t ntable0 slots0 i1 with - | Fail -> Fail + | Fail e -> Fail e | Return (ntable1, slots1) -> Return (ntable1, slots1) end end @@ -262,28 +262,28 @@ let rec hashmap_hash_map_move_elements_fwd_back let hashmap_hash_map_try_resize_fwd_back (t : Type0) (self : hashmap_hash_map_t t) : result (hashmap_hash_map_t t) = begin match scalar_cast U32 Usize core_num_u32_max_c with - | Fail -> Fail + | Fail e -> Fail e | Return max_usize -> let capacity = vec_len (hashmap_list_t t) self.hashmap_hash_map_slots in begin match usize_div max_usize 2 with - | Fail -> Fail + | Fail e -> Fail e | Return n1 -> let (i, i0) = self.hashmap_hash_map_max_load_factor in begin match usize_div n1 i with - | Fail -> Fail + | Fail e -> Fail e | Return i1 -> if capacity <= i1 then begin match usize_mul capacity 2 with - | Fail -> Fail + | Fail e -> Fail e | Return i2 -> begin match hashmap_hash_map_new_with_capacity_fwd t i2 i i0 with - | Fail -> Fail + | Fail e -> Fail e | Return ntable -> begin match hashmap_hash_map_move_elements_fwd_back t ntable self.hashmap_hash_map_slots 0 with - | Fail -> Fail + | Fail e -> Fail e | Return (ntable0, _) -> Return (Mkhashmap_hash_map_t self.hashmap_hash_map_num_entries (i, i0) ntable0.hashmap_hash_map_max_load @@ -304,15 +304,15 @@ let hashmap_hash_map_insert_fwd_back result (hashmap_hash_map_t t) = begin match hashmap_hash_map_insert_no_resize_fwd_back t self key value with - | Fail -> Fail + | Fail e -> Fail e | Return self0 -> begin match hashmap_hash_map_len_fwd t self0 with - | Fail -> Fail + | Fail e -> Fail e | Return i -> if i > self0.hashmap_hash_map_max_load then begin match hashmap_hash_map_try_resize_fwd_back t self0 with - | Fail -> Fail + | Fail e -> Fail e | Return self1 -> Return self1 end else Return self0 @@ -331,7 +331,7 @@ let rec hashmap_hash_map_contains_key_in_list_fwd then Return true else begin match hashmap_hash_map_contains_key_in_list_fwd t key ls0 with - | Fail -> Fail + | Fail e -> Fail e | Return b -> Return b end | HashmapListNil -> Return false @@ -341,19 +341,19 @@ let rec hashmap_hash_map_contains_key_in_list_fwd let hashmap_hash_map_contains_key_fwd (t : Type0) (self : hashmap_hash_map_t t) (key : usize) : result bool = begin match hashmap_hash_key_fwd key with - | Fail -> Fail + | Fail e -> Fail e | Return hash -> let i = vec_len (hashmap_list_t t) self.hashmap_hash_map_slots in begin match usize_rem hash i with - | Fail -> Fail + | Fail e -> Fail e | Return hash_mod -> begin match vec_index_fwd (hashmap_list_t t) self.hashmap_hash_map_slots hash_mod with - | Fail -> Fail + | Fail e -> Fail e | Return l -> begin match hashmap_hash_map_contains_key_in_list_fwd t key l with - | Fail -> Fail + | Fail e -> Fail e | Return b -> Return b end end @@ -371,29 +371,29 @@ let rec hashmap_hash_map_get_in_list_fwd then Return cvalue else begin match hashmap_hash_map_get_in_list_fwd t key ls0 with - | Fail -> Fail + | Fail e -> Fail e | Return x -> Return x end - | HashmapListNil -> Fail + | HashmapListNil -> Fail Failure end (** [hashmap_main::hashmap::HashMap::{0}::get] *) let hashmap_hash_map_get_fwd (t : Type0) (self : hashmap_hash_map_t t) (key : usize) : result t = begin match hashmap_hash_key_fwd key with - | Fail -> Fail + | Fail e -> Fail e | Return hash -> let i = vec_len (hashmap_list_t t) self.hashmap_hash_map_slots in begin match usize_rem hash i with - | Fail -> Fail + | Fail e -> Fail e | Return hash_mod -> begin match vec_index_fwd (hashmap_list_t t) self.hashmap_hash_map_slots hash_mod with - | Fail -> Fail + | Fail e -> Fail e | Return l -> begin match hashmap_hash_map_get_in_list_fwd t key l with - | Fail -> Fail + | Fail e -> Fail e | Return x -> Return x end end @@ -412,10 +412,10 @@ let rec hashmap_hash_map_get_mut_in_list_fwd then Return cvalue else begin match hashmap_hash_map_get_mut_in_list_fwd t key ls0 with - | Fail -> Fail + | Fail e -> Fail e | Return x -> Return x end - | HashmapListNil -> Fail + | HashmapListNil -> Fail Failure end (** [hashmap_main::hashmap::HashMap::{0}::get_mut_in_list] *) @@ -430,29 +430,29 @@ let rec hashmap_hash_map_get_mut_in_list_back then Return (HashmapListCons ckey ret ls0) else begin match hashmap_hash_map_get_mut_in_list_back t key ls0 ret with - | Fail -> Fail + | Fail e -> Fail e | Return ls1 -> Return (HashmapListCons ckey cvalue ls1) end - | HashmapListNil -> Fail + | HashmapListNil -> Fail Failure end (** [hashmap_main::hashmap::HashMap::{0}::get_mut] *) let hashmap_hash_map_get_mut_fwd (t : Type0) (self : hashmap_hash_map_t t) (key : usize) : result t = begin match hashmap_hash_key_fwd key with - | Fail -> Fail + | Fail e -> Fail e | Return hash -> let i = vec_len (hashmap_list_t t) self.hashmap_hash_map_slots in begin match usize_rem hash i with - | Fail -> Fail + | Fail e -> Fail e | Return hash_mod -> begin match vec_index_mut_fwd (hashmap_list_t t) self.hashmap_hash_map_slots hash_mod with - | Fail -> Fail + | Fail e -> Fail e | Return l -> begin match hashmap_hash_map_get_mut_in_list_fwd t key l with - | Fail -> Fail + | Fail e -> Fail e | Return x -> Return x end end @@ -465,24 +465,24 @@ let hashmap_hash_map_get_mut_back result (hashmap_hash_map_t t) = begin match hashmap_hash_key_fwd key with - | Fail -> Fail + | Fail e -> Fail e | Return hash -> let i = vec_len (hashmap_list_t t) self.hashmap_hash_map_slots in begin match usize_rem hash i with - | Fail -> Fail + | Fail e -> Fail e | Return hash_mod -> begin match vec_index_mut_fwd (hashmap_list_t t) self.hashmap_hash_map_slots hash_mod with - | Fail -> Fail + | Fail e -> Fail e | Return l -> begin match hashmap_hash_map_get_mut_in_list_back t key l ret with - | Fail -> Fail + | Fail e -> Fail e | Return l0 -> begin match vec_index_mut_back (hashmap_list_t t) self.hashmap_hash_map_slots hash_mod l0 with - | Fail -> Fail + | Fail e -> Fail e | Return v -> Return (Mkhashmap_hash_map_t self.hashmap_hash_map_num_entries self.hashmap_hash_map_max_load_factor @@ -508,11 +508,11 @@ let rec hashmap_hash_map_remove_from_list_fwd HashmapListNil in begin match mv_ls with | HashmapListCons i cvalue tl0 -> Return (Some cvalue) - | HashmapListNil -> Fail + | HashmapListNil -> Fail Failure end else begin match hashmap_hash_map_remove_from_list_fwd t key tl with - | Fail -> Fail + | Fail e -> Fail e | Return opt -> Return opt end | HashmapListNil -> Return None @@ -533,11 +533,11 @@ let rec hashmap_hash_map_remove_from_list_back HashmapListNil in begin match mv_ls with | HashmapListCons i cvalue tl0 -> Return tl0 - | HashmapListNil -> Fail + | HashmapListNil -> Fail Failure end else begin match hashmap_hash_map_remove_from_list_back t key tl with - | Fail -> Fail + | Fail e -> Fail e | Return tl0 -> Return (HashmapListCons ckey x tl0) end | HashmapListNil -> Return HashmapListNil @@ -547,25 +547,25 @@ let rec hashmap_hash_map_remove_from_list_back let hashmap_hash_map_remove_fwd (t : Type0) (self : hashmap_hash_map_t t) (key : usize) : result (option t) = begin match hashmap_hash_key_fwd key with - | Fail -> Fail + | Fail e -> Fail e | Return hash -> let i = vec_len (hashmap_list_t t) self.hashmap_hash_map_slots in begin match usize_rem hash i with - | Fail -> Fail + | Fail e -> Fail e | Return hash_mod -> begin match vec_index_mut_fwd (hashmap_list_t t) self.hashmap_hash_map_slots hash_mod with - | Fail -> Fail + | Fail e -> Fail e | Return l -> begin match hashmap_hash_map_remove_from_list_fwd t key l with - | Fail -> Fail + | Fail e -> Fail e | Return x -> begin match x with | None -> Return None | Some x0 -> begin match usize_sub self.hashmap_hash_map_num_entries 1 with - | Fail -> Fail + | Fail e -> Fail e | Return _ -> Return (Some x0) end end @@ -580,29 +580,29 @@ let hashmap_hash_map_remove_back result (hashmap_hash_map_t t) = begin match hashmap_hash_key_fwd key with - | Fail -> Fail + | Fail e -> Fail e | Return hash -> let i = vec_len (hashmap_list_t t) self.hashmap_hash_map_slots in begin match usize_rem hash i with - | Fail -> Fail + | Fail e -> Fail e | Return hash_mod -> begin match vec_index_mut_fwd (hashmap_list_t t) self.hashmap_hash_map_slots hash_mod with - | Fail -> Fail + | Fail e -> Fail e | Return l -> begin match hashmap_hash_map_remove_from_list_fwd t key l with - | Fail -> Fail + | Fail e -> Fail e | Return x -> begin match x with | None -> begin match hashmap_hash_map_remove_from_list_back t key l with - | Fail -> Fail + | Fail e -> Fail e | Return l0 -> begin match vec_index_mut_back (hashmap_list_t t) self.hashmap_hash_map_slots hash_mod l0 with - | Fail -> Fail + | Fail e -> Fail e | Return v -> Return (Mkhashmap_hash_map_t self.hashmap_hash_map_num_entries self.hashmap_hash_map_max_load_factor @@ -611,15 +611,15 @@ let hashmap_hash_map_remove_back end | Some x0 -> begin match usize_sub self.hashmap_hash_map_num_entries 1 with - | Fail -> Fail + | Fail e -> Fail e | Return i0 -> begin match hashmap_hash_map_remove_from_list_back t key l with - | Fail -> Fail + | Fail e -> Fail e | Return l0 -> begin match vec_index_mut_back (hashmap_list_t t) self.hashmap_hash_map_slots hash_mod l0 with - | Fail -> Fail + | Fail e -> Fail e | Return v -> Return (Mkhashmap_hash_map_t i0 self.hashmap_hash_map_max_load_factor @@ -636,69 +636,69 @@ let hashmap_hash_map_remove_back (** [hashmap_main::hashmap::test1] *) let hashmap_test1_fwd : result unit = begin match hashmap_hash_map_new_fwd u64 with - | Fail -> Fail + | Fail e -> Fail e | Return hm -> begin match hashmap_hash_map_insert_fwd_back u64 hm 0 42 with - | Fail -> Fail + | Fail e -> Fail e | Return hm0 -> begin match hashmap_hash_map_insert_fwd_back u64 hm0 128 18 with - | Fail -> Fail + | Fail e -> Fail e | Return hm1 -> begin match hashmap_hash_map_insert_fwd_back u64 hm1 1024 138 with - | Fail -> Fail + | Fail e -> Fail e | Return hm2 -> begin match hashmap_hash_map_insert_fwd_back u64 hm2 1056 256 with - | Fail -> Fail + | Fail e -> Fail e | Return hm3 -> begin match hashmap_hash_map_get_fwd u64 hm3 128 with - | Fail -> Fail + | Fail e -> Fail e | Return i -> if not (i = 18) - then Fail + then Fail Failure else begin match hashmap_hash_map_get_mut_back u64 hm3 1024 56 with - | Fail -> Fail + | Fail e -> Fail e | Return hm4 -> begin match hashmap_hash_map_get_fwd u64 hm4 1024 with - | Fail -> Fail + | Fail e -> Fail e | Return i0 -> if not (i0 = 56) - then Fail + then Fail Failure else begin match hashmap_hash_map_remove_fwd u64 hm4 1024 with - | Fail -> Fail + | Fail e -> Fail e | Return x -> begin match x with - | None -> Fail + | None -> Fail Failure | Some x0 -> if not (x0 = 56) - then Fail + then Fail Failure else begin match hashmap_hash_map_remove_back u64 hm4 1024 with - | Fail -> Fail + | Fail e -> Fail e | Return hm5 -> begin match hashmap_hash_map_get_fwd u64 hm5 0 with - | Fail -> Fail + | Fail e -> Fail e | Return i1 -> if not (i1 = 42) - then Fail + then Fail Failure else begin match hashmap_hash_map_get_fwd u64 hm5 128 with - | Fail -> Fail + | Fail e -> Fail e | Return i2 -> if not (i2 = 18) - then Fail + then Fail Failure else begin match hashmap_hash_map_get_fwd u64 hm5 1056 with - | Fail -> Fail + | Fail e -> Fail e | Return i3 -> if not (i3 = 256) - then Fail + then Fail Failure else Return () end end @@ -722,13 +722,13 @@ let _ = assert_norm (hashmap_test1_fwd = Return ()) let insert_on_disk_fwd (key : usize) (value : u64) (st : state) : result (state & unit) = begin match hashmap_utils_deserialize_fwd st with - | Fail -> Fail + | Fail e -> Fail e | Return (st0, hm) -> begin match hashmap_hash_map_insert_fwd_back u64 hm key value with - | Fail -> Fail + | Fail e -> Fail e | Return hm0 -> begin match hashmap_utils_serialize_fwd hm0 st0 with - | Fail -> Fail + | Fail e -> Fail e | Return (st1, _) -> Return (st1, ()) end end diff --git a/tests/fstar/hashmap_on_disk/HashmapMain.Properties.fst b/tests/fstar/hashmap_on_disk/HashmapMain.Properties.fst index 4df039a8..106fe05a 100644 --- a/tests/fstar/hashmap_on_disk/HashmapMain.Properties.fst +++ b/tests/fstar/hashmap_on_disk/HashmapMain.Properties.fst @@ -19,7 +19,7 @@ val state_v : state -> hashmap_hash_map_t u64 assume val serialize_lem (hm : hashmap_hash_map_t u64) (st : state) : Lemma ( match hashmap_utils_serialize_fwd hm st with - | Fail -> True + | Fail _ -> True | Return (st', ()) -> state_v st' == hm) [SMTPat (hashmap_utils_serialize_fwd hm st)] @@ -27,7 +27,7 @@ val serialize_lem (hm : hashmap_hash_map_t u64) (st : state) : Lemma ( assume val deserialize_lem (st : state) : Lemma ( match hashmap_utils_deserialize_fwd st with - | Fail -> True + | Fail _ -> True | Return (st', hm) -> hm == state_v st /\ st' == st) [SMTPat (hashmap_utils_deserialize_fwd st)] @@ -38,11 +38,11 @@ val deserialize_lem (st : state) : Lemma ( /// in the hash map previously stored on disk. val insert_on_disk_fwd_lem (key : usize) (value : u64) (st : state) : Lemma ( match insert_on_disk_fwd key value st with - | Fail -> True + | Fail _ -> True | Return (st', ()) -> let hm = state_v st in match hashmap_hash_map_insert_fwd_back u64 hm key value with - | Fail -> False + | Fail _ -> False | Return hm' -> hm' == state_v st') let insert_on_disk_fwd_lem key value st = () diff --git a/tests/fstar/hashmap_on_disk/Primitives.fst b/tests/fstar/hashmap_on_disk/Primitives.fst index 96138e46..82622656 100644 --- a/tests/fstar/hashmap_on_disk/Primitives.fst +++ b/tests/fstar/hashmap_on_disk/Primitives.fst @@ -18,9 +18,13 @@ let rec list_update #a ls i x = #pop-options (*** Result *) +type error : Type0 = +| Failure +| OutOfFuel + type result (a : Type0) : Type0 = | Return : v:a -> result a -| Fail : result a +| Fail : e:error -> result a // Monadic bind and return. // Re-definining those allows us to customize the result of the monadic notations @@ -29,10 +33,10 @@ let return (#a : Type0) (x:a) : result a = Return x let bind (#a #b : Type0) (m : result a) (f : a -> result b) : result b = match m with | Return x -> f x - | Fail -> Fail + | Fail e -> Fail e // Monadic assert(...) -let massert (b:bool) : result unit = if b then Return () else Fail +let massert (b:bool) : result unit = if b then Return () else Fail Failure // Normalize and unwrap a successful result (used for globals). let eval_global (#a : Type0) (x : result a{Return? (normalize_term x)}) : a = Return?.v x @@ -119,12 +123,12 @@ let scalar_max (ty : scalar_ty) : int = type scalar (ty : scalar_ty) : eqtype = x:int{scalar_min ty <= x && x <= scalar_max ty} let mk_scalar (ty : scalar_ty) (x : int) : result (scalar ty) = - if scalar_min ty <= x && scalar_max ty >= x then Return x else Fail + if scalar_min ty <= x && scalar_max ty >= x then Return x else Fail Failure let scalar_neg (#ty : scalar_ty) (x : scalar ty) : result (scalar ty) = mk_scalar ty (-x) let scalar_div (#ty : scalar_ty) (x : scalar ty) (y : scalar ty) : result (scalar ty) = - if y <> 0 then mk_scalar ty (x / y) else Fail + if y <> 0 then mk_scalar ty (x / y) else Fail Failure /// The remainder operation let int_rem (x : int) (y : int{y <> 0}) : int = @@ -137,7 +141,7 @@ let _ = assert_norm(int_rem 1 (-2) = 1) let _ = assert_norm(int_rem (-1) (-2) = -1) let scalar_rem (#ty : scalar_ty) (x : scalar ty) (y : scalar ty) : result (scalar ty) = - if y <> 0 then mk_scalar ty (int_rem x y) else Fail + if y <> 0 then mk_scalar ty (int_rem x y) else Fail Failure let scalar_add (#ty : scalar_ty) (x : scalar ty) (y : scalar ty) : result (scalar ty) = mk_scalar ty (x + y) @@ -258,7 +262,7 @@ let vec_push_back (a : Type0) (v : vec a) (x : a) : (requires True) (ensures (fun res -> match res with - | Fail -> True + | Fail e -> e == Failure | Return v' -> length v' = length v + 1)) = if length v < usize_max then begin (**) assert_norm(length [x] == 1); @@ -266,22 +270,22 @@ let vec_push_back (a : Type0) (v : vec a) (x : a) : (**) assert(length (append v [x]) = length v + 1); Return (append v [x]) end - else Fail + else Fail Failure // The **forward** function shouldn't be used let vec_insert_fwd (a : Type0) (v : vec a) (i : usize) (x : a) : result unit = - if i < length v then Return () else Fail + if i < length v then Return () else Fail Failure let vec_insert_back (a : Type0) (v : vec a) (i : usize) (x : a) : result (vec a) = - if i < length v then Return (list_update v i x) else Fail + if i < length v then Return (list_update v i x) else Fail Failure // The **backward** function shouldn't be used let vec_index_fwd (a : Type0) (v : vec a) (i : usize) : result a = - if i < length v then Return (index v i) else Fail + if i < length v then Return (index v i) else Fail Failure let vec_index_back (a : Type0) (v : vec a) (i : usize) (x : a) : result unit = - if i < length v then Return () else Fail + if i < length v then Return () else Fail Failure let vec_index_mut_fwd (a : Type0) (v : vec a) (i : usize) : result a = - if i < length v then Return (index v i) else Fail + if i < length v then Return (index v i) else Fail Failure let vec_index_mut_back (a : Type0) (v : vec a) (i : usize) (nx : a) : result (vec a) = - if i < length v then Return (list_update v i nx) else Fail + if i < length v then Return (list_update v i nx) else Fail Failure diff --git a/tests/fstar/misc/Constants.fst b/tests/fstar/misc/Constants.fst index 884d1778..a0658206 100644 --- a/tests/fstar/misc/Constants.fst +++ b/tests/fstar/misc/Constants.fst @@ -23,11 +23,11 @@ let x2_c : u32 = eval_global x2_body (** [constants::incr] *) let incr_fwd (n : u32) : result u32 = - begin match u32_add n 1 with | Fail -> Fail | Return i -> Return i end + begin match u32_add n 1 with | Fail e -> Fail e | Return i -> Return i end (** [constants::X3] *) let x3_body : result u32 = - begin match incr_fwd 32 with | Fail -> Fail | Return i -> Return i end + begin match incr_fwd 32 with | Fail e -> Fail e | Return i -> Return i end let x3_c : u32 = eval_global x3_body (** [constants::mk_pair0] *) @@ -42,12 +42,18 @@ let mk_pair1_fwd (x : u32) (y : u32) : result (pair_t u32 u32) = (** [constants::P0] *) let p0_body : result (u32 & u32) = - begin match mk_pair0_fwd 0 1 with | Fail -> Fail | Return p -> Return p end + begin match mk_pair0_fwd 0 1 with + | Fail e -> Fail e + | Return p -> Return p + end let p0_c : (u32 & u32) = eval_global p0_body (** [constants::P1] *) let p1_body : result (pair_t u32 u32) = - begin match mk_pair1_fwd 0 1 with | Fail -> Fail | Return p -> Return p end + begin match mk_pair1_fwd 0 1 with + | Fail e -> Fail e + | Return p -> Return p + end let p1_c : pair_t u32 u32 = eval_global p1_body (** [constants::P2] *) @@ -67,7 +73,10 @@ let wrap_new_fwd (t : Type0) (val0 : t) : result (wrap_t t) = (** [constants::Y] *) let y_body : result (wrap_t i32) = - begin match wrap_new_fwd i32 2 with | Fail -> Fail | Return w -> Return w end + begin match wrap_new_fwd i32 2 with + | Fail e -> Fail e + | Return w -> Return w + end let y_c : wrap_t i32 = eval_global y_body (** [constants::unwrap_y] *) @@ -75,7 +84,7 @@ let unwrap_y_fwd : result i32 = Return y_c.wrap_val (** [constants::YVAL] *) let yval_body : result i32 = - begin match unwrap_y_fwd with | Fail -> Fail | Return i -> Return i end + begin match unwrap_y_fwd with | Fail e -> Fail e | Return i -> Return i end let yval_c : i32 = eval_global yval_body (** [constants::get_z1::Z1] *) @@ -87,7 +96,7 @@ let get_z1_fwd : result i32 = Return get_z1_z1_c (** [constants::add] *) let add_fwd (a : i32) (b : i32) : result i32 = - begin match i32_add a b with | Fail -> Fail | Return i -> Return i end + begin match i32_add a b with | Fail e -> Fail e | Return i -> Return i end (** [constants::Q1] *) let q1_body : result i32 = Return 5 @@ -99,19 +108,19 @@ let q2_c : i32 = eval_global q2_body (** [constants::Q3] *) let q3_body : result i32 = - begin match add_fwd q2_c 3 with | Fail -> Fail | Return i -> Return i end + begin match add_fwd q2_c 3 with | Fail e -> Fail e | Return i -> Return i end let q3_c : i32 = eval_global q3_body (** [constants::get_z2] *) let get_z2_fwd : result i32 = begin match get_z1_fwd with - | Fail -> Fail + | Fail e -> Fail e | Return i -> begin match add_fwd i q3_c with - | Fail -> Fail + | Fail e -> Fail e | Return i0 -> begin match add_fwd q1_c i0 with - | Fail -> Fail + | Fail e -> Fail e | Return i1 -> Return i1 end end @@ -123,7 +132,7 @@ let s1_c : u32 = eval_global s1_body (** [constants::S2] *) let s2_body : result u32 = - begin match incr_fwd s1_c with | Fail -> Fail | Return i -> Return i end + begin match incr_fwd s1_c with | Fail e -> Fail e | Return i -> Return i end let s2_c : u32 = eval_global s2_body (** [constants::S3] *) @@ -132,6 +141,9 @@ let s3_c : pair_t u32 u32 = eval_global s3_body (** [constants::S4] *) let s4_body : result (pair_t u32 u32) = - begin match mk_pair1_fwd 7 8 with | Fail -> Fail | Return p -> Return p end + begin match mk_pair1_fwd 7 8 with + | Fail e -> Fail e + | Return p -> Return p + end let s4_c : pair_t u32 u32 = eval_global s4_body diff --git a/tests/fstar/misc/External.Funs.fst b/tests/fstar/misc/External.Funs.fst index 68a0061e..a57472d4 100644 --- a/tests/fstar/misc/External.Funs.fst +++ b/tests/fstar/misc/External.Funs.fst @@ -10,13 +10,13 @@ include External.Opaque (** [external::swap] *) let swap_fwd (t : Type0) (x : t) (y : t) (st : state) : result (state & unit) = begin match core_mem_swap_fwd t x y st with - | Fail -> Fail + | Fail e -> Fail e | Return (st0, _) -> begin match core_mem_swap_back0 t x y st st0 with - | Fail -> Fail + | Fail e -> Fail e | Return (st1, _) -> begin match core_mem_swap_back1 t x y st st1 with - | Fail -> Fail + | Fail e -> Fail e | Return (st2, _) -> Return (st2, ()) end end @@ -28,13 +28,13 @@ let swap_back result (state & (t & t)) = begin match core_mem_swap_fwd t x y st with - | Fail -> Fail + | Fail e -> Fail e | Return (st1, _) -> begin match core_mem_swap_back0 t x y st st1 with - | Fail -> Fail + | Fail e -> Fail e | Return (st2, x0) -> begin match core_mem_swap_back1 t x y st st2 with - | Fail -> Fail + | Fail e -> Fail e | Return (_, y0) -> Return (st0, (x0, y0)) end end @@ -44,12 +44,12 @@ let swap_back let test_new_non_zero_u32_fwd (x : u32) (st : state) : result (state & core_num_nonzero_non_zero_u32_t) = begin match core_num_nonzero_non_zero_u32_new_fwd x st with - | Fail -> Fail + | Fail e -> Fail e | Return (st0, opt) -> begin match core_option_option_unwrap_fwd core_num_nonzero_non_zero_u32_t opt st0 with - | Fail -> Fail + | Fail e -> Fail e | Return (st1, nzu) -> Return (st1, nzu) end end @@ -58,7 +58,7 @@ let test_new_non_zero_u32_fwd let test_vec_fwd : result unit = let v = vec_new u32 in begin match vec_push_back u32 v 0 with - | Fail -> Fail + | Fail e -> Fail e | Return _ -> Return () end @@ -69,13 +69,13 @@ let _ = assert_norm (test_vec_fwd = Return ()) let custom_swap_fwd (t : Type0) (x : t) (y : t) (st : state) : result (state & t) = begin match core_mem_swap_fwd t x y st with - | Fail -> Fail + | Fail e -> Fail e | Return (st0, _) -> begin match core_mem_swap_back0 t x y st st0 with - | Fail -> Fail + | Fail e -> Fail e | Return (st1, x0) -> begin match core_mem_swap_back1 t x y st st1 with - | Fail -> Fail + | Fail e -> Fail e | Return (st2, _) -> Return (st2, x0) end end @@ -87,13 +87,13 @@ let custom_swap_back result (state & (t & t)) = begin match core_mem_swap_fwd t x y st with - | Fail -> Fail + | Fail e -> Fail e | Return (st1, _) -> begin match core_mem_swap_back0 t x y st st1 with - | Fail -> Fail + | Fail e -> Fail e | Return (st2, _) -> begin match core_mem_swap_back1 t x y st st2 with - | Fail -> Fail + | Fail e -> Fail e | Return (_, y0) -> Return (st0, (ret, y0)) end end @@ -103,7 +103,7 @@ let custom_swap_back let test_custom_swap_fwd (x : u32) (y : u32) (st : state) : result (state & unit) = begin match custom_swap_fwd u32 x y st with - | Fail -> Fail + | Fail e -> Fail e | Return (st0, _) -> Return (st0, ()) end @@ -113,18 +113,19 @@ let test_custom_swap_back result (state & (u32 & u32)) = begin match custom_swap_back u32 x y st 1 st0 with - | Fail -> Fail + | Fail e -> Fail e | Return (st1, (x0, y0)) -> Return (st1, (x0, y0)) end (** [external::test_swap_non_zero] *) let test_swap_non_zero_fwd (x : u32) (st : state) : result (state & u32) = begin match swap_fwd u32 x 0 st with - | Fail -> Fail + | Fail e -> Fail e | Return (st0, _) -> begin match swap_back u32 x 0 st st0 with - | Fail -> Fail - | Return (st1, (x0, _)) -> if x0 = 0 then Fail else Return (st1, x0) + | Fail e -> Fail e + | Return (st1, (x0, _)) -> + if x0 = 0 then Fail Failure else Return (st1, x0) end end diff --git a/tests/fstar/misc/NoNestedBorrows.fst b/tests/fstar/misc/NoNestedBorrows.fst index 36dea95b..8424a7cc 100644 --- a/tests/fstar/misc/NoNestedBorrows.fst +++ b/tests/fstar/misc/NoNestedBorrows.fst @@ -32,38 +32,38 @@ type sum_t (t1 t2 : Type0) = (** [no_nested_borrows::neg_test] *) let neg_test_fwd (x : i32) : result i32 = - begin match i32_neg x with | Fail -> Fail | Return i -> Return i end + begin match i32_neg x with | Fail e -> Fail e | Return i -> Return i end (** [no_nested_borrows::add_test] *) let add_test_fwd (x : u32) (y : u32) : result u32 = - begin match u32_add x y with | Fail -> Fail | Return i -> Return i end + begin match u32_add x y with | Fail e -> Fail e | Return i -> Return i end (** [no_nested_borrows::subs_test] *) let subs_test_fwd (x : u32) (y : u32) : result u32 = - begin match u32_sub x y with | Fail -> Fail | Return i -> Return i end + begin match u32_sub x y with | Fail e -> Fail e | Return i -> Return i end (** [no_nested_borrows::div_test] *) let div_test_fwd (x : u32) (y : u32) : result u32 = - begin match u32_div x y with | Fail -> Fail | Return i -> Return i end + begin match u32_div x y with | Fail e -> Fail e | Return i -> Return i end (** [no_nested_borrows::div_test1] *) let div_test1_fwd (x : u32) : result u32 = - begin match u32_div x 2 with | Fail -> Fail | Return i -> Return i end + begin match u32_div x 2 with | Fail e -> Fail e | Return i -> Return i end (** [no_nested_borrows::rem_test] *) let rem_test_fwd (x : u32) (y : u32) : result u32 = - begin match u32_rem x y with | Fail -> Fail | Return i -> Return i end + begin match u32_rem x y with | Fail e -> Fail e | Return i -> Return i end (** [no_nested_borrows::cast_test] *) let cast_test_fwd (x : u32) : result i32 = begin match scalar_cast U32 I32 x with - | Fail -> Fail + | Fail e -> Fail e | Return i -> Return i end (** [no_nested_borrows::test2] *) let test2_fwd : result unit = - begin match u32_add 23 44 with | Fail -> Fail | Return _ -> Return () end + begin match u32_add 23 44 with | Fail e -> Fail e | Return _ -> Return () end (** Unit test for [no_nested_borrows::test2] *) let _ = assert_norm (test2_fwd = Return ()) @@ -75,14 +75,14 @@ let get_max_fwd (x : u32) (y : u32) : result u32 = (** [no_nested_borrows::test3] *) let test3_fwd : result unit = begin match get_max_fwd 4 3 with - | Fail -> Fail + | Fail e -> Fail e | Return x -> begin match get_max_fwd 10 11 with - | Fail -> Fail + | Fail e -> Fail e | Return y -> begin match u32_add x y with - | Fail -> Fail - | Return z -> if not (z = 15) then Fail else Return () + | Fail e -> Fail e + | Return z -> if not (z = 15) then Fail Failure else Return () end end end @@ -93,15 +93,16 @@ let _ = assert_norm (test3_fwd = Return ()) (** [no_nested_borrows::test_neg1] *) let test_neg1_fwd : result unit = begin match i32_neg 3 with - | Fail -> Fail - | Return y -> if not (y = -3) then Fail else Return () + | Fail e -> Fail e + | Return y -> if not (y = -3) then Fail Failure else Return () end (** Unit test for [no_nested_borrows::test_neg1] *) let _ = assert_norm (test_neg1_fwd = Return ()) (** [no_nested_borrows::refs_test1] *) -let refs_test1_fwd : result unit = if not (1 = 1) then Fail else Return () +let refs_test1_fwd : result unit = + if not (1 = 1) then Fail Failure else Return () (** Unit test for [no_nested_borrows::refs_test1] *) let _ = assert_norm (refs_test1_fwd = Return ()) @@ -109,11 +110,14 @@ let _ = assert_norm (refs_test1_fwd = Return ()) (** [no_nested_borrows::refs_test2] *) let refs_test2_fwd : result unit = if not (2 = 2) - then Fail + then Fail Failure else if not (0 = 0) - then Fail - else if not (2 = 2) then Fail else if not (2 = 2) then Fail else Return () + then Fail Failure + else + if not (2 = 2) + then Fail Failure + else if not (2 = 2) then Fail Failure else Return () (** Unit test for [no_nested_borrows::refs_test2] *) let _ = assert_norm (refs_test2_fwd = Return ()) @@ -126,7 +130,7 @@ let _ = assert_norm (test_list1_fwd = Return ()) (** [no_nested_borrows::test_box1] *) let test_box1_fwd : result unit = - let b = 1 in let x = b in if not (x = 1) then Fail else Return () + let b = 1 in let x = b in if not (x = 1) then Fail Failure else Return () (** Unit test for [no_nested_borrows::test_box1] *) let _ = assert_norm (test_box1_fwd = Return ()) @@ -136,16 +140,17 @@ let copy_int_fwd (x : i32) : result i32 = Return x (** [no_nested_borrows::test_unreachable] *) let test_unreachable_fwd (b : bool) : result unit = - if b then Fail else Return () + if b then Fail Failure else Return () (** [no_nested_borrows::test_panic] *) -let test_panic_fwd (b : bool) : result unit = if b then Fail else Return () +let test_panic_fwd (b : bool) : result unit = + if b then Fail Failure else Return () (** [no_nested_borrows::test_copy_int] *) let test_copy_int_fwd : result unit = begin match copy_int_fwd 0 with - | Fail -> Fail - | Return y -> if not (0 = y) then Fail else Return () + | Fail e -> Fail e + | Return y -> if not (0 = y) then Fail Failure else Return () end (** Unit test for [no_nested_borrows::test_copy_int] *) @@ -162,8 +167,8 @@ let is_cons_fwd (t : Type0) (l : list_t t) : result bool = let test_is_cons_fwd : result unit = let l = ListNil in begin match is_cons_fwd i32 (ListCons 0 l) with - | Fail -> Fail - | Return b -> if not b then Fail else Return () + | Fail e -> Fail e + | Return b -> if not b then Fail Failure else Return () end (** Unit test for [no_nested_borrows::test_is_cons] *) @@ -171,14 +176,18 @@ let _ = assert_norm (test_is_cons_fwd = Return ()) (** [no_nested_borrows::split_list] *) let split_list_fwd (t : Type0) (l : list_t t) : result (t & (list_t t)) = - begin match l with | ListCons hd tl -> Return (hd, tl) | ListNil -> Fail end + begin match l with + | ListCons hd tl -> Return (hd, tl) + | ListNil -> Fail Failure + end (** [no_nested_borrows::test_split_list] *) let test_split_list_fwd : result unit = let l = ListNil in begin match split_list_fwd i32 (ListCons 0 l) with - | Fail -> Fail - | Return p -> let (hd, _) = p in if not (hd = 0) then Fail else Return () + | Fail e -> Fail e + | Return p -> + let (hd, _) = p in if not (hd = 0) then Fail Failure else Return () end (** Unit test for [no_nested_borrows::test_split_list] *) @@ -196,18 +205,20 @@ let choose_back (** [no_nested_borrows::choose_test] *) let choose_test_fwd : result unit = begin match choose_fwd i32 true 0 0 with - | Fail -> Fail + | Fail e -> Fail e | Return z -> begin match i32_add z 1 with - | Fail -> Fail + | Fail e -> Fail e | Return z0 -> if not (z0 = 1) - then Fail + then Fail Failure else begin match choose_back i32 true 0 0 z0 with - | Fail -> Fail + | Fail e -> Fail e | Return (x, y) -> - if not (x = 1) then Fail else if not (y = 0) then Fail else Return () + if not (x = 1) + then Fail Failure + else if not (y = 0) then Fail Failure else Return () end end end @@ -233,9 +244,12 @@ let rec list_length_fwd (t : Type0) (l : list_t t) : result u32 = begin match l with | ListCons x l1 -> begin match list_length_fwd t l1 with - | Fail -> Fail + | Fail e -> Fail e | Return i -> - begin match u32_add 1 i with | Fail -> Fail | Return i0 -> Return i0 end + begin match u32_add 1 i with + | Fail e -> Fail e + | Return i0 -> Return i0 + end end | ListNil -> Return 0 end @@ -248,14 +262,14 @@ let rec list_nth_shared_fwd (t : Type0) (l : list_t t) (i : u32) : result t = then Return x else begin match u32_sub i 1 with - | Fail -> Fail + | Fail e -> Fail e | Return i0 -> begin match list_nth_shared_fwd t tl i0 with - | Fail -> Fail + | Fail e -> Fail e | Return x0 -> Return x0 end end - | ListNil -> Fail + | ListNil -> Fail Failure end (** [no_nested_borrows::list_nth_mut] *) @@ -266,14 +280,14 @@ let rec list_nth_mut_fwd (t : Type0) (l : list_t t) (i : u32) : result t = then Return x else begin match u32_sub i 1 with - | Fail -> Fail + | Fail e -> Fail e | Return i0 -> begin match list_nth_mut_fwd t tl i0 with - | Fail -> Fail + | Fail e -> Fail e | Return x0 -> Return x0 end end - | ListNil -> Fail + | ListNil -> Fail Failure end (** [no_nested_borrows::list_nth_mut] *) @@ -285,14 +299,14 @@ let rec list_nth_mut_back then Return (ListCons ret tl) else begin match u32_sub i 1 with - | Fail -> Fail + | Fail e -> Fail e | Return i0 -> begin match list_nth_mut_back t tl i0 ret with - | Fail -> Fail + | Fail e -> Fail e | Return tl0 -> Return (ListCons x tl0) end end - | ListNil -> Fail + | ListNil -> Fail Failure end (** [no_nested_borrows::list_rev_aux] *) @@ -301,7 +315,7 @@ let rec list_rev_aux_fwd begin match li with | ListCons hd tl -> begin match list_rev_aux_fwd t tl (ListCons hd lo) with - | Fail -> Fail + | Fail e -> Fail e | Return l -> Return l end | ListNil -> Return lo @@ -311,7 +325,7 @@ let rec list_rev_aux_fwd let list_rev_fwd_back (t : Type0) (l : list_t t) : result (list_t t) = let li = mem_replace_fwd (list_t t) l ListNil in begin match list_rev_aux_fwd t li ListNil with - | Fail -> Fail + | Fail e -> Fail e | Return l0 -> Return l0 end @@ -321,48 +335,48 @@ let test_list_functions_fwd : result unit = let l0 = ListCons 2 l in let l1 = ListCons 1 l0 in begin match list_length_fwd i32 (ListCons 0 l1) with - | Fail -> Fail + | Fail e -> Fail e | Return i -> if not (i = 3) - then Fail + then Fail Failure else begin match list_nth_shared_fwd i32 (ListCons 0 l1) 0 with - | Fail -> Fail + | Fail e -> Fail e | Return i0 -> if not (i0 = 0) - then Fail + then Fail Failure else begin match list_nth_shared_fwd i32 (ListCons 0 l1) 1 with - | Fail -> Fail + | Fail e -> Fail e | Return i1 -> if not (i1 = 1) - then Fail + then Fail Failure else begin match list_nth_shared_fwd i32 (ListCons 0 l1) 2 with - | Fail -> Fail + | Fail e -> Fail e | Return i2 -> if not (i2 = 2) - then Fail + then Fail Failure else begin match list_nth_mut_back i32 (ListCons 0 l1) 1 3 with - | Fail -> Fail + | Fail e -> Fail e | Return ls -> begin match list_nth_shared_fwd i32 ls 0 with - | Fail -> Fail + | Fail e -> Fail e | Return i3 -> if not (i3 = 0) - then Fail + then Fail Failure else begin match list_nth_shared_fwd i32 ls 1 with - | Fail -> Fail + | Fail e -> Fail e | Return i4 -> if not (i4 = 3) - then Fail + then Fail Failure else begin match list_nth_shared_fwd i32 ls 2 with - | Fail -> Fail + | Fail e -> Fail e | Return i5 -> - if not (i5 = 2) then Fail else Return () + if not (i5 = 2) then Fail Failure else Return () end end end @@ -449,31 +463,31 @@ let new_pair1_fwd : result (struct_with_pair_t u32 u32) = (** [no_nested_borrows::test_constants] *) let test_constants_fwd : result unit = begin match new_tuple1_fwd with - | Fail -> Fail + | Fail e -> Fail e | Return swt -> let (i, _) = swt.struct_with_tuple_p in if not (i = 1) - then Fail + then Fail Failure else begin match new_tuple2_fwd with - | Fail -> Fail + | Fail e -> Fail e | Return swt0 -> let (i0, _) = swt0.struct_with_tuple_p in if not (i0 = 1) - then Fail + then Fail Failure else begin match new_tuple3_fwd with - | Fail -> Fail + | Fail e -> Fail e | Return swt1 -> let (i1, _) = swt1.struct_with_tuple_p in if not (i1 = 1) - then Fail + then Fail Failure else begin match new_pair1_fwd with - | Fail -> Fail + | Fail e -> Fail e | Return swp -> if not (swp.struct_with_pair_p.pair_x = 1) - then Fail + then Fail Failure else Return () end end @@ -491,7 +505,8 @@ let _ = assert_norm (test_weird_borrows1_fwd = Return ()) (** [no_nested_borrows::test_mem_replace] *) let test_mem_replace_fwd_back (px : u32) : result u32 = - let y = mem_replace_fwd u32 px 1 in if not (y = 0) then Fail else Return 2 + let y = mem_replace_fwd u32 px 1 in + if not (y = 0) then Fail Failure else Return 2 (** [no_nested_borrows::test_shared_borrow_bool1] *) let test_shared_borrow_bool1_fwd (b : bool) : result u32 = diff --git a/tests/fstar/misc/Paper.fst b/tests/fstar/misc/Paper.fst index 424889ef..0f8604d1 100644 --- a/tests/fstar/misc/Paper.fst +++ b/tests/fstar/misc/Paper.fst @@ -7,13 +7,13 @@ open Primitives (** [paper::ref_incr] *) let ref_incr_fwd_back (x : i32) : result i32 = - begin match i32_add x 1 with | Fail -> Fail | Return x0 -> Return x0 end + begin match i32_add x 1 with | Fail e -> Fail e | Return x0 -> Return x0 end (** [paper::test_incr] *) let test_incr_fwd : result unit = begin match ref_incr_fwd_back 0 with - | Fail -> Fail - | Return x -> if not (x = 1) then Fail else Return () + | Fail e -> Fail e + | Return x -> if not (x = 1) then Fail Failure else Return () end (** Unit test for [paper::test_incr] *) @@ -31,18 +31,20 @@ let choose_back (** [paper::test_choose] *) let test_choose_fwd : result unit = begin match choose_fwd i32 true 0 0 with - | Fail -> Fail + | Fail e -> Fail e | Return z -> begin match i32_add z 1 with - | Fail -> Fail + | Fail e -> Fail e | Return z0 -> if not (z0 = 1) - then Fail + then Fail Failure else begin match choose_back i32 true 0 0 z0 with - | Fail -> Fail + | Fail e -> Fail e | Return (x, y) -> - if not (x = 1) then Fail else if not (y = 0) then Fail else Return () + if not (x = 1) + then Fail Failure + else if not (y = 0) then Fail Failure else Return () end end end @@ -63,14 +65,14 @@ let rec list_nth_mut_fwd (t : Type0) (l : list_t t) (i : u32) : result t = then Return x else begin match u32_sub i 1 with - | Fail -> Fail + | Fail e -> Fail e | Return i0 -> begin match list_nth_mut_fwd t tl i0 with - | Fail -> Fail + | Fail e -> Fail e | Return x0 -> Return x0 end end - | ListNil -> Fail + | ListNil -> Fail Failure end (** [paper::list_nth_mut] *) @@ -82,14 +84,14 @@ let rec list_nth_mut_back then Return (ListCons ret tl) else begin match u32_sub i 1 with - | Fail -> Fail + | Fail e -> Fail e | Return i0 -> begin match list_nth_mut_back t tl i0 ret with - | Fail -> Fail + | Fail e -> Fail e | Return tl0 -> Return (ListCons x tl0) end end - | ListNil -> Fail + | ListNil -> Fail Failure end (** [paper::sum] *) @@ -97,9 +99,12 @@ let rec sum_fwd (l : list_t i32) : result i32 = begin match l with | ListCons x tl -> begin match sum_fwd tl with - | Fail -> Fail + | Fail e -> Fail e | Return i -> - begin match i32_add x i with | Fail -> Fail | Return i0 -> Return i0 end + begin match i32_add x i with + | Fail e -> Fail e + | Return i0 -> Return i0 + end end | ListNil -> Return 0 end @@ -110,17 +115,17 @@ let test_nth_fwd : result unit = let l0 = ListCons 3 l in let l1 = ListCons 2 l0 in begin match list_nth_mut_fwd i32 (ListCons 1 l1) 2 with - | Fail -> Fail + | Fail e -> Fail e | Return x -> begin match i32_add x 1 with - | Fail -> Fail + | Fail e -> Fail e | Return x0 -> begin match list_nth_mut_back i32 (ListCons 1 l1) 2 x0 with - | Fail -> Fail + | Fail e -> Fail e | Return l2 -> begin match sum_fwd l2 with - | Fail -> Fail - | Return i -> if not (i = 7) then Fail else Return () + | Fail e -> Fail e + | Return i -> if not (i = 7) then Fail Failure else Return () end end end @@ -133,13 +138,13 @@ let _ = assert_norm (test_nth_fwd = Return ()) let call_choose_fwd (p : (u32 & u32)) : result u32 = let (px, py) = p in begin match choose_fwd u32 true px py with - | Fail -> Fail + | Fail e -> Fail e | Return pz -> begin match u32_add pz 1 with - | Fail -> Fail + | Fail e -> Fail e | Return pz0 -> begin match choose_back u32 true px py pz0 with - | Fail -> Fail + | Fail e -> Fail e | Return (px0, _) -> Return px0 end end diff --git a/tests/fstar/misc/PoloniusList.fst b/tests/fstar/misc/PoloniusList.fst index 73e98884..158a5fc7 100644 --- a/tests/fstar/misc/PoloniusList.fst +++ b/tests/fstar/misc/PoloniusList.fst @@ -18,7 +18,7 @@ let rec get_list_at_x_fwd (ls : list_t u32) (x : u32) : result (list_t u32) = then Return (ListCons hd tl) else begin match get_list_at_x_fwd tl x with - | Fail -> Fail + | Fail e -> Fail e | Return l -> Return l end | ListNil -> Return ListNil @@ -33,7 +33,7 @@ let rec get_list_at_x_back then Return ret else begin match get_list_at_x_back tl x ret with - | Fail -> Fail + | Fail e -> Fail e | Return tl0 -> Return (ListCons hd tl0) end | ListNil -> Return ret diff --git a/tests/fstar/misc/Primitives.fst b/tests/fstar/misc/Primitives.fst index 96138e46..82622656 100644 --- a/tests/fstar/misc/Primitives.fst +++ b/tests/fstar/misc/Primitives.fst @@ -18,9 +18,13 @@ let rec list_update #a ls i x = #pop-options (*** Result *) +type error : Type0 = +| Failure +| OutOfFuel + type result (a : Type0) : Type0 = | Return : v:a -> result a -| Fail : result a +| Fail : e:error -> result a // Monadic bind and return. // Re-definining those allows us to customize the result of the monadic notations @@ -29,10 +33,10 @@ let return (#a : Type0) (x:a) : result a = Return x let bind (#a #b : Type0) (m : result a) (f : a -> result b) : result b = match m with | Return x -> f x - | Fail -> Fail + | Fail e -> Fail e // Monadic assert(...) -let massert (b:bool) : result unit = if b then Return () else Fail +let massert (b:bool) : result unit = if b then Return () else Fail Failure // Normalize and unwrap a successful result (used for globals). let eval_global (#a : Type0) (x : result a{Return? (normalize_term x)}) : a = Return?.v x @@ -119,12 +123,12 @@ let scalar_max (ty : scalar_ty) : int = type scalar (ty : scalar_ty) : eqtype = x:int{scalar_min ty <= x && x <= scalar_max ty} let mk_scalar (ty : scalar_ty) (x : int) : result (scalar ty) = - if scalar_min ty <= x && scalar_max ty >= x then Return x else Fail + if scalar_min ty <= x && scalar_max ty >= x then Return x else Fail Failure let scalar_neg (#ty : scalar_ty) (x : scalar ty) : result (scalar ty) = mk_scalar ty (-x) let scalar_div (#ty : scalar_ty) (x : scalar ty) (y : scalar ty) : result (scalar ty) = - if y <> 0 then mk_scalar ty (x / y) else Fail + if y <> 0 then mk_scalar ty (x / y) else Fail Failure /// The remainder operation let int_rem (x : int) (y : int{y <> 0}) : int = @@ -137,7 +141,7 @@ let _ = assert_norm(int_rem 1 (-2) = 1) let _ = assert_norm(int_rem (-1) (-2) = -1) let scalar_rem (#ty : scalar_ty) (x : scalar ty) (y : scalar ty) : result (scalar ty) = - if y <> 0 then mk_scalar ty (int_rem x y) else Fail + if y <> 0 then mk_scalar ty (int_rem x y) else Fail Failure let scalar_add (#ty : scalar_ty) (x : scalar ty) (y : scalar ty) : result (scalar ty) = mk_scalar ty (x + y) @@ -258,7 +262,7 @@ let vec_push_back (a : Type0) (v : vec a) (x : a) : (requires True) (ensures (fun res -> match res with - | Fail -> True + | Fail e -> e == Failure | Return v' -> length v' = length v + 1)) = if length v < usize_max then begin (**) assert_norm(length [x] == 1); @@ -266,22 +270,22 @@ let vec_push_back (a : Type0) (v : vec a) (x : a) : (**) assert(length (append v [x]) = length v + 1); Return (append v [x]) end - else Fail + else Fail Failure // The **forward** function shouldn't be used let vec_insert_fwd (a : Type0) (v : vec a) (i : usize) (x : a) : result unit = - if i < length v then Return () else Fail + if i < length v then Return () else Fail Failure let vec_insert_back (a : Type0) (v : vec a) (i : usize) (x : a) : result (vec a) = - if i < length v then Return (list_update v i x) else Fail + if i < length v then Return (list_update v i x) else Fail Failure // The **backward** function shouldn't be used let vec_index_fwd (a : Type0) (v : vec a) (i : usize) : result a = - if i < length v then Return (index v i) else Fail + if i < length v then Return (index v i) else Fail Failure let vec_index_back (a : Type0) (v : vec a) (i : usize) (x : a) : result unit = - if i < length v then Return () else Fail + if i < length v then Return () else Fail Failure let vec_index_mut_fwd (a : Type0) (v : vec a) (i : usize) : result a = - if i < length v then Return (index v i) else Fail + if i < length v then Return (index v i) else Fail Failure let vec_index_mut_back (a : Type0) (v : vec a) (i : usize) (nx : a) : result (vec a) = - if i < length v then Return (list_update v i nx) else Fail + if i < length v then Return (list_update v i nx) else Fail Failure |