theory ArchAcc_R

lemma page_table_at_state_relation:
  "\<lbrakk>page_table_at (ptrFromPAddr ptr) s; pspace_aligned s;
     (s, sa) \<in> state_relation;pspace_distinct' sa\<rbrakk>
  \<Longrightarrow> page_table_at' (ptrFromPAddr ptr) sa" apply (clarsimp simp:page_table_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:ptrFromPAddr_def ptBits_def pageBits_def pteBits_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 + pptrBaseOffset + (y << 2)) \<in> dom (ksPSpace sa)") prefer 2 apply (clarsimp simp: pspace_dom_def) apply (rule_tac x = "ptr + pptrBaseOffset" 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 pte_relation_must_pte) 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: pteBits_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>typ_at (AArch APageTable) (ptrFromPAddr ptr) s; pspace_aligned s; (s, sa) \<in> state_relation; pspace_distinct' sa\<rbrakk> \<Longrightarrow> page_table_at' (ptrFromPAddr ptr) sa proof (prove)
goal (1 subgoal):
 1. \<And>pt. \<lbrakk>pspace_aligned s; pspace_distinct' sa; pspace_relation (kheap s) (ksPSpace sa); kheap s (ptrFromPAddr ptr) = Some (ArchObj (PageTable pt)); 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 (ptrFromPAddr ptr) ptBits \<and> (\<forall>y<0x100. pte_at' (ptrFromPAddr ptr + (y << 2)) sa) proof (prove)
goal (1 subgoal):
 1. \<And>pt. \<lbrakk>pspace_aligned s; pspace_distinct' sa; kheap s (ptrFromPAddr ptr) = Some (ArchObj (PageTable pt)); 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 (ptrFromPAddr ptr) ptBits \<and> (\<forall>y<0x100. pte_at' (ptrFromPAddr ptr + (y << 2)) sa) proof (prove)
goal (2 subgoals):
 1. \<And>pt. \<lbrakk>pspace_aligned s; pspace_distinct' sa; kheap s (ptrFromPAddr ptr) = Some (ArchObj (PageTable pt)); 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 pt \<in> dom (kheap s)
 2. \<And>pt. \<lbrakk>pspace_aligned s; pspace_distinct' sa; kheap s (ptrFromPAddr ptr) = Some (ArchObj (PageTable pt)); 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 pt))) (?x25 pt). case x of (y, P) \<Rightarrow> P (the (kheap s (?x25 pt))) (the (ksPSpace sa y))\<rbrakk> \<Longrightarrow> is_aligned (ptrFromPAddr ptr) ptBits \<and> (\<forall>y<0x100. pte_at' (ptrFromPAddr ptr + (y << 2)) sa) proof (prove)
goal (1 subgoal):
 1. \<And>pt. \<lbrakk>pspace_aligned s; pspace_distinct' sa; kheap s (ptrFromPAddr ptr) = Some (ArchObj (PageTable pt)); 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 (ptrFromPAddr ptr))) (ptrFromPAddr ptr). case x of (y, P) \<Rightarrow> P (the (kheap s (ptrFromPAddr ptr))) (the (ksPSpace sa y))\<rbrakk> \<Longrightarrow> is_aligned (ptrFromPAddr ptr) ptBits \<and> (\<forall>y<0x100. pte_at' (ptrFromPAddr ptr + (y << 2)) sa) proof (prove)
goal (1 subgoal):
 1. \<And>pt. \<lbrakk>pspace_aligned s; pspace_distinct' sa; kheap s (ptrFromPAddr ptr) = Some (ArchObj (PageTable pt)); 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. pte_relation x (ArchObj (PageTable pt)) (the (ksPSpace sa (ptrFromPAddr ptr + (UCAST(8 \<rightarrow> 32) x << 2))))\<rbrakk> \<Longrightarrow> is_aligned (ptrFromPAddr ptr) ptBits \<and> (\<forall>y<0x100. pte_at' (ptrFromPAddr ptr + (y << 2)) sa) proof (prove)
