theory Orphanage

lemma createObjects_no_orphans [wp]:
  "\<lbrace> \<lambda>s. no_orphans s \<and> pspace_aligned' s \<and> pspace_no_overlap' ptr sz s \<and> pspace_distinct' s
      \<and> n \<noteq> 0 \<and> range_cover ptr sz (objBitsKO val + gbits) n
      \<and> \<not> case_option False (is_active_thread_state \<circ> tcbState) (projectKO_opt val) \<rbrace>
   createObjects ptr n val gbits
   \<lbrace> \<lambda>rv s. no_orphans s \<rbrace>" apply (clarsimp simp: no_orphans_def all_active_tcb_ptrs_def
                        is_active_tcb_ptr_def all_queued_tcb_ptrs_def) apply (simp only: imp_conv_disj pred_tcb_at'_def createObjects_def) apply (wp hoare_vcg_all_lift hoare_vcg_disj_lift createObjects_orig_obj_at2') apply clarsimp apply (erule(1) impE) apply clarsimp apply (drule_tac x = x in spec) apply (erule impE) apply (clarsimp simp:obj_at'_def projectKOs split: option.splits) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. no_orphans s \<and> pspace_aligned' s \<and> pspace_no_overlap' ptr sz s \<and> pspace_distinct' s \<and> n \<noteq> 0 \<and> range_cover ptr sz (objBitsKO val + gbits) n \<and> \<not> (case projectKO_opt val of None \<Rightarrow> False | Some x \<Rightarrow> (is_active_thread_state \<circ> tcbState) x)\<rbrace> createObjects ptr n val gbits \<lbrace>\<lambda>rv. no_orphans\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. (\<forall>tcb_ptr. st_tcb_at' is_active_thread_state tcb_ptr s \<longrightarrow> tcb_ptr = ksCurThread s \<or> (\<exists>a b. tcb_ptr \<in> set (ksReadyQueues s (a, b))) \<or> ksSchedulerAction s = SwitchToThread tcb_ptr) \<and> pspace_aligned' s \<and> pspace_no_overlap' ptr sz s \<and> pspace_distinct' s \<and> 0 < n \<and> range_cover ptr sz (objBitsKO val + gbits) n \<and> \<not> (case projectKO_opt val of None \<Rightarrow> False | Some x2 \<Rightarrow> is_active_thread_state (tcbState x2))\<rbrace> createObjects ptr n val gbits \<lbrace>\<lambda>rv s. \<forall>tcb_ptr. st_tcb_at' is_active_thread_state tcb_ptr s \<longrightarrow> tcb_ptr = ksCurThread s \<or> (\<exists>a b. tcb_ptr \<in> set (ksReadyQueues s (a, b))) \<or> ksSchedulerAction s = SwitchToThread tcb_ptr\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. (\<forall>tcb_ptr. \<not> obj_at' (\<lambda>ko. is_active_thread_state (itcbState (tcb_to_itcb' ko))) tcb_ptr s \<or> tcb_ptr = ksCurThread s \<or> (\<exists>a b. tcb_ptr \<in> set (ksReadyQueues s (a, b))) \<or> ksSchedulerAction s = SwitchToThread tcb_ptr) \<and> pspace_aligned' s \<and> pspace_no_overlap' ptr sz s \<and> pspace_distinct' s \<and> 0 < n \<and> range_cover ptr sz (objBitsKO val + gbits) n \<and> \<not> (case projectKO_opt val of None \<Rightarrow> False | Some x2 \<Rightarrow> is_active_thread_state (tcbState x2))\<rbrace> do oBits <- return (objBitsKO val);
gBits <- return (oBits + gbits);
createObjects' ptr n val gbits;
return (map (\<lambda>n. ptr + n `~shiftL~` gBits) [0 .e. word_of_nat n - 1])
od \<lbrace>\<lambda>rv s. \<forall>tcb_ptr. \<not> obj_at' (\<lambda>ko. is_active_thread_state (itcbState (tcb_to_itcb' ko))) tcb_ptr s \<or> tcb_ptr = ksCurThread s \<or> (\<exists>a b. tcb_ptr \<in> set (ksReadyQueues s (a, b))) \<or> ksSchedulerAction s = SwitchToThread tcb_ptr\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (\<forall>tcb_ptr. \<not> obj_at' (\<lambda>ko. is_active_thread_state (itcbState (tcb_to_itcb' ko))) tcb_ptr s \<or> tcb_ptr = ksCurThread s \<or> (\<exists>a b. tcb_ptr \<in> set (ksReadyQueues s (a, b))) \<or> ksSchedulerAction s = SwitchToThread tcb_ptr) \<and> pspace_aligned' s \<and> pspace_no_overlap' ptr sz s \<and> pspace_distinct' s \<and> 0 < n \<and> range_cover ptr sz (objBitsKO val + gbits) n \<and> \<not> (case projectKO_opt val of None \<Rightarrow> False | Some x2 \<Rightarrow> is_active_thread_state (tcbState x2)) \<Longrightarrow> \<forall>x. n \<noteq> 0 \<and> range_cover ptr (?sz12 x (objBitsKO val) (objBitsKO val + gbits)) (objBitsKO val + gbits) n \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> \<not> obj_at' (\<lambda>a. is_active_thread_state (itcbState (tcb_to_itcb' a))) x s \<and> \<not> (case projectKO_opt val of None \<Rightarrow> False | Some a \<Rightarrow> is_active_thread_state (itcbState (tcb_to_itcb' a))) \<and> pspace_no_overlap' ptr (?sz12 x (objBitsKO val) (objBitsKO val + gbits)) s \<or> x = ksCurThread s \<or> (\<exists>a b. x \<in> set (ksReadyQueues s (a, b))) \<or> ksSchedulerAction s = SwitchToThread x proof (prove)
goal (1 subgoal):
 1. \<And>s x. \<lbrakk>\<forall>tcb_ptr. obj_at' (\<lambda>ko. is_active_thread_state (tcbState ko)) tcb_ptr s \<longrightarrow> tcb_ptr = ksCurThread s \<or> (\<exists>a b. tcb_ptr \<in> set (ksReadyQueues s (a, b))) \<or> ksSchedulerAction s = SwitchToThread tcb_ptr; pspace_aligned' s; pspace_no_overlap' ptr sz s; pspace_distinct' s; 0 < n; range_cover ptr sz (objBitsKO val + gbits) n; \<not> (case projectKO_opt val of None \<Rightarrow> False | Some x2 \<Rightarrow> is_active_thread_state (tcbState x2)); range_cover ptr (?sz12 x (objBitsKO val) (objBitsKO val + gbits)) (objBitsKO val + gbits) n \<longrightarrow> obj_at' (\<lambda>a. is_active_thread_state (tcbState a)) x s \<or> \<not> pspace_no_overlap' ptr (?sz12 x (objBitsKO val) (objBitsKO val + gbits)) s; x \<noteq> ksCurThread s; sch_act_not x s\<rbrakk> \<Longrightarrow> \<exists>a b. x \<in> set (ksReadyQueues s (a, b)) proof (prove)
