theory ArchUserOp_IF

lemma requiv_device_mem_eq:
  "\<lbrakk> reads_equiv aag s s'; globals_equiv s s'; invs s; invs s'; valid_pdpt_objs s;
     valid_pdpt_objs s'; is_subject aag (cur_thread s); AllowRead \<in> ptable_rights_s s x;
     ptable_lift_s s x = Some y; pas_refined aag s; pas_refined aag s' \<rbrakk>
     \<Longrightarrow> device_mem s (ptrFromPAddr y) = device_mem s' (ptrFromPAddr y)" apply (simp add: device_mem_def) apply (rule conjI) apply (erule reads_equivE) apply (clarsimp simp: in_device_frame_def) apply (rule exI) apply (rule device_frame_at_equiv) apply assumption+ apply (erule_tac f="underlying_memory" in equiv_forE) apply (frule_tac auth=Read in user_op_access_data_at[where s=s]) apply (fastforce simp: ptable_lift_s_def ptable_rights_s_def vspace_cap_rights_to_auth_def
                | intro typ_at_device_data_at)+ apply (rule reads_read) apply (fastforce simp: ptrFromPAddr_mask_simp) apply clarsimp apply (frule requiv_ptable_rights_eq, fastforce+) apply (frule requiv_ptable_lift_eq, fastforce+) apply (clarsimp simp: globals_equiv_def) apply (erule notE) apply (erule reads_equivE) apply (clarsimp simp: in_device_frame_def) apply (rule exI) apply (rule device_frame_at_equiv) apply assumption+ apply (erule_tac f="underlying_memory" in equiv_forE) apply (erule equiv_symmetric[THEN iffD1]) apply (frule_tac auth=Read in user_op_access_data_at[where s=s']) apply (fastforce simp: ptable_lift_s_def ptable_rights_s_def vspace_cap_rights_to_auth_def
               | intro typ_at_device_data_at)+ apply (rule reads_read) apply (fastforce simp: ptrFromPAddr_mask_simp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>reads_equiv aag s s'; globals_equiv s s'; invs s; invs s'; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; \<forall>x\<in>ran (kheap s'). obj_valid_pdpt x; is_subject aag (cur_thread s); AllowRead \<in> ptable_rights_s s x; ptable_lift_s s x = Some y; pas_refined aag s; pas_refined aag s'\<rbrakk> \<Longrightarrow> device_mem s (ptrFromPAddr y) = device_mem s' (ptrFromPAddr y) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>reads_equiv aag s s'; globals_equiv s s'; invs s; invs s'; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; \<forall>x\<in>ran (kheap s'). obj_valid_pdpt x; is_subject aag (cur_thread s); AllowRead \<in> ptable_rights_s s x; ptable_lift_s s x = Some y; pas_refined aag s; pas_refined aag s'\<rbrakk> \<Longrightarrow> (in_device_frame (ptrFromPAddr y) s \<longrightarrow> in_device_frame (ptrFromPAddr y) s') \<and> (\<not> in_device_frame (ptrFromPAddr y) s \<longrightarrow> \<not> in_device_frame (ptrFromPAddr y) s') proof (prove)
goal (2 subgoals):
 1. \<lbrakk>reads_equiv aag s s'; globals_equiv s s'; invs s; invs s'; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; \<forall>x\<in>ran (kheap s'). obj_valid_pdpt x; is_subject aag (cur_thread s); AllowRead \<in> ptable_rights_s s x; ptable_lift_s s x = Some y; pas_refined aag s; pas_refined aag s'\<rbrakk> \<Longrightarrow> in_device_frame (ptrFromPAddr y) s \<longrightarrow> in_device_frame (ptrFromPAddr y) s'
 2. \<lbrakk>reads_equiv aag s s'; globals_equiv s s'; invs s; invs s'; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; \<forall>x\<in>ran (kheap s'). obj_valid_pdpt x; is_subject aag (cur_thread s); AllowRead \<in> ptable_rights_s s x; ptable_lift_s s x = Some y; pas_refined aag s; pas_refined aag s'\<rbrakk> \<Longrightarrow> \<not> in_device_frame (ptrFromPAddr y) s \<longrightarrow> \<not> in_device_frame (ptrFromPAddr y) s' proof (prove)
goal (2 subgoals):
 1. \<lbrakk>globals_equiv s s'; invs s; invs s'; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; \<forall>x\<in>ran (kheap s'). obj_valid_pdpt x; is_subject aag (cur_thread s); AllowRead \<in> ptable_rights_s s x; ptable_lift_s s x = Some y; pas_refined aag s; pas_refined aag s'; equiv_for (aag_can_read aag) kheap s s'; equiv_machine_state (aag_can_read aag) (machine_state s) (machine_state s'); equiv_for (aag_can_read aag \<circ> fst) cdt s s'; equiv_for (aag_can_read aag \<circ> fst) cdt_list s s'; equiv_for (aag_can_read aag) ekheap s s'; equiv_for (aag_can_read aag \<circ> fst) is_original_cap s s'; equiv_for (aag_can_read_irq aag) interrupt_states s s'; equiv_for (aag_can_read_irq aag) interrupt_irq_node s s'; equiv_asids (aag_can_read_asid aag) s s'; equiv_for (aag_can_read_domain aag) ready_queues s s'; cur_thread s = cur_thread s'; cur_domain s = cur_domain s'; scheduler_action s = scheduler_action s'; work_units_completed s = work_units_completed s'; equiv_irq_state (machine_state s) (machine_state s')\<rbrakk> \<Longrightarrow> in_device_frame (ptrFromPAddr y) s \<longrightarrow> in_device_frame (ptrFromPAddr y) s'
 2. \<lbrakk>reads_equiv aag s s'; globals_equiv s s'; invs s; invs s'; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; \<forall>x\<in>ran (kheap s'). obj_valid_pdpt x; is_subject aag (cur_thread s); AllowRead \<in> ptable_rights_s s x; ptable_lift_s s x = Some y; pas_refined aag s; pas_refined aag s'\<rbrakk> \<Longrightarrow> \<not> in_device_frame (ptrFromPAddr y) s \<longrightarrow> \<not> in_device_frame (ptrFromPAddr y) s' proof (prove)
goal (2 subgoals):
 1. \<And>sz. \<lbrakk>globals_equiv s s'; invs s; invs s'; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; \<forall>x\<in>ran (kheap s'). obj_valid_pdpt x; is_subject aag (cur_thread s'); AllowRead \<in> ptable_rights_s s x; ptable_lift_s s x = Some y; pas_refined aag s; pas_refined aag s'; equiv_for (aag_can_read aag) kheap s s'; equiv_for (aag_can_read aag \<circ> fst) cdt s s'; equiv_for (aag_can_read aag \<circ> fst) cdt_list s s'; equiv_for (aag_can_read aag) ekheap s s'; equiv_for (aag_can_read aag \<circ> fst) is_original_cap s s'; equiv_for (aag_can_read_irq aag) interrupt_states s s'; equiv_for (aag_can_read_irq aag) interrupt_irq_node s s'; equiv_asids (aag_can_read_asid aag) s s'; equiv_for (aag_can_read_domain aag) ready_queues s s'; cur_thread s = cur_thread s'; cur_domain s = cur_domain s'; scheduler_action s = scheduler_action s'; work_units_completed s = work_units_completed s'; equiv_irq_state (machine_state s) (machine_state s'); equiv_for (aag_can_read aag) underlying_memory (machine_state s) (machine_state s'); equiv_for (aag_can_read aag) device_state (machine_state s) (machine_state s'); typ_at (AArch (ADeviceData sz)) (ptrFromPAddr y && ~~ mask (pageBitsForSize sz)) s\<rbrakk> \<Longrightarrow> \<exists>sz. typ_at (AArch (ADeviceData sz)) (ptrFromPAddr y && ~~ mask (pageBitsForSize sz)) s'
 2. \<lbrakk>reads_equiv aag s s'; globals_equiv s s'; invs s; invs s'; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; \<forall>x\<in>ran (kheap s'). obj_valid_pdpt x; is_subject aag (cur_thread s); AllowRead \<in> ptable_rights_s s x; ptable_lift_s s x = Some y; pas_refined aag s; pas_refined aag s'\<rbrakk> \<Longrightarrow> \<not> in_device_frame (ptrFromPAddr y) s \<longrightarrow> \<not> in_device_frame (ptrFromPAddr y) s' proof (prove)
goal (2 subgoals):
 1. \<And>sz. \<lbrakk>globals_equiv s s'; invs s; invs s'; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; \<forall>x\<in>ran (kheap s'). obj_valid_pdpt x; is_subject aag (cur_thread s'); AllowRead \<in> ptable_rights_s s x; ptable_lift_s s x = Some y; pas_refined aag s; pas_refined aag s'; equiv_for (aag_can_read aag) kheap s s'; equiv_for (aag_can_read aag \<circ> fst) cdt s s'; equiv_for (aag_can_read aag \<circ> fst) cdt_list s s'; equiv_for (aag_can_read aag) ekheap s s'; equiv_for (aag_can_read aag \<circ> fst) is_original_cap s s'; equiv_for (aag_can_read_irq aag) interrupt_states s s'; equiv_for (aag_can_read_irq aag) interrupt_irq_node s s'; equiv_asids (aag_can_read_asid aag) s s'; equiv_for (aag_can_read_domain aag) ready_queues s s'; cur_thread s = cur_thread s'; cur_domain s = cur_domain s'; scheduler_action s = scheduler_action s'; work_units_completed s = work_units_completed s'; equiv_irq_state (machine_state s) (machine_state s'); equiv_for (aag_can_read aag) underlying_memory (machine_state s) (machine_state s'); equiv_for (aag_can_read aag) device_state (machine_state s) (machine_state s'); typ_at (AArch (ADeviceData sz)) (ptrFromPAddr y && ~~ mask (pageBitsForSize sz)) s\<rbrakk> \<Longrightarrow> typ_at (AArch (ADeviceData (?sz18 sz))) (ptrFromPAddr y && ~~ mask (pageBitsForSize (?sz18 sz))) s'
 2. \<lbrakk>reads_equiv aag s s'; globals_equiv s s'; invs s; invs s'; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; \<forall>x\<in>ran (kheap s'). obj_valid_pdpt x; is_subject aag (cur_thread s); AllowRead \<in> ptable_rights_s s x; ptable_lift_s s x = Some y; pas_refined aag s; pas_refined aag s'\<rbrakk> \<Longrightarrow> \<not> in_device_frame (ptrFromPAddr y) s \<longrightarrow> \<not> in_device_frame (ptrFromPAddr y) s' proof (prove)
