lifting.v 5.76 KB
Newer Older
1 2
From iris.program_logic Require Export weakestpre.
From iris.program_logic Require Import ownership ectx_lifting. (* 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.
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.
14
Implicit Types l : loc.
15

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

Ralf Jung's avatar
Ralf Jung committed
21 22 23 24 25
Lemma wp_bindi {E e} Ki Φ :
  WP e @ E {{ v, WP fill_item Ki (of_val v) @ E {{ Φ }} }} 
     WP fill_item Ki e @ E {{ Φ }}.
Proof. exact: weakestpre.wp_bind. Qed.

26
(** Base axioms for core primitives of the language: Stateful reductions. *)
27
Lemma wp_alloc_pst E σ v Φ :
28
   ownP σ   ( l, σ !! l = None  ownP (<[l:=v]>σ) ={E}= Φ (LitV (LitLoc l)))
29
   WP Alloc (of_val v) @ E {{ Φ }}.
30
Proof.
31 32
  iIntros "[HP HΦ]".
  iApply (wp_lift_atomic_head_step (Alloc (of_val v)) σ); eauto with fsaV.
33
  iFrame "HP". iNext. iIntros (v2 σ2 ef) "[% HP]". inv_head_step.
34 35
  match goal with H: _ = of_val v2 |- _ => apply (inj of_val (LitV _)) in H end.
  subst v2. iSplit; last done. iApply "HΦ"; by iSplit.
36
Qed.
37

38
Lemma wp_load_pst E σ l v Φ :
39
  σ !! l = Some v 
40
   ownP σ   (ownP σ ={E}= Φ v)  WP Load (Lit (LitLoc l)) @ E {{ Φ }}.
41
Proof.
42
  intros. rewrite -(wp_lift_atomic_det_head_step σ v σ None) ?right_id //;
43
    last (by intros; inv_head_step; eauto using to_of_val). solve_atomic.
44
Qed.
45

46 47
Lemma wp_store_pst E σ l v v' Φ :
  σ !! l = Some v' 
48
   ownP σ   (ownP (<[l:=v]>σ) ={E}= Φ (LitV LitUnit))
49
   WP Store (Lit (LitLoc l)) (of_val v) @ E {{ Φ }}.
50
Proof.
51 52 53
  intros ?.
  rewrite-(wp_lift_atomic_det_head_step σ (LitV LitUnit) (<[l:=v]>σ) None)
    ?right_id //; last (by intros; inv_head_step; eauto). solve_atomic.
54
Qed.
55

56 57
Lemma wp_cas_fail_pst E σ l v1 v2 v' Φ :
  σ !! l = Some v'  v'  v1 
58
   ownP σ   (ownP σ ={E}= Φ (LitV $ LitBool false))
59
   WP CAS (Lit (LitLoc l)) (of_val v1) (of_val v2) @ E {{ Φ }}.
Ralf Jung's avatar
Ralf Jung committed
60
Proof.
61 62 63
  intros ??.
  rewrite -(wp_lift_atomic_det_head_step σ (LitV $ LitBool false) σ None)
    ?right_id //; last (by intros; inv_head_step; eauto). solve_atomic.
Ralf Jung's avatar
Ralf Jung committed
64
Qed.
65

66 67
Lemma wp_cas_suc_pst E σ l v1 v2 Φ :
  σ !! l = Some v1 
68
   ownP σ   (ownP (<[l:=v2]>σ) ={E}= Φ (LitV $ LitBool true))
69
   WP CAS (Lit (LitLoc l)) (of_val v1) (of_val v2) @ E {{ Φ }}.
Ralf Jung's avatar
Ralf Jung committed
70
Proof.
71 72 73
  intros ?. rewrite -(wp_lift_atomic_det_head_step σ (LitV $ LitBool true)
    (<[l:=v2]>σ) None) ?right_id //; last (by intros; inv_head_step; eauto).
  solve_atomic.
Ralf Jung's avatar
Ralf Jung committed
74 75
Qed.

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

85
Lemma wp_rec E f x erec e1 e2 Φ :
86
  e1 = Rec f x erec 
87
  is_Some (to_val e2) 
88
  Closed (f :b: x :b: []) erec 
Robbert Krebbers's avatar
Robbert Krebbers committed
89
   WP subst' x e2 (subst' f e1 erec) @ E {{ Φ }}  WP App e1 e2 @ E {{ Φ }}.
