theory CSpaceInv_AI

lemma set_cap_valid_objs:
  "\<lbrace>(valid_objs::'state_ext::state_ext state \<Rightarrow> bool) and valid_cap x
        and tcb_cap_valid x p\<rbrace>
      set_cap x p \<lbrace>\<lambda>_. valid_objs\<rbrace>" apply (simp add: set_cap_def split_def) apply (rule hoare_seq_ext [OF _ get_object_sp]) apply (case_tac obj, simp_all split del: if_split) apply clarsimp apply (wp set_object_valid_objs) apply (clarsimp simp: obj_at_def a_type_def wf_cs_upd) apply (erule(1) valid_objsE) apply (clarsimp simp: valid_obj_def valid_cs_def
                         valid_cs_size_def wf_cs_upd) apply (clarsimp simp: ran_def split: if_split_asm) apply blast apply (rule hoare_pre, wp set_object_valid_objs) apply (clarsimp simp: obj_at_def a_type_def tcb_cap_valid_def
                        is_tcb_def) apply (erule(1) valid_objsE) apply (clarsimp simp: valid_obj_def valid_tcb_def
                        ran_tcb_cap_cases) apply (intro conjI impI, simp_all add: pred_tcb_at_def obj_at_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs and valid_cap x and tcb_cap_valid x p\<rbrace> set_cap x p \<lbrace>\<lambda>_. valid_objs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs and valid_cap x and tcb_cap_valid x p\<rbrace> do obj <- get_object (fst p);
(case obj of CNode sz cn \<Rightarrow> if snd p \<in> dom cn \<and> well_formed_cnode_n sz cn then return $ CNode sz $ cn(snd p \<mapsto> x) else fail | TCB tcb \<Rightarrow> if snd p = tcb_cnode_index 0 then return $ TCB $ tcb\<lparr>tcb_ctable := x\<rparr> else if snd p = tcb_cnode_index 1 then return $ TCB $ tcb\<lparr>tcb_vtable := x\<rparr> else if snd p = tcb_cnode_index 2 then return $ TCB $ tcb\<lparr>tcb_reply := x\<rparr> else if snd p = tcb_cnode_index 3 then return $ TCB $ tcb\<lparr>tcb_caller := x\<rparr> else if snd p = tcb_cnode_index 4 then return $ TCB $ tcb\<lparr>tcb_ipcframe := x\<rparr> else fail | _ \<Rightarrow> fail) >>= set_object (fst p)
od \<lbrace>\<lambda>_. valid_objs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>obj. \<lbrace>valid_objs and valid_cap x and tcb_cap_valid x p and ko_at obj (fst p)\<rbrace> (case obj of CNode sz cn \<Rightarrow> if snd p \<in> dom cn \<and> well_formed_cnode_n sz cn then return $ CNode sz $ cn(snd p \<mapsto> x) else fail | TCB tcb \<Rightarrow> if snd p = tcb_cnode_index 0 then return $ TCB $ tcb\<lparr>tcb_ctable := x\<rparr> else if snd p = tcb_cnode_index 1 then return $ TCB $ tcb\<lparr>tcb_vtable := x\<rparr> else if snd p = tcb_cnode_index 2 then return $ TCB $ tcb\<lparr>tcb_reply := x\<rparr> else if snd p = tcb_cnode_index 3 then return $ TCB $ tcb\<lparr>tcb_caller := x\<rparr> else if snd p = tcb_cnode_index 4 then return $ TCB $ tcb\<lparr>tcb_ipcframe := x\<rparr> else fail | _ \<Rightarrow> fail) >>= set_object (fst p) \<lbrace>\<lambda>_. valid_objs\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>obj x11 x12. obj = CNode x11 x12 \<Longrightarrow> \<lbrace>valid_objs and valid_cap x and tcb_cap_valid x p and ko_at (CNode x11 x12) (fst p)\<rbrace> (if snd p \<in> dom x12 \<and> well_formed_cnode_n x11 x12 then return $ CNode x11 $ x12(snd p \<mapsto> x) else fail) >>= set_object (fst p) \<lbrace>\<lambda>_. valid_objs\<rbrace>
 2. \<And>obj x2. obj = TCB x2 \<Longrightarrow> \<lbrace>valid_objs and valid_cap x and tcb_cap_valid x p and ko_at (TCB x2) (fst p)\<rbrace> (if snd p = tcb_cnode_index 0 then return $ TCB $ x2\<lparr>tcb_ctable := x\<rparr> else if snd p = tcb_cnode_index 1 then return $ TCB $ x2\<lparr>tcb_vtable := x\<rparr> else if snd p = tcb_cnode_index 2 then return $ TCB $ x2\<lparr>tcb_reply := x\<rparr> else if snd p = tcb_cnode_index 3 then return $ TCB $ x2\<lparr>tcb_caller := x\<rparr> else if snd p = tcb_cnode_index 4 then return $ TCB $ x2\<lparr>tcb_ipcframe := x\<rparr> else fail) >>= set_object (fst p) \<lbrace>\<lambda>_. valid_objs\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x11 x12 y. \<lbrakk>well_formed_cnode_n x11 x12; x12 (snd p) = Some y\<rbrakk> \<Longrightarrow> \<lbrace>valid_objs and valid_cap x and tcb_cap_valid x p and ko_at (CNode x11 x12) (fst p)\<rbrace> set_object (fst p) (CNode x11 (x12(snd p \<mapsto> x))) \<lbrace>\<lambda>_. valid_objs\<rbrace>
 2. \<And>obj x2. obj = TCB x2 \<Longrightarrow> \<lbrace>valid_objs and valid_cap x and tcb_cap_valid x p and ko_at (TCB x2) (fst p)\<rbrace> (if snd p = tcb_cnode_index 0 then return $ TCB $ x2\<lparr>tcb_ctable := x\<rparr> else if snd p = tcb_cnode_index 1 then return $ TCB $ x2\<lparr>tcb_vtable := x\<rparr> else if snd p = tcb_cnode_index 2 then return $ TCB $ x2\<lparr>tcb_reply := x\<rparr> else if snd p = tcb_cnode_index 3 then return $ TCB $ x2\<lparr>tcb_caller := x\<rparr> else if snd p = tcb_cnode_index 4 then return $ TCB $ x2\<lparr>tcb_ipcframe := x\<rparr> else fail) >>= set_object (fst p) \<lbrace>\<lambda>_. valid_objs\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x11 x12 y s. \<lbrakk>well_formed_cnode_n x11 x12; x12 (snd p) = Some y; (valid_objs and valid_cap x and tcb_cap_valid x p and ko_at (CNode x11 x12) (fst p)) s\<rbrakk> \<Longrightarrow> (valid_objs and valid_obj (fst p) (CNode x11 (x12(snd p \<mapsto> x)))) s
 2. \<And>obj x2. obj = TCB x2 \<Longrightarrow> \<lbrace>valid_objs and valid_cap x and tcb_cap_valid x p and ko_at (TCB x2) (fst p)\<rbrace> (if snd p = tcb_cnode_index 0 then return $ TCB $ x2\<lparr>tcb_ctable := x\<rparr> else if snd p = tcb_cnode_index 1 then return $ TCB $ x2\<lparr>tcb_vtable := x\<rparr> else if snd p = tcb_cnode_index 2 then return $ TCB $ x2\<lparr>tcb_reply := x\<rparr> else if snd p = tcb_cnode_index 3 then return $ TCB $ x2\<lparr>tcb_caller := x\<rparr> else if snd p = tcb_cnode_index 4 then return $ TCB $ x2\<lparr>tcb_ipcframe := x\<rparr> else fail) >>= set_object (fst p) \<lbrace>\<lambda>_. valid_objs\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x11 x12 y s. \<lbrakk>well_formed_cnode_n x11 x12; x12 (snd p) = Some y; valid_objs s; s \<turnstile> x; tcb_cap_valid x p s; kheap s (fst p) = Some (CNode x11 x12)\<rbrakk> \<Longrightarrow> valid_obj (fst p) (CNode x11 (x12(snd p \<mapsto> x))) s
 2. \<And>obj x2. obj = TCB x2 \<Longrightarrow> \<lbrace>valid_objs and valid_cap x and tcb_cap_valid x p and ko_at (TCB x2) (fst p)\<rbrace> (if snd p = tcb_cnode_index 0 then return $ TCB $ x2\<lparr>tcb_ctable := x\<rparr> else if snd p = tcb_cnode_index 1 then return $ TCB $ x2\<lparr>tcb_vtable := x\<rparr> else if snd p = tcb_cnode_index 2 then return $ TCB $ x2\<lparr>tcb_reply := x\<rparr> else if snd p = tcb_cnode_index 3 then return $ TCB $ x2\<lparr>tcb_caller := x\<rparr> else if snd p = tcb_cnode_index 4 then return $ TCB $ x2\<lparr>tcb_ipcframe := x\<rparr> else fail) >>= set_object (fst p) \<lbrace>\<lambda>_. valid_objs\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x11 x12 y s. \<lbrakk>well_formed_cnode_n x11 x12; x12 (snd p) = Some y; s \<turnstile> x; tcb_cap_valid x p s; kheap s (fst p) = Some (CNode x11 x12); valid_obj (fst p) (CNode x11 x12) s\<rbrakk> \<Longrightarrow> valid_obj (fst p) (CNode x11 (x12(snd p \<mapsto> x))) s
 2. \<And>obj x2. obj = TCB x2 \<Longrightarrow> \<lbrace>valid_objs and valid_cap x and tcb_cap_valid x p and ko_at (TCB x2) (fst p)\<rbrace> (if snd p = tcb_cnode_index 0 then return $ TCB $ x2\<lparr>tcb_ctable := x\<rparr> else if snd p = tcb_cnode_index 1 then return $ TCB $ x2\<lparr>tcb_vtable := x\<rparr> else if snd p = tcb_cnode_index 2 then return $ TCB $ x2\<lparr>tcb_reply := x\<rparr> else if snd p = tcb_cnode_index 3 then return $ TCB $ x2\<lparr>tcb_caller := x\<rparr> else if snd p = tcb_cnode_index 4 then return $ TCB $ x2\<lparr>tcb_ipcframe := x\<rparr> else fail) >>= set_object (fst p) \<lbrace>\<lambda>_. valid_objs\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x11 x12 y s cap. \<lbrakk>well_formed_cnode_n x11 x12; x12 (snd p) = Some y; s \<turnstile> x; tcb_cap_valid x p s; kheap s (fst p) = Some (CNode x11 x12); cap \<in> ran (x12(snd p \<mapsto> x)); \<forall>cap\<in>ran x12. s \<turnstile> cap; x11 < word_bits - cte_level_bits\<rbrakk> \<Longrightarrow> s \<turnstile> cap
 2. \<And>obj x2. obj = TCB x2 \<Longrightarrow> \<lbrace>valid_objs and valid_cap x and tcb_cap_valid x p and ko_at (TCB x2) (fst p)\<rbrace> (if snd p = tcb_cnode_index 0 then return $ TCB $ x2\<lparr>tcb_ctable := x\<rparr> else if snd p = tcb_cnode_index 1 then return $ TCB $ x2\<lparr>tcb_vtable := x\<rparr> else if snd p = tcb_cnode_index 2 then return $ TCB $ x2\<lparr>tcb_reply := x\<rparr> else if snd p = tcb_cnode_index 3 then return $ TCB $ x2\<lparr>tcb_caller := x\<rparr> else if snd p = tcb_cnode_index 4 then return $ TCB $ x2\<lparr>tcb_ipcframe := x\<rparr> else fail) >>= set_object (fst p) \<lbrace>\<lambda>_. valid_objs\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x11 x12 y s cap a. \<lbrakk>\<forall>cap. (\<exists>a. x12 a = Some cap) \<longrightarrow> s \<turnstile> cap; x11 < word_bits - cte_level_bits; well_formed_cnode_n x11 x12; x12 (snd p) = Some y; s \<turnstile> x; tcb_cap_valid x p s; kheap s (fst p) = Some (CNode x11 x12); a = snd p \<longrightarrow> x = cap; a = snd p \<or> x12 a = Some cap\<rbrakk> \<Longrightarrow> s \<turnstile> cap
 2. \<And>obj x2. obj = TCB x2 \<Longrightarrow> \<lbrace>valid_objs and valid_cap x and tcb_cap_valid x p and ko_at (TCB x2) (fst p)\<rbrace> (if snd p = tcb_cnode_index 0 then return $ TCB $ x2\<lparr>tcb_ctable := x\<rparr> else if snd p = tcb_cnode_index 1 then return $ TCB $ x2\<lparr>tcb_vtable := x\<rparr> else if snd p = tcb_cnode_index 2 then return $ TCB $ x2\<lparr>tcb_reply := x\<rparr> else if snd p = tcb_cnode_index 3 then return $ TCB $ x2\<lparr>tcb_caller := x\<rparr> else if snd p = tcb_cnode_index 4 then return $ TCB $ x2\<lparr>tcb_ipcframe := x\<rparr> else fail) >>= set_object (fst p) \<lbrace>\<lambda>_. valid_objs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>obj x2. obj = TCB x2 \<Longrightarrow> \<lbrace>valid_objs and valid_cap x and tcb_cap_valid x p and ko_at (TCB x2) (fst p)\<rbrace> (if snd p = tcb_cnode_index 0 then return $ TCB $ x2\<lparr>tcb_ctable := x\<rparr> else if snd p = tcb_cnode_index 1 then return $ TCB $ x2\<lparr>tcb_vtable := x\<rparr> else if snd p = tcb_cnode_index 2 then return $ TCB $ x2\<lparr>tcb_reply := x\<rparr> else if snd p = tcb_cnode_index 3 then return $ TCB $ x2\<lparr>tcb_caller := x\<rparr> else if snd p = tcb_cnode_index 4 then return $ TCB $ x2\<lparr>tcb_ipcframe := x\<rparr> else fail) >>= set_object (fst p) \<lbrace>\<lambda>_. valid_objs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>obj x2 s. \<lbrakk>obj = TCB x2; (valid_objs and valid_cap x and tcb_cap_valid x p and ko_at (TCB x2) (fst p)) s\<rbrakk> \<Longrightarrow> (snd p = tcb_cnode_index 0 \<longrightarrow> valid_objs s \<and> valid_obj (fst p) (TCB $ x2\<lparr>tcb_ctable := x\<rparr>) s) \<and> (snd p \<noteq> tcb_cnode_index 0 \<longrightarrow> (snd p = tcb_cnode_index 1 \<longrightarrow> valid_objs s \<and> valid_obj (fst p) (TCB $ x2\<lparr>tcb_vtable := x\<rparr>) s) \<and> (snd p \<noteq> tcb_cnode_index 1 \<longrightarrow> (snd p = tcb_cnode_index 2 \<longrightarrow> valid_objs s \<and> valid_obj (fst p) (TCB $ x2\<lparr>tcb_reply := x\<rparr>) s) \<and> (snd p \<noteq> tcb_cnode_index 2 \<longrightarrow> (snd p = tcb_cnode_index 3 \<longrightarrow> valid_objs s \<and> valid_obj (fst p) (TCB $ x2\<lparr>tcb_caller := x\<rparr>) s) \<and> (snd p \<noteq> tcb_cnode_index 3 \<longrightarrow> (snd p = tcb_cnode_index 4 \<longrightarrow> valid_objs s \<and> valid_obj (fst p) (TCB $ x2\<lparr>tcb_ipcframe := x\<rparr>) s) \<and> (snd p \<noteq> tcb_cnode_index 4 \<longrightarrow> True))))) proof (prove)
goal (1 subgoal):
 1. \<And>x2 s. \<lbrakk>valid_objs s; s \<turnstile> x; kheap s (fst p) = Some (TCB x2); st_tcb_at (\<lambda>st. case tcb_cap_cases (snd p) of None \<Rightarrow> True | Some (getF, setF, restr) \<Rightarrow> restr (fst p) st x) (fst p) s; snd p = tcb_cnode_index 4 \<longrightarrow> valid_ipc_buffer_cap x (tcb_ipc_buffer x2)\<rbrakk> \<Longrightarrow> (snd p = tcb_cnode_index 0 \<longrightarrow> valid_obj (fst p) (TCB (x2\<lparr>tcb_ctable := x\<rparr>)) s) \<and> (snd p \<noteq> tcb_cnode_index 0 \<longrightarrow> (snd p = tcb_cnode_index (Suc 0) \<longrightarrow> valid_obj (fst p) (TCB (x2\<lparr>tcb_vtable := x\<rparr>)) s) \<and> (snd p \<noteq> tcb_cnode_index (Suc 0) \<longrightarrow> (snd p = tcb_cnode_index 2 \<longrightarrow> valid_obj (fst p) (TCB (x2\<lparr>tcb_reply := x\<rparr>)) s) \<and> (snd p \<noteq> tcb_cnode_index 2 \<longrightarrow> (snd p = tcb_cnode_index 3 \<longrightarrow> valid_obj (fst p) (TCB (x2\<lparr>tcb_caller := x\<rparr>)) s) \<and> (snd p \<noteq> tcb_cnode_index 3 \<longrightarrow> snd p = tcb_cnode_index 4 \<longrightarrow> valid_obj (fst p) (TCB (x2\<lparr>tcb_ipcframe := x\<rparr>)) s)))) proof (prove)
goal (1 subgoal):
 1. \<And>x2 s. \<lbrakk>s \<turnstile> x; kheap s (fst p) = Some (TCB x2); st_tcb_at (\<lambda>st. case tcb_cap_cases (snd p) of None \<Rightarrow> True | Some (getF, setF, restr) \<Rightarrow> restr (fst p) st x) (fst p) s; snd p = tcb_cnode_index 4 \<longrightarrow> valid_ipc_buffer_cap x (tcb_ipc_buffer x2); valid_obj (fst p) (TCB x2) s\<rbrakk> \<Longrightarrow> (snd p = tcb_cnode_index 0 \<longrightarrow> valid_obj (fst p) (TCB (x2\<lparr>tcb_ctable := x\<rparr>)) s) \<and> (snd p \<noteq> tcb_cnode_index 0 \<longrightarrow> (snd p = tcb_cnode_index (Suc 0) \<longrightarrow> valid_obj (fst p) (TCB (x2\<lparr>tcb_vtable := x\<rparr>)) s) \<and> (snd p \<noteq> tcb_cnode_index (Suc 0) \<longrightarrow> (snd p = tcb_cnode_index 2 \<longrightarrow> valid_obj (fst p) (TCB (x2\<lparr>tcb_reply := x\<rparr>)) s) \<and> (snd p \<noteq> tcb_cnode_index 2 \<longrightarrow> (snd p = tcb_cnode_index 3 \<longrightarrow> valid_obj (fst p) (TCB (x2\<lparr>tcb_caller := x\<rparr>)) s) \<and> (snd p \<noteq> tcb_cnode_index 3 \<longrightarrow> snd p = tcb_cnode_index 4 \<longrightarrow> valid_obj (fst p) (TCB (x2\<lparr>tcb_ipcframe := x\<rparr>)) s)))) proof (prove)
goal (1 subgoal):
 1. \<And>x2 s. \<lbrakk>s \<turnstile> x; kheap s (fst p) = Some (TCB x2); st_tcb_at (\<lambda>st. case tcb_cap_cases (snd p) of None \<Rightarrow> True | Some (getF, setF, restr) \<Rightarrow> restr (fst p) st x) (fst p) s; snd p = tcb_cnode_index 4 \<longrightarrow> valid_ipc_buffer_cap x (tcb_ipc_buffer x2); s \<turnstile> tcb_ctable x2; s \<turnstile> tcb_vtable x2; is_valid_vtable_root (tcb_vtable x2) \<or> NullCap = tcb_vtable x2; s \<turnstile> tcb_reply x2; is_master_reply_cap (tcb_reply x2) \<and> obj_ref_of (tcb_reply x2) = fst p \<and> AllowGrant \<in> cap_rights (tcb_reply x2) \<or> halted (tcb_state x2) \<and> tcb_reply x2 = NullCap; s \<turnstile> tcb_caller x2; (case tcb_state x2 of BlockedOnReceive e data \<Rightarrow> (=) NullCap | _ \<Rightarrow> is_reply_cap or (=) NullCap) (tcb_caller x2); s \<turnstile> tcb_ipcframe x2; is_nondevice_page_cap (tcb_ipcframe x2) \<or> NullCap = tcb_ipcframe x2; valid_ipc_buffer_cap (tcb_ipcframe x2) (tcb_ipc_buffer x2); valid_tcb_state (tcb_state x2) s; case tcb_fault x2 of None \<Rightarrow> True | Some x \<Rightarrow> valid_fault x; length (tcb_fault_handler x2) = word_bits; valid_bound_ntfn (tcb_bound_notification x2) s; valid_arch_tcb (tcb_arch x2) s; snd p \<noteq> tcb_cnode_index 0\<rbrakk> \<Longrightarrow> (snd p = tcb_cnode_index (Suc 0) \<longrightarrow> is_valid_vtable_root x \<or> NullCap = x) \<and> (snd p \<noteq> tcb_cnode_index (Suc 0) \<longrightarrow> (snd p = tcb_cnode_index 2 \<longrightarrow> is_master_reply_cap x \<and> obj_ref_of x = fst p \<and> AllowGrant \<in> cap_rights x \<or> halted (tcb_state x2) \<and> x = NullCap) \<and> (snd p \<noteq> tcb_cnode_index 2 \<longrightarrow> (snd p = tcb_cnode_index 3 \<longrightarrow> (case tcb_state x2 of BlockedOnReceive e data \<Rightarrow> (=) NullCap | _ \<Rightarrow> is_reply_cap or (=) NullCap) x) \<and> (snd p \<noteq> tcb_cnode_index 3 \<longrightarrow> snd p = tcb_cnode_index 4 \<longrightarrow> is_nondevice_page_cap x \<or> NullCap = x))) proof (prove)
goal:
No subgoals!