theory Detype_R

lemma placeNewObject_cte_wp_at'':
  "\<lbrace>\<lambda>s. cte_wp_at' P slot s \<and>
  objBitsKO (injectKOS val) + us < word_bits \<and>
  is_aligned ptr (objBitsKO (injectKOS val) + us) \<and>
  pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) s \<and>
  pspace_aligned' s \<and> pspace_distinct' s\<rbrace>
  placeNewObject ptr val us \<lbrace>\<lambda>a s. cte_wp_at' P slot s\<rbrace>" apply (simp add:cte_wp_at_cases_mask' obj_at'_real_def) apply (wp hoare_vcg_disj_lift placeNewObject_ko_wp_at') apply (clarsimp simp:conj_comms) apply (intro conjI impI allI impI) apply (drule(4) not_in_new_cap_addrs') apply (clarsimp simp:ko_wp_at'_def) apply (drule (4)not_in_new_cap_addrs')+ apply (clarsimp simp:ko_wp_at'_def) apply (elim disjE) apply simp apply clarsimp apply (drule (4)not_in_new_cap_addrs')+ apply (clarsimp simp:ko_wp_at'_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. cte_wp_at' P slot s \<and> objBitsKO (injectKOS val) + us < word_bits \<and> is_aligned ptr (objBitsKO (injectKOS val) + us) \<and> pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) s \<and> pspace_aligned' s \<and> pspace_distinct' s\<rbrace> placeNewObject ptr val us \<lbrace>\<lambda>a. cte_wp_at' P slot\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. (ko_wp_at' (\<lambda>ko. \<exists>obj. projectKO_opt ko = Some obj \<and> P obj) slot s \<or> slot && mask tcbBlockSizeBits \<in> dom tcb_cte_cases \<and> ko_wp_at' (\<lambda>ko. \<exists>obj. projectKO_opt ko = Some obj \<and> P (fst (the (tcb_cte_cases (slot && mask tcbBlockSizeBits))) obj)) (slot && ~~ mask tcbBlockSizeBits) s) \<and> objBitsKO (injectKOS val) + us < word_bits \<and> is_aligned ptr (objBitsKO (injectKOS val) + us) \<and> pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) s \<and> pspace_aligned' s \<and> pspace_distinct' s\<rbrace> placeNewObject ptr val us \<lbrace>\<lambda>a s. ko_wp_at' (\<lambda>ko. \<exists>obj. projectKO_opt ko = Some obj \<and> P obj) slot s \<or> slot && mask tcbBlockSizeBits \<in> dom tcb_cte_cases \<and> ko_wp_at' (\<lambda>ko. \<exists>obj. projectKO_opt ko = Some obj \<and> P (fst (the (tcb_cte_cases (slot && mask tcbBlockSizeBits))) obj)) (slot && ~~ mask tcbBlockSizeBits) s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (ko_wp_at' (\<lambda>ko. \<exists>obj. projectKO_opt ko = Some obj \<and> P obj) slot s \<or> slot && mask tcbBlockSizeBits \<in> dom tcb_cte_cases \<and> ko_wp_at' (\<lambda>ko. \<exists>obj. projectKO_opt ko = Some obj \<and> P (fst (the (tcb_cte_cases (slot && mask tcbBlockSizeBits))) obj)) (slot && ~~ mask tcbBlockSizeBits) s) \<and> objBitsKO (injectKOS val) + us < word_bits \<and> is_aligned ptr (objBitsKO (injectKOS val) + us) \<and> pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) s \<and> pspace_aligned' s \<and> pspace_distinct' s \<Longrightarrow> (if slot \<in> set (new_cap_addrs (2 ^ us) ptr (injectKOS val)) then \<exists>obj. projectKO_opt (injectKOS val) = Some obj \<and> P obj else ko_wp_at' (\<lambda>ko. \<exists>obj. projectKO_opt ko = Some obj \<and> P obj) slot s) \<and> objBitsKO (injectKOS val) + us < word_bits \<and> is_aligned ptr (objBitsKO (injectKOS val) + us) \<and> pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) s \<and> pspace_aligned' s \<and> pspace_distinct' s \<or> slot && mask tcbBlockSizeBits \<in> dom tcb_cte_cases \<and> (if slot && ~~ mask tcbBlockSizeBits \<in> set (new_cap_addrs (2 ^ us) ptr (injectKOS val)) then \<exists>obj. projectKO_opt (injectKOS val) = Some obj \<and> P (fst (the (tcb_cte_cases (slot && mask tcbBlockSizeBits))) obj) else ko_wp_at' (\<lambda>ko. \<exists>obj. projectKO_opt ko = Some obj \<and> P (fst (the (tcb_cte_cases (slot && mask tcbBlockSizeBits))) obj)) (slot && ~~ mask tcbBlockSizeBits) s) \<and> objBitsKO (injectKOS val) + us < word_bits \<and> is_aligned ptr (objBitsKO (injectKOS val) + us) \<and> pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) s \<and> pspace_aligned' s \<and> pspace_distinct' s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>pspace_aligned' s; pspace_distinct' s; is_aligned ptr (objBitsKO (injectKOS val) + us); objBitsKO (injectKOS val) + us < word_bits; pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) s; ko_wp_at' (\<lambda>ko. \<exists>obj. P obj \<and> projectKO_opt ko = Some obj) slot s \<or> slot && mask tcbBlockSizeBits \<in> dom tcb_cte_cases \<and> ko_wp_at' (\<lambda>ko. \<exists>obj. projectKO_opt ko = Some obj \<and> P (fst (the (tcb_cte_cases (slot && mask tcbBlockSizeBits))) obj)) (slot && ~~ mask tcbBlockSizeBits) s\<rbrakk> \<Longrightarrow> (slot && ~~ mask tcbBlockSizeBits \<notin> set (new_cap_addrs (2 ^ us) ptr (injectKOS val)) \<longrightarrow> slot \<in> set (new_cap_addrs (2 ^ us) ptr (injectKOS val)) \<longrightarrow> (\<exists>obj. P obj \<and> projectKO_opt (injectKOS val) = Some obj) \<or> slot && mask tcbBlockSizeBits \<in> dom tcb_cte_cases \<and> ko_wp_at' (\<lambda>ko. \<exists>obj. projectKO_opt ko = Some obj \<and> P (fst (the (tcb_cte_cases (slot && mask tcbBlockSizeBits))) obj)) (slot && ~~ mask tcbBlockSizeBits) s) \<and> (slot && ~~ mask tcbBlockSizeBits \<in> set (new_cap_addrs (2 ^ us) ptr (injectKOS val)) \<longrightarrow> (slot \<in> set (new_cap_addrs (2 ^ us) ptr (injectKOS val)) \<longrightarrow> (\<exists>obj. P obj \<and> projectKO_opt (injectKOS val) = Some obj) \<or> slot && mask tcbBlockSizeBits \<in> dom tcb_cte_cases \<and> (\<exists>obj. projectKO_opt (injectKOS val) = Some obj \<and> P (fst (the (tcb_cte_cases (slot && mask tcbBlockSizeBits))) obj))) \<and> (slot \<notin> set (new_cap_addrs (2 ^ us) ptr (injectKOS val)) \<longrightarrow> ko_wp_at' (\<lambda>ko. \<exists>obj. P obj \<and> projectKO_opt ko = Some obj) slot s \<or> slot && mask tcbBlockSizeBits \<in> dom tcb_cte_cases \<and> (\<exists>obj. projectKO_opt (injectKOS val) = Some obj \<and> P (fst (the (tcb_cte_cases (slot && mask tcbBlockSizeBits))) obj)))) proof (prove)
