theory ArchRetype_AI

lemma valid_asid_map:
  "valid_asid_map s \<Longrightarrow> valid_asid_map s'" apply (clarsimp simp: valid_asid_map_def) apply (drule bspec, blast) apply (clarsimp simp: vspace_at_asid_def) apply (drule vs_lookup_2ConsD) apply clarsimp apply (erule vs_lookup_atE) apply (drule vs_lookup1D) apply clarsimp apply (drule obj_at_pres) apply (fastforce simp: vs_asid_refs_def graph_of_def
                  intro: vs_lookupI vs_lookup1I) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_asid_map s \<Longrightarrow> valid_asid_map s' proof (prove)
goal (1 subgoal):
 1. \<And>a aa b. \<lbrakk>(a, aa, b) \<in> graph_of (arm_asid_map (arch_state s)); dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; \<forall>x\<in>graph_of (arm_asid_map (arch_state s)). case x of (asid, hwasid, pd) \<Rightarrow> vspace_at_asid asid pd s \<and> asid \<noteq> 0\<rbrakk> \<Longrightarrow> vspace_at_asid a b s' \<and> a \<noteq> 0 proof (prove)
goal (1 subgoal):
 1. \<And>a aa b. \<lbrakk>(a, aa, b) \<in> graph_of (arm_asid_map (arch_state s)); dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; case (a, aa, b) of (asid, hwasid, pd) \<Rightarrow> vspace_at_asid asid pd s \<and> asid \<noteq> 0\<rbrakk> \<Longrightarrow> vspace_at_asid a b s' \<and> a \<noteq> 0 proof (prove)
goal (1 subgoal):
 1. \<And>a aa b. \<lbrakk>(a, aa, b) \<in> graph_of (arm_asid_map (arch_state s)); dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; ([VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) None] \<rhd> b) s; a \<noteq> 0\<rbrakk> \<Longrightarrow> ([VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) None] \<rhd> b) s' proof (prove)
goal (1 subgoal):
 1. \<And>a aa b. \<lbrakk>(a, aa, b) \<in> graph_of (arm_asid_map (arch_state s)); dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; a \<noteq> 0; \<exists>p'. ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) None] \<rhd> p') s \<and> (([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) None], p'), [VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) None], b) \<in> vs_lookup1 s\<rbrakk> \<Longrightarrow> ([VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) None] \<rhd> b) s' proof (prove)
goal (1 subgoal):
 1. \<And>a aa b p'. \<lbrakk>(a, aa, b) \<in> graph_of (arm_asid_map (arch_state s)); dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; a \<noteq> 0; ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) None] \<rhd> p') s; (([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) None], p'), [VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) None], b) \<in> vs_lookup1 s\<rbrakk> \<Longrightarrow> ([VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) None] \<rhd> b) s' proof (prove)
goal (1 subgoal):
 1. \<And>a aa b p'. \<lbrakk>(a, aa, b) \<in> graph_of (arm_asid_map (arch_state s)); dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; a \<noteq> 0; (([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) None], p'), [VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) None], b) \<in> vs_lookup1 s; asid_table s (asid_high_bits_of a) = Some p'\<rbrakk> \<Longrightarrow> ([VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) None] \<rhd> b) s' proof (prove)
goal (1 subgoal):
 1. \<And>a aa b p'. \<lbrakk>(a, aa, b) \<in> graph_of (arm_asid_map (arch_state s)); dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; a \<noteq> 0; asid_table s (asid_high_bits_of a) = Some p'; \<exists>rs r p p'a ko. ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) None], p') = (rs, p) \<and> ([VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) None], b) = (r # rs, p'a) \<and> ko_at ko p s \<and> (r, p'a) \<in> vs_refs ko\<rbrakk> \<Longrightarrow> ([VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) None] \<rhd> b) s' proof (prove)
goal (1 subgoal):
 1. \<And>a aa b p' ko. \<lbrakk>(a, aa, b) \<in> graph_of (arm_asid_map (arch_state s)); dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; a \<noteq> 0; asid_table s (asid_high_bits_of a) = Some p'; ko_at ko p' s; (VSRef (a && mask local.asid_low_bits) (Some AASIDPool), b) \<in> vs_refs ko\<rbrakk> \<Longrightarrow> ([VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) None] \<rhd> b) s' proof (prove)
goal (1 subgoal):
 1. \<And>a aa b p' ko. \<lbrakk>(a, aa, b) \<in> graph_of (arm_asid_map (arch_state s)); dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; a \<noteq> 0; asid_table s (asid_high_bits_of a) = Some p'; (VSRef (a && mask local.asid_low_bits) (Some AASIDPool), b) \<in> vs_refs ko; ko_at ko p' s'\<rbrakk> \<Longrightarrow> ([VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) None] \<rhd> b) s' proof (prove)
goal:
No subgoals!