theory TcbAcc_AI

lemma thread_set_valid_objs_triv:
  assumes x: "\<And>tcb. \<forall>(getF, v) \<in> ran tcb_cap_cases.
                  getF (f tcb) = getF tcb"
  assumes z: "\<And>tcb. tcb_state (f tcb) = tcb_state tcb"
  assumes w: "\<And>tcb. tcb_ipc_buffer (f tcb) = tcb_ipc_buffer tcb
                        \<or> (tcb_ipc_buffer (f tcb) = 0)"
  assumes y: "\<And>tcb. tcb_fault_handler (f tcb) \<noteq> tcb_fault_handler tcb
                       \<longrightarrow> length (tcb_fault_handler (f tcb)) = word_bits"
  assumes a: "\<And>tcb. tcb_fault (f tcb) \<noteq> tcb_fault tcb
                       \<longrightarrow> (case tcb_fault (f tcb) of None \<Rightarrow> True
                                                   | Some f \<Rightarrow> valid_fault f)"
  assumes b: "\<And>tcb. tcb_bound_notification (f tcb) \<noteq> tcb_bound_notification tcb
                       \<longrightarrow> tcb_bound_notification (f tcb) = None"
  assumes c: "\<And>tcb s::'z::state_ext state.
                     valid_arch_tcb (tcb_arch (f tcb)) s = valid_arch_tcb (tcb_arch tcb) s"
  shows "\<lbrace>valid_objs\<rbrace> thread_set f t \<lbrace>\<lambda>rv. valid_objs :: 'z::state_ext state \<Rightarrow> bool\<rbrace>" using bspec [OF x, OF tcb_ipcframe_in_cases] apply (simp add: thread_set_def) apply wp apply clarsimp apply (drule get_tcb_SomeD) apply (erule (1) pspace_valid_objsE) apply (clarsimp simp add: valid_obj_def valid_tcb_def valid_bound_ntfn_def z
                            split_paired_Ball obj_at_def c
                            a_type_def bspec_split[OF x]) apply (rule conjI) apply (elim allEI) apply auto[1] apply (rule conjI) apply (cut_tac tcb = y in w) apply (auto simp: valid_ipc_buffer_cap_simps)[1] apply (cut_tac tcb=y in y) apply (cut_tac tcb=y in a) apply (cut_tac tcb=y in b) by auto[1]

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs\<rbrace> thread_set f t \<lbrace>\<lambda>rv. valid_objs\<rbrace> proof (prove)
using this:
case (tcb_ipcframe, tcb_ipcframe_update, \<lambda>_ _. is_nondevice_page_cap or (=) NullCap) of (getF, v) \<Rightarrow> getF (f ?tcb1) = getF ?tcb1

goal (1 subgoal):
 1. \<lbrace>valid_objs\<rbrace> thread_set f t \<lbrace>\<lambda>rv. valid_objs\<rbrace> proof (prove)
goal (1 subgoal):
 1. (\<And>tcb. tcb_ipcframe (f tcb) = tcb_ipcframe tcb) \<Longrightarrow> \<lbrace>valid_objs\<rbrace> do tcb <- gets_the (get_tcb t);
set_object t (TCB (f tcb))
od \<lbrace>\<lambda>rv. valid_objs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>\<And>tcb. tcb_ipcframe (f tcb) = tcb_ipcframe tcb; valid_objs s\<rbrakk> \<Longrightarrow> get_tcb t s \<noteq> None \<longrightarrow> (valid_objs and valid_obj t (TCB (f (the (get_tcb t s))))) s proof (prove)
goal (1 subgoal):
 1. \<And>s y. \<lbrakk>\<And>tcb. tcb_ipcframe (f tcb) = tcb_ipcframe tcb; valid_objs s; get_tcb t s = Some y\<rbrakk> \<Longrightarrow> valid_obj t (TCB (f y)) s proof (prove)
goal (1 subgoal):
 1. \<And>s y. \<lbrakk>\<And>tcb. tcb_ipcframe (f tcb) = tcb_ipcframe tcb; valid_objs s; kheap s t = Some (TCB y)\<rbrakk> \<Longrightarrow> valid_obj t (TCB (f y)) s proof (prove)
goal (1 subgoal):
 1. \<And>s y. \<lbrakk>\<And>tcb. tcb_ipcframe (f tcb) = tcb_ipcframe tcb; valid_objs s; kheap s t = Some (TCB y); valid_obj t (TCB y) s\<rbrakk> \<Longrightarrow> valid_obj t (TCB (f y)) s proof (prove)
