theory Retype_R

lemma cte_wp_at_retype':
  assumes ko: "makeObjectKO dev tp = Some obj"
      and pv: "pspace_aligned' s" "pspace_distinct' s"
     and pv': "pspace_aligned' (ksPSpace_update (\<lambda>x xa. if xa \<in> set addrs then Some obj else ksPSpace s xa) s)"
              "pspace_distinct' (ksPSpace_update (\<lambda>x xa. if xa \<in> set addrs then Some obj else ksPSpace s xa) s)"
      and al: "\<forall>x \<in> set addrs. is_aligned x (objBitsKO obj)"
      and pn: "\<forall>x \<in> set addrs. ksPSpace s x = None"
   shows
  "cte_wp_at' P p (ksPSpace_update (\<lambda>x xa. if xa \<in> set addrs then Some obj else ksPSpace s xa) s)
      = (if tp = Inr (APIObjectType ArchTypes_H.CapTableObject) \<and> p \<in> set addrs
           \<or> tp = Inr (APIObjectType ArchTypes_H.TCBObject)
                         \<and> (p && ~~ mask tcbBlockSizeBits \<in> set addrs) \<and> (p && mask tcbBlockSizeBits \<in> dom tcb_cte_cases)
              then P (CTE NullCap nullMDBNode)
              else cte_wp_at' P p s)"
  (is "cte_wp_at' P p ?s' = ?Q") apply (subgoal_tac "\<forall>p \<in> set addrs. \<forall>(P :: cte \<Rightarrow> bool). \<not> obj_at' P p s") apply (subgoal_tac "\<forall>p \<in> set addrs. \<forall>(P :: tcb \<Rightarrow> bool). \<not> obj_at' P p s") apply (subgoal_tac "(\<exists>P :: cte \<Rightarrow> bool. obj_at' P p ?s')
                          \<longrightarrow> (\<not> (\<exists>P :: tcb \<Rightarrow> bool. obj_at' P (p && ~~ mask tcbBlockSizeBits) ?s'))") apply (simp only: cte_wp_at_obj_cases_mask foldr_update_obj_at'[OF pv pv' al]) apply (simp    add: projectKOs the_ctes_makeObject
                         makeObjectKO_eq [OF ko]
                         makeObject_cte dom_def
              split del: if_split
                   cong: if_cong) apply (insert al ko) apply (simp, safe, simp_all) apply fastforce apply fastforce apply (clarsimp elim!: obj_atE' simp: projectKOs objBits_simps) apply (drule ps_clearD[where y=p and n=tcbBlockSizeBits]) apply simp apply (rule order_trans_rules(17)) apply (clarsimp cong: if_cong) apply (rule word_and_le2) apply (rule word_neg_and_le[simplified field_simps]) apply (clarsimp elim!: obj_atE' simp: pn)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cte_wp_at' P p (s\<lparr>ksPSpace := \<lambda>xa. if xa \<in> set addrs then Some obj else ksPSpace s xa\<rparr>) = (if tp = Inr (APIObjectType ArchTypes_H.apiobject_type.CapTableObject) \<and> p \<in> set addrs \<or> tp = Inr (APIObjectType ArchTypes_H.apiobject_type.TCBObject) \<and> p && ~~ mask tcbBlockSizeBits \<in> set addrs \<and> p && mask tcbBlockSizeBits \<in> dom tcb_cte_cases then P (CTE capability.NullCap nullMDBNode) else cte_wp_at' P p s) proof (prove)
goal (2 subgoals):
 1. \<forall>p\<in>set addrs. \<forall>P. \<not> obj_at' P p s \<Longrightarrow> cte_wp_at' P p (s\<lparr>ksPSpace := \<lambda>xa. if xa \<in> set addrs then Some obj else ksPSpace s xa\<rparr>) = (if tp = Inr (APIObjectType ArchTypes_H.apiobject_type.CapTableObject) \<and> p \<in> set addrs \<or> tp = Inr (APIObjectType ArchTypes_H.apiobject_type.TCBObject) \<and> p && ~~ mask tcbBlockSizeBits \<in> set addrs \<and> p && mask tcbBlockSizeBits \<in> dom tcb_cte_cases then P (CTE capability.NullCap nullMDBNode) else cte_wp_at' P p s)
 2. \<forall>p\<in>set addrs. \<forall>P. \<not> obj_at' P p s proof (prove)
goal (3 subgoals):
 1. \<lbrakk>\<forall>p\<in>set addrs. \<forall>P. \<not> obj_at' P p s; \<forall>p\<in>set addrs. \<forall>P. \<not> obj_at' P p s\<rbrakk> \<Longrightarrow> cte_wp_at' P p (s\<lparr>ksPSpace := \<lambda>xa. if xa \<in> set addrs then Some obj else ksPSpace s xa\<rparr>) = (if tp = Inr (APIObjectType ArchTypes_H.apiobject_type.CapTableObject) \<and> p \<in> set addrs \<or> tp = Inr (APIObjectType ArchTypes_H.apiobject_type.TCBObject) \<and> p && ~~ mask tcbBlockSizeBits \<in> set addrs \<and> p && mask tcbBlockSizeBits \<in> dom tcb_cte_cases then P (CTE capability.NullCap nullMDBNode) else cte_wp_at' P p s)
 2. \<forall>p\<in>set addrs. \<forall>P. \<not> obj_at' P p s \<Longrightarrow> \<forall>p\<in>set addrs. \<forall>P. \<not> obj_at' P p s
 3. \<forall>p\<in>set addrs. \<forall>P. \<not> obj_at' P p s proof (prove)
