theory CNodeInv_R

lemma cap_relation_NullCap:
  "cap_relation cap cap' \<Longrightarrow>
   (update_cap_data P x cap = cap.NullCap) = (RetypeDecls_H.updateCapData P x cap' = capability.NullCap)" apply (cases cap) apply (simp_all add: Let_def mask_cap_def cap_rights_update_def update_cap_data_closedform
                                 arch_update_cap_data_def word_bits_def updateCapData_def isCap_simps
                      split del: if_split) apply simp apply simp apply (clarsimp simp: word_size word_size_def cteRightsBits_def cteGuardBits_def) apply (clarsimp simp: ARM_H.updateCapData_def isCap_simps split del: if_split) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cap_relation cap cap' \<Longrightarrow> (update_cap_data P x cap = cap.NullCap) = (global.updateCapData P x cap' = capability.NullCap) proof (prove)
goal (12 subgoals):
 1. \<lbrakk>cap_relation cap cap'; cap = cap.NullCap\<rbrakk> \<Longrightarrow> (update_cap_data P x cap = cap.NullCap) = (global.updateCapData P x cap' = capability.NullCap)
 2. \<And>x21 x22 x23 x24. \<lbrakk>cap_relation cap cap'; cap = cap.UntypedCap x21 x22 x23 x24\<rbrakk> \<Longrightarrow> (update_cap_data P x cap = cap.NullCap) = (global.updateCapData P x cap' = capability.NullCap)
 3. \<And>x31 x32 x33. \<lbrakk>cap_relation cap cap'; cap = cap.EndpointCap x31 x32 x33\<rbrakk> \<Longrightarrow> (update_cap_data P x cap = cap.NullCap) = (global.updateCapData P x cap' = capability.NullCap)
 4. \<And>x41 x42 x43. \<lbrakk>cap_relation cap cap'; cap = cap.NotificationCap x41 x42 x43\<rbrakk> \<Longrightarrow> (update_cap_data P x cap = cap.NullCap) = (global.updateCapData P x cap' = capability.NullCap)
 5. \<And>x51 x52 x53. \<lbrakk>cap_relation cap cap'; cap = cap.ReplyCap x51 x52 x53\<rbrakk> \<Longrightarrow> (update_cap_data P x cap = cap.NullCap) = (global.updateCapData P x cap' = capability.NullCap)
 6. \<And>x61 x62 x63. \<lbrakk>cap_relation cap cap'; cap = cap.CNodeCap x61 x62 x63\<rbrakk> \<Longrightarrow> (update_cap_data P x cap = cap.NullCap) = (global.updateCapData P x cap' = capability.NullCap)
 7. \<And>x7. \<lbrakk>cap_relation cap cap'; cap = cap.ThreadCap x7\<rbrakk> \<Longrightarrow> (update_cap_data P x cap = cap.NullCap) = (global.updateCapData P x cap' = capability.NullCap)
 8. \<lbrakk>cap_relation cap cap'; cap = cap.DomainCap\<rbrakk> \<Longrightarrow> (update_cap_data P x cap = cap.NullCap) = (global.updateCapData P x cap' = capability.NullCap)
 9. \<lbrakk>cap_relation cap cap'; cap = cap.IRQControlCap\<rbrakk> \<Longrightarrow> (update_cap_data P x cap = cap.NullCap) = (global.updateCapData P x cap' = capability.NullCap)
 10. \<And>x10. \<lbrakk>cap_relation cap cap'; cap = cap.IRQHandlerCap x10\<rbrakk> \<Longrightarrow> (update_cap_data P x cap = cap.NullCap) = (global.updateCapData P x cap' = capability.NullCap)
