theory ArchUserOp_IF

lemma requiv_get_pd_entry_eq:
  "\<lbrakk> reads_equiv aag s s'; is_subject aag pd \<rbrakk>
     \<Longrightarrow> get_pd_entry (\<lambda>obj. get_arch_obj (kheap s obj)) pd x =
         get_pd_entry (\<lambda>obj. get_arch_obj (kheap s' obj)) pd x" apply (erule reads_equivE) apply (erule equiv_forE) apply (subgoal_tac "aag_can_read aag pd") apply (simp add: get_pd_entry_def split: option.splits) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>reads_equiv aag s s'; is_subject aag pd\<rbrakk> \<Longrightarrow> get_pd_entry (\<lambda>obj. get_arch_obj (kheap s obj)) pd x = get_pd_entry (\<lambda>obj. get_arch_obj (kheap s' obj)) pd x proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_subject aag pd; 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> get_pd_entry (\<lambda>obj. get_arch_obj (kheap s obj)) pd x = get_pd_entry (\<lambda>obj. get_arch_obj (kheap s' obj)) pd x proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_subject aag pd; 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'); \<And>x. aag_can_read aag x \<Longrightarrow> kheap s x = kheap s' x\<rbrakk> \<Longrightarrow> get_pd_entry (\<lambda>obj. get_arch_obj (kheap s obj)) pd x = get_pd_entry (\<lambda>obj. get_arch_obj (kheap s' obj)) pd x proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_subject aag pd; 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'); \<And>x. aag_can_read aag x \<Longrightarrow> kheap s x = kheap s' x; aag_can_read aag pd\<rbrakk> \<Longrightarrow> get_pd_entry (\<lambda>obj. get_arch_obj (kheap s obj)) pd x = get_pd_entry (\<lambda>obj. get_arch_obj (kheap s' obj)) pd x
 2. \<lbrakk>is_subject aag pd; 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'); \<And>x. aag_can_read aag x \<Longrightarrow> kheap s x = kheap s' x\<rbrakk> \<Longrightarrow> aag_can_read aag pd proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_subject aag pd; 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'); \<And>x. aag_can_read aag x \<Longrightarrow> kheap s x = kheap s' x\<rbrakk> \<Longrightarrow> aag_can_read aag pd proof (prove)
goal:
No subgoals!