goal (4 subgoals):
 1. \<lbrakk>\<forall>p\<in>set addrs. \<forall>P. \<not> obj_at' P p s; \<forall>p\<in>set addrs. \<forall>P. \<not> obj_at' P p s; (\<exists>P. obj_at' P p (s\<lparr>ksPSpace := \<lambda>xa. if xa \<in> set addrs then Some obj else ksPSpace s xa\<rparr>)) \<longrightarrow> (\<nexists>P. obj_at' P (p && ~~ mask tcbBlockSizeBits) (s\<lparr>ksPSpace := \<lambda>xa. if xa \<in> set addrs then Some obj else ksPSpace s xa\<rparr>))\<rbrakk> \<Longrightarrow> cte_wp_at' P p (s\<lparr>ksPSpace := \<lambda>xa. if xa \<in> set addrs then Some obj else ksPSpace s xa\<rparr>) = (if tp = Inr (APIObjectType ArchTypes_H.apiobject_type.CapTableObject) \<and> p \<in> set addrs \<or> tp = Inr (APIObjectType ArchTypes_H.apiobject_type.TCBObject) \<and> p && ~~ mask tcbBlockSizeBits \<in> set addrs \<and> p && mask tcbBlockSizeBits \<in> dom tcb_cte_cases then P (CTE capability.NullCap nullMDBNode) else cte_wp_at' P p s)
 2. \<lbrakk>\<forall>p\<in>set addrs. \<forall>P. \<not> obj_at' P p s; \<forall>p\<in>set addrs. \<forall>P. \<not> obj_at' P p s\<rbrakk> \<Longrightarrow> (\<exists>P. obj_at' P p (s\<lparr>ksPSpace := \<lambda>xa. if xa \<in> set addrs then Some obj else ksPSpace s xa\<rparr>)) \<longrightarrow> (\<nexists>P. obj_at' P (p && ~~ mask tcbBlockSizeBits) (s\<lparr>ksPSpace := \<lambda>xa. if xa \<in> set addrs then Some obj else ksPSpace s xa\<rparr>))
 3. \<forall>p\<in>set addrs. \<forall>P. \<not> obj_at' P p s \<Longrightarrow> \<forall>p\<in>set addrs. \<forall>P. \<not> obj_at' P p s
 4. \<forall>p\<in>set addrs. \<forall>P. \<not> obj_at' P p s proof (prove)
goal (4 subgoals):
 1. \<lbrakk>\<forall>p\<in>set addrs. \<forall>P. \<not> obj_at' P p s; \<forall>p\<in>set addrs. \<forall>P. \<not> obj_at' P p s; (\<exists>P. if p \<in> set addrs then \<exists>obj'. projectKO_opt obj = Some obj' \<and> P obj' else obj_at' P p s) \<longrightarrow> (\<nexists>P. if p && ~~ mask tcbBlockSizeBits \<in> set addrs then \<exists>obj'. projectKO_opt obj = Some obj' \<and> P obj' else obj_at' P (p && ~~ mask tcbBlockSizeBits) s)\<rbrakk> \<Longrightarrow> ((if p \<in> set addrs then \<exists>obj'. projectKO_opt obj = Some obj' \<and> P obj' else obj_at' P p s) \<or> p && mask tcbBlockSizeBits \<in> dom tcb_cte_cases \<and> (if p && ~~ mask tcbBlockSizeBits \<in> set addrs then \<exists>obj'. projectKO_opt obj = Some obj' \<and> (P \<circ> fst (the (tcb_cte_cases (p && mask tcbBlockSizeBits)))) obj' else obj_at' (P \<circ> fst (the (tcb_cte_cases (p && mask tcbBlockSizeBits)))) (p && ~~ mask tcbBlockSizeBits) s)) = (if tp = Inr (APIObjectType ArchTypes_H.apiobject_type.CapTableObject) \<and> p \<in> set addrs \<or> tp = Inr (APIObjectType ArchTypes_H.apiobject_type.TCBObject) \<and> p && ~~ mask tcbBlockSizeBits \<in> set addrs \<and> p && mask tcbBlockSizeBits \<in> dom tcb_cte_cases then P (CTE capability.NullCap nullMDBNode) else obj_at' P p s \<or> p && mask tcbBlockSizeBits \<in> dom tcb_cte_cases \<and> obj_at' (P \<circ> fst (the (tcb_cte_cases (p && mask tcbBlockSizeBits)))) (p && ~~ mask tcbBlockSizeBits) s)
 2. \<lbrakk>\<forall>p\<in>set addrs. \<forall>P. \<not> obj_at' P p s; \<forall>p\<in>set addrs. \<forall>P. \<not> obj_at' P p s\<rbrakk> \<Longrightarrow> (\<exists>P. obj_at' P p (s\<lparr>ksPSpace := \<lambda>xa. if xa \<in> set addrs then Some obj else ksPSpace s xa\<rparr>)) \<longrightarrow> (\<nexists>P. obj_at' P (p && ~~ mask tcbBlockSizeBits) (s\<lparr>ksPSpace := \<lambda>xa. if xa \<in> set addrs then Some obj else ksPSpace s xa\<rparr>))
 3. \<forall>p\<in>set addrs. \<forall>P. \<not> obj_at' P p s \<Longrightarrow> \<forall>p\<in>set addrs. \<forall>P. \<not> obj_at' P p s
 4. \<forall>p\<in>set addrs. \<forall>P. \<not> obj_at' P p s proof (prove)
goal (4 subgoals):
 1. \<lbrakk>\<forall>p\<in>set addrs. \<forall>P. \<not> obj_at' P p s; \<forall>p\<in>set addrs. \<forall>P. \<not> obj_at' P p s; (\<exists>P. if p \<in> set addrs then tp = Inr (APIObjectType ArchTypes_H.apiobject_type.CapTableObject) \<and> P (CTE capability.NullCap nullMDBNode) else obj_at' P p s) \<longrightarrow> (\<forall>P. \<not> (if p && ~~ mask tcbBlockSizeBits \<in> set addrs then tp = Inr (APIObjectType ArchTypes_H.apiobject_type.TCBObject) \<and> P makeObject else obj_at' P (p && ~~ mask tcbBlockSizeBits) s))\<rbrakk> \<Longrightarrow> ((if p \<in> set addrs then tp = Inr (APIObjectType ArchTypes_H.apiobject_type.CapTableObject) \<and> P (CTE capability.NullCap nullMDBNode) else obj_at' P p s) \<or> (\<exists>a b. tcb_cte_cases (p && mask tcbBlockSizeBits) = Some (a, b)) \<and> (if p && ~~ mask tcbBlockSizeBits \<in> set addrs then tp = Inr (APIObjectType ArchTypes_H.apiobject_type.TCBObject) \<and> P (if tcb_cte_cases (p && mask tcbBlockSizeBits) = None then fst (the None) makeObject else CTE capability.NullCap nullMDBNode) else obj_at' (P \<circ> fst (the (tcb_cte_cases (p && mask tcbBlockSizeBits)))) (p && ~~ mask tcbBlockSizeBits) s)) = (if tp = Inr (APIObjectType ArchTypes_H.apiobject_type.CapTableObject) \<and> p \<in> set addrs \<or> tp = Inr (APIObjectType ArchTypes_H.apiobject_type.TCBObject) \<and> p && ~~ mask tcbBlockSizeBits \<in> set addrs \<and> (\<exists>a b. tcb_cte_cases (p && mask tcbBlockSizeBits) = Some (a, b)) then P (CTE capability.NullCap nullMDBNode) else obj_at' P p s \<or> (\<exists>a b. tcb_cte_cases (p && mask tcbBlockSizeBits) = Some (a, b)) \<and> obj_at' (P \<circ> fst (the (tcb_cte_cases (p && mask tcbBlockSizeBits)))) (p && ~~ mask tcbBlockSizeBits) s)
 2. \<lbrakk>\<forall>p\<in>set addrs. \<forall>P. \<not> obj_at' P p s; \<forall>p\<in>set addrs. \<forall>P. \<not> obj_at' P p s\<rbrakk> \<Longrightarrow> (\<exists>P. obj_at' P p (s\<lparr>ksPSpace := \<lambda>xa. if xa \<in> set addrs then Some obj else ksPSpace s xa\<rparr>)) \<longrightarrow> (\<nexists>P. obj_at' P (p && ~~ mask tcbBlockSizeBits) (s\<lparr>ksPSpace := \<lambda>xa. if xa \<in> set addrs then Some obj else ksPSpace s xa\<rparr>))
 3. \<forall>p\<in>set addrs. \<forall>P. \<not> obj_at' P p s \<Longrightarrow> \<forall>p\<in>set addrs. \<forall>P. \<not> obj_at' P p s
 4. \<forall>p\<in>set addrs. \<forall>P. \<not> obj_at' P p s proof (prove)
