theory CNode_DR

lemma reply_cap_insert_corres:
  "sid \<noteq> did\<Longrightarrow>dcorres dc \<top>
    (valid_idle and not_idle_thread did and valid_mdb and st_tcb_at (\<lambda>r. \<not> inactive r \<and> \<not> idle r) sid
     and valid_etcbs and tcb_at did and tcb_at sid and valid_objs)
    (insert_cap_child (cdl_cap.ReplyCap sid rights)  (sid, tcb_replycap_slot)
      (did, tcb_caller_slot))
    (cap_insert (cap.ReplyCap sid False rights) (sid,tcb_cnode_index 2) (did,tcb_cnode_index 3))" apply (rule corres_guard_imp) apply (rule insert_cap_child_corres [where cap = "cap.ReplyCap sid False rights"
      and src = "(sid, tcb_cnode_index 2)" and child = "(did, tcb_cnode_index 3)",
      unfolded transform_cap_def transform_tcb_slot_simp
      ,simplified]) apply clarsimp+ apply (frule st_tcb_at_reply_cap_valid) apply simp+ apply (frule tcb_caller_cap) apply simp+ apply (clarsimp simp:cte_wp_at_caps_of_state should_be_parent_of_def) apply (clarsimp simp: word_bits_def is_master_reply_cap_def
   split:cap.splits) apply (rule conjI) apply (drule caps_of_state_cteD)+ apply (frule(1) cte_wp_tcb_cap_valid) apply (clarsimp simp:valid_mdb_def reply_master_revocable_def) apply (drule_tac x = "sid" in spec) apply (drule_tac x = "tcb_cnode_index 2" in spec) apply (clarsimp simp:cte_wp_at_caps_of_state is_master_reply_cap_def) apply (drule caps_of_state_cteD)+ apply (frule(1) cte_wp_tcb_cap_valid[where p = "(did,tcb_cnode_index 3)"]) apply (rule conjI) apply (clarsimp simp:valid_idle_def not_idle_thread_def) apply (clarsimp simp:pred_tcb_at_def2 obj_at_def) apply (clarsimp simp:tcb_at_def dest!:get_tcb_SomeD) apply (drule cte_wp_valid_cap) apply simp apply (simp add:valid_cap_def cap_aligned_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. sid \<noteq> did \<Longrightarrow> dcorres dc (\<lambda>_. True) (valid_idle and not_idle_thread did and valid_mdb and st_tcb_at (\<lambda>r. r \<noteq> Inactive \<and> r \<noteq> IdleThreadState) sid and valid_etcbs and tcb_at did and tcb_at sid and valid_objs) (insert_cap_child (cdl_cap.ReplyCap sid rights) (sid, tcb_replycap_slot) (did, tcb_caller_slot)) (cap_insert (cap.ReplyCap sid False rights) (sid, tcb_cnode_index 2) (did, tcb_cnode_index 3)) proof (prove)
goal (3 subgoals):
 1. sid \<noteq> did \<Longrightarrow> dcorres dc ?Q ?Q' (insert_cap_child (cdl_cap.ReplyCap sid rights) (sid, tcb_replycap_slot) (did, tcb_caller_slot)) (cap_insert (cap.ReplyCap sid False rights) (sid, tcb_cnode_index 2) (did, tcb_cnode_index 3))
 2. \<And>s. \<lbrakk>sid \<noteq> did; True\<rbrakk> \<Longrightarrow> ?Q s
 3. \<And>s. \<lbrakk>sid \<noteq> did; (valid_idle and not_idle_thread did and valid_mdb and st_tcb_at (\<lambda>r. r \<noteq> Inactive \<and> r \<noteq> IdleThreadState) sid and valid_etcbs and tcb_at did and tcb_at sid and valid_objs) s\<rbrakk> \<Longrightarrow> ?Q' s proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>sid \<noteq> did; True\<rbrakk> \<Longrightarrow> True
 2. \<And>s. \<lbrakk>sid \<noteq> did; (valid_idle and not_idle_thread did and valid_mdb and st_tcb_at (\<lambda>r. r \<noteq> Inactive \<and> r \<noteq> IdleThreadState) sid and valid_etcbs and tcb_at did and tcb_at sid and valid_objs) s\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>cap'. should_be_parent_of cap' (is_original_cap s (sid, tcb_cnode_index 2)) (cap.ReplyCap sid False rights) (cap_insert_dest_original (cap.ReplyCap sid False rights) cap')) (sid, tcb_cnode_index 2) s \<and> not_idle_thread did s \<and> valid_idle s \<and> valid_etcbs s \<and> valid_mdb s \<and> not_idle_thread sid s \<and> valid_objs s \<and> cap_aligned (cap.ReplyCap sid False rights) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>sid \<noteq> did; valid_idle s; not_idle_thread did s; valid_mdb s; st_tcb_at (\<lambda>r. r \<noteq> Inactive \<and> r \<noteq> IdleThreadState) sid s; valid_etcbs s; tcb_at did s; tcb_at sid s; valid_objs s\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>cap'. should_be_parent_of cap' (is_original_cap s (sid, tcb_cnode_index 2)) (cap.ReplyCap sid False rights) (cap_insert_dest_original (cap.ReplyCap sid False rights) cap')) (sid, tcb_cnode_index 2) s \<and> not_idle_thread sid s \<and> cap_aligned (cap.ReplyCap sid False rights) proof (prove)
