theory Finalise_DR

lemma finalise_slot_inner1_add_if_Null:
  "monadic_rewrite F False \<top>
     (finalise_slot_inner1 victim)
     (do cap \<leftarrow> KHeap_D.get_cap victim;
        if cap = cdl_cap.NullCap then return (cdl_cap.NullCap, True)
        else do
          final \<leftarrow> PageTableUnmap_D.is_final_cap cap;
          (cap', irqopt) \<leftarrow> CSpace_D.finalise_cap cap final;
          removeable \<leftarrow> gets $ CSpace_D.cap_removeable cap' victim;
          when (\<not> removeable) (KHeap_D.set_cap victim cap')
               \<sqinter> KHeap_D.set_cap victim cap';
          return (cap', removeable)
       od
     od)" supply if_cong[cong] apply (rule monadic_rewrite_weaken_flags[where F=False and E=False, simplified]) apply (simp add: finalise_slot_inner1_def when_def PageTableUnmap_D.is_final_cap_def) apply (rule monadic_rewrite_bind_tail) apply (rule monadic_rewrite_if_r, clarsimp) apply (monadic_rewrite_l monadic_rewrite_pick_alternative_1) apply (monadic_rewrite_l monadic_rewrite_if_l_False) apply monadic_rewrite_symb_exec_l_drop apply (monadic_rewrite_symb_exec_l_known True) apply monadic_rewrite_symb_exec_l apply (rule monadic_rewrite_refl) apply wpsimp+ apply (rule monadic_rewrite_refl) apply (clarsimp simp: CSpace_D.cap_removeable_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. monadic_rewrite F False (\<lambda>_. True) (finalise_slot_inner1 victim) (do cap <- KHeap_D.get_cap victim;
if cap = cdl_cap.NullCap then return (cdl_cap.NullCap, True) else do final <- PageTableUnmap_D.is_final_cap cap;
(cap', irqopt) <- CSpace_D.finalise_cap cap final;
removeable <- gets $ CSpace_D.cap_removeable cap' victim;
when (\<not> removeable) (KHeap_D.set_cap victim cap') \<sqinter> KHeap_D.set_cap victim cap';
return (cap', removeable)
od
od) proof (prove)
goal (1 subgoal):
 1. monadic_rewrite F False (\<lambda>_. True) (finalise_slot_inner1 victim) (do cap <- KHeap_D.get_cap victim;
if cap = cdl_cap.NullCap then return (cdl_cap.NullCap, True) else do final <- PageTableUnmap_D.is_final_cap cap;
(cap', irqopt) <- CSpace_D.finalise_cap cap final;
removeable <- gets $ CSpace_D.cap_removeable cap' victim;
when (\<not> removeable) (KHeap_D.set_cap victim cap') \<sqinter> KHeap_D.set_cap victim cap';
return (cap', removeable)
od
od) proof (prove)
goal (1 subgoal):
 1. monadic_rewrite False False (\<lambda>_. True) (finalise_slot_inner1 victim) (do cap <- KHeap_D.get_cap victim;
if cap = cdl_cap.NullCap then return (cdl_cap.NullCap, True) else do final <- PageTableUnmap_D.is_final_cap cap;
(cap', irqopt) <- CSpace_D.finalise_cap cap final;
removeable <- gets $ CSpace_D.cap_removeable cap' victim;
when (\<not> removeable) (KHeap_D.set_cap victim cap') \<sqinter> KHeap_D.set_cap victim cap';
return (cap', removeable)
od
od) proof (prove)
goal (1 subgoal):
 1. monadic_rewrite False False (\<lambda>_. True) (do cap <- KHeap_D.get_cap victim;
final <- gets (PageTableUnmap_D.is_final_cap' cap);
(cap', irqopt) <- CSpace_D.finalise_cap cap final;
removeable <- gets (CSpace_D.cap_removeable cap' victim);
y <- (if \<not> removeable then KHeap_D.set_cap victim cap' else return ()) \<sqinter> KHeap_D.set_cap victim cap';
return (cap', removeable)
od) (do cap <- KHeap_D.get_cap victim;
if cap = cdl_cap.NullCap then return (cdl_cap.NullCap, True) else do final <- gets (PageTableUnmap_D.is_final_cap' cap);
(cap', irqopt) <- CSpace_D.finalise_cap cap final;
removeable <- gets (CSpace_D.cap_removeable cap' victim);
y <- (if \<not> removeable then KHeap_D.set_cap victim cap' else return ()) \<sqinter> KHeap_D.set_cap victim cap';
return (cap', removeable)
od
od) proof (prove)
goal (2 subgoals):
 1. \<And>cap. monadic_rewrite False False (?Q4 cap) (do final <- gets (PageTableUnmap_D.is_final_cap' cap);
(cap', irqopt) <- CSpace_D.finalise_cap cap final;
removeable <- gets (CSpace_D.cap_removeable cap' victim);
y <- (if \<not> removeable then KHeap_D.set_cap victim cap' else return ()) \<sqinter> KHeap_D.set_cap victim cap';
return (cap', removeable)
od) (if cap = cdl_cap.NullCap then return (cdl_cap.NullCap, True) else do final <- gets (PageTableUnmap_D.is_final_cap' cap);
(cap', irqopt) <- CSpace_D.finalise_cap cap final;
removeable <- gets (CSpace_D.cap_removeable cap' victim);
y <- (if \<not> removeable then KHeap_D.set_cap victim cap' else return ()) \<sqinter> KHeap_D.set_cap victim cap';
return (cap', removeable)
od)
 2. \<lbrace>\<lambda>_. True\<rbrace> KHeap_D.get_cap victim \<lbrace>?Q4\<rbrace> proof (prove)
goal (3 subgoals):
 1. monadic_rewrite False False (?Q7 cdl_cap.NullCap) (do final <- gets (PageTableUnmap_D.is_final_cap' cdl_cap.NullCap);
removeable <- gets (CSpace_D.cap_removeable cdl_cap.NullCap victim);
y <- (if \<not> removeable then KHeap_D.set_cap victim cdl_cap.NullCap else return ()) \<sqinter> KHeap_D.set_cap victim cdl_cap.NullCap;
return (cdl_cap.NullCap, removeable)
od) (return (cdl_cap.NullCap, True))
 2. \<And>cap. cap \<noteq> cdl_cap.NullCap \<Longrightarrow> monadic_rewrite False False (?R7 cap) (do final <- gets (PageTableUnmap_D.is_final_cap' cap);
(cap', irqopt) <- CSpace_D.finalise_cap cap final;
removeable <- gets (CSpace_D.cap_removeable cap' victim);
y <- (if \<not> removeable then KHeap_D.set_cap victim cap' else return ()) \<sqinter> KHeap_D.set_cap victim cap';
return (cap', removeable)
od) (do final <- gets (PageTableUnmap_D.is_final_cap' cap);
(cap', irqopt) <- CSpace_D.finalise_cap cap final;
removeable <- gets (CSpace_D.cap_removeable cap' victim);
y <- (if \<not> removeable then KHeap_D.set_cap victim cap' else return ()) \<sqinter> KHeap_D.set_cap victim cap';
return (cap', removeable)
od)
 3. \<lbrace>\<lambda>_. True\<rbrace> KHeap_D.get_cap victim \<lbrace>\<lambda>cap s. (cap = cdl_cap.NullCap \<longrightarrow> ?Q7 cap s) \<and> (cap \<noteq> cdl_cap.NullCap \<longrightarrow> ?R7 cap s)\<rbrace> proof (prove)
goal (3 subgoals):
 1. monadic_rewrite False False (?Q15 cdl_cap.NullCap) (do x <- gets (PageTableUnmap_D.is_final_cap' cdl_cap.NullCap);
xa <- gets (CSpace_D.cap_removeable cdl_cap.NullCap victim);
y <- if \<not> xa then KHeap_D.set_cap victim cdl_cap.NullCap else return ();
return (cdl_cap.NullCap, xa)
od) (return (cdl_cap.NullCap, True))
 2. \<And>cap. cap \<noteq> cdl_cap.NullCap \<Longrightarrow> monadic_rewrite False False (?R7 cap) (do final <- gets (PageTableUnmap_D.is_final_cap' cap);
(cap', irqopt) <- CSpace_D.finalise_cap cap final;
removeable <- gets (CSpace_D.cap_removeable cap' victim);
y <- (if \<not> removeable then KHeap_D.set_cap victim cap' else return ()) \<sqinter> KHeap_D.set_cap victim cap';
return (cap', removeable)
od) (do final <- gets (PageTableUnmap_D.is_final_cap' cap);
(cap', irqopt) <- CSpace_D.finalise_cap cap final;
removeable <- gets (CSpace_D.cap_removeable cap' victim);
y <- (if \<not> removeable then KHeap_D.set_cap victim cap' else return ()) \<sqinter> KHeap_D.set_cap victim cap';
return (cap', removeable)
od)
 3. \<lbrace>\<lambda>_. True\<rbrace> KHeap_D.get_cap victim \<lbrace>\<lambda>cap s. (cap = cdl_cap.NullCap \<longrightarrow> ((\<lambda>a. True) and ?Q15 cap) s) \<and> (cap \<noteq> cdl_cap.NullCap \<longrightarrow> ?R7 cap s)\<rbrace> proof (prove)
goal (3 subgoals):
 1. monadic_rewrite False False (?Q55 cdl_cap.NullCap) (do x <- gets (PageTableUnmap_D.is_final_cap' cdl_cap.NullCap);
xa <- gets (CSpace_D.cap_removeable cdl_cap.NullCap victim);
y <- return ();
return (cdl_cap.NullCap, xa)
od) (return (cdl_cap.NullCap, True))
 2. \<And>cap. cap \<noteq> cdl_cap.NullCap \<Longrightarrow> monadic_rewrite False False (?R7 cap) (do final <- gets (PageTableUnmap_D.is_final_cap' cap);
(cap', irqopt) <- CSpace_D.finalise_cap cap final;
removeable <- gets (CSpace_D.cap_removeable cap' victim);
y <- (if \<not> removeable then KHeap_D.set_cap victim cap' else return ()) \<sqinter> KHeap_D.set_cap victim cap';
return (cap', removeable)
od) (do final <- gets (PageTableUnmap_D.is_final_cap' cap);
(cap', irqopt) <- CSpace_D.finalise_cap cap final;
removeable <- gets (CSpace_D.cap_removeable cap' victim);
y <- (if \<not> removeable then KHeap_D.set_cap victim cap' else return ()) \<sqinter> KHeap_D.set_cap victim cap';
return (cap', removeable)
od)
 3. \<lbrace>\<lambda>_. True\<rbrace> KHeap_D.get_cap victim \<lbrace>\<lambda>cap s. (cap = cdl_cap.NullCap \<longrightarrow> ((\<lambda>a. True) and ((\<lambda>a. ((\<lambda>_. \<not> \<not> CSpace_D.cap_removeable cdl_cap.NullCap victim a) and (\<lambda>_. True)) a) and ?Q55 cap)) s) \<and> (cap \<noteq> cdl_cap.NullCap \<longrightarrow> ?R7 cap s)\<rbrace> proof (prove)
goal (3 subgoals):
 1. monadic_rewrite False False (?P99 cdl_cap.NullCap) (do xa <- gets (CSpace_D.cap_removeable cdl_cap.NullCap victim);
y <- return ();
return (cdl_cap.NullCap, xa)
od) (return (cdl_cap.NullCap, True))
 2. \<And>cap. cap \<noteq> cdl_cap.NullCap \<Longrightarrow> monadic_rewrite False False (?R7 cap) (do final <- gets (PageTableUnmap_D.is_final_cap' cap);
(cap', irqopt) <- CSpace_D.finalise_cap cap final;
removeable <- gets (CSpace_D.cap_removeable cap' victim);
y <- (if \<not> removeable then KHeap_D.set_cap victim cap' else return ()) \<sqinter> KHeap_D.set_cap victim cap';
return (cap', removeable)
od) (do final <- gets (PageTableUnmap_D.is_final_cap' cap);
(cap', irqopt) <- CSpace_D.finalise_cap cap final;
removeable <- gets (CSpace_D.cap_removeable cap' victim);
y <- (if \<not> removeable then KHeap_D.set_cap victim cap' else return ()) \<sqinter> KHeap_D.set_cap victim cap';
return (cap', removeable)
od)
 3. \<lbrace>\<lambda>_. True\<rbrace> KHeap_D.get_cap victim \<lbrace>\<lambda>cap s. (cap = cdl_cap.NullCap \<longrightarrow> ((\<lambda>a. True) and ((\<lambda>a. ((\<lambda>_. \<not> \<not> CSpace_D.cap_removeable cdl_cap.NullCap victim a) and (\<lambda>_. True)) a) and (?P99 cap and (\<lambda>a. True)))) s) \<and> (cap \<noteq> cdl_cap.NullCap \<longrightarrow> ?R7 cap s)\<rbrace> proof (prove)
goal (4 subgoals):
 1. monadic_rewrite False False (?Q139 cdl_cap.NullCap) (do y <- return ();
return (cdl_cap.NullCap, True)
od) (return (cdl_cap.NullCap, True))
 2. \<lbrace>?P141 cdl_cap.NullCap\<rbrace> gets (CSpace_D.cap_removeable cdl_cap.NullCap victim) \<lbrace>\<lambda>rv' s. rv' = True\<rbrace>
 3. \<And>cap. cap \<noteq> cdl_cap.NullCap \<Longrightarrow> monadic_rewrite False False (?R7 cap) (do final <- gets (PageTableUnmap_D.is_final_cap' cap);
(cap', irqopt) <- CSpace_D.finalise_cap cap final;
removeable <- gets (CSpace_D.cap_removeable cap' victim);
y <- (if \<not> removeable then KHeap_D.set_cap victim cap' else return ()) \<sqinter> KHeap_D.set_cap victim cap';
return (cap', removeable)
od) (do final <- gets (PageTableUnmap_D.is_final_cap' cap);
(cap', irqopt) <- CSpace_D.finalise_cap cap final;
removeable <- gets (CSpace_D.cap_removeable cap' victim);
y <- (if \<not> removeable then KHeap_D.set_cap victim cap' else return ()) \<sqinter> KHeap_D.set_cap victim cap';
return (cap', removeable)
od)
 4. \<lbrace>\<lambda>_. True\<rbrace> KHeap_D.get_cap victim \<lbrace>\<lambda>cap s. (cap = cdl_cap.NullCap \<longrightarrow> ((\<lambda>a. True) and ((\<lambda>a. ((\<lambda>_. \<not> \<not> CSpace_D.cap_removeable cdl_cap.NullCap victim a) and (\<lambda>_. True)) a) and (?P141 cap and (\<lambda>a. True) and ?Q139 cap and (\<lambda>a. True)))) s) \<and> (cap \<noteq> cdl_cap.NullCap \<longrightarrow> ?R7 cap s)\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>y. monadic_rewrite False False (?Q175 y) (return (cdl_cap.NullCap, True)) (return (cdl_cap.NullCap, True))
 2. \<lbrace>?P179 cdl_cap.NullCap\<rbrace> return () \<lbrace>?Q175\<rbrace>
 3. \<lbrace>?P141 cdl_cap.NullCap\<rbrace> gets (CSpace_D.cap_removeable cdl_cap.NullCap victim) \<lbrace>\<lambda>rv' s. rv' = True\<rbrace>
 4. \<And>cap. cap \<noteq> cdl_cap.NullCap \<Longrightarrow> monadic_rewrite False False (?R7 cap) (do final <- gets (PageTableUnmap_D.is_final_cap' cap);
(cap', irqopt) <- CSpace_D.finalise_cap cap final;
removeable <- gets (CSpace_D.cap_removeable cap' victim);
y <- (if \<not> removeable then KHeap_D.set_cap victim cap' else return ()) \<sqinter> KHeap_D.set_cap victim cap';
return (cap', removeable)
od) (do final <- gets (PageTableUnmap_D.is_final_cap' cap);
(cap', irqopt) <- CSpace_D.finalise_cap cap final;
removeable <- gets (CSpace_D.cap_removeable cap' victim);
y <- (if \<not> removeable then KHeap_D.set_cap victim cap' else return ()) \<sqinter> KHeap_D.set_cap victim cap';
return (cap', removeable)
od)
 5. \<lbrace>\<lambda>_. True\<rbrace> KHeap_D.get_cap victim \<lbrace>\<lambda>cap s. (cap = cdl_cap.NullCap \<longrightarrow> ((\<lambda>a. True) and ((\<lambda>a. ((\<lambda>_. \<not> \<not> CSpace_D.cap_removeable cdl_cap.NullCap victim a) and (\<lambda>_. True)) a) and (?P141 cap and (\<lambda>a. True) and (?P179 cap and (\<lambda>a. True)) and (\<lambda>a. True)))) s) \<and> (cap \<noteq> cdl_cap.NullCap \<longrightarrow> ?R7 cap s)\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<lbrace>?P179 cdl_cap.NullCap\<rbrace> return () \<lbrace>\<lambda>y _. True\<rbrace>
 2. \<lbrace>?P141 cdl_cap.NullCap\<rbrace> gets (CSpace_D.cap_removeable cdl_cap.NullCap victim) \<lbrace>\<lambda>rv' s. rv' = True\<rbrace>
 3. \<And>cap. cap \<noteq> cdl_cap.NullCap \<Longrightarrow> monadic_rewrite False False (?R7 cap) (do final <- gets (PageTableUnmap_D.is_final_cap' cap);
(cap', irqopt) <- CSpace_D.finalise_cap cap final;
removeable <- gets (CSpace_D.cap_removeable cap' victim);
y <- (if \<not> removeable then KHeap_D.set_cap victim cap' else return ()) \<sqinter> KHeap_D.set_cap victim cap';
return (cap', removeable)
od) (do final <- gets (PageTableUnmap_D.is_final_cap' cap);
(cap', irqopt) <- CSpace_D.finalise_cap cap final;
removeable <- gets (CSpace_D.cap_removeable cap' victim);
y <- (if \<not> removeable then KHeap_D.set_cap victim cap' else return ()) \<sqinter> KHeap_D.set_cap victim cap';
return (cap', removeable)
od)
 4. \<lbrace>\<lambda>_. True\<rbrace> KHeap_D.get_cap victim \<lbrace>\<lambda>cap s. (cap = cdl_cap.NullCap \<longrightarrow> ((\<lambda>a. True) and ((\<lambda>a. ((\<lambda>_. \<not> \<not> CSpace_D.cap_removeable cdl_cap.NullCap victim a) and (\<lambda>_. True)) a) and (?P141 cap and (\<lambda>a. True) and (?P179 cap and (\<lambda>a. True)) and (\<lambda>a. True)))) s) \<and> (cap \<noteq> cdl_cap.NullCap \<longrightarrow> ?R7 cap s)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>cap. cap \<noteq> cdl_cap.NullCap \<Longrightarrow> monadic_rewrite False False (?R7 cap) (do final <- gets (PageTableUnmap_D.is_final_cap' cap);
(cap', irqopt) <- CSpace_D.finalise_cap cap final;
removeable <- gets (CSpace_D.cap_removeable cap' victim);
y <- (if \<not> removeable then KHeap_D.set_cap victim cap' else return ()) \<sqinter> KHeap_D.set_cap victim cap';
return (cap', removeable)
od) (do final <- gets (PageTableUnmap_D.is_final_cap' cap);
(cap', irqopt) <- CSpace_D.finalise_cap cap final;
removeable <- gets (CSpace_D.cap_removeable cap' victim);
y <- (if \<not> removeable then KHeap_D.set_cap victim cap' else return ()) \<sqinter> KHeap_D.set_cap victim cap';
return (cap', removeable)
od)
 2. \<lbrace>\<lambda>_. True\<rbrace> KHeap_D.get_cap victim \<lbrace>\<lambda>cap s. (cap = cdl_cap.NullCap \<longrightarrow> ((\<lambda>a. True) and ((\<lambda>a. ((\<lambda>_. \<not> \<not> CSpace_D.cap_removeable cdl_cap.NullCap victim a) and (\<lambda>_. True)) a) and ((\<lambda>a. CSpace_D.cap_removeable cdl_cap.NullCap victim a = True) and (\<lambda>a. True) and ((\<lambda>a. True) and (\<lambda>a. True)) and (\<lambda>a. True)))) s) \<and> (cap \<noteq> cdl_cap.NullCap \<longrightarrow> ?R7 cap s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> KHeap_D.get_cap victim \<lbrace>\<lambda>cap s. (cap = cdl_cap.NullCap \<longrightarrow> ((\<lambda>a. True) and ((\<lambda>a. ((\<lambda>_. \<not> \<not> CSpace_D.cap_removeable cdl_cap.NullCap victim a) and (\<lambda>_. True)) a) and ((\<lambda>a. CSpace_D.cap_removeable cdl_cap.NullCap victim a = True) and (\<lambda>a. True) and ((\<lambda>a. True) and (\<lambda>a. True)) and (\<lambda>a. True)))) s) \<and> (cap \<noteq> cdl_cap.NullCap \<longrightarrow> True)\<rbrace> proof (prove)
goal:
No subgoals!