kings-crown/FVELER_Isabelle huggingface dataset:
theory Orphanage

lemma bindNotification_no_orphans[wp]:
  "\<lbrace>no_orphans\<rbrace> bindNotification t ntfn \<lbrace>\<lambda>_. no_orphans\<rbrace>" unfolding bindNotification_def by wp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>no_orphans\<rbrace> bindNotification t ntfn \<lbrace>\<lambda>_. no_orphans\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>no_orphans\<rbrace> do ntfna <- getNotification ntfn;
setNotification ntfn $ ntfnBoundTCB_update (\<lambda>_. Just t) ntfna;
setBoundNotification (Just ntfn) t
od \<lbrace>\<lambda>_. no_orphans\<rbrace>
theory Orphanage

lemma invokeIRQControl_no_orphans [wp]:
  "\<lbrace> \<lambda>s. no_orphans s \<rbrace>
   performIRQControl i
   \<lbrace> \<lambda>rv s. no_orphans s \<rbrace>" apply (cases i, simp_all add: performIRQControl_def ARM_H.performIRQControl_def) apply (rename_tac archinv) apply (case_tac archinv) apply (wp | clarsimp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>no_orphans\<rbrace> global.performIRQControl i \<lbrace>\<lambda>rv. no_orphans\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x1. i = irqcontrol_invocation.ArchIRQControl x1 \<Longrightarrow> \<lbrace>no_orphans\<rbrace> case x1 of local.irqcontrol_invocation.IssueIRQHandler irq destSlot srcSlot trigger \<Rightarrow> withoutPreemption $ do doMachineOp $ setIRQTrigger irq trigger;
setIRQState irqstate.IRQSignal (IRQ irq);
cteInsert (capability.IRQHandlerCap (IRQ irq)) srcSlot destSlot;
return ()
od \<lbrace>\<lambda>rv. no_orphans\<rbrace>
 2. \<And>x21 x22 x23. i = Invocations_H.irqcontrol_invocation.IssueIRQHandler x21 x22 x23 \<Longrightarrow> \<lbrace>no_orphans\<rbrace> liftE (do y <- setIRQState irqstate.IRQSignal x21;
cteInsert (capability.IRQHandlerCap x21) x23 x22
od) \<lbrace>\<lambda>rv. no_orphans\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>archinv. i = irqcontrol_invocation.ArchIRQControl archinv \<Longrightarrow> \<lbrace>no_orphans\<rbrace> case archinv of local.irqcontrol_invocation.IssueIRQHandler irq destSlot srcSlot trigger \<Rightarrow> withoutPreemption $ do doMachineOp $ setIRQTrigger irq trigger;
setIRQState irqstate.IRQSignal (IRQ irq);
cteInsert (capability.IRQHandlerCap (IRQ irq)) srcSlot destSlot;
return ()
od \<lbrace>\<lambda>rv. no_orphans\<rbrace>
 2. \<And>x21 x22 x23. i = Invocations_H.irqcontrol_invocation.IssueIRQHandler x21 x22 x23 \<Longrightarrow> \<lbrace>no_orphans\<rbrace> liftE (do y <- setIRQState irqstate.IRQSignal x21;
cteInsert (capability.IRQHandlerCap x21) x23 x22
od) \<lbrace>\<lambda>rv. no_orphans\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>archinv x1 x2 x3 x4. \<lbrakk>i = irqcontrol_invocation.ArchIRQControl archinv; archinv = local.irqcontrol_invocation.IssueIRQHandler x1 x2 x3 x4\<rbrakk> \<Longrightarrow> \<lbrace>no_orphans\<rbrace> case archinv of local.irqcontrol_invocation.IssueIRQHandler irq destSlot srcSlot trigger \<Rightarrow> withoutPreemption $ do doMachineOp $ setIRQTrigger irq trigger;
setIRQState irqstate.IRQSignal (IRQ irq);
cteInsert (capability.IRQHandlerCap (IRQ irq)) srcSlot destSlot;
return ()
od \<lbrace>\<lambda>rv. no_orphans\<rbrace>
 2. \<And>x21 x22 x23. i = Invocations_H.irqcontrol_invocation.IssueIRQHandler x21 x22 x23 \<Longrightarrow> \<lbrace>no_orphans\<rbrace> liftE (do y <- setIRQState irqstate.IRQSignal x21;
cteInsert (capability.IRQHandlerCap x21) x23 x22
od) \<lbrace>\<lambda>rv. no_orphans\<rbrace> proof (prove)
goal:
No subgoals!
theory Orphanage