goal (4 subgoals):
 1. \<And>s. \<lbrakk>sid \<noteq> did; valid_idle s; not_idle_thread did s; valid_mdb s; st_tcb_at (\<lambda>r. r \<noteq> Inactive \<and> r \<noteq> IdleThreadState) sid s; valid_etcbs s; tcb_at did s; tcb_at sid s; valid_objs s\<rbrakk> \<Longrightarrow> valid_objs s
 2. \<And>s. \<lbrakk>sid \<noteq> did; valid_idle s; not_idle_thread did s; valid_mdb s; st_tcb_at (\<lambda>r. r \<noteq> Inactive \<and> r \<noteq> IdleThreadState) sid s; valid_etcbs s; tcb_at did s; tcb_at sid s; valid_objs s\<rbrakk> \<Longrightarrow> True
 3. \<And>s. \<lbrakk>sid \<noteq> did; valid_idle s; not_idle_thread did s; valid_mdb s; st_tcb_at (\<lambda>r. r \<noteq> Inactive \<and> r \<noteq> IdleThreadState) sid s; valid_etcbs s; tcb_at did s; tcb_at sid s; valid_objs s\<rbrakk> \<Longrightarrow> \<not> (Inactive \<noteq> Inactive \<and> Inactive \<noteq> IdleThreadState) \<and> \<not> (IdleThreadState \<noteq> Inactive \<and> IdleThreadState \<noteq> IdleThreadState)
 4. \<And>s. \<lbrakk>sid \<noteq> did; valid_idle s; not_idle_thread did s; valid_mdb s; st_tcb_at (\<lambda>r. r \<noteq> Inactive \<and> r \<noteq> IdleThreadState) sid s; valid_etcbs s; tcb_at did s; tcb_at sid s; valid_objs s; cte_wp_at (\<lambda>cap. is_master_reply_cap cap \<and> obj_ref_of cap = sid) (sid, tcb_cnode_index 2) s\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>cap'. should_be_parent_of cap' (is_original_cap s (sid, tcb_cnode_index 2)) (cap.ReplyCap sid False rights) (cap_insert_dest_original (cap.ReplyCap sid False rights) cap')) (sid, tcb_cnode_index 2) s \<and> not_idle_thread sid s \<and> cap_aligned (cap.ReplyCap sid False rights) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>sid \<noteq> did; valid_idle s; not_idle_thread did s; valid_mdb s; st_tcb_at (\<lambda>r. r \<noteq> Inactive \<and> r \<noteq> IdleThreadState) sid s; valid_etcbs s; tcb_at did s; tcb_at sid s; valid_objs s; cte_wp_at (\<lambda>cap. is_master_reply_cap cap \<and> obj_ref_of cap = sid) (sid, tcb_cnode_index 2) s\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>cap'. should_be_parent_of cap' (is_original_cap s (sid, tcb_cnode_index 2)) (cap.ReplyCap sid False rights) (cap_insert_dest_original (cap.ReplyCap sid False rights) cap')) (sid, tcb_cnode_index 2) s \<and> not_idle_thread sid s \<and> cap_aligned (cap.ReplyCap sid False rights) proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>sid \<noteq> did; valid_idle s; not_idle_thread did s; valid_mdb s; st_tcb_at (\<lambda>r. r \<noteq> Inactive \<and> r \<noteq> IdleThreadState) sid s; valid_etcbs s; tcb_at did s; tcb_at sid s; valid_objs s; cte_wp_at (\<lambda>cap. is_master_reply_cap cap \<and> obj_ref_of cap = sid) (sid, tcb_cnode_index 2) s\<rbrakk> \<Longrightarrow> valid_objs s
 2. \<And>s. \<lbrakk>sid \<noteq> did; valid_idle s; not_idle_thread did s; valid_mdb s; st_tcb_at (\<lambda>r. r \<noteq> Inactive \<and> r \<noteq> IdleThreadState) sid s; valid_etcbs s; tcb_at did s; tcb_at sid s; valid_objs s; cte_wp_at (\<lambda>cap. is_master_reply_cap cap \<and> obj_ref_of cap = sid) (sid, tcb_cnode_index 2) s; cte_wp_at (is_reply_cap or (=) cap.NullCap) (did, tcb_cnode_index 3) s\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>cap'. should_be_parent_of cap' (is_original_cap s (sid, tcb_cnode_index 2)) (cap.ReplyCap sid False rights) (cap_insert_dest_original (cap.ReplyCap sid False rights) cap')) (sid, tcb_cnode_index 2) s \<and> not_idle_thread sid s \<and> cap_aligned (cap.ReplyCap sid False rights) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>sid \<noteq> did; valid_idle s; not_idle_thread did s; valid_mdb s; st_tcb_at (\<lambda>r. r \<noteq> Inactive \<and> r \<noteq> IdleThreadState) sid s; valid_etcbs s; tcb_at did s; tcb_at sid s; valid_objs s; cte_wp_at (\<lambda>cap. is_master_reply_cap cap \<and> obj_ref_of cap = sid) (sid, tcb_cnode_index 2) s; cte_wp_at (is_reply_cap or (=) cap.NullCap) (did, tcb_cnode_index 3) s\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>cap'. should_be_parent_of cap' (is_original_cap s (sid, tcb_cnode_index 2)) (cap.ReplyCap sid False rights) (cap_insert_dest_original (cap.ReplyCap sid False rights) cap')) (sid, tcb_cnode_index 2) s \<and> not_idle_thread sid s \<and> cap_aligned (cap.ReplyCap sid False rights) proof (prove)
