theory Detype_R

lemma ctes_of_ko_at:
  "ctes_of s p = Some a \<Longrightarrow>
  (\<exists>ptr ko. (ksPSpace s ptr = Some ko \<and> p \<in> obj_range' ptr ko))" apply (clarsimp simp: map_to_ctes_def Let_def split: if_split_asm) apply (intro exI conjI, assumption) apply (simp add: obj_range'_def objBits_simps' add.commute) apply (simp add: is_aligned_no_wrap') apply (intro exI conjI, assumption) apply (clarsimp simp: objBits_simps' obj_range'_def word_and_le2) apply (thin_tac "P" for P)+ apply (simp add: mask_def) apply word_bitwise done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ctes_of s p = Some a \<Longrightarrow> \<exists>ptr ko. ksPSpace s ptr = Some ko \<and> p \<in> obj_range' ptr ko proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned p (objBitsKO (KOCTE undefined)); {p + 1..p + 2 ^ objBitsKO (KOCTE undefined) - 1} \<inter> dom (ksPSpace s) = {}; ksPSpace s p = Some (KOCTE a)\<rbrakk> \<Longrightarrow> \<exists>ptr ko. ksPSpace s ptr = Some ko \<and> p \<in> obj_range' ptr ko
 2. \<And>tcb aa b. \<lbrakk>is_aligned p (objBitsKO (KOCTE undefined)) \<longrightarrow> (\<forall>cte. ksPSpace s p \<noteq> Some (KOCTE cte)) \<or> {p + 1..p + 2 ^ objBitsKO (KOCTE undefined) - 1} \<inter> dom (ksPSpace s) \<noteq> {}; {(p && ~~ mask (objBitsKO (KOTCB undefined))) + 1..(p && ~~ mask (objBitsKO (KOTCB undefined))) + 2 ^ objBitsKO (KOTCB undefined) - 1} \<inter> dom (ksPSpace s) = {}; ksPSpace s (p && ~~ mask (objBitsKO (KOTCB undefined))) = Some (KOTCB tcb); a = aa tcb; tcb_cte_cases (p && mask (objBitsKO (KOTCB undefined))) = Some (aa, b)\<rbrakk> \<Longrightarrow> \<exists>ptr ko. ksPSpace s ptr = Some ko \<and> p \<in> obj_range' ptr ko proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned p (objBitsKO (KOCTE undefined)); {p + 1..p + 2 ^ objBitsKO (KOCTE undefined) - 1} \<inter> dom (ksPSpace s) = {}; ksPSpace s p = Some (KOCTE a)\<rbrakk> \<Longrightarrow> p \<in> obj_range' p (KOCTE a)
 2. \<And>tcb aa b. \<lbrakk>is_aligned p (objBitsKO (KOCTE undefined)) \<longrightarrow> (\<forall>cte. ksPSpace s p \<noteq> Some (KOCTE cte)) \<or> {p + 1..p + 2 ^ objBitsKO (KOCTE undefined) - 1} \<inter> dom (ksPSpace s) \<noteq> {}; {(p && ~~ mask (objBitsKO (KOTCB undefined))) + 1..(p && ~~ mask (objBitsKO (KOTCB undefined))) + 2 ^ objBitsKO (KOTCB undefined) - 1} \<inter> dom (ksPSpace s) = {}; ksPSpace s (p && ~~ mask (objBitsKO (KOTCB undefined))) = Some (KOTCB tcb); a = aa tcb; tcb_cte_cases (p && mask (objBitsKO (KOTCB undefined))) = Some (aa, b)\<rbrakk> \<Longrightarrow> \<exists>ptr ko. ksPSpace s ptr = Some ko \<and> p \<in> obj_range' ptr ko proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned p 4; {1 + p..p + 0xF} \<inter> dom (ksPSpace s) = {}; ksPSpace s p = Some (KOCTE a)\<rbrakk> \<Longrightarrow> p \<le> p + 0xF
 2. \<And>tcb aa b. \<lbrakk>is_aligned p (objBitsKO (KOCTE undefined)) \<longrightarrow> (\<forall>cte. ksPSpace s p \<noteq> Some (KOCTE cte)) \<or> {p + 1..p + 2 ^ objBitsKO (KOCTE undefined) - 1} \<inter> dom (ksPSpace s) \<noteq> {}; {(p && ~~ mask (objBitsKO (KOTCB undefined))) + 1..(p && ~~ mask (objBitsKO (KOTCB undefined))) + 2 ^ objBitsKO (KOTCB undefined) - 1} \<inter> dom (ksPSpace s) = {}; ksPSpace s (p && ~~ mask (objBitsKO (KOTCB undefined))) = Some (KOTCB tcb); a = aa tcb; tcb_cte_cases (p && mask (objBitsKO (KOTCB undefined))) = Some (aa, b)\<rbrakk> \<Longrightarrow> \<exists>ptr ko. ksPSpace s ptr = Some ko \<and> p \<in> obj_range' ptr ko proof (prove)
goal (1 subgoal):
 1. \<And>tcb aa b. \<lbrakk>is_aligned p (objBitsKO (KOCTE undefined)) \<longrightarrow> (\<forall>cte. ksPSpace s p \<noteq> Some (KOCTE cte)) \<or> {p + 1..p + 2 ^ objBitsKO (KOCTE undefined) - 1} \<inter> dom (ksPSpace s) \<noteq> {}; {(p && ~~ mask (objBitsKO (KOTCB undefined))) + 1..(p && ~~ mask (objBitsKO (KOTCB undefined))) + 2 ^ objBitsKO (KOTCB undefined) - 1} \<inter> dom (ksPSpace s) = {}; ksPSpace s (p && ~~ mask (objBitsKO (KOTCB undefined))) = Some (KOTCB tcb); a = aa tcb; tcb_cte_cases (p && mask (objBitsKO (KOTCB undefined))) = Some (aa, b)\<rbrakk> \<Longrightarrow> \<exists>ptr ko. ksPSpace s ptr = Some ko \<and> p \<in> obj_range' ptr ko proof (prove)
goal (1 subgoal):
 1. \<And>tcb aa b. \<lbrakk>is_aligned p (objBitsKO (KOCTE undefined)) \<longrightarrow> (\<forall>cte. ksPSpace s p \<noteq> Some (KOCTE cte)) \<or> {p + 1..p + 2 ^ objBitsKO (KOCTE undefined) - 1} \<inter> dom (ksPSpace s) \<noteq> {}; {(p && ~~ mask (objBitsKO (KOTCB undefined))) + 1..(p && ~~ mask (objBitsKO (KOTCB undefined))) + 2 ^ objBitsKO (KOTCB undefined) - 1} \<inter> dom (ksPSpace s) = {}; ksPSpace s (p && ~~ mask (objBitsKO (KOTCB undefined))) = Some (KOTCB tcb); a = aa tcb; tcb_cte_cases (p && mask (objBitsKO (KOTCB undefined))) = Some (aa, b)\<rbrakk> \<Longrightarrow> p \<in> obj_range' (p && ~~ mask (objBitsKO (KOTCB undefined))) (KOTCB tcb) proof (prove)
goal (1 subgoal):
 1. \<And>tcb aa b. \<lbrakk>is_aligned p 4 \<longrightarrow> (\<forall>cte. ksPSpace s p \<noteq> Some (KOCTE cte)) \<or> {p + 1..0xF + p} \<inter> dom (ksPSpace s) \<noteq> {}; {(p && ~~ mask 9) + 1..0x1FF + (p && ~~ mask 9)} \<inter> dom (ksPSpace s) = {}; ksPSpace s (p && ~~ mask 9) = Some (KOTCB tcb); a = aa tcb; tcb_cte_cases (p && mask 9) = Some (aa, b)\<rbrakk> \<Longrightarrow> p \<le> 0x1FF + (p && ~~ mask 9) proof (prove)
goal (1 subgoal):
 1. \<And>tcb a b. p \<le> 0x1FF + (p && ~~ mask 9) proof (prove)
goal (1 subgoal):
 1. p \<le> 0x1FF + (p && 0xFFFFFE00) proof (prove)
goal:
No subgoals!