From 34b93f99698ffcfaa5ab0c334b52002b260f7e83 Mon Sep 17 00:00:00 2001
From: David Swasey <swasey@mpi-sws.org>
Date: Sun, 18 Dec 2016 14:08:37 +0100
Subject: [PATCH] Restore the weaker notion of atomicity (both are now
 available).

---
 theories/heap_lang/tactics.v           | 10 ++++----
 theories/program_logic/ectx_language.v | 14 +++++------
 theories/program_logic/hoare.v         | 19 +++++++++++---
 theories/program_logic/weakestpre.v    | 35 +++++++++++++++++++++-----
 theories/tests/ipm_paper.v             |  2 +-
 5 files changed, 58 insertions(+), 22 deletions(-)

diff --git a/theories/heap_lang/tactics.v b/theories/heap_lang/tactics.v
index 6cfa3e1df..64401c566 100644
--- a/theories/heap_lang/tactics.v
+++ b/theories/heap_lang/tactics.v
@@ -187,9 +187,9 @@ Definition is_atomic (e : expr) :=
   | App (Rec _ _ (Lit _)) (Lit _) => true
   | _ => false
   end.
-Lemma is_atomic_correct e : is_atomic e → StronglyAtomic (to_expr e).
+Lemma is_atomic_correct e : is_atomic e → Atomic (to_expr e).
 Proof.
-  intros He. apply ectx_language_strongly_atomic.
+  intros He. apply strongly_atomic_atomic, ectx_language_strong_atomic.
   - intros σ e' σ' ef Hstep; simpl in *. revert Hstep.
     destruct e=> //=; repeat (simplify_eq/=; case_match=>//);
       inversion 1; simplify_eq/=; rewrite ?to_of_val; eauto.
@@ -226,11 +226,11 @@ Hint Extern 10 (AsVal _) => solve_as_val : typeclass_instances.
 
 Ltac solve_atomic :=
   match goal with
-  | |- StronglyAtomic ?e =>
-     let e' := W.of_expr e in change (StronglyAtomic (W.to_expr e'));
+  | |- Atomic ?e =>
+     let e' := W.of_expr e in change (Atomic (W.to_expr e'));
      apply W.is_atomic_correct; vm_compute; exact I
   end.
-Hint Extern 10 (StronglyAtomic _) => solve_atomic : typeclass_instances.
+Hint Extern 10 (Atomic _) => solve_atomic : typeclass_instances.
 
 (** Substitution *)
 Ltac simpl_subst :=
diff --git a/theories/program_logic/ectx_language.v b/theories/program_logic/ectx_language.v
index af8b796f9..3bad0f053 100644
--- a/theories/program_logic/ectx_language.v
+++ b/theories/program_logic/ectx_language.v
@@ -117,20 +117,20 @@ Section ectx_language.
     rewrite -not_reducible -not_head_reducible. eauto using prim_head_reducible.
   Qed.
 