goal (1 subgoal):
 1. \<And>s cap capa. \<lbrakk>obj_ref_of cap \<noteq> did; valid_idle s; not_idle_thread did s; valid_mdb s; st_tcb_at (\<lambda>r. r \<noteq> Inactive \<and> r \<noteq> IdleThreadState) (obj_ref_of cap) s; valid_etcbs s; tcb_at did s; tcb_at (obj_ref_of cap) s; valid_objs s; caps_of_state s (obj_ref_of cap, tcb_cnode_index 2) = Some cap; caps_of_state s (did, tcb_cnode_index 3) = Some capa; is_reply_cap capa \<or> cap.NullCap = capa; is_master_reply_cap cap; sid = obj_ref_of cap\<rbrakk> \<Longrightarrow> is_original_cap s (obj_ref_of cap, tcb_cnode_index 2) \<and> same_region_as cap (cap.ReplyCap (obj_ref_of cap) False rights) \<and> (case cap of cap.EndpointCap ref badge R \<Rightarrow> badge \<noteq> 0 \<longrightarrow> cap_ep_badge (cap.ReplyCap (obj_ref_of cap) False rights) = badge \<and> \<not> cap_insert_dest_original (cap.ReplyCap (obj_ref_of cap) False rights) cap | cap.NotificationCap ref badge R \<Rightarrow> badge \<noteq> 0 \<longrightarrow> cap_ep_badge (cap.ReplyCap (obj_ref_of cap) False rights) = badge \<and> \<not> cap_insert_dest_original (cap.ReplyCap (obj_ref_of cap) False rights) cap | _ \<Rightarrow> True) \<and> not_idle_thread (obj_ref_of cap) s \<and> cap_aligned (cap.ReplyCap (obj_ref_of cap) False rights) proof (prove)
