theory ArchRetype_AC

lemma pas_refined:
  "\<lbrakk> invs s; pas_refined aag s \<rbrakk> \<Longrightarrow> pas_refined aag s'" apply (erule pas_refined_state_objs_to_policy_subset) apply (simp add: state_objs_to_policy_def refs_eq vrefs_eq mdb_and_revokable) apply (rule subsetI, rename_tac x, case_tac x, simp) apply (erule state_bits_to_policy.cases) apply (solves \<open>auto intro!: sbta_caps intro: caps_retype split: cap.split\<close>) apply (solves \<open>auto intro!: sbta_untyped intro: caps_retype split: cap.split\<close>) apply (blast intro: state_bits_to_policy.intros) apply (blast intro: state_bits_to_policy.intros) apply (force intro!: sbta_cdt
                       dest: caps_of_state_pres invs_mdb_cte'[THEN mdb_cte_atD[rotated]]) apply (force intro!: sbta_cdt_transferable
                      dest: caps_of_state_pres invs_mdb_cte'[THEN mdb_cte_atD[rotated]]) apply (simp add: vrefs_eq) apply (blast intro: state_bits_to_policy.intros) apply (simp add: vrefs_eq) apply (force elim!: state_asids_to_policy_aux.cases
                 intro: state_asids_to_policy_aux.intros caps_retype
                 split: cap.split
                 dest: sata_asid[OF caps_retype, rotated]) apply clarsimp apply (erule state_irqs_to_policy_aux.cases) apply (solves\<open>auto intro!: sita_controlled intro: caps_retype split: cap.split\<close>) apply (rule domains_of_state) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>invs s; pas_refined aag s\<rbrakk> \<Longrightarrow> pas_refined aag s' proof (prove)
goal (5 subgoals):
 1. invs s \<Longrightarrow> state_objs_to_policy s' \<subseteq> state_objs_to_policy s
 2. invs s \<Longrightarrow> state_asids_to_policy aag s' \<subseteq> state_asids_to_policy aag s
 3. invs s \<Longrightarrow> state_irqs_to_policy aag s' \<subseteq> state_irqs_to_policy aag s
 4. invs s \<Longrightarrow> domains_of_state s' \<subseteq> domains_of_state s
 5. invs s \<Longrightarrow> interrupt_irq_node s' = interrupt_irq_node s proof (prove)
