(almost) instantiate lifting lemma for allocation

.gitignore

@@ -5,5 +5,6 @@
 *.aux
 \#*\#
 *~
+*.bak
 .coq-native/
 Makefile

_CoqProject

 -Q . ""
-./prelude/option.v
-./prelude/fin_map_dom.v
-./prelude/bsets.v
-./prelude/fin_maps.v
-./prelude/vector.v
-./prelude/pmap.v
-./prelude/stringmap.v
-./prelude/fin_collections.v
-./prelude/mapset.v
-./prelude/proof_irrel.v
-./prelude/hashset.v
-./prelude/pretty.v
-./prelude/countable.v
-./prelude/orders.v
-./prelude/natmap.v
-./prelude/strings.v
-./prelude/relations.v
-./prelude/collections.v
-./prelude/listset.v
-./prelude/streams.v
-./prelude/gmap.v
-./prelude/base.v
-./prelude/tactics.v
-./prelude/prelude.v
-./prelude/listset_nodup.v
-./prelude/finite.v
-./prelude/numbers.v
-./prelude/nmap.v
-./prelude/zmap.v
-./prelude/co_pset.v
-./prelude/lexico.v
-./prelude/sets.v
-./prelude/decidable.v
-./prelude/list.v
-./prelude/error.v
-./modures/option.v
-./modures/cmra.v
-./modures/sts.v
-./modures/auth.v
-./modures/fin_maps.v
-./modures/logic.v
-./modures/cofe.v
-./modures/base.v
-./modures/dra.v
-./modures/cofe_solver.v
-./modures/agree.v
-./modures/ra.v
-./modures/excl.v
-./iris/model.v
-./iris/adequacy.v
-./iris/hoare_lifting.v
-./iris/lifting.v
-./iris/namespace.v
-./iris/viewshifts.v
-./iris/wsat.v
-./iris/ownership.v
-./iris/weakestpre.v
-./iris/language.v
-./iris/pviewshifts.v
-./iris/resources.v
-./iris/hoare.v
-./iris/parameter.v
-./barrier/heap_lang.v
+prelude/option.v
+prelude/fin_map_dom.v
+prelude/bsets.v
+prelude/fin_maps.v
+prelude/vector.v
+prelude/pmap.v
+prelude/stringmap.v
+prelude/fin_collections.v
+prelude/mapset.v
+prelude/proof_irrel.v
+prelude/hashset.v
+prelude/pretty.v
+prelude/countable.v
+prelude/orders.v
+prelude/natmap.v
+prelude/strings.v
+prelude/relations.v
+prelude/collections.v
+prelude/listset.v
+prelude/streams.v
+prelude/gmap.v
+prelude/base.v
+prelude/tactics.v
+prelude/prelude.v
+prelude/listset_nodup.v
+prelude/finite.v
+prelude/numbers.v
+prelude/nmap.v
+prelude/zmap.v
+prelude/co_pset.v
+prelude/lexico.v
+prelude/sets.v
+prelude/decidable.v
+prelude/list.v
+prelude/error.v
+modures/option.v
+modures/cmra.v
+modures/sts.v
+modures/auth.v
+modures/fin_maps.v
+modures/logic.v
+modures/cofe.v
+modures/base.v
+modures/dra.v
+modures/cofe_solver.v
+modures/agree.v
+modures/ra.v
+modures/excl.v
+iris/model.v
+iris/adequacy.v
+iris/hoare_lifting.v
+iris/lifting.v
+iris/namespace.v
+iris/viewshifts.v
+iris/wsat.v
+iris/ownership.v
+iris/weakestpre.v
+iris/language.v
+iris/pviewshifts.v
+iris/resources.v
+iris/hoare.v
+iris/parameter.v
+barrier/heap_lang.v
+barrier/parameter.v

barrier/heap_lang.v

 Require Import Autosubst.Autosubst.
-Require Import prelude.option prelude.gmap iris.parameter.
+Require Import prelude.option prelude.gmap iris.language.
 
 (** Some tactics useful when dealing with equality of sigma-like types: existT T0 t0 = existT T1 t1.
     They all assume such an equality is the first thing on the "stack" (goal). *)
@@ -55,6 +55,9 @@ Instance Subst_expr : Subst expr. derive. Defined.
 Instance SubstLemmas_expr : SubstLemmas expr. derive. Qed.
 
 Definition Lam (e: {bind expr}) := Rec (e.[up ids]).
+Definition Let' (e1: expr) (e2: {bind expr}) := App (Lam e2) e1.
+Definition Seq (e1 e2: expr) := Let' e1 (e2.[up ids]).
+
 Definition LitUnit := Lit tt.
 Definition LitTrue := Lit true.
 Definition LitFalse := Lit false.