goal (1 subgoal):
 1. \<And>s capa x52 x53. \<lbrakk>sid \<noteq> did; valid_idle s; not_idle_thread did s; valid_mdb s; st_tcb_at (\<lambda>r. r \<noteq> Inactive \<and> r \<noteq> IdleThreadState) sid s; valid_etcbs s; tcb_at did s; tcb_at sid s; valid_objs s; caps_of_state s (sid, tcb_cnode_index 2) = Some (cap.ReplyCap sid True x53); caps_of_state s (did, tcb_cnode_index 3) = Some capa; is_reply_cap capa \<or> cap.NullCap = capa; x52\<rbrakk> \<Longrightarrow> is_original_cap s (sid, tcb_cnode_index 2) \<and> not_idle_thread sid s \<and> cap_aligned (cap.ReplyCap sid False rights) proof (prove)
goal (2 subgoals):
 1. \<And>s capa x52 x53. \<lbrakk>sid \<noteq> did; valid_idle s; not_idle_thread did s; valid_mdb s; st_tcb_at (\<lambda>r. r \<noteq> Inactive \<and> r \<noteq> IdleThreadState) sid s; valid_etcbs s; tcb_at did s; tcb_at sid s; valid_objs s; caps_of_state s (sid, tcb_cnode_index 2) = Some (cap.ReplyCap sid True x53); caps_of_state s (did, tcb_cnode_index 3) = Some capa; is_reply_cap capa \<or> cap.NullCap = capa; x52\<rbrakk> \<Longrightarrow> is_original_cap s (sid, tcb_cnode_index 2)
 2. \<And>s capa x52 x53. \<lbrakk>sid \<noteq> did; valid_idle s; not_idle_thread did s; valid_mdb s; st_tcb_at (\<lambda>r. r \<noteq> Inactive \<and> r \<noteq> IdleThreadState) sid s; valid_etcbs s; tcb_at did s; tcb_at sid s; valid_objs s; caps_of_state s (sid, tcb_cnode_index 2) = Some (cap.ReplyCap sid True x53); caps_of_state s (did, tcb_cnode_index 3) = Some capa; is_reply_cap capa \<or> cap.NullCap = capa; x52\<rbrakk> \<Longrightarrow> not_idle_thread sid s \<and> cap_aligned (cap.ReplyCap sid False rights) proof (prove)
goal (2 subgoals):
 1. \<And>s capa x52 x53. \<lbrakk>sid \<noteq> did; valid_idle s; not_idle_thread did s; valid_mdb s; st_tcb_at (\<lambda>r. r \<noteq> Inactive \<and> r \<noteq> IdleThreadState) sid s; valid_etcbs s; tcb_at did s; tcb_at sid s; valid_objs s; is_reply_cap capa \<or> cap.NullCap = capa; x52; cte_wp_at ((=) (cap.ReplyCap sid True x53)) (sid, tcb_cnode_index 2) s; cte_wp_at ((=) capa) (did, tcb_cnode_index 3) s\<rbrakk> \<Longrightarrow> is_original_cap s (sid, tcb_cnode_index 2)
 2. \<And>s capa x52 x53. \<lbrakk>sid \<noteq> did; valid_idle s; not_idle_thread did s; valid_mdb s; st_tcb_at (\<lambda>r. r \<noteq> Inactive \<and> r \<noteq> IdleThreadState) sid s; valid_etcbs s; tcb_at did s; tcb_at sid s; valid_objs s; caps_of_state s (sid, tcb_cnode_index 2) = Some (cap.ReplyCap sid True x53); caps_of_state s (did, tcb_cnode_index 3) = Some capa; is_reply_cap capa \<or> cap.NullCap = capa; x52\<rbrakk> \<Longrightarrow> not_idle_thread sid s \<and> cap_aligned (cap.ReplyCap sid False rights) proof (prove)
