theory ArchCNodeInv_AI

lemma copy_of_cap_range [CNodeInv_AI_assms]:
  "copy_of cap cap' \<Longrightarrow> cap_range cap = cap_range cap'" apply (clarsimp simp: copy_of_def split: if_split_asm) apply (cases cap', simp_all add: same_object_as_def) apply (clarsimp simp: is_cap_simps bits_of_def cap_range_def
                      split: cap.split_asm)+ apply (rename_tac acap' acap) apply (case_tac acap, simp_all) apply (clarsimp split: arch_cap.split_asm cap.split_asm)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. copy_of cap cap' \<Longrightarrow> cap_range cap = cap_range cap' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> is_untyped_cap cap'; same_object_as cap' cap; is_reply_cap cap' = is_reply_cap cap; is_master_reply_cap cap' = is_master_reply_cap cap\<rbrakk> \<Longrightarrow> cap_range cap = cap_range cap' proof (prove)
goal (7 subgoals):
 1. \<And>x32 x33. \<lbrakk>is_ep_cap cap; is_reply_cap (EndpointCap (obj_ref_of cap) x32 x33) = is_reply_cap cap; is_master_reply_cap (EndpointCap (obj_ref_of cap) x32 x33) = is_master_reply_cap cap; cap' = EndpointCap (obj_ref_of cap) x32 x33\<rbrakk> \<Longrightarrow> cap_range cap = cap_range (EndpointCap (obj_ref_of cap) x32 x33)
 2. \<And>x42 x43. \<lbrakk>is_ntfn_cap cap; is_reply_cap (NotificationCap (obj_ref_of cap) x42 x43) = is_reply_cap cap; is_master_reply_cap (NotificationCap (obj_ref_of cap) x42 x43) = is_master_reply_cap cap; cap' = NotificationCap (obj_ref_of cap) x42 x43\<rbrakk> \<Longrightarrow> cap_range cap = cap_range (NotificationCap (obj_ref_of cap) x42 x43)
 3. \<And>x51 x52 x53. \<lbrakk>\<exists>m' cr. cap = ReplyCap x51 m' cr; is_reply_cap (ReplyCap x51 x52 x53) = is_reply_cap cap; is_master_reply_cap (ReplyCap x51 x52 x53) = is_master_reply_cap cap; cap' = ReplyCap x51 x52 x53\<rbrakk> \<Longrightarrow> cap_range cap = cap_range (ReplyCap x51 x52 x53)
 4. \<And>x63. \<lbrakk>is_cnode_cap cap; is_reply_cap (CNodeCap (obj_ref_of cap) (bits_of cap) x63) = is_reply_cap cap; is_master_reply_cap (CNodeCap (obj_ref_of cap) (bits_of cap) x63) = is_master_reply_cap cap; cap' = CNodeCap (obj_ref_of cap) (bits_of cap) x63\<rbrakk> \<Longrightarrow> cap_range cap = cap_range (CNodeCap (obj_ref_of cap) (bits_of cap) x63)
 5. \<lbrakk>is_thread_cap cap; is_reply_cap (ThreadCap (obj_ref_of cap)) = is_reply_cap cap; is_master_reply_cap (ThreadCap (obj_ref_of cap)) = is_master_reply_cap cap; cap' = ThreadCap (obj_ref_of cap)\<rbrakk> \<Longrightarrow> cap_range cap = cap_range (ThreadCap (obj_ref_of cap))
 6. \<lbrakk>case cap of IRQHandlerCap n \<Rightarrow> False | _ \<Rightarrow> same_region_as IRQControlCap cap; is_reply_cap IRQControlCap = is_reply_cap cap; is_master_reply_cap IRQControlCap = is_master_reply_cap cap; cap' = IRQControlCap\<rbrakk> \<Longrightarrow> cap_range cap = cap_range IRQControlCap
 7. \<And>x12. \<lbrakk>case cap of ArchObjectCap x \<Rightarrow> same_aobject_as x12 x | _ \<Rightarrow> same_region_as (ArchObjectCap x12) cap; is_reply_cap (ArchObjectCap x12) = is_reply_cap cap; is_master_reply_cap (ArchObjectCap x12) = is_master_reply_cap cap; cap' = ArchObjectCap x12\<rbrakk> \<Longrightarrow> cap_range cap = cap_range (ArchObjectCap x12) proof (prove)
goal (1 subgoal):
 1. \<And>x12 x12a. \<lbrakk>cap' = ArchObjectCap x12; cap = ArchObjectCap x12a; case x12 of PageCap dev ref x pgsz xa \<Rightarrow> case x12a of PageCap dev' ref' xb pgsz' xc \<Rightarrow> (dev, ref, pgsz) = (dev', ref', pgsz') \<and> ref \<le> ref + 2 ^ pageBitsForSize pgsz - 1 | _ \<Rightarrow> arch_same_region_as x12 x12a | _ \<Rightarrow> arch_same_region_as x12 x12a\<rbrakk> \<Longrightarrow> set_option (aobj_ref x12a) = set_option (aobj_ref x12) proof (prove)
goal (1 subgoal):
 1. \<And>acap' acap. \<lbrakk>cap' = ArchObjectCap acap'; cap = ArchObjectCap acap; case acap' of PageCap dev ref x pgsz xa \<Rightarrow> case acap of PageCap dev' ref' xb pgsz' xc \<Rightarrow> (dev, ref, pgsz) = (dev', ref', pgsz') \<and> ref \<le> ref + 2 ^ pageBitsForSize pgsz - 1 | _ \<Rightarrow> arch_same_region_as acap' acap | _ \<Rightarrow> arch_same_region_as acap' acap\<rbrakk> \<Longrightarrow> set_option (aobj_ref acap) = set_option (aobj_ref acap') proof (prove)
goal (5 subgoals):
 1. \<And>acap' acap x11 x12. \<lbrakk>cap' = ArchObjectCap acap'; cap = ArchObjectCap (ASIDPoolCap x11 x12); case acap' of PageCap dev ref x pgsz xa \<Rightarrow> case acap of PageCap dev' ref' xb pgsz' xc \<Rightarrow> (dev, ref, pgsz) = (dev', ref', pgsz') \<and> ref \<le> ref + 2 ^ pageBitsForSize pgsz - 1 | _ \<Rightarrow> arch_same_region_as acap' acap | _ \<Rightarrow> arch_same_region_as acap' acap; acap = ASIDPoolCap x11 x12\<rbrakk> \<Longrightarrow> {x11} = set_option (aobj_ref acap')
 2. \<And>acap' acap. \<lbrakk>cap' = ArchObjectCap acap'; cap = ArchObjectCap ASIDControlCap; case acap' of PageCap dev ref x pgsz xa \<Rightarrow> case acap of PageCap dev' ref' xb pgsz' xc \<Rightarrow> (dev, ref, pgsz) = (dev', ref', pgsz') \<and> ref \<le> ref + 2 ^ pageBitsForSize pgsz - 1 | _ \<Rightarrow> arch_same_region_as acap' acap | _ \<Rightarrow> arch_same_region_as acap' acap; acap = ASIDControlCap\<rbrakk> \<Longrightarrow> {} = set_option (aobj_ref acap')
 3. \<And>acap' acap x31 x32 x33 x34 x35. \<lbrakk>cap' = ArchObjectCap acap'; cap = ArchObjectCap (PageCap x31 x32 x33 x34 x35); case acap' of PageCap dev ref x pgsz xa \<Rightarrow> case acap of PageCap dev' ref' xb pgsz' xc \<Rightarrow> (dev, ref, pgsz) = (dev', ref', pgsz') \<and> ref \<le> ref + 2 ^ pageBitsForSize pgsz - 1 | _ \<Rightarrow> arch_same_region_as acap' acap | _ \<Rightarrow> arch_same_region_as acap' acap; acap = PageCap x31 x32 x33 x34 x35\<rbrakk> \<Longrightarrow> {x32} = set_option (aobj_ref acap')
 4. \<And>acap' acap x41 x42. \<lbrakk>cap' = ArchObjectCap acap'; cap = ArchObjectCap (PageTableCap x41 x42); case acap' of PageCap dev ref x pgsz xa \<Rightarrow> case acap of PageCap dev' ref' xb pgsz' xc \<Rightarrow> (dev, ref, pgsz) = (dev', ref', pgsz') \<and> ref \<le> ref + 2 ^ pageBitsForSize pgsz - 1 | _ \<Rightarrow> arch_same_region_as acap' acap | _ \<Rightarrow> arch_same_region_as acap' acap; acap = PageTableCap x41 x42\<rbrakk> \<Longrightarrow> {x41} = set_option (aobj_ref acap')
 5. \<And>acap' acap x51 x52. \<lbrakk>cap' = ArchObjectCap acap'; cap = ArchObjectCap (PageDirectoryCap x51 x52); case acap' of PageCap dev ref x pgsz xa \<Rightarrow> case acap of PageCap dev' ref' xb pgsz' xc \<Rightarrow> (dev, ref, pgsz) = (dev', ref', pgsz') \<and> ref \<le> ref + 2 ^ pageBitsForSize pgsz - 1 | _ \<Rightarrow> arch_same_region_as acap' acap | _ \<Rightarrow> arch_same_region_as acap' acap; acap = PageDirectoryCap x51 x52\<rbrakk> \<Longrightarrow> {x51} = set_option (aobj_ref acap') proof (prove)
goal:
No subgoals!