From 9a579d2d37f1249eb4ea8872b3d6646105dfee5e Mon Sep 17 00:00:00 2001
From: Jesper Bengtson <jesper@bengtson.at>
Date: Fri, 21 Aug 2020 13:05:11 +0200
Subject: [PATCH] added branch existance check
---
theories/channel/channel.v | 13 +++++++------
1 file changed, 7 insertions(+), 6 deletions(-)
diff --git a/theories/channel/channel.v b/theories/channel/channel.v
index 6482abe..6e72e0c 100644
--- a/theories/channel/channel.v
+++ b/theories/channel/channel.v
@@ -111,7 +111,7 @@ Notation "c ↣ p" := (iProto_mapsto c p)
(at level 20, format "c ↣ p").
Definition iProto_nchoice {Σ} (a : action) (branches : gmap Z (iProp Σ * iProto Σ)) : iProto Σ :=
- (<a @ (n : Z)> MSG #n {{fst (branches !!! n)}}; snd (branches !!! n))%proto.
+ (<a @ (n : Z)> MSG #n {{⌜is_Some (branches !! n)⌝ ∗ (branches !!! n).1}}; (branches !!! n).2)%proto.
Definition iProto_choice {Σ} (a : action) (P1 P2 : iProp Σ)
(p1 p2 : iProto Σ) : iProto Σ :=
@@ -319,27 +319,28 @@ Section channel.
Qed.
Lemma nselect_spec c (n : Z) branches :
- {{{ c ↣ iProto_nchoice Send branches ∗ (branches !!! n).1 }}}
+ {{{ c ↣ iProto_nchoice Send branches ∗ ⌜is_Some (branches !! n)⌝ ∗ (branches !!! n).1 }}}
send c #n
{{{ RET #(); c ↣ (branches !!! n).2 }}}.
Proof.
rewrite /iProto_nchoice. iIntros (Φ) "[Hc HP] HΦ".
iApply (send_spec with "[Hc HP] HΦ").
iApply (iProto_mapsto_le with "Hc").
- iIntros "!>". iExists n. by iFrame "HP".
+ iIntros "!>". iExists n.
+ by iFrame "HP".
Qed.
Lemma nbranch_spec c branches :
{{{ c ↣ (iProto_nchoice Recv branches) }}}
recv c
- {{{ (n : Z) , RET #n; c ↣ (branches !!! n).2 ∗ (branches !!! n).1 }}}.
+ {{{ (n : Z) , RET #n; c ↣ (branches !!! n).2 ∗ ⌜is_Some (branches !! n)⌝ ∗ (branches !!! n).1 }}}.
Proof.
rewrite /iProto_nchoice. iIntros (Φ) "Hc HΦ".
iApply (recv_spec _ (tele_app _)
- (tele_app (TT := [tele _ : Z]) (λ n, (branches !!! n).1))%I
+ (tele_app (TT := [tele _ : Z]) (λ n, ⌜is_Some (branches !! n)⌝ ∗ (branches !!! n).1))%I
(tele_app _) with "[Hc]").
{ iApply (iProto_mapsto_le with "Hc").
- iIntros "!> /=" (n) "HP". iExists n. by iSplitL. }
+ iIntros "!> /=" (n) "[H1 H2]". iExists n. iSplitL; by auto. }
rewrite -bi_tforall_forall.
iIntros "!>" (n) "[Hc H]". iApply "HΦ". iFrame.
Qed.
--
GitLab