goal (4 subgoals):
 1. \<lbrakk>\<forall>p\<in>set addrs. \<forall>P. \<not> obj_at' P p s; \<forall>p\<in>set addrs. \<forall>P. \<not> obj_at' P p s; (\<exists>P. if p \<in> set addrs then tp = Inr (APIObjectType ArchTypes_H.apiobject_type.CapTableObject) \<and> P (CTE capability.NullCap nullMDBNode) else obj_at' P p s) \<longrightarrow> (\<forall>P. \<not> (if p && ~~ mask tcbBlockSizeBits \<in> set addrs then tp = Inr (APIObjectType ArchTypes_H.apiobject_type.TCBObject) \<and> P makeObject else obj_at' P (p && ~~ mask tcbBlockSizeBits) s)); \<forall>x\<in>set addrs. is_aligned x (objBitsKO obj); makeObjectKO dev tp = Some obj\<rbrakk> \<Longrightarrow> ((if p \<in> set addrs then tp = Inr (APIObjectType ArchTypes_H.apiobject_type.CapTableObject) \<and> P (CTE capability.NullCap nullMDBNode) else obj_at' P p s) \<or> (\<exists>a b. tcb_cte_cases (p && mask tcbBlockSizeBits) = Some (a, b)) \<and> (if p && ~~ mask tcbBlockSizeBits \<in> set addrs then tp = Inr (APIObjectType ArchTypes_H.apiobject_type.TCBObject) \<and> P (if tcb_cte_cases (p && mask tcbBlockSizeBits) = None then fst (the None) makeObject else CTE capability.NullCap nullMDBNode) else obj_at' (P \<circ> fst (the (tcb_cte_cases (p && mask tcbBlockSizeBits)))) (p && ~~ mask tcbBlockSizeBits) s)) = (if tp = Inr (APIObjectType ArchTypes_H.apiobject_type.CapTableObject) \<and> p \<in> set addrs \<or> tp = Inr (APIObjectType ArchTypes_H.apiobject_type.TCBObject) \<and> p && ~~ mask tcbBlockSizeBits \<in> set addrs \<and> (\<exists>a b. tcb_cte_cases (p && mask tcbBlockSizeBits) = Some (a, b)) then P (CTE capability.NullCap nullMDBNode) else obj_at' P p s \<or> (\<exists>a b. tcb_cte_cases (p && mask tcbBlockSizeBits) = Some (a, b)) \<and> obj_at' (P \<circ> fst (the (tcb_cte_cases (p && mask tcbBlockSizeBits)))) (p && ~~ mask tcbBlockSizeBits) s)
 2. \<lbrakk>\<forall>p\<in>set addrs. \<forall>P. \<not> obj_at' P p s; \<forall>p\<in>set addrs. \<forall>P. \<not> obj_at' P p s; \<forall>x\<in>set addrs. is_aligned x (objBitsKO obj); makeObjectKO dev tp = Some obj\<rbrakk> \<Longrightarrow> (\<exists>P. obj_at' P p (s\<lparr>ksPSpace := \<lambda>xa. if xa \<in> set addrs then Some obj else ksPSpace s xa\<rparr>)) \<longrightarrow> (\<nexists>P. obj_at' P (p && ~~ mask tcbBlockSizeBits) (s\<lparr>ksPSpace := \<lambda>xa. if xa \<in> set addrs then Some obj else ksPSpace s xa\<rparr>))
 3. \<lbrakk>\<forall>p\<in>set addrs. \<forall>P. \<not> obj_at' P p s; \<forall>x\<in>set addrs. is_aligned x (objBitsKO obj); makeObjectKO dev tp = Some obj\<rbrakk> \<Longrightarrow> \<forall>p\<in>set addrs. \<forall>P. \<not> obj_at' P p s
 4. \<lbrakk>\<forall>x\<in>set addrs. is_aligned x (objBitsKO obj); makeObjectKO dev tp = Some obj\<rbrakk> \<Longrightarrow> \<forall>p\<in>set addrs. \<forall>P. \<not> obj_at' P p s proof (prove)
goal (5 subgoals):
 1. \<And>a b. \<lbrakk>\<forall>p\<in>set addrs. \<forall>P. \<not> obj_at' P p s; \<forall>p\<in>set addrs. \<forall>P. \<not> obj_at' P p s; \<forall>x\<in>set addrs. is_aligned x (objBitsKO obj); makeObjectKO dev (Inr (APIObjectType ArchTypes_H.apiobject_type.CapTableObject)) = Some obj; tcb_cte_cases (p && mask tcbBlockSizeBits) = Some (a, b); \<forall>P. \<not> P (CTE capability.NullCap nullMDBNode); p && ~~ mask tcbBlockSizeBits \<notin> set addrs; p \<in> set addrs; tp = Inr (APIObjectType ArchTypes_H.apiobject_type.CapTableObject); obj_at' (P \<circ> a) (p && ~~ mask tcbBlockSizeBits) s\<rbrakk> \<Longrightarrow> P (CTE capability.NullCap nullMDBNode)
 2. \<And>a b. \<lbrakk>\<forall>p\<in>set addrs. \<forall>P. \<not> obj_at' P p s; \<forall>p\<in>set addrs. \<forall>P. \<not> obj_at' P p s; \<forall>x\<in>set addrs. is_aligned x (objBitsKO obj); makeObjectKO dev (Inr (APIObjectType ArchTypes_H.apiobject_type.TCBObject)) = Some obj; tcb_cte_cases (p && mask tcbBlockSizeBits) = Some (a, b); \<forall>P. \<not> P makeObject; p && ~~ mask tcbBlockSizeBits \<in> set addrs; p \<notin> set addrs; tp = Inr (APIObjectType ArchTypes_H.apiobject_type.TCBObject); obj_at' P p s\<rbrakk> \<Longrightarrow> P (CTE capability.NullCap nullMDBNode)
 3. \<And>P Pa. \<lbrakk>\<forall>p\<in>set addrs. \<forall>P. \<not> obj_at' P p s; \<forall>p\<in>set addrs. \<forall>P. \<not> obj_at' P p s; \<forall>x\<in>set addrs. is_aligned x (objBitsKO obj); makeObjectKO dev tp = Some obj; obj_at' P p (s\<lparr>ksPSpace := \<lambda>xa. if xa \<in> set addrs then Some obj else ksPSpace s xa\<rparr>); obj_at' Pa (p && ~~ mask tcbBlockSizeBits) (s\<lparr>ksPSpace := \<lambda>xa. if xa \<in> set addrs then Some obj else ksPSpace s xa\<rparr>)\<rbrakk> \<Longrightarrow> False
 4. \<And>p P. \<lbrakk>\<forall>p\<in>set addrs. \<forall>P. \<not> obj_at' P p s; \<forall>x\<in>set addrs. is_aligned x (objBitsKO obj); makeObjectKO dev tp = Some obj; p \<in> set addrs; obj_at' P p s\<rbrakk> \<Longrightarrow> False
 5. \<And>p P. \<lbrakk>\<forall>x\<in>set addrs. is_aligned x (objBitsKO obj); makeObjectKO dev tp = Some obj; p \<in> set addrs; obj_at' P p s\<rbrakk> \<Longrightarrow> False proof (prove)
