theory KHeap_R

lemma ctes_of_setObject_cte:
  "\<lbrace>\<lambda>s. P ((ctes_of s) (p \<mapsto> cte))\<rbrace> setObject p (cte :: cte) \<lbrace>\<lambda>rv s. P (ctes_of s)\<rbrace>" apply (clarsimp simp: setObject_def split_def valid_def in_monad) apply (drule(1) updateObject_cte_is_tcb_or_cte[OF _ refl, rotated]) apply (elim exE conjE disjE rsubst[where P=P]) apply (clarsimp simp: lookupAround2_char1) apply (subst map_to_ctes_upd_tcb; assumption?) apply (clarsimp simp: mask_def objBits_defs field_simps ps_clear_def3) apply (clarsimp simp: tcb_cte_cases_change) apply (rule ext, clarsimp) apply (intro conjI impI) apply (clarsimp simp: tcb_cte_cases_def split: if_split_asm) apply (drule(1) cte_wp_at_tcbI'[where P="(=) cte"]) apply (simp add: ps_clear_def3 field_simps) apply assumption+ apply (simp add: cte_wp_at_ctes_of) apply (clarsimp simp: map_to_ctes_upd_cte ps_clear_def3 field_simps mask_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P ((ctes_of s)(p \<mapsto> cte))\<rbrace> setObject p cte \<lbrace>\<lambda>rv s. P (ctes_of s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s a ba s'' obj'. \<lbrakk>P ((ctes_of s)(p \<mapsto> cte)); fst (lookupAround2 p (ksPSpace s)) = Some (a, ba); (obj', s'') \<in> fst (updateObject cte ba p a (snd (lookupAround2 p (ksPSpace s))) s)\<rbrakk> \<Longrightarrow> P (map_to_ctes ((ksPSpace s)(a \<mapsto> obj'))) proof (prove)
goal (1 subgoal):
 1. \<And>s a ba s'' obj'. \<lbrakk>P ((ctes_of s)(p \<mapsto> cte)); fst (lookupAround2 p (ksPSpace s)) = Some (a, ba); (\<exists>tcb getF setF. ba = KOTCB tcb \<and> s'' = s \<and> tcb_cte_cases (p - a) = Some (getF, setF) \<and> obj' = KOTCB (setF (\<lambda>x. cte) tcb) \<and> is_aligned a tcbBlockSizeBits \<and> ps_clear a tcbBlockSizeBits s) \<or> (\<exists>cte'. ba = KOCTE cte' \<and> obj' = KOCTE cte \<and> s'' = s \<and> p = a \<and> is_aligned p cte_level_bits \<and> ps_clear p cte_level_bits s)\<rbrakk> \<Longrightarrow> P (map_to_ctes ((ksPSpace s)(a \<mapsto> obj'))) proof (prove)
