theory Finalise_DR

lemma dcorres_delete_cap_simple_set_pt:
  "dcorres dc \<top> ((\<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 ko_at (ArchObj (arch_kernel_obj.PageTable fun)) (ptr && ~~ mask pt_bits))
    (delete_cap_simple (ptr && ~~ mask pt_bits, unat (ptr && mask pt_bits >> 2)))
    (set_pt (ptr && ~~ mask pt_bits) (fun(ucast (ptr && mask pt_bits >> 2) := ARM_A.pte.InvalidPTE)))" apply (simp add: delete_cap_simple_def set_pt_def gets_the_def gets_def bind_assoc get_object_def) apply (rule dcorres_absorb_get_l) apply (clarsimp simp: assert_def corres_free_fail
                 split: Structures_A.kernel_object.split_asm arch_kernel_obj.splits) apply (frule opt_cap_page) apply simp+ apply (clarsimp simp:gets_def assert_opt_def PageTableUnmap_D.is_final_cap_def PageTableUnmap_D.is_final_cap'_def) apply (rule dcorres_absorb_get_l) apply (clarsimp simp: always_empty_slot_def gets_the_def gets_def bind_assoc) apply (rule remove_cdt_pt_slot_exec[where pg_id = pg_id]) apply (rule corres_guard_imp) apply (rule dcorres_set_pte_cap) apply (simp add:transform_pte_def)+ apply clarsimp apply simp 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 pt_page_relation (ptr && ~~ mask pt_bits) pg_id ptr UNIV and valid_idle and ako_at (arch_kernel_obj.PageTable fun) (ptr && ~~ mask pt_bits)) (delete_cap_simple (ptr && ~~ mask pt_bits, unat (ptr && mask pt_bits >> 2))) (set_pt (ptr && ~~ mask pt_bits) (fun(UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2) := InvalidPTE))) 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 pt_page_relation (ptr && ~~ mask pt_bits) pg_id ptr UNIV and valid_idle and ako_at (arch_kernel_obj.PageTable fun) (ptr && ~~ mask pt_bits)) (do x <- get;
cap <- assert_opt (opt_cap (ptr && ~~ mask pt_bits, unat (ptr && mask pt_bits >> 2)) x);
unless (cap = cdl_cap.NullCap) (do final <- PageTableUnmap_D.is_final_cap cap;
y <- PageTableUnmap_D.fast_finalise cap final;
always_empty_slot (ptr && ~~ mask pt_bits, unat (ptr && mask pt_bits >> 2))
od)
od) (KHeap_A.set_object (ptr && ~~ mask pt_bits) (ArchObj (arch_kernel_obj.PageTable (fun(UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2) := InvalidPTE))))) proof (prove)
goal (1 subgoal):
 1. \<And>s'. \<lbrakk>True; ((\<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 fun) (ptr && ~~ mask pt_bits)) s'\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (do cap <- assert_opt (opt_cap (ptr && ~~ mask pt_bits, unat (ptr && mask pt_bits >> 2)) (transform s'));
unless (cap = cdl_cap.NullCap) (do final <- PageTableUnmap_D.is_final_cap cap;
y <- PageTableUnmap_D.fast_finalise cap final;
always_empty_slot (ptr && ~~ mask pt_bits, unat (ptr && mask pt_bits >> 2))
od)
od) (KHeap_A.set_object (ptr && ~~ mask pt_bits) (ArchObj (arch_kernel_obj.PageTable (fun(UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2) := InvalidPTE))))) proof (prove)
goal (1 subgoal):
 1. \<And>s'. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); pt_page_relation (ptr && ~~ mask pt_bits) pg_id ptr UNIV s'; valid_idle s'; ako_at (arch_kernel_obj.PageTable fun) (ptr && ~~ mask pt_bits) s'\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (do cap <- assert_opt (opt_cap (ptr && ~~ mask pt_bits, unat (ptr && mask pt_bits >> 2)) (transform s'));
unless (cap = cdl_cap.NullCap) (do final <- PageTableUnmap_D.is_final_cap cap;
y <- PageTableUnmap_D.fast_finalise cap final;
always_empty_slot (ptr && ~~ mask pt_bits, unat (ptr && mask pt_bits >> 2))
od)
od) (KHeap_A.set_object (ptr && ~~ mask pt_bits) (ArchObj (arch_kernel_obj.PageTable (fun(UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2) := InvalidPTE))))) proof (prove)
goal (2 subgoals):
 1. \<And>s'. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); pt_page_relation (ptr && ~~ mask pt_bits) pg_id ptr UNIV s'; valid_idle s'; ako_at (arch_kernel_obj.PageTable fun) (ptr && ~~ mask pt_bits) s'\<rbrakk> \<Longrightarrow> pt_page_relation (?a5 s') (?pg5 s') (?x5 s') (?S5 s') s'
 2. \<And>s'. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); pt_page_relation (ptr && ~~ mask pt_bits) pg_id ptr UNIV s'; valid_idle s'; ako_at (arch_kernel_obj.PageTable fun) (ptr && ~~ mask pt_bits) s'; \<exists>f sz. opt_cap (?a5 s', unat (?x5 s' && mask pt_bits >> 2)) (transform s') = Some (FrameCap False (?pg5 s') f sz Fake None)\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (do cap <- assert_opt (opt_cap (ptr && ~~ mask pt_bits, unat (ptr && mask pt_bits >> 2)) (transform s'));
unless (cap = cdl_cap.NullCap) (do final <- PageTableUnmap_D.is_final_cap cap;
y <- PageTableUnmap_D.fast_finalise cap final;
always_empty_slot (ptr && ~~ mask pt_bits, unat (ptr && mask pt_bits >> 2))
od)
od) (KHeap_A.set_object (ptr && ~~ mask pt_bits) (ArchObj (arch_kernel_obj.PageTable (fun(UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2) := InvalidPTE))))) proof (prove)
goal (1 subgoal):
 1. \<And>s'. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); pt_page_relation (ptr && ~~ mask pt_bits) pg_id ptr UNIV s'; valid_idle s'; ako_at (arch_kernel_obj.PageTable fun) (ptr && ~~ mask pt_bits) s'; \<exists>f sz. opt_cap (ptr && ~~ mask pt_bits, unat (ptr && mask pt_bits >> 2)) (transform s') = Some (FrameCap False pg_id f sz Fake None)\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (do cap <- assert_opt (opt_cap (ptr && ~~ mask pt_bits, unat (ptr && mask pt_bits >> 2)) (transform s'));