goal (5 subgoals):
 1. invs s \<Longrightarrow> state_bits_to_policy (caps_of_state s') (thread_st_auth s) (thread_bound_ntfns s) (cdt s) (state_vrefs s) \<subseteq> state_bits_to_policy (caps_of_state s) (thread_st_auth s) (thread_bound_ntfns s) (cdt s) (state_vrefs s)
 2. invs s \<Longrightarrow> state_asids_to_policy aag s' \<subseteq> state_asids_to_policy aag s
 3. invs s \<Longrightarrow> state_irqs_to_policy aag s' \<subseteq> state_irqs_to_policy aag s
 4. invs s \<Longrightarrow> domains_of_state s' \<subseteq> domains_of_state s
 5. invs s \<Longrightarrow> interrupt_irq_node s' = interrupt_irq_node s proof (prove)
goal (5 subgoals):
 1. \<And>x a b c. \<lbrakk>invs s; (a, b, c) \<in> state_bits_to_policy (caps_of_state s') (thread_st_auth s) (thread_bound_ntfns s) (cdt s) (state_vrefs s); x = (a, b, c)\<rbrakk> \<Longrightarrow> (a, b, c) \<in> state_bits_to_policy (caps_of_state s) (thread_st_auth s) (thread_bound_ntfns s) (cdt s) (state_vrefs s)
 2. invs s \<Longrightarrow> state_asids_to_policy aag s' \<subseteq> state_asids_to_policy aag s
 3. invs s \<Longrightarrow> state_irqs_to_policy aag s' \<subseteq> state_irqs_to_policy aag s
 4. invs s \<Longrightarrow> domains_of_state s' \<subseteq> domains_of_state s
 5. invs s \<Longrightarrow> interrupt_irq_node s' = interrupt_irq_node s proof (prove)
goal (11 subgoals):
 1. \<And>x a b c ptr cap oref auth. \<lbrakk>invs s; x = (a, b, c); a = fst ptr; b = auth; c = oref; caps_of_state s' ptr = Some cap; oref \<in> obj_refs_ac cap; auth \<in> cap_auth_conferred cap\<rbrakk> \<Longrightarrow> (a, b, c) \<in> state_bits_to_policy (caps_of_state s) (thread_st_auth s) (thread_bound_ntfns s) (cdt s) (state_vrefs s)
 2. \<And>x a b c ptr cap oref. \<lbrakk>invs s; x = (a, b, c); a = fst ptr; b = Control; c = oref; caps_of_state s' ptr = Some cap; oref \<in> untyped_range cap\<rbrakk> \<Longrightarrow> (a, b, c) \<in> state_bits_to_policy (caps_of_state s) (thread_st_auth s) (thread_bound_ntfns s) (cdt s) (state_vrefs s)
 3. \<And>x a b c oref' auth oref. \<lbrakk>invs s; x = (a, b, c); a = oref; b = auth; c = oref'; (oref', auth) \<in> thread_st_auth s oref\<rbrakk> \<Longrightarrow> (a, b, c) \<in> state_bits_to_policy (caps_of_state s) (thread_st_auth s) (thread_bound_ntfns s) (cdt s) (state_vrefs s)
 4. \<And>x a b c oref oref' auth. \<lbrakk>invs s; x = (a, b, c); a = oref; b = auth; c = oref'; thread_bound_ntfns s oref = Some oref'; auth \<in> {Receive, Reset}\<rbrakk> \<Longrightarrow> (a, b, c) \<in> state_bits_to_policy (caps_of_state s) (thread_st_auth s) (thread_bound_ntfns s) (cdt s) (state_vrefs s)
 5. \<And>x a b c slot' slot. \<lbrakk>invs s; x = (a, b, c); a = fst slot; b = Control; c = fst slot'; cdt s slot' = Some slot; \<not> is_transferable_in slot' s'\<rbrakk> \<Longrightarrow> (a, b, c) \<in> state_bits_to_policy (caps_of_state s) (thread_st_auth s) (thread_bound_ntfns s) (cdt s) (state_vrefs s)
 6. \<And>x a b c slot' slot. \<lbrakk>invs s; x = (a, b, c); a = fst slot; b = DeleteDerived; c = fst slot'; cdt s slot' = Some slot\<rbrakk> \<Longrightarrow> (a, b, c) \<in> state_bits_to_policy (caps_of_state s) (thread_st_auth s) (thread_bound_ntfns s) (cdt s) (state_vrefs s)
 7. \<And>x a b c ptr' uu_ uv_ auth ptr. \<lbrakk>invs s; x = (a, b, c); a = ptr; b = auth; c = ptr'; (ptr', uu_, uv_, auth) \<in> state_vrefs s ptr\<rbrakk> \<Longrightarrow> (a, b, c) \<in> state_bits_to_policy (caps_of_state s) (thread_st_auth s) (thread_bound_ntfns s) (cdt s) (state_vrefs s)
 8. invs s \<Longrightarrow> state_asids_to_policy aag s' \<subseteq> state_asids_to_policy aag s
 9. invs s \<Longrightarrow> state_irqs_to_policy aag s' \<subseteq> state_irqs_to_policy aag s
 10. invs s \<Longrightarrow> domains_of_state s' \<subseteq> domains_of_state s
A total of 11 subgoals... proof (prove)
goal (10 subgoals):
 1. \<And>x a b c ptr cap oref. \<lbrakk>invs s; x = (a, b, c); a = fst ptr; b = Control; c = oref; caps_of_state s' ptr = Some cap; oref \<in> untyped_range cap\<rbrakk> \<Longrightarrow> (a, b, c) \<in> state_bits_to_policy (caps_of_state s) (thread_st_auth s) (thread_bound_ntfns s) (cdt s) (state_vrefs s)
 2. \<And>x a b c oref' auth oref. \<lbrakk>invs s; x = (a, b, c); a = oref; b = auth; c = oref'; (oref', auth) \<in> thread_st_auth s oref\<rbrakk> \<Longrightarrow> (a, b, c) \<in> state_bits_to_policy (caps_of_state s) (thread_st_auth s) (thread_bound_ntfns s) (cdt s) (state_vrefs s)
 3. \<And>x a b c oref oref' auth. \<lbrakk>invs s; x = (a, b, c); a = oref; b = auth; c = oref'; thread_bound_ntfns s oref = Some oref'; auth \<in> {Receive, Reset}\<rbrakk> \<Longrightarrow> (a, b, c) \<in> state_bits_to_policy (caps_of_state s) (thread_st_auth s) (thread_bound_ntfns s) (cdt s) (state_vrefs s)
 4. \<And>x a b c slot' slot. \<lbrakk>invs s; x = (a, b, c); a = fst slot; b = Control; c = fst slot'; cdt s slot' = Some slot; \<not> is_transferable_in slot' s'\<rbrakk> \<Longrightarrow> (a, b, c) \<in> state_bits_to_policy (caps_of_state s) (thread_st_auth s) (thread_bound_ntfns s) (cdt s) (state_vrefs s)
 5. \<And>x a b c slot' slot. \<lbrakk>invs s; x = (a, b, c); a = fst slot; b = DeleteDerived; c = fst slot'; cdt s slot' = Some slot\<rbrakk> \<Longrightarrow> (a, b, c) \<in> state_bits_to_policy (caps_of_state s) (thread_st_auth s) (thread_bound_ntfns s) (cdt s) (state_vrefs s)
 6. \<And>x a b c ptr' uu_ uv_ auth ptr. \<lbrakk>invs s; x = (a, b, c); a = ptr; b = auth; c = ptr'; (ptr', uu_, uv_, auth) \<in> state_vrefs s ptr\<rbrakk> \<Longrightarrow> (a, b, c) \<in> state_bits_to_policy (caps_of_state s) (thread_st_auth s) (thread_bound_ntfns s) (cdt s) (state_vrefs s)
 7. invs s \<Longrightarrow> state_asids_to_policy aag s' \<subseteq> state_asids_to_policy aag s
 8. invs s \<Longrightarrow> state_irqs_to_policy aag s' \<subseteq> state_irqs_to_policy aag s
 9. invs s \<Longrightarrow> domains_of_state s' \<subseteq> domains_of_state s
 10. invs s \<Longrightarrow> interrupt_irq_node s' = interrupt_irq_node s proof (prove)
goal (9 subgoals):
 1. \<And>x a b c oref' auth oref. \<lbrakk>invs s; x = (a, b, c); a = oref; b = auth; c = oref'; (oref', auth) \<in> thread_st_auth s oref\<rbrakk> \<Longrightarrow> (a, b, c) \<in> state_bits_to_policy (caps_of_state s) (thread_st_auth s) (thread_bound_ntfns s) (cdt s) (state_vrefs s)
 2. \<And>x a b c oref oref' auth. \<lbrakk>invs s; x = (a, b, c); a = oref; b = auth; c = oref'; thread_bound_ntfns s oref = Some oref'; auth \<in> {Receive, Reset}\<rbrakk> \<Longrightarrow> (a, b, c) \<in> state_bits_to_policy (caps_of_state s) (thread_st_auth s) (thread_bound_ntfns s) (cdt s) (state_vrefs s)
 3. \<And>x a b c slot' slot. \<lbrakk>invs s; x = (a, b, c); a = fst slot; b = Control; c = fst slot'; cdt s slot' = Some slot; \<not> is_transferable_in slot' s'\<rbrakk> \<Longrightarrow> (a, b, c) \<in> state_bits_to_policy (caps_of_state s) (thread_st_auth s) (thread_bound_ntfns s) (cdt s) (state_vrefs s)
 4. \<And>x a b c slot' slot. \<lbrakk>invs s; x = (a, b, c); a = fst slot; b = DeleteDerived; c = fst slot'; cdt s slot' = Some slot\<rbrakk> \<Longrightarrow> (a, b, c) \<in> state_bits_to_policy (caps_of_state s) (thread_st_auth s) (thread_bound_ntfns s) (cdt s) (state_vrefs s)
 5. \<And>x a b c ptr' uu_ uv_ auth ptr. \<lbrakk>invs s; x = (a, b, c); a = ptr; b = auth; c = ptr'; (ptr', uu_, uv_, auth) \<in> state_vrefs s ptr\<rbrakk> \<Longrightarrow> (a, b, c) \<in> state_bits_to_policy (caps_of_state s) (thread_st_auth s) (thread_bound_ntfns s) (cdt s) (state_vrefs s)
 6. invs s \<Longrightarrow> state_asids_to_policy aag s' \<subseteq> state_asids_to_policy aag s
 7. invs s \<Longrightarrow> state_irqs_to_policy aag s' \<subseteq> state_irqs_to_policy aag s
 8. invs s \<Longrightarrow> domains_of_state s' \<subseteq> domains_of_state s
 9. invs s \<Longrightarrow> interrupt_irq_node s' = interrupt_irq_node s proof (prove)
goal (8 subgoals):
 1. \<And>x a b c oref oref' auth. \<lbrakk>invs s; x = (a, b, c); a = oref; b = auth; c = oref'; thread_bound_ntfns s oref = Some oref'; auth \<in> {Receive, Reset}\<rbrakk> \<Longrightarrow> (a, b, c) \<in> state_bits_to_policy (caps_of_state s) (thread_st_auth s) (thread_bound_ntfns s) (cdt s) (state_vrefs s)
 2. \<And>x a b c slot' slot. \<lbrakk>invs s; x = (a, b, c); a = fst slot; b = Control; c = fst slot'; cdt s slot' = Some slot; \<not> is_transferable_in slot' s'\<rbrakk> \<Longrightarrow> (a, b, c) \<in> state_bits_to_policy (caps_of_state s) (thread_st_auth s) (thread_bound_ntfns s) (cdt s) (state_vrefs s)
 3. \<And>x a b c slot' slot. \<lbrakk>invs s; x = (a, b, c); a = fst slot; b = DeleteDerived; c = fst slot'; cdt s slot' = Some slot\<rbrakk> \<Longrightarrow> (a, b, c) \<in> state_bits_to_policy (caps_of_state s) (thread_st_auth s) (thread_bound_ntfns s) (cdt s) (state_vrefs s)
 4. \<And>x a b c ptr' uu_ uv_ auth ptr. \<lbrakk>invs s; x = (a, b, c); a = ptr; b = auth; c = ptr'; (ptr', uu_, uv_, auth) \<in> state_vrefs s ptr\<rbrakk> \<Longrightarrow> (a, b, c) \<in> state_bits_to_policy (caps_of_state s) (thread_st_auth s) (thread_bound_ntfns s) (cdt s) (state_vrefs s)
 5. invs s \<Longrightarrow> state_asids_to_policy aag s' \<subseteq> state_asids_to_policy aag s
 6. invs s \<Longrightarrow> state_irqs_to_policy aag s' \<subseteq> state_irqs_to_policy aag s
 7. invs s \<Longrightarrow> domains_of_state s' \<subseteq> domains_of_state s
 8. invs s \<Longrightarrow> interrupt_irq_node s' = interrupt_irq_node s proof (prove)
goal (7 subgoals):
 1. \<And>x a b c slot' slot. \<lbrakk>invs s; x = (a, b, c); a = fst slot; b = Control; c = fst slot'; cdt s slot' = Some slot; \<not> is_transferable_in slot' s'\<rbrakk> \<Longrightarrow> (a, b, c) \<in> state_bits_to_policy (caps_of_state s) (thread_st_auth s) (thread_bound_ntfns s) (cdt s) (state_vrefs s)
 2. \<And>x a b c slot' slot. \<lbrakk>invs s; x = (a, b, c); a = fst slot; b = DeleteDerived; c = fst slot'; cdt s slot' = Some slot\<rbrakk> \<Longrightarrow> (a, b, c) \<in> state_bits_to_policy (caps_of_state s) (thread_st_auth s) (thread_bound_ntfns s) (cdt s) (state_vrefs s)
 3. \<And>x a b c ptr' uu_ uv_ auth ptr. \<lbrakk>invs s; x = (a, b, c); a = ptr; b = auth; c = ptr'; (ptr', uu_, uv_, auth) \<in> state_vrefs s ptr\<rbrakk> \<Longrightarrow> (a, b, c) \<in> state_bits_to_policy (caps_of_state s) (thread_st_auth s) (thread_bound_ntfns s) (cdt s) (state_vrefs s)
 4. invs s \<Longrightarrow> state_asids_to_policy aag s' \<subseteq> state_asids_to_policy aag s
 5. invs s \<Longrightarrow> state_irqs_to_policy aag s' \<subseteq> state_irqs_to_policy aag s
 6. invs s \<Longrightarrow> domains_of_state s' \<subseteq> domains_of_state s
 7. invs s \<Longrightarrow> interrupt_irq_node s' = interrupt_irq_node s proof (prove)
goal (6 subgoals):
 1. \<And>x a b c slot' slot. \<lbrakk>invs s; x = (a, b, c); a = fst slot; b = DeleteDerived; c = fst slot'; cdt s slot' = Some slot\<rbrakk> \<Longrightarrow> (a, b, c) \<in> state_bits_to_policy (caps_of_state s) (thread_st_auth s) (thread_bound_ntfns s) (cdt s) (state_vrefs s)
 2. \<And>x a b c ptr' uu_ uv_ auth ptr. \<lbrakk>invs s; x = (a, b, c); a = ptr; b = auth; c = ptr'; (ptr', uu_, uv_, auth) \<in> state_vrefs s ptr\<rbrakk> \<Longrightarrow> (a, b, c) \<in> state_bits_to_policy (caps_of_state s) (thread_st_auth s) (thread_bound_ntfns s) (cdt s) (state_vrefs s)
 3. invs s \<Longrightarrow> state_asids_to_policy aag s' \<subseteq> state_asids_to_policy aag s
 4. invs s \<Longrightarrow> state_irqs_to_policy aag s' \<subseteq> state_irqs_to_policy aag s
 5. invs s \<Longrightarrow> domains_of_state s' \<subseteq> domains_of_state s
 6. invs s \<Longrightarrow> interrupt_irq_node s' = interrupt_irq_node s proof (prove)
goal (5 subgoals):
 1. \<And>x a b c ptr' uu_ uv_ auth ptr. \<lbrakk>invs s; x = (a, b, c); a = ptr; b = auth; c = ptr'; (ptr', uu_, uv_, auth) \<in> state_vrefs s ptr\<rbrakk> \<Longrightarrow> (a, b, c) \<in> state_bits_to_policy (caps_of_state s) (thread_st_auth s) (thread_bound_ntfns s) (cdt s) (state_vrefs s)
 2. invs s \<Longrightarrow> state_asids_to_policy aag s' \<subseteq> state_asids_to_policy aag s
 3. invs s \<Longrightarrow> state_irqs_to_policy aag s' \<subseteq> state_irqs_to_policy aag s
 4. invs s \<Longrightarrow> domains_of_state s' \<subseteq> domains_of_state s
 5. invs s \<Longrightarrow> interrupt_irq_node s' = interrupt_irq_node s proof (prove)
goal (5 subgoals):
 1. \<And>x a b c ptr' uu_ uv_ auth ptr. \<lbrakk>invs s; x = (ptr, auth, ptr'); a = ptr; b = auth; c = ptr'; (ptr', uu_, uv_, auth) \<in> state_vrefs s ptr\<rbrakk> \<Longrightarrow> (ptr, auth, ptr') \<in> state_bits_to_policy (caps_of_state s) (thread_st_auth s) (thread_bound_ntfns s) (cdt s) (state_vrefs s)
 2. invs s \<Longrightarrow> state_asids_to_policy aag s' \<subseteq> state_asids_to_policy aag s
 3. invs s \<Longrightarrow> state_irqs_to_policy aag s' \<subseteq> state_irqs_to_policy aag s
 4. invs s \<Longrightarrow> domains_of_state s' \<subseteq> domains_of_state s
 5. invs s \<Longrightarrow> interrupt_irq_node s' = interrupt_irq_node s proof (prove)
goal (4 subgoals):
 1. invs s \<Longrightarrow> state_asids_to_policy aag s' \<subseteq> state_asids_to_policy aag s
 2. invs s \<Longrightarrow> state_irqs_to_policy aag s' \<subseteq> state_irqs_to_policy aag s
 3. invs s \<Longrightarrow> domains_of_state s' \<subseteq> domains_of_state s
 4. invs s \<Longrightarrow> interrupt_irq_node s' = interrupt_irq_node s proof (prove)
goal (4 subgoals):
 1. invs s \<Longrightarrow> state_asids_to_policy_aux aag (caps_of_state s') (asid_table s) (state_vrefs s) \<subseteq> state_asids_to_policy_aux aag (caps_of_state s) (asid_table s) (state_vrefs s)
 2. invs s \<Longrightarrow> state_irqs_to_policy aag s' \<subseteq> state_irqs_to_policy aag s
 3. invs s \<Longrightarrow> domains_of_state s' \<subseteq> domains_of_state s
 4. invs s \<Longrightarrow> interrupt_irq_node s' = interrupt_irq_node s proof (prove)
goal (3 subgoals):
 1. invs s \<Longrightarrow> state_irqs_to_policy aag s' \<subseteq> state_irqs_to_policy aag s
 2. invs s \<Longrightarrow> domains_of_state s' \<subseteq> domains_of_state s
 3. invs s \<Longrightarrow> interrupt_irq_node s' = interrupt_irq_node s proof (prove)
goal (3 subgoals):
 1. \<And>a aa b. \<lbrakk>invs s; (a, aa, b) \<in> state_irqs_to_policy aag s'\<rbrakk> \<Longrightarrow> (a, aa, b) \<in> state_irqs_to_policy aag s
 2. invs s \<Longrightarrow> domains_of_state s' \<subseteq> domains_of_state s
 3. invs s \<Longrightarrow> interrupt_irq_node s' = interrupt_irq_node s proof (prove)
goal (3 subgoals):
 1. \<And>a aa b ptr cap irq. \<lbrakk>invs s; a = pasObjectAbs aag (fst ptr); aa = Control; b = pasIRQAbs aag irq; caps_of_state s' ptr = Some cap; irq \<in> cap_irqs_controlled cap\<rbrakk> \<Longrightarrow> (a, aa, b) \<in> state_irqs_to_policy aag s
 2. invs s \<Longrightarrow> domains_of_state s' \<subseteq> domains_of_state s
 3. invs s \<Longrightarrow> interrupt_irq_node s' = interrupt_irq_node s proof (prove)
goal (2 subgoals):
 1. invs s \<Longrightarrow> domains_of_state s' \<subseteq> domains_of_state s
 2. invs s \<Longrightarrow> interrupt_irq_node s' = interrupt_irq_node s proof (prove)
goal (1 subgoal):
 1. invs s \<Longrightarrow> interrupt_irq_node s' = interrupt_irq_node s proof (prove)
goal:
No subgoals!