theory Invoke_C

lemma mapME_ensureEmptySlot':
  "\<lbrace>P\<rbrace>
  mapME (\<lambda>x. injection_handler Inl (ensureEmptySlot (f x))) slots
  \<lbrace>\<lambda>rva s. P s \<and> (\<forall>slot \<in> set slots. (\<exists>cte. cteCap cte = capability.NullCap \<and> ctes_of s (f slot) = Some cte))\<rbrace>, -" including no_pre apply (induct slots arbitrary: P) apply wpsimp apply (rename_tac a slots P) apply (simp add: mapME_def sequenceE_def Let_def) apply (rule_tac Q="\<lambda>rv. P and (\<lambda>s. \<exists>cte. cteCap cte = capability.NullCap \<and> ctes_of s (f a) = Some cte)" in validE_R_sp) apply (simp add: ensureEmptySlot_def unlessE_def) apply (wp injection_wp_E[OF refl] getCTE_wp') apply (clarsimp simp: cte_wp_at_ctes_of) apply (erule meta_allE) apply wp apply (fold validE_R_def) apply (erule hoare_post_imp_R) apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> mapME (\<lambda>x. injection_handler Inl (ensureEmptySlot (f x))) slots \<lbrace>\<lambda>rva s. P s \<and> (\<forall>slot\<in>set slots. \<exists>cte. cteCap cte = capability.NullCap \<and> ctes_of s (f slot) = Some cte)\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> mapME (\<lambda>x. injection_handler Inl (ensureEmptySlot (f x))) slots \<lbrace>\<lambda>rva s. P s \<and> (\<forall>slot\<in>set slots. \<exists>cte. cteCap cte = capability.NullCap \<and> ctes_of s (f slot) = Some cte)\<rbrace>, - proof (prove)
