theory CSpace1_R

lemma cap_map_update_data:
  assumes "cap_relation c c'"
  shows   "cap_relation (update_cap_data p x c) (updateCapData p x c')" proof - note simps = update_cap_data_def updateCapData_def word_size
               isCap_defs is_cap_defs Let_def
               cap_rights_update_def badge_update_def { fix x :: word32 define y where "y \<equiv> (x >> 8) && mask 18" define z where "z \<equiv> unat ((x >> 3) && mask 5)" have "of_bl (to_bl (y && mask z)) = (of_bl (replicate (32-z) False @ drop (32-z) (to_bl y))::word32)" by (simp add: bl_and_mask) then have "y && mask z = of_bl (drop (32 - z) (to_bl y))" apply simp apply (subst test_bit_eq_iff [symmetric]) apply (rule ext) apply (clarsimp simp: test_bit_of_bl nth_append) done } note x = this from assms show ?thesis apply (cases c) apply (simp_all add: simps)[5] defer apply (simp_all add: simps)[4] apply (clarsimp simp: simps the_arch_cap_def) apply (rename_tac arch_cap) apply (case_tac arch_cap) apply (simp_all add: simps arch_update_cap_data_def
                             ARM_H.updateCapData_def)[5]
  \<comment> \<open>CNodeCap\<close> apply (simp add: simps word_bits_def the_cnode_cap_def andCapRights_def
                   rightsFromWord_def data_to_rights_def nth_ucast cteRightsBits_def
                   cteGuardBits_def) apply (insert x) apply (subgoal_tac "unat ((x >> 3) && mask 5) < unat (2^5::word32)") prefer 2 apply (fold word_less_nat_alt)[1] apply (rule and_mask_less_size) apply (simp add: word_size) apply (simp add: word_bw_assocs) done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cap_relation (update_cap_data p x c) (global.updateCapData p x c') proof (state)
goal (1 subgoal):
 1. cap_relation (update_cap_data p x c) (global.updateCapData p x c') proof (state)
this:
update_cap_data ?preserve ?w ?cap \<equiv> if is_ep_cap ?cap then if cap_ep_badge ?cap = 0 \<and> \<not> ?preserve then badge_update ?w ?cap else cap.NullCap else if is_ntfn_cap ?cap then if cap_ep_badge ?cap = 0 \<and> \<not> ?preserve then badge_update ?w ?cap else cap.NullCap else if is_cnode_cap ?cap then let (oref, bits, guard) = the_cnode_cap ?cap; (guard_size', guard'') = update_cnode_cap_data ?w; guard' = drop (size guard'' - guard_size') (to_bl guard'') in if word_bits < guard_size' + bits then cap.NullCap else cap.CNodeCap oref bits guard' else if is_arch_cap ?cap then arch_update_cap_data ?preserve ?w (the_arch_cap ?cap) else ?cap
global.updateCapData ?x0.0 ?x1.0 ?x2.0 \<equiv> let (v16, v17, v18) = (?x0.0, ?x1.0, ?x2.0) in if isEndpointCap v18 then let preserve = v16; new = v17; cap = v18 in if \<not> preserve \<and> capEPBadge cap = 0 then capEPBadge_update (\<lambda>_. new && mask badgeBits) cap else if True then capability.NullCap else undefined else if isNotificationCap v18 then let preserve = v16; new = v17; cap = v18 in if \<not> preserve \<and> capNtfnBadge cap = 0 then capNtfnBadge_update (\<lambda>_. new && mask badgeBits) cap else if True then capability.NullCap else undefined else if isCNodeCap v18 then let w = v17; cap = v18; guardSizeBits = wordSizeCase 5 6; guardSize = fromIntegral $ w `~shiftR~` cteRightsBits && mask guardSizeBits; guard = w `~shiftR~` (cteRightsBits + guardSizeBits) && mask cteGuardBits && mask guardSize in if finiteBitSize w < guardSize + capCNodeBits cap then capability.NullCap else if True then capCNodeGuardSize_update (\<lambda>_. guardSize) (capCNodeGuard_update (\<lambda>_. guard) cap) else undefined else if isArchObjectCap v18 then let p = v16; w = v17 in Let (capCap v18) (Arch.updateCapData p w) else let cap = v18 in cap
size ?w = LENGTH(?'a)
isZombie ?v \<equiv> case ?v of capability.Zombie v0 v1 v2 \<Rightarrow> True | _ \<Rightarrow> False
isArchObjectCap ?v \<equiv> case ?v of capability.ArchObjectCap v0 \<Rightarrow> True | _ \<Rightarrow> False
isThreadCap ?v \<equiv> case ?v of capability.ThreadCap v0 \<Rightarrow> True | _ \<Rightarrow> False
isCNodeCap ?v \<equiv> case ?v of capability.CNodeCap v0 v1 v2 v3 \<Rightarrow> True | _ \<Rightarrow> False
isNotificationCap ?v \<equiv> case ?v of capability.NotificationCap v0 v1 v2 v3 \<Rightarrow> True | _ \<Rightarrow> False
isEndpointCap ?v \<equiv> case ?v of capability.EndpointCap v0 v1 v2 v3 v4 v5 \<Rightarrow> True | _ \<Rightarrow> False
isUntypedCap ?v \<equiv> case ?v of capability.UntypedCap v0 v1 v2 v3 \<Rightarrow> True | _ \<Rightarrow> False
isNullCap ?v \<equiv> case ?v of capability.NullCap \<Rightarrow> True | _ \<Rightarrow> False
isIRQHandlerCap ?v \<equiv> case ?v of capability.IRQHandlerCap v0 \<Rightarrow> True | _ \<Rightarrow> False
isIRQControlCap ?v \<equiv> case ?v of capability.IRQControlCap \<Rightarrow> True | _ \<Rightarrow> False
isReplyCap ?v \<equiv> case ?v of capability.ReplyCap v0 v1 v2 \<Rightarrow> True | _ \<Rightarrow> False
isPageCap ?v \<equiv> case ?v of arch_capability.PageCap v0 v1 v2 v3 v4 \<Rightarrow> True | _ \<Rightarrow> False
isPageTableCap ?v \<equiv> case ?v of arch_capability.PageTableCap v0 v1 \<Rightarrow> True | _ \<Rightarrow> False
isPageDirectoryCap ?v \<equiv> case ?v of arch_capability.PageDirectoryCap v0 v1 \<Rightarrow> True | _ \<Rightarrow> False
isASIDControlCap ?v \<equiv> case ?v of arch_capability.ASIDControlCap \<Rightarrow> True | _ \<Rightarrow> False
isASIDPoolCap ?v \<equiv> case ?v of arch_capability.ASIDPoolCap v0 v1 \<Rightarrow> True | _ \<Rightarrow> False
isArchPageCap ?cap \<equiv> case ?cap of capability.ArchObjectCap (arch_capability.PageCap d ref rghts sz data) \<Rightarrow> True | capability.ArchObjectCap _ \<Rightarrow> False | _ \<Rightarrow> False
isDomainCap ?v \<equiv> case ?v of capability.DomainCap \<Rightarrow> True | _ \<Rightarrow> False
is_arch_cap ?cap \<equiv> case ?cap of cap.ArchObjectCap x \<Rightarrow> True | _ \<Rightarrow> False
is_zombie ?cap \<equiv> case ?cap of cap.Zombie x xa xb \<Rightarrow> True | _ \<Rightarrow> False
Let ?s ?f \<equiv> ?f ?s
cap_rights_update ?cr' ?cap \<equiv> case ?cap of cap.EndpointCap oref badge cr \<Rightarrow> cap.EndpointCap oref badge ?cr' | cap.NotificationCap oref badge cr \<Rightarrow> cap.NotificationCap oref badge (?cr' - {AllowGrant, AllowGrantReply}) | cap.ReplyCap t m cr \<Rightarrow> cap.ReplyCap t m (?cr' - {AllowRead, AllowGrantReply} \<union> {AllowWrite}) | cap.ArchObjectCap acap \<Rightarrow> cap.ArchObjectCap (acap_rights_update ?cr' acap) | _ \<Rightarrow> ?cap
badge_update ?data ?cap \<equiv> case ?cap of cap.EndpointCap oref badge cr \<Rightarrow> cap.EndpointCap oref (?data && mask badge_bits) cr | cap.NotificationCap oref badge cr \<Rightarrow> cap.NotificationCap oref (?data && mask badge_bits) cr | _ \<Rightarrow> ?cap

goal (1 subgoal):
 1. cap_relation (update_cap_data p x c) (global.updateCapData p x c') proof (state)
this:
update_cap_data ?preserve ?w ?cap \<equiv> if is_ep_cap ?cap then if cap_ep_badge ?cap = 0 \<and> \<not> ?preserve then badge_update ?w ?cap else cap.NullCap else if is_ntfn_cap ?cap then if cap_ep_badge ?cap = 0 \<and> \<not> ?preserve then badge_update ?w ?cap else cap.NullCap else if is_cnode_cap ?cap then let (oref, bits, guard) = the_cnode_cap ?cap; (guard_size', guard'') = update_cnode_cap_data ?w; guard' = drop (size guard'' - guard_size') (to_bl guard'') in if word_bits < guard_size' + bits then cap.NullCap else cap.CNodeCap oref bits guard' else if is_arch_cap ?cap then arch_update_cap_data ?preserve ?w (the_arch_cap ?cap) else ?cap
global.updateCapData ?x0.0 ?x1.0 ?x2.0 \<equiv> let (v16, v17, v18) = (?x0.0, ?x1.0, ?x2.0) in if isEndpointCap v18 then let preserve = v16; new = v17; cap = v18 in if \<not> preserve \<and> capEPBadge cap = 0 then capEPBadge_update (\<lambda>_. new && mask badgeBits) cap else if True then capability.NullCap else undefined else if isNotificationCap v18 then let preserve = v16; new = v17; cap = v18 in if \<not> preserve \<and> capNtfnBadge cap = 0 then capNtfnBadge_update (\<lambda>_. new && mask badgeBits) cap else if True then capability.NullCap else undefined else if isCNodeCap v18 then let w = v17; cap = v18; guardSizeBits = wordSizeCase 5 6; guardSize = fromIntegral $ w `~shiftR~` cteRightsBits && mask guardSizeBits; guard = w `~shiftR~` (cteRightsBits + guardSizeBits) && mask cteGuardBits && mask guardSize in if finiteBitSize w < guardSize + capCNodeBits cap then capability.NullCap else if True then capCNodeGuardSize_update (\<lambda>_. guardSize) (capCNodeGuard_update (\<lambda>_. guard) cap) else undefined else if isArchObjectCap v18 then let p = v16; w = v17 in Let (capCap v18) (Arch.updateCapData p w) else let cap = v18 in cap
size ?w = LENGTH(?'a)
isZombie ?v \<equiv> case ?v of capability.Zombie v0 v1 v2 \<Rightarrow> True | _ \<Rightarrow> False
isArchObjectCap ?v \<equiv> case ?v of capability.ArchObjectCap v0 \<Rightarrow> True | _ \<Rightarrow> False
isThreadCap ?v \<equiv> case ?v of capability.ThreadCap v0 \<Rightarrow> True | _ \<Rightarrow> False
isCNodeCap ?v \<equiv> case ?v of capability.CNodeCap v0 v1 v2 v3 \<Rightarrow> True | _ \<Rightarrow> False
isNotificationCap ?v \<equiv> case ?v of capability.NotificationCap v0 v1 v2 v3 \<Rightarrow> True | _ \<Rightarrow> False
isEndpointCap ?v \<equiv> case ?v of capability.EndpointCap v0 v1 v2 v3 v4 v5 \<Rightarrow> True | _ \<Rightarrow> False
isUntypedCap ?v \<equiv> case ?v of capability.UntypedCap v0 v1 v2 v3 \<Rightarrow> True | _ \<Rightarrow> False
isNullCap ?v \<equiv> case ?v of capability.NullCap \<Rightarrow> True | _ \<Rightarrow> False
isIRQHandlerCap ?v \<equiv> case ?v of capability.IRQHandlerCap v0 \<Rightarrow> True | _ \<Rightarrow> False
isIRQControlCap ?v \<equiv> case ?v of capability.IRQControlCap \<Rightarrow> True | _ \<Rightarrow> False
isReplyCap ?v \<equiv> case ?v of capability.ReplyCap v0 v1 v2 \<Rightarrow> True | _ \<Rightarrow> False
isPageCap ?v \<equiv> case ?v of arch_capability.PageCap v0 v1 v2 v3 v4 \<Rightarrow> True | _ \<Rightarrow> False
isPageTableCap ?v \<equiv> case ?v of arch_capability.PageTableCap v0 v1 \<Rightarrow> True | _ \<Rightarrow> False
isPageDirectoryCap ?v \<equiv> case ?v of arch_capability.PageDirectoryCap v0 v1 \<Rightarrow> True | _ \<Rightarrow> False
isASIDControlCap ?v \<equiv> case ?v of arch_capability.ASIDControlCap \<Rightarrow> True | _ \<Rightarrow> False
isASIDPoolCap ?v \<equiv> case ?v of arch_capability.ASIDPoolCap v0 v1 \<Rightarrow> True | _ \<Rightarrow> False
isArchPageCap ?cap \<equiv> case ?cap of capability.ArchObjectCap (arch_capability.PageCap d ref rghts sz data) \<Rightarrow> True | capability.ArchObjectCap _ \<Rightarrow> False | _ \<Rightarrow> False
isDomainCap ?v \<equiv> case ?v of capability.DomainCap \<Rightarrow> True | _ \<Rightarrow> False
is_arch_cap ?cap \<equiv> case ?cap of cap.ArchObjectCap x \<Rightarrow> True | _ \<Rightarrow> False
is_zombie ?cap \<equiv> case ?cap of cap.Zombie x xa xb \<Rightarrow> True | _ \<Rightarrow> False
Let ?s ?f \<equiv> ?f ?s
cap_rights_update ?cr' ?cap \<equiv> case ?cap of cap.EndpointCap oref badge cr \<Rightarrow> cap.EndpointCap oref badge ?cr' | cap.NotificationCap oref badge cr \<Rightarrow> cap.NotificationCap oref badge (?cr' - {AllowGrant, AllowGrantReply}) | cap.ReplyCap t m cr \<Rightarrow> cap.ReplyCap t m (?cr' - {AllowRead, AllowGrantReply} \<union> {AllowWrite}) | cap.ArchObjectCap acap \<Rightarrow> cap.ArchObjectCap (acap_rights_update ?cr' acap) | _ \<Rightarrow> ?cap
badge_update ?data ?cap \<equiv> case ?cap of cap.EndpointCap oref badge cr \<Rightarrow> cap.EndpointCap oref (?data && mask badge_bits) cr | cap.NotificationCap oref badge cr \<Rightarrow> cap.NotificationCap oref (?data && mask badge_bits) cr | _ \<Rightarrow> ?cap

goal (1 subgoal):
 1. cap_relation (update_cap_data p x c) (global.updateCapData p x c') proof (state)
goal (1 subgoal):
 1. cap_relation (update_cap_data p x c) (global.updateCapData p x c') proof (state)
this:
y \<equiv> (x >> 8) && mask 18

goal (1 subgoal):
 1. cap_relation (update_cap_data p x c) (global.updateCapData p x c') proof (state)
this:
z \<equiv> unat ((x >> 3) && mask 5)

goal (1 subgoal):
 1. cap_relation (update_cap_data p x c) (global.updateCapData p x c') proof (prove)
goal (1 subgoal):
 1. of_bl (to_bl (y && mask z)) = of_bl (replicate (32 - z) False @ drop (32 - z) (to_bl y)) proof (state)
this:
of_bl (to_bl (y && mask z)) = of_bl (replicate (32 - z) False @ drop (32 - z) (to_bl y))

goal (1 subgoal):
 1. cap_relation (update_cap_data p x c) (global.updateCapData p x c') proof (chain)
picking this:
of_bl (to_bl (y && mask z)) = of_bl (replicate (32 - z) False @ drop (32 - z) (to_bl y)) proof (prove)
using this:
of_bl (to_bl (y && mask z)) = of_bl (replicate (32 - z) False @ drop (32 - z) (to_bl y))

goal (1 subgoal):
 1. y && mask z = of_bl (drop (32 - z) (to_bl y)) proof (prove)
goal (1 subgoal):
 1. y && mask z = of_bl (replicate (32 - z) False @ drop (32 - z) (to_bl y)) \<Longrightarrow> of_bl (replicate (32 - z) False @ drop (32 - z) (to_bl y)) = of_bl (drop (32 - z) (to_bl y)) proof (prove)
goal (1 subgoal):
 1. y && mask z = of_bl (replicate (32 - z) False @ drop (32 - z) (to_bl y)) \<Longrightarrow> (!!) (of_bl (replicate (32 - z) False @ drop (32 - z) (to_bl y))) = (!!) (of_bl (drop (32 - z) (to_bl y))) proof (prove)
goal (1 subgoal):
 1. \<And>x. y && mask z = of_bl (replicate (32 - z) False @ drop (32 - z) (to_bl y)) \<Longrightarrow> of_bl (replicate (32 - z) False @ drop (32 - z) (to_bl y)) !! x = of_bl (drop (32 - z) (to_bl y)) !! x proof (prove)
goal:
No subgoals! proof (state)
this:
y && mask z = of_bl (drop (32 - z) (to_bl y))

goal (1 subgoal):
 1. cap_relation (update_cap_data p x c) (global.updateCapData p x c') proof (state)
this:
((?xa2 >> 8) && mask 18) && mask (unat ((?xa2 >> 3) && mask 5)) = of_bl (drop (32 - unat ((?xa2 >> 3) && mask 5)) (to_bl ((?xa2 >> 8) && mask 18)))

goal (1 subgoal):
 1. cap_relation (update_cap_data p x c) (global.updateCapData p x c') proof (state)
this:
((?xa2 >> 8) && mask 18) && mask (unat ((?xa2 >> 3) && mask 5)) = of_bl (drop (32 - unat ((?xa2 >> 3) && mask 5)) (to_bl ((?xa2 >> 8) && mask 18)))

goal (1 subgoal):
 1. cap_relation (update_cap_data p x c) (global.updateCapData p x c') proof (chain)
picking this:
cap_relation c c' proof (prove)
using this:
cap_relation c c'

goal (1 subgoal):
 1. cap_relation (update_cap_data p x c) (global.updateCapData p x c') proof (prove)
goal (12 subgoals):
 1. \<lbrakk>cap_relation c c'; c = cap.NullCap\<rbrakk> \<Longrightarrow> cap_relation (update_cap_data p x c) (global.updateCapData p x c')
 2. \<And>x21 x22 x23 x24. \<lbrakk>cap_relation c c'; c = cap.UntypedCap x21 x22 x23 x24\<rbrakk> \<Longrightarrow> cap_relation (update_cap_data p x c) (global.updateCapData p x c')
 3. \<And>x31 x32 x33. \<lbrakk>cap_relation c c'; c = cap.EndpointCap x31 x32 x33\<rbrakk> \<Longrightarrow> cap_relation (update_cap_data p x c) (global.updateCapData p x c')
 4. \<And>x41 x42 x43. \<lbrakk>cap_relation c c'; c = cap.NotificationCap x41 x42 x43\<rbrakk> \<Longrightarrow> cap_relation (update_cap_data p x c) (global.updateCapData p x c')
 5. \<And>x51 x52 x53. \<lbrakk>cap_relation c c'; c = cap.ReplyCap x51 x52 x53\<rbrakk> \<Longrightarrow> cap_relation (update_cap_data p x c) (global.updateCapData p x c')
 6. \<And>x61 x62 x63. \<lbrakk>cap_relation c c'; c = cap.CNodeCap x61 x62 x63\<rbrakk> \<Longrightarrow> cap_relation (update_cap_data p x c) (global.updateCapData p x c')
 7. \<And>x7. \<lbrakk>cap_relation c c'; c = cap.ThreadCap x7\<rbrakk> \<Longrightarrow> cap_relation (update_cap_data p x c) (global.updateCapData p x c')
 8. \<lbrakk>cap_relation c c'; c = cap.DomainCap\<rbrakk> \<Longrightarrow> cap_relation (update_cap_data p x c) (global.updateCapData p x c')
 9. \<lbrakk>cap_relation c c'; c = cap.IRQControlCap\<rbrakk> \<Longrightarrow> cap_relation (update_cap_data p x c) (global.updateCapData p x c')
 10. \<And>x10. \<lbrakk>cap_relation c c'; c = cap.IRQHandlerCap x10\<rbrakk> \<Longrightarrow> cap_relation (update_cap_data p x c) (global.updateCapData p x c')
A total of 12 subgoals... proof (prove)
goal (7 subgoals):
 1. \<And>x61 x62 x63. \<lbrakk>cap_relation c c'; c = cap.CNodeCap x61 x62 x63\<rbrakk> \<Longrightarrow> cap_relation (update_cap_data p x c) (global.updateCapData p x c')
 2. \<And>x7. \<lbrakk>cap_relation c c'; c = cap.ThreadCap x7\<rbrakk> \<Longrightarrow> cap_relation (update_cap_data p x c) (global.updateCapData p x c')
 3. \<lbrakk>cap_relation c c'; c = cap.DomainCap\<rbrakk> \<Longrightarrow> cap_relation (update_cap_data p x c) (global.updateCapData p x c')
 4. \<lbrakk>cap_relation c c'; c = cap.IRQControlCap\<rbrakk> \<Longrightarrow> cap_relation (update_cap_data p x c) (global.updateCapData p x c')
 5. \<And>x10. \<lbrakk>cap_relation c c'; c = cap.IRQHandlerCap x10\<rbrakk> \<Longrightarrow> cap_relation (update_cap_data p x c) (global.updateCapData p x c')
 6. \<And>x111 x112 x113. \<lbrakk>cap_relation c c'; c = cap.Zombie x111 x112 x113\<rbrakk> \<Longrightarrow> cap_relation (update_cap_data p x c) (global.updateCapData p x c')
 7. \<And>x12. \<lbrakk>cap_relation c c'; c = cap.ArchObjectCap x12\<rbrakk> \<Longrightarrow> cap_relation (update_cap_data p x c) (global.updateCapData p x c') proof (prove)
goal (7 subgoals):
 1. \<And>x7. \<lbrakk>cap_relation c c'; c = cap.ThreadCap x7\<rbrakk> \<Longrightarrow> cap_relation (update_cap_data p x c) (global.updateCapData p x c')
 2. \<lbrakk>cap_relation c c'; c = cap.DomainCap\<rbrakk> \<Longrightarrow> cap_relation (update_cap_data p x c) (global.updateCapData p x c')
 3. \<lbrakk>cap_relation c c'; c = cap.IRQControlCap\<rbrakk> \<Longrightarrow> cap_relation (update_cap_data p x c) (global.updateCapData p x c')
 4. \<And>x10. \<lbrakk>cap_relation c c'; c = cap.IRQHandlerCap x10\<rbrakk> \<Longrightarrow> cap_relation (update_cap_data p x c) (global.updateCapData p x c')
 5. \<And>x111 x112 x113. \<lbrakk>cap_relation c c'; c = cap.Zombie x111 x112 x113\<rbrakk> \<Longrightarrow> cap_relation (update_cap_data p x c) (global.updateCapData p x c')
 6. \<And>x12. \<lbrakk>cap_relation c c'; c = cap.ArchObjectCap x12\<rbrakk> \<Longrightarrow> cap_relation (update_cap_data p x c) (global.updateCapData p x c')
 7. \<And>x61 x62 x63. \<lbrakk>cap_relation c c'; c = cap.CNodeCap x61 x62 x63\<rbrakk> \<Longrightarrow> cap_relation (update_cap_data p x c) (global.updateCapData p x c') proof (prove)
