lifting.v 4.11 KB
Newer Older
1 2 3 4
Require Export barrier.parameter.
Require Import prelude.gmap iris.lifting.
Import uPred.

Ralf Jung's avatar
Ralf Jung committed
5 6 7 8 9 10 11 12 13
(* 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.

14 15 16 17
(** Base axioms for core primitives of the language. *)

(* TODO RJ: Figure out some better way to make the
   postcondition a predicate over a *location* *)
Ralf Jung's avatar
Ralf Jung committed
18 19
(* TODO RJ: There is probably a specialized version of the lifting
   lemma that would be useful here. *)
20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46
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.
Ralf Jung's avatar
Ralf Jung committed
47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96

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.