theory Machine_C

lemma invalidateCacheRange_I_ccorres:
  "ccorres dc xfdc (\<lambda>_. w1 \<le> w2 \<and> w3 \<le> w3 + (w2 - w1)
                      \<and> w1 && mask 5 = w3 && mask 5)
                   (\<lbrace>\<acute>start = w1\<rbrace> \<inter> \<lbrace>\<acute>end = w2\<rbrace> \<inter> \<lbrace>\<acute>pstart = w3\<rbrace>) []
           (doMachineOp (invalidateCacheRange_I w1 w2 w3))
           (Call invalidateCacheRange_I_'proc)" apply (rule ccorres_gen_asm[where G=\<top>, simplified]) apply (cinit' lift: start_' end_' pstart_') apply (clarsimp simp: word_sle_def whileAnno_def) apply (ccorres_remove_UNIV_guard) apply (simp add: invalidateCacheRange_I_def) apply csymbr apply (rule cacheRangeOp_ccorres) apply (rule empty_fail_invalidateByVA_I) apply clarsimp apply (cinitlift index_') apply (rule ccorres_guard_imp2) apply csymbr apply (ctac add: invalidateByVA_I_ccorres) apply (clarsimp simp: lineStart_def cacheLineBits_def shiftr_shiftl1
                          mask_out_sub_mask) apply (drule_tac s="w1 && mask 5" in sym, simp add: cache_range_lineIndex_helper) apply (vcg exspec=invalidateByVA_I_modifies) apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres dc xfdc (\<lambda>_. w1 \<le> w2 \<and> w3 \<le> w3 + (w2 - w1) \<and> w1 && mask 5 = w3 && mask 5) (\<lbrace>\<acute>start = w1\<rbrace> \<inter> \<lbrace>\<acute>end = w2\<rbrace> \<inter> \<lbrace>\<acute>pstart = w3\<rbrace>) [] (doMachineOp (invalidateCacheRange_I w1 w2 w3)) (Call invalidateCacheRange_I_'proc) proof (prove)
goal (1 subgoal):
 1. w1 \<le> w2 \<and> w3 \<le> w3 + (w2 - w1) \<and> w1 && mask 5 = w3 && mask 5 \<Longrightarrow> ccorres dc xfdc (\<lambda>_. True) (\<lbrace>\<acute>start = w1\<rbrace> \<inter> \<lbrace>\<acute>end = w2\<rbrace> \<inter> \<lbrace>\<acute>pstart = w3\<rbrace>) [] (doMachineOp (invalidateCacheRange_I w1 w2 w3)) (Call invalidateCacheRange_I_'proc) proof (prove)
goal (2 subgoals):
 1. \<And>pstart end start. \<lbrakk>w1 \<le> w2 \<and> w3 \<le> w3 + (w2 - w1) \<and> w1 && mask 5 = w3 && mask 5; pstart = w3; end = w2; start = w1\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q695 pstart end start) (?Q'695 pstart end start) [SKIP] (doMachineOp (invalidateCacheRange_I w1 w2 w3)) (\<acute>index :== start >> 5;;
WHILE \<acute>index < (end >> 5) + 1 DO
  \<acute>line :== \<acute>index << 5;;
CALL invalidateByVA_I_'proc(\<acute>line,pstart + (\<acute>line - start));;
\<acute>index :== \<acute>index + 1
OD)
 2. \<And>pstart end start s s'. \<lbrakk>w1 \<le> w2 \<and> w3 \<le> w3 + (w2 - w1) \<and> w1 && mask 5 = w3 && mask 5; pstart = w3; end = w2; start = w1; (s, s') \<in> rf_sr; True; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q695 pstart end start s \<and> s' \<in> ?Q'695 pstart end start proof (prove)
goal (2 subgoals):
 1. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q695 w3 w2 w1) (?Q'695 w3 w2 w1) [SKIP] (doMachineOp (invalidateCacheRange_I w1 w2 w3)) (\<acute>index :== w1 >> 5;;
While \<lbrace>\<acute>index < (w2 >> 5) + 1\<rbrace> (\<acute>line :== \<acute>index << 5;;
CALL invalidateByVA_I_'proc(\<acute>line,w3 + (\<acute>line - w1));;
\<acute>index :== \<acute>index + 1))
 2. \<And>pstart end start s s'. \<lbrakk>w1 \<le> w2 \<and> w3 \<le> w3 + (w2 - w1) \<and> w1 && mask 5 = w3 && mask 5; pstart = w3; end = w2; start = w1; (s, s') \<in> rf_sr; True; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q695 pstart end start s \<and> s' \<in> ?Q'695 pstart end start proof (prove)
