lifting.v 5.81 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.
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
(** Base axioms for core primitives of the language: Stateful reductions. *)
21
Lemma wp_alloc_pst E σ e v Φ :
22
  to_val e = Some v 
23
   ownP σ   ( l, σ !! l = None  ownP (<[l:=v]>σ) ={E}= Φ (LitV (LitLoc l)))
24
   WP Alloc e @ E {{ Φ }}.
25
Proof.
Ralf Jung's avatar
Ralf Jung committed
26
  iIntros {?}  "[HP HΦ]".
Ralf Jung's avatar
Ralf Jung committed
27
  (* TODO: This works around ssreflect bug #22. *)
Ralf Jung's avatar
Ralf Jung committed
28
  set (φ (e' : expr []) σ' ef :=  l,
29
    ef = None  e' = Lit (LitLoc l)  σ' = <[l:=v]>σ  σ !! l = None).
Ralf Jung's avatar
Ralf Jung committed
30
31
  iApply (wp_lift_atomic_head_step (Alloc e) φ σ); try (by simpl; eauto);
    [by intros; subst φ; inv_head_step; eauto 8|].
32
33
  iFrame "HP". iNext. iIntros {v2 σ2 ef} "[Hφ HP]".
  iDestruct "Hφ" as %(l & -> & [= <-]%of_to_val_flip & -> & ?); simpl.
Robbert Krebbers's avatar
Robbert Krebbers committed
34
  iSplit; last done. iApply "HΦ"; by iSplit.
35
Qed.
36

37
Lemma wp_load_pst E σ l v Φ :
Ralf Jung's avatar
Ralf Jung committed
38
  σ !! l = Some v 
39
   ownP σ   (ownP σ ={E}= Φ v)  WP Load (Lit (LitLoc l)) @ E {{ Φ }}.
Ralf Jung's avatar
Ralf Jung committed
40
Proof.
41
  intros. rewrite -(wp_lift_atomic_det_head_step σ v σ None) ?right_id //;
Robbert Krebbers's avatar
Robbert Krebbers committed
42
    last (by intros; inv_head_step; eauto using to_of_val); simpl; by eauto.
Ralf Jung's avatar
Ralf Jung committed
43
Qed.
44

45
Lemma wp_store_pst E σ l e v v' Φ :
46
  to_val e = Some v  σ !! l = Some v' 
47
   ownP σ   (ownP (<[l:=v]>σ) ={E}= Φ (LitV LitUnit))
48
   WP Store (Lit (LitLoc l)) e @ E {{ Φ }}.
Ralf Jung's avatar
Ralf Jung committed
49
Proof.
50
  intros. rewrite-(wp_lift_atomic_det_head_step σ (LitV LitUnit) (<[l:=v]>σ) None)
Robbert Krebbers's avatar
Robbert Krebbers committed
51
    ?right_id //; last (by intros; inv_head_step; eauto); simpl; by eauto.
Ralf Jung's avatar
Ralf Jung committed
52
Qed.
53

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

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

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

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

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

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

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

116
Lemma wp_if_false E e1 e2 Φ :
117
   WP e2 @ E {{ Φ }}  WP If (Lit (LitBool false)) e1 e2 @ E {{ Φ }}.
118
Proof.
119
  rewrite -(wp_lift_pure_det_head_step (If _ _ _) e2 None)
Robbert Krebbers's avatar
Robbert Krebbers committed
120
    ?right_id //; intros; inv_head_step; eauto.
121
Qed.
122

123
Lemma wp_fst E e1 v1 e2 v2 Φ :
124
  to_val e1 = Some v1  to_val e2 = Some v2 
125
   (|={E}=> Φ v1)  WP Fst (Pair e1 e2) @ E {{ Φ }}.
Ralf Jung's avatar
Ralf Jung committed
126
Proof.
127
  intros. rewrite -(wp_lift_pure_det_head_step (Fst _) e1 None)
128
    ?right_id -?wp_value_pvs //; intros; inv_head_step; eauto.
Ralf Jung's avatar
Ralf Jung committed
129
Qed.
130

131
Lemma wp_snd E e1 v1 e2 v2 Φ :
132
  to_val e1 = Some v1  to_val e2 = Some v2 
133
   (|={E}=> Φ v2)  WP Snd (Pair e1 e2) @ E {{ Φ }}.
Ralf Jung's avatar
Ralf Jung committed
134
Proof.
135
  intros. rewrite -(wp_lift_pure_det_head_step (Snd _) e2 None)
136
    ?right_id -?wp_value_pvs //; intros; inv_head_step; eauto.
Ralf Jung's avatar
Ralf Jung committed
137
Qed.
138

139
Lemma wp_case_inl E e0 v0 e1 e2 Φ :
140
  to_val e0 = Some v0 
141
   WP App e1 e0 @ E {{ Φ }}  WP Case (InjL e0) e1 e2 @ E {{ Φ }}.
Ralf Jung's avatar
Ralf Jung committed
142
Proof.
143
  intros. rewrite -(wp_lift_pure_det_head_step (Case _ _ _)
Robbert Krebbers's avatar
Robbert Krebbers committed
144
    (App e1 e0) None) ?right_id //; intros; inv_head_step; eauto.
Ralf Jung's avatar
Ralf Jung committed
145
Qed.
146

147
Lemma wp_case_inr E e0 v0 e1 e2 Φ :
148
  to_val e0 = Some v0 
149
   WP App e2 e0 @ E {{ Φ }}  WP Case (InjR e0) e1 e2 @ E {{ Φ }}.
Ralf Jung's avatar
Ralf Jung committed
150
Proof.
151
  intros. rewrite -(wp_lift_pure_det_head_step (Case _ _ _)
Robbert Krebbers's avatar
Robbert Krebbers committed
152
    (App e2 e0) None) ?right_id //; intros; inv_head_step; eauto.
Ralf Jung's avatar
Ralf Jung committed
153
Qed.
154
End lifting.