theory Syscall_R

lemma transferCaps_non_null_cte_wp_at':
  assumes PUC: "\<And>cap. P cap \<Longrightarrow> \<not> isUntypedCap cap"
  shows "\<lbrace>cte_wp_at' (\<lambda>cte. P (cteCap cte) \<and> cteCap cte \<noteq> capability.NullCap) ptr\<rbrace>
     transferCaps info caps ep rcvr rcvBuf
   \<lbrace>\<lambda>_. cte_wp_at' (\<lambda>cte. P (cteCap cte) \<and> cteCap cte \<noteq> capability.NullCap) ptr\<rbrace>" proof - have CTEF: "\<And>P p s. \<lbrakk> cte_wp_at' P p s; \<And>cte. P cte \<Longrightarrow> False \<rbrakk> \<Longrightarrow> False" by (erule cte_wp_atE', auto) show ?thesis unfolding transferCaps_def apply (wp | wpc)+ apply (rule transferCapsToSlots_pres2) apply (rule hoare_weaken_pre [OF cteInsert_weak_cte_wp_at3]) apply (rule PUC,simp) apply (clarsimp simp: cte_wp_at_ctes_of) apply (wp hoare_vcg_all_lift hoare_weak_lift_imp | simp add:ball_conj_distrib)+ done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>cte_wp_at' (\<lambda>cte. P (cteCap cte) \<and> cteCap cte \<noteq> capability.NullCap) ptr\<rbrace> transferCaps info caps ep rcvr rcvBuf \<lbrace>\<lambda>_. cte_wp_at' (\<lambda>cte. P (cteCap cte) \<and> cteCap cte \<noteq> capability.NullCap) ptr\<rbrace> proof (state)
goal (1 subgoal):
 1. \<lbrace>cte_wp_at' (\<lambda>cte. P (cteCap cte) \<and> cteCap cte \<noteq> capability.NullCap) ptr\<rbrace> transferCaps info caps ep rcvr rcvBuf \<lbrace>\<lambda>_. cte_wp_at' (\<lambda>cte. P (cteCap cte) \<and> cteCap cte \<noteq> capability.NullCap) ptr\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>P p s. \<lbrakk>cte_wp_at' P p s; \<And>cte. P cte \<Longrightarrow> False\<rbrakk> \<Longrightarrow> False proof (state)
this:
\<lbrakk>cte_wp_at' ?P ?p ?s; \<And>cte. ?P cte \<Longrightarrow> False\<rbrakk> \<Longrightarrow> False

goal (1 subgoal):
 1. \<lbrace>cte_wp_at' (\<lambda>cte. P (cteCap cte) \<and> cteCap cte \<noteq> capability.NullCap) ptr\<rbrace> transferCaps info caps ep rcvr rcvBuf \<lbrace>\<lambda>_. cte_wp_at' (\<lambda>cte. P (cteCap cte) \<and> cteCap cte \<noteq> capability.NullCap) ptr\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>cte_wp_at' (\<lambda>cte. P (cteCap cte) \<and> cteCap cte \<noteq> capability.NullCap) ptr\<rbrace> transferCaps info caps ep rcvr rcvBuf \<lbrace>\<lambda>_. cte_wp_at' (\<lambda>cte. P (cteCap cte) \<and> cteCap cte \<noteq> capability.NullCap) ptr\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>cte_wp_at' (\<lambda>cte. P (cteCap cte) \<and> cteCap cte \<noteq> capability.NullCap) ptr\<rbrace> do destSlots <- getReceiveSlots rcvr rcvBuf;
