theory Ipc_C

lemma cteDeleteOne_tcbFault:
  "\<lbrace>obj_at' (\<lambda>tcb. P (tcbFault tcb)) t\<rbrace>
  cteDeleteOne slot
  \<lbrace>\<lambda>_. obj_at' (\<lambda>tcb. P (tcbFault tcb)) t\<rbrace>" apply (simp add: cteDeleteOne_def unless_when split_def) apply (simp add: finaliseCapTrue_standin_def Let_def) apply (rule hoare_pre) apply (wp emptySlot_tcbFault cancelAllIPC_tcbFault getCTE_wp'
            cancelAllSignals_tcbFault unbindNotification_tcbFault
            isFinalCapability_inv unbindMaybeNotification_tcbFault
            hoare_weak_lift_imp
          | wpc | simp add: Let_def)+ apply (clarsimp split: if_split) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>obj_at' (\<lambda>tcb. P (tcbFault tcb)) t\<rbrace> cteDeleteOne slot \<lbrace>\<lambda>_. obj_at' (\<lambda>tcb. P (tcbFault tcb)) t\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>obj_at' (\<lambda>tcb. P (tcbFault tcb)) t\<rbrace> do cte <- getCTE slot;
when (cteCap cte \<noteq> capability.NullCap) (do final <- isFinalCapability cte;
p <- finaliseCapTrue_standin (cteCap cte) final;
y <- assert (capRemovable (fst p) slot \<and> snd p = capability.NullCap);
emptySlot slot capability.NullCap
od)
od \<lbrace>\<lambda>_. obj_at' (\<lambda>tcb. P (tcbFault tcb)) t\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>obj_at' (\<lambda>tcb. P (tcbFault tcb)) t\<rbrace> do cte <- getCTE slot;
when (cteCap cte \<noteq> capability.NullCap) (do final <- isFinalCapability cte;
p <- if isEndpointCap (cteCap cte) then do y <- when final (cancelAllIPC (capEPPtr (cteCap cte)));
return (capability.NullCap, capability.NullCap)
od else if isNotificationCap (cteCap cte) then let ptr = capNtfnPtr (cteCap cte) in do y <- when final (do y <- unbindMaybeNotification ptr;
cancelAllSignals ptr
od);
return (capability.NullCap, capability.NullCap)
od else if isReplyCap (cteCap cte) then return (capability.NullCap, capability.NullCap) else if cteCap cte = capability.NullCap then return (capability.NullCap, capability.NullCap) else if cteCap cte = capability.DomainCap then return (capability.NullCap, capability.NullCap) else fail;
y <- assert (capRemovable (fst p) slot \<and> snd p = capability.NullCap);
emptySlot slot capability.NullCap
od)
od \<lbrace>\<lambda>_. obj_at' (\<lambda>tcb. P (tcbFault tcb)) t\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> do cte <- getCTE slot;
when (cteCap cte \<noteq> capability.NullCap) (do final <- isFinalCapability cte;
p <- if isEndpointCap (cteCap cte) then do y <- when final (cancelAllIPC (capEPPtr (cteCap cte)));
return (capability.NullCap, capability.NullCap)
od else if isNotificationCap (cteCap cte) then let ptr = capNtfnPtr (cteCap cte) in do y <- when final (do y <- unbindMaybeNotification ptr;
cancelAllSignals ptr
od);
return (capability.NullCap, capability.NullCap)
od else if isReplyCap (cteCap cte) then return (capability.NullCap, capability.NullCap) else if cteCap cte = capability.NullCap then return (capability.NullCap, capability.NullCap) else if cteCap cte = capability.DomainCap then return (capability.NullCap, capability.NullCap) else fail;
y <- assert (capRemovable (fst p) slot \<and> snd p = capability.NullCap);
emptySlot slot capability.NullCap
od)
od \<lbrace>\<lambda>_. obj_at' (\<lambda>tcb. P (tcbFault tcb)) t\<rbrace>
 2. \<And>s. obj_at' (\<lambda>tcb. P (tcbFault tcb)) t s \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. obj_at' (\<lambda>tcb. P (tcbFault tcb)) t s \<Longrightarrow> \<forall>cte. cte_wp_at' ((=) cte) slot s \<longrightarrow> (if cteCap cte \<noteq> capability.NullCap then \<lambda>s. (isEndpointCap (cteCap cte) \<longrightarrow> capRemovable (fst (capability.NullCap, capability.NullCap)) slot \<and> snd (capability.NullCap, capability.NullCap) = capability.NullCap \<longrightarrow> obj_at' (\<lambda>tcb. P (tcbFault tcb)) t s) \<and> (\<not> isEndpointCap (cteCap cte) \<longrightarrow> (isNotificationCap (cteCap cte) \<longrightarrow> capRemovable (fst (capability.NullCap, capability.NullCap)) slot \<and> snd (capability.NullCap, capability.NullCap) = capability.NullCap \<longrightarrow> obj_at' (\<lambda>tcb. P (tcbFault tcb)) t s) \<and> (\<not> isNotificationCap (cteCap cte) \<longrightarrow> (isReplyCap (cteCap cte) \<longrightarrow> capRemovable (fst (capability.NullCap, capability.NullCap)) slot \<and> snd (capability.NullCap, capability.NullCap) = capability.NullCap \<longrightarrow> obj_at' (\<lambda>tcb. P (tcbFault tcb)) t s) \<and> (\<not> isReplyCap (cteCap cte) \<longrightarrow> (cteCap cte = capability.NullCap \<longrightarrow> capRemovable (fst (capability.NullCap, capability.NullCap)) slot \<and> snd (capability.NullCap, capability.NullCap) = capability.NullCap \<longrightarrow> obj_at' (\<lambda>tcb. P (tcbFault tcb)) t s) \<and> (cteCap cte \<noteq> capability.NullCap \<longrightarrow> (cteCap cte = capability.DomainCap \<longrightarrow> capRemovable (fst (capability.NullCap, capability.NullCap)) slot \<and> snd (capability.NullCap, capability.NullCap) = capability.NullCap \<longrightarrow> obj_at' (\<lambda>tcb. P (tcbFault tcb)) t s) \<and> (cteCap cte \<noteq> capability.DomainCap \<longrightarrow> True))))) else obj_at' (\<lambda>tcb. P (tcbFault tcb)) t) s proof (prove)
goal:
No subgoals!