theory VSpace_C

lemma ccap_relation_mapped_asid_0:
  "ccap_relation (ArchObjectCap (PageCap d v0 v1 v2 v3)) cap
  \<Longrightarrow> (generic_frame_cap_get_capFMappedASID_CL (cap_lift cap) \<noteq> 0 \<longrightarrow> v3 \<noteq> None) \<and>
     (generic_frame_cap_get_capFMappedASID_CL (cap_lift cap) = 0 \<longrightarrow> v3 = None)" apply (erule ccap_relationE) apply (drule sym, frule (1) cap_to_H_PageCap_tag) apply (rule conjI) apply (rule impI) apply (rule notI, erule notE) apply clarsimp apply (erule disjE) apply (clarsimp simp: cap_lift_frame_cap cap_to_H_def
                          generic_frame_cap_get_capFMappedASID_CL_def
                    split: if_split_asm) apply (clarsimp simp: cap_lift_small_frame_cap cap_to_H_def
                         generic_frame_cap_get_capFMappedASID_CL_def
                   split: if_split_asm) apply clarsimp apply (erule disjE) apply (rule ccontr) apply clarsimp apply (clarsimp simp: cap_lift_frame_cap cap_to_H_def
                         generic_frame_cap_get_capFMappedASID_CL_def
                   split: if_split_asm) apply (drule word_aligned_0_sum [where n=asid_low_bits]) apply fastforce apply (simp add: mask_def asid_low_bits_def word_and_le1) apply (simp add: asid_low_bits_def word_bits_def) apply clarsimp apply (drule word_shift_zero [where m=8]) apply (rule order_trans) apply (rule word_and_le1) apply (simp add: mask_def) apply (simp add: asid_low_bits_def word_bits_def) apply simp apply (rule ccontr) apply clarsimp apply (clarsimp simp: cap_lift_small_frame_cap cap_to_H_def
                        generic_frame_cap_get_capFMappedASID_CL_def
                  split: if_split_asm) apply (drule word_aligned_0_sum [where n=asid_low_bits]) apply fastforce apply (simp add: mask_def asid_low_bits_def word_and_le1) apply (simp add: asid_low_bits_def word_bits_def) apply clarsimp apply (drule word_shift_zero [where m=8]) apply (rule order_trans) apply (rule word_and_le1) apply (simp add: mask_def) apply (simp add: asid_low_bits_def word_bits_def) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccap_relation (capability.ArchObjectCap (arch_capability.PageCap d v0 v1 v2 v3)) cap \<Longrightarrow> (generic_frame_cap_get_capFMappedASID_CL (cap_lift cap) \<noteq> 0 \<longrightarrow> v3 \<noteq> None) \<and> (generic_frame_cap_get_capFMappedASID_CL (cap_lift cap) = 0 \<longrightarrow> v3 = None) proof (prove)
goal (1 subgoal):
 1. \<And>vl. \<lbrakk>cap_lift cap = Some vl; capability.ArchObjectCap (arch_capability.PageCap d v0 v1 v2 v3) = cap_to_H vl; c_valid_cap cap\<rbrakk> \<Longrightarrow> (generic_frame_cap_get_capFMappedASID_CL (cap_lift cap) \<noteq> 0 \<longrightarrow> v3 \<noteq> None) \<and> (generic_frame_cap_get_capFMappedASID_CL (cap_lift cap) = 0 \<longrightarrow> v3 = None) proof (prove)
goal (1 subgoal):
 1. \<And>vl. \<lbrakk>cap_lift cap = Some vl; c_valid_cap cap; cap_to_H vl = capability.ArchObjectCap (arch_capability.PageCap d v0 v1 v2 v3); cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_frame_cap \<or> cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap\<rbrakk> \<Longrightarrow> (generic_frame_cap_get_capFMappedASID_CL (cap_lift cap) \<noteq> 0 \<longrightarrow> v3 \<noteq> None) \<and> (generic_frame_cap_get_capFMappedASID_CL (cap_lift cap) = 0 \<longrightarrow> v3 = None) proof (prove)
goal (2 subgoals):
 1. \<And>vl. \<lbrakk>cap_lift cap = Some vl; c_valid_cap cap; cap_to_H vl = capability.ArchObjectCap (arch_capability.PageCap d v0 v1 v2 v3); cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_frame_cap \<or> cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap\<rbrakk> \<Longrightarrow> generic_frame_cap_get_capFMappedASID_CL (cap_lift cap) \<noteq> 0 \<longrightarrow> v3 \<noteq> None
 2. \<And>vl. \<lbrakk>cap_lift cap = Some vl; c_valid_cap cap; cap_to_H vl = capability.ArchObjectCap (arch_capability.PageCap d v0 v1 v2 v3); cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_frame_cap \<or> cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap\<rbrakk> \<Longrightarrow> generic_frame_cap_get_capFMappedASID_CL (cap_lift cap) = 0 \<longrightarrow> v3 = None proof (prove)
goal (2 subgoals):
 1. \<And>vl. \<lbrakk>cap_lift cap = Some vl; c_valid_cap cap; cap_to_H vl = capability.ArchObjectCap (arch_capability.PageCap d v0 v1 v2 v3); cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_frame_cap \<or> cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap; generic_frame_cap_get_capFMappedASID_CL (cap_lift cap) \<noteq> 0\<rbrakk> \<Longrightarrow> v3 \<noteq> None
 2. \<And>vl. \<lbrakk>cap_lift cap = Some vl; c_valid_cap cap; cap_to_H vl = capability.ArchObjectCap (arch_capability.PageCap d v0 v1 v2 v3); cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_frame_cap \<or> cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap\<rbrakk> \<Longrightarrow> generic_frame_cap_get_capFMappedASID_CL (cap_lift cap) = 0 \<longrightarrow> v3 = None proof (prove)
goal (2 subgoals):
 1. \<And>vl. \<lbrakk>cap_lift cap = Some vl; c_valid_cap cap; cap_to_H vl = capability.ArchObjectCap (arch_capability.PageCap d v0 v1 v2 v3); cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_frame_cap \<or> cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap; v3 = None\<rbrakk> \<Longrightarrow> generic_frame_cap_get_capFMappedASID_CL (cap_lift cap) = 0
 2. \<And>vl. \<lbrakk>cap_lift cap = Some vl; c_valid_cap cap; cap_to_H vl = capability.ArchObjectCap (arch_capability.PageCap d v0 v1 v2 v3); cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_frame_cap \<or> cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap\<rbrakk> \<Longrightarrow> generic_frame_cap_get_capFMappedASID_CL (cap_lift cap) = 0 \<longrightarrow> v3 = None proof (prove)
goal (2 subgoals):
 1. \<And>vl. \<lbrakk>cap_lift cap = Some vl; c_valid_cap cap; cap_to_H vl = capability.ArchObjectCap (arch_capability.PageCap d v0 v1 v2 None); cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_frame_cap \<or> cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap; v3 = None\<rbrakk> \<Longrightarrow> generic_frame_cap_get_capFMappedASID_CL (Some vl) = 0
 2. \<And>vl. \<lbrakk>cap_lift cap = Some vl; c_valid_cap cap; cap_to_H vl = capability.ArchObjectCap (arch_capability.PageCap d v0 v1 v2 v3); cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_frame_cap \<or> cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap\<rbrakk> \<Longrightarrow> generic_frame_cap_get_capFMappedASID_CL (cap_lift cap) = 0 \<longrightarrow> v3 = None proof (prove)
