theory Detype_R

lemma (in detype_locale') deletionIsSafe:
  assumes sr: "(s, s') \<in> state_relation"
  and    cap: "cap = cap.UntypedCap d base magnitude idx"
  and      vs: "valid_pspace s"
  and      al: "is_aligned base magnitude"
  and      vu: "valid_untyped (cap.UntypedCap d base magnitude idx) s"
  shows       "deletionIsSafe base magnitude s'" proof - interpret Arch .  (* FIXME: arch_split *)
   note blah[simp del] =  atLeastatMost_subset_iff atLeastLessThan_iff
          Int_atLeastAtMost atLeastatMost_empty_iff split_paired_Ex
          atLeastAtMost_iff have "\<And>t m r. \<exists>ptr. cte_wp_at ((=) (cap.ReplyCap t m r)) ptr s
        \<Longrightarrow> t \<notin> {base .. base + 2 ^ magnitude - 1}" by (fastforce dest!: valid_cap2 simp: cap obj_reply_refs_def) hence "\<forall>ptr t m r. cte_wp_at ((=) (cap.ReplyCap t m r)) ptr s
         \<longrightarrow> t \<notin> {base .. base + 2 ^ magnitude - 1}" by (fastforce simp del: split_paired_All) hence "\<forall>t. t \<in> {base .. base + 2 ^ magnitude - 1} \<longrightarrow>
          (\<forall>ptr m r. \<not> cte_wp_at ((=) (cap.ReplyCap t m r)) ptr s)" by fastforce hence cte: "\<forall>t. t \<in> {base .. base + 2 ^ magnitude - 1} \<longrightarrow>
          (\<forall>ptr m r. \<not> cte_wp_at' (\<lambda>cte. cteCap cte = ReplyCap t m r) ptr s')" unfolding deletionIsSafe_def apply - apply (erule allEI) apply (rule impI, drule(1) mp) apply (thin_tac "t \<in> S" for S) apply (intro allI) apply (clarsimp simp: cte_wp_at_neg2 cte_wp_at_ctes_of
                simp del: split_paired_All) apply (frule pspace_relation_cte_wp_atI [rotated]) apply (rule invs_valid_objs [OF invs]) apply (rule state_relation_pspace_relation [OF sr]) apply (clarsimp simp: cte_wp_at_neg2 simp del: split_paired_All) apply (drule_tac x="(a,b)" in spec) apply (clarsimp simp: cte_wp_cte_at cte_wp_at_caps_of_state) apply (case_tac c, simp_all) apply fastforce done have arch: "\<And> ko p. \<lbrakk> ksPSpace s' p = Some (KOArch ko); p \<in> {base..base + 2 ^ magnitude - 1} \<rbrakk>
             \<Longrightarrow> 6 \<le> magnitude" using sr vs vu apply (clarsimp simp: state_relation_def) apply (erule(1) pspace_dom_relatedE) apply (frule obj_relation_cuts_eqv_base_in_detype_range[symmetric]) apply simp apply (clarsimp simp:valid_pspace_def)+ apply simp apply (clarsimp simp:valid_untyped_def) apply (drule spec)+ apply (erule(1) impE) apply (erule impE) apply (drule p_in_obj_range) apply (clarsimp)+ apply blast apply clarsimp apply (drule card_mono[rotated]) apply fastforce apply (clarsimp simp:valid_pspace_def obj_range_def p_assoc_help) apply (subst (asm) word_range_card) apply (rule is_aligned_no_overflow') apply (erule(1) pspace_alignedD) apply (subst (asm) word_range_card) apply (rule is_aligned_no_overflow'[OF al]) apply (rule ccontr) apply (simp add:not_le) apply (subgoal_tac "obj_bits koa < 32") prefer 2 apply (case_tac koa,simp_all add:objBits_simps word_bits_def) apply (drule(1) valid_cs_size_objsI) apply (clarsimp simp:valid_cs_size_def word_bits_def cte_level_bits_def) apply (rename_tac arch_kernel_obj) apply (case_tac arch_kernel_obj,simp_all add:pageBits_def word_bits_def) apply (simp add:pageBitsForSize_def split:vmpage_size.splits) apply (subgoal_tac "6 \<le> obj_bits koa") apply simp apply (case_tac koa, simp_all add: other_obj_relation_def
                                       objBits_simps cte_relation_def
                                split: if_splits) apply (rename_tac arch_kernel_obj,
           case_tac arch_kernel_obj;
           simp add: arch_kobj_size_def pageBits_def pageBitsForSize_def)+ done thus ?thesis using cte by (auto simp: deletionIsSafe_def) qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. deletionIsSafe base magnitude s' proof (state)
goal (1 subgoal):
 1. deletionIsSafe base magnitude s' proof (prove)
goal:
No subgoals! proof (state)
goal (1 subgoal):
 1. deletionIsSafe base magnitude s' proof (state)
goal (1 subgoal):
 1. deletionIsSafe base magnitude s' proof (state)
this:
({?a..?b} \<subseteq> {?c..?d}) = (\<not> ?a \<le> ?b \<or> ?c \<le> ?a \<and> ?b \<le> ?d)
(?i \<in> {?l..<?u}) = (?l \<le> ?i \<and> ?i < ?u)
{?a..?b} \<inter> {?c..?d} = {max ?a ?c..min ?b ?d}
({?a..?b} = {}) = (\<not> ?a \<le> ?b)
(\<exists>x. ?P x) = (\<exists>a b. ?P (a, b))
(?i \<in> {?l..?u}) = (?l \<le> ?i \<and> ?i \<le> ?u)

goal (1 subgoal):
 1. deletionIsSafe base magnitude s' proof (prove)
goal (1 subgoal):
 1. \<And>t m r. \<exists>ptr. cte_wp_at ((=) (cap.ReplyCap t m r)) ptr s \<Longrightarrow> t \<notin> {base..base + 2 ^ magnitude - 1} proof (state)
this:
\<exists>ptr. cte_wp_at ((=) (cap.ReplyCap ?t ?m ?r)) ptr s \<Longrightarrow> ?t \<notin> {base..base + 2 ^ magnitude - 1}

goal (1 subgoal):
 1. deletionIsSafe base magnitude s' proof (prove)
using this:
\<exists>ptr. cte_wp_at ((=) (cap.ReplyCap ?t ?m ?r)) ptr s \<Longrightarrow> ?t \<notin> {base..base + 2 ^ magnitude - 1}

goal (1 subgoal):
 1. \<forall>ptr t m r. cte_wp_at ((=) (cap.ReplyCap t m r)) ptr s \<longrightarrow> t \<notin> {base..base + 2 ^ magnitude - 1} proof (state)
this:
\<forall>ptr t m r. cte_wp_at ((=) (cap.ReplyCap t m r)) ptr s \<longrightarrow> t \<notin> {base..base + 2 ^ magnitude - 1}

goal (1 subgoal):
 1. deletionIsSafe base magnitude s' proof (prove)
using this:
\<forall>ptr t m r. cte_wp_at ((=) (cap.ReplyCap t m r)) ptr s \<longrightarrow> t \<notin> {base..base + 2 ^ magnitude - 1}

goal (1 subgoal):
 1. \<forall>t. t \<in> {base..base + 2 ^ magnitude - 1} \<longrightarrow> (\<forall>ptr m r. \<not> cte_wp_at ((=) (cap.ReplyCap t m r)) ptr s) proof (state)
this:
\<forall>t. t \<in> {base..base + 2 ^ magnitude - 1} \<longrightarrow> (\<forall>ptr m r. \<not> cte_wp_at ((=) (cap.ReplyCap t m r)) ptr s)

goal (1 subgoal):
 1. deletionIsSafe base magnitude s' proof (prove)
using this:
\<forall>t. t \<in> {base..base + 2 ^ magnitude - 1} \<longrightarrow> (\<forall>ptr m r. \<not> cte_wp_at ((=) (cap.ReplyCap t m r)) ptr s)

goal (1 subgoal):
 1. \<forall>t. t \<in> {base..base + 2 ^ magnitude - 1} \<longrightarrow> (\<forall>ptr m r. \<not> cte_wp_at' (\<lambda>cte. cteCap cte = capability.ReplyCap t m r) ptr s') proof (prove)
using this:
\<forall>t. t \<in> {base..base + 2 ^ magnitude - 1} \<longrightarrow> (\<forall>ptr m r. \<not> cte_wp_at ((=) (cap.ReplyCap t m r)) ptr s)

goal (1 subgoal):
 1. \<forall>t. t \<in> {base..base + 2 ^ magnitude - 1} \<longrightarrow> (\<forall>ptr m r. \<not> cte_wp_at' (\<lambda>cte. cteCap cte = capability.ReplyCap t m r) ptr s') proof (prove)
goal (1 subgoal):
 1. \<forall>t. t \<in> {base..base + 2 ^ magnitude - 1} \<longrightarrow> (\<forall>ptr m r. \<not> cte_wp_at ((=) (cap.ReplyCap t m r)) ptr s) \<Longrightarrow> \<forall>t. t \<in> {base..base + 2 ^ magnitude - 1} \<longrightarrow> (\<forall>ptr m r. \<not> cte_wp_at' (\<lambda>cte. cteCap cte = capability.ReplyCap t m r) ptr s') proof (prove)
goal (1 subgoal):
 1. \<And>t. t \<in> {base..base + 2 ^ magnitude - 1} \<longrightarrow> (\<forall>ptr m r. \<not> cte_wp_at ((=) (cap.ReplyCap t m r)) ptr s) \<Longrightarrow> t \<in> {base..base + 2 ^ magnitude - 1} \<longrightarrow> (\<forall>ptr m r. \<not> cte_wp_at' (\<lambda>cte. cteCap cte = capability.ReplyCap t m r) ptr s') proof (prove)
goal (1 subgoal):
 1. \<And>t. \<lbrakk>t \<in> {base..base + 2 ^ magnitude - 1}; \<forall>ptr m r. \<not> cte_wp_at ((=) (cap.ReplyCap t m r)) ptr s\<rbrakk> \<Longrightarrow> \<forall>ptr m r. \<not> cte_wp_at' (\<lambda>cte. cteCap cte = capability.ReplyCap t m r) ptr s' proof (prove)
goal (1 subgoal):
 1. \<And>t. \<forall>ptr m r. \<not> cte_wp_at ((=) (cap.ReplyCap t m r)) ptr s \<Longrightarrow> \<forall>ptr m r. \<not> cte_wp_at' (\<lambda>cte. cteCap cte = capability.ReplyCap t m r) ptr s' proof (prove)
goal (1 subgoal):
 1. \<And>t ptr m r. \<forall>ptr m r. \<not> cte_wp_at ((=) (cap.ReplyCap t m r)) ptr s \<Longrightarrow> \<not> cte_wp_at' (\<lambda>cte. cteCap cte = capability.ReplyCap t m r) ptr s' proof (prove)
goal (1 subgoal):
 1. \<And>t ptr m r cte. \<lbrakk>\<forall>ptr. cte_wp_at (\<lambda>_. True) ptr s \<longrightarrow> (\<forall>m r. cte_wp_at ((\<noteq>) (cap.ReplyCap t m r)) ptr s); ctes_of s' ptr = Some cte; cteCap cte = capability.ReplyCap t m r\<rbrakk> \<Longrightarrow> False proof (prove)