-  Lemma ectx_language_atomic e :
-    (∀ σ e' σ' efs, head_step e σ e' σ' efs → irreducible e' σ') →
+  Lemma ectx_language_strong_atomic e :
+    (∀ σ e' σ' efs, head_step e σ e' σ' efs → is_Some (to_val e')) →
     sub_redexes_are_values e →
-    Atomic e.
+    StronglyAtomic e.
   Proof.
     intros Hatomic_step Hatomic_fill σ e' σ' efs [K e1' e2' -> -> Hstep].
     assert (K = empty_ectx) as -> by eauto 10 using val_stuck.
     rewrite fill_empty. eapply Hatomic_step. by rewrite fill_empty.
   Qed.
 
-  Lemma ectx_language_strongly_atomic e :
-    (∀ σ e' σ' efs, head_step e σ e' σ' efs → is_Some (to_val e')) →
-    sub_values e →
-    StronglyAtomic e.
+  Lemma ectx_language_atomic e :
+    (∀ σ e' σ' efs, head_step e σ e' σ' efs → irreducible e' σ') →
+    sub_redexes_are_values e →
+    Atomic e.
   Proof.
     intros Hatomic_step Hatomic_fill σ e' σ' efs [K e1' e2' -> -> Hstep].
     assert (K = empty_ectx) as -> by eauto 10 using val_stuck.
diff --git a/theories/program_logic/hoare.v b/theories/program_logic/hoare.v
index b3a8a4677..953c05f6f 100644
--- a/theories/program_logic/hoare.v
+++ b/theories/program_logic/hoare.v
@@ -42,6 +42,7 @@ Notation "{{ P } } e ? {{ v , Q } }" := (ht false ⊤ P%I e%E (λ v, Q)%I)
 
 Section hoare.
 Context `{irisG Λ Σ}.
+Implicit Types p : bool.
 Implicit Types P Q : iProp Σ.
 Implicit Types Φ Ψ : val Λ → iProp Σ.
 Implicit Types v : val Λ.
@@ -75,17 +76,29 @@ Proof.
   iIntros (v) "Hv". by iApply "HΦ".
 Qed.
 
-Lemma ht_atomic p E1 E2 P P' Φ Φ' e :
-  StronglyAtomic e →
+Lemma ht_atomic' p E1 E2 P P' Φ Φ' e :
+  StronglyAtomic e ∨ p ∧ Atomic e →
   (P ={E1,E2}=> P') ∧ {{ P' }} e @ p; E2 {{ Φ' }} ∧ (∀ v, Φ' v ={E2,E1}=> Φ v)
   ⊢ {{ P }} e @ p; E1 {{ Φ }}.
 Proof.
-  iIntros (?) "(#Hvs & #Hwp & #HΦ) !# HP". iApply (wp_atomic _ _ E2); auto.
+  iIntros (?) "(#Hvs & #Hwp & #HΦ) !# HP". iApply (wp_atomic' _ _ E2); auto.
   iMod ("Hvs" with "HP") as "HP". iModIntro.
   iApply (wp_wand with "[HP]"); [by iApply "Hwp"|].
   iIntros (v) "Hv". by iApply "HΦ".
 Qed.
 
+Lemma ht_strong_atomic p E1 E2 P P' Φ Φ' e :
+  StronglyAtomic e →
+  (P ={E1,E2}=> P') ∧ {{ P' }} e @ p; E2 {{ Φ' }} ∧ (∀ v, Φ' v ={E2,E1}=> Φ v)
+  ⊢ {{ P }} e @ p; E1 {{ Φ }}.
+Proof. by eauto using ht_atomic'. Qed.
+
+Lemma ht_atomic E1 E2 P P' Φ Φ' e :
+  Atomic e →
+  (P ={E1,E2}=> P') ∧ {{ P' }} e @ E2 {{ Φ' }} ∧ (∀ v, Φ' v ={E2,E1}=> Φ v)
+  ⊢ {{ P }} e @ E1 {{ Φ }}.
+Proof. by eauto using ht_atomic'. Qed.
+
 Lemma ht_bind `{LanguageCtx Λ K} p E P Φ Φ' e :
   {{ P }} e @ p; E {{ Φ }} ∧ (∀ v, {{ Φ v }} K (of_val v) @ p; E {{ Φ' }})
   ⊢ {{ P }} K e @ p; E {{ Φ' }}.
diff --git a/theories/program_logic/weakestpre.v b/theories/program_logic/weakestpre.v
index b205ee399..12c77165c 100644
--- a/theories/program_logic/weakestpre.v
+++ b/theories/program_logic/weakestpre.v
@@ -165,6 +165,7 @@ Notation "'{{{' P } } } e ? {{{ 'RET' pat ; Q } } }" :=
 
 Section wp.
 Context `{irisG Λ Σ}.
+Implicit Types p : bool.
 Implicit Types P : iProp Σ.
 Implicit Types Φ : val Λ → iProp Σ.
 Implicit Types v : val Λ.
@@ -231,8 +232,8 @@ Qed.
 Lemma wp_fupd p E e Φ : WP e @ p; E {{ v, |={E}=> Φ v }} ⊢ WP e @ p; E {{ Φ }}.
 Proof. iIntros "H". iApply (wp_strong_mono p E); try iFrame; auto. Qed.
 
-Lemma wp_atomic p E1 E2 e Φ :
-  StronglyAtomic e →
+Lemma wp_atomic' p E1 E2 e Φ :
+  StronglyAtomic e ∨ p ∧ Atomic e →
   (|={E1,E2}=> WP e @ p; E2 {{ v, |={E2,E1}=> Φ v }}) ⊢ WP e @ p; E1 {{ Φ }}.
 Proof.
   iIntros (Hatomic) "H". rewrite !wp_unfold /wp_pre.
@@ -240,9 +241,15 @@ Proof.
   { by iDestruct "H" as ">>> $". }
   iIntros (σ1) "Hσ". iMod "H". iMod ("H" $! σ1 with "Hσ") as "[$ H]".
   iModIntro. iNext. iIntros (e2 σ2 efs Hstep).
-  destruct (Hatomic _ _ _ _ Hstep) as [v <-%of_to_val].
-  iMod ("H" with "[#]") as "($ & H & $)"; first done.
-  iMod (wp_value_inv with "H") as ">H". by iApply wp_value'.
+  destruct Hatomic as [Hstrong|[? Hweak]].
+  - destruct (Hstrong _ _ _ _ Hstep) as [v <-%of_to_val].
+    iMod ("H" with "[#]") as "($ & H & $)"; first done.
+    iMod (wp_value_inv with "H") as ">H". by iApply wp_value'.
+  - destruct p; last done. iMod ("H" with "[//]") as "(Hphy & H & $)".
+    rewrite !wp_unfold /wp_pre. destruct (to_val e2).
+    + iDestruct "H" as ">> $". by iFrame.
+    + iMod ("H" with "[$]") as "[H _]".
+      iDestruct "H" as %(? & ? & ? & ?). by edestruct (Hweak _ _ _ _ Hstep).
 Qed.
 
 Lemma wp_step_fupd p E1 E2 e P Φ :
@@ -307,6 +314,15 @@ Lemma wp_value_fupd p E Φ e v `{!IntoVal e v} :
   (|={E}=> Φ v) ⊢ WP e @ p; E {{ Φ }}.
 Proof. intros. rewrite -wp_fupd -wp_value //. Qed.
 
+Lemma wp_strong_atomic p E1 E2 e Φ :
+  StronglyAtomic e →
+  (|={E1,E2}=> WP e @ p; E2 {{ v, |={E2,E1}=> Φ v }}) ⊢ WP e @ p; E1 {{ Φ }}.
+Proof. by eauto using wp_atomic'. Qed.
+Lemma wp_atomic E1 E2 e Φ :
+  Atomic e →
+  (|={E1,E2}=> WP e @ E2 {{ v, |={E2,E1}=> Φ v }}) ⊢ WP e @ E1 {{ Φ }}.
+Proof. by eauto using wp_atomic'. Qed.
+
 Lemma wp_frame_l p E e Φ R : R ∗ WP e @ p; E {{ Φ }} ⊢ WP e @ p; E {{ v, R ∗ Φ v }}.
 Proof. iIntros "[??]". iApply (wp_strong_mono p E E _ Φ); try iFrame; eauto. Qed.
 Lemma wp_frame_r p E e Φ R : WP e @ p; E {{ Φ }} ∗ R ⊢ WP e @ p; E {{ v, Φ v ∗ R }}.
@@ -369,9 +385,16 @@ Section proofmode_classes.
   Proof. by rewrite /ElimModal fupd_frame_r wand_elim_r fupd_wp. Qed.
 
   (* lower precedence, if possible, it should persistently pick elim_upd_fupd_wp *)
-  Global Instance elim_modal_fupd_wp_atomic E1 E2 e P Φ :
+  Global Instance elim_modal_fupd_wp_strong_atomic E1 E2 e P Φ :
     StronglyAtomic e →
     ElimModal (|={E1,E2}=> P) P
             (WP e @ p; E1 {{ Φ }}) (WP e @ p; E2 {{ v, |={E2,E1}=> Φ v }})%I | 100.
+  Proof. intros. by rewrite /ElimModal fupd_frame_r wand_elim_r wp_strong_atomic. Qed.
+
+  (* lower precedence than elim_modal_fupd_wp_strong_atomic (for no good reason) *)
+  Global Instance elim_modal_fupd_wp_atomic E1 E2 e P Φ :
+    Atomic e →
+    ElimModal (|={E1,E2}=> P) P
+            (WP e @ E1 {{ Φ }}) (WP e @ E2 {{ v, |={E2,E1}=> Φ v }})%I | 110.
   Proof. intros. by rewrite /ElimModal fupd_frame_r wand_elim_r wp_atomic. Qed.
 End proofmode_classes.
diff --git a/theories/tests/ipm_paper.v b/theories/tests/ipm_paper.v
index 0922cd5bb..6834c5c5e 100644
--- a/theories/tests/ipm_paper.v
+++ b/theories/tests/ipm_paper.v
@@ -101,7 +101,7 @@ update modalities (which we did not cover in the paper). Normally we use these
 mask changing update modalities directly in our proofs, but in this file we use
 the first prove the rule as a lemma, and then use that. *)
 Lemma wp_inv_open `{irisG Λ Σ} N E P e Φ :
-  nclose N ⊆ E → StronglyAtomic e →
+  nclose N ⊆ E → Atomic e →
   inv N P ∗ (▷ P -∗ WP e @ E ∖ ↑N {{ v, ▷ P ∗ Φ v }}) ⊢ WP e @ E {{ Φ }}.
 Proof.
   iIntros (??) "[#Hinv Hwp]".
-- 
GitLab