theory Orphanage

lemma cancelAllSignals_no_orphans [wp]:
  "\<lbrace> \<lambda>s. no_orphans s \<and> valid_queues' s \<and> valid_objs' s \<rbrace>
    cancelAllSignals ntfn
   \<lbrace> \<lambda>rv s. no_orphans s \<rbrace>" unfolding cancelAllSignals_def apply (wp sts_valid_objs' set_ntfn_valid_objs' sts_st_tcb'
            hoare_vcg_const_Ball_lift tcbSchedEnqueue_almost_no_orphans
             | wpc
             | clarsimp simp: valid_tcb_state'_def)+ apply (rename_tac list) apply (rule_tac V="\<lambda>_. valid_queues' and valid_objs'"
                and I="no_orphans and (\<lambda>s. \<forall>t\<in>set list. tcb_at' t s)"
                in mapM_x_inv_wp2) apply simp apply (wp sts_valid_objs' set_ntfn_valid_objs' sts_st_tcb'
            hoare_vcg_const_Ball_lift tcbSchedEnqueue_almost_no_orphans|
          clarsimp simp: valid_tcb_state'_def)+ apply (rule_tac Q="\<lambda>rv. no_orphans and valid_objs' and valid_queues' and ko_at' rv ntfn"
                 in hoare_post_imp) apply (fastforce simp: valid_obj'_def valid_ntfn'_def obj_at'_def projectKOs) apply (wp get_ntfn_sp' | clarsimp)+ 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> cancelAllSignals ntfn \<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 ntfna <- getNotification ntfn;
case ntfnObj ntfna of Structures_H.ntfn.WaitingNtfn queue \<Rightarrow> do setNotification ntfn (ntfnObj_update (\<lambda>_. Structures_H.ntfn.IdleNtfn) ntfna);
forM_x queue (\<lambda>t. do setThreadState Structures_H.thread_state.Restart t;
tcbSchedEnqueue t
od);
rescheduleRequired
od | _ \<Rightarrow> return ()
od \<lbrace>\<lambda>rv. no_orphans\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>ntfn x3. ntfnObj ntfn = Structures_H.ntfn.WaitingNtfn x3 \<Longrightarrow> \<lbrace>?B25 ntfn x3 ()\<rbrace> mapM_x (\<lambda>t. do y <- setThreadState Structures_H.thread_state.Restart t;
tcbSchedEnqueue t
od) x3 \<lbrace>\<lambda>xa s. no_orphans s \<and> valid_queues' s\<rbrace>
 2. \<And>ntfna x3. ntfnObj ntfna = Structures_H.ntfn.WaitingNtfn x3 \<Longrightarrow> \<lbrace>?R15 ntfna x3\<rbrace> setNotification ntfn (ntfnObj_update (\<lambda>_. Structures_H.ntfn.IdleNtfn) ntfna) \<lbrace>?B25 ntfna x3\<rbrace>
 3. \<lbrace>?Q\<rbrace> getNotification ntfn \<lbrace>\<lambda>ntfn s. (ntfnObj ntfn = Structures_H.ntfn.IdleNtfn \<longrightarrow> no_orphans s) \<and> (\<forall>x. ntfnObj ntfn = Structures_H.ntfn.ActiveNtfn x \<longrightarrow> no_orphans s) \<and> (\<forall>x. ntfnObj ntfn = Structures_H.ntfn.WaitingNtfn x \<longrightarrow> ?R15 ntfn x s)\<rbrace>
 4. \<And>s. no_orphans s \<and> valid_queues' s \<and> valid_objs' s \<Longrightarrow> ?Q s proof (prove)
