theory Detype_R

lemma locateCTE_ko_wp_at':
  "\<lbrace>cte_at' src and pspace_distinct' \<rbrace>
   locateCTE src
   \<lbrace>\<lambda>rv. ko_wp_at' \<top> rv \<rbrace>" apply (clarsimp simp:locateCTE_def split_def) apply wp apply (clarsimp simp:cte_wp_at'_def getObject_def
    gets_def split_def get_def bind_def return_def
    ko_wp_at'_def lookupAround2_char1 assert_opt_def) apply (clarsimp split:option.splits
    simp:fail_def return_def lookupAround2_char1) apply (case_tac ba) apply (simp_all add:cte_check_def) apply (clarsimp simp:lookupAround2_char1
      objBits_simps cte_update_def) apply (drule(1) pspace_distinctD')+ apply (simp add:objBits_simps) apply (clarsimp simp:objBits_simps cte_update_def) apply (drule(1) pspace_distinctD')+ apply (simp add:objBits_simps) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>cte_wp_at' (\<lambda>_. True) src and pspace_distinct'\<rbrace> locateCTE src \<lbrace>ko_wp_at' (\<lambda>_. True)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>cte_wp_at' (\<lambda>_. True) src and pspace_distinct'\<rbrace> do ps <- gets ksPSpace;
p <- assert_opt (fst (lookupAround2 src ps));
y <- assert (cte_check (snd p) src (fst p) (snd (lookupAround2 src ps)));
return (fst p)
od \<lbrace>ko_wp_at' (\<lambda>_. True)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (cte_wp_at' (\<lambda>_. True) src and pspace_distinct') s \<Longrightarrow> fst (lookupAround2 src (ksPSpace s)) \<noteq> None \<longrightarrow> cte_check (snd (the (fst (lookupAround2 src (ksPSpace s))))) src (fst (the (fst (lookupAround2 src (ksPSpace s))))) (snd (lookupAround2 src (ksPSpace s))) \<longrightarrow> ko_wp_at' (\<lambda>_. True) (fst (the (fst (lookupAround2 src (ksPSpace s))))) s proof (prove)
goal (1 subgoal):
 1. \<And>s cte a b. \<lbrakk>pspace_distinct' s; (\<Union>x\<in>fst ((case fst (lookupAround2 src (ksPSpace s)) of None \<Rightarrow> fail | Some v \<Rightarrow> \<lambda>s. ({(v, s)}, False)) s). fst (loadObject src (fst (fst x)) (snd (lookupAround2 src (ksPSpace s))) (snd (fst x)) (snd x))) = {(cte, s)}; a \<le> src; \<forall>z. a < z \<and> z \<le> src \<longrightarrow> ksPSpace s z = None; ksPSpace s a = Some b; cte_check (snd (the (fst (lookupAround2 src (ksPSpace s))))) src (fst (the (fst (lookupAround2 src (ksPSpace s))))) (snd (lookupAround2 src (ksPSpace s)))\<rbrakk> \<Longrightarrow> \<exists>ko. ksPSpace s (fst (the (fst (lookupAround2 src (ksPSpace s))))) = Some ko \<and> is_aligned (fst (the (fst (lookupAround2 src (ksPSpace s))))) (objBitsKO ko) \<and> ps_clear (fst (the (fst (lookupAround2 src (ksPSpace s))))) (objBitsKO ko) s proof (prove)
goal (1 subgoal):
 1. \<And>s cte a b aa ba. \<lbrakk>a \<le> src; \<forall>z. a < z \<and> z \<le> src \<longrightarrow> ksPSpace s z = None; ksPSpace s a = Some b; cte_check ba src aa (snd (lookupAround2 src (ksPSpace s))); pspace_distinct' s; fst (loadObject src aa (snd (lookupAround2 src (ksPSpace s))) ba s) = {(cte, s)}; aa \<le> src; ksPSpace s aa = Some ba; \<forall>z. aa < z \<and> z \<le> src \<longrightarrow> ksPSpace s z = None\<rbrakk> \<Longrightarrow> is_aligned aa (objBitsKO ba) \<and> ps_clear aa (objBitsKO ba) s proof (prove)