90
Proof.
91
  intros -> [v2 ?] ?. rewrite -(wp_lift_pure_det_head_step (App _ _)
92 93 94
    (subst' x e2 (subst' f (Rec f x erec) erec)) None) //= ?right_id;
    intros; inv_head_step; eauto.
Qed.
95

96 97 98
Lemma wp_un_op E op li li' Φ :
  un_op_eval op li = Some li' 
   (|={E}=> Φ (LitV li'))  WP UnOp op (Lit li) @ E {{ Φ }}.
99
Proof.
100
  intros. rewrite -(wp_lift_pure_det_head_step (UnOp op _) (Lit li') None)
101
    ?right_id -?wp_value_pvs //; intros; inv_head_step; eauto.
Ralf Jung's avatar
Ralf Jung committed
102
Qed.
103

104 105 106
Lemma wp_bin_op E op li1 li2 li' Φ :
  bin_op_eval op li1 li2 = Some li' 
   (|={E}=> Φ (LitV li'))  WP BinOp op (Lit li1) (Lit li2) @ E {{ Φ }}.
Ralf Jung's avatar
Ralf Jung committed
107
Proof.
108
  intros Heval. rewrite -(wp_lift_pure_det_head_step (BinOp op _ _) (Lit li') None)
109
    ?right_id -?wp_value_pvs //; intros; inv_head_step; eauto.
Ralf Jung's avatar
Ralf Jung committed
110
Qed.
111

112
Lemma wp_if_true E e1 e2 Φ :
113
   WP e1 @ E {{ Φ }}  WP If (Lit (LitBool true)) e1 e2 @ E {{ Φ }}.
Ralf Jung's avatar
Ralf Jung committed
114
Proof.
115
  rewrite -(wp_lift_pure_det_head_step (If _ _ _) e1 None)
116
    ?right_id //; intros; inv_head_step; eauto.
117 118
Qed.

119
Lemma wp_if_false E e1 e2 Φ :
120
   WP e2 @ E {{ Φ }}  WP If (Lit (LitBool false)) e1 e2 @ E {{ Φ }}.
121
Proof.
122
  rewrite -(wp_lift_pure_det_head_step (If _ _ _) e2 None)
123
    ?right_id //; intros; inv_head_step; eauto.
124
Qed.
125

126 127
Lemma wp_fst E e1 v1 e2 Φ :
  to_val e1 = Some v1  is_Some (to_val e2) 
128
   (|={E}=> Φ v1)  WP Fst (Pair e1 e2) @ E {{ Φ }}.
129
Proof.
130
  intros ? [v2 ?]. rewrite -(wp_lift_pure_det_head_step (Fst _) e1 None)
131
    ?right_id -?wp_value_pvs //; intros; inv_head_step; eauto.
132
Qed.
133

134 135
Lemma wp_snd E e1 e2 v2 Φ :
  is_Some (to_val e1)  to_val e2 = Some v2 
136
   (|={E}=> Φ v2)  WP Snd (Pair e1 e2) @ E {{ Φ }}.
137
Proof.
138
  intros [v1 ?] ?. rewrite -(wp_lift_pure_det_head_step (Snd _) e2 None)
139
    ?right_id -?wp_value_pvs //; intros; inv_head_step; eauto.
140
Qed.
141

142 143
Lemma wp_case_inl E e0 e1 e2 Φ :
  is_Some (to_val e0) 
144
   WP App e1 e0 @ E {{ Φ }}  WP Case (InjL e0) e1 e2 @ E {{ Φ }}.
145
Proof.
146
  intros [v0 ?]. rewrite -(wp_lift_pure_det_head_step (Case _ _ _)
147
    (App e1 e0) None) ?right_id //; intros; inv_head_step; eauto.
148
Qed.
149

150 151
Lemma wp_case_inr E e0 e1 e2 Φ :
  is_Some (to_val e0) 
152
   WP App e2 e0 @ E {{ Φ }}  WP Case (InjR e0) e1 e2 @ E {{ Φ }}.
153
Proof.
154
  intros [v0 ?]. rewrite -(wp_lift_pure_det_head_step (Case _ _ _)
155
    (App e2 e0) None) ?right_id //; intros; inv_head_step; eauto.
156
Qed.
157
End lifting.