goal (3 subgoals):
 1. \<And>t ptr m r cte. \<lbrakk>\<forall>ptr. cte_wp_at (\<lambda>_. True) ptr s \<longrightarrow> (\<forall>m r. cte_wp_at ((\<noteq>) (cap.ReplyCap t m r)) ptr s); ctes_of s' ptr = Some cte; cteCap cte = capability.ReplyCap t m r\<rbrakk> \<Longrightarrow> valid_objs (?s18 t ptr m r cte)
 2. \<And>t ptr m r cte. \<lbrakk>\<forall>ptr. cte_wp_at (\<lambda>_. True) ptr s \<longrightarrow> (\<forall>m r. cte_wp_at ((\<noteq>) (cap.ReplyCap t m r)) ptr s); ctes_of s' ptr = Some cte; cteCap cte = capability.ReplyCap t m r\<rbrakk> \<Longrightarrow> pspace_relation (kheap (?s18 t ptr m r cte)) (ksPSpace s')
 3. \<And>t ptr m r cte. \<lbrakk>\<forall>ptr. cte_wp_at (\<lambda>_. True) ptr s \<longrightarrow> (\<forall>m r. cte_wp_at ((\<noteq>) (cap.ReplyCap t m r)) ptr s); ctes_of s' ptr = Some cte; cteCap cte = capability.ReplyCap t m r; \<exists>c slot. cte_wp_at ((=) c) slot (?s18 t ptr m r cte) \<and> cap_relation c (cteCap cte) \<and> ptr = cte_map slot\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>t ptr m r cte. \<lbrakk>\<forall>ptr. cte_wp_at (\<lambda>_. True) ptr s \<longrightarrow> (\<forall>m r. cte_wp_at ((\<noteq>) (cap.ReplyCap t m r)) ptr s); ctes_of s' ptr = Some cte; cteCap cte = capability.ReplyCap t m r\<rbrakk> \<Longrightarrow> pspace_relation (kheap s) (ksPSpace s')
 2. \<And>t ptr m r cte. \<lbrakk>\<forall>ptr. cte_wp_at (\<lambda>_. True) ptr s \<longrightarrow> (\<forall>m r. cte_wp_at ((\<noteq>) (cap.ReplyCap t m r)) ptr s); ctes_of s' ptr = Some cte; cteCap cte = capability.ReplyCap t m r; \<exists>c slot. cte_wp_at ((=) c) slot s \<and> cap_relation c (cteCap cte) \<and> ptr = cte_map slot\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>t ptr m r cte. \<lbrakk>\<forall>ptr. cte_wp_at (\<lambda>_. True) ptr s \<longrightarrow> (\<forall>m r. cte_wp_at ((\<noteq>) (cap.ReplyCap t m r)) ptr s); ctes_of s' ptr = Some cte; cteCap cte = capability.ReplyCap t m r; \<exists>c slot. cte_wp_at ((=) c) slot s \<and> cap_relation c (cteCap cte) \<and> ptr = cte_map slot\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>t m r cte c a b. \<lbrakk>\<forall>ptr. cte_wp_at (\<lambda>_. True) ptr s \<longrightarrow> (\<forall>m r. cte_wp_at ((\<noteq>) (cap.ReplyCap t m r)) ptr s); ctes_of s' (cte_map (a, b)) = Some cte; cteCap cte = capability.ReplyCap t m r; cte_wp_at ((=) c) (a, b) s; cap_relation c (capability.ReplyCap t m r)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>t m r cte c a b. \<lbrakk>ctes_of s' (cte_map (a, b)) = Some cte; cteCap cte = capability.ReplyCap t m r; cte_wp_at ((=) c) (a, b) s; cap_relation c (capability.ReplyCap t m r); cte_wp_at (\<lambda>_. True) (a, b) s \<longrightarrow> (\<forall>m r. cte_wp_at ((\<noteq>) (cap.ReplyCap t m r)) (a, b) s)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>t m r cte c a b. \<lbrakk>ctes_of s' (cte_map (a, b)) = Some cte; cteCap cte = capability.ReplyCap t m r; caps_of_state s (a, b) = Some c; cap_relation c (capability.ReplyCap t m r); \<forall>m r. cap.ReplyCap t m r \<noteq> c\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>t m r cte c a b x53. \<lbrakk>ctes_of s' (cte_map (a, b)) = Some cte; cteCap cte = capability.ReplyCap t m (AllowGrant \<in> x53); caps_of_state s (a, b) = Some (cap.ReplyCap t m x53); r = (AllowGrant \<in> x53); \<forall>ma. ma = (\<not> m); c = cap.ReplyCap t m x53\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals! proof (state)
this:
\<forall>t. t \<in> {base..base + 2 ^ magnitude - 1} \<longrightarrow> (\<forall>ptr m r. \<not> cte_wp_at' (\<lambda>cte. cteCap cte = capability.ReplyCap t m r) ptr s')

goal (1 subgoal):
 1. deletionIsSafe base magnitude s' proof (prove)
goal (1 subgoal):
 1. \<And>ko p. \<lbrakk>ksPSpace s' p = Some (KOArch ko); p \<in> {base..base + 2 ^ magnitude - 1}\<rbrakk> \<Longrightarrow> 6 \<le> magnitude proof (prove)
using this:
(s, s') \<in> state_relation
valid_pspace s
valid_untyped (cap.UntypedCap d base magnitude idx) s

goal (1 subgoal):
 1. \<And>ko p. \<lbrakk>ksPSpace s' p = Some (KOArch ko); p \<in> {base..base + 2 ^ magnitude - 1}\<rbrakk> \<Longrightarrow> 6 \<le> magnitude proof (prove)
goal (1 subgoal):
 1. \<And>ko p. \<lbrakk>ksPSpace s' p = Some (KOArch ko); p \<in> {base..base + 2 ^ magnitude - 1}; valid_pspace s; valid_untyped (cap.UntypedCap d base magnitude idx) s; pspace_relation (kheap s) (ksPSpace s'); ekheap_relation (ekheap s) (ksPSpace s'); sched_act_relation (scheduler_action s) (ksSchedulerAction s'); ready_queues_relation (ready_queues s) (ksReadyQueues s'); ghost_relation (kheap s) (gsUserPages s') (gsCNodes s'); cdt_relation (swp (cte_wp_at (\<lambda>_. True)) s) (cdt s) (ctes_of s'); cdt_list_relation (cdt_list s) (cdt s) (ctes_of s'); revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) (ctes_of s'); (arch_state s, ksArchState s') \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState s'); cur_thread s = ksCurThread s'; idle_thread s = ksIdleThread s'; machine_state s = ksMachineState s'; work_units_completed s = ksWorkUnitsCompleted s'; domain_index s = ksDomScheduleIdx s'; domain_list s = ksDomSchedule s'; cur_domain s = ksCurDomain s'; domain_time s = ksDomainTime s'\<rbrakk> \<Longrightarrow> 6 \<le> magnitude proof (prove)
goal (1 subgoal):
 1. \<And>ko p y koa P. \<lbrakk>p \<in> {base..base + 2 ^ magnitude - 1}; valid_pspace s; valid_untyped (cap.UntypedCap d base magnitude idx) s; pspace_relation (kheap s) (ksPSpace s'); ekheap_relation (ekheap s) (ksPSpace s'); sched_act_relation (scheduler_action s) (ksSchedulerAction s'); ready_queues_relation (ready_queues s) (ksReadyQueues s'); ghost_relation (kheap s) (gsUserPages s') (gsCNodes s'); cdt_relation (swp (cte_wp_at (\<lambda>_. True)) s) (cdt s) (ctes_of s'); cdt_list_relation (cdt_list s) (cdt s) (ctes_of s'); revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) (ctes_of s'); (arch_state s, ksArchState s') \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState s'); cur_thread s = ksCurThread s'; idle_thread s = ksIdleThread s'; machine_state s = ksMachineState s'; work_units_completed s = ksWorkUnitsCompleted s'; domain_index s = ksDomScheduleIdx s'; domain_list s = ksDomSchedule s'; cur_domain s = ksCurDomain s'; domain_time s = ksDomainTime s'; kheap s y = Some koa; (p, P) \<in> obj_relation_cuts koa y; P koa (KOArch ko)\<rbrakk> \<Longrightarrow> 6 \<le> magnitude proof (prove)
goal (5 subgoals):
 1. \<And>ko p y koa P. \<lbrakk>p \<in> {base..base + 2 ^ magnitude - 1}; valid_pspace s; valid_untyped (cap.UntypedCap d base magnitude idx) s; pspace_relation (kheap s) (ksPSpace s'); ekheap_relation (ekheap s) (ksPSpace s'); sched_act_relation (scheduler_action s) (ksSchedulerAction s'); ready_queues_relation (ready_queues s) (ksReadyQueues s'); ghost_relation (kheap s) (gsUserPages s') (gsCNodes s'); cdt_relation (swp (cte_wp_at (\<lambda>_. True)) s) (cdt s) (ctes_of s'); cdt_list_relation (cdt_list s) (cdt s) (ctes_of s'); revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) (ctes_of s'); (arch_state s, ksArchState s') \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState s'); cur_thread s = ksCurThread s'; idle_thread s = ksIdleThread s'; machine_state s = ksMachineState s'; work_units_completed s = ksWorkUnitsCompleted s'; domain_index s = ksDomScheduleIdx s'; domain_list s = ksDomSchedule s'; cur_domain s = ksCurDomain s'; domain_time s = ksDomainTime s'; kheap s y = Some koa; (p, P) \<in> obj_relation_cuts koa y; P koa (KOArch ko)\<rbrakk> \<Longrightarrow> kheap (?s23 ko p y koa P) y = Some koa
 2. \<And>ko p y koa P. \<lbrakk>p \<in> {base..base + 2 ^ magnitude - 1}; valid_pspace s; valid_untyped (cap.UntypedCap d base magnitude idx) s; pspace_relation (kheap s) (ksPSpace s'); ekheap_relation (ekheap s) (ksPSpace s'); sched_act_relation (scheduler_action s) (ksSchedulerAction s'); ready_queues_relation (ready_queues s) (ksReadyQueues s'); ghost_relation (kheap s) (gsUserPages s') (gsCNodes s'); cdt_relation (swp (cte_wp_at (\<lambda>_. True)) s) (cdt s) (ctes_of s'); cdt_list_relation (cdt_list s) (cdt s) (ctes_of s'); revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) (ctes_of s'); (arch_state s, ksArchState s') \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState s'); cur_thread s = ksCurThread s'; idle_thread s = ksIdleThread s'; machine_state s = ksMachineState s'; work_units_completed s = ksWorkUnitsCompleted s'; domain_index s = ksDomScheduleIdx s'; domain_list s = ksDomSchedule s'; cur_domain s = ksCurDomain s'; domain_time s = ksDomainTime s'; kheap s y = Some koa; (p, P) \<in> obj_relation_cuts koa y; P koa (KOArch ko)\<rbrakk> \<Longrightarrow> valid_objs (?s23 ko p y koa P)
 3. \<And>ko p y koa P. \<lbrakk>p \<in> {base..base + 2 ^ magnitude - 1}; valid_pspace s; valid_untyped (cap.UntypedCap d base magnitude idx) s; pspace_relation (kheap s) (ksPSpace s'); ekheap_relation (ekheap s) (ksPSpace s'); sched_act_relation (scheduler_action s) (ksSchedulerAction s'); ready_queues_relation (ready_queues s) (ksReadyQueues s'); ghost_relation (kheap s) (gsUserPages s') (gsCNodes s'); cdt_relation (swp (cte_wp_at (\<lambda>_. True)) s) (cdt s) (ctes_of s'); cdt_list_relation (cdt_list s) (cdt s) (ctes_of s'); revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) (ctes_of s'); (arch_state s, ksArchState s') \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState s'); cur_thread s = ksCurThread s'; idle_thread s = ksIdleThread s'; machine_state s = ksMachineState s'; work_units_completed s = ksWorkUnitsCompleted s'; domain_index s = ksDomScheduleIdx s'; domain_list s = ksDomSchedule s'; cur_domain s = ksCurDomain s'; domain_time s = ksDomainTime s'; kheap s y = Some koa; (p, P) \<in> obj_relation_cuts koa y; P koa (KOArch ko)\<rbrakk> \<Longrightarrow> pspace_aligned (?s23 ko p y koa P)
 4. \<And>ko p y koa P. \<lbrakk>p \<in> {base..base + 2 ^ magnitude - 1}; valid_pspace s; valid_untyped (cap.UntypedCap d base magnitude idx) s; pspace_relation (kheap s) (ksPSpace s'); ekheap_relation (ekheap s) (ksPSpace s'); sched_act_relation (scheduler_action s) (ksSchedulerAction s'); ready_queues_relation (ready_queues s) (ksReadyQueues s'); ghost_relation (kheap s) (gsUserPages s') (gsCNodes s'); cdt_relation (swp (cte_wp_at (\<lambda>_. True)) s) (cdt s) (ctes_of s'); cdt_list_relation (cdt_list s) (cdt s) (ctes_of s'); revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) (ctes_of s'); (arch_state s, ksArchState s') \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState s'); cur_thread s = ksCurThread s'; idle_thread s = ksIdleThread s'; machine_state s = ksMachineState s'; work_units_completed s = ksWorkUnitsCompleted s'; domain_index s = ksDomScheduleIdx s'; domain_list s = ksDomSchedule s'; cur_domain s = ksCurDomain s'; domain_time s = ksDomainTime s'; kheap s y = Some koa; (p, P) \<in> obj_relation_cuts koa y; P koa (KOArch ko)\<rbrakk> \<Longrightarrow> valid_untyped (cap.UntypedCap (?d23 ko p y koa P) (?base23 ko p y koa P) (?bits23 ko p y koa P) (?idx23 ko p y koa P)) (?s23 ko p y koa P)
 5. \<And>ko p y koa P. \<lbrakk>p \<in> {base..base + 2 ^ magnitude - 1}; valid_pspace s; valid_untyped (cap.UntypedCap d base magnitude idx) s; pspace_relation (kheap s) (ksPSpace s'); ekheap_relation (ekheap s) (ksPSpace s'); sched_act_relation (scheduler_action s) (ksSchedulerAction s'); ready_queues_relation (ready_queues s) (ksReadyQueues s'); ghost_relation (kheap s) (gsUserPages s') (gsCNodes s'); cdt_relation (swp (cte_wp_at (\<lambda>_. True)) s) (cdt s) (ctes_of s'); cdt_list_relation (cdt_list s) (cdt s) (ctes_of s'); revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) (ctes_of s'); (arch_state s, ksArchState s') \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState s'); cur_thread s = ksCurThread s'; idle_thread s = ksIdleThread s'; machine_state s = ksMachineState s'; work_units_completed s = ksWorkUnitsCompleted s'; domain_index s = ksDomScheduleIdx s'; domain_list s = ksDomSchedule s'; cur_domain s = ksCurDomain s'; domain_time s = ksDomainTime s'; kheap s y = Some koa; (p, P) \<in> obj_relation_cuts koa y; P koa (KOArch ko); (p \<in> {?base23 ko p y koa P..?base23 ko p y koa P + 2 ^ ?bits23 ko p y koa P - 1}) = (y \<in> {?base23 ko p y koa P..?base23 ko p y koa P + 2 ^ ?bits23 ko p y koa P - 1})\<rbrakk> \<Longrightarrow> 6 \<le> magnitude proof (prove)