goal (2 subgoals):
 1. \<And>rv'. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q695 w3 w2 w1) (?G'709 rv') [SKIP] (doMachineOp (invalidateCacheRange_I w1 w2 w3)) (\<acute>index :== w1 >> 5;;
While \<lbrace>\<acute>index < (w2 >> 5) + 1\<rbrace> (\<acute>line :== \<acute>index << 5;;
CALL invalidateByVA_I_'proc(\<acute>line,w3 + (\<acute>line - w1));;
\<acute>index :== \<acute>index + 1))
 2. \<And>pstart end start s s'. \<lbrakk>w1 \<le> w2 \<and> w3 \<le> w3 + (w2 - w1) \<and> w1 && mask 5 = w3 && mask 5; pstart = w3; end = w2; start = w1; (s, s') \<in> rf_sr; True; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q695 pstart end start s \<and> s' \<in> {s. s \<in> ?G'712 pstart end start}
flex-flex pairs:
?G'712 w3 w2 w1 \<equiv>\<^sup>? ?G'709 () proof (prove)
goal (2 subgoals):
 1. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q695 w3 w2 w1) (?G'709 ()) [SKIP] (doMachineOp (cacheRangeOp invalidateByVA_I w1 w2 w3)) (\<acute>index :== w1 >> 5;;
While \<lbrace>\<acute>index < (w2 >> 5) + 1\<rbrace> (\<acute>line :== \<acute>index << 5;;
CALL invalidateByVA_I_'proc(\<acute>line,w3 + (\<acute>line - w1));;
\<acute>index :== \<acute>index + 1))
 2. \<And>pstart end start s s'. \<lbrakk>w1 \<le> w2 \<and> w3 \<le> w3 + (w2 - w1) \<and> w1 && mask 5 = w3 && mask 5; pstart = w3; end = w2; start = w1; (s, s') \<in> rf_sr; True; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q695 pstart end start s \<and> s' \<in> {s. s \<in> ?G'712 pstart end start}
flex-flex pairs:
?G'712 w3 w2 w1 \<equiv>\<^sup>? ?G'709 () proof (prove)
goal (2 subgoals):
 1. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q695 w3 w2 w1) (?G'741 ()) [SKIP] (doMachineOp (cacheRangeOp invalidateByVA_I w1 w2 w3)) (While \<lbrace>\<acute>index < (w2 >> 5) + 1\<rbrace> (\<acute>line :== \<acute>index << 5;;
CALL invalidateByVA_I_'proc(\<acute>line,w3 + (\<acute>line - w1));;
\<acute>index :== \<acute>index + 1))
 2. \<And>pstart end start s s'. \<lbrakk>w1 \<le> w2 \<and> w3 \<le> w3 + (w2 - w1) \<and> w1 && mask 5 = w3 && mask 5; pstart = w3; end = w2; start = w1; (s, s') \<in> rf_sr; True; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q695 pstart end start s \<and> s' \<in> {s. s \<in> {s. index_'_update (\<lambda>_. start >> 5) s \<in> ?G'742 pstart end start}}
flex-flex pairs:
?G'742 w3 w2 w1 \<equiv>\<^sup>? ?G'741 () proof (prove)
goal (4 subgoals):
 1. \<And>x y. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5\<rbrakk> \<Longrightarrow> empty_fail (invalidateByVA_I x y)
 2. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5\<rbrakk> \<Longrightarrow> \<forall>n. ccorres dc xfdc (\<lambda>_. True) \<lbrace>\<acute>index = lineIndex w1 + word_of_nat n\<rbrace> [SKIP] (doMachineOp (invalidateByVA_I (lineStart w1 + word_of_nat n * 0x20) (lineStart w3 + word_of_nat n * 0x20))) (\<acute>line :== \<acute>index << 5;;
CALL invalidateByVA_I_'proc(\<acute>line,w3 + (\<acute>line - w1)))
 3. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5\<rbrakk> \<Longrightarrow> \<forall>s. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} \<acute>line :== \<acute>index << 5;;
