theory Finalise_DR

lemma caps_of_state_transform_opt_cap_no_idle:
  "\<lbrakk>caps_of_state s p = Some cap; valid_etcbs s\<rbrakk>
   \<Longrightarrow> opt_cap (transform_cslot_ptr p) (transform s)
          = Some (transform_cap cap) \<or>
      opt_cap (transform_cslot_ptr p) (transform s)
          = None" apply (frule caps_of_state_cteD) apply (cases p) apply (erule cte_wp_atE) apply (clarsimp simp: opt_cap_def transform_cslot_ptr_def object_slots_def
                         slots_of_def transform_def transform_objects_def
                         transform_cnode_contents_def well_formed_cnode_n_def
                         restrict_map_def
                   split: option.splits if_split_asm nat.splits) apply (frule(1) eqset_imp_iff[THEN iffD1, OF _ domI]) apply (simp add: nat_to_bl_zero_zero option_map_join_def) apply clarsimp apply (frule(1) eqset_imp_iff[THEN iffD1, OF _ domI]) apply (simp add: option_map_join_def nat_to_bl_dest) apply (clarsimp simp: cap_installed_at_irq_def valid_irq_node_def
                         obj_at_def is_cap_table_def well_formed_cnode_n_def
                         length_set_helper word_bl.Abs_inverse
                         object_slots_def nat_bl_to_bin_lt2p) apply (frule(1) valid_etcbs_tcb_etcb) by (clarsimp simp: opt_cap_def transform_cslot_ptr_def
                        slots_of_def restrict_map_def
                        transform_def object_slots_def transform_objects_def
                        valid_irq_node_def obj_at_def is_cap_table_def tcb_cap_cases_def
                        transform_tcb_def tcb_slot_defs infer_tcb_bound_notification_def
                        bl_to_bin_tcb_cnode_index bl_to_bin_tcb_cnode_index_le0
                 split: if_split_asm option.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>caps_of_state s p = Some cap; valid_etcbs s\<rbrakk> \<Longrightarrow> opt_cap (transform_cslot_ptr p) (transform s) = Some (transform_cap cap) \<or> opt_cap (transform_cslot_ptr p) (transform s) = None proof (prove)
goal (1 subgoal):
 1. \<lbrakk>caps_of_state s p = Some cap; valid_etcbs s; cte_wp_at ((=) cap) p s\<rbrakk> \<Longrightarrow> opt_cap (transform_cslot_ptr p) (transform s) = Some (transform_cap cap) \<or> opt_cap (transform_cslot_ptr p) (transform s) = None proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>caps_of_state s p = Some cap; valid_etcbs s; cte_wp_at ((=) cap) p s; p = (a, b)\<rbrakk> \<Longrightarrow> opt_cap (transform_cslot_ptr p) (transform s) = Some (transform_cap cap) \<or> opt_cap (transform_cslot_ptr p) (transform s) = None proof (prove)
goal (2 subgoals):
 1. \<And>a b sz fun cte. \<lbrakk>caps_of_state s p = Some cap; valid_etcbs s; p = (a, b); kheap s (fst p) = Some (kernel_object.CNode sz fun); well_formed_cnode_n sz fun; fun (snd p) = Some cte; cap = cte\<rbrakk> \<Longrightarrow> opt_cap (transform_cslot_ptr p) (transform s) = Some (transform_cap cap) \<or> opt_cap (transform_cslot_ptr p) (transform s) = None
 2. \<And>a b tcb getF setF restr. \<lbrakk>caps_of_state s p = Some cap; valid_etcbs s; p = (a, b); kheap s (fst p) = Some (TCB tcb); tcb_cap_cases (snd p) = Some (getF, setF, restr); cap = getF tcb\<rbrakk> \<Longrightarrow> opt_cap (transform_cslot_ptr p) (transform s) = Some (transform_cap cap) \<or> opt_cap (transform_cslot_ptr p) (transform s) = None proof (prove)
goal (3 subgoals):
 1. \<And>a b fun z. \<lbrakk>caps_of_state s (a, b) = Some cap; valid_etcbs s; p = (a, b); kheap s a = Some (kernel_object.CNode 0 fun); dom fun = {[]}; fun b = Some cap; a \<noteq> idle_thread s; option_map_join fun (nat_to_bl 0 (nat (bl_to_bin b))) = Some z\<rbrakk> \<Longrightarrow> transform_cap z = transform_cap cap
 2. \<And>a b sz fun x2 y x2a. \<lbrakk>(case x2 of Tcb x \<Rightarrow> cdl_tcb_caps x | cdl_object.CNode x \<Rightarrow> cdl_cnode_caps x | AsidPool x \<Rightarrow> cdl_asid_pool_caps x | cdl_object.PageTable x \<Rightarrow> cdl_page_table_caps x | cdl_object.PageDirectory x \<Rightarrow> cdl_page_directory_caps x | IRQNode x \<Rightarrow> cdl_irq_node_caps x | _ \<Rightarrow> \<lambda>x. None) (nat (bl_to_bin b)) = Some y; caps_of_state s (a, b) = Some cap; valid_etcbs s; p = (a, b); kheap s a = Some (kernel_object.CNode (Suc x2a) fun); dom fun = {x. length x = Suc x2a}; fun b = Some cap; a \<noteq> idle_thread s; sz = Suc x2a; cdl_object.CNode \<lparr>cdl_cnode_caps = \<lambda>n. map_option transform_cap (option_map_join fun (nat_to_bl (Suc x2a) n)), cdl_cnode_size_bits = Suc x2a\<rparr> = x2\<rbrakk> \<Longrightarrow> y = transform_cap cap
 3. \<And>a b tcb getF setF restr. \<lbrakk>caps_of_state s p = Some cap; valid_etcbs s; p = (a, b); kheap s (fst p) = Some (TCB tcb); tcb_cap_cases (snd p) = Some (getF, setF, restr); cap = getF tcb\<rbrakk> \<Longrightarrow> opt_cap (transform_cslot_ptr p) (transform s) = Some (transform_cap cap) \<or> opt_cap (transform_cslot_ptr p) (transform s) = None proof (prove)
goal (3 subgoals):
 1. \<And>a b fun z. \<lbrakk>caps_of_state s (a, b) = Some cap; valid_etcbs s; p = (a, b); kheap s a = Some (kernel_object.CNode 0 fun); dom fun = {[]}; fun b = Some cap; a \<noteq> idle_thread s; option_map_join fun (nat_to_bl 0 (nat (bl_to_bin b))) = Some z; b \<in> {[]}\<rbrakk> \<Longrightarrow> transform_cap z = transform_cap cap
 2. \<And>a b sz fun x2 y x2a. \<lbrakk>(case x2 of Tcb x \<Rightarrow> cdl_tcb_caps x | cdl_object.CNode x \<Rightarrow> cdl_cnode_caps x | AsidPool x \<Rightarrow> cdl_asid_pool_caps x | cdl_object.PageTable x \<Rightarrow> cdl_page_table_caps x | cdl_object.PageDirectory x \<Rightarrow> cdl_page_directory_caps x | IRQNode x \<Rightarrow> cdl_irq_node_caps x | _ \<Rightarrow> \<lambda>x. None) (nat (bl_to_bin b)) = Some y; caps_of_state s (a, b) = Some cap; valid_etcbs s; p = (a, b); kheap s a = Some (kernel_object.CNode (Suc x2a) fun); dom fun = {x. length x = Suc x2a}; fun b = Some cap; a \<noteq> idle_thread s; sz = Suc x2a; cdl_object.CNode \<lparr>cdl_cnode_caps = \<lambda>n. map_option transform_cap (option_map_join fun (nat_to_bl (Suc x2a) n)), cdl_cnode_size_bits = Suc x2a\<rparr> = x2\<rbrakk> \<Longrightarrow> y = transform_cap cap
 3. \<And>a b tcb getF setF restr. \<lbrakk>caps_of_state s p = Some cap; valid_etcbs s; p = (a, b); kheap s (fst p) = Some (TCB tcb); tcb_cap_cases (snd p) = Some (getF, setF, restr); cap = getF tcb\<rbrakk> \<Longrightarrow> opt_cap (transform_cslot_ptr p) (transform s) = Some (transform_cap cap) \<or> opt_cap (transform_cslot_ptr p) (transform s) = None proof (prove)
goal (2 subgoals):
 1. \<And>a b sz fun x2 y x2a. \<lbrakk>(case x2 of Tcb x \<Rightarrow> cdl_tcb_caps x | cdl_object.CNode x \<Rightarrow> cdl_cnode_caps x | AsidPool x \<Rightarrow> cdl_asid_pool_caps x | cdl_object.PageTable x \<Rightarrow> cdl_page_table_caps x | cdl_object.PageDirectory x \<Rightarrow> cdl_page_directory_caps x | IRQNode x \<Rightarrow> cdl_irq_node_caps x | _ \<Rightarrow> \<lambda>x. None) (nat (bl_to_bin b)) = Some y; caps_of_state s (a, b) = Some cap; valid_etcbs s; p = (a, b); kheap s a = Some (kernel_object.CNode (Suc x2a) fun); dom fun = {x. length x = Suc x2a}; fun b = Some cap; a \<noteq> idle_thread s; sz = Suc x2a; cdl_object.CNode \<lparr>cdl_cnode_caps = \<lambda>n. map_option transform_cap (option_map_join fun (nat_to_bl (Suc x2a) n)), cdl_cnode_size_bits = Suc x2a\<rparr> = x2\<rbrakk> \<Longrightarrow> y = transform_cap cap
 2. \<And>a b tcb getF setF restr. \<lbrakk>caps_of_state s p = Some cap; valid_etcbs s; p = (a, b); kheap s (fst p) = Some (TCB tcb); tcb_cap_cases (snd p) = Some (getF, setF, restr); cap = getF tcb\<rbrakk> \<Longrightarrow> opt_cap (transform_cslot_ptr p) (transform s) = Some (transform_cap cap) \<or> opt_cap (transform_cslot_ptr p) (transform s) = None proof (prove)
goal (2 subgoals):
 1. \<And>a b fun x2a z. \<lbrakk>caps_of_state s (a, b) = Some cap; valid_etcbs s; p = (a, b); kheap s a = Some (kernel_object.CNode (Suc x2a) fun); dom fun = {x. length x = Suc x2a}; fun b = Some cap; a \<noteq> idle_thread s; option_map_join fun (nat_to_bl (Suc x2a) (nat (bl_to_bin b))) = Some z\<rbrakk> \<Longrightarrow> transform_cap z = transform_cap cap
 2. \<And>a b tcb getF setF restr. \<lbrakk>caps_of_state s p = Some cap; valid_etcbs s; p = (a, b); kheap s (fst p) = Some (TCB tcb); tcb_cap_cases (snd p) = Some (getF, setF, restr); cap = getF tcb\<rbrakk> \<Longrightarrow> opt_cap (transform_cslot_ptr p) (transform s) = Some (transform_cap cap) \<or> opt_cap (transform_cslot_ptr p) (transform s) = None proof (prove)
goal (2 subgoals):
 1. \<And>a b fun x2a z. \<lbrakk>caps_of_state s (a, b) = Some cap; valid_etcbs s; p = (a, b); kheap s a = Some (kernel_object.CNode (Suc x2a) fun); dom fun = {x. length x = Suc x2a}; fun b = Some cap; a \<noteq> idle_thread s; option_map_join fun (nat_to_bl (Suc x2a) (nat (bl_to_bin b))) = Some z; b \<in> {x. length x = Suc x2a}\<rbrakk> \<Longrightarrow> transform_cap z = transform_cap cap
 2. \<And>a b tcb getF setF restr. \<lbrakk>caps_of_state s p = Some cap; valid_etcbs s; p = (a, b); kheap s (fst p) = Some (TCB tcb); tcb_cap_cases (snd p) = Some (getF, setF, restr); cap = getF tcb\<rbrakk> \<Longrightarrow> opt_cap (transform_cslot_ptr p) (transform s) = Some (transform_cap cap) \<or> opt_cap (transform_cslot_ptr p) (transform s) = None proof (prove)
goal (1 subgoal):
 1. \<And>a b tcb getF setF restr. \<lbrakk>caps_of_state s p = Some cap; valid_etcbs s; p = (a, b); kheap s (fst p) = Some (TCB tcb); tcb_cap_cases (snd p) = Some (getF, setF, restr); cap = getF tcb\<rbrakk> \<Longrightarrow> opt_cap (transform_cslot_ptr p) (transform s) = Some (transform_cap cap) \<or> opt_cap (transform_cslot_ptr p) (transform s) = None proof (prove)
goal (1 subgoal):
 1. \<And>a b tcb getF setF restr y. \<lbrakk>caps_of_state s (a, b) = Some (getF tcb); valid_etcbs s; p = (a, b); kheap s a = Some (TCB tcb); tcb_cap_cases b = Some (getF, setF, restr); cap = getF tcb; opt_cap (transform_cslot_ptr (a, b)) (transform s) = Some y\<rbrakk> \<Longrightarrow> y = transform_cap (getF tcb) proof (prove)
goal (1 subgoal):
 1. \<And>a b tcb getF setF restr y. \<lbrakk>caps_of_state s (a, b) = Some (getF tcb); valid_etcbs s; p = (a, b); kheap s a = Some (TCB tcb); tcb_cap_cases b = Some (getF, setF, restr); cap = getF tcb; opt_cap (transform_cslot_ptr (a, b)) (transform s) = Some y; \<exists>etcb. ekheap s a = Some etcb\<rbrakk> \<Longrightarrow> y = transform_cap (getF tcb)