goal (4 subgoals):
 1. \<And>ko p y koa P. \<lbrakk>p \<in> {base..base + 2 ^ magnitude - 1}; valid_pspace s; valid_untyped (cap.UntypedCap d base magnitude idx) s; pspace_relation (kheap s) (ksPSpace s'); ekheap_relation (ekheap s) (ksPSpace s'); sched_act_relation (scheduler_action s) (ksSchedulerAction s'); ready_queues_relation (ready_queues s) (ksReadyQueues s'); ghost_relation (kheap s) (gsUserPages s') (gsCNodes s'); cdt_relation (swp (cte_wp_at (\<lambda>_. True)) s) (cdt s) (ctes_of s'); cdt_list_relation (cdt_list s) (cdt s) (ctes_of s'); revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) (ctes_of s'); (arch_state s, ksArchState s') \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState s'); cur_thread s = ksCurThread s'; idle_thread s = ksIdleThread s'; machine_state s = ksMachineState s'; work_units_completed s = ksWorkUnitsCompleted s'; domain_index s = ksDomScheduleIdx s'; domain_list s = ksDomSchedule s'; cur_domain s = ksCurDomain s'; domain_time s = ksDomainTime s'; kheap s y = Some koa; (p, P) \<in> obj_relation_cuts koa y; P koa (KOArch ko)\<rbrakk> \<Longrightarrow> valid_objs s
 2. \<And>ko p y koa P. \<lbrakk>p \<in> {base..base + 2 ^ magnitude - 1}; valid_pspace s; valid_untyped (cap.UntypedCap d base magnitude idx) s; pspace_relation (kheap s) (ksPSpace s'); ekheap_relation (ekheap s) (ksPSpace s'); sched_act_relation (scheduler_action s) (ksSchedulerAction s'); ready_queues_relation (ready_queues s) (ksReadyQueues s'); ghost_relation (kheap s) (gsUserPages s') (gsCNodes s'); cdt_relation (swp (cte_wp_at (\<lambda>_. True)) s) (cdt s) (ctes_of s'); cdt_list_relation (cdt_list s) (cdt s) (ctes_of s'); revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) (ctes_of s'); (arch_state s, ksArchState s') \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState s'); cur_thread s = ksCurThread s'; idle_thread s = ksIdleThread s'; machine_state s = ksMachineState s'; work_units_completed s = ksWorkUnitsCompleted s'; domain_index s = ksDomScheduleIdx s'; domain_list s = ksDomSchedule s'; cur_domain s = ksCurDomain s'; domain_time s = ksDomainTime s'; kheap s y = Some koa; (p, P) \<in> obj_relation_cuts koa y; P koa (KOArch ko)\<rbrakk> \<Longrightarrow> pspace_aligned s
 3. \<And>ko p y koa P. \<lbrakk>p \<in> {base..base + 2 ^ magnitude - 1}; valid_pspace s; valid_untyped (cap.UntypedCap d base magnitude idx) s; pspace_relation (kheap s) (ksPSpace s'); ekheap_relation (ekheap s) (ksPSpace s'); sched_act_relation (scheduler_action s) (ksSchedulerAction s'); ready_queues_relation (ready_queues s) (ksReadyQueues s'); ghost_relation (kheap s) (gsUserPages s') (gsCNodes s'); cdt_relation (swp (cte_wp_at (\<lambda>_. True)) s) (cdt s) (ctes_of s'); cdt_list_relation (cdt_list s) (cdt s) (ctes_of s'); revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) (ctes_of s'); (arch_state s, ksArchState s') \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState s'); cur_thread s = ksCurThread s'; idle_thread s = ksIdleThread s'; machine_state s = ksMachineState s'; work_units_completed s = ksWorkUnitsCompleted s'; domain_index s = ksDomScheduleIdx s'; domain_list s = ksDomSchedule s'; cur_domain s = ksCurDomain s'; domain_time s = ksDomainTime s'; kheap s y = Some koa; (p, P) \<in> obj_relation_cuts koa y; P koa (KOArch ko)\<rbrakk> \<Longrightarrow> valid_untyped (cap.UntypedCap (?d23 ko p y koa P) (?base23 ko p y koa P) (?bits23 ko p y koa P) (?idx23 ko p y koa P)) s
 4. \<And>ko p y koa P. \<lbrakk>p \<in> {base..base + 2 ^ magnitude - 1}; valid_pspace s; valid_untyped (cap.UntypedCap d base magnitude idx) s; pspace_relation (kheap s) (ksPSpace s'); ekheap_relation (ekheap s) (ksPSpace s'); sched_act_relation (scheduler_action s) (ksSchedulerAction s'); ready_queues_relation (ready_queues s) (ksReadyQueues s'); ghost_relation (kheap s) (gsUserPages s') (gsCNodes s'); cdt_relation (swp (cte_wp_at (\<lambda>_. True)) s) (cdt s) (ctes_of s'); cdt_list_relation (cdt_list s) (cdt s) (ctes_of s'); revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) (ctes_of s'); (arch_state s, ksArchState s') \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState s'); cur_thread s = ksCurThread s'; idle_thread s = ksIdleThread s'; machine_state s = ksMachineState s'; work_units_completed s = ksWorkUnitsCompleted s'; domain_index s = ksDomScheduleIdx s'; domain_list s = ksDomSchedule s'; cur_domain s = ksCurDomain s'; domain_time s = ksDomainTime s'; kheap s y = Some koa; (p, P) \<in> obj_relation_cuts koa y; P koa (KOArch ko); (p \<in> {?base23 ko p y koa P..?base23 ko p y koa P + 2 ^ ?bits23 ko p y koa P - 1}) = (y \<in> {?base23 ko p y koa P..?base23 ko p y koa P + 2 ^ ?bits23 ko p y koa P - 1})\<rbrakk> \<Longrightarrow> 6 \<le> magnitude proof (prove)
goal (2 subgoals):
 1. \<And>ko p y koa P. \<lbrakk>p \<in> {base..base + 2 ^ magnitude - 1}; valid_untyped (cap.UntypedCap d base magnitude idx) s; pspace_relation (kheap s) (ksPSpace s'); ekheap_relation (ekheap s) (ksPSpace s'); sched_act_relation (scheduler_action s) (ksSchedulerAction s'); ready_queues_relation (ready_queues s) (ksReadyQueues s'); ghost_relation (kheap s) (gsUserPages s') (gsCNodes s'); cdt_relation (swp (cte_wp_at (\<lambda>_. True)) s) (cdt s) (ctes_of s'); cdt_list_relation (cdt_list s) (cdt s) (ctes_of s'); revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) (ctes_of s'); (arch_state s, ksArchState s') \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState s'); cur_thread s = ksCurThread s'; idle_thread s = ksIdleThread s'; machine_state s = ksMachineState s'; work_units_completed s = ksWorkUnitsCompleted s'; domain_index s = ksDomScheduleIdx s'; domain_list s = ksDomSchedule s'; cur_domain s = ksCurDomain s'; domain_time s = ksDomainTime s'; kheap s y = Some koa; (p, P) \<in> obj_relation_cuts koa y; P koa (KOArch ko); valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s)\<rbrakk> \<Longrightarrow> valid_untyped (cap.UntypedCap (?d23 ko p y koa P) (?base23 ko p y koa P) (?bits23 ko p y koa P) (?idx23 ko p y koa P)) s
 2. \<And>ko p y koa P. \<lbrakk>p \<in> {base..base + 2 ^ magnitude - 1}; valid_pspace s; valid_untyped (cap.UntypedCap d base magnitude idx) s; pspace_relation (kheap s) (ksPSpace s'); ekheap_relation (ekheap s) (ksPSpace s'); sched_act_relation (scheduler_action s) (ksSchedulerAction s'); ready_queues_relation (ready_queues s) (ksReadyQueues s'); ghost_relation (kheap s) (gsUserPages s') (gsCNodes s'); cdt_relation (swp (cte_wp_at (\<lambda>_. True)) s) (cdt s) (ctes_of s'); cdt_list_relation (cdt_list s) (cdt s) (ctes_of s'); revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) (ctes_of s'); (arch_state s, ksArchState s') \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState s'); cur_thread s = ksCurThread s'; idle_thread s = ksIdleThread s'; machine_state s = ksMachineState s'; work_units_completed s = ksWorkUnitsCompleted s'; domain_index s = ksDomScheduleIdx s'; domain_list s = ksDomSchedule s'; cur_domain s = ksCurDomain s'; domain_time s = ksDomainTime s'; kheap s y = Some koa; (p, P) \<in> obj_relation_cuts koa y; P koa (KOArch ko); (p \<in> {?base23 ko p y koa P..?base23 ko p y koa P + 2 ^ ?bits23 ko p y koa P - 1}) = (y \<in> {?base23 ko p y koa P..?base23 ko p y koa P + 2 ^ ?bits23 ko p y koa P - 1})\<rbrakk> \<Longrightarrow> 6 \<le> magnitude proof (prove)
goal (1 subgoal):
 1. \<And>ko p y koa P. \<lbrakk>p \<in> {base..base + 2 ^ magnitude - 1}; valid_pspace s; valid_untyped (cap.UntypedCap d base magnitude idx) s; pspace_relation (kheap s) (ksPSpace s'); ekheap_relation (ekheap s) (ksPSpace s'); sched_act_relation (scheduler_action s) (ksSchedulerAction s'); ready_queues_relation (ready_queues s) (ksReadyQueues s'); ghost_relation (kheap s) (gsUserPages s') (gsCNodes s'); cdt_relation (swp (cte_wp_at (\<lambda>_. True)) s) (cdt s) (ctes_of s'); cdt_list_relation (cdt_list s) (cdt s) (ctes_of s'); revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) (ctes_of s'); (arch_state s, ksArchState s') \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState s'); cur_thread s = ksCurThread s'; idle_thread s = ksIdleThread s'; machine_state s = ksMachineState s'; work_units_completed s = ksWorkUnitsCompleted s'; domain_index s = ksDomScheduleIdx s'; domain_list s = ksDomSchedule s'; cur_domain s = ksCurDomain s'; domain_time s = ksDomainTime s'; kheap s y = Some koa; (p, P) \<in> obj_relation_cuts koa y; P koa (KOArch ko); (p \<in> {base..base + 2 ^ magnitude - 1}) = (y \<in> {base..base + 2 ^ magnitude - 1})\<rbrakk> \<Longrightarrow> 6 \<le> magnitude proof (prove)
goal (1 subgoal):
 1. \<And>ko p y koa P. \<lbrakk>y \<in> {base..base + 2 ^ magnitude - 1}; valid_pspace s; \<forall>p obj. kheap s p = Some obj \<longrightarrow> obj_range p obj \<inter> {base..base + 2 ^ magnitude - 1} \<noteq> {} \<longrightarrow> obj_range p obj \<subseteq> {base..base + 2 ^ magnitude - 1} \<and> (if idx < 2 ^ magnitude then {base + word_of_nat idx..base + 2 ^ magnitude - 1} else {}) \<inter> obj_range p obj = {}; pspace_relation (kheap s) (ksPSpace s'); ekheap_relation (ekheap s) (ksPSpace s'); sched_act_relation (scheduler_action s) (ksSchedulerAction s'); ready_queues_relation (ready_queues s) (ksReadyQueues s'); ghost_relation (kheap s) (gsUserPages s') (gsCNodes s'); cdt_relation (swp (cte_wp_at (\<lambda>_. True)) s) (cdt s) (ctes_of s'); cdt_list_relation (cdt_list s) (cdt s) (ctes_of s'); revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) (ctes_of s'); (arch_state s, ksArchState s') \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState s'); cur_thread s = ksCurThread s'; idle_thread s = ksIdleThread s'; machine_state s = ksMachineState s'; work_units_completed s = ksWorkUnitsCompleted s'; domain_index s = ksDomScheduleIdx s'; domain_list s = ksDomSchedule s'; cur_domain s = ksCurDomain s'; domain_time s = ksDomainTime s'; kheap s y = Some koa; (p, P) \<in> obj_relation_cuts koa y; P koa (KOArch ko); p \<in> {base..base + 2 ^ magnitude - 1}\<rbrakk> \<Longrightarrow> 6 \<le> magnitude proof (prove)
goal (1 subgoal):
 1. \<And>ko p y koa P. \<lbrakk>y \<in> {base..base + 2 ^ magnitude - 1}; valid_pspace s; pspace_relation (kheap s) (ksPSpace s'); ekheap_relation (ekheap s) (ksPSpace s'); sched_act_relation (scheduler_action s) (ksSchedulerAction s'); ready_queues_relation (ready_queues s) (ksReadyQueues s'); ghost_relation (kheap s) (gsUserPages s') (gsCNodes s'); cdt_relation (swp (cte_wp_at (\<lambda>_. True)) s) (cdt s) (ctes_of s'); cdt_list_relation (cdt_list s) (cdt s) (ctes_of s'); revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) (ctes_of s'); (arch_state s, ksArchState s') \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState s'); cur_thread s = ksCurThread s'; idle_thread s = ksIdleThread s'; machine_state s = ksMachineState s'; work_units_completed s = ksWorkUnitsCompleted s'; domain_index s = ksDomScheduleIdx s'; domain_list s = ksDomSchedule s'; cur_domain s = ksCurDomain s'; domain_time s = ksDomainTime s'; kheap s y = Some koa; (p, P) \<in> obj_relation_cuts koa y; P koa (KOArch ko); p \<in> {base..base + 2 ^ magnitude - 1}; kheap s (?p37 ko p y koa P) = Some (?obj39 ko p y koa P) \<longrightarrow> obj_range (?p37 ko p y koa P) (?obj39 ko p y koa P) \<inter> {base..base + 2 ^ magnitude - 1} \<noteq> {} \<longrightarrow> obj_range (?p37 ko p y koa P) (?obj39 ko p y koa P) \<subseteq> {base..base + 2 ^ magnitude - 1} \<and> (if idx < 2 ^ magnitude then {base + word_of_nat idx..base + 2 ^ magnitude - 1} else {}) \<inter> obj_range (?p37 ko p y koa P) (?obj39 ko p y koa P) = {}\<rbrakk> \<Longrightarrow> 6 \<le> magnitude proof (prove)
goal (1 subgoal):
 1. \<And>ko p y koa P. \<lbrakk>y \<in> {base..base + 2 ^ magnitude - 1}; valid_pspace s; pspace_relation (kheap s) (ksPSpace s'); ekheap_relation (ekheap s) (ksPSpace s'); sched_act_relation (scheduler_action s) (ksSchedulerAction s'); ready_queues_relation (ready_queues s) (ksReadyQueues s'); ghost_relation (kheap s) (gsUserPages s') (gsCNodes s'); cdt_relation (swp (cte_wp_at (\<lambda>_. True)) s) (cdt s) (ctes_of s'); cdt_list_relation (cdt_list s) (cdt s) (ctes_of s'); revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) (ctes_of s'); (arch_state s, ksArchState s') \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState s'); cur_thread s = ksCurThread s'; idle_thread s = ksIdleThread s'; machine_state s = ksMachineState s'; work_units_completed s = ksWorkUnitsCompleted s'; domain_index s = ksDomScheduleIdx s'; domain_list s = ksDomSchedule s'; cur_domain s = ksCurDomain s'; domain_time s = ksDomainTime s'; kheap s y = Some koa; (p, P) \<in> obj_relation_cuts koa y; P koa (KOArch ko); p \<in> {base..base + 2 ^ magnitude - 1}; obj_range y koa \<inter> {base..base + 2 ^ magnitude - 1} \<noteq> {} \<longrightarrow> obj_range y koa \<subseteq> {base..base + 2 ^ magnitude - 1} \<and> (if idx < 2 ^ magnitude then {base + word_of_nat idx..base + 2 ^ magnitude - 1} else {}) \<inter> obj_range y koa = {}\<rbrakk> \<Longrightarrow> 6 \<le> magnitude proof (prove)
