theory VSpace_C

lemma generic_frame_mapped_address:
  "\<lbrakk> cap_to_H a = capability.ArchObjectCap (arch_capability.PageCap d v0 v1 v2 v3);
     cap_lift (cte_C.cap_C cte') = Some a;
     cl_valid_cte \<lparr>cap_CL = a, cteMDBNode_CL = mdb_node_lift (cteMDBNode_C cte')\<rparr>;
     generic_frame_cap_set_capFMappedAddress_CL (Some a) (scast asidInvalid) 0 = Some cap';
    cap_lift (cte_C.cap_C cte'a) = Some cap'\<rbrakk>
  \<Longrightarrow> ArchObjectCap (PageCap d v0 v1 v2 None) = cap_to_H cap' \<and> c_valid_cap (cte_C.cap_C cte'a)" apply (cases cte') apply (cases cte'a) apply (clarsimp simp: cl_valid_cte_def) apply (frule (1) cap_to_H_PageCap_tag) apply (erule disjE) apply (simp add: cap_frame_cap_lift) apply (simp add: generic_frame_cap_set_capFMappedAddress_CL_def) apply (clarsimp simp: cap_to_H_def) apply (simp add: asidInvalid_def split: if_split) apply (simp add: c_valid_cap_def cl_valid_cap_def) apply (simp add: cap_small_frame_cap_lift) apply (simp add: generic_frame_cap_set_capFMappedAddress_CL_def) apply (clarsimp simp: cap_to_H_def) apply (simp add: asidInvalid_def split: if_split) apply (simp add: c_valid_cap_def cl_valid_cap_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cap_to_H a = capability.ArchObjectCap (arch_capability.PageCap d v0 v1 v2 v3); cap_lift (cte_C.cap_C cte') = Some a; cl_valid_cte \<lparr>cap_CL = a, cteMDBNode_CL = mdb_node_lift (cteMDBNode_C cte')\<rparr>; generic_frame_cap_set_capFMappedAddress_CL (Some a) (SCAST(32 signed \<rightarrow> 32) asidInvalid) 0 = Some cap'; cap_lift (cte_C.cap_C cte'a) = Some cap'\<rbrakk> \<Longrightarrow> capability.ArchObjectCap (arch_capability.PageCap d v0 v1 v2 None) = cap_to_H cap' \<and> c_valid_cap (cte_C.cap_C cte'a) proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2. \<lbrakk>cap_to_H a = capability.ArchObjectCap (arch_capability.PageCap d v0 v1 v2 v3); cap_lift (cte_C.cap_C cte') = Some a; cl_valid_cte \<lparr>cap_CL = a, cteMDBNode_CL = mdb_node_lift (cteMDBNode_C cte')\<rparr>; generic_frame_cap_set_capFMappedAddress_CL (Some a) (SCAST(32 signed \<rightarrow> 32) asidInvalid) 0 = Some cap'; cap_lift (cte_C.cap_C cte'a) = Some cap'; cte' = cte_C x1 x2\<rbrakk> \<Longrightarrow> capability.ArchObjectCap (arch_capability.PageCap d v0 v1 v2 None) = cap_to_H cap' \<and> c_valid_cap (cte_C.cap_C cte'a) proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2 x1a x2a. \<lbrakk>cap_to_H a = capability.ArchObjectCap (arch_capability.PageCap d v0 v1 v2 v3); cap_lift (cte_C.cap_C cte') = Some a; cl_valid_cte \<lparr>cap_CL = a, cteMDBNode_CL = mdb_node_lift (cteMDBNode_C cte')\<rparr>; generic_frame_cap_set_capFMappedAddress_CL (Some a) (SCAST(32 signed \<rightarrow> 32) asidInvalid) 0 = Some cap'; cap_lift (cte_C.cap_C cte'a) = Some cap'; cte' = cte_C x1 x2; cte'a = cte_C x1a x2a\<rbrakk> \<Longrightarrow> capability.ArchObjectCap (arch_capability.PageCap d v0 v1 v2 None) = cap_to_H cap' \<and> c_valid_cap (cte_C.cap_C cte'a) proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2 x1a x2a. \<lbrakk>cap_to_H a = capability.ArchObjectCap (arch_capability.PageCap d v0 v1 v2 v3); cap_lift x1 = Some a; cl_valid_cap a; generic_frame_cap_set_capFMappedAddress_CL (Some a) (SCAST(32 signed \<rightarrow> 32) asidInvalid) 0 = Some cap'; cap_lift x1a = Some cap'; cte' = cte_C x1 x2; cte'a = cte_C x1a x2a\<rbrakk> \<Longrightarrow> capability.ArchObjectCap (arch_capability.PageCap d v0 v1 v2 None) = cap_to_H cap' \<and> c_valid_cap x1a proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2 x1a x2a. \<lbrakk>cap_to_H a = capability.ArchObjectCap (arch_capability.PageCap d v0 v1 v2 v3); cap_lift x1 = Some a; cl_valid_cap a; generic_frame_cap_set_capFMappedAddress_CL (Some a) (SCAST(32 signed \<rightarrow> 32) asidInvalid) 0 = Some cap'; cap_lift x1a = Some cap'; cte' = cte_C x1 x2; cte'a = cte_C x1a x2a; cap_get_tag x1 = SCAST(32 signed \<rightarrow> 32) cap_frame_cap \<or> cap_get_tag x1 = SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap\<rbrakk> \<Longrightarrow> capability.ArchObjectCap (arch_capability.PageCap d v0 v1 v2 None) = cap_to_H cap' \<and> c_valid_cap x1a proof (prove)
goal (2 subgoals):
 1. \<And>x1 x2 x1a x2a. \<lbrakk>cap_to_H a = capability.ArchObjectCap (arch_capability.PageCap d v0 v1 v2 v3); cap_lift x1 = Some a; cl_valid_cap a; generic_frame_cap_set_capFMappedAddress_CL (Some a) (SCAST(32 signed \<rightarrow> 32) asidInvalid) 0 = Some cap'; cap_lift x1a = Some cap'; cte' = cte_C x1 x2; cte'a = cte_C x1a x2a; cap_get_tag x1 = SCAST(32 signed \<rightarrow> 32) cap_frame_cap\<rbrakk> \<Longrightarrow> capability.ArchObjectCap (arch_capability.PageCap d v0 v1 v2 None) = cap_to_H cap' \<and> c_valid_cap x1a
 2. \<And>x1 x2 x1a x2a. \<lbrakk>cap_to_H a = capability.ArchObjectCap (arch_capability.PageCap d v0 v1 v2 v3); cap_lift x1 = Some a; cl_valid_cap a; generic_frame_cap_set_capFMappedAddress_CL (Some a) (SCAST(32 signed \<rightarrow> 32) asidInvalid) 0 = Some cap'; cap_lift x1a = Some cap'; cte' = cte_C x1 x2; cte'a = cte_C x1a x2a; cap_get_tag x1 = SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap\<rbrakk> \<Longrightarrow> capability.ArchObjectCap (arch_capability.PageCap d v0 v1 v2 None) = cap_to_H cap' \<and> c_valid_cap x1a proof (prove)
goal (2 subgoals):
 1. \<And>x1 x2 x1a x2a. \<lbrakk>cap_to_H (Cap_frame_cap (cap_frame_cap_lift x1)) = capability.ArchObjectCap (arch_capability.PageCap d v0 v1 v2 v3); cap_lift x1 = Some (Cap_frame_cap (cap_frame_cap_lift x1)); cl_valid_cap (Cap_frame_cap (cap_frame_cap_lift x1)); generic_frame_cap_set_capFMappedAddress_CL (Some (Cap_frame_cap (cap_frame_cap_lift x1))) (SCAST(32 signed \<rightarrow> 32) asidInvalid) 0 = Some cap'; cap_lift x1a = Some cap'; cte' = cte_C x1 x2; cte'a = cte_C x1a x2a; a = Cap_frame_cap (cap_frame_cap_lift x1)\<rbrakk> \<Longrightarrow> capability.ArchObjectCap (arch_capability.PageCap d v0 v1 v2 None) = cap_to_H cap' \<and> c_valid_cap x1a
 2. \<And>x1 x2 x1a x2a. \<lbrakk>cap_to_H a = capability.ArchObjectCap (arch_capability.PageCap d v0 v1 v2 v3); cap_lift x1 = Some a; cl_valid_cap a; generic_frame_cap_set_capFMappedAddress_CL (Some a) (SCAST(32 signed \<rightarrow> 32) asidInvalid) 0 = Some cap'; cap_lift x1a = Some cap'; cte' = cte_C x1 x2; cte'a = cte_C x1a x2a; cap_get_tag x1 = SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap\<rbrakk> \<Longrightarrow> capability.ArchObjectCap (arch_capability.PageCap d v0 v1 v2 None) = cap_to_H cap' \<and> c_valid_cap x1a proof (prove)
goal (2 subgoals):
 1. \<And>x1 x2 x1a x2a. \<lbrakk>cap_to_H (Cap_frame_cap (cap_frame_cap_lift x1)) = capability.ArchObjectCap (arch_capability.PageCap d v0 v1 v2 v3); cap_lift x1 = Some (Cap_frame_cap (cap_frame_cap_lift x1)); cl_valid_cap (Cap_frame_cap (cap_frame_cap_lift x1)); Cap_frame_cap (cap_frame_cap_lift x1\<lparr>cap_frame_cap_CL.capFMappedASIDHigh_CL := (SCAST(32 signed \<rightarrow> 32) asidInvalid >> local.asid_low_bits) && mask local.asid_high_bits, cap_frame_cap_CL.capFMappedASIDLow_CL := SCAST(32 signed \<rightarrow> 32) asidInvalid && mask local.asid_low_bits, cap_frame_cap_CL.capFMappedAddress_CL := 0\<rparr>) = cap'; cap_lift x1a = Some cap'; cte' = cte_C x1 x2; cte'a = cte_C x1a x2a; a = Cap_frame_cap (cap_frame_cap_lift x1)\<rbrakk> \<Longrightarrow> capability.ArchObjectCap (arch_capability.PageCap d v0 v1 v2 None) = cap_to_H cap' \<and> c_valid_cap x1a
 2. \<And>x1 x2 x1a x2a. \<lbrakk>cap_to_H a = capability.ArchObjectCap (arch_capability.PageCap d v0 v1 v2 v3); cap_lift x1 = Some a; cl_valid_cap a; generic_frame_cap_set_capFMappedAddress_CL (Some a) (SCAST(32 signed \<rightarrow> 32) asidInvalid) 0 = Some cap'; cap_lift x1a = Some cap'; cte' = cte_C x1 x2; cte'a = cte_C x1a x2a; cap_get_tag x1 = SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap\<rbrakk> \<Longrightarrow> capability.ArchObjectCap (arch_capability.PageCap d v0 v1 v2 None) = cap_to_H cap' \<and> c_valid_cap x1a proof (prove)
goal (2 subgoals):
 1. \<And>x1 x2 x1a x2a. \<lbrakk>cap_lift x1 = Some (Cap_frame_cap (cap_frame_cap_lift x1)); cl_valid_cap (Cap_frame_cap (cap_frame_cap_lift x1)); cap_lift x1a = Some (Cap_frame_cap (cap_frame_cap_lift x1\<lparr>cap_frame_cap_CL.capFMappedASIDHigh_CL := (SCAST(32 signed \<rightarrow> 32) asidInvalid >> local.asid_low_bits) && mask local.asid_high_bits, cap_frame_cap_CL.capFMappedASIDLow_CL := SCAST(32 signed \<rightarrow> 32) asidInvalid && mask local.asid_low_bits, cap_frame_cap_CL.capFMappedAddress_CL := 0\<rparr>)); cte' = cte_C x1 x2; cte'a = cte_C x1a x2a; a = Cap_frame_cap (cap_frame_cap_lift x1); cap' = Cap_frame_cap (cap_frame_cap_lift x1\<lparr>cap_frame_cap_CL.capFMappedASIDHigh_CL := (SCAST(32 signed \<rightarrow> 32) asidInvalid >> local.asid_low_bits) && mask local.asid_high_bits, cap_frame_cap_CL.capFMappedASIDLow_CL := SCAST(32 signed \<rightarrow> 32) asidInvalid && mask local.asid_low_bits, cap_frame_cap_CL.capFMappedAddress_CL := 0\<rparr>); d = to_bool (cap_frame_cap_CL.capFIsDevice_CL (cap_frame_cap_lift x1)); v0 = cap_frame_cap_CL.capFBasePtr_CL (cap_frame_cap_lift x1); v1 = vmrights_to_H (cap_frame_cap_CL.capFVMRights_CL (cap_frame_cap_lift x1)); v2 = framesize_to_H (capFSize_CL (cap_frame_cap_lift x1)); v3 = (if cap_frame_cap_CL.capFMappedASIDHigh_CL (cap_frame_cap_lift x1) = 0 \<and> cap_frame_cap_CL.capFMappedASIDLow_CL (cap_frame_cap_lift x1) = 0 then None else Some ((cap_frame_cap_CL.capFMappedASIDHigh_CL (cap_frame_cap_lift x1) << local.asidLowBits) + cap_frame_cap_CL.capFMappedASIDLow_CL (cap_frame_cap_lift x1), cap_frame_cap_CL.capFMappedAddress_CL (cap_frame_cap_lift x1)))\<rbrakk> \<Longrightarrow> None = (if (SCAST(32 signed \<rightarrow> 32) asidInvalid >> local.asid_low_bits) && mask local.asid_high_bits = 0 \<and> SCAST(32 signed \<rightarrow> 32) asidInvalid && mask local.asid_low_bits = 0 then None else Some ((cap_frame_cap_CL.capFMappedASIDHigh_CL (cap_frame_cap_lift x1\<lparr>cap_frame_cap_CL.capFMappedASIDHigh_CL := (SCAST(32 signed \<rightarrow> 32) asidInvalid >> local.asid_low_bits) && mask local.asid_high_bits, cap_frame_cap_CL.capFMappedASIDLow_CL := SCAST(32 signed \<rightarrow> 32) asidInvalid && mask local.asid_low_bits, cap_frame_cap_CL.capFMappedAddress_CL := 0\<rparr>) << local.asidLowBits) + cap_frame_cap_CL.capFMappedASIDLow_CL (cap_frame_cap_lift x1\<lparr>cap_frame_cap_CL.capFMappedASIDHigh_CL := (SCAST(32 signed \<rightarrow> 32) asidInvalid >> local.asid_low_bits) && mask local.asid_high_bits, cap_frame_cap_CL.capFMappedASIDLow_CL := SCAST(32 signed \<rightarrow> 32) asidInvalid && mask local.asid_low_bits, cap_frame_cap_CL.capFMappedAddress_CL := 0\<rparr>), cap_frame_cap_CL.capFMappedAddress_CL (cap_frame_cap_lift x1\<lparr>cap_frame_cap_CL.capFMappedASIDHigh_CL := (SCAST(32 signed \<rightarrow> 32) asidInvalid >> local.asid_low_bits) && mask local.asid_high_bits, cap_frame_cap_CL.capFMappedASIDLow_CL := SCAST(32 signed \<rightarrow> 32) asidInvalid && mask local.asid_low_bits, cap_frame_cap_CL.capFMappedAddress_CL := 0\<rparr>))) \<and> c_valid_cap x1a
 2. \<And>x1 x2 x1a x2a. \<lbrakk>cap_to_H a = capability.ArchObjectCap (arch_capability.PageCap d v0 v1 v2 v3); cap_lift x1 = Some a; cl_valid_cap a; generic_frame_cap_set_capFMappedAddress_CL (Some a) (SCAST(32 signed \<rightarrow> 32) asidInvalid) 0 = Some cap'; cap_lift x1a = Some cap'; cte' = cte_C x1 x2; cte'a = cte_C x1a x2a; cap_get_tag x1 = SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap\<rbrakk> \<Longrightarrow> capability.ArchObjectCap (arch_capability.PageCap d v0 v1 v2 None) = cap_to_H cap' \<and> c_valid_cap x1a proof (prove)
goal (2 subgoals):
 1. \<And>x1 x2 x1a x2a. \<lbrakk>cap_lift x1 = Some (Cap_frame_cap (cap_frame_cap_lift x1)); cl_valid_cap (Cap_frame_cap (cap_frame_cap_lift x1)); cap_lift x1a = Some (Cap_frame_cap (cap_frame_cap_lift x1\<lparr>cap_frame_cap_CL.capFMappedASIDHigh_CL := 0, cap_frame_cap_CL.capFMappedASIDLow_CL := 0, cap_frame_cap_CL.capFMappedAddress_CL := 0\<rparr>)); cte' = cte_C x1 x2; cte'a = cte_C x1a x2a; a = Cap_frame_cap (cap_frame_cap_lift x1); cap' = Cap_frame_cap (cap_frame_cap_lift x1\<lparr>cap_frame_cap_CL.capFMappedASIDHigh_CL := 0, cap_frame_cap_CL.capFMappedASIDLow_CL := 0, cap_frame_cap_CL.capFMappedAddress_CL := 0\<rparr>); d = to_bool (cap_frame_cap_CL.capFIsDevice_CL (cap_frame_cap_lift x1)); v0 = cap_frame_cap_CL.capFBasePtr_CL (cap_frame_cap_lift x1); v1 = vmrights_to_H (cap_frame_cap_CL.capFVMRights_CL (cap_frame_cap_lift x1)); v2 = framesize_to_H (capFSize_CL (cap_frame_cap_lift x1)); v3 = (if cap_frame_cap_CL.capFMappedASIDHigh_CL (cap_frame_cap_lift x1) = 0 \<and> cap_frame_cap_CL.capFMappedASIDLow_CL (cap_frame_cap_lift x1) = 0 then None else Some ((cap_frame_cap_CL.capFMappedASIDHigh_CL (cap_frame_cap_lift x1) << local.asidLowBits) + cap_frame_cap_CL.capFMappedASIDLow_CL (cap_frame_cap_lift x1), cap_frame_cap_CL.capFMappedAddress_CL (cap_frame_cap_lift x1)))\<rbrakk> \<Longrightarrow> c_valid_cap x1a
 2. \<And>x1 x2 x1a x2a. \<lbrakk>cap_to_H a = capability.ArchObjectCap (arch_capability.PageCap d v0 v1 v2 v3); cap_lift x1 = Some a; cl_valid_cap a; generic_frame_cap_set_capFMappedAddress_CL (Some a) (SCAST(32 signed \<rightarrow> 32) asidInvalid) 0 = Some cap'; cap_lift x1a = Some cap'; cte' = cte_C x1 x2; cte'a = cte_C x1a x2a; cap_get_tag x1 = SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap\<rbrakk> \<Longrightarrow> capability.ArchObjectCap (arch_capability.PageCap d v0 v1 v2 None) = cap_to_H cap' \<and> c_valid_cap x1a proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2 x1a x2a. \<lbrakk>cap_to_H a = capability.ArchObjectCap (arch_capability.PageCap d v0 v1 v2 v3); cap_lift x1 = Some a; cl_valid_cap a; generic_frame_cap_set_capFMappedAddress_CL (Some a) (SCAST(32 signed \<rightarrow> 32) asidInvalid) 0 = Some cap'; cap_lift x1a = Some cap'; cte' = cte_C x1 x2; cte'a = cte_C x1a x2a; cap_get_tag x1 = SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap\<rbrakk> \<Longrightarrow> capability.ArchObjectCap (arch_capability.PageCap d v0 v1 v2 None) = cap_to_H cap' \<and> c_valid_cap x1a proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2 x1a x2a. \<lbrakk>cap_to_H (Cap_small_frame_cap (cap_small_frame_cap_lift x1)) = capability.ArchObjectCap (arch_capability.PageCap d v0 v1 v2 v3); cap_lift x1 = Some (Cap_small_frame_cap (cap_small_frame_cap_lift x1)); cl_valid_cap (Cap_small_frame_cap (cap_small_frame_cap_lift x1)); generic_frame_cap_set_capFMappedAddress_CL (Some (Cap_small_frame_cap (cap_small_frame_cap_lift x1))) (SCAST(32 signed \<rightarrow> 32) asidInvalid) 0 = Some cap'; cap_lift x1a = Some cap'; cte' = cte_C x1 x2; cte'a = cte_C x1a x2a; a = Cap_small_frame_cap (cap_small_frame_cap_lift x1)\<rbrakk> \<Longrightarrow> capability.ArchObjectCap (arch_capability.PageCap d v0 v1 v2 None) = cap_to_H cap' \<and> c_valid_cap x1a proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2 x1a x2a. \<lbrakk>cap_to_H (Cap_small_frame_cap (cap_small_frame_cap_lift x1)) = capability.ArchObjectCap (arch_capability.PageCap d v0 v1 v2 v3); cap_lift x1 = Some (Cap_small_frame_cap (cap_small_frame_cap_lift x1)); cl_valid_cap (Cap_small_frame_cap (cap_small_frame_cap_lift x1)); Cap_small_frame_cap (cap_small_frame_cap_lift x1\<lparr>cap_small_frame_cap_CL.capFMappedASIDHigh_CL := (SCAST(32 signed \<rightarrow> 32) asidInvalid >> local.asid_low_bits) && mask local.asid_high_bits, cap_small_frame_cap_CL.capFMappedASIDLow_CL := SCAST(32 signed \<rightarrow> 32) asidInvalid && mask local.asid_low_bits, cap_small_frame_cap_CL.capFMappedAddress_CL := 0\<rparr>) = cap'; cap_lift x1a = Some cap'; cte' = cte_C x1 x2; cte'a = cte_C x1a x2a; a = Cap_small_frame_cap (cap_small_frame_cap_lift x1)\<rbrakk> \<Longrightarrow> capability.ArchObjectCap (arch_capability.PageCap d v0 v1 v2 None) = cap_to_H cap' \<and> c_valid_cap x1a proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2 x1a x2a. \<lbrakk>cap_lift x1 = Some (Cap_small_frame_cap (cap_small_frame_cap_lift x1)); cl_valid_cap (Cap_small_frame_cap (cap_small_frame_cap_lift x1)); cap_lift x1a = Some (Cap_small_frame_cap (cap_small_frame_cap_lift x1\<lparr>cap_small_frame_cap_CL.capFMappedASIDHigh_CL := (SCAST(32 signed \<rightarrow> 32) asidInvalid >> local.asid_low_bits) && mask local.asid_high_bits, cap_small_frame_cap_CL.capFMappedASIDLow_CL := SCAST(32 signed \<rightarrow> 32) asidInvalid && mask local.asid_low_bits, cap_small_frame_cap_CL.capFMappedAddress_CL := 0\<rparr>)); cte' = cte_C x1 x2; cte'a = cte_C x1a x2a; a = Cap_small_frame_cap (cap_small_frame_cap_lift x1); cap' = Cap_small_frame_cap (cap_small_frame_cap_lift x1\<lparr>cap_small_frame_cap_CL.capFMappedASIDHigh_CL := (SCAST(32 signed \<rightarrow> 32) asidInvalid >> local.asid_low_bits) && mask local.asid_high_bits, cap_small_frame_cap_CL.capFMappedASIDLow_CL := SCAST(32 signed \<rightarrow> 32) asidInvalid && mask local.asid_low_bits, cap_small_frame_cap_CL.capFMappedAddress_CL := 0\<rparr>); d = to_bool (cap_small_frame_cap_CL.capFIsDevice_CL (cap_small_frame_cap_lift x1)); v0 = cap_small_frame_cap_CL.capFBasePtr_CL (cap_small_frame_cap_lift x1); v1 = vmrights_to_H (cap_small_frame_cap_CL.capFVMRights_CL (cap_small_frame_cap_lift x1)); v2 = Wellformed_C.ARMSmallPage; v3 = (if cap_small_frame_cap_CL.capFMappedASIDHigh_CL (cap_small_frame_cap_lift x1) = 0 \<and> cap_small_frame_cap_CL.capFMappedASIDLow_CL (cap_small_frame_cap_lift x1) = 0 then None else Some ((cap_small_frame_cap_CL.capFMappedASIDHigh_CL (cap_small_frame_cap_lift x1) << local.asidLowBits) + cap_small_frame_cap_CL.capFMappedASIDLow_CL (cap_small_frame_cap_lift x1), cap_small_frame_cap_CL.capFMappedAddress_CL (cap_small_frame_cap_lift x1)))\<rbrakk> \<Longrightarrow> None = (if (SCAST(32 signed \<rightarrow> 32) asidInvalid >> local.asid_low_bits) && mask local.asid_high_bits = 0 \<and> SCAST(32 signed \<rightarrow> 32) asidInvalid && mask local.asid_low_bits = 0 then None else Some ((cap_small_frame_cap_CL.capFMappedASIDHigh_CL (cap_small_frame_cap_lift x1\<lparr>cap_small_frame_cap_CL.capFMappedASIDHigh_CL := (SCAST(32 signed \<rightarrow> 32) asidInvalid >> local.asid_low_bits) && mask local.asid_high_bits, cap_small_frame_cap_CL.capFMappedASIDLow_CL := SCAST(32 signed \<rightarrow> 32) asidInvalid && mask local.asid_low_bits, cap_small_frame_cap_CL.capFMappedAddress_CL := 0\<rparr>) << local.asidLowBits) + cap_small_frame_cap_CL.capFMappedASIDLow_CL (cap_small_frame_cap_lift x1\<lparr>cap_small_frame_cap_CL.capFMappedASIDHigh_CL := (SCAST(32 signed \<rightarrow> 32) asidInvalid >> local.asid_low_bits) && mask local.asid_high_bits, cap_small_frame_cap_CL.capFMappedASIDLow_CL := SCAST(32 signed \<rightarrow> 32) asidInvalid && mask local.asid_low_bits, cap_small_frame_cap_CL.capFMappedAddress_CL := 0\<rparr>), cap_small_frame_cap_CL.capFMappedAddress_CL (cap_small_frame_cap_lift x1\<lparr>cap_small_frame_cap_CL.capFMappedASIDHigh_CL := (SCAST(32 signed \<rightarrow> 32) asidInvalid >> local.asid_low_bits) && mask local.asid_high_bits, cap_small_frame_cap_CL.capFMappedASIDLow_CL := SCAST(32 signed \<rightarrow> 32) asidInvalid && mask local.asid_low_bits, cap_small_frame_cap_CL.capFMappedAddress_CL := 0\<rparr>))) \<and> c_valid_cap x1a proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2 x1a x2a. \<lbrakk>cap_lift x1 = Some (Cap_small_frame_cap (cap_small_frame_cap_lift x1)); cl_valid_cap (Cap_small_frame_cap (cap_small_frame_cap_lift x1)); cap_lift x1a = Some (Cap_small_frame_cap (cap_small_frame_cap_lift x1\<lparr>cap_small_frame_cap_CL.capFMappedASIDHigh_CL := 0, cap_small_frame_cap_CL.capFMappedASIDLow_CL := 0, cap_small_frame_cap_CL.capFMappedAddress_CL := 0\<rparr>)); cte' = cte_C x1 x2; cte'a = cte_C x1a x2a; a = Cap_small_frame_cap (cap_small_frame_cap_lift x1); cap' = Cap_small_frame_cap (cap_small_frame_cap_lift x1\<lparr>cap_small_frame_cap_CL.capFMappedASIDHigh_CL := 0, cap_small_frame_cap_CL.capFMappedASIDLow_CL := 0, cap_small_frame_cap_CL.capFMappedAddress_CL := 0\<rparr>); d = to_bool (cap_small_frame_cap_CL.capFIsDevice_CL (cap_small_frame_cap_lift x1)); v0 = cap_small_frame_cap_CL.capFBasePtr_CL (cap_small_frame_cap_lift x1); v1 = vmrights_to_H (cap_small_frame_cap_CL.capFVMRights_CL (cap_small_frame_cap_lift x1)); v2 = Wellformed_C.ARMSmallPage; v3 = (if cap_small_frame_cap_CL.capFMappedASIDHigh_CL (cap_small_frame_cap_lift x1) = 0 \<and> cap_small_frame_cap_CL.capFMappedASIDLow_CL (cap_small_frame_cap_lift x1) = 0 then None else Some ((cap_small_frame_cap_CL.capFMappedASIDHigh_CL (cap_small_frame_cap_lift x1) << local.asidLowBits) + cap_small_frame_cap_CL.capFMappedASIDLow_CL (cap_small_frame_cap_lift x1), cap_small_frame_cap_CL.capFMappedAddress_CL (cap_small_frame_cap_lift x1)))\<rbrakk> \<Longrightarrow> c_valid_cap x1a proof (prove)
goal:
No subgoals!