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