theory ArchArch_AI

lemma valid_vs_lookup_at_upd_strg:
  "valid_vs_lookup s \<and>
   ko_at (ArchObj (ASIDPool Map.empty)) ap s \<and>
   asid_table s asid = None \<and>
   (\<exists>ptr cap. caps_of_state s ptr = Some cap \<and> ap \<in> obj_refs cap \<and>
              vs_cap_ref cap = Some [VSRef (ucast asid) None])
   \<longrightarrow>
   valid_vs_lookup (s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := (asid_table s)(asid \<mapsto> ap)\<rparr>\<rparr>)" apply clarsimp apply (subgoal_tac "asid_update ap asid s") prefer 2 apply unfold_locales[1] apply assumption+ apply (erule (1) asid_update.valid_vs_lookup') apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_vs_lookup s \<and> ako_at (ASIDPool (\<lambda>x. None)) ap s \<and> asid_table s asid = None \<and> (\<exists>ptr cap. caps_of_state s ptr = Some cap \<and> ap \<in> obj_refs cap \<and> vs_cap_ref cap = Some [VSRef (UCAST(7 \<rightarrow> 32) asid) None]) \<longrightarrow> valid_vs_lookup (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 b cap. \<lbrakk>valid_vs_lookup s; ako_at (ASIDPool (\<lambda>x. None)) ap s; asid_table s asid = None; caps_of_state s (a, b) = Some cap; ap \<in> obj_refs cap; vs_cap_ref cap = Some [VSRef (UCAST(7 \<rightarrow> 32) asid) None]\<rbrakk> \<Longrightarrow> valid_vs_lookup (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 b cap. \<lbrakk>valid_vs_lookup s; ako_at (ASIDPool (\<lambda>x. None)) ap s; asid_table s asid = None; caps_of_state s (a, b) = Some cap; ap \<in> obj_refs cap; vs_cap_ref cap = Some [VSRef (UCAST(7 \<rightarrow> 32) asid) None]; asid_update ap asid s\<rbrakk> \<Longrightarrow> valid_vs_lookup (s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := (asid_table s)(asid \<mapsto> ap)\<rparr>\<rparr>)
 2. \<And>a b cap. \<lbrakk>valid_vs_lookup s; ako_at (ASIDPool (\<lambda>x. None)) ap s; asid_table s asid = None; caps_of_state s (a, b) = Some cap; ap \<in> obj_refs cap; vs_cap_ref cap = Some [VSRef (UCAST(7 \<rightarrow> 32) asid) None]\<rbrakk> \<Longrightarrow> asid_update ap asid s proof (prove)
goal (2 subgoals):
 1. \<And>a b cap. \<lbrakk>valid_vs_lookup s; ako_at (ASIDPool (\<lambda>x. None)) ap s; asid_table s asid = None; caps_of_state s (a, b) = Some cap; ap \<in> obj_refs cap; vs_cap_ref cap = Some [VSRef (UCAST(7 \<rightarrow> 32) asid) None]\<rbrakk> \<Longrightarrow> asid_update ap asid s
 2. \<And>a b cap. \<lbrakk>valid_vs_lookup s; ako_at (ASIDPool (\<lambda>x. None)) ap s; asid_table s asid = None; caps_of_state s (a, b) = Some cap; ap \<in> obj_refs cap; vs_cap_ref cap = Some [VSRef (UCAST(7 \<rightarrow> 32) asid) None]; asid_update ap asid s\<rbrakk> \<Longrightarrow> valid_vs_lookup (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 b cap. \<lbrakk>valid_vs_lookup s; ako_at (ASIDPool (\<lambda>x. None)) ap s; asid_table s asid = None; caps_of_state s (a, b) = Some cap; ap \<in> obj_refs cap; vs_cap_ref cap = Some [VSRef (UCAST(7 \<rightarrow> 32) asid) None]\<rbrakk> \<Longrightarrow> ako_at (ASIDPool (\<lambda>x. None)) ap s
 2. \<And>a b cap. \<lbrakk>valid_vs_lookup s; ako_at (ASIDPool (\<lambda>x. None)) ap s; asid_table s asid = None; caps_of_state s (a, b) = Some cap; ap \<in> obj_refs cap; vs_cap_ref cap = Some [VSRef (UCAST(7 \<rightarrow> 32) asid) None]\<rbrakk> \<Longrightarrow> asid_table s asid = None
 3. \<And>a b cap. \<lbrakk>valid_vs_lookup s; ako_at (ASIDPool (\<lambda>x. None)) ap s; asid_table s asid = None; caps_of_state s (a, b) = Some cap; ap \<in> obj_refs cap; vs_cap_ref cap = Some [VSRef (UCAST(7 \<rightarrow> 32) asid) None]; asid_update ap asid s\<rbrakk> \<Longrightarrow> valid_vs_lookup (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 b cap. \<lbrakk>valid_vs_lookup s; ako_at (ASIDPool (\<lambda>x. None)) ap s; asid_table s asid = None; caps_of_state s (a, b) = Some cap; ap \<in> obj_refs cap; vs_cap_ref cap = Some [VSRef (UCAST(7 \<rightarrow> 32) asid) None]; asid_update ap asid s\<rbrakk> \<Longrightarrow> valid_vs_lookup (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 b cap. \<lbrakk>valid_vs_lookup s; ako_at (ASIDPool (\<lambda>x. None)) ap s; asid_table s asid = None; caps_of_state s (a, b) = Some cap; ap \<in> obj_refs cap; vs_cap_ref cap = Some [VSRef (UCAST(7 \<rightarrow> 32) asid) None]\<rbrakk> \<Longrightarrow> \<exists>ptr cap. caps_of_state s ptr = Some cap \<and> ap \<in> obj_refs cap \<and> vs_cap_ref cap = Some [VSRef (UCAST(7 \<rightarrow> 32) asid) None] proof (prove)
goal:
No subgoals!