theory Tcb_C

lemma isValidVTableRoot_conv:
  "\<lbrakk> ccap_relation cap cap' \<rbrakk>
      \<Longrightarrow> isValidVTableRoot_C cap' = isValidVTableRoot cap" apply (clarsimp simp: isValidVTableRoot_C_def
                        if_1_0_0 from_bool_0 isValidVTableRoot_def
                        ARM_H.isValidVTableRoot_def) apply (case_tac "isArchCap_tag (cap_get_tag cap')") apply (clarsimp simp: cap_get_tag_isCap cap_get_tag_isCap_ArchObject) apply (case_tac "cap_get_tag cap' = scast cap_page_directory_cap") apply (clarsimp split: arch_capability.split simp: isCap_simps) apply (clarsimp simp: ccap_relation_def map_option_Some_eq2
                          cap_page_directory_cap_lift cap_to_H_def) apply (clarsimp split: if_split) apply (clarsimp simp: cap_get_tag_isCap cap_get_tag_isCap_ArchObject) apply (simp split: arch_capability.split_asm add: isCap_simps) apply (case_tac "cap_get_tag cap' = scast cap_page_directory_cap") apply (clarsimp simp: cap_page_directory_cap_def isArchCap_tag_def2) apply (clarsimp simp: cap_get_tag_isCap split: capability.split_asm) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccap_relation cap cap' \<Longrightarrow> isValidVTableRoot_C cap' = isValidVTableRoot cap proof (prove)
goal (1 subgoal):
 1. ccap_relation cap cap' \<Longrightarrow> (cap_get_tag cap' = SCAST(32 signed \<rightarrow> 32) cap_page_directory_cap \<and> to_bool (capPDIsMapped_CL (cap_page_directory_cap_lift cap'))) = (case cap of capability.ArchObjectCap (arch_capability.PageDirectoryCap x None) \<Rightarrow> False | capability.ArchObjectCap (arch_capability.PageDirectoryCap x (Some xa)) \<Rightarrow> True | capability.ArchObjectCap _ \<Rightarrow> False | _ \<Rightarrow> False) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ccap_relation cap cap'; isArchCap_tag (cap_get_tag cap')\<rbrakk> \<Longrightarrow> (cap_get_tag cap' = SCAST(32 signed \<rightarrow> 32) cap_page_directory_cap \<and> to_bool (capPDIsMapped_CL (cap_page_directory_cap_lift cap'))) = (case cap of capability.ArchObjectCap (arch_capability.PageDirectoryCap x None) \<Rightarrow> False | capability.ArchObjectCap (arch_capability.PageDirectoryCap x (Some xa)) \<Rightarrow> True | capability.ArchObjectCap _ \<Rightarrow> False | _ \<Rightarrow> False)
 2. \<lbrakk>ccap_relation cap cap'; \<not> isArchCap_tag (cap_get_tag cap')\<rbrakk> \<Longrightarrow> (cap_get_tag cap' = SCAST(32 signed \<rightarrow> 32) cap_page_directory_cap \<and> to_bool (capPDIsMapped_CL (cap_page_directory_cap_lift cap'))) = (case cap of capability.ArchObjectCap (arch_capability.PageDirectoryCap x None) \<Rightarrow> False | capability.ArchObjectCap (arch_capability.PageDirectoryCap x (Some xa)) \<Rightarrow> True | capability.ArchObjectCap _ \<Rightarrow> False | _ \<Rightarrow> False) proof (prove)
goal (2 subgoals):
 1. \<And>arch_cap. \<lbrakk>ccap_relation (capability.ArchObjectCap arch_cap) cap'; cap = capability.ArchObjectCap arch_cap\<rbrakk> \<Longrightarrow> (isPageDirectoryCap arch_cap \<and> to_bool (capPDIsMapped_CL (cap_page_directory_cap_lift cap'))) = (case arch_cap of arch_capability.PageDirectoryCap x None \<Rightarrow> False | arch_capability.PageDirectoryCap x (Some xaa) \<Rightarrow> True | _ \<Rightarrow> False)
 2. \<lbrakk>ccap_relation cap cap'; \<not> isArchCap_tag (cap_get_tag cap')\<rbrakk> \<Longrightarrow> (cap_get_tag cap' = SCAST(32 signed \<rightarrow> 32) cap_page_directory_cap \<and> to_bool (capPDIsMapped_CL (cap_page_directory_cap_lift cap'))) = (case cap of capability.ArchObjectCap (arch_capability.PageDirectoryCap x None) \<Rightarrow> False | capability.ArchObjectCap (arch_capability.PageDirectoryCap x (Some xa)) \<Rightarrow> True | capability.ArchObjectCap _ \<Rightarrow> False | _ \<Rightarrow> False) proof (prove)