goal (8 subgoals):
 1. \<And>s cte a b aa ba x1. \<lbrakk>a \<le> src; \<forall>z. a < z \<and> z \<le> src \<longrightarrow> ksPSpace s z = None; ksPSpace s a = Some b; cte_check ba src aa (snd (lookupAround2 src (ksPSpace s))); pspace_distinct' s; fst (loadObject src aa (snd (lookupAround2 src (ksPSpace s))) ba s) = {(cte, s)}; aa \<le> src; ksPSpace s aa = Some ba; \<forall>z. aa < z \<and> z \<le> src \<longrightarrow> ksPSpace s z = None; ba = KOEndpoint x1\<rbrakk> \<Longrightarrow> is_aligned aa (objBitsKO ba) \<and> ps_clear aa (objBitsKO ba) s
 2. \<And>s cte a b aa ba x2. \<lbrakk>a \<le> src; \<forall>z. a < z \<and> z \<le> src \<longrightarrow> ksPSpace s z = None; ksPSpace s a = Some b; cte_check ba src aa (snd (lookupAround2 src (ksPSpace s))); pspace_distinct' s; fst (loadObject src aa (snd (lookupAround2 src (ksPSpace s))) ba s) = {(cte, s)}; aa \<le> src; ksPSpace s aa = Some ba; \<forall>z. aa < z \<and> z \<le> src \<longrightarrow> ksPSpace s z = None; ba = KONotification x2\<rbrakk> \<Longrightarrow> is_aligned aa (objBitsKO ba) \<and> ps_clear aa (objBitsKO ba) s
 3. \<And>s cte a b aa ba. \<lbrakk>a \<le> src; \<forall>z. a < z \<and> z \<le> src \<longrightarrow> ksPSpace s z = None; ksPSpace s a = Some b; cte_check ba src aa (snd (lookupAround2 src (ksPSpace s))); pspace_distinct' s; fst (loadObject src aa (snd (lookupAround2 src (ksPSpace s))) ba s) = {(cte, s)}; aa \<le> src; ksPSpace s aa = Some ba; \<forall>z. aa < z \<and> z \<le> src \<longrightarrow> ksPSpace s z = None; ba = KOKernelData\<rbrakk> \<Longrightarrow> is_aligned aa (objBitsKO ba) \<and> ps_clear aa (objBitsKO ba) s
 4. \<And>s cte a b aa ba. \<lbrakk>a \<le> src; \<forall>z. a < z \<and> z \<le> src \<longrightarrow> ksPSpace s z = None; ksPSpace s a = Some b; cte_check ba src aa (snd (lookupAround2 src (ksPSpace s))); pspace_distinct' s; fst (loadObject src aa (snd (lookupAround2 src (ksPSpace s))) ba s) = {(cte, s)}; aa \<le> src; ksPSpace s aa = Some ba; \<forall>z. aa < z \<and> z \<le> src \<longrightarrow> ksPSpace s z = None; ba = KOUserData\<rbrakk> \<Longrightarrow> is_aligned aa (objBitsKO ba) \<and> ps_clear aa (objBitsKO ba) s
 5. \<And>s cte a b aa ba. \<lbrakk>a \<le> src; \<forall>z. a < z \<and> z \<le> src \<longrightarrow> ksPSpace s z = None; ksPSpace s a = Some b; cte_check ba src aa (snd (lookupAround2 src (ksPSpace s))); pspace_distinct' s; fst (loadObject src aa (snd (lookupAround2 src (ksPSpace s))) ba s) = {(cte, s)}; aa \<le> src; ksPSpace s aa = Some ba; \<forall>z. aa < z \<and> z \<le> src \<longrightarrow> ksPSpace s z = None; ba = KOUserDataDevice\<rbrakk> \<Longrightarrow> is_aligned aa (objBitsKO ba) \<and> ps_clear aa (objBitsKO ba) s
 6. \<And>s cte a b aa ba x6. \<lbrakk>a \<le> src; \<forall>z. a < z \<and> z \<le> src \<longrightarrow> ksPSpace s z = None; ksPSpace s a = Some b; cte_check ba src aa (snd (lookupAround2 src (ksPSpace s))); pspace_distinct' s; fst (loadObject src aa (snd (lookupAround2 src (ksPSpace s))) ba s) = {(cte, s)}; aa \<le> src; ksPSpace s aa = Some ba; \<forall>z. aa < z \<and> z \<le> src \<longrightarrow> ksPSpace s z = None; ba = KOTCB x6\<rbrakk> \<Longrightarrow> is_aligned aa (objBitsKO ba) \<and> ps_clear aa (objBitsKO ba) s
 7. \<And>s cte a b aa ba x7. \<lbrakk>a \<le> src; \<forall>z. a < z \<and> z \<le> src \<longrightarrow> ksPSpace s z = None; ksPSpace s a = Some b; cte_check ba src aa (snd (lookupAround2 src (ksPSpace s))); pspace_distinct' s; fst (loadObject src aa (snd (lookupAround2 src (ksPSpace s))) ba s) = {(cte, s)}; aa \<le> src; ksPSpace s aa = Some ba; \<forall>z. aa < z \<and> z \<le> src \<longrightarrow> ksPSpace s z = None; ba = KOCTE x7\<rbrakk> \<Longrightarrow> is_aligned aa (objBitsKO ba) \<and> ps_clear aa (objBitsKO ba) s
 8. \<And>s cte a b aa ba x8. \<lbrakk>a \<le> src; \<forall>z. a < z \<and> z \<le> src \<longrightarrow> ksPSpace s z = None; ksPSpace s a = Some b; cte_check ba src aa (snd (lookupAround2 src (ksPSpace s))); pspace_distinct' s; fst (loadObject src aa (snd (lookupAround2 src (ksPSpace s))) ba s) = {(cte, s)}; aa \<le> src; ksPSpace s aa = Some ba; \<forall>z. aa < z \<and> z \<le> src \<longrightarrow> ksPSpace s z = None; ba = KOArch x8\<rbrakk> \<Longrightarrow> is_aligned aa (objBitsKO ba) \<and> ps_clear aa (objBitsKO ba) s proof (prove)
