theory Machine_C

lemma cleanInvalidateCacheRange_RAM_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 \<and> unat (w2 - w2) \<le> gsMaxObjectSize s))
                   (\<lbrace>\<acute>start = w1\<rbrace> \<inter> \<lbrace>\<acute>end = w2\<rbrace> \<inter> \<lbrace>\<acute>pstart = w3\<rbrace>) []
           (doMachineOp (cleanInvalidateCacheRange_RAM w1 w2 w3))
           (Call cleanInvalidateCacheRange_RAM_'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_srnoop) apply (simp add: cleanInvalidateCacheRange_RAM_def doMachineOp_bind
                      empty_fail_dsb empty_fail_cleanInvalidateL2Range
                      empty_fail_cleanInvalByVA empty_fail_cond) apply (ctac (no_vcg) add: cleanCacheRange_PoC_ccorres) apply (ctac (no_vcg) add: dsb_ccorres) apply (ctac (no_vcg) add: cleanInvalidateL2Range_ccorres) apply csymbr apply (rule ccorres_split_nothrow_novcg) apply (rule cacheRangeOp_ccorres) apply (rule empty_fail_cleanInvalByVA) apply clarsimp apply (cinitlift index_') apply (rule ccorres_guard_imp2) apply csymbr apply (ctac add: cleanInvalByVA_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=cleanInvalByVA_modifies) apply (rule ceqv_refl) apply (ctac (no_vcg) add: dsb_ccorres) apply (wp | clarsimp simp: guard_is_UNIVI)+ 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 \<and> unat (w2 - w2) \<le> gsMaxObjectSize s)) (\<lbrace>\<acute>start = w1\<rbrace> \<inter> \<lbrace>\<acute>end = w2\<rbrace> \<inter> \<lbrace>\<acute>pstart = w3\<rbrace>) [] (doMachineOp (cleanInvalidateCacheRange_RAM w1 w2 w3)) (Call cleanInvalidateCacheRange_RAM_'proc) proof (prove)
