theory ArchArch_AC

lemma find_pd_for_asid_authority1:
  "\<lbrace>pas_refined aag\<rbrace>
   find_pd_for_asid asid
   \<lbrace>\<lambda>pd _. (pasASIDAbs aag asid, Control, pasObjectAbs aag pd) \<in> pasPolicy aag\<rbrace>,-" apply (rule hoare_pre) apply (simp add: find_pd_for_asid_def) apply (wp | wpc)+ apply (clarsimp simp: obj_at_def pas_refined_def) apply (erule subsetD, erule sata_asid_lookup) apply (simp add: state_vrefs_def vs_refs_no_global_pts_def image_def) apply (rule rev_bexI, erule graph_ofI) apply (simp add: mask_asid_low_bits_ucast_ucast) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pas_refined aag\<rbrace> find_pd_for_asid asid \<lbrace>\<lambda>pd _. (pasASIDAbs aag asid, Control, pasObjectAbs aag pd) \<in> pasPolicy aag\<rbrace>, - proof (prove)
goal (2 subgoals):
 1. \<lbrace>?P'\<rbrace> find_pd_for_asid asid \<lbrace>\<lambda>pd _. (pasASIDAbs aag asid, Control, pasObjectAbs aag pd) \<in> pasPolicy aag\<rbrace>, -
 2. \<And>s. pas_refined aag s \<Longrightarrow> ?P' s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?P'\<rbrace> doE y <- assertE (0 < asid);
asid_table <- liftE (gets (arm_asid_table \<circ> arch_state));
pool <- case asid_table (asid_high_bits_of asid) of None \<Rightarrow> throwError InvalidRoot | Some ptr \<Rightarrow> liftE (get_asid_pool ptr);
case pool (UCAST(32 \<rightarrow> 10) asid) of None \<Rightarrow> throwError InvalidRoot | Some x2 \<Rightarrow> returnOk x2
odE \<lbrace>\<lambda>pd _. (pasASIDAbs aag asid, Control, pasObjectAbs aag pd) \<in> pasPolicy aag\<rbrace>, -
 2. \<And>s. pas_refined aag s \<Longrightarrow> ?P' s proof (prove)
goal (1 subgoal):
 1. \<And>s. pas_refined aag s \<Longrightarrow> 0 < asid \<longrightarrow> True \<and> True \<and> ((arm_asid_table \<circ> arch_state) s (asid_high_bits_of asid) = None \<longrightarrow> True) \<and> (\<forall>x. (arm_asid_table \<circ> arch_state) s (asid_high_bits_of asid) = Some x \<longrightarrow> (\<forall>pool. ako_at (ASIDPool pool) x s \<longrightarrow> (pool (UCAST(32 \<rightarrow> 10) asid) = None \<longrightarrow> True) \<and> (\<forall>x. pool (UCAST(32 \<rightarrow> 10) asid) = Some x \<longrightarrow> (pasASIDAbs aag asid, Control, pasObjectAbs aag x) \<in> pasPolicy aag))) proof (prove)
goal (1 subgoal):
 1. \<And>s x pool xa. \<lbrakk>pas_wellformed aag; irq_map_wellformed aag s; tcb_domain_map_wellformed aag s; state_objs_in_policy aag s; state_asids_to_policy_aux aag (caps_of_state s) (asid_table s) (state_vrefs s) \<subseteq> pasPolicy aag; state_irqs_to_policy aag s \<subseteq> pasPolicy aag; 0 < asid; asid_table s (asid_high_bits_of asid) = Some x; kheap s x = Some (ArchObj (ASIDPool pool)); pool (UCAST(32 \<rightarrow> 10) asid) = Some xa\<rbrakk> \<Longrightarrow> (pasASIDAbs aag asid, Control, pasObjectAbs aag xa) \<in> pasPolicy aag proof (prove)
goal (1 subgoal):
 1. \<And>s x pool xa. \<lbrakk>pas_wellformed aag; irq_map_wellformed aag s; tcb_domain_map_wellformed aag s; state_objs_in_policy aag s; state_irqs_to_policy aag s \<subseteq> pasPolicy aag; 0 < asid; kheap s x = Some (ArchObj (ASIDPool pool)); pool (UCAST(32 \<rightarrow> 10) asid) = Some xa\<rbrakk> \<Longrightarrow> (xa, asid && mask local.asid_low_bits, AASIDPool, Control) \<in> state_vrefs s x proof (prove)
goal (1 subgoal):
 1. \<And>s x pool xa. \<lbrakk>policy_wellformed (pasPolicy aag) (pasMaySendIrqs aag) {y. \<exists>x. y = pasIRQAbs aag x} (pasSubject aag); irq_map_wellformed aag s; tcb_domain_map_wellformed aag s; state_objs_in_policy aag s; state_irqs_to_policy aag s \<subseteq> pasPolicy aag; 0 < asid; kheap s x = Some (ArchObj (ASIDPool pool)); pool (UCAST(32 \<rightarrow> 10) asid) = Some xa\<rbrakk> \<Longrightarrow> \<exists>x\<in>graph_of pool. (xa, asid && mask local.asid_low_bits, AASIDPool, Control) = (case x of (r, p) \<Rightarrow> (p, UCAST(10 \<rightarrow> 32) r, AASIDPool, Control)) proof (prove)
goal (1 subgoal):
 1. \<And>s x pool xa. \<lbrakk>policy_wellformed (pasPolicy aag) (pasMaySendIrqs aag) {y. \<exists>x. y = pasIRQAbs aag x} (pasSubject aag); irq_map_wellformed aag s; tcb_domain_map_wellformed aag s; state_objs_in_policy aag s; state_irqs_to_policy aag s \<subseteq> pasPolicy aag; 0 < asid; kheap s x = Some (ArchObj (ASIDPool pool)); pool (UCAST(32 \<rightarrow> 10) asid) = Some xa\<rbrakk> \<Longrightarrow> (xa, asid && mask local.asid_low_bits, AASIDPool, Control) = (case (UCAST(32 \<rightarrow> 10) asid, xa) of (r, p) \<Rightarrow> (p, UCAST(10 \<rightarrow> 32) r, AASIDPool, Control)) proof (prove)
goal:
No subgoals!