theory ArchCSpace_AI

lemma set_untyped_cap_as_full_valid_arch_caps [CSpace_AI_assms]:
  "\<lbrace>valid_arch_caps and cte_wp_at ((=) src_cap) src\<rbrace>
   set_untyped_cap_as_full src_cap cap src
   \<lbrace>\<lambda>ya. valid_arch_caps\<rbrace>" apply (clarsimp simp:valid_arch_caps_def set_untyped_cap_as_full_def) apply (intro conjI impI) apply (wp set_cap_valid_vs_lookup set_cap_valid_table_caps) apply (clarsimp simp del:fun_upd_apply simp:cte_wp_at_caps_of_state) apply (subst unique_table_refs_upd_eqD) apply ((simp add: is_cap_simps table_cap_ref_def)+) apply clarsimp apply (subst unique_table_caps_upd_eqD) apply simp+ apply (clarsimp simp:is_cap_simps cte_wp_at_caps_of_state)+ apply wp apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_arch_caps and cte_wp_at ((=) src_cap) src\<rbrace> set_untyped_cap_as_full src_cap cap src \<lbrace>\<lambda>ya. valid_arch_caps\<rbrace> proof (prove)
goal (1 subgoal):
 1. (is_untyped_cap src_cap \<and> is_untyped_cap cap \<and> obj_ref_of src_cap = obj_ref_of cap \<and> cap_bits_untyped src_cap = cap_bits_untyped cap \<longrightarrow> \<lbrace>valid_vs_lookup and valid_table_caps and (\<lambda>s. unique_table_caps (caps_of_state s) \<and> unique_table_refs (caps_of_state s)) and cte_wp_at ((=) src_cap) src\<rbrace> set_cap (max_free_index_update src_cap) src \<lbrace>\<lambda>ya. valid_vs_lookup and valid_table_caps and (\<lambda>s. unique_table_caps (caps_of_state s) \<and> unique_table_refs (caps_of_state s))\<rbrace>) \<and> ((obj_ref_of src_cap = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap src_cap \<longrightarrow> cap_bits_untyped src_cap \<noteq> cap_bits_untyped cap) \<longrightarrow> \<lbrace>valid_vs_lookup and valid_table_caps and (\<lambda>s. unique_table_caps (caps_of_state s) \<and> unique_table_refs (caps_of_state s)) and cte_wp_at ((=) src_cap) src\<rbrace> return () \<lbrace>\<lambda>ya. valid_vs_lookup and valid_table_caps and (\<lambda>s. unique_table_caps (caps_of_state s) \<and> unique_table_refs (caps_of_state s))\<rbrace>) proof (prove)