goal (3 subgoals):
 1. \<And>s. \<lbrakk>pspace_aligned' s; pspace_distinct' s; is_aligned ptr (objBitsKO (injectKOS val) + us); objBitsKO (injectKOS val) + us < word_bits; pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) s; ko_wp_at' (\<lambda>ko. \<exists>obj. P obj \<and> projectKO_opt ko = Some obj) slot s \<or> slot && mask tcbBlockSizeBits \<in> dom tcb_cte_cases \<and> ko_wp_at' (\<lambda>ko. \<exists>obj. projectKO_opt ko = Some obj \<and> P (fst (the (tcb_cte_cases (slot && mask tcbBlockSizeBits))) obj)) (slot && ~~ mask tcbBlockSizeBits) s; slot && ~~ mask tcbBlockSizeBits \<notin> set (new_cap_addrs (2 ^ us) ptr (injectKOS val)); slot \<in> set (new_cap_addrs (2 ^ us) ptr (injectKOS val))\<rbrakk> \<Longrightarrow> (\<exists>obj. P obj \<and> projectKO_opt (injectKOS val) = Some obj) \<or> slot && mask tcbBlockSizeBits \<in> dom tcb_cte_cases \<and> ko_wp_at' (\<lambda>ko. \<exists>obj. projectKO_opt ko = Some obj \<and> P (fst (the (tcb_cte_cases (slot && mask tcbBlockSizeBits))) obj)) (slot && ~~ mask tcbBlockSizeBits) s
 2. \<And>s. \<lbrakk>pspace_aligned' s; pspace_distinct' s; is_aligned ptr (objBitsKO (injectKOS val) + us); objBitsKO (injectKOS val) + us < word_bits; pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) s; ko_wp_at' (\<lambda>ko. \<exists>obj. P obj \<and> projectKO_opt ko = Some obj) slot s \<or> slot && mask tcbBlockSizeBits \<in> dom tcb_cte_cases \<and> ko_wp_at' (\<lambda>ko. \<exists>obj. projectKO_opt ko = Some obj \<and> P (fst (the (tcb_cte_cases (slot && mask tcbBlockSizeBits))) obj)) (slot && ~~ mask tcbBlockSizeBits) s; slot && ~~ mask tcbBlockSizeBits \<in> set (new_cap_addrs (2 ^ us) ptr (injectKOS val)); slot \<in> set (new_cap_addrs (2 ^ us) ptr (injectKOS val))\<rbrakk> \<Longrightarrow> (\<exists>obj. P obj \<and> projectKO_opt (injectKOS val) = Some obj) \<or> slot && mask tcbBlockSizeBits \<in> dom tcb_cte_cases \<and> (\<exists>obj. projectKO_opt (injectKOS val) = Some obj \<and> P (fst (the (tcb_cte_cases (slot && mask tcbBlockSizeBits))) obj))
 3. \<And>s. \<lbrakk>pspace_aligned' s; pspace_distinct' s; is_aligned ptr (objBitsKO (injectKOS val) + us); objBitsKO (injectKOS val) + us < word_bits; pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) s; ko_wp_at' (\<lambda>ko. \<exists>obj. P obj \<and> projectKO_opt ko = Some obj) slot s \<or> slot && mask tcbBlockSizeBits \<in> dom tcb_cte_cases \<and> ko_wp_at' (\<lambda>ko. \<exists>obj. projectKO_opt ko = Some obj \<and> P (fst (the (tcb_cte_cases (slot && mask tcbBlockSizeBits))) obj)) (slot && ~~ mask tcbBlockSizeBits) s; slot && ~~ mask tcbBlockSizeBits \<in> set (new_cap_addrs (2 ^ us) ptr (injectKOS val)); slot \<notin> set (new_cap_addrs (2 ^ us) ptr (injectKOS val))\<rbrakk> \<Longrightarrow> ko_wp_at' (\<lambda>ko. \<exists>obj. P obj \<and> projectKO_opt ko = Some obj) slot s \<or> slot && mask tcbBlockSizeBits \<in> dom tcb_cte_cases \<and> (\<exists>obj. projectKO_opt (injectKOS val) = Some obj \<and> P (fst (the (tcb_cte_cases (slot && mask tcbBlockSizeBits))) obj)) proof (prove)