goal (3 subgoals):
 1. \<And>vl. \<lbrakk>cap_lift cap = Some vl; c_valid_cap cap; cap_to_H vl = capability.ArchObjectCap (arch_capability.PageCap d v0 v1 v2 None); v3 = None; cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_frame_cap\<rbrakk> \<Longrightarrow> generic_frame_cap_get_capFMappedASID_CL (Some vl) = 0
 2. \<And>vl. \<lbrakk>cap_lift cap = Some vl; c_valid_cap cap; cap_to_H vl = capability.ArchObjectCap (arch_capability.PageCap d v0 v1 v2 None); v3 = None; cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap\<rbrakk> \<Longrightarrow> generic_frame_cap_get_capFMappedASID_CL (Some vl) = 0
 3. \<And>vl. \<lbrakk>cap_lift cap = Some vl; c_valid_cap cap; cap_to_H vl = capability.ArchObjectCap (arch_capability.PageCap d v0 v1 v2 v3); cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_frame_cap \<or> cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap\<rbrakk> \<Longrightarrow> generic_frame_cap_get_capFMappedASID_CL (cap_lift cap) = 0 \<longrightarrow> v3 = None proof (prove)
goal (2 subgoals):
 1. \<And>vl. \<lbrakk>cap_lift cap = Some vl; c_valid_cap cap; cap_to_H vl = capability.ArchObjectCap (arch_capability.PageCap d v0 v1 v2 None); v3 = None; cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap\<rbrakk> \<Longrightarrow> generic_frame_cap_get_capFMappedASID_CL (Some vl) = 0
 2. \<And>vl. \<lbrakk>cap_lift cap = Some vl; c_valid_cap cap; cap_to_H vl = capability.ArchObjectCap (arch_capability.PageCap d v0 v1 v2 v3); cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_frame_cap \<or> cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap\<rbrakk> \<Longrightarrow> generic_frame_cap_get_capFMappedASID_CL (cap_lift cap) = 0 \<longrightarrow> v3 = None proof (prove)
goal (1 subgoal):
 1. \<And>vl. \<lbrakk>cap_lift cap = Some vl; c_valid_cap cap; cap_to_H vl = capability.ArchObjectCap (arch_capability.PageCap d v0 v1 v2 v3); cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_frame_cap \<or> cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap\<rbrakk> \<Longrightarrow> generic_frame_cap_get_capFMappedASID_CL (cap_lift cap) = 0 \<longrightarrow> v3 = None proof (prove)
goal (1 subgoal):
 1. \<And>vl. \<lbrakk>cap_lift cap = Some vl; c_valid_cap cap; cap_to_H vl = capability.ArchObjectCap (arch_capability.PageCap d v0 v1 v2 v3); cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_frame_cap \<or> cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap; generic_frame_cap_get_capFMappedASID_CL (Some vl) = 0\<rbrakk> \<Longrightarrow> v3 = None proof (prove)
goal (2 subgoals):
 1. \<And>vl. \<lbrakk>cap_lift cap = Some vl; c_valid_cap cap; cap_to_H vl = capability.ArchObjectCap (arch_capability.PageCap d v0 v1 v2 v3); generic_frame_cap_get_capFMappedASID_CL (Some vl) = 0; cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_frame_cap\<rbrakk> \<Longrightarrow> v3 = None
 2. \<And>vl. \<lbrakk>cap_lift cap = Some vl; c_valid_cap cap; cap_to_H vl = capability.ArchObjectCap (arch_capability.PageCap d v0 v1 v2 v3); generic_frame_cap_get_capFMappedASID_CL (Some vl) = 0; cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap\<rbrakk> \<Longrightarrow> v3 = None proof (prove)
goal (2 subgoals):
 1. \<And>vl. \<lbrakk>cap_lift cap = Some vl; c_valid_cap cap; cap_to_H vl = capability.ArchObjectCap (arch_capability.PageCap d v0 v1 v2 v3); generic_frame_cap_get_capFMappedASID_CL (Some vl) = 0; cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_frame_cap; v3 \<noteq> None\<rbrakk> \<Longrightarrow> False
 2. \<And>vl. \<lbrakk>cap_lift cap = Some vl; c_valid_cap cap; cap_to_H vl = capability.ArchObjectCap (arch_capability.PageCap d v0 v1 v2 v3); generic_frame_cap_get_capFMappedASID_CL (Some vl) = 0; cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap\<rbrakk> \<Longrightarrow> v3 = None proof (prove)
goal (2 subgoals):
 1. \<And>vl a b. \<lbrakk>cap_lift cap = Some vl; c_valid_cap cap; cap_to_H vl = capability.ArchObjectCap (arch_capability.PageCap d v0 v1 v2 (Some (a, b))); generic_frame_cap_get_capFMappedASID_CL (Some vl) = 0; cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_frame_cap; v3 = Some (a, b)\<rbrakk> \<Longrightarrow> False
 2. \<And>vl. \<lbrakk>cap_lift cap = Some vl; c_valid_cap cap; cap_to_H vl = capability.ArchObjectCap (arch_capability.PageCap d v0 v1 v2 v3); generic_frame_cap_get_capFMappedASID_CL (Some vl) = 0; cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap\<rbrakk> \<Longrightarrow> v3 = None proof (prove)
goal (2 subgoals):
 1. \<lbrakk>c_valid_cap cap; cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_frame_cap; v3 = Some (0, (cap_C.words_C cap.[Suc 0] << 14) && ~~ mask 14); d = to_bool ((cap_C.words_C cap.[0] >> 29) && 1); v0 = (cap_C.words_C cap.[0] << 10) && ~~ mask 14; v1 = vmrights_to_H ((cap_C.words_C cap.[Suc 0] >> 18) && mask 2); v2 = framesize_to_H ((cap_C.words_C cap.[Suc 0] >> 30) && mask 2); (cap_C.words_C cap.[0] >> 22) && mask 7 = 0 \<longrightarrow> (cap_C.words_C cap.[Suc 0] >> 20) && mask 10 \<noteq> 0; ((cap_C.words_C cap.[0] >> 22) && mask 7 << local.asid_low_bits) + ((cap_C.words_C cap.[Suc 0] >> 20) && mask 10) = 0\<rbrakk> \<Longrightarrow> False
 2. \<And>vl. \<lbrakk>cap_lift cap = Some vl; c_valid_cap cap; cap_to_H vl = capability.ArchObjectCap (arch_capability.PageCap d v0 v1 v2 v3); generic_frame_cap_get_capFMappedASID_CL (Some vl) = 0; cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap\<rbrakk> \<Longrightarrow> v3 = None proof (prove)
