theory ArchCSpaceInvPre_AI

lemma set_cap_valid_vs_lookup:
  "\<lbrace>\<lambda>s. valid_vs_lookup s
      \<and> (\<forall>vref cap'. cte_wp_at ((=) cap') ptr s
                \<longrightarrow> vs_cap_ref cap' = Some vref
                \<longrightarrow> (vs_cap_ref cap = Some vref \<and> obj_refs cap = obj_refs cap')
                 \<or> (\<not> is_final_cap' cap' s \<and> \<not> reachable_pg_cap cap' s)
                 \<or> (\<forall>oref. oref \<in> obj_refs cap' \<longrightarrow> \<not> (vref \<unrhd> oref) s))
      \<and> unique_table_refs (caps_of_state s)\<rbrace>
     set_cap cap ptr
   \<lbrace>\<lambda>rv. valid_vs_lookup\<rbrace>" apply (simp add: valid_vs_lookup_def
              del: split_paired_All split_paired_Ex) apply (rule hoare_pre) apply (wp hoare_vcg_all_lift hoare_convert_imp[OF set_cap.vs_lookup_pages]
             hoare_vcg_disj_lift) apply (elim conjE allEI, rule impI, drule(1) mp) apply (simp only: simp_thms) apply (elim exE conjE) apply (case_tac "p' = ptr") apply (clarsimp simp: cte_wp_at_caps_of_state) apply (elim disjE impCE) apply fastforce apply clarsimp apply (drule (1) not_final_another_caps) apply (erule obj_ref_is_gen_obj_ref) apply (simp, elim exEI, clarsimp simp: gen_obj_refs_eq) apply (rule conjI, clarsimp) apply (drule(3) unique_table_refsD) apply (clarsimp simp: reachable_pg_cap_def is_pg_cap_def) apply (case_tac cap, simp_all add: vs_cap_ref_simps)[1] apply (rename_tac arch_cap) apply (case_tac arch_cap,
           simp_all add: vs_cap_ref_simps table_cap_ref_simps)[1] apply (clarsimp dest!: table_cap_ref_vs_cap_ref_Some) apply fastforce apply (clarsimp dest!: table_cap_ref_vs_cap_ref_Some)+ apply (auto simp: cte_wp_at_caps_of_state)[1] done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. valid_vs_lookup s \<and> (\<forall>vref cap'. cte_wp_at ((=) cap') ptr s \<longrightarrow> vs_cap_ref cap' = Some vref \<longrightarrow> vs_cap_ref cap = Some vref \<and> obj_refs cap = obj_refs cap' \<or> \<not> is_final_cap' cap' s \<and> \<not> reachable_pg_cap cap' s \<or> (\<forall>oref. oref \<in> obj_refs cap' \<longrightarrow> (vref, oref) \<notin> vs_lookup_pages s)) \<and> unique_table_refs (caps_of_state s)\<rbrace> set_cap cap ptr \<lbrace>\<lambda>rv. valid_vs_lookup\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. (\<forall>p ref. (ref \<unrhd> p) s \<longrightarrow> ref \<noteq> [VSRef 0 (Some AASIDPool), VSRef 0 None] \<and> (\<exists>p' cap. caps_of_state s p' = Some cap \<and> p \<in> obj_refs cap \<and> vs_cap_ref cap = Some ref)) \<and> (\<forall>vref cap'. cte_wp_at ((=) cap') ptr s \<longrightarrow> vs_cap_ref cap' = Some vref \<longrightarrow> vs_cap_ref cap = Some vref \<and> obj_refs cap = obj_refs cap' \<or> \<not> is_final_cap' cap' s \<and> \<not> reachable_pg_cap cap' s \<or> (\<forall>oref. oref \<in> obj_refs cap' \<longrightarrow> (vref, oref) \<notin> vs_lookup_pages s)) \<and> unique_table_refs (caps_of_state s)\<rbrace> set_cap cap ptr \<lbrace>\<lambda>rv s. \<forall>p ref. (ref \<unrhd> p) s \<longrightarrow> ref \<noteq> [VSRef 0 (Some AASIDPool), VSRef 0 None] \<and> (\<exists>p' cap. caps_of_state s p' = Some cap \<and> p \<in> obj_refs cap \<and> vs_cap_ref cap = Some ref)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> set_cap cap ptr \<lbrace>\<lambda>rv s. \<forall>p ref. (ref \<unrhd> p) s \<longrightarrow> ref \<noteq> [VSRef 0 (Some AASIDPool), VSRef 0 None] \<and> (\<exists>p' cap. caps_of_state s p' = Some cap \<and> p \<in> obj_refs cap \<and> vs_cap_ref cap = Some ref)\<rbrace>
 2. \<And>s. (\<forall>p ref. (ref \<unrhd> p) s \<longrightarrow> ref \<noteq> [VSRef 0 (Some AASIDPool), VSRef 0 None] \<and> (\<exists>p' cap. caps_of_state s p' = Some cap \<and> p \<in> obj_refs cap \<and> vs_cap_ref cap = Some ref)) \<and> (\<forall>vref cap'. cte_wp_at ((=) cap') ptr s \<longrightarrow> vs_cap_ref cap' = Some vref \<longrightarrow> vs_cap_ref cap = Some vref \<and> obj_refs cap = obj_refs cap' \<or> \<not> is_final_cap' cap' s \<and> \<not> reachable_pg_cap cap' s \<or> (\<forall>oref. oref \<in> obj_refs cap' \<longrightarrow> (vref, oref) \<notin> vs_lookup_pages s)) \<and> unique_table_refs (caps_of_state s) \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. (\<forall>p ref. (ref \<unrhd> p) s \<longrightarrow> ref \<noteq> [VSRef 0 (Some AASIDPool), VSRef 0 None] \<and> (\<exists>p' cap. caps_of_state s p' = Some cap \<and> p \<in> obj_refs cap \<and> vs_cap_ref cap = Some ref)) \<and> (\<forall>vref cap'. cte_wp_at ((=) cap') ptr s \<longrightarrow> vs_cap_ref cap' = Some vref \<longrightarrow> vs_cap_ref cap = Some vref \<and> obj_refs cap = obj_refs cap' \<or> \<not> is_final_cap' cap' s \<and> \<not> reachable_pg_cap cap' s \<or> (\<forall>oref. oref \<in> obj_refs cap' \<longrightarrow> (vref, oref) \<notin> vs_lookup_pages s)) \<and> unique_table_refs (caps_of_state s) \<Longrightarrow> \<forall>x xa. (xa \<unrhd> x) s \<longrightarrow> xa \<noteq> [VSRef 0 (Some AASIDPool), VSRef 0 None] \<and> (\<exists>p' capa. ((caps_of_state s)(ptr \<mapsto> cap)) p' = Some capa \<and> x \<in> obj_refs capa \<and> vs_cap_ref capa = Some xa) proof (prove)
goal (1 subgoal):
 1. \<And>s x xa. \<lbrakk>\<forall>vref cap'. cte_wp_at ((=) cap') ptr s \<longrightarrow> vs_cap_ref cap' = Some vref \<longrightarrow> vs_cap_ref cap = Some vref \<and> obj_refs cap = obj_refs cap' \<or> \<not> is_final_cap' cap' s \<and> \<not> reachable_pg_cap cap' s \<or> (\<forall>oref. oref \<in> obj_refs cap' \<longrightarrow> (vref, oref) \<notin> vs_lookup_pages s); unique_table_refs (caps_of_state s); (xa \<unrhd> x) s; xa \<noteq> [VSRef 0 (Some AASIDPool), VSRef 0 None] \<and> (\<exists>p' cap. caps_of_state s p' = Some cap \<and> x \<in> obj_refs cap \<and> vs_cap_ref cap = Some xa)\<rbrakk> \<Longrightarrow> xa \<noteq> [VSRef 0 (Some AASIDPool), VSRef 0 None] \<and> (\<exists>p' capa. ((caps_of_state s)(ptr \<mapsto> cap)) p' = Some capa \<and> x \<in> obj_refs capa \<and> vs_cap_ref capa = Some xa) proof (prove)