goal (3 subgoals):
 1. \<And>x111 x112 x113. \<lbrakk>cap_relation c c'; c = cap.Zombie x111 x112 x113\<rbrakk> \<Longrightarrow> cap_relation (update_cap_data p x c) (global.updateCapData p x c')
 2. \<And>x12. \<lbrakk>cap_relation c c'; c = cap.ArchObjectCap x12\<rbrakk> \<Longrightarrow> cap_relation (update_cap_data p x c) (global.updateCapData p x c')
 3. \<And>x61 x62 x63. \<lbrakk>cap_relation c c'; c = cap.CNodeCap x61 x62 x63\<rbrakk> \<Longrightarrow> cap_relation (update_cap_data p x c) (global.updateCapData p x c') proof (prove)
goal (2 subgoals):
 1. \<And>x12. \<lbrakk>cap_relation c c'; c = cap.ArchObjectCap x12\<rbrakk> \<Longrightarrow> cap_relation (update_cap_data p x c) (global.updateCapData p x c')
 2. \<And>x61 x62 x63. \<lbrakk>cap_relation c c'; c = cap.CNodeCap x61 x62 x63\<rbrakk> \<Longrightarrow> cap_relation (update_cap_data p x c) (global.updateCapData p x c') proof (prove)
goal (2 subgoals):
 1. \<And>arch_cap. \<lbrakk>cap_relation c c'; c = cap.ArchObjectCap arch_cap\<rbrakk> \<Longrightarrow> cap_relation (update_cap_data p x c) (global.updateCapData p x c')
 2. \<And>x61 x62 x63. \<lbrakk>cap_relation c c'; c = cap.CNodeCap x61 x62 x63\<rbrakk> \<Longrightarrow> cap_relation (update_cap_data p x c) (global.updateCapData p x c') proof (prove)