info' <- return (msgCapsUnwrapped_update (\<lambda>_. 0) (msgExtraCaps_update (\<lambda>_. 0) info));
case rcvBuf of None \<Rightarrow> return info' | Some rcvBuffer \<Rightarrow> transferCapsToSlots ep rcvBuffer 0 caps destSlots info'
od \<lbrace>\<lambda>_. cte_wp_at' (\<lambda>cte. P (cteCap cte) \<and> cteCap cte \<noteq> capability.NullCap) ptr\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>destSlots info' x2. rcvBuf = Some x2 \<Longrightarrow> \<lbrace>?R12 destSlots info' x2\<rbrace> transferCapsToSlots ep x2 0 caps destSlots info' \<lbrace>\<lambda>_. cte_wp_at' (\<lambda>cte. P (cteCap cte) \<and> cteCap cte \<noteq> capability.NullCap) ptr\<rbrace>
 2. \<And>destSlots. \<lbrace>?B1 destSlots\<rbrace> return (msgCapsUnwrapped_update (\<lambda>_. 0) (msgExtraCaps_update (\<lambda>_. 0) info)) \<lbrace>\<lambda>info' s. (rcvBuf = None \<longrightarrow> cte_wp_at' (\<lambda>cte. P (cteCap cte) \<and> cteCap cte \<noteq> capability.NullCap) ptr s) \<and> (\<forall>x. rcvBuf = Some x \<longrightarrow> ?R12 destSlots info' x s)\<rbrace>
 3. \<lbrace>?Q\<rbrace> getReceiveSlots rcvr rcvBuf \<lbrace>?B1\<rbrace>
 4. \<And>s. cte_wp_at' (\<lambda>cte. P (cteCap cte) \<and> cteCap cte \<noteq> capability.NullCap) ptr s \<Longrightarrow> ?Q s proof (prove)
goal (5 subgoals):
 1. \<And>destSlots info' x2 cap src dest. rcvBuf = Some x2 \<Longrightarrow> \<lbrace>\<lambda>s. cte_wp_at' (\<lambda>cte. P (cteCap cte) \<and> cteCap cte \<noteq> capability.NullCap) ptr s \<and> cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) dest s \<and> ex_cte_cap_wp_to' (\<lambda>_. True) dest s\<rbrace> cteInsert cap src dest \<lbrace>\<lambda>_. cte_wp_at' (\<lambda>cte. P (cteCap cte) \<and> cteCap cte \<noteq> capability.NullCap) ptr\<rbrace>
 2. \<And>destSlots info' x2 b n. rcvBuf = Some x2 \<Longrightarrow> \<lbrace>cte_wp_at' (\<lambda>cte. P (cteCap cte) \<and> cteCap cte \<noteq> capability.NullCap) ptr\<rbrace> setExtraBadge x2 b n \<lbrace>\<lambda>_. cte_wp_at' (\<lambda>cte. P (cteCap cte) \<and> cteCap cte \<noteq> capability.NullCap) ptr\<rbrace>
 3. \<And>destSlots. \<lbrace>?B1 destSlots\<rbrace> return (msgCapsUnwrapped_update (\<lambda>_. 0) (msgExtraCaps_update (\<lambda>_. 0) info)) \<lbrace>\<lambda>info' s. (rcvBuf = None \<longrightarrow> cte_wp_at' (\<lambda>cte. P (cteCap cte) \<and> cteCap cte \<noteq> capability.NullCap) ptr s) \<and> (\<forall>x. rcvBuf = Some x \<longrightarrow> cte_wp_at' (\<lambda>cte. P (cteCap cte) \<and> cteCap cte \<noteq> capability.NullCap) ptr s \<and> (\<forall>x\<in>set destSlots. ex_cte_cap_wp_to' (\<lambda>_. True) x s \<and> cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) x s) \<and> distinct destSlots)\<rbrace>
 4. \<lbrace>?Q\<rbrace> getReceiveSlots rcvr rcvBuf \<lbrace>?B1\<rbrace>
 5. \<And>s. cte_wp_at' (\<lambda>cte. P (cteCap cte) \<and> cteCap cte \<noteq> capability.NullCap) ptr s \<Longrightarrow> ?Q s proof (prove)
goal (6 subgoals):
 1. \<And>destSlots info' x2 cap src dest cte. \<lbrakk>rcvBuf = Some x2; P cte \<and> cte \<noteq> capability.NullCap\<rbrakk> \<Longrightarrow> \<not> isUntypedCap cte
 2. \<And>destSlots info' x2 cap src dest s. \<lbrakk>rcvBuf = Some x2; cte_wp_at' (\<lambda>cte. P (cteCap cte) \<and> cteCap cte \<noteq> capability.NullCap) ptr s \<and> cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) dest s \<and> ex_cte_cap_wp_to' (\<lambda>_. True) dest s\<rbrakk> \<Longrightarrow> if ptr = dest then P cap \<and> cap \<noteq> capability.NullCap else cte_wp_at' (\<lambda>cte. P (cteCap cte) \<and> cteCap cte \<noteq> capability.NullCap) ptr s
 3. \<And>destSlots info' x2 b n. rcvBuf = Some x2 \<Longrightarrow> \<lbrace>cte_wp_at' (\<lambda>cte. P (cteCap cte) \<and> cteCap cte \<noteq> capability.NullCap) ptr\<rbrace> setExtraBadge x2 b n \<lbrace>\<lambda>_. cte_wp_at' (\<lambda>cte. P (cteCap cte) \<and> cteCap cte \<noteq> capability.NullCap) ptr\<rbrace>
 4. \<And>destSlots. \<lbrace>?B1 destSlots\<rbrace> return (msgCapsUnwrapped_update (\<lambda>_. 0) (msgExtraCaps_update (\<lambda>_. 0) info)) \<lbrace>\<lambda>info' s. (rcvBuf = None \<longrightarrow> cte_wp_at' (\<lambda>cte. P (cteCap cte) \<and> cteCap cte \<noteq> capability.NullCap) ptr s) \<and> (\<forall>x. rcvBuf = Some x \<longrightarrow> cte_wp_at' (\<lambda>cte. P (cteCap cte) \<and> cteCap cte \<noteq> capability.NullCap) ptr s \<and> (\<forall>x\<in>set destSlots. ex_cte_cap_wp_to' (\<lambda>_. True) x s \<and> cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) x s) \<and> distinct destSlots)\<rbrace>
 5. \<lbrace>?Q\<rbrace> getReceiveSlots rcvr rcvBuf \<lbrace>?B1\<rbrace>
 6. \<And>s. cte_wp_at' (\<lambda>cte. P (cteCap cte) \<and> cteCap cte \<noteq> capability.NullCap) ptr s \<Longrightarrow> ?Q s proof (prove)