goal (4 subgoals):
 1. \<And>sz. \<lbrakk>globals_equiv s s'; invs s; invs s'; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; \<forall>x\<in>ran (kheap s'). obj_valid_pdpt x; is_subject aag (cur_thread s'); AllowRead \<in> ptable_rights_s s x; ptable_lift_s s x = Some y; pas_refined aag s; pas_refined aag s'; equiv_for (aag_can_read aag) kheap s s'; equiv_for (aag_can_read aag \<circ> fst) cdt s s'; equiv_for (aag_can_read aag \<circ> fst) cdt_list s s'; equiv_for (aag_can_read aag) ekheap s s'; equiv_for (aag_can_read aag \<circ> fst) is_original_cap s s'; equiv_for (aag_can_read_irq aag) interrupt_states s s'; equiv_for (aag_can_read_irq aag) interrupt_irq_node s s'; equiv_asids (aag_can_read_asid aag) s s'; equiv_for (aag_can_read_domain aag) ready_queues s s'; cur_thread s = cur_thread s'; cur_domain s = cur_domain s'; scheduler_action s = scheduler_action s'; work_units_completed s = work_units_completed s'; equiv_irq_state (machine_state s) (machine_state s'); equiv_for (aag_can_read aag) underlying_memory (machine_state s) (machine_state s'); equiv_for (aag_can_read aag) device_state (machine_state s) (machine_state s'); typ_at (AArch (ADeviceData sz)) (ptrFromPAddr y && ~~ mask (pageBitsForSize sz)) s\<rbrakk> \<Longrightarrow> typ_at (AArch (ADeviceData (?sz18 sz))) (ptrFromPAddr y && ~~ mask (pageBitsForSize (?sz18 sz))) (?s20 sz)
 2. \<And>sz. \<lbrakk>globals_equiv s s'; invs s; invs s'; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; \<forall>x\<in>ran (kheap s'). obj_valid_pdpt x; is_subject aag (cur_thread s'); AllowRead \<in> ptable_rights_s s x; ptable_lift_s s x = Some y; pas_refined aag s; pas_refined aag s'; equiv_for (aag_can_read aag) kheap s s'; equiv_for (aag_can_read aag \<circ> fst) cdt s s'; equiv_for (aag_can_read aag \<circ> fst) cdt_list s s'; equiv_for (aag_can_read aag) ekheap s s'; equiv_for (aag_can_read aag \<circ> fst) is_original_cap s s'; equiv_for (aag_can_read_irq aag) interrupt_states s s'; equiv_for (aag_can_read_irq aag) interrupt_irq_node s s'; equiv_asids (aag_can_read_asid aag) s s'; equiv_for (aag_can_read_domain aag) ready_queues s s'; cur_thread s = cur_thread s'; cur_domain s = cur_domain s'; scheduler_action s = scheduler_action s'; work_units_completed s = work_units_completed s'; equiv_irq_state (machine_state s) (machine_state s'); equiv_for (aag_can_read aag) underlying_memory (machine_state s) (machine_state s'); equiv_for (aag_can_read aag) device_state (machine_state s) (machine_state s'); typ_at (AArch (ADeviceData sz)) (ptrFromPAddr y && ~~ mask (pageBitsForSize sz)) s\<rbrakk> \<Longrightarrow> equiv_for (?P20 sz) kheap (?s20 sz) s'
 3. \<And>sz. \<lbrakk>globals_equiv s s'; invs s; invs s'; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; \<forall>x\<in>ran (kheap s'). obj_valid_pdpt x; is_subject aag (cur_thread s'); AllowRead \<in> ptable_rights_s s x; ptable_lift_s s x = Some y; pas_refined aag s; pas_refined aag s'; equiv_for (aag_can_read aag) kheap s s'; equiv_for (aag_can_read aag \<circ> fst) cdt s s'; equiv_for (aag_can_read aag \<circ> fst) cdt_list s s'; equiv_for (aag_can_read aag) ekheap s s'; equiv_for (aag_can_read aag \<circ> fst) is_original_cap s s'; equiv_for (aag_can_read_irq aag) interrupt_states s s'; equiv_for (aag_can_read_irq aag) interrupt_irq_node s s'; equiv_asids (aag_can_read_asid aag) s s'; equiv_for (aag_can_read_domain aag) ready_queues s s'; cur_thread s = cur_thread s'; cur_domain s = cur_domain s'; scheduler_action s = scheduler_action s'; work_units_completed s = work_units_completed s'; equiv_irq_state (machine_state s) (machine_state s'); equiv_for (aag_can_read aag) underlying_memory (machine_state s) (machine_state s'); equiv_for (aag_can_read aag) device_state (machine_state s) (machine_state s'); typ_at (AArch (ADeviceData sz)) (ptrFromPAddr y && ~~ mask (pageBitsForSize sz)) s\<rbrakk> \<Longrightarrow> ?P20 sz (ptrFromPAddr y && ~~ mask (pageBitsForSize (?sz18 sz)))
 4. \<lbrakk>reads_equiv aag s s'; globals_equiv s s'; invs s; invs s'; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; \<forall>x\<in>ran (kheap s'). obj_valid_pdpt x; is_subject aag (cur_thread s); AllowRead \<in> ptable_rights_s s x; ptable_lift_s s x = Some y; pas_refined aag s; pas_refined aag s'\<rbrakk> \<Longrightarrow> \<not> in_device_frame (ptrFromPAddr y) s \<longrightarrow> \<not> in_device_frame (ptrFromPAddr y) s' proof (prove)
goal (2 subgoals):
 1. \<And>sz. \<lbrakk>globals_equiv s s'; invs s; invs s'; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; \<forall>x\<in>ran (kheap s'). obj_valid_pdpt x; is_subject aag (cur_thread s'); AllowRead \<in> ptable_rights_s s x; ptable_lift_s s x = Some y; pas_refined aag s; pas_refined aag s'; equiv_for (aag_can_read aag) kheap s s'; equiv_for (aag_can_read aag \<circ> fst) cdt s s'; equiv_for (aag_can_read aag \<circ> fst) cdt_list s s'; equiv_for (aag_can_read aag) ekheap s s'; equiv_for (aag_can_read aag \<circ> fst) is_original_cap s s'; equiv_for (aag_can_read_irq aag) interrupt_states s s'; equiv_for (aag_can_read_irq aag) interrupt_irq_node s s'; equiv_asids (aag_can_read_asid aag) s s'; equiv_for (aag_can_read_domain aag) ready_queues s s'; cur_thread s = cur_thread s'; cur_domain s = cur_domain s'; scheduler_action s = scheduler_action s'; work_units_completed s = work_units_completed s'; equiv_irq_state (machine_state s) (machine_state s'); equiv_for (aag_can_read aag) underlying_memory (machine_state s) (machine_state s'); equiv_for (aag_can_read aag) device_state (machine_state s) (machine_state s'); typ_at (AArch (ADeviceData sz)) (ptrFromPAddr y && ~~ mask (pageBitsForSize sz)) s\<rbrakk> \<Longrightarrow> aag_can_read aag (ptrFromPAddr y && ~~ mask (pageBitsForSize sz))
 2. \<lbrakk>reads_equiv aag s s'; globals_equiv s s'; invs s; invs s'; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; \<forall>x\<in>ran (kheap s'). obj_valid_pdpt x; is_subject aag (cur_thread s); AllowRead \<in> ptable_rights_s s x; ptable_lift_s s x = Some y; pas_refined aag s; pas_refined aag s'\<rbrakk> \<Longrightarrow> \<not> in_device_frame (ptrFromPAddr y) s \<longrightarrow> \<not> in_device_frame (ptrFromPAddr y) s' proof (prove)
goal (2 subgoals):
 1. \<And>sz. \<lbrakk>globals_equiv s s'; invs s; invs s'; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; \<forall>x\<in>ran (kheap s'). obj_valid_pdpt x; is_subject aag (cur_thread s'); AllowRead \<in> ptable_rights_s s x; ptable_lift_s s x = Some y; pas_refined aag s; pas_refined aag s'; equiv_for (aag_can_read aag) kheap s s'; equiv_for (aag_can_read aag \<circ> fst) cdt s s'; equiv_for (aag_can_read aag \<circ> fst) cdt_list s s'; equiv_for (aag_can_read aag) ekheap s s'; equiv_for (aag_can_read aag \<circ> fst) is_original_cap s s'; equiv_for (aag_can_read_irq aag) interrupt_states s s'; equiv_for (aag_can_read_irq aag) interrupt_irq_node s s'; equiv_asids (aag_can_read_asid aag) s s'; equiv_for (aag_can_read_domain aag) ready_queues s s'; cur_thread s = cur_thread s'; cur_domain s = cur_domain s'; scheduler_action s = scheduler_action s'; work_units_completed s = work_units_completed s'; equiv_irq_state (machine_state s) (machine_state s'); equiv_for (aag_can_read aag) device_state (machine_state s) (machine_state s'); typ_at (AArch (ADeviceData sz)) (ptrFromPAddr y && ~~ mask (pageBitsForSize sz)) s; \<And>x. aag_can_read aag x \<Longrightarrow> underlying_memory (machine_state s) x = underlying_memory (machine_state s') x\<rbrakk> \<Longrightarrow> aag_can_read aag (ptrFromPAddr y && ~~ mask (pageBitsForSize sz))
 2. \<lbrakk>reads_equiv aag s s'; globals_equiv s s'; invs s; invs s'; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; \<forall>x\<in>ran (kheap s'). obj_valid_pdpt x; is_subject aag (cur_thread s); AllowRead \<in> ptable_rights_s s x; ptable_lift_s s x = Some y; pas_refined aag s; pas_refined aag s'\<rbrakk> \<Longrightarrow> \<not> in_device_frame (ptrFromPAddr y) s \<longrightarrow> \<not> in_device_frame (ptrFromPAddr y) s' proof (prove)
goal (8 subgoals):
 1. \<And>sz. \<lbrakk>globals_equiv s s'; invs s; invs s'; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; \<forall>x\<in>ran (kheap s'). obj_valid_pdpt x; is_subject aag (cur_thread s'); AllowRead \<in> ptable_rights_s s x; ptable_lift_s s x = Some y; pas_refined aag s; pas_refined aag s'; equiv_for (aag_can_read aag) kheap s s'; equiv_for (aag_can_read aag \<circ> fst) cdt s s'; equiv_for (aag_can_read aag \<circ> fst) cdt_list s s'; equiv_for (aag_can_read aag) ekheap s s'; equiv_for (aag_can_read aag \<circ> fst) is_original_cap s s'; equiv_for (aag_can_read_irq aag) interrupt_states s s'; equiv_for (aag_can_read_irq aag) interrupt_irq_node s s'; equiv_asids (aag_can_read_asid aag) s s'; equiv_for (aag_can_read_domain aag) ready_queues s s'; cur_thread s = cur_thread s'; cur_domain s = cur_domain s'; scheduler_action s = scheduler_action s'; work_units_completed s = work_units_completed s'; equiv_irq_state (machine_state s) (machine_state s'); equiv_for (aag_can_read aag) device_state (machine_state s) (machine_state s'); typ_at (AArch (ADeviceData sz)) (ptrFromPAddr y && ~~ mask (pageBitsForSize sz)) s; \<And>x. aag_can_read aag x \<Longrightarrow> underlying_memory (machine_state s) x = underlying_memory (machine_state s') x\<rbrakk> \<Longrightarrow> \<forall>x\<in>ran (kheap s). obj_valid_pdpt x
 2. \<And>sz. \<lbrakk>globals_equiv s s'; invs s; invs s'; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; \<forall>x\<in>ran (kheap s'). obj_valid_pdpt x; is_subject aag (cur_thread s'); AllowRead \<in> ptable_rights_s s x; ptable_lift_s s x = Some y; pas_refined aag s; pas_refined aag s'; equiv_for (aag_can_read aag) kheap s s'; equiv_for (aag_can_read aag \<circ> fst) cdt s s'; equiv_for (aag_can_read aag \<circ> fst) cdt_list s s'; equiv_for (aag_can_read aag) ekheap s s'; equiv_for (aag_can_read aag \<circ> fst) is_original_cap s s'; equiv_for (aag_can_read_irq aag) interrupt_states s s'; equiv_for (aag_can_read_irq aag) interrupt_irq_node s s'; equiv_asids (aag_can_read_asid aag) s s'; equiv_for (aag_can_read_domain aag) ready_queues s s'; cur_thread s = cur_thread s'; cur_domain s = cur_domain s'; scheduler_action s = scheduler_action s'; work_units_completed s = work_units_completed s'; equiv_irq_state (machine_state s) (machine_state s'); equiv_for (aag_can_read aag) device_state (machine_state s) (machine_state s'); typ_at (AArch (ADeviceData sz)) (ptrFromPAddr y && ~~ mask (pageBitsForSize sz)) s; \<And>x. aag_can_read aag x \<Longrightarrow> underlying_memory (machine_state s) x = underlying_memory (machine_state s') x\<rbrakk> \<Longrightarrow> pas_refined (?aag26 sz) s
 3. \<And>sz. \<lbrakk>globals_equiv s s'; invs s; invs s'; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; \<forall>x\<in>ran (kheap s'). obj_valid_pdpt x; is_subject aag (cur_thread s'); AllowRead \<in> ptable_rights_s s x; ptable_lift_s s x = Some y; pas_refined aag s; pas_refined aag s'; equiv_for (aag_can_read aag) kheap s s'; equiv_for (aag_can_read aag \<circ> fst) cdt s s'; equiv_for (aag_can_read aag \<circ> fst) cdt_list s s'; equiv_for (aag_can_read aag) ekheap s s'; equiv_for (aag_can_read aag \<circ> fst) is_original_cap s s'; equiv_for (aag_can_read_irq aag) interrupt_states s s'; equiv_for (aag_can_read_irq aag) interrupt_irq_node s s'; equiv_asids (aag_can_read_asid aag) s s'; equiv_for (aag_can_read_domain aag) ready_queues s s'; cur_thread s = cur_thread s'; cur_domain s = cur_domain s'; scheduler_action s = scheduler_action s'; work_units_completed s = work_units_completed s'; equiv_irq_state (machine_state s) (machine_state s'); equiv_for (aag_can_read aag) device_state (machine_state s) (machine_state s'); typ_at (AArch (ADeviceData sz)) (ptrFromPAddr y && ~~ mask (pageBitsForSize sz)) s; \<And>x. aag_can_read aag x \<Longrightarrow> underlying_memory (machine_state s) x = underlying_memory (machine_state s') x\<rbrakk> \<Longrightarrow> is_subject (?aag26 sz) (?tcb26 sz)
 4. \<And>sz. \<lbrakk>globals_equiv s s'; invs s; invs s'; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; \<forall>x\<in>ran (kheap s'). obj_valid_pdpt x; is_subject aag (cur_thread s'); AllowRead \<in> ptable_rights_s s x; ptable_lift_s s x = Some y; pas_refined aag s; pas_refined aag s'; equiv_for (aag_can_read aag) kheap s s'; equiv_for (aag_can_read aag \<circ> fst) cdt s s'; equiv_for (aag_can_read aag \<circ> fst) cdt_list s s'; equiv_for (aag_can_read aag) ekheap s s'; equiv_for (aag_can_read aag \<circ> fst) is_original_cap s s'; equiv_for (aag_can_read_irq aag) interrupt_states s s'; equiv_for (aag_can_read_irq aag) interrupt_irq_node s s'; equiv_asids (aag_can_read_asid aag) s s'; equiv_for (aag_can_read_domain aag) ready_queues s s'; cur_thread s = cur_thread s'; cur_domain s = cur_domain s'; scheduler_action s = scheduler_action s'; work_units_completed s = work_units_completed s'; equiv_irq_state (machine_state s) (machine_state s'); equiv_for (aag_can_read aag) device_state (machine_state s) (machine_state s'); typ_at (AArch (ADeviceData sz)) (ptrFromPAddr y && ~~ mask (pageBitsForSize sz)) s; \<And>x. aag_can_read aag x \<Longrightarrow> underlying_memory (machine_state s) x = underlying_memory (machine_state s') x\<rbrakk> \<Longrightarrow> ptable_lift (?tcb26 sz) s (?x26 sz) = Some (?ptr26 sz)
 5. \<And>sz. \<lbrakk>globals_equiv s s'; invs s; invs s'; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; \<forall>x\<in>ran (kheap s'). obj_valid_pdpt x; is_subject aag (cur_thread s'); AllowRead \<in> ptable_rights_s s x; ptable_lift_s s x = Some y; pas_refined aag s; pas_refined aag s'; equiv_for (aag_can_read aag) kheap s s'; equiv_for (aag_can_read aag \<circ> fst) cdt s s'; equiv_for (aag_can_read aag \<circ> fst) cdt_list s s'; equiv_for (aag_can_read aag) ekheap s s'; equiv_for (aag_can_read aag \<circ> fst) is_original_cap s s'; equiv_for (aag_can_read_irq aag) interrupt_states s s'; equiv_for (aag_can_read_irq aag) interrupt_irq_node s s'; equiv_asids (aag_can_read_asid aag) s s'; equiv_for (aag_can_read_domain aag) ready_queues s s'; cur_thread s = cur_thread s'; cur_domain s = cur_domain s'; scheduler_action s = scheduler_action s'; work_units_completed s = work_units_completed s'; equiv_irq_state (machine_state s) (machine_state s'); equiv_for (aag_can_read aag) device_state (machine_state s) (machine_state s'); typ_at (AArch (ADeviceData sz)) (ptrFromPAddr y && ~~ mask (pageBitsForSize sz)) s; \<And>x. aag_can_read aag x \<Longrightarrow> underlying_memory (machine_state s) x = underlying_memory (machine_state s') x\<rbrakk> \<Longrightarrow> data_at (?sz26 sz) (ptrFromPAddr (?ptr26 sz) && ~~ mask (pageBitsForSize (?sz26 sz))) s
 6. \<And>sz. \<lbrakk>globals_equiv s s'; invs s; invs s'; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; \<forall>x\<in>ran (kheap s'). obj_valid_pdpt x; is_subject aag (cur_thread s'); AllowRead \<in> ptable_rights_s s x; ptable_lift_s s x = Some y; pas_refined aag s; pas_refined aag s'; equiv_for (aag_can_read aag) kheap s s'; equiv_for (aag_can_read aag \<circ> fst) cdt s s'; equiv_for (aag_can_read aag \<circ> fst) cdt_list s s'; equiv_for (aag_can_read aag) ekheap s s'; equiv_for (aag_can_read aag \<circ> fst) is_original_cap s s'; equiv_for (aag_can_read_irq aag) interrupt_states s s'; equiv_for (aag_can_read_irq aag) interrupt_irq_node s s'; equiv_asids (aag_can_read_asid aag) s s'; equiv_for (aag_can_read_domain aag) ready_queues s s'; cur_thread s = cur_thread s'; cur_domain s = cur_domain s'; scheduler_action s = scheduler_action s'; work_units_completed s = work_units_completed s'; equiv_irq_state (machine_state s) (machine_state s'); equiv_for (aag_can_read aag) device_state (machine_state s) (machine_state s'); typ_at (AArch (ADeviceData sz)) (ptrFromPAddr y && ~~ mask (pageBitsForSize sz)) s; \<And>x. aag_can_read aag x \<Longrightarrow> underlying_memory (machine_state s) x = underlying_memory (machine_state s') x\<rbrakk> \<Longrightarrow> Read \<in> vspace_cap_rights_to_auth (ptable_rights (?tcb26 sz) s (?x26 sz))
 7. \<And>sz. \<lbrakk>globals_equiv s s'; invs s; invs s'; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; \<forall>x\<in>ran (kheap s'). obj_valid_pdpt x; is_subject aag (cur_thread s'); AllowRead \<in> ptable_rights_s s x; ptable_lift_s s x = Some y; pas_refined aag s; pas_refined aag s'; equiv_for (aag_can_read aag) kheap s s'; equiv_for (aag_can_read aag \<circ> fst) cdt s s'; equiv_for (aag_can_read aag \<circ> fst) cdt_list s s'; equiv_for (aag_can_read aag) ekheap s s'; equiv_for (aag_can_read aag \<circ> fst) is_original_cap s s'; equiv_for (aag_can_read_irq aag) interrupt_states s s'; equiv_for (aag_can_read_irq aag) interrupt_irq_node s s'; equiv_asids (aag_can_read_asid aag) s s'; equiv_for (aag_can_read_domain aag) ready_queues s s'; cur_thread s = cur_thread s'; cur_domain s = cur_domain s'; scheduler_action s = scheduler_action s'; work_units_completed s = work_units_completed s'; equiv_irq_state (machine_state s) (machine_state s'); equiv_for (aag_can_read aag) device_state (machine_state s) (machine_state s'); typ_at (AArch (ADeviceData sz)) (ptrFromPAddr y && ~~ mask (pageBitsForSize sz)) s; \<And>x. aag_can_read aag x \<Longrightarrow> underlying_memory (machine_state s) x = underlying_memory (machine_state s') x; (pasObjectAbs (?aag26 sz) (?tcb26 sz), Read, pasObjectAbs (?aag26 sz) (ptrFromPAddr (?ptr26 sz && ~~ mask (pageBitsForSize (?sz26 sz))))) \<in> pasPolicy (?aag26 sz)\<rbrakk> \<Longrightarrow> aag_can_read aag (ptrFromPAddr y && ~~ mask (pageBitsForSize sz))
 8. \<lbrakk>reads_equiv aag s s'; globals_equiv s s'; invs s; invs s'; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; \<forall>x\<in>ran (kheap s'). obj_valid_pdpt x; is_subject aag (cur_thread s); AllowRead \<in> ptable_rights_s s x; ptable_lift_s s x = Some y; pas_refined aag s; pas_refined aag s'\<rbrakk> \<Longrightarrow> \<not> in_device_frame (ptrFromPAddr y) s \<longrightarrow> \<not> in_device_frame (ptrFromPAddr y) s' proof (prove)
goal (2 subgoals):
 1. \<And>sz. \<lbrakk>globals_equiv s s'; invs s; invs s'; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; \<forall>x\<in>ran (kheap s'). obj_valid_pdpt x; is_subject aag (cur_thread s'); AllowRead \<in> ptable_rights_s s x; ptable_lift_s s x = Some y; pas_refined aag s; pas_refined aag s'; equiv_for (aag_can_read aag) kheap s s'; equiv_for (aag_can_read aag \<circ> fst) cdt s s'; equiv_for (aag_can_read aag \<circ> fst) cdt_list s s'; equiv_for (aag_can_read aag) ekheap s s'; equiv_for (aag_can_read aag \<circ> fst) is_original_cap s s'; equiv_for (aag_can_read_irq aag) interrupt_states s s'; equiv_for (aag_can_read_irq aag) interrupt_irq_node s s'; equiv_asids (aag_can_read_asid aag) s s'; equiv_for (aag_can_read_domain aag) ready_queues s s'; cur_thread s = cur_thread s'; cur_domain s = cur_domain s'; scheduler_action s = scheduler_action s'; work_units_completed s = work_units_completed s'; equiv_irq_state (machine_state s) (machine_state s'); equiv_for (aag_can_read aag) device_state (machine_state s) (machine_state s'); typ_at (AArch (ADeviceData sz)) (ptrFromPAddr y && ~~ mask (pageBitsForSize sz)) s; \<And>x. aag_can_read aag x \<Longrightarrow> underlying_memory (machine_state s) x = underlying_memory (machine_state s') x; (pasObjectAbs aag (cur_thread s'), Read, pasObjectAbs aag (ptrFromPAddr (y && ~~ mask (pageBitsForSize sz)))) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> aag_can_read aag (ptrFromPAddr y && ~~ mask (pageBitsForSize sz))
 2. \<lbrakk>reads_equiv aag s s'; globals_equiv s s'; invs s; invs s'; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; \<forall>x\<in>ran (kheap s'). obj_valid_pdpt x; is_subject aag (cur_thread s); AllowRead \<in> ptable_rights_s s x; ptable_lift_s s x = Some y; pas_refined aag s; pas_refined aag s'\<rbrakk> \<Longrightarrow> \<not> in_device_frame (ptrFromPAddr y) s \<longrightarrow> \<not> in_device_frame (ptrFromPAddr y) s' proof (prove)
goal (2 subgoals):
 1. \<And>sz. \<lbrakk>globals_equiv s s'; invs s; invs s'; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; \<forall>x\<in>ran (kheap s'). obj_valid_pdpt x; is_subject aag (cur_thread s'); AllowRead \<in> ptable_rights_s s x; ptable_lift_s s x = Some y; pas_refined aag s; pas_refined aag s'; equiv_for (aag_can_read aag) kheap s s'; equiv_for (aag_can_read aag \<circ> fst) cdt s s'; equiv_for (aag_can_read aag \<circ> fst) cdt_list s s'; equiv_for (aag_can_read aag) ekheap s s'; equiv_for (aag_can_read aag \<circ> fst) is_original_cap s s'; equiv_for (aag_can_read_irq aag) interrupt_states s s'; equiv_for (aag_can_read_irq aag) interrupt_irq_node s s'; equiv_asids (aag_can_read_asid aag) s s'; equiv_for (aag_can_read_domain aag) ready_queues s s'; cur_thread s = cur_thread s'; cur_domain s = cur_domain s'; scheduler_action s = scheduler_action s'; work_units_completed s = work_units_completed s'; equiv_irq_state (machine_state s) (machine_state s'); equiv_for (aag_can_read aag) device_state (machine_state s) (machine_state s'); typ_at (AArch (ADeviceData sz)) (ptrFromPAddr y && ~~ mask (pageBitsForSize sz)) s; \<And>x. aag_can_read aag x \<Longrightarrow> underlying_memory (machine_state s) x = underlying_memory (machine_state s') x; (pasObjectAbs aag (cur_thread s'), Read, pasObjectAbs aag (ptrFromPAddr (y && ~~ mask (pageBitsForSize sz)))) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> (pasSubject aag, Read, pasObjectAbs aag (ptrFromPAddr y && ~~ mask (pageBitsForSize sz))) \<in> pasPolicy aag
 2. \<lbrakk>reads_equiv aag s s'; globals_equiv s s'; invs s; invs s'; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; \<forall>x\<in>ran (kheap s'). obj_valid_pdpt x; is_subject aag (cur_thread s); AllowRead \<in> ptable_rights_s s x; ptable_lift_s s x = Some y; pas_refined aag s; pas_refined aag s'\<rbrakk> \<Longrightarrow> \<not> in_device_frame (ptrFromPAddr y) s \<longrightarrow> \<not> in_device_frame (ptrFromPAddr y) s' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>reads_equiv aag s s'; globals_equiv s s'; invs s; invs s'; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; \<forall>x\<in>ran (kheap s'). obj_valid_pdpt x; is_subject aag (cur_thread s); AllowRead \<in> ptable_rights_s s x; ptable_lift_s s x = Some y; pas_refined aag s; pas_refined aag s'\<rbrakk> \<Longrightarrow> \<not> in_device_frame (ptrFromPAddr y) s \<longrightarrow> \<not> in_device_frame (ptrFromPAddr y) s' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>reads_equiv aag s s'; globals_equiv s s'; invs s; invs s'; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; \<forall>x\<in>ran (kheap s'). obj_valid_pdpt x; is_subject aag (cur_thread s); AllowRead \<in> ptable_rights_s s x; ptable_lift_s s x = Some y; pas_refined aag s; pas_refined aag s'; \<not> in_device_frame (ptrFromPAddr y) s; in_device_frame (ptrFromPAddr y) s'\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>reads_equiv aag s s'; globals_equiv s s'; invs s; invs s'; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; \<forall>x\<in>ran (kheap s'). obj_valid_pdpt x; is_subject aag (cur_thread s); AllowRead \<in> ptable_rights_s s x; ptable_lift_s s x = Some y; pas_refined aag s; pas_refined aag s'; \<not> in_device_frame (ptrFromPAddr y) s; in_device_frame (ptrFromPAddr y) s'; ptable_rights_s s = ptable_rights_s s'\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>reads_equiv aag s s'; globals_equiv s s'; invs s; invs s'; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; \<forall>x\<in>ran (kheap s'). obj_valid_pdpt x; is_subject aag (cur_thread s); AllowRead \<in> ptable_rights_s s x; ptable_lift_s s x = Some y; pas_refined aag s; pas_refined aag s'; \<not> in_device_frame (ptrFromPAddr y) s; in_device_frame (ptrFromPAddr y) s'; ptable_rights_s s = ptable_rights_s s'; ptable_lift_s s x = ptable_lift_s s' x\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>reads_equiv aag s s'; invs s; invs s'; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; \<forall>x\<in>ran (kheap s'). obj_valid_pdpt x; is_subject aag (cur_thread s'); AllowRead \<in> ptable_rights_s s' x; ptable_lift_s s' x = Some y; pas_refined aag s; pas_refined aag s'; \<not> in_device_frame (ptrFromPAddr y) s; in_device_frame (ptrFromPAddr y) s'; ptable_rights_s s = ptable_rights_s s'; ptable_lift_s s x = Some y; arm_global_pd (arch_state s) = arm_global_pd (arch_state s'); kheap s (arm_global_pd (arch_state s')) = kheap s' (arm_global_pd (arch_state s')); cur_thread s' \<noteq> idle_thread s \<longrightarrow> exclusive_state (machine_state s) = exclusive_state (machine_state s'); idle_equiv s s'; cur_thread s = cur_thread s'; dom (device_state (machine_state s)) = dom (device_state (machine_state s'))\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>reads_equiv aag s s'; invs s; invs s'; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; \<forall>x\<in>ran (kheap s'). obj_valid_pdpt x; is_subject aag (cur_thread s'); AllowRead \<in> ptable_rights_s s' x; ptable_lift_s s' x = Some y; pas_refined aag s; pas_refined aag s'; in_device_frame (ptrFromPAddr y) s'; ptable_rights_s s = ptable_rights_s s'; ptable_lift_s s x = Some y; arm_global_pd (arch_state s) = arm_global_pd (arch_state s'); kheap s (arm_global_pd (arch_state s')) = kheap s' (arm_global_pd (arch_state s')); cur_thread s' \<noteq> idle_thread s \<longrightarrow> exclusive_state (machine_state s) = exclusive_state (machine_state s'); idle_equiv s s'; cur_thread s = cur_thread s'; dom (device_state (machine_state s)) = dom (device_state (machine_state s'))\<rbrakk> \<Longrightarrow> in_device_frame (ptrFromPAddr y) s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>invs s; invs s'; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; \<forall>x\<in>ran (kheap s'). obj_valid_pdpt x; is_subject aag (cur_thread s'); AllowRead \<in> ptable_rights_s s' x; ptable_lift_s s' x = Some y; pas_refined aag s; pas_refined aag s'; in_device_frame (ptrFromPAddr y) s'; ptable_rights_s s = ptable_rights_s s'; ptable_lift_s s x = Some y; arm_global_pd (arch_state s) = arm_global_pd (arch_state s'); kheap s (arm_global_pd (arch_state s')) = kheap s' (arm_global_pd (arch_state s')); cur_thread s' \<noteq> idle_thread s \<longrightarrow> exclusive_state (machine_state s) = exclusive_state (machine_state s'); idle_equiv s s'; cur_thread s = cur_thread s'; dom (device_state (machine_state s)) = dom (device_state (machine_state s')); equiv_for (aag_can_read aag) kheap s s'; equiv_machine_state (aag_can_read aag) (machine_state s) (machine_state s'); equiv_for (aag_can_read aag \<circ> fst) cdt s s'; equiv_for (aag_can_read aag \<circ> fst) cdt_list s s'; equiv_for (aag_can_read aag) ekheap s s'; equiv_for (aag_can_read aag \<circ> fst) is_original_cap s s'; equiv_for (aag_can_read_irq aag) interrupt_states s s'; equiv_for (aag_can_read_irq aag) interrupt_irq_node s s'; equiv_asids (aag_can_read_asid aag) s s'; equiv_for (aag_can_read_domain aag) ready_queues s s'; cur_thread s = cur_thread s'; cur_domain s = cur_domain s'; scheduler_action s = scheduler_action s'; work_units_completed s = work_units_completed s'; equiv_irq_state (machine_state s) (machine_state s')\<rbrakk> \<Longrightarrow> in_device_frame (ptrFromPAddr y) s proof (prove)
goal (1 subgoal):
 1. \<And>sz. \<lbrakk>invs s; invs s'; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; \<forall>x\<in>ran (kheap s'). obj_valid_pdpt x; is_subject aag (cur_thread s'); AllowRead \<in> ptable_rights_s s' x; ptable_lift_s s' x = Some y; pas_refined aag s; pas_refined aag s'; ptable_rights_s s = ptable_rights_s s'; ptable_lift_s s x = Some y; arm_global_pd (arch_state s) = arm_global_pd (arch_state s'); kheap s (arm_global_pd (arch_state s')) = kheap s' (arm_global_pd (arch_state s')); cur_thread s' \<noteq> idle_thread s \<longrightarrow> exclusive_state (machine_state s) = exclusive_state (machine_state s'); idle_equiv s s'; dom (device_state (machine_state s)) = dom (device_state (machine_state s')); equiv_for (aag_can_read aag) kheap s s'; equiv_for (aag_can_read aag \<circ> fst) cdt s s'; equiv_for (aag_can_read aag \<circ> fst) cdt_list s s'; equiv_for (aag_can_read aag) ekheap s s'; equiv_for (aag_can_read aag \<circ> fst) is_original_cap s s'; equiv_for (aag_can_read_irq aag) interrupt_states s s'; equiv_for (aag_can_read_irq aag) interrupt_irq_node s s'; equiv_asids (aag_can_read_asid aag) s s'; equiv_for (aag_can_read_domain aag) ready_queues s s'; cur_thread s = cur_thread s'; cur_domain s = cur_domain s'; scheduler_action s = scheduler_action s'; work_units_completed s = work_units_completed s'; equiv_irq_state (machine_state s) (machine_state s'); typ_at (AArch (ADeviceData sz)) (ptrFromPAddr y && ~~ mask (pageBitsForSize sz)) s'; equiv_for (aag_can_read aag) underlying_memory (machine_state s) (machine_state s'); equiv_for (aag_can_read aag) device_state (machine_state s) (machine_state s')\<rbrakk> \<Longrightarrow> \<exists>sz. typ_at (AArch (ADeviceData sz)) (ptrFromPAddr y && ~~ mask (pageBitsForSize sz)) s proof (prove)
goal (1 subgoal):
 1. \<And>sz. \<lbrakk>invs s; invs s'; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; \<forall>x\<in>ran (kheap s'). obj_valid_pdpt x; is_subject aag (cur_thread s'); AllowRead \<in> ptable_rights_s s' x; ptable_lift_s s' x = Some y; pas_refined aag s; pas_refined aag s'; ptable_rights_s s = ptable_rights_s s'; ptable_lift_s s x = Some y; arm_global_pd (arch_state s) = arm_global_pd (arch_state s'); kheap s (arm_global_pd (arch_state s')) = kheap s' (arm_global_pd (arch_state s')); cur_thread s' \<noteq> idle_thread s \<longrightarrow> exclusive_state (machine_state s) = exclusive_state (machine_state s'); idle_equiv s s'; dom (device_state (machine_state s)) = dom (device_state (machine_state s')); equiv_for (aag_can_read aag) kheap s s'; equiv_for (aag_can_read aag \<circ> fst) cdt s s'; equiv_for (aag_can_read aag \<circ> fst) cdt_list s s'; equiv_for (aag_can_read aag) ekheap s s'; equiv_for (aag_can_read aag \<circ> fst) is_original_cap s s'; equiv_for (aag_can_read_irq aag) interrupt_states s s'; equiv_for (aag_can_read_irq aag) interrupt_irq_node s s'; equiv_asids (aag_can_read_asid aag) s s'; equiv_for (aag_can_read_domain aag) ready_queues s s'; cur_thread s = cur_thread s'; cur_domain s = cur_domain s'; scheduler_action s = scheduler_action s'; work_units_completed s = work_units_completed s'; equiv_irq_state (machine_state s) (machine_state s'); typ_at (AArch (ADeviceData sz)) (ptrFromPAddr y && ~~ mask (pageBitsForSize sz)) s'; equiv_for (aag_can_read aag) underlying_memory (machine_state s) (machine_state s'); equiv_for (aag_can_read aag) device_state (machine_state s) (machine_state s')\<rbrakk> \<Longrightarrow> typ_at (AArch (ADeviceData (?sz99 sz))) (ptrFromPAddr y && ~~ mask (pageBitsForSize (?sz99 sz))) s proof (prove)
goal (3 subgoals):
 1. \<And>sz. \<lbrakk>invs s; invs s'; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; \<forall>x\<in>ran (kheap s'). obj_valid_pdpt x; is_subject aag (cur_thread s'); AllowRead \<in> ptable_rights_s s' x; ptable_lift_s s' x = Some y; pas_refined aag s; pas_refined aag s'; ptable_rights_s s = ptable_rights_s s'; ptable_lift_s s x = Some y; arm_global_pd (arch_state s) = arm_global_pd (arch_state s'); kheap s (arm_global_pd (arch_state s')) = kheap s' (arm_global_pd (arch_state s')); cur_thread s' \<noteq> idle_thread s \<longrightarrow> exclusive_state (machine_state s) = exclusive_state (machine_state s'); idle_equiv s s'; dom (device_state (machine_state s)) = dom (device_state (machine_state s')); equiv_for (aag_can_read aag) kheap s s'; equiv_for (aag_can_read aag \<circ> fst) cdt s s'; equiv_for (aag_can_read aag \<circ> fst) cdt_list s s'; equiv_for (aag_can_read aag) ekheap s s'; equiv_for (aag_can_read aag \<circ> fst) is_original_cap s s'; equiv_for (aag_can_read_irq aag) interrupt_states s s'; equiv_for (aag_can_read_irq aag) interrupt_irq_node s s'; equiv_asids (aag_can_read_asid aag) s s'; equiv_for (aag_can_read_domain aag) ready_queues s s'; cur_thread s = cur_thread s'; cur_domain s = cur_domain s'; scheduler_action s = scheduler_action s'; work_units_completed s = work_units_completed s'; equiv_irq_state (machine_state s) (machine_state s'); typ_at (AArch (ADeviceData sz)) (ptrFromPAddr y && ~~ mask (pageBitsForSize sz)) s'; equiv_for (aag_can_read aag) underlying_memory (machine_state s) (machine_state s'); equiv_for (aag_can_read aag) device_state (machine_state s) (machine_state s')\<rbrakk> \<Longrightarrow> typ_at (AArch (ADeviceData (?sz99 sz))) (ptrFromPAddr y && ~~ mask (pageBitsForSize (?sz99 sz))) (?s101 sz)
 2. \<And>sz. \<lbrakk>invs s; invs s'; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; \<forall>x\<in>ran (kheap s'). obj_valid_pdpt x; is_subject aag (cur_thread s'); AllowRead \<in> ptable_rights_s s' x; ptable_lift_s s' x = Some y; pas_refined aag s; pas_refined aag s'; ptable_rights_s s = ptable_rights_s s'; ptable_lift_s s x = Some y; arm_global_pd (arch_state s) = arm_global_pd (arch_state s'); kheap s (arm_global_pd (arch_state s')) = kheap s' (arm_global_pd (arch_state s')); cur_thread s' \<noteq> idle_thread s \<longrightarrow> exclusive_state (machine_state s) = exclusive_state (machine_state s'); idle_equiv s s'; dom (device_state (machine_state s)) = dom (device_state (machine_state s')); equiv_for (aag_can_read aag) kheap s s'; equiv_for (aag_can_read aag \<circ> fst) cdt s s'; equiv_for (aag_can_read aag \<circ> fst) cdt_list s s'; equiv_for (aag_can_read aag) ekheap s s'; equiv_for (aag_can_read aag \<circ> fst) is_original_cap s s'; equiv_for (aag_can_read_irq aag) interrupt_states s s'; equiv_for (aag_can_read_irq aag) interrupt_irq_node s s'; equiv_asids (aag_can_read_asid aag) s s'; equiv_for (aag_can_read_domain aag) ready_queues s s'; cur_thread s = cur_thread s'; cur_domain s = cur_domain s'; scheduler_action s = scheduler_action s'; work_units_completed s = work_units_completed s'; equiv_irq_state (machine_state s) (machine_state s'); typ_at (AArch (ADeviceData sz)) (ptrFromPAddr y && ~~ mask (pageBitsForSize sz)) s'; equiv_for (aag_can_read aag) underlying_memory (machine_state s) (machine_state s'); equiv_for (aag_can_read aag) device_state (machine_state s) (machine_state s')\<rbrakk> \<Longrightarrow> equiv_for (?P101 sz) kheap (?s101 sz) s
 3. \<And>sz. \<lbrakk>invs s; invs s'; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; \<forall>x\<in>ran (kheap s'). obj_valid_pdpt x; is_subject aag (cur_thread s'); AllowRead \<in> ptable_rights_s s' x; ptable_lift_s s' x = Some y; pas_refined aag s; pas_refined aag s'; ptable_rights_s s = ptable_rights_s s'; ptable_lift_s s x = Some y; arm_global_pd (arch_state s) = arm_global_pd (arch_state s'); kheap s (arm_global_pd (arch_state s')) = kheap s' (arm_global_pd (arch_state s')); cur_thread s' \<noteq> idle_thread s \<longrightarrow> exclusive_state (machine_state s) = exclusive_state (machine_state s'); idle_equiv s s'; dom (device_state (machine_state s)) = dom (device_state (machine_state s')); equiv_for (aag_can_read aag) kheap s s'; equiv_for (aag_can_read aag \<circ> fst) cdt s s'; equiv_for (aag_can_read aag \<circ> fst) cdt_list s s'; equiv_for (aag_can_read aag) ekheap s s'; equiv_for (aag_can_read aag \<circ> fst) is_original_cap s s'; equiv_for (aag_can_read_irq aag) interrupt_states s s'; equiv_for (aag_can_read_irq aag) interrupt_irq_node s s'; equiv_asids (aag_can_read_asid aag) s s'; equiv_for (aag_can_read_domain aag) ready_queues s s'; cur_thread s = cur_thread s'; cur_domain s = cur_domain s'; scheduler_action s = scheduler_action s'; work_units_completed s = work_units_completed s'; equiv_irq_state (machine_state s) (machine_state s'); typ_at (AArch (ADeviceData sz)) (ptrFromPAddr y && ~~ mask (pageBitsForSize sz)) s'; equiv_for (aag_can_read aag) underlying_memory (machine_state s) (machine_state s'); equiv_for (aag_can_read aag) device_state (machine_state s) (machine_state s')\<rbrakk> \<Longrightarrow> ?P101 sz (ptrFromPAddr y && ~~ mask (pageBitsForSize (?sz99 sz))) proof (prove)
goal (2 subgoals):
 1. \<And>sz. \<lbrakk>invs s; invs s'; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; \<forall>x\<in>ran (kheap s'). obj_valid_pdpt x; is_subject aag (cur_thread s'); AllowRead \<in> ptable_rights_s s' x; ptable_lift_s s' x = Some y; pas_refined aag s; pas_refined aag s'; ptable_rights_s s = ptable_rights_s s'; ptable_lift_s s x = Some y; arm_global_pd (arch_state s) = arm_global_pd (arch_state s'); kheap s (arm_global_pd (arch_state s')) = kheap s' (arm_global_pd (arch_state s')); cur_thread s' \<noteq> idle_thread s \<longrightarrow> exclusive_state (machine_state s) = exclusive_state (machine_state s'); idle_equiv s s'; dom (device_state (machine_state s)) = dom (device_state (machine_state s')); equiv_for (aag_can_read aag) kheap s s'; equiv_for (aag_can_read aag \<circ> fst) cdt s s'; equiv_for (aag_can_read aag \<circ> fst) cdt_list s s'; equiv_for (aag_can_read aag) ekheap s s'; equiv_for (aag_can_read aag \<circ> fst) is_original_cap s s'; equiv_for (aag_can_read_irq aag) interrupt_states s s'; equiv_for (aag_can_read_irq aag) interrupt_irq_node s s'; equiv_asids (aag_can_read_asid aag) s s'; equiv_for (aag_can_read_domain aag) ready_queues s s'; cur_thread s = cur_thread s'; cur_domain s = cur_domain s'; scheduler_action s = scheduler_action s'; work_units_completed s = work_units_completed s'; equiv_irq_state (machine_state s) (machine_state s'); typ_at (AArch (ADeviceData sz)) (ptrFromPAddr y && ~~ mask (pageBitsForSize sz)) s'; equiv_for (aag_can_read aag) underlying_memory (machine_state s) (machine_state s'); equiv_for (aag_can_read aag) device_state (machine_state s) (machine_state s')\<rbrakk> \<Longrightarrow> equiv_for (?P101 sz) kheap s' s
 2. \<And>sz. \<lbrakk>invs s; invs s'; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; \<forall>x\<in>ran (kheap s'). obj_valid_pdpt x; is_subject aag (cur_thread s'); AllowRead \<in> ptable_rights_s s' x; ptable_lift_s s' x = Some y; pas_refined aag s; pas_refined aag s'; ptable_rights_s s = ptable_rights_s s'; ptable_lift_s s x = Some y; arm_global_pd (arch_state s) = arm_global_pd (arch_state s'); kheap s (arm_global_pd (arch_state s')) = kheap s' (arm_global_pd (arch_state s')); cur_thread s' \<noteq> idle_thread s \<longrightarrow> exclusive_state (machine_state s) = exclusive_state (machine_state s'); idle_equiv s s'; dom (device_state (machine_state s)) = dom (device_state (machine_state s')); equiv_for (aag_can_read aag) kheap s s'; equiv_for (aag_can_read aag \<circ> fst) cdt s s'; equiv_for (aag_can_read aag \<circ> fst) cdt_list s s'; equiv_for (aag_can_read aag) ekheap s s'; equiv_for (aag_can_read aag \<circ> fst) is_original_cap s s'; equiv_for (aag_can_read_irq aag) interrupt_states s s'; equiv_for (aag_can_read_irq aag) interrupt_irq_node s s'; equiv_asids (aag_can_read_asid aag) s s'; equiv_for (aag_can_read_domain aag) ready_queues s s'; cur_thread s = cur_thread s'; cur_domain s = cur_domain s'; scheduler_action s = scheduler_action s'; work_units_completed s = work_units_completed s'; equiv_irq_state (machine_state s) (machine_state s'); typ_at (AArch (ADeviceData sz)) (ptrFromPAddr y && ~~ mask (pageBitsForSize sz)) s'; equiv_for (aag_can_read aag) underlying_memory (machine_state s) (machine_state s'); equiv_for (aag_can_read aag) device_state (machine_state s) (machine_state s')\<rbrakk> \<Longrightarrow> ?P101 sz (ptrFromPAddr y && ~~ mask (pageBitsForSize sz)) proof (prove)
goal (2 subgoals):
 1. \<And>sz. \<lbrakk>invs s; invs s'; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; \<forall>x\<in>ran (kheap s'). obj_valid_pdpt x; is_subject aag (cur_thread s'); AllowRead \<in> ptable_rights_s s' x; ptable_lift_s s' x = Some y; pas_refined aag s; pas_refined aag s'; ptable_rights_s s = ptable_rights_s s'; ptable_lift_s s x = Some y; arm_global_pd (arch_state s) = arm_global_pd (arch_state s'); kheap s (arm_global_pd (arch_state s')) = kheap s' (arm_global_pd (arch_state s')); cur_thread s' \<noteq> idle_thread s \<longrightarrow> exclusive_state (machine_state s) = exclusive_state (machine_state s'); idle_equiv s s'; dom (device_state (machine_state s)) = dom (device_state (machine_state s')); equiv_for (aag_can_read aag) kheap s s'; equiv_for (aag_can_read aag \<circ> fst) cdt s s'; equiv_for (aag_can_read aag \<circ> fst) cdt_list s s'; equiv_for (aag_can_read aag) ekheap s s'; equiv_for (aag_can_read aag \<circ> fst) is_original_cap s s'; equiv_for (aag_can_read_irq aag) interrupt_states s s'; equiv_for (aag_can_read_irq aag) interrupt_irq_node s s'; equiv_asids (aag_can_read_asid aag) s s'; equiv_for (aag_can_read_domain aag) ready_queues s s'; cur_thread s = cur_thread s'; cur_domain s = cur_domain s'; scheduler_action s = scheduler_action s'; work_units_completed s = work_units_completed s'; equiv_irq_state (machine_state s) (machine_state s'); typ_at (AArch (ADeviceData sz)) (ptrFromPAddr y && ~~ mask (pageBitsForSize sz)) s'; equiv_for (aag_can_read aag) device_state (machine_state s) (machine_state s'); \<And>x. aag_can_read aag x \<Longrightarrow> underlying_memory (machine_state s) x = underlying_memory (machine_state s') x\<rbrakk> \<Longrightarrow> equiv_for (?P101 sz) kheap s' s
 2. \<And>sz. \<lbrakk>invs s; invs s'; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; \<forall>x\<in>ran (kheap s'). obj_valid_pdpt x; is_subject aag (cur_thread s'); AllowRead \<in> ptable_rights_s s' x; ptable_lift_s s' x = Some y; pas_refined aag s; pas_refined aag s'; ptable_rights_s s = ptable_rights_s s'; ptable_lift_s s x = Some y; arm_global_pd (arch_state s) = arm_global_pd (arch_state s'); kheap s (arm_global_pd (arch_state s')) = kheap s' (arm_global_pd (arch_state s')); cur_thread s' \<noteq> idle_thread s \<longrightarrow> exclusive_state (machine_state s) = exclusive_state (machine_state s'); idle_equiv s s'; dom (device_state (machine_state s)) = dom (device_state (machine_state s')); equiv_for (aag_can_read aag) kheap s s'; equiv_for (aag_can_read aag \<circ> fst) cdt s s'; equiv_for (aag_can_read aag \<circ> fst) cdt_list s s'; equiv_for (aag_can_read aag) ekheap s s'; equiv_for (aag_can_read aag \<circ> fst) is_original_cap s s'; equiv_for (aag_can_read_irq aag) interrupt_states s s'; equiv_for (aag_can_read_irq aag) interrupt_irq_node s s'; equiv_asids (aag_can_read_asid aag) s s'; equiv_for (aag_can_read_domain aag) ready_queues s s'; cur_thread s = cur_thread s'; cur_domain s = cur_domain s'; scheduler_action s = scheduler_action s'; work_units_completed s = work_units_completed s'; equiv_irq_state (machine_state s) (machine_state s'); typ_at (AArch (ADeviceData sz)) (ptrFromPAddr y && ~~ mask (pageBitsForSize sz)) s'; equiv_for (aag_can_read aag) underlying_memory (machine_state s) (machine_state s'); equiv_for (aag_can_read aag) device_state (machine_state s) (machine_state s')\<rbrakk> \<Longrightarrow> ?P101 sz (ptrFromPAddr y && ~~ mask (pageBitsForSize sz)) proof (prove)
goal (1 subgoal):
 1. \<And>sz. \<lbrakk>invs s; invs s'; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; \<forall>x\<in>ran (kheap s'). obj_valid_pdpt x; is_subject aag (cur_thread s'); AllowRead \<in> ptable_rights_s s' x; ptable_lift_s s' x = Some y; pas_refined aag s; pas_refined aag s'; ptable_rights_s s = ptable_rights_s s'; ptable_lift_s s x = Some y; arm_global_pd (arch_state s) = arm_global_pd (arch_state s'); kheap s (arm_global_pd (arch_state s')) = kheap s' (arm_global_pd (arch_state s')); cur_thread s' \<noteq> idle_thread s \<longrightarrow> exclusive_state (machine_state s) = exclusive_state (machine_state s'); idle_equiv s s'; dom (device_state (machine_state s)) = dom (device_state (machine_state s')); equiv_for (aag_can_read aag) kheap s s'; equiv_for (aag_can_read aag \<circ> fst) cdt s s'; equiv_for (aag_can_read aag \<circ> fst) cdt_list s s'; equiv_for (aag_can_read aag) ekheap s s'; equiv_for (aag_can_read aag \<circ> fst) is_original_cap s s'; equiv_for (aag_can_read_irq aag) interrupt_states s s'; equiv_for (aag_can_read_irq aag) interrupt_irq_node s s'; equiv_asids (aag_can_read_asid aag) s s'; equiv_for (aag_can_read_domain aag) ready_queues s s'; cur_thread s = cur_thread s'; cur_domain s = cur_domain s'; scheduler_action s = scheduler_action s'; work_units_completed s = work_units_completed s'; equiv_irq_state (machine_state s) (machine_state s'); typ_at (AArch (ADeviceData sz)) (ptrFromPAddr y && ~~ mask (pageBitsForSize sz)) s'; equiv_for (aag_can_read aag) underlying_memory (machine_state s) (machine_state s'); equiv_for (aag_can_read aag) device_state (machine_state s) (machine_state s')\<rbrakk> \<Longrightarrow> aag_can_read aag (ptrFromPAddr y && ~~ mask (pageBitsForSize sz)) proof (prove)
goal (7 subgoals):
 1. \<And>sz. \<lbrakk>invs s; invs s'; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; \<forall>x\<in>ran (kheap s'). obj_valid_pdpt x; is_subject aag (cur_thread s'); AllowRead \<in> ptable_rights_s s' x; ptable_lift_s s' x = Some y; pas_refined aag s; pas_refined aag s'; ptable_rights_s s = ptable_rights_s s'; ptable_lift_s s x = Some y; arm_global_pd (arch_state s) = arm_global_pd (arch_state s'); kheap s (arm_global_pd (arch_state s')) = kheap s' (arm_global_pd (arch_state s')); cur_thread s' \<noteq> idle_thread s \<longrightarrow> exclusive_state (machine_state s) = exclusive_state (machine_state s'); idle_equiv s s'; dom (device_state (machine_state s)) = dom (device_state (machine_state s')); equiv_for (aag_can_read aag) kheap s s'; equiv_for (aag_can_read aag \<circ> fst) cdt s s'; equiv_for (aag_can_read aag \<circ> fst) cdt_list s s'; equiv_for (aag_can_read aag) ekheap s s'; equiv_for (aag_can_read aag \<circ> fst) is_original_cap s s'; equiv_for (aag_can_read_irq aag) interrupt_states s s'; equiv_for (aag_can_read_irq aag) interrupt_irq_node s s'; equiv_asids (aag_can_read_asid aag) s s'; equiv_for (aag_can_read_domain aag) ready_queues s s'; cur_thread s = cur_thread s'; cur_domain s = cur_domain s'; scheduler_action s = scheduler_action s'; work_units_completed s = work_units_completed s'; equiv_irq_state (machine_state s) (machine_state s'); typ_at (AArch (ADeviceData sz)) (ptrFromPAddr y && ~~ mask (pageBitsForSize sz)) s'; equiv_for (aag_can_read aag) underlying_memory (machine_state s) (machine_state s'); equiv_for (aag_can_read aag) device_state (machine_state s) (machine_state s')\<rbrakk> \<Longrightarrow> \<forall>x\<in>ran (kheap s'). obj_valid_pdpt x
 2. \<And>sz. \<lbrakk>invs s; invs s'; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; \<forall>x\<in>ran (kheap s'). obj_valid_pdpt x; is_subject aag (cur_thread s'); AllowRead \<in> ptable_rights_s s' x; ptable_lift_s s' x = Some y; pas_refined aag s; pas_refined aag s'; ptable_rights_s s = ptable_rights_s s'; ptable_lift_s s x = Some y; arm_global_pd (arch_state s) = arm_global_pd (arch_state s'); kheap s (arm_global_pd (arch_state s')) = kheap s' (arm_global_pd (arch_state s')); cur_thread s' \<noteq> idle_thread s \<longrightarrow> exclusive_state (machine_state s) = exclusive_state (machine_state s'); idle_equiv s s'; dom (device_state (machine_state s)) = dom (device_state (machine_state s')); equiv_for (aag_can_read aag) kheap s s'; equiv_for (aag_can_read aag \<circ> fst) cdt s s'; equiv_for (aag_can_read aag \<circ> fst) cdt_list s s'; equiv_for (aag_can_read aag) ekheap s s'; equiv_for (aag_can_read aag \<circ> fst) is_original_cap s s'; equiv_for (aag_can_read_irq aag) interrupt_states s s'; equiv_for (aag_can_read_irq aag) interrupt_irq_node s s'; equiv_asids (aag_can_read_asid aag) s s'; equiv_for (aag_can_read_domain aag) ready_queues s s'; cur_thread s = cur_thread s'; cur_domain s = cur_domain s'; scheduler_action s = scheduler_action s'; work_units_completed s = work_units_completed s'; equiv_irq_state (machine_state s) (machine_state s'); typ_at (AArch (ADeviceData sz)) (ptrFromPAddr y && ~~ mask (pageBitsForSize sz)) s'; equiv_for (aag_can_read aag) underlying_memory (machine_state s) (machine_state s'); equiv_for (aag_can_read aag) device_state (machine_state s) (machine_state s')\<rbrakk> \<Longrightarrow> pas_refined (?aag109 sz) s'
 3. \<And>sz. \<lbrakk>invs s; invs s'; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; \<forall>x\<in>ran (kheap s'). obj_valid_pdpt x; is_subject aag (cur_thread s'); AllowRead \<in> ptable_rights_s s' x; ptable_lift_s s' x = Some y; pas_refined aag s; pas_refined aag s'; ptable_rights_s s = ptable_rights_s s'; ptable_lift_s s x = Some y; arm_global_pd (arch_state s) = arm_global_pd (arch_state s'); kheap s (arm_global_pd (arch_state s')) = kheap s' (arm_global_pd (arch_state s')); cur_thread s' \<noteq> idle_thread s \<longrightarrow> exclusive_state (machine_state s) = exclusive_state (machine_state s'); idle_equiv s s'; dom (device_state (machine_state s)) = dom (device_state (machine_state s')); equiv_for (aag_can_read aag) kheap s s'; equiv_for (aag_can_read aag \<circ> fst) cdt s s'; equiv_for (aag_can_read aag \<circ> fst) cdt_list s s'; equiv_for (aag_can_read aag) ekheap s s'; equiv_for (aag_can_read aag \<circ> fst) is_original_cap s s'; equiv_for (aag_can_read_irq aag) interrupt_states s s'; equiv_for (aag_can_read_irq aag) interrupt_irq_node s s'; equiv_asids (aag_can_read_asid aag) s s'; equiv_for (aag_can_read_domain aag) ready_queues s s'; cur_thread s = cur_thread s'; cur_domain s = cur_domain s'; scheduler_action s = scheduler_action s'; work_units_completed s = work_units_completed s'; equiv_irq_state (machine_state s) (machine_state s'); typ_at (AArch (ADeviceData sz)) (ptrFromPAddr y && ~~ mask (pageBitsForSize sz)) s'; equiv_for (aag_can_read aag) underlying_memory (machine_state s) (machine_state s'); equiv_for (aag_can_read aag) device_state (machine_state s) (machine_state s')\<rbrakk> \<Longrightarrow> is_subject (?aag109 sz) (?tcb109 sz)
 4. \<And>sz. \<lbrakk>invs s; invs s'; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; \<forall>x\<in>ran (kheap s'). obj_valid_pdpt x; is_subject aag (cur_thread s'); AllowRead \<in> ptable_rights_s s' x; ptable_lift_s s' x = Some y; pas_refined aag s; pas_refined aag s'; ptable_rights_s s = ptable_rights_s s'; ptable_lift_s s x = Some y; arm_global_pd (arch_state s) = arm_global_pd (arch_state s'); kheap s (arm_global_pd (arch_state s')) = kheap s' (arm_global_pd (arch_state s')); cur_thread s' \<noteq> idle_thread s \<longrightarrow> exclusive_state (machine_state s) = exclusive_state (machine_state s'); idle_equiv s s'; dom (device_state (machine_state s)) = dom (device_state (machine_state s')); equiv_for (aag_can_read aag) kheap s s'; equiv_for (aag_can_read aag \<circ> fst) cdt s s'; equiv_for (aag_can_read aag \<circ> fst) cdt_list s s'; equiv_for (aag_can_read aag) ekheap s s'; equiv_for (aag_can_read aag \<circ> fst) is_original_cap s s'; equiv_for (aag_can_read_irq aag) interrupt_states s s'; equiv_for (aag_can_read_irq aag) interrupt_irq_node s s'; equiv_asids (aag_can_read_asid aag) s s'; equiv_for (aag_can_read_domain aag) ready_queues s s'; cur_thread s = cur_thread s'; cur_domain s = cur_domain s'; scheduler_action s = scheduler_action s'; work_units_completed s = work_units_completed s'; equiv_irq_state (machine_state s) (machine_state s'); typ_at (AArch (ADeviceData sz)) (ptrFromPAddr y && ~~ mask (pageBitsForSize sz)) s'; equiv_for (aag_can_read aag) underlying_memory (machine_state s) (machine_state s'); equiv_for (aag_can_read aag) device_state (machine_state s) (machine_state s')\<rbrakk> \<Longrightarrow> ptable_lift (?tcb109 sz) s' (?x109 sz) = Some (?ptr109 sz)
 5. \<And>sz. \<lbrakk>invs s; invs s'; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; \<forall>x\<in>ran (kheap s'). obj_valid_pdpt x; is_subject aag (cur_thread s'); AllowRead \<in> ptable_rights_s s' x; ptable_lift_s s' x = Some y; pas_refined aag s; pas_refined aag s'; ptable_rights_s s = ptable_rights_s s'; ptable_lift_s s x = Some y; arm_global_pd (arch_state s) = arm_global_pd (arch_state s'); kheap s (arm_global_pd (arch_state s')) = kheap s' (arm_global_pd (arch_state s')); cur_thread s' \<noteq> idle_thread s \<longrightarrow> exclusive_state (machine_state s) = exclusive_state (machine_state s'); idle_equiv s s'; dom (device_state (machine_state s)) = dom (device_state (machine_state s')); equiv_for (aag_can_read aag) kheap s s'; equiv_for (aag_can_read aag \<circ> fst) cdt s s'; equiv_for (aag_can_read aag \<circ> fst) cdt_list s s'; equiv_for (aag_can_read aag) ekheap s s'; equiv_for (aag_can_read aag \<circ> fst) is_original_cap s s'; equiv_for (aag_can_read_irq aag) interrupt_states s s'; equiv_for (aag_can_read_irq aag) interrupt_irq_node s s'; equiv_asids (aag_can_read_asid aag) s s'; equiv_for (aag_can_read_domain aag) ready_queues s s'; cur_thread s = cur_thread s'; cur_domain s = cur_domain s'; scheduler_action s = scheduler_action s'; work_units_completed s = work_units_completed s'; equiv_irq_state (machine_state s) (machine_state s'); typ_at (AArch (ADeviceData sz)) (ptrFromPAddr y && ~~ mask (pageBitsForSize sz)) s'; equiv_for (aag_can_read aag) underlying_memory (machine_state s) (machine_state s'); equiv_for (aag_can_read aag) device_state (machine_state s) (machine_state s')\<rbrakk> \<Longrightarrow> data_at (?sz109 sz) (ptrFromPAddr (?ptr109 sz) && ~~ mask (pageBitsForSize (?sz109 sz))) s'
 6. \<And>sz. \<lbrakk>invs s; invs s'; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; \<forall>x\<in>ran (kheap s'). obj_valid_pdpt x; is_subject aag (cur_thread s'); AllowRead \<in> ptable_rights_s s' x; ptable_lift_s s' x = Some y; pas_refined aag s; pas_refined aag s'; ptable_rights_s s = ptable_rights_s s'; ptable_lift_s s x = Some y; arm_global_pd (arch_state s) = arm_global_pd (arch_state s'); kheap s (arm_global_pd (arch_state s')) = kheap s' (arm_global_pd (arch_state s')); cur_thread s' \<noteq> idle_thread s \<longrightarrow> exclusive_state (machine_state s) = exclusive_state (machine_state s'); idle_equiv s s'; dom (device_state (machine_state s)) = dom (device_state (machine_state s')); equiv_for (aag_can_read aag) kheap s s'; equiv_for (aag_can_read aag \<circ> fst) cdt s s'; equiv_for (aag_can_read aag \<circ> fst) cdt_list s s'; equiv_for (aag_can_read aag) ekheap s s'; equiv_for (aag_can_read aag \<circ> fst) is_original_cap s s'; equiv_for (aag_can_read_irq aag) interrupt_states s s'; equiv_for (aag_can_read_irq aag) interrupt_irq_node s s'; equiv_asids (aag_can_read_asid aag) s s'; equiv_for (aag_can_read_domain aag) ready_queues s s'; cur_thread s = cur_thread s'; cur_domain s = cur_domain s'; scheduler_action s = scheduler_action s'; work_units_completed s = work_units_completed s'; equiv_irq_state (machine_state s) (machine_state s'); typ_at (AArch (ADeviceData sz)) (ptrFromPAddr y && ~~ mask (pageBitsForSize sz)) s'; equiv_for (aag_can_read aag) underlying_memory (machine_state s) (machine_state s'); equiv_for (aag_can_read aag) device_state (machine_state s) (machine_state s')\<rbrakk> \<Longrightarrow> Read \<in> vspace_cap_rights_to_auth (ptable_rights (?tcb109 sz) s' (?x109 sz))
 7. \<And>sz. \<lbrakk>invs s; invs s'; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; \<forall>x\<in>ran (kheap s'). obj_valid_pdpt x; is_subject aag (cur_thread s'); AllowRead \<in> ptable_rights_s s' x; ptable_lift_s s' x = Some y; pas_refined aag s; pas_refined aag s'; ptable_rights_s s = ptable_rights_s s'; ptable_lift_s s x = Some y; arm_global_pd (arch_state s) = arm_global_pd (arch_state s'); kheap s (arm_global_pd (arch_state s')) = kheap s' (arm_global_pd (arch_state s')); cur_thread s' \<noteq> idle_thread s \<longrightarrow> exclusive_state (machine_state s) = exclusive_state (machine_state s'); idle_equiv s s'; dom (device_state (machine_state s)) = dom (device_state (machine_state s')); equiv_for (aag_can_read aag) kheap s s'; equiv_for (aag_can_read aag \<circ> fst) cdt s s'; equiv_for (aag_can_read aag \<circ> fst) cdt_list s s'; equiv_for (aag_can_read aag) ekheap s s'; equiv_for (aag_can_read aag \<circ> fst) is_original_cap s s'; equiv_for (aag_can_read_irq aag) interrupt_states s s'; equiv_for (aag_can_read_irq aag) interrupt_irq_node s s'; equiv_asids (aag_can_read_asid aag) s s'; equiv_for (aag_can_read_domain aag) ready_queues s s'; cur_thread s = cur_thread s'; cur_domain s = cur_domain s'; scheduler_action s = scheduler_action s'; work_units_completed s = work_units_completed s'; equiv_irq_state (machine_state s) (machine_state s'); typ_at (AArch (ADeviceData sz)) (ptrFromPAddr y && ~~ mask (pageBitsForSize sz)) s'; equiv_for (aag_can_read aag) underlying_memory (machine_state s) (machine_state s'); equiv_for (aag_can_read aag) device_state (machine_state s) (machine_state s'); (pasObjectAbs (?aag109 sz) (?tcb109 sz), Read, pasObjectAbs (?aag109 sz) (ptrFromPAddr (?ptr109 sz && ~~ mask (pageBitsForSize (?sz109 sz))))) \<in> pasPolicy (?aag109 sz)\<rbrakk> \<Longrightarrow> aag_can_read aag (ptrFromPAddr y && ~~ mask (pageBitsForSize sz)) proof (prove)
goal (1 subgoal):
 1. \<And>sz. \<lbrakk>invs s; invs s'; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; \<forall>x\<in>ran (kheap s'). obj_valid_pdpt x; is_subject aag (cur_thread s'); AllowRead \<in> ptable_rights_s s' x; ptable_lift_s s' x = Some y; pas_refined aag s; pas_refined aag s'; ptable_rights_s s = ptable_rights_s s'; ptable_lift_s s x = Some y; arm_global_pd (arch_state s) = arm_global_pd (arch_state s'); kheap s (arm_global_pd (arch_state s')) = kheap s' (arm_global_pd (arch_state s')); cur_thread s' \<noteq> idle_thread s \<longrightarrow> exclusive_state (machine_state s) = exclusive_state (machine_state s'); idle_equiv s s'; dom (device_state (machine_state s)) = dom (device_state (machine_state s')); equiv_for (aag_can_read aag) kheap s s'; equiv_for (aag_can_read aag \<circ> fst) cdt s s'; equiv_for (aag_can_read aag \<circ> fst) cdt_list s s'; equiv_for (aag_can_read aag) ekheap s s'; equiv_for (aag_can_read aag \<circ> fst) is_original_cap s s'; equiv_for (aag_can_read_irq aag) interrupt_states s s'; equiv_for (aag_can_read_irq aag) interrupt_irq_node s s'; equiv_asids (aag_can_read_asid aag) s s'; equiv_for (aag_can_read_domain aag) ready_queues s s'; cur_thread s = cur_thread s'; cur_domain s = cur_domain s'; scheduler_action s = scheduler_action s'; work_units_completed s = work_units_completed s'; equiv_irq_state (machine_state s) (machine_state s'); typ_at (AArch (ADeviceData sz)) (ptrFromPAddr y && ~~ mask (pageBitsForSize sz)) s'; equiv_for (aag_can_read aag) underlying_memory (machine_state s) (machine_state s'); equiv_for (aag_can_read aag) device_state (machine_state s) (machine_state s'); (pasObjectAbs aag (cur_thread s'), Read, pasObjectAbs aag (ptrFromPAddr (y && ~~ mask (pageBitsForSize sz)))) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> aag_can_read aag (ptrFromPAddr y && ~~ mask (pageBitsForSize sz)) proof (prove)
goal (1 subgoal):
 1. \<And>sz. \<lbrakk>invs s; invs s'; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; \<forall>x\<in>ran (kheap s'). obj_valid_pdpt x; is_subject aag (cur_thread s'); AllowRead \<in> ptable_rights_s s' x; ptable_lift_s s' x = Some y; pas_refined aag s; pas_refined aag s'; ptable_rights_s s = ptable_rights_s s'; ptable_lift_s s x = Some y; arm_global_pd (arch_state s) = arm_global_pd (arch_state s'); kheap s (arm_global_pd (arch_state s')) = kheap s' (arm_global_pd (arch_state s')); cur_thread s' \<noteq> idle_thread s \<longrightarrow> exclusive_state (machine_state s) = exclusive_state (machine_state s'); idle_equiv s s'; dom (device_state (machine_state s)) = dom (device_state (machine_state s')); equiv_for (aag_can_read aag) kheap s s'; equiv_for (aag_can_read aag \<circ> fst) cdt s s'; equiv_for (aag_can_read aag \<circ> fst) cdt_list s s'; equiv_for (aag_can_read aag) ekheap s s'; equiv_for (aag_can_read aag \<circ> fst) is_original_cap s s'; equiv_for (aag_can_read_irq aag) interrupt_states s s'; equiv_for (aag_can_read_irq aag) interrupt_irq_node s s'; equiv_asids (aag_can_read_asid aag) s s'; equiv_for (aag_can_read_domain aag) ready_queues s s'; cur_thread s = cur_thread s'; cur_domain s = cur_domain s'; scheduler_action s = scheduler_action s'; work_units_completed s = work_units_completed s'; equiv_irq_state (machine_state s) (machine_state s'); typ_at (AArch (ADeviceData sz)) (ptrFromPAddr y && ~~ mask (pageBitsForSize sz)) s'; equiv_for (aag_can_read aag) underlying_memory (machine_state s) (machine_state s'); equiv_for (aag_can_read aag) device_state (machine_state s) (machine_state s'); (pasObjectAbs aag (cur_thread s'), Read, pasObjectAbs aag (ptrFromPAddr (y && ~~ mask (pageBitsForSize sz)))) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> (pasSubject aag, Read, pasObjectAbs aag (ptrFromPAddr y && ~~ mask (pageBitsForSize sz))) \<in> pasPolicy aag proof (prove)
goal:
No subgoals!