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