theory CNodeInv_AI

lemma tcb_valid_nonspecial_cap:
  "\<lbrakk> caps_of_state s p = Some cap; valid_objs s;
       \<forall>ptr st. \<forall>(getF, setF, restr) \<in> ran tcb_cap_cases.
                    \<not> restr ptr st cap \<or> (\<forall>cap. restr ptr st cap);
       \<forall>ptr. (is_nondevice_page_cap cap \<or> cap = cap.NullCap) \<and>
             valid_ipc_buffer_cap cap ptr
                \<longrightarrow> valid_ipc_buffer_cap cap' ptr \<rbrakk>
      \<Longrightarrow> tcb_cap_valid cap' p s" apply (drule cte_wp_tcb_cap_valid[rotated]) apply (erule caps_of_state_cteD) apply (clarsimp simp: tcb_cap_valid_def st_tcb_def2) apply (clarsimp split: option.split_asm) apply (rule conjI) apply (drule spec, drule spec, drule bspec, erule ranI) apply fastforce apply (clarsimp simp: eq_commute) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>caps_of_state s p = Some cap; valid_objs s; \<forall>ptr st. \<forall>(getF, setF, restr)\<in>ran tcb_cap_cases. \<not> restr ptr st cap \<or> (\<forall>cap. restr ptr st cap); \<forall>ptr. (is_nondevice_page_cap cap \<or> cap = NullCap) \<and> valid_ipc_buffer_cap cap ptr \<longrightarrow> valid_ipc_buffer_cap cap' ptr\<rbrakk> \<Longrightarrow> tcb_cap_valid cap' p s proof (prove)
goal (2 subgoals):
 1. \<lbrakk>caps_of_state s p = Some cap; \<forall>ptr st. \<forall>(getF, setF, restr)\<in>ran tcb_cap_cases. \<not> restr ptr st cap \<or> (\<forall>cap. restr ptr st cap); \<forall>ptr. (is_nondevice_page_cap cap \<or> cap = NullCap) \<and> valid_ipc_buffer_cap cap ptr \<longrightarrow> valid_ipc_buffer_cap cap' ptr\<rbrakk> \<Longrightarrow> cte_wp_at ((=) ?c) ?p s
 2. \<lbrakk>caps_of_state s p = Some cap; \<forall>ptr st. \<forall>(getF, setF, restr)\<in>ran tcb_cap_cases. \<not> restr ptr st cap \<or> (\<forall>cap. restr ptr st cap); \<forall>ptr. (is_nondevice_page_cap cap \<or> cap = NullCap) \<and> valid_ipc_buffer_cap cap ptr \<longrightarrow> valid_ipc_buffer_cap cap' ptr; tcb_cap_valid ?c ?p s\<rbrakk> \<Longrightarrow> tcb_cap_valid cap' p s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>caps_of_state s p = Some cap; \<forall>ptr st. \<forall>(getF, setF, restr)\<in>ran tcb_cap_cases. \<not> restr ptr st cap \<or> (\<forall>cap. restr ptr st cap); \<forall>ptr. (is_nondevice_page_cap cap \<or> cap = NullCap) \<and> valid_ipc_buffer_cap cap ptr \<longrightarrow> valid_ipc_buffer_cap cap' ptr; tcb_cap_valid cap p s\<rbrakk> \<Longrightarrow> tcb_cap_valid cap' p s proof (prove)