goal (2 subgoals):
 1. \<And>s capa x52 x53. \<lbrakk>sid \<noteq> did; valid_idle s; not_idle_thread did s; valid_mdb s; st_tcb_at (\<lambda>r. r \<noteq> Inactive \<and> r \<noteq> IdleThreadState) sid s; valid_etcbs s; tcb_at did s; tcb_at sid s; valid_objs s; is_reply_cap capa \<or> cap.NullCap = capa; x52; cte_wp_at ((=) (cap.ReplyCap sid True x53)) (sid, tcb_cnode_index 2) s; cte_wp_at ((=) capa) (did, tcb_cnode_index 3) s; tcb_cap_valid (cap.ReplyCap sid True x53) (sid, tcb_cnode_index 2) s\<rbrakk> \<Longrightarrow> is_original_cap s (sid, tcb_cnode_index 2)
 2. \<And>s capa x52 x53. \<lbrakk>sid \<noteq> did; valid_idle s; not_idle_thread did s; valid_mdb s; st_tcb_at (\<lambda>r. r \<noteq> Inactive \<and> r \<noteq> IdleThreadState) sid s; valid_etcbs s; tcb_at did s; tcb_at sid s; valid_objs s; caps_of_state s (sid, tcb_cnode_index 2) = Some (cap.ReplyCap sid True x53); caps_of_state s (did, tcb_cnode_index 3) = Some capa; is_reply_cap capa \<or> cap.NullCap = capa; x52\<rbrakk> \<Longrightarrow> not_idle_thread sid s \<and> cap_aligned (cap.ReplyCap sid False rights) proof (prove)
goal (2 subgoals):
 1. \<And>s capa x52 x53. \<lbrakk>sid \<noteq> did; valid_idle s; not_idle_thread did s; st_tcb_at (\<lambda>r. r \<noteq> Inactive \<and> r \<noteq> IdleThreadState) sid s; valid_etcbs s; tcb_at did s; tcb_at sid s; valid_objs s; is_reply_cap capa \<or> cap.NullCap = capa; x52; cte_wp_at ((=) (cap.ReplyCap sid True x53)) (sid, tcb_cnode_index 2) s; cte_wp_at ((=) capa) (did, tcb_cnode_index 3) s; tcb_cap_valid (cap.ReplyCap sid True x53) (sid, tcb_cnode_index 2) s; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); \<forall>a b cap. caps_of_state s (a, b) = Some cap \<longrightarrow> is_master_reply_cap cap \<longrightarrow> is_original_cap s (a, b); reply_mdb (cdt s) (caps_of_state s)\<rbrakk> \<Longrightarrow> is_original_cap s (sid, tcb_cnode_index 2)
 2. \<And>s capa x52 x53. \<lbrakk>sid \<noteq> did; valid_idle s; not_idle_thread did s; valid_mdb s; st_tcb_at (\<lambda>r. r \<noteq> Inactive \<and> r \<noteq> IdleThreadState) sid s; valid_etcbs s; tcb_at did s; tcb_at sid s; valid_objs s; caps_of_state s (sid, tcb_cnode_index 2) = Some (cap.ReplyCap sid True x53); caps_of_state s (did, tcb_cnode_index 3) = Some capa; is_reply_cap capa \<or> cap.NullCap = capa; x52\<rbrakk> \<Longrightarrow> not_idle_thread sid s \<and> cap_aligned (cap.ReplyCap sid False rights) proof (prove)
goal (2 subgoals):
 1. \<And>s capa x52 x53. \<lbrakk>sid \<noteq> did; valid_idle s; not_idle_thread did s; st_tcb_at (\<lambda>r. r \<noteq> Inactive \<and> r \<noteq> IdleThreadState) sid s; valid_etcbs s; tcb_at did s; tcb_at sid s; valid_objs s; is_reply_cap capa \<or> cap.NullCap = capa; x52; cte_wp_at ((=) (cap.ReplyCap sid True x53)) (sid, tcb_cnode_index 2) s; cte_wp_at ((=) capa) (did, tcb_cnode_index 3) s; tcb_cap_valid (cap.ReplyCap sid True x53) (sid, tcb_cnode_index 2) s; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); \<forall>b cap. caps_of_state s (sid, b) = Some cap \<longrightarrow> is_master_reply_cap cap \<longrightarrow> is_original_cap s (sid, b)\<rbrakk> \<Longrightarrow> is_original_cap s (sid, tcb_cnode_index 2)
 2. \<And>s capa x52 x53. \<lbrakk>sid \<noteq> did; valid_idle s; not_idle_thread did s; valid_mdb s; st_tcb_at (\<lambda>r. r \<noteq> Inactive \<and> r \<noteq> IdleThreadState) sid s; valid_etcbs s; tcb_at did s; tcb_at sid s; valid_objs s; caps_of_state s (sid, tcb_cnode_index 2) = Some (cap.ReplyCap sid True x53); caps_of_state s (did, tcb_cnode_index 3) = Some capa; is_reply_cap capa \<or> cap.NullCap = capa; x52\<rbrakk> \<Longrightarrow> not_idle_thread sid s \<and> cap_aligned (cap.ReplyCap sid False rights) proof (prove)
