theory Finalise_DR

lemma dcorres_delete_cap_simple_section:
  "dcorres dc \<top> (invs and pd_section_relation (lookup_pd_slot pd v && ~~ mask pd_bits) oid
                    (lookup_pd_slot pd v) and  K (is_aligned pd pd_bits \<and> v < kernel_base))
           (delete_cap_simple (cdl_lookup_pd_slot pd v))
           (store_pde (lookup_pd_slot pd v) ARM_A.pde.InvalidPDE)" apply (clarsimp simp: store_pde_def transform_pd_slot_ref_def lookup_pd_slot_def) apply (rule corres_gen_asm2) apply (subst dcorres_lookup_pd_slot, simp add: pd_bits_def pageBits_def) apply (clarsimp simp: transform_pd_slot_ref_def lookup_pd_slot_def) apply (rule corres_guard_imp) apply (rule corres_symb_exec_r) apply (rule dcorres_delete_cap_simple_set_pde[where oid = oid]) apply (drule(1) less_kernel_base_mapping_slots) apply (simp add: lookup_pd_slot_def) apply wpsimp+ apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) (invs and pd_section_relation (lookup_pd_slot pd v && ~~ mask pd_bits) oid (lookup_pd_slot pd v) and K (is_aligned pd pd_bits \<and> v < kernel_base)) (delete_cap_simple (cdl_lookup_pd_slot pd v)) (store_pde (lookup_pd_slot pd v) InvalidPDE) proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) (invs and pd_section_relation (pd + (v >> 20 << 2) && ~~ mask pd_bits) oid (pd + (v >> 20 << 2)) and (\<lambda>y. is_aligned pd pd_bits \<and> v < kernel_base)) (delete_cap_simple (cdl_lookup_pd_slot pd v)) (do pda <- get_pd (pd + (v >> 20 << 2) && ~~ mask pd_bits);
set_pd (pd + (v >> 20 << 2) && ~~ mask pd_bits) (pda(UCAST(32 \<rightarrow> 12) (pd + (v >> 20 << 2) && mask pd_bits >> 2) := InvalidPDE))
od) proof (prove)
goal (1 subgoal):
 1. is_aligned pd pd_bits \<and> v < kernel_base \<Longrightarrow> dcorres dc (\<lambda>_. True) (invs and pd_section_relation (pd + (v >> 20 << 2) && ~~ mask pd_bits) oid (pd + (v >> 20 << 2))) (delete_cap_simple (cdl_lookup_pd_slot pd v)) (do pda <- get_pd (pd + (v >> 20 << 2) && ~~ mask pd_bits);
set_pd (pd + (v >> 20 << 2) && ~~ mask pd_bits) (pda(UCAST(32 \<rightarrow> 12) (pd + (v >> 20 << 2) && mask pd_bits >> 2) := InvalidPDE))
od) proof (prove)
goal (1 subgoal):
 1. is_aligned pd pd_bits \<and> v < kernel_base \<Longrightarrow> dcorres dc (\<lambda>_. True) (invs and pd_section_relation (pd + (v >> 20 << 2) && ~~ mask pd_bits) oid (pd + (v >> 20 << 2))) (delete_cap_simple (transform_pd_slot_ref (lookup_pd_slot pd v))) (do pda <- get_pd (pd + (v >> 20 << 2) && ~~ mask pd_bits);
set_pd (pd + (v >> 20 << 2) && ~~ mask pd_bits) (pda(UCAST(32 \<rightarrow> 12) (pd + (v >> 20 << 2) && mask pd_bits >> 2) := InvalidPDE))
od) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned pd pd_bits; v < kernel_base\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) (invs and pd_section_relation (pd + (v >> 20 << 2) && ~~ mask pd_bits) oid (pd + (v >> 20 << 2))) (delete_cap_simple (pd + (v >> 20 << 2) && ~~ mask pd_bits, unat (pd + (v >> 20 << 2) && mask pd_bits >> 2))) (do pda <- get_pd (pd + (v >> 20 << 2) && ~~ mask pd_bits);
set_pd (pd + (v >> 20 << 2) && ~~ mask pd_bits) (pda(UCAST(32 \<rightarrow> 12) (pd + (v >> 20 << 2) && mask pd_bits >> 2) := InvalidPDE))
od) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>is_aligned pd pd_bits; v < kernel_base\<rbrakk> \<Longrightarrow> dcorres dc ?Q3 ?Q'3 (delete_cap_simple (pd + (v >> 20 << 2) && ~~ mask pd_bits, unat (pd + (v >> 20 << 2) && mask pd_bits >> 2))) (do pda <- get_pd (pd + (v >> 20 << 2) && ~~ mask pd_bits);
set_pd (pd + (v >> 20 << 2) && ~~ mask pd_bits) (pda(UCAST(32 \<rightarrow> 12) (pd + (v >> 20 << 2) && mask pd_bits >> 2) := InvalidPDE))
od)
 2. \<And>s. \<lbrakk>is_aligned pd pd_bits; v < kernel_base; True\<rbrakk> \<Longrightarrow> ?Q3 s
 3. \<And>s. \<lbrakk>is_aligned pd pd_bits; v < kernel_base; (invs and pd_section_relation (pd + (v >> 20 << 2) && ~~ mask pd_bits) oid (pd + (v >> 20 << 2))) s\<rbrakk> \<Longrightarrow> ?Q'3 s proof (prove)
