kings-crown/FVELER_Isabelle huggingface dataset:
theory Orphanage

lemma asUser_almost_no_orphans:
  "\<lbrace>almost_no_orphans t\<rbrace> asUser a f \<lbrace>\<lambda>_. almost_no_orphans t\<rbrace>" unfolding almost_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>almost_no_orphans t\<rbrace> asUser a f \<lbrace>\<lambda>_. almost_no_orphans t\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<forall>ptr. ptr = ksCurThread s \<or> ptr \<in> {tcb_ptr. \<exists>priority. tcb_ptr \<in> set (ksReadyQueues s priority)} \<or> \<not> typ_at' TCBT ptr s \<or> st_tcb_at' (\<lambda>thread_state. \<not> is_active_thread_state thread_state) ptr s \<or> ptr = t \<or> ksSchedulerAction s = SwitchToThread ptr\<rbrace> asUser a f \<lbrace>\<lambda>_ s. \<forall>ptr. ptr = ksCurThread s \<or> ptr \<in> {tcb_ptr. \<exists>priority. tcb_ptr \<in> set (ksReadyQueues s priority)} \<or> \<not> typ_at' TCBT ptr s \<or> st_tcb_at' (\<lambda>thread_state. \<not> is_active_thread_state thread_state) ptr s \<or> ptr = t \<or> ksSchedulerAction s = SwitchToThread ptr\<rbrace> proof (prove)
goal:
No subgoals!
theory Orphanage

lemma handleInterrupt_no_orphans [wp]:
  "\<lbrace> \<lambda>s. no_orphans s \<and> invs' s \<rbrace>
   handleInterrupt irq
   \<lbrace> \<lambda>rv s. no_orphans s \<rbrace>" unfolding handleInterrupt_def apply (rule hoare_pre) apply (wp hoare_drop_imps hoare_vcg_all_lift getIRQState_inv
          | wpc | clarsimp simp: invs'_def valid_state'_def maskIrqSignal_def
                                 handleReservedIRQ_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. no_orphans s \<and> invs' s\<rbrace> handleInterrupt irq \<lbrace>\<lambda>rv. no_orphans\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. no_orphans s \<and> invs' s\<rbrace> if maxIRQ < irq then doMachineOp $ do maskInterrupt True irq;
ackInterrupt irq
od else do st <- getIRQState irq;
case st of irqstate.IRQInactive \<Rightarrow> haskell_fail $ [] @ show irq | irqstate.IRQSignal \<Rightarrow> do slot <- getIRQSlot irq;
cap <- getSlotCap slot;
case cap of capability.NotificationCap x xa True xb \<Rightarrow> sendSignal (capNtfnPtr cap) (capNtfnBadge cap) | capability.NotificationCap x xa False xb \<Rightarrow> doMachineOp $ debugPrint $ [] @ show irq | _ \<Rightarrow> doMachineOp $ debugPrint $ [] @ show irq;
maskIrqSignal irq
od | irqstate.IRQTimer \<Rightarrow> do timerTick;
doMachineOp resetTimer
od | irqstate.IRQReserved \<Rightarrow> handleReservedIRQ irq;
doMachineOp $ ackInterrupt irq
od \<lbrace>\<lambda>rv. no_orphans\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> if maxIRQ < irq then doMachineOp $ do maskInterrupt True irq;
ackInterrupt irq
od else do st <- getIRQState irq;
case st of irqstate.IRQInactive \<Rightarrow> haskell_fail $ [] @ show irq | irqstate.IRQSignal \<Rightarrow> do slot <- getIRQSlot irq;
cap <- getSlotCap slot;
case cap of capability.NotificationCap x xa True xb \<Rightarrow> sendSignal (capNtfnPtr cap) (capNtfnBadge cap) | capability.NotificationCap x xa False xb \<Rightarrow> doMachineOp $ debugPrint $ [] @ show irq | _ \<Rightarrow> doMachineOp $ debugPrint $ [] @ show irq;
maskIrqSignal irq
od | irqstate.IRQTimer \<Rightarrow> do timerTick;
doMachineOp resetTimer
od | irqstate.IRQReserved \<Rightarrow> handleReservedIRQ irq;
doMachineOp $ ackInterrupt irq
od \<lbrace>\<lambda>rv. no_orphans\<rbrace>
 2. \<And>s. no_orphans s \<and> invs' s \<Longrightarrow> ?Q s proof (prove)
