diff --git a/lib/Corres_Method.thy b/lib/Corres_Method.thy index de1e0cfc5a..f6b9b52ff5 100644 --- a/lib/Corres_Method.thy +++ b/lib/Corres_Method.thy @@ -42,6 +42,9 @@ method is_hoare_schematic_post = succeeds \wp_pre, rule hoare_post_False hoareE_post_False\, succeeds \wp_pre, rule wp_post_taut wp_post_tautE\ +(* Succeed if wpsimp or wp can safely be applied *) +method is_safe_wp = is_wp, fails \is_hoare_schematic_post\ + section \Main corres method\ named_theorems corres_splits @@ -52,7 +55,8 @@ method corres_split declares corres_splits = no_name_eta, rule corres_splits Despite that, we are still careful with simp etc here, in case the user does provide a corres rule that generates a schematic in those side condition goals. *) method corres_cleanup methods m uses simp simp_del split split_del cong intro = - m + #break "corres_cleanup", + ( m | assumption | rule refl TrueI | clarsimp simp del: corres_no_simp simp_del simp: simp split: split split del: split_del @@ -60,7 +64,7 @@ method corres_cleanup methods m uses simp simp_del split split_del cong intro = (* enables passing in conjI for terminal goals: *) | (rule intro; corres_cleanup m simp: simp simp_del: simp_del split: split split_del: split_del - cong: cong intro: intro) + cong: cong intro: intro)) (* Apply a single corres rule and attempt to solve non-corres and non-wp side conditions. We don't expect any wp side conditions, but check anyway for safety. If the rule is declared @@ -124,7 +128,7 @@ method corres' (* simplify head corres goal, e.g. for things like liftM unfolding if the user provides such a rule as "simp". Not clarsimp, because clarsimp will still perform hypsubst on assumptions and might through that rewrite guards *) - | succeeds \is_corres\, + | is_corres, simp (no_asm_use) cong: corres_weaker_cong cong split: split split del: if_split split_del add: simp corres_simp del: corres_no_simp simp_del (* simplify any remaining side condition head goal (non-corres, non-wp). This is either a side @@ -142,7 +146,7 @@ method corres' otherwise the goal will still have schematic post conditions. Fail if there is a free schematic postcondition despite all these measures. *) - | succeeds \is_wp\, fails \is_hoare_schematic_post\, + | is_safe_wp, (wpsimp wp: wp wp_del: wp_del simp: simp simp_del: simp_del split: split split_del: split_del cong: cong)+ )+)[1] @@ -160,6 +164,10 @@ method corres section \Corres rule setup\ +(* Avoid using equations in the assumptions. subst_all gets around (no_asm_use) in some cases, + which we don't want. *) +lemmas [corres_no_simp] = subst_all + lemmas [corres_splits] = corres_split corres_splitEE diff --git a/lib/Corres_UL.thy b/lib/Corres_UL.thy index e3a31254a9..ab06df6519 100644 --- a/lib/Corres_UL.thy +++ b/lib/Corres_UL.thy @@ -472,6 +472,13 @@ lemma corres_if3: text \Some equivalences about liftM and other useful simps\ +(* These rules are declared [simp], which in hindsight was not a good decision, because they + change the return relation which often is schematic when these rules apply in the goal. + In those circumstances it is usually safer to unfold liftM_def and proceed with the resulting + substituted term. + + (We leave the [simp] attribute here, because too many proofs now depend on it) +*) lemma corres_liftM_simp[simp]: "corres_underlying sr nf nf' r P P' (liftM t f) g = corres_underlying sr nf nf' (r \ t) P P' f g" diff --git a/lib/ROOT b/lib/ROOT index e4f8b7a3c1..9ff4b9c4a1 100644 --- a/lib/ROOT +++ b/lib/ROOT @@ -104,6 +104,7 @@ session LibTest (lib) in test = Refine + ASpec ExecSpec theories + Corres_Test Crunch_Test_NonDet Crunch_Test_Qualified_NonDet Crunch_Test_Qualified_Trace diff --git a/lib/test/Corres_Test.thy b/lib/test/Corres_Test.thy new file mode 100644 index 0000000000..eec44b9e1e --- /dev/null +++ b/lib/test/Corres_Test.thy @@ -0,0 +1,312 @@ +(* + * Copyright 2023, Proofcraft Pty Ltd + * + * SPDX-License-Identifier: BSD-2-Clause + *) + +theory Corres_Test +imports Lib.Corres_Method +begin + +(* Test cases and tutorial/docs for Corres_Method *) + + +section "Setup" + +(* Setting up some monads and lemmas to play with later *) +experiment + fixes sr nf nf' + + fixes f f' :: "('s, nat) nondet_monad" + assumes f: "corres_underlying sr nf nf' (=) \ \ f f'" + + fixes Q g g' t + assumes g: "\x x'::nat. x = t x' \ corres_underlying sr nf nf' (=) Q \ (g x) (g' x')" + assumes t: "\x. t x = x" + + fixes P + assumes Q: "\P\ f \\_. Q\" + + fixes h h' + assumes h: "corres_underlying sr nf nf' (=) \ \ h h'" +begin + +abbreviation "corres \ corres_underlying sr nf nf'" + + +section "Examples" + +(* The purpose of the corres method is to make progres on easy corres steps, where things + "obviously" match up on the concrete and abstract side. You can provide basic terminal + corres rules like f and g to try. You can provide simp rules to rewrite corres goals + and to solve side conditions of terminal rules such as the rule for g above. Finally, + you can provide wp rules to solve or make progress on the final wp goals that a corres + proof produces. *) +lemma "corres (=) P \ (do x \ f; g x od) (do y \ f'; g' y od)" + by (corres corres: f g wp: Q simp: t) + +(* All of these can be declared globally and will be picked up by the method *) +context + notes [corres] = f g + notes [wp] = Q + notes [simp] = t +begin + +lemma "corres (=) P \ (do x \ f; g x od) (do y \ f'; g' y od)" + by corres + +end + +(* During development, the rules needed are often not declared [corres] yet or the right + simp rules for side conditions etc have yet to be figured out. The following proof + demonstrates this process. *) +lemma "corres (=) P \ (do x \ f; g x od) (do y \ f'; g' y od)" + (* We begin by invoking "corres" *) + apply corres + (* In this case, not much has happened yet, corres has only produced schematic preconditions. + However, we can see that f and f' are the heads of both sides, and searching with find_theorems + for a corres rule that mentions those two turns up the rule "f", which we provided to the corres + method. At this point we can either go back and add it to the previous line, or we + add a new invocation. The process is very similar to using wpsimp. *) + apply (corres corres: f) + (* We see that f has been split off, and we now have a goal for g. Same process as above finds + the corresponding rule. *) + apply (corres corres: g) + (* This solves the corres goal but leaves the side condition of the "g" rule. We can + now either solve it manually with "apply (simp add: t)" and then continue, or, if it really + is as simple as a few simp rules, we can tell the corres method to apply it directly *) + apply (corres simp: t) + (* We now have only wp goals and the final implication left. *) + apply (wp Q) + apply wp + apply simp + apply simp + done + +(* Once we have found this proof, we can roll it up, and merge eg. the "simp: t" into the corres + line before. *) +lemma "corres (=) P \ (do x \ f; g x od) (do y \ f'; g' y od)" + apply corres + apply (corres corres: f) + apply (corres corres: g simp: t) + (* Adding "wp: Q" to the previous line does not help at this stage, because this wp goal + is produced in the (corres corres: f) line above. We could do + apply (corres corres: g simp: t wp: Q)+ + above, which *would* solve the rest of the goals, but using + in an uncontrolled way + is not very stable and therefore not recommended style. *) + apply (wp Q) + apply wp + apply simp + apply simp + done + +(* Merging the g and f corres lines does enable us to prove the Q wp rule. *) +lemma "corres (=) P \ (do x \ f; g x od) (do y \ f'; g' y od)" + apply corres + apply (corres corres: f g simp: t wp: Q) + (* This will still leave the final implication, because we have produced that implication + outside this subgoal. Merging the two corres invocations above will attempt the final + implications automatically as well. *) + apply simp + apply simp + done + + +section "More controlled single-stepping" + +(* Sometimes invoking "corres" does too much or too little. + Too much can occur when the method applies a rule we didn't know is in the [corres] set and + which leaves us with a strange side condition to solve. Or we may have added an unsafe, + not-really-terminal rule to [corres] and now we are getting an unprovable goal. Too little + can occur when the method refuses to split off the head terms even though it looks like a + terminal corres rule should apply. For these cases, we can take apart some of the internal + steps like this: *) +lemma "corres (=) P \ (do x \ f; g x od) (do y \ f'; g' y od)" + (* Controlled way to only introduce schematic preconditions and the final implication *) + apply corres_pre + (* Invoking "corres" would now fail. Maybe we are convinced that the "f" rule is declared + [corres] and we want to figure out why it does not apply. Invoking the corres_split method + will give us the goal the terminal corres rule is tried on: *) + apply corres_split + (* Trying out "rule f" does work now -- if it didn't we could debug that and find out why *) + apply (succeeds \rule f\) + (* Turns out we forgot to declare it, so we add it manually, and the corres method now + succeeds on the subgoal *) + apply (corres corres: f) + (* For the next goal, we have only g. Maybe we want to debug why corres doesn't solve the + application of the "g" rule automatically, or where the "x = t x" side condition comes from. + To do that, we can apply the rule manually: *) + apply (rule g) + (* Now it is clear where that side condition comes from, and we can look for rules to solve + it. *) + apply (simp add: t) + apply (wpsimp wp: Q)+ + done + + +(* Using apply_debug *) +lemma "corres (=) P \ (do x \ f; g x od) (do y \ f'; g' y od)" + (* The corres method declares a "corres" breakpoint tag that can be used with apply_debug to + step through what it does. This is useful if the method goes too far or applies rules we + didn't expect. The (trace) option to apply_debug allows us to see which rules were applied. *) + apply_debug (trace) (tags "corres") (corres corres: f g simp: t wp: Q) + continue (* guard implication *) + continue (* application of f *) + continue (* application of g, including solved side condition for t *) + continue (* wpsimp+, which happens to solve all remaining goals *) + finish + done + +lemma "corres (=) P \ (do x \ f; g x od) (do y \ f'; g' y od)" + (* There is also a corres_cleanup breakpoint for further data *) + apply_debug (trace) (tags "corres", "corres_cleanup") (corres corres: f g simp: t wp: Q) + continue (* guard implication *) + continue (* application of f *) + continue (* application of g, showing side condition *) + continue (* solve side condition (separate goal) *) + continue (* wpsimp+, which happens to solve all remaining goals *) + finish + done + +(* Rewriting corres terms *) +lemma "corres (=) P \ (do x \ f; g x od) (do y \ liftM t f'; g' y od)" + (* In this goal, corres will stop at liftM without finding a rule to apply. Unfolding + liftM_def exposes the bare f' to the toplevel and lets it apply the existing "f" rule. + The "t" rewrite happens to solve the now more complex side condition for g. + Unfolding liftM_def is generally preferred to the liftM corres simp rules, because + these transform schematic guards in ways that later hinder unification. *) + by (corres corres: f g simp: liftM_def t wp: Q) + +(* Rewriting corres terms more carefully *) +lemma "corres (=) P \ (do x \ f; g x od) (do y \ liftM t f'; g' y od)" + (* "term_simp" tells corres to apply the following simp rules only to the side conditions + of terminal corres steps, not to the corres terms themselves. Usually those simp rules + are fairly distinct and side-condition rules don't do anything to the corres terms, so + it's fine to put them in the "simp:" section, but occasionally we want more control. *) + by (corres corres: f g simp: liftM_def term_simp: t wp: Q) + +(* Dealing with asserts and symbolic execution *) +lemma "corres (=) P \ (do s \ get; assert (P s); x \ f; g x od) (do y \ f'; g' y od)" + (* Here we'd like to do symbolic execution on "get" and then use the unsafe rule + corres_assert_gen_asm_l for the assert. Often it is good enough to locally + provide such rules as [corres], but adding corres_symb_exec_l here for instance will + go too far. It will try to execute all of get, assert, and f: *) + apply (corres corres: corres_symb_exec_l[where P=P]) + (* unsolvable *) + oops + +lemma "corres (=) P \ (do s \ get; assert (P s); x \ f; g x od) (do y \ f'; g' y od)" + (* We can provide the same rule as a fallback rule. This means it will be tried only when + no other rule has worked. This lets f and corres_assert_gen_asm_l go first. *) + by (corres corres: corres_assert_gen_asm_l f g + fallback: corres_symb_exec_l[where P=P] + simp: t wp: Q) + +lemma "corres (=) P \ (do s \ get; assert (P s); x \ f; g x od) (do y \ f'; g' y od)" + (* For even more control, we can instantiate the rule further: *) + by (corres corres: corres_assert_gen_asm_l f g + fallback: corres_symb_exec_l[where P=P and m=get] + simp: t wp: Q) + + +section "@{method corres'} and @{method corres_cleanup} parameter methods" + +(* First with corres only, no cleanup method: *) +lemma "corres (=) P \ (do x \ f; g x; h od) (do y \ f'; g' y; h' od)" + apply (corres corres: f g) + (* Imagine we get here, and (simp add: t) wasn't strong enough to solve the side condition. + Maybe we needed fastforce for it: *) + apply (fastforce simp: t) + (* It is absolutely fine to leave this fastforce here, and continue the corres proof *) + apply (corres corres: h) + apply (wpsimp wp: Q)+ + done + +(* Sometimes that one fastforce is the only thing standing in the way of full automation. Providing + the fastforce as a cleanup method can help here. *) +lemma "corres (=) P \ (do x \ f; g x; h od) (do y \ f'; g' y; h' od)" + by (corres' \fastforce simp: t\ corres: f g h wp: Q) + +(* Providing "succeed" will stop at any side condition without solving it. Occasionally useful for + debugging: *) +lemma "corres (=) P \ (do x \ f; g x; h od) (do y \ f'; g' y; h' od)" + apply (corres' \succeed\ corres: f g h term_simp: t) + (* stops at side condition for g, even though t was available in term_simp *) + apply (simp add: t) + apply (corres corres: h) + apply (wpsimp wp: Q)+ + done + +(* Providing something like fastforce can lead to non-termination or slowdown, because the method + will be tried for any side condition. If there is a distinctive goal pattern that can + distinguish when the cleanup method should be run, you can use "match" to restrict the method: *) +lemma "corres (=) P \ (do x \ f; g x; h od) (do y \ f'; g' y; h' od)" + by (corres' \match conclusion in "x = t y" for x y \ \fastforce simp: t\\ corres: f g h wp: Q) + + +section "Form of [@{attribute corres}] rules" + +(* The method expects terminal corres rules to instantiate return relation and guards. + It also expects distinct variables for the abstract and concrete side and tries hard to + not accidentally mix these by rewriting corres terms with assumptions. + + For instance, it would be tempting to write the "g" rule as follows: *) +lemma g': "corres (=) Q \ (g x) (g' x)" + by (simp add: g t) + +(* This will usually not apply in the corres proof, because the goal will tend to have + the form "corres (=) Q \ (g x) (g' y)" with a side condition connecting x and y, and not + "corres (=) Q \ (g x) (g' x)" *) +lemma "corres (=) P \ (do x \ f; g x od) (do y \ f'; g' y od)" + apply (corres corres: f g') + (* \x y. x = y \ corres (=) (?R2 x) (?R'2 y) (g x) (g' y) *) + apply (fails \rule g'\) + (* The original "g" rule from the top of this file works, because it has separate x and y *) + apply (rule g) + apply (wpsimp wp: Q simp: t)+ + done + +(* The corres method refuses to rewrite guards for the same reason. + Because corres is careful with keeping abstract and concrete variables separate, + it is usually safe to interleave corres with corres_cases or corres_cases_both *) +lemma "corres (=) P \ + (do x \ case z of None \ f | Some x' \ do return x'; f od; g x od) + (do y \ f'; g' y od)" + by (corres corres: f g simp: t wp: Q | corres_cases)+ + +(* It is usually safe to interleave corres with methods that solve their goal, such as + fastforce, blast, etc. + + It is *not* generally safe to interleave corres with simp or clarsimp. It can occasionally be + useful to invoke simp or clarsimp manually on corres terms with schematics, but + generally it is unsafe and should be avoided. Use the "simp:" facility of the corres method + instead wherever possible, because it provides some protection against common pitfalls. + + Occasionally it is useful to interleave with tactics that work on specific kinds of goals + only, e.g. a clarsimp on goals that are not corres goals. For this, the predicate methods + is_corres, is_wp, and is_safe_wp are available. These do not change the proof state, but they + fail when their predicate does not hold. + + is_corres succeeds on corres goals only + is_wp succeeds on wp goals only (valid, validE, no_fail) + is_safe_wp succeeds only on wp goals without a schematic post condition (where wpsimp is not safe) + + Boolean combinations of predicates can be obtained with "," "|" and "fails" for "and", "or", and + "not". +*) + +(* Example of predicate methods *) +lemma "corres (=) P \ + (do x \ case z of None \ f | Some x' \ do return x'; f od; g x od) + (do y \ f'; g' y od)" + (* Do case distinction and apply the corres method only to the corres goals: *) + apply (corres_cases; (is_corres, corres corres: f g)?) + (* Find all safe wp goals and run wpsimp on them *) + apply (all \(is_safe_wp, wpsimp wp: Q)?\) + (* Only non-corres and non-wp should remain -- fail if that is not the case *) + apply (all \fails \is_corres | is_wp\, simp add: t\) + done + +end + +end diff --git a/proof/refine/RISCV64/ArchAcc_R.thy b/proof/refine/RISCV64/ArchAcc_R.thy index a7689ac983..3beb2515cf 100644 --- a/proof/refine/RISCV64/ArchAcc_R.thy +++ b/proof/refine/RISCV64/ArchAcc_R.thy @@ -334,8 +334,9 @@ lemma corres_cross_over_pte_at: done lemma getObject_PTE_corres[corres]: - "corres pte_relation' (pte_at p and pspace_aligned and pspace_distinct) \ - (get_pte p) (getObject p)" + "p = p' \ + corres pte_relation' (pte_at p and pspace_aligned and pspace_distinct) \ + (get_pte p) (getObject p')" apply (rule corres_cross_over_pte_at, fastforce) apply (simp add: getObject_def gets_map_def split_def bind_assoc) apply (rule corres_no_failI) @@ -451,8 +452,8 @@ lemma setObject_PT_corres: done lemma storePTE_corres[corres]: - "pte_relation' pte pte' \ - corres dc (pte_at p and pspace_aligned and pspace_distinct) \ (store_pte p pte) (storePTE p pte')" + "\ p = p'; pte_relation' pte pte' \ \ + corres dc (pte_at p and pspace_aligned and pspace_distinct) \ (store_pte p pte) (storePTE p' pte')" apply (simp add: store_pte_def storePTE_def) apply (rule corres_assume_pre, simp add: pte_at_def) apply (rule corres_symb_exec_l) @@ -577,7 +578,7 @@ lemma pteAtIndex_corres: \ (get_pte (pt_slot_offset level pt vptr)) (pteAtIndex level' pt vptr)" - by (simp add: pteAtIndex_def) (rule getObject_PTE_corres) + by (simp add: pteAtIndex_def getObject_PTE_corres) lemma user_region_or: "\ vref \ user_region; vref' \ user_region \ \ vref || vref' \ user_region" diff --git a/proof/refine/RISCV64/Arch_R.thy b/proof/refine/RISCV64/Arch_R.thy index cb087dc3fe..223f87637a 100644 --- a/proof/refine/RISCV64/Arch_R.thy +++ b/proof/refine/RISCV64/Arch_R.thy @@ -454,12 +454,7 @@ lemma checkSlot_corres: (check_slot p test) (checkSlot p test')" apply (simp add: check_slot_def checkSlot_def unlessE_whenE liftE_bindE) - apply (rule corres_guard_imp) - apply (rule corres_split[OF getObject_PTE_corres]) - apply (rule corres_whenE, simp) - apply (rule corres_trivial, simp) - apply simp - apply wpsimp+ + apply (corres corres: corres_throwErrorTT[of ser]) done lemma vmrights_map_vm_kernel_only[simp]: diff --git a/proof/refine/RISCV64/VSpace_R.thy b/proof/refine/RISCV64/VSpace_R.thy index 264597b36b..1c6ce35bf0 100644 --- a/proof/refine/RISCV64/VSpace_R.thy +++ b/proof/refine/RISCV64/VSpace_R.thy @@ -295,18 +295,7 @@ lemma unmapPageTable_corres: (unmap_page_table asid vptr pt) (unmapPageTable asid' vptr' pt')" apply (clarsimp simp: assms unmap_page_table_def unmapPageTable_def ignoreFailure_def const_def) - apply (rule corres_guard_imp) - apply (rule corres_split_catch[where E="\\" and E'="\\", OF _ corres_return_trivial]) - apply (rule corres_split_eqrE[OF findVSpaceForASID_corres[OF refl]]) - apply (rule corres_split_eqrE[OF lookupPTFromLevel_corres[OF _ refl]]) - apply simp - apply (simp add: liftE_bindE) - apply (rule corres_split[OF storePTE_corres]) - apply simp - apply simp - apply (rule corres_machine_op) - apply (rule corres_Id; simp) - apply (wpsimp wp: pt_lookup_from_level_wp)+ + apply (corres corres: lookupPTFromLevel_corres wp: pt_lookup_from_level_wp) apply (clarsimp simp: invs_distinct invs_psp_aligned invs_vspace_objs invs_valid_asid_table pte_at_eq) apply (rule_tac x=asid in exI) @@ -361,11 +350,11 @@ lemma unmapPage_corres: apply (rule whenE_throwError_corres_initial, simp, simp) apply (rule corres_splitEE) apply (rule corres_rel_imp) - apply (rule liftE_get_pte_corres[@lift_corres_args], simp) + apply (rule liftE_get_pte_corres, simp) apply fastforce apply (rule corres_splitEE[OF checkMappingPPtr_corres]; assumption?) apply (simp add: liftE_bindE) - apply (rule corres_split[OF storePTE_corres]) + apply (rule corres_split[OF storePTE_corres], rule refl) apply simp apply simp apply (rule corres_machine_op, rule corres_Id, rule refl; simp) @@ -474,12 +463,7 @@ lemma performPageInvocation_corres: apply (simp add: bind_assoc) apply (rule corres_guard_imp) apply (simp add: perform_pg_inv_map_def) - apply (rule corres_split[OF updateCap_same_master]) - apply simp - apply (rule corres_split[OF storePTE_corres]) - apply assumption - apply (rule corres_machine_op, rule corres_Id; simp) - apply wpsimp+ + apply (corres corres: updateCap_same_master) apply (clarsimp simp: invs_valid_objs invs_distinct invs_psp_aligned) apply (clarsimp simp: cte_wp_at_caps_of_state is_arch_update_def is_cap_simps) apply (clarsimp simp: same_ref_def) @@ -590,12 +574,7 @@ lemma performPageTableInvocation_corres: apply (clarsimp simp: valid_pti_def valid_pti'_def split: arch_cap.splits capability.split_asm arch_capability.split_asm) apply (rule corres_guard_imp) - apply (rule corres_split[OF updateCap_same_master]) - apply simp - apply (rule corres_split[OF storePTE_corres]) - apply assumption - apply (rule corres_machine_op, rule corres_Id; simp) - apply wpsimp+ + apply (corres corres: updateCap_same_master) apply (clarsimp simp: cte_wp_at_caps_of_state is_arch_update_def invs_valid_objs invs_psp_aligned invs_distinct) apply (case_tac cap; simp add: is_cap_simps cap_master_cap_simps)