From 98b48609e50076443f2c83bb83eaf829eb17c61b Mon Sep 17 00:00:00 2001
From: Ralf Jung <post@ralfj.de>
Date: Tue, 2 Feb 2016 11:14:23 +0100
Subject: [PATCH] make proofs of physical lifting much shorter

---
 barrier/heap_lang.v         | 48 +++++++++++++++++++
 barrier/heap_lang_tactics.v |  6 ++-
 barrier/lifting.v           | 96 +++++++++++++++++++------------------
 3 files changed, 102 insertions(+), 48 deletions(-)

diff --git a/barrier/heap_lang.v b/barrier/heap_lang.v
index d2f508384..2732cd83f 100644
--- a/barrier/heap_lang.v
+++ b/barrier/heap_lang.v
@@ -105,7 +105,9 @@ Inductive ectx_item :=
   | CasLCtx (e1 : expr)  (e2 : expr)
   | CasMCtx (v0 : val) (e2 : expr)
   | CasRCtx (v0 : val) (v1 : val).
+
 Notation ectx := (list ectx_item).
+
 Implicit Types Ki : ectx_item.
 Implicit Types K : ectx.
 
@@ -132,6 +134,7 @@ Definition ectx_item_fill (Ki : ectx_item) (e : expr) : expr :=
   | CasMCtx v0 e2 => Cas (of_val v0) e e2
   | CasRCtx v0 v1 => Cas (of_val v0) (of_val v1) e
   end.
+
 Instance ectx_fill : Fill ectx expr :=
   fix go K e := let _ : Fill _ _ := @go in
   match K with [] => e | Ki :: K => ectx_item_fill Ki (fill K e) end.
@@ -181,6 +184,9 @@ Inductive head_step : expr -> state -> expr -> state -> option expr -> Prop :=
      σ !! l = Some v1 →
      head_step (Cas (Loc l) e1 e2) σ LitTrue (<[l:=v2]>σ) None.
 
+Definition head_reducible e σ : Prop :=
+  ∃ e' σ' ef, head_step e σ e' σ' ef.
+
 (** Atomic expressions *)
 Definition atomic (e: expr) :=
   match e with
@@ -202,40 +208,53 @@ Inductive prim_step
 (** Basic properties about the language *)
 Lemma to_of_val v : to_val (of_val v) = Some v.
 Proof. by induction v; simplify_option_equality. Qed.
+
 Lemma of_to_val e v : to_val e = Some v → of_val v = e.
 Proof.
   revert v; induction e; intros; simplify_option_equality; auto with f_equal.
 Qed.
+
 Instance: Injective (=) (=) of_val.
 Proof. by intros ?? Hv; apply (injective Some); rewrite -!to_of_val Hv. Qed.
+
 Instance ectx_item_fill_inj Ki : Injective (=) (=) (ectx_item_fill Ki).
 Proof. destruct Ki; intros ???; simplify_equality'; auto with f_equal. Qed.
+
 Instance ectx_fill_inj K : Injective (=) (=) (fill K).
 Proof. red; induction K as [|Ki K IH]; naive_solver. Qed.
+
 Lemma fill_app K1 K2 e : fill (K1 ++ K2) e = fill K1 (fill K2 e).
 Proof. revert e; induction K1; simpl; auto with f_equal. Qed.
+
 Lemma fill_val K e : is_Some (to_val (fill K e)) → is_Some (to_val e).
 Proof.
   intros [v' Hv']; revert v' Hv'.
   induction K as [|[]]; intros; simplify_option_equality; eauto.
 Qed.
+
 Lemma fill_not_val K e : to_val e = None → to_val (fill K e) = None.
 Proof. rewrite !eq_None_not_Some; eauto using fill_val. Qed.
+
 Lemma values_head_stuck e1 σ1 e2 σ2 ef :
   head_step e1 σ1 e2 σ2 ef → to_val e1 = None.
 Proof. destruct 1; naive_solver. Qed.
+
 Lemma values_stuck e1 σ1 e2 σ2 ef : prim_step e1 σ1 e2 σ2 ef → to_val e1 = None.
 Proof. intros [??? -> -> ?]; eauto using fill_not_val, values_head_stuck. Qed.
+
 Lemma atomic_not_val e : atomic e → to_val e = None.
 Proof. destruct e; naive_solver. Qed.
+
 Lemma atomic_fill K e : atomic (fill K e) → to_val e = None → K = [].
 Proof.
   rewrite eq_None_not_Some.
   destruct K as [|[]]; naive_solver eauto using fill_val.
 Qed.
+
 Lemma atomic_head_step e1 σ1 e2 σ2 ef :
   atomic e1 → head_step e1 σ1 e2 σ2 ef → is_Some (to_val e2).
 Proof. destruct 2; simpl; rewrite ?to_of_val; naive_solver. Qed.
+
 Lemma atomic_step e1 σ1 e2 σ2 ef :
   atomic e1 → prim_step e1 σ1 e2 σ2 ef → is_Some (to_val e2).
 Proof.
@@ -243,9 +262,11 @@ Proof.
   assert (K = []) as -> by eauto 10 using atomic_fill, values_head_stuck.
   naive_solver eauto using atomic_head_step.
 Qed.
+
 Lemma head_ctx_step_val Ki e σ1 e2 σ2 ef :
   head_step (ectx_item_fill Ki e) σ1 e2 σ2 ef → is_Some (to_val e).
 Proof. destruct Ki; inversion_clear 1; simplify_option_equality; eauto. Qed.
+
 Lemma fill_item_inj Ki1 Ki2 e1 e2 :
   to_val e1 = None → to_val e2 = None →
   ectx_item_fill Ki1 e1 = ectx_item_fill Ki2 e2 → Ki1 = Ki2.
@@ -255,6 +276,7 @@ Proof.
     | H : to_val (of_val _) = None |- _ => by rewrite to_of_val in H
     end; auto.
 Qed.