CALL invalidateByVA_I_'proc(\<acute>line,w3 + (\<acute>line - w1)) \<lbrace>\<acute>index = \<^bsup>s\<^esup>index\<rbrace>
 4. \<And>pstart end start s s'. \<lbrakk>w1 \<le> w2 \<and> w3 \<le> w3 + (w2 - w1) \<and> w1 && mask 5 = w3 && mask 5; pstart = w3; end = w2; start = w1; (s, s') \<in> rf_sr; True; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (start \<le> end \<and> pstart \<le> pstart + (end - start) \<and> start && mask 5 = pstart && mask 5) \<and> s' \<in> {s. s \<in> {s. index_'_update (\<lambda>_. start >> 5) s \<in> \<lbrace>\<acute>index = start >> 5\<rbrace>}} proof (prove)
goal (3 subgoals):
 1. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5\<rbrakk> \<Longrightarrow> \<forall>n. ccorres dc xfdc (\<lambda>_. True) \<lbrace>\<acute>index = lineIndex w1 + word_of_nat n\<rbrace> [SKIP] (doMachineOp (invalidateByVA_I (lineStart w1 + word_of_nat n * 0x20) (lineStart w3 + word_of_nat n * 0x20))) (\<acute>line :== \<acute>index << 5;;
CALL invalidateByVA_I_'proc(\<acute>line,w3 + (\<acute>line - w1)))
 2. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5\<rbrakk> \<Longrightarrow> \<forall>s. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} \<acute>line :== \<acute>index << 5;;
CALL invalidateByVA_I_'proc(\<acute>line,w3 + (\<acute>line - w1)) \<lbrace>\<acute>index = \<^bsup>s\<^esup>index\<rbrace>
 3. \<And>pstart end start s s'. \<lbrakk>w1 \<le> w2 \<and> w3 \<le> w3 + (w2 - w1) \<and> w1 && mask 5 = w3 && mask 5; pstart = w3; end = w2; start = w1; (s, s') \<in> rf_sr; True; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (start \<le> end \<and> pstart \<le> pstart + (end - start) \<and> start && mask 5 = pstart && mask 5) \<and> s' \<in> {s. s \<in> {s. index_'_update (\<lambda>_. start >> 5) s \<in> \<lbrace>\<acute>index = start >> 5\<rbrace>}} proof (prove)
goal (3 subgoals):
 1. \<And>n. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5\<rbrakk> \<Longrightarrow> ccorres dc xfdc (\<lambda>_. True) \<lbrace>\<acute>index = lineIndex w1 + word_of_nat n\<rbrace> [SKIP] (doMachineOp (invalidateByVA_I (lineStart w1 + word_of_nat n * 0x20) (lineStart w3 + word_of_nat n * 0x20))) (\<acute>line :== \<acute>index << 5;;
CALL invalidateByVA_I_'proc(\<acute>line,w3 + (\<acute>line - w1)))
 2. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5\<rbrakk> \<Longrightarrow> \<forall>s. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} \<acute>line :== \<acute>index << 5;;
CALL invalidateByVA_I_'proc(\<acute>line,w3 + (\<acute>line - w1)) \<lbrace>\<acute>index = \<^bsup>s\<^esup>index\<rbrace>
 3. \<And>pstart end start s s'. \<lbrakk>w1 \<le> w2 \<and> w3 \<le> w3 + (w2 - w1) \<and> w1 && mask 5 = w3 && mask 5; pstart = w3; end = w2; start = w1; (s, s') \<in> rf_sr; True; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (start \<le> end \<and> pstart \<le> pstart + (end - start) \<and> start && mask 5 = pstart && mask 5) \<and> s' \<in> {s. s \<in> {s. index_'_update (\<lambda>_. start >> 5) s \<in> \<lbrace>\<acute>index = start >> 5\<rbrace>}} proof (prove)
goal (3 subgoals):
 1. \<And>n index. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5; index = lineIndex w1 + word_of_nat n\<rbrakk> \<Longrightarrow> ccorres dc xfdc (\<lambda>_. True) UNIV [SKIP] (doMachineOp (invalidateByVA_I (lineStart w1 + word_of_nat n * 0x20) (lineStart w3 + word_of_nat n * 0x20))) (\<acute>line :== index << 5;;
CALL invalidateByVA_I_'proc(\<acute>line,w3 + (\<acute>line - w1)))
 2. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5\<rbrakk> \<Longrightarrow> \<forall>s. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} \<acute>line :== \<acute>index << 5;;