goal (2 subgoals):
 1. \<And>ko p y koa P. \<lbrakk>y \<in> {base..base + 2 ^ magnitude - 1}; valid_pspace s; pspace_relation (kheap s) (ksPSpace s'); ekheap_relation (ekheap s) (ksPSpace s'); sched_act_relation (scheduler_action s) (ksSchedulerAction s'); ready_queues_relation (ready_queues s) (ksReadyQueues s'); ghost_relation (kheap s) (gsUserPages s') (gsCNodes s'); cdt_relation (swp (cte_wp_at (\<lambda>_. True)) s) (cdt s) (ctes_of s'); cdt_list_relation (cdt_list s) (cdt s) (ctes_of s'); revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) (ctes_of s'); (arch_state s, ksArchState s') \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState s'); cur_thread s = ksCurThread s'; idle_thread s = ksIdleThread s'; machine_state s = ksMachineState s'; work_units_completed s = ksWorkUnitsCompleted s'; domain_index s = ksDomScheduleIdx s'; domain_list s = ksDomSchedule s'; cur_domain s = ksCurDomain s'; domain_time s = ksDomainTime s'; kheap s y = Some koa; (p, P) \<in> obj_relation_cuts koa y; P koa (KOArch ko); p \<in> {base..base + 2 ^ magnitude - 1}\<rbrakk> \<Longrightarrow> obj_range y koa \<inter> {base..base + 2 ^ magnitude - 1} \<noteq> {}
 2. \<And>ko p y koa P. \<lbrakk>y \<in> {base..base + 2 ^ magnitude - 1}; valid_pspace s; pspace_relation (kheap s) (ksPSpace s'); ekheap_relation (ekheap s) (ksPSpace s'); sched_act_relation (scheduler_action s) (ksSchedulerAction s'); ready_queues_relation (ready_queues s) (ksReadyQueues s'); ghost_relation (kheap s) (gsUserPages s') (gsCNodes s'); cdt_relation (swp (cte_wp_at (\<lambda>_. True)) s) (cdt s) (ctes_of s'); cdt_list_relation (cdt_list s) (cdt s) (ctes_of s'); revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) (ctes_of s'); (arch_state s, ksArchState s') \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState s'); cur_thread s = ksCurThread s'; idle_thread s = ksIdleThread s'; machine_state s = ksMachineState s'; work_units_completed s = ksWorkUnitsCompleted s'; domain_index s = ksDomScheduleIdx s'; domain_list s = ksDomSchedule s'; cur_domain s = ksCurDomain s'; domain_time s = ksDomainTime s'; kheap s y = Some koa; (p, P) \<in> obj_relation_cuts koa y; P koa (KOArch ko); p \<in> {base..base + 2 ^ magnitude - 1}; obj_range y koa \<subseteq> {base..base + 2 ^ magnitude - 1} \<and> (if idx < 2 ^ magnitude then {base + word_of_nat idx..base + 2 ^ magnitude - 1} else {}) \<inter> obj_range y koa = {}\<rbrakk> \<Longrightarrow> 6 \<le> magnitude proof (prove)
goal (4 subgoals):
 1. \<And>ko p y koa P. \<lbrakk>y \<in> {base..base + 2 ^ magnitude - 1}; valid_pspace s; pspace_relation (kheap s) (ksPSpace s'); ekheap_relation (ekheap s) (ksPSpace s'); sched_act_relation (scheduler_action s) (ksSchedulerAction s'); ready_queues_relation (ready_queues s) (ksReadyQueues s'); ghost_relation (kheap s) (gsUserPages s') (gsCNodes s'); cdt_relation (swp (cte_wp_at (\<lambda>_. True)) s) (cdt s) (ctes_of s'); cdt_list_relation (cdt_list s) (cdt s) (ctes_of s'); revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) (ctes_of s'); (arch_state s, ksArchState s') \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState s'); cur_thread s = ksCurThread s'; idle_thread s = ksIdleThread s'; machine_state s = ksMachineState s'; work_units_completed s = ksWorkUnitsCompleted s'; domain_index s = ksDomScheduleIdx s'; domain_list s = ksDomSchedule s'; cur_domain s = ksCurDomain s'; domain_time s = ksDomainTime s'; (p, P) \<in> obj_relation_cuts koa y; P koa (KOArch ko); p \<in> {base..base + 2 ^ magnitude - 1}\<rbrakk> \<Longrightarrow> pspace_aligned s
 2. \<And>ko p y koa P. \<lbrakk>y \<in> {base..base + 2 ^ magnitude - 1}; valid_pspace s; pspace_relation (kheap s) (ksPSpace s'); ekheap_relation (ekheap s) (ksPSpace s'); sched_act_relation (scheduler_action s) (ksSchedulerAction s'); ready_queues_relation (ready_queues s) (ksReadyQueues s'); ghost_relation (kheap s) (gsUserPages s') (gsCNodes s'); cdt_relation (swp (cte_wp_at (\<lambda>_. True)) s) (cdt s) (ctes_of s'); cdt_list_relation (cdt_list s) (cdt s) (ctes_of s'); revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) (ctes_of s'); (arch_state s, ksArchState s') \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState s'); cur_thread s = ksCurThread s'; idle_thread s = ksIdleThread s'; machine_state s = ksMachineState s'; work_units_completed s = ksWorkUnitsCompleted s'; domain_index s = ksDomScheduleIdx s'; domain_list s = ksDomSchedule s'; cur_domain s = ksCurDomain s'; domain_time s = ksDomainTime s'; (p, P) \<in> obj_relation_cuts koa y; P koa (KOArch ko); p \<in> {base..base + 2 ^ magnitude - 1}\<rbrakk> \<Longrightarrow> valid_objs s
 3. \<And>ko p y koa P. \<lbrakk>y \<in> {base..base + 2 ^ magnitude - 1}; valid_pspace s; pspace_relation (kheap s) (ksPSpace s'); ekheap_relation (ekheap s) (ksPSpace s'); sched_act_relation (scheduler_action s) (ksSchedulerAction s'); ready_queues_relation (ready_queues s) (ksReadyQueues s'); ghost_relation (kheap s) (gsUserPages s') (gsCNodes s'); cdt_relation (swp (cte_wp_at (\<lambda>_. True)) s) (cdt s) (ctes_of s'); cdt_list_relation (cdt_list s) (cdt s) (ctes_of s'); revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) (ctes_of s'); (arch_state s, ksArchState s') \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState s'); cur_thread s = ksCurThread s'; idle_thread s = ksIdleThread s'; machine_state s = ksMachineState s'; work_units_completed s = ksWorkUnitsCompleted s'; domain_index s = ksDomScheduleIdx s'; domain_list s = ksDomSchedule s'; cur_domain s = ksCurDomain s'; domain_time s = ksDomainTime s'; (p, P) \<in> obj_relation_cuts koa y; P koa (KOArch ko); p \<in> {base..base + 2 ^ magnitude - 1}; y \<in> obj_range y koa\<rbrakk> \<Longrightarrow> obj_range y koa \<inter> {base..base + 2 ^ magnitude - 1} \<noteq> {}
 4. \<And>ko p y koa P. \<lbrakk>y \<in> {base..base + 2 ^ magnitude - 1}; valid_pspace s; pspace_relation (kheap s) (ksPSpace s'); ekheap_relation (ekheap s) (ksPSpace s'); sched_act_relation (scheduler_action s) (ksSchedulerAction s'); ready_queues_relation (ready_queues s) (ksReadyQueues s'); ghost_relation (kheap s) (gsUserPages s') (gsCNodes s'); cdt_relation (swp (cte_wp_at (\<lambda>_. True)) s) (cdt s) (ctes_of s'); cdt_list_relation (cdt_list s) (cdt s) (ctes_of s'); revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) (ctes_of s'); (arch_state s, ksArchState s') \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState s'); cur_thread s = ksCurThread s'; idle_thread s = ksIdleThread s'; machine_state s = ksMachineState s'; work_units_completed s = ksWorkUnitsCompleted s'; domain_index s = ksDomScheduleIdx s'; domain_list s = ksDomSchedule s'; cur_domain s = ksCurDomain s'; domain_time s = ksDomainTime s'; kheap s y = Some koa; (p, P) \<in> obj_relation_cuts koa y; P koa (KOArch ko); p \<in> {base..base + 2 ^ magnitude - 1}; obj_range y koa \<subseteq> {base..base + 2 ^ magnitude - 1} \<and> (if idx < 2 ^ magnitude then {base + word_of_nat idx..base + 2 ^ magnitude - 1} else {}) \<inter> obj_range y koa = {}\<rbrakk> \<Longrightarrow> 6 \<le> magnitude proof (prove)
goal (2 subgoals):
 1. \<And>ko p y koa P. \<lbrakk>y \<in> {base..base + 2 ^ magnitude - 1}; valid_pspace s; pspace_relation (kheap s) (ksPSpace s'); ekheap_relation (ekheap s) (ksPSpace s'); sched_act_relation (scheduler_action s) (ksSchedulerAction s'); ready_queues_relation (ready_queues s) (ksReadyQueues s'); ghost_relation (kheap s) (gsUserPages s') (gsCNodes s'); cdt_relation (swp (cte_wp_at (\<lambda>_. True)) s) (cdt s) (ctes_of s'); cdt_list_relation (cdt_list s) (cdt s) (ctes_of s'); revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) (ctes_of s'); (arch_state s, ksArchState s') \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState s'); cur_thread s = ksCurThread s'; idle_thread s = ksIdleThread s'; machine_state s = ksMachineState s'; work_units_completed s = ksWorkUnitsCompleted s'; domain_index s = ksDomScheduleIdx s'; domain_list s = ksDomSchedule s'; cur_domain s = ksCurDomain s'; domain_time s = ksDomainTime s'; (p, P) \<in> obj_relation_cuts koa y; P koa (KOArch ko); p \<in> {base..base + 2 ^ magnitude - 1}; y \<in> obj_range y koa; obj_range y koa \<inter> {base..base + 2 ^ magnitude - 1} = {}\<rbrakk> \<Longrightarrow> False
 2. \<And>ko p y koa P. \<lbrakk>y \<in> {base..base + 2 ^ magnitude - 1}; valid_pspace s; pspace_relation (kheap s) (ksPSpace s'); ekheap_relation (ekheap s) (ksPSpace s'); sched_act_relation (scheduler_action s) (ksSchedulerAction s'); ready_queues_relation (ready_queues s) (ksReadyQueues s'); ghost_relation (kheap s) (gsUserPages s') (gsCNodes s'); cdt_relation (swp (cte_wp_at (\<lambda>_. True)) s) (cdt s) (ctes_of s'); cdt_list_relation (cdt_list s) (cdt s) (ctes_of s'); revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) (ctes_of s'); (arch_state s, ksArchState s') \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState s'); cur_thread s = ksCurThread s'; idle_thread s = ksIdleThread s'; machine_state s = ksMachineState s'; work_units_completed s = ksWorkUnitsCompleted s'; domain_index s = ksDomScheduleIdx s'; domain_list s = ksDomSchedule s'; cur_domain s = ksCurDomain s'; domain_time s = ksDomainTime s'; kheap s y = Some koa; (p, P) \<in> obj_relation_cuts koa y; P koa (KOArch ko); p \<in> {base..base + 2 ^ magnitude - 1}; obj_range y koa \<subseteq> {base..base + 2 ^ magnitude - 1} \<and> (if idx < 2 ^ magnitude then {base + word_of_nat idx..base + 2 ^ magnitude - 1} else {}) \<inter> obj_range y koa = {}\<rbrakk> \<Longrightarrow> 6 \<le> magnitude proof (prove)
goal (1 subgoal):
 1. \<And>ko p y koa P. \<lbrakk>y \<in> {base..base + 2 ^ magnitude - 1}; valid_pspace s; pspace_relation (kheap s) (ksPSpace s'); ekheap_relation (ekheap s) (ksPSpace s'); sched_act_relation (scheduler_action s) (ksSchedulerAction s'); ready_queues_relation (ready_queues s) (ksReadyQueues s'); ghost_relation (kheap s) (gsUserPages s') (gsCNodes s'); cdt_relation (swp (cte_wp_at (\<lambda>_. True)) s) (cdt s) (ctes_of s'); cdt_list_relation (cdt_list s) (cdt s) (ctes_of s'); revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) (ctes_of s'); (arch_state s, ksArchState s') \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState s'); cur_thread s = ksCurThread s'; idle_thread s = ksIdleThread s'; machine_state s = ksMachineState s'; work_units_completed s = ksWorkUnitsCompleted s'; domain_index s = ksDomScheduleIdx s'; domain_list s = ksDomSchedule s'; cur_domain s = ksCurDomain s'; domain_time s = ksDomainTime s'; kheap s y = Some koa; (p, P) \<in> obj_relation_cuts koa y; P koa (KOArch ko); p \<in> {base..base + 2 ^ magnitude - 1}; obj_range y koa \<subseteq> {base..base + 2 ^ magnitude - 1} \<and> (if idx < 2 ^ magnitude then {base + word_of_nat idx..base + 2 ^ magnitude - 1} else {}) \<inter> obj_range y koa = {}\<rbrakk> \<Longrightarrow> 6 \<le> magnitude proof (prove)
goal (1 subgoal):
 1. \<And>ko p y koa P. \<lbrakk>y \<in> {base..base + 2 ^ magnitude - 1}; valid_pspace s; pspace_relation (kheap s) (ksPSpace s'); ekheap_relation (ekheap s) (ksPSpace s'); sched_act_relation (scheduler_action s) (ksSchedulerAction s'); ready_queues_relation (ready_queues s) (ksReadyQueues s'); ghost_relation (kheap s) (gsUserPages s') (gsCNodes s'); cdt_relation (swp (cte_wp_at (\<lambda>_. True)) s) (cdt s) (ctes_of s'); cdt_list_relation (cdt_list s) (cdt s) (ctes_of s'); revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) (ctes_of s'); (arch_state s, ksArchState s') \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState s'); cur_thread s = ksCurThread s'; idle_thread s = ksIdleThread s'; machine_state s = ksMachineState s'; work_units_completed s = ksWorkUnitsCompleted s'; domain_index s = ksDomScheduleIdx s'; domain_list s = ksDomSchedule s'; cur_domain s = ksCurDomain s'; domain_time s = ksDomainTime s'; kheap s y = Some koa; (p, P) \<in> obj_relation_cuts koa y; P koa (KOArch ko); p \<in> {base..base + 2 ^ magnitude - 1}; obj_range y koa \<subseteq> {base..base + 2 ^ magnitude - 1}; (if idx < 2 ^ magnitude then {base + word_of_nat idx..base + 2 ^ magnitude - 1} else {}) \<inter> obj_range y koa = {}\<rbrakk> \<Longrightarrow> 6 \<le> magnitude proof (prove)