lemma invokeIRQHandler_no_orphans [wp]:
  "\<lbrace> \<lambda>s. no_orphans s \<and> invs' s \<rbrace>
   invokeIRQHandler i
   \<lbrace> \<lambda>reply s. no_orphans s \<rbrace>" apply (cases i, simp_all add: invokeIRQHandler_def) apply (wp | clarsimp | fastforce)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. no_orphans s \<and> invs' s\<rbrace> local.invokeIRQHandler i \<lbrace>\<lambda>reply. no_orphans\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>x1. i = AckIRQ x1 \<Longrightarrow> \<lbrace>\<lambda>s. no_orphans s \<and> invs' s\<rbrace> doMachineOp (maskInterrupt False x1) \<lbrace>\<lambda>reply. no_orphans\<rbrace>
 2. \<And>x2. i = irqhandler_invocation.ClearIRQHandler x2 \<Longrightarrow> \<lbrace>\<lambda>s. no_orphans s \<and> invs' s\<rbrace> return () \<lbrace>\<lambda>reply. no_orphans\<rbrace>
 3. \<And>x31 x32 x33. i = irqhandler_invocation.SetIRQHandler x31 x32 x33 \<Longrightarrow> \<lbrace>\<lambda>s. no_orphans s \<and> invs' s\<rbrace> return () \<lbrace>\<lambda>reply. no_orphans\<rbrace> proof (prove)
goal:
No subgoals!
theory Orphanage

lemma performPageTableInvocation_no_orphans [wp]:
  "\<lbrace> \<lambda>s. no_orphans s \<rbrace>
   performPageTableInvocation pti
   \<lbrace> \<lambda>reply s. no_orphans s \<rbrace>" apply (cases pti, simp_all add: performPageTableInvocation_def) apply (rule hoare_pre) apply (wp mapM_x_wp' | wpc | clarsimp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>no_orphans\<rbrace> performPageTableInvocation pti \<lbrace>\<lambda>reply. no_orphans\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x11 x12. pti = ARM_H.PageTableUnmap x11 x12 \<Longrightarrow> \<lbrace>no_orphans\<rbrace> do y <- case capPTMappedAddress x11 of None \<Rightarrow> return () | Some (asid, vaddr) \<Rightarrow> do y <- unmapPageTable asid vaddr (capPTBasePtr x11);
y <- mapM_x (swp storePTE ARM_H.InvalidPTE) [capPTBasePtr x11 , capPTBasePtr x11 + 2 ^ pteBits .e. capPTBasePtr x11 + 2 ^ ptBits - 1];
doMachineOp (cleanCacheRange_PoU (capPTBasePtr x11) (capPTBasePtr x11 + 2 ^ ptBits - 1) (addrFromPPtr (capPTBasePtr x11)))
od;
cap <- liftM capCap (getSlotCap x12);
updateCap x12 (capability.ArchObjectCap (capPTMappedAddress_update (\<lambda>_. None) cap))
od \<lbrace>\<lambda>reply. no_orphans\<rbrace>
 2. \<And>x21 x22 x23 x24. pti = ARM_H.PageTableMap x21 x22 x23 x24 \<Longrightarrow> \<lbrace>no_orphans\<rbrace> do y <- updateCap x22 x21;