goal (2 subgoals):
 1. is_untyped_cap src_cap \<and> is_untyped_cap cap \<and> obj_ref_of src_cap = obj_ref_of cap \<and> cap_bits_untyped src_cap = cap_bits_untyped cap \<Longrightarrow> \<lbrace>valid_vs_lookup and valid_table_caps and (\<lambda>s. unique_table_caps (caps_of_state s) \<and> unique_table_refs (caps_of_state s)) and cte_wp_at ((=) src_cap) src\<rbrace> set_cap (max_free_index_update src_cap) src \<lbrace>\<lambda>ya. valid_vs_lookup and valid_table_caps and (\<lambda>s. unique_table_caps (caps_of_state s) \<and> unique_table_refs (caps_of_state s))\<rbrace>
 2. obj_ref_of src_cap = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap src_cap \<longrightarrow> cap_bits_untyped src_cap \<noteq> cap_bits_untyped cap \<Longrightarrow> \<lbrace>valid_vs_lookup and valid_table_caps and (\<lambda>s. unique_table_caps (caps_of_state s) \<and> unique_table_refs (caps_of_state s)) and cte_wp_at ((=) src_cap) src\<rbrace> return () \<lbrace>\<lambda>ya. valid_vs_lookup and valid_table_caps and (\<lambda>s. unique_table_caps (caps_of_state s) \<and> unique_table_refs (caps_of_state s))\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>is_untyped_cap src_cap \<and> is_untyped_cap cap \<and> obj_ref_of src_cap = obj_ref_of cap \<and> cap_bits_untyped src_cap = cap_bits_untyped cap; (valid_vs_lookup and valid_table_caps and (\<lambda>s. unique_table_caps (caps_of_state s) \<and> unique_table_refs (caps_of_state s)) and cte_wp_at ((=) src_cap) src) s\<rbrakk> \<Longrightarrow> (valid_vs_lookup s \<and> (\<forall>vref cap'. cte_wp_at ((=) cap') src s \<longrightarrow> vs_cap_ref cap' = Some vref \<longrightarrow> vs_cap_ref (max_free_index_update src_cap) = Some vref \<and> obj_refs (max_free_index_update src_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)) \<and> (valid_table_caps s \<and> (is_pt_cap (max_free_index_update src_cap) \<or> is_pd_cap (max_free_index_update src_cap) \<longrightarrow> cap_asid (max_free_index_update src_cap) = None \<longrightarrow> (\<forall>r\<in>obj_refs (max_free_index_update src_cap). obj_at (empty_table (set (second_level_tables (arch_state s)))) r s))) \<and> unique_table_caps ((caps_of_state s)(src \<mapsto> max_free_index_update src_cap)) \<and> unique_table_refs ((caps_of_state s)(src \<mapsto> max_free_index_update src_cap))
 2. obj_ref_of src_cap = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap src_cap \<longrightarrow> cap_bits_untyped src_cap \<noteq> cap_bits_untyped cap \<Longrightarrow> \<lbrace>valid_vs_lookup and valid_table_caps and (\<lambda>s. unique_table_caps (caps_of_state s) \<and> unique_table_refs (caps_of_state s)) and cte_wp_at ((=) src_cap) src\<rbrace> return () \<lbrace>\<lambda>ya. valid_vs_lookup and valid_table_caps and (\<lambda>s. unique_table_caps (caps_of_state s) \<and> unique_table_refs (caps_of_state s))\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>is_untyped_cap src_cap; valid_vs_lookup s; is_untyped_cap cap; valid_table_caps s; obj_ref_of src_cap = obj_ref_of cap; cap_bits_untyped src_cap = cap_bits_untyped cap; unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s); caps_of_state s src = Some src_cap\<rbrakk> \<Longrightarrow> (is_pt_cap src_cap \<longrightarrow> cap_asid src_cap = None \<longrightarrow> (\<forall>r\<in>obj_refs src_cap. obj_at (empty_table (set (second_level_tables (arch_state s)))) r s)) \<and> (is_pd_cap src_cap \<longrightarrow> cap_asid src_cap = None \<longrightarrow> (\<forall>r\<in>obj_refs src_cap. obj_at (empty_table (set (second_level_tables (arch_state s)))) r s)) \<and> unique_table_caps ((caps_of_state s)(src \<mapsto> max_free_index_update src_cap)) \<and> unique_table_refs ((caps_of_state s)(src \<mapsto> max_free_index_update src_cap))
 2. obj_ref_of src_cap = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap src_cap \<longrightarrow> cap_bits_untyped src_cap \<noteq> cap_bits_untyped cap \<Longrightarrow> \<lbrace>valid_vs_lookup and valid_table_caps and (\<lambda>s. unique_table_caps (caps_of_state s) \<and> unique_table_refs (caps_of_state s)) and cte_wp_at ((=) src_cap) src\<rbrace> return () \<lbrace>\<lambda>ya. valid_vs_lookup and valid_table_caps and (\<lambda>s. unique_table_caps (caps_of_state s) \<and> unique_table_refs (caps_of_state s))\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>s. \<lbrakk>is_untyped_cap src_cap; valid_vs_lookup s; is_untyped_cap cap; valid_table_caps s; obj_ref_of src_cap = obj_ref_of cap; cap_bits_untyped src_cap = cap_bits_untyped cap; unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s); caps_of_state s src = Some src_cap\<rbrakk> \<Longrightarrow> caps_of_state s src = Some (?b33 s)
 2. \<And>s. \<lbrakk>is_untyped_cap src_cap; valid_vs_lookup s; is_untyped_cap cap; valid_table_caps s; obj_ref_of src_cap = obj_ref_of cap; cap_bits_untyped src_cap = cap_bits_untyped cap; unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s); caps_of_state s src = Some src_cap\<rbrakk> \<Longrightarrow> obj_refs (?b33 s) = obj_refs (max_free_index_update src_cap)
 3. \<And>s. \<lbrakk>is_untyped_cap src_cap; valid_vs_lookup s; is_untyped_cap cap; valid_table_caps s; obj_ref_of src_cap = obj_ref_of cap; cap_bits_untyped src_cap = cap_bits_untyped cap; unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s); caps_of_state s src = Some src_cap\<rbrakk> \<Longrightarrow> table_cap_ref (?b33 s) = table_cap_ref (max_free_index_update src_cap)
 4. \<And>s. \<lbrakk>is_untyped_cap src_cap; valid_vs_lookup s; is_untyped_cap cap; valid_table_caps s; obj_ref_of src_cap = obj_ref_of cap; cap_bits_untyped src_cap = cap_bits_untyped cap; unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s); caps_of_state s src = Some src_cap\<rbrakk> \<Longrightarrow> (is_pt_cap src_cap \<longrightarrow> cap_asid src_cap = None \<longrightarrow> (\<forall>r\<in>obj_refs src_cap. obj_at (empty_table (set (second_level_tables (arch_state s)))) r s)) \<and> (is_pd_cap src_cap \<longrightarrow> cap_asid src_cap = None \<longrightarrow> (\<forall>r\<in>obj_refs src_cap. obj_at (empty_table (set (second_level_tables (arch_state s)))) r s)) \<and> unique_table_caps ((caps_of_state s)(src \<mapsto> max_free_index_update src_cap)) \<and> unique_table_refs (caps_of_state s)
 5. obj_ref_of src_cap = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap src_cap \<longrightarrow> cap_bits_untyped src_cap \<noteq> cap_bits_untyped cap \<Longrightarrow> \<lbrace>valid_vs_lookup and valid_table_caps and (\<lambda>s. unique_table_caps (caps_of_state s) \<and> unique_table_refs (caps_of_state s)) and cte_wp_at ((=) src_cap) src\<rbrace> return () \<lbrace>\<lambda>ya. valid_vs_lookup and valid_table_caps and (\<lambda>s. unique_table_caps (caps_of_state s) \<and> unique_table_refs (caps_of_state s))\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>s. \<lbrakk>\<exists>dev r bits f. src_cap = UntypedCap dev r bits f; valid_vs_lookup s; \<exists>dev r bits f. cap = UntypedCap dev r bits f; valid_table_caps s; obj_ref_of src_cap = obj_ref_of cap; cap_bits_untyped src_cap = cap_bits_untyped cap; unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s); caps_of_state s src = Some src_cap\<rbrakk> \<Longrightarrow> (case src_cap of ArchObjectCap (ASIDPoolCap obj_ref asid) \<Rightarrow> Some [VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | ArchObjectCap (PageTableCap obj_ref None) \<Rightarrow> None | ArchObjectCap (PageTableCap obj_ref (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] | ArchObjectCap (PageDirectoryCap obj_ref None) \<Rightarrow> None | ArchObjectCap (PageDirectoryCap obj_ref (Some asida)) \<Rightarrow> Some [VSRef (asida && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asida)) None] | ArchObjectCap _ \<Rightarrow> None | _ \<Rightarrow> None) = (case max_free_index_update src_cap of ArchObjectCap (ASIDPoolCap obj_ref asid) \<Rightarrow> Some [VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | ArchObjectCap (PageTableCap obj_ref None) \<Rightarrow> None | ArchObjectCap (PageTableCap obj_ref (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] | ArchObjectCap (PageDirectoryCap obj_ref None) \<Rightarrow> None | ArchObjectCap (PageDirectoryCap obj_ref (Some asida)) \<Rightarrow> Some [VSRef (asida && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asida)) None] | ArchObjectCap _ \<Rightarrow> None | _ \<Rightarrow> None)
 2. \<And>s. \<lbrakk>is_untyped_cap src_cap; valid_vs_lookup s; is_untyped_cap cap; valid_table_caps s; obj_ref_of src_cap = obj_ref_of cap; cap_bits_untyped src_cap = cap_bits_untyped cap; unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s); caps_of_state s src = Some src_cap\<rbrakk> \<Longrightarrow> (is_pt_cap src_cap \<longrightarrow> cap_asid src_cap = None \<longrightarrow> (\<forall>r\<in>obj_refs src_cap. obj_at (empty_table (set (second_level_tables (arch_state s)))) r s)) \<and> (is_pd_cap src_cap \<longrightarrow> cap_asid src_cap = None \<longrightarrow> (\<forall>r\<in>obj_refs src_cap. obj_at (empty_table (set (second_level_tables (arch_state s)))) r s)) \<and> unique_table_caps ((caps_of_state s)(src \<mapsto> max_free_index_update src_cap)) \<and> unique_table_refs (caps_of_state s)
 3. obj_ref_of src_cap = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap src_cap \<longrightarrow> cap_bits_untyped src_cap \<noteq> cap_bits_untyped cap \<Longrightarrow> \<lbrace>valid_vs_lookup and valid_table_caps and (\<lambda>s. unique_table_caps (caps_of_state s) \<and> unique_table_refs (caps_of_state s)) and cte_wp_at ((=) src_cap) src\<rbrace> return () \<lbrace>\<lambda>ya. valid_vs_lookup and valid_table_caps and (\<lambda>s. unique_table_caps (caps_of_state s) \<and> unique_table_refs (caps_of_state s))\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>is_untyped_cap src_cap; valid_vs_lookup s; is_untyped_cap cap; valid_table_caps s; obj_ref_of src_cap = obj_ref_of cap; cap_bits_untyped src_cap = cap_bits_untyped cap; unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s); caps_of_state s src = Some src_cap\<rbrakk> \<Longrightarrow> (is_pt_cap src_cap \<longrightarrow> cap_asid src_cap = None \<longrightarrow> (\<forall>r\<in>obj_refs src_cap. obj_at (empty_table (set (second_level_tables (arch_state s)))) r s)) \<and> (is_pd_cap src_cap \<longrightarrow> cap_asid src_cap = None \<longrightarrow> (\<forall>r\<in>obj_refs src_cap. obj_at (empty_table (set (second_level_tables (arch_state s)))) r s)) \<and> unique_table_caps ((caps_of_state s)(src \<mapsto> max_free_index_update src_cap)) \<and> unique_table_refs (caps_of_state s)
 2. obj_ref_of src_cap = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap src_cap \<longrightarrow> cap_bits_untyped src_cap \<noteq> cap_bits_untyped cap \<Longrightarrow> \<lbrace>valid_vs_lookup and valid_table_caps and (\<lambda>s. unique_table_caps (caps_of_state s) \<and> unique_table_refs (caps_of_state s)) and cte_wp_at ((=) src_cap) src\<rbrace> return () \<lbrace>\<lambda>ya. valid_vs_lookup and valid_table_caps and (\<lambda>s. unique_table_caps (caps_of_state s) \<and> unique_table_refs (caps_of_state s))\<rbrace> proof (prove)
