theory CNodeInv_R

lemma updateCap_noop_invs:
  "\<lbrace>invs' and cte_wp_at' (\<lambda>cte. cteCap cte = cap) slot\<rbrace>
     updateCap slot cap
   \<lbrace>\<lambda>rv. invs'\<rbrace>" apply (simp add: invs'_def valid_state'_def
                   valid_pspace'_def valid_mdb'_def) apply (rule hoare_pre) apply (wp updateCap_ctes_of_wp updateCap_iflive'
             updateCap_ifunsafe' updateCap_idle'
             valid_arch_state_lift' valid_irq_node_lift
             updateCap_noop_irq_handlers sch_act_wf_lift
             untyped_ranges_zero_lift) apply (clarsimp simp: cte_wp_at_ctes_of modify_map_apply) apply (strengthen untyped_ranges_zero_delta[where xs=Nil, mk_strg I E]) apply (case_tac cte) apply (clarsimp simp: fun_upd_idem cteCaps_of_def modify_map_apply
                        valid_mdb'_def) apply (frule(1) ctes_of_valid') apply (frule(1) valid_global_refsD_with_objSize) apply clarsimp apply (rule_tac P="(=) cte" for cte in if_unsafe_then_capD') apply (simp add: cte_wp_at_ctes_of) apply assumption apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs' and cte_wp_at' (\<lambda>cte. cteCap cte = cap) slot\<rbrace> updateCap slot cap \<lbrace>\<lambda>rv. invs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>(\<lambda>s. valid_objs' s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> no_0_obj' s \<and> valid_mdb_ctes (ctes_of 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' and cte_wp_at' (\<lambda>cte. cteCap cte = cap) slot\<rbrace> updateCap slot cap \<lbrace>\<lambda>rv. (\<lambda>s. valid_objs' s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> no_0_obj' s \<and> valid_mdb_ctes (ctes_of s) \<and> sch_act_wf (ksSchedulerAction s) s \<and> Invariants_H.valid_queues s \<and> sym_refs (state_refs_of' s) \<and> if_live_then_nonz_cap' s \<and> if_unsafe_then_cap' s \<and> valid_idle' s \<and> valid_global_refs' s \<and> valid_arch_state' s \<and> valid_irq_node' (irq_node' s) s \<and> valid_irq_handlers' s \<and> valid_irq_states' s \<and> valid_machine_state' s \<and> irqs_masked' s \<and> valid_queues' s \<and> ct_not_inQ s \<and> ct_idle_or_in_cur_domain' s \<and> valid_pde_mappings' s \<and> pspace_domain_valid s \<and> ksCurDomain s \<le> maxDomain \<and> ksDomSchedule s \<noteq> [] \<and> (\<forall>x\<in>set (ksDomSchedule s). dschDomain x \<le> maxDomain \<and> 0 < dschLength x) \<and> ksDomSchedule s = ksDomSchedule (KernelInit_H.newKernelState undefined) \<and> ksDomScheduleIdx s < length (ksDomSchedule (KernelInit_H.newKernelState undefined)) \<and> untyped_ranges_zero' s) and cur_tcb'\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> updateCap slot cap \<lbrace>\<lambda>rv. (\<lambda>s. valid_objs' s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> no_0_obj' s \<and> valid_mdb_ctes (ctes_of s) \<and> sch_act_wf (ksSchedulerAction s) s \<and> Invariants_H.valid_queues s \<and> sym_refs (state_refs_of' s) \<and> if_live_then_nonz_cap' s \<and> if_unsafe_then_cap' s \<and> valid_idle' s \<and> valid_global_refs' s \<and> valid_arch_state' s \<and> valid_irq_node' (irq_node' s) s \<and> valid_irq_handlers' s \<and> valid_irq_states' s \<and> valid_machine_state' s \<and> irqs_masked' s \<and> valid_queues' s \<and> ct_not_inQ s \<and> ct_idle_or_in_cur_domain' s \<and> valid_pde_mappings' s \<and> pspace_domain_valid s \<and> ksCurDomain s \<le> maxDomain \<and> ksDomSchedule s \<noteq> [] \<and> (\<forall>x\<in>set (ksDomSchedule s). dschDomain x \<le> maxDomain \<and> 0 < dschLength x) \<and> ksDomSchedule s = ksDomSchedule (KernelInit_H.newKernelState undefined) \<and> ksDomScheduleIdx s < length (ksDomSchedule (KernelInit_H.newKernelState undefined)) \<and> untyped_ranges_zero' s) and cur_tcb'\<rbrace>
 2. \<And>s. ((\<lambda>s. valid_objs' s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> no_0_obj' s \<and> valid_mdb_ctes (ctes_of 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' and cte_wp_at' (\<lambda>cte. cteCap cte = cap) slot) s \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. ((\<lambda>s. valid_objs' s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> no_0_obj' s \<and> valid_mdb_ctes (ctes_of 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' and cte_wp_at' (\<lambda>cte. cteCap cte = cap) slot) s \<Longrightarrow> (valid_objs' s \<and> valid_cap' cap s) \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> no_0_obj' s \<and> valid_mdb_ctes (modify_map (ctes_of s) slot (cteCap_update (\<lambda>_. cap))) \<and> sch_act_wf (ksSchedulerAction s) s \<and> Invariants_H.valid_queues s \<and> sym_refs (state_refs_of' s) \<and> (cte_wp_at' (\<lambda>cte'. \<forall>p'\<in>zobj_refs' (cteCap cte') - zobj_refs' cap. ko_wp_at' (Not \<circ> live') p' s) slot s \<and> if_live_then_nonz_cap' s) \<and> (if_unsafe_then_cap' s \<and> valid_objs' s \<and> cte_wp_at' (\<lambda>cte. \<forall>r\<in>cte_refs' (cteCap cte) (irq_node' s) - cte_refs' cap (irq_node' s). cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) r s \<and> (r = slot \<longrightarrow> cap = capability.NullCap)) slot s \<and> (cap \<noteq> capability.NullCap \<longrightarrow> ex_cte_cap_wp_to' (\<lambda>_. True) slot s)) \<and> valid_idle' s \<and> (valid_global_refs' and (\<lambda>s. kernel_data_refs \<inter> capRange cap = {}) and (\<lambda>s. 2 ^ capBits cap \<le> gsMaxObjectSize s)) s \<and> valid_arch_state' s \<and> valid_irq_node' (irq_node' s) s \<and> (valid_irq_handlers' and cte_wp_at' (\<lambda>cte. cteCap cte = cap) slot) 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_inv (modify_map (cteCaps_of s) slot (K cap)) (gsUntypedZeroRanges s) \<and> cur_tcb' s proof (prove)
goal (1 subgoal):
 1. \<And>s cte. \<lbrakk>valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb_ctes (ctes_of 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; ctes_of s slot = Some cte; cap = cteCap cte\<rbrakk> \<Longrightarrow> valid_cap' (cteCap cte) s \<and> valid_mdb_ctes ((ctes_of s)(slot \<mapsto> cteCap_update (\<lambda>_. cteCap cte) cte)) \<and> (cteCap cte \<noteq> capability.NullCap \<longrightarrow> ex_cte_cap_wp_to' (\<lambda>_. True) slot s) \<and> kernel_data_refs \<inter> capRange (cteCap cte) = {} \<and> 2 ^ capBits (cteCap cte) \<le> gsMaxObjectSize s \<and> untyped_ranges_zero_inv (modify_map (cteCaps_of s) slot (\<lambda>y. cteCap cte)) (gsUntypedZeroRanges s) proof (prove)
goal (1 subgoal):
 1. \<And>s cte. \<lbrakk>valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb_ctes (ctes_of 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; ctes_of s slot = Some cte; cap = cteCap cte\<rbrakk> \<Longrightarrow> valid_cap' (cteCap cte) s \<and> valid_mdb_ctes ((ctes_of s)(slot \<mapsto> cteCap_update (\<lambda>_. cteCap cte) cte)) \<and> (cteCap cte \<noteq> capability.NullCap \<longrightarrow> ex_cte_cap_wp_to' (\<lambda>_. True) slot s) \<and> kernel_data_refs \<inter> capRange (cteCap cte) = {} \<and> 2 ^ capBits (cteCap cte) \<le> gsMaxObjectSize s \<and> (\<forall>p. p \<notin> set [] \<longrightarrow> modify_map (cteCaps_of s) slot (\<lambda>y. cteCap cte) p = cteCaps_of s p) \<and> valid_mdb' s \<and> valid_objs' s \<and> (ran ((untypedZeroRange \<circ>\<^sub>m cteCaps_of s) |` set []) \<subseteq> gsUntypedZeroRanges s \<longrightarrow> gsUntypedZeroRanges s = gsUntypedZeroRanges s - ran ((untypedZeroRange \<circ>\<^sub>m cteCaps_of s) |` set []) \<union> ran ((untypedZeroRange \<circ>\<^sub>m modify_map (cteCaps_of s) slot (\<lambda>y. cteCap cte)) |` set [])) proof (prove)
goal (1 subgoal):
 1. \<And>s cte x1 x2. \<lbrakk>valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb_ctes (ctes_of 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; ctes_of s slot = Some cte; cap = cteCap cte; cte = CTE x1 x2\<rbrakk> \<Longrightarrow> valid_cap' (cteCap cte) s \<and> valid_mdb_ctes ((ctes_of s)(slot \<mapsto> cteCap_update (\<lambda>_. cteCap cte) cte)) \<and> (cteCap cte \<noteq> capability.NullCap \<longrightarrow> ex_cte_cap_wp_to' (\<lambda>_. True) slot s) \<and> kernel_data_refs \<inter> capRange (cteCap cte) = {} \<and> 2 ^ capBits (cteCap cte) \<le> gsMaxObjectSize s \<and> (\<forall>p. p \<notin> set [] \<longrightarrow> modify_map (cteCaps_of s) slot (\<lambda>y. cteCap cte) p = cteCaps_of s p) \<and> valid_mdb' s \<and> valid_objs' s \<and> (ran ((untypedZeroRange \<circ>\<^sub>m cteCaps_of s) |` set []) \<subseteq> gsUntypedZeroRanges s \<longrightarrow> gsUntypedZeroRanges s = gsUntypedZeroRanges s - ran ((untypedZeroRange \<circ>\<^sub>m cteCaps_of s) |` set []) \<union> ran ((untypedZeroRange \<circ>\<^sub>m modify_map (cteCaps_of s) slot (\<lambda>y. cteCap cte)) |` set [])) proof (prove)
goal (1 subgoal):
 1. \<And>s x2. \<lbrakk>valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb_ctes (ctes_of 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_inv (map_option cteCap \<circ> ctes_of s) (gsUntypedZeroRanges s); cur_tcb' s; ctes_of s slot = Some (CTE cap x2)\<rbrakk> \<Longrightarrow> valid_cap' cap s \<and> (cap \<noteq> capability.NullCap \<longrightarrow> ex_cte_cap_wp_to' (\<lambda>_. True) slot s) \<and> kernel_data_refs \<inter> capRange cap = {} \<and> 2 ^ capBits cap \<le> gsMaxObjectSize s proof (prove)
goal (1 subgoal):
 1. \<And>s x2. \<lbrakk>valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb_ctes (ctes_of 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_inv (map_option cteCap \<circ> ctes_of s) (gsUntypedZeroRanges s); cur_tcb' s; ctes_of s slot = Some (CTE cap x2); valid_cap' (cteCap (CTE cap x2)) s\<rbrakk> \<Longrightarrow> valid_cap' cap s \<and> (cap \<noteq> capability.NullCap \<longrightarrow> ex_cte_cap_wp_to' (\<lambda>_. True) slot s) \<and> kernel_data_refs \<inter> capRange cap = {} \<and> 2 ^ capBits cap \<le> gsMaxObjectSize s proof (prove)
goal (1 subgoal):
 1. \<And>s x2. \<lbrakk>valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb_ctes (ctes_of 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_inv (map_option cteCap \<circ> ctes_of s) (gsUntypedZeroRanges s); cur_tcb' s; ctes_of s slot = Some (CTE cap x2); valid_cap' (cteCap (CTE cap x2)) s; kernel_data_refs \<inter> capRange (cteCap (CTE cap x2)) = {} \<and> global_refs' s \<subseteq> kernel_data_refs \<and> 2 ^ capBits (cteCap (CTE cap x2)) \<le> gsMaxObjectSize s\<rbrakk> \<Longrightarrow> valid_cap' cap s \<and> (cap \<noteq> capability.NullCap \<longrightarrow> ex_cte_cap_wp_to' (\<lambda>_. True) slot s) \<and> kernel_data_refs \<inter> capRange cap = {} \<and> 2 ^ capBits cap \<le> gsMaxObjectSize s proof (prove)
goal (1 subgoal):
 1. \<And>s x2. \<lbrakk>valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb_ctes (ctes_of 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_inv (map_option cteCap \<circ> ctes_of s) (gsUntypedZeroRanges s); cur_tcb' s; ctes_of s slot = Some (CTE cap x2); valid_cap' cap s; kernel_data_refs \<inter> capRange cap = {}; global_refs' s \<subseteq> kernel_data_refs; 2 ^ capBits cap \<le> gsMaxObjectSize s; cap \<noteq> capability.NullCap\<rbrakk> \<Longrightarrow> ex_cte_cap_wp_to' (\<lambda>_. True) slot s proof (prove)
goal (3 subgoals):
 1. \<And>s x2. \<lbrakk>valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb_ctes (ctes_of 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_inv (map_option cteCap \<circ> ctes_of s) (gsUntypedZeroRanges s); cur_tcb' s; ctes_of s slot = Some (CTE cap x2); valid_cap' cap s; kernel_data_refs \<inter> capRange cap = {}; global_refs' s \<subseteq> kernel_data_refs; 2 ^ capBits cap \<le> gsMaxObjectSize s; cap \<noteq> capability.NullCap\<rbrakk> \<Longrightarrow> cte_wp_at' ((=) (?cte177 s x2)) slot s
 2. \<And>s x2. \<lbrakk>valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb_ctes (ctes_of 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_inv (map_option cteCap \<circ> ctes_of s) (gsUntypedZeroRanges s); cur_tcb' s; ctes_of s slot = Some (CTE cap x2); valid_cap' cap s; kernel_data_refs \<inter> capRange cap = {}; global_refs' s \<subseteq> kernel_data_refs; 2 ^ capBits cap \<le> gsMaxObjectSize s; cap \<noteq> capability.NullCap\<rbrakk> \<Longrightarrow> if_unsafe_then_cap' s
 3. \<And>s x2 cte. \<lbrakk>valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb_ctes (ctes_of 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_inv (map_option cteCap \<circ> ctes_of s) (gsUntypedZeroRanges s); cur_tcb' s; ctes_of s slot = Some (CTE cap x2); valid_cap' cap s; kernel_data_refs \<inter> capRange cap = {}; global_refs' s \<subseteq> kernel_data_refs; 2 ^ capBits cap \<le> gsMaxObjectSize s; cap \<noteq> capability.NullCap; ?cte177 s x2 = cte\<rbrakk> \<Longrightarrow> cteCap cte \<noteq> capability.NullCap proof (prove)
goal (2 subgoals):
 1. \<And>s x2. \<lbrakk>valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb_ctes (ctes_of 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_inv (map_option cteCap \<circ> ctes_of s) (gsUntypedZeroRanges s); cur_tcb' s; ctes_of s slot = Some (CTE cap x2); valid_cap' cap s; kernel_data_refs \<inter> capRange cap = {}; global_refs' s \<subseteq> kernel_data_refs; 2 ^ capBits cap \<le> gsMaxObjectSize s; cap \<noteq> capability.NullCap\<rbrakk> \<Longrightarrow> if_unsafe_then_cap' s
 2. \<And>s x2 cte. \<lbrakk>valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb_ctes (ctes_of 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_inv (map_option cteCap \<circ> ctes_of s) (gsUntypedZeroRanges s); cur_tcb' s; ctes_of s slot = Some (CTE cap x2); valid_cap' cap s; kernel_data_refs \<inter> capRange cap = {}; global_refs' s \<subseteq> kernel_data_refs; 2 ^ capBits cap \<le> gsMaxObjectSize s; cap \<noteq> capability.NullCap; CTE cap x2 = cte\<rbrakk> \<Longrightarrow> cteCap cte \<noteq> capability.NullCap proof (prove)
goal (1 subgoal):
 1. \<And>s x2 cte. \<lbrakk>valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb_ctes (ctes_of 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_inv (map_option cteCap \<circ> ctes_of s) (gsUntypedZeroRanges s); cur_tcb' s; ctes_of s slot = Some (CTE cap x2); valid_cap' cap s; kernel_data_refs \<inter> capRange cap = {}; global_refs' s \<subseteq> kernel_data_refs; 2 ^ capBits cap \<le> gsMaxObjectSize s; cap \<noteq> capability.NullCap; CTE cap x2 = cte\<rbrakk> \<Longrightarrow> cteCap cte \<noteq> capability.NullCap proof (prove)
goal:
No subgoals!