goal (1 subgoal):
 1. \<And>s y. \<lbrakk>\<And>tcb. tcb_ipcframe (f tcb) = tcb_ipcframe tcb; valid_objs s; kheap s t = Some (TCB y); \<forall>x a b. (x, a, b) \<in> ran tcb_cap_cases \<longrightarrow> s \<turnstile> x y \<and> b t (tcb_state y) (x y); valid_ipc_buffer_cap (tcb_ipcframe y) (tcb_ipc_buffer y); valid_tcb_state (tcb_state y) s; case tcb_fault y of None \<Rightarrow> True | Some f \<Rightarrow> valid_fault f; length (tcb_fault_handler y) = word_bits; case tcb_bound_notification y of None \<Rightarrow> True | Some a \<Rightarrow> ntfn_at a s; valid_arch_tcb (tcb_arch y) s\<rbrakk> \<Longrightarrow> (\<forall>x a b. (x, a, b) \<in> ran tcb_cap_cases \<longrightarrow> b t (tcb_state y) (x y)) \<and> valid_ipc_buffer_cap (tcb_ipcframe y) (tcb_ipc_buffer (f y)) \<and> (case tcb_fault (f y) of None \<Rightarrow> True | Some x \<Rightarrow> valid_fault x) \<and> length (tcb_fault_handler (f y)) = word_bits \<and> (case tcb_bound_notification (f y) of None \<Rightarrow> True | Some a \<Rightarrow> ntfn_at a s) proof (prove)
goal (2 subgoals):
 1. \<And>s y. \<lbrakk>\<And>tcb. tcb_ipcframe (f tcb) = tcb_ipcframe tcb; valid_objs s; kheap s t = Some (TCB y); \<forall>x a b. (x, a, b) \<in> ran tcb_cap_cases \<longrightarrow> s \<turnstile> x y \<and> b t (tcb_state y) (x y); valid_ipc_buffer_cap (tcb_ipcframe y) (tcb_ipc_buffer y); valid_tcb_state (tcb_state y) s; case tcb_fault y of None \<Rightarrow> True | Some f \<Rightarrow> valid_fault f; length (tcb_fault_handler y) = word_bits; case tcb_bound_notification y of None \<Rightarrow> True | Some a \<Rightarrow> ntfn_at a s; valid_arch_tcb (tcb_arch y) s\<rbrakk> \<Longrightarrow> \<forall>x a b. (x, a, b) \<in> ran tcb_cap_cases \<longrightarrow> b t (tcb_state y) (x y)
 2. \<And>s y. \<lbrakk>\<And>tcb. tcb_ipcframe (f tcb) = tcb_ipcframe tcb; valid_objs s; kheap s t = Some (TCB y); \<forall>x a b. (x, a, b) \<in> ran tcb_cap_cases \<longrightarrow> s \<turnstile> x y \<and> b t (tcb_state y) (x y); valid_ipc_buffer_cap (tcb_ipcframe y) (tcb_ipc_buffer y); valid_tcb_state (tcb_state y) s; case tcb_fault y of None \<Rightarrow> True | Some f \<Rightarrow> valid_fault f; length (tcb_fault_handler y) = word_bits; case tcb_bound_notification y of None \<Rightarrow> True | Some a \<Rightarrow> ntfn_at a s; valid_arch_tcb (tcb_arch y) s\<rbrakk> \<Longrightarrow> valid_ipc_buffer_cap (tcb_ipcframe y) (tcb_ipc_buffer (f y)) \<and> (case tcb_fault (f y) of None \<Rightarrow> True | Some x \<Rightarrow> valid_fault x) \<and> length (tcb_fault_handler (f y)) = word_bits \<and> (case tcb_bound_notification (f y) of None \<Rightarrow> True | Some a \<Rightarrow> ntfn_at a s) proof (prove)