goal (6 subgoals):
 1. \<And>arch_cap x11 x12. \<lbrakk>cap_relation c c'; c = cap.ArchObjectCap arch_cap; arch_cap = arch_cap.ASIDPoolCap x11 x12\<rbrakk> \<Longrightarrow> cap_relation (update_cap_data p x c) (global.updateCapData p x c')
 2. \<And>arch_cap. \<lbrakk>cap_relation c c'; c = cap.ArchObjectCap arch_cap; arch_cap = arch_cap.ASIDControlCap\<rbrakk> \<Longrightarrow> cap_relation (update_cap_data p x c) (global.updateCapData p x c')
 3. \<And>arch_cap x31 x32 x33 x34 x35. \<lbrakk>cap_relation c c'; c = cap.ArchObjectCap arch_cap; arch_cap = arch_cap.PageCap x31 x32 x33 x34 x35\<rbrakk> \<Longrightarrow> cap_relation (update_cap_data p x c) (global.updateCapData p x c')
 4. \<And>arch_cap x41 x42. \<lbrakk>cap_relation c c'; c = cap.ArchObjectCap arch_cap; arch_cap = arch_cap.PageTableCap x41 x42\<rbrakk> \<Longrightarrow> cap_relation (update_cap_data p x c) (global.updateCapData p x c')
 5. \<And>arch_cap x51 x52. \<lbrakk>cap_relation c c'; c = cap.ArchObjectCap arch_cap; arch_cap = arch_cap.PageDirectoryCap x51 x52\<rbrakk> \<Longrightarrow> cap_relation (update_cap_data p x c) (global.updateCapData p x c')
 6. \<And>x61 x62 x63. \<lbrakk>cap_relation c c'; c = cap.CNodeCap x61 x62 x63\<rbrakk> \<Longrightarrow> cap_relation (update_cap_data p x c) (global.updateCapData p x c') proof (prove)