goal (6 subgoals):
 1. \<And>pda. \<lbrakk>is_aligned pd pd_bits; v < kernel_base\<rbrakk> \<Longrightarrow> dcorres dc ?Q3 (?Q'7 pda) (delete_cap_simple (pd + (v >> 20 << 2) && ~~ mask pd_bits, unat (pd + (v >> 20 << 2) && mask pd_bits >> 2))) (set_pd (pd + (v >> 20 << 2) && ~~ mask pd_bits) (pda(UCAST(32 \<rightarrow> 12) (pd + (v >> 20 << 2) && mask pd_bits >> 2) := InvalidPDE)))
 2. \<lbrakk>is_aligned pd pd_bits; v < kernel_base\<rbrakk> \<Longrightarrow> \<lbrace>?Q'3\<rbrace> get_pd (pd + (v >> 20 << 2) && ~~ mask pd_bits) \<lbrace>?Q'7\<rbrace>
 3. \<And>s. \<lbrakk>is_aligned pd pd_bits; v < kernel_base; ?Q'3 s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> get_pd (pd + (v >> 20 << 2) && ~~ mask pd_bits) \<lbrace>\<lambda>r. (=) s\<rbrace>
 4. \<lbrakk>is_aligned pd pd_bits; v < kernel_base; False\<rbrakk> \<Longrightarrow> no_fail ?Q'3 (get_pd (pd + (v >> 20 << 2) && ~~ mask pd_bits))
 5. \<And>s. \<lbrakk>is_aligned pd pd_bits; v < kernel_base; True\<rbrakk> \<Longrightarrow> ?Q3 s
 6. \<And>s. \<lbrakk>is_aligned pd pd_bits; v < kernel_base; (invs and pd_section_relation (pd + (v >> 20 << 2) && ~~ mask pd_bits) oid (pd + (v >> 20 << 2))) s\<rbrakk> \<Longrightarrow> ?Q'3 s proof (prove)
goal (6 subgoals):
 1. \<And>pda. \<lbrakk>is_aligned pd pd_bits; v < kernel_base\<rbrakk> \<Longrightarrow> UCAST(32 \<rightarrow> 12) (pd + (v >> 20 << 2) && mask pd_bits >> 2) \<notin> kernel_mapping_slots
 2. \<lbrakk>is_aligned pd pd_bits; v < kernel_base\<rbrakk> \<Longrightarrow> \<lbrace>?Q'3\<rbrace> get_pd (pd + (v >> 20 << 2) && ~~ mask pd_bits) \<lbrace>\<lambda>pda. (\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s)) and (pd_pt_relation (pd + (v >> 20 << 2) && ~~ mask pd_bits) oid (pd + (v >> 20 << 2)) or pd_section_relation (pd + (v >> 20 << 2) && ~~ mask pd_bits) oid (pd + (v >> 20 << 2)) or pd_super_section_relation (pd + (v >> 20 << 2) && ~~ mask pd_bits) oid (pd + (v >> 20 << 2))) and valid_idle and ako_at (arch_kernel_obj.PageDirectory pda) (pd + (v >> 20 << 2) && ~~ mask pd_bits)\<rbrace>
 3. \<And>s. \<lbrakk>is_aligned pd pd_bits; v < kernel_base; ?Q'3 s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> get_pd (pd + (v >> 20 << 2) && ~~ mask pd_bits) \<lbrace>\<lambda>r. (=) s\<rbrace>
 4. \<lbrakk>is_aligned pd pd_bits; v < kernel_base; False\<rbrakk> \<Longrightarrow> no_fail ?Q'3 (get_pd (pd + (v >> 20 << 2) && ~~ mask pd_bits))
 5. \<And>s. \<lbrakk>is_aligned pd pd_bits; v < kernel_base; True\<rbrakk> \<Longrightarrow> True
 6. \<And>s. \<lbrakk>is_aligned pd pd_bits; v < kernel_base; (invs and pd_section_relation (pd + (v >> 20 << 2) && ~~ mask pd_bits) oid (pd + (v >> 20 << 2))) s\<rbrakk> \<Longrightarrow> ?Q'3 s proof (prove)
goal (6 subgoals):
 1. \<And>pda. \<lbrakk>is_aligned pd pd_bits; UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd v && mask pd_bits >> 2) \<notin> kernel_mapping_slots\<rbrakk> \<Longrightarrow> UCAST(32 \<rightarrow> 12) (pd + (v >> 20 << 2) && mask pd_bits >> 2) \<notin> kernel_mapping_slots
 2. \<lbrakk>is_aligned pd pd_bits; v < kernel_base\<rbrakk> \<Longrightarrow> \<lbrace>?Q'3\<rbrace> get_pd (pd + (v >> 20 << 2) && ~~ mask pd_bits) \<lbrace>\<lambda>pda. (\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s)) and (pd_pt_relation (pd + (v >> 20 << 2) && ~~ mask pd_bits) oid (pd + (v >> 20 << 2)) or pd_section_relation (pd + (v >> 20 << 2) && ~~ mask pd_bits) oid (pd + (v >> 20 << 2)) or pd_super_section_relation (pd + (v >> 20 << 2) && ~~ mask pd_bits) oid (pd + (v >> 20 << 2))) and valid_idle and ako_at (arch_kernel_obj.PageDirectory pda) (pd + (v >> 20 << 2) && ~~ mask pd_bits)\<rbrace>
 3. \<And>s. \<lbrakk>is_aligned pd pd_bits; v < kernel_base; ?Q'3 s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> get_pd (pd + (v >> 20 << 2) && ~~ mask pd_bits) \<lbrace>\<lambda>r. (=) s\<rbrace>
 4. \<lbrakk>is_aligned pd pd_bits; v < kernel_base; False\<rbrakk> \<Longrightarrow> no_fail ?Q'3 (get_pd (pd + (v >> 20 << 2) && ~~ mask pd_bits))
 5. \<And>s. \<lbrakk>is_aligned pd pd_bits; v < kernel_base; True\<rbrakk> \<Longrightarrow> True
 6. \<And>s. \<lbrakk>is_aligned pd pd_bits; v < kernel_base; (invs and pd_section_relation (pd + (v >> 20 << 2) && ~~ mask pd_bits) oid (pd + (v >> 20 << 2))) s\<rbrakk> \<Longrightarrow> ?Q'3 s proof (prove)