goal (3 subgoals):
 1. \<And>arch_cap. \<lbrakk>ccap_relation (capability.ArchObjectCap arch_cap) cap'; cap = capability.ArchObjectCap arch_cap; cap_get_tag cap' = SCAST(32 signed \<rightarrow> 32) cap_page_directory_cap\<rbrakk> \<Longrightarrow> (isPageDirectoryCap arch_cap \<and> to_bool (capPDIsMapped_CL (cap_page_directory_cap_lift cap'))) = (case arch_cap of arch_capability.PageDirectoryCap x None \<Rightarrow> False | arch_capability.PageDirectoryCap x (Some xaa) \<Rightarrow> True | _ \<Rightarrow> False)
 2. \<And>arch_cap. \<lbrakk>ccap_relation (capability.ArchObjectCap arch_cap) cap'; cap = capability.ArchObjectCap arch_cap; cap_get_tag cap' \<noteq> SCAST(32 signed \<rightarrow> 32) cap_page_directory_cap\<rbrakk> \<Longrightarrow> (isPageDirectoryCap arch_cap \<and> to_bool (capPDIsMapped_CL (cap_page_directory_cap_lift cap'))) = (case arch_cap of arch_capability.PageDirectoryCap x None \<Rightarrow> False | arch_capability.PageDirectoryCap x (Some xaa) \<Rightarrow> True | _ \<Rightarrow> False)
 3. \<lbrakk>ccap_relation cap cap'; \<not> isArchCap_tag (cap_get_tag cap')\<rbrakk> \<Longrightarrow> (cap_get_tag cap' = SCAST(32 signed \<rightarrow> 32) cap_page_directory_cap \<and> to_bool (capPDIsMapped_CL (cap_page_directory_cap_lift cap'))) = (case cap of capability.ArchObjectCap (arch_capability.PageDirectoryCap x None) \<Rightarrow> False | capability.ArchObjectCap (arch_capability.PageDirectoryCap x (Some xa)) \<Rightarrow> True | capability.ArchObjectCap _ \<Rightarrow> False | _ \<Rightarrow> False) proof (prove)
goal (3 subgoals):
 1. \<And>x51 x52. \<lbrakk>ccap_relation (capability.ArchObjectCap (arch_capability.PageDirectoryCap x51 x52)) cap'; cap = capability.ArchObjectCap (arch_capability.PageDirectoryCap x51 x52); cap_get_tag cap' = SCAST(32 signed \<rightarrow> 32) cap_page_directory_cap\<rbrakk> \<Longrightarrow> to_bool (capPDIsMapped_CL (cap_page_directory_cap_lift cap')) = (case x52 of None \<Rightarrow> False | Some xa \<Rightarrow> True)
 2. \<And>arch_cap. \<lbrakk>ccap_relation (capability.ArchObjectCap arch_cap) cap'; cap = capability.ArchObjectCap arch_cap; cap_get_tag cap' \<noteq> SCAST(32 signed \<rightarrow> 32) cap_page_directory_cap\<rbrakk> \<Longrightarrow> (isPageDirectoryCap arch_cap \<and> to_bool (capPDIsMapped_CL (cap_page_directory_cap_lift cap'))) = (case arch_cap of arch_capability.PageDirectoryCap x None \<Rightarrow> False | arch_capability.PageDirectoryCap x (Some xaa) \<Rightarrow> True | _ \<Rightarrow> False)
 3. \<lbrakk>ccap_relation cap cap'; \<not> isArchCap_tag (cap_get_tag cap')\<rbrakk> \<Longrightarrow> (cap_get_tag cap' = SCAST(32 signed \<rightarrow> 32) cap_page_directory_cap \<and> to_bool (capPDIsMapped_CL (cap_page_directory_cap_lift cap'))) = (case cap of capability.ArchObjectCap (arch_capability.PageDirectoryCap x None) \<Rightarrow> False | capability.ArchObjectCap (arch_capability.PageDirectoryCap x (Some xa)) \<Rightarrow> True | capability.ArchObjectCap _ \<Rightarrow> False | _ \<Rightarrow> False) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>cap = capability.ArchObjectCap (arch_capability.PageDirectoryCap (capPDBasePtr_CL (cap_page_directory_cap_lift cap')) (if to_bool (capPDIsMapped_CL (cap_page_directory_cap_lift cap')) then Some (capPDMappedASID_CL (cap_page_directory_cap_lift cap')) else None)); cap_lift cap' = Some (Cap_page_directory_cap (cap_page_directory_cap_lift cap'))\<rbrakk> \<Longrightarrow> to_bool (capPDIsMapped_CL (cap_page_directory_cap_lift cap')) = (case if to_bool (capPDIsMapped_CL (cap_page_directory_cap_lift cap')) then Some (capPDMappedASID_CL (cap_page_directory_cap_lift cap')) else None of None \<Rightarrow> False | Some xa \<Rightarrow> True)
 2. \<And>arch_cap. \<lbrakk>ccap_relation (capability.ArchObjectCap arch_cap) cap'; cap = capability.ArchObjectCap arch_cap; cap_get_tag cap' \<noteq> SCAST(32 signed \<rightarrow> 32) cap_page_directory_cap\<rbrakk> \<Longrightarrow> (isPageDirectoryCap arch_cap \<and> to_bool (capPDIsMapped_CL (cap_page_directory_cap_lift cap'))) = (case arch_cap of arch_capability.PageDirectoryCap x None \<Rightarrow> False | arch_capability.PageDirectoryCap x (Some xaa) \<Rightarrow> True | _ \<Rightarrow> False)
 3. \<lbrakk>ccap_relation cap cap'; \<not> isArchCap_tag (cap_get_tag cap')\<rbrakk> \<Longrightarrow> (cap_get_tag cap' = SCAST(32 signed \<rightarrow> 32) cap_page_directory_cap \<and> to_bool (capPDIsMapped_CL (cap_page_directory_cap_lift cap'))) = (case cap of capability.ArchObjectCap (arch_capability.PageDirectoryCap x None) \<Rightarrow> False | capability.ArchObjectCap (arch_capability.PageDirectoryCap x (Some xa)) \<Rightarrow> True | capability.ArchObjectCap _ \<Rightarrow> False | _ \<Rightarrow> False) proof (prove)
goal (2 subgoals):
 1. \<And>arch_cap. \<lbrakk>ccap_relation (capability.ArchObjectCap arch_cap) cap'; cap = capability.ArchObjectCap arch_cap; cap_get_tag cap' \<noteq> SCAST(32 signed \<rightarrow> 32) cap_page_directory_cap\<rbrakk> \<Longrightarrow> (isPageDirectoryCap arch_cap \<and> to_bool (capPDIsMapped_CL (cap_page_directory_cap_lift cap'))) = (case arch_cap of arch_capability.PageDirectoryCap x None \<Rightarrow> False | arch_capability.PageDirectoryCap x (Some xaa) \<Rightarrow> True | _ \<Rightarrow> False)
 2. \<lbrakk>ccap_relation cap cap'; \<not> isArchCap_tag (cap_get_tag cap')\<rbrakk> \<Longrightarrow> (cap_get_tag cap' = SCAST(32 signed \<rightarrow> 32) cap_page_directory_cap \<and> to_bool (capPDIsMapped_CL (cap_page_directory_cap_lift cap'))) = (case cap of capability.ArchObjectCap (arch_capability.PageDirectoryCap x None) \<Rightarrow> False | capability.ArchObjectCap (arch_capability.PageDirectoryCap x (Some xa)) \<Rightarrow> True | capability.ArchObjectCap _ \<Rightarrow> False | _ \<Rightarrow> False) proof (prove)
goal (2 subgoals):
 1. \<And>arch_cap. \<lbrakk>ccap_relation (capability.ArchObjectCap arch_cap) cap'; cap = capability.ArchObjectCap arch_cap; \<not> isPageDirectoryCap arch_cap; case arch_cap of arch_capability.PageDirectoryCap x None \<Rightarrow> False | arch_capability.PageDirectoryCap x (Some xaa) \<Rightarrow> True | _ \<Rightarrow> False\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>ccap_relation cap cap'; \<not> isArchCap_tag (cap_get_tag cap')\<rbrakk> \<Longrightarrow> (cap_get_tag cap' = SCAST(32 signed \<rightarrow> 32) cap_page_directory_cap \<and> to_bool (capPDIsMapped_CL (cap_page_directory_cap_lift cap'))) = (case cap of capability.ArchObjectCap (arch_capability.PageDirectoryCap x None) \<Rightarrow> False | capability.ArchObjectCap (arch_capability.PageDirectoryCap x (Some xa)) \<Rightarrow> True | capability.ArchObjectCap _ \<Rightarrow> False | _ \<Rightarrow> False) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ccap_relation cap cap'; \<not> isArchCap_tag (cap_get_tag cap')\<rbrakk> \<Longrightarrow> (cap_get_tag cap' = SCAST(32 signed \<rightarrow> 32) cap_page_directory_cap \<and> to_bool (capPDIsMapped_CL (cap_page_directory_cap_lift cap'))) = (case cap of capability.ArchObjectCap (arch_capability.PageDirectoryCap x None) \<Rightarrow> False | capability.ArchObjectCap (arch_capability.PageDirectoryCap x (Some xa)) \<Rightarrow> True | capability.ArchObjectCap _ \<Rightarrow> False | _ \<Rightarrow> False) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ccap_relation cap cap'; \<not> isArchCap_tag (cap_get_tag cap'); cap_get_tag cap' = SCAST(32 signed \<rightarrow> 32) cap_page_directory_cap\<rbrakk> \<Longrightarrow> (cap_get_tag cap' = SCAST(32 signed \<rightarrow> 32) cap_page_directory_cap \<and> to_bool (capPDIsMapped_CL (cap_page_directory_cap_lift cap'))) = (case cap of capability.ArchObjectCap (arch_capability.PageDirectoryCap x None) \<Rightarrow> False | capability.ArchObjectCap (arch_capability.PageDirectoryCap x (Some xa)) \<Rightarrow> True | capability.ArchObjectCap _ \<Rightarrow> False | _ \<Rightarrow> False)
 2. \<lbrakk>ccap_relation cap cap'; \<not> isArchCap_tag (cap_get_tag cap'); cap_get_tag cap' \<noteq> SCAST(32 signed \<rightarrow> 32) cap_page_directory_cap\<rbrakk> \<Longrightarrow> (cap_get_tag cap' = SCAST(32 signed \<rightarrow> 32) cap_page_directory_cap \<and> to_bool (capPDIsMapped_CL (cap_page_directory_cap_lift cap'))) = (case cap of capability.ArchObjectCap (arch_capability.PageDirectoryCap x None) \<Rightarrow> False | capability.ArchObjectCap (arch_capability.PageDirectoryCap x (Some xa)) \<Rightarrow> True | capability.ArchObjectCap _ \<Rightarrow> False | _ \<Rightarrow> False) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ccap_relation cap cap'; \<not> isArchCap_tag (cap_get_tag cap'); cap_get_tag cap' \<noteq> SCAST(32 signed \<rightarrow> 32) cap_page_directory_cap\<rbrakk> \<Longrightarrow> (cap_get_tag cap' = SCAST(32 signed \<rightarrow> 32) cap_page_directory_cap \<and> to_bool (capPDIsMapped_CL (cap_page_directory_cap_lift cap'))) = (case cap of capability.ArchObjectCap (arch_capability.PageDirectoryCap x None) \<Rightarrow> False | capability.ArchObjectCap (arch_capability.PageDirectoryCap x (Some xa)) \<Rightarrow> True | capability.ArchObjectCap _ \<Rightarrow> False | _ \<Rightarrow> False) proof (prove)
goal:
No subgoals!