goal:
No subgoals!
theory Orphanage

lemma updateRestartPC_no_orphans[wp]:
  "\<lbrace> \<lambda>s. no_orphans s \<and> invs' s \<rbrace>
   updateRestartPC t
   \<lbrace> \<lambda>rv s. no_orphans s \<rbrace>" by (wpsimp simp: updateRestartPC_def asUser_no_orphans)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. no_orphans s \<and> invs' s\<rbrace> updateRestartPC t \<lbrace>\<lambda>rv. no_orphans\<rbrace>
theory Orphanage

lemma updateRestartPC_valid_queues'[wp]:
  "\<lbrace> \<lambda>s. valid_queues' s \<rbrace>
   updateRestartPC t
   \<lbrace> \<lambda>rv s. valid_queues' s \<rbrace>" unfolding updateRestartPC_def apply (rule asUser_valid_queues') done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_queues'\<rbrace> updateRestartPC t \<lbrace>\<lambda>rv. valid_queues'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_queues'\<rbrace> asUser t (getRegister Thread_H.nextInstructionRegister >>= setRegister Thread_H.faultRegister) \<lbrace>\<lambda>rv. valid_queues'\<rbrace> proof (prove)
goal:
No subgoals!
theory Orphanage

lemma updateRestartPC_no_orphans_invs'_valid_queues'[wp]:
  "\<lbrace>\<lambda>s. no_orphans s \<and> invs' s \<and> valid_queues' s \<rbrace>
   updateRestartPC t
   \<lbrace>\<lambda>rv s. no_orphans s \<and> valid_queues' s \<rbrace>" by (wpsimp simp: updateRestartPC_def asUser_no_orphans)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. no_orphans s \<and> invs' s \<and> valid_queues' s\<rbrace> updateRestartPC t \<lbrace>\<lambda>rv s. no_orphans s \<and> valid_queues' s\<rbrace>
theory Orphanage

lemma invalidateHWASIDEntry_no_orphans [wp]:
  "\<lbrace> \<lambda>s. no_orphans s \<rbrace>
   invalidateHWASIDEntry hwASID
   \<lbrace> \<lambda>reply 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> invalidateHWASIDEntry hwASID \<lbrace>\<lambda>reply. 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> invalidateHWASIDEntry hwASID \<lbrace>\<lambda>reply 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 invalidateASID_no_orphans [wp]:
  "\<lbrace> \<lambda>s. no_orphans s \<rbrace>
   invalidateASID asid
   \<lbrace> \<lambda>reply 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> invalidateASID asid \<lbrace>\<lambda>reply. 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> invalidateASID asid \<lbrace>\<lambda>reply 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 findFreeHWASID_no_orphans [wp]:
  "\<lbrace> \<lambda>s. no_orphans s \<rbrace>
   findFreeHWASID
   \<lbrace> \<lambda>reply 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> findFreeHWASID \<lbrace>\<lambda>reply. 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> findFreeHWASID \<lbrace>\<lambda>reply 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 invalidateASIDEntry_no_orphans [wp]:
  "\<lbrace> \<lambda>s. no_orphans s \<rbrace>
   invalidateASIDEntry asid
   \<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> invalidateASIDEntry asid \<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> invalidateASIDEntry asid \<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 storePTE_no_orphans [wp]:
  "\<lbrace> \<lambda>s. no_orphans s \<rbrace>
   storePTE ptr val
   \<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> storePTE ptr val \<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> storePTE ptr val \<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 storePDE_no_orphans [wp]:
  "\<lbrace> \<lambda>s. no_orphans s \<rbrace>
   storePDE ptr val
   \<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> storePDE ptr val \<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> storePDE ptr val \<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 flushTable_no_orphans [wp]:
  "\<lbrace> \<lambda>s. no_orphans s \<rbrace>
   flushTable pd asid vptr
   \<lbrace> \<lambda>reply s. no_orphans s \<rbrace>" unfolding flushTable_def apply (wp hoare_drop_imps | wpc | clarsimp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>no_orphans\<rbrace> flushTable pd asid vptr \<lbrace>\<lambda>reply. no_orphans\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>no_orphans\<rbrace> do haskell_assert (vptr && mask (pageBitsForSize ARMSection) = 0) [];