goal (1 subgoal):
 1. \<And>pt. \<lbrakk>pspace_aligned s; pspace_distinct' sa; kheap s (ptrFromPAddr ptr) = Some (ArchObj (PageTable pt)); 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. pte_relation x (ArchObj (PageTable pt)) (the (ksPSpace sa (ptrFromPAddr ptr + (UCAST(8 \<rightarrow> 32) x << 2)))); is_aligned (ptrFromPAddr ptr) (obj_bits (ArchObj (PageTable pt)))\<rbrakk> \<Longrightarrow> is_aligned (ptrFromPAddr ptr) ptBits \<and> (\<forall>y<0x100. pte_at' (ptrFromPAddr ptr + (y << 2)) sa) proof (prove)
goal (1 subgoal):
 1. \<And>pt. \<lbrakk>pspace_aligned s; pspace_distinct' sa; kheap s (ptr + pptrBaseOffset) = Some (ArchObj (PageTable pt)); 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. pte_relation x (ArchObj (PageTable pt)) (the (ksPSpace sa (ptr + pptrBaseOffset + (UCAST(8 \<rightarrow> 32) x << 2)))); is_aligned (ptr + pptrBaseOffset) 10\<rbrakk> \<Longrightarrow> \<forall>y<0x100. pte_at' (ptr + pptrBaseOffset + (y << 2)) sa proof (prove)
goal (1 subgoal):
 1. \<And>pt y. \<lbrakk>pspace_aligned s; pspace_distinct' sa; kheap s (ptr + pptrBaseOffset) = Some (ArchObj (PageTable pt)); 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. pte_relation x (ArchObj (PageTable pt)) (the (ksPSpace sa (ptr + pptrBaseOffset + (UCAST(8 \<rightarrow> 32) x << 2)))); is_aligned (ptr + pptrBaseOffset) 10; y < 0x100\<rbrakk> \<Longrightarrow> pte_at' (ptr + pptrBaseOffset + (y << 2)) sa proof (prove)
goal (1 subgoal):
 1. \<And>pt y. \<lbrakk>pspace_aligned s; pspace_distinct' sa; kheap s (ptr + pptrBaseOffset) = Some (ArchObj (PageTable pt)); 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 + pptrBaseOffset) 10; y < 0x100; pte_relation (UCAST(32 \<rightarrow> 8) y) (ArchObj (PageTable pt)) (the (ksPSpace sa (ptr + pptrBaseOffset + (UCAST(8 \<rightarrow> 32) (UCAST(32 \<rightarrow> 8) y) << 2))))\<rbrakk> \<Longrightarrow> pte_at' (ptr + pptrBaseOffset + (y << 2)) sa proof (prove)
goal (1 subgoal):
 1. \<And>pt y. \<lbrakk>pspace_aligned s; pspace_distinct' sa; kheap s (ptr + pptrBaseOffset) = Some (ArchObj (PageTable pt)); 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 + pptrBaseOffset) 10; y < 0x100; pte_relation (UCAST(32 \<rightarrow> 8) y) (ArchObj (PageTable pt)) (the (ksPSpace sa (ptr + pptrBaseOffset + (UCAST(8 \<rightarrow> 32) (UCAST(32 \<rightarrow> 8) y) << 2)))); dom (ksPSpace sa) = pspace_dom (kheap s)\<rbrakk> \<Longrightarrow> pte_at' (ptr + pptrBaseOffset + (y << 2)) sa proof (prove)
goal (1 subgoal):
 1. \<And>pt y. \<lbrakk>pspace_aligned s; pspace_distinct' sa; kheap s (ptr + pptrBaseOffset) = Some (ArchObj (PageTable pt)); 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 + pptrBaseOffset) 10; y < 0x100; pte_relation (UCAST(32 \<rightarrow> 8) y) (ArchObj (PageTable pt)) (the (ksPSpace sa (ptr + pptrBaseOffset + (UCAST(8 \<rightarrow> 32) (UCAST(32 \<rightarrow> 8) y) << 2)))); dom (ksPSpace sa) = pspace_dom (kheap s)\<rbrakk> \<Longrightarrow> \<exists>ko. ksPSpace sa (ptr + pptrBaseOffset + (y << 2)) = Some ko \<and> is_aligned (ptr + pptrBaseOffset + (y << 2)) (objBitsKO ko) \<and> koTypeOf ko = ArchT PTET \<and> ps_clear (ptr + pptrBaseOffset + (y << 2)) (objBitsKO ko) sa proof (prove)
