proofmode.v 6.07 KB
Newer Older
Robbert Krebbers's avatar
Robbert Krebbers committed
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
From iris.proofmode Require Import coq_tactics.
From iris.proofmode Require Export weakestpre.
From iris.heap_lang Require Export wp_tactics heap.
Import uPred.

Ltac strip_later ::= iNext.

Section heap.
Context {Σ : gFunctors} `{heapG Σ}.
Implicit Types N : namespace.
Implicit Types P Q : iPropG heap_lang Σ.
Implicit Types Φ : val  iPropG heap_lang Σ.
Implicit Types Δ : envs (iResR heap_lang (globalF Σ)).

Global Instance sep_destruct_mapsto l q v :
  SepDestruct false (l {q} v) (l {q/2} v) (l {q/2} v).
Proof. by rewrite /SepDestruct heap_mapsto_op_split. Qed.

Lemma tac_wp_alloc Δ Δ' N E j e v Φ :
  to_val e = Some v  
  Δ  heap_ctx N  nclose N  E 
  StripLaterEnvs Δ Δ' 
  ( l,  Δ'',
    envs_app false (Esnoc Enil j (l  v)) Δ' = Some Δ''  Δ''  Φ (LocV l)) 
  Δ  WP Alloc e @ E {{ Φ }}.
Proof.
  intros ???? HΔ; eapply wp_alloc; eauto.
  rewrite strip_later_env_sound; apply later_mono, forall_intro=> l.
  destruct (HΔ l) as (Δ''&?&HΔ'). rewrite envs_app_sound //; simpl.
  by rewrite right_id HΔ'.
Qed.

Lemma tac_wp_load Δ Δ' N E i l q v Φ :
  Δ  heap_ctx N  nclose N  E 
  StripLaterEnvs Δ Δ' 
  envs_lookup i Δ' = Some (false, l {q} v)%I 
  Δ'  Φ v 
  Δ  WP Load (Loc l) @ E {{ Φ }}.
Proof.
  intros. eapply wp_load; eauto.
  rewrite strip_later_env_sound -later_sep envs_lookup_split //; simpl.
  by apply later_mono, sep_mono_r, wand_mono.
Qed.

Lemma tac_wp_store Δ Δ' Δ'' N E i l v e v' Φ :
  to_val e = Some v' 
  Δ  heap_ctx N  nclose N  E 
  StripLaterEnvs Δ Δ' 
  envs_lookup i Δ' = Some (false, l  v)%I 
  envs_simple_replace i false (Esnoc Enil i (l  v')) Δ' = Some Δ'' 
  Δ''  Φ (LitV LitUnit)  Δ  WP Store (Loc l) e @ E {{ Φ }}.
Proof.
  intros. eapply wp_store; eauto.
  rewrite strip_later_env_sound -later_sep envs_simple_replace_sound //; simpl.
  rewrite right_id. by apply later_mono, sep_mono_r, wand_mono.
Qed.

Lemma tac_wp_cas_fail Δ Δ' N E i l q v e1 v1 e2 v2 Φ :
  to_val e1 = Some v1  to_val e2 = Some v2 
  Δ  heap_ctx N  nclose N  E 
  StripLaterEnvs Δ Δ' 
  envs_lookup i Δ' = Some (false, l {q} v)%I  v  v1 
  Δ'  Φ (LitV (LitBool false)) 
  Δ  WP CAS (Loc l) e1 e2 @ E {{ Φ }}.
Proof.
  intros. eapply wp_cas_fail; eauto.
  rewrite strip_later_env_sound -later_sep envs_lookup_split //; simpl.
  by apply later_mono, sep_mono_r, wand_mono.
Qed.

Lemma tac_wp_cas_suc Δ Δ' Δ'' N E i l e1 v1 e2 v2 Φ :
  to_val e1 = Some v1  to_val e2 = Some v2 
  Δ  heap_ctx N  nclose N  E 
  StripLaterEnvs Δ Δ' 
  envs_lookup i Δ' = Some (false, l  v1)%I 
  envs_simple_replace i false (Esnoc Enil i (l  v2)) Δ' = Some Δ'' 
  Δ''  Φ (LitV (LitBool true))  Δ  WP CAS (Loc l) e1 e2 @ E {{ Φ }}.
Proof.
  intros. eapply wp_cas_suc; eauto.
  rewrite strip_later_env_sound -later_sep envs_simple_replace_sound //; simpl.
  rewrite right_id. by apply later_mono, sep_mono_r, wand_mono.
Qed.
End heap.

Tactic Notation "wp_apply" open_constr(lem) :=
  match goal with
  | |- _  wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
    wp_bind K; iApply lem; try iNext)
  end.

Tactic Notation "wp_apply" open_constr(lem) constr(Hs) :=
  match goal with
  | |- _  wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
    wp_bind K; iApply lem Hs; try iNext)
  end.

Tactic Notation "wp_alloc" ident(l) "as" constr(H) :=
  match goal with
  | |- _  wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
    match eval hnf in e' with
    | Alloc ?e =>
       wp_bind K; eapply tac_wp_alloc with _ _ H _;
         [wp_done || fail 2 "wp_alloc:" e "not a value"
         |iAssumption || fail 2 "wp_alloc: cannot find heap_ctx"
         |done || eauto with ndisj
         |apply _
         |intros l; eexists; split;
           [env_cbv; reflexivity || fail 2 "wp_alloc:" H "not fresh"
           |wp_finish]]
    end)
  end.
Tactic Notation "wp_alloc" ident(l) := let H := iFresh in wp_alloc l as H.

Tactic Notation "wp_load" :=
  match goal with
  | |- _  wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
    match eval hnf in e' with
    | Load (Loc ?l) =>
       wp_bind K; eapply tac_wp_load;
         [iAssumption || fail 2 "wp_load: cannot find heap_ctx"
         |done || eauto with ndisj
         |apply _
         |iAssumptionCore || fail 2 "wp_cas_fail: cannot find" l "↦ ?"
         |wp_finish]
    end)
  end.

Tactic Notation "wp_store" :=
  match goal with
  | |- _  wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
    match eval hnf in e' with
    | Store ?l ?e =>
       wp_bind K; eapply tac_wp_store;
         [wp_done || fail 2 "wp_store:" e "not a value"
         |iAssumption || fail 2 "wp_store: cannot find heap_ctx"
         |done || eauto with ndisj
         |apply _
         |iAssumptionCore || fail 2 "wp_store: cannot find" l "↦ ?"
         |env_cbv; reflexivity
         |wp_finish]
    end)
  end.

Tactic Notation "wp_cas_fail" :=
  match goal with
  | |- _  wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
    match eval hnf in e' with
    | CAS (Loc ?l) ?e1 ?e2 =>
       wp_bind K; eapply tac_wp_cas_fail;
         [wp_done || fail 2 "wp_cas_fail:" e1 "not a value"
         |wp_done || fail 2 "wp_cas_fail:" e2 "not a value"
         |iAssumption || fail 2 "wp_cas_fail: cannot find heap_ctx"
         |done || eauto with ndisj
         |apply _
         |iAssumptionCore || fail 2 "wp_cas_fail: cannot find" l "↦ ?"
         |try discriminate
         |wp_finish]
    end)
  end.

Tactic Notation "wp_cas_suc" :=
  match goal with
  | |- _  wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
    match eval hnf in e' with
    | CAS (Loc ?l) ?e1 ?e2 =>
       wp_bind K; eapply tac_wp_cas_suc;
         [wp_done || fail 2 "wp_cas_suc:" e1 "not a value"
         |wp_done || fail 2 "wp_cas_suc:" e1 "not a value"
         |iAssumption || fail 2 "wp_cas_suc: cannot find heap_ctx"
         |done || eauto with ndisj
         |apply _
         |iAssumptionCore || fail 2 "wp_cas_suc: cannot find" l "↦ ?"
         |env_cbv; reflexivity
         |wp_finish]
    end)
  end.