theory ArchInvariants_AI

lemma vs_lookup_atD:
  "([VSRef (ucast asid) None] \<rhd> p) s \<Longrightarrow> arm_asid_table (arch_state s) asid = Some p" apply (simp add: vs_lookup_def) apply (clarsimp simp: vs_asid_refs_def graph_of_def) apply (drule rtranclD) apply (erule disjE) apply (clarsimp simp: up_ucast_inj_eq) apply clarsimp apply (drule tranclD2) apply (clarsimp simp: up_ucast_inj_eq) apply (drule vs_lookup1D) apply (clarsimp simp: vs_refs_def) apply (clarsimp split: split: kernel_object.splits arch_kernel_obj.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ([VSRef (UCAST(7 \<rightarrow> 32) asid) None] \<rhd> p) s \<Longrightarrow> asid_table s asid = Some p proof (prove)
goal (1 subgoal):
 1. ([VSRef (UCAST(7 \<rightarrow> 32) asid) None], p) \<in> (vs_lookup1 s)\<^sup>* `` vs_asid_refs (asid_table s) \<Longrightarrow> asid_table s asid = Some p proof (prove)
goal (1 subgoal):
 1. \<And>aa ba. \<lbrakk>(([VSRef (UCAST(7 \<rightarrow> 32) aa) None], ba), [VSRef (UCAST(7 \<rightarrow> 32) asid) None], p) \<in> (vs_lookup1 s)\<^sup>*; asid_table s aa = Some ba\<rbrakk> \<Longrightarrow> asid_table s asid = Some p proof (prove)
goal (1 subgoal):
 1. \<And>aa ba. \<lbrakk>asid_table s aa = Some ba; ([VSRef (UCAST(7 \<rightarrow> 32) aa) None], ba) = ([VSRef (UCAST(7 \<rightarrow> 32) asid) None], p) \<or> ([VSRef (UCAST(7 \<rightarrow> 32) aa) None], ba) \<noteq> ([VSRef (UCAST(7 \<rightarrow> 32) asid) None], p) \<and> (([VSRef (UCAST(7 \<rightarrow> 32) aa) None], ba), [VSRef (UCAST(7 \<rightarrow> 32) asid) None], p) \<in> (vs_lookup1 s)\<^sup>+\<rbrakk> \<Longrightarrow> asid_table s asid = Some p proof (prove)
goal (2 subgoals):
 1. \<And>aa ba. \<lbrakk>asid_table s aa = Some ba; ([VSRef (UCAST(7 \<rightarrow> 32) aa) None], ba) = ([VSRef (UCAST(7 \<rightarrow> 32) asid) None], p)\<rbrakk> \<Longrightarrow> asid_table s asid = Some p
 2. \<And>aa ba. \<lbrakk>asid_table s aa = Some ba; ([VSRef (UCAST(7 \<rightarrow> 32) aa) None], ba) \<noteq> ([VSRef (UCAST(7 \<rightarrow> 32) asid) None], p) \<and> (([VSRef (UCAST(7 \<rightarrow> 32) aa) None], ba), [VSRef (UCAST(7 \<rightarrow> 32) asid) None], p) \<in> (vs_lookup1 s)\<^sup>+\<rbrakk> \<Longrightarrow> asid_table s asid = Some p proof (prove)
goal (1 subgoal):
 1. \<And>aa ba. \<lbrakk>asid_table s aa = Some ba; ([VSRef (UCAST(7 \<rightarrow> 32) aa) None], ba) \<noteq> ([VSRef (UCAST(7 \<rightarrow> 32) asid) None], p) \<and> (([VSRef (UCAST(7 \<rightarrow> 32) aa) None], ba), [VSRef (UCAST(7 \<rightarrow> 32) asid) None], p) \<in> (vs_lookup1 s)\<^sup>+\<rbrakk> \<Longrightarrow> asid_table s asid = Some p proof (prove)
goal (1 subgoal):
 1. \<And>aa ba. \<lbrakk>asid_table s aa = Some ba; UCAST(7 \<rightarrow> 32) aa = UCAST(7 \<rightarrow> 32) asid \<longrightarrow> ba \<noteq> p; (([VSRef (UCAST(7 \<rightarrow> 32) aa) None], ba), [VSRef (UCAST(7 \<rightarrow> 32) asid) None], p) \<in> (vs_lookup1 s)\<^sup>+\<rbrakk> \<Longrightarrow> asid_table s asid = Some p proof (prove)
goal (1 subgoal):
 1. \<And>aa ba. \<lbrakk>asid_table s aa = Some ba; UCAST(7 \<rightarrow> 32) aa = UCAST(7 \<rightarrow> 32) asid \<longrightarrow> ba \<noteq> p; \<exists>z. (([VSRef (UCAST(7 \<rightarrow> 32) aa) None], ba), z) \<in> (vs_lookup1 s)\<^sup>* \<and> (z, [VSRef (UCAST(7 \<rightarrow> 32) asid) None], p) \<in> vs_lookup1 s\<rbrakk> \<Longrightarrow> asid_table s asid = Some p proof (prove)
goal (1 subgoal):
 1. \<And>aa ba a b. \<lbrakk>asid_table s aa = Some ba; aa = asid \<longrightarrow> ba \<noteq> p; (([VSRef (UCAST(7 \<rightarrow> 32) aa) None], ba), a, b) \<in> (vs_lookup1 s)\<^sup>*; ((a, b), [VSRef (UCAST(7 \<rightarrow> 32) asid) None], p) \<in> vs_lookup1 s\<rbrakk> \<Longrightarrow> asid_table s asid = Some p proof (prove)
goal (1 subgoal):
 1. \<And>aa ba a b. \<lbrakk>asid_table s aa = Some ba; aa = asid \<longrightarrow> ba \<noteq> p; (([VSRef (UCAST(7 \<rightarrow> 32) aa) None], ba), a, b) \<in> (vs_lookup1 s)\<^sup>*; \<exists>rs r pa p' ko. (a, b) = (rs, pa) \<and> ([VSRef (UCAST(7 \<rightarrow> 32) asid) None], p) = (r # rs, p') \<and> ko_at ko pa s \<and> (r, p') \<in> vs_refs ko\<rbrakk> \<Longrightarrow> asid_table s asid = Some p proof (prove)
goal (1 subgoal):
 1. \<And>aa ba b ko. \<lbrakk>asid_table s aa = Some ba; aa = asid \<longrightarrow> ba \<noteq> p; (([VSRef (UCAST(7 \<rightarrow> 32) aa) None], ba), [], b) \<in> (vs_lookup1 s)\<^sup>*; ko_at ko b s; (VSRef (UCAST(7 \<rightarrow> 32) asid) None, p) \<in> (case ko of ArchObj (ASIDPool pool) \<Rightarrow> (\<lambda>(r, y). (VSRef (UCAST(10 \<rightarrow> 32) r) (Some AASIDPool), y)) ` graph_of pool | ArchObj (PageDirectory pd) \<Rightarrow> (\<lambda>(r, y). (VSRef (UCAST(12 \<rightarrow> 32) r) (Some APageDirectory), y)) ` graph_of (\<lambda>x. if x \<in> kernel_mapping_slots then None else pde_ref (pd x)) | ArchObj _ \<Rightarrow> {} | _ \<Rightarrow> {})\<rbrakk> \<Longrightarrow> asid_table s asid = Some p proof (prove)
goal:
No subgoals!