root_switched <- setVMRootForFlush pd asid;
maybe_hw_asid <- loadHWASID asid;
when (isJust maybe_hw_asid) $ do doMachineOp $ invalidateLocalTLB_ASID (fromJust maybe_hw_asid);
when root_switched $ getCurThread >>= setVMRoot
od
od \<lbrace>\<lambda>reply. no_orphans\<rbrace> proof (prove)
goal:
No subgoals!
theory Orphanage

lemma setASIDPool_no_orphans [wp]:
  "\<lbrace> \<lambda>s. no_orphans s \<rbrace>
   setObject p (ap :: asidpool)
   \<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> setObject p ap \<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> setObject p ap \<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 deleteASID_no_orphans [wp]:
  "\<lbrace> \<lambda>s. no_orphans s \<rbrace>
   deleteASID asid pd
   \<lbrace> \<lambda>rv s. no_orphans s \<rbrace>" unfolding deleteASID_def apply (wp getObject_inv loadObject_default_inv | wpc | clarsimp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>no_orphans\<rbrace> deleteASID asid pd \<lbrace>\<lambda>rv. no_orphans\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>no_orphans\<rbrace> do asidTable <- gets (armKSASIDTable \<circ> ksArchState);
case asidTable (asidHighBitsOf asid) of None \<Rightarrow> return () | Some poolPtr \<Rightarrow> do pool <- liftM (inv asidpool.ASIDPool) $ getObject poolPtr;
when (pool (asid && mask asidLowBits) = Just pd) $ do flushSpace asid;
invalidateASIDEntry asid;
pool' <- return (pool aLU [(asid && mask asidLowBits, Nothing)]);
setObject poolPtr $ asidpool.ASIDPool pool';
getCurThread >>= setVMRoot
od
od
od \<lbrace>\<lambda>rv. no_orphans\<rbrace> proof (prove)
goal:
No subgoals!
theory Orphanage

lemma deletingIRQHandler_no_orphans [wp]:
  "\<lbrace> \<lambda>s. no_orphans s \<and> invs' s \<rbrace>
   deletingIRQHandler irq
   \<lbrace> \<lambda>rv s. no_orphans s \<rbrace>" unfolding deletingIRQHandler_def apply (wp, auto) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. no_orphans s \<and> invs' s\<rbrace> deletingIRQHandler irq \<lbrace>\<lambda>rv. no_orphans\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. no_orphans s \<and> invs' s\<rbrace> do slot <- getIRQSlot irq;
cap <- getSlotCap slot;
haskell_assert (isNotificationCap cap \<or> isNullCap cap) [];
cteDeleteOne slot
od \<lbrace>\<lambda>rv. no_orphans\<rbrace> proof (prove)
goal:
No subgoals!
theory Orphanage