goal (2 subgoals):
 1. \<And>s cte a b aa ba x6. \<lbrakk>a \<le> src; \<forall>z. a < z \<and> z \<le> src \<longrightarrow> ksPSpace s z = None; ksPSpace s a = Some b; is_aligned aa (objBits x6) \<and> (case snd (lookupAround2 src (ksPSpace s)) of None \<Rightarrow> True | Some z \<Rightarrow> 2 ^ objBits x6 \<le> z - aa) \<and> (src - aa = tcbVTableSlot << cteSizeBits \<or> src - aa = tcbCTableSlot << cteSizeBits \<or> src - aa = tcbReplySlot << cteSizeBits \<or> src - aa = tcbCallerSlot << cteSizeBits \<or> src - aa = tcbIPCBufferSlot << cteSizeBits); pspace_distinct' s; fst (loadObject src aa (snd (lookupAround2 src (ksPSpace s))) (KOTCB x6) s) = {(cte, s)}; aa \<le> src; ksPSpace s aa = Some (KOTCB x6); \<forall>z. aa < z \<and> z \<le> src \<longrightarrow> ksPSpace s z = None; ba = KOTCB x6\<rbrakk> \<Longrightarrow> is_aligned aa (objBitsKO (KOTCB x6)) \<and> ps_clear aa (objBitsKO (KOTCB x6)) s
 2. \<And>s cte a b ba x7. \<lbrakk>a \<le> src; \<forall>z. a < z \<and> z \<le> src \<longrightarrow> ksPSpace s z = None; ksPSpace s a = Some b; is_aligned src (objBits makeObject) \<and> (case snd (lookupAround2 src (ksPSpace s)) of None \<Rightarrow> True | Some z \<Rightarrow> 2 ^ objBits makeObject \<le> z - src); pspace_distinct' s; fst (loadObject src src (snd (lookupAround2 src (ksPSpace s))) (KOCTE x7) s) = {(cte, s)}; ksPSpace s src = Some (KOCTE x7); \<forall>z. src < z \<and> z \<le> src \<longrightarrow> ksPSpace s z = None; ba = KOCTE x7\<rbrakk> \<Longrightarrow> is_aligned src (objBitsKO (KOCTE x7)) \<and> ps_clear src (objBitsKO (KOCTE x7)) s proof (prove)
