proofmode.v 25.3 KB
Newer Older
1
From iris.program_logic Require Export weakestpre total_weakestpre.
2
From iris.program_logic Require Import atomic.
3
From iris.proofmode Require Import coq_tactics reduction.
4
From iris.proofmode Require Export tactics.
5
From iris.heap_lang Require Export tactics lifting.
6
From iris.heap_lang Require Import notation.
7
Set Default Proof Using "Type".
Robbert Krebbers's avatar
Robbert Krebbers committed
8 9
Import uPred.

10
Lemma tac_wp_expr_eval `{!heapG Σ} Δ s E Φ e e' :
11
  ( (e'':=e'), e = e'') 
12
  envs_entails Δ (WP e' @ s; E {{ Φ }})  envs_entails Δ (WP e @ s; E {{ Φ }}).
13
Proof. by intros ->. Qed.
14
Lemma tac_twp_expr_eval `{!heapG Σ} Δ s E Φ e e' :
15
  ( (e'':=e'), e = e'') 
16 17
  envs_entails Δ (WP e' @ s; E [{ Φ }])  envs_entails Δ (WP e @ s; E [{ Φ }]).
Proof. by intros ->. Qed.
18

19
Tactic Notation "wp_expr_eval" tactic(t) :=
20
  iStartProof;
21 22 23 24 25 26 27 28 29
  lazymatch goal with
  | |- envs_entails _ (wp ?s ?E ?e ?Q) =>
    eapply tac_wp_expr_eval;
      [let x := fresh in intros x; t; unfold x; reflexivity|]
  | |- envs_entails _ (twp ?s ?E ?e ?Q) =>
    eapply tac_twp_expr_eval;
      [let x := fresh in intros x; t; unfold x; reflexivity|]
  | _ => fail "wp_expr_eval: not a 'wp'"
  end.
30

31
Lemma tac_wp_pure `{!heapG Σ} Δ Δ' s E e1 e2 φ n Φ :
32
  PureExec φ n e1 e2 
33
  φ 
34
  MaybeIntoLaterNEnvs n Δ Δ' 
35 36
  envs_entails Δ' (WP e2 @ s; E {{ Φ }}) 
  envs_entails Δ (WP e1 @ s; E {{ Φ }}).
37
Proof.
38
  rewrite envs_entails_eq=> ??? HΔ'. rewrite into_laterN_env_sound /=.
39 40
  rewrite HΔ' -lifting.wp_pure_step_later //.
Qed.
41
Lemma tac_twp_pure `{!heapG Σ} Δ s E e1 e2 φ n Φ :
42
  PureExec φ n e1 e2 
43 44 45 46
  φ 
  envs_entails Δ (WP e2 @ s; E [{ Φ }]) 
  envs_entails Δ (WP e1 @ s; E [{ Φ }]).
Proof.
47
  rewrite envs_entails_eq=> ?? ->. rewrite -total_lifting.twp_pure_step //.
48
Qed.
49

50
Lemma tac_wp_value `{!heapG Σ} Δ s E Φ v :
51 52
  envs_entails Δ (Φ v)  envs_entails Δ (WP (Val v) @ s; E {{ Φ }}).
Proof. rewrite envs_entails_eq=> ->. by apply wp_value. Qed.
53
Lemma tac_twp_value `{!heapG Σ} Δ s E Φ v :
54 55
  envs_entails Δ (Φ v)  envs_entails Δ (WP (Val v) @ s; E [{ Φ }]).
Proof. rewrite envs_entails_eq=> ->. by apply twp_value. Qed.
56

57 58
Ltac wp_expr_simpl := wp_expr_eval simpl.

Robbert Krebbers's avatar
Robbert Krebbers committed
59
Ltac wp_value_head :=
60 61 62 63 64 65 66
  first [eapply tac_wp_value || eapply tac_twp_value].

Ltac wp_finish :=
  wp_expr_simpl;      (* simplify occurences of subst/fill *)
  try wp_value_head;  (* in case we have reached a value, get rid of the WP *)
  pm_prettify.        (* prettify ▷s caused by [MaybeIntoLaterNEnvs] and
                         λs caused by wp_value *)
Robbert Krebbers's avatar
Robbert Krebbers committed
67

68 69 70 71 72 73 74
(** The argument [efoc] can be used to specify the construct that should be
reduced. For example, you can write [wp_pure (EIf _ _ _)], which will search
for an [EIf _ _ _] in the expression, and reduce it.

The use of [open_constr] in this tactic is essential. It will convert all holes
(i.e. [_]s) into evars, that later get unified when an occurences is found
(see [unify e' efoc] in the code below). *)
75
Tactic Notation "wp_pure" open_constr(efoc) :=
76 77
  iStartProof;
  lazymatch goal with
78
  | |- envs_entails _ (wp ?s ?E ?e ?Q) =>
Robbert Krebbers's avatar
Robbert Krebbers committed
79 80 81
    let e := eval simpl in e in
    reshape_expr e ltac:(fun K e' =>
      unify e' efoc;
82
      eapply (tac_wp_pure _ _ _ _ (fill K e'));
Ralf Jung's avatar
Ralf Jung committed
83
      [iSolveTC                       (* PureExec *)
Robbert Krebbers's avatar
Robbert Krebbers committed
84
      |try fast_done                  (* The pure condition for PureExec *)
Ralf Jung's avatar
Ralf Jung committed
85
      |iSolveTC                       (* IntoLaters *)
86
      |wp_finish                      (* new goal *)
Robbert Krebbers's avatar
Robbert Krebbers committed
87
      ])
Robbert Krebbers's avatar
Robbert Krebbers committed
88
    || fail "wp_pure: cannot find" efoc "in" e "or" efoc "is not a redex"
89 90 91 92 93
  | |- envs_entails _ (twp ?s ?E ?e ?Q) =>
    let e := eval simpl in e in
    reshape_expr e ltac:(fun K e' =>
      unify e' efoc;
      eapply (tac_twp_pure _ _ _ (fill K e'));
Ralf Jung's avatar
Ralf Jung committed
94
      [iSolveTC                       (* PureExec *)
95
      |try fast_done                  (* The pure condition for PureExec *)
96
      |wp_finish                      (* new goal *)
97
      ])
Robbert Krebbers's avatar
Robbert Krebbers committed
98
    || fail "wp_pure: cannot find" efoc "in" e "or" efoc "is not a redex"
99
  | _ => fail "wp_pure: not a 'wp'"
100 101
  end.

102 103 104 105 106
(* TODO: do this in one go, without [repeat]. *)
Ltac wp_pures :=
  iStartProof;
  repeat (wp_pure _; []). (* The `;[]` makes sure that no side-condition
                             magically spawns. *)
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
107

108 109 110
(** Unlike [wp_pures], the tactics [wp_rec] and [wp_lam] should also reduce
lambdas/recs that are hidden behind a definition, i.e. they should use
[AsRecV_recv] as a proper instance instead of a [Hint Extern].
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
111

112 113 114
We achieve this by putting [AsRecV_recv] in the current environment so that it
can be used as an instance by the typeclass resolution system. We then perform
the reduction, and finally we clear this new hypothesis. *)
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
115 116
Tactic Notation "wp_rec" :=
  let H := fresh in
117
  assert (H := AsRecV_recv);
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
118 119 120
  wp_pure (App _ _);
  clear H.

121
Tactic Notation "wp_if" := wp_pure (If _ _ _).
122 123
Tactic Notation "wp_if_true" := wp_pure (If (LitV (LitBool true)) _ _).
Tactic Notation "wp_if_false" := wp_pure (If (LitV (LitBool false)) _ _).
124 125 126 127
Tactic Notation "wp_unop" := wp_pure (UnOp _ _).
Tactic Notation "wp_binop" := wp_pure (BinOp _ _ _).
Tactic Notation "wp_op" := wp_unop || wp_binop.
Tactic Notation "wp_lam" := wp_rec.
128 129
Tactic Notation "wp_let" := wp_pure (Rec BAnon (BNamed _) _); wp_lam.
Tactic Notation "wp_seq" := wp_pure (Rec BAnon BAnon _); wp_lam.
130 131
Tactic Notation "wp_proj" := wp_pure (Fst _) || wp_pure (Snd _).
Tactic Notation "wp_case" := wp_pure (Case _ _ _).
132 133 134 135
Tactic Notation "wp_match" := wp_case; wp_pure (Rec _ _ _); wp_lam.
Tactic Notation "wp_inj" := wp_pure (InjL _) || wp_pure (InjR _).
Tactic Notation "wp_pair" := wp_pure (Pair _ _).
Tactic Notation "wp_closure" := wp_pure (Rec _ _ _).
136

137
Lemma tac_wp_bind `{!heapG Σ} K Δ s E Φ e f :
138
  f = (λ e, fill K e)  (* as an eta expanded hypothesis so that we can `simpl` it *)
139
  envs_entails Δ (WP e @ s; E {{ v, WP f (Val v) @ s; E {{ Φ }} }})%I 
Ralf Jung's avatar
Ralf Jung committed
140
  envs_entails Δ (WP fill K e @ s; E {{ Φ }}).
141
Proof. rewrite envs_entails_eq=> -> ->. by apply: wp_bind. Qed.
142
Lemma tac_twp_bind `{!heapG Σ} K Δ s E Φ e f :
143
  f = (λ e, fill K e)  (* as an eta expanded hypothesis so that we can `simpl` it *)
144
  envs_entails Δ (WP e @ s; E [{ v, WP f (Val v) @ s; E [{ Φ }] }])%I 
145
  envs_entails Δ (WP fill K e @ s; E [{ Φ }]).
146
Proof. rewrite envs_entails_eq=> -> ->. by apply: twp_bind. Qed.
147

Robbert Krebbers's avatar
Robbert Krebbers committed
148 149 150
Ltac wp_bind_core K :=
  lazymatch eval hnf in K with
  | [] => idtac
151
  | _ => eapply (tac_wp_bind K); [simpl; reflexivity|reduction.pm_prettify]
Robbert Krebbers's avatar
Robbert Krebbers committed
152
  end.
153 154 155
Ltac twp_bind_core K :=
  lazymatch eval hnf in K with
  | [] => idtac
156
  | _ => eapply (tac_twp_bind K); [simpl; reflexivity|reduction.pm_prettify]
157
  end.
Robbert Krebbers's avatar
Robbert Krebbers committed
158

159 160 161
Tactic Notation "wp_bind" open_constr(efoc) :=
  iStartProof;
  lazymatch goal with
162
  | |- envs_entails _ (wp ?s ?E ?e ?Q) =>
163 164
    reshape_expr e ltac:(fun K e' => unify e' efoc; wp_bind_core K)
    || fail "wp_bind: cannot find" efoc "in" e
165 166 167
  | |- envs_entails _ (twp ?s ?E ?e ?Q) =>
    reshape_expr e ltac:(fun K e' => unify e' efoc; twp_bind_core K)
    || fail "wp_bind: cannot find" efoc "in" e
168 169 170 171
  | _ => fail "wp_bind: not a 'wp'"
  end.

(** Heap tactics *)
Robbert Krebbers's avatar
Robbert Krebbers committed
172
Section heap.
173
Context `{!heapG Σ}.
174 175
Implicit Types P Q : iProp Σ.
Implicit Types Φ : val  iProp Σ.
Robbert Krebbers's avatar
Robbert Krebbers committed
176
Implicit Types Δ : envs (uPredI (iResUR Σ)).
177 178
Implicit Types v : val.
Implicit Types z : Z.
Robbert Krebbers's avatar
Robbert Krebbers committed
179

Amin Timany's avatar
Amin Timany committed
180 181 182 183 184 185 186 187 188 189 190 191
Lemma tac_wp_allocN Δ Δ' s E j K v n Φ :
  0 < n 
  MaybeIntoLaterNEnvs 1 Δ Δ' 
  ( l,  Δ'',
    envs_app false (Esnoc Enil j (array l (replicate (Z.to_nat n) v))) Δ' = Some Δ'' 
    envs_entails Δ'' (WP fill K (Val $ LitV l) @ s; E {{ Φ }})) 
  envs_entails Δ (WP fill K (AllocN #n v) @ s; E {{ Φ }}).
Proof.
  rewrite envs_entails_eq=> ? ? HΔ.
  rewrite -wp_bind. eapply wand_apply; first exact: wp_allocN.
  rewrite left_id into_laterN_env_sound; apply later_mono, forall_intro=> l.
  destruct (HΔ l) as (Δ''&?&HΔ'). rewrite envs_app_sound //; simpl.
192
  apply wand_intro_l. by rewrite (sep_elim_l (l ↦∗ _)%I) right_id wand_elim_r.
Amin Timany's avatar
Amin Timany committed
193 194 195 196 197 198 199 200 201 202 203 204 205
Qed.
Lemma tac_twp_allocN Δ s E j K v n Φ :
  0 < n 
  ( l,  Δ',
    envs_app false (Esnoc Enil j (array l (replicate (Z.to_nat n) v))) Δ
    = Some Δ' 
    envs_entails Δ' (WP fill K (Val $ LitV l) @ s; E [{ Φ }])) 
  envs_entails Δ (WP fill K (AllocN #n v) @ s; E [{ Φ }]).
Proof.
  rewrite envs_entails_eq=> ? HΔ.
  rewrite -twp_bind. eapply wand_apply; first exact: twp_allocN.
  rewrite left_id. apply forall_intro=> l.
  destruct (HΔ l) as (Δ'&?&HΔ'). rewrite envs_app_sound //; simpl.
206
  apply wand_intro_l. by rewrite (sep_elim_l (l ↦∗ _)%I) right_id wand_elim_r.
Amin Timany's avatar
Amin Timany committed
207 208
Qed.

209
Lemma tac_wp_alloc Δ Δ' s E j K v Φ :
210
  MaybeIntoLaterNEnvs 1 Δ Δ' 
Robbert Krebbers's avatar
Robbert Krebbers committed
211
  ( l,  Δ'',
212
    envs_app false (Esnoc Enil j (l  v)) Δ' = Some Δ'' 
213 214
    envs_entails Δ'' (WP fill K (Val $ LitV l) @ s; E {{ Φ }})) 
  envs_entails Δ (WP fill K (Alloc v) @ s; E {{ Φ }}).
Robbert Krebbers's avatar
Robbert Krebbers committed
215
Proof.
216
  rewrite envs_entails_eq=> ? HΔ.
217
  rewrite -wp_bind. eapply wand_apply; first exact: wp_alloc.
218
  rewrite left_id into_laterN_env_sound; apply later_mono, forall_intro=> l.
Robbert Krebbers's avatar
Robbert Krebbers committed
219
  destruct (HΔ l) as (Δ''&?&HΔ'). rewrite envs_app_sound //; simpl.
220
  apply wand_intro_l. by rewrite (sep_elim_l (l  v)%I) right_id wand_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
221
Qed.
222
Lemma tac_twp_alloc Δ s E j K v Φ :
223 224
  ( l,  Δ',
    envs_app false (Esnoc Enil j (l  v)) Δ = Some Δ' 
225 226
    envs_entails Δ' (WP fill K (Val $ LitV l) @ s; E [{ Φ }])) 
  envs_entails Δ (WP fill K (Alloc v) @ s; E [{ Φ }]).
227
Proof.
228
  rewrite envs_entails_eq=> HΔ.
229 230 231
  rewrite -twp_bind. eapply wand_apply; first exact: twp_alloc.
  rewrite left_id. apply forall_intro=> l.
  destruct (HΔ l) as (Δ'&?&HΔ'). rewrite envs_app_sound //; simpl.
232
  apply wand_intro_l. by rewrite (sep_elim_l (l  v)%I) right_id wand_elim_r.
233
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
234

235
Lemma tac_wp_load Δ Δ' s E i K l q v Φ :
236
  MaybeIntoLaterNEnvs 1 Δ Δ' 
Robbert Krebbers's avatar
Robbert Krebbers committed
237
  envs_lookup i Δ' = Some (false, l {q} v)%I 
238 239
  envs_entails Δ' (WP fill K (Val v) @ s; E {{ Φ }}) 
  envs_entails Δ (WP fill K (Load (LitV l)) @ s; E {{ Φ }}).
Robbert Krebbers's avatar
Robbert Krebbers committed
240
Proof.
241
  rewrite envs_entails_eq=> ???.
242
  rewrite -wp_bind. eapply wand_apply; first exact: wp_load.
243
  rewrite into_laterN_env_sound -later_sep envs_lookup_split //; simpl.
Robbert Krebbers's avatar
Robbert Krebbers committed
244 245
  by apply later_mono, sep_mono_r, wand_mono.
Qed.
246 247
Lemma tac_twp_load Δ s E i K l q v Φ :
  envs_lookup i Δ = Some (false, l {q} v)%I 
248 249
  envs_entails Δ (WP fill K (Val v) @ s; E [{ Φ }]) 
  envs_entails Δ (WP fill K (Load (LitV l)) @ s; E [{ Φ }]).
250
Proof.
251
  rewrite envs_entails_eq=> ??.
252 253 254 255
  rewrite -twp_bind. eapply wand_apply; first exact: twp_load.
  rewrite envs_lookup_split //; simpl.
  by apply sep_mono_r, wand_mono.
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
256

257
Lemma tac_wp_store Δ Δ' Δ'' s E i K l v v' Φ :
258
  MaybeIntoLaterNEnvs 1 Δ Δ' 
Robbert Krebbers's avatar
Robbert Krebbers committed
259 260
  envs_lookup i Δ' = Some (false, l  v)%I 
  envs_simple_replace i false (Esnoc Enil i (l  v')) Δ' = Some Δ'' 
261 262
  envs_entails Δ'' (WP fill K (Val $ LitV LitUnit) @ s; E {{ Φ }}) 
  envs_entails Δ (WP fill K (Store (LitV l) (Val v')) @ s; E {{ Φ }}).
Robbert Krebbers's avatar
Robbert Krebbers committed
263
Proof.
264
  rewrite envs_entails_eq=> ????.
265
  rewrite -wp_bind. eapply wand_apply; first by eapply wp_store.
266
  rewrite into_laterN_env_sound -later_sep envs_simple_replace_sound //; simpl.
Robbert Krebbers's avatar
Robbert Krebbers committed
267 268
  rewrite right_id. by apply later_mono, sep_mono_r, wand_mono.
Qed.
269
Lemma tac_twp_store Δ Δ' s E i K l v v' Φ :
270 271
  envs_lookup i Δ = Some (false, l  v)%I 
  envs_simple_replace i false (Esnoc Enil i (l  v')) Δ = Some Δ' 
272 273
  envs_entails Δ' (WP fill K (Val $ LitV LitUnit) @ s; E [{ Φ }]) 
  envs_entails Δ (WP fill K (Store (LitV l) v') @ s; E [{ Φ }]).
274
Proof.
275 276
  rewrite envs_entails_eq. intros. rewrite -twp_bind.
  eapply wand_apply; first by eapply twp_store.
277 278 279
  rewrite envs_simple_replace_sound //; simpl.
  rewrite right_id. by apply sep_mono_r, wand_mono.
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
280

281
Lemma tac_wp_cas Δ Δ' Δ'' s E i K l v v1 v2 Φ :
282 283 284 285
  MaybeIntoLaterNEnvs 1 Δ Δ' 
  envs_lookup i Δ' = Some (false, l  v)%I 
  envs_simple_replace i false (Esnoc Enil i (l  v2)) Δ' = Some Δ'' 
  vals_cas_compare_safe v v1 
286 287 288
  (v = v1  envs_entails Δ'' (WP fill K (Val $ LitV true) @ s; E {{ Φ }})) 
  (v  v1  envs_entails Δ' (WP fill K (Val $ LitV false) @ s; E {{ Φ }})) 
  envs_entails Δ (WP fill K (CAS (LitV l) (Val v1) (Val v2)) @ s; E {{ Φ }}).
289
Proof.
290
  rewrite envs_entails_eq=> ???? Hsuc Hfail. destruct (decide (v = v1)) as [<-|Hne].
291 292 293 294
  - rewrite -wp_bind. eapply wand_apply; first exact: wp_cas_suc.
    rewrite into_laterN_env_sound -later_sep /= {1}envs_simple_replace_sound //; simpl.
    apply later_mono, sep_mono_r. rewrite right_id. apply wand_mono; auto.
  - rewrite -wp_bind. eapply wand_apply.
295
    { eapply wp_cas_fail; eauto. }
296 297 298
    rewrite into_laterN_env_sound -later_sep /= {1}envs_lookup_split //; simpl.
    apply later_mono, sep_mono_r. apply wand_mono; auto.
Qed.
299
Lemma tac_twp_cas Δ Δ' s E i K l v v1 v2 Φ :
300 301 302
  envs_lookup i Δ = Some (false, l  v)%I 
  envs_simple_replace i false (Esnoc Enil i (l  v2)) Δ = Some Δ' 
  vals_cas_compare_safe v v1 
303 304 305
  (v = v1  envs_entails Δ' (WP fill K (Val $ LitV true) @ s; E [{ Φ }])) 
  (v  v1  envs_entails Δ (WP fill K (Val $ LitV false) @ s; E [{ Φ }])) 
  envs_entails Δ (WP fill K (CAS (LitV l) v1 v2) @ s; E [{ Φ }]).
306
Proof.
307
  rewrite envs_entails_eq=> ??? Hsuc Hfail. destruct (decide (v = v1)) as [<-|Hne].
308 309 310 311
  - rewrite -twp_bind. eapply wand_apply; first exact: twp_cas_suc.
    rewrite /= {1}envs_simple_replace_sound //; simpl.
    apply sep_mono_r. rewrite right_id. apply wand_mono; auto.
  - rewrite -twp_bind. eapply wand_apply.
312
    { eapply twp_cas_fail; eauto. }
313 314 315 316
    rewrite /= {1}envs_lookup_split //; simpl.
    apply sep_mono_r. apply wand_mono; auto.
Qed.

317
Lemma tac_wp_cas_fail Δ Δ' s E i K l q v v1 v2 Φ :
318
  MaybeIntoLaterNEnvs 1 Δ Δ' 
319 320
  envs_lookup i Δ' = Some (false, l {q} v)%I 
  v  v1  vals_cas_compare_safe v v1 
321 322
  envs_entails Δ' (WP fill K (Val $ LitV false) @ s; E {{ Φ }}) 
  envs_entails Δ (WP fill K (CAS (LitV l) v1 v2) @ s; E {{ Φ }}).
Robbert Krebbers's avatar
Robbert Krebbers committed
323
Proof.
324
  rewrite envs_entails_eq=> ?????.
325
  rewrite -wp_bind. eapply wand_apply; first exact: wp_cas_fail.
326
  rewrite into_laterN_env_sound -later_sep envs_lookup_split //; simpl.
Robbert Krebbers's avatar
Robbert Krebbers committed
327 328
  by apply later_mono, sep_mono_r, wand_mono.
Qed.
329
Lemma tac_twp_cas_fail Δ s E i K l q v v1 v2 Φ :
330 331
  envs_lookup i Δ = Some (false, l {q} v)%I 
  v  v1  vals_cas_compare_safe v v1 
332 333
  envs_entails Δ (WP fill K (Val $ LitV false) @ s; E [{ Φ }]) 
  envs_entails Δ (WP fill K (CAS (LitV l) v1 v2) @ s; E [{ Φ }]).
334
Proof.
335 336 337
  rewrite envs_entails_eq. intros. rewrite -twp_bind.
  eapply wand_apply; first exact: twp_cas_fail.
  rewrite envs_lookup_split //=. by do 2 f_equiv.
338
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
339

340
Lemma tac_wp_cas_suc Δ Δ' Δ'' s E i K l v v1 v2 Φ :
341
  MaybeIntoLaterNEnvs 1 Δ Δ' 
342
  envs_lookup i Δ' = Some (false, l  v)%I 
Robbert Krebbers's avatar
Robbert Krebbers committed
343
  envs_simple_replace i false (Esnoc Enil i (l  v2)) Δ' = Some Δ'' 
344
  v = v1  val_is_unboxed v 
345 346
  envs_entails Δ'' (WP fill K (Val $ LitV true) @ s; E {{ Φ }}) 
  envs_entails Δ (WP fill K (CAS (LitV l) v1 v2) @ s; E {{ Φ }}).
Robbert Krebbers's avatar
Robbert Krebbers committed
347
Proof.
348
  rewrite envs_entails_eq=> ??????; subst.
349 350
  rewrite -wp_bind. eapply wand_apply.
  { eapply wp_cas_suc; eauto. by left. }
351
  rewrite into_laterN_env_sound -later_sep envs_simple_replace_sound //; simpl.
Robbert Krebbers's avatar
Robbert Krebbers committed
352 353
  rewrite right_id. by apply later_mono, sep_mono_r, wand_mono.
Qed.
354
Lemma tac_twp_cas_suc Δ Δ' s E i K l v v1 v2 Φ :
355
  envs_lookup i Δ = Some (false, l  v)%I 
356
  envs_simple_replace i false (Esnoc Enil i (l  v2)) Δ = Some Δ' 
357
  v = v1  val_is_unboxed v 
358 359
  envs_entails Δ' (WP fill K (Val $ LitV true) @ s; E [{ Φ }]) 
  envs_entails Δ (WP fill K (CAS (LitV l) v1 v2) @ s; E [{ Φ }]).
360
Proof.
361
  rewrite envs_entails_eq=>?????; subst.
362 363
  rewrite -twp_bind. eapply wand_apply.
  { eapply twp_cas_suc; eauto. by left. }
364 365 366
  rewrite envs_simple_replace_sound //; simpl.
  rewrite right_id. by apply sep_mono_r, wand_mono.
Qed.
367

368
Lemma tac_wp_faa Δ Δ' Δ'' s E i K l z1 z2 Φ :
369
  MaybeIntoLaterNEnvs 1 Δ Δ' 
370 371 372 373
  envs_lookup i Δ' = Some (false, l  LitV z1)%I 
  envs_simple_replace i false (Esnoc Enil i (l  LitV (z1 + z2))) Δ' = Some Δ'' 
  envs_entails Δ'' (WP fill K (Val $ LitV z1) @ s; E {{ Φ }}) 
  envs_entails Δ (WP fill K (FAA (LitV l) (LitV z2)) @ s; E {{ Φ }}).
374
Proof.
375 376
  rewrite envs_entails_eq=> ????.
  rewrite -wp_bind. eapply wand_apply; first exact: (wp_faa _ _ _ z1 z2).
377 378 379
  rewrite into_laterN_env_sound -later_sep envs_simple_replace_sound //; simpl.
  rewrite right_id. by apply later_mono, sep_mono_r, wand_mono.
Qed.
380 381 382 383 384
Lemma tac_twp_faa Δ Δ' s E i K l z1 z2 Φ :
  envs_lookup i Δ = Some (false, l  LitV z1)%I 
  envs_simple_replace i false (Esnoc Enil i (l  LitV (z1 + z2))) Δ = Some Δ' 
  envs_entails Δ' (WP fill K (Val $ LitV z1) @ s; E [{ Φ }]) 
  envs_entails Δ (WP fill K (FAA (LitV l) (LitV z2)) @ s; E [{ Φ }]).
385
Proof.
386 387
  rewrite envs_entails_eq=> ???.
  rewrite -twp_bind. eapply wand_apply; first exact: (twp_faa _ _ _ z1 z2).
388 389 390
  rewrite envs_simple_replace_sound //; simpl.
  rewrite right_id. by apply sep_mono_r, wand_mono.
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
391 392
End heap.

Ralf Jung's avatar
Ralf Jung committed
393 394
(** Evaluate [lem] to a hypothesis [H] that can be applied, and then run
[wp_bind K; tac H] for every possible evaluation context.  [tac] can do
Ralf Jung's avatar
Ralf Jung committed
395 396
[iApplyHyp H] to actually apply the hypothesis.  TC resolution of [lem] premises
happens *after* [tac H] got executed. *)
397
Tactic Notation "wp_apply_core" open_constr(lem) tactic(tac) :=
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
398
  wp_pures;
399 400
  iPoseProofCore lem as false true (fun H =>
    lazymatch goal with
401
    | |- envs_entails _ (wp ?s ?E ?e ?Q) =>
402
      reshape_expr e ltac:(fun K e' =>
403
        wp_bind_core K; tac H) ||
404 405 406
      lazymatch iTypeOf H with
      | Some (_,?P) => fail "wp_apply: cannot apply" P
      end
407 408
    | |- envs_entails _ (twp ?s ?E ?e ?Q) =>
      reshape_expr e ltac:(fun K e' =>
409
        twp_bind_core K; tac H) ||
410 411 412
      lazymatch iTypeOf H with
      | Some (_,?P) => fail "wp_apply: cannot apply" P
      end
413 414
    | _ => fail "wp_apply: not a 'wp'"
    end).
415 416
Tactic Notation "wp_apply" open_constr(lem) :=
  wp_apply_core lem (fun H => iApplyHyp H; try iNext; try wp_expr_simpl).
Ralf Jung's avatar
Ralf Jung committed
417 418 419 420
(** Tactic tailored for atomic triples: the first, simple one just runs
[iAuIntro] on the goal, as atomic triples always have an atomic update as their
premise.  The second one additionaly does some framing: it gets rid of [Hs] from
the context, which is intended to be the non-laterable assertions that iAuIntro
421 422
would choke on.  You get them all back in the continuation of the atomic
operation. *)
423
Tactic Notation "awp_apply" open_constr(lem) :=
424
  wp_apply_core lem (fun H => iApplyHyp H; last iAuIntro).
425
Tactic Notation "awp_apply" open_constr(lem) "without" constr(Hs) :=
426
  wp_apply_core lem (fun H => iApply wp_frame_wand_l; iSplitL Hs; [iAccu|iApplyHyp H; last iAuIntro]).
Robbert Krebbers's avatar
Robbert Krebbers committed
427 428

Tactic Notation "wp_alloc" ident(l) "as" constr(H) :=
429
  let Htmp := iFresh in
430 431 432
  let finish _ :=
    first [intros l | fail 1 "wp_alloc:" l "not fresh"];
      eexists; split;
433
        [pm_reflexivity || fail "wp_alloc:" H "not fresh"
434
        |iDestructHyp Htmp as H; wp_finish] in
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
435
  wp_pures;
Amin Timany's avatar
Amin Timany committed
436 437 438 439 440 441 442 443
  (** The code first tries to use allocation lemma for a single reference,
     ie, [tac_wp_alloc] (respectively, [tac_twp_alloc]).
     If that fails, it tries to use the lemma [tac_wp_allocN]
     (respectively, [tac_twp_allocN]) for allocating an array.
     Notice that we could have used the array allocation lemma also for single
     references. However, that would produce the resource l ↦∗ [v] instead of
     l ↦ v for single references. These are logically equivalent assertions
     but are not equal. *)
444
  lazymatch goal with
445
  | |- envs_entails _ (wp ?s ?E ?e ?Q) =>
Amin Timany's avatar
Amin Timany committed
446 447 448 449 450 451 452 453 454 455 456 457 458 459
    let process_single _ :=
        first
          [reshape_expr e ltac:(fun K e' => eapply (tac_wp_alloc _ _ _ _ Htmp K))
          |fail 1 "wp_alloc: cannot find 'Alloc' in" e];
        [iSolveTC
        |finish ()]
    in
    let process_array _ :=
        first
          [reshape_expr e ltac:(fun K e' => eapply (tac_wp_allocN _ _ _ _ Htmp K))
          |fail 1 "wp_alloc: cannot find 'Alloc' in" e];
        [idtac|iSolveTC
         |finish ()]
    in (process_single ()) || (process_array ())
460
  | |- envs_entails _ (twp ?s ?E ?e ?Q) =>
Amin Timany's avatar
Amin Timany committed
461 462 463 464 465 466 467 468 469 470 471 472
    let process_single _ :=
        first
          [reshape_expr e ltac:(fun K e' => eapply (tac_twp_alloc _ _ _ Htmp K))
          |fail 1 "wp_alloc: cannot find 'Alloc' in" e];
        finish ()
    in
    let process_array _ :=
        first
          [reshape_expr e ltac:(fun K e' => eapply (tac_twp_allocN _ _ _ Htmp K))
          |fail 1 "wp_alloc: cannot find 'Alloc' in" e];
        finish ()
    in (process_single ()) || (process_array ())
473
  | _ => fail "wp_alloc: not a 'wp'"
Robbert Krebbers's avatar
Robbert Krebbers committed
474
  end.
475

476
Tactic Notation "wp_alloc" ident(l) :=
477
  wp_alloc l as "?".
Robbert Krebbers's avatar
Robbert Krebbers committed
478 479

Tactic Notation "wp_load" :=
480 481 482
  let solve_mapsto _ :=
    let l := match goal with |- _ = Some (_, (?l {_} _)%I) => l end in
    iAssumptionCore || fail "wp_load: cannot find" l "↦ ?" in
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
483
  wp_pures;
484
  lazymatch goal with
485
  | |- envs_entails _ (wp ?s ?E ?e ?Q) =>
486
    first
487
      [reshape_expr e ltac:(fun K e' => eapply (tac_wp_load _ _ _ _ _ K))
488
      |fail 1 "wp_load: cannot find 'Load' in" e];
Ralf Jung's avatar
Ralf Jung committed
489
    [iSolveTC
490
    |solve_mapsto ()
491
    |wp_finish]
492 493 494 495 496
  | |- envs_entails _ (twp ?s ?E ?e ?Q) =>
    first
      [reshape_expr e ltac:(fun K e' => eapply (tac_twp_load _ _ _ _ K))
      |fail 1 "wp_load: cannot find 'Load' in" e];
    [solve_mapsto ()
497
    |wp_finish]
498
  | _ => fail "wp_load: not a 'wp'"
Robbert Krebbers's avatar
Robbert Krebbers committed
499 500 501
  end.

Tactic Notation "wp_store" :=
502 503 504
  let solve_mapsto _ :=
    let l := match goal with |- _ = Some (_, (?l {_} _)%I) => l end in
    iAssumptionCore || fail "wp_store: cannot find" l "↦ ?" in
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
505
  wp_pures;
506
  lazymatch goal with
507
  | |- envs_entails _ (wp ?s ?E ?e ?Q) =>
508
    first
509
      [reshape_expr e ltac:(fun K e' => eapply (tac_wp_store _ _ _ _ _ _ K))
510
      |fail 1 "wp_store: cannot find 'Store' in" e];
Ralf Jung's avatar
Ralf Jung committed
511
    [iSolveTC
512
    |solve_mapsto ()
513
    |pm_reflexivity
514
    |first [wp_seq|wp_finish]]
515 516
  | |- envs_entails _ (twp ?s ?E ?e ?Q) =>
    first
517
      [reshape_expr e ltac:(fun K e' => eapply (tac_twp_store _ _ _ _ _ K))
518 519
      |fail 1 "wp_store: cannot find 'Store' in" e];
    [solve_mapsto ()
520
    |pm_reflexivity
521
    |first [wp_seq|wp_finish]]
522
  | _ => fail "wp_store: not a 'wp'"
Robbert Krebbers's avatar
Robbert Krebbers committed
523 524
  end.

525 526 527 528
Tactic Notation "wp_cas" "as" simple_intropattern(H1) "|" simple_intropattern(H2) :=
  let solve_mapsto _ :=
    let l := match goal with |- _ = Some (_, (?l {_} _)%I) => l end in
    iAssumptionCore || fail "wp_cas: cannot find" l "↦ ?" in
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
529
  wp_pures;
530 531 532
  lazymatch goal with
  | |- envs_entails _ (wp ?s ?E ?e ?Q) =>
    first
533
      [reshape_expr e ltac:(fun K e' => eapply (tac_wp_cas _ _ _ _ _ _ K))
534 535 536 537 538
      |fail 1 "wp_cas: cannot find 'CAS' in" e];
    [iSolveTC
    |solve_mapsto ()
    |pm_reflexivity
    |try (fast_done || (left; fast_done) || (right; fast_done)) (* vals_cas_compare_safe *)
539 540
    |intros H1; wp_finish
    |intros H2; wp_finish]
541 542
  | |- envs_entails _ (twp ?E ?e ?Q) =>
    first
543
      [reshape_expr e ltac:(fun K e' => eapply (tac_twp_cas _ _ _ _ _ K))
544 545 546 547
      |fail 1 "wp_cas: cannot find 'CAS' in" e];
    [solve_mapsto ()
    |pm_reflexivity
    |try (fast_done || (left; fast_done) || (right; fast_done)) (* vals_cas_compare_safe *)
548 549
    |intros H1; wp_finish
    |intros H2; wp_finish]
550 551 552
  | _ => fail "wp_cas: not a 'wp'"
  end.

Robbert Krebbers's avatar
Robbert Krebbers committed
553
Tactic Notation "wp_cas_fail" :=
554 555 556
  let solve_mapsto _ :=
    let l := match goal with |- _ = Some (_, (?l {_} _)%I) => l end in
    iAssumptionCore || fail "wp_cas_fail: cannot find" l "↦ ?" in
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
557
  wp_pures;
558
  lazymatch goal with
559
  | |- envs_entails _ (wp ?s ?E ?e ?Q) =>
560
    first
561
      [reshape_expr e ltac:(fun K e' => eapply (tac_wp_cas_fail _ _ _ _ _ K))
562
      |fail 1 "wp_cas_fail: cannot find 'CAS' in" e];
Ralf Jung's avatar
Ralf Jung committed
563
    [iSolveTC
564 565
    |solve_mapsto ()
    |try congruence
566
    |try (fast_done || (left; fast_done) || (right; fast_done)) (* vals_cas_compare_safe *)
567
    |wp_finish]
568 569
  | |- envs_entails _ (twp ?s ?E ?e ?Q) =>
    first
570
      [reshape_expr e ltac:(fun K e' => eapply (tac_twp_cas_fail _ _ _ _ K))
571 572
      |fail 1 "wp_cas_fail: cannot find 'CAS' in" e];
    [solve_mapsto ()
573
    |try congruence
574
    |try (fast_done || (left; fast_done) || (right; fast_done)) (* vals_cas_compare_safe *)
575
    |wp_finish]
576
  | _ => fail "wp_cas_fail: not a 'wp'"
Robbert Krebbers's avatar
Robbert Krebbers committed
577 578 579
  end.

Tactic Notation "wp_cas_suc" :=
580 581 582
  let solve_mapsto _ :=
    let l := match goal with |- _ = Some (_, (?l {_} _)%I) => l end in
    iAssumptionCore || fail "wp_cas_suc: cannot find" l "↦ ?" in
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
583
  wp_pures;
584
  lazymatch goal with
585
  | |- envs_entails _ (wp ?s ?E ?e ?Q) =>
586
    first
587
      [reshape_expr e ltac:(fun K e' => eapply (tac_wp_cas_suc _ _ _ _ _ _ K))
588
      |fail 1 "wp_cas_suc: cannot find 'CAS' in" e];
Ralf Jung's avatar
Ralf Jung committed
589
    [iSolveTC
590
    |solve_mapsto ()
591
    |pm_reflexivity
592 593
    |try congruence
    |try fast_done (* vals_cas_compare_safe *)
594
    |wp_finish]
Robbert Krebbers's avatar
Robbert Krebbers committed
595
  | |- envs_entails _ (twp ?s ?E ?e ?Q) =>
596
    first
597
      [reshape_expr e ltac:(fun K e' => eapply (tac_twp_cas_suc _ _ _ _ _ K))
598 599
      |fail 1 "wp_cas_suc: cannot find 'CAS' in" e];
    [solve_mapsto ()
600
    |pm_reflexivity
601 602
    |try congruence
    |try fast_done (* vals_cas_compare_safe *)
603
    |wp_finish]
604
  | _ => fail "wp_cas_suc: not a 'wp'"
Robbert Krebbers's avatar
Robbert Krebbers committed
605
  end.
606 607

Tactic Notation "wp_faa" :=
608 609 610
  let solve_mapsto _ :=
    let l := match goal with |- _ = Some (_, (?l {_} _)%I) => l end in
    iAssumptionCore || fail "wp_cas_suc: cannot find" l "↦ ?" in
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
611
  wp_pures;
612
  lazymatch goal with
Ralf Jung's avatar
Ralf Jung committed
613
  | |- envs_entails _ (wp ?s ?E ?e ?Q) =>
614
    first
615
      [reshape_expr e ltac:(fun K e' => eapply (tac_wp_faa _ _ _ _ _ _ K))