1(* 2 * Copyright 2014, General Dynamics C4 Systems 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(GD_GPL) 9 *) 10 11theory TcbQueue_C 12imports Ctac_lemmas_C 13begin 14 15(* FIXME: move *) 16lemma (in semigroup) foldl_first: 17 "f x (foldl f y zs) = foldl f (f x y) zs" 18 by (induction zs arbitrary: x y) (auto simp: assoc) 19 20(* FIXME: move *) 21lemma (in monoid) foldl_first': 22 "f x (foldl f z zs) = foldl f x zs" 23 using foldl_first by simp 24 25context kernel 26begin 27 28lemma tcb_queueD: 29 assumes queue_rel: "tcb_queue_relation getNext getPrev mp queue qprev qhead" 30 and valid_ntfn: "distinct queue" 31 and in_queue: "tcbp \<in> set queue" 32 and cs_tcb: "mp (tcb_ptr_to_ctcb_ptr tcbp) = Some tcb" 33 shows "(if tcbp = hd queue then getPrev tcb = qprev 34 else (\<exists>n < (length queue) - 1. getPrev tcb = tcb_ptr_to_ctcb_ptr (queue ! n) 35 \<and> tcbp = queue ! Suc n)) 36 \<and> (if tcbp = last queue then getNext tcb = NULL 37 else (\<exists>n < (length queue) - 1. tcbp = queue ! n 38 \<and> getNext tcb = tcb_ptr_to_ctcb_ptr (queue ! Suc n)))" 39 (is "?prev tcb queue qprev \<and> ?next tcb queue") 40 using queue_rel in_queue valid_ntfn 41proof (induct queue arbitrary: qprev qhead) 42 case Nil 43 thus ?case by simp 44next 45 case (Cons tcb' tcbs qprev' qhead') 46 have "tcbp = tcb' \<or> tcbp \<in> set tcbs" using Cons.prems by simp 47 thus ?case 48 proof 49 assume tcbp: "tcbp = tcb'" 50 hence "?prev tcb (tcb' # tcbs) qprev'" 51 using Cons.prems cs_tcb by clarsimp 52 moreover 53 have "?next tcb (tcb' # tcbs)" 54 proof (cases "tcbs = []") 55 case True 56 thus ?thesis using tcbp Cons.prems cs_tcb by clarsimp 57 next 58 case False 59 hence "tcbp \<noteq> last tcbs" using tcbp Cons.prems by clarsimp 60 thus ?thesis using False tcbp Cons.prems cs_tcb 61 apply clarsimp 62 apply (rule exI [where x = 0]) 63 apply simp 64 apply (cases tcbs) 65 apply simp_all 66 done 67 qed 68 ultimately show ?thesis .. 69 next 70 assume tcbp: "tcbp \<in> set tcbs" 71 obtain tcb2 where cs_tcb2: "mp (tcb_ptr_to_ctcb_ptr tcb') = Some tcb2" 72 and rel2: "tcb_queue_relation getNext getPrev mp tcbs (tcb_ptr_to_ctcb_ptr tcb') (getNext tcb2)" 73 using Cons.prems 74 by clarsimp 75 76 have ih: "?prev tcb tcbs (tcb_ptr_to_ctcb_ptr tcb') \<and> ?next tcb tcbs" 77 proof (rule Cons.hyps) 78 from Cons.prems show (* "\<forall>t\<in>set tcbs. tcb_at' t s" 79 and *) "distinct tcbs" by simp_all 80 qed fact+ 81 82 from tcbp Cons.prems have tcbp_not_tcb': "tcbp \<noteq> tcb'" by clarsimp 83 from tcbp have tcbsnz: "tcbs \<noteq> []" by clarsimp 84 hence hd_tcbs: "hd tcbs = tcbs ! 0" by (simp add: hd_conv_nth) 85 86 show ?case 87 proof (rule conjI) 88 show "?prev tcb (tcb' # tcbs) qprev'" 89 using ih [THEN conjunct1] tcbp_not_tcb' hd_tcbs tcbsnz 90 apply (clarsimp split: if_split_asm) 91 apply fastforce 92 apply (rule_tac x = "Suc n" in exI) 93 apply simp 94 done 95 next 96 show "?next tcb (tcb' # tcbs)" 97 using ih [THEN conjunct2] tcbp_not_tcb' hd_tcbs tcbsnz 98 apply (clarsimp split: if_split_asm) 99 apply (rule_tac x = "Suc n" in exI) 100 apply simp 101 done 102 qed 103 qed 104qed 105 106lemma tcb_queue_memberD: 107 assumes queue_rel: "tcb_queue_relation getNext getPrev (cslift s') queue qprev qhead" 108 and in_queue: "tcbp \<in> set queue" 109 and valid_ntfn: "\<forall>t\<in>set queue. tcb_at' t s" 110 and rf_sr: "(s, s') \<in> rf_sr" 111 shows "\<exists>tcb. cslift s' (tcb_ptr_to_ctcb_ptr tcbp) = Some tcb" 112 using assms 113 apply - 114 apply (drule (1) bspec) 115 apply (drule (1) tcb_at_h_t_valid) 116 apply (clarsimp simp add: h_t_valid_clift_Some_iff) 117 done 118 119lemma tcb_queue_valid_ptrsD: 120 assumes in_queue: "tcbp \<in> set queue" 121 and rf_sr: "(s, s') \<in> rf_sr" 122 and valid_ntfn: "\<forall>t\<in>set queue. tcb_at' t s" "distinct queue" 123 and queue_rel: "tcb_queue_relation getNext getPrev (cslift s') queue NULL qhead" 124 shows "\<exists>tcb. cslift s' (tcb_ptr_to_ctcb_ptr tcbp) = Some tcb 125 \<and> (getPrev tcb \<noteq> NULL \<longrightarrow> s' \<Turnstile>\<^sub>c (getPrev tcb) 126 \<and> getPrev tcb \<in> tcb_ptr_to_ctcb_ptr ` set queue) 127 \<and> (getNext tcb \<noteq> NULL \<longrightarrow> s' \<Turnstile>\<^sub>c (getNext tcb) 128 \<and> getNext tcb \<in> tcb_ptr_to_ctcb_ptr ` set queue)" 129 using assms 130 apply - 131 apply (frule (3) tcb_queue_memberD) 132 apply (elim exE) 133 apply (frule (3) tcb_queueD) 134 apply (auto intro!: tcb_at_h_t_valid elim!: bspec split: if_split_asm) 135 done 136 137lemma tcb_queue_relation_restrict0: 138 "set queue \<subseteq> S \<Longrightarrow> tcb_queue_relation getNext getPrev mp queue qprev qhead = 139 tcb_queue_relation getNext getPrev (restrict_map mp (tcb_ptr_to_ctcb_ptr ` S)) queue qprev qhead" 140proof (induct queue arbitrary: S qprev qhead) 141 case Nil thus ?case by simp 142next 143 case (Cons tcb tcbs S' qprev' qhead') 144 thus ?case 145 using Cons by auto 146qed 147 148lemma tcb_queue_relation_restrict: 149 "tcb_queue_relation getNext getPrev mp queue qprev qhead = 150 tcb_queue_relation getNext getPrev (restrict_map mp (tcb_ptr_to_ctcb_ptr ` set queue)) queue qprev qhead" 151 apply (rule tcb_queue_relation_restrict0) 152 apply simp 153 done 154 155lemma tcb_queue_relation_only_next_prev: 156 assumes mapeq: "option_map getNext \<circ> mp = option_map getNext \<circ> mp'" "option_map getPrev \<circ> mp = option_map getPrev \<circ> mp'" 157 shows "tcb_queue_relation getNext getPrev mp queue qprev qhead = tcb_queue_relation getNext getPrev mp' queue qprev qhead" 158proof (induct queue arbitrary: qprev qhead) 159 case Nil thus ?case by simp 160next 161 case (Cons tcb tcbs qprev' qhead') 162 thus ?case 163 apply clarsimp 164 apply (rule iffI) 165 apply clarsimp 166 apply (frule compD [OF mapeq(1)]) 167 apply clarsimp 168 apply (frule compD [OF mapeq(2)]) 169 apply clarsimp 170 apply clarsimp 171 apply (frule compD [OF mapeq(1) [symmetric]]) 172 apply clarsimp 173 apply (frule compD [OF mapeq(2) [symmetric]]) 174 apply clarsimp 175 done 176qed 177 178 179lemma tcb_queue_relation_cong: 180 assumes queuec: "queue = queue'" 181 and qpc: "qprev = qprev'" 182 and qhc: "qhead = qhead'" 183 and mpc: "\<And>p. p \<in> tcb_ptr_to_ctcb_ptr ` set queue' \<Longrightarrow> mp p = mp' p" 184 shows "tcb_queue_relation getNext getPrev mp queue qprev qhead = 185 tcb_queue_relation getNext getPrev mp' queue' qprev' qhead'" (is "?LHS = ?RHS") 186proof - 187 have "?LHS = tcb_queue_relation getNext getPrev (mp |` (tcb_ptr_to_ctcb_ptr ` set queue')) queue' qprev' qhead'" 188 by (simp add: queuec qpc qhc, subst tcb_queue_relation_restrict, rule refl) 189 190 also have "\<dots> = tcb_queue_relation getNext getPrev (mp' |` (tcb_ptr_to_ctcb_ptr ` set queue')) queue' qprev' qhead'" 191 by (simp add: mpc cong: restrict_map_cong) 192 193 also have "\<dots> = ?RHS" 194 by (simp add: tcb_queue_relation_restrict [symmetric]) 195 196 finally show ?thesis . 197qed 198 199lemma tcb_queue_relation'_cong: 200 assumes queuec: "queue = queue'" 201 and qhc: "qhead = qhead'" 202 and qpc: "qend = qend'" 203 and mpc: "\<And>p. p \<in> tcb_ptr_to_ctcb_ptr ` set queue' \<Longrightarrow> mp p = mp' p" 204 shows "tcb_queue_relation' getNext getPrev mp queue qhead qend = 205 tcb_queue_relation' getNext getPrev mp' queue' qhead' qend'" (is "?LHS = ?RHS") 206proof - 207 have "?LHS = tcb_queue_relation' getNext getPrev (mp |` (tcb_ptr_to_ctcb_ptr ` set queue')) queue' qhead' qend'" 208 by (clarsimp simp add: queuec qpc qhc tcb_queue_relation'_def , subst tcb_queue_relation_restrict, rule refl) 209 210 also have "\<dots> = tcb_queue_relation' getNext getPrev (mp' |` (tcb_ptr_to_ctcb_ptr ` set queue')) queue' qhead' qend'" 211 by (simp add: mpc cong: restrict_map_cong) 212 213 also have "\<dots> = ?RHS" 214 by (simp add: tcb_queue_relation'_def tcb_queue_relation_restrict [symmetric]) 215 216 finally show ?thesis . 217qed 218 219 220(* MOVE *) 221lemma tcb_aligned': 222 "tcb_at' t s \<Longrightarrow> is_aligned t tcbBlockSizeBits" 223 apply (drule obj_at_aligned') 224 apply (simp add: objBits_simps) 225 apply (simp add: objBits_simps) 226 done 227 228lemma tcb_at_not_NULL: 229 assumes tat: "tcb_at' t s" 230 shows "tcb_ptr_to_ctcb_ptr t \<noteq> NULL" 231proof 232 assume "tcb_ptr_to_ctcb_ptr t = NULL" 233 with tat have "tcb_at' (ctcb_ptr_to_tcb_ptr NULL) s" 234 apply - 235 apply (erule subst) 236 apply simp 237 done 238 239 hence "is_aligned (ctcb_ptr_to_tcb_ptr NULL) tcbBlockSizeBits" 240 by (rule tcb_aligned') 241 242 moreover have "ctcb_ptr_to_tcb_ptr NULL !! ctcb_size_bits" 243 unfolding ctcb_ptr_to_tcb_ptr_def ctcb_offset_defs 244 by simp 245 ultimately show False by (simp add: is_aligned_nth ctcb_offset_defs objBits_defs) 246qed 247 248lemma tcb_queue_relation_not_NULL: 249 assumes tq: "tcb_queue_relation getNext getPrev mp queue qprev qhead" 250 and valid_ep: "\<forall>t\<in>set queue. tcb_at' t s" 251 shows "\<forall>t \<in> set queue. tcb_ptr_to_ctcb_ptr t \<noteq> NULL" 252proof (cases "queue = []") 253 case True thus ?thesis by simp 254next 255 case False 256 show ?thesis 257 proof (rule ballI, rule notI) 258 fix t 259 assume tq: "t \<in> set queue" and "tcb_ptr_to_ctcb_ptr t = NULL" 260 hence "ctcb_ptr_to_tcb_ptr NULL \<in> set queue" 261 apply - 262 apply (erule subst) 263 apply simp 264 done 265 266 with valid_ep(1) have "tcb_at' (ctcb_ptr_to_tcb_ptr NULL) s" .. 267 thus False 268 apply - 269 apply (drule tcb_at_not_NULL) 270 apply simp 271 done 272 qed 273qed 274 275lemmas tcb_queue_relation_not_NULL' = bspec [OF tcb_queue_relation_not_NULL] 276 277lemma tcb_queue_relation_head_hd: 278 assumes tq: "tcb_queue_relation getNext getPrev mp queue qprev qhead" 279 and tcbs: "queue \<noteq> []" 280 shows "ctcb_ptr_to_tcb_ptr qhead = hd queue" 281 using assms 282 apply (cases queue) 283 apply simp 284 apply simp 285 done 286 287lemma tcb_queue_relation_next_not_NULL: 288 assumes tq: "tcb_queue_relation getNext getPrev mp queue qprev qhead" 289 and valid_ep: "\<forall>t\<in>set queue. tcb_at' t s" "distinct queue" 290 and tcbs: "queue \<noteq> []" 291 shows "qhead \<noteq> NULL" 292proof - 293 have "ctcb_ptr_to_tcb_ptr qhead \<in> set queue" using tq tcbs 294 by (simp add: tcb_queue_relation_head_hd) 295 296 with tq valid_ep(1) have "tcb_ptr_to_ctcb_ptr (ctcb_ptr_to_tcb_ptr qhead) \<noteq> NULL" 297 by (rule tcb_queue_relation_not_NULL') 298 299 thus ?thesis by simp 300qed 301 302lemma tcb_queue_relation_ptr_rel: 303 assumes tq: "tcb_queue_relation getNext getPrev mp queue qprev qhead" 304 and valid_ep: "\<forall>t\<in>set queue. tcb_at' t s" "distinct queue" 305 and cs_tcb: "mp (tcb_ptr_to_ctcb_ptr tcbp) = Some tcb" 306 and prev_not_queue: "ctcb_ptr_to_tcb_ptr qprev \<notin> set queue" 307 and in_queue: "tcbp \<in> set queue" 308 shows "tcb_ptr_to_ctcb_ptr tcbp \<noteq> getNext tcb \<and> tcb_ptr_to_ctcb_ptr tcbp \<noteq> getPrev tcb 309 \<and> (getNext tcb \<noteq> NULL \<longrightarrow> getNext tcb \<noteq> getPrev tcb)" 310 using tq valid_ep in_queue cs_tcb prev_not_queue 311 apply - 312 apply (frule (3) tcb_queueD) 313 apply (frule (2) tcb_queue_relation_not_NULL') 314 apply (simp split: if_split_asm) 315 apply (rule not_sym) 316 apply (rule notI) 317 apply simp 318 apply (clarsimp simp: inj_eq distinct_conv_nth) 319 apply (intro conjI impI) 320 apply (clarsimp simp: inj_eq distinct_conv_nth) 321 apply (rule not_sym) 322 apply clarsimp 323 apply clarsimp 324 apply (clarsimp simp: inj_eq) 325 apply (intro conjI impI) 326 apply (clarsimp simp: distinct_conv_nth) 327 apply (erule_tac s = "queue ! Suc n" in subst) 328 apply (clarsimp simp: distinct_conv_nth) 329 apply clarsimp 330 apply (case_tac "na = Suc n") 331 apply hypsubst 332 apply (clarsimp simp: distinct_conv_nth) 333 apply (clarsimp simp: distinct_conv_nth) 334 done 335 336lemma distinct_cons_nth: 337 assumes dxs: "distinct xs" 338 and ln: "n < length xs" 339 and x: "x \<notin> set xs" 340 shows "(x # xs) ! n \<noteq> xs ! n" 341proof 342 assume n: "(x # xs) ! n = xs ! n" 343 have ln': "n < length (x # xs)" using ln by simp 344 have sln: "Suc n < length (x # xs)" using ln by simp 345 346 from n have "(x # xs) ! n = (x # xs) ! Suc n" by simp 347 moreover have "distinct (x # xs)" using dxs x by simp 348 ultimately show False 349 unfolding distinct_conv_nth 350 apply - 351 apply (drule spec, drule mp [OF _ ln']) 352 apply (drule spec, drule mp [OF _ sln]) 353 apply simp 354 done 355qed 356 357lemma distinct_nth: 358 assumes dist: "distinct xs" 359 and ln: "n < length xs" 360 and lm: "m < length xs" 361 shows "(xs ! n = xs ! m) = (n = m)" 362 using dist ln lm 363 apply (cases "n = m") 364 apply simp 365 apply (clarsimp simp: distinct_conv_nth) 366 done 367 368lemma distinct_nth_cons: 369 assumes dist: "distinct xs" 370 and xxs: "x \<notin> set xs" 371 and ln: "n < length xs" 372 and lm: "m < length xs" 373 shows "((x # xs) ! n = xs ! m) = (n = Suc m)" 374proof (cases "n = Suc m") 375 case True 376 thus ?thesis by simp 377next 378 case False 379 380 have ln': "n < length (x # xs)" using ln by simp 381 have lm': "Suc m < length (x # xs)" using lm by simp 382 383 have "distinct (x # xs)" using dist xxs by simp 384 thus ?thesis using False 385 unfolding distinct_conv_nth 386 apply - 387 apply (drule spec, drule mp [OF _ ln']) 388 apply (drule spec, drule mp [OF _ lm']) 389 apply clarsimp 390 done 391qed 392 393lemma distinct_nth_cons': 394 assumes dist: "distinct xs" 395 and xxs: "x \<notin> set xs" 396 and ln: "n < length xs" 397 and lm: "m < length xs" 398 shows "(xs ! n = (x # xs) ! m) = (m = Suc n)" 399proof (cases "m = Suc n") 400 case True 401 thus ?thesis by simp 402next 403 case False 404 405 have ln': "Suc n < length (x # xs)" using ln by simp 406 have lm': "m < length (x # xs)" using lm by simp 407 408 have "distinct (x # xs)" using dist xxs by simp 409 thus ?thesis using False 410 unfolding distinct_conv_nth 411 apply - 412 apply (drule spec, drule mp [OF _ ln']) 413 apply (drule spec, drule mp [OF _ lm']) 414 apply clarsimp 415 done 416qed 417 418lemma nth_first_not_member: 419 assumes xxs: "x \<notin> set xs" 420 and ln: "n < length xs" 421 shows "((x # xs) ! n = x) = (n = 0)" 422 using xxs ln 423 apply (cases n) 424 apply simp 425 apply clarsimp 426 done 427 428lemma tcb_queue_next_prev: 429 assumes qr: "tcb_queue_relation getNext getPrev mp queue qprev qhead" 430 and valid_ep: "\<forall>t\<in>set queue. tcb_at' t s" "distinct queue" 431 and tcb: "mp (tcb_ptr_to_ctcb_ptr tcbp) = Some tcb" 432 and tcb': "mp (tcb_ptr_to_ctcb_ptr tcbp') = Some tcb'" 433 and tq: "tcbp \<in> set queue" "tcbp' \<in> set queue" 434 and prev_not_queue: "ctcb_ptr_to_tcb_ptr qprev \<notin> set queue" 435 and tcbs: "tcbp \<noteq> tcbp'" 436 shows "(getNext tcb = tcb_ptr_to_ctcb_ptr tcbp') = 437 (getPrev tcb' = tcb_ptr_to_ctcb_ptr tcbp)" 438 using qr valid_ep prev_not_queue tq tcb tcb' tcbs 439 apply - 440 apply (frule (1) tcb_queueD) 441 apply (rule tq(1)) 442 apply (rule tcb) 443 apply (frule (1) tcb_queueD) 444 apply (rule tq(2)) 445 apply (rule tcb') 446 apply (cases queue) 447 apply simp 448 apply (cut_tac bspec [OF tcb_queue_relation_not_NULL, OF qr valid_ep(1) tq(1)]) 449 apply (cut_tac bspec [OF tcb_queue_relation_not_NULL, OF qr valid_ep(1) tq(2)]) 450 apply (simp add: inj_eq split: if_split_asm) 451 apply clarsimp 452 apply clarsimp 453 subgoal by (clarsimp simp: last_conv_nth distinct_nth distinct_nth_cons) 454 apply (clarsimp simp: last_conv_nth distinct_nth distinct_nth_cons) 455 apply (subgoal_tac "list ! Suc na \<noteq> tcbp'") 456 apply clarsimp 457 apply clarsimp 458 subgoal by (clarsimp simp: last_conv_nth distinct_nth distinct_nth_cons nth_first_not_member) 459 subgoal by (fastforce simp: last_conv_nth distinct_nth distinct_nth_cons nth_first_not_member) 460 subgoal by (clarsimp simp: last_conv_nth distinct_nth distinct_nth_cons distinct_nth_cons' nth_first_not_member) 461 by (fastforce simp: last_conv_nth distinct_nth distinct_nth_cons distinct_nth_cons' nth_first_not_member) 462 463 464lemma null_not_in: 465 "\<lbrakk>tcb_queue_relation getNext getPrev mp queue qprev qhead; \<forall>t\<in>set queue. tcb_at' t s; distinct queue\<rbrakk> 466 \<Longrightarrow> ctcb_ptr_to_tcb_ptr NULL \<notin> set queue" 467 apply - 468 apply (rule notI) 469 apply (drule (2) tcb_queue_relation_not_NULL') 470 apply simp 471 done 472 473lemma tcb_queue_relationI': 474 "\<lbrakk> tcb_queue_relation getNext getPrev hp queue NULL qhead; 475 qend = (if queue = [] then NULL else (tcb_ptr_to_ctcb_ptr (last queue))) \<rbrakk> 476 \<Longrightarrow> tcb_queue_relation' getNext getPrev hp queue qhead qend" 477 unfolding tcb_queue_relation'_def 478 by simp 479 480lemma tcb_queue_relationE': 481 "\<lbrakk> tcb_queue_relation' getNext getPrev hp queue qhead qend; 482 \<lbrakk> tcb_queue_relation getNext getPrev hp queue NULL qhead; 483 qend = (if queue = [] then NULL else (tcb_ptr_to_ctcb_ptr (last queue))) \<rbrakk> \<Longrightarrow> P \<rbrakk> \<Longrightarrow> P" 484 unfolding tcb_queue_relation'_def 485 by simp 486 487lemma tcb_queue_relation'_queue_rel: 488 "tcb_queue_relation' getNext getPrev hp queue qhead qend 489 \<Longrightarrow> tcb_queue_relation getNext getPrev hp queue NULL qhead" 490 unfolding tcb_queue_relation'_def 491 by simp 492 493lemma tcb_queue_singleton_iff: 494 assumes queue_rel: "tcb_queue_relation getNext getPrev mp queue NULL qhead" 495 and in_queue: "tcbp \<in> set queue" 496 and valid_ntfn: "\<forall>t\<in>set queue. tcb_at' t s" "distinct queue" 497 and cs_tcb: "mp (tcb_ptr_to_ctcb_ptr tcbp) = Some tcb" 498 shows "(queue = [tcbp]) = (getNext tcb = NULL \<and> getPrev tcb = NULL)" 499proof (rule iffI) 500 assume "queue = [tcbp]" 501 thus "(getNext tcb = NULL \<and> getPrev tcb = NULL)" using queue_rel cs_tcb 502 by clarsimp 503next 504 assume asms: "getNext tcb = NULL \<and> getPrev tcb = NULL" 505 hence "hd queue = tcbp" using queue_rel valid_ntfn in_queue cs_tcb 506 apply - 507 apply (drule (3) tcb_queueD) 508 apply (rule classical) 509 apply clarsimp 510 apply (cut_tac x = "queue ! n" in bspec [OF tcb_queue_relation_not_NULL [OF queue_rel valid_ntfn(1)]]) 511 apply clarsimp 512 apply simp 513 done 514 moreover have "last queue = tcbp" using queue_rel valid_ntfn in_queue cs_tcb asms 515 apply - 516 apply (drule (3) tcb_queueD) 517 apply (rule classical) 518 apply clarsimp 519 apply (cut_tac x = "queue ! Suc n" in bspec [OF tcb_queue_relation_not_NULL [OF queue_rel valid_ntfn(1)]]) 520 apply clarsimp 521 apply simp 522 done 523 moreover have "queue \<noteq> []" using in_queue by clarsimp 524 ultimately show "queue = [tcbp]" using valid_ntfn in_queue 525 apply clarsimp 526 apply (simp add: hd_conv_nth last_conv_nth nth_eq_iff_index_eq) 527 apply (cases queue) 528 apply simp 529 apply simp 530 done 531qed 532 533 534lemma distinct_remove1_take_drop: 535 "\<lbrakk> distinct ls; n < length ls \<rbrakk> \<Longrightarrow> remove1 (ls ! n) ls = (take n ls) @ drop (Suc n) ls" 536proof (induct ls arbitrary: n) 537 case Nil thus ?case by simp 538next 539 case (Cons x xs n) 540 541 show ?case 542 proof (cases n) 543 case 0 544 thus ?thesis by simp 545 next 546 case (Suc m) 547 548 hence "((x # xs) ! n) \<noteq> x" using Cons.prems by clarsimp 549 thus ?thesis using Suc Cons.prems by (clarsimp simp add: Cons.hyps) 550 qed 551qed 552 553 554definition 555 "upd_unless_null \<equiv> \<lambda>p v f. if p = NULL then f else fun_upd f p (Some v)" 556 557lemma upd_unless_null_cong_helper: 558 "\<And>p p' v mp S. \<lbrakk> p' \<in> tcb_ptr_to_ctcb_ptr ` S; ctcb_ptr_to_tcb_ptr p \<notin> S \<rbrakk> \<Longrightarrow> (upd_unless_null p v mp) p' = mp p'" 559 unfolding upd_unless_null_def 560 apply simp 561 apply (intro impI conjI) 562 apply (erule imageE) 563 apply hypsubst 564 apply (simp only: ctcb_ptr_to_ctcb_ptr) 565 apply blast 566 done 567 568lemma tcbDequeue_update0: 569 assumes in_queue: "tcbp \<in> set queue" 570 and valid_ntfn: "\<forall>t\<in>set queue. tcb_at' t s" "distinct queue" 571 and queue_rel: "tcb_queue_relation tn tp mp queue qprev qhead" 572 and prev_not_queue: "ctcb_ptr_to_tcb_ptr qprev \<notin> set queue" 573 and cs_tcb: "mp (tcb_ptr_to_ctcb_ptr tcbp) = Some tcb" 574 and f: "\<And>v f g. tn (tn_update f v) = f (tn v) \<and> tp (tp_update g v) = g (tp v) 575 \<and> tn (tp_update f v) = tn v \<and> tp (tn_update g v) = tp v" 576 shows "tcb_queue_relation tn tp 577 (upd_unless_null (tn tcb) (tp_update (\<lambda>_. tp tcb) (the (mp (tn tcb)))) 578 (upd_unless_null (tp tcb) (tn_update (\<lambda>_. tn tcb) (the (mp (tp tcb)))) mp)) 579 (remove1 tcbp queue) 580 (if tcb_ptr_to_ctcb_ptr tcbp = qhead then tp tcb else qprev) 581 (if tcb_ptr_to_ctcb_ptr tcbp = qhead then tn tcb else qhead)" 582 (is "tcb_queue_relation tn tp ?mp (remove1 tcbp queue) (?qprev qprev qhead) (?qhead qhead)") 583 using queue_rel valid_ntfn prev_not_queue in_queue 584proof (induct queue arbitrary: qprev qhead) 585 case Nil 586 thus ?case by simp 587next 588 case (Cons tcb' tcbs qprev' qhead') 589 590 have "tcbp = tcb' \<or> tcbp \<in> set tcbs" using Cons.prems by simp 591 thus ?case 592 proof 593 assume tcbp: "tcbp = tcb'" 594 hence qp: "qprev' = tp tcb" and qh: "qhead' = tcb_ptr_to_ctcb_ptr tcb'" 595 using Cons.prems cs_tcb by auto 596 597 from Cons.prems have tq: "tcb_queue_relation tn tp mp tcbs (tcb_ptr_to_ctcb_ptr tcb') (tn tcb)" 598 using Cons.prems cs_tcb tcbp by clarsimp 599 600 note ind_prems = Cons.prems 601 note ind_hyp = Cons.hyps 602 603 show ?thesis 604 proof (cases tcbs) 605 case Nil thus ?thesis using Cons.prems tcbp cs_tcb by clarsimp 606 next 607 case (Cons tcbs_hd tcbss) 608 609 have nnull: "tn tcb \<noteq> NULL" using tq 610 proof (rule tcb_queue_relation_next_not_NULL) 611 from ind_prems show "\<forall>t\<in>set tcbs. tcb_at' t s" 612 and "distinct tcbs" by simp_all 613 show "tcbs \<noteq> []" using Cons by simp 614 qed 615 616 from Cons ind_prems have "tcbs_hd \<notin> set tcbss" by simp 617 hence mpeq: "\<And>p. p \<in> tcb_ptr_to_ctcb_ptr ` set tcbss \<Longrightarrow> ?mp p = mp p" 618 using tq cs_tcb tcbp Cons nnull ind_prems 619 apply - 620 apply (subst upd_unless_null_cong_helper, assumption, clarsimp)+ 621 apply simp 622 done 623 624 have "tcb_ptr_to_ctcb_ptr tcbp \<noteq> tn tcb \<and> tcb_ptr_to_ctcb_ptr tcbp \<noteq> tp tcb 625 \<and> tn tcb \<noteq> tp tcb" using tq cs_tcb ind_prems nnull 626 apply - 627 apply (drule (5) tcb_queue_relation_ptr_rel) 628 apply clarsimp 629 done 630 631 hence "?mp (tcb_ptr_to_ctcb_ptr tcbs_hd) = Some (tp_update (\<lambda>_. tp tcb) (the (mp (tn tcb))))" 632 using qp qh tq cs_tcb tcbp Cons nnull 633 by (simp add: upd_unless_null_def) 634 635 thus ?thesis using qp qh tq cs_tcb tcbp Cons nnull 636 apply (simp (no_asm) add: tcbp Cons split del: if_split) 637 apply (subst tcb_queue_relation_cong [OF refl refl refl mpeq]) 638 apply assumption 639 apply (clarsimp simp: f) 640 done 641 qed 642 next 643 assume inset: "tcbp \<in> set tcbs" 644 hence tcbp: "tcbp \<noteq> tcb'" using Cons.prems by clarsimp 645 646 obtain tcb2 where cs_tcb2: "mp (tcb_ptr_to_ctcb_ptr tcb') = Some tcb2" 647 and rel2: "tcb_queue_relation tn tp mp tcbs (tcb_ptr_to_ctcb_ptr tcb') (tn tcb2)" 648 and qh: "qhead' = tcb_ptr_to_ctcb_ptr tcb'" 649 and qp: "qprev' = tp tcb2" 650 using Cons.prems 651 by clarsimp 652 653 have nnull: "tcb_ptr_to_ctcb_ptr tcb' \<noteq> NULL" using Cons.prems 654 apply - 655 apply (erule (1) tcb_queue_relation_not_NULL') 656 apply simp 657 done 658 659 have ih: "tcb_queue_relation tn tp ?mp (remove1 tcbp tcbs) 660 (?qprev (tcb_ptr_to_ctcb_ptr tcb') (tn tcb2)) 661 (?qhead (tn tcb2))" using rel2 662 proof (rule Cons.hyps) 663 from Cons.prems show "\<forall>t\<in>set tcbs. tcb_at' t s" 664 and "distinct tcbs" 665 and "ctcb_ptr_to_tcb_ptr (tcb_ptr_to_ctcb_ptr tcb') \<notin> set tcbs" by simp_all 666 qed fact 667 668 have tcb_next: "tn tcb \<noteq> tcb_ptr_to_ctcb_ptr tcb'" 669 using Cons.prems tcb_queue_next_prev[OF Cons.prems(1), OF _ _ cs_tcb cs_tcb2] 670 tcbp qp[symmetric] 671 by auto 672 673 show ?thesis using tcbp 674 proof (cases "tn tcb2 = tcb_ptr_to_ctcb_ptr tcbp") 675 case True 676 hence tcb_prev: "tp tcb = tcb_ptr_to_ctcb_ptr tcb'" using Cons.prems cs_tcb2 cs_tcb not_sym [OF tcbp] 677 apply - 678 apply (subst tcb_queue_next_prev [symmetric], assumption+) 679 apply simp 680 apply simp 681 apply simp 682 apply (rule not_sym [OF tcbp]) 683 apply simp 684 done 685 686 hence "?mp (tcb_ptr_to_ctcb_ptr tcb') = Some (tn_update (\<lambda>_. tn tcb) tcb2)" 687 using tcb_next nnull cs_tcb2 unfolding upd_unless_null_def by simp 688 689 thus ?thesis using tcbp cs_tcb qh qp True ih tcb_prev 690 by (simp add: inj_eq f) 691 next 692 case False 693 hence tcb_prev: "tp tcb \<noteq> tcb_ptr_to_ctcb_ptr tcb'" 694 using Cons.prems cs_tcb2 cs_tcb not_sym [OF tcbp] 695 apply - 696 apply (subst tcb_queue_next_prev [symmetric], assumption+) 697 apply simp 698 apply simp 699 apply simp 700 apply (rule not_sym [OF tcbp]) 701 apply simp 702 done 703 hence "?mp (tcb_ptr_to_ctcb_ptr tcb') = Some tcb2" 704 using tcb_next nnull cs_tcb2 unfolding upd_unless_null_def by simp 705 706 thus ?thesis using tcbp cs_tcb qh qp False ih tcb_prev 707 by (simp add: inj_eq) 708 qed 709 qed 710qed 711 712lemma tcbDequeue_update: 713 assumes queue_rel: "tcb_queue_relation' tn tp mp queue qhead qend" 714 and in_queue: "tcbp \<in> set queue" 715 and valid_ntfn: "\<forall>t\<in>set queue. tcb_at' t s" "distinct queue" 716 and cs_tcb: "mp (tcb_ptr_to_ctcb_ptr tcbp) = Some tcb" 717 and f: "\<And>v f g. tn (tn_update f v) = f (tn v) \<and> tp (tp_update g v) = g (tp v) 718 \<and> tn (tp_update f v) = tn v \<and> tp (tn_update g v) = tp v" 719 shows "tcb_queue_relation' tn tp 720 (upd_unless_null (tn tcb) (tp_update (\<lambda>_. tp tcb) (the (mp (tn tcb)))) 721 (upd_unless_null (tp tcb) (tn_update (\<lambda>_. tn tcb) (the (mp (tp tcb)))) mp)) 722 (remove1 tcbp queue) 723 (if tp tcb = NULL then tn tcb else qhead) 724 (if tn tcb = NULL then tp tcb else qend)" 725proof - 726 have ne: "NULL = (if tcb_ptr_to_ctcb_ptr tcbp = qhead then tp tcb else NULL)" 727 using queue_rel in_queue cs_tcb 728 apply - 729 apply (drule tcb_queue_relation'_queue_rel) 730 apply (clarsimp split: if_split) 731 apply (cases queue) 732 apply simp 733 apply clarsimp 734 done 735 736 have if2: "(if tp tcb = NULL then tn tcb else qhead) = 737 (if tcb_ptr_to_ctcb_ptr tcbp = qhead then tn tcb else qhead)" 738 using tcb_queue_relation'_queue_rel [OF queue_rel] in_queue cs_tcb valid_ntfn 739 apply - 740 apply (cases queue) 741 apply simp 742 apply (frule (3) tcb_queueD) 743 apply (simp add: inj_eq) 744 apply (intro impI) 745 apply simp 746 apply (elim conjE exE) 747 apply (cut_tac x = "queue ! n" 748 in bspec [OF tcb_queue_relation_not_NULL [OF tcb_queue_relation'_queue_rel [OF queue_rel] valid_ntfn(1)]]) 749 apply (rule nth_mem) 750 apply clarsimp 751 apply clarsimp 752 done 753 754 note null_not_in' = null_not_in [OF tcb_queue_relation'_queue_rel [OF queue_rel] valid_ntfn(1) valid_ntfn(2)] 755 756 show ?thesis 757 proof (rule tcb_queue_relationI') 758 show "tcb_queue_relation tn tp 759 (upd_unless_null (tn tcb) 760 (tp_update (\<lambda>_. tp tcb) (the (mp (tn tcb)))) 761 (upd_unless_null (tp tcb) 762 (tn_update (\<lambda>_. tn tcb) (the (mp (tp tcb)))) mp)) 763 (remove1 tcbp queue) NULL 764 (if tp tcb = NULL then tn tcb else qhead)" 765 using in_queue valid_ntfn tcb_queue_relation'_queue_rel [OF queue_rel] null_not_in' cs_tcb 766 by (subst ne, subst if2, rule tcbDequeue_update0[rotated -1, OF f]) 767 next 768 have r1: "(remove1 tcbp queue = []) = (tn tcb = NULL \<and> tp tcb = NULL)" 769 using in_queue tcb_queue_relation'_queue_rel [OF queue_rel] cs_tcb valid_ntfn null_not_in' 770 apply - 771 apply (subst tcb_queue_singleton_iff [symmetric], assumption+) 772 apply (fastforce simp: remove1_empty) 773 done 774 have "queue \<noteq> []" using in_queue by clarsimp 775 thus "(if tn tcb = NULL then tp tcb else qend) = 776 (if remove1 tcbp queue = [] then NULL else tcb_ptr_to_ctcb_ptr (last (remove1 tcbp queue)))" 777 using queue_rel in_queue cs_tcb valid_ntfn 778 tcb_queue_relation_not_NULL [OF tcb_queue_relation'_queue_rel [OF queue_rel] valid_ntfn(1)] 779 apply - 780 apply (erule tcb_queue_relationE') 781 apply (frule (3) tcb_queueD) 782 apply (subst r1) 783 apply simp 784 apply (intro impI conjI) 785 apply (subgoal_tac "tcbp = last queue") 786 apply simp 787 apply (subgoal_tac "(remove1 (last queue) queue) \<noteq> []") 788 apply (clarsimp simp: inj_eq last_conv_nth nth_eq_iff_index_eq length_remove1 789 distinct_remove1_take_drop split: if_split_asm) 790 apply arith 791 apply (clarsimp simp: remove1_empty last_conv_nth hd_conv_nth nth_eq_iff_index_eq not_le split: if_split_asm) 792 apply (cases queue) 793 apply simp 794 apply simp 795 apply (fastforce simp: inj_eq split: if_split_asm) 796 apply (clarsimp simp: last_conv_nth distinct_remove1_take_drop nth_eq_iff_index_eq inj_eq split: if_split_asm) 797 apply arith 798 apply (simp add: nth_append min_def nth_eq_iff_index_eq) 799 apply clarsimp 800 apply arith 801 done 802 qed 803qed 804 805lemmas tcbEPDequeue_update 806 = tcbDequeue_update[where tn=tcbEPNext_C and tn_update=tcbEPNext_C_update 807 and tp=tcbEPPrev_C and tp_update=tcbEPPrev_C_update, 808 simplified] 809 810lemma tcb_queue_relation_ptr_rel': 811 assumes tq: "tcb_queue_relation getNext getPrev mp queue NULL qhead" 812 and valid_ep: "\<forall>t\<in>set queue. tcb_at' t s" "distinct queue" 813 and cs_tcb: "mp (tcb_ptr_to_ctcb_ptr tcbp) = Some tcb" 814 and in_queue: "tcbp \<in> set queue" 815 shows "tcb_ptr_to_ctcb_ptr tcbp \<noteq> getNext tcb \<and> tcb_ptr_to_ctcb_ptr tcbp \<noteq> getPrev tcb 816 \<and> (getNext tcb \<noteq> NULL \<longrightarrow> getNext tcb \<noteq> getPrev tcb)" 817 using tq valid_ep cs_tcb null_not_in [OF tq valid_ep(1) valid_ep(2)] in_queue 818 by (rule tcb_queue_relation_ptr_rel) 819 820lemma tcb_queue_head_empty_iff: 821 "\<lbrakk> tcb_queue_relation getNext getPrev mp queue NULL qhead; \<forall>t \<in> set queue. tcb_at' t s \<rbrakk> \<Longrightarrow> 822 (qhead = NULL) = (queue = [])" 823 apply (rule classical) 824 apply (cases queue) 825 apply simp 826 apply (frule (1) tcb_queue_relation_not_NULL) 827 apply clarsimp 828 done 829 830lemma ctcb_ptr_to_tcb_ptr_aligned: 831 assumes al: "is_aligned (ctcb_ptr_to_tcb_ptr ptr) tcbBlockSizeBits" 832 shows "is_aligned (ptr_val ptr) ctcb_size_bits" 833proof - 834 have "is_aligned (ptr_val (tcb_ptr_to_ctcb_ptr (ctcb_ptr_to_tcb_ptr ptr))) ctcb_size_bits" 835 unfolding tcb_ptr_to_ctcb_ptr_def using al 836 apply simp 837 apply (erule aligned_add_aligned) 838 apply (unfold ctcb_offset_defs, rule is_aligned_triv) 839 apply (simp add: word_bits_conv objBits_defs)+ 840 done 841 thus ?thesis by simp 842qed 843 844lemma ctcb_size_bits_ge_4: "4 \<le> ctcb_size_bits" 845 by (simp add: ctcb_size_bits_def) 846 847lemma tcb_queue_relation_next_mask: 848 assumes tq: "tcb_queue_relation getNext getPrev mp queue NULL qhead" 849 and valid_ep: "\<forall>t\<in>set queue. tcb_at' t s" "distinct queue" 850 and cs_tcb: "mp (tcb_ptr_to_ctcb_ptr tcbp) = Some tcb" 851 and in_queue: "tcbp \<in> set queue" 852 and bits: "bits \<le> ctcb_size_bits" 853 shows "ptr_val (getNext tcb) && ~~ mask bits = ptr_val (getNext tcb)" 854proof (cases "(getNext tcb) = NULL") 855 case True 856 thus ?thesis by simp 857next 858 case False 859 860 hence "ctcb_ptr_to_tcb_ptr (getNext tcb) \<in> set queue" using assms 861 apply - 862 apply (drule (3) tcb_queueD) 863 apply (clarsimp split: if_split_asm) 864 done 865 866 with valid_ep(1) have "tcb_at' (ctcb_ptr_to_tcb_ptr (getNext tcb)) s" .. 867 hence "is_aligned (ctcb_ptr_to_tcb_ptr (getNext tcb)) tcbBlockSizeBits" by (rule tcb_aligned') 868 hence "is_aligned (ptr_val (getNext tcb)) ctcb_size_bits" by (rule ctcb_ptr_to_tcb_ptr_aligned) 869 thus ?thesis using bits by (simp add: is_aligned_neg_mask) 870qed 871 872lemma tcb_queue_relation_prev_mask: 873 assumes tq: "tcb_queue_relation getNext getPrev mp queue NULL qhead" 874 and valid_ep: "\<forall>t\<in>set queue. tcb_at' t s" "distinct queue" 875 and cs_tcb: "mp (tcb_ptr_to_ctcb_ptr tcbp) = Some tcb" 876 and in_queue: "tcbp \<in> set queue" 877 and bits: "bits \<le> ctcb_size_bits" 878 shows "ptr_val (getPrev tcb) && ~~ mask bits = ptr_val (getPrev tcb)" 879proof (cases "(getPrev tcb) = NULL") 880 case True 881 thus ?thesis by simp 882next 883 case False 884 885 hence "ctcb_ptr_to_tcb_ptr (getPrev tcb) \<in> set queue" using assms 886 apply - 887 apply (drule (3) tcb_queueD) 888 apply (clarsimp split: if_split_asm) 889 done 890 891 with valid_ep(1) have "tcb_at' (ctcb_ptr_to_tcb_ptr (getPrev tcb)) s" .. 892 hence "is_aligned (ctcb_ptr_to_tcb_ptr (getPrev tcb)) tcbBlockSizeBits" by (rule tcb_aligned') 893 hence "is_aligned (ptr_val (getPrev tcb)) ctcb_size_bits" by (rule ctcb_ptr_to_tcb_ptr_aligned) 894 thus ?thesis using bits by (simp add: is_aligned_neg_mask) 895qed 896 897lemma tcb_queue_relation'_next_mask: 898 assumes tq: "tcb_queue_relation' getNext getPrev mp queue qhead qend" 899 and valid_ep: "\<forall>t\<in>set queue. tcb_at' t s" "distinct queue" 900 and cs_tcb: "mp (tcb_ptr_to_ctcb_ptr tcbp) = Some tcb" 901 and in_queue: "tcbp \<in> set queue" 902 and bits: "bits \<le> ctcb_size_bits" 903 shows "ptr_val (getNext tcb) && ~~ mask bits = ptr_val (getNext tcb)" 904 by (rule tcb_queue_relation_next_mask [OF tcb_queue_relation'_queue_rel], fact+) 905 906lemma tcb_queue_relation'_prev_mask: 907 assumes tq: "tcb_queue_relation' getNext getPrev mp queue qhead qend" 908 and valid_ep: "\<forall>t\<in>set queue. tcb_at' t s" "distinct queue" 909 and cs_tcb: "mp (tcb_ptr_to_ctcb_ptr tcbp) = Some tcb" 910 and in_queue: "tcbp \<in> set queue" 911 and bits: "bits \<le> ctcb_size_bits" 912 shows "ptr_val (getPrev tcb) && ~~ mask bits = ptr_val (getPrev tcb)" 913 by (rule tcb_queue_relation_prev_mask [OF tcb_queue_relation'_queue_rel], fact+) 914 915lemma tcb_queue_relation_next_sign: 916 assumes 917 "tcb_queue_relation getNext getPrev mp queue NULL qhead" and 918 valid_ep: "\<forall>t\<in>set queue. tcb_at' t s" 919 "distinct queue" 920 "mp (tcb_ptr_to_ctcb_ptr tcbp) = Some tcb" 921 "tcbp \<in> set queue" and 922 canon: "pspace_canonical' s" 923 shows "sign_extend 47 (ptr_val (getNext tcb)) = ptr_val (getNext tcb)" 924proof (cases "(getNext tcb) = NULL") 925 case True 926 thus ?thesis by simp 927next 928 case False 929 930 hence "ctcb_ptr_to_tcb_ptr (getNext tcb) \<in> set queue" using assms 931 apply - 932 apply (drule (3) tcb_queueD) 933 apply (clarsimp split: if_split_asm) 934 done 935 936 with valid_ep(1) have tcb: "tcb_at' (ctcb_ptr_to_tcb_ptr (getNext tcb)) s" .. 937 with canon have "canonical_address (ctcb_ptr_to_tcb_ptr (getNext tcb))" by (simp add: obj_at'_is_canonical) 938 moreover 939 have "is_aligned (ctcb_ptr_to_tcb_ptr (getNext tcb)) tcbBlockSizeBits" using tcb by (rule tcb_aligned') 940 ultimately 941 have "canonical_address (ptr_val (getNext tcb))" by (rule canonical_address_ctcb_ptr) 942 thus ?thesis 943 by (simp add: sign_extend_canonical_address[symmetric]) 944qed 945 946lemma tcb_queue_relation'_next_sign: 947 "\<lbrakk> tcb_queue_relation' getNext getPrev mp queue qhead qend; \<forall>t\<in>set queue. tcb_at' t s; 948 distinct queue; mp (tcb_ptr_to_ctcb_ptr tcbp) = Some tcb; tcbp \<in> set queue; pspace_canonical' s\<rbrakk> 949\<Longrightarrow> sign_extend 47 (ptr_val (getNext tcb)) = ptr_val (getNext tcb)" 950 by (rule tcb_queue_relation_next_sign [OF tcb_queue_relation'_queue_rel]) 951 952lemma tcb_queue_relation_prev_sign: 953 assumes 954 "tcb_queue_relation getNext getPrev mp queue NULL qhead" and 955 valid_ep: "\<forall>t\<in>set queue. tcb_at' t s" 956 "distinct queue" 957 "mp (tcb_ptr_to_ctcb_ptr tcbp) = Some tcb" 958 "tcbp \<in> set queue" and 959 canon: "pspace_canonical' s" 960 shows "sign_extend 47 (ptr_val (getPrev tcb)) = ptr_val (getPrev tcb)" 961proof (cases "(getPrev tcb) = NULL") 962 case True 963 thus ?thesis by simp 964next 965 case False 966 967 hence "ctcb_ptr_to_tcb_ptr (getPrev tcb) \<in> set queue" using assms 968 apply - 969 apply (drule (3) tcb_queueD) 970 apply (clarsimp split: if_split_asm) 971 done 972 973 with valid_ep(1) have tcb: "tcb_at' (ctcb_ptr_to_tcb_ptr (getPrev tcb)) s" .. 974 with canon have "canonical_address (ctcb_ptr_to_tcb_ptr (getPrev tcb))" by (simp add: obj_at'_is_canonical) 975 moreover 976 have "is_aligned (ctcb_ptr_to_tcb_ptr (getPrev tcb)) tcbBlockSizeBits" using tcb by (rule tcb_aligned') 977 ultimately 978 have "canonical_address (ptr_val (getPrev tcb))" by (rule canonical_address_ctcb_ptr) 979 thus ?thesis 980 by (simp add: sign_extend_canonical_address[symmetric]) 981qed 982 983lemma tcb_queue_relation'_prev_sign: 984 "\<lbrakk> tcb_queue_relation' getNext getPrev mp queue qhead qend; \<forall>t\<in>set queue. tcb_at' t s; 985 distinct queue; mp (tcb_ptr_to_ctcb_ptr tcbp) = Some tcb; tcbp \<in> set queue; pspace_canonical' s\<rbrakk> 986\<Longrightarrow> sign_extend 47 (ptr_val (getPrev tcb)) = ptr_val (getPrev tcb)" 987 by (rule tcb_queue_relation_prev_sign [OF tcb_queue_relation'_queue_rel]) 988 989 990lemma cready_queues_relation_null_queue_ptrs: 991 assumes rel: "cready_queues_relation mp cq aq" 992 and same: "option_map tcb_null_ep_ptrs \<circ> mp' = option_map tcb_null_ep_ptrs \<circ> mp" 993 shows "cready_queues_relation mp' cq aq" 994 using rel 995 apply (clarsimp simp: cready_queues_relation_def Let_def all_conj_distrib) 996 apply (drule spec, drule spec, drule mp, (erule conjI)+, assumption) 997 apply (clarsimp simp: tcb_queue_relation'_def) 998 apply (erule iffD2 [OF tcb_queue_relation_only_next_prev, rotated -1]) 999 apply (rule ext) 1000 apply (case_tac "mp' x") 1001 apply (frule compD [OF same]) 1002 apply simp 1003 apply (frule compD [OF same]) 1004 apply (clarsimp simp: tcb_null_ep_ptrs_def) 1005 apply (case_tac z, case_tac a) 1006 apply simp 1007 \<comment> \<open>clag\<close> 1008 apply (rule ext) 1009 apply (case_tac "mp' x") 1010 apply (frule compD [OF same]) 1011 apply simp 1012 apply (frule compD [OF same]) 1013 apply (clarsimp simp: tcb_null_ep_ptrs_def) 1014 apply (case_tac z, case_tac a) 1015 apply simp 1016 done 1017 1018lemma cready_queues_relation_not_queue_ptrs: 1019 assumes rel: "cready_queues_relation mp cq aq" 1020 and same: "option_map tcbSchedNext_C \<circ> mp' = option_map tcbSchedNext_C \<circ> mp" 1021 "option_map tcbSchedPrev_C \<circ> mp' = option_map tcbSchedPrev_C \<circ> mp" 1022 shows "cready_queues_relation mp' cq aq" 1023 using rel 1024 apply (clarsimp simp: cready_queues_relation_def tcb_queue_relation'_def Let_def all_conj_distrib) 1025 apply (drule spec, drule spec, drule mp, (erule conjI)+, assumption) 1026 apply clarsimp 1027 apply (erule iffD2 [OF tcb_queue_relation_only_next_prev, rotated -1]) 1028 apply (rule same) 1029 apply (rule same) 1030 done 1031 1032lemma ntfn_ep_disjoint: 1033 assumes srs: "sym_refs (state_refs_of' s)" 1034 and epat: "ko_at' ep epptr s" 1035 and ntfnat: "ko_at' ntfn ntfnptr s" 1036 and ntfnq: "isWaitingNtfn (ntfnObj ntfn)" 1037 and epq: "isSendEP ep \<or> isRecvEP ep" 1038 shows "set (epQueue ep) \<inter> set (ntfnQueue (ntfnObj ntfn)) = {}" 1039 using srs epat ntfnat ntfnq epq 1040 apply - 1041 apply (subst disjoint_iff_not_equal, intro ballI, rule notI) 1042 apply (drule sym_refs_ko_atD', clarsimp)+ 1043 apply clarsimp 1044 apply (clarsimp simp: isWaitingNtfn_def isSendEP_def isRecvEP_def 1045 split: ntfn.splits endpoint.splits) 1046 apply (drule bspec, fastforce simp: ko_wp_at'_def)+ 1047 apply (fastforce simp: ko_wp_at'_def refs_of_rev') 1048 apply (drule bspec, fastforce simp: ko_wp_at'_def)+ 1049 apply (fastforce simp: ko_wp_at'_def refs_of_rev') 1050 done 1051 1052lemma ntfn_ntfn_disjoint: 1053 assumes srs: "sym_refs (state_refs_of' s)" 1054 and ntfnat: "ko_at' ntfn ntfnptr s" 1055 and ntfnat': "ko_at' ntfn' ntfnptr' s" 1056 and ntfnq: "isWaitingNtfn (ntfnObj ntfn)" 1057 and ntfnq': "isWaitingNtfn (ntfnObj ntfn')" 1058 and neq: "ntfnptr' \<noteq> ntfnptr" 1059 shows "set (ntfnQueue (ntfnObj ntfn)) \<inter> set (ntfnQueue (ntfnObj ntfn')) = {}" 1060 using srs ntfnat ntfnat' ntfnq ntfnq' neq 1061 apply - 1062 apply (subst disjoint_iff_not_equal, intro ballI, rule notI) 1063 apply (drule sym_refs_ko_atD', clarsimp)+ 1064 apply clarsimp 1065 apply (clarsimp simp: isWaitingNtfn_def split: ntfn.splits) 1066 apply (drule bspec, fastforce simp: ko_wp_at'_def)+ 1067 apply (clarsimp simp: ko_wp_at'_def refs_of_rev') 1068 done 1069 1070lemma tcb_queue_relation'_empty[simp]: 1071 "tcb_queue_relation' getNext getPrev mp [] qhead qend = 1072 (qend = tcb_Ptr 0 \<and> qhead = tcb_Ptr 0)" 1073 by (simp add: tcb_queue_relation'_def) 1074 1075lemma cnotification_relation_ntfn_queue: 1076 fixes ntfn :: "Structures_H.notification" 1077 defines "qs \<equiv> if isWaitingNtfn (ntfnObj ntfn) then set (ntfnQueue (ntfnObj ntfn)) else {}" 1078 assumes ntfn: "cnotification_relation (cslift t) ntfn' b" 1079 and srs: "sym_refs (state_refs_of' s)" 1080 and koat: "ko_at' ntfn ntfnptr s" 1081 and koat': "ko_at' ntfn' ntfnptr' s" 1082 and mpeq: "(cslift t' |` (- (tcb_ptr_to_ctcb_ptr ` qs))) = (cslift t |` (- (tcb_ptr_to_ctcb_ptr ` qs)))" 1083 and neq: "ntfnptr' \<noteq> ntfnptr" 1084 shows "cnotification_relation (cslift t') ntfn' b" 1085proof - 1086 have rl: "\<And>p. \<lbrakk> p \<in> tcb_ptr_to_ctcb_ptr ` set (ntfnQueue (ntfnObj ntfn')); 1087 isWaitingNtfn (ntfnObj ntfn); isWaitingNtfn (ntfnObj ntfn')\<rbrakk> 1088 \<Longrightarrow> cslift t p = cslift t' p" using srs koat' koat mpeq neq 1089 apply - 1090 apply (drule (3) ntfn_ntfn_disjoint [OF _ koat koat']) 1091 apply (erule restrict_map_eqI [symmetric]) 1092 apply (erule imageE) 1093 apply (fastforce simp: disjoint_iff_not_equal inj_eq qs_def) 1094 done 1095 1096 show ?thesis using ntfn rl mpeq unfolding cnotification_relation_def 1097 apply (simp add: Let_def) 1098 apply (cases "ntfnObj ntfn'") 1099 apply simp 1100 apply simp 1101 apply (cases "isWaitingNtfn (ntfnObj ntfn)") 1102 apply (simp add: isWaitingNtfn_def cong: tcb_queue_relation'_cong) 1103 apply (simp add: qs_def) 1104 done 1105qed 1106 1107lemma cpspace_relation_ntfn_update_ntfn: 1108 fixes ntfn :: "Structures_H.notification" 1109 defines "qs \<equiv> if isWaitingNtfn (ntfnObj ntfn) then set (ntfnQueue (ntfnObj ntfn)) else {}" 1110 assumes koat: "ko_at' ntfn ntfnptr s" 1111 and invs: "invs' s" 1112 and cp: "cpspace_ntfn_relation (ksPSpace s) (t_hrs_' (globals t))" 1113 and rel: "cnotification_relation (cslift t') ntfn' notification" 1114 and mpeq: "(cslift t' |` (- (tcb_ptr_to_ctcb_ptr ` qs))) = (cslift t |` (- (tcb_ptr_to_ctcb_ptr ` qs)))" 1115 shows "cmap_relation (map_to_ntfns (ksPSpace s(ntfnptr \<mapsto> KONotification ntfn'))) 1116 (cslift t(Ptr ntfnptr \<mapsto> notification)) Ptr (cnotification_relation (cslift t'))" 1117 using koat invs cp rel 1118 apply - 1119 apply (subst map_comp_update) 1120 apply (simp add: projectKO_opts_defs) 1121 apply (frule ko_at_projectKO_opt) 1122 apply (rule cmap_relationE1, assumption+) 1123 apply (erule (3) cmap_relation_upd_relI) 1124 apply (erule (1) cnotification_relation_ntfn_queue [OF _ invs_sym' koat]) 1125 apply (erule (1) map_to_ko_atI') 1126 apply (fold qs_def, rule mpeq) 1127 apply assumption 1128 apply simp 1129 done 1130 1131lemma cendpoint_relation_upd_tcb_no_queues: 1132 assumes cs: "mp thread = Some tcb" 1133 and next_pres: "option_map tcbEPNext_C \<circ> mp = option_map tcbEPNext_C \<circ> mp'" 1134 and prev_pres: "option_map tcbEPPrev_C \<circ> mp = option_map tcbEPPrev_C \<circ> mp'" 1135 shows "cendpoint_relation mp a b = cendpoint_relation mp' a b" 1136proof - 1137 show ?thesis 1138 unfolding cendpoint_relation_def 1139 apply (simp add: Let_def) 1140 apply (cases a) 1141 apply (simp add: tcb_queue_relation'_def tcb_queue_relation_only_next_prev [OF next_pres prev_pres, symmetric])+ 1142 done 1143qed 1144 1145lemma cnotification_relation_upd_tcb_no_queues: 1146 assumes cs: "mp thread = Some tcb" 1147 and next_pres: "option_map tcbEPNext_C \<circ> mp = option_map tcbEPNext_C \<circ> mp'" 1148 and prev_pres: "option_map tcbEPPrev_C \<circ> mp = option_map tcbEPPrev_C \<circ> mp'" 1149 shows "cnotification_relation mp a b = cnotification_relation mp' a b" 1150proof - 1151 show ?thesis 1152 unfolding cnotification_relation_def 1153 apply (simp add: Let_def) 1154 apply (cases "ntfnObj a") 1155 apply (simp add: tcb_queue_relation'_def tcb_queue_relation_only_next_prev [OF next_pres prev_pres, symmetric])+ 1156 done 1157qed 1158 1159lemma cendpoint_relation_ntfn_queue: 1160 assumes srs: "sym_refs (state_refs_of' s)" 1161 and koat: "ko_at' ntfn ntfnptr s" 1162 and iswaiting: "isWaitingNtfn (ntfnObj ntfn)" 1163 and mpeq: "(cslift t' |` (- (tcb_ptr_to_ctcb_ptr ` set (ntfnQueue (ntfnObj ntfn))))) 1164 = (cslift t |` (- (tcb_ptr_to_ctcb_ptr ` set (ntfnQueue (ntfnObj ntfn)))))" 1165 and koat': "ko_at' a epptr s" 1166 shows "cendpoint_relation (cslift t) a b = cendpoint_relation (cslift t') a b" 1167proof - 1168 have rl: "\<And>p. \<lbrakk> p \<in> tcb_ptr_to_ctcb_ptr ` set (epQueue a); isSendEP a \<or> isRecvEP a \<rbrakk> 1169 \<Longrightarrow> cslift t p = cslift t' p" using srs koat' koat iswaiting mpeq 1170 apply - 1171 apply (drule (4) ntfn_ep_disjoint) 1172 apply (erule restrict_map_eqI [symmetric]) 1173 apply (erule imageE) 1174 apply (clarsimp simp: disjoint_iff_not_equal inj_eq) 1175 done 1176 1177 show ?thesis 1178 unfolding cendpoint_relation_def using rl 1179 apply (simp add: Let_def) 1180 apply (cases a) 1181 apply (simp add: isRecvEP_def cong: tcb_queue_relation'_cong) 1182 apply simp 1183 apply (simp add: isSendEP_def isRecvEP_def cong: tcb_queue_relation'_cong) 1184 done 1185qed 1186 1187lemma cvariable_relation_upd_const: 1188 "m x \<noteq> None 1189 \<Longrightarrow> cvariable_array_map_relation (m (x \<mapsto> y)) (\<lambda>x. n) 1190 = cvariable_array_map_relation m (\<lambda>x. n)" 1191 by (auto simp: fun_eq_iff cvariable_array_map_relation_def) 1192 1193(* FIXME: move *) 1194lemma invs'_pspace_domain_valid: 1195 "invs' s \<Longrightarrow> pspace_domain_valid s" 1196 by (simp add: invs'_def valid_state'_def) 1197 1198lemma ptr_span_ctcb_subset: 1199 "is_aligned p tcbBlockSizeBits \<Longrightarrow> ptr_span (tcb_ptr_to_ctcb_ptr p) \<subseteq> {p .. p + 2^tcbBlockSizeBits-1}" 1200 apply (simp add: tcb_ptr_to_ctcb_ptr_def ctcb_offset_def) 1201 apply (frule aligned_add_aligned[where m=ctcb_size_bits, OF _ is_aligned_triv], 1202 simp add: objBits_defs ctcb_size_bits_def) 1203 apply (subst upto_intvl_eq'; clarsimp) 1204 apply (erule is_aligned_no_wrap', simp add: ctcb_size_bits_def) 1205 apply (rule conjI) 1206 apply (erule is_aligned_no_wrap', simp add: objBits_defs ctcb_size_bits_def) 1207 apply (cut_tac word_add_le_mono1[where k=p and j="2^tcbBlockSizeBits-1"]) 1208 apply (simp add: field_simps) 1209 apply (simp add: objBits_defs ctcb_size_bits_def) 1210 apply (subst field_simps, subst unat_plus_simple[where x=p, THEN iffD1, symmetric]) 1211 apply (erule is_aligned_no_overflow') 1212 apply (rule unat_lt2p) 1213 done 1214 1215(* FIXME: move *) 1216lemma tcb_at'_non_kernel_data_ref: 1217 "pspace_domain_valid s \<Longrightarrow> tcb_at' p s \<Longrightarrow> ptr_span (tcb_ptr_to_ctcb_ptr p) \<inter> kernel_data_refs = {}" 1218 apply (rule disjoint_subset[OF ptr_span_ctcb_subset]) 1219 apply (erule tcb_aligned') 1220 apply (drule map_to_tcbs_from_tcb_at) 1221 apply (clarsimp simp: pspace_domain_valid_def map_comp_def split: option.splits) 1222 apply (drule spec, drule spec, drule (1) mp) 1223 apply (simp add: projectKOs objBits_simps) 1224 done 1225 1226lemmas tcb_at'_non_kernel_data_ref' 1227 = tcb_at'_non_kernel_data_ref[OF invs'_pspace_domain_valid] 1228 1229(* FIXME: move. Wants to go in SR_lemmas_C, but dependencies make this hard. *) 1230lemma fpu_null_state_heap_update_span_disjoint: 1231 assumes "ptr_span p \<inter> kernel_data_refs = {}" 1232 shows "fpu_null_state_relation (hrs_mem_update (heap_update p v) h) = fpu_null_state_relation h" 1233 by (cases "ptr_span (fpu_state_Ptr (symbol_table ''x86KSnullFpuState'')) \<subseteq> kernel_data_refs"; 1234 clarsimp simp: fpu_null_state_relation_def lift_t_Some_iff hrs_mem_update 1235 h_val_update_regions_disjoint 1236 dest!: disjoint_subset2[OF _ assms]) 1237 1238(* FIXME: move near tag_disj_via_td_name *) 1239lemma tag_not_less_via_td_name: 1240 assumes ta: "typ_name (typ_info_t TYPE('a)) \<noteq> pad_typ_name" 1241 assumes tina: "typ_name (typ_info_t TYPE('a)) \<notin> td_names (typ_info_t TYPE('b))" 1242 shows "\<not> typ_uinfo_t TYPE('a::c_type) < typ_uinfo_t TYPE('b::c_type)" 1243 using assms 1244 by (auto simp: sub_typ_proper_def typ_tag_lt_def typ_simps dest: td_set_td_names) 1245 1246(* FIXME: move *) 1247lemma td_set_map_td_commute[rule_format]: 1248 "\<forall>i. td_set (map_td f t) i = apfst (map_td f) ` td_set t i" 1249 "\<forall>i. td_set_struct (map_td_struct f st) i = apfst (map_td f) ` td_set_struct st i" 1250 "\<forall>i. td_set_list (map_td_list f ts) i = apfst (map_td f) ` td_set_list ts i" 1251 "\<forall>i. td_set_pair (map_td_pair f tp) i = apfst (map_td f) ` td_set_pair tp i" 1252 apply (induct t and st and ts and tp) 1253 apply simp_all 1254 apply (case_tac dt_pair; clarsimp simp: image_Un) 1255 done 1256 1257(* FIXME: move *) 1258lemma td_set_export_uinfo_eq: 1259 "td_set (export_uinfo t) i = apfst export_uinfo ` td_set t i" 1260 unfolding export_uinfo_def by (rule td_set_map_td_commute) 1261 1262(* FIXME: move *) 1263lemma td_set_adjust_ti_eq: 1264 "td_set (adjust_ti t a b) i = apfst (\<lambda>t. adjust_ti t a b) ` td_set t i" 1265 unfolding adjust_ti_def by (rule td_set_map_td_commute) 1266 1267(* FIXME: move *) 1268lemma td_set_list_app: 1269 "td_set_list (ts @ ts') i = td_set_list ts i \<union> td_set_list ts' (i + size_td_list ts)" 1270 apply (induct ts arbitrary: i, simp) 1271 apply (rename_tac p ps i, case_tac p, simp add: Un_assoc field_simps) 1272 done 1273 1274(* FIXME: move *) 1275lemma apfst_comp: 1276 "apfst f \<circ> apfst g = apfst (f \<circ> g)" 1277 by auto 1278 1279lemma td_set_offset_wf[rule_format]: 1280 fixes td :: "'a typ_desc" 1281 and st :: "'a typ_struct" 1282 and ts :: "('a typ_desc, char list) dt_pair list" 1283 and tp :: "('a typ_desc, char list) dt_pair" 1284 shows "\<forall>s n m. (s, n) \<in> td_set td m \<longrightarrow> m \<le> n" 1285 "\<forall>s n m. (s, n) \<in> td_set_struct st m \<longrightarrow> m \<le> n" 1286 "\<forall>s n m. (s, n) \<in> td_set_list ts m \<longrightarrow> m \<le> n" 1287 "\<forall>s n m. (s, n) \<in> td_set_pair tp m \<longrightarrow> m \<le> n" 1288 apply (induct td and st and ts and tp) 1289 apply simp_all 1290 apply (case_tac dt_pair; fastforce) 1291 done 1292 1293lemma field_lookup_offset_wf[rule_format]: 1294 fixes td :: "'a typ_desc" 1295 and st :: "'a typ_struct" 1296 and ts :: "('a typ_desc, char list) dt_pair list" 1297 and tp :: "('a typ_desc, char list) dt_pair" 1298 shows "\<forall>s n m f. field_lookup td f m = Some (s, n) \<longrightarrow> m \<le> n" 1299 "\<forall>s n m f. field_lookup_struct st f m = Some (s, n) \<longrightarrow> m \<le> n" 1300 "\<forall>s n m f. field_lookup_list ts f m = Some (s, n) \<longrightarrow> m \<le> n" 1301 "\<forall>s n m f. field_lookup_pair tp f m = Some (s, n) \<longrightarrow> m \<le> n" 1302 apply (induct td and st and ts and tp) 1303 apply simp_all 1304 apply (fastforce split: option.splits)+ 1305 done 1306 1307lemma td_set_field_lookup_wf[rule_format]: 1308 fixes td :: "'a typ_desc" 1309 and st :: "'a typ_struct" 1310 and ts :: "('a typ_desc, char list) dt_pair list" 1311 and tp :: "('a typ_desc, char list) dt_pair" 1312 shows "\<forall>k m. wf_desc td \<longrightarrow> k \<in> td_set td m \<longrightarrow> (\<exists>f. field_lookup td f m = Some k)" 1313 "\<forall>k m. wf_desc_struct st \<longrightarrow> k \<in> td_set_struct st m \<longrightarrow> (\<exists>f. field_lookup_struct st f m = Some k)" 1314 "\<forall>k m. wf_desc_list ts \<longrightarrow> k \<in> td_set_list ts m \<longrightarrow> (\<exists>f. field_lookup_list ts f m = Some k)" 1315 "\<forall>k m. wf_desc_pair tp \<longrightarrow> k \<in> td_set_pair tp m \<longrightarrow> (\<exists>f. field_lookup_pair tp f m = Some k)" 1316 using td_set_field_lookup'[of td st ts tp] 1317 apply - 1318 apply (clarsimp, frule td_set_offset_wf, drule spec, drule spec, drule spec, drule mp, 1319 erule rsubst[where P="\<lambda>n. (s,n) \<in> td_set" for s td_set], subst add_diff_inverse_nat, 1320 simp add: not_less, simp, simp)+ 1321 done 1322 1323lemma td_set_image_field_lookup: 1324 "wf_desc td \<Longrightarrow> k \<in> f ` td_set td m \<Longrightarrow> (\<exists>fn. option_map f (field_lookup td fn m) = Some k)" 1325 "wf_desc_struct st \<Longrightarrow> k \<in> f ` td_set_struct st m \<Longrightarrow> (\<exists>fn. option_map f (field_lookup_struct st fn m) = Some k)" 1326 "wf_desc_list ts \<Longrightarrow> k \<in> f ` td_set_list ts m \<Longrightarrow> (\<exists>fn. option_map f (field_lookup_list ts fn m) = Some k)" 1327 "wf_desc_pair tp \<Longrightarrow> k \<in> f ` td_set_pair tp m \<Longrightarrow> (\<exists>fn. option_map f (field_lookup_pair tp fn m) = Some k)" 1328 by (fastforce simp: image_def dest: td_set_field_lookup_wf)+ 1329 1330lemma field_lookup_td_set[rule_format]: 1331 fixes td :: "'a typ_desc" 1332 and st :: "'a typ_struct" 1333 and ts :: "('a typ_desc, char list) dt_pair list" 1334 and tp :: "('a typ_desc, char list) dt_pair" 1335 shows "\<forall>k m f. field_lookup td f m = Some k \<longrightarrow> k \<in> td_set td m" 1336 "\<forall>k m f. field_lookup_struct st f m = Some k \<longrightarrow> k \<in> td_set_struct st m" 1337 "\<forall>k m f. field_lookup_list ts f m = Some k \<longrightarrow> k \<in> td_set_list ts m" 1338 "\<forall>k m f. field_lookup_pair tp f m = Some k \<longrightarrow> k \<in> td_set_pair tp m" 1339 using td_set_field_lookup_rev'[of td st ts tp] 1340 apply - 1341 apply (clarsimp, frule field_lookup_offset_wf, drule spec, drule spec, drule spec, drule mp, 1342 rule exI, erule rsubst[where P="\<lambda>n. f = Some (s,n)" for f s], subst add_diff_inverse_nat, 1343 simp add: not_less, simp, simp)+ 1344 done 1345 1346lemma field_lookup_list_Some: 1347 assumes "wf_desc_list ts" 1348 assumes "field_lookup_list ts (fn # fns') m = Some (s, n)" 1349 shows "\<exists>td' m'. field_lookup_list ts [fn] m = Some (td', m') \<and> field_lookup td' fns' m' = Some (s, n)" 1350 using assms 1351 apply (induct ts arbitrary: m, simp) 1352 apply (rename_tac tp ts m, case_tac tp) 1353 apply (clarsimp split: if_splits option.splits simp: field_lookup_list_None) 1354 done 1355 1356lemma field_lookup_Some_cases: 1357 assumes "wf_desc td" 1358 assumes "field_lookup td fns m = Some (s,n)" 1359 shows "case fns of 1360 [] \<Rightarrow> s = td \<and> m = n 1361 | fn # fns' \<Rightarrow> \<exists>td' m'. field_lookup td [fn] m = Some (td',m') 1362 \<and> field_lookup td' fns' m' = Some (s,n)" 1363 using assms 1364 apply (cases fns; simp) 1365 apply (cases td, rename_tac fn fns' st tn, clarsimp) 1366 apply (case_tac st; clarsimp simp: field_lookup_list_Some) 1367 done 1368 1369lemma field_lookup_SomeE: 1370 assumes lookup: "field_lookup td fns m = Some (s,n)" 1371 assumes wf: "wf_desc td" 1372 assumes nil: "\<lbrakk> fns = []; s = td; m = n \<rbrakk> \<Longrightarrow> P" 1373 assumes some: "\<And>fn fns' td' m'. \<lbrakk> fns = fn # fns'; field_lookup td [fn] m = Some (td',m'); 1374 field_lookup td' fns' m' = Some (s,n) \<rbrakk> \<Longrightarrow> P" 1375 shows P 1376 using field_lookup_Some_cases[OF wf lookup] 1377 by (cases fns) (auto simp add: nil some) 1378 1379lemmas typ_combine_simps = 1380 ti_typ_pad_combine_def[where tag="TypDesc st tn" for st tn] 1381 ti_typ_combine_def[where tag="TypDesc st tn" for st tn] 1382 ti_pad_combine_def[where tag="TypDesc st tn" for st tn] 1383 align_td_array' size_td_array 1384 CompoundCTypes.field_names_list_def 1385 empty_typ_info_def 1386 final_pad_def padup_def 1387 align_of_def 1388 1389bundle typ_combine_bundle = 1390 typ_combine_simps[simp] 1391 if_weak_cong[cong] 1392 1393schematic_goal tcb_C_typ_info_unfold: 1394 "typ_info_t (?t :: tcb_C itself) = TypDesc ?st ?tn" 1395 including typ_combine_bundle by (simp add: tcb_C_typ_info tcb_C_tag_def) 1396 1397schematic_goal arch_tcb_C_typ_info_unfold: 1398 "typ_info_t (?t :: arch_tcb_C itself) = TypDesc ?st ?tn" 1399 including typ_combine_bundle by (simp add: arch_tcb_C_typ_info arch_tcb_C_tag_def) 1400 1401schematic_goal user_context_C_typ_info_unfold: 1402 "typ_info_t (?t :: user_context_C itself) = TypDesc ?st ?tn" 1403 including typ_combine_bundle by (simp add: user_context_C_typ_info user_context_C_tag_def) 1404 1405schematic_goal user_fpu_state_C_typ_info_unfold: 1406 "typ_info_t (?t :: user_fpu_state_C itself) = TypDesc ?st ?tn" 1407 including typ_combine_bundle by (simp add: user_fpu_state_C_typ_info user_fpu_state_C_tag_def) 1408 1409lemma user_fpu_state_C_in_tcb_C_offset: 1410 "(typ_uinfo_t TYPE(user_fpu_state_C), n) \<in> td_set (typ_uinfo_t TYPE(tcb_C)) 0 \<Longrightarrow> n = 0" 1411 \<comment> \<open>Examine the fields of tcb_C.\<close> 1412 apply (simp add: typ_uinfo_t_def tcb_C_typ_info_unfold td_set_export_uinfo_eq td_set_adjust_ti_eq 1413 image_comp image_Un apfst_comp o_def[where f=export_uinfo] 1414 del: export_uinfo_typdesc_simp) 1415 apply (elim disjE) 1416 apply (all \<open>drule td_set_image_field_lookup[rotated]; clarsimp\<close>) 1417 apply (all \<open>drule arg_cong[where f=typ_name]; simp add: adjust_ti_def\<close>) 1418 apply (all \<open>(solves \<open>drule field_lookup_td_set; drule td_set_td_names; simp\<close>)?\<close>) 1419 \<comment> \<open>Only the arch_tcb_C may contain user_fpu_state_C, so examine the fields of that.\<close> 1420 apply (drule field_lookup_td_set) 1421 apply (simp add: arch_tcb_C_typ_info_unfold td_set_adjust_ti_eq) 1422 apply (drule td_set_image_field_lookup[rotated]; clarsimp simp: adjust_ti_def) 1423 \<comment> \<open>Similarly for user_context_C.\<close> 1424 apply (drule field_lookup_td_set) 1425 apply (simp add: user_context_C_typ_info_unfold td_set_adjust_ti_eq) 1426 apply (elim disjE) 1427 apply (all \<open>drule td_set_image_field_lookup[rotated]; clarsimp simp: adjust_ti_def\<close>) 1428 apply (all \<open>(solves \<open>drule field_lookup_td_set; drule td_set_td_names; simp\<close>)?\<close>) 1429 \<comment> \<open>Finally, we have user_fpu_state_C.\<close> 1430 apply (rename_tac fns s) 1431 apply (case_tac fns; clarsimp) 1432 \<comment> \<open>But we must also show that there is no user_fpu_state_C buried within user_fpu_state_C.\<close> 1433 apply (drule field_lookup_td_set) 1434 apply (simp add: user_fpu_state_C_typ_info_unfold td_set_adjust_ti_eq) 1435 apply (elim disjE; clarsimp simp: adjust_ti_def) 1436 apply (drule td_set_td_names; simp) 1437 done 1438 1439context 1440 fixes t :: "tcb_C ptr" 1441 fixes tcb :: tcb_C 1442 fixes h u :: heap_raw_state 1443 fixes t_fpu :: "user_fpu_state_C ptr" 1444 defines "t_fpu \<equiv> fpu_state_Ptr &(user_context_Ptr &(atcb_Ptr &(t\<rightarrow>[''tcbArch_C''])\<rightarrow>[''tcbContext_C''])\<rightarrow>[''fpuState_C''])" 1445 defines "u \<equiv> hrs_mem_update (heap_update t tcb) h" 1446 assumes f: "clift u t_fpu = clift h t_fpu" 1447 assumes v: "hrs_htd h \<Turnstile>\<^sub>t t" 1448begin 1449 1450lemma fpu_state_preservation: 1451 "(clift u :: user_fpu_state_C typ_heap) = clift h" 1452 apply (rule ext) 1453 apply (rename_tac null_fpu) 1454 apply (case_tac "ptr_val null_fpu = ptr_val t_fpu") 1455 subgoal for null_fpu 1456 using f by (cases null_fpu; clarsimp simp: u_def t_fpu_def lift_t_if split: if_splits) 1457 apply (subgoal_tac "hrs_htd h \<Turnstile>\<^sub>t t_fpu") 1458 prefer 2 subgoal 1459 unfolding t_fpu_def 1460 by (rule h_t_valid_field[OF h_t_valid_field[OF h_t_valid_field[OF v]]], simp+) 1461 using f v unfolding u_def t_fpu_def 1462 apply (cases h; case_tac "hrs_htd h \<Turnstile>\<^sub>t null_fpu"; 1463 clarsimp simp: lift_t_if hrs_mem_update_def hrs_htd_def) 1464 apply (thin_tac "_ \<Turnstile>\<^sub>t fpu_state_Ptr _", thin_tac "h_val _ _ = h_val _ _", thin_tac "h = _") 1465 apply (rule h_val_heap_same; simp add: sub_typ_proper_def tag_not_less_via_td_name field_lvalue_def) 1466 apply (thin_tac "_ \<Turnstile>\<^sub>t _", thin_tac "_ \<Turnstile>\<^sub>t _", simp) 1467 apply (erule contrapos_np; simp add: field_of_t_def field_of_def) 1468 apply (drule user_fpu_state_C_in_tcb_C_offset) 1469 apply (simp add: unat_eq_0) 1470 done 1471 1472lemma fpu_null_state_preservation: 1473 shows "fpu_null_state_relation u = fpu_null_state_relation h" 1474 by (simp add: fpu_null_state_relation_def fpu_state_preservation) 1475 1476end 1477 1478lemma rf_sr_tcb_update_no_queue: 1479 "\<lbrakk> (s, s') \<in> rf_sr; 1480 ko_at' tcb thread s; 1481 t_hrs_' (globals t) = hrs_mem_update (heap_update (tcb_ptr_to_ctcb_ptr thread) ctcb) 1482 (t_hrs_' (globals s')); 1483 tcbEPNext_C ctcb = tcbEPNext_C (the (cslift s' (tcb_ptr_to_ctcb_ptr thread))); 1484 tcbEPPrev_C ctcb = tcbEPPrev_C (the (cslift s' (tcb_ptr_to_ctcb_ptr thread))); 1485 tcbSchedNext_C ctcb = tcbSchedNext_C (the (cslift s' (tcb_ptr_to_ctcb_ptr thread))); 1486 tcbSchedPrev_C ctcb = tcbSchedPrev_C (the (cslift s' (tcb_ptr_to_ctcb_ptr thread))); 1487 fpuState_C (tcbContext_C (tcbArch_C ctcb)) 1488 = fpuState_C (tcbContext_C (tcbArch_C (the (cslift s' (tcb_ptr_to_ctcb_ptr thread))))); 1489 (\<forall>x\<in>ran tcb_cte_cases. (\<lambda>(getF, setF). getF tcb' = getF tcb) x); 1490 ctcb_relation tcb' ctcb 1491 \<rbrakk> 1492 \<Longrightarrow> (s\<lparr>ksPSpace := ksPSpace s(thread \<mapsto> KOTCB tcb')\<rparr>, 1493 x\<lparr>globals := globals s'\<lparr>t_hrs_' := t_hrs_' (globals t)\<rparr>\<rparr>) \<in> rf_sr" 1494 unfolding rf_sr_def state_relation_def cstate_relation_def cpspace_relation_def 1495 apply (clarsimp simp: Let_def update_tcb_map_tos map_to_ctes_upd_tcb_no_ctes 1496 heap_to_user_data_def) 1497 apply (frule (1) cmap_relation_ko_atD) 1498 apply (erule obj_atE') 1499 apply (clarsimp simp: projectKOs) 1500 apply (clarsimp simp: map_comp_update projectKO_opt_tcb cvariable_relation_upd_const 1501 typ_heap_simps') 1502 apply (intro conjI) 1503 subgoal by (clarsimp simp: cmap_relation_def map_comp_update projectKO_opts_defs inj_eq) 1504 apply (erule iffD1 [OF cmap_relation_cong, OF refl refl, rotated -1]) 1505 apply simp 1506 apply (rule cendpoint_relation_upd_tcb_no_queues, assumption+) 1507 subgoal by (clarsimp intro!: ext) 1508 subgoal by (clarsimp intro!: ext) 1509 apply (erule iffD1 [OF cmap_relation_cong, OF refl refl, rotated -1]) 1510 apply simp 1511 apply (rule cnotification_relation_upd_tcb_no_queues, assumption+) 1512 subgoal by (clarsimp intro!: ext) 1513 subgoal by (clarsimp intro!: ext) 1514 apply (erule cready_queues_relation_not_queue_ptrs) 1515 subgoal by (clarsimp intro!: ext) 1516 subgoal by (clarsimp intro!: ext) 1517 subgoal by (clarsimp simp: carch_state_relation_def fpu_null_state_preservation typ_heap_simps') 1518 by (simp add: cmachine_state_relation_def) 1519 1520lemma rf_sr_tcb_update_no_queue_helper: 1521 "(s, s'\<lparr> globals := globals s' \<lparr> t_hrs_' := t_hrs_' (globals (undefined 1522 \<lparr> globals := (undefined \<lparr> t_hrs_' := f (globals s') (t_hrs_' (globals s')) \<rparr>)\<rparr>))\<rparr>\<rparr>) \<in> rf_sr 1523 \<Longrightarrow> (s, globals_update (\<lambda>v. t_hrs_'_update (f v) v) s') \<in> rf_sr" 1524 by (simp cong: StateSpace.state.fold_congs globals.fold_congs) 1525 1526lemmas rf_sr_tcb_update_no_queue2 1527 = rf_sr_tcb_update_no_queue_helper [OF rf_sr_tcb_update_no_queue, simplified] 1528 1529lemma tcb_queue_relation_not_in_q: 1530 "ctcb_ptr_to_tcb_ptr x \<notin> set xs \<Longrightarrow> 1531 tcb_queue_relation' nxtFn prvFn (hp(x := v)) xs start end 1532 = tcb_queue_relation' nxtFn prvFn hp xs start end" 1533 by (rule tcb_queue_relation'_cong, auto) 1534 1535lemma rf_sr_tcb_update_not_in_queue: 1536 "\<lbrakk> (s, s') \<in> rf_sr; ko_at' tcb thread s; 1537 t_hrs_' (globals t) = hrs_mem_update (heap_update 1538 (tcb_ptr_to_ctcb_ptr thread) ctcb) (t_hrs_' (globals s')); 1539 \<not> live' (KOTCB tcb); invs' s; 1540 (\<forall>x\<in>ran tcb_cte_cases. (\<lambda>(getF, setF). getF tcb' = getF tcb) x); 1541 ctcb_relation tcb' ctcb \<rbrakk> 1542 \<Longrightarrow> (s\<lparr>ksPSpace := ksPSpace s(thread \<mapsto> KOTCB tcb')\<rparr>, 1543 x\<lparr>globals := globals s'\<lparr>t_hrs_' := t_hrs_' (globals t)\<rparr>\<rparr>) \<in> rf_sr" 1544 unfolding rf_sr_def state_relation_def cstate_relation_def cpspace_relation_def 1545 apply (clarsimp simp: Let_def update_tcb_map_tos map_to_ctes_upd_tcb_no_ctes 1546 heap_to_user_data_def live'_def) 1547 apply (frule (1) cmap_relation_ko_atD) 1548 apply (erule obj_atE') 1549 apply (clarsimp simp: projectKOs) 1550 apply (clarsimp simp: map_comp_update projectKO_opt_tcb cvariable_relation_upd_const 1551 typ_heap_simps') 1552 apply (subgoal_tac "\<forall>rf. \<not> ko_wp_at' (\<lambda>ko. rf \<in> refs_of' ko) thread s") 1553 prefer 2 1554 apply clarsimp 1555 apply (auto simp: obj_at'_def ko_wp_at'_def)[1] 1556 apply (intro conjI) 1557 subgoal by (clarsimp simp: cmap_relation_def map_comp_update projectKO_opts_defs inj_eq) 1558 apply (erule iffD1 [OF cmap_relation_cong, OF refl refl, rotated -1]) 1559 apply clarsimp 1560 apply (subgoal_tac "thread \<notin> (fst ` ep_q_refs_of' a)") 1561 apply (clarsimp simp: cendpoint_relation_def Let_def split: Structures_H.endpoint.split) 1562 subgoal by (intro conjI impI allI, simp_all add: image_def tcb_queue_relation_not_in_q)[1] 1563 apply (drule(1) map_to_ko_atI') 1564 apply (drule sym_refs_ko_atD', clarsimp+) 1565 subgoal by blast 1566 apply (erule iffD1 [OF cmap_relation_cong, OF refl refl, rotated -1]) 1567 apply clarsimp 1568 apply (subgoal_tac "thread \<notin> (fst ` ntfn_q_refs_of' (ntfnObj a))") 1569 apply (clarsimp simp: cnotification_relation_def Let_def 1570 split: ntfn.splits) 1571 subgoal by (simp add: image_def tcb_queue_relation_not_in_q)[1] 1572 apply (drule(1) map_to_ko_atI') 1573 apply (drule sym_refs_ko_atD', clarsimp+) 1574 subgoal by blast 1575 apply (simp add: cready_queues_relation_def, erule allEI) 1576 apply (clarsimp simp: Let_def) 1577 apply (subst tcb_queue_relation_not_in_q) 1578 apply clarsimp 1579 apply (drule valid_queues_obj_at'D, clarsimp) 1580 apply (clarsimp simp: obj_at'_def projectKOs inQ_def) 1581 subgoal by simp 1582 apply (simp add: carch_state_relation_def) 1583 subgoal by (clarsimp simp: fpu_null_state_heap_update_span_disjoint[OF tcb_at'_non_kernel_data_ref'] 1584 global_ioport_bitmap_heap_update_tag_disj_simps obj_at'_def projectKOs) 1585 by (simp add: cmachine_state_relation_def) 1586 1587lemmas rf_sr_tcb_update_not_in_queue2 1588 = rf_sr_tcb_update_no_queue_helper [OF rf_sr_tcb_update_not_in_queue, simplified] 1589 1590end 1591end 1592