theory PageTableDuplicates

lemma handleRecv_valid_duplicates'[wp]:
  "\<lbrace>(\<lambda>s. vs_valid_duplicates' (ksPSpace s))\<rbrace>
  handleRecv isBlocking \<lbrace>\<lambda>r s. vs_valid_duplicates' (ksPSpace s)\<rbrace>" apply (simp add: handleRecv_def cong: if_cong) apply (rule hoare_pre) apply wp apply ((wp getNotification_wp | wpc | simp add: whenE_def split del: if_split)+)[1] apply (rule_tac Q="\<lambda>rv s. vs_valid_duplicates' (ksPSpace s)"

                   in hoare_post_impErr[rotated]) apply (clarsimp simp: isCap_simps sch_act_sane_not) apply assumption apply (wp deleteCallerCap_nonz_cap)+ apply (auto elim: st_tcb_ex_cap'' pred_tcb'_weakenE
             dest!: st_tcb_at_idle_thread'
              simp: ct_in_state'_def sch_act_sane_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. vs_valid_duplicates' (ksPSpace s)\<rbrace> handleRecv isBlocking \<lbrace>\<lambda>r s. vs_valid_duplicates' (ksPSpace s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. vs_valid_duplicates' (ksPSpace s)\<rbrace> do thread <- getCurThread;
epCPtr <- asUser thread (getRegister Thread_H.capRegister);
capFaultOnFailure epCPtr True (doE epCap <- lookupCap thread epCPtr;
case epCap of capability.NotificationCap ntfnPtr x xa True \<Rightarrow> doE ntfn <- withoutFailure $ getNotification ntfnPtr;
boundTCB <- returnOk $ ntfnBoundTCB ntfn;
if boundTCB = Just thread \<or> boundTCB = Nothing then withoutFailure $ receiveSignal thread epCap isBlocking else throw $ Fault_H.lookup_failure.MissingCapability 0
odE | capability.NotificationCap ntfnPtr x xa False \<Rightarrow> throw $ Fault_H.lookup_failure.MissingCapability 0 | capability.EndpointCap x xa xb True xc xd \<Rightarrow> withoutFailure $ do deleteCallerCap thread;
receiveIPC thread epCap isBlocking
od | capability.EndpointCap x xa xb False xc xd \<Rightarrow> throw $ Fault_H.lookup_failure.MissingCapability 0 | _ \<Rightarrow> throw $ Fault_H.lookup_failure.MissingCapability 0
odE) <catch> handleFault thread
od \<lbrace>\<lambda>r s. vs_valid_duplicates' (ksPSpace s)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> do thread <- getCurThread;
epCPtr <- asUser thread (getRegister Thread_H.capRegister);
capFaultOnFailure epCPtr True (doE epCap <- lookupCap thread epCPtr;
case epCap of capability.NotificationCap ntfnPtr x xa True \<Rightarrow> doE ntfn <- withoutFailure $ getNotification ntfnPtr;
boundTCB <- returnOk $ ntfnBoundTCB ntfn;
if boundTCB = Just thread \<or> boundTCB = Nothing then withoutFailure $ receiveSignal thread epCap isBlocking else throw $ Fault_H.lookup_failure.MissingCapability 0
odE | capability.NotificationCap ntfnPtr x xa False \<Rightarrow> throw $ Fault_H.lookup_failure.MissingCapability 0 | capability.EndpointCap x xa xb True xc xd \<Rightarrow> withoutFailure $ do deleteCallerCap thread;
receiveIPC thread epCap isBlocking
od | capability.EndpointCap x xa xb False xc xd \<Rightarrow> throw $ Fault_H.lookup_failure.MissingCapability 0 | _ \<Rightarrow> throw $ Fault_H.lookup_failure.MissingCapability 0
odE) <catch> handleFault thread
od \<lbrace>\<lambda>r s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 2. \<And>s. vs_valid_duplicates' (ksPSpace s) \<Longrightarrow> ?Q s proof (prove)
goal (5 subgoals):
 1. \<And>thread epCPtr epCap. \<lbrace>?B9 thread epCPtr epCap\<rbrace> case epCap of capability.NotificationCap ntfnPtr x xa True \<Rightarrow> doE ntfn <- withoutFailure $ getNotification ntfnPtr;
boundTCB <- returnOk $ ntfnBoundTCB ntfn;
if boundTCB = Just thread \<or> boundTCB = Nothing then withoutFailure $ receiveSignal thread epCap isBlocking else throw $ Fault_H.lookup_failure.MissingCapability 0
odE | capability.NotificationCap ntfnPtr x xa False \<Rightarrow> throw $ Fault_H.lookup_failure.MissingCapability 0 | capability.EndpointCap x xa xb True xc xd \<Rightarrow> withoutFailure $ do deleteCallerCap thread;
receiveIPC thread epCap isBlocking
od | capability.EndpointCap x xa xb False xc xd \<Rightarrow> throw $ Fault_H.lookup_failure.MissingCapability 0 | _ \<Rightarrow> throw $ Fault_H.lookup_failure.MissingCapability 0 \<lbrace>\<lambda>r s. vs_valid_duplicates' (ksPSpace s)\<rbrace>, \<lbrace>\<lambda>ft s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 2. \<And>thread epCPtr. \<lbrace>?B5 thread epCPtr\<rbrace> lookupCap thread epCPtr \<lbrace>?B9 thread epCPtr\<rbrace>, \<lbrace>\<lambda>ft s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 3. \<And>thread. \<lbrace>?B4 thread\<rbrace> asUser thread (getRegister Thread_H.capRegister) \<lbrace>?B5 thread\<rbrace>
 4. \<lbrace>?Q\<rbrace> getCurThread \<lbrace>?B4\<rbrace>
 5. \<And>s. vs_valid_duplicates' (ksPSpace s) \<Longrightarrow> ?Q s proof (prove)
goal (4 subgoals):
 1. \<And>thread epCPtr. \<lbrace>?B5 thread epCPtr\<rbrace> lookupCap thread epCPtr \<lbrace>\<lambda>epCap s. (\<forall>x. epCap = capability.ThreadCap x \<longrightarrow> vs_valid_duplicates' (ksPSpace s) \<and> True) \<and> (epCap = capability.NullCap \<longrightarrow> vs_valid_duplicates' (ksPSpace s) \<and> True) \<and> (\<forall>x xa xb xc. epCap = capability.NotificationCap x xa xb xc \<longrightarrow> (xc = True \<longrightarrow> True \<and> (\<forall>ntfn. ko_at' ntfn x s \<longrightarrow> True \<and> (ntfnBoundTCB ntfn = Just thread \<or> ntfnBoundTCB ntfn = Nothing \<longrightarrow> True \<and> vs_valid_duplicates' (ksPSpace s)) \<and> (\<not> (ntfnBoundTCB ntfn = Just thread \<or> ntfnBoundTCB ntfn = Nothing) \<longrightarrow> vs_valid_duplicates' (ksPSpace s) \<and> True))) \<and> (xc = False \<longrightarrow> vs_valid_duplicates' (ksPSpace s) \<and> True)) \<and> (\<forall>x. epCap = capability.IRQHandlerCap x \<longrightarrow> vs_valid_duplicates' (ksPSpace s) \<and> True) \<and> (\<forall>x xa xb xc xd xe. epCap = capability.EndpointCap x xa xb xc xd xe \<longrightarrow> (xc = True \<longrightarrow> True \<and> vs_valid_duplicates' (ksPSpace s)) \<and> (xc = False \<longrightarrow> vs_valid_duplicates' (ksPSpace s) \<and> True)) \<and> (epCap = capability.DomainCap \<longrightarrow> vs_valid_duplicates' (ksPSpace s) \<and> True) \<and> (\<forall>x xa xb. epCap = capability.Zombie x xa xb \<longrightarrow> vs_valid_duplicates' (ksPSpace s) \<and> True) \<and> (\<forall>x. epCap = capability.ArchObjectCap x \<longrightarrow> vs_valid_duplicates' (ksPSpace s) \<and> True) \<and> (\<forall>x xa xb. epCap = capability.ReplyCap x xa xb \<longrightarrow> vs_valid_duplicates' (ksPSpace s) \<and> True) \<and> (\<forall>x xa xb xc. epCap = capability.UntypedCap x xa xb xc \<longrightarrow> vs_valid_duplicates' (ksPSpace s) \<and> True) \<and> (\<forall>x xa xb xc. epCap = capability.CNodeCap x xa xb xc \<longrightarrow> vs_valid_duplicates' (ksPSpace s) \<and> True) \<and> (epCap = capability.IRQControlCap \<longrightarrow> vs_valid_duplicates' (ksPSpace s) \<and> True)\<rbrace>, \<lbrace>\<lambda>ft s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 2. \<And>thread. \<lbrace>?B4 thread\<rbrace> asUser thread (getRegister Thread_H.capRegister) \<lbrace>?B5 thread\<rbrace>
 3. \<lbrace>?Q\<rbrace> getCurThread \<lbrace>?B4\<rbrace>
 4. \<And>s. vs_valid_duplicates' (ksPSpace s) \<Longrightarrow> ?Q s proof (prove)
goal (6 subgoals):
 1. \<And>thread epCPtr rv s. vs_valid_duplicates' (ksPSpace s) \<Longrightarrow> (\<forall>x. rv = capability.ThreadCap x \<longrightarrow> vs_valid_duplicates' (ksPSpace s) \<and> True) \<and> (rv = capability.NullCap \<longrightarrow> vs_valid_duplicates' (ksPSpace s) \<and> True) \<and> (\<forall>x xa xb xc. rv = capability.NotificationCap x xa xb xc \<longrightarrow> (xc = True \<longrightarrow> True \<and> (\<forall>ntfn. ko_at' ntfn x s \<longrightarrow> True \<and> (ntfnBoundTCB ntfn = Just thread \<or> ntfnBoundTCB ntfn = Nothing \<longrightarrow> True \<and> vs_valid_duplicates' (ksPSpace s)) \<and> (\<not> (ntfnBoundTCB ntfn = Just thread \<or> ntfnBoundTCB ntfn = Nothing) \<longrightarrow> vs_valid_duplicates' (ksPSpace s) \<and> True))) \<and> (xc = False \<longrightarrow> vs_valid_duplicates' (ksPSpace s) \<and> True)) \<and> (\<forall>x. rv = capability.IRQHandlerCap x \<longrightarrow> vs_valid_duplicates' (ksPSpace s) \<and> True) \<and> (\<forall>x xa xb xc xd xe. rv = capability.EndpointCap x xa xb xc xd xe \<longrightarrow> (xc = True \<longrightarrow> True \<and> vs_valid_duplicates' (ksPSpace s)) \<and> (xc = False \<longrightarrow> vs_valid_duplicates' (ksPSpace s) \<and> True)) \<and> (rv = capability.DomainCap \<longrightarrow> vs_valid_duplicates' (ksPSpace s) \<and> True) \<and> (\<forall>x xa xb. rv = capability.Zombie x xa xb \<longrightarrow> vs_valid_duplicates' (ksPSpace s) \<and> True) \<and> (\<forall>x. rv = capability.ArchObjectCap x \<longrightarrow> vs_valid_duplicates' (ksPSpace s) \<and> True) \<and> (\<forall>x xa xb. rv = capability.ReplyCap x xa xb \<longrightarrow> vs_valid_duplicates' (ksPSpace s) \<and> True) \<and> (\<forall>x xa xb xc. rv = capability.UntypedCap x xa xb xc \<longrightarrow> vs_valid_duplicates' (ksPSpace s) \<and> True) \<and> (\<forall>x xa xb xc. rv = capability.CNodeCap x xa xb xc \<longrightarrow> vs_valid_duplicates' (ksPSpace s) \<and> True) \<and> (rv = capability.IRQControlCap \<longrightarrow> vs_valid_duplicates' (ksPSpace s) \<and> True)
 2. \<And>thread epCPtr e s. ?E316 thread epCPtr e s \<Longrightarrow> vs_valid_duplicates' (ksPSpace s)
 3. \<And>thread epCPtr. \<lbrace>?B5 thread epCPtr\<rbrace> lookupCap thread epCPtr \<lbrace>\<lambda>rv s. vs_valid_duplicates' (ksPSpace s)\<rbrace>, \<lbrace>?E316 thread epCPtr\<rbrace>
 4. \<And>thread. \<lbrace>?B4 thread\<rbrace> asUser thread (getRegister Thread_H.capRegister) \<lbrace>?B5 thread\<rbrace>
 5. \<lbrace>?Q\<rbrace> getCurThread \<lbrace>?B4\<rbrace>
 6. \<And>s. vs_valid_duplicates' (ksPSpace s) \<Longrightarrow> ?Q s proof (prove)
goal (5 subgoals):
 1. \<And>thread epCPtr e s. ?E316 thread epCPtr e s \<Longrightarrow> vs_valid_duplicates' (ksPSpace s)
 2. \<And>thread epCPtr. \<lbrace>?B5 thread epCPtr\<rbrace> lookupCap thread epCPtr \<lbrace>\<lambda>rv s. vs_valid_duplicates' (ksPSpace s)\<rbrace>, \<lbrace>?E316 thread epCPtr\<rbrace>
 3. \<And>thread. \<lbrace>?B4 thread\<rbrace> asUser thread (getRegister Thread_H.capRegister) \<lbrace>?B5 thread\<rbrace>
 4. \<lbrace>?Q\<rbrace> getCurThread \<lbrace>?B4\<rbrace>
 5. \<And>s. vs_valid_duplicates' (ksPSpace s) \<Longrightarrow> ?Q s proof (prove)
goal (4 subgoals):
 1. \<And>thread epCPtr. \<lbrace>?B5 thread epCPtr\<rbrace> lookupCap thread epCPtr \<lbrace>\<lambda>rv s. vs_valid_duplicates' (ksPSpace s)\<rbrace>, \<lbrace>\<lambda>e s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 2. \<And>thread. \<lbrace>?B4 thread\<rbrace> asUser thread (getRegister Thread_H.capRegister) \<lbrace>?B5 thread\<rbrace>
 3. \<lbrace>?Q\<rbrace> getCurThread \<lbrace>?B4\<rbrace>
 4. \<And>s. vs_valid_duplicates' (ksPSpace s) \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. vs_valid_duplicates' (ksPSpace s) \<Longrightarrow> vs_valid_duplicates' (ksPSpace s) \<and> vs_valid_duplicates' (ksPSpace s) proof (prove)
goal:
No subgoals!