Skip to content
Snippets Groups Projects
Commit d74e871f authored by Jonas Kastberg's avatar Jonas Kastberg
Browse files

Some cleanup

parent cf65eca7
No related branches found
No related tags found
1 merge request!39Multiparty synchronous
Hide whitespace changes
Inline Side-by-side
theories/channel/multi_channel.v
+ 43
− 71
View file @ d74e871f
...@@ -148,9 +148,8 @@ Section channel. ...@@ -148,9 +148,8 @@ Section channel.
Lemma iProto_pointsto_le c p1 p2 : c ↣ p1 ⊢ ▷ (p1 ⊑ p2) -∗ c ↣ p2. Lemma iProto_pointsto_le c p1 p2 : c ↣ p1 ⊢ ▷ (p1 ⊑ p2) -∗ c ↣ p2.
Proof. Proof.
rewrite iProto_pointsto_eq. rewrite iProto_pointsto_eq.
iDestruct 1 as iDestruct 1 as (?????? ->) "(#IH & Hls & Hle & H● & H◯ & Hown)".
(γ γE l n i p ->) "(#IH & Hls & Hle & H● & H◯ & Hown)". iIntros "Hle'". iExists _,_,_,_,_,p'.
iIntros "Hle'". iExists γ, γE, l, n, i, p.
iSplit; [done|]. iFrame "#∗". iSplit; [done|]. iFrame "#∗".
iApply (iProto_le_trans with "Hle Hle'"). iApply (iProto_le_trans with "Hle Hle'").
Qed. Qed.
...@@ -160,36 +159,28 @@ Section channel. ...@@ -160,36 +159,28 @@ Section channel.
([∗ list] i ↦ _ ∈ replicate n x2, P i). ([∗ list] i ↦ _ ∈ replicate n x2, P i).
Proof. Proof.
iIntros "H". iIntros "H".
iInduction n as [|n] "IHn". iInduction n as [|n] "IHn"; [done|].
{ done. }
replace (S n) with (n + 1) by lia. replace (S n) with (n + 1) by lia.
rewrite !replicate_add. rewrite !replicate_add /=. iDestruct "H" as "[H1 H2]".
simpl. iDestruct "H" as "[H1 H2]". iSplitL "H1"; [by iApply "IHn"|]=> /=.
iSplitL "H1". by rewrite !replicate_length.
{ by iApply "IHn". }
simpl. rewrite !replicate_length. iFrame.
Qed. Qed.
Lemma array_to_matrix_pre l n m v : Lemma array_to_matrix_pre l n m v :
l ↦∗ replicate (n * m) v -∗ l ↦∗ replicate (n * m) v -∗
[∗ list] i ↦ _ ∈ replicate n (), [∗ list] i ↦ _ ∈ replicate n (), (l +ₗ i*m) ↦∗ replicate m v.
(l +ₗ i*m) ↦∗ replicate m v.
Proof. Proof.
iIntros "Hl". iIntros "Hl".
iInduction n as [|n] "IHn". iInduction n as [|n] "IHn"; [done|].
{ done. }
replace (S n) with (n + 1) by lia. replace (S n) with (n + 1) by lia.
replace ((n + 1) * m) with (n * m + m) by lia. replace ((n + 1) * m) with (n * m + m) by lia.
rewrite !replicate_add. simpl. rewrite !replicate_add /= array_app=> /=.
rewrite array_app. iDestruct "Hl" as "[Hl Hls]".
iDestruct "Hl" as "[H1 H2]". iDestruct ("IHn" with "Hl") as "Hl".
iDestruct ("IHn" with "H1") as "H1". iFrame=> /=.
iFrame. rewrite Nat.add_0_r !replicate_length.
simpl.
rewrite Nat.add_0_r.
rewrite !replicate_length.
replace (Z.of_nat (n * m)) with (Z.of_nat n * Z.of_nat m)%Z by lia. replace (Z.of_nat (n * m)) with (Z.of_nat n * Z.of_nat m)%Z by lia.
iFrame. by iFrame.
Qed. Qed.
Lemma array_to_matrix l n v : Lemma array_to_matrix l n v :
...@@ -198,20 +189,17 @@ Section channel. ...@@ -198,20 +189,17 @@ Section channel.
[∗ list] j ↦ _ ∈ replicate n (), [∗ list] j ↦ _ ∈ replicate n (),
(l +ₗ pos n i j) ↦ v. (l +ₗ pos n i j) ↦ v.
Proof. Proof.
iIntros "H". iIntros "Hl".
iDestruct (array_to_matrix_pre with "H") as "H". iDestruct (array_to_matrix_pre with "Hl") as "Hl".
iApply (big_sepL_impl with "H"). iApply (big_sepL_impl with "Hl").
iIntros "!>" (i ? HSome) "H". iIntros "!>" (i ? _) "Hl".
clear HSome.
rewrite /array.
iApply big_sepL_replicate. iApply big_sepL_replicate.
iApply (big_sepL_impl with "H"). iApply (big_sepL_impl with "Hl").
iIntros "!>" (j ? HSome) "Hl". iIntros "!>" (j ? HSome) "Hl".
rewrite /pos.
rewrite Loc.add_assoc. rewrite Loc.add_assoc.
replace (Z.of_nat i * Z.of_nat n + Z.of_nat j)%Z with replace (Z.of_nat i * Z.of_nat n + Z.of_nat j)%Z with
(Z.of_nat (i * n + j))%Z by lia. (Z.of_nat (i * n + j))%Z by lia.
apply lookup_replicate in HSome as [-> _]. done. by apply lookup_replicate in HSome as [-> _].
Qed. Qed.
(** ** Specifications of [send] and [recv] *) (** ** Specifications of [send] and [recv] *)
...@@ -234,49 +222,37 @@ Section channel. ...@@ -234,49 +222,37 @@ Section channel.
own (γEs !!! i) (◯E (Next (ps !!! i))) ∗ own (γEs !!! i) (◯E (Next (ps !!! i))) ∗
iProto_own γ i (ps !!! i))%I with "[Hps']" as "H". iProto_own γ i (ps !!! i))%I with "[Hps']" as "H".
{ clear Hle. { clear Hle.
(* iInduction n as [|n] "IHn" forall (ps HSome Heq). *)
iInduction n as [|n] "IHn" forall (ps Hdom). iInduction n as [|n] "IHn" forall (ps Hdom).
{ iExists []. iModIntro. simpl. done. } { iExists []. iModIntro. simpl. done. }
(* assert (n < S n) by lia. *) assert (is_Some (ps !! n)) as [p HSome].
assert (is_Some (ps !! n)) as [p ?]. { apply elem_of_dom. rewrite Hdom. apply elem_of_set_seq. lia. }
{ apply elem_of_dom. iDestruct (big_sepM_delete _ _ n with "Hps'") as "[Hp Hps']"; [done|].
rewrite Hdom.
apply elem_of_set_seq.
lia. }
iDestruct (big_sepM_delete _ _ n with "Hps'") as "[Hp Hps']".
{ done. }
iMod (own_alloc (●E (Next p) ⋅ ◯E (Next p))) as (γE) "[Hauth Hfrag]". iMod (own_alloc (●E (Next p) ⋅ ◯E (Next p))) as (γE) "[Hauth Hfrag]".
{ apply excl_auth_valid. } { apply excl_auth_valid. }
iMod ("IHn" with "[] Hps'") as (γEs Hlen) "H". iMod ("IHn" with "[] Hps'") as (γEs Hlen) "H".
{ iPureIntro. { iPureIntro.
rewrite dom_delete_L. rewrite Hdom. rewrite dom_delete_L Hdom.
replace (S n) with (n + 1) by lia. replace (S n) with (n + 1) by lia.
rewrite set_seq_add_L. rewrite set_seq_add_L /= right_id_L difference_union_distr_l_L
simpl. difference_diag_L right_id_L.
rewrite right_id_L.
rewrite difference_union_distr_l_L.
rewrite difference_diag_L. rewrite right_id_L.
assert (n ∉ (set_seq 0 n:gset _)); [|set_solver]. assert (n ∉ (set_seq 0 n:gset _)); [|set_solver].
intros Hin%elem_of_set_seq. lia. } intros Hin%elem_of_set_seq. lia. }
iModIntro. iExists (γEs++[γE]). iModIntro. iExists (γEs++[γE]).
replace (S n) with (n + 1) by lia. replace (S n) with (n + 1) by lia.
rewrite replicate_add. rewrite replicate_add big_sepL_app app_length Hlen.
rewrite big_sepL_app. iSplit; [done|]=> /=.
rewrite app_length.
rewrite Hlen. iSplit; [done|].
simpl.
iSplitL "H". iSplitL "H".
{ iApply (big_sepL_impl with "H"). { iApply (big_sepL_impl with "H").
iIntros "!>" (i ? HSome') "(Hauth & Hfrag & Hown)". iIntros "!>" (i ? HSome') "(Hauth & Hfrag & Hown)".
assert (i < n). assert (i < n) as Hle.
{ by apply lookup_replicate_1 in HSome' as [? ?]. } { by apply lookup_replicate_1 in HSome' as [??]. }
assert (delete n ps !!! i = ps !!! i) as Heq'. assert (delete n ps !!! i = ps !!! i) as Heq'.
{ apply lookup_total_delete_ne. lia. } { apply lookup_total_delete_ne. lia. }
rewrite Heq'. iFrame. rewrite Heq'. iFrame.
rewrite lookup_total_app_l; [|lia]. iFrame. } rewrite lookup_total_app_l; [|lia]. iFrame. }
simpl. rewrite replicate_length. rewrite Nat.add_0_r. rewrite replicate_length Nat.add_0_r.
rewrite list_lookup_total_middle; [|done]. rewrite list_lookup_total_middle; [|done].
rewrite lookup_total_alt. rewrite H. simpl. iFrame. } rewrite lookup_total_alt HSome. by iFrame. }
iMod "H" as (γEs Hlen) "H". iMod "H" as (γEs Hlen) "H".
iAssert (|={⊤}=> iAssert (|={⊤}=>
[∗ list] i ↦ _ ∈ replicate n (), [∗ list] i ↦ _ ∈ replicate n (),
...@@ -292,11 +268,8 @@ Section channel. ...@@ -292,11 +268,8 @@ Section channel.
iApply big_sepL_fupd. iApply big_sepL_fupd.
iApply (big_sepL_impl with "H1"). iApply (big_sepL_impl with "H1").
iIntros "!>" (j ? HSome'') "H1". iIntros "!>" (j ? HSome'') "H1".
iMod (own_alloc (Excl ())) as (γ') "Hγ'". iMod (own_alloc (Excl ())) as (γ') "Hγ'"; [done|].
{ done. } iExists γ'. iApply inv_alloc. iLeft. iFrame. }
iExists γ'.
iApply inv_alloc.
iLeft. iFrame. }
iMod "IH" as "#IH". iMod "IH" as "#IH".
iMod (inv_alloc with "Hps") as "#IHp". iMod (inv_alloc with "Hps") as "#IHp".
iExists _,_,_,_. iExists _,_,_,_.
...@@ -319,16 +292,15 @@ Section channel. ...@@ -319,16 +292,15 @@ Section channel.
{ apply lookup_replicate in HSome' as [_ Hle']. done. } { apply lookup_replicate in HSome' as [_ Hle']. done. }
assert (j < n) as Hle''. assert (j < n) as Hle''.
{ apply lookup_replicate in HSome'' as [_ Hle'']. done. } { apply lookup_replicate in HSome'' as [_ Hle'']. done. }
iDestruct (big_sepL_lookup _ _ i () with "IH") as "IH''". iDestruct (big_sepL_lookup _ _ i () with "IH") as "IH'";
{ rewrite lookup_replicate. done. } [by rewrite lookup_replicate|].
iDestruct (big_sepL_lookup _ _ j () with "IH''") as "IH'''". iDestruct (big_sepL_lookup _ _ j () with "IH'") as "IH''";
{ rewrite lookup_replicate. done. } [by rewrite lookup_replicate|].
iFrame "#". iDestruct (big_sepL_lookup _ _ j () with "IH") as "H";
iDestruct (big_sepL_lookup _ _ j () with "IH") as "H". [by rewrite lookup_replicate|].
{ rewrite lookup_replicate. done. } iDestruct (big_sepL_lookup _ _ i () with "H") as "H'";
iDestruct (big_sepL_lookup _ _ i () with "H") as "H'". [by rewrite lookup_replicate|].
{ rewrite lookup_replicate. done. } iDestruct "IH''" as (γ1) "?".
iDestruct "IH'''" as (γ1) "?".
iDestruct "H'" as (γ2) "?". iDestruct "H'" as (γ2) "?".
iExists _, _. iFrame "#". iExists _, _. iFrame "#".
Qed. Qed.
......
theories/channel/multi_proto.v
+ 60
− 98
View file @ d74e871f
...@@ -510,23 +510,23 @@ Section proto. ...@@ -510,23 +510,23 @@ Section proto.
End proto. End proto.
Instance iProto_inhabited {Σ V} : Inhabited (iProto Σ V) := populate (END). Global Instance iProto_inhabited {Σ V} : Inhabited (iProto Σ V) := populate END.
Definition can_step {Σ V} (rec : gmap nat (iProto Σ V) → iProp Σ) Definition can_step {Σ V} (rec : gmap nat (iProto Σ V) → iProp Σ)
(ps : gmap nat (iProto Σ V)) (i j : nat) : iProp Σ := (ps : gmap nat (iProto Σ V)) (i j : nat) : iProp Σ :=
∀ m1 m2, ∀ m1 m2,
((ps !!! i ≡ <(Send, j)> m1) -∗ (ps !!! j ≡ <(Recv, i)> m2) -∗ (ps !!! i ≡ <(Send, j)> m1) -∗
∀ v p1, iMsg_car m1 v (Next p1) -∗ (ps !!! j ≡ <(Recv, i)> m2) -∗
∃ p2, iMsg_car m2 v (Next p2) ∗ ∀ v p1, iMsg_car m1 v (Next p1) -∗
▷ (rec (<[i:=p1]>(<[j:=p2]>ps)))). ∃ p2, iMsg_car m2 v (Next p2) ∗
▷ (rec (<[i:=p1]>(<[j:=p2]>ps))).
Definition valid_target {Σ V} (ps : gmap nat (iProto Σ V)) (i j : nat) : iProp Σ := Definition valid_target {Σ V} (ps : gmap nat (iProto Σ V)) (i j : nat) : iProp Σ :=
∀ a m, ((ps !!! i ≡ <(a, j)> m) -∗ ⌜is_Some (ps !! j)⌝). ∀ a m, (ps !!! i ≡ <(a, j)> m) -∗ ⌜is_Some (ps !! j)⌝.
Definition iProto_consistent_pre {Σ V} (rec : gmap nat (iProto Σ V) → iProp Σ) Definition iProto_consistent_pre {Σ V} (rec : gmap nat (iProto Σ V) → iProp Σ)
(ps : gmap nat (iProto Σ V)) : iProp Σ := (ps : gmap nat (iProto Σ V)) : iProp Σ :=
(∀ i j, valid_target ps i j) ∗ (∀ i j, valid_target ps i j) ∗ (∀ i j, can_step rec ps i j).
(∀ i j, can_step rec ps i j).
Global Instance iProto_consistent_pre_ne {Σ V} Global Instance iProto_consistent_pre_ne {Σ V}
(rec : gmapO natO (iProto Σ V) -n> iPropO Σ) : (rec : gmapO natO (iProto Σ V) -n> iPropO Σ) :
...@@ -616,7 +616,6 @@ Definition iProto_own_frag `{!protoG Σ V} (γ : gname) ...@@ -616,7 +616,6 @@ Definition iProto_own_frag `{!protoG Σ V} (γ : gname)
Definition iProto_own_auth `{!protoG Σ V} (γ : gname) Definition iProto_own_auth `{!protoG Σ V} (γ : gname)
(ps : gmap nat (iProto Σ V)) : iProp Σ := (ps : gmap nat (iProto Σ V)) : iProp Σ :=
(* own γ (● ∅). *)
own γ (gmap_view_auth (DfracOwn 1) (((λ p, Excl' (Next p)) <$> ps) : gmap _ _)). own γ (gmap_view_auth (DfracOwn 1) (((λ p, Excl' (Next p)) <$> ps) : gmap _ _)).
Definition iProto_ctx `{protoG Σ V} Definition iProto_ctx `{protoG Σ V}
...@@ -669,21 +668,18 @@ Section proto. ...@@ -669,21 +668,18 @@ Section proto.
Lemma iProto_le_send_inv i p1 m2 : Lemma iProto_le_send_inv i p1 m2 :
p1 ⊑ (<(Send,i)> m2) -∗ ∃ m1, p1 ⊑ (<(Send,i)> m2) -∗ ∃ m1,
(p1 ≡ <(Send,i)> m1) ∗ (p1 ≡ <(Send,i)> m1) ∗
∀ v p2', iMsg_car m2 v (Next p2') -∗ ∃ p1', ∀ v p2', iMsg_car m2 v (Next p2') -∗
▷ (p1' ⊑ p2') ∗ iMsg_car m1 v (Next p1'). ∃ p1', ▷ (p1' ⊑ p2') ∗ iMsg_car m1 v (Next p1').
Proof. Proof.
rewrite iProto_le_unfold. rewrite iProto_le_unfold.
iIntros "[[_ Heq]|H]". iIntros "[[_ Heq]|H]".
{ iDestruct (iProto_message_end_equivI with "Heq") as %[]. } { by iDestruct (iProto_message_end_equivI with "Heq") as %[]. }
iDestruct "H" as (a1 a2 m1 m2') "(Hp1 & Hp2 & H)". iDestruct "H" as (a1 a2 m1 m2') "(Hp1 & Hp2 & H)".
rewrite iProto_message_equivI. iDestruct "Hp2" as "[%Heq Hm2]". rewrite iProto_message_equivI. iDestruct "Hp2" as "[%Heq Hm2]".
simplify_eq. simplify_eq.
destruct a1 as [[]]; [|done]. destruct a1 as [[]]; [|done].
iDestruct "H" as (->) "H". iDestruct "H" as (->) "H". iExists m1. iFrame "Hp1".
iExists m1. iFrame. iIntros (v p2). iSpecialize ("Hm2" $! v (Next p2)). by iRewrite "Hm2".
iIntros (v p2).
iSpecialize ("Hm2" $! v (Next p2)).
iRewrite "Hm2". iApply "H".
Qed. Qed.
Lemma iProto_le_send_send_inv i m1 m2 v p2' : Lemma iProto_le_send_send_inv i m1 m2 v p2' :
...@@ -699,8 +695,8 @@ Section proto. ...@@ -699,8 +695,8 @@ Section proto.
Lemma iProto_le_recv_inv_l i m1 p2 : Lemma iProto_le_recv_inv_l i m1 p2 :
(<(Recv,i)> m1) ⊑ p2 -∗ ∃ m2, (<(Recv,i)> m1) ⊑ p2 -∗ ∃ m2,
(p2 ≡ <(Recv,i)> m2) ∗ (p2 ≡ <(Recv,i)> m2) ∗
∀ v p1', iMsg_car m1 v (Next p1') -∗ ∃ p2', ∀ v p1', iMsg_car m1 v (Next p1') -∗
▷ (p1' ⊑ p2') ∗ iMsg_car m2 v (Next p2'). ∃ p2', ▷ (p1' ⊑ p2') ∗ iMsg_car m2 v (Next p2').
Proof. Proof.
rewrite iProto_le_unfold. rewrite iProto_le_unfold.
iIntros "[[Heq _]|H]". iIntros "[[Heq _]|H]".
...@@ -709,18 +705,15 @@ Section proto. ...@@ -709,18 +705,15 @@ Section proto.
rewrite iProto_message_equivI. iDestruct "Hp1" as "[%Heq Hm1]". rewrite iProto_message_equivI. iDestruct "Hp1" as "[%Heq Hm1]".
simplify_eq. simplify_eq.
destruct a2 as [[]]; [done|]. destruct a2 as [[]]; [done|].
iDestruct "H" as (->) "H". iDestruct "H" as (->) "H". iExists m2. iFrame "Hp2".
iExists m2. iFrame. iIntros (v p1). iSpecialize ("Hm1" $! v (Next p1)). by iRewrite "Hm1".
iIntros (v p1).
iSpecialize ("Hm1" $! v (Next p1)).
iRewrite "Hm1". iApply "H".
Qed. Qed.
Lemma iProto_le_recv_inv_r i p1 m2 : Lemma iProto_le_recv_inv_r i p1 m2 :
(p1 ⊑ <(Recv,i)> m2) -∗ ∃ m1, (p1 ⊑ <(Recv,i)> m2) -∗ ∃ m1,
(p1 ≡ <(Recv,i)> m1) ∗ (p1 ≡ <(Recv,i)> m1) ∗
∀ v p1', iMsg_car m1 v (Next p1') -∗ ∃ p2', ∀ v p1', iMsg_car m1 v (Next p1') -∗
▷ (p1' ⊑ p2') ∗ iMsg_car m2 v (Next p2'). ∃ p2', ▷ (p1' ⊑ p2') ∗ iMsg_car m2 v (Next p2').
Proof. Proof.
rewrite iProto_le_unfold. rewrite iProto_le_unfold.
iIntros "[[_ Heq]|H]". iIntros "[[_ Heq]|H]".
...@@ -759,12 +752,10 @@ Section proto. ...@@ -759,12 +752,10 @@ Section proto.
destruct t1,t2; [|done|done|]. destruct t1,t2; [|done|done|].
- rewrite iProto_message_equivI. - rewrite iProto_message_equivI.
iDestruct "Hp1" as (Heq) "Hp1". simplify_eq. iDestruct "Hp1" as (Heq) "Hp1". simplify_eq.
iDestruct "H" as (->) "H". iDestruct "H" as (->) "H". by iExists _.
iExists _. done.
- rewrite iProto_message_equivI. - rewrite iProto_message_equivI.
iDestruct "Hp1" as (Heq) "Hp1". simplify_eq. iDestruct "Hp1" as (Heq) "Hp1". simplify_eq.
iDestruct "H" as (->) "H". iDestruct "H" as (->) "H". by iExists _.
iExists _. done.
Qed. Qed.
Lemma iProto_le_msg_inv_r j a p1 m2 : Lemma iProto_le_msg_inv_r j a p1 m2 :
...@@ -778,12 +769,10 @@ Section proto. ...@@ -778,12 +769,10 @@ Section proto.
destruct t1,t2; [|done|done|]. destruct t1,t2; [|done|done|].
- rewrite iProto_message_equivI. - rewrite iProto_message_equivI.
iDestruct "Hp2" as (Heq) "Hp2". simplify_eq. iDestruct "Hp2" as (Heq) "Hp2". simplify_eq.
iDestruct "H" as (->) "H". iDestruct "H" as (->) "H". by iExists _.
iExists _. done.
- rewrite iProto_message_equivI. - rewrite iProto_message_equivI.
iDestruct "Hp2" as (Heq) "Hp2". simplify_eq. iDestruct "Hp2" as (Heq) "Hp2". simplify_eq.
iDestruct "H" as (->) "H". iDestruct "H" as (->) "H". by iExists _.
iExists _. done.
Qed. Qed.
Lemma valid_target_le ps i p1 p2 : Lemma valid_target_le ps i p1 p2 :
...@@ -798,7 +787,7 @@ Section proto. ...@@ -798,7 +787,7 @@ Section proto.
iFrame "Hle". iFrame "Hle".
iIntros (i' j' a m) "Hm". iIntros (i' j' a m) "Hm".
destruct (decide (i = j')) as [->|Hneqj]. destruct (decide (i = j')) as [->|Hneqj].
{ rewrite lookup_insert. done. } { by rewrite lookup_insert. }
rewrite lookup_insert_ne; [|done]. rewrite lookup_insert_ne; [|done].
destruct (decide (i = i')) as [->|Hneqi]. destruct (decide (i = i')) as [->|Hneqi].
{ rewrite lookup_total_insert. iRewrite "H" in "Hm". { rewrite lookup_total_insert. iRewrite "H" in "Hm".
...@@ -807,8 +796,7 @@ Section proto. ...@@ -807,8 +796,7 @@ Section proto.
by iApply "Hprot". } by iApply "Hprot". }
destruct Hmsg as (t & n & m & Hmsg). destruct Hmsg as (t & n & m & Hmsg).
setoid_rewrite Hmsg. setoid_rewrite Hmsg.
iDestruct (iProto_le_msg_inv_l with "Hle") as (m2) "#Heq". iDestruct (iProto_le_msg_inv_l with "Hle") as (m2) "#Heq". iFrame "Hle".
iFrame.
iIntros (i' j' a m') "Hm". iIntros (i' j' a m') "Hm".
destruct (decide (i = j')) as [->|Hneqj]. destruct (decide (i = j')) as [->|Hneqj].
{ rewrite lookup_insert. done. } { rewrite lookup_insert. done. }
...@@ -1020,7 +1008,8 @@ Lemma iProto_le_dual p1 p2 : p2 ⊑ p1 -∗ iProto_dual p1 ⊑ iProto_dual p2. ...@@ -1020,7 +1008,8 @@ Lemma iProto_le_dual p1 p2 : p2 ⊑ p1 -∗ iProto_dual p1 ⊑ iProto_dual p2.
iExists (p1' <++> p3). iSplitR "Hm1"; [|by simpl; eauto]. iExists (p1' <++> p3). iSplitR "Hm1"; [|by simpl; eauto].
iIntros "!>". iRewrite "Hp24". by iApply ("IH" with "H1"). iIntros "!>". iRewrite "Hp24". by iApply ("IH" with "H1").
- iDestruct (iProto_le_recv_inv_r with "H1") as (m1) "[Hp1 H1]". - iDestruct (iProto_le_recv_inv_r with "H1") as (m1) "[Hp1 H1]".
iRewrite "Hp1"; clear p1. rewrite !iProto_app_message. iApply iProto_le_recv. iRewrite "Hp1"; clear p1. rewrite !iProto_app_message.
iApply iProto_le_recv.
iIntros (v p13). iDestruct 1 as (p1') "[Hm1 #Hp13]". iIntros (v p13). iDestruct 1 as (p1') "[Hm1 #Hp13]".
iDestruct ("H1" with "Hm1") as (p2'') "[H1 Hm2]". iDestruct ("H1" with "Hm1") as (p2'') "[H1 Hm2]".
iExists (p2'' <++> p4). iSplitR "Hm2"; [|by simpl; eauto]. iExists (p2'' <++> p4). iSplitR "Hm2"; [|by simpl; eauto].
...@@ -1123,9 +1112,7 @@ Lemma iProto_le_dual p1 p2 : p2 ⊑ p1 -∗ iProto_dual p1 ⊑ iProto_dual p2. ...@@ -1123,9 +1112,7 @@ Lemma iProto_le_dual p1 p2 : p2 ⊑ p1 -∗ iProto_dual p1 ⊑ iProto_dual p2.
ps !!! i ≡ (<(a, j)> m) -∗ ps !!! i ≡ (<(a, j)> m) -∗
⌜is_Some (ps !! j)⌝. ⌜is_Some (ps !! j)⌝.
Proof. Proof.
rewrite iProto_consistent_unfold. rewrite iProto_consistent_unfold. iDestruct 1 as "[Htar _]". iApply "Htar".
iDestruct 1 as "[Htar _]".
iApply "Htar".
Qed. Qed.
Lemma iProto_consistent_step ps m1 m2 i j v p1 : Lemma iProto_consistent_step ps m1 m2 i j v p1 :
...@@ -1153,13 +1140,10 @@ Lemma iProto_le_dual p1 p2 : p2 ⊑ p1 -∗ iProto_dual p1 ⊑ iProto_dual p2. ...@@ -1153,13 +1140,10 @@ Lemma iProto_le_dual p1 p2 : p2 ⊑ p1 -∗ iProto_dual p1 ⊑ iProto_dual p2.
iDestruct (own_valid_2 with "H● H◯") as "H✓". iDestruct (own_valid_2 with "H● H◯") as "H✓".
rewrite gmap_view_both_validI. rewrite gmap_view_both_validI.
iDestruct "H✓" as "[_ [H1 H2]]". iDestruct "H✓" as "[_ [H1 H2]]".
rewrite lookup_total_alt. rewrite lookup_total_alt lookup_fmap.
rewrite lookup_fmap.
destruct (ps !! i); last first. destruct (ps !! i); last first.
{ simpl. rewrite !option_equivI. done. } { by rewrite !option_equivI. }
simpl. simpl. rewrite !option_equivI excl_equivI. by iNext.
rewrite !option_equivI excl_equivI.
by iNext.
Qed. Qed.
Lemma iProto_own_auth_update γ ps i p p' : Lemma iProto_own_auth_update γ ps i p p' :
...@@ -1184,19 +1168,13 @@ Lemma iProto_le_dual p1 p2 : p2 ⊑ p1 -∗ iProto_dual p1 ⊑ iProto_dual p2. ...@@ -1184,19 +1168,13 @@ Lemma iProto_le_dual p1 p2 : p2 ⊑ p1 -∗ iProto_dual p1 ⊑ iProto_dual p2.
{ apply gmap_view_auth_valid. } { apply gmap_view_auth_valid. }
iExists γ. iExists γ.
iInduction ps as [|i p ps Hin] "IH" using map_ind. iInduction ps as [|i p ps Hin] "IH" using map_ind.
{ iModIntro. iFrame. { iModIntro. iFrame. by iApply big_sepM_empty. }
by iApply big_sepM_empty. }
iMod ("IH" with "Hauth") as "[Hauth Hfrags]". iMod ("IH" with "Hauth") as "[Hauth Hfrags]".
rewrite big_sepM_insert; [|done]. iFrame "Hfrags". rewrite big_sepM_insert; [|done]. iFrame "Hfrags".
iMod (own_update with "Hauth") as "[Hauth Hfrag]". iMod (own_update with "Hauth") as "[Hauth Hfrag]".
{ apply (gmap_view_alloc _ i (DfracOwn 1) (Excl' (Next p))). { apply (gmap_view_alloc _ i (DfracOwn 1) (Excl' (Next p))); [|done|done].
- rewrite lookup_fmap. rewrite Hin. done. by rewrite lookup_fmap Hin. }
- done. iModIntro. rewrite -fmap_insert. iFrame.
- done. }
iFrame.
iModIntro.
rewrite -fmap_insert.
iFrame.
iExists _. iFrame. iApply iProto_le_refl. iExists _. iFrame. iApply iProto_le_refl.
Qed. Qed.
...@@ -1211,9 +1189,9 @@ Lemma iProto_le_dual p1 p2 : p2 ⊑ p1 -∗ iProto_dual p1 ⊑ iProto_dual p2. ...@@ -1211,9 +1189,9 @@ Lemma iProto_le_dual p1 p2 : p2 ⊑ p1 -∗ iProto_dual p1 ⊑ iProto_dual p2.
▷ iProto_consistent ps -∗ ▷ iProto_consistent ps -∗
|==> ∃ γ, iProto_ctx γ (dom ps) ∗ [∗ map] i ↦p ∈ ps, iProto_own γ i p. |==> ∃ γ, iProto_ctx γ (dom ps) ∗ [∗ map] i ↦p ∈ ps, iProto_own γ i p.
Proof. Proof.
iIntros "Hconsistnet". iIntros "Hconsistent".
iMod iProto_own_auth_alloc as (γ) "[Hauth Hfrags]". iMod iProto_own_auth_alloc as (γ) "[Hauth Hfrags]".
iExists γ. iFrame. iExists _. iFrame. done. iExists γ. iFrame. iExists _. by iFrame.
Qed. Qed.
Lemma own_prot_idx γ i j (p1 p2 : iProto Σ V) : Lemma own_prot_idx γ i j (p1 p2 : iProto Σ V) :
...@@ -1224,7 +1202,7 @@ Lemma iProto_le_dual p1 p2 : p2 ⊑ p1 -∗ iProto_dual p1 ⊑ iProto_dual p2. ...@@ -1224,7 +1202,7 @@ Lemma iProto_le_dual p1 p2 : p2 ⊑ p1 -∗ iProto_dual p1 ⊑ iProto_dual p2.
iIntros "Hown Hown'" (->). iIntros "Hown Hown'" (->).
iDestruct (own_valid_2 with "Hown Hown'") as "H". iDestruct (own_valid_2 with "Hown Hown'") as "H".
rewrite uPred.cmra_valid_elim. rewrite uPred.cmra_valid_elim.
iDestruct "H" as %H%gmap_view_frag_op_validN. by destruct H. by iDestruct "H" as %[]%gmap_view_frag_op_validN.
Qed. Qed.
Lemma iProto_step γ ps_dom i j m1 m2 p1 v : Lemma iProto_step γ ps_dom i j m1 m2 p1 v :
...@@ -1243,52 +1221,40 @@ Lemma iProto_le_dual p1 p2 : p2 ⊑ p1 -∗ iProto_dual p1 ⊑ iProto_dual p2. ...@@ -1243,52 +1221,40 @@ Lemma iProto_le_dual p1 p2 : p2 ⊑ p1 -∗ iProto_dual p1 ⊑ iProto_dual p2.
iDestruct (iProto_own_auth_agree with "Hauth Hj") as "#Hpj". iDestruct (iProto_own_auth_agree with "Hauth Hj") as "#Hpj".
iDestruct (own_prot_idx with "Hi Hj") as %Hneq. iDestruct (own_prot_idx with "Hi Hj") as %Hneq.
iAssert (▷ (<[i:=<(Send, j)> m1]>ps !!! j ≡ pj))%I as "Hpj'". iAssert (▷ (<[i:=<(Send, j)> m1]>ps !!! j ≡ pj))%I as "Hpj'".
{ rewrite lookup_total_insert_ne; done. } { by rewrite lookup_total_insert_ne. }
iAssert (▷ (⌜is_Some (ps !! i)⌝ ∗ (pi ⊑ (<(Send, j)> m1))))%I with "[Hile]" iAssert (▷ (⌜is_Some (ps !! i)⌝ ∗ (pi ⊑ (<(Send, j)> m1))))%I with "[Hile]"
as "[Hi' Hile]". as "[Hi' Hile]".
{ iNext. { iNext. iDestruct (iProto_le_msg_inv_r with "Hile") as (m) "#Heq".
iDestruct (iProto_le_msg_inv_r with "Hile") as (m) "#H". iFrame. iRewrite "Heq" in "Hpi". rewrite lookup_total_alt.
iFrame.
iRewrite "H" in "Hpi".
rewrite lookup_total_alt. simpl.
destruct (ps !! i); [done|]. destruct (ps !! i); [done|].
simpl. iDestruct (iProto_end_message_equivI with "Hpi") as "[]". } iDestruct (iProto_end_message_equivI with "Hpi") as "[]". }
iAssert (▷ (⌜is_Some (ps !! j)⌝ ∗ (pj ⊑ (<(Recv, i)> m2))))%I with "[Hjle]" iAssert (▷ (⌜is_Some (ps !! j)⌝ ∗ (pj ⊑ (<(Recv, i)> m2))))%I with "[Hjle]"
as "[Hj' Hjle]". as "[Hj' Hjle]".
{ iNext. { iNext. iDestruct (iProto_le_msg_inv_r with "Hjle") as (m) "#Heq".
iDestruct (iProto_le_msg_inv_r with "Hjle") as (m) "#H". iFrame. iRewrite "Heq" in "Hpj". rewrite !lookup_total_alt.
iFrame.
iRewrite "H" in "Hpj".
rewrite !lookup_total_alt. simpl.
destruct (ps !! j); [done|]. destruct (ps !! j); [done|].
simpl. iDestruct (iProto_end_message_equivI with "Hpj") as "[]". } iDestruct (iProto_end_message_equivI with "Hpj") as "[]". }
iDestruct (iProto_consistent_le with "Hconsistent Hpi Hile") as "Hconsistent". iDestruct (iProto_consistent_le with "Hconsistent Hpi Hile") as "Hconsistent".
iDestruct (iProto_consistent_le with "Hconsistent Hpj' Hjle") as "Hconsistent". iDestruct (iProto_consistent_le with "Hconsistent Hpj' Hjle") as "Hconsistent".
iDestruct (iProto_consistent_step _ _ _ i j with "Hconsistent [] [] [Hm //]") as iDestruct (iProto_consistent_step _ _ _ i j with "Hconsistent [] [] [Hm //]") as
(p2) "[Hm2 Hconsistent]". (p2) "[Hm2 Hconsistent]".
{ rewrite lookup_total_insert_ne; [|done]. { rewrite lookup_total_insert_ne; [|done].
rewrite lookup_total_insert_ne; [|done]. rewrite lookup_total_insert_ne; [|done].
iNext. rewrite lookup_total_insert. done. } by rewrite lookup_total_insert. }
{ rewrite lookup_total_insert_ne; [|done]. { rewrite lookup_total_insert_ne; [|done].
iNext. rewrite lookup_total_insert. done. } by rewrite lookup_total_insert. }
iMod (iProto_own_auth_update _ _ _ _ p2 with "Hauth Hj") as "[Hauth Hj]". iMod (iProto_own_auth_update _ _ _ _ p2 with "Hauth Hj") as "[Hauth Hj]".
iMod (iProto_own_auth_update _ _ _ _ p1 with "Hauth Hi") as "[Hauth Hi]". iMod (iProto_own_auth_update _ _ _ _ p1 with "Hauth Hi") as "[Hauth Hi]".
iIntros "!>!>". iExists p2. iFrame. iIntros "!>!>". iExists p2. iFrame "Hm2".
iDestruct "Hi'" as %Hi. iDestruct "Hi'" as %Hi. iDestruct "Hj'" as %Hj.
iDestruct "Hj'" as %Hj.
iSplitL "Hconsistent Hauth". iSplitL "Hconsistent Hauth".
{ iExists (<[i:=p1]> (<[j:=p2]> ps)). { iExists (<[i:=p1]> (<[j:=p2]> ps)).
iSplit. iSplit.
{ rewrite !dom_insert_lookup_L; [done|..]. { rewrite !dom_insert_lookup_L; [done..|by rewrite lookup_insert_ne]. }
- done.
- by rewrite lookup_insert_ne. }
iFrame. rewrite insert_insert. iFrame. rewrite insert_insert.
rewrite insert_commute; [|done]. rewrite insert_insert. rewrite insert_commute; [|done]. rewrite insert_insert.
rewrite insert_commute; [|done]. done. } by rewrite insert_commute; [|done]. }
iSplitL "Hi". iSplitL "Hi"; iExists _; iFrame; iApply iProto_le_refl.
- iExists _. iFrame. iApply iProto_le_refl.
- iExists _. iFrame. iApply iProto_le_refl.
Qed. Qed.
Lemma iProto_target γ ps_dom i a j m : Lemma iProto_target γ ps_dom i a j m :
...@@ -1300,20 +1266,16 @@ Lemma iProto_le_dual p1 p2 : p2 ⊑ p1 -∗ iProto_dual p1 ⊑ iProto_dual p2. ...@@ -1300,20 +1266,16 @@ Lemma iProto_le_dual p1 p2 : p2 ⊑ p1 -∗ iProto_dual p1 ⊑ iProto_dual p2.
rewrite /iProto_ctx /iProto_own. rewrite /iProto_ctx /iProto_own.
iDestruct "Hctx" as (ps Hdom) "[Hauth Hps]". iDestruct "Hctx" as (ps Hdom) "[Hauth Hps]".
iDestruct "Hown" as (p') "[Hle Hown]". iDestruct "Hown" as (p') "[Hle Hown]".
iDestruct (iProto_own_auth_agree with "Hauth Hown") as "#H". iDestruct (iProto_own_auth_agree with "Hauth Hown") as "#Hi".
iDestruct (iProto_le_msg_inv_r with "Hle") as (m') "#Heq". iDestruct (iProto_le_msg_inv_r with "Hle") as (m') "#Heq".
iAssert (▷ (⌜is_Some (ps !! j)⌝ ∗ iProto_consistent ps))%I iAssert (▷ (⌜is_Some (ps !! j)⌝ ∗ iProto_consistent ps))%I
with "[Hps]" as "[H1 H2]". with "[Hps]" as "[HSome Hps]".
{ iNext. { iNext. iRewrite "Heq" in "Hi".
iRewrite "Heq" in "H". iDestruct (iProto_consistent_target with "Hps Hi") as "#$". by iFrame. }
iDestruct (iProto_consistent_target with "Hps H") as "#H'". iSplitL "HSome".
iFrame. done. } { iNext. iDestruct "HSome" as %Heq.
iSplitL "H1". iPureIntro. simplify_eq. by apply elem_of_dom. }
{ iNext. iDestruct "H1" as %Heq. iSplitL "Hauth Hps"; iExists _; by iFrame.
iPureIntro. simplify_eq. apply elem_of_dom. done. }
iSplitL "Hauth H2".
{ iExists _. iFrame. done. }
iExists _. iFrame.
Qed. Qed.
(* (** The instances below make it possible to use the tactics [iIntros], *) (* (** The instances below make it possible to use the tactics [iIntros], *)
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment