simplify stateful lifting lemmas; prove fork lemma

barrier/heap_lang.v

@@ -280,22 +280,20 @@ Inductive prim_step : expr -> state -> expr -> state -> option expr -> Prop :=
     prim_step (Cas (Loc l) e1 e2) σ LitTrue (<[l:=v2]>σ) None
 .
 
-Definition reducible e: Prop :=
-  exists σ e' σ' ef, prim_step e σ e' σ' ef.
+Definition reducible e σ : Prop :=
+  ∃ e' σ' ef, prim_step e σ e' σ' ef.
 
-Lemma reducible_not_value e:
-  reducible e -> e2v e = None.
+Lemma reducible_not_value e σ :
+  reducible e σ → e2v e = None.
 Proof.
-  intros (σ' & e'' & σ'' & ef & Hstep). destruct Hstep; simpl in *; reflexivity.
+  intros (e' & σ' & ef & Hstep). destruct Hstep; simpl in *; reflexivity.
 Qed.
 
-Definition stuck (e : expr) : Prop :=
-  forall K e',
-    e = fill K e' ->
-    ~reducible e'.
+Definition stuck (e : expr) σ : Prop :=
+  ∀ K e', e = fill K e' → ~reducible e' σ.
 
-Lemma values_stuck v :
-  stuck (v2e v).
+Lemma values_stuck v σ :
+  stuck (v2e v) σ.
 Proof.
   intros ?? Heq.
   edestruct (fill_value K) as [v' Hv'].
@@ -309,9 +307,9 @@ Section step_by_value.
      expression has a non-value e in the hole, then K is a left
      sub-context of K' - in other words, e also contains the reducible
      expression *)
-Lemma step_by_value {K K' e e'} :
+Lemma step_by_value {K K' e e' σ} :
   fill K e = fill K' e' ->
-  reducible e' ->
+  reducible e' σ ->
   e2v e = None ->
   exists K'', K' = comp_ctx K K''.
 Proof.
@@ -324,7 +322,7 @@ Proof.
                       by erewrite ?v2v).
   Ltac bad_red   Hfill e' Hred := exfalso; destruct e';
       try discriminate Hfill; [];
