theory Untyped_R

lemma updateFreeIndex_clear_invs':
  "\<lbrace>\<lambda>s. invs' s \<and>
        (\<exists>ptr sz. pspace_no_overlap' ptr sz s \<and> idx \<le> 2 ^ sz \<and>
        cte_wp_at' ((\<lambda>c. isUntypedCap c \<and> capPtr c = ptr \<and> capBlockSize c = sz) o cteCap) src s)
        \<and> is_aligned (of_nat idx :: word32) minUntypedSizeBits
        \<and> descendants_of' src (ctes_of s) = {}\<rbrace>
   updateFreeIndex src idx
   \<lbrace>\<lambda>r s. invs' s\<rbrace>" apply (clarsimp simp:invs'_def valid_state'_def) apply (wp updateFreeIndex_valid_pspace_no_overlap') apply (simp add: updateFreeIndex_def updateTrackedFreeIndex_def) apply (wp updateFreeIndex_valid_pspace_no_overlap' sch_act_wf_lift valid_queues_lift
             updateCap_iflive' tcb_in_cur_domain'_lift
            | simp add: pred_tcb_at'_def)+ apply (rule hoare_vcg_conj_lift) apply (simp add: ifunsafe'_def3 cteInsert_def setUntypedCapAsFull_def
               split del: if_split) apply wp+ apply (rule hoare_vcg_conj_lift) apply (simp add:updateCap_def) apply wp+ apply (wp valid_irq_node_lift) apply (rule hoare_vcg_conj_lift) apply (simp add:updateCap_def) apply (wp setCTE_irq_handlers' getCTE_wp) apply (simp add:updateCap_def) apply (wp irqs_masked_lift valid_queues_lift' cur_tcb_lift ct_idle_or_in_cur_domain'_lift
                hoare_vcg_disj_lift untyped_ranges_zero_lift getCTE_wp
               | wp (once) hoare_use_eq[where f="gsUntypedZeroRanges"]
               | simp add: getSlotCap_def
               | simp add: cte_wp_at_ctes_of)+ apply (clarsimp simp: cte_wp_at_ctes_of fun_upd_def[symmetric]) apply (clarsimp simp: isCap_simps) apply (frule(1) valid_global_refsD_with_objSize) apply clarsimp apply (intro conjI allI impI) apply (clarsimp simp: modify_map_def cteCaps_of_def ifunsafe'_def3 split:if_splits) apply (drule_tac x=src in spec) apply (clarsimp simp:isCap_simps) apply (rule_tac x = cref' in exI) apply clarsimp apply (drule_tac x = cref in spec) apply clarsimp apply (rule_tac x = cref' in exI) apply clarsimp apply (clarsimp simp: valid_pspace'_def) apply (erule untyped_ranges_zero_fun_upd, simp_all) apply (clarsimp simp: untypedZeroRange_def cteCaps_of_def isCap_simps) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. invs' s \<and> (\<exists>ptr sz. pspace_no_overlap' ptr sz s \<and> idx \<le> 2 ^ sz \<and> cte_wp_at' ((\<lambda>c. isUntypedCap c \<and> capPtr c = ptr \<and> capBlockSize c = sz) \<circ> cteCap) src s) \<and> is_aligned (word_of_nat idx) minUntypedSizeBits \<and> descendants_of' src (ctes_of s) = {}\<rbrace> updateFreeIndex src idx \<lbrace>\<lambda>r. invs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<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> (\<exists>ptr sz. pspace_no_overlap' ptr sz s \<and> idx \<le> 2 ^ sz \<and> cte_wp_at' ((\<lambda>c. isUntypedCap c \<and> capPtr c = ptr \<and> capBlockSize c = sz) \<circ> cteCap) src s) \<and> is_aligned (word_of_nat idx) minUntypedSizeBits \<and> descendants_of' src (ctes_of s) = {}\<rbrace> updateFreeIndex src idx \<lbrace>\<lambda>r 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> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?P'1\<rbrace> updateFreeIndex src idx \<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. 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> (\<exists>ptr sz. pspace_no_overlap' ptr sz s \<and> idx \<le> 2 ^ sz \<and> cte_wp_at' ((\<lambda>c. isUntypedCap c \<and> capPtr c = ptr \<and> capBlockSize c = sz) \<circ> cteCap) src s) \<and> is_aligned (word_of_nat idx) minUntypedSizeBits \<and> descendants_of' src (ctes_of s) = {} \<Longrightarrow> (valid_pspace' s \<and> (\<exists>ptr sz. pspace_no_overlap' ptr sz s \<and> idx \<le> 2 ^ sz \<and> cte_wp_at' ((\<lambda>c. isUntypedCap c \<and> capPtr c = ptr \<and> capBlockSize c = sz) \<circ> cteCap) src s) \<and> is_aligned (word_of_nat idx) minUntypedSizeBits \<and> descendants_of' src (ctes_of s) = {}) \<and> ?P'1 s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?P'1\<rbrace> do y <- do cap <- getSlotCap src;
y <- modify (\<lambda>ks. ks\<lparr>gsUntypedZeroRanges := case untypedZeroRange cap of None \<Rightarrow> gsUntypedZeroRanges ks | Some r \<Rightarrow> gsUntypedZeroRanges ks - {r}\<rparr>);
modify (\<lambda>ks. ks\<lparr>gsUntypedZeroRanges := case untypedZeroRange (capFreeIndex_update (\<lambda>_. idx) cap) of None \<Rightarrow> gsUntypedZeroRanges ks | Some r \<Rightarrow> insert r (gsUntypedZeroRanges ks)\<rparr>)
od;
cap <- getSlotCap src;
updateCap src (capFreeIndex_update (\<lambda>_. idx) cap)
od \<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. 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> (\<exists>ptr sz. pspace_no_overlap' ptr sz s \<and> idx \<le> 2 ^ sz \<and> cte_wp_at' ((\<lambda>c. isUntypedCap c \<and> capPtr c = ptr \<and> capBlockSize c = sz) \<circ> cteCap) src s) \<and> is_aligned (word_of_nat idx) minUntypedSizeBits \<and> descendants_of' src (ctes_of s) = {} \<Longrightarrow> (valid_pspace' s \<and> (\<exists>ptr sz. pspace_no_overlap' ptr sz s \<and> idx \<le> 2 ^ sz \<and> cte_wp_at' ((\<lambda>c. isUntypedCap c \<and> capPtr c = ptr \<and> capBlockSize c = sz) \<circ> cteCap) src s) \<and> is_aligned (word_of_nat idx) minUntypedSizeBits \<and> descendants_of' src (ctes_of s) = {}) \<and> ?P'1 s proof (prove)
goal (4 subgoals):
 1. \<And>cap. \<lbrace>?P'164 () cap\<rbrace> updateCap src (capFreeIndex_update (\<lambda>_. idx) cap) \<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>y. \<lbrace>?B159 y\<rbrace> getSlotCap src \<lbrace>\<lambda>cap s. sym_refs (state_refs_of' s) \<and> (cte_wp_at' (\<lambda>cte'. \<forall>p'\<in>zobj_refs' (cteCap cte') - zobj_refs' (capFreeIndex_update (\<lambda>_. idx) cap). ko_wp_at' (Not \<circ> live') p' s) src s \<and> if_live_then_nonz_cap' s) \<and> ?P'164 y cap s\<rbrace>
 3. \<lbrace>?P'81\<rbrace> do cap <- getSlotCap src;
y <- modify (\<lambda>ks. ks\<lparr>gsUntypedZeroRanges := case untypedZeroRange cap of None \<Rightarrow> gsUntypedZeroRanges ks | Some r \<Rightarrow> gsUntypedZeroRanges ks - {r}\<rparr>);
modify (\<lambda>ks. ks\<lparr>gsUntypedZeroRanges := case untypedZeroRange (capFreeIndex_update (\<lambda>_. idx) cap) of None \<Rightarrow> gsUntypedZeroRanges ks | Some r \<Rightarrow> insert r (gsUntypedZeroRanges ks)\<rparr>)
od \<lbrace>?B159\<rbrace>
 4. \<And>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> (\<exists>ptr sz. pspace_no_overlap' ptr sz s \<and> idx \<le> 2 ^ sz \<and> cte_wp_at' ((\<lambda>c. isUntypedCap c \<and> capPtr c = ptr \<and> capBlockSize c = sz) \<circ> cteCap) src s) \<and> is_aligned (word_of_nat idx) minUntypedSizeBits \<and> descendants_of' src (ctes_of s) = {} \<Longrightarrow> (valid_pspace' s \<and> (\<exists>ptr sz. pspace_no_overlap' ptr sz s \<and> idx \<le> 2 ^ sz \<and> cte_wp_at' ((\<lambda>c. isUntypedCap c \<and> capPtr c = ptr \<and> capBlockSize c = sz) \<circ> cteCap) src s) \<and> is_aligned (word_of_nat idx) minUntypedSizeBits \<and> descendants_of' src (ctes_of s) = {}) \<and> sch_act_wf (ksSchedulerAction s) s \<and> Invariants_H.valid_queues s \<and> ?P'81 s proof (prove)