goal (2 subgoals):
 1. \<And>s y x a b. \<lbrakk>\<And>tcb. tcb_ipcframe (f tcb) = tcb_ipcframe tcb; valid_objs s; kheap s t = Some (TCB y); valid_ipc_buffer_cap (tcb_ipcframe y) (tcb_ipc_buffer y); valid_tcb_state (tcb_state y) s; case tcb_fault y of None \<Rightarrow> True | Some f \<Rightarrow> valid_fault f; length (tcb_fault_handler y) = word_bits; case tcb_bound_notification y of None \<Rightarrow> True | Some a \<Rightarrow> ntfn_at a s; valid_arch_tcb (tcb_arch y) s; (x, a, b) \<in> ran tcb_cap_cases \<longrightarrow> s \<turnstile> x y \<and> b t (tcb_state y) (x y)\<rbrakk> \<Longrightarrow> (x, a, b) \<in> ran tcb_cap_cases \<longrightarrow> b t (tcb_state y) (x y)
 2. \<And>s y. \<lbrakk>\<And>tcb. tcb_ipcframe (f tcb) = tcb_ipcframe tcb; valid_objs s; kheap s t = Some (TCB y); \<forall>x a b. (x, a, b) \<in> ran tcb_cap_cases \<longrightarrow> s \<turnstile> x y \<and> b t (tcb_state y) (x y); valid_ipc_buffer_cap (tcb_ipcframe y) (tcb_ipc_buffer y); valid_tcb_state (tcb_state y) s; case tcb_fault y of None \<Rightarrow> True | Some f \<Rightarrow> valid_fault f; length (tcb_fault_handler y) = word_bits; case tcb_bound_notification y of None \<Rightarrow> True | Some a \<Rightarrow> ntfn_at a s; valid_arch_tcb (tcb_arch y) s\<rbrakk> \<Longrightarrow> valid_ipc_buffer_cap (tcb_ipcframe y) (tcb_ipc_buffer (f y)) \<and> (case tcb_fault (f y) of None \<Rightarrow> True | Some x \<Rightarrow> valid_fault x) \<and> length (tcb_fault_handler (f y)) = word_bits \<and> (case tcb_bound_notification (f y) of None \<Rightarrow> True | Some a \<Rightarrow> ntfn_at a s) proof (prove)
goal (1 subgoal):
 1. \<And>s y. \<lbrakk>\<And>tcb. tcb_ipcframe (f tcb) = tcb_ipcframe tcb; valid_objs s; kheap s t = Some (TCB y); \<forall>x a b. (x, a, b) \<in> ran tcb_cap_cases \<longrightarrow> s \<turnstile> x y \<and> b t (tcb_state y) (x y); valid_ipc_buffer_cap (tcb_ipcframe y) (tcb_ipc_buffer y); valid_tcb_state (tcb_state y) s; case tcb_fault y of None \<Rightarrow> True | Some f \<Rightarrow> valid_fault f; length (tcb_fault_handler y) = word_bits; case tcb_bound_notification y of None \<Rightarrow> True | Some a \<Rightarrow> ntfn_at a s; valid_arch_tcb (tcb_arch y) s\<rbrakk> \<Longrightarrow> valid_ipc_buffer_cap (tcb_ipcframe y) (tcb_ipc_buffer (f y)) \<and> (case tcb_fault (f y) of None \<Rightarrow> True | Some x \<Rightarrow> valid_fault x) \<and> length (tcb_fault_handler (f y)) = word_bits \<and> (case tcb_bound_notification (f y) of None \<Rightarrow> True | Some a \<Rightarrow> ntfn_at a s) proof (prove)
goal (2 subgoals):
 1. \<And>s y. \<lbrakk>\<And>tcb. tcb_ipcframe (f tcb) = tcb_ipcframe tcb; valid_objs s; kheap s t = Some (TCB y); \<forall>x a b. (x, a, b) \<in> ran tcb_cap_cases \<longrightarrow> s \<turnstile> x y \<and> b t (tcb_state y) (x y); valid_ipc_buffer_cap (tcb_ipcframe y) (tcb_ipc_buffer y); valid_tcb_state (tcb_state y) s; case tcb_fault y of None \<Rightarrow> True | Some f \<Rightarrow> valid_fault f; length (tcb_fault_handler y) = word_bits; case tcb_bound_notification y of None \<Rightarrow> True | Some a \<Rightarrow> ntfn_at a s; valid_arch_tcb (tcb_arch y) s\<rbrakk> \<Longrightarrow> valid_ipc_buffer_cap (tcb_ipcframe y) (tcb_ipc_buffer (f y))
 2. \<And>s y. \<lbrakk>\<And>tcb. tcb_ipcframe (f tcb) = tcb_ipcframe tcb; valid_objs s; kheap s t = Some (TCB y); \<forall>x a b. (x, a, b) \<in> ran tcb_cap_cases \<longrightarrow> s \<turnstile> x y \<and> b t (tcb_state y) (x y); valid_ipc_buffer_cap (tcb_ipcframe y) (tcb_ipc_buffer y); valid_tcb_state (tcb_state y) s; case tcb_fault y of None \<Rightarrow> True | Some f \<Rightarrow> valid_fault f; length (tcb_fault_handler y) = word_bits; case tcb_bound_notification y of None \<Rightarrow> True | Some a \<Rightarrow> ntfn_at a s; valid_arch_tcb (tcb_arch y) s\<rbrakk> \<Longrightarrow> (case tcb_fault (f y) of None \<Rightarrow> True | Some x \<Rightarrow> valid_fault x) \<and> length (tcb_fault_handler (f y)) = word_bits \<and> (case tcb_bound_notification (f y) of None \<Rightarrow> True | Some a \<Rightarrow> ntfn_at a s) proof (prove)