goal (1 subgoal):
 1. \<And>tcb. \<lbrakk>caps_of_state s p = Some cap; \<forall>ptr st. \<forall>x\<in>ran tcb_cap_cases. case x of (getF, setF, restr) \<Rightarrow> restr ptr st cap \<longrightarrow> All (restr ptr st); \<forall>ptr. (is_nondevice_page_cap cap \<or> cap = NullCap) \<and> valid_ipc_buffer_cap cap ptr \<longrightarrow> valid_ipc_buffer_cap cap' ptr; tcb_at (fst p) s; snd p = tcb_cnode_index 4 \<longrightarrow> (\<forall>tcb. ko_at (TCB tcb) (fst p) s \<longrightarrow> valid_ipc_buffer_cap cap (tcb_ipc_buffer tcb)); get_tcb (fst p) s = Some tcb; case tcb_cap_cases (snd p) of None \<Rightarrow> True | Some (getF, setF, restr) \<Rightarrow> restr (fst p) (tcb_state tcb) cap\<rbrakk> \<Longrightarrow> (case tcb_cap_cases (snd p) of None \<Rightarrow> True | Some (getF, setF, restr) \<Rightarrow> restr (fst p) (tcb_state tcb) cap') \<and> (snd p = tcb_cnode_index 4 \<longrightarrow> (\<forall>tcb. ko_at (TCB tcb) (fst p) s \<longrightarrow> valid_ipc_buffer_cap cap' (tcb_ipc_buffer tcb))) proof (prove)
goal (1 subgoal):
 1. \<And>tcb a aa b. \<lbrakk>caps_of_state s p = Some cap; \<forall>ptr st. \<forall>x\<in>ran tcb_cap_cases. case x of (getF, setF, restr) \<Rightarrow> restr ptr st cap \<longrightarrow> All (restr ptr st); \<forall>ptr. (is_nondevice_page_cap cap \<or> cap = NullCap) \<and> valid_ipc_buffer_cap cap ptr \<longrightarrow> valid_ipc_buffer_cap cap' ptr; tcb_at (fst p) s; snd p = tcb_cnode_index 4 \<longrightarrow> (\<forall>tcb. ko_at (TCB tcb) (fst p) s \<longrightarrow> valid_ipc_buffer_cap cap (tcb_ipc_buffer tcb)); get_tcb (fst p) s = Some tcb; tcb_cap_cases (snd p) = Some (a, aa, b); b (fst p) (tcb_state tcb) cap\<rbrakk> \<Longrightarrow> b (fst p) (tcb_state tcb) cap' \<and> (snd p = tcb_cnode_index 4 \<longrightarrow> (\<forall>tcb. ko_at (TCB tcb) (fst p) s \<longrightarrow> valid_ipc_buffer_cap cap' (tcb_ipc_buffer tcb))) proof (prove)
goal (2 subgoals):
 1. \<And>tcb a aa b. \<lbrakk>caps_of_state s p = Some cap; \<forall>ptr st. \<forall>x\<in>ran tcb_cap_cases. case x of (getF, setF, restr) \<Rightarrow> restr ptr st cap \<longrightarrow> All (restr ptr st); \<forall>ptr. (is_nondevice_page_cap cap \<or> cap = NullCap) \<and> valid_ipc_buffer_cap cap ptr \<longrightarrow> valid_ipc_buffer_cap cap' ptr; tcb_at (fst p) s; snd p = tcb_cnode_index 4 \<longrightarrow> (\<forall>tcb. ko_at (TCB tcb) (fst p) s \<longrightarrow> valid_ipc_buffer_cap cap (tcb_ipc_buffer tcb)); get_tcb (fst p) s = Some tcb; tcb_cap_cases (snd p) = Some (a, aa, b); b (fst p) (tcb_state tcb) cap\<rbrakk> \<Longrightarrow> b (fst p) (tcb_state tcb) cap'
 2. \<And>tcb a aa b. \<lbrakk>caps_of_state s p = Some cap; \<forall>ptr st. \<forall>x\<in>ran tcb_cap_cases. case x of (getF, setF, restr) \<Rightarrow> restr ptr st cap \<longrightarrow> All (restr ptr st); \<forall>ptr. (is_nondevice_page_cap cap \<or> cap = NullCap) \<and> valid_ipc_buffer_cap cap ptr \<longrightarrow> valid_ipc_buffer_cap cap' ptr; tcb_at (fst p) s; snd p = tcb_cnode_index 4 \<longrightarrow> (\<forall>tcb. ko_at (TCB tcb) (fst p) s \<longrightarrow> valid_ipc_buffer_cap cap (tcb_ipc_buffer tcb)); get_tcb (fst p) s = Some tcb; tcb_cap_cases (snd p) = Some (a, aa, b); b (fst p) (tcb_state tcb) cap\<rbrakk> \<Longrightarrow> snd p = tcb_cnode_index 4 \<longrightarrow> (\<forall>tcb. ko_at (TCB tcb) (fst p) s \<longrightarrow> valid_ipc_buffer_cap cap' (tcb_ipc_buffer tcb)) proof (prove)
goal (2 subgoals):
 1. \<And>tcb a aa b. \<lbrakk>caps_of_state s p = Some cap; \<forall>ptr. (is_nondevice_page_cap cap \<or> cap = NullCap) \<and> valid_ipc_buffer_cap cap ptr \<longrightarrow> valid_ipc_buffer_cap cap' ptr; tcb_at (fst p) s; snd p = tcb_cnode_index 4 \<longrightarrow> (\<forall>tcb. ko_at (TCB tcb) (fst p) s \<longrightarrow> valid_ipc_buffer_cap cap (tcb_ipc_buffer tcb)); get_tcb (fst p) s = Some tcb; tcb_cap_cases (snd p) = Some (a, aa, b); b (fst p) (tcb_state tcb) cap; case (a, aa, b) of (getF, setF, restr) \<Rightarrow> restr (?ptr36 tcb a aa b) (?st38 tcb a aa b) cap \<longrightarrow> All (restr (?ptr36 tcb a aa b) (?st38 tcb a aa b))\<rbrakk> \<Longrightarrow> b (fst p) (tcb_state tcb) cap'
 2. \<And>tcb a aa b. \<lbrakk>caps_of_state s p = Some cap; \<forall>ptr st. \<forall>x\<in>ran tcb_cap_cases. case x of (getF, setF, restr) \<Rightarrow> restr ptr st cap \<longrightarrow> All (restr ptr st); \<forall>ptr. (is_nondevice_page_cap cap \<or> cap = NullCap) \<and> valid_ipc_buffer_cap cap ptr \<longrightarrow> valid_ipc_buffer_cap cap' ptr; tcb_at (fst p) s; snd p = tcb_cnode_index 4 \<longrightarrow> (\<forall>tcb. ko_at (TCB tcb) (fst p) s \<longrightarrow> valid_ipc_buffer_cap cap (tcb_ipc_buffer tcb)); get_tcb (fst p) s = Some tcb; tcb_cap_cases (snd p) = Some (a, aa, b); b (fst p) (tcb_state tcb) cap\<rbrakk> \<Longrightarrow> snd p = tcb_cnode_index 4 \<longrightarrow> (\<forall>tcb. ko_at (TCB tcb) (fst p) s \<longrightarrow> valid_ipc_buffer_cap cap' (tcb_ipc_buffer tcb)) proof (prove)
goal (1 subgoal):
 1. \<And>tcb a aa b. \<lbrakk>caps_of_state s p = Some cap; \<forall>ptr st. \<forall>x\<in>ran tcb_cap_cases. case x of (getF, setF, restr) \<Rightarrow> restr ptr st cap \<longrightarrow> All (restr ptr st); \<forall>ptr. (is_nondevice_page_cap cap \<or> cap = NullCap) \<and> valid_ipc_buffer_cap cap ptr \<longrightarrow> valid_ipc_buffer_cap cap' ptr; tcb_at (fst p) s; snd p = tcb_cnode_index 4 \<longrightarrow> (\<forall>tcb. ko_at (TCB tcb) (fst p) s \<longrightarrow> valid_ipc_buffer_cap cap (tcb_ipc_buffer tcb)); get_tcb (fst p) s = Some tcb; tcb_cap_cases (snd p) = Some (a, aa, b); b (fst p) (tcb_state tcb) cap\<rbrakk> \<Longrightarrow> snd p = tcb_cnode_index 4 \<longrightarrow> (\<forall>tcb. ko_at (TCB tcb) (fst p) s \<longrightarrow> valid_ipc_buffer_cap cap' (tcb_ipc_buffer tcb)) proof (prove)
goal:
No subgoals!