goal (5 subgoals):
 1. \<And>cap. \<lbrace>?P169 () cap\<rbrace> updateCap src (capFreeIndex_update (\<lambda>_. idx) cap) \<lbrace>\<lambda>rv. if_unsafe_then_cap'\<rbrace>
 2. \<And>cap. \<lbrace>?P'168 () cap\<rbrace> updateCap src (capFreeIndex_update (\<lambda>_. idx) cap) \<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>
 3. \<And>y. \<lbrace>?B159 y\<rbrace> getSlotCap src \<lbrace>\<lambda>cap s. sym_refs (state_refs_of' s) \<and> (cte_wp_at' (\<lambda>cte'. \<forall>p'\<in>zobj_refs' (cteCap cte') - zobj_refs' (capFreeIndex_update (\<lambda>_. idx) cap). ko_wp_at' (Not \<circ> live') p' s) src s \<and> if_live_then_nonz_cap' s) \<and> ?P169 y cap s \<and> ?P'168 y cap s\<rbrace>
 4. \<lbrace>?P'81\<rbrace> do cap <- getSlotCap src;
y <- modify (\<lambda>ks. ks\<lparr>gsUntypedZeroRanges := case untypedZeroRange cap of None \<Rightarrow> gsUntypedZeroRanges ks | Some r \<Rightarrow> gsUntypedZeroRanges ks - {r}\<rparr>);
modify (\<lambda>ks. ks\<lparr>gsUntypedZeroRanges := case untypedZeroRange (capFreeIndex_update (\<lambda>_. idx) cap) of None \<Rightarrow> gsUntypedZeroRanges ks | Some r \<Rightarrow> insert r (gsUntypedZeroRanges ks)\<rparr>)
od \<lbrace>?B159\<rbrace>
 5. \<And>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> (\<exists>ptr sz. pspace_no_overlap' ptr sz s \<and> idx \<le> 2 ^ sz \<and> cte_wp_at' ((\<lambda>c. isUntypedCap c \<and> capPtr c = ptr \<and> capBlockSize c = sz) \<circ> cteCap) src s) \<and> is_aligned (word_of_nat idx) minUntypedSizeBits \<and> descendants_of' src (ctes_of s) = {} \<Longrightarrow> (valid_pspace' s \<and> (\<exists>ptr sz. pspace_no_overlap' ptr sz s \<and> idx \<le> 2 ^ sz \<and> cte_wp_at' ((\<lambda>c. isUntypedCap c \<and> capPtr c = ptr \<and> capBlockSize c = sz) \<circ> cteCap) src s) \<and> is_aligned (word_of_nat idx) minUntypedSizeBits \<and> descendants_of' src (ctes_of s) = {}) \<and> sch_act_wf (ksSchedulerAction s) s \<and> Invariants_H.valid_queues s \<and> ?P'81 s proof (prove)
goal (5 subgoals):
 1. \<And>cap. \<lbrace>?P169 () cap\<rbrace> updateCap src (capFreeIndex_update (\<lambda>_. idx) cap) \<lbrace>\<lambda>rv s. \<forall>cref. (\<exists>cap. cteCaps_of s cref = Some cap \<and> cap \<noteq> capability.NullCap) \<longrightarrow> (\<exists>cref' cap'. cteCaps_of s cref' = Some cap' \<and> cref \<in> cte_refs' cap' (irq_node' s))\<rbrace>
 2. \<And>cap. \<lbrace>?P'168 () cap\<rbrace> updateCap src (capFreeIndex_update (\<lambda>_. idx) cap) \<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>
 3. \<And>y. \<lbrace>?B159 y\<rbrace> getSlotCap src \<lbrace>\<lambda>cap s. sym_refs (state_refs_of' s) \<and> (cte_wp_at' (\<lambda>cte'. \<forall>p'\<in>zobj_refs' (cteCap cte') - zobj_refs' (capFreeIndex_update (\<lambda>_. idx) cap). ko_wp_at' (Not \<circ> live') p' s) src s \<and> if_live_then_nonz_cap' s) \<and> ?P169 y cap s \<and> ?P'168 y cap s\<rbrace>
 4. \<lbrace>?P'81\<rbrace> do cap <- getSlotCap src;
y <- modify (\<lambda>ks. ks\<lparr>gsUntypedZeroRanges := case untypedZeroRange cap of None \<Rightarrow> gsUntypedZeroRanges ks | Some r \<Rightarrow> gsUntypedZeroRanges ks - {r}\<rparr>);
modify (\<lambda>ks. ks\<lparr>gsUntypedZeroRanges := case untypedZeroRange (capFreeIndex_update (\<lambda>_. idx) cap) of None \<Rightarrow> gsUntypedZeroRanges ks | Some r \<Rightarrow> insert r (gsUntypedZeroRanges ks)\<rparr>)
od \<lbrace>?B159\<rbrace>
 5. \<And>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> (\<exists>ptr sz. pspace_no_overlap' ptr sz s \<and> idx \<le> 2 ^ sz \<and> cte_wp_at' ((\<lambda>c. isUntypedCap c \<and> capPtr c = ptr \<and> capBlockSize c = sz) \<circ> cteCap) src s) \<and> is_aligned (word_of_nat idx) minUntypedSizeBits \<and> descendants_of' src (ctes_of s) = {} \<Longrightarrow> (valid_pspace' s \<and> (\<exists>ptr sz. pspace_no_overlap' ptr sz s \<and> idx \<le> 2 ^ sz \<and> cte_wp_at' ((\<lambda>c. isUntypedCap c \<and> capPtr c = ptr \<and> capBlockSize c = sz) \<circ> cteCap) src s) \<and> is_aligned (word_of_nat idx) minUntypedSizeBits \<and> descendants_of' src (ctes_of s) = {}) \<and> sch_act_wf (ksSchedulerAction s) s \<and> Invariants_H.valid_queues s \<and> ?P'81 s proof (prove)
goal (4 subgoals):
 1. \<And>cap. \<lbrace>?P'190 () cap\<rbrace> updateCap src (capFreeIndex_update (\<lambda>_. idx) cap) \<lbrace>\<lambda>rv s. 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>y. \<lbrace>?B159 y\<rbrace> getSlotCap src \<lbrace>\<lambda>cap s. sym_refs (state_refs_of' s) \<and> (cte_wp_at' (\<lambda>cte'. \<forall>p'\<in>zobj_refs' (cteCap cte') - zobj_refs' (capFreeIndex_update (\<lambda>_. idx) cap). ko_wp_at' (Not \<circ> live') p' s) src s \<and> if_live_then_nonz_cap' s) \<and> (\<forall>cref. (\<exists>capa. modify_map (cteCaps_of s) src (K (capFreeIndex_update (\<lambda>_. idx) cap)) cref = Some capa \<and> capa \<noteq> capability.NullCap) \<longrightarrow> (\<exists>cref' cap'. modify_map (cteCaps_of s) src (K (capFreeIndex_update (\<lambda>_. idx) cap)) cref' = Some cap' \<and> cref \<in> cte_refs' cap' (irq_node' s))) \<and> valid_idle' s \<and> (valid_global_refs' and (\<lambda>s. kernel_data_refs \<inter> capRange (capFreeIndex_update (\<lambda>_. idx) cap) = {}) and (\<lambda>s. 2 ^ capBits (capFreeIndex_update (\<lambda>_. idx) cap) \<le> gsMaxObjectSize s)) s \<and> ?P'190 y cap s\<rbrace>
 3. \<lbrace>?P'81\<rbrace> do cap <- getSlotCap src;
y <- modify (\<lambda>ks. ks\<lparr>gsUntypedZeroRanges := case untypedZeroRange cap of None \<Rightarrow> gsUntypedZeroRanges ks | Some r \<Rightarrow> gsUntypedZeroRanges ks - {r}\<rparr>);
modify (\<lambda>ks. ks\<lparr>gsUntypedZeroRanges := case untypedZeroRange (capFreeIndex_update (\<lambda>_. idx) cap) of None \<Rightarrow> gsUntypedZeroRanges ks | Some r \<Rightarrow> insert r (gsUntypedZeroRanges ks)\<rparr>)
od \<lbrace>?B159\<rbrace>
 4. \<And>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> (\<exists>ptr sz. pspace_no_overlap' ptr sz s \<and> idx \<le> 2 ^ sz \<and> cte_wp_at' ((\<lambda>c. isUntypedCap c \<and> capPtr c = ptr \<and> capBlockSize c = sz) \<circ> cteCap) src s) \<and> is_aligned (word_of_nat idx) minUntypedSizeBits \<and> descendants_of' src (ctes_of s) = {} \<Longrightarrow> (valid_pspace' s \<and> (\<exists>ptr sz. pspace_no_overlap' ptr sz s \<and> idx \<le> 2 ^ sz \<and> cte_wp_at' ((\<lambda>c. isUntypedCap c \<and> capPtr c = ptr \<and> capBlockSize c = sz) \<circ> cteCap) src s) \<and> is_aligned (word_of_nat idx) minUntypedSizeBits \<and> descendants_of' src (ctes_of s) = {}) \<and> sch_act_wf (ksSchedulerAction s) s \<and> Invariants_H.valid_queues s \<and> ?P'81 s proof (prove)
goal (5 subgoals):
 1. \<And>cap. \<lbrace>?P196 () cap\<rbrace> updateCap src (capFreeIndex_update (\<lambda>_. idx) cap) \<lbrace>\<lambda>rv. valid_arch_state'\<rbrace>
 2. \<And>cap. \<lbrace>?P'195 () cap\<rbrace> updateCap src (capFreeIndex_update (\<lambda>_. idx) cap) \<lbrace>\<lambda>rv s. 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>y. \<lbrace>?B159 y\<rbrace> getSlotCap src \<lbrace>\<lambda>cap s. sym_refs (state_refs_of' s) \<and> (cte_wp_at' (\<lambda>cte'. \<forall>p'\<in>zobj_refs' (cteCap cte') - zobj_refs' (capFreeIndex_update (\<lambda>_. idx) cap). ko_wp_at' (Not \<circ> live') p' s) src s \<and> if_live_then_nonz_cap' s) \<and> (\<forall>cref. (\<exists>capa. modify_map (cteCaps_of s) src (K (capFreeIndex_update (\<lambda>_. idx) cap)) cref = Some capa \<and> capa \<noteq> capability.NullCap) \<longrightarrow> (\<exists>cref' cap'. modify_map (cteCaps_of s) src (K (capFreeIndex_update (\<lambda>_. idx) cap)) cref' = Some cap' \<and> cref \<in> cte_refs' cap' (irq_node' s))) \<and> valid_idle' s \<and> (valid_global_refs' and (\<lambda>s. kernel_data_refs \<inter> capRange (capFreeIndex_update (\<lambda>_. idx) cap) = {}) and (\<lambda>s. 2 ^ capBits (capFreeIndex_update (\<lambda>_. idx) cap) \<le> gsMaxObjectSize s)) s \<and> ?P196 y cap s \<and> ?P'195 y cap s\<rbrace>
 4. \<lbrace>?P'81\<rbrace> do cap <- getSlotCap src;
y <- modify (\<lambda>ks. ks\<lparr>gsUntypedZeroRanges := case untypedZeroRange cap of None \<Rightarrow> gsUntypedZeroRanges ks | Some r \<Rightarrow> gsUntypedZeroRanges ks - {r}\<rparr>);
modify (\<lambda>ks. ks\<lparr>gsUntypedZeroRanges := case untypedZeroRange (capFreeIndex_update (\<lambda>_. idx) cap) of None \<Rightarrow> gsUntypedZeroRanges ks | Some r \<Rightarrow> insert r (gsUntypedZeroRanges ks)\<rparr>)
od \<lbrace>?B159\<rbrace>
 5. \<And>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> (\<exists>ptr sz. pspace_no_overlap' ptr sz s \<and> idx \<le> 2 ^ sz \<and> cte_wp_at' ((\<lambda>c. isUntypedCap c \<and> capPtr c = ptr \<and> capBlockSize c = sz) \<circ> cteCap) src s) \<and> is_aligned (word_of_nat idx) minUntypedSizeBits \<and> descendants_of' src (ctes_of s) = {} \<Longrightarrow> (valid_pspace' s \<and> (\<exists>ptr sz. pspace_no_overlap' ptr sz s \<and> idx \<le> 2 ^ sz \<and> cte_wp_at' ((\<lambda>c. isUntypedCap c \<and> capPtr c = ptr \<and> capBlockSize c = sz) \<circ> cteCap) src s) \<and> is_aligned (word_of_nat idx) minUntypedSizeBits \<and> descendants_of' src (ctes_of s) = {}) \<and> sch_act_wf (ksSchedulerAction s) s \<and> Invariants_H.valid_queues s \<and> ?P'81 s proof (prove)
goal (5 subgoals):
 1. \<And>cap. \<lbrace>?P196 () cap\<rbrace> do cte <- getCTE src;
setCTE src (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. idx) cap) cte)
od \<lbrace>\<lambda>rv. valid_arch_state'\<rbrace>
 2. \<And>cap. \<lbrace>?P'195 () cap\<rbrace> updateCap src (capFreeIndex_update (\<lambda>_. idx) cap) \<lbrace>\<lambda>rv s. 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>y. \<lbrace>?B159 y\<rbrace> getSlotCap src \<lbrace>\<lambda>cap s. sym_refs (state_refs_of' s) \<and> (cte_wp_at' (\<lambda>cte'. \<forall>p'\<in>zobj_refs' (cteCap cte') - zobj_refs' (capFreeIndex_update (\<lambda>_. idx) cap). ko_wp_at' (Not \<circ> live') p' s) src s \<and> if_live_then_nonz_cap' s) \<and> (\<forall>cref. (\<exists>capa. modify_map (cteCaps_of s) src (K (capFreeIndex_update (\<lambda>_. idx) cap)) cref = Some capa \<and> capa \<noteq> capability.NullCap) \<longrightarrow> (\<exists>cref' cap'. modify_map (cteCaps_of s) src (K (capFreeIndex_update (\<lambda>_. idx) cap)) cref' = Some cap' \<and> cref \<in> cte_refs' cap' (irq_node' s))) \<and> valid_idle' s \<and> (valid_global_refs' and (\<lambda>s. kernel_data_refs \<inter> capRange (capFreeIndex_update (\<lambda>_. idx) cap) = {}) and (\<lambda>s. 2 ^ capBits (capFreeIndex_update (\<lambda>_. idx) cap) \<le> gsMaxObjectSize s)) s \<and> ?P196 y cap s \<and> ?P'195 y cap s\<rbrace>
 4. \<lbrace>?P'81\<rbrace> do cap <- getSlotCap src;
y <- modify (\<lambda>ks. ks\<lparr>gsUntypedZeroRanges := case untypedZeroRange cap of None \<Rightarrow> gsUntypedZeroRanges ks | Some r \<Rightarrow> gsUntypedZeroRanges ks - {r}\<rparr>);
modify (\<lambda>ks. ks\<lparr>gsUntypedZeroRanges := case untypedZeroRange (capFreeIndex_update (\<lambda>_. idx) cap) of None \<Rightarrow> gsUntypedZeroRanges ks | Some r \<Rightarrow> insert r (gsUntypedZeroRanges ks)\<rparr>)
od \<lbrace>?B159\<rbrace>
 5. \<And>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> (\<exists>ptr sz. pspace_no_overlap' ptr sz s \<and> idx \<le> 2 ^ sz \<and> cte_wp_at' ((\<lambda>c. isUntypedCap c \<and> capPtr c = ptr \<and> capBlockSize c = sz) \<circ> cteCap) src s) \<and> is_aligned (word_of_nat idx) minUntypedSizeBits \<and> descendants_of' src (ctes_of s) = {} \<Longrightarrow> (valid_pspace' s \<and> (\<exists>ptr sz. pspace_no_overlap' ptr sz s \<and> idx \<le> 2 ^ sz \<and> cte_wp_at' ((\<lambda>c. isUntypedCap c \<and> capPtr c = ptr \<and> capBlockSize c = sz) \<circ> cteCap) src s) \<and> is_aligned (word_of_nat idx) minUntypedSizeBits \<and> descendants_of' src (ctes_of s) = {}) \<and> sch_act_wf (ksSchedulerAction s) s \<and> Invariants_H.valid_queues s \<and> ?P'81 s proof (prove)
goal (4 subgoals):
 1. \<And>cap. \<lbrace>?P'195 () cap\<rbrace> updateCap src (capFreeIndex_update (\<lambda>_. idx) cap) \<lbrace>\<lambda>rv s. 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>y. \<lbrace>?B159 y\<rbrace> getSlotCap src \<lbrace>\<lambda>cap s. sym_refs (state_refs_of' s) \<and> (cte_wp_at' (\<lambda>cte'. \<forall>p'\<in>zobj_refs' (cteCap cte') - zobj_refs' (capFreeIndex_update (\<lambda>_. idx) cap). ko_wp_at' (Not \<circ> live') p' s) src s \<and> if_live_then_nonz_cap' s) \<and> (\<forall>cref. (\<exists>capa. modify_map (cteCaps_of s) src (K (capFreeIndex_update (\<lambda>_. idx) cap)) cref = Some capa \<and> capa \<noteq> capability.NullCap) \<longrightarrow> (\<exists>cref' cap'. modify_map (cteCaps_of s) src (K (capFreeIndex_update (\<lambda>_. idx) cap)) cref' = Some cap' \<and> cref \<in> cte_refs' cap' (irq_node' s))) \<and> valid_idle' s \<and> (valid_global_refs' and (\<lambda>s. kernel_data_refs \<inter> capRange (capFreeIndex_update (\<lambda>_. idx) cap) = {}) and (\<lambda>s. 2 ^ capBits (capFreeIndex_update (\<lambda>_. idx) cap) \<le> gsMaxObjectSize s)) s \<and> valid_arch_state' s \<and> ?P'195 y cap s\<rbrace>
 3. \<lbrace>?P'81\<rbrace> do cap <- getSlotCap src;
y <- modify (\<lambda>ks. ks\<lparr>gsUntypedZeroRanges := case untypedZeroRange cap of None \<Rightarrow> gsUntypedZeroRanges ks | Some r \<Rightarrow> gsUntypedZeroRanges ks - {r}\<rparr>);
modify (\<lambda>ks. ks\<lparr>gsUntypedZeroRanges := case untypedZeroRange (capFreeIndex_update (\<lambda>_. idx) cap) of None \<Rightarrow> gsUntypedZeroRanges ks | Some r \<Rightarrow> insert r (gsUntypedZeroRanges ks)\<rparr>)
od \<lbrace>?B159\<rbrace>
 4. \<And>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> (\<exists>ptr sz. pspace_no_overlap' ptr sz s \<and> idx \<le> 2 ^ sz \<and> cte_wp_at' ((\<lambda>c. isUntypedCap c \<and> capPtr c = ptr \<and> capBlockSize c = sz) \<circ> cteCap) src s) \<and> is_aligned (word_of_nat idx) minUntypedSizeBits \<and> descendants_of' src (ctes_of s) = {} \<Longrightarrow> (valid_pspace' s \<and> (\<exists>ptr sz. pspace_no_overlap' ptr sz s \<and> idx \<le> 2 ^ sz \<and> cte_wp_at' ((\<lambda>c. isUntypedCap c \<and> capPtr c = ptr \<and> capBlockSize c = sz) \<circ> cteCap) src s) \<and> is_aligned (word_of_nat idx) minUntypedSizeBits \<and> descendants_of' src (ctes_of s) = {}) \<and> sch_act_wf (ksSchedulerAction s) s \<and> Invariants_H.valid_queues s \<and> ?P'81 s proof (prove)
goal (4 subgoals):
 1. \<And>cap. \<lbrace>?P'206 () cap\<rbrace> updateCap src (capFreeIndex_update (\<lambda>_. idx) cap) \<lbrace>\<lambda>rv s. 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>y. \<lbrace>?B159 y\<rbrace> getSlotCap src \<lbrace>\<lambda>cap s. sym_refs (state_refs_of' s) \<and> (cte_wp_at' (\<lambda>cte'. \<forall>p'\<in>zobj_refs' (cteCap cte') - zobj_refs' (capFreeIndex_update (\<lambda>_. idx) cap). ko_wp_at' (Not \<circ> live') p' s) src s \<and> if_live_then_nonz_cap' s) \<and> (\<forall>cref. (\<exists>capa. modify_map (cteCaps_of s) src (K (capFreeIndex_update (\<lambda>_. idx) cap)) cref = Some capa \<and> capa \<noteq> capability.NullCap) \<longrightarrow> (\<exists>cref' cap'. modify_map (cteCaps_of s) src (K (capFreeIndex_update (\<lambda>_. idx) cap)) cref' = Some cap' \<and> cref \<in> cte_refs' cap' (irq_node' s))) \<and> valid_idle' s \<and> (valid_global_refs' and (\<lambda>s. kernel_data_refs \<inter> capRange (capFreeIndex_update (\<lambda>_. idx) cap) = {}) and (\<lambda>s. 2 ^ capBits (capFreeIndex_update (\<lambda>_. idx) cap) \<le> gsMaxObjectSize s)) s \<and> valid_arch_state' s \<and> valid_irq_node' (irq_node' s) s \<and> ?P'206 y cap s\<rbrace>
 3. \<lbrace>?P'81\<rbrace> do cap <- getSlotCap src;
y <- modify (\<lambda>ks. ks\<lparr>gsUntypedZeroRanges := case untypedZeroRange cap of None \<Rightarrow> gsUntypedZeroRanges ks | Some r \<Rightarrow> gsUntypedZeroRanges ks - {r}\<rparr>);
modify (\<lambda>ks. ks\<lparr>gsUntypedZeroRanges := case untypedZeroRange (capFreeIndex_update (\<lambda>_. idx) cap) of None \<Rightarrow> gsUntypedZeroRanges ks | Some r \<Rightarrow> insert r (gsUntypedZeroRanges ks)\<rparr>)
od \<lbrace>?B159\<rbrace>
 4. \<And>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> (\<exists>ptr sz. pspace_no_overlap' ptr sz s \<and> idx \<le> 2 ^ sz \<and> cte_wp_at' ((\<lambda>c. isUntypedCap c \<and> capPtr c = ptr \<and> capBlockSize c = sz) \<circ> cteCap) src s) \<and> is_aligned (word_of_nat idx) minUntypedSizeBits \<and> descendants_of' src (ctes_of s) = {} \<Longrightarrow> (valid_pspace' s \<and> (\<exists>ptr sz. pspace_no_overlap' ptr sz s \<and> idx \<le> 2 ^ sz \<and> cte_wp_at' ((\<lambda>c. isUntypedCap c \<and> capPtr c = ptr \<and> capBlockSize c = sz) \<circ> cteCap) src s) \<and> is_aligned (word_of_nat idx) minUntypedSizeBits \<and> descendants_of' src (ctes_of s) = {}) \<and> sch_act_wf (ksSchedulerAction s) s \<and> Invariants_H.valid_queues s \<and> ?P'81 s proof (prove)
goal (5 subgoals):
 1. \<And>cap. \<lbrace>?P216 () cap\<rbrace> updateCap src (capFreeIndex_update (\<lambda>_. idx) cap) \<lbrace>\<lambda>rv. valid_irq_handlers'\<rbrace>
 2. \<And>cap. \<lbrace>?P'215 () cap\<rbrace> updateCap src (capFreeIndex_update (\<lambda>_. idx) cap) \<lbrace>\<lambda>rv s. 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>y. \<lbrace>?B159 y\<rbrace> getSlotCap src \<lbrace>\<lambda>cap s. sym_refs (state_refs_of' s) \<and> (cte_wp_at' (\<lambda>cte'. \<forall>p'\<in>zobj_refs' (cteCap cte') - zobj_refs' (capFreeIndex_update (\<lambda>_. idx) cap). ko_wp_at' (Not \<circ> live') p' s) src s \<and> if_live_then_nonz_cap' s) \<and> (\<forall>cref. (\<exists>capa. modify_map (cteCaps_of s) src (K (capFreeIndex_update (\<lambda>_. idx) cap)) cref = Some capa \<and> capa \<noteq> capability.NullCap) \<longrightarrow> (\<exists>cref' cap'. modify_map (cteCaps_of s) src (K (capFreeIndex_update (\<lambda>_. idx) cap)) cref' = Some cap' \<and> cref \<in> cte_refs' cap' (irq_node' s))) \<and> valid_idle' s \<and> (valid_global_refs' and (\<lambda>s. kernel_data_refs \<inter> capRange (capFreeIndex_update (\<lambda>_. idx) cap) = {}) and (\<lambda>s. 2 ^ capBits (capFreeIndex_update (\<lambda>_. idx) cap) \<le> gsMaxObjectSize s)) s \<and> valid_arch_state' s \<and> valid_irq_node' (irq_node' s) s \<and> ?P216 y cap s \<and> ?P'215 y cap s\<rbrace>
 4. \<lbrace>?P'81\<rbrace> do cap <- getSlotCap src;
y <- modify (\<lambda>ks. ks\<lparr>gsUntypedZeroRanges := case untypedZeroRange cap of None \<Rightarrow> gsUntypedZeroRanges ks | Some r \<Rightarrow> gsUntypedZeroRanges ks - {r}\<rparr>);
modify (\<lambda>ks. ks\<lparr>gsUntypedZeroRanges := case untypedZeroRange (capFreeIndex_update (\<lambda>_. idx) cap) of None \<Rightarrow> gsUntypedZeroRanges ks | Some r \<Rightarrow> insert r (gsUntypedZeroRanges ks)\<rparr>)
od \<lbrace>?B159\<rbrace>
 5. \<And>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> (\<exists>ptr sz. pspace_no_overlap' ptr sz s \<and> idx \<le> 2 ^ sz \<and> cte_wp_at' ((\<lambda>c. isUntypedCap c \<and> capPtr c = ptr \<and> capBlockSize c = sz) \<circ> cteCap) src s) \<and> is_aligned (word_of_nat idx) minUntypedSizeBits \<and> descendants_of' src (ctes_of s) = {} \<Longrightarrow> (valid_pspace' s \<and> (\<exists>ptr sz. pspace_no_overlap' ptr sz s \<and> idx \<le> 2 ^ sz \<and> cte_wp_at' ((\<lambda>c. isUntypedCap c \<and> capPtr c = ptr \<and> capBlockSize c = sz) \<circ> cteCap) src s) \<and> is_aligned (word_of_nat idx) minUntypedSizeBits \<and> descendants_of' src (ctes_of s) = {}) \<and> sch_act_wf (ksSchedulerAction s) s \<and> Invariants_H.valid_queues s \<and> ?P'81 s proof (prove)
goal (5 subgoals):
 1. \<And>cap. \<lbrace>?P216 () cap\<rbrace> do cte <- getCTE src;
setCTE src (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. idx) cap) cte)
od \<lbrace>\<lambda>rv. valid_irq_handlers'\<rbrace>
 2. \<And>cap. \<lbrace>?P'215 () cap\<rbrace> updateCap src (capFreeIndex_update (\<lambda>_. idx) cap) \<lbrace>\<lambda>rv s. 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>y. \<lbrace>?B159 y\<rbrace> getSlotCap src \<lbrace>\<lambda>cap s. sym_refs (state_refs_of' s) \<and> (cte_wp_at' (\<lambda>cte'. \<forall>p'\<in>zobj_refs' (cteCap cte') - zobj_refs' (capFreeIndex_update (\<lambda>_. idx) cap). ko_wp_at' (Not \<circ> live') p' s) src s \<and> if_live_then_nonz_cap' s) \<and> (\<forall>cref. (\<exists>capa. modify_map (cteCaps_of s) src (K (capFreeIndex_update (\<lambda>_. idx) cap)) cref = Some capa \<and> capa \<noteq> capability.NullCap) \<longrightarrow> (\<exists>cref' cap'. modify_map (cteCaps_of s) src (K (capFreeIndex_update (\<lambda>_. idx) cap)) cref' = Some cap' \<and> cref \<in> cte_refs' cap' (irq_node' s))) \<and> valid_idle' s \<and> (valid_global_refs' and (\<lambda>s. kernel_data_refs \<inter> capRange (capFreeIndex_update (\<lambda>_. idx) cap) = {}) and (\<lambda>s. 2 ^ capBits (capFreeIndex_update (\<lambda>_. idx) cap) \<le> gsMaxObjectSize s)) s \<and> valid_arch_state' s \<and> valid_irq_node' (irq_node' s) s \<and> ?P216 y cap s \<and> ?P'215 y cap s\<rbrace>
 4. \<lbrace>?P'81\<rbrace> do cap <- getSlotCap src;
y <- modify (\<lambda>ks. ks\<lparr>gsUntypedZeroRanges := case untypedZeroRange cap of None \<Rightarrow> gsUntypedZeroRanges ks | Some r \<Rightarrow> gsUntypedZeroRanges ks - {r}\<rparr>);
modify (\<lambda>ks. ks\<lparr>gsUntypedZeroRanges := case untypedZeroRange (capFreeIndex_update (\<lambda>_. idx) cap) of None \<Rightarrow> gsUntypedZeroRanges ks | Some r \<Rightarrow> insert r (gsUntypedZeroRanges ks)\<rparr>)
od \<lbrace>?B159\<rbrace>
 5. \<And>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> (\<exists>ptr sz. pspace_no_overlap' ptr sz s \<and> idx \<le> 2 ^ sz \<and> cte_wp_at' ((\<lambda>c. isUntypedCap c \<and> capPtr c = ptr \<and> capBlockSize c = sz) \<circ> cteCap) src s) \<and> is_aligned (word_of_nat idx) minUntypedSizeBits \<and> descendants_of' src (ctes_of s) = {} \<Longrightarrow> (valid_pspace' s \<and> (\<exists>ptr sz. pspace_no_overlap' ptr sz s \<and> idx \<le> 2 ^ sz \<and> cte_wp_at' ((\<lambda>c. isUntypedCap c \<and> capPtr c = ptr \<and> capBlockSize c = sz) \<circ> cteCap) src s) \<and> is_aligned (word_of_nat idx) minUntypedSizeBits \<and> descendants_of' src (ctes_of s) = {}) \<and> sch_act_wf (ksSchedulerAction s) s \<and> Invariants_H.valid_queues s \<and> ?P'81 s proof (prove)
goal (4 subgoals):
 1. \<And>cap. \<lbrace>?P'215 () cap\<rbrace> updateCap src (capFreeIndex_update (\<lambda>_. idx) cap) \<lbrace>\<lambda>rv s. 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>y. \<lbrace>?B159 y\<rbrace> getSlotCap src \<lbrace>\<lambda>cap s. sym_refs (state_refs_of' s) \<and> (cte_wp_at' (\<lambda>cte'. \<forall>p'\<in>zobj_refs' (cteCap cte') - zobj_refs' (capFreeIndex_update (\<lambda>_. idx) cap). ko_wp_at' (Not \<circ> live') p' s) src s \<and> if_live_then_nonz_cap' s) \<and> (\<forall>cref. (\<exists>capa. modify_map (cteCaps_of s) src (K (capFreeIndex_update (\<lambda>_. idx) cap)) cref = Some capa \<and> capa \<noteq> capability.NullCap) \<longrightarrow> (\<exists>cref' cap'. modify_map (cteCaps_of s) src (K (capFreeIndex_update (\<lambda>_. idx) cap)) cref' = Some cap' \<and> cref \<in> cte_refs' cap' (irq_node' s))) \<and> valid_idle' s \<and> (valid_global_refs' and (\<lambda>s. kernel_data_refs \<inter> capRange (capFreeIndex_update (\<lambda>_. idx) cap) = {}) and (\<lambda>s. 2 ^ capBits (capFreeIndex_update (\<lambda>_. idx) cap) \<le> gsMaxObjectSize s)) s \<and> valid_arch_state' s \<and> valid_irq_node' (irq_node' s) s \<and> (cte_wp_at' (\<lambda>_. True) src s \<longrightarrow> (\<exists>cte. cte_wp_at' ((=) cte) src s \<and> valid_irq_handlers' s \<and> (\<forall>irq. cteCap (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. idx) cap) cte) = capability.IRQHandlerCap irq \<longrightarrow> irq_issued' irq s))) \<and> ?P'215 y cap s\<rbrace>
 3. \<lbrace>?P'81\<rbrace> do cap <- getSlotCap src;
y <- modify (\<lambda>ks. ks\<lparr>gsUntypedZeroRanges := case untypedZeroRange cap of None \<Rightarrow> gsUntypedZeroRanges ks | Some r \<Rightarrow> gsUntypedZeroRanges ks - {r}\<rparr>);
modify (\<lambda>ks. ks\<lparr>gsUntypedZeroRanges := case untypedZeroRange (capFreeIndex_update (\<lambda>_. idx) cap) of None \<Rightarrow> gsUntypedZeroRanges ks | Some r \<Rightarrow> insert r (gsUntypedZeroRanges ks)\<rparr>)
od \<lbrace>?B159\<rbrace>
 4. \<And>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> (\<exists>ptr sz. pspace_no_overlap' ptr sz s \<and> idx \<le> 2 ^ sz \<and> cte_wp_at' ((\<lambda>c. isUntypedCap c \<and> capPtr c = ptr \<and> capBlockSize c = sz) \<circ> cteCap) src s) \<and> is_aligned (word_of_nat idx) minUntypedSizeBits \<and> descendants_of' src (ctes_of s) = {} \<Longrightarrow> (valid_pspace' s \<and> (\<exists>ptr sz. pspace_no_overlap' ptr sz s \<and> idx \<le> 2 ^ sz \<and> cte_wp_at' ((\<lambda>c. isUntypedCap c \<and> capPtr c = ptr \<and> capBlockSize c = sz) \<circ> cteCap) src s) \<and> is_aligned (word_of_nat idx) minUntypedSizeBits \<and> descendants_of' src (ctes_of s) = {}) \<and> sch_act_wf (ksSchedulerAction s) s \<and> Invariants_H.valid_queues s \<and> ?P'81 s proof (prove)
goal (4 subgoals):
 1. \<And>cap. \<lbrace>?P'215 () cap\<rbrace> do cte <- getCTE src;
setCTE src (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. idx) cap) cte)
od \<lbrace>\<lambda>rv s. 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>y. \<lbrace>?B159 y\<rbrace> getSlotCap src \<lbrace>\<lambda>cap s. sym_refs (state_refs_of' s) \<and> (cte_wp_at' (\<lambda>cte'. \<forall>p'\<in>zobj_refs' (cteCap cte') - zobj_refs' (capFreeIndex_update (\<lambda>_. idx) cap). ko_wp_at' (Not \<circ> live') p' s) src s \<and> if_live_then_nonz_cap' s) \<and> (\<forall>cref. (\<exists>capa. modify_map (cteCaps_of s) src (K (capFreeIndex_update (\<lambda>_. idx) cap)) cref = Some capa \<and> capa \<noteq> capability.NullCap) \<longrightarrow> (\<exists>cref' cap'. modify_map (cteCaps_of s) src (K (capFreeIndex_update (\<lambda>_. idx) cap)) cref' = Some cap' \<and> cref \<in> cte_refs' cap' (irq_node' s))) \<and> valid_idle' s \<and> (valid_global_refs' and (\<lambda>s. kernel_data_refs \<inter> capRange (capFreeIndex_update (\<lambda>_. idx) cap) = {}) and (\<lambda>s. 2 ^ capBits (capFreeIndex_update (\<lambda>_. idx) cap) \<le> gsMaxObjectSize s)) s \<and> valid_arch_state' s \<and> valid_irq_node' (irq_node' s) s \<and> (cte_wp_at' (\<lambda>_. True) src s \<longrightarrow> (\<exists>cte. cte_wp_at' ((=) cte) src s \<and> valid_irq_handlers' s \<and> (\<forall>irq. cteCap (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. idx) cap) cte) = capability.IRQHandlerCap irq \<longrightarrow> irq_issued' irq s))) \<and> ?P'215 y cap s\<rbrace>
 3. \<lbrace>?P'81\<rbrace> do cap <- getSlotCap src;
y <- modify (\<lambda>ks. ks\<lparr>gsUntypedZeroRanges := case untypedZeroRange cap of None \<Rightarrow> gsUntypedZeroRanges ks | Some r \<Rightarrow> gsUntypedZeroRanges ks - {r}\<rparr>);
modify (\<lambda>ks. ks\<lparr>gsUntypedZeroRanges := case untypedZeroRange (capFreeIndex_update (\<lambda>_. idx) cap) of None \<Rightarrow> gsUntypedZeroRanges ks | Some r \<Rightarrow> insert r (gsUntypedZeroRanges ks)\<rparr>)
od \<lbrace>?B159\<rbrace>
 4. \<And>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> (\<exists>ptr sz. pspace_no_overlap' ptr sz s \<and> idx \<le> 2 ^ sz \<and> cte_wp_at' ((\<lambda>c. isUntypedCap c \<and> capPtr c = ptr \<and> capBlockSize c = sz) \<circ> cteCap) src s) \<and> is_aligned (word_of_nat idx) minUntypedSizeBits \<and> descendants_of' src (ctes_of s) = {} \<Longrightarrow> (valid_pspace' s \<and> (\<exists>ptr sz. pspace_no_overlap' ptr sz s \<and> idx \<le> 2 ^ sz \<and> cte_wp_at' ((\<lambda>c. isUntypedCap c \<and> capPtr c = ptr \<and> capBlockSize c = sz) \<circ> cteCap) src s) \<and> is_aligned (word_of_nat idx) minUntypedSizeBits \<and> descendants_of' src (ctes_of s) = {}) \<and> sch_act_wf (ksSchedulerAction s) s \<and> Invariants_H.valid_queues s \<and> ?P'81 s proof (prove)
goal (1 subgoal):
 1. \<And>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> (\<exists>ptr sz. pspace_no_overlap' ptr sz s \<and> idx \<le> 2 ^ sz \<and> (\<exists>cte. ctes_of s src = Some cte \<and> isUntypedCap (cteCap cte) \<and> capPtr (cteCap cte) = ptr \<and> capBlockSize (cteCap cte) = sz)) \<and> is_aligned (word_of_nat idx) minUntypedSizeBits \<and> descendants_of' src (ctes_of s) = {} \<Longrightarrow> (\<exists>cte. ctes_of s src = Some cte) \<longrightarrow> (\<exists>cte. ctes_of s src = Some cte \<and> (\<exists>ctea. ctes_of s src = Some ctea \<and> (\<exists>cte. ctes_of s src = Some cte \<and> (\<forall>p'\<in>zobj_refs' (cteCap cte) - zobj_refs' (capFreeIndex_update (\<lambda>_. idx) (cteCap ctea)). ko_wp_at' (\<lambda>a. \<not> live' a) p' s)) \<and> (\<forall>cref. (\<exists>cap. modify_map (cteCaps_of s) src (\<lambda>a. capFreeIndex_update (\<lambda>_. idx) (cteCap ctea)) cref = Some cap \<and> cap \<noteq> capability.NullCap) \<longrightarrow> (\<exists>cref' cap'. modify_map (cteCaps_of s) src (\<lambda>a. capFreeIndex_update (\<lambda>_. idx) (cteCap ctea)) cref' = Some cap' \<and> cref \<in> cte_refs' cap' (irq_node' s))) \<and> kernel_data_refs \<inter> capRange (capFreeIndex_update (\<lambda>_. idx) (cteCap ctea)) = {} \<and> 2 ^ capBits (capFreeIndex_update (\<lambda>_. idx) (cteCap ctea)) \<le> gsMaxObjectSize s \<and> (\<forall>irq. capFreeIndex_update (\<lambda>_. idx) (cteCap ctea) = capability.IRQHandlerCap irq \<longrightarrow> irq_issued' irq s) \<and> ksDomSchedule (KernelInit_H.newKernelState undefined) \<noteq> [] \<and> untyped_ranges_zero_inv (\<lambda>a. if a = src then Some (capFreeIndex_update (\<lambda>_. idx) (cteCap ctea)) else cteCaps_of (s\<lparr>gsUntypedZeroRanges := case untypedZeroRange (cteCap cte) of None \<Rightarrow> gsUntypedZeroRanges s | Some r \<Rightarrow> gsUntypedZeroRanges s - {r}, gsUntypedZeroRanges := case untypedZeroRange (capFreeIndex_update (\<lambda>_. idx) (cteCap cte)) of None \<Rightarrow> gsUntypedZeroRanges (s\<lparr>gsUntypedZeroRanges := case untypedZeroRange (cteCap cte) of None \<Rightarrow> gsUntypedZeroRanges s | Some r \<Rightarrow> gsUntypedZeroRanges s - {r}\<rparr>) | Some r \<Rightarrow> insert r (gsUntypedZeroRanges (s\<lparr>gsUntypedZeroRanges := case untypedZeroRange (cteCap cte) of None \<Rightarrow> gsUntypedZeroRanges s | Some r \<Rightarrow> gsUntypedZeroRanges s - {r}\<rparr>))\<rparr>) a) (case untypedZeroRange (capFreeIndex_update (\<lambda>_. idx) (cteCap cte)) of None \<Rightarrow> case untypedZeroRange (cteCap cte) of None \<Rightarrow> gsUntypedZeroRanges s | Some r \<Rightarrow> gsUntypedZeroRanges s - {r} | Some r \<Rightarrow> insert r (case untypedZeroRange (cteCap cte) of None \<Rightarrow> gsUntypedZeroRanges s | Some r \<Rightarrow> gsUntypedZeroRanges s - {r})))) proof (prove)
goal (1 subgoal):
 1. \<And>s cte. \<lbrakk>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; is_aligned (word_of_nat idx) minUntypedSizeBits; descendants_of' src (ctes_of s) = {}; pspace_no_overlap' (capPtr (cteCap cte)) (capBlockSize (cteCap cte)) s; idx \<le> 2 ^ capBlockSize (cteCap cte); isUntypedCap (cteCap cte); ctes_of s src = Some cte\<rbrakk> \<Longrightarrow> (\<forall>cref. (\<exists>cap. modify_map (cteCaps_of s) src (\<lambda>a. capFreeIndex_update (\<lambda>_. idx) (cteCap cte)) cref = Some cap \<and> cap \<noteq> capability.NullCap) \<longrightarrow> (\<exists>cref' cap'. modify_map (cteCaps_of s) src (\<lambda>a. capFreeIndex_update (\<lambda>_. idx) (cteCap cte)) cref' = Some cap' \<and> cref \<in> cte_refs' cap' (irq_node' s))) \<and> kernel_data_refs \<inter> capRange (capFreeIndex_update (\<lambda>_. idx) (cteCap cte)) = {} \<and> 2 ^ capBits (capFreeIndex_update (\<lambda>_. idx) (cteCap cte)) \<le> gsMaxObjectSize s \<and> (\<forall>irq. capFreeIndex_update (\<lambda>_. idx) (cteCap cte) = capability.IRQHandlerCap irq \<longrightarrow> irq_issued' irq s) \<and> untyped_ranges_zero_inv ((cteCaps_of s)(src \<mapsto> capFreeIndex_update (\<lambda>_. idx) (cteCap cte))) (case untypedZeroRange (capFreeIndex_update (\<lambda>_. idx) (cteCap cte)) of None \<Rightarrow> case untypedZeroRange (cteCap cte) of None \<Rightarrow> gsUntypedZeroRanges s | Some r \<Rightarrow> gsUntypedZeroRanges s - {r} | Some r \<Rightarrow> insert r (case untypedZeroRange (cteCap cte) of None \<Rightarrow> gsUntypedZeroRanges s | Some r \<Rightarrow> gsUntypedZeroRanges s - {r})) proof (prove)
goal (1 subgoal):
 1. \<And>s cte d v0 v1 f. \<lbrakk>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; is_aligned (word_of_nat idx) minUntypedSizeBits; descendants_of' src (ctes_of s) = {}; pspace_no_overlap' v0 v1 s; idx \<le> 2 ^ v1; ctes_of s src = Some cte; cteCap cte = capability.UntypedCap d v0 v1 f\<rbrakk> \<Longrightarrow> (\<forall>cref. (\<exists>cap. modify_map (cteCaps_of s) src (\<lambda>a. capability.UntypedCap d v0 v1 idx) cref = Some cap \<and> cap \<noteq> capability.NullCap) \<longrightarrow> (\<exists>cref' cap'. modify_map (cteCaps_of s) src (\<lambda>a. capability.UntypedCap d v0 v1 idx) cref' = Some cap' \<and> cref \<in> cte_refs' cap' (irq_node' s))) \<and> kernel_data_refs \<inter> {v0..v0 + 2 ^ v1 - 1} = {} \<and> 2 ^ v1 \<le> gsMaxObjectSize s \<and> untyped_ranges_zero_inv ((cteCaps_of s)(src \<mapsto> capability.UntypedCap d v0 v1 idx)) (case untypedZeroRange (capability.UntypedCap d v0 v1 idx) of None \<Rightarrow> case untypedZeroRange (capability.UntypedCap d v0 v1 f) of None \<Rightarrow> gsUntypedZeroRanges s | Some r \<Rightarrow> gsUntypedZeroRanges s - {r} | Some r \<Rightarrow> insert r (case untypedZeroRange (capability.UntypedCap d v0 v1 f) of None \<Rightarrow> gsUntypedZeroRanges s | Some r \<Rightarrow> gsUntypedZeroRanges s - {r})) proof (prove)
goal (1 subgoal):
 1. \<And>s cte d v0 v1 f. \<lbrakk>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; is_aligned (word_of_nat idx) minUntypedSizeBits; descendants_of' src (ctes_of s) = {}; pspace_no_overlap' v0 v1 s; idx \<le> 2 ^ v1; ctes_of s src = Some cte; cteCap cte = capability.UntypedCap d v0 v1 f; kernel_data_refs \<inter> capRange (cteCap cte) = {} \<and> global_refs' s \<subseteq> kernel_data_refs \<and> 2 ^ capBits (cteCap cte) \<le> gsMaxObjectSize s\<rbrakk> \<Longrightarrow> (\<forall>cref. (\<exists>cap. modify_map (cteCaps_of s) src (\<lambda>a. capability.UntypedCap d v0 v1 idx) cref = Some cap \<and> cap \<noteq> capability.NullCap) \<longrightarrow> (\<exists>cref' cap'. modify_map (cteCaps_of s) src (\<lambda>a. capability.UntypedCap d v0 v1 idx) cref' = Some cap' \<and> cref \<in> cte_refs' cap' (irq_node' s))) \<and> kernel_data_refs \<inter> {v0..v0 + 2 ^ v1 - 1} = {} \<and> 2 ^ v1 \<le> gsMaxObjectSize s \<and> untyped_ranges_zero_inv ((cteCaps_of s)(src \<mapsto> capability.UntypedCap d v0 v1 idx)) (case untypedZeroRange (capability.UntypedCap d v0 v1 idx) of None \<Rightarrow> case untypedZeroRange (capability.UntypedCap d v0 v1 f) of None \<Rightarrow> gsUntypedZeroRanges s | Some r \<Rightarrow> gsUntypedZeroRanges s - {r} | Some r \<Rightarrow> insert r (case untypedZeroRange (capability.UntypedCap d v0 v1 f) of None \<Rightarrow> gsUntypedZeroRanges s | Some r \<Rightarrow> gsUntypedZeroRanges s - {r})) proof (prove)
goal (1 subgoal):
 1. \<And>s cte d v0 v1 f. \<lbrakk>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; is_aligned (word_of_nat idx) minUntypedSizeBits; descendants_of' src (ctes_of s) = {}; pspace_no_overlap' v0 v1 s; idx \<le> 2 ^ v1; ctes_of s src = Some cte; cteCap cte = capability.UntypedCap d v0 v1 f; kernel_data_refs \<inter> {v0..v0 + 2 ^ v1 - 1} = {}; global_refs' s \<subseteq> kernel_data_refs; 2 ^ v1 \<le> gsMaxObjectSize s\<rbrakk> \<Longrightarrow> (\<forall>cref. (\<exists>cap. modify_map (cteCaps_of s) src (\<lambda>a. capability.UntypedCap d v0 v1 idx) cref = Some cap \<and> cap \<noteq> capability.NullCap) \<longrightarrow> (\<exists>cref' cap'. modify_map (cteCaps_of s) src (\<lambda>a. capability.UntypedCap d v0 v1 idx) cref' = Some cap' \<and> cref \<in> cte_refs' cap' (irq_node' s))) \<and> untyped_ranges_zero_inv ((cteCaps_of s)(src \<mapsto> capability.UntypedCap d v0 v1 idx)) (case untypedZeroRange (capability.UntypedCap d v0 v1 idx) of None \<Rightarrow> case untypedZeroRange (capability.UntypedCap d v0 v1 f) of None \<Rightarrow> gsUntypedZeroRanges s | Some r \<Rightarrow> gsUntypedZeroRanges s - {r} | Some r \<Rightarrow> insert r (case untypedZeroRange (capability.UntypedCap d v0 v1 f) of None \<Rightarrow> gsUntypedZeroRanges s | Some r \<Rightarrow> gsUntypedZeroRanges s - {r})) proof (prove)
goal (2 subgoals):
 1. \<And>s cte d v0 v1 f cref. \<lbrakk>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; is_aligned (word_of_nat idx) minUntypedSizeBits; descendants_of' src (ctes_of s) = {}; pspace_no_overlap' v0 v1 s; idx \<le> 2 ^ v1; ctes_of s src = Some cte; cteCap cte = capability.UntypedCap d v0 v1 f; kernel_data_refs \<inter> {v0..v0 + 2 ^ v1 - 1} = {}; global_refs' s \<subseteq> kernel_data_refs; 2 ^ v1 \<le> gsMaxObjectSize s; \<exists>cap. modify_map (cteCaps_of s) src (\<lambda>a. capability.UntypedCap d v0 v1 idx) cref = Some cap \<and> cap \<noteq> capability.NullCap\<rbrakk> \<Longrightarrow> \<exists>cref' cap'. modify_map (cteCaps_of s) src (\<lambda>a. capability.UntypedCap d v0 v1 idx) cref' = Some cap' \<and> cref \<in> cte_refs' cap' (irq_node' s)
 2. \<And>s cte d v0 v1 f. \<lbrakk>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; is_aligned (word_of_nat idx) minUntypedSizeBits; descendants_of' src (ctes_of s) = {}; pspace_no_overlap' v0 v1 s; idx \<le> 2 ^ v1; ctes_of s src = Some cte; cteCap cte = capability.UntypedCap d v0 v1 f; kernel_data_refs \<inter> {v0..v0 + 2 ^ v1 - 1} = {}; global_refs' s \<subseteq> kernel_data_refs; 2 ^ v1 \<le> gsMaxObjectSize s\<rbrakk> \<Longrightarrow> untyped_ranges_zero_inv ((cteCaps_of s)(src \<mapsto> capability.UntypedCap d v0 v1 idx)) (case untypedZeroRange (capability.UntypedCap d v0 v1 idx) of None \<Rightarrow> case untypedZeroRange (capability.UntypedCap d v0 v1 f) of None \<Rightarrow> gsUntypedZeroRanges s | Some r \<Rightarrow> gsUntypedZeroRanges s - {r} | Some r \<Rightarrow> insert r (case untypedZeroRange (capability.UntypedCap d v0 v1 f) of None \<Rightarrow> gsUntypedZeroRanges s | Some r \<Rightarrow> gsUntypedZeroRanges s - {r})) proof (prove)
goal (3 subgoals):
 1. \<And>s cte d v0 v1 f. \<lbrakk>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; \<forall>cref. (\<exists>cap. (\<exists>z. ctes_of s cref = Some z \<and> cteCap z = cap) \<and> cap \<noteq> capability.NullCap) \<longrightarrow> (\<exists>cref' cap'. (\<exists>z. ctes_of s cref' = Some z \<and> cteCap z = cap') \<and> cref \<in> cte_refs' cap' (irq_node' 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_inv (map_option cteCap \<circ> ctes_of s) (gsUntypedZeroRanges s); cur_tcb' s; is_aligned (word_of_nat idx) minUntypedSizeBits; descendants_of' src (ctes_of s) = {}; pspace_no_overlap' v0 v1 s; idx \<le> 2 ^ v1; ctes_of s src = Some cte; cteCap cte = capability.UntypedCap d v0 v1 f; kernel_data_refs \<inter> {v0..v0 + 2 ^ v1 - 1} = {}; global_refs' s \<subseteq> kernel_data_refs; 2 ^ v1 \<le> gsMaxObjectSize s\<rbrakk> \<Longrightarrow> \<exists>cref'. cref' \<noteq> src \<and> (cref' \<noteq> src \<longrightarrow> (\<exists>cap'. (\<exists>z. ctes_of s cref' = Some z \<and> cteCap z = cap') \<and> src \<in> cte_refs' cap' (irq_node' s)))
 2. \<And>s cte d v0 v1 f cref z. \<lbrakk>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; \<forall>cref. (\<exists>cap. (\<exists>z. ctes_of s cref = Some z \<and> cteCap z = cap) \<and> cap \<noteq> capability.NullCap) \<longrightarrow> (\<exists>cref' cap'. (\<exists>z. ctes_of s cref' = Some z \<and> cteCap z = cap') \<and> cref \<in> cte_refs' cap' (irq_node' 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_inv (map_option cteCap \<circ> ctes_of s) (gsUntypedZeroRanges s); cur_tcb' s; is_aligned (word_of_nat idx) minUntypedSizeBits; descendants_of' src (ctes_of s) = {}; pspace_no_overlap' v0 v1 s; idx \<le> 2 ^ v1; ctes_of s src = Some cte; cteCap cte = capability.UntypedCap d v0 v1 f; kernel_data_refs \<inter> {v0..v0 + 2 ^ v1 - 1} = {}; global_refs' s \<subseteq> kernel_data_refs; 2 ^ v1 \<le> gsMaxObjectSize s; cref \<noteq> src; cteCap z \<noteq> capability.NullCap; ctes_of s cref = Some z\<rbrakk> \<Longrightarrow> \<exists>cref'. cref' \<noteq> src \<and> (cref' \<noteq> src \<longrightarrow> (\<exists>cap'. (\<exists>z. ctes_of s cref' = Some z \<and> cteCap z = cap') \<and> cref \<in> cte_refs' cap' (irq_node' s)))
 3. \<And>s cte d v0 v1 f. \<lbrakk>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; is_aligned (word_of_nat idx) minUntypedSizeBits; descendants_of' src (ctes_of s) = {}; pspace_no_overlap' v0 v1 s; idx \<le> 2 ^ v1; ctes_of s src = Some cte; cteCap cte = capability.UntypedCap d v0 v1 f; kernel_data_refs \<inter> {v0..v0 + 2 ^ v1 - 1} = {}; global_refs' s \<subseteq> kernel_data_refs; 2 ^ v1 \<le> gsMaxObjectSize s\<rbrakk> \<Longrightarrow> untyped_ranges_zero_inv ((cteCaps_of s)(src \<mapsto> capability.UntypedCap d v0 v1 idx)) (case untypedZeroRange (capability.UntypedCap d v0 v1 idx) of None \<Rightarrow> case untypedZeroRange (capability.UntypedCap d v0 v1 f) of None \<Rightarrow> gsUntypedZeroRanges s | Some r \<Rightarrow> gsUntypedZeroRanges s - {r} | Some r \<Rightarrow> insert r (case untypedZeroRange (capability.UntypedCap d v0 v1 f) of None \<Rightarrow> gsUntypedZeroRanges s | Some r \<Rightarrow> gsUntypedZeroRanges s - {r})) proof (prove)
goal (3 subgoals):
 1. \<And>s cte d v0 v1 f. \<lbrakk>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; 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_inv (map_option cteCap \<circ> ctes_of s) (gsUntypedZeroRanges s); cur_tcb' s; is_aligned (word_of_nat idx) minUntypedSizeBits; descendants_of' src (ctes_of s) = {}; pspace_no_overlap' v0 v1 s; idx \<le> 2 ^ v1; ctes_of s src = Some cte; cteCap cte = capability.UntypedCap d v0 v1 f; kernel_data_refs \<inter> {v0..v0 + 2 ^ v1 - 1} = {}; global_refs' s \<subseteq> kernel_data_refs; 2 ^ v1 \<le> gsMaxObjectSize s; (\<exists>cap. (\<exists>z. ctes_of s src = Some z \<and> cteCap z = cap) \<and> cap \<noteq> capability.NullCap) \<longrightarrow> (\<exists>cref' cap'. (\<exists>z. ctes_of s cref' = Some z \<and> cteCap z = cap') \<and> src \<in> cte_refs' cap' (irq_node' s))\<rbrakk> \<Longrightarrow> \<exists>cref'. cref' \<noteq> src \<and> (cref' \<noteq> src \<longrightarrow> (\<exists>cap'. (\<exists>z. ctes_of s cref' = Some z \<and> cteCap z = cap') \<and> src \<in> cte_refs' cap' (irq_node' s)))
 2. \<And>s cte d v0 v1 f cref z. \<lbrakk>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; \<forall>cref. (\<exists>cap. (\<exists>z. ctes_of s cref = Some z \<and> cteCap z = cap) \<and> cap \<noteq> capability.NullCap) \<longrightarrow> (\<exists>cref' cap'. (\<exists>z. ctes_of s cref' = Some z \<and> cteCap z = cap') \<and> cref \<in> cte_refs' cap' (irq_node' 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_inv (map_option cteCap \<circ> ctes_of s) (gsUntypedZeroRanges s); cur_tcb' s; is_aligned (word_of_nat idx) minUntypedSizeBits; descendants_of' src (ctes_of s) = {}; pspace_no_overlap' v0 v1 s; idx \<le> 2 ^ v1; ctes_of s src = Some cte; cteCap cte = capability.UntypedCap d v0 v1 f; kernel_data_refs \<inter> {v0..v0 + 2 ^ v1 - 1} = {}; global_refs' s \<subseteq> kernel_data_refs; 2 ^ v1 \<le> gsMaxObjectSize s; cref \<noteq> src; cteCap z \<noteq> capability.NullCap; ctes_of s cref = Some z\<rbrakk> \<Longrightarrow> \<exists>cref'. cref' \<noteq> src \<and> (cref' \<noteq> src \<longrightarrow> (\<exists>cap'. (\<exists>z. ctes_of s cref' = Some z \<and> cteCap z = cap') \<and> cref \<in> cte_refs' cap' (irq_node' s)))
 3. \<And>s cte d v0 v1 f. \<lbrakk>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; is_aligned (word_of_nat idx) minUntypedSizeBits; descendants_of' src (ctes_of s) = {}; pspace_no_overlap' v0 v1 s; idx \<le> 2 ^ v1; ctes_of s src = Some cte; cteCap cte = capability.UntypedCap d v0 v1 f; kernel_data_refs \<inter> {v0..v0 + 2 ^ v1 - 1} = {}; global_refs' s \<subseteq> kernel_data_refs; 2 ^ v1 \<le> gsMaxObjectSize s\<rbrakk> \<Longrightarrow> untyped_ranges_zero_inv ((cteCaps_of s)(src \<mapsto> capability.UntypedCap d v0 v1 idx)) (case untypedZeroRange (capability.UntypedCap d v0 v1 idx) of None \<Rightarrow> case untypedZeroRange (capability.UntypedCap d v0 v1 f) of None \<Rightarrow> gsUntypedZeroRanges s | Some r \<Rightarrow> gsUntypedZeroRanges s - {r} | Some r \<Rightarrow> insert r (case untypedZeroRange (capability.UntypedCap d v0 v1 f) of None \<Rightarrow> gsUntypedZeroRanges s | Some r \<Rightarrow> gsUntypedZeroRanges s - {r})) proof (prove)
goal (3 subgoals):
 1. \<And>s cte d v0 v1 f cref' z. \<lbrakk>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; 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_inv (map_option cteCap \<circ> ctes_of s) (gsUntypedZeroRanges s); cur_tcb' s; is_aligned (word_of_nat idx) minUntypedSizeBits; descendants_of' src (ctes_of s) = {}; pspace_no_overlap' v0 v1 s; idx \<le> 2 ^ v1; ctes_of s src = Some cte; cteCap cte = capability.UntypedCap d v0 v1 f; kernel_data_refs \<inter> {v0..v0 + 2 ^ v1 - 1} = {}; global_refs' s \<subseteq> kernel_data_refs; 2 ^ v1 \<le> gsMaxObjectSize s; src \<in> cte_refs' (cteCap z) (irq_node' s); ctes_of s cref' = Some z\<rbrakk> \<Longrightarrow> \<exists>cref'. cref' \<noteq> src \<and> (cref' \<noteq> src \<longrightarrow> (\<exists>cap'. (\<exists>z. ctes_of s cref' = Some z \<and> cteCap z = cap') \<and> src \<in> cte_refs' cap' (irq_node' s)))
 2. \<And>s cte d v0 v1 f cref z. \<lbrakk>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; \<forall>cref. (\<exists>cap. (\<exists>z. ctes_of s cref = Some z \<and> cteCap z = cap) \<and> cap \<noteq> capability.NullCap) \<longrightarrow> (\<exists>cref' cap'. (\<exists>z. ctes_of s cref' = Some z \<and> cteCap z = cap') \<and> cref \<in> cte_refs' cap' (irq_node' 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_inv (map_option cteCap \<circ> ctes_of s) (gsUntypedZeroRanges s); cur_tcb' s; is_aligned (word_of_nat idx) minUntypedSizeBits; descendants_of' src (ctes_of s) = {}; pspace_no_overlap' v0 v1 s; idx \<le> 2 ^ v1; ctes_of s src = Some cte; cteCap cte = capability.UntypedCap d v0 v1 f; kernel_data_refs \<inter> {v0..v0 + 2 ^ v1 - 1} = {}; global_refs' s \<subseteq> kernel_data_refs; 2 ^ v1 \<le> gsMaxObjectSize s; cref \<noteq> src; cteCap z \<noteq> capability.NullCap; ctes_of s cref = Some z\<rbrakk> \<Longrightarrow> \<exists>cref'. cref' \<noteq> src \<and> (cref' \<noteq> src \<longrightarrow> (\<exists>cap'. (\<exists>z. ctes_of s cref' = Some z \<and> cteCap z = cap') \<and> cref \<in> cte_refs' cap' (irq_node' s)))
 3. \<And>s cte d v0 v1 f. \<lbrakk>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; is_aligned (word_of_nat idx) minUntypedSizeBits; descendants_of' src (ctes_of s) = {}; pspace_no_overlap' v0 v1 s; idx \<le> 2 ^ v1; ctes_of s src = Some cte; cteCap cte = capability.UntypedCap d v0 v1 f; kernel_data_refs \<inter> {v0..v0 + 2 ^ v1 - 1} = {}; global_refs' s \<subseteq> kernel_data_refs; 2 ^ v1 \<le> gsMaxObjectSize s\<rbrakk> \<Longrightarrow> untyped_ranges_zero_inv ((cteCaps_of s)(src \<mapsto> capability.UntypedCap d v0 v1 idx)) (case untypedZeroRange (capability.UntypedCap d v0 v1 idx) of None \<Rightarrow> case untypedZeroRange (capability.UntypedCap d v0 v1 f) of None \<Rightarrow> gsUntypedZeroRanges s | Some r \<Rightarrow> gsUntypedZeroRanges s - {r} | Some r \<Rightarrow> insert r (case untypedZeroRange (capability.UntypedCap d v0 v1 f) of None \<Rightarrow> gsUntypedZeroRanges s | Some r \<Rightarrow> gsUntypedZeroRanges s - {r})) proof (prove)
goal (3 subgoals):
 1. \<And>s cte d v0 v1 f cref' z. \<lbrakk>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; 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_inv (map_option cteCap \<circ> ctes_of s) (gsUntypedZeroRanges s); cur_tcb' s; is_aligned (word_of_nat idx) minUntypedSizeBits; descendants_of' src (ctes_of s) = {}; pspace_no_overlap' v0 v1 s; idx \<le> 2 ^ v1; ctes_of s src = Some cte; cteCap cte = capability.UntypedCap d v0 v1 f; kernel_data_refs \<inter> {v0..v0 + 2 ^ v1 - 1} = {}; global_refs' s \<subseteq> kernel_data_refs; 2 ^ v1 \<le> gsMaxObjectSize s; src \<in> cte_refs' (cteCap z) (irq_node' s); ctes_of s cref' = Some z\<rbrakk> \<Longrightarrow> cref' \<noteq> src \<and> (cref' \<noteq> src \<longrightarrow> (\<exists>cap'. (\<exists>z. ctes_of s cref' = Some z \<and> cteCap z = cap') \<and> src \<in> cte_refs' cap' (irq_node' s)))
 2. \<And>s cte d v0 v1 f cref z. \<lbrakk>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; \<forall>cref. (\<exists>cap. (\<exists>z. ctes_of s cref = Some z \<and> cteCap z = cap) \<and> cap \<noteq> capability.NullCap) \<longrightarrow> (\<exists>cref' cap'. (\<exists>z. ctes_of s cref' = Some z \<and> cteCap z = cap') \<and> cref \<in> cte_refs' cap' (irq_node' 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_inv (map_option cteCap \<circ> ctes_of s) (gsUntypedZeroRanges s); cur_tcb' s; is_aligned (word_of_nat idx) minUntypedSizeBits; descendants_of' src (ctes_of s) = {}; pspace_no_overlap' v0 v1 s; idx \<le> 2 ^ v1; ctes_of s src = Some cte; cteCap cte = capability.UntypedCap d v0 v1 f; kernel_data_refs \<inter> {v0..v0 + 2 ^ v1 - 1} = {}; global_refs' s \<subseteq> kernel_data_refs; 2 ^ v1 \<le> gsMaxObjectSize s; cref \<noteq> src; cteCap z \<noteq> capability.NullCap; ctes_of s cref = Some z\<rbrakk> \<Longrightarrow> \<exists>cref'. cref' \<noteq> src \<and> (cref' \<noteq> src \<longrightarrow> (\<exists>cap'. (\<exists>z. ctes_of s cref' = Some z \<and> cteCap z = cap') \<and> cref \<in> cte_refs' cap' (irq_node' s)))
 3. \<And>s cte d v0 v1 f. \<lbrakk>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; is_aligned (word_of_nat idx) minUntypedSizeBits; descendants_of' src (ctes_of s) = {}; pspace_no_overlap' v0 v1 s; idx \<le> 2 ^ v1; ctes_of s src = Some cte; cteCap cte = capability.UntypedCap d v0 v1 f; kernel_data_refs \<inter> {v0..v0 + 2 ^ v1 - 1} = {}; global_refs' s \<subseteq> kernel_data_refs; 2 ^ v1 \<le> gsMaxObjectSize s\<rbrakk> \<Longrightarrow> untyped_ranges_zero_inv ((cteCaps_of s)(src \<mapsto> capability.UntypedCap d v0 v1 idx)) (case untypedZeroRange (capability.UntypedCap d v0 v1 idx) of None \<Rightarrow> case untypedZeroRange (capability.UntypedCap d v0 v1 f) of None \<Rightarrow> gsUntypedZeroRanges s | Some r \<Rightarrow> gsUntypedZeroRanges s - {r} | Some r \<Rightarrow> insert r (case untypedZeroRange (capability.UntypedCap d v0 v1 f) of None \<Rightarrow> gsUntypedZeroRanges s | Some r \<Rightarrow> gsUntypedZeroRanges s - {r})) proof (prove)
goal (2 subgoals):
 1. \<And>s cte d v0 v1 f cref z. \<lbrakk>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; \<forall>cref. (\<exists>cap. (\<exists>z. ctes_of s cref = Some z \<and> cteCap z = cap) \<and> cap \<noteq> capability.NullCap) \<longrightarrow> (\<exists>cref' cap'. (\<exists>z. ctes_of s cref' = Some z \<and> cteCap z = cap') \<and> cref \<in> cte_refs' cap' (irq_node' 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_inv (map_option cteCap \<circ> ctes_of s) (gsUntypedZeroRanges s); cur_tcb' s; is_aligned (word_of_nat idx) minUntypedSizeBits; descendants_of' src (ctes_of s) = {}; pspace_no_overlap' v0 v1 s; idx \<le> 2 ^ v1; ctes_of s src = Some cte; cteCap cte = capability.UntypedCap d v0 v1 f; kernel_data_refs \<inter> {v0..v0 + 2 ^ v1 - 1} = {}; global_refs' s \<subseteq> kernel_data_refs; 2 ^ v1 \<le> gsMaxObjectSize s; cref \<noteq> src; cteCap z \<noteq> capability.NullCap; ctes_of s cref = Some z\<rbrakk> \<Longrightarrow> \<exists>cref'. cref' \<noteq> src \<and> (cref' \<noteq> src \<longrightarrow> (\<exists>cap'. (\<exists>z. ctes_of s cref' = Some z \<and> cteCap z = cap') \<and> cref \<in> cte_refs' cap' (irq_node' s)))
 2. \<And>s cte d v0 v1 f. \<lbrakk>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; is_aligned (word_of_nat idx) minUntypedSizeBits; descendants_of' src (ctes_of s) = {}; pspace_no_overlap' v0 v1 s; idx \<le> 2 ^ v1; ctes_of s src = Some cte; cteCap cte = capability.UntypedCap d v0 v1 f; kernel_data_refs \<inter> {v0..v0 + 2 ^ v1 - 1} = {}; global_refs' s \<subseteq> kernel_data_refs; 2 ^ v1 \<le> gsMaxObjectSize s\<rbrakk> \<Longrightarrow> untyped_ranges_zero_inv ((cteCaps_of s)(src \<mapsto> capability.UntypedCap d v0 v1 idx)) (case untypedZeroRange (capability.UntypedCap d v0 v1 idx) of None \<Rightarrow> case untypedZeroRange (capability.UntypedCap d v0 v1 f) of None \<Rightarrow> gsUntypedZeroRanges s | Some r \<Rightarrow> gsUntypedZeroRanges s - {r} | Some r \<Rightarrow> insert r (case untypedZeroRange (capability.UntypedCap d v0 v1 f) of None \<Rightarrow> gsUntypedZeroRanges s | Some r \<Rightarrow> gsUntypedZeroRanges s - {r})) proof (prove)
goal (2 subgoals):
 1. \<And>s cte d v0 v1 f cref z. \<lbrakk>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; 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_inv (map_option cteCap \<circ> ctes_of s) (gsUntypedZeroRanges s); cur_tcb' s; is_aligned (word_of_nat idx) minUntypedSizeBits; descendants_of' src (ctes_of s) = {}; pspace_no_overlap' v0 v1 s; idx \<le> 2 ^ v1; ctes_of s src = Some cte; cteCap cte = capability.UntypedCap d v0 v1 f; kernel_data_refs \<inter> {v0..v0 + 2 ^ v1 - 1} = {}; global_refs' s \<subseteq> kernel_data_refs; 2 ^ v1 \<le> gsMaxObjectSize s; cref \<noteq> src; cteCap z \<noteq> capability.NullCap; ctes_of s cref = Some z; (\<exists>cap. (\<exists>z. ctes_of s cref = Some z \<and> cteCap z = cap) \<and> cap \<noteq> capability.NullCap) \<longrightarrow> (\<exists>cref' cap'. (\<exists>z. ctes_of s cref' = Some z \<and> cteCap z = cap') \<and> cref \<in> cte_refs' cap' (irq_node' s))\<rbrakk> \<Longrightarrow> \<exists>cref'. cref' \<noteq> src \<and> (cref' \<noteq> src \<longrightarrow> (\<exists>cap'. (\<exists>z. ctes_of s cref' = Some z \<and> cteCap z = cap') \<and> cref \<in> cte_refs' cap' (irq_node' s)))
 2. \<And>s cte d v0 v1 f. \<lbrakk>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; is_aligned (word_of_nat idx) minUntypedSizeBits; descendants_of' src (ctes_of s) = {}; pspace_no_overlap' v0 v1 s; idx \<le> 2 ^ v1; ctes_of s src = Some cte; cteCap cte = capability.UntypedCap d v0 v1 f; kernel_data_refs \<inter> {v0..v0 + 2 ^ v1 - 1} = {}; global_refs' s \<subseteq> kernel_data_refs; 2 ^ v1 \<le> gsMaxObjectSize s\<rbrakk> \<Longrightarrow> untyped_ranges_zero_inv ((cteCaps_of s)(src \<mapsto> capability.UntypedCap d v0 v1 idx)) (case untypedZeroRange (capability.UntypedCap d v0 v1 idx) of None \<Rightarrow> case untypedZeroRange (capability.UntypedCap d v0 v1 f) of None \<Rightarrow> gsUntypedZeroRanges s | Some r \<Rightarrow> gsUntypedZeroRanges s - {r} | Some r \<Rightarrow> insert r (case untypedZeroRange (capability.UntypedCap d v0 v1 f) of None \<Rightarrow> gsUntypedZeroRanges s | Some r \<Rightarrow> gsUntypedZeroRanges s - {r})) proof (prove)
goal (2 subgoals):
 1. \<And>s cte d v0 v1 f cref z cref' za. \<lbrakk>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; 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_inv (map_option cteCap \<circ> ctes_of s) (gsUntypedZeroRanges s); cur_tcb' s; is_aligned (word_of_nat idx) minUntypedSizeBits; descendants_of' src (ctes_of s) = {}; pspace_no_overlap' v0 v1 s; idx \<le> 2 ^ v1; ctes_of s src = Some cte; cteCap cte = capability.UntypedCap d v0 v1 f; kernel_data_refs \<inter> {v0..v0 + 2 ^ v1 - 1} = {}; global_refs' s \<subseteq> kernel_data_refs; 2 ^ v1 \<le> gsMaxObjectSize s; cref \<noteq> src; cteCap z \<noteq> capability.NullCap; ctes_of s cref = Some z; cref \<in> cte_refs' (cteCap za) (irq_node' s); ctes_of s cref' = Some za\<rbrakk> \<Longrightarrow> \<exists>cref'. cref' \<noteq> src \<and> (cref' \<noteq> src \<longrightarrow> (\<exists>cap'. (\<exists>z. ctes_of s cref' = Some z \<and> cteCap z = cap') \<and> cref \<in> cte_refs' cap' (irq_node' s)))
 2. \<And>s cte d v0 v1 f. \<lbrakk>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; is_aligned (word_of_nat idx) minUntypedSizeBits; descendants_of' src (ctes_of s) = {}; pspace_no_overlap' v0 v1 s; idx \<le> 2 ^ v1; ctes_of s src = Some cte; cteCap cte = capability.UntypedCap d v0 v1 f; kernel_data_refs \<inter> {v0..v0 + 2 ^ v1 - 1} = {}; global_refs' s \<subseteq> kernel_data_refs; 2 ^ v1 \<le> gsMaxObjectSize s\<rbrakk> \<Longrightarrow> untyped_ranges_zero_inv ((cteCaps_of s)(src \<mapsto> capability.UntypedCap d v0 v1 idx)) (case untypedZeroRange (capability.UntypedCap d v0 v1 idx) of None \<Rightarrow> case untypedZeroRange (capability.UntypedCap d v0 v1 f) of None \<Rightarrow> gsUntypedZeroRanges s | Some r \<Rightarrow> gsUntypedZeroRanges s - {r} | Some r \<Rightarrow> insert r (case untypedZeroRange (capability.UntypedCap d v0 v1 f) of None \<Rightarrow> gsUntypedZeroRanges s | Some r \<Rightarrow> gsUntypedZeroRanges s - {r})) proof (prove)
goal (2 subgoals):
 1. \<And>s cte d v0 v1 f cref z cref' za. \<lbrakk>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; 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_inv (map_option cteCap \<circ> ctes_of s) (gsUntypedZeroRanges s); cur_tcb' s; is_aligned (word_of_nat idx) minUntypedSizeBits; descendants_of' src (ctes_of s) = {}; pspace_no_overlap' v0 v1 s; idx \<le> 2 ^ v1; ctes_of s src = Some cte; cteCap cte = capability.UntypedCap d v0 v1 f; kernel_data_refs \<inter> {v0..v0 + 2 ^ v1 - 1} = {}; global_refs' s \<subseteq> kernel_data_refs; 2 ^ v1 \<le> gsMaxObjectSize s; cref \<noteq> src; cteCap z \<noteq> capability.NullCap; ctes_of s cref = Some z; cref \<in> cte_refs' (cteCap za) (irq_node' s); ctes_of s cref' = Some za\<rbrakk> \<Longrightarrow> cref' \<noteq> src \<and> (cref' \<noteq> src \<longrightarrow> (\<exists>cap'. (\<exists>z. ctes_of s cref' = Some z \<and> cteCap z = cap') \<and> cref \<in> cte_refs' cap' (irq_node' s)))
 2. \<And>s cte d v0 v1 f. \<lbrakk>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; is_aligned (word_of_nat idx) minUntypedSizeBits; descendants_of' src (ctes_of s) = {}; pspace_no_overlap' v0 v1 s; idx \<le> 2 ^ v1; ctes_of s src = Some cte; cteCap cte = capability.UntypedCap d v0 v1 f; kernel_data_refs \<inter> {v0..v0 + 2 ^ v1 - 1} = {}; global_refs' s \<subseteq> kernel_data_refs; 2 ^ v1 \<le> gsMaxObjectSize s\<rbrakk> \<Longrightarrow> untyped_ranges_zero_inv ((cteCaps_of s)(src \<mapsto> capability.UntypedCap d v0 v1 idx)) (case untypedZeroRange (capability.UntypedCap d v0 v1 idx) of None \<Rightarrow> case untypedZeroRange (capability.UntypedCap d v0 v1 f) of None \<Rightarrow> gsUntypedZeroRanges s | Some r \<Rightarrow> gsUntypedZeroRanges s - {r} | Some r \<Rightarrow> insert r (case untypedZeroRange (capability.UntypedCap d v0 v1 f) of None \<Rightarrow> gsUntypedZeroRanges s | Some r \<Rightarrow> gsUntypedZeroRanges s - {r})) proof (prove)
goal (1 subgoal):
 1. \<And>s cte d v0 v1 f. \<lbrakk>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; is_aligned (word_of_nat idx) minUntypedSizeBits; descendants_of' src (ctes_of s) = {}; pspace_no_overlap' v0 v1 s; idx \<le> 2 ^ v1; ctes_of s src = Some cte; cteCap cte = capability.UntypedCap d v0 v1 f; kernel_data_refs \<inter> {v0..v0 + 2 ^ v1 - 1} = {}; global_refs' s \<subseteq> kernel_data_refs; 2 ^ v1 \<le> gsMaxObjectSize s\<rbrakk> \<Longrightarrow> untyped_ranges_zero_inv ((cteCaps_of s)(src \<mapsto> capability.UntypedCap d v0 v1 idx)) (case untypedZeroRange (capability.UntypedCap d v0 v1 idx) of None \<Rightarrow> case untypedZeroRange (capability.UntypedCap d v0 v1 f) of None \<Rightarrow> gsUntypedZeroRanges s | Some r \<Rightarrow> gsUntypedZeroRanges s - {r} | Some r \<Rightarrow> insert r (case untypedZeroRange (capability.UntypedCap d v0 v1 f) of None \<Rightarrow> gsUntypedZeroRanges s | Some r \<Rightarrow> gsUntypedZeroRanges s - {r})) proof (prove)
goal (1 subgoal):
 1. \<And>s cte d v0 v1 f. \<lbrakk>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; is_aligned (word_of_nat idx) minUntypedSizeBits; descendants_of' src (ctes_of s) = {}; pspace_no_overlap' v0 v1 s; idx \<le> 2 ^ v1; ctes_of s src = Some cte; cteCap cte = capability.UntypedCap d v0 v1 f; kernel_data_refs \<inter> {v0..v0 + 2 ^ v1 - 1} = {}; global_refs' s \<subseteq> kernel_data_refs; 2 ^ v1 \<le> gsMaxObjectSize s; valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb' s\<rbrakk> \<Longrightarrow> untyped_ranges_zero_inv ((cteCaps_of s)(src \<mapsto> capability.UntypedCap d v0 v1 idx)) (case untypedZeroRange (capability.UntypedCap d v0 v1 idx) of None \<Rightarrow> case untypedZeroRange (capability.UntypedCap d v0 v1 f) of None \<Rightarrow> gsUntypedZeroRanges s | Some r \<Rightarrow> gsUntypedZeroRanges s - {r} | Some r \<Rightarrow> insert r (case untypedZeroRange (capability.UntypedCap d v0 v1 f) of None \<Rightarrow> gsUntypedZeroRanges s | Some r \<Rightarrow> gsUntypedZeroRanges s - {r})) proof (prove)
goal (1 subgoal):
 1. \<And>s cte d v0 v1 f. \<lbrakk>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)); cur_tcb' s; is_aligned (word_of_nat idx) minUntypedSizeBits; descendants_of' src (ctes_of s) = {}; pspace_no_overlap' v0 v1 s; idx \<le> 2 ^ v1; ctes_of s src = Some cte; cteCap cte = capability.UntypedCap d v0 v1 f; kernel_data_refs \<inter> {v0..v0 + 2 ^ v1 - 1} = {}; global_refs' s \<subseteq> kernel_data_refs; 2 ^ v1 \<le> gsMaxObjectSize s; valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb' s; set_option ((untypedZeroRange \<circ>\<^sub>m cteCaps_of s) src) \<subseteq> gsUntypedZeroRanges s\<rbrakk> \<Longrightarrow> (case untypedZeroRange (capability.UntypedCap d v0 v1 idx) of None \<Rightarrow> case untypedZeroRange (capability.UntypedCap d v0 v1 f) of None \<Rightarrow> gsUntypedZeroRanges s | Some r \<Rightarrow> gsUntypedZeroRanges s - {r} | Some r \<Rightarrow> insert r (case untypedZeroRange (capability.UntypedCap d v0 v1 f) of None \<Rightarrow> gsUntypedZeroRanges s | Some r \<Rightarrow> gsUntypedZeroRanges s - {r})) = gsUntypedZeroRanges s - set_option ((untypedZeroRange \<circ>\<^sub>m cteCaps_of s) src) \<union> set_option (untypedZeroRange (capability.UntypedCap d v0 v1 idx)) proof (prove)
goal:
No subgoals!