lifting.v 5.69 KB
Newer Older
1
2
3
4
5
From iris.program_logic Require Export weakestpre.
From iris.heap_lang Require Export lang.
From iris.program_logic Require Import lifting.
From iris.program_logic Require Import ownership. (* for ownP *)
From iris.heap_lang Require Import tactics.
6
Import uPred.
7
Local Hint Extern 0 (language.reducible _ _) => do_step ltac:(eauto 2).
8

9
Section lifting.
10
Context {Σ : iFunctor}.
11
12
Implicit Types P Q : iProp heap_lang Σ.
Implicit Types Φ : val  iProp heap_lang Σ.
13
Implicit Types K : ectx.
14
Implicit Types ef : option (expr []).
Ralf Jung's avatar
Ralf Jung committed
15
16

(** Bind. *)
17
Lemma wp_bind {E e} K Φ :
18
  #> e @ E {{ λ v, #> fill K (of_val v) @ E {{ Φ }}}}  #> fill K e @ E {{ Φ }}.
19
Proof. apply weakestpre.wp_bind. Qed.
Ralf Jung's avatar
Ralf Jung committed
20

21
(** Base axioms for core primitives of the language: Stateful reductions. *)
22
Lemma wp_alloc_pst E σ e v Φ :
23
  to_val e = Some v 
24
  ( ownP σ   ( l, σ !! l = None  ownP (<[l:=v]>σ) - Φ (LocV l)))
25
   #> Alloc e @ E {{ Φ }}.
