theory Untyped_R

lemma insertNewCap_invs':
  "\<lbrace>invs' and ct_active'
          and valid_cap' cap
          and cte_wp_at' (\<lambda>cte. isUntypedCap (cteCap cte) \<and>
                              sameRegionAs (cteCap cte) cap) parent
          and K (\<not> isZombie cap) and (\<lambda>s. descendants_range' cap parent (ctes_of s))
          and caps_overlap_reserved' (untypedRange cap)
          and ex_cte_cap_to' slot
          and (\<lambda>s. ksIdleThread s \<notin> capRange cap)
          and (\<lambda>s. \<forall>irq. cap = IRQHandlerCap irq \<longrightarrow> irq_issued' irq s)\<rbrace>
     insertNewCap parent slot cap
   \<lbrace>\<lambda>rv. invs'\<rbrace>" apply (rule insertNewCap_nullcap) apply (simp add: invs'_def valid_state'_def) apply (rule hoare_pre) apply (wp insertNewCap_valid_pspace' sch_act_wf_lift
             valid_queues_lift cur_tcb_lift tcb_in_cur_domain'_lift
             insertNewCap_valid_global_refs'
             valid_arch_state_lift'
             valid_irq_node_lift insertNewCap_valid_irq_handlers) apply (clarsimp simp: cte_wp_at_ctes_of) apply (frule ctes_of_valid[rotated, where p=parent, OF valid_pspace_valid_objs']) apply (fastforce simp: cte_wp_at_ctes_of) apply (auto simp: isCap_simps sameRegionAs_def3 intro!: capRange_subset_capBits
              elim: valid_capAligned) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs' and ct_active' and valid_cap' cap and cte_wp_at' (\<lambda>cte. isUntypedCap (cteCap cte) \<and> global.sameRegionAs (cteCap cte) cap) parent and K (\<not> isZombie cap) and (\<lambda>s. descendants_range' cap parent (ctes_of s)) and caps_overlap_reserved' (untypedRange cap) and ex_cte_cap_wp_to' (\<lambda>_. True) slot and (\<lambda>s. ksIdleThread s \<notin> capRange cap) and (\<lambda>s. \<forall>irq. cap = capability.IRQHandlerCap irq \<longrightarrow> irq_issued' irq s)\<rbrace> insertNewCap parent slot cap \<lbrace>\<lambda>rv. invs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs' and ct_active' and valid_cap' cap and cte_wp_at' (\<lambda>cte. isUntypedCap (cteCap cte) \<and> global.sameRegionAs (cteCap cte) cap) parent and K (\<not> isZombie cap) and (\<lambda>s. descendants_range' cap parent (ctes_of s)) and caps_overlap_reserved' (untypedRange cap) and ex_cte_cap_wp_to' (\<lambda>_. True) slot and (\<lambda>s. ksIdleThread s \<notin> capRange cap) and (\<lambda>s. \<forall>irq. cap = capability.IRQHandlerCap irq \<longrightarrow> irq_issued' irq s) and cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) slot\<rbrace> insertNewCap parent slot cap \<lbrace>\<lambda>rv. 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' and ct_active' and valid_cap' cap and cte_wp_at' (\<lambda>cte. isUntypedCap (cteCap cte) \<and> global.sameRegionAs (cteCap cte) cap) parent and (\<lambda>y. \<not> isZombie cap) and (\<lambda>s. descendants_range' cap parent (ctes_of s)) and caps_overlap_reserved' (untypedRange cap) and ex_cte_cap_wp_to' (\<lambda>_. True) slot and (\<lambda>s. ksIdleThread s \<notin> capRange cap) and (\<lambda>s. \<forall>irq. cap = capability.IRQHandlerCap irq \<longrightarrow> irq_issued' irq s) and cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) slot\<rbrace> insertNewCap parent slot cap \<lbrace>\<lambda>rv. (\<lambda>s. valid_pspace' s \<and> sch_act_wf (ksSchedulerAction s) s \<and> Invariants_H.valid_queues s \<and> sym_refs (state_refs_of' s) \<and> if_live_then_nonz_cap' s \<and> if_unsafe_then_cap' s \<and> valid_idle' s \<and> valid_global_refs' s \<and> valid_arch_state' s \<and> valid_irq_node' (irq_node' s) s \<and> valid_irq_handlers' s \<and> valid_irq_states' s \<and> valid_machine_state' s \<and> irqs_masked' s \<and> valid_queues' s \<and> ct_not_inQ s \<and> ct_idle_or_in_cur_domain' s \<and> valid_pde_mappings' s \<and> pspace_domain_valid s \<and> ksCurDomain s \<le> maxDomain \<and> ksDomSchedule s \<noteq> [] \<and> (\<forall>x\<in>set (ksDomSchedule s). dschDomain x \<le> maxDomain \<and> 0 < dschLength x) \<and> ksDomSchedule s = ksDomSchedule (KernelInit_H.newKernelState undefined) \<and> ksDomScheduleIdx s < length (ksDomSchedule (KernelInit_H.newKernelState undefined)) \<and> untyped_ranges_zero' s) and cur_tcb'\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q2\<rbrace> insertNewCap parent slot cap \<lbrace>\<lambda>rv. (\<lambda>s. valid_pspace' s \<and> sch_act_wf (ksSchedulerAction s) s \<and> Invariants_H.valid_queues s \<and> sym_refs (state_refs_of' s) \<and> if_live_then_nonz_cap' s \<and> if_unsafe_then_cap' s \<and> valid_idle' s \<and> valid_global_refs' s \<and> valid_arch_state' s \<and> valid_irq_node' (irq_node' s) s \<and> valid_irq_handlers' s \<and> valid_irq_states' s \<and> valid_machine_state' s \<and> irqs_masked' s \<and> valid_queues' s \<and> ct_not_inQ s \<and> ct_idle_or_in_cur_domain' s \<and> valid_pde_mappings' s \<and> pspace_domain_valid s \<and> ksCurDomain s \<le> maxDomain \<and> ksDomSchedule s \<noteq> [] \<and> (\<forall>x\<in>set (ksDomSchedule s). dschDomain x \<le> maxDomain \<and> 0 < dschLength x) \<and> ksDomSchedule s = ksDomSchedule (KernelInit_H.newKernelState undefined) \<and> ksDomScheduleIdx s < length (ksDomSchedule (KernelInit_H.newKernelState undefined)) \<and> untyped_ranges_zero' s) and cur_tcb'\<rbrace>
 2. \<And>s. ((\<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' and ct_active' and valid_cap' cap and cte_wp_at' (\<lambda>cte. isUntypedCap (cteCap cte) \<and> global.sameRegionAs (cteCap cte) cap) parent and (\<lambda>y. \<not> isZombie cap) and (\<lambda>s. descendants_range' cap parent (ctes_of s)) and caps_overlap_reserved' (untypedRange cap) and ex_cte_cap_wp_to' (\<lambda>_. True) slot and (\<lambda>s. ksIdleThread s \<notin> capRange cap) and (\<lambda>s. \<forall>irq. cap = capability.IRQHandlerCap irq \<longrightarrow> irq_issued' irq s) and cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) slot) s \<Longrightarrow> ?Q2 s proof (prove)
goal (1 subgoal):
 1. \<And>s. ((\<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' and ct_active' and valid_cap' cap and cte_wp_at' (\<lambda>cte. isUntypedCap (cteCap cte) \<and> global.sameRegionAs (cteCap cte) cap) parent and (\<lambda>y. \<not> isZombie cap) and (\<lambda>s. descendants_range' cap parent (ctes_of s)) and caps_overlap_reserved' (untypedRange cap) and ex_cte_cap_wp_to' (\<lambda>_. True) slot and (\<lambda>s. ksIdleThread s \<notin> capRange cap) and (\<lambda>s. \<forall>irq. cap = capability.IRQHandlerCap irq \<longrightarrow> irq_issued' irq s) and cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) slot) s \<Longrightarrow> (valid_pspace' s \<and> valid_cap' cap s \<and> slot \<noteq> parent \<and> caps_overlap_reserved' (untypedRange cap) s \<and> cte_wp_at' (\<lambda>cte. isUntypedCap (cteCap cte) \<and> global.sameRegionAs (cteCap cte) cap) parent s \<and> \<not> isZombie cap \<and> descendants_range' cap parent (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' and ex_cte_cap_wp_to' (\<lambda>_. True) slot) s \<and> valid_idle' s \<and> (valid_global_refs' and cte_wp_at' (\<lambda>cte. capRange cap \<subseteq> capRange (cteCap cte) \<and> capBits cap \<le> capBits (cteCap cte)) parent) s \<and> valid_arch_state' s \<and> valid_irq_node' (irq_node' s) s \<and> (valid_irq_handlers' and (\<lambda>s. \<forall>irq. cap = capability.IRQHandlerCap irq \<longrightarrow> irq_issued' irq s)) 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' and ct_active') 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' and valid_objs' and valid_mdb') s \<and> cur_tcb' s proof (prove)
goal (1 subgoal):
 1. \<And>s cte ctea. \<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; ct_active' s; valid_cap' cap s; \<not> isZombie cap; ctes_of s parent = Some cte; descendants_range' cap parent (ctes_of s); isUntypedCap (cteCap cte); global.sameRegionAs (cteCap cte) cap; caps_overlap_reserved' (untypedRange cap) s; ex_cte_cap_wp_to' (\<lambda>_. True) slot s; ksIdleThread s \<notin> capRange cap; \<forall>irq. cap = capability.IRQHandlerCap irq \<longrightarrow> irq_issued' irq s; ctes_of s slot = Some ctea; cteCap ctea = capability.NullCap\<rbrakk> \<Longrightarrow> slot \<noteq> parent \<and> capRange cap \<subseteq> capRange (cteCap cte) \<and> capBits cap \<le> capBits (cteCap cte) \<and> valid_objs' s \<and> valid_mdb' s proof (prove)
goal (2 subgoals):
 1. \<And>s cte ctea. \<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; ct_active' s; valid_cap' cap s; \<not> isZombie cap; ctes_of s parent = Some cte; descendants_range' cap parent (ctes_of s); isUntypedCap (cteCap cte); global.sameRegionAs (cteCap cte) cap; caps_overlap_reserved' (untypedRange cap) s; ex_cte_cap_wp_to' (\<lambda>_. True) slot s; ksIdleThread s \<notin> capRange cap; \<forall>irq. cap = capability.IRQHandlerCap irq \<longrightarrow> irq_issued' irq s; ctes_of s slot = Some ctea; cteCap ctea = capability.NullCap\<rbrakk> \<Longrightarrow> cte_wp_at' ((=) (?cte155 s cte ctea)) parent s
 2. \<And>s cte ctea. \<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; ct_active' s; valid_cap' cap s; \<not> isZombie cap; ctes_of s parent = Some cte; descendants_range' cap parent (ctes_of s); isUntypedCap (cteCap cte); global.sameRegionAs (cteCap cte) cap; caps_overlap_reserved' (untypedRange cap) s; ex_cte_cap_wp_to' (\<lambda>_. True) slot s; ksIdleThread s \<notin> capRange cap; \<forall>irq. cap = capability.IRQHandlerCap irq \<longrightarrow> irq_issued' irq s; ctes_of s slot = Some ctea; cteCap ctea = capability.NullCap; valid_cap' (cteCap (?cte155 s cte ctea)) s\<rbrakk> \<Longrightarrow> slot \<noteq> parent \<and> capRange cap \<subseteq> capRange (cteCap cte) \<and> capBits cap \<le> capBits (cteCap cte) \<and> valid_objs' s \<and> valid_mdb' s proof (prove)
goal (1 subgoal):
 1. \<And>s cte ctea. \<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; ct_active' s; valid_cap' cap s; \<not> isZombie cap; ctes_of s parent = Some cte; descendants_range' cap parent (ctes_of s); isUntypedCap (cteCap cte); global.sameRegionAs (cteCap cte) cap; caps_overlap_reserved' (untypedRange cap) s; ex_cte_cap_wp_to' (\<lambda>_. True) slot s; ksIdleThread s \<notin> capRange cap; \<forall>irq. cap = capability.IRQHandlerCap irq \<longrightarrow> irq_issued' irq s; ctes_of s slot = Some ctea; cteCap ctea = capability.NullCap; valid_cap' (cteCap cte) s\<rbrakk> \<Longrightarrow> slot \<noteq> parent \<and> capRange cap \<subseteq> capRange (cteCap cte) \<and> capBits cap \<le> capBits (cteCap cte) \<and> valid_objs' s \<and> valid_mdb' s proof (prove)
goal:
No subgoals!