goal (2 subgoals):
 1. \<And>ko p y koa P. \<lbrakk>y \<in> {base..base + 2 ^ magnitude - 1}; valid_pspace s; pspace_relation (kheap s) (ksPSpace s'); ekheap_relation (ekheap s) (ksPSpace s'); sched_act_relation (scheduler_action s) (ksSchedulerAction s'); ready_queues_relation (ready_queues s) (ksReadyQueues s'); ghost_relation (kheap s) (gsUserPages s') (gsCNodes s'); cdt_relation (swp (cte_wp_at (\<lambda>_. True)) s) (cdt s) (ctes_of s'); cdt_list_relation (cdt_list s) (cdt s) (ctes_of s'); revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) (ctes_of s'); (arch_state s, ksArchState s') \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState s'); cur_thread s = ksCurThread s'; idle_thread s = ksIdleThread s'; machine_state s = ksMachineState s'; work_units_completed s = ksWorkUnitsCompleted s'; domain_index s = ksDomScheduleIdx s'; domain_list s = ksDomSchedule s'; cur_domain s = ksCurDomain s'; domain_time s = ksDomainTime s'; kheap s y = Some koa; (p, P) \<in> obj_relation_cuts koa y; P koa (KOArch ko); p \<in> {base..base + 2 ^ magnitude - 1}; (if idx < 2 ^ magnitude then {base + word_of_nat idx..base + 2 ^ magnitude - 1} else {}) \<inter> obj_range y koa = {}\<rbrakk> \<Longrightarrow> finite {base..base + 2 ^ magnitude - 1}
 2. \<And>ko p y koa P. \<lbrakk>y \<in> {base..base + 2 ^ magnitude - 1}; valid_pspace s; pspace_relation (kheap s) (ksPSpace s'); ekheap_relation (ekheap s) (ksPSpace s'); sched_act_relation (scheduler_action s) (ksSchedulerAction s'); ready_queues_relation (ready_queues s) (ksReadyQueues s'); ghost_relation (kheap s) (gsUserPages s') (gsCNodes s'); cdt_relation (swp (cte_wp_at (\<lambda>_. True)) s) (cdt s) (ctes_of s'); cdt_list_relation (cdt_list s) (cdt s) (ctes_of s'); revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) (ctes_of s'); (arch_state s, ksArchState s') \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState s'); cur_thread s = ksCurThread s'; idle_thread s = ksIdleThread s'; machine_state s = ksMachineState s'; work_units_completed s = ksWorkUnitsCompleted s'; domain_index s = ksDomScheduleIdx s'; domain_list s = ksDomSchedule s'; cur_domain s = ksCurDomain s'; domain_time s = ksDomainTime s'; kheap s y = Some koa; (p, P) \<in> obj_relation_cuts koa y; P koa (KOArch ko); p \<in> {base..base + 2 ^ magnitude - 1}; (if idx < 2 ^ magnitude then {base + word_of_nat idx..base + 2 ^ magnitude - 1} else {}) \<inter> obj_range y koa = {}; card (obj_range y koa) \<le> card {base..base + 2 ^ magnitude - 1}\<rbrakk> \<Longrightarrow> 6 \<le> magnitude proof (prove)
goal (1 subgoal):
 1. \<And>ko p y koa P. \<lbrakk>y \<in> {base..base + 2 ^ magnitude - 1}; valid_pspace s; pspace_relation (kheap s) (ksPSpace s'); ekheap_relation (ekheap s) (ksPSpace s'); sched_act_relation (scheduler_action s) (ksSchedulerAction s'); ready_queues_relation (ready_queues s) (ksReadyQueues s'); ghost_relation (kheap s) (gsUserPages s') (gsCNodes s'); cdt_relation (swp (cte_wp_at (\<lambda>_. True)) s) (cdt s) (ctes_of s'); cdt_list_relation (cdt_list s) (cdt s) (ctes_of s'); revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) (ctes_of s'); (arch_state s, ksArchState s') \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState s'); cur_thread s = ksCurThread s'; idle_thread s = ksIdleThread s'; machine_state s = ksMachineState s'; work_units_completed s = ksWorkUnitsCompleted s'; domain_index s = ksDomScheduleIdx s'; domain_list s = ksDomSchedule s'; cur_domain s = ksCurDomain s'; domain_time s = ksDomainTime s'; kheap s y = Some koa; (p, P) \<in> obj_relation_cuts koa y; P koa (KOArch ko); p \<in> {base..base + 2 ^ magnitude - 1}; (if idx < 2 ^ magnitude then {base + word_of_nat idx..base + 2 ^ magnitude - 1} else {}) \<inter> obj_range y koa = {}; card (obj_range y koa) \<le> card {base..base + 2 ^ magnitude - 1}\<rbrakk> \<Longrightarrow> 6 \<le> magnitude proof (prove)
goal (1 subgoal):
 1. \<And>ko p y koa P. \<lbrakk>y \<in> {base..base + (2 ^ magnitude - 1)}; pspace_relation (kheap s) (ksPSpace s'); ekheap_relation (ekheap s) (ksPSpace s'); sched_act_relation (scheduler_action s) (ksSchedulerAction s'); ready_queues_relation (ready_queues s) (ksReadyQueues s'); ghost_relation (kheap s) (gsUserPages s') (gsCNodes s'); cdt_relation (swp (cte_wp_at (\<lambda>_. True)) s) (cdt s) (ctes_of s'); cdt_list_relation (cdt_list s) (cdt s) (ctes_of s'); revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) (ctes_of s'); (arch_state s, ksArchState s') \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState s'); cur_thread s = ksCurThread s'; idle_thread s = ksIdleThread s'; machine_state s = ksMachineState s'; work_units_completed s = ksWorkUnitsCompleted s'; domain_index s = ksDomScheduleIdx s'; domain_list s = ksDomSchedule s'; cur_domain s = ksCurDomain s'; domain_time s = ksDomainTime s'; kheap s y = Some koa; (p, P) \<in> obj_relation_cuts koa y; P koa (KOArch ko); p \<in> {base..base + (2 ^ magnitude - 1)}; (if idx < 2 ^ magnitude then {base + word_of_nat idx..base + 2 ^ magnitude - 1} else {}) \<inter> {y..y + (2 ^ obj_bits koa - 1)} = {}; card {y..y + (2 ^ obj_bits koa - 1)} \<le> card {base..base + (2 ^ magnitude - 1)}; valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s)\<rbrakk> \<Longrightarrow> 6 \<le> magnitude proof (prove)
goal (2 subgoals):
 1. \<And>ko p y koa P. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); y \<in> {base..base + (2 ^ magnitude - 1)}; pspace_relation (kheap s) (ksPSpace s'); ekheap_relation (ekheap s) (ksPSpace s'); sched_act_relation (scheduler_action s) (ksSchedulerAction s'); ready_queues_relation (ready_queues s) (ksReadyQueues s'); ghost_relation (kheap s) (gsUserPages s') (gsCNodes s'); cdt_relation (swp (cte_wp_at (\<lambda>_. True)) s) (cdt s) (ctes_of s'); cdt_list_relation (cdt_list s) (cdt s) (ctes_of s'); revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) (ctes_of s'); (arch_state s, ksArchState s') \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState s'); cur_thread s = ksCurThread s'; idle_thread s = ksIdleThread s'; machine_state s = ksMachineState s'; work_units_completed s = ksWorkUnitsCompleted s'; domain_index s = ksDomScheduleIdx s'; domain_list s = ksDomSchedule s'; cur_domain s = ksCurDomain s'; domain_time s = ksDomainTime s'; kheap s y = Some koa; (p, P) \<in> obj_relation_cuts koa y; P koa (KOArch ko); p \<in> {base..base + (2 ^ magnitude - 1)}; (if idx < 2 ^ magnitude then {base + word_of_nat idx..base + 2 ^ magnitude - 1} else {}) \<inter> {y..y + (2 ^ obj_bits koa - 1)} = {}\<rbrakk> \<Longrightarrow> y \<le> y + (2 ^ obj_bits koa - 1)
 2. \<And>ko p y koa P. \<lbrakk>y \<in> {base..base + (2 ^ magnitude - 1)}; pspace_relation (kheap s) (ksPSpace s'); ekheap_relation (ekheap s) (ksPSpace s'); sched_act_relation (scheduler_action s) (ksSchedulerAction s'); ready_queues_relation (ready_queues s) (ksReadyQueues s'); ghost_relation (kheap s) (gsUserPages s') (gsCNodes s'); cdt_relation (swp (cte_wp_at (\<lambda>_. True)) s) (cdt s) (ctes_of s'); cdt_list_relation (cdt_list s) (cdt s) (ctes_of s'); revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) (ctes_of s'); (arch_state s, ksArchState s') \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState s'); cur_thread s = ksCurThread s'; idle_thread s = ksIdleThread s'; machine_state s = ksMachineState s'; work_units_completed s = ksWorkUnitsCompleted s'; domain_index s = ksDomScheduleIdx s'; domain_list s = ksDomSchedule s'; cur_domain s = ksCurDomain s'; domain_time s = ksDomainTime s'; kheap s y = Some koa; (p, P) \<in> obj_relation_cuts koa y; P koa (KOArch ko); p \<in> {base..base + (2 ^ magnitude - 1)}; (if idx < 2 ^ magnitude then {base + word_of_nat idx..base + 2 ^ magnitude - 1} else {}) \<inter> {y..y + (2 ^ obj_bits koa - 1)} = {}; unat (2 ^ obj_bits koa - 1) + 1 \<le> card {base..base + (2 ^ magnitude - 1)}; valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s)\<rbrakk> \<Longrightarrow> 6 \<le> magnitude proof (prove)
goal (2 subgoals):
 1. \<And>ko p y koa P. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); y \<in> {base..base + (2 ^ magnitude - 1)}; pspace_relation (kheap s) (ksPSpace s'); ekheap_relation (ekheap s) (ksPSpace s'); sched_act_relation (scheduler_action s) (ksSchedulerAction s'); ready_queues_relation (ready_queues s) (ksReadyQueues s'); ghost_relation (kheap s) (gsUserPages s') (gsCNodes s'); cdt_relation (swp (cte_wp_at (\<lambda>_. True)) s) (cdt s) (ctes_of s'); cdt_list_relation (cdt_list s) (cdt s) (ctes_of s'); revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) (ctes_of s'); (arch_state s, ksArchState s') \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState s'); cur_thread s = ksCurThread s'; idle_thread s = ksIdleThread s'; machine_state s = ksMachineState s'; work_units_completed s = ksWorkUnitsCompleted s'; domain_index s = ksDomScheduleIdx s'; domain_list s = ksDomSchedule s'; cur_domain s = ksCurDomain s'; domain_time s = ksDomainTime s'; kheap s y = Some koa; (p, P) \<in> obj_relation_cuts koa y; P koa (KOArch ko); p \<in> {base..base + (2 ^ magnitude - 1)}; (if idx < 2 ^ magnitude then {base + word_of_nat idx..base + 2 ^ magnitude - 1} else {}) \<inter> {y..y + (2 ^ obj_bits koa - 1)} = {}\<rbrakk> \<Longrightarrow> is_aligned y (obj_bits koa)
 2. \<And>ko p y koa P. \<lbrakk>y \<in> {base..base + (2 ^ magnitude - 1)}; pspace_relation (kheap s) (ksPSpace s'); ekheap_relation (ekheap s) (ksPSpace s'); sched_act_relation (scheduler_action s) (ksSchedulerAction s'); ready_queues_relation (ready_queues s) (ksReadyQueues s'); ghost_relation (kheap s) (gsUserPages s') (gsCNodes s'); cdt_relation (swp (cte_wp_at (\<lambda>_. True)) s) (cdt s) (ctes_of s'); cdt_list_relation (cdt_list s) (cdt s) (ctes_of s'); revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) (ctes_of s'); (arch_state s, ksArchState s') \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState s'); cur_thread s = ksCurThread s'; idle_thread s = ksIdleThread s'; machine_state s = ksMachineState s'; work_units_completed s = ksWorkUnitsCompleted s'; domain_index s = ksDomScheduleIdx s'; domain_list s = ksDomSchedule s'; cur_domain s = ksCurDomain s'; domain_time s = ksDomainTime s'; kheap s y = Some koa; (p, P) \<in> obj_relation_cuts koa y; P koa (KOArch ko); p \<in> {base..base + (2 ^ magnitude - 1)}; (if idx < 2 ^ magnitude then {base + word_of_nat idx..base + 2 ^ magnitude - 1} else {}) \<inter> {y..y + (2 ^ obj_bits koa - 1)} = {}; unat (2 ^ obj_bits koa - 1) + 1 \<le> card {base..base + (2 ^ magnitude - 1)}; valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s)\<rbrakk> \<Longrightarrow> 6 \<le> magnitude proof (prove)
goal (1 subgoal):
 1. \<And>ko p y koa P. \<lbrakk>y \<in> {base..base + (2 ^ magnitude - 1)}; pspace_relation (kheap s) (ksPSpace s'); ekheap_relation (ekheap s) (ksPSpace s'); sched_act_relation (scheduler_action s) (ksSchedulerAction s'); ready_queues_relation (ready_queues s) (ksReadyQueues s'); ghost_relation (kheap s) (gsUserPages s') (gsCNodes s'); cdt_relation (swp (cte_wp_at (\<lambda>_. True)) s) (cdt s) (ctes_of s'); cdt_list_relation (cdt_list s) (cdt s) (ctes_of s'); revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) (ctes_of s'); (arch_state s, ksArchState s') \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState s'); cur_thread s = ksCurThread s'; idle_thread s = ksIdleThread s'; machine_state s = ksMachineState s'; work_units_completed s = ksWorkUnitsCompleted s'; domain_index s = ksDomScheduleIdx s'; domain_list s = ksDomSchedule s'; cur_domain s = ksCurDomain s'; domain_time s = ksDomainTime s'; kheap s y = Some koa; (p, P) \<in> obj_relation_cuts koa y; P koa (KOArch ko); p \<in> {base..base + (2 ^ magnitude - 1)}; (if idx < 2 ^ magnitude then {base + word_of_nat idx..base + 2 ^ magnitude - 1} else {}) \<inter> {y..y + (2 ^ obj_bits koa - 1)} = {}; unat (2 ^ obj_bits koa - 1) + 1 \<le> card {base..base + (2 ^ magnitude - 1)}; valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s)\<rbrakk> \<Longrightarrow> 6 \<le> magnitude proof (prove)