goal (5 subgoals):
 1. \<lbrakk>c_valid_cap cap; cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_frame_cap; v3 = Some (0, (cap_C.words_C cap.[Suc 0] << 14) && ~~ mask 14); d = to_bool ((cap_C.words_C cap.[0] >> 29) && 1); v0 = (cap_C.words_C cap.[0] << 10) && ~~ mask 14; v1 = vmrights_to_H ((cap_C.words_C cap.[Suc 0] >> 18) && mask 2); v2 = framesize_to_H ((cap_C.words_C cap.[Suc 0] >> 30) && mask 2); (cap_C.words_C cap.[0] >> 22) && mask 7 = 0 \<longrightarrow> (cap_C.words_C cap.[Suc 0] >> 20) && mask 10 \<noteq> 0\<rbrakk> \<Longrightarrow> is_aligned ((cap_C.words_C cap.[0] >> 22) && mask 7 << local.asid_low_bits) local.asid_low_bits
 2. \<lbrakk>c_valid_cap cap; cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_frame_cap; v3 = Some (0, (cap_C.words_C cap.[Suc 0] << 14) && ~~ mask 14); d = to_bool ((cap_C.words_C cap.[0] >> 29) && 1); v0 = (cap_C.words_C cap.[0] << 10) && ~~ mask 14; v1 = vmrights_to_H ((cap_C.words_C cap.[Suc 0] >> 18) && mask 2); v2 = framesize_to_H ((cap_C.words_C cap.[Suc 0] >> 30) && mask 2); (cap_C.words_C cap.[0] >> 22) && mask 7 = 0 \<longrightarrow> (cap_C.words_C cap.[Suc 0] >> 20) && mask 10 \<noteq> 0\<rbrakk> \<Longrightarrow> (cap_C.words_C cap.[Suc 0] >> 20) && mask 10 \<le> mask local.asid_low_bits
 3. \<lbrakk>c_valid_cap cap; cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_frame_cap; v3 = Some (0, (cap_C.words_C cap.[Suc 0] << 14) && ~~ mask 14); d = to_bool ((cap_C.words_C cap.[0] >> 29) && 1); v0 = (cap_C.words_C cap.[0] << 10) && ~~ mask 14; v1 = vmrights_to_H ((cap_C.words_C cap.[Suc 0] >> 18) && mask 2); v2 = framesize_to_H ((cap_C.words_C cap.[Suc 0] >> 30) && mask 2); (cap_C.words_C cap.[0] >> 22) && mask 7 = 0 \<longrightarrow> (cap_C.words_C cap.[Suc 0] >> 20) && mask 10 \<noteq> 0\<rbrakk> \<Longrightarrow> local.asid_low_bits < LENGTH(32)
 4. \<lbrakk>c_valid_cap cap; cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_frame_cap; v3 = Some (0, (cap_C.words_C cap.[Suc 0] << 14) && ~~ mask 14); d = to_bool ((cap_C.words_C cap.[0] >> 29) && 1); v0 = (cap_C.words_C cap.[0] << 10) && ~~ mask 14; v1 = vmrights_to_H ((cap_C.words_C cap.[Suc 0] >> 18) && mask 2); v2 = framesize_to_H ((cap_C.words_C cap.[Suc 0] >> 30) && mask 2); (cap_C.words_C cap.[0] >> 22) && mask 7 = 0 \<longrightarrow> (cap_C.words_C cap.[Suc 0] >> 20) && mask 10 \<noteq> 0; (cap_C.words_C cap.[0] >> 22) && mask 7 << local.asid_low_bits = 0 \<and> (cap_C.words_C cap.[Suc 0] >> 20) && mask 10 = 0\<rbrakk> \<Longrightarrow> False
 5. \<And>vl. \<lbrakk>cap_lift cap = Some vl; c_valid_cap cap; cap_to_H vl = capability.ArchObjectCap (arch_capability.PageCap d v0 v1 v2 v3); generic_frame_cap_get_capFMappedASID_CL (Some vl) = 0; cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap\<rbrakk> \<Longrightarrow> v3 = None proof (prove)
goal (4 subgoals):
 1. \<lbrakk>c_valid_cap cap; cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_frame_cap; v3 = Some (0, (cap_C.words_C cap.[Suc 0] << 14) && ~~ mask 14); d = to_bool ((cap_C.words_C cap.[0] >> 29) && 1); v0 = (cap_C.words_C cap.[0] << 10) && ~~ mask 14; v1 = vmrights_to_H ((cap_C.words_C cap.[Suc 0] >> 18) && mask 2); v2 = framesize_to_H ((cap_C.words_C cap.[Suc 0] >> 30) && mask 2); (cap_C.words_C cap.[0] >> 22) && mask 7 = 0 \<longrightarrow> (cap_C.words_C cap.[Suc 0] >> 20) && mask 10 \<noteq> 0\<rbrakk> \<Longrightarrow> (cap_C.words_C cap.[Suc 0] >> 20) && mask 10 \<le> mask local.asid_low_bits
 2. \<lbrakk>c_valid_cap cap; cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_frame_cap; v3 = Some (0, (cap_C.words_C cap.[Suc 0] << 14) && ~~ mask 14); d = to_bool ((cap_C.words_C cap.[0] >> 29) && 1); v0 = (cap_C.words_C cap.[0] << 10) && ~~ mask 14; v1 = vmrights_to_H ((cap_C.words_C cap.[Suc 0] >> 18) && mask 2); v2 = framesize_to_H ((cap_C.words_C cap.[Suc 0] >> 30) && mask 2); (cap_C.words_C cap.[0] >> 22) && mask 7 = 0 \<longrightarrow> (cap_C.words_C cap.[Suc 0] >> 20) && mask 10 \<noteq> 0\<rbrakk> \<Longrightarrow> local.asid_low_bits < LENGTH(32)
 3. \<lbrakk>c_valid_cap cap; cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_frame_cap; v3 = Some (0, (cap_C.words_C cap.[Suc 0] << 14) && ~~ mask 14); d = to_bool ((cap_C.words_C cap.[0] >> 29) && 1); v0 = (cap_C.words_C cap.[0] << 10) && ~~ mask 14; v1 = vmrights_to_H ((cap_C.words_C cap.[Suc 0] >> 18) && mask 2); v2 = framesize_to_H ((cap_C.words_C cap.[Suc 0] >> 30) && mask 2); (cap_C.words_C cap.[0] >> 22) && mask 7 = 0 \<longrightarrow> (cap_C.words_C cap.[Suc 0] >> 20) && mask 10 \<noteq> 0; (cap_C.words_C cap.[0] >> 22) && mask 7 << local.asid_low_bits = 0 \<and> (cap_C.words_C cap.[Suc 0] >> 20) && mask 10 = 0\<rbrakk> \<Longrightarrow> False
 4. \<And>vl. \<lbrakk>cap_lift cap = Some vl; c_valid_cap cap; cap_to_H vl = capability.ArchObjectCap (arch_capability.PageCap d v0 v1 v2 v3); generic_frame_cap_get_capFMappedASID_CL (Some vl) = 0; cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap\<rbrakk> \<Longrightarrow> v3 = None proof (prove)
