From 00444b07b5f38dcf42c652b1409782403c75f0a5 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 6 Dec 2016 18:49:10 +0100
Subject: [PATCH] new definition of atomicity: reduces in one step to sth. that
 doesn't reduce further

---
 heap_lang/lifting.v           |  3 +--
 heap_lang/tactics.v           |  1 +
 program_logic/ectx_language.v |  2 +-
 program_logic/ectx_lifting.v  | 11 ++++-------
 program_logic/language.v      |  6 +++++-
 program_logic/lifting.v       | 20 +++++++++-----------
 program_logic/weakestpre.v    | 11 ++++++++---
 7 files changed, 29 insertions(+), 25 deletions(-)

diff --git a/heap_lang/lifting.v b/heap_lang/lifting.v
index fbdde12b2..eb07aaa0b 100644
--- a/heap_lang/lifting.v
+++ b/heap_lang/lifting.v
@@ -53,8 +53,7 @@ Proof.
   iIntros (Φ) "HP HΦ".
   iApply (wp_lift_atomic_head_step (Alloc (of_val v)) σ); eauto.
   iFrame "HP". iNext. iIntros (v2 σ2 ef) "[% HP]". inv_head_step.
-  match goal with H: _ = of_val v2 |- _ => apply (inj of_val (LitV _)) in H end.
-  subst v2. iSplit. iApply "HΦ"; by iSplit. by iApply big_sepL_nil.
+  iSplitL; last by iApply big_sepL_nil. iApply "HΦ". by iSplit.
 Qed.
 
 Lemma wp_load_pst E σ l v :
diff --git a/heap_lang/tactics.v b/heap_lang/tactics.v
index 4d9c1633c..47d495d0e 100644
--- a/heap_lang/tactics.v
+++ b/heap_lang/tactics.v
@@ -187,6 +187,7 @@ Lemma atomic_correct e : atomic e → language.atomic (to_expr e).
 Proof.
   intros He. apply ectx_language_atomic.
   - intros σ e' σ' ef.
+    intros H; apply language.val_irreducible; revert H.
     destruct e; simpl; try done; repeat (case_match; try done);
     inversion 1; rewrite ?to_of_val; eauto. subst.
     unfold subst'; repeat (case_match || contradiction || simplify_eq/=); eauto.
diff --git a/program_logic/ectx_language.v b/program_logic/ectx_language.v
index ea0adc138..b86522443 100644
--- a/program_logic/ectx_language.v
+++ b/program_logic/ectx_language.v
@@ -90,7 +90,7 @@ Section ectx_language.
   Proof. intros (e'&σ'&efs&?). eexists e', σ', efs. by apply head_prim_step. Qed.
 
   Lemma ectx_language_atomic e :