goal (2 subgoals):
 1. \<And>ko p y koa P. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); y \<in> {base..base + (2 ^ magnitude - 1)}; pspace_relation (kheap s) (ksPSpace s'); ekheap_relation (ekheap s) (ksPSpace s'); sched_act_relation (scheduler_action s) (ksSchedulerAction s'); ready_queues_relation (ready_queues s) (ksReadyQueues s'); ghost_relation (kheap s) (gsUserPages s') (gsCNodes s'); cdt_relation (swp (cte_wp_at (\<lambda>_. True)) s) (cdt s) (ctes_of s'); cdt_list_relation (cdt_list s) (cdt s) (ctes_of s'); revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) (ctes_of s'); (arch_state s, ksArchState s') \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState s'); cur_thread s = ksCurThread s'; idle_thread s = ksIdleThread s'; machine_state s = ksMachineState s'; work_units_completed s = ksWorkUnitsCompleted s'; domain_index s = ksDomScheduleIdx s'; domain_list s = ksDomSchedule s'; cur_domain s = ksCurDomain s'; domain_time s = ksDomainTime s'; kheap s y = Some koa; (p, P) \<in> obj_relation_cuts koa y; P koa (KOArch ko); p \<in> {base..base + (2 ^ magnitude - 1)}; (if idx < 2 ^ magnitude then {base + word_of_nat idx..base + 2 ^ magnitude - 1} else {}) \<inter> {y..y + (2 ^ obj_bits koa - 1)} = {}\<rbrakk> \<Longrightarrow> base \<le> base + (2 ^ magnitude - 1)
 2. \<And>ko p y koa P. \<lbrakk>y \<in> {base..base + (2 ^ magnitude - 1)}; pspace_relation (kheap s) (ksPSpace s'); ekheap_relation (ekheap s) (ksPSpace s'); sched_act_relation (scheduler_action s) (ksSchedulerAction s'); ready_queues_relation (ready_queues s) (ksReadyQueues s'); ghost_relation (kheap s) (gsUserPages s') (gsCNodes s'); cdt_relation (swp (cte_wp_at (\<lambda>_. True)) s) (cdt s) (ctes_of s'); cdt_list_relation (cdt_list s) (cdt s) (ctes_of s'); revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) (ctes_of s'); (arch_state s, ksArchState s') \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState s'); cur_thread s = ksCurThread s'; idle_thread s = ksIdleThread s'; machine_state s = ksMachineState s'; work_units_completed s = ksWorkUnitsCompleted s'; domain_index s = ksDomScheduleIdx s'; domain_list s = ksDomSchedule s'; cur_domain s = ksCurDomain s'; domain_time s = ksDomainTime s'; kheap s y = Some koa; (p, P) \<in> obj_relation_cuts koa y; P koa (KOArch ko); p \<in> {base..base + (2 ^ magnitude - 1)}; (if idx < 2 ^ magnitude then {base + word_of_nat idx..base + 2 ^ magnitude - 1} else {}) \<inter> {y..y + (2 ^ obj_bits koa - 1)} = {}; unat (2 ^ obj_bits koa - 1) + 1 \<le> unat (2 ^ magnitude - 1) + 1; valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s)\<rbrakk> \<Longrightarrow> 6 \<le> magnitude proof (prove)
goal (1 subgoal):
 1. \<And>ko p y koa P. \<lbrakk>y \<in> {base..base + (2 ^ magnitude - 1)}; pspace_relation (kheap s) (ksPSpace s'); ekheap_relation (ekheap s) (ksPSpace s'); sched_act_relation (scheduler_action s) (ksSchedulerAction s'); ready_queues_relation (ready_queues s) (ksReadyQueues s'); ghost_relation (kheap s) (gsUserPages s') (gsCNodes s'); cdt_relation (swp (cte_wp_at (\<lambda>_. True)) s) (cdt s) (ctes_of s'); cdt_list_relation (cdt_list s) (cdt s) (ctes_of s'); revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) (ctes_of s'); (arch_state s, ksArchState s') \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState s'); cur_thread s = ksCurThread s'; idle_thread s = ksIdleThread s'; machine_state s = ksMachineState s'; work_units_completed s = ksWorkUnitsCompleted s'; domain_index s = ksDomScheduleIdx s'; domain_list s = ksDomSchedule s'; cur_domain s = ksCurDomain s'; domain_time s = ksDomainTime s'; kheap s y = Some koa; (p, P) \<in> obj_relation_cuts koa y; P koa (KOArch ko); p \<in> {base..base + (2 ^ magnitude - 1)}; (if idx < 2 ^ magnitude then {base + word_of_nat idx..base + 2 ^ magnitude - 1} else {}) \<inter> {y..y + (2 ^ obj_bits koa - 1)} = {}; unat (2 ^ obj_bits koa - 1) + 1 \<le> unat (2 ^ magnitude - 1) + 1; valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s)\<rbrakk> \<Longrightarrow> 6 \<le> magnitude proof (prove)
goal (1 subgoal):
 1. \<And>ko p y koa P. \<lbrakk>y \<in> {base..base + (2 ^ magnitude - 1)}; pspace_relation (kheap s) (ksPSpace s'); ekheap_relation (ekheap s) (ksPSpace s'); sched_act_relation (scheduler_action s) (ksSchedulerAction s'); ready_queues_relation (ready_queues s) (ksReadyQueues s'); ghost_relation (kheap s) (gsUserPages s') (gsCNodes s'); cdt_relation (swp (cte_wp_at (\<lambda>_. True)) s) (cdt s) (ctes_of s'); cdt_list_relation (cdt_list s) (cdt s) (ctes_of s'); revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) (ctes_of s'); (arch_state s, ksArchState s') \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState s'); cur_thread s = ksCurThread s'; idle_thread s = ksIdleThread s'; machine_state s = ksMachineState s'; work_units_completed s = ksWorkUnitsCompleted s'; domain_index s = ksDomScheduleIdx s'; domain_list s = ksDomSchedule s'; cur_domain s = ksCurDomain s'; domain_time s = ksDomainTime s'; kheap s y = Some koa; (p, P) \<in> obj_relation_cuts koa y; P koa (KOArch ko); p \<in> {base..base + (2 ^ magnitude - 1)}; (if idx < 2 ^ magnitude then {base + word_of_nat idx..base + 2 ^ magnitude - 1} else {}) \<inter> {y..y + (2 ^ obj_bits koa - 1)} = {}; unat (2 ^ obj_bits koa - 1) + 1 \<le> unat (2 ^ magnitude - 1) + 1; valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); \<not> 6 \<le> magnitude\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>ko p y koa P. \<lbrakk>y \<in> {base..base + (2 ^ magnitude - 1)}; pspace_relation (kheap s) (ksPSpace s'); ekheap_relation (ekheap s) (ksPSpace s'); sched_act_relation (scheduler_action s) (ksSchedulerAction s'); ready_queues_relation (ready_queues s) (ksReadyQueues s'); ghost_relation (kheap s) (gsUserPages s') (gsCNodes s'); cdt_relation (swp (cte_wp_at (\<lambda>_. True)) s) (cdt s) (ctes_of s'); cdt_list_relation (cdt_list s) (cdt s) (ctes_of s'); revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) (ctes_of s'); (arch_state s, ksArchState s') \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState s'); cur_thread s = ksCurThread s'; idle_thread s = ksIdleThread s'; machine_state s = ksMachineState s'; work_units_completed s = ksWorkUnitsCompleted s'; domain_index s = ksDomScheduleIdx s'; domain_list s = ksDomSchedule s'; cur_domain s = ksCurDomain s'; domain_time s = ksDomainTime s'; kheap s y = Some koa; (p, P) \<in> obj_relation_cuts koa y; P koa (KOArch ko); p \<in> {base..base + (2 ^ magnitude - 1)}; (if idx < 2 ^ magnitude then {base + word_of_nat idx..base + 2 ^ magnitude - 1} else {}) \<inter> {y..y + (2 ^ obj_bits koa - 1)} = {}; Suc (unat (2 ^ obj_bits koa - 1)) \<le> 2 ^ magnitude; valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); magnitude < 6\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>ko p y koa P. \<lbrakk>y \<in> {base..base + (2 ^ magnitude - 1)}; pspace_relation (kheap s) (ksPSpace s'); ekheap_relation (ekheap s) (ksPSpace s'); sched_act_relation (scheduler_action s) (ksSchedulerAction s'); ready_queues_relation (ready_queues s) (ksReadyQueues s'); ghost_relation (kheap s) (gsUserPages s') (gsCNodes s'); cdt_relation (swp (cte_wp_at (\<lambda>_. True)) s) (cdt s) (ctes_of s'); cdt_list_relation (cdt_list s) (cdt s) (ctes_of s'); revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) (ctes_of s'); (arch_state s, ksArchState s') \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState s'); cur_thread s = ksCurThread s'; idle_thread s = ksIdleThread s'; machine_state s = ksMachineState s'; work_units_completed s = ksWorkUnitsCompleted s'; domain_index s = ksDomScheduleIdx s'; domain_list s = ksDomSchedule s'; cur_domain s = ksCurDomain s'; domain_time s = ksDomainTime s'; kheap s y = Some koa; (p, P) \<in> obj_relation_cuts koa y; P koa (KOArch ko); p \<in> {base..base + (2 ^ magnitude - 1)}; (if idx < 2 ^ magnitude then {base + word_of_nat idx..base + 2 ^ magnitude - 1} else {}) \<inter> {y..y + (2 ^ obj_bits koa - 1)} = {}; Suc (unat (2 ^ obj_bits koa - 1)) \<le> 2 ^ magnitude; valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); magnitude < 6; obj_bits koa < 32\<rbrakk> \<Longrightarrow> False
 2. \<And>ko p y koa P. \<lbrakk>y \<in> {base..base + (2 ^ magnitude - 1)}; pspace_relation (kheap s) (ksPSpace s'); ekheap_relation (ekheap s) (ksPSpace s'); sched_act_relation (scheduler_action s) (ksSchedulerAction s'); ready_queues_relation (ready_queues s) (ksReadyQueues s'); ghost_relation (kheap s) (gsUserPages s') (gsCNodes s'); cdt_relation (swp (cte_wp_at (\<lambda>_. True)) s) (cdt s) (ctes_of s'); cdt_list_relation (cdt_list s) (cdt s) (ctes_of s'); revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) (ctes_of s'); (arch_state s, ksArchState s') \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState s'); cur_thread s = ksCurThread s'; idle_thread s = ksIdleThread s'; machine_state s = ksMachineState s'; work_units_completed s = ksWorkUnitsCompleted s'; domain_index s = ksDomScheduleIdx s'; domain_list s = ksDomSchedule s'; cur_domain s = ksCurDomain s'; domain_time s = ksDomainTime s'; kheap s y = Some koa; (p, P) \<in> obj_relation_cuts koa y; P koa (KOArch ko); p \<in> {base..base + (2 ^ magnitude - 1)}; (if idx < 2 ^ magnitude then {base + word_of_nat idx..base + 2 ^ magnitude - 1} else {}) \<inter> {y..y + (2 ^ obj_bits koa - 1)} = {}; Suc (unat (2 ^ obj_bits koa - 1)) \<le> 2 ^ magnitude; valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); magnitude < 6\<rbrakk> \<Longrightarrow> obj_bits koa < 32 proof (prove)
goal (2 subgoals):
 1. \<And>ko p y koa P. \<lbrakk>y \<in> {base..base + (2 ^ magnitude - 1)}; pspace_relation (kheap s) (ksPSpace s'); ekheap_relation (ekheap s) (ksPSpace s'); sched_act_relation (scheduler_action s) (ksSchedulerAction s'); ready_queues_relation (ready_queues s) (ksReadyQueues s'); ghost_relation (kheap s) (gsUserPages s') (gsCNodes s'); cdt_relation (swp (cte_wp_at (\<lambda>_. True)) s) (cdt s) (ctes_of s'); cdt_list_relation (cdt_list s) (cdt s) (ctes_of s'); revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) (ctes_of s'); (arch_state s, ksArchState s') \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState s'); cur_thread s = ksCurThread s'; idle_thread s = ksIdleThread s'; machine_state s = ksMachineState s'; work_units_completed s = ksWorkUnitsCompleted s'; domain_index s = ksDomScheduleIdx s'; domain_list s = ksDomSchedule s'; cur_domain s = ksCurDomain s'; domain_time s = ksDomainTime s'; kheap s y = Some koa; (p, P) \<in> obj_relation_cuts koa y; P koa (KOArch ko); p \<in> {base..base + (2 ^ magnitude - 1)}; (if idx < 2 ^ magnitude then {base + word_of_nat idx..base + 2 ^ magnitude - 1} else {}) \<inter> {y..y + (2 ^ obj_bits koa - 1)} = {}; Suc (unat (2 ^ obj_bits koa - 1)) \<le> 2 ^ magnitude; valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); magnitude < 6\<rbrakk> \<Longrightarrow> obj_bits koa < 32
 2. \<And>ko p y koa P. \<lbrakk>y \<in> {base..base + (2 ^ magnitude - 1)}; pspace_relation (kheap s) (ksPSpace s'); ekheap_relation (ekheap s) (ksPSpace s'); sched_act_relation (scheduler_action s) (ksSchedulerAction s'); ready_queues_relation (ready_queues s) (ksReadyQueues s'); ghost_relation (kheap s) (gsUserPages s') (gsCNodes s'); cdt_relation (swp (cte_wp_at (\<lambda>_. True)) s) (cdt s) (ctes_of s'); cdt_list_relation (cdt_list s) (cdt s) (ctes_of s'); revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) (ctes_of s'); (arch_state s, ksArchState s') \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState s'); cur_thread s = ksCurThread s'; idle_thread s = ksIdleThread s'; machine_state s = ksMachineState s'; work_units_completed s = ksWorkUnitsCompleted s'; domain_index s = ksDomScheduleIdx s'; domain_list s = ksDomSchedule s'; cur_domain s = ksCurDomain s'; domain_time s = ksDomainTime s'; kheap s y = Some koa; (p, P) \<in> obj_relation_cuts koa y; P koa (KOArch ko); p \<in> {base..base + (2 ^ magnitude - 1)}; (if idx < 2 ^ magnitude then {base + word_of_nat idx..base + 2 ^ magnitude - 1} else {}) \<inter> {y..y + (2 ^ obj_bits koa - 1)} = {}; Suc (unat (2 ^ obj_bits koa - 1)) \<le> 2 ^ magnitude; valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); magnitude < 6; obj_bits koa < 32\<rbrakk> \<Longrightarrow> False proof (prove)