goal (3 subgoals):
 1. \<lbrakk>c_valid_cap cap; cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_frame_cap; v3 = Some (0, (cap_C.words_C cap.[Suc 0] << 14) && ~~ mask 14); d = to_bool ((cap_C.words_C cap.[0] >> 29) && 1); v0 = (cap_C.words_C cap.[0] << 10) && ~~ mask 14; v1 = vmrights_to_H ((cap_C.words_C cap.[Suc 0] >> 18) && mask 2); v2 = framesize_to_H ((cap_C.words_C cap.[Suc 0] >> 30) && mask 2); (cap_C.words_C cap.[0] >> 22) && mask 7 = 0 \<longrightarrow> (cap_C.words_C cap.[Suc 0] >> 20) && mask 10 \<noteq> 0\<rbrakk> \<Longrightarrow> local.asid_low_bits < LENGTH(32)
 2. \<lbrakk>c_valid_cap cap; cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_frame_cap; v3 = Some (0, (cap_C.words_C cap.[Suc 0] << 14) && ~~ mask 14); d = to_bool ((cap_C.words_C cap.[0] >> 29) && 1); v0 = (cap_C.words_C cap.[0] << 10) && ~~ mask 14; v1 = vmrights_to_H ((cap_C.words_C cap.[Suc 0] >> 18) && mask 2); v2 = framesize_to_H ((cap_C.words_C cap.[Suc 0] >> 30) && mask 2); (cap_C.words_C cap.[0] >> 22) && mask 7 = 0 \<longrightarrow> (cap_C.words_C cap.[Suc 0] >> 20) && mask 10 \<noteq> 0; (cap_C.words_C cap.[0] >> 22) && mask 7 << local.asid_low_bits = 0 \<and> (cap_C.words_C cap.[Suc 0] >> 20) && mask 10 = 0\<rbrakk> \<Longrightarrow> False
 3. \<And>vl. \<lbrakk>cap_lift cap = Some vl; c_valid_cap cap; cap_to_H vl = capability.ArchObjectCap (arch_capability.PageCap d v0 v1 v2 v3); generic_frame_cap_get_capFMappedASID_CL (Some vl) = 0; cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap\<rbrakk> \<Longrightarrow> v3 = None proof (prove)
goal (2 subgoals):
 1. \<lbrakk>c_valid_cap cap; cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_frame_cap; v3 = Some (0, (cap_C.words_C cap.[Suc 0] << 14) && ~~ mask 14); d = to_bool ((cap_C.words_C cap.[0] >> 29) && 1); v0 = (cap_C.words_C cap.[0] << 10) && ~~ mask 14; v1 = vmrights_to_H ((cap_C.words_C cap.[Suc 0] >> 18) && mask 2); v2 = framesize_to_H ((cap_C.words_C cap.[Suc 0] >> 30) && mask 2); (cap_C.words_C cap.[0] >> 22) && mask 7 = 0 \<longrightarrow> (cap_C.words_C cap.[Suc 0] >> 20) && mask 10 \<noteq> 0; (cap_C.words_C cap.[0] >> 22) && mask 7 << local.asid_low_bits = 0 \<and> (cap_C.words_C cap.[Suc 0] >> 20) && mask 10 = 0\<rbrakk> \<Longrightarrow> False
 2. \<And>vl. \<lbrakk>cap_lift cap = Some vl; c_valid_cap cap; cap_to_H vl = capability.ArchObjectCap (arch_capability.PageCap d v0 v1 v2 v3); generic_frame_cap_get_capFMappedASID_CL (Some vl) = 0; cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap\<rbrakk> \<Longrightarrow> v3 = None proof (prove)
goal (2 subgoals):
 1. \<lbrakk>c_valid_cap cap; cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_frame_cap; v3 = Some (0, (cap_C.words_C cap.[Suc 0] << 14) && ~~ mask 14); d = to_bool ((cap_C.words_C cap.[0] >> 29) && 1); v0 = (cap_C.words_C cap.[0] << 10) && ~~ mask 14; v1 = vmrights_to_H ((cap_C.words_C cap.[Suc 0] >> 18) && mask 2); v2 = framesize_to_H ((cap_C.words_C cap.[Suc 0] >> 30) && mask 2); (cap_C.words_C cap.[0] >> 22) && mask 7 \<noteq> 0; (cap_C.words_C cap.[0] >> 22) && mask 7 << local.asid_low_bits = 0; (cap_C.words_C cap.[Suc 0] >> 20) && mask 10 = 0\<rbrakk> \<Longrightarrow> False
 2. \<And>vl. \<lbrakk>cap_lift cap = Some vl; c_valid_cap cap; cap_to_H vl = capability.ArchObjectCap (arch_capability.PageCap d v0 v1 v2 v3); generic_frame_cap_get_capFMappedASID_CL (Some vl) = 0; cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap\<rbrakk> \<Longrightarrow> v3 = None proof (prove)
goal (4 subgoals):
 1. \<lbrakk>c_valid_cap cap; cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_frame_cap; v3 = Some (0, (cap_C.words_C cap.[Suc 0] << 14) && ~~ mask 14); d = to_bool ((cap_C.words_C cap.[0] >> 29) && 1); v0 = (cap_C.words_C cap.[0] << 10) && ~~ mask 14; v1 = vmrights_to_H ((cap_C.words_C cap.[Suc 0] >> 18) && mask 2); v2 = framesize_to_H ((cap_C.words_C cap.[Suc 0] >> 30) && mask 2); (cap_C.words_C cap.[0] >> 22) && mask 7 \<noteq> 0; (cap_C.words_C cap.[Suc 0] >> 20) && mask 10 = 0\<rbrakk> \<Longrightarrow> (cap_C.words_C cap.[0] >> 22) && mask 7 \<le> 2 ^ 8
 2. \<lbrakk>c_valid_cap cap; cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_frame_cap; v3 = Some (0, (cap_C.words_C cap.[Suc 0] << 14) && ~~ mask 14); d = to_bool ((cap_C.words_C cap.[0] >> 29) && 1); v0 = (cap_C.words_C cap.[0] << 10) && ~~ mask 14; v1 = vmrights_to_H ((cap_C.words_C cap.[Suc 0] >> 18) && mask 2); v2 = framesize_to_H ((cap_C.words_C cap.[Suc 0] >> 30) && mask 2); (cap_C.words_C cap.[0] >> 22) && mask 7 \<noteq> 0; (cap_C.words_C cap.[Suc 0] >> 20) && mask 10 = 0\<rbrakk> \<Longrightarrow> 8 + local.asid_low_bits < LENGTH(32)
 3. \<lbrakk>c_valid_cap cap; cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_frame_cap; v3 = Some (0, (cap_C.words_C cap.[Suc 0] << 14) && ~~ mask 14); d = to_bool ((cap_C.words_C cap.[0] >> 29) && 1); v0 = (cap_C.words_C cap.[0] << 10) && ~~ mask 14; v1 = vmrights_to_H ((cap_C.words_C cap.[Suc 0] >> 18) && mask 2); v2 = framesize_to_H ((cap_C.words_C cap.[Suc 0] >> 30) && mask 2); (cap_C.words_C cap.[0] >> 22) && mask 7 \<noteq> 0; (cap_C.words_C cap.[Suc 0] >> 20) && mask 10 = 0; (cap_C.words_C cap.[0] >> 22) && mask 7 = 0\<rbrakk> \<Longrightarrow> False
 4. \<And>vl. \<lbrakk>cap_lift cap = Some vl; c_valid_cap cap; cap_to_H vl = capability.ArchObjectCap (arch_capability.PageCap d v0 v1 v2 v3); generic_frame_cap_get_capFMappedASID_CL (Some vl) = 0; cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap\<rbrakk> \<Longrightarrow> v3 = None proof (prove)