-      case: Hfill; intros; subst; destruct Hred as (σ' & e'' & σ'' & ef & Hstep);
+      case: Hfill; intros; subst; destruct Hred as (e'' & σ'' & ef & Hstep);
       inversion Hstep; done || (clear Hstep; subst;
       eapply fill_not_value2; last (
         try match goal with [ H : _ = fill _ _ |- _ ] => erewrite <-H end; simpl;
@@ -451,14 +449,14 @@ Section Language.
   |}.
   Next Obligation.
     intros e1 σ1 e2 σ2 ef (K & e1' & e2' & He1 & He2 & Hstep). subst e1 e2.
-    eapply fill_not_value. eapply reducible_not_value. do 4 eexists; eassumption.
+    eapply fill_not_value. eapply reducible_not_value. do 3 eexists; eassumption.
   Qed.
   Next Obligation.
     intros ? ? ? ? ? Hatomic (K & e1' & e2' & Heq1 & Heq2 & Hstep).
     subst. move: (Hatomic). rewrite (atomic_fill e1' K).
     - rewrite !fill_empty. eauto using atomic_step.
     - assumption.
-    - clear Hatomic. eapply reducible_not_value. do 4 eexists; eassumption.
+    - clear Hatomic. eapply reducible_not_value. do 3 eexists; eassumption.
   Qed.
 
   (** We can have bind with arbitrary evaluation contexts **)
@@ -470,8 +468,8 @@ Section Language.
       exists (comp_ctx K K'), e1', e2'. rewrite -!fill_comp Heq1 Heq2.
       split; last split; reflexivity || assumption.
     - intros ? ? ? ? ? Hnval (K'' & e1'' & e2'' & Heq1 & Heq2 & Hstep).
-      destruct (step_by_value Heq1) as [K' HeqK].
-      + do 4 eexists. eassumption.
+      destruct (step_by_value (σ:=σ1) Heq1) as [K' HeqK].
+      + do 3 eexists. eassumption.
       + assumption.
       + subst e2 K''. rewrite -fill_comp in Heq1. apply fill_inj_r in Heq1.
         subst e1'. exists (fill K' e2''). split; first by rewrite -fill_comp.
@@ -479,15 +477,15 @@ Section Language.
   Qed.
 
   Lemma prim_ectx_step e1 σ1 e2 σ2 ef :
-    reducible e1 →
+    reducible e1 σ1 →
     ectx_step e1 σ1 e2 σ2 ef →
     prim_step e1 σ1 e2 σ2 ef.
   Proof.
     intros Hred (K' & e1' & e2' & Heq1 & Heq2 & Hstep).
-    destruct (@step_by_value K' EmptyCtx e1' e1) as [K'' [HK' HK'']%comp_empty].
+    destruct (@step_by_value K' EmptyCtx e1' e1 σ1) as [K'' [HK' HK'']%comp_empty].
     - by rewrite fill_empty.
     - done.
-    - apply reducible_not_value. do 4 eexists; eassumption.
+    - eapply reducible_not_value. do 3 eexists; eassumption.
     - subst K' K'' e1 e2. by rewrite !fill_empty.
   Qed.
 

barrier/lifting.v

 Require Export barrier.parameter.
-Require Import prelude.gmap iris.lifting.
+Require Import prelude.gmap iris.lifting barrier.heap_lang.
 Import uPred.
 
 (* TODO RJ: Figure out a way to to always use our Σ. *)
@@ -11,7 +11,35 @@ Proof.
   by apply (wp_bind (Σ:=Σ) (K := fill K)), fill_is_ctx.
 Qed.
 
-(** Base axioms for core primitives of the language. *)
+(** 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.
+  (* RJ FIXME WTF the bound names of wp_lift_step *changed*?!?? *)
+  intros ? He Hsafe Hstep.
+  etransitivity; last eapply wp_lift_step with (σ2 := σ1)
+    (φ0 := λ e' σ' ef, ef = None ∧ φ e' σ'); last first.
+  - intros e2 σ2 ef Hstep'%prim_ectx_step; last done.
+    by apply Hstep.
+  - destruct Hsafe as (e' & σ' & ? & ?).
+    do 3 eexists. exists EmptyCtx. do 2 eexists.
+    split_ands; try (by rewrite fill_empty); eassumption.
+  - done.
+  - eassumption.
+  - apply pvs_mono. apply sep_mono; first done.
+    apply later_mono. 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; move=>[-> Hφ]. eapply const_intro_l; first eexact Hφ.
+    rewrite always_and_sep_l' associative -always_and_sep_l' wand_elim_r.
+    apply pvs_mono. rewrite right_id. done.
+Qed.
 
 (* TODO RJ: Figure out some better way to make the
    postcondition a predicate over a *location* *)
@@ -23,11 +51,9 @@ Lemma wp_alloc E σ v:
 Proof.
   (* RJ FIXME: rewrite would be nicer... *)
   etransitivity; last eapply wp_lift_step with (σ1 := σ)
-    (φ := λ e' σ' ef, ∃ l, e' = Loc l ∧ σ' = <[l:=v]>σ ∧ σ !! l = None ∧ ef = None);
+    (φ := λ e' σ', ∃ l, e' = Loc l ∧ σ' = <[l:=v]>σ ∧ σ !! l = None);
     last first.
-  - intros e2 σ2 ef Hstep%prim_ectx_step; last first.
-    { exists ∅. do 3 eexists. eapply AllocS with (l:=0); by rewrite ?v2v. }
-    inversion_clear Hstep.
+  - intros e2 σ2 ef Hstep. inversion_clear Hstep. split; first done.
     rewrite v2v in Hv. inversion_clear Hv.
     eexists; split_ands; done.
   - (* RJ FIXME: Need to find a fresh location. *) admit.
@@ -36,9 +62,9 @@ Proof.
   - (* RJ FIXME I am sure there is a better way to invoke right_id, but I could not find it. *)
     rewrite -pvs_intro. rewrite -{1}[ownP σ](@right_id _ _ _ _ uPred.sep_True).
     apply sep_mono; first done. rewrite -later_intro.
-    apply forall_intro=>e2. apply forall_intro=>σ2. apply forall_intro=>ef.
+    apply forall_intro=>e2. apply forall_intro=>σ2.
     apply wand_intro_l. rewrite right_id. rewrite -pvs_intro.
-    apply const_elim_l. intros [l [-> [-> [Hl ->]]]]. rewrite right_id.
+    apply const_elim_l. intros [l [-> [-> Hl]]].
     rewrite -wp_value'; last reflexivity.
     erewrite <-exist_intro with (a := l). apply and_intro.
     + by apply const_intro.
@@ -50,21 +76,17 @@ Lemma wp_load E σ l v:
   ownP (Σ:=Σ) σ ⊑ wp (Σ:=Σ) E (Load (Loc l)) (λ v', ■(v' = v) ∧ ownP (Σ:=Σ) σ).
 Proof.
   intros Hl. etransitivity; last eapply wp_lift_step with (σ1 := σ)
-    (φ := λ e' σ' ef, e' = v2e v ∧ σ' = σ ∧ ef = None); last first.
-  - intros e2 σ2 ef Hstep%prim_ectx_step; last first.
-    { exists σ. do 3 eexists. eapply LoadS; eassumption. }
-    move: Hl. inversion_clear Hstep=>{σ}. rewrite Hlookup.
-    case=>->. done.
-  - do 3 eexists. exists EmptyCtx. do 2 eexists.
-    split_ands; try (by rewrite fill_empty); [].
-    eapply LoadS; eassumption.
+    (φ := λ e' σ', e' = v2e v ∧ σ' = σ); last first.
+  - intros e2 σ2 ef Hstep. move: Hl. inversion_clear Hstep=>{σ}.
+    rewrite Hlookup. case=>->. done.
+  - do 3 eexists. eapply LoadS; eassumption.
   - reflexivity.
   - reflexivity.
   - rewrite -pvs_intro. rewrite -{1}[ownP σ](@right_id _ _ _ _ uPred.sep_True).
     apply sep_mono; first done. rewrite -later_intro.
-    apply forall_intro=>e2. apply forall_intro=>σ2. apply forall_intro=>ef.
+    apply forall_intro=>e2. apply forall_intro=>σ2.
     apply wand_intro_l. rewrite right_id. rewrite -pvs_intro.
-    apply const_elim_l. intros [-> [-> ->]]. rewrite right_id.
+    apply const_elim_l. intros [-> ->].
     rewrite -wp_value. apply and_intro.
     + by apply const_intro.
     + done.
@@ -72,25 +94,47 @@ Qed.
 
 Lemma wp_store E σ l v v':
   σ !! l = Some v' →
-  ownP (Σ:=Σ) σ ⊑ wp (Σ:=Σ) E (Store (Loc l) (v2e v)) (λ v', ■(v' = LitVUnit) ∧ ownP (Σ:=Σ) (<[l:=v]>σ)).
+  ownP (Σ:=Σ) σ ⊑ wp (Σ:=Σ) E (Store (Loc l) (v2e v))
+       (λ v', ■(v' = LitVUnit) ∧ ownP (Σ:=Σ) (<[l:=v]>σ)).
 Proof.
   intros Hl. etransitivity; last eapply wp_lift_step with (σ1 := σ)
-    (φ := λ e' σ' ef, e' = LitUnit ∧ σ' = <[l:=v]>σ ∧ ef = None); last first.
-  - intros e2 σ2 ef Hstep%prim_ectx_step; last first.
-    { exists σ. do 3 eexists. eapply StoreS; last (eexists; eassumption). by rewrite v2v. }
-    move: Hl. inversion_clear Hstep=>{σ2}. rewrite v2v in Hv. inversion_clear Hv.
-    done.
-  - do 3 eexists. exists EmptyCtx. do 2 eexists.
-    split_ands; try (by rewrite fill_empty); [].
-    eapply StoreS; last (eexists; eassumption). by rewrite v2v.
+    (φ := λ e' σ', e' = LitUnit ∧ σ' = <[l:=v]>σ); last first.
+  - intros e2 σ2 ef Hstep. move: Hl. inversion_clear Hstep=>{σ2}.
+    rewrite v2v in Hv. inversion_clear Hv. done.
+  - do 3 eexists. eapply StoreS; last (eexists; eassumption). by rewrite v2v.
   - reflexivity.
   - reflexivity.
   - rewrite -pvs_intro. rewrite -{1}[ownP σ](@right_id _ _ _ _ uPred.sep_True).
     apply sep_mono; first done. rewrite -later_intro.
-    apply forall_intro=>e2. apply forall_intro=>σ2. apply forall_intro=>ef.
+    apply forall_intro=>e2. apply forall_intro=>σ2.
     apply wand_intro_l. rewrite right_id. rewrite -pvs_intro.
-    apply const_elim_l. intros [-> [-> ->]]. rewrite right_id.
+    apply const_elim_l. intros [-> ->].
     rewrite -wp_value'; last reflexivity. apply and_intro.
     + by apply const_intro.
     + done.
 Qed.
+
+(** Base axioms for core primitives of the language: Stateless reductions *)
+
+Lemma wp_fork E e :
+  ▷ wp (Σ:=Σ) coPset_all e (λ _, True) ⊑ wp (Σ:=Σ) E (Fork e) (λ _, True).
+Proof.
+  etransitivity; last eapply wp_lift_pure_step with
+    (φ := λ e' ef, e' = LitUnit ∧ ef = Some e);
+    last first.
+  - intros σ1 e2 σ2 ef Hstep%prim_ectx_step; last first.
+    { do 3 eexists. eapply ForkS. }
+    inversion_clear Hstep. done.
+  - intros ?. do 3 eexists. exists EmptyCtx. do 2 eexists.
+    split_ands; try (by rewrite fill_empty); [].
+    eapply ForkS.
+  - reflexivity.
+  - apply later_mono.
+    apply forall_intro=>e2. apply forall_intro=>ef.
+    apply impl_intro_l. apply const_elim_l. intros [-> ->].
+    (* FIXME RJ This is ridicolous. *)
+    transitivity (True ★ wp coPset_all e (λ _ : ival Σ, True))%I;
+      first by rewrite left_id.
+    apply sep_mono; last reflexivity.
+    rewrite -wp_value'; reflexivity.
+Qed.

modures/logic.v

@@ -454,6 +454,18 @@ Proof.
   intros H; apply impl_intro_l. by rewrite -H and_elim_l.
 Qed.
 
+Lemma const_intro_l φ Q R :
+  φ → (■φ ∧ Q) ⊑ R → Q ⊑ R.
+Proof.
+  intros ? <-. apply and_intro; last done.
+  by apply const_intro.
+Qed.
+Lemma const_intro_r φ Q R : φ → (Q ∧ ■φ) ⊑ R → Q ⊑ R.
+Proof.
+  (* FIXME RJ: Why does this not work? rewrite (commutative uPred_and Q (■φ)%I). *)
+  intros ? <-. apply and_intro; first done.
+  by apply const_intro.
+Qed.
 Lemma const_elim_l φ Q R : (φ → Q ⊑ R) → (■ φ ∧ Q) ⊑ R.
 Proof. intros; apply const_elim with φ; eauto. Qed.
 Lemma const_elim_r φ Q R : (φ → Q ⊑ R) → (Q ∧ ■ φ) ⊑ R.