goal (7 subgoals):
 1. \<And>s. \<lbrakk>is_untyped_cap src_cap; valid_vs_lookup s; is_untyped_cap cap; valid_table_caps s; obj_ref_of src_cap = obj_ref_of cap; cap_bits_untyped src_cap = cap_bits_untyped cap; unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s); caps_of_state s src = Some src_cap\<rbrakk> \<Longrightarrow> caps_of_state s src = Some (?b51 s)
 2. \<And>s. \<lbrakk>is_untyped_cap src_cap; valid_vs_lookup s; is_untyped_cap cap; valid_table_caps s; obj_ref_of src_cap = obj_ref_of cap; cap_bits_untyped src_cap = cap_bits_untyped cap; unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s); caps_of_state s src = Some src_cap\<rbrakk> \<Longrightarrow> cap_asid (?b51 s) = cap_asid (max_free_index_update src_cap)
 3. \<And>s. \<lbrakk>is_untyped_cap src_cap; valid_vs_lookup s; is_untyped_cap cap; valid_table_caps s; obj_ref_of src_cap = obj_ref_of cap; cap_bits_untyped src_cap = cap_bits_untyped cap; unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s); caps_of_state s src = Some src_cap\<rbrakk> \<Longrightarrow> obj_refs (?b51 s) = obj_refs (max_free_index_update src_cap)
 4. \<And>s. \<lbrakk>is_untyped_cap src_cap; valid_vs_lookup s; is_untyped_cap cap; valid_table_caps s; obj_ref_of src_cap = obj_ref_of cap; cap_bits_untyped src_cap = cap_bits_untyped cap; unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s); caps_of_state s src = Some src_cap\<rbrakk> \<Longrightarrow> is_pd_cap (?b51 s) = is_pd_cap (max_free_index_update src_cap)
 5. \<And>s. \<lbrakk>is_untyped_cap src_cap; valid_vs_lookup s; is_untyped_cap cap; valid_table_caps s; obj_ref_of src_cap = obj_ref_of cap; cap_bits_untyped src_cap = cap_bits_untyped cap; unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s); caps_of_state s src = Some src_cap\<rbrakk> \<Longrightarrow> is_pt_cap (?b51 s) = is_pt_cap (max_free_index_update src_cap)
 6. \<And>s. \<lbrakk>is_untyped_cap src_cap; valid_vs_lookup s; is_untyped_cap cap; valid_table_caps s; obj_ref_of src_cap = obj_ref_of cap; cap_bits_untyped src_cap = cap_bits_untyped cap; unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s); caps_of_state s src = Some src_cap\<rbrakk> \<Longrightarrow> (is_pt_cap src_cap \<longrightarrow> cap_asid src_cap = None \<longrightarrow> (\<forall>r\<in>obj_refs src_cap. obj_at (empty_table (set (second_level_tables (arch_state s)))) r s)) \<and> (is_pd_cap src_cap \<longrightarrow> cap_asid src_cap = None \<longrightarrow> (\<forall>r\<in>obj_refs src_cap. obj_at (empty_table (set (second_level_tables (arch_state s)))) r s)) \<and> unique_table_caps (caps_of_state s) \<and> unique_table_refs (caps_of_state s)
 7. obj_ref_of src_cap = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap src_cap \<longrightarrow> cap_bits_untyped src_cap \<noteq> cap_bits_untyped cap \<Longrightarrow> \<lbrace>valid_vs_lookup and valid_table_caps and (\<lambda>s. unique_table_caps (caps_of_state s) \<and> unique_table_refs (caps_of_state s)) and cte_wp_at ((=) src_cap) src\<rbrace> return () \<lbrace>\<lambda>ya. valid_vs_lookup and valid_table_caps and (\<lambda>s. unique_table_caps (caps_of_state s) \<and> unique_table_refs (caps_of_state s))\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>is_untyped_cap src_cap; valid_vs_lookup s; is_untyped_cap cap; valid_table_caps s; obj_ref_of src_cap = obj_ref_of cap; cap_bits_untyped src_cap = cap_bits_untyped cap; unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s); caps_of_state s src = Some src_cap\<rbrakk> \<Longrightarrow> (is_pt_cap src_cap \<longrightarrow> cap_asid src_cap = None \<longrightarrow> (\<forall>r\<in>obj_refs src_cap. obj_at (empty_table (set (second_level_tables (arch_state s)))) r s)) \<and> (is_pd_cap src_cap \<longrightarrow> cap_asid src_cap = None \<longrightarrow> (\<forall>r\<in>obj_refs src_cap. obj_at (empty_table (set (second_level_tables (arch_state s)))) r s))
 2. obj_ref_of src_cap = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap src_cap \<longrightarrow> cap_bits_untyped src_cap \<noteq> cap_bits_untyped cap \<Longrightarrow> \<lbrace>valid_vs_lookup and valid_table_caps and (\<lambda>s. unique_table_caps (caps_of_state s) \<and> unique_table_refs (caps_of_state s)) and cte_wp_at ((=) src_cap) src\<rbrace> return () \<lbrace>\<lambda>ya. valid_vs_lookup and valid_table_caps and (\<lambda>s. unique_table_caps (caps_of_state s) \<and> unique_table_refs (caps_of_state s))\<rbrace> proof (prove)
