theory CNodeInv_R

lemma suspend_not_recursive_ctes:
  "\<lbrace>\<lambda>s. P (not_recursive_ctes s)\<rbrace>
     suspend t
   \<lbrace>\<lambda>rv s. P (not_recursive_ctes s)\<rbrace>" apply (simp only: suspend_def not_recursive_ctes_def cteCaps_of_def) unfolding updateRestartPC_def apply (wp threadSet_ctes_of | simp add: unless_def del: o_apply)+ apply (fold cteCaps_of_def) apply (wp cancelIPC_cteCaps_of) apply (clarsimp elim!: rsubst[where P=P] intro!: set_eqI) apply (clarsimp simp: cte_wp_at_ctes_of cteCaps_of_def) apply (auto simp: isCap_simps finaliseCap_def Let_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (not_recursive_ctes s)\<rbrace> ThreadDecls_H.suspend t \<lbrace>\<lambda>rv s. P (not_recursive_ctes s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P {ptr. \<exists>cap. (map_option cteCap \<circ> ctes_of s) ptr = Some cap \<and> \<not> (isZombie cap \<and> capZombiePtr cap = ptr)}\<rbrace> do cancelIPC t;
state <- getThreadState t;
if state = Structures_H.thread_state.Running then updateRestartPC t else return ();
setThreadState Structures_H.thread_state.Inactive t;
tcbSchedDequeue t
od \<lbrace>\<lambda>rv s. P {ptr. \<exists>cap. (map_option cteCap \<circ> ctes_of s) ptr = Some cap \<and> \<not> (isZombie cap \<and> capZombiePtr cap = ptr)}\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P {ptr. \<exists>cap. (map_option cteCap \<circ> ctes_of s) ptr = Some cap \<and> \<not> (isZombie cap \<and> capZombiePtr cap = ptr)}\<rbrace> do cancelIPC t;
state <- getThreadState t;
if state = Structures_H.thread_state.Running then asUser t (getRegister Thread_H.nextInstructionRegister >>= setRegister Thread_H.faultRegister) else return ();
setThreadState Structures_H.thread_state.Inactive t;
tcbSchedDequeue t
od \<lbrace>\<lambda>rv s. P {ptr. \<exists>cap. (map_option cteCap \<circ> ctes_of s) ptr = Some cap \<and> \<not> (isZombie cap \<and> capZombiePtr cap = ptr)}\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> cancelIPC t \<lbrace>\<lambda>a b. P {ptr. \<exists>cap. (map_option cteCap \<circ> ctes_of b) ptr = Some cap \<and> (isZombie cap \<longrightarrow> capZombiePtr cap \<noteq> ptr)}\<rbrace>
 2. \<And>s. P {ptr. \<exists>cap. (map_option cteCap \<circ> ctes_of s) ptr = Some cap \<and> \<not> (isZombie cap \<and> capZombiePtr cap = ptr)} \<Longrightarrow> ?Q s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> cancelIPC t \<lbrace>\<lambda>a b. P {ptr. \<exists>cap. cteCaps_of b ptr = Some cap \<and> (isZombie cap \<longrightarrow> capZombiePtr cap \<noteq> ptr)}\<rbrace>
 2. \<And>s. P {ptr. \<exists>cap. cteCaps_of s ptr = Some cap \<and> \<not> (isZombie cap \<and> capZombiePtr cap = ptr)} \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. P {ptr. \<exists>cap. cteCaps_of s ptr = Some cap \<and> \<not> (isZombie cap \<and> capZombiePtr cap = ptr)} \<Longrightarrow> (\<forall>p. cte_wp_at' (\<lambda>cte. \<exists>final. global.finaliseCap (cteCap cte) final True \<noteq> fail) p s \<longrightarrow> P {ptr. \<exists>cap. ((cteCaps_of s)(p \<mapsto> capability.NullCap)) ptr = Some cap \<and> (isZombie cap \<longrightarrow> capZombiePtr cap \<noteq> ptr)}) \<and> P {ptr. \<exists>cap. cteCaps_of s ptr = Some cap \<and> (isZombie cap \<longrightarrow> capZombiePtr cap \<noteq> ptr)} proof (prove)
goal (1 subgoal):
 1. \<And>s p x. cte_wp_at' (\<lambda>cte. \<exists>final. global.finaliseCap (cteCap cte) final True \<noteq> fail) p s \<Longrightarrow> (\<exists>cap. cteCaps_of s x = Some cap \<and> (isZombie cap \<longrightarrow> capZombiePtr cap \<noteq> x)) = ((x = p \<longrightarrow> isZombie capability.NullCap \<longrightarrow> capZombiePtr capability.NullCap \<noteq> p) \<and> (x \<noteq> p \<longrightarrow> (\<exists>cap. cteCaps_of s x = Some cap \<and> (isZombie cap \<longrightarrow> capZombiePtr cap \<noteq> x)))) proof (prove)
goal (1 subgoal):
 1. \<And>s p x cte final. \<lbrakk>ctes_of s p = Some cte; global.finaliseCap (cteCap cte) final True \<noteq> fail\<rbrakk> \<Longrightarrow> (\<exists>cap. (\<exists>z. ctes_of s x = Some z \<and> cteCap z = cap) \<and> (isZombie cap \<longrightarrow> capZombiePtr cap \<noteq> x)) = ((x = p \<longrightarrow> isZombie capability.NullCap \<longrightarrow> capZombiePtr capability.NullCap \<noteq> p) \<and> (x \<noteq> p \<longrightarrow> (\<exists>cap. (\<exists>z. ctes_of s x = Some z \<and> cteCap z = cap) \<and> (isZombie cap \<longrightarrow> capZombiePtr cap \<noteq> x)))) proof (prove)
goal:
No subgoals!