theory Fastpath_C

lemma isValidVTableRoot_fp_lemma:
  "(index (cap_C.words_C ccap) 0 && 0x1F = 0x10 || scast cap_page_directory_cap)
            = isValidVTableRoot_C ccap" apply (simp add: isValidVTableRoot_C_def ARM_H.isValidVTableRoot_def
                   cap_case_isPageDirectoryCap if_bool_simps) apply (subst split_word_eq_on_mask[where m="mask 4"]) apply (simp add: mask_def word_bw_assocs word_ao_dist cap_page_directory_cap_def) apply (subgoal_tac "cap_get_tag ccap = scast cap_page_directory_cap
                  \<Longrightarrow> (index (cap_C.words_C ccap) 0 && 0x10 = 0x10) = to_bool (capPDIsMapped_CL (cap_page_directory_cap_lift ccap))") apply (clarsimp simp add: cap_get_tag_eq_x mask_def
                             cap_page_directory_cap_def split: if_split) apply (rule conj_cong[OF refl]) apply clarsimp apply (clarsimp simp: cap_lift_page_directory_cap
                        cap_to_H_simps
                        to_bool_def bool_mask[folded word_neq_0_conv]
                        cap_page_directory_cap_lift_def
                 elim!: ccap_relationE split: if_split) apply (thin_tac "P" for P) apply word_bitwise done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (cap_C.words_C ccap.[0] && 0x1F = 0x10 || SCAST(32 signed \<rightarrow> 32) cap_page_directory_cap) = isValidVTableRoot_C ccap proof (prove)
goal (1 subgoal):
 1. (cap_C.words_C ccap.[0] && 0x1F = 0x10 || SCAST(32 signed \<rightarrow> 32) cap_page_directory_cap) = (cap_get_tag ccap = SCAST(32 signed \<rightarrow> 32) cap_page_directory_cap \<and> to_bool (capPDIsMapped_CL (cap_page_directory_cap_lift ccap))) proof (prove)
goal (1 subgoal):
 1. ((cap_C.words_C ccap.[0] && 0x1F) && mask 4 = (0x10 || SCAST(32 signed \<rightarrow> 32) cap_page_directory_cap) && mask 4 \<and> (cap_C.words_C ccap.[0] && 0x1F) && ~~ mask 4 = (0x10 || SCAST(32 signed \<rightarrow> 32) cap_page_directory_cap) && ~~ mask 4) = (cap_get_tag ccap = SCAST(32 signed \<rightarrow> 32) cap_page_directory_cap \<and> to_bool (capPDIsMapped_CL (cap_page_directory_cap_lift ccap))) proof (prove)
goal (1 subgoal):
 1. (cap_C.words_C ccap.[0] && 0xF = 9 \<and> cap_C.words_C ccap.[0] && 0x10 = 0x10) = (cap_get_tag ccap = 9 \<and> to_bool (capPDIsMapped_CL (cap_page_directory_cap_lift ccap))) proof (prove)
goal (2 subgoals):
 1. (cap_get_tag ccap = SCAST(32 signed \<rightarrow> 32) cap_page_directory_cap \<Longrightarrow> (cap_C.words_C ccap.[0] && 0x10 = 0x10) = to_bool (capPDIsMapped_CL (cap_page_directory_cap_lift ccap))) \<Longrightarrow> (cap_C.words_C ccap.[0] && 0xF = 9 \<and> cap_C.words_C ccap.[0] && 0x10 = 0x10) = (cap_get_tag ccap = 9 \<and> to_bool (capPDIsMapped_CL (cap_page_directory_cap_lift ccap)))
 2. cap_get_tag ccap = SCAST(32 signed \<rightarrow> 32) cap_page_directory_cap \<Longrightarrow> (cap_C.words_C ccap.[0] && 0x10 = 0x10) = to_bool (capPDIsMapped_CL (cap_page_directory_cap_lift ccap)) proof (prove)
goal (2 subgoals):
 1. (cap_C.words_C ccap.[0] && 0xF = 9 \<Longrightarrow> (cap_C.words_C ccap.[0] && 0x10 = 0x10) = to_bool (capPDIsMapped_CL (cap_page_directory_cap_lift ccap))) \<Longrightarrow> (cap_C.words_C ccap.[0] && 0xF = 9 \<and> cap_C.words_C ccap.[0] && 0x10 = 0x10) = (cap_C.words_C ccap.[0] && 0xF = 9 \<and> to_bool (capPDIsMapped_CL (cap_page_directory_cap_lift ccap)))
 2. cap_get_tag ccap = SCAST(32 signed \<rightarrow> 32) cap_page_directory_cap \<Longrightarrow> (cap_C.words_C ccap.[0] && 0x10 = 0x10) = to_bool (capPDIsMapped_CL (cap_page_directory_cap_lift ccap)) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>cap_C.words_C ccap.[0] && 0xF = 9 \<Longrightarrow> (cap_C.words_C ccap.[0] && 0x10 = 0x10) = to_bool (capPDIsMapped_CL (cap_page_directory_cap_lift ccap)); cap_C.words_C ccap.[0] && 0xF = 9\<rbrakk> \<Longrightarrow> (cap_C.words_C ccap.[0] && 0x10 = 0x10) = to_bool (capPDIsMapped_CL (cap_page_directory_cap_lift ccap))
 2. cap_get_tag ccap = SCAST(32 signed \<rightarrow> 32) cap_page_directory_cap \<Longrightarrow> (cap_C.words_C ccap.[0] && 0x10 = 0x10) = to_bool (capPDIsMapped_CL (cap_page_directory_cap_lift ccap)) proof (prove)
goal (1 subgoal):
 1. cap_get_tag ccap = SCAST(32 signed \<rightarrow> 32) cap_page_directory_cap \<Longrightarrow> (cap_C.words_C ccap.[0] && 0x10 = 0x10) = to_bool (capPDIsMapped_CL (cap_page_directory_cap_lift ccap)) proof (prove)
goal (1 subgoal):
 1. cap_get_tag ccap = SCAST(32 signed \<rightarrow> 32) cap_page_directory_cap \<Longrightarrow> (cap_C.words_C ccap.[0] && 0x10 = 0x10) = ((cap_C.words_C ccap.[0] >> 4) && 1 = 1) proof (prove)
goal (1 subgoal):
 1. (cap_C.words_C ccap.[0] && 0x10 = 0x10) = ((cap_C.words_C ccap.[0] >> 4) && 1 = 1) proof (prove)
goal:
No subgoals!