theory Tcb_IF

lemma rec_del_globals_equiv:
  "\<lbrace>\<lambda>s. invs s \<and> globals_equiv st s \<and> emptyable (slot_rdcall call) s \<and> valid_rec_del_call call s\<rbrace>
   rec_del call
   \<lbrace>\<lambda>_. globals_equiv st\<rbrace>" apply (wp finalise_cap_globals_equiv
            rec_del_preservation2[where Q="valid_arch_state"
                                    and R="\<lambda>cap s. invs s \<and> valid_cap cap s
                                                 \<and> (\<forall>p. cap = ThreadCap p \<longrightarrow> p \<noteq> idle_thread s)"]) apply simp apply (wp set_cap_globals_equiv'') apply simp apply (wp empty_slot_globals_equiv)+ apply simp apply (wp)+ apply simp apply fastforce apply (fastforce simp: invs_def valid_state_def valid_arch_caps_vs_lookup
                            valid_pspace_def no_cap_to_idle_thread''
                      dest: caps_of_state_valid) apply (wp preemption_point_inv | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. invs s \<and> globals_equiv st s \<and> emptyable (slot_rdcall call) s \<and> valid_rec_del_call call s\<rbrace> rec_del call \<lbrace>\<lambda>_. globals_equiv st\<rbrace> proof (prove)
goal (12 subgoals):
 1. \<And>cap final s. ((\<lambda>s. invs s \<and> s \<turnstile> cap \<and> (\<forall>p. cap = ThreadCap p \<longrightarrow> p \<noteq> idle_thread s)) and globals_equiv st) s \<Longrightarrow> (globals_equiv st and invs and valid_cap cap and (\<lambda>s. \<forall>p. cap = ThreadCap p \<longrightarrow> p \<noteq> idle_thread s)) s
 2. \<And>cap b. \<lbrace>valid_arch_state and globals_equiv st\<rbrace> set_cap cap b \<lbrace>\<lambda>_. globals_equiv st\<rbrace>
 3. \<And>cap b. \<lbrace>valid_arch_state\<rbrace> set_cap cap b \<lbrace>\<lambda>_. valid_arch_state\<rbrace>
 4. \<And>slot free. \<lbrace>valid_arch_state and globals_equiv st\<rbrace> empty_slot slot free \<lbrace>\<lambda>_. globals_equiv st\<rbrace>
 5. \<And>slot free. \<lbrace>valid_arch_state\<rbrace> empty_slot slot free \<lbrace>\<lambda>_. valid_arch_state\<rbrace>
 6. \<And>a b. \<lbrace>valid_arch_state\<rbrace> cap_swap_for_delete a b \<lbrace>\<lambda>_. valid_arch_state\<rbrace>
 7. \<And>a b. \<lbrace>valid_arch_state and globals_equiv st\<rbrace> cap_swap_for_delete a b \<lbrace>\<lambda>_. globals_equiv st\<rbrace>
 8. \<And>s. invs s \<Longrightarrow> valid_arch_state s
 9. \<And>s slot cap. \<lbrakk>invs s; caps_of_state s slot = Some cap\<rbrakk> \<Longrightarrow> invs s \<and> s \<turnstile> cap \<and> (\<forall>p. cap = ThreadCap p \<longrightarrow> p \<noteq> idle_thread s)
 10. \<lbrace>valid_arch_state\<rbrace> preemption_point \<lbrace>\<lambda>_. valid_arch_state\<rbrace>
A total of 12 subgoals... proof (prove)
goal (11 subgoals):
 1. \<And>cap b. \<lbrace>valid_arch_state and globals_equiv st\<rbrace> set_cap cap b \<lbrace>\<lambda>_. globals_equiv st\<rbrace>
 2. \<And>cap b. \<lbrace>valid_arch_state\<rbrace> set_cap cap b \<lbrace>\<lambda>_. valid_arch_state\<rbrace>
 3. \<And>slot free. \<lbrace>valid_arch_state and globals_equiv st\<rbrace> empty_slot slot free \<lbrace>\<lambda>_. globals_equiv st\<rbrace>
 4. \<And>slot free. \<lbrace>valid_arch_state\<rbrace> empty_slot slot free \<lbrace>\<lambda>_. valid_arch_state\<rbrace>
 5. \<And>a b. \<lbrace>valid_arch_state\<rbrace> cap_swap_for_delete a b \<lbrace>\<lambda>_. valid_arch_state\<rbrace>
 6. \<And>a b. \<lbrace>valid_arch_state and globals_equiv st\<rbrace> cap_swap_for_delete a b \<lbrace>\<lambda>_. globals_equiv st\<rbrace>
 7. \<And>s. invs s \<Longrightarrow> valid_arch_state s
 8. \<And>s slot cap. \<lbrakk>invs s; caps_of_state s slot = Some cap\<rbrakk> \<Longrightarrow> invs s \<and> s \<turnstile> cap \<and> (\<forall>p. cap = ThreadCap p \<longrightarrow> p \<noteq> idle_thread s)
 9. \<lbrace>valid_arch_state\<rbrace> preemption_point \<lbrace>\<lambda>_. valid_arch_state\<rbrace>
 10. \<lbrace>valid_arch_state and globals_equiv st\<rbrace> preemption_point \<lbrace>\<lambda>_. globals_equiv st\<rbrace>
A total of 11 subgoals... proof (prove)
goal (11 subgoals):
 1. \<And>cap b s. (valid_arch_state and globals_equiv st) s \<Longrightarrow> (globals_equiv st and valid_arch_state) s
 2. \<And>cap b. \<lbrace>valid_arch_state\<rbrace> set_cap cap b \<lbrace>\<lambda>_. valid_arch_state\<rbrace>
 3. \<And>slot free. \<lbrace>valid_arch_state and globals_equiv st\<rbrace> empty_slot slot free \<lbrace>\<lambda>_. globals_equiv st\<rbrace>
 4. \<And>slot free. \<lbrace>valid_arch_state\<rbrace> empty_slot slot free \<lbrace>\<lambda>_. valid_arch_state\<rbrace>
 5. \<And>a b. \<lbrace>valid_arch_state\<rbrace> cap_swap_for_delete a b \<lbrace>\<lambda>_. valid_arch_state\<rbrace>
 6. \<And>a b. \<lbrace>valid_arch_state and globals_equiv st\<rbrace> cap_swap_for_delete a b \<lbrace>\<lambda>_. globals_equiv st\<rbrace>
 7. \<And>s. invs s \<Longrightarrow> valid_arch_state s
 8. \<And>s slot cap. \<lbrakk>invs s; caps_of_state s slot = Some cap\<rbrakk> \<Longrightarrow> invs s \<and> s \<turnstile> cap \<and> (\<forall>p. cap = ThreadCap p \<longrightarrow> p \<noteq> idle_thread s)
 9. \<lbrace>valid_arch_state\<rbrace> preemption_point \<lbrace>\<lambda>_. valid_arch_state\<rbrace>
 10. \<lbrace>valid_arch_state and globals_equiv st\<rbrace> preemption_point \<lbrace>\<lambda>_. globals_equiv st\<rbrace>
A total of 11 subgoals... proof (prove)
goal (10 subgoals):
 1. \<And>cap b. \<lbrace>valid_arch_state\<rbrace> set_cap cap b \<lbrace>\<lambda>_. valid_arch_state\<rbrace>
 2. \<And>slot free. \<lbrace>valid_arch_state and globals_equiv st\<rbrace> empty_slot slot free \<lbrace>\<lambda>_. globals_equiv st\<rbrace>
 3. \<And>slot free. \<lbrace>valid_arch_state\<rbrace> empty_slot slot free \<lbrace>\<lambda>_. valid_arch_state\<rbrace>
 4. \<And>a b. \<lbrace>valid_arch_state\<rbrace> cap_swap_for_delete a b \<lbrace>\<lambda>_. valid_arch_state\<rbrace>
 5. \<And>a b. \<lbrace>valid_arch_state and globals_equiv st\<rbrace> cap_swap_for_delete a b \<lbrace>\<lambda>_. globals_equiv st\<rbrace>
 6. \<And>s. invs s \<Longrightarrow> valid_arch_state s
 7. \<And>s slot cap. \<lbrakk>invs s; caps_of_state s slot = Some cap\<rbrakk> \<Longrightarrow> invs s \<and> s \<turnstile> cap \<and> (\<forall>p. cap = ThreadCap p \<longrightarrow> p \<noteq> idle_thread s)
 8. \<lbrace>valid_arch_state\<rbrace> preemption_point \<lbrace>\<lambda>_. valid_arch_state\<rbrace>
 9. \<lbrace>valid_arch_state and globals_equiv st\<rbrace> preemption_point \<lbrace>\<lambda>_. globals_equiv st\<rbrace>
 10. \<And>s. invs s \<and> globals_equiv st s \<and> emptyable (slot_rdcall call) s \<and> valid_rec_del_call call s \<Longrightarrow> invs s \<and> globals_equiv st s \<and> emptyable (slot_rdcall call) s \<and> valid_rec_del_call call s proof (prove)
goal (9 subgoals):
 1. \<And>slot free s. (valid_arch_state and globals_equiv st) s \<Longrightarrow> (globals_equiv st and valid_arch_state) s
 2. \<And>slot free. \<lbrace>valid_arch_state\<rbrace> empty_slot slot free \<lbrace>\<lambda>_. valid_arch_state\<rbrace>
 3. \<And>a b. \<lbrace>valid_arch_state\<rbrace> cap_swap_for_delete a b \<lbrace>\<lambda>_. valid_arch_state\<rbrace>
 4. \<And>a b. \<lbrace>valid_arch_state and globals_equiv st\<rbrace> cap_swap_for_delete a b \<lbrace>\<lambda>_. globals_equiv st\<rbrace>
 5. \<And>s. invs s \<Longrightarrow> valid_arch_state s
 6. \<And>s slot cap. \<lbrakk>invs s; caps_of_state s slot = Some cap\<rbrakk> \<Longrightarrow> invs s \<and> s \<turnstile> cap \<and> (\<forall>p. cap = ThreadCap p \<longrightarrow> p \<noteq> idle_thread s)
 7. \<lbrace>valid_arch_state\<rbrace> preemption_point \<lbrace>\<lambda>_. valid_arch_state\<rbrace>
 8. \<lbrace>valid_arch_state and globals_equiv st\<rbrace> preemption_point \<lbrace>\<lambda>_. globals_equiv st\<rbrace>
 9. \<And>s. invs s \<and> globals_equiv st s \<and> emptyable (slot_rdcall call) s \<and> valid_rec_del_call call s \<Longrightarrow> invs s \<and> globals_equiv st s \<and> emptyable (slot_rdcall call) s \<and> valid_rec_del_call call s proof (prove)
goal (8 subgoals):
 1. \<And>slot free. \<lbrace>valid_arch_state\<rbrace> empty_slot slot free \<lbrace>\<lambda>_. valid_arch_state\<rbrace>
 2. \<And>a b. \<lbrace>valid_arch_state\<rbrace> cap_swap_for_delete a b \<lbrace>\<lambda>_. valid_arch_state\<rbrace>
 3. \<And>a b. \<lbrace>valid_arch_state and globals_equiv st\<rbrace> cap_swap_for_delete a b \<lbrace>\<lambda>_. globals_equiv st\<rbrace>
 4. \<And>s. invs s \<Longrightarrow> valid_arch_state s
 5. \<And>s slot cap. \<lbrakk>invs s; caps_of_state s slot = Some cap\<rbrakk> \<Longrightarrow> invs s \<and> s \<turnstile> cap \<and> (\<forall>p. cap = ThreadCap p \<longrightarrow> p \<noteq> idle_thread s)
 6. \<lbrace>valid_arch_state\<rbrace> preemption_point \<lbrace>\<lambda>_. valid_arch_state\<rbrace>
 7. \<lbrace>valid_arch_state and globals_equiv st\<rbrace> preemption_point \<lbrace>\<lambda>_. globals_equiv st\<rbrace>
 8. \<And>s. invs s \<and> globals_equiv st s \<and> emptyable (slot_rdcall call) s \<and> valid_rec_del_call call s \<Longrightarrow> invs s \<and> globals_equiv st s \<and> emptyable (slot_rdcall call) s \<and> valid_rec_del_call call s proof (prove)
goal (6 subgoals):
 1. \<And>a b s. (valid_arch_state and globals_equiv st) s \<Longrightarrow> (globals_equiv st and valid_arch_state) s
 2. \<And>s. invs s \<Longrightarrow> valid_arch_state s
 3. \<And>s slot cap. \<lbrakk>invs s; caps_of_state s slot = Some cap\<rbrakk> \<Longrightarrow> invs s \<and> s \<turnstile> cap \<and> (\<forall>p. cap = ThreadCap p \<longrightarrow> p \<noteq> idle_thread s)
 4. \<lbrace>valid_arch_state\<rbrace> preemption_point \<lbrace>\<lambda>_. valid_arch_state\<rbrace>
 5. \<lbrace>valid_arch_state and globals_equiv st\<rbrace> preemption_point \<lbrace>\<lambda>_. globals_equiv st\<rbrace>
 6. \<And>s. invs s \<and> globals_equiv st s \<and> emptyable (slot_rdcall call) s \<and> valid_rec_del_call call s \<Longrightarrow> invs s \<and> globals_equiv st s \<and> emptyable (slot_rdcall call) s \<and> valid_rec_del_call call s proof (prove)
goal (5 subgoals):
 1. \<And>s. invs s \<Longrightarrow> valid_arch_state s
 2. \<And>s slot cap. \<lbrakk>invs s; caps_of_state s slot = Some cap\<rbrakk> \<Longrightarrow> invs s \<and> s \<turnstile> cap \<and> (\<forall>p. cap = ThreadCap p \<longrightarrow> p \<noteq> idle_thread s)
 3. \<lbrace>valid_arch_state\<rbrace> preemption_point \<lbrace>\<lambda>_. valid_arch_state\<rbrace>
 4. \<lbrace>valid_arch_state and globals_equiv st\<rbrace> preemption_point \<lbrace>\<lambda>_. globals_equiv st\<rbrace>
 5. \<And>s. invs s \<and> globals_equiv st s \<and> emptyable (slot_rdcall call) s \<and> valid_rec_del_call call s \<Longrightarrow> invs s \<and> globals_equiv st s \<and> emptyable (slot_rdcall call) s \<and> valid_rec_del_call call s proof (prove)
goal (4 subgoals):
 1. \<And>s slot cap. \<lbrakk>invs s; caps_of_state s slot = Some cap\<rbrakk> \<Longrightarrow> invs s \<and> s \<turnstile> cap \<and> (\<forall>p. cap = ThreadCap p \<longrightarrow> p \<noteq> idle_thread s)
 2. \<lbrace>valid_arch_state\<rbrace> preemption_point \<lbrace>\<lambda>_. valid_arch_state\<rbrace>
 3. \<lbrace>valid_arch_state and globals_equiv st\<rbrace> preemption_point \<lbrace>\<lambda>_. globals_equiv st\<rbrace>
 4. \<And>s. invs s \<and> globals_equiv st s \<and> emptyable (slot_rdcall call) s \<and> valid_rec_del_call call s \<Longrightarrow> invs s \<and> globals_equiv st s \<and> emptyable (slot_rdcall call) s \<and> valid_rec_del_call call s proof (prove)
goal (3 subgoals):
 1. \<lbrace>valid_arch_state\<rbrace> preemption_point \<lbrace>\<lambda>_. valid_arch_state\<rbrace>
 2. \<lbrace>valid_arch_state and globals_equiv st\<rbrace> preemption_point \<lbrace>\<lambda>_. globals_equiv st\<rbrace>
 3. \<And>s. invs s \<and> globals_equiv st s \<and> emptyable (slot_rdcall call) s \<and> valid_rec_del_call call s \<Longrightarrow> invs s \<and> globals_equiv st s \<and> emptyable (slot_rdcall call) s \<and> valid_rec_del_call call s proof (prove)
goal:
No subgoals!