theory ArchAcc_R

lemma page_directory_at_state_relation:
  "\<lbrakk>page_directory_at ptr s; pspace_aligned s;
     (s, sa) \<in> state_relation;pspace_distinct' sa\<rbrakk>
  \<Longrightarrow> page_directory_at' ptr sa" apply (clarsimp simp:page_directory_at'_def state_relation_def obj_at_def) apply (clarsimp simp:pspace_relation_def) apply (drule bspec) apply fastforce apply clarsimp apply (frule(1) pspace_alignedD) apply (simp add: pdBits_def pageBits_def pdeBits_def) apply clarsimp apply (drule_tac x = "ucast y" in spec) apply (drule sym[where s = "pspace_dom (kheap s)"]) apply (clarsimp simp:typ_at'_def ko_wp_at'_def) apply (subgoal_tac "(ptr + (y << 2)) \<in> dom (ksPSpace sa)") prefer 2 apply (clarsimp simp: pspace_dom_def) apply (rule_tac x = "ptr" in bexI[where A = "dom (kheap s)"]) apply (simp add: image_def) apply (rule_tac x = "ucast y" in exI) apply (simp add:ucast_ucast_len) apply fastforce apply (thin_tac "dom a = b" for a b) apply (frule(1) pspace_alignedD) apply (clarsimp simp:ucast_ucast_len split:if_splits) apply (drule pde_relation_must_pde) apply (drule(1) pspace_distinctD') apply (clarsimp simp:objBits_simps archObjSize_def) apply (rule is_aligned_weaken) apply (erule aligned_add_aligned) apply (rule is_aligned_shiftl_self) apply simp apply (simp add: pdeBits_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>typ_at (AArch APageDirectory) ptr s; pspace_aligned s; (s, sa) \<in> state_relation; pspace_distinct' sa\<rbrakk> \<Longrightarrow> page_directory_at' ptr sa proof (prove)
goal (1 subgoal):
 1. \<And>pd. \<lbrakk>pspace_aligned s; pspace_distinct' sa; pspace_relation (kheap s) (ksPSpace sa); kheap s ptr = Some (ArchObj (PageDirectory pd)); ekheap_relation (ekheap s) (ksPSpace sa); sched_act_relation (scheduler_action s) (ksSchedulerAction sa); ready_queues_relation (ready_queues s) (ksReadyQueues sa); ghost_relation (kheap s) (gsUserPages sa) (gsCNodes sa); cdt_relation (swp (cte_wp_at (\<lambda>_. True)) s) (cdt s) (ctes_of sa); cdt_list_relation (cdt_list s) (cdt s) (ctes_of sa); revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) (ctes_of sa); (arch_state s, ksArchState sa) \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState sa); cur_thread s = ksCurThread sa; idle_thread s = ksIdleThread sa; machine_state s = ksMachineState sa; work_units_completed s = ksWorkUnitsCompleted sa; domain_index s = ksDomScheduleIdx sa; domain_list s = ksDomSchedule sa; cur_domain s = ksCurDomain sa; domain_time s = ksDomainTime sa\<rbrakk> \<Longrightarrow> is_aligned ptr pdBits \<and> (\<forall>y<0x1000. pde_at' (ptr + (y << 2)) sa) proof (prove)
goal (1 subgoal):
 1. \<And>pd. \<lbrakk>pspace_aligned s; pspace_distinct' sa; kheap s ptr = Some (ArchObj (PageDirectory pd)); ekheap_relation (ekheap s) (ksPSpace sa); sched_act_relation (scheduler_action s) (ksSchedulerAction sa); ready_queues_relation (ready_queues s) (ksReadyQueues sa); ghost_relation (kheap s) (gsUserPages sa) (gsCNodes sa); cdt_relation (swp (cte_wp_at (\<lambda>_. True)) s) (cdt s) (ctes_of sa); cdt_list_relation (cdt_list s) (cdt s) (ctes_of sa); revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) (ctes_of sa); (arch_state s, ksArchState sa) \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState sa); cur_thread s = ksCurThread sa; idle_thread s = ksIdleThread sa; machine_state s = ksMachineState sa; work_units_completed s = ksWorkUnitsCompleted sa; domain_index s = ksDomScheduleIdx sa; domain_list s = ksDomSchedule sa; cur_domain s = ksCurDomain sa; domain_time s = ksDomainTime sa; pspace_dom (kheap s) = dom (ksPSpace sa); \<forall>x\<in>dom (kheap s). \<forall>xa\<in>obj_relation_cuts (the (kheap s x)) x. case xa of (y, P) \<Rightarrow> P (the (kheap s x)) (the (ksPSpace sa y))\<rbrakk> \<Longrightarrow> is_aligned ptr pdBits \<and> (\<forall>y<0x1000. pde_at' (ptr + (y << 2)) sa) proof (prove)
goal (2 subgoals):
 1. \<And>pd. \<lbrakk>pspace_aligned s; pspace_distinct' sa; kheap s ptr = Some (ArchObj (PageDirectory pd)); ekheap_relation (ekheap s) (ksPSpace sa); sched_act_relation (scheduler_action s) (ksSchedulerAction sa); ready_queues_relation (ready_queues s) (ksReadyQueues sa); ghost_relation (kheap s) (gsUserPages sa) (gsCNodes sa); cdt_relation (swp (cte_wp_at (\<lambda>_. True)) s) (cdt s) (ctes_of sa); cdt_list_relation (cdt_list s) (cdt s) (ctes_of sa); revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) (ctes_of sa); (arch_state s, ksArchState sa) \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState sa); cur_thread s = ksCurThread sa; idle_thread s = ksIdleThread sa; machine_state s = ksMachineState sa; work_units_completed s = ksWorkUnitsCompleted sa; domain_index s = ksDomScheduleIdx sa; domain_list s = ksDomSchedule sa; cur_domain s = ksCurDomain sa; domain_time s = ksDomainTime sa; pspace_dom (kheap s) = dom (ksPSpace sa)\<rbrakk> \<Longrightarrow> ?x25 pd \<in> dom (kheap s)
 2. \<And>pd. \<lbrakk>pspace_aligned s; pspace_distinct' sa; kheap s ptr = Some (ArchObj (PageDirectory pd)); ekheap_relation (ekheap s) (ksPSpace sa); sched_act_relation (scheduler_action s) (ksSchedulerAction sa); ready_queues_relation (ready_queues s) (ksReadyQueues sa); ghost_relation (kheap s) (gsUserPages sa) (gsCNodes sa); cdt_relation (swp (cte_wp_at (\<lambda>_. True)) s) (cdt s) (ctes_of sa); cdt_list_relation (cdt_list s) (cdt s) (ctes_of sa); revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) (ctes_of sa); (arch_state s, ksArchState sa) \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState sa); cur_thread s = ksCurThread sa; idle_thread s = ksIdleThread sa; machine_state s = ksMachineState sa; work_units_completed s = ksWorkUnitsCompleted sa; domain_index s = ksDomScheduleIdx sa; domain_list s = ksDomSchedule sa; cur_domain s = ksCurDomain sa; domain_time s = ksDomainTime sa; pspace_dom (kheap s) = dom (ksPSpace sa); \<forall>x\<in>obj_relation_cuts (the (kheap s (?x25 pd))) (?x25 pd). case x of (y, P) \<Rightarrow> P (the (kheap s (?x25 pd))) (the (ksPSpace sa y))\<rbrakk> \<Longrightarrow> is_aligned ptr pdBits \<and> (\<forall>y<0x1000. pde_at' (ptr + (y << 2)) sa) proof (prove)
goal (1 subgoal):
 1. \<And>pd. \<lbrakk>pspace_aligned s; pspace_distinct' sa; kheap s ptr = Some (ArchObj (PageDirectory pd)); ekheap_relation (ekheap s) (ksPSpace sa); sched_act_relation (scheduler_action s) (ksSchedulerAction sa); ready_queues_relation (ready_queues s) (ksReadyQueues sa); ghost_relation (kheap s) (gsUserPages sa) (gsCNodes sa); cdt_relation (swp (cte_wp_at (\<lambda>_. True)) s) (cdt s) (ctes_of sa); cdt_list_relation (cdt_list s) (cdt s) (ctes_of sa); revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) (ctes_of sa); (arch_state s, ksArchState sa) \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState sa); cur_thread s = ksCurThread sa; idle_thread s = ksIdleThread sa; machine_state s = ksMachineState sa; work_units_completed s = ksWorkUnitsCompleted sa; domain_index s = ksDomScheduleIdx sa; domain_list s = ksDomSchedule sa; cur_domain s = ksCurDomain sa; domain_time s = ksDomainTime sa; pspace_dom (kheap s) = dom (ksPSpace sa); \<forall>x\<in>obj_relation_cuts (the (kheap s ptr)) ptr. case x of (y, P) \<Rightarrow> P (the (kheap s ptr)) (the (ksPSpace sa y))\<rbrakk> \<Longrightarrow> is_aligned ptr pdBits \<and> (\<forall>y<0x1000. pde_at' (ptr + (y << 2)) sa) proof (prove)