goal (2 subgoals):
 1. \<And>pt y. \<lbrakk>pspace_aligned s; pspace_distinct' sa; kheap s (ptr + pptrBaseOffset) = Some (ArchObj (PageTable pt)); 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 + pptrBaseOffset) 10; y < 0x100; pte_relation (UCAST(32 \<rightarrow> 8) y) (ArchObj (PageTable pt)) (the (ksPSpace sa (ptr + pptrBaseOffset + (UCAST(8 \<rightarrow> 32) (UCAST(32 \<rightarrow> 8) y) << 2)))); dom (ksPSpace sa) = pspace_dom (kheap s); ptr + pptrBaseOffset + (y << 2) \<in> dom (ksPSpace sa)\<rbrakk> \<Longrightarrow> \<exists>ko. ksPSpace sa (ptr + pptrBaseOffset + (y << 2)) = Some ko \<and> is_aligned (ptr + pptrBaseOffset + (y << 2)) (objBitsKO ko) \<and> koTypeOf ko = ArchT PTET \<and> ps_clear (ptr + pptrBaseOffset + (y << 2)) (objBitsKO ko) sa
 2. \<And>pt y. \<lbrakk>pspace_aligned s; pspace_distinct' sa; kheap s (ptr + pptrBaseOffset) = Some (ArchObj (PageTable pt)); 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 + pptrBaseOffset) 10; y < 0x100; pte_relation (UCAST(32 \<rightarrow> 8) y) (ArchObj (PageTable pt)) (the (ksPSpace sa (ptr + pptrBaseOffset + (UCAST(8 \<rightarrow> 32) (UCAST(32 \<rightarrow> 8) y) << 2)))); dom (ksPSpace sa) = pspace_dom (kheap s)\<rbrakk> \<Longrightarrow> ptr + pptrBaseOffset + (y << 2) \<in> dom (ksPSpace sa) proof (prove)
goal (2 subgoals):
 1. \<And>pt y. \<lbrakk>pspace_aligned s; pspace_distinct' sa; kheap s (ptr + pptrBaseOffset) = Some (ArchObj (PageTable pt)); 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 + pptrBaseOffset) 10; y < 0x100; pte_relation (UCAST(32 \<rightarrow> 8) y) (ArchObj (PageTable pt)) (the (ksPSpace sa (ptr + pptrBaseOffset + (UCAST(8 \<rightarrow> 32) (UCAST(32 \<rightarrow> 8) y) << 2)))); dom (ksPSpace sa) = pspace_dom (kheap s)\<rbrakk> \<Longrightarrow> ptr + pptrBaseOffset + (y << 2) \<in> dom (ksPSpace sa)
 2. \<And>pt y. \<lbrakk>pspace_aligned s; pspace_distinct' sa; kheap s (ptr + pptrBaseOffset) = Some (ArchObj (PageTable pt)); 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 + pptrBaseOffset) 10; y < 0x100; pte_relation (UCAST(32 \<rightarrow> 8) y) (ArchObj (PageTable pt)) (the (ksPSpace sa (ptr + pptrBaseOffset + (UCAST(8 \<rightarrow> 32) (UCAST(32 \<rightarrow> 8) y) << 2)))); dom (ksPSpace sa) = pspace_dom (kheap s); ptr + pptrBaseOffset + (y << 2) \<in> dom (ksPSpace sa)\<rbrakk> \<Longrightarrow> \<exists>ko. ksPSpace sa (ptr + pptrBaseOffset + (y << 2)) = Some ko \<and> is_aligned (ptr + pptrBaseOffset + (y << 2)) (objBitsKO ko) \<and> koTypeOf ko = ArchT PTET \<and> ps_clear (ptr + pptrBaseOffset + (y << 2)) (objBitsKO ko) sa proof (prove)