goal (2 subgoals):
 1. \<And>s a ba s'' obj' tcb getF setF. \<lbrakk>fst (lookupAround2 p (ksPSpace s)) = Some (a, ba); ba = KOTCB tcb; s'' = s; tcb_cte_cases (p - a) = Some (getF, setF); obj' = KOTCB (setF (\<lambda>x. cte) tcb); is_aligned a tcbBlockSizeBits; ps_clear a tcbBlockSizeBits s\<rbrakk> \<Longrightarrow> (ctes_of s)(p \<mapsto> cte) = map_to_ctes ((ksPSpace s)(a \<mapsto> obj'))
 2. \<And>s a ba s'' obj' cte'. \<lbrakk>fst (lookupAround2 p (ksPSpace s)) = Some (a, ba); ba = KOCTE cte'; obj' = KOCTE cte; s'' = s; p = a; is_aligned p cte_level_bits; ps_clear p cte_level_bits s\<rbrakk> \<Longrightarrow> (ctes_of s)(p \<mapsto> cte) = map_to_ctes ((ksPSpace s)(a \<mapsto> obj')) proof (prove)
goal (2 subgoals):
 1. \<And>s a tcb getF setF. \<lbrakk>tcb_cte_cases (p - a) = Some (getF, setF); is_aligned a tcbBlockSizeBits; ps_clear a tcbBlockSizeBits s; a \<le> p; ksPSpace s a = Some (KOTCB tcb); \<forall>z. a < z \<and> z \<le> p \<longrightarrow> ksPSpace s z = None\<rbrakk> \<Longrightarrow> (ctes_of s)(p \<mapsto> cte) = map_to_ctes ((ksPSpace s)(a \<mapsto> KOTCB (setF (\<lambda>x. cte) tcb)))
 2. \<And>s a ba s'' obj' cte'. \<lbrakk>fst (lookupAround2 p (ksPSpace s)) = Some (a, ba); ba = KOCTE cte'; obj' = KOCTE cte; s'' = s; p = a; is_aligned p cte_level_bits; ps_clear p cte_level_bits s\<rbrakk> \<Longrightarrow> (ctes_of s)(p \<mapsto> cte) = map_to_ctes ((ksPSpace s)(a \<mapsto> obj')) proof (prove)
goal (3 subgoals):
 1. \<And>s a tcb getF setF. \<lbrakk>tcb_cte_cases (p - a) = Some (getF, setF); is_aligned a tcbBlockSizeBits; ps_clear a tcbBlockSizeBits s; a \<le> p; ksPSpace s a = Some (KOTCB tcb); \<forall>z. a < z \<and> z \<le> p \<longrightarrow> ksPSpace s z = None\<rbrakk> \<Longrightarrow> {a + 1..a + mask tcbBlockSizeBits} \<inter> dom (ksPSpace s) = {}
 2. \<And>s a tcb getF setF. \<lbrakk>tcb_cte_cases (p - a) = Some (getF, setF); is_aligned a tcbBlockSizeBits; ps_clear a tcbBlockSizeBits s; a \<le> p; ksPSpace s a = Some (KOTCB tcb); \<forall>z. a < z \<and> z \<le> p \<longrightarrow> ksPSpace s z = None\<rbrakk> \<Longrightarrow> (ctes_of s)(p \<mapsto> cte) = (\<lambda>x. if \<exists>getF setFa. tcb_cte_cases (x - a) = Some (getF, setFa) \<and> getF (setF (\<lambda>a. cte) tcb) \<noteq> getF tcb then case tcb_cte_cases (x - a) of Some (getF, setFa) \<Rightarrow> Some (getF (setF (\<lambda>a. cte) tcb)) else ctes_of s x)
 3. \<And>s a ba s'' obj' cte'. \<lbrakk>fst (lookupAround2 p (ksPSpace s)) = Some (a, ba); ba = KOCTE cte'; obj' = KOCTE cte; s'' = s; p = a; is_aligned p cte_level_bits; ps_clear p cte_level_bits s\<rbrakk> \<Longrightarrow> (ctes_of s)(p \<mapsto> cte) = map_to_ctes ((ksPSpace s)(a \<mapsto> obj')) proof (prove)
goal (2 subgoals):
 1. \<And>s a tcb getF setF. \<lbrakk>tcb_cte_cases (p - a) = Some (getF, setF); is_aligned a tcbBlockSizeBits; ps_clear a tcbBlockSizeBits s; a \<le> p; ksPSpace s a = Some (KOTCB tcb); \<forall>z. a < z \<and> z \<le> p \<longrightarrow> ksPSpace s z = None\<rbrakk> \<Longrightarrow> (ctes_of s)(p \<mapsto> cte) = (\<lambda>x. if \<exists>getF setFa. tcb_cte_cases (x - a) = Some (getF, setFa) \<and> getF (setF (\<lambda>a. cte) tcb) \<noteq> getF tcb then case tcb_cte_cases (x - a) of Some (getF, setFa) \<Rightarrow> Some (getF (setF (\<lambda>a. cte) tcb)) else ctes_of s x)
 2. \<And>s a ba s'' obj' cte'. \<lbrakk>fst (lookupAround2 p (ksPSpace s)) = Some (a, ba); ba = KOCTE cte'; obj' = KOCTE cte; s'' = s; p = a; is_aligned p cte_level_bits; ps_clear p cte_level_bits s\<rbrakk> \<Longrightarrow> (ctes_of s)(p \<mapsto> cte) = map_to_ctes ((ksPSpace s)(a \<mapsto> obj')) proof (prove)
goal (2 subgoals):
 1. \<And>s a tcb getF setF. \<lbrakk>tcb_cte_cases (p - a) = Some (getF, setF); is_aligned a tcbBlockSizeBits; ps_clear a tcbBlockSizeBits s; a \<le> p; ksPSpace s a = Some (KOTCB tcb); \<forall>z. a < z \<and> z \<le> p \<longrightarrow> ksPSpace s z = None\<rbrakk> \<Longrightarrow> (ctes_of s)(p \<mapsto> cte) = (\<lambda>x. if p = x \<and> cte \<noteq> getF tcb then case tcb_cte_cases (x - a) of Some (getF, setFa) \<Rightarrow> Some (getF (setF (\<lambda>a. cte) tcb)) else ctes_of s x)
 2. \<And>s a ba s'' obj' cte'. \<lbrakk>fst (lookupAround2 p (ksPSpace s)) = Some (a, ba); ba = KOCTE cte'; obj' = KOCTE cte; s'' = s; p = a; is_aligned p cte_level_bits; ps_clear p cte_level_bits s\<rbrakk> \<Longrightarrow> (ctes_of s)(p \<mapsto> cte) = map_to_ctes ((ksPSpace s)(a \<mapsto> obj')) proof (prove)
goal (2 subgoals):
 1. \<And>s a tcb getF setF. \<lbrakk>tcb_cte_cases (p - a) = Some (getF, setF); is_aligned a tcbBlockSizeBits; ps_clear a tcbBlockSizeBits s; a \<le> p; ksPSpace s a = Some (KOTCB tcb); \<forall>z. a < z \<and> z \<le> p \<longrightarrow> ksPSpace s z = None\<rbrakk> \<Longrightarrow> (cte \<noteq> getF tcb \<longrightarrow> cte = getF (setF (\<lambda>a. cte) tcb)) \<and> (cte = getF tcb \<longrightarrow> Some (getF tcb) = ctes_of s p)
 2. \<And>s a ba s'' obj' cte'. \<lbrakk>fst (lookupAround2 p (ksPSpace s)) = Some (a, ba); ba = KOCTE cte'; obj' = KOCTE cte; s'' = s; p = a; is_aligned p cte_level_bits; ps_clear p cte_level_bits s\<rbrakk> \<Longrightarrow> (ctes_of s)(p \<mapsto> cte) = map_to_ctes ((ksPSpace s)(a \<mapsto> obj')) proof (prove)
goal (3 subgoals):
 1. \<And>s a tcb getF setF. \<lbrakk>tcb_cte_cases (p - a) = Some (getF, setF); is_aligned a tcbBlockSizeBits; ps_clear a tcbBlockSizeBits s; a \<le> p; ksPSpace s a = Some (KOTCB tcb); \<forall>z. a < z \<and> z \<le> p \<longrightarrow> ksPSpace s z = None; cte \<noteq> getF tcb\<rbrakk> \<Longrightarrow> cte = getF (setF (\<lambda>a. cte) tcb)
 2. \<And>s a tcb getF setF. \<lbrakk>tcb_cte_cases (p - a) = Some (getF, setF); is_aligned a tcbBlockSizeBits; ps_clear a tcbBlockSizeBits s; a \<le> p; ksPSpace s a = Some (KOTCB tcb); \<forall>z. a < z \<and> z \<le> p \<longrightarrow> ksPSpace s z = None; cte = getF tcb\<rbrakk> \<Longrightarrow> Some (getF tcb) = ctes_of s p
 3. \<And>s a ba s'' obj' cte'. \<lbrakk>fst (lookupAround2 p (ksPSpace s)) = Some (a, ba); ba = KOCTE cte'; obj' = KOCTE cte; s'' = s; p = a; is_aligned p cte_level_bits; ps_clear p cte_level_bits s\<rbrakk> \<Longrightarrow> (ctes_of s)(p \<mapsto> cte) = map_to_ctes ((ksPSpace s)(a \<mapsto> obj')) proof (prove)
goal (2 subgoals):
 1. \<And>s a tcb getF setF. \<lbrakk>tcb_cte_cases (p - a) = Some (getF, setF); is_aligned a tcbBlockSizeBits; ps_clear a tcbBlockSizeBits s; a \<le> p; ksPSpace s a = Some (KOTCB tcb); \<forall>z. a < z \<and> z \<le> p \<longrightarrow> ksPSpace s z = None; cte = getF tcb\<rbrakk> \<Longrightarrow> Some (getF tcb) = ctes_of s p
 2. \<And>s a ba s'' obj' cte'. \<lbrakk>fst (lookupAround2 p (ksPSpace s)) = Some (a, ba); ba = KOCTE cte'; obj' = KOCTE cte; s'' = s; p = a; is_aligned p cte_level_bits; ps_clear p cte_level_bits s\<rbrakk> \<Longrightarrow> (ctes_of s)(p \<mapsto> cte) = map_to_ctes ((ksPSpace s)(a \<mapsto> obj')) proof (prove)
goal (5 subgoals):
 1. \<And>s a tcb getF setF. \<lbrakk>tcb_cte_cases (p - a) = Some (getF, setF); is_aligned a tcbBlockSizeBits; ps_clear a tcbBlockSizeBits s; a \<le> p; \<forall>z. a < z \<and> z \<le> p \<longrightarrow> ksPSpace s z = None; cte = getF tcb\<rbrakk> \<Longrightarrow> ps_clear a tcbBlockSizeBits s
 2. \<And>s a tcb getF setF. \<lbrakk>tcb_cte_cases (p - a) = Some (getF, setF); is_aligned a tcbBlockSizeBits; ps_clear a tcbBlockSizeBits s; a \<le> p; \<forall>z. a < z \<and> z \<le> p \<longrightarrow> ksPSpace s z = None; cte = getF tcb\<rbrakk> \<Longrightarrow> tcb_cte_cases (?ptr131 s a tcb getF setF - a) = Some (?getF131 s a tcb getF setF, ?setF131 s a tcb getF setF)
 3. \<And>s a tcb getF setF. \<lbrakk>tcb_cte_cases (p - a) = Some (getF, setF); is_aligned a tcbBlockSizeBits; ps_clear a tcbBlockSizeBits s; a \<le> p; \<forall>z. a < z \<and> z \<le> p \<longrightarrow> ksPSpace s z = None; cte = getF tcb\<rbrakk> \<Longrightarrow> cte = ?getF131 s a tcb getF setF tcb
 4. \<And>s a tcb getF setF. \<lbrakk>tcb_cte_cases (p - a) = Some (getF, setF); is_aligned a tcbBlockSizeBits; ps_clear a tcbBlockSizeBits s; a \<le> p; \<forall>z. a < z \<and> z \<le> p \<longrightarrow> ksPSpace s z = None; cte = getF tcb; cte_wp_at' ((=) cte) (?ptr131 s a tcb getF setF) s\<rbrakk> \<Longrightarrow> Some (getF tcb) = ctes_of s p
 5. \<And>s a ba s'' obj' cte'. \<lbrakk>fst (lookupAround2 p (ksPSpace s)) = Some (a, ba); ba = KOCTE cte'; obj' = KOCTE cte; s'' = s; p = a; is_aligned p cte_level_bits; ps_clear p cte_level_bits s\<rbrakk> \<Longrightarrow> (ctes_of s)(p \<mapsto> cte) = map_to_ctes ((ksPSpace s)(a \<mapsto> obj')) proof (prove)
goal (4 subgoals):
 1. \<And>s a tcb getF setF. \<lbrakk>tcb_cte_cases (p - a) = Some (getF, setF); is_aligned a tcbBlockSizeBits; ps_clear a tcbBlockSizeBits s; a \<le> p; \<forall>z. a < z \<and> z \<le> p \<longrightarrow> ksPSpace s z = None; cte = getF tcb\<rbrakk> \<Longrightarrow> tcb_cte_cases (?ptr131 s a tcb getF setF - a) = Some (?getF131 s a tcb getF setF, ?setF131 s a tcb getF setF)
 2. \<And>s a tcb getF setF. \<lbrakk>tcb_cte_cases (p - a) = Some (getF, setF); is_aligned a tcbBlockSizeBits; ps_clear a tcbBlockSizeBits s; a \<le> p; \<forall>z. a < z \<and> z \<le> p \<longrightarrow> ksPSpace s z = None; cte = getF tcb\<rbrakk> \<Longrightarrow> cte = ?getF131 s a tcb getF setF tcb
 3. \<And>s a tcb getF setF. \<lbrakk>tcb_cte_cases (p - a) = Some (getF, setF); is_aligned a tcbBlockSizeBits; ps_clear a tcbBlockSizeBits s; a \<le> p; \<forall>z. a < z \<and> z \<le> p \<longrightarrow> ksPSpace s z = None; cte = getF tcb; cte_wp_at' ((=) cte) (?ptr131 s a tcb getF setF) s\<rbrakk> \<Longrightarrow> Some (getF tcb) = ctes_of s p
 4. \<And>s a ba s'' obj' cte'. \<lbrakk>fst (lookupAround2 p (ksPSpace s)) = Some (a, ba); ba = KOCTE cte'; obj' = KOCTE cte; s'' = s; p = a; is_aligned p cte_level_bits; ps_clear p cte_level_bits s\<rbrakk> \<Longrightarrow> (ctes_of s)(p \<mapsto> cte) = map_to_ctes ((ksPSpace s)(a \<mapsto> obj')) proof (prove)
goal (2 subgoals):
 1. \<And>s a tcb getF setF. \<lbrakk>tcb_cte_cases (p - a) = Some (getF, setF); is_aligned a tcbBlockSizeBits; ps_clear a tcbBlockSizeBits s; a \<le> p; \<forall>z. a < z \<and> z \<le> p \<longrightarrow> ksPSpace s z = None; cte = getF tcb; cte_wp_at' ((=) cte) p s\<rbrakk> \<Longrightarrow> Some (getF tcb) = ctes_of s p
 2. \<And>s a ba s'' obj' cte'. \<lbrakk>fst (lookupAround2 p (ksPSpace s)) = Some (a, ba); ba = KOCTE cte'; obj' = KOCTE cte; s'' = s; p = a; is_aligned p cte_level_bits; ps_clear p cte_level_bits s\<rbrakk> \<Longrightarrow> (ctes_of s)(p \<mapsto> cte) = map_to_ctes ((ksPSpace s)(a \<mapsto> obj')) proof (prove)
goal (1 subgoal):
 1. \<And>s a ba s'' obj' cte'. \<lbrakk>fst (lookupAround2 p (ksPSpace s)) = Some (a, ba); ba = KOCTE cte'; obj' = KOCTE cte; s'' = s; p = a; is_aligned p cte_level_bits; ps_clear p cte_level_bits s\<rbrakk> \<Longrightarrow> (ctes_of s)(p \<mapsto> cte) = map_to_ctes ((ksPSpace s)(a \<mapsto> obj')) proof (prove)
goal:
No subgoals!