goal (1 subgoal):
 1. \<And>pd. \<lbrakk>pspace_aligned s; pspace_distinct' sa; kheap s ptr = Some (ArchObj (PageDirectory pd)); ekheap_relation (ekheap s) (ksPSpace sa); sched_act_relation (scheduler_action s) (ksSchedulerAction sa); ready_queues_relation (ready_queues s) (ksReadyQueues sa); ghost_relation (kheap s) (gsUserPages sa) (gsCNodes sa); cdt_relation (swp (cte_wp_at (\<lambda>_. True)) s) (cdt s) (ctes_of sa); cdt_list_relation (cdt_list s) (cdt s) (ctes_of sa); revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) (ctes_of sa); (arch_state s, ksArchState sa) \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState sa); cur_thread s = ksCurThread sa; idle_thread s = ksIdleThread sa; machine_state s = ksMachineState sa; work_units_completed s = ksWorkUnitsCompleted sa; domain_index s = ksDomScheduleIdx sa; domain_list s = ksDomSchedule sa; cur_domain s = ksCurDomain sa; domain_time s = ksDomainTime sa; pspace_dom (kheap s) = dom (ksPSpace sa); \<forall>x. pde_relation x (ArchObj (PageDirectory pd)) (the (ksPSpace sa (ptr + (UCAST(12 \<rightarrow> 32) x << 2))))\<rbrakk> \<Longrightarrow> is_aligned ptr pdBits \<and> (\<forall>y<0x1000. pde_at' (ptr + (y << 2)) sa) proof (prove)
goal (1 subgoal):
 1. \<And>pd. \<lbrakk>pspace_aligned s; pspace_distinct' sa; kheap s ptr = Some (ArchObj (PageDirectory pd)); ekheap_relation (ekheap s) (ksPSpace sa); sched_act_relation (scheduler_action s) (ksSchedulerAction sa); ready_queues_relation (ready_queues s) (ksReadyQueues sa); ghost_relation (kheap s) (gsUserPages sa) (gsCNodes sa); cdt_relation (swp (cte_wp_at (\<lambda>_. True)) s) (cdt s) (ctes_of sa); cdt_list_relation (cdt_list s) (cdt s) (ctes_of sa); revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) (ctes_of sa); (arch_state s, ksArchState sa) \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState sa); cur_thread s = ksCurThread sa; idle_thread s = ksIdleThread sa; machine_state s = ksMachineState sa; work_units_completed s = ksWorkUnitsCompleted sa; domain_index s = ksDomScheduleIdx sa; domain_list s = ksDomSchedule sa; cur_domain s = ksCurDomain sa; domain_time s = ksDomainTime sa; pspace_dom (kheap s) = dom (ksPSpace sa); \<forall>x. pde_relation x (ArchObj (PageDirectory pd)) (the (ksPSpace sa (ptr + (UCAST(12 \<rightarrow> 32) x << 2)))); is_aligned ptr (obj_bits (ArchObj (PageDirectory pd)))\<rbrakk> \<Longrightarrow> is_aligned ptr pdBits \<and> (\<forall>y<0x1000. pde_at' (ptr + (y << 2)) sa) proof (prove)
goal (1 subgoal):
 1. \<And>pd. \<lbrakk>pspace_aligned s; pspace_distinct' sa; kheap s ptr = Some (ArchObj (PageDirectory pd)); ekheap_relation (ekheap s) (ksPSpace sa); sched_act_relation (scheduler_action s) (ksSchedulerAction sa); ready_queues_relation (ready_queues s) (ksReadyQueues sa); ghost_relation (kheap s) (gsUserPages sa) (gsCNodes sa); cdt_relation (swp (cte_wp_at (\<lambda>_. True)) s) (cdt s) (ctes_of sa); cdt_list_relation (cdt_list s) (cdt s) (ctes_of sa); revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) (ctes_of sa); (arch_state s, ksArchState sa) \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState sa); cur_thread s = ksCurThread sa; idle_thread s = ksIdleThread sa; machine_state s = ksMachineState sa; work_units_completed s = ksWorkUnitsCompleted sa; domain_index s = ksDomScheduleIdx sa; domain_list s = ksDomSchedule sa; cur_domain s = ksCurDomain sa; domain_time s = ksDomainTime sa; pspace_dom (kheap s) = dom (ksPSpace sa); \<forall>x. pde_relation x (ArchObj (PageDirectory pd)) (the (ksPSpace sa (ptr + (UCAST(12 \<rightarrow> 32) x << 2)))); is_aligned ptr 14\<rbrakk> \<Longrightarrow> \<forall>y<0x1000. pde_at' (ptr + (y << 2)) sa proof (prove)
goal (1 subgoal):
 1. \<And>pd y. \<lbrakk>pspace_aligned s; pspace_distinct' sa; kheap s ptr = Some (ArchObj (PageDirectory pd)); ekheap_relation (ekheap s) (ksPSpace sa); sched_act_relation (scheduler_action s) (ksSchedulerAction sa); ready_queues_relation (ready_queues s) (ksReadyQueues sa); ghost_relation (kheap s) (gsUserPages sa) (gsCNodes sa); cdt_relation (swp (cte_wp_at (\<lambda>_. True)) s) (cdt s) (ctes_of sa); cdt_list_relation (cdt_list s) (cdt s) (ctes_of sa); revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) (ctes_of sa); (arch_state s, ksArchState sa) \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState sa); cur_thread s = ksCurThread sa; idle_thread s = ksIdleThread sa; machine_state s = ksMachineState sa; work_units_completed s = ksWorkUnitsCompleted sa; domain_index s = ksDomScheduleIdx sa; domain_list s = ksDomSchedule sa; cur_domain s = ksCurDomain sa; domain_time s = ksDomainTime sa; pspace_dom (kheap s) = dom (ksPSpace sa); \<forall>x. pde_relation x (ArchObj (PageDirectory pd)) (the (ksPSpace sa (ptr + (UCAST(12 \<rightarrow> 32) x << 2)))); is_aligned ptr 14; y < 0x1000\<rbrakk> \<Longrightarrow> pde_at' (ptr + (y << 2)) sa proof (prove)
goal (1 subgoal):
 1. \<And>pd y. \<lbrakk>pspace_aligned s; pspace_distinct' sa; kheap s ptr = Some (ArchObj (PageDirectory pd)); ekheap_relation (ekheap s) (ksPSpace sa); sched_act_relation (scheduler_action s) (ksSchedulerAction sa); ready_queues_relation (ready_queues s) (ksReadyQueues sa); ghost_relation (kheap s) (gsUserPages sa) (gsCNodes sa); cdt_relation (swp (cte_wp_at (\<lambda>_. True)) s) (cdt s) (ctes_of sa); cdt_list_relation (cdt_list s) (cdt s) (ctes_of sa); revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) (ctes_of sa); (arch_state s, ksArchState sa) \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState sa); cur_thread s = ksCurThread sa; idle_thread s = ksIdleThread sa; machine_state s = ksMachineState sa; work_units_completed s = ksWorkUnitsCompleted sa; domain_index s = ksDomScheduleIdx sa; domain_list s = ksDomSchedule sa; cur_domain s = ksCurDomain sa; domain_time s = ksDomainTime sa; pspace_dom (kheap s) = dom (ksPSpace sa); is_aligned ptr 14; y < 0x1000; pde_relation (UCAST(32 \<rightarrow> 12) y) (ArchObj (PageDirectory pd)) (the (ksPSpace sa (ptr + (UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) y) << 2))))\<rbrakk> \<Longrightarrow> pde_at' (ptr + (y << 2)) sa proof (prove)