goal (5 subgoals):
 1. \<And>destSlots info' x2 cap src dest s. \<lbrakk>rcvBuf = Some x2; cte_wp_at' (\<lambda>cte. P (cteCap cte) \<and> cteCap cte \<noteq> capability.NullCap) ptr s \<and> cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) dest s \<and> ex_cte_cap_wp_to' (\<lambda>_. True) dest s\<rbrakk> \<Longrightarrow> if ptr = dest then P cap \<and> cap \<noteq> capability.NullCap else cte_wp_at' (\<lambda>cte. P (cteCap cte) \<and> cteCap cte \<noteq> capability.NullCap) ptr s
 2. \<And>destSlots info' x2 b n. rcvBuf = Some x2 \<Longrightarrow> \<lbrace>cte_wp_at' (\<lambda>cte. P (cteCap cte) \<and> cteCap cte \<noteq> capability.NullCap) ptr\<rbrace> setExtraBadge x2 b n \<lbrace>\<lambda>_. cte_wp_at' (\<lambda>cte. P (cteCap cte) \<and> cteCap cte \<noteq> capability.NullCap) ptr\<rbrace>
 3. \<And>destSlots. \<lbrace>?B1 destSlots\<rbrace> return (msgCapsUnwrapped_update (\<lambda>_. 0) (msgExtraCaps_update (\<lambda>_. 0) info)) \<lbrace>\<lambda>info' s. (rcvBuf = None \<longrightarrow> cte_wp_at' (\<lambda>cte. P (cteCap cte) \<and> cteCap cte \<noteq> capability.NullCap) ptr s) \<and> (\<forall>x. rcvBuf = Some x \<longrightarrow> cte_wp_at' (\<lambda>cte. P (cteCap cte) \<and> cteCap cte \<noteq> capability.NullCap) ptr s \<and> (\<forall>x\<in>set destSlots. ex_cte_cap_wp_to' (\<lambda>_. True) x s \<and> cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) x s) \<and> distinct destSlots)\<rbrace>
 4. \<lbrace>?Q\<rbrace> getReceiveSlots rcvr rcvBuf \<lbrace>?B1\<rbrace>
 5. \<And>s. cte_wp_at' (\<lambda>cte. P (cteCap cte) \<and> cteCap cte \<noteq> capability.NullCap) ptr s \<Longrightarrow> ?Q s proof (prove)
goal (4 subgoals):
 1. \<And>destSlots info' x2 b n. rcvBuf = Some x2 \<Longrightarrow> \<lbrace>cte_wp_at' (\<lambda>cte. P (cteCap cte) \<and> cteCap cte \<noteq> capability.NullCap) ptr\<rbrace> setExtraBadge x2 b n \<lbrace>\<lambda>_. cte_wp_at' (\<lambda>cte. P (cteCap cte) \<and> cteCap cte \<noteq> capability.NullCap) ptr\<rbrace>
 2. \<And>destSlots. \<lbrace>?B1 destSlots\<rbrace> return (msgCapsUnwrapped_update (\<lambda>_. 0) (msgExtraCaps_update (\<lambda>_. 0) info)) \<lbrace>\<lambda>info' s. (rcvBuf = None \<longrightarrow> cte_wp_at' (\<lambda>cte. P (cteCap cte) \<and> cteCap cte \<noteq> capability.NullCap) ptr s) \<and> (\<forall>x. rcvBuf = Some x \<longrightarrow> cte_wp_at' (\<lambda>cte. P (cteCap cte) \<and> cteCap cte \<noteq> capability.NullCap) ptr s \<and> (\<forall>x\<in>set destSlots. ex_cte_cap_wp_to' (\<lambda>_. True) x s \<and> cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) x s) \<and> distinct destSlots)\<rbrace>
 3. \<lbrace>?Q\<rbrace> getReceiveSlots rcvr rcvBuf \<lbrace>?B1\<rbrace>
 4. \<And>s. cte_wp_at' (\<lambda>cte. P (cteCap cte) \<and> cteCap cte \<noteq> capability.NullCap) ptr s \<Longrightarrow> ?Q s proof (prove)
goal:
No subgoals! proof (state)
this:
\<lbrace>cte_wp_at' (\<lambda>cte. P (cteCap cte) \<and> cteCap cte \<noteq> capability.NullCap) ptr\<rbrace> transferCaps info caps ep rcvr rcvBuf \<lbrace>\<lambda>_. cte_wp_at' (\<lambda>cte. P (cteCap cte) \<and> cteCap cte \<noteq> capability.NullCap) ptr\<rbrace>

goal:
No subgoals!