diff options
| author | Son Ho | 2022-11-15 15:23:16 +0100 |
|---|---|---|
| committer | Son HO | 2022-11-16 15:45:32 +0100 |
| commit | bd5706896dec0a1aef1accdf51f93af00c5dc6fe (patch) | |
| tree | 09dd5431d351c8ef894092ea25fd9d2af54d3d6e /tests/fstar/betree_back_stateful | |
| parent | dbb5d549176edd60440e689fd28c529944bc6e51 (diff) | |
Improve formatting
Diffstat (limited to 'tests/fstar/betree_back_stateful')
| -rw-r--r-- | tests/fstar/betree_back_stateful/BetreeMain.Funs.fst | 30 |
1 files changed, 16 insertions, 14 deletions
diff --git a/tests/fstar/betree_back_stateful/BetreeMain.Funs.fst b/tests/fstar/betree_back_stateful/BetreeMain.Funs.fst index 6a2b7c09..1560624b 100644 --- a/tests/fstar/betree_back_stateful/BetreeMain.Funs.fst +++ b/tests/fstar/betree_back_stateful/BetreeMain.Funs.fst @@ -1222,8 +1222,8 @@ let rec betree_node_apply_messages_fwd (node_id_cnt : betree_node_id_counter_t) (msgs : betree_list_t (u64 & betree_message_t)) (st : state) : Tot (result (state & unit)) - (decreases (betree_node_apply_messages_decreases self params node_id_cnt msgs - st)) + (decreases ( + betree_node_apply_messages_decreases self params node_id_cnt msgs st)) = begin match self with | BetreeNodeInternal node -> @@ -1318,8 +1318,8 @@ and betree_node_apply_messages_back'a (node_id_cnt : betree_node_id_counter_t) (msgs : betree_list_t (u64 & betree_message_t)) (st : state) (st0 : state) : Tot (result (state & (betree_node_t & betree_node_id_counter_t))) - (decreases (betree_node_apply_messages_decreases self params node_id_cnt msgs - st)) + (decreases ( + betree_node_apply_messages_decreases self params node_id_cnt msgs st)) = begin match self with | BetreeNodeInternal node -> @@ -1425,8 +1425,8 @@ and betree_node_apply_messages_back1 (node_id_cnt : betree_node_id_counter_t) (msgs : betree_list_t (u64 & betree_message_t)) (st : state) (st0 : state) : Tot (result (state & unit)) - (decreases (betree_node_apply_messages_decreases self params node_id_cnt msgs - st)) + (decreases ( + betree_node_apply_messages_decreases self params node_id_cnt msgs st)) = begin match self with | BetreeNodeInternal node -> @@ -1533,8 +1533,8 @@ and betree_internal_flush_fwd (node_id_cnt : betree_node_id_counter_t) (content : betree_list_t (u64 & betree_message_t)) (st : state) : Tot (result (state & (betree_list_t (u64 & betree_message_t)))) - (decreases (betree_internal_flush_decreases self params node_id_cnt content - st)) + (decreases ( + betree_internal_flush_decreases self params node_id_cnt content st)) = begin match betree_list_partition_at_pivot_fwd betree_message_t content @@ -1619,10 +1619,11 @@ and betree_internal_flush_fwd and betree_internal_flush_back'a (self : betree_internal_t) (params : betree_params_t) (node_id_cnt : betree_node_id_counter_t) - (content : betree_list_t (u64 & betree_message_t)) (st : state) (st0 : state) : + (content : betree_list_t (u64 & betree_message_t)) (st : state) (st0 : state) + : Tot (result (state & (betree_internal_t & betree_node_id_counter_t))) - (decreases (betree_internal_flush_decreases self params node_id_cnt content - st)) + (decreases ( + betree_internal_flush_decreases self params node_id_cnt content st)) = begin match betree_list_partition_at_pivot_fwd betree_message_t content @@ -1716,10 +1717,11 @@ and betree_internal_flush_back'a and betree_internal_flush_back1 (self : betree_internal_t) (params : betree_params_t) (node_id_cnt : betree_node_id_counter_t) - (content : betree_list_t (u64 & betree_message_t)) (st : state) (st0 : state) : + (content : betree_list_t (u64 & betree_message_t)) (st : state) (st0 : state) + : Tot (result (state & unit)) - (decreases (betree_internal_flush_decreases self params node_id_cnt content - st)) + (decreases ( + betree_internal_flush_decreases self params node_id_cnt content st)) = begin match betree_list_partition_at_pivot_fwd betree_message_t content |