theory Machine_C

lemma cleanCacheRange_PoU_ccorres:
  "ccorres dc xfdc ((\<lambda>s. unat (w2 - w1) \<le> gsMaxObjectSize s)
                    and (\<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 (cleanCacheRange_PoU w1 w2 w3))
           (Call cleanCacheRange_PoU_'proc)" apply (rule ccorres_gen_asm) apply (cinit' lift: start_' end_' pstart_') apply (clarsimp simp: word_sle_def whileAnno_def) apply (ccorres_remove_UNIV_guard) apply (rule ccorres_Guard_Seq) apply (rule ccorres_basic_srnoop2, simp) apply (simp add: cleanCacheRange_PoU_def) apply csymbr apply (rule cacheRangeOp_ccorres) apply (rule empty_fail_cleanByVA_PoU) apply clarsimp apply (cinitlift index_') apply (rule ccorres_guard_imp2) apply csymbr apply (ctac add: cleanByVA_PoU_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=cleanByVA_PoU_modifies) apply clarsimp apply (frule(1) ghost_assertion_size_logic) apply (clarsimp simp: o_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres dc xfdc ((\<lambda>s. unat (w2 - w1) \<le> gsMaxObjectSize s) and (\<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 (cleanCacheRange_PoU w1 w2 w3)) (Call cleanCacheRange_PoU_'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>s. unat (w2 - w1) \<le> gsMaxObjectSize s) (\<lbrace>\<acute>start = w1\<rbrace> \<inter> \<lbrace>\<acute>end = w2\<rbrace> \<inter> \<lbrace>\<acute>pstart = w3\<rbrace>) [] (doMachineOp (cleanCacheRange_PoU w1 w2 w3)) (Call cleanCacheRange_PoU_'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 (?Q797 pstart end start) (?Q'797 pstart end start) [SKIP] (doMachineOp (cleanCacheRange_PoU w1 w2 w3)) (Guard GhostStateError \<lbrace>(gs_get_assn cap_get_capSizeBits_'proc \<acute>ghost'state = 0 \<or> end - start \<le> gs_get_assn cap_get_capSizeBits_'proc \<acute>ghost'state) \<and> start \<le> end \<and> pstart \<le> pstart + (end - start)\<rbrace> (\<acute>globals :== ghost'state_'_update id);;
(\<acute>index :== start >> 5;;
WHILE \<acute>index < (end >> 5) + 1 DO
  \<acute>line :== \<acute>index << 5;;
CALL cleanByVA_PoU_'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; unat (w2 - w1) \<le> gsMaxObjectSize s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q797 pstart end start s \<and> s' \<in> ?Q'797 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 (?Q797 w3 w2 w1) (?Q'797 w3 w2 w1) [SKIP] (doMachineOp (cleanCacheRange_PoU w1 w2 w3)) (Guard GhostStateError \<lbrace>gs_get_assn cap_get_capSizeBits_'proc \<acute>ghost'state = 0 \<or> w2 - w1 \<le> gs_get_assn cap_get_capSizeBits_'proc \<acute>ghost'state\<rbrace> (\<acute>globals :== ghost'state_'_update id);;
(\<acute>index :== w1 >> 5;;
While \<lbrace>\<acute>index < (w2 >> 5) + 1\<rbrace> (\<acute>line :== \<acute>index << 5;;
CALL cleanByVA_PoU_'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; unat (w2 - w1) \<le> gsMaxObjectSize s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q797 pstart end start s \<and> s' \<in> ?Q'797 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 (?Q797 w3 w2 w1) (?G'811 rv') [SKIP] (doMachineOp (cleanCacheRange_PoU w1 w2 w3)) (Guard GhostStateError \<lbrace>gs_get_assn cap_get_capSizeBits_'proc \<acute>ghost'state = 0 \<or> w2 - w1 \<le> gs_get_assn cap_get_capSizeBits_'proc \<acute>ghost'state\<rbrace> (\<acute>globals :== ghost'state_'_update id);;
(\<acute>index :== w1 >> 5;;
While \<lbrace>\<acute>index < (w2 >> 5) + 1\<rbrace> (\<acute>line :== \<acute>index << 5;;
CALL cleanByVA_PoU_'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; unat (w2 - w1) \<le> gsMaxObjectSize s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q797 pstart end start s \<and> s' \<in> {s. s \<in> ?G'814 pstart end start}
flex-flex pairs:
?G'814 w3 w2 w1 \<equiv>\<^sup>? ?G'811 () 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 (?Q797 w3 w2 w1) (?C'847 rv') [SKIP] (doMachineOp (cleanCacheRange_PoU w1 w2 w3)) (\<acute>globals :== ghost'state_'_update id;;
(\<acute>index :== w1 >> 5;;
While \<lbrace>\<acute>index < (w2 >> 5) + 1\<rbrace> (\<acute>line :== \<acute>index << 5;;
CALL cleanByVA_PoU_'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; unat (w2 - w1) \<le> gsMaxObjectSize s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q797 pstart end start s \<and> s' \<in> {s. s \<in> ?C'848 pstart end start \<inter> \<lbrace>gs_get_assn cap_get_capSizeBits_'proc \<acute>ghost'state = 0 \<or> end - start \<le> gs_get_assn cap_get_capSizeBits_'proc \<acute>ghost'state\<rbrace>}
flex-flex pairs:
?C'848 w3 w2 w1 \<equiv>\<^sup>? ?C'847 () 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 (?Q797 w3 w2 w1) (?G'851 rv') [SKIP] (doMachineOp (cleanCacheRange_PoU w1 w2 w3)) (\<acute>index :== w1 >> 5;;
While \<lbrace>\<acute>index < (w2 >> 5) + 1\<rbrace> (\<acute>line :== \<acute>index << 5;;
CALL cleanByVA_PoU_'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; unat (w2 - w1) \<le> gsMaxObjectSize s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q797 pstart end start s \<and> s' \<in> {s. s \<in> {s. globals_update (ghost'state_'_update id) s \<in> ?G'854 pstart end start} \<inter> \<lbrace>gs_get_assn cap_get_capSizeBits_'proc \<acute>ghost'state = 0 \<or> end - start \<le> gs_get_assn cap_get_capSizeBits_'proc \<acute>ghost'state\<rbrace>}
flex-flex pairs:
?G'854 w3 w2 w1 \<equiv>\<^sup>? ?G'851 () 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 (?Q797 w3 w2 w1) (?G'851 ()) [SKIP] (doMachineOp (cacheRangeOp cleanByVA_PoU w1 w2 w3)) (\<acute>index :== w1 >> 5;;
While \<lbrace>\<acute>index < (w2 >> 5) + 1\<rbrace> (\<acute>line :== \<acute>index << 5;;
CALL cleanByVA_PoU_'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; unat (w2 - w1) \<le> gsMaxObjectSize s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q797 pstart end start s \<and> s' \<in> {s. s \<in> {s. globals_update (ghost'state_'_update id) s \<in> ?G'854 pstart end start} \<inter> \<lbrace>gs_get_assn cap_get_capSizeBits_'proc \<acute>ghost'state = 0 \<or> end - start \<le> gs_get_assn cap_get_capSizeBits_'proc \<acute>ghost'state\<rbrace>}
flex-flex pairs:
?G'854 w3 w2 w1 \<equiv>\<^sup>? ?G'851 () 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 (?Q797 w3 w2 w1) (?G'864 ()) [SKIP] (doMachineOp (cacheRangeOp cleanByVA_PoU w1 w2 w3)) (While \<lbrace>\<acute>index < (w2 >> 5) + 1\<rbrace> (\<acute>line :== \<acute>index << 5;;
CALL cleanByVA_PoU_'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; unat (w2 - w1) \<le> gsMaxObjectSize s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q797 pstart end start s \<and> s' \<in> {s. s \<in> {s. globals_update (ghost'state_'_update id) s \<in> {s. index_'_update (\<lambda>_. start >> 5) s \<in> ?G'865 pstart end start}} \<inter> \<lbrace>gs_get_assn cap_get_capSizeBits_'proc \<acute>ghost'state = 0 \<or> end - start \<le> gs_get_assn cap_get_capSizeBits_'proc \<acute>ghost'state\<rbrace>}
flex-flex pairs:
?G'865 w3 w2 w1 \<equiv>\<^sup>? ?G'864 () 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 (cleanByVA_PoU 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 (cleanByVA_PoU (lineStart w1 + word_of_nat n * 0x20) (lineStart w3 + word_of_nat n * 0x20))) (\<acute>line :== \<acute>index << 5;;
CALL cleanByVA_PoU_'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 cleanByVA_PoU_'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; unat (w2 - w1) \<le> gsMaxObjectSize s; 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. globals_update (ghost'state_'_update id) s \<in> {s. index_'_update (\<lambda>_. start >> 5) s \<in> \<lbrace>\<acute>index = start >> 5\<rbrace>}} \<inter> \<lbrace>gs_get_assn cap_get_capSizeBits_'proc \<acute>ghost'state = 0 \<or> end - start \<le> gs_get_assn cap_get_capSizeBits_'proc \<acute>ghost'state\<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 (cleanByVA_PoU (lineStart w1 + word_of_nat n * 0x20) (lineStart w3 + word_of_nat n * 0x20))) (\<acute>line :== \<acute>index << 5;;
CALL cleanByVA_PoU_'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 cleanByVA_PoU_'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; unat (w2 - w1) \<le> gsMaxObjectSize s; 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. globals_update (ghost'state_'_update id) s \<in> {s. index_'_update (\<lambda>_. start >> 5) s \<in> \<lbrace>\<acute>index = start >> 5\<rbrace>}} \<inter> \<lbrace>gs_get_assn cap_get_capSizeBits_'proc \<acute>ghost'state = 0 \<or> end - start \<le> gs_get_assn cap_get_capSizeBits_'proc \<acute>ghost'state\<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 (cleanByVA_PoU (lineStart w1 + word_of_nat n * 0x20) (lineStart w3 + word_of_nat n * 0x20))) (\<acute>line :== \<acute>index << 5;;
CALL cleanByVA_PoU_'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 cleanByVA_PoU_'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; unat (w2 - w1) \<le> gsMaxObjectSize s; 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. globals_update (ghost'state_'_update id) s \<in> {s. index_'_update (\<lambda>_. start >> 5) s \<in> \<lbrace>\<acute>index = start >> 5\<rbrace>}} \<inter> \<lbrace>gs_get_assn cap_get_capSizeBits_'proc \<acute>ghost'state = 0 \<or> end - start \<le> gs_get_assn cap_get_capSizeBits_'proc \<acute>ghost'state\<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 (cleanByVA_PoU (lineStart w1 + word_of_nat n * 0x20) (lineStart w3 + word_of_nat n * 0x20))) (\<acute>line :== index << 5;;
CALL cleanByVA_PoU_'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 cleanByVA_PoU_'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; unat (w2 - w1) \<le> gsMaxObjectSize s; 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. globals_update (ghost'state_'_update id) s \<in> {s. index_'_update (\<lambda>_. start >> 5) s \<in> \<lbrace>\<acute>index = start >> 5\<rbrace>}} \<inter> \<lbrace>gs_get_assn cap_get_capSizeBits_'proc \<acute>ghost'state = 0 \<or> end - start \<le> gs_get_assn cap_get_capSizeBits_'proc \<acute>ghost'state\<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 (?Q996 n index) (?Q'996 n index) [SKIP] (doMachineOp (cleanByVA_PoU (lineStart w1 + word_of_nat n * 0x20) (lineStart w3 + word_of_nat n * 0x20))) (\<acute>line :== index << 5;;
CALL cleanByVA_PoU_'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> ?Q996 n index s \<and> s' \<in> ?Q'996 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 cleanByVA_PoU_'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; unat (w2 - w1) \<le> gsMaxObjectSize s; 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. globals_update (ghost'state_'_update id) s \<in> {s. index_'_update (\<lambda>_. start >> 5) s \<in> \<lbrace>\<acute>index = start >> 5\<rbrace>}} \<inter> \<lbrace>gs_get_assn cap_get_capSizeBits_'proc \<acute>ghost'state = 0 \<or> end - start \<le> gs_get_assn cap_get_capSizeBits_'proc \<acute>ghost'state\<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 (?Q996 n index) (?G'1001 n index) [SKIP] (doMachineOp (cleanByVA_PoU (lineStart w1 + word_of_nat n * 0x20) (lineStart w3 + word_of_nat n * 0x20))) (CALL cleanByVA_PoU_'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> ?Q996 n index s \<and> s' \<in> {s. line_'_update (\<lambda>_. index << 5) s \<in> ?G'1001 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 cleanByVA_PoU_'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; unat (w2 - w1) \<le> gsMaxObjectSize s; 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. globals_update (ghost'state_'_update id) s \<in> {s. index_'_update (\<lambda>_. start >> 5) s \<in> \<lbrace>\<acute>index = start >> 5\<rbrace>}} \<inter> \<lbrace>gs_get_assn cap_get_capSizeBits_'proc \<acute>ghost'state = 0 \<or> end - start \<le> gs_get_assn cap_get_capSizeBits_'proc \<acute>ghost'state\<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 cleanByVA_PoU_'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; unat (w2 - w1) \<le> gsMaxObjectSize s; 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. globals_update (ghost'state_'_update id) s \<in> {s. index_'_update (\<lambda>_. start >> 5) s \<in> \<lbrace>\<acute>index = start >> 5\<rbrace>}} \<inter> \<lbrace>gs_get_assn cap_get_capSizeBits_'proc \<acute>ghost'state = 0 \<or> end - start \<le> gs_get_assn cap_get_capSizeBits_'proc \<acute>ghost'state\<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 cleanByVA_PoU_'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; unat (w2 - w1) \<le> gsMaxObjectSize s; 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. globals_update (ghost'state_'_update id) s \<in> {s. index_'_update (\<lambda>_. start >> 5) s \<in> \<lbrace>\<acute>index = start >> 5\<rbrace>}} \<inter> \<lbrace>gs_get_assn cap_get_capSizeBits_'proc \<acute>ghost'state = 0 \<or> end - start \<le> gs_get_assn cap_get_capSizeBits_'proc \<acute>ghost'state\<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 cleanByVA_PoU_'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; unat (w2 - w1) \<le> gsMaxObjectSize s; 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. globals_update (ghost'state_'_update id) s \<in> {s. index_'_update (\<lambda>_. start >> 5) s \<in> \<lbrace>\<acute>index = start >> 5\<rbrace>}} \<inter> \<lbrace>gs_get_assn cap_get_capSizeBits_'proc \<acute>ghost'state = 0 \<or> end - start \<le> gs_get_assn cap_get_capSizeBits_'proc \<acute>ghost'state\<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; unat (w2 - w1) \<le> gsMaxObjectSize s; 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. globals_update (ghost'state_'_update id) s \<in> {s. index_'_update (\<lambda>_. start >> 5) s \<in> \<lbrace>\<acute>index = start >> 5\<rbrace>}} \<inter> \<lbrace>gs_get_assn cap_get_capSizeBits_'proc \<acute>ghost'state = 0 \<or> end - start \<le> gs_get_assn cap_get_capSizeBits_'proc \<acute>ghost'state\<rbrace>} proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; unat (w2 - w1) \<le> gsMaxObjectSize s; w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5; \<not> w2 - w1 \<le> ghost_assertion_data_get cap_get_capSizeBits_'proc (\<lambda>a. snd (snd a)) (ghost'state_' (globals s'))\<rbrakk> \<Longrightarrow> ghost_assertion_data_get cap_get_capSizeBits_'proc (\<lambda>a. snd (snd a)) (ghost'state_' (globals s')) = 0 proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; unat (w2 - w1) \<le> gsMaxObjectSize s; w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5; \<not> w2 - w1 \<le> ghost_assertion_data_get cap_get_capSizeBits_'proc (\<lambda>a. snd (snd a)) (ghost'state_' (globals s')); gs_get_assn cap_get_capSizeBits_'proc (ghost'state_' (globals s')) = 0 \<or> w2 - w1 \<le> gs_get_assn cap_get_capSizeBits_'proc (ghost'state_' (globals s'))\<rbrakk> \<Longrightarrow> ghost_assertion_data_get cap_get_capSizeBits_'proc (\<lambda>a. snd (snd a)) (ghost'state_' (globals s')) = 0 proof (prove)
goal:
No subgoals!