y <- storePDE x24 x23;
doMachineOp (cleanByVA_PoU x24 (addrFromPPtr x24))
od \<lbrace>\<lambda>reply. no_orphans\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>x11 x12. pti = ARM_H.PageTableUnmap x11 x12 \<Longrightarrow> \<lbrace>?Q8 x11 x12\<rbrace> do y <- case capPTMappedAddress x11 of None \<Rightarrow> return () | Some (asid, vaddr) \<Rightarrow> do y <- unmapPageTable asid vaddr (capPTBasePtr x11);
y <- mapM_x (swp storePTE ARM_H.InvalidPTE) [capPTBasePtr x11 , capPTBasePtr x11 + 2 ^ pteBits .e. capPTBasePtr x11 + 2 ^ ptBits - 1];
doMachineOp (cleanCacheRange_PoU (capPTBasePtr x11) (capPTBasePtr x11 + 2 ^ ptBits - 1) (addrFromPPtr (capPTBasePtr x11)))
od;
cap <- liftM capCap (getSlotCap x12);
updateCap x12 (capability.ArchObjectCap (capPTMappedAddress_update (\<lambda>_. None) cap))
od \<lbrace>\<lambda>reply. no_orphans\<rbrace>
 2. \<And>x11 x12 s. \<lbrakk>pti = ARM_H.PageTableUnmap x11 x12; no_orphans s\<rbrakk> \<Longrightarrow> ?Q8 x11 x12 s
 3. \<And>x21 x22 x23 x24. pti = ARM_H.PageTableMap x21 x22 x23 x24 \<Longrightarrow> \<lbrace>no_orphans\<rbrace> do y <- updateCap x22 x21;
y <- storePDE x24 x23;
doMachineOp (cleanByVA_PoU x24 (addrFromPPtr x24))
od \<lbrace>\<lambda>reply. no_orphans\<rbrace> proof (prove)
goal:
No subgoals!
theory Orphanage

lemma performASIDPoolInvocation_no_orphans [wp]:
  "\<lbrace> \<lambda>s. no_orphans s \<rbrace>
   performASIDPoolInvocation api
   \<lbrace> \<lambda>reply s. no_orphans s \<rbrace>" apply (cases api, simp_all add: performASIDPoolInvocation_def) apply (wp getObject_inv loadObject_default_inv | clarsimp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>no_orphans\<rbrace> performASIDPoolInvocation api \<lbrace>\<lambda>reply. no_orphans\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2 x3. api = asidpool_invocation.Assign x1 x2 x3 \<Longrightarrow> \<lbrace>no_orphans\<rbrace> do oldcap <- getSlotCap x3;
pool <- liftM (inv asidpool.ASIDPool) (getObject x2);
y <- updateCap x3 (capability.ArchObjectCap (capPDMappedASID_update (\<lambda>_. Some x1) (capCap oldcap)));
setObject x2 (asidpool.ASIDPool (pool(x1 && mask local.asid_low_bits \<mapsto> capPDBasePtr (capCap oldcap))))
od \<lbrace>\<lambda>reply. no_orphans\<rbrace> proof (prove)
goal:
No subgoals!
theory Orphanage

lemma performPageDirectoryInvocation_no_orphans [wp]:
  "\<lbrace> \<lambda>s. no_orphans s \<rbrace>
   performPageDirectoryInvocation pdi
   \<lbrace> \<lambda>reply s. no_orphans s \<rbrace>" apply (cases pdi, simp_all add: performPageDirectoryInvocation_def) apply (wp | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>no_orphans\<rbrace> performPageDirectoryInvocation pdi \<lbrace>\<lambda>reply. no_orphans\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x21 x22 x23 x24 x25 x26. pdi = ARM_H.PageDirectoryFlush x21 x22 x23 x24 x25 x26 \<Longrightarrow> \<lbrace>no_orphans\<rbrace> when (x22 < x23) (do root_switched <- setVMRootForFlush x25 x26;
y <- doMachineOp (doFlush x21 x22 x23 x24);
when root_switched (getCurThread >>= setVMRoot)
od) \<lbrace>\<lambda>reply. no_orphans\<rbrace> proof (prove)
goal:
No subgoals!
theory Orphanage