goal (4 subgoals):
 1. \<And>a b. \<lbrakk>\<forall>p\<in>set addrs. \<forall>P. \<not> obj_at' P p s; \<forall>p\<in>set addrs. \<forall>P. \<not> obj_at' P p s; \<forall>x\<in>set addrs. is_aligned x (objBitsKO obj); makeObjectKO dev (Inr (APIObjectType ArchTypes_H.apiobject_type.TCBObject)) = Some obj; tcb_cte_cases (p && mask tcbBlockSizeBits) = Some (a, b); \<forall>P. \<not> P makeObject; p && ~~ mask tcbBlockSizeBits \<in> set addrs; p \<notin> set addrs; tp = Inr (APIObjectType ArchTypes_H.apiobject_type.TCBObject); obj_at' P p s\<rbrakk> \<Longrightarrow> P (CTE capability.NullCap nullMDBNode)
 2. \<And>P Pa. \<lbrakk>\<forall>p\<in>set addrs. \<forall>P. \<not> obj_at' P p s; \<forall>p\<in>set addrs. \<forall>P. \<not> obj_at' P p s; \<forall>x\<in>set addrs. is_aligned x (objBitsKO obj); makeObjectKO dev tp = Some obj; obj_at' P p (s\<lparr>ksPSpace := \<lambda>xa. if xa \<in> set addrs then Some obj else ksPSpace s xa\<rparr>); obj_at' Pa (p && ~~ mask tcbBlockSizeBits) (s\<lparr>ksPSpace := \<lambda>xa. if xa \<in> set addrs then Some obj else ksPSpace s xa\<rparr>)\<rbrakk> \<Longrightarrow> False
 3. \<And>p P. \<lbrakk>\<forall>p\<in>set addrs. \<forall>P. \<not> obj_at' P p s; \<forall>x\<in>set addrs. is_aligned x (objBitsKO obj); makeObjectKO dev tp = Some obj; p \<in> set addrs; obj_at' P p s\<rbrakk> \<Longrightarrow> False
 4. \<And>p P. \<lbrakk>\<forall>x\<in>set addrs. is_aligned x (objBitsKO obj); makeObjectKO dev tp = Some obj; p \<in> set addrs; obj_at' P p s\<rbrakk> \<Longrightarrow> False proof (prove)
goal (3 subgoals):
 1. \<And>P Pa. \<lbrakk>\<forall>p\<in>set addrs. \<forall>P. \<not> obj_at' P p s; \<forall>p\<in>set addrs. \<forall>P. \<not> obj_at' P p s; \<forall>x\<in>set addrs. is_aligned x (objBitsKO obj); makeObjectKO dev tp = Some obj; obj_at' P p (s\<lparr>ksPSpace := \<lambda>xa. if xa \<in> set addrs then Some obj else ksPSpace s xa\<rparr>); obj_at' Pa (p && ~~ mask tcbBlockSizeBits) (s\<lparr>ksPSpace := \<lambda>xa. if xa \<in> set addrs then Some obj else ksPSpace s xa\<rparr>)\<rbrakk> \<Longrightarrow> False
 2. \<And>p P. \<lbrakk>\<forall>p\<in>set addrs. \<forall>P. \<not> obj_at' P p s; \<forall>x\<in>set addrs. is_aligned x (objBitsKO obj); makeObjectKO dev tp = Some obj; p \<in> set addrs; obj_at' P p s\<rbrakk> \<Longrightarrow> False
 3. \<And>p P. \<lbrakk>\<forall>x\<in>set addrs. is_aligned x (objBitsKO obj); makeObjectKO dev tp = Some obj; p \<in> set addrs; obj_at' P p s\<rbrakk> \<Longrightarrow> False proof (prove)
goal (3 subgoals):
 1. \<And>P Pa obja objaa. \<lbrakk>\<forall>p\<in>set addrs. \<forall>P. \<not> obj_at' P p s; \<forall>p\<in>set addrs. \<forall>P. \<not> obj_at' P p s; \<forall>x\<in>set addrs. is_aligned x (case obj of KOEndpoint x \<Rightarrow> epSizeBits | KONotification x \<Rightarrow> ntfnSizeBits | KOTCB x \<Rightarrow> tcbBlockSizeBits | KOCTE x \<Rightarrow> cteSizeBits | KOArch x \<Rightarrow> archObjSize x | _ \<Rightarrow> pageBits); makeObjectKO dev tp = Some obj; (if p \<in> set addrs then Some obj else ksPSpace s p) = Some (KOCTE obja); is_aligned p cteSizeBits; P obja; ps_clear p cteSizeBits (s\<lparr>ksPSpace := \<lambda>xa. if xa \<in> set addrs then Some obj else ksPSpace s xa\<rparr>); (if p && ~~ mask tcbBlockSizeBits \<in> set addrs then Some obj else ksPSpace s (p && ~~ mask tcbBlockSizeBits)) = Some (KOTCB objaa); Pa objaa; ps_clear (p && ~~ mask tcbBlockSizeBits) tcbBlockSizeBits (s\<lparr>ksPSpace := \<lambda>xa. if xa \<in> set addrs then Some obj else ksPSpace s xa\<rparr>)\<rbrakk> \<Longrightarrow> False
 2. \<And>p P. \<lbrakk>\<forall>p\<in>set addrs. \<forall>P. \<not> obj_at' P p s; \<forall>x\<in>set addrs. is_aligned x (objBitsKO obj); makeObjectKO dev tp = Some obj; p \<in> set addrs; obj_at' P p s\<rbrakk> \<Longrightarrow> False
 3. \<And>p P. \<lbrakk>\<forall>x\<in>set addrs. is_aligned x (objBitsKO obj); makeObjectKO dev tp = Some obj; p \<in> set addrs; obj_at' P p s\<rbrakk> \<Longrightarrow> False proof (prove)
