1(* 2 * Copyright 2014, NICTA 3 * 4 * This software may be distributed and modified according to the terms of 5 * the BSD 2-Clause license. Note that NO WARRANTY is provided. 6 * See "LICENSE_BSD2.txt" for details. 7 * 8 * @TAG(NICTA_BSD) 9 *) 10 11theory WPTutorial 12imports "Refine.Bits_R" 13begin 14 15text {* 16This is a tutorial on the use of the various Hoare mechanisms developed 17for the L4.verified project. We import Bits_R above, which is a compromise 18between the twin goals of getting the Hoare setup from L4.verified and not 19importing existing properties. It's probably best to work from a prebuilt 20Refine Isabelle image which includes Bits_R. 21*} 22 23text {* The point of our apparatus is to prove Hoare triples. These are a 24triple of a precondition, function, and postcondition. In our state-monadic 25world, the precondition is a function of the state, and the postcondition 26is a function of the return value and the state. In example 1 below, 27the precondition doesn't impose any restriction on the state, and the 28postcondition only requires that the return value be the obvious one. *} 29 30text {* The weakest precondition tool, wp, attempts to construct the 31weakest precondition for a given postcondition. Use wp (with the command 32"apply wp") to solve example 1 *} 33 34lemma example_1: 35 "\<lbrace>\<lambda>s. True\<rbrace> return 1 \<lbrace>\<lambda>rv s. rv = 1\<rbrace>" 36 apply wp 37 apply simp 38 done 39 40text {* The wp tool works in reverse order (from postcondition to weakest 41precondition, rather than from precondition to strongest postcondition). 42It stops when it encounters a postcondition/function pair it doesn't 43know any rules for. Try example 2 below, noting where wp gets stuck. 44 45The wp method already knows how to handle most monadic operations 46(liftE, catch, assert, when, if-then-else, etc) but there are some 47exceptions. One is the split operator, which hides behind Isabelle syntax 48that looks like (\<lambda>(x, y). blah), {(x, y). blah}, (\<forall>(x, y) \<in> S. blah). 49Solve the problem by unfolding it with (simp add: split_def). 50 51The intermediate precondition seen when wp stops is a schematic variable. 52The wp tool uses Isabelle's underlying unification mechanism to set the 53precondition as it goes. This usually works well, but there are some 54problems, especially with tuples. Note the strange behaviour if we use 55clarsimp instead of (simp add: split_def) to deal with the split constant. 56The root cause of this strange behaviour is that the unification mechanism 57does not know how to construct a ?P such that "?P (a, b) = a". This is 58annoying, since it means that clarsimp/clarify/safe must frequently be 59avoided. 60*} 61 62lemma example_2: 63 "\<lbrace>\<lambda>s. s = [(True, False), (False, True)]\<rbrace> do 64 v \<leftarrow> gets length; 65 (x, y) \<leftarrow> gets hd; 66 return x 67 od \<lbrace>\<lambda>rv s. rv\<rbrace>" 68 apply wp 69 apply (simp add: split_def) 70 apply wp+ 71 apply simp 72 done 73 74text {* 75An additional annoyance to the clarsimp/tuple issue described above is 76the splitter. The wp tool is designed to work on a hoare triple with a 77schematic precondition. Note how the simplifier splits the problem 78in two because it contains an if constant. Delete the split 79rule from the simpset with (simp split del: if_split) to avoid this 80issue and see where wp gets stuck. 81 82We still need to deal with the if constant. In this (somewhat contrived) 83example we can give the simplifier the rule if_apply_def2 to make 84progress. 85 86Note that wp can deal with a function it knows nothing about if 87the postcondition is constant in the return value and state. 88*} 89 90lemma example_3: 91 "\<lbrace>\<lambda>s. s = [False, True]\<rbrace> do 92 x \<leftarrow> gets hd; 93 possible_state_change_that_isnt_defined; 94 y \<leftarrow> gets (if x then \<bottom> else \<top>); 95 return $ y \<and> \<not> x 96 od \<lbrace>\<lambda>rv s. rv\<rbrace>" 97 apply wp 98 apply (simp add: if_apply_def2 split del: if_split) 99 apply wp+ 100 apply simp 101 done 102 103text {* Let's make this more interesting by introducing some functions 104from the abstract specification. The set_endpoint function (an abbreviation 105for the function set_simple_ko) is used to set the contents of an endpoint 106object somewhere in the kernel object heap (kheap). The cap derivation 107tree (cdt) lives in an entirely different field of the state to the kheap, 108so this fact about it should be unchanged by the endpoint update. 109Solve example 4 - you'll have to unfold enough definitions that wp knows 110what to do. *} 111 112lemma example_4: 113 "\<lbrace>\<lambda>s. cdt s (42, [True, False]) = None\<rbrace> 114 set_endpoint ptr Structures_A.IdleEP 115 \<lbrace>\<lambda>rv s. cdt s (42, [True, False]) = None\<rbrace>" 116 apply (simp add: set_simple_ko_def set_object_def get_object_def) 117 apply wp 118 apply clarsimp 119 done 120 121text {* 122Example 4 proved that a property about the cdt was preserved from 123before set_endpoint to after. This preservation property is true for 124any property that just talks about the cdt. Example 5 rephrases 125example 4 in this style. Get used to this style of Hoare triple, 126it is very common in our proofs. 127*} 128 129lemma example_5: 130 "\<lbrace>\<lambda>s. P (cdt s)\<rbrace> 131 set_endpoint ptr Structures_A.IdleEP 132 \<lbrace>\<lambda>rv s. P (cdt s)\<rbrace>" 133 apply (simp add: set_simple_ko_def set_object_def get_object_def) 134 apply wp 135 apply clarsimp 136 done 137 138text {* 139The set_cap function from the abstract specification is not much different 140to set_endpoint. However, caps can live within CSpace objects or within 141TCBs, and the set_cap function handles this issue with a case division. 142 143The wp tool doesn't know anything about how to deal with case statements. 144In addition to the tricks we've learned already, use the wpc tool to break 145up the case statement into components so that wp can deal with it to solve 146example 6. 147*} 148 149lemma example_6: 150 "\<lbrace>\<lambda>s. P (cdt s)\<rbrace> 151 set_cap cap ptr 152 \<lbrace>\<lambda>rv s. P (cdt s)\<rbrace>" 153 apply (simp add: set_cap_def split_def set_object_def 154 get_object_def) 155 apply (wp | wpc)+ 156 apply simp 157 done 158 159text {* 160The wp method can be given additional arguments which are theorems to use 161as summaries. Solve example 7 by supplying example 6 as a rule to 162use with (wp example_6). 163*} 164 165lemma example_7: 166 "\<lbrace>\<lambda>s. cdt s ptr' = None\<rbrace> do 167 set_cap cap.NullCap ptr; 168 v \<leftarrow> gets (\<lambda>s. cdt s ptr); 169 assert (v = None); 170 set_cap cap.NullCap ptr'; 171 set_cap cap.IRQControlCap ptr'; 172 return True 173 od \<lbrace>\<lambda>rv s. cdt s ptr = None \<and> cdt s ptr' = None\<rbrace>" 174 apply (wp example_6) 175 apply simp 176 done 177 178text {* 179There isn't a good reason not to use example_6 whenever possible, so we can 180declare example_6 a member of the wp rule set by changing its proof site to 181"lemma example_6[wp]:", by doing "declare example_6[wp]", or by putting it 182in a group of lemmas declared wp with "lemmas foo[wp] = example_6". 183Pick one of those options and remove the manual reference to example_6 from 184the proof of example_7. 185*} 186 187text {* 188These preservation Hoare triples are often easy to prove and apply, so much 189of the effort is in typing them all out. To speed this up we have the crunch 190tool. Let's prove that setup_reply_master and set_endpoint don't change 191another field of the state, machine_state. I've typed out the required 192crunch command below. Let's explain the bits. The naming scheme 193"machine_state_preserved:" sets a common suffix for all the lemmas 194proved. Just like with lemma names, we could add the theorems to the wp set 195with "machine_state_preserved[wp]:". What follows is a list of functions. 196The crunch tool also descends through the call graph of functions, so it 197proves a rule about set_cap because setup_reply_master calls it. The last 198argument is the term to appear in the precondition and postcondition. 199 200The final, optional bit of the crunch syntax is a group of modifiers, which 201go between the parentheses inserted below. The crunch command doesn't 202currently work. We need to provide some additional simp and wp rules 203with syntax like (simp: some rules wp: some rules). If you look at the way 204crunch failed, you'll spot which simp rule we need to add to make some 205progress. 206 207But not much more progress. To get through set_endpoint, we need to deal 208with a slightly complex postcondition to get_object, one which incorporates 209an assertion about its return value. We can solve this problem by simply 210throwing the extra assumption away - supplying the wp rule hoare_drop_imps 211does this. There are standard sets of simp and wp rules which are frequently 212helpful to crunch, crunch_simps and crunch_wps, which contain the rules we 213added here. 214*} 215 216crunch machine_state_preserved: 217 setup_reply_master, set_simple_ko 218 "\<lambda>s. P (machine_state s)" 219 (simp: split_def wp: crunch_wps) 220 221end 222