A total of 12 subgoals... proof (prove)
goal (4 subgoals):
 1. \<And>x31 x32 x33. \<lbrakk>cap' = capability.EndpointCap x31 x32 (AllowWrite \<in> x33) (AllowRead \<in> x33) (AllowGrant \<in> x33) (AllowGrantReply \<in> x33); cap = cap.EndpointCap x31 x32 x33\<rbrakk> \<Longrightarrow> ((if x32 = 0 \<and> \<not> P then cap.EndpointCap x31 (x && mask 28) x33 else cap.NullCap) = cap.NullCap) = ((if \<not> P \<and> x32 = 0 then capability.EndpointCap x31 (x && mask 28) (AllowWrite \<in> x33) (AllowRead \<in> x33) (AllowGrant \<in> x33) (AllowGrantReply \<in> x33) else capability.NullCap) = capability.NullCap)
 2. \<And>x41 x42 x43. \<lbrakk>cap' = capability.NotificationCap x41 x42 (AllowWrite \<in> x43) (AllowRead \<in> x43); cap = cap.NotificationCap x41 x42 x43\<rbrakk> \<Longrightarrow> ((if x42 = 0 \<and> \<not> P then cap.NotificationCap x41 (x && mask 28) x43 else cap.NullCap) = cap.NullCap) = ((if \<not> P \<and> x42 = 0 then capability.NotificationCap x41 (x && mask 28) (AllowWrite \<in> x43) (AllowRead \<in> x43) else capability.NullCap) = capability.NullCap)
 3. \<And>x61 x62 x63. \<lbrakk>cap' = capability.CNodeCap x61 x62 (of_bl x63) (length x63); cap = cap.CNodeCap x61 x62 x63\<rbrakk> \<Longrightarrow> ((if 32 < unat ((x >> 3) && mask 5) + x62 then cap.NullCap else cap.CNodeCap x61 x62 (drop (size ((x >> 8) && mask 18) - unat ((x >> 3) && mask 5)) (to_bl ((x >> 8) && mask 18)))) = cap.NullCap) = ((if size x < unat ((x >> cteRightsBits) && mask 5) + x62 then capability.NullCap else capability.CNodeCap x61 x62 ((x >> cteRightsBits + 5) && mask cteGuardBits && mask (unat ((x >> cteRightsBits) && mask 5))) (unat ((x >> cteRightsBits) && mask 5))) = capability.NullCap)
 4. \<And>x12. \<lbrakk>\<exists>a'. acap_relation x12 a' \<and> cap' = capability.ArchObjectCap a'; cap = cap.ArchObjectCap x12\<rbrakk> \<Longrightarrow> (if \<exists>v0 v1 v2 v3 v4 v5. cap' = capability.EndpointCap v0 v1 v2 v3 v4 v5 then if \<not> P \<and> capEPBadge cap' = 0 then capEPBadge_update (\<lambda>_. x && mask 28) cap' else capability.NullCap else if \<exists>v0 v1 v2 v3. cap' = capability.NotificationCap v0 v1 v2 v3 then if \<not> P \<and> capNtfnBadge cap' = 0 then capNtfnBadge_update (\<lambda>_. x && mask 28) cap' else capability.NullCap else if \<exists>v0 v1 v2 v3. cap' = capability.CNodeCap v0 v1 v2 v3 then if size x < unat ((x >> cteRightsBits) && mask 5) + capCNodeBits cap' then capability.NullCap else capCNodeGuardSize_update (\<lambda>_. unat ((x >> cteRightsBits) && mask 5)) (capCNodeGuard_update (\<lambda>_. (x >> cteRightsBits + 5) && mask cteGuardBits && mask (unat ((x >> cteRightsBits) && mask 5))) cap') else if \<exists>v0. cap' = capability.ArchObjectCap v0 then Arch.updateCapData P x (capCap cap') else cap') \<noteq> capability.NullCap proof (prove)
goal (3 subgoals):
 1. \<And>x41 x42 x43. \<lbrakk>cap' = capability.NotificationCap x41 x42 (AllowWrite \<in> x43) (AllowRead \<in> x43); cap = cap.NotificationCap x41 x42 x43\<rbrakk> \<Longrightarrow> ((if x42 = 0 \<and> \<not> P then cap.NotificationCap x41 (x && mask 28) x43 else cap.NullCap) = cap.NullCap) = ((if \<not> P \<and> x42 = 0 then capability.NotificationCap x41 (x && mask 28) (AllowWrite \<in> x43) (AllowRead \<in> x43) else capability.NullCap) = capability.NullCap)
 2. \<And>x61 x62 x63. \<lbrakk>cap' = capability.CNodeCap x61 x62 (of_bl x63) (length x63); cap = cap.CNodeCap x61 x62 x63\<rbrakk> \<Longrightarrow> ((if 32 < unat ((x >> 3) && mask 5) + x62 then cap.NullCap else cap.CNodeCap x61 x62 (drop (size ((x >> 8) && mask 18) - unat ((x >> 3) && mask 5)) (to_bl ((x >> 8) && mask 18)))) = cap.NullCap) = ((if size x < unat ((x >> cteRightsBits) && mask 5) + x62 then capability.NullCap else capability.CNodeCap x61 x62 ((x >> cteRightsBits + 5) && mask cteGuardBits && mask (unat ((x >> cteRightsBits) && mask 5))) (unat ((x >> cteRightsBits) && mask 5))) = capability.NullCap)
 3. \<And>x12. \<lbrakk>\<exists>a'. acap_relation x12 a' \<and> cap' = capability.ArchObjectCap a'; cap = cap.ArchObjectCap x12\<rbrakk> \<Longrightarrow> (if \<exists>v0 v1 v2 v3 v4 v5. cap' = capability.EndpointCap v0 v1 v2 v3 v4 v5 then if \<not> P \<and> capEPBadge cap' = 0 then capEPBadge_update (\<lambda>_. x && mask 28) cap' else capability.NullCap else if \<exists>v0 v1 v2 v3. cap' = capability.NotificationCap v0 v1 v2 v3 then if \<not> P \<and> capNtfnBadge cap' = 0 then capNtfnBadge_update (\<lambda>_. x && mask 28) cap' else capability.NullCap else if \<exists>v0 v1 v2 v3. cap' = capability.CNodeCap v0 v1 v2 v3 then if size x < unat ((x >> cteRightsBits) && mask 5) + capCNodeBits cap' then capability.NullCap else capCNodeGuardSize_update (\<lambda>_. unat ((x >> cteRightsBits) && mask 5)) (capCNodeGuard_update (\<lambda>_. (x >> cteRightsBits + 5) && mask cteGuardBits && mask (unat ((x >> cteRightsBits) && mask 5))) cap') else if \<exists>v0. cap' = capability.ArchObjectCap v0 then Arch.updateCapData P x (capCap cap') else cap') \<noteq> capability.NullCap proof (prove)
goal (2 subgoals):
 1. \<And>x61 x62 x63. \<lbrakk>cap' = capability.CNodeCap x61 x62 (of_bl x63) (length x63); cap = cap.CNodeCap x61 x62 x63\<rbrakk> \<Longrightarrow> ((if 32 < unat ((x >> 3) && mask 5) + x62 then cap.NullCap else cap.CNodeCap x61 x62 (drop (size ((x >> 8) && mask 18) - unat ((x >> 3) && mask 5)) (to_bl ((x >> 8) && mask 18)))) = cap.NullCap) = ((if size x < unat ((x >> cteRightsBits) && mask 5) + x62 then capability.NullCap else capability.CNodeCap x61 x62 ((x >> cteRightsBits + 5) && mask cteGuardBits && mask (unat ((x >> cteRightsBits) && mask 5))) (unat ((x >> cteRightsBits) && mask 5))) = capability.NullCap)
 2. \<And>x12. \<lbrakk>\<exists>a'. acap_relation x12 a' \<and> cap' = capability.ArchObjectCap a'; cap = cap.ArchObjectCap x12\<rbrakk> \<Longrightarrow> (if \<exists>v0 v1 v2 v3 v4 v5. cap' = capability.EndpointCap v0 v1 v2 v3 v4 v5 then if \<not> P \<and> capEPBadge cap' = 0 then capEPBadge_update (\<lambda>_. x && mask 28) cap' else capability.NullCap else if \<exists>v0 v1 v2 v3. cap' = capability.NotificationCap v0 v1 v2 v3 then if \<not> P \<and> capNtfnBadge cap' = 0 then capNtfnBadge_update (\<lambda>_. x && mask 28) cap' else capability.NullCap else if \<exists>v0 v1 v2 v3. cap' = capability.CNodeCap v0 v1 v2 v3 then if size x < unat ((x >> cteRightsBits) && mask 5) + capCNodeBits cap' then capability.NullCap else capCNodeGuardSize_update (\<lambda>_. unat ((x >> cteRightsBits) && mask 5)) (capCNodeGuard_update (\<lambda>_. (x >> cteRightsBits + 5) && mask cteGuardBits && mask (unat ((x >> cteRightsBits) && mask 5))) cap') else if \<exists>v0. cap' = capability.ArchObjectCap v0 then Arch.updateCapData P x (capCap cap') else cap') \<noteq> capability.NullCap proof (prove)
goal (1 subgoal):
 1. \<And>x12. \<lbrakk>\<exists>a'. acap_relation x12 a' \<and> cap' = capability.ArchObjectCap a'; cap = cap.ArchObjectCap x12\<rbrakk> \<Longrightarrow> (if \<exists>v0 v1 v2 v3 v4 v5. cap' = capability.EndpointCap v0 v1 v2 v3 v4 v5 then if \<not> P \<and> capEPBadge cap' = 0 then capEPBadge_update (\<lambda>_. x && mask 28) cap' else capability.NullCap else if \<exists>v0 v1 v2 v3. cap' = capability.NotificationCap v0 v1 v2 v3 then if \<not> P \<and> capNtfnBadge cap' = 0 then capNtfnBadge_update (\<lambda>_. x && mask 28) cap' else capability.NullCap else if \<exists>v0 v1 v2 v3. cap' = capability.CNodeCap v0 v1 v2 v3 then if size x < unat ((x >> cteRightsBits) && mask 5) + capCNodeBits cap' then capability.NullCap else capCNodeGuardSize_update (\<lambda>_. unat ((x >> cteRightsBits) && mask 5)) (capCNodeGuard_update (\<lambda>_. (x >> cteRightsBits + 5) && mask cteGuardBits && mask (unat ((x >> cteRightsBits) && mask 5))) cap') else if \<exists>v0. cap' = capability.ArchObjectCap v0 then Arch.updateCapData P x (capCap cap') else cap') \<noteq> capability.NullCap proof (prove)
goal:
No subgoals!