goal (6 subgoals):
 1. \<And>P Pa obja objaa. \<lbrakk>\<forall>p\<in>set addrs. \<forall>P. \<not> obj_at' P p s; \<forall>p\<in>set addrs. \<forall>P. \<not> obj_at' P p s; \<forall>x\<in>set addrs. is_aligned x (case obj of KOEndpoint x \<Rightarrow> epSizeBits | KONotification x \<Rightarrow> ntfnSizeBits | KOTCB x \<Rightarrow> tcbBlockSizeBits | KOCTE x \<Rightarrow> cteSizeBits | KOArch x \<Rightarrow> archObjSize x | _ \<Rightarrow> pageBits); makeObjectKO dev tp = Some obj; (if p \<in> set addrs then Some obj else ksPSpace s p) = Some (KOCTE obja); is_aligned p cteSizeBits; P obja; ps_clear p cteSizeBits (s\<lparr>ksPSpace := \<lambda>xa. if xa \<in> set addrs then Some obj else ksPSpace s xa\<rparr>); (if p && ~~ mask tcbBlockSizeBits \<in> set addrs then Some obj else ksPSpace s (p && ~~ mask tcbBlockSizeBits)) = Some (KOTCB objaa); Pa objaa\<rbrakk> \<Longrightarrow> ksPSpace (s\<lparr>ksPSpace := \<lambda>xa. if xa \<in> set addrs then Some obj else ksPSpace s xa\<rparr>) p = Some (?v129 P Pa obja objaa)
 2. \<And>P Pa obja objaa. \<lbrakk>\<forall>p\<in>set addrs. \<forall>P. \<not> obj_at' P p s; \<forall>p\<in>set addrs. \<forall>P. \<not> obj_at' P p s; \<forall>x\<in>set addrs. is_aligned x (case obj of KOEndpoint x \<Rightarrow> epSizeBits | KONotification x \<Rightarrow> ntfnSizeBits | KOTCB x \<Rightarrow> tcbBlockSizeBits | KOCTE x \<Rightarrow> cteSizeBits | KOArch x \<Rightarrow> archObjSize x | _ \<Rightarrow> pageBits); makeObjectKO dev tp = Some obj; (if p \<in> set addrs then Some obj else ksPSpace s p) = Some (KOCTE obja); is_aligned p cteSizeBits; P obja; ps_clear p cteSizeBits (s\<lparr>ksPSpace := \<lambda>xa. if xa \<in> set addrs then Some obj else ksPSpace s xa\<rparr>); (if p && ~~ mask tcbBlockSizeBits \<in> set addrs then Some obj else ksPSpace s (p && ~~ mask tcbBlockSizeBits)) = Some (KOTCB objaa); Pa objaa\<rbrakk> \<Longrightarrow> p && ~~ mask tcbBlockSizeBits < p
 3. \<And>P Pa obja objaa. \<lbrakk>\<forall>p\<in>set addrs. \<forall>P. \<not> obj_at' P p s; \<forall>p\<in>set addrs. \<forall>P. \<not> obj_at' P p s; \<forall>x\<in>set addrs. is_aligned x (case obj of KOEndpoint x \<Rightarrow> epSizeBits | KONotification x \<Rightarrow> ntfnSizeBits | KOTCB x \<Rightarrow> tcbBlockSizeBits | KOCTE x \<Rightarrow> cteSizeBits | KOArch x \<Rightarrow> archObjSize x | _ \<Rightarrow> pageBits); makeObjectKO dev tp = Some obj; (if p \<in> set addrs then Some obj else ksPSpace s p) = Some (KOCTE obja); is_aligned p cteSizeBits; P obja; ps_clear p cteSizeBits (s\<lparr>ksPSpace := \<lambda>xa. if xa \<in> set addrs then Some obj else ksPSpace s xa\<rparr>); (if p && ~~ mask tcbBlockSizeBits \<in> set addrs then Some obj else ksPSpace s (p && ~~ mask tcbBlockSizeBits)) = Some (KOTCB objaa); Pa objaa\<rbrakk> \<Longrightarrow> p \<le> (p && ~~ mask tcbBlockSizeBits) + 2 ^ tcbBlockSizeBits - 1
 4. \<And>P Pa obja objaa. \<lbrakk>\<forall>p\<in>set addrs. \<forall>P. \<not> obj_at' P p s; \<forall>p\<in>set addrs. \<forall>P. \<not> obj_at' P p s; \<forall>x\<in>set addrs. is_aligned x (case obj of KOEndpoint x \<Rightarrow> epSizeBits | KONotification x \<Rightarrow> ntfnSizeBits | KOTCB x \<Rightarrow> tcbBlockSizeBits | KOCTE x \<Rightarrow> cteSizeBits | KOArch x \<Rightarrow> archObjSize x | _ \<Rightarrow> pageBits); makeObjectKO dev tp = Some obj; (if p \<in> set addrs then Some obj else ksPSpace s p) = Some (KOCTE obja); is_aligned p cteSizeBits; P obja; ps_clear p cteSizeBits (s\<lparr>ksPSpace := \<lambda>xa. if xa \<in> set addrs then Some obj else ksPSpace s xa\<rparr>); (if p && ~~ mask tcbBlockSizeBits \<in> set addrs then Some obj else ksPSpace s (p && ~~ mask tcbBlockSizeBits)) = Some (KOTCB objaa); Pa objaa; False\<rbrakk> \<Longrightarrow> False
 5. \<And>p P. \<lbrakk>\<forall>p\<in>set addrs. \<forall>P. \<not> obj_at' P p s; \<forall>x\<in>set addrs. is_aligned x (objBitsKO obj); makeObjectKO dev tp = Some obj; p \<in> set addrs; obj_at' P p s\<rbrakk> \<Longrightarrow> False
 6. \<And>p P. \<lbrakk>\<forall>x\<in>set addrs. is_aligned x (objBitsKO obj); makeObjectKO dev tp = Some obj; p \<in> set addrs; obj_at' P p s\<rbrakk> \<Longrightarrow> False proof (prove)