goal (2 subgoals):
 1. \<And>s cte a b aa x6. \<lbrakk>a \<le> src; \<forall>z. a < z \<and> z \<le> src \<longrightarrow> ksPSpace s z = None; ksPSpace s a = Some b; pspace_distinct' s; fst (loadObject src aa (snd (lookupAround2 src (ksPSpace s))) (KOTCB x6) s) = {(cte, s)}; aa \<le> src; ksPSpace s aa = Some (KOTCB x6); \<forall>z. aa < z \<and> z \<le> src \<longrightarrow> ksPSpace s z = None; is_aligned aa tcbBlockSizeBits; case snd (lookupAround2 src (ksPSpace s)) of None \<Rightarrow> True | Some z \<Rightarrow> 2 ^ tcbBlockSizeBits \<le> z - aa; src - aa = tcbVTableSlot << cteSizeBits \<or> src - aa = tcbCTableSlot << cteSizeBits \<or> src - aa = tcbReplySlot << cteSizeBits \<or> src - aa = tcbCallerSlot << cteSizeBits \<or> src - aa = tcbIPCBufferSlot << cteSizeBits\<rbrakk> \<Longrightarrow> ps_clear aa tcbBlockSizeBits s
 2. \<And>s cte a b ba x7. \<lbrakk>a \<le> src; \<forall>z. a < z \<and> z \<le> src \<longrightarrow> ksPSpace s z = None; ksPSpace s a = Some b; is_aligned src (objBits makeObject) \<and> (case snd (lookupAround2 src (ksPSpace s)) of None \<Rightarrow> True | Some z \<Rightarrow> 2 ^ objBits makeObject \<le> z - src); pspace_distinct' s; fst (loadObject src src (snd (lookupAround2 src (ksPSpace s))) (KOCTE x7) s) = {(cte, s)}; ksPSpace s src = Some (KOCTE x7); \<forall>z. src < z \<and> z \<le> src \<longrightarrow> ksPSpace s z = None; ba = KOCTE x7\<rbrakk> \<Longrightarrow> is_aligned src (objBitsKO (KOCTE x7)) \<and> ps_clear src (objBitsKO (KOCTE x7)) s proof (prove)