goal (1 subgoal):
 1. \<And>pd y. \<lbrakk>pspace_aligned s; pspace_distinct' sa; kheap s ptr = Some (ArchObj (PageDirectory pd)); ekheap_relation (ekheap s) (ksPSpace sa); sched_act_relation (scheduler_action s) (ksSchedulerAction sa); ready_queues_relation (ready_queues s) (ksReadyQueues sa); ghost_relation (kheap s) (gsUserPages sa) (gsCNodes sa); cdt_relation (swp (cte_wp_at (\<lambda>_. True)) s) (cdt s) (ctes_of sa); cdt_list_relation (cdt_list s) (cdt s) (ctes_of sa); revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) (ctes_of sa); (arch_state s, ksArchState sa) \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState sa); cur_thread s = ksCurThread sa; idle_thread s = ksIdleThread sa; machine_state s = ksMachineState sa; work_units_completed s = ksWorkUnitsCompleted sa; domain_index s = ksDomScheduleIdx sa; domain_list s = ksDomSchedule sa; cur_domain s = ksCurDomain sa; domain_time s = ksDomainTime sa; is_aligned ptr 14; y < 0x1000; pde_relation (UCAST(32 \<rightarrow> 12) y) (ArchObj (PageDirectory pd)) (the (ksPSpace sa (ptr + (UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) y) << 2)))); dom (ksPSpace sa) = pspace_dom (kheap s)\<rbrakk> \<Longrightarrow> pde_at' (ptr + (y << 2)) sa proof (prove)
goal (1 subgoal):
 1. \<And>pd y. \<lbrakk>pspace_aligned s; pspace_distinct' sa; kheap s ptr = Some (ArchObj (PageDirectory pd)); ekheap_relation (ekheap s) (ksPSpace sa); sched_act_relation (scheduler_action s) (ksSchedulerAction sa); ready_queues_relation (ready_queues s) (ksReadyQueues sa); ghost_relation (kheap s) (gsUserPages sa) (gsCNodes sa); cdt_relation (swp (cte_wp_at (\<lambda>_. True)) s) (cdt s) (ctes_of sa); cdt_list_relation (cdt_list s) (cdt s) (ctes_of sa); revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) (ctes_of sa); (arch_state s, ksArchState sa) \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState sa); cur_thread s = ksCurThread sa; idle_thread s = ksIdleThread sa; machine_state s = ksMachineState sa; work_units_completed s = ksWorkUnitsCompleted sa; domain_index s = ksDomScheduleIdx sa; domain_list s = ksDomSchedule sa; cur_domain s = ksCurDomain sa; domain_time s = ksDomainTime sa; is_aligned ptr 14; y < 0x1000; pde_relation (UCAST(32 \<rightarrow> 12) y) (ArchObj (PageDirectory pd)) (the (ksPSpace sa (ptr + (UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) y) << 2)))); dom (ksPSpace sa) = pspace_dom (kheap s)\<rbrakk> \<Longrightarrow> \<exists>ko. ksPSpace sa (ptr + (y << 2)) = Some ko \<and> is_aligned (ptr + (y << 2)) (objBitsKO ko) \<and> koTypeOf ko = ArchT PDET \<and> ps_clear (ptr + (y << 2)) (objBitsKO ko) sa proof (prove)
goal (2 subgoals):
 1. \<And>pd y. \<lbrakk>pspace_aligned s; pspace_distinct' sa; kheap s ptr = Some (ArchObj (PageDirectory pd)); ekheap_relation (ekheap s) (ksPSpace sa); sched_act_relation (scheduler_action s) (ksSchedulerAction sa); ready_queues_relation (ready_queues s) (ksReadyQueues sa); ghost_relation (kheap s) (gsUserPages sa) (gsCNodes sa); cdt_relation (swp (cte_wp_at (\<lambda>_. True)) s) (cdt s) (ctes_of sa); cdt_list_relation (cdt_list s) (cdt s) (ctes_of sa); revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) (ctes_of sa); (arch_state s, ksArchState sa) \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState sa); cur_thread s = ksCurThread sa; idle_thread s = ksIdleThread sa; machine_state s = ksMachineState sa; work_units_completed s = ksWorkUnitsCompleted sa; domain_index s = ksDomScheduleIdx sa; domain_list s = ksDomSchedule sa; cur_domain s = ksCurDomain sa; domain_time s = ksDomainTime sa; is_aligned ptr 14; y < 0x1000; pde_relation (UCAST(32 \<rightarrow> 12) y) (ArchObj (PageDirectory pd)) (the (ksPSpace sa (ptr + (UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) y) << 2)))); dom (ksPSpace sa) = pspace_dom (kheap s); ptr + (y << 2) \<in> dom (ksPSpace sa)\<rbrakk> \<Longrightarrow> \<exists>ko. ksPSpace sa (ptr + (y << 2)) = Some ko \<and> is_aligned (ptr + (y << 2)) (objBitsKO ko) \<and> koTypeOf ko = ArchT PDET \<and> ps_clear (ptr + (y << 2)) (objBitsKO ko) sa
 2. \<And>pd y. \<lbrakk>pspace_aligned s; pspace_distinct' sa; kheap s ptr = Some (ArchObj (PageDirectory pd)); ekheap_relation (ekheap s) (ksPSpace sa); sched_act_relation (scheduler_action s) (ksSchedulerAction sa); ready_queues_relation (ready_queues s) (ksReadyQueues sa); ghost_relation (kheap s) (gsUserPages sa) (gsCNodes sa); cdt_relation (swp (cte_wp_at (\<lambda>_. True)) s) (cdt s) (ctes_of sa); cdt_list_relation (cdt_list s) (cdt s) (ctes_of sa); revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) (ctes_of sa); (arch_state s, ksArchState sa) \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState sa); cur_thread s = ksCurThread sa; idle_thread s = ksIdleThread sa; machine_state s = ksMachineState sa; work_units_completed s = ksWorkUnitsCompleted sa; domain_index s = ksDomScheduleIdx sa; domain_list s = ksDomSchedule sa; cur_domain s = ksCurDomain sa; domain_time s = ksDomainTime sa; is_aligned ptr 14; y < 0x1000; pde_relation (UCAST(32 \<rightarrow> 12) y) (ArchObj (PageDirectory pd)) (the (ksPSpace sa (ptr + (UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) y) << 2)))); dom (ksPSpace sa) = pspace_dom (kheap s)\<rbrakk> \<Longrightarrow> ptr + (y << 2) \<in> dom (ksPSpace sa) proof (prove)
goal (2 subgoals):
 1. \<And>pd y. \<lbrakk>pspace_aligned s; pspace_distinct' sa; kheap s ptr = Some (ArchObj (PageDirectory pd)); ekheap_relation (ekheap s) (ksPSpace sa); sched_act_relation (scheduler_action s) (ksSchedulerAction sa); ready_queues_relation (ready_queues s) (ksReadyQueues sa); ghost_relation (kheap s) (gsUserPages sa) (gsCNodes sa); cdt_relation (swp (cte_wp_at (\<lambda>_. True)) s) (cdt s) (ctes_of sa); cdt_list_relation (cdt_list s) (cdt s) (ctes_of sa); revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) (ctes_of sa); (arch_state s, ksArchState sa) \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState sa); cur_thread s = ksCurThread sa; idle_thread s = ksIdleThread sa; machine_state s = ksMachineState sa; work_units_completed s = ksWorkUnitsCompleted sa; domain_index s = ksDomScheduleIdx sa; domain_list s = ksDomSchedule sa; cur_domain s = ksCurDomain sa; domain_time s = ksDomainTime sa; is_aligned ptr 14; y < 0x1000; pde_relation (UCAST(32 \<rightarrow> 12) y) (ArchObj (PageDirectory pd)) (the (ksPSpace sa (ptr + (UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) y) << 2)))); dom (ksPSpace sa) = pspace_dom (kheap s)\<rbrakk> \<Longrightarrow> ptr + (y << 2) \<in> dom (ksPSpace sa)
 2. \<And>pd y. \<lbrakk>pspace_aligned s; pspace_distinct' sa; kheap s ptr = Some (ArchObj (PageDirectory pd)); ekheap_relation (ekheap s) (ksPSpace sa); sched_act_relation (scheduler_action s) (ksSchedulerAction sa); ready_queues_relation (ready_queues s) (ksReadyQueues sa); ghost_relation (kheap s) (gsUserPages sa) (gsCNodes sa); cdt_relation (swp (cte_wp_at (\<lambda>_. True)) s) (cdt s) (ctes_of sa); cdt_list_relation (cdt_list s) (cdt s) (ctes_of sa); revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) (ctes_of sa); (arch_state s, ksArchState sa) \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState sa); cur_thread s = ksCurThread sa; idle_thread s = ksIdleThread sa; machine_state s = ksMachineState sa; work_units_completed s = ksWorkUnitsCompleted sa; domain_index s = ksDomScheduleIdx sa; domain_list s = ksDomSchedule sa; cur_domain s = ksCurDomain sa; domain_time s = ksDomainTime sa; is_aligned ptr 14; y < 0x1000; pde_relation (UCAST(32 \<rightarrow> 12) y) (ArchObj (PageDirectory pd)) (the (ksPSpace sa (ptr + (UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) y) << 2)))); dom (ksPSpace sa) = pspace_dom (kheap s); ptr + (y << 2) \<in> dom (ksPSpace sa)\<rbrakk> \<Longrightarrow> \<exists>ko. ksPSpace sa (ptr + (y << 2)) = Some ko \<and> is_aligned (ptr + (y << 2)) (objBitsKO ko) \<and> koTypeOf ko = ArchT PDET \<and> ps_clear (ptr + (y << 2)) (objBitsKO ko) sa proof (prove)