goal (3 subgoals):
 1. \<And>ko p y koa P x11 x12. \<lbrakk>y \<in> {base..base + (2 ^ magnitude - 1)}; pspace_relation (kheap s) (ksPSpace s'); ekheap_relation (ekheap s) (ksPSpace s'); sched_act_relation (scheduler_action s) (ksSchedulerAction s'); ready_queues_relation (ready_queues s) (ksReadyQueues s'); ghost_relation (kheap s) (gsUserPages s') (gsCNodes s'); cdt_relation (swp (cte_wp_at (\<lambda>_. True)) s) (cdt s) (ctes_of s'); cdt_list_relation (cdt_list s) (cdt s) (ctes_of s'); revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) (ctes_of s'); (arch_state s, ksArchState s') \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState s'); cur_thread s = ksCurThread s'; idle_thread s = ksIdleThread s'; machine_state s = ksMachineState s'; work_units_completed s = ksWorkUnitsCompleted s'; domain_index s = ksDomScheduleIdx s'; domain_list s = ksDomSchedule s'; cur_domain s = ksCurDomain s'; domain_time s = ksDomainTime s'; kheap s y = Some (CNode x11 x12); (p, P) \<in> (if well_formed_cnode_n x11 x12 then {(cte_map (y, ya), cte_relation ya) |ya. ya \<in> dom x12} else {(y, \<lambda>_ _. False)}); P (CNode x11 x12) (KOArch ko); p \<in> {base..base + (2 ^ magnitude - 1)}; (if idx < 2 ^ magnitude then {base + word_of_nat idx..base + 2 ^ magnitude - 1} else {}) \<inter> {y..y + (2 ^ (cte_level_bits + x11) - 1)} = {}; Suc (unat (2 ^ (cte_level_bits + x11) - 1)) \<le> 2 ^ magnitude; valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); magnitude < 6; koa = CNode x11 x12\<rbrakk> \<Longrightarrow> cte_level_bits + x11 < 32
 2. \<And>ko p y koa P x5. \<lbrakk>y \<in> {base..base + (2 ^ magnitude - 1)}; pspace_relation (kheap s) (ksPSpace s'); ekheap_relation (ekheap s) (ksPSpace s'); sched_act_relation (scheduler_action s) (ksSchedulerAction s'); ready_queues_relation (ready_queues s) (ksReadyQueues s'); ghost_relation (kheap s) (gsUserPages s') (gsCNodes s'); cdt_relation (swp (cte_wp_at (\<lambda>_. True)) s) (cdt s) (ctes_of s'); cdt_list_relation (cdt_list s) (cdt s) (ctes_of s'); revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) (ctes_of s'); (arch_state s, ksArchState s') \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState s'); cur_thread s = ksCurThread s'; idle_thread s = ksIdleThread s'; machine_state s = ksMachineState s'; work_units_completed s = ksWorkUnitsCompleted s'; domain_index s = ksDomScheduleIdx s'; domain_list s = ksDomSchedule s'; cur_domain s = ksCurDomain s'; domain_time s = ksDomainTime s'; kheap s y = Some (ArchObj x5); (p, P) \<in> aobj_relation_cuts x5 y; P (ArchObj x5) (KOArch ko); p \<in> {base..base + (2 ^ magnitude - 1)}; (if idx < 2 ^ magnitude then {base + word_of_nat idx..base + 2 ^ magnitude - 1} else {}) \<inter> {y..y + (2 ^ arch_kobj_size x5 - 1)} = {}; Suc (unat (2 ^ arch_kobj_size x5 - 1)) \<le> 2 ^ magnitude; valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); magnitude < 6; koa = ArchObj x5\<rbrakk> \<Longrightarrow> arch_kobj_size x5 < 32
 3. \<And>ko p y koa P. \<lbrakk>y \<in> {base..base + (2 ^ magnitude - 1)}; pspace_relation (kheap s) (ksPSpace s'); ekheap_relation (ekheap s) (ksPSpace s'); sched_act_relation (scheduler_action s) (ksSchedulerAction s'); ready_queues_relation (ready_queues s) (ksReadyQueues s'); ghost_relation (kheap s) (gsUserPages s') (gsCNodes s'); cdt_relation (swp (cte_wp_at (\<lambda>_. True)) s) (cdt s) (ctes_of s'); cdt_list_relation (cdt_list s) (cdt s) (ctes_of s'); revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) (ctes_of s'); (arch_state s, ksArchState s') \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState s'); cur_thread s = ksCurThread s'; idle_thread s = ksIdleThread s'; machine_state s = ksMachineState s'; work_units_completed s = ksWorkUnitsCompleted s'; domain_index s = ksDomScheduleIdx s'; domain_list s = ksDomSchedule s'; cur_domain s = ksCurDomain s'; domain_time s = ksDomainTime s'; kheap s y = Some koa; (p, P) \<in> obj_relation_cuts koa y; P koa (KOArch ko); p \<in> {base..base + (2 ^ magnitude - 1)}; (if idx < 2 ^ magnitude then {base + word_of_nat idx..base + 2 ^ magnitude - 1} else {}) \<inter> {y..y + (2 ^ obj_bits koa - 1)} = {}; obj_bits koa \<le> magnitude; valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); magnitude < 6\<rbrakk> \<Longrightarrow> False proof (prove)
goal (3 subgoals):
 1. \<And>ko p y koa P x11 x12. \<lbrakk>y \<in> {base..base + (2 ^ magnitude - 1)}; pspace_relation (kheap s) (ksPSpace s'); ekheap_relation (ekheap s) (ksPSpace s'); sched_act_relation (scheduler_action s) (ksSchedulerAction s'); ready_queues_relation (ready_queues s) (ksReadyQueues s'); ghost_relation (kheap s) (gsUserPages s') (gsCNodes s'); cdt_relation (swp (cte_wp_at (\<lambda>_. True)) s) (cdt s) (ctes_of s'); cdt_list_relation (cdt_list s) (cdt s) (ctes_of s'); revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) (ctes_of s'); (arch_state s, ksArchState s') \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState s'); cur_thread s = ksCurThread s'; idle_thread s = ksIdleThread s'; machine_state s = ksMachineState s'; work_units_completed s = ksWorkUnitsCompleted s'; domain_index s = ksDomScheduleIdx s'; domain_list s = ksDomSchedule s'; cur_domain s = ksCurDomain s'; domain_time s = ksDomainTime s'; kheap s y = Some (CNode x11 x12); (p, P) \<in> (if well_formed_cnode_n x11 x12 then {(cte_map (y, ya), cte_relation ya) |ya. ya \<in> dom x12} else {(y, \<lambda>_ _. False)}); P (CNode x11 x12) (KOArch ko); p \<in> {base..base + (2 ^ magnitude - 1)}; (if idx < 2 ^ magnitude then {base + word_of_nat idx..base + 2 ^ magnitude - 1} else {}) \<inter> {y..y + (2 ^ (cte_level_bits + x11) - 1)} = {}; Suc (unat (2 ^ (cte_level_bits + x11) - 1)) \<le> 2 ^ magnitude; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); magnitude < 6; koa = CNode x11 x12; valid_cs_size x11 x12\<rbrakk> \<Longrightarrow> cte_level_bits + x11 < 32
 2. \<And>ko p y koa P x5. \<lbrakk>y \<in> {base..base + (2 ^ magnitude - 1)}; pspace_relation (kheap s) (ksPSpace s'); ekheap_relation (ekheap s) (ksPSpace s'); sched_act_relation (scheduler_action s) (ksSchedulerAction s'); ready_queues_relation (ready_queues s) (ksReadyQueues s'); ghost_relation (kheap s) (gsUserPages s') (gsCNodes s'); cdt_relation (swp (cte_wp_at (\<lambda>_. True)) s) (cdt s) (ctes_of s'); cdt_list_relation (cdt_list s) (cdt s) (ctes_of s'); revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) (ctes_of s'); (arch_state s, ksArchState s') \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState s'); cur_thread s = ksCurThread s'; idle_thread s = ksIdleThread s'; machine_state s = ksMachineState s'; work_units_completed s = ksWorkUnitsCompleted s'; domain_index s = ksDomScheduleIdx s'; domain_list s = ksDomSchedule s'; cur_domain s = ksCurDomain s'; domain_time s = ksDomainTime s'; kheap s y = Some (ArchObj x5); (p, P) \<in> aobj_relation_cuts x5 y; P (ArchObj x5) (KOArch ko); p \<in> {base..base + (2 ^ magnitude - 1)}; (if idx < 2 ^ magnitude then {base + word_of_nat idx..base + 2 ^ magnitude - 1} else {}) \<inter> {y..y + (2 ^ arch_kobj_size x5 - 1)} = {}; Suc (unat (2 ^ arch_kobj_size x5 - 1)) \<le> 2 ^ magnitude; valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); magnitude < 6; koa = ArchObj x5\<rbrakk> \<Longrightarrow> arch_kobj_size x5 < 32
 3. \<And>ko p y koa P. \<lbrakk>y \<in> {base..base + (2 ^ magnitude - 1)}; pspace_relation (kheap s) (ksPSpace s'); ekheap_relation (ekheap s) (ksPSpace s'); sched_act_relation (scheduler_action s) (ksSchedulerAction s'); ready_queues_relation (ready_queues s) (ksReadyQueues s'); ghost_relation (kheap s) (gsUserPages s') (gsCNodes s'); cdt_relation (swp (cte_wp_at (\<lambda>_. True)) s) (cdt s) (ctes_of s'); cdt_list_relation (cdt_list s) (cdt s) (ctes_of s'); revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) (ctes_of s'); (arch_state s, ksArchState s') \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState s'); cur_thread s = ksCurThread s'; idle_thread s = ksIdleThread s'; machine_state s = ksMachineState s'; work_units_completed s = ksWorkUnitsCompleted s'; domain_index s = ksDomScheduleIdx s'; domain_list s = ksDomSchedule s'; cur_domain s = ksCurDomain s'; domain_time s = ksDomainTime s'; kheap s y = Some koa; (p, P) \<in> obj_relation_cuts koa y; P koa (KOArch ko); p \<in> {base..base + (2 ^ magnitude - 1)}; (if idx < 2 ^ magnitude then {base + word_of_nat idx..base + 2 ^ magnitude - 1} else {}) \<inter> {y..y + (2 ^ obj_bits koa - 1)} = {}; obj_bits koa \<le> magnitude; valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); magnitude < 6\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>ko p y koa P x5. \<lbrakk>y \<in> {base..base + (2 ^ magnitude - 1)}; pspace_relation (kheap s) (ksPSpace s'); ekheap_relation (ekheap s) (ksPSpace s'); sched_act_relation (scheduler_action s) (ksSchedulerAction s'); ready_queues_relation (ready_queues s) (ksReadyQueues s'); ghost_relation (kheap s) (gsUserPages s') (gsCNodes s'); cdt_relation (swp (cte_wp_at (\<lambda>_. True)) s) (cdt s) (ctes_of s'); cdt_list_relation (cdt_list s) (cdt s) (ctes_of s'); revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) (ctes_of s'); (arch_state s, ksArchState s') \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState s'); cur_thread s = ksCurThread s'; idle_thread s = ksIdleThread s'; machine_state s = ksMachineState s'; work_units_completed s = ksWorkUnitsCompleted s'; domain_index s = ksDomScheduleIdx s'; domain_list s = ksDomSchedule s'; cur_domain s = ksCurDomain s'; domain_time s = ksDomainTime s'; kheap s y = Some (ArchObj x5); (p, P) \<in> aobj_relation_cuts x5 y; P (ArchObj x5) (KOArch ko); p \<in> {base..base + (2 ^ magnitude - 1)}; (if idx < 2 ^ magnitude then {base + word_of_nat idx..base + 2 ^ magnitude - 1} else {}) \<inter> {y..y + (2 ^ arch_kobj_size x5 - 1)} = {}; Suc (unat (2 ^ arch_kobj_size x5 - 1)) \<le> 2 ^ magnitude; valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); magnitude < 6; koa = ArchObj x5\<rbrakk> \<Longrightarrow> arch_kobj_size x5 < 32
 2. \<And>ko p y koa P. \<lbrakk>y \<in> {base..base + (2 ^ magnitude - 1)}; pspace_relation (kheap s) (ksPSpace s'); ekheap_relation (ekheap s) (ksPSpace s'); sched_act_relation (scheduler_action s) (ksSchedulerAction s'); ready_queues_relation (ready_queues s) (ksReadyQueues s'); ghost_relation (kheap s) (gsUserPages s') (gsCNodes s'); cdt_relation (swp (cte_wp_at (\<lambda>_. True)) s) (cdt s) (ctes_of s'); cdt_list_relation (cdt_list s) (cdt s) (ctes_of s'); revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) (ctes_of s'); (arch_state s, ksArchState s') \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState s'); cur_thread s = ksCurThread s'; idle_thread s = ksIdleThread s'; machine_state s = ksMachineState s'; work_units_completed s = ksWorkUnitsCompleted s'; domain_index s = ksDomScheduleIdx s'; domain_list s = ksDomSchedule s'; cur_domain s = ksCurDomain s'; domain_time s = ksDomainTime s'; kheap s y = Some koa; (p, P) \<in> obj_relation_cuts koa y; P koa (KOArch ko); p \<in> {base..base + (2 ^ magnitude - 1)}; (if idx < 2 ^ magnitude then {base + word_of_nat idx..base + 2 ^ magnitude - 1} else {}) \<inter> {y..y + (2 ^ obj_bits koa - 1)} = {}; obj_bits koa \<le> magnitude; valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); magnitude < 6\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>ko p y koa P arch_kernel_obj. \<lbrakk>y \<in> {base..base + (2 ^ magnitude - 1)}; pspace_relation (kheap s) (ksPSpace s'); ekheap_relation (ekheap s) (ksPSpace s'); sched_act_relation (scheduler_action s) (ksSchedulerAction s'); ready_queues_relation (ready_queues s) (ksReadyQueues s'); ghost_relation (kheap s) (gsUserPages s') (gsCNodes s'); cdt_relation (swp (cte_wp_at (\<lambda>_. True)) s) (cdt s) (ctes_of s'); cdt_list_relation (cdt_list s) (cdt s) (ctes_of s'); revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) (ctes_of s'); (arch_state s, ksArchState s') \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState s'); cur_thread s = ksCurThread s'; idle_thread s = ksIdleThread s'; machine_state s = ksMachineState s'; work_units_completed s = ksWorkUnitsCompleted s'; domain_index s = ksDomScheduleIdx s'; domain_list s = ksDomSchedule s'; cur_domain s = ksCurDomain s'; domain_time s = ksDomainTime s'; kheap s y = Some (ArchObj arch_kernel_obj); (p, P) \<in> aobj_relation_cuts arch_kernel_obj y; P (ArchObj arch_kernel_obj) (KOArch ko); p \<in> {base..base + (2 ^ magnitude - 1)}; (if idx < 2 ^ magnitude then {base + word_of_nat idx..base + 2 ^ magnitude - 1} else {}) \<inter> {y..y + (2 ^ arch_kobj_size arch_kernel_obj - 1)} = {}; Suc (unat (2 ^ arch_kobj_size arch_kernel_obj - 1)) \<le> 2 ^ magnitude; valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); magnitude < 6; koa = ArchObj arch_kernel_obj\<rbrakk> \<Longrightarrow> arch_kobj_size arch_kernel_obj < 32
 2. \<And>ko p y koa P. \<lbrakk>y \<in> {base..base + (2 ^ magnitude - 1)}; pspace_relation (kheap s) (ksPSpace s'); ekheap_relation (ekheap s) (ksPSpace s'); sched_act_relation (scheduler_action s) (ksSchedulerAction s'); ready_queues_relation (ready_queues s) (ksReadyQueues s'); ghost_relation (kheap s) (gsUserPages s') (gsCNodes s'); cdt_relation (swp (cte_wp_at (\<lambda>_. True)) s) (cdt s) (ctes_of s'); cdt_list_relation (cdt_list s) (cdt s) (ctes_of s'); revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) (ctes_of s'); (arch_state s, ksArchState s') \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState s'); cur_thread s = ksCurThread s'; idle_thread s = ksIdleThread s'; machine_state s = ksMachineState s'; work_units_completed s = ksWorkUnitsCompleted s'; domain_index s = ksDomScheduleIdx s'; domain_list s = ksDomSchedule s'; cur_domain s = ksCurDomain s'; domain_time s = ksDomainTime s'; kheap s y = Some koa; (p, P) \<in> obj_relation_cuts koa y; P koa (KOArch ko); p \<in> {base..base + (2 ^ magnitude - 1)}; (if idx < 2 ^ magnitude then {base + word_of_nat idx..base + 2 ^ magnitude - 1} else {}) \<inter> {y..y + (2 ^ obj_bits koa - 1)} = {}; obj_bits koa \<le> magnitude; valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); magnitude < 6\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>ko p y koa P arch_kernel_obj x41 x42. \<lbrakk>y \<in> {base..base + (2 ^ magnitude - 1)}; pspace_relation (kheap s) (ksPSpace s'); ekheap_relation (ekheap s) (ksPSpace s'); sched_act_relation (scheduler_action s) (ksSchedulerAction s'); ready_queues_relation (ready_queues s) (ksReadyQueues s'); ghost_relation (kheap s) (gsUserPages s') (gsCNodes s'); cdt_relation (swp (cte_wp_at (\<lambda>_. True)) s) (cdt s) (ctes_of s'); cdt_list_relation (cdt_list s) (cdt s) (ctes_of s'); revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) (ctes_of s'); (arch_state s, ksArchState s') \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState s'); cur_thread s = ksCurThread s'; idle_thread s = ksIdleThread s'; machine_state s = ksMachineState s'; work_units_completed s = ksWorkUnitsCompleted s'; domain_index s = ksDomScheduleIdx s'; domain_list s = ksDomSchedule s'; cur_domain s = ksCurDomain s'; domain_time s = ksDomainTime s'; kheap s y = Some (ArchObj (DataPage x41 x42)); \<exists>n. p = y + n * 0x1000 \<and> P = (\<lambda>_ obj. obj = (if x41 then KOUserDataDevice else KOUserData)) \<and> n < 2 ^ (pageBitsForSize x42 - 12); P (ArchObj (DataPage x41 x42)) (KOArch ko); p \<in> {base..base + (2 ^ magnitude - 1)}; (if idx < 2 ^ magnitude then {base + word_of_nat idx..base + 2 ^ magnitude - 1} else {}) \<inter> {y..y + (2 ^ pageBitsForSize x42 - 1)} = {}; Suc (unat (2 ^ pageBitsForSize x42 - 1)) \<le> 2 ^ magnitude; valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); magnitude < 6; koa = ArchObj (DataPage x41 x42); arch_kernel_obj = DataPage x41 x42\<rbrakk> \<Longrightarrow> pageBitsForSize x42 < 32
 2. \<And>ko p y koa P. \<lbrakk>y \<in> {base..base + (2 ^ magnitude - 1)}; pspace_relation (kheap s) (ksPSpace s'); ekheap_relation (ekheap s) (ksPSpace s'); sched_act_relation (scheduler_action s) (ksSchedulerAction s'); ready_queues_relation (ready_queues s) (ksReadyQueues s'); ghost_relation (kheap s) (gsUserPages s') (gsCNodes s'); cdt_relation (swp (cte_wp_at (\<lambda>_. True)) s) (cdt s) (ctes_of s'); cdt_list_relation (cdt_list s) (cdt s) (ctes_of s'); revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) (ctes_of s'); (arch_state s, ksArchState s') \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState s'); cur_thread s = ksCurThread s'; idle_thread s = ksIdleThread s'; machine_state s = ksMachineState s'; work_units_completed s = ksWorkUnitsCompleted s'; domain_index s = ksDomScheduleIdx s'; domain_list s = ksDomSchedule s'; cur_domain s = ksCurDomain s'; domain_time s = ksDomainTime s'; kheap s y = Some koa; (p, P) \<in> obj_relation_cuts koa y; P koa (KOArch ko); p \<in> {base..base + (2 ^ magnitude - 1)}; (if idx < 2 ^ magnitude then {base + word_of_nat idx..base + 2 ^ magnitude - 1} else {}) \<inter> {y..y + (2 ^ obj_bits koa - 1)} = {}; obj_bits koa \<le> magnitude; valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); magnitude < 6\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>ko p y koa P. \<lbrakk>y \<in> {base..base + (2 ^ magnitude - 1)}; pspace_relation (kheap s) (ksPSpace s'); ekheap_relation (ekheap s) (ksPSpace s'); sched_act_relation (scheduler_action s) (ksSchedulerAction s'); ready_queues_relation (ready_queues s) (ksReadyQueues s'); ghost_relation (kheap s) (gsUserPages s') (gsCNodes s'); cdt_relation (swp (cte_wp_at (\<lambda>_. True)) s) (cdt s) (ctes_of s'); cdt_list_relation (cdt_list s) (cdt s) (ctes_of s'); revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) (ctes_of s'); (arch_state s, ksArchState s') \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState s'); cur_thread s = ksCurThread s'; idle_thread s = ksIdleThread s'; machine_state s = ksMachineState s'; work_units_completed s = ksWorkUnitsCompleted s'; domain_index s = ksDomScheduleIdx s'; domain_list s = ksDomSchedule s'; cur_domain s = ksCurDomain s'; domain_time s = ksDomainTime s'; kheap s y = Some koa; (p, P) \<in> obj_relation_cuts koa y; P koa (KOArch ko); p \<in> {base..base + (2 ^ magnitude - 1)}; (if idx < 2 ^ magnitude then {base + word_of_nat idx..base + 2 ^ magnitude - 1} else {}) \<inter> {y..y + (2 ^ obj_bits koa - 1)} = {}; obj_bits koa \<le> magnitude; valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); magnitude < 6\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>ko p y koa P. \<lbrakk>y \<in> {base..base + (2 ^ magnitude - 1)}; pspace_relation (kheap s) (ksPSpace s'); ekheap_relation (ekheap s) (ksPSpace s'); sched_act_relation (scheduler_action s) (ksSchedulerAction s'); ready_queues_relation (ready_queues s) (ksReadyQueues s'); ghost_relation (kheap s) (gsUserPages s') (gsCNodes s'); cdt_relation (swp (cte_wp_at (\<lambda>_. True)) s) (cdt s) (ctes_of s'); cdt_list_relation (cdt_list s) (cdt s) (ctes_of s'); revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) (ctes_of s'); (arch_state s, ksArchState s') \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState s'); cur_thread s = ksCurThread s'; idle_thread s = ksIdleThread s'; machine_state s = ksMachineState s'; work_units_completed s = ksWorkUnitsCompleted s'; domain_index s = ksDomScheduleIdx s'; domain_list s = ksDomSchedule s'; cur_domain s = ksCurDomain s'; domain_time s = ksDomainTime s'; kheap s y = Some koa; (p, P) \<in> obj_relation_cuts koa y; P koa (KOArch ko); p \<in> {base..base + (2 ^ magnitude - 1)}; (if idx < 2 ^ magnitude then {base + word_of_nat idx..base + 2 ^ magnitude - 1} else {}) \<inter> {y..y + (2 ^ obj_bits koa - 1)} = {}; obj_bits koa \<le> magnitude; valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); magnitude < 6; 6 \<le> obj_bits koa\<rbrakk> \<Longrightarrow> False
 2. \<And>ko p y koa P. \<lbrakk>y \<in> {base..base + (2 ^ magnitude - 1)}; pspace_relation (kheap s) (ksPSpace s'); ekheap_relation (ekheap s) (ksPSpace s'); sched_act_relation (scheduler_action s) (ksSchedulerAction s'); ready_queues_relation (ready_queues s) (ksReadyQueues s'); ghost_relation (kheap s) (gsUserPages s') (gsCNodes s'); cdt_relation (swp (cte_wp_at (\<lambda>_. True)) s) (cdt s) (ctes_of s'); cdt_list_relation (cdt_list s) (cdt s) (ctes_of s'); revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) (ctes_of s'); (arch_state s, ksArchState s') \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState s'); cur_thread s = ksCurThread s'; idle_thread s = ksIdleThread s'; machine_state s = ksMachineState s'; work_units_completed s = ksWorkUnitsCompleted s'; domain_index s = ksDomScheduleIdx s'; domain_list s = ksDomSchedule s'; cur_domain s = ksCurDomain s'; domain_time s = ksDomainTime s'; kheap s y = Some koa; (p, P) \<in> obj_relation_cuts koa y; P koa (KOArch ko); p \<in> {base..base + (2 ^ magnitude - 1)}; (if idx < 2 ^ magnitude then {base + word_of_nat idx..base + 2 ^ magnitude - 1} else {}) \<inter> {y..y + (2 ^ obj_bits koa - 1)} = {}; obj_bits koa \<le> magnitude; valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); magnitude < 6\<rbrakk> \<Longrightarrow> 6 \<le> obj_bits koa proof (prove)