goal (2 subgoals):
 1. \<And>s capa x52 x53. \<lbrakk>sid \<noteq> did; valid_idle s; not_idle_thread did s; st_tcb_at (\<lambda>r. r \<noteq> Inactive \<and> r \<noteq> IdleThreadState) sid s; valid_etcbs s; tcb_at did s; tcb_at sid s; valid_objs s; is_reply_cap capa \<or> cap.NullCap = capa; x52; cte_wp_at ((=) (cap.ReplyCap sid True x53)) (sid, tcb_cnode_index 2) s; cte_wp_at ((=) capa) (did, tcb_cnode_index 3) s; tcb_cap_valid (cap.ReplyCap sid True x53) (sid, tcb_cnode_index 2) s; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); \<forall>cap. caps_of_state s (sid, tcb_cnode_index 2) = Some cap \<longrightarrow> is_master_reply_cap cap \<longrightarrow> is_original_cap s (sid, tcb_cnode_index 2)\<rbrakk> \<Longrightarrow> is_original_cap s (sid, tcb_cnode_index 2)
 2. \<And>s capa x52 x53. \<lbrakk>sid \<noteq> did; valid_idle s; not_idle_thread did s; valid_mdb s; st_tcb_at (\<lambda>r. r \<noteq> Inactive \<and> r \<noteq> IdleThreadState) sid s; valid_etcbs s; tcb_at did s; tcb_at sid s; valid_objs s; caps_of_state s (sid, tcb_cnode_index 2) = Some (cap.ReplyCap sid True x53); caps_of_state s (did, tcb_cnode_index 3) = Some capa; is_reply_cap capa \<or> cap.NullCap = capa; x52\<rbrakk> \<Longrightarrow> not_idle_thread sid s \<and> cap_aligned (cap.ReplyCap sid False rights) proof (prove)
goal (1 subgoal):
 1. \<And>s capa x52 x53. \<lbrakk>sid \<noteq> did; valid_idle s; not_idle_thread did s; valid_mdb s; st_tcb_at (\<lambda>r. r \<noteq> Inactive \<and> r \<noteq> IdleThreadState) sid s; valid_etcbs s; tcb_at did s; tcb_at sid s; valid_objs s; caps_of_state s (sid, tcb_cnode_index 2) = Some (cap.ReplyCap sid True x53); caps_of_state s (did, tcb_cnode_index 3) = Some capa; is_reply_cap capa \<or> cap.NullCap = capa; x52\<rbrakk> \<Longrightarrow> not_idle_thread sid s \<and> cap_aligned (cap.ReplyCap sid False rights) proof (prove)
goal (1 subgoal):
 1. \<And>s capa x52 x53. \<lbrakk>sid \<noteq> did; valid_idle s; not_idle_thread did s; valid_mdb s; st_tcb_at (\<lambda>r. r \<noteq> Inactive \<and> r \<noteq> IdleThreadState) sid s; valid_etcbs s; tcb_at did s; tcb_at sid s; valid_objs s; is_reply_cap capa \<or> cap.NullCap = capa; x52; cte_wp_at ((=) (cap.ReplyCap sid True x53)) (sid, tcb_cnode_index 2) s; cte_wp_at ((=) capa) (did, tcb_cnode_index 3) s\<rbrakk> \<Longrightarrow> not_idle_thread sid s \<and> cap_aligned (cap.ReplyCap sid False rights) proof (prove)