goal (2 subgoals):
 1. \<And>pd y. \<lbrakk>pspace_aligned s; pspace_distinct' sa; kheap s ptr = Some (ArchObj (PageDirectory pd)); ekheap_relation (ekheap s) (ksPSpace sa); sched_act_relation (scheduler_action s) (ksSchedulerAction sa); ready_queues_relation (ready_queues s) (ksReadyQueues sa); ghost_relation (kheap s) (gsUserPages sa) (gsCNodes sa); cdt_relation (swp (cte_wp_at (\<lambda>_. True)) s) (cdt s) (ctes_of sa); cdt_list_relation (cdt_list s) (cdt s) (ctes_of sa); revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) (ctes_of sa); (arch_state s, ksArchState sa) \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState sa); cur_thread s = ksCurThread sa; idle_thread s = ksIdleThread sa; machine_state s = ksMachineState sa; work_units_completed s = ksWorkUnitsCompleted sa; domain_index s = ksDomScheduleIdx sa; domain_list s = ksDomSchedule sa; cur_domain s = ksCurDomain sa; domain_time s = ksDomainTime sa; is_aligned ptr 14; y < 0x1000; pde_relation (UCAST(32 \<rightarrow> 12) y) (ArchObj (PageDirectory pd)) (the (ksPSpace sa (ptr + (UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) y) << 2)))); dom (ksPSpace sa) = (\<Union>x\<in>dom (kheap s). fst ` obj_relation_cuts (the (kheap s x)) x)\<rbrakk> \<Longrightarrow> \<exists>x\<in>dom (kheap s). ptr + (y << 2) \<in> fst ` obj_relation_cuts (the (kheap s x)) x
 2. \<And>pd y. \<lbrakk>pspace_aligned s; pspace_distinct' sa; kheap s ptr = Some (ArchObj (PageDirectory pd)); ekheap_relation (ekheap s) (ksPSpace sa); sched_act_relation (scheduler_action s) (ksSchedulerAction sa); ready_queues_relation (ready_queues s) (ksReadyQueues sa); ghost_relation (kheap s) (gsUserPages sa) (gsCNodes sa); cdt_relation (swp (cte_wp_at (\<lambda>_. True)) s) (cdt s) (ctes_of sa); cdt_list_relation (cdt_list s) (cdt s) (ctes_of sa); revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) (ctes_of sa); (arch_state s, ksArchState sa) \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState sa); cur_thread s = ksCurThread sa; idle_thread s = ksIdleThread sa; machine_state s = ksMachineState sa; work_units_completed s = ksWorkUnitsCompleted sa; domain_index s = ksDomScheduleIdx sa; domain_list s = ksDomSchedule sa; cur_domain s = ksCurDomain sa; domain_time s = ksDomainTime sa; is_aligned ptr 14; y < 0x1000; pde_relation (UCAST(32 \<rightarrow> 12) y) (ArchObj (PageDirectory pd)) (the (ksPSpace sa (ptr + (UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) y) << 2)))); dom (ksPSpace sa) = pspace_dom (kheap s); ptr + (y << 2) \<in> dom (ksPSpace sa)\<rbrakk> \<Longrightarrow> \<exists>ko. ksPSpace sa (ptr + (y << 2)) = Some ko \<and> is_aligned (ptr + (y << 2)) (objBitsKO ko) \<and> koTypeOf ko = ArchT PDET \<and> ps_clear (ptr + (y << 2)) (objBitsKO ko) sa proof (prove)
goal (3 subgoals):
 1. \<And>pd y. \<lbrakk>pspace_aligned s; pspace_distinct' sa; kheap s ptr = Some (ArchObj (PageDirectory pd)); ekheap_relation (ekheap s) (ksPSpace sa); sched_act_relation (scheduler_action s) (ksSchedulerAction sa); ready_queues_relation (ready_queues s) (ksReadyQueues sa); ghost_relation (kheap s) (gsUserPages sa) (gsCNodes sa); cdt_relation (swp (cte_wp_at (\<lambda>_. True)) s) (cdt s) (ctes_of sa); cdt_list_relation (cdt_list s) (cdt s) (ctes_of sa); revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) (ctes_of sa); (arch_state s, ksArchState sa) \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState sa); cur_thread s = ksCurThread sa; idle_thread s = ksIdleThread sa; machine_state s = ksMachineState sa; work_units_completed s = ksWorkUnitsCompleted sa; domain_index s = ksDomScheduleIdx sa; domain_list s = ksDomSchedule sa; cur_domain s = ksCurDomain sa; domain_time s = ksDomainTime sa; is_aligned ptr 14; y < 0x1000; pde_relation (UCAST(32 \<rightarrow> 12) y) (ArchObj (PageDirectory pd)) (the (ksPSpace sa (ptr + (UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) y) << 2)))); dom (ksPSpace sa) = (\<Union>x\<in>dom (kheap s). fst ` obj_relation_cuts (the (kheap s x)) x)\<rbrakk> \<Longrightarrow> ptr + (y << 2) \<in> fst ` obj_relation_cuts (the (kheap s ptr)) ptr
 2. \<And>pd y. \<lbrakk>pspace_aligned s; pspace_distinct' sa; kheap s ptr = Some (ArchObj (PageDirectory pd)); ekheap_relation (ekheap s) (ksPSpace sa); sched_act_relation (scheduler_action s) (ksSchedulerAction sa); ready_queues_relation (ready_queues s) (ksReadyQueues sa); ghost_relation (kheap s) (gsUserPages sa) (gsCNodes sa); cdt_relation (swp (cte_wp_at (\<lambda>_. True)) s) (cdt s) (ctes_of sa); cdt_list_relation (cdt_list s) (cdt s) (ctes_of sa); revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) (ctes_of sa); (arch_state s, ksArchState sa) \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState sa); cur_thread s = ksCurThread sa; idle_thread s = ksIdleThread sa; machine_state s = ksMachineState sa; work_units_completed s = ksWorkUnitsCompleted sa; domain_index s = ksDomScheduleIdx sa; domain_list s = ksDomSchedule sa; cur_domain s = ksCurDomain sa; domain_time s = ksDomainTime sa; is_aligned ptr 14; y < 0x1000; pde_relation (UCAST(32 \<rightarrow> 12) y) (ArchObj (PageDirectory pd)) (the (ksPSpace sa (ptr + (UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) y) << 2)))); dom (ksPSpace sa) = (\<Union>x\<in>dom (kheap s). fst ` obj_relation_cuts (the (kheap s x)) x)\<rbrakk> \<Longrightarrow> ptr \<in> dom (kheap s)
 3. \<And>pd y. \<lbrakk>pspace_aligned s; pspace_distinct' sa; kheap s ptr = Some (ArchObj (PageDirectory pd)); ekheap_relation (ekheap s) (ksPSpace sa); sched_act_relation (scheduler_action s) (ksSchedulerAction sa); ready_queues_relation (ready_queues s) (ksReadyQueues sa); ghost_relation (kheap s) (gsUserPages sa) (gsCNodes sa); cdt_relation (swp (cte_wp_at (\<lambda>_. True)) s) (cdt s) (ctes_of sa); cdt_list_relation (cdt_list s) (cdt s) (ctes_of sa); revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) (ctes_of sa); (arch_state s, ksArchState sa) \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState sa); cur_thread s = ksCurThread sa; idle_thread s = ksIdleThread sa; machine_state s = ksMachineState sa; work_units_completed s = ksWorkUnitsCompleted sa; domain_index s = ksDomScheduleIdx sa; domain_list s = ksDomSchedule sa; cur_domain s = ksCurDomain sa; domain_time s = ksDomainTime sa; is_aligned ptr 14; y < 0x1000; pde_relation (UCAST(32 \<rightarrow> 12) y) (ArchObj (PageDirectory pd)) (the (ksPSpace sa (ptr + (UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) y) << 2)))); dom (ksPSpace sa) = pspace_dom (kheap s); ptr + (y << 2) \<in> dom (ksPSpace sa)\<rbrakk> \<Longrightarrow> \<exists>ko. ksPSpace sa (ptr + (y << 2)) = Some ko \<and> is_aligned (ptr + (y << 2)) (objBitsKO ko) \<and> koTypeOf ko = ArchT PDET \<and> ps_clear (ptr + (y << 2)) (objBitsKO ko) sa proof (prove)
