theory ArchUserOp_IF

lemma requiv_user_device_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_state (machine_state s) (ptrFromPAddr y) =
         device_state (machine_state s') (ptrFromPAddr y)" apply (simp add: ptable_lift_s_def) apply (frule ptable_rights_imp_frameD) apply fastforce apply (fastforce simp: ptable_rights_s_def) apply (erule reads_equivE) apply clarsimp apply (erule_tac f="device_state" in equiv_forD) 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_user_data_at)+)[6] apply (rule reads_read) apply (frule_tac auth=Read in user_op_access) apply (fastforce simp: ptable_lift_s_def ptable_rights_s_def vspace_cap_rights_to_auth_def)+ 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_state (machine_state s) (ptrFromPAddr y) = device_state (machine_state 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 (cur_thread s) s x = Some y; pas_refined aag s; pas_refined aag s'\<rbrakk> \<Longrightarrow> device_state (machine_state s) (ptrFromPAddr y) = device_state (machine_state s') (ptrFromPAddr y) proof (prove)
goal (3 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 (cur_thread s) s x = Some y; pas_refined aag s; pas_refined aag s'\<rbrakk> \<Longrightarrow> valid_state 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 (cur_thread s) s x = Some y; pas_refined aag s; pas_refined aag s'\<rbrakk> \<Longrightarrow> ptable_rights (cur_thread s) s x \<noteq> {}
 3. \<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 (cur_thread s) s x = Some y; pas_refined aag s; pas_refined aag s'; \<exists>sz. data_at sz (ptrFromPAddr y && ~~ mask (pageBitsForSize sz)) s\<rbrakk> \<Longrightarrow> device_state (machine_state s) (ptrFromPAddr y) = device_state (machine_state s') (ptrFromPAddr y) 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 (cur_thread s) s x = Some y; pas_refined aag s; pas_refined aag s'\<rbrakk> \<Longrightarrow> ptable_rights (cur_thread s) s x \<noteq> {}
 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 (cur_thread s) s x = Some y; pas_refined aag s; pas_refined aag s'; \<exists>sz. data_at sz (ptrFromPAddr y && ~~ mask (pageBitsForSize sz)) s\<rbrakk> \<Longrightarrow> device_state (machine_state s) (ptrFromPAddr y) = device_state (machine_state 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 (cur_thread s) s x = Some y; pas_refined aag s; pas_refined aag s'; \<exists>sz. data_at sz (ptrFromPAddr y && ~~ mask (pageBitsForSize sz)) s\<rbrakk> \<Longrightarrow> device_state (machine_state s) (ptrFromPAddr y) = device_state (machine_state s') (ptrFromPAddr y) proof (prove)
goal (1 subgoal):
 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 (cur_thread s) s x = Some y; pas_refined aag s; pas_refined aag s'; \<exists>sz. data_at sz (ptrFromPAddr y && ~~ mask (pageBitsForSize sz)) 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> device_state (machine_state s) (ptrFromPAddr y) = device_state (machine_state s') (ptrFromPAddr y) proof (prove)
goal (1 subgoal):
 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 (cur_thread 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'); data_at 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> device_state (machine_state s) (ptrFromPAddr y) = device_state (machine_state s') (ptrFromPAddr y) proof (prove)
goal (1 subgoal):
 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 (cur_thread 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'); data_at sz (ptrFromPAddr y && ~~ mask (pageBitsForSize sz)) s; equiv_for (aag_can_read aag) underlying_memory (machine_state s) (machine_state s')\<rbrakk> \<Longrightarrow> aag_can_read aag (ptrFromPAddr y) proof (prove)
goal (7 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 (cur_thread 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'); data_at sz (ptrFromPAddr y && ~~ mask (pageBitsForSize sz)) s; equiv_for (aag_can_read aag) underlying_memory (machine_state s) (machine_state s')\<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 (cur_thread 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'); data_at sz (ptrFromPAddr y && ~~ mask (pageBitsForSize sz)) s; equiv_for (aag_can_read aag) underlying_memory (machine_state s) (machine_state s')\<rbrakk> \<Longrightarrow> pas_refined (?aag16 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 (cur_thread 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'); data_at sz (ptrFromPAddr y && ~~ mask (pageBitsForSize sz)) s; equiv_for (aag_can_read aag) underlying_memory (machine_state s) (machine_state s')\<rbrakk> \<Longrightarrow> is_subject (?aag16 sz) (?tcb16 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 (cur_thread 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'); data_at sz (ptrFromPAddr y && ~~ mask (pageBitsForSize sz)) s; equiv_for (aag_can_read aag) underlying_memory (machine_state s) (machine_state s')\<rbrakk> \<Longrightarrow> ptable_lift (?tcb16 sz) s (?x16 sz) = Some (?ptr16 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 (cur_thread 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'); data_at sz (ptrFromPAddr y && ~~ mask (pageBitsForSize sz)) s; equiv_for (aag_can_read aag) underlying_memory (machine_state s) (machine_state s')\<rbrakk> \<Longrightarrow> data_at (?sz16 sz) (ptrFromPAddr (?ptr16 sz) && ~~ mask (pageBitsForSize (?sz16 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 (cur_thread 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'); data_at sz (ptrFromPAddr y && ~~ mask (pageBitsForSize sz)) s; equiv_for (aag_can_read aag) underlying_memory (machine_state s) (machine_state s')\<rbrakk> \<Longrightarrow> Read \<in> vspace_cap_rights_to_auth (ptable_rights (?tcb16 sz) s (?x16 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 (cur_thread 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'); data_at sz (ptrFromPAddr y && ~~ mask (pageBitsForSize sz)) s; equiv_for (aag_can_read aag) underlying_memory (machine_state s) (machine_state s'); (pasObjectAbs (?aag16 sz) (?tcb16 sz), Read, pasObjectAbs (?aag16 sz) (ptrFromPAddr (?ptr16 sz && ~~ mask (pageBitsForSize (?sz16 sz))))) \<in> pasPolicy (?aag16 sz)\<rbrakk> \<Longrightarrow> aag_can_read aag (ptrFromPAddr y) proof (prove)
goal (1 subgoal):
 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 (cur_thread 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'); data_at sz (ptrFromPAddr y && ~~ mask (pageBitsForSize sz)) s; equiv_for (aag_can_read aag) underlying_memory (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) proof (prove)
goal (1 subgoal):
 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 (cur_thread 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'); data_at sz (ptrFromPAddr y && ~~ mask (pageBitsForSize sz)) s; equiv_for (aag_can_read aag) underlying_memory (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)) \<in> pasPolicy aag proof (prove)
goal (5 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 (cur_thread 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'); data_at sz (ptrFromPAddr y && ~~ mask (pageBitsForSize sz)) s; equiv_for (aag_can_read aag) underlying_memory (machine_state s) (machine_state s'); (pasObjectAbs aag (cur_thread s'), Read, pasObjectAbs aag (ptrFromPAddr (y && ~~ mask (pageBitsForSize sz)))) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> pas_refined (?aag32 sz) s
 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 (cur_thread 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'); data_at sz (ptrFromPAddr y && ~~ mask (pageBitsForSize sz)) s; equiv_for (aag_can_read aag) underlying_memory (machine_state s) (machine_state s'); (pasObjectAbs aag (cur_thread s'), Read, pasObjectAbs aag (ptrFromPAddr (y && ~~ mask (pageBitsForSize sz)))) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> is_subject (?aag32 sz) (?tcb32 sz)
 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 (cur_thread 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'); data_at sz (ptrFromPAddr y && ~~ mask (pageBitsForSize sz)) s; equiv_for (aag_can_read aag) underlying_memory (machine_state s) (machine_state s'); (pasObjectAbs aag (cur_thread s'), Read, pasObjectAbs aag (ptrFromPAddr (y && ~~ mask (pageBitsForSize sz)))) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> ptable_lift (?tcb32 sz) s (?x32 sz) = Some (?ptr32 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 (cur_thread 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'); data_at sz (ptrFromPAddr y && ~~ mask (pageBitsForSize sz)) s; equiv_for (aag_can_read aag) underlying_memory (machine_state s) (machine_state s'); (pasObjectAbs aag (cur_thread s'), Read, pasObjectAbs aag (ptrFromPAddr (y && ~~ mask (pageBitsForSize sz)))) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> Read \<in> vspace_cap_rights_to_auth (ptable_rights (?tcb32 sz) s (?x32 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 (cur_thread 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'); data_at sz (ptrFromPAddr y && ~~ mask (pageBitsForSize sz)) s; equiv_for (aag_can_read aag) underlying_memory (machine_state s) (machine_state s'); (pasObjectAbs aag (cur_thread s'), Read, pasObjectAbs aag (ptrFromPAddr (y && ~~ mask (pageBitsForSize sz)))) \<in> pasPolicy aag; (pasObjectAbs (?aag32 sz) (?tcb32 sz), Read, pasObjectAbs (?aag32 sz) (ptrFromPAddr (?ptr32 sz))) \<in> pasPolicy (?aag32 sz)\<rbrakk> \<Longrightarrow> (pasSubject aag, Read, pasObjectAbs aag (ptrFromPAddr y)) \<in> pasPolicy aag proof (prove)
goal:
No subgoals!