1(* 2 * 3 * Copyright 2017, Data61, CSIRO 4 * 5 * This software may be distributed and modified according to the terms of 6 * the GNU General Public License version 2. Note that NO WARRANTY is provided. 7 * See "LICENSE_GPLv2.txt" for details. 8 * 9 * @TAG(DATA61_GPL) 10 *) 11 12(* 13 Test proofs for corres methods. Builds on AInvs image. 14*) 15 16theory Corres_Test 17imports "Refine.VSpace_R" "Lib.Corres_Method" 18begin 19 20chapter \<open>The Corres Method\<close> 21 22section \<open>Introduction\<close> 23 24text \<open>The @{method corres} method tries to do for corres-style refinement proofs what 25@{method wp} did for hoare logic proofs. The intention is to automate the application 26of corres calculational rules, so that the bulk of the manual proof is now handling 27a verification condition. In general refinement proofs are difficult to automate, so here we 28exploit the fact that in l4v the abstract and executable specifications tend to be structurally 29similar. Corres proofs are based on the @{const corres_underlying} constant, which takes a number 30of parameters that allow it to be specialized for different flavours of refinement. 31 32A corres statement has the following form: @{term "corres_underlying sr nf nf' r P P' f f'"}, where 33@{term sr} is a state-relation, @{term nf} and @{term nf'} refer to whether or not the left and 34right hand functions may fail, @{term r} is a return value relation between the functions, @{term P} 35and @{term P'} are preconditions for the functions @{term f} and @{term f'} respectively. Informally 36the statement says that: under the given preconditions, for every execution of @{term f'} there exists 37an execution of @{term f} that is related by the given state relation @{term sr} and return-value 38relation @{term r}. 39 40If the left and right side of a corres statement share similar structure, we can "unzip" the function 41into one corres obligation for each atomic function. This is done through the application of 42 @{thm corres_split}. 43\<close> 44 45thm corres_split[no_vars] 46 47text \<open>Briefly this states that: given a corres goal proving refinement between @{term "a >>= b"} and 48 @{term "c >>= d"}, we can decompose this into a proof showing refinement between @{term a} and 49@{term c}, and between @{term a} and @{term c}. Additionally @{term a} and @{term c} must establish 50appropriate postconditions to satisfy the obligations of proving refinement between @{term b} and @{term d}. 51 52The first subgoal that is produced has an important characteristic: the preconditions for each 53side may only discuss the return value of its respective side. This means that rules such as 54@{term "corres_underlying sr nf nf' r (\<lambda>s. x = x') (\<lambda>_. True) (f x) (f' x')"} will not apply to a goal 55 if @{term x} and @{term x'} are variables generated by applying @{thm corres_split} (i.e. the 56return values of functions). 57 58This means that any such conditions must instead be phrased as an assumption to the rule, and our rule must be 59rephrased as follows: 60 @{term "x = x' \<Longrightarrow> corres_underlying sr nf nf' r (\<lambda>_. True) (\<lambda>_. True) (f x) (f' x')"}. 61The result is that we must solve @{term "x = x'"} immediately after applying our rule. While this 62is not a major concern for a manual proof, it proves to be a significant obstacle if we're trying 63to focus on automating the "corres" part of the refinement. 64\<close> 65 66section \<open>corres_underlyingK and corres_rv\<close> 67 68text \<open>To remedy this situation, we augment the @{const corres_underlying} definition to include 69yet another flag: a single boolean. This new constant: @{const corres_underlyingK}, 70will form the basis of the calculus for our corres method.\<close> 71 72thm corres_underlyingK_def[no_vars] 73 74text \<open>The boolean in @{const corres_underlyingK} can be thought of as a stateless precondition. It 75is used to propagate additional proof obligations for rules that either do not need to discuss 76either the left or right hand state, or must discuss bound variables from both sides.\<close> 77 78thm corresK_split[no_vars] 79 80text \<open>In this split rule for @{const corres_underlyingK} we see that the additional precondition @{term F'} 81may discuss both @{term rv} and @{term rv'}. To show that this condition is satisified, however, 82we can't use hoare logic and instead need a new definition: @{const corres_rv}.\<close> 83 84thm corres_rv_def_I_know_what_I'm_doing[no_vars] 85 86text \<open>This is a weaker form of @{const corres_underlying} that is only interested in the return value 87of the functions. In essence, it states the given functions will establish @{term Q} after executing, 88assuming the given return-value relation @{term r} holds, along with the given stateless precondition 89@{term F} and left/right preconditions @{term P} and @{term P'}. 90 91The assumption in general is that corres_rv rules should never be written, instead corres_rv obligations 92should be propagated into either the stateless precondition (@{term F} from @{term corres_underlyingK}), 93the left precondition (@{term P}) or the right precondition @{term P'}. This is implicitly handled 94by @{method corres_rv} (called from @{method corres}) by applying one of the following rules to each conjunct:\<close> 95 96thm corres_rv_defer 97thm corres_rv_wp_left 98thm corres_rv_wp_right 99 100text \<open>If none of these rules can be safely applied, then @{method corres_rv} will leave the 101 obligation untouched. The user can manually apply one of them if desired, but this is liable to 102 create unsolvable proof obligations. In the worst case, the user may manually solve the goal in-place.\<close> 103 104thm corres_rv_proveT[no_vars] 105 106section \<open>The corres method\<close> 107 108text \<open>The core algorithm of the corres method is simple: 109 1) start by applying any necessary weakening rules to ensure the goal has schematic preconditions 110 2) apply a known @{thm corres} or @{thm corresK} rule (see next section) 111 3) if unsuccessful, apply a split rule (i.e. @{thm corresK_split}) and go to 2 112 113Importantly, @{method corres} will not split a goal if it ultimately is not able to apply at least 114one @{thm corres} or @{thm corresK} rule. 115\<close> 116 117subsection \<open>The corres and corresK named_theorems\<close> 118 119text \<open>To address the fact that existing refinement rules are phrased as @{const corres_underlying} 120and not @{const corres_underlyingK} there are two different named_theorems that are used for different 121kind of rules @{thm corres} and @{thm corresK}. A @{thm corres} rule is understood to be phrased 122with @{const corres_underlying} and may have additional assumptions. These assumptions will be 123propagated through the additional @{term F} flag in @{const corres_underlyingK}, rather than presented 124as proof obligations immediately. A @{thm corresK} rule is understood to be phrased with 125@{const corres_underlyingK}, and is meant for calculational rules which may have proper assumptions that 126should not be propagated. 127\<close> 128thm corresK 129thm corres 130 131subsection \<open>The corresc method\<close> 132 133text \<open>Similar to @{method wpc}, @{method corresc} can handle case statements in @{const corres_underlyingK} 134proof goals. Importantly, however, it is split into two sub-methods @{method corresc_left} and 135@{method corresc_right}, which perform case-splitting on each side respectively. The combined method 136@{method corresc}, however, attempts to discharge the contradictions that arise from the quadratic 137blowup of a case analysis on both the left and right sides.\<close> 138 139subsection \<open>corres_concrete_r, corres_concrete_rE\<close> 140 141text \<open>Some @{thm corresK} rules should only be applied if certain variables are concrete 142(i.e. not schematic) in the goal. These are classified separately with the named_theorems 143@{thm corres_concrete_r} and @{thm corres_concrete_rER}. The first 144indicates that the return value relation of the goal must be concrete, the second indicates that 145only the left side of the error relation must be concrete.\<close> 146 147thm corres_concrete_r 148thm corres_concrete_rER 149 150subsection \<open>The corres_search method\<close> 151 152text \<open>The purpose of @{method corres_search} is to address cases where there is non-trivial control flow. 153In particular: in the case where there is an "if" statement or either side needs to be symbolically 154executed. The core idea is that corres_search should be provided with a "search" rule that acts 155as an anchoring point. Symbolic execution and control flow is decomposed until either the given 156rule is successfully applied or all search branches are exhausted.\<close> 157 158subsubsection \<open>Symbolic Execution\<close> 159 160text \<open>Symbolic execution is handled by two named theorems: 161 @{thm corres_symb_exec_ls} and @{thm corres_symb_exec_rs}, which perform symbolic execution on 162the left and right hand sides of a corres goal.\<close> 163 164thm corres_symb_exec_ls 165thm corres_symb_exec_rs 166 167text \<open>A function may be symbolically executed if it does not modify the state, i.e. its only purpose 168is to compute some value and return it. After being symbolically executed, 169this value can only be discussed by the precondition of the associated side or the stateless 170precondition of corresK. The resulting @{const corres_rv} goal has @{const corres_noop} as the 171function on the alternate side. This gives @{method corres_rv} a hint that the resulting obligation 172should be aggressively re-written into a hoare triple over @{term m} if it can't be propagated 173back statelessly safely. 174\<close> 175 176 177section \<open>Demo\<close> 178 179 180context begin interpretation Arch . 181 182(* VSpace_R *) 183 184 185lemmas load_hw_asid_corres_args[corres] = 186 load_hw_asid_corres[@lift_corres_args] 187 188lemmas invalidate_asid_corres_args[corres] = 189 invalidate_asid_corres[@lift_corres_args] 190 191lemmas invalidate_hw_asid_entry_corres_args[corres] = 192 invalidate_hw_asid_entry_corres[@lift_corres_args] 193 194lemma invalidate_asid_entry_corres: 195 "corres dc (valid_vspace_objs and valid_asid_map 196 and K (asid \<le> mask asid_bits \<and> asid \<noteq> 0) 197 and vspace_at_asid asid pd and valid_vs_lookup 198 and unique_table_refs o caps_of_state 199 and valid_global_objs and valid_arch_state 200 and pspace_aligned and pspace_distinct) 201 (pspace_aligned' and pspace_distinct' and no_0_obj') 202 (invalidate_asid_entry asid) (invalidateASIDEntry asid)" 203 apply (simp add: invalidate_asid_entry_def invalidateASIDEntry_def) 204 apply_debug (trace) (* apply_trace between steps *) 205 (tags "corres") (* break at breakpoints labelled "corres" *) 206 corres (* weaken precondition *) 207 continue (* split *) 208 continue (* solve load_hw_asid *) 209 continue (* split *) 210 continue (* apply corres_when *) 211 continue (* trivial simplification *) 212 continue (* invalidate _hw_asid_entry *) 213 finish (* invalidate_asid *) 214 215 apply (corressimp wp: load_hw_asid_wp)+ 216 apply clarsimp 217 apply (fastforce simp: pd_at_asid_uniq) 218 done 219 220 221crunch typ_at'[wp]: invalidateASIDEntry, flushSpace "typ_at' T t" 222crunch ksCurThread[wp]: invalidateASIDEntry, flushSpace "\<lambda>s. P (ksCurThread s)" 223crunch obj_at'[wp]: invalidateASIDEntry, flushSpace "obj_at' P p" 224 225lemmas flush_space_corres_args[corres] = 226 flush_space_corres[@lift_corres_args] 227 228lemmas invalidate_asid_entry_corres_args[corres] = 229 invalidate_asid_entry_corres[@lift_corres_args] 230 231 232lemma corres_inst_eq_ext: 233 "(\<And>x. corres_inst_eq (f x) (f' x)) \<Longrightarrow> corres_inst_eq f f'" 234 by (auto simp add: corres_inst_eq_def) 235 236lemma delete_asid_corresb: 237 notes [corres] = corres_gets_asid gct_corres set_asid_pool_corres and 238 [@lift_corres_args, corres] = get_asid_pool_corres_inv' 239 invalidate_asid_entry_corres 240 set_vm_root_corres 241 notes [wp] = set_asid_pool_asid_map_unmap set_asid_pool_vs_lookup_unmap' 242 set_asid_pool_vspace_objs_unmap' 243 invalidate_asid_entry_invalidates 244 getASID_wp 245 shows 246 "corres dc 247 (invs and valid_etcbs and K (asid \<le> mask asid_bits \<and> asid \<noteq> 0)) 248 (pspace_aligned' and pspace_distinct' and no_0_obj' 249 and valid_arch_state' and cur_tcb') 250 (delete_asid asid pd) (deleteASID asid pd)" 251 apply (simp add: delete_asid_def deleteASID_def) 252 apply_debug (trace) (* apply_trace between steps *) 253 (tags "corres") (* break at breakpoints labelled "corres" *) 254 corres (* weaken precondition *) 255 continue (* split *) 256 continue (* gets rule *) 257 continue (* corresc *) 258 continue (* return rule *) 259 continue (* split *) 260 continue (* function application *) 261 continue (* liftM rule *) 262 continue (* get_asid_pool_corres_inv' *) 263 continue (* function application *) 264 continue (* function application *) 265 continue (* corresK_when *) 266 continue (* split *) 267 continue (* flush_space_corres *) 268 continue (* K_bind *) 269 continue (* K_bind *) 270 continue (* split *) 271 continue (* invalidate_asid_entry_corres *) 272 continue (* K_bind *) 273 continue (* return bind *) 274 continue (* K_bind *) 275 continue (* split *) 276 continue (* backtracking *) 277 continue (* split *) 278 continue (* function application *) 279 continue (* set_asid_pool_corres *) 280 continue (* K_bind *) 281 continue (* K_bind *) 282 continue (* split *) 283 continue (* gct_corres *) 284 continue (* set_vm_root_corres *) 285 finish (* backtracking? *) 286 apply (corressimp simp: mask_asid_low_bits_ucast_ucast 287 | fold cur_tcb_def | wps)+ 288 apply (frule arm_asid_table_related,clarsimp) 289 apply (rule conjI) 290 apply (intro impI allI) 291 apply (rule conjI) 292 apply (safe; assumption?) 293 apply (rule ext) 294 apply (fastforce simp: inv_def dest: ucast_ucast_eq) 295 apply (rule context_conjI) 296 apply (fastforce simp: o_def dest: valid_asid_tableD invs_valid_asid_table) 297 apply (intro allI impI) 298 apply (subgoal_tac "vspace_at_asid asid pd s") 299 prefer 2 300 apply (simp add: vspace_at_asid_def) 301 apply (rule vs_lookupI) 302 apply (simp add: vs_asid_refs_def) 303 apply (rule image_eqI[OF refl]) 304 apply (rule graph_ofI) 305 apply fastforce 306 apply (rule r_into_rtrancl) 307 apply simp 308 apply (rule vs_lookup1I [OF _ _ refl], assumption) 309 apply (simp add: vs_refs_def) 310 apply (rule image_eqI[rotated], erule graph_ofI) 311 apply (simp add: mask_asid_low_bits_ucast_ucast) 312 prefer 2 313 apply (intro allI impI context_conjI; assumption?) 314 apply (rule aligned_distinct_relation_asid_pool_atI'; fastforce?) 315 apply (fastforce simp: o_def dest: valid_asid_tableD invs_valid_asid_table) 316 apply (simp add: cur_tcb'_def) 317 apply (safe; assumption?) 318 apply (erule ko_at_weakenE) 319 apply (clarsimp simp: graph_of_def) 320 apply (fastforce split: if_split_asm) 321 apply (frule invs_vspace_objs) 322 apply (drule (2) valid_vspace_objsD) 323 apply (erule ranE) 324 apply (fastforce split: if_split_asm) 325 apply (erule ko_at_weakenE) 326 apply (clarsimp simp: graph_of_def) 327 apply (fastforce split: if_split_asm) 328 done 329 330lemma cte_wp_at_ex: 331 "cte_wp_at (\<lambda>_. True) p s \<Longrightarrow> (\<exists>cap. cte_wp_at ((=) cap) p s)" 332 by (simp add: cte_wp_at_def) 333 334(* Sadly broken: 335lemma set_vm_root_for_flush_corres: 336 notes [corres] = gct_corres getSlotCap_corres 337 shows 338 "corres (=) 339 (cur_tcb and vspace_at_asid asid pd 340 and K (asid \<noteq> 0 \<and> asid \<le> mask asid_bits) 341 and valid_asid_map and valid_vs_lookup 342 and valid_vspace_objs and valid_global_objs 343 and unique_table_refs o caps_of_state 344 and valid_arch_state 345 and pspace_aligned and pspace_distinct) 346 (pspace_aligned' and pspace_distinct' and no_0_obj') 347 (set_vm_root_for_flush pd asid) 348 (setVMRootForFlush pd asid)" 349 apply (simp add: set_vm_root_for_flush_def setVMRootForFlush_def getThreadVSpaceRoot_def locateSlot_conv) 350 apply corres 351 apply_debug (trace) (tags "corres_search") (corres_search search: arm_context_switch_corres) 352 continue (* step left *) 353 continue (* if rule *) 354 continue (* failed corres on first subgoal, trying next *) 355 continue (* fail corres on last subgoal, trying reverse if rule *) 356 continue (* can't make corres progress here, trying other goal *) 357 finish (* successful goal discharged by corres *) 358 359 apply (corressimp wp: get_cap_wp getSlotCap_wp)+ 360 apply (rule context_conjI) 361 subgoal by (simp add: cte_map_def objBits_simps tcb_cnode_index_def 362 tcbVTableSlot_def to_bl_1 cte_level_bits_def) 363 apply (rule context_conjI) 364 subgoal by (fastforce simp: cur_tcb_def intro!: tcb_at_cte_at_1[simplified]) 365 apply (rule conjI) 366 subgoal by (fastforce simp: isCap_simps) 367 apply (drule cte_wp_at_ex) 368 apply clarsimp 369 apply (drule (1) pspace_relation_cte_wp_at[rotated 1]; (assumption | clarsimp)?) 370 apply (drule cte_wp_at_norm') 371 apply clarsimp 372 apply (rule_tac x="cteCap cte" in exI) 373 apply (auto elim: cte_wp_at_weakenE' dest!: curthread_relation) 374 done 375 376text \<open>Note we can wrap it all up in corressimp\<close> 377 378lemma set_vm_root_for_flush_corres': 379 notes [corres] = gct_corres getSlotCap_corres 380 shows 381 "corres (=) 382 (cur_tcb and vspace_at_asid asid pd 383 and K (asid \<noteq> 0 \<and> asid \<le> mask asid_bits) 384 and valid_asid_map and valid_vs_lookup 385 and valid_vspace_objs and valid_global_objs 386 and unique_table_refs o caps_of_state 387 and valid_arch_state 388 and pspace_aligned and pspace_distinct) 389 (pspace_aligned' and pspace_distinct' and no_0_obj') 390 (set_vm_root_for_flush pd asid) 391 (setVMRootForFlush pd asid)" 392 apply (simp add: set_vm_root_for_flush_def setVMRootForFlush_def getThreadVSpaceRoot_def locateSlot_conv) 393 apply (corressimp search: arm_context_switch_corres 394 wp: get_cap_wp getSlotCap_wp 395 simp: isCap_simps) 396 apply (rule context_conjI) 397 subgoal by (simp add: cte_map_def objBits_simps tcb_cnode_index_def 398 tcbVTableSlot_def to_bl_1 cte_level_bits_def) 399 apply (rule context_conjI) 400 subgoal by (fastforce simp: cur_tcb_def intro!: tcb_at_cte_at_1[simplified]) 401 apply (rule conjI) 402 subgoal by (fastforce) 403 apply (drule cte_wp_at_ex) 404 apply clarsimp 405 apply (drule (1) pspace_relation_cte_wp_at[rotated 1]; (assumption | clarsimp)?) 406 apply (drule cte_wp_at_norm') 407 apply clarsimp 408 apply (rule_tac x="cteCap cte" in exI) 409 apply (auto elim: cte_wp_at_weakenE' dest!: curthread_relation) 410 done 411*) 412 413end 414end 415