goal (1 subgoal):
 1. obj_ref_of src_cap = obj_ref_of cap \<longrightarrow> (\<exists>dev r bits f. cap = UntypedCap dev r bits f) \<longrightarrow> (\<exists>dev r bits f. src_cap = UntypedCap dev r bits f) \<longrightarrow> cap_bits_untyped src_cap \<noteq> cap_bits_untyped cap \<Longrightarrow> \<lbrace>valid_vs_lookup and valid_table_caps and (\<lambda>s. unique_table_caps (caps_of_state s) \<and> unique_table_refs (caps_of_state s)) and cte_wp_at ((=) src_cap) src\<rbrace> return () \<lbrace>\<lambda>ya. valid_vs_lookup and valid_table_caps and (\<lambda>s. unique_table_caps (caps_of_state s) \<and> unique_table_refs (caps_of_state s))\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>obj_ref_of src_cap = obj_ref_of cap \<longrightarrow> (\<exists>dev r bits f. cap = UntypedCap dev r bits f) \<longrightarrow> (\<exists>dev r bits f. src_cap = UntypedCap dev r bits f) \<longrightarrow> cap_bits_untyped src_cap \<noteq> cap_bits_untyped cap; (valid_vs_lookup and valid_table_caps and (\<lambda>s. unique_table_caps (caps_of_state s) \<and> unique_table_refs (caps_of_state s)) and cte_wp_at ((=) src_cap) src) s\<rbrakk> \<Longrightarrow> (valid_vs_lookup and valid_table_caps and (\<lambda>s. unique_table_caps (caps_of_state s) \<and> unique_table_refs (caps_of_state s))) s proof (prove)
goal:
No subgoals!