lifting.v 6.08 KB
Newer Older
1
From iris.program_logic Require Export ectx_weakestpre.
2
From iris.program_logic Require Import ownership. (* for ownP *)
3
From iris.heap_lang Require Export lang.
4
From iris.heap_lang Require Import tactics.
5
From iris.proofmode Require Import weakestpre.
6
Import uPred.
Robbert Krebbers's avatar
Robbert Krebbers committed
7
Local Hint Extern 0 (head_reducible _ _) => do_head_step 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 ef : option (expr []).
Ralf Jung's avatar
Ralf Jung committed
14

15
(** Bind. This bundles some arguments that wp_ectx_bind leaves as indices. *)
16
Lemma wp_bind {E e} K Φ :
17
  WP e @ E {{ v, WP fill K (of_val v) @ E {{ Φ }} }}  WP fill K e @ E {{ Φ }}.
18
Proof. exact: wp_ectx_bind. Qed.
Ralf Jung's avatar
Ralf Jung committed
19

20
Lemma wp_bindi {E e} Ki Φ :
21
  WP e @ E {{ v, WP fill_item Ki (of_val v) @ E {{ Φ }} }} 
22 23 24
     WP fill_item Ki e @ E {{ Φ }}.
Proof. exact: weakestpre.wp_bind. Qed.

25
(** Base axioms for core primitives of the language: Stateful reductions. *)
26
Lemma wp_alloc_pst E σ e v Φ :
27
  to_val e = Some v 
28
  ( ownP σ   ( l, σ !! l = None  ownP (<[l:=v]>σ) - Φ (LocV l)))
29
   WP Alloc e @ E {{ Φ }}.
