theory CNodeInv_AI

lemma cap_swap_for_delete_emptyable[wp]:
  "\<lbrace>emptyable sl and emptyable sl'\<rbrace> cap_swap_for_delete sl' sl \<lbrace>\<lambda>rv. emptyable sl\<rbrace>" apply (simp add: emptyable_def cap_swap_for_delete_def cap_swap_def tcb_at_typ) apply (rule hoare_pre) apply (subst imp_conv_disj)+ apply (wp hoare_vcg_disj_lift set_cdt_typ_at set_cap_typ_at | simp split del: if_split)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>emptyable sl and emptyable sl'\<rbrace> cap_swap_for_delete sl' sl \<lbrace>\<lambda>rv. emptyable sl\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>(\<lambda>s. typ_at ATCB (fst sl) s \<and> snd sl = tcb_cnode_index 2 \<longrightarrow> st_tcb_at halted (fst sl) s) and (\<lambda>s. typ_at ATCB (fst sl') s \<and> snd sl' = tcb_cnode_index 2 \<longrightarrow> st_tcb_at halted (fst sl') s)\<rbrace> when (sl' \<noteq> sl) (do cap1 <- get_cap sl';
cap2 <- get_cap sl;
y <- set_cap cap2 sl';
y <- set_cap cap1 sl;
slot1_p <- gets (\<lambda>s. cdt s sl');
slot2_p <- gets (\<lambda>s. cdt s sl);
cdt <- gets cdt;
y <- set_cdt ((\<lambda>n. if cdt n = Some sl' then Some sl else if cdt n = Some sl then Some sl' else cdt n)(sl' := if cdt sl = Some sl' then Some sl else if cdt sl = Some sl then Some sl' else cdt sl, sl := if cdt sl' = Some sl' then Some sl else if cdt sl' = Some sl then Some sl' else cdt sl'));
y <- do_extended_op (cap_swap_ext sl' sl slot1_p slot2_p);
is_original <- gets is_original_cap;
y <- set_original sl' (is_original sl);
set_original sl (is_original sl')
od) \<lbrace>\<lambda>rv s. typ_at ATCB (fst sl) s \<and> snd sl = tcb_cnode_index 2 \<longrightarrow> st_tcb_at halted (fst sl) s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q3\<rbrace> when (sl' \<noteq> sl) (do cap1 <- get_cap sl';
cap2 <- get_cap sl;
y <- set_cap cap2 sl';
y <- set_cap cap1 sl;
slot1_p <- gets (\<lambda>s. cdt s sl');
slot2_p <- gets (\<lambda>s. cdt s sl);
cdt <- gets cdt;
y <- set_cdt ((\<lambda>n. if cdt n = Some sl' then Some sl else if cdt n = Some sl then Some sl' else cdt n)(sl' := if cdt sl = Some sl' then Some sl else if cdt sl = Some sl then Some sl' else cdt sl, sl := if cdt sl' = Some sl' then Some sl else if cdt sl' = Some sl then Some sl' else cdt sl'));
y <- do_extended_op (cap_swap_ext sl' sl slot1_p slot2_p);
is_original <- gets is_original_cap;
y <- set_original sl' (is_original sl);
set_original sl (is_original sl')
od) \<lbrace>\<lambda>rv s. typ_at ATCB (fst sl) s \<and> snd sl = tcb_cnode_index 2 \<longrightarrow> st_tcb_at halted (fst sl) s\<rbrace>
 2. \<And>s. ((\<lambda>s. typ_at ATCB (fst sl) s \<and> snd sl = tcb_cnode_index 2 \<longrightarrow> st_tcb_at halted (fst sl) s) and (\<lambda>s. typ_at ATCB (fst sl') s \<and> snd sl' = tcb_cnode_index 2 \<longrightarrow> st_tcb_at halted (fst sl') s)) s \<Longrightarrow> ?Q3 s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q3\<rbrace> when (sl' \<noteq> sl) (do cap1 <- get_cap sl';
cap2 <- get_cap sl;
y <- set_cap cap2 sl';
y <- set_cap cap1 sl;
slot1_p <- gets (\<lambda>s. cdt s sl');
slot2_p <- gets (\<lambda>s. cdt s sl);
cdt <- gets cdt;
y <- set_cdt ((\<lambda>n. if cdt n = Some sl' then Some sl else if cdt n = Some sl then Some sl' else cdt n)(sl' := if cdt sl = Some sl' then Some sl else if cdt sl = Some sl then Some sl' else cdt sl, sl := if cdt sl' = Some sl' then Some sl else if cdt sl' = Some sl then Some sl' else cdt sl'));
y <- do_extended_op (cap_swap_ext sl' sl slot1_p slot2_p);
is_original <- gets is_original_cap;
y <- set_original sl' (is_original sl);
set_original sl (is_original sl')
od) \<lbrace>\<lambda>rv s. \<not> (typ_at ATCB (fst sl) s \<and> snd sl = tcb_cnode_index 2) \<or> st_tcb_at halted (fst sl) s\<rbrace>
 2. \<And>s. ((\<lambda>s. typ_at ATCB (fst sl) s \<and> snd sl = tcb_cnode_index 2 \<longrightarrow> st_tcb_at halted (fst sl) s) and (\<lambda>s. typ_at ATCB (fst sl') s \<and> snd sl' = tcb_cnode_index 2 \<longrightarrow> st_tcb_at halted (fst sl') s)) s \<Longrightarrow> ?Q3 s proof (prove)
goal:
No subgoals!