26
Proof.
27
  (* TODO RJ: This works around ssreflect bug #22. *)
28
29
  intros. set (φ v' σ' ef :=  l,
    ef = None  v' = LocV l  σ' = <[l:=v]>σ  σ !! l = None).
30
  rewrite -(wp_lift_atomic_step (Alloc e) φ σ) // /φ;
Ralf Jung's avatar
Ralf Jung committed
31
    last by intros; inv_step; eauto 8.
32
  apply sep_mono, later_mono; first done.
33
34
  apply forall_intro=>e2; apply forall_intro=>σ2; apply forall_intro=>ef.
  apply wand_intro_l.
35
  rewrite always_and_sep_l -assoc -always_and_sep_l.
36
37
  apply const_elim_l=>-[l [-> [-> [-> ?]]]].
  by rewrite (forall_elim l) right_id const_equiv // left_id wand_elim_r.
38
Qed.
39

40
Lemma wp_load_pst E σ l v Φ :
Ralf Jung's avatar
Ralf Jung committed
41
  σ !! l = Some v 
42
  ( ownP σ   (ownP σ - Φ v))  #> Load (Loc l) @ E {{ Φ }}.
Ralf Jung's avatar
Ralf Jung committed
43
Proof.
44
45
  intros. rewrite -(wp_lift_atomic_det_step σ v σ None) ?right_id //;
    last by intros; inv_step; eauto using to_of_val.
Ralf Jung's avatar
Ralf Jung committed
46
Qed.
47

48
Lemma wp_store_pst E σ l e v v' Φ :
49
  to_val e = Some v  σ !! l = Some v' 
50
  ( ownP σ   (ownP (<[l:=v]>σ) - Φ (LitV LitUnit)))
51
   #> Store (Loc l) e @ E {{ Φ }}.
Ralf Jung's avatar
Ralf Jung committed
52
Proof.
53
  intros. rewrite -(wp_lift_atomic_det_step σ (LitV LitUnit) (<[l:=v]>σ) None)
54
    ?right_id //; last by intros; inv_step; eauto.
Ralf Jung's avatar
Ralf Jung committed
55
Qed.
56

57
Lemma wp_cas_fail_pst E σ l e1 v1 e2 v2 v' Φ :
58
  to_val e1 = Some v1  to_val e2 = Some v2  σ !! l = Some v'  v'  v1 
59
  ( ownP σ   (ownP σ - Φ (LitV $ LitBool false)))
60
   #> CAS (Loc l) e1 e2 @ E {{ Φ }}.
Ralf Jung's avatar
Ralf Jung committed
61
Proof.
Ralf Jung's avatar
Ralf Jung committed
62
  intros. rewrite -(wp_lift_atomic_det_step σ (LitV $ LitBool false) σ None)
63
    ?right_id //; last by intros; inv_step; eauto.
Ralf Jung's avatar
Ralf Jung committed
64
Qed.
65

66
Lemma wp_cas_suc_pst E σ l e1 v1 e2 v2 Φ :
67
  to_val e1 = Some v1  to_val e2 = Some v2  σ !! l = Some v1 
68
  ( ownP σ   (ownP (<[l:=v2]>σ) - Φ (LitV $ LitBool true)))
69
   #> CAS (Loc l) e1 e2 @ E {{ Φ }}.
Ralf Jung's avatar
Ralf Jung committed
70
Proof.
71
72
  intros. rewrite -(wp_lift_atomic_det_step σ (LitV $ LitBool true)
    (<[l:=v2]>σ) None) ?right_id //; last by intros; inv_step; eauto.
Ralf Jung's avatar
Ralf Jung committed
73
74
Qed.

75
(** Base axioms for core primitives of the language: Stateless reductions *)
76
Lemma wp_fork E e Φ :
77
  ( Φ (LitV LitUnit)   #> e {{ λ _, True }})  #> Fork e @ E {{ Φ }}.
78
Proof.
79
  rewrite -(wp_lift_pure_det_step (Fork e) (Lit LitUnit) (Some e)) //=;
80
    last by intros; inv_step; eauto.
81
  rewrite later_sep -(wp_value _ _ (Lit _)) //.
82
Qed.
83

84
Lemma wp_rec E f x e1 e2 v Φ :
85
  to_val e2 = Some v 
Ralf Jung's avatar
Ralf Jung committed
86
   #> subst' x e2 (subst' f (Rec f x e1) e1) @ E {{ Φ }}
87
   #> App (Rec f x e1) e2 @ E {{ Φ }}.
88
Proof.
89
  intros. rewrite -(wp_lift_pure_det_step (App _ _)
90
    (subst' x e2 (subst' f (Rec f x e1) e1)) None) //= ?right_id;
91
    intros; inv_step; eauto.
92
Qed.
93

94
95
Lemma wp_rec' E f x erec e1 e2 v2 Φ :
  e1 = Rec f x erec 
96
  to_val e2 = Some v2 
Ralf Jung's avatar
Ralf Jung committed
97
   #> subst' x e2 (subst' f e1 erec) @ E {{ Φ }}
98
   #> App e1 e2 @ E {{ Φ }}.
99
100
Proof. intros ->. apply wp_rec. Qed.

101
Lemma wp_un_op E op l l' Φ :
102
  un_op_eval op l = Some l' 
103
   Φ (LitV l')  #> UnOp op (Lit l) @ E {{ Φ }}.
104
Proof.
105
  intros. rewrite -(wp_lift_pure_det_step (UnOp op _) (Lit l') None)
106
    ?right_id -?wp_value //; intros; inv_step; eauto.
Ralf Jung's avatar
Ralf Jung committed
107
Qed.
108

109
Lemma wp_bin_op E op l1 l2 l' Φ :
110
  bin_op_eval op l1 l2 = Some l' 
111
   Φ (LitV l')  #> BinOp op (Lit l1) (Lit l2) @ E {{ Φ }}.
Ralf Jung's avatar
Ralf Jung committed
112
Proof.
113
  intros Heval. rewrite -(wp_lift_pure_det_step (BinOp op _ _) (Lit l') None)
114
    ?right_id -?wp_value //; intros; inv_step; eauto.
Ralf Jung's avatar
Ralf Jung committed
115
Qed.
116

117
Lemma wp_if_true E e1 e2 Φ :
118
   #> e1 @ E {{ Φ }}  #> If (Lit (LitBool true)) e1 e2 @ E {{ Φ }}.
Ralf Jung's avatar
Ralf Jung committed
119
Proof.
120
  rewrite -(wp_lift_pure_det_step (If _ _ _) e1 None)
121
    ?right_id //; intros; inv_step; eauto.
122
123
Qed.

124
Lemma wp_if_false E e1 e2 Φ :
125
   #> e2 @ E {{ Φ }}  #> If (Lit (LitBool false)) e1 e2 @ E {{ Φ }}.
126
127
Proof.
  rewrite -(wp_lift_pure_det_step (If _ _ _) e2 None)
128
    ?right_id //; intros; inv_step; eauto.
129
Qed.
130

131
Lemma wp_fst E e1 v1 e2 v2 Φ :
132
  to_val e1 = Some v1  to_val e2 = Some v2 
133
   Φ v1  #> Fst (Pair e1 e2) @ E {{ Φ }}.
Ralf Jung's avatar
Ralf Jung committed
134
Proof.
135
  intros. rewrite -(wp_lift_pure_det_step (Fst _) e1 None)
136
    ?right_id -?wp_value //; intros; inv_step; eauto.
Ralf Jung's avatar
Ralf Jung committed
137
Qed.
138

139
Lemma wp_snd E e1 v1 e2 v2 Φ :
140
  to_val e1 = Some v1  to_val e2 = Some v2 
141
   Φ v2  #> Snd (Pair e1 e2) @ E {{ Φ }}.
Ralf Jung's avatar
Ralf Jung committed
142
Proof.
143
  intros. rewrite -(wp_lift_pure_det_step (Snd _) e2 None)
144
    ?right_id -?wp_value //; intros; inv_step; eauto.
Ralf Jung's avatar
Ralf Jung committed
145
Qed.
146

147
Lemma wp_case_inl E e0 v0 e1 e2 Φ :
148
  to_val e0 = Some v0 
149
   #> App e1 e0 @ E {{ Φ }}  #> Case (InjL e0) e1 e2 @ E {{ Φ }}.
Ralf Jung's avatar
Ralf Jung committed
150
Proof.
151
152
  intros. rewrite -(wp_lift_pure_det_step (Case _ _ _)
    (App e1 e0) None) ?right_id //; intros; inv_step; eauto.
Ralf Jung's avatar
Ralf Jung committed
153
Qed.
154

155
Lemma wp_case_inr E e0 v0 e1 e2 Φ :
156
  to_val e0 = Some v0 
157
   #> App e2 e0 @ E {{ Φ }}  #> Case (InjR e0) e1 e2 @ E {{ Φ }}.
Ralf Jung's avatar
Ralf Jung committed
158
Proof.
159
160
  intros. rewrite -(wp_lift_pure_det_step (Case _ _ _)
    (App e2 e0) None) ?right_id //; intros; inv_step; eauto.
Ralf Jung's avatar
Ralf Jung committed
161
Qed.
162

163
End lifting.