theory CNode_DR

lemma dcorres_get_object_cnode_split:
  assumes c: "\<And>cnode. dcorres r P (P' cnode) (a (cdl_object.CNode cnode)) c"
  shows   "dcorres r P
                    (\<lambda>s. (\<forall>sz cs. (get_cnode' ptr s = Some (sz,cs)) \<longrightarrow> P' (obj_cnode (transform_cnode sz cs)) s) \<and>
                         get_cnode' ptr s \<noteq> None \<and>
                         cnode_size_bits (the (kheap s ptr)) \<noteq> 0 \<and>
                         valid_idle s)
                    (KHeap_D.get_object ptr >>= a) c" apply (rule corres_guard_imp [where
         Q = "\<lambda>s. \<forall>obj. cdl_objects s ptr = Some (cdl_object.CNode obj) \<longrightarrow> P s" and
         Q' = "\<lambda>s. (\<forall>obj'. (get_cnode' ptr s = Some obj')\<longrightarrow> (P' (obj_cnode (transform_cnode (fst obj') (snd obj'))) s) ) \<and>
                    get_cnode' ptr s \<noteq> None \<and> cnode_size_bits (the (kheap s ptr)) \<noteq> 0 \<and> valid_idle s"]) apply (rule dcorres_get_object_special [where C = "Types_D.CNode" and UN_C = obj_cnode
           and AP = "\<lambda> ptr s. get_cnode' ptr s" and AP_LIFT = "\<lambda>cn _. obj_cnode (transform_cnode (fst cn) (snd cn))"
           and AP_Q = "\<lambda>s. cnode_size_bits (the (kheap s ptr)) \<noteq> 0 \<and> valid_idle s" and R="\<lambda>obj s. P s"]) apply simp apply (case_tac obj) apply clarsimp apply (drule (1) opt_object_cnode [OF _ get_cnode'D]) apply (simp add: transform_cnode_def) defer apply (rule c) apply simp_all apply (clarsimp split: nat.splits) apply (clarsimp simp: get_cnode'_def cnode_size_bits_def split:  option.splits kernel_object.split) apply (case_tac x2, simp_all) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. dcorres r P (\<lambda>s. (\<forall>sz cs. get_cnode' ptr s = Some (sz, cs) \<longrightarrow> P' (obj_cnode (transform_cnode sz cs)) s) \<and> get_cnode' ptr s \<noteq> None \<and> cnode_size_bits (the (kheap s ptr)) \<noteq> 0 \<and> valid_idle s) (KHeap_D.get_object ptr >>= a) c proof (prove)
goal (3 subgoals):
 1. dcorres r (\<lambda>s. \<forall>obj. cdl_objects s ptr = Some (cdl_object.CNode obj) \<longrightarrow> P s) (\<lambda>s. (\<forall>obj'. get_cnode' ptr s = Some obj' \<longrightarrow> P' (obj_cnode (transform_cnode (fst obj') (snd obj'))) s) \<and> get_cnode' ptr s \<noteq> None \<and> cnode_size_bits (the (kheap s ptr)) \<noteq> 0 \<and> valid_idle s) (KHeap_D.get_object ptr >>= a) c
 2. \<And>s. P s \<Longrightarrow> \<forall>obj. cdl_objects s ptr = Some (cdl_object.CNode obj) \<longrightarrow> P s
 3. \<And>s. (\<forall>sz cs. get_cnode' ptr s = Some (sz, cs) \<longrightarrow> P' (obj_cnode (transform_cnode sz cs)) s) \<and> get_cnode' ptr s \<noteq> None \<and> cnode_size_bits (the (kheap s ptr)) \<noteq> 0 \<and> valid_idle s \<Longrightarrow> (\<forall>obj'. get_cnode' ptr s = Some obj' \<longrightarrow> P' (obj_cnode (transform_cnode (fst obj') (snd obj'))) s) \<and> get_cnode' ptr s \<noteq> None \<and> cnode_size_bits (the (kheap s ptr)) \<noteq> 0 \<and> valid_idle s proof (prove)
goal (5 subgoals):
 1. \<And>obj. obj_cnode (cdl_object.CNode obj) = obj
 2. \<And>s obj. \<lbrakk>get_cnode' ptr s = Some obj; cnode_size_bits (the (kheap s ptr)) \<noteq> 0 \<and> valid_idle s\<rbrakk> \<Longrightarrow> cdl_objects (transform s) ptr = Some (cdl_object.CNode (obj_cnode (transform_cnode (fst obj) (snd obj))))
 3. \<And>obj. dcorres r P (P' obj) (a (cdl_object.CNode obj)) c
 4. \<And>s. P s \<Longrightarrow> \<forall>obj. cdl_objects s ptr = Some (cdl_object.CNode obj) \<longrightarrow> P s
 5. \<And>s. (\<forall>sz cs. get_cnode' ptr s = Some (sz, cs) \<longrightarrow> P' (obj_cnode (transform_cnode sz cs)) s) \<and> get_cnode' ptr s \<noteq> None \<and> cnode_size_bits (the (kheap s ptr)) \<noteq> 0 \<and> valid_idle s \<Longrightarrow> (\<forall>obj'. get_cnode' ptr s = Some obj' \<longrightarrow> P' (obj_cnode (transform_cnode (fst obj') (snd obj'))) s) \<and> get_cnode' ptr s \<noteq> None \<and> cnode_size_bits (the (kheap s ptr)) \<noteq> 0 \<and> valid_idle s proof (prove)
goal (4 subgoals):
 1. \<And>s obj. \<lbrakk>get_cnode' ptr s = Some obj; cnode_size_bits (the (kheap s ptr)) \<noteq> 0 \<and> valid_idle s\<rbrakk> \<Longrightarrow> cdl_objects (transform s) ptr = Some (cdl_object.CNode (obj_cnode (transform_cnode (fst obj) (snd obj))))
 2. \<And>obj. dcorres r P (P' obj) (a (cdl_object.CNode obj)) c
 3. \<And>s. P s \<Longrightarrow> \<forall>obj. cdl_objects s ptr = Some (cdl_object.CNode obj) \<longrightarrow> P s
 4. \<And>s. (\<forall>sz cs. get_cnode' ptr s = Some (sz, cs) \<longrightarrow> P' (obj_cnode (transform_cnode sz cs)) s) \<and> get_cnode' ptr s \<noteq> None \<and> cnode_size_bits (the (kheap s ptr)) \<noteq> 0 \<and> valid_idle s \<Longrightarrow> (\<forall>obj'. get_cnode' ptr s = Some obj' \<longrightarrow> P' (obj_cnode (transform_cnode (fst obj') (snd obj'))) s) \<and> get_cnode' ptr s \<noteq> None \<and> cnode_size_bits (the (kheap s ptr)) \<noteq> 0 \<and> valid_idle s proof (prove)
goal (4 subgoals):
 1. \<And>s obj a b. \<lbrakk>get_cnode' ptr s = Some obj; cnode_size_bits (the (kheap s ptr)) \<noteq> 0 \<and> valid_idle s; obj = (a, b)\<rbrakk> \<Longrightarrow> cdl_objects (transform s) ptr = Some (cdl_object.CNode (obj_cnode (transform_cnode (fst obj) (snd obj))))
 2. \<And>obj. dcorres r P (P' obj) (a (cdl_object.CNode obj)) c
 3. \<And>s. P s \<Longrightarrow> \<forall>obj. cdl_objects s ptr = Some (cdl_object.CNode obj) \<longrightarrow> P s
 4. \<And>s. (\<forall>sz cs. get_cnode' ptr s = Some (sz, cs) \<longrightarrow> P' (obj_cnode (transform_cnode sz cs)) s) \<and> get_cnode' ptr s \<noteq> None \<and> cnode_size_bits (the (kheap s ptr)) \<noteq> 0 \<and> valid_idle s \<Longrightarrow> (\<forall>obj'. get_cnode' ptr s = Some obj' \<longrightarrow> P' (obj_cnode (transform_cnode (fst obj') (snd obj'))) s) \<and> get_cnode' ptr s \<noteq> None \<and> cnode_size_bits (the (kheap s ptr)) \<noteq> 0 \<and> valid_idle s proof (prove)
goal (4 subgoals):
 1. \<And>s aa ba. \<lbrakk>get_cnode' ptr s = Some (aa, ba); 0 < cnode_size_bits (the (kheap s ptr)); valid_idle s\<rbrakk> \<Longrightarrow> cdl_objects (transform s) ptr = Some (cdl_object.CNode (obj_cnode (transform_cnode aa ba)))
 2. \<And>obj. dcorres r P (P' obj) (a (cdl_object.CNode obj)) c
 3. \<And>s. P s \<Longrightarrow> \<forall>obj. cdl_objects s ptr = Some (cdl_object.CNode obj) \<longrightarrow> P s
 4. \<And>s. (\<forall>sz cs. get_cnode' ptr s = Some (sz, cs) \<longrightarrow> P' (obj_cnode (transform_cnode sz cs)) s) \<and> get_cnode' ptr s \<noteq> None \<and> cnode_size_bits (the (kheap s ptr)) \<noteq> 0 \<and> valid_idle s \<Longrightarrow> (\<forall>obj'. get_cnode' ptr s = Some obj' \<longrightarrow> P' (obj_cnode (transform_cnode (fst obj') (snd obj'))) s) \<and> get_cnode' ptr s \<noteq> None \<and> cnode_size_bits (the (kheap s ptr)) \<noteq> 0 \<and> valid_idle s proof (prove)
goal (4 subgoals):
 1. \<And>s aa ba. \<lbrakk>get_cnode' ptr s = Some (aa, ba); 0 < cnode_size_bits (the (kheap s ptr)); cdl_objects (transform s) ptr = Some (transform_object (machine_state s) ptr (?opt_etcb16 s aa ba) (kernel_object.CNode aa ba))\<rbrakk> \<Longrightarrow> cdl_objects (transform s) ptr = Some (cdl_object.CNode (obj_cnode (transform_cnode aa ba)))
 2. \<And>obj. dcorres r P (P' obj) (a (cdl_object.CNode obj)) c
 3. \<And>s. P s \<Longrightarrow> \<forall>obj. cdl_objects s ptr = Some (cdl_object.CNode obj) \<longrightarrow> P s
 4. \<And>s. (\<forall>sz cs. get_cnode' ptr s = Some (sz, cs) \<longrightarrow> P' (obj_cnode (transform_cnode sz cs)) s) \<and> get_cnode' ptr s \<noteq> None \<and> cnode_size_bits (the (kheap s ptr)) \<noteq> 0 \<and> valid_idle s \<Longrightarrow> (\<forall>obj'. get_cnode' ptr s = Some obj' \<longrightarrow> P' (obj_cnode (transform_cnode (fst obj') (snd obj'))) s) \<and> get_cnode' ptr s \<noteq> None \<and> cnode_size_bits (the (kheap s ptr)) \<noteq> 0 \<and> valid_idle s proof (prove)
goal (4 subgoals):
 1. \<And>s aa ba. \<lbrakk>get_cnode' ptr s = Some (aa, ba); 0 < cnode_size_bits (the (kheap s ptr)); cdl_objects (transform s) ptr = Some (case aa of 0 \<Rightarrow> IRQNode \<lparr>cdl_irq_node_caps = transform_cnode_contents 0 ba\<rparr> | Suc nat \<Rightarrow> cdl_object.CNode \<lparr>cdl_cnode_caps = transform_cnode_contents (Suc nat) ba, cdl_cnode_size_bits = Suc nat\<rparr>)\<rbrakk> \<Longrightarrow> 0 < aa \<and> (0 < aa \<longrightarrow> (case aa of 0 \<Rightarrow> IRQNode \<lparr>cdl_irq_node_caps = transform_cnode_contents 0 ba\<rparr> | Suc nat \<Rightarrow> cdl_object.CNode \<lparr>cdl_cnode_caps = transform_cnode_contents (Suc nat) ba, cdl_cnode_size_bits = Suc nat\<rparr>) = cdl_object.CNode \<lparr>cdl_cnode_caps = transform_cnode_contents aa ba, cdl_cnode_size_bits = aa\<rparr>)
 2. \<And>obj. dcorres r P (P' obj) (a (cdl_object.CNode obj)) c
 3. \<And>s. P s \<Longrightarrow> \<forall>obj. cdl_objects s ptr = Some (cdl_object.CNode obj) \<longrightarrow> P s
 4. \<And>s. (\<forall>sz cs. get_cnode' ptr s = Some (sz, cs) \<longrightarrow> P' (obj_cnode (transform_cnode sz cs)) s) \<and> get_cnode' ptr s \<noteq> None \<and> cnode_size_bits (the (kheap s ptr)) \<noteq> 0 \<and> valid_idle s \<Longrightarrow> (\<forall>obj'. get_cnode' ptr s = Some obj' \<longrightarrow> P' (obj_cnode (transform_cnode (fst obj') (snd obj'))) s) \<and> get_cnode' ptr s \<noteq> None \<and> cnode_size_bits (the (kheap s ptr)) \<noteq> 0 \<and> valid_idle s proof (prove)
goal (4 subgoals):
 1. \<And>obj. dcorres r P (P' obj) (a (cdl_object.CNode obj)) c
 2. \<And>s. P s \<Longrightarrow> \<forall>obj. cdl_objects s ptr = Some (cdl_object.CNode obj) \<longrightarrow> P s
 3. \<And>s. (\<forall>sz cs. get_cnode' ptr s = Some (sz, cs) \<longrightarrow> P' (obj_cnode (transform_cnode sz cs)) s) \<and> get_cnode' ptr s \<noteq> None \<and> cnode_size_bits (the (kheap s ptr)) \<noteq> 0 \<and> valid_idle s \<Longrightarrow> (\<forall>obj'. get_cnode' ptr s = Some obj' \<longrightarrow> P' (obj_cnode (transform_cnode (fst obj') (snd obj'))) s) \<and> get_cnode' ptr s \<noteq> None \<and> cnode_size_bits (the (kheap s ptr)) \<noteq> 0 \<and> valid_idle s
 4. \<And>s aa ba. \<lbrakk>get_cnode' ptr s = Some (aa, ba); 0 < cnode_size_bits (the (kheap s ptr)); cdl_objects (transform s) ptr = Some (case aa of 0 \<Rightarrow> IRQNode \<lparr>cdl_irq_node_caps = transform_cnode_contents 0 ba\<rparr> | Suc nat \<Rightarrow> cdl_object.CNode \<lparr>cdl_cnode_caps = transform_cnode_contents (Suc nat) ba, cdl_cnode_size_bits = Suc nat\<rparr>)\<rbrakk> \<Longrightarrow> 0 < aa \<and> (0 < aa \<longrightarrow> (case aa of 0 \<Rightarrow> IRQNode \<lparr>cdl_irq_node_caps = transform_cnode_contents 0 ba\<rparr> | Suc nat \<Rightarrow> cdl_object.CNode \<lparr>cdl_cnode_caps = transform_cnode_contents (Suc nat) ba, cdl_cnode_size_bits = Suc nat\<rparr>) = cdl_object.CNode \<lparr>cdl_cnode_caps = transform_cnode_contents aa ba, cdl_cnode_size_bits = aa\<rparr>) proof (prove)
goal (3 subgoals):
 1. \<And>s. P s \<Longrightarrow> \<forall>obj. cdl_objects s ptr = Some (cdl_object.CNode obj) \<longrightarrow> P s
 2. \<And>s. (\<forall>sz cs. get_cnode' ptr s = Some (sz, cs) \<longrightarrow> P' (obj_cnode (transform_cnode sz cs)) s) \<and> get_cnode' ptr s \<noteq> None \<and> cnode_size_bits (the (kheap s ptr)) \<noteq> 0 \<and> valid_idle s \<Longrightarrow> (\<forall>obj'. get_cnode' ptr s = Some obj' \<longrightarrow> P' (obj_cnode (transform_cnode (fst obj') (snd obj'))) s) \<and> get_cnode' ptr s \<noteq> None \<and> cnode_size_bits (the (kheap s ptr)) \<noteq> 0 \<and> valid_idle s
 3. \<And>s aa ba. \<lbrakk>get_cnode' ptr s = Some (aa, ba); 0 < cnode_size_bits (the (kheap s ptr)); cdl_objects (transform s) ptr = Some (case aa of 0 \<Rightarrow> IRQNode \<lparr>cdl_irq_node_caps = transform_cnode_contents 0 ba\<rparr> | Suc nat \<Rightarrow> cdl_object.CNode \<lparr>cdl_cnode_caps = transform_cnode_contents (Suc nat) ba, cdl_cnode_size_bits = Suc nat\<rparr>)\<rbrakk> \<Longrightarrow> 0 < aa \<and> (0 < aa \<longrightarrow> (case aa of 0 \<Rightarrow> IRQNode \<lparr>cdl_irq_node_caps = transform_cnode_contents 0 ba\<rparr> | Suc nat \<Rightarrow> cdl_object.CNode \<lparr>cdl_cnode_caps = transform_cnode_contents (Suc nat) ba, cdl_cnode_size_bits = Suc nat\<rparr>) = cdl_object.CNode \<lparr>cdl_cnode_caps = transform_cnode_contents aa ba, cdl_cnode_size_bits = aa\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s aa ba. \<lbrakk>get_cnode' ptr s = Some (aa, ba); 0 < cnode_size_bits (the (kheap s ptr)); cdl_objects (transform s) ptr = Some (case aa of 0 \<Rightarrow> IRQNode \<lparr>cdl_irq_node_caps = transform_cnode_contents 0 ba\<rparr> | Suc nat \<Rightarrow> cdl_object.CNode \<lparr>cdl_cnode_caps = transform_cnode_contents (Suc nat) ba, cdl_cnode_size_bits = Suc nat\<rparr>)\<rbrakk> \<Longrightarrow> 0 < aa \<and> (0 < aa \<longrightarrow> (case aa of 0 \<Rightarrow> IRQNode \<lparr>cdl_irq_node_caps = transform_cnode_contents 0 ba\<rparr> | Suc nat \<Rightarrow> cdl_object.CNode \<lparr>cdl_cnode_caps = transform_cnode_contents (Suc nat) ba, cdl_cnode_size_bits = Suc nat\<rparr>) = cdl_object.CNode \<lparr>cdl_cnode_caps = transform_cnode_contents aa ba, cdl_cnode_size_bits = aa\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s ba. \<lbrakk>get_cnode' ptr s = Some (0, ba); 0 < cnode_size_bits (the (kheap s ptr)); cdl_objects (transform s) ptr = Some (IRQNode \<lparr>cdl_irq_node_caps = transform_cnode_contents 0 ba\<rparr>)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>s ba x2. \<lbrakk>0 < (case x2 of kernel_object.CNode sz cs \<Rightarrow> sz | _ \<Rightarrow> 0); cdl_objects (transform s) ptr = Some (IRQNode \<lparr>cdl_irq_node_caps = transform_cnode_contents 0 ba\<rparr>); kheap s ptr = Some x2; (case x2 of kernel_object.CNode sz cn \<Rightarrow> Some (sz, cn) | _ \<Rightarrow> None) = Some (0, ba)\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!