goal (5 subgoals):
 1. \<lbrakk>c_valid_cap cap; cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_frame_cap; v3 = Some (0, (cap_C.words_C cap.[Suc 0] << 14) && ~~ mask 14); d = to_bool ((cap_C.words_C cap.[0] >> 29) && 1); v0 = (cap_C.words_C cap.[0] << 10) && ~~ mask 14; v1 = vmrights_to_H ((cap_C.words_C cap.[Suc 0] >> 18) && mask 2); v2 = framesize_to_H ((cap_C.words_C cap.[Suc 0] >> 30) && mask 2); (cap_C.words_C cap.[0] >> 22) && mask 7 \<noteq> 0; (cap_C.words_C cap.[Suc 0] >> 20) && mask 10 = 0\<rbrakk> \<Longrightarrow> (cap_C.words_C cap.[0] >> 22) && mask 7 \<le> ?y96
 2. \<lbrakk>c_valid_cap cap; cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_frame_cap; v3 = Some (0, (cap_C.words_C cap.[Suc 0] << 14) && ~~ mask 14); d = to_bool ((cap_C.words_C cap.[0] >> 29) && 1); v0 = (cap_C.words_C cap.[0] << 10) && ~~ mask 14; v1 = vmrights_to_H ((cap_C.words_C cap.[Suc 0] >> 18) && mask 2); v2 = framesize_to_H ((cap_C.words_C cap.[Suc 0] >> 30) && mask 2); (cap_C.words_C cap.[0] >> 22) && mask 7 \<noteq> 0; (cap_C.words_C cap.[Suc 0] >> 20) && mask 10 = 0\<rbrakk> \<Longrightarrow> ?y96 \<le> 2 ^ 8
 3. \<lbrakk>c_valid_cap cap; cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_frame_cap; v3 = Some (0, (cap_C.words_C cap.[Suc 0] << 14) && ~~ mask 14); d = to_bool ((cap_C.words_C cap.[0] >> 29) && 1); v0 = (cap_C.words_C cap.[0] << 10) && ~~ mask 14; v1 = vmrights_to_H ((cap_C.words_C cap.[Suc 0] >> 18) && mask 2); v2 = framesize_to_H ((cap_C.words_C cap.[Suc 0] >> 30) && mask 2); (cap_C.words_C cap.[0] >> 22) && mask 7 \<noteq> 0; (cap_C.words_C cap.[Suc 0] >> 20) && mask 10 = 0\<rbrakk> \<Longrightarrow> 8 + local.asid_low_bits < LENGTH(32)
 4. \<lbrakk>c_valid_cap cap; cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_frame_cap; v3 = Some (0, (cap_C.words_C cap.[Suc 0] << 14) && ~~ mask 14); d = to_bool ((cap_C.words_C cap.[0] >> 29) && 1); v0 = (cap_C.words_C cap.[0] << 10) && ~~ mask 14; v1 = vmrights_to_H ((cap_C.words_C cap.[Suc 0] >> 18) && mask 2); v2 = framesize_to_H ((cap_C.words_C cap.[Suc 0] >> 30) && mask 2); (cap_C.words_C cap.[0] >> 22) && mask 7 \<noteq> 0; (cap_C.words_C cap.[Suc 0] >> 20) && mask 10 = 0; (cap_C.words_C cap.[0] >> 22) && mask 7 = 0\<rbrakk> \<Longrightarrow> False
 5. \<And>vl. \<lbrakk>cap_lift cap = Some vl; c_valid_cap cap; cap_to_H vl = capability.ArchObjectCap (arch_capability.PageCap d v0 v1 v2 v3); generic_frame_cap_get_capFMappedASID_CL (Some vl) = 0; cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap\<rbrakk> \<Longrightarrow> v3 = None proof (prove)
goal (4 subgoals):
 1. \<lbrakk>c_valid_cap cap; cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_frame_cap; v3 = Some (0, (cap_C.words_C cap.[Suc 0] << 14) && ~~ mask 14); d = to_bool ((cap_C.words_C cap.[0] >> 29) && 1); v0 = (cap_C.words_C cap.[0] << 10) && ~~ mask 14; v1 = vmrights_to_H ((cap_C.words_C cap.[Suc 0] >> 18) && mask 2); v2 = framesize_to_H ((cap_C.words_C cap.[Suc 0] >> 30) && mask 2); (cap_C.words_C cap.[0] >> 22) && mask 7 \<noteq> 0; (cap_C.words_C cap.[Suc 0] >> 20) && mask 10 = 0\<rbrakk> \<Longrightarrow> mask 7 \<le> 2 ^ 8
 2. \<lbrakk>c_valid_cap cap; cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_frame_cap; v3 = Some (0, (cap_C.words_C cap.[Suc 0] << 14) && ~~ mask 14); d = to_bool ((cap_C.words_C cap.[0] >> 29) && 1); v0 = (cap_C.words_C cap.[0] << 10) && ~~ mask 14; v1 = vmrights_to_H ((cap_C.words_C cap.[Suc 0] >> 18) && mask 2); v2 = framesize_to_H ((cap_C.words_C cap.[Suc 0] >> 30) && mask 2); (cap_C.words_C cap.[0] >> 22) && mask 7 \<noteq> 0; (cap_C.words_C cap.[Suc 0] >> 20) && mask 10 = 0\<rbrakk> \<Longrightarrow> 8 + local.asid_low_bits < LENGTH(32)
 3. \<lbrakk>c_valid_cap cap; cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_frame_cap; v3 = Some (0, (cap_C.words_C cap.[Suc 0] << 14) && ~~ mask 14); d = to_bool ((cap_C.words_C cap.[0] >> 29) && 1); v0 = (cap_C.words_C cap.[0] << 10) && ~~ mask 14; v1 = vmrights_to_H ((cap_C.words_C cap.[Suc 0] >> 18) && mask 2); v2 = framesize_to_H ((cap_C.words_C cap.[Suc 0] >> 30) && mask 2); (cap_C.words_C cap.[0] >> 22) && mask 7 \<noteq> 0; (cap_C.words_C cap.[Suc 0] >> 20) && mask 10 = 0; (cap_C.words_C cap.[0] >> 22) && mask 7 = 0\<rbrakk> \<Longrightarrow> False
 4. \<And>vl. \<lbrakk>cap_lift cap = Some vl; c_valid_cap cap; cap_to_H vl = capability.ArchObjectCap (arch_capability.PageCap d v0 v1 v2 v3); generic_frame_cap_get_capFMappedASID_CL (Some vl) = 0; cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap\<rbrakk> \<Longrightarrow> v3 = None proof (prove)
goal (3 subgoals):
 1. \<lbrakk>c_valid_cap cap; cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_frame_cap; v3 = Some (0, (cap_C.words_C cap.[Suc 0] << 14) && ~~ mask 14); d = to_bool ((cap_C.words_C cap.[0] >> 29) && 1); v0 = (cap_C.words_C cap.[0] << 10) && ~~ mask 14; v1 = vmrights_to_H ((cap_C.words_C cap.[Suc 0] >> 18) && mask 2); v2 = framesize_to_H ((cap_C.words_C cap.[Suc 0] >> 30) && mask 2); (cap_C.words_C cap.[0] >> 22) && mask 7 \<noteq> 0; (cap_C.words_C cap.[Suc 0] >> 20) && mask 10 = 0\<rbrakk> \<Longrightarrow> 8 + local.asid_low_bits < LENGTH(32)
 2. \<lbrakk>c_valid_cap cap; cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_frame_cap; v3 = Some (0, (cap_C.words_C cap.[Suc 0] << 14) && ~~ mask 14); d = to_bool ((cap_C.words_C cap.[0] >> 29) && 1); v0 = (cap_C.words_C cap.[0] << 10) && ~~ mask 14; v1 = vmrights_to_H ((cap_C.words_C cap.[Suc 0] >> 18) && mask 2); v2 = framesize_to_H ((cap_C.words_C cap.[Suc 0] >> 30) && mask 2); (cap_C.words_C cap.[0] >> 22) && mask 7 \<noteq> 0; (cap_C.words_C cap.[Suc 0] >> 20) && mask 10 = 0; (cap_C.words_C cap.[0] >> 22) && mask 7 = 0\<rbrakk> \<Longrightarrow> False
 3. \<And>vl. \<lbrakk>cap_lift cap = Some vl; c_valid_cap cap; cap_to_H vl = capability.ArchObjectCap (arch_capability.PageCap d v0 v1 v2 v3); generic_frame_cap_get_capFMappedASID_CL (Some vl) = 0; cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap\<rbrakk> \<Longrightarrow> v3 = None proof (prove)