@@ -233,6 +236,14 @@ Proof.
   intros Hnval Hval. erewrite fill_not_value in Hval by assumption. discriminate.
 Qed.
 
+Lemma comp_empty K K' :
+  EmptyCtx = comp_ctx K K' →
+  K = EmptyCtx ∧ K' = EmptyCtx.
+Proof.
+  destruct K; try discriminate.
+  destruct K'; try discriminate.
+  done.
+Qed.
 
 (** The stepping relation *)
 Inductive prim_step : expr -> state -> expr -> state -> option expr -> Prop :=
@@ -252,7 +263,7 @@ Inductive prim_step : expr -> state -> expr -> state -> option expr -> Prop :=
     prim_step (Case (InjR e0) e1 e2) σ (e2.[e0/]) σ None
 | ForkS e σ:
     prim_step (Fork e) σ LitUnit σ (Some e)
-| RefS e v σ l (Hv : e2v e = Some v) (Hfresh : σ !! l = None):
+| AllocS e v σ l (Hv : e2v e = Some v) (Hfresh : σ !! l = None):
     prim_step (Alloc e) σ (Loc l) (<[l:=v]>σ) None
 | LoadS l v σ (Hlookup : σ !! l = Some v):
     prim_step (Load (Loc l)) σ (v2e v) σ None
@@ -426,7 +437,7 @@ Section Language.
     exists K e1' e2', e1 = fill K e1' /\ e2 = fill K e2' /\
                       prim_step e1' σ1 e2' σ2 ef.
 
-  Program Instance heap_lang : Language expr value state := {|
+  Global Program Instance heap_lang : Language expr value state := {|
     of_val := v2e;
     to_val := e2v;
     language.atomic := atomic;
@@ -464,10 +475,17 @@ Section Language.
         do 3 eexists. split; last split; eassumption || reflexivity.
   Qed.
 
-End Language.
+  Lemma prim_ectx_step e1 σ1 e2 σ2 ef :
+    reducible e1 →
+    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].
+    - by rewrite fill_empty.
+    - done.
+    - apply reducible_not_value. do 4 eexists; eassumption.
+    - subst K' K'' e1 e2. by rewrite !fill_empty.
+  Qed.
 
-(* This is just to demonstrate that we can instantiate IParam. *)
-Module IParam.
-  Definition Σ := IParamConst heap_lang unitRA.
-  Print Assumptions Σ.
-End IParam.
+End Language.

barrier/lifting.v

+Require Export barrier.parameter.
+Require Import prelude.gmap iris.lifting.
+Import uPred.
+
+(** Base axioms for core primitives of the language. *)
+
+(* TODO RJ: Figure out some better way to make the
+   postcondition a predicate over a *location* *)
+(* TODO RJ: Figure out a way to to always use our Σ. *)
+Lemma wp_alloc E σ v:
+  ownP (Σ:=Σ) σ ⊑ wp (Σ:=Σ) E (Alloc (v2e v))
+       (λ v', ∃ l, ■(v' = LocV l ∧ σ !! l = None) ∧ ownP (Σ:=Σ) (<[l:=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);
+    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.
+    rewrite v2v in Hv. inversion_clear Hv.
+    eexists; split_ands; done.
+  - (* RJ FIXME: Need to find a fresh location. *) admit.
+  - reflexivity.
+  - reflexivity.
+  - (* 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 wand_intro_l. rewrite right_id. rewrite -pvs_intro.
+    apply const_elim_l. intros [l [-> [-> [Hl ->]]]]. rewrite right_id.
+    rewrite -wp_value'; last reflexivity.
+    erewrite <-exist_intro with (a := l). apply and_intro.
+    + by apply const_intro.
+    + done.
+Abort.

barrier/parameter.v

+Require Export barrier.heap_lang.
+Require Import iris.parameter.
+
+Definition Σ := IParamConst heap_lang unitRA.
+Print Assumptions Σ.

iris/weakestpre.v

@@ -177,10 +177,18 @@ Proof.
 Qed.
 
 (* Derived rules *)
+Opaque uPred_holds.
 Import uPred.
 Global Instance wp_mono' E e :
   Proper (pointwise_relation _ (⊑) ==> (⊑)) (wp E e).
 Proof. by intros Q Q' ?; apply wp_mono. Qed.
+Lemma wp_value' E Q e v : 
+  to_val e = Some v →
+  Q v ⊑ wp E e Q.
+Proof.
+  intros Hv. apply of_to_val in Hv.
+  rewrite -Hv. by apply wp_value.
+Qed.
 Lemma wp_frame_l E e Q R : (R ★ wp E e Q) ⊑ wp E e (λ v, R ★ Q v).
 Proof. setoid_rewrite (commutative _ R); apply wp_frame_r. Qed.
 Lemma wp_frame_later_l E e Q R :