goal (5 subgoals):
 1. \<And>P Pa obja objaa. \<lbrakk>\<forall>p\<in>set addrs. \<forall>P. \<not> obj_at' P p s; \<forall>p\<in>set addrs. \<forall>P. \<not> obj_at' P p s; \<forall>x\<in>set addrs. is_aligned x (case obj of KOEndpoint x \<Rightarrow> epSizeBits | KONotification x \<Rightarrow> ntfnSizeBits | KOTCB x \<Rightarrow> tcbBlockSizeBits | KOCTE x \<Rightarrow> cteSizeBits | KOArch x \<Rightarrow> archObjSize x | _ \<Rightarrow> pageBits); makeObjectKO dev tp = Some obj; (if p \<in> set addrs then Some obj else ksPSpace s p) = Some (KOCTE obja); is_aligned p cteSizeBits; P obja; ps_clear p cteSizeBits (s\<lparr>ksPSpace := \<lambda>xa. if xa \<in> set addrs then Some obj else ksPSpace s xa\<rparr>); (if p && ~~ mask tcbBlockSizeBits \<in> set addrs then Some obj else ksPSpace s (p && ~~ mask tcbBlockSizeBits)) = Some (KOTCB objaa); Pa objaa\<rbrakk> \<Longrightarrow> p && ~~ mask tcbBlockSizeBits < p
 2. \<And>P Pa obja objaa. \<lbrakk>\<forall>p\<in>set addrs. \<forall>P. \<not> obj_at' P p s; \<forall>p\<in>set addrs. \<forall>P. \<not> obj_at' P p s; \<forall>x\<in>set addrs. is_aligned x (case obj of KOEndpoint x \<Rightarrow> epSizeBits | KONotification x \<Rightarrow> ntfnSizeBits | KOTCB x \<Rightarrow> tcbBlockSizeBits | KOCTE x \<Rightarrow> cteSizeBits | KOArch x \<Rightarrow> archObjSize x | _ \<Rightarrow> pageBits); makeObjectKO dev tp = Some obj; (if p \<in> set addrs then Some obj else ksPSpace s p) = Some (KOCTE obja); is_aligned p cteSizeBits; P obja; ps_clear p cteSizeBits (s\<lparr>ksPSpace := \<lambda>xa. if xa \<in> set addrs then Some obj else ksPSpace s xa\<rparr>); (if p && ~~ mask tcbBlockSizeBits \<in> set addrs then Some obj else ksPSpace s (p && ~~ mask tcbBlockSizeBits)) = Some (KOTCB objaa); Pa objaa\<rbrakk> \<Longrightarrow> p \<le> (p && ~~ mask tcbBlockSizeBits) + 2 ^ tcbBlockSizeBits - 1
 3. \<And>P Pa obja objaa. \<lbrakk>\<forall>p\<in>set addrs. \<forall>P. \<not> obj_at' P p s; \<forall>p\<in>set addrs. \<forall>P. \<not> obj_at' P p s; \<forall>x\<in>set addrs. is_aligned x (case obj of KOEndpoint x \<Rightarrow> epSizeBits | KONotification x \<Rightarrow> ntfnSizeBits | KOTCB x \<Rightarrow> tcbBlockSizeBits | KOCTE x \<Rightarrow> cteSizeBits | KOArch x \<Rightarrow> archObjSize x | _ \<Rightarrow> pageBits); makeObjectKO dev tp = Some obj; (if p \<in> set addrs then Some obj else ksPSpace s p) = Some (KOCTE obja); is_aligned p cteSizeBits; P obja; ps_clear p cteSizeBits (s\<lparr>ksPSpace := \<lambda>xa. if xa \<in> set addrs then Some obj else ksPSpace s xa\<rparr>); (if p && ~~ mask tcbBlockSizeBits \<in> set addrs then Some obj else ksPSpace s (p && ~~ mask tcbBlockSizeBits)) = Some (KOTCB objaa); Pa objaa; False\<rbrakk> \<Longrightarrow> False
 4. \<And>p P. \<lbrakk>\<forall>p\<in>set addrs. \<forall>P. \<not> obj_at' P p s; \<forall>x\<in>set addrs. is_aligned x (objBitsKO obj); makeObjectKO dev tp = Some obj; p \<in> set addrs; obj_at' P p s\<rbrakk> \<Longrightarrow> False
 5. \<And>p P. \<lbrakk>\<forall>x\<in>set addrs. is_aligned x (objBitsKO obj); makeObjectKO dev tp = Some obj; p \<in> set addrs; obj_at' P p s\<rbrakk> \<Longrightarrow> False proof (prove)
