theory Finalise_DR

lemma dcorres_store_invalid_pde_super_section:
  "dcorres dc \<top> (pd_super_section_relation (ptr && ~~ mask pd_bits) pg_id ptr
   and invs
   and K (ucast (ptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots))
  (delete_cap_simple (ptr && ~~ mask pd_bits, unat (ptr && mask pd_bits >> 2)))
  (store_pde ptr ARM_A.pde.InvalidPDE)" apply simp apply (rule corres_gen_asm2) apply (rule corres_guard_imp) apply (simp add:store_pde_def) apply (rule corres_symb_exec_r) apply (rule dcorres_delete_cap_simple_set_pde[where oid = pg_id]) apply simp 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) (pd_super_section_relation (ptr && ~~ mask pd_bits) pg_id ptr and invs and K (UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots)) (delete_cap_simple (ptr && ~~ mask pd_bits, unat (ptr && mask pd_bits >> 2))) (store_pde ptr InvalidPDE) proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) (pd_super_section_relation (ptr && ~~ mask pd_bits) pg_id ptr and invs and (\<lambda>y. UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots)) (delete_cap_simple (ptr && ~~ mask pd_bits, unat (ptr && mask pd_bits >> 2))) (store_pde ptr InvalidPDE) proof (prove)
goal (1 subgoal):
 1. UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots \<Longrightarrow> dcorres dc (\<lambda>_. True) (pd_super_section_relation (ptr && ~~ mask pd_bits) pg_id ptr and invs) (delete_cap_simple (ptr && ~~ mask pd_bits, unat (ptr && mask pd_bits >> 2))) (store_pde ptr InvalidPDE) proof (prove)
goal (3 subgoals):
 1. UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots \<Longrightarrow> dcorres dc ?Q2 ?Q'2 (delete_cap_simple (ptr && ~~ mask pd_bits, unat (ptr && mask pd_bits >> 2))) (store_pde ptr InvalidPDE)
 2. \<And>s. \<lbrakk>UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots; True\<rbrakk> \<Longrightarrow> ?Q2 s
 3. \<And>s. \<lbrakk>UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots; (pd_super_section_relation (ptr && ~~ mask pd_bits) pg_id ptr and invs) s\<rbrakk> \<Longrightarrow> ?Q'2 s proof (prove)
goal (3 subgoals):
 1. UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots \<Longrightarrow> dcorres dc ?Q2 ?Q'2 (delete_cap_simple (ptr && ~~ mask pd_bits, unat (ptr && mask pd_bits >> 2))) (do pd <- get_pd (ptr && ~~ mask pd_bits);
set_pd (ptr && ~~ mask pd_bits) (pd(UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) := InvalidPDE))
od)
 2. \<And>s. \<lbrakk>UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots; True\<rbrakk> \<Longrightarrow> ?Q2 s
 3. \<And>s. \<lbrakk>UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots; (pd_super_section_relation (ptr && ~~ mask pd_bits) pg_id ptr and invs) s\<rbrakk> \<Longrightarrow> ?Q'2 s proof (prove)
goal (6 subgoals):
 1. \<And>rv. UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots \<Longrightarrow> dcorres dc ?Q2 (?Q'6 rv) (delete_cap_simple (ptr && ~~ mask pd_bits, unat (ptr && mask pd_bits >> 2))) (set_pd (ptr && ~~ mask pd_bits) (rv(UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) := InvalidPDE)))
 2. UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots \<Longrightarrow> \<lbrace>?Q'2\<rbrace> get_pd (ptr && ~~ mask pd_bits) \<lbrace>?Q'6\<rbrace>
 3. \<And>s. \<lbrakk>UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots; ?Q'2 s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> get_pd (ptr && ~~ mask pd_bits) \<lbrace>\<lambda>r. (=) s\<rbrace>
 4. \<lbrakk>UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots; False\<rbrakk> \<Longrightarrow> no_fail ?Q'2 (get_pd (ptr && ~~ mask pd_bits))
 5. \<And>s. \<lbrakk>UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots; True\<rbrakk> \<Longrightarrow> ?Q2 s
 6. \<And>s. \<lbrakk>UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots; (pd_super_section_relation (ptr && ~~ mask pd_bits) pg_id ptr and invs) s\<rbrakk> \<Longrightarrow> ?Q'2 s proof (prove)
goal (6 subgoals):
 1. \<And>rv. UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots \<Longrightarrow> UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots
 2. UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots \<Longrightarrow> \<lbrace>?Q'2\<rbrace> get_pd (ptr && ~~ mask pd_bits) \<lbrace>\<lambda>rv. (\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s)) and (pd_pt_relation (ptr && ~~ mask pd_bits) pg_id ptr or pd_section_relation (ptr && ~~ mask pd_bits) pg_id ptr or pd_super_section_relation (ptr && ~~ mask pd_bits) pg_id ptr) and valid_idle and ako_at (arch_kernel_obj.PageDirectory rv) (ptr && ~~ mask pd_bits)\<rbrace>
 3. \<And>s. \<lbrakk>UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots; ?Q'2 s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> get_pd (ptr && ~~ mask pd_bits) \<lbrace>\<lambda>r. (=) s\<rbrace>
 4. \<lbrakk>UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots; False\<rbrakk> \<Longrightarrow> no_fail ?Q'2 (get_pd (ptr && ~~ mask pd_bits))
 5. \<And>s. \<lbrakk>UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots; True\<rbrakk> \<Longrightarrow> True
 6. \<And>s. \<lbrakk>UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots; (pd_super_section_relation (ptr && ~~ mask pd_bits) pg_id ptr and invs) s\<rbrakk> \<Longrightarrow> ?Q'2 s proof (prove)
goal (5 subgoals):
 1. UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots \<Longrightarrow> \<lbrace>?Q'2\<rbrace> get_pd (ptr && ~~ mask pd_bits) \<lbrace>\<lambda>rv. (\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s)) and (pd_pt_relation (ptr && ~~ mask pd_bits) pg_id ptr or pd_section_relation (ptr && ~~ mask pd_bits) pg_id ptr or pd_super_section_relation (ptr && ~~ mask pd_bits) pg_id ptr) and valid_idle and ako_at (arch_kernel_obj.PageDirectory rv) (ptr && ~~ mask pd_bits)\<rbrace>
 2. \<And>s. \<lbrakk>UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots; ?Q'2 s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> get_pd (ptr && ~~ mask pd_bits) \<lbrace>\<lambda>r. (=) s\<rbrace>
 3. \<lbrakk>UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots; False\<rbrakk> \<Longrightarrow> no_fail ?Q'2 (get_pd (ptr && ~~ mask pd_bits))
 4. \<And>s. \<lbrakk>UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots; True\<rbrakk> \<Longrightarrow> True
 5. \<And>s. \<lbrakk>UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots; (pd_super_section_relation (ptr && ~~ mask pd_bits) pg_id ptr and invs) s\<rbrakk> \<Longrightarrow> ?Q'2 s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots; pd_super_section_relation (ptr && ~~ mask pd_bits) pg_id ptr s \<and> invs s\<rbrakk> \<Longrightarrow> (\<exists>pd. ako_at (arch_kernel_obj.PageDirectory pd) (ptr && ~~ mask pd_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!