goal (1 subgoal):
 1. \<And>s x. \<lbrakk>\<forall>tcb_ptr. obj_at' (\<lambda>ko. is_active_thread_state (tcbState ko)) tcb_ptr s \<longrightarrow> tcb_ptr = ksCurThread s \<or> (\<exists>a b. tcb_ptr \<in> set (ksReadyQueues s (a, b))) \<or> ksSchedulerAction s = SwitchToThread tcb_ptr; pspace_aligned' s; pspace_no_overlap' ptr sz s; pspace_distinct' s; 0 < n; range_cover ptr sz (objBitsKO val + gbits) n; \<not> (case projectKO_opt val of None \<Rightarrow> False | Some x2 \<Rightarrow> is_active_thread_state (tcbState x2)); x \<noteq> ksCurThread s; sch_act_not x s; obj_at' (\<lambda>a. is_active_thread_state (tcbState a)) x s \<or> \<not> pspace_no_overlap' ptr sz s\<rbrakk> \<Longrightarrow> \<exists>a b. x \<in> set (ksReadyQueues s (a, b)) proof (prove)
goal (1 subgoal):
 1. \<And>s x. \<lbrakk>\<forall>tcb_ptr. obj_at' (\<lambda>ko. is_active_thread_state (tcbState ko)) tcb_ptr s \<longrightarrow> tcb_ptr = ksCurThread s \<or> (\<exists>a b. tcb_ptr \<in> set (ksReadyQueues s (a, b))) \<or> ksSchedulerAction s = SwitchToThread tcb_ptr; pspace_aligned' s; pspace_no_overlap' ptr sz s; pspace_distinct' s; 0 < n; range_cover ptr sz (objBitsKO val + gbits) n; \<not> (case projectKO_opt val of None \<Rightarrow> False | Some x2 \<Rightarrow> is_active_thread_state (tcbState x2)); x \<noteq> ksCurThread s; sch_act_not x s; obj_at' (\<lambda>a. is_active_thread_state (tcbState a)) x s\<rbrakk> \<Longrightarrow> \<exists>a b. x \<in> set (ksReadyQueues s (a, b)) proof (prove)