goal (2 subgoals):
 1. \<And>pt y. \<lbrakk>pspace_aligned s; pspace_distinct' sa; kheap s (ptr + pptrBaseOffset) = Some (ArchObj (PageTable pt)); 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 + pptrBaseOffset) 10; y < 0x100; pte_relation (UCAST(32 \<rightarrow> 8) y) (ArchObj (PageTable pt)) (the (ksPSpace sa (ptr + pptrBaseOffset + (UCAST(8 \<rightarrow> 32) (UCAST(32 \<rightarrow> 8) 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 + pptrBaseOffset + (y << 2) \<in> fst ` obj_relation_cuts (the (kheap s x)) x
 2. \<And>pt y. \<lbrakk>pspace_aligned s; pspace_distinct' sa; kheap s (ptr + pptrBaseOffset) = Some (ArchObj (PageTable pt)); 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 + pptrBaseOffset) 10; y < 0x100; pte_relation (UCAST(32 \<rightarrow> 8) y) (ArchObj (PageTable pt)) (the (ksPSpace sa (ptr + pptrBaseOffset + (UCAST(8 \<rightarrow> 32) (UCAST(32 \<rightarrow> 8) y) << 2)))); dom (ksPSpace sa) = pspace_dom (kheap s); ptr + pptrBaseOffset + (y << 2) \<in> dom (ksPSpace sa)\<rbrakk> \<Longrightarrow> \<exists>ko. ksPSpace sa (ptr + pptrBaseOffset + (y << 2)) = Some ko \<and> is_aligned (ptr + pptrBaseOffset + (y << 2)) (objBitsKO ko) \<and> koTypeOf ko = ArchT PTET \<and> ps_clear (ptr + pptrBaseOffset + (y << 2)) (objBitsKO ko) sa proof (prove)
goal (3 subgoals):
 1. \<And>pt y. \<lbrakk>pspace_aligned s; pspace_distinct' sa; kheap s (ptr + pptrBaseOffset) = Some (ArchObj (PageTable pt)); 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 + pptrBaseOffset) 10; y < 0x100; pte_relation (UCAST(32 \<rightarrow> 8) y) (ArchObj (PageTable pt)) (the (ksPSpace sa (ptr + pptrBaseOffset + (UCAST(8 \<rightarrow> 32) (UCAST(32 \<rightarrow> 8) y) << 2)))); dom (ksPSpace sa) = (\<Union>x\<in>dom (kheap s). fst ` obj_relation_cuts (the (kheap s x)) x)\<rbrakk> \<Longrightarrow> ptr + pptrBaseOffset + (y << 2) \<in> fst ` obj_relation_cuts (the (kheap s (ptr + pptrBaseOffset))) (ptr + pptrBaseOffset)
 2. \<And>pt y. \<lbrakk>pspace_aligned s; pspace_distinct' sa; kheap s (ptr + pptrBaseOffset) = Some (ArchObj (PageTable pt)); 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 + pptrBaseOffset) 10; y < 0x100; pte_relation (UCAST(32 \<rightarrow> 8) y) (ArchObj (PageTable pt)) (the (ksPSpace sa (ptr + pptrBaseOffset + (UCAST(8 \<rightarrow> 32) (UCAST(32 \<rightarrow> 8) y) << 2)))); dom (ksPSpace sa) = (\<Union>x\<in>dom (kheap s). fst ` obj_relation_cuts (the (kheap s x)) x)\<rbrakk> \<Longrightarrow> ptr + pptrBaseOffset \<in> dom (kheap s)
 3. \<And>pt y. \<lbrakk>pspace_aligned s; pspace_distinct' sa; kheap s (ptr + pptrBaseOffset) = Some (ArchObj (PageTable pt)); 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 + pptrBaseOffset) 10; y < 0x100; pte_relation (UCAST(32 \<rightarrow> 8) y) (ArchObj (PageTable pt)) (the (ksPSpace sa (ptr + pptrBaseOffset + (UCAST(8 \<rightarrow> 32) (UCAST(32 \<rightarrow> 8) y) << 2)))); dom (ksPSpace sa) = pspace_dom (kheap s); ptr + pptrBaseOffset + (y << 2) \<in> dom (ksPSpace sa)\<rbrakk> \<Longrightarrow> \<exists>ko. ksPSpace sa (ptr + pptrBaseOffset + (y << 2)) = Some ko \<and> is_aligned (ptr + pptrBaseOffset + (y << 2)) (objBitsKO ko) \<and> koTypeOf ko = ArchT PTET \<and> ps_clear (ptr + pptrBaseOffset + (y << 2)) (objBitsKO ko) sa proof (prove)