unless (cap = cdl_cap.NullCap) (do final <- PageTableUnmap_D.is_final_cap cap;
y <- PageTableUnmap_D.fast_finalise cap final;
always_empty_slot (ptr && ~~ mask pt_bits, unat (ptr && mask pt_bits >> 2))
od)
od) (KHeap_A.set_object (ptr && ~~ mask pt_bits) (ArchObj (arch_kernel_obj.PageTable (fun(UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2) := InvalidPTE))))) proof (prove)
goal (1 subgoal):
 1. \<And>s' f sz. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); pt_page_relation (ptr && ~~ mask pt_bits) pg_id ptr UNIV s'; valid_idle s'; ako_at (arch_kernel_obj.PageTable fun) (ptr && ~~ mask pt_bits) s'; opt_cap (ptr && ~~ mask pt_bits, unat (ptr && mask pt_bits >> 2)) (transform s') = Some (FrameCap False pg_id f sz Fake None)\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (do s <- get;
always_empty_slot (ptr && ~~ mask pt_bits, unat (ptr && mask pt_bits >> 2))
od) (KHeap_A.set_object (ptr && ~~ mask pt_bits) (ArchObj (arch_kernel_obj.PageTable (fun(UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2) := InvalidPTE))))) proof (prove)
goal (1 subgoal):
 1. \<And>s' f sz s'a. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); pt_page_relation (ptr && ~~ mask pt_bits) pg_id ptr UNIV s'; valid_idle s'; ako_at (arch_kernel_obj.PageTable fun) (ptr && ~~ mask pt_bits) s'; opt_cap (ptr && ~~ mask pt_bits, unat (ptr && mask pt_bits >> 2)) (transform s') = Some (FrameCap False pg_id f sz Fake None); transform s' = transform s'a; s' = s'a\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s'a)) ((=) s'a) (always_empty_slot (ptr && ~~ mask pt_bits, unat (ptr && mask pt_bits >> 2))) (KHeap_A.set_object (ptr && ~~ mask pt_bits) (ArchObj (arch_kernel_obj.PageTable (fun(UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2) := InvalidPTE))))) proof (prove)
