From e9c6a8ea48f371a32e7e6b658acceb06d49d7bfa Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 16 Feb 2016 19:36:09 +0100
Subject: [PATCH] strengthen auth and heap rules to only require the assertion
 under a later

Whenever clients get this stuff out of invariants, this is much more convenient for them, compared to applying timelessness themselves.
On the other hand, this makes the test proofs slightly more annoying, since they have to manually strip away that later. I am not sure if it is worth having separate lemmas (well, tactics, soon) for that.
Eventually, we should have a tactic which, given "... * P * ... |- ... * \later^n P * ...", automatically gets rid of the P.
---
 heap_lang/heap.v     | 12 ++++++------
 heap_lang/tests.v    |  6 +++---
 program_logic/auth.v |  6 ++++--
 3 files changed, 13 insertions(+), 11 deletions(-)

diff --git a/heap_lang/heap.v b/heap_lang/heap.v
index a3a890a45..f7e5715eb 100644
--- a/heap_lang/heap.v
+++ b/heap_lang/heap.v
@@ -97,7 +97,7 @@ Section heap.
     { by rewrite -pvs_frame_r -(auth_empty E γ) left_id. }
     apply wp_strip_pvs, (auth_fsa (heap_inv HeapI) (wp_fsa (Alloc e)))
       with N γ ∅; simpl; eauto with I.
-    apply sep_mono_r, forall_intro=> h; apply wand_intro_l.
+    rewrite -later_intro. apply sep_mono_r,forall_intro=> h; apply wand_intro_l.
     rewrite -assoc left_id; apply const_elim_sep_l=> ?.
     rewrite {1}[(â–·ownP _)%I]pvs_timeless pvs_frame_r; apply wp_strip_pvs.
     rewrite /wp_fsa -(wp_alloc_pst _ (of_heap h)) //.
@@ -116,13 +116,13 @@ Section heap.
   Lemma wp_load N E γ l v P Q :
     nclose N ⊆ E →
     P ⊑ heap_ctx HeapI γ N →