goal (1 subgoal):
 1. \<And>x61 x62 x63. \<lbrakk>cap_relation c c'; c = cap.CNodeCap x61 x62 x63\<rbrakk> \<Longrightarrow> cap_relation (update_cap_data p x c) (global.updateCapData p x c') proof (prove)
goal (1 subgoal):
 1. \<And>x61 x62 x63. \<lbrakk>c' = capability.CNodeCap x61 x62 (of_bl x63) (length x63); c = cap.CNodeCap x61 x62 x63\<rbrakk> \<Longrightarrow> \<not> 32 < unat ((x >> 3) && mask 5) + x62 \<longrightarrow> (x >> 8) && mask 18 && mask (unat ((x >> 3) && mask 5)) = of_bl (drop (32 - unat ((x >> 3) && mask 5)) (to_bl ((x >> 8) && mask 18))) proof (prove)
goal (1 subgoal):
 1. \<And>x61 x62 x63. \<lbrakk>c' = capability.CNodeCap x61 x62 (of_bl x63) (length x63); c = cap.CNodeCap x61 x62 x63; \<And>xa. ((xa >> 8) && mask 18) && mask (unat ((xa >> 3) && mask 5)) = of_bl (drop (32 - unat ((xa >> 3) && mask 5)) (to_bl ((xa >> 8) && mask 18)))\<rbrakk> \<Longrightarrow> \<not> 32 < unat ((x >> 3) && mask 5) + x62 \<longrightarrow> (x >> 8) && mask 18 && mask (unat ((x >> 3) && mask 5)) = of_bl (drop (32 - unat ((x >> 3) && mask 5)) (to_bl ((x >> 8) && mask 18))) proof (prove)