goal (3 subgoals):
 1. \<And>pd y. \<lbrakk>pspace_aligned s; pspace_distinct' sa; kheap s ptr = Some (ArchObj (PageDirectory pd)); ekheap_relation (ekheap s) (ksPSpace sa); sched_act_relation (scheduler_action s) (ksSchedulerAction sa); ready_queues_relation (ready_queues s) (ksReadyQueues sa); ghost_relation (kheap s) (gsUserPages sa) (gsCNodes sa); cdt_relation (swp (cte_wp_at (\<lambda>_. True)) s) (cdt s) (ctes_of sa); cdt_list_relation (cdt_list s) (cdt s) (ctes_of sa); revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) (ctes_of sa); (arch_state s, ksArchState sa) \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState sa); cur_thread s = ksCurThread sa; idle_thread s = ksIdleThread sa; machine_state s = ksMachineState sa; work_units_completed s = ksWorkUnitsCompleted sa; domain_index s = ksDomScheduleIdx sa; domain_list s = ksDomSchedule sa; cur_domain s = ksCurDomain sa; domain_time s = ksDomainTime sa; is_aligned ptr 14; y < 0x1000; pde_relation (UCAST(32 \<rightarrow> 12) y) (ArchObj (PageDirectory pd)) (the (ksPSpace sa (ptr + (UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) y) << 2)))); dom (ksPSpace sa) = \<Union> {y. \<exists>x\<in>dom (kheap s). y = {y. \<exists>x\<in>obj_relation_cuts (the (kheap s x)) x. y = fst x}}\<rbrakk> \<Longrightarrow> \<exists>x. y << 2 = UCAST(12 \<rightarrow> 32) x << 2
 2. \<And>pd y. \<lbrakk>pspace_aligned s; pspace_distinct' sa; kheap s ptr = Some (ArchObj (PageDirectory pd)); ekheap_relation (ekheap s) (ksPSpace sa); sched_act_relation (scheduler_action s) (ksSchedulerAction sa); ready_queues_relation (ready_queues s) (ksReadyQueues sa); ghost_relation (kheap s) (gsUserPages sa) (gsCNodes sa); cdt_relation (swp (cte_wp_at (\<lambda>_. True)) s) (cdt s) (ctes_of sa); cdt_list_relation (cdt_list s) (cdt s) (ctes_of sa); revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) (ctes_of sa); (arch_state s, ksArchState sa) \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState sa); cur_thread s = ksCurThread sa; idle_thread s = ksIdleThread sa; machine_state s = ksMachineState sa; work_units_completed s = ksWorkUnitsCompleted sa; domain_index s = ksDomScheduleIdx sa; domain_list s = ksDomSchedule sa; cur_domain s = ksCurDomain sa; domain_time s = ksDomainTime sa; is_aligned ptr 14; y < 0x1000; pde_relation (UCAST(32 \<rightarrow> 12) y) (ArchObj (PageDirectory pd)) (the (ksPSpace sa (ptr + (UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) y) << 2)))); dom (ksPSpace sa) = (\<Union>x\<in>dom (kheap s). fst ` obj_relation_cuts (the (kheap s x)) x)\<rbrakk> \<Longrightarrow> ptr \<in> dom (kheap s)
 3. \<And>pd y. \<lbrakk>pspace_aligned s; pspace_distinct' sa; kheap s ptr = Some (ArchObj (PageDirectory pd)); ekheap_relation (ekheap s) (ksPSpace sa); sched_act_relation (scheduler_action s) (ksSchedulerAction sa); ready_queues_relation (ready_queues s) (ksReadyQueues sa); ghost_relation (kheap s) (gsUserPages sa) (gsCNodes sa); cdt_relation (swp (cte_wp_at (\<lambda>_. True)) s) (cdt s) (ctes_of sa); cdt_list_relation (cdt_list s) (cdt s) (ctes_of sa); revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) (ctes_of sa); (arch_state s, ksArchState sa) \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState sa); cur_thread s = ksCurThread sa; idle_thread s = ksIdleThread sa; machine_state s = ksMachineState sa; work_units_completed s = ksWorkUnitsCompleted sa; domain_index s = ksDomScheduleIdx sa; domain_list s = ksDomSchedule sa; cur_domain s = ksCurDomain sa; domain_time s = ksDomainTime sa; is_aligned ptr 14; y < 0x1000; pde_relation (UCAST(32 \<rightarrow> 12) y) (ArchObj (PageDirectory pd)) (the (ksPSpace sa (ptr + (UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) y) << 2)))); dom (ksPSpace sa) = pspace_dom (kheap s); ptr + (y << 2) \<in> dom (ksPSpace sa)\<rbrakk> \<Longrightarrow> \<exists>ko. ksPSpace sa (ptr + (y << 2)) = Some ko \<and> is_aligned (ptr + (y << 2)) (objBitsKO ko) \<and> koTypeOf ko = ArchT PDET \<and> ps_clear (ptr + (y << 2)) (objBitsKO ko) sa proof (prove)
goal (3 subgoals):
 1. \<And>pd y. \<lbrakk>pspace_aligned s; pspace_distinct' sa; kheap s ptr = Some (ArchObj (PageDirectory pd)); ekheap_relation (ekheap s) (ksPSpace sa); sched_act_relation (scheduler_action s) (ksSchedulerAction sa); ready_queues_relation (ready_queues s) (ksReadyQueues sa); ghost_relation (kheap s) (gsUserPages sa) (gsCNodes sa); cdt_relation (swp (cte_wp_at (\<lambda>_. True)) s) (cdt s) (ctes_of sa); cdt_list_relation (cdt_list s) (cdt s) (ctes_of sa); revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) (ctes_of sa); (arch_state s, ksArchState sa) \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState sa); cur_thread s = ksCurThread sa; idle_thread s = ksIdleThread sa; machine_state s = ksMachineState sa; work_units_completed s = ksWorkUnitsCompleted sa; domain_index s = ksDomScheduleIdx sa; domain_list s = ksDomSchedule sa; cur_domain s = ksCurDomain sa; domain_time s = ksDomainTime sa; is_aligned ptr 14; y < 0x1000; pde_relation (UCAST(32 \<rightarrow> 12) y) (ArchObj (PageDirectory pd)) (the (ksPSpace sa (ptr + (UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) y) << 2)))); dom (ksPSpace sa) = \<Union> {y. \<exists>x\<in>dom (kheap s). y = {y. \<exists>x\<in>obj_relation_cuts (the (kheap s x)) x. y = fst x}}\<rbrakk> \<Longrightarrow> y << 2 = UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) y) << 2
 2. \<And>pd y. \<lbrakk>pspace_aligned s; pspace_distinct' sa; kheap s ptr = Some (ArchObj (PageDirectory pd)); ekheap_relation (ekheap s) (ksPSpace sa); sched_act_relation (scheduler_action s) (ksSchedulerAction sa); ready_queues_relation (ready_queues s) (ksReadyQueues sa); ghost_relation (kheap s) (gsUserPages sa) (gsCNodes sa); cdt_relation (swp (cte_wp_at (\<lambda>_. True)) s) (cdt s) (ctes_of sa); cdt_list_relation (cdt_list s) (cdt s) (ctes_of sa); revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) (ctes_of sa); (arch_state s, ksArchState sa) \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState sa); cur_thread s = ksCurThread sa; idle_thread s = ksIdleThread sa; machine_state s = ksMachineState sa; work_units_completed s = ksWorkUnitsCompleted sa; domain_index s = ksDomScheduleIdx sa; domain_list s = ksDomSchedule sa; cur_domain s = ksCurDomain sa; domain_time s = ksDomainTime sa; is_aligned ptr 14; y < 0x1000; pde_relation (UCAST(32 \<rightarrow> 12) y) (ArchObj (PageDirectory pd)) (the (ksPSpace sa (ptr + (UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) y) << 2)))); dom (ksPSpace sa) = (\<Union>x\<in>dom (kheap s). fst ` obj_relation_cuts (the (kheap s x)) x)\<rbrakk> \<Longrightarrow> ptr \<in> dom (kheap s)
 3. \<And>pd y. \<lbrakk>pspace_aligned s; pspace_distinct' sa; kheap s ptr = Some (ArchObj (PageDirectory pd)); ekheap_relation (ekheap s) (ksPSpace sa); sched_act_relation (scheduler_action s) (ksSchedulerAction sa); ready_queues_relation (ready_queues s) (ksReadyQueues sa); ghost_relation (kheap s) (gsUserPages sa) (gsCNodes sa); cdt_relation (swp (cte_wp_at (\<lambda>_. True)) s) (cdt s) (ctes_of sa); cdt_list_relation (cdt_list s) (cdt s) (ctes_of sa); revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) (ctes_of sa); (arch_state s, ksArchState sa) \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState sa); cur_thread s = ksCurThread sa; idle_thread s = ksIdleThread sa; machine_state s = ksMachineState sa; work_units_completed s = ksWorkUnitsCompleted sa; domain_index s = ksDomScheduleIdx sa; domain_list s = ksDomSchedule sa; cur_domain s = ksCurDomain sa; domain_time s = ksDomainTime sa; is_aligned ptr 14; y < 0x1000; pde_relation (UCAST(32 \<rightarrow> 12) y) (ArchObj (PageDirectory pd)) (the (ksPSpace sa (ptr + (UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) y) << 2)))); dom (ksPSpace sa) = pspace_dom (kheap s); ptr + (y << 2) \<in> dom (ksPSpace sa)\<rbrakk> \<Longrightarrow> \<exists>ko. ksPSpace sa (ptr + (y << 2)) = Some ko \<and> is_aligned (ptr + (y << 2)) (objBitsKO ko) \<and> koTypeOf ko = ArchT PDET \<and> ps_clear (ptr + (y << 2)) (objBitsKO ko) sa proof (prove)