goal (1 subgoal):
 1. \<And>ko p y koa P. \<lbrakk>y \<in> {base..base + (2 ^ magnitude - 1)}; pspace_relation (kheap s) (ksPSpace s'); ekheap_relation (ekheap s) (ksPSpace s'); sched_act_relation (scheduler_action s) (ksSchedulerAction s'); ready_queues_relation (ready_queues s) (ksReadyQueues s'); ghost_relation (kheap s) (gsUserPages s') (gsCNodes s'); cdt_relation (swp (cte_wp_at (\<lambda>_. True)) s) (cdt s) (ctes_of s'); cdt_list_relation (cdt_list s) (cdt s) (ctes_of s'); revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) (ctes_of s'); (arch_state s, ksArchState s') \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState s'); cur_thread s = ksCurThread s'; idle_thread s = ksIdleThread s'; machine_state s = ksMachineState s'; work_units_completed s = ksWorkUnitsCompleted s'; domain_index s = ksDomScheduleIdx s'; domain_list s = ksDomSchedule s'; cur_domain s = ksCurDomain s'; domain_time s = ksDomainTime s'; kheap s y = Some koa; (p, P) \<in> obj_relation_cuts koa y; P koa (KOArch ko); p \<in> {base..base + (2 ^ magnitude - 1)}; (if idx < 2 ^ magnitude then {base + word_of_nat idx..base + 2 ^ magnitude - 1} else {}) \<inter> {y..y + (2 ^ obj_bits koa - 1)} = {}; obj_bits koa \<le> magnitude; valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); magnitude < 6\<rbrakk> \<Longrightarrow> 6 \<le> obj_bits koa proof (prove)
goal (2 subgoals):
 1. \<And>ko p y koa P x5. \<lbrakk>arch_kobj_size x5 \<le> magnitude; valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); magnitude < 6; koa = ArchObj x5; y \<in> {base..base + (2 ^ magnitude - 1)}; pspace_relation (kheap s) (ksPSpace s'); ekheap_relation (ekheap s) (ksPSpace s'); sched_act_relation (scheduler_action s) (ksSchedulerAction s'); ready_queues_relation (ready_queues s) (ksReadyQueues s'); ghost_relation (kheap s) (gsUserPages s') (gsCNodes s'); cdt_relation (swp (cte_wp_at (\<lambda>_. True)) s) (cdt s) (ctes_of s'); cdt_list_relation (cdt_list s) (cdt s) (ctes_of s'); revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) (ctes_of s'); (arch_state s, ksArchState s') \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState s'); cur_thread s = ksCurThread s'; idle_thread s = ksIdleThread s'; machine_state s = ksMachineState s'; work_units_completed s = ksWorkUnitsCompleted s'; domain_index s = ksDomScheduleIdx s'; domain_list s = ksDomSchedule s'; cur_domain s = ksCurDomain s'; domain_time s = ksDomainTime s'; kheap s y = Some (ArchObj x5); (p, P) \<in> aobj_relation_cuts x5 y; P (ArchObj x5) (KOArch ko); p \<in> {base..base + (2 ^ magnitude - 1)}; idx < 2 ^ magnitude; {base + word_of_nat idx..base + 2 ^ magnitude - 1} \<inter> {y..y + (2 ^ arch_kobj_size x5 - 1)} = {}\<rbrakk> \<Longrightarrow> False
 2. \<And>ko p y koa P x5. \<lbrakk>arch_kobj_size x5 \<le> magnitude; valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); magnitude < 6; koa = ArchObj x5; y \<in> {base..base + (2 ^ magnitude - 1)}; pspace_relation (kheap s) (ksPSpace s'); ekheap_relation (ekheap s) (ksPSpace s'); sched_act_relation (scheduler_action s) (ksSchedulerAction s'); ready_queues_relation (ready_queues s) (ksReadyQueues s'); ghost_relation (kheap s) (gsUserPages s') (gsCNodes s'); cdt_relation (swp (cte_wp_at (\<lambda>_. True)) s) (cdt s) (ctes_of s'); cdt_list_relation (cdt_list s) (cdt s) (ctes_of s'); revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) (ctes_of s'); (arch_state s, ksArchState s') \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState s'); cur_thread s = ksCurThread s'; idle_thread s = ksIdleThread s'; machine_state s = ksMachineState s'; work_units_completed s = ksWorkUnitsCompleted s'; domain_index s = ksDomScheduleIdx s'; domain_list s = ksDomSchedule s'; cur_domain s = ksCurDomain s'; domain_time s = ksDomainTime s'; kheap s y = Some (ArchObj x5); (p, P) \<in> aobj_relation_cuts x5 y; P (ArchObj x5) (KOArch ko); p \<in> {base..base + (2 ^ magnitude - 1)}; \<not> idx < 2 ^ magnitude\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals! proof (state)
this:
\<lbrakk>ksPSpace s' ?p = Some (KOArch ?ko); ?p \<in> {base..base + 2 ^ magnitude - 1}\<rbrakk> \<Longrightarrow> 6 \<le> magnitude

goal (1 subgoal):
 1. deletionIsSafe base magnitude s' proof (prove)
using this:
\<lbrakk>ksPSpace s' ?p = Some (KOArch ?ko); ?p \<in> {base..base + 2 ^ magnitude - 1}\<rbrakk> \<Longrightarrow> 6 \<le> magnitude

goal (1 subgoal):
 1. deletionIsSafe base magnitude s' proof (prove)
using this:
\<lbrakk>ksPSpace s' ?p = Some (KOArch ?ko); ?p \<in> {base..base + 2 ^ magnitude - 1}\<rbrakk> \<Longrightarrow> 6 \<le> magnitude
\<forall>t. t \<in> {base..base + 2 ^ magnitude - 1} \<longrightarrow> (\<forall>ptr m r. \<not> cte_wp_at' (\<lambda>cte. cteCap cte = capability.ReplyCap t m r) ptr s')

goal (1 subgoal):
 1. deletionIsSafe base magnitude s' proof (state)
this:
deletionIsSafe base magnitude s'

goal:
No subgoals!