theory ArchVSpace_AI

lemma mdb_cte_at_store_pte[wp]:
  "\<lbrace>\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s)\<rbrace>
   store_pte y pte
   \<lbrace>\<lambda>r s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s)\<rbrace>" apply (clarsimp simp:mdb_cte_at_def) apply (simp only: imp_conv_disj) apply (wp hoare_vcg_disj_lift hoare_vcg_all_lift) apply (simp add:store_pte_def set_pt_def) apply wp apply (wp|simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s)\<rbrace> store_pte y pte \<lbrace>\<lambda>r s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<forall>a b aa ba. cdt s (aa, ba) = Some (a, b) \<longrightarrow> cte_wp_at ((\<noteq>) NullCap) (a, b) s \<and> cte_wp_at ((\<noteq>) NullCap) (aa, ba) s\<rbrace> store_pte y pte \<lbrace>\<lambda>r s. \<forall>a b aa ba. cdt s (aa, ba) = Some (a, b) \<longrightarrow> cte_wp_at ((\<noteq>) NullCap) (a, b) s \<and> cte_wp_at ((\<noteq>) NullCap) (aa, ba) s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<forall>a b aa ba. cdt s (aa, ba) \<noteq> Some (a, b) \<or> cte_wp_at ((\<noteq>) NullCap) (a, b) s \<and> cte_wp_at ((\<noteq>) NullCap) (aa, ba) s\<rbrace> store_pte y pte \<lbrace>\<lambda>r s. \<forall>a b aa ba. cdt s (aa, ba) \<noteq> Some (a, b) \<or> cte_wp_at ((\<noteq>) NullCap) (a, b) s \<and> cte_wp_at ((\<noteq>) NullCap) (aa, ba) s\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>a b aa ba. \<lbrace>?P8 a b aa ba\<rbrace> store_pte y pte \<lbrace>\<lambda>rv s. cdt s (aa, ba) \<noteq> Some (a, b)\<rbrace>
 2. \<And>a b aa ba. \<lbrace>?P'8 a b aa ba\<rbrace> store_pte y pte \<lbrace>\<lambda>rv s. cte_wp_at ((\<noteq>) NullCap) (a, b) s \<and> cte_wp_at ((\<noteq>) NullCap) (aa, ba) s\<rbrace>
 3. \<And>s. \<forall>a b aa ba. cdt s (aa, ba) \<noteq> Some (a, b) \<or> cte_wp_at ((\<noteq>) NullCap) (a, b) s \<and> cte_wp_at ((\<noteq>) NullCap) (aa, ba) s \<Longrightarrow> \<forall>x xa xb xc. ?P8 x xa xb xc s \<or> ?P'8 x xa xb xc s proof (prove)
goal (3 subgoals):
 1. \<And>a b aa ba. \<lbrace>?P8 a b aa ba\<rbrace> do pt <- get_pt (y && ~~ mask pt_bits);
set_object (y && ~~ mask pt_bits) (ArchObj (PageTable (pt(UCAST(32 \<rightarrow> 8) (y && mask pt_bits >> 2) := pte))))
od \<lbrace>\<lambda>rv s. cdt s (aa, ba) \<noteq> Some (a, b)\<rbrace>
 2. \<And>a b aa ba. \<lbrace>?P'8 a b aa ba\<rbrace> store_pte y pte \<lbrace>\<lambda>rv s. cte_wp_at ((\<noteq>) NullCap) (a, b) s \<and> cte_wp_at ((\<noteq>) NullCap) (aa, ba) s\<rbrace>
 3. \<And>s. \<forall>a b aa ba. cdt s (aa, ba) \<noteq> Some (a, b) \<or> cte_wp_at ((\<noteq>) NullCap) (a, b) s \<and> cte_wp_at ((\<noteq>) NullCap) (aa, ba) s \<Longrightarrow> \<forall>x xa xb xc. ?P8 x xa xb xc s \<or> ?P'8 x xa xb xc s proof (prove)
goal (2 subgoals):
 1. \<And>a b aa ba. \<lbrace>?P'8 a b aa ba\<rbrace> store_pte y pte \<lbrace>\<lambda>rv s. cte_wp_at ((\<noteq>) NullCap) (a, b) s \<and> cte_wp_at ((\<noteq>) NullCap) (aa, ba) s\<rbrace>
 2. \<And>s. \<forall>a b aa ba. cdt s (aa, ba) \<noteq> Some (a, b) \<or> cte_wp_at ((\<noteq>) NullCap) (a, b) s \<and> cte_wp_at ((\<noteq>) NullCap) (aa, ba) s \<Longrightarrow> \<forall>x xa xb xc. (\<forall>pt. ako_at (PageTable pt) (y && ~~ mask pt_bits) s \<longrightarrow> cdt s (xb, xc) \<noteq> Some (x, xa)) \<or> ?P'8 x xa xb xc s proof (prove)
goal:
No subgoals!