goal (2 subgoals):
 1. \<And>P. \<lbrace>P\<rbrace> mapME (\<lambda>x. injection_handler Inl (ensureEmptySlot (f x))) [] \<lbrace>\<lambda>rva s. P s \<and> (\<forall>slot\<in>set []. \<exists>cte. cteCap cte = capability.NullCap \<and> ctes_of s (f slot) = Some cte)\<rbrace>, -
 2. \<And>x1 slots P. (\<And>P. \<lbrace>P\<rbrace> mapME (\<lambda>x. injection_handler Inl (ensureEmptySlot (f x))) slots \<lbrace>\<lambda>rva s. P s \<and> (\<forall>slot\<in>set slots. \<exists>cte. cteCap cte = capability.NullCap \<and> ctes_of s (f slot) = Some cte)\<rbrace>, -) \<Longrightarrow> \<lbrace>P\<rbrace> mapME (\<lambda>x. injection_handler Inl (ensureEmptySlot (f x))) (x1 # slots) \<lbrace>\<lambda>rva s. P s \<and> (\<forall>slot\<in>set (x1 # slots). \<exists>cte. cteCap cte = capability.NullCap \<and> ctes_of s (f slot) = Some cte)\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<And>x1 slots P. (\<And>P. \<lbrace>P\<rbrace> mapME (\<lambda>x. injection_handler Inl (ensureEmptySlot (f x))) slots \<lbrace>\<lambda>rva s. P s \<and> (\<forall>slot\<in>set slots. \<exists>cte. cteCap cte = capability.NullCap \<and> ctes_of s (f slot) = Some cte)\<rbrace>, -) \<Longrightarrow> \<lbrace>P\<rbrace> mapME (\<lambda>x. injection_handler Inl (ensureEmptySlot (f x))) (x1 # slots) \<lbrace>\<lambda>rva s. P s \<and> (\<forall>slot\<in>set (x1 # slots). \<exists>cte. cteCap cte = capability.NullCap \<and> ctes_of s (f slot) = Some cte)\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<And>a slots P. (\<And>P. \<lbrace>P\<rbrace> mapME (\<lambda>x. injection_handler Inl (ensureEmptySlot (f x))) slots \<lbrace>\<lambda>rva s. P s \<and> (\<forall>slot\<in>set slots. \<exists>cte. cteCap cte = capability.NullCap \<and> ctes_of s (f slot) = Some cte)\<rbrace>, -) \<Longrightarrow> \<lbrace>P\<rbrace> mapME (\<lambda>x. injection_handler Inl (ensureEmptySlot (f x))) (a # slots) \<lbrace>\<lambda>rva s. P s \<and> (\<forall>slot\<in>set (a # slots). \<exists>cte. cteCap cte = capability.NullCap \<and> ctes_of s (f slot) = Some cte)\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<And>a slots P. (\<And>P. \<lbrace>P\<rbrace> foldr (\<lambda>p q. doE x <- p;
y <- q;
returnOk (() # y)
odE) (map (\<lambda>x. injection_handler Inl (ensureEmptySlot (f x))) slots) (returnOk []) \<lbrace>\<lambda>rva s. P s \<and> (\<forall>slot\<in>set slots. \<exists>cte. cteCap cte = capability.NullCap \<and> ctes_of s (f slot) = Some cte)\<rbrace>, -) \<Longrightarrow> \<lbrace>P\<rbrace> doE x <- injection_handler Inl (ensureEmptySlot (f a));
y <- foldr (\<lambda>p q. doE x <- p;
y <- q;
returnOk (() # y)
odE) (map (\<lambda>x. injection_handler Inl (ensureEmptySlot (f x))) slots) (returnOk []);
returnOk (() # y)
odE \<lbrace>\<lambda>rva s. P s \<and> (\<exists>cte. cteCap cte = capability.NullCap \<and> ctes_of s (f a) = Some cte) \<and> (\<forall>slot\<in>set slots. \<exists>cte. cteCap cte = capability.NullCap \<and> ctes_of s (f slot) = Some cte)\<rbrace>, - proof (prove)
goal (2 subgoals):
 1. \<And>a slots P. (\<And>P. \<lbrace>P\<rbrace> foldr (\<lambda>p q. doE x <- p;
y <- q;
returnOk (() # y)
odE) (map (\<lambda>x. injection_handler Inl (ensureEmptySlot (f x))) slots) (returnOk []) \<lbrace>\<lambda>rva s. P s \<and> (\<forall>slot\<in>set slots. \<exists>cte. cteCap cte = capability.NullCap \<and> ctes_of s (f slot) = Some cte)\<rbrace>, -) \<Longrightarrow> \<lbrace>P\<rbrace> injection_handler Inl (ensureEmptySlot (f a)) \<lbrace>\<lambda>rv. P and (\<lambda>s. \<exists>cte. cteCap cte = capability.NullCap \<and> ctes_of s (f a) = Some cte)\<rbrace>, -
 2. \<And>a slots P x. (\<And>P. \<lbrace>P\<rbrace> foldr (\<lambda>p q. doE x <- p;
y <- q;
returnOk (() # y)
odE) (map (\<lambda>x. injection_handler Inl (ensureEmptySlot (f x))) slots) (returnOk []) \<lbrace>\<lambda>rva s. P s \<and> (\<forall>slot\<in>set slots. \<exists>cte. cteCap cte = capability.NullCap \<and> ctes_of s (f slot) = Some cte)\<rbrace>, -) \<Longrightarrow> \<lbrace>P and (\<lambda>s. \<exists>cte. cteCap cte = capability.NullCap \<and> ctes_of s (f a) = Some cte)\<rbrace> doE y <- foldr (\<lambda>p q. doE x <- p;
y <- q;
returnOk (() # y)
odE) (map (\<lambda>x. injection_handler Inl (ensureEmptySlot (f x))) slots) (returnOk []);
returnOk (() # y)
odE \<lbrace>\<lambda>rva s. P s \<and> (\<exists>cte. cteCap cte = capability.NullCap \<and> ctes_of s (f a) = Some cte) \<and> (\<forall>slot\<in>set slots. \<exists>cte. cteCap cte = capability.NullCap \<and> ctes_of s (f slot) = Some cte)\<rbrace>, - proof (prove)
goal (2 subgoals):
 1. \<And>a slots P. (\<And>P. \<lbrace>P\<rbrace> foldr (\<lambda>p q. doE x <- p;
y <- q;
returnOk (() # y)
odE) (map (\<lambda>x. injection_handler Inl (doE cte <- liftE (getCTE (f x));
if cteCap cte = capability.NullCap then returnOk () else throwError Fault_H.syscall_error.DeleteFirst
odE)) slots) (returnOk []) \<lbrace>\<lambda>rva s. P s \<and> (\<forall>slot\<in>set slots. \<exists>cte. cteCap cte = capability.NullCap \<and> ctes_of s (f slot) = Some cte)\<rbrace>, -) \<Longrightarrow> \<lbrace>P\<rbrace> injection_handler Inl (doE cte <- liftE (getCTE (f a));
if cteCap cte = capability.NullCap then returnOk () else throwError Fault_H.syscall_error.DeleteFirst
odE) \<lbrace>\<lambda>rv. P and (\<lambda>s. \<exists>cte. cteCap cte = capability.NullCap \<and> ctes_of s (f a) = Some cte)\<rbrace>, -
 2. \<And>a slots P x. (\<And>P. \<lbrace>P\<rbrace> foldr (\<lambda>p q. doE x <- p;
y <- q;
returnOk (() # y)
odE) (map (\<lambda>x. injection_handler Inl (ensureEmptySlot (f x))) slots) (returnOk []) \<lbrace>\<lambda>rva s. P s \<and> (\<forall>slot\<in>set slots. \<exists>cte. cteCap cte = capability.NullCap \<and> ctes_of s (f slot) = Some cte)\<rbrace>, -) \<Longrightarrow> \<lbrace>P and (\<lambda>s. \<exists>cte. cteCap cte = capability.NullCap \<and> ctes_of s (f a) = Some cte)\<rbrace> doE y <- foldr (\<lambda>p q. doE x <- p;
y <- q;
returnOk (() # y)
odE) (map (\<lambda>x. injection_handler Inl (ensureEmptySlot (f x))) slots) (returnOk []);
returnOk (() # y)
odE \<lbrace>\<lambda>rva s. P s \<and> (\<exists>cte. cteCap cte = capability.NullCap \<and> ctes_of s (f a) = Some cte) \<and> (\<forall>slot\<in>set slots. \<exists>cte. cteCap cte = capability.NullCap \<and> ctes_of s (f slot) = Some cte)\<rbrace>, - proof (prove)
goal (2 subgoals):
 1. \<And>a slots P s. \<lbrakk>\<And>P. \<lbrace>P\<rbrace> foldr (\<lambda>p q. doE x <- p;
y <- q;
returnOk (() # y)
odE) (map (\<lambda>x. injection_handler Inl (doE cte <- liftE (getCTE (f x));
if cteCap cte = capability.NullCap then returnOk () else throwError Fault_H.syscall_error.DeleteFirst
odE)) slots) (returnOk []) \<lbrace>\<lambda>rva s. P s \<and> (\<forall>slot\<in>set slots. \<exists>cte. cteCap cte = capability.NullCap \<and> ctes_of s (f slot) = Some cte)\<rbrace>, -; P s\<rbrakk> \<Longrightarrow> \<forall>cte. cte_wp_at' ((=) cte) (f a) s \<longrightarrow> (cteCap cte = capability.NullCap \<longrightarrow> P s \<and> (\<exists>cte. cteCap cte = capability.NullCap \<and> ctes_of s (f a) = Some cte)) \<and> (cteCap cte \<noteq> capability.NullCap \<longrightarrow> True)
 2. \<And>a slots P x. (\<And>P. \<lbrace>P\<rbrace> foldr (\<lambda>p q. doE x <- p;
y <- q;
returnOk (() # y)
odE) (map (\<lambda>x. injection_handler Inl (ensureEmptySlot (f x))) slots) (returnOk []) \<lbrace>\<lambda>rva s. P s \<and> (\<forall>slot\<in>set slots. \<exists>cte. cteCap cte = capability.NullCap \<and> ctes_of s (f slot) = Some cte)\<rbrace>, -) \<Longrightarrow> \<lbrace>P and (\<lambda>s. \<exists>cte. cteCap cte = capability.NullCap \<and> ctes_of s (f a) = Some cte)\<rbrace> doE y <- foldr (\<lambda>p q. doE x <- p;
y <- q;
returnOk (() # y)
odE) (map (\<lambda>x. injection_handler Inl (ensureEmptySlot (f x))) slots) (returnOk []);
returnOk (() # y)
odE \<lbrace>\<lambda>rva s. P s \<and> (\<exists>cte. cteCap cte = capability.NullCap \<and> ctes_of s (f a) = Some cte) \<and> (\<forall>slot\<in>set slots. \<exists>cte. cteCap cte = capability.NullCap \<and> ctes_of s (f slot) = Some cte)\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<And>a slots P x. (\<And>P. \<lbrace>P\<rbrace> foldr (\<lambda>p q. doE x <- p;
y <- q;
returnOk (() # y)
odE) (map (\<lambda>x. injection_handler Inl (ensureEmptySlot (f x))) slots) (returnOk []) \<lbrace>\<lambda>rva s. P s \<and> (\<forall>slot\<in>set slots. \<exists>cte. cteCap cte = capability.NullCap \<and> ctes_of s (f slot) = Some cte)\<rbrace>, -) \<Longrightarrow> \<lbrace>P and (\<lambda>s. \<exists>cte. cteCap cte = capability.NullCap \<and> ctes_of s (f a) = Some cte)\<rbrace> doE y <- foldr (\<lambda>p q. doE x <- p;
y <- q;
returnOk (() # y)
odE) (map (\<lambda>x. injection_handler Inl (ensureEmptySlot (f x))) slots) (returnOk []);
returnOk (() # y)
odE \<lbrace>\<lambda>rva s. P s \<and> (\<exists>cte. cteCap cte = capability.NullCap \<and> ctes_of s (f a) = Some cte) \<and> (\<forall>slot\<in>set slots. \<exists>cte. cteCap cte = capability.NullCap \<and> ctes_of s (f slot) = Some cte)\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<And>a slots P x. \<lbrace>?x25 a slots P x\<rbrace> foldr (\<lambda>p q. doE x <- p;
y <- q;
returnOk (() # y)
odE) (map (\<lambda>x. injection_handler Inl (ensureEmptySlot (f x))) slots) (returnOk []) \<lbrace>\<lambda>rva s. ?x25 a slots P x s \<and> (\<forall>slot\<in>set slots. \<exists>cte. cteCap cte = capability.NullCap \<and> ctes_of s (f slot) = Some cte)\<rbrace>, - \<Longrightarrow> \<lbrace>P and (\<lambda>s. \<exists>cte. cteCap cte = capability.NullCap \<and> ctes_of s (f a) = Some cte)\<rbrace> doE y <- foldr (\<lambda>p q. doE x <- p;
y <- q;
returnOk (() # y)
odE) (map (\<lambda>x. injection_handler Inl (ensureEmptySlot (f x))) slots) (returnOk []);
returnOk (() # y)
odE \<lbrace>\<lambda>rva s. P s \<and> (\<exists>cte. cteCap cte = capability.NullCap \<and> ctes_of s (f a) = Some cte) \<and> (\<forall>slot\<in>set slots. \<exists>cte. cteCap cte = capability.NullCap \<and> ctes_of s (f slot) = Some cte)\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<And>a slots P x. \<lbrace>?x25 a slots P x\<rbrace> foldr (\<lambda>p q. doE x <- p;
y <- q;
returnOk (() # y)
odE) (map (\<lambda>x. injection_handler Inl (ensureEmptySlot (f x))) slots) (returnOk []) \<lbrace>\<lambda>rva s. ?x25 a slots P x s \<and> (\<forall>slot\<in>set slots. \<exists>cte. cteCap cte = capability.NullCap \<and> ctes_of s (f slot) = Some cte)\<rbrace>, - \<Longrightarrow> \<lbrace>P and (\<lambda>s. \<exists>cte. cteCap cte = capability.NullCap \<and> ctes_of s (f a) = Some cte)\<rbrace> foldr (\<lambda>p q. doE x <- p;
y <- q;
returnOk (() # y)
odE) (map (\<lambda>x. injection_handler Inl (ensureEmptySlot (f x))) slots) (returnOk []) \<lbrace>\<lambda>y b. P b \<and> (\<exists>cte. cteCap cte = capability.NullCap \<and> ctes_of b (f a) = Some cte) \<and> (\<forall>slot\<in>set slots. \<exists>cte. cteCap cte = capability.NullCap \<and> ctes_of b (f slot) = Some cte)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>a slots P x. \<lbrace>?x25 a slots P x\<rbrace> foldr (\<lambda>p q. doE x <- p;
y <- q;
returnOk (() # y)
odE) (map (\<lambda>x. injection_handler Inl (ensureEmptySlot (f x))) slots) (returnOk []) \<lbrace>\<lambda>rva s. ?x25 a slots P x s \<and> (\<forall>slot\<in>set slots. \<exists>cte. cteCap cte = capability.NullCap \<and> ctes_of s (f slot) = Some cte)\<rbrace>, - \<Longrightarrow> \<lbrace>P and (\<lambda>s. \<exists>cte. cteCap cte = capability.NullCap \<and> ctes_of s (f a) = Some cte)\<rbrace> foldr (\<lambda>p q. doE x <- p;
y <- q;
returnOk (() # y)
odE) (map (\<lambda>x. injection_handler Inl (ensureEmptySlot (f x))) slots) (returnOk []) \<lbrace>\<lambda>y b. P b \<and> (\<exists>cte. cteCap cte = capability.NullCap \<and> ctes_of b (f a) = Some cte) \<and> (\<forall>slot\<in>set slots. \<exists>cte. cteCap cte = capability.NullCap \<and> ctes_of b (f slot) = Some cte)\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<And>a slots P x rv s. (P and (\<lambda>s. \<exists>cte. cteCap cte = capability.NullCap \<and> ctes_of s (f a) = Some cte)) s \<and> (\<forall>slot\<in>set slots. \<exists>cte. cteCap cte = capability.NullCap \<and> ctes_of s (f slot) = Some cte) \<Longrightarrow> P s \<and> (\<exists>cte. cteCap cte = capability.NullCap \<and> ctes_of s (f a) = Some cte) \<and> (\<forall>slot\<in>set slots. \<exists>cte. cteCap cte = capability.NullCap \<and> ctes_of s (f slot) = Some cte) proof (prove)
goal:
No subgoals!