theory Orphanage

lemma createNewObjects_no_orphans:
  "\<lbrace>\<lambda>s. no_orphans s \<and> invs' s \<and> pspace_no_overlap' ptr sz s
         \<and> (\<forall>slot\<in>set slots. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s)
         \<and> cte_wp_at' (\<lambda>cte. cteCap cte = UntypedCap d (ptr && ~~ mask sz) sz idx) cref s
         \<and> caps_no_overlap'' ptr sz s
         \<and> range_cover ptr sz (APIType_capBits tp us) (length slots)
         \<and> (tp = APIObjectType ArchTypes_H.CapTableObject \<longrightarrow> us > 0)
         \<and> caps_overlap_reserved' {ptr..ptr + of_nat (length slots) * 2 ^ APIType_capBits tp us - 1} s
         \<and> slots \<noteq> [] \<and> distinct slots \<and> ptr \<noteq> 0\<rbrace>
   createNewObjects tp cref slots ptr us d
   \<lbrace> \<lambda>rv s. no_orphans s \<rbrace>" apply (rule hoare_name_pre_state) apply clarsimp apply (rule hoare_pre) apply (rule createNewObjects_wp_helper) apply simp+ apply (simp add:insertNewCaps_def) apply wp apply (rule_tac P = "length caps = length slots" in hoare_gen_asm) apply (wp zipWithM_x_inv) apply simp apply (wp createNewCaps_no_orphans[where sz = sz] | clarsimp)+ apply (rule hoare_strengthen_post[OF createNewCaps_ret_len]) apply simp apply (clarsimp simp:invs_pspace_aligned' invs_valid_pspace' invs_pspace_distinct') apply (intro conjI) apply (erule range_cover.range_cover_n_less[where 'a=32, folded word_bits_def]) apply (clarsimp simp:cte_wp_at_ctes_of) apply (simp add:invs'_def valid_state'_def) apply (simp add: invs_ksCurDomain_maxDomain') done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. no_orphans s \<and> invs' s \<and> pspace_no_overlap' ptr sz s \<and> (\<forall>slot\<in>set slots. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s) \<and> cte_wp_at' (\<lambda>cte. cteCap cte = capability.UntypedCap d (ptr && ~~ mask sz) sz idx) cref s \<and> caps_no_overlap'' ptr sz s \<and> range_cover ptr sz (APIType_capBits tp us) (length slots) \<and> (tp = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> 0 < us) \<and> caps_overlap_reserved' {ptr..ptr + word_of_nat (length slots) * 2 ^ APIType_capBits tp us - 1} s \<and> slots \<noteq> [] \<and> distinct slots \<and> ptr \<noteq> 0\<rbrace> createNewObjects tp cref slots ptr us d \<lbrace>\<lambda>rv. no_orphans\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. no_orphans s \<and> invs' s \<and> pspace_no_overlap' ptr sz s \<and> (\<forall>slot\<in>set slots. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s) \<and> cte_wp_at' (\<lambda>cte. cteCap cte = capability.UntypedCap d (ptr && ~~ mask sz) sz idx) cref s \<and> caps_no_overlap'' ptr sz s \<and> range_cover ptr sz (APIType_capBits tp us) (length slots) \<and> (tp = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> 0 < us) \<and> caps_overlap_reserved' {ptr..ptr + word_of_nat (length slots) * 2 ^ APIType_capBits tp us - 1} s \<and> slots \<noteq> [] \<and> distinct slots \<and> ptr \<noteq> 0 \<Longrightarrow> \<lbrace>(=) s\<rbrace> createNewObjects tp cref slots ptr us d \<lbrace>\<lambda>rv. no_orphans\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>no_orphans s; invs' s; pspace_no_overlap' ptr sz s; \<forall>slot\<in>set slots. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s; cte_wp_at' (\<lambda>cte. cteCap cte = capability.UntypedCap d (ptr && ~~ mask sz) sz idx) cref s; caps_no_overlap'' ptr sz s; range_cover ptr sz (APIType_capBits tp us) (length slots); tp = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> 0 < us; caps_overlap_reserved' {ptr..ptr + word_of_nat (length slots) * 2 ^ APIType_capBits tp us - 1} s; slots \<noteq> []; distinct slots; ptr \<noteq> 0\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> createNewObjects tp cref slots ptr us d \<lbrace>\<lambda>rv. no_orphans\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>no_orphans s; invs' s; pspace_no_overlap' ptr sz s; \<forall>slot\<in>set slots. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s; cte_wp_at' (\<lambda>cte. cteCap cte = capability.UntypedCap d (ptr && ~~ mask sz) sz idx) cref s; caps_no_overlap'' ptr sz s; range_cover ptr sz (APIType_capBits tp us) (length slots); tp = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> 0 < us; caps_overlap_reserved' {ptr..ptr + word_of_nat (length slots) * 2 ^ APIType_capBits tp us - 1} s; slots \<noteq> []; distinct slots; ptr \<noteq> 0\<rbrakk> \<Longrightarrow> \<lbrace>?Q13 s\<rbrace> createNewObjects tp cref slots ptr us d \<lbrace>\<lambda>rv. no_orphans\<rbrace>
 2. \<And>s sa. \<lbrakk>no_orphans s; invs' s; pspace_no_overlap' ptr sz s; \<forall>slot\<in>set slots. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s; cte_wp_at' (\<lambda>cte. cteCap cte = capability.UntypedCap d (ptr && ~~ mask sz) sz idx) cref s; caps_no_overlap'' ptr sz s; range_cover ptr sz (APIType_capBits tp us) (length slots); tp = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> 0 < us; caps_overlap_reserved' {ptr..ptr + word_of_nat (length slots) * 2 ^ APIType_capBits tp us - 1} s; slots \<noteq> []; distinct slots; ptr \<noteq> 0; s = sa\<rbrakk> \<Longrightarrow> ?Q13 s sa proof (prove)
goal (6 subgoals):
 1. \<And>s. \<lbrakk>no_orphans s; invs' s; pspace_no_overlap' ptr sz s; \<forall>slot\<in>set slots. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s; cte_wp_at' (\<lambda>cte. cteCap cte = capability.UntypedCap d (ptr && ~~ mask sz) sz idx) cref s; caps_no_overlap'' ptr sz s; range_cover ptr sz (APIType_capBits tp us) (length slots); tp = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> 0 < us; caps_overlap_reserved' {ptr..ptr + word_of_nat (length slots) * 2 ^ APIType_capBits tp us - 1} s; slots \<noteq> []; distinct slots; ptr \<noteq> 0\<rbrakk> \<Longrightarrow> distinct slots
 2. \<And>s. \<lbrakk>no_orphans s; invs' s; pspace_no_overlap' ptr sz s; \<forall>slot\<in>set slots. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s; cte_wp_at' (\<lambda>cte. cteCap cte = capability.UntypedCap d (ptr && ~~ mask sz) sz idx) cref s; caps_no_overlap'' ptr sz s; range_cover ptr sz (APIType_capBits tp us) (length slots); tp = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> 0 < us; caps_overlap_reserved' {ptr..ptr + word_of_nat (length slots) * 2 ^ APIType_capBits tp us - 1} s; slots \<noteq> []; distinct slots; ptr \<noteq> 0\<rbrakk> \<Longrightarrow> range_cover ptr (?sz16 s) (getObjectSize tp us) (length slots)
 3. \<And>s. \<lbrakk>no_orphans s; invs' s; pspace_no_overlap' ptr sz s; \<forall>slot\<in>set slots. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s; cte_wp_at' (\<lambda>cte. cteCap cte = capability.UntypedCap d (ptr && ~~ mask sz) sz idx) cref s; caps_no_overlap'' ptr sz s; range_cover ptr sz (APIType_capBits tp us) (length slots); tp = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> 0 < us; caps_overlap_reserved' {ptr..ptr + word_of_nat (length slots) * 2 ^ APIType_capBits tp us - 1} s; slots \<noteq> []; distinct slots; ptr \<noteq> 0\<rbrakk> \<Longrightarrow> ptr \<noteq> 0
 4. \<And>s. \<lbrakk>no_orphans s; invs' s; pspace_no_overlap' ptr sz s; \<forall>slot\<in>set slots. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s; cte_wp_at' (\<lambda>cte. cteCap cte = capability.UntypedCap d (ptr && ~~ mask sz) sz idx) cref s; caps_no_overlap'' ptr sz s; range_cover ptr sz (APIType_capBits tp us) (length slots); tp = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> 0 < us; caps_overlap_reserved' {ptr..ptr + word_of_nat (length slots) * 2 ^ APIType_capBits tp us - 1} s; slots \<noteq> []; distinct slots; ptr \<noteq> 0\<rbrakk> \<Longrightarrow> length slots \<noteq> 0
 5. \<And>s. \<lbrakk>no_orphans s; invs' s; pspace_no_overlap' ptr sz s; \<forall>slot\<in>set slots. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s; cte_wp_at' (\<lambda>cte. cteCap cte = capability.UntypedCap d (ptr && ~~ mask sz) sz idx) cref s; caps_no_overlap'' ptr sz s; range_cover ptr sz (APIType_capBits tp us) (length slots); tp = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> 0 < us; caps_overlap_reserved' {ptr..ptr + word_of_nat (length slots) * 2 ^ APIType_capBits tp us - 1} s; slots \<noteq> []; distinct slots; ptr \<noteq> 0\<rbrakk> \<Longrightarrow> \<lbrace>?P16 s\<rbrace> insertNewCaps tp cref slots ptr us d \<lbrace>\<lambda>rv. no_orphans\<rbrace>
 6. \<And>s sa. \<lbrakk>no_orphans s; invs' s; pspace_no_overlap' ptr sz s; \<forall>slot\<in>set slots. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s; cte_wp_at' (\<lambda>cte. cteCap cte = capability.UntypedCap d (ptr && ~~ mask sz) sz idx) cref s; caps_no_overlap'' ptr sz s; range_cover ptr sz (APIType_capBits tp us) (length slots); tp = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> 0 < us; caps_overlap_reserved' {ptr..ptr + word_of_nat (length slots) * 2 ^ APIType_capBits tp us - 1} s; slots \<noteq> []; distinct slots; ptr \<noteq> 0; s = sa\<rbrakk> \<Longrightarrow> (?P16 s and (cte_wp_at' (\<lambda>c. isUntypedCap (cteCap c)) cref and (\<lambda>s. \<forall>slot\<in>set slots. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s) and pspace_no_overlap' ptr (?sz16 s) and caps_no_overlap'' ptr (?sz16 s) and valid_pspace' and valid_arch_state' and caps_overlap_reserved' {ptr..ptr + word_of_nat (length slots) * 2 ^ getObjectSize tp us - 1} and (\<lambda>s. ksCurDomain s \<le> maxDomain))) sa proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>no_orphans s; invs' s; pspace_no_overlap' ptr sz s; \<forall>slot\<in>set slots. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s; cte_wp_at' (\<lambda>cte. cteCap cte = capability.UntypedCap d (ptr && ~~ mask sz) sz idx) cref s; caps_no_overlap'' ptr sz s; range_cover ptr sz (APIType_capBits tp us) (length slots); tp = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> 0 < us; caps_overlap_reserved' {ptr..ptr + word_of_nat (length slots) * 2 ^ APIType_capBits tp us - 1} s; slots \<noteq> []; distinct slots; ptr \<noteq> 0\<rbrakk> \<Longrightarrow> \<lbrace>?P16 s\<rbrace> insertNewCaps tp cref slots ptr us d \<lbrace>\<lambda>rv. no_orphans\<rbrace>
 2. \<And>s sa. \<lbrakk>no_orphans s; invs' s; pspace_no_overlap' ptr sz s; \<forall>slot\<in>set slots. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s; cte_wp_at' (\<lambda>cte. cteCap cte = capability.UntypedCap d (ptr && ~~ mask sz) sz idx) cref s; caps_no_overlap'' ptr sz s; range_cover ptr sz (APIType_capBits tp us) (length slots); tp = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> 0 < us; caps_overlap_reserved' {ptr..ptr + word_of_nat (length slots) * 2 ^ APIType_capBits tp us - 1} s; slots \<noteq> []; distinct slots; ptr \<noteq> 0; s = sa\<rbrakk> \<Longrightarrow> (?P16 s and (cte_wp_at' (\<lambda>c. isUntypedCap (cteCap c)) cref and (\<lambda>s. \<forall>slot\<in>set slots. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s) and pspace_no_overlap' ptr sz and caps_no_overlap'' ptr sz and valid_pspace' and valid_arch_state' and caps_overlap_reserved' {ptr..ptr + word_of_nat (length slots) * 2 ^ getObjectSize tp us - 1} and (\<lambda>s. ksCurDomain s \<le> maxDomain))) sa proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>no_orphans s; invs' s; pspace_no_overlap' ptr sz s; \<forall>slot\<in>set slots. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s; cte_wp_at' (\<lambda>cte. cteCap cte = capability.UntypedCap d (ptr && ~~ mask sz) sz idx) cref s; caps_no_overlap'' ptr sz s; range_cover ptr sz (APIType_capBits tp us) (length slots); tp = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> 0 < us; caps_overlap_reserved' {ptr..ptr + word_of_nat (length slots) * 2 ^ APIType_capBits tp us - 1} s; slots \<noteq> []; distinct slots; ptr \<noteq> 0\<rbrakk> \<Longrightarrow> \<lbrace>?P16 s\<rbrace> createNewCaps tp ptr (length slots) us d >>= zipWithM_x (insertNewCap cref) slots \<lbrace>\<lambda>rv. no_orphans\<rbrace>
 2. \<And>s sa. \<lbrakk>no_orphans s; invs' s; pspace_no_overlap' ptr sz s; \<forall>slot\<in>set slots. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s; cte_wp_at' (\<lambda>cte. cteCap cte = capability.UntypedCap d (ptr && ~~ mask sz) sz idx) cref s; caps_no_overlap'' ptr sz s; range_cover ptr sz (APIType_capBits tp us) (length slots); tp = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> 0 < us; caps_overlap_reserved' {ptr..ptr + word_of_nat (length slots) * 2 ^ APIType_capBits tp us - 1} s; slots \<noteq> []; distinct slots; ptr \<noteq> 0; s = sa\<rbrakk> \<Longrightarrow> (?P16 s and (cte_wp_at' (\<lambda>c. isUntypedCap (cteCap c)) cref and (\<lambda>s. \<forall>slot\<in>set slots. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s) and pspace_no_overlap' ptr sz and caps_no_overlap'' ptr sz and valid_pspace' and valid_arch_state' and caps_overlap_reserved' {ptr..ptr + word_of_nat (length slots) * 2 ^ getObjectSize tp us - 1} and (\<lambda>s. ksCurDomain s \<le> maxDomain))) sa proof (prove)
goal (3 subgoals):
 1. \<And>s caps. \<lbrakk>no_orphans s; invs' s; pspace_no_overlap' ptr sz s; \<forall>slot\<in>set slots. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s; cte_wp_at' (\<lambda>cte. cteCap cte = capability.UntypedCap d (ptr && ~~ mask sz) sz idx) cref s; caps_no_overlap'' ptr sz s; range_cover ptr sz (APIType_capBits tp us) (length slots); tp = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> 0 < us; caps_overlap_reserved' {ptr..ptr + word_of_nat (length slots) * 2 ^ APIType_capBits tp us - 1} s; slots \<noteq> []; distinct slots; ptr \<noteq> 0\<rbrakk> \<Longrightarrow> \<lbrace>?B23 s caps\<rbrace> zipWithM_x (insertNewCap cref) slots caps \<lbrace>\<lambda>rv. no_orphans\<rbrace>
 2. \<And>s. \<lbrakk>no_orphans s; invs' s; pspace_no_overlap' ptr sz s; \<forall>slot\<in>set slots. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s; cte_wp_at' (\<lambda>cte. cteCap cte = capability.UntypedCap d (ptr && ~~ mask sz) sz idx) cref s; caps_no_overlap'' ptr sz s; range_cover ptr sz (APIType_capBits tp us) (length slots); tp = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> 0 < us; caps_overlap_reserved' {ptr..ptr + word_of_nat (length slots) * 2 ^ APIType_capBits tp us - 1} s; slots \<noteq> []; distinct slots; ptr \<noteq> 0\<rbrakk> \<Longrightarrow> \<lbrace>?P16 s\<rbrace> createNewCaps tp ptr (length slots) us d \<lbrace>?B23 s\<rbrace>
 3. \<And>s sa. \<lbrakk>no_orphans s; invs' s; pspace_no_overlap' ptr sz s; \<forall>slot\<in>set slots. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s; cte_wp_at' (\<lambda>cte. cteCap cte = capability.UntypedCap d (ptr && ~~ mask sz) sz idx) cref s; caps_no_overlap'' ptr sz s; range_cover ptr sz (APIType_capBits tp us) (length slots); tp = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> 0 < us; caps_overlap_reserved' {ptr..ptr + word_of_nat (length slots) * 2 ^ APIType_capBits tp us - 1} s; slots \<noteq> []; distinct slots; ptr \<noteq> 0; s = sa\<rbrakk> \<Longrightarrow> (?P16 s and (cte_wp_at' (\<lambda>c. isUntypedCap (cteCap c)) cref and (\<lambda>s. \<forall>slot\<in>set slots. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s) and pspace_no_overlap' ptr sz and caps_no_overlap'' ptr sz and valid_pspace' and valid_arch_state' and caps_overlap_reserved' {ptr..ptr + word_of_nat (length slots) * 2 ^ getObjectSize tp us - 1} and (\<lambda>s. ksCurDomain s \<le> maxDomain))) sa proof (prove)
goal (3 subgoals):
 1. \<And>s caps. \<lbrakk>no_orphans s; invs' s; pspace_no_overlap' ptr sz s; \<forall>slot\<in>set slots. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s; cte_wp_at' (\<lambda>cte. cteCap cte = capability.UntypedCap d (ptr && ~~ mask sz) sz idx) cref s; caps_no_overlap'' ptr sz s; range_cover ptr sz (APIType_capBits tp us) (length slots); tp = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> 0 < us; caps_overlap_reserved' {ptr..ptr + word_of_nat (length slots) * 2 ^ APIType_capBits tp us - 1} s; slots \<noteq> []; distinct slots; ptr \<noteq> 0; length caps = length slots\<rbrakk> \<Longrightarrow> \<lbrace>?P'25 s caps\<rbrace> zipWithM_x (insertNewCap cref) slots caps \<lbrace>\<lambda>rv. no_orphans\<rbrace>
 2. \<And>s. \<lbrakk>no_orphans s; invs' s; pspace_no_overlap' ptr sz s; \<forall>slot\<in>set slots. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s; cte_wp_at' (\<lambda>cte. cteCap cte = capability.UntypedCap d (ptr && ~~ mask sz) sz idx) cref s; caps_no_overlap'' ptr sz s; range_cover ptr sz (APIType_capBits tp us) (length slots); tp = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> 0 < us; caps_overlap_reserved' {ptr..ptr + word_of_nat (length slots) * 2 ^ APIType_capBits tp us - 1} s; slots \<noteq> []; distinct slots; ptr \<noteq> 0\<rbrakk> \<Longrightarrow> \<lbrace>?P16 s\<rbrace> createNewCaps tp ptr (length slots) us d \<lbrace>\<lambda>caps. ?P'25 s caps and K (length caps = length slots)\<rbrace>
 3. \<And>s sa. \<lbrakk>no_orphans s; invs' s; pspace_no_overlap' ptr sz s; \<forall>slot\<in>set slots. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s; cte_wp_at' (\<lambda>cte. cteCap cte = capability.UntypedCap d (ptr && ~~ mask sz) sz idx) cref s; caps_no_overlap'' ptr sz s; range_cover ptr sz (APIType_capBits tp us) (length slots); tp = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> 0 < us; caps_overlap_reserved' {ptr..ptr + word_of_nat (length slots) * 2 ^ APIType_capBits tp us - 1} s; slots \<noteq> []; distinct slots; ptr \<noteq> 0; s = sa\<rbrakk> \<Longrightarrow> (?P16 s and (cte_wp_at' (\<lambda>c. isUntypedCap (cteCap c)) cref and (\<lambda>s. \<forall>slot\<in>set slots. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s) and pspace_no_overlap' ptr sz and caps_no_overlap'' ptr sz and valid_pspace' and valid_arch_state' and caps_overlap_reserved' {ptr..ptr + word_of_nat (length slots) * 2 ^ getObjectSize tp us - 1} and (\<lambda>s. ksCurDomain s \<le> maxDomain))) sa proof (prove)
goal (3 subgoals):
 1. \<And>s caps. \<lbrakk>no_orphans s; invs' s; pspace_no_overlap' ptr sz s; \<forall>slot\<in>set slots. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s; cte_wp_at' (\<lambda>cte. cteCap cte = capability.UntypedCap d (ptr && ~~ mask sz) sz idx) cref s; caps_no_overlap'' ptr sz s; range_cover ptr sz (APIType_capBits tp us) (length slots); tp = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> 0 < us; caps_overlap_reserved' {ptr..ptr + word_of_nat (length slots) * 2 ^ APIType_capBits tp us - 1} s; slots \<noteq> []; distinct slots; ptr \<noteq> 0; length caps = length slots\<rbrakk> \<Longrightarrow> length slots = length caps
 2. \<And>s. \<lbrakk>no_orphans s; invs' s; pspace_no_overlap' ptr sz s; \<forall>slot\<in>set slots. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s; cte_wp_at' (\<lambda>cte. cteCap cte = capability.UntypedCap d (ptr && ~~ mask sz) sz idx) cref s; caps_no_overlap'' ptr sz s; range_cover ptr sz (APIType_capBits tp us) (length slots); tp = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> 0 < us; caps_overlap_reserved' {ptr..ptr + word_of_nat (length slots) * 2 ^ APIType_capBits tp us - 1} s; slots \<noteq> []; distinct slots; ptr \<noteq> 0\<rbrakk> \<Longrightarrow> \<lbrace>?P16 s\<rbrace> createNewCaps tp ptr (length slots) us d \<lbrace>\<lambda>caps. no_orphans and K (length caps = length slots)\<rbrace>
 3. \<And>s sa. \<lbrakk>no_orphans s; invs' s; pspace_no_overlap' ptr sz s; \<forall>slot\<in>set slots. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s; cte_wp_at' (\<lambda>cte. cteCap cte = capability.UntypedCap d (ptr && ~~ mask sz) sz idx) cref s; caps_no_overlap'' ptr sz s; range_cover ptr sz (APIType_capBits tp us) (length slots); tp = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> 0 < us; caps_overlap_reserved' {ptr..ptr + word_of_nat (length slots) * 2 ^ APIType_capBits tp us - 1} s; slots \<noteq> []; distinct slots; ptr \<noteq> 0; s = sa\<rbrakk> \<Longrightarrow> (?P16 s and (cte_wp_at' (\<lambda>c. isUntypedCap (cteCap c)) cref and (\<lambda>s. \<forall>slot\<in>set slots. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s) and pspace_no_overlap' ptr sz and caps_no_overlap'' ptr sz and valid_pspace' and valid_arch_state' and caps_overlap_reserved' {ptr..ptr + word_of_nat (length slots) * 2 ^ getObjectSize tp us - 1} and (\<lambda>s. ksCurDomain s \<le> maxDomain))) sa proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>no_orphans s; invs' s; pspace_no_overlap' ptr sz s; \<forall>slot\<in>set slots. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s; cte_wp_at' (\<lambda>cte. cteCap cte = capability.UntypedCap d (ptr && ~~ mask sz) sz idx) cref s; caps_no_overlap'' ptr sz s; range_cover ptr sz (APIType_capBits tp us) (length slots); tp = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> 0 < us; caps_overlap_reserved' {ptr..ptr + word_of_nat (length slots) * 2 ^ APIType_capBits tp us - 1} s; slots \<noteq> []; distinct slots; ptr \<noteq> 0\<rbrakk> \<Longrightarrow> \<lbrace>?P16 s\<rbrace> createNewCaps tp ptr (length slots) us d \<lbrace>\<lambda>caps. no_orphans and K (length caps = length slots)\<rbrace>
 2. \<And>s sa. \<lbrakk>no_orphans s; invs' s; pspace_no_overlap' ptr sz s; \<forall>slot\<in>set slots. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s; cte_wp_at' (\<lambda>cte. cteCap cte = capability.UntypedCap d (ptr && ~~ mask sz) sz idx) cref s; caps_no_overlap'' ptr sz s; range_cover ptr sz (APIType_capBits tp us) (length slots); tp = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> 0 < us; caps_overlap_reserved' {ptr..ptr + word_of_nat (length slots) * 2 ^ APIType_capBits tp us - 1} s; slots \<noteq> []; distinct slots; ptr \<noteq> 0; s = sa\<rbrakk> \<Longrightarrow> (?P16 s and (cte_wp_at' (\<lambda>c. isUntypedCap (cteCap c)) cref and (\<lambda>s. \<forall>slot\<in>set slots. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s) and pspace_no_overlap' ptr sz and caps_no_overlap'' ptr sz and valid_pspace' and valid_arch_state' and caps_overlap_reserved' {ptr..ptr + word_of_nat (length slots) * 2 ^ getObjectSize tp us - 1} and (\<lambda>s. ksCurDomain s \<le> maxDomain))) sa proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>no_orphans s; invs' s; pspace_no_overlap' ptr sz s; \<forall>slot\<in>set slots. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s; cte_wp_at' (\<lambda>cte. cteCap cte = capability.UntypedCap d (ptr && ~~ mask sz) sz idx) cref s; caps_no_overlap'' ptr sz s; range_cover ptr sz (APIType_capBits tp us) (length slots); tp = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> 0 < us; caps_overlap_reserved' {ptr..ptr + word_of_nat (length slots) * 2 ^ APIType_capBits tp us - 1} s; slots \<noteq> []; distinct slots; ptr \<noteq> 0\<rbrakk> \<Longrightarrow> \<lbrace>?P'32 s\<rbrace> createNewCaps tp ptr (length slots) us d \<lbrace>\<lambda>rv s. length rv = length slots\<rbrace>
 2. \<And>s sa. \<lbrakk>no_orphans s; invs' s; pspace_no_overlap' ptr sz s; \<forall>slot\<in>set slots. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s; cte_wp_at' (\<lambda>cte. cteCap cte = capability.UntypedCap d (ptr && ~~ mask sz) sz idx) cref s; caps_no_overlap'' ptr sz s; range_cover ptr sz (APIType_capBits tp us) (length slots); tp = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> 0 < us; caps_overlap_reserved' {ptr..ptr + word_of_nat (length slots) * 2 ^ APIType_capBits tp us - 1} s; slots \<noteq> []; distinct slots; ptr \<noteq> 0; s = sa\<rbrakk> \<Longrightarrow> ((\<lambda>sa. ((\<lambda>s. no_orphans s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s \<and> (tp = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> 0 < us)) and K (range_cover ptr sz (APIType_capBits tp us) (length slots) \<and> 0 < length slots)) sa \<and> ?P'32 s sa) and (cte_wp_at' (\<lambda>c. isUntypedCap (cteCap c)) cref and (\<lambda>s. \<forall>slot\<in>set slots. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s) and pspace_no_overlap' ptr sz and caps_no_overlap'' ptr sz and valid_pspace' and valid_arch_state' and caps_overlap_reserved' {ptr..ptr + word_of_nat (length slots) * 2 ^ getObjectSize tp us - 1} and (\<lambda>s. ksCurDomain s \<le> maxDomain))) sa proof (prove)
goal (2 subgoals):
 1. \<And>s rv sa. \<lbrakk>no_orphans s; invs' s; pspace_no_overlap' ptr sz s; \<forall>slot\<in>set slots. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s; cte_wp_at' (\<lambda>cte. cteCap cte = capability.UntypedCap d (ptr && ~~ mask sz) sz idx) cref s; caps_no_overlap'' ptr sz s; range_cover ptr sz (APIType_capBits tp us) (length slots); tp = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> 0 < us; caps_overlap_reserved' {ptr..ptr + word_of_nat (length slots) * 2 ^ APIType_capBits tp us - 1} s; slots \<noteq> []; distinct slots; ptr \<noteq> 0; length slots = length rv\<rbrakk> \<Longrightarrow> length rv = length slots
 2. \<And>s sa. \<lbrakk>no_orphans s; invs' s; pspace_no_overlap' ptr sz s; \<forall>slot\<in>set slots. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s; cte_wp_at' (\<lambda>cte. cteCap cte = capability.UntypedCap d (ptr && ~~ mask sz) sz idx) cref s; caps_no_overlap'' ptr sz s; range_cover ptr sz (APIType_capBits tp us) (length slots); tp = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> 0 < us; caps_overlap_reserved' {ptr..ptr + word_of_nat (length slots) * 2 ^ APIType_capBits tp us - 1} s; slots \<noteq> []; distinct slots; ptr \<noteq> 0; s = sa\<rbrakk> \<Longrightarrow> ((\<lambda>s. ((\<lambda>s. no_orphans s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s \<and> (tp = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> 0 < us)) and K (range_cover ptr sz (APIType_capBits tp us) (length slots) \<and> 0 < length slots)) s \<and> K (length slots < 2 ^ word_bits \<and> length slots \<noteq> 0) s) and (cte_wp_at' (\<lambda>c. isUntypedCap (cteCap c)) cref and (\<lambda>s. \<forall>slot\<in>set slots. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s) and pspace_no_overlap' ptr sz and caps_no_overlap'' ptr sz and valid_pspace' and valid_arch_state' and caps_overlap_reserved' {ptr..ptr + word_of_nat (length slots) * 2 ^ getObjectSize tp us - 1} and (\<lambda>s. ksCurDomain s \<le> maxDomain))) sa proof (prove)
goal (1 subgoal):
 1. \<And>s sa. \<lbrakk>no_orphans s; invs' s; pspace_no_overlap' ptr sz s; \<forall>slot\<in>set slots. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s; cte_wp_at' (\<lambda>cte. cteCap cte = capability.UntypedCap d (ptr && ~~ mask sz) sz idx) cref s; caps_no_overlap'' ptr sz s; range_cover ptr sz (APIType_capBits tp us) (length slots); tp = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> 0 < us; caps_overlap_reserved' {ptr..ptr + word_of_nat (length slots) * 2 ^ APIType_capBits tp us - 1} s; slots \<noteq> []; distinct slots; ptr \<noteq> 0; s = sa\<rbrakk> \<Longrightarrow> ((\<lambda>s. ((\<lambda>s. no_orphans s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s \<and> (tp = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> 0 < us)) and K (range_cover ptr sz (APIType_capBits tp us) (length slots) \<and> 0 < length slots)) s \<and> K (length slots < 2 ^ word_bits \<and> length slots \<noteq> 0) s) and (cte_wp_at' (\<lambda>c. isUntypedCap (cteCap c)) cref and (\<lambda>s. \<forall>slot\<in>set slots. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s) and pspace_no_overlap' ptr sz and caps_no_overlap'' ptr sz and valid_pspace' and valid_arch_state' and caps_overlap_reserved' {ptr..ptr + word_of_nat (length slots) * 2 ^ getObjectSize tp us - 1} and (\<lambda>s. ksCurDomain s \<le> maxDomain))) sa proof (prove)
goal (1 subgoal):
 1. \<And>sa. \<lbrakk>no_orphans sa; invs' sa; pspace_no_overlap' ptr sz sa; \<forall>slot\<in>set slots. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot sa; cte_wp_at' (\<lambda>cte. cteCap cte = capability.UntypedCap d (ptr && ~~ mask sz) sz idx) cref sa; caps_no_overlap'' ptr sz sa; range_cover ptr sz (APIType_capBits tp us) (length slots); tp = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> 0 < us; caps_overlap_reserved' {ptr..ptr + word_of_nat (length slots) * 2 ^ APIType_capBits tp us - 1} sa; slots \<noteq> []; distinct slots; ptr \<noteq> 0\<rbrakk> \<Longrightarrow> length slots < 2 ^ word_bits \<and> cte_wp_at' (\<lambda>c. isUntypedCap (cteCap c)) cref sa \<and> valid_arch_state' sa \<and> ksCurDomain sa \<le> maxDomain proof (prove)
goal (4 subgoals):
 1. \<And>sa. \<lbrakk>no_orphans sa; invs' sa; pspace_no_overlap' ptr sz sa; \<forall>slot\<in>set slots. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot sa; cte_wp_at' (\<lambda>cte. cteCap cte = capability.UntypedCap d (ptr && ~~ mask sz) sz idx) cref sa; caps_no_overlap'' ptr sz sa; range_cover ptr sz (APIType_capBits tp us) (length slots); tp = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> 0 < us; caps_overlap_reserved' {ptr..ptr + word_of_nat (length slots) * 2 ^ APIType_capBits tp us - 1} sa; slots \<noteq> []; distinct slots; ptr \<noteq> 0\<rbrakk> \<Longrightarrow> length slots < 2 ^ word_bits
 2. \<And>sa. \<lbrakk>no_orphans sa; invs' sa; pspace_no_overlap' ptr sz sa; \<forall>slot\<in>set slots. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot sa; cte_wp_at' (\<lambda>cte. cteCap cte = capability.UntypedCap d (ptr && ~~ mask sz) sz idx) cref sa; caps_no_overlap'' ptr sz sa; range_cover ptr sz (APIType_capBits tp us) (length slots); tp = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> 0 < us; caps_overlap_reserved' {ptr..ptr + word_of_nat (length slots) * 2 ^ APIType_capBits tp us - 1} sa; slots \<noteq> []; distinct slots; ptr \<noteq> 0\<rbrakk> \<Longrightarrow> cte_wp_at' (\<lambda>c. isUntypedCap (cteCap c)) cref sa
 3. \<And>sa. \<lbrakk>no_orphans sa; invs' sa; pspace_no_overlap' ptr sz sa; \<forall>slot\<in>set slots. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot sa; cte_wp_at' (\<lambda>cte. cteCap cte = capability.UntypedCap d (ptr && ~~ mask sz) sz idx) cref sa; caps_no_overlap'' ptr sz sa; range_cover ptr sz (APIType_capBits tp us) (length slots); tp = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> 0 < us; caps_overlap_reserved' {ptr..ptr + word_of_nat (length slots) * 2 ^ APIType_capBits tp us - 1} sa; slots \<noteq> []; distinct slots; ptr \<noteq> 0\<rbrakk> \<Longrightarrow> valid_arch_state' sa
 4. \<And>sa. \<lbrakk>no_orphans sa; invs' sa; pspace_no_overlap' ptr sz sa; \<forall>slot\<in>set slots. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot sa; cte_wp_at' (\<lambda>cte. cteCap cte = capability.UntypedCap d (ptr && ~~ mask sz) sz idx) cref sa; caps_no_overlap'' ptr sz sa; range_cover ptr sz (APIType_capBits tp us) (length slots); tp = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> 0 < us; caps_overlap_reserved' {ptr..ptr + word_of_nat (length slots) * 2 ^ APIType_capBits tp us - 1} sa; slots \<noteq> []; distinct slots; ptr \<noteq> 0\<rbrakk> \<Longrightarrow> ksCurDomain sa \<le> maxDomain proof (prove)
goal (3 subgoals):
 1. \<And>sa. \<lbrakk>no_orphans sa; invs' sa; pspace_no_overlap' ptr sz sa; \<forall>slot\<in>set slots. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot sa; cte_wp_at' (\<lambda>cte. cteCap cte = capability.UntypedCap d (ptr && ~~ mask sz) sz idx) cref sa; caps_no_overlap'' ptr sz sa; range_cover ptr sz (APIType_capBits tp us) (length slots); tp = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> 0 < us; caps_overlap_reserved' {ptr..ptr + word_of_nat (length slots) * 2 ^ APIType_capBits tp us - 1} sa; slots \<noteq> []; distinct slots; ptr \<noteq> 0\<rbrakk> \<Longrightarrow> cte_wp_at' (\<lambda>c. isUntypedCap (cteCap c)) cref sa
 2. \<And>sa. \<lbrakk>no_orphans sa; invs' sa; pspace_no_overlap' ptr sz sa; \<forall>slot\<in>set slots. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot sa; cte_wp_at' (\<lambda>cte. cteCap cte = capability.UntypedCap d (ptr && ~~ mask sz) sz idx) cref sa; caps_no_overlap'' ptr sz sa; range_cover ptr sz (APIType_capBits tp us) (length slots); tp = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> 0 < us; caps_overlap_reserved' {ptr..ptr + word_of_nat (length slots) * 2 ^ APIType_capBits tp us - 1} sa; slots \<noteq> []; distinct slots; ptr \<noteq> 0\<rbrakk> \<Longrightarrow> valid_arch_state' sa
 3. \<And>sa. \<lbrakk>no_orphans sa; invs' sa; pspace_no_overlap' ptr sz sa; \<forall>slot\<in>set slots. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot sa; cte_wp_at' (\<lambda>cte. cteCap cte = capability.UntypedCap d (ptr && ~~ mask sz) sz idx) cref sa; caps_no_overlap'' ptr sz sa; range_cover ptr sz (APIType_capBits tp us) (length slots); tp = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> 0 < us; caps_overlap_reserved' {ptr..ptr + word_of_nat (length slots) * 2 ^ APIType_capBits tp us - 1} sa; slots \<noteq> []; distinct slots; ptr \<noteq> 0\<rbrakk> \<Longrightarrow> ksCurDomain sa \<le> maxDomain proof (prove)
goal (2 subgoals):
 1. \<And>sa. \<lbrakk>no_orphans sa; invs' sa; pspace_no_overlap' ptr sz sa; \<forall>slot\<in>set slots. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot sa; cte_wp_at' (\<lambda>cte. cteCap cte = capability.UntypedCap d (ptr && ~~ mask sz) sz idx) cref sa; caps_no_overlap'' ptr sz sa; range_cover ptr sz (APIType_capBits tp us) (length slots); tp = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> 0 < us; caps_overlap_reserved' {ptr..ptr + word_of_nat (length slots) * 2 ^ APIType_capBits tp us - 1} sa; slots \<noteq> []; distinct slots; ptr \<noteq> 0\<rbrakk> \<Longrightarrow> valid_arch_state' sa
 2. \<And>sa. \<lbrakk>no_orphans sa; invs' sa; pspace_no_overlap' ptr sz sa; \<forall>slot\<in>set slots. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot sa; cte_wp_at' (\<lambda>cte. cteCap cte = capability.UntypedCap d (ptr && ~~ mask sz) sz idx) cref sa; caps_no_overlap'' ptr sz sa; range_cover ptr sz (APIType_capBits tp us) (length slots); tp = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> 0 < us; caps_overlap_reserved' {ptr..ptr + word_of_nat (length slots) * 2 ^ APIType_capBits tp us - 1} sa; slots \<noteq> []; distinct slots; ptr \<noteq> 0\<rbrakk> \<Longrightarrow> ksCurDomain sa \<le> maxDomain proof (prove)
goal (1 subgoal):
 1. \<And>sa. \<lbrakk>no_orphans sa; invs' sa; pspace_no_overlap' ptr sz sa; \<forall>slot\<in>set slots. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot sa; cte_wp_at' (\<lambda>cte. cteCap cte = capability.UntypedCap d (ptr && ~~ mask sz) sz idx) cref sa; caps_no_overlap'' ptr sz sa; range_cover ptr sz (APIType_capBits tp us) (length slots); tp = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> 0 < us; caps_overlap_reserved' {ptr..ptr + word_of_nat (length slots) * 2 ^ APIType_capBits tp us - 1} sa; slots \<noteq> []; distinct slots; ptr \<noteq> 0\<rbrakk> \<Longrightarrow> ksCurDomain sa \<le> maxDomain proof (prove)
goal:
No subgoals!