1(* 2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230) 3 * 4 * SPDX-License-Identifier: BSD-2-Clause 5 *) 6 7(* 8Hoare reasoning and WP (weakest-precondition) generator rules for the option monad. 9 10This list is almost certainly incomplete; add rules here as they are needed. 11*) 12 13theory OptionMonadWP 14imports 15 OptionMonadND 16 WP 17begin 18 19declare K_def [simp] 20 21(* Hoare triples. 22 TODO: design a sensible syntax for them. *) 23 24(* Partial correctness. *) 25definition ovalid :: "('s \<Rightarrow> bool) \<Rightarrow> ('s \<Rightarrow> 'a option) \<Rightarrow> ('a \<Rightarrow> 's \<Rightarrow> bool) \<Rightarrow> bool" where 26 "ovalid P f Q \<equiv> \<forall>s r. P s \<and> f s = Some r \<longrightarrow> Q r s" 27(* Total correctness. *) 28definition ovalidNF :: "('s \<Rightarrow> bool) \<Rightarrow> ('s \<Rightarrow> 'a option) \<Rightarrow> ('a \<Rightarrow> 's \<Rightarrow> bool) \<Rightarrow> bool" where 29 "ovalidNF P f Q \<equiv> \<forall>s. P s \<longrightarrow> (f s \<noteq> None \<and> (\<forall>r. f s = Some r \<longrightarrow> Q r s))" 30(* Termination. *) 31definition no_ofail where "no_ofail P f \<equiv> \<forall>s. P s \<longrightarrow> f s \<noteq> None" 32 33(* 34This rule lets us apply ovalidNF machinery for proving no_ofail. 35However, we ought to eventually write working wp rules for no_ofail (see below). 36*) 37lemma no_ofail_is_ovalidNF: "no_ofail P f \<equiv> ovalidNF P f (\<lambda>_ _. True)" 38 by (simp add: no_ofail_def ovalidNF_def) 39lemma ovalidNF_combine: "\<lbrakk> ovalid P f Q; no_ofail P f \<rbrakk> \<Longrightarrow> ovalidNF P f Q" 40 by (auto simp: ovalidNF_def ovalid_def no_ofail_def) 41 42 43(* Annotating programs with loop invariant and measure. *) 44definition owhile_inv :: 45 "('a \<Rightarrow> 's \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 's \<Rightarrow> 'a option) \<Rightarrow> 'a 46 \<Rightarrow> ('a \<Rightarrow> 's \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 's \<Rightarrow> nat) \<Rightarrow> 's \<Rightarrow> 'a option" 47 where "owhile_inv C B x I M = owhile C B x" 48 49lemmas owhile_add_inv = owhile_inv_def[symmetric] 50 51 52(* WP rules for ovalid. *) 53lemma obind_wp [wp]: 54 "\<lbrakk> \<And>r. ovalid (R r) (g r) Q; ovalid P f R \<rbrakk> \<Longrightarrow> ovalid P (obind f g) Q" 55 by (simp add: ovalid_def obind_def split: option.splits, fast) 56 57lemma oreturn_wp [wp]: 58 "ovalid (P x) (oreturn x) P" 59 by (simp add: ovalid_def) 60 61lemma ocondition_wp [wp]: 62 "\<lbrakk> ovalid L l Q; ovalid R r Q \<rbrakk> 63 \<Longrightarrow> ovalid (\<lambda>s. if C s then L s else R s) (ocondition C l r) Q" 64 by (auto simp: ovalid_def ocondition_def) 65 66lemma ofail_wp [wp]: 67 "ovalid (\<lambda>_. True) ofail Q" 68 by (simp add: ovalid_def ofail_def) 69 70lemma ovalid_K_bind_wp [wp]: 71 "ovalid P f Q \<Longrightarrow> ovalid P (K_bind f x) Q" 72 by simp 73 74lemma ogets_wp [wp]: "ovalid (\<lambda>s. P (f s) s) (ogets f) P" 75 by (simp add: ovalid_def ogets_def) 76 77lemma oguard_wp [wp]: "ovalid (\<lambda>s. f s \<longrightarrow> P () s) (oguard f) P" 78 by (simp add: ovalid_def oguard_def) 79 80lemma oskip_wp [wp]: 81 "ovalid (\<lambda>s. P () s) oskip P" 82 by (simp add: ovalid_def oskip_def) 83 84lemma ovalid_case_prod [wp]: 85 assumes "(\<And>x y. ovalid (P x y) (B x y) Q)" 86 shows "ovalid (case v of (x, y) \<Rightarrow> P x y) (case v of (x, y) \<Rightarrow> B x y) Q" 87 using assms unfolding ovalid_def by auto 88 89lemma owhile_ovalid [wp]: 90"\<lbrakk>\<And>a. ovalid (\<lambda>s. I a s \<and> C a s) (B a) I; 91 \<And>a s. \<lbrakk>I a s; \<not> C a s\<rbrakk> \<Longrightarrow> Q a s\<rbrakk> 92 \<Longrightarrow> ovalid (I a) (owhile_inv C B a I M) Q" 93 unfolding owhile_inv_def owhile_def ovalid_def 94 apply clarify 95 apply (frule_tac I = "\<lambda>a. I a s" in option_while_rule) 96 apply auto 97 done 98 99definition ovalid_property where "ovalid_property P x = (\<lambda>s f. (\<forall>r. Some r = x s f \<longrightarrow> P r s))" 100lemma ovalid_is_triple [wp_trip]: 101 "ovalid P f Q = triple_judgement P f (ovalid_property Q (\<lambda>s f. f s))" 102 by (auto simp: triple_judgement_def ovalid_def ovalid_property_def) 103 104 105lemma ovalid_wp_comb1 [wp_comb]: 106 "\<lbrakk> ovalid P' f Q; ovalid P f Q'; \<And>s. P s \<Longrightarrow> P' s \<rbrakk> \<Longrightarrow> ovalid P f (\<lambda>r s. Q r s \<and> Q' r s)" 107 by (simp add: ovalid_def) 108 109lemma ovalid_wp_comb2 [wp_comb]: 110 "\<lbrakk> ovalid P f Q; \<And>s. P' s \<Longrightarrow> P s \<rbrakk> \<Longrightarrow> ovalid P' f Q" 111 by (auto simp: ovalid_def) 112 113lemma ovalid_wp_comb3 [wp_comb]: 114 "\<lbrakk> ovalid P f Q; ovalid P' f Q' \<rbrakk> \<Longrightarrow> ovalid (\<lambda>s. P s \<and> P' s) f (\<lambda>r s. Q r s \<and> Q' r s)" 115 by (auto simp: ovalid_def) 116 117 118 119(* WP rules for ovalidNF. *) 120lemma obind_NF_wp [wp]: 121 "\<lbrakk> \<And>r. ovalidNF (R r) (g r) Q; ovalidNF P f R \<rbrakk> \<Longrightarrow> ovalidNF P (obind f g) Q" 122 by (auto simp: ovalidNF_def obind_def split: option.splits) 123 124lemma oreturn_NF_wp [wp]: 125 "ovalidNF (P x) (oreturn x) P" 126 by (simp add: ovalidNF_def oreturn_def) 127 128lemma ocondition_NF_wp [wp]: 129 "\<lbrakk> ovalidNF L l Q; ovalidNF R r Q \<rbrakk> 130 \<Longrightarrow> ovalidNF (\<lambda>s. if C s then L s else R s) (ocondition C l r) Q" 131 by (simp add: ovalidNF_def ocondition_def) 132 133lemma ofail_NF_wp [wp]: 134 "ovalidNF (\<lambda>_. False) ofail Q" 135 by (simp add: ovalidNF_def ofail_def) 136 137lemma ovalidNF_K_bind_wp [wp]: 138 "ovalidNF P f Q \<Longrightarrow> ovalidNF P (K_bind f x) Q" 139 by simp 140 141lemma ogets_NF_wp [wp]: 142 "ovalidNF (\<lambda>s. P (f s) s) (ogets f) P" 143 by (simp add: ovalidNF_def ogets_def) 144 145lemma oguard_NF_wp [wp]: 146 "ovalidNF (\<lambda>s. f s \<and> P () s) (oguard f) P" 147 by (simp add: ovalidNF_def oguard_def) 148 149lemma oskip_NF_wp [wp]: 150 "ovalidNF (\<lambda>s. P () s) oskip P" 151 by (simp add: ovalidNF_def oskip_def) 152 153lemma ovalid_NF_case_prod [wp]: 154 assumes "(\<And>x y. ovalidNF (P x y) (B x y) Q)" 155 shows "ovalidNF (case v of (x, y) \<Rightarrow> P x y) (case v of (x, y) \<Rightarrow> B x y) Q" 156 using assms unfolding ovalidNF_def by auto 157 158lemma owhile_NF [wp]: 159"\<lbrakk>\<And>a. ovalidNF (\<lambda>s. I a s \<and> C a s) (B a) I; 160 \<And>a m. ovalid (\<lambda>s. I a s \<and> C a s \<and> M a s = m) (B a) (\<lambda>r s. M r s < m); 161 \<And>a s. \<lbrakk>I a s; \<not> C a s\<rbrakk> \<Longrightarrow> Q a s\<rbrakk> 162 \<Longrightarrow> ovalidNF (I a) (owhile_inv C B a I M) Q" 163 unfolding owhile_inv_def ovalidNF_def ovalid_def 164 apply clarify 165 apply (rule_tac I = I and M = "measure (\<lambda>r. M r s)" in owhile_rule) 166 apply fastforce 167 apply fastforce 168 apply fastforce 169 apply blast+ 170 done 171 172definition ovalidNF_property where "ovalidNF_property P x = (\<lambda>s f. (x s f \<noteq> None \<and> (\<forall>r. Some r = x s f \<longrightarrow> P r s)))" 173lemma ovalidNF_is_triple [wp_trip]: 174 "ovalidNF P f Q = triple_judgement P f (ovalidNF_property Q (\<lambda>s f. f s))" 175 by (auto simp: triple_judgement_def ovalidNF_def ovalidNF_property_def) 176 177 178lemma ovalidNF_wp_comb1 [wp_comb]: 179 "\<lbrakk> ovalidNF P' f Q; ovalidNF P f Q'; \<And>s. P s \<Longrightarrow> P' s \<rbrakk> \<Longrightarrow> ovalidNF P f (\<lambda>r s. Q r s \<and> Q' r s)" 180 by (simp add: ovalidNF_def) 181 182lemma ovalidNF_wp_comb2 [wp_comb]: 183 "\<lbrakk> ovalidNF P f Q; \<And>s. P' s \<Longrightarrow> P s \<rbrakk> \<Longrightarrow> ovalidNF P' f Q" 184 by (simp add: ovalidNF_def) 185 186lemma ovalidNF_wp_comb3 [wp_comb]: 187 "\<lbrakk> ovalidNF P f Q; ovalidNF P' f Q' \<rbrakk> \<Longrightarrow> ovalidNF (\<lambda>s. P s \<and> P' s) f (\<lambda>r s. Q r s \<and> Q' r s)" 188 by (simp add: ovalidNF_def) 189 190 191 192(* FIXME: WP rules for no_ofail, which might not be correct. *) 193lemma no_ofail_ofail [wp]: "no_ofail (\<lambda>_. False) ofail" 194 by (simp add: no_ofail_def ofail_def) 195 196lemma no_ofail_ogets [wp]: "no_ofail (\<lambda>_. True) (ogets f)" 197 by (simp add: no_ofail_def ogets_def) 198 199lemma no_ofail_obind [wp]: 200 "\<lbrakk> \<And>r. no_ofail (P r) (g r); no_ofail Q f; ovalid Q f P \<rbrakk> \<Longrightarrow> no_ofail Q (obind f g)" 201 by (auto simp: no_ofail_def obind_def ovalid_def) 202 203lemma no_ofail_K_bind [wp]: 204 "no_ofail P f \<Longrightarrow> no_ofail P (K_bind f x)" 205 by simp 206 207lemma no_ofail_oguard [wp]: 208 "no_ofail (\<lambda>s. f s) (oguard f)" 209 by (auto simp: no_ofail_def oguard_def) 210 211lemma no_ofail_ocondition [wp]: 212 "\<lbrakk> no_ofail L l; no_ofail R r \<rbrakk> 213 \<Longrightarrow> no_ofail (\<lambda>s. if C s then L s else R s) (ocondition C l r)" 214 by (simp add: no_ofail_def ocondition_def) 215 216lemma no_ofail_oreturn [wp]: 217 "no_ofail (\<lambda>_. True) (oreturn x)" 218 by (simp add: no_ofail_def oreturn_def) 219 220lemma no_ofail_oskip [wp]: 221 "no_ofail (\<lambda>_. True) oskip" 222 by (simp add: no_ofail_def oskip_def) 223 224lemma no_ofail_is_triple [wp_trip]: 225 "no_ofail P f = triple_judgement P f (\<lambda>s f. f s \<noteq> None)" 226 by (auto simp: triple_judgement_def no_ofail_def) 227 228lemma no_ofail_wp_comb1 [wp_comb]: 229 "\<lbrakk> no_ofail P f; \<And>s. P' s \<Longrightarrow> P s \<rbrakk> \<Longrightarrow> no_ofail P' f" 230 by (simp add: no_ofail_def) 231 232lemma no_ofail_wp_comb2 [wp_comb]: 233 "\<lbrakk> no_ofail P f; no_ofail P' f \<rbrakk> \<Longrightarrow> no_ofail (\<lambda>s. P s \<and> P' s) f" 234 by (simp add: no_ofail_def) 235 236 237 238(* Some extra lemmas for our predicates. *) 239lemma ovalid_grab_asm: 240 "(G \<Longrightarrow> ovalid P f Q) \<Longrightarrow> ovalid (\<lambda>s. G \<and> P s) f Q" 241 by (simp add: ovalid_def) 242lemma ovalidNF_grab_asm: 243 "(G \<Longrightarrow> ovalidNF P f Q) \<Longrightarrow> ovalidNF (\<lambda>s. G \<and> P s) f Q" 244 by (simp add: ovalidNF_def) 245lemma no_ofail_grab_asm: 246 "(G \<Longrightarrow> no_ofail P f) \<Longrightarrow> no_ofail (\<lambda>s. G \<and> P s) f" 247 by (simp add: no_ofail_def) 248 249lemma ovalid_assume_pre: 250 "(\<And>s. P s \<Longrightarrow> ovalid P f Q) \<Longrightarrow> ovalid P f Q" 251 by (auto simp: ovalid_def) 252lemma ovalidNF_assume_pre: 253 "(\<And>s. P s \<Longrightarrow> ovalidNF P f Q) \<Longrightarrow> ovalidNF P f Q" 254 by (simp add: ovalidNF_def) 255lemma no_ofail_assume_pre: 256 "(\<And>s. P s \<Longrightarrow> no_ofail P f) \<Longrightarrow> no_ofail P f" 257 by (simp add: no_ofail_def) 258 259lemma ovalid_pre_imp: 260 "\<lbrakk> \<And>s. P' s \<Longrightarrow> P s; ovalid P f Q \<rbrakk> \<Longrightarrow> ovalid P' f Q" 261 by (simp add: ovalid_def) 262lemma ovalidNF_pre_imp: 263 "\<lbrakk> \<And>s. P' s \<Longrightarrow> P s; ovalidNF P f Q \<rbrakk> \<Longrightarrow> ovalidNF P' f Q" 264 by (simp add: ovalidNF_def) 265lemma no_ofail_pre_imp: 266 "\<lbrakk> \<And>s. P' s \<Longrightarrow> P s; no_ofail P f \<rbrakk> \<Longrightarrow> no_ofail P' f" 267 by (simp add: no_ofail_def) 268 269lemma ovalid_post_imp: 270 "\<lbrakk> \<And>r s. Q r s \<Longrightarrow> Q' r s; ovalid P f Q \<rbrakk> \<Longrightarrow> ovalid P f Q'" 271 by (simp add: ovalid_def) 272lemma ovalidNF_post_imp: 273 "\<lbrakk> \<And>r s. Q r s \<Longrightarrow> Q' r s; ovalidNF P f Q \<rbrakk> \<Longrightarrow> ovalidNF P f Q'" 274 by (simp add: ovalidNF_def) 275 276lemma ovalid_post_imp_assuming_pre: 277 "\<lbrakk> \<And>r s. \<lbrakk> P s; Q r s \<rbrakk> \<Longrightarrow> Q' r s; ovalid P f Q \<rbrakk> \<Longrightarrow> ovalid P f Q'" 278 by (simp add: ovalid_def) 279lemma ovalidNF_post_imp_assuming_pre: 280 "\<lbrakk> \<And>r s. \<lbrakk> P s; Q r s \<rbrakk> \<Longrightarrow> Q' r s; ovalidNF P f Q \<rbrakk> \<Longrightarrow> ovalidNF P f Q'" 281 by (simp add: ovalidNF_def) 282 283end 284