theory SR_lemmas_C

lemma small_frame_cap_is_mapped_alt:
  "cap_get_tag cp = scast cap_small_frame_cap \<Longrightarrow>
   (cap_small_frame_cap_CL.capFMappedASIDHigh_CL (cap_small_frame_cap_lift cp) = 0
       \<and> cap_small_frame_cap_CL.capFMappedASIDLow_CL (cap_small_frame_cap_lift cp) = 0)
    = ((cap_small_frame_cap_CL.capFMappedASIDHigh_CL (cap_small_frame_cap_lift cp)
              << asidLowBits)
         + cap_small_frame_cap_CL.capFMappedASIDLow_CL (cap_small_frame_cap_lift cp)
              = 0)" apply (simp add: cap_lift_small_frame_cap cap_small_frame_cap_lift_def) apply (subst word_plus_and_or_coroll) apply (rule word_eqI) apply (clarsimp simp: word_ops_nth_size nth_shiftl asid_low_bits_def) apply (simp add: word_or_zero) apply safe apply simp apply (rule word_eqI) apply (drule_tac x="n + asid_low_bits" in word_eqD)+ apply (clarsimp simp add: word_ops_nth_size asid_low_bits_def nth_shiftl nth_shiftr) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cap_get_tag cp = SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap \<Longrightarrow> (cap_small_frame_cap_CL.capFMappedASIDHigh_CL (cap_small_frame_cap_lift cp) = 0 \<and> cap_small_frame_cap_CL.capFMappedASIDLow_CL (cap_small_frame_cap_lift cp) = 0) = ((cap_small_frame_cap_CL.capFMappedASIDHigh_CL (cap_small_frame_cap_lift cp) << local.asidLowBits) + cap_small_frame_cap_CL.capFMappedASIDLow_CL (cap_small_frame_cap_lift cp) = 0) proof (prove)
goal (1 subgoal):
 1. cap_get_tag cp = SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap \<Longrightarrow> ((cap_C.words_C cp.[0] >> 24) && mask 7 = 0 \<and> (cap_C.words_C cp.[Suc 0] >> 22) && mask 10 = 0) = (((cap_C.words_C cp.[0] >> 24) && mask 7 << local.asid_low_bits) + ((cap_C.words_C cp.[Suc 0] >> 22) && mask 10) = 0) proof (prove)
goal (2 subgoals):
 1. cap_get_tag cp = SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap \<Longrightarrow> ((cap_C.words_C cp.[0] >> 24) && mask 7 << local.asid_low_bits) && (cap_C.words_C cp.[Suc 0] >> 22) && mask 10 = 0
 2. cap_get_tag cp = SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap \<Longrightarrow> ((cap_C.words_C cp.[0] >> 24) && mask 7 = 0 \<and> (cap_C.words_C cp.[Suc 0] >> 22) && mask 10 = 0) = (((cap_C.words_C cp.[0] >> 24) && mask 7 << local.asid_low_bits) || (cap_C.words_C cp.[Suc 0] >> 22) && mask 10 = 0) proof (prove)
goal (2 subgoals):
 1. \<And>n. cap_get_tag cp = SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap \<Longrightarrow> n < size (((cap_C.words_C cp.[0] >> 24) && mask 7 << local.asid_low_bits) && (cap_C.words_C cp.[Suc 0] >> 22) && mask 10) \<longrightarrow> (((cap_C.words_C cp.[0] >> 24) && mask 7 << local.asid_low_bits) && (cap_C.words_C cp.[Suc 0] >> 22) && mask 10) !! n = 0 !! n
 2. cap_get_tag cp = SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap \<Longrightarrow> ((cap_C.words_C cp.[0] >> 24) && mask 7 = 0 \<and> (cap_C.words_C cp.[Suc 0] >> 22) && mask 10 = 0) = (((cap_C.words_C cp.[0] >> 24) && mask 7 << local.asid_low_bits) || (cap_C.words_C cp.[Suc 0] >> 22) && mask 10 = 0) proof (prove)
goal (1 subgoal):
 1. cap_get_tag cp = SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap \<Longrightarrow> ((cap_C.words_C cp.[0] >> 24) && mask 7 = 0 \<and> (cap_C.words_C cp.[Suc 0] >> 22) && mask 10 = 0) = (((cap_C.words_C cp.[0] >> 24) && mask 7 << local.asid_low_bits) || (cap_C.words_C cp.[Suc 0] >> 22) && mask 10 = 0) proof (prove)
goal (1 subgoal):
 1. cap_get_tag cp = SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap \<Longrightarrow> ((cap_C.words_C cp.[0] >> 24) && mask 7 = 0 \<and> (cap_C.words_C cp.[Suc 0] >> 22) && mask 10 = 0) = ((cap_C.words_C cp.[0] >> 24) && mask 7 << local.asid_low_bits = 0 \<and> (cap_C.words_C cp.[Suc 0] >> 22) && mask 10 = 0) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>cap_get_tag cp = SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap; (cap_C.words_C cp.[0] >> 24) && mask 7 = 0; (cap_C.words_C cp.[Suc 0] >> 22) && mask 10 = 0\<rbrakk> \<Longrightarrow> (cap_C.words_C cp.[0] >> 24) && mask 7 << local.asid_low_bits = 0
 2. \<lbrakk>cap_get_tag cp = SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap; (cap_C.words_C cp.[0] >> 24) && mask 7 << local.asid_low_bits = 0; (cap_C.words_C cp.[Suc 0] >> 22) && mask 10 = 0\<rbrakk> \<Longrightarrow> (cap_C.words_C cp.[0] >> 24) && mask 7 = 0 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cap_get_tag cp = SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap; (cap_C.words_C cp.[0] >> 24) && mask 7 << local.asid_low_bits = 0; (cap_C.words_C cp.[Suc 0] >> 22) && mask 10 = 0\<rbrakk> \<Longrightarrow> (cap_C.words_C cp.[0] >> 24) && mask 7 = 0 proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>cap_get_tag cp = SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap; (cap_C.words_C cp.[0] >> 24) && mask 7 << local.asid_low_bits = 0; (cap_C.words_C cp.[Suc 0] >> 22) && mask 10 = 0\<rbrakk> \<Longrightarrow> n < size ((cap_C.words_C cp.[0] >> 24) && mask 7) \<longrightarrow> ((cap_C.words_C cp.[0] >> 24) && mask 7) !! n = 0 !! n proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>cap_get_tag cp !! (n + local.asid_low_bits) = SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap !! (n + local.asid_low_bits); ((cap_C.words_C cp.[0] >> 24) && mask 7 << local.asid_low_bits) !! (n + local.asid_low_bits) = 0 !! (n + local.asid_low_bits); ((cap_C.words_C cp.[Suc 0] >> 22) && mask 10) !! (n + local.asid_low_bits) = 0 !! (n + local.asid_low_bits)\<rbrakk> \<Longrightarrow> n < size ((cap_C.words_C cp.[0] >> 24) && mask 7) \<longrightarrow> ((cap_C.words_C cp.[0] >> 24) && mask 7) !! n = 0 !! n proof (prove)
goal:
No subgoals!