theory Untyped_R

lemma cte_wp_at_pspace_no_overlapI':
  "\<lbrakk>invs' s; cte_wp_at' (\<lambda>c. cteCap c = capability.UntypedCap
                                          d (ptr && ~~ mask sz) sz idx) cref s;
    idx \<le> unat (ptr && mask sz); sz < word_bits\<rbrakk>
   \<Longrightarrow> pspace_no_overlap' ptr sz s" apply (clarsimp simp:cte_wp_at_ctes_of) apply (case_tac cte,clarsimp) apply (frule ctes_of_valid_cap') apply (simp add:invs_valid_objs') apply (clarsimp simp:valid_cap'_def invs'_def valid_state'_def valid_pspace'_def
    valid_untyped'_def simp del:usableUntypedRange.simps) apply (unfold pspace_no_overlap'_def) apply (intro allI impI) apply (unfold ko_wp_at'_def) apply (clarsimp simp del: atLeastAtMost_iff
          atLeastatMost_subset_iff atLeastLessThan_iff
          Int_atLeastAtMost atLeastatMost_empty_iff  usableUntypedRange.simps) apply (drule spec)+ apply (frule(1) pspace_distinctD') apply (frule(1) pspace_alignedD') apply (erule(1) impE)+ apply (clarsimp simp: obj_range'_def simp del: atLeastAtMost_iff
          atLeastatMost_subset_iff atLeastLessThan_iff
          Int_atLeastAtMost atLeastatMost_empty_iff  usableUntypedRange.simps) apply (erule disjoint_subset2[rotated]) apply (frule(1) le_mask_le_2p) apply (clarsimp simp:p_assoc_help) apply (rule le_plus'[OF word_and_le2]) apply simp apply (erule word_of_nat_le) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>invs' s; cte_wp_at' (\<lambda>c. cteCap c = capability.UntypedCap d (ptr && ~~ mask sz) sz idx) cref s; idx \<le> unat (ptr && mask sz); sz < word_bits\<rbrakk> \<Longrightarrow> pspace_no_overlap' ptr sz s proof (prove)
goal (1 subgoal):
 1. \<And>cte. \<lbrakk>invs' s; idx \<le> unat (ptr && mask sz); sz < word_bits; ctes_of s cref = Some cte; cteCap cte = capability.UntypedCap d (ptr && ~~ mask sz) sz idx\<rbrakk> \<Longrightarrow> pspace_no_overlap' ptr sz s proof (prove)
goal (1 subgoal):
 1. \<And>x2. \<lbrakk>invs' s; idx \<le> unat (ptr && mask sz); sz < word_bits; ctes_of s cref = Some (CTE (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) x2)\<rbrakk> \<Longrightarrow> pspace_no_overlap' ptr sz s proof (prove)
goal (2 subgoals):
 1. \<And>x2. \<lbrakk>invs' s; idx \<le> unat (ptr && mask sz); sz < word_bits; ctes_of s cref = Some (CTE (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) x2)\<rbrakk> \<Longrightarrow> valid_objs' s
 2. \<And>x2. \<lbrakk>invs' s; idx \<le> unat (ptr && mask sz); sz < word_bits; ctes_of s cref = Some (CTE (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) x2); valid_cap' (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) s\<rbrakk> \<Longrightarrow> pspace_no_overlap' ptr sz s proof (prove)
goal (1 subgoal):
 1. \<And>x2. \<lbrakk>invs' s; idx \<le> unat (ptr && mask sz); sz < word_bits; ctes_of s cref = Some (CTE (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) x2); valid_cap' (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) s\<rbrakk> \<Longrightarrow> pspace_no_overlap' ptr sz s proof (prove)
goal (1 subgoal):
 1. \<And>x2. \<lbrakk>idx \<le> unat (ptr && mask sz); sz < word_bits; ctes_of s cref = Some (CTE (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) x2); valid_objs' s; capAligned (capability.UntypedCap d (ptr && ~~ mask sz) sz idx); pspace_aligned' s; \<forall>ptr'. \<not> ko_wp_at' (\<lambda>ko. {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subset> obj_range' ptr' ko \<or> obj_range' ptr' ko \<inter> usableUntypedRange (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) \<noteq> {}) ptr' s; pspace_distinct' s; ptr && ~~ mask sz \<noteq> 0; no_0_obj' s; minUntypedSizeBits \<le> sz; valid_mdb' s; sz \<le> maxUntypedSizeBits; sch_act_wf (ksSchedulerAction s) s; idx \<le> 2 ^ sz; is_aligned (word_of_nat idx) minUntypedSizeBits; 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\<rbrakk> \<Longrightarrow> pspace_no_overlap' ptr sz s proof (prove)
goal (1 subgoal):
 1. \<And>x2. \<lbrakk>idx \<le> unat (ptr && mask sz); sz < word_bits; ctes_of s cref = Some (CTE (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) x2); valid_objs' s; capAligned (capability.UntypedCap d (ptr && ~~ mask sz) sz idx); pspace_aligned' s; \<forall>ptr'. \<not> ko_wp_at' (\<lambda>ko. {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subset> obj_range' ptr' ko \<or> obj_range' ptr' ko \<inter> usableUntypedRange (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) \<noteq> {}) ptr' s; pspace_distinct' s; ptr && ~~ mask sz \<noteq> 0; no_0_obj' s; minUntypedSizeBits \<le> sz; valid_mdb' s; sz \<le> maxUntypedSizeBits; sch_act_wf (ksSchedulerAction s) s; idx \<le> 2 ^ sz; is_aligned (word_of_nat idx) minUntypedSizeBits; 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\<rbrakk> \<Longrightarrow> \<forall>x ko. ksPSpace s x = Some ko \<longrightarrow> {x..x + 2 ^ objBitsKO ko - 1} \<inter> up_aligned_area ptr sz = {} proof (prove)
goal (1 subgoal):
 1. \<And>x2 x ko. \<lbrakk>idx \<le> unat (ptr && mask sz); sz < word_bits; ctes_of s cref = Some (CTE (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) x2); valid_objs' s; capAligned (capability.UntypedCap d (ptr && ~~ mask sz) sz idx); pspace_aligned' s; \<forall>ptr'. \<not> ko_wp_at' (\<lambda>ko. {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subset> obj_range' ptr' ko \<or> obj_range' ptr' ko \<inter> usableUntypedRange (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) \<noteq> {}) ptr' s; pspace_distinct' s; ptr && ~~ mask sz \<noteq> 0; no_0_obj' s; minUntypedSizeBits \<le> sz; valid_mdb' s; sz \<le> maxUntypedSizeBits; sch_act_wf (ksSchedulerAction s) s; idx \<le> 2 ^ sz; is_aligned (word_of_nat idx) minUntypedSizeBits; 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; ksPSpace s x = Some ko\<rbrakk> \<Longrightarrow> {x..x + 2 ^ objBitsKO ko - 1} \<inter> up_aligned_area ptr sz = {} proof (prove)
goal (1 subgoal):
 1. \<And>x2 x ko. \<lbrakk>idx \<le> unat (ptr && mask sz); sz < word_bits; ctes_of s cref = Some (CTE (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) x2); valid_objs' s; capAligned (capability.UntypedCap d (ptr && ~~ mask sz) sz idx); pspace_aligned' s; \<forall>ptr'. \<nexists>ko. ksPSpace s ptr' = Some ko \<and> is_aligned ptr' (objBitsKO ko) \<and> ({ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subset> obj_range' ptr' ko \<or> obj_range' ptr' ko \<inter> usableUntypedRange (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) \<noteq> {}) \<and> ps_clear ptr' (objBitsKO ko) s; pspace_distinct' s; ptr && ~~ mask sz \<noteq> 0; no_0_obj' s; minUntypedSizeBits \<le> sz; valid_mdb' s; sz \<le> maxUntypedSizeBits; sch_act_wf (ksSchedulerAction s) s; idx \<le> 2 ^ sz; is_aligned (word_of_nat idx) minUntypedSizeBits; 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; ksPSpace s x = Some ko\<rbrakk> \<Longrightarrow> {x..x + 2 ^ objBitsKO ko - 1} \<inter> up_aligned_area ptr sz = {} proof (prove)
goal (1 subgoal):
 1. \<And>x2 x ko. \<lbrakk>idx \<le> unat (ptr && mask sz); sz < word_bits; ctes_of s cref = Some (CTE (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) x2); valid_objs' s; capAligned (capability.UntypedCap d (ptr && ~~ mask sz) sz idx); pspace_aligned' s; \<forall>ptr' ko. is_aligned ptr' (objBitsKO ko) \<longrightarrow> ksPSpace s ptr' = Some ko \<longrightarrow> \<not> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subset> obj_range' ptr' ko \<and> obj_range' ptr' ko \<inter> usableUntypedRange (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) = {} \<or> \<not> ps_clear ptr' (objBitsKO ko) s; pspace_distinct' s; ptr && ~~ mask sz \<noteq> 0; no_0_obj' s; minUntypedSizeBits \<le> sz; valid_mdb' s; sz \<le> maxUntypedSizeBits; sch_act_wf (ksSchedulerAction s) s; idx \<le> 2 ^ sz; is_aligned (word_of_nat idx) minUntypedSizeBits; 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; ksPSpace s x = Some ko\<rbrakk> \<Longrightarrow> {x..x + 2 ^ objBitsKO ko - 1} \<inter> up_aligned_area ptr sz = {} proof (prove)
goal (1 subgoal):
 1. \<And>x2 x ko. \<lbrakk>idx \<le> unat (ptr && mask sz); sz < word_bits; ctes_of s cref = Some (CTE (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) x2); valid_objs' s; capAligned (capability.UntypedCap d (ptr && ~~ mask sz) sz idx); pspace_aligned' s; pspace_distinct' s; ptr && ~~ mask sz \<noteq> 0; no_0_obj' s; minUntypedSizeBits \<le> sz; valid_mdb' s; sz \<le> maxUntypedSizeBits; sch_act_wf (ksSchedulerAction s) s; idx \<le> 2 ^ sz; is_aligned (word_of_nat idx) minUntypedSizeBits; 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; ksPSpace s x = Some ko; is_aligned (?ptr'46 x2 x ko) (objBitsKO (?ko48 x2 x ko)) \<longrightarrow> ksPSpace s (?ptr'46 x2 x ko) = Some (?ko48 x2 x ko) \<longrightarrow> \<not> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subset> obj_range' (?ptr'46 x2 x ko) (?ko48 x2 x ko) \<and> obj_range' (?ptr'46 x2 x ko) (?ko48 x2 x ko) \<inter> usableUntypedRange (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) = {} \<or> \<not> ps_clear (?ptr'46 x2 x ko) (objBitsKO (?ko48 x2 x ko)) s\<rbrakk> \<Longrightarrow> {x..x + 2 ^ objBitsKO ko - 1} \<inter> up_aligned_area ptr sz = {} proof (prove)
goal (1 subgoal):
 1. \<And>x2 x ko. \<lbrakk>idx \<le> unat (ptr && mask sz); sz < word_bits; ctes_of s cref = Some (CTE (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) x2); valid_objs' s; capAligned (capability.UntypedCap d (ptr && ~~ mask sz) sz idx); pspace_aligned' s; pspace_distinct' s; ptr && ~~ mask sz \<noteq> 0; no_0_obj' s; minUntypedSizeBits \<le> sz; valid_mdb' s; sz \<le> maxUntypedSizeBits; sch_act_wf (ksSchedulerAction s) s; idx \<le> 2 ^ sz; is_aligned (word_of_nat idx) minUntypedSizeBits; 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; ksPSpace s x = Some ko; is_aligned (?ptr'46 x2 x ko) (objBitsKO (?ko48 x2 x ko)) \<longrightarrow> ksPSpace s (?ptr'46 x2 x ko) = Some (?ko48 x2 x ko) \<longrightarrow> \<not> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subset> obj_range' (?ptr'46 x2 x ko) (?ko48 x2 x ko) \<and> obj_range' (?ptr'46 x2 x ko) (?ko48 x2 x ko) \<inter> usableUntypedRange (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) = {} \<or> \<not> ps_clear (?ptr'46 x2 x ko) (objBitsKO (?ko48 x2 x ko)) s; ps_clear x (objBitsKO ko) s\<rbrakk> \<Longrightarrow> {x..x + 2 ^ objBitsKO ko - 1} \<inter> up_aligned_area ptr sz = {} proof (prove)
goal (1 subgoal):
 1. \<And>x2 x ko. \<lbrakk>idx \<le> unat (ptr && mask sz); sz < word_bits; ctes_of s cref = Some (CTE (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) x2); valid_objs' s; capAligned (capability.UntypedCap d (ptr && ~~ mask sz) sz idx); pspace_aligned' s; pspace_distinct' s; ptr && ~~ mask sz \<noteq> 0; no_0_obj' s; minUntypedSizeBits \<le> sz; valid_mdb' s; sz \<le> maxUntypedSizeBits; sch_act_wf (ksSchedulerAction s) s; idx \<le> 2 ^ sz; is_aligned (word_of_nat idx) minUntypedSizeBits; 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; ksPSpace s x = Some ko; is_aligned (?ptr'46 x2 x ko) (objBitsKO (?ko48 x2 x ko)) \<longrightarrow> ksPSpace s (?ptr'46 x2 x ko) = Some (?ko48 x2 x ko) \<longrightarrow> \<not> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subset> obj_range' (?ptr'46 x2 x ko) (?ko48 x2 x ko) \<and> obj_range' (?ptr'46 x2 x ko) (?ko48 x2 x ko) \<inter> usableUntypedRange (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) = {} \<or> \<not> ps_clear (?ptr'46 x2 x ko) (objBitsKO (?ko48 x2 x ko)) s; ps_clear x (objBitsKO ko) s; is_aligned x (objBitsKO ko)\<rbrakk> \<Longrightarrow> {x..x + 2 ^ objBitsKO ko - 1} \<inter> up_aligned_area ptr sz = {} proof (prove)
goal (1 subgoal):
 1. \<And>x2 x ko. \<lbrakk>idx \<le> unat (ptr && mask sz); sz < word_bits; ctes_of s cref = Some (CTE (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) x2); valid_objs' s; capAligned (capability.UntypedCap d (ptr && ~~ mask sz) sz idx); pspace_aligned' s; pspace_distinct' s; ptr && ~~ mask sz \<noteq> 0; no_0_obj' s; minUntypedSizeBits \<le> sz; valid_mdb' s; sz \<le> maxUntypedSizeBits; sch_act_wf (ksSchedulerAction s) s; idx \<le> 2 ^ sz; is_aligned (word_of_nat idx) minUntypedSizeBits; 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; ksPSpace s x = Some ko; ps_clear x (objBitsKO ko) s; is_aligned x (objBitsKO ko); \<not> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subset> obj_range' x ko \<and> obj_range' x ko \<inter> usableUntypedRange (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) = {} \<or> \<not> ps_clear x (objBitsKO ko) s\<rbrakk> \<Longrightarrow> {x..x + 2 ^ objBitsKO ko - 1} \<inter> up_aligned_area ptr sz = {} proof (prove)
goal (1 subgoal):
 1. \<And>x2 x ko. \<lbrakk>idx \<le> unat (ptr && mask sz); sz < word_bits; ctes_of s cref = Some (CTE (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) x2); valid_objs' s; capAligned (capability.UntypedCap d (ptr && ~~ mask sz) sz idx); pspace_aligned' s; pspace_distinct' s; ptr && ~~ mask sz \<noteq> 0; no_0_obj' s; minUntypedSizeBits \<le> sz; valid_mdb' s; sz \<le> maxUntypedSizeBits; sch_act_wf (ksSchedulerAction s) s; idx \<le> 2 ^ sz; is_aligned (word_of_nat idx) minUntypedSizeBits; 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; ksPSpace s x = Some ko; ps_clear x (objBitsKO ko) s; is_aligned x (objBitsKO ko); \<not> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subset> {x..x + 2 ^ objBitsKO ko - 1}; {x..x + 2 ^ objBitsKO ko - 1} \<inter> usableUntypedRange (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) = {}\<rbrakk> \<Longrightarrow> {x..x + 2 ^ objBitsKO ko - 1} \<inter> up_aligned_area ptr sz = {} proof (prove)
goal (1 subgoal):
 1. \<And>x2 x ko. \<lbrakk>idx \<le> unat (ptr && mask sz); sz < word_bits; ctes_of s cref = Some (CTE (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) x2); valid_objs' s; capAligned (capability.UntypedCap d (ptr && ~~ mask sz) sz idx); pspace_aligned' s; pspace_distinct' s; ptr && ~~ mask sz \<noteq> 0; no_0_obj' s; minUntypedSizeBits \<le> sz; valid_mdb' s; sz \<le> maxUntypedSizeBits; sch_act_wf (ksSchedulerAction s) s; idx \<le> 2 ^ sz; is_aligned (word_of_nat idx) minUntypedSizeBits; 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; ksPSpace s x = Some ko; ps_clear x (objBitsKO ko) s; is_aligned x (objBitsKO ko); \<not> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subset> {x..x + 2 ^ objBitsKO ko - 1}\<rbrakk> \<Longrightarrow> up_aligned_area ptr sz \<subseteq> usableUntypedRange (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) proof (prove)
goal (1 subgoal):
 1. \<And>x2 x ko. \<lbrakk>idx \<le> unat (ptr && mask sz); sz < word_bits; ctes_of s cref = Some (CTE (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) x2); valid_objs' s; capAligned (capability.UntypedCap d (ptr && ~~ mask sz) sz idx); pspace_aligned' s; pspace_distinct' s; ptr && ~~ mask sz \<noteq> 0; no_0_obj' s; minUntypedSizeBits \<le> sz; valid_mdb' s; sz \<le> maxUntypedSizeBits; sch_act_wf (ksSchedulerAction s) s; idx \<le> 2 ^ sz; is_aligned (word_of_nat idx) minUntypedSizeBits; 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; ksPSpace s x = Some ko; ps_clear x (objBitsKO ko) s; is_aligned x (objBitsKO ko); \<not> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subset> {x..x + 2 ^ objBitsKO ko - 1}; idx < 2 ^ sz\<rbrakk> \<Longrightarrow> up_aligned_area ptr sz \<subseteq> usableUntypedRange (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) proof (prove)
goal (1 subgoal):
 1. \<And>x2 x ko. \<lbrakk>idx \<le> unat (ptr && mask sz); sz < word_bits; ctes_of s cref = Some (CTE (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) x2); valid_objs' s; capAligned (capability.UntypedCap d (ptr && ~~ mask sz) sz idx); pspace_aligned' s; pspace_distinct' s; ptr && ~~ mask sz \<noteq> 0; no_0_obj' s; minUntypedSizeBits \<le> sz; valid_mdb' s; sz \<le> maxUntypedSizeBits; sch_act_wf (ksSchedulerAction s) s; is_aligned (word_of_nat idx) minUntypedSizeBits; 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; ksPSpace s x = Some ko; ps_clear x (objBitsKO ko) s; is_aligned x (objBitsKO ko); \<not> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + (2 ^ sz - 1)} \<subset> {x..x + (2 ^ objBitsKO ko - 1)}; idx < 2 ^ sz; ptr \<le> (ptr && ~~ mask sz) + (2 ^ sz - 1)\<rbrakk> \<Longrightarrow> (ptr && ~~ mask sz) + word_of_nat idx \<le> ptr proof (prove)
goal (1 subgoal):
 1. \<And>x2 x ko. \<lbrakk>idx \<le> unat (ptr && mask sz); sz < word_bits; ctes_of s cref = Some (CTE (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) x2); valid_objs' s; capAligned (capability.UntypedCap d (ptr && ~~ mask sz) sz idx); pspace_aligned' s; pspace_distinct' s; ptr && ~~ mask sz \<noteq> 0; no_0_obj' s; minUntypedSizeBits \<le> sz; valid_mdb' s; sz \<le> maxUntypedSizeBits; sch_act_wf (ksSchedulerAction s) s; is_aligned (word_of_nat idx) minUntypedSizeBits; 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; ksPSpace s x = Some ko; ps_clear x (objBitsKO ko) s; is_aligned x (objBitsKO ko); \<not> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + (2 ^ sz - 1)} \<subset> {x..x + (2 ^ objBitsKO ko - 1)}; idx < 2 ^ sz; ptr \<le> (ptr && ~~ mask sz) + (2 ^ sz - 1)\<rbrakk> \<Longrightarrow> word_of_nat idx \<le> ptr - (ptr && ~~ mask sz) proof (prove)
goal (1 subgoal):
 1. \<And>x2 x ko. \<lbrakk>idx \<le> unat (ptr && mask sz); sz < word_bits; ctes_of s cref = Some (CTE (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) x2); valid_objs' s; capAligned (capability.UntypedCap d (ptr && ~~ mask sz) sz idx); pspace_aligned' s; pspace_distinct' s; ptr && ~~ mask sz \<noteq> 0; no_0_obj' s; minUntypedSizeBits \<le> sz; valid_mdb' s; sz \<le> maxUntypedSizeBits; sch_act_wf (ksSchedulerAction s) s; is_aligned (word_of_nat idx) minUntypedSizeBits; 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; ksPSpace s x = Some ko; ps_clear x (objBitsKO ko) s; is_aligned x (objBitsKO ko); \<not> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + (2 ^ sz - 1)} \<subset> {x..x + (2 ^ objBitsKO ko - 1)}; idx < 2 ^ sz; ptr \<le> (ptr && ~~ mask sz) + (2 ^ sz - 1)\<rbrakk> \<Longrightarrow> word_of_nat idx \<le> ptr && mask sz proof (prove)
goal:
No subgoals!