goal (2 subgoals):
 1. \<And>x61 x62 x63. \<lbrakk>c' = capability.CNodeCap x61 x62 (of_bl x63) (length x63); c = cap.CNodeCap x61 x62 x63; \<And>xa. ((xa >> 8) && mask 18) && mask (unat ((xa >> 3) && mask 5)) = of_bl (drop (32 - unat ((xa >> 3) && mask 5)) (to_bl ((xa >> 8) && mask 18))); unat ((x >> 3) && mask 5) < unat (2 ^ 5)\<rbrakk> \<Longrightarrow> \<not> 32 < unat ((x >> 3) && mask 5) + x62 \<longrightarrow> (x >> 8) && mask 18 && mask (unat ((x >> 3) && mask 5)) = of_bl (drop (32 - unat ((x >> 3) && mask 5)) (to_bl ((x >> 8) && mask 18)))
 2. \<And>x61 x62 x63. \<lbrakk>c' = capability.CNodeCap x61 x62 (of_bl x63) (length x63); c = cap.CNodeCap x61 x62 x63; \<And>xa. ((xa >> 8) && mask 18) && mask (unat ((xa >> 3) && mask 5)) = of_bl (drop (32 - unat ((xa >> 3) && mask 5)) (to_bl ((xa >> 8) && mask 18)))\<rbrakk> \<Longrightarrow> unat ((x >> 3) && mask 5) < unat (2 ^ 5) proof (prove)