goal (1 subgoal):
 1. w1 \<le> w2 \<and> w3 \<le> w3 + (w2 - w1) \<and> w1 && mask 5 = w3 && mask 5 \<and> unat (w2 - w2) \<le> gsMaxObjectSize s \<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 (cleanInvalidateCacheRange_RAM w1 w2 w3)) (Call cleanInvalidateCacheRange_RAM_'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 (?Q1177 pstart end start) (?Q'1177 pstart end start) [SKIP] (doMachineOp (cleanInvalidateCacheRange_RAM 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\<rbrace> (\<acute>globals :== ghost'state_'_update id);;
(CALL cleanCacheRange_PoC_'proc(start,end,pstart);;
(CALL dsb_'proc();;
(CALL plat_cleanInvalidateL2Range_'proc(pstart,pstart + (end - start));;
(\<acute>index :== start >> 5;;
(WHILE \<acute>index < (end >> 5) + 1 DO
  \<acute>line :== \<acute>index << 5;;
CALL cleanInvalByVA_'proc(\<acute>line,pstart + (\<acute>line - start));;
\<acute>index :== \<acute>index + 1
OD;;
CALL dsb_'proc()))))))
 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> ?Q1177 pstart end start s \<and> s' \<in> ?Q'1177 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 (?Q1177 w3 w2 w1) (?Q'1177 w3 w2 w1) [SKIP] (doMachineOp (cleanInvalidateCacheRange_RAM 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);;
(CALL cleanCacheRange_PoC_'proc(w1,w2,w3);;
(CALL dsb_'proc();;
(CALL plat_cleanInvalidateL2Range_'proc(w3,w3 + (w2 - w1));;
(\<acute>index :== w1 >> 5;;
(While \<lbrace>\<acute>index < (w2 >> 5) + 1\<rbrace> (\<acute>line :== \<acute>index << 5;;
CALL cleanInvalByVA_'proc(\<acute>line,w3 + (\<acute>line - w1));;
\<acute>index :== \<acute>index + 1);;
CALL dsb_'proc()))))))
 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> ?Q1177 pstart end start s \<and> s' \<in> ?Q'1177 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 (?Q1177 w3 w2 w1) (?G'1191 rv') [SKIP] (doMachineOp (cleanInvalidateCacheRange_RAM 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);;
(CALL cleanCacheRange_PoC_'proc(w1,w2,w3);;
(CALL dsb_'proc();;
(CALL plat_cleanInvalidateL2Range_'proc(w3,w3 + (w2 - w1));;
(\<acute>index :== w1 >> 5;;
(While \<lbrace>\<acute>index < (w2 >> 5) + 1\<rbrace> (\<acute>line :== \<acute>index << 5;;
CALL cleanInvalByVA_'proc(\<acute>line,w3 + (\<acute>line - w1));;
\<acute>index :== \<acute>index + 1);;
CALL dsb_'proc()))))))
 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> ?Q1177 pstart end start s \<and> s' \<in> {s. s \<in> ?G'1194 pstart end start}
flex-flex pairs:
?G'1194 w3 w2 w1 \<equiv>\<^sup>? ?G'1191 () 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 (?Q1177 w3 w2 w1) (?C'1247 rv') [SKIP] (doMachineOp (cleanInvalidateCacheRange_RAM w1 w2 w3)) (\<acute>globals :== ghost'state_'_update id;;
(CALL cleanCacheRange_PoC_'proc(w1,w2,w3);;
(CALL dsb_'proc();;
(CALL plat_cleanInvalidateL2Range_'proc(w3,w3 + (w2 - w1));;
(\<acute>index :== w1 >> 5;;
(While \<lbrace>\<acute>index < (w2 >> 5) + 1\<rbrace> (\<acute>line :== \<acute>index << 5;;
CALL cleanInvalByVA_'proc(\<acute>line,w3 + (\<acute>line - w1));;
\<acute>index :== \<acute>index + 1);;
CALL dsb_'proc()))))))
 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> ?Q1177 pstart end start s \<and> s' \<in> {s. s \<in> ?C'1248 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'1248 w3 w2 w1 \<equiv>\<^sup>? ?C'1247 () proof (prove)
goal (4 subgoals):
 1. \<And>rv'. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q1177 w3 w2 w1) (?C'1247 rv') [SKIP] (doMachineOp (cleanInvalidateCacheRange_RAM w1 w2 w3)) (CALL cleanCacheRange_PoC_'proc(w1,w2,w3);;
(CALL dsb_'proc();;
(CALL plat_cleanInvalidateL2Range_'proc(w3,w3 + (w2 - w1));;
(\<acute>index :== w1 >> 5;;
(While \<lbrace>\<acute>index < (w2 >> 5) + 1\<rbrace> (\<acute>line :== \<acute>index << 5;;
CALL cleanInvalByVA_'proc(\<acute>line,w3 + (\<acute>line - w1));;
\<acute>index :== \<acute>index + 1);;
CALL dsb_'proc())))))
 2. \<And>rv' s'. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5\<rbrakk> \<Longrightarrow> globals (globals_update (ghost'state_'_update id) s') = globals s'
 3. \<And>rv' s'. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5; s' \<in> ?C'1247 rv'\<rbrakk> \<Longrightarrow> globals_update (ghost'state_'_update id) s' \<in> ?C'1247 rv'
 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> ?Q1177 pstart end start s \<and> s' \<in> {s. s \<in> ?C'1248 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'1248 w3 w2 w1 \<equiv>\<^sup>? ?C'1247 () proof (prove)
goal (4 subgoals):
 1. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q1177 w3 w2 w1) (?C'1247 ()) [SKIP] (do rv <- doMachineOp (cleanCacheRange_PoC w1 w2 w3);
rv <- doMachineOp dsb;
rv <- doMachineOp (cleanInvalidateL2Range w3 (w3 + (w2 - w1)));
rv <- doMachineOp (cacheRangeOp cleanInvalByVA w1 w2 w3);
doMachineOp dsb
od) (CALL cleanCacheRange_PoC_'proc(w1,w2,w3);;
(CALL dsb_'proc();;
(CALL plat_cleanInvalidateL2Range_'proc(w3,w3 + (w2 - w1));;
(\<acute>index :== w1 >> 5;;
(While \<lbrace>\<acute>index < (w2 >> 5) + 1\<rbrace> (\<acute>line :== \<acute>index << 5;;
CALL cleanInvalByVA_'proc(\<acute>line,w3 + (\<acute>line - w1));;
\<acute>index :== \<acute>index + 1);;
CALL dsb_'proc())))))
 2. \<And>rv' s'. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5\<rbrakk> \<Longrightarrow> globals (globals_update (ghost'state_'_update id) s') = globals s'
 3. \<And>rv' s'. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5; s' \<in> ?C'1247 rv'\<rbrakk> \<Longrightarrow> globals_update (ghost'state_'_update id) s' \<in> ?C'1247 rv'
 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> ?Q1177 pstart end start s \<and> s' \<in> {s. s \<in> ?C'1248 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'1248 w3 w2 w1 \<equiv>\<^sup>? ?C'1247 () proof (prove)
goal (5 subgoals):
 1. \<And>rv xfdca. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5; dc rv xfdca\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q1258 rv) (?Q'1258 rv xfdca) [SKIP] (do rv <- doMachineOp dsb;
rv <- doMachineOp (cleanInvalidateL2Range w3 (w3 + (w2 - w1)));
rv <- doMachineOp (cacheRangeOp cleanInvalByVA w1 w2 w3);
doMachineOp dsb
od) (CALL dsb_'proc();;
(CALL plat_cleanInvalidateL2Range_'proc(w3,w3 + (w2 - w1));;
(\<acute>index :== w1 >> 5;;
(While \<lbrace>\<acute>index < (w2 >> 5) + 1\<rbrace> (\<acute>line :== \<acute>index << 5;;
CALL cleanInvalByVA_'proc(\<acute>line,w3 + (\<acute>line - w1));;
\<acute>index :== \<acute>index + 1);;
CALL dsb_'proc()))))
 2. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5\<rbrakk> \<Longrightarrow> \<lbrace>?R1273 w3 w2 w1\<rbrace> doMachineOp (cleanCacheRange_PoC w1 w2 w3) \<lbrace>?Q1258\<rbrace>
 3. \<And>rv' s'. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5\<rbrakk> \<Longrightarrow> globals (globals_update (ghost'state_'_update id) s') = globals s'
 4. \<And>rv' s'. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5; s' \<in> {s. pstart_'_update (\<lambda>_. w3) (end_'_update (\<lambda>_. w2) (start_'_update (\<lambda>_. w1) s)) \<in> \<lbrace>\<acute>start = w1\<rbrace> \<inter> \<lbrace>\<acute>end = w2\<rbrace> \<inter> \<lbrace>\<acute>pstart = w3\<rbrace>} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> ?Q'1267 rv' t rv}\<rbrakk> \<Longrightarrow> globals_update (ghost'state_'_update id) s' \<in> {s. pstart_'_update (\<lambda>_. w3) (end_'_update (\<lambda>_. w2) (start_'_update (\<lambda>_. w1) s)) \<in> \<lbrace>\<acute>start = w1\<rbrace> \<inter> \<lbrace>\<acute>end = w2\<rbrace> \<inter> \<lbrace>\<acute>pstart = w3\<rbrace>} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> ?Q'1267 rv' t rv}
 5. \<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> ((\<lambda>a. start \<le> end \<and> pstart \<le> pstart + (end - start) \<and> start && mask 5 = pstart && mask 5) and ?R1273 pstart end start) s \<and> s' \<in> {s. s \<in> {s. pstart_'_update (\<lambda>_. pstart) (end_'_update (\<lambda>_. end) (start_'_update (\<lambda>_. start) s)) \<in> \<lbrace>\<acute>start = start\<rbrace> \<inter> \<lbrace>\<acute>end = end\<rbrace> \<inter> \<lbrace>\<acute>pstart = pstart\<rbrace>} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> ?Q'1270 pstart end start t rv} \<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:
?Q'1270 w3 w2 w1 \<equiv>\<^sup>? ?Q'1267 ()
?Q'1267 () \<equiv>\<^sup>? \<lambda>t rv. ?Q'1258 rv (xfdc t) proof (prove)
goal (6 subgoals):
 1. \<And>rv xfdca rva xfdcb. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5; dc rv xfdca; dc rva xfdcb\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q1304 rv xfdca rva) (?Q'1304 rv xfdca rva xfdcb) [SKIP] (do rv <- doMachineOp (cleanInvalidateL2Range w3 (w3 + (w2 - w1)));
rv <- doMachineOp (cacheRangeOp cleanInvalByVA w1 w2 w3);
doMachineOp dsb
od) (CALL plat_cleanInvalidateL2Range_'proc(w3,w3 + (w2 - w1));;
(\<acute>index :== w1 >> 5;;
(While \<lbrace>\<acute>index < (w2 >> 5) + 1\<rbrace> (\<acute>line :== \<acute>index << 5;;
CALL cleanInvalByVA_'proc(\<acute>line,w3 + (\<acute>line - w1));;
\<acute>index :== \<acute>index + 1);;
CALL dsb_'proc())))
 2. \<And>rv xfdc. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5; dc rv xfdc\<rbrakk> \<Longrightarrow> \<lbrace>?R1314 rv\<rbrace> doMachineOp dsb \<lbrace>?Q1304 rv xfdc\<rbrace>
 3. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5\<rbrakk> \<Longrightarrow> \<lbrace>?R1273 w3 w2 w1\<rbrace> doMachineOp (cleanCacheRange_PoC w1 w2 w3) \<lbrace>\<lambda>a. (\<lambda>a. True) and ?R1314 a\<rbrace>
 4. \<And>rv' s'. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5\<rbrakk> \<Longrightarrow> globals (globals_update (ghost'state_'_update id) s') = globals s'
 5. \<And>rv' s'. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5; s' \<in> {s. pstart_'_update (\<lambda>_. w3) (end_'_update (\<lambda>_. w2) (start_'_update (\<lambda>_. w1) s)) \<in> \<lbrace>\<acute>start = w1\<rbrace> \<inter> \<lbrace>\<acute>end = w2\<rbrace> \<inter> \<lbrace>\<acute>pstart = w3\<rbrace>} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> {s. s \<in> UNIV} \<inter> {s'. \<forall>ta rva. dc rva (xfdc ta) \<longrightarrow> s'\<lparr>globals := globals ta\<rparr> \<in> ?Q'1317 rv' t rv ta rva}}\<rbrakk> \<Longrightarrow> globals_update (ghost'state_'_update id) s' \<in> {s. pstart_'_update (\<lambda>_. w3) (end_'_update (\<lambda>_. w2) (start_'_update (\<lambda>_. w1) s)) \<in> \<lbrace>\<acute>start = w1\<rbrace> \<inter> \<lbrace>\<acute>end = w2\<rbrace> \<inter> \<lbrace>\<acute>pstart = w3\<rbrace>} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> {s. s \<in> UNIV} \<inter> {s'. \<forall>ta rva. dc rva (xfdc ta) \<longrightarrow> s'\<lparr>globals := globals ta\<rparr> \<in> ?Q'1317 rv' t rv ta rva}}
 6. \<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> ((\<lambda>a. start \<le> end \<and> pstart \<le> pstart + (end - start) \<and> start && mask 5 = pstart && mask 5) and ?R1273 pstart end start) s \<and> s' \<in> {s. s \<in> {s. pstart_'_update (\<lambda>_. pstart) (end_'_update (\<lambda>_. end) (start_'_update (\<lambda>_. start) s)) \<in> \<lbrace>\<acute>start = start\<rbrace> \<inter> \<lbrace>\<acute>end = end\<rbrace> \<inter> \<lbrace>\<acute>pstart = pstart\<rbrace>} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> {s. s \<in> UNIV} \<inter> {s'. \<forall>ta rva. dc rva (xfdc ta) \<longrightarrow> s'\<lparr>globals := globals ta\<rparr> \<in> ?Q'1320 pstart end start t rv ta rva}} \<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:
?Q'1320 w3 w2 w1 \<equiv>\<^sup>? ?Q'1317 ()
?Q'1317 () \<equiv>\<^sup>? \<lambda>t rv ta rva. ?Q'1304 rv (xfdc t) rva (xfdc ta) proof (prove)
goal (7 subgoals):
 1. \<And>rv xfdca rva xfdcb rvb xfdcc. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5; dc rv xfdca; dc rva xfdcb; dc rvb xfdcc\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q1353 rv xfdca rva xfdcb rvb) (?Q'1353 rv xfdca rva xfdcb rvb xfdcc) [SKIP] (do rv <- doMachineOp (cacheRangeOp cleanInvalByVA w1 w2 w3);
doMachineOp dsb
od) (\<acute>index :== w1 >> 5;;
(While \<lbrace>\<acute>index < (w2 >> 5) + 1\<rbrace> (\<acute>line :== \<acute>index << 5;;
CALL cleanInvalByVA_'proc(\<acute>line,w3 + (\<acute>line - w1));;
\<acute>index :== \<acute>index + 1);;
CALL dsb_'proc()))
 2. \<And>rv xfdca rva xfdc. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5; dc rv xfdca; dc rva xfdc\<rbrakk> \<Longrightarrow> \<lbrace>?R1363 rv xfdca rva\<rbrace> doMachineOp (cleanInvalidateL2Range w3 (w3 + (w2 - w1))) \<lbrace>?Q1353 rv xfdca rva xfdc\<rbrace>
 3. \<And>rv xfdc. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5; dc rv xfdc\<rbrakk> \<Longrightarrow> \<lbrace>?R1314 rv\<rbrace> doMachineOp dsb \<lbrace>\<lambda>a. (\<lambda>a. True) and ?R1363 rv xfdc a\<rbrace>
 4. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5\<rbrakk> \<Longrightarrow> \<lbrace>?R1273 w3 w2 w1\<rbrace> doMachineOp (cleanCacheRange_PoC w1 w2 w3) \<lbrace>\<lambda>a. (\<lambda>a. True) and ?R1314 a\<rbrace>
 5. \<And>rv' s'. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5\<rbrakk> \<Longrightarrow> globals (globals_update (ghost'state_'_update id) s') = globals s'
 6. \<And>rv' s'. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5; s' \<in> {s. pstart_'_update (\<lambda>_. w3) (end_'_update (\<lambda>_. w2) (start_'_update (\<lambda>_. w1) s)) \<in> \<lbrace>\<acute>start = w1\<rbrace> \<inter> \<lbrace>\<acute>end = w2\<rbrace> \<inter> \<lbrace>\<acute>pstart = w3\<rbrace>} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> {s. s \<in> UNIV} \<inter> {s'. \<forall>ta rva. dc rva (xfdc ta) \<longrightarrow> s'\<lparr>globals := globals ta\<rparr> \<in> {s. end_'_update (\<lambda>_. w3 + (w2 - w1)) (start_'_update (\<lambda>_. w3) s) \<in> \<lbrace>\<acute>start = w3\<rbrace> \<inter> \<lbrace>\<acute>end = w3 + (w2 - w1)\<rbrace>} \<inter> {s'. \<forall>tb rvb. dc rvb (xfdc tb) \<longrightarrow> s'\<lparr>globals := globals tb\<rparr> \<in> ?Q'1366 rv' t rv ta rva tb rvb}}}\<rbrakk> \<Longrightarrow> globals_update (ghost'state_'_update id) s' \<in> {s. pstart_'_update (\<lambda>_. w3) (end_'_update (\<lambda>_. w2) (start_'_update (\<lambda>_. w1) s)) \<in> \<lbrace>\<acute>start = w1\<rbrace> \<inter> \<lbrace>\<acute>end = w2\<rbrace> \<inter> \<lbrace>\<acute>pstart = w3\<rbrace>} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> {s. s \<in> UNIV} \<inter> {s'. \<forall>ta rva. dc rva (xfdc ta) \<longrightarrow> s'\<lparr>globals := globals ta\<rparr> \<in> {s. end_'_update (\<lambda>_. w3 + (w2 - w1)) (start_'_update (\<lambda>_. w3) s) \<in> \<lbrace>\<acute>start = w3\<rbrace> \<inter> \<lbrace>\<acute>end = w3 + (w2 - w1)\<rbrace>} \<inter> {s'. \<forall>tb rvb. dc rvb (xfdc tb) \<longrightarrow> s'\<lparr>globals := globals tb\<rparr> \<in> ?Q'1366 rv' t rv ta rva tb rvb}}}
 7. \<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> ((\<lambda>a. start \<le> end \<and> pstart \<le> pstart + (end - start) \<and> start && mask 5 = pstart && mask 5) and ?R1273 pstart end start) s \<and> s' \<in> {s. s \<in> {s. pstart_'_update (\<lambda>_. pstart) (end_'_update (\<lambda>_. end) (start_'_update (\<lambda>_. start) s)) \<in> \<lbrace>\<acute>start = start\<rbrace> \<inter> \<lbrace>\<acute>end = end\<rbrace> \<inter> \<lbrace>\<acute>pstart = pstart\<rbrace>} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> {s. s \<in> UNIV} \<inter> {s'. \<forall>ta rva. dc rva (xfdc ta) \<longrightarrow> s'\<lparr>globals := globals ta\<rparr> \<in> {s. end_'_update (\<lambda>_. pstart + (end - start)) (start_'_update (\<lambda>_. pstart) s) \<in> \<lbrace>\<acute>start = pstart\<rbrace> \<inter> \<lbrace>\<acute>end = pstart + (end - start)\<rbrace>} \<inter> {s'. \<forall>tb rvb. dc rvb (xfdc tb) \<longrightarrow> s'\<lparr>globals := globals tb\<rparr> \<in> ?Q'1369 pstart end start t rv ta rva tb rvb}}} \<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:
?Q'1369 w3 w2 w1 \<equiv>\<^sup>? ?Q'1366 ()
?Q'1366 () \<equiv>\<^sup>? \<lambda>t rv ta rva tb rvb. ?Q'1353 rv (xfdc t) rva (xfdc ta) rvb (xfdc tb) proof (prove)
goal (7 subgoals):
 1. \<And>rv xfdca rva xfdcb rvb xfdcc. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5; dc rv xfdca; dc rva xfdcb; dc rvb xfdcc\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q1353 rv xfdca rva xfdcb rvb) (?G'1404 rv xfdca rva xfdcb rvb xfdcc) [SKIP] (do rv <- doMachineOp (cacheRangeOp cleanInvalByVA w1 w2 w3);
doMachineOp dsb
od) (While \<lbrace>\<acute>index < (w2 >> 5) + 1\<rbrace> (\<acute>line :== \<acute>index << 5;;
CALL cleanInvalByVA_'proc(\<acute>line,w3 + (\<acute>line - w1));;
\<acute>index :== \<acute>index + 1);;
CALL dsb_'proc())
 2. \<And>rv xfdca rva xfdc. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5; dc rv xfdca; dc rva xfdc\<rbrakk> \<Longrightarrow> \<lbrace>?R1363 rv xfdca rva\<rbrace> doMachineOp (cleanInvalidateL2Range w3 (w3 + (w2 - w1))) \<lbrace>?Q1353 rv xfdca rva xfdc\<rbrace>
 3. \<And>rv xfdc. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5; dc rv xfdc\<rbrakk> \<Longrightarrow> \<lbrace>?R1314 rv\<rbrace> doMachineOp dsb \<lbrace>\<lambda>a. (\<lambda>a. True) and ?R1363 rv xfdc a\<rbrace>
 4. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5\<rbrakk> \<Longrightarrow> \<lbrace>?R1273 w3 w2 w1\<rbrace> doMachineOp (cleanCacheRange_PoC w1 w2 w3) \<lbrace>\<lambda>a. (\<lambda>a. True) and ?R1314 a\<rbrace>
 5. \<And>rv' s'. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5\<rbrakk> \<Longrightarrow> globals (globals_update (ghost'state_'_update id) s') = globals s'
 6. \<And>rv' s'. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5; s' \<in> {s. pstart_'_update (\<lambda>_. w3) (end_'_update (\<lambda>_. w2) (start_'_update (\<lambda>_. w1) s)) \<in> \<lbrace>\<acute>start = w1\<rbrace> \<inter> \<lbrace>\<acute>end = w2\<rbrace> \<inter> \<lbrace>\<acute>pstart = w3\<rbrace>} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> {s. s \<in> UNIV} \<inter> {s'. \<forall>ta rva. dc rva (xfdc ta) \<longrightarrow> s'\<lparr>globals := globals ta\<rparr> \<in> {s. end_'_update (\<lambda>_. w3 + (w2 - w1)) (start_'_update (\<lambda>_. w3) s) \<in> \<lbrace>\<acute>start = w3\<rbrace> \<inter> \<lbrace>\<acute>end = w3 + (w2 - w1)\<rbrace>} \<inter> {s'. \<forall>tb rvb. dc rvb (xfdc tb) \<longrightarrow> s'\<lparr>globals := globals tb\<rparr> \<in> {s. index_'_update (\<lambda>_. w1 >> 5) s \<in> ?G'1409 rv' t rv ta rva tb rvb}}}}\<rbrakk> \<Longrightarrow> globals_update (ghost'state_'_update id) s' \<in> {s. pstart_'_update (\<lambda>_. w3) (end_'_update (\<lambda>_. w2) (start_'_update (\<lambda>_. w1) s)) \<in> \<lbrace>\<acute>start = w1\<rbrace> \<inter> \<lbrace>\<acute>end = w2\<rbrace> \<inter> \<lbrace>\<acute>pstart = w3\<rbrace>} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> {s. s \<in> UNIV} \<inter> {s'. \<forall>ta rva. dc rva (xfdc ta) \<longrightarrow> s'\<lparr>globals := globals ta\<rparr> \<in> {s. end_'_update (\<lambda>_. w3 + (w2 - w1)) (start_'_update (\<lambda>_. w3) s) \<in> \<lbrace>\<acute>start = w3\<rbrace> \<inter> \<lbrace>\<acute>end = w3 + (w2 - w1)\<rbrace>} \<inter> {s'. \<forall>tb rvb. dc rvb (xfdc tb) \<longrightarrow> s'\<lparr>globals := globals tb\<rparr> \<in> {s. index_'_update (\<lambda>_. w1 >> 5) s \<in> ?G'1409 rv' t rv ta rva tb rvb}}}}
 7. \<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> ((\<lambda>a. start \<le> end \<and> pstart \<le> pstart + (end - start) \<and> start && mask 5 = pstart && mask 5) and ?R1273 pstart end start) s \<and> s' \<in> {s. s \<in> {s. pstart_'_update (\<lambda>_. pstart) (end_'_update (\<lambda>_. end) (start_'_update (\<lambda>_. start) s)) \<in> \<lbrace>\<acute>start = start\<rbrace> \<inter> \<lbrace>\<acute>end = end\<rbrace> \<inter> \<lbrace>\<acute>pstart = pstart\<rbrace>} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> {s. s \<in> UNIV} \<inter> {s'. \<forall>ta rva. dc rva (xfdc ta) \<longrightarrow> s'\<lparr>globals := globals ta\<rparr> \<in> {s. end_'_update (\<lambda>_. pstart + (end - start)) (start_'_update (\<lambda>_. pstart) s) \<in> \<lbrace>\<acute>start = pstart\<rbrace> \<inter> \<lbrace>\<acute>end = pstart + (end - start)\<rbrace>} \<inter> {s'. \<forall>tb rvb. dc rvb (xfdc tb) \<longrightarrow> s'\<lparr>globals := globals tb\<rparr> \<in> {s. index_'_update (\<lambda>_. start >> 5) s \<in> ?G'1410 pstart end start t rv ta rva tb rvb}}}} \<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'1410 w3 w2 w1 \<equiv>\<^sup>? ?G'1409 ()
?G'1409 () \<equiv>\<^sup>? \<lambda>t rv ta rva tb rvb. ?G'1404 rv (xfdc t) rva (xfdc ta) rvb (xfdc tb) proof (prove)
goal (11 subgoals):
 1. \<And>rv xfdca rva xfdcb rvb xfdc. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5; dc rv xfdca; dc rva xfdcb; dc rvb xfdc\<rbrakk> \<Longrightarrow> ccorres (?r'1501 rv xfdca rva xfdcb rvb xfdc) (?xf'1501 rv xfdca rva xfdcb rvb xfdc) (?P1507 rv xfdca rva xfdcb rvb) (?G'1404 rv xfdca rva xfdcb rvb xfdc) [] (doMachineOp (cacheRangeOp cleanInvalByVA w1 w2 w3)) (While \<lbrace>\<acute>index < (w2 >> 5) + 1\<rbrace> (\<acute>line :== \<acute>index << 5;;
CALL cleanInvalByVA_'proc(\<acute>line,w3 + (\<acute>line - w1));;
\<acute>index :== \<acute>index + 1))
 2. \<And>rv xfdca rva xfdcb rvb xfdc rv' t t'. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5; dc rv xfdca; dc rva xfdcb; dc rvb xfdc\<rbrakk> \<Longrightarrow> ceqv \<Gamma> (?xf'1501 rv xfdca rva xfdcb rvb xfdc) rv' t t' (CALL dsb_'proc()) (?d'1501 rv xfdca rva xfdcb rvb xfdc rv')
 3. \<And>rv xfdca rva xfdcb rvb xfdcc rvc rv'. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5; dc rv xfdca; dc rva xfdcb; dc rvb xfdcc; ?r'1501 rv xfdca rva xfdcb rvb xfdcc rvc rv'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q1501 rv xfdca rva xfdcb rvb xfdcc rvc) (?Q'1501 rv xfdca rva xfdcb rvb xfdcc rvc rv') [SKIP] (doMachineOp dsb) (?d'1501 rv xfdca rva xfdcb rvb xfdcc rv')
 4. \<And>rv xfdca rva xfdcb rvb xfdc. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5; dc rv xfdca; dc rva xfdcb; dc rvb xfdc\<rbrakk> \<Longrightarrow> \<lbrace>?R1505 rv xfdca rva xfdcb rvb\<rbrace> doMachineOp (cacheRangeOp cleanInvalByVA w1 w2 w3) \<lbrace>?Q1501 rv xfdca rva xfdcb rvb xfdc\<rbrace>
 5. \<And>rv xfdca rva xfdcb rvb xfdc. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5; dc rv xfdca; dc rva xfdcb; dc rvb xfdc\<rbrakk> \<Longrightarrow> guard_is_UNIV (?r'1501 rv xfdca rva xfdcb rvb xfdc) (?xf'1501 rv xfdca rva xfdcb rvb xfdc) (?Q'1501 rv xfdca rva xfdcb rvb xfdc)
 6. \<And>rv xfdca rva xfdc. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5; dc rv xfdca; dc rva xfdc\<rbrakk> \<Longrightarrow> \<lbrace>?R1363 rv xfdca rva\<rbrace> doMachineOp (cleanInvalidateL2Range w3 (w3 + (w2 - w1))) \<lbrace>\<lambda>a. ?P1507 rv xfdca rva xfdc a and ?R1505 rv xfdca rva xfdc a\<rbrace>
 7. \<And>rv xfdc. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5; dc rv xfdc\<rbrakk> \<Longrightarrow> \<lbrace>?R1314 rv\<rbrace> doMachineOp dsb \<lbrace>\<lambda>a. (\<lambda>a. True) and ?R1363 rv xfdc a\<rbrace>
 8. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5\<rbrakk> \<Longrightarrow> \<lbrace>?R1273 w3 w2 w1\<rbrace> doMachineOp (cleanCacheRange_PoC w1 w2 w3) \<lbrace>\<lambda>a. (\<lambda>a. True) and ?R1314 a\<rbrace>
 9. \<And>rv' s'. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5\<rbrakk> \<Longrightarrow> globals (globals_update (ghost'state_'_update id) s') = globals s'
 10. \<And>rv' s'. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5; s' \<in> {s. pstart_'_update (\<lambda>_. w3) (end_'_update (\<lambda>_. w2) (start_'_update (\<lambda>_. w1) s)) \<in> \<lbrace>\<acute>start = w1\<rbrace> \<inter> \<lbrace>\<acute>end = w2\<rbrace> \<inter> \<lbrace>\<acute>pstart = w3\<rbrace>} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> {s. s \<in> UNIV} \<inter> {s'. \<forall>ta rva. dc rva (xfdc ta) \<longrightarrow> s'\<lparr>globals := globals ta\<rparr> \<in> {s. end_'_update (\<lambda>_. w3 + (w2 - w1)) (start_'_update (\<lambda>_. w3) s) \<in> \<lbrace>\<acute>start = w3\<rbrace> \<inter> \<lbrace>\<acute>end = w3 + (w2 - w1)\<rbrace>} \<inter> {s'. \<forall>tb rvb. dc rvb (xfdc tb) \<longrightarrow> s'\<lparr>globals := globals tb\<rparr> \<in> {s. index_'_update (\<lambda>_. w1 >> 5) s \<in> ?G'1409 rv' t rv ta rva tb rvb}}}}\<rbrakk> \<Longrightarrow> globals_update (ghost'state_'_update id) s' \<in> {s. pstart_'_update (\<lambda>_. w3) (end_'_update (\<lambda>_. w2) (start_'_update (\<lambda>_. w1) s)) \<in> \<lbrace>\<acute>start = w1\<rbrace> \<inter> \<lbrace>\<acute>end = w2\<rbrace> \<inter> \<lbrace>\<acute>pstart = w3\<rbrace>} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> {s. s \<in> UNIV} \<inter> {s'. \<forall>ta rva. dc rva (xfdc ta) \<longrightarrow> s'\<lparr>globals := globals ta\<rparr> \<in> {s. end_'_update (\<lambda>_. w3 + (w2 - w1)) (start_'_update (\<lambda>_. w3) s) \<in> \<lbrace>\<acute>start = w3\<rbrace> \<inter> \<lbrace>\<acute>end = w3 + (w2 - w1)\<rbrace>} \<inter> {s'. \<forall>tb rvb. dc rvb (xfdc tb) \<longrightarrow> s'\<lparr>globals := globals tb\<rparr> \<in> {s. index_'_update (\<lambda>_. w1 >> 5) s \<in> ?G'1409 rv' t rv ta rva tb rvb}}}}
A total of 11 subgoals...
flex-flex pairs:
?G'1410 w3 w2 w1 \<equiv>\<^sup>? ?G'1409 ()
?G'1409 () \<equiv>\<^sup>? \<lambda>t rv ta rva tb rvb. ?G'1404 rv (xfdc t) rva (xfdc ta) rvb (xfdc tb) proof (prove)
goal (13 subgoals):
 1. \<And>rv xfdca rva xfdcb rvb xfdc x y. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5; dc rv xfdca; dc rva xfdcb; dc rvb xfdc\<rbrakk> \<Longrightarrow> empty_fail (cleanInvalByVA x y)
 2. \<And>rv xfdca rva xfdcb rvb xfdcc. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5; dc rv xfdca; dc rva xfdcb; dc rvb xfdcc\<rbrakk> \<Longrightarrow> \<forall>n. ccorres dc xfdc (\<lambda>_. True) \<lbrace>\<acute>index = lineIndex w1 + word_of_nat n\<rbrace> [] (doMachineOp (cleanInvalByVA (lineStart w1 + word_of_nat n * 0x20) (lineStart w3 + word_of_nat n * 0x20))) (\<acute>line :== \<acute>index << 5;;
CALL cleanInvalByVA_'proc(\<acute>line,w3 + (\<acute>line - w1)))
 3. \<And>rv xfdca rva xfdcb rvb xfdc. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5; dc rv xfdca; dc rva xfdcb; dc rvb xfdc\<rbrakk> \<Longrightarrow> \<forall>s. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} \<acute>line :== \<acute>index << 5;;
CALL cleanInvalByVA_'proc(\<acute>line,w3 + (\<acute>line - w1)) \<lbrace>\<acute>index = \<^bsup>s\<^esup>index\<rbrace>
 4. \<And>rv xfdca rva xfdcb rvb xfdcc rv' t t'. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5; dc rv xfdca; dc rva xfdcb; dc rvb xfdcc\<rbrakk> \<Longrightarrow> ceqv \<Gamma> xfdc rv' t t' (CALL dsb_'proc()) (?d'1501 rv xfdca rva xfdcb rvb xfdcc rv')
 5. \<And>rv xfdca rva xfdcb rvb xfdcc rvc rv'. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5; dc rv xfdca; dc rva xfdcb; dc rvb xfdcc; dc rvc rv'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q1501 rv xfdca rva xfdcb rvb xfdcc rvc) (?Q'1501 rv xfdca rva xfdcb rvb xfdcc rvc rv') [SKIP] (doMachineOp dsb) (?d'1501 rv xfdca rva xfdcb rvb xfdcc rv')
 6. \<And>rv xfdca rva xfdcb rvb xfdc. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5; dc rv xfdca; dc rva xfdcb; dc rvb xfdc\<rbrakk> \<Longrightarrow> \<lbrace>?R1505 rv xfdca rva xfdcb rvb\<rbrace> doMachineOp (cacheRangeOp cleanInvalByVA w1 w2 w3) \<lbrace>?Q1501 rv xfdca rva xfdcb rvb xfdc\<rbrace>
 7. \<And>rv xfdca rva xfdcb rvb xfdcc. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5; dc rv xfdca; dc rva xfdcb; dc rvb xfdcc\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (?Q'1501 rv xfdca rva xfdcb rvb xfdcc)
 8. \<And>rv xfdca rva xfdc. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5; dc rv xfdca; dc rva xfdc\<rbrakk> \<Longrightarrow> \<lbrace>?R1363 rv xfdca rva\<rbrace> doMachineOp (cleanInvalidateL2Range w3 (w3 + (w2 - w1))) \<lbrace>\<lambda>a. (\<lambda>a. w1 \<le> w2 \<and> w3 \<le> w3 + (w2 - w1) \<and> w1 && mask 5 = w3 && mask 5) and ?R1505 rv xfdca rva xfdc a\<rbrace>
 9. \<And>rv xfdc. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5; dc rv xfdc\<rbrakk> \<Longrightarrow> \<lbrace>?R1314 rv\<rbrace> doMachineOp dsb \<lbrace>\<lambda>a. (\<lambda>a. True) and ?R1363 rv xfdc a\<rbrace>
 10. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5\<rbrakk> \<Longrightarrow> \<lbrace>?R1273 w3 w2 w1\<rbrace> doMachineOp (cleanCacheRange_PoC w1 w2 w3) \<lbrace>\<lambda>a. (\<lambda>a. True) and ?R1314 a\<rbrace>
A total of 13 subgoals... proof (prove)
goal (12 subgoals):
 1. \<And>rv xfdca rva xfdcb rvb xfdcc. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5; dc rv xfdca; dc rva xfdcb; dc rvb xfdcc\<rbrakk> \<Longrightarrow> \<forall>n. ccorres dc xfdc (\<lambda>_. True) \<lbrace>\<acute>index = lineIndex w1 + word_of_nat n\<rbrace> [] (doMachineOp (cleanInvalByVA (lineStart w1 + word_of_nat n * 0x20) (lineStart w3 + word_of_nat n * 0x20))) (\<acute>line :== \<acute>index << 5;;
CALL cleanInvalByVA_'proc(\<acute>line,w3 + (\<acute>line - w1)))
 2. \<And>rv xfdca rva xfdcb rvb xfdc. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5; dc rv xfdca; dc rva xfdcb; dc rvb xfdc\<rbrakk> \<Longrightarrow> \<forall>s. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} \<acute>line :== \<acute>index << 5;;
CALL cleanInvalByVA_'proc(\<acute>line,w3 + (\<acute>line - w1)) \<lbrace>\<acute>index = \<^bsup>s\<^esup>index\<rbrace>
 3. \<And>rv xfdca rva xfdcb rvb xfdcc rv' t t'. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5; dc rv xfdca; dc rva xfdcb; dc rvb xfdcc\<rbrakk> \<Longrightarrow> ceqv \<Gamma> xfdc rv' t t' (CALL dsb_'proc()) (?d'1501 rv xfdca rva xfdcb rvb xfdcc rv')
 4. \<And>rv xfdca rva xfdcb rvb xfdcc rvc rv'. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5; dc rv xfdca; dc rva xfdcb; dc rvb xfdcc; dc rvc rv'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q1501 rv xfdca rva xfdcb rvb xfdcc rvc) (?Q'1501 rv xfdca rva xfdcb rvb xfdcc rvc rv') [SKIP] (doMachineOp dsb) (?d'1501 rv xfdca rva xfdcb rvb xfdcc rv')
 5. \<And>rv xfdca rva xfdcb rvb xfdc. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5; dc rv xfdca; dc rva xfdcb; dc rvb xfdc\<rbrakk> \<Longrightarrow> \<lbrace>?R1505 rv xfdca rva xfdcb rvb\<rbrace> doMachineOp (cacheRangeOp cleanInvalByVA w1 w2 w3) \<lbrace>?Q1501 rv xfdca rva xfdcb rvb xfdc\<rbrace>
 6. \<And>rv xfdca rva xfdcb rvb xfdcc. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5; dc rv xfdca; dc rva xfdcb; dc rvb xfdcc\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (?Q'1501 rv xfdca rva xfdcb rvb xfdcc)
 7. \<And>rv xfdca rva xfdc. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5; dc rv xfdca; dc rva xfdc\<rbrakk> \<Longrightarrow> \<lbrace>?R1363 rv xfdca rva\<rbrace> doMachineOp (cleanInvalidateL2Range w3 (w3 + (w2 - w1))) \<lbrace>\<lambda>a. (\<lambda>a. w1 \<le> w2 \<and> w3 \<le> w3 + (w2 - w1) \<and> w1 && mask 5 = w3 && mask 5) and ?R1505 rv xfdca rva xfdc a\<rbrace>
 8. \<And>rv xfdc. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5; dc rv xfdc\<rbrakk> \<Longrightarrow> \<lbrace>?R1314 rv\<rbrace> doMachineOp dsb \<lbrace>\<lambda>a. (\<lambda>a. True) and ?R1363 rv xfdc a\<rbrace>
 9. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5\<rbrakk> \<Longrightarrow> \<lbrace>?R1273 w3 w2 w1\<rbrace> doMachineOp (cleanCacheRange_PoC w1 w2 w3) \<lbrace>\<lambda>a. (\<lambda>a. True) and ?R1314 a\<rbrace>
 10. \<And>rv' s'. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5\<rbrakk> \<Longrightarrow> globals (globals_update (ghost'state_'_update id) s') = globals s'
A total of 12 subgoals... proof (prove)
goal (12 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> [] (doMachineOp (cleanInvalByVA (lineStart w1 + word_of_nat n * 0x20) (lineStart w3 + word_of_nat n * 0x20))) (\<acute>line :== \<acute>index << 5;;
CALL cleanInvalByVA_'proc(\<acute>line,w3 + (\<acute>line - w1)))
 2. \<And>rv xfdca rva xfdcb rvb xfdc. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5; dc rv xfdca; dc rva xfdcb; dc rvb xfdc\<rbrakk> \<Longrightarrow> \<forall>s. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} \<acute>line :== \<acute>index << 5;;
CALL cleanInvalByVA_'proc(\<acute>line,w3 + (\<acute>line - w1)) \<lbrace>\<acute>index = \<^bsup>s\<^esup>index\<rbrace>
 3. \<And>rv xfdca rva xfdcb rvb xfdcc rv' t t'. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5; dc rv xfdca; dc rva xfdcb; dc rvb xfdcc\<rbrakk> \<Longrightarrow> ceqv \<Gamma> xfdc rv' t t' (CALL dsb_'proc()) (?d'1501 rv xfdca rva xfdcb rvb xfdcc rv')
 4. \<And>rv xfdca rva xfdcb rvb xfdcc rvc rv'. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5; dc rv xfdca; dc rva xfdcb; dc rvb xfdcc; dc rvc rv'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q1501 rv xfdca rva xfdcb rvb xfdcc rvc) (?Q'1501 rv xfdca rva xfdcb rvb xfdcc rvc rv') [SKIP] (doMachineOp dsb) (?d'1501 rv xfdca rva xfdcb rvb xfdcc rv')
 5. \<And>rv xfdca rva xfdcb rvb xfdc. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5; dc rv xfdca; dc rva xfdcb; dc rvb xfdc\<rbrakk> \<Longrightarrow> \<lbrace>?R1505 rv xfdca rva xfdcb rvb\<rbrace> doMachineOp (cacheRangeOp cleanInvalByVA w1 w2 w3) \<lbrace>?Q1501 rv xfdca rva xfdcb rvb xfdc\<rbrace>
 6. \<And>rv xfdca rva xfdcb rvb xfdcc. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5; dc rv xfdca; dc rva xfdcb; dc rvb xfdcc\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (?Q'1501 rv xfdca rva xfdcb rvb xfdcc)
 7. \<And>rv xfdca rva xfdc. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5; dc rv xfdca; dc rva xfdc\<rbrakk> \<Longrightarrow> \<lbrace>?R1363 rv xfdca rva\<rbrace> doMachineOp (cleanInvalidateL2Range w3 (w3 + (w2 - w1))) \<lbrace>\<lambda>a. (\<lambda>a. w1 \<le> w2 \<and> w3 \<le> w3 + (w2 - w1) \<and> w1 && mask 5 = w3 && mask 5) and ?R1505 rv xfdca rva xfdc a\<rbrace>
 8. \<And>rv xfdc. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5; dc rv xfdc\<rbrakk> \<Longrightarrow> \<lbrace>?R1314 rv\<rbrace> doMachineOp dsb \<lbrace>\<lambda>a. (\<lambda>a. True) and ?R1363 rv xfdc a\<rbrace>
 9. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5\<rbrakk> \<Longrightarrow> \<lbrace>?R1273 w3 w2 w1\<rbrace> doMachineOp (cleanCacheRange_PoC w1 w2 w3) \<lbrace>\<lambda>a. (\<lambda>a. True) and ?R1314 a\<rbrace>
 10. \<And>rv' s'. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5\<rbrakk> \<Longrightarrow> globals (globals_update (ghost'state_'_update id) s') = globals s'
A total of 12 subgoals... proof (prove)
goal (12 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 [] (doMachineOp (cleanInvalByVA (lineStart w1 + word_of_nat n * 0x20) (lineStart w3 + word_of_nat n * 0x20))) (\<acute>line :== index << 5;;
CALL cleanInvalByVA_'proc(\<acute>line,w3 + (\<acute>line - w1)))
 2. \<And>rv xfdca rva xfdcb rvb xfdc. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5; dc rv xfdca; dc rva xfdcb; dc rvb xfdc\<rbrakk> \<Longrightarrow> \<forall>s. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} \<acute>line :== \<acute>index << 5;;
CALL cleanInvalByVA_'proc(\<acute>line,w3 + (\<acute>line - w1)) \<lbrace>\<acute>index = \<^bsup>s\<^esup>index\<rbrace>
 3. \<And>rv xfdca rva xfdcb rvb xfdcc rv' t t'. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5; dc rv xfdca; dc rva xfdcb; dc rvb xfdcc\<rbrakk> \<Longrightarrow> ceqv \<Gamma> xfdc rv' t t' (CALL dsb_'proc()) (?d'1501 rv xfdca rva xfdcb rvb xfdcc rv')
 4. \<And>rv xfdca rva xfdcb rvb xfdcc rvc rv'. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5; dc rv xfdca; dc rva xfdcb; dc rvb xfdcc; dc rvc rv'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q1501 rv xfdca rva xfdcb rvb xfdcc rvc) (?Q'1501 rv xfdca rva xfdcb rvb xfdcc rvc rv') [SKIP] (doMachineOp dsb) (?d'1501 rv xfdca rva xfdcb rvb xfdcc rv')
 5. \<And>rv xfdca rva xfdcb rvb xfdc. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5; dc rv xfdca; dc rva xfdcb; dc rvb xfdc\<rbrakk> \<Longrightarrow> \<lbrace>?R1505 rv xfdca rva xfdcb rvb\<rbrace> doMachineOp (cacheRangeOp cleanInvalByVA w1 w2 w3) \<lbrace>?Q1501 rv xfdca rva xfdcb rvb xfdc\<rbrace>
 6. \<And>rv xfdca rva xfdcb rvb xfdcc. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5; dc rv xfdca; dc rva xfdcb; dc rvb xfdcc\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (?Q'1501 rv xfdca rva xfdcb rvb xfdcc)
 7. \<And>rv xfdca rva xfdc. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5; dc rv xfdca; dc rva xfdc\<rbrakk> \<Longrightarrow> \<lbrace>?R1363 rv xfdca rva\<rbrace> doMachineOp (cleanInvalidateL2Range w3 (w3 + (w2 - w1))) \<lbrace>\<lambda>a. (\<lambda>a. w1 \<le> w2 \<and> w3 \<le> w3 + (w2 - w1) \<and> w1 && mask 5 = w3 && mask 5) and ?R1505 rv xfdca rva xfdc a\<rbrace>
 8. \<And>rv xfdc. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5; dc rv xfdc\<rbrakk> \<Longrightarrow> \<lbrace>?R1314 rv\<rbrace> doMachineOp dsb \<lbrace>\<lambda>a. (\<lambda>a. True) and ?R1363 rv xfdc a\<rbrace>
 9. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5\<rbrakk> \<Longrightarrow> \<lbrace>?R1273 w3 w2 w1\<rbrace> doMachineOp (cleanCacheRange_PoC w1 w2 w3) \<lbrace>\<lambda>a. (\<lambda>a. True) and ?R1314 a\<rbrace>
 10. \<And>rv' s'. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5\<rbrakk> \<Longrightarrow> globals (globals_update (ghost'state_'_update id) s') = globals s'
A total of 12 subgoals... proof (prove)
goal (13 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 (?Q1572 n index) (?Q'1572 n index) [] (doMachineOp (cleanInvalByVA (lineStart w1 + word_of_nat n * 0x20) (lineStart w3 + word_of_nat n * 0x20))) (\<acute>line :== index << 5;;
CALL cleanInvalByVA_'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> ?Q1572 n index s \<and> s' \<in> ?Q'1572 n index
 3. \<And>rv xfdca rva xfdcb rvb xfdc. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5; dc rv xfdca; dc rva xfdcb; dc rvb xfdc\<rbrakk> \<Longrightarrow> \<forall>s. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} \<acute>line :== \<acute>index << 5;;
CALL cleanInvalByVA_'proc(\<acute>line,w3 + (\<acute>line - w1)) \<lbrace>\<acute>index = \<^bsup>s\<^esup>index\<rbrace>
 4. \<And>rv xfdca rva xfdcb rvb xfdcc rv' t t'. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5; dc rv xfdca; dc rva xfdcb; dc rvb xfdcc\<rbrakk> \<Longrightarrow> ceqv \<Gamma> xfdc rv' t t' (CALL dsb_'proc()) (?d'1501 rv xfdca rva xfdcb rvb xfdcc rv')
 5. \<And>rv xfdca rva xfdcb rvb xfdcc rvc rv'. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5; dc rv xfdca; dc rva xfdcb; dc rvb xfdcc; dc rvc rv'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q1501 rv xfdca rva xfdcb rvb xfdcc rvc) (?Q'1501 rv xfdca rva xfdcb rvb xfdcc rvc rv') [SKIP] (doMachineOp dsb) (?d'1501 rv xfdca rva xfdcb rvb xfdcc rv')
 6. \<And>rv xfdca rva xfdcb rvb xfdc. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5; dc rv xfdca; dc rva xfdcb; dc rvb xfdc\<rbrakk> \<Longrightarrow> \<lbrace>?R1505 rv xfdca rva xfdcb rvb\<rbrace> doMachineOp (cacheRangeOp cleanInvalByVA w1 w2 w3) \<lbrace>?Q1501 rv xfdca rva xfdcb rvb xfdc\<rbrace>
 7. \<And>rv xfdca rva xfdcb rvb xfdcc. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5; dc rv xfdca; dc rva xfdcb; dc rvb xfdcc\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (?Q'1501 rv xfdca rva xfdcb rvb xfdcc)
 8. \<And>rv xfdca rva xfdc. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5; dc rv xfdca; dc rva xfdc\<rbrakk> \<Longrightarrow> \<lbrace>?R1363 rv xfdca rva\<rbrace> doMachineOp (cleanInvalidateL2Range w3 (w3 + (w2 - w1))) \<lbrace>\<lambda>a. (\<lambda>a. w1 \<le> w2 \<and> w3 \<le> w3 + (w2 - w1) \<and> w1 && mask 5 = w3 && mask 5) and ?R1505 rv xfdca rva xfdc a\<rbrace>
 9. \<And>rv xfdc. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5; dc rv xfdc\<rbrakk> \<Longrightarrow> \<lbrace>?R1314 rv\<rbrace> doMachineOp dsb \<lbrace>\<lambda>a. (\<lambda>a. True) and ?R1363 rv xfdc a\<rbrace>
 10. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5\<rbrakk> \<Longrightarrow> \<lbrace>?R1273 w3 w2 w1\<rbrace> doMachineOp (cleanCacheRange_PoC w1 w2 w3) \<lbrace>\<lambda>a. (\<lambda>a. True) and ?R1314 a\<rbrace>
A total of 13 subgoals... proof (prove)
goal (13 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 (?Q1572 n index) (?G'1577 n index) [] (doMachineOp (cleanInvalByVA (lineStart w1 + word_of_nat n * 0x20) (lineStart w3 + word_of_nat n * 0x20))) (CALL cleanInvalByVA_'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> ?Q1572 n index s \<and> s' \<in> {s. line_'_update (\<lambda>_. index << 5) s \<in> ?G'1577 n index}
 3. \<And>rv xfdca rva xfdcb rvb xfdc. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5; dc rv xfdca; dc rva xfdcb; dc rvb xfdc\<rbrakk> \<Longrightarrow> \<forall>s. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} \<acute>line :== \<acute>index << 5;;
CALL cleanInvalByVA_'proc(\<acute>line,w3 + (\<acute>line - w1)) \<lbrace>\<acute>index = \<^bsup>s\<^esup>index\<rbrace>
 4. \<And>rv xfdca rva xfdcb rvb xfdcc rv' t t'. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5; dc rv xfdca; dc rva xfdcb; dc rvb xfdcc\<rbrakk> \<Longrightarrow> ceqv \<Gamma> xfdc rv' t t' (CALL dsb_'proc()) (?d'1501 rv xfdca rva xfdcb rvb xfdcc rv')
 5. \<And>rv xfdca rva xfdcb rvb xfdcc rvc rv'. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5; dc rv xfdca; dc rva xfdcb; dc rvb xfdcc; dc rvc rv'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q1501 rv xfdca rva xfdcb rvb xfdcc rvc) (?Q'1501 rv xfdca rva xfdcb rvb xfdcc rvc rv') [SKIP] (doMachineOp dsb) (?d'1501 rv xfdca rva xfdcb rvb xfdcc rv')
 6. \<And>rv xfdca rva xfdcb rvb xfdc. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5; dc rv xfdca; dc rva xfdcb; dc rvb xfdc\<rbrakk> \<Longrightarrow> \<lbrace>?R1505 rv xfdca rva xfdcb rvb\<rbrace> doMachineOp (cacheRangeOp cleanInvalByVA w1 w2 w3) \<lbrace>?Q1501 rv xfdca rva xfdcb rvb xfdc\<rbrace>
 7. \<And>rv xfdca rva xfdcb rvb xfdcc. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5; dc rv xfdca; dc rva xfdcb; dc rvb xfdcc\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (?Q'1501 rv xfdca rva xfdcb rvb xfdcc)
 8. \<And>rv xfdca rva xfdc. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5; dc rv xfdca; dc rva xfdc\<rbrakk> \<Longrightarrow> \<lbrace>?R1363 rv xfdca rva\<rbrace> doMachineOp (cleanInvalidateL2Range w3 (w3 + (w2 - w1))) \<lbrace>\<lambda>a. (\<lambda>a. w1 \<le> w2 \<and> w3 \<le> w3 + (w2 - w1) \<and> w1 && mask 5 = w3 && mask 5) and ?R1505 rv xfdca rva xfdc a\<rbrace>
 9. \<And>rv xfdc. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5; dc rv xfdc\<rbrakk> \<Longrightarrow> \<lbrace>?R1314 rv\<rbrace> doMachineOp dsb \<lbrace>\<lambda>a. (\<lambda>a. True) and ?R1363 rv xfdc a\<rbrace>
 10. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5\<rbrakk> \<Longrightarrow> \<lbrace>?R1273 w3 w2 w1\<rbrace> doMachineOp (cleanCacheRange_PoC w1 w2 w3) \<lbrace>\<lambda>a. (\<lambda>a. True) and ?R1314 a\<rbrace>
A total of 13 subgoals... proof (prove)
goal (12 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. \<And>rv xfdca rva xfdcb rvb xfdc. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5; dc rv xfdca; dc rva xfdcb; dc rvb xfdc\<rbrakk> \<Longrightarrow> \<forall>s. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} \<acute>line :== \<acute>index << 5;;
CALL cleanInvalByVA_'proc(\<acute>line,w3 + (\<acute>line - w1)) \<lbrace>\<acute>index = \<^bsup>s\<^esup>index\<rbrace>
 3. \<And>rv xfdca rva xfdcb rvb xfdcc rv' t t'. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5; dc rv xfdca; dc rva xfdcb; dc rvb xfdcc\<rbrakk> \<Longrightarrow> ceqv \<Gamma> xfdc rv' t t' (CALL dsb_'proc()) (?d'1501 rv xfdca rva xfdcb rvb xfdcc rv')
 4. \<And>rv xfdca rva xfdcb rvb xfdcc rvc rv'. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5; dc rv xfdca; dc rva xfdcb; dc rvb xfdcc; dc rvc rv'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q1501 rv xfdca rva xfdcb rvb xfdcc rvc) (?Q'1501 rv xfdca rva xfdcb rvb xfdcc rvc rv') [SKIP] (doMachineOp dsb) (?d'1501 rv xfdca rva xfdcb rvb xfdcc rv')
 5. \<And>rv xfdca rva xfdcb rvb xfdc. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5; dc rv xfdca; dc rva xfdcb; dc rvb xfdc\<rbrakk> \<Longrightarrow> \<lbrace>?R1505 rv xfdca rva xfdcb rvb\<rbrace> doMachineOp (cacheRangeOp cleanInvalByVA w1 w2 w3) \<lbrace>?Q1501 rv xfdca rva xfdcb rvb xfdc\<rbrace>
 6. \<And>rv xfdca rva xfdcb rvb xfdcc. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5; dc rv xfdca; dc rva xfdcb; dc rvb xfdcc\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (?Q'1501 rv xfdca rva xfdcb rvb xfdcc)
 7. \<And>rv xfdca rva xfdc. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5; dc rv xfdca; dc rva xfdc\<rbrakk> \<Longrightarrow> \<lbrace>?R1363 rv xfdca rva\<rbrace> doMachineOp (cleanInvalidateL2Range w3 (w3 + (w2 - w1))) \<lbrace>\<lambda>a. (\<lambda>a. w1 \<le> w2 \<and> w3 \<le> w3 + (w2 - w1) \<and> w1 && mask 5 = w3 && mask 5) and ?R1505 rv xfdca rva xfdc a\<rbrace>
 8. \<And>rv xfdc. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5; dc rv xfdc\<rbrakk> \<Longrightarrow> \<lbrace>?R1314 rv\<rbrace> doMachineOp dsb \<lbrace>\<lambda>a. (\<lambda>a. True) and ?R1363 rv xfdc a\<rbrace>
 9. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5\<rbrakk> \<Longrightarrow> \<lbrace>?R1273 w3 w2 w1\<rbrace> doMachineOp (cleanCacheRange_PoC w1 w2 w3) \<lbrace>\<lambda>a. (\<lambda>a. True) and ?R1314 a\<rbrace>
 10. \<And>rv' s'. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5\<rbrakk> \<Longrightarrow> globals (globals_update (ghost'state_'_update id) s') = globals s'
A total of 12 subgoals... proof (prove)
goal (12 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. \<And>rv xfdca rva xfdcb rvb xfdc. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5; dc rv xfdca; dc rva xfdcb; dc rvb xfdc\<rbrakk> \<Longrightarrow> \<forall>s. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} \<acute>line :== \<acute>index << 5;;
CALL cleanInvalByVA_'proc(\<acute>line,w3 + (\<acute>line - w1)) \<lbrace>\<acute>index = \<^bsup>s\<^esup>index\<rbrace>
 3. \<And>rv xfdca rva xfdcb rvb xfdcc rv' t t'. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5; dc rv xfdca; dc rva xfdcb; dc rvb xfdcc\<rbrakk> \<Longrightarrow> ceqv \<Gamma> xfdc rv' t t' (CALL dsb_'proc()) (?d'1501 rv xfdca rva xfdcb rvb xfdcc rv')
 4. \<And>rv xfdca rva xfdcb rvb xfdcc rvc rv'. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5; dc rv xfdca; dc rva xfdcb; dc rvb xfdcc; dc rvc rv'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q1501 rv xfdca rva xfdcb rvb xfdcc rvc) (?Q'1501 rv xfdca rva xfdcb rvb xfdcc rvc rv') [SKIP] (doMachineOp dsb) (?d'1501 rv xfdca rva xfdcb rvb xfdcc rv')
 5. \<And>rv xfdca rva xfdcb rvb xfdc. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5; dc rv xfdca; dc rva xfdcb; dc rvb xfdc\<rbrakk> \<Longrightarrow> \<lbrace>?R1505 rv xfdca rva xfdcb rvb\<rbrace> doMachineOp (cacheRangeOp cleanInvalByVA w1 w2 w3) \<lbrace>?Q1501 rv xfdca rva xfdcb rvb xfdc\<rbrace>
 6. \<And>rv xfdca rva xfdcb rvb xfdcc. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5; dc rv xfdca; dc rva xfdcb; dc rvb xfdcc\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (?Q'1501 rv xfdca rva xfdcb rvb xfdcc)
 7. \<And>rv xfdca rva xfdc. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5; dc rv xfdca; dc rva xfdc\<rbrakk> \<Longrightarrow> \<lbrace>?R1363 rv xfdca rva\<rbrace> doMachineOp (cleanInvalidateL2Range w3 (w3 + (w2 - w1))) \<lbrace>\<lambda>a. (\<lambda>a. w1 \<le> w2 \<and> w3 \<le> w3 + (w2 - w1) \<and> w1 && mask 5 = w3 && mask 5) and ?R1505 rv xfdca rva xfdc a\<rbrace>
 8. \<And>rv xfdc. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5; dc rv xfdc\<rbrakk> \<Longrightarrow> \<lbrace>?R1314 rv\<rbrace> doMachineOp dsb \<lbrace>\<lambda>a. (\<lambda>a. True) and ?R1363 rv xfdc a\<rbrace>
 9. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5\<rbrakk> \<Longrightarrow> \<lbrace>?R1273 w3 w2 w1\<rbrace> doMachineOp (cleanCacheRange_PoC w1 w2 w3) \<lbrace>\<lambda>a. (\<lambda>a. True) and ?R1314 a\<rbrace>
 10. \<And>rv' s'. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5\<rbrakk> \<Longrightarrow> globals (globals_update (ghost'state_'_update id) s') = globals s'
A total of 12 subgoals... proof (prove)
goal (11 subgoals):
 1. \<And>rv xfdca rva xfdcb rvb xfdc. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5; dc rv xfdca; dc rva xfdcb; dc rvb xfdc\<rbrakk> \<Longrightarrow> \<forall>s. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} \<acute>line :== \<acute>index << 5;;
CALL cleanInvalByVA_'proc(\<acute>line,w3 + (\<acute>line - w1)) \<lbrace>\<acute>index = \<^bsup>s\<^esup>index\<rbrace>
 2. \<And>rv xfdca rva xfdcb rvb xfdcc rv' t t'. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5; dc rv xfdca; dc rva xfdcb; dc rvb xfdcc\<rbrakk> \<Longrightarrow> ceqv \<Gamma> xfdc rv' t t' (CALL dsb_'proc()) (?d'1501 rv xfdca rva xfdcb rvb xfdcc rv')
 3. \<And>rv xfdca rva xfdcb rvb xfdcc rvc rv'. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5; dc rv xfdca; dc rva xfdcb; dc rvb xfdcc; dc rvc rv'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q1501 rv xfdca rva xfdcb rvb xfdcc rvc) (?Q'1501 rv xfdca rva xfdcb rvb xfdcc rvc rv') [SKIP] (doMachineOp dsb) (?d'1501 rv xfdca rva xfdcb rvb xfdcc rv')
 4. \<And>rv xfdca rva xfdcb rvb xfdc. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5; dc rv xfdca; dc rva xfdcb; dc rvb xfdc\<rbrakk> \<Longrightarrow> \<lbrace>?R1505 rv xfdca rva xfdcb rvb\<rbrace> doMachineOp (cacheRangeOp cleanInvalByVA w1 w2 w3) \<lbrace>?Q1501 rv xfdca rva xfdcb rvb xfdc\<rbrace>
 5. \<And>rv xfdca rva xfdcb rvb xfdcc. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5; dc rv xfdca; dc rva xfdcb; dc rvb xfdcc\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (?Q'1501 rv xfdca rva xfdcb rvb xfdcc)
 6. \<And>rv xfdca rva xfdc. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5; dc rv xfdca; dc rva xfdc\<rbrakk> \<Longrightarrow> \<lbrace>?R1363 rv xfdca rva\<rbrace> doMachineOp (cleanInvalidateL2Range w3 (w3 + (w2 - w1))) \<lbrace>\<lambda>a. (\<lambda>a. w1 \<le> w2 \<and> w3 \<le> w3 + (w2 - w1) \<and> w1 && mask 5 = w3 && mask 5) and ?R1505 rv xfdca rva xfdc a\<rbrace>
 7. \<And>rv xfdc. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5; dc rv xfdc\<rbrakk> \<Longrightarrow> \<lbrace>?R1314 rv\<rbrace> doMachineOp dsb \<lbrace>\<lambda>a. (\<lambda>a. True) and ?R1363 rv xfdc a\<rbrace>
 8. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5\<rbrakk> \<Longrightarrow> \<lbrace>?R1273 w3 w2 w1\<rbrace> doMachineOp (cleanCacheRange_PoC w1 w2 w3) \<lbrace>\<lambda>a. (\<lambda>a. True) and ?R1314 a\<rbrace>
 9. \<And>rv' s'. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5\<rbrakk> \<Longrightarrow> globals (globals_update (ghost'state_'_update id) s') = globals s'
 10. \<And>rv' s'. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5; s' \<in> {s. pstart_'_update (\<lambda>_. w3) (end_'_update (\<lambda>_. w2) (start_'_update (\<lambda>_. w1) s)) \<in> \<lbrace>\<acute>start = w1\<rbrace> \<inter> \<lbrace>\<acute>end = w2\<rbrace> \<inter> \<lbrace>\<acute>pstart = w3\<rbrace>} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> {s. s \<in> UNIV} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> {s. end_'_update (\<lambda>_. w3 + (w2 - w1)) (start_'_update (\<lambda>_. w3) s) \<in> \<lbrace>\<acute>start = w3\<rbrace> \<inter> \<lbrace>\<acute>end = w3 + (w2 - w1)\<rbrace>} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> {s. index_'_update (\<lambda>_. w1 >> 5) s \<in> \<lbrace>\<acute>index = w1 >> 5\<rbrace>}}}}\<rbrakk> \<Longrightarrow> globals_update (ghost'state_'_update id) s' \<in> {s. pstart_'_update (\<lambda>_. w3) (end_'_update (\<lambda>_. w2) (start_'_update (\<lambda>_. w1) s)) \<in> \<lbrace>\<acute>start = w1\<rbrace> \<inter> \<lbrace>\<acute>end = w2\<rbrace> \<inter> \<lbrace>\<acute>pstart = w3\<rbrace>} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> {s. s \<in> UNIV} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> {s. end_'_update (\<lambda>_. w3 + (w2 - w1)) (start_'_update (\<lambda>_. w3) s) \<in> \<lbrace>\<acute>start = w3\<rbrace> \<inter> \<lbrace>\<acute>end = w3 + (w2 - w1)\<rbrace>} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> {s. index_'_update (\<lambda>_. w1 >> 5) s \<in> \<lbrace>\<acute>index = w1 >> 5\<rbrace>}}}}
A total of 11 subgoals... proof (prove)
goal (10 subgoals):
 1. \<And>rv xfdca rva xfdcb rvb xfdcc rv' t t'. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5; dc rv xfdca; dc rva xfdcb; dc rvb xfdcc\<rbrakk> \<Longrightarrow> ceqv \<Gamma> xfdc rv' t t' (CALL dsb_'proc()) (?d'1501 rv xfdca rva xfdcb rvb xfdcc rv')
 2. \<And>rv xfdca rva xfdcb rvb xfdcc rvc rv'. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5; dc rv xfdca; dc rva xfdcb; dc rvb xfdcc; dc rvc rv'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q1501 rv xfdca rva xfdcb rvb xfdcc rvc) (?Q'1501 rv xfdca rva xfdcb rvb xfdcc rvc rv') [SKIP] (doMachineOp dsb) (?d'1501 rv xfdca rva xfdcb rvb xfdcc rv')
 3. \<And>rv xfdca rva xfdcb rvb xfdc. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5; dc rv xfdca; dc rva xfdcb; dc rvb xfdc\<rbrakk> \<Longrightarrow> \<lbrace>?R1505 rv xfdca rva xfdcb rvb\<rbrace> doMachineOp (cacheRangeOp cleanInvalByVA w1 w2 w3) \<lbrace>?Q1501 rv xfdca rva xfdcb rvb xfdc\<rbrace>
 4. \<And>rv xfdca rva xfdcb rvb xfdcc. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5; dc rv xfdca; dc rva xfdcb; dc rvb xfdcc\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (?Q'1501 rv xfdca rva xfdcb rvb xfdcc)
 5. \<And>rv xfdca rva xfdc. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5; dc rv xfdca; dc rva xfdc\<rbrakk> \<Longrightarrow> \<lbrace>?R1363 rv xfdca rva\<rbrace> doMachineOp (cleanInvalidateL2Range w3 (w3 + (w2 - w1))) \<lbrace>\<lambda>a. (\<lambda>a. w1 \<le> w2 \<and> w3 \<le> w3 + (w2 - w1) \<and> w1 && mask 5 = w3 && mask 5) and ?R1505 rv xfdca rva xfdc a\<rbrace>
 6. \<And>rv xfdc. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5; dc rv xfdc\<rbrakk> \<Longrightarrow> \<lbrace>?R1314 rv\<rbrace> doMachineOp dsb \<lbrace>\<lambda>a. (\<lambda>a. True) and ?R1363 rv xfdc a\<rbrace>
 7. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5\<rbrakk> \<Longrightarrow> \<lbrace>?R1273 w3 w2 w1\<rbrace> doMachineOp (cleanCacheRange_PoC w1 w2 w3) \<lbrace>\<lambda>a. (\<lambda>a. True) and ?R1314 a\<rbrace>
 8. \<And>rv' s'. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5\<rbrakk> \<Longrightarrow> globals (globals_update (ghost'state_'_update id) s') = globals s'
 9. \<And>rv' s'. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5; s' \<in> {s. pstart_'_update (\<lambda>_. w3) (end_'_update (\<lambda>_. w2) (start_'_update (\<lambda>_. w1) s)) \<in> \<lbrace>\<acute>start = w1\<rbrace> \<inter> \<lbrace>\<acute>end = w2\<rbrace> \<inter> \<lbrace>\<acute>pstart = w3\<rbrace>} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> {s. s \<in> UNIV} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> {s. end_'_update (\<lambda>_. w3 + (w2 - w1)) (start_'_update (\<lambda>_. w3) s) \<in> \<lbrace>\<acute>start = w3\<rbrace> \<inter> \<lbrace>\<acute>end = w3 + (w2 - w1)\<rbrace>} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> {s. index_'_update (\<lambda>_. w1 >> 5) s \<in> \<lbrace>\<acute>index = w1 >> 5\<rbrace>}}}}\<rbrakk> \<Longrightarrow> globals_update (ghost'state_'_update id) s' \<in> {s. pstart_'_update (\<lambda>_. w3) (end_'_update (\<lambda>_. w2) (start_'_update (\<lambda>_. w1) s)) \<in> \<lbrace>\<acute>start = w1\<rbrace> \<inter> \<lbrace>\<acute>end = w2\<rbrace> \<inter> \<lbrace>\<acute>pstart = w3\<rbrace>} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> {s. s \<in> UNIV} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> {s. end_'_update (\<lambda>_. w3 + (w2 - w1)) (start_'_update (\<lambda>_. w3) s) \<in> \<lbrace>\<acute>start = w3\<rbrace> \<inter> \<lbrace>\<acute>end = w3 + (w2 - w1)\<rbrace>} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> {s. index_'_update (\<lambda>_. w1 >> 5) s \<in> \<lbrace>\<acute>index = w1 >> 5\<rbrace>}}}}
 10. \<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> ((\<lambda>a. start \<le> end \<and> pstart \<le> pstart + (end - start) \<and> start && mask 5 = pstart && mask 5) and ?R1273 pstart end start) s \<and> s' \<in> {s. s \<in> {s. pstart_'_update (\<lambda>_. pstart) (end_'_update (\<lambda>_. end) (start_'_update (\<lambda>_. start) s)) \<in> \<lbrace>\<acute>start = start\<rbrace> \<inter> \<lbrace>\<acute>end = end\<rbrace> \<inter> \<lbrace>\<acute>pstart = pstart\<rbrace>} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> {s. s \<in> UNIV} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> {s. end_'_update (\<lambda>_. pstart + (end - start)) (start_'_update (\<lambda>_. pstart) s) \<in> \<lbrace>\<acute>start = pstart\<rbrace> \<inter> \<lbrace>\<acute>end = pstart + (end - start)\<rbrace>} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<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 (9 subgoals):
 1. \<And>rv xfdca rva xfdcb rvb xfdcc rvc rv'. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5; dc rv xfdca; dc rva xfdcb; dc rvb xfdcc; dc rvc rv'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q1501 rv xfdca rva xfdcb rvb xfdcc rvc) (?Q'1501 rv xfdca rva xfdcb rvb xfdcc rvc rv') [SKIP] (doMachineOp dsb) (CALL dsb_'proc())
 2. \<And>rv xfdca rva xfdcb rvb xfdc. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5; dc rv xfdca; dc rva xfdcb; dc rvb xfdc\<rbrakk> \<Longrightarrow> \<lbrace>?R1505 rv xfdca rva xfdcb rvb\<rbrace> doMachineOp (cacheRangeOp cleanInvalByVA w1 w2 w3) \<lbrace>?Q1501 rv xfdca rva xfdcb rvb xfdc\<rbrace>
 3. \<And>rv xfdca rva xfdcb rvb xfdcc. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5; dc rv xfdca; dc rva xfdcb; dc rvb xfdcc\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (?Q'1501 rv xfdca rva xfdcb rvb xfdcc)
 4. \<And>rv xfdca rva xfdc. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5; dc rv xfdca; dc rva xfdc\<rbrakk> \<Longrightarrow> \<lbrace>?R1363 rv xfdca rva\<rbrace> doMachineOp (cleanInvalidateL2Range w3 (w3 + (w2 - w1))) \<lbrace>\<lambda>a. (\<lambda>a. w1 \<le> w2 \<and> w3 \<le> w3 + (w2 - w1) \<and> w1 && mask 5 = w3 && mask 5) and ?R1505 rv xfdca rva xfdc a\<rbrace>
 5. \<And>rv xfdc. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5; dc rv xfdc\<rbrakk> \<Longrightarrow> \<lbrace>?R1314 rv\<rbrace> doMachineOp dsb \<lbrace>\<lambda>a. (\<lambda>a. True) and ?R1363 rv xfdc a\<rbrace>
 6. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5\<rbrakk> \<Longrightarrow> \<lbrace>?R1273 w3 w2 w1\<rbrace> doMachineOp (cleanCacheRange_PoC w1 w2 w3) \<lbrace>\<lambda>a. (\<lambda>a. True) and ?R1314 a\<rbrace>
 7. \<And>rv' s'. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5\<rbrakk> \<Longrightarrow> globals (globals_update (ghost'state_'_update id) s') = globals s'
 8. \<And>rv' s'. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5; s' \<in> {s. pstart_'_update (\<lambda>_. w3) (end_'_update (\<lambda>_. w2) (start_'_update (\<lambda>_. w1) s)) \<in> \<lbrace>\<acute>start = w1\<rbrace> \<inter> \<lbrace>\<acute>end = w2\<rbrace> \<inter> \<lbrace>\<acute>pstart = w3\<rbrace>} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> {s. s \<in> UNIV} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> {s. end_'_update (\<lambda>_. w3 + (w2 - w1)) (start_'_update (\<lambda>_. w3) s) \<in> \<lbrace>\<acute>start = w3\<rbrace> \<inter> \<lbrace>\<acute>end = w3 + (w2 - w1)\<rbrace>} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> {s. index_'_update (\<lambda>_. w1 >> 5) s \<in> \<lbrace>\<acute>index = w1 >> 5\<rbrace>}}}}\<rbrakk> \<Longrightarrow> globals_update (ghost'state_'_update id) s' \<in> {s. pstart_'_update (\<lambda>_. w3) (end_'_update (\<lambda>_. w2) (start_'_update (\<lambda>_. w1) s)) \<in> \<lbrace>\<acute>start = w1\<rbrace> \<inter> \<lbrace>\<acute>end = w2\<rbrace> \<inter> \<lbrace>\<acute>pstart = w3\<rbrace>} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> {s. s \<in> UNIV} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> {s. end_'_update (\<lambda>_. w3 + (w2 - w1)) (start_'_update (\<lambda>_. w3) s) \<in> \<lbrace>\<acute>start = w3\<rbrace> \<inter> \<lbrace>\<acute>end = w3 + (w2 - w1)\<rbrace>} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> {s. index_'_update (\<lambda>_. w1 >> 5) s \<in> \<lbrace>\<acute>index = w1 >> 5\<rbrace>}}}}
 9. \<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> ((\<lambda>a. start \<le> end \<and> pstart \<le> pstart + (end - start) \<and> start && mask 5 = pstart && mask 5) and ?R1273 pstart end start) s \<and> s' \<in> {s. s \<in> {s. pstart_'_update (\<lambda>_. pstart) (end_'_update (\<lambda>_. end) (start_'_update (\<lambda>_. start) s)) \<in> \<lbrace>\<acute>start = start\<rbrace> \<inter> \<lbrace>\<acute>end = end\<rbrace> \<inter> \<lbrace>\<acute>pstart = pstart\<rbrace>} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> {s. s \<in> UNIV} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> {s. end_'_update (\<lambda>_. pstart + (end - start)) (start_'_update (\<lambda>_. pstart) s) \<in> \<lbrace>\<acute>start = pstart\<rbrace> \<inter> \<lbrace>\<acute>end = pstart + (end - start)\<rbrace>} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<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 (8 subgoals):
 1. \<And>rv xfdca rva xfdcb rvb xfdc. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5; dc rv xfdca; dc rva xfdcb; dc rvb xfdc\<rbrakk> \<Longrightarrow> \<lbrace>?R1505 rv xfdca rva xfdcb rvb\<rbrace> doMachineOp (cacheRangeOp cleanInvalByVA w1 w2 w3) \<lbrace>\<lambda>rvc _. True\<rbrace>
 2. \<And>rv xfdca rva xfdcb rvb xfdcc. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5; dc rv xfdca; dc rva xfdcb; dc rvb xfdcc\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (\<lambda>rvc rv'. {s. s \<in> UNIV})
 3. \<And>rv xfdca rva xfdc. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5; dc rv xfdca; dc rva xfdc\<rbrakk> \<Longrightarrow> \<lbrace>?R1363 rv xfdca rva\<rbrace> doMachineOp (cleanInvalidateL2Range w3 (w3 + (w2 - w1))) \<lbrace>\<lambda>a. (\<lambda>a. w1 \<le> w2 \<and> w3 \<le> w3 + (w2 - w1) \<and> w1 && mask 5 = w3 && mask 5) and ?R1505 rv xfdca rva xfdc a\<rbrace>
 4. \<And>rv xfdc. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5; dc rv xfdc\<rbrakk> \<Longrightarrow> \<lbrace>?R1314 rv\<rbrace> doMachineOp dsb \<lbrace>\<lambda>a. (\<lambda>a. True) and ?R1363 rv xfdc a\<rbrace>
 5. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5\<rbrakk> \<Longrightarrow> \<lbrace>?R1273 w3 w2 w1\<rbrace> doMachineOp (cleanCacheRange_PoC w1 w2 w3) \<lbrace>\<lambda>a. (\<lambda>a. True) and ?R1314 a\<rbrace>
 6. \<And>rv' s'. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5\<rbrakk> \<Longrightarrow> globals (globals_update (ghost'state_'_update id) s') = globals s'
 7. \<And>rv' s'. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5; s' \<in> {s. pstart_'_update (\<lambda>_. w3) (end_'_update (\<lambda>_. w2) (start_'_update (\<lambda>_. w1) s)) \<in> \<lbrace>\<acute>start = w1\<rbrace> \<inter> \<lbrace>\<acute>end = w2\<rbrace> \<inter> \<lbrace>\<acute>pstart = w3\<rbrace>} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> {s. s \<in> UNIV} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> {s. end_'_update (\<lambda>_. w3 + (w2 - w1)) (start_'_update (\<lambda>_. w3) s) \<in> \<lbrace>\<acute>start = w3\<rbrace> \<inter> \<lbrace>\<acute>end = w3 + (w2 - w1)\<rbrace>} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> {s. index_'_update (\<lambda>_. w1 >> 5) s \<in> \<lbrace>\<acute>index = w1 >> 5\<rbrace>}}}}\<rbrakk> \<Longrightarrow> globals_update (ghost'state_'_update id) s' \<in> {s. pstart_'_update (\<lambda>_. w3) (end_'_update (\<lambda>_. w2) (start_'_update (\<lambda>_. w1) s)) \<in> \<lbrace>\<acute>start = w1\<rbrace> \<inter> \<lbrace>\<acute>end = w2\<rbrace> \<inter> \<lbrace>\<acute>pstart = w3\<rbrace>} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> {s. s \<in> UNIV} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> {s. end_'_update (\<lambda>_. w3 + (w2 - w1)) (start_'_update (\<lambda>_. w3) s) \<in> \<lbrace>\<acute>start = w3\<rbrace> \<inter> \<lbrace>\<acute>end = w3 + (w2 - w1)\<rbrace>} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> {s. index_'_update (\<lambda>_. w1 >> 5) s \<in> \<lbrace>\<acute>index = w1 >> 5\<rbrace>}}}}
 8. \<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> ((\<lambda>a. start \<le> end \<and> pstart \<le> pstart + (end - start) \<and> start && mask 5 = pstart && mask 5) and ?R1273 pstart end start) s \<and> s' \<in> {s. s \<in> {s. pstart_'_update (\<lambda>_. pstart) (end_'_update (\<lambda>_. end) (start_'_update (\<lambda>_. start) s)) \<in> \<lbrace>\<acute>start = start\<rbrace> \<inter> \<lbrace>\<acute>end = end\<rbrace> \<inter> \<lbrace>\<acute>pstart = pstart\<rbrace>} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> {s. s \<in> UNIV} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> {s. end_'_update (\<lambda>_. pstart + (end - start)) (start_'_update (\<lambda>_. pstart) s) \<in> \<lbrace>\<acute>start = pstart\<rbrace> \<inter> \<lbrace>\<acute>end = pstart + (end - start)\<rbrace>} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<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!