goal (2 subgoals):
 1. \<And>s y. \<lbrakk>\<And>tcb. tcb_ipcframe (f tcb) = tcb_ipcframe tcb; valid_objs s; kheap s t = Some (TCB y); \<forall>x a b. (x, a, b) \<in> ran tcb_cap_cases \<longrightarrow> s \<turnstile> x y \<and> b t (tcb_state y) (x y); valid_ipc_buffer_cap (tcb_ipcframe y) (tcb_ipc_buffer y); valid_tcb_state (tcb_state y) s; case tcb_fault y of None \<Rightarrow> True | Some f \<Rightarrow> valid_fault f; length (tcb_fault_handler y) = word_bits; case tcb_bound_notification y of None \<Rightarrow> True | Some a \<Rightarrow> ntfn_at a s; valid_arch_tcb (tcb_arch y) s; tcb_ipc_buffer (f y) = tcb_ipc_buffer y \<or> tcb_ipc_buffer (f y) = 0\<rbrakk> \<Longrightarrow> valid_ipc_buffer_cap (tcb_ipcframe y) (tcb_ipc_buffer (f y))
 2. \<And>s y. \<lbrakk>\<And>tcb. tcb_ipcframe (f tcb) = tcb_ipcframe tcb; valid_objs s; kheap s t = Some (TCB y); \<forall>x a b. (x, a, b) \<in> ran tcb_cap_cases \<longrightarrow> s \<turnstile> x y \<and> b t (tcb_state y) (x y); valid_ipc_buffer_cap (tcb_ipcframe y) (tcb_ipc_buffer y); valid_tcb_state (tcb_state y) s; case tcb_fault y of None \<Rightarrow> True | Some f \<Rightarrow> valid_fault f; length (tcb_fault_handler y) = word_bits; case tcb_bound_notification y of None \<Rightarrow> True | Some a \<Rightarrow> ntfn_at a s; valid_arch_tcb (tcb_arch y) s\<rbrakk> \<Longrightarrow> (case tcb_fault (f y) of None \<Rightarrow> True | Some x \<Rightarrow> valid_fault x) \<and> length (tcb_fault_handler (f y)) = word_bits \<and> (case tcb_bound_notification (f y) of None \<Rightarrow> True | Some a \<Rightarrow> ntfn_at a s) proof (prove)
goal (1 subgoal):
 1. \<And>s y. \<lbrakk>\<And>tcb. tcb_ipcframe (f tcb) = tcb_ipcframe tcb; valid_objs s; kheap s t = Some (TCB y); \<forall>x a b. (x, a, b) \<in> ran tcb_cap_cases \<longrightarrow> s \<turnstile> x y \<and> b t (tcb_state y) (x y); valid_ipc_buffer_cap (tcb_ipcframe y) (tcb_ipc_buffer y); valid_tcb_state (tcb_state y) s; case tcb_fault y of None \<Rightarrow> True | Some f \<Rightarrow> valid_fault f; length (tcb_fault_handler y) = word_bits; case tcb_bound_notification y of None \<Rightarrow> True | Some a \<Rightarrow> ntfn_at a s; valid_arch_tcb (tcb_arch y) s\<rbrakk> \<Longrightarrow> (case tcb_fault (f y) of None \<Rightarrow> True | Some x \<Rightarrow> valid_fault x) \<and> length (tcb_fault_handler (f y)) = word_bits \<and> (case tcb_bound_notification (f y) of None \<Rightarrow> True | Some a \<Rightarrow> ntfn_at a s) proof (prove)