-    P ⊑ (heap_mapsto HeapI γ l v ★ ▷ (heap_mapsto HeapI γ l v -★ Q v)) →
+    P ⊑ (▷ heap_mapsto HeapI γ l v ★ ▷ (heap_mapsto HeapI γ l v -★ Q v)) →
     P ⊑ wp E (Load (Loc l)) Q.
   Proof.
     rewrite /heap_ctx /heap_inv /heap_mapsto=>HN ? HPQ.
     apply (auth_fsa' (heap_inv HeapI) (wp_fsa _) id)
       with N γ {[ l ↦ Excl v ]}; simpl; eauto with I.
-    rewrite HPQ{HPQ}; apply sep_mono_r, forall_intro=> h; apply wand_intro_l.
+    rewrite HPQ{HPQ}. apply sep_mono_r, forall_intro=> h; apply wand_intro_l.
     rewrite -assoc; apply const_elim_sep_l=> ?.
     rewrite {1}[(â–·ownP _)%I]pvs_timeless pvs_frame_r; apply wp_strip_pvs.
     rewrite -(wp_load_pst _ (<[l:=v]>(of_heap h))) ?lookup_insert //.
@@ -135,7 +135,7 @@ Section heap.
   Lemma wp_store N E γ l v' e v P Q :
     to_val e = Some v → nclose N ⊆ E → 
     P ⊑ heap_ctx HeapI γ N →
-    P ⊑ (heap_mapsto HeapI γ l v' ★
+    P ⊑ (▷ heap_mapsto HeapI γ l v' ★
           ▷ (heap_mapsto HeapI γ l v -★ Q (LitV LitUnit))) →
     P ⊑ wp E (Store (Loc l) e) Q.
   Proof.
@@ -157,7 +157,7 @@ Section heap.
     to_val e1 = Some v1 → to_val e2 = Some v2 → v' ≠ v1 →
     nclose N ⊆ E →
     P ⊑ heap_ctx HeapI γ N →
-    P ⊑ (heap_mapsto HeapI γ l v' ★
+    P ⊑ (▷ heap_mapsto HeapI γ l v' ★
           ▷ (heap_mapsto HeapI γ l v' -★ Q (LitV (LitBool false)))) →
     P ⊑ wp E (Cas (Loc l) e1 e2) Q.
   Proof.
@@ -178,7 +178,7 @@ Section heap.
     to_val e1 = Some v1 → to_val e2 = Some v2 →
     nclose N ⊆ E →
     P ⊑ heap_ctx HeapI γ N →
-    P ⊑ (heap_mapsto HeapI γ l v1 ★
+    P ⊑ (▷ heap_mapsto HeapI γ l v1 ★
           ▷ (heap_mapsto HeapI γ l v2 -★ Q (LitV (LitBool true)))) →
     P ⊑ wp E (Cas (Loc l) e1 e2) Q.
   Proof.
diff --git a/heap_lang/tests.v b/heap_lang/tests.v
index 8d98a5ee0..c4d9b90ff 100644
--- a/heap_lang/tests.v
+++ b/heap_lang/tests.v
@@ -35,14 +35,14 @@ Section LiftingTests.
     rewrite -later_intro; apply forall_intro=>l; apply wand_intro_l.
     wp_rec.
     wp_focus (! LocV l)%L.
-    eapply wp_load; eauto with I; []. apply sep_mono_r.
+    eapply wp_load; eauto with I; []. rewrite -later_intro. apply sep_mono_r.
     rewrite -later_intro; apply wand_intro_l.
     wp_bin_op.
     wp_focus (_ <- _)%L.
-    eapply wp_store; eauto with I; []. apply sep_mono_r.
+    eapply wp_store; eauto with I; []. rewrite -later_intro. apply sep_mono_r.
     rewrite -later_intro. apply wand_intro_l.
     wp_rec.
-    eapply wp_load; eauto with I; []. apply sep_mono; first done.
+    eapply wp_load; eauto with I; []. rewrite -later_intro. apply sep_mono_r.
     rewrite -later_intro. apply wand_intro_l.
     by apply const_intro.
   Qed.
diff --git a/program_logic/auth.v b/program_logic/auth.v
index 4e94acc1c..cb70202c6 100644
--- a/program_logic/auth.v
+++ b/program_logic/auth.v
@@ -100,7 +100,7 @@ Section auth.
     fsaV →
     nclose N ⊆ E →
     P ⊑ auth_ctx AuthI γ N φ →
-    P ⊑ (auth_own AuthI γ a ★ ∀ a',
+    P ⊑ (▷ auth_own AuthI γ a ★ ∀ a',
           ■ ✓ (a ⋅ a') ★ ▷ φ (a ⋅ a') -★
           fsa (E ∖ nclose N) (λ x, ∃ L Lv (Hup : LocalUpdate Lv L),
             ■ (Lv a ∧ ✓ (L a ⋅ a')) ★ ▷ φ (L a ⋅ a') ★
@@ -110,6 +110,8 @@ Section auth.
     rewrite /auth_ctx=>? HN Hinv Hinner.
     eapply (inv_fsa fsa); eauto. rewrite Hinner=>{Hinner Hinv P HN}.
     apply wand_intro_l. rewrite assoc.
+    rewrite (pvs_timeless (E ∖ N)) pvs_frame_l pvs_frame_r.
+    apply (fsa_strip_pvs fsa).
     rewrite (auth_opened (E ∖ N)) !pvs_frame_r !sep_exist_r.
     apply (fsa_strip_pvs fsa). apply exist_elim=>a'.
     rewrite (forall_elim a'). rewrite [(▷_ ★ _)%I]comm.
@@ -130,7 +132,7 @@ Section auth.
     fsaV →
     nclose N ⊆ E →
     P ⊑ auth_ctx AuthI γ N φ →
-    P ⊑ (auth_own AuthI γ a ★ (∀ a',
+    P ⊑ (▷ auth_own AuthI γ a ★ (∀ a',
           ■ ✓ (a ⋅ a') ★ ▷ φ (a ⋅ a') -★
           fsa (E ∖ nclose N) (λ x,
             ■ (Lv a ∧ ✓ (L a ⋅ a')) ★ ▷ φ (L a ⋅ a') ★
-- 
GitLab