goal (1 subgoal):
 1. \<And>s capa x52 x53. \<lbrakk>sid \<noteq> did; valid_idle s; not_idle_thread did s; valid_mdb s; st_tcb_at (\<lambda>r. r \<noteq> Inactive \<and> r \<noteq> IdleThreadState) sid s; valid_etcbs s; tcb_at did s; tcb_at sid s; valid_objs s; is_reply_cap capa \<or> cap.NullCap = capa; x52; cte_wp_at ((=) (cap.ReplyCap sid True x53)) (sid, tcb_cnode_index 2) s; cte_wp_at ((=) capa) (did, tcb_cnode_index 3) s; tcb_cap_valid capa (did, tcb_cnode_index 3) s\<rbrakk> \<Longrightarrow> not_idle_thread sid s \<and> cap_aligned (cap.ReplyCap sid False rights) proof (prove)
goal (2 subgoals):
 1. \<And>s capa x52 x53. \<lbrakk>sid \<noteq> did; valid_idle s; not_idle_thread did s; valid_mdb s; st_tcb_at (\<lambda>r. r \<noteq> Inactive \<and> r \<noteq> IdleThreadState) sid s; valid_etcbs s; tcb_at did s; tcb_at sid s; valid_objs s; is_reply_cap capa \<or> cap.NullCap = capa; x52; cte_wp_at ((=) (cap.ReplyCap sid True x53)) (sid, tcb_cnode_index 2) s; cte_wp_at ((=) capa) (did, tcb_cnode_index 3) s; tcb_cap_valid capa (did, tcb_cnode_index 3) s\<rbrakk> \<Longrightarrow> not_idle_thread sid s
 2. \<And>s capa x52 x53. \<lbrakk>sid \<noteq> did; valid_idle s; not_idle_thread did s; valid_mdb s; st_tcb_at (\<lambda>r. r \<noteq> Inactive \<and> r \<noteq> IdleThreadState) sid s; valid_etcbs s; tcb_at did s; tcb_at sid s; valid_objs s; is_reply_cap capa \<or> cap.NullCap = capa; x52; cte_wp_at ((=) (cap.ReplyCap sid True x53)) (sid, tcb_cnode_index 2) s; cte_wp_at ((=) capa) (did, tcb_cnode_index 3) s; tcb_cap_valid capa (did, tcb_cnode_index 3) s\<rbrakk> \<Longrightarrow> cap_aligned (cap.ReplyCap sid False rights) proof (prove)
goal (2 subgoals):
 1. \<And>s capa x52 x53. \<lbrakk>did \<noteq> idle_thread_ptr; valid_mdb s; st_tcb_at (\<lambda>r. r \<noteq> Inactive \<and> r \<noteq> IdleThreadState) idle_thread_ptr s; valid_etcbs s; tcb_at did s; tcb_at idle_thread_ptr s; valid_objs s; is_reply_cap capa \<or> cap.NullCap = capa; x52; cte_wp_at ((=) (cap.ReplyCap idle_thread_ptr True x53)) (idle_thread_ptr, tcb_cnode_index 2) s; cte_wp_at ((=) capa) (did, tcb_cnode_index 3) s; tcb_cap_valid capa (did, tcb_cnode_index 3) s; idle_tcb_at (\<lambda>(st, ab). idle st \<and> (case ab of (ntfn, arch) \<Rightarrow> ntfn = None \<and> valid_arch_idle arch)) idle_thread_ptr s; idle_thread s = idle_thread_ptr; sid = idle_thread_ptr\<rbrakk> \<Longrightarrow> False
 2. \<And>s capa x52 x53. \<lbrakk>sid \<noteq> did; valid_idle s; not_idle_thread did s; valid_mdb s; st_tcb_at (\<lambda>r. r \<noteq> Inactive \<and> r \<noteq> IdleThreadState) sid s; valid_etcbs s; tcb_at did s; tcb_at sid s; valid_objs s; is_reply_cap capa \<or> cap.NullCap = capa; x52; cte_wp_at ((=) (cap.ReplyCap sid True x53)) (sid, tcb_cnode_index 2) s; cte_wp_at ((=) capa) (did, tcb_cnode_index 3) s; tcb_cap_valid capa (did, tcb_cnode_index 3) s\<rbrakk> \<Longrightarrow> cap_aligned (cap.ReplyCap sid False rights) proof (prove)