goal (3 subgoals):
 1. \<And>pt y. \<lbrakk>pspace_aligned s; pspace_distinct' sa; kheap s (ptr + pptrBaseOffset) = Some (ArchObj (PageTable pt)); 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 + pptrBaseOffset) 10; y < 0x100; pte_relation (UCAST(32 \<rightarrow> 8) y) (ArchObj (PageTable pt)) (the (ksPSpace sa (ptr + pptrBaseOffset + (UCAST(8 \<rightarrow> 32) (UCAST(32 \<rightarrow> 8) 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(8 \<rightarrow> 32) x << 2
 2. \<And>pt y. \<lbrakk>pspace_aligned s; pspace_distinct' sa; kheap s (ptr + pptrBaseOffset) = Some (ArchObj (PageTable pt)); 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 + pptrBaseOffset) 10; y < 0x100; pte_relation (UCAST(32 \<rightarrow> 8) y) (ArchObj (PageTable pt)) (the (ksPSpace sa (ptr + pptrBaseOffset + (UCAST(8 \<rightarrow> 32) (UCAST(32 \<rightarrow> 8) y) << 2)))); dom (ksPSpace sa) = (\<Union>x\<in>dom (kheap s). fst ` obj_relation_cuts (the (kheap s x)) x)\<rbrakk> \<Longrightarrow> ptr + pptrBaseOffset \<in> dom (kheap s)
 3. \<And>pt y. \<lbrakk>pspace_aligned s; pspace_distinct' sa; kheap s (ptr + pptrBaseOffset) = Some (ArchObj (PageTable pt)); 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 + pptrBaseOffset) 10; y < 0x100; pte_relation (UCAST(32 \<rightarrow> 8) y) (ArchObj (PageTable pt)) (the (ksPSpace sa (ptr + pptrBaseOffset + (UCAST(8 \<rightarrow> 32) (UCAST(32 \<rightarrow> 8) y) << 2)))); dom (ksPSpace sa) = pspace_dom (kheap s); ptr + pptrBaseOffset + (y << 2) \<in> dom (ksPSpace sa)\<rbrakk> \<Longrightarrow> \<exists>ko. ksPSpace sa (ptr + pptrBaseOffset + (y << 2)) = Some ko \<and> is_aligned (ptr + pptrBaseOffset + (y << 2)) (objBitsKO ko) \<and> koTypeOf ko = ArchT PTET \<and> ps_clear (ptr + pptrBaseOffset + (y << 2)) (objBitsKO ko) sa proof (prove)
goal (3 subgoals):
 1. \<And>pt y. \<lbrakk>pspace_aligned s; pspace_distinct' sa; kheap s (ptr + pptrBaseOffset) = Some (ArchObj (PageTable pt)); 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 + pptrBaseOffset) 10; y < 0x100; pte_relation (UCAST(32 \<rightarrow> 8) y) (ArchObj (PageTable pt)) (the (ksPSpace sa (ptr + pptrBaseOffset + (UCAST(8 \<rightarrow> 32) (UCAST(32 \<rightarrow> 8) 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(8 \<rightarrow> 32) (UCAST(32 \<rightarrow> 8) y) << 2
 2. \<And>pt y. \<lbrakk>pspace_aligned s; pspace_distinct' sa; kheap s (ptr + pptrBaseOffset) = Some (ArchObj (PageTable pt)); 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 + pptrBaseOffset) 10; y < 0x100; pte_relation (UCAST(32 \<rightarrow> 8) y) (ArchObj (PageTable pt)) (the (ksPSpace sa (ptr + pptrBaseOffset + (UCAST(8 \<rightarrow> 32) (UCAST(32 \<rightarrow> 8) y) << 2)))); dom (ksPSpace sa) = (\<Union>x\<in>dom (kheap s). fst ` obj_relation_cuts (the (kheap s x)) x)\<rbrakk> \<Longrightarrow> ptr + pptrBaseOffset \<in> dom (kheap s)
 3. \<And>pt y. \<lbrakk>pspace_aligned s; pspace_distinct' sa; kheap s (ptr + pptrBaseOffset) = Some (ArchObj (PageTable pt)); 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 + pptrBaseOffset) 10; y < 0x100; pte_relation (UCAST(32 \<rightarrow> 8) y) (ArchObj (PageTable pt)) (the (ksPSpace sa (ptr + pptrBaseOffset + (UCAST(8 \<rightarrow> 32) (UCAST(32 \<rightarrow> 8) y) << 2)))); dom (ksPSpace sa) = pspace_dom (kheap s); ptr + pptrBaseOffset + (y << 2) \<in> dom (ksPSpace sa)\<rbrakk> \<Longrightarrow> \<exists>ko. ksPSpace sa (ptr + pptrBaseOffset + (y << 2)) = Some ko \<and> is_aligned (ptr + pptrBaseOffset + (y << 2)) (objBitsKO ko) \<and> koTypeOf ko = ArchT PTET \<and> ps_clear (ptr + pptrBaseOffset + (y << 2)) (objBitsKO ko) sa proof (prove)
