theory CNode_DR

lemma update_cap_rights_transform [simp]:
  "update_cap_rights (Types_D.cap_rights (transform_cap cap) \<inter> R) (transform_cap cap) =
  update_cap_rights (Structures_A.cap_rights cap \<inter> R) (transform_cap cap)" apply (simp add: update_cap_rights_def transform_cap_def) apply (auto simp: Types_D.cap_rights_def split: cap.splits arch_cap.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. update_cap_rights (Types_D.cap_rights (transform_cap cap) \<inter> R) (transform_cap cap) = update_cap_rights (Structures_A.cap_rights cap \<inter> R) (transform_cap cap) proof (prove)
goal (1 subgoal):
 1. (case case cap of cap.NullCap \<Rightarrow> cdl_cap.NullCap | cap.UntypedCap dev ptr size_bits idx \<Rightarrow> cdl_cap.UntypedCap dev {ptr..ptr + 2 ^ size_bits - 1} (free_range_of_untyped idx size_bits ptr) | cap.EndpointCap x xa xb \<Rightarrow> cdl_cap.EndpointCap x xa xb | cap.NotificationCap x xa xb \<Rightarrow> cdl_cap.NotificationCap x xa xb | cap.ReplyCap ptr is_master cap_rights_ \<Rightarrow> if is_master then MasterReplyCap ptr else cdl_cap.ReplyCap ptr cap_rights_ | cap.CNodeCap ptr size_bits guard \<Rightarrow> cdl_cap.CNodeCap ptr (of_bl guard) (length guard) size_bits | ThreadCap x \<Rightarrow> TcbCap x | cap.DomainCap \<Rightarrow> cdl_cap.DomainCap | IRQControlCap \<Rightarrow> IrqControlCap | IRQHandlerCap x \<Rightarrow> IrqHandlerCap x | Zombie ptr x xa \<Rightarrow> ZombieCap ptr | ArchObjectCap (ASIDPoolCap ptr asid) \<Rightarrow> AsidPoolCap ptr (fst $ transform_asid asid) | ArchObjectCap ASIDControlCap \<Rightarrow> AsidControlCap | ArchObjectCap (PageCap dev ptr cap_rights_ sz mp) \<Rightarrow> FrameCap dev ptr cap_rights_ (pageBitsForSize sz) Real (transform_mapping mp) | ArchObjectCap (arch_cap.PageTableCap ptr mp) \<Rightarrow> cdl_cap.PageTableCap ptr Real (transform_mapping mp) | ArchObjectCap (arch_cap.PageDirectoryCap ptr mp) \<Rightarrow> cdl_cap.PageDirectoryCap ptr Real (map_option transform_asid mp) of cdl_cap.EndpointCap f1 f2 x \<Rightarrow> cdl_cap.EndpointCap f1 f2 (Types_D.cap_rights (case cap of cap.NullCap \<Rightarrow> cdl_cap.NullCap | cap.UntypedCap dev ptr size_bits idx \<Rightarrow> cdl_cap.UntypedCap dev {ptr..ptr + 2 ^ size_bits - 1} (free_range_of_untyped idx size_bits ptr) | cap.EndpointCap x xa xb \<Rightarrow> cdl_cap.EndpointCap x xa xb | cap.NotificationCap x xa xb \<Rightarrow> cdl_cap.NotificationCap x xa xb | cap.ReplyCap ptr is_master cap_rights_ \<Rightarrow> if is_master then MasterReplyCap ptr else cdl_cap.ReplyCap ptr cap_rights_ | cap.CNodeCap ptr size_bits guard \<Rightarrow> cdl_cap.CNodeCap ptr (of_bl guard) (length guard) size_bits | ThreadCap x \<Rightarrow> TcbCap x | cap.DomainCap \<Rightarrow> cdl_cap.DomainCap | IRQControlCap \<Rightarrow> IrqControlCap | IRQHandlerCap x \<Rightarrow> IrqHandlerCap x | Zombie ptr x xa \<Rightarrow> ZombieCap ptr | ArchObjectCap (ASIDPoolCap ptr asid) \<Rightarrow> AsidPoolCap ptr (fst $ transform_asid asid) | ArchObjectCap ASIDControlCap \<Rightarrow> AsidControlCap | ArchObjectCap (PageCap dev ptr cap_rights_ sz mp) \<Rightarrow> FrameCap dev ptr cap_rights_ (pageBitsForSize sz) Real (transform_mapping mp) | ArchObjectCap (arch_cap.PageTableCap ptr mp) \<Rightarrow> cdl_cap.PageTableCap ptr Real (transform_mapping mp) | ArchObjectCap (arch_cap.PageDirectoryCap ptr mp) \<Rightarrow> cdl_cap.PageDirectoryCap ptr Real (map_option transform_asid mp)) \<inter> R) | cdl_cap.NotificationCap f1 f2 x \<Rightarrow> cdl_cap.NotificationCap f1 f2 (Types_D.cap_rights (case cap of cap.NullCap \<Rightarrow> cdl_cap.NullCap | cap.UntypedCap dev ptr size_bits idx \<Rightarrow> cdl_cap.UntypedCap dev {ptr..ptr + 2 ^ size_bits - 1} (free_range_of_untyped idx size_bits ptr) | cap.EndpointCap x xa xb \<Rightarrow> cdl_cap.EndpointCap x xa xb | cap.NotificationCap x xa xb \<Rightarrow> cdl_cap.NotificationCap x xa xb | cap.ReplyCap ptr is_master cap_rights_ \<Rightarrow> if is_master then MasterReplyCap ptr else cdl_cap.ReplyCap ptr cap_rights_ | cap.CNodeCap ptr size_bits guard \<Rightarrow> cdl_cap.CNodeCap ptr (of_bl guard) (length guard) size_bits | ThreadCap x \<Rightarrow> TcbCap x | cap.DomainCap \<Rightarrow> cdl_cap.DomainCap | IRQControlCap \<Rightarrow> IrqControlCap | IRQHandlerCap x \<Rightarrow> IrqHandlerCap x | Zombie ptr x xa \<Rightarrow> ZombieCap ptr | ArchObjectCap (ASIDPoolCap ptr asid) \<Rightarrow> AsidPoolCap ptr (fst $ transform_asid asid) | ArchObjectCap ASIDControlCap \<Rightarrow> AsidControlCap | ArchObjectCap (PageCap dev ptr cap_rights_ sz mp) \<Rightarrow> FrameCap dev ptr cap_rights_ (pageBitsForSize sz) Real (transform_mapping mp) | ArchObjectCap (arch_cap.PageTableCap ptr mp) \<Rightarrow> cdl_cap.PageTableCap ptr Real (transform_mapping mp) | ArchObjectCap (arch_cap.PageDirectoryCap ptr mp) \<Rightarrow> cdl_cap.PageDirectoryCap ptr Real (map_option transform_asid mp)) \<inter> R - {AllowGrant, AllowGrantReply}) | cdl_cap.ReplyCap f1 x \<Rightarrow> cdl_cap.ReplyCap f1 (Types_D.cap_rights (case cap of cap.NullCap \<Rightarrow> cdl_cap.NullCap | cap.UntypedCap dev ptr size_bits idx \<Rightarrow> cdl_cap.UntypedCap dev {ptr..ptr + 2 ^ size_bits - 1} (free_range_of_untyped idx size_bits ptr) | cap.EndpointCap x xa xb \<Rightarrow> cdl_cap.EndpointCap x xa xb | cap.NotificationCap x xa xb \<Rightarrow> cdl_cap.NotificationCap x xa xb | cap.ReplyCap ptr is_master cap_rights_ \<Rightarrow> if is_master then MasterReplyCap ptr else cdl_cap.ReplyCap ptr cap_rights_ | cap.CNodeCap ptr size_bits guard \<Rightarrow> cdl_cap.CNodeCap ptr (of_bl guard) (length guard) size_bits | ThreadCap x \<Rightarrow> TcbCap x | cap.DomainCap \<Rightarrow> cdl_cap.DomainCap | IRQControlCap \<Rightarrow> IrqControlCap | IRQHandlerCap x \<Rightarrow> IrqHandlerCap x | Zombie ptr x xa \<Rightarrow> ZombieCap ptr | ArchObjectCap (ASIDPoolCap ptr asid) \<Rightarrow> AsidPoolCap ptr (fst $ transform_asid asid) | ArchObjectCap ASIDControlCap \<Rightarrow> AsidControlCap | ArchObjectCap (PageCap dev ptr cap_rights_ sz mp) \<Rightarrow> FrameCap dev ptr cap_rights_ (pageBitsForSize sz) Real (transform_mapping mp) | ArchObjectCap (arch_cap.PageTableCap ptr mp) \<Rightarrow> cdl_cap.PageTableCap ptr Real (transform_mapping mp) | ArchObjectCap (arch_cap.PageDirectoryCap ptr mp) \<Rightarrow> cdl_cap.PageDirectoryCap ptr Real (map_option transform_asid mp)) \<inter> R - {AllowRead, AllowGrantReply} \<union> {AllowWrite}) | FrameCap dev f1 x f2 f3 f4 \<Rightarrow> FrameCap dev f1 (validate_vm_rights (Types_D.cap_rights (case cap of cap.NullCap \<Rightarrow> cdl_cap.NullCap | cap.UntypedCap dev ptr size_bits idx \<Rightarrow> cdl_cap.UntypedCap dev {ptr..ptr + 2 ^ size_bits - 1} (free_range_of_untyped idx size_bits ptr) | cap.EndpointCap x xa xb \<Rightarrow> cdl_cap.EndpointCap x xa xb | cap.NotificationCap x xa xb \<Rightarrow> cdl_cap.NotificationCap x xa xb | cap.ReplyCap ptr is_master cap_rights_ \<Rightarrow> if is_master then MasterReplyCap ptr else cdl_cap.ReplyCap ptr cap_rights_ | cap.CNodeCap ptr size_bits guard \<Rightarrow> cdl_cap.CNodeCap ptr (of_bl guard) (length guard) size_bits | ThreadCap x \<Rightarrow> TcbCap x | cap.DomainCap \<Rightarrow> cdl_cap.DomainCap | IRQControlCap \<Rightarrow> IrqControlCap | IRQHandlerCap x \<Rightarrow> IrqHandlerCap x | Zombie ptr x xa \<Rightarrow> ZombieCap ptr | ArchObjectCap (ASIDPoolCap ptr asid) \<Rightarrow> AsidPoolCap ptr (fst $ transform_asid asid) | ArchObjectCap ASIDControlCap \<Rightarrow> AsidControlCap | ArchObjectCap (PageCap dev ptr cap_rights_ sz mp) \<Rightarrow> FrameCap dev ptr cap_rights_ (pageBitsForSize sz) Real (transform_mapping mp) | ArchObjectCap (arch_cap.PageTableCap ptr mp) \<Rightarrow> cdl_cap.PageTableCap ptr Real (transform_mapping mp) | ArchObjectCap (arch_cap.PageDirectoryCap ptr mp) \<Rightarrow> cdl_cap.PageDirectoryCap ptr Real (map_option transform_asid mp)) \<inter> R)) f2 f3 f4 | _ \<Rightarrow> case cap of cap.NullCap \<Rightarrow> cdl_cap.NullCap | cap.UntypedCap dev ptr size_bits idx \<Rightarrow> cdl_cap.UntypedCap dev {ptr..ptr + 2 ^ size_bits - 1} (free_range_of_untyped idx size_bits ptr) | cap.EndpointCap x xa xb \<Rightarrow> cdl_cap.EndpointCap x xa xb | cap.NotificationCap x xa xb \<Rightarrow> cdl_cap.NotificationCap x xa xb | cap.ReplyCap ptr is_master cap_rights_ \<Rightarrow> if is_master then MasterReplyCap ptr else cdl_cap.ReplyCap ptr cap_rights_ | cap.CNodeCap ptr size_bits guard \<Rightarrow> cdl_cap.CNodeCap ptr (of_bl guard) (length guard) size_bits | ThreadCap x \<Rightarrow> TcbCap x | cap.DomainCap \<Rightarrow> cdl_cap.DomainCap | IRQControlCap \<Rightarrow> IrqControlCap | IRQHandlerCap x \<Rightarrow> IrqHandlerCap x | Zombie ptr x xa \<Rightarrow> ZombieCap ptr | ArchObjectCap (ASIDPoolCap ptr asid) \<Rightarrow> AsidPoolCap ptr (fst $ transform_asid asid) | ArchObjectCap ASIDControlCap \<Rightarrow> AsidControlCap | ArchObjectCap (PageCap dev ptr cap_rights_ sz mp) \<Rightarrow> FrameCap dev ptr cap_rights_ (pageBitsForSize sz) Real (transform_mapping mp) | ArchObjectCap (arch_cap.PageTableCap ptr mp) \<Rightarrow> cdl_cap.PageTableCap ptr Real (transform_mapping mp) | ArchObjectCap (arch_cap.PageDirectoryCap ptr mp) \<Rightarrow> cdl_cap.PageDirectoryCap ptr Real (map_option transform_asid mp)) = (case case cap of cap.NullCap \<Rightarrow> cdl_cap.NullCap | cap.UntypedCap dev ptr size_bits idx \<Rightarrow> cdl_cap.UntypedCap dev {ptr..ptr + 2 ^ size_bits - 1} (free_range_of_untyped idx size_bits ptr) | cap.EndpointCap x xa xb \<Rightarrow> cdl_cap.EndpointCap x xa xb | cap.NotificationCap x xa xb \<Rightarrow> cdl_cap.NotificationCap x xa xb | cap.ReplyCap ptr is_master cap_rights_ \<Rightarrow> if is_master then MasterReplyCap ptr else cdl_cap.ReplyCap ptr cap_rights_ | cap.CNodeCap ptr size_bits guard \<Rightarrow> cdl_cap.CNodeCap ptr (of_bl guard) (length guard) size_bits | ThreadCap x \<Rightarrow> TcbCap x | cap.DomainCap \<Rightarrow> cdl_cap.DomainCap | IRQControlCap \<Rightarrow> IrqControlCap | IRQHandlerCap x \<Rightarrow> IrqHandlerCap x | Zombie ptr x xa \<Rightarrow> ZombieCap ptr | ArchObjectCap (ASIDPoolCap ptr asid) \<Rightarrow> AsidPoolCap ptr (fst $ transform_asid asid) | ArchObjectCap ASIDControlCap \<Rightarrow> AsidControlCap | ArchObjectCap (PageCap dev ptr cap_rights_ sz mp) \<Rightarrow> FrameCap dev ptr cap_rights_ (pageBitsForSize sz) Real (transform_mapping mp) | ArchObjectCap (arch_cap.PageTableCap ptr mp) \<Rightarrow> cdl_cap.PageTableCap ptr Real (transform_mapping mp) | ArchObjectCap (arch_cap.PageDirectoryCap ptr mp) \<Rightarrow> cdl_cap.PageDirectoryCap ptr Real (map_option transform_asid mp) of cdl_cap.EndpointCap f1 f2 x \<Rightarrow> cdl_cap.EndpointCap f1 f2 (Structures_A.cap_rights cap \<inter> R) | cdl_cap.NotificationCap f1 f2 x \<Rightarrow> cdl_cap.NotificationCap f1 f2 (Structures_A.cap_rights cap \<inter> R - {AllowGrant, AllowGrantReply}) | cdl_cap.ReplyCap f1 x \<Rightarrow> cdl_cap.ReplyCap f1 (Structures_A.cap_rights cap \<inter> R - {AllowRead, AllowGrantReply} \<union> {AllowWrite}) | FrameCap dev f1 x f2 f3 f4 \<Rightarrow> FrameCap dev f1 (validate_vm_rights (Structures_A.cap_rights cap \<inter> R)) f2 f3 f4 | _ \<Rightarrow> case cap of cap.NullCap \<Rightarrow> cdl_cap.NullCap | cap.UntypedCap dev ptr size_bits idx \<Rightarrow> cdl_cap.UntypedCap dev {ptr..ptr + 2 ^ size_bits - 1} (free_range_of_untyped idx size_bits ptr) | cap.EndpointCap x xa xb \<Rightarrow> cdl_cap.EndpointCap x xa xb | cap.NotificationCap x xa xb \<Rightarrow> cdl_cap.NotificationCap x xa xb | cap.ReplyCap ptr is_master cap_rights_ \<Rightarrow> if is_master then MasterReplyCap ptr else cdl_cap.ReplyCap ptr cap_rights_ | cap.CNodeCap ptr size_bits guard \<Rightarrow> cdl_cap.CNodeCap ptr (of_bl guard) (length guard) size_bits | ThreadCap x \<Rightarrow> TcbCap x | cap.DomainCap \<Rightarrow> cdl_cap.DomainCap | IRQControlCap \<Rightarrow> IrqControlCap | IRQHandlerCap x \<Rightarrow> IrqHandlerCap x | Zombie ptr x xa \<Rightarrow> ZombieCap ptr | ArchObjectCap (ASIDPoolCap ptr asid) \<Rightarrow> AsidPoolCap ptr (fst $ transform_asid asid) | ArchObjectCap ASIDControlCap \<Rightarrow> AsidControlCap | ArchObjectCap (PageCap dev ptr cap_rights_ sz mp) \<Rightarrow> FrameCap dev ptr cap_rights_ (pageBitsForSize sz) Real (transform_mapping mp) | ArchObjectCap (arch_cap.PageTableCap ptr mp) \<Rightarrow> cdl_cap.PageTableCap ptr Real (transform_mapping mp) | ArchObjectCap (arch_cap.PageDirectoryCap ptr mp) \<Rightarrow> cdl_cap.PageDirectoryCap ptr Real (map_option transform_asid mp)) proof (prove)
goal:
No subgoals!