prove bind, load and store lemmas

_CoqProject

@@ -63,3 +63,4 @@ iris/hoare.v
 iris/parameter.v
 barrier/heap_lang.v
 barrier/parameter.v
+barrier/lifting.v

barrier/heap_lang.v

@@ -58,19 +58,22 @@ 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.
-
 Inductive value :=
 | RecV (e : {bind 2 of expr})
-| LitV (T : Type) (t : T)  (* arbitrary Coq values become literal values *)
+| LitV {T : Type} (t : T)  (* arbitrary Coq values become literal values *)
 | PairV (v1 v2 : value)
 | InjLV (v : value)
 | InjRV (v : value)
 | LocV (l : loc)
 .
 
+Definition LitUnit := Lit tt.
+Definition LitVUnit := LitV tt.
+Definition LitTrue := Lit true.
+Definition LitVTrue := LitV true.
+Definition LitFalse := Lit false.
+Definition LitVFalse := LitV false.
+
 Fixpoint v2e (v : value) : expr :=
   match v with
   | LitV _ t => Lit t
@@ -84,7 +87,7 @@ Fixpoint v2e (v : value) : expr :=
 Fixpoint e2v (e : expr) : option value :=
   match e with
   | Rec e => Some (RecV e)
-  | Lit T t => Some (LitV T t)
+  | Lit _ t => Some (LitV t)
   | Pair e1 e2 => v1 ← e2v e1;
                   v2 ← e2v e2;
                   Some (PairV v1 v2)

barrier/lifting.v

@@ -2,11 +2,21 @@ Require Export barrier.parameter.
 Require Import prelude.gmap iris.lifting.
 Import uPred.
 
+(* TODO RJ: Figure out a way to to always use our Σ. *)
+
+(** Bind. *)
+Lemma wp_bind E e K Q :
+  wp E e (λ v, wp (Σ:=Σ) E (fill K (of_val v)) Q) ⊑ wp (Σ:=Σ) E (fill K e) Q.
+Proof.
+  by apply (wp_bind (Σ:=Σ) (K := fill K)), fill_is_ctx.
+Qed.
+
 (** 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 Σ. *)
+(* TODO RJ: There is probably a specialized version of the lifting
+   lemma that would be useful here. *)
 Lemma wp_alloc E σ v:
   ownP (Σ:=Σ) σ ⊑ wp (Σ:=Σ) E (Alloc (v2e v))
        (λ v', ∃ l, ■(v' = LocV l ∧ σ !! l = None) ∧ ownP (Σ:=Σ) (<[l:=v]>σ)).
@@ -34,3 +44,53 @@ Proof.
     + by apply const_intro.
     + done.
 Abort.
+
+Lemma wp_load E σ l v:
+  σ !! l = Some 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.
+  - 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 wand_intro_l. rewrite right_id. rewrite -pvs_intro.
+    apply const_elim_l. intros [-> [-> ->]]. rewrite right_id.
+    rewrite -wp_value. apply and_intro.
+    + by apply const_intro.
+    + done.
+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]>σ)).
+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.
+  - 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 wand_intro_l. rewrite right_id. rewrite -pvs_intro.
+    apply const_elim_l. intros [-> [-> ->]]. rewrite right_id.
+    rewrite -wp_value'; last reflexivity. apply and_intro.
+    + by apply const_intro.
+    + done.
+Qed.