CALL invalidateByVA_I_'proc(\<acute>line,w3 + (\<acute>line - w1)) \<lbrace>\<acute>index = \<^bsup>s\<^esup>index\<rbrace>
 3. \<And>pstart end start s s'. \<lbrakk>w1 \<le> w2 \<and> w3 \<le> w3 + (w2 - w1) \<and> w1 && mask 5 = w3 && mask 5; pstart = w3; end = w2; start = w1; (s, s') \<in> rf_sr; True; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (start \<le> end \<and> pstart \<le> pstart + (end - start) \<and> start && mask 5 = pstart && mask 5) \<and> s' \<in> {s. s \<in> {s. index_'_update (\<lambda>_. start >> 5) s \<in> \<lbrace>\<acute>index = start >> 5\<rbrace>}} proof (prove)
goal (4 subgoals):
 1. \<And>n index. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5; index = lineIndex w1 + word_of_nat n\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q873 n index) (?Q'873 n index) [SKIP] (doMachineOp (invalidateByVA_I (lineStart w1 + word_of_nat n * 0x20) (lineStart w3 + word_of_nat n * 0x20))) (\<acute>line :== index << 5;;
CALL invalidateByVA_I_'proc(\<acute>line,w3 + (\<acute>line - w1)))
 2. \<And>n index s s'. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5; index = lineIndex w1 + word_of_nat n; (s, s') \<in> rf_sr; True; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q873 n index s \<and> s' \<in> ?Q'873 n index
 3. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5\<rbrakk> \<Longrightarrow> \<forall>s. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} \<acute>line :== \<acute>index << 5;;
CALL invalidateByVA_I_'proc(\<acute>line,w3 + (\<acute>line - w1)) \<lbrace>\<acute>index = \<^bsup>s\<^esup>index\<rbrace>
 4. \<And>pstart end start s s'. \<lbrakk>w1 \<le> w2 \<and> w3 \<le> w3 + (w2 - w1) \<and> w1 && mask 5 = w3 && mask 5; pstart = w3; end = w2; start = w1; (s, s') \<in> rf_sr; True; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (start \<le> end \<and> pstart \<le> pstart + (end - start) \<and> start && mask 5 = pstart && mask 5) \<and> s' \<in> {s. s \<in> {s. index_'_update (\<lambda>_. start >> 5) s \<in> \<lbrace>\<acute>index = start >> 5\<rbrace>}} proof (prove)
goal (4 subgoals):
 1. \<And>n index. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5; index = lineIndex w1 + word_of_nat n\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q873 n index) (?G'878 n index) [SKIP] (doMachineOp (invalidateByVA_I (lineStart w1 + word_of_nat n * 0x20) (lineStart w3 + word_of_nat n * 0x20))) (CALL invalidateByVA_I_'proc(index << 5,w3 + ((index << 5) - w1)))
 2. \<And>n index s s'. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5; index = lineIndex w1 + word_of_nat n; (s, s') \<in> rf_sr; True; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q873 n index s \<and> s' \<in> {s. line_'_update (\<lambda>_. index << 5) s \<in> ?G'878 n index}
 3. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5\<rbrakk> \<Longrightarrow> \<forall>s. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} \<acute>line :== \<acute>index << 5;;
CALL invalidateByVA_I_'proc(\<acute>line,w3 + (\<acute>line - w1)) \<lbrace>\<acute>index = \<^bsup>s\<^esup>index\<rbrace>
 4. \<And>pstart end start s s'. \<lbrakk>w1 \<le> w2 \<and> w3 \<le> w3 + (w2 - w1) \<and> w1 && mask 5 = w3 && mask 5; pstart = w3; end = w2; start = w1; (s, s') \<in> rf_sr; True; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (start \<le> end \<and> pstart \<le> pstart + (end - start) \<and> start && mask 5 = pstart && mask 5) \<and> s' \<in> {s. s \<in> {s. index_'_update (\<lambda>_. start >> 5) s \<in> \<lbrace>\<acute>index = start >> 5\<rbrace>}} proof (prove)