30
Proof.
Ralf Jung's avatar
Ralf Jung committed
31
  (* TODO: This works around ssreflect bug #22. *)
32 33
  intros. set (φ (e' : expr []) σ' ef :=  l,
    ef = None  e' = Loc l  σ' = <[l:=v]>σ  σ !! l = None).
34
  rewrite -(wp_lift_atomic_head_step (Alloc e) φ σ) // /φ;
Robbert Krebbers's avatar
Robbert Krebbers committed
35
    last (by intros; inv_head_step; eauto 8); last (by simpl; eauto).
36 37 38
  iIntros  "[HP HΦ]". iFrame "HP". iNext.
  iIntros {v2 σ2 ef} "[% HP]".
  (* FIXME: I should not have to refer to "H0". *)
Robbert Krebbers's avatar
Robbert Krebbers committed
39 40
  destruct H0 as (l & -> & [= <-]%of_to_val_flip & -> & ?); simpl.
  iSplit; last done. iApply "HΦ"; by iSplit.
41
Qed.
42

43
Lemma wp_load_pst E σ l v Φ :
Ralf Jung's avatar
Ralf Jung committed
44
  σ !! l = Some v 
45
  ( ownP σ   (ownP σ - Φ v))  WP Load (Loc l) @ E {{ Φ }}.
Ralf Jung's avatar
Ralf Jung committed
46
Proof.
47
  intros. rewrite -(wp_lift_atomic_det_head_step σ v σ None) ?right_id //;
Robbert Krebbers's avatar
Robbert Krebbers committed
48
    last (by intros; inv_head_step; eauto using to_of_val); simpl; by eauto.
Ralf Jung's avatar
Ralf Jung committed
49
Qed.
50

51
Lemma wp_store_pst E σ l e v v' Φ :
52
  to_val e = Some v  σ !! l = Some v' 
53
  ( ownP σ   (ownP (<[l:=v]>σ) - Φ (LitV LitUnit)))
54
   WP Store (Loc l) e @ E {{ Φ }}.
Ralf Jung's avatar
Ralf Jung committed
55
Proof.
56
  intros. rewrite-(wp_lift_atomic_det_head_step σ (LitV LitUnit) (<[l:=v]>σ) None)
Robbert Krebbers's avatar
Robbert Krebbers committed
57
    ?right_id //; last (by intros; inv_head_step; eauto); simpl; by eauto.
Ralf Jung's avatar
Ralf Jung committed
58
Qed.
59

60
Lemma wp_cas_fail_pst E σ l e1 v1 e2 v2 v' Φ :
61
  to_val e1 = Some v1  to_val e2 = Some v2  σ !! l = Some v'  v'  v1 
62
  ( ownP σ   (ownP σ - Φ (LitV $ LitBool false)))
63
   WP CAS (Loc l) e1 e2 @ E {{ Φ }}.
Ralf Jung's avatar
Ralf Jung committed
64
Proof.
65
  intros. rewrite -(wp_lift_atomic_det_head_step σ (LitV $ LitBool false) σ None)
Robbert Krebbers's avatar
Robbert Krebbers committed
66
    ?right_id //; last (by intros; inv_head_step; eauto);
67
    simpl; by eauto 10.
Ralf Jung's avatar
Ralf Jung committed
68
Qed.
69

70
Lemma wp_cas_suc_pst E σ l e1 v1 e2 v2 Φ :
71
  to_val e1 = Some v1  to_val e2 = Some v2  σ !! l = Some v1 
72
  ( ownP σ   (ownP (<[l:=v2]>σ) - Φ (LitV $ LitBool true)))
73
   WP CAS (Loc l) e1 e2 @ E {{ Φ }}.
Ralf Jung's avatar
Ralf Jung committed
74
Proof.
75
  intros. rewrite -(wp_lift_atomic_det_head_step σ (LitV $ LitBool true)
Robbert Krebbers's avatar
Robbert Krebbers committed
76
    (<[l:=v2]>σ) None) ?right_id //; last (by intros; inv_head_step; eauto);
77
    simpl; by eauto 10.
Ralf Jung's avatar
Ralf Jung committed
78 79
Qed.

80
(** Base axioms for core primitives of the language: Stateless reductions *)
81
Lemma wp_fork E e Φ :
82
  ( Φ (LitV LitUnit)   WP e {{ _, True }})  WP Fork e @ E {{ Φ }}.
83
Proof.
84
  rewrite -(wp_lift_pure_det_head_step (Fork e) (Lit LitUnit) (Some e)) //=;
Robbert Krebbers's avatar
Robbert Krebbers committed
85
    last by intros; inv_head_step; eauto.
86
  rewrite later_sep -(wp_value _ _ (Lit _)) //.
87
Qed.
88

89
Lemma wp_rec E f x e1 e2 v Φ :
90
  to_val e2 = Some v 
91 92
   WP subst' x e2 (subst' f (Rec f x e1) e1) @ E {{ Φ }}
   WP App (Rec f x e1) e2 @ E {{ Φ }}.
93
Proof.
94
  intros. rewrite -(wp_lift_pure_det_head_step (App _ _)
95
    (subst' x e2 (subst' f (Rec f x e1) e1)) None) //= ?right_id;
Robbert Krebbers's avatar
Robbert Krebbers committed
96
    intros; inv_head_step; eauto.
97
Qed.
98

99 100
Lemma wp_rec' E f x erec e1 e2 v2 Φ :
  e1 = Rec f x erec 
101
  to_val e2 = Some v2 
102 103
   WP subst' x e2 (subst' f e1 erec) @ E {{ Φ }}
   WP App e1 e2 @ E {{ Φ }}.
104 105
Proof. intros ->. apply wp_rec. Qed.

106
Lemma wp_un_op E op l l' Φ :
107
  un_op_eval op l = Some l' 