lemma arch_performInvocation_no_orphans [wp]:
  "\<lbrace> \<lambda>s. no_orphans s \<and> invs' s \<and> valid_arch_inv' i s \<and> ct_active' s \<rbrace>
   Arch.performInvocation i
   \<lbrace> \<lambda>reply s. no_orphans s \<rbrace>" unfolding ARM_H.performInvocation_def performARMMMUInvocation_def apply (cases i, simp_all add: valid_arch_inv'_def) apply (wp | clarsimp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. no_orphans s \<and> invs' s \<and> valid_arch_inv' i s \<and> ct_active' s\<rbrace> Arch.performInvocation i \<lbrace>\<lambda>reply. no_orphans\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. no_orphans s \<and> invs' s \<and> valid_arch_inv' i s \<and> ct_active' s\<rbrace> withoutPreemption $ case i of invocation.InvokePageTable oper \<Rightarrow> do performPageTableInvocation oper;
return []
od | invocation.InvokePageDirectory oper \<Rightarrow> do performPageDirectoryInvocation oper;
return []
od | invocation.InvokePage oper \<Rightarrow> performPageInvocation oper | invocation.InvokeASIDControl oper \<Rightarrow> do performASIDControlInvocation oper;
return []
od | invocation.InvokeASIDPool oper \<Rightarrow> do performASIDPoolInvocation oper;
return []
od \<lbrace>\<lambda>reply. no_orphans\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>x1. i = invocation.InvokePageTable x1 \<Longrightarrow> \<lbrace>\<lambda>s. no_orphans s \<and> invs' s \<and> valid_pti' x1 s \<and> ct_active' s\<rbrace> liftE (do y <- performPageTableInvocation x1;
return []
od) \<lbrace>\<lambda>reply. no_orphans\<rbrace>
 2. \<And>x2. i = invocation.InvokePageDirectory x2 \<Longrightarrow> \<lbrace>\<lambda>s. no_orphans s \<and> invs' s \<and> ct_active' s\<rbrace> liftE (do y <- performPageDirectoryInvocation x2;
return []
od) \<lbrace>\<lambda>reply. no_orphans\<rbrace>
 3. \<And>x3. i = invocation.InvokePage x3 \<Longrightarrow> \<lbrace>\<lambda>s. no_orphans s \<and> invs' s \<and> valid_page_inv' x3 s \<and> ct_active' s\<rbrace> liftE (performPageInvocation x3) \<lbrace>\<lambda>reply. no_orphans\<rbrace>
 4. \<And>x4. i = invocation.InvokeASIDControl x4 \<Longrightarrow> \<lbrace>\<lambda>s. no_orphans s \<and> invs' s \<and> valid_aci' x4 s \<and> ct_active' s\<rbrace> liftE (do y <- performASIDControlInvocation x4;
return []
od) \<lbrace>\<lambda>reply. no_orphans\<rbrace>
 5. \<And>x5. i = invocation.InvokeASIDPool x5 \<Longrightarrow> \<lbrace>\<lambda>s. no_orphans s \<and> invs' s \<and> valid_apinv' x5 s \<and> ct_active' s\<rbrace> liftE (do y <- performASIDPoolInvocation x5;
return []
od) \<lbrace>\<lambda>reply. no_orphans\<rbrace> proof (prove)
goal:
No subgoals!
theory Orphanage

