1(*
2 * Copyright 2014, NICTA
3 *
4 * This software may be distributed and modified according to the terms of
5 * the GNU General Public License version 2. Note that NO WARRANTY is provided.
6 * See "LICENSE_GPLv2.txt" for details.
7 *
8 * @TAG(NICTA_GPL)
9 *)
10
11theory Sep_Tactic_Examples
12imports
13  "SepDSpec.Sep_Tactic_Helper"
14  KHeap_DP
15begin
16
17
18(* Thesis : Automated Tactics for Seperation Logic *)
19
20(* seperation logic *)
21
22(* after we show that addition and disjointedness on our heap obeys certain laws, we get a seperation algebra *)
23
24(* connectives *)
25
26term "P \<and>* Q"
27
28term "P \<longrightarrow>* Q"
29
30lemma frame_rule:
31  "\<And>R. \<lbrace>P\<rbrace> f \<lbrace>\<lambda>_. Q\<rbrace> \<Longrightarrow> \<lbrace>P \<and>* R\<rbrace> f \<lbrace>\<lambda>_. Q \<and>* R\<rbrace>"
32  oops
33
34thm swap_cap_wp[no_vars]
35
36lemma
37 "\<lbrace><dest \<mapsto>c - \<and>* src \<mapsto>c cap \<and>* R>\<rbrace>
38    move_cap cap' src dest
39  \<lbrace>\<lambda>_. <dest \<mapsto>c cap'  \<and>* src \<mapsto>c NullCap \<and>* R>\<rbrace>"
40  apply (simp add: move_cap_def)
41  apply (wp swap_parents_wp set_cap_wp) (* set_cap doesn't apply *)
42thm set_cap_wp[no_vars]
43   apply (rule hoare_strengthen_post)
44    apply (wp set_cap_wp)
45   apply (clarsimp simp: sep_conj_ac )
46oops
47
48
49(* tactics we had pre-thesis *)
50
51lemma "(A \<and>* B \<and>* C \<and>* D) s  \<Longrightarrow>  (A \<and>* B \<and>* C \<and>* D) s"
52  apply (sep_select 4)
53  apply (sep_select_asm 3)
54  apply (sep_select 2)
55  apply (sep_cancel)
56  apply (sep_cancel)
57  apply (sep_cancel)
58done
59
60(* forward reasoning *)
61
62
63lemma example_drule:
64  "(ptr \<mapsto>o obj) s
65  \<Longrightarrow> (ptr \<mapsto>S obj \<and>* ptr \<mapsto>f obj) s"
66  by (metis sep_conj_commute sep_map_o_decomp)
67
68lemma sep_drule_example:
69  "(ptr \<mapsto>o obj \<and>* A \<and>* B ) s
70  \<Longrightarrow> (A \<and>* B \<and>* ptr \<mapsto>f obj \<and>* ptr \<mapsto>S obj) s"
71  apply (sep_drule  example_drule)
72  apply (sep_solve)
73done
74
75(* backwards reasoning *)
76
77lemma example_rule:
78  "(ptr \<mapsto>f obj \<and>* ptr \<mapsto>S obj) s
79  \<Longrightarrow> (ptr \<mapsto>o obj) s"
80  by (metis sep_map_o_decomp)
81
82lemma sep_rule_example: "(ptr \<mapsto>f obj \<and>* A \<and>* B \<and>* ptr \<mapsto>S obj ) s \<Longrightarrow> (ptr \<mapsto>o obj \<and>* A \<and>* B) s"
83  apply (sep_rule example_rule)
84  apply (sep_solve)
85done
86
87
88
89(* the state of proving before new stuff *)
90
91lemma swap_cap_wp_old:
92  "\<lbrace><dest \<mapsto>c cap \<and>*  src \<mapsto>c cap' \<and>* R>\<rbrace>
93    swap_cap cap' src cap dest
94   \<lbrace>\<lambda>_.<dest \<mapsto>c cap' \<and>* src \<mapsto>c cap \<and>* R>\<rbrace>"
95  apply (clarsimp simp add: swap_cap_def)
96  apply (wp swap_parents_wp set_cap_wp)
97  apply (rule hoare_chain)
98    apply (rule set_cap_wp)
99    apply (sep_solve)+
100done
101
102
103lemma move_cap_wp_old:
104 "\<lbrace><dest \<mapsto>c - \<and>* src \<mapsto>c cap \<and>* R>\<rbrace>
105    move_cap cap' src dest
106  \<lbrace>\<lambda>_. <dest \<mapsto>c cap'  \<and>* src \<mapsto>c NullCap \<and>* R>\<rbrace>"
107  including no_pre
108  apply (simp add: move_cap_def)
109  apply (wp swap_parents_wp)
110   apply (rule hoare_strengthen_post)
111    apply (rule set_cap_wp)
112   apply (sep_select 2)
113   apply (sep_solve)
114  apply (rule hoare_chain)
115    apply (rule insert_cap_orphan_wp)
116   apply (sep_solve)
117  apply (sep_solve)
118done
119
120lemma invoke_cnode_rotate2_wp_old:
121  "(dest) \<noteq> (rnd) \<Longrightarrow>
122  \<lbrace><dest \<mapsto>c cap1 \<and>* src \<mapsto>c cap2 \<and>*
123    rnd \<mapsto>c - \<and>* R>\<rbrace>
124     invoke_cnode (RotateCall cap1 cap2 dest src rnd)
125  \<lbrace>\<lambda>_. <dest \<mapsto>c NullCap \<and>* src \<mapsto>c cap1 \<and>*
126    rnd \<mapsto>c cap2 \<and>* R>\<rbrace>"
127  including no_pre
128  apply (clarsimp simp: invoke_cnode_def)
129  apply (wp)
130   apply (rule hoare_strengthen_post)
131    apply (rule move_cap_wp)
132   apply (sep_solve )
133  apply (rule hoare_chain)
134    apply (rule move_cap_wp)
135   apply (sep_select_asm 2, sep_select_asm 3)
136   apply (sep_solve)
137  apply (sep_solve)
138done
139
140(* new sep_select/asm *)
141
142lemma "(A \<and>* B \<and>* C \<and>* D) s  \<Longrightarrow>  (A \<and>* B \<and>* C \<and>* D) s"
143  apply (sep_select 4 3 2 1)
144  apply (sep_select_asm 4 3 2 1)
145  apply (sep_select_asm 2 4)
146oops
147
148
149(* sep_select_pre/post *)
150
151lemma "\<lbrace>A \<and>* B \<and>* C \<and>* D\<rbrace> f \<lbrace>\<lambda>_. A \<and>* B \<and>* C \<and>* D\<rbrace>"
152  apply (sep_select_pre 4 1 2 3)
153  apply (sep_select_post 3 4 2 1)
154  apply (sep_select_post 3 4)
155oops
156
157(* can be made to work for arbitrary monads *)
158
159lemma "\<lbrace>A \<and>* B \<and>* C \<and>* D\<rbrace> f \<lbrace>\<lambda>_. A \<and>* B \<and>* C \<and>* D\<rbrace>, \<lbrace>E\<rbrace>"
160  apply (sep_select_pre 4 1 2 3)
161  apply (sep_select_post 3 4 2 1)
162  apply (sep_select_post 3 4)
163oops
164
165lemma "\<lbrace>A \<and>* B \<and>* C \<and>* D\<rbrace> f \<lbrace>\<lambda>_. A \<and>* B \<and>* C \<and>* D\<rbrace>, -"
166  apply (sep_select_pre 4 1 2 3)
167  apply (sep_select_post 3 4 2 1)
168  apply (sep_select_post 3 4)
169oops
170
171lemma "(P \<and>* (P \<longrightarrow>* Q)) s \<Longrightarrow> Q s"
172  apply (sep_mp, assumption )
173  done
174
175lemma "P s \<Longrightarrow> (Q \<longrightarrow>* (P \<and>* Q)) s"
176  apply (erule sep_curry[rotated])
177  apply (assumption)
178  done
179
180thm sep_mp[no_vars] sep_curry[rotated, no_vars]
181
182
183(* wp tactic testing *)
184
185
186(* sep_wand approach *)
187
188method_setup debug = {*
189  Attrib.thms >> (fn _ => fn ctxt =>
190   let
191     val wp_pre_tac = SELECT_GOAL (Method.NO_CONTEXT_TACTIC ctxt
192                      (Method_Closure.apply_method ctxt @{method wp_pre} [] [] [] ctxt []))
193   in
194     SIMPLE_METHOD' (CHANGED o wp_pre_tac)
195   end
196)
197*}
198
199lemma move_cap_wp2:
200 "\<lbrace><dest \<mapsto>c - \<and>* src \<mapsto>c cap \<and>* R>\<rbrace>
201    move_cap cap' src dest
202  \<lbrace>\<lambda>_. <dest \<mapsto>c cap'  \<and>* src \<mapsto>c NullCap \<and>* R>\<rbrace>"
203  apply (simp add: move_cap_def)
204  apply (sep_wp set_cap_wp swap_parents_wp insert_cap_orphan_wp)+
205  apply (sep_solve)
206  done
207
208lemma swap_cap_wp2:
209  "\<lbrace><dest \<mapsto>c cap \<and>*  src \<mapsto>c cap' \<and>* R>\<rbrace>
210    swap_cap cap' src cap dest
211   \<lbrace>\<lambda>_.<dest \<mapsto>c cap' \<and>* src \<mapsto>c cap \<and>* R>\<rbrace>"
212  apply (clarsimp simp: swap_cap_def)
213  apply (sep_wp swap_parents_wp set_cap_wp)+
214  apply (sep_solve)
215  done
216
217lemma invoke_cnode_rotate2_wp:
218  "(dest) \<noteq> (rnd) \<Longrightarrow>
219  \<lbrace><dest \<mapsto>c cap1 \<and>* src \<mapsto>c cap2 \<and>*
220    rnd \<mapsto>c - \<and>* R>\<rbrace>
221     invoke_cnode (RotateCall cap1 cap2 dest src rnd)
222  \<lbrace>\<lambda>_. <dest \<mapsto>c NullCap \<and>* src \<mapsto>c cap1 \<and>*
223    rnd \<mapsto>c cap2 \<and>* R>\<rbrace>"
224  apply (clarsimp simp: invoke_cnode_def)
225  apply (sep_wp move_cap_wp)+
226  apply (sep_solve)
227  done
228
229
230(* sep_drule/rule *)
231
232lemma sep_rule_example2:
233 "\<lbrakk>(ptr \<mapsto>o obj) s; finite (dom (object_slots obj))\<rbrakk> \<Longrightarrow>
234   (ptr \<mapsto>E obj \<and>* ptr \<mapsto>f obj \<and>* (\<And>* slot\<in>dom (object_slots obj). (ptr, slot) \<mapsto>s obj)) s"
235  apply (subst (asm) sep_map_o_decomp)
236  apply (subst (asm) sep_map_S_decomp, simp+)
237  apply sep_solve
238  done
239
240lemma sep_drule_example2:
241 "\<lbrakk>(ptr \<mapsto>f obj \<and>* (\<And>* slot\<in>dom (object_slots obj). (ptr, slot) \<mapsto>s obj) \<and>* ptr \<mapsto>E obj) s;
242   finite (dom (object_slots obj))\<rbrakk>
243    \<Longrightarrow>
244  (ptr \<mapsto>o obj) s"
245  by (metis sep_map_S_decomp sep_map_o_decomp)
246
247(* sep_curry *)
248
249lemma sep_drule_example_lemma:
250  "\<lbrakk>(H \<and>* Z \<and>* J \<and>* L \<and>* Y \<and>* ptr \<mapsto>f obj \<and>* A \<and>* B \<and>*
251    (\<And>* slot\<in>dom (object_slots obj). (ptr, slot) \<mapsto>s obj) \<and>* D \<and>* G \<and>* E \<and>* F \<and>* ptr \<mapsto>E obj ) s;
252    finite (dom (object_slots obj))\<rbrakk>
253  \<Longrightarrow>
254   (D \<and>* G \<and>* E \<and>* F  \<and>* ptr \<mapsto>o obj \<and>* H \<and>* Z \<and>* J \<and>* L \<and>* Y \<and>* A \<and>* B) s"
255  apply (sep_drule sep_drule_example2)
256   apply assumption
257  apply sep_solve
258  done
259
260
261(* sep_back *)
262
263
264lemma sep_rule_example_lemma:
265 "\<lbrakk>(H \<and>* Z \<and>* J \<and>* L \<and>* Y \<and>* ptr \<mapsto>o obj \<and>* A \<and>* B \<and>* D \<and>* G \<and>* E \<and>* F ) s;
266  finite (dom (object_slots obj))\<rbrakk> \<Longrightarrow>
267  (D \<and>* G \<and>* E \<and>* F  \<and>* ptr \<mapsto>f obj \<and>* H \<and>* Z \<and>* J \<and>* L \<and>* Y \<and>* ptr \<mapsto>E obj \<and>*
268   A \<and>* B \<and>* (\<And>* slot\<in>dom (object_slots obj). (ptr, slot) \<mapsto>s obj)) s"
269  apply (sep_rule sep_rule_example2)
270   apply sep_solve
271  apply assumption
272  done
273
274
275(* works even with multiple conjuncts in assumptions and conclusions *)
276lemma sep_rule_double_conjunct_example:
277  "\<lbrakk>((obj_id, slot) \<mapsto>c cap \<and>* obj_id \<mapsto>f obj) s;
278    object_slots obj slot = Some cap\<rbrakk>
279  \<Longrightarrow> ((obj_id, slot) \<mapsto>s obj \<and>* obj_id \<mapsto>f obj) s"
280  apply (sep_drule sep_map_s_sep_map_c)
281   apply assumption
282  apply (sep_cancel)+
283  done
284
285lemma sep_rule_double_conjunct_lemma:
286  "\<lbrakk>(H \<and>* Z \<and>* J \<and>* L \<and>* Y \<and>* obj_id \<mapsto>f obj \<and>* A \<and>* B \<and>* D \<and>* G \<and>* E \<and>* F \<and>* (obj_id, slot) \<mapsto>c cap ) s;
287    object_slots obj slot = Some cap\<rbrakk> \<Longrightarrow>
288   (D \<and>* G \<and>* E \<and>* F  \<and>*(obj_id, slot) \<mapsto>s obj \<and>* H \<and>* Z \<and>* J \<and>* L \<and>* Y \<and>* A \<and>* B \<and>*  obj_id \<mapsto>f obj) s"
289  apply (sep_rule sep_rule_double_conjunct_example)
290   apply sep_solve
291  apply assumption
292  done
293
294(* side-conditions*)
295
296
297lemma sep_drule_side_condition_lemma:
298 "\<lbrakk>(H \<and>* Z \<and>* J \<and>* L \<and>* Y \<and>* obj_id \<mapsto>f obj \<and>* A \<and>* B \<and>* D \<and>* G \<and>* E \<and>* F \<and>* (obj_id, slot) \<mapsto>c cap ) s;
299    object_slots obj slot = Some cap\<rbrakk> \<Longrightarrow>
300   (D \<and>* G \<and>* E \<and>* F  \<and>*(obj_id, slot) \<mapsto>s obj \<and>* H \<and>* Z \<and>* J \<and>* L \<and>* Y \<and>* A \<and>* B \<and>*  obj_id \<mapsto>f obj) s"
301  apply (sep_drule sep_rule_double_conjunct_example, assumption)
302  apply (sep_solve)
303  done
304
305schematic_goal "(P \<and>* ?A) s \<Longrightarrow> (A \<and>* B \<and>* P) s"
306  apply (sep_solve)
307  done
308
309
310end
311