theory CNodeInv_R

lemma emptySlot_rvk_prog:
  "\<lbrace>\<lambda>s. revoke_progress_ord m (option_map capToRPO \<circ> cteCaps_of s)\<rbrace>
     emptySlot sl opt
   \<lbrace>\<lambda>rv s. revoke_progress_ord m (option_map capToRPO \<circ> cteCaps_of s)\<rbrace>" apply (simp add: emptySlot_def case_Null_If) apply (wp getCTE_cteCap_wp opt_return_pres_lift) apply (clarsimp simp: o_def split: option.split) apply (erule rpo_trans) apply (rule rpo_delta[where S="{sl}"], simp_all) apply (simp add: modify_map_def) apply (simp add: Int_insert_left dom_def modify_map_def) apply (clarsimp simp: capToRPO_def split: capability.split) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. revoke_progress_ord m (map_option capToRPO \<circ> cteCaps_of s)\<rbrace> emptySlot sl opt \<lbrace>\<lambda>rv s. revoke_progress_ord m (map_option capToRPO \<circ> cteCaps_of s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. revoke_progress_ord m (map_option capToRPO \<circ> cteCaps_of s)\<rbrace> do y <- clearUntypedFreeIndex sl;
newCTE <- getCTE sl;
if cteCap newCTE = capability.NullCap then return () else do y <- updateMDB (mdbPrev (cteMDBNode newCTE)) (mdbNext_update (\<lambda>_. mdbNext (cteMDBNode newCTE)));
y <- updateMDB (mdbNext (cteMDBNode newCTE)) (\<lambda>mdb. mdbFirstBadged_update (\<lambda>_. mdbFirstBadged mdb \<or> mdbFirstBadged (cteMDBNode newCTE)) (mdbPrev_update (\<lambda>_. mdbPrev (cteMDBNode newCTE)) mdb));
y <- updateCap sl capability.NullCap;
y <- updateMDB sl (const nullMDBNode);
global.postCapDeletion opt
od
od \<lbrace>\<lambda>rv s. revoke_progress_ord m (map_option capToRPO \<circ> cteCaps_of s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. revoke_progress_ord m (map_option capToRPO \<circ> cteCaps_of s) \<Longrightarrow> case cteCaps_of s sl of None \<Rightarrow> True | Some cap \<Rightarrow> (cap = capability.NullCap \<longrightarrow> revoke_progress_ord m (map_option capToRPO \<circ> cteCaps_of s)) \<and> (cap \<noteq> capability.NullCap \<longrightarrow> revoke_progress_ord m (map_option capToRPO \<circ> modify_map (cteCaps_of s) sl (K capability.NullCap))) proof (prove)
goal (1 subgoal):
 1. \<And>s x2. \<lbrakk>revoke_progress_ord m (\<lambda>x. map_option capToRPO (cteCaps_of s x)); cteCaps_of s sl = Some x2; x2 \<noteq> capability.NullCap\<rbrakk> \<Longrightarrow> revoke_progress_ord m (\<lambda>a. map_option capToRPO (modify_map (cteCaps_of s) sl (\<lambda>a. capability.NullCap) a)) proof (prove)
goal (1 subgoal):
 1. \<And>s x2. \<lbrakk>cteCaps_of s sl = Some x2; x2 \<noteq> capability.NullCap\<rbrakk> \<Longrightarrow> revoke_progress_ord (\<lambda>x. map_option capToRPO (cteCaps_of s x)) (\<lambda>a. map_option capToRPO (modify_map (cteCaps_of s) sl (\<lambda>a. capability.NullCap) a)) proof (prove)
goal (2 subgoals):
 1. \<And>s x2 x. \<lbrakk>cteCaps_of s sl = Some x2; x2 \<noteq> capability.NullCap; x \<noteq> sl\<rbrakk> \<Longrightarrow> map_option capToRPO (cteCaps_of s x) = map_option capToRPO (modify_map (cteCaps_of s) sl (\<lambda>a. capability.NullCap) x)
 2. \<And>s x2. \<lbrakk>cteCaps_of s sl = Some x2; x2 \<noteq> capability.NullCap\<rbrakk> \<Longrightarrow> (\<Sum>x\<in>{sl} \<inter> dom (\<lambda>a. map_option capToRPO (modify_map (cteCaps_of s) sl (\<lambda>a. capability.NullCap) a)). rpo_measure x (map_option capToRPO (modify_map (cteCaps_of s) x (\<lambda>a. capability.NullCap) x))) < (\<Sum>x\<in>{sl} \<inter> dom (\<lambda>x. map_option capToRPO (cteCaps_of s x)). rpo_measure x (Some (capToRPO x2))) proof (prove)
goal (1 subgoal):
 1. \<And>s x2. \<lbrakk>cteCaps_of s sl = Some x2; x2 \<noteq> capability.NullCap\<rbrakk> \<Longrightarrow> (\<Sum>x\<in>{sl} \<inter> dom (\<lambda>a. map_option capToRPO (modify_map (cteCaps_of s) sl (\<lambda>a. capability.NullCap) a)). rpo_measure x (map_option capToRPO (modify_map (cteCaps_of s) x (\<lambda>a. capability.NullCap) x))) < (\<Sum>x\<in>{sl} \<inter> dom (\<lambda>x. map_option capToRPO (cteCaps_of s x)). rpo_measure x (Some (capToRPO x2))) proof (prove)
goal (1 subgoal):
 1. \<And>s x2. \<lbrakk>cteCaps_of s sl = Some x2; x2 \<noteq> capability.NullCap\<rbrakk> \<Longrightarrow> rpo_measure sl (Some (capToRPO capability.NullCap)) < rpo_measure sl (Some (capToRPO x2)) proof (prove)
goal:
No subgoals!