theory Finalise_DR

lemma dcorres_store_invalid_pte:
  "dcorres dc \<top> (pt_page_relation (ptr && ~~ mask pt_bits) pg_id ptr UNIV
   and invs )
  (delete_cap_simple (ptr && ~~ mask pt_bits, unat (ptr && mask pt_bits >> 2)))
  (store_pte ptr ARM_A.pte.InvalidPTE)" apply (rule corres_guard_imp) apply (simp add:store_pte_def) apply (rule corres_symb_exec_r) apply (rule dcorres_delete_cap_simple_set_pt[where pg_id = pg_id]) apply (wp|simp)+ apply (clarsimp simp: invs_def valid_mdb_def valid_state_def valid_pspace_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) (pt_page_relation (ptr && ~~ mask pt_bits) pg_id ptr UNIV and invs) (delete_cap_simple (ptr && ~~ mask pt_bits, unat (ptr && mask pt_bits >> 2))) (store_pte ptr InvalidPTE) proof (prove)
goal (3 subgoals):
 1. dcorres dc ?Q ?Q' (delete_cap_simple (ptr && ~~ mask pt_bits, unat (ptr && mask pt_bits >> 2))) (store_pte ptr InvalidPTE)
 2. \<And>s. True \<Longrightarrow> ?Q s
 3. \<And>s. (pt_page_relation (ptr && ~~ mask pt_bits) pg_id ptr UNIV and invs) s \<Longrightarrow> ?Q' s proof (prove)
goal (3 subgoals):
 1. dcorres dc ?Q ?Q' (delete_cap_simple (ptr && ~~ mask pt_bits, unat (ptr && mask pt_bits >> 2))) (do pt <- get_pt (ptr && ~~ mask pt_bits);
set_pt (ptr && ~~ mask pt_bits) (pt(UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2) := InvalidPTE))
od)
 2. \<And>s. True \<Longrightarrow> ?Q s
 3. \<And>s. (pt_page_relation (ptr && ~~ mask pt_bits) pg_id ptr UNIV and invs) s \<Longrightarrow> ?Q' s proof (prove)
goal (6 subgoals):
 1. \<And>rv. dcorres dc ?Q (?Q'4 rv) (delete_cap_simple (ptr && ~~ mask pt_bits, unat (ptr && mask pt_bits >> 2))) (set_pt (ptr && ~~ mask pt_bits) (rv(UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2) := InvalidPTE)))
 2. \<lbrace>?Q'\<rbrace> get_pt (ptr && ~~ mask pt_bits) \<lbrace>?Q'4\<rbrace>
 3. \<And>s. ?Q' s \<Longrightarrow> \<lbrace>(=) s\<rbrace> get_pt (ptr && ~~ mask pt_bits) \<lbrace>\<lambda>r. (=) s\<rbrace>
 4. False \<Longrightarrow> no_fail ?Q' (get_pt (ptr && ~~ mask pt_bits))
 5. \<And>s. True \<Longrightarrow> ?Q s
 6. \<And>s. (pt_page_relation (ptr && ~~ mask pt_bits) pg_id ptr UNIV and invs) s \<Longrightarrow> ?Q' s proof (prove)
goal (5 subgoals):
 1. \<lbrace>?Q'\<rbrace> get_pt (ptr && ~~ mask pt_bits) \<lbrace>\<lambda>rv. (\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s)) and pt_page_relation (ptr && ~~ mask pt_bits) pg_id ptr UNIV and valid_idle and ako_at (arch_kernel_obj.PageTable rv) (ptr && ~~ mask pt_bits)\<rbrace>
 2. \<And>s. ?Q' s \<Longrightarrow> \<lbrace>(=) s\<rbrace> get_pt (ptr && ~~ mask pt_bits) \<lbrace>\<lambda>r. (=) s\<rbrace>
 3. False \<Longrightarrow> no_fail ?Q' (get_pt (ptr && ~~ mask pt_bits))
 4. \<And>s. True \<Longrightarrow> True
 5. \<And>s. (pt_page_relation (ptr && ~~ mask pt_bits) pg_id ptr UNIV and invs) s \<Longrightarrow> ?Q' s proof (prove)
goal (1 subgoal):
 1. \<And>s. pt_page_relation (ptr && ~~ mask pt_bits) pg_id ptr UNIV s \<and> invs s \<Longrightarrow> (\<exists>pt. ako_at (arch_kernel_obj.PageTable pt) (ptr && ~~ mask pt_bits) s) \<longrightarrow> mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s) \<and> valid_idle s proof (prove)
goal:
No subgoals!