diff options
Diffstat (limited to 'tests')
23 files changed, 391 insertions, 334 deletions
diff --git a/tests/coq/betree/BetreeMain_Funs.v b/tests/coq/betree/BetreeMain_Funs.v index 10cdedd1..fe22b029 100644 --- a/tests/coq/betree/BetreeMain_Funs.v +++ b/tests/coq/betree/BetreeMain_Funs.v @@ -1156,6 +1156,7 @@ Definition betree_be_tree_lookup_back . (** [betree_main::main] *) -Definition main_fwd : result unit := Return tt. +Definition main_fwd : result unit := + Return tt. End BetreeMain_Funs . diff --git a/tests/coq/betree/_CoqProject b/tests/coq/betree/_CoqProject index 42c62421..e5a3f799 100644 --- a/tests/coq/betree/_CoqProject +++ b/tests/coq/betree/_CoqProject @@ -3,7 +3,7 @@ -arg -w -arg all -BetreeMain_Types.v Primitives.v +BetreeMain_Types.v BetreeMain_Funs.v BetreeMain_Opaque.v diff --git a/tests/coq/hashmap/Hashmap_Funs.v b/tests/coq/hashmap/Hashmap_Funs.v index f1af0c21..b952e60c 100644 --- a/tests/coq/hashmap/Hashmap_Funs.v +++ b/tests/coq/hashmap/Hashmap_Funs.v @@ -9,7 +9,8 @@ Import Hashmap_Types. Module Hashmap_Funs. (** [hashmap::hash_key] *) -Definition hash_key_fwd (k : usize) : result usize := Return k. +Definition hash_key_fwd (k : usize) : result usize := + Return k. (** [hashmap::HashMap::{0}::allocate_slots] *) Fixpoint hash_map_allocate_slots_loop_fwd diff --git a/tests/coq/hashmap/_CoqProject b/tests/coq/hashmap/_CoqProject index 7f80afbf..daa9b2ba 100644 --- a/tests/coq/hashmap/_CoqProject +++ b/tests/coq/hashmap/_CoqProject @@ -3,6 +3,6 @@ -arg -w -arg all -Hashmap_Types.v Primitives.v +Hashmap_Types.v Hashmap_Funs.v diff --git a/tests/coq/hashmap_on_disk/HashmapMain_Funs.v b/tests/coq/hashmap_on_disk/HashmapMain_Funs.v index 7c86dbe1..2a3ad87c 100644 --- a/tests/coq/hashmap_on_disk/HashmapMain_Funs.v +++ b/tests/coq/hashmap_on_disk/HashmapMain_Funs.v @@ -11,7 +11,8 @@ Import HashmapMain_Opaque. Module HashmapMain_Funs. (** [hashmap_main::hashmap::hash_key] *) -Definition hashmap_hash_key_fwd (k : usize) : result usize := Return k. +Definition hashmap_hash_key_fwd (k : usize) : result usize := + Return k. (** [hashmap_main::hashmap::HashMap::{0}::allocate_slots] *) Fixpoint hashmap_hash_map_allocate_slots_loop_fwd @@ -598,7 +599,8 @@ Definition insert_on_disk_fwd . (** [hashmap_main::main] *) -Definition main_fwd : result unit := Return tt. +Definition main_fwd : result unit := + Return tt. (** Unit test for [hashmap_main::main] *) Check (main_fwd )%return. diff --git a/tests/coq/misc/Constants.v b/tests/coq/misc/Constants.v index acc15a13..0a72558d 100644 --- a/tests/coq/misc/Constants.v +++ b/tests/coq/misc/Constants.v @@ -23,7 +23,8 @@ Definition x2_body : result u32 := Return (3%u32). Definition x2_c : u32 := x2_body%global. (** [constants::incr] *) -Definition incr_fwd (n : u32) : result u32 := u32_add n 1%u32. +Definition incr_fwd (n : u32) : result u32 := + u32_add n 1%u32. (** [constants::X3] *) Definition x3_body : result u32 := incr_fwd (32%u32). @@ -80,7 +81,8 @@ Definition y_body : result (Wrap_t i32) := wrap_new_fwd i32 (2%i32). Definition y_c : Wrap_t i32 := y_body%global. (** [constants::unwrap_y] *) -Definition unwrap_y_fwd : result i32 := Return y_c.(Wrap_val). +Definition unwrap_y_fwd : result i32 := + Return y_c.(Wrap_val). (** [constants::YVAL] *) Definition yval_body : result i32 := unwrap_y_fwd. @@ -91,10 +93,12 @@ Definition get_z1_z1_body : result i32 := Return (3%i32). Definition get_z1_z1_c : i32 := get_z1_z1_body%global. (** [constants::get_z1] *) -Definition get_z1_fwd : result i32 := Return get_z1_z1_c. +Definition get_z1_fwd : result i32 := + Return get_z1_z1_c. (** [constants::add] *) -Definition add_fwd (a : i32) (b : i32) : result i32 := i32_add a b. +Definition add_fwd (a : i32) (b : i32) : result i32 := + i32_add a b. (** [constants::Q1] *) Definition q1_body : result i32 := Return (5%i32). diff --git a/tests/coq/misc/NoNestedBorrows.v b/tests/coq/misc/NoNestedBorrows.v index 10654887..98ed1cf6 100644 --- a/tests/coq/misc/NoNestedBorrows.v +++ b/tests/coq/misc/NoNestedBorrows.v @@ -46,28 +46,36 @@ Arguments SumLeft {T1} {T2} _. Arguments SumRight {T1} {T2} _. (** [no_nested_borrows::neg_test] *) -Definition neg_test_fwd (x : i32) : result i32 := i32_neg x. +Definition neg_test_fwd (x : i32) : result i32 := + i32_neg x. (** [no_nested_borrows::add_test] *) -Definition add_test_fwd (x : u32) (y : u32) : result u32 := u32_add x y. +Definition add_test_fwd (x : u32) (y : u32) : result u32 := + u32_add x y. (** [no_nested_borrows::subs_test] *) -Definition subs_test_fwd (x : u32) (y : u32) : result u32 := u32_sub x y. +Definition subs_test_fwd (x : u32) (y : u32) : result u32 := + u32_sub x y. (** [no_nested_borrows::div_test] *) -Definition div_test_fwd (x : u32) (y : u32) : result u32 := u32_div x y. +Definition div_test_fwd (x : u32) (y : u32) : result u32 := + u32_div x y. (** [no_nested_borrows::div_test1] *) -Definition div_test1_fwd (x : u32) : result u32 := u32_div x 2%u32. +Definition div_test1_fwd (x : u32) : result u32 := + u32_div x 2%u32. (** [no_nested_borrows::rem_test] *) -Definition rem_test_fwd (x : u32) (y : u32) : result u32 := u32_rem x y. +Definition rem_test_fwd (x : u32) (y : u32) : result u32 := + u32_rem x y. (** [no_nested_borrows::cast_test] *) -Definition cast_test_fwd (x : u32) : result i32 := scalar_cast U32 I32 x. +Definition cast_test_fwd (x : u32) : result i32 := + scalar_cast U32 I32 x. (** [no_nested_borrows::test2] *) -Definition test2_fwd : result unit := _ <- u32_add 23%u32 44%u32; Return tt. +Definition test2_fwd : result unit := + _ <- u32_add 23%u32 44%u32; Return tt. (** Unit test for [no_nested_borrows::test2] *) Check (test2_fwd )%return. @@ -122,7 +130,8 @@ Definition refs_test2_fwd : result unit := Check (refs_test2_fwd )%return. (** [no_nested_borrows::test_list1] *) -Definition test_list1_fwd : result unit := Return tt. +Definition test_list1_fwd : result unit := + Return tt. (** Unit test for [no_nested_borrows::test_list1] *) Check (test_list1_fwd )%return. @@ -138,7 +147,8 @@ Definition test_box1_fwd : result unit := Check (test_box1_fwd )%return. (** [no_nested_borrows::copy_int] *) -Definition copy_int_fwd (x : i32) : result i32 := Return x. +Definition copy_int_fwd (x : i32) : result i32 := + Return x. (** [no_nested_borrows::test_unreachable] *) Definition test_unreachable_fwd (b : bool) : result unit := @@ -468,7 +478,8 @@ Definition test_constants_fwd : result unit := Check (test_constants_fwd )%return. (** [no_nested_borrows::test_weird_borrows1] *) -Definition test_weird_borrows1_fwd : result unit := Return tt. +Definition test_weird_borrows1_fwd : result unit := + Return tt. (** Unit test for [no_nested_borrows::test_weird_borrows1] *) Check (test_weird_borrows1_fwd )%return. @@ -485,7 +496,8 @@ Definition test_shared_borrow_bool1_fwd (b : bool) : result u32 := . (** [no_nested_borrows::test_shared_borrow_bool2] *) -Definition test_shared_borrow_bool2_fwd : result u32 := Return (0%u32). +Definition test_shared_borrow_bool2_fwd : result u32 := + Return (0%u32). (** [no_nested_borrows::test_shared_borrow_enum1] *) Definition test_shared_borrow_enum1_fwd (l : List_t u32) : result u32 := @@ -496,6 +508,7 @@ Definition test_shared_borrow_enum1_fwd (l : List_t u32) : result u32 := . (** [no_nested_borrows::test_shared_borrow_enum2] *) -Definition test_shared_borrow_enum2_fwd : result u32 := Return (0%u32). +Definition test_shared_borrow_enum2_fwd : result u32 := + Return (0%u32). End NoNestedBorrows . diff --git a/tests/coq/misc/Paper.v b/tests/coq/misc/Paper.v index cb4486c6..8045222d 100644 --- a/tests/coq/misc/Paper.v +++ b/tests/coq/misc/Paper.v @@ -7,7 +7,8 @@ Local Open Scope Primitives_scope. Module Paper. (** [paper::ref_incr] *) -Definition ref_incr_fwd_back (x : i32) : result i32 := i32_add x 1%i32. +Definition ref_incr_fwd_back (x : i32) : result i32 := + i32_add x 1%i32. (** [paper::test_incr] *) Definition test_incr_fwd : result unit := diff --git a/tests/coq/misc/_CoqProject b/tests/coq/misc/_CoqProject index db6c2742..87dea3e6 100644 --- a/tests/coq/misc/_CoqProject +++ b/tests/coq/misc/_CoqProject @@ -3,12 +3,12 @@ -arg -w -arg all -Loops.v +Constants.v +External_Types.v Primitives.v +Loops.v External_Funs.v -Constants.v PoloniusList.v -External_Types.v NoNestedBorrows.v External_Opaque.v Paper.v diff --git a/tests/fstar/betree/BetreeMain.Funs.fst b/tests/fstar/betree/BetreeMain.Funs.fst index 8c0c1cc1..f3a01884 100644 --- a/tests/fstar/betree/BetreeMain.Funs.fst +++ b/tests/fstar/betree/BetreeMain.Funs.fst @@ -41,7 +41,8 @@ let betree_fresh_node_id_fwd (counter : u64) : result u64 = let* _ = u64_add counter 1 in Return counter (** [betree_main::betree::fresh_node_id] *) -let betree_fresh_node_id_back (counter : u64) : result u64 = u64_add counter 1 +let betree_fresh_node_id_back (counter : u64) : result u64 = + u64_add counter 1 (** [betree_main::betree::NodeIdCounter::{0}::new] *) let betree_node_id_counter_new_fwd : result betree_node_id_counter_t = @@ -161,11 +162,11 @@ let rec betree_list_partition_at_pivot_fwd let (i, x) = hd in if i >= pivot then Return (BetreeListNil, BetreeListCons (i, x) tl) - else begin + else let* p = betree_list_partition_at_pivot_fwd t tl pivot in let (ls0, ls1) = p in let l = ls0 in - Return (BetreeListCons (i, x) l, ls1) end + Return (BetreeListCons (i, x) l, ls1) | BetreeListNil -> Return (BetreeListNil, BetreeListNil) end @@ -257,10 +258,10 @@ let rec betree_node_lookup_first_message_for_key_back let (i, m) = x in if i >= key then Return ret - else begin + else let* next_msgs0 = betree_node_lookup_first_message_for_key_back key next_msgs ret in - Return (BetreeListCons (i, m) next_msgs0) end + Return (BetreeListCons (i, m) next_msgs0) | BetreeListNil -> Return ret end @@ -273,7 +274,7 @@ let rec betree_node_apply_upserts_fwd = let* b = betree_list_head_has_key_fwd betree_message_t msgs key in if b - then begin + then let* msg = betree_list_pop_front_fwd (u64 & betree_message_t) msgs in let (_, m) = msg in begin match m with @@ -283,13 +284,13 @@ let rec betree_node_apply_upserts_fwd let* v = betree_upsert_update_fwd prev s in let* msgs0 = betree_list_pop_front_back (u64 & betree_message_t) msgs in betree_node_apply_upserts_fwd msgs0 (Some v) key st - end end - else begin + end + else let* (st0, v) = core_option_option_unwrap_fwd u64 prev st in let* _ = betree_list_push_front_fwd_back (u64 & betree_message_t) msgs (key, BetreeMessageInsert v) in - Return (st0, v) end + Return (st0, v) (** [betree_main::betree::Node::{5}::apply_upserts] *) let rec betree_node_apply_upserts_back @@ -300,7 +301,7 @@ let rec betree_node_apply_upserts_back = let* b = betree_list_head_has_key_fwd betree_message_t msgs key in if b - then begin + then let* msg = betree_list_pop_front_fwd (u64 & betree_message_t) msgs in let (_, m) = msg in begin match m with @@ -310,11 +311,11 @@ let rec betree_node_apply_upserts_back let* v = betree_upsert_update_fwd prev s in let* msgs0 = betree_list_pop_front_back (u64 & betree_message_t) msgs in betree_node_apply_upserts_back msgs0 (Some v) key st - end end - else begin + end + else let* (_, v) = core_option_option_unwrap_fwd u64 prev st in betree_list_push_front_fwd_back (u64 & betree_message_t) msgs (key, - BetreeMessageInsert v) end + BetreeMessageInsert v) (** [betree_main::betree::Node::{5}::lookup] *) let rec betree_node_lookup_fwd @@ -331,13 +332,13 @@ let rec betree_node_lookup_fwd | BetreeListCons p l -> let (k, msg) = p in if k <> key - then begin + then let* (st1, opt) = betree_internal_lookup_in_children_fwd node key st0 in let* _ = betree_node_lookup_first_message_for_key_back key msgs (BetreeListCons (k, msg) l) in - Return (st1, opt) end + Return (st1, opt) else begin match msg with | BetreeMessageInsert v -> @@ -394,12 +395,12 @@ and betree_node_lookup_back | BetreeListCons p l -> let (k, msg) = p in if k <> key - then begin + then let* _ = betree_node_lookup_first_message_for_key_back key msgs (BetreeListCons (k, msg) l) in let* node0 = betree_internal_lookup_in_children_back node key st0 in - Return (BetreeNodeInternal node0) end + Return (BetreeNodeInternal node0) else begin match msg with | BetreeMessageInsert v -> @@ -458,14 +459,14 @@ and betree_internal_lookup_in_children_back (decreases (betree_internal_lookup_in_children_decreases self key st)) = if key < self.betree_internal_pivot - then begin + then let* n = betree_node_lookup_back self.betree_internal_left key st in Return (Mkbetree_internal_t self.betree_internal_id - self.betree_internal_pivot n self.betree_internal_right) end - else begin + self.betree_internal_pivot n self.betree_internal_right) + else let* n = betree_node_lookup_back self.betree_internal_right key st in Return (Mkbetree_internal_t self.betree_internal_id - self.betree_internal_pivot self.betree_internal_left n) end + self.betree_internal_pivot self.betree_internal_left n) (** [betree_main::betree::Node::{5}::lookup_mut_in_bindings] *) let rec betree_node_lookup_mut_in_bindings_fwd @@ -494,9 +495,9 @@ let rec betree_node_lookup_mut_in_bindings_back let (i, i0) = hd in if i >= key then Return ret - else begin + else let* tl0 = betree_node_lookup_mut_in_bindings_back key tl ret in - Return (BetreeListCons (i, i0) tl0) end + Return (BetreeListCons (i, i0) tl0) | BetreeListNil -> Return ret end @@ -509,7 +510,7 @@ let betree_node_apply_to_leaf_fwd_back let* bindings0 = betree_node_lookup_mut_in_bindings_fwd key bindings in let* b = betree_list_head_has_key_fwd u64 bindings0 key in if b - then begin + then let* hd = betree_list_pop_front_fwd (u64 & u64) bindings0 in begin match new_msg with | BetreeMessageInsert v -> @@ -527,7 +528,7 @@ let betree_node_apply_to_leaf_fwd_back let* bindings2 = betree_list_push_front_fwd_back (u64 & u64) bindings1 (key, v) in betree_node_lookup_mut_in_bindings_back key bindings bindings2 - end end + end else begin match new_msg with | BetreeMessageInsert v -> @@ -568,11 +569,11 @@ let rec betree_node_filter_messages_for_key_fwd_back | BetreeListCons p l -> let (k, m) = p in if k = key - then begin + then let* msgs0 = betree_list_pop_front_back (u64 & betree_message_t) (BetreeListCons (k, m) l) in - betree_node_filter_messages_for_key_fwd_back key msgs0 end + betree_node_filter_messages_for_key_fwd_back key msgs0 else Return (BetreeListCons (k, m) l) | BetreeListNil -> Return BetreeListNil end @@ -603,10 +604,10 @@ let rec betree_node_lookup_first_message_after_key_back | BetreeListCons p next_msgs -> let (k, m) = p in if k = key - then begin + then let* next_msgs0 = betree_node_lookup_first_message_after_key_back key next_msgs ret in - Return (BetreeListCons (k, m) next_msgs0) end + Return (BetreeListCons (k, m) next_msgs0) else Return ret | BetreeListNil -> Return ret end @@ -665,11 +666,11 @@ let betree_node_apply_to_internal_fwd_back betree_node_lookup_first_message_for_key_back key msgs msgs3 end end - else begin + else let* msgs1 = betree_list_push_front_fwd_back (u64 & betree_message_t) msgs0 (key, new_msg) in - betree_node_lookup_first_message_for_key_back key msgs msgs1 end + betree_node_lookup_first_message_for_key_back key msgs msgs1 (** [betree_main::betree::Node::{5}::apply_messages_to_internal] *) let rec betree_node_apply_messages_to_internal_fwd_back @@ -703,34 +704,34 @@ let rec betree_node_apply_messages_fwd betree_node_apply_messages_to_internal_fwd_back content msgs in let* num_msgs = betree_list_len_fwd (u64 & betree_message_t) content0 in if num_msgs >= params.betree_params_min_flush_size - then begin + then let* (st1, content1) = betree_internal_flush_fwd node params node_id_cnt content0 st0 in let* (node0, _) = betree_internal_flush_back node params node_id_cnt content0 st0 in let* (st2, _) = betree_store_internal_node_fwd node0.betree_internal_id content1 st1 in - Return (st2, ()) end - else begin + Return (st2, ()) + else let* (st1, _) = betree_store_internal_node_fwd node.betree_internal_id content0 st0 in - Return (st1, ()) end + Return (st1, ()) | BetreeNodeLeaf node -> let* (st0, content) = betree_load_leaf_node_fwd node.betree_leaf_id st in let* content0 = betree_node_apply_messages_to_leaf_fwd_back content msgs in let* len = betree_list_len_fwd (u64 & u64) content0 in let* i = u64_mul 2 params.betree_params_split_size in if len >= i - then begin + then let* (st1, _) = betree_leaf_split_fwd node content0 params node_id_cnt st0 in let* (st2, _) = betree_store_leaf_node_fwd node.betree_leaf_id BetreeListNil st1 in - Return (st2, ()) end - else begin + Return (st2, ()) + else let* (st1, _) = betree_store_leaf_node_fwd node.betree_leaf_id content0 st0 in - Return (st1, ()) end + Return (st1, ()) end (** [betree_main::betree::Node::{5}::apply_messages] *) @@ -750,36 +751,36 @@ and betree_node_apply_messages_back betree_node_apply_messages_to_internal_fwd_back content msgs in let* num_msgs = betree_list_len_fwd (u64 & betree_message_t) content0 in if num_msgs >= params.betree_params_min_flush_size - then begin + then let* (st1, content1) = betree_internal_flush_fwd node params node_id_cnt content0 st0 in let* (node0, node_id_cnt0) = betree_internal_flush_back node params node_id_cnt content0 st0 in let* _ = betree_store_internal_node_fwd node0.betree_internal_id content1 st1 in - Return (BetreeNodeInternal node0, node_id_cnt0) end - else begin + Return (BetreeNodeInternal node0, node_id_cnt0) + else let* _ = betree_store_internal_node_fwd node.betree_internal_id content0 st0 in - Return (BetreeNodeInternal node, node_id_cnt) end + Return (BetreeNodeInternal node, node_id_cnt) | BetreeNodeLeaf node -> let* (st0, content) = betree_load_leaf_node_fwd node.betree_leaf_id st in let* content0 = betree_node_apply_messages_to_leaf_fwd_back content msgs in let* len = betree_list_len_fwd (u64 & u64) content0 in let* i = u64_mul 2 params.betree_params_split_size in if len >= i - then begin + then let* (st1, new_node) = betree_leaf_split_fwd node content0 params node_id_cnt st0 in let* _ = betree_store_leaf_node_fwd node.betree_leaf_id BetreeListNil st1 in let* node_id_cnt0 = betree_leaf_split_back node content0 params node_id_cnt st0 in - Return (BetreeNodeInternal new_node, node_id_cnt0) end - else begin + Return (BetreeNodeInternal new_node, node_id_cnt0) + else let* _ = betree_store_leaf_node_fwd node.betree_leaf_id content0 st0 in Return (BetreeNodeLeaf (Mkbetree_leaf_t node.betree_leaf_id len), - node_id_cnt) end + node_id_cnt) end (** [betree_main::betree::Internal::{4}::flush] *) @@ -797,7 +798,7 @@ and betree_internal_flush_fwd let (msgs_left, msgs_right) = p in let* len_left = betree_list_len_fwd (u64 & betree_message_t) msgs_left in if len_left >= params.betree_params_min_flush_size - then begin + then let* (st0, _) = betree_node_apply_messages_fwd self.betree_internal_left params node_id_cnt msgs_left st in @@ -806,23 +807,23 @@ and betree_internal_flush_fwd node_id_cnt msgs_left st in let* len_right = betree_list_len_fwd (u64 & betree_message_t) msgs_right in if len_right >= params.betree_params_min_flush_size - then begin + then let* (st1, _) = betree_node_apply_messages_fwd self.betree_internal_right params node_id_cnt0 msgs_right st0 in let* _ = betree_node_apply_messages_back self.betree_internal_right params node_id_cnt0 msgs_right st0 in - Return (st1, BetreeListNil) end - else Return (st0, msgs_right) end - else begin + Return (st1, BetreeListNil) + else Return (st0, msgs_right) + else let* (st0, _) = betree_node_apply_messages_fwd self.betree_internal_right params node_id_cnt msgs_right st in let* _ = betree_node_apply_messages_back self.betree_internal_right params node_id_cnt msgs_right st in - Return (st0, msgs_left) end + Return (st0, msgs_left) (** [betree_main::betree::Internal::{4}::flush] *) and betree_internal_flush_back @@ -839,7 +840,7 @@ and betree_internal_flush_back let (msgs_left, msgs_right) = p in let* len_left = betree_list_len_fwd (u64 & betree_message_t) msgs_left in if len_left >= params.betree_params_min_flush_size - then begin + then let* (st0, _) = betree_node_apply_messages_fwd self.betree_internal_left params node_id_cnt msgs_left st in @@ -848,22 +849,21 @@ and betree_internal_flush_back node_id_cnt msgs_left st in let* len_right = betree_list_len_fwd (u64 & betree_message_t) msgs_right in if len_right >= params.betree_params_min_flush_size - then begin + then let* (n0, node_id_cnt1) = betree_node_apply_messages_back self.betree_internal_right params node_id_cnt0 msgs_right st0 in Return (Mkbetree_internal_t self.betree_internal_id - self.betree_internal_pivot n n0, node_id_cnt1) end + self.betree_internal_pivot n n0, node_id_cnt1) else Return (Mkbetree_internal_t self.betree_internal_id self.betree_internal_pivot n self.betree_internal_right, node_id_cnt0) - end - else begin + else let* (n, node_id_cnt0) = betree_node_apply_messages_back self.betree_internal_right params node_id_cnt msgs_right st in Return (Mkbetree_internal_t self.betree_internal_id - self.betree_internal_pivot self.betree_internal_left n, node_id_cnt0) end + self.betree_internal_pivot self.betree_internal_left n, node_id_cnt0) (** [betree_main::betree::Node::{5}::apply] *) let betree_node_apply_fwd @@ -994,7 +994,8 @@ let betree_be_tree_lookup_back self.betree_be_tree_node_id_cnt n) (** [betree_main::main] *) -let main_fwd : result unit = Return () +let main_fwd : result unit = + Return () (** Unit test for [betree_main::main] *) let _ = assert_norm (main_fwd = Return ()) diff --git a/tests/fstar/betree_back_stateful/BetreeMain.Funs.fst b/tests/fstar/betree_back_stateful/BetreeMain.Funs.fst index 201778df..7e44928c 100644 --- a/tests/fstar/betree_back_stateful/BetreeMain.Funs.fst +++ b/tests/fstar/betree_back_stateful/BetreeMain.Funs.fst @@ -41,7 +41,8 @@ let betree_fresh_node_id_fwd (counter : u64) : result u64 = let* _ = u64_add counter 1 in Return counter (** [betree_main::betree::fresh_node_id] *) -let betree_fresh_node_id_back (counter : u64) : result u64 = u64_add counter 1 +let betree_fresh_node_id_back (counter : u64) : result u64 = + u64_add counter 1 (** [betree_main::betree::NodeIdCounter::{0}::new] *) let betree_node_id_counter_new_fwd : result betree_node_id_counter_t = @@ -161,11 +162,11 @@ let rec betree_list_partition_at_pivot_fwd let (i, x) = hd in if i >= pivot then Return (BetreeListNil, BetreeListCons (i, x) tl) - else begin + else let* p = betree_list_partition_at_pivot_fwd t tl pivot in let (ls0, ls1) = p in let l = ls0 in - Return (BetreeListCons (i, x) l, ls1) end + Return (BetreeListCons (i, x) l, ls1) | BetreeListNil -> Return (BetreeListNil, BetreeListNil) end @@ -296,10 +297,10 @@ let rec betree_node_lookup_first_message_for_key_back let (i, m) = x in if i >= key then Return ret - else begin + else let* next_msgs0 = betree_node_lookup_first_message_for_key_back key next_msgs ret in - Return (BetreeListCons (i, m) next_msgs0) end + Return (BetreeListCons (i, m) next_msgs0) | BetreeListNil -> Return ret end @@ -312,7 +313,7 @@ let rec betree_node_apply_upserts_fwd = let* b = betree_list_head_has_key_fwd betree_message_t msgs key in if b - then begin + then let* msg = betree_list_pop_front_fwd (u64 & betree_message_t) msgs in let (_, m) = msg in begin match m with @@ -322,13 +323,13 @@ let rec betree_node_apply_upserts_fwd let* v = betree_upsert_update_fwd prev s in let* msgs0 = betree_list_pop_front_back (u64 & betree_message_t) msgs in betree_node_apply_upserts_fwd msgs0 (Some v) key st - end end - else begin + end + else let* (st0, v) = core_option_option_unwrap_fwd u64 prev st in let* _ = betree_list_push_front_fwd_back (u64 & betree_message_t) msgs (key, BetreeMessageInsert v) in - Return (st0, v) end + Return (st0, v) (** [betree_main::betree::Node::{5}::apply_upserts] *) let rec betree_node_apply_upserts_back @@ -339,7 +340,7 @@ let rec betree_node_apply_upserts_back = let* b = betree_list_head_has_key_fwd betree_message_t msgs key in if b - then begin + then let* msg = betree_list_pop_front_fwd (u64 & betree_message_t) msgs in let (_, m) = msg in begin match m with @@ -349,13 +350,13 @@ let rec betree_node_apply_upserts_back let* v = betree_upsert_update_fwd prev s in let* msgs0 = betree_list_pop_front_back (u64 & betree_message_t) msgs in betree_node_apply_upserts_back msgs0 (Some v) key st st0 - end end - else begin + end + else let* (_, v) = core_option_option_unwrap_fwd u64 prev st in let* msgs0 = betree_list_push_front_fwd_back (u64 & betree_message_t) msgs (key, BetreeMessageInsert v) in - Return (st0, msgs0) end + Return (st0, msgs0) (** [betree_main::betree::Node::{5}::lookup] *) let rec betree_node_lookup_fwd @@ -372,13 +373,13 @@ let rec betree_node_lookup_fwd | BetreeListCons p l -> let (k, msg) = p in if k <> key - then begin + then let* (st1, opt) = betree_internal_lookup_in_children_fwd node key st0 in let* _ = betree_node_lookup_first_message_for_key_back key msgs (BetreeListCons (k, msg) l) in - Return (st1, opt) end + Return (st1, opt) else begin match msg with | BetreeMessageInsert v -> @@ -436,13 +437,13 @@ and betree_node_lookup_back | BetreeListCons p l -> let (k, msg) = p in if k <> key - then begin + then let* _ = betree_node_lookup_first_message_for_key_back key msgs (BetreeListCons (k, msg) l) in let* (st2, node0) = betree_internal_lookup_in_children_back node key st1 st0 in - Return (st2, BetreeNodeInternal node0) end + Return (st2, BetreeNodeInternal node0) else begin match msg with | BetreeMessageInsert v -> @@ -503,16 +504,16 @@ and betree_internal_lookup_in_children_back (decreases (betree_internal_lookup_in_children_decreases self key st)) = if key < self.betree_internal_pivot - then begin + then let* (st1, n) = betree_node_lookup_back self.betree_internal_left key st st0 in Return (st1, Mkbetree_internal_t self.betree_internal_id - self.betree_internal_pivot n self.betree_internal_right) end - else begin + self.betree_internal_pivot n self.betree_internal_right) + else let* (st1, n) = betree_node_lookup_back self.betree_internal_right key st st0 in Return (st1, Mkbetree_internal_t self.betree_internal_id - self.betree_internal_pivot self.betree_internal_left n) end + self.betree_internal_pivot self.betree_internal_left n) (** [betree_main::betree::Node::{5}::lookup_mut_in_bindings] *) let rec betree_node_lookup_mut_in_bindings_fwd @@ -541,9 +542,9 @@ let rec betree_node_lookup_mut_in_bindings_back let (i, i0) = hd in if i >= key then Return ret - else begin + else let* tl0 = betree_node_lookup_mut_in_bindings_back key tl ret in - Return (BetreeListCons (i, i0) tl0) end + Return (BetreeListCons (i, i0) tl0) | BetreeListNil -> Return ret end @@ -556,7 +557,7 @@ let betree_node_apply_to_leaf_fwd_back let* bindings0 = betree_node_lookup_mut_in_bindings_fwd key bindings in let* b = betree_list_head_has_key_fwd u64 bindings0 key in if b - then begin + then let* hd = betree_list_pop_front_fwd (u64 & u64) bindings0 in begin match new_msg with | BetreeMessageInsert v -> @@ -574,7 +575,7 @@ let betree_node_apply_to_leaf_fwd_back let* bindings2 = betree_list_push_front_fwd_back (u64 & u64) bindings1 (key, v) in betree_node_lookup_mut_in_bindings_back key bindings bindings2 - end end + end else begin match new_msg with | BetreeMessageInsert v -> @@ -615,11 +616,11 @@ let rec betree_node_filter_messages_for_key_fwd_back | BetreeListCons p l -> let (k, m) = p in if k = key - then begin + then let* msgs0 = betree_list_pop_front_back (u64 & betree_message_t) (BetreeListCons (k, m) l) in - betree_node_filter_messages_for_key_fwd_back key msgs0 end + betree_node_filter_messages_for_key_fwd_back key msgs0 else Return (BetreeListCons (k, m) l) | BetreeListNil -> Return BetreeListNil end @@ -650,10 +651,10 @@ let rec betree_node_lookup_first_message_after_key_back | BetreeListCons p next_msgs -> let (k, m) = p in if k = key - then begin + then let* next_msgs0 = betree_node_lookup_first_message_after_key_back key next_msgs ret in - Return (BetreeListCons (k, m) next_msgs0) end + Return (BetreeListCons (k, m) next_msgs0) else Return ret | BetreeListNil -> Return ret end @@ -712,11 +713,11 @@ let betree_node_apply_to_internal_fwd_back betree_node_lookup_first_message_for_key_back key msgs msgs3 end end - else begin + else let* msgs1 = betree_list_push_front_fwd_back (u64 & betree_message_t) msgs0 (key, new_msg) in - betree_node_lookup_first_message_for_key_back key msgs msgs1 end + betree_node_lookup_first_message_for_key_back key msgs msgs1 (** [betree_main::betree::Node::{5}::apply_messages_to_internal] *) let rec betree_node_apply_messages_to_internal_fwd_back @@ -750,7 +751,7 @@ let rec betree_node_apply_messages_fwd betree_node_apply_messages_to_internal_fwd_back content msgs in let* num_msgs = betree_list_len_fwd (u64 & betree_message_t) content0 in if num_msgs >= params.betree_params_min_flush_size - then begin + then let* (st1, content1) = betree_internal_flush_fwd node params node_id_cnt content0 st0 in let* (st2, (node0, _)) = @@ -758,27 +759,27 @@ let rec betree_node_apply_messages_fwd in let* (st3, _) = betree_store_internal_node_fwd node0.betree_internal_id content1 st2 in - Return (st3, ()) end - else begin + Return (st3, ()) + else let* (st1, _) = betree_store_internal_node_fwd node.betree_internal_id content0 st0 in - Return (st1, ()) end + Return (st1, ()) | BetreeNodeLeaf node -> let* (st0, content) = betree_load_leaf_node_fwd node.betree_leaf_id st in let* content0 = betree_node_apply_messages_to_leaf_fwd_back content msgs in let* len = betree_list_len_fwd (u64 & u64) content0 in let* i = u64_mul 2 params.betree_params_split_size in if len >= i - then begin + then let* (st1, _) = betree_leaf_split_fwd node content0 params node_id_cnt st0 in let* (st2, _) = betree_store_leaf_node_fwd node.betree_leaf_id BetreeListNil st1 in - betree_leaf_split_back0 node content0 params node_id_cnt st0 st2 end - else begin + betree_leaf_split_back0 node content0 params node_id_cnt st0 st2 + else let* (st1, _) = betree_store_leaf_node_fwd node.betree_leaf_id content0 st0 in - Return (st1, ()) end + Return (st1, ()) end (** [betree_main::betree::Node::{5}::apply_messages] *) @@ -798,7 +799,7 @@ and betree_node_apply_messages_back'a betree_node_apply_messages_to_internal_fwd_back content msgs in let* num_msgs = betree_list_len_fwd (u64 & betree_message_t) content0 in if num_msgs >= params.betree_params_min_flush_size - then begin + then let* (st2, content1) = betree_internal_flush_fwd node params node_id_cnt content0 st1 in let* (st3, (node0, node_id_cnt0)) = @@ -806,18 +807,18 @@ and betree_node_apply_messages_back'a in let* _ = betree_store_internal_node_fwd node0.betree_internal_id content1 st3 in - Return (st0, (BetreeNodeInternal node0, node_id_cnt0)) end - else begin + Return (st0, (BetreeNodeInternal node0, node_id_cnt0)) + else let* _ = betree_store_internal_node_fwd node.betree_internal_id content0 st1 in - Return (st0, (BetreeNodeInternal node, node_id_cnt)) end + Return (st0, (BetreeNodeInternal node, node_id_cnt)) | BetreeNodeLeaf node -> let* (st1, content) = betree_load_leaf_node_fwd node.betree_leaf_id st in let* content0 = betree_node_apply_messages_to_leaf_fwd_back content msgs in let* len = betree_list_len_fwd (u64 & u64) content0 in let* i = u64_mul 2 params.betree_params_split_size in if len >= i - then begin + then let* (st2, new_node) = betree_leaf_split_fwd node content0 params node_id_cnt st1 in let* (st3, _) = @@ -826,11 +827,11 @@ and betree_node_apply_messages_back'a in let* (st4, node_id_cnt0) = betree_leaf_split_back2 node content0 params node_id_cnt st1 st0 in - Return (st4, (BetreeNodeInternal new_node, node_id_cnt0)) end - else begin + Return (st4, (BetreeNodeInternal new_node, node_id_cnt0)) + else let* _ = betree_store_leaf_node_fwd node.betree_leaf_id content0 st1 in Return (st0, (BetreeNodeLeaf (Mkbetree_leaf_t node.betree_leaf_id len), - node_id_cnt)) end + node_id_cnt)) end (** [betree_main::betree::Node::{5}::apply_messages] *) @@ -850,7 +851,7 @@ and betree_node_apply_messages_back1 betree_node_apply_messages_to_internal_fwd_back content msgs in let* num_msgs = betree_list_len_fwd (u64 & betree_message_t) content0 in if num_msgs >= params.betree_params_min_flush_size - then begin + then let* (st2, content1) = betree_internal_flush_fwd node params node_id_cnt content0 st1 in let* (st3, (node0, _)) = @@ -858,28 +859,28 @@ and betree_node_apply_messages_back1 in let* _ = betree_store_internal_node_fwd node0.betree_internal_id content1 st3 in - betree_internal_flush_back1 node params node_id_cnt content0 st1 st0 end - else begin + betree_internal_flush_back1 node params node_id_cnt content0 st1 st0 + else let* _ = betree_store_internal_node_fwd node.betree_internal_id content0 st1 in - Return (st0, ()) end + Return (st0, ()) | BetreeNodeLeaf node -> let* (st1, content) = betree_load_leaf_node_fwd node.betree_leaf_id st in let* content0 = betree_node_apply_messages_to_leaf_fwd_back content msgs in let* len = betree_list_len_fwd (u64 & u64) content0 in let* i = u64_mul 2 params.betree_params_split_size in if len >= i - then begin + then let* (st2, _) = betree_leaf_split_fwd node content0 params node_id_cnt st1 in let* (st3, _) = betree_store_leaf_node_fwd node.betree_leaf_id BetreeListNil st2 in let* _ = betree_leaf_split_back0 node content0 params node_id_cnt st1 st3 in - betree_leaf_split_back1 node content0 params node_id_cnt st1 st0 end - else begin + betree_leaf_split_back1 node content0 params node_id_cnt st1 st0 + else let* _ = betree_store_leaf_node_fwd node.betree_leaf_id content0 st1 in - Return (st0, ()) end + Return (st0, ()) end (** [betree_main::betree::Internal::{4}::flush] *) @@ -897,7 +898,7 @@ and betree_internal_flush_fwd let (msgs_left, msgs_right) = p in let* len_left = betree_list_len_fwd (u64 & betree_message_t) msgs_left in if len_left >= params.betree_params_min_flush_size - then begin + then let* (st0, _) = betree_node_apply_messages_fwd self.betree_internal_left params node_id_cnt msgs_left st in @@ -909,7 +910,7 @@ and betree_internal_flush_fwd node_id_cnt msgs_left st st1 in let* len_right = betree_list_len_fwd (u64 & betree_message_t) msgs_right in if len_right >= params.betree_params_min_flush_size - then begin + then let* (st3, _) = betree_node_apply_messages_fwd self.betree_internal_right params node_id_cnt0 msgs_right st2 in @@ -919,9 +920,9 @@ and betree_internal_flush_fwd let* (st5, ()) = betree_node_apply_messages_back1 self.betree_internal_right params node_id_cnt0 msgs_right st2 st4 in - Return (st5, BetreeListNil) end - else Return (st2, msgs_right) end - else begin + Return (st5, BetreeListNil) + else Return (st2, msgs_right) + else let* (st0, _) = betree_node_apply_messages_fwd self.betree_internal_right params node_id_cnt msgs_right st in @@ -931,7 +932,7 @@ and betree_internal_flush_fwd let* (st2, ()) = betree_node_apply_messages_back1 self.betree_internal_right params node_id_cnt msgs_right st st1 in - Return (st2, msgs_left) end + Return (st2, msgs_left) (** [betree_main::betree::Internal::{4}::flush] *) and betree_internal_flush_back'a @@ -949,7 +950,7 @@ and betree_internal_flush_back'a let (msgs_left, msgs_right) = p in let* len_left = betree_list_len_fwd (u64 & betree_message_t) msgs_left in if len_left >= params.betree_params_min_flush_size - then begin + then let* (st1, _) = betree_node_apply_messages_fwd self.betree_internal_left params node_id_cnt msgs_left st in @@ -961,7 +962,7 @@ and betree_internal_flush_back'a node_id_cnt msgs_left st st2 in let* len_right = betree_list_len_fwd (u64 & betree_message_t) msgs_right in if len_right >= params.betree_params_min_flush_size - then begin + then let* (st4, _) = betree_node_apply_messages_fwd self.betree_internal_right params node_id_cnt0 msgs_right st3 in @@ -972,12 +973,11 @@ and betree_internal_flush_back'a betree_node_apply_messages_back1 self.betree_internal_right params node_id_cnt0 msgs_right st3 st5 in Return (st0, (Mkbetree_internal_t self.betree_internal_id - self.betree_internal_pivot n n0, node_id_cnt1)) end + self.betree_internal_pivot n n0, node_id_cnt1)) else Return (st0, (Mkbetree_internal_t self.betree_internal_id self.betree_internal_pivot n self.betree_internal_right, node_id_cnt0)) - end - else begin + else let* (st1, _) = betree_node_apply_messages_fwd self.betree_internal_right params node_id_cnt msgs_right st in @@ -989,7 +989,6 @@ and betree_internal_flush_back'a node_id_cnt msgs_right st st2 in Return (st0, (Mkbetree_internal_t self.betree_internal_id self.betree_internal_pivot self.betree_internal_left n, node_id_cnt0)) - end (** [betree_main::betree::Internal::{4}::flush] *) and betree_internal_flush_back1 @@ -1007,7 +1006,7 @@ and betree_internal_flush_back1 let (msgs_left, msgs_right) = p in let* len_left = betree_list_len_fwd (u64 & betree_message_t) msgs_left in if len_left >= params.betree_params_min_flush_size - then begin + then let* (st1, _) = betree_node_apply_messages_fwd self.betree_internal_left params node_id_cnt msgs_left st in @@ -1019,7 +1018,7 @@ and betree_internal_flush_back1 node_id_cnt msgs_left st st2 in let* len_right = betree_list_len_fwd (u64 & betree_message_t) msgs_right in if len_right >= params.betree_params_min_flush_size - then begin + then let* (st4, _) = betree_node_apply_messages_fwd self.betree_internal_right params node_id_cnt0 msgs_right st3 in @@ -1029,9 +1028,9 @@ and betree_internal_flush_back1 let* _ = betree_node_apply_messages_back1 self.betree_internal_right params node_id_cnt0 msgs_right st3 st5 in - Return (st0, ()) end - else Return (st0, ()) end - else begin + Return (st0, ()) + else Return (st0, ()) + else let* (st1, _) = betree_node_apply_messages_fwd self.betree_internal_right params node_id_cnt msgs_right st in @@ -1041,7 +1040,7 @@ and betree_internal_flush_back1 let* _ = betree_node_apply_messages_back1 self.betree_internal_right params node_id_cnt msgs_right st st2 in - Return (st0, ()) end + Return (st0, ()) (** [betree_main::betree::Node::{5}::apply] *) let betree_node_apply_fwd @@ -1226,7 +1225,8 @@ let betree_be_tree_lookup_back self.betree_be_tree_node_id_cnt n) (** [betree_main::main] *) -let main_fwd : result unit = Return () +let main_fwd : result unit = + Return () (** Unit test for [betree_main::main] *) let _ = assert_norm (main_fwd = Return ()) diff --git a/tests/fstar/hashmap/Hashmap.Funs.fst b/tests/fstar/hashmap/Hashmap.Funs.fst index 0140aadc..62799976 100644 --- a/tests/fstar/hashmap/Hashmap.Funs.fst +++ b/tests/fstar/hashmap/Hashmap.Funs.fst @@ -8,7 +8,8 @@ include Hashmap.Clauses #set-options "--z3rlimit 50 --fuel 1 --ifuel 1" (** [hashmap::hash_key] *) -let hash_key_fwd (k : usize) : result usize = Return k +let hash_key_fwd (k : usize) : result usize = + Return k (** [hashmap::HashMap::{0}::allocate_slots] *) let rec hash_map_allocate_slots_loop_fwd @@ -17,10 +18,10 @@ let rec hash_map_allocate_slots_loop_fwd (decreases (hash_map_allocate_slots_loop_decreases t slots n)) = if n > 0 - then begin + then let* slots0 = vec_push_back (list_t t) slots ListNil in let* n0 = usize_sub n 1 in - hash_map_allocate_slots_loop_fwd t slots0 n0 end + hash_map_allocate_slots_loop_fwd t slots0 n0 else Return slots (** [hashmap::HashMap::{0}::allocate_slots] *) @@ -52,10 +53,10 @@ let rec hash_map_clear_loop_fwd_back = let i0 = vec_len (list_t t) slots in if i < i0 - then begin + then let* i1 = usize_add i 1 in let* slots0 = vec_index_mut_back (list_t t) slots i ListNil in - hash_map_clear_loop_fwd_back t slots0 i1 end + hash_map_clear_loop_fwd_back t slots0 i1 else Return slots (** [hashmap::HashMap::{0}::clear] *) @@ -98,9 +99,9 @@ let rec hash_map_insert_in_list_loop_back | ListCons ckey cvalue tl -> if ckey = key then Return (ListCons ckey value tl) - else begin + else let* tl0 = hash_map_insert_in_list_loop_back t key value tl in - Return (ListCons ckey cvalue tl0) end + Return (ListCons ckey cvalue tl0) | ListNil -> let l = ListNil in Return (ListCons key value l) end @@ -120,17 +121,17 @@ let hash_map_insert_no_resize_fwd_back let* l = vec_index_mut_fwd (list_t t) self.hash_map_slots hash_mod in let* inserted = hash_map_insert_in_list_fwd t key value l in if inserted - then begin + then let* i0 = usize_add self.hash_map_num_entries 1 in let* l0 = hash_map_insert_in_list_back t key value l in let* v = vec_index_mut_back (list_t t) self.hash_map_slots hash_mod l0 in Return (Mkhash_map_t i0 self.hash_map_max_load_factor - self.hash_map_max_load v) end - else begin + self.hash_map_max_load v) + else let* l0 = hash_map_insert_in_list_back t key value l in let* v = vec_index_mut_back (list_t t) self.hash_map_slots hash_mod l0 in Return (Mkhash_map_t self.hash_map_num_entries - self.hash_map_max_load_factor self.hash_map_max_load v) end + self.hash_map_max_load_factor self.hash_map_max_load v) (** [core::num::u32::{9}::MAX] *) let core_num_u32_max_body : result u32 = Return 4294967295 @@ -162,14 +163,14 @@ let rec hash_map_move_elements_loop_fwd_back = let i0 = vec_len (list_t t) slots in if i < i0 - then begin + then let* l = vec_index_mut_fwd (list_t t) slots i in let ls = mem_replace_fwd (list_t t) l ListNil in let* ntable0 = hash_map_move_elements_from_list_fwd_back t ntable ls in let* i1 = usize_add i 1 in let l0 = mem_replace_back (list_t t) l ListNil in let* slots0 = vec_index_mut_back (list_t t) slots i l0 in - hash_map_move_elements_loop_fwd_back t ntable0 slots0 i1 end + hash_map_move_elements_loop_fwd_back t ntable0 slots0 i1 else Return (ntable, slots) (** [hashmap::HashMap::{0}::move_elements] *) @@ -188,13 +189,13 @@ let hash_map_try_resize_fwd_back let (i, i0) = self.hash_map_max_load_factor in let* i1 = usize_div n1 i in if capacity <= i1 - then begin + then let* i2 = usize_mul capacity 2 in let* ntable = hash_map_new_with_capacity_fwd t i2 i i0 in let* (ntable0, _) = hash_map_move_elements_fwd_back t ntable self.hash_map_slots 0 in Return (Mkhash_map_t self.hash_map_num_entries (i, i0) - ntable0.hash_map_max_load ntable0.hash_map_slots) end + ntable0.hash_map_max_load ntable0.hash_map_slots) else Return (Mkhash_map_t self.hash_map_num_entries (i, i0) self.hash_map_max_load self.hash_map_slots) @@ -293,9 +294,9 @@ let rec hash_map_get_mut_in_list_loop_back | ListCons ckey cvalue tl -> if ckey = key then Return (ListCons ckey ret tl) - else begin + else let* tl0 = hash_map_get_mut_in_list_loop_back t tl key ret in - Return (ListCons ckey cvalue tl0) end + Return (ListCons ckey cvalue tl0) | ListNil -> Fail Failure end @@ -366,9 +367,9 @@ let rec hash_map_remove_from_list_loop_back | ListCons i cvalue tl0 -> Return tl0 | ListNil -> Fail Failure end - else begin + else let* tl0 = hash_map_remove_from_list_loop_back t key tl in - Return (ListCons ckey x tl0) end + Return (ListCons ckey x tl0) | ListNil -> Return ListNil end @@ -423,31 +424,31 @@ let test1_fwd : result unit = let* i = hash_map_get_fwd u64 hm3 128 in if not (i = 18) then Fail Failure - else begin + else let* hm4 = hash_map_get_mut_back u64 hm3 1024 56 in let* i0 = hash_map_get_fwd u64 hm4 1024 in if not (i0 = 56) then Fail Failure - else begin + else let* x = hash_map_remove_fwd u64 hm4 1024 in begin match x with | None -> Fail Failure | Some x0 -> if not (x0 = 56) then Fail Failure - else begin + else let* hm5 = hash_map_remove_back u64 hm4 1024 in let* i1 = hash_map_get_fwd u64 hm5 0 in if not (i1 = 42) then Fail Failure - else begin + else let* i2 = hash_map_get_fwd u64 hm5 128 in if not (i2 = 18) then Fail Failure - else begin + else let* i3 = hash_map_get_fwd u64 hm5 1056 in - if not (i3 = 256) then Fail Failure else Return () end end end - end end end + if not (i3 = 256) then Fail Failure else Return () + end (** Unit test for [hashmap::test1] *) let _ = assert_norm (test1_fwd = Return ()) diff --git a/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst b/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst index 51021daf..7e1a7636 100644 --- a/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst +++ b/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst @@ -9,7 +9,8 @@ include HashmapMain.Clauses #set-options "--z3rlimit 50 --fuel 1 --ifuel 1" (** [hashmap_main::hashmap::hash_key] *) -let hashmap_hash_key_fwd (k : usize) : result usize = Return k +let hashmap_hash_key_fwd (k : usize) : result usize = + Return k (** [hashmap_main::hashmap::HashMap::{0}::allocate_slots] *) let rec hashmap_hash_map_allocate_slots_loop_fwd @@ -18,10 +19,10 @@ let rec hashmap_hash_map_allocate_slots_loop_fwd (decreases (hashmap_hash_map_allocate_slots_loop_decreases t slots n)) = if n > 0 - then begin + then let* slots0 = vec_push_back (hashmap_list_t t) slots HashmapListNil in let* n0 = usize_sub n 1 in - hashmap_hash_map_allocate_slots_loop_fwd t slots0 n0 end + hashmap_hash_map_allocate_slots_loop_fwd t slots0 n0 else Return slots (** [hashmap_main::hashmap::HashMap::{0}::allocate_slots] *) @@ -56,11 +57,11 @@ let rec hashmap_hash_map_clear_loop_fwd_back = let i0 = vec_len (hashmap_list_t t) slots in if i < i0 - then begin + then let* i1 = usize_add i 1 in let* slots0 = vec_index_mut_back (hashmap_list_t t) slots i HashmapListNil in - hashmap_hash_map_clear_loop_fwd_back t slots0 i1 end + hashmap_hash_map_clear_loop_fwd_back t slots0 i1 else Return slots (** [hashmap_main::hashmap::HashMap::{0}::clear] *) @@ -105,9 +106,9 @@ let rec hashmap_hash_map_insert_in_list_loop_back | HashmapListCons ckey cvalue tl -> if ckey = key then Return (HashmapListCons ckey value tl) - else begin + else let* tl0 = hashmap_hash_map_insert_in_list_loop_back t key value tl in - Return (HashmapListCons ckey cvalue tl0) end + Return (HashmapListCons ckey cvalue tl0) | HashmapListNil -> let l = HashmapListNil in Return (HashmapListCons key value l) end @@ -132,22 +133,21 @@ let hashmap_hash_map_insert_no_resize_fwd_back in let* inserted = hashmap_hash_map_insert_in_list_fwd t key value l in if inserted - then begin + then let* i0 = usize_add self.hashmap_hash_map_num_entries 1 in let* l0 = hashmap_hash_map_insert_in_list_back t key value l in let* v = vec_index_mut_back (hashmap_list_t t) self.hashmap_hash_map_slots hash_mod l0 in Return (Mkhashmap_hash_map_t i0 self.hashmap_hash_map_max_load_factor - self.hashmap_hash_map_max_load v) end - else begin + self.hashmap_hash_map_max_load v) + else let* l0 = hashmap_hash_map_insert_in_list_back t key value l in let* v = vec_index_mut_back (hashmap_list_t t) self.hashmap_hash_map_slots hash_mod l0 in Return (Mkhashmap_hash_map_t self.hashmap_hash_map_num_entries self.hashmap_hash_map_max_load_factor self.hashmap_hash_map_max_load v) - end (** [core::num::u32::{9}::MAX] *) let core_num_u32_max_body : result u32 = Return 4294967295 @@ -183,7 +183,7 @@ let rec hashmap_hash_map_move_elements_loop_fwd_back = let i0 = vec_len (hashmap_list_t t) slots in if i < i0 - then begin + then let* l = vec_index_mut_fwd (hashmap_list_t t) slots i in let ls = mem_replace_fwd (hashmap_list_t t) l HashmapListNil in let* ntable0 = @@ -191,7 +191,7 @@ let rec hashmap_hash_map_move_elements_loop_fwd_back let* i1 = usize_add i 1 in let l0 = mem_replace_back (hashmap_list_t t) l HashmapListNil in let* slots0 = vec_index_mut_back (hashmap_list_t t) slots i l0 in - hashmap_hash_map_move_elements_loop_fwd_back t ntable0 slots0 i1 end + hashmap_hash_map_move_elements_loop_fwd_back t ntable0 slots0 i1 else Return (ntable, slots) (** [hashmap_main::hashmap::HashMap::{0}::move_elements] *) @@ -211,14 +211,14 @@ let hashmap_hash_map_try_resize_fwd_back let (i, i0) = self.hashmap_hash_map_max_load_factor in let* i1 = usize_div n1 i in if capacity <= i1 - then begin + then let* i2 = usize_mul capacity 2 in let* ntable = hashmap_hash_map_new_with_capacity_fwd t i2 i i0 in let* (ntable0, _) = hashmap_hash_map_move_elements_fwd_back t ntable self.hashmap_hash_map_slots 0 in Return (Mkhashmap_hash_map_t self.hashmap_hash_map_num_entries (i, i0) - ntable0.hashmap_hash_map_max_load ntable0.hashmap_hash_map_slots) end + ntable0.hashmap_hash_map_max_load ntable0.hashmap_hash_map_slots) else Return (Mkhashmap_hash_map_t self.hashmap_hash_map_num_entries (i, i0) self.hashmap_hash_map_max_load self.hashmap_hash_map_slots) @@ -321,9 +321,9 @@ let rec hashmap_hash_map_get_mut_in_list_loop_back | HashmapListCons ckey cvalue tl -> if ckey = key then Return (HashmapListCons ckey ret tl) - else begin + else let* tl0 = hashmap_hash_map_get_mut_in_list_loop_back t tl key ret in - Return (HashmapListCons ckey cvalue tl0) end + Return (HashmapListCons ckey cvalue tl0) | HashmapListNil -> Fail Failure end @@ -406,9 +406,9 @@ let rec hashmap_hash_map_remove_from_list_loop_back | HashmapListCons i cvalue tl0 -> Return tl0 | HashmapListNil -> Fail Failure end - else begin + else let* tl0 = hashmap_hash_map_remove_from_list_loop_back t key tl in - Return (HashmapListCons ckey x tl0) end + Return (HashmapListCons ckey x tl0) | HashmapListNil -> Return HashmapListNil end @@ -475,31 +475,31 @@ let hashmap_test1_fwd : result unit = let* i = hashmap_hash_map_get_fwd u64 hm3 128 in if not (i = 18) then Fail Failure - else begin + else let* hm4 = hashmap_hash_map_get_mut_back u64 hm3 1024 56 in let* i0 = hashmap_hash_map_get_fwd u64 hm4 1024 in if not (i0 = 56) then Fail Failure - else begin + else let* x = hashmap_hash_map_remove_fwd u64 hm4 1024 in begin match x with | None -> Fail Failure | Some x0 -> if not (x0 = 56) then Fail Failure - else begin + else let* hm5 = hashmap_hash_map_remove_back u64 hm4 1024 in let* i1 = hashmap_hash_map_get_fwd u64 hm5 0 in if not (i1 = 42) then Fail Failure - else begin + else let* i2 = hashmap_hash_map_get_fwd u64 hm5 128 in if not (i2 = 18) then Fail Failure - else begin + else let* i3 = hashmap_hash_map_get_fwd u64 hm5 1056 in - if not (i3 = 256) then Fail Failure else Return () end end end - end end end + if not (i3 = 256) then Fail Failure else Return () + end (** Unit test for [hashmap_main::hashmap::test1] *) let _ = assert_norm (hashmap_test1_fwd = Return ()) @@ -513,7 +513,8 @@ let insert_on_disk_fwd Return (st1, ()) (** [hashmap_main::main] *) -let main_fwd : result unit = Return () +let main_fwd : result unit = + Return () (** Unit test for [hashmap_main::main] *) let _ = assert_norm (main_fwd = Return ()) diff --git a/tests/fstar/misc/Constants.fst b/tests/fstar/misc/Constants.fst index 1a2f4133..bf13ad43 100644 --- a/tests/fstar/misc/Constants.fst +++ b/tests/fstar/misc/Constants.fst @@ -22,14 +22,16 @@ let x2_body : result u32 = Return 3 let x2_c : u32 = eval_global x2_body (** [constants::incr] *) -let incr_fwd (n : u32) : result u32 = u32_add n 1 +let incr_fwd (n : u32) : result u32 = + u32_add n 1 (** [constants::X3] *) let x3_body : result u32 = incr_fwd 32 let x3_c : u32 = eval_global x3_body (** [constants::mk_pair0] *) -let mk_pair0_fwd (x : u32) (y : u32) : result (u32 & u32) = Return (x, y) +let mk_pair0_fwd (x : u32) (y : u32) : result (u32 & u32) = + Return (x, y) (** [constants::Pair] *) type pair_t (t1 t2 : Type0) = { pair_x : t1; pair_y : t2; } @@ -66,7 +68,8 @@ let y_body : result (wrap_t i32) = wrap_new_fwd i32 2 let y_c : wrap_t i32 = eval_global y_body (** [constants::unwrap_y] *) -let unwrap_y_fwd : result i32 = Return y_c.wrap_val +let unwrap_y_fwd : result i32 = + Return y_c.wrap_val (** [constants::YVAL] *) let yval_body : result i32 = unwrap_y_fwd @@ -77,10 +80,12 @@ let get_z1_z1_body : result i32 = Return 3 let get_z1_z1_c : i32 = eval_global get_z1_z1_body (** [constants::get_z1] *) -let get_z1_fwd : result i32 = Return get_z1_z1_c +let get_z1_fwd : result i32 = + Return get_z1_z1_c (** [constants::add] *) -let add_fwd (a : i32) (b : i32) : result i32 = i32_add a b +let add_fwd (a : i32) (b : i32) : result i32 = + i32_add a b (** [constants::Q1] *) let q1_body : result i32 = Return 5 diff --git a/tests/fstar/misc/Loops.Funs.fst b/tests/fstar/misc/Loops.Funs.fst index 0d3c39f7..7fe175e5 100644 --- a/tests/fstar/misc/Loops.Funs.fst +++ b/tests/fstar/misc/Loops.Funs.fst @@ -13,13 +13,12 @@ let rec sum_loop_fwd Tot (result u32) (decreases (sum_loop_decreases max i s)) = if i < max - then begin - let* s0 = u32_add s i in let* i0 = u32_add i 1 in sum_loop_fwd max i0 s0 - end + then let* s0 = u32_add s i in let* i0 = u32_add i 1 in sum_loop_fwd max i0 s0 else u32_mul s 2 (** [loops::sum] *) -let sum_fwd (max : u32) : result u32 = sum_loop_fwd max 0 0 +let sum_fwd (max : u32) : result u32 = + sum_loop_fwd max 0 0 (** [loops::sum_with_mut_borrows] *) let rec sum_with_mut_borrows_loop_fwd @@ -27,10 +26,10 @@ let rec sum_with_mut_borrows_loop_fwd Tot (result u32) (decreases (sum_with_mut_borrows_loop_decreases max mi ms)) = if mi < max - then begin + then let* ms0 = u32_add ms mi in let* mi0 = u32_add mi 1 in - sum_with_mut_borrows_loop_fwd max mi0 ms0 end + sum_with_mut_borrows_loop_fwd max mi0 ms0 else u32_mul ms 2 (** [loops::sum_with_mut_borrows] *) @@ -43,10 +42,10 @@ let rec sum_with_shared_borrows_loop_fwd Tot (result u32) (decreases (sum_with_shared_borrows_loop_decreases max i s)) = if i < max - then begin + then let* i0 = u32_add i 1 in let* s0 = u32_add s i0 in - sum_with_shared_borrows_loop_fwd max i0 s0 end + sum_with_shared_borrows_loop_fwd max i0 s0 else u32_mul s 2 (** [loops::sum_with_shared_borrows] *) @@ -60,14 +59,15 @@ let rec clear_loop_fwd_back = let i0 = vec_len u32 v in if i < i0 - then begin + then let* i1 = usize_add i 1 in let* v0 = vec_index_mut_back u32 v i 0 in - clear_loop_fwd_back v0 i1 end + clear_loop_fwd_back v0 i1 else Return v (** [loops::clear] *) -let clear_fwd_back (v : vec u32) : result (vec u32) = clear_loop_fwd_back v 0 +let clear_fwd_back (v : vec u32) : result (vec u32) = + clear_loop_fwd_back v 0 (** [loops::list_mem] *) let rec list_mem_loop_fwd @@ -92,7 +92,7 @@ let rec list_nth_mut_loop_loop_fwd | ListCons x tl -> if i = 0 then Return x - else begin let* i0 = u32_sub i 1 in list_nth_mut_loop_loop_fwd t tl i0 end + else let* i0 = u32_sub i 1 in list_nth_mut_loop_loop_fwd t tl i0 | ListNil -> Fail Failure end @@ -109,10 +109,10 @@ let rec list_nth_mut_loop_loop_back | ListCons x tl -> if i = 0 then Return (ListCons ret tl) - else begin + else let* i0 = u32_sub i 1 in let* tl0 = list_nth_mut_loop_loop_back t tl i0 ret in - Return (ListCons x tl0) end + Return (ListCons x tl0) | ListNil -> Fail Failure end @@ -130,8 +130,7 @@ let rec list_nth_shared_loop_loop_fwd | ListCons x tl -> if i = 0 then Return x - else begin let* i0 = u32_sub i 1 in list_nth_shared_loop_loop_fwd t tl i0 - end + else let* i0 = u32_sub i 1 in list_nth_shared_loop_loop_fwd t tl i0 | ListNil -> Fail Failure end @@ -163,8 +162,7 @@ let rec get_elem_mut_loop_back | ListCons y tl -> if y = x then Return (ListCons ret tl) - else begin - let* tl0 = get_elem_mut_loop_back x tl ret in Return (ListCons y tl0) end + else let* tl0 = get_elem_mut_loop_back x tl ret in Return (ListCons y tl0) | ListNil -> Fail Failure end @@ -193,7 +191,8 @@ let get_elem_shared_fwd let* l = vec_index_fwd (list_t usize) slots 0 in get_elem_shared_loop_fwd x l (** [loops::id_mut] *) -let id_mut_fwd (t : Type0) (ls : list_t t) : result (list_t t) = Return ls +let id_mut_fwd (t : Type0) (ls : list_t t) : result (list_t t) = + Return ls (** [loops::id_mut] *) let id_mut_back @@ -201,7 +200,8 @@ let id_mut_back Return ret (** [loops::id_shared] *) -let id_shared_fwd (t : Type0) (ls : list_t t) : result (list_t t) = Return ls +let id_shared_fwd (t : Type0) (ls : list_t t) : result (list_t t) = + Return ls (** [loops::list_nth_mut_loop_with_id] *) let rec list_nth_mut_loop_with_id_loop_fwd @@ -212,8 +212,7 @@ let rec list_nth_mut_loop_with_id_loop_fwd | ListCons x tl -> if i = 0 then Return x - else begin - let* i0 = u32_sub i 1 in list_nth_mut_loop_with_id_loop_fwd t i0 tl end + else let* i0 = u32_sub i 1 in list_nth_mut_loop_with_id_loop_fwd t i0 tl | ListNil -> Fail Failure end @@ -232,10 +231,10 @@ let rec list_nth_mut_loop_with_id_loop_back | ListCons x tl -> if i = 0 then Return (ListCons ret tl) - else begin + else let* i0 = u32_sub i 1 in let* tl0 = list_nth_mut_loop_with_id_loop_back t i0 tl ret in - Return (ListCons x tl0) end + Return (ListCons x tl0) | ListNil -> Fail Failure end @@ -256,9 +255,7 @@ let rec list_nth_shared_loop_with_id_loop_fwd | ListCons x tl -> if i = 0 then Return x - else begin - let* i0 = u32_sub i 1 in list_nth_shared_loop_with_id_loop_fwd t i0 tl - end + else let* i0 = u32_sub i 1 in list_nth_shared_loop_with_id_loop_fwd t i0 tl | ListNil -> Fail Failure end @@ -280,9 +277,8 @@ let rec list_nth_mut_loop_pair_loop_fwd | ListCons x1 tl1 -> if i = 0 then Return (x0, x1) - else begin + else let* i0 = u32_sub i 1 in list_nth_mut_loop_pair_loop_fwd t tl0 tl1 i0 - end | ListNil -> Fail Failure end | ListNil -> Fail Failure @@ -305,10 +301,10 @@ let rec list_nth_mut_loop_pair_loop_back'a | ListCons x1 tl1 -> if i = 0 then Return (ListCons ret tl0) - else begin + else let* i0 = u32_sub i 1 in let* tl00 = list_nth_mut_loop_pair_loop_back'a t tl0 tl1 i0 ret in - Return (ListCons x0 tl00) end + Return (ListCons x0 tl00) | ListNil -> Fail Failure end | ListNil -> Fail Failure @@ -333,10 +329,10 @@ let rec list_nth_mut_loop_pair_loop_back'b | ListCons x1 tl1 -> if i = 0 then Return (ListCons ret tl1) - else begin + else let* i0 = u32_sub i 1 in let* tl10 = list_nth_mut_loop_pair_loop_back'b t tl0 tl1 i0 ret in - Return (ListCons x1 tl10) end + Return (ListCons x1 tl10) | ListNil -> Fail Failure end | ListNil -> Fail Failure @@ -361,9 +357,9 @@ let rec list_nth_shared_loop_pair_loop_fwd | ListCons x1 tl1 -> if i = 0 then Return (x0, x1) - else begin + else let* i0 = u32_sub i 1 in - list_nth_shared_loop_pair_loop_fwd t tl0 tl1 i0 end + list_nth_shared_loop_pair_loop_fwd t tl0 tl1 i0 | ListNil -> Fail Failure end | ListNil -> Fail Failure @@ -386,9 +382,9 @@ let rec list_nth_mut_loop_pair_merge_loop_fwd | ListCons x1 tl1 -> if i = 0 then Return (x0, x1) - else begin + else let* i0 = u32_sub i 1 in - list_nth_mut_loop_pair_merge_loop_fwd t tl0 tl1 i0 end + list_nth_mut_loop_pair_merge_loop_fwd t tl0 tl1 i0 | ListNil -> Fail Failure end | ListNil -> Fail Failure @@ -411,11 +407,11 @@ let rec list_nth_mut_loop_pair_merge_loop_back | ListCons x1 tl1 -> if i = 0 then let (x, x2) = ret in Return (ListCons x tl0, ListCons x2 tl1) - else begin + else let* i0 = u32_sub i 1 in let* (tl00, tl10) = list_nth_mut_loop_pair_merge_loop_back t tl0 tl1 i0 ret in - Return (ListCons x0 tl00, ListCons x1 tl10) end + Return (ListCons x0 tl00, ListCons x1 tl10) | ListNil -> Fail Failure end | ListNil -> Fail Failure @@ -440,9 +436,9 @@ let rec list_nth_shared_loop_pair_merge_loop_fwd | ListCons x1 tl1 -> if i = 0 then Return (x0, x1) - else begin + else let* i0 = u32_sub i 1 in - list_nth_shared_loop_pair_merge_loop_fwd t tl0 tl1 i0 end + list_nth_shared_loop_pair_merge_loop_fwd t tl0 tl1 i0 | ListNil -> Fail Failure end | ListNil -> Fail Failure @@ -465,9 +461,9 @@ let rec list_nth_mut_shared_loop_pair_loop_fwd | ListCons x1 tl1 -> if i = 0 then Return (x0, x1) - else begin + else let* i0 = u32_sub i 1 in - list_nth_mut_shared_loop_pair_loop_fwd t tl0 tl1 i0 end + list_nth_mut_shared_loop_pair_loop_fwd t tl0 tl1 i0 | ListNil -> Fail Failure end | ListNil -> Fail Failure @@ -490,10 +486,10 @@ let rec list_nth_mut_shared_loop_pair_loop_back | ListCons x1 tl1 -> if i = 0 then Return (ListCons ret tl0) - else begin + else let* i0 = u32_sub i 1 in let* tl00 = list_nth_mut_shared_loop_pair_loop_back t tl0 tl1 i0 ret in - Return (ListCons x0 tl00) end + Return (ListCons x0 tl00) | ListNil -> Fail Failure end | ListNil -> Fail Failure @@ -518,9 +514,9 @@ let rec list_nth_mut_shared_loop_pair_merge_loop_fwd | ListCons x1 tl1 -> if i = 0 then Return (x0, x1) - else begin + else let* i0 = u32_sub i 1 in - list_nth_mut_shared_loop_pair_merge_loop_fwd t tl0 tl1 i0 end + list_nth_mut_shared_loop_pair_merge_loop_fwd t tl0 tl1 i0 | ListNil -> Fail Failure end | ListNil -> Fail Failure @@ -543,11 +539,11 @@ let rec list_nth_mut_shared_loop_pair_merge_loop_back | ListCons x1 tl1 -> if i = 0 then Return (ListCons ret tl0) - else begin + else let* i0 = u32_sub i 1 in let* tl00 = list_nth_mut_shared_loop_pair_merge_loop_back t tl0 tl1 i0 ret in - Return (ListCons x0 tl00) end + Return (ListCons x0 tl00) | ListNil -> Fail Failure end | ListNil -> Fail Failure @@ -572,9 +568,9 @@ let rec list_nth_shared_mut_loop_pair_loop_fwd | ListCons x1 tl1 -> if i = 0 then Return (x0, x1) - else begin + else let* i0 = u32_sub i 1 in - list_nth_shared_mut_loop_pair_loop_fwd t tl0 tl1 i0 end + list_nth_shared_mut_loop_pair_loop_fwd t tl0 tl1 i0 | ListNil -> Fail Failure end | ListNil -> Fail Failure @@ -597,10 +593,10 @@ let rec list_nth_shared_mut_loop_pair_loop_back | ListCons x1 tl1 -> if i = 0 then Return (ListCons ret tl1) - else begin + else let* i0 = u32_sub i 1 in let* tl10 = list_nth_shared_mut_loop_pair_loop_back t tl0 tl1 i0 ret in - Return (ListCons x1 tl10) end + Return (ListCons x1 tl10) | ListNil -> Fail Failure end | ListNil -> Fail Failure @@ -625,9 +621,9 @@ let rec list_nth_shared_mut_loop_pair_merge_loop_fwd | ListCons x1 tl1 -> if i = 0 then Return (x0, x1) - else begin + else let* i0 = u32_sub i 1 in - list_nth_shared_mut_loop_pair_merge_loop_fwd t tl0 tl1 i0 end + list_nth_shared_mut_loop_pair_merge_loop_fwd t tl0 tl1 i0 | ListNil -> Fail Failure end | ListNil -> Fail Failure @@ -650,11 +646,11 @@ let rec list_nth_shared_mut_loop_pair_merge_loop_back | ListCons x1 tl1 -> if i = 0 then Return (ListCons ret tl1) - else begin + else let* i0 = u32_sub i 1 in let* tl10 = list_nth_shared_mut_loop_pair_merge_loop_back t tl0 tl1 i0 ret in - Return (ListCons x1 tl10) end + Return (ListCons x1 tl10) | ListNil -> Fail Failure end | ListNil -> Fail Failure diff --git a/tests/fstar/misc/NoNestedBorrows.fst b/tests/fstar/misc/NoNestedBorrows.fst index ce1f544c..1e186c79 100644 --- a/tests/fstar/misc/NoNestedBorrows.fst +++ b/tests/fstar/misc/NoNestedBorrows.fst @@ -31,28 +31,36 @@ type sum_t (t1 t2 : Type0) = | SumRight : t2 -> sum_t t1 t2 (** [no_nested_borrows::neg_test] *) -let neg_test_fwd (x : i32) : result i32 = i32_neg x +let neg_test_fwd (x : i32) : result i32 = + i32_neg x (** [no_nested_borrows::add_test] *) -let add_test_fwd (x : u32) (y : u32) : result u32 = u32_add x y +let add_test_fwd (x : u32) (y : u32) : result u32 = + u32_add x y (** [no_nested_borrows::subs_test] *) -let subs_test_fwd (x : u32) (y : u32) : result u32 = u32_sub x y +let subs_test_fwd (x : u32) (y : u32) : result u32 = + u32_sub x y (** [no_nested_borrows::div_test] *) -let div_test_fwd (x : u32) (y : u32) : result u32 = u32_div x y +let div_test_fwd (x : u32) (y : u32) : result u32 = + u32_div x y (** [no_nested_borrows::div_test1] *) -let div_test1_fwd (x : u32) : result u32 = u32_div x 2 +let div_test1_fwd (x : u32) : result u32 = + u32_div x 2 (** [no_nested_borrows::rem_test] *) -let rem_test_fwd (x : u32) (y : u32) : result u32 = u32_rem x y +let rem_test_fwd (x : u32) (y : u32) : result u32 = + u32_rem x y (** [no_nested_borrows::cast_test] *) -let cast_test_fwd (x : u32) : result i32 = scalar_cast U32 I32 x +let cast_test_fwd (x : u32) : result i32 = + scalar_cast U32 I32 x (** [no_nested_borrows::test2] *) -let test2_fwd : result unit = let* _ = u32_add 23 44 in Return () +let test2_fwd : result unit = + let* _ = u32_add 23 44 in Return () (** Unit test for [no_nested_borrows::test2] *) let _ = assert_norm (test2_fwd = Return ()) @@ -101,7 +109,8 @@ let refs_test2_fwd : result unit = let _ = assert_norm (refs_test2_fwd = Return ()) (** [no_nested_borrows::test_list1] *) -let test_list1_fwd : result unit = Return () +let test_list1_fwd : result unit = + Return () (** Unit test for [no_nested_borrows::test_list1] *) let _ = assert_norm (test_list1_fwd = Return ()) @@ -114,7 +123,8 @@ let test_box1_fwd : result unit = let _ = assert_norm (test_box1_fwd = Return ()) (** [no_nested_borrows::copy_int] *) -let copy_int_fwd (x : i32) : result i32 = Return x +let copy_int_fwd (x : i32) : result i32 = + Return x (** [no_nested_borrows::test_unreachable] *) let test_unreachable_fwd (b : bool) : result unit = @@ -179,17 +189,18 @@ let choose_test_fwd : result unit = let* z0 = i32_add z 1 in if not (z0 = 1) then Fail Failure - else begin + else let* (x, y) = choose_back i32 true 0 0 z0 in if not (x = 1) then Fail Failure - else if not (y = 0) then Fail Failure else Return () end + else if not (y = 0) then Fail Failure else Return () (** Unit test for [no_nested_borrows::choose_test] *) let _ = assert_norm (choose_test_fwd = Return ()) (** [no_nested_borrows::test_char] *) -let test_char_fwd : result char = Return 'a' +let test_char_fwd : result char = + Return 'a' (** [no_nested_borrows::NodeElem] *) type node_elem_t (t : Type0) = @@ -214,7 +225,7 @@ let rec list_nth_shared_fwd (t : Type0) (l : list_t t) (i : u32) : result t = | ListCons x tl -> if i = 0 then Return x - else begin let* i0 = u32_sub i 1 in list_nth_shared_fwd t tl i0 end + else let* i0 = u32_sub i 1 in list_nth_shared_fwd t tl i0 | ListNil -> Fail Failure end @@ -224,7 +235,7 @@ let rec list_nth_mut_fwd (t : Type0) (l : list_t t) (i : u32) : result t = | ListCons x tl -> if i = 0 then Return x - else begin let* i0 = u32_sub i 1 in list_nth_mut_fwd t tl i0 end + else let* i0 = u32_sub i 1 in list_nth_mut_fwd t tl i0 | ListNil -> Fail Failure end @@ -235,10 +246,10 @@ let rec list_nth_mut_back | ListCons x tl -> if i = 0 then Return (ListCons ret tl) - else begin + else let* i0 = u32_sub i 1 in let* tl0 = list_nth_mut_back t tl i0 ret in - Return (ListCons x tl0) end + Return (ListCons x tl0) | ListNil -> Fail Failure end @@ -263,31 +274,30 @@ let test_list_functions_fwd : result unit = let* i = list_length_fwd i32 (ListCons 0 l1) in if not (i = 3) then Fail Failure - else begin + else let* i0 = list_nth_shared_fwd i32 (ListCons 0 l1) 0 in if not (i0 = 0) then Fail Failure - else begin + else let* i1 = list_nth_shared_fwd i32 (ListCons 0 l1) 1 in if not (i1 = 1) then Fail Failure - else begin + else let* i2 = list_nth_shared_fwd i32 (ListCons 0 l1) 2 in if not (i2 = 2) then Fail Failure - else begin + else let* ls = list_nth_mut_back i32 (ListCons 0 l1) 1 3 in let* i3 = list_nth_shared_fwd i32 ls 0 in if not (i3 = 0) then Fail Failure - else begin + else let* i4 = list_nth_shared_fwd i32 ls 1 in if not (i4 = 3) then Fail Failure - else begin + else let* i5 = list_nth_shared_fwd i32 ls 2 in - if not (i5 = 2) then Fail Failure else Return () end end end end - end end + if not (i5 = 2) then Fail Failure else Return () (** Unit test for [no_nested_borrows::test_list_functions] *) let _ = assert_norm (test_list_functions_fwd = Return ()) @@ -369,27 +379,28 @@ let test_constants_fwd : result unit = let (i, _) = swt.struct_with_tuple_p in if not (i = 1) then Fail Failure - else begin + else let* swt0 = new_tuple2_fwd in let (i0, _) = swt0.struct_with_tuple_p in if not (i0 = 1) then Fail Failure - else begin + else let* swt1 = new_tuple3_fwd in let (i1, _) = swt1.struct_with_tuple_p in if not (i1 = 1) then Fail Failure - else begin + else let* swp = new_pair1_fwd in if not (swp.struct_with_pair_p.pair_x = 1) then Fail Failure - else Return () end end end + else Return () (** Unit test for [no_nested_borrows::test_constants] *) let _ = assert_norm (test_constants_fwd = Return ()) (** [no_nested_borrows::test_weird_borrows1] *) -let test_weird_borrows1_fwd : result unit = Return () +let test_weird_borrows1_fwd : result unit = + Return () (** Unit test for [no_nested_borrows::test_weird_borrows1] *) let _ = assert_norm (test_weird_borrows1_fwd = Return ()) @@ -404,12 +415,14 @@ let test_shared_borrow_bool1_fwd (b : bool) : result u32 = if b then Return 0 else Return 1 (** [no_nested_borrows::test_shared_borrow_bool2] *) -let test_shared_borrow_bool2_fwd : result u32 = Return 0 +let test_shared_borrow_bool2_fwd : result u32 = + Return 0 (** [no_nested_borrows::test_shared_borrow_enum1] *) let test_shared_borrow_enum1_fwd (l : list_t u32) : result u32 = begin match l with | ListCons i l0 -> Return 1 | ListNil -> Return 0 end (** [no_nested_borrows::test_shared_borrow_enum2] *) -let test_shared_borrow_enum2_fwd : result u32 = Return 0 +let test_shared_borrow_enum2_fwd : result u32 = + Return 0 diff --git a/tests/fstar/misc/Paper.fst b/tests/fstar/misc/Paper.fst index 95f13f62..4ab31de3 100644 --- a/tests/fstar/misc/Paper.fst +++ b/tests/fstar/misc/Paper.fst @@ -6,7 +6,8 @@ open Primitives #set-options "--z3rlimit 50 --fuel 1 --ifuel 1" (** [paper::ref_incr] *) -let ref_incr_fwd_back (x : i32) : result i32 = i32_add x 1 +let ref_incr_fwd_back (x : i32) : result i32 = + i32_add x 1 (** [paper::test_incr] *) let test_incr_fwd : result unit = @@ -31,11 +32,11 @@ let test_choose_fwd : result unit = let* z0 = i32_add z 1 in if not (z0 = 1) then Fail Failure - else begin + else let* (x, y) = choose_back i32 true 0 0 z0 in if not (x = 1) then Fail Failure - else if not (y = 0) then Fail Failure else Return () end + else if not (y = 0) then Fail Failure else Return () (** Unit test for [paper::test_choose] *) let _ = assert_norm (test_choose_fwd = Return ()) @@ -51,7 +52,7 @@ let rec list_nth_mut_fwd (t : Type0) (l : list_t t) (i : u32) : result t = | ListCons x tl -> if i = 0 then Return x - else begin let* i0 = u32_sub i 1 in list_nth_mut_fwd t tl i0 end + else let* i0 = u32_sub i 1 in list_nth_mut_fwd t tl i0 | ListNil -> Fail Failure end @@ -62,10 +63,10 @@ let rec list_nth_mut_back | ListCons x tl -> if i = 0 then Return (ListCons ret tl) - else begin + else let* i0 = u32_sub i 1 in let* tl0 = list_nth_mut_back t tl i0 ret in - Return (ListCons x tl0) end + Return (ListCons x tl0) | ListNil -> Fail Failure end diff --git a/tests/fstar/misc/PoloniusList.fst b/tests/fstar/misc/PoloniusList.fst index db0dc0d5..e2144487 100644 --- a/tests/fstar/misc/PoloniusList.fst +++ b/tests/fstar/misc/PoloniusList.fst @@ -25,8 +25,7 @@ let rec get_list_at_x_back | ListCons hd tl -> if hd = x then Return ret - else begin - let* tl0 = get_list_at_x_back tl x ret in Return (ListCons hd tl0) end + else let* tl0 = get_list_at_x_back tl x ret in Return (ListCons hd tl0) | ListNil -> Return ret end diff --git a/tests/lean/hashmap/Hashmap/Funs.lean b/tests/lean/hashmap/Hashmap/Funs.lean index 1b03b7a2..78ed970a 100644 --- a/tests/lean/hashmap/Hashmap/Funs.lean +++ b/tests/lean/hashmap/Hashmap/Funs.lean @@ -5,7 +5,8 @@ import Hashmap.Types import Hashmap.Clauses.Clauses /- [hashmap::hash_key] -/ -def hash_key_fwd (k : USize) : result USize := result.ret k +def hash_key_fwd (k : USize) : result USize := + result.ret k /- [hashmap::HashMap::{0}::allocate_slots] -/ def hash_map_allocate_slots_loop_fwd @@ -119,7 +120,8 @@ def hash_map_insert_in_list_loop_back let tl0 <- hash_map_insert_in_list_loop_back T key value tl result.ret (list_t.ListCons ckey cvalue tl0) | list_t.ListNil => - let l := list_t.ListNil result.ret (list_t.ListCons key value l) + let l := list_t.ListNil + result.ret (list_t.ListCons key value l) termination_by hash_map_insert_in_list_loop_back key value ls => hash_map_insert_in_list_loop_terminates T key value ls diff --git a/tests/lean/hashmap_on_disk/HashmapMain/Funs.lean b/tests/lean/hashmap_on_disk/HashmapMain/Funs.lean index 2795ecfa..5b7d6f46 100644 --- a/tests/lean/hashmap_on_disk/HashmapMain/Funs.lean +++ b/tests/lean/hashmap_on_disk/HashmapMain/Funs.lean @@ -8,7 +8,8 @@ import HashmapMain.Clauses.Clauses section variable (opaque_defs: OpaqueDefs) /- [hashmap_main::hashmap::hash_key] -/ -def hashmap_hash_key_fwd (k : USize) : result USize := result.ret k +def hashmap_hash_key_fwd (k : USize) : result USize := + result.ret k /- [hashmap_main::hashmap::HashMap::{0}::allocate_slots] -/ def hashmap_hash_map_allocate_slots_loop_fwd @@ -638,7 +639,8 @@ def insert_on_disk_fwd result.ret (st1, ()) /- [hashmap_main::main] -/ -def main_fwd : result Unit := result.ret () +def main_fwd : result Unit := + result.ret () /- Unit test for [hashmap_main::main] -/ #assert (main_fwd = .ret ()) diff --git a/tests/lean/misc/constants/Constants.lean b/tests/lean/misc/constants/Constants.lean index a5cbe363..9ef9ca44 100644 --- a/tests/lean/misc/constants/Constants.lean +++ b/tests/lean/misc/constants/Constants.lean @@ -82,7 +82,8 @@ structure OpaqueDefs where def y_c : wrap_t Int32 := eval_global y_body (by simp) /- [constants::unwrap_y] -/ - def unwrap_y_fwd : result Int32 := result.ret y_c.wrap_val + def unwrap_y_fwd : result Int32 := + result.ret y_c.wrap_val /- [constants::YVAL] -/ def yval_body : result Int32 := unwrap_y_fwd @@ -94,10 +95,12 @@ structure OpaqueDefs where def get_z1_z1_c : Int32 := eval_global get_z1_z1_body (by simp) /- [constants::get_z1] -/ - def get_z1_fwd : result Int32 := result.ret get_z1_z1_c + def get_z1_fwd : result Int32 := + result.ret get_z1_z1_c /- [constants::add] -/ - def add_fwd (a : Int32) (b : Int32) : result Int32 := Int32.checked_add a b + def add_fwd (a : Int32) (b : Int32) : result Int32 := + Int32.checked_add a b /- [constants::Q1] -/ def q1_body : result Int32 := result.ret (Int32.ofNatCore 5 (by intlit)) diff --git a/tests/lean/misc/loops/Loops/Funs.lean b/tests/lean/misc/loops/Loops/Funs.lean index 33a3a881..8b7e8a1f 100644 --- a/tests/lean/misc/loops/Loops/Funs.lean +++ b/tests/lean/misc/loops/Loops/Funs.lean @@ -221,7 +221,8 @@ def get_elem_shared_fwd get_elem_shared_loop_fwd x l /- [loops::id_mut] -/ -def id_mut_fwd (T : Type) (ls : list_t T) : result (list_t T) := result.ret ls +def id_mut_fwd (T : Type) (ls : list_t T) : result (list_t T) := + result.ret ls /- [loops::id_mut] -/ def id_mut_back diff --git a/tests/lean/misc/no_nested_borrows/NoNestedBorrows.lean b/tests/lean/misc/no_nested_borrows/NoNestedBorrows.lean index d871392b..53093519 100644 --- a/tests/lean/misc/no_nested_borrows/NoNestedBorrows.lean +++ b/tests/lean/misc/no_nested_borrows/NoNestedBorrows.lean @@ -30,7 +30,8 @@ structure OpaqueDefs where | SumRight : T2 -> sum_t T1 T2 /- [no_nested_borrows::neg_test] -/ - def neg_test_fwd (x : Int32) : result Int32 := Int32.checked_neg x + def neg_test_fwd (x : Int32) : result Int32 := + Int32.checked_neg x /- [no_nested_borrows::add_test] -/ def add_test_fwd (x : UInt32) (y : UInt32) : result UInt32 := @@ -53,7 +54,8 @@ structure OpaqueDefs where UInt32.checked_rem x y /- [no_nested_borrows::cast_test] -/ - def cast_test_fwd (x : UInt32) : result Int32 := scalar_cast Int32 x + def cast_test_fwd (x : UInt32) : result Int32 := + scalar_cast Int32 x /- [no_nested_borrows::test2] -/ def test2_fwd : result Unit := @@ -128,7 +130,8 @@ structure OpaqueDefs where #assert (refs_test2_fwd = .ret ()) /- [no_nested_borrows::test_list1] -/ - def test_list1_fwd : result Unit := result.ret () + def test_list1_fwd : result Unit := + result.ret () /- Unit test for [no_nested_borrows::test_list1] -/ #assert (test_list1_fwd = .ret ()) @@ -145,7 +148,8 @@ structure OpaqueDefs where #assert (test_box1_fwd = .ret ()) /- [no_nested_borrows::copy_int] -/ - def copy_int_fwd (x : Int32) : result Int32 := result.ret x + def copy_int_fwd (x : Int32) : result Int32 := + result.ret x /- [no_nested_borrows::test_unreachable] -/ def test_unreachable_fwd (b : Bool) : result Unit := @@ -240,7 +244,8 @@ structure OpaqueDefs where #assert (choose_test_fwd = .ret ()) /- [no_nested_borrows::test_char] -/ - def test_char_fwd : result Char := result.ret 'a' + def test_char_fwd : result Char := + result.ret 'a' /- [no_nested_borrows::NodeElem] -/ mutual inductive node_elem_t (T : Type) := @@ -389,16 +394,19 @@ structure OpaqueDefs where /- [no_nested_borrows::id_mut_pair1] -/ def id_mut_pair1_back (T1 T2 : Type) (x : T1) (y : T2) (ret0 : (T1 × T2)) : result (T1 × T2) := - let (t, t0) := ret0 result.ret (t, t0) + let (t, t0) := ret0 + result.ret (t, t0) /- [no_nested_borrows::id_mut_pair2] -/ def id_mut_pair2_fwd (T1 T2 : Type) (p : (T1 × T2)) : result (T1 × T2) := - let (t, t0) := p result.ret (t, t0) + let (t, t0) := p + result.ret (t, t0) /- [no_nested_borrows::id_mut_pair2] -/ def id_mut_pair2_back (T1 T2 : Type) (p : (T1 × T2)) (ret0 : (T1 × T2)) : result (T1 × T2) := - let (t, t0) := ret0 result.ret (t, t0) + let (t, t0) := ret0 + result.ret (t, t0) /- [no_nested_borrows::id_mut_pair3] -/ def id_mut_pair3_fwd (T1 T2 : Type) (x : T1) (y : T2) : result (T1 × T2) := @@ -416,7 +424,8 @@ structure OpaqueDefs where /- [no_nested_borrows::id_mut_pair4] -/ def id_mut_pair4_fwd (T1 T2 : Type) (p : (T1 × T2)) : result (T1 × T2) := - let (t, t0) := p result.ret (t, t0) + let (t, t0) := p + result.ret (t, t0) /- [no_nested_borrows::id_mut_pair4] -/ def id_mut_pair4_back'a @@ -505,7 +514,8 @@ structure OpaqueDefs where #assert (test_constants_fwd = .ret ()) /- [no_nested_borrows::test_weird_borrows1] -/ - def test_weird_borrows1_fwd : result Unit := result.ret () + def test_weird_borrows1_fwd : result Unit := + result.ret () /- Unit test for [no_nested_borrows::test_weird_borrows1] -/ #assert (test_weird_borrows1_fwd = .ret ()) |