theory Machine_C

lemma cleanCacheRange_RAM_ccorres:
  "ccorres dc xfdc (\<lambda>s. w1 \<le> w2 \<and> w3 \<le> w3 + (w2 - w1)
                      \<and> w1 && mask 5 = w3 && mask 5
                      \<and> 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_RAM w1 w2 w3))
           (Call cleanCacheRange_RAM_'proc)" apply (cinit' lift: start_' end_' pstart_') apply (simp add: cleanCacheRange_RAM_def doMachineOp_bind empty_fail_dsb empty_fail_cleanL2Range
                    empty_fail_cond) apply (rule ccorres_Guard_Seq) apply (rule ccorres_basic_srnoop2, simp) apply (ctac (no_vcg) add: cleanCacheRange_PoC_ccorres) apply (ctac (no_vcg) add: dsb_ccorres) apply (rule_tac P="\<lambda>s. unat (w2 - w1) \<le> gsMaxObjectSize s"
        in ccorres_cross_over_guard) apply (rule ccorres_Guard_Seq) apply (rule ccorres_basic_srnoop2, simp) apply (ctac (no_vcg) add: cleanL2Range_ccorres) apply wp+ apply clarsimp apply (auto dest: ghost_assertion_size_logic simp: o_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres dc xfdc (\<lambda>s. w1 \<le> w2 \<and> w3 \<le> w3 + (w2 - w1) \<and> w1 && mask 5 = w3 && mask 5 \<and> 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_RAM w1 w2 w3)) (Call cleanCacheRange_RAM_'proc) proof (prove)
goal (2 subgoals):
 1. \<And>pstart end start. \<lbrakk>pstart = w3; end = w2; start = w1\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q378 pstart end start) (?Q'378 pstart end start) [SKIP] (doMachineOp (cleanCacheRange_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 \<and> pstart \<le> pstart + (end - start)\<rbrace> (\<acute>globals :== ghost'state_'_update id);;
(CALL cleanCacheRange_PoC_'proc(start,end,pstart);;
(CALL dsb_'proc();;
(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);;
CALL plat_cleanL2Range_'proc(pstart,pstart + (end - start))))))
 2. \<And>pstart end start s s'. \<lbrakk>pstart = w3; end = w2; start = w1; (s, s') \<in> rf_sr; w1 \<le> w2 \<and> w3 \<le> w3 + (w2 - w1) \<and> w1 && mask 5 = w3 && mask 5 \<and> unat (w2 - w1) \<le> gsMaxObjectSize s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q378 pstart end start s \<and> s' \<in> ?Q'378 pstart end start proof (prove)
goal (2 subgoals):
 1. \<And>pstart end start. \<lbrakk>pstart = w3; end = w2; start = w1\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q378 w3 w2 w1) (?Q'378 w3 w2 w1) [SKIP] (do rv <- doMachineOp (cleanCacheRange_PoC w1 w2 w3);
rv <- doMachineOp dsb;
doMachineOp (cleanL2Range w3 (w3 + (w2 - w1)))
od) (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) \<and> w1 \<le> w2 \<and> w3 \<le> w3 + (w2 - w1)\<rbrace> (\<acute>globals :== ghost'state_'_update id);;
(CALL cleanCacheRange_PoC_'proc(w1,w2,w3);;
(CALL dsb_'proc();;
(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) \<and> w1 \<le> w2 \<and> w3 \<le> w3 + (w2 - w1)\<rbrace> (\<acute>globals :== ghost'state_'_update id);;
CALL plat_cleanL2Range_'proc(w3,w3 + (w2 - w1))))))
 2. \<And>pstart end start s s'. \<lbrakk>pstart = w3; end = w2; start = w1; (s, s') \<in> rf_sr; w1 \<le> w2 \<and> w3 \<le> w3 + (w2 - w1) \<and> w1 && mask 5 = w3 && mask 5 \<and> unat (w2 - w1) \<le> gsMaxObjectSize s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q378 pstart end start s \<and> s' \<in> ?Q'378 pstart end start proof (prove)
goal (2 subgoals):
 1. \<And>pstart end start. \<lbrakk>pstart = w3; end = w2; start = w1\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q378 w3 w2 w1) (?C'386 w3 w2 w1) [SKIP] (do rv <- doMachineOp (cleanCacheRange_PoC w1 w2 w3);
rv <- doMachineOp dsb;
doMachineOp (cleanL2Range w3 (w3 + (w2 - w1)))
od) (\<acute>globals :== ghost'state_'_update id;;
(CALL cleanCacheRange_PoC_'proc(w1,w2,w3);;
(CALL dsb_'proc();;
(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) \<and> w1 \<le> w2 \<and> w3 \<le> w3 + (w2 - w1)\<rbrace> (\<acute>globals :== ghost'state_'_update id);;
CALL plat_cleanL2Range_'proc(w3,w3 + (w2 - w1))))))
 2. \<And>pstart end start s s'. \<lbrakk>pstart = w3; end = w2; start = w1; (s, s') \<in> rf_sr; w1 \<le> w2 \<and> w3 \<le> w3 + (w2 - w1) \<and> w1 && mask 5 = w3 && mask 5 \<and> unat (w2 - w1) \<le> gsMaxObjectSize s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q378 pstart end start s \<and> s' \<in> ?C'386 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) \<and> start \<le> end \<and> pstart \<le> pstart + (end - start)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>pstart end start. \<lbrakk>pstart = w3; end = w2; start = w1\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q378 w3 w2 w1) (?G'393 w3 w2 w1) [SKIP] (do rv <- doMachineOp (cleanCacheRange_PoC w1 w2 w3);
rv <- doMachineOp dsb;
doMachineOp (cleanL2Range w3 (w3 + (w2 - w1)))
od) (CALL cleanCacheRange_PoC_'proc(w1,w2,w3);;
(CALL dsb_'proc();;
(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) \<and> w1 \<le> w2 \<and> w3 \<le> w3 + (w2 - w1)\<rbrace> (\<acute>globals :== ghost'state_'_update id);;
CALL plat_cleanL2Range_'proc(w3,w3 + (w2 - w1)))))
 2. \<And>pstart end start s s'. \<lbrakk>pstart = w3; end = w2; start = w1; (s, s') \<in> rf_sr; w1 \<le> w2 \<and> w3 \<le> w3 + (w2 - w1) \<and> w1 && mask 5 = w3 && mask 5 \<and> unat (w2 - w1) \<le> gsMaxObjectSize s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q378 pstart end start s \<and> s' \<in> {s. globals_update (ghost'state_'_update id) s \<in> ?G'393 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) \<and> start \<le> end \<and> pstart \<le> pstart + (end - start)\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>pstart end start rv xfdca. \<lbrakk>pstart = w3; end = w2; start = w1; dc rv xfdca\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q401 pstart end start rv) (?Q'415 rv xfdca) [SKIP] (do rv <- doMachineOp dsb;
doMachineOp (cleanL2Range w3 (w3 + (w2 - w1)))
od) (CALL dsb_'proc();;
(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) \<and> w1 \<le> w2 \<and> w3 \<le> w3 + (w2 - w1)\<rbrace> (\<acute>globals :== ghost'state_'_update id);;
CALL plat_cleanL2Range_'proc(w3,w3 + (w2 - w1))))
 2. \<And>pstart end start. \<lbrakk>pstart = w3; end = w2; start = w1\<rbrakk> \<Longrightarrow> \<lbrace>?R409 w3 w2 w1\<rbrace> doMachineOp (cleanCacheRange_PoC w1 w2 w3) \<lbrace>?Q401 pstart end start\<rbrace>
 3. \<And>pstart end start s s'. \<lbrakk>pstart = w3; end = w2; start = w1; (s, s') \<in> rf_sr; w1 \<le> w2 \<and> w3 \<le> w3 + (w2 - w1) \<and> w1 && mask 5 = w3 && mask 5 \<and> 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 ?R409 pstart end start) s \<and> s' \<in> {s. globals_update (ghost'state_'_update id) 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'414 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) \<and> start \<le> end \<and> pstart \<le> pstart + (end - start)\<rbrace>