goal (1 subgoal):
 1. \<And>s x xa. \<lbrakk>\<forall>vref cap'. cte_wp_at ((=) cap') ptr s \<longrightarrow> vs_cap_ref cap' = Some vref \<longrightarrow> vs_cap_ref cap = Some vref \<and> obj_refs cap = obj_refs cap' \<or> \<not> is_final_cap' cap' s \<and> \<not> reachable_pg_cap cap' s \<or> (\<forall>oref. oref \<in> obj_refs cap' \<longrightarrow> (vref, oref) \<notin> vs_lookup_pages s); unique_table_refs (caps_of_state s); (xa \<unrhd> x) s; xa \<noteq> [VSRef 0 (Some AASIDPool), VSRef 0 None] \<and> (\<exists>p' cap. caps_of_state s p' = Some cap \<and> x \<in> obj_refs cap \<and> vs_cap_ref cap = Some xa)\<rbrakk> \<Longrightarrow> \<exists>p' capa. ((caps_of_state s)(ptr \<mapsto> cap)) p' = Some capa \<and> x \<in> obj_refs capa \<and> vs_cap_ref capa = Some xa proof (prove)
goal (1 subgoal):
 1. \<And>s x xa p' capa. \<lbrakk>\<forall>vref cap'. cte_wp_at ((=) cap') ptr s \<longrightarrow> vs_cap_ref cap' = Some vref \<longrightarrow> vs_cap_ref cap = Some vref \<and> obj_refs cap = obj_refs cap' \<or> \<not> is_final_cap' cap' s \<and> \<not> reachable_pg_cap cap' s \<or> (\<forall>oref. oref \<in> obj_refs cap' \<longrightarrow> (vref, oref) \<notin> vs_lookup_pages s); unique_table_refs (caps_of_state s); (xa \<unrhd> x) s; xa \<noteq> [VSRef 0 (Some AASIDPool), VSRef 0 None]; caps_of_state s p' = Some capa; x \<in> obj_refs capa; vs_cap_ref capa = Some xa\<rbrakk> \<Longrightarrow> \<exists>p' capa. ((caps_of_state s)(ptr \<mapsto> cap)) p' = Some capa \<and> x \<in> obj_refs capa \<and> vs_cap_ref capa = Some xa proof (prove)
goal (2 subgoals):
 1. \<And>s x xa p' capa. \<lbrakk>\<forall>vref cap'. cte_wp_at ((=) cap') ptr s \<longrightarrow> vs_cap_ref cap' = Some vref \<longrightarrow> vs_cap_ref cap = Some vref \<and> obj_refs cap = obj_refs cap' \<or> \<not> is_final_cap' cap' s \<and> \<not> reachable_pg_cap cap' s \<or> (\<forall>oref. oref \<in> obj_refs cap' \<longrightarrow> (vref, oref) \<notin> vs_lookup_pages s); unique_table_refs (caps_of_state s); (xa \<unrhd> x) s; xa \<noteq> [VSRef 0 (Some AASIDPool), VSRef 0 None]; caps_of_state s p' = Some capa; x \<in> obj_refs capa; vs_cap_ref capa = Some xa; p' = ptr\<rbrakk> \<Longrightarrow> \<exists>p' capa. ((caps_of_state s)(ptr \<mapsto> cap)) p' = Some capa \<and> x \<in> obj_refs capa \<and> vs_cap_ref capa = Some xa
 2. \<And>s x xa p' capa. \<lbrakk>\<forall>vref cap'. cte_wp_at ((=) cap') ptr s \<longrightarrow> vs_cap_ref cap' = Some vref \<longrightarrow> vs_cap_ref cap = Some vref \<and> obj_refs cap = obj_refs cap' \<or> \<not> is_final_cap' cap' s \<and> \<not> reachable_pg_cap cap' s \<or> (\<forall>oref. oref \<in> obj_refs cap' \<longrightarrow> (vref, oref) \<notin> vs_lookup_pages s); unique_table_refs (caps_of_state s); (xa \<unrhd> x) s; xa \<noteq> [VSRef 0 (Some AASIDPool), VSRef 0 None]; caps_of_state s p' = Some capa; x \<in> obj_refs capa; vs_cap_ref capa = Some xa; p' \<noteq> ptr\<rbrakk> \<Longrightarrow> \<exists>p' capa. ((caps_of_state s)(ptr \<mapsto> cap)) p' = Some capa \<and> x \<in> obj_refs capa \<and> vs_cap_ref capa = Some xa proof (prove)
goal (2 subgoals):
 1. \<And>s x xa a b capa. \<lbrakk>vs_cap_ref cap = Some xa \<and> obj_refs cap = obj_refs capa \<or> \<not> is_final_cap' capa s \<and> \<not> reachable_pg_cap capa s \<or> (\<forall>oref. oref \<in> obj_refs capa \<longrightarrow> (xa, oref) \<notin> vs_lookup_pages s); unique_table_refs (caps_of_state s); (xa \<unrhd> x) s; xa \<noteq> [VSRef 0 (Some AASIDPool), VSRef 0 None]; caps_of_state s (a, b) = Some capa; x \<in> obj_refs capa; vs_cap_ref capa = Some xa; ptr = (a, b)\<rbrakk> \<Longrightarrow> \<exists>aa ba. (aa = a \<and> ba = b \<longrightarrow> x \<in> obj_refs cap \<and> vs_cap_ref cap = Some xa) \<and> ((aa = a \<longrightarrow> ba \<noteq> b) \<longrightarrow> (\<exists>cap. caps_of_state s (aa, ba) = Some cap \<and> x \<in> obj_refs cap \<and> vs_cap_ref cap = Some xa))
 2. \<And>s x xa p' capa. \<lbrakk>\<forall>vref cap'. cte_wp_at ((=) cap') ptr s \<longrightarrow> vs_cap_ref cap' = Some vref \<longrightarrow> vs_cap_ref cap = Some vref \<and> obj_refs cap = obj_refs cap' \<or> \<not> is_final_cap' cap' s \<and> \<not> reachable_pg_cap cap' s \<or> (\<forall>oref. oref \<in> obj_refs cap' \<longrightarrow> (vref, oref) \<notin> vs_lookup_pages s); unique_table_refs (caps_of_state s); (xa \<unrhd> x) s; xa \<noteq> [VSRef 0 (Some AASIDPool), VSRef 0 None]; caps_of_state s p' = Some capa; x \<in> obj_refs capa; vs_cap_ref capa = Some xa; p' \<noteq> ptr\<rbrakk> \<Longrightarrow> \<exists>p' capa. ((caps_of_state s)(ptr \<mapsto> cap)) p' = Some capa \<and> x \<in> obj_refs capa \<and> vs_cap_ref capa = Some xa proof (prove)
goal (4 subgoals):
 1. \<And>s x xa a b capa. \<lbrakk>unique_table_refs (caps_of_state s); (xa \<unrhd> x) s; xa \<noteq> [VSRef 0 (Some AASIDPool), VSRef 0 None]; caps_of_state s (a, b) = Some capa; x \<in> obj_refs capa; vs_cap_ref capa = Some xa; ptr = (a, b); vs_cap_ref cap = Some xa \<and> obj_refs cap = obj_refs capa\<rbrakk> \<Longrightarrow> \<exists>aa ba. (aa = a \<and> ba = b \<longrightarrow> x \<in> obj_refs cap \<and> vs_cap_ref cap = Some xa) \<and> ((aa = a \<longrightarrow> ba \<noteq> b) \<longrightarrow> (\<exists>cap. caps_of_state s (aa, ba) = Some cap \<and> x \<in> obj_refs cap \<and> vs_cap_ref cap = Some xa))
 2. \<And>s x xa a b capa. \<lbrakk>unique_table_refs (caps_of_state s); (xa \<unrhd> x) s; xa \<noteq> [VSRef 0 (Some AASIDPool), VSRef 0 None]; caps_of_state s (a, b) = Some capa; x \<in> obj_refs capa; vs_cap_ref capa = Some xa; ptr = (a, b); \<not> is_final_cap' capa s \<and> \<not> reachable_pg_cap capa s\<rbrakk> \<Longrightarrow> \<exists>aa ba. (aa = a \<and> ba = b \<longrightarrow> x \<in> obj_refs cap \<and> vs_cap_ref cap = Some xa) \<and> ((aa = a \<longrightarrow> ba \<noteq> b) \<longrightarrow> (\<exists>cap. caps_of_state s (aa, ba) = Some cap \<and> x \<in> obj_refs cap \<and> vs_cap_ref cap = Some xa))
 3. \<And>s x xa a b capa. \<lbrakk>unique_table_refs (caps_of_state s); (xa \<unrhd> x) s; xa \<noteq> [VSRef 0 (Some AASIDPool), VSRef 0 None]; caps_of_state s (a, b) = Some capa; x \<in> obj_refs capa; vs_cap_ref capa = Some xa; ptr = (a, b); \<forall>oref. oref \<in> obj_refs capa \<longrightarrow> (xa, oref) \<notin> vs_lookup_pages s\<rbrakk> \<Longrightarrow> \<exists>aa ba. (aa = a \<and> ba = b \<longrightarrow> x \<in> obj_refs cap \<and> vs_cap_ref cap = Some xa) \<and> ((aa = a \<longrightarrow> ba \<noteq> b) \<longrightarrow> (\<exists>cap. caps_of_state s (aa, ba) = Some cap \<and> x \<in> obj_refs cap \<and> vs_cap_ref cap = Some xa))
 4. \<And>s x xa p' capa. \<lbrakk>\<forall>vref cap'. cte_wp_at ((=) cap') ptr s \<longrightarrow> vs_cap_ref cap' = Some vref \<longrightarrow> vs_cap_ref cap = Some vref \<and> obj_refs cap = obj_refs cap' \<or> \<not> is_final_cap' cap' s \<and> \<not> reachable_pg_cap cap' s \<or> (\<forall>oref. oref \<in> obj_refs cap' \<longrightarrow> (vref, oref) \<notin> vs_lookup_pages s); unique_table_refs (caps_of_state s); (xa \<unrhd> x) s; xa \<noteq> [VSRef 0 (Some AASIDPool), VSRef 0 None]; caps_of_state s p' = Some capa; x \<in> obj_refs capa; vs_cap_ref capa = Some xa; p' \<noteq> ptr\<rbrakk> \<Longrightarrow> \<exists>p' capa. ((caps_of_state s)(ptr \<mapsto> cap)) p' = Some capa \<and> x \<in> obj_refs capa \<and> vs_cap_ref capa = Some xa proof (prove)
goal (3 subgoals):
 1. \<And>s x xa a b capa. \<lbrakk>unique_table_refs (caps_of_state s); (xa \<unrhd> x) s; xa \<noteq> [VSRef 0 (Some AASIDPool), VSRef 0 None]; caps_of_state s (a, b) = Some capa; x \<in> obj_refs capa; vs_cap_ref capa = Some xa; ptr = (a, b); \<not> is_final_cap' capa s \<and> \<not> reachable_pg_cap capa s\<rbrakk> \<Longrightarrow> \<exists>aa ba. (aa = a \<and> ba = b \<longrightarrow> x \<in> obj_refs cap \<and> vs_cap_ref cap = Some xa) \<and> ((aa = a \<longrightarrow> ba \<noteq> b) \<longrightarrow> (\<exists>cap. caps_of_state s (aa, ba) = Some cap \<and> x \<in> obj_refs cap \<and> vs_cap_ref cap = Some xa))
 2. \<And>s x xa a b capa. \<lbrakk>unique_table_refs (caps_of_state s); (xa \<unrhd> x) s; xa \<noteq> [VSRef 0 (Some AASIDPool), VSRef 0 None]; caps_of_state s (a, b) = Some capa; x \<in> obj_refs capa; vs_cap_ref capa = Some xa; ptr = (a, b); \<forall>oref. oref \<in> obj_refs capa \<longrightarrow> (xa, oref) \<notin> vs_lookup_pages s\<rbrakk> \<Longrightarrow> \<exists>aa ba. (aa = a \<and> ba = b \<longrightarrow> x \<in> obj_refs cap \<and> vs_cap_ref cap = Some xa) \<and> ((aa = a \<longrightarrow> ba \<noteq> b) \<longrightarrow> (\<exists>cap. caps_of_state s (aa, ba) = Some cap \<and> x \<in> obj_refs cap \<and> vs_cap_ref cap = Some xa))
 3. \<And>s x xa p' capa. \<lbrakk>\<forall>vref cap'. cte_wp_at ((=) cap') ptr s \<longrightarrow> vs_cap_ref cap' = Some vref \<longrightarrow> vs_cap_ref cap = Some vref \<and> obj_refs cap = obj_refs cap' \<or> \<not> is_final_cap' cap' s \<and> \<not> reachable_pg_cap cap' s \<or> (\<forall>oref. oref \<in> obj_refs cap' \<longrightarrow> (vref, oref) \<notin> vs_lookup_pages s); unique_table_refs (caps_of_state s); (xa \<unrhd> x) s; xa \<noteq> [VSRef 0 (Some AASIDPool), VSRef 0 None]; caps_of_state s p' = Some capa; x \<in> obj_refs capa; vs_cap_ref capa = Some xa; p' \<noteq> ptr\<rbrakk> \<Longrightarrow> \<exists>p' capa. ((caps_of_state s)(ptr \<mapsto> cap)) p' = Some capa \<and> x \<in> obj_refs capa \<and> vs_cap_ref capa = Some xa proof (prove)
goal (3 subgoals):
 1. \<And>s x xa a b capa. \<lbrakk>unique_table_refs (caps_of_state s); (xa \<unrhd> x) s; xa \<noteq> [VSRef 0 (Some AASIDPool), VSRef 0 None]; caps_of_state s (a, b) = Some capa; x \<in> obj_refs capa; vs_cap_ref capa = Some xa; ptr = (a, b); \<not> is_final_cap' capa s; \<not> reachable_pg_cap capa s\<rbrakk> \<Longrightarrow> \<exists>aa ba. (aa = a \<and> ba = b \<longrightarrow> x \<in> obj_refs cap \<and> vs_cap_ref cap = Some xa) \<and> ((aa = a \<longrightarrow> ba \<noteq> b) \<longrightarrow> (\<exists>cap. caps_of_state s (aa, ba) = Some cap \<and> x \<in> obj_refs cap \<and> vs_cap_ref cap = Some xa))
 2. \<And>s x xa a b capa. \<lbrakk>unique_table_refs (caps_of_state s); (xa \<unrhd> x) s; xa \<noteq> [VSRef 0 (Some AASIDPool), VSRef 0 None]; caps_of_state s (a, b) = Some capa; x \<in> obj_refs capa; vs_cap_ref capa = Some xa; ptr = (a, b); \<forall>oref. oref \<in> obj_refs capa \<longrightarrow> (xa, oref) \<notin> vs_lookup_pages s\<rbrakk> \<Longrightarrow> \<exists>aa ba. (aa = a \<and> ba = b \<longrightarrow> x \<in> obj_refs cap \<and> vs_cap_ref cap = Some xa) \<and> ((aa = a \<longrightarrow> ba \<noteq> b) \<longrightarrow> (\<exists>cap. caps_of_state s (aa, ba) = Some cap \<and> x \<in> obj_refs cap \<and> vs_cap_ref cap = Some xa))
 3. \<And>s x xa p' capa. \<lbrakk>\<forall>vref cap'. cte_wp_at ((=) cap') ptr s \<longrightarrow> vs_cap_ref cap' = Some vref \<longrightarrow> vs_cap_ref cap = Some vref \<and> obj_refs cap = obj_refs cap' \<or> \<not> is_final_cap' cap' s \<and> \<not> reachable_pg_cap cap' s \<or> (\<forall>oref. oref \<in> obj_refs cap' \<longrightarrow> (vref, oref) \<notin> vs_lookup_pages s); unique_table_refs (caps_of_state s); (xa \<unrhd> x) s; xa \<noteq> [VSRef 0 (Some AASIDPool), VSRef 0 None]; caps_of_state s p' = Some capa; x \<in> obj_refs capa; vs_cap_ref capa = Some xa; p' \<noteq> ptr\<rbrakk> \<Longrightarrow> \<exists>p' capa. ((caps_of_state s)(ptr \<mapsto> cap)) p' = Some capa \<and> x \<in> obj_refs capa \<and> vs_cap_ref capa = Some xa proof (prove)
goal (4 subgoals):
 1. \<And>s x xa a b cap. \<lbrakk>unique_table_refs (caps_of_state s); (xa \<unrhd> x) s; xa \<noteq> [VSRef 0 (Some AASIDPool), VSRef 0 None]; caps_of_state s (a, b) = Some cap; x \<in> obj_refs cap; vs_cap_ref cap = Some xa; ptr = (a, b); \<not> reachable_pg_cap cap s\<rbrakk> \<Longrightarrow> ?r58 s x xa a b cap \<in> gen_obj_refs cap
 2. \<And>s x xa a b capa. \<lbrakk>unique_table_refs (caps_of_state s); (xa \<unrhd> x) s; xa \<noteq> [VSRef 0 (Some AASIDPool), VSRef 0 None]; caps_of_state s (a, b) = Some capa; x \<in> obj_refs capa; vs_cap_ref capa = Some xa; ptr = (a, b); \<not> reachable_pg_cap capa s; \<exists>p' cap'. p' \<noteq> (a, b) \<and> caps_of_state s p' = Some cap' \<and> gen_obj_refs cap' = gen_obj_refs capa \<and> \<not> is_final_cap' cap' s\<rbrakk> \<Longrightarrow> \<exists>aa ba. (aa = a \<and> ba = b \<longrightarrow> x \<in> obj_refs cap \<and> vs_cap_ref cap = Some xa) \<and> ((aa = a \<longrightarrow> ba \<noteq> b) \<longrightarrow> (\<exists>cap. caps_of_state s (aa, ba) = Some cap \<and> x \<in> obj_refs cap \<and> vs_cap_ref cap = Some xa))
 3. \<And>s x xa a b capa. \<lbrakk>unique_table_refs (caps_of_state s); (xa \<unrhd> x) s; xa \<noteq> [VSRef 0 (Some AASIDPool), VSRef 0 None]; caps_of_state s (a, b) = Some capa; x \<in> obj_refs capa; vs_cap_ref capa = Some xa; ptr = (a, b); \<forall>oref. oref \<in> obj_refs capa \<longrightarrow> (xa, oref) \<notin> vs_lookup_pages s\<rbrakk> \<Longrightarrow> \<exists>aa ba. (aa = a \<and> ba = b \<longrightarrow> x \<in> obj_refs cap \<and> vs_cap_ref cap = Some xa) \<and> ((aa = a \<longrightarrow> ba \<noteq> b) \<longrightarrow> (\<exists>cap. caps_of_state s (aa, ba) = Some cap \<and> x \<in> obj_refs cap \<and> vs_cap_ref cap = Some xa))
 4. \<And>s x xa p' capa. \<lbrakk>\<forall>vref cap'. cte_wp_at ((=) cap') ptr s \<longrightarrow> vs_cap_ref cap' = Some vref \<longrightarrow> vs_cap_ref cap = Some vref \<and> obj_refs cap = obj_refs cap' \<or> \<not> is_final_cap' cap' s \<and> \<not> reachable_pg_cap cap' s \<or> (\<forall>oref. oref \<in> obj_refs cap' \<longrightarrow> (vref, oref) \<notin> vs_lookup_pages s); unique_table_refs (caps_of_state s); (xa \<unrhd> x) s; xa \<noteq> [VSRef 0 (Some AASIDPool), VSRef 0 None]; caps_of_state s p' = Some capa; x \<in> obj_refs capa; vs_cap_ref capa = Some xa; p' \<noteq> ptr\<rbrakk> \<Longrightarrow> \<exists>p' capa. ((caps_of_state s)(ptr \<mapsto> cap)) p' = Some capa \<and> x \<in> obj_refs capa \<and> vs_cap_ref capa = Some xa proof (prove)
goal (3 subgoals):
 1. \<And>s x xa a b capa. \<lbrakk>unique_table_refs (caps_of_state s); (xa \<unrhd> x) s; xa \<noteq> [VSRef 0 (Some AASIDPool), VSRef 0 None]; caps_of_state s (a, b) = Some capa; x \<in> obj_refs capa; vs_cap_ref capa = Some xa; ptr = (a, b); \<not> reachable_pg_cap capa s; \<exists>p' cap'. p' \<noteq> (a, b) \<and> caps_of_state s p' = Some cap' \<and> gen_obj_refs cap' = gen_obj_refs capa \<and> \<not> is_final_cap' cap' s\<rbrakk> \<Longrightarrow> \<exists>aa ba. (aa = a \<and> ba = b \<longrightarrow> x \<in> obj_refs cap \<and> vs_cap_ref cap = Some xa) \<and> ((aa = a \<longrightarrow> ba \<noteq> b) \<longrightarrow> (\<exists>cap. caps_of_state s (aa, ba) = Some cap \<and> x \<in> obj_refs cap \<and> vs_cap_ref cap = Some xa))
 2. \<And>s x xa a b capa. \<lbrakk>unique_table_refs (caps_of_state s); (xa \<unrhd> x) s; xa \<noteq> [VSRef 0 (Some AASIDPool), VSRef 0 None]; caps_of_state s (a, b) = Some capa; x \<in> obj_refs capa; vs_cap_ref capa = Some xa; ptr = (a, b); \<forall>oref. oref \<in> obj_refs capa \<longrightarrow> (xa, oref) \<notin> vs_lookup_pages s\<rbrakk> \<Longrightarrow> \<exists>aa ba. (aa = a \<and> ba = b \<longrightarrow> x \<in> obj_refs cap \<and> vs_cap_ref cap = Some xa) \<and> ((aa = a \<longrightarrow> ba \<noteq> b) \<longrightarrow> (\<exists>cap. caps_of_state s (aa, ba) = Some cap \<and> x \<in> obj_refs cap \<and> vs_cap_ref cap = Some xa))
 3. \<And>s x xa p' capa. \<lbrakk>\<forall>vref cap'. cte_wp_at ((=) cap') ptr s \<longrightarrow> vs_cap_ref cap' = Some vref \<longrightarrow> vs_cap_ref cap = Some vref \<and> obj_refs cap = obj_refs cap' \<or> \<not> is_final_cap' cap' s \<and> \<not> reachable_pg_cap cap' s \<or> (\<forall>oref. oref \<in> obj_refs cap' \<longrightarrow> (vref, oref) \<notin> vs_lookup_pages s); unique_table_refs (caps_of_state s); (xa \<unrhd> x) s; xa \<noteq> [VSRef 0 (Some AASIDPool), VSRef 0 None]; caps_of_state s p' = Some capa; x \<in> obj_refs capa; vs_cap_ref capa = Some xa; p' \<noteq> ptr\<rbrakk> \<Longrightarrow> \<exists>p' capa. ((caps_of_state s)(ptr \<mapsto> cap)) p' = Some capa \<and> x \<in> obj_refs capa \<and> vs_cap_ref capa = Some xa proof (prove)
goal (3 subgoals):
 1. \<And>s x xa a b capa xb xc cap'. \<lbrakk>unique_table_refs (caps_of_state s); (xa \<unrhd> x) s; xa \<noteq> [VSRef 0 (Some AASIDPool), VSRef 0 None]; caps_of_state s (a, b) = Some capa; x \<in> obj_refs capa; vs_cap_ref capa = Some xa; ptr = (a, b); \<not> reachable_pg_cap capa s; xb = a \<longrightarrow> xc \<noteq> b; caps_of_state s (xb, xc) = Some cap'; obj_refs cap' = obj_refs capa; cap_irqs cap' = cap_irqs capa; arch_gen_refs cap' = arch_gen_refs capa; \<not> is_final_cap' cap' s\<rbrakk> \<Longrightarrow> (xb = a \<and> xc = b \<longrightarrow> x \<in> obj_refs cap \<and> vs_cap_ref cap = Some xa) \<and> vs_cap_ref cap' = Some xa
 2. \<And>s x xa a b capa. \<lbrakk>unique_table_refs (caps_of_state s); (xa \<unrhd> x) s; xa \<noteq> [VSRef 0 (Some AASIDPool), VSRef 0 None]; caps_of_state s (a, b) = Some capa; x \<in> obj_refs capa; vs_cap_ref capa = Some xa; ptr = (a, b); \<forall>oref. oref \<in> obj_refs capa \<longrightarrow> (xa, oref) \<notin> vs_lookup_pages s\<rbrakk> \<Longrightarrow> \<exists>aa ba. (aa = a \<and> ba = b \<longrightarrow> x \<in> obj_refs cap \<and> vs_cap_ref cap = Some xa) \<and> ((aa = a \<longrightarrow> ba \<noteq> b) \<longrightarrow> (\<exists>cap. caps_of_state s (aa, ba) = Some cap \<and> x \<in> obj_refs cap \<and> vs_cap_ref cap = Some xa))
 3. \<And>s x xa p' capa. \<lbrakk>\<forall>vref cap'. cte_wp_at ((=) cap') ptr s \<longrightarrow> vs_cap_ref cap' = Some vref \<longrightarrow> vs_cap_ref cap = Some vref \<and> obj_refs cap = obj_refs cap' \<or> \<not> is_final_cap' cap' s \<and> \<not> reachable_pg_cap cap' s \<or> (\<forall>oref. oref \<in> obj_refs cap' \<longrightarrow> (vref, oref) \<notin> vs_lookup_pages s); unique_table_refs (caps_of_state s); (xa \<unrhd> x) s; xa \<noteq> [VSRef 0 (Some AASIDPool), VSRef 0 None]; caps_of_state s p' = Some capa; x \<in> obj_refs capa; vs_cap_ref capa = Some xa; p' \<noteq> ptr\<rbrakk> \<Longrightarrow> \<exists>p' capa. ((caps_of_state s)(ptr \<mapsto> cap)) p' = Some capa \<and> x \<in> obj_refs capa \<and> vs_cap_ref capa = Some xa proof (prove)
goal (3 subgoals):
 1. \<And>s x xa a b cap xb xc cap'. \<lbrakk>unique_table_refs (caps_of_state s); (xa \<unrhd> x) s; xa \<noteq> [VSRef 0 (Some AASIDPool), VSRef 0 None]; caps_of_state s (a, b) = Some cap; x \<in> obj_refs cap; vs_cap_ref cap = Some xa; ptr = (a, b); \<not> reachable_pg_cap cap s; xb = a \<longrightarrow> xc \<noteq> b; caps_of_state s (xb, xc) = Some cap'; obj_refs cap' = obj_refs cap; cap_irqs cap' = cap_irqs cap; arch_gen_refs cap' = arch_gen_refs cap; \<not> is_final_cap' cap' s\<rbrakk> \<Longrightarrow> vs_cap_ref cap' = Some xa
 2. \<And>s x xa a b capa. \<lbrakk>unique_table_refs (caps_of_state s); (xa \<unrhd> x) s; xa \<noteq> [VSRef 0 (Some AASIDPool), VSRef 0 None]; caps_of_state s (a, b) = Some capa; x \<in> obj_refs capa; vs_cap_ref capa = Some xa; ptr = (a, b); \<forall>oref. oref \<in> obj_refs capa \<longrightarrow> (xa, oref) \<notin> vs_lookup_pages s\<rbrakk> \<Longrightarrow> \<exists>aa ba. (aa = a \<and> ba = b \<longrightarrow> x \<in> obj_refs cap \<and> vs_cap_ref cap = Some xa) \<and> ((aa = a \<longrightarrow> ba \<noteq> b) \<longrightarrow> (\<exists>cap. caps_of_state s (aa, ba) = Some cap \<and> x \<in> obj_refs cap \<and> vs_cap_ref cap = Some xa))
 3. \<And>s x xa p' capa. \<lbrakk>\<forall>vref cap'. cte_wp_at ((=) cap') ptr s \<longrightarrow> vs_cap_ref cap' = Some vref \<longrightarrow> vs_cap_ref cap = Some vref \<and> obj_refs cap = obj_refs cap' \<or> \<not> is_final_cap' cap' s \<and> \<not> reachable_pg_cap cap' s \<or> (\<forall>oref. oref \<in> obj_refs cap' \<longrightarrow> (vref, oref) \<notin> vs_lookup_pages s); unique_table_refs (caps_of_state s); (xa \<unrhd> x) s; xa \<noteq> [VSRef 0 (Some AASIDPool), VSRef 0 None]; caps_of_state s p' = Some capa; x \<in> obj_refs capa; vs_cap_ref capa = Some xa; p' \<noteq> ptr\<rbrakk> \<Longrightarrow> \<exists>p' capa. ((caps_of_state s)(ptr \<mapsto> cap)) p' = Some capa \<and> x \<in> obj_refs capa \<and> vs_cap_ref capa = Some xa proof (prove)
goal (3 subgoals):
 1. \<And>s x xa a b cap xb xc cap'. \<lbrakk>(xa \<unrhd> x) s; xa \<noteq> [VSRef 0 (Some AASIDPool), VSRef 0 None]; caps_of_state s (a, b) = Some cap; x \<in> obj_refs cap; vs_cap_ref cap = Some xa; ptr = (a, b); \<not> reachable_pg_cap cap s; xb = a \<longrightarrow> xc \<noteq> b; caps_of_state s (xb, xc) = Some cap'; obj_refs cap' = obj_refs cap; cap_irqs cap' = cap_irqs cap; arch_gen_refs cap' = arch_gen_refs cap; \<not> is_final_cap' cap' s; table_cap_ref cap' = table_cap_ref cap\<rbrakk> \<Longrightarrow> vs_cap_ref cap' = Some xa
 2. \<And>s x xa a b capa. \<lbrakk>unique_table_refs (caps_of_state s); (xa \<unrhd> x) s; xa \<noteq> [VSRef 0 (Some AASIDPool), VSRef 0 None]; caps_of_state s (a, b) = Some capa; x \<in> obj_refs capa; vs_cap_ref capa = Some xa; ptr = (a, b); \<forall>oref. oref \<in> obj_refs capa \<longrightarrow> (xa, oref) \<notin> vs_lookup_pages s\<rbrakk> \<Longrightarrow> \<exists>aa ba. (aa = a \<and> ba = b \<longrightarrow> x \<in> obj_refs cap \<and> vs_cap_ref cap = Some xa) \<and> ((aa = a \<longrightarrow> ba \<noteq> b) \<longrightarrow> (\<exists>cap. caps_of_state s (aa, ba) = Some cap \<and> x \<in> obj_refs cap \<and> vs_cap_ref cap = Some xa))
 3. \<And>s x xa p' capa. \<lbrakk>\<forall>vref cap'. cte_wp_at ((=) cap') ptr s \<longrightarrow> vs_cap_ref cap' = Some vref \<longrightarrow> vs_cap_ref cap = Some vref \<and> obj_refs cap = obj_refs cap' \<or> \<not> is_final_cap' cap' s \<and> \<not> reachable_pg_cap cap' s \<or> (\<forall>oref. oref \<in> obj_refs cap' \<longrightarrow> (vref, oref) \<notin> vs_lookup_pages s); unique_table_refs (caps_of_state s); (xa \<unrhd> x) s; xa \<noteq> [VSRef 0 (Some AASIDPool), VSRef 0 None]; caps_of_state s p' = Some capa; x \<in> obj_refs capa; vs_cap_ref capa = Some xa; p' \<noteq> ptr\<rbrakk> \<Longrightarrow> \<exists>p' capa. ((caps_of_state s)(ptr \<mapsto> cap)) p' = Some capa \<and> x \<in> obj_refs capa \<and> vs_cap_ref capa = Some xa proof (prove)
goal (3 subgoals):
 1. \<And>s x xa a b cap xb xc cap'. \<lbrakk>(xa \<unrhd> x) s; xa \<noteq> [VSRef 0 (Some AASIDPool), VSRef 0 None]; caps_of_state s (a, b) = Some cap; x \<in> obj_refs cap; vs_cap_ref cap = Some xa; ptr = (a, b); (\<forall>dev p R sz m. cap \<noteq> ArchObjectCap (PageCap dev p R sz m)) \<or> (xa, obj_ref_of cap) \<notin> vs_lookup_pages s; xb = a \<longrightarrow> xc \<noteq> b; caps_of_state s (xb, xc) = Some cap'; obj_refs cap' = obj_refs cap; cap_irqs cap' = cap_irqs cap; arch_gen_refs cap' = arch_gen_refs cap; \<not> is_final_cap' cap' s; table_cap_ref cap' = table_cap_ref cap\<rbrakk> \<Longrightarrow> vs_cap_ref cap' = Some xa
 2. \<And>s x xa a b capa. \<lbrakk>unique_table_refs (caps_of_state s); (xa \<unrhd> x) s; xa \<noteq> [VSRef 0 (Some AASIDPool), VSRef 0 None]; caps_of_state s (a, b) = Some capa; x \<in> obj_refs capa; vs_cap_ref capa = Some xa; ptr = (a, b); \<forall>oref. oref \<in> obj_refs capa \<longrightarrow> (xa, oref) \<notin> vs_lookup_pages s\<rbrakk> \<Longrightarrow> \<exists>aa ba. (aa = a \<and> ba = b \<longrightarrow> x \<in> obj_refs cap \<and> vs_cap_ref cap = Some xa) \<and> ((aa = a \<longrightarrow> ba \<noteq> b) \<longrightarrow> (\<exists>cap. caps_of_state s (aa, ba) = Some cap \<and> x \<in> obj_refs cap \<and> vs_cap_ref cap = Some xa))
 3. \<And>s x xa p' capa. \<lbrakk>\<forall>vref cap'. cte_wp_at ((=) cap') ptr s \<longrightarrow> vs_cap_ref cap' = Some vref \<longrightarrow> vs_cap_ref cap = Some vref \<and> obj_refs cap = obj_refs cap' \<or> \<not> is_final_cap' cap' s \<and> \<not> reachable_pg_cap cap' s \<or> (\<forall>oref. oref \<in> obj_refs cap' \<longrightarrow> (vref, oref) \<notin> vs_lookup_pages s); unique_table_refs (caps_of_state s); (xa \<unrhd> x) s; xa \<noteq> [VSRef 0 (Some AASIDPool), VSRef 0 None]; caps_of_state s p' = Some capa; x \<in> obj_refs capa; vs_cap_ref capa = Some xa; p' \<noteq> ptr\<rbrakk> \<Longrightarrow> \<exists>p' capa. ((caps_of_state s)(ptr \<mapsto> cap)) p' = Some capa \<and> x \<in> obj_refs capa \<and> vs_cap_ref capa = Some xa proof (prove)
goal (3 subgoals):
 1. \<And>s x xa a b cap xb xc cap' x12. \<lbrakk>(xa \<unrhd> x) s; xa \<noteq> [VSRef 0 (Some AASIDPool), VSRef 0 None]; caps_of_state s (a, b) = Some (ArchObjectCap x12); aobj_ref x12 = Some x; vs_cap_ref (ArchObjectCap x12) = Some xa; ptr = (a, b); \<forall>dev p R sz m. x12 \<noteq> PageCap dev p R sz m; xb = a \<longrightarrow> xc \<noteq> b; caps_of_state s (xb, xc) = Some cap'; obj_refs cap' = {x}; cap_irqs cap' = {}; arch_gen_refs cap' = arch_gen_obj_refs x12; \<not> is_final_cap' cap' s; table_cap_ref cap' = table_cap_ref (ArchObjectCap x12); cap = ArchObjectCap x12\<rbrakk> \<Longrightarrow> vs_cap_ref cap' = Some xa
 2. \<And>s x xa a b capa. \<lbrakk>unique_table_refs (caps_of_state s); (xa \<unrhd> x) s; xa \<noteq> [VSRef 0 (Some AASIDPool), VSRef 0 None]; caps_of_state s (a, b) = Some capa; x \<in> obj_refs capa; vs_cap_ref capa = Some xa; ptr = (a, b); \<forall>oref. oref \<in> obj_refs capa \<longrightarrow> (xa, oref) \<notin> vs_lookup_pages s\<rbrakk> \<Longrightarrow> \<exists>aa ba. (aa = a \<and> ba = b \<longrightarrow> x \<in> obj_refs cap \<and> vs_cap_ref cap = Some xa) \<and> ((aa = a \<longrightarrow> ba \<noteq> b) \<longrightarrow> (\<exists>cap. caps_of_state s (aa, ba) = Some cap \<and> x \<in> obj_refs cap \<and> vs_cap_ref cap = Some xa))
 3. \<And>s x xa p' capa. \<lbrakk>\<forall>vref cap'. cte_wp_at ((=) cap') ptr s \<longrightarrow> vs_cap_ref cap' = Some vref \<longrightarrow> vs_cap_ref cap = Some vref \<and> obj_refs cap = obj_refs cap' \<or> \<not> is_final_cap' cap' s \<and> \<not> reachable_pg_cap cap' s \<or> (\<forall>oref. oref \<in> obj_refs cap' \<longrightarrow> (vref, oref) \<notin> vs_lookup_pages s); unique_table_refs (caps_of_state s); (xa \<unrhd> x) s; xa \<noteq> [VSRef 0 (Some AASIDPool), VSRef 0 None]; caps_of_state s p' = Some capa; x \<in> obj_refs capa; vs_cap_ref capa = Some xa; p' \<noteq> ptr\<rbrakk> \<Longrightarrow> \<exists>p' capa. ((caps_of_state s)(ptr \<mapsto> cap)) p' = Some capa \<and> x \<in> obj_refs capa \<and> vs_cap_ref capa = Some xa proof (prove)
goal (3 subgoals):
 1. \<And>s x xa a b cap xb xc cap' arch_cap. \<lbrakk>(xa \<unrhd> x) s; xa \<noteq> [VSRef 0 (Some AASIDPool), VSRef 0 None]; caps_of_state s (a, b) = Some (ArchObjectCap arch_cap); aobj_ref arch_cap = Some x; vs_cap_ref (ArchObjectCap arch_cap) = Some xa; ptr = (a, b); \<forall>dev p R sz m. arch_cap \<noteq> PageCap dev p R sz m; xb = a \<longrightarrow> xc \<noteq> b; caps_of_state s (xb, xc) = Some cap'; obj_refs cap' = {x}; cap_irqs cap' = {}; arch_gen_refs cap' = arch_gen_obj_refs arch_cap; \<not> is_final_cap' cap' s; table_cap_ref cap' = table_cap_ref (ArchObjectCap arch_cap); cap = ArchObjectCap arch_cap\<rbrakk> \<Longrightarrow> vs_cap_ref cap' = Some xa
 2. \<And>s x xa a b capa. \<lbrakk>unique_table_refs (caps_of_state s); (xa \<unrhd> x) s; xa \<noteq> [VSRef 0 (Some AASIDPool), VSRef 0 None]; caps_of_state s (a, b) = Some capa; x \<in> obj_refs capa; vs_cap_ref capa = Some xa; ptr = (a, b); \<forall>oref. oref \<in> obj_refs capa \<longrightarrow> (xa, oref) \<notin> vs_lookup_pages s\<rbrakk> \<Longrightarrow> \<exists>aa ba. (aa = a \<and> ba = b \<longrightarrow> x \<in> obj_refs cap \<and> vs_cap_ref cap = Some xa) \<and> ((aa = a \<longrightarrow> ba \<noteq> b) \<longrightarrow> (\<exists>cap. caps_of_state s (aa, ba) = Some cap \<and> x \<in> obj_refs cap \<and> vs_cap_ref cap = Some xa))
 3. \<And>s x xa p' capa. \<lbrakk>\<forall>vref cap'. cte_wp_at ((=) cap') ptr s \<longrightarrow> vs_cap_ref cap' = Some vref \<longrightarrow> vs_cap_ref cap = Some vref \<and> obj_refs cap = obj_refs cap' \<or> \<not> is_final_cap' cap' s \<and> \<not> reachable_pg_cap cap' s \<or> (\<forall>oref. oref \<in> obj_refs cap' \<longrightarrow> (vref, oref) \<notin> vs_lookup_pages s); unique_table_refs (caps_of_state s); (xa \<unrhd> x) s; xa \<noteq> [VSRef 0 (Some AASIDPool), VSRef 0 None]; caps_of_state s p' = Some capa; x \<in> obj_refs capa; vs_cap_ref capa = Some xa; p' \<noteq> ptr\<rbrakk> \<Longrightarrow> \<exists>p' capa. ((caps_of_state s)(ptr \<mapsto> cap)) p' = Some capa \<and> x \<in> obj_refs capa \<and> vs_cap_ref capa = Some xa proof (prove)
goal (6 subgoals):
 1. \<And>s x xa a b cap xb xc cap' arch_cap x11 x12. \<lbrakk>(xa \<unrhd> x) s; xa \<noteq> [VSRef 0 (Some AASIDPool), VSRef 0 None]; caps_of_state s (a, b) = Some (ArchObjectCap (ASIDPoolCap x x12)); x11 = x; [VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of x12)) None] = xa; ptr = (a, b); xb = a \<longrightarrow> xc \<noteq> b; caps_of_state s (xb, xc) = Some cap'; obj_refs cap' = {x}; cap_irqs cap' = {}; arch_gen_refs cap' = {}; \<not> is_final_cap' cap' s; table_cap_ref cap' = Some xa; cap = ArchObjectCap (ASIDPoolCap x x12); arch_cap = ASIDPoolCap x x12\<rbrakk> \<Longrightarrow> vs_cap_ref cap' = Some xa
 2. \<And>s x xa a b cap xb xc cap' arch_cap x31 x32 x33 x34 x35. \<lbrakk>(xa \<unrhd> x) s; caps_of_state s (a, b) = Some (ArchObjectCap (PageCap True x x33 x34 x35)); x32 = x; vs_cap_ref (ArchObjectCap (PageCap True x x33 x34 x35)) = Some xa; ptr = (a, b); All Not; caps_of_state s (xb, xc) = Some cap'; obj_refs cap' = {x}; cap_irqs cap' = {}; arch_gen_refs cap' = {}; x31; table_cap_ref cap' = None; cap = ArchObjectCap (PageCap True x x33 x34 x35); arch_cap = PageCap True x x33 x34 x35\<rbrakk> \<Longrightarrow> vs_cap_ref cap' = Some xa
 3. \<And>s x xa a b cap xb xc cap' arch_cap x41 x42. \<lbrakk>(xa \<unrhd> x) s; xa \<noteq> [VSRef 0 (Some AASIDPool), VSRef 0 None]; caps_of_state s (a, b) = Some (ArchObjectCap (PageTableCap x x42)); x41 = x; (case x42 of None \<Rightarrow> None | Some (asid, vptr) \<Rightarrow> Some [VSRef (vptr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None]) = Some xa; ptr = (a, b); xb = a \<longrightarrow> xc \<noteq> b; caps_of_state s (xb, xc) = Some cap'; obj_refs cap' = {x}; cap_irqs cap' = {}; arch_gen_refs cap' = {}; \<not> is_final_cap' cap' s; table_cap_ref cap' = Some xa; cap = ArchObjectCap (PageTableCap x x42); arch_cap = PageTableCap x x42\<rbrakk> \<Longrightarrow> vs_cap_ref cap' = Some xa
 4. \<And>s x xa a b cap xb xc cap' arch_cap x51 x52. \<lbrakk>(xa \<unrhd> x) s; xa \<noteq> [VSRef 0 (Some AASIDPool), VSRef 0 None]; caps_of_state s (a, b) = Some (ArchObjectCap (PageDirectoryCap x x52)); x51 = x; (case x52 of None \<Rightarrow> None | Some asid \<Rightarrow> Some [VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None]) = Some xa; ptr = (a, b); xb = a \<longrightarrow> xc \<noteq> b; caps_of_state s (xb, xc) = Some cap'; obj_refs cap' = {x}; cap_irqs cap' = {}; arch_gen_refs cap' = {}; \<not> is_final_cap' cap' s; table_cap_ref cap' = Some xa; cap = ArchObjectCap (PageDirectoryCap x x52); arch_cap = PageDirectoryCap x x52\<rbrakk> \<Longrightarrow> vs_cap_ref cap' = Some xa
 5. \<And>s x xa a b capa. \<lbrakk>unique_table_refs (caps_of_state s); (xa \<unrhd> x) s; xa \<noteq> [VSRef 0 (Some AASIDPool), VSRef 0 None]; caps_of_state s (a, b) = Some capa; x \<in> obj_refs capa; vs_cap_ref capa = Some xa; ptr = (a, b); \<forall>oref. oref \<in> obj_refs capa \<longrightarrow> (xa, oref) \<notin> vs_lookup_pages s\<rbrakk> \<Longrightarrow> \<exists>aa ba. (aa = a \<and> ba = b \<longrightarrow> x \<in> obj_refs cap \<and> vs_cap_ref cap = Some xa) \<and> ((aa = a \<longrightarrow> ba \<noteq> b) \<longrightarrow> (\<exists>cap. caps_of_state s (aa, ba) = Some cap \<and> x \<in> obj_refs cap \<and> vs_cap_ref cap = Some xa))
 6. \<And>s x xa p' capa. \<lbrakk>\<forall>vref cap'. cte_wp_at ((=) cap') ptr s \<longrightarrow> vs_cap_ref cap' = Some vref \<longrightarrow> vs_cap_ref cap = Some vref \<and> obj_refs cap = obj_refs cap' \<or> \<not> is_final_cap' cap' s \<and> \<not> reachable_pg_cap cap' s \<or> (\<forall>oref. oref \<in> obj_refs cap' \<longrightarrow> (vref, oref) \<notin> vs_lookup_pages s); unique_table_refs (caps_of_state s); (xa \<unrhd> x) s; xa \<noteq> [VSRef 0 (Some AASIDPool), VSRef 0 None]; caps_of_state s p' = Some capa; x \<in> obj_refs capa; vs_cap_ref capa = Some xa; p' \<noteq> ptr\<rbrakk> \<Longrightarrow> \<exists>p' capa. ((caps_of_state s)(ptr \<mapsto> cap)) p' = Some capa \<and> x \<in> obj_refs capa \<and> vs_cap_ref capa = Some xa proof (prove)
goal (5 subgoals):
 1. \<And>s x xa a b cap xb xc cap' arch_cap x31 x32 x33 x34 x35. \<lbrakk>(xa \<unrhd> x) s; caps_of_state s (a, b) = Some (ArchObjectCap (PageCap True x x33 x34 x35)); x32 = x; vs_cap_ref (ArchObjectCap (PageCap True x x33 x34 x35)) = Some xa; ptr = (a, b); All Not; caps_of_state s (xb, xc) = Some cap'; obj_refs cap' = {x}; cap_irqs cap' = {}; arch_gen_refs cap' = {}; x31; table_cap_ref cap' = None; cap = ArchObjectCap (PageCap True x x33 x34 x35); arch_cap = PageCap True x x33 x34 x35\<rbrakk> \<Longrightarrow> vs_cap_ref cap' = Some xa
 2. \<And>s x xa a b cap xb xc cap' arch_cap x41 x42. \<lbrakk>(xa \<unrhd> x) s; xa \<noteq> [VSRef 0 (Some AASIDPool), VSRef 0 None]; caps_of_state s (a, b) = Some (ArchObjectCap (PageTableCap x x42)); x41 = x; (case x42 of None \<Rightarrow> None | Some (asid, vptr) \<Rightarrow> Some [VSRef (vptr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None]) = Some xa; ptr = (a, b); xb = a \<longrightarrow> xc \<noteq> b; caps_of_state s (xb, xc) = Some cap'; obj_refs cap' = {x}; cap_irqs cap' = {}; arch_gen_refs cap' = {}; \<not> is_final_cap' cap' s; table_cap_ref cap' = Some xa; cap = ArchObjectCap (PageTableCap x x42); arch_cap = PageTableCap x x42\<rbrakk> \<Longrightarrow> vs_cap_ref cap' = Some xa
 3. \<And>s x xa a b cap xb xc cap' arch_cap x51 x52. \<lbrakk>(xa \<unrhd> x) s; xa \<noteq> [VSRef 0 (Some AASIDPool), VSRef 0 None]; caps_of_state s (a, b) = Some (ArchObjectCap (PageDirectoryCap x x52)); x51 = x; (case x52 of None \<Rightarrow> None | Some asid \<Rightarrow> Some [VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None]) = Some xa; ptr = (a, b); xb = a \<longrightarrow> xc \<noteq> b; caps_of_state s (xb, xc) = Some cap'; obj_refs cap' = {x}; cap_irqs cap' = {}; arch_gen_refs cap' = {}; \<not> is_final_cap' cap' s; table_cap_ref cap' = Some xa; cap = ArchObjectCap (PageDirectoryCap x x52); arch_cap = PageDirectoryCap x x52\<rbrakk> \<Longrightarrow> vs_cap_ref cap' = Some xa
 4. \<And>s x xa a b capa. \<lbrakk>unique_table_refs (caps_of_state s); (xa \<unrhd> x) s; xa \<noteq> [VSRef 0 (Some AASIDPool), VSRef 0 None]; caps_of_state s (a, b) = Some capa; x \<in> obj_refs capa; vs_cap_ref capa = Some xa; ptr = (a, b); \<forall>oref. oref \<in> obj_refs capa \<longrightarrow> (xa, oref) \<notin> vs_lookup_pages s\<rbrakk> \<Longrightarrow> \<exists>aa ba. (aa = a \<and> ba = b \<longrightarrow> x \<in> obj_refs cap \<and> vs_cap_ref cap = Some xa) \<and> ((aa = a \<longrightarrow> ba \<noteq> b) \<longrightarrow> (\<exists>cap. caps_of_state s (aa, ba) = Some cap \<and> x \<in> obj_refs cap \<and> vs_cap_ref cap = Some xa))
 5. \<And>s x xa p' capa. \<lbrakk>\<forall>vref cap'. cte_wp_at ((=) cap') ptr s \<longrightarrow> vs_cap_ref cap' = Some vref \<longrightarrow> vs_cap_ref cap = Some vref \<and> obj_refs cap = obj_refs cap' \<or> \<not> is_final_cap' cap' s \<and> \<not> reachable_pg_cap cap' s \<or> (\<forall>oref. oref \<in> obj_refs cap' \<longrightarrow> (vref, oref) \<notin> vs_lookup_pages s); unique_table_refs (caps_of_state s); (xa \<unrhd> x) s; xa \<noteq> [VSRef 0 (Some AASIDPool), VSRef 0 None]; caps_of_state s p' = Some capa; x \<in> obj_refs capa; vs_cap_ref capa = Some xa; p' \<noteq> ptr\<rbrakk> \<Longrightarrow> \<exists>p' capa. ((caps_of_state s)(ptr \<mapsto> cap)) p' = Some capa \<and> x \<in> obj_refs capa \<and> vs_cap_ref capa = Some xa proof (prove)
goal (4 subgoals):
 1. \<And>s x xa a b cap xb xc cap' arch_cap x41 x42. \<lbrakk>(xa \<unrhd> x) s; xa \<noteq> [VSRef 0 (Some AASIDPool), VSRef 0 None]; caps_of_state s (a, b) = Some (ArchObjectCap (PageTableCap x x42)); x41 = x; (case x42 of None \<Rightarrow> None | Some (asid, vptr) \<Rightarrow> Some [VSRef (vptr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None]) = Some xa; ptr = (a, b); xb = a \<longrightarrow> xc \<noteq> b; caps_of_state s (xb, xc) = Some cap'; obj_refs cap' = {x}; cap_irqs cap' = {}; arch_gen_refs cap' = {}; \<not> is_final_cap' cap' s; table_cap_ref cap' = Some xa; cap = ArchObjectCap (PageTableCap x x42); arch_cap = PageTableCap x x42\<rbrakk> \<Longrightarrow> vs_cap_ref cap' = Some xa
 2. \<And>s x xa a b cap xb xc cap' arch_cap x51 x52. \<lbrakk>(xa \<unrhd> x) s; xa \<noteq> [VSRef 0 (Some AASIDPool), VSRef 0 None]; caps_of_state s (a, b) = Some (ArchObjectCap (PageDirectoryCap x x52)); x51 = x; (case x52 of None \<Rightarrow> None | Some asid \<Rightarrow> Some [VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None]) = Some xa; ptr = (a, b); xb = a \<longrightarrow> xc \<noteq> b; caps_of_state s (xb, xc) = Some cap'; obj_refs cap' = {x}; cap_irqs cap' = {}; arch_gen_refs cap' = {}; \<not> is_final_cap' cap' s; table_cap_ref cap' = Some xa; cap = ArchObjectCap (PageDirectoryCap x x52); arch_cap = PageDirectoryCap x x52\<rbrakk> \<Longrightarrow> vs_cap_ref cap' = Some xa
 3. \<And>s x xa a b capa. \<lbrakk>unique_table_refs (caps_of_state s); (xa \<unrhd> x) s; xa \<noteq> [VSRef 0 (Some AASIDPool), VSRef 0 None]; caps_of_state s (a, b) = Some capa; x \<in> obj_refs capa; vs_cap_ref capa = Some xa; ptr = (a, b); \<forall>oref. oref \<in> obj_refs capa \<longrightarrow> (xa, oref) \<notin> vs_lookup_pages s\<rbrakk> \<Longrightarrow> \<exists>aa ba. (aa = a \<and> ba = b \<longrightarrow> x \<in> obj_refs cap \<and> vs_cap_ref cap = Some xa) \<and> ((aa = a \<longrightarrow> ba \<noteq> b) \<longrightarrow> (\<exists>cap. caps_of_state s (aa, ba) = Some cap \<and> x \<in> obj_refs cap \<and> vs_cap_ref cap = Some xa))
 4. \<And>s x xa p' capa. \<lbrakk>\<forall>vref cap'. cte_wp_at ((=) cap') ptr s \<longrightarrow> vs_cap_ref cap' = Some vref \<longrightarrow> vs_cap_ref cap = Some vref \<and> obj_refs cap = obj_refs cap' \<or> \<not> is_final_cap' cap' s \<and> \<not> reachable_pg_cap cap' s \<or> (\<forall>oref. oref \<in> obj_refs cap' \<longrightarrow> (vref, oref) \<notin> vs_lookup_pages s); unique_table_refs (caps_of_state s); (xa \<unrhd> x) s; xa \<noteq> [VSRef 0 (Some AASIDPool), VSRef 0 None]; caps_of_state s p' = Some capa; x \<in> obj_refs capa; vs_cap_ref capa = Some xa; p' \<noteq> ptr\<rbrakk> \<Longrightarrow> \<exists>p' capa. ((caps_of_state s)(ptr \<mapsto> cap)) p' = Some capa \<and> x \<in> obj_refs capa \<and> vs_cap_ref capa = Some xa proof (prove)
goal (1 subgoal):
 1. \<And>s x xa a b capa. \<lbrakk>\<forall>vref cap'. cte_wp_at ((=) cap') ptr s \<longrightarrow> vs_cap_ref cap' = Some vref \<longrightarrow> vs_cap_ref cap = Some vref \<and> obj_refs cap = obj_refs cap' \<or> \<not> is_final_cap' cap' s \<and> \<not> reachable_pg_cap cap' s \<or> (\<forall>oref. oref \<in> obj_refs cap' \<longrightarrow> (vref, oref) \<notin> vs_lookup_pages s); unique_table_refs (caps_of_state s); (xa \<unrhd> x) s; xa \<noteq> [VSRef 0 (Some AASIDPool), VSRef 0 None]; caps_of_state s (a, b) = Some capa; x \<in> obj_refs capa; vs_cap_ref capa = Some xa; (a, b) \<noteq> ptr\<rbrakk> \<Longrightarrow> \<exists>a b. ((a, b) = ptr \<longrightarrow> x \<in> obj_refs cap \<and> vs_cap_ref cap = Some xa) \<and> ((a, b) \<noteq> ptr \<longrightarrow> (\<exists>cap. caps_of_state s (a, b) = Some cap \<and> x \<in> obj_refs cap \<and> vs_cap_ref cap = Some xa)) proof (prove)
goal:
No subgoals!