goal (2 subgoals):
 1. \<And>pt y. \<lbrakk>pspace_aligned s; pspace_distinct' sa; kheap s (ptr + pptrBaseOffset) = Some (ArchObj (PageTable pt)); 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 + pptrBaseOffset) 10; y < 0x100; pte_relation (UCAST(32 \<rightarrow> 8) y) (ArchObj (PageTable pt)) (the (ksPSpace sa (ptr + pptrBaseOffset + (UCAST(8 \<rightarrow> 32) (UCAST(32 \<rightarrow> 8) y) << 2)))); dom (ksPSpace sa) = (\<Union>x\<in>dom (kheap s). fst ` obj_relation_cuts (the (kheap s x)) x)\<rbrakk> \<Longrightarrow> ptr + pptrBaseOffset \<in> dom (kheap s)
 2. \<And>pt y. \<lbrakk>pspace_aligned s; pspace_distinct' sa; kheap s (ptr + pptrBaseOffset) = Some (ArchObj (PageTable pt)); 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 + pptrBaseOffset) 10; y < 0x100; pte_relation (UCAST(32 \<rightarrow> 8) y) (ArchObj (PageTable pt)) (the (ksPSpace sa (ptr + pptrBaseOffset + (UCAST(8 \<rightarrow> 32) (UCAST(32 \<rightarrow> 8) y) << 2)))); dom (ksPSpace sa) = pspace_dom (kheap s); ptr + pptrBaseOffset + (y << 2) \<in> dom (ksPSpace sa)\<rbrakk> \<Longrightarrow> \<exists>ko. ksPSpace sa (ptr + pptrBaseOffset + (y << 2)) = Some ko \<and> is_aligned (ptr + pptrBaseOffset + (y << 2)) (objBitsKO ko) \<and> koTypeOf ko = ArchT PTET \<and> ps_clear (ptr + pptrBaseOffset + (y << 2)) (objBitsKO ko) sa proof (prove)
goal (1 subgoal):
 1. \<And>pt y. \<lbrakk>pspace_aligned s; pspace_distinct' sa; kheap s (ptr + pptrBaseOffset) = Some (ArchObj (PageTable pt)); 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 + pptrBaseOffset) 10; y < 0x100; pte_relation (UCAST(32 \<rightarrow> 8) y) (ArchObj (PageTable pt)) (the (ksPSpace sa (ptr + pptrBaseOffset + (UCAST(8 \<rightarrow> 32) (UCAST(32 \<rightarrow> 8) y) << 2)))); dom (ksPSpace sa) = pspace_dom (kheap s); ptr + pptrBaseOffset + (y << 2) \<in> dom (ksPSpace sa)\<rbrakk> \<Longrightarrow> \<exists>ko. ksPSpace sa (ptr + pptrBaseOffset + (y << 2)) = Some ko \<and> is_aligned (ptr + pptrBaseOffset + (y << 2)) (objBitsKO ko) \<and> koTypeOf ko = ArchT PTET \<and> ps_clear (ptr + pptrBaseOffset + (y << 2)) (objBitsKO ko) sa proof (prove)