goal (1 subgoal):
 1. \<And>s y. \<lbrakk>\<And>tcb. tcb_ipcframe (f tcb) = tcb_ipcframe tcb; valid_objs s; kheap s t = Some (TCB y); \<forall>x a b. (x, a, b) \<in> ran tcb_cap_cases \<longrightarrow> s \<turnstile> x y \<and> b t (tcb_state y) (x y); valid_ipc_buffer_cap (tcb_ipcframe y) (tcb_ipc_buffer y); valid_tcb_state (tcb_state y) s; case tcb_fault y of None \<Rightarrow> True | Some f \<Rightarrow> valid_fault f; length (tcb_fault_handler y) = word_bits; case tcb_bound_notification y of None \<Rightarrow> True | Some a \<Rightarrow> ntfn_at a s; valid_arch_tcb (tcb_arch y) s; tcb_fault_handler (f y) \<noteq> tcb_fault_handler y \<longrightarrow> length (tcb_fault_handler (f y)) = word_bits\<rbrakk> \<Longrightarrow> (case tcb_fault (f y) of None \<Rightarrow> True | Some x \<Rightarrow> valid_fault x) \<and> length (tcb_fault_handler (f y)) = word_bits \<and> (case tcb_bound_notification (f y) of None \<Rightarrow> True | Some a \<Rightarrow> ntfn_at a s) proof (prove)
goal (1 subgoal):
 1. \<And>s y. \<lbrakk>\<And>tcb. tcb_ipcframe (f tcb) = tcb_ipcframe tcb; valid_objs s; kheap s t = Some (TCB y); \<forall>x a b. (x, a, b) \<in> ran tcb_cap_cases \<longrightarrow> s \<turnstile> x y \<and> b t (tcb_state y) (x y); valid_ipc_buffer_cap (tcb_ipcframe y) (tcb_ipc_buffer y); valid_tcb_state (tcb_state y) s; case tcb_fault y of None \<Rightarrow> True | Some f \<Rightarrow> valid_fault f; length (tcb_fault_handler y) = word_bits; case tcb_bound_notification y of None \<Rightarrow> True | Some a \<Rightarrow> ntfn_at a s; valid_arch_tcb (tcb_arch y) s; tcb_fault_handler (f y) \<noteq> tcb_fault_handler y \<longrightarrow> length (tcb_fault_handler (f y)) = word_bits; tcb_fault (f y) \<noteq> tcb_fault y \<longrightarrow> (case tcb_fault (f y) of None \<Rightarrow> True | Some f \<Rightarrow> valid_fault f)\<rbrakk> \<Longrightarrow> (case tcb_fault (f y) of None \<Rightarrow> True | Some x \<Rightarrow> valid_fault x) \<and> length (tcb_fault_handler (f y)) = word_bits \<and> (case tcb_bound_notification (f y) of None \<Rightarrow> True | Some a \<Rightarrow> ntfn_at a s) proof (prove)
goal (1 subgoal):
 1. \<And>s y. \<lbrakk>\<And>tcb. tcb_ipcframe (f tcb) = tcb_ipcframe tcb; valid_objs s; kheap s t = Some (TCB y); \<forall>x a b. (x, a, b) \<in> ran tcb_cap_cases \<longrightarrow> s \<turnstile> x y \<and> b t (tcb_state y) (x y); valid_ipc_buffer_cap (tcb_ipcframe y) (tcb_ipc_buffer y); valid_tcb_state (tcb_state y) s; case tcb_fault y of None \<Rightarrow> True | Some f \<Rightarrow> valid_fault f; length (tcb_fault_handler y) = word_bits; case tcb_bound_notification y of None \<Rightarrow> True | Some a \<Rightarrow> ntfn_at a s; valid_arch_tcb (tcb_arch y) s; tcb_fault_handler (f y) \<noteq> tcb_fault_handler y \<longrightarrow> length (tcb_fault_handler (f y)) = word_bits; tcb_fault (f y) \<noteq> tcb_fault y \<longrightarrow> (case tcb_fault (f y) of None \<Rightarrow> True | Some f \<Rightarrow> valid_fault f); tcb_bound_notification (f y) \<noteq> tcb_bound_notification y \<longrightarrow> tcb_bound_notification (f y) = None\<rbrakk> \<Longrightarrow> (case tcb_fault (f y) of None \<Rightarrow> True | Some x \<Rightarrow> valid_fault x) \<and> length (tcb_fault_handler (f y)) = word_bits \<and> (case tcb_bound_notification (f y) of None \<Rightarrow> True | Some a \<Rightarrow> ntfn_at a s)