lemma no_orphans_finalise_prop_stuff:
  "no_cte_prop no_orphans = no_orphans"
  "finalise_prop_stuff no_orphans" by (simp_all add: no_cte_prop_def finalise_prop_stuff_def
                    setCTE_no_orphans,
    simp_all add: no_orphans_def all_active_tcb_ptrs_def
                  is_active_tcb_ptr_def all_queued_tcb_ptrs_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_cte_prop no_orphans = no_orphans &&& finalise_prop_stuff no_orphans
theory Orphanage

lemma cteRevoke_no_orphans [wp]:
  "\<lbrace> \<lambda>s. no_orphans s \<and> invs' s \<and> sch_act_simple s \<rbrace>
   cteRevoke ptr
   \<lbrace> \<lambda>rv s. no_orphans s \<rbrace>" apply (rule_tac Q="\<lambda>rv s. no_orphans s \<and> invs' s \<and> sch_act_simple s"
                      in hoare_strengthen_post) apply (wp cteRevoke_preservation cteDelete_invs' cteDelete_sch_act_simple)+ apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. no_orphans s \<and> invs' s \<and> sch_act_simple s\<rbrace> cteRevoke ptr \<lbrace>\<lambda>rv. no_orphans\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>\<lambda>s. no_orphans s \<and> invs' s \<and> sch_act_simple s\<rbrace> cteRevoke ptr \<lbrace>\<lambda>rv s. no_orphans s \<and> invs' s \<and> sch_act_simple s\<rbrace>
 2. \<And>rv s. no_orphans s \<and> invs' s \<and> sch_act_simple s \<Longrightarrow> no_orphans s proof (prove)
goal (5 subgoals):
 1. \<And>s ptr sa. no_orphans sa \<and> invs' sa \<and> sch_act_simple sa \<Longrightarrow> (no_orphans and invs' and sch_act_simple and K True) sa \<and> (invs' and sch_act_simple and K True) sa \<and> (invs' and sch_act_simple and (\<lambda>s. \<not> True \<longrightarrow> ex_cte_cap_wp_to' (\<lambda>_. True) ptr s)) sa \<and> (no_orphans and invs' and sch_act_simple and K True) sa \<and> (invs' and sch_act_simple and K True) sa \<and> (invs' and sch_act_simple and (\<lambda>s. \<not> True \<longrightarrow> ex_cte_cap_wp_to' (\<lambda>_. True) ptr s)) sa
 2. \<And>s f sa. (no_orphans (ksWorkUnitsCompleted_update f sa) \<and> invs' (ksWorkUnitsCompleted_update f sa) \<and> sch_act_simple (ksWorkUnitsCompleted_update f sa)) = (no_orphans sa \<and> invs' sa \<and> sch_act_simple sa)
 3. \<And>s. irq_state_independent_H (\<lambda>s. no_orphans s \<and> invs' s \<and> sch_act_simple s)
 4. \<And>s. no_orphans s \<and> invs' s \<and> sch_act_simple s \<Longrightarrow> no_orphans s \<and> invs' s \<and> sch_act_simple s
 5. \<And>rv s. no_orphans s \<and> invs' s \<and> sch_act_simple s \<Longrightarrow> no_orphans s proof (prove)
goal:
No subgoals!
theory Orphanage

lemma cancelSignal_valid_queues' [wp]:
  "\<lbrace> \<lambda>s. valid_queues' s \<and> valid_objs' s \<rbrace>
   cancelSignal t ntfn
   \<lbrace> \<lambda>rv s. valid_queues' s \<rbrace>" unfolding cancelSignal_def Let_def apply (rule hoare_pre) apply (wp hoare_drop_imps | wpc | clarsimp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. valid_queues' s \<and> valid_objs' s\<rbrace> cancelSignal t ntfn \<lbrace>\<lambda>rv. valid_queues'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. valid_queues' s \<and> valid_objs' s\<rbrace> do ntfna <- getNotification ntfn;
haskell_assert (case ntfnObj ntfna of Structures_H.ntfn.WaitingNtfn x \<Rightarrow> True | _ \<Rightarrow> False) [];
queue' <- return (delete t $ ntfnQueue $ ntfnObj ntfna);
ntfn' <- case queue' of [] \<Rightarrow> return $ Structures_H.ntfn.IdleNtfn | a # list \<Rightarrow> return $ ntfnQueue_update (\<lambda>_. queue') (ntfnObj ntfna);
setNotification ntfn (ntfnObj_update (\<lambda>_. ntfn') ntfna);
setThreadState Structures_H.thread_state.Inactive t
od \<lbrace>\<lambda>rv. valid_queues'\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> do ntfna <- getNotification ntfn;
haskell_assert (case ntfnObj ntfna of Structures_H.ntfn.WaitingNtfn x \<Rightarrow> True | _ \<Rightarrow> False) [];
queue' <- return (delete t $ ntfnQueue $ ntfnObj ntfna);
ntfn' <- case queue' of [] \<Rightarrow> return $ Structures_H.ntfn.IdleNtfn | a # list \<Rightarrow> return $ ntfnQueue_update (\<lambda>_. queue') (ntfnObj ntfna);
setNotification ntfn (ntfnObj_update (\<lambda>_. ntfn') ntfna);
setThreadState Structures_H.thread_state.Inactive t
od \<lbrace>\<lambda>rv. valid_queues'\<rbrace>
 2. \<And>s. valid_queues' s \<and> valid_objs' s \<Longrightarrow> ?Q s proof (prove)
goal:
No subgoals!
theory Orphanage

lemma restart_no_orphans [wp]:
  "\<lbrace> \<lambda>s. no_orphans s \<and> invs' s \<and> sch_act_simple s \<and> tcb_at' t s \<rbrace>
   restart t
   \<lbrace> \<lambda>rv s. no_orphans s \<rbrace>" unfolding restart_def isStopped_def2 apply (wp tcbSchedEnqueue_almost_no_orphans sts_st_tcb' cancelIPC_weak_sch_act_wf
         | clarsimp simp: o_def if_apply_def2
         | strengthen no_orphans_strg_almost
         | strengthen invs_valid_queues'
         | wp (once) hoare_drop_imps)+ apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. no_orphans s \<and> invs' s \<and> sch_act_simple s \<and> tcb_at' t s\<rbrace> ThreadDecls_H.restart t \<lbrace>\<lambda>rv. no_orphans\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. no_orphans s \<and> invs' s \<and> sch_act_simple s \<and> tcb_at' t s\<rbrace> do blocked <- liftM (Not \<circ> activatable') (getThreadState t);
when blocked $ do cancelIPC t;
setupReplyMaster t;
setThreadState Structures_H.thread_state.Restart t;
tcbSchedEnqueue t;
possibleSwitchTo t
od
od \<lbrace>\<lambda>rv. no_orphans\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>no_orphans s; invs' s; sch_act_simple s; tcb_at' t s\<rbrakk> \<Longrightarrow> valid_objs' s \<and> sch_act_wf (ksSchedulerAction s) s \<and> weak_sch_act_wf (ksSchedulerAction s) s proof (prove)
goal:
No subgoals!
theory Orphanage

lemma almost_no_orphans_no_orphans':
  "\<lbrakk> almost_no_orphans t s; ksCurThread s = t\<rbrakk> \<Longrightarrow> no_orphans s" by (auto simp: almost_no_orphans_def no_orphans_def all_active_tcb_ptrs_def)

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

lemma setMCPriority_no_orphans[wp]:
  "\<lbrace>no_orphans\<rbrace> setMCPriority t prio \<lbrace>\<lambda>rv. no_orphans\<rbrace>" unfolding setMCPriority_def apply (rule hoare_pre) apply (wp threadSet_no_orphans) by clarsimp+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>no_orphans\<rbrace> setMCPriority t prio \<lbrace>\<lambda>rv. no_orphans\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>no_orphans\<rbrace> threadSet (tcbMCP_update (\<lambda>_. prio)) t \<lbrace>\<lambda>rv. no_orphans\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> threadSet (tcbMCP_update (\<lambda>_. prio)) t \<lbrace>\<lambda>rv. no_orphans\<rbrace>
 2. \<And>s. no_orphans s \<Longrightarrow> ?Q s proof (prove)
goal (2 subgoals):
 1. \<forall>tcb. \<not> is_active_thread_state (tcbState tcb) \<longrightarrow> \<not> is_active_thread_state (tcbState (tcbMCP_update (\<lambda>_. prio) tcb))
 2. \<And>s. no_orphans s \<Longrightarrow> no_orphans s
theory Orphanage

lemma threadSet_ipcbuffer_invs:
  "is_aligned a msg_align_bits \<Longrightarrow>
  \<lbrace>invs' and tcb_at' t\<rbrace> threadSet (tcbIPCBuffer_update (\<lambda>_. a)) t \<lbrace>\<lambda>rv. invs'\<rbrace>" apply (wp threadSet_invs_trivial, simp_all add: inQ_def cong: conj_cong) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_aligned a msg_align_bits \<Longrightarrow> \<lbrace>invs' and tcb_at' t\<rbrace> threadSet (tcbIPCBuffer_update (\<lambda>_. a)) t \<lbrace>\<lambda>rv. invs'\<rbrace> proof (prove)
goal:
No subgoals!