flex-flex pairs:
\<lambda>t rv. ?Q'415 rv (xfdc t) \<equiv>\<^sup>? ?Q'414 w3 w2 w1 proof (prove)
goal (4 subgoals):
 1. \<And>pstart end start rv xfdca rva xfdcb. \<lbrakk>pstart = w3; end = w2; start = w1; dc rv xfdca; dc rva xfdcb\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q447 pstart end start rv xfdca rva) (?Q'464 rv xfdca rva xfdcb) [SKIP] (doMachineOp (cleanL2Range w3 (w3 + (w2 - w1)))) (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) \<and> w1 \<le> w2 \<and> w3 \<le> w3 + (w2 - w1)\<rbrace> (\<acute>globals :== ghost'state_'_update id);;
CALL plat_cleanL2Range_'proc(w3,w3 + (w2 - w1)))
 2. \<And>pstart end start rv xfdc. \<lbrakk>pstart = w3; end = w2; start = w1; dc rv xfdc\<rbrakk> \<Longrightarrow> \<lbrace>?R460 pstart end start rv\<rbrace> doMachineOp dsb \<lbrace>?Q447 pstart end start rv xfdc\<rbrace>
 3. \<And>pstart end start. \<lbrakk>pstart = w3; end = w2; start = w1\<rbrakk> \<Longrightarrow> \<lbrace>?R409 w3 w2 w1\<rbrace> doMachineOp (cleanCacheRange_PoC w1 w2 w3) \<lbrace>\<lambda>a. (\<lambda>a. True) and ?R460 pstart end start a\<rbrace>
 4. \<And>pstart end start s s'. \<lbrakk>pstart = w3; end = w2; start = w1; (s, s') \<in> rf_sr; w1 \<le> w2 \<and> w3 \<le> w3 + (w2 - w1) \<and> w1 && mask 5 = w3 && mask 5 \<and> 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 ?R409 pstart end start) s \<and> s' \<in> {s. globals_update (ghost'state_'_update id) 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'465 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) \<and> start \<le> end \<and> pstart \<le> pstart + (end - start)\<rbrace>