goal (2 subgoals):
 1. \<And>x61 x62 x63. \<lbrakk>c' = capability.CNodeCap x61 x62 (of_bl x63) (length x63); c = cap.CNodeCap x61 x62 x63; \<And>xa. ((xa >> 8) && mask 18) && mask (unat ((xa >> 3) && mask 5)) = of_bl (drop (32 - unat ((xa >> 3) && mask 5)) (to_bl ((xa >> 8) && mask 18)))\<rbrakk> \<Longrightarrow> unat ((x >> 3) && mask 5) < unat (2 ^ 5)
 2. \<And>x61 x62 x63. \<lbrakk>c' = capability.CNodeCap x61 x62 (of_bl x63) (length x63); c = cap.CNodeCap x61 x62 x63; \<And>xa. ((xa >> 8) && mask 18) && mask (unat ((xa >> 3) && mask 5)) = of_bl (drop (32 - unat ((xa >> 3) && mask 5)) (to_bl ((xa >> 8) && mask 18))); unat ((x >> 3) && mask 5) < unat (2 ^ 5)\<rbrakk> \<Longrightarrow> \<not> 32 < unat ((x >> 3) && mask 5) + x62 \<longrightarrow> (x >> 8) && mask 18 && mask (unat ((x >> 3) && mask 5)) = of_bl (drop (32 - unat ((x >> 3) && mask 5)) (to_bl ((x >> 8) && mask 18))) proof (prove)
