proofmode.v 26.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
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 Δ'' 
185 186
    envs_entails Δ'' (WP fill K (Val $ LitV $ LitLoc l) @ s; E {{ Φ }})) 
  envs_entails Δ (WP fill K (AllocN (Val $ LitV $ LitInt n) (Val v)) @ s; E {{ Φ }}).
Amin Timany's avatar
Amin Timany committed
187 188 189 190 191
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
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 Δ' 
199 200
    envs_entails Δ' (WP fill K (Val $ LitV $ LitLoc l) @ s; E [{ Φ }])) 
  envs_entails Δ (WP fill K (AllocN (Val $ LitV $ LitInt n) (Val v)) @ s; E [{ Φ }]).
Amin Timany's avatar
Amin Timany committed
201 202 203 204 205
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
    envs_entails Δ'' (WP fill K (Val $ LitV l) @ s; E {{ Φ }})) 
214
  envs_entails Δ (WP fill K (Alloc (Val 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 $ LitLoc l) @ s; E [{ Φ }])) 
  envs_entails Δ (WP fill K (Alloc (Val 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

Ralf Jung's avatar
Ralf Jung committed
281
Lemma tac_wp_cmpxchg Δ Δ' Δ'' s E i K l v v1 v2 Φ :
282 283 284
  MaybeIntoLaterNEnvs 1 Δ Δ' 
  envs_lookup i Δ' = Some (false, l  v)%I 
  envs_simple_replace i false (Esnoc Enil i (l  v2)) Δ' = Some Δ'' 
Ralf Jung's avatar
Ralf Jung committed
285
  vals_cmpxchg_compare_safe v v1 
286
  (val_for_compare v = val_for_compare v1 
287
   envs_entails Δ'' (WP fill K (Val $ PairV v (LitV $ LitBool true)) @ s; E {{ Φ }})) 
288
  (val_for_compare v  val_for_compare v1 
289
   envs_entails Δ' (WP fill K (Val $ PairV v (LitV $ LitBool false)) @ s; E {{ Φ }})) 
Ralf Jung's avatar
Ralf Jung committed
290
  envs_entails Δ (WP fill K (CmpXchg (LitV l) (Val v1) (Val v2)) @ s; E {{ Φ }}).
291
Proof.
292 293 294
  rewrite envs_entails_eq=> ???? Hsuc Hfail.
  destruct (decide (val_for_compare v = val_for_compare v1)) as [Heq|Hne].
  - rewrite -wp_bind. eapply wand_apply.
Ralf Jung's avatar
Ralf Jung committed
295
    { eapply wp_cmpxchg_suc; eauto. }
296 297 298
    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.
Ralf Jung's avatar
Ralf Jung committed
299
    { eapply wp_cmpxchg_fail; eauto. }
300 301 302
    rewrite into_laterN_env_sound -later_sep /= {1}envs_lookup_split //; simpl.
    apply later_mono, sep_mono_r. apply wand_mono; auto.
Qed.
Ralf Jung's avatar
Ralf Jung committed
303
Lemma tac_twp_cmpxchg Δ Δ' s E i K l v v1 v2 Φ :
304 305
  envs_lookup i Δ = Some (false, l  v)%I 
  envs_simple_replace i false (Esnoc Enil i (l  v2)) Δ = Some Δ' 
Ralf Jung's avatar
Ralf Jung committed
306
  vals_cmpxchg_compare_safe v v1 
307
  (val_for_compare v = val_for_compare v1 
308
   envs_entails Δ' (WP fill K (Val $ PairV v (LitV $ LitBool true)) @ s; E [{ Φ }])) 
309
  (val_for_compare v  val_for_compare v1 
310
   envs_entails Δ (WP fill K (Val $ PairV v (LitV $ LitBool false)) @ s; E [{ Φ }])) 
Ralf Jung's avatar
Ralf Jung committed
311
  envs_entails Δ (WP fill K (CmpXchg (LitV l) v1 v2) @ s; E [{ Φ }]).
312
Proof.
313 314 315
  rewrite envs_entails_eq=> ??? Hsuc Hfail.
  destruct (decide (val_for_compare v = val_for_compare v1)) as [Heq|Hne].
  - rewrite -twp_bind. eapply wand_apply.
Ralf Jung's avatar
Ralf Jung committed
316
    { eapply twp_cmpxchg_suc; eauto. }
317 318 319
    rewrite /= {1}envs_simple_replace_sound //; simpl.
    apply sep_mono_r. rewrite right_id. apply wand_mono; auto.
  - rewrite -twp_bind. eapply wand_apply.
Ralf Jung's avatar
Ralf Jung committed
320
    { eapply twp_cmpxchg_fail; eauto. }
321 322 323 324
    rewrite /= {1}envs_lookup_split //; simpl.
    apply sep_mono_r. apply wand_mono; auto.
Qed.

Ralf Jung's avatar
Ralf Jung committed
325
Lemma tac_wp_cmpxchg_fail Δ Δ' s E i K l q v v1 v2 Φ :
326
  MaybeIntoLaterNEnvs 1 Δ Δ' 
327
  envs_lookup i Δ' = Some (false, l {q} v)%I 
Ralf Jung's avatar
Ralf Jung committed
328
  val_for_compare v  val_for_compare v1  vals_cmpxchg_compare_safe v v1 
329
  envs_entails Δ' (WP fill K (Val $ PairV v (LitV $ LitBool false)) @ s; E {{ Φ }}) 
Ralf Jung's avatar
Ralf Jung committed
330
  envs_entails Δ (WP fill K (CmpXchg (LitV l) v1 v2) @ s; E {{ Φ }}).
Robbert Krebbers's avatar
Robbert Krebbers committed
331
Proof.
332
  rewrite envs_entails_eq=> ?????.
Ralf Jung's avatar
Ralf Jung committed
333
  rewrite -wp_bind. eapply wand_apply; first exact: wp_cmpxchg_fail.
334
  rewrite into_laterN_env_sound -later_sep envs_lookup_split //; simpl.
Robbert Krebbers's avatar
Robbert Krebbers committed
335 336
  by apply later_mono, sep_mono_r, wand_mono.
Qed.
Ralf Jung's avatar
Ralf Jung committed
337
Lemma tac_twp_cmpxchg_fail Δ s E i K l q v v1 v2 Φ :
338
  envs_lookup i Δ = Some (false, l {q} v)%I 
Ralf Jung's avatar
Ralf Jung committed
339
  val_for_compare v  val_for_compare v1  vals_cmpxchg_compare_safe v v1 
340
  envs_entails Δ (WP fill K (Val $ PairV v (LitV $ LitBool false)) @ s; E [{ Φ }]) 
Ralf Jung's avatar
Ralf Jung committed
341
  envs_entails Δ (WP fill K (CmpXchg (LitV l) v1 v2) @ s; E [{ Φ }]).
342
Proof.
343
  rewrite envs_entails_eq. intros. rewrite -twp_bind.
Ralf Jung's avatar
Ralf Jung committed
344
  eapply wand_apply; first exact: twp_cmpxchg_fail.
345
  rewrite envs_lookup_split //=. by do 2 f_equiv.
346
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
347

Ralf Jung's avatar
Ralf Jung committed
348
Lemma tac_wp_cmpxchg_suc Δ Δ' Δ'' s E i K l v v1 v2 Φ :
349
  MaybeIntoLaterNEnvs 1 Δ Δ' 
350
  envs_lookup i Δ' = Some (false, l  v)%I 
Robbert Krebbers's avatar
Robbert Krebbers committed
351
  envs_simple_replace i false (Esnoc Enil i (l  v2)) Δ' = Some Δ'' 
Ralf Jung's avatar
Ralf Jung committed
352
  val_for_compare v = val_for_compare v1  vals_cmpxchg_compare_safe v v1 
353
  envs_entails Δ'' (WP fill K (Val $ PairV v (LitV $ LitBool true)) @ s; E {{ Φ }}) 
Ralf Jung's avatar
Ralf Jung committed
354
  envs_entails Δ (WP fill K (CmpXchg (LitV l) v1 v2) @ s; E {{ Φ }}).
Robbert Krebbers's avatar
Robbert Krebbers committed
355
Proof.
356
  rewrite envs_entails_eq=> ??????; subst.
357
  rewrite -wp_bind. eapply wand_apply.
Ralf Jung's avatar
Ralf Jung committed
358
  { eapply wp_cmpxchg_suc; eauto. }
359
  rewrite into_laterN_env_sound -later_sep envs_simple_replace_sound //; simpl.
Robbert Krebbers's avatar
Robbert Krebbers committed
360 361
  rewrite right_id. by apply later_mono, sep_mono_r, wand_mono.
Qed.
Ralf Jung's avatar
Ralf Jung committed
362
Lemma tac_twp_cmpxchg_suc Δ Δ' s E i K l v v1 v2 Φ :
363
  envs_lookup i Δ = Some (false, l  v)%I 
364
  envs_simple_replace i false (Esnoc Enil i (l  v2)) Δ = Some Δ' 
Ralf Jung's avatar
Ralf Jung committed
365
  val_for_compare v = val_for_compare v1  vals_cmpxchg_compare_safe v v1 
366
  envs_entails Δ' (WP fill K (Val $ PairV v (LitV $ LitBool true)) @ s; E [{ Φ }]) 
Ralf Jung's avatar
Ralf Jung committed
367
  envs_entails Δ (WP fill K (CmpXchg (LitV l) v1 v2) @ s; E [{ Φ }]).
368
Proof.
369
  rewrite envs_entails_eq=>?????; subst.
370
  rewrite -twp_bind. eapply wand_apply.
Ralf Jung's avatar
Ralf Jung committed
371
  { eapply twp_cmpxchg_suc; eauto. }
372 373 374
  rewrite envs_simple_replace_sound //; simpl.
  rewrite right_id. by apply sep_mono_r, wand_mono.
Qed.
375

376
Lemma tac_wp_faa Δ Δ' Δ'' s E i K l z1 z2 Φ :
377
  MaybeIntoLaterNEnvs 1 Δ Δ' 
378 379 380 381
  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 {{ Φ }}).
382
Proof.
383 384
  rewrite envs_entails_eq=> ????.
  rewrite -wp_bind. eapply wand_apply; first exact: (wp_faa _ _ _ z1 z2).
385 386 387
  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.
388 389 390 391 392
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 [{ Φ }]).
393
Proof.
394 395
  rewrite envs_entails_eq=> ???.
  rewrite -twp_bind. eapply wand_apply; first exact: (twp_faa _ _ _ z1 z2).
396 397 398
  rewrite envs_simple_replace_sound //; simpl.
  rewrite right_id. by apply sep_mono_r, wand_mono.
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
399 400
End heap.

Ralf Jung's avatar
Ralf Jung committed
401 402
(** 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
403 404
[iApplyHyp H] to actually apply the hypothesis.  TC resolution of [lem] premises
happens *after* [tac H] got executed. *)
405
Tactic Notation "wp_apply_core" open_constr(lem) tactic(tac) :=
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
406
  wp_pures;
Paolo G. Giarrusso's avatar
Paolo G. Giarrusso committed
407
  iPoseProofCore lem as false (fun H =>
408
    lazymatch goal with
409
    | |- envs_entails _ (wp ?s ?E ?e ?Q) =>
410
      reshape_expr e ltac:(fun K e' =>
411
        wp_bind_core K; tac H) ||
412 413 414
      lazymatch iTypeOf H with
      | Some (_,?P) => fail "wp_apply: cannot apply" P
      end
415 416
    | |- envs_entails _ (twp ?s ?E ?e ?Q) =>
      reshape_expr e ltac:(fun K e' =>
417
        twp_bind_core K; tac H) ||
418 419 420
      lazymatch iTypeOf H with
      | Some (_,?P) => fail "wp_apply: cannot apply" P
      end
421 422
    | _ => fail "wp_apply: not a 'wp'"
    end).
423 424
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
425 426 427 428
(** 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
429 430
would choke on.  You get them all back in the continuation of the atomic
operation. *)
431
Tactic Notation "awp_apply" open_constr(lem) :=
432
  wp_apply_core lem (fun H => iApplyHyp H; last iAuIntro).
433
Tactic Notation "awp_apply" open_constr(lem) "without" constr(Hs) :=
434
  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
435 436

Tactic Notation "wp_alloc" ident(l) "as" constr(H) :=
437
  let Htmp := iFresh in
438 439 440
  let finish _ :=
    first [intros l | fail 1 "wp_alloc:" l "not fresh"];
      eexists; split;
441
        [pm_reflexivity || fail "wp_alloc:" H "not fresh"
442
        |iDestructHyp Htmp as H; wp_finish] in
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
443
  wp_pures;
Amin Timany's avatar
Amin Timany committed
444 445 446 447 448 449 450 451
  (** 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. *)
452
  lazymatch goal with
453
  | |- envs_entails _ (wp ?s ?E ?e ?Q) =>
Amin Timany's avatar
Amin Timany committed
454 455 456 457 458 459 460 461 462 463 464 465 466 467
    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 ())
468
  | |- envs_entails _ (twp ?s ?E ?e ?Q) =>
Amin Timany's avatar
Amin Timany committed
469 470 471 472 473 474 475 476 477 478 479 480
    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 ())
481
  | _ => fail "wp_alloc: not a 'wp'"
Robbert Krebbers's avatar
Robbert Krebbers committed
482
  end.
483

484
Tactic Notation "wp_alloc" ident(l) :=
485
  wp_alloc l as "?".
Robbert Krebbers's avatar
Robbert Krebbers committed
486 487

Tactic Notation "wp_load" :=
488 489 490
  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
491
  wp_pures;
492
  lazymatch goal with
493
  | |- envs_entails _ (wp ?s ?E ?e ?Q) =>
494
    first
495
      [reshape_expr e ltac:(fun K e' => eapply (tac_wp_load _ _ _ _ _ K))
496
      |fail 1 "wp_load: cannot find 'Load' in" e];
Ralf Jung's avatar
Ralf Jung committed
497
    [iSolveTC
498
    |solve_mapsto ()
499
    |wp_finish]
500 501 502 503 504
  | |- 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 ()
505
    |wp_finish]
506
  | _ => fail "wp_load: not a 'wp'"
Robbert Krebbers's avatar
Robbert Krebbers committed
507 508 509
  end.

Tactic Notation "wp_store" :=
510 511 512
  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
513
  wp_pures;
514
  lazymatch goal with
515
  | |- envs_entails _ (wp ?s ?E ?e ?Q) =>
516
    first
517
      [reshape_expr e ltac:(fun K e' => eapply (tac_wp_store _ _ _ _ _ _ K))
518
      |fail 1 "wp_store: cannot find 'Store' in" e];
Ralf Jung's avatar
Ralf Jung committed
519
    [iSolveTC
520
    |solve_mapsto ()
521
    |pm_reflexivity
522
    |first [wp_seq|wp_finish]]
523 524
  | |- envs_entails _ (twp ?s ?E ?e ?Q) =>
    first
525
      [reshape_expr e ltac:(fun K e' => eapply (tac_twp_store _ _ _ _ _ K))
526 527
      |fail 1 "wp_store: cannot find 'Store' in" e];
    [solve_mapsto ()
528
    |pm_reflexivity
529
    |first [wp_seq|wp_finish]]
530
  | _ => fail "wp_store: not a 'wp'"
Robbert Krebbers's avatar
Robbert Krebbers committed
531 532
  end.

Ralf Jung's avatar
Ralf Jung committed
533 534
Ltac solve_vals_cmpxchg_compare_safe :=
  (* The first branch is for when we have [vals_cmpxchg_compare_safe] in the context.
535 536 537 538
     The other two branches are for when either one of the branches reduces to
     [True] or we have it in the context. *)
  fast_done || (left; fast_done) || (right; fast_done).

Ralf Jung's avatar
Ralf Jung committed
539
Tactic Notation "wp_cmpxchg" "as" simple_intropattern(H1) "|" simple_intropattern(H2) :=
540 541
  let solve_mapsto _ :=
    let l := match goal with |- _ = Some (_, (?l {_} _)%I) => l end in
Ralf Jung's avatar
Ralf Jung committed
542
    iAssumptionCore || fail "wp_cmpxchg: cannot find" l "↦ ?" in
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
543
  wp_pures;
544 545 546
  lazymatch goal with
  | |- envs_entails _ (wp ?s ?E ?e ?Q) =>
    first
Ralf Jung's avatar
Ralf Jung committed
547 548
      [reshape_expr e ltac:(fun K e' => eapply (tac_wp_cmpxchg _ _ _ _ _ _ K))
      |fail 1 "wp_cmpxchg: cannot find 'CmpXchg' in" e];
549 550 551
    [iSolveTC
    |solve_mapsto ()
    |pm_reflexivity
Ralf Jung's avatar
Ralf Jung committed
552
    |try solve_vals_cmpxchg_compare_safe
553 554
    |intros H1; wp_finish
    |intros H2; wp_finish]
555 556
  | |- envs_entails _ (twp ?E ?e ?Q) =>
    first
Ralf Jung's avatar
Ralf Jung committed
557 558
      [reshape_expr e ltac:(fun K e' => eapply (tac_twp_cmpxchg _ _ _ _ _ K))
      |fail 1 "wp_cmpxchg: cannot find 'CmpXchg' in" e];
559 560
    [solve_mapsto ()
    |pm_reflexivity
Ralf Jung's avatar
Ralf Jung committed
561
    |try solve_vals_cmpxchg_compare_safe
562 563
    |intros H1; wp_finish
    |intros H2; wp_finish]
Ralf Jung's avatar
Ralf Jung committed
564
  | _ => fail "wp_cmpxchg: not a 'wp'"
565 566
  end.

Ralf Jung's avatar
Ralf Jung committed
567
Tactic Notation "wp_cmpxchg_fail" :=
568 569
  let solve_mapsto _ :=
    let l := match goal with |- _ = Some (_, (?l {_} _)%I) => l end in
Ralf Jung's avatar
Ralf Jung committed
570
    iAssumptionCore || fail "wp_cmpxchg_fail: cannot find" l "↦ ?" in
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
571
  wp_pures;
572
  lazymatch goal with
573
  | |- envs_entails _ (wp ?s ?E ?e ?Q) =>
574
    first
Ralf Jung's avatar
Ralf Jung committed
575 576
      [reshape_expr e ltac:(fun K e' => eapply (tac_wp_cmpxchg_fail _ _ _ _ _ K))
      |fail 1 "wp_cmpxchg_fail: cannot find 'CmpXchg' in" e];
Ralf Jung's avatar
Ralf Jung committed
577
    [iSolveTC
578
    |solve_mapsto ()
579
    |try (simpl; congruence) (* value inequality *)
Ralf Jung's avatar
Ralf Jung committed
580
    |try solve_vals_cmpxchg_compare_safe
581
    |wp_finish]
582 583
  | |- envs_entails _ (twp ?s ?E ?e ?Q) =>
    first
Ralf Jung's avatar
Ralf Jung committed
584 585
      [reshape_expr e ltac:(fun K e' => eapply (tac_twp_cmpxchg_fail _ _ _ _ K))
      |fail 1 "wp_cmpxchg_fail: cannot find 'CmpXchg' in" e];
586
    [solve_mapsto ()
587
    |try (simpl; congruence) (* value inequality *)
Ralf Jung's avatar
Ralf Jung committed
588
    |try solve_vals_cmpxchg_compare_safe
589
    |wp_finish]
Ralf Jung's avatar
Ralf Jung committed
590
  | _ => fail "wp_cmpxchg_fail: not a 'wp'"
Robbert Krebbers's avatar
Robbert Krebbers committed
591 592
  end.

Ralf Jung's avatar
Ralf Jung committed
593
Tactic Notation "wp_cmpxchg_suc" :=
594 595
  let solve_mapsto _ :=
    let l := match goal with |- _ = Some (_, (?l {_} _)%I) => l end in
Ralf Jung's avatar
Ralf Jung committed
596
    iAssumptionCore || fail "wp_cmpxchg_suc: cannot find" l "↦ ?" in
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
597
  wp_pures;
598
  lazymatch goal with
599
  | |- envs_entails _ (wp ?s ?E ?e ?Q) =>
600
    first
Ralf Jung's avatar
Ralf Jung committed
601 602
      [reshape_expr e ltac:(fun K e' => eapply (tac_wp_cmpxchg_suc _ _ _ _ _ _ K))
      |fail 1 "wp_cmpxchg_suc: cannot find 'CmpXchg' in" e];
Ralf Jung's avatar
Ralf Jung committed
603
    [iSolveTC
604
    |solve_mapsto ()
605
    |pm_reflexivity
606
    |try (simpl; congruence) (* value equality *)
Ralf Jung's avatar
Ralf Jung committed
607
    |try solve_vals_cmpxchg_compare_safe
608
    |wp_finish]
Robbert Krebbers's avatar
Robbert Krebbers committed
609
  | |- envs_entails _ (twp ?s ?E ?e ?Q) =>
610
    first
Ralf Jung's avatar
Ralf Jung committed
611 612
      [reshape_expr e ltac:(fun K e' => eapply (tac_twp_cmpxchg_suc _ _ _ _ _ K))
      |fail 1 "wp_cmpxchg_suc: cannot find 'CmpXchg' in" e];
613
    [solve_mapsto ()
614
    |pm_reflexivity
615
    |try (simpl; congruence) (* value equality *)
Ralf Jung's avatar
Ralf Jung committed
616
    |try solve_vals_cmpxchg_compare_safe
617
    |wp_finish]
Ralf Jung's avatar
Ralf Jung committed
618
  | _ => fail "wp_cmpxchg_suc: not a 'wp'"
Robbert Krebbers's avatar
Robbert Krebbers committed
619
  end.
620 621

Tactic Notation "wp_faa" :=
622 623
  let solve_mapsto _ :=
    let l := match goal with |- _ = Some (_, (?l {_} _)%I) => l end in
Ralf Jung's avatar
Ralf Jung committed
624
    iAssumptionCore || fail "wp_faa: cannot find" l "↦ ?" in
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
625
  wp_pures;
626
  lazymatch goal with
Ralf Jung's avatar
Ralf Jung committed
627
  | |- envs_entails _ (wp ?s ?E ?e ?Q) =>
628
    first
629
      [reshape_expr e ltac:(fun K e' => eapply (tac_wp_faa _ _ _ _ _ _ K))
630
      |fail 1 "wp_faa: cannot find 'FAA' in" e];
Ralf Jung's avatar