goal (2 subgoals):
 1. \<lbrakk>c_valid_cap cap; cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_frame_cap; v3 = Some (0, (cap_C.words_C cap.[Suc 0] << 14) && ~~ mask 14); d = to_bool ((cap_C.words_C cap.[0] >> 29) && 1); v0 = (cap_C.words_C cap.[0] << 10) && ~~ mask 14; v1 = vmrights_to_H ((cap_C.words_C cap.[Suc 0] >> 18) && mask 2); v2 = framesize_to_H ((cap_C.words_C cap.[Suc 0] >> 30) && mask 2); (cap_C.words_C cap.[0] >> 22) && mask 7 \<noteq> 0; (cap_C.words_C cap.[Suc 0] >> 20) && mask 10 = 0; (cap_C.words_C cap.[0] >> 22) && mask 7 = 0\<rbrakk> \<Longrightarrow> False
 2. \<And>vl. \<lbrakk>cap_lift cap = Some vl; c_valid_cap cap; cap_to_H vl = capability.ArchObjectCap (arch_capability.PageCap d v0 v1 v2 v3); generic_frame_cap_get_capFMappedASID_CL (Some vl) = 0; cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap\<rbrakk> \<Longrightarrow> v3 = None proof (prove)
goal (1 subgoal):
 1. \<And>vl. \<lbrakk>cap_lift cap = Some vl; c_valid_cap cap; cap_to_H vl = capability.ArchObjectCap (arch_capability.PageCap d v0 v1 v2 v3); generic_frame_cap_get_capFMappedASID_CL (Some vl) = 0; cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap\<rbrakk> \<Longrightarrow> v3 = None proof (prove)
goal (1 subgoal):
 1. \<And>vl. \<lbrakk>cap_lift cap = Some vl; c_valid_cap cap; cap_to_H vl = capability.ArchObjectCap (arch_capability.PageCap d v0 v1 v2 v3); generic_frame_cap_get_capFMappedASID_CL (Some vl) = 0; cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap; v3 \<noteq> None\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>vl a b. \<lbrakk>cap_lift cap = Some vl; cap_to_H vl = capability.ArchObjectCap (arch_capability.PageCap d v0 v1 v2 (Some (a, b))); generic_frame_cap_get_capFMappedASID_CL (Some vl) = 0; cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap; v3 = Some (a, b)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap; v3 = Some (0, (cap_C.words_C cap.[Suc 0] << 12) && ~~ mask 12); d = to_bool ((cap_C.words_C cap.[0] >> 31) && 1); v0 = (cap_C.words_C cap.[0] << 8) && ~~ mask 12; v1 = vmrights_to_H ((cap_C.words_C cap.[Suc 0] >> 20) && mask 2); v2 = Wellformed_C.ARMSmallPage; (cap_C.words_C cap.[0] >> 24) && mask 7 = 0 \<longrightarrow> (cap_C.words_C cap.[Suc 0] >> 22) && mask 10 \<noteq> 0; ((cap_C.words_C cap.[0] >> 24) && mask 7 << local.asid_low_bits) + ((cap_C.words_C cap.[Suc 0] >> 22) && mask 10) = 0\<rbrakk> \<Longrightarrow> False proof (prove)
goal (4 subgoals):
 1. \<lbrakk>cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap; v3 = Some (0, (cap_C.words_C cap.[Suc 0] << 12) && ~~ mask 12); d = to_bool ((cap_C.words_C cap.[0] >> 31) && 1); v0 = (cap_C.words_C cap.[0] << 8) && ~~ mask 12; v1 = vmrights_to_H ((cap_C.words_C cap.[Suc 0] >> 20) && mask 2); v2 = Wellformed_C.ARMSmallPage; (cap_C.words_C cap.[0] >> 24) && mask 7 = 0 \<longrightarrow> (cap_C.words_C cap.[Suc 0] >> 22) && mask 10 \<noteq> 0\<rbrakk> \<Longrightarrow> is_aligned ((cap_C.words_C cap.[0] >> 24) && mask 7 << local.asid_low_bits) local.asid_low_bits
 2. \<lbrakk>cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap; v3 = Some (0, (cap_C.words_C cap.[Suc 0] << 12) && ~~ mask 12); d = to_bool ((cap_C.words_C cap.[0] >> 31) && 1); v0 = (cap_C.words_C cap.[0] << 8) && ~~ mask 12; v1 = vmrights_to_H ((cap_C.words_C cap.[Suc 0] >> 20) && mask 2); v2 = Wellformed_C.ARMSmallPage; (cap_C.words_C cap.[0] >> 24) && mask 7 = 0 \<longrightarrow> (cap_C.words_C cap.[Suc 0] >> 22) && mask 10 \<noteq> 0\<rbrakk> \<Longrightarrow> (cap_C.words_C cap.[Suc 0] >> 22) && mask 10 \<le> mask local.asid_low_bits
 3. \<lbrakk>cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap; v3 = Some (0, (cap_C.words_C cap.[Suc 0] << 12) && ~~ mask 12); d = to_bool ((cap_C.words_C cap.[0] >> 31) && 1); v0 = (cap_C.words_C cap.[0] << 8) && ~~ mask 12; v1 = vmrights_to_H ((cap_C.words_C cap.[Suc 0] >> 20) && mask 2); v2 = Wellformed_C.ARMSmallPage; (cap_C.words_C cap.[0] >> 24) && mask 7 = 0 \<longrightarrow> (cap_C.words_C cap.[Suc 0] >> 22) && mask 10 \<noteq> 0\<rbrakk> \<Longrightarrow> local.asid_low_bits < LENGTH(32)
 4. \<lbrakk>cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap; v3 = Some (0, (cap_C.words_C cap.[Suc 0] << 12) && ~~ mask 12); d = to_bool ((cap_C.words_C cap.[0] >> 31) && 1); v0 = (cap_C.words_C cap.[0] << 8) && ~~ mask 12; v1 = vmrights_to_H ((cap_C.words_C cap.[Suc 0] >> 20) && mask 2); v2 = Wellformed_C.ARMSmallPage; (cap_C.words_C cap.[0] >> 24) && mask 7 = 0 \<longrightarrow> (cap_C.words_C cap.[Suc 0] >> 22) && mask 10 \<noteq> 0; (cap_C.words_C cap.[0] >> 24) && mask 7 << local.asid_low_bits = 0 \<and> (cap_C.words_C cap.[Suc 0] >> 22) && mask 10 = 0\<rbrakk> \<Longrightarrow> False proof (prove)