goal (5 subgoals):
 1. \<lbrakk>is_aligned pd pd_bits; v < kernel_base\<rbrakk> \<Longrightarrow> \<lbrace>?Q'3\<rbrace> get_pd (pd + (v >> 20 << 2) && ~~ mask pd_bits) \<lbrace>\<lambda>pda. (\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s)) and (pd_pt_relation (pd + (v >> 20 << 2) && ~~ mask pd_bits) oid (pd + (v >> 20 << 2)) or pd_section_relation (pd + (v >> 20 << 2) && ~~ mask pd_bits) oid (pd + (v >> 20 << 2)) or pd_super_section_relation (pd + (v >> 20 << 2) && ~~ mask pd_bits) oid (pd + (v >> 20 << 2))) and valid_idle and ako_at (arch_kernel_obj.PageDirectory pda) (pd + (v >> 20 << 2) && ~~ mask pd_bits)\<rbrace>
 2. \<And>s. \<lbrakk>is_aligned pd pd_bits; v < kernel_base; ?Q'3 s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> get_pd (pd + (v >> 20 << 2) && ~~ mask pd_bits) \<lbrace>\<lambda>r. (=) s\<rbrace>
 3. \<lbrakk>is_aligned pd pd_bits; v < kernel_base; False\<rbrakk> \<Longrightarrow> no_fail ?Q'3 (get_pd (pd + (v >> 20 << 2) && ~~ mask pd_bits))
 4. \<And>s. \<lbrakk>is_aligned pd pd_bits; v < kernel_base; True\<rbrakk> \<Longrightarrow> True
 5. \<And>s. \<lbrakk>is_aligned pd pd_bits; v < kernel_base; (invs and pd_section_relation (pd + (v >> 20 << 2) && ~~ mask pd_bits) oid (pd + (v >> 20 << 2))) s\<rbrakk> \<Longrightarrow> ?Q'3 s proof (prove)
goal (1 subgoal):
 1. \<And>s pda. \<lbrakk>is_aligned pd pd_bits; v < kernel_base; invs s; pd_section_relation (pd + (v >> 20 << 2) && ~~ mask pd_bits) oid (pd + (v >> 20 << 2)) s; ako_at (arch_kernel_obj.PageDirectory pda) (pd + (v >> 20 << 2) && ~~ mask pd_bits) s\<rbrakk> \<Longrightarrow> mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s) \<and> valid_idle s proof (prove)
goal:
No subgoals!