goal (4 subgoals):
 1. \<And>ntfn list. ntfnObj ntfn = Structures_H.ntfn.WaitingNtfn list \<Longrightarrow> \<lbrace>?B25 ntfn list ()\<rbrace> mapM_x (\<lambda>t. do y <- setThreadState Structures_H.thread_state.Restart t;
tcbSchedEnqueue t
od) list \<lbrace>\<lambda>xa s. no_orphans s \<and> valid_queues' s\<rbrace>
 2. \<And>ntfna x3. ntfnObj ntfna = Structures_H.ntfn.WaitingNtfn x3 \<Longrightarrow> \<lbrace>?R15 ntfna x3\<rbrace> setNotification ntfn (ntfnObj_update (\<lambda>_. Structures_H.ntfn.IdleNtfn) ntfna) \<lbrace>?B25 ntfna x3\<rbrace>
 3. \<lbrace>?Q\<rbrace> getNotification ntfn \<lbrace>\<lambda>ntfn s. (ntfnObj ntfn = Structures_H.ntfn.IdleNtfn \<longrightarrow> no_orphans s) \<and> (\<forall>x. ntfnObj ntfn = Structures_H.ntfn.ActiveNtfn x \<longrightarrow> no_orphans s) \<and> (\<forall>x. ntfnObj ntfn = Structures_H.ntfn.WaitingNtfn x \<longrightarrow> ?R15 ntfn x s)\<rbrace>
 4. \<And>s. no_orphans s \<and> valid_queues' s \<and> valid_objs' s \<Longrightarrow> ?Q s proof (prove)