goal (3 subgoals):
 1. \<lbrakk>cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap; v3 = Some (0, (cap_C.words_C cap.[Suc 0] << 12) && ~~ mask 12); d = to_bool ((cap_C.words_C cap.[0] >> 31) && 1); v0 = (cap_C.words_C cap.[0] << 8) && ~~ mask 12; v1 = vmrights_to_H ((cap_C.words_C cap.[Suc 0] >> 20) && mask 2); v2 = Wellformed_C.ARMSmallPage; (cap_C.words_C cap.[0] >> 24) && mask 7 = 0 \<longrightarrow> (cap_C.words_C cap.[Suc 0] >> 22) && mask 10 \<noteq> 0\<rbrakk> \<Longrightarrow> (cap_C.words_C cap.[Suc 0] >> 22) && mask 10 \<le> mask local.asid_low_bits
 2. \<lbrakk>cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap; v3 = Some (0, (cap_C.words_C cap.[Suc 0] << 12) && ~~ mask 12); d = to_bool ((cap_C.words_C cap.[0] >> 31) && 1); v0 = (cap_C.words_C cap.[0] << 8) && ~~ mask 12; v1 = vmrights_to_H ((cap_C.words_C cap.[Suc 0] >> 20) && mask 2); v2 = Wellformed_C.ARMSmallPage; (cap_C.words_C cap.[0] >> 24) && mask 7 = 0 \<longrightarrow> (cap_C.words_C cap.[Suc 0] >> 22) && mask 10 \<noteq> 0\<rbrakk> \<Longrightarrow> local.asid_low_bits < LENGTH(32)
 3. \<lbrakk>cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap; v3 = Some (0, (cap_C.words_C cap.[Suc 0] << 12) && ~~ mask 12); d = to_bool ((cap_C.words_C cap.[0] >> 31) && 1); v0 = (cap_C.words_C cap.[0] << 8) && ~~ mask 12; v1 = vmrights_to_H ((cap_C.words_C cap.[Suc 0] >> 20) && mask 2); v2 = Wellformed_C.ARMSmallPage; (cap_C.words_C cap.[0] >> 24) && mask 7 = 0 \<longrightarrow> (cap_C.words_C cap.[Suc 0] >> 22) && mask 10 \<noteq> 0; (cap_C.words_C cap.[0] >> 24) && mask 7 << local.asid_low_bits = 0 \<and> (cap_C.words_C cap.[Suc 0] >> 22) && mask 10 = 0\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<lbrakk>cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap; v3 = Some (0, (cap_C.words_C cap.[Suc 0] << 12) && ~~ mask 12); d = to_bool ((cap_C.words_C cap.[0] >> 31) && 1); v0 = (cap_C.words_C cap.[0] << 8) && ~~ mask 12; v1 = vmrights_to_H ((cap_C.words_C cap.[Suc 0] >> 20) && mask 2); v2 = Wellformed_C.ARMSmallPage; (cap_C.words_C cap.[0] >> 24) && mask 7 = 0 \<longrightarrow> (cap_C.words_C cap.[Suc 0] >> 22) && mask 10 \<noteq> 0\<rbrakk> \<Longrightarrow> local.asid_low_bits < LENGTH(32)
 2. \<lbrakk>cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap; v3 = Some (0, (cap_C.words_C cap.[Suc 0] << 12) && ~~ mask 12); d = to_bool ((cap_C.words_C cap.[0] >> 31) && 1); v0 = (cap_C.words_C cap.[0] << 8) && ~~ mask 12; v1 = vmrights_to_H ((cap_C.words_C cap.[Suc 0] >> 20) && mask 2); v2 = Wellformed_C.ARMSmallPage; (cap_C.words_C cap.[0] >> 24) && mask 7 = 0 \<longrightarrow> (cap_C.words_C cap.[Suc 0] >> 22) && mask 10 \<noteq> 0; (cap_C.words_C cap.[0] >> 24) && mask 7 << local.asid_low_bits = 0 \<and> (cap_C.words_C cap.[Suc 0] >> 22) && mask 10 = 0\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap; v3 = Some (0, (cap_C.words_C cap.[Suc 0] << 12) && ~~ mask 12); d = to_bool ((cap_C.words_C cap.[0] >> 31) && 1); v0 = (cap_C.words_C cap.[0] << 8) && ~~ mask 12; v1 = vmrights_to_H ((cap_C.words_C cap.[Suc 0] >> 20) && mask 2); v2 = Wellformed_C.ARMSmallPage; (cap_C.words_C cap.[0] >> 24) && mask 7 = 0 \<longrightarrow> (cap_C.words_C cap.[Suc 0] >> 22) && mask 10 \<noteq> 0; (cap_C.words_C cap.[0] >> 24) && mask 7 << local.asid_low_bits = 0 \<and> (cap_C.words_C cap.[Suc 0] >> 22) && mask 10 = 0\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap; v3 = Some (0, (cap_C.words_C cap.[Suc 0] << 12) && ~~ mask 12); d = to_bool ((cap_C.words_C cap.[0] >> 31) && 1); v0 = (cap_C.words_C cap.[0] << 8) && ~~ mask 12; v1 = vmrights_to_H ((cap_C.words_C cap.[Suc 0] >> 20) && mask 2); v2 = Wellformed_C.ARMSmallPage; (cap_C.words_C cap.[0] >> 24) && mask 7 \<noteq> 0; (cap_C.words_C cap.[0] >> 24) && mask 7 << local.asid_low_bits = 0; (cap_C.words_C cap.[Suc 0] >> 22) && mask 10 = 0\<rbrakk> \<Longrightarrow> False proof (prove)
goal (3 subgoals):
 1. \<lbrakk>cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap; v3 = Some (0, (cap_C.words_C cap.[Suc 0] << 12) && ~~ mask 12); d = to_bool ((cap_C.words_C cap.[0] >> 31) && 1); v0 = (cap_C.words_C cap.[0] << 8) && ~~ mask 12; v1 = vmrights_to_H ((cap_C.words_C cap.[Suc 0] >> 20) && mask 2); v2 = Wellformed_C.ARMSmallPage; (cap_C.words_C cap.[0] >> 24) && mask 7 \<noteq> 0; (cap_C.words_C cap.[Suc 0] >> 22) && mask 10 = 0\<rbrakk> \<Longrightarrow> (cap_C.words_C cap.[0] >> 24) && mask 7 \<le> 2 ^ 8
 2. \<lbrakk>cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap; v3 = Some (0, (cap_C.words_C cap.[Suc 0] << 12) && ~~ mask 12); d = to_bool ((cap_C.words_C cap.[0] >> 31) && 1); v0 = (cap_C.words_C cap.[0] << 8) && ~~ mask 12; v1 = vmrights_to_H ((cap_C.words_C cap.[Suc 0] >> 20) && mask 2); v2 = Wellformed_C.ARMSmallPage; (cap_C.words_C cap.[0] >> 24) && mask 7 \<noteq> 0; (cap_C.words_C cap.[Suc 0] >> 22) && mask 10 = 0\<rbrakk> \<Longrightarrow> 8 + local.asid_low_bits < LENGTH(32)
 3. \<lbrakk>cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap; v3 = Some (0, (cap_C.words_C cap.[Suc 0] << 12) && ~~ mask 12); d = to_bool ((cap_C.words_C cap.[0] >> 31) && 1); v0 = (cap_C.words_C cap.[0] << 8) && ~~ mask 12; v1 = vmrights_to_H ((cap_C.words_C cap.[Suc 0] >> 20) && mask 2); v2 = Wellformed_C.ARMSmallPage; (cap_C.words_C cap.[0] >> 24) && mask 7 \<noteq> 0; (cap_C.words_C cap.[Suc 0] >> 22) && mask 10 = 0; (cap_C.words_C cap.[0] >> 24) && mask 7 = 0\<rbrakk> \<Longrightarrow> False proof (prove)