goal (6 subgoals):
 1. \<And>P Pa obja objaa. \<lbrakk>\<forall>p\<in>set addrs. \<forall>P. \<not> obj_at' P p s; \<forall>p\<in>set addrs. \<forall>P. \<not> obj_at' P p s; \<forall>x\<in>set addrs. is_aligned x (case obj of KOEndpoint x \<Rightarrow> epSizeBits | KONotification x \<Rightarrow> ntfnSizeBits | KOTCB x \<Rightarrow> tcbBlockSizeBits | KOCTE x \<Rightarrow> cteSizeBits | KOArch x \<Rightarrow> archObjSize x | _ \<Rightarrow> pageBits); makeObjectKO dev tp = Some obj; (if p \<in> set addrs then Some obj else ksPSpace s p) = Some (KOCTE obja); is_aligned p cteSizeBits; P obja; ps_clear p cteSizeBits (s\<lparr>ksPSpace := \<lambda>xa. if xa \<in> set addrs then Some obj else ksPSpace s xa\<rparr>); (if p && ~~ mask tcbBlockSizeBits \<in> set addrs then Some obj else ksPSpace s (p && ~~ mask tcbBlockSizeBits)) = Some (KOTCB objaa); Pa objaa\<rbrakk> \<Longrightarrow> p && ~~ mask tcbBlockSizeBits \<noteq> p
 2. \<And>P Pa obja objaa. \<lbrakk>\<forall>p\<in>set addrs. \<forall>P. \<not> obj_at' P p s; \<forall>p\<in>set addrs. \<forall>P. \<not> obj_at' P p s; \<forall>x\<in>set addrs. is_aligned x (case obj of KOEndpoint x \<Rightarrow> epSizeBits | KONotification x \<Rightarrow> ntfnSizeBits | KOTCB x \<Rightarrow> tcbBlockSizeBits | KOCTE x \<Rightarrow> cteSizeBits | KOArch x \<Rightarrow> archObjSize x | _ \<Rightarrow> pageBits); makeObjectKO dev tp = Some obj; (if p \<in> set addrs then Some obj else ksPSpace s p) = Some (KOCTE obja); is_aligned p cteSizeBits; P obja; ps_clear p cteSizeBits (s\<lparr>ksPSpace := \<lambda>xa. if xa \<in> set addrs then Some obj else ksPSpace s xa\<rparr>); (if p && ~~ mask tcbBlockSizeBits \<in> set addrs then Some obj else ksPSpace s (p && ~~ mask tcbBlockSizeBits)) = Some (KOTCB objaa); Pa objaa\<rbrakk> \<Longrightarrow> p && ~~ mask tcbBlockSizeBits \<le> p
 3. \<And>P Pa obja objaa. \<lbrakk>\<forall>p\<in>set addrs. \<forall>P. \<not> obj_at' P p s; \<forall>p\<in>set addrs. \<forall>P. \<not> obj_at' P p s; \<forall>x\<in>set addrs. is_aligned x (case obj of KOEndpoint x \<Rightarrow> epSizeBits | KONotification x \<Rightarrow> ntfnSizeBits | KOTCB x \<Rightarrow> tcbBlockSizeBits | KOCTE x \<Rightarrow> cteSizeBits | KOArch x \<Rightarrow> archObjSize x | _ \<Rightarrow> pageBits); makeObjectKO dev tp = Some obj; (if p \<in> set addrs then Some obj else ksPSpace s p) = Some (KOCTE obja); is_aligned p cteSizeBits; P obja; ps_clear p cteSizeBits (s\<lparr>ksPSpace := \<lambda>xa. if xa \<in> set addrs then Some obj else ksPSpace s xa\<rparr>); (if p && ~~ mask tcbBlockSizeBits \<in> set addrs then Some obj else ksPSpace s (p && ~~ mask tcbBlockSizeBits)) = Some (KOTCB objaa); Pa objaa\<rbrakk> \<Longrightarrow> p \<le> (p && ~~ mask tcbBlockSizeBits) + 2 ^ tcbBlockSizeBits - 1
 4. \<And>P Pa obja objaa. \<lbrakk>\<forall>p\<in>set addrs. \<forall>P. \<not> obj_at' P p s; \<forall>p\<in>set addrs. \<forall>P. \<not> obj_at' P p s; \<forall>x\<in>set addrs. is_aligned x (case obj of KOEndpoint x \<Rightarrow> epSizeBits | KONotification x \<Rightarrow> ntfnSizeBits | KOTCB x \<Rightarrow> tcbBlockSizeBits | KOCTE x \<Rightarrow> cteSizeBits | KOArch x \<Rightarrow> archObjSize x | _ \<Rightarrow> pageBits); makeObjectKO dev tp = Some obj; (if p \<in> set addrs then Some obj else ksPSpace s p) = Some (KOCTE obja); is_aligned p cteSizeBits; P obja; ps_clear p cteSizeBits (s\<lparr>ksPSpace := \<lambda>xa. if xa \<in> set addrs then Some obj else ksPSpace s xa\<rparr>); (if p && ~~ mask tcbBlockSizeBits \<in> set addrs then Some obj else ksPSpace s (p && ~~ mask tcbBlockSizeBits)) = Some (KOTCB objaa); Pa objaa; False\<rbrakk> \<Longrightarrow> False
 5. \<And>p P. \<lbrakk>\<forall>p\<in>set addrs. \<forall>P. \<not> obj_at' P p s; \<forall>x\<in>set addrs. is_aligned x (objBitsKO obj); makeObjectKO dev tp = Some obj; p \<in> set addrs; obj_at' P p s\<rbrakk> \<Longrightarrow> False
 6. \<And>p P. \<lbrakk>\<forall>x\<in>set addrs. is_aligned x (objBitsKO obj); makeObjectKO dev tp = Some obj; p \<in> set addrs; obj_at' P p s\<rbrakk> \<Longrightarrow> False proof (prove)
goal (5 subgoals):
 1. \<And>P Pa obja objaa. \<lbrakk>\<forall>p\<in>set addrs. \<forall>P. \<not> obj_at' P p s; \<forall>p\<in>set addrs. \<forall>P. \<not> obj_at' P p s; \<forall>x\<in>set addrs. is_aligned x (case obj of KOEndpoint x \<Rightarrow> epSizeBits | KONotification x \<Rightarrow> ntfnSizeBits | KOTCB x \<Rightarrow> tcbBlockSizeBits | KOCTE x \<Rightarrow> cteSizeBits | KOArch x \<Rightarrow> archObjSize x | _ \<Rightarrow> pageBits); makeObjectKO dev tp = Some obj; (if p \<in> set addrs then Some obj else ksPSpace s p) = Some (KOCTE obja); is_aligned p cteSizeBits; P obja; ps_clear p cteSizeBits (s\<lparr>ksPSpace := \<lambda>xa. if xa \<in> set addrs then Some obj else ksPSpace s xa\<rparr>); (if p && ~~ mask tcbBlockSizeBits \<in> set addrs then Some obj else ksPSpace s (p && ~~ mask tcbBlockSizeBits)) = Some (KOTCB objaa); Pa objaa\<rbrakk> \<Longrightarrow> p && ~~ mask tcbBlockSizeBits \<le> p
 2. \<And>P Pa obja objaa. \<lbrakk>\<forall>p\<in>set addrs. \<forall>P. \<not> obj_at' P p s; \<forall>p\<in>set addrs. \<forall>P. \<not> obj_at' P p s; \<forall>x\<in>set addrs. is_aligned x (case obj of KOEndpoint x \<Rightarrow> epSizeBits | KONotification x \<Rightarrow> ntfnSizeBits | KOTCB x \<Rightarrow> tcbBlockSizeBits | KOCTE x \<Rightarrow> cteSizeBits | KOArch x \<Rightarrow> archObjSize x | _ \<Rightarrow> pageBits); makeObjectKO dev tp = Some obj; (if p \<in> set addrs then Some obj else ksPSpace s p) = Some (KOCTE obja); is_aligned p cteSizeBits; P obja; ps_clear p cteSizeBits (s\<lparr>ksPSpace := \<lambda>xa. if xa \<in> set addrs then Some obj else ksPSpace s xa\<rparr>); (if p && ~~ mask tcbBlockSizeBits \<in> set addrs then Some obj else ksPSpace s (p && ~~ mask tcbBlockSizeBits)) = Some (KOTCB objaa); Pa objaa\<rbrakk> \<Longrightarrow> p \<le> (p && ~~ mask tcbBlockSizeBits) + 2 ^ tcbBlockSizeBits - 1
 3. \<And>P Pa obja objaa. \<lbrakk>\<forall>p\<in>set addrs. \<forall>P. \<not> obj_at' P p s; \<forall>p\<in>set addrs. \<forall>P. \<not> obj_at' P p s; \<forall>x\<in>set addrs. is_aligned x (case obj of KOEndpoint x \<Rightarrow> epSizeBits | KONotification x \<Rightarrow> ntfnSizeBits | KOTCB x \<Rightarrow> tcbBlockSizeBits | KOCTE x \<Rightarrow> cteSizeBits | KOArch x \<Rightarrow> archObjSize x | _ \<Rightarrow> pageBits); makeObjectKO dev tp = Some obj; (if p \<in> set addrs then Some obj else ksPSpace s p) = Some (KOCTE obja); is_aligned p cteSizeBits; P obja; ps_clear p cteSizeBits (s\<lparr>ksPSpace := \<lambda>xa. if xa \<in> set addrs then Some obj else ksPSpace s xa\<rparr>); (if p && ~~ mask tcbBlockSizeBits \<in> set addrs then Some obj else ksPSpace s (p && ~~ mask tcbBlockSizeBits)) = Some (KOTCB objaa); Pa objaa; False\<rbrakk> \<Longrightarrow> False
 4. \<And>p P. \<lbrakk>\<forall>p\<in>set addrs. \<forall>P. \<not> obj_at' P p s; \<forall>x\<in>set addrs. is_aligned x (objBitsKO obj); makeObjectKO dev tp = Some obj; p \<in> set addrs; obj_at' P p s\<rbrakk> \<Longrightarrow> False
 5. \<And>p P. \<lbrakk>\<forall>x\<in>set addrs. is_aligned x (objBitsKO obj); makeObjectKO dev tp = Some obj; p \<in> set addrs; obj_at' P p s\<rbrakk> \<Longrightarrow> False proof (prove)