+
 (* When something does a step, and another decomposition of the same expression
 has a non-val [e] in the hole, then [K] is a left sub-context of [K'] - in
 other words, [e] also contains the reducible expression *)
@@ -270,12 +292,29 @@ Proof.
   cut (Ki = Ki'); [naive_solver eauto using prefix_of_cons|].
   eauto using fill_item_inj, values_head_stuck, fill_not_val.
 Qed.
+
+Lemma prim_head_step e1 σ1 e2 σ2 ef :
+  head_reducible e1 σ1 →
+  prim_step e1 σ1 e2 σ2 ef →
+  head_step e1 σ1 e2 σ2 ef.
+Proof.
+  intros (e2'' & σ2'' & ef'' & Hstep'')  [K' e1' e2' Heq1 Heq2  Hstep].
+  assert (K' `prefix_of` []) as Hemp.
+  { eapply step_by_val; last first.
+    - eexact Hstep''.
+    - eapply values_head_stuck. eexact Hstep.
+    - done. }
+  destruct K'; last by (exfalso; eapply prefix_of_nil_not; eassumption).
+  by subst e1 e2.
+Qed.
+
 Lemma alloc_fresh e v σ :
   let l := fresh (dom _ σ) in
   to_val e = Some v → head_step (Alloc e) σ (Loc l) (<[l:=v]>σ) None.
 Proof.
   by intros; apply AllocS, (not_elem_of_dom (D:=gset positive)), is_fresh.
 Qed.
+
 End heap_lang.
 
 (** Language *)
@@ -284,6 +323,7 @@ Program Canonical Structure heap_lang : language := {|
   of_val := heap_lang.of_val; to_val := heap_lang.to_val;
   atomic := heap_lang.atomic; prim_step := heap_lang.prim_step;
 |}.
+
 Solve Obligations with eauto using heap_lang.to_of_val, heap_lang.of_to_val,
   heap_lang.values_stuck, heap_lang.atomic_not_val, heap_lang.atomic_step.
 Global Instance heap_lang_ctx : CtxLanguage heap_lang heap_lang.ectx.
@@ -299,3 +339,11 @@ Proof.
     exists (fill K' e2''); rewrite heap_lang.fill_app; split; auto.
     econstructor; eauto.
 Qed.
+
+Lemma head_reducible_reducible e σ :
+  heap_lang.head_reducible e σ → reducible e σ.
+Proof.
+  intros H. destruct H; destruct_conjs.
+  do 3 eexists.
+  eapply heap_lang.Ectx_step with (K:=[]); last eassumption; done.
+Qed.
diff --git a/barrier/heap_lang_tactics.v b/barrier/heap_lang_tactics.v
index 5a3f3d081..bac971cdc 100644
--- a/barrier/heap_lang_tactics.v
+++ b/barrier/heap_lang_tactics.v
@@ -61,7 +61,8 @@ Ltac reshape_expr e tac :=
   end in go (@nil ectx_item) e.
 
 Ltac do_step tac :=
-  try match goal with |- reducible _ _ => eexists _, _, _ end;
+  try match goal with |- language.reducible _ _ => eexists _, _, _ end;
+  try match goal with |- head_reducible _ _ => eexists _, _, _ end;
   simpl;
   match goal with
   | |- prim_step ?e1 ?σ1 ?e2 ?σ2 ?ef =>
@@ -69,4 +70,7 @@ Ltac do_step tac :=
        eapply Ectx_step with K e1' _); [reflexivity|reflexivity|];
        first [apply alloc_fresh|econstructor];
        rewrite ?to_of_val; tac; fail
+  | |- head_step ?e1 ?σ1 ?e2 ?σ2 ?ef =>
+       first [apply alloc_fresh|econstructor];
+       rewrite ?to_of_val; tac; fail
   end.
diff --git a/barrier/lifting.v b/barrier/lifting.v
index cd947d259..921116856 100644
--- a/barrier/lifting.v
+++ b/barrier/lifting.v
@@ -2,7 +2,8 @@ Require Import prelude.gmap iris.lifting.
 Require Export iris.weakestpre barrier.heap_lang_tactics.
 Import uPred.
 Import heap_lang.
-Local Hint Extern 0 (reducible _ _) => do_step ltac:(eauto 2).
+Local Hint Extern 0 (language.reducible _ _) => do_step ltac:(eauto 2).
+Local Hint Extern 0 (head_reducible _ _) => do_step ltac:(eauto 2).
 
 Section lifting.
 Context {Σ : iFunctor}.
@@ -16,84 +17,75 @@ Lemma wp_bind {E e} K Q :
 Proof. apply wp_bind. Qed.
 
 (** Base axioms for core primitives of the language: Stateful reductions. *)
-Lemma wp_lift_step E1 E2 (φ : expr → state → Prop) Q e1 σ1 :
-  E1 ⊆ E2 → to_val e1 = None →
-  reducible e1 σ1 →
-  (∀ e2 σ2 ef, prim_step e1 σ1 e2 σ2 ef → ef = None ∧ φ e2 σ2) →
-  pvs E2 E1 (ownP σ1 ★ ▷ ∀ e2 σ2, (■ φ e2 σ2 ∧ ownP σ2) -★
-    pvs E1 E2 (wp E2 e2 Q))
-  ⊑ wp E2 e1 Q.
-Proof.
-  intros ? He Hsafe Hstep.
-  rewrite -(wp_lift_step E1 E2 (λ e' σ' ef, ef = None ∧ φ e' σ') _ _ σ1) //.
-  apply pvs_mono, sep_mono, later_mono; first done.
-  apply forall_mono=>e2; apply forall_mono=>σ2.
-  apply forall_intro=>ef; apply wand_intro_l.
-  rewrite always_and_sep_l' -associative -always_and_sep_l'.
-  apply const_elim_l=>-[-> ?] /=.
-  by rewrite const_equiv // left_id wand_elim_r right_id.
-Qed.
-
-(* TODO RJ: Figure out some better way to make the
-   postcondition a predicate over a *location* *)
 Lemma wp_alloc_pst E σ e v Q :
   to_val e = Some v →
   (ownP σ ★ ▷ (∀ l, ■(σ !! l = None) ∧ ownP (<[l:=v]>σ) -★ Q (LocV l)))
        ⊑ wp E (Alloc e) Q.
 Proof.
-  intros; set (φ e' σ' := ∃ l, e' = Loc l ∧ σ' = <[l:=v]>σ ∧ σ !! l = None).
-  rewrite -(wp_lift_step E E φ _ _  σ) // /φ; last by intros; inv_step; eauto.
+  intros; set (φ e' σ' ef := ∃ l, e' = Loc l ∧ σ' = <[l:=v]>σ ∧ σ !! l = None
+                                ∧ ef = (None : option expr)).
+  rewrite -(wp_lift_step E E φ _ _  σ) // /φ; last (by intros; inv_step; eauto); [].
   rewrite -pvs_intro. apply sep_mono, later_mono; first done.
-  apply forall_intro=>e2; apply forall_intro=>σ2; apply wand_intro_l.
+  apply forall_intro=>e2; apply forall_intro=>σ2; apply forall_intro=>ef.
+  apply wand_intro_l.
   rewrite -pvs_intro always_and_sep_l' -associative -always_and_sep_l'.
-  apply const_elim_l=>-[l [-> [-> ?]]].
-  by rewrite (forall_elim l) const_equiv // left_id wand_elim_r -wp_value'.
+  apply const_elim_l=>-[l [-> [-> [? ->]]]].
+  rewrite right_id (forall_elim l) const_equiv //.
+  by rewrite left_id wand_elim_r -wp_value'.
 Qed.
+
+Lemma wp_lift_atomic_det_step {E Q e1} σ1 v2 σ2 :
+  to_val e1 = None →
+  head_reducible e1 σ1 →
+  (∀ e' σ' ef, head_step e1 σ1 e' σ' ef → ef = None ∧ e' = of_val v2 ∧ σ' = σ2) →
+  (ownP σ1 ★ ▷ (ownP σ2 -★ Q v2)) ⊑ wp E e1 Q.
+Proof.
+  intros He Hsafe Hstep.
+  rewrite -(wp_lift_step E E (λ e' σ' ef, ef = None ∧ e' = of_val v2 ∧ σ' = σ2) _ e1 σ1) //; last first. 
+  { intros. by apply Hstep, prim_head_step. }
+  { by apply head_reducible_reducible. }
+  rewrite -pvs_intro. apply sep_mono, later_mono; first done.
+  apply forall_intro=>e2'; apply forall_intro=>σ2'.
+  apply forall_intro=>ef; apply wand_intro_l.
+  rewrite always_and_sep_l' -associative -always_and_sep_l'.
+  apply const_elim_l=>-[-> [-> ->]] /=.
+  rewrite -pvs_intro right_id -wp_value.
+  by rewrite wand_elim_r.
+Qed.
+
+
 Lemma wp_load_pst E σ l v Q :
   σ !! l = Some v →
   (ownP σ ★ ▷ (ownP σ -★ Q v)) ⊑ wp E (Load (Loc l)) Q.
 Proof.
-  intros; rewrite -(wp_lift_step E E (λ e' σ', e' = of_val v ∧ σ' = σ)) //;
-    last by intros; inv_step; eauto.
-  rewrite -pvs_intro; apply sep_mono, later_mono; first done.
-  apply forall_intro=>e2; apply forall_intro=>σ2; apply wand_intro_l.
-  rewrite -pvs_intro always_and_sep_l' -associative -always_and_sep_l'.
-  apply const_elim_l=>-[-> ->]; by rewrite wand_elim_r -wp_value.
+  intros; rewrite -(wp_lift_atomic_det_step σ v σ) //;
+    last (by intros; inv_step; eauto).
 Qed.
+
 Lemma wp_store_pst E σ l e v v' Q :
   to_val e = Some v → σ !! l = Some v' →
   (ownP σ ★ ▷ (ownP (<[l:=v]>σ) -★ Q LitUnitV)) ⊑ wp E (Store (Loc l) e) Q.
 Proof.
   intros.
-  rewrite -(wp_lift_step E E (λ e' σ', e' = LitUnit ∧ σ' = <[l:=v]>σ)) //;
+  rewrite -(wp_lift_atomic_det_step σ LitUnitV (<[l:=v]>σ)) //;
     last by intros; inv_step; eauto.
-  rewrite -pvs_intro; apply sep_mono, later_mono; first done.
-  apply forall_intro=>e2; apply forall_intro=>σ2; apply wand_intro_l.
-  rewrite -pvs_intro always_and_sep_l' -associative -always_and_sep_l'.
-  apply const_elim_l=>-[-> ->]; by rewrite wand_elim_r -wp_value'.
 Qed.
+
 Lemma wp_cas_fail_pst E σ l e1 v1 e2 v2 v' Q :
   to_val e1 = Some v1 → to_val e2 = Some v2 → σ !! l = Some v' → v' ≠ v1 →
   (ownP σ ★ ▷ (ownP σ -★ Q LitFalseV)) ⊑ wp E (Cas (Loc l) e1 e2) Q.
 Proof.
-  intros; rewrite -(wp_lift_step E E (λ e' σ', e' = LitFalse ∧ σ' = σ)) //;
+  intros; rewrite -(wp_lift_atomic_det_step σ LitFalseV σ) //;
     last by intros; inv_step; eauto.
-  rewrite -pvs_intro; apply sep_mono, later_mono; first done.
-  apply forall_intro=>e2'; apply forall_intro=>σ2; apply wand_intro_l.
-  rewrite -pvs_intro always_and_sep_l' -associative -always_and_sep_l'.
-  apply const_elim_l=>-[-> ->]; by rewrite wand_elim_r -wp_value'.
 Qed.
+
 Lemma wp_cas_suc_pst E σ l e1 v1 e2 v2 Q :
   to_val e1 = Some v1 → to_val e2 = Some v2 → σ !! l = Some v1 →
   (ownP σ ★ ▷ (ownP (<[l:=v2]>σ) -★ Q LitTrueV)) ⊑ wp E (Cas (Loc l) e1 e2) Q.
 Proof.
   intros.
-  rewrite -(wp_lift_step E E (λ e' σ', e' = LitTrue ∧ σ' = <[l:=v2]>σ)) //;
+  rewrite -(wp_lift_atomic_det_step σ LitTrueV (<[l:=v2]>σ)) //;
     last by intros; inv_step; eauto.
-  rewrite -pvs_intro; apply sep_mono, later_mono; first done.
-  apply forall_intro=>e2'; apply forall_intro=>σ2; apply wand_intro_l.
-  rewrite -pvs_intro always_and_sep_l' -associative -always_and_sep_l'.
-  apply const_elim_l=>-[-> ->]; by rewrite wand_elim_r -wp_value'.
 Qed.
 
 (** Base axioms for core primitives of the language: Stateless reductions *)
@@ -107,6 +99,7 @@ Proof.
   apply sep_intro_True_l; last done.
   by rewrite -wp_value' //; apply const_intro.
 Qed.
+
 Lemma wp_lift_pure_step E (φ : expr → Prop) Q e1 :
   to_val e1 = None →
   (∀ σ1, reducible e1 σ1) →
@@ -118,6 +111,7 @@ Proof.
   apply impl_intro_l, const_elim_l=>-[-> ?] /=.
   by rewrite const_equiv // left_id right_id.
 Qed.
+
 Lemma wp_rec E ef e v Q :
   to_val e = Some v →
   ▷ wp E ef.[Rec ef, e /] Q ⊑ wp E (App (Rec ef) e) Q.
@@ -126,6 +120,7 @@ Proof.
     Q (App (Rec ef) e)) //=; last by intros; inv_step; eauto.
   by apply later_mono, forall_intro=>e2; apply impl_intro_l, const_elim_l=>->.
 Qed.
+
 Lemma wp_plus E n1 n2 Q :
   ▷ Q (LitNatV (n1 + n2)) ⊑ wp E (Plus (LitNat n1) (LitNat n2)) Q.
 Proof.
@@ -134,6 +129,7 @@ Proof.
   apply later_mono, forall_intro=>e2; apply impl_intro_l, const_elim_l=>->.
   by rewrite -wp_value'.
 Qed.
+
 Lemma wp_le_true E n1 n2 Q :
   n1 ≤ n2 →
   ▷ Q LitTrueV ⊑ wp E (Le (LitNat n1) (LitNat n2)) Q.
@@ -143,6 +139,7 @@ Proof.
   apply later_mono, forall_intro=>e2; apply impl_intro_l, const_elim_l=>->.
   by rewrite -wp_value'.
 Qed.
+
 Lemma wp_le_false E n1 n2 Q :
   n1 > n2 →
   ▷ Q LitFalseV ⊑ wp E (Le (LitNat n1) (LitNat n2)) Q.
@@ -152,6 +149,7 @@ Proof.
   apply later_mono, forall_intro=>e2; apply impl_intro_l, const_elim_l=>->.
   by rewrite -wp_value'.
 Qed.
+
 Lemma wp_fst E e1 v1 e2 v2 Q :
   to_val e1 = Some v1 → to_val e2 = Some v2 →
   ▷Q v1 ⊑ wp E (Fst (Pair e1 e2)) Q.
@@ -161,6 +159,7 @@ Proof.
   apply later_mono, forall_intro=>e2'; apply impl_intro_l, const_elim_l=>->.
   by rewrite -wp_value'.
 Qed.
+
 Lemma wp_snd E e1 v1 e2 v2 Q :
   to_val e1 = Some v1 → to_val e2 = Some v2 →
   ▷ Q v2 ⊑ wp E (Snd (Pair e1 e2)) Q.
@@ -170,6 +169,7 @@ Proof.
   apply later_mono, forall_intro=>e2'; apply impl_intro_l, const_elim_l=>->.
   by rewrite -wp_value'.
 Qed.
+
 Lemma wp_case_inl E e0 v0 e1 e2 Q :
   to_val e0 = Some v0 →
   ▷ wp E e1.[e0/] Q ⊑ wp E (Case (InjL e0) e1 e2) Q.
@@ -178,6 +178,7 @@ Proof.
     (Case (InjL e0) e1 e2)) //=; last by intros; inv_step; eauto.
   by apply later_mono, forall_intro=>e1'; apply impl_intro_l, const_elim_l=>->.
 Qed.
+
 Lemma wp_case_inr E e0 v0 e1 e2 Q :
   to_val e0 = Some v0 →
   ▷ wp E e2.[e0/] Q ⊑ wp E (Case (InjR e0) e1 e2) Q.
@@ -197,4 +198,5 @@ Proof.
   * rewrite -wp_le_true; auto.
   * rewrite -wp_le_false; auto with lia.
 Qed.
+
 End lifting.
-- 
GitLab