theory CNode_DR

lemma dcorres_update_cap_data:
  "cap = transform_cap cap' \<Longrightarrow>
   dcorres (\<lambda>c c'. c = transform_cap c') \<top>
    (valid_idle and valid_cap cap')
  (CSpace_D.update_cap_data preserve data cap)
  (return (CSpace_A.update_cap_data preserve data cap'))" apply (unfold CSpace_D.update_cap_data_def) apply (simp add:gets_the_def gets_def bind_assoc) apply (case_tac cap') apply (simp_all add:transform_cap_def update_cap_data_def is_cap_simps Let_def) apply (simp add: CSpace_D.badge_update_def update_cap_badge_def
                      Structures_A.badge_update_def Types_D.badge_bits_def) apply (simp add: CSpace_D.badge_update_def update_cap_badge_def
                     Structures_A.badge_update_def Types_D.badge_bits_def) apply (simp add:  bind_assoc gets_the_def gets_def the_cnode_cap_def) apply (clarsimp simp:word_bits_def dest!:leI) apply (simp add:of_drop_to_bl) apply (simp add:mask_twice) apply (clarsimp simp:word_size word_bits_def) apply (rename_tac arch_cap) apply (case_tac arch_cap, simp_all add: arch_update_cap_data_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cap = transform_cap cap' \<Longrightarrow> dcorres (\<lambda>c c'. c = transform_cap c') (\<lambda>_. True) (valid_idle and valid_cap cap') (CSpace_D.update_cap_data preserve data cap) (return (CSpace_A.update_cap_data preserve data cap')) proof (prove)
goal (1 subgoal):
 1. cap = transform_cap cap' \<Longrightarrow> dcorres (\<lambda>c c'. c = transform_cap c') (\<lambda>_. True) (valid_idle and valid_cap cap') (return $ case cap of cdl_cap.EndpointCap x b xa \<Rightarrow> if b = 0 \<and> \<not> preserve then CSpace_D.badge_update data cap else cdl_cap.NullCap | cdl_cap.NotificationCap x b xa \<Rightarrow> if b = 0 \<and> \<not> preserve then CSpace_D.badge_update data cap else cdl_cap.NullCap | cdl_cap.CNodeCap object guard guard_size sz \<Rightarrow> let reserved_bits = 3; guard_bits = 18; guard_size_bits = 5; new_guard_size = unat ((data >> reserved_bits) && mask guard_size_bits); new_guard = (data >> reserved_bits + guard_size_bits) && mask (min (unat ((data >> reserved_bits) && mask guard_size_bits)) guard_bits) in if word_bits < new_guard_size + sz then cdl_cap.NullCap else cdl_cap.CNodeCap object new_guard new_guard_size sz | _ \<Rightarrow> cap) (return (CSpace_A.update_cap_data preserve data cap')) proof (prove)
goal (1 subgoal):
 1. cap = transform_cap cap' \<Longrightarrow> (\<exists>s'. valid_idle s' \<and> s' \<turnstile> cap') \<longrightarrow> (case transform_cap cap' of cdl_cap.EndpointCap x b xa \<Rightarrow> if b = 0 \<and> \<not> preserve then CSpace_D.badge_update data cap else cdl_cap.NullCap | cdl_cap.NotificationCap x b xa \<Rightarrow> if b = 0 \<and> \<not> preserve then CSpace_D.badge_update data cap else cdl_cap.NullCap | cdl_cap.CNodeCap object guard guard_size sz \<Rightarrow> let reserved_bits = 3; guard_bits = 18; guard_size_bits = 5; new_guard_size = unat ((data >> reserved_bits) && mask guard_size_bits); new_guard = (data >> reserved_bits + guard_size_bits) && mask (min (unat ((data >> reserved_bits) && mask guard_size_bits)) guard_bits) in if word_bits < new_guard_size + sz then cdl_cap.NullCap else cdl_cap.CNodeCap object new_guard new_guard_size sz | _ \<Rightarrow> cap) = transform_cap (CSpace_A.update_cap_data preserve data cap') proof (prove)
goal (12 subgoals):
 1. \<lbrakk>cap = transform_cap cap'; cap' = cap.NullCap\<rbrakk> \<Longrightarrow> (\<exists>s'. valid_idle s' \<and> s' \<turnstile> cap') \<longrightarrow> (case transform_cap cap' of cdl_cap.EndpointCap x b xa \<Rightarrow> if b = 0 \<and> \<not> preserve then CSpace_D.badge_update data cap else cdl_cap.NullCap | cdl_cap.NotificationCap x b xa \<Rightarrow> if b = 0 \<and> \<not> preserve then CSpace_D.badge_update data cap else cdl_cap.NullCap | cdl_cap.CNodeCap object guard guard_size sz \<Rightarrow> let reserved_bits = 3; guard_bits = 18; guard_size_bits = 5; new_guard_size = unat ((data >> reserved_bits) && mask guard_size_bits); new_guard = (data >> reserved_bits + guard_size_bits) && mask (min (unat ((data >> reserved_bits) && mask guard_size_bits)) guard_bits) in if word_bits < new_guard_size + sz then cdl_cap.NullCap else cdl_cap.CNodeCap object new_guard new_guard_size sz | _ \<Rightarrow> cap) = transform_cap (CSpace_A.update_cap_data preserve data cap')
 2. \<And>x21 x22 x23 x24. \<lbrakk>cap = transform_cap cap'; cap' = cap.UntypedCap x21 x22 x23 x24\<rbrakk> \<Longrightarrow> (\<exists>s'. valid_idle s' \<and> s' \<turnstile> cap') \<longrightarrow> (case transform_cap cap' of cdl_cap.EndpointCap x b xa \<Rightarrow> if b = 0 \<and> \<not> preserve then CSpace_D.badge_update data cap else cdl_cap.NullCap | cdl_cap.NotificationCap x b xa \<Rightarrow> if b = 0 \<and> \<not> preserve then CSpace_D.badge_update data cap else cdl_cap.NullCap | cdl_cap.CNodeCap object guard guard_size sz \<Rightarrow> let reserved_bits = 3; guard_bits = 18; guard_size_bits = 5; new_guard_size = unat ((data >> reserved_bits) && mask guard_size_bits); new_guard = (data >> reserved_bits + guard_size_bits) && mask (min (unat ((data >> reserved_bits) && mask guard_size_bits)) guard_bits) in if word_bits < new_guard_size + sz then cdl_cap.NullCap else cdl_cap.CNodeCap object new_guard new_guard_size sz | _ \<Rightarrow> cap) = transform_cap (CSpace_A.update_cap_data preserve data cap')
 3. \<And>x31 x32 x33. \<lbrakk>cap = transform_cap cap'; cap' = cap.EndpointCap x31 x32 x33\<rbrakk> \<Longrightarrow> (\<exists>s'. valid_idle s' \<and> s' \<turnstile> cap') \<longrightarrow> (case transform_cap cap' of cdl_cap.EndpointCap x b xa \<Rightarrow> if b = 0 \<and> \<not> preserve then CSpace_D.badge_update data cap else cdl_cap.NullCap | cdl_cap.NotificationCap x b xa \<Rightarrow> if b = 0 \<and> \<not> preserve then CSpace_D.badge_update data cap else cdl_cap.NullCap | cdl_cap.CNodeCap object guard guard_size sz \<Rightarrow> let reserved_bits = 3; guard_bits = 18; guard_size_bits = 5; new_guard_size = unat ((data >> reserved_bits) && mask guard_size_bits); new_guard = (data >> reserved_bits + guard_size_bits) && mask (min (unat ((data >> reserved_bits) && mask guard_size_bits)) guard_bits) in if word_bits < new_guard_size + sz then cdl_cap.NullCap else cdl_cap.CNodeCap object new_guard new_guard_size sz | _ \<Rightarrow> cap) = transform_cap (CSpace_A.update_cap_data preserve data cap')
 4. \<And>x41 x42 x43. \<lbrakk>cap = transform_cap cap'; cap' = cap.NotificationCap x41 x42 x43\<rbrakk> \<Longrightarrow> (\<exists>s'. valid_idle s' \<and> s' \<turnstile> cap') \<longrightarrow> (case transform_cap cap' of cdl_cap.EndpointCap x b xa \<Rightarrow> if b = 0 \<and> \<not> preserve then CSpace_D.badge_update data cap else cdl_cap.NullCap | cdl_cap.NotificationCap x b xa \<Rightarrow> if b = 0 \<and> \<not> preserve then CSpace_D.badge_update data cap else cdl_cap.NullCap | cdl_cap.CNodeCap object guard guard_size sz \<Rightarrow> let reserved_bits = 3; guard_bits = 18; guard_size_bits = 5; new_guard_size = unat ((data >> reserved_bits) && mask guard_size_bits); new_guard = (data >> reserved_bits + guard_size_bits) && mask (min (unat ((data >> reserved_bits) && mask guard_size_bits)) guard_bits) in if word_bits < new_guard_size + sz then cdl_cap.NullCap else cdl_cap.CNodeCap object new_guard new_guard_size sz | _ \<Rightarrow> cap) = transform_cap (CSpace_A.update_cap_data preserve data cap')
 5. \<And>x51 x52 x53. \<lbrakk>cap = transform_cap cap'; cap' = cap.ReplyCap x51 x52 x53\<rbrakk> \<Longrightarrow> (\<exists>s'. valid_idle s' \<and> s' \<turnstile> cap') \<longrightarrow> (case transform_cap cap' of cdl_cap.EndpointCap x b xa \<Rightarrow> if b = 0 \<and> \<not> preserve then CSpace_D.badge_update data cap else cdl_cap.NullCap | cdl_cap.NotificationCap x b xa \<Rightarrow> if b = 0 \<and> \<not> preserve then CSpace_D.badge_update data cap else cdl_cap.NullCap | cdl_cap.CNodeCap object guard guard_size sz \<Rightarrow> let reserved_bits = 3; guard_bits = 18; guard_size_bits = 5; new_guard_size = unat ((data >> reserved_bits) && mask guard_size_bits); new_guard = (data >> reserved_bits + guard_size_bits) && mask (min (unat ((data >> reserved_bits) && mask guard_size_bits)) guard_bits) in if word_bits < new_guard_size + sz then cdl_cap.NullCap else cdl_cap.CNodeCap object new_guard new_guard_size sz | _ \<Rightarrow> cap) = transform_cap (CSpace_A.update_cap_data preserve data cap')
 6. \<And>x61 x62 x63. \<lbrakk>cap = transform_cap cap'; cap' = cap.CNodeCap x61 x62 x63\<rbrakk> \<Longrightarrow> (\<exists>s'. valid_idle s' \<and> s' \<turnstile> cap') \<longrightarrow> (case transform_cap cap' of cdl_cap.EndpointCap x b xa \<Rightarrow> if b = 0 \<and> \<not> preserve then CSpace_D.badge_update data cap else cdl_cap.NullCap | cdl_cap.NotificationCap x b xa \<Rightarrow> if b = 0 \<and> \<not> preserve then CSpace_D.badge_update data cap else cdl_cap.NullCap | cdl_cap.CNodeCap object guard guard_size sz \<Rightarrow> let reserved_bits = 3; guard_bits = 18; guard_size_bits = 5; new_guard_size = unat ((data >> reserved_bits) && mask guard_size_bits); new_guard = (data >> reserved_bits + guard_size_bits) && mask (min (unat ((data >> reserved_bits) && mask guard_size_bits)) guard_bits) in if word_bits < new_guard_size + sz then cdl_cap.NullCap else cdl_cap.CNodeCap object new_guard new_guard_size sz | _ \<Rightarrow> cap) = transform_cap (CSpace_A.update_cap_data preserve data cap')
 7. \<And>x7. \<lbrakk>cap = transform_cap cap'; cap' = ThreadCap x7\<rbrakk> \<Longrightarrow> (\<exists>s'. valid_idle s' \<and> s' \<turnstile> cap') \<longrightarrow> (case transform_cap cap' of cdl_cap.EndpointCap x b xa \<Rightarrow> if b = 0 \<and> \<not> preserve then CSpace_D.badge_update data cap else cdl_cap.NullCap | cdl_cap.NotificationCap x b xa \<Rightarrow> if b = 0 \<and> \<not> preserve then CSpace_D.badge_update data cap else cdl_cap.NullCap | cdl_cap.CNodeCap object guard guard_size sz \<Rightarrow> let reserved_bits = 3; guard_bits = 18; guard_size_bits = 5; new_guard_size = unat ((data >> reserved_bits) && mask guard_size_bits); new_guard = (data >> reserved_bits + guard_size_bits) && mask (min (unat ((data >> reserved_bits) && mask guard_size_bits)) guard_bits) in if word_bits < new_guard_size + sz then cdl_cap.NullCap else cdl_cap.CNodeCap object new_guard new_guard_size sz | _ \<Rightarrow> cap) = transform_cap (CSpace_A.update_cap_data preserve data cap')
 8. \<lbrakk>cap = transform_cap cap'; cap' = cap.DomainCap\<rbrakk> \<Longrightarrow> (\<exists>s'. valid_idle s' \<and> s' \<turnstile> cap') \<longrightarrow> (case transform_cap cap' of cdl_cap.EndpointCap x b xa \<Rightarrow> if b = 0 \<and> \<not> preserve then CSpace_D.badge_update data cap else cdl_cap.NullCap | cdl_cap.NotificationCap x b xa \<Rightarrow> if b = 0 \<and> \<not> preserve then CSpace_D.badge_update data cap else cdl_cap.NullCap | cdl_cap.CNodeCap object guard guard_size sz \<Rightarrow> let reserved_bits = 3; guard_bits = 18; guard_size_bits = 5; new_guard_size = unat ((data >> reserved_bits) && mask guard_size_bits); new_guard = (data >> reserved_bits + guard_size_bits) && mask (min (unat ((data >> reserved_bits) && mask guard_size_bits)) guard_bits) in if word_bits < new_guard_size + sz then cdl_cap.NullCap else cdl_cap.CNodeCap object new_guard new_guard_size sz | _ \<Rightarrow> cap) = transform_cap (CSpace_A.update_cap_data preserve data cap')
 9. \<lbrakk>cap = transform_cap cap'; cap' = IRQControlCap\<rbrakk> \<Longrightarrow> (\<exists>s'. valid_idle s' \<and> s' \<turnstile> cap') \<longrightarrow> (case transform_cap cap' of cdl_cap.EndpointCap x b xa \<Rightarrow> if b = 0 \<and> \<not> preserve then CSpace_D.badge_update data cap else cdl_cap.NullCap | cdl_cap.NotificationCap x b xa \<Rightarrow> if b = 0 \<and> \<not> preserve then CSpace_D.badge_update data cap else cdl_cap.NullCap | cdl_cap.CNodeCap object guard guard_size sz \<Rightarrow> let reserved_bits = 3; guard_bits = 18; guard_size_bits = 5; new_guard_size = unat ((data >> reserved_bits) && mask guard_size_bits); new_guard = (data >> reserved_bits + guard_size_bits) && mask (min (unat ((data >> reserved_bits) && mask guard_size_bits)) guard_bits) in if word_bits < new_guard_size + sz then cdl_cap.NullCap else cdl_cap.CNodeCap object new_guard new_guard_size sz | _ \<Rightarrow> cap) = transform_cap (CSpace_A.update_cap_data preserve data cap')
 10. \<And>x10. \<lbrakk>cap = transform_cap cap'; cap' = IRQHandlerCap x10\<rbrakk> \<Longrightarrow> (\<exists>s'. valid_idle s' \<and> s' \<turnstile> cap') \<longrightarrow> (case transform_cap cap' of cdl_cap.EndpointCap x b xa \<Rightarrow> if b = 0 \<and> \<not> preserve then CSpace_D.badge_update data cap else cdl_cap.NullCap | cdl_cap.NotificationCap x b xa \<Rightarrow> if b = 0 \<and> \<not> preserve then CSpace_D.badge_update data cap else cdl_cap.NullCap | cdl_cap.CNodeCap object guard guard_size sz \<Rightarrow> let reserved_bits = 3; guard_bits = 18; guard_size_bits = 5; new_guard_size = unat ((data >> reserved_bits) && mask guard_size_bits); new_guard = (data >> reserved_bits + guard_size_bits) && mask (min (unat ((data >> reserved_bits) && mask guard_size_bits)) guard_bits) in if word_bits < new_guard_size + sz then cdl_cap.NullCap else cdl_cap.CNodeCap object new_guard new_guard_size sz | _ \<Rightarrow> cap) = transform_cap (CSpace_A.update_cap_data preserve data cap')
A total of 12 subgoals... proof (prove)
goal (4 subgoals):
 1. \<And>x31 x32 x33. \<lbrakk>cap = cdl_cap.EndpointCap x31 x32 x33; cap' = cap.EndpointCap x31 x32 x33\<rbrakk> \<Longrightarrow> (x32 = 0 \<and> \<not> preserve \<longrightarrow> (\<exists>s'. valid_idle s' \<and> s' \<turnstile> cap.EndpointCap x31 0 x33) \<longrightarrow> CSpace_D.badge_update data (cdl_cap.EndpointCap x31 0 x33) = (case Structures_A.badge_update data (cap.EndpointCap x31 0 x33) 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))) \<and> ((x32 = 0 \<longrightarrow> preserve) \<longrightarrow> x32 = 0 \<and> \<not> preserve \<longrightarrow> (\<exists>s'. valid_idle s' \<and> s' \<turnstile> cap.EndpointCap x31 0 x33) \<longrightarrow> CSpace_D.badge_update data (cdl_cap.EndpointCap x31 0 x33) = (case Structures_A.badge_update data (cap.EndpointCap x31 0 x33) 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)))
 2. \<And>x41 x42 x43. \<lbrakk>cap = cdl_cap.NotificationCap x41 x42 x43; cap' = cap.NotificationCap x41 x42 x43\<rbrakk> \<Longrightarrow> (x42 = 0 \<and> \<not> preserve \<longrightarrow> (\<exists>s'. valid_idle s' \<and> s' \<turnstile> cap.NotificationCap x41 0 x43) \<longrightarrow> CSpace_D.badge_update data (cdl_cap.NotificationCap x41 0 x43) = (case Structures_A.badge_update data (cap.NotificationCap x41 0 x43) 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))) \<and> ((x42 = 0 \<longrightarrow> preserve) \<longrightarrow> x42 = 0 \<and> \<not> preserve \<longrightarrow> (\<exists>s'. valid_idle s' \<and> s' \<turnstile> cap.NotificationCap x41 0 x43) \<longrightarrow> CSpace_D.badge_update data (cdl_cap.NotificationCap x41 0 x43) = (case Structures_A.badge_update data (cap.NotificationCap x41 0 x43) 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)))
 3. \<And>x61 x62 x63. \<lbrakk>cap = cdl_cap.CNodeCap x61 (of_bl x63) (length x63) x62; cap' = cap.CNodeCap x61 x62 x63\<rbrakk> \<Longrightarrow> (word_bits < unat ((data >> 3) && mask 5) + x62 \<longrightarrow> (\<exists>s'. valid_idle s' \<and> s' \<turnstile> cap.CNodeCap x61 x62 x63) \<longrightarrow> cdl_cap.NullCap = (case case the_cnode_cap (cap.CNodeCap x61 x62 x63) of (oref, bits, guard) \<Rightarrow> if word_bits < unat ((data >> 3) && mask 5) + bits then cap.NullCap else cap.CNodeCap oref bits (drop (size ((data >> 8) && mask 18) - unat ((data >> 3) && mask 5)) (to_bl ((data >> 8) && mask 18))) 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 ptr badge cap_rights_ \<Rightarrow> cdl_cap.EndpointCap ptr badge cap_rights_ | cap.NotificationCap ptr badge cap_rights_ \<Rightarrow> cdl_cap.NotificationCap ptr badge cap_rights_ | 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 ptr \<Rightarrow> TcbCap ptr | cap.DomainCap \<Rightarrow> cdl_cap.DomainCap | IRQControlCap \<Rightarrow> IrqControlCap | IRQHandlerCap irq \<Rightarrow> IrqHandlerCap irq | 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))) \<and> (\<not> word_bits < unat ((data >> 3) && mask 5) + x62 \<longrightarrow> (\<exists>s'. valid_idle s' \<and> s' \<turnstile> cap.CNodeCap x61 x62 x63) \<longrightarrow> cdl_cap.CNodeCap x61 ((data >> 8) && mask (min (unat ((data >> 3) && mask 5)) 18)) (unat ((data >> 3) && mask 5)) x62 = (case case the_cnode_cap (cap.CNodeCap x61 x62 x63) of (oref, bits, guard) \<Rightarrow> if word_bits < unat ((data >> 3) && mask 5) + bits then cap.NullCap else cap.CNodeCap oref bits (drop (size ((data >> 8) && mask 18) - unat ((data >> 3) && mask 5)) (to_bl ((data >> 8) && mask 18))) 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 ptr badge cap_rights_ \<Rightarrow> cdl_cap.EndpointCap ptr badge cap_rights_ | cap.NotificationCap ptr badge cap_rights_ \<Rightarrow> cdl_cap.NotificationCap ptr badge cap_rights_ | 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 ptr \<Rightarrow> TcbCap ptr | cap.DomainCap \<Rightarrow> cdl_cap.DomainCap | IRQControlCap \<Rightarrow> IrqControlCap | IRQHandlerCap irq \<Rightarrow> IrqHandlerCap irq | 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)))
 4. \<And>x12. \<lbrakk>cap = (case x12 of ASIDPoolCap ptr asid \<Rightarrow> AsidPoolCap ptr (fst $ transform_asid asid) | ASIDControlCap \<Rightarrow> AsidControlCap | PageCap dev ptr cap_rights_ sz mp \<Rightarrow> FrameCap dev ptr cap_rights_ (pageBitsForSize sz) Real (transform_mapping mp) | arch_cap.PageTableCap ptr mp \<Rightarrow> cdl_cap.PageTableCap ptr Real (transform_mapping mp) | arch_cap.PageDirectoryCap ptr mp \<Rightarrow> cdl_cap.PageDirectoryCap ptr Real (map_option transform_asid mp)); cap' = ArchObjectCap x12\<rbrakk> \<Longrightarrow> (\<exists>s'. valid_idle s' \<and> s' \<turnstile> ArchObjectCap x12) \<longrightarrow> (case case x12 of ASIDPoolCap ptr asid \<Rightarrow> AsidPoolCap ptr (fst $ transform_asid asid) | ASIDControlCap \<Rightarrow> AsidControlCap | PageCap dev ptr cap_rights_ sz mp \<Rightarrow> FrameCap dev ptr cap_rights_ (pageBitsForSize sz) Real (transform_mapping mp) | arch_cap.PageTableCap ptr mp \<Rightarrow> cdl_cap.PageTableCap ptr Real (transform_mapping mp) | arch_cap.PageDirectoryCap ptr mp \<Rightarrow> cdl_cap.PageDirectoryCap ptr Real (map_option transform_asid mp) of cdl_cap.EndpointCap x b xa \<Rightarrow> if b = 0 \<and> \<not> preserve then CSpace_D.badge_update data cap else cdl_cap.NullCap | cdl_cap.NotificationCap x b xa \<Rightarrow> if b = 0 \<and> \<not> preserve then CSpace_D.badge_update data cap else cdl_cap.NullCap | cdl_cap.CNodeCap object guard guard_size sz \<Rightarrow> let reserved_bits = 3; guard_bits = 18; guard_size_bits = 5; new_guard_size = unat ((data >> reserved_bits) && mask guard_size_bits); new_guard = (data >> reserved_bits + guard_size_bits) && mask (min (unat ((data >> reserved_bits) && mask guard_size_bits)) guard_bits) in if word_bits < new_guard_size + sz then cdl_cap.NullCap else cdl_cap.CNodeCap object new_guard new_guard_size sz | _ \<Rightarrow> cap) = (case arch_update_cap_data preserve data x12 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 ptr badge cap_rights_ \<Rightarrow> cdl_cap.EndpointCap ptr badge cap_rights_ | cap.NotificationCap ptr badge cap_rights_ \<Rightarrow> cdl_cap.NotificationCap ptr badge cap_rights_ | 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 ptr \<Rightarrow> TcbCap ptr | cap.DomainCap \<Rightarrow> cdl_cap.DomainCap | IRQControlCap \<Rightarrow> IrqControlCap | IRQHandlerCap irq \<Rightarrow> IrqHandlerCap irq | 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 (3 subgoals):
 1. \<And>x41 x42 x43. \<lbrakk>cap = cdl_cap.NotificationCap x41 x42 x43; cap' = cap.NotificationCap x41 x42 x43\<rbrakk> \<Longrightarrow> (x42 = 0 \<and> \<not> preserve \<longrightarrow> (\<exists>s'. valid_idle s' \<and> s' \<turnstile> cap.NotificationCap x41 0 x43) \<longrightarrow> CSpace_D.badge_update data (cdl_cap.NotificationCap x41 0 x43) = (case Structures_A.badge_update data (cap.NotificationCap x41 0 x43) 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))) \<and> ((x42 = 0 \<longrightarrow> preserve) \<longrightarrow> x42 = 0 \<and> \<not> preserve \<longrightarrow> (\<exists>s'. valid_idle s' \<and> s' \<turnstile> cap.NotificationCap x41 0 x43) \<longrightarrow> CSpace_D.badge_update data (cdl_cap.NotificationCap x41 0 x43) = (case Structures_A.badge_update data (cap.NotificationCap x41 0 x43) 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)))
 2. \<And>x61 x62 x63. \<lbrakk>cap = cdl_cap.CNodeCap x61 (of_bl x63) (length x63) x62; cap' = cap.CNodeCap x61 x62 x63\<rbrakk> \<Longrightarrow> (word_bits < unat ((data >> 3) && mask 5) + x62 \<longrightarrow> (\<exists>s'. valid_idle s' \<and> s' \<turnstile> cap.CNodeCap x61 x62 x63) \<longrightarrow> cdl_cap.NullCap = (case case the_cnode_cap (cap.CNodeCap x61 x62 x63) of (oref, bits, guard) \<Rightarrow> if word_bits < unat ((data >> 3) && mask 5) + bits then cap.NullCap else cap.CNodeCap oref bits (drop (size ((data >> 8) && mask 18) - unat ((data >> 3) && mask 5)) (to_bl ((data >> 8) && mask 18))) 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 ptr badge cap_rights_ \<Rightarrow> cdl_cap.EndpointCap ptr badge cap_rights_ | cap.NotificationCap ptr badge cap_rights_ \<Rightarrow> cdl_cap.NotificationCap ptr badge cap_rights_ | 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 ptr \<Rightarrow> TcbCap ptr | cap.DomainCap \<Rightarrow> cdl_cap.DomainCap | IRQControlCap \<Rightarrow> IrqControlCap | IRQHandlerCap irq \<Rightarrow> IrqHandlerCap irq | 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))) \<and> (\<not> word_bits < unat ((data >> 3) && mask 5) + x62 \<longrightarrow> (\<exists>s'. valid_idle s' \<and> s' \<turnstile> cap.CNodeCap x61 x62 x63) \<longrightarrow> cdl_cap.CNodeCap x61 ((data >> 8) && mask (min (unat ((data >> 3) && mask 5)) 18)) (unat ((data >> 3) && mask 5)) x62 = (case case the_cnode_cap (cap.CNodeCap x61 x62 x63) of (oref, bits, guard) \<Rightarrow> if word_bits < unat ((data >> 3) && mask 5) + bits then cap.NullCap else cap.CNodeCap oref bits (drop (size ((data >> 8) && mask 18) - unat ((data >> 3) && mask 5)) (to_bl ((data >> 8) && mask 18))) 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 ptr badge cap_rights_ \<Rightarrow> cdl_cap.EndpointCap ptr badge cap_rights_ | cap.NotificationCap ptr badge cap_rights_ \<Rightarrow> cdl_cap.NotificationCap ptr badge cap_rights_ | 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 ptr \<Rightarrow> TcbCap ptr | cap.DomainCap \<Rightarrow> cdl_cap.DomainCap | IRQControlCap \<Rightarrow> IrqControlCap | IRQHandlerCap irq \<Rightarrow> IrqHandlerCap irq | 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)))
 3. \<And>x12. \<lbrakk>cap = (case x12 of ASIDPoolCap ptr asid \<Rightarrow> AsidPoolCap ptr (fst $ transform_asid asid) | ASIDControlCap \<Rightarrow> AsidControlCap | PageCap dev ptr cap_rights_ sz mp \<Rightarrow> FrameCap dev ptr cap_rights_ (pageBitsForSize sz) Real (transform_mapping mp) | arch_cap.PageTableCap ptr mp \<Rightarrow> cdl_cap.PageTableCap ptr Real (transform_mapping mp) | arch_cap.PageDirectoryCap ptr mp \<Rightarrow> cdl_cap.PageDirectoryCap ptr Real (map_option transform_asid mp)); cap' = ArchObjectCap x12\<rbrakk> \<Longrightarrow> (\<exists>s'. valid_idle s' \<and> s' \<turnstile> ArchObjectCap x12) \<longrightarrow> (case case x12 of ASIDPoolCap ptr asid \<Rightarrow> AsidPoolCap ptr (fst $ transform_asid asid) | ASIDControlCap \<Rightarrow> AsidControlCap | PageCap dev ptr cap_rights_ sz mp \<Rightarrow> FrameCap dev ptr cap_rights_ (pageBitsForSize sz) Real (transform_mapping mp) | arch_cap.PageTableCap ptr mp \<Rightarrow> cdl_cap.PageTableCap ptr Real (transform_mapping mp) | arch_cap.PageDirectoryCap ptr mp \<Rightarrow> cdl_cap.PageDirectoryCap ptr Real (map_option transform_asid mp) of cdl_cap.EndpointCap x b xa \<Rightarrow> if b = 0 \<and> \<not> preserve then CSpace_D.badge_update data cap else cdl_cap.NullCap | cdl_cap.NotificationCap x b xa \<Rightarrow> if b = 0 \<and> \<not> preserve then CSpace_D.badge_update data cap else cdl_cap.NullCap | cdl_cap.CNodeCap object guard guard_size sz \<Rightarrow> let reserved_bits = 3; guard_bits = 18; guard_size_bits = 5; new_guard_size = unat ((data >> reserved_bits) && mask guard_size_bits); new_guard = (data >> reserved_bits + guard_size_bits) && mask (min (unat ((data >> reserved_bits) && mask guard_size_bits)) guard_bits) in if word_bits < new_guard_size + sz then cdl_cap.NullCap else cdl_cap.CNodeCap object new_guard new_guard_size sz | _ \<Rightarrow> cap) = (case arch_update_cap_data preserve data x12 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 ptr badge cap_rights_ \<Rightarrow> cdl_cap.EndpointCap ptr badge cap_rights_ | cap.NotificationCap ptr badge cap_rights_ \<Rightarrow> cdl_cap.NotificationCap ptr badge cap_rights_ | 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 ptr \<Rightarrow> TcbCap ptr | cap.DomainCap \<Rightarrow> cdl_cap.DomainCap | IRQControlCap \<Rightarrow> IrqControlCap | IRQHandlerCap irq \<Rightarrow> IrqHandlerCap irq | 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 (2 subgoals):
 1. \<And>x61 x62 x63. \<lbrakk>cap = cdl_cap.CNodeCap x61 (of_bl x63) (length x63) x62; cap' = cap.CNodeCap x61 x62 x63\<rbrakk> \<Longrightarrow> (word_bits < unat ((data >> 3) && mask 5) + x62 \<longrightarrow> (\<exists>s'. valid_idle s' \<and> s' \<turnstile> cap.CNodeCap x61 x62 x63) \<longrightarrow> cdl_cap.NullCap = (case case the_cnode_cap (cap.CNodeCap x61 x62 x63) of (oref, bits, guard) \<Rightarrow> if word_bits < unat ((data >> 3) && mask 5) + bits then cap.NullCap else cap.CNodeCap oref bits (drop (size ((data >> 8) && mask 18) - unat ((data >> 3) && mask 5)) (to_bl ((data >> 8) && mask 18))) 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 ptr badge cap_rights_ \<Rightarrow> cdl_cap.EndpointCap ptr badge cap_rights_ | cap.NotificationCap ptr badge cap_rights_ \<Rightarrow> cdl_cap.NotificationCap ptr badge cap_rights_ | 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 ptr \<Rightarrow> TcbCap ptr | cap.DomainCap \<Rightarrow> cdl_cap.DomainCap | IRQControlCap \<Rightarrow> IrqControlCap | IRQHandlerCap irq \<Rightarrow> IrqHandlerCap irq | 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))) \<and> (\<not> word_bits < unat ((data >> 3) && mask 5) + x62 \<longrightarrow> (\<exists>s'. valid_idle s' \<and> s' \<turnstile> cap.CNodeCap x61 x62 x63) \<longrightarrow> cdl_cap.CNodeCap x61 ((data >> 8) && mask (min (unat ((data >> 3) && mask 5)) 18)) (unat ((data >> 3) && mask 5)) x62 = (case case the_cnode_cap (cap.CNodeCap x61 x62 x63) of (oref, bits, guard) \<Rightarrow> if word_bits < unat ((data >> 3) && mask 5) + bits then cap.NullCap else cap.CNodeCap oref bits (drop (size ((data >> 8) && mask 18) - unat ((data >> 3) && mask 5)) (to_bl ((data >> 8) && mask 18))) 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 ptr badge cap_rights_ \<Rightarrow> cdl_cap.EndpointCap ptr badge cap_rights_ | cap.NotificationCap ptr badge cap_rights_ \<Rightarrow> cdl_cap.NotificationCap ptr badge cap_rights_ | 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 ptr \<Rightarrow> TcbCap ptr | cap.DomainCap \<Rightarrow> cdl_cap.DomainCap | IRQControlCap \<Rightarrow> IrqControlCap | IRQHandlerCap irq \<Rightarrow> IrqHandlerCap irq | 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)))
 2. \<And>x12. \<lbrakk>cap = (case x12 of ASIDPoolCap ptr asid \<Rightarrow> AsidPoolCap ptr (fst $ transform_asid asid) | ASIDControlCap \<Rightarrow> AsidControlCap | PageCap dev ptr cap_rights_ sz mp \<Rightarrow> FrameCap dev ptr cap_rights_ (pageBitsForSize sz) Real (transform_mapping mp) | arch_cap.PageTableCap ptr mp \<Rightarrow> cdl_cap.PageTableCap ptr Real (transform_mapping mp) | arch_cap.PageDirectoryCap ptr mp \<Rightarrow> cdl_cap.PageDirectoryCap ptr Real (map_option transform_asid mp)); cap' = ArchObjectCap x12\<rbrakk> \<Longrightarrow> (\<exists>s'. valid_idle s' \<and> s' \<turnstile> ArchObjectCap x12) \<longrightarrow> (case case x12 of ASIDPoolCap ptr asid \<Rightarrow> AsidPoolCap ptr (fst $ transform_asid asid) | ASIDControlCap \<Rightarrow> AsidControlCap | PageCap dev ptr cap_rights_ sz mp \<Rightarrow> FrameCap dev ptr cap_rights_ (pageBitsForSize sz) Real (transform_mapping mp) | arch_cap.PageTableCap ptr mp \<Rightarrow> cdl_cap.PageTableCap ptr Real (transform_mapping mp) | arch_cap.PageDirectoryCap ptr mp \<Rightarrow> cdl_cap.PageDirectoryCap ptr Real (map_option transform_asid mp) of cdl_cap.EndpointCap x b xa \<Rightarrow> if b = 0 \<and> \<not> preserve then CSpace_D.badge_update data cap else cdl_cap.NullCap | cdl_cap.NotificationCap x b xa \<Rightarrow> if b = 0 \<and> \<not> preserve then CSpace_D.badge_update data cap else cdl_cap.NullCap | cdl_cap.CNodeCap object guard guard_size sz \<Rightarrow> let reserved_bits = 3; guard_bits = 18; guard_size_bits = 5; new_guard_size = unat ((data >> reserved_bits) && mask guard_size_bits); new_guard = (data >> reserved_bits + guard_size_bits) && mask (min (unat ((data >> reserved_bits) && mask guard_size_bits)) guard_bits) in if word_bits < new_guard_size + sz then cdl_cap.NullCap else cdl_cap.CNodeCap object new_guard new_guard_size sz | _ \<Rightarrow> cap) = (case arch_update_cap_data preserve data x12 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 ptr badge cap_rights_ \<Rightarrow> cdl_cap.EndpointCap ptr badge cap_rights_ | cap.NotificationCap ptr badge cap_rights_ \<Rightarrow> cdl_cap.NotificationCap ptr badge cap_rights_ | 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 ptr \<Rightarrow> TcbCap ptr | cap.DomainCap \<Rightarrow> cdl_cap.DomainCap | IRQControlCap \<Rightarrow> IrqControlCap | IRQHandlerCap irq \<Rightarrow> IrqHandlerCap irq | 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 (2 subgoals):
 1. \<And>x61 x62 x63. \<lbrakk>cap = cdl_cap.CNodeCap x61 (of_bl x63) (length x63) x62; cap' = cap.CNodeCap x61 x62 x63\<rbrakk> \<Longrightarrow> \<not> word_bits < unat ((data >> 3) && mask 5) + x62 \<longrightarrow> (\<exists>s'. valid_idle s' \<and> s' \<turnstile> cap.CNodeCap x61 x62 x63) \<longrightarrow> (data >> 8) && mask (min (unat ((data >> 3) && mask 5)) 18) = of_bl (drop (size ((data >> 8) && mask 18) - unat ((data >> 3) && mask 5)) (to_bl ((data >> 8) && mask 18))) \<and> unat ((data >> 3) && mask 5) = 32 - (size ((data >> 8) && mask 18) - unat ((data >> 3) && mask 5))
 2. \<And>x12. \<lbrakk>cap = (case x12 of ASIDPoolCap ptr asid \<Rightarrow> AsidPoolCap ptr (fst $ transform_asid asid) | ASIDControlCap \<Rightarrow> AsidControlCap | PageCap dev ptr cap_rights_ sz mp \<Rightarrow> FrameCap dev ptr cap_rights_ (pageBitsForSize sz) Real (transform_mapping mp) | arch_cap.PageTableCap ptr mp \<Rightarrow> cdl_cap.PageTableCap ptr Real (transform_mapping mp) | arch_cap.PageDirectoryCap ptr mp \<Rightarrow> cdl_cap.PageDirectoryCap ptr Real (map_option transform_asid mp)); cap' = ArchObjectCap x12\<rbrakk> \<Longrightarrow> (\<exists>s'. valid_idle s' \<and> s' \<turnstile> ArchObjectCap x12) \<longrightarrow> (case case x12 of ASIDPoolCap ptr asid \<Rightarrow> AsidPoolCap ptr (fst $ transform_asid asid) | ASIDControlCap \<Rightarrow> AsidControlCap | PageCap dev ptr cap_rights_ sz mp \<Rightarrow> FrameCap dev ptr cap_rights_ (pageBitsForSize sz) Real (transform_mapping mp) | arch_cap.PageTableCap ptr mp \<Rightarrow> cdl_cap.PageTableCap ptr Real (transform_mapping mp) | arch_cap.PageDirectoryCap ptr mp \<Rightarrow> cdl_cap.PageDirectoryCap ptr Real (map_option transform_asid mp) of cdl_cap.EndpointCap x b xa \<Rightarrow> if b = 0 \<and> \<not> preserve then CSpace_D.badge_update data cap else cdl_cap.NullCap | cdl_cap.NotificationCap x b xa \<Rightarrow> if b = 0 \<and> \<not> preserve then CSpace_D.badge_update data cap else cdl_cap.NullCap | cdl_cap.CNodeCap object guard guard_size sz \<Rightarrow> let reserved_bits = 3; guard_bits = 18; guard_size_bits = 5; new_guard_size = unat ((data >> reserved_bits) && mask guard_size_bits); new_guard = (data >> reserved_bits + guard_size_bits) && mask (min (unat ((data >> reserved_bits) && mask guard_size_bits)) guard_bits) in if word_bits < new_guard_size + sz then cdl_cap.NullCap else cdl_cap.CNodeCap object new_guard new_guard_size sz | _ \<Rightarrow> cap) = (case arch_update_cap_data preserve data x12 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 ptr badge cap_rights_ \<Rightarrow> cdl_cap.EndpointCap ptr badge cap_rights_ | cap.NotificationCap ptr badge cap_rights_ \<Rightarrow> cdl_cap.NotificationCap ptr badge cap_rights_ | 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 ptr \<Rightarrow> TcbCap ptr | cap.DomainCap \<Rightarrow> cdl_cap.DomainCap | IRQControlCap \<Rightarrow> IrqControlCap | IRQHandlerCap irq \<Rightarrow> IrqHandlerCap irq | 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 (2 subgoals):
 1. \<And>x61 x62 x63 s'. \<lbrakk>cap = cdl_cap.CNodeCap x61 (of_bl x63) (length x63) x62; cap' = cap.CNodeCap x61 x62 x63; unat ((data >> 3) && mask 5) + x62 \<le> 32; valid_idle s'; s' \<turnstile> cap.CNodeCap x61 x62 x63\<rbrakk> \<Longrightarrow> (data >> 8) && mask (min (unat ((data >> 3) && mask 5)) 18) = of_bl (drop (size ((data >> 8) && mask 18) - unat ((data >> 3) && mask 5)) (to_bl ((data >> 8) && mask 18))) \<and> unat ((data >> 3) && mask 5) = 32 - (size ((data >> 8) && mask 18) - unat ((data >> 3) && mask 5))
 2. \<And>x12. \<lbrakk>cap = (case x12 of ASIDPoolCap ptr asid \<Rightarrow> AsidPoolCap ptr (fst $ transform_asid asid) | ASIDControlCap \<Rightarrow> AsidControlCap | PageCap dev ptr cap_rights_ sz mp \<Rightarrow> FrameCap dev ptr cap_rights_ (pageBitsForSize sz) Real (transform_mapping mp) | arch_cap.PageTableCap ptr mp \<Rightarrow> cdl_cap.PageTableCap ptr Real (transform_mapping mp) | arch_cap.PageDirectoryCap ptr mp \<Rightarrow> cdl_cap.PageDirectoryCap ptr Real (map_option transform_asid mp)); cap' = ArchObjectCap x12\<rbrakk> \<Longrightarrow> (\<exists>s'. valid_idle s' \<and> s' \<turnstile> ArchObjectCap x12) \<longrightarrow> (case case x12 of ASIDPoolCap ptr asid \<Rightarrow> AsidPoolCap ptr (fst $ transform_asid asid) | ASIDControlCap \<Rightarrow> AsidControlCap | PageCap dev ptr cap_rights_ sz mp \<Rightarrow> FrameCap dev ptr cap_rights_ (pageBitsForSize sz) Real (transform_mapping mp) | arch_cap.PageTableCap ptr mp \<Rightarrow> cdl_cap.PageTableCap ptr Real (transform_mapping mp) | arch_cap.PageDirectoryCap ptr mp \<Rightarrow> cdl_cap.PageDirectoryCap ptr Real (map_option transform_asid mp) of cdl_cap.EndpointCap x b xa \<Rightarrow> if b = 0 \<and> \<not> preserve then CSpace_D.badge_update data cap else cdl_cap.NullCap | cdl_cap.NotificationCap x b xa \<Rightarrow> if b = 0 \<and> \<not> preserve then CSpace_D.badge_update data cap else cdl_cap.NullCap | cdl_cap.CNodeCap object guard guard_size sz \<Rightarrow> let reserved_bits = 3; guard_bits = 18; guard_size_bits = 5; new_guard_size = unat ((data >> reserved_bits) && mask guard_size_bits); new_guard = (data >> reserved_bits + guard_size_bits) && mask (min (unat ((data >> reserved_bits) && mask guard_size_bits)) guard_bits) in if word_bits < new_guard_size + sz then cdl_cap.NullCap else cdl_cap.CNodeCap object new_guard new_guard_size sz | _ \<Rightarrow> cap) = (case arch_update_cap_data preserve data x12 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 ptr badge cap_rights_ \<Rightarrow> cdl_cap.EndpointCap ptr badge cap_rights_ | cap.NotificationCap ptr badge cap_rights_ \<Rightarrow> cdl_cap.NotificationCap ptr badge cap_rights_ | 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 ptr \<Rightarrow> TcbCap ptr | cap.DomainCap \<Rightarrow> cdl_cap.DomainCap | IRQControlCap \<Rightarrow> IrqControlCap | IRQHandlerCap irq \<Rightarrow> IrqHandlerCap irq | 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 (2 subgoals):
 1. \<And>x61 x62 x63 s'. \<lbrakk>cap = cdl_cap.CNodeCap x61 (of_bl x63) (length x63) x62; cap' = cap.CNodeCap x61 x62 x63; unat ((data >> 3) && mask 5) + x62 \<le> 32; valid_idle s'; s' \<turnstile> cap.CNodeCap x61 x62 x63\<rbrakk> \<Longrightarrow> (data >> 8) && mask (min (unat ((data >> 3) && mask 5)) 18) = ((data >> 8) && mask 18) && mask (size ((data >> 8) && mask 18) - (size ((data >> 8) && mask 18) - unat ((data >> 3) && mask 5))) \<and> unat ((data >> 3) && mask 5) = 32 - (size ((data >> 8) && mask 18) - unat ((data >> 3) && mask 5))
 2. \<And>x12. \<lbrakk>cap = (case x12 of ASIDPoolCap ptr asid \<Rightarrow> AsidPoolCap ptr (fst $ transform_asid asid) | ASIDControlCap \<Rightarrow> AsidControlCap | PageCap dev ptr cap_rights_ sz mp \<Rightarrow> FrameCap dev ptr cap_rights_ (pageBitsForSize sz) Real (transform_mapping mp) | arch_cap.PageTableCap ptr mp \<Rightarrow> cdl_cap.PageTableCap ptr Real (transform_mapping mp) | arch_cap.PageDirectoryCap ptr mp \<Rightarrow> cdl_cap.PageDirectoryCap ptr Real (map_option transform_asid mp)); cap' = ArchObjectCap x12\<rbrakk> \<Longrightarrow> (\<exists>s'. valid_idle s' \<and> s' \<turnstile> ArchObjectCap x12) \<longrightarrow> (case case x12 of ASIDPoolCap ptr asid \<Rightarrow> AsidPoolCap ptr (fst $ transform_asid asid) | ASIDControlCap \<Rightarrow> AsidControlCap | PageCap dev ptr cap_rights_ sz mp \<Rightarrow> FrameCap dev ptr cap_rights_ (pageBitsForSize sz) Real (transform_mapping mp) | arch_cap.PageTableCap ptr mp \<Rightarrow> cdl_cap.PageTableCap ptr Real (transform_mapping mp) | arch_cap.PageDirectoryCap ptr mp \<Rightarrow> cdl_cap.PageDirectoryCap ptr Real (map_option transform_asid mp) of cdl_cap.EndpointCap x b xa \<Rightarrow> if b = 0 \<and> \<not> preserve then CSpace_D.badge_update data cap else cdl_cap.NullCap | cdl_cap.NotificationCap x b xa \<Rightarrow> if b = 0 \<and> \<not> preserve then CSpace_D.badge_update data cap else cdl_cap.NullCap | cdl_cap.CNodeCap object guard guard_size sz \<Rightarrow> let reserved_bits = 3; guard_bits = 18; guard_size_bits = 5; new_guard_size = unat ((data >> reserved_bits) && mask guard_size_bits); new_guard = (data >> reserved_bits + guard_size_bits) && mask (min (unat ((data >> reserved_bits) && mask guard_size_bits)) guard_bits) in if word_bits < new_guard_size + sz then cdl_cap.NullCap else cdl_cap.CNodeCap object new_guard new_guard_size sz | _ \<Rightarrow> cap) = (case arch_update_cap_data preserve data x12 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 ptr badge cap_rights_ \<Rightarrow> cdl_cap.EndpointCap ptr badge cap_rights_ | cap.NotificationCap ptr badge cap_rights_ \<Rightarrow> cdl_cap.NotificationCap ptr badge cap_rights_ | 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 ptr \<Rightarrow> TcbCap ptr | cap.DomainCap \<Rightarrow> cdl_cap.DomainCap | IRQControlCap \<Rightarrow> IrqControlCap | IRQHandlerCap irq \<Rightarrow> IrqHandlerCap irq | 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 (2 subgoals):
 1. \<And>x61 x62 x63 s'. \<lbrakk>cap = cdl_cap.CNodeCap x61 (of_bl x63) (length x63) x62; cap' = cap.CNodeCap x61 x62 x63; unat ((data >> 3) && mask 5) + x62 \<le> 32; valid_idle s'; s' \<turnstile> cap.CNodeCap x61 x62 x63\<rbrakk> \<Longrightarrow> (data >> 8) && mask (min (unat ((data >> 3) && mask 5)) 18) = (data >> 8) && mask (min (size ((data >> 8) && mask 18) - (size ((data >> 8) && mask 18) - unat ((data >> 3) && mask 5))) 18) \<and> unat ((data >> 3) && mask 5) = 32 - (size ((data >> 8) && mask 18) - unat ((data >> 3) && mask 5))
 2. \<And>x12. \<lbrakk>cap = (case x12 of ASIDPoolCap ptr asid \<Rightarrow> AsidPoolCap ptr (fst $ transform_asid asid) | ASIDControlCap \<Rightarrow> AsidControlCap | PageCap dev ptr cap_rights_ sz mp \<Rightarrow> FrameCap dev ptr cap_rights_ (pageBitsForSize sz) Real (transform_mapping mp) | arch_cap.PageTableCap ptr mp \<Rightarrow> cdl_cap.PageTableCap ptr Real (transform_mapping mp) | arch_cap.PageDirectoryCap ptr mp \<Rightarrow> cdl_cap.PageDirectoryCap ptr Real (map_option transform_asid mp)); cap' = ArchObjectCap x12\<rbrakk> \<Longrightarrow> (\<exists>s'. valid_idle s' \<and> s' \<turnstile> ArchObjectCap x12) \<longrightarrow> (case case x12 of ASIDPoolCap ptr asid \<Rightarrow> AsidPoolCap ptr (fst $ transform_asid asid) | ASIDControlCap \<Rightarrow> AsidControlCap | PageCap dev ptr cap_rights_ sz mp \<Rightarrow> FrameCap dev ptr cap_rights_ (pageBitsForSize sz) Real (transform_mapping mp) | arch_cap.PageTableCap ptr mp \<Rightarrow> cdl_cap.PageTableCap ptr Real (transform_mapping mp) | arch_cap.PageDirectoryCap ptr mp \<Rightarrow> cdl_cap.PageDirectoryCap ptr Real (map_option transform_asid mp) of cdl_cap.EndpointCap x b xa \<Rightarrow> if b = 0 \<and> \<not> preserve then CSpace_D.badge_update data cap else cdl_cap.NullCap | cdl_cap.NotificationCap x b xa \<Rightarrow> if b = 0 \<and> \<not> preserve then CSpace_D.badge_update data cap else cdl_cap.NullCap | cdl_cap.CNodeCap object guard guard_size sz \<Rightarrow> let reserved_bits = 3; guard_bits = 18; guard_size_bits = 5; new_guard_size = unat ((data >> reserved_bits) && mask guard_size_bits); new_guard = (data >> reserved_bits + guard_size_bits) && mask (min (unat ((data >> reserved_bits) && mask guard_size_bits)) guard_bits) in if word_bits < new_guard_size + sz then cdl_cap.NullCap else cdl_cap.CNodeCap object new_guard new_guard_size sz | _ \<Rightarrow> cap) = (case arch_update_cap_data preserve data x12 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 ptr badge cap_rights_ \<Rightarrow> cdl_cap.EndpointCap ptr badge cap_rights_ | cap.NotificationCap ptr badge cap_rights_ \<Rightarrow> cdl_cap.NotificationCap ptr badge cap_rights_ | 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 ptr \<Rightarrow> TcbCap ptr | cap.DomainCap \<Rightarrow> cdl_cap.DomainCap | IRQControlCap \<Rightarrow> IrqControlCap | IRQHandlerCap irq \<Rightarrow> IrqHandlerCap irq | 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 (1 subgoal):
 1. \<And>x12. \<lbrakk>cap = (case x12 of ASIDPoolCap ptr asid \<Rightarrow> AsidPoolCap ptr (fst $ transform_asid asid) | ASIDControlCap \<Rightarrow> AsidControlCap | PageCap dev ptr cap_rights_ sz mp \<Rightarrow> FrameCap dev ptr cap_rights_ (pageBitsForSize sz) Real (transform_mapping mp) | arch_cap.PageTableCap ptr mp \<Rightarrow> cdl_cap.PageTableCap ptr Real (transform_mapping mp) | arch_cap.PageDirectoryCap ptr mp \<Rightarrow> cdl_cap.PageDirectoryCap ptr Real (map_option transform_asid mp)); cap' = ArchObjectCap x12\<rbrakk> \<Longrightarrow> (\<exists>s'. valid_idle s' \<and> s' \<turnstile> ArchObjectCap x12) \<longrightarrow> (case case x12 of ASIDPoolCap ptr asid \<Rightarrow> AsidPoolCap ptr (fst $ transform_asid asid) | ASIDControlCap \<Rightarrow> AsidControlCap | PageCap dev ptr cap_rights_ sz mp \<Rightarrow> FrameCap dev ptr cap_rights_ (pageBitsForSize sz) Real (transform_mapping mp) | arch_cap.PageTableCap ptr mp \<Rightarrow> cdl_cap.PageTableCap ptr Real (transform_mapping mp) | arch_cap.PageDirectoryCap ptr mp \<Rightarrow> cdl_cap.PageDirectoryCap ptr Real (map_option transform_asid mp) of cdl_cap.EndpointCap x b xa \<Rightarrow> if b = 0 \<and> \<not> preserve then CSpace_D.badge_update data cap else cdl_cap.NullCap | cdl_cap.NotificationCap x b xa \<Rightarrow> if b = 0 \<and> \<not> preserve then CSpace_D.badge_update data cap else cdl_cap.NullCap | cdl_cap.CNodeCap object guard guard_size sz \<Rightarrow> let reserved_bits = 3; guard_bits = 18; guard_size_bits = 5; new_guard_size = unat ((data >> reserved_bits) && mask guard_size_bits); new_guard = (data >> reserved_bits + guard_size_bits) && mask (min (unat ((data >> reserved_bits) && mask guard_size_bits)) guard_bits) in if word_bits < new_guard_size + sz then cdl_cap.NullCap else cdl_cap.CNodeCap object new_guard new_guard_size sz | _ \<Rightarrow> cap) = (case arch_update_cap_data preserve data x12 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 ptr badge cap_rights_ \<Rightarrow> cdl_cap.EndpointCap ptr badge cap_rights_ | cap.NotificationCap ptr badge cap_rights_ \<Rightarrow> cdl_cap.NotificationCap ptr badge cap_rights_ | 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 ptr \<Rightarrow> TcbCap ptr | cap.DomainCap \<Rightarrow> cdl_cap.DomainCap | IRQControlCap \<Rightarrow> IrqControlCap | IRQHandlerCap irq \<Rightarrow> IrqHandlerCap irq | 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 (1 subgoal):
 1. \<And>arch_cap. \<lbrakk>cap = (case arch_cap of ASIDPoolCap ptr asid \<Rightarrow> AsidPoolCap ptr (fst $ transform_asid asid) | ASIDControlCap \<Rightarrow> AsidControlCap | PageCap dev ptr cap_rights_ sz mp \<Rightarrow> FrameCap dev ptr cap_rights_ (pageBitsForSize sz) Real (transform_mapping mp) | arch_cap.PageTableCap ptr mp \<Rightarrow> cdl_cap.PageTableCap ptr Real (transform_mapping mp) | arch_cap.PageDirectoryCap ptr mp \<Rightarrow> cdl_cap.PageDirectoryCap ptr Real (map_option transform_asid mp)); cap' = ArchObjectCap arch_cap\<rbrakk> \<Longrightarrow> (\<exists>s'. valid_idle s' \<and> s' \<turnstile> ArchObjectCap arch_cap) \<longrightarrow> (case case arch_cap of ASIDPoolCap ptr asid \<Rightarrow> AsidPoolCap ptr (fst $ transform_asid asid) | ASIDControlCap \<Rightarrow> AsidControlCap | PageCap dev ptr cap_rights_ sz mp \<Rightarrow> FrameCap dev ptr cap_rights_ (pageBitsForSize sz) Real (transform_mapping mp) | arch_cap.PageTableCap ptr mp \<Rightarrow> cdl_cap.PageTableCap ptr Real (transform_mapping mp) | arch_cap.PageDirectoryCap ptr mp \<Rightarrow> cdl_cap.PageDirectoryCap ptr Real (map_option transform_asid mp) of cdl_cap.EndpointCap x b xa \<Rightarrow> if b = 0 \<and> \<not> preserve then CSpace_D.badge_update data cap else cdl_cap.NullCap | cdl_cap.NotificationCap x b xa \<Rightarrow> if b = 0 \<and> \<not> preserve then CSpace_D.badge_update data cap else cdl_cap.NullCap | cdl_cap.CNodeCap object guard guard_size sz \<Rightarrow> let reserved_bits = 3; guard_bits = 18; guard_size_bits = 5; new_guard_size = unat ((data >> reserved_bits) && mask guard_size_bits); new_guard = (data >> reserved_bits + guard_size_bits) && mask (min (unat ((data >> reserved_bits) && mask guard_size_bits)) guard_bits) in if word_bits < new_guard_size + sz then cdl_cap.NullCap else cdl_cap.CNodeCap object new_guard new_guard_size sz | _ \<Rightarrow> cap) = (case arch_update_cap_data preserve data arch_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 ptr badge cap_rights_ \<Rightarrow> cdl_cap.EndpointCap ptr badge cap_rights_ | cap.NotificationCap ptr badge cap_rights_ \<Rightarrow> cdl_cap.NotificationCap ptr badge cap_rights_ | 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 ptr \<Rightarrow> TcbCap ptr | cap.DomainCap \<Rightarrow> cdl_cap.DomainCap | IRQControlCap \<Rightarrow> IrqControlCap | IRQHandlerCap irq \<Rightarrow> IrqHandlerCap irq | 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!