1(* 2 * Copyright 2017, Data61 3 * Commonwealth Scientific and Industrial Research Organisation (CSIRO) 4 * ABN 41 687 119 230. 5 * 6 * This software may be distributed and modified according to the terms of 7 * the BSD 2-Clause license. Note that NO WARRANTY is provided. 8 * See "LICENSE_BSD2.txt" for details. 9 * 10 * @TAG(DATA61_BSD) 11 *) 12 13chapter \<open>Extending C refinement proofs using AutoCorres\<close> 14 15theory AutoCorres_C 16imports 17 Corres_C 18 AutoCorresModifiesProofs 19begin 20 21text \<open> 22This theory provides some tools for extending existing collections of C refinement proofs, 23which use the @{term ccorresG} framework, with new proofs using the higher-level 24@{term corres_underlying} framework. We use AutoCorres to move between the frameworks. 25 26See AutoCorresTest for examples. 27\<close> 28 29section \<open>Setup\<close> 30 31text \<open> 32The imports for this theory cause a merge between AutoCorres and the preamble for CRefine. 33AutoCorres both adds to and deletes from various rule sets, such that the merge produces 34an entirely new theory context, which is unfamiliar to any previous CRefine or AutoCorres 35development. In particular, rules which were deleted in AutoCorres may reappear in this 36theory, but in a different place in the rule set than they appeared in Corres_C. 37 38The following setup restores the ordering from @{theory CRefine.Corres_C} for the crucial 39@{attribute wp_comb} rule set, and places new rules introduced by @{theory AutoCorres.AutoCorres} at 40the end of the @{attribute wp_comb} set. 41 42To ensure that we only have to do this once, we are careful to ensure that there is only 43one theory merge between AutoCorres and CRefine. We import @{theory CRefine.L4VerifiedLinks} into 44@{theory CRefine.AutoCorresModifiesProofs}, and import the latter here. This satisfies the 45dependencies from @{theory CRefine.AutoCorresModifiesProofs} to @{theory AutoCorres.AutoCorres}, and from 46this theory to @{theory CRefine.L4VerifiedLinks} and @{theory CRefine.Corres_C}, without duplicating 47theory merges. Finally, we list @{theory CRefine.L4VerifiedLinks} as a top-level theory in the 48CBaseRefine session, so that @{theory AutoCorres.AutoCorres} need not be processed in a CRefine 49session, but do not import @{theory AutoCorres.AutoCorres} into @{text CBaseRefine.Include_C}, since that would 50cause a redundant theory merge. 51\<close> 52 53setup \<open> 54 fn thy => let 55 fun get_combs thy = #combs (WeakestPre.get_rules (Proof_Context.init_global thy) []) 56 val corres_c_combs = get_combs (Context.get_theory {long=true} thy "CRefine.Corres_C") 57 val accorres_combs = get_combs thy 58 val subtract_thms = subtract (fn (a,b) => Thm.prop_of a = Thm.prop_of b) 59 val accorres_extra = subtract_thms corres_c_combs accorres_combs 60 fun upd attr = fold_rev (snd oo Thm.apply_attribute attr) 61 val add = upd WeakestPre.combs_add 62 val del = upd WeakestPre.combs_del 63 val upd_gen = add corres_c_combs o add accorres_extra o del accorres_combs 64 in Context.theory_of (upd_gen (Context.Theory thy)) end 65\<close> 66 67text \<open> 68AutoCorres adds some rules about @{term whenE} to the @{attribute wp} set, which don't always 69behave nicely. They introduce @{term If} expressions into pre and post conditions, where they 70don't always simplify as one might expect. We replace them with a rule that does allow the 71conditional to simplify away more often. 72 73FIXME: Move this change into AutoCorres itself, or the underlying VCG library. 74\<close> 75 76lemmas [wp del] = 77 NonDetMonadEx.validE_whenE 78 NonDetMonadVCG.hoare_whenE_wps 79 80lemmas hoare_whenE_wp2 [wp] = 81 NonDetMonadVCG.hoare_whenE_wps[simplified if_apply_def2] 82 83section \<open>Rules for proving @{term ccorres_underlying} goals\<close> 84 85text \<open> 86Following are rules for converting a @{term ccorresG} goal to a @{term corres_underlying} 87goal, by making use of an automatically generated @{term ac_corres} fact about the procedure. 88 89For the first two of these, the user is expected to specify the return-value relation for the 90resulting @{term corres_underlying} goal, and will be required to prove that it implies the 91return-value relation of the original @{term ccorresG} goal. 92 93In the general case, the C can return some extra information via global variables. 94\<close> 95 96(* FIXME: provide a way to use this rule, and its rv_spec version, in ac_init. *) 97lemma corres_to_ccorres_extra_globals: 98 assumes rf_sr_def: "rf_sr \<equiv> {(s,s'). cstate_relation s (globals s')}" 99 assumes acc: "ac_corres globals check_term \<Gamma> ret_xf G (liftE ac) c" 100 assumes cac: "corres_underlying {(s,s'). cstate_relation s s'} True True 101 R P Q a (do x \<leftarrow> ac; y \<leftarrow> gets g; return (x,y) od)" 102 assumes pre: "\<And>s s'. cstate_relation s (globals s') \<Longrightarrow> P' s \<and> s' \<in> Q' \<Longrightarrow> P s \<and> Q (globals s')" 103 assumes p_g: "\<And>s s'. cstate_relation s (globals s') \<Longrightarrow> P' s \<and> s' \<in> Q' \<Longrightarrow> G s'" 104 assumes ret: "\<And>r s'. R r (ret_xf s', g (globals s')) \<longrightarrow> R' r (ret_xf' s')" 105 shows "ccorresG rf_sr \<Gamma> R' ret_xf' P' Q' [] a c" 106 unfolding rf_sr_def using ac_corres_ccorres_underlying[OF acc] 107 apply (clarsimp intro!: ccorresI') 108 apply (frule corres_underlyingD[OF cac, simplified], (simp add: pre)+) 109 apply (clarsimp simp: bind_def return_def simpler_gets_def) 110 apply (erule ccorresE, simp+, erule p_g, simp+) 111 apply (simp add: liftE_def) 112 apply assumption 113 apply (fastforce simp: unif_rrel_def dest: mp[OF ret] split: xstate.splits) 114 done 115 116text \<open> 117In the case where there is no extra information returned via global variables, the rule is simpler. 118\<close> 119 120lemma corres_to_ccorres: 121 assumes rf_sr_def: "rf_sr \<equiv> {(s,s'). cstate_relation s (globals s')}" 122 assumes acc: "ac_corres globals check_term \<Gamma> ret_xf G (liftE ac) c" 123 assumes cac: "corres_underlying {(s,s'). cstate_relation s s'} True True R P Q a ac" 124 assumes pre: "\<And>s s'. cstate_relation s (globals s') \<Longrightarrow> P' s \<and> s' \<in> Q' \<Longrightarrow> P s \<and> Q (globals s')" 125 assumes p_g: "\<And>s s'. cstate_relation s (globals s') \<Longrightarrow> P' s \<and> s' \<in> Q' \<Longrightarrow> G s'" 126 assumes ret: "\<And>r s'. R r (ret_xf s') \<longrightarrow> R' r (ret_xf' s')" 127 shows "ccorresG rf_sr \<Gamma> R' ret_xf' P' Q' [] a c" 128 apply (rule corres_to_ccorres_extra_globals[OF rf_sr_def acc, where g="K ()" and R="\<lambda>v. R v o fst"]) 129 apply (simp add: liftM_def[symmetric]) 130 apply (rule corres_rel_imp, rule cac) 131 apply (auto simp: pre p_g ret) 132 done 133 134text \<open> 135In the following versions of the above rules, the return-value relation for the resulting 136@{term corres_underlying} goal is fixed to a reasonably general relation. In cases where this 137return-value relation is good enough, it saves the effort of explicitly specifying a return-value 138relation. 139\<close> 140 141lemma corres_to_ccorres_extra_globals_rv_spec: 142 assumes "rf_sr \<equiv> {(s,s'). cstate_relation s (globals s')}" 143 assumes "ac_corres globals check_term \<Gamma> ret_xf G (liftE ac) c" 144 assumes "corres_underlying {(s,s'). cstate_relation s s'} True True 145 (\<lambda>r (x,y). \<forall>s'. x = ret_xf s' \<and> y = g (globals s') \<longrightarrow> R' r (ret_xf' s')) 146 P Q a (do x \<leftarrow> ac; y \<leftarrow> gets g; return (x, y) od)" 147 assumes "\<And>s s'. cstate_relation s (globals s') \<Longrightarrow> P' s \<and> s' \<in> Q' \<Longrightarrow> P s \<and> Q (globals s')" 148 assumes "\<And>s s'. cstate_relation s (globals s') \<Longrightarrow> P' s \<and> s' \<in> Q' \<Longrightarrow> G s'" 149 shows "ccorresG rf_sr \<Gamma> R' ret_xf' P' Q' [] a c" 150 using assms by (auto intro: corres_to_ccorres_extra_globals) 151 152lemma corres_to_ccorres_rv_spec: 153 assumes "rf_sr \<equiv> {(s,s'). cstate_relation s (globals s')}" 154 assumes "ac_corres globals check_term \<Gamma> ret_xf G (liftE ac) c" 155 assumes "corres_underlying {(s,s'). cstate_relation s s'} True True 156 (\<lambda>r r'. \<forall>s'. r' = ret_xf s' \<longrightarrow> R' r (ret_xf' s')) P Q a ac" 157 assumes "\<And>s s'. cstate_relation s (globals s') \<Longrightarrow> P' s \<and> s' \<in> Q' \<Longrightarrow> P s \<and> Q (globals s')" 158 assumes "\<And>s s'. cstate_relation s (globals s') \<Longrightarrow> P' s \<and> s' \<in> Q' \<Longrightarrow> G s'" 159 shows "ccorresG rf_sr \<Gamma> R' ret_xf' P' Q' [] a c" 160 using assms by (auto intro: corres_to_ccorres) 161 162section \<open>Rules for importing @{term ccorresG} facts\<close> 163 164text \<open> 165While proving a @{term corres_underlying} goal which was obtained from a @{term ccorresG} goal, 166we might want to make use of existing @{term ccorresG} facts about called procedures. Following 167are rules for converting existing @{term ccorresG} facts to suitable @{term corres_underlying} 168facts. 169\<close> 170 171lemma in_AC_call_simpl: 172 fixes r s s' arg_pred ret_xf \<Gamma> f_'proc 173 shows "(r, s') \<in> fst (AC_call_L1 arg_pred globals ret_xf (L1_call_simpl check_term \<Gamma> f_'proc) s) \<Longrightarrow> 174 \<exists>cs cs'. s = globals cs \<and> arg_pred cs \<and> 175 (check_term \<longrightarrow> \<Gamma> \<turnstile> Call f_'proc \<down> Normal cs) \<and> 176 \<Gamma> \<turnstile> \<langle>Call f_'proc, Normal cs\<rangle> \<Rightarrow> Normal cs' \<and> 177 s' = globals cs' \<and> r = ret_xf cs'" 178 apply (clarsimp simp: AC_call_L1_def L2_call_L1_def L1_call_simpl_def 179 in_monad liftM_def select_def select_f_def 180 split: xstate.splits sum.splits) 181 apply (rename_tac cs cs' status; case_tac status; fastforce) 182 done 183 184text \<open> 185Given a @{term ccorresG} fact, we need to process its preconditions to obtain a 186@{term corres_underlying} fact in a usable form. The following definition, rules and method 187provide some machinery for this processing. 188 189For a @{term ccorresG} rule about a procedure call, the concrete precondition typically 190describes how local variables in the C state relate to the arguments of the abstract procedure 191call. In some cases, it might also talk about the global C state. 192 193For the conversion from @{term ccorresG} to @{term corres_underlying}, we will use AutoCorres 194to generate an abstract wrapper around the C call. The wrapper will also have a precondition 195describing the relationship between local variables in the C state, and arguments to the 196wrapper. 197 198The purpose of this machinery, then, is to partition the components of the @{term ccorresG} 199precondition. Preconditions concerning function arguments are matched between the @{term ccorresG} 200fact and the AutoCorres-generated wrapper, and need not appear in the preconditions of the 201resulting @{term ccorres_underlying} rule. On the other hand, preconditions concerning global 202state must appear in the resulting @{term ccorres_underlying} rule. 203\<close> 204 205definition 206 "ccorres_to_corres_pre Q E Q' s' \<equiv> Q (globals s') \<longrightarrow> E s' \<and> s' \<in> Q'" 207 208text \<open> 209In @{term ccorres_to_corres_pre}, parameter @{term Q'} is the @{term ccorresG} precondition 210begin analysed; parameter @{term Q} is a schematic variable for what will become the precondition 211of the resulting @{term ccorres_underlying} rule, and therefore only concerns global state; and 212parameter @{term E} accumulates equalities between arguments to the AutoCorres-generated wrapper 213and the arguments to the abstract function call in the @{term ccorresG} fact. 214\<close> 215 216text \<open> 217Preconditions concerning global variables are incorporated into the precondition of the 218resulting @{term ccorres_underlying} fact. 219\<close> 220lemma ccorres_to_corres_pre_globals_Int: 221 assumes "ccorres_to_corres_pre Q E Q' s'" 222 shows "ccorres_to_corres_pre (P and Q) E ({s'. P (globals s')} \<inter> Q') s'" 223 using assms by (simp add: ccorres_to_corres_pre_def) 224 225lemmas ccorres_to_corres_pre_globals_base 226 = ccorres_to_corres_pre_globals_Int[where Q'=UNIV, simplified Int_UNIV_right] 227 228text \<open> 229For preconditions concerning function arguments, we can eliminate any mention of C local 230variable state, and are left with a predicate on the argument to AutoCorres-generated 231wrapper. Typically, this will be a relation to an argument to the abstract call in the 232@{term ccorresG} fact. 233\<close> 234lemma ccorres_to_corres_pre_local_Int: 235 assumes "f s' = x" 236 assumes "ccorres_to_corres_pre Q (K (P x) and E) Q' s'" 237 shows "ccorres_to_corres_pre Q E ({s'. P (f s')} \<inter> Q') s'" 238 using assms by (simp add: ccorres_to_corres_pre_def) 239 240lemmas ccorres_to_corres_pre_local_base 241 = ccorres_to_corres_pre_local_Int[where Q'=UNIV, simplified Int_UNIV_right] 242 243lemma ccorres_to_corres_pre_UNIV_Int: 244 assumes "ccorres_to_corres_pre Q E Q' s'" 245 shows "ccorres_to_corres_pre Q E (UNIV \<inter> Q') s'" 246 using assms by (simp add: ccorres_to_corres_pre_def) 247 248lemmas ccorres_to_corres_pre_intros = 249 ccorres_to_corres_pre_UNIV_Int 250 ccorres_to_corres_pre_globals_Int 251 ccorres_to_corres_pre_globals_base 252 253lemmas ccorres_to_corres_pre_elims = 254 ccorres_to_corres_pre_local_Int 255 ccorres_to_corres_pre_local_base 256 257lemma ccorres_to_corres_pre_finalise: 258 "E s' \<Longrightarrow> ccorres_to_corres_pre \<top> E UNIV s'" 259 by (simp add: ccorres_to_corres_pre_def) 260 261method ccorres_to_corres_pre_step = 262 (rule ccorres_to_corres_pre_intros | erule ccorres_to_corres_pre_elims) 263 264method ccorres_to_corres_pre_process = ( 265 (elim pred_andE)?, 266 (simp only: Int_assoc)?, 267 (ccorres_to_corres_pre_step+)?, 268 (rule ccorres_to_corres_pre_finalise), 269 (intro pred_andI TrueI; clarsimp) 270) 271 272text \<open> 273We can easily obtain a partial @{term corres_underlying} fact from a @{term ccorresG} fact. 274However, this is not strong enough to prove @{term ccorresG} goals of the form produced by 275@{thm corres_to_ccorres} above. 276\<close> 277 278lemma ccorres_to_corres_partial: 279 assumes rf_sr_def: "rf_sr \<equiv> {(s,s'). cstate_relation s (globals s')}" 280 assumes ac_def: "ac_f \<equiv> AC_call_L1 G globals ret_xf (L1_call_simpl check_term \<Gamma> f_'proc)" 281 assumes ccorres: "ccorresG rf_sr \<Gamma> R' ret_xf' P Q' [] dspec_f (Call f_'proc)" 282 assumes pre: "\<And>s'. G s' \<Longrightarrow> ccorres_to_corres_pre Q \<top> Q' s'" 283 assumes ret: "\<And>r s'. R r (ret_xf s') \<longleftrightarrow> R' r (ret_xf' s')" 284 shows "corres_underlying {(s, s'). cstate_relation s s'} True False R P Q dspec_f ac_f" 285 using ccorres ret pre unfolding ac_def ccorres_to_corres_pre_def 286 by (fastforce simp: unif_rrel_def corres_underlying_def ccorres_underlying_def rf_sr_def 287 intro: EHOther dest: in_AC_call_simpl) 288 289text \<open> 290If we are willing to prove termination of the C code, we can obtain a rule which can be used 291with or without the AutoCorres no_c_termination setting, and which is strong enough to prove 292goals obtained from @{thm corres_to_ccorres}. 293\<close> 294 295lemma ccorres_to_corres_with_termination: 296 assumes rf_sr_def: "rf_sr \<equiv> {(s,s'). cstate_relation s (globals s')}" 297 assumes ac_def: "ac_f \<equiv> AC_call_L1 G globals ret_xf (L1_call_simpl check_term \<Gamma> f_'proc)" 298 assumes ccorres: "ccorresG rf_sr \<Gamma> R' ret_xf' P Q' [] dspec_f (Call f_'proc)" 299 assumes pre: "\<And>s'. G s' \<Longrightarrow> ccorres_to_corres_pre Q \<top> Q' s'" 300 assumes ret: "\<And>r s'. R r (ret_xf s') \<longleftrightarrow> R' r (ret_xf' s')" 301 assumes terminates: 302 "\<And>s s'. \<lbrakk> cstate_relation s (globals s'); P s; \<not> snd (dspec_f s); G s' \<rbrakk> \<Longrightarrow> 303 \<Gamma> \<turnstile> Call f_'proc \<down> Normal s'" 304 shows "corres_underlying {(s, s'). cstate_relation s s'} True True R P Q dspec_f ac_f" 305 using ccorres ret pre unfolding ac_def ccorres_to_corres_pre_def 306 apply (clarsimp simp: corres_underlying_def ccorres_underlying_def rf_sr_def) 307 apply (rule conjI) 308 apply (fastforce simp: unif_rrel_def intro: EHOther dest: in_AC_call_simpl) 309 apply (clarsimp simp: AC_call_L1_def L2_call_L1_def L1_call_simpl_def) 310 apply (cases check_term; 311 clarsimp simp: select_f_def select_def snd_bind snd_assert get_def 312 split: sum.splits prod.splits) 313 apply (erule impE, blast intro: terminates) 314 apply (erule disjE) 315 apply (monad_eq split: xstate.splits sum.splits) 316 apply (drule EHOther, fastforce) 317 apply blast 318 apply (drule EHOther, fastforce) 319 apply blast 320 apply (monad_eq split: xstate.splits) 321 apply (fastforce dest: EHAbrupt[OF _ EHEmpty]) 322 apply (monad_eq split: xstate.splits sum.splits) 323 apply (drule EHOther, fastforce) 324 apply blast 325 apply (drule EHOther, fastforce) 326 apply blast 327 apply (monad_eq split: xstate.splits) 328 apply (fastforce dest: EHAbrupt[OF _ EHEmpty]) 329 done 330 331text \<open> 332When using AutoCorres with the no_c_termination setting, we need not prove termination 333of the C code. 334\<close> 335 336lemma ccorres_to_corres_no_termination: 337 assumes rf_sr_def: "rf_sr \<equiv> {(s,s'). cstate_relation s (globals s')}" 338 assumes ac_def: "ac_f \<equiv> AC_call_L1 G globals ret_xf (L1_call_simpl False \<Gamma> f_'proc)" 339 assumes ccorres: "ccorresG rf_sr \<Gamma> R' ret_xf' P Q' [] dspec_f (Call f_'proc)" 340 assumes pre: "\<And>s'. G s' \<Longrightarrow> ccorres_to_corres_pre Q \<top> Q' s'" 341 assumes ret: "\<And>r s'. R r (ret_xf s') \<longleftrightarrow> R' r (ret_xf' s')" 342 shows "corres_underlying {(s, s'). cstate_relation s s'} True True R P Q dspec_f ac_f" 343 using ccorres ret pre unfolding ac_def ccorres_to_corres_pre_def 344 apply (clarsimp simp: ac_def corres_underlying_def ccorres_underlying_def rf_sr_def) 345 apply (rule conjI) 346 apply (fastforce simp: unif_rrel_def intro: EHOther dest: in_AC_call_simpl) 347 apply (clarsimp simp: AC_call_L1_def L2_call_L1_def L1_call_simpl_def) 348 apply (clarsimp simp: select_f_def select_def snd_bind snd_assert get_def 349 split: sum.splits prod.splits) 350 apply (monad_eq split: xstate.splits sum.splits) 351 apply (drule EHOther, fastforce) 352 apply blast 353 apply (drule EHOther, fastforce) 354 apply blast 355 apply (monad_eq split: xstate.splits) 356 apply (fastforce dest: EHAbrupt[OF _ EHEmpty]) 357 done 358 359section \<open>Proof automation\<close> 360 361text \<open> 362We now provide ML functions for constructing simple proof automation tools. 363 364The first implements a method which converts a @{term ccorresG} goal into a 365@{term corres_underlying} goal, using @{thm corres_to_ccorres}, and automatically 366solving some subgoals. In some cases, it will also guess an appropriate return-value 367relation. 368 369The second is an attribute which converts a @{term ccorresG} fact into a 370@{term corres_underlying} fact. 371 372The setup functions are parameterised over a state relation. We instantiate them 373for the C kernel below. 374\<close> 375 376ML \<open> 377signature AUTOCORRES_CREFINE = sig 378 val setup_ac_init : thm -> (Proof.context -> Proof.method) context_parser 379 val setup_ac_attr : thm -> attribute context_parser 380end 381 382structure AutoCorresCRefine : AUTOCORRES_CREFINE = struct 383 384 fun proc_base_name termerr qualified_'proc_name = 385 unsuffix "_'proc" (List.last (Long_Name.explode qualified_'proc_name)) 386 handle Empty => raise termerr "empty proc name" 387 handle Fail _ => raise termerr "not a _'proc" 388 389 fun get_call_'proc_name termerr c = case c of 390 Const (@{const_name Call}, _) $ Const (qualified_'proc_name, _) => qualified_'proc_name 391 | _ => raise termerr "not a Call" 392 393 fun match_ccorres_term termerr ccorres_term = case ccorres_term of 394 @{term Trueprop} $ 395 (Const (@{const_name ccorres_underlying}, _) 396 $ _ $ c_Gamma $ c_rel $ c_xf $ a_rel $ a_xf $ _ $ _ $ c_hs $ _ $ c_c) => 397 let 398 val _ = if c_rel = a_rel orelse c_xf = a_xf then () 399 else raise termerr "not a ccorres goal" 400 in 401 { c_Gamma=c_Gamma, c_rel=c_rel, c_xf=c_xf, c_hs=c_hs, c_c=c_c } 402 end 403 | _ => raise termerr "not a ccorres goal" 404 405 fun match_ac_corres_term ac_corres_fact_name ac_corres_term = case ac_corres_term of 406 @{term Trueprop} $ (Const (@{const_name ac_corres}, _) 407 $ _ $ _ $ ac_Gamma $ ac_xf $ _ $ (Const (@{const_name liftE}, _) $ _) $ ac_c) 408 => { ac_Gamma=ac_Gamma, ac_xf=ac_xf, ac_c=ac_c } 409 | _ => error ("ac_init_tac: " ^ ac_corres_fact_name ^ " not an ac_corres fact") 410 411 fun match_ac_wrap_term ac_wrap_name ac_wrap_term = case ac_wrap_term of 412 Const (@{const_name Pure.eq}, _) $ _ 413 $ (Const (@{const_name AC_call_L1}, _) $ _ $ Const (@{const_name globals}, _) $ ac_xf 414 $ (Const (@{const_name L1_call_simpl}, _) $ check_term $ ac_Gamma 415 $ (Const (ac_proc_name, _)))) 416 => { ac_Gamma=ac_Gamma, ac_xf=ac_xf, check_term=check_term, ac_proc_name=ac_proc_name } 417 | _ => error ("ac_attr: " ^ ac_wrap_name ^ " wasn't in the expected form") 418 419 fun auto_rv_relation ctxt mk_imp ac_xf c_rel c_xf = 420 let 421 (* Find the types of return-value relations and extraction functions. *) 422 val ccorres_xf_ty = fastype_of c_xf 423 val c_state_ty = case ccorres_xf_ty of 424 Type("fun", [st_ty, _]) => st_ty 425 | _ => raise TYPE ("ac_init_tac'", [ccorres_xf_ty], [c_xf]) 426 val ac_corres_xf_ty = fastype_of ac_xf 427 val ac_corres_ret_ty = case ac_corres_xf_ty of 428 Type("fun", [_, acr_ty]) => acr_ty 429 | _ => raise TYPE ("ac_init_tac'", [ac_corres_xf_ty], [ac_xf]) 430 val ccorres_rrel_ty = fastype_of c_rel 431 val abstract_ret_ty = case ccorres_rrel_ty of 432 Type("fun", [ar_ty, Type("fun", [_, @{typ bool}])]) => ar_ty 433 | _ => raise TYPE("ac_init_tac'", [ccorres_rrel_ty], [c_rel]) 434 val ac_corres_rrel_ty = abstract_ret_ty --> ac_corres_ret_ty --> @{typ bool} 435 436 (* A function for building implications between return-value relations, 437 of the form used in corres_to_ccorres. *) 438 fun mk_rv_prop rv_rel = 439 let 440 val r_var = Free ("r", abstract_ret_ty) 441 val state_var = Free ("s'", c_state_ty) 442 fun mk_rel r xf = r $ r_var $ (xf $ state_var) 443 val assm = mk_rel rv_rel ac_xf 444 val conc = mk_rel c_rel c_xf 445 val prop = HOLogic.mk_Trueprop (mk_imp (assm, conc)) 446 in 447 Logic.all r_var (Logic.all state_var prop) 448 end 449 450 (* Try two strategies for guessing a simple return-value relation, 451 and proving a corresponding implication: 452 - If dc works, use that. 453 - If the types allow us to reuse the relation we were given, try that. *) 454 fun first _ [] = NONE 455 | first f (x::xs) = (if f x then SOME x else first f xs) 456 fun prove_rv rv_rel = 457 (Goal.prove ctxt [] [] (mk_rv_prop rv_rel) (fn _ => full_simp_tac ctxt 1); true) 458 handle ERROR _ => false 459 in 460 first prove_rv [Const (@{const_name dc}, ac_corres_rrel_ty), c_rel] 461 |> Option.map (Thm.cterm_of ctxt) 462 end 463 464 fun ac_init_tac corres_to_ccorres corres_to_ccorres_rv_spec ctxt (insts, fixes) ccorres_goal_t = 465 let 466 fun termerr msg = TERM ("ac_init_tac: " ^ msg, [ccorres_goal_t]) 467 468 (* Find the arguments to ccorres in the goal. *) 469 val { c_Gamma, c_rel, c_xf, c_hs, c_c } = match_ccorres_term termerr ccorres_goal_t 470 val proc_name = proc_base_name termerr (get_call_'proc_name termerr c_c) 471 472 (* Check that the handler stack is empty. *) 473 val _ = case c_hs of Const (@{const_name Nil}, _) => () 474 | _ => raise termerr "non-empty handler stack" 475 476 (* Find the AutoCorres-generated fact for that procedure. *) 477 val ac_corres_fact_name = proc_name ^ "'_ac_corres" 478 val ac_corres_fact = Proof_Context.get_thm ctxt ac_corres_fact_name 479 handle ERROR msg => error ("ac_init_tac: " ^ msg) 480 481 (* Find the arguments to ac_corres in the AutoCorres-generated fact. *) 482 val { ac_Gamma, ac_xf, ac_c } = 483 match_ac_corres_term ac_corres_fact_name (Thm.prop_of ac_corres_fact) 484 485 (* Check that AutoCorres-generated fact is as expected. *) 486 val _ = if ac_c = c_c andalso c_Gamma = ac_Gamma then () 487 else error ("ac_init_tac: " ^ ac_corres_fact_name ^ " unexpected fact") 488 489 fun corres_to_ccorres_inst rv_rel = 490 Drule.infer_instantiate ctxt [(("R",0), rv_rel)] corres_to_ccorres 491 492 val auto_rv_relation_tac = 493 case auto_rv_relation ctxt HOLogic.mk_imp ac_xf c_rel c_xf of 494 SOME rv_rel => 495 resolve_tac ctxt [corres_to_ccorres_inst rv_rel] 1 THEN 496 resolve_tac ctxt [ac_corres_fact] 1 THEN 497 SOLVED' (full_simp_tac ctxt) 4 THEN 498 TRY (SOLVED' (full_simp_tac ctxt) 3) 499 | NONE => 500 resolve_tac ctxt [corres_to_ccorres_rv_spec] 1 THEN 501 resolve_tac ctxt [ac_corres_fact] 1 THEN 502 TRY (SOLVED' (full_simp_tac ctxt) 3) 503 504 fun spec_rv_relation_tac thm = 505 let 506 val init_thm = (ac_corres_fact RS corres_to_ccorres) RS thm 507 val inst_thm = Rule_Insts.where_rule ctxt insts fixes init_thm 508 val tac = 509 TRY (SOLVED' (full_simp_tac ctxt) 4) THEN 510 TRY (SOLVED' (full_simp_tac ctxt) 3) 511 in 512 tac inst_thm 513 end 514 in 515 if null insts andalso null fixes 516 then auto_rv_relation_tac 517 else spec_rv_relation_tac 518 end 519 520 fun ac_attr conv_with_term conv_no_term gen_ctxt insts fixes ccorres_thm = 521 let 522 val ctxt = Context.proof_of gen_ctxt 523 val ccorres_t = Thm.prop_of ccorres_thm 524 525 fun termerr msg = TERM ("ac_attr: " ^ msg, [ccorres_t]) 526 527 (* Find the arguments to ccorres in the given fact. *) 528 val { c_Gamma, c_rel, c_xf, c_c, ... } = match_ccorres_term termerr ccorres_t 529 530 val qualified_'proc_name = get_call_'proc_name termerr c_c 531 val proc_name = proc_base_name termerr qualified_'proc_name 532 533 (* Find the AutoCorres-generated wrapper, and extract relevant arguments. *) 534 val ac_wrap_name = proc_name ^ "'_def" 535 val ac_wrap_def = Proof_Context.get_thm ctxt ac_wrap_name 536 handle ERROR msg => error ("ac_attr: " ^ msg) 537 538 val { ac_Gamma, ac_xf, check_term, ac_proc_name } = 539 match_ac_wrap_term ac_wrap_name (Thm.prop_of ac_wrap_def) 540 541 (* Check that AutoCorres-generated wrapper is as expected. *) 542 val _ = if ac_proc_name = qualified_'proc_name andalso ac_Gamma = c_Gamma then () 543 else error ("ac_attr: " ^ ac_wrap_name ^ " wasn't in the expected form") 544 545 val ccorres_to_corres = case check_term of 546 @{term False} => conv_no_term | _ => conv_with_term 547 548 fun ccorres_to_corres_inst rv_rel = 549 Drule.infer_instantiate ctxt [(("R",0), rv_rel)] ccorres_to_corres 550 551 val (ccorres_to_corres', rv_tac) = 552 if null insts andalso null fixes then 553 case auto_rv_relation ctxt HOLogic.mk_eq ac_xf c_rel c_xf of 554 SOME rv_rel => (ccorres_to_corres_inst rv_rel, SOLVED' (full_simp_tac ctxt) 2) 555 | NONE => (ccorres_to_corres, all_tac) 556 else (Rule_Insts.where_rule ctxt insts fixes ccorres_to_corres, all_tac) 557 558 val ac_corres_init_thm = ccorres_thm RS (ac_wrap_def RS ccorres_to_corres') 559 560 val ccorres_to_corres_pre_process_tac = Method.NO_CONTEXT_TACTIC ctxt 561 (Method_Closure.apply_method ctxt @{method ccorres_to_corres_pre_process} 562 [] [] [] ctxt []) 563 564 val tac = rv_tac THEN ccorres_to_corres_pre_process_tac 565 in 566 Seq.hd (tac ac_corres_init_thm) |> asm_full_simplify ctxt 567 end 568 569 val where_for_parser = 570 Scan.lift 571 (Scan.optional 572 (Args.$$$ "where" |-- 573 Parse.and_list 574 (Parse.position Args.var -- (Args.$$$ "=" |-- Parse.!!! Args.embedded_inner_syntax)) 575 -- Parse.for_fixes) 576 ([],[])) 577 578 fun setup_ac_init rf_sr_def = 579 let 580 val corres_to_ccorres = rf_sr_def RS @{thm corres_to_ccorres} 581 val corres_to_ccorres_rv_spec = rf_sr_def RS @{thm corres_to_ccorres_rv_spec} 582 val tac = ac_init_tac corres_to_ccorres corres_to_ccorres_rv_spec 583 in 584 where_for_parser >> 585 (fn args => fn ctxt => fn facts => 586 SIMPLE_METHOD (SUBGOAL (tac ctxt args o #1) 1) facts) 587 end 588 589 fun setup_ac_attr rf_sr_def = 590 let 591 val conv_with_term = rf_sr_def RS @{thm ccorres_to_corres_with_termination} 592 val conv_no_term = rf_sr_def RS @{thm ccorres_to_corres_no_termination} 593 in 594 where_for_parser >> 595 (fn (insts, fixes) => fn (ctxt, ccorres_thm) => 596 (NONE, SOME (ac_attr conv_with_term conv_no_term ctxt insts fixes ccorres_thm))) 597 end 598end 599\<close> 600 601section \<open>Kernel instantiation\<close> 602 603text \<open>Here, we instantiate the proof automation for the C kernel.\<close> 604 605context kernel begin 606 607method_setup ac_init = \<open>AutoCorresCRefine.setup_ac_init @{thm rf_sr_def}\<close> 608attribute_setup ac = \<open>AutoCorresCRefine.setup_ac_attr @{thm rf_sr_def}\<close> 609 610text \<open> 611FIXME: It would be nice to have an abbreviation for the @{term corres_underlying} relation 612that comes out of @{method ac_init}. Unfortunately, this causes renumbering of metavariables 613produced in resolution, breaking many proofs, so we avoid this for now. 614\<close> 615(* abbreviation "corres_ac \<equiv> corres_underlying {(s, s'). cstate_relation s s'} True True" *) 616 617end 618 619section \<open>Experiments with transferring bitfield proofs\<close> 620 621text \<open>Generic transfer rules\<close> 622lemma autocorres_transfer_spec: 623 assumes ac_def: 624 "ac_f \<equiv> AC_call_L1 arg_rel globals ret_xf (L1_call_simpl check_termination \<Gamma> f_'proc)" 625 assumes c_spec: 626 "\<forall>s0. \<Gamma>\<turnstile> (Collect (\<lambda>s. s0 = s \<and> P s)) Call f_'proc (Collect (Q s0))" 627 assumes precond_deps: 628 "\<And>s t. \<lbrakk> arg_rel s; arg_rel t; globals s = globals t \<rbrakk> \<Longrightarrow> P s = P t" 629 assumes postcond_deps: 630 "\<And>s0 s0' s t. \<lbrakk> arg_rel s0; arg_rel s0'; globals s0 = globals s0'; 631 ret_xf s = ret_xf t; globals s = globals t \<rbrakk> \<Longrightarrow> Q s0 s = Q s0' t" 632 shows "\<lbrace>\<lambda>s. P cs \<and> s = globals cs \<and> arg_rel cs \<rbrace> 633 ac_f 634 \<lbrace>\<lambda>r s'. \<exists>cs'. s' = globals cs' \<and> r = ret_xf cs' \<and> Q cs cs' \<rbrace>" 635 apply (clarsimp simp: valid_def ac_def AC_call_L1_def L2_call_L1_def L1_call_simpl_def 636 in_monad' in_liftM select_f_def in_select in_fail 637 split: sum.splits xstate.splits) 638 apply (rename_tac r', case_tac r'; clarsimp) 639 apply (rename_tac xst, case_tac xst; clarsimp) 640 apply (drule_tac ?s0.1=s in exec_normal[OF _ _ c_spec[rule_format], rotated]) 641 apply (blast dest: precond_deps) 642 apply (blast dest: postcond_deps) 643 done 644 645text \<open>This one is probably more useful\<close> 646lemma autocorres_transfer_spec_no_modifies: 647 assumes ac_def: 648 "ac_f \<equiv> AC_call_L1 arg_rel globals ret_xf (L1_call_simpl check_termination \<Gamma> f_'proc)" 649 assumes c_spec: 650 "\<forall>s0. hoarep \<Gamma> {} {} (P' s0) (Call f_'proc) (Collect (Q s0)) A" \<comment> \<open>syntax parser barfs...\<close> 651 assumes c_modifies: 652 "\<forall>\<sigma>. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {\<sigma>} Call f_'proc {t. t may_not_modify_globals \<sigma>}" 653 assumes c_spec_unify: 654 "\<And>s0. P' s0 = {s. s0 = s \<and> P s}" 655 assumes precond_deps: 656 "\<And>s0 s t. \<lbrakk> arg_rel s; arg_rel t; globals s = globals t \<rbrakk> \<Longrightarrow> P s = P t" 657 assumes postcond_deps: 658 "\<And>s0 s0' s t. \<lbrakk> arg_rel s0; arg_rel s0'; globals s0 = globals s0'; 659 ret_xf s = ret_xf t; globals s = globals t \<rbrakk> \<Longrightarrow> Q s0 s = Q s0' t" 660 shows "\<lbrace>\<lambda>s. s = globals cs \<and> P cs \<and> arg_rel cs \<rbrace> 661 ac_f 662 \<lbrace>\<lambda>r s'. s' = globals cs \<and> (\<exists>cs'. r = ret_xf cs' \<and> Q cs cs') \<rbrace>" 663 apply (clarsimp simp: valid_def ac_def AC_call_L1_def L2_call_L1_def L1_call_simpl_def 664 in_monad' in_liftM select_f_def in_select in_fail 665 split: sum.splits xstate.splits) 666 apply (rename_tac r', case_tac r'; clarsimp) 667 apply (rename_tac xst, case_tac xst; clarsimp) 668 apply (frule_tac ?s0.1=s in exec_normal[OF _ _ c_spec[rule_format], rotated]) 669 apply (clarsimp simp: c_spec_unify) 670 apply (blast dest: precond_deps) 671 apply (frule exec_normal[OF singletonI _ c_modifies[rule_format]]) 672 apply (clarsimp simp: meq_def) 673 apply (blast dest: postcond_deps) 674 done 675 676subsection \<open>Helpers\<close> 677 678lemma All_to_all': 679 "(\<forall>x. P x) \<Longrightarrow> (\<And>x. P x)" 680 by simp 681 682text \<open> 683 Convert references to global or local state variables, to the opposite one. 684 FIXME: surely this has been proven already. 685\<close> 686lemma collect_lift: 687 "Collect (\<lambda>s. s0 = s \<and> f s) = Collect (\<lambda>s. s0 = s \<and> f s0)" 688 by blast 689lemma collect_unlift: 690 "Collect (\<lambda>s. s0 = s \<and> f s0 s) = Collect (\<lambda>s. s0 = s \<and> f s s)" 691 by blast 692 693 694subsection \<open>Experiment with wrapping specs\<close> 695lemma exec_no_fault: 696 assumes asms: "s \<in> P" 697 and ce: "Gamma \<turnstile> \<langle>c, Normal s\<rangle> \<Rightarrow> Fault f" 698 and valid: "Gamma \<turnstile> P c Q, A" 699 shows "False" 700 using valid ce asms 701 apply - 702 apply (frule hoare_sound) 703 apply (clarsimp simp: NonDetMonad.bind_def cvalid_def split_def HoarePartialDef.valid_def) 704 apply (drule spec, drule spec, drule (1) mp) 705 apply auto 706 done 707 708lemma exec_no_stuck: 709 assumes asms: "s \<in> P" 710 and ce: "Gamma \<turnstile> \<langle>c, Normal s\<rangle> \<Rightarrow> Stuck" 711 and valid: "Gamma \<turnstile> P c Q, A" 712 shows "False" 713 using valid ce asms 714 apply - 715 apply (frule hoare_sound) 716 apply (clarsimp simp: NonDetMonad.bind_def cvalid_def split_def HoarePartialDef.valid_def) 717 apply (drule spec, drule spec, drule (1) mp) 718 apply auto 719 done 720 721definition L1_call_simpl_spec where 722 "L1_call_simpl_spec check_term Gamma proc precond postcond = 723 L1_spec (Collect (\<lambda>(s, t). precond s s \<and> postcond s t))" 724 725lemma L1corres_call_simpl_spec: 726 "\<lbrakk> \<forall>s0. Gamma\<turnstile> (Collect (precond s0)) (Call proc) (Collect (postcond s0)); 727 \<And>s. ct \<Longrightarrow> Gamma\<turnstile>Call proc \<down> Normal s \<rbrakk> \<Longrightarrow> 728 L1corres ct Gamma (L1_call_simpl_spec ct Gamma proc precond postcond) (Call proc)" 729 apply (clarsimp simp: L1corres_def L1_call_simpl_spec_def L1_defs 730 assert_def snd_select snd_liftE snd_spec 731 in_monad' in_spec 732 split: xstate.splits) 733 apply (case_tac t) 734 apply (blast dest: exec_normal[rotated]) 735 apply (blast dest: exec_abrupt[rotated]) 736 apply (blast intro: exec_no_fault[rotated]) 737 apply (blast intro: exec_no_stuck[rotated]) 738 done 739 740 741section \<open>Termination proofs\<close> 742text \<open> 743 Proving termination side conditions for @{thm ccorres_to_corres_with_termination}. 744 745 To begin with, we can automatically prove terminates for most 746 helper functions as they do not have recursion or loops. 747\<close> 748 749named_theorems terminates_trivial 750 751method_setup terminates_setup = \<open> 752 let 753 fun tac ctxt goal_t = 754 case Logic.strip_assums_concl goal_t of 755 @{term_pat "Trueprop (_ \<turnstile> Call ?f_'proc \<down> _)"} => 756 let 757 val f = dest_Const f_'proc |> fst |> Long_Name.base_name |> unsuffix "_'proc"; 758 val impl = Proof_Context.get_thm ctxt (f ^ "_impl"); 759 val body = Proof_Context.get_thm ctxt (f ^ "_body_def"); 760 in 761 EVERY [ 762 resolve_tac ctxt @{thms terminates.Call} 1, 763 resolve_tac ctxt [impl] 1, 764 simp_tac (ctxt addsimps (body :: @{thms return_C_def lvar_nondet_init_def})) 1 765 ] 766 end 767 in 768 Scan.succeed (fn ctxt => Method.SIMPLE_METHOD (SUBGOAL (tac ctxt o #1) 1)) 769 end 770\<close> 771 772method terminates_trivial declares terminates_trivial = 773 (terminates_setup; intro terminates_trivial) 774 775lemma [terminates_trivial]: 776 "\<lbrakk> \<And>s. \<Gamma> \<turnstile> c \<down> Normal s \<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> Guard F G c \<down> Normal s" 777 apply (blast intro: terminates.Guard terminates.GuardFault) 778 done 779lemma [terminates_trivial]: 780 "\<lbrakk> \<And>s. \<Gamma> \<turnstile> c1 \<down> Normal s; \<And>s. \<Gamma> \<turnstile> c2 \<down> Normal s \<rbrakk> \<Longrightarrow> 781 \<Gamma> \<turnstile> Cond C c1 c2 \<down> Normal s" 782 apply (blast intro: terminates.CondTrue terminates.CondFalse) 783 done 784lemma [terminates_trivial]: 785 "\<lbrakk> \<Gamma> \<turnstile> c1 \<down> Normal s; \<And>s. \<Gamma> \<turnstile> c2 \<down> Normal s \<rbrakk> \<Longrightarrow> 786 \<Gamma> \<turnstile> c1;;c2 \<down> Normal s" 787 apply (erule terminates.Seq) 788 apply clarsimp 789 apply (case_tac s'; auto) 790 done 791 792lemma [terminates_trivial]: 793 fixes \<Gamma> return init shows 794 "\<lbrakk> \<And>s. \<Gamma> \<turnstile> Call p \<down> Normal s; \<And>s t u. \<Gamma> \<turnstile> c s t \<down> Normal u \<rbrakk> \<Longrightarrow> 795 \<Gamma> \<turnstile> call init p return c \<down> Normal s" 796 apply (case_tac "\<Gamma> p") 797 apply (erule terminates_callUndefined) 798 apply (fastforce simp: terminates_Call_body intro: terminates_call) 799 done 800 801lemmas [terminates_trivial] = 802 terminates.Basic 803 terminates.Catch[rule_format] 804 terminates.Throw 805 terminates.Skip 806 terminates.Spec 807 808section \<open>Additional infrastructure\<close> 809 810(* FIXME: Needs reorganisation. Much of the following should be moved elsewhere. *) 811 812context kernel begin 813 814lemma wpc_helper_corres_final: 815 "corres_underlying sr nf nf' rv Q Q' f f' 816 \<Longrightarrow> wpc_helper (P, P') (Q, {s. Q' s}) (corres_underlying sr nf nf' rv P (\<lambda>s. s \<in> P') f f')" 817 apply (clarsimp simp: wpc_helper_def) 818 apply (erule corres_guard_imp) 819 apply auto 820 done 821 822wpc_setup "\<lambda>m. corres_underlying sr nf nf' rv P P' m f'" wpc_helper_corres_final 823wpc_setup "\<lambda>m. corres_underlying sr nf nf' rv P P' (m >>= f) f'" wpc_helper_corres_final 824 825lemma condition_const: "condition (\<lambda>_. P) L R = (if P then L else R)" 826 by (simp add: condition_def split: if_splits) 827 828definition 829 errglobals :: "globals \<Rightarrow> errtype" 830where 831 "errglobals s \<equiv> \<lparr> errfault = seL4_Fault_lift (current_fault_' s), 832 errlookup_fault = lookup_fault_lift (current_lookup_fault_' s), 833 errsyscall = current_syscall_error_' s \<rparr>" 834 835lemma errstate_errglobals: 836 "errstate s' = errglobals (globals s')" 837 by (auto simp: errstate_def errglobals_def) 838 839lemma errglobals_simps [simp]: 840 "errfault (errglobals s) = seL4_Fault_lift (current_fault_' s)" 841 "errlookup_fault (errglobals s) = lookup_fault_lift (current_lookup_fault_' s)" 842 "errsyscall (errglobals s) = current_syscall_error_' s" 843 by (auto simp: errglobals_def) 844 845definition 846 "lift_rv ef vf elf R E \<equiv> 847 \<lambda>r (r',e'). (case r of Inl e \<Rightarrow> ef r' \<noteq> scast EXCEPTION_NONE \<and> E e (ef r') (elf e') 848 | Inr v \<Rightarrow> ef r' = scast EXCEPTION_NONE \<and> R v (vf r'))" 849 850(* FIXME: provide a way to use this rule (and derived versions below) in ac_init. *) 851lemma corres_to_ccorres_rv_spec_liftxf: 852 assumes ac: "ac_corres globals check_term \<Gamma> ret_xf G (liftE ac) c" 853 assumes cu: 854 "corres_underlying 855 {(s,s'). cstate_relation s s'} True True (lift_rv ef vf elf R' E) 856 P Q a (do r' \<leftarrow> ac; e' \<leftarrow> gets exf; return (r',e') od)" 857 assumes "\<And>s'. esf (errstate s') = elf (exf (globals s'))" 858 assumes "\<And>e f e'. E' e f e' = E e f (esf e')" 859 assumes "\<And>s s'. cstate_relation s (globals s') \<Longrightarrow> P' s \<and> s' \<in> Q' \<Longrightarrow> P s \<and> Q (globals s')" 860 assumes "\<And>s s'. cstate_relation s (globals s') \<Longrightarrow> P' s \<and> s' \<in> Q' \<Longrightarrow> G s'" 861 shows "ccorres (E' \<currency> R') (liftxf errstate ef vf ret_xf) P' Q' [] a c" 862 apply (rule corres_to_ccorres_extra_globals_rv_spec[OF _ _ corres_rel_imp, OF rf_sr_def ac cu]) 863 apply (all \<open>clarsimp simp: assms(5-6) liftxf_def\<close>) 864 apply (clarsimp simp: lift_rv_def liftxf_def assms(3-4) split: sum.splits) 865 done 866 867lemmas corres_to_ccorres_rv_spec_errglobals = 868 corres_to_ccorres_rv_spec_liftxf 869 [where elf="\<lambda>e. e" and esf="\<lambda>e. e" and E=E' for E', OF _ _ errstate_errglobals] 870 871lemmas corres_to_ccorres_rv_spec_current_fault = 872 corres_to_ccorres_rv_spec_liftxf 873 [where elf=seL4_Fault_lift and esf=errfault, OF _ _ errfault_errstate] 874 875lemmas corres_to_ccorres_rv_spec_current_lookup_fault = 876 corres_to_ccorres_rv_spec_liftxf 877 [where elf=lookup_fault_lift and esf=errlookup_fault, OF _ _ errlookup_fault_errstate] 878 879lemmas corres_to_ccorres_rv_spec_current_syscall_error = 880 corres_to_ccorres_rv_spec_liftxf 881 [where elf="\<lambda>e. e" and esf=errsyscall, OF _ _ errsyscall_errstate] 882 883lemma lift_rv_returnOk: 884 assumes "ef r = scast EXCEPTION_NONE" 885 assumes "R rv (vf r)" 886 shows "corres_underlying 887 {(x, y). cstate_relation x y} True True (lift_rv ef vf elf R E) \<top> \<top> 888 (returnOk rv) 889 (do e' \<leftarrow> gets exf; return (r, e') od)" 890 apply (clarsimp simp: corres_underlying_def snd_bind snd_modify snd_gets in_monad) 891 apply (rule bexI[of _ "(Inr rv, s)" for s]; simp add: in_monad lift_rv_def assms) 892 done 893 894lemma lift_rv_throwError': 895 assumes "\<And>s s'. cstate_relation s s' \<longrightarrow> cstate_relation s (esu s')" 896 assumes "ef r \<noteq> scast EXCEPTION_NONE" 897 assumes "\<And>err'. E err (ef r) (elf (exf (esu err')))" 898 shows "corres_underlying 899 {(x, y). cstate_relation x y} True True (lift_rv ef vf elf R E) \<top> \<top> 900 (throwError err) 901 (do _ \<leftarrow> modify esu; e' \<leftarrow> gets exf; return (r, e') od)" 902 apply (clarsimp simp: corres_underlying_def snd_bind snd_modify snd_gets in_monad) 903 apply (rule bexI[of _ "(Inl err, s)" for s]; simp add: in_monad lift_rv_def assms) 904 done 905 906lemma cstate_relation_errglobals_updates: 907 "cstate_relation s s' \<longrightarrow> cstate_relation s (current_fault_'_update f s')" 908 "cstate_relation s s' \<longrightarrow> cstate_relation s (current_lookup_fault_'_update lf s')" 909 "cstate_relation s s' \<longrightarrow> cstate_relation s (current_syscall_error_'_update sce s')" 910 by (auto simp: cstate_relation_def carch_state_relation_def cmachine_state_relation_def) 911 912lemmas lift_rv_throwError = 913 cstate_relation_errglobals_updates[THEN lift_rv_throwError'] 914 915lemma valid_spec_to_wp: 916 assumes "\<And>\<sigma>. \<lbrace> \<lambda>s. s = \<sigma> \<and> P s \<rbrace> f \<lbrace> \<lambda>r s. s = \<sigma> \<and> R r s \<rbrace>" 917 shows "\<lbrace> \<lambda>s. P s \<and> (\<forall>r. R r s \<longrightarrow> Q r s) \<rbrace> f \<lbrace> Q \<rbrace>" 918 using assms by (fastforce simp: valid_def) 919 920lemmas valid_spec_to_wp' = valid_spec_to_wp[where P=\<top>, simplified] 921 922lemma spec_result_Normal: 923 fixes \<Gamma> 924 assumes p_spec: "\<forall>s. \<Gamma>,{} \<turnstile> {s'. s = s' \<and> P s s'} p (Q s)" 925 shows "\<forall>s t. P s s \<longrightarrow> \<Gamma> \<turnstile> \<langle>p, Normal s\<rangle> \<Rightarrow> t \<longrightarrow> t \<in> range Normal" 926 by (rule all_forward[OF p_spec], drule hoare_sound) 927 (auto simp: cvalid_def HoarePartialDef.valid_def image_def) 928 929lemma terminates_spec_no_fail: 930 fixes \<Gamma> 931 assumes ac: "ac \<equiv> AC_call_L1 arg_rel globals ret_xf (L1_call_simpl check_termination \<Gamma> f_'proc)" 932 assumes p_spec: "\<forall>s. \<Gamma>,{} \<turnstile> {s'. s = s' \<and> P s s'} (Call f_'proc) (Q s)" 933 assumes terminates: "\<forall>s. P s s \<longrightarrow> \<Gamma> \<turnstile> Call f_'proc \<down> Normal s" 934 assumes nf_pre: "\<And>s. N (globals s) \<Longrightarrow> arg_rel s \<Longrightarrow> P s s" 935 shows "no_fail N ac" 936 proof - 937 have normal: "\<forall>s t. P s s \<longrightarrow> \<Gamma> \<turnstile> \<langle>Call f_'proc, Normal s\<rangle> \<Rightarrow> t \<longrightarrow> t \<in> range Normal" 938 using spec_result_Normal p_spec by simp 939 have L1_call_simpl_no_fail: 940 "no_fail (\<lambda>s. P s s) (L1_call_simpl check_termination \<Gamma> f_'proc)" 941 apply (wpsimp simp: L1_call_simpl_def wp: non_fail_select select_wp) 942 using terminates normal by auto 943 have select_f_L1_call_simpl_no_fail: 944 "\<And>s. no_fail (\<lambda>_. P s s) (select_f (L1_call_simpl check_termination \<Gamma> f_'proc s))" 945 using L1_call_simpl_no_fail[unfolded no_fail_def] 946 by wpsimp 947 have select_f_L1_call_simpl_rv: 948 "\<And>s. \<lbrace>\<lambda>_. P s s\<rbrace> select_f (L1_call_simpl check_termination \<Gamma> f_'proc s) \<lbrace>\<lambda>r s. fst r = Inr ()\<rbrace>" 949 apply (wp, clarsimp simp: L1_call_simpl_def in_monad in_select split: xstate.splits) 950 apply (match premises in "s \<noteq> Stuck" for s \<Rightarrow> \<open>cases s\<close>) 951 using normal by auto 952 show ?thesis 953 apply (clarsimp simp: ac AC_call_L1_def L2_call_L1_def) 954 apply (wpsimp wp: select_f_L1_call_simpl_no_fail non_fail_select 955 wp_del: select_f_wp) 956 apply (rule hoare_strengthen_post[OF select_f_L1_call_simpl_rv], fastforce) 957 apply (wpsimp wp: select_wp nf_pre)+ 958 done 959 qed 960 961lemmas terminates_spec_no_fail' = 962 terminates_spec_no_fail[where P="\<top>\<top>", simplified] 963 964lemma valid_spec_to_corres_symb_exec_r: 965 assumes spec': "\<And>\<sigma>. \<lbrace> \<lambda>s. s = \<sigma> \<and> P' s \<rbrace> f \<lbrace> \<lambda>r s. s = \<sigma> \<and> Q' r s \<rbrace>" 966 assumes nf: "nf' \<Longrightarrow> no_fail N' f" 967 assumes corres_rv: "\<And>rv'. corres_underlying sr nf nf' r P (R' rv') a (c rv')" 968 shows "corres_underlying sr nf nf' r P (\<lambda>s. N' s \<and> P' s \<and> (\<forall>r. Q' r s \<longrightarrow> R' r s)) a (f >>= c)" 969 by (rule corres_symb_exec_r[OF corres_rv]) 970 (wpsimp wp: valid_spec_to_wp[OF spec'] nf)+ 971 972lemma valid_spec_to_corres_gen_symb_exec_r: 973 assumes spec': "\<And>\<sigma>. \<lbrace> \<lambda>s. s = \<sigma> \<and> P' s \<rbrace> f \<lbrace> \<lambda>r s. s = \<sigma> \<and> Q' r \<rbrace>" 974 assumes nf: "nf' \<Longrightarrow> no_fail N' f" 975 assumes corres_rv: "\<And>rv'. Q' rv' \<Longrightarrow> corres_underlying sr nf nf' r P (R' rv') a (c rv')" 976 shows "corres_underlying sr nf nf' r P (\<lambda>s. N' s \<and> P' s \<and> (\<forall>r. Q' r \<longrightarrow> R' r s)) a (f >>= c)" 977 by (rule corres_symb_exec_r, rule_tac F="Q' rv" in corres_gen_asm2, erule corres_rv) 978 (wpsimp wp: valid_spec_to_wp[OF spec'] nf)+ 979 980lemmas valid_spec_to_corres_symb_exec_r' = 981 valid_spec_to_corres_symb_exec_r[where P'=\<top>, simplified] 982 983lemmas valid_spec_to_corres_gen_symb_exec_r' = 984 valid_spec_to_corres_gen_symb_exec_r[where P'=\<top>, simplified] 985 986abbreviation 987 "gslift (s :: globals) \<equiv> clift (t_hrs_' s)" 988 989abbreviation 990 "c_h_t_g_valid" :: "globals \<Rightarrow> 'a::c_type ptr \<Rightarrow> bool" ("_ \<Turnstile>\<^sub>g _" [99,99] 100) 991where 992 "s \<Turnstile>\<^sub>g p == hrs_htd (t_hrs_' s),c_guard \<Turnstile>\<^sub>t p" 993 994(* Mirrors ccorres_symb_exec_l, to get access to what's known about the abstract return value 995 in the concrete precondition. Not sure if this is necessary, or even a good idea. *) 996lemma corres_symb_exec_l'': 997 assumes corres: "\<And>rv. corres_underlying sr nf nf' r (R rv) (R' rv) (x rv) y" 998 assumes no_upd: "\<And>s. P s \<Longrightarrow> \<lbrace>(=) s\<rbrace> m \<lbrace>\<lambda>r. (=) s\<rbrace>" 999 assumes result: "\<lbrace>Q\<rbrace> m \<lbrace>R\<rbrace>" 1000 assumes nofail: "\<not> nf \<longrightarrow> no_fail P m" 1001 assumes mtfail: "empty_fail m" 1002 shows "corres_underlying sr nf nf' r 1003 (P and Q) (\<lambda>s'. \<forall>rv s. (s,s') \<in> sr \<and> R rv s \<longrightarrow> R' rv s') 1004 (m >>= (\<lambda>rv. x rv)) y" 1005 using corres unfolding corres_underlying_def 1006 apply (clarsimp; rename_tac s s') 1007 apply (subgoal_tac "\<not> snd (m s)") 1008 prefer 2 1009 using nofail 1010 apply (cases nf; clarsimp simp: no_fail_def elim!: not_snd_bindI1) 1011 apply (erule empty_fail_not_snd [OF _ mtfail, THEN exE]; clarsimp; rename_tac rv t) 1012 apply (subgoal_tac "t = s") 1013 prefer 2 1014 apply (frule use_valid, rule no_upd, simp+) 1015 apply clarsimp 1016 apply (drule_tac x=rv in spec, drule_tac x=rv in meta_spec, drule (1) bspec, simp) 1017 apply (frule use_valid, rule result, assumption) 1018 apply (drule mp, rule_tac x=s in exI, simp_all) 1019 apply (subgoal_tac "nf \<longrightarrow> \<not> snd (x rv s)") 1020 prefer 2 1021 apply (cases nf; clarsimp simp: no_fail_def elim!: not_snd_bindI2) 1022 apply (clarsimp; rename_tac fv' t') 1023 apply (drule (1) bspec; clarsimp; rename_tac fv t) 1024 apply (rule_tac x="(fv,t)" in bexI; clarsimp simp: bind_def) 1025 apply (rule bexI[rotated], assumption, simp) 1026 done 1027 1028lemma corres_stateAssert_l: 1029 assumes "corres_underlying sr nf nf' r P P' (a ()) c" 1030 shows "corres_underlying sr nf nf' r 1031 (\<lambda>s. (\<not> nf \<longrightarrow> Q s) \<and> (Q s \<longrightarrow> P s)) P' 1032 (stateAssert Q bs >>= a) c" 1033 apply (rule corres_guard_imp[OF corres_symb_exec_l''[where P="\<lambda>s. nf \<or> Q s"]]) 1034 using assms apply simp 1035 apply (wpsimp simp: stateAssert_def)+ 1036 done 1037 1038lemma corres_guard_r: 1039 assumes "corres_underlying sr nf nf' r P P' a (c ())" 1040 shows "corres_underlying sr nf nf' r P (\<lambda>s. (nf' \<longrightarrow> f s) \<and> (f s \<longrightarrow> P' s)) 1041 a (guard f >>= c)" 1042 apply (rule corres_guard_imp[OF corres_symb_exec_r'[where R'="\<lambda>s. nf' \<longrightarrow> f s"]]) 1043 using assms apply simp 1044 apply wpsimp+ 1045 done 1046 1047lemma corres_cross_over_guard: 1048 assumes "corres_underlying sr nf nf' r P P' a c" 1049 shows "corres_underlying sr nf nf' r (P and Q) (\<lambda>s'. \<forall>s. (s,s') \<in> sr \<and> Q s \<longrightarrow> P' s') a c" 1050 by (rule stronger_corres_guard_imp[OF assms]) auto 1051 1052end 1053 1054end 1055