theory CSpaceInvPre_AI

lemma set_cap_caps_of_state[wp]:
  "\<lbrace>\<lambda>s. P ((caps_of_state s) (ptr \<mapsto> cap))\<rbrace> set_cap cap ptr \<lbrace>\<lambda>rv s. P (caps_of_state s)\<rbrace>" apply (cases ptr) apply (clarsimp 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 cong: if_cong bind_cong) apply (wpsimp wp: set_object_wp) apply (fastforce elim!: rsubst[where P=P]
                    simp: caps_of_state_cte_wp_at cte_wp_at_cases
                          fun_upd_def[symmetric] wf_cs_upd obj_at_def) apply (wpsimp wp: set_object_wp) apply (clarsimp simp: obj_at_def) apply (safe elim!: rsubst[where P=P];
         rule ext; clarsimp simp: caps_of_state_cte_wp_at cte_wp_at_cases) apply (auto simp: tcb_cap_cases_def split: if_split_asm) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P ((caps_of_state s)(ptr \<mapsto> cap))\<rbrace> set_cap cap ptr \<lbrace>\<lambda>rv s. P (caps_of_state s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>a b. ptr = (a, b) \<Longrightarrow> \<lbrace>\<lambda>s. P ((caps_of_state s)(ptr \<mapsto> cap))\<rbrace> set_cap cap ptr \<lbrace>\<lambda>rv s. P (caps_of_state s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>a b. ptr = (a, b) \<Longrightarrow> \<lbrace>\<lambda>s. P ((caps_of_state s)((a, b) \<mapsto> cap))\<rbrace> do obj <- get_object a;
(case obj of CNode sz cn \<Rightarrow> if snd (a, b) \<in> dom cn \<and> well_formed_cnode_n sz cn then return $ CNode sz $ cn(snd (a, b) \<mapsto> cap) else fail | TCB tcb \<Rightarrow> if snd (a, b) = tcb_cnode_index 0 then return $ TCB $ tcb\<lparr>tcb_ctable := cap\<rparr> else if snd (a, b) = tcb_cnode_index 1 then return $ TCB $ tcb\<lparr>tcb_vtable := cap\<rparr> else if snd (a, b) = tcb_cnode_index 2 then return $ TCB $ tcb\<lparr>tcb_reply := cap\<rparr> else if snd (a, b) = tcb_cnode_index 3 then return $ TCB $ tcb\<lparr>tcb_caller := cap\<rparr> else if snd (a, b) = tcb_cnode_index 4 then return $ TCB $ tcb\<lparr>tcb_ipcframe := cap\<rparr> else fail | _ \<Rightarrow> fail) >>= set_object a
od \<lbrace>\<lambda>rv s. P (caps_of_state s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>a b obj. ptr = (a, b) \<Longrightarrow> \<lbrace>(\<lambda>s. P ((caps_of_state s)((a, b) \<mapsto> cap))) and ko_at obj a\<rbrace> (case obj of CNode sz cn \<Rightarrow> if snd (a, b) \<in> dom cn \<and> well_formed_cnode_n sz cn then return $ CNode sz $ cn(snd (a, b) \<mapsto> cap) else fail | TCB tcb \<Rightarrow> if snd (a, b) = tcb_cnode_index 0 then return $ TCB $ tcb\<lparr>tcb_ctable := cap\<rparr> else if snd (a, b) = tcb_cnode_index 1 then return $ TCB $ tcb\<lparr>tcb_vtable := cap\<rparr> else if snd (a, b) = tcb_cnode_index 2 then return $ TCB $ tcb\<lparr>tcb_reply := cap\<rparr> else if snd (a, b) = tcb_cnode_index 3 then return $ TCB $ tcb\<lparr>tcb_caller := cap\<rparr> else if snd (a, b) = tcb_cnode_index 4 then return $ TCB $ tcb\<lparr>tcb_ipcframe := cap\<rparr> else fail | _ \<Rightarrow> fail) >>= set_object a \<lbrace>\<lambda>rv s. P (caps_of_state s)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>a b obj x11 x12. \<lbrakk>ptr = (a, b); obj = CNode x11 x12\<rbrakk> \<Longrightarrow> \<lbrace>(\<lambda>s. P ((caps_of_state s)((a, b) \<mapsto> cap))) and ko_at (CNode x11 x12) a\<rbrace> (if b \<in> dom x12 \<and> well_formed_cnode_n x11 x12 then return (CNode x11 (x12(b \<mapsto> cap))) else fail) >>= set_object a \<lbrace>\<lambda>rv s. P (caps_of_state s)\<rbrace>
 2. \<And>a b obj x2. \<lbrakk>ptr = (a, b); obj = TCB x2\<rbrakk> \<Longrightarrow> \<lbrace>(\<lambda>s. P ((caps_of_state s)((a, b) \<mapsto> cap))) and ko_at (TCB x2) a\<rbrace> (if b = tcb_cnode_index 0 then return (TCB (x2\<lparr>tcb_ctable := cap\<rparr>)) else if b = tcb_cnode_index (Suc 0) then return (TCB (x2\<lparr>tcb_vtable := cap\<rparr>)) else if b = tcb_cnode_index 2 then return (TCB (x2\<lparr>tcb_reply := cap\<rparr>)) else if b = tcb_cnode_index 3 then return (TCB (x2\<lparr>tcb_caller := cap\<rparr>)) else if b = tcb_cnode_index 4 then return (TCB (x2\<lparr>tcb_ipcframe := cap\<rparr>)) else fail) >>= set_object a \<lbrace>\<lambda>rv s. P (caps_of_state s)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>a b x11 x12 s y. \<lbrakk>ptr = (a, b); P ((caps_of_state s)((a, b) \<mapsto> cap)); ko_at (CNode x11 x12) a s; well_formed_cnode_n x11 x12; x12 b = Some y\<rbrakk> \<Longrightarrow> P (caps_of_state (s\<lparr>kheap := (kheap s)(a \<mapsto> CNode x11 (\<lambda>a. if a = b then Some cap else x12 a))\<rparr>))
 2. \<And>a b obj x2. \<lbrakk>ptr = (a, b); obj = TCB x2\<rbrakk> \<Longrightarrow> \<lbrace>(\<lambda>s. P ((caps_of_state s)((a, b) \<mapsto> cap))) and ko_at (TCB x2) a\<rbrace> (if b = tcb_cnode_index 0 then return (TCB (x2\<lparr>tcb_ctable := cap\<rparr>)) else if b = tcb_cnode_index (Suc 0) then return (TCB (x2\<lparr>tcb_vtable := cap\<rparr>)) else if b = tcb_cnode_index 2 then return (TCB (x2\<lparr>tcb_reply := cap\<rparr>)) else if b = tcb_cnode_index 3 then return (TCB (x2\<lparr>tcb_caller := cap\<rparr>)) else if b = tcb_cnode_index 4 then return (TCB (x2\<lparr>tcb_ipcframe := cap\<rparr>)) else fail) >>= set_object a \<lbrace>\<lambda>rv s. P (caps_of_state s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>a b obj x2. \<lbrakk>ptr = (a, b); obj = TCB x2\<rbrakk> \<Longrightarrow> \<lbrace>(\<lambda>s. P ((caps_of_state s)((a, b) \<mapsto> cap))) and ko_at (TCB x2) a\<rbrace> (if b = tcb_cnode_index 0 then return (TCB (x2\<lparr>tcb_ctable := cap\<rparr>)) else if b = tcb_cnode_index (Suc 0) then return (TCB (x2\<lparr>tcb_vtable := cap\<rparr>)) else if b = tcb_cnode_index 2 then return (TCB (x2\<lparr>tcb_reply := cap\<rparr>)) else if b = tcb_cnode_index 3 then return (TCB (x2\<lparr>tcb_caller := cap\<rparr>)) else if b = tcb_cnode_index 4 then return (TCB (x2\<lparr>tcb_ipcframe := cap\<rparr>)) else fail) >>= set_object a \<lbrace>\<lambda>rv s. P (caps_of_state s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>a b x2 s. \<lbrakk>ptr = (a, b); P ((caps_of_state s)((a, b) \<mapsto> cap)); ko_at (TCB x2) a s\<rbrakk> \<Longrightarrow> (b = tcb_cnode_index 0 \<longrightarrow> P (caps_of_state (s\<lparr>kheap := (kheap s)(a \<mapsto> TCB (x2\<lparr>tcb_ctable := cap\<rparr>))\<rparr>))) \<and> (b \<noteq> tcb_cnode_index 0 \<longrightarrow> (b = tcb_cnode_index (Suc 0) \<longrightarrow> P (caps_of_state (s\<lparr>kheap := (kheap s)(a \<mapsto> TCB (x2\<lparr>tcb_vtable := cap\<rparr>))\<rparr>))) \<and> (b \<noteq> tcb_cnode_index (Suc 0) \<longrightarrow> (b = tcb_cnode_index 2 \<longrightarrow> P (caps_of_state (s\<lparr>kheap := (kheap s)(a \<mapsto> TCB (x2\<lparr>tcb_reply := cap\<rparr>))\<rparr>))) \<and> (b \<noteq> tcb_cnode_index 2 \<longrightarrow> (b = tcb_cnode_index 3 \<longrightarrow> P (caps_of_state (s\<lparr>kheap := (kheap s)(a \<mapsto> TCB (x2\<lparr>tcb_caller := cap\<rparr>))\<rparr>))) \<and> (b \<noteq> tcb_cnode_index 3 \<longrightarrow> b = tcb_cnode_index 4 \<longrightarrow> P (caps_of_state (s\<lparr>kheap := (kheap s)(a \<mapsto> TCB (x2\<lparr>tcb_ipcframe := cap\<rparr>))\<rparr>)))))) proof (prove)
goal (1 subgoal):
 1. \<And>a b x2 s. \<lbrakk>ptr = (a, b); P ((caps_of_state s)((a, b) \<mapsto> cap)); kheap s a = Some (TCB x2)\<rbrakk> \<Longrightarrow> (b = tcb_cnode_index 0 \<longrightarrow> P (caps_of_state (s\<lparr>kheap := (kheap s)(a \<mapsto> TCB (x2\<lparr>tcb_ctable := cap\<rparr>))\<rparr>))) \<and> (b \<noteq> tcb_cnode_index 0 \<longrightarrow> (b = tcb_cnode_index (Suc 0) \<longrightarrow> P (caps_of_state (s\<lparr>kheap := (kheap s)(a \<mapsto> TCB (x2\<lparr>tcb_vtable := cap\<rparr>))\<rparr>))) \<and> (b \<noteq> tcb_cnode_index (Suc 0) \<longrightarrow> (b = tcb_cnode_index 2 \<longrightarrow> P (caps_of_state (s\<lparr>kheap := (kheap s)(a \<mapsto> TCB (x2\<lparr>tcb_reply := cap\<rparr>))\<rparr>))) \<and> (b \<noteq> tcb_cnode_index 2 \<longrightarrow> (b = tcb_cnode_index 3 \<longrightarrow> P (caps_of_state (s\<lparr>kheap := (kheap s)(a \<mapsto> TCB (x2\<lparr>tcb_caller := cap\<rparr>))\<rparr>))) \<and> (b \<noteq> tcb_cnode_index 3 \<longrightarrow> b = tcb_cnode_index 4 \<longrightarrow> P (caps_of_state (s\<lparr>kheap := (kheap s)(a \<mapsto> TCB (x2\<lparr>tcb_ipcframe := cap\<rparr>))\<rparr>)))))) proof (prove)
goal (5 subgoals):
 1. \<And>a x2 s aa b. \<lbrakk>ptr = (a, tcb_cnode_index 0); kheap s a = Some (TCB x2)\<rbrakk> \<Longrightarrow> (aa = a \<longrightarrow> ((\<exists>get set restr. tcb_cap_cases b = Some (get, set, restr)) \<longrightarrow> b \<noteq> tcb_cnode_index 0 \<longrightarrow> (THE cap. \<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> cap = get x2) = (THE capa. \<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> capa = get (x2\<lparr>tcb_ctable := cap\<rparr>))) \<and> ((\<forall>cap get. (\<forall>set restr. tcb_cap_cases b \<noteq> Some (get, set, restr)) \<or> cap \<noteq> get x2) \<longrightarrow> b \<noteq> tcb_cnode_index 0 \<longrightarrow> (\<forall>capa get. (\<forall>set restr. tcb_cap_cases b \<noteq> Some (get, set, restr)) \<or> capa \<noteq> get (x2\<lparr>tcb_ctable := cap\<rparr>)))) \<and> (aa \<noteq> a \<longrightarrow> (\<exists>cap. (\<exists>sz fun. kheap s aa = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> fun b = Some cap) \<or> (\<exists>tcb. kheap s aa = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> cap = get tcb))) \<longrightarrow> (\<exists>cap. (\<exists>sz fun. well_formed_cnode_n sz fun \<and> kheap s aa = Some (CNode sz fun) \<and> fun b = Some cap) \<or> (\<exists>tcb. kheap s aa = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> cap = get tcb))))
 2. \<And>a x2 s aa b. \<lbrakk>ptr = (a, tcb_cnode_index (Suc 0)); kheap s a = Some (TCB x2)\<rbrakk> \<Longrightarrow> (aa = a \<longrightarrow> ((\<exists>get set restr. tcb_cap_cases b = Some (get, set, restr)) \<longrightarrow> b \<noteq> tcb_cnode_index (Suc 0) \<longrightarrow> (THE cap. \<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> cap = get x2) = (THE capa. \<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> capa = get (x2\<lparr>tcb_vtable := cap\<rparr>))) \<and> ((\<forall>cap get. (\<forall>set restr. tcb_cap_cases b \<noteq> Some (get, set, restr)) \<or> cap \<noteq> get x2) \<longrightarrow> b \<noteq> tcb_cnode_index (Suc 0) \<longrightarrow> (\<forall>capa get. (\<forall>set restr. tcb_cap_cases b \<noteq> Some (get, set, restr)) \<or> capa \<noteq> get (x2\<lparr>tcb_vtable := cap\<rparr>)))) \<and> (aa \<noteq> a \<longrightarrow> (\<exists>cap. (\<exists>sz fun. kheap s aa = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> fun b = Some cap) \<or> (\<exists>tcb. kheap s aa = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> cap = get tcb))) \<longrightarrow> (\<exists>cap. (\<exists>sz fun. well_formed_cnode_n sz fun \<and> kheap s aa = Some (CNode sz fun) \<and> fun b = Some cap) \<or> (\<exists>tcb. kheap s aa = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> cap = get tcb))))
 3. \<And>a x2 s aa b. \<lbrakk>ptr = (a, tcb_cnode_index 2); kheap s a = Some (TCB x2)\<rbrakk> \<Longrightarrow> (aa = a \<longrightarrow> ((\<exists>get set restr. tcb_cap_cases b = Some (get, set, restr)) \<longrightarrow> b \<noteq> tcb_cnode_index 2 \<longrightarrow> (THE cap. \<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> cap = get x2) = (THE capa. \<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> capa = get (x2\<lparr>tcb_reply := cap\<rparr>))) \<and> ((\<forall>cap get. (\<forall>set restr. tcb_cap_cases b \<noteq> Some (get, set, restr)) \<or> cap \<noteq> get x2) \<longrightarrow> b \<noteq> tcb_cnode_index 2 \<longrightarrow> (\<forall>capa get. (\<forall>set restr. tcb_cap_cases b \<noteq> Some (get, set, restr)) \<or> capa \<noteq> get (x2\<lparr>tcb_reply := cap\<rparr>)))) \<and> (aa \<noteq> a \<longrightarrow> (\<exists>cap. (\<exists>sz fun. kheap s aa = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> fun b = Some cap) \<or> (\<exists>tcb. kheap s aa = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> cap = get tcb))) \<longrightarrow> (\<exists>cap. (\<exists>sz fun. well_formed_cnode_n sz fun \<and> kheap s aa = Some (CNode sz fun) \<and> fun b = Some cap) \<or> (\<exists>tcb. kheap s aa = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> cap = get tcb))))
 4. \<And>a x2 s aa b. \<lbrakk>ptr = (a, tcb_cnode_index 3); kheap s a = Some (TCB x2)\<rbrakk> \<Longrightarrow> (aa = a \<longrightarrow> ((\<exists>get set restr. tcb_cap_cases b = Some (get, set, restr)) \<longrightarrow> b \<noteq> tcb_cnode_index 3 \<longrightarrow> (THE cap. \<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> cap = get x2) = (THE capa. \<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> capa = get (x2\<lparr>tcb_caller := cap\<rparr>))) \<and> ((\<forall>cap get. (\<forall>set restr. tcb_cap_cases b \<noteq> Some (get, set, restr)) \<or> cap \<noteq> get x2) \<longrightarrow> b \<noteq> tcb_cnode_index 3 \<longrightarrow> (\<forall>capa get. (\<forall>set restr. tcb_cap_cases b \<noteq> Some (get, set, restr)) \<or> capa \<noteq> get (x2\<lparr>tcb_caller := cap\<rparr>)))) \<and> (aa \<noteq> a \<longrightarrow> (\<exists>cap. (\<exists>sz fun. kheap s aa = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> fun b = Some cap) \<or> (\<exists>tcb. kheap s aa = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> cap = get tcb))) \<longrightarrow> (\<exists>cap. (\<exists>sz fun. well_formed_cnode_n sz fun \<and> kheap s aa = Some (CNode sz fun) \<and> fun b = Some cap) \<or> (\<exists>tcb. kheap s aa = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> cap = get tcb))))
 5. \<And>a x2 s aa b. \<lbrakk>ptr = (a, tcb_cnode_index 4); kheap s a = Some (TCB x2)\<rbrakk> \<Longrightarrow> (aa = a \<longrightarrow> ((\<exists>get set restr. tcb_cap_cases b = Some (get, set, restr)) \<longrightarrow> b \<noteq> tcb_cnode_index 4 \<longrightarrow> (THE cap. \<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> cap = get x2) = (THE capa. \<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> capa = get (x2\<lparr>tcb_ipcframe := cap\<rparr>))) \<and> ((\<forall>cap get. (\<forall>set restr. tcb_cap_cases b \<noteq> Some (get, set, restr)) \<or> cap \<noteq> get x2) \<longrightarrow> b \<noteq> tcb_cnode_index 4 \<longrightarrow> (\<forall>capa get. (\<forall>set restr. tcb_cap_cases b \<noteq> Some (get, set, restr)) \<or> capa \<noteq> get (x2\<lparr>tcb_ipcframe := cap\<rparr>)))) \<and> (aa \<noteq> a \<longrightarrow> (\<exists>cap. (\<exists>sz fun. kheap s aa = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> fun b = Some cap) \<or> (\<exists>tcb. kheap s aa = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> cap = get tcb))) \<longrightarrow> (\<exists>cap. (\<exists>sz fun. well_formed_cnode_n sz fun \<and> kheap s aa = Some (CNode sz fun) \<and> fun b = Some cap) \<or> (\<exists>tcb. kheap s aa = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> cap = get tcb)))) proof (prove)
goal:
No subgoals!