Commit fc30ca08 authored by Robbert Krebbers's avatar Robbert Krebbers

Generalize update tactics into iMod and iModIntro for modalities.

There are now two proof mode tactics for dealing with modalities:

- `iModIntro` : introduction of a modality
- `iMod pm_trm as (x1 ... xn) "ipat"` : eliminate a modality

The behavior of these tactics can be controlled by instances of the `IntroModal`
and `ElimModal` type class. We have declared instances for later, except 0,
basic updates and fancy updates. The tactic `iMod` is flexible enough that it
can also eliminate an updates around a weakest pre, and so forth.

The corresponding introduction patterns of these tactics are `!>` and `>`.

These tactics replace the tactics `iUpdIntro`, `iUpd` and `iTimeless`.

Source of backwards incompatability: the introduction pattern `!>` is used for
introduction of arbitrary modalities. It used to introduce laters by stripping
of a later of each hypotheses.
parent 9bc0a38b
...@@ -98,8 +98,19 @@ Separating logic specific tactics ...@@ -98,8 +98,19 @@ Separating logic specific tactics
- `iCombine "H1" "H2" as "H"` : turns `H1 : P1` and `H2 : P2` into - `iCombine "H1" "H2" as "H"` : turns `H1 : P1` and `H2 : P2` into
`H : P1 ★ P2`. `H : P1 ★ P2`.
Modalities
----------
- `iModIntro` : introduction of a modality that is an instance of the
`IntoModal` type class. Instances include: later, except 0, basic update and
fancy update.
- `iMod pm_trm as (x1 ... xn) "ipat"` : eliminate a modality `pm_trm` that is
an instance of the `ElimModal` type class. Instances include: later, except 0,
basic update and fancy update.
The later modality The later modality
------------------ ------------------
- `iNext` : introduce a later by stripping laters from all hypotheses. - `iNext` : introduce a later by stripping laters from all hypotheses.
- `iLöb as "IH" forall (x1 ... xn)` : perform Löb induction by generating a - `iLöb as "IH" forall (x1 ... xn)` : perform Löb induction by generating a
hypothesis `IH : ▷ goal`. The tactic generalizes over the Coq level variables hypothesis `IH : ▷ goal`. The tactic generalizes over the Coq level variables
...@@ -108,6 +119,7 @@ The later modality ...@@ -108,6 +119,7 @@ The later modality
Induction Induction
--------- ---------
- `iInduction x as cpat "IH" forall (x1 ... xn) "selpat"` : perform induction on - `iInduction x as cpat "IH" forall (x1 ... xn) "selpat"` : perform induction on
the Coq term `x`. The Coq introduction pattern is used to name the introduced the Coq term `x`. The Coq introduction pattern is used to name the introduced
variables. The induction hypotheses are inserted into the persistent context variables. The induction hypotheses are inserted into the persistent context
...@@ -124,13 +136,8 @@ Rewriting ...@@ -124,13 +136,8 @@ Rewriting
Iris Iris
---- ----
- `iUpdIntro` : introduction of an update modality. - `iInv N as (x1 ... xn) "ipat" "Hclose"` : open the invariant `N`, the update
- `iUpd pm_trm as (x1 ... xn) "ipat"` : run an update modality `pm_trm` (if the for closing the invariant is put in a hypothesis named `Hclose`.
goal permits, i.e. it can be expanded to an update modality.
- `iInv N as (x1 ... xn) "ipat"` : open the invariant `N`.
- `iTimeless "H"` : strip a later of a timeless hypothesis `H` (if the goal
permits, i.e. it is a later, True now, update modality, or a weakest
precondition).
Miscellaneous Miscellaneous
------------- -------------
...@@ -170,8 +177,7 @@ _introduction patterns_: ...@@ -170,8 +177,7 @@ _introduction patterns_:
- `[]` : false elimination. - `[]` : false elimination.
- `%` : move the hypothesis to the pure Coq context (anonymously). - `%` : move the hypothesis to the pure Coq context (anonymously).
- `# ipat` : move the hypothesis to the persistent context. - `# ipat` : move the hypothesis to the persistent context.
- `> ipat` : remove a later of a timeless hypothesis (if the goal permits). - `> ipat` : eliminate a modality (if the goal permits).
- `==> ipat` : run an update modality (if the goal permits).
Apart from this, there are the following introduction patterns that can only Apart from this, there are the following introduction patterns that can only
appear at the top level: appear at the top level:
...@@ -181,8 +187,7 @@ appear at the top level: ...@@ -181,8 +187,7 @@ appear at the top level:
previous pattern, e.g., `{$H1 H2 $H3}`). previous pattern, e.g., `{$H1 H2 $H3}`).
- `!%` : introduce a pure goal (and leave the proof mode). - `!%` : introduce a pure goal (and leave the proof mode).
- `!#` : introduce an always modality (given that the spatial context is empty). - `!#` : introduce an always modality (given that the spatial context is empty).
- `!>` : introduce a later (which strips laters from all hypotheses). - `!>` : introduce a modality.
- `!==>` : introduce an update modality
- `/=` : perform `simpl`. - `/=` : perform `simpl`.
- `*` : introduce all universal quantifiers. - `*` : introduce all universal quantifiers.
- `**` : introduce all universal quantifiers, as well as all arrows and wands. - `**` : introduce all universal quantifiers, as well as all arrows and wands.
...@@ -222,9 +227,9 @@ _specification patterns_ to express splitting of hypotheses: ...@@ -222,9 +227,9 @@ _specification patterns_ to express splitting of hypotheses:
framed in the generated goal. framed in the generated goal.
- `[-H1 ... Hn]` : negated form of the above pattern. This pattern does not - `[-H1 ... Hn]` : negated form of the above pattern. This pattern does not
accept hypotheses prefixed with a `$`. accept hypotheses prefixed with a `$`.
- `==>[H1 ... Hn]` : same as the above pattern, but can only be used if the goal - `>[H1 ... Hn]` : same as the above pattern, but can only be used if the goal
is an update modality, in which case the update modality will be kept in the is a modality, in which case the modality will be kept in the generated goal
goal of the premise too. for the premise will be wrapped into the modality.
- `[#]` : This pattern can be used when eliminating `P -★ Q` with `P` - `[#]` : This pattern can be used when eliminating `P -★ Q` with `P`
persistent. Using this pattern, all hypotheses are available in the goal for persistent. Using this pattern, all hypotheses are available in the goal for
`P`, as well the remaining goal. `P`, as well the remaining goal.
......
...@@ -20,7 +20,7 @@ Definition heap_adequacy Σ `{heapPreG Σ} e σ φ : ...@@ -20,7 +20,7 @@ Definition heap_adequacy Σ `{heapPreG Σ} e σ φ :
adequate e σ φ. adequate e σ φ.
Proof. Proof.
intros Hwp; eapply (wp_adequacy Σ); iIntros (?) "Hσ". intros Hwp; eapply (wp_adequacy Σ); iIntros (?) "Hσ".
iUpd (auth_alloc to_heap _ heapN _ σ with "[Hσ]") as (γ) "[Hh _]";[|by iNext|]. iMod (auth_alloc to_heap _ heapN _ σ with "[Hσ]") as (γ) "[Hh _]";[|by iNext|].
{ exact: to_heap_valid. } { exact: to_heap_valid. }
set (Hheap := HeapG _ _ _ γ). set (Hheap := HeapG _ _ _ γ).
iApply (Hwp _). by rewrite /heap_ctx. iApply (Hwp _). by rewrite /heap_ctx.
......
...@@ -109,10 +109,10 @@ Section heap. ...@@ -109,10 +109,10 @@ Section heap.
heap_ctx ( l, l v ={E}= Φ (LitV (LitLoc l))) WP Alloc e @ E {{ Φ }}. heap_ctx ( l, l v ={E}= Φ (LitV (LitLoc l))) WP Alloc e @ E {{ Φ }}.
Proof. Proof.
iIntros (<-%of_to_val ?) "[#Hinv HΦ]". rewrite /heap_ctx. iIntros (<-%of_to_val ?) "[#Hinv HΦ]". rewrite /heap_ctx.
iUpd (auth_empty heap_name) as "Ha". iMod (auth_empty heap_name) as "Ha".
iUpd (auth_open with "[$Hinv $Ha]") as (σ) "(%&Hσ&Hcl)"; first done. iMod (auth_open with "[$Hinv $Ha]") as (σ) "(%&Hσ&Hcl)"; first done.
iApply wp_alloc_pst. iFrame "Hσ". iNext. iIntros (l) "[% Hσ] !==>". iApply wp_alloc_pst. iFrame "Hσ". iNext. iIntros (l) "[% Hσ] !>".
iUpd ("Hcl" with "* [Hσ]") as "Ha". iMod ("Hcl" with "* [Hσ]") as "Ha".
{ iFrame. iPureIntro. rewrite to_heap_insert. { iFrame. iPureIntro. rewrite to_heap_insert.
eapply alloc_singleton_local_update; by auto using lookup_to_heap_None. } eapply alloc_singleton_local_update; by auto using lookup_to_heap_None. }
iApply "HΦ". by rewrite heap_mapsto_eq /heap_mapsto_def. iApply "HΦ". by rewrite heap_mapsto_eq /heap_mapsto_def.
...@@ -125,10 +125,10 @@ Section heap. ...@@ -125,10 +125,10 @@ Section heap.
Proof. Proof.
iIntros (?) "[#Hinv [>Hl HΦ]]". iIntros (?) "[#Hinv [>Hl HΦ]]".
rewrite /heap_ctx heap_mapsto_eq /heap_mapsto_def. rewrite /heap_ctx heap_mapsto_eq /heap_mapsto_def.
iUpd (auth_open with "[$Hinv $Hl]") as (σ) "(%&Hσ&Hcl)"; first done. iMod (auth_open with "[$Hinv $Hl]") as (σ) "(%&Hσ&Hcl)"; first done.
iApply (wp_load_pst _ σ); first eauto using heap_singleton_included. iApply (wp_load_pst _ σ); first eauto using heap_singleton_included.
iIntros "{$Hσ} !> Hσ !==>". iUpd ("Hcl" with "* [Hσ]") as "Ha"; first eauto. iIntros "{$Hσ}"; iNext; iIntros "Hσ !>".
by iApply "HΦ". iMod ("Hcl" with "* [Hσ]") as "Ha"; first eauto. by iApply "HΦ".
Qed. Qed.
Lemma wp_store E l v' e v Φ : Lemma wp_store E l v' e v Φ :
...@@ -138,9 +138,9 @@ Section heap. ...@@ -138,9 +138,9 @@ Section heap.
Proof. Proof.
iIntros (<-%of_to_val ?) "[#Hinv [>Hl HΦ]]". iIntros (<-%of_to_val ?) "[#Hinv [>Hl HΦ]]".
rewrite /heap_ctx heap_mapsto_eq /heap_mapsto_def. rewrite /heap_ctx heap_mapsto_eq /heap_mapsto_def.
iUpd (auth_open with "[$Hinv $Hl]") as (σ) "(%&Hσ&Hcl)"; first done. iMod (auth_open with "[$Hinv $Hl]") as (σ) "(%&Hσ&Hcl)"; first done.
iApply (wp_store_pst _ σ); first eauto using heap_singleton_included. iApply (wp_store_pst _ σ); first eauto using heap_singleton_included.
iIntros "{$Hσ} !> Hσ !==>". iUpd ("Hcl" with "* [Hσ]") as "Ha". iIntros "{$Hσ}"; iNext; iIntros "Hσ !>". iMod ("Hcl" with "* [Hσ]") as "Ha".
{ iFrame. iPureIntro. rewrite to_heap_insert. { iFrame. iPureIntro. rewrite to_heap_insert.
eapply singleton_local_update, exclusive_local_update; last done. eapply singleton_local_update, exclusive_local_update; last done.
by eapply heap_singleton_included'. } by eapply heap_singleton_included'. }
...@@ -154,10 +154,10 @@ Section heap. ...@@ -154,10 +154,10 @@ Section heap.
Proof. Proof.
iIntros (<-%of_to_val <-%of_to_val ??) "[#Hinv [>Hl HΦ]]". iIntros (<-%of_to_val <-%of_to_val ??) "[#Hinv [>Hl HΦ]]".
rewrite /heap_ctx heap_mapsto_eq /heap_mapsto_def. rewrite /heap_ctx heap_mapsto_eq /heap_mapsto_def.
iUpd (auth_open with "[$Hinv $Hl]") as (σ) "(%&Hσ&Hcl)"; first done. iMod (auth_open with "[$Hinv $Hl]") as (σ) "(%&Hσ&Hcl)"; first done.
iApply (wp_cas_fail_pst _ σ); [eauto using heap_singleton_included|done|]. iApply (wp_cas_fail_pst _ σ); [eauto using heap_singleton_included|done|].
iIntros "{$Hσ} !> Hσ !==>". iUpd ("Hcl" with "* [Hσ]") as "Ha"; first eauto. iIntros "{$Hσ}"; iNext; iIntros "Hσ !>".
by iApply "HΦ". iMod ("Hcl" with "* [Hσ]") as "Ha"; first eauto. by iApply "HΦ".
Qed. Qed.
Lemma wp_cas_suc E l e1 v1 e2 v2 Φ : Lemma wp_cas_suc E l e1 v1 e2 v2 Φ :
...@@ -167,9 +167,9 @@ Section heap. ...@@ -167,9 +167,9 @@ Section heap.
Proof. Proof.
iIntros (<-%of_to_val <-%of_to_val ?) "[#Hinv [>Hl HΦ]]". iIntros (<-%of_to_val <-%of_to_val ?) "[#Hinv [>Hl HΦ]]".
rewrite /heap_ctx heap_mapsto_eq /heap_mapsto_def. rewrite /heap_ctx heap_mapsto_eq /heap_mapsto_def.
iUpd (auth_open with "[$Hinv $Hl]") as (σ) "(%&Hσ&Hcl)"; first done. iMod (auth_open with "[$Hinv $Hl]") as (σ) "(%&Hσ&Hcl)"; first done.
iApply (wp_cas_suc_pst _ σ); first eauto using heap_singleton_included. iApply (wp_cas_suc_pst _ σ); first eauto using heap_singleton_included.
iIntros "{$Hσ} !> Hσ !==>". iUpd ("Hcl" with "* [Hσ]") as "Ha". iIntros "{$Hσ}"; iNext; iIntros "Hσ !>". iMod ("Hcl" with "* [Hσ]") as "Ha".
{ iFrame. iPureIntro. rewrite to_heap_insert. { iFrame. iPureIntro. rewrite to_heap_insert.
eapply singleton_local_update, exclusive_local_update; last done. eapply singleton_local_update, exclusive_local_update; last done.
by eapply heap_singleton_included'. } by eapply heap_singleton_included'. }
......
...@@ -97,22 +97,22 @@ Lemma newbarrier_spec (P : iProp Σ) (Φ : val → iProp Σ) : ...@@ -97,22 +97,22 @@ Lemma newbarrier_spec (P : iProp Σ) (Φ : val → iProp Σ) :
Proof. Proof.
iIntros (HN) "[#? HΦ]". iIntros (HN) "[#? HΦ]".
rewrite /newbarrier /=. wp_seq. wp_alloc l as "Hl". rewrite /newbarrier /=. wp_seq. wp_alloc l as "Hl".
iApply ("HΦ" with "==>[-]"). iApply ("HΦ" with ">[-]").
iUpd (saved_prop_alloc (F:=idCF) P) as (γ) "#?". iMod (saved_prop_alloc (F:=idCF) P) as (γ) "#?".
iUpd (sts_alloc (barrier_inv l P) _ N (State Low {[ γ ]}) with "[-]") iMod (sts_alloc (barrier_inv l P) _ N (State Low {[ γ ]}) with "[-]")
as (γ') "[#? Hγ']"; eauto. as (γ') "[#? Hγ']"; eauto.
{ iNext. rewrite /barrier_inv /=. iFrame. { iNext. rewrite /barrier_inv /=. iFrame.
iExists (const P). rewrite !big_sepS_singleton /=. eauto. } iExists (const P). rewrite !big_sepS_singleton /=. eauto. }
iAssert (barrier_ctx γ' l P)%I as "#?". iAssert (barrier_ctx γ' l P)%I as "#?".
{ rewrite /barrier_ctx. by repeat iSplit. } { rewrite /barrier_ctx. by repeat iSplit. }
iAssert (sts_ownS γ' (i_states γ) {[Change γ]} iAssert (sts_ownS γ' (i_states γ) {[Change γ]}
sts_ownS γ' low_states {[Send]})%I with "==>[-]" as "[Hr Hs]". sts_ownS γ' low_states {[Send]})%I with ">[-]" as "[Hr Hs]".
{ iApply sts_ownS_op; eauto using i_states_closed, low_states_closed. { iApply sts_ownS_op; eauto using i_states_closed, low_states_closed.
- set_solver. - set_solver.
- iApply (sts_own_weaken with "Hγ'"); - iApply (sts_own_weaken with "Hγ'");
auto using sts.closed_op, i_states_closed, low_states_closed; auto using sts.closed_op, i_states_closed, low_states_closed;
abstract set_solver. } abstract set_solver. }
iUpdIntro. rewrite /recv /send. iSplitL "Hr". iModIntro. rewrite /recv /send. iSplitL "Hr".
- iExists γ', P, P, γ. iFrame. auto. - iExists γ', P, P, γ. iFrame. auto.
- auto. - auto.
Qed. Qed.
...@@ -122,14 +122,14 @@ Lemma signal_spec l P (Φ : val → iProp Σ) : ...@@ -122,14 +122,14 @@ Lemma signal_spec l P (Φ : val → iProp Σ) :
Proof. Proof.
rewrite /signal /send /barrier_ctx /=. rewrite /signal /send /barrier_ctx /=.
iIntros "(Hs&HP&HΦ)"; iDestruct "Hs" as (γ) "[#(%&Hh&Hsts) Hγ]". wp_let. iIntros "(Hs&HP&HΦ)"; iDestruct "Hs" as (γ) "[#(%&Hh&Hsts) Hγ]". wp_let.
iUpd (sts_openS (barrier_inv l P) _ _ γ with "[Hγ]") iMod (sts_openS (barrier_inv l P) _ _ γ with "[Hγ]")
as ([p I]) "(% & [Hl Hr] & Hclose)"; eauto. as ([p I]) "(% & [Hl Hr] & Hclose)"; eauto.
destruct p; [|done]. wp_store. iFrame "HΦ". destruct p; [|done]. wp_store. iFrame "HΦ".
iUpd ("Hclose" $! (State High I) ( : set token) with "[-]"); last done. iMod ("Hclose" $! (State High I) ( : set token) with "[-]"); last done.
iSplit; [iPureIntro; by eauto using signal_step|]. iSplit; [iPureIntro; by eauto using signal_step|].
iNext. rewrite {2}/barrier_inv /ress /=; iFrame "Hl". iNext. rewrite {2}/barrier_inv /ress /=; iFrame "Hl".
iDestruct "Hr" as (Ψ) "[Hr Hsp]"; iExists Ψ; iFrame "Hsp". iDestruct "Hr" as (Ψ) "[Hr Hsp]"; iExists Ψ; iFrame "Hsp".
iIntros "!> _"; by iApply "Hr". iNext. iIntros "_"; by iApply "Hr".
Qed. Qed.
Lemma wait_spec l P (Φ : val iProp Σ) : Lemma wait_spec l P (Φ : val iProp Σ) :
...@@ -138,14 +138,14 @@ Proof. ...@@ -138,14 +138,14 @@ Proof.
rename P into R; rewrite /recv /barrier_ctx. rename P into R; rewrite /recv /barrier_ctx.
iIntros "[Hr HΦ]"; iDestruct "Hr" as (γ P Q i) "(#(%&Hh&Hsts)&Hγ&#HQ&HQR)". iIntros "[Hr HΦ]"; iDestruct "Hr" as (γ P Q i) "(#(%&Hh&Hsts)&Hγ&#HQ&HQR)".
iLöb as "IH". wp_rec. wp_bind (! _)%E. iLöb as "IH". wp_rec. wp_bind (! _)%E.
iUpd (sts_openS (barrier_inv l P) _ _ γ with "[Hγ]") iMod (sts_openS (barrier_inv l P) _ _ γ with "[Hγ]")
as ([p I]) "(% & [Hl Hr] & Hclose)"; eauto. as ([p I]) "(% & [Hl Hr] & Hclose)"; eauto.
wp_load. destruct p. wp_load. destruct p.
- iUpd ("Hclose" $! (State Low I) {[ Change i ]} with "[Hl Hr]") as "Hγ". - iMod ("Hclose" $! (State Low I) {[ Change i ]} with "[Hl Hr]") as "Hγ".
{ iSplit; first done. iNext. rewrite {2}/barrier_inv /=. by iFrame. } { iSplit; first done. iNext. rewrite {2}/barrier_inv /=. by iFrame. }
iAssert (sts_ownS γ (i_states i) {[Change i]})%I with "==>[Hγ]" as "Hγ". iAssert (sts_ownS γ (i_states i) {[Change i]})%I with ">[Hγ]" as "Hγ".
{ iApply (sts_own_weaken with "Hγ"); eauto using i_states_closed. } { iApply (sts_own_weaken with "Hγ"); eauto using i_states_closed. }
iUpdIntro. wp_if. iModIntro. wp_if.
iApply ("IH" with "Hγ [HQR] HΦ"). auto. iApply ("IH" with "Hγ [HQR] HΦ"). auto.
- (* a High state: the comparison succeeds, and we perform a transition and - (* a High state: the comparison succeeds, and we perform a transition and
return to the client *) return to the client *)
...@@ -153,12 +153,12 @@ Proof. ...@@ -153,12 +153,12 @@ Proof.
iDestruct (big_sepS_delete _ _ i with "Hsp") as "[#HΨi Hsp]"; first done. iDestruct (big_sepS_delete _ _ i with "Hsp") as "[#HΨi Hsp]"; first done.
iAssert ( Ψ i [ set] j I {[i]}, Ψ j)%I with "[HΨ]" as "[HΨ HΨ']". iAssert ( Ψ i [ set] j I {[i]}, Ψ j)%I with "[HΨ]" as "[HΨ HΨ']".
{ iNext. iApply (big_sepS_delete _ _ i); first done. by iApply "HΨ". } { iNext. iApply (big_sepS_delete _ _ i); first done. by iApply "HΨ". }
iUpd ("Hclose" $! (State High (I {[ i ]})) ( : set token) with "[HΨ' Hl Hsp]"). iMod ("Hclose" $! (State High (I {[ i ]})) ( : set token) with "[HΨ' Hl Hsp]").
{ iSplit; [iPureIntro; by eauto using wait_step|]. { iSplit; [iPureIntro; by eauto using wait_step|].
iNext. rewrite {2}/barrier_inv /=; iFrame "Hl". iExists Ψ; iFrame. auto. } iNext. rewrite {2}/barrier_inv /=; iFrame "Hl". iExists Ψ; iFrame. auto. }
iPoseProof (saved_prop_agree i Q (Ψ i) with "[#]") as "Heq"; first by auto. iPoseProof (saved_prop_agree i Q (Ψ i) with "[#]") as "Heq"; first by auto.
iUpdIntro. wp_if. iModIntro. wp_if.
iUpdIntro. iApply "HΦ". iApply "HQR". by iRewrite "Heq". iModIntro. iApply "HΦ". iApply "HQR". by iRewrite "Heq".
Qed. Qed.
Lemma recv_split E l P1 P2 : Lemma recv_split E l P1 P2 :
...@@ -166,25 +166,25 @@ Lemma recv_split E l P1 P2 : ...@@ -166,25 +166,25 @@ Lemma recv_split E l P1 P2 :
Proof. Proof.
rename P1 into R1; rename P2 into R2. rewrite {1}/recv /barrier_ctx. rename P1 into R1; rename P2 into R2. rewrite {1}/recv /barrier_ctx.
iIntros (?). iDestruct 1 as (γ P Q i) "(#(%&Hh&Hsts)&Hγ&#HQ&HQR)". iIntros (?). iDestruct 1 as (γ P Q i) "(#(%&Hh&Hsts)&Hγ&#HQ&HQR)".
iUpd (sts_openS (barrier_inv l P) _ _ γ with "[Hγ]") iMod (sts_openS (barrier_inv l P) _ _ γ with "[Hγ]")
as ([p I]) "(% & [Hl Hr] & Hclose)"; eauto. as ([p I]) "(% & [Hl Hr] & Hclose)"; eauto.
iUpd (saved_prop_alloc_strong (R1: %CF (iProp Σ)) I) as (i1) "[% #Hi1]". iMod (saved_prop_alloc_strong (R1: %CF (iProp Σ)) I) as (i1) "[% #Hi1]".
iUpd (saved_prop_alloc_strong (R2: %CF (iProp Σ)) (I {[i1]})) iMod (saved_prop_alloc_strong (R2: %CF (iProp Σ)) (I {[i1]}))
as (i2) "[Hi2' #Hi2]"; iDestruct "Hi2'" as %Hi2. as (i2) "[Hi2' #Hi2]"; iDestruct "Hi2'" as %Hi2.
rewrite ->not_elem_of_union, elem_of_singleton in Hi2; destruct Hi2. rewrite ->not_elem_of_union, elem_of_singleton in Hi2; destruct Hi2.
iUpd ("Hclose" $! (State p ({[i1; i2]} I {[i]})) iMod ("Hclose" $! (State p ({[i1; i2]} I {[i]}))
{[Change i1; Change i2 ]} with "[-]") as "Hγ". {[Change i1; Change i2 ]} with "[-]") as "Hγ".
{ iSplit; first by eauto using split_step. { iSplit; first by eauto using split_step.
iNext. rewrite {2}/barrier_inv /=. iFrame "Hl". iNext. rewrite {2}/barrier_inv /=. iFrame "Hl".
iApply (ress_split _ _ _ Q R1 R2); eauto. iFrame; auto. } iApply (ress_split _ _ _ Q R1 R2); eauto. iFrame; auto. }
iAssert (sts_ownS γ (i_states i1) {[Change i1]} iAssert (sts_ownS γ (i_states i1) {[Change i1]}
sts_ownS γ (i_states i2) {[Change i2]})%I with "==>[-]" as "[Hγ1 Hγ2]". sts_ownS γ (i_states i2) {[Change i2]})%I with ">[-]" as "[Hγ1 Hγ2]".
{ iApply sts_ownS_op; eauto using i_states_closed, low_states_closed. { iApply sts_ownS_op; eauto using i_states_closed, low_states_closed.
- abstract set_solver. - abstract set_solver.
- iApply (sts_own_weaken with "Hγ"); - iApply (sts_own_weaken with "Hγ");
eauto using sts.closed_op, i_states_closed. eauto using sts.closed_op, i_states_closed.
abstract set_solver. } abstract set_solver. }
iUpdIntro; iSplitL "Hγ1"; rewrite /recv /barrier_ctx. iModIntro; iSplitL "Hγ1"; rewrite /recv /barrier_ctx.
- iExists γ, P, R1, i1. iFrame; auto. - iExists γ, P, R1, i1. iFrame; auto.
- iExists γ, P, R2, i2. iFrame; auto. - iExists γ, P, R2, i2. iFrame; auto.
Qed. Qed.
...@@ -194,7 +194,7 @@ Proof. ...@@ -194,7 +194,7 @@ Proof.
rewrite /recv. rewrite /recv.
iIntros "HP HP1"; iDestruct "HP1" as (γ P Q i) "(#Hctx&Hγ&Hi&HP1)". iIntros "HP HP1"; iDestruct "HP1" as (γ P Q i) "(#Hctx&Hγ&Hi&HP1)".
iExists γ, P, Q, i. iFrame "Hctx Hγ Hi". iExists γ, P, Q, i. iFrame "Hctx Hγ Hi".
iIntros "!> HQ". by iApply "HP"; iApply "HP1". iNext. iIntros "HQ". by iApply "HP"; iApply "HP1".
Qed. Qed.
Lemma recv_mono l P1 P2 : (P1 P2) recv l P1 recv l P2. Lemma recv_mono l P1 P2 : (P1 P2) recv l P1 recv l P2.
......
...@@ -38,10 +38,10 @@ Section mono_proof. ...@@ -38,10 +38,10 @@ Section mono_proof.
heap_ctx ( l, mcounter l 0 - Φ #l) WP newcounter #() {{ Φ }}. heap_ctx ( l, mcounter l 0 - Φ #l) WP newcounter #() {{ Φ }}.
Proof. Proof.
iIntros (?) "[#Hh HΦ]". rewrite /newcounter /=. wp_seq. wp_alloc l as "Hl". iIntros (?) "[#Hh HΦ]". rewrite /newcounter /=. wp_seq. wp_alloc l as "Hl".
iUpd (own_alloc ( (O:mnat) (O:mnat))) as (γ) "[Hγ Hγ']"; first done. iMod (own_alloc ( (O:mnat) (O:mnat))) as (γ) "[Hγ Hγ']"; first done.
iUpd (inv_alloc N _ (mcounter_inv γ l) with "[Hl Hγ]"). iMod (inv_alloc N _ (mcounter_inv γ l) with "[Hl Hγ]").
{ iNext. iExists 0%nat. by iFrame. } { iNext. iExists 0%nat. by iFrame. }
iUpdIntro. iApply "HΦ". rewrite /mcounter; eauto 10. iModIntro. iApply "HΦ". rewrite /mcounter; eauto 10.
Qed. Qed.
Lemma inc_mono_spec l n (Φ : val iProp Σ) : Lemma inc_mono_spec l n (Φ : val iProp Σ) :
...@@ -50,22 +50,22 @@ Section mono_proof. ...@@ -50,22 +50,22 @@ Section mono_proof.
iIntros "[Hl HΦ]". iLöb as "IH". wp_rec. iIntros "[Hl HΦ]". iLöb as "IH". wp_rec.
iDestruct "Hl" as (γ) "(% & #? & #Hinv & Hγf)". iDestruct "Hl" as (γ) "(% & #? & #Hinv & Hγf)".
wp_bind (! _)%E. iInv N as (c) ">[Hγ Hl]" "Hclose". wp_bind (! _)%E. iInv N as (c) ">[Hγ Hl]" "Hclose".
wp_load. iUpd ("Hclose" with "[Hl Hγ]") as "_"; [iNext; iExists c; by iFrame|]. wp_load. iMod ("Hclose" with "[Hl Hγ]") as "_"; [iNext; iExists c; by iFrame|].
iUpdIntro. wp_let. wp_op. iModIntro. wp_let. wp_op.
wp_bind (CAS _ _ _). iInv N as (c') ">[Hγ Hl]" "Hclose". wp_bind (CAS _ _ _). iInv N as (c') ">[Hγ Hl]" "Hclose".
destruct (decide (c' = c)) as [->|]. destruct (decide (c' = c)) as [->|].
- iDestruct (own_valid_2 with "[$Hγ $Hγf]") - iDestruct (own_valid_2 with "[$Hγ $Hγf]")
as %[?%mnat_included _]%auth_valid_discrete_2. as %[?%mnat_included _]%auth_valid_discrete_2.
iUpd (own_update_2 with "[$Hγ $Hγf]") as "[Hγ Hγf]". iMod (own_update_2 with "[$Hγ $Hγf]") as "[Hγ Hγf]".
{ apply auth_update, (mnat_local_update _ _ (S c)); auto. } { apply auth_update, (mnat_local_update _ _ (S c)); auto. }
wp_cas_suc. iUpd ("Hclose" with "[Hl Hγ]") as "_". wp_cas_suc. iMod ("Hclose" with "[Hl Hγ]") as "_".
{ iNext. iExists (S c). rewrite Nat2Z.inj_succ Z.add_1_l. by iFrame. } { iNext. iExists (S c). rewrite Nat2Z.inj_succ Z.add_1_l. by iFrame. }
iUpdIntro. wp_if. iApply "HΦ"; iExists γ; repeat iSplit; eauto. iModIntro. wp_if. iApply "HΦ"; iExists γ; repeat iSplit; eauto.
iApply (own_mono with "Hγf"). apply: auth_frag_mono. iApply (own_mono with "Hγf"). apply: auth_frag_mono.
by apply mnat_included, le_n_S. by apply mnat_included, le_n_S.
- wp_cas_fail; first (by intros [= ?%Nat2Z.inj]). - wp_cas_fail; first (by intros [= ?%Nat2Z.inj]).
iUpd ("Hclose" with "[Hl Hγ]") as "_"; [iNext; iExists c'; by iFrame|]. iMod ("Hclose" with "[Hl Hγ]") as "_"; [iNext; iExists c'; by iFrame|].
iUpdIntro. wp_if. iApply ("IH" with "[Hγf] HΦ"). iModIntro. wp_if. iApply ("IH" with "[Hγf] HΦ").
rewrite {3}/mcounter; eauto 10. rewrite {3}/mcounter; eauto 10.
Qed. Qed.
...@@ -77,9 +77,9 @@ Section mono_proof. ...@@ -77,9 +77,9 @@ Section mono_proof.
rewrite /read /=. wp_let. iInv N as (c) ">[Hγ Hl]" "Hclose". wp_load. rewrite /read /=. wp_let. iInv N as (c) ">[Hγ Hl]" "Hclose". wp_load.
iDestruct (own_valid_2 with "[$Hγ $Hγf]") iDestruct (own_valid_2 with "[$Hγ $Hγf]")
as %[?%mnat_included _]%auth_valid_discrete_2. as %[?%mnat_included _]%auth_valid_discrete_2.
iUpd (own_update_2 with "[$Hγ $Hγf]") as "[Hγ Hγf]". iMod (own_update_2 with "[$Hγ $Hγf]") as "[Hγ Hγf]".
{ apply auth_update, (mnat_local_update _ _ c); auto. } { apply auth_update, (mnat_local_update _ _ c); auto. }
iUpd ("Hclose" with "[Hl Hγ]") as "_"; [iNext; iExists c; by iFrame|]. iMod ("Hclose" with "[Hl Hγ]") as "_"; [iNext; iExists c; by iFrame|].
iApply ("HΦ" with "[%]"); rewrite /mcounter; eauto 10. iApply ("HΦ" with "[%]"); rewrite /mcounter; eauto 10.
Qed. Qed.
End mono_proof. End mono_proof.
...@@ -116,11 +116,11 @@ Section contrib_spec. ...@@ -116,11 +116,11 @@ Section contrib_spec.
WP newcounter #() {{ Φ }}. WP newcounter #() {{ Φ }}.
Proof. Proof.
iIntros (?) "[#Hh HΦ]". rewrite /newcounter /=. wp_seq. wp_alloc l as "Hl". iIntros (?) "[#Hh HΦ]". rewrite /newcounter /=. wp_seq. wp_alloc l as "Hl".
iUpd (own_alloc ( (Some (1%Qp, O%nat)) (Some (1%Qp, 0%nat)))) iMod (own_alloc ( (Some (1%Qp, O%nat)) (Some (1%Qp, 0%nat))))
as (γ) "[Hγ Hγ']"; first done. as (γ) "[Hγ Hγ']"; first done.
iUpd (inv_alloc N _ (ccounter_inv γ l) with "[Hl Hγ]"). iMod (inv_alloc N _ (ccounter_inv γ l) with "[Hl Hγ]").
{ iNext. iExists 0%nat. by iFrame. } { iNext. iExists 0%nat. by iFrame. }
iUpdIntro. iApply "HΦ". rewrite /ccounter_ctx /ccounter; eauto 10. iModIntro. iApply "HΦ". rewrite /ccounter_ctx /ccounter; eauto 10.
Qed. Qed.
Lemma inc_contrib_spec γ l q n (Φ : val iProp Σ) : Lemma inc_contrib_spec γ l q n (Φ : val iProp Σ) :
...@@ -129,19 +129,19 @@ Section contrib_spec. ...@@ -129,19 +129,19 @@ Section contrib_spec.
Proof. Proof.
iIntros "(#(%&?&?) & Hγf & HΦ)". iLöb as "IH". wp_rec. iIntros "(#(%&?&?) & Hγf & HΦ)". iLöb as "IH". wp_rec.
wp_bind (! _)%E. iInv N as (c) ">[Hγ Hl]" "Hclose". wp_bind (! _)%E. iInv N as (c) ">[Hγ Hl]" "Hclose".
wp_load. iUpd ("Hclose" with "[Hl Hγ]") as "_"; [iNext; iExists c; by iFrame|]. wp_load. iMod ("Hclose" with "[Hl Hγ]") as "_"; [iNext; iExists c; by iFrame|].
iUpdIntro. wp_let. wp_op. iModIntro. wp_let. wp_op.
wp_bind (CAS _ _ _). iInv N as (c') ">[Hγ Hl]" "Hclose". wp_bind (CAS _ _ _). iInv N as (c') ">[Hγ Hl]" "Hclose".
destruct (decide (c' = c)) as [->|]. destruct (decide (c' = c)) as [->|].
- iUpd (own_update_2 with "[$Hγ $Hγf]") as "[Hγ Hγf]". - iMod (own_update_2 with "[$Hγ $Hγf]") as "[Hγ Hγf]".
{ apply auth_update, option_local_update, prod_local_update_2. { apply auth_update, option_local_update, prod_local_update_2.
apply (nat_local_update _ _ (S c) (S n)); omega. } apply (nat_local_update _ _ (S c) (S n)); omega. }
wp_cas_suc. iUpd ("Hclose" with "[Hl Hγ]") as "_". wp_cas_suc. iMod ("Hclose" with "[Hl Hγ]") as "_".
{ iNext. iExists (S c). rewrite Nat2Z.inj_succ Z.add_1_l. by iFrame. } { iNext. iExists (S c). rewrite Nat2Z.inj_succ Z.add_1_l. by iFrame. }
iUpdIntro. wp_if. by iApply "HΦ". iModIntro. wp_if. by iApply "HΦ".
- wp_cas_fail; first (by intros [= ?%Nat2Z.inj]). - wp_cas_fail; first (by intros [= ?%Nat2Z.inj]).
iUpd ("Hclose" with "[Hl Hγ]") as "_"; [iNext; iExists c'; by iFrame|]. iMod ("Hclose" with "[Hl Hγ]") as "_"; [iNext; iExists c'; by iFrame|].
iUpdIntro. wp_if. by iApply ("IH" with "[Hγf] HΦ"). iModIntro. wp_if. by iApply ("IH" with "[Hγf] HΦ").
Qed. Qed.
Lemma read_contrib_spec γ l q n (Φ : val iProp Σ) : Lemma read_contrib_spec γ l q n (Φ : val iProp Σ) :
...@@ -153,7 +153,7 @@ Section contrib_spec. ...@@ -153,7 +153,7 @@ Section contrib_spec.
rewrite /read /=. wp_let. iInv N as (c) ">[Hγ Hl]" "Hclose". wp_load. rewrite /read /=. wp_let. iInv N as (c) ">[Hγ Hl]" "Hclose". wp_load.
iDestruct (own_valid_2 with "[$Hγ $Hγf]") iDestruct (own_valid_2 with "[$Hγ $Hγf]")
as %[[? ?%nat_included]%Some_pair_included_total_2 _]%auth_valid_discrete_2. as %[[? ?%nat_included]%Some_pair_included_total_2 _]%auth_valid_discrete_2.
iUpd ("Hclose" with "[Hl Hγ]") as "_"; [iNext; iExists c; by iFrame|]. iMod ("Hclose" with "[Hl Hγ]") as "_"; [iNext; iExists c; by iFrame|].
iApply ("HΦ" with "[%]"); rewrite /ccounter; eauto 10. iApply ("HΦ" with "[%]"); rewrite /ccounter; eauto 10.
Qed. Qed.
...@@ -165,7 +165,7 @@ Section contrib_spec. ...@@ -165,7 +165,7 @@ Section contrib_spec.
rewrite /read /=. wp_let. iInv N as (c) ">[Hγ Hl]" "Hclose". wp_load. rewrite /read /=. wp_let. iInv N as (c) ">[Hγ Hl]" "Hclose". wp_load.
iDestruct (own_valid_2 with "[$Hγ $Hγf]") as %[Hn _]%auth_valid_discrete_2. iDestruct (own_valid_2 with "[$Hγ $Hγf]") as %[Hn _]%auth_valid_discrete_2.
apply (Some_included_exclusive _) in Hn as [= ->]%leibniz_equiv; last done. apply (Some_included_exclusive _) in Hn as [= ->]%leibniz_equiv; last done.
iUpd ("Hclose" with "[Hl Hγ]") as "_"; [iNext; iExists c; by iFrame|]. iMod ("Hclose" with "[Hl Hγ]") as "_"; [iNext; iExists c; by iFrame|].
by iApply "HΦ". by iApply "HΦ".
Qed.