kings-crown/FVELER_Isabelle huggingface dataset:
theory Orphanage

lemma ThreadDecls_H_switchToThread_ct [wp]:
  "\<lbrace> \<top> \<rbrace>
   switchToThread tcb_ptr
   \<lbrace> \<lambda>rv s. ksCurThread s = tcb_ptr \<rbrace>" unfolding switchToThread_def apply (wp | clarsimp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> global.switchToThread tcb_ptr \<lbrace>\<lambda>rv s. ksCurThread s = tcb_ptr\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> do Arch.switchToThread tcb_ptr;
tcbSchedDequeue tcb_ptr;
setCurThread tcb_ptr
od \<lbrace>\<lambda>rv s. ksCurThread s = tcb_ptr\<rbrace> proof (prove)
goal:
No subgoals!
theory Orphanage

lemma tcbSchedEnqueue_in_ksQ':
  "\<lbrace>valid_queues' and tcb_at' t and K (t = t')\<rbrace>
     tcbSchedEnqueue t'
   \<lbrace>\<lambda>r s. \<exists>domain priority. t \<in> set (ksReadyQueues s (domain, priority))\<rbrace>" apply (rule hoare_gen_asm) apply (wp tcbSchedEnqueue_in_ksQ | clarsimp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_queues' and tcb_at' t and K (t = t')\<rbrace> tcbSchedEnqueue t' \<lbrace>\<lambda>r s. \<exists>domain priority. t \<in> set (ksReadyQueues s (domain, priority))\<rbrace> proof (prove)
goal (1 subgoal):
 1. t = t' \<Longrightarrow> \<lbrace>valid_queues' and tcb_at' t\<rbrace> tcbSchedEnqueue t' \<lbrace>\<lambda>r s. \<exists>domain priority. t \<in> set (ksReadyQueues s (domain, priority))\<rbrace> proof (prove)
goal:
No subgoals!
theory Orphanage