goal (1 subgoal):
 1. \<And>pt y. \<lbrakk>pspace_aligned s; pspace_distinct' sa; kheap s (ptr + pptrBaseOffset) = Some (ArchObj (PageTable pt)); 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 + pptrBaseOffset) 10; y < 0x100; pte_relation (UCAST(32 \<rightarrow> 8) y) (ArchObj (PageTable pt)) (the (ksPSpace sa (ptr + pptrBaseOffset + (UCAST(8 \<rightarrow> 32) (UCAST(32 \<rightarrow> 8) y) << 2)))); ptr + pptrBaseOffset + (y << 2) \<in> dom (ksPSpace sa)\<rbrakk> \<Longrightarrow> \<exists>ko. ksPSpace sa (ptr + pptrBaseOffset + (y << 2)) = Some ko \<and> is_aligned (ptr + pptrBaseOffset + (y << 2)) (objBitsKO ko) \<and> koTypeOf ko = ArchT PTET \<and> ps_clear (ptr + pptrBaseOffset + (y << 2)) (objBitsKO ko) sa proof (prove)
goal (1 subgoal):
 1. \<And>pt y. \<lbrakk>pspace_aligned s; pspace_distinct' sa; kheap s (ptr + pptrBaseOffset) = Some (ArchObj (PageTable pt)); 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 + pptrBaseOffset) 10; y < 0x100; pte_relation (UCAST(32 \<rightarrow> 8) y) (ArchObj (PageTable pt)) (the (ksPSpace sa (ptr + pptrBaseOffset + (UCAST(8 \<rightarrow> 32) (UCAST(32 \<rightarrow> 8) y) << 2)))); ptr + pptrBaseOffset + (y << 2) \<in> dom (ksPSpace sa); is_aligned (ptr + pptrBaseOffset) (obj_bits (ArchObj (PageTable pt)))\<rbrakk> \<Longrightarrow> \<exists>ko. ksPSpace sa (ptr + pptrBaseOffset + (y << 2)) = Some ko \<and> is_aligned (ptr + pptrBaseOffset + (y << 2)) (objBitsKO ko) \<and> koTypeOf ko = ArchT PTET \<and> ps_clear (ptr + pptrBaseOffset + (y << 2)) (objBitsKO ko) sa proof (prove)
goal (1 subgoal):
 1. \<And>pt y ya. \<lbrakk>pspace_aligned s; pspace_distinct' sa; kheap s (ptr + pptrBaseOffset) = Some (ArchObj (PageTable pt)); 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 + pptrBaseOffset) 10; y < 0x100; pte_relation (UCAST(32 \<rightarrow> 8) y) (ArchObj (PageTable pt)) ya; ksPSpace sa (ptr + pptrBaseOffset + (y << 2)) = Some ya\<rbrakk> \<Longrightarrow> is_aligned (ptr + pptrBaseOffset + (y << 2)) (objBitsKO ya) \<and> koTypeOf ya = ArchT PTET \<and> ps_clear (ptr + pptrBaseOffset + (y << 2)) (objBitsKO ya) sa proof (prove)
goal (1 subgoal):
 1. \<And>pt y ya. \<lbrakk>pspace_aligned s; pspace_distinct' sa; kheap s (ptr + pptrBaseOffset) = Some (ArchObj (PageTable pt)); 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 + pptrBaseOffset) 10; y < 0x100; ksPSpace sa (ptr + pptrBaseOffset + (y << 2)) = Some ya; \<exists>pte. ya = KOArch (KOPTE pte)\<rbrakk> \<Longrightarrow> is_aligned (ptr + pptrBaseOffset + (y << 2)) (objBitsKO ya) \<and> koTypeOf ya = ArchT PTET \<and> ps_clear (ptr + pptrBaseOffset + (y << 2)) (objBitsKO ya) sa proof (prove)
goal (1 subgoal):
 1. \<And>pt y ya. \<lbrakk>pspace_aligned s; pspace_distinct' sa; kheap s (ptr + pptrBaseOffset) = Some (ArchObj (PageTable pt)); 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 + pptrBaseOffset) 10; y < 0x100; \<exists>pte. ya = KOArch (KOPTE pte); ps_clear (ptr + pptrBaseOffset + (y << 2)) (objBitsKO ya) sa\<rbrakk> \<Longrightarrow> is_aligned (ptr + pptrBaseOffset + (y << 2)) (objBitsKO ya) \<and> koTypeOf ya = ArchT PTET \<and> ps_clear (ptr + pptrBaseOffset + (y << 2)) (objBitsKO ya) sa proof (prove)
