add iAuIntro tactic to prove an atomic update; introduce atomic_step

97838371 · Ralf Jung · 2e1d3454 · 97838371 · 97838371 · 97838371
Commit 97838371 authored Apr 25, 2018 by Ralf Jung
--- a/theories/bi/lib/atomic.v
+++ b/theories/bi/lib/atomic.v
 From iris.bi Require Export bi updates.
 From iris.bi.lib Require Import fixpoint laterable.
 From stdpp Require Import coPset.
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import coq_tactics tactics.
 Set Default Proof Using "Type".

-(** atomic_update as a fixed-point of the equation
-   AU = ∃ P. ▷ P ∗ □ (▷ P ==∗ α ∗ (α ==∗ AU) ∧ (β ==∗ Q))
- *)
 Section definition.
-  Context `{BiFUpd PROP} {A B : Type}
+  Context `{BiFUpd PROP} {A B : Type}.
+  Implicit Types
+    (Eo Em : coPset) (* outside/module masks *)
    (α : A → PROP) (* atomic pre-condition *)
+    (P : PROP) (* abortion condition *)
    (β : A → B → PROP) (* atomic post-condition *)
-    (Eo Em : coPset) (* outside/module masks *)
    (Φ : A → B → PROP) (* post-condition *)
  .

-  Definition atomic_shift (P P' : PROP) : PROP :=
-    (□ (∀ E, ⌜Eo ⊆ E⌝ → P ={E, E∖Em}=∗ ∃ x, α x ∗
-          ((α x ={E∖Em, E}=∗ P') ∧ (∀ y, β x y ={E∖Em, E}=∗ Φ x y)))
+(** atomic_step as the "introduction form" of atomic updates *)
+  Definition atomic_step Eo Em α P β Φ : PROP :=
+    (|={Eo, Eo∖Em}=> ∃ x, α x ∗
+          ((α x ={Eo∖Em, Eo}=∗ P) ∧ (∀ y, β x y ={Eo∖Em, Eo}=∗ Φ x y))
    )%I.

-  Lemma atomic_shift_mono P P1 P2:
-    □ (P1 -∗ P2) -∗ □ (atomic_shift P P1 -∗ atomic_shift P P2).
+  Lemma atomic_shift_mono Eo Em α P1 P2 β Φ :
+    □ (P1 -∗ P2) -∗
+    □ (atomic_step Eo Em α P1 β Φ -∗ atomic_step Eo Em α P2 β Φ).
  Proof.
-    iIntros "#HP12 !# #AS !# * % HP".
-    iMod ("AS" with "[% //] HP") as (x) "[Hα Hclose]".
+    iIntros "#HP12 !# AS". iMod "AS" as (x) "[Hα Hclose]".
    iModIntro. iExists x. iFrame "Hα". iSplit.
    - iIntros "Hα". iDestruct "Hclose" as "[Hclose _]".
      iApply "HP12". iApply "Hclose". done.
@@ -32,21 +32,28 @@ Section definition.
      iApply "Hclose". done.
  Qed.

+(** atomic_update as a fixed-point of the equation
+   AU = ∃ P. ▷ P ∗ □ (▷ P ==∗ α ∗ (α ==∗ AU) ∧ (β ==∗ Q))
+ *)
+  Context Eo Em α β Φ.
+
  Definition atomic_update_pre (Ψ : () → PROP) (_ : ()) : PROP :=
-    (∃ (P : PROP), ▷ P ∗ atomic_shift (▷ P) (Ψ ()))%I.
+    (∃ (P : PROP), ▷ P ∗
+     □ (∀ E, ⌜Eo ⊆ E⌝ → (▷ P) -∗ atomic_step E Em α (Ψ ()) β Φ))%I.

  Local Instance atomic_update_pre_mono : BiMonoPred atomic_update_pre.
  Proof.
    constructor.
    - iIntros (P1 P2) "#HP12". iIntros ([]) "AU".
-      iDestruct "AU" as (P) "[HP AS]". iExists P. iFrame.
-      iApply (atomic_shift_mono with "[HP12]"); last done.
-      iAlways. iApply "HP12".
+      iDestruct "AU" as (P) "[HP #AS]". iExists P. iFrame.
+      iIntros "!# * % HP". iApply (atomic_shift_mono with "HP12").
+      iApply ("AS" with "[%]"); done.
    - intros ??. solve_proper.
  Qed.

  Definition atomic_update_def :=
    bi_greatest_fixpoint atomic_update_pre ().
+
 End definition.

 (** Seal it *)
@@ -62,13 +69,32 @@ Section lemmas.

  Local Existing Instance atomic_update_pre_mono.

+  Global Instance atomic_step_ne Eo Em n :
+    Proper (
+        pointwise_relation A (dist n) ==>
+        dist n ==>
+        pointwise_relation A (pointwise_relation B (dist n)) ==>
+        pointwise_relation A (pointwise_relation B (dist n)) ==>
+        dist n
+    ) (atomic_step (PROP:=PROP) Eo Em).
+  Proof. solve_proper. Qed.
+
+  Global Instance atomic_update_ne Eo Em n :
+    Proper (
+        pointwise_relation A (dist n) ==>
+        pointwise_relation A (pointwise_relation B (dist n)) ==>
+        pointwise_relation A (pointwise_relation B (dist n)) ==>
+        dist n
+    ) (atomic_update (PROP:=PROP) Eo Em).
+  Proof.
+    rewrite atomic_update_eq /atomic_update_def /atomic_update_pre. solve_proper.
+  Qed.
+
  (** The ellimination form: an accessor *)
-  Lemma aupd_acc α β Eo Em Φ E :
+  Lemma aupd_acc  Eo Em E α β Φ :
    Eo ⊆ E →
-    atomic_update α β Eo Em Φ -∗
-    |={E, E∖Em}=> ∃ x, α x ∗
-      ((α x ={E∖Em, E}=∗ atomic_update α β Eo Em Φ) ∧
-       (∀ y, β x y ={E∖Em, E}=∗ Φ x y)).
+    atomic_update Eo Em α β Φ -∗
+    atomic_step E Em α (atomic_update Eo Em α β Φ) β Φ.
  Proof using Type*.
    rewrite atomic_update_eq {1}/atomic_update_def /=. iIntros (HE) "HUpd".
    iPoseProof (greatest_fixpoint_unfold_1 with "HUpd") as "HUpd".
@@ -77,8 +103,8 @@ Section lemmas.
    iModIntro. iExists x. iFrame.
  Qed.

-  Global Instance aupd_laterable α β Eo Em Φ :
-    Laterable (atomic_update α β Eo Em Φ).
+  Global Instance aupd_laterable Eo Em α β Φ :
+    Laterable (atomic_update Eo Em α β Φ).
  Proof.
    rewrite /Laterable atomic_update_eq {1}/atomic_update_def /=. iIntros "AU".
    iPoseProof (greatest_fixpoint_unfold_1 with "AU") as (P) "[HP #AS]".
@@ -86,20 +112,18 @@ Section lemmas.
    iApply greatest_fixpoint_unfold_2. iExists P. iFrame "#∗".
  Qed.

-  Lemma aupd_intro P α β Eo Em Φ :
-    Em ⊆ Eo → Laterable P →
-    P -∗
-    □ (P -∗ |={Eo, Eo∖Em}=> ∃ x, α x ∗
-      ((α x ={Eo∖Em, Eo}=∗ P) ∧ (∀ y, β x y ={Eo∖Em, Eo}=∗ Φ x y))) -∗
-    atomic_update α β Eo Em Φ.
+  Lemma aupd_intro P Q α β Eo Em Φ :
+    Em ⊆ Eo → Affine P → Persistent P → Laterable Q →
+    (P ∗ Q -∗ atomic_step Eo Em α Q β Φ) →
+    P ∗ Q -∗ atomic_update Eo Em α β Φ.
  Proof.
    rewrite atomic_update_eq {1}/atomic_update_def /=.
-    iIntros (??) "HP #AU".
-    iApply (greatest_fixpoint_coind _ (λ _, P)); last done. iIntros "!#" ([]) "HP".
-    iDestruct (laterable with "HP") as (P') "[HP' #HPi]". iExists P'. iFrame.
-    iIntros "!#" (E HE) "HP'". iDestruct ("HPi" with "HP'") as ">HP {HPi}".
+    iIntros (???? HAU) "[#HP HQ]".
+    iApply (greatest_fixpoint_coind _ (λ _, Q)); last done. iIntros "!#" ([]) "HQ".
+    iDestruct (laterable with "HQ") as (Q') "[HQ' #HQi]". iExists Q'. iFrame.
+    iIntros "!#" (E HE) "HQ'". iDestruct ("HQi" with "HQ'") as ">HQ {HQi}".
    iApply fupd_mask_frame_diff_open; last
-      iMod ("AU" with "HP") as (x) "[Hα Hclose] {AU}"; [done..|].
+      iMod (HAU with "[$HQ]") as (x) "[Hα Hclose]"; [done..|].
    iModIntro. iExists x. iFrame. iSplit.
    - iDestruct "Hclose" as "[Hclose _]". iIntros "Hα".
      iApply fupd_mask_frame_diff_close; last (by iApply "Hclose"); done.
@@ -107,3 +131,33 @@ Section lemmas.
      iApply fupd_mask_frame_diff_close; last (by iApply "Hclose"); done.
  Qed.
 End lemmas.
+
+(** ProofMode support for atomic updates *)
+
+Section proof_mode.
+  Context `{BiFUpd PROP} {A B : Type}.
+  Implicit Types (α : A → PROP) (β: A → B → PROP) (P : PROP) (Φ : A → B → PROP).
+
+  Lemma tac_aupd_intro Γp Γs n α β Eo Em Φ P :
+    Em ⊆ Eo →
+    Timeless (PROP:=PROP) emp →
+    TCForall Laterable (env_to_list Γs) →
+    P = prop_of_env Γs →
+    envs_entails (Envs Γp Γs n) (atomic_step Eo Em α P β Φ) →
+    envs_entails (Envs Γp Γs n) (atomic_update Eo Em α β Φ).
+  Proof.
+    intros ?? HΓs ->. rewrite envs_entails_eq of_envs_eq' /atomic_step /=.
+    setoid_rewrite prop_of_env_sound =>HAU.
+    apply aupd_intro; [done|apply _..|]. done.
+  Qed. 
+End proof_mode.
+
+(** Now the coq-level tactics *)
+
+Tactic Notation "iAuIntro" :=
+  iStartProof; eapply tac_aupd_intro; [
+    (* Em ⊆ Eo: to be proven by user *)
+  | iSolveTC || fail "iAuIntro: emp is not timeless"
+  | iSolveTC || fail "Not all spatial assumptions are laterable"
+  | (* P = ...: make the P pretty *) env_reflexivity
+  | (* the new proof mode goal *) ].
--- a/theories/bi/lib/laterable.v
+++ b/theories/bi/lib/laterable.v
@@ -50,4 +50,10 @@ Section instances.
    - iApply "HP". done.
    - iApply "HQ". done.
  Qed.
+
+  Global Instance big_sepL_laterable Ps :
+    Timeless (PROP:=PROP) emp →
+    TCForall Laterable Ps →
+    Laterable (PROP:=PROP) ([∗] Ps).
+  Proof. induction 2; simpl; apply _. Qed.
 End instances.
--- a/theories/heap_lang/lib/atomic_heap.v
+++ b/theories/heap_lang/lib/atomic_heap.v
@@ -22,23 +22,23 @@ Structure atomic_heap {Σ} `{!heapG Σ} := AtomicHeap {
    {{{ True }}} alloc v {{{ l, RET #l; mapsto l 1 v }}};
  load_spec (l : loc) :
    atomic_wp (load #l)%E
+              ⊤ ⊤
              (λ '(v, q), mapsto l q v)
              (λ '(v, q) (_:()), mapsto l q v)
-              ⊤ ⊤
              (λ '(v, q) _, v);
  store_spec (l : loc) (e : expr) (w : val) :
    IntoVal e w →
    atomic_wp (store (#l, e))%E
+              ⊤ ⊤
              (λ v, mapsto l 1 v)
              (λ v (_:()), mapsto l 1 w)
-              ⊤ ⊤
              (λ _ _, #()%V);
  cas_spec (l : loc) (e1 e2 : expr) (w1 w2 : val) :
    IntoVal e1 w1 → IntoVal e2 w2 →
    atomic_wp (cas (#l, e1, e2))%E
+              ⊤ ⊤
              (λ v, mapsto l 1 v)
              (λ v (_:()), if decide (v = w1) then mapsto l 1 w2 else mapsto l 1 v)
-              ⊤ ⊤
              (λ v _, #(if decide (v = w1) then true else false)%V);
 }.
 Arguments atomic_heap _ {_}.
@@ -64,9 +64,9 @@ Section proof.

  Lemma primitive_load_spec (l : loc) :
    atomic_wp (primitive_load #l)%E
+              ⊤ ⊤
              (λ '(v, q), l ↦{q} v)%I
              (λ '(v, q) (_:()), l ↦{q} v)%I
-              ⊤ ⊤
              (λ '(v, q) _, v).
  Proof.
    iIntros (Q Φ) "? AU". wp_let.
@@ -77,9 +77,9 @@ Section proof.
  Lemma primitive_store_spec (l : loc) (e : expr) (w : val) :
    IntoVal e w →
    atomic_wp (primitive_store (#l, e))%E
+              ⊤ ⊤
              (λ v, l ↦ v)%I
              (λ v (_:()), l ↦ w)%I
-              ⊤ ⊤
              (λ _ _, #()%V).
  Proof.
    iIntros (<-%of_to_val Q Φ) "? AU". wp_let. wp_proj. wp_proj.
@@ -90,9 +90,9 @@ Section proof.
  Lemma primitive_cas_spec (l : loc) e1 e2 (w1 w2 : val) :
    IntoVal e1 w1 → IntoVal e2 w2 →
    atomic_wp (primitive_cas (#l, e1, e2))%E
+              ⊤ ⊤
              (λ v, l ↦ v)%I
              (λ v (_:()), if decide (v = w1) then l ↦ w2 else l ↦ v)%I
-              ⊤ ⊤
              (λ v _, #(if decide (v = w1) then true else false)%V).
  Proof.
    iIntros (<-%of_to_val <-%of_to_val Q Φ) "? AU". wp_let. repeat wp_proj.

--- a/theories/heap_lang/lib/increment.v
+++ b/theories/heap_lang/lib/increment.v
@@ -21,23 +21,23 @@ Section increment.

  Lemma incr_spec (l: loc) :
        atomic_wp (incr #l)
+                  ⊤ ⊤
                  (λ (v: Z), aheap.(mapsto) l 1 #v)%I
                  (λ v (_:()), aheap.(mapsto) l 1 #(v + 1))%I
-                  ⊤ ⊤
                  (λ v _, #v).
  Proof.
    iIntros (Q Φ) "HQ AU". iLöb as "IH". wp_let.
-    wp_apply (load_spec with "HQ").
+    wp_apply (load_spec with "[HQ]"); first by iAccu.
    (* Prove the atomic shift for load *)
-    iApply (aupd_intro with "AU"); first done. iIntros "!# AU".
+    iAuIntro; first done.
    iMod (aupd_acc with "AU") as (x) "[H↦ [Hclose _]]"; first solve_ndisj.
    iModIntro. iExists (#x, 1%Qp). iFrame "H↦". iSplit; first done.
    iIntros ([]) "H↦". iMod ("Hclose" with "H↦") as "AU". iIntros "!> HQ".
    (* Now go on *)
    wp_let. wp_op. wp_bind (aheap.(cas) _)%I.
-    wp_apply (cas_spec with "HQ").
+    wp_apply (cas_spec with "[HQ]"); first by iAccu.
    (* Prove the atomic shift for CAS *)
-    iApply (aupd_intro with "AU"); first done. iIntros "!# AU".
+    iAuIntro; first done.
    iMod (aupd_acc with "AU") as (x') "[H↦ Hclose]"; first solve_ndisj.
    iModIntro. iExists #x'. iFrame. iSplit.
    { iDestruct "Hclose" as "[Hclose _]". iApply "Hclose". }
@@ -69,8 +69,7 @@ Section increment_client.
       to move this to the persisten context even without the additional □. *)
    iAssert (□ WP incr primitive_atomic_heap #l {{ _, True }})%I as "#Aupd".
    { iAlways. wp_apply (incr_spec with "[]"); first iEmpIntro. clear x.
-      iApply (aupd_intro with "[]"); try iEmpIntro; [done|apply _|]. iIntros "!# _".
-      iInv nroot as (x) ">H↦" "Hclose".
+      iAuIntro; first done. iInv nroot as (x) ">H↦" "Hclose".
      iMod fupd_intro_mask' as "Hclose2"; last iModIntro; first set_solver.
      iExists _. iFrame. iSplit.
      { iIntros "H↦". iMod "Hclose2" as "_". iMod ("Hclose" with "[-]"); last done.

--- a/theories/program_logic/atomic.v
+++ b/theories/program_logic/atomic.v
@@ -5,12 +5,12 @@ Set Default Proof Using "Type".

 Definition atomic_wp `{irisG Λ Σ} {A B : Type}
  (e: expr Λ) (* expression *)
+  (Eo Em : coPset) (* outside/module masks *)
  (α: A → iProp Σ) (* atomic pre-condition *)
  (β: A → B → iProp Σ) (* atomic post-condition *)
-  (Eo Em : coPset) (* outside/module masks *)
  (f: A → B → val Λ) (* Turn the return data into the return value *)
  : iProp Σ :=
-    (∀ Q Φ, Q -∗ atomic_update α β Eo Em (λ x y, Q -∗ Φ (f x y)) -∗
+    (∀ Q Φ, Q -∗ atomic_update Eo Em α β (λ x y, Q -∗ Φ (f x y)) -∗
             WP e {{ Φ }})%I.
 (* Note: To add a private postcondition, use
   atomic_update α β Eo Em (λ x y, POST x y -∗ Φ (f x y)) *)
--- a/theories/proofmode/coq_tactics.v
+++ b/theories/proofmode/coq_tactics.v
@@ -152,6 +152,11 @@ Implicit Types P Q : PROP.
 Lemma of_envs_eq Δ :
  of_envs Δ = (⌜envs_wf Δ⌝ ∧ □ [∧] env_intuitionistic Δ ∗ [∗] env_spatial Δ)%I.
 Proof. done. Qed.
+(** An environment is a ∗ of something persistent and the spatial environment.
+TODO: Can we define it as such? *)
+Lemma of_envs_eq' Δ :
+  of_envs Δ ⊣⊢ (⌜envs_wf Δ⌝ ∧ □ [∧] env_intuitionistic Δ) ∗ [∗] env_spatial Δ.
+Proof. rewrite of_envs_eq persistent_and_sep_assoc //. Qed.

 Lemma envs_delete_persistent Δ i : envs_delete false i true Δ = Δ. 
 Proof. by destruct Δ. Qed.
@@ -436,12 +441,12 @@ Proof.
  destruct d; simplify_eq/=; solve_sep_entails.
 Qed.

-Lemma prop_of_env_sound Δ : of_envs Δ ⊢ prop_of_env (env_spatial Δ).
+Lemma prop_of_env_sound Γ : prop_of_env Γ ⊣⊢ [∗] Γ.
 Proof.
-  destruct Δ as [? Γ]. rewrite /of_envs /= and_elim_r sep_elim_r.
-  destruct Γ as [|Γ ? P0]=>//=. revert P0.
-  induction Γ as [|Γ IH ? P]=>P0; [rewrite /= right_id //|].
-  rewrite /= assoc (comm _ P0 P) IH //.
+  destruct Γ as [|Γ ? P]; simpl; first done.
+  revert P. induction Γ as [|Γ IH ? Q]=>P; simpl.
+  - by rewrite right_id.
+  - rewrite /= IH (comm _ Q _) assoc. done.
 Qed.

 Lemma maybe_wand_sound (mP : option PROP) Q :
@@ -1080,7 +1085,10 @@ Qed.
 Lemma tac_accu Δ P :
  prop_of_env (env_spatial Δ) = P →
  envs_entails Δ P.
-Proof. rewrite envs_entails_eq=><-. apply prop_of_env_sound. Qed.
+Proof.
+  rewrite envs_entails_eq=><-.
+  rewrite prop_of_env_sound /of_envs and_elim_r sep_elim_r //.
+Qed.

 (** * Fresh *)
 Lemma envs_incr_counter_equiv Δ: envs_Forall2 (⊣⊢) Δ (envs_incr_counter Δ).