flex-flex pairs:
?Q'465 w3 w2 w1 \<equiv>\<^sup>? \<lambda>t rv ta rva. ?Q'464 rv (xfdc t) rva (xfdc ta) proof (prove)
goal (4 subgoals):
 1. \<And>pstart end start rv xfdca rva xfdcb. \<lbrakk>pstart = w3; end = w2; start = w1; dc rv xfdca; dc rva xfdcb\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?P'503 pstart end start rv xfdca rva) (?Q500 rv xfdca rva xfdcb) [SKIP] (doMachineOp (cleanL2Range w3 (w3 + (w2 - w1)))) (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) \<and> w1 \<le> w2 \<and> w3 \<le> w3 + (w2 - w1)\<rbrace> (\<acute>globals :== ghost'state_'_update id);;
CALL plat_cleanL2Range_'proc(w3,w3 + (w2 - w1)))
 2. \<And>pstart end start rv xfdc. \<lbrakk>pstart = w3; end = w2; start = w1; dc rv xfdc\<rbrakk> \<Longrightarrow> \<lbrace>?R460 pstart end start rv\<rbrace> doMachineOp dsb \<lbrace>\<lambda>a. (\<lambda>s. unat (w2 - w1) \<le> gsMaxObjectSize s) and ?P'503 pstart end start rv xfdc a\<rbrace>
 3. \<And>pstart end start. \<lbrakk>pstart = w3; end = w2; start = w1\<rbrakk> \<Longrightarrow> \<lbrace>?R409 w3 w2 w1\<rbrace> doMachineOp (cleanCacheRange_PoC w1 w2 w3) \<lbrace>\<lambda>a. (\<lambda>a. True) and ?R460 pstart end start a\<rbrace>
 4. \<And>pstart end start s s'. \<lbrakk>pstart = w3; end = w2; start = w1; (s, s') \<in> rf_sr; w1 \<le> w2 \<and> w3 \<le> w3 + (w2 - w1) \<and> w1 && mask 5 = w3 && mask 5 \<and> 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 ?R409 pstart end start) s \<and> s' \<in> {s. globals_update (ghost'state_'_update id) 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'. \<forall>s. (s, s') \<in> rf_sr \<and> unat (end - start) \<le> gsMaxObjectSize s \<longrightarrow> s' \<in> ?Q501 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) \<and> start \<le> end \<and> pstart \<le> pstart + (end - start)\<rbrace>
