theory ArchFinalise_AI

lemma (* replace_cap_invs_arch_update *)[Finalise_AI_asms]:
  "\<lbrace>\<lambda>s. cte_wp_at (replaceable_or_arch_update s p cap) p s
        \<and> invs s
        \<and> cap \<noteq> cap.NullCap
        \<and> ex_cte_cap_wp_to (appropriate_cte_cap cap) p s
        \<and> s \<turnstile> cap\<rbrace>
     set_cap cap p
   \<lbrace>\<lambda>rv s. invs s\<rbrace>" apply (simp add:replaceable_or_arch_update_def) apply (cases "is_pg_cap cap") apply (wp hoare_pre_disj[OF arch_update_cap_invs_unmap_page arch_update_cap_invs_map]) apply (simp add:replaceable_or_arch_update_def replaceable_def cte_wp_at_caps_of_state) apply (clarsimp simp: cte_wp_at_caps_of_state is_cap_simps gen_obj_refs_def
                         cap_master_cap_simps is_arch_update_def) apply (wp replace_cap_invs) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. cte_wp_at (replaceable_or_arch_update s p cap) p s \<and> invs s \<and> cap \<noteq> NullCap \<and> ex_cte_cap_wp_to (appropriate_cte_cap cap) p s \<and> s \<turnstile> cap\<rbrace> set_cap cap p \<lbrace>\<lambda>rv. invs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. cte_wp_at (\<lambda>cap'. (is_pg_cap cap \<longrightarrow> is_arch_update cap cap' \<and> (\<forall>vref. vs_cap_ref cap' = Some vref \<longrightarrow> vs_cap_ref cap = Some vref \<and> obj_refs cap = obj_refs cap' \<or> (\<forall>oref\<in>obj_refs cap'. (vref, oref) \<notin> vs_lookup_pages s))) \<and> (\<not> is_pg_cap cap \<longrightarrow> replaceable s p cap cap')) p s \<and> invs s \<and> cap \<noteq> NullCap \<and> ex_cte_cap_wp_to (appropriate_cte_cap cap) p s \<and> s \<turnstile> cap\<rbrace> set_cap cap p \<lbrace>\<lambda>rv. invs\<rbrace> proof (prove)
goal (2 subgoals):
 1. is_pg_cap cap \<Longrightarrow> \<lbrace>\<lambda>s. cte_wp_at (\<lambda>cap'. (is_pg_cap cap \<longrightarrow> is_arch_update cap cap' \<and> (\<forall>vref. vs_cap_ref cap' = Some vref \<longrightarrow> vs_cap_ref cap = Some vref \<and> obj_refs cap = obj_refs cap' \<or> (\<forall>oref\<in>obj_refs cap'. (vref, oref) \<notin> vs_lookup_pages s))) \<and> (\<not> is_pg_cap cap \<longrightarrow> replaceable s p cap cap')) p s \<and> invs s \<and> cap \<noteq> NullCap \<and> ex_cte_cap_wp_to (appropriate_cte_cap cap) p s \<and> s \<turnstile> cap\<rbrace> set_cap cap p \<lbrace>\<lambda>rv. invs\<rbrace>
 2. \<not> is_pg_cap cap \<Longrightarrow> \<lbrace>\<lambda>s. cte_wp_at (\<lambda>cap'. (is_pg_cap cap \<longrightarrow> is_arch_update cap cap' \<and> (\<forall>vref. vs_cap_ref cap' = Some vref \<longrightarrow> vs_cap_ref cap = Some vref \<and> obj_refs cap = obj_refs cap' \<or> (\<forall>oref\<in>obj_refs cap'. (vref, oref) \<notin> vs_lookup_pages s))) \<and> (\<not> is_pg_cap cap \<longrightarrow> replaceable s p cap cap')) p s \<and> invs s \<and> cap \<noteq> NullCap \<and> ex_cte_cap_wp_to (appropriate_cte_cap cap) p s \<and> s \<turnstile> cap\<rbrace> set_cap cap p \<lbrace>\<lambda>rv. invs\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>is_pg_cap cap; cte_wp_at (\<lambda>cap'. (is_pg_cap cap \<longrightarrow> is_arch_update cap cap' \<and> (\<forall>vref. vs_cap_ref cap' = Some vref \<longrightarrow> vs_cap_ref cap = Some vref \<and> obj_refs cap = obj_refs cap' \<or> (\<forall>oref\<in>obj_refs cap'. (vref, oref) \<notin> vs_lookup_pages s))) \<and> (\<not> is_pg_cap cap \<longrightarrow> replaceable s p cap cap')) p s \<and> invs s \<and> cap \<noteq> NullCap \<and> ex_cte_cap_wp_to (appropriate_cte_cap cap) p s \<and> s \<turnstile> cap\<rbrakk> \<Longrightarrow> ((\<lambda>s. cte_wp_at (\<lambda>c. (\<forall>p'\<in>obj_refs c. \<forall>ref. vs_cap_ref c = Some ref \<longrightarrow> (ref, p') \<notin> vs_lookup_pages s) \<and> is_arch_update cap c) p s) and invs and valid_cap cap and K (is_pg_cap cap) or cte_wp_at (is_arch_update cap and (\<lambda>c. \<forall>r. vs_cap_ref c = Some r \<longrightarrow> vs_cap_ref cap = Some r)) p and invs and valid_cap cap) s
 2. \<not> is_pg_cap cap \<Longrightarrow> \<lbrace>\<lambda>s. cte_wp_at (\<lambda>cap'. (is_pg_cap cap \<longrightarrow> is_arch_update cap cap' \<and> (\<forall>vref. vs_cap_ref cap' = Some vref \<longrightarrow> vs_cap_ref cap = Some vref \<and> obj_refs cap = obj_refs cap' \<or> (\<forall>oref\<in>obj_refs cap'. (vref, oref) \<notin> vs_lookup_pages s))) \<and> (\<not> is_pg_cap cap \<longrightarrow> replaceable s p cap cap')) p s \<and> invs s \<and> cap \<noteq> NullCap \<and> ex_cte_cap_wp_to (appropriate_cte_cap cap) p s \<and> s \<turnstile> cap\<rbrace> set_cap cap p \<lbrace>\<lambda>rv. invs\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>is_pg_cap cap; (\<exists>capa. caps_of_state s p = Some capa \<and> is_arch_update cap capa \<and> (\<forall>vref. vs_cap_ref capa = Some vref \<longrightarrow> vs_cap_ref cap = Some vref \<and> obj_refs cap = obj_refs capa \<or> (\<forall>oref\<in>obj_refs capa. (vref, oref) \<notin> vs_lookup_pages s))) \<and> invs s \<and> cap \<noteq> NullCap \<and> ex_cte_cap_wp_to (appropriate_cte_cap cap) p s \<and> s \<turnstile> cap\<rbrakk> \<Longrightarrow> (\<exists>capa. caps_of_state s p = Some capa \<and> (\<forall>p'\<in>obj_refs capa. \<forall>ref. vs_cap_ref capa = Some ref \<longrightarrow> (ref, p') \<notin> vs_lookup_pages s) \<and> is_arch_update cap capa) \<or> (\<exists>capa. caps_of_state s p = Some capa \<and> is_arch_update cap capa \<and> (\<forall>r. vs_cap_ref capa = Some r \<longrightarrow> vs_cap_ref cap = Some r))
 2. \<not> is_pg_cap cap \<Longrightarrow> \<lbrace>\<lambda>s. cte_wp_at (\<lambda>cap'. (is_pg_cap cap \<longrightarrow> is_arch_update cap cap' \<and> (\<forall>vref. vs_cap_ref cap' = Some vref \<longrightarrow> vs_cap_ref cap = Some vref \<and> obj_refs cap = obj_refs cap' \<or> (\<forall>oref\<in>obj_refs cap'. (vref, oref) \<notin> vs_lookup_pages s))) \<and> (\<not> is_pg_cap cap \<longrightarrow> replaceable s p cap cap')) p s \<and> invs s \<and> cap \<noteq> NullCap \<and> ex_cte_cap_wp_to (appropriate_cte_cap cap) p s \<and> s \<turnstile> cap\<rbrace> set_cap cap p \<lbrace>\<lambda>rv. invs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<not> is_pg_cap cap \<Longrightarrow> \<lbrace>\<lambda>s. cte_wp_at (\<lambda>cap'. (is_pg_cap cap \<longrightarrow> is_arch_update cap cap' \<and> (\<forall>vref. vs_cap_ref cap' = Some vref \<longrightarrow> vs_cap_ref cap = Some vref \<and> obj_refs cap = obj_refs cap' \<or> (\<forall>oref\<in>obj_refs cap'. (vref, oref) \<notin> vs_lookup_pages s))) \<and> (\<not> is_pg_cap cap \<longrightarrow> replaceable s p cap cap')) p s \<and> invs s \<and> cap \<noteq> NullCap \<and> ex_cte_cap_wp_to (appropriate_cte_cap cap) p s \<and> s \<turnstile> cap\<rbrace> set_cap cap p \<lbrace>\<lambda>rv. invs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>\<not> is_pg_cap cap; cte_wp_at (\<lambda>cap'. (is_pg_cap cap \<longrightarrow> is_arch_update cap cap' \<and> (\<forall>vref. vs_cap_ref cap' = Some vref \<longrightarrow> vs_cap_ref cap = Some vref \<and> obj_refs cap = obj_refs cap' \<or> (\<forall>oref\<in>obj_refs cap'. (vref, oref) \<notin> vs_lookup_pages s))) \<and> (\<not> is_pg_cap cap \<longrightarrow> replaceable s p cap cap')) p s \<and> invs s \<and> cap \<noteq> NullCap \<and> ex_cte_cap_wp_to (appropriate_cte_cap cap) p s \<and> s \<turnstile> cap\<rbrakk> \<Longrightarrow> invs s \<and> cte_wp_at (replaceable s p cap) p s \<and> cap \<noteq> NullCap \<and> ex_cte_cap_wp_to (appropriate_cte_cap cap) p s \<and> s \<turnstile> cap proof (prove)
goal:
No subgoals!