lemma all_invs_but_ct_idle_or_in_cur_domain'_strg:
  "invs' s \<longrightarrow> all_invs_but_ct_idle_or_in_cur_domain' s" by (clarsimp simp: invs'_to_invs_no_cicd'_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. invs' s \<longrightarrow> all_invs_but_ct_idle_or_in_cur_domain' s
theory Orphanage

lemma setSchedulerAction_cnt_sch_act_not[wp]:
  "\<lbrace> \<top> \<rbrace> setSchedulerAction ChooseNewThread \<lbrace>\<lambda>rv s. sch_act_not x s\<rbrace>" by (rule hoare_pre, rule hoare_strengthen_post[OF setSchedulerAction_direct]) auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> setSchedulerAction ChooseNewThread \<lbrace>\<lambda>rv. sch_act_not x\<rbrace>
theory Orphanage

lemma obj_at'_static_fix:
  "\<lbrakk> obj_at' (\<lambda>(ko::'a::pspace_storable). True) p s ; P \<rbrakk> \<Longrightarrow> obj_at' (\<lambda>(ko::'a::pspace_storable). P) p s" by (erule obj_at'_weakenE, simp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>obj_at' (\<lambda>ko. True) p s; P\<rbrakk> \<Longrightarrow> obj_at' (\<lambda>ko. P) p s
theory Orphanage

lemma tcbSchedEnqueue_in_ksQ_aqtp[wp]:
  "\<lbrace>valid_queues' and tcb_at' t\<rbrace> tcbSchedEnqueue t
   \<lbrace>\<lambda>r s. t \<in> all_queued_tcb_ptrs s\<rbrace>" apply (clarsimp simp: all_queued_tcb_ptrs_def) apply (rule tcbSchedEnqueue_in_ksQ) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_queues' and tcb_at' t\<rbrace> tcbSchedEnqueue t \<lbrace>\<lambda>r s. t \<in> all_queued_tcb_ptrs s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_queues' and tcb_at' t\<rbrace> tcbSchedEnqueue t \<lbrace>\<lambda>r s. \<exists>a b. t \<in> set (ksReadyQueues s (a, b))\<rbrace> proof (prove)
goal:
No subgoals!
theory Orphanage

lemma ct_active_st_tcb_at':
  "ct_active' s = st_tcb_at' runnable' (ksCurThread s) s" apply (rule iffI) apply (drule ct_active_runnable') apply (simp add: ct_in_state'_def) apply (clarsimp simp: ct_in_state'_def) apply (erule pred_tcb'_weakenE) apply (case_tac st, auto) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ct_active' s = st_tcb_at' runnable' (ksCurThread s) s proof (prove)
goal (2 subgoals):
 1. ct_active' s \<Longrightarrow> st_tcb_at' runnable' (ksCurThread s) s
 2. st_tcb_at' runnable' (ksCurThread s) s \<Longrightarrow> ct_active' s proof (prove)
goal (2 subgoals):
 1. ct_in_state' runnable' s \<Longrightarrow> st_tcb_at' runnable' (ksCurThread s) s
 2. st_tcb_at' runnable' (ksCurThread s) s \<Longrightarrow> ct_active' s proof (prove)
goal (1 subgoal):
 1. st_tcb_at' runnable' (ksCurThread s) s \<Longrightarrow> ct_active' s proof (prove)
goal (1 subgoal):
 1. st_tcb_at' runnable' (ksCurThread s) s \<Longrightarrow> st_tcb_at' active' (ksCurThread s) s proof (prove)
goal (1 subgoal):
 1. \<And>st. runnable' st \<Longrightarrow> active' st proof (prove)
goal:
No subgoals!
theory Orphanage

lemma tcbSchedEnqueue_in_ksQ_already_queued_aqtp:
  "\<lbrace>\<lambda>s. valid_queues' s \<and> tcb_at' t s \<and>
    t' \<in> all_queued_tcb_ptrs s \<rbrace> tcbSchedEnqueue t
   \<lbrace>\<lambda>r s. t' \<in> all_queued_tcb_ptrs s \<rbrace>" by (clarsimp simp: all_queued_tcb_ptrs_def tcbSchedEnqueue_in_ksQ_already_queued)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. valid_queues' s \<and> tcb_at' t s \<and> t' \<in> all_queued_tcb_ptrs s\<rbrace> tcbSchedEnqueue t \<lbrace>\<lambda>r s. t' \<in> all_queued_tcb_ptrs s\<rbrace>
theory Orphanage

lemma invs_switchToThread_runnable':
  "\<lbrakk> invs' s ; ksSchedulerAction s = SwitchToThread t \<rbrakk> \<Longrightarrow> st_tcb_at' runnable' t s" by (simp add: invs'_def valid_state'_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>invs' s; ksSchedulerAction s = SwitchToThread t\<rbrakk> \<Longrightarrow> st_tcb_at' runnable' t s
theory Orphanage

lemma not_pred_tcb_at'I:
  "\<lbrakk> pred_tcb_at' f (Not \<circ> P) t s ; tcb_at' t s \<rbrakk> \<Longrightarrow> \<not> pred_tcb_at' f P t s" by (subst (asm) pred_tcb_at'_Not, blast)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pred_tcb_at' f (Not \<circ> P) t s; tcb_at' t s\<rbrakk> \<Longrightarrow> \<not> pred_tcb_at' f P t s
theory Orphanage

lemma in_all_active_tcb_ptrsD:
  "t \<in> all_active_tcb_ptrs s \<Longrightarrow> st_tcb_at' runnable' t s" unfolding all_active_tcb_ptrs_def is_active_tcb_ptr_def
             is_active_thread_state_def isRunning_def isRestart_def apply clarsimp apply (erule pred_tcb'_weakenE) apply (case_tac st; clarsimp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. t \<in> all_active_tcb_ptrs s \<Longrightarrow> st_tcb_at' runnable' t s proof (prove)
goal (1 subgoal):
 1. t \<in> {tcb_ptr. st_tcb_at' (\<lambda>ts. (case ts of Structures_H.thread_state.Running \<Rightarrow> True | _ \<Rightarrow> False) \<or> (case ts of Structures_H.thread_state.Restart \<Rightarrow> True | _ \<Rightarrow> False)) tcb_ptr s} \<Longrightarrow> st_tcb_at' runnable' t s proof (prove)
goal (1 subgoal):
 1. st_tcb_at' (\<lambda>ts. (case ts of Structures_H.thread_state.Running \<Rightarrow> True | _ \<Rightarrow> False) \<or> (case ts of Structures_H.thread_state.Restart \<Rightarrow> True | _ \<Rightarrow> False)) t s \<Longrightarrow> st_tcb_at' runnable' t s proof (prove)
goal (1 subgoal):
 1. \<And>st. (case st of Structures_H.thread_state.Running \<Rightarrow> True | _ \<Rightarrow> False) \<or> (case st of Structures_H.thread_state.Restart \<Rightarrow> True | _ \<Rightarrow> False) \<Longrightarrow> runnable' st proof (prove)
goal:
No subgoals!
theory Orphanage

lemma setNotification_no_orphans [wp]:
  "\<lbrace> \<lambda>s. no_orphans s \<rbrace>
   setNotification p ntfn
   \<lbrace> \<lambda>_ s. no_orphans s \<rbrace>" apply (rule no_orphans_lift) apply (wp | clarsimp simp: setNotification_def updateObject_default_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>no_orphans\<rbrace> setNotification p ntfn \<lbrace>\<lambda>_. no_orphans\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>tcb_ptr. \<lbrace>\<lambda>s. \<not> typ_at' TCBT tcb_ptr s\<rbrace> setNotification p ntfn \<lbrace>\<lambda>_ s. \<not> typ_at' TCBT tcb_ptr s\<rbrace>
 2. \<And>tcb_ptr. \<lbrace>\<lambda>s. tcb_ptr = ksCurThread s\<rbrace> setNotification p ntfn \<lbrace>\<lambda>_ s. tcb_ptr = ksCurThread s\<rbrace>
 3. \<And>P pa. \<lbrace>st_tcb_at' P pa\<rbrace> setNotification p ntfn \<lbrace>\<lambda>_. st_tcb_at' P pa\<rbrace>
 4. \<And>P. \<lbrace>\<lambda>s. P (ksReadyQueues s)\<rbrace> setNotification p ntfn \<lbrace>\<lambda>_ s. P (ksReadyQueues s)\<rbrace>
 5. \<And>P. \<lbrace>\<lambda>s. P (ksSchedulerAction s)\<rbrace> setNotification p ntfn \<lbrace>\<lambda>_ s. P (ksSchedulerAction s)\<rbrace> proof (prove)
goal:
No subgoals!
theory Orphanage

lemma possibleSwitchTo_almost_no_orphans [wp]:
  "\<lbrace> \<lambda>s. almost_no_orphans target s \<and> valid_queues' s \<and> st_tcb_at' runnable' target s
         \<and> weak_sch_act_wf (ksSchedulerAction s) s \<rbrace>
   possibleSwitchTo target
   \<lbrace> \<lambda>rv s. no_orphans s \<rbrace>" unfolding possibleSwitchTo_def by (wp rescheduleRequired_valid_queues'_weak tcbSchedEnqueue_almost_no_orphans
         ssa_almost_no_orphans hoare_weak_lift_imp
     | wpc | clarsimp
     | wp (once) hoare_drop_imp)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. almost_no_orphans target s \<and> valid_queues' s \<and> st_tcb_at' runnable' target s \<and> weak_sch_act_wf (ksSchedulerAction s) s\<rbrace> possibleSwitchTo target \<lbrace>\<lambda>rv. no_orphans\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. almost_no_orphans target s \<and> valid_queues' s \<and> st_tcb_at' runnable' target s \<and> weak_sch_act_wf (ksSchedulerAction s) s\<rbrace> do curDom <- curDomain;
targetDom <- threadGet tcbDomain target;
action <- getSchedulerAction;
if targetDom \<noteq> curDom then tcbSchedEnqueue target else if action \<noteq> ResumeCurrentThread then do rescheduleRequired;
tcbSchedEnqueue target
od else setSchedulerAction $ SwitchToThread target
od \<lbrace>\<lambda>rv. no_orphans\<rbrace>
theory Orphanage

lemma no_orphans_is_almost[simp]:
  "no_orphans s \<Longrightarrow> almost_no_orphans t s" by (clarsimp simp: no_orphans_def almost_no_orphans_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_orphans s \<Longrightarrow> almost_no_orphans t s
theory Orphanage

lemma handleDoubleFault_no_orphans [wp]:
  "\<lbrace> \<lambda>s. no_orphans s \<and> valid_queues' s \<rbrace>
   handleDoubleFault tptr ex1 ex2
   \<lbrace> \<lambda>rv s. no_orphans s \<rbrace>" unfolding handleDoubleFault_def apply (wp setThreadState_not_active_no_orphans
         | clarsimp simp: is_active_thread_state_def isRestart_def isRunning_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. no_orphans s \<and> valid_queues' s\<rbrace> handleDoubleFault tptr ex1 ex2 \<lbrace>\<lambda>rv. no_orphans\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. no_orphans s \<and> valid_queues' s\<rbrace> do setThreadState Structures_H.thread_state.Inactive tptr;
faultPC <- asUser tptr getRestartPC;
errmsg <- return ([] @ show ex2 @ [] @ show ex1 @ [] @ show tptr @ [] @ show faultPC);
doMachineOp $ debugPrint errmsg
od \<lbrace>\<lambda>rv. no_orphans\<rbrace> proof (prove)
goal:
No subgoals!
theory Orphanage

lemma setupCallerCap_no_orphans [wp]:
  "\<lbrace> \<lambda>s. no_orphans s \<and> valid_queues' s \<rbrace>
   setupCallerCap sender receiver gr
   \<lbrace> \<lambda>rv s. no_orphans s \<rbrace>" unfolding setupCallerCap_def apply (wp setThreadState_not_active_no_orphans
         | clarsimp simp: is_active_thread_state_def isRestart_def isRunning_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. no_orphans s \<and> valid_queues' s\<rbrace> setupCallerCap sender receiver gr \<lbrace>\<lambda>rv. no_orphans\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. no_orphans s \<and> valid_queues' s\<rbrace> do setThreadState Structures_H.thread_state.BlockedOnReply sender;
replySlot <- getThreadReplySlot sender;
masterCTE <- getCTE replySlot;
masterCap <- return (cteCap masterCTE);
haskell_assert (isReplyCap masterCap \<and> capReplyMaster masterCap \<and> capTCBPtr masterCap = sender) [];
haskell_assert (mdbNext (cteMDBNode masterCTE) = nullPointer) [];
callerSlot <- getThreadCallerSlot receiver;
callerCap <- getSlotCap callerSlot;
haskell_assert (isNullCap callerCap) [];
cteInsert (capability.ReplyCap sender False gr) replySlot callerSlot
od \<lbrace>\<lambda>rv. no_orphans\<rbrace> proof (prove)
goal:
No subgoals!
theory Orphanage

lemma setupCallerCap_almost_no_orphans [wp]:
  "\<lbrace> \<lambda>s. almost_no_orphans tcb_ptr s \<and> valid_queues' s \<rbrace>
   setupCallerCap sender receiver gr
   \<lbrace> \<lambda>rv s. almost_no_orphans tcb_ptr s \<rbrace>" unfolding setupCallerCap_def apply (wp setThreadState_not_active_almost_no_orphans
         | clarsimp simp: is_active_thread_state_def isRestart_def isRunning_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. almost_no_orphans tcb_ptr s \<and> valid_queues' s\<rbrace> setupCallerCap sender receiver gr \<lbrace>\<lambda>rv. almost_no_orphans tcb_ptr\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. almost_no_orphans tcb_ptr s \<and> valid_queues' s\<rbrace> do setThreadState Structures_H.thread_state.BlockedOnReply sender;
replySlot <- getThreadReplySlot sender;
masterCTE <- getCTE replySlot;
masterCap <- return (cteCap masterCTE);
haskell_assert (isReplyCap masterCap \<and> capReplyMaster masterCap \<and> capTCBPtr masterCap = sender) [];
haskell_assert (mdbNext (cteMDBNode masterCTE) = nullPointer) [];
callerSlot <- getThreadCallerSlot receiver;
callerCap <- getSlotCap callerSlot;
haskell_assert (isNullCap callerCap) [];
cteInsert (capability.ReplyCap sender False gr) replySlot callerSlot
od \<lbrace>\<lambda>rv. almost_no_orphans tcb_ptr\<rbrace> proof (prove)
goal:
No subgoals!
theory Orphanage

lemma replyFromKernel_no_orphans [wp]:
  "\<lbrace> \<lambda>s. no_orphans s \<rbrace>
   replyFromKernel thread r
   \<lbrace> \<lambda>rv s. no_orphans s \<rbrace>" apply (cases r, simp_all add: replyFromKernel_def) apply wp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>no_orphans\<rbrace> replyFromKernel thread r \<lbrace>\<lambda>rv. no_orphans\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>a b. r = (a, b) \<Longrightarrow> \<lbrace>no_orphans\<rbrace> do destIPCBuffer <- lookupIPCBuffer True thread;
y <- asUser thread (setRegister Notification_H.badgeRegister 0);
len <- setMRs thread destIPCBuffer b;
setMessageInfo thread (Types_H.message_info.MI len 0 0 a)
od \<lbrace>\<lambda>rv. no_orphans\<rbrace> proof (prove)
goal:
No subgoals!
theory Orphanage

lemma copyGlobalMappings_no_orphans [wp]:
  "\<lbrace> \<lambda>s. no_orphans s \<rbrace>
   copyGlobalMappings newPD
   \<lbrace> \<lambda>rv s. no_orphans s \<rbrace>" unfolding no_orphans_disj all_queued_tcb_ptrs_def apply (wp hoare_vcg_all_lift hoare_vcg_disj_lift) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>no_orphans\<rbrace> copyGlobalMappings newPD \<lbrace>\<lambda>rv. no_orphans\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<forall>tcb_ptr. tcb_ptr = ksCurThread s \<or> tcb_ptr \<in> {tcb_ptr. \<exists>priority. tcb_ptr \<in> set (ksReadyQueues s priority)} \<or> \<not> typ_at' TCBT tcb_ptr s \<or> st_tcb_at' (\<lambda>state. \<not> is_active_thread_state state) tcb_ptr s \<or> ksSchedulerAction s = SwitchToThread tcb_ptr\<rbrace> copyGlobalMappings newPD \<lbrace>\<lambda>rv s. \<forall>tcb_ptr. tcb_ptr = ksCurThread s \<or> tcb_ptr \<in> {tcb_ptr. \<exists>priority. tcb_ptr \<in> set (ksReadyQueues s priority)} \<or> \<not> typ_at' TCBT tcb_ptr s \<or> st_tcb_at' (\<lambda>state. \<not> is_active_thread_state state) tcb_ptr s \<or> ksSchedulerAction s = SwitchToThread tcb_ptr\<rbrace> proof (prove)
goal:
No subgoals!
theory Orphanage

lemma ksMachineState_ksPSpace_upd_comm:
  "ksPSpace_update g (ksMachineState_update f s) =
   ksMachineState_update f (ksPSpace_update g s)" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ksPSpace_update g (ksMachineState_update f s) = ksMachineState_update f (ksPSpace_update g s)
theory Orphanage

lemma setInterruptState_no_orphans [wp]:
  "\<lbrace> \<lambda>s. no_orphans s \<rbrace>
   setInterruptState a
   \<lbrace> \<lambda>rv s. no_orphans s \<rbrace>" unfolding no_orphans_disj all_queued_tcb_ptrs_def apply (wp hoare_vcg_all_lift hoare_vcg_disj_lift | clarsimp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>no_orphans\<rbrace> setInterruptState a \<lbrace>\<lambda>rv. no_orphans\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<forall>tcb_ptr. tcb_ptr = ksCurThread s \<or> tcb_ptr \<in> {tcb_ptr. \<exists>priority. tcb_ptr \<in> set (ksReadyQueues s priority)} \<or> \<not> typ_at' TCBT tcb_ptr s \<or> st_tcb_at' (\<lambda>state. \<not> is_active_thread_state state) tcb_ptr s \<or> ksSchedulerAction s = SwitchToThread tcb_ptr\<rbrace> setInterruptState a \<lbrace>\<lambda>rv s. \<forall>tcb_ptr. tcb_ptr = ksCurThread s \<or> tcb_ptr \<in> {tcb_ptr. \<exists>priority. tcb_ptr \<in> set (ksReadyQueues s priority)} \<or> \<not> typ_at' TCBT tcb_ptr s \<or> st_tcb_at' (\<lambda>state. \<not> is_active_thread_state state) tcb_ptr s \<or> ksSchedulerAction s = SwitchToThread tcb_ptr\<rbrace> proof (prove)
goal:
No subgoals!
theory Orphanage

lemma mapM_x_match:
  "\<lbrace>I and V xs\<rbrace> mapM_x m xs \<lbrace>\<lambda>rv. Q\<rbrace> \<Longrightarrow> \<lbrace>I and V xs\<rbrace> mapM_x m xs \<lbrace>\<lambda>rv. Q\<rbrace>" by assumption

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>I and V xs\<rbrace> mapM_x m xs \<lbrace>\<lambda>rv. Q\<rbrace> \<Longrightarrow> \<lbrace>I and V xs\<rbrace> mapM_x m xs \<lbrace>\<lambda>rv. Q\<rbrace>
theory Orphanage

lemma unbindNotification_no_orphans[wp]:
  "\<lbrace>\<lambda>s. no_orphans s\<rbrace>
    unbindNotification t
   \<lbrace> \<lambda>rv s. no_orphans s\<rbrace>" unfolding unbindNotification_def apply (rule hoare_seq_ext[OF _ gbn_sp']) apply (case_tac ntfnPtr, simp_all, wp, simp) apply (rule hoare_seq_ext[OF _ get_ntfn_sp']) apply (wp | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>no_orphans\<rbrace> unbindNotification t \<lbrace>\<lambda>rv. no_orphans\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>no_orphans\<rbrace> do ntfnPtr <- getBoundNotification t;
case ntfnPtr of None \<Rightarrow> return () | Some ntfnPtr' \<Rightarrow> do ntfn <- getNotification ntfnPtr';
doUnbindNotification ntfnPtr' ntfn t
od
od \<lbrace>\<lambda>rv. no_orphans\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>ntfnPtr. \<lbrace>bound_tcb_at' (\<lambda>st. st = ntfnPtr) t and no_orphans\<rbrace> case ntfnPtr of None \<Rightarrow> return () | Some ntfnPtr' \<Rightarrow> do ntfn <- getNotification ntfnPtr';
doUnbindNotification ntfnPtr' ntfn t
od \<lbrace>\<lambda>rv. no_orphans\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>ntfnPtr a. ntfnPtr = Some a \<Longrightarrow> \<lbrace>bound_tcb_at' (\<lambda>st. st = Some a) t and no_orphans\<rbrace> do ntfn <- getNotification a;
y <- setNotification a (ntfnBoundTCB_update (\<lambda>_. None) ntfn);
setBoundNotification None t
od \<lbrace>\<lambda>rv. no_orphans\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>ntfnPtr a ntfn. ntfnPtr = Some a \<Longrightarrow> \<lbrace>bound_tcb_at' (\<lambda>st. st = Some a) t and no_orphans and ko_at' ntfn a\<rbrace> do y <- setNotification a (ntfnBoundTCB_update (\<lambda>_. None) ntfn);
setBoundNotification None t
od \<lbrace>\<lambda>rv. no_orphans\<rbrace> proof (prove)
goal:
No subgoals!
theory Orphanage

lemma unbindMaybeNotification_no_orphans[wp]:
  "\<lbrace>\<lambda>s. no_orphans s\<rbrace>
    unbindMaybeNotification a
   \<lbrace> \<lambda>rv s. no_orphans s\<rbrace>" unfolding unbindMaybeNotification_def by (wp getNotification_wp | simp | wpc)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>no_orphans\<rbrace> unbindMaybeNotification a \<lbrace>\<lambda>rv. no_orphans\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>no_orphans\<rbrace> do ntfn <- getNotification a;
case ntfnBoundTCB ntfn of None \<Rightarrow> return () | Some t \<Rightarrow> doUnbindNotification a ntfn t
od \<lbrace>\<lambda>rv. no_orphans\<rbrace>
theory Orphanage

lemma finaliseCapTrue_standin_no_orphans [wp]:
  "\<lbrace> \<lambda>s. no_orphans s \<and> valid_queues' s \<and> valid_objs' s \<rbrace>
    finaliseCapTrue_standin cap final
   \<lbrace> \<lambda>rv s. no_orphans s \<rbrace>" unfolding finaliseCapTrue_standin_def apply (rule hoare_pre) apply (wp | clarsimp simp: Let_def | wpc)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. no_orphans s \<and> valid_queues' s \<and> valid_objs' s\<rbrace> finaliseCapTrue_standin cap final \<lbrace>\<lambda>rv. no_orphans\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. no_orphans s \<and> valid_queues' s \<and> valid_objs' s\<rbrace> if isEndpointCap cap then do y <- when final (cancelAllIPC (capEPPtr cap));
return (capability.NullCap, capability.NullCap)
od else if isNotificationCap cap then let ptr = capNtfnPtr cap in do y <- when final (do y <- unbindMaybeNotification ptr;
cancelAllSignals ptr
od);
return (capability.NullCap, capability.NullCap)
od else if isReplyCap cap then return (capability.NullCap, capability.NullCap) else if cap = capability.NullCap then return (capability.NullCap, capability.NullCap) else if cap = capability.DomainCap then return (capability.NullCap, capability.NullCap) else fail \<lbrace>\<lambda>rv. no_orphans\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> if isEndpointCap cap then do y <- when final (cancelAllIPC (capEPPtr cap));
return (capability.NullCap, capability.NullCap)
od else if isNotificationCap cap then let ptr = capNtfnPtr cap in do y <- when final (do y <- unbindMaybeNotification ptr;
cancelAllSignals ptr
od);
return (capability.NullCap, capability.NullCap)
od else if isReplyCap cap then return (capability.NullCap, capability.NullCap) else if cap = capability.NullCap then return (capability.NullCap, capability.NullCap) else if cap = capability.DomainCap then return (capability.NullCap, capability.NullCap) else fail \<lbrace>\<lambda>rv. no_orphans\<rbrace>
 2. \<And>s. no_orphans s \<and> valid_queues' s \<and> valid_objs' s \<Longrightarrow> ?Q s proof (prove)
goal:
No subgoals!
theory Orphanage

lemma cteDeleteOne_no_orphans [wp]:
  "\<lbrace> \<lambda>s. no_orphans s \<and> valid_queues' s \<and> valid_objs' s \<rbrace>
   cteDeleteOne slot
   \<lbrace> \<lambda>rv s. no_orphans s \<rbrace>" unfolding cteDeleteOne_def apply (wp assert_inv isFinalCapability_inv weak_if_wp | clarsimp simp: unless_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. no_orphans s \<and> valid_queues' s \<and> valid_objs' s\<rbrace> cteDeleteOne slot \<lbrace>\<lambda>rv. no_orphans\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. no_orphans s \<and> valid_queues' s \<and> valid_objs' s\<rbrace> do cte <- getCTE slot;
unless (isNullCap $ cteCap cte) $ do final <- isFinalCapability cte;
(remainder, info) <- finaliseCapTrue_standin (cteCap cte) final;
haskell_assert (capRemovable remainder slot \<and> isNullCap info) $ [];
emptySlot slot capability.NullCap
od
od \<lbrace>\<lambda>rv. no_orphans\<rbrace> proof (prove)
goal:
No subgoals!