theory CNodeInv_AI

lemma empty_slot_rvk_prog:
  "\<lbrace>\<lambda>s. revoke_progress_ord m (option_map cap_to_rpo \<circ> caps_of_state s)\<rbrace>
     empty_slot sl opt
   \<lbrace>\<lambda>rv s. revoke_progress_ord m (option_map cap_to_rpo \<circ> caps_of_state s)\<rbrace>" apply (simp add: empty_slot_def) apply (rule hoare_pre) apply (wp opt_return_pres_lift | simp split del: if_split)+ apply (wp get_cap_wp) apply (clarsimp simp: cte_wp_at_caps_of_state) apply (erule rpo_trans) apply (rule rpo_delta[where S="{sl}"],
         simp_all add: dom_def caps_of_state_set_finite exception_set_finite) apply (case_tac cap, simp_all add: cap_to_rpo_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s)\<rbrace> empty_slot sl opt \<lbrace>\<lambda>rv s. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s)\<rbrace> do cap <- get_cap sl;
if cap = NullCap then return () else do slot_p <- gets (\<lambda>s. cdt s sl);
cdt <- gets cdt;
y <- set_cdt ((\<lambda>p. if cdt p = Some sl then cdt sl else cdt p)(sl := None));
y <- do_extended_op (empty_slot_ext sl slot_p);
y <- set_original sl False;
y <- set_cap NullCap sl;
post_cap_deletion opt
od
od \<lbrace>\<lambda>rv s. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q4\<rbrace> do cap <- get_cap sl;
if cap = NullCap then return () else do slot_p <- gets (\<lambda>s. cdt s sl);
cdt <- gets cdt;
y <- set_cdt ((\<lambda>p. if cdt p = Some sl then cdt sl else cdt p)(sl := None));
y <- do_extended_op (empty_slot_ext sl slot_p);
y <- set_original sl False;
y <- set_cap NullCap sl;
post_cap_deletion opt
od
od \<lbrace>\<lambda>rv s. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s)\<rbrace>
 2. \<And>s. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s) \<Longrightarrow> ?Q4 s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q4\<rbrace> get_cap sl \<lbrace>\<lambda>cap s. (cap = NullCap \<longrightarrow> revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s)) \<and> (cap \<noteq> NullCap \<longrightarrow> revoke_progress_ord m (\<lambda>a. map_option cap_to_rpo (if a = sl then Some NullCap else caps_of_state s a)))\<rbrace>
 2. \<And>s. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s) \<Longrightarrow> ?Q4 s proof (prove)
goal (1 subgoal):
 1. \<And>s. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s) \<Longrightarrow> \<forall>cap. cte_wp_at ((=) cap) sl s \<longrightarrow> (cap = NullCap \<longrightarrow> revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s)) \<and> (cap \<noteq> NullCap \<longrightarrow> revoke_progress_ord m (\<lambda>a. map_option cap_to_rpo (if a = sl then Some NullCap else caps_of_state s a))) proof (prove)
goal (1 subgoal):
 1. \<And>s cap. \<lbrakk>revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s); caps_of_state s sl = Some cap; cap \<noteq> NullCap\<rbrakk> \<Longrightarrow> revoke_progress_ord m (\<lambda>a. map_option cap_to_rpo (if a = sl then Some NullCap else caps_of_state s a)) proof (prove)
goal (1 subgoal):
 1. \<And>s cap. \<lbrakk>caps_of_state s sl = Some cap; cap \<noteq> NullCap\<rbrakk> \<Longrightarrow> revoke_progress_ord (map_option cap_to_rpo \<circ> caps_of_state s) (\<lambda>a. map_option cap_to_rpo (if a = sl then Some NullCap else caps_of_state s a)) proof (prove)
goal (1 subgoal):
 1. \<And>s cap. \<lbrakk>caps_of_state s sl = Some cap; cap \<noteq> NullCap\<rbrakk> \<Longrightarrow> rpo_measure sl (Some (cap_to_rpo NullCap)) < rpo_measure sl (Some (cap_to_rpo cap)) proof (prove)
goal:
No subgoals!