diff --git a/multi_actris/channel/channel.v b/multi_actris/channel/channel.v
index 89937a2550979a790b45293561e19769fcebf966..0a1248a74245c07abcf33c1ac2380321efd39aae 100644
--- a/multi_actris/channel/channel.v
+++ b/multi_actris/channel/channel.v
@@ -103,7 +103,7 @@ Definition iProto_pointsto_def `{!heapGS Σ, !chanG Σ}
(c : val) (p : iProto Σ) : iProp Σ :=
∃ γ γE1 (l:loc) (i:nat) (n:nat) p',
⌜ c = (#l,#n,#i)%V ⌠∗
- inv (nroot.@"ctx") (iProto_ctx γ (set_seq 0 n)) ∗
+ inv (nroot.@"ctx") (iProto_ctx γ n) ∗
([∗list] j ↦ _ ∈ replicate n (),
∃ γE2 γt1 γt2,
inv (nroot.@"p") (chan_inv γ γE1 γt1 i j (l +ₗ (pos n i j))) ∗
@@ -121,12 +121,12 @@ Notation "c ↣ p" := (iProto_pointsto c p)
(at level 20, format "c ↣ p").
Definition chan_pool `{!heapGS Σ, !chanG Σ}
- (cs : val) (ps : gmap nat (iProto Σ)) : iProp Σ :=
- ∃ γ (γEs : list gname) (l:loc) (n:nat),
- ⌜cs = (#l,#n)%V⌠∗ ⌜∀ i, is_Some (ps !! i) → i < n⌠∗
- inv (nroot.@"ctx") (iProto_ctx γ (set_seq 0 n)) ∗
+ (cs : val) (i':nat) (ps : list (iProto Σ)) : iProp Σ :=
+ ∃ γ (γEs : list gname) (n:nat) (l:loc),
+ ⌜cs = (#l,#n)%V⌠∗ ⌜(i' + length ps = n)%nat⌠∗
+ inv (nroot.@"ctx") (iProto_ctx γ n) ∗
[∗ list] i ↦ _ ∈ replicate n (),
- (∀ p, ⌜ps !! i = Some p⌠-∗
+ (∀ p, ⌜i' <= i⌠-∗ ⌜ps !! (i - i') = Some p⌠-∗
own (γEs !!! i) (â—E (Next p)) ∗
own (γEs !!! i) (◯E (Next p)) ∗
iProto_own γ i p) ∗
@@ -203,63 +203,53 @@ Section channel.
Qed.
(** ** Specifications of [send] and [recv] *)
- Lemma new_chan_spec (n:nat) (ps:gmap nat (iProto Σ)) :
- 0 < n →
- dom ps = set_seq 0 n →
+ Lemma new_chan_spec (ps:list (iProto Σ)) :
+ 0 < length ps →
{{{ iProto_consistent ps }}}
- new_chan #n
- {{{ cs, RET cs; chan_pool cs ps }}}.
+ new_chan #(length ps)
+ {{{ cs, RET cs; chan_pool cs 0 ps }}}.
Proof.
- iIntros (Hle Hdom Φ) "Hps HΦ". wp_lam.
+ iIntros (Hle Φ) "Hps HΦ". wp_lam.
wp_smart_apply wp_allocN; [lia|done|].
iIntros (l) "[Hl _]".
iMod (iProto_init with "Hps") as (γ) "[Hps Hps']".
wp_pures. iApply "HΦ".
iAssert (|==> ∃ (γEs : list gname),
- ⌜length γEs = n⌠∗
- [∗ list] i ↦ _ ∈ replicate n (),
+ ⌜length γEs = length ps⌠∗
+ [∗ list] i ↦ _ ∈ replicate (length ps) (),
own (γEs !!! i) (â—E (Next (ps !!! i))) ∗
own (γEs !!! i) (◯E (Next (ps !!! i))) ∗
iProto_own γ i (ps !!! i))%I with "[Hps']" as "H".
{ clear Hle.
- iInduction n as [|n] "IHn" forall (ps Hdom).
+ iInduction ps as [|p ps] "IHn" using rev_ind.
{ iExists []. iModIntro. simpl. done. }
- assert (is_Some (ps !! n)) as [p HSome].
- { apply elem_of_dom. rewrite Hdom. apply elem_of_set_seq. lia. }
- iDestruct (big_sepM_delete _ _ n with "Hps'") as "[Hp Hps']"; [done|].
+ iDestruct "Hps'" as "[Hps' Hp]".
iMod (own_alloc (â—E (Next p) â‹… â—¯E (Next p))) as (γE) "[Hauth Hfrag]".
{ apply excl_auth_valid. }
- iMod ("IHn" with "[] Hps'") as (γEs Hlen) "H".
- { iPureIntro.
- rewrite dom_delete_L Hdom.
- replace (S n) with (n + 1) by lia.
- rewrite set_seq_add_L /= right_id_L difference_union_distr_l_L
- difference_diag_L right_id_L.
- assert (n ∉ (set_seq 0 n:gset _)); [|set_solver].
- intros Hin%elem_of_set_seq. lia. }
+ iMod ("IHn" with "Hps'") as (γEs Hlen) "H".
iModIntro. iExists (γEs++[γE]).
- replace (S n) with (n + 1) by lia.
- rewrite replicate_add big_sepL_app app_length Hlen.
- iSplit; [done|]=> /=.
+ rewrite !app_length Hlen.
+ iSplit; [iPureIntro=>/=;lia|]=> /=.
+ rewrite replicate_add.
iSplitL "H".
{ iApply (big_sepL_impl with "H").
iIntros "!>" (i ? HSome') "(Hauth & Hfrag & Hown)".
- assert (i < n) as Hle.
+ assert (i < length ps) as Hle.
{ by apply lookup_replicate_1 in HSome' as [??]. }
- assert (delete n ps !!! i = ps !!! i) as Heq'.
- { apply lookup_total_delete_ne. lia. }
- rewrite Heq'. iFrame.
- rewrite lookup_total_app_l; [|lia]. iFrame. }
+ rewrite !lookup_total_app_l; [|lia..]. iFrame. }
rewrite replicate_length Nat.add_0_r.
- rewrite list_lookup_total_middle; [|done].
- rewrite lookup_total_alt HSome. by iFrame. }
+ simpl. rewrite right_id_L.
+ rewrite !lookup_total_app_r; [|lia..]. rewrite !Hlen.
+ rewrite Nat.sub_diag. simpl. iFrame.
+ iDestruct "Hp" as "[$ _]". }
iMod "H" as (γEs Hlen) "H".
+ set n := length ps.
iAssert (|={⊤}=>
- [∗ list] i ↦ _ ∈ replicate n (),
- [∗ list] j ↦ _ ∈ replicate n (),
+ [∗ list] i ↦ _ ∈ replicate (length ps) (),
+ [∗ list] j ↦ _ ∈ replicate (length ps) (),
∃ γt,
inv (nroot.@"p") (chan_inv γ (γEs !!! i) γt i j
- (l +â‚— (pos n i j))))%I with "[Hl]" as "IH".
+ (l +â‚— (pos (length ps) i j))))%I with "[Hl]" as "IH".
{ replace (Z.to_nat (Z.of_nat n * Z.of_nat n)) with (n*n) by lia.
iDestruct (array_to_matrix with "Hl") as "Hl".
iApply big_sepL_fupd.
@@ -273,19 +263,19 @@ Section channel.
iMod "IH" as "#IH".
iMod (inv_alloc with "Hps") as "#IHp".
iExists _,_,_,_.
- iModIntro. iSplit; [done|].
+ iModIntro.
+ iSplit.
+ { iPureIntro. done. }
iSplit.
- { iPureIntro. intros i HSome.
- apply elem_of_dom in HSome.
- rewrite Hdom in HSome.
- apply elem_of_set_seq in HSome. lia. }
- rewrite Hdom. iFrame "IHp".
+ { done. }
+ iFrame "IHp".
iApply (big_sepL_impl with "H").
iIntros "!>" (i ? HSome') "(Hauth & Hfrag & Hown)".
iSplitL.
- { iIntros (p HSome'').
- rewrite lookup_total_alt. rewrite HSome''.
- iFrame. }
+ { iIntros (p Hle' HSome'').
+ iFrame. rewrite right_id_L in HSome''.
+ rewrite (list_lookup_total_alt ps).
+ rewrite HSome''. simpl. iFrame. }
iApply big_sepL_intro.
iIntros "!>" (j ? HSome'').
assert (i < n) as Hle'.
@@ -305,40 +295,64 @@ Section channel.
iExists _, _. iFrame "#".
Qed.
- Lemma get_chan_spec cs (i:nat) ps p :
- ps !! i = Some p →
- {{{ chan_pool cs ps }}}
+ Lemma get_chan_spec cs i ps p :
+ {{{ chan_pool cs i (p::ps) }}}
get_chan cs #i
- {{{ c, RET c; c ↣ p ∗ chan_pool cs (delete i ps) }}}.
+ {{{ c, RET c; c ↣ p ∗ chan_pool cs (i+1) ps }}}.
Proof.
- iIntros (HSome Φ) "Hcs HΦ".
- iDestruct "Hcs" as (γp γEs l n -> Hle) "[#IHp Hl]".
+ iIntros (Φ) "Hcs HΦ".
+ iDestruct "Hcs" as (γp γEs n l -> <-) "[#IHp Hl]".
wp_lam. wp_pures.
- assert (i < n); [by apply Hle|].
- iDestruct (big_sepL_delete _ _ i () with "Hl") as "[[Hi #IHs] H]";
- [by apply lookup_replicate|].
- iDestruct ("Hi" with "[//]") as "(Hauth & Hown & Hp)".
+ simpl.
+ rewrite replicate_add. simpl.
+ iDestruct "Hl" as "[Hl1 [[Hi #IHs] Hl3]]". simpl.
+ iDestruct ("Hi" with "[] []") as "(Hauth & Hown & Hp)".
+ { rewrite right_id_L. rewrite replicate_length. iPureIntro. lia. }
+ { rewrite right_id_L. rewrite replicate_length.
+ rewrite Nat.sub_diag. simpl. done. }
iModIntro.
iApply "HΦ".
- iSplitR "H".
+ iSplitR "Hl1 Hl3".
{ rewrite iProto_pointsto_eq. iExists _, _, _, _, _, _.
- iSplit; [done|]. iFrame "#∗". iSplit; [|iNext; done].
+ iSplit; [done|].
+ rewrite replicate_length. rewrite right_id_L.
+ iFrame "#∗".
+ iSplit; [|iNext; done].
+ rewrite replicate_add.
iApply (big_sepL_impl with "IHs").
iIntros "!>" (???). iDestruct 1 as (γt1 γt2) "[??]".
iExists _,_,_. iFrame. }
iExists _, _, _, _. iSplit; [done|].
iSplit.
- { iPureIntro. intros i' HSome'. apply Hle.
- assert (i ≠i').
- { intros ->. rewrite lookup_delete in HSome'. by inversion HSome'. }
- by rewrite lookup_delete_ne in HSome'. }
+ { iPureIntro. lia. }
iFrame "#∗".
- iApply (big_sepL_impl with "H").
+ rewrite replicate_add.
+ simpl.
+ iSplitL "Hl1".
+ { iApply (big_sepL_impl with "Hl1").
+ iIntros "!>" (i' ? HSome'').
+ assert (i' < i).
+ { rewrite lookup_replicate in HSome''. lia. }
+ iIntros "[H $]" (p' Hle'). lia. }
+ simpl.
+ iFrame "#∗".
+ iSplitR.
+ { iIntros (p' Hle'). rewrite right_id_L in Hle'.
+ rewrite replicate_length in Hle'. lia. }
+ iApply (big_sepL_impl with "Hl3").
iIntros "!>" (i' ? HSome'').
- case_decide.
- { simplify_eq. iFrame "#".
- iIntros "_" (p' Hin). simplify_eq. by rewrite lookup_delete in Hin. }
- rewrite lookup_delete_ne; [|done]. by eauto.
+ assert (i' < length ps).
+ { rewrite lookup_replicate in HSome''. lia. }
+ iIntros "[H $]" (p' Hle' HSome).
+ iApply "H".
+ { iPureIntro. lia. }
+ iPureIntro.
+ rewrite replicate_length.
+ rewrite replicate_length in HSome.
+ replace (i + S i' - i) with (S i') by lia.
+ simpl.
+ replace (i + S i' - (i+1)) with (i') in HSome by lia.
+ done.
Qed.
Lemma vpos_spec (n i j : nat) :
@@ -363,10 +377,10 @@ Section channel.
iDestruct (iProto_le_msg_inv_r with "Hle") as (m') "#Heq".
iRewrite "Heq" in "Hown".
iAssert (▷ (▷ ⌜j < n⌠∗ iProto_own γ i (<(Send, j)> m') ∗
- iProto_ctx γ (set_seq 0 n)))%I with "[HI Hown]"
+ iProto_ctx γ n))%I with "[HI Hown]"
as "[HI [Hown Hctx]]".
{ iNext. iDestruct (iProto_target with "HI Hown") as "[Hin [$ $]]".
- iFrame. iNext. iDestruct "Hin" as %Hin. by set_solver. }
+ iFrame. }
iRewrite -"Heq" in "Hown". wp_pures. iModIntro. iFrame.
wp_smart_apply (vpos_spec); [done|]; iIntros "_".
iDestruct "HI" as %Hle.
@@ -456,9 +470,9 @@ Section channel.
iDestruct (iProto_le_msg_inv_r with "Hle") as (m') "#Heq".
iRewrite "Heq" in "Hown".
iAssert (▷ (▷ ⌜j < n⌠∗ iProto_own γ i (<(Recv, j)> m') ∗
- iProto_ctx γ (set_seq 0 n)))%I with "[HI Hown]" as "[HI [Hown Hctx]]".
+ iProto_ctx γ n))%I with "[HI Hown]" as "[HI [Hown Hctx]]".
{ iNext. iDestruct (iProto_target with "HI Hown") as "[Hin [$$]]".
- iFrame. iNext. iDestruct "Hin" as %Hin. by set_solver. }
+ iFrame. }
iRewrite -"Heq" in "Hown". wp_pures. iModIntro. iFrame.
wp_smart_apply (vpos_spec); [done|]; iIntros "_".
iDestruct "HI" as %Hle.
@@ -505,4 +519,28 @@ Section channel.
iRewrite "Hp". iFrame "#∗". iApply iProto_le_refl.
Qed.
+ Lemma iProto_le_select_l {TT1 TT2:tele} j
+ (v1 : TT1 → val) (v2 : TT2 → val) P1 P2 (p1 : TT1 → iProto Σ) (p2 : TT2 → iProto Σ) :
+ ⊢ (iProto_choice (Send, j) v1 v2 P1 P2 p1 p2) ⊑
+ (<(Send,j) @.. (tt:TT1)> MSG (InjLV (v1 tt)) {{ P1 tt }} ; p1 tt).
+ Proof.
+ rewrite /iProto_choice.
+ iApply iProto_le_trans; last first.
+ { iApply iProto_le_texist_elim_r. iIntros (x). iExists x.
+ iApply iProto_le_refl. }
+ iIntros (tt). by iExists (inl tt).
+ Qed.
+
+ Lemma iProto_le_select_r {TT1 TT2:tele} j
+ (v1 : TT1 → val) (v2 : TT2 → val) P1 P2 (p1 : TT1 → iProto Σ) (p2 : TT2 → iProto Σ) :
+ ⊢ (iProto_choice (Send, j) v1 v2 P1 P2 p1 p2) ⊑
+ (<(Send,j) @.. (tt:TT2)> MSG (InjRV (v2 tt)) {{ P2 tt }} ; p2 tt).
+ Proof.
+ rewrite /iProto_choice.
+ iApply iProto_le_trans; last first.
+ { iApply iProto_le_texist_elim_r. iIntros (x). iExists x.
+ iApply iProto_le_refl. }
+ iIntros (tt). by iExists (inr tt).
+ Qed.
+
End channel.
diff --git a/multi_actris/channel/proto.v b/multi_actris/channel/proto.v
index dbb1b16e265bc573133ee6d5180461709e85f43b..e5a2b781b7c649a66ea6594969299667b21f4f3a 100644
--- a/multi_actris/channel/proto.v
+++ b/multi_actris/channel/proto.v
@@ -173,22 +173,6 @@ Notation "< a @.. x1 .. xn > m" := (iProto_message a (∃.. x1, .. (∃.. xn, m)
(at level 200, a at level 10, x1 closed binder, xn closed binder, m at level 200,
format "< a @.. x1 .. xn > m") : proto_scope.
-Notation "<!> m" := (<Send> m) (at level 200, m at level 200) : proto_scope.
-Notation "<! x1 .. xn > m" := (<!> ∃ x1, .. (∃ xn, m) ..)
- (at level 200, x1 closed binder, xn closed binder, m at level 200,
- format "<! x1 .. xn > m") : proto_scope.
-Notation "<!.. x1 .. xn > m" := (<!> ∃.. x1, .. (∃.. xn, m) ..)
- (at level 200, x1 closed binder, xn closed binder, m at level 200,
- format "<!.. x1 .. xn > m") : proto_scope.
-
-Notation "<?> m" := (<Recv> m) (at level 200, m at level 200) : proto_scope.
-Notation "<? x1 .. xn > m" := (<?> ∃ x1, .. (∃ xn, m) ..)
- (at level 200, x1 closed binder, xn closed binder, m at level 200,
- format "<? x1 .. xn > m") : proto_scope.
-Notation "<?.. x1 .. xn > m" := (<?> ∃.. x1, .. (∃.. xn, m) ..)
- (at level 200, x1 closed binder, xn closed binder, m at level 200,
- format "<?.. x1 .. xn > m") : proto_scope.
-
Class MsgTele {Σ V} {TT : tele} (m : iMsg Σ V)
(tv : TT -t> V) (tP : TT -t> iProp Σ) (tp : TT -t> iProto Σ V) :=
msg_tele : m ≡ (∃.. x, MSG tele_app tv x {{ tele_app tP x }}; tele_app tp x)%msg.
@@ -512,8 +496,8 @@ End proto.
Global Instance iProto_inhabited {Σ V} : Inhabited (iProto Σ V) := populate END.
-Definition can_step {Σ V} (rec : gmap nat (iProto Σ V) → iProp Σ)
- (ps : gmap nat (iProto Σ V)) (i j : nat) : iProp Σ :=
+Definition can_step {Σ V} (rec : list (iProto Σ V) → iProp Σ)
+ (ps : list (iProto Σ V)) (i j : nat) : iProp Σ :=
∀ m1 m2,
(ps !!! i ≡ <(Send, j)> m1) -∗
(ps !!! j ≡ <(Recv, i)> m2) -∗
@@ -521,21 +505,21 @@ Definition can_step {Σ V} (rec : gmap nat (iProto Σ V) → iProp Σ)
∃ 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 : list (iProto Σ V)) (i j : nat) : iProp Σ :=
∀ a m, (ps !!! i ≡ <(a, j)> m) -∗ ⌜is_Some (ps !! j)âŒ.
-Definition iProto_consistent_pre {Σ V} (rec : gmap nat (iProto Σ V) → iProp Σ)
- (ps : gmap nat (iProto Σ V)) : iProp Σ :=
+Definition iProto_consistent_pre {Σ V} (rec : list (iProto Σ V) → iProp Σ)
+ (ps : list (iProto Σ V)) : iProp Σ :=
(∀ i j, valid_target ps i j) ∗ (∀ i j, can_step rec ps i j).
Global Instance iProto_consistent_pre_ne {Σ V}
- (rec : gmapO natO (iProto Σ V) -n> iPropO Σ) :
+ (rec : listO (iProto Σ V) -n> iPropO Σ) :
NonExpansive (iProto_consistent_pre rec).
Proof. rewrite /iProto_consistent_pre /can_step /valid_target. solve_proper. Qed.
Program Definition iProto_consistent_pre' {Σ V}
- (rec : gmapO natO (iProto Σ V) -n> iPropO Σ) :
- gmapO natO (iProto Σ V) -n> iPropO Σ :=
+ (rec : listO (iProto Σ V) -n> iPropO Σ) :
+ listO (iProto Σ V) -n> iPropO Σ :=
λne ps, iProto_consistent_pre (λ ps, rec ps) ps.
Local Instance iProto_consistent_pre_contractive {Σ V} : Contractive (@iProto_consistent_pre' Σ V).
@@ -544,7 +528,7 @@ Proof.
solve_contractive.
Qed.
-Definition iProto_consistent {Σ V} (ps : gmap nat (iProto Σ V)) : iProp Σ :=
+Definition iProto_consistent {Σ V} (ps : list (iProto Σ V)) : iProp Σ :=
fixpoint iProto_consistent_pre' ps.
Arguments iProto_consistent {_ _} _%proto.
@@ -555,7 +539,7 @@ Proof. solve_proper. Qed.
Global Instance iProto_consistent_proper {Σ V} : Proper ((≡) ==> (⊣⊢)) (@iProto_consistent Σ V).
Proof. solve_proper. Qed.
-Lemma iProto_consistent_unfold {Σ V} (ps : gmap nat (iProto Σ V)) :
+Lemma iProto_consistent_unfold {Σ V} (ps : list (iProto Σ V)) :
iProto_consistent ps ≡ (iProto_consistent_pre iProto_consistent) ps.
Proof.
apply: (fixpoint_unfold iProto_consistent_pre').
@@ -615,12 +599,13 @@ Definition iProto_own_frag `{!protoG Σ V} (γ : gname)
own γ (gmap_view_frag i (DfracOwn 1) (Excl' (Next p))).
Definition iProto_own_auth `{!protoG Σ V} (γ : gname)
- (ps : gmap nat (iProto Σ V)) : iProp Σ :=
- own γ (gmap_view_auth (DfracOwn 1) (((λ p, Excl' (Next p)) <$> ps) : gmap _ _)).
+ (ps : list (iProto Σ V)) : iProp Σ :=
+ own γ (gmap_view_auth (DfracOwn 1) (((λ p, Excl' (Next p)) <$>
+ (list_to_map (zip (seq 0 (length ps)) ps))) : gmap _ _)).
Definition iProto_ctx `{protoG Σ V}
- (γ : gname) (ps_dom : gset nat) : iProp Σ :=
- ∃ ps, ⌜dom ps = ps_dom⌠∗ iProto_own_auth γ ps ∗ ▷ iProto_consistent ps.
+ (γ : gname) (ps_len : nat) : iProp Σ :=
+ ∃ ps, ⌜length ps = ps_len⌠∗ iProto_own_auth γ ps ∗ ▷ iProto_consistent ps.
(** * The connective for ownership of channel ends *)
Definition iProto_own `{!protoG Σ V}
@@ -802,34 +787,34 @@ Section proto.
ps !!! i ≡ p1 -∗
p1 ⊑ p2 -∗
(∀ i' j', valid_target (<[i := p2]>ps) i' j') ∗ p1 ⊑ p2.
- Proof.
- iIntros "Hprot #HSome Hle".
- pose proof (iProto_case p1) as [Hend|Hmsg].
- { rewrite Hend. iDestruct (iProto_le_end_inv_l with "Hle") as "#H".
- iFrame "Hle".
- iIntros (i' j' a m) "Hm".
- destruct (decide (i = j')) as [->|Hneqj].
- { by rewrite lookup_insert. }
- rewrite lookup_insert_ne; [|done].
- destruct (decide (i = i')) as [->|Hneqi].
- { rewrite lookup_total_insert. iRewrite "H" in "Hm".
- by iDestruct (iProto_end_message_equivI with "Hm") as "Hm". }
- rewrite lookup_total_insert_ne; [|done].
- by iApply "Hprot". }
- destruct Hmsg as (t & n & m & Hmsg).
- setoid_rewrite Hmsg.
- iDestruct (iProto_le_msg_inv_l with "Hle") as (m2) "#Heq". iFrame "Hle".
- iIntros (i' j' a m') "Hm".
- destruct (decide (i = j')) as [->|Hneqj].
- { rewrite lookup_insert. done. }
- rewrite lookup_insert_ne; [|done].
- destruct (decide (i = i')) as [->|Hneqi].
- { rewrite lookup_total_insert. iRewrite "Heq" in "Hm".
- iDestruct (iProto_message_equivI with "Hm") as (Heq) "Hm".
- simplify_eq. by iApply "Hprot". }
- rewrite lookup_total_insert_ne; [|done].
- by iApply "Hprot".
- Qed.
+ Proof. Admitted.
+ (* iIntros "Hprot #HSome Hle". *)
+ (* pose proof (iProto_case p1) as [Hend|Hmsg]. *)
+ (* { rewrite Hend. iDestruct (iProto_le_end_inv_l with "Hle") as "#H". *)
+ (* iFrame "Hle". *)
+ (* iIntros (i' j' a m) "Hm". *)
+ (* destruct (decide (i = j')) as [->|Hneqj]. *)
+ (* { Search list_lookup_total insert. rewrite list_lookup_total_insert. ; [done|]. lia. done. } *)
+ (* rewrite lookup_insert_ne; [|done]. *)
+ (* destruct (decide (i = i')) as [->|Hneqi]. *)
+ (* { rewrite lookup_total_insert. iRewrite "H" in "Hm". *)
+ (* by iDestruct (iProto_end_message_equivI with "Hm") as "Hm". } *)
+ (* rewrite lookup_total_insert_ne; [|done]. *)
+ (* by iApply "Hprot". } *)
+ (* destruct Hmsg as (t & n & m & Hmsg). *)
+ (* setoid_rewrite Hmsg. *)
+ (* iDestruct (iProto_le_msg_inv_l with "Hle") as (m2) "#Heq". iFrame "Hle". *)
+ (* iIntros (i' j' a m') "Hm". *)
+ (* destruct (decide (i = j')) as [->|Hneqj]. *)
+ (* { rewrite lookup_insert. done. } *)
+ (* rewrite lookup_insert_ne; [|done]. *)
+ (* destruct (decide (i = i')) as [->|Hneqi]. *)
+ (* { rewrite lookup_total_insert. iRewrite "Heq" in "Hm". *)
+ (* iDestruct (iProto_message_equivI with "Hm") as (Heq) "Hm". *)
+ (* simplify_eq. by iApply "Hprot". } *)
+ (* rewrite lookup_total_insert_ne; [|done]. *)
+ (* by iApply "Hprot". *)
+ (* Qed. *)
Lemma iProto_consistent_le ps i p1 p2 :
iProto_consistent ps -∗
@@ -847,7 +832,7 @@ Section proto.
iFrame.
iIntros (i' j' m1 m2) "#Hm1 #Hm2".
destruct (decide (i = i')) as [<-|Hneq].
- { rewrite lookup_total_insert.
+ { rewrite list_lookup_total_insert; [|admit].
pose proof (iProto_case p2) as [Hend|Hmsg].
{ setoid_rewrite Hend. rewrite iProto_end_message_equivI. done. }
destruct Hmsg as (a&?&m&Hmsg).
@@ -865,23 +850,23 @@ Section proto.
iDestruct "Hle" as (m') "[#Heq H]".
iDestruct ("H" with "Hm1'") as (p') "[Hle H]".
destruct (decide (i = j')) as [<-|Hneq].
- { rewrite lookup_total_insert. rewrite iProto_message_equivI.
- iDestruct "Hm2" as "[%Heq _]". done. }
+ { rewrite list_lookup_total_insert. rewrite iProto_message_equivI.
+ iDestruct "Hm2" as "[%Heq _]". done. admit. }
iDestruct ("Hprot" $!i j' with "[] [] H") as "Hprot".
- { iRewrite -"Heq". rewrite !lookup_total_alt. iRewrite "HSome". done. }
- { rewrite lookup_total_insert_ne; [|done]. done. }
+ { iRewrite -"Heq". rewrite !list_lookup_total_alt. iRewrite "HSome". done. }
+ { rewrite list_lookup_total_insert_ne; [|done]. done. }
iDestruct "Hprot" as (p'') "[Hm Hprot]".
iExists p''. iFrame.
iNext.
iDestruct ("IH" with "Hprot Hle [HSome]") as "HI".
- { by rewrite lookup_total_insert. }
+ { rewrite list_lookup_total_insert; [done|]. admit. }
iClear "IH Hm1 Hm2 Heq".
- rewrite insert_insert.
- rewrite (insert_commute _ j' i); [|done].
- rewrite insert_insert. done. }
- rewrite lookup_total_insert_ne; [|done].
+ rewrite list_insert_insert.
+ rewrite (list_insert_commute _ j' i); [|done].
+ rewrite list_insert_insert. done. }
+ rewrite list_lookup_total_insert_ne; [|done].
destruct (decide (i = j')) as [<-|Hneq'].
- { rewrite lookup_total_insert.
+ { rewrite list_lookup_total_insert.
pose proof (iProto_case p2) as [Hend|Hmsg].
{ setoid_rewrite Hend. rewrite iProto_end_message_equivI. done. }
destruct Hmsg as (a&?&m&Hmsg).
@@ -897,31 +882,31 @@ Section proto.
iDestruct "Hle" as (m') "[#Heq Hle]".
iDestruct ("Hprot" $!i' with "[] [] Hm1'") as "Hprot".
{ done. }
- { rewrite !lookup_total_alt. iRewrite "HSome". done. }
+ { rewrite !list_lookup_total_alt. iRewrite "HSome". done. }
iDestruct ("Hprot") as (p') "[Hm1' Hprot]".
iDestruct ("Hle" with "Hm1'") as (p2') "[Hle Hm']".
iSpecialize ("Hm2" $! v (Next p2')).
iExists p2'.
iRewrite -"Hm2". iFrame.
iDestruct ("IH" with "Hprot Hle []") as "HI".
- { iPureIntro. rewrite lookup_total_insert_ne; [|done].
- rewrite lookup_total_insert. done. }
- rewrite insert_commute; [|done].
- rewrite !insert_insert. done. }
- rewrite lookup_total_insert_ne; [|done].
+ { iPureIntro. rewrite list_lookup_total_insert_ne; [|done].
+ rewrite list_lookup_total_insert. done. admit. }
+ rewrite list_insert_commute; [|done].
+ rewrite !list_insert_insert. done. admit. }
+ rewrite list_lookup_total_insert_ne; [|done].
iIntros (v p) "Hm1'".
iDestruct ("Hprot" $!i' j' with "[//] [//] Hm1'") as "Hprot".
iDestruct "Hprot" as (p') "[Hm2' Hprot]".
iExists p'. iFrame.
iNext.
- rewrite (insert_commute _ j' i); [|done].
- rewrite (insert_commute _ i' i); [|done].
+ rewrite (list_insert_commute _ j' i); [|done].
+ rewrite (list_insert_commute _ i' i); [|done].
iApply ("IH" with "Hprot Hle []").
- rewrite lookup_total_insert_ne; [|done].
- rewrite lookup_total_insert_ne; [|done].
+ rewrite list_lookup_total_insert_ne; [|done].
+ rewrite list_lookup_total_insert_ne; [|done].
done.
- Qed.
-
+ Admitted.
+
Lemma iProto_le_send i m1 m2 :
(∀ v p2', iMsg_car m2 v (Next p2') -∗ ∃ p1',
▷ (p1' ⊑ p2') ∗ iMsg_car m1 v (Next p1')) -∗
@@ -1156,16 +1141,16 @@ Section proto.
Lemma iProto_own_auth_agree γ ps i p :
iProto_own_auth γ ps -∗ iProto_own_frag γ i p -∗ ▷ (ps !!! i ≡ p).
- Proof.
- iIntros "Hâ— Hâ—¯".
- iDestruct (own_valid_2 with "H◠H◯") as "H✓".
- rewrite gmap_view_both_validI.
- iDestruct "H✓" as "[_ [H1 H2]]".
- rewrite lookup_total_alt lookup_fmap.
- destruct (ps !! i); last first.
- { by rewrite !option_equivI. }
- simpl. rewrite !option_equivI excl_equivI. by iNext.
- Qed.
+ Proof. Admitted.
+ (* iIntros "Hâ— Hâ—¯". *)
+ (* iDestruct (own_valid_2 with "H◠H◯") as "H✓". *)
+ (* rewrite gmap_view_both_validI. *)
+ (* iDestruct "H✓" as "[_ [H1 H2]]". *)
+ (* rewrite list_lookup_total_alt lookup_fmap. *)
+ (* destruct (ps !! i); last first. *)
+ (* { rewrite !option_equivI. } *)
+ (* simpl. rewrite !option_equivI excl_equivI. by iNext. *)
+ (* Qed. *)
Lemma iProto_own_auth_update γ ps i p p' :
iProto_own_auth γ ps -∗ iProto_own_frag γ i p ==∗
@@ -1174,25 +1159,24 @@ Section proto.
iIntros "Hâ— Hâ—¯".
iMod (own_update_2 with "Hâ— Hâ—¯") as "[H1 H2]"; [|iModIntro].
{ eapply (gmap_view_replace _ _ _ (Excl' (Next p'))). done. }
- iFrame. rewrite -fmap_insert. done.
- Qed.
-
+ iFrame. rewrite -fmap_insert. Admitted.
+
Lemma iProto_own_auth_alloc ps :
- ⊢ |==> ∃ γ, iProto_own_auth γ ps ∗ [∗ map] i ↦p ∈ ps, iProto_own γ i p.
- Proof.
- iMod (own_alloc (gmap_view_auth (DfracOwn 1) ∅)) as (γ) "Hauth".
- { apply gmap_view_auth_valid. }
- iExists γ.
- iInduction ps as [|i p ps Hin] "IH" using map_ind.
- { iModIntro. iFrame. by iApply big_sepM_empty. }
- iMod ("IH" with "Hauth") as "[Hauth Hfrags]".
- rewrite big_sepM_insert; [|done]. iFrame "Hfrags".
- iMod (own_update with "Hauth") as "[Hauth Hfrag]".
- { apply (gmap_view_alloc _ i (DfracOwn 1) (Excl' (Next p))); [|done|done].
- by rewrite lookup_fmap Hin. }
- iModIntro. rewrite -fmap_insert. iFrame.
- iExists _. iFrame. iApply iProto_le_refl.
- Qed.
+ ⊢ |==> ∃ γ, iProto_own_auth γ ps ∗ [∗ list] i ↦p ∈ ps, iProto_own γ i p.
+ Proof. Admitted.
+ (* iMod (own_alloc (gmap_view_auth (DfracOwn 1) ∅)) as (γ) "Hauth". *)
+ (* { apply gmap_view_auth_valid. } *)
+ (* iExists γ. *)
+ (* iInduction ps as [|i p ps Hin] "IH" using map_ind. *)
+ (* { iModIntro. iFrame. by iApply big_sepM_empty. } *)
+ (* iMod ("IH" with "Hauth") as "[Hauth Hfrags]". *)
+ (* rewrite big_sepM_insert; [|done]. iFrame "Hfrags". *)
+ (* iMod (own_update with "Hauth") as "[Hauth Hfrag]". *)
+ (* { apply (gmap_view_alloc _ i (DfracOwn 1) (Excl' (Next p))); [|done|done]. *)
+ (* by rewrite lookup_fmap Hin. } *)
+ (* iModIntro. rewrite -fmap_insert. iFrame. *)
+ (* iExists _. iFrame. iApply iProto_le_refl. *)
+ (* Qed. *)
Lemma iProto_own_le γ s p1 p2 :
iProto_own γ s p1 -∗ ▷ (p1 ⊑ p2) -∗ iProto_own γ s p2.
@@ -1203,7 +1187,7 @@ Section proto.
Lemma iProto_init ps :
▷ iProto_consistent ps -∗
- |==> ∃ γ, iProto_ctx γ (dom ps) ∗ [∗ map] i ↦p ∈ ps, iProto_own γ i p.
+ |==> ∃ γ, iProto_ctx γ (length ps) ∗ [∗ list] i ↦p ∈ ps, iProto_own γ i p.
Proof.
iIntros "Hconsistent".
iMod iProto_own_auth_alloc as (γ) "[Hauth Hfrags]".
@@ -1227,28 +1211,28 @@ Section proto.
iDestruct (iProto_own_auth_agree with "Hauth Hj") as "#Hpj".
iDestruct (own_prot_idx with "Hi Hj") as %Hneq.
iAssert (▷ (<[i:=<(Send, j)> m1]>ps !!! j ≡ pj))%I as "Hpj'".
- { by rewrite lookup_total_insert_ne. }
+ { by rewrite list_lookup_total_insert_ne. }
iAssert (▷ (⌜is_Some (ps !! i)⌠∗ (pi ⊑ (<(Send, j)> m1))))%I with "[Hile]"
as "[Hi' Hile]".
{ iNext. iDestruct (iProto_le_msg_inv_r with "Hile") as (m) "#Heq".
- iFrame. iRewrite "Heq" in "Hpi". rewrite lookup_total_alt.
+ iFrame. iRewrite "Heq" in "Hpi". rewrite list_lookup_total_alt.
destruct (ps !! i); [done|].
iDestruct (iProto_end_message_equivI with "Hpi") as "[]". }
iAssert (▷ (⌜is_Some (ps !! j)⌠∗ (pj ⊑ (<(Recv, i)> m2))))%I with "[Hjle]"
as "[Hj' Hjle]".
{ iNext. iDestruct (iProto_le_msg_inv_r with "Hjle") as (m) "#Heq".
- iFrame. iRewrite "Heq" in "Hpj". rewrite !lookup_total_alt.
+ iFrame. iRewrite "Heq" in "Hpj". rewrite !list_lookup_total_alt.
destruct (ps !! j); [done|].
iDestruct (iProto_end_message_equivI with "Hpj") as "[]". }
iDestruct (iProto_consistent_le with "Hconsistent Hpi Hile") as "Hconsistent".
iDestruct (iProto_consistent_le with "Hconsistent Hpj' Hjle") as "Hconsistent".
iDestruct (iProto_consistent_step _ _ _ i j with "Hconsistent [] [] [Hm //]") as
(p2) "[Hm2 Hconsistent]".
- { rewrite lookup_total_insert_ne; [|done].
- rewrite lookup_total_insert_ne; [|done].
- by rewrite lookup_total_insert. }
- { rewrite lookup_total_insert_ne; [|done].
- by rewrite lookup_total_insert. }
+ { rewrite list_lookup_total_insert_ne; [|done].
+ rewrite list_lookup_total_insert_ne; [|done].
+ rewrite list_lookup_total_insert; [done|]. admit. }
+ { rewrite list_lookup_total_insert_ne; [|done].
+ rewrite list_lookup_total_insert; [done|]. admit. }
iMod (iProto_own_auth_update _ _ _ _ p2 with "Hauth Hj") as "[Hauth Hj]".
iMod (iProto_own_auth_update _ _ _ _ p1 with "Hauth Hi") as "[Hauth Hi]".
iIntros "!>!>". iExists p2. iFrame "Hm2".
@@ -1256,17 +1240,18 @@ Section proto.
iSplitL "Hconsistent Hauth".
{ iExists (<[i:=p1]> (<[j:=p2]> ps)).
iSplit.
- { rewrite !dom_insert_lookup_L; [done..|by rewrite lookup_insert_ne]. }
- iFrame. rewrite insert_insert.
- rewrite insert_commute; [|done]. rewrite insert_insert.
- by rewrite insert_commute; [|done]. }
+ { admit.
+ (* rewrite !dom_insert_lookup_L; [done..|by rewrite lookup_insert_ne]. *)}
+ iFrame. rewrite list_insert_insert.
+ rewrite list_insert_commute; [|done]. rewrite list_insert_insert.
+ by rewrite list_insert_commute; [|done]. }
iSplitL "Hi"; iExists _; iFrame; iApply iProto_le_refl.
- Qed.
+ Admitted.
Lemma iProto_target γ ps_dom i a j m :
iProto_ctx γ ps_dom -∗
iProto_own γ i (<(a, j)> m) -∗
- â–· (⌜j ∈ ps_domâŒ) ∗ iProto_ctx γ ps_dom ∗ iProto_own γ i (<(a, j)> m).
+ â–· (⌜j < ps_domâŒ) ∗ iProto_ctx γ ps_dom ∗ iProto_own γ i (<(a, j)> m).
Proof.
iIntros "Hctx Hown".
rewrite /iProto_ctx /iProto_own.
@@ -1280,9 +1265,9 @@ Section proto.
iDestruct (iProto_consistent_target with "Hps Hi") as "#$". by iFrame. }
iSplitL "HSome".
{ iNext. iDestruct "HSome" as %Heq.
- iPureIntro. simplify_eq. by apply elem_of_dom. }
+ iPureIntro. simplify_eq. admit. }
iSplitL "Hauth Hps"; iExists _; by iFrame.
- Qed.
+ Admitted.
(* (** The instances below make it possible to use the tactics [iIntros], *)
(* [iExist], [iSplitL]/[iSplitR], [iFrame] and [iModIntro] on [iProto_le] goals. *) *)