goal (3 subgoals):
 1. \<And>s. \<lbrakk>pspace_aligned' s; pspace_distinct' s; is_aligned ptr (objBitsKO (injectKOS val) + us); objBitsKO (injectKOS val) + us < word_bits; pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) s; ko_wp_at' (\<lambda>ko. \<exists>obj. P obj \<and> projectKO_opt ko = Some obj) slot s \<or> slot && mask tcbBlockSizeBits \<in> dom tcb_cte_cases \<and> ko_wp_at' (\<lambda>ko. \<exists>obj. projectKO_opt ko = Some obj \<and> P (fst (the (tcb_cte_cases (slot && mask tcbBlockSizeBits))) obj)) (slot && ~~ mask tcbBlockSizeBits) s; slot && ~~ mask tcbBlockSizeBits \<notin> set (new_cap_addrs (2 ^ us) ptr (injectKOS val)); ksPSpace s slot = None\<rbrakk> \<Longrightarrow> (\<exists>obj. P obj \<and> projectKO_opt (injectKOS val) = Some obj) \<or> slot && mask tcbBlockSizeBits \<in> dom tcb_cte_cases \<and> ko_wp_at' (\<lambda>ko. \<exists>obj. projectKO_opt ko = Some obj \<and> P (fst (the (tcb_cte_cases (slot && mask tcbBlockSizeBits))) obj)) (slot && ~~ mask tcbBlockSizeBits) s
 2. \<And>s. \<lbrakk>pspace_aligned' s; pspace_distinct' s; is_aligned ptr (objBitsKO (injectKOS val) + us); objBitsKO (injectKOS val) + us < word_bits; pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) s; ko_wp_at' (\<lambda>ko. \<exists>obj. P obj \<and> projectKO_opt ko = Some obj) slot s \<or> slot && mask tcbBlockSizeBits \<in> dom tcb_cte_cases \<and> ko_wp_at' (\<lambda>ko. \<exists>obj. projectKO_opt ko = Some obj \<and> P (fst (the (tcb_cte_cases (slot && mask tcbBlockSizeBits))) obj)) (slot && ~~ mask tcbBlockSizeBits) s; slot && ~~ mask tcbBlockSizeBits \<in> set (new_cap_addrs (2 ^ us) ptr (injectKOS val)); slot \<in> set (new_cap_addrs (2 ^ us) ptr (injectKOS val))\<rbrakk> \<Longrightarrow> (\<exists>obj. P obj \<and> projectKO_opt (injectKOS val) = Some obj) \<or> slot && mask tcbBlockSizeBits \<in> dom tcb_cte_cases \<and> (\<exists>obj. projectKO_opt (injectKOS val) = Some obj \<and> P (fst (the (tcb_cte_cases (slot && mask tcbBlockSizeBits))) obj))
 3. \<And>s. \<lbrakk>pspace_aligned' s; pspace_distinct' s; is_aligned ptr (objBitsKO (injectKOS val) + us); objBitsKO (injectKOS val) + us < word_bits; pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) s; ko_wp_at' (\<lambda>ko. \<exists>obj. P obj \<and> projectKO_opt ko = Some obj) slot s \<or> slot && mask tcbBlockSizeBits \<in> dom tcb_cte_cases \<and> ko_wp_at' (\<lambda>ko. \<exists>obj. projectKO_opt ko = Some obj \<and> P (fst (the (tcb_cte_cases (slot && mask tcbBlockSizeBits))) obj)) (slot && ~~ mask tcbBlockSizeBits) s; slot && ~~ mask tcbBlockSizeBits \<in> set (new_cap_addrs (2 ^ us) ptr (injectKOS val)); slot \<notin> set (new_cap_addrs (2 ^ us) ptr (injectKOS val))\<rbrakk> \<Longrightarrow> ko_wp_at' (\<lambda>ko. \<exists>obj. P obj \<and> projectKO_opt ko = Some obj) slot s \<or> slot && mask tcbBlockSizeBits \<in> dom tcb_cte_cases \<and> (\<exists>obj. projectKO_opt (injectKOS val) = Some obj \<and> P (fst (the (tcb_cte_cases (slot && mask tcbBlockSizeBits))) obj)) proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>pspace_aligned' s; pspace_distinct' s; is_aligned ptr (objBitsKO (injectKOS val) + us); objBitsKO (injectKOS val) + us < word_bits; pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) s; ko_wp_at' (\<lambda>ko. \<exists>obj. P obj \<and> projectKO_opt ko = Some obj) slot s \<or> slot && mask tcbBlockSizeBits \<in> dom tcb_cte_cases \<and> ko_wp_at' (\<lambda>ko. \<exists>obj. projectKO_opt ko = Some obj \<and> P (fst (the (tcb_cte_cases (slot && mask tcbBlockSizeBits))) obj)) (slot && ~~ mask tcbBlockSizeBits) s; slot && ~~ mask tcbBlockSizeBits \<in> set (new_cap_addrs (2 ^ us) ptr (injectKOS val)); slot \<in> set (new_cap_addrs (2 ^ us) ptr (injectKOS val))\<rbrakk> \<Longrightarrow> (\<exists>obj. P obj \<and> projectKO_opt (injectKOS val) = Some obj) \<or> slot && mask tcbBlockSizeBits \<in> dom tcb_cte_cases \<and> (\<exists>obj. projectKO_opt (injectKOS val) = Some obj \<and> P (fst (the (tcb_cte_cases (slot && mask tcbBlockSizeBits))) obj))
 2. \<And>s. \<lbrakk>pspace_aligned' s; pspace_distinct' s; is_aligned ptr (objBitsKO (injectKOS val) + us); objBitsKO (injectKOS val) + us < word_bits; pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) s; ko_wp_at' (\<lambda>ko. \<exists>obj. P obj \<and> projectKO_opt ko = Some obj) slot s \<or> slot && mask tcbBlockSizeBits \<in> dom tcb_cte_cases \<and> ko_wp_at' (\<lambda>ko. \<exists>obj. projectKO_opt ko = Some obj \<and> P (fst (the (tcb_cte_cases (slot && mask tcbBlockSizeBits))) obj)) (slot && ~~ mask tcbBlockSizeBits) s; slot && ~~ mask tcbBlockSizeBits \<in> set (new_cap_addrs (2 ^ us) ptr (injectKOS val)); slot \<notin> set (new_cap_addrs (2 ^ us) ptr (injectKOS val))\<rbrakk> \<Longrightarrow> ko_wp_at' (\<lambda>ko. \<exists>obj. P obj \<and> projectKO_opt ko = Some obj) slot s \<or> slot && mask tcbBlockSizeBits \<in> dom tcb_cte_cases \<and> (\<exists>obj. projectKO_opt (injectKOS val) = Some obj \<and> P (fst (the (tcb_cte_cases (slot && mask tcbBlockSizeBits))) obj)) proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>pspace_aligned' s; pspace_distinct' s; is_aligned ptr (objBitsKO (injectKOS val) + us); objBitsKO (injectKOS val) + us < word_bits; pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) s; ko_wp_at' (\<lambda>ko. \<exists>obj. P obj \<and> projectKO_opt ko = Some obj) slot s \<or> slot && mask tcbBlockSizeBits \<in> dom tcb_cte_cases \<and> ko_wp_at' (\<lambda>ko. \<exists>obj. projectKO_opt ko = Some obj \<and> P (fst (the (tcb_cte_cases (slot && mask tcbBlockSizeBits))) obj)) (slot && ~~ mask tcbBlockSizeBits) s; ksPSpace s (slot && ~~ mask tcbBlockSizeBits) = None; ksPSpace s slot = None\<rbrakk> \<Longrightarrow> (\<exists>obj. P obj \<and> projectKO_opt (injectKOS val) = Some obj) \<or> slot && mask tcbBlockSizeBits \<in> dom tcb_cte_cases \<and> (\<exists>obj. projectKO_opt (injectKOS val) = Some obj \<and> P (fst (the (tcb_cte_cases (slot && mask tcbBlockSizeBits))) obj))
 2. \<And>s. \<lbrakk>pspace_aligned' s; pspace_distinct' s; is_aligned ptr (objBitsKO (injectKOS val) + us); objBitsKO (injectKOS val) + us < word_bits; pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) s; ko_wp_at' (\<lambda>ko. \<exists>obj. P obj \<and> projectKO_opt ko = Some obj) slot s \<or> slot && mask tcbBlockSizeBits \<in> dom tcb_cte_cases \<and> ko_wp_at' (\<lambda>ko. \<exists>obj. projectKO_opt ko = Some obj \<and> P (fst (the (tcb_cte_cases (slot && mask tcbBlockSizeBits))) obj)) (slot && ~~ mask tcbBlockSizeBits) s; slot && ~~ mask tcbBlockSizeBits \<in> set (new_cap_addrs (2 ^ us) ptr (injectKOS val)); slot \<notin> set (new_cap_addrs (2 ^ us) ptr (injectKOS val))\<rbrakk> \<Longrightarrow> ko_wp_at' (\<lambda>ko. \<exists>obj. P obj \<and> projectKO_opt ko = Some obj) slot s \<or> slot && mask tcbBlockSizeBits \<in> dom tcb_cte_cases \<and> (\<exists>obj. projectKO_opt (injectKOS val) = Some obj \<and> P (fst (the (tcb_cte_cases (slot && mask tcbBlockSizeBits))) obj)) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>pspace_aligned' s; pspace_distinct' s; is_aligned ptr (objBitsKO (injectKOS val) + us); objBitsKO (injectKOS val) + us < word_bits; pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) s; ko_wp_at' (\<lambda>ko. \<exists>obj. P obj \<and> projectKO_opt ko = Some obj) slot s \<or> slot && mask tcbBlockSizeBits \<in> dom tcb_cte_cases \<and> ko_wp_at' (\<lambda>ko. \<exists>obj. projectKO_opt ko = Some obj \<and> P (fst (the (tcb_cte_cases (slot && mask tcbBlockSizeBits))) obj)) (slot && ~~ mask tcbBlockSizeBits) s; slot && ~~ mask tcbBlockSizeBits \<in> set (new_cap_addrs (2 ^ us) ptr (injectKOS val)); slot \<notin> set (new_cap_addrs (2 ^ us) ptr (injectKOS val))\<rbrakk> \<Longrightarrow> ko_wp_at' (\<lambda>ko. \<exists>obj. P obj \<and> projectKO_opt ko = Some obj) slot s \<or> slot && mask tcbBlockSizeBits \<in> dom tcb_cte_cases \<and> (\<exists>obj. projectKO_opt (injectKOS val) = Some obj \<and> P (fst (the (tcb_cte_cases (slot && mask tcbBlockSizeBits))) obj)) proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>pspace_aligned' s; pspace_distinct' s; is_aligned ptr (objBitsKO (injectKOS val) + us); objBitsKO (injectKOS val) + us < word_bits; pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) s; slot && ~~ mask tcbBlockSizeBits \<in> set (new_cap_addrs (2 ^ us) ptr (injectKOS val)); slot \<notin> set (new_cap_addrs (2 ^ us) ptr (injectKOS val)); ko_wp_at' (\<lambda>ko. \<exists>obj. P obj \<and> projectKO_opt ko = Some obj) slot s\<rbrakk> \<Longrightarrow> ko_wp_at' (\<lambda>ko. \<exists>obj. P obj \<and> projectKO_opt ko = Some obj) slot s \<or> slot && mask tcbBlockSizeBits \<in> dom tcb_cte_cases \<and> (\<exists>obj. projectKO_opt (injectKOS val) = Some obj \<and> P (fst (the (tcb_cte_cases (slot && mask tcbBlockSizeBits))) obj))
 2. \<And>s. \<lbrakk>pspace_aligned' s; pspace_distinct' s; is_aligned ptr (objBitsKO (injectKOS val) + us); objBitsKO (injectKOS val) + us < word_bits; pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) s; slot && ~~ mask tcbBlockSizeBits \<in> set (new_cap_addrs (2 ^ us) ptr (injectKOS val)); slot \<notin> set (new_cap_addrs (2 ^ us) ptr (injectKOS val)); slot && mask tcbBlockSizeBits \<in> dom tcb_cte_cases \<and> ko_wp_at' (\<lambda>ko. \<exists>obj. projectKO_opt ko = Some obj \<and> P (fst (the (tcb_cte_cases (slot && mask tcbBlockSizeBits))) obj)) (slot && ~~ mask tcbBlockSizeBits) s\<rbrakk> \<Longrightarrow> ko_wp_at' (\<lambda>ko. \<exists>obj. P obj \<and> projectKO_opt ko = Some obj) slot s \<or> slot && mask tcbBlockSizeBits \<in> dom tcb_cte_cases \<and> (\<exists>obj. projectKO_opt (injectKOS val) = Some obj \<and> P (fst (the (tcb_cte_cases (slot && mask tcbBlockSizeBits))) obj)) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>pspace_aligned' s; pspace_distinct' s; is_aligned ptr (objBitsKO (injectKOS val) + us); objBitsKO (injectKOS val) + us < word_bits; pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) s; slot && ~~ mask tcbBlockSizeBits \<in> set (new_cap_addrs (2 ^ us) ptr (injectKOS val)); slot \<notin> set (new_cap_addrs (2 ^ us) ptr (injectKOS val)); slot && mask tcbBlockSizeBits \<in> dom tcb_cte_cases \<and> ko_wp_at' (\<lambda>ko. \<exists>obj. projectKO_opt ko = Some obj \<and> P (fst (the (tcb_cte_cases (slot && mask tcbBlockSizeBits))) obj)) (slot && ~~ mask tcbBlockSizeBits) s\<rbrakk> \<Longrightarrow> ko_wp_at' (\<lambda>ko. \<exists>obj. P obj \<and> projectKO_opt ko = Some obj) slot s \<or> slot && mask tcbBlockSizeBits \<in> dom tcb_cte_cases \<and> (\<exists>obj. projectKO_opt (injectKOS val) = Some obj \<and> P (fst (the (tcb_cte_cases (slot && mask tcbBlockSizeBits))) obj)) proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>pspace_aligned' s; pspace_distinct' s; is_aligned ptr (objBitsKO (injectKOS val) + us); objBitsKO (injectKOS val) + us < word_bits; pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) s; slot && ~~ mask tcbBlockSizeBits \<in> set (new_cap_addrs (2 ^ us) ptr (injectKOS val)); slot \<notin> set (new_cap_addrs (2 ^ us) ptr (injectKOS val)); ko_wp_at' (\<lambda>ko. \<exists>obj. projectKO_opt ko = Some obj \<and> P (a obj)) (slot && ~~ mask tcbBlockSizeBits) s; tcb_cte_cases (slot && mask tcbBlockSizeBits) = Some (a, b); \<forall>obj. projectKO_opt (injectKOS val) = Some obj \<longrightarrow> \<not> P (a obj)\<rbrakk> \<Longrightarrow> ko_wp_at' (\<lambda>ko. \<exists>obj. P obj \<and> projectKO_opt ko = Some obj) slot s proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>pspace_aligned' s; pspace_distinct' s; is_aligned ptr (objBitsKO (injectKOS val) + us); objBitsKO (injectKOS val) + us < word_bits; pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) s; slot \<notin> set (new_cap_addrs (2 ^ us) ptr (injectKOS val)); ko_wp_at' (\<lambda>ko. \<exists>obj. projectKO_opt ko = Some obj \<and> P (a obj)) (slot && ~~ mask tcbBlockSizeBits) s; tcb_cte_cases (slot && mask tcbBlockSizeBits) = Some (a, b); \<forall>obj. projectKO_opt (injectKOS val) = Some obj \<longrightarrow> \<not> P (a obj); ksPSpace s (slot && ~~ mask tcbBlockSizeBits) = None\<rbrakk> \<Longrightarrow> ko_wp_at' (\<lambda>ko. \<exists>obj. P obj \<and> projectKO_opt ko = Some obj) slot s proof (prove)
goal:
No subgoals!