lemma getThreadState_restart [wp]:
  "\<lbrace> \<lambda>s. tcb_at' thread s \<rbrace>
   getThreadState thread
   \<lbrace> \<lambda>rv s. rv = Structures_H.thread_state.Restart \<longrightarrow> st_tcb_at' isRestart thread s \<rbrace>" apply (rule hoare_strengthen_post) apply (rule gts_st_tcb') apply (clarsimp simp add: pred_tcb_at'_def obj_at'_def isRestart_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>tcb_at' thread\<rbrace> getThreadState thread \<lbrace>\<lambda>rv s. rv = Structures_H.thread_state.Restart \<longrightarrow> st_tcb_at' isRestart thread s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>tcb_at' thread\<rbrace> getThreadState thread \<lbrace>?Q\<rbrace>
 2. \<And>rv s. ?Q rv s \<Longrightarrow> rv = Structures_H.thread_state.Restart \<longrightarrow> st_tcb_at' isRestart thread s proof (prove)
goal (1 subgoal):
 1. \<And>rv s. st_tcb_at' (\<lambda>st. st = rv) thread s \<Longrightarrow> rv = Structures_H.thread_state.Restart \<longrightarrow> st_tcb_at' isRestart thread s proof (prove)
goal:
No subgoals!
theory Orphanage

lemma receiveSignal_no_orphans [wp]:
  "\<lbrace> \<lambda>s. no_orphans s \<and> valid_queues' s \<rbrace>
   receiveSignal thread cap isBlocking
   \<lbrace> \<lambda>rv s. no_orphans s \<rbrace>" unfolding receiveSignal_def apply (wp hoare_drop_imps setThreadState_not_active_no_orphans | wpc
         | clarsimp simp: is_active_thread_state_def isRunning_def isRestart_def
                          doNBRecvFailedTransfer_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. no_orphans s \<and> valid_queues' s\<rbrace> receiveSignal thread cap isBlocking \<lbrace>\<lambda>rv. no_orphans\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. no_orphans s \<and> valid_queues' s\<rbrace> do ntfnPtr <- return (capNtfnPtr cap);
ntfn <- getNotification ntfnPtr;
case ntfnObj ntfn of Structures_H.ntfn.IdleNtfn \<Rightarrow> case isBlocking of True \<Rightarrow> do setThreadState (Structures_H.thread_state.BlockedOnNotification ntfnPtr) thread;
setNotification ntfnPtr $ ntfnObj_update (\<lambda>_. Structures_H.ntfn.WaitingNtfn [thread]) ntfn
od | False \<Rightarrow> doNBRecvFailedTransfer thread | Structures_H.ntfn.ActiveNtfn badge \<Rightarrow> do asUser thread $ setRegister Notification_H.badgeRegister badge;
setNotification ntfnPtr $ ntfnObj_update (\<lambda>_. Structures_H.ntfn.IdleNtfn) ntfn
od | Structures_H.ntfn.WaitingNtfn queue \<Rightarrow> case isBlocking of True \<Rightarrow> do setThreadState (Structures_H.thread_state.BlockedOnNotification ntfnPtr) thread;
setNotification ntfnPtr $ ntfnObj_update (\<lambda>_. Structures_H.ntfn.WaitingNtfn (queue @ [thread])) ntfn
od | False \<Rightarrow> doNBRecvFailedTransfer thread
od \<lbrace>\<lambda>rv. no_orphans\<rbrace> proof (prove)
goal:
No subgoals!
theory Orphanage

lemma deleteCallerCap_no_orphans [wp]:
  "\<lbrace> \<lambda>s. no_orphans s \<and> invs' s \<rbrace>
   deleteCallerCap receiver
   \<lbrace> \<lambda>rv s. no_orphans s \<rbrace>" unfolding deleteCallerCap_def by wpsimp auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. no_orphans s \<and> invs' s\<rbrace> deleteCallerCap receiver \<lbrace>\<lambda>rv. no_orphans\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. no_orphans s \<and> invs' s\<rbrace> do callerSlot <- getThreadCallerSlot receiver;
callerCap <- getSlotCap callerSlot;
haskell_assert (isReplyCap callerCap \<or> isNullCap callerCap) [];
cteDeleteOne callerSlot
od \<lbrace>\<lambda>rv. no_orphans\<rbrace>
theory Orphanage

lemma remove_neg_strg:
  "(A \<and> B) \<longrightarrow> ((x \<longrightarrow> A) \<and> (\<not> x \<longrightarrow> B))" by blast

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. A \<and> B \<longrightarrow> (x \<longrightarrow> A) \<and> (\<not> x \<longrightarrow> B)
theory Orphanage

lemma handleYield_no_orphans [wp]:
  "\<lbrace> \<lambda>s. no_orphans s \<and> invs' s \<rbrace>
   handleYield
   \<lbrace> \<lambda>rv . no_orphans \<rbrace>" unfolding handleYield_def apply (wp tcbSchedAppend_almost_no_orphans) apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. no_orphans s \<and> invs' s\<rbrace> handleYield \<lbrace>\<lambda>rv. no_orphans\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. no_orphans s \<and> invs' s\<rbrace> do thread <- getCurThread;
tcbSchedDequeue thread;
tcbSchedAppend thread;
rescheduleRequired
od \<lbrace>\<lambda>rv. no_orphans\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. no_orphans s \<and> invs' s \<Longrightarrow> no_orphans s \<and> (valid_queues' and tcb_at' (ksCurThread s)) s \<and> (valid_queues' and tcb_at' (ksCurThread s)) s \<and> tcb_at' (ksCurThread s) s proof (prove)
goal:
No subgoals!
theory Orphanage

lemma activatable_from_running':
  "ct_running' s \<Longrightarrow> ct_in_state' activatable' s" by (clarsimp simp: ct_in_state'_def elim!: pred_tcb'_weakenE)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ct_running' s \<Longrightarrow> ct_in_state' activatable' s
theory Orphanage

lemma sts_tcb_at'_preserve:
  "\<lbrace> st_tcb_at' P t and K (P st) \<rbrace> setThreadState st t' \<lbrace>\<lambda>_. st_tcb_at' P t \<rbrace>" by (wpsimp wp: sts_st_tcb')

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>st_tcb_at' P t and K (P st)\<rbrace> setThreadState st t' \<lbrace>\<lambda>_. st_tcb_at' P t\<rbrace>
theory Orphanage

lemma sts_tcb_at'_preserve':
  "\<lbrace> st_tcb_at' P t and st_tcb_at' (\<lambda>st. \<not> P st) t' and K (\<not> P st) \<rbrace>
  setThreadState st t'
  \<lbrace>\<lambda>_. st_tcb_at' P t \<rbrace>" by (wpsimp wp: sts_st_tcb' simp: st_tcb_at_neg')

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>st_tcb_at' P t and st_tcb_at' (\<lambda>st. \<not> P st) t' and K (\<not> P st)\<rbrace> setThreadState st t' \<lbrace>\<lambda>_. st_tcb_at' P t\<rbrace>
theory Orphanage

theorem callKernel_no_orphans [wp]:
  "\<lbrace> \<lambda>s. invs' s \<and> vs_valid_duplicates' (ksPSpace s) \<and>
          (e \<noteq> Interrupt \<longrightarrow> ct_running' s) \<and>
          ksSchedulerAction s = ResumeCurrentThread \<and> no_orphans s \<rbrace>
   callKernel e
   \<lbrace> \<lambda>rv s. no_orphans s \<rbrace>" unfolding callKernel_def by (wpsimp wp: weak_if_wp schedule_invs' hoare_drop_imps)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. invs' s \<and> vs_valid_duplicates' (ksPSpace s) \<and> (e \<noteq> Interrupt \<longrightarrow> ct_running' s) \<and> ksSchedulerAction s = ResumeCurrentThread \<and> no_orphans s\<rbrace> callKernel e \<lbrace>\<lambda>rv. no_orphans\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. invs' s \<and> vs_valid_duplicates' (ksPSpace s) \<and> (e \<noteq> Interrupt \<longrightarrow> ct_running' s) \<and> ksSchedulerAction s = ResumeCurrentThread \<and> no_orphans s\<rbrace> do stateAssert fastpathKernelAssertions [];
runExceptT $ handleEvent e `~catchError~` (\<lambda>_. withoutPreemption $ do irq <- doMachineOp (getActiveIRQ True);
when (isJust irq) $ handleInterrupt (fromJust irq)
od);
ThreadDecls_H.schedule;
activateThread;
stateAssert kernelExitAssertions []
od \<lbrace>\<lambda>rv. no_orphans\<rbrace>
theory SIMPL_Lemmas

lemma hoarep_false_pre:
  "\<Gamma>\<turnstile>\<^bsub>/F\<^esub> {} f Q,A" by (clarsimp intro!: hoare_complete simp: HoarePartialDef.valid_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<Gamma>\<turnstile>\<^bsub>/F\<^esub> {} f Q,A
theory SIMPL_Lemmas

lemma hoarep_false_pre_gen:
  "\<forall>s. \<Gamma>\<turnstile>\<^bsub>/F s\<^esub> {} f (Q s),(A s)" by (rule allI, rule hoarep_false_pre)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>s. \<Gamma>\<turnstile>\<^bsub>/F s\<^esub> {} f (Q s),(A s)
theory SIMPL_Lemmas

lemma Cond_true:
  "\<Gamma> \<turnstile>\<^bsub>/F\<^esub> P t Q, A \<Longrightarrow> \<Gamma> \<turnstile>\<^bsub>/F\<^esub> (P \<inter> b) Cond b t f Q, A" apply (rule hoare_complete) apply (drule hoare_sound) apply (clarsimp simp: HoarePartialDef.cvalid_def HoarePartialDef.valid_def) apply (erule exec_Normal_elim_cases) apply fastforce apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<Gamma>\<turnstile>\<^bsub>/F\<^esub> P t Q,A \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/F\<^esub> (P \<inter> b) Cond b t f Q,A proof (prove)
goal (1 subgoal):
 1. \<Gamma>\<turnstile>\<^bsub>/F\<^esub> P t Q,A \<Longrightarrow> \<Gamma>\<Turnstile>\<^bsub>/F\<^esub> (P \<inter> b) Cond b t f Q,A proof (prove)
goal (1 subgoal):
 1. \<Gamma>,{}\<Turnstile>\<^bsub>/F\<^esub> P t Q,A \<Longrightarrow> \<Gamma>\<Turnstile>\<^bsub>/F\<^esub> (P \<inter> b) Cond b t f Q,A proof (prove)
goal (1 subgoal):
 1. \<And>ta x. \<lbrakk>\<forall>s ta. \<Gamma>\<turnstile> \<langle>t,s\<rangle> \<Rightarrow> ta \<longrightarrow> s \<in> Normal ` P \<longrightarrow> ta \<notin> Fault ` F \<longrightarrow> ta \<in> Normal ` Q \<or> ta \<in> Abrupt ` A; \<Gamma>\<turnstile> \<langle>Cond b t f,Normal x\<rangle> \<Rightarrow> ta; x \<in> P; x \<in> b; ta \<notin> Fault ` F; ta \<notin> Abrupt ` A\<rbrakk> \<Longrightarrow> ta \<in> Normal ` Q proof (prove)
goal (2 subgoals):
 1. \<And>ta x. \<lbrakk>\<forall>s ta. \<Gamma>\<turnstile> \<langle>t,s\<rangle> \<Rightarrow> ta \<longrightarrow> s \<in> Normal ` P \<longrightarrow> ta \<notin> Fault ` F \<longrightarrow> ta \<in> Normal ` Q \<or> ta \<in> Abrupt ` A; x \<in> P; x \<in> b; ta \<notin> Fault ` F; ta \<notin> Abrupt ` A; x \<in> b; \<Gamma>\<turnstile> \<langle>t,Normal x\<rangle> \<Rightarrow> ta\<rbrakk> \<Longrightarrow> ta \<in> Normal ` Q
 2. \<And>ta x. \<lbrakk>\<forall>s ta. \<Gamma>\<turnstile> \<langle>t,s\<rangle> \<Rightarrow> ta \<longrightarrow> s \<in> Normal ` P \<longrightarrow> ta \<notin> Fault ` F \<longrightarrow> ta \<in> Normal ` Q \<or> ta \<in> Abrupt ` A; x \<in> P; x \<in> b; ta \<notin> Fault ` F; ta \<notin> Abrupt ` A; x \<notin> b; \<Gamma>\<turnstile> \<langle>f,Normal x\<rangle> \<Rightarrow> ta\<rbrakk> \<Longrightarrow> ta \<in> Normal ` Q proof (prove)
goal (1 subgoal):
 1. \<And>ta x. \<lbrakk>\<forall>s ta. \<Gamma>\<turnstile> \<langle>t,s\<rangle> \<Rightarrow> ta \<longrightarrow> s \<in> Normal ` P \<longrightarrow> ta \<notin> Fault ` F \<longrightarrow> ta \<in> Normal ` Q \<or> ta \<in> Abrupt ` A; x \<in> P; x \<in> b; ta \<notin> Fault ` F; ta \<notin> Abrupt ` A; x \<notin> b; \<Gamma>\<turnstile> \<langle>f,Normal x\<rangle> \<Rightarrow> ta\<rbrakk> \<Longrightarrow> ta \<in> Normal ` Q proof (prove)
goal:
No subgoals!