goal (1 subgoal):
 1. \<And>s x. \<lbrakk>pspace_aligned' s; pspace_no_overlap' ptr sz s; pspace_distinct' s; 0 < n; range_cover ptr sz (objBitsKO val + gbits) n; \<not> (case projectKO_opt val of None \<Rightarrow> False | Some x2 \<Rightarrow> is_active_thread_state (tcbState x2)); x \<noteq> ksCurThread s; sch_act_not x s; obj_at' (\<lambda>a. is_active_thread_state (tcbState a)) x s; obj_at' (\<lambda>ko. is_active_thread_state (tcbState ko)) x s \<longrightarrow> x = ksCurThread s \<or> (\<exists>a b. x \<in> set (ksReadyQueues s (a, b))) \<or> ksSchedulerAction s = SwitchToThread x\<rbrakk> \<Longrightarrow> \<exists>a b. x \<in> set (ksReadyQueues s (a, b)) proof (prove)
goal (2 subgoals):
 1. \<And>s x. \<lbrakk>pspace_aligned' s; pspace_no_overlap' ptr sz s; pspace_distinct' s; 0 < n; range_cover ptr sz (objBitsKO val + gbits) n; \<not> (case projectKO_opt val of None \<Rightarrow> False | Some x2 \<Rightarrow> is_active_thread_state (tcbState x2)); x \<noteq> ksCurThread s; sch_act_not x s; obj_at' (\<lambda>a. is_active_thread_state (tcbState a)) x s\<rbrakk> \<Longrightarrow> obj_at' (\<lambda>ko. is_active_thread_state (tcbState ko)) x s
 2. \<And>s x. \<lbrakk>pspace_aligned' s; pspace_no_overlap' ptr sz s; pspace_distinct' s; 0 < n; range_cover ptr sz (objBitsKO val + gbits) n; \<not> (case projectKO_opt val of None \<Rightarrow> False | Some x2 \<Rightarrow> is_active_thread_state (tcbState x2)); x \<noteq> ksCurThread s; sch_act_not x s; obj_at' (\<lambda>a. is_active_thread_state (tcbState a)) x s; x = ksCurThread s \<or> (\<exists>a b. x \<in> set (ksReadyQueues s (a, b))) \<or> ksSchedulerAction s = SwitchToThread x\<rbrakk> \<Longrightarrow> \<exists>a b. x \<in> set (ksReadyQueues s (a, b)) proof (prove)
goal (1 subgoal):
 1. \<And>s x. \<lbrakk>pspace_aligned' s; pspace_no_overlap' ptr sz s; pspace_distinct' s; 0 < n; range_cover ptr sz (objBitsKO val + gbits) n; \<not> (case projectKO_opt val of None \<Rightarrow> False | Some x2 \<Rightarrow> is_active_thread_state (tcbState x2)); x \<noteq> ksCurThread s; sch_act_not x s; obj_at' (\<lambda>a. is_active_thread_state (tcbState a)) x s; x = ksCurThread s \<or> (\<exists>a b. x \<in> set (ksReadyQueues s (a, b))) \<or> ksSchedulerAction s = SwitchToThread x\<rbrakk> \<Longrightarrow> \<exists>a b. x \<in> set (ksReadyQueues s (a, b)) proof (prove)
goal:
No subgoals!