flex-flex pairs:
\<lambda>t rv ta rva. ?Q500 rv (xfdc t) rva (xfdc ta) \<equiv>\<^sup>? ?Q501 w3 w2 w1 proof (prove)
goal (4 subgoals):
 1. \<And>pstart end start rv xfdca rva xfdcb. \<lbrakk>pstart = w3; end = w2; start = w1; dc rv xfdca; dc rva xfdcb\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?P'503 pstart end start rv xfdca rva) (?C'508 rv xfdca rva xfdcb) [SKIP] (doMachineOp (cleanL2Range w3 (w3 + (w2 - w1)))) (\<acute>globals :== ghost'state_'_update id;;
CALL plat_cleanL2Range_'proc(w3,w3 + (w2 - w1)))
 2. \<And>pstart end start rv xfdc. \<lbrakk>pstart = w3; end = w2; start = w1; dc rv xfdc\<rbrakk> \<Longrightarrow> \<lbrace>?R460 pstart end start rv\<rbrace> doMachineOp dsb \<lbrace>\<lambda>a. (\<lambda>s. unat (w2 - w1) \<le> gsMaxObjectSize s) and ?P'503 pstart end start rv xfdc a\<rbrace>
 3. \<And>pstart end start. \<lbrakk>pstart = w3; end = w2; start = w1\<rbrakk> \<Longrightarrow> \<lbrace>?R409 w3 w2 w1\<rbrace> doMachineOp (cleanCacheRange_PoC w1 w2 w3) \<lbrace>\<lambda>a. (\<lambda>a. True) and ?R460 pstart end start a\<rbrace>
 4. \<And>pstart end start s s'. \<lbrakk>pstart = w3; end = w2; start = w1; (s, s') \<in> rf_sr; w1 \<le> w2 \<and> w3 \<le> w3 + (w2 - w1) \<and> w1 && mask 5 = w3 && mask 5 \<and> 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 ?R409 pstart end start) s \<and> s' \<in> {s. globals_update (ghost'state_'_update id) 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'. \<forall>s. (s, s') \<in> rf_sr \<and> unat (end - start) \<le> gsMaxObjectSize s \<longrightarrow> s' \<in> ?C'506 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) \<and> start \<le> end \<and> pstart \<le> pstart + (end - start)\<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) \<and> start \<le> end \<and> pstart \<le> pstart + (end - start)\<rbrace>
flex-flex pairs:
\<lambda>t rv ta rva. ?C'508 rv (xfdc t) rva (xfdc ta) \<equiv>\<^sup>? ?C'506 w3 w2 w1 proof (prove)
goal (4 subgoals):
 1. \<And>pstart end start rv xfdca rva xfdcb. \<lbrakk>pstart = w3; end = w2; start = w1; dc rv xfdca; dc rva xfdcb\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?P'503 pstart end start rv xfdca rva) (?G'515 rv xfdca rva xfdcb) [SKIP] (doMachineOp (cleanL2Range w3 (w3 + (w2 - w1)))) (CALL plat_cleanL2Range_'proc(w3,w3 + (w2 - w1)))
 2. \<And>pstart end start rv xfdc. \<lbrakk>pstart = w3; end = w2; start = w1; dc rv xfdc\<rbrakk> \<Longrightarrow> \<lbrace>?R460 pstart end start rv\<rbrace> doMachineOp dsb \<lbrace>\<lambda>a. (\<lambda>s. unat (w2 - w1) \<le> gsMaxObjectSize s) and ?P'503 pstart end start rv xfdc a\<rbrace>
 3. \<And>pstart end start. \<lbrakk>pstart = w3; end = w2; start = w1\<rbrakk> \<Longrightarrow> \<lbrace>?R409 w3 w2 w1\<rbrace> doMachineOp (cleanCacheRange_PoC w1 w2 w3) \<lbrace>\<lambda>a. (\<lambda>a. True) and ?R460 pstart end start a\<rbrace>
 4. \<And>pstart end start s s'. \<lbrakk>pstart = w3; end = w2; start = w1; (s, s') \<in> rf_sr; w1 \<le> w2 \<and> w3 \<le> w3 + (w2 - w1) \<and> w1 && mask 5 = w3 && mask 5 \<and> 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 ?R409 pstart end start) s \<and> s' \<in> {s. globals_update (ghost'state_'_update id) 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'. \<forall>s. (s, s') \<in> rf_sr \<and> unat (end - start) \<le> gsMaxObjectSize s \<longrightarrow> s' \<in> {s. globals_update (ghost'state_'_update id) s \<in> ?G'516 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) \<and> start \<le> end \<and> pstart \<le> pstart + (end - start)\<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) \<and> start \<le> end \<and> pstart \<le> pstart + (end - start)\<rbrace>
flex-flex pairs:
?G'516 w3 w2 w1 \<equiv>\<^sup>? \<lambda>t rv ta rva. ?G'515 rv (xfdc t) rva (xfdc ta) proof (prove)
goal (3 subgoals):
 1. \<And>pstart end start rv xfdc. \<lbrakk>pstart = w3; end = w2; start = w1; dc rv xfdc\<rbrakk> \<Longrightarrow> \<lbrace>?R460 pstart end start rv\<rbrace> doMachineOp dsb \<lbrace>\<lambda>a. (\<lambda>s. unat (w2 - w1) \<le> gsMaxObjectSize s) and (\<lambda>a. True)\<rbrace>
 2. \<And>pstart end start. \<lbrakk>pstart = w3; end = w2; start = w1\<rbrakk> \<Longrightarrow> \<lbrace>?R409 w3 w2 w1\<rbrace> doMachineOp (cleanCacheRange_PoC w1 w2 w3) \<lbrace>\<lambda>a. (\<lambda>a. True) and ?R460 pstart end start a\<rbrace>
 3. \<And>pstart end start s s'. \<lbrakk>pstart = w3; end = w2; start = w1; (s, s') \<in> rf_sr; w1 \<le> w2 \<and> w3 \<le> w3 + (w2 - w1) \<and> w1 && mask 5 = w3 && mask 5 \<and> 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 ?R409 pstart end start) s \<and> s' \<in> {s. globals_update (ghost'state_'_update id) 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'. \<forall>s. (s, s') \<in> rf_sr \<and> unat (end - start) \<le> gsMaxObjectSize s \<longrightarrow> s' \<in> {s. globals_update (ghost'state_'_update id) s \<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> \<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>}}}} \<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) \<and> start \<le> end \<and> pstart \<le> pstart + (end - start)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>pstart end start s s'. \<lbrakk>pstart = w3; end = w2; start = w1; (s, s') \<in> rf_sr; w1 \<le> w2 \<and> w3 \<le> w3 + (w2 - w1) \<and> w1 && mask 5 = w3 && mask 5 \<and> 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 (\<lambda>a. True \<and> unat (end - start) \<le> gsMaxObjectSize a \<and> True)) s \<and> s' \<in> {s. globals_update (ghost'state_'_update id) 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'. \<forall>s. (s, s') \<in> rf_sr \<and> unat (end - start) \<le> gsMaxObjectSize s \<longrightarrow> s' \<in> {s. globals_update (ghost'state_'_update id) s \<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> \<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>}}}} \<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) \<and> start \<le> end \<and> pstart \<le> pstart + (end - start)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5; unat (w2 - w1) \<le> gsMaxObjectSize s\<rbrakk> \<Longrightarrow> (\<forall>t. (\<exists>s. (s, s'\<lparr>globals := globals t\<rparr>) \<in> rf_sr \<and> unat (w2 - w1) \<le> gsMaxObjectSize s) \<longrightarrow> ghost_assertion_data_get cap_get_capSizeBits_'proc (\<lambda>a. snd (snd a)) (ghost'state_' (globals t)) = 0 \<or> w2 - w1 \<le> ghost_assertion_data_get cap_get_capSizeBits_'proc (\<lambda>a. snd (snd a)) (ghost'state_' (globals t))) \<and> (ghost_assertion_data_get cap_get_capSizeBits_'proc (\<lambda>a. snd (snd a)) (ghost'state_' (globals s')) = 0 \<or> w2 - w1 \<le> ghost_assertion_data_get cap_get_capSizeBits_'proc (\<lambda>a. snd (snd a)) (ghost'state_' (globals s'))) proof (prove)
goal:
No subgoals!