goal (2 subgoals):
 1. \<And>pd y. \<lbrakk>pspace_aligned s; pspace_distinct' sa; kheap s ptr = Some (ArchObj (PageDirectory pd)); ekheap_relation (ekheap s) (ksPSpace sa); sched_act_relation (scheduler_action s) (ksSchedulerAction sa); ready_queues_relation (ready_queues s) (ksReadyQueues sa); ghost_relation (kheap s) (gsUserPages sa) (gsCNodes sa); cdt_relation (swp (cte_wp_at (\<lambda>_. True)) s) (cdt s) (ctes_of sa); cdt_list_relation (cdt_list s) (cdt s) (ctes_of sa); revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) (ctes_of sa); (arch_state s, ksArchState sa) \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState sa); cur_thread s = ksCurThread sa; idle_thread s = ksIdleThread sa; machine_state s = ksMachineState sa; work_units_completed s = ksWorkUnitsCompleted sa; domain_index s = ksDomScheduleIdx sa; domain_list s = ksDomSchedule sa; cur_domain s = ksCurDomain sa; domain_time s = ksDomainTime sa; is_aligned ptr 14; y < 0x1000; pde_relation (UCAST(32 \<rightarrow> 12) y) (ArchObj (PageDirectory pd)) (the (ksPSpace sa (ptr + (UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) y) << 2)))); dom (ksPSpace sa) = (\<Union>x\<in>dom (kheap s). fst ` obj_relation_cuts (the (kheap s x)) x)\<rbrakk> \<Longrightarrow> ptr \<in> dom (kheap s)
 2. \<And>pd y. \<lbrakk>pspace_aligned s; pspace_distinct' sa; kheap s ptr = Some (ArchObj (PageDirectory pd)); ekheap_relation (ekheap s) (ksPSpace sa); sched_act_relation (scheduler_action s) (ksSchedulerAction sa); ready_queues_relation (ready_queues s) (ksReadyQueues sa); ghost_relation (kheap s) (gsUserPages sa) (gsCNodes sa); cdt_relation (swp (cte_wp_at (\<lambda>_. True)) s) (cdt s) (ctes_of sa); cdt_list_relation (cdt_list s) (cdt s) (ctes_of sa); revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) (ctes_of sa); (arch_state s, ksArchState sa) \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState sa); cur_thread s = ksCurThread sa; idle_thread s = ksIdleThread sa; machine_state s = ksMachineState sa; work_units_completed s = ksWorkUnitsCompleted sa; domain_index s = ksDomScheduleIdx sa; domain_list s = ksDomSchedule sa; cur_domain s = ksCurDomain sa; domain_time s = ksDomainTime sa; is_aligned ptr 14; y < 0x1000; pde_relation (UCAST(32 \<rightarrow> 12) y) (ArchObj (PageDirectory pd)) (the (ksPSpace sa (ptr + (UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) y) << 2)))); dom (ksPSpace sa) = pspace_dom (kheap s); ptr + (y << 2) \<in> dom (ksPSpace sa)\<rbrakk> \<Longrightarrow> \<exists>ko. ksPSpace sa (ptr + (y << 2)) = Some ko \<and> is_aligned (ptr + (y << 2)) (objBitsKO ko) \<and> koTypeOf ko = ArchT PDET \<and> ps_clear (ptr + (y << 2)) (objBitsKO ko) sa proof (prove)
goal (1 subgoal):
 1. \<And>pd y. \<lbrakk>pspace_aligned s; pspace_distinct' sa; kheap s ptr = Some (ArchObj (PageDirectory pd)); ekheap_relation (ekheap s) (ksPSpace sa); sched_act_relation (scheduler_action s) (ksSchedulerAction sa); ready_queues_relation (ready_queues s) (ksReadyQueues sa); ghost_relation (kheap s) (gsUserPages sa) (gsCNodes sa); cdt_relation (swp (cte_wp_at (\<lambda>_. True)) s) (cdt s) (ctes_of sa); cdt_list_relation (cdt_list s) (cdt s) (ctes_of sa); revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) (ctes_of sa); (arch_state s, ksArchState sa) \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState sa); cur_thread s = ksCurThread sa; idle_thread s = ksIdleThread sa; machine_state s = ksMachineState sa; work_units_completed s = ksWorkUnitsCompleted sa; domain_index s = ksDomScheduleIdx sa; domain_list s = ksDomSchedule sa; cur_domain s = ksCurDomain sa; domain_time s = ksDomainTime sa; is_aligned ptr 14; y < 0x1000; pde_relation (UCAST(32 \<rightarrow> 12) y) (ArchObj (PageDirectory pd)) (the (ksPSpace sa (ptr + (UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) y) << 2)))); dom (ksPSpace sa) = pspace_dom (kheap s); ptr + (y << 2) \<in> dom (ksPSpace sa)\<rbrakk> \<Longrightarrow> \<exists>ko. ksPSpace sa (ptr + (y << 2)) = Some ko \<and> is_aligned (ptr + (y << 2)) (objBitsKO ko) \<and> koTypeOf ko = ArchT PDET \<and> ps_clear (ptr + (y << 2)) (objBitsKO ko) sa proof (prove)
goal (1 subgoal):
 1. \<And>pd y. \<lbrakk>pspace_aligned s; pspace_distinct' sa; kheap s ptr = Some (ArchObj (PageDirectory pd)); ekheap_relation (ekheap s) (ksPSpace sa); sched_act_relation (scheduler_action s) (ksSchedulerAction sa); ready_queues_relation (ready_queues s) (ksReadyQueues sa); ghost_relation (kheap s) (gsUserPages sa) (gsCNodes sa); cdt_relation (swp (cte_wp_at (\<lambda>_. True)) s) (cdt s) (ctes_of sa); cdt_list_relation (cdt_list s) (cdt s) (ctes_of sa); revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) (ctes_of sa); (arch_state s, ksArchState sa) \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState sa); cur_thread s = ksCurThread sa; idle_thread s = ksIdleThread sa; machine_state s = ksMachineState sa; work_units_completed s = ksWorkUnitsCompleted sa; domain_index s = ksDomScheduleIdx sa; domain_list s = ksDomSchedule sa; cur_domain s = ksCurDomain sa; domain_time s = ksDomainTime sa; is_aligned ptr 14; y < 0x1000; pde_relation (UCAST(32 \<rightarrow> 12) y) (ArchObj (PageDirectory pd)) (the (ksPSpace sa (ptr + (UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) y) << 2)))); ptr + (y << 2) \<in> dom (ksPSpace sa)\<rbrakk> \<Longrightarrow> \<exists>ko. ksPSpace sa (ptr + (y << 2)) = Some ko \<and> is_aligned (ptr + (y << 2)) (objBitsKO ko) \<and> koTypeOf ko = ArchT PDET \<and> ps_clear (ptr + (y << 2)) (objBitsKO ko) sa proof (prove)