goal (2 subgoals):
 1. \<And>x61 x62 x63. \<lbrakk>c' = capability.CNodeCap x61 x62 (of_bl x63) (length x63); c = cap.CNodeCap x61 x62 x63; \<And>xa. ((xa >> 8) && mask 18) && mask (unat ((xa >> 3) && mask 5)) = of_bl (drop (32 - unat ((xa >> 3) && mask 5)) (to_bl ((xa >> 8) && mask 18)))\<rbrakk> \<Longrightarrow> (x >> 3) && mask 5 < 2 ^ 5
 2. \<And>x61 x62 x63. \<lbrakk>c' = capability.CNodeCap x61 x62 (of_bl x63) (length x63); c = cap.CNodeCap x61 x62 x63; \<And>xa. ((xa >> 8) && mask 18) && mask (unat ((xa >> 3) && mask 5)) = of_bl (drop (32 - unat ((xa >> 3) && mask 5)) (to_bl ((xa >> 8) && mask 18))); unat ((x >> 3) && mask 5) < unat (2 ^ 5)\<rbrakk> \<Longrightarrow> \<not> 32 < unat ((x >> 3) && mask 5) + x62 \<longrightarrow> (x >> 8) && mask 18 && mask (unat ((x >> 3) && mask 5)) = of_bl (drop (32 - unat ((x >> 3) && mask 5)) (to_bl ((x >> 8) && mask 18))) proof (prove)
