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.