goal (3 subgoals):
 1. \<And>n index s s'. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5; index = lineIndex w1 + word_of_nat n; (s, s') \<in> rf_sr; True; s' \<in> UNIV\<rbrakk> \<Longrightarrow> True \<and> s' \<in> {s. line_'_update (\<lambda>_. index << 5) s \<in> {s. paddr_'_update (\<lambda>_. w3 + ((index << 5) - w1)) (vaddr_'_update (\<lambda>_. index << 5) s) \<in> \<lbrace>\<acute>vaddr = lineStart w1 + word_of_nat n * 0x20\<rbrace> \<inter> \<lbrace>\<acute>paddr = lineStart w3 + word_of_nat n * 0x20\<rbrace>}}
 2. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5\<rbrakk> \<Longrightarrow> \<forall>s. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} \<acute>line :== \<acute>index << 5;;
CALL invalidateByVA_I_'proc(\<acute>line,w3 + (\<acute>line - w1)) \<lbrace>\<acute>index = \<^bsup>s\<^esup>index\<rbrace>
 3. \<And>pstart end start s s'. \<lbrakk>w1 \<le> w2 \<and> w3 \<le> w3 + (w2 - w1) \<and> w1 && mask 5 = w3 && mask 5; pstart = w3; end = w2; start = w1; (s, s') \<in> rf_sr; True; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (start \<le> end \<and> pstart \<le> pstart + (end - start) \<and> start && mask 5 = pstart && mask 5) \<and> s' \<in> {s. s \<in> {s. index_'_update (\<lambda>_. start >> 5) s \<in> \<lbrace>\<acute>index = start >> 5\<rbrace>}} proof (prove)
goal (3 subgoals):
 1. \<And>n s s'. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5; (s, s') \<in> rf_sr\<rbrakk> \<Longrightarrow> lineIndex w1 + word_of_nat n << 5 = w1 - (w3 && mask 5) + word_of_nat n * 0x20
 2. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5\<rbrakk> \<Longrightarrow> \<forall>s. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} \<acute>line :== \<acute>index << 5;;
CALL invalidateByVA_I_'proc(\<acute>line,w3 + (\<acute>line - w1)) \<lbrace>\<acute>index = \<^bsup>s\<^esup>index\<rbrace>
 3. \<And>pstart end start s s'. \<lbrakk>w1 \<le> w2 \<and> w3 \<le> w3 + (w2 - w1) \<and> w1 && mask 5 = w3 && mask 5; pstart = w3; end = w2; start = w1; (s, s') \<in> rf_sr; True; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (start \<le> end \<and> pstart \<le> pstart + (end - start) \<and> start && mask 5 = pstart && mask 5) \<and> s' \<in> {s. s \<in> {s. index_'_update (\<lambda>_. start >> 5) s \<in> \<lbrace>\<acute>index = start >> 5\<rbrace>}} proof (prove)
goal (2 subgoals):
 1. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5\<rbrakk> \<Longrightarrow> \<forall>s. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} \<acute>line :== \<acute>index << 5;;
CALL invalidateByVA_I_'proc(\<acute>line,w3 + (\<acute>line - w1)) \<lbrace>\<acute>index = \<^bsup>s\<^esup>index\<rbrace>
 2. \<And>pstart end start s s'. \<lbrakk>w1 \<le> w2 \<and> w3 \<le> w3 + (w2 - w1) \<and> w1 && mask 5 = w3 && mask 5; pstart = w3; end = w2; start = w1; (s, s') \<in> rf_sr; True; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (start \<le> end \<and> pstart \<le> pstart + (end - start) \<and> start && mask 5 = pstart && mask 5) \<and> s' \<in> {s. s \<in> {s. index_'_update (\<lambda>_. start >> 5) s \<in> \<lbrace>\<acute>index = start >> 5\<rbrace>}} proof (prove)
goal (1 subgoal):
 1. \<And>pstart end start s s'. \<lbrakk>w1 \<le> w2 \<and> w3 \<le> w3 + (w2 - w1) \<and> w1 && mask 5 = w3 && mask 5; pstart = w3; end = w2; start = w1; (s, s') \<in> rf_sr; True; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (start \<le> end \<and> pstart \<le> pstart + (end - start) \<and> start && mask 5 = pstart && mask 5) \<and> s' \<in> {s. s \<in> {s. index_'_update (\<lambda>_. start >> 5) s \<in> \<lbrace>\<acute>index = start >> 5\<rbrace>}} proof (prove)
goal:
No subgoals!