goal (1 subgoal):
 1. \<And>pd y. \<lbrakk>pspace_aligned s; pspace_distinct' sa; kheap s ptr = Some (ArchObj (PageDirectory pd)); ekheap_relation (ekheap s) (ksPSpace sa); sched_act_relation (scheduler_action s) (ksSchedulerAction sa); ready_queues_relation (ready_queues s) (ksReadyQueues sa); ghost_relation (kheap s) (gsUserPages sa) (gsCNodes sa); cdt_relation (swp (cte_wp_at (\<lambda>_. True)) s) (cdt s) (ctes_of sa); cdt_list_relation (cdt_list s) (cdt s) (ctes_of sa); revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) (ctes_of sa); (arch_state s, ksArchState sa) \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState sa); cur_thread s = ksCurThread sa; idle_thread s = ksIdleThread sa; machine_state s = ksMachineState sa; work_units_completed s = ksWorkUnitsCompleted sa; domain_index s = ksDomScheduleIdx sa; domain_list s = ksDomSchedule sa; cur_domain s = ksCurDomain sa; domain_time s = ksDomainTime sa; is_aligned ptr 14; y < 0x1000; pde_relation (UCAST(32 \<rightarrow> 12) y) (ArchObj (PageDirectory pd)) (the (ksPSpace sa (ptr + (UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) y) << 2)))); ptr + (y << 2) \<in> dom (ksPSpace sa); is_aligned ptr (obj_bits (ArchObj (PageDirectory pd)))\<rbrakk> \<Longrightarrow> \<exists>ko. ksPSpace sa (ptr + (y << 2)) = Some ko \<and> is_aligned (ptr + (y << 2)) (objBitsKO ko) \<and> koTypeOf ko = ArchT PDET \<and> ps_clear (ptr + (y << 2)) (objBitsKO ko) sa proof (prove)
goal (1 subgoal):
 1. \<And>pd y ya. \<lbrakk>pspace_aligned s; pspace_distinct' sa; kheap s ptr = Some (ArchObj (PageDirectory pd)); ekheap_relation (ekheap s) (ksPSpace sa); sched_act_relation (scheduler_action s) (ksSchedulerAction sa); ready_queues_relation (ready_queues s) (ksReadyQueues sa); ghost_relation (kheap s) (gsUserPages sa) (gsCNodes sa); cdt_relation (swp (cte_wp_at (\<lambda>_. True)) s) (cdt s) (ctes_of sa); cdt_list_relation (cdt_list s) (cdt s) (ctes_of sa); revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) (ctes_of sa); (arch_state s, ksArchState sa) \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState sa); cur_thread s = ksCurThread sa; idle_thread s = ksIdleThread sa; machine_state s = ksMachineState sa; work_units_completed s = ksWorkUnitsCompleted sa; domain_index s = ksDomScheduleIdx sa; domain_list s = ksDomSchedule sa; cur_domain s = ksCurDomain sa; domain_time s = ksDomainTime sa; is_aligned ptr 14; y < 0x1000; pde_relation (UCAST(32 \<rightarrow> 12) y) (ArchObj (PageDirectory pd)) ya; ksPSpace sa (ptr + (y << 2)) = Some ya\<rbrakk> \<Longrightarrow> is_aligned (ptr + (y << 2)) (objBitsKO ya) \<and> koTypeOf ya = ArchT PDET \<and> ps_clear (ptr + (y << 2)) (objBitsKO ya) sa proof (prove)
goal (1 subgoal):
 1. \<And>pd y ya. \<lbrakk>pspace_aligned s; pspace_distinct' sa; kheap s ptr = Some (ArchObj (PageDirectory pd)); ekheap_relation (ekheap s) (ksPSpace sa); sched_act_relation (scheduler_action s) (ksSchedulerAction sa); ready_queues_relation (ready_queues s) (ksReadyQueues sa); ghost_relation (kheap s) (gsUserPages sa) (gsCNodes sa); cdt_relation (swp (cte_wp_at (\<lambda>_. True)) s) (cdt s) (ctes_of sa); cdt_list_relation (cdt_list s) (cdt s) (ctes_of sa); revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) (ctes_of sa); (arch_state s, ksArchState sa) \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState sa); cur_thread s = ksCurThread sa; idle_thread s = ksIdleThread sa; machine_state s = ksMachineState sa; work_units_completed s = ksWorkUnitsCompleted sa; domain_index s = ksDomScheduleIdx sa; domain_list s = ksDomSchedule sa; cur_domain s = ksCurDomain sa; domain_time s = ksDomainTime sa; is_aligned ptr 14; y < 0x1000; ksPSpace sa (ptr + (y << 2)) = Some ya; \<exists>pde. ya = KOArch (KOPDE pde)\<rbrakk> \<Longrightarrow> is_aligned (ptr + (y << 2)) (objBitsKO ya) \<and> koTypeOf ya = ArchT PDET \<and> ps_clear (ptr + (y << 2)) (objBitsKO ya) sa proof (prove)
goal (1 subgoal):
 1. \<And>pd y ya. \<lbrakk>pspace_aligned s; pspace_distinct' sa; kheap s ptr = Some (ArchObj (PageDirectory pd)); ekheap_relation (ekheap s) (ksPSpace sa); sched_act_relation (scheduler_action s) (ksSchedulerAction sa); ready_queues_relation (ready_queues s) (ksReadyQueues sa); ghost_relation (kheap s) (gsUserPages sa) (gsCNodes sa); cdt_relation (swp (cte_wp_at (\<lambda>_. True)) s) (cdt s) (ctes_of sa); cdt_list_relation (cdt_list s) (cdt s) (ctes_of sa); revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) (ctes_of sa); (arch_state s, ksArchState sa) \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState sa); cur_thread s = ksCurThread sa; idle_thread s = ksIdleThread sa; machine_state s = ksMachineState sa; work_units_completed s = ksWorkUnitsCompleted sa; domain_index s = ksDomScheduleIdx sa; domain_list s = ksDomSchedule sa; cur_domain s = ksCurDomain sa; domain_time s = ksDomainTime sa; is_aligned ptr 14; y < 0x1000; \<exists>pde. ya = KOArch (KOPDE pde); ps_clear (ptr + (y << 2)) (objBitsKO ya) sa\<rbrakk> \<Longrightarrow> is_aligned (ptr + (y << 2)) (objBitsKO ya) \<and> koTypeOf ya = ArchT PDET \<and> ps_clear (ptr + (y << 2)) (objBitsKO ya) sa proof (prove)
goal (1 subgoal):
 1. \<And>pd y. \<lbrakk>pspace_aligned s; pspace_distinct' sa; kheap s ptr = Some (ArchObj (PageDirectory pd)); ekheap_relation (ekheap s) (ksPSpace sa); sched_act_relation (scheduler_action s) (ksSchedulerAction sa); ready_queues_relation (ready_queues s) (ksReadyQueues sa); ghost_relation (kheap s) (gsUserPages sa) (gsCNodes sa); cdt_relation (swp (cte_wp_at (\<lambda>_. True)) s) (cdt s) (ctes_of sa); cdt_list_relation (cdt_list s) (cdt s) (ctes_of sa); revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) (ctes_of sa); (arch_state s, ksArchState sa) \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState sa); cur_thread s = ksCurThread sa; idle_thread s = ksIdleThread sa; machine_state s = ksMachineState sa; work_units_completed s = ksWorkUnitsCompleted sa; domain_index s = ksDomScheduleIdx sa; domain_list s = ksDomSchedule sa; cur_domain s = ksCurDomain sa; domain_time s = ksDomainTime sa; is_aligned ptr 14; y < 0x1000; ps_clear (ptr + (y << 2)) pdeBits sa\<rbrakk> \<Longrightarrow> is_aligned (ptr + (y << 2)) pdeBits proof (prove)
goal (2 subgoals):
 1. \<And>pd y. \<lbrakk>pspace_aligned s; pspace_distinct' sa; kheap s ptr = Some (ArchObj (PageDirectory pd)); ekheap_relation (ekheap s) (ksPSpace sa); sched_act_relation (scheduler_action s) (ksSchedulerAction sa); ready_queues_relation (ready_queues s) (ksReadyQueues sa); ghost_relation (kheap s) (gsUserPages sa) (gsCNodes sa); cdt_relation (swp (cte_wp_at (\<lambda>_. True)) s) (cdt s) (ctes_of sa); cdt_list_relation (cdt_list s) (cdt s) (ctes_of sa); revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) (ctes_of sa); (arch_state s, ksArchState sa) \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState sa); cur_thread s = ksCurThread sa; idle_thread s = ksIdleThread sa; machine_state s = ksMachineState sa; work_units_completed s = ksWorkUnitsCompleted sa; domain_index s = ksDomScheduleIdx sa; domain_list s = ksDomSchedule sa; cur_domain s = ksCurDomain sa; domain_time s = ksDomainTime sa; is_aligned ptr 14; y < 0x1000; ps_clear (ptr + (y << 2)) pdeBits sa\<rbrakk> \<Longrightarrow> is_aligned (ptr + (y << 2)) (?x71 pd y)
 2. \<And>pd y. \<lbrakk>pspace_aligned s; pspace_distinct' sa; kheap s ptr = Some (ArchObj (PageDirectory pd)); ekheap_relation (ekheap s) (ksPSpace sa); sched_act_relation (scheduler_action s) (ksSchedulerAction sa); ready_queues_relation (ready_queues s) (ksReadyQueues sa); ghost_relation (kheap s) (gsUserPages sa) (gsCNodes sa); cdt_relation (swp (cte_wp_at (\<lambda>_. True)) s) (cdt s) (ctes_of sa); cdt_list_relation (cdt_list s) (cdt s) (ctes_of sa); revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) (ctes_of sa); (arch_state s, ksArchState sa) \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState sa); cur_thread s = ksCurThread sa; idle_thread s = ksIdleThread sa; machine_state s = ksMachineState sa; work_units_completed s = ksWorkUnitsCompleted sa; domain_index s = ksDomScheduleIdx sa; domain_list s = ksDomSchedule sa; cur_domain s = ksCurDomain sa; domain_time s = ksDomainTime sa; is_aligned ptr 14; y < 0x1000; ps_clear (ptr + (y << 2)) pdeBits sa\<rbrakk> \<Longrightarrow> pdeBits \<le> ?x71 pd y proof (prove)