goal (4 subgoals):
 1. \<And>P Pa obja objaa. \<lbrakk>\<forall>p\<in>set addrs. \<forall>P. \<not> obj_at' P p s; \<forall>p\<in>set addrs. \<forall>P. \<not> obj_at' P p s; \<forall>x\<in>set addrs. is_aligned x (case obj of KOEndpoint x \<Rightarrow> epSizeBits | KONotification x \<Rightarrow> ntfnSizeBits | KOTCB x \<Rightarrow> tcbBlockSizeBits | KOCTE x \<Rightarrow> cteSizeBits | KOArch x \<Rightarrow> archObjSize x | _ \<Rightarrow> pageBits); makeObjectKO dev tp = Some obj; (if p \<in> set addrs then Some obj else ksPSpace s p) = Some (KOCTE obja); is_aligned p cteSizeBits; P obja; ps_clear p cteSizeBits (s\<lparr>ksPSpace := \<lambda>xa. if xa \<in> set addrs then Some obj else ksPSpace s xa\<rparr>); (if p && ~~ mask tcbBlockSizeBits \<in> set addrs then Some obj else ksPSpace s (p && ~~ mask tcbBlockSizeBits)) = Some (KOTCB objaa); Pa objaa\<rbrakk> \<Longrightarrow> p \<le> (p && ~~ mask tcbBlockSizeBits) + 2 ^ tcbBlockSizeBits - 1
 2. \<And>P Pa obja objaa. \<lbrakk>\<forall>p\<in>set addrs. \<forall>P. \<not> obj_at' P p s; \<forall>p\<in>set addrs. \<forall>P. \<not> obj_at' P p s; \<forall>x\<in>set addrs. is_aligned x (case obj of KOEndpoint x \<Rightarrow> epSizeBits | KONotification x \<Rightarrow> ntfnSizeBits | KOTCB x \<Rightarrow> tcbBlockSizeBits | KOCTE x \<Rightarrow> cteSizeBits | KOArch x \<Rightarrow> archObjSize x | _ \<Rightarrow> pageBits); makeObjectKO dev tp = Some obj; (if p \<in> set addrs then Some obj else ksPSpace s p) = Some (KOCTE obja); is_aligned p cteSizeBits; P obja; ps_clear p cteSizeBits (s\<lparr>ksPSpace := \<lambda>xa. if xa \<in> set addrs then Some obj else ksPSpace s xa\<rparr>); (if p && ~~ mask tcbBlockSizeBits \<in> set addrs then Some obj else ksPSpace s (p && ~~ mask tcbBlockSizeBits)) = Some (KOTCB objaa); Pa objaa; False\<rbrakk> \<Longrightarrow> False
 3. \<And>p P. \<lbrakk>\<forall>p\<in>set addrs. \<forall>P. \<not> obj_at' P p s; \<forall>x\<in>set addrs. is_aligned x (objBitsKO obj); makeObjectKO dev tp = Some obj; p \<in> set addrs; obj_at' P p s\<rbrakk> \<Longrightarrow> False
 4. \<And>p P. \<lbrakk>\<forall>x\<in>set addrs. is_aligned x (objBitsKO obj); makeObjectKO dev tp = Some obj; p \<in> set addrs; obj_at' P p s\<rbrakk> \<Longrightarrow> False proof (prove)
goal (3 subgoals):
 1. \<And>P Pa obja objaa. \<lbrakk>\<forall>p\<in>set addrs. \<forall>P. \<not> obj_at' P p s; \<forall>p\<in>set addrs. \<forall>P. \<not> obj_at' P p s; \<forall>x\<in>set addrs. is_aligned x (case obj of KOEndpoint x \<Rightarrow> epSizeBits | KONotification x \<Rightarrow> ntfnSizeBits | KOTCB x \<Rightarrow> tcbBlockSizeBits | KOCTE x \<Rightarrow> cteSizeBits | KOArch x \<Rightarrow> archObjSize x | _ \<Rightarrow> pageBits); makeObjectKO dev tp = Some obj; (if p \<in> set addrs then Some obj else ksPSpace s p) = Some (KOCTE obja); is_aligned p cteSizeBits; P obja; ps_clear p cteSizeBits (s\<lparr>ksPSpace := \<lambda>xa. if xa \<in> set addrs then Some obj else ksPSpace s xa\<rparr>); (if p && ~~ mask tcbBlockSizeBits \<in> set addrs then Some obj else ksPSpace s (p && ~~ mask tcbBlockSizeBits)) = Some (KOTCB objaa); Pa objaa; False\<rbrakk> \<Longrightarrow> False
 2. \<And>p P. \<lbrakk>\<forall>p\<in>set addrs. \<forall>P. \<not> obj_at' P p s; \<forall>x\<in>set addrs. is_aligned x (objBitsKO obj); makeObjectKO dev tp = Some obj; p \<in> set addrs; obj_at' P p s\<rbrakk> \<Longrightarrow> False
 3. \<And>p P. \<lbrakk>\<forall>x\<in>set addrs. is_aligned x (objBitsKO obj); makeObjectKO dev tp = Some obj; p \<in> set addrs; obj_at' P p s\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!