goal (5 subgoals):
 1. \<And>ntfn list s. \<lbrakk>ntfnObj ntfn = Structures_H.ntfn.WaitingNtfn list; (no_orphans and (\<lambda>s. \<forall>t\<in>set list. tcb_at' t s)) s; (valid_queues' and valid_objs') s\<rbrakk> \<Longrightarrow> no_orphans s \<and> valid_queues' s
 2. \<And>ntfn list a as. \<lbrakk>ntfnObj ntfn = Structures_H.ntfn.WaitingNtfn list; suffix (a # as) list\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. (no_orphans and (\<lambda>s. \<forall>t\<in>set list. tcb_at' t s)) s \<and> (valid_queues' and valid_objs') s\<rbrace> do y <- setThreadState Structures_H.thread_state.Restart a;
tcbSchedEnqueue a
od \<lbrace>\<lambda>r s. (no_orphans and (\<lambda>s. \<forall>t\<in>set list. tcb_at' t s)) s \<and> (valid_queues' and valid_objs') s\<rbrace>
 3. \<And>ntfna x3. ntfnObj ntfna = Structures_H.ntfn.WaitingNtfn x3 \<Longrightarrow> \<lbrace>?R15 ntfna x3\<rbrace> setNotification ntfn (ntfnObj_update (\<lambda>_. Structures_H.ntfn.IdleNtfn) ntfna) \<lbrace>\<lambda>a. no_orphans and (\<lambda>s. \<forall>t\<in>set x3. tcb_at' t s) and (valid_queues' and valid_objs')\<rbrace>
 4. \<lbrace>?Q\<rbrace> getNotification ntfn \<lbrace>\<lambda>ntfn s. (ntfnObj ntfn = Structures_H.ntfn.IdleNtfn \<longrightarrow> no_orphans s) \<and> (\<forall>x. ntfnObj ntfn = Structures_H.ntfn.ActiveNtfn x \<longrightarrow> no_orphans s) \<and> (\<forall>x. ntfnObj ntfn = Structures_H.ntfn.WaitingNtfn x \<longrightarrow> ?R15 ntfn x s)\<rbrace>
 5. \<And>s. no_orphans s \<and> valid_queues' s \<and> valid_objs' s \<Longrightarrow> ?Q s proof (prove)
goal (4 subgoals):
 1. \<And>ntfn list a as. \<lbrakk>ntfnObj ntfn = Structures_H.ntfn.WaitingNtfn list; suffix (a # as) list\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. (no_orphans and (\<lambda>s. \<forall>t\<in>set list. tcb_at' t s)) s \<and> (valid_queues' and valid_objs') s\<rbrace> do y <- setThreadState Structures_H.thread_state.Restart a;
tcbSchedEnqueue a
od \<lbrace>\<lambda>r s. (no_orphans and (\<lambda>s. \<forall>t\<in>set list. tcb_at' t s)) s \<and> (valid_queues' and valid_objs') s\<rbrace>
 2. \<And>ntfna x3. ntfnObj ntfna = Structures_H.ntfn.WaitingNtfn x3 \<Longrightarrow> \<lbrace>?R15 ntfna x3\<rbrace> setNotification ntfn (ntfnObj_update (\<lambda>_. Structures_H.ntfn.IdleNtfn) ntfna) \<lbrace>\<lambda>a. no_orphans and (\<lambda>s. \<forall>t\<in>set x3. tcb_at' t s) and (valid_queues' and valid_objs')\<rbrace>
 3. \<lbrace>?Q\<rbrace> getNotification ntfn \<lbrace>\<lambda>ntfn s. (ntfnObj ntfn = Structures_H.ntfn.IdleNtfn \<longrightarrow> no_orphans s) \<and> (\<forall>x. ntfnObj ntfn = Structures_H.ntfn.ActiveNtfn x \<longrightarrow> no_orphans s) \<and> (\<forall>x. ntfnObj ntfn = Structures_H.ntfn.WaitingNtfn x \<longrightarrow> ?R15 ntfn x s)\<rbrace>
 4. \<And>s. no_orphans s \<and> valid_queues' s \<and> valid_objs' s \<Longrightarrow> ?Q s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> getNotification ntfn \<lbrace>\<lambda>ntfn s. (ntfnObj ntfn = Structures_H.ntfn.IdleNtfn \<longrightarrow> no_orphans s) \<and> ((\<exists>x. ntfnObj ntfn = Structures_H.ntfn.ActiveNtfn x) \<longrightarrow> no_orphans s) \<and> (\<forall>x. ntfnObj ntfn = Structures_H.ntfn.WaitingNtfn x \<longrightarrow> no_orphans s \<and> (\<forall>x\<in>set x. tcb_at' x s) \<and> valid_queues' s \<and> valid_objs' s \<and> valid_ntfn' (ntfnObj_update (\<lambda>_. Structures_H.ntfn.IdleNtfn) ntfn) s)\<rbrace>
 2. \<And>s. no_orphans s \<and> valid_queues' s \<and> valid_objs' s \<Longrightarrow> ?Q s proof (prove)
goal (3 subgoals):
 1. \<And>rv s. (no_orphans and valid_objs' and valid_queues' and ko_at' rv ntfn) s \<Longrightarrow> (ntfnObj rv = Structures_H.ntfn.IdleNtfn \<longrightarrow> no_orphans s) \<and> ((\<exists>x. ntfnObj rv = Structures_H.ntfn.ActiveNtfn x) \<longrightarrow> no_orphans s) \<and> (\<forall>x. ntfnObj rv = Structures_H.ntfn.WaitingNtfn x \<longrightarrow> no_orphans s \<and> (\<forall>x\<in>set x. tcb_at' x s) \<and> valid_queues' s \<and> valid_objs' s \<and> valid_ntfn' (ntfnObj_update (\<lambda>_. Structures_H.ntfn.IdleNtfn) rv) s)
 2. \<lbrace>?Q\<rbrace> getNotification ntfn \<lbrace>\<lambda>rv. no_orphans and valid_objs' and valid_queues' and ko_at' rv ntfn\<rbrace>
 3. \<And>s. no_orphans s \<and> valid_queues' s \<and> valid_objs' s \<Longrightarrow> ?Q s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> getNotification ntfn \<lbrace>\<lambda>rv. no_orphans and valid_objs' and valid_queues' and ko_at' rv ntfn\<rbrace>
 2. \<And>s. no_orphans s \<and> valid_queues' s \<and> valid_objs' s \<Longrightarrow> ?Q s proof (prove)
goal:
No subgoals!