goal (1 subgoal):
 1. \<And>s capa x52 x53. \<lbrakk>sid \<noteq> did; valid_idle s; not_idle_thread did s; valid_mdb s; st_tcb_at (\<lambda>r. r \<noteq> Inactive \<and> r \<noteq> IdleThreadState) sid s; valid_etcbs s; tcb_at did s; tcb_at sid s; valid_objs s; is_reply_cap capa \<or> cap.NullCap = capa; x52; cte_wp_at ((=) (cap.ReplyCap sid True x53)) (sid, tcb_cnode_index 2) s; cte_wp_at ((=) capa) (did, tcb_cnode_index 3) s; tcb_cap_valid capa (did, tcb_cnode_index 3) s\<rbrakk> \<Longrightarrow> cap_aligned (cap.ReplyCap sid False rights) proof (prove)
goal (1 subgoal):
 1. \<And>s capa x52 x53 tcb tcba. \<lbrakk>sid \<noteq> did; valid_idle s; not_idle_thread did s; valid_mdb s; st_tcb_at (\<lambda>r. r \<noteq> Inactive \<and> r \<noteq> IdleThreadState) sid s; valid_etcbs s; valid_objs s; is_reply_cap capa \<or> cap.NullCap = capa; x52; cte_wp_at ((=) (cap.ReplyCap sid True x53)) (sid, tcb_cnode_index 2) s; cte_wp_at ((=) capa) (did, tcb_cnode_index 3) s; tcb_cap_valid capa (did, tcb_cnode_index 3) s; kheap s did = Some (TCB tcb); kheap s sid = Some (TCB tcba)\<rbrakk> \<Longrightarrow> cap_aligned (cap.ReplyCap sid False rights) proof (prove)
goal (2 subgoals):
 1. \<And>s capa x52 x53 tcb tcba. \<lbrakk>sid \<noteq> did; valid_idle s; not_idle_thread did s; valid_mdb s; st_tcb_at (\<lambda>r. r \<noteq> Inactive \<and> r \<noteq> IdleThreadState) sid s; valid_etcbs s; valid_objs s; is_reply_cap capa \<or> cap.NullCap = capa; x52; cte_wp_at ((=) capa) (did, tcb_cnode_index 3) s; tcb_cap_valid capa (did, tcb_cnode_index 3) s; kheap s did = Some (TCB tcb); kheap s sid = Some (TCB tcba)\<rbrakk> \<Longrightarrow> valid_objs s
 2. \<And>s capa x52 x53 tcb tcba. \<lbrakk>sid \<noteq> did; valid_idle s; not_idle_thread did s; valid_mdb s; st_tcb_at (\<lambda>r. r \<noteq> Inactive \<and> r \<noteq> IdleThreadState) sid s; valid_etcbs s; valid_objs s; is_reply_cap capa \<or> cap.NullCap = capa; x52; cte_wp_at ((=) capa) (did, tcb_cnode_index 3) s; tcb_cap_valid capa (did, tcb_cnode_index 3) s; kheap s did = Some (TCB tcb); kheap s sid = Some (TCB tcba); s \<turnstile> cap.ReplyCap sid True x53\<rbrakk> \<Longrightarrow> cap_aligned (cap.ReplyCap sid False rights) proof (prove)
goal (1 subgoal):
 1. \<And>s capa x52 x53 tcb tcba. \<lbrakk>sid \<noteq> did; valid_idle s; not_idle_thread did s; valid_mdb s; st_tcb_at (\<lambda>r. r \<noteq> Inactive \<and> r \<noteq> IdleThreadState) sid s; valid_etcbs s; valid_objs s; is_reply_cap capa \<or> cap.NullCap = capa; x52; cte_wp_at ((=) capa) (did, tcb_cnode_index 3) s; tcb_cap_valid capa (did, tcb_cnode_index 3) s; kheap s did = Some (TCB tcb); kheap s sid = Some (TCB tcba); s \<turnstile> cap.ReplyCap sid True x53\<rbrakk> \<Longrightarrow> cap_aligned (cap.ReplyCap sid False rights) proof (prove)
goal:
No subgoals!