theory Finalise_DR

lemma dcorres_unmap_page_table_store_pde:
  "dcorres dc \<top> ((\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s))
    and valid_idle and K (is_aligned pd 14 \<and> vptr < kernel_base)
    and pd_pt_relation (lookup_pd_slot pd vptr && ~~ mask pd_bits) pt_id (lookup_pd_slot pd vptr) )
           (delete_cap_simple (cdl_lookup_pd_slot pd vptr))
           (store_pde (lookup_pd_slot pd vptr) ARM_A.pde.InvalidPDE)" apply (rule corres_guard_imp) apply (rule corres_gen_asm2) apply (subst dcorres_lookup_pd_slot,assumption) apply (simp add:store_pde_def) apply (rule corres_symb_exec_r) apply (simp add:transform_pd_slot_ref_def) apply (rule corres_gen_asm2) apply (rule dcorres_delete_cap_simple_set_pde[where oid = pt_id]) apply assumption apply (wp|simp)+ apply (rule impI) apply (rule less_kernel_base_mapping_slots) apply (simp add: pd_bits_def pageBits_def)+ done

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