goal (1 subgoal):
 1. \<And>f sz s'a. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s'a) (cdt s'a); pt_page_relation (ptr && ~~ mask pt_bits) pg_id ptr UNIV s'a; valid_idle s'a; ako_at (arch_kernel_obj.PageTable fun) (ptr && ~~ mask pt_bits) s'a; opt_cap (ptr && ~~ mask pt_bits, unat (ptr && mask pt_bits >> 2)) (transform s'a) = Some (FrameCap False pg_id f sz Fake None)\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s'a)) ((=) s'a) (do y <- remove_parent (ptr && ~~ mask pt_bits, unat (ptr && mask pt_bits >> 2));
KHeap_D.set_cap (ptr && ~~ mask pt_bits, unat (ptr && mask pt_bits >> 2)) cdl_cap.NullCap
od) (KHeap_A.set_object (ptr && ~~ mask pt_bits) (ArchObj (arch_kernel_obj.PageTable (fun(UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2) := InvalidPTE))))) proof (prove)
goal (2 subgoals):
 1. \<And>f sz s'a. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s'a) (cdt s'a); pt_page_relation (ptr && ~~ mask pt_bits) pg_id ptr UNIV s'a; valid_idle s'a; ako_at (arch_kernel_obj.PageTable fun) (ptr && ~~ mask pt_bits) s'a; opt_cap (ptr && ~~ mask pt_bits, unat (ptr && mask pt_bits >> 2)) (transform s'a) = Some (FrameCap False pg_id f sz Fake None)\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) ((=) s'a) (KHeap_D.set_cap (ptr && ~~ mask pt_bits, unat (ptr && mask pt_bits >> 2)) cdl_cap.NullCap) (KHeap_A.set_object (ptr && ~~ mask pt_bits) (ArchObj (arch_kernel_obj.PageTable (fun(UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2) := InvalidPTE)))))
 2. \<And>f sz s'a s. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s'a) (cdt s'a); pt_page_relation (ptr && ~~ mask pt_bits) pg_id ptr UNIV s'a; valid_idle s'a; ako_at (arch_kernel_obj.PageTable fun) (ptr && ~~ mask pt_bits) s'a; opt_cap (ptr && ~~ mask pt_bits, unat (ptr && mask pt_bits >> 2)) (transform s'a) = Some (FrameCap False pg_id f sz Fake None)\<rbrakk> \<Longrightarrow> s'a = s \<longrightarrow> ((\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s)) and valid_idle and pt_page_relation (ptr && ~~ mask pt_bits) pg_id (?ptr13 f sz s'a) UNIV) s proof (prove)
goal (4 subgoals):
 1. \<And>f sz s'a. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s'a) (cdt s'a); pt_page_relation (ptr && ~~ mask pt_bits) pg_id ptr UNIV s'a; valid_idle s'a; ako_at (arch_kernel_obj.PageTable fun) (ptr && ~~ mask pt_bits) s'a; opt_cap (ptr && ~~ mask pt_bits, unat (ptr && mask pt_bits >> 2)) (transform s'a) = Some (FrameCap False pg_id f sz Fake None)\<rbrakk> \<Longrightarrow> dcorres dc (?Q16 f sz s'a) (?Q'16 f sz s'a) (KHeap_D.set_cap (ptr && ~~ mask pt_bits, unat (ptr && mask pt_bits >> 2)) cdl_cap.NullCap) (KHeap_A.set_object (ptr && ~~ mask pt_bits) (ArchObj (arch_kernel_obj.PageTable (fun(UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2) := InvalidPTE)))))
 2. \<And>f sz s'a s. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s'a) (cdt s'a); pt_page_relation (ptr && ~~ mask pt_bits) pg_id ptr UNIV s'a; valid_idle s'a; ako_at (arch_kernel_obj.PageTable fun) (ptr && ~~ mask pt_bits) s'a; opt_cap (ptr && ~~ mask pt_bits, unat (ptr && mask pt_bits >> 2)) (transform s'a) = Some (FrameCap False pg_id f sz Fake None); True\<rbrakk> \<Longrightarrow> ?Q16 f sz s'a s
 3. \<And>f sz s'a s. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s'a) (cdt s'a); pt_page_relation (ptr && ~~ mask pt_bits) pg_id ptr UNIV s'a; valid_idle s'a; ako_at (arch_kernel_obj.PageTable fun) (ptr && ~~ mask pt_bits) s'a; opt_cap (ptr && ~~ mask pt_bits, unat (ptr && mask pt_bits >> 2)) (transform s'a) = Some (FrameCap False pg_id f sz Fake None); s'a = s\<rbrakk> \<Longrightarrow> ?Q'16 f sz s'a s
 4. \<And>f sz s'a s. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s'a) (cdt s'a); pt_page_relation (ptr && ~~ mask pt_bits) pg_id ptr UNIV s'a; valid_idle s'a; ako_at (arch_kernel_obj.PageTable fun) (ptr && ~~ mask pt_bits) s'a; opt_cap (ptr && ~~ mask pt_bits, unat (ptr && mask pt_bits >> 2)) (transform s'a) = Some (FrameCap False pg_id f sz Fake None)\<rbrakk> \<Longrightarrow> s'a = s \<longrightarrow> ((\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s)) and valid_idle and pt_page_relation (ptr && ~~ mask pt_bits) pg_id (?ptr13 f sz s'a) UNIV) s proof (prove)
goal (5 subgoals):
 1. \<And>f sz s'a. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s'a) (cdt s'a); pt_page_relation (ptr && ~~ mask pt_bits) pg_id ptr UNIV s'a; valid_idle s'a; ako_at (arch_kernel_obj.PageTable fun) (ptr && ~~ mask pt_bits) s'a; opt_cap (ptr && ~~ mask pt_bits, unat (ptr && mask pt_bits >> 2)) (transform s'a) = Some (FrameCap False pg_id f sz Fake None)\<rbrakk> \<Longrightarrow> ?x20 f sz s'a = ptr && mask pt_bits >> 2
 2. \<And>f sz s'a. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s'a) (cdt s'a); pt_page_relation (ptr && ~~ mask pt_bits) pg_id ptr UNIV s'a; valid_idle s'a; ako_at (arch_kernel_obj.PageTable fun) (ptr && ~~ mask pt_bits) s'a; opt_cap (ptr && ~~ mask pt_bits, unat (ptr && mask pt_bits >> 2)) (transform s'a) = Some (FrameCap False pg_id f sz Fake None)\<rbrakk> \<Longrightarrow> cdl_cap.NullCap = transform_pte InvalidPTE
 3. \<And>f sz s'a s. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s'a) (cdt s'a); pt_page_relation (ptr && ~~ mask pt_bits) pg_id ptr UNIV s'a; valid_idle s'a; ako_at (arch_kernel_obj.PageTable fun) (ptr && ~~ mask pt_bits) s'a; opt_cap (ptr && ~~ mask pt_bits, unat (ptr && mask pt_bits >> 2)) (transform s'a) = Some (FrameCap False pg_id f sz Fake None); True\<rbrakk> \<Longrightarrow> True
 4. \<And>f sz s'a s. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s'a) (cdt s'a); pt_page_relation (ptr && ~~ mask pt_bits) pg_id ptr UNIV s'a; valid_idle s'a; ako_at (arch_kernel_obj.PageTable fun) (ptr && ~~ mask pt_bits) s'a; opt_cap (ptr && ~~ mask pt_bits, unat (ptr && mask pt_bits >> 2)) (transform s'a) = Some (FrameCap False pg_id f sz Fake None); s'a = s\<rbrakk> \<Longrightarrow> (valid_idle and ako_at (arch_kernel_obj.PageTable fun) (ptr && ~~ mask pt_bits)) s
 5. \<And>f sz s'a s. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s'a) (cdt s'a); pt_page_relation (ptr && ~~ mask pt_bits) pg_id ptr UNIV s'a; valid_idle s'a; ako_at (arch_kernel_obj.PageTable fun) (ptr && ~~ mask pt_bits) s'a; opt_cap (ptr && ~~ mask pt_bits, unat (ptr && mask pt_bits >> 2)) (transform s'a) = Some (FrameCap False pg_id f sz Fake None)\<rbrakk> \<Longrightarrow> s'a = s \<longrightarrow> ((\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s)) and valid_idle and pt_page_relation (ptr && ~~ mask pt_bits) pg_id (?ptr13 f sz s'a) UNIV) s proof (prove)
goal (1 subgoal):
 1. \<And>f sz s'a s. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s'a) (cdt s'a); pt_page_relation (ptr && ~~ mask pt_bits) pg_id ptr UNIV s'a; valid_idle s'a; ako_at (arch_kernel_obj.PageTable fun) (ptr && ~~ mask pt_bits) s'a; opt_cap (ptr && ~~ mask pt_bits, unat (ptr && mask pt_bits >> 2)) (transform s'a) = Some (FrameCap False pg_id f sz Fake None)\<rbrakk> \<Longrightarrow> s'a = s \<longrightarrow> mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s) \<and> valid_idle s \<and> pt_page_relation (ptr && ~~ mask pt_bits) pg_id (?ptr13 f sz s) UNIV s proof (prove)
goal (1 subgoal):
 1. \<And>f sz s. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s); pt_page_relation (ptr && ~~ mask pt_bits) pg_id ptr UNIV s; valid_idle s; ako_at (arch_kernel_obj.PageTable fun) (ptr && ~~ mask pt_bits) s; opt_cap (ptr && ~~ mask pt_bits, unat (ptr && mask pt_bits >> 2)) (transform s) = Some (FrameCap False pg_id f sz Fake None)\<rbrakk> \<Longrightarrow> pt_page_relation (ptr && ~~ mask pt_bits) pg_id (?ptr13 f sz s) UNIV s proof (prove)
goal:
No subgoals!