goal (4 subgoals):
 1. \<lbrakk>cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap; v3 = Some (0, (cap_C.words_C cap.[Suc 0] << 12) && ~~ mask 12); d = to_bool ((cap_C.words_C cap.[0] >> 31) && 1); v0 = (cap_C.words_C cap.[0] << 8) && ~~ mask 12; v1 = vmrights_to_H ((cap_C.words_C cap.[Suc 0] >> 20) && mask 2); v2 = Wellformed_C.ARMSmallPage; (cap_C.words_C cap.[0] >> 24) && mask 7 \<noteq> 0; (cap_C.words_C cap.[Suc 0] >> 22) && mask 10 = 0\<rbrakk> \<Longrightarrow> (cap_C.words_C cap.[0] >> 24) && mask 7 \<le> ?y141
 2. \<lbrakk>cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap; v3 = Some (0, (cap_C.words_C cap.[Suc 0] << 12) && ~~ mask 12); d = to_bool ((cap_C.words_C cap.[0] >> 31) && 1); v0 = (cap_C.words_C cap.[0] << 8) && ~~ mask 12; v1 = vmrights_to_H ((cap_C.words_C cap.[Suc 0] >> 20) && mask 2); v2 = Wellformed_C.ARMSmallPage; (cap_C.words_C cap.[0] >> 24) && mask 7 \<noteq> 0; (cap_C.words_C cap.[Suc 0] >> 22) && mask 10 = 0\<rbrakk> \<Longrightarrow> ?y141 \<le> 2 ^ 8
 3. \<lbrakk>cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap; v3 = Some (0, (cap_C.words_C cap.[Suc 0] << 12) && ~~ mask 12); d = to_bool ((cap_C.words_C cap.[0] >> 31) && 1); v0 = (cap_C.words_C cap.[0] << 8) && ~~ mask 12; v1 = vmrights_to_H ((cap_C.words_C cap.[Suc 0] >> 20) && mask 2); v2 = Wellformed_C.ARMSmallPage; (cap_C.words_C cap.[0] >> 24) && mask 7 \<noteq> 0; (cap_C.words_C cap.[Suc 0] >> 22) && mask 10 = 0\<rbrakk> \<Longrightarrow> 8 + local.asid_low_bits < LENGTH(32)
 4. \<lbrakk>cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap; v3 = Some (0, (cap_C.words_C cap.[Suc 0] << 12) && ~~ mask 12); d = to_bool ((cap_C.words_C cap.[0] >> 31) && 1); v0 = (cap_C.words_C cap.[0] << 8) && ~~ mask 12; v1 = vmrights_to_H ((cap_C.words_C cap.[Suc 0] >> 20) && mask 2); v2 = Wellformed_C.ARMSmallPage; (cap_C.words_C cap.[0] >> 24) && mask 7 \<noteq> 0; (cap_C.words_C cap.[Suc 0] >> 22) && mask 10 = 0; (cap_C.words_C cap.[0] >> 24) && mask 7 = 0\<rbrakk> \<Longrightarrow> False proof (prove)
goal (3 subgoals):
 1. \<lbrakk>cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap; v3 = Some (0, (cap_C.words_C cap.[Suc 0] << 12) && ~~ mask 12); d = to_bool ((cap_C.words_C cap.[0] >> 31) && 1); v0 = (cap_C.words_C cap.[0] << 8) && ~~ mask 12; v1 = vmrights_to_H ((cap_C.words_C cap.[Suc 0] >> 20) && mask 2); v2 = Wellformed_C.ARMSmallPage; (cap_C.words_C cap.[0] >> 24) && mask 7 \<noteq> 0; (cap_C.words_C cap.[Suc 0] >> 22) && mask 10 = 0\<rbrakk> \<Longrightarrow> mask 7 \<le> 2 ^ 8
 2. \<lbrakk>cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap; v3 = Some (0, (cap_C.words_C cap.[Suc 0] << 12) && ~~ mask 12); d = to_bool ((cap_C.words_C cap.[0] >> 31) && 1); v0 = (cap_C.words_C cap.[0] << 8) && ~~ mask 12; v1 = vmrights_to_H ((cap_C.words_C cap.[Suc 0] >> 20) && mask 2); v2 = Wellformed_C.ARMSmallPage; (cap_C.words_C cap.[0] >> 24) && mask 7 \<noteq> 0; (cap_C.words_C cap.[Suc 0] >> 22) && mask 10 = 0\<rbrakk> \<Longrightarrow> 8 + local.asid_low_bits < LENGTH(32)
 3. \<lbrakk>cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap; v3 = Some (0, (cap_C.words_C cap.[Suc 0] << 12) && ~~ mask 12); d = to_bool ((cap_C.words_C cap.[0] >> 31) && 1); v0 = (cap_C.words_C cap.[0] << 8) && ~~ mask 12; v1 = vmrights_to_H ((cap_C.words_C cap.[Suc 0] >> 20) && mask 2); v2 = Wellformed_C.ARMSmallPage; (cap_C.words_C cap.[0] >> 24) && mask 7 \<noteq> 0; (cap_C.words_C cap.[Suc 0] >> 22) && mask 10 = 0; (cap_C.words_C cap.[0] >> 24) && mask 7 = 0\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<lbrakk>cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap; v3 = Some (0, (cap_C.words_C cap.[Suc 0] << 12) && ~~ mask 12); d = to_bool ((cap_C.words_C cap.[0] >> 31) && 1); v0 = (cap_C.words_C cap.[0] << 8) && ~~ mask 12; v1 = vmrights_to_H ((cap_C.words_C cap.[Suc 0] >> 20) && mask 2); v2 = Wellformed_C.ARMSmallPage; (cap_C.words_C cap.[0] >> 24) && mask 7 \<noteq> 0; (cap_C.words_C cap.[Suc 0] >> 22) && mask 10 = 0\<rbrakk> \<Longrightarrow> 8 + local.asid_low_bits < LENGTH(32)
 2. \<lbrakk>cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap; v3 = Some (0, (cap_C.words_C cap.[Suc 0] << 12) && ~~ mask 12); d = to_bool ((cap_C.words_C cap.[0] >> 31) && 1); v0 = (cap_C.words_C cap.[0] << 8) && ~~ mask 12; v1 = vmrights_to_H ((cap_C.words_C cap.[Suc 0] >> 20) && mask 2); v2 = Wellformed_C.ARMSmallPage; (cap_C.words_C cap.[0] >> 24) && mask 7 \<noteq> 0; (cap_C.words_C cap.[Suc 0] >> 22) && mask 10 = 0; (cap_C.words_C cap.[0] >> 24) && mask 7 = 0\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap; v3 = Some (0, (cap_C.words_C cap.[Suc 0] << 12) && ~~ mask 12); d = to_bool ((cap_C.words_C cap.[0] >> 31) && 1); v0 = (cap_C.words_C cap.[0] << 8) && ~~ mask 12; v1 = vmrights_to_H ((cap_C.words_C cap.[Suc 0] >> 20) && mask 2); v2 = Wellformed_C.ARMSmallPage; (cap_C.words_C cap.[0] >> 24) && mask 7 \<noteq> 0; (cap_C.words_C cap.[Suc 0] >> 22) && mask 10 = 0; (cap_C.words_C cap.[0] >> 24) && mask 7 = 0\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!