goal (2 subgoals):
 1. \<And>x61 x62 x63. \<lbrakk>c' = capability.CNodeCap x61 x62 (of_bl x63) (length x63); c = cap.CNodeCap x61 x62 x63; \<And>xa. ((xa >> 8) && mask 18) && mask (unat ((xa >> 3) && mask 5)) = of_bl (drop (32 - unat ((xa >> 3) && mask 5)) (to_bl ((xa >> 8) && mask 18)))\<rbrakk> \<Longrightarrow> 5 < size (x >> 3)
 2. \<And>x61 x62 x63. \<lbrakk>c' = capability.CNodeCap x61 x62 (of_bl x63) (length x63); c = cap.CNodeCap x61 x62 x63; \<And>xa. ((xa >> 8) && mask 18) && mask (unat ((xa >> 3) && mask 5)) = of_bl (drop (32 - unat ((xa >> 3) && mask 5)) (to_bl ((xa >> 8) && mask 18))); unat ((x >> 3) && mask 5) < unat (2 ^ 5)\<rbrakk> \<Longrightarrow> \<not> 32 < unat ((x >> 3) && mask 5) + x62 \<longrightarrow> (x >> 8) && mask 18 && mask (unat ((x >> 3) && mask 5)) = of_bl (drop (32 - unat ((x >> 3) && mask 5)) (to_bl ((x >> 8) && mask 18))) proof (prove)
goal (1 subgoal):
 1. \<And>x61 x62 x63. \<lbrakk>c' = capability.CNodeCap x61 x62 (of_bl x63) (length x63); c = cap.CNodeCap x61 x62 x63; \<And>xa. ((xa >> 8) && mask 18) && mask (unat ((xa >> 3) && mask 5)) = of_bl (drop (32 - unat ((xa >> 3) && mask 5)) (to_bl ((xa >> 8) && mask 18))); unat ((x >> 3) && mask 5) < unat (2 ^ 5)\<rbrakk> \<Longrightarrow> \<not> 32 < unat ((x >> 3) && mask 5) + x62 \<longrightarrow> (x >> 8) && mask 18 && mask (unat ((x >> 3) && mask 5)) = of_bl (drop (32 - unat ((x >> 3) && mask 5)) (to_bl ((x >> 8) && mask 18))) proof (prove)
goal:
No subgoals! proof (state)
this:
cap_relation (update_cap_data p x c) (global.updateCapData p x c')

goal:
No subgoals!