goal (3 subgoals):
 1. \<And>pd y. \<lbrakk>pspace_aligned s; pspace_distinct' sa; kheap s ptr = Some (ArchObj (PageDirectory pd)); ekheap_relation (ekheap s) (ksPSpace sa); sched_act_relation (scheduler_action s) (ksSchedulerAction sa); ready_queues_relation (ready_queues s) (ksReadyQueues sa); ghost_relation (kheap s) (gsUserPages sa) (gsCNodes sa); cdt_relation (swp (cte_wp_at (\<lambda>_. True)) s) (cdt s) (ctes_of sa); cdt_list_relation (cdt_list s) (cdt s) (ctes_of sa); revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) (ctes_of sa); (arch_state s, ksArchState sa) \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState sa); cur_thread s = ksCurThread sa; idle_thread s = ksIdleThread sa; machine_state s = ksMachineState sa; work_units_completed s = ksWorkUnitsCompleted sa; domain_index s = ksDomScheduleIdx sa; domain_list s = ksDomSchedule sa; cur_domain s = ksCurDomain sa; domain_time s = ksDomainTime sa; y < 0x1000; ps_clear (ptr + (y << 2)) pdeBits sa\<rbrakk> \<Longrightarrow> is_aligned (y << 2) (?x71 pd y)
 2. \<And>pd y. \<lbrakk>pspace_aligned s; pspace_distinct' sa; kheap s ptr = Some (ArchObj (PageDirectory pd)); ekheap_relation (ekheap s) (ksPSpace sa); sched_act_relation (scheduler_action s) (ksSchedulerAction sa); ready_queues_relation (ready_queues s) (ksReadyQueues sa); ghost_relation (kheap s) (gsUserPages sa) (gsCNodes sa); cdt_relation (swp (cte_wp_at (\<lambda>_. True)) s) (cdt s) (ctes_of sa); cdt_list_relation (cdt_list s) (cdt s) (ctes_of sa); revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) (ctes_of sa); (arch_state s, ksArchState sa) \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState sa); cur_thread s = ksCurThread sa; idle_thread s = ksIdleThread sa; machine_state s = ksMachineState sa; work_units_completed s = ksWorkUnitsCompleted sa; domain_index s = ksDomScheduleIdx sa; domain_list s = ksDomSchedule sa; cur_domain s = ksCurDomain sa; domain_time s = ksDomainTime sa; y < 0x1000; ps_clear (ptr + (y << 2)) pdeBits sa\<rbrakk> \<Longrightarrow> ?x71 pd y \<le> 14
 3. \<And>pd y. \<lbrakk>pspace_aligned s; pspace_distinct' sa; kheap s ptr = Some (ArchObj (PageDirectory pd)); ekheap_relation (ekheap s) (ksPSpace sa); sched_act_relation (scheduler_action s) (ksSchedulerAction sa); ready_queues_relation (ready_queues s) (ksReadyQueues sa); ghost_relation (kheap s) (gsUserPages sa) (gsCNodes sa); cdt_relation (swp (cte_wp_at (\<lambda>_. True)) s) (cdt s) (ctes_of sa); cdt_list_relation (cdt_list s) (cdt s) (ctes_of sa); revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) (ctes_of sa); (arch_state s, ksArchState sa) \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState sa); cur_thread s = ksCurThread sa; idle_thread s = ksIdleThread sa; machine_state s = ksMachineState sa; work_units_completed s = ksWorkUnitsCompleted sa; domain_index s = ksDomScheduleIdx sa; domain_list s = ksDomSchedule sa; cur_domain s = ksCurDomain sa; domain_time s = ksDomainTime sa; is_aligned ptr 14; y < 0x1000; ps_clear (ptr + (y << 2)) pdeBits sa\<rbrakk> \<Longrightarrow> pdeBits \<le> ?x71 pd y proof (prove)
goal (2 subgoals):
 1. \<And>pd y. \<lbrakk>pspace_aligned s; pspace_distinct' sa; kheap s ptr = Some (ArchObj (PageDirectory pd)); ekheap_relation (ekheap s) (ksPSpace sa); sched_act_relation (scheduler_action s) (ksSchedulerAction sa); ready_queues_relation (ready_queues s) (ksReadyQueues sa); ghost_relation (kheap s) (gsUserPages sa) (gsCNodes sa); cdt_relation (swp (cte_wp_at (\<lambda>_. True)) s) (cdt s) (ctes_of sa); cdt_list_relation (cdt_list s) (cdt s) (ctes_of sa); revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) (ctes_of sa); (arch_state s, ksArchState sa) \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState sa); cur_thread s = ksCurThread sa; idle_thread s = ksIdleThread sa; machine_state s = ksMachineState sa; work_units_completed s = ksWorkUnitsCompleted sa; domain_index s = ksDomScheduleIdx sa; domain_list s = ksDomSchedule sa; cur_domain s = ksCurDomain sa; domain_time s = ksDomainTime sa; y < 0x1000; ps_clear (ptr + (y << 2)) pdeBits sa\<rbrakk> \<Longrightarrow> 2 \<le> 14
 2. \<And>pd y. \<lbrakk>pspace_aligned s; pspace_distinct' sa; kheap s ptr = Some (ArchObj (PageDirectory pd)); ekheap_relation (ekheap s) (ksPSpace sa); sched_act_relation (scheduler_action s) (ksSchedulerAction sa); ready_queues_relation (ready_queues s) (ksReadyQueues sa); ghost_relation (kheap s) (gsUserPages sa) (gsCNodes sa); cdt_relation (swp (cte_wp_at (\<lambda>_. True)) s) (cdt s) (ctes_of sa); cdt_list_relation (cdt_list s) (cdt s) (ctes_of sa); revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) (ctes_of sa); (arch_state s, ksArchState sa) \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState sa); cur_thread s = ksCurThread sa; idle_thread s = ksIdleThread sa; machine_state s = ksMachineState sa; work_units_completed s = ksWorkUnitsCompleted sa; domain_index s = ksDomScheduleIdx sa; domain_list s = ksDomSchedule sa; cur_domain s = ksCurDomain sa; domain_time s = ksDomainTime sa; is_aligned ptr 14; y < 0x1000; ps_clear (ptr + (y << 2)) pdeBits sa\<rbrakk> \<Longrightarrow> pdeBits \<le> 2 proof (prove)
goal (1 subgoal):
 1. \<And>pd y. \<lbrakk>pspace_aligned s; pspace_distinct' sa; kheap s ptr = Some (ArchObj (PageDirectory pd)); ekheap_relation (ekheap s) (ksPSpace sa); sched_act_relation (scheduler_action s) (ksSchedulerAction sa); ready_queues_relation (ready_queues s) (ksReadyQueues sa); ghost_relation (kheap s) (gsUserPages sa) (gsCNodes sa); cdt_relation (swp (cte_wp_at (\<lambda>_. True)) s) (cdt s) (ctes_of sa); cdt_list_relation (cdt_list s) (cdt s) (ctes_of sa); revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) (ctes_of sa); (arch_state s, ksArchState sa) \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState sa); cur_thread s = ksCurThread sa; idle_thread s = ksIdleThread sa; machine_state s = ksMachineState sa; work_units_completed s = ksWorkUnitsCompleted sa; domain_index s = ksDomScheduleIdx sa; domain_list s = ksDomSchedule sa; cur_domain s = ksCurDomain sa; domain_time s = ksDomainTime sa; is_aligned ptr 14; y < 0x1000; ps_clear (ptr + (y << 2)) pdeBits sa\<rbrakk> \<Longrightarrow> pdeBits \<le> 2 proof (prove)
goal:
No subgoals!