theory ArchArch_AC

lemma pas_refined_set_asid_strg:
  "pas_refined aag s \<and> is_subject aag pool \<and>
   (\<forall>asid. asid_high_bits_of asid = base \<longrightarrow> is_subject_asid aag asid)
   \<longrightarrow> pas_refined aag (s\<lparr>arch_state :=
                          arch_state s\<lparr>arm_asid_table := (arm_asid_table (arch_state s))(base \<mapsto> pool)\<rparr>\<rparr>)" apply (clarsimp simp: pas_refined_def state_objs_to_policy_def) apply (erule state_asids_to_policy_aux.cases, simp_all split: if_split_asm) apply (auto intro: state_asids_to_policy_aux.intros auth_graph_map_memI[OF sbta_vref]
                 intro!: pas_refined_refl[simplified pas_refined_def state_objs_to_policy_def]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. pas_refined aag s \<and> is_subject aag pool \<and> (\<forall>asid. asid_high_bits_of asid = base \<longrightarrow> is_subject_asid aag asid) \<longrightarrow> pas_refined aag (s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := (asid_table s)(base \<mapsto> pool)\<rparr>\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>a aa b. \<lbrakk>(a, aa, b) \<in> state_asids_to_policy_aux aag (caps_of_state s) ((asid_table s)(base \<mapsto> pool)) (state_vrefs s); pas_wellformed aag; irq_map_wellformed aag s; tcb_domain_map_wellformed aag s; auth_graph_map (pasObjectAbs aag) (state_bits_to_policy (caps_of_state s) (thread_st_auth s) (thread_bound_ntfns s) (cdt s) (state_vrefs s)) \<subseteq> pasPolicy aag; 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; is_subject aag pool; \<forall>asid. asid_high_bits_of asid = base \<longrightarrow> is_subject_asid aag asid\<rbrakk> \<Longrightarrow> (a, aa, b) \<in> pasPolicy aag proof (prove)
goal (5 subgoals):
 1. \<And>a aa b ptr acap asid. \<lbrakk>pas_wellformed aag; irq_map_wellformed aag s; tcb_domain_map_wellformed aag s; auth_graph_map (pasObjectAbs aag) (state_bits_to_policy (caps_of_state s) (thread_st_auth s) (thread_bound_ntfns s) (cdt s) (state_vrefs s)) \<subseteq> pasPolicy aag; 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; is_subject aag pool; \<forall>asid. asid_high_bits_of asid = base \<longrightarrow> is_subject_asid aag asid; a = pasObjectAbs aag (fst ptr); aa = Control; b = pasASIDAbs aag asid; caps_of_state s ptr = Some (ArchObjectCap acap); asid \<in> acap_asid' acap\<rbrakk> \<Longrightarrow> (pasObjectAbs aag (fst ptr), Control, pasASIDAbs aag asid) \<in> pasPolicy aag
 2. \<And>a aa b asid poolptr pdptr ab. \<lbrakk>(pdptr, asid && mask local.asid_low_bits, AASIDPool, ab) \<in> state_vrefs s poolptr; pas_wellformed aag; irq_map_wellformed aag s; tcb_domain_map_wellformed aag s; auth_graph_map (pasObjectAbs aag) (state_bits_to_policy (caps_of_state s) (thread_st_auth s) (thread_bound_ntfns s) (cdt s) (state_vrefs s)) \<subseteq> pasPolicy aag; 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; is_subject aag poolptr; \<forall>asid. asid_high_bits_of asid = base \<longrightarrow> is_subject_asid aag asid; a = pasSubject aag; aa = ab; b = pasObjectAbs aag pdptr; asid_high_bits_of asid = base; pool = poolptr\<rbrakk> \<Longrightarrow> (pasSubject aag, ab, pasObjectAbs aag pdptr) \<in> pasPolicy aag
 3. \<And>a aa b asid poolptr pdptr ab. \<lbrakk>(pdptr, asid && mask local.asid_low_bits, AASIDPool, ab) \<in> state_vrefs s poolptr; pas_wellformed aag; irq_map_wellformed aag s; tcb_domain_map_wellformed aag s; auth_graph_map (pasObjectAbs aag) (state_bits_to_policy (caps_of_state s) (thread_st_auth s) (thread_bound_ntfns s) (cdt s) (state_vrefs s)) \<subseteq> pasPolicy aag; 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; is_subject aag pool; \<forall>asid. asid_high_bits_of asid = base \<longrightarrow> is_subject_asid aag asid; a = pasASIDAbs aag asid; aa = ab; b = pasObjectAbs aag pdptr; asid_high_bits_of asid \<noteq> base; asid_table s (asid_high_bits_of asid) = Some poolptr\<rbrakk> \<Longrightarrow> (pasASIDAbs aag asid, ab, pasObjectAbs aag pdptr) \<in> pasPolicy aag
 4. \<And>a aa b asid poolptr. \<lbrakk>asid \<noteq> 0; pas_wellformed aag; irq_map_wellformed aag s; tcb_domain_map_wellformed aag s; auth_graph_map (pasObjectAbs aag) (state_bits_to_policy (caps_of_state s) (thread_st_auth s) (thread_bound_ntfns s) (cdt s) (state_vrefs s)) \<subseteq> pasPolicy aag; 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; is_subject aag poolptr; \<forall>asid. asid_high_bits_of asid = base \<longrightarrow> is_subject_asid aag asid; a = pasSubject aag; aa = AAuth ASIDPoolMapsASID; b = pasSubject aag; asid_high_bits_of asid = base; pool = poolptr\<rbrakk> \<Longrightarrow> (pasSubject aag, AAuth ASIDPoolMapsASID, pasSubject aag) \<in> pasPolicy aag
 5. \<And>a aa b asid poolptr. \<lbrakk>asid \<noteq> 0; pas_wellformed aag; irq_map_wellformed aag s; tcb_domain_map_wellformed aag s; auth_graph_map (pasObjectAbs aag) (state_bits_to_policy (caps_of_state s) (thread_st_auth s) (thread_bound_ntfns s) (cdt s) (state_vrefs s)) \<subseteq> pasPolicy aag; 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; is_subject aag pool; \<forall>asid. asid_high_bits_of asid = base \<longrightarrow> is_subject_asid aag asid; a = pasObjectAbs aag poolptr; aa = AAuth ASIDPoolMapsASID; b = pasASIDAbs aag asid; asid_high_bits_of asid \<noteq> base; asid_table s (asid_high_bits_of asid) = Some poolptr\<rbrakk> \<Longrightarrow> (pasObjectAbs aag poolptr, AAuth ASIDPoolMapsASID, pasASIDAbs aag asid) \<in> pasPolicy aag proof (prove)
goal:
No subgoals!