1(* 2 * Copyright 2014, NICTA 3 * 4 * This software may be distributed and modified according to the terms of 5 * the GNU General Public License version 2. Note that NO WARRANTY is provided. 6 * See "LICENSE_GPLv2.txt" for details. 7 * 8 * @TAG(NICTA_GPL) 9 *) 10 11theory Corres_C 12imports 13 "CLib.CCorresLemmas" 14 "../$L4V_ARCH/SR_lemmas_C" 15begin 16 17abbreviation 18 "return_C \<equiv> CLanguage.creturn global_exn_var_'_update" 19lemmas return_C_def = creturn_def 20 21abbreviation 22 "return_void_C \<equiv> CLanguage.creturn_void global_exn_var_'_update" 23lemmas return_void_C_def = creturn_void_def 24 25abbreviation 26 "break_C \<equiv> CLanguage.cbreak global_exn_var_'_update" 27lemmas breakk_C_def = cbreak_def 28 29abbreviation 30 "catchbrk_C \<equiv> CLanguage.ccatchbrk global_exn_var_'" 31lemmas catchbrk_C_def = ccatchbrk_def 32 33(* This is to avoid typing this all the time \<dots> *) 34abbreviation (in kernel) 35 "modifies_spec f \<equiv> \<forall>s. \<Gamma> \<turnstile>\<^bsub>/UNIV\<^esub> {s} Call f {t. t may_not_modify_globals s}" 36 37section "Error monad" 38 39(* Dealing with THROW in a nice fashion --- it is always going to be catching break or skip at the end of the function. 40 In retrospect, if ccatchbrk is always if ... then SKIP else THROW we are OK without the globals_update thing *) 41 42definition 43 wfhandlers :: "rf_com list \<Rightarrow> bool" 44where 45 "wfhandlers hs \<equiv> \<forall>\<Gamma> s t n. global_exn_var_' s = Return 46 \<and> \<Gamma> \<turnstile>\<^sub>h \<langle>hs, s\<rangle> \<Rightarrow> (n, t) \<longrightarrow> t = Normal s" 47 48lemma wfhandlers_ccatchbrk: 49 "wfhandlers (catchbrk_C # hs) = wfhandlers hs" 50 unfolding wfhandlers_def ccatchbrk_def 51 apply rule 52 apply (intro allI impI) 53 apply (drule_tac x = \<Gamma> in spec) 54 apply ((drule spec)+, erule mp) 55 apply simp 56 apply (rule EHAbrupt) 57 apply rule 58 apply simp 59 apply rule 60 apply fastforce 61 apply (intro allI impI) 62 apply (drule_tac x = \<Gamma> in spec) 63 apply ((drule spec)+, erule mp) 64 apply simp 65 apply (erule conjE) 66 apply (erule exec_handlers.cases) 67 apply (fastforce elim: exec_Normal_elim_cases)+ 68 done 69 70lemma wfhandlers_skip: 71 "wfhandlers (SKIP # hs)" 72 unfolding wfhandlers_def 73 apply (intro allI impI) 74 apply (erule conjE) 75 apply (erule exec_handlers.cases) 76 apply (auto elim: exec_Normal_elim_cases) 77 done 78 79lemmas wfhandlers_simps [simp] = wfhandlers_skip wfhandlers_ccatchbrk 80 81lemma wfhandlersD: 82 "\<lbrakk>wfhandlers hs; \<Gamma> \<turnstile>\<^sub>h \<langle>hs, s\<rangle> \<Rightarrow> (n, t); global_exn_var_' s = Return\<rbrakk> \<Longrightarrow> t = Normal s" 83 unfolding wfhandlers_def by auto 84 85record 'b exxf = 86 exflag :: machine_word 87 exstate :: errtype 88 exvalue :: 'b 89 90definition 91 liftxf :: "(cstate \<Rightarrow> errtype) \<Rightarrow> ('a \<Rightarrow> machine_word) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> (cstate \<Rightarrow> 'a) \<Rightarrow> cstate \<Rightarrow> 'b exxf" 92 where 93 "liftxf et ef vf xf \<equiv> \<lambda>s. \<lparr> exflag = ef (xf s), exstate = et s, exvalue = vf (xf s) \<rparr>" 94 95lemma exflag_liftxf [simp]: 96 "exflag (liftxf es sf vf xf s) = sf (xf s)" 97 unfolding liftxf_def by simp 98 99lemma exstate_liftxf [simp]: 100 "exstate (liftxf es sf vf xf s) = es s" 101 unfolding liftxf_def by simp 102 103lemma exvalue_liftxf [simp]: 104 "exvalue (liftxf es sf vf xf s) = vf (xf s)" 105 unfolding liftxf_def by simp 106 107 108(* This is more or less ccorres specific, so it goes here *) 109 110primrec 111 crel_sum_comb :: "('a \<Rightarrow> machine_word \<Rightarrow> errtype \<Rightarrow> bool) \<Rightarrow> ('c \<Rightarrow> 'b \<Rightarrow> bool) 112 \<Rightarrow> ('a + 'c \<Rightarrow> 'b exxf \<Rightarrow> bool)" (infixl "\<currency>" 95) 113where 114 "(f \<currency> g) (Inr x) y = (exflag y = scast EXCEPTION_NONE \<and> g x (exvalue y))" 115| "(f \<currency> g) (Inl x) y = (exflag y \<noteq> scast EXCEPTION_NONE \<and> f x (exflag y) (exstate y))" 116 117lemma ccorres_split_nothrowE: 118 fixes R' :: "cstate set" 119 assumes ac: "ccorres_underlying sr \<Gamma> 120 (f' \<currency> r') (liftxf es ef' vf' xf') 121 (f' \<currency> r') (liftxf es ef' vf' xf') 122 P P' hs a c" 123 and ceqv: "\<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' d (d' rv')" 124 and bd: "\<And>rv rv'. \<lbrakk> r' rv (vf' rv'); ef' rv' = scast EXCEPTION_NONE \<rbrakk> 125 \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (Q rv) (Q' rv rv') hs (b rv) (d' rv')" 126 and err: "\<And>err rv' err'. \<lbrakk>ef' rv' \<noteq> scast EXCEPTION_NONE; f' err (ef' rv') err' \<rbrakk> 127 \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (QE err) (Q'' err rv' err') hs 128 (throwError err) (d' rv')" 129 and valid: "\<lbrace>R\<rbrace> a \<lbrace>Q\<rbrace>,\<lbrace>QE\<rbrace>" 130 and valid': "\<Gamma> \<turnstile>\<^bsub>/F\<^esub> R' c ({s. (ef' (xf' s) = scast EXCEPTION_NONE \<longrightarrow> (\<forall>rv. r' rv (vf' (xf' s)) \<longrightarrow> s \<in> Q' rv (xf' s))) \<and> 131 (ef' (xf' s) \<noteq> scast EXCEPTION_NONE \<longrightarrow> (\<forall>err. f' err (ef' (xf' s)) (es s) \<longrightarrow> s \<in> Q'' err (xf' s) (es s)))})" (is "\<Gamma> \<turnstile>\<^bsub>/F\<^esub> R' c {s. ?Q'' s}") 132 shows "ccorres_underlying sr \<Gamma> r xf arrel axf (P and R) (P' \<inter> R') hs 133 (a >>=E (\<lambda>rv. b rv)) (c ;; d)" 134 unfolding bindE_def 135 apply (rule_tac R="case_sum QE Q" 136 and R'="\<lambda>rv. {s. s \<in> case_sum QE' QR' rv (xf' s)}" for QE' QR' 137 in ccorres_master_split_hs) 138 apply (rule ac) 139 apply (rule ccorres_abstract[OF ceqv]) 140 apply (case_tac rv, simp_all add: lift_def) 141 apply (rule ccorres_abstract[where xf'=es, OF ceqv_refl]) 142 apply (rule ccorres_gen_asm2) 143 apply (rule ccorres_gen_asm2) 144 apply (rule_tac err'=rv'a in err) 145 apply assumption+ 146 apply (rule ccorres_gen_asm2) 147 apply (rule ccorres_gen_asm2) 148 apply (erule(1) bd) 149 apply (rule ccorres_empty[where P=\<top>]) 150 apply (rule hoare_strengthen_post, rule valid[unfolded validE_def]) 151 apply (simp split: sum.split_asm) 152 apply (rule exec_handlers_Hoare_Post, 153 rule exec_handlers_Hoare_from_vcg_nofail[OF valid', where A="{}"]) 154 apply (auto simp: ccHoarePost_def split: sum.split) 155 done 156 157lemma ccorres_split_nothrow_novcgE: 158 fixes R' :: "cstate set" 159 assumes ac: "ccorres_underlying sr \<Gamma> 160 (f' \<currency> r') (liftxf es ef' vf' xf') 161 (f' \<currency> r') (liftxf es ef' vf' xf') 162 P P' [] a c" 163 and ceqv: "\<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' d (d' rv')" 164 and bd: "\<And>rv rv'. \<lbrakk> r' rv (vf' rv'); ef' rv' = scast EXCEPTION_NONE \<rbrakk> 165 \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (Q rv) (Q' rv rv') hs (b rv) (d' rv')" 166 and err: "\<And>err rv' err'. \<lbrakk> ef' rv' \<noteq> scast EXCEPTION_NONE; f' err (ef' rv') err' \<rbrakk> 167 \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf 168 (QE err) (Q'' err rv' err') hs (throwError err) (d' rv')" 169 and valid: "\<lbrace>R\<rbrace> a \<lbrace>Q\<rbrace>,\<lbrace>QE\<rbrace>" 170 and novcg: "guard_is_UNIV (\<lambda>rv rv'. r' rv (vf' rv')) 171 xf' (\<lambda>rv rv'. {s. ef' rv' = scast EXCEPTION_NONE \<longrightarrow> s \<in> Q' rv rv'})" 172 \<comment> \<open>hack\<close> 173 and novcg_err: "\<And>err. guard_is_UNIV (\<lambda>rv. f' err (ef' rv)) es 174 (\<lambda>rv rv'. {s. ef' (xf' s) \<noteq> scast EXCEPTION_NONE \<longrightarrow> s \<in> Q'' err rv rv'})" 175 shows "ccorres_underlying sr \<Gamma> r xf arrel axf (P and R) P' hs (a >>=E (\<lambda>rv. b rv)) (c ;; d)" 176 unfolding bindE_def 177 apply (rule_tac R="case_sum QE Q" 178 and R'="\<lambda>rv. {s. s \<in> case_sum QE' QR' rv (xf' s)}" for QE' QR' 179 in ccorres_master_split_nohs_UNIV) 180 apply (rule ac) 181 apply (rule ccorres_abstract[OF ceqv]) 182 apply (case_tac rv, simp_all add: lift_def) 183 apply (rule ccorres_abstract[where xf'=es, OF ceqv_refl]) 184 apply (rule ccorres_gen_asm2) 185 apply (rule ccorres_gen_asm2) 186 apply (rule_tac err'=rv'a in err) 187 apply assumption+ 188 apply (rule ccorres_gen_asm2) 189 apply (rule ccorres_gen_asm2) 190 apply (erule(1) bd) 191 apply (rule hoare_strengthen_post, rule valid[unfolded validE_def]) 192 apply (simp split: sum.split_asm) 193 apply (insert novcg novcg_err) 194 apply (clarsimp simp: guard_is_UNIV_def split: sum.split) 195 done 196 197(* Unit would be more appropriate, but the record package will simplify xfdc to () *) 198definition 199 "xfdc (t :: cstate) \<equiv> (0 :: nat)" 200 201lemma xfdc_equal [simp]: 202 "xfdc t = xfdc s" 203 unfolding xfdc_def by simp 204 205lemmas ccorres_split_nothrow_novcg_dc 206 = ccorres_split_nothrow_novcg[where r'=dc and xf'=xfdc, OF _ ceqv_refl] 207 208abbreviation 209 "exfdc \<equiv> liftxf undefined (\<lambda>_. scast EXCEPTION_NONE) id xfdc" 210 211lemma ccorres_return_C': 212 assumes xfc: "\<And>s. (xf (global_exn_var_'_update (\<lambda>_. Return) (xfu (\<lambda>_. v s) s))) = v s" 213 and wfh: "wfhandlers hs" 214 and srv: "\<And>s s'. (s, s') \<in> sr \<Longrightarrow> 215 (s, global_exn_var_'_update (\<lambda>_. Return) (xfu (\<lambda>_. v s') s')) \<in> sr" 216 shows "ccorres_underlying sr \<Gamma> r rvxf arrel xf \<top> {s. arrel rv (v s)} hs 217 (return rv) (return_C xfu v)" 218 using wfh 219 unfolding creturn_def 220 apply - 221 apply (rule ccorresI') 222 apply (erule exec_handlers.cases) 223 apply clarsimp 224 apply (clarsimp elim!: exec_Normal_elim_cases) 225 apply (drule (1) wfhandlersD) 226 apply simp 227 apply (frule exec_handlers_less2, clarsimp) 228 apply (clarsimp simp: return_def unif_rrel_def xfc) 229 apply (auto elim!: srv)[1] 230 apply (clarsimp elim!: exec_Normal_elim_cases) 231 apply simp 232 done 233 234lemma ccorres_return_CE': 235 assumes xfc: "\<And>s. xf (global_exn_var_'_update (\<lambda>_. Return) 236 (xfu (\<lambda>_. v s) s)) = v s" 237 and wfh: "wfhandlers hs" 238 and srv: "\<And>s s'. (s, s') \<in> sr \<Longrightarrow> (s, global_exn_var_'_update (\<lambda>_. Return) (xfu (\<lambda>_. v s') s')) \<in> sr" 239 shows "ccorres_underlying sr \<Gamma> rvr rvxf (f \<currency> r) (liftxf es sf vf xf) 240 \<top> {s. sf (v s) = scast EXCEPTION_NONE \<and> r rv (vf (v s))} hs 241 (returnOk rv) (return_C xfu v)" 242 using wfh 243 unfolding creturn_def 244 apply - 245 apply (rule ccorresI') 246 apply (erule exec_handlers.cases) 247 apply clarsimp 248 apply (clarsimp elim!: exec_Normal_elim_cases) 249 apply (drule (1) wfhandlersD) 250 apply simp 251 apply (simp add: returnOk_def return_def) 252 apply (drule exec_handlers_less2, clarsimp+) 253 apply (auto simp: unif_rrel_def xfc elim!: srv)[1] 254 apply (clarsimp elim!: exec_Normal_elim_cases) 255 apply simp 256 done 257 258lemma ccorres_return_C_errorE': 259 assumes xfc: "\<And>s. xf (global_exn_var_'_update (\<lambda>_. Return) (xfu (\<lambda>_. v s) s)) = v s" 260 and esc: "\<And>s. es (global_exn_var_'_update (\<lambda>_. Return) (xfu (\<lambda>_. v s) s)) = es s" 261 and wfh: "wfhandlers hs" 262 and srv: "\<And>s s'. (s, s') \<in> sr \<Longrightarrow> (s, global_exn_var_'_update (\<lambda>_. Return) (xfu (\<lambda>_. v s') s')) \<in> sr" 263 shows "ccorres_underlying sr \<Gamma> rvr rvxf (f \<currency> r) (liftxf es sf vf xf) 264 \<top> {s. sf (v s) \<noteq> scast EXCEPTION_NONE \<and> f rv (sf (v s)) (es s)} hs 265 (throwError rv) (return_C xfu v)" 266 using wfh 267 unfolding creturn_def 268 apply - 269 apply (rule ccorresI') 270 apply (erule exec_handlers.cases) 271 apply clarsimp 272 apply (clarsimp elim!: exec_Normal_elim_cases) 273 apply (drule (1) wfhandlersD) 274 apply simp 275 apply (simp add: throwError_def return_def) 276 apply (drule exec_handlers_less2, clarsimp+) 277 apply (auto simp: unif_rrel_def xfc esc elim!: srv)[1] 278 apply (clarsimp elim!: exec_Normal_elim_cases) 279 apply simp 280 done 281 282context kernel 283begin 284 285 286abbreviation 287 "ccorres r xf \<equiv> ccorres_underlying rf_sr \<Gamma> r xf r xf" 288 289lemma ccorres_basic_srnoop: 290 assumes asm: "ccorres_underlying rf_sr Gamm r xf arrel axf G G' hs a c" 291 and gsr: "\<And>s'. globals (g s') = globals s'" 292 and gG: "\<And>s'. s' \<in> G' \<Longrightarrow> g s' \<in> G'" 293 shows "ccorres_underlying rf_sr Gamm r xf arrel axf G G' hs a (Basic g ;; c)" 294 using asm unfolding rf_sr_def 295 apply (rule ccorres_basic_srnoop) 296 apply (simp add: gsr) 297 apply (erule gG) 298 done 299 300lemma ccorres_basic_srnoop2: 301 assumes gsr: "\<And>s'. globals (g s') = globals s'" 302 assumes asm: "ccorres_underlying rf_sr Gamm r xf arrel axf G G' hs a c" 303 shows "ccorres_underlying rf_sr Gamm r xf arrel axf G {s. g s \<in> G'} hs a (Basic g ;; c)" 304 apply (rule ccorres_guard_imp2) 305 apply (rule ccorres_symb_exec_r) 306 apply (rule asm) 307 apply vcg 308 apply (rule conseqPre, vcg, clarsimp simp: rf_sr_def gsr) 309 apply clarsimp 310 done 311 312 313(* The naming convention here is that xf', xfr, and xfru are the terms we instantiate *) 314lemma ccorres_call: 315 assumes cul: "ccorres_underlying rf_sr \<Gamma> r xf'' r xf'' A C' [] a (Call f)" 316 and ggl: "\<And>x y s. globals (g x y s) = globals s" 317 and xfg: "\<And>a s t. (xf' (g a t (s\<lparr>globals := globals t\<rparr>))) = xf'' t" 318 and igl: "\<And>s. globals (i s) = globals s" 319 shows "ccorres_underlying rf_sr \<Gamma> r xf' arrel axf 320 A {s. i s \<in> C'} hs a (call i f (\<lambda>s t. s\<lparr>globals := globals t\<rparr>) (\<lambda>x y. Basic (g x y)))" 321 using cul 322 unfolding rf_sr_def 323 apply - 324 apply (rule ccorres_call) 325 apply (erule ccorres_guard_imp) 326 apply simp 327 apply clarsimp 328 apply (simp add: ggl) 329 apply (simp add: xfg) 330 apply (clarsimp simp: igl) 331 done 332 333lemma ccorres_callE: 334 "\<lbrakk> ccorres_underlying rf_sr \<Gamma> r (liftxf es sf vf xf'') 335 r (liftxf es sf vf xf'') A C' [] a (Call f); 336 \<And>x y s. globals (g x y s) = globals s; 337 \<And>a s t. es (g a t (s\<lparr>globals := globals t\<rparr>)) = es t; 338 \<And>a s t. xf' (g a t (s\<lparr>globals := globals t\<rparr>)) = xf'' t; 339 \<And>s. globals (i s) = globals s 340 \<rbrakk> 341 \<Longrightarrow> ccorres_underlying rf_sr \<Gamma> r (liftxf es sf vf xf') arrel axf A {s. i s \<in> C'} hs a 342 (call i f (\<lambda>s t. s\<lparr>globals := globals t\<rparr>) (\<lambda>x y. Basic (g x y)))" 343 apply (erule ccorres_call) 344 apply assumption 345 apply (simp add: liftxf_def) 346 apply assumption 347 done 348 349lemma ccorres_call_record: 350 assumes cul: "ccorres_underlying rf_sr \<Gamma> r xf'' r xf'' A C' [] a (Call f)" 351 and ggl: "\<And>f s. globals (xfu' f s) = globals s" 352 and xfxfu: "\<And>v s. xf' (xfu' (\<lambda>_. v) s) = v" 353 and xfrxfru: "\<And>v s. xfr (xfru (\<lambda>_. v) s) = v" 354 and igl: "\<And>s. globals (i s) = globals s" 355 shows "ccorres_underlying rf_sr \<Gamma> r (xfr \<circ> xf') arrel axf 356 A {s. i s \<in> C'} hs a (call i f (\<lambda>s t. s\<lparr>globals := globals t\<rparr>) 357 (\<lambda>_ t. Basic (xfu' (\<lambda>_. xfru (\<lambda>_. xf'' t) oldv))))" 358 apply (rule ccorres_call) 359 apply (rule cul) 360 apply (rule ggl) 361 apply (simp add: xfrxfru xfxfu) 362 apply (rule igl) 363 done 364 365lemmas ccorres_split_nothrow_call = ccorres_split_nothrow [OF ccorres_call] 366lemmas ccorres_split_nothrow_callE = ccorres_split_nothrowE [OF ccorres_callE] 367 368lemma ccorres_split_nothrow_call_novcg: 369 assumes ac: "ccorres r' xf'' P P' [] a (Call f)" 370 and gg: "\<And>x y s. globals (g x y s) = globals s" 371 and xfxf: "\<And>a s t. xf' (g a t (s\<lparr>globals := globals t\<rparr>)) = xf'' t" 372 and gi: "\<And>s. globals (i s) = globals s" 373 and ceqv: "\<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' d (d' rv')" 374 and bd: "\<And>rv rv'. r' rv rv' \<Longrightarrow> ccorres_underlying rf_sr \<Gamma> r xf arrel axf (Q rv) (Q' rv rv') hs (b rv) (d' rv')" 375 and valid: "\<lbrace>R\<rbrace> a \<lbrace>Q\<rbrace>" 376 shows "ccorres_underlying rf_sr \<Gamma> r xf arrel axf (P and R) ({s. i s \<in> P'} \<inter> 377 {s'. (\<forall>t rv. r' rv (xf'' t) \<longrightarrow> g s' t (s'\<lparr>globals := globals t\<rparr>) \<in> Q' rv (xf'' t))}) 378 hs (a >>= (\<lambda>rv. b rv)) 379 (call i f (\<lambda>s t. s\<lparr>globals := globals t\<rparr>) (\<lambda>x y. Basic (g x y)) ;; d)" (is "ccorres_underlying rf_sr \<Gamma> r xf arrel axf ?P (?Q1 \<inter> ?Q2) hs ?A ?B") 380 apply (rule ccorres_master_split_nohs) 381 apply (rule ccorres_call [OF ac]) 382 apply (rule gg) 383 apply (rule xfxf) 384 apply (rule gi) 385 apply (rule ccorres_abstract[OF ceqv]) 386 apply (rule ccorres_gen_asm2) 387 apply (erule bd) 388 apply (simp add: valid) 389 apply (rule exec_handlers_Hoare_call_Basic) 390 apply (clarsimp simp: ccHoarePost_def xfxf) 391 apply simp 392 done 393 394definition 395 errstate :: "cstate \<Rightarrow> errtype" 396where 397 "errstate s \<equiv> \<lparr> errfault = seL4_Fault_lift (current_fault_' (globals s)), 398 errlookup_fault = lookup_fault_lift (current_lookup_fault_' (globals s)), 399 errsyscall = current_syscall_error_' (globals s) \<rparr>" 400 401lemma errlookup_fault_errstate [simp]: 402 "errlookup_fault (errstate s) = lookup_fault_lift (current_lookup_fault_' (globals s))" 403 unfolding errstate_def 404 by simp 405 406lemma errfault_errstate [simp]: 407 "errfault (errstate s) = seL4_Fault_lift (current_fault_' (globals s))" 408 unfolding errstate_def 409 by simp 410 411lemma errsyscall_errstate [simp]: 412 "errsyscall (errstate s) = (current_syscall_error_' (globals s))" 413 unfolding errstate_def 414 by simp 415 416lemma errstate_state_update [simp]: 417 assumes f: "\<And>s. current_fault_' (globals (g s)) = current_fault_' (globals s)" 418 and lf: "\<And>s. current_lookup_fault_' (globals (g s)) = current_lookup_fault_' (globals s)" 419 and se: "\<And>s. current_syscall_error_' (globals (g s)) = current_syscall_error_' (globals s)" 420 shows "errstate (g s) = errstate s" 421 by (simp add: f lf se errstate_def) 422 423lemma ccorres_split_nothrow_call_novcgE: 424 assumes ac: "ccorres (f' \<currency> r') (liftxf errstate ef' vf' xf'') P P' [] a (Call f)" 425 and gg: "\<And>x y s. globals (g x y s) = globals s" 426 and xfxf: "\<And>a s t. xf' (g a t (s\<lparr>globals := globals t\<rparr>)) = xf'' t" 427 and gi: "\<And>s. globals (i s) = globals s" 428 and ceqv: "\<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' d (d' rv')" 429 and bd: "\<And>rv rv'. \<lbrakk>r' rv (vf' rv'); ef' rv' = scast EXCEPTION_NONE\<rbrakk> 430 \<Longrightarrow> ccorres_underlying rf_sr \<Gamma> (fl \<currency> r) xf arrel axf 431 (Q rv) (Q' rv rv') hs (b rv) (d' rv')" 432 and err: "\<And>err rv' err'. \<lbrakk>ef' rv' \<noteq> scast EXCEPTION_NONE; f' err (ef' rv') err'\<rbrakk> 433 \<Longrightarrow> ccorres_underlying rf_sr \<Gamma> (fl \<currency> r) xf arrel axf 434 (QE err) (Q'' err rv' err') hs (throwError err) (d' rv')" 435 and valid: "\<lbrace>R\<rbrace> a \<lbrace>Q\<rbrace>, \<lbrace>QE\<rbrace>" 436 shows "ccorres_underlying rf_sr \<Gamma> (fl \<currency> r) xf arrel axf (P and R) ({s. i s \<in> P'} \<inter> 437 {s. \<forall>t. (ef' (xf'' t) = scast EXCEPTION_NONE \<longrightarrow> (\<forall>rv. r' rv (vf' (xf'' t)) \<longrightarrow> g s t (s\<lparr>globals := globals t\<rparr>) \<in> Q' rv (xf'' t))) \<and> 438 (ef' (xf'' t) \<noteq> scast EXCEPTION_NONE \<longrightarrow> 439 (\<forall>err. f' err (ef' (xf'' t)) (errstate t) \<longrightarrow> g s t (s\<lparr>globals := globals t\<rparr>) \<in> Q'' err (xf'' t) (errstate t)))} 440 ) hs (a >>=E b) (call i f (\<lambda>s t. s\<lparr>globals := globals t\<rparr>) (\<lambda>x y. Basic (g x y));; 441 d)" (is "ccorres_underlying rf_sr \<Gamma> ?r ?xf arrel axf ?P (?Q1 \<inter> ?Q2) hs ?A ?B") 442 unfolding bindE_def 443 apply (rule_tac R="case_sum QE Q" 444 and R'="\<lambda>rv. {s. s \<in> case_sum QE' QR' rv (xf' s)}" for QE' QR' 445 in ccorres_master_split_nohs) 446 apply (rule ccorres_callE [OF ac]) 447 apply (rule gg) 448 apply (rule errstate_state_update) 449 apply (simp add: gg)+ 450 apply (rule xfxf) 451 apply (rule gi) 452 apply (rule ccorres_abstract[OF ceqv]) 453 apply (case_tac rv, simp_all add: lift_def) 454 apply (rule_tac xf'=errstate in ccorres_abstract[OF ceqv_refl]) 455 apply (rule ccorres_gen_asm2) 456 apply (rule ccorres_gen_asm2) 457 apply (erule_tac err'1=rv'a in err, assumption) 458 apply (rule ccorres_gen_asm2) 459 apply (rule ccorres_gen_asm2) 460 apply (erule(1) bd) 461 apply (rule hoare_strengthen_post) 462 apply (rule valid [unfolded validE_def]) 463 apply (simp split: sum.split_asm) 464 apply (rule exec_handlers_Hoare_call_Basic) 465 apply (clarsimp simp: ccHoarePost_def xfxf gg errstate_def 466 split: sum.split) 467 apply simp 468 done 469 470lemma ccorres_split_nothrow_call_record: 471 assumes ac: "ccorres r' xf'' P P' [] a (Call f)" 472 and ceqv: "\<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' d (d' rv')" 473 and bd: "\<And>rv rv'. r' rv rv' \<Longrightarrow> ccorres_underlying rf_sr \<Gamma> r xf arrel axf (Q rv) (Q' rv rv') hs (b rv) (d' (xfru (\<lambda>_. rv') oldv))" 474 and ggl: "\<And>f s. globals (xfu' f s) = globals s" 475 and xfxfu: "\<And>v s. xf' (xfu' (\<lambda>_. v) s) = v" 476 and xfrxfru: "\<And>v s. xfr (xfru (\<lambda>_. v) s) = v" 477 and igl: "\<And>s. globals (i s) = globals s" 478 and valid: "\<lbrace>R\<rbrace> a \<lbrace>Q\<rbrace>" 479 and valid': "\<Gamma> \<turnstile>\<^bsub>/F\<^esub> R' call i f (\<lambda>s t. s\<lparr>globals := globals t\<rparr>) (\<lambda>_ t. Basic (xfu' (\<lambda>_. xfru (\<lambda>_. xf'' t) oldv))) 480 {s. xf' s = xfru (\<lambda>_. (xfr \<circ> xf') s) oldv \<and> (\<forall>rv. r' rv ((xfr \<circ> xf') s) \<longrightarrow> s \<in> Q' rv ((xfr \<circ> xf') s))}" 481 shows "ccorres_underlying rf_sr \<Gamma> r xf arrel axf (P and R) ({s. i s \<in> P'} \<inter> R') hs (a >>= (\<lambda>rv. b rv)) (call i f (\<lambda>s t. s\<lparr>globals := globals t\<rparr>) 482 (\<lambda>_ t. Basic (xfu' (\<lambda>_. xfru (\<lambda>_. xf'' t) oldv))) ;; d)" 483 using ac ggl xfxfu xfrxfru igl ceqv 484 apply (rule ccorres_split_nothrow_record [OF ccorres_call_record]) 485 apply (erule bd) 486 apply (rule valid) 487 apply (rule valid') 488 done 489 490lemma ccorres_split_nothrow_call_record_novcg: 491 assumes ac: "ccorres r' xf'' P P' [] a (Call f)" 492 and ceqv: "\<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' d (d' rv')" 493 and bd: "\<And>rv rv'. r' rv rv' \<Longrightarrow> ccorres_underlying rf_sr \<Gamma> r xf arrel axf (Q rv) (Q' rv rv') hs (b rv) (d' (xfru (\<lambda>_. rv') oldv))" 494 and ggl: "\<And>f s. globals (xfu' f s) = globals s" 495 and xfxfu: "\<And>v s. xf' (xfu' (\<lambda>_. v) s) = v" 496 and xfrxfru: "\<And>v s. xfr (xfru (\<lambda>_. v) s) = v" 497 and igl: "\<And>s. globals (i s) = globals s" 498 and valid: "\<lbrace>R\<rbrace> a \<lbrace>Q\<rbrace>" 499 and novcg: "guard_is_UNIV r' (xfr \<circ> xf') Q'" 500 \<comment> \<open>This might cause problems \<dots> has to be preserved across c in vcg case, but we can't do that\<close> 501 and xfoldv: "\<And>s. xf' s = xfru (\<lambda>_. (xfr \<circ> xf') s) oldv" 502 shows "ccorres_underlying rf_sr \<Gamma> r xf arrel axf (P and R) ({s. i s \<in> P'}) hs (a >>= (\<lambda>rv. b rv)) (call i f (\<lambda>s t. s\<lparr>globals := globals t\<rparr>) 503 (\<lambda>_ t. Basic (xfu' (\<lambda>_. xfru (\<lambda>_. xf'' t) oldv))) ;; d)" 504 using ac ggl xfxfu xfrxfru igl ceqv 505 apply (rule ccorres_split_nothrow_record_novcg [OF ccorres_call_record]) 506 apply (erule bd) 507 apply (rule valid) 508 apply (rule novcg) 509 apply (rule xfoldv) 510 done 511 512lemma ccorres_return_C: 513 assumes xf1: "\<And>s f. xf (global_exn_var_'_update f (xfu (\<lambda>_. v s) s)) = v s" 514 and xfu: "\<And>s f. globals (xfu f s) = globals s" 515 and wfh: "wfhandlers hs" 516 shows "ccorres_underlying rf_sr \<Gamma> r rvxf arrel xf \<top> {s. arrel rv (v s)} 517 hs (return rv) (return_C xfu v)" 518 apply (rule ccorres_guard_imp2, rule ccorres_return_C') 519 apply (simp add: xf1) 520 apply (rule wfh) 521 apply (simp add: xfu rf_sr_def cong: cstate_relation_only_t_hrs) 522 apply simp 523 done 524 525lemma ccorres_return_CE: 526 assumes xf1: "\<And>s f. xf (global_exn_var_'_update f (xfu (\<lambda>_. v s) s)) = v s" 527 and xfu: "\<And>s f. globals (xfu f s) = globals s" 528 and wfh: "wfhandlers hs" 529 shows "ccorres_underlying rf_sr \<Gamma> rvr rxf (f \<currency> r) (liftxf es sf vf xf) 530 \<top> {s. sf (v s) = scast EXCEPTION_NONE \<and> r rv (vf (v s))} hs 531 (returnOk rv) (return_C xfu v)" 532 apply (rule ccorres_guard_imp2, rule ccorres_return_CE') 533 apply (simp add: xf1) 534 apply (rule wfh) 535 apply (simp add: xfu rf_sr_def cong: cstate_relation_only_t_hrs) 536 apply simp 537 done 538 539lemma ccorres_return_C_errorE: 540 assumes xfc: "\<And>s. xf (global_exn_var_'_update (\<lambda>_. Return) (xfu (\<lambda>_. v s) s)) = v s" 541 and esc: "\<And>s. es (global_exn_var_'_update (\<lambda>_. Return) (xfu (\<lambda>_. v s) s)) = es s" 542 and xfu: "\<And>s f. globals (xfu f s) = globals s" 543 and wfh: "wfhandlers hs" 544 shows "ccorres_underlying rf_sr \<Gamma> rvr rvxf (f \<currency> r) (liftxf es sf vf xf) 545 \<top> {s. sf (v s) \<noteq> scast EXCEPTION_NONE \<and> f rv (sf (v s)) (es s)} hs 546 (throwError rv) (return_C xfu v)" 547 apply (rule ccorres_guard_imp2, rule ccorres_return_C_errorE') 548 apply (rule xfc) 549 apply (rule esc) 550 apply (rule wfh) 551 apply (simp add: xfu rf_sr_def cong: cstate_relation_only_t_hrs) 552 apply simp 553 done 554 555 556(* Generalise *) 557(* c can't fail here, so no /F *) 558lemma ccorres_noop: 559 assumes nop: "\<forall>s. \<Gamma> \<turnstile> {s} c {t. t may_not_modify_globals s}" 560 shows "ccorres_underlying rf_sr \<Gamma> dc xf arrel axf \<top> UNIV hs (return ()) c" 561 apply (rule ccorres_from_vcg, rule allI, simp add: return_def) 562 apply (rule HoarePartial.conseq_exploit_pre) 563 apply simp 564 apply (intro allI impI) 565 apply (rule HoarePartial.conseq) 566 apply (rule nop) 567 apply clarsimp 568 apply (erule iffD1 [OF rf_sr_upd, rotated -1]) 569 apply (clarsimp simp: meq_def mex_def)+ 570 done 571 572lemma ccorres_noop_spec: 573 assumes s: "\<forall>s. \<Gamma> \<turnstile> (P s) c (R s), (A s)" 574 and nop: "\<forall>s. \<Gamma> \<turnstile>\<^bsub>/F\<^esub> {s} c {t. t may_not_modify_globals s}" 575 shows "ccorres_underlying rf_sr \<Gamma> dc xf arrel axf \<top> {s. s \<in> P s} hs (return ()) c" 576 apply (rule ccorres_from_vcg, rule allI, simp add: return_def) 577 apply (rule HoarePartial.conseq_exploit_pre) 578 apply simp 579 apply (intro allI impI) 580 apply (rule HoarePartial.conseq) 581 apply (rule allI) 582 apply (rule HoarePartialProps.Merge_PostConj) 583 apply (rule_tac P = "{s} \<inter> P s" in conseqPre) 584 apply (rule_tac x = s in spec [OF s]) 585 apply clarsimp 586 apply (rule_tac x = s in spec [OF nop]) 587 apply simp 588 apply clarsimp 589 apply clarsimp 590 apply (erule iffD2 [OF rf_sr_upd, rotated -1]) 591 apply (clarsimp simp: meq_def mex_def)+ 592 done 593 594 595(* FIXME: MOVE *) 596lemma ccorres_symb_exec_r2: 597 assumes cul: "ccorres_underlying rf_sr \<Gamma> r xf arrel axf R Q' hs a d" 598 and ex: "\<Gamma> \<turnstile> R' c Q'" 599 and pres: "\<forall>s. \<Gamma> \<turnstile>\<^bsub>/F\<^esub> {s} c {t. t may_not_modify_globals s}" 600 shows "ccorres_underlying rf_sr \<Gamma> r xf arrel axf R R' hs a (c ;; d)" 601 apply (rule ccorres_add_return) 602 apply (rule ccorres_guard_imp2) 603 apply (rule ccorres_split_nothrow') 604 apply (rule ccorres_noop_spec) 605 apply (rule allI) 606 apply (rule ex) 607 apply (rule pres) 608 apply simp 609 apply (rule cul) 610 apply wp 611 apply (rule HoarePartialProps.augment_Faults [OF ex]) 612 apply simp 613 apply simp 614 done 615 616lemma ccorres_trim_redundant_throw: 617 "\<lbrakk>ccorres_underlying rf_sr \<Gamma> arrel axf arrel axf G G' (SKIP # hs) a c; 618 \<And>s f. axf (global_exn_var_'_update f s) = axf s \<rbrakk> 619 \<Longrightarrow> ccorres_underlying rf_sr \<Gamma> r xf arrel axf G G' (SKIP # hs) 620 a (c;; Basic (global_exn_var_'_update (\<lambda>_. Return));; THROW)" 621 apply - 622 apply (rule ccorres_trim_redundant_throw') 623 apply simp 624 apply simp 625 apply (simp add: rf_sr_upd_safe) 626 done 627 628end 629 630 631lemmas in_magnitude_check' = 632 in_magnitude_check [where v = "fst z" and s' = "snd z" for z, folded surjective_pairing] 633 634 635(* Defined in terms of access_ti for convenience *) 636 637lemma fd_cons_update_accessD: 638 "\<lbrakk> fd_cons_update_access d n; length bs = n \<rbrakk> \<Longrightarrow> field_update d (field_access d v bs) v = v" 639 unfolding fd_cons_update_access_def by simp 640 641lemma fd_cons_access_updateD: 642 "\<lbrakk> fd_cons_access_update d n; length bs = n; length bs' = n\<rbrakk> \<Longrightarrow> field_access d (field_update d bs v) bs' = field_access d (field_update d bs v') bs'" 643 unfolding fd_cons_access_update_def by clarsimp 644 645context kernel 646begin 647 648(* Tests *) 649 650lemma cte_C_cap_C_tcb_C': 651 fixes val :: "cap_C" and ptr :: "cte_C ptr" 652 assumes cl: "clift hp ptr = Some z" 653 shows "(clift (hrs_mem_update (heap_update (Ptr &(ptr\<rightarrow>[''cap_C''])) val) hp)) = 654 (clift hp :: tcb_C typ_heap)" 655 using cl 656 by (simp add: typ_heap_simps) 657 658lemma cte_C_cap_C_update: 659 fixes val :: "cap_C" and ptr :: "cte_C ptr" 660 assumes cl: "clift hp ptr = Some z" 661 shows "(clift (hrs_mem_update (heap_update (Ptr &(ptr\<rightarrow>[''cap_C''])) val) hp)) = 662 clift hp(ptr \<mapsto> cte_C.cap_C_update (\<lambda>_. val) z)" 663 using cl 664 by (simp add: clift_field_update) 665 666abbreviation 667 "modifies_heap_spec f \<equiv> \<forall>s. \<Gamma> \<turnstile>\<^bsub>/UNIV\<^esub> {s} Call f {t. t may_only_modify_globals s in [t_hrs]}" 668 669(* Used for bitfield lemmas. Note that this doesn't follow the usual schematic merging: we generally need concrete G and G' *) 670lemma ccorres_from_spec_modifies_heap: 671 assumes spec: "\<forall>s. \<Gamma>\<turnstile> \<lbrace>s. P s\<rbrace> Call f {t. Q s t}" 672 and mod: "modifies_heap_spec f" 673 and xfg: "\<And>f s. xf (globals_update f s) = xf s" 674 and Pimp: "\<And>s s'. \<lbrakk> G s; s' \<in> G'; (s, s') \<in> rf_sr \<rbrakk> \<Longrightarrow> P s'" 675 and rl: "\<And>s s' t'. \<lbrakk>G s; s' \<in> G'; (s, s') \<in> rf_sr; Q s' t'\<rbrakk> 676 \<Longrightarrow> \<exists>(rv, t) \<in> fst (a s). 677 (t, t'\<lparr>globals := globals s'\<lparr>t_hrs_' := t_hrs_' (globals t')\<rparr>\<rparr>) \<in> rf_sr 678 \<and> r rv (xf t')" 679 shows "ccorres_underlying rf_sr \<Gamma> r xf arrel axf G G' [] a (Call f)" 680 apply (rule ccorres_Call_call_for_vcg) 681 apply (rule ccorres_from_vcg) 682 apply (rule allI, rule conseqPre) 683 apply (rule HoarePartial.ProcModifyReturnNoAbr 684 [where return' = "\<lambda>s t. t\<lparr> globals := globals s\<lparr>t_hrs_' := t_hrs_' (globals t) \<rparr>\<rparr>"]) 685 apply (rule HoarePartial.ProcSpecNoAbrupt [OF _ _ spec]) 686 apply (rule subset_refl) 687 apply vcg 688 prefer 2 689 apply (rule mod) 690 apply (clarsimp simp: mex_def meq_def) 691 apply (clarsimp simp: split_beta Pimp) 692 apply (subst bex_cong [OF refl]) 693 apply (rule arg_cong2 [where f = "(\<and>)"]) 694 apply (rule_tac y = "t\<lparr>globals := globals x\<lparr>t_hrs_' := t_hrs_' (globals t)\<rparr>\<rparr>" in rf_sr_upd, simp_all) 695 apply (drule (3) rl) 696 apply (clarsimp simp: xfg elim!: bexI [rotated]) 697 done 698 699(* Used for bitfield lemmas *) 700lemma ccorres_from_spec_modifies: 701 assumes spec: "\<forall>s. \<Gamma>\<turnstile> \<lbrace>s. P s\<rbrace> Call f {t. Q s t}" 702 and mod: "modifies_spec f" 703 and xfg: "\<And>f s. xf (globals_update f s) = xf s" 704 and Pimp: "\<And>s s'. \<lbrakk> G s; s' \<in> G'; (s, s') \<in> rf_sr \<rbrakk> \<Longrightarrow> P s'" 705 and rl: "\<And>s s' t'. \<lbrakk>G s; s' \<in> G'; (s, s') \<in> rf_sr; Q s' t'\<rbrakk> 706 \<Longrightarrow> \<exists>(rv, t) \<in> fst (a s). (t, s') \<in> rf_sr \<and> r rv (xf t')" 707 shows "ccorres_underlying rf_sr \<Gamma> r xf arrel axf G G' [] a (Call f)" 708 apply (rule ccorres_Call_call_for_vcg) 709 apply (rule ccorres_from_vcg) 710 apply (rule allI, rule conseqPre) 711 apply (rule HoarePartial.ProcModifyReturnNoAbr 712 [where return' = "\<lambda>s t. t\<lparr> globals := globals s \<rparr>"]) 713 apply (rule HoarePartial.ProcSpecNoAbrupt [OF _ _ spec]) 714 apply (rule subset_refl) 715 apply vcg 716 prefer 2 717 apply (rule mod) 718 apply (clarsimp simp: mex_def meq_def) 719 apply (clarsimp simp: split_beta Pimp) 720 apply (subst bex_cong [OF refl]) 721 apply (rule arg_cong2 [where f = "(\<and>)"]) 722 apply (rule_tac y = "x" in rf_sr_upd, simp_all) 723 apply (drule (3) rl) 724 apply (clarsimp simp: xfg elim!: bexI [rotated]) 725 done 726 727lemma ccorres_trim_return: 728 assumes fg: "\<And>s. xfu (\<lambda>_. axf s) s = s" 729 and xfu: "\<And>f s. axf (global_exn_var_'_update f s) = axf s" 730 and cc: "ccorres_underlying rf_sr \<Gamma> arrel axf arrel axf G G' (SKIP # hs) a c" 731 shows "ccorres_underlying rf_sr \<Gamma> r xf arrel axf G G' (SKIP # hs) a (c ;; return_C xfu axf)" 732 using fg unfolding creturn_def 733 apply - 734 apply (rule ccorres_rhs_assoc2)+ 735 apply (rule ccorres_trim_redundant_throw) 736 apply (clarsimp split del: if_split) 737 apply (rule iffD2 [OF ccorres_semantic_equiv, OF _ cc]) 738 apply (rule semantic_equivI) 739 apply (case_tac s') 740 apply (auto elim!: exec_Normal_elim_cases exec_elim_cases intro!: exec.intros)[4] 741 apply (rule xfu) 742 done 743 744lemma rf_sr_globals_exn_var: 745 "((s, global_exn_var_'_update f s') \<in> rf_sr) 746 = ((s, s') \<in> rf_sr)" 747 by (rule rf_sr_upd, simp_all) 748 749lemma ccorres_trim_returnE: 750 assumes fg: "\<And>s. xfu (\<lambda>_. axf s) s = s" 751 and xfu: "\<And>f s. axf (global_exn_var_'_update f s) = axf s" 752 and cc: "ccorres r (liftxf errstate ef vf axf) 753 G G' (SKIP # hs) a c" 754 shows "ccorres_underlying rf_sr \<Gamma> rvr rvxf r (liftxf errstate ef vf axf) 755 G G' (SKIP # hs) a (c ;; return_C xfu axf)" 756 unfolding creturn_def 757 apply (rule ccorres_rhs_assoc2)+ 758 apply (rule ccorres_trim_redundant_throw') 759 apply (simp add: fg) 760 apply (rule iffD2 [OF ccorres_semantic_equiv, OF _ cc]) 761 apply (rule semantic_equivI) 762 apply (case_tac s') 763 apply (auto elim!: exec_Normal_elim_cases exec_elim_cases intro!: exec.intros)[4] 764 apply (simp add: liftxf_def xfu) 765 apply (simp add: rf_sr_globals_exn_var) 766 done 767 768lemma ccorres_sequence_while_genQ: 769 fixes i :: "nat" and xf :: "globals myvars \<Rightarrow> ('c :: len) word" 770 assumes one: "\<And>n ys. \<lbrakk> n < length xs \<rbrakk> \<Longrightarrow> 771 ccorres (\<lambda>rv rv'. r' (ys @ [rv]) rv') xf' 772 (F (n * j)) ({s. xf s = of_nat (i + n * j) \<and> r' ys (xf' s)} \<inter> Q) hs 773 (xs ! n) body" 774 and pn: "\<And>n. P n = (n < of_nat (i + length xs * j))" 775 and bodyi: "\<forall>s. xf s < of_nat (i + length xs * j) 776 \<longrightarrow> \<Gamma> \<turnstile>\<^bsub>/UNIV\<^esub> ({s} \<inter> Q) body {t. xf t = xf s \<and> xf_update (\<lambda>x. xf t + of_nat j) t \<in> Q}" 777 and hi: "\<And>n. Suc n < length xs \<Longrightarrow> \<lbrace> F (n * j) \<rbrace> (xs ! n) \<lbrace>\<lambda>_. F (Suc n * j)\<rbrace>" 778 and lxs: "i + length xs * j< 2 ^ len_of TYPE('c)" 779 and xf: "\<forall>s f. xf (xf_update f s) = f (xf s) \<and> globals (xf_update f s) = globals s" 780 and xf': "\<forall>s f. xf' (xf_update f s) = (xf' s)" 781 and j: "j > 0" 782 shows "ccorres (\<lambda>rv (i', rv'). r' rv rv' \<and> i' = of_nat (i + length xs * of_nat j)) 783 (\<lambda>s. (xf s, xf' s)) 784 (\<lambda>s. P 0 \<longrightarrow> F 0 s) ({s. xf s = of_nat i \<and> r' [] (xf' s)} \<inter> Q) hs 785 (sequence xs) 786 (While {s. P (xf s)} 787 (body ;; Basic (\<lambda>s. xf_update (\<lambda>_. xf s + of_nat j) s)))" 788 (is "ccorres ?r' ?xf' ?G (?G' \<inter> _) hs (sequence xs) ?body") 789 apply (rule ccorres_sequence_while_genQ' [OF one pn bodyi hi lxs xf xf']) 790 apply simp 791 apply simp 792 apply (clarsimp simp: rf_sr_def xf) 793 apply (simp add: j) 794 done 795 796lemma ccorres_sequence_while_gen': 797 fixes i :: "nat" and xf :: "globals myvars \<Rightarrow> ('c :: len) word" 798 assumes one: "\<And>n ys. \<lbrakk> n < length xs \<rbrakk> \<Longrightarrow> 799 ccorres (\<lambda>rv rv'. r' (ys @ [rv]) rv') xf' 800 (F (n * j)) {s. xf s = of_nat (i + n * j) \<and> r' ys (xf' s)} hs 801 (xs ! n) body" 802 and pn: "\<And>n. P n = (n < of_nat (i + length xs * j))" 803 and bodyi: "\<forall>s. \<Gamma> \<turnstile>\<^bsub>/UNIV\<^esub> {s} body {t. xf t = xf s}" 804 and hi: "\<And>n. Suc n < length xs \<Longrightarrow> \<lbrace> F (n * j) \<rbrace> (xs ! n) \<lbrace>\<lambda>_. F (Suc n * j)\<rbrace>" 805 and lxs: "i + length xs * j< 2 ^ len_of TYPE('c)" 806 and xf: "\<forall>s f. xf (xf_update f s) = f (xf s) \<and> globals (xf_update f s) = globals s" 807 and xf': "\<forall>s f. xf' (xf_update f s) = (xf' s)" 808 and j: "j > 0" 809 shows "ccorres (\<lambda>rv (i', rv'). r' rv rv' \<and> i' = of_nat (i + length xs * of_nat j)) 810 (\<lambda>s. (xf s, xf' s)) 811 (F 0) ({s. xf s = of_nat i \<and> r' [] (xf' s)}) hs 812 (sequence xs) 813 (While {s. P (xf s)} 814 (body ;; Basic (\<lambda>s. xf_update (\<lambda>_. xf s + of_nat j) s)))" 815 (is "ccorres ?r' ?xf' ?G ?G' hs (sequence xs) ?body") 816 using assms 817 apply - 818 apply (rule ccorres_guard_imp2) 819 apply (rule ccorres_sequence_while_genQ [where Q=UNIV]) 820 apply (assumption|simp)+ 821 done 822 823lemma ccorres_sequence_x_while_genQ': 824 fixes xf :: "globals myvars \<Rightarrow> ('c :: len) word" 825 shows 826 "\<lbrakk>\<And>n. n < length xs \<Longrightarrow> ccorres dc xfdc (F (n * j)) ({s. xf s = of_nat (i + n * j)} \<inter> Q) hs (xs ! n) body; 827 \<And>n. P n = (n < of_nat (i + length xs * j)); 828 \<forall>s. xf s < of_nat (i + length xs * j) 829 \<longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> ({s} \<inter> Q) body {t. xf t = xf s \<and> xf_update (\<lambda>x. xf t + of_nat j) t \<in> Q}; 830 \<And>n. Suc n < length xs \<Longrightarrow> \<lbrace>F (n * j)\<rbrace> xs ! n \<lbrace>\<lambda>_. F (Suc n * j)\<rbrace>; i + length xs * j < 2 ^ len_of TYPE('c); 831 \<forall>s f. xf (xf_update f s) = f (xf s) \<and> globals (xf_update f s) = globals s; j > 0 \<rbrakk> 832 \<Longrightarrow> ccorres (\<lambda>rv i'. i' = of_nat (i + length xs * of_nat j)) xf (\<lambda>s. P 0 \<longrightarrow> F 0 s) ({s. xf s = of_nat i} \<inter> Q) hs 833 (NonDetMonad.sequence_x xs) 834 (While {s. P (xf s)} (body;; 835 Basic (\<lambda>s. xf_update (\<lambda>_. xf s + of_nat j) s)))" 836 apply (simp add: sequence_x_sequence liftM_def[symmetric] 837 ccorres_liftM_simp) 838 apply (rule ccorres_rel_imp) 839 apply (rule ccorres_sequence_while_genQ 840 [where xf'=xfdc and r'=dc and xf_update=xf_update, simplified], 841 (simp add: dc_def)+) 842 done 843 844lemma ccorres_sequence_x_while_gen': 845 fixes xf :: "globals myvars \<Rightarrow> ('c :: len) word" 846 shows 847 "\<lbrakk>\<And>n ys. n < length xs \<Longrightarrow> ccorres dc xfdc (F (n * j)) {s. xf s = of_nat (i + n * j)} hs (xs ! n) body; 848 \<And>n. P n = (n < of_nat (i + length xs * j)); \<forall>s. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} body {t. xf t = xf s}; 849 \<And>n. Suc n < length xs \<Longrightarrow> \<lbrace>F (n * j)\<rbrace> xs ! n \<lbrace>\<lambda>_. F (Suc n * j)\<rbrace>; i + length xs * j < 2 ^ len_of TYPE('c); 850 \<forall>s f. xf (xf_update f s) = f (xf s) \<and> globals (xf_update f s) = globals s; 0 < j \<rbrakk> 851 \<Longrightarrow> ccorres (\<lambda>rv i'. i' = of_nat (i + length xs * of_nat j)) xf (F 0) {s. xf s = of_nat i} hs 852 (NonDetMonad.sequence_x xs) 853 (While {s. P (xf s)} (body;; 854 Basic (\<lambda>s. xf_update (\<lambda>_. xf s + of_nat j) s)))" 855 apply (simp add: sequence_x_sequence liftM_def[symmetric] 856 ccorres_liftM_simp) 857 apply (rule ccorres_rel_imp) 858 apply (rule ccorres_sequence_while_gen' 859 [where xf'=xfdc and r'=dc and xf_update=xf_update, simplified], 860 (simp add: dc_def)+) 861 done 862 863lemma i_xf_for_sequence: 864 "\<forall>s f. i_' (i_'_update f s) = f (i_' s) \<and> globals (i_'_update f s) = globals s" 865 by simp 866 867lemmas ccorres_sequence_x_while' 868 = ccorres_sequence_x_while_gen' [OF _ _ _ _ _ i_xf_for_sequence, folded word_bits_def, 869 where j=1, simplified] 870 871lemma ccorres_sequence_x_while_genQ: 872 fixes xf :: "globals myvars \<Rightarrow> ('c :: len) word" 873 assumes one: "\<forall>n < length xs. ccorres dc xfdc (F (n * j) ) ({s. xf s = of_nat n * of_nat j} \<inter> Q) hs (xs ! n) body" 874 and pn: "\<And>n. P n = (n < of_nat (length xs * j))" 875 and bodyi: "\<forall>s. xf s < of_nat (length xs * j) 876 \<longrightarrow> \<Gamma> \<turnstile>\<^bsub>/UNIV\<^esub> ({s} \<inter> Q) body {t. xf t = xf s \<and> xf_update (\<lambda>x. xf t + of_nat j) t \<in> Q}" 877 and hi: "\<And>n. Suc n < length xs \<Longrightarrow> \<lbrace> F (n * j) \<rbrace> (xs ! n) \<lbrace>\<lambda>_. F (Suc n * j)\<rbrace>" 878 and lxs: "length xs * j < 2 ^ len_of TYPE('c)" 879 and xf: "\<forall>s f. xf (xf_update f s) = f (xf s) \<and> globals (xf_update f s) = globals s" 880 and j: "0 < j" 881 shows "ccorres (\<lambda>rv rv'. rv' = of_nat (length xs) * of_nat j) xf (\<lambda>s. P 0 \<longrightarrow> F 0 s) 882 {s. xf_update (\<lambda>_. 0) s \<in> Q} hs 883 (sequence_x xs) 884 (Basic (\<lambda>s. xf_update (\<lambda>_. 0) s);; 885 (While {s. P (xf s)} 886 (body ;; Basic (\<lambda>s. xf_update (\<lambda>_. xf s + of_nat j) s))))" 887 apply (rule ccorres_symb_exec_r) 888 apply (rule ccorres_sequence_x_while_genQ' [where i=0 and xf_update=xf_update and Q=Q, simplified]) 889 apply (simp add: assms hi[simplified])+ 890 apply (rule conseqPre, vcg) 891 apply (clarsimp simp add: xf) 892 apply (rule conseqPre, vcg) 893 apply (simp add: xf rf_sr_def) 894 done 895 896lemma ccorres_sequence_x_while_gen: 897 fixes xf :: "globals myvars \<Rightarrow> ('c :: len) word" 898 assumes one: "\<forall>n < length xs. ccorres dc xfdc (F (n * j)) {s. xf s = of_nat n * of_nat j} hs (xs ! n) body" 899 and pn: "\<And>n. P n = (n < of_nat (length xs * j))" 900 and bodyi: "\<forall>s. \<Gamma> \<turnstile>\<^bsub>/UNIV\<^esub> {s} body {t. xf t = xf s}" 901 and hi: "\<And>n. Suc n < length xs \<Longrightarrow> \<lbrace> F (n * j) \<rbrace> (xs ! n) \<lbrace>\<lambda>_. F (Suc n * j)\<rbrace>" 902 and lxs: "length xs * j < 2 ^ len_of TYPE('c)" 903 and xf: "\<forall>s f. xf (xf_update f s) = f (xf s) \<and> globals (xf_update f s) = globals s" 904 and j: "0 < j" 905 shows "ccorres (\<lambda>rv rv'. rv' = of_nat (length xs) * of_nat j) xf (F 0) UNIV hs 906 (sequence_x xs) 907 (Basic (\<lambda>s. xf_update (\<lambda>_. 0) s);; 908 (While {s. P (xf s)} 909 (body ;; Basic (\<lambda>s. xf_update (\<lambda>_. xf s + of_nat j) s))))" 910 apply (rule ccorres_symb_exec_r) 911 apply (rule ccorres_sequence_x_while_gen' [where i=0 and xf_update=xf_update, simplified]) 912 apply (simp add: assms hi[simplified])+ 913 apply vcg 914 apply (simp add: xf) 915 apply vcg 916 apply (simp add: xf rf_sr_def) 917 done 918 919lemmas ccorres_sequence_x_while 920 = ccorres_sequence_x_while_gen [OF _ _ _ _ _ i_xf_for_sequence, folded word_bits_def, 921 where j=1, simplified] 922 923lemmas ccorres_sequence_x_whileQ 924 = ccorres_sequence_x_while_genQ [OF _ _ _ _ _ i_xf_for_sequence, folded word_bits_def, 925 where j=1, simplified] 926 927lemma ccorres_mapM_x_while_gen: 928 fixes xf :: "globals myvars \<Rightarrow> ('c :: len) word" 929 assumes rl: "\<forall>n. n < length xs \<longrightarrow> ccorres dc xfdc (F (n * j)) {s. xf s = of_nat n * of_nat j} hs (f (xs ! n)) body" 930 and guard: "\<And>n. P n = (n < of_nat (length xs * j))" 931 and bodyi: "\<forall>s. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} body {s'. xf s' = xf s}" 932 and hi: "\<And>n. Suc n < length xs \<Longrightarrow> \<lbrace>F (n * j)\<rbrace> f (xs ! n) \<lbrace>\<lambda>_. F (Suc n * j)\<rbrace>" 933 and wb: "length xs * j < 2 ^ len_of TYPE('c)" 934 and xf: "\<forall>s f. xf (xf_update f s) = f (xf s) \<and> globals (xf_update f s) = globals s" 935 and j: "0 < j" 936 shows "ccorres (\<lambda>rv rv'. rv' = of_nat (length xs) * of_nat j) xf (F (0 :: nat)) UNIV hs 937 (mapM_x f xs) 938 (Basic (\<lambda>s. xf_update (\<lambda>_. 0) s);; 939 (While {s. P (xf s)} 940 (body ;; Basic (\<lambda>s. xf_update (\<lambda>_. xf s + of_nat j) s))))" 941 unfolding mapM_x_def 942 apply (rule ccorres_rel_imp) 943 apply (rule ccorres_sequence_x_while_gen[where xf_update=xf_update]) 944 apply (simp add: assms hi[simplified])+ 945 done 946 947lemmas ccorres_mapM_x_while 948 = ccorres_mapM_x_while_gen [OF _ _ _ _ _ i_xf_for_sequence, folded word_bits_def, 949 where j=1, simplified] 950 951lemma ccorres_mapM_x_while_genQ: 952 fixes xf :: "globals myvars \<Rightarrow> ('c :: len) word" 953 assumes rl: "\<forall>n. n < length xs \<longrightarrow> ccorres dc xfdc (F (n * j)) ({s. xf s = of_nat n * of_nat j} \<inter> Q) hs (f (xs ! n)) body" 954 and guard: "\<And>n. P n = (n < of_nat (length xs * j))" 955 and bodyi: "\<forall>s. xf s < of_nat (length xs * j) 956 \<longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> ({s} \<inter> Q) body {t. xf t = xf s \<and> xf_update (\<lambda>x. xf t + of_nat j) t \<in> Q}" 957 and hi: "\<And>n. Suc n < length xs \<Longrightarrow> \<lbrace>F (n * j)\<rbrace> f (xs ! n) \<lbrace>\<lambda>_. F (Suc n * j)\<rbrace>" 958 and wb: "length xs * j < 2 ^ len_of TYPE('c)" 959 and xf: "\<forall>s f. xf (xf_update f s) = f (xf s) \<and> globals (xf_update f s) = globals s" 960 and j: "0 < j" 961 shows "ccorres (\<lambda>rv rv'. rv' = of_nat (length xs) * of_nat j) xf (\<lambda>s. P 0 \<longrightarrow> F (0 :: nat) s) 962 {s. xf_update (\<lambda>_. 0) s \<in> Q} hs 963 (mapM_x f xs) 964 (Basic (\<lambda>s. xf_update (\<lambda>_. 0) s);; 965 (While {s. P (xf s)} 966 (body ;; Basic (\<lambda>s. xf_update (\<lambda>_. xf s + of_nat j) s))))" 967 unfolding mapM_x_def 968 apply (rule ccorres_rel_imp) 969 apply (rule ccorres_sequence_x_while_genQ[where xf_update=xf_update]) 970 apply (simp add: assms hi[simplified])+ 971 done 972 973lemmas ccorres_mapM_x_whileQ 974 = ccorres_mapM_x_while_genQ [OF _ _ _ _ _ i_xf_for_sequence, folded word_bits_def, 975 where j=1, simplified] 976 977lemma ccorres_mapM_x_while_gen': 978 fixes xf :: "globals myvars \<Rightarrow> ('c :: len) word" 979 assumes rl: "\<forall>n. n < length xs \<longrightarrow> 980 ccorres dc xfdc (F (n * j)) {s. xf s = of_nat (i + n * j)} hs (f (xs ! n)) body" 981 and guard: "\<And>n. P n = (n < of_nat (i + length xs * j))" 982 and bodyi: "\<forall>s. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} body {s'. xf s' = xf s}" 983 and hi: "\<And>n. Suc n < length xs \<Longrightarrow> \<lbrace>F (n *j)\<rbrace> f (xs ! n) \<lbrace>\<lambda>_. F (Suc n * j)\<rbrace>" 984 and wb: "i + length xs * j < 2 ^ len_of TYPE('c)" 985 and xf: "\<forall>s f. xf (xf_update f s) = f (xf s) \<and> globals (xf_update f s) = globals s" 986 and j: "0 < j" 987 shows "ccorres (\<lambda>rv rv'. rv' = of_nat (i + length xs * j)) xf 988 (F (0 :: nat)) {s. xf s = of_nat i} hs 989 (mapM_x f xs) 990 (While {s. P (xf s)} 991 (body ;; Basic (\<lambda>s. xf_update (\<lambda>_. xf s + of_nat j) s)))" 992 unfolding mapM_x_def 993 apply (rule ccorres_rel_imp) 994 apply (rule ccorres_sequence_x_while_gen'[where xf_update=xf_update]) 995 apply (clarsimp simp only: length_map nth_map rl) 996 apply (simp add: assms hi[simplified])+ 997 done 998 999lemmas ccorres_mapM_x_while' 1000 = ccorres_mapM_x_while_gen' [OF _ _ _ _ _ i_xf_for_sequence, folded word_bits_def, 1001 where j=1, simplified] 1002 1003lemma ccorres_zipWithM_x_while_genQ: 1004 fixes xf :: "globals myvars \<Rightarrow> ('c :: len) word" 1005 assumes rl: "\<forall>n. n < length xs \<and> n < length ys \<longrightarrow> ccorres dc xfdc (F (n * j)) ({s. xf s = of_nat n * of_nat j} \<inter> Q) 1006 hs (f (xs ! n) (ys ! n)) body" 1007 and guard: "\<And>n. P n = (n < of_nat (min (length xs) (length ys)) * of_nat j)" 1008 and bodyi: "\<forall>s. xf s < of_nat (min (length xs) (length ys)) * of_nat j 1009 \<longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> ({s} \<inter> Q) body {t. xf t = xf s \<and> xf_update (\<lambda>x. xf t + of_nat j) t \<in> Q}" 1010 and hi: "\<And>n. Suc n < length xs \<and> Suc n < length ys \<Longrightarrow> \<lbrace>F (n * j)\<rbrace> f (xs ! n) (ys ! n) \<lbrace>\<lambda>_. F (Suc n * j)\<rbrace>" 1011 and wb: "min (length xs) (length ys) * j < 2 ^ len_of TYPE('c)" 1012 and xf: "\<forall>s f. xf (xf_update f s) = f (xf s) \<and> globals (xf_update f s) = globals s" 1013 and j: "0 < j" 1014 shows "ccorres (\<lambda>rv rv'. rv' = of_nat (min (length xs) (length ys) * j)) xf 1015 (F (0 :: nat)) {s. xf_update (\<lambda>_. 0) s \<in> Q} hs 1016 (zipWithM_x f xs ys) 1017 (Basic (\<lambda>s. xf_update (\<lambda>_. 0) s);; 1018 (While {s. P (xf s)} 1019 (body ;; Basic (\<lambda>s. xf_update (\<lambda>_. xf s + of_nat j) s))))" 1020 unfolding zipWithM_x_def 1021 apply (rule ccorres_guard_imp) 1022 apply (rule ccorres_rel_imp [OF ccorres_sequence_x_while_genQ[where F=F, OF _ _ _ _ _ xf j]], 1023 simp_all add: length_zipWith) 1024 apply (simp add: length_zipWith zipWith_nth) 1025 apply (rule rl) 1026 apply (rule guard) 1027 apply (rule bodyi) 1028 apply (simp add: zipWith_nth hi[simplified]) 1029 apply (rule wb) 1030 done 1031 1032lemmas ccorres_zipWithM_x_while_gen = ccorres_zipWithM_x_while_genQ[where Q=UNIV, simplified] 1033 1034lemmas ccorres_zipWithM_x_while 1035 = ccorres_zipWithM_x_while_gen[OF _ _ _ _ _ i_xf_for_sequence, folded word_bits_def, 1036 where j=1, simplified] 1037 1038end 1039 1040lemma ccorres_sequenceE_while_gen_either_way: 1041 fixes xf :: "globals myvars \<Rightarrow> ('c :: len) word" 1042 assumes one: "\<And>n ys. \<lbrakk> n < length xs; n = length ys \<rbrakk> \<Longrightarrow> 1043 ccorres_underlying sr \<Gamma> (inr_rrel (\<lambda>rv rv'. r' (ys @ [rv]) rv')) xf' 1044 (inl_rrel arrel) axf 1045 (F n) (Q \<inter> {s. xf s = xfrel n \<and> r' ys (xf' s)}) hs 1046 (xs ! n) body" 1047 and pn: "\<And>n. (n < length xs \<longrightarrow> P (xfrel n)) \<and> \<not> P (xfrel (length xs))" 1048 and xfrel_u: "\<And>n. xfrel_upd (xfrel n) = xfrel (Suc n)" 1049 and bodyi: "\<And>s. s \<in> Q \<Longrightarrow> \<Gamma> \<turnstile>\<^bsub>/UNIV\<^esub> {s} body (Q \<inter> {t. xf t = xf s}), UNIV" 1050 and hi: "\<And>n. n < length xs \<Longrightarrow> \<lbrace> F n \<rbrace> (xs ! n) \<lbrace>\<lambda>_. F (Suc n)\<rbrace>,-" 1051 and xf: "\<forall>s f. xf (xf_update f s) = f (xf s)" 1052 and xf': "\<forall>s f. xf' (xf_update f s) = (xf' s) 1053 \<and> ((xf_update f s \<in> Q) = (s \<in> Q)) 1054 \<and> (\<forall>s'. ((s', xf_update f s) \<in> sr) = ((s', s) \<in> sr))" 1055 shows "ccorres_underlying sr \<Gamma> (inr_rrel (\<lambda>rv (i', rv'). r' rv rv' \<and> i' = xfrel (length xs))) 1056 (\<lambda>s. (xf s, xf' s)) arrel axf 1057 (F 0) (Q \<inter> {s. xf s = xfrel 0 \<and> r' [] (xf' s)}) hs 1058 (sequenceE xs) 1059 (While {s. P (xf s)} 1060 (body ;; Basic (\<lambda>s. xf_update (\<lambda>_. xfrel_upd (xf s)) s)))" 1061 (is "ccorres_underlying sr \<Gamma> (inr_rrel ?r') ?xf' arrel axf ?G ?G' hs (sequenceE xs) ?body") 1062proof - 1063 define init_xs where "init_xs \<equiv> xs" 1064 1065 have rl: "xs = drop (length init_xs - length xs) init_xs" unfolding init_xs_def 1066 by fastforce 1067 1068 note pn' = pn [folded init_xs_def] 1069 note one' = one [folded init_xs_def] 1070 note hi' = hi [folded init_xs_def] 1071 1072 let ?Q = "\<lambda>xs. F (length init_xs - length xs)" 1073 let ?Q' = "\<lambda>xs zs. Q \<inter> {s. (xf s) = xfrel (length init_xs - length xs) 1074 \<and> r' zs (xf' s)}" 1075 let ?r'' = "\<lambda>zs rv (i', rv'). r' (zs @ rv) rv' 1076 \<and> i' = xfrel (length init_xs)" 1077 1078 have "\<forall>zs. length zs = length init_xs - length xs \<longrightarrow> 1079 ccorres_underlying sr \<Gamma> (inr_rrel (?r'' zs)) ?xf' (inl_rrel arrel) axf 1080 (?Q xs) (?Q' xs zs) hs 1081 (sequenceE xs) ?body" 1082 using rl 1083 proof (induct xs) 1084 case Nil 1085 thus ?case 1086 apply clarsimp 1087 apply (rule iffD1 [OF ccorres_expand_while_iff]) 1088 apply (simp add: sequenceE_def returnOk_def) 1089 apply (rule ccorres_guard_imp2) 1090 apply (rule ccorres_cond_false) 1091 apply (rule ccorres_return_Skip') 1092 apply (simp add: pn') 1093 done 1094 next 1095 case (Cons y ys) 1096 1097 from Cons.prems have ly: "length (y # ys) \<le> length init_xs" by simp 1098 hence ln: "(length init_xs - length ys) = Suc (length init_xs - length (y # ys))" by simp 1099 hence yv: "y = init_xs ! (length init_xs - length (y # ys))" using Cons.prems 1100 by (fastforce simp add: drop_Suc_nth not_le) 1101 1102 have lt0: "0 < length init_xs" using ly by clarsimp 1103 hence ly': "length init_xs - length (y # ys) < length init_xs" by simp 1104 1105 note one'' = one'[OF ly', simplified yv[symmetric]] 1106 1107 have ys_eq: "ys = drop (length init_xs - length ys) init_xs" 1108 using ln Cons.prems 1109 by (fastforce simp add: drop_Suc_nth not_le) 1110 note ih = Cons.hyps [OF ys_eq, rule_format] 1111 1112 note hi'' = hi' [OF ly', folded yv] 1113 1114 show ?case 1115 apply (clarsimp simp: sequenceE_Cons) 1116 apply (rule ccorres_guard_imp2) 1117 apply (rule iffD1 [OF ccorres_expand_while_iff]) 1118 apply (rule ccorres_cond_true) 1119 apply (rule ccorres_rhs_assoc)+ 1120 apply (rule ccorres_splitE) 1121 apply (simp add: inl_rrel_inl_rrel) 1122 apply (rule_tac ys="zs" in one'') 1123 apply simp 1124 apply (rule ceqv_refl) 1125 apply (rule ccorres_symb_exec_r) 1126 apply (simp add: liftME_def[symmetric] liftME_liftM) 1127 apply (rule ccorres_rel_imp2, rule_tac zs="zs @ [rv]" in ih) 1128 apply (cut_tac ly, simp) 1129 apply (clarsimp elim!: inl_inrE) 1130 apply (clarsimp elim!: inl_inrE) 1131 apply vcg 1132 apply (rule conseqPre) 1133 apply vcg 1134 apply (clarsimp simp: xf xf') 1135 apply (subst ln) 1136 apply (rule hi'') 1137 apply (rule HoarePartialDef.Conseq [where P = "Q \<inter> {s. xfrel_upd (xf s) = xfrel (length init_xs - length ys)}"]) 1138 apply (intro ballI exI) 1139 apply (rule conjI) 1140 apply (rule_tac s=s in bodyi) 1141 apply simp 1142 apply (clarsimp simp: xf xf' ccHoarePost_def elim!: inl_inrE) 1143 apply (clarsimp simp: ln pn' xfrel_u diff_Suc_less[OF lt0]) 1144 done 1145 qed 1146 thus ?thesis 1147 by (clarsimp simp: init_xs_def dest!: spec[where x=Nil] 1148 elim!: ccorres_rel_imp2 inl_inrE) 1149 qed 1150 1151lemma ccorres_sequenceE_while_down: 1152 fixes xf :: "globals myvars \<Rightarrow> ('c :: len) word" 1153 assumes one: "\<And>n ys. \<lbrakk> n < length xs; n = length ys \<rbrakk> \<Longrightarrow> 1154 ccorres_underlying sr \<Gamma> (inr_rrel (\<lambda>rv rv'. r' (ys @ [rv]) rv')) xf' 1155 (inl_rrel arrel) axf 1156 (F n) (Q \<inter> {s. xf s = (startv - of_nat n) \<and> r' ys (xf' s)}) hs 1157 (xs ! n) body" 1158 and pn: "\<And>n. (n < length xs \<longrightarrow> P (startv - of_nat n)) \<and> \<not> P (startv - of_nat (length xs))" 1159 and bodyi: "\<And>s. s \<in> Q \<Longrightarrow> \<Gamma> \<turnstile>\<^bsub>/UNIV\<^esub> {s} body (Q \<inter> {t. xf t = xf s}), UNIV" 1160 and hi: "\<And>n. n < length xs \<Longrightarrow> \<lbrace> F n \<rbrace> (xs ! n) \<lbrace>\<lambda>_. F (Suc n)\<rbrace>,-" 1161 and xf: "\<forall>s f. xf (xf_update f s) = f (xf s)" 1162 and xf': "\<forall>s f. xf' (xf_update f s) = (xf' s) 1163 \<and> ((xf_update f s \<in> Q) = (s \<in> Q)) 1164 \<and> (\<forall>s'. ((s', xf_update f s) \<in> sr) = ((s', s) \<in> sr))" 1165 shows "ccorres_underlying sr \<Gamma> (inr_rrel (\<lambda>rv (i', rv'). r' rv rv' \<and> i' = (startv - of_nat (length xs)))) 1166 (\<lambda>s. (xf s, xf' s)) arrel axf 1167 (F 0) (Q \<inter> {s. xf s = (startv - of_nat 0) \<and> r' [] (xf' s)}) hs 1168 (sequenceE xs) 1169 (While {s. P (xf s)} 1170 (body ;; Basic (\<lambda>s. xf_update (\<lambda>_. xf s - 1) s)))" 1171 (is "ccorres_underlying sr \<Gamma> (inr_rrel ?r') ?xf' arrel axf ?G ?G' hs (sequenceE xs) ?body") 1172 by (rule ccorres_sequenceE_while_gen_either_way 1173 [OF one, where xf_update=xf_update], 1174 simp_all add: bodyi hi xf xf' pn) 1175 1176lemma ccorres_sequenceE_while_gen': 1177 fixes i :: "nat" and xf :: "globals myvars \<Rightarrow> ('c :: len) word" 1178 assumes one: "\<And>n ys. \<lbrakk> n < length xs; n = length ys \<rbrakk> \<Longrightarrow> 1179 ccorres_underlying sr \<Gamma> (inr_rrel (\<lambda>rv rv'. r' (ys @ [rv]) rv')) xf' 1180 (inl_rrel arrel) axf 1181 (F n) (Q \<inter> {s. xf s = of_nat (i + n) \<and> r' ys (xf' s)}) hs 1182 (xs ! n) body" 1183 and pn: "\<And>n. P n = (n < of_nat (i + length xs))" 1184 and bodyi: "\<And>s. s \<in> Q \<Longrightarrow> \<Gamma> \<turnstile>\<^bsub>/UNIV\<^esub> {s} body (Q \<inter> {t. xf t = xf s}), UNIV" 1185 and hi: "\<And>n. n < length xs \<Longrightarrow> \<lbrace> F n \<rbrace> (xs ! n) \<lbrace>\<lambda>_. F (Suc n)\<rbrace>,-" 1186 and lxs: "i + length xs < 2 ^ len_of TYPE('c)" 1187 and xf: "\<forall>s f. xf (xf_update f s) = f (xf s)" 1188 and xf': "\<forall>s f. xf' (xf_update f s) = (xf' s) 1189 \<and> ((xf_update f s \<in> Q) = (s \<in> Q)) 1190 \<and> (\<forall>s'. ((s', xf_update f s) \<in> sr) = ((s', s) \<in> sr))" 1191 shows "ccorres_underlying sr \<Gamma> (inr_rrel (\<lambda>rv (i', rv'). r' rv rv' \<and> i' = of_nat (i + length xs))) 1192 (\<lambda>s. (xf s, xf' s)) arrel axf 1193 (F 0) (Q \<inter> {s. xf s = of_nat i \<and> r' [] (xf' s)}) hs 1194 (sequenceE xs) 1195 (While {s. P (xf s)} 1196 (body ;; Basic (\<lambda>s. xf_update (\<lambda>_. xf s + 1) s)))" 1197 (is "ccorres_underlying sr \<Gamma> (inr_rrel ?r') ?xf' arrel axf ?G ?G' hs (sequenceE xs) ?body") 1198 apply (rule ccorres_sequenceE_while_gen_either_way 1199 [OF one, where xf_update=xf_update, simplified add_0_right], 1200 simp_all add: bodyi hi lxs xf xf' pn) 1201 apply clarsimp 1202 apply (simp only: Abs_fnat_hom_add, rule of_nat_mono_maybe) 1203 apply (rule lxs) 1204 apply simp 1205 done 1206 1207lemma ccorres_sequenceE_while: 1208 fixes axf :: "globals myvars \<Rightarrow> 'e" shows 1209 "\<lbrakk>\<And>ys. length ys < length xs \<Longrightarrow> 1210 ccorres_underlying sr \<Gamma> (inr_rrel (\<lambda>rv rv'. r' (ys @ [rv]) rv')) xf' 1211 (inl_rrel arrel) axf 1212 (F (length ys)) (Q \<inter> {s. i_' s = of_nat (length ys) \<and> r' ys (xf' s)}) hs 1213 (xs ! length ys) body; 1214 \<And>n. P n = (n < of_nat (length xs)); 1215 \<And>s. s \<in> Q \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} body (Q \<inter> {t. i_' t = i_' s}),UNIV; 1216 \<And>n. n < length xs \<Longrightarrow> \<lbrace>F n\<rbrace> xs ! n \<lbrace>\<lambda>_. F (Suc n)\<rbrace>, -; 1217 length xs < 2 ^ word_bits; 1218 \<forall>s f. xf' (i_'_update f s) = xf' s 1219 \<and> ((i_'_update f s \<in> Q) = (s \<in> Q)) 1220 \<and> (\<forall>s'. ((s', i_'_update f s) \<in> sr) = ((s', s) \<in> sr)) \<rbrakk> 1221 \<Longrightarrow> ccorres_underlying sr \<Gamma> (inr_rrel (\<lambda>rv (i', rv'). r' rv rv' \<and> i' = of_nat (length xs))) 1222 (\<lambda>s. (i_' s, xf' s)) arrel axf 1223 (F 0) (Q \<inter> {s. r' [] (xf' s)}) hs 1224 (sequenceE xs) 1225 (Basic (\<lambda>s. i_'_update (\<lambda>_. 0) s) ;; 1226 While {s. P (i_' s)} (body;; 1227 Basic (\<lambda>s. i_'_update (\<lambda>_. i_' s + 1) s)))" 1228 apply (rule ccorres_guard_imp2) 1229 apply (rule ccorres_symb_exec_r) 1230 apply (rule ccorres_sequenceE_while_gen'[where i=0, simplified, where xf_update=i_'_update], 1231 (assumption | simp)+) 1232 apply (simp add: word_bits_def) 1233 apply simp+ 1234 apply vcg 1235 apply (rule conseqPre, vcg) 1236 apply clarsimp 1237 apply simp 1238 done 1239 1240context kernel begin 1241 1242lemma ccorres_split_nothrow_novcg_case_sum: 1243 "\<lbrakk>ccorresG sr \<Gamma> (f' \<currency> r') (liftxf es ef' vf' xf') P P' [] a c; 1244 \<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' d (d' rv'); 1245 \<And>rv rv'. \<lbrakk> r' rv (vf' rv'); ef' rv' = scast EXCEPTION_NONE \<rbrakk> 1246 \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (Q rv) (Q' rv rv') hs (b rv) (d' rv'); 1247 \<And>err rv' err'. 1248 \<lbrakk> ef' rv' \<noteq> scast EXCEPTION_NONE; f' err (ef' rv') err' \<rbrakk> 1249 \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (QE err) (Q'' err rv' err') hs (e err) (d' rv'); 1250 \<lbrace>R\<rbrace> a \<lbrace>Q\<rbrace>, \<lbrace>QE\<rbrace>; guard_is_UNIV (\<lambda>rv rv'. r' rv (vf' rv')) xf' 1251 (\<lambda>rv rv'. {s. ef' rv' = scast EXCEPTION_NONE \<longrightarrow> s \<in> Q' rv rv'}); 1252 \<And>err. guard_is_UNIV (\<lambda>rv. f' err (ef' rv)) es 1253 (\<lambda>rv rv'. {s. ef' (xf' s) \<noteq> scast EXCEPTION_NONE \<longrightarrow> s \<in> Q'' err rv rv'})\<rbrakk> 1254 \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (P and R) P' hs (a >>= case_sum e b) (c;;d)" 1255 apply (rule_tac R="case_sum QE Q" and R'="case_sum QE' QR'" for QE' QR' 1256 in ccorres_master_split_nohs_UNIV) 1257 apply assumption 1258 apply (case_tac rv, simp_all)[1] 1259 apply (erule ccorres_abstract) 1260 apply (rule ccorres_abstract[where xf'=es], rule ceqv_refl) 1261 apply (rule_tac P="ef' rv' \<noteq> scast EXCEPTION_NONE" in ccorres_gen_asm2) 1262 apply (rule_tac P="f' aa (ef' rv') rv'a" in ccorres_gen_asm2) 1263 apply assumption 1264 apply (erule ccorres_abstract) 1265 apply (rule_tac P="r' ba (vf' rv')" in ccorres_gen_asm2) 1266 apply (rule_tac P="ef' rv' = scast EXCEPTION_NONE" in ccorres_gen_asm2) 1267 apply assumption 1268 apply (simp add: validE_def) 1269 apply (erule hoare_strengthen_post, simp split: sum.split_asm) 1270 apply (clarsimp simp: guard_is_UNIV_def 1271 split: sum.split) 1272 done 1273 1274lemma ccorres_split_nothrow_case_sum: 1275 "\<lbrakk>ccorresG sr \<Gamma> (f' \<currency> r') (liftxf es ef' vf' xf') P P' hs a c; 1276 \<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' d (d' rv'); 1277 \<And>rv rv'. \<lbrakk> r' rv (vf' rv'); ef' rv' = scast EXCEPTION_NONE \<rbrakk> 1278 \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (Q rv) (Q' rv rv') hs (b rv) (d' rv'); 1279 \<And>err rv' err'. 1280 \<lbrakk> ef' rv' \<noteq> scast EXCEPTION_NONE; f' err (ef' rv') err' \<rbrakk> 1281 \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (QE err) (Q'' err rv' err') hs (e err) (d' rv'); 1282 \<lbrace>R\<rbrace> a \<lbrace>Q\<rbrace>, \<lbrace>QE\<rbrace>; \<Gamma> \<turnstile>\<^bsub>/UNIV\<^esub> R' c {s. (\<forall>rv'. ef' (xf' s) = scast EXCEPTION_NONE \<longrightarrow> r' rv' (vf' (xf' s)) 1283 \<longrightarrow> s \<in> Q' rv' (xf' s)) 1284 \<and> (\<forall>ft. ef' (xf' s) \<noteq> scast EXCEPTION_NONE \<longrightarrow> f' ft (ef' (xf' s)) (es s) 1285 \<longrightarrow> s \<in> Q'' ft (xf' s) (es s))} \<rbrakk> 1286 \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (P and R) (P' \<inter> R') hs (a >>= case_sum e b) (c;;d)" 1287 apply (erule_tac R="case_sum QE Q" and R'="case_sum QE' QR'" for QE' QR' 1288 in ccorres_master_split_hs) 1289 apply (case_tac rv, simp_all)[1] 1290 apply (erule ccorres_abstract) 1291 apply (rule ccorres_abstract[where xf'=es], rule ceqv_refl) 1292 apply (rule_tac P="ef' rv' \<noteq> scast EXCEPTION_NONE" in ccorres_gen_asm2) 1293 apply (rule_tac P="f' aa (ef' rv') rv'a" in ccorres_gen_asm2) 1294 apply assumption 1295 apply (erule ccorres_abstract) 1296 apply (rule_tac P="r' ba (vf' rv')" in ccorres_gen_asm2) 1297 apply (rule_tac P="ef' rv' = scast EXCEPTION_NONE" in ccorres_gen_asm2) 1298 apply assumption 1299 apply (rule ccorres_empty[where P=\<top>]) 1300 apply (simp add: validE_def) 1301 apply (erule hoare_strengthen_post, simp split: sum.split_asm) 1302 apply (drule exec_handlers_Hoare_from_vcg_nofail) 1303 apply (erule exec_handlers_Hoare_Post [OF _ _ subset_refl]) 1304 apply (clarsimp simp: ccHoarePost_def split: sum.split) 1305 done 1306 1307end 1308 1309text \<open>@{method ccorres_rewrite} support for discarding everything after @{term creturn}.\<close> 1310 1311lemma never_continues_creturn [C_simp_throws]: 1312 "never_continues \<Gamma> (creturn rtu xfu v)" 1313 by (auto simp: never_continues_def creturn_def elim: exec_elim_cases) 1314 1315lemma never_continues_creturn_void [C_simp_throws]: 1316 "never_continues \<Gamma> (creturn_void rtu)" 1317 by (auto simp: never_continues_def creturn_void_def elim: exec_elim_cases) 1318 1319lemma 1320 "ccorres_underlying sr \<Gamma> r xf r' xf' P P' hs H 1321 (c1 ;; (c2 ;; c3 ;; (creturn rtu xfu v ;; c4 ;; c5) ;; c6 ;; c7))" 1322 apply ccorres_rewrite 1323 apply (match conclusion in "ccorres_underlying sr \<Gamma> r xf r' xf' P P' hs H 1324 (c1 ;; (c2 ;; c3 ;; creturn rtu xfu v))" \<Rightarrow> \<open>-\<close>) 1325 oops 1326 1327end 1328