From afed8a408f7a802a63687fb8c1201b358c37d32b Mon Sep 17 00:00:00 2001
From: Jonas Kastberg Hinrichsen <jihgfee@gmail.com>
Date: Fri, 5 Apr 2024 01:17:22 +0200
Subject: [PATCH] Clean up
---
.../examples/leader_election_del_alt.v | 93 +++++++------------
1 file changed, 36 insertions(+), 57 deletions(-)
diff --git a/multi_actris/examples/leader_election_del_alt.v b/multi_actris/examples/leader_election_del_alt.v
index 4495041..e7429c2 100644
--- a/multi_actris/examples/leader_election_del_alt.v
+++ b/multi_actris/examples/leader_election_del_alt.v
@@ -24,7 +24,6 @@ Definition process : val :=
Definition init : val :=
λ: "c" "idl" "id" "idr",
- (* Notice missing leader *)
send "c" "idl" #true;; send "c" "idl" "id";;
process "c" "idl" "id" "idr" #true.
@@ -53,11 +52,11 @@ Definition program : val :=
let: "c1" := get_chan "cs" #1 in
let: "c2" := get_chan "cs" #2 in
let: "c3" := get_chan "cs" #3 in
- Fork (let: "id_max" := process "c1" #0 #1 #2 #false in
+ Fork (let: "id_max" := process "c1" #0 #1 #2 #false in
forward "c1" "c1'" #0 #1 #2 "id_max");;
- Fork (let: "id_max" := process "c2" #1 #2 #3 #false in
+ Fork (let: "id_max" := process "c2" #1 #2 #3 #false in
forward "c2" "c1'" #1 #2 #3 "id_max");;
- Fork (let: "id_max" := process "c3" #2 #3 #0 #false in
+ Fork (let: "id_max" := process "c3" #2 #3 #0 #false in
forward "c3" "c1'" #2 #3 #0 "id_max");;
let: "id_max" := init "c0" #3 #0 #1 in
forward "c0" "c1'" #3 #0 #1 "id_max".
@@ -79,15 +78,18 @@ Section ring_leader_election_example.
then <(Send,il)> MSG #false ; <(Send, il)> MSG #i ; rec false
else if isp then rec isp
else <(Send,il)> MSG #true ; <(Send,il)> MSG #i ; rec true)%proto
- (<(Recv,ir) @ (i':nat)> MSG #i' {{ if bool_decide (i = i') then P else True%I }};
+ (<(Recv,ir) @ (i':nat)> MSG #i'
+ {{ if bool_decide (i = i') then P else True%I }};
if (bool_decide (i = i')) then p i
else <(Send,il)> MSG #false; <(Send,il)> MSG #i'; p i')%proto.
- Instance rle_prot_aux_contractive il i ir P p : Contractive (my_recv_prot il i ir P p).
+ Instance rle_prot_aux_contractive il i ir P p :
+ Contractive (my_recv_prot il i ir P p).
Proof. rewrite /my_recv_prot. solve_proto_contractive. Qed.
Definition rle_prot il i ir P p := fixpoint (my_recv_prot il i ir P p).
Instance rle_prot_unfold il i ir isp P p :
- ProtoUnfold (rle_prot il i ir P p isp) (my_recv_prot il i ir P p (rle_prot il i ir P p) isp).
+ ProtoUnfold (rle_prot il i ir P p isp)
+ (my_recv_prot il i ir P p (rle_prot il i ir P p) isp).
Proof. apply proto_unfold_eq, (fixpoint_unfold (my_recv_prot il i ir P p)). Qed.
Lemma rle_prot_unfold' il i ir isp P p :
(rle_prot il i ir P p isp) ≡
@@ -107,42 +109,27 @@ Section ring_leader_election_example.
iLöb as "IH" forall (Φ isp).
wp_lam. wp_recv (b) as "_".
destruct b.
- - wp_pures. wp_recv (i') as "_".
- wp_pures.
- case_bool_decide as Hlt.
+ - wp_recv (i') as "_".
+ wp_pures. case_bool_decide as Hlt.
{ case_bool_decide; [|lia].
- wp_pures. wp_send with "[//]".
- wp_send with "[//]". wp_pures.
- iApply ("IH" with "Hc HΦ"). }
+ wp_send with "[//]". wp_send with "[//]".
+ wp_smart_apply ("IH" with "Hc HΦ"). }
case_bool_decide as Hlt2.
- { case_bool_decide; [lia|].
- wp_pures. case_bool_decide; [|simplify_eq;lia].
- wp_send with "[//]".
- wp_send with "[//]". wp_pures.
- iApply ("IH" with "Hc HΦ"). }
+ { case_bool_decide; [lia|]. wp_pures. case_bool_decide; [|simplify_eq;lia].
+ wp_send with "[//]". wp_send with "[//]".
+ wp_smart_apply ("IH" with "Hc HΦ"). }
case_bool_decide; [lia|].
- wp_pures.
- case_bool_decide; [simplify_eq;lia|].
- wp_pures.
- destruct isp.
- { wp_pures. iApply ("IH" with "Hc HΦ"). }
- wp_pures.
- wp_send with "[//]".
- wp_send with "[//]".
- wp_pures. iApply ("IH" with "Hc HΦ").
- - wp_pures.
- wp_recv (id') as "HP". wp_pures.
+ wp_pures. case_bool_decide; [simplify_eq;lia|]. wp_pures.
+ destruct isp; [by wp_smart_apply ("IH" with "Hc HΦ")|].
+ wp_send with "[//]". wp_send with "[//]".
+ wp_smart_apply ("IH" with "Hc HΦ").
+ - wp_recv (id') as "HP". wp_pures.
case_bool_decide as Hlt.
{ case_bool_decide; [|simplify_eq;lia].
- wp_pures. subst. iApply "HΦ".
- iFrame.
- case_bool_decide; [|lia].
- done. }
+ wp_pures. subst. iApply "HΦ". iFrame. by case_bool_decide. }
case_bool_decide; [simplify_eq;lia|].
wp_send with "[//]". wp_send with "[//]". wp_pures. iApply "HΦ".
- iFrame.
- case_bool_decide; [simplify_eq;lia|].
- done.
+ iFrame. by case_bool_decide; [simplify_eq;lia|].
Qed.
Lemma init_spec c il i ir p P :
@@ -151,7 +138,7 @@ Section ring_leader_election_example.
{{{ i', RET #i'; c ↣ p i' ∗ if (bool_decide (i = i')) then P else True%I }}}.
Proof.
iIntros (Φ) "[Hc HP] HΦ". wp_lam. wp_send with "[//]". wp_send with "[HP//]".
- wp_pures. iApply (process_spec with "Hc HΦ").
+ wp_smart_apply (process_spec with "Hc HΦ").
Qed.
Definition forward_prot (P:iProp Σ) (il i ir i_max : nat) : iProto Σ :=
@@ -214,8 +201,7 @@ Section ring_leader_election_example.
Qed.
Definition prot_pool' : list (iProto Σ) :=
- [relay_recv_preprot;
- relay_send_preprot].
+ [relay_recv_preprot; relay_send_preprot].
Lemma prot_pool_consistent' : ⊢ iProto_consistent (prot_pool').
Proof.
@@ -229,7 +215,7 @@ Section ring_leader_election_example.
Qed.
Lemma forward_spec c c' il i ir i_max :
- {{{ c ↣ forward_prot (c' ↣ relay_send_prot i_max) il i ir i_max ∗
+ {{{ c ↣ forward_prot (c' ↣ relay_send_prot i_max) il i ir i_max ∗
if (bool_decide (i = i_max)) then c' ↣ relay_send_preprot else True%I }}}
forward c c' #il #i #ir #i_max
{{{ RET #(); True }}}.
@@ -239,34 +225,27 @@ Section ring_leader_election_example.
wp_pures. case_bool_decide.
- simplify_eq. wp_pures.
case_bool_decide; [|simplify_eq;lia].
- wp_send with "[//]".
- wp_pures. wp_send with "[Hc'//]".
- wp_recv as "Hc'". by iApply "HΦ".
- - case_bool_decide; [simplify_eq;lia|].
- wp_pures. iClear "Hc'".
- wp_recv as "Hc'".
- wp_send with "[//]".
- wp_send with "[Hc'//]".
+ wp_send with "[//]". wp_send with "[Hc'//]". wp_recv as "Hc'".
by iApply "HΦ".
+ - case_bool_decide; [simplify_eq;lia|].
+ iClear "Hc'". wp_recv as "Hc'".
+ wp_send with "[//]". wp_send with "[Hc'//]". by iApply "HΦ".
Qed.
Lemma program_spec :
{{{ True }}} program #() {{{ RET #(); True }}}.
- Proof.
+ Proof.
iIntros (Φ) "_ HΦ". wp_lam.
wp_new_chan (prot_pool') with (prot_pool_consistent')
as (c0' c1') "Hc0'" "Hc1'".
wp_smart_apply (wp_fork with "[Hc0']").
- { iIntros "!>".
- wp_pures.
- wp_recv (i_max) as "_". wp_pures.
- iLöb as "IH".
- wp_recv as "_". wp_pures.
- wp_smart_apply wp_assert.
+ { iIntros "!>". wp_recv (i_max) as "_". wp_pures.
+ iLöb as "IH". wp_recv as "_". wp_smart_apply wp_assert.
wp_pures. iModIntro. iSplit; [iPureIntro; f_equiv; by case_bool_decide|].
iIntros "!>". wp_pures. by iApply "IH". }
- wp_new_chan (prot_pool (c1' ↣ relay_send_preprot) (λ i_max, c1' ↣ relay_send_prot i_max)) with prot_pool_consistent
- as (c0 c1 c2 c3) "Hc0" "Hc1" "Hc2" "Hc3".
+ wp_new_chan (prot_pool (c1' ↣ relay_send_preprot)
+ (λ i_max, c1' ↣ relay_send_prot i_max))
+ with prot_pool_consistent as (c0 c1 c2 c3) "Hc0" "Hc1" "Hc2" "Hc3".
wp_smart_apply (wp_fork with "[Hc1]").
{ iIntros "!>". wp_smart_apply (process_spec with "Hc1").
iIntros (i') "Hc1". by wp_smart_apply (forward_spec with "[$Hc1]"). }
--
GitLab