108
   Φ (LitV l')  WP UnOp op (Lit l) @ E {{ Φ }}.
109
Proof.
110
  intros. rewrite -(wp_lift_pure_det_head_step (UnOp op _) (Lit l') None)
Robbert Krebbers's avatar
Robbert Krebbers committed
111
    ?right_id -?wp_value //; intros; inv_head_step; eauto.
Ralf Jung's avatar
Ralf Jung committed
112
Qed.
113

114
Lemma wp_bin_op E op l1 l2 l' Φ :
115
  bin_op_eval op l1 l2 = Some l' 
116
   Φ (LitV l')  WP BinOp op (Lit l1) (Lit l2) @ E {{ Φ }}.
Ralf Jung's avatar
Ralf Jung committed
117
Proof.
118
  intros Heval. rewrite -(wp_lift_pure_det_head_step (BinOp op _ _) (Lit l') None)
Robbert Krebbers's avatar
Robbert Krebbers committed
119
    ?right_id -?wp_value //; intros; inv_head_step; eauto.
Ralf Jung's avatar
Ralf Jung committed
120
Qed.
121

122
Lemma wp_if_true E e1 e2 Φ :
123
   WP e1 @ E {{ Φ }}  WP If (Lit (LitBool true)) e1 e2 @ E {{ Φ }}.
Ralf Jung's avatar
Ralf Jung committed
124
Proof.
125
  rewrite -(wp_lift_pure_det_head_step (If _ _ _) e1 None)
Robbert Krebbers's avatar
Robbert Krebbers committed
126
    ?right_id //; intros; inv_head_step; eauto.
127 128
Qed.

129
Lemma wp_if_false E e1 e2 Φ :
130
   WP e2 @ E {{ Φ }}  WP If (Lit (LitBool false)) e1 e2 @ E {{ Φ }}.
131
Proof.
132
  rewrite -(wp_lift_pure_det_head_step (If _ _ _) e2 None)
Robbert Krebbers's avatar
Robbert Krebbers committed
133
    ?right_id //; intros; inv_head_step; eauto.
134
Qed.
135

136
Lemma wp_fst E e1 v1 e2 v2 Φ :
137
  to_val e1 = Some v1  to_val e2 = Some v2 
138
   Φ v1  WP Fst (Pair e1 e2) @ E {{ Φ }}.
Ralf Jung's avatar
Ralf Jung committed
139
Proof.
140
  intros. rewrite -(wp_lift_pure_det_head_step (Fst _) e1 None)
Robbert Krebbers's avatar
Robbert Krebbers committed
141
    ?right_id -?wp_value //; intros; inv_head_step; eauto.
Ralf Jung's avatar
Ralf Jung committed
142
Qed.
143

144
Lemma wp_snd E e1 v1 e2 v2 Φ :
145
  to_val e1 = Some v1  to_val e2 = Some v2 
146
   Φ v2  WP Snd (Pair e1 e2) @ E {{ Φ }}.
Ralf Jung's avatar
Ralf Jung committed
147
Proof.
148
  intros. rewrite -(wp_lift_pure_det_head_step (Snd _) e2 None)
Robbert Krebbers's avatar
Robbert Krebbers committed
149
    ?right_id -?wp_value //; intros; inv_head_step; eauto.
Ralf Jung's avatar
Ralf Jung committed
150
Qed.
151

152
Lemma wp_case_inl E e0 v0 e1 e2 Φ :
153
  to_val e0 = Some v0 
154
   WP App e1 e0 @ E {{ Φ }}  WP Case (InjL e0) e1 e2 @ E {{ Φ }}.
Ralf Jung's avatar
Ralf Jung committed
155
Proof.
156
  intros. rewrite -(wp_lift_pure_det_head_step (Case _ _ _)
Robbert Krebbers's avatar
Robbert Krebbers committed
157
    (App e1 e0) None) ?right_id //; intros; inv_head_step; eauto.
Ralf Jung's avatar
Ralf Jung committed
158
Qed.
159

160
Lemma wp_case_inr E e0 v0 e1 e2 Φ :
161
  to_val e0 = Some v0 
162
   WP App e2 e0 @ E {{ Φ }}  WP Case (InjR e0) e1 e2 @ E {{ Φ }}.
Ralf Jung's avatar
Ralf Jung committed
163
Proof.
164
  intros. rewrite -(wp_lift_pure_det_head_step (Case _ _ _)
Robbert Krebbers's avatar
Robbert Krebbers committed
165
    (App e2 e0) None) ?right_id //; intros; inv_head_step; eauto.
Ralf Jung's avatar
Ralf Jung committed
166
Qed.
167
End lifting.