goal (1 subgoal):
 1. \<And>pt y. \<lbrakk>pspace_aligned s; pspace_distinct' sa; kheap s (ptr + pptrBaseOffset) = Some (ArchObj (PageTable pt)); 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 + pptrBaseOffset) 10; y < 0x100; ps_clear (ptr + pptrBaseOffset + (y << 2)) pteBits sa\<rbrakk> \<Longrightarrow> is_aligned (ptr + pptrBaseOffset + (y << 2)) pteBits proof (prove)
goal (2 subgoals):
 1. \<And>pt y. \<lbrakk>pspace_aligned s; pspace_distinct' sa; kheap s (ptr + pptrBaseOffset) = Some (ArchObj (PageTable pt)); 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 + pptrBaseOffset) 10; y < 0x100; ps_clear (ptr + pptrBaseOffset + (y << 2)) pteBits sa\<rbrakk> \<Longrightarrow> is_aligned (ptr + pptrBaseOffset + (y << 2)) (?x71 pt y)
 2. \<And>pt y. \<lbrakk>pspace_aligned s; pspace_distinct' sa; kheap s (ptr + pptrBaseOffset) = Some (ArchObj (PageTable pt)); 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 + pptrBaseOffset) 10; y < 0x100; ps_clear (ptr + pptrBaseOffset + (y << 2)) pteBits sa\<rbrakk> \<Longrightarrow> pteBits \<le> ?x71 pt y proof (prove)
goal (3 subgoals):
 1. \<And>pt y. \<lbrakk>pspace_aligned s; pspace_distinct' sa; kheap s (ptr + pptrBaseOffset) = Some (ArchObj (PageTable pt)); 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 < 0x100; ps_clear (ptr + pptrBaseOffset + (y << 2)) pteBits sa\<rbrakk> \<Longrightarrow> is_aligned (y << 2) (?x71 pt y)
 2. \<And>pt y. \<lbrakk>pspace_aligned s; pspace_distinct' sa; kheap s (ptr + pptrBaseOffset) = Some (ArchObj (PageTable pt)); 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 < 0x100; ps_clear (ptr + pptrBaseOffset + (y << 2)) pteBits sa\<rbrakk> \<Longrightarrow> ?x71 pt y \<le> 10
 3. \<And>pt y. \<lbrakk>pspace_aligned s; pspace_distinct' sa; kheap s (ptr + pptrBaseOffset) = Some (ArchObj (PageTable pt)); 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 + pptrBaseOffset) 10; y < 0x100; ps_clear (ptr + pptrBaseOffset + (y << 2)) pteBits sa\<rbrakk> \<Longrightarrow> pteBits \<le> ?x71 pt y proof (prove)
goal (2 subgoals):
 1. \<And>pt y. \<lbrakk>pspace_aligned s; pspace_distinct' sa; kheap s (ptr + pptrBaseOffset) = Some (ArchObj (PageTable pt)); 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 < 0x100; ps_clear (ptr + pptrBaseOffset + (y << 2)) pteBits sa\<rbrakk> \<Longrightarrow> 2 \<le> 10
 2. \<And>pt y. \<lbrakk>pspace_aligned s; pspace_distinct' sa; kheap s (ptr + pptrBaseOffset) = Some (ArchObj (PageTable pt)); 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 + pptrBaseOffset) 10; y < 0x100; ps_clear (ptr + pptrBaseOffset + (y << 2)) pteBits sa\<rbrakk> \<Longrightarrow> pteBits \<le> 2 proof (prove)
goal (1 subgoal):
 1. \<And>pt y. \<lbrakk>pspace_aligned s; pspace_distinct' sa; kheap s (ptr + pptrBaseOffset) = Some (ArchObj (PageTable pt)); 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 + pptrBaseOffset) 10; y < 0x100; ps_clear (ptr + pptrBaseOffset + (y << 2)) pteBits sa\<rbrakk> \<Longrightarrow> pteBits \<le> 2 proof (prove)
goal:
No subgoals!