goal (2 subgoals):
 1. \<And>s cte a b aa x6. \<lbrakk>a \<le> src; \<forall>z. a < z \<and> z \<le> src \<longrightarrow> ksPSpace s z = None; pspace_distinct' s; fst (loadObject src aa (snd (lookupAround2 src (ksPSpace s))) (KOTCB x6) s) = {(cte, s)}; aa \<le> src; \<forall>z. aa < z \<and> z \<le> src \<longrightarrow> ksPSpace s z = None; is_aligned aa tcbBlockSizeBits; case snd (lookupAround2 src (ksPSpace s)) of None \<Rightarrow> True | Some z \<Rightarrow> 2 ^ tcbBlockSizeBits \<le> z - aa; src - aa = tcbVTableSlot << cteSizeBits \<or> src - aa = tcbCTableSlot << cteSizeBits \<or> src - aa = tcbReplySlot << cteSizeBits \<or> src - aa = tcbCallerSlot << cteSizeBits \<or> src - aa = tcbIPCBufferSlot << cteSizeBits; ps_clear a (objBitsKO b) s; ps_clear aa (objBitsKO (KOTCB x6)) s\<rbrakk> \<Longrightarrow> ps_clear aa tcbBlockSizeBits s
 2. \<And>s cte a b ba x7. \<lbrakk>a \<le> src; \<forall>z. a < z \<and> z \<le> src \<longrightarrow> ksPSpace s z = None; ksPSpace s a = Some b; is_aligned src (objBits makeObject) \<and> (case snd (lookupAround2 src (ksPSpace s)) of None \<Rightarrow> True | Some z \<Rightarrow> 2 ^ objBits makeObject \<le> z - src); pspace_distinct' s; fst (loadObject src src (snd (lookupAround2 src (ksPSpace s))) (KOCTE x7) s) = {(cte, s)}; ksPSpace s src = Some (KOCTE x7); \<forall>z. src < z \<and> z \<le> src \<longrightarrow> ksPSpace s z = None; ba = KOCTE x7\<rbrakk> \<Longrightarrow> is_aligned src (objBitsKO (KOCTE x7)) \<and> ps_clear src (objBitsKO (KOCTE x7)) s proof (prove)
goal (1 subgoal):
 1. \<And>s cte a b ba x7. \<lbrakk>a \<le> src; \<forall>z. a < z \<and> z \<le> src \<longrightarrow> ksPSpace s z = None; ksPSpace s a = Some b; is_aligned src (objBits makeObject) \<and> (case snd (lookupAround2 src (ksPSpace s)) of None \<Rightarrow> True | Some z \<Rightarrow> 2 ^ objBits makeObject \<le> z - src); pspace_distinct' s; fst (loadObject src src (snd (lookupAround2 src (ksPSpace s))) (KOCTE x7) s) = {(cte, s)}; ksPSpace s src = Some (KOCTE x7); \<forall>z. src < z \<and> z \<le> src \<longrightarrow> ksPSpace s z = None; ba = KOCTE x7\<rbrakk> \<Longrightarrow> is_aligned src (objBitsKO (KOCTE x7)) \<and> ps_clear src (objBitsKO (KOCTE x7)) s proof (prove)
goal (1 subgoal):
 1. \<And>s cte a b x7. \<lbrakk>a \<le> src; \<forall>z. a < z \<and> z \<le> src \<longrightarrow> ksPSpace s z = None; ksPSpace s a = Some b; pspace_distinct' s; fst (loadObject src src (snd (lookupAround2 src (ksPSpace s))) (KOCTE x7) s) = {(cte, s)}; ksPSpace s src = Some (KOCTE x7); \<forall>z. src < z \<and> z \<le> src \<longrightarrow> ksPSpace s z = None; is_aligned src cteSizeBits; case snd (lookupAround2 src (ksPSpace s)) of None \<Rightarrow> True | Some z \<Rightarrow> 2 ^ cteSizeBits \<le> z - src\<rbrakk> \<Longrightarrow> ps_clear src cteSizeBits s proof (prove)
goal (1 subgoal):
 1. \<And>s cte a b x7. \<lbrakk>a \<le> src; \<forall>z. a < z \<and> z \<le> src \<longrightarrow> ksPSpace s z = None; pspace_distinct' s; fst (loadObject src src (snd (lookupAround2 src (ksPSpace s))) (KOCTE x7) s) = {(cte, s)}; \<forall>z. src < z \<and> z \<le> src \<longrightarrow> ksPSpace s z = None; is_aligned src cteSizeBits; case snd (lookupAround2 src (ksPSpace s)) of None \<Rightarrow> True | Some z \<Rightarrow> 2 ^ cteSizeBits \<le> z - src; ps_clear a (objBitsKO b) s; ps_clear src (objBitsKO (KOCTE x7)) s\<rbrakk> \<Longrightarrow> ps_clear src cteSizeBits s proof (prove)
goal:
No subgoals!