-    (∀ σ e' σ' efs, head_step e σ e' σ' efs → is_Some (to_val e')) →
+    (∀ σ e' σ' efs, head_step e σ e' σ' efs → irreducible e' σ') →
     (∀ K e', e = fill K e' → to_val e' = None → K = empty_ectx) →
     atomic e.
   Proof.
diff --git a/program_logic/ectx_lifting.v b/program_logic/ectx_lifting.v
index e075f00b7..a95cb59df 100644
--- a/program_logic/ectx_lifting.v
+++ b/program_logic/ectx_lifting.v
@@ -39,19 +39,17 @@ Proof.
 Qed.
 
 Lemma wp_lift_atomic_head_step {E Φ} e1 σ1 :
-  atomic e1 →
   head_reducible e1 σ1 →
-  ▷ ownP σ1 ∗ ▷ (∀ v2 σ2 efs,
-  ⌜head_step e1 σ1 (of_val v2) σ2 efs⌝ ∧ ownP σ2 -∗
-    Φ v2 ∗ [∗ list] ef ∈ efs, WP ef {{ _, True }})
+  ▷ ownP σ1 ∗ ▷ (∀ e2 σ2 efs,
+  ⌜head_step e1 σ1 e2 σ2 efs⌝ ∧ ownP σ2 -∗
+    default False (to_val e2) Φ ∗ [∗ list] ef ∈ efs, WP ef {{ _, True }})
   ⊢ WP e1 @ E {{ Φ }}.
 Proof.
-  iIntros (??) "[? H]". iApply wp_lift_atomic_step; eauto. iFrame. iNext.
+  iIntros (?) "[? H]". iApply wp_lift_atomic_step; eauto. iFrame. iNext.
   iIntros (???) "[% ?]". iApply "H". eauto.
 Qed.
 
 Lemma wp_lift_atomic_det_head_step {E Φ e1} σ1 v2 σ2 efs :
-  atomic e1 →
   head_reducible e1 σ1 →
   (∀ e2' σ2' efs', head_step e1 σ1 e2' σ2' efs' →
     σ2 = σ2' ∧ to_val e2' = Some v2 ∧ efs = efs') →
@@ -61,7 +59,6 @@ Lemma wp_lift_atomic_det_head_step {E Φ e1} σ1 v2 σ2 efs :
 Proof. eauto using wp_lift_atomic_det_step. Qed.
 
 Lemma wp_lift_atomic_det_head_step' {E e1} σ1 v2 σ2 :
-  atomic e1 →
   head_reducible e1 σ1 →
   (∀ e2' σ2' efs', head_step e1 σ1 e2' σ2' efs' →
     σ2 = σ2' ∧ to_val e2' = Some v2 ∧ [] = efs') →
diff --git a/program_logic/language.v b/program_logic/language.v
index a1955ed2f..a1eff5564 100644
--- a/program_logic/language.v
+++ b/program_logic/language.v
@@ -34,8 +34,10 @@ Section language.
 
   Definition reducible (e : expr Λ) (σ : state Λ) :=
     ∃ e' σ' efs, prim_step e σ e' σ' efs.
+  Definition irreducible (e : expr Λ) (σ : state Λ) :=
+    ∀e' σ' efs, ~prim_step e σ e' σ' efs. 
   Definition atomic (e : expr Λ) : Prop :=
-    ∀ σ e' σ' efs, prim_step e σ e' σ' efs → is_Some (to_val e').
+    ∀ σ e' σ' efs, prim_step e σ e' σ' efs → irreducible e' σ'.
   Inductive step (ρ1 ρ2 : cfg Λ) : Prop :=
     | step_atomic e1 σ1 e2 σ2 efs t1 t2 :
        ρ1 = (t1 ++ e1 :: t2, σ1) →
@@ -47,6 +49,8 @@ Section language.
   Proof. intros <-. by rewrite to_of_val. Qed.
   Lemma reducible_not_val e σ : reducible e σ → to_val e = None.
   Proof. intros (?&?&?&?); eauto using val_stuck. Qed.
+  Lemma val_irreducible e σ : is_Some (to_val e) → irreducible e σ.
+  Proof. intros [??] ??? ?%val_stuck. by destruct (to_val e). Qed.
   Global Instance of_val_inj : Inj (=) (=) (@of_val Λ).
   Proof. by intros v v' Hv; apply (inj Some); rewrite -!to_of_val Hv. Qed.
 End language.
diff --git a/program_logic/lifting.v b/program_logic/lifting.v
index cac55e484..54c060992 100644
--- a/program_logic/lifting.v
+++ b/program_logic/lifting.v
@@ -45,23 +45,21 @@ Qed.
 
 (** Derived lifting lemmas. *)
 Lemma wp_lift_atomic_step {E Φ} e1 σ1 :
-  atomic e1 →
   reducible e1 σ1 →
-  (▷ ownP σ1 ∗ ▷ ∀ v2 σ2 efs, ⌜prim_step e1 σ1 (of_val v2) σ2 efs⌝ ∗ ownP σ2 -∗
-    Φ v2 ∗ [∗ list] ef ∈ efs, WP ef {{ _, True }})
+  (▷ ownP σ1 ∗ ▷ ∀ e2 σ2 efs, ⌜prim_step e1 σ1 e2 σ2 efs⌝ ∗ ownP σ2 -∗
+    default False (to_val e2) Φ ∗ [∗ list] ef ∈ efs, WP ef {{ _, True }})
   ⊢ WP e1 @ E {{ Φ }}.
 Proof.
-  iIntros (Hatomic ?) "[Hσ H]". iApply (wp_lift_step E _ e1).
+  iIntros (?) "[Hσ H]". iApply (wp_lift_step E _ e1).
   iMod (fupd_intro_mask' E ∅) as "Hclose"; first set_solver. iModIntro.
   iExists σ1. iFrame "Hσ"; iSplit; eauto.
   iNext; iIntros (e2 σ2 efs) "[% Hσ]".
-  edestruct (Hatomic σ1 e2 σ2 efs) as [v2 <-%of_to_val]; eauto.
-  iDestruct ("H" $! v2 σ2 efs with "[Hσ]") as "[HΦ $]"; first by eauto.
-  iMod "Hclose". iApply wp_value; auto using to_of_val.
+  iDestruct ("H" $! e2 σ2 efs with "[Hσ]") as "[HΦ $]"; first by eauto.
+  destruct (to_val e2) eqn:?; last by iExFalso.
+  iMod "Hclose". iApply wp_value; auto using to_of_val. done.
 Qed.
 
 Lemma wp_lift_atomic_det_step {E Φ e1} σ1 v2 σ2 efs :
-  atomic e1 →
   reducible e1 σ1 →
   (∀ e2' σ2' efs', prim_step e1 σ1 e2' σ2' efs' →
                    σ2 = σ2' ∧ to_val e2' = Some v2 ∧ efs = efs') →
@@ -69,9 +67,9 @@ Lemma wp_lift_atomic_det_step {E Φ e1} σ1 v2 σ2 efs :
     Φ v2 ∗ [∗ list] ef ∈ efs, WP ef {{ _, True }})
   ⊢ WP e1 @ E {{ Φ }}.
 Proof.
-  iIntros (?? Hdet) "[Hσ1 Hσ2]". iApply (wp_lift_atomic_step _ σ1); try done.
-  iFrame. iNext. iIntros (v2' σ2' efs') "[% Hσ2']".
-  edestruct Hdet as (->&->%of_to_val%(inj of_val)&->). done. by iApply "Hσ2".
+  iIntros (? Hdet) "[Hσ1 Hσ2]". iApply (wp_lift_atomic_step _ σ1); try done.
+  iFrame. iNext. iIntros (e2' σ2' efs') "[% Hσ2']".
+  edestruct Hdet as (->&Hval&->). done. rewrite Hval. by iApply "Hσ2".
 Qed.
 
 Lemma wp_lift_pure_det_step `{Inhabited (state Λ)} {E Φ} e1 e2 efs :
diff --git a/program_logic/weakestpre.v b/program_logic/weakestpre.v
index 6999d2311..5cf0ae793 100644
--- a/program_logic/weakestpre.v
+++ b/program_logic/weakestpre.v
@@ -197,9 +197,14 @@ Proof.
   { iDestruct "H" as (v') "[% ?]"; simplify_eq. }
   iMod ("H" $! σ1 with "Hσ") as "[$ H]".
   iModIntro. iNext. iIntros (e2 σ2 efs Hstep).
-  destruct (Hatomic _ _ _ _ Hstep) as [v <-%of_to_val].
-  iMod ("H" $! _ σ2 efs with "[#]") as "($ & H & $)"; auto.
-  iMod (wp_value_inv with "H") as ">H". by iApply wp_value'.
+  iMod ("H" with "* []") as "(Hphy & H & $)"; first done.
+  rewrite wp_unfold /wp_pre. iDestruct "H" as "[H|H]".
+  - iDestruct "H" as (v) "[% >>?]". iModIntro. iFrame.
+    rewrite -(of_to_val e2 v) //. by iApply wp_value'.
+  - iDestruct "H" as "[_ H]".
+    iMod ("H" with "* Hphy") as "[H _]".
+    iDestruct "H" as %(? & ? & ? & ?). exfalso.
+    by eapply (Hatomic _ _ _ _ Hstep).
 Qed.
 
 Lemma wp_fupd_step E1 E2 e P Φ :
-- 
GitLab