theory Retype_R

lemma createObjects_no_cte_invs:
  assumes moKO: "makeObjectKO dev ty = Some val"
  assumes no_cte: "\<And>c. projectKO_opt val \<noteq> Some (c::cte)"
  assumes no_tcb: "\<And>t. projectKO_opt val \<noteq> Some (t::tcb)"
  shows
  "\<lbrace>\<lambda>s. range_cover ptr sz ((objBitsKO val) + gbits) n \<and> n \<noteq> 0 \<and> invs' s \<and> ct_active' s
        \<and> pspace_no_overlap' ptr sz s \<and> ptr \<noteq> 0
        \<and> {ptr .. (ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> kernel_data_refs = {}
        \<and> caps_overlap_reserved' {ptr..ptr + of_nat (n * 2 ^ gbits * 2 ^ objBitsKO val) - 1} s
        \<and> caps_no_overlap'' ptr sz s \<and>
       refs_of' val = {} \<and> \<not> live' val
            \<and> (\<forall>pde. projectKO_opt val = Some pde \<longrightarrow> pde = InvalidPDE)\<rbrace>
  createObjects ptr n val gbits
  \<lbrace>\<lambda>rv. invs'\<rbrace>" proof - have co_ct_not_inQ:
    "\<lbrakk>range_cover ptr sz ((objBitsKO val) + gbits) n; n \<noteq> 0\<rbrakk> \<Longrightarrow>
     \<lbrace>\<lambda>s. ct_not_inQ s \<and> pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrace>
      createObjects ptr n val gbits \<lbrace>\<lambda>_. ct_not_inQ\<rbrace>"
    (is "\<lbrakk> _; _ \<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. ct_not_inQ s \<and> ?REST s\<rbrace> _ \<lbrace>_\<rbrace>") apply (simp add: ct_not_inQ_def) apply (rule_tac Q="\<lambda>s. (ksSchedulerAction s = ResumeCurrentThread) \<longrightarrow>
                             (obj_at' (Not \<circ> tcbQueued) (ksCurThread s) s \<and> ?REST s)"
             in hoare_pre_imp, clarsimp) apply (rule hoare_convert_imp [OF createObjects_nosch]) apply (rule hoare_weaken_pre) apply (wps createObjects_ct) apply (wp createObjects_obj_at_other) apply (simp)+ done show ?thesis apply (rule hoare_grab_asm)+ apply (clarsimp simp: invs'_def valid_state'_def) apply wp apply (rule hoare_pre) apply (rule hoare_vcg_conj_lift) apply (simp add: createObjects_def,wp createObjects_valid_pspace_untyped') apply (wp assms | simp add: objBits_def)+ apply (wp createObjects_sch createObjects_queues) apply (rule hoare_vcg_conj_lift) apply (simp add: createObjects_def) apply (wp createObjects_state_refs_of'') apply (rule hoare_vcg_conj_lift) apply (simp add: createObjects_def) apply (wp createObjects_iflive') apply (wp createObjects_no_cte_ifunsafe' irqs_masked_lift
             createObjects_idle' createObjects_no_cte_valid_global
             createObjects_valid_arch createObjects_irq_state
             createObjects_no_cte_irq_handlers createObjects_cur'
             createObjects_queues' [OF no_tcb]
             assms | simp add: objBits_def )+ apply (rule hoare_vcg_conj_lift) apply (simp add: createObjects_def) apply (wp createObjects_idle') apply (wp createObjects_no_cte_ifunsafe' irqs_masked_lift
             createObjects_idle' createObjects_no_cte_valid_global
             createObjects_valid_arch createObjects_irq_state
             createObjects_no_cte_irq_handlers createObjects_cur'
             createObjects_queues' [OF no_tcb] assms
             createObjects_pspace_domain_valid co_ct_not_inQ
             createObjects_ct_idle_or_in_cur_domain'
             createObjects_untyped_ranges_zero'[OF moKO]
         | simp)+ apply clarsimp apply ((intro conjI; assumption?); simp add: valid_pspace'_def objBits_def) apply (fastforce simp add: no_cte no_tcb split_def split: option.splits) apply (clarsimp simp: invs'_def no_tcb valid_state'_def no_cte  split: option.splits) done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. range_cover ptr sz (objBitsKO val + gbits) n \<and> n \<noteq> 0 \<and> invs' s \<and> ct_active' s \<and> pspace_no_overlap' ptr sz s \<and> ptr \<noteq> 0 \<and> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> kernel_data_refs = {} \<and> caps_overlap_reserved' {ptr..ptr + word_of_nat (n * 2 ^ gbits * 2 ^ objBitsKO val) - 1} s \<and> caps_no_overlap'' ptr sz s \<and> refs_of' val = {} \<and> \<not> live' val \<and> (\<forall>pde. projectKO_opt val = Some pde \<longrightarrow> pde = ARM_H.InvalidPDE)\<rbrace> createObjects ptr n val gbits \<lbrace>\<lambda>rv. invs'\<rbrace> proof (state)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. range_cover ptr sz (objBitsKO val + gbits) n \<and> n \<noteq> 0 \<and> invs' s \<and> ct_active' s \<and> pspace_no_overlap' ptr sz s \<and> ptr \<noteq> 0 \<and> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> kernel_data_refs = {} \<and> caps_overlap_reserved' {ptr..ptr + word_of_nat (n * 2 ^ gbits * 2 ^ objBitsKO val) - 1} s \<and> caps_no_overlap'' ptr sz s \<and> refs_of' val = {} \<and> \<not> live' val \<and> (\<forall>pde. projectKO_opt val = Some pde \<longrightarrow> pde = ARM_H.InvalidPDE)\<rbrace> createObjects ptr n val gbits \<lbrace>\<lambda>rv. invs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>range_cover ptr sz (objBitsKO val + gbits) n; n \<noteq> 0\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. ct_not_inQ s \<and> pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrace> createObjects ptr n val gbits \<lbrace>\<lambda>_. ct_not_inQ\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>range_cover ptr sz (objBitsKO val + gbits) n; 0 < n\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. (ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> obj_at' (Not \<circ> tcbQueued) (ksCurThread s) s) \<and> pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrace> createObjects ptr n val gbits \<lbrace>\<lambda>_ s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> obj_at' (Not \<circ> tcbQueued) (ksCurThread s) s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>range_cover ptr sz (objBitsKO val + gbits) n; 0 < n\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> obj_at' (Not \<circ> tcbQueued) (ksCurThread s) s \<and> pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrace> createObjects ptr n val gbits \<lbrace>\<lambda>_ s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> obj_at' (Not \<circ> tcbQueued) (ksCurThread s) s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>range_cover ptr sz (objBitsKO val + gbits) n; 0 < n\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. obj_at' (Not \<circ> tcbQueued) (ksCurThread s) s \<and> pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrace> createObjects ptr n val gbits \<lbrace>\<lambda>rv s. obj_at' (Not \<circ> tcbQueued) (ksCurThread s) s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrakk>range_cover ptr sz (objBitsKO val + gbits) n; 0 < n\<rbrakk> \<Longrightarrow> \<lbrace>?Q8\<rbrace> createObjects ptr n val gbits \<lbrace>\<lambda>rv s. obj_at' (Not \<circ> tcbQueued) (ksCurThread s) s\<rbrace>
 2. \<And>s. \<lbrakk>range_cover ptr sz (objBitsKO val + gbits) n; 0 < n; obj_at' (Not \<circ> tcbQueued) (ksCurThread s) s \<and> pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrakk> \<Longrightarrow> ?Q8 s proof (prove)
goal (2 subgoals):
 1. \<And>prev_s. \<lbrakk>range_cover ptr sz (objBitsKO val + gbits) n; 0 < n\<rbrakk> \<Longrightarrow> \<lbrace>?P11 prev_s\<rbrace> createObjects ptr n val gbits \<lbrace>\<lambda>rv. obj_at' (Not \<circ> tcbQueued) (ksCurThread prev_s)\<rbrace>
 2. \<And>s. \<lbrakk>range_cover ptr sz (objBitsKO val + gbits) n; 0 < n; obj_at' (Not \<circ> tcbQueued) (ksCurThread s) s \<and> pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrakk> \<Longrightarrow> ?P11 s s proof (prove)
goal (2 subgoals):
 1. \<And>prev_s. \<lbrakk>range_cover ptr sz (objBitsKO val + gbits) n; 0 < n\<rbrakk> \<Longrightarrow> n \<noteq> 0
 2. \<And>s. \<lbrakk>range_cover ptr sz (objBitsKO val + gbits) n; 0 < n; obj_at' (Not \<circ> tcbQueued) (ksCurThread s) s \<and> pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrakk> \<Longrightarrow> obj_at' (Not \<circ> tcbQueued) (ksCurThread s) s \<and> valid_pspace' s \<and> pspace_no_overlap' ptr sz s proof (prove)
goal:
No subgoals! proof (state)
this:
\<lbrakk>range_cover ptr sz (objBitsKO val + gbits) n; n \<noteq> 0\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. ct_not_inQ s \<and> pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrace> createObjects ptr n val gbits \<lbrace>\<lambda>_. ct_not_inQ\<rbrace>

goal (1 subgoal):
 1. \<lbrace>\<lambda>s. range_cover ptr sz (objBitsKO val + gbits) n \<and> n \<noteq> 0 \<and> invs' s \<and> ct_active' s \<and> pspace_no_overlap' ptr sz s \<and> ptr \<noteq> 0 \<and> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> kernel_data_refs = {} \<and> caps_overlap_reserved' {ptr..ptr + word_of_nat (n * 2 ^ gbits * 2 ^ objBitsKO val) - 1} s \<and> caps_no_overlap'' ptr sz s \<and> refs_of' val = {} \<and> \<not> live' val \<and> (\<forall>pde. projectKO_opt val = Some pde \<longrightarrow> pde = ARM_H.InvalidPDE)\<rbrace> createObjects ptr n val gbits \<lbrace>\<lambda>rv. invs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. range_cover ptr sz (objBitsKO val + gbits) n \<and> n \<noteq> 0 \<and> invs' s \<and> ct_active' s \<and> pspace_no_overlap' ptr sz s \<and> ptr \<noteq> 0 \<and> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> kernel_data_refs = {} \<and> caps_overlap_reserved' {ptr..ptr + word_of_nat (n * 2 ^ gbits * 2 ^ objBitsKO val) - 1} s \<and> caps_no_overlap'' ptr sz s \<and> refs_of' val = {} \<and> \<not> live' val \<and> (\<forall>pde. projectKO_opt val = Some pde \<longrightarrow> pde = ARM_H.InvalidPDE)\<rbrace> createObjects ptr n val gbits \<lbrace>\<lambda>rv. invs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>range_cover ptr sz (objBitsKO val + gbits) n; n \<noteq> 0\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. invs' s \<and> ct_active' s \<and> pspace_no_overlap' ptr sz s \<and> ptr \<noteq> 0 \<and> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> kernel_data_refs = {} \<and> caps_overlap_reserved' {ptr..ptr + word_of_nat (n * 2 ^ gbits * 2 ^ objBitsKO val) - 1} s \<and> caps_no_overlap'' ptr sz s \<and> refs_of' val = {} \<and> \<not> live' val \<and> (\<forall>pde. projectKO_opt val = Some pde \<longrightarrow> pde = ARM_H.InvalidPDE)\<rbrace> createObjects ptr n val gbits \<lbrace>\<lambda>rv. invs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>range_cover ptr sz (objBitsKO val + gbits) n; 0 < n\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. valid_pspace' s \<and> sch_act_wf (ksSchedulerAction s) s \<and> Invariants_H.valid_queues s \<and> sym_refs (state_refs_of' s) \<and> if_live_then_nonz_cap' s \<and> if_unsafe_then_cap' s \<and> valid_idle' s \<and> valid_global_refs' s \<and> valid_arch_state' s \<and> valid_irq_node' (irq_node' s) s \<and> valid_irq_handlers' s \<and> valid_irq_states' s \<and> valid_machine_state' s \<and> irqs_masked' s \<and> valid_queues' s \<and> ct_not_inQ s \<and> ct_idle_or_in_cur_domain' s \<and> valid_pde_mappings' s \<and> pspace_domain_valid s \<and> ksCurDomain s \<le> maxDomain \<and> ksDomSchedule s \<noteq> [] \<and> (\<forall>x\<in>set (ksDomSchedule s). dschDomain x \<le> maxDomain \<and> 0 < dschLength x) \<and> ksDomSchedule s = ksDomSchedule (KernelInit_H.newKernelState undefined) \<and> ksDomScheduleIdx s < length (ksDomSchedule (KernelInit_H.newKernelState undefined)) \<and> untyped_ranges_zero' s \<and> cur_tcb' s \<and> ct_active' s \<and> pspace_no_overlap' ptr sz s \<and> ptr \<noteq> 0 \<and> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> kernel_data_refs = {} \<and> caps_overlap_reserved' {ptr..ptr + word_of_nat n * 2 ^ gbits * 2 ^ objBitsKO val - 1} s \<and> caps_no_overlap'' ptr sz s \<and> refs_of' val = {} \<and> \<not> live' val \<and> (\<forall>pde. projectKO_opt val = Some pde \<longrightarrow> pde = ARM_H.InvalidPDE)\<rbrace> createObjects ptr n val gbits \<lbrace>\<lambda>rv. (\<lambda>s. valid_pspace' s \<and> sch_act_wf (ksSchedulerAction s) s \<and> Invariants_H.valid_queues s \<and> sym_refs (state_refs_of' s) \<and> if_live_then_nonz_cap' s \<and> if_unsafe_then_cap' s \<and> valid_idle' s \<and> valid_global_refs' s \<and> valid_arch_state' s \<and> valid_irq_node' (irq_node' s) s \<and> valid_irq_handlers' s \<and> valid_irq_states' s \<and> valid_machine_state' s \<and> irqs_masked' s \<and> valid_queues' s \<and> ct_not_inQ s \<and> ct_idle_or_in_cur_domain' s \<and> valid_pde_mappings' s \<and> pspace_domain_valid s \<and> ksCurDomain s \<le> maxDomain \<and> ksDomSchedule s \<noteq> [] \<and> (\<forall>x\<in>set (ksDomSchedule s). dschDomain x \<le> maxDomain \<and> 0 < dschLength x) \<and> ksDomSchedule s = ksDomSchedule (KernelInit_H.newKernelState undefined) \<and> ksDomScheduleIdx s < length (ksDomSchedule (KernelInit_H.newKernelState undefined)) \<and> untyped_ranges_zero' s) and cur_tcb'\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrakk>range_cover ptr sz (objBitsKO val + gbits) n; 0 < n\<rbrakk> \<Longrightarrow> \<lbrace>?Q4\<rbrace> createObjects ptr n val gbits \<lbrace>\<lambda>rv s. valid_pspace' s \<and> (sch_act_wf (ksSchedulerAction s) s \<and> Invariants_H.valid_queues s \<and> sym_refs (state_refs_of' s) \<and> if_live_then_nonz_cap' s \<and> if_unsafe_then_cap' s \<and> valid_idle' s \<and> valid_global_refs' s \<and> valid_arch_state' s \<and> valid_irq_node' (irq_node' s) s \<and> valid_irq_handlers' s \<and> valid_irq_states' s \<and> valid_machine_state' s \<and> irqs_masked' s \<and> valid_queues' s \<and> ct_not_inQ s \<and> ct_idle_or_in_cur_domain' s \<and> valid_pde_mappings' s \<and> pspace_domain_valid s \<and> ksCurDomain s \<le> maxDomain \<and> ksDomSchedule s \<noteq> [] \<and> (\<forall>x\<in>set (ksDomSchedule s). dschDomain x \<le> maxDomain \<and> 0 < dschLength x) \<and> ksDomSchedule s = ksDomSchedule (KernelInit_H.newKernelState undefined) \<and> ksDomScheduleIdx s < length (ksDomSchedule (KernelInit_H.newKernelState undefined)) \<and> untyped_ranges_zero' s) \<and> cur_tcb' s\<rbrace>
 2. \<And>s. \<lbrakk>range_cover ptr sz (objBitsKO val + gbits) n; 0 < n; valid_pspace' s \<and> sch_act_wf (ksSchedulerAction s) s \<and> Invariants_H.valid_queues s \<and> sym_refs (state_refs_of' s) \<and> if_live_then_nonz_cap' s \<and> if_unsafe_then_cap' s \<and> valid_idle' s \<and> valid_global_refs' s \<and> valid_arch_state' s \<and> valid_irq_node' (irq_node' s) s \<and> valid_irq_handlers' s \<and> valid_irq_states' s \<and> valid_machine_state' s \<and> irqs_masked' s \<and> valid_queues' s \<and> ct_not_inQ s \<and> ct_idle_or_in_cur_domain' s \<and> valid_pde_mappings' s \<and> pspace_domain_valid s \<and> ksCurDomain s \<le> maxDomain \<and> ksDomSchedule s \<noteq> [] \<and> (\<forall>x\<in>set (ksDomSchedule s). dschDomain x \<le> maxDomain \<and> 0 < dschLength x) \<and> ksDomSchedule s = ksDomSchedule (KernelInit_H.newKernelState undefined) \<and> ksDomScheduleIdx s < length (ksDomSchedule (KernelInit_H.newKernelState undefined)) \<and> untyped_ranges_zero' s \<and> cur_tcb' s \<and> ct_active' s \<and> pspace_no_overlap' ptr sz s \<and> ptr \<noteq> 0 \<and> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> kernel_data_refs = {} \<and> caps_overlap_reserved' {ptr..ptr + word_of_nat n * 2 ^ gbits * 2 ^ objBitsKO val - 1} s \<and> caps_no_overlap'' ptr sz s \<and> refs_of' val = {} \<and> \<not> live' val \<and> (\<forall>pde. projectKO_opt val = Some pde \<longrightarrow> pde = ARM_H.InvalidPDE)\<rbrakk> \<Longrightarrow> ?Q4 s proof (prove)
goal (3 subgoals):
 1. \<lbrakk>range_cover ptr sz (objBitsKO val + gbits) n; 0 < n\<rbrakk> \<Longrightarrow> \<lbrace>?Q7\<rbrace> createObjects ptr n val gbits \<lbrace>\<lambda>rv s. valid_pspace' s \<and> (sch_act_wf (ksSchedulerAction s) s \<and> Invariants_H.valid_queues s \<and> sym_refs (state_refs_of' s) \<and> if_live_then_nonz_cap' s \<and> if_unsafe_then_cap' s \<and> valid_idle' s \<and> valid_global_refs' s \<and> valid_arch_state' s \<and> valid_irq_node' (irq_node' s) s \<and> valid_irq_handlers' s \<and> valid_irq_states' s \<and> valid_machine_state' s \<and> irqs_masked' s \<and> valid_queues' s \<and> ct_not_inQ s \<and> ct_idle_or_in_cur_domain' s \<and> valid_pde_mappings' s \<and> pspace_domain_valid s \<and> ksCurDomain s \<le> maxDomain \<and> ksDomSchedule s \<noteq> [] \<and> (\<forall>x\<in>set (ksDomSchedule s). dschDomain x \<le> maxDomain \<and> 0 < dschLength x) \<and> ksDomSchedule s = ksDomSchedule (KernelInit_H.newKernelState undefined) \<and> ksDomScheduleIdx s < length (ksDomSchedule (KernelInit_H.newKernelState undefined)) \<and> untyped_ranges_zero' s) \<and> cur_tcb' s\<rbrace>
 2. \<And>s. \<lbrakk>range_cover ptr sz (objBitsKO val + gbits) n; 0 < n; ?Q4 s\<rbrakk> \<Longrightarrow> ?Q7 s
 3. \<And>s. \<lbrakk>range_cover ptr sz (objBitsKO val + gbits) n; 0 < n; valid_pspace' s \<and> sch_act_wf (ksSchedulerAction s) s \<and> Invariants_H.valid_queues s \<and> sym_refs (state_refs_of' s) \<and> if_live_then_nonz_cap' s \<and> if_unsafe_then_cap' s \<and> valid_idle' s \<and> valid_global_refs' s \<and> valid_arch_state' s \<and> valid_irq_node' (irq_node' s) s \<and> valid_irq_handlers' s \<and> valid_irq_states' s \<and> valid_machine_state' s \<and> irqs_masked' s \<and> valid_queues' s \<and> ct_not_inQ s \<and> ct_idle_or_in_cur_domain' s \<and> valid_pde_mappings' s \<and> pspace_domain_valid s \<and> ksCurDomain s \<le> maxDomain \<and> ksDomSchedule s \<noteq> [] \<and> (\<forall>x\<in>set (ksDomSchedule s). dschDomain x \<le> maxDomain \<and> 0 < dschLength x) \<and> ksDomSchedule s = ksDomSchedule (KernelInit_H.newKernelState undefined) \<and> ksDomScheduleIdx s < length (ksDomSchedule (KernelInit_H.newKernelState undefined)) \<and> untyped_ranges_zero' s \<and> cur_tcb' s \<and> ct_active' s \<and> pspace_no_overlap' ptr sz s \<and> ptr \<noteq> 0 \<and> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> kernel_data_refs = {} \<and> caps_overlap_reserved' {ptr..ptr + word_of_nat n * 2 ^ gbits * 2 ^ objBitsKO val - 1} s \<and> caps_no_overlap'' ptr sz s \<and> refs_of' val = {} \<and> \<not> live' val \<and> (\<forall>pde. projectKO_opt val = Some pde \<longrightarrow> pde = ARM_H.InvalidPDE)\<rbrakk> \<Longrightarrow> ?Q4 s proof (prove)
goal (4 subgoals):
 1. \<lbrakk>range_cover ptr sz (objBitsKO val + gbits) n; 0 < n\<rbrakk> \<Longrightarrow> \<lbrace>?P10\<rbrace> createObjects ptr n val gbits \<lbrace>\<lambda>rv. valid_pspace'\<rbrace>
 2. \<lbrakk>range_cover ptr sz (objBitsKO val + gbits) n; 0 < n\<rbrakk> \<Longrightarrow> \<lbrace>?P'10\<rbrace> createObjects ptr n val gbits \<lbrace>\<lambda>rv s. (sch_act_wf (ksSchedulerAction s) s \<and> Invariants_H.valid_queues s \<and> sym_refs (state_refs_of' s) \<and> if_live_then_nonz_cap' s \<and> if_unsafe_then_cap' s \<and> valid_idle' s \<and> valid_global_refs' s \<and> valid_arch_state' s \<and> valid_irq_node' (irq_node' s) s \<and> valid_irq_handlers' s \<and> valid_irq_states' s \<and> valid_machine_state' s \<and> irqs_masked' s \<and> valid_queues' s \<and> ct_not_inQ s \<and> ct_idle_or_in_cur_domain' s \<and> valid_pde_mappings' s \<and> pspace_domain_valid s \<and> ksCurDomain s \<le> maxDomain \<and> ksDomSchedule s \<noteq> [] \<and> (\<forall>x\<in>set (ksDomSchedule s). dschDomain x \<le> maxDomain \<and> 0 < dschLength x) \<and> ksDomSchedule s = ksDomSchedule (KernelInit_H.newKernelState undefined) \<and> ksDomScheduleIdx s < length (ksDomSchedule (KernelInit_H.newKernelState undefined)) \<and> untyped_ranges_zero' s) \<and> cur_tcb' s\<rbrace>
 3. \<And>s. \<lbrakk>range_cover ptr sz (objBitsKO val + gbits) n; 0 < n; ?Q4 s\<rbrakk> \<Longrightarrow> ?P10 s \<and> ?P'10 s
 4. \<And>s. \<lbrakk>range_cover ptr sz (objBitsKO val + gbits) n; 0 < n; valid_pspace' s \<and> sch_act_wf (ksSchedulerAction s) s \<and> Invariants_H.valid_queues s \<and> sym_refs (state_refs_of' s) \<and> if_live_then_nonz_cap' s \<and> if_unsafe_then_cap' s \<and> valid_idle' s \<and> valid_global_refs' s \<and> valid_arch_state' s \<and> valid_irq_node' (irq_node' s) s \<and> valid_irq_handlers' s \<and> valid_irq_states' s \<and> valid_machine_state' s \<and> irqs_masked' s \<and> valid_queues' s \<and> ct_not_inQ s \<and> ct_idle_or_in_cur_domain' s \<and> valid_pde_mappings' s \<and> pspace_domain_valid s \<and> ksCurDomain s \<le> maxDomain \<and> ksDomSchedule s \<noteq> [] \<and> (\<forall>x\<in>set (ksDomSchedule s). dschDomain x \<le> maxDomain \<and> 0 < dschLength x) \<and> ksDomSchedule s = ksDomSchedule (KernelInit_H.newKernelState undefined) \<and> ksDomScheduleIdx s < length (ksDomSchedule (KernelInit_H.newKernelState undefined)) \<and> untyped_ranges_zero' s \<and> cur_tcb' s \<and> ct_active' s \<and> pspace_no_overlap' ptr sz s \<and> ptr \<noteq> 0 \<and> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> kernel_data_refs = {} \<and> caps_overlap_reserved' {ptr..ptr + word_of_nat n * 2 ^ gbits * 2 ^ objBitsKO val - 1} s \<and> caps_no_overlap'' ptr sz s \<and> refs_of' val = {} \<and> \<not> live' val \<and> (\<forall>pde. projectKO_opt val = Some pde \<longrightarrow> pde = ARM_H.InvalidPDE)\<rbrakk> \<Longrightarrow> ?Q4 s proof (prove)
goal (6 subgoals):
 1. \<lbrakk>range_cover ptr sz (objBitsKO val + gbits) n; 0 < n\<rbrakk> \<Longrightarrow> makeObjectKO ?dev16 ?ty16 = Some val
 2. \<lbrakk>range_cover ptr sz (objBitsKO val + gbits) n; 0 < n\<rbrakk> \<Longrightarrow> n \<noteq> 0
 3. \<lbrakk>range_cover ptr sz (objBitsKO val + gbits) n; 0 < n\<rbrakk> \<Longrightarrow> range_cover ptr ?sz16 (objBitsKO val + gbits) n
 4. \<lbrakk>range_cover ptr sz (objBitsKO val + gbits) n; 0 < n\<rbrakk> \<Longrightarrow> \<lbrace>?P'10\<rbrace> createObjects ptr n val gbits \<lbrace>\<lambda>rv s. (sch_act_wf (ksSchedulerAction s) s \<and> Invariants_H.valid_queues s \<and> sym_refs (state_refs_of' s) \<and> if_live_then_nonz_cap' s \<and> if_unsafe_then_cap' s \<and> valid_idle' s \<and> valid_global_refs' s \<and> valid_arch_state' s \<and> valid_irq_node' (irq_node' s) s \<and> valid_irq_handlers' s \<and> valid_irq_states' s \<and> valid_machine_state' s \<and> irqs_masked' s \<and> valid_queues' s \<and> ct_not_inQ s \<and> ct_idle_or_in_cur_domain' s \<and> valid_pde_mappings' s \<and> pspace_domain_valid s \<and> ksCurDomain s \<le> maxDomain \<and> ksDomSchedule s \<noteq> [] \<and> (\<forall>x\<in>set (ksDomSchedule s). dschDomain x \<le> maxDomain \<and> 0 < dschLength x) \<and> ksDomSchedule s = ksDomSchedule (KernelInit_H.newKernelState undefined) \<and> ksDomScheduleIdx s < length (ksDomSchedule (KernelInit_H.newKernelState undefined)) \<and> untyped_ranges_zero' s) \<and> cur_tcb' s\<rbrace>
 5. \<And>s. \<lbrakk>range_cover ptr sz (objBitsKO val + gbits) n; 0 < n; ?Q4 s\<rbrakk> \<Longrightarrow> (pspace_no_overlap' ptr ?sz16 s \<and> valid_pspace' s \<and> caps_no_overlap'' ptr ?sz16 s \<and> ptr \<noteq> 0 \<and> caps_overlap_reserved' {ptr..ptr + word_of_nat (n * 2 ^ gbits * 2 ^ objBitsKO val) - 1} s) \<and> ?P'10 s
 6. \<And>s. \<lbrakk>range_cover ptr sz (objBitsKO val + gbits) n; 0 < n; valid_pspace' s \<and> sch_act_wf (ksSchedulerAction s) s \<and> Invariants_H.valid_queues s \<and> sym_refs (state_refs_of' s) \<and> if_live_then_nonz_cap' s \<and> if_unsafe_then_cap' s \<and> valid_idle' s \<and> valid_global_refs' s \<and> valid_arch_state' s \<and> valid_irq_node' (irq_node' s) s \<and> valid_irq_handlers' s \<and> valid_irq_states' s \<and> valid_machine_state' s \<and> irqs_masked' s \<and> valid_queues' s \<and> ct_not_inQ s \<and> ct_idle_or_in_cur_domain' s \<and> valid_pde_mappings' s \<and> pspace_domain_valid s \<and> ksCurDomain s \<le> maxDomain \<and> ksDomSchedule s \<noteq> [] \<and> (\<forall>x\<in>set (ksDomSchedule s). dschDomain x \<le> maxDomain \<and> 0 < dschLength x) \<and> ksDomSchedule s = ksDomSchedule (KernelInit_H.newKernelState undefined) \<and> ksDomScheduleIdx s < length (ksDomSchedule (KernelInit_H.newKernelState undefined)) \<and> untyped_ranges_zero' s \<and> cur_tcb' s \<and> ct_active' s \<and> pspace_no_overlap' ptr sz s \<and> ptr \<noteq> 0 \<and> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> kernel_data_refs = {} \<and> caps_overlap_reserved' {ptr..ptr + word_of_nat n * 2 ^ gbits * 2 ^ objBitsKO val - 1} s \<and> caps_no_overlap'' ptr sz s \<and> refs_of' val = {} \<and> \<not> live' val \<and> (\<forall>pde. projectKO_opt val = Some pde \<longrightarrow> pde = ARM_H.InvalidPDE)\<rbrakk> \<Longrightarrow> ?Q4 s proof (prove)
goal (3 subgoals):
 1. \<lbrakk>range_cover ptr sz (objBitsKO val + gbits) n; 0 < n\<rbrakk> \<Longrightarrow> \<lbrace>?P'10\<rbrace> createObjects ptr n val gbits \<lbrace>\<lambda>rv s. sch_act_wf (ksSchedulerAction s) s \<and> Invariants_H.valid_queues s \<and> sym_refs (state_refs_of' s) \<and> if_live_then_nonz_cap' s \<and> if_unsafe_then_cap' s \<and> valid_idle' s \<and> valid_global_refs' s \<and> valid_arch_state' s \<and> valid_irq_node' (irq_node' s) s \<and> valid_irq_handlers' s \<and> valid_irq_states' s \<and> valid_machine_state' s \<and> irqs_masked' s \<and> valid_queues' s \<and> ct_not_inQ s \<and> ct_idle_or_in_cur_domain' s \<and> valid_pde_mappings' s \<and> pspace_domain_valid s \<and> ksCurDomain s \<le> maxDomain \<and> ksDomSchedule s \<noteq> [] \<and> (\<forall>x\<in>set (ksDomSchedule s). dschDomain x \<le> maxDomain \<and> 0 < dschLength x) \<and> ksDomSchedule s = ksDomSchedule (KernelInit_H.newKernelState undefined) \<and> ksDomScheduleIdx s < length (ksDomSchedule (KernelInit_H.newKernelState undefined)) \<and> untyped_ranges_zero' s \<and> cur_tcb' s\<rbrace>
 2. \<And>s. \<lbrakk>range_cover ptr sz (objBitsKO val + gbits) n; 0 < n; ?Q4 s\<rbrakk> \<Longrightarrow> (pspace_no_overlap' ptr sz s \<and> valid_pspace' s \<and> caps_no_overlap'' ptr sz s \<and> ptr \<noteq> 0 \<and> caps_overlap_reserved' {ptr..ptr + word_of_nat (n * 2 ^ gbits * 2 ^ objBitsKO val) - 1} s) \<and> ?P'10 s
 3. \<And>s. \<lbrakk>range_cover ptr sz (objBitsKO val + gbits) n; 0 < n; valid_pspace' s \<and> sch_act_wf (ksSchedulerAction s) s \<and> Invariants_H.valid_queues s \<and> sym_refs (state_refs_of' s) \<and> if_live_then_nonz_cap' s \<and> if_unsafe_then_cap' s \<and> valid_idle' s \<and> valid_global_refs' s \<and> valid_arch_state' s \<and> valid_irq_node' (irq_node' s) s \<and> valid_irq_handlers' s \<and> valid_irq_states' s \<and> valid_machine_state' s \<and> irqs_masked' s \<and> valid_queues' s \<and> ct_not_inQ s \<and> ct_idle_or_in_cur_domain' s \<and> valid_pde_mappings' s \<and> pspace_domain_valid s \<and> ksCurDomain s \<le> maxDomain \<and> ksDomSchedule s \<noteq> [] \<and> (\<forall>x\<in>set (ksDomSchedule s). dschDomain x \<le> maxDomain \<and> 0 < dschLength x) \<and> ksDomSchedule s = ksDomSchedule (KernelInit_H.newKernelState undefined) \<and> ksDomScheduleIdx s < length (ksDomSchedule (KernelInit_H.newKernelState undefined)) \<and> untyped_ranges_zero' s \<and> cur_tcb' s \<and> ct_active' s \<and> pspace_no_overlap' ptr sz s \<and> ptr \<noteq> 0 \<and> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> kernel_data_refs = {} \<and> caps_overlap_reserved' {ptr..ptr + word_of_nat n * 2 ^ gbits * 2 ^ objBitsKO val - 1} s \<and> caps_no_overlap'' ptr sz s \<and> refs_of' val = {} \<and> \<not> live' val \<and> (\<forall>pde. projectKO_opt val = Some pde \<longrightarrow> pde = ARM_H.InvalidPDE)\<rbrakk> \<Longrightarrow> ?Q4 s proof (prove)
goal (3 subgoals):
 1. \<lbrakk>range_cover ptr sz (objBitsKO val + gbits) n; 0 < n\<rbrakk> \<Longrightarrow> \<lbrace>?P'26\<rbrace> createObjects ptr n val gbits \<lbrace>\<lambda>rv s. sym_refs (state_refs_of' s) \<and> if_live_then_nonz_cap' s \<and> if_unsafe_then_cap' s \<and> valid_idle' s \<and> valid_global_refs' s \<and> valid_arch_state' s \<and> valid_irq_node' (irq_node' s) s \<and> valid_irq_handlers' s \<and> valid_irq_states' s \<and> valid_machine_state' s \<and> irqs_masked' s \<and> valid_queues' s \<and> ct_not_inQ s \<and> ct_idle_or_in_cur_domain' s \<and> valid_pde_mappings' s \<and> pspace_domain_valid s \<and> ksCurDomain s \<le> maxDomain \<and> ksDomSchedule s \<noteq> [] \<and> (\<forall>x\<in>set (ksDomSchedule s). dschDomain x \<le> maxDomain \<and> 0 < dschLength x) \<and> ksDomSchedule s = ksDomSchedule (KernelInit_H.newKernelState undefined) \<and> ksDomScheduleIdx s < length (ksDomSchedule (KernelInit_H.newKernelState undefined)) \<and> untyped_ranges_zero' s \<and> cur_tcb' s\<rbrace>
 2. \<And>s. \<lbrakk>range_cover ptr sz (objBitsKO val + gbits) n; 0 < n; ?Q4 s\<rbrakk> \<Longrightarrow> (pspace_no_overlap' ptr sz s \<and> valid_pspace' s \<and> caps_no_overlap'' ptr sz s \<and> ptr \<noteq> 0 \<and> caps_overlap_reserved' {ptr..ptr + word_of_nat (n * 2 ^ gbits * 2 ^ objBitsKO val) - 1} s) \<and> ((\<lambda>s. sch_act_wf (ksSchedulerAction s) s) and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr ?sz25 and K (range_cover ptr ?sz25 (objBitsKO val + gbits) n \<and> n \<noteq> 0)) s \<and> (Invariants_H.valid_queues s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr ?sz27 s \<and> range_cover ptr ?sz27 (objBitsKO val + gbits) n \<and> n \<noteq> 0) \<and> ?P'26 s
 3. \<And>s. \<lbrakk>range_cover ptr sz (objBitsKO val + gbits) n; 0 < n; valid_pspace' s \<and> sch_act_wf (ksSchedulerAction s) s \<and> Invariants_H.valid_queues s \<and> sym_refs (state_refs_of' s) \<and> if_live_then_nonz_cap' s \<and> if_unsafe_then_cap' s \<and> valid_idle' s \<and> valid_global_refs' s \<and> valid_arch_state' s \<and> valid_irq_node' (irq_node' s) s \<and> valid_irq_handlers' s \<and> valid_irq_states' s \<and> valid_machine_state' s \<and> irqs_masked' s \<and> valid_queues' s \<and> ct_not_inQ s \<and> ct_idle_or_in_cur_domain' s \<and> valid_pde_mappings' s \<and> pspace_domain_valid s \<and> ksCurDomain s \<le> maxDomain \<and> ksDomSchedule s \<noteq> [] \<and> (\<forall>x\<in>set (ksDomSchedule s). dschDomain x \<le> maxDomain \<and> 0 < dschLength x) \<and> ksDomSchedule s = ksDomSchedule (KernelInit_H.newKernelState undefined) \<and> ksDomScheduleIdx s < length (ksDomSchedule (KernelInit_H.newKernelState undefined)) \<and> untyped_ranges_zero' s \<and> cur_tcb' s \<and> ct_active' s \<and> pspace_no_overlap' ptr sz s \<and> ptr \<noteq> 0 \<and> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> kernel_data_refs = {} \<and> caps_overlap_reserved' {ptr..ptr + word_of_nat n * 2 ^ gbits * 2 ^ objBitsKO val - 1} s \<and> caps_no_overlap'' ptr sz s \<and> refs_of' val = {} \<and> \<not> live' val \<and> (\<forall>pde. projectKO_opt val = Some pde \<longrightarrow> pde = ARM_H.InvalidPDE)\<rbrakk> \<Longrightarrow> ?Q4 s proof (prove)
goal (4 subgoals):
 1. \<lbrakk>range_cover ptr sz (objBitsKO val + gbits) n; 0 < n\<rbrakk> \<Longrightarrow> \<lbrace>?P29\<rbrace> createObjects ptr n val gbits \<lbrace>\<lambda>rv s. sym_refs (state_refs_of' s)\<rbrace>
 2. \<lbrakk>range_cover ptr sz (objBitsKO val + gbits) n; 0 < n\<rbrakk> \<Longrightarrow> \<lbrace>?P'29\<rbrace> createObjects ptr n val gbits \<lbrace>\<lambda>rv s. if_live_then_nonz_cap' s \<and> if_unsafe_then_cap' s \<and> valid_idle' s \<and> valid_global_refs' s \<and> valid_arch_state' s \<and> valid_irq_node' (irq_node' s) s \<and> valid_irq_handlers' s \<and> valid_irq_states' s \<and> valid_machine_state' s \<and> irqs_masked' s \<and> valid_queues' s \<and> ct_not_inQ s \<and> ct_idle_or_in_cur_domain' s \<and> valid_pde_mappings' s \<and> pspace_domain_valid s \<and> ksCurDomain s \<le> maxDomain \<and> ksDomSchedule s \<noteq> [] \<and> (\<forall>x\<in>set (ksDomSchedule s). dschDomain x \<le> maxDomain \<and> 0 < dschLength x) \<and> ksDomSchedule s = ksDomSchedule (KernelInit_H.newKernelState undefined) \<and> ksDomScheduleIdx s < length (ksDomSchedule (KernelInit_H.newKernelState undefined)) \<and> untyped_ranges_zero' s \<and> cur_tcb' s\<rbrace>
 3. \<And>s. \<lbrakk>range_cover ptr sz (objBitsKO val + gbits) n; 0 < n; ?Q4 s\<rbrakk> \<Longrightarrow> (pspace_no_overlap' ptr sz s \<and> valid_pspace' s \<and> caps_no_overlap'' ptr sz s \<and> ptr \<noteq> 0 \<and> caps_overlap_reserved' {ptr..ptr + word_of_nat (n * 2 ^ gbits * 2 ^ objBitsKO val) - 1} s) \<and> ((\<lambda>s. sch_act_wf (ksSchedulerAction s) s) and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr ?sz25 and K (range_cover ptr ?sz25 (objBitsKO val + gbits) n \<and> n \<noteq> 0)) s \<and> (Invariants_H.valid_queues s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr ?sz27 s \<and> range_cover ptr ?sz27 (objBitsKO val + gbits) n \<and> n \<noteq> 0) \<and> ?P29 s \<and> ?P'29 s
 4. \<And>s. \<lbrakk>range_cover ptr sz (objBitsKO val + gbits) n; 0 < n; valid_pspace' s \<and> sch_act_wf (ksSchedulerAction s) s \<and> Invariants_H.valid_queues s \<and> sym_refs (state_refs_of' s) \<and> if_live_then_nonz_cap' s \<and> if_unsafe_then_cap' s \<and> valid_idle' s \<and> valid_global_refs' s \<and> valid_arch_state' s \<and> valid_irq_node' (irq_node' s) s \<and> valid_irq_handlers' s \<and> valid_irq_states' s \<and> valid_machine_state' s \<and> irqs_masked' s \<and> valid_queues' s \<and> ct_not_inQ s \<and> ct_idle_or_in_cur_domain' s \<and> valid_pde_mappings' s \<and> pspace_domain_valid s \<and> ksCurDomain s \<le> maxDomain \<and> ksDomSchedule s \<noteq> [] \<and> (\<forall>x\<in>set (ksDomSchedule s). dschDomain x \<le> maxDomain \<and> 0 < dschLength x) \<and> ksDomSchedule s = ksDomSchedule (KernelInit_H.newKernelState undefined) \<and> ksDomScheduleIdx s < length (ksDomSchedule (KernelInit_H.newKernelState undefined)) \<and> untyped_ranges_zero' s \<and> cur_tcb' s \<and> ct_active' s \<and> pspace_no_overlap' ptr sz s \<and> ptr \<noteq> 0 \<and> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> kernel_data_refs = {} \<and> caps_overlap_reserved' {ptr..ptr + word_of_nat n * 2 ^ gbits * 2 ^ objBitsKO val - 1} s \<and> caps_no_overlap'' ptr sz s \<and> refs_of' val = {} \<and> \<not> live' val \<and> (\<forall>pde. projectKO_opt val = Some pde \<longrightarrow> pde = ARM_H.InvalidPDE)\<rbrakk> \<Longrightarrow> ?Q4 s proof (prove)
goal (4 subgoals):
 1. \<lbrakk>range_cover ptr sz (objBitsKO val + gbits) n; 0 < n\<rbrakk> \<Longrightarrow> \<lbrace>?P29\<rbrace> do y <- createObjects' ptr n val gbits;
return (map (\<lambda>n. ptr + (n << objBitsKO val + gbits)) [0 .e. word_of_nat n - 1])
od \<lbrace>\<lambda>rv s. sym_refs (state_refs_of' s)\<rbrace>
 2. \<lbrakk>range_cover ptr sz (objBitsKO val + gbits) n; 0 < n\<rbrakk> \<Longrightarrow> \<lbrace>?P'29\<rbrace> createObjects ptr n val gbits \<lbrace>\<lambda>rv s. if_live_then_nonz_cap' s \<and> if_unsafe_then_cap' s \<and> valid_idle' s \<and> valid_global_refs' s \<and> valid_arch_state' s \<and> valid_irq_node' (irq_node' s) s \<and> valid_irq_handlers' s \<and> valid_irq_states' s \<and> valid_machine_state' s \<and> irqs_masked' s \<and> valid_queues' s \<and> ct_not_inQ s \<and> ct_idle_or_in_cur_domain' s \<and> valid_pde_mappings' s \<and> pspace_domain_valid s \<and> ksCurDomain s \<le> maxDomain \<and> ksDomSchedule s \<noteq> [] \<and> (\<forall>x\<in>set (ksDomSchedule s). dschDomain x \<le> maxDomain \<and> 0 < dschLength x) \<and> ksDomSchedule s = ksDomSchedule (KernelInit_H.newKernelState undefined) \<and> ksDomScheduleIdx s < length (ksDomSchedule (KernelInit_H.newKernelState undefined)) \<and> untyped_ranges_zero' s \<and> cur_tcb' s\<rbrace>
 3. \<And>s. \<lbrakk>range_cover ptr sz (objBitsKO val + gbits) n; 0 < n; ?Q4 s\<rbrakk> \<Longrightarrow> (pspace_no_overlap' ptr sz s \<and> valid_pspace' s \<and> caps_no_overlap'' ptr sz s \<and> ptr \<noteq> 0 \<and> caps_overlap_reserved' {ptr..ptr + word_of_nat (n * 2 ^ gbits * 2 ^ objBitsKO val) - 1} s) \<and> ((\<lambda>s. sch_act_wf (ksSchedulerAction s) s) and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr ?sz25 and K (range_cover ptr ?sz25 (objBitsKO val + gbits) n \<and> n \<noteq> 0)) s \<and> (Invariants_H.valid_queues s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr ?sz27 s \<and> range_cover ptr ?sz27 (objBitsKO val + gbits) n \<and> n \<noteq> 0) \<and> ?P29 s \<and> ?P'29 s
 4. \<And>s. \<lbrakk>range_cover ptr sz (objBitsKO val + gbits) n; 0 < n; valid_pspace' s \<and> sch_act_wf (ksSchedulerAction s) s \<and> Invariants_H.valid_queues s \<and> sym_refs (state_refs_of' s) \<and> if_live_then_nonz_cap' s \<and> if_unsafe_then_cap' s \<and> valid_idle' s \<and> valid_global_refs' s \<and> valid_arch_state' s \<and> valid_irq_node' (irq_node' s) s \<and> valid_irq_handlers' s \<and> valid_irq_states' s \<and> valid_machine_state' s \<and> irqs_masked' s \<and> valid_queues' s \<and> ct_not_inQ s \<and> ct_idle_or_in_cur_domain' s \<and> valid_pde_mappings' s \<and> pspace_domain_valid s \<and> ksCurDomain s \<le> maxDomain \<and> ksDomSchedule s \<noteq> [] \<and> (\<forall>x\<in>set (ksDomSchedule s). dschDomain x \<le> maxDomain \<and> 0 < dschLength x) \<and> ksDomSchedule s = ksDomSchedule (KernelInit_H.newKernelState undefined) \<and> ksDomScheduleIdx s < length (ksDomSchedule (KernelInit_H.newKernelState undefined)) \<and> untyped_ranges_zero' s \<and> cur_tcb' s \<and> ct_active' s \<and> pspace_no_overlap' ptr sz s \<and> ptr \<noteq> 0 \<and> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> kernel_data_refs = {} \<and> caps_overlap_reserved' {ptr..ptr + word_of_nat n * 2 ^ gbits * 2 ^ objBitsKO val - 1} s \<and> caps_no_overlap'' ptr sz s \<and> refs_of' val = {} \<and> \<not> live' val \<and> (\<forall>pde. projectKO_opt val = Some pde \<longrightarrow> pde = ARM_H.InvalidPDE)\<rbrakk> \<Longrightarrow> ?Q4 s proof (prove)
goal (3 subgoals):
 1. \<lbrakk>range_cover ptr sz (objBitsKO val + gbits) n; 0 < n\<rbrakk> \<Longrightarrow> \<lbrace>?P'29\<rbrace> createObjects ptr n val gbits \<lbrace>\<lambda>rv s. if_live_then_nonz_cap' s \<and> if_unsafe_then_cap' s \<and> valid_idle' s \<and> valid_global_refs' s \<and> valid_arch_state' s \<and> valid_irq_node' (irq_node' s) s \<and> valid_irq_handlers' s \<and> valid_irq_states' s \<and> valid_machine_state' s \<and> irqs_masked' s \<and> valid_queues' s \<and> ct_not_inQ s \<and> ct_idle_or_in_cur_domain' s \<and> valid_pde_mappings' s \<and> pspace_domain_valid s \<and> ksCurDomain s \<le> maxDomain \<and> ksDomSchedule s \<noteq> [] \<and> (\<forall>x\<in>set (ksDomSchedule s). dschDomain x \<le> maxDomain \<and> 0 < dschLength x) \<and> ksDomSchedule s = ksDomSchedule (KernelInit_H.newKernelState undefined) \<and> ksDomScheduleIdx s < length (ksDomSchedule (KernelInit_H.newKernelState undefined)) \<and> untyped_ranges_zero' s \<and> cur_tcb' s\<rbrace>
 2. \<And>s. \<lbrakk>range_cover ptr sz (objBitsKO val + gbits) n; 0 < n; ?Q4 s\<rbrakk> \<Longrightarrow> (pspace_no_overlap' ptr sz s \<and> valid_pspace' s \<and> caps_no_overlap'' ptr sz s \<and> ptr \<noteq> 0 \<and> caps_overlap_reserved' {ptr..ptr + word_of_nat (n * 2 ^ gbits * 2 ^ objBitsKO val) - 1} s) \<and> ((\<lambda>s. sch_act_wf (ksSchedulerAction s) s) and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr ?sz25 and K (range_cover ptr ?sz25 (objBitsKO val + gbits) n \<and> n \<noteq> 0)) s \<and> (Invariants_H.valid_queues s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr ?sz27 s \<and> range_cover ptr ?sz27 (objBitsKO val + gbits) n \<and> n \<noteq> 0) \<and> (n \<noteq> 0 \<and> range_cover ptr ?sz35 (objBitsKO val + gbits) n \<and> sym_refs (state_refs_of' s) \<and> refs_of' val = {} \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr ?sz35 s) \<and> ?P'29 s
 3. \<And>s. \<lbrakk>range_cover ptr sz (objBitsKO val + gbits) n; 0 < n; valid_pspace' s \<and> sch_act_wf (ksSchedulerAction s) s \<and> Invariants_H.valid_queues s \<and> sym_refs (state_refs_of' s) \<and> if_live_then_nonz_cap' s \<and> if_unsafe_then_cap' s \<and> valid_idle' s \<and> valid_global_refs' s \<and> valid_arch_state' s \<and> valid_irq_node' (irq_node' s) s \<and> valid_irq_handlers' s \<and> valid_irq_states' s \<and> valid_machine_state' s \<and> irqs_masked' s \<and> valid_queues' s \<and> ct_not_inQ s \<and> ct_idle_or_in_cur_domain' s \<and> valid_pde_mappings' s \<and> pspace_domain_valid s \<and> ksCurDomain s \<le> maxDomain \<and> ksDomSchedule s \<noteq> [] \<and> (\<forall>x\<in>set (ksDomSchedule s). dschDomain x \<le> maxDomain \<and> 0 < dschLength x) \<and> ksDomSchedule s = ksDomSchedule (KernelInit_H.newKernelState undefined) \<and> ksDomScheduleIdx s < length (ksDomSchedule (KernelInit_H.newKernelState undefined)) \<and> untyped_ranges_zero' s \<and> cur_tcb' s \<and> ct_active' s \<and> pspace_no_overlap' ptr sz s \<and> ptr \<noteq> 0 \<and> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> kernel_data_refs = {} \<and> caps_overlap_reserved' {ptr..ptr + word_of_nat n * 2 ^ gbits * 2 ^ objBitsKO val - 1} s \<and> caps_no_overlap'' ptr sz s \<and> refs_of' val = {} \<and> \<not> live' val \<and> (\<forall>pde. projectKO_opt val = Some pde \<longrightarrow> pde = ARM_H.InvalidPDE)\<rbrakk> \<Longrightarrow> ?Q4 s proof (prove)
goal (4 subgoals):
 1. \<lbrakk>range_cover ptr sz (objBitsKO val + gbits) n; 0 < n\<rbrakk> \<Longrightarrow> \<lbrace>?P38\<rbrace> createObjects ptr n val gbits \<lbrace>\<lambda>rv. if_live_then_nonz_cap'\<rbrace>
 2. \<lbrakk>range_cover ptr sz (objBitsKO val + gbits) n; 0 < n\<rbrakk> \<Longrightarrow> \<lbrace>?P'38\<rbrace> createObjects ptr n val gbits \<lbrace>\<lambda>rv s. if_unsafe_then_cap' s \<and> valid_idle' s \<and> valid_global_refs' s \<and> valid_arch_state' s \<and> valid_irq_node' (irq_node' s) s \<and> valid_irq_handlers' s \<and> valid_irq_states' s \<and> valid_machine_state' s \<and> irqs_masked' s \<and> valid_queues' s \<and> ct_not_inQ s \<and> ct_idle_or_in_cur_domain' s \<and> valid_pde_mappings' s \<and> pspace_domain_valid s \<and> ksCurDomain s \<le> maxDomain \<and> ksDomSchedule s \<noteq> [] \<and> (\<forall>x\<in>set (ksDomSchedule s). dschDomain x \<le> maxDomain \<and> 0 < dschLength x) \<and> ksDomSchedule s = ksDomSchedule (KernelInit_H.newKernelState undefined) \<and> ksDomScheduleIdx s < length (ksDomSchedule (KernelInit_H.newKernelState undefined)) \<and> untyped_ranges_zero' s \<and> cur_tcb' s\<rbrace>
 3. \<And>s. \<lbrakk>range_cover ptr sz (objBitsKO val + gbits) n; 0 < n; ?Q4 s\<rbrakk> \<Longrightarrow> (pspace_no_overlap' ptr sz s \<and> valid_pspace' s \<and> caps_no_overlap'' ptr sz s \<and> ptr \<noteq> 0 \<and> caps_overlap_reserved' {ptr..ptr + word_of_nat (n * 2 ^ gbits * 2 ^ objBitsKO val) - 1} s) \<and> ((\<lambda>s. sch_act_wf (ksSchedulerAction s) s) and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr ?sz25 and K (range_cover ptr ?sz25 (objBitsKO val + gbits) n \<and> n \<noteq> 0)) s \<and> (Invariants_H.valid_queues s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr ?sz27 s \<and> range_cover ptr ?sz27 (objBitsKO val + gbits) n \<and> n \<noteq> 0) \<and> (n \<noteq> 0 \<and> range_cover ptr ?sz35 (objBitsKO val + gbits) n \<and> sym_refs (state_refs_of' s) \<and> refs_of' val = {} \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr ?sz35 s) \<and> ?P38 s \<and> ?P'38 s
 4. \<And>s. \<lbrakk>range_cover ptr sz (objBitsKO val + gbits) n; 0 < n; valid_pspace' s \<and> sch_act_wf (ksSchedulerAction s) s \<and> Invariants_H.valid_queues s \<and> sym_refs (state_refs_of' s) \<and> if_live_then_nonz_cap' s \<and> if_unsafe_then_cap' s \<and> valid_idle' s \<and> valid_global_refs' s \<and> valid_arch_state' s \<and> valid_irq_node' (irq_node' s) s \<and> valid_irq_handlers' s \<and> valid_irq_states' s \<and> valid_machine_state' s \<and> irqs_masked' s \<and> valid_queues' s \<and> ct_not_inQ s \<and> ct_idle_or_in_cur_domain' s \<and> valid_pde_mappings' s \<and> pspace_domain_valid s \<and> ksCurDomain s \<le> maxDomain \<and> ksDomSchedule s \<noteq> [] \<and> (\<forall>x\<in>set (ksDomSchedule s). dschDomain x \<le> maxDomain \<and> 0 < dschLength x) \<and> ksDomSchedule s = ksDomSchedule (KernelInit_H.newKernelState undefined) \<and> ksDomScheduleIdx s < length (ksDomSchedule (KernelInit_H.newKernelState undefined)) \<and> untyped_ranges_zero' s \<and> cur_tcb' s \<and> ct_active' s \<and> pspace_no_overlap' ptr sz s \<and> ptr \<noteq> 0 \<and> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> kernel_data_refs = {} \<and> caps_overlap_reserved' {ptr..ptr + word_of_nat n * 2 ^ gbits * 2 ^ objBitsKO val - 1} s \<and> caps_no_overlap'' ptr sz s \<and> refs_of' val = {} \<and> \<not> live' val \<and> (\<forall>pde. projectKO_opt val = Some pde \<longrightarrow> pde = ARM_H.InvalidPDE)\<rbrakk> \<Longrightarrow> ?Q4 s proof (prove)
goal (4 subgoals):
 1. \<lbrakk>range_cover ptr sz (objBitsKO val + gbits) n; 0 < n\<rbrakk> \<Longrightarrow> \<lbrace>?P38\<rbrace> do y <- createObjects' ptr n val gbits;
return (map (\<lambda>n. ptr + (n << objBitsKO val + gbits)) [0 .e. word_of_nat n - 1])
od \<lbrace>\<lambda>rv. if_live_then_nonz_cap'\<rbrace>
 2. \<lbrakk>range_cover ptr sz (objBitsKO val + gbits) n; 0 < n\<rbrakk> \<Longrightarrow> \<lbrace>?P'38\<rbrace> createObjects ptr n val gbits \<lbrace>\<lambda>rv s. if_unsafe_then_cap' s \<and> valid_idle' s \<and> valid_global_refs' s \<and> valid_arch_state' s \<and> valid_irq_node' (irq_node' s) s \<and> valid_irq_handlers' s \<and> valid_irq_states' s \<and> valid_machine_state' s \<and> irqs_masked' s \<and> valid_queues' s \<and> ct_not_inQ s \<and> ct_idle_or_in_cur_domain' s \<and> valid_pde_mappings' s \<and> pspace_domain_valid s \<and> ksCurDomain s \<le> maxDomain \<and> ksDomSchedule s \<noteq> [] \<and> (\<forall>x\<in>set (ksDomSchedule s). dschDomain x \<le> maxDomain \<and> 0 < dschLength x) \<and> ksDomSchedule s = ksDomSchedule (KernelInit_H.newKernelState undefined) \<and> ksDomScheduleIdx s < length (ksDomSchedule (KernelInit_H.newKernelState undefined)) \<and> untyped_ranges_zero' s \<and> cur_tcb' s\<rbrace>
 3. \<And>s. \<lbrakk>range_cover ptr sz (objBitsKO val + gbits) n; 0 < n; ?Q4 s\<rbrakk> \<Longrightarrow> (pspace_no_overlap' ptr sz s \<and> valid_pspace' s \<and> caps_no_overlap'' ptr sz s \<and> ptr \<noteq> 0 \<and> caps_overlap_reserved' {ptr..ptr + word_of_nat (n * 2 ^ gbits * 2 ^ objBitsKO val) - 1} s) \<and> ((\<lambda>s. sch_act_wf (ksSchedulerAction s) s) and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr ?sz25 and K (range_cover ptr ?sz25 (objBitsKO val + gbits) n \<and> n \<noteq> 0)) s \<and> (Invariants_H.valid_queues s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr ?sz27 s \<and> range_cover ptr ?sz27 (objBitsKO val + gbits) n \<and> n \<noteq> 0) \<and> (n \<noteq> 0 \<and> range_cover ptr ?sz35 (objBitsKO val + gbits) n \<and> sym_refs (state_refs_of' s) \<and> refs_of' val = {} \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr ?sz35 s) \<and> ?P38 s \<and> ?P'38 s
 4. \<And>s. \<lbrakk>range_cover ptr sz (objBitsKO val + gbits) n; 0 < n; valid_pspace' s \<and> sch_act_wf (ksSchedulerAction s) s \<and> Invariants_H.valid_queues s \<and> sym_refs (state_refs_of' s) \<and> if_live_then_nonz_cap' s \<and> if_unsafe_then_cap' s \<and> valid_idle' s \<and> valid_global_refs' s \<and> valid_arch_state' s \<and> valid_irq_node' (irq_node' s) s \<and> valid_irq_handlers' s \<and> valid_irq_states' s \<and> valid_machine_state' s \<and> irqs_masked' s \<and> valid_queues' s \<and> ct_not_inQ s \<and> ct_idle_or_in_cur_domain' s \<and> valid_pde_mappings' s \<and> pspace_domain_valid s \<and> ksCurDomain s \<le> maxDomain \<and> ksDomSchedule s \<noteq> [] \<and> (\<forall>x\<in>set (ksDomSchedule s). dschDomain x \<le> maxDomain \<and> 0 < dschLength x) \<and> ksDomSchedule s = ksDomSchedule (KernelInit_H.newKernelState undefined) \<and> ksDomScheduleIdx s < length (ksDomSchedule (KernelInit_H.newKernelState undefined)) \<and> untyped_ranges_zero' s \<and> cur_tcb' s \<and> ct_active' s \<and> pspace_no_overlap' ptr sz s \<and> ptr \<noteq> 0 \<and> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> kernel_data_refs = {} \<and> caps_overlap_reserved' {ptr..ptr + word_of_nat n * 2 ^ gbits * 2 ^ objBitsKO val - 1} s \<and> caps_no_overlap'' ptr sz s \<and> refs_of' val = {} \<and> \<not> live' val \<and> (\<forall>pde. projectKO_opt val = Some pde \<longrightarrow> pde = ARM_H.InvalidPDE)\<rbrakk> \<Longrightarrow> ?Q4 s proof (prove)
goal (3 subgoals):
 1. \<lbrakk>range_cover ptr sz (objBitsKO val + gbits) n; 0 < n\<rbrakk> \<Longrightarrow> \<lbrace>?P'38\<rbrace> createObjects ptr n val gbits \<lbrace>\<lambda>rv s. if_unsafe_then_cap' s \<and> valid_idle' s \<and> valid_global_refs' s \<and> valid_arch_state' s \<and> valid_irq_node' (irq_node' s) s \<and> valid_irq_handlers' s \<and> valid_irq_states' s \<and> valid_machine_state' s \<and> irqs_masked' s \<and> valid_queues' s \<and> ct_not_inQ s \<and> ct_idle_or_in_cur_domain' s \<and> valid_pde_mappings' s \<and> pspace_domain_valid s \<and> ksCurDomain s \<le> maxDomain \<and> ksDomSchedule s \<noteq> [] \<and> (\<forall>x\<in>set (ksDomSchedule s). dschDomain x \<le> maxDomain \<and> 0 < dschLength x) \<and> ksDomSchedule s = ksDomSchedule (KernelInit_H.newKernelState undefined) \<and> ksDomScheduleIdx s < length (ksDomSchedule (KernelInit_H.newKernelState undefined)) \<and> untyped_ranges_zero' s \<and> cur_tcb' s\<rbrace>
 2. \<And>s. \<lbrakk>range_cover ptr sz (objBitsKO val + gbits) n; 0 < n; ?Q4 s\<rbrakk> \<Longrightarrow> (pspace_no_overlap' ptr sz s \<and> valid_pspace' s \<and> caps_no_overlap'' ptr sz s \<and> ptr \<noteq> 0 \<and> caps_overlap_reserved' {ptr..ptr + word_of_nat (n * 2 ^ gbits * 2 ^ objBitsKO val) - 1} s) \<and> ((\<lambda>s. sch_act_wf (ksSchedulerAction s) s) and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr ?sz25 and K (range_cover ptr ?sz25 (objBitsKO val + gbits) n \<and> n \<noteq> 0)) s \<and> (Invariants_H.valid_queues s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr ?sz27 s \<and> range_cover ptr ?sz27 (objBitsKO val + gbits) n \<and> n \<noteq> 0) \<and> (n \<noteq> 0 \<and> range_cover ptr ?sz35 (objBitsKO val + gbits) n \<and> sym_refs (state_refs_of' s) \<and> refs_of' val = {} \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr ?sz35 s) \<and> (if_live_then_nonz_cap' s \<and> \<not> live' val \<and> n \<noteq> 0 \<and> range_cover ptr ?sz44 (objBitsKO val + gbits) n \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr ?sz44 s) \<and> ?P'38 s
 3. \<And>s. \<lbrakk>range_cover ptr sz (objBitsKO val + gbits) n; 0 < n; valid_pspace' s \<and> sch_act_wf (ksSchedulerAction s) s \<and> Invariants_H.valid_queues s \<and> sym_refs (state_refs_of' s) \<and> if_live_then_nonz_cap' s \<and> if_unsafe_then_cap' s \<and> valid_idle' s \<and> valid_global_refs' s \<and> valid_arch_state' s \<and> valid_irq_node' (irq_node' s) s \<and> valid_irq_handlers' s \<and> valid_irq_states' s \<and> valid_machine_state' s \<and> irqs_masked' s \<and> valid_queues' s \<and> ct_not_inQ s \<and> ct_idle_or_in_cur_domain' s \<and> valid_pde_mappings' s \<and> pspace_domain_valid s \<and> ksCurDomain s \<le> maxDomain \<and> ksDomSchedule s \<noteq> [] \<and> (\<forall>x\<in>set (ksDomSchedule s). dschDomain x \<le> maxDomain \<and> 0 < dschLength x) \<and> ksDomSchedule s = ksDomSchedule (KernelInit_H.newKernelState undefined) \<and> ksDomScheduleIdx s < length (ksDomSchedule (KernelInit_H.newKernelState undefined)) \<and> untyped_ranges_zero' s \<and> cur_tcb' s \<and> ct_active' s \<and> pspace_no_overlap' ptr sz s \<and> ptr \<noteq> 0 \<and> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> kernel_data_refs = {} \<and> caps_overlap_reserved' {ptr..ptr + word_of_nat n * 2 ^ gbits * 2 ^ objBitsKO val - 1} s \<and> caps_no_overlap'' ptr sz s \<and> refs_of' val = {} \<and> \<not> live' val \<and> (\<forall>pde. projectKO_opt val = Some pde \<longrightarrow> pde = ARM_H.InvalidPDE)\<rbrakk> \<Longrightarrow> ?Q4 s proof (prove)
goal (3 subgoals):
 1. \<lbrakk>range_cover ptr sz (objBitsKO val + gbits) n; 0 < n\<rbrakk> \<Longrightarrow> \<lbrace>?P'47\<rbrace> createObjects ptr n val gbits \<lbrace>\<lambda>rv s. valid_idle' s \<and> valid_global_refs' s \<and> valid_arch_state' s \<and> valid_irq_node' (irq_node' s) s \<and> valid_irq_handlers' s \<and> valid_irq_states' s \<and> valid_machine_state' s \<and> irqs_masked' s \<and> valid_queues' s \<and> ct_not_inQ s \<and> ct_idle_or_in_cur_domain' s \<and> valid_pde_mappings' s \<and> pspace_domain_valid s \<and> ksCurDomain s \<le> maxDomain \<and> ksDomSchedule s \<noteq> [] \<and> (\<forall>x\<in>set (ksDomSchedule s). dschDomain x \<le> maxDomain \<and> 0 < dschLength x) \<and> ksDomSchedule s = ksDomSchedule (KernelInit_H.newKernelState undefined) \<and> ksDomScheduleIdx s < length (ksDomSchedule (KernelInit_H.newKernelState undefined)) \<and> untyped_ranges_zero' s \<and> cur_tcb' s\<rbrace>
 2. \<And>s. \<lbrakk>range_cover ptr sz (objBitsKO val + gbits) n; 0 < n; ?Q4 s\<rbrakk> \<Longrightarrow> (pspace_no_overlap' ptr sz s \<and> valid_pspace' s \<and> caps_no_overlap'' ptr sz s \<and> ptr \<noteq> 0 \<and> caps_overlap_reserved' {ptr..ptr + word_of_nat (n * 2 ^ gbits * 2 ^ objBitsKO val) - 1} s) \<and> ((\<lambda>s. sch_act_wf (ksSchedulerAction s) s) and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr ?sz25 and K (range_cover ptr ?sz25 (objBitsKO val + gbits) n \<and> n \<noteq> 0)) s \<and> (Invariants_H.valid_queues s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr ?sz27 s \<and> range_cover ptr ?sz27 (objBitsKO val + gbits) n \<and> n \<noteq> 0) \<and> (n \<noteq> 0 \<and> range_cover ptr ?sz35 (objBitsKO val + gbits) n \<and> sym_refs (state_refs_of' s) \<and> refs_of' val = {} \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr ?sz35 s) \<and> (if_live_then_nonz_cap' s \<and> \<not> live' val \<and> n \<noteq> 0 \<and> range_cover ptr ?sz44 (objBitsKO val + gbits) n \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr ?sz44 s) \<and> (valid_pspace' s \<and> pspace_no_overlap' ptr ?sz48 s \<and> range_cover ptr ?sz48 (objBitsKO val + gbits) n \<and> n \<noteq> 0 \<and> if_unsafe_then_cap' s) \<and> ?P'47 s
 3. \<And>s. \<lbrakk>range_cover ptr sz (objBitsKO val + gbits) n; 0 < n; valid_pspace' s \<and> sch_act_wf (ksSchedulerAction s) s \<and> Invariants_H.valid_queues s \<and> sym_refs (state_refs_of' s) \<and> if_live_then_nonz_cap' s \<and> if_unsafe_then_cap' s \<and> valid_idle' s \<and> valid_global_refs' s \<and> valid_arch_state' s \<and> valid_irq_node' (irq_node' s) s \<and> valid_irq_handlers' s \<and> valid_irq_states' s \<and> valid_machine_state' s \<and> irqs_masked' s \<and> valid_queues' s \<and> ct_not_inQ s \<and> ct_idle_or_in_cur_domain' s \<and> valid_pde_mappings' s \<and> pspace_domain_valid s \<and> ksCurDomain s \<le> maxDomain \<and> ksDomSchedule s \<noteq> [] \<and> (\<forall>x\<in>set (ksDomSchedule s). dschDomain x \<le> maxDomain \<and> 0 < dschLength x) \<and> ksDomSchedule s = ksDomSchedule (KernelInit_H.newKernelState undefined) \<and> ksDomScheduleIdx s < length (ksDomSchedule (KernelInit_H.newKernelState undefined)) \<and> untyped_ranges_zero' s \<and> cur_tcb' s \<and> ct_active' s \<and> pspace_no_overlap' ptr sz s \<and> ptr \<noteq> 0 \<and> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> kernel_data_refs = {} \<and> caps_overlap_reserved' {ptr..ptr + word_of_nat n * 2 ^ gbits * 2 ^ objBitsKO val - 1} s \<and> caps_no_overlap'' ptr sz s \<and> refs_of' val = {} \<and> \<not> live' val \<and> (\<forall>pde. projectKO_opt val = Some pde \<longrightarrow> pde = ARM_H.InvalidPDE)\<rbrakk> \<Longrightarrow> ?Q4 s proof (prove)
goal (4 subgoals):
 1. \<lbrakk>range_cover ptr sz (objBitsKO val + gbits) n; 0 < n\<rbrakk> \<Longrightarrow> \<lbrace>?P52\<rbrace> createObjects ptr n val gbits \<lbrace>\<lambda>rv. valid_idle'\<rbrace>
 2. \<lbrakk>range_cover ptr sz (objBitsKO val + gbits) n; 0 < n\<rbrakk> \<Longrightarrow> \<lbrace>?P'52\<rbrace> createObjects ptr n val gbits \<lbrace>\<lambda>rv s. valid_global_refs' s \<and> valid_arch_state' s \<and> valid_irq_node' (irq_node' s) s \<and> valid_irq_handlers' s \<and> valid_irq_states' s \<and> valid_machine_state' s \<and> irqs_masked' s \<and> valid_queues' s \<and> ct_not_inQ s \<and> ct_idle_or_in_cur_domain' s \<and> valid_pde_mappings' s \<and> pspace_domain_valid s \<and> ksCurDomain s \<le> maxDomain \<and> ksDomSchedule s \<noteq> [] \<and> (\<forall>x\<in>set (ksDomSchedule s). dschDomain x \<le> maxDomain \<and> 0 < dschLength x) \<and> ksDomSchedule s = ksDomSchedule (KernelInit_H.newKernelState undefined) \<and> ksDomScheduleIdx s < length (ksDomSchedule (KernelInit_H.newKernelState undefined)) \<and> untyped_ranges_zero' s \<and> cur_tcb' s\<rbrace>
 3. \<And>s. \<lbrakk>range_cover ptr sz (objBitsKO val + gbits) n; 0 < n; ?Q4 s\<rbrakk> \<Longrightarrow> (pspace_no_overlap' ptr sz s \<and> valid_pspace' s \<and> caps_no_overlap'' ptr sz s \<and> ptr \<noteq> 0 \<and> caps_overlap_reserved' {ptr..ptr + word_of_nat (n * 2 ^ gbits * 2 ^ objBitsKO val) - 1} s) \<and> ((\<lambda>s. sch_act_wf (ksSchedulerAction s) s) and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr ?sz25 and K (range_cover ptr ?sz25 (objBitsKO val + gbits) n \<and> n \<noteq> 0)) s \<and> (Invariants_H.valid_queues s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr ?sz27 s \<and> range_cover ptr ?sz27 (objBitsKO val + gbits) n \<and> n \<noteq> 0) \<and> (n \<noteq> 0 \<and> range_cover ptr ?sz35 (objBitsKO val + gbits) n \<and> sym_refs (state_refs_of' s) \<and> refs_of' val = {} \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr ?sz35 s) \<and> (if_live_then_nonz_cap' s \<and> \<not> live' val \<and> n \<noteq> 0 \<and> range_cover ptr ?sz44 (objBitsKO val + gbits) n \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr ?sz44 s) \<and> (valid_pspace' s \<and> pspace_no_overlap' ptr ?sz48 s \<and> range_cover ptr ?sz48 (objBitsKO val + gbits) n \<and> n \<noteq> 0 \<and> if_unsafe_then_cap' s) \<and> ?P52 s \<and> ?P'52 s
 4. \<And>s. \<lbrakk>range_cover ptr sz (objBitsKO val + gbits) n; 0 < n; valid_pspace' s \<and> sch_act_wf (ksSchedulerAction s) s \<and> Invariants_H.valid_queues s \<and> sym_refs (state_refs_of' s) \<and> if_live_then_nonz_cap' s \<and> if_unsafe_then_cap' s \<and> valid_idle' s \<and> valid_global_refs' s \<and> valid_arch_state' s \<and> valid_irq_node' (irq_node' s) s \<and> valid_irq_handlers' s \<and> valid_irq_states' s \<and> valid_machine_state' s \<and> irqs_masked' s \<and> valid_queues' s \<and> ct_not_inQ s \<and> ct_idle_or_in_cur_domain' s \<and> valid_pde_mappings' s \<and> pspace_domain_valid s \<and> ksCurDomain s \<le> maxDomain \<and> ksDomSchedule s \<noteq> [] \<and> (\<forall>x\<in>set (ksDomSchedule s). dschDomain x \<le> maxDomain \<and> 0 < dschLength x) \<and> ksDomSchedule s = ksDomSchedule (KernelInit_H.newKernelState undefined) \<and> ksDomScheduleIdx s < length (ksDomSchedule (KernelInit_H.newKernelState undefined)) \<and> untyped_ranges_zero' s \<and> cur_tcb' s \<and> ct_active' s \<and> pspace_no_overlap' ptr sz s \<and> ptr \<noteq> 0 \<and> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> kernel_data_refs = {} \<and> caps_overlap_reserved' {ptr..ptr + word_of_nat n * 2 ^ gbits * 2 ^ objBitsKO val - 1} s \<and> caps_no_overlap'' ptr sz s \<and> refs_of' val = {} \<and> \<not> live' val \<and> (\<forall>pde. projectKO_opt val = Some pde \<longrightarrow> pde = ARM_H.InvalidPDE)\<rbrakk> \<Longrightarrow> ?Q4 s proof (prove)
goal (4 subgoals):
 1. \<lbrakk>range_cover ptr sz (objBitsKO val + gbits) n; 0 < n\<rbrakk> \<Longrightarrow> \<lbrace>?P52\<rbrace> do y <- createObjects' ptr n val gbits;
return (map (\<lambda>n. ptr + (n << objBitsKO val + gbits)) [0 .e. word_of_nat n - 1])
od \<lbrace>\<lambda>rv. valid_idle'\<rbrace>
 2. \<lbrakk>range_cover ptr sz (objBitsKO val + gbits) n; 0 < n\<rbrakk> \<Longrightarrow> \<lbrace>?P'52\<rbrace> createObjects ptr n val gbits \<lbrace>\<lambda>rv s. valid_global_refs' s \<and> valid_arch_state' s \<and> valid_irq_node' (irq_node' s) s \<and> valid_irq_handlers' s \<and> valid_irq_states' s \<and> valid_machine_state' s \<and> irqs_masked' s \<and> valid_queues' s \<and> ct_not_inQ s \<and> ct_idle_or_in_cur_domain' s \<and> valid_pde_mappings' s \<and> pspace_domain_valid s \<and> ksCurDomain s \<le> maxDomain \<and> ksDomSchedule s \<noteq> [] \<and> (\<forall>x\<in>set (ksDomSchedule s). dschDomain x \<le> maxDomain \<and> 0 < dschLength x) \<and> ksDomSchedule s = ksDomSchedule (KernelInit_H.newKernelState undefined) \<and> ksDomScheduleIdx s < length (ksDomSchedule (KernelInit_H.newKernelState undefined)) \<and> untyped_ranges_zero' s \<and> cur_tcb' s\<rbrace>
 3. \<And>s. \<lbrakk>range_cover ptr sz (objBitsKO val + gbits) n; 0 < n; ?Q4 s\<rbrakk> \<Longrightarrow> (pspace_no_overlap' ptr sz s \<and> valid_pspace' s \<and> caps_no_overlap'' ptr sz s \<and> ptr \<noteq> 0 \<and> caps_overlap_reserved' {ptr..ptr + word_of_nat (n * 2 ^ gbits * 2 ^ objBitsKO val) - 1} s) \<and> ((\<lambda>s. sch_act_wf (ksSchedulerAction s) s) and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr ?sz25 and K (range_cover ptr ?sz25 (objBitsKO val + gbits) n \<and> n \<noteq> 0)) s \<and> (Invariants_H.valid_queues s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr ?sz27 s \<and> range_cover ptr ?sz27 (objBitsKO val + gbits) n \<and> n \<noteq> 0) \<and> (n \<noteq> 0 \<and> range_cover ptr ?sz35 (objBitsKO val + gbits) n \<and> sym_refs (state_refs_of' s) \<and> refs_of' val = {} \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr ?sz35 s) \<and> (if_live_then_nonz_cap' s \<and> \<not> live' val \<and> n \<noteq> 0 \<and> range_cover ptr ?sz44 (objBitsKO val + gbits) n \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr ?sz44 s) \<and> (valid_pspace' s \<and> pspace_no_overlap' ptr ?sz48 s \<and> range_cover ptr ?sz48 (objBitsKO val + gbits) n \<and> n \<noteq> 0 \<and> if_unsafe_then_cap' s) \<and> ?P52 s \<and> ?P'52 s
 4. \<And>s. \<lbrakk>range_cover ptr sz (objBitsKO val + gbits) n; 0 < n; valid_pspace' s \<and> sch_act_wf (ksSchedulerAction s) s \<and> Invariants_H.valid_queues s \<and> sym_refs (state_refs_of' s) \<and> if_live_then_nonz_cap' s \<and> if_unsafe_then_cap' s \<and> valid_idle' s \<and> valid_global_refs' s \<and> valid_arch_state' s \<and> valid_irq_node' (irq_node' s) s \<and> valid_irq_handlers' s \<and> valid_irq_states' s \<and> valid_machine_state' s \<and> irqs_masked' s \<and> valid_queues' s \<and> ct_not_inQ s \<and> ct_idle_or_in_cur_domain' s \<and> valid_pde_mappings' s \<and> pspace_domain_valid s \<and> ksCurDomain s \<le> maxDomain \<and> ksDomSchedule s \<noteq> [] \<and> (\<forall>x\<in>set (ksDomSchedule s). dschDomain x \<le> maxDomain \<and> 0 < dschLength x) \<and> ksDomSchedule s = ksDomSchedule (KernelInit_H.newKernelState undefined) \<and> ksDomScheduleIdx s < length (ksDomSchedule (KernelInit_H.newKernelState undefined)) \<and> untyped_ranges_zero' s \<and> cur_tcb' s \<and> ct_active' s \<and> pspace_no_overlap' ptr sz s \<and> ptr \<noteq> 0 \<and> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> kernel_data_refs = {} \<and> caps_overlap_reserved' {ptr..ptr + word_of_nat n * 2 ^ gbits * 2 ^ objBitsKO val - 1} s \<and> caps_no_overlap'' ptr sz s \<and> refs_of' val = {} \<and> \<not> live' val \<and> (\<forall>pde. projectKO_opt val = Some pde \<longrightarrow> pde = ARM_H.InvalidPDE)\<rbrakk> \<Longrightarrow> ?Q4 s proof (prove)
goal (3 subgoals):
 1. \<lbrakk>range_cover ptr sz (objBitsKO val + gbits) n; 0 < n\<rbrakk> \<Longrightarrow> \<lbrace>?P'52\<rbrace> createObjects ptr n val gbits \<lbrace>\<lambda>rv s. valid_global_refs' s \<and> valid_arch_state' s \<and> valid_irq_node' (irq_node' s) s \<and> valid_irq_handlers' s \<and> valid_irq_states' s \<and> valid_machine_state' s \<and> irqs_masked' s \<and> valid_queues' s \<and> ct_not_inQ s \<and> ct_idle_or_in_cur_domain' s \<and> valid_pde_mappings' s \<and> pspace_domain_valid s \<and> ksCurDomain s \<le> maxDomain \<and> ksDomSchedule s \<noteq> [] \<and> (\<forall>x\<in>set (ksDomSchedule s). dschDomain x \<le> maxDomain \<and> 0 < dschLength x) \<and> ksDomSchedule s = ksDomSchedule (KernelInit_H.newKernelState undefined) \<and> ksDomScheduleIdx s < length (ksDomSchedule (KernelInit_H.newKernelState undefined)) \<and> untyped_ranges_zero' s \<and> cur_tcb' s\<rbrace>
 2. \<And>s. \<lbrakk>range_cover ptr sz (objBitsKO val + gbits) n; 0 < n; ?Q4 s\<rbrakk> \<Longrightarrow> (pspace_no_overlap' ptr sz s \<and> valid_pspace' s \<and> caps_no_overlap'' ptr sz s \<and> ptr \<noteq> 0 \<and> caps_overlap_reserved' {ptr..ptr + word_of_nat (n * 2 ^ gbits * 2 ^ objBitsKO val) - 1} s) \<and> ((\<lambda>s. sch_act_wf (ksSchedulerAction s) s) and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr ?sz25 and K (range_cover ptr ?sz25 (objBitsKO val + gbits) n \<and> n \<noteq> 0)) s \<and> (Invariants_H.valid_queues s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr ?sz27 s \<and> range_cover ptr ?sz27 (objBitsKO val + gbits) n \<and> n \<noteq> 0) \<and> (n \<noteq> 0 \<and> range_cover ptr ?sz35 (objBitsKO val + gbits) n \<and> sym_refs (state_refs_of' s) \<and> refs_of' val = {} \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr ?sz35 s) \<and> (if_live_then_nonz_cap' s \<and> \<not> live' val \<and> n \<noteq> 0 \<and> range_cover ptr ?sz44 (objBitsKO val + gbits) n \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr ?sz44 s) \<and> (valid_pspace' s \<and> pspace_no_overlap' ptr ?sz48 s \<and> range_cover ptr ?sz48 (objBitsKO val + gbits) n \<and> n \<noteq> 0 \<and> if_unsafe_then_cap' s) \<and> (valid_idle' and valid_pspace' and pspace_no_overlap' ptr ?sz58 and (\<lambda>s. \<not> (case projectKO_opt val of None \<Rightarrow> False | Some cte \<Rightarrow> ksIdleThread s \<in> capRange (cteCap cte)) \<and> (\<forall>(getF, setF)\<in>ran tcb_cte_cases. \<not> (case projectKO_opt val of None \<Rightarrow> False | Some tcb \<Rightarrow> ksIdleThread s \<in> capRange (cteCap (getF tcb))))) and K (range_cover ptr ?sz58 (objBitsKO val + gbits) n \<and> n \<noteq> 0)) s \<and> ?P'52 s
 3. \<And>s. \<lbrakk>range_cover ptr sz (objBitsKO val + gbits) n; 0 < n; valid_pspace' s \<and> sch_act_wf (ksSchedulerAction s) s \<and> Invariants_H.valid_queues s \<and> sym_refs (state_refs_of' s) \<and> if_live_then_nonz_cap' s \<and> if_unsafe_then_cap' s \<and> valid_idle' s \<and> valid_global_refs' s \<and> valid_arch_state' s \<and> valid_irq_node' (irq_node' s) s \<and> valid_irq_handlers' s \<and> valid_irq_states' s \<and> valid_machine_state' s \<and> irqs_masked' s \<and> valid_queues' s \<and> ct_not_inQ s \<and> ct_idle_or_in_cur_domain' s \<and> valid_pde_mappings' s \<and> pspace_domain_valid s \<and> ksCurDomain s \<le> maxDomain \<and> ksDomSchedule s \<noteq> [] \<and> (\<forall>x\<in>set (ksDomSchedule s). dschDomain x \<le> maxDomain \<and> 0 < dschLength x) \<and> ksDomSchedule s = ksDomSchedule (KernelInit_H.newKernelState undefined) \<and> ksDomScheduleIdx s < length (ksDomSchedule (KernelInit_H.newKernelState undefined)) \<and> untyped_ranges_zero' s \<and> cur_tcb' s \<and> ct_active' s \<and> pspace_no_overlap' ptr sz s \<and> ptr \<noteq> 0 \<and> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> kernel_data_refs = {} \<and> caps_overlap_reserved' {ptr..ptr + word_of_nat n * 2 ^ gbits * 2 ^ objBitsKO val - 1} s \<and> caps_no_overlap'' ptr sz s \<and> refs_of' val = {} \<and> \<not> live' val \<and> (\<forall>pde. projectKO_opt val = Some pde \<longrightarrow> pde = ARM_H.InvalidPDE)\<rbrakk> \<Longrightarrow> ?Q4 s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>range_cover ptr sz (objBitsKO val + gbits) n; 0 < n; valid_pspace' s \<and> sch_act_wf (ksSchedulerAction s) s \<and> Invariants_H.valid_queues s \<and> sym_refs (state_refs_of' s) \<and> if_live_then_nonz_cap' s \<and> if_unsafe_then_cap' s \<and> valid_idle' s \<and> valid_global_refs' s \<and> valid_arch_state' s \<and> valid_irq_node' (irq_node' s) s \<and> valid_irq_handlers' s \<and> valid_irq_states' s \<and> valid_machine_state' s \<and> irqs_masked' s \<and> valid_queues' s \<and> ct_not_inQ s \<and> ct_idle_or_in_cur_domain' s \<and> valid_pde_mappings' s \<and> pspace_domain_valid s \<and> ksCurDomain s \<le> maxDomain \<and> ksDomSchedule s \<noteq> [] \<and> (\<forall>x\<in>set (ksDomSchedule s). dschDomain x \<le> maxDomain \<and> 0 < dschLength x) \<and> ksDomSchedule s = ksDomSchedule (KernelInit_H.newKernelState undefined) \<and> ksDomScheduleIdx s < length (ksDomSchedule (KernelInit_H.newKernelState undefined)) \<and> untyped_ranges_zero' s \<and> cur_tcb' s \<and> ct_active' s \<and> pspace_no_overlap' ptr sz s \<and> ptr \<noteq> 0 \<and> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> kernel_data_refs = {} \<and> caps_overlap_reserved' {ptr..ptr + word_of_nat n * 2 ^ gbits * 2 ^ objBitsKO val - 1} s \<and> caps_no_overlap'' ptr sz s \<and> refs_of' val = {} \<and> \<not> live' val \<and> (\<forall>pde. projectKO_opt val = Some pde \<longrightarrow> pde = ARM_H.InvalidPDE)\<rbrakk> \<Longrightarrow> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr ?sz25 s \<and> range_cover ptr ?sz25 (objBitsKO val + gbits) n \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr ?sz27 s \<and> range_cover ptr ?sz27 (objBitsKO val + gbits) n \<and> range_cover ptr ?sz35 (objBitsKO val + gbits) n \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr ?sz35 s \<and> range_cover ptr ?sz44 (objBitsKO val + gbits) n \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr ?sz44 s \<and> pspace_no_overlap' ptr ?sz48 s \<and> range_cover ptr ?sz48 (objBitsKO val + gbits) n \<and> pspace_no_overlap' ptr ?sz58 s \<and> \<not> (case projectKO_opt val of None \<Rightarrow> False | Some cte \<Rightarrow> ksIdleThread s \<in> capRange (cteCap cte)) \<and> (\<forall>x\<in>ran tcb_cte_cases. case x of (getF, setF) \<Rightarrow> \<not> (case projectKO_opt val of None \<Rightarrow> False | Some tcb \<Rightarrow> ksIdleThread s \<in> capRange (cteCap (getF tcb)))) \<and> range_cover ptr ?sz58 (objBitsKO val + gbits) n \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr ?sz62 s \<and> range_cover ptr ?sz62 (objBitsKO val + gbits) n \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr ?sz66 s \<and> range_cover ptr ?sz66 (objBitsKO val + gbits) n \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr ?sz68 s \<and> range_cover ptr ?sz68 (objBitsKO val + gbits) n \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr ?sz70 s \<and> range_cover ptr ?sz70 (objBitsKO val + gbits) n \<and> range_cover ptr ?sz76 (objBitsKO val + gbits) n \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr ?sz76 s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr ?sz82 s \<and> range_cover ptr ?sz82 (objBitsKO val + gbits) n \<and> pspace_no_overlap' ptr ?sz88 s \<and> range_cover ptr ?sz88 (objBitsKO val + gbits) n \<and> range_cover ptr ?sz90 (objBitsKO val + gbits) n \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr ?sz90 s \<and> range_cover ptr ?sz92 (objBitsKO val + gbits) n \<and> {ptr..(ptr && ~~ mask ?sz92) + 2 ^ ?sz92 - 1} \<inter> kernel_data_refs = {} \<and> ksDomSchedule (KernelInit_H.newKernelState undefined) \<noteq> [] \<and> pspace_no_overlap' ptr ?sz104 s \<and> range_cover ptr ?sz104 (objBitsKO val + gbits) n \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr ?sz105 s \<and> range_cover ptr ?sz105 (objBitsKO val + gbits) n proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>range_cover ptr sz (objBitsKO val + gbits) n; 0 < n; valid_pspace' s; sch_act_wf (ksSchedulerAction s) s; Invariants_H.valid_queues s; sym_refs (state_refs_of' s); if_live_then_nonz_cap' s; if_unsafe_then_cap' s; valid_idle' s; valid_global_refs' s; valid_arch_state' s; valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; valid_machine_state' s; irqs_masked' s; valid_queues' s; ct_not_inQ s; ct_idle_or_in_cur_domain' s; valid_pde_mappings' s; pspace_domain_valid s; ksCurDomain s \<le> maxDomain; ksDomSchedule (KernelInit_H.newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (KernelInit_H.newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (KernelInit_H.newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (KernelInit_H.newKernelState undefined)); untyped_ranges_zero' s; cur_tcb' s; ct_active' s; pspace_no_overlap' ptr sz s; ptr \<noteq> 0; {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> kernel_data_refs = {}; caps_overlap_reserved' {ptr..ptr + word_of_nat n * 2 ^ gbits * 2 ^ objBitsKO val - 1} s; caps_no_overlap'' ptr sz s; refs_of' val = {}; \<not> live' val; \<forall>pde. projectKO_opt val = Some pde \<longrightarrow> pde = ARM_H.InvalidPDE\<rbrakk> \<Longrightarrow> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr ?sz25 s \<and> range_cover ptr ?sz25 (objBitsKO val + gbits) n \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr ?sz27 s \<and> range_cover ptr ?sz27 (objBitsKO val + gbits) n \<and> range_cover ptr ?sz35 (objBitsKO val + gbits) n \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr ?sz35 s \<and> range_cover ptr ?sz44 (objBitsKO val + gbits) n \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr ?sz44 s \<and> pspace_no_overlap' ptr ?sz48 s \<and> range_cover ptr ?sz48 (objBitsKO val + gbits) n \<and> pspace_no_overlap' ptr ?sz58 s \<and> \<not> (case projectKO_opt val of None \<Rightarrow> False | Some cte \<Rightarrow> ksIdleThread s \<in> capRange (cteCap cte)) \<and> (\<forall>x\<in>ran tcb_cte_cases. case x of (getF, setF) \<Rightarrow> \<not> (case projectKO_opt val of None \<Rightarrow> False | Some tcb \<Rightarrow> ksIdleThread s \<in> capRange (cteCap (getF tcb)))) \<and> range_cover ptr ?sz58 (objBitsKO val + gbits) n \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr ?sz62 s \<and> range_cover ptr ?sz62 (objBitsKO val + gbits) n \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr ?sz66 s \<and> range_cover ptr ?sz66 (objBitsKO val + gbits) n \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr ?sz68 s \<and> range_cover ptr ?sz68 (objBitsKO val + gbits) n \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr ?sz70 s \<and> range_cover ptr ?sz70 (objBitsKO val + gbits) n \<and> range_cover ptr ?sz76 (objBitsKO val + gbits) n \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr ?sz76 s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr ?sz82 s \<and> range_cover ptr ?sz82 (objBitsKO val + gbits) n \<and> pspace_no_overlap' ptr ?sz88 s \<and> range_cover ptr ?sz88 (objBitsKO val + gbits) n \<and> range_cover ptr ?sz90 (objBitsKO val + gbits) n \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr ?sz90 s \<and> range_cover ptr ?sz92 (objBitsKO val + gbits) n \<and> {ptr..(ptr && ~~ mask ?sz92) + 2 ^ ?sz92 - 1} \<inter> kernel_data_refs = {} \<and> pspace_no_overlap' ptr ?sz104 s \<and> range_cover ptr ?sz104 (objBitsKO val + gbits) n \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr ?sz105 s \<and> range_cover ptr ?sz105 (objBitsKO val + gbits) n proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>range_cover ptr sz (objBitsKO val + gbits) n; 0 < n; valid_objs' s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> no_0_obj' s \<and> valid_mdb' s; sch_act_wf (ksSchedulerAction s) s; Invariants_H.valid_queues s; sym_refs (state_refs_of' s); if_live_then_nonz_cap' s; if_unsafe_then_cap' s; valid_idle' s; valid_global_refs' s; valid_arch_state' s; valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; valid_machine_state' s; irqs_masked' s; valid_queues' s; ct_not_inQ s; ct_idle_or_in_cur_domain' s; valid_pde_mappings' s; pspace_domain_valid s; ksCurDomain s \<le> maxDomain; ksDomSchedule (KernelInit_H.newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (KernelInit_H.newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (KernelInit_H.newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (KernelInit_H.newKernelState undefined)); untyped_ranges_zero' s; cur_tcb' s; ct_active' s; pspace_no_overlap' ptr sz s; ptr \<noteq> 0; {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> kernel_data_refs = {}; caps_overlap_reserved' {ptr..ptr + word_of_nat n * 2 ^ gbits * 2 ^ objBitsKO val - 1} s; caps_no_overlap'' ptr sz s; refs_of' val = {}; \<not> live' val; \<forall>pde. projectKO_opt val = Some pde \<longrightarrow> pde = ARM_H.InvalidPDE\<rbrakk> \<Longrightarrow> \<not> (case projectKO_opt val of None \<Rightarrow> False | Some cte \<Rightarrow> ksIdleThread s \<in> capRange (cteCap cte))
 2. \<And>s. \<lbrakk>range_cover ptr sz (objBitsKO val + gbits) n; 0 < n; valid_objs' s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> no_0_obj' s \<and> valid_mdb' s; sch_act_wf (ksSchedulerAction s) s; Invariants_H.valid_queues s; sym_refs (state_refs_of' s); if_live_then_nonz_cap' s; if_unsafe_then_cap' s; valid_idle' s; valid_global_refs' s; valid_arch_state' s; valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; valid_machine_state' s; irqs_masked' s; valid_queues' s; ct_not_inQ s; ct_idle_or_in_cur_domain' s; valid_pde_mappings' s; pspace_domain_valid s; ksCurDomain s \<le> maxDomain; ksDomSchedule (KernelInit_H.newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (KernelInit_H.newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (KernelInit_H.newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (KernelInit_H.newKernelState undefined)); untyped_ranges_zero' s; cur_tcb' s; ct_active' s; pspace_no_overlap' ptr sz s; ptr \<noteq> 0; {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> kernel_data_refs = {}; caps_overlap_reserved' {ptr..ptr + word_of_nat n * 2 ^ gbits * 2 ^ objBitsKO val - 1} s; caps_no_overlap'' ptr sz s; refs_of' val = {}; \<not> live' val; \<forall>pde. projectKO_opt val = Some pde \<longrightarrow> pde = ARM_H.InvalidPDE\<rbrakk> \<Longrightarrow> \<forall>x\<in>ran tcb_cte_cases. case x of (getF, setF) \<Rightarrow> \<not> (case projectKO_opt val of None \<Rightarrow> False | Some tcb \<Rightarrow> ksIdleThread s \<in> capRange (cteCap (getF tcb))) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>range_cover ptr sz (objBitsKO val + gbits) n; 0 < n; valid_objs' s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> no_0_obj' s \<and> valid_mdb' s; sch_act_wf (ksSchedulerAction s) s; Invariants_H.valid_queues s; sym_refs (state_refs_of' s); if_live_then_nonz_cap' s; if_unsafe_then_cap' s; valid_idle' s; valid_global_refs' s; valid_arch_state' s; valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; valid_machine_state' s; irqs_masked' s; valid_queues' s; ct_not_inQ s; ct_idle_or_in_cur_domain' s; valid_pde_mappings' s; pspace_domain_valid s; ksCurDomain s \<le> maxDomain; ksDomSchedule (KernelInit_H.newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (KernelInit_H.newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (KernelInit_H.newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (KernelInit_H.newKernelState undefined)); untyped_ranges_zero' s; cur_tcb' s; ct_active' s; pspace_no_overlap' ptr sz s; ptr \<noteq> 0; {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> kernel_data_refs = {}; caps_overlap_reserved' {ptr..ptr + word_of_nat n * 2 ^ gbits * 2 ^ objBitsKO val - 1} s; caps_no_overlap'' ptr sz s; refs_of' val = {}; \<not> live' val; \<forall>pde. projectKO_opt val = Some pde \<longrightarrow> pde = ARM_H.InvalidPDE\<rbrakk> \<Longrightarrow> \<forall>x\<in>ran tcb_cte_cases. case x of (getF, setF) \<Rightarrow> \<not> (case projectKO_opt val of None \<Rightarrow> False | Some tcb \<Rightarrow> ksIdleThread s \<in> capRange (cteCap (getF tcb))) proof (prove)
goal:
No subgoals! proof (state)
this:
\<lbrace>\<lambda>s. range_cover ptr sz (objBitsKO val + gbits) n \<and> n \<noteq> 0 \<and> invs' s \<and> ct_active' s \<and> pspace_no_overlap' ptr sz s \<and> ptr \<noteq> 0 \<and> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> kernel_data_refs = {} \<and> caps_overlap_reserved' {ptr..ptr + word_of_nat (n * 2 ^ gbits * 2 ^ objBitsKO val) - 1} s \<and> caps_no_overlap'' ptr sz s \<and> refs_of' val = {} \<and> \<not> live' val \<and> (\<forall>pde. projectKO_opt val = Some pde \<longrightarrow> pde = ARM_H.InvalidPDE)\<rbrace> createObjects ptr n val gbits \<lbrace>\<lambda>rv. invs'\<rbrace>

goal:
No subgoals!