theory ArchArch_AI

lemma valid_asid_map':
  "valid_asid_map s \<Longrightarrow> valid_asid_map s'" using empty apply (clarsimp simp: valid_asid_map_def s'_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 (rule vs_lookupI[rotated]) apply (rule r_into_rtrancl) apply (rule vs_lookup1I) apply (fastforce simp: obj_at_def) apply assumption apply simp apply (clarsimp simp: vs_asid_refs_def graph_of_def) apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_asid_map s \<Longrightarrow> valid_asid_map s' proof (prove)
using this:
asid_table s asid = None

goal (1 subgoal):
 1. valid_asid_map s \<Longrightarrow> valid_asid_map s' proof (prove)
goal (1 subgoal):
 1. \<And>a aa b. \<lbrakk>asid_table s asid = None; (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\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := (asid_table s)(asid \<mapsto> ap)\<rparr>\<rparr>) \<and> a \<noteq> 0 proof (prove)
goal (1 subgoal):
 1. \<And>a aa b. \<lbrakk>asid_table s asid = None; (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\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := (asid_table s)(asid \<mapsto> ap)\<rparr>\<rparr>) \<and> a \<noteq> 0 proof (prove)
goal (1 subgoal):
 1. \<And>a aa b. \<lbrakk>asid_table s asid = None; (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\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := (asid_table s)(asid \<mapsto> ap)\<rparr>\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>a aa b. \<lbrakk>asid_table s asid = None; (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\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := (asid_table s)(asid \<mapsto> ap)\<rparr>\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>a aa b p'. \<lbrakk>asid_table s asid = None; (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\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := (asid_table s)(asid \<mapsto> ap)\<rparr>\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>a aa b p'. \<lbrakk>asid_table s asid = None; (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\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := (asid_table s)(asid \<mapsto> ap)\<rparr>\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>a aa b p'. \<lbrakk>asid_table s asid = None; (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\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := (asid_table s)(asid \<mapsto> ap)\<rparr>\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>a aa b p' ko. \<lbrakk>asid_table s asid = None; (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\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := (asid_table s)(asid \<mapsto> ap)\<rparr>\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>a aa b p' ko. \<lbrakk>asid_table s asid = None; (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> (?ref'25 a aa b p' ko, [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\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := (asid_table s)(asid \<mapsto> ap)\<rparr>\<rparr>))\<^sup>*
 2. \<And>a aa b p' ko. \<lbrakk>asid_table s asid = None; (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> ?ref'25 a aa b p' ko \<in> vs_asid_refs (asid_table (s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := (asid_table s)(asid \<mapsto> ap)\<rparr>\<rparr>)) proof (prove)
goal (2 subgoals):
 1. \<And>a aa b p' ko. \<lbrakk>asid_table s asid = None; (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> (?ref'25 a aa b p' ko, [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\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := (asid_table s)(asid \<mapsto> ap)\<rparr>\<rparr>)
 2. \<And>a aa b p' ko. \<lbrakk>asid_table s asid = None; (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> ?ref'25 a aa b p' ko \<in> vs_asid_refs (asid_table (s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := (asid_table s)(asid \<mapsto> ap)\<rparr>\<rparr>)) proof (prove)
goal (4 subgoals):
 1. \<And>a aa b p' ko. \<lbrakk>asid_table s asid = None; (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> ko_at (?ko30 a aa b p' ko) (?p30 a aa b p' ko) (s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := (asid_table s)(asid \<mapsto> ap)\<rparr>\<rparr>)
 2. \<And>a aa b p' ko. \<lbrakk>asid_table s asid = None; (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> (?r30 a aa b p' ko, b) \<in> vs_refs (?ko30 a aa b p' ko)
 3. \<And>a aa b p' ko. \<lbrakk>asid_table s asid = None; (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] = ?r30 a aa b p' ko # ?rs30 a aa b p' ko
 4. \<And>a aa b p' ko. \<lbrakk>asid_table s asid = None; (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> (?rs30 a aa b p' ko, ?p30 a aa b p' ko) \<in> vs_asid_refs (asid_table (s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := (asid_table s)(asid \<mapsto> ap)\<rparr>\<rparr>)) proof (prove)
goal (3 subgoals):
 1. \<And>a aa b p' ko. \<lbrakk>asid_table s asid = None; (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> (?r30 a aa b p' ko, b) \<in> vs_refs ko
 2. \<And>a aa b p' ko. \<lbrakk>asid_table s asid = None; (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] = ?r30 a aa b p' ko # ?rs30 a aa b p' ko
 3. \<And>a aa b p' ko. \<lbrakk>asid_table s asid = None; (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> (?rs30 a aa b p' ko, p') \<in> vs_asid_refs (asid_table (s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := (asid_table s)(asid \<mapsto> ap)\<rparr>\<rparr>)) proof (prove)
goal (2 subgoals):
 1. \<And>a aa b p' ko. \<lbrakk>asid_table s asid = None; (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] = VSRef (a && mask local.asid_low_bits) (Some AASIDPool) # ?rs30 a aa b p' ko
 2. \<And>a aa b p' ko. \<lbrakk>asid_table s asid = None; (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> (?rs30 a aa b p' ko, p') \<in> vs_asid_refs (asid_table (s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := (asid_table s)(asid \<mapsto> ap)\<rparr>\<rparr>)) proof (prove)
goal (1 subgoal):
 1. \<And>a aa b p' ko. \<lbrakk>asid_table s asid = None; (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 (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) None], p') \<in> vs_asid_refs (asid_table (s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := (asid_table s)(asid \<mapsto> ap)\<rparr>\<rparr>)) proof (prove)
goal (1 subgoal):
 1. \<And>a aa b p' ko. \<lbrakk>asid_table s asid = None; arm_asid_map (arch_state s) a = Some (aa, b); 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 (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) None], p') \<in> (\<lambda>x. case x of (r, p) \<Rightarrow> ([VSRef (UCAST(7 \<rightarrow> 32) r) None], p)) ` {(x, y). (if x = asid then Some ap else asid_table s x) = Some y} proof (prove)
goal:
No subgoals!