theory VSpace_C

lemma performPageDirectoryInvocationFlush_ccorres:
  "ccorres (K (K \<bottom>) \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_')
       (invs' and K (asid \<le> mask asid_bits)
              and (\<lambda>s. ps \<le> ps + (ve - vs) \<and> vs && mask 5 = ps && mask 5
                  \<and> unat (ve - vs) \<le> gsMaxObjectSize s))
       (\<lbrace>\<acute>pd = Ptr pd\<rbrace> \<inter> \<lbrace>\<acute>asid = asid\<rbrace> \<inter>
               \<lbrace>\<acute>start = vs\<rbrace> \<inter> \<lbrace>\<acute>end =  ve\<rbrace> \<inter> \<lbrace>\<acute>pstart = ps\<rbrace> \<inter> \<lbrace>flushtype_relation typ \<acute>invLabel___int \<rbrace>)
       []
       (liftE (performPageDirectoryInvocation (PageDirectoryFlush typ vs ve ps pd asid)))
       (Call performPDFlush_'proc)" apply (simp only: liftE_liftM ccorres_liftM_simp) apply (cinit lift: pd_' asid_' start_' end_' pstart_' invLabel___int_') apply (unfold when_def) apply (rule ccorres_cond_seq) apply (rule ccorres_cond2[where R=\<top>]) apply (simp split: if_split) apply (rule ccorres_rhs_assoc)+ apply (ctac (no_vcg) add: setVMRootForFlush_ccorres) apply (ctac (no_vcg) add: doFlush_ccorres) apply (rule ccorres_add_return2) apply (rule ccorres_split_nothrow_novcg_dc) apply (rule ccorres_cond2[where R=\<top>]) apply (simp split: if_split bool.splits) apply (rule ccorres_pre_getCurThread) apply (ctac add: setVMRoot_ccorres) apply (rule ccorres_return_Skip) apply (rule_tac P=\<top> and P'=UNIV in ccorres_from_vcg_throws) apply (rule allI, rule conseqPre, vcg) apply (clarsimp simp: return_def) apply wp apply (simp add: guard_is_UNIV_def) apply (simp add: cur_tcb'_def[symmetric]) apply (rule_tac Q="\<lambda>_ s. invs' s \<and> cur_tcb' s" in hoare_post_imp) apply (simp add: invs'_invs_no_cicd) apply wp+ apply (simp) apply (rule_tac P=\<top> and P'=UNIV in ccorres_from_vcg_throws) apply (rule allI, rule conseqPre, vcg) apply (clarsimp simp: return_def) apply (clarsimp simp: order_less_imp_le) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres (K (K (\<lambda>_. False)) \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (invs' and K (asid \<le> mask local.asid_bits) and (\<lambda>s. ps \<le> ps + (ve - vs) \<and> vs && mask 5 = ps && mask 5 \<and> unat (ve - vs) \<le> gsMaxObjectSize s)) (\<lbrace>\<acute>pd = pde_Ptr pd\<rbrace> \<inter> \<lbrace>\<acute>asid = asid\<rbrace> \<inter> \<lbrace>\<acute>start = vs\<rbrace> \<inter> \<lbrace>\<acute>end = ve\<rbrace> \<inter> \<lbrace>\<acute>pstart = ps\<rbrace> \<inter> \<lbrace>flushtype_relation typ \<acute>invLabel___int\<rbrace>) [] (liftE (performPageDirectoryInvocation (ARM_H.PageDirectoryFlush typ vs ve ps pd asid))) (Call performPDFlush_'proc) proof (prove)
goal (1 subgoal):
 1. ccorres (K (K (\<lambda>_. False)) \<currency> dc \<circ> Inr) (liftxf errstate id (K ()) ret__unsigned_long_') (invs' and K (asid \<le> mask local.asid_bits) and (\<lambda>s. ps \<le> ps + (ve - vs) \<and> vs && mask 5 = ps && mask 5 \<and> unat (ve - vs) \<le> gsMaxObjectSize s)) (\<lbrace>\<acute>pd = pde_Ptr pd\<rbrace> \<inter> \<lbrace>\<acute>asid = asid\<rbrace> \<inter> \<lbrace>\<acute>start = vs\<rbrace> \<inter> \<lbrace>\<acute>end = ve\<rbrace> \<inter> \<lbrace>\<acute>pstart = ps\<rbrace> \<inter> \<lbrace>flushtype_relation typ \<acute>invLabel___int\<rbrace>) [] (performPageDirectoryInvocation (ARM_H.PageDirectoryFlush typ vs ve ps pd asid)) (Call performPDFlush_'proc) proof (prove)
goal (2 subgoals):
 1. \<And>invLabel___int pstart end start asida pda. \<lbrakk>flushtype_relation typ invLabel___int; pstart = ps; end = ve; start = vs; asida = asid; pda = pde_Ptr pd\<rbrakk> \<Longrightarrow> ccorres (K (K (\<lambda>_. False)) \<currency> dc \<circ> Inr) (liftxf errstate id (K ()) ret__unsigned_long_') (?Q887 invLabel___int pstart end start asida pda) (?Q'887 invLabel___int pstart end start asida pda) [SKIP] (when (vs < ve) (do root_switched <- setVMRootForFlush pd asid;
y <- doMachineOp (doFlush typ vs ve ps);
when root_switched (getCurThread >>= setVMRoot)
od)) (IF start < end THEN
  \<acute>root_switched :== CALL setVMRootForFlush_'proc(pda,asida);;
CALL doFlush_'proc(invLabel___int,start,end,pstart);;
IF \<acute>root_switched \<noteq> 0 THEN
  CALL setVMRoot_'proc(\<acute>ksCurThread)
FI
FI;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))
 2. \<And>invLabel___int pstart end start asida pda s s'. \<lbrakk>flushtype_relation typ invLabel___int; pstart = ps; end = ve; start = vs; asida = asid; pda = pde_Ptr pd; (s, s') \<in> rf_sr; (invs' and (\<lambda>y. asid \<le> mask local.asid_bits) and (\<lambda>s. ps \<le> ps + (ve - vs) \<and> vs && mask 5 = ps && mask 5 \<and> unat (ve - vs) \<le> gsMaxObjectSize s)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q887 invLabel___int pstart end start asida pda s \<and> s' \<in> ?Q'887 invLabel___int pstart end start asida pda proof (prove)
goal (2 subgoals):
 1. \<And>invLabel___int pstart end start asida pda. \<lbrakk>flushtype_relation typ invLabel___int; pstart = ps; end = ve; start = vs; asida = asid; pda = pde_Ptr pd\<rbrakk> \<Longrightarrow> ccorres (K (K (\<lambda>_. False)) \<currency> dc \<circ> Inr) (liftxf errstate id (K ()) ret__unsigned_long_') (?Q887 invLabel___int pstart end start asida pda) (?Q'887 invLabel___int pstart end start asida pda) [SKIP] (if vs < ve then do root_switched <- setVMRootForFlush pd asid;
y <- doMachineOp (doFlush typ vs ve ps);
if root_switched then getCurThread >>= setVMRoot else return ()
od else return ()) (IF start < end THEN
  \<acute>root_switched :== CALL setVMRootForFlush_'proc(pda,asida);;
CALL doFlush_'proc(invLabel___int,start,end,pstart);;
IF \<acute>root_switched \<noteq> 0 THEN
  CALL setVMRoot_'proc(\<acute>ksCurThread)
FI
FI;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))
 2. \<And>invLabel___int pstart end start asida pda s s'. \<lbrakk>flushtype_relation typ invLabel___int; pstart = ps; end = ve; start = vs; asida = asid; pda = pde_Ptr pd; (s, s') \<in> rf_sr; (invs' and (\<lambda>y. asid \<le> mask local.asid_bits) and (\<lambda>s. ps \<le> ps + (ve - vs) \<and> vs && mask 5 = ps && mask 5 \<and> unat (ve - vs) \<le> gsMaxObjectSize s)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q887 invLabel___int pstart end start asida pda s \<and> s' \<in> ?Q'887 invLabel___int pstart end start asida pda proof (prove)
goal (2 subgoals):
 1. \<And>invLabel___int pstart end start asida pda. \<lbrakk>flushtype_relation typ invLabel___int; pstart = ps; end = ve; start = vs; asida = asid; pda = pde_Ptr pd\<rbrakk> \<Longrightarrow> ccorres (K (K (\<lambda>_. False)) \<currency> dc \<circ> Inr) (liftxf errstate id (K ()) ret__unsigned_long_') (?Q887 invLabel___int pstart end start asida pda) (?Q'887 invLabel___int pstart end start asida pda) [SKIP] (if vs < ve then do root_switched <- setVMRootForFlush pd asid;
y <- doMachineOp (doFlush typ vs ve ps);
if root_switched then getCurThread >>= setVMRoot else return ()
od else return ()) (IF start < end THEN
  \<acute>root_switched :== CALL setVMRootForFlush_'proc(pda,asida);;
CALL doFlush_'proc(invLabel___int,start,end,pstart);;
IF \<acute>root_switched \<noteq> 0 THEN
  CALL setVMRoot_'proc(\<acute>ksCurThread)
FI;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE)
ELSE
  SKIP;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE)
FI)
 2. \<And>invLabel___int pstart end start asida pda s s'. \<lbrakk>flushtype_relation typ invLabel___int; pstart = ps; end = ve; start = vs; asida = asid; pda = pde_Ptr pd; (s, s') \<in> rf_sr; (invs' and (\<lambda>y. asid \<le> mask local.asid_bits) and (\<lambda>s. ps \<le> ps + (ve - vs) \<and> vs && mask 5 = ps && mask 5 \<and> unat (ve - vs) \<le> gsMaxObjectSize s)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q887 invLabel___int pstart end start asida pda s \<and> s' \<in> ?Q'887 invLabel___int pstart end start asida pda proof (prove)
goal (4 subgoals):
 1. \<And>invLabel___int pstart end start asida pda. \<lbrakk>flushtype_relation typ invLabel___int; pstart = ps; end = ve; start = vs; asida = asid; pda = pde_Ptr pd\<rbrakk> \<Longrightarrow> \<forall>s s'. (s, s') \<in> rf_sr \<and> True \<longrightarrow> (vs < ve) = (s' \<in> \<lbrace>start < end\<rbrace>)
 2. \<And>invLabel___int pstart end start asida pda. \<lbrakk>flushtype_relation typ invLabel___int; pstart = ps; end = ve; start = vs; asida = asid; pda = pde_Ptr pd\<rbrakk> \<Longrightarrow> ccorres (K (K (\<lambda>_. False)) \<currency> dc \<circ> Inr) (liftxf errstate id (K ()) ret__unsigned_long_') (?Pt895 invLabel___int pstart end start asida pda) (?Rt895 invLabel___int pstart end start asida pda) [SKIP] (do root_switched <- setVMRootForFlush pd asid;
y <- doMachineOp (doFlush typ vs ve ps);
if root_switched then getCurThread >>= setVMRoot else return ()
od) (\<acute>root_switched :== CALL setVMRootForFlush_'proc(pda,asida);;
CALL doFlush_'proc(invLabel___int,start,end,pstart);;
IF \<acute>root_switched \<noteq> 0 THEN
  CALL setVMRoot_'proc(\<acute>ksCurThread)
FI;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))
 3. \<And>invLabel___int pstart end start asida pda. \<lbrakk>flushtype_relation typ invLabel___int; pstart = ps; end = ve; start = vs; asida = asid; pda = pde_Ptr pd\<rbrakk> \<Longrightarrow> ccorres (K (K (\<lambda>_. False)) \<currency> dc \<circ> Inr) (liftxf errstate id (K ()) ret__unsigned_long_') (?Pf895 invLabel___int pstart end start asida pda) (?Rf895 invLabel___int pstart end start asida pda) [SKIP] (return ()) (SKIP;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))
 4. \<And>invLabel___int pstart end start asida pda s s'. \<lbrakk>flushtype_relation typ invLabel___int; pstart = ps; end = ve; start = vs; asida = asid; pda = pde_Ptr pd; (s, s') \<in> rf_sr; (invs' and (\<lambda>y. asid \<le> mask local.asid_bits) and (\<lambda>s. ps \<le> ps + (ve - vs) \<and> vs && mask 5 = ps && mask 5 \<and> unat (ve - vs) \<le> gsMaxObjectSize s)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. vs < ve \<longrightarrow> ?Pt895 invLabel___int pstart end start asida pda s) and (\<lambda>s. \<not> vs < ve \<longrightarrow> ?Pf895 invLabel___int pstart end start asida pda s)) s \<and> s' \<in> {s. (s \<in> \<lbrace>start < end\<rbrace> \<longrightarrow> s \<in> ?Rt895 invLabel___int pstart end start asida pda) \<and> (s \<notin> \<lbrace>start < end\<rbrace> \<longrightarrow> s \<in> ?Rf895 invLabel___int pstart end start asida pda)} proof (prove)
goal (3 subgoals):
 1. \<And>invLabel___int pstart end start asida pda. \<lbrakk>flushtype_relation typ invLabel___int; pstart = ps; end = ve; start = vs; asida = asid; pda = pde_Ptr pd\<rbrakk> \<Longrightarrow> ccorres (K (K (\<lambda>_. False)) \<currency> dc \<circ> Inr) (liftxf errstate id (K ()) ret__unsigned_long_') (?Pt895 invLabel___int pstart end start asida pda) (?Rt895 invLabel___int pstart end start asida pda) [SKIP] (do root_switched <- setVMRootForFlush pd asid;
y <- doMachineOp (doFlush typ vs ve ps);
if root_switched then getCurThread >>= setVMRoot else return ()
od) (\<acute>root_switched :== CALL setVMRootForFlush_'proc(pda,asida);;
CALL doFlush_'proc(invLabel___int,start,end,pstart);;
IF \<acute>root_switched \<noteq> 0 THEN
  CALL setVMRoot_'proc(\<acute>ksCurThread)
FI;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))
 2. \<And>invLabel___int pstart end start asida pda. \<lbrakk>flushtype_relation typ invLabel___int; pstart = ps; end = ve; start = vs; asida = asid; pda = pde_Ptr pd\<rbrakk> \<Longrightarrow> ccorres (K (K (\<lambda>_. False)) \<currency> dc \<circ> Inr) (liftxf errstate id (K ()) ret__unsigned_long_') (?Pf895 invLabel___int pstart end start asida pda) (?Rf895 invLabel___int pstart end start asida pda) [SKIP] (return ()) (SKIP;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))
 3. \<And>invLabel___int pstart end start asida pda s s'. \<lbrakk>flushtype_relation typ invLabel___int; pstart = ps; end = ve; start = vs; asida = asid; pda = pde_Ptr pd; (s, s') \<in> rf_sr; (invs' and (\<lambda>y. asid \<le> mask local.asid_bits) and (\<lambda>s. ps \<le> ps + (ve - vs) \<and> vs && mask 5 = ps && mask 5 \<and> unat (ve - vs) \<le> gsMaxObjectSize s)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. vs < ve \<longrightarrow> ?Pt895 invLabel___int pstart end start asida pda s) and (\<lambda>s. \<not> vs < ve \<longrightarrow> ?Pf895 invLabel___int pstart end start asida pda s)) s \<and> s' \<in> {s. (s \<in> \<lbrace>start < end\<rbrace> \<longrightarrow> s \<in> ?Rt895 invLabel___int pstart end start asida pda) \<and> (s \<notin> \<lbrace>start < end\<rbrace> \<longrightarrow> s \<in> ?Rf895 invLabel___int pstart end start asida pda)} proof (prove)
goal (3 subgoals):
 1. \<And>invLabel___int pstart end start asida pda. \<lbrakk>flushtype_relation typ invLabel___int; pstart = ps; end = ve; start = vs; asida = asid; pda = pde_Ptr pd\<rbrakk> \<Longrightarrow> ccorres (K (K (\<lambda>_. False)) \<currency> dc \<circ> Inr) (liftxf errstate id (K ()) ret__unsigned_long_') (?Pt895 invLabel___int pstart end start asida pda) (?Rt895 invLabel___int pstart end start asida pda) [SKIP] (do root_switched <- setVMRootForFlush pd asid;
y <- doMachineOp (doFlush typ vs ve ps);
if root_switched then getCurThread >>= setVMRoot else return ()
od) (\<acute>root_switched :== CALL setVMRootForFlush_'proc(pda,asida);;
(CALL doFlush_'proc(invLabel___int,start,end,pstart);;
(IF \<acute>root_switched \<noteq> 0 THEN
  CALL setVMRoot_'proc(\<acute>ksCurThread)
FI;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))))
 2. \<And>invLabel___int pstart end start asida pda. \<lbrakk>flushtype_relation typ invLabel___int; pstart = ps; end = ve; start = vs; asida = asid; pda = pde_Ptr pd\<rbrakk> \<Longrightarrow> ccorres (K (K (\<lambda>_. False)) \<currency> dc \<circ> Inr) (liftxf errstate id (K ()) ret__unsigned_long_') (?Pf895 invLabel___int pstart end start asida pda) (?Rf895 invLabel___int pstart end start asida pda) [SKIP] (return ()) (SKIP;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))
 3. \<And>invLabel___int pstart end start asida pda s s'. \<lbrakk>flushtype_relation typ invLabel___int; pstart = ps; end = ve; start = vs; asida = asid; pda = pde_Ptr pd; (s, s') \<in> rf_sr; (invs' and (\<lambda>y. asid \<le> mask local.asid_bits) and (\<lambda>s. ps \<le> ps + (ve - vs) \<and> vs && mask 5 = ps && mask 5 \<and> unat (ve - vs) \<le> gsMaxObjectSize s)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. vs < ve \<longrightarrow> ?Pt895 invLabel___int pstart end start asida pda s) and (\<lambda>s. \<not> vs < ve \<longrightarrow> ?Pf895 invLabel___int pstart end start asida pda s)) s \<and> s' \<in> {s. (s \<in> \<lbrace>start < end\<rbrace> \<longrightarrow> s \<in> ?Rt895 invLabel___int pstart end start asida pda) \<and> (s \<notin> \<lbrace>start < end\<rbrace> \<longrightarrow> s \<in> ?Rf895 invLabel___int pstart end start asida pda)} proof (prove)
goal (4 subgoals):
 1. \<And>invLabel___int pstart end start asida pda rv root_switched. \<lbrakk>flushtype_relation typ invLabel___int; pstart = ps; end = ve; start = vs; asida = asid; pda = pde_Ptr pd; root_switched = from_bool rv\<rbrakk> \<Longrightarrow> ccorres (K (K (\<lambda>_. False)) \<currency> dc \<circ> Inr) (liftxf errstate id (K ()) ret__unsigned_long_') (?Q909 invLabel___int pstart end start asida pda rv) (?Q'909 invLabel___int pstart end start asida pda rv root_switched) [SKIP] (do y <- doMachineOp (doFlush typ vs ve ps);
if rv then getCurThread >>= setVMRoot else return ()
od) (CALL doFlush_'proc(invLabel___int,start,end,pstart);;
(IF root_switched \<noteq> 0 THEN
  CALL setVMRoot_'proc(\<acute>ksCurThread)
FI;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE)))
 2. \<And>invLabel___int pstart end start asida pda. \<lbrakk>flushtype_relation typ invLabel___int; pstart = ps; end = ve; start = vs; asida = asid; pda = pde_Ptr pd\<rbrakk> \<Longrightarrow> \<lbrace>?R909 invLabel___int pstart end start asida pda\<rbrace> setVMRootForFlush pd asid \<lbrace>?Q909 invLabel___int pstart end start asida pda\<rbrace>
 3. \<And>invLabel___int pstart end start asida pda. \<lbrakk>flushtype_relation typ invLabel___int; pstart = ps; end = ve; start = vs; asida = asid; pda = pde_Ptr pd\<rbrakk> \<Longrightarrow> ccorres (K (K (\<lambda>_. False)) \<currency> dc \<circ> Inr) (liftxf errstate id (K ()) ret__unsigned_long_') (?Pf895 invLabel___int pstart end start asida pda) (?Rf895 invLabel___int pstart end start asida pda) [SKIP] (return ()) (SKIP;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))
 4. \<And>invLabel___int pstart end start asida pda s s'. \<lbrakk>flushtype_relation typ invLabel___int; pstart = ps; end = ve; start = vs; asida = asid; pda = pde_Ptr pd; (s, s') \<in> rf_sr; (invs' and (\<lambda>y. asid \<le> mask local.asid_bits) and (\<lambda>s. ps \<le> ps + (ve - vs) \<and> vs && mask 5 = ps && mask 5 \<and> unat (ve - vs) \<le> gsMaxObjectSize s)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. vs < ve \<longrightarrow> (invs' and (\<lambda>s. asid \<le> mask local.asid_bits) and ?R909 invLabel___int pstart end start asida pda) s) and (\<lambda>s. \<not> vs < ve \<longrightarrow> ?Pf895 invLabel___int pstart end start asida pda s)) s \<and> s' \<in> {s. (s \<in> \<lbrace>start < end\<rbrace> \<longrightarrow> s \<in> {s. asid_'_update (\<lambda>_. asida) (pd_'_update (\<lambda>_. pda) s) \<in> UNIV \<inter> \<lbrace>\<acute>pd = pde_Ptr pd\<rbrace> \<inter> \<lbrace>\<acute>asid = asid\<rbrace>} \<inter> {s'. \<forall>t rv. ret__unsigned_long_' t = from_bool rv \<longrightarrow> root_switched_'_update (\<lambda>_. ret__unsigned_long_' t) (s'\<lparr>globals := globals t\<rparr>) \<in> ?Q'909 invLabel___int pstart end start asida pda rv (ret__unsigned_long_' t)}) \<and> (s \<notin> \<lbrace>start < end\<rbrace> \<longrightarrow> s \<in> ?Rf895 invLabel___int pstart end start asida pda)} proof (prove)
goal (5 subgoals):
 1. \<And>invLabel___int pstart end start asida pda rv root_switched rva xfdc. \<lbrakk>flushtype_relation typ invLabel___int; pstart = ps; end = ve; start = vs; asida = asid; pda = pde_Ptr pd; root_switched = from_bool rv; dc rva xfdc\<rbrakk> \<Longrightarrow> ccorres (K (K (\<lambda>_. False)) \<currency> dc \<circ> Inr) (liftxf errstate id (K ()) ret__unsigned_long_') (?Q1016 invLabel___int pstart end start asida pda rv root_switched rva) (?Q'1016 invLabel___int pstart end start asida pda rv root_switched rva xfdc) [SKIP] (if rv then getCurThread >>= setVMRoot else return ()) (IF root_switched \<noteq> 0 THEN
  CALL setVMRoot_'proc(\<acute>ksCurThread)
FI;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))
 2. \<And>invLabel___int pstart end start asida pda rv root_switched. \<lbrakk>flushtype_relation typ invLabel___int; pstart = ps; end = ve; start = vs; asida = asid; pda = pde_Ptr pd; root_switched = from_bool rv\<rbrakk> \<Longrightarrow> \<lbrace>?R1018 invLabel___int pstart end start asida pda rv\<rbrace> doMachineOp (doFlush typ vs ve ps) \<lbrace>?Q1016 invLabel___int pstart end start asida pda rv root_switched\<rbrace>
 3. \<And>invLabel___int pstart end start asida pda. \<lbrakk>flushtype_relation typ invLabel___int; pstart = ps; end = ve; start = vs; asida = asid; pda = pde_Ptr pd\<rbrakk> \<Longrightarrow> \<lbrace>?R909 invLabel___int pstart end start asida pda\<rbrace> setVMRootForFlush pd asid \<lbrace>\<lambda>rv. (\<lambda>s. vs \<le> ve \<and> ps \<le> ps + (ve - vs) \<and> vs && mask 5 = ps && mask 5 \<and> unat (ve - vs) \<le> gsMaxObjectSize s) and ?R1018 invLabel___int pstart end start asida pda rv\<rbrace>
 4. \<And>invLabel___int pstart end start asida pda. \<lbrakk>flushtype_relation typ invLabel___int; pstart = ps; end = ve; start = vs; asida = asid; pda = pde_Ptr pd\<rbrakk> \<Longrightarrow> ccorres (K (K (\<lambda>_. False)) \<currency> dc \<circ> Inr) (liftxf errstate id (K ()) ret__unsigned_long_') (?Pf895 invLabel___int pstart end start asida pda) (?Rf895 invLabel___int pstart end start asida pda) [SKIP] (return ()) (SKIP;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))
 5. \<And>invLabel___int pstart end start asida pda s s'. \<lbrakk>flushtype_relation typ invLabel___int; pstart = ps; end = ve; start = vs; asida = asid; pda = pde_Ptr pd; (s, s') \<in> rf_sr; (invs' and (\<lambda>y. asid \<le> mask local.asid_bits) and (\<lambda>s. ps \<le> ps + (ve - vs) \<and> vs && mask 5 = ps && mask 5 \<and> unat (ve - vs) \<le> gsMaxObjectSize s)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. vs < ve \<longrightarrow> (invs' and (\<lambda>s. asid \<le> mask local.asid_bits) and ?R909 invLabel___int pstart end start asida pda) s) and (\<lambda>s. \<not> vs < ve \<longrightarrow> ?Pf895 invLabel___int pstart end start asida pda s)) s \<and> s' \<in> {s. (s \<in> \<lbrace>start < end\<rbrace> \<longrightarrow> s \<in> {s. asid_'_update (\<lambda>_. asida) (pd_'_update (\<lambda>_. pda) s) \<in> UNIV \<inter> \<lbrace>\<acute>pd = pde_Ptr pd\<rbrace> \<inter> \<lbrace>\<acute>asid = asid\<rbrace>} \<inter> {s'. \<forall>t rv. ret__unsigned_long_' t = from_bool rv \<longrightarrow> root_switched_'_update (\<lambda>_. ret__unsigned_long_' t) (s'\<lparr>globals := globals t\<rparr>) \<in> {s. pstart_'_update (\<lambda>_. pstart) (end_'_update (\<lambda>_. end) (start_'_update (\<lambda>_. start) (s\<lparr>invLabel___int_' := invLabel___int\<rparr>))) \<in> \<lbrace>flushtype_relation typ \<acute>invLabel___int\<rbrace> \<inter> \<lbrace>\<acute>start = vs\<rbrace> \<inter> \<lbrace>\<acute>end = ve\<rbrace> \<inter> \<lbrace>\<acute>pstart = ps\<rbrace>} \<inter> {s'. \<forall>ta rva. dc rva (xfdc ta) \<longrightarrow> s'\<lparr>globals := globals ta\<rparr> \<in> ?Q'1016 invLabel___int pstart end start asida pda rv (ret__unsigned_long_' t) rva (xfdc ta)}}) \<and> (s \<notin> \<lbrace>start < end\<rbrace> \<longrightarrow> s \<in> ?Rf895 invLabel___int pstart end start asida pda)} proof (prove)
goal (5 subgoals):
 1. \<And>invLabel___int pstart end start asida pda rv root_switched rva xfdc. \<lbrakk>flushtype_relation typ invLabel___int; pstart = ps; end = ve; start = vs; asida = asid; pda = pde_Ptr pd; root_switched = from_bool rv; dc rva xfdc\<rbrakk> \<Longrightarrow> ccorres (K (K (\<lambda>_. False)) \<currency> dc \<circ> Inr) (liftxf errstate id (K ()) ret__unsigned_long_') (?Q1016 invLabel___int pstart end start asida pda rv root_switched rva) (?Q'1016 invLabel___int pstart end start asida pda rv root_switched rva xfdc) [SKIP] ((if rv then getCurThread >>= setVMRoot else return ()) >>= return) (IF root_switched \<noteq> 0 THEN
  CALL setVMRoot_'proc(\<acute>ksCurThread)
FI;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))
 2. \<And>invLabel___int pstart end start asida pda rv root_switched. \<lbrakk>flushtype_relation typ invLabel___int; pstart = ps; end = ve; start = vs; asida = asid; pda = pde_Ptr pd; root_switched = from_bool rv\<rbrakk> \<Longrightarrow> \<lbrace>?R1018 invLabel___int pstart end start asida pda rv\<rbrace> doMachineOp (doFlush typ vs ve ps) \<lbrace>?Q1016 invLabel___int pstart end start asida pda rv root_switched\<rbrace>
 3. \<And>invLabel___int pstart end start asida pda. \<lbrakk>flushtype_relation typ invLabel___int; pstart = ps; end = ve; start = vs; asida = asid; pda = pde_Ptr pd\<rbrakk> \<Longrightarrow> \<lbrace>?R909 invLabel___int pstart end start asida pda\<rbrace> setVMRootForFlush pd asid \<lbrace>\<lambda>rv. (\<lambda>s. vs \<le> ve \<and> ps \<le> ps + (ve - vs) \<and> vs && mask 5 = ps && mask 5 \<and> unat (ve - vs) \<le> gsMaxObjectSize s) and ?R1018 invLabel___int pstart end start asida pda rv\<rbrace>
 4. \<And>invLabel___int pstart end start asida pda. \<lbrakk>flushtype_relation typ invLabel___int; pstart = ps; end = ve; start = vs; asida = asid; pda = pde_Ptr pd\<rbrakk> \<Longrightarrow> ccorres (K (K (\<lambda>_. False)) \<currency> dc \<circ> Inr) (liftxf errstate id (K ()) ret__unsigned_long_') (?Pf895 invLabel___int pstart end start asida pda) (?Rf895 invLabel___int pstart end start asida pda) [SKIP] (return ()) (SKIP;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))
 5. \<And>invLabel___int pstart end start asida pda s s'. \<lbrakk>flushtype_relation typ invLabel___int; pstart = ps; end = ve; start = vs; asida = asid; pda = pde_Ptr pd; (s, s') \<in> rf_sr; (invs' and (\<lambda>y. asid \<le> mask local.asid_bits) and (\<lambda>s. ps \<le> ps + (ve - vs) \<and> vs && mask 5 = ps && mask 5 \<and> unat (ve - vs) \<le> gsMaxObjectSize s)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. vs < ve \<longrightarrow> (invs' and (\<lambda>s. asid \<le> mask local.asid_bits) and ?R909 invLabel___int pstart end start asida pda) s) and (\<lambda>s. \<not> vs < ve \<longrightarrow> ?Pf895 invLabel___int pstart end start asida pda s)) s \<and> s' \<in> {s. (s \<in> \<lbrace>start < end\<rbrace> \<longrightarrow> s \<in> {s. asid_'_update (\<lambda>_. asida) (pd_'_update (\<lambda>_. pda) s) \<in> UNIV \<inter> \<lbrace>\<acute>pd = pde_Ptr pd\<rbrace> \<inter> \<lbrace>\<acute>asid = asid\<rbrace>} \<inter> {s'. \<forall>t rv. ret__unsigned_long_' t = from_bool rv \<longrightarrow> root_switched_'_update (\<lambda>_. ret__unsigned_long_' t) (s'\<lparr>globals := globals t\<rparr>) \<in> {s. pstart_'_update (\<lambda>_. pstart) (end_'_update (\<lambda>_. end) (start_'_update (\<lambda>_. start) (s\<lparr>invLabel___int_' := invLabel___int\<rparr>))) \<in> \<lbrace>flushtype_relation typ \<acute>invLabel___int\<rbrace> \<inter> \<lbrace>\<acute>start = vs\<rbrace> \<inter> \<lbrace>\<acute>end = ve\<rbrace> \<inter> \<lbrace>\<acute>pstart = ps\<rbrace>} \<inter> {s'. \<forall>ta rva. dc rva (xfdc ta) \<longrightarrow> s'\<lparr>globals := globals ta\<rparr> \<in> ?Q'1016 invLabel___int pstart end start asida pda rv (ret__unsigned_long_' t) rva (xfdc ta)}}) \<and> (s \<notin> \<lbrace>start < end\<rbrace> \<longrightarrow> s \<in> ?Rf895 invLabel___int pstart end start asida pda)} proof (prove)
goal (8 subgoals):
 1. \<And>invLabel___int pstart end start asida pda rv root_switched rva xfdca. \<lbrakk>flushtype_relation typ invLabel___int; pstart = ps; end = ve; start = vs; asida = asid; pda = pde_Ptr pd; root_switched = from_bool rv; dc rva xfdca\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?P1058 invLabel___int pstart end start asida pda rv root_switched rva) (?Q'1016 invLabel___int pstart end start asida pda rv root_switched rva xfdca) [] (if rv then getCurThread >>= setVMRoot else return ()) (IF root_switched \<noteq> 0 THEN
  CALL setVMRoot_'proc(\<acute>ksCurThread)
FI)
 2. \<And>invLabel___int pstart end start asida pda rv root_switched rva xfdc x rv'. \<lbrakk>flushtype_relation typ invLabel___int; pstart = ps; end = ve; start = vs; asida = asid; pda = pde_Ptr pd; root_switched = from_bool rv; dc rva xfdc; dc x rv'\<rbrakk> \<Longrightarrow> ccorres (K (K (\<lambda>_. False)) \<currency> dc \<circ> Inr) (liftxf errstate id (K ()) ret__unsigned_long_') (?Q1057 invLabel___int pstart end start asida pda rv root_switched rva xfdc x) (?Q'1057 invLabel___int pstart end start asida pda rv root_switched rva xfdc x rv') [SKIP] (return x) (return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))
 3. \<And>invLabel___int pstart end start asida pda rv root_switched rva xfdc. \<lbrakk>flushtype_relation typ invLabel___int; pstart = ps; end = ve; start = vs; asida = asid; pda = pde_Ptr pd; root_switched = from_bool rv; dc rva xfdc\<rbrakk> \<Longrightarrow> \<lbrace>?R1059 invLabel___int pstart end start asida pda rv root_switched rva\<rbrace> if rv then getCurThread >>= setVMRoot else return () \<lbrace>?Q1057 invLabel___int pstart end start asida pda rv root_switched rva xfdc\<rbrace>
 4. \<And>invLabel___int pstart end start asida pda rv root_switched rva xfdca. \<lbrakk>flushtype_relation typ invLabel___int; pstart = ps; end = ve; start = vs; asida = asid; pda = pde_Ptr pd; root_switched = from_bool rv; dc rva xfdca\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (?Q'1057 invLabel___int pstart end start asida pda rv root_switched rva xfdca)
 5. \<And>invLabel___int pstart end start asida pda rv root_switched. \<lbrakk>flushtype_relation typ invLabel___int; pstart = ps; end = ve; start = vs; asida = asid; pda = pde_Ptr pd; root_switched = from_bool rv\<rbrakk> \<Longrightarrow> \<lbrace>?R1018 invLabel___int pstart end start asida pda rv\<rbrace> doMachineOp (doFlush typ vs ve ps) \<lbrace>\<lambda>rva. ?P1058 invLabel___int pstart end start asida pda rv root_switched rva and ?R1059 invLabel___int pstart end start asida pda rv root_switched rva\<rbrace>
 6. \<And>invLabel___int pstart end start asida pda. \<lbrakk>flushtype_relation typ invLabel___int; pstart = ps; end = ve; start = vs; asida = asid; pda = pde_Ptr pd\<rbrakk> \<Longrightarrow> \<lbrace>?R909 invLabel___int pstart end start asida pda\<rbrace> setVMRootForFlush pd asid \<lbrace>\<lambda>rv. (\<lambda>s. vs \<le> ve \<and> ps \<le> ps + (ve - vs) \<and> vs && mask 5 = ps && mask 5 \<and> unat (ve - vs) \<le> gsMaxObjectSize s) and ?R1018 invLabel___int pstart end start asida pda rv\<rbrace>
 7. \<And>invLabel___int pstart end start asida pda. \<lbrakk>flushtype_relation typ invLabel___int; pstart = ps; end = ve; start = vs; asida = asid; pda = pde_Ptr pd\<rbrakk> \<Longrightarrow> ccorres (K (K (\<lambda>_. False)) \<currency> dc \<circ> Inr) (liftxf errstate id (K ()) ret__unsigned_long_') (?Pf895 invLabel___int pstart end start asida pda) (?Rf895 invLabel___int pstart end start asida pda) [SKIP] (return ()) (SKIP;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))
 8. \<And>invLabel___int pstart end start asida pda s s'. \<lbrakk>flushtype_relation typ invLabel___int; pstart = ps; end = ve; start = vs; asida = asid; pda = pde_Ptr pd; (s, s') \<in> rf_sr; (invs' and (\<lambda>y. asid \<le> mask local.asid_bits) and (\<lambda>s. ps \<le> ps + (ve - vs) \<and> vs && mask 5 = ps && mask 5 \<and> unat (ve - vs) \<le> gsMaxObjectSize s)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. vs < ve \<longrightarrow> (invs' and (\<lambda>s. asid \<le> mask local.asid_bits) and ?R909 invLabel___int pstart end start asida pda) s) and (\<lambda>s. \<not> vs < ve \<longrightarrow> ?Pf895 invLabel___int pstart end start asida pda s)) s \<and> s' \<in> {s. (s \<in> \<lbrace>start < end\<rbrace> \<longrightarrow> s \<in> {s. asid_'_update (\<lambda>_. asida) (pd_'_update (\<lambda>_. pda) s) \<in> UNIV \<inter> \<lbrace>\<acute>pd = pde_Ptr pd\<rbrace> \<inter> \<lbrace>\<acute>asid = asid\<rbrace>} \<inter> {s'. \<forall>t rv. ret__unsigned_long_' t = from_bool rv \<longrightarrow> root_switched_'_update (\<lambda>_. ret__unsigned_long_' t) (s'\<lparr>globals := globals t\<rparr>) \<in> {s. pstart_'_update (\<lambda>_. pstart) (end_'_update (\<lambda>_. end) (start_'_update (\<lambda>_. start) (s\<lparr>invLabel___int_' := invLabel___int\<rparr>))) \<in> \<lbrace>flushtype_relation typ \<acute>invLabel___int\<rbrace> \<inter> \<lbrace>\<acute>start = vs\<rbrace> \<inter> \<lbrace>\<acute>end = ve\<rbrace> \<inter> \<lbrace>\<acute>pstart = ps\<rbrace>} \<inter> {s'. \<forall>ta rva. dc rva (xfdc ta) \<longrightarrow> s'\<lparr>globals := globals ta\<rparr> \<in> ?Q'1016 invLabel___int pstart end start asida pda rv (ret__unsigned_long_' t) rva (xfdc ta)}}) \<and> (s \<notin> \<lbrace>start < end\<rbrace> \<longrightarrow> s \<in> ?Rf895 invLabel___int pstart end start asida pda)} proof (prove)
goal (10 subgoals):
 1. \<And>invLabel___int pstart end start asida pda rv root_switched rva xfdc. \<lbrakk>flushtype_relation typ invLabel___int; pstart = ps; end = ve; start = vs; asida = asid; pda = pde_Ptr pd; root_switched = from_bool rv; dc rva xfdc\<rbrakk> \<Longrightarrow> \<forall>s s'. (s, s') \<in> rf_sr \<and> True \<longrightarrow> rv = (s' \<in> \<lbrace>root_switched \<noteq> 0\<rbrace>)
 2. \<And>invLabel___int pstart end start asida pda rv root_switched rva xfdca. \<lbrakk>flushtype_relation typ invLabel___int; pstart = ps; end = ve; start = vs; asida = asid; pda = pde_Ptr pd; root_switched = from_bool rv; dc rva xfdca\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Pt1066 invLabel___int pstart end start asida pda rv root_switched rva) (?Rt1064 invLabel___int pstart end start asida pda rv root_switched rva xfdca) [] (getCurThread >>= setVMRoot) (CALL setVMRoot_'proc(\<acute>ksCurThread))
 3. \<And>invLabel___int pstart end start asida pda rv root_switched rva xfdca. \<lbrakk>flushtype_relation typ invLabel___int; pstart = ps; end = ve; start = vs; asida = asid; pda = pde_Ptr pd; root_switched = from_bool rv; dc rva xfdca\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Pf1068 invLabel___int pstart end start asida pda rv root_switched rva) (?Rf1064 invLabel___int pstart end start asida pda rv root_switched rva xfdca) [] (return ()) SKIP
 4. \<And>invLabel___int pstart end start asida pda rv root_switched rva xfdc x rv'. \<lbrakk>flushtype_relation typ invLabel___int; pstart = ps; end = ve; start = vs; asida = asid; pda = pde_Ptr pd; root_switched = from_bool rv; dc rva xfdc; dc x rv'\<rbrakk> \<Longrightarrow> ccorres (K (K (\<lambda>_. False)) \<currency> dc \<circ> Inr) (liftxf errstate id (K ()) ret__unsigned_long_') (?Q1057 invLabel___int pstart end start asida pda rv root_switched rva xfdc x) (?Q'1057 invLabel___int pstart end start asida pda rv root_switched rva xfdc x rv') [SKIP] (return x) (return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))
 5. \<And>invLabel___int pstart end start asida pda rv root_switched rva xfdc. \<lbrakk>flushtype_relation typ invLabel___int; pstart = ps; end = ve; start = vs; asida = asid; pda = pde_Ptr pd; root_switched = from_bool rv; dc rva xfdc\<rbrakk> \<Longrightarrow> \<lbrace>?R1059 invLabel___int pstart end start asida pda rv root_switched rva\<rbrace> if rv then getCurThread >>= setVMRoot else return () \<lbrace>?Q1057 invLabel___int pstart end start asida pda rv root_switched rva xfdc\<rbrace>
 6. \<And>invLabel___int pstart end start asida pda rv root_switched rva xfdca. \<lbrakk>flushtype_relation typ invLabel___int; pstart = ps; end = ve; start = vs; asida = asid; pda = pde_Ptr pd; root_switched = from_bool rv; dc rva xfdca\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (?Q'1057 invLabel___int pstart end start asida pda rv root_switched rva xfdca)
 7. \<And>invLabel___int pstart end start asida pda rv root_switched. \<lbrakk>flushtype_relation typ invLabel___int; pstart = ps; end = ve; start = vs; asida = asid; pda = pde_Ptr pd; root_switched = from_bool rv\<rbrakk> \<Longrightarrow> \<lbrace>?R1018 invLabel___int pstart end start asida pda rv\<rbrace> doMachineOp (doFlush typ vs ve ps) \<lbrace>\<lambda>rva. (\<lambda>_. True) and (\<lambda>s. rv \<longrightarrow> ?Pt1066 invLabel___int pstart end start asida pda rv root_switched rva s) and (\<lambda>s. \<not> rv \<longrightarrow> ?Pf1068 invLabel___int pstart end start asida pda rv root_switched rva s) and ?R1059 invLabel___int pstart end start asida pda rv root_switched rva\<rbrace>
 8. \<And>invLabel___int pstart end start asida pda. \<lbrakk>flushtype_relation typ invLabel___int; pstart = ps; end = ve; start = vs; asida = asid; pda = pde_Ptr pd\<rbrakk> \<Longrightarrow> \<lbrace>?R909 invLabel___int pstart end start asida pda\<rbrace> setVMRootForFlush pd asid \<lbrace>\<lambda>rv. (\<lambda>s. vs \<le> ve \<and> ps \<le> ps + (ve - vs) \<and> vs && mask 5 = ps && mask 5 \<and> unat (ve - vs) \<le> gsMaxObjectSize s) and ?R1018 invLabel___int pstart end start asida pda rv\<rbrace>
 9. \<And>invLabel___int pstart end start asida pda. \<lbrakk>flushtype_relation typ invLabel___int; pstart = ps; end = ve; start = vs; asida = asid; pda = pde_Ptr pd\<rbrakk> \<Longrightarrow> ccorres (K (K (\<lambda>_. False)) \<currency> dc \<circ> Inr) (liftxf errstate id (K ()) ret__unsigned_long_') (?Pf895 invLabel___int pstart end start asida pda) (?Rf895 invLabel___int pstart end start asida pda) [SKIP] (return ()) (SKIP;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))
 10. \<And>invLabel___int pstart end start asida pda s s'. \<lbrakk>flushtype_relation typ invLabel___int; pstart = ps; end = ve; start = vs; asida = asid; pda = pde_Ptr pd; (s, s') \<in> rf_sr; (invs' and (\<lambda>y. asid \<le> mask local.asid_bits) and (\<lambda>s. ps \<le> ps + (ve - vs) \<and> vs && mask 5 = ps && mask 5 \<and> unat (ve - vs) \<le> gsMaxObjectSize s)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. vs < ve \<longrightarrow> (invs' and (\<lambda>s. asid \<le> mask local.asid_bits) and ?R909 invLabel___int pstart end start asida pda) s) and (\<lambda>s. \<not> vs < ve \<longrightarrow> ?Pf895 invLabel___int pstart end start asida pda s)) s \<and> s' \<in> {s. (s \<in> \<lbrace>start < end\<rbrace> \<longrightarrow> s \<in> {s. asid_'_update (\<lambda>_. asida) (pd_'_update (\<lambda>_. pda) s) \<in> UNIV \<inter> \<lbrace>\<acute>pd = pde_Ptr pd\<rbrace> \<inter> \<lbrace>\<acute>asid = asid\<rbrace>} \<inter> {s'. \<forall>t rv. ret__unsigned_long_' t = from_bool rv \<longrightarrow> root_switched_'_update (\<lambda>_. ret__unsigned_long_' t) (s'\<lparr>globals := globals t\<rparr>) \<in> {s. pstart_'_update (\<lambda>_. pstart) (end_'_update (\<lambda>_. end) (start_'_update (\<lambda>_. start) (s\<lparr>invLabel___int_' := invLabel___int\<rparr>))) \<in> \<lbrace>flushtype_relation typ \<acute>invLabel___int\<rbrace> \<inter> \<lbrace>\<acute>start = vs\<rbrace> \<inter> \<lbrace>\<acute>end = ve\<rbrace> \<inter> \<lbrace>\<acute>pstart = ps\<rbrace>} \<inter> {s'. \<forall>ta rva. dc rva (xfdc ta) \<longrightarrow> s'\<lparr>globals := globals ta\<rparr> \<in> {s. (s \<in> \<lbrace>\<^bsup>t\<^esup>ret__unsigned_long \<noteq> 0\<rbrace> \<longrightarrow> s \<in> ?Rt1064 invLabel___int pstart end start asida pda rv (ret__unsigned_long_' t) rva (xfdc ta)) \<and> (s \<notin> \<lbrace>\<^bsup>t\<^esup>ret__unsigned_long \<noteq> 0\<rbrace> \<longrightarrow> s \<in> ?Rf1064 invLabel___int pstart end start asida pda rv (ret__unsigned_long_' t) rva (xfdc ta))}}}) \<and> (s \<notin> \<lbrace>start < end\<rbrace> \<longrightarrow> s \<in> ?Rf895 invLabel___int pstart end start asida pda)} proof (prove)
goal (9 subgoals):
 1. \<And>invLabel___int pstart end start asida pda rv root_switched rva xfdca. \<lbrakk>flushtype_relation typ invLabel___int; pstart = ps; end = ve; start = vs; asida = asid; pda = pde_Ptr pd; root_switched = from_bool rv; dc rva xfdca\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Pt1066 invLabel___int pstart end start asida pda rv root_switched rva) (?Rt1064 invLabel___int pstart end start asida pda rv root_switched rva xfdca) [] (getCurThread >>= setVMRoot) (CALL setVMRoot_'proc(\<acute>ksCurThread))
 2. \<And>invLabel___int pstart end start asida pda rv root_switched rva xfdca. \<lbrakk>flushtype_relation typ invLabel___int; pstart = ps; end = ve; start = vs; asida = asid; pda = pde_Ptr pd; root_switched = from_bool rv; dc rva xfdca\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Pf1068 invLabel___int pstart end start asida pda rv root_switched rva) (?Rf1064 invLabel___int pstart end start asida pda rv root_switched rva xfdca) [] (return ()) SKIP
 3. \<And>invLabel___int pstart end start asida pda rv root_switched rva xfdc x rv'. \<lbrakk>flushtype_relation typ invLabel___int; pstart = ps; end = ve; start = vs; asida = asid; pda = pde_Ptr pd; root_switched = from_bool rv; dc rva xfdc; dc x rv'\<rbrakk> \<Longrightarrow> ccorres (K (K (\<lambda>_. False)) \<currency> dc \<circ> Inr) (liftxf errstate id (K ()) ret__unsigned_long_') (?Q1057 invLabel___int pstart end start asida pda rv root_switched rva xfdc x) (?Q'1057 invLabel___int pstart end start asida pda rv root_switched rva xfdc x rv') [SKIP] (return x) (return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))
 4. \<And>invLabel___int pstart end start asida pda rv root_switched rva xfdc. \<lbrakk>flushtype_relation typ invLabel___int; pstart = ps; end = ve; start = vs; asida = asid; pda = pde_Ptr pd; root_switched = from_bool rv; dc rva xfdc\<rbrakk> \<Longrightarrow> \<lbrace>?R1059 invLabel___int pstart end start asida pda rv root_switched rva\<rbrace> if rv then getCurThread >>= setVMRoot else return () \<lbrace>?Q1057 invLabel___int pstart end start asida pda rv root_switched rva xfdc\<rbrace>
 5. \<And>invLabel___int pstart end start asida pda rv root_switched rva xfdca. \<lbrakk>flushtype_relation typ invLabel___int; pstart = ps; end = ve; start = vs; asida = asid; pda = pde_Ptr pd; root_switched = from_bool rv; dc rva xfdca\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (?Q'1057 invLabel___int pstart end start asida pda rv root_switched rva xfdca)
 6. \<And>invLabel___int pstart end start asida pda rv root_switched. \<lbrakk>flushtype_relation typ invLabel___int; pstart = ps; end = ve; start = vs; asida = asid; pda = pde_Ptr pd; root_switched = from_bool rv\<rbrakk> \<Longrightarrow> \<lbrace>?R1018 invLabel___int pstart end start asida pda rv\<rbrace> doMachineOp (doFlush typ vs ve ps) \<lbrace>\<lambda>rva. (\<lambda>_. True) and (\<lambda>s. rv \<longrightarrow> ?Pt1066 invLabel___int pstart end start asida pda rv root_switched rva s) and (\<lambda>s. \<not> rv \<longrightarrow> ?Pf1068 invLabel___int pstart end start asida pda rv root_switched rva s) and ?R1059 invLabel___int pstart end start asida pda rv root_switched rva\<rbrace>
 7. \<And>invLabel___int pstart end start asida pda. \<lbrakk>flushtype_relation typ invLabel___int; pstart = ps; end = ve; start = vs; asida = asid; pda = pde_Ptr pd\<rbrakk> \<Longrightarrow> \<lbrace>?R909 invLabel___int pstart end start asida pda\<rbrace> setVMRootForFlush pd asid \<lbrace>\<lambda>rv. (\<lambda>s. vs \<le> ve \<and> ps \<le> ps + (ve - vs) \<and> vs && mask 5 = ps && mask 5 \<and> unat (ve - vs) \<le> gsMaxObjectSize s) and ?R1018 invLabel___int pstart end start asida pda rv\<rbrace>
 8. \<And>invLabel___int pstart end start asida pda. \<lbrakk>flushtype_relation typ invLabel___int; pstart = ps; end = ve; start = vs; asida = asid; pda = pde_Ptr pd\<rbrakk> \<Longrightarrow> ccorres (K (K (\<lambda>_. False)) \<currency> dc \<circ> Inr) (liftxf errstate id (K ()) ret__unsigned_long_') (?Pf895 invLabel___int pstart end start asida pda) (?Rf895 invLabel___int pstart end start asida pda) [SKIP] (return ()) (SKIP;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))
 9. \<And>invLabel___int pstart end start asida pda s s'. \<lbrakk>flushtype_relation typ invLabel___int; pstart = ps; end = ve; start = vs; asida = asid; pda = pde_Ptr pd; (s, s') \<in> rf_sr; (invs' and (\<lambda>y. asid \<le> mask local.asid_bits) and (\<lambda>s. ps \<le> ps + (ve - vs) \<and> vs && mask 5 = ps && mask 5 \<and> unat (ve - vs) \<le> gsMaxObjectSize s)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. vs < ve \<longrightarrow> (invs' and (\<lambda>s. asid \<le> mask local.asid_bits) and ?R909 invLabel___int pstart end start asida pda) s) and (\<lambda>s. \<not> vs < ve \<longrightarrow> ?Pf895 invLabel___int pstart end start asida pda s)) s \<and> s' \<in> {s. (s \<in> \<lbrace>start < end\<rbrace> \<longrightarrow> s \<in> {s. asid_'_update (\<lambda>_. asida) (pd_'_update (\<lambda>_. pda) s) \<in> UNIV \<inter> \<lbrace>\<acute>pd = pde_Ptr pd\<rbrace> \<inter> \<lbrace>\<acute>asid = asid\<rbrace>} \<inter> {s'. \<forall>t rv. ret__unsigned_long_' t = from_bool rv \<longrightarrow> root_switched_'_update (\<lambda>_. ret__unsigned_long_' t) (s'\<lparr>globals := globals t\<rparr>) \<in> {s. pstart_'_update (\<lambda>_. pstart) (end_'_update (\<lambda>_. end) (start_'_update (\<lambda>_. start) (s\<lparr>invLabel___int_' := invLabel___int\<rparr>))) \<in> \<lbrace>flushtype_relation typ \<acute>invLabel___int\<rbrace> \<inter> \<lbrace>\<acute>start = vs\<rbrace> \<inter> \<lbrace>\<acute>end = ve\<rbrace> \<inter> \<lbrace>\<acute>pstart = ps\<rbrace>} \<inter> {s'. \<forall>ta rva. dc rva (xfdc ta) \<longrightarrow> s'\<lparr>globals := globals ta\<rparr> \<in> {s. (s \<in> \<lbrace>\<^bsup>t\<^esup>ret__unsigned_long \<noteq> 0\<rbrace> \<longrightarrow> s \<in> ?Rt1064 invLabel___int pstart end start asida pda rv (ret__unsigned_long_' t) rva (xfdc ta)) \<and> (s \<notin> \<lbrace>\<^bsup>t\<^esup>ret__unsigned_long \<noteq> 0\<rbrace> \<longrightarrow> s \<in> ?Rf1064 invLabel___int pstart end start asida pda rv (ret__unsigned_long_' t) rva (xfdc ta))}}}) \<and> (s \<notin> \<lbrace>start < end\<rbrace> \<longrightarrow> s \<in> ?Rf895 invLabel___int pstart end start asida pda)} proof (prove)
goal (9 subgoals):
 1. \<And>invLabel___int pstart end start asida pda rv root_switched rva xfdca rvb. \<lbrakk>flushtype_relation typ invLabel___int; pstart = ps; end = ve; start = vs; asida = asid; pda = pde_Ptr pd; root_switched = from_bool rv; dc rva xfdca\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?P1077 invLabel___int pstart end start asida pda rv root_switched rva rvb) (?P'1076 invLabel___int pstart end start asida pda rv root_switched rva xfdca rvb) [] (setVMRoot rvb) (CALL setVMRoot_'proc(\<acute>ksCurThread))
 2. \<And>invLabel___int pstart end start asida pda rv root_switched rva xfdca. \<lbrakk>flushtype_relation typ invLabel___int; pstart = ps; end = ve; start = vs; asida = asid; pda = pde_Ptr pd; root_switched = from_bool rv; dc rva xfdca\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Pf1068 invLabel___int pstart end start asida pda rv root_switched rva) (?Rf1064 invLabel___int pstart end start asida pda rv root_switched rva xfdca) [] (return ()) SKIP
 3. \<And>invLabel___int pstart end start asida pda rv root_switched rva xfdc x rv'. \<lbrakk>flushtype_relation typ invLabel___int; pstart = ps; end = ve; start = vs; asida = asid; pda = pde_Ptr pd; root_switched = from_bool rv; dc rva xfdc; dc x rv'\<rbrakk> \<Longrightarrow> ccorres (K (K (\<lambda>_. False)) \<currency> dc \<circ> Inr) (liftxf errstate id (K ()) ret__unsigned_long_') (?Q1057 invLabel___int pstart end start asida pda rv root_switched rva xfdc x) (?Q'1057 invLabel___int pstart end start asida pda rv root_switched rva xfdc x rv') [SKIP] (return x) (return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))
 4. \<And>invLabel___int pstart end start asida pda rv root_switched rva xfdc. \<lbrakk>flushtype_relation typ invLabel___int; pstart = ps; end = ve; start = vs; asida = asid; pda = pde_Ptr pd; root_switched = from_bool rv; dc rva xfdc\<rbrakk> \<Longrightarrow> \<lbrace>?R1059 invLabel___int pstart end start asida pda rv root_switched rva\<rbrace> if rv then getCurThread >>= setVMRoot else return () \<lbrace>?Q1057 invLabel___int pstart end start asida pda rv root_switched rva xfdc\<rbrace>
 5. \<And>invLabel___int pstart end start asida pda rv root_switched rva xfdca. \<lbrakk>flushtype_relation typ invLabel___int; pstart = ps; end = ve; start = vs; asida = asid; pda = pde_Ptr pd; root_switched = from_bool rv; dc rva xfdca\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (?Q'1057 invLabel___int pstart end start asida pda rv root_switched rva xfdca)
 6. \<And>invLabel___int pstart end start asida pda rv root_switched. \<lbrakk>flushtype_relation typ invLabel___int; pstart = ps; end = ve; start = vs; asida = asid; pda = pde_Ptr pd; root_switched = from_bool rv\<rbrakk> \<Longrightarrow> \<lbrace>?R1018 invLabel___int pstart end start asida pda rv\<rbrace> doMachineOp (doFlush typ vs ve ps) \<lbrace>\<lambda>rva. (\<lambda>_. True) and (\<lambda>s. rv \<longrightarrow> (\<forall>rvb. ksCurThread s = rvb \<longrightarrow> ?P1077 invLabel___int pstart end start asida pda rv root_switched rva rvb s)) and (\<lambda>s. \<not> rv \<longrightarrow> ?Pf1068 invLabel___int pstart end start asida pda rv root_switched rva s) and ?R1059 invLabel___int pstart end start asida pda rv root_switched rva\<rbrace>
 7. \<And>invLabel___int pstart end start asida pda. \<lbrakk>flushtype_relation typ invLabel___int; pstart = ps; end = ve; start = vs; asida = asid; pda = pde_Ptr pd\<rbrakk> \<Longrightarrow> \<lbrace>?R909 invLabel___int pstart end start asida pda\<rbrace> setVMRootForFlush pd asid \<lbrace>\<lambda>rv. (\<lambda>s. vs \<le> ve \<and> ps \<le> ps + (ve - vs) \<and> vs && mask 5 = ps && mask 5 \<and> unat (ve - vs) \<le> gsMaxObjectSize s) and ?R1018 invLabel___int pstart end start asida pda rv\<rbrace>
 8. \<And>invLabel___int pstart end start asida pda. \<lbrakk>flushtype_relation typ invLabel___int; pstart = ps; end = ve; start = vs; asida = asid; pda = pde_Ptr pd\<rbrakk> \<Longrightarrow> ccorres (K (K (\<lambda>_. False)) \<currency> dc \<circ> Inr) (liftxf errstate id (K ()) ret__unsigned_long_') (?Pf895 invLabel___int pstart end start asida pda) (?Rf895 invLabel___int pstart end start asida pda) [SKIP] (return ()) (SKIP;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))
 9. \<And>invLabel___int pstart end start asida pda s s'. \<lbrakk>flushtype_relation typ invLabel___int; pstart = ps; end = ve; start = vs; asida = asid; pda = pde_Ptr pd; (s, s') \<in> rf_sr; (invs' and (\<lambda>y. asid \<le> mask local.asid_bits) and (\<lambda>s. ps \<le> ps + (ve - vs) \<and> vs && mask 5 = ps && mask 5 \<and> unat (ve - vs) \<le> gsMaxObjectSize s)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. vs < ve \<longrightarrow> (invs' and (\<lambda>s. asid \<le> mask local.asid_bits) and ?R909 invLabel___int pstart end start asida pda) s) and (\<lambda>s. \<not> vs < ve \<longrightarrow> ?Pf895 invLabel___int pstart end start asida pda s)) s \<and> s' \<in> {s. (s \<in> \<lbrace>start < end\<rbrace> \<longrightarrow> s \<in> {s. asid_'_update (\<lambda>_. asida) (pd_'_update (\<lambda>_. pda) s) \<in> UNIV \<inter> \<lbrace>\<acute>pd = pde_Ptr pd\<rbrace> \<inter> \<lbrace>\<acute>asid = asid\<rbrace>} \<inter> {s'. \<forall>t rv. ret__unsigned_long_' t = from_bool rv \<longrightarrow> root_switched_'_update (\<lambda>_. ret__unsigned_long_' t) (s'\<lparr>globals := globals t\<rparr>) \<in> {s. pstart_'_update (\<lambda>_. pstart) (end_'_update (\<lambda>_. end) (start_'_update (\<lambda>_. start) (s\<lparr>invLabel___int_' := invLabel___int\<rparr>))) \<in> \<lbrace>flushtype_relation typ \<acute>invLabel___int\<rbrace> \<inter> \<lbrace>\<acute>start = vs\<rbrace> \<inter> \<lbrace>\<acute>end = ve\<rbrace> \<inter> \<lbrace>\<acute>pstart = ps\<rbrace>} \<inter> {s'. \<forall>ta rva. dc rva (xfdc ta) \<longrightarrow> s'\<lparr>globals := globals ta\<rparr> \<in> {s. (s \<in> \<lbrace>\<^bsup>t\<^esup>ret__unsigned_long \<noteq> 0\<rbrace> \<longrightarrow> s \<in> {s. \<forall>rvb. ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr rvb \<longrightarrow> s \<in> ?P'1076 invLabel___int pstart end start asida pda rv (ret__unsigned_long_' t) rva (xfdc ta) rvb}) \<and> (s \<notin> \<lbrace>\<^bsup>t\<^esup>ret__unsigned_long \<noteq> 0\<rbrace> \<longrightarrow> s \<in> ?Rf1064 invLabel___int pstart end start asida pda rv (ret__unsigned_long_' t) rva (xfdc ta))}}}) \<and> (s \<notin> \<lbrace>start < end\<rbrace> \<longrightarrow> s \<in> ?Rf895 invLabel___int pstart end start asida pda)} proof (prove)
goal (8 subgoals):
 1. \<And>invLabel___int pstart end start asida pda rv root_switched rva xfdca. \<lbrakk>flushtype_relation typ invLabel___int; pstart = ps; end = ve; start = vs; asida = asid; pda = pde_Ptr pd; root_switched = from_bool rv; dc rva xfdca\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Pf1068 invLabel___int pstart end start asida pda rv root_switched rva) (?Rf1064 invLabel___int pstart end start asida pda rv root_switched rva xfdca) [] (return ()) SKIP
 2. \<And>invLabel___int pstart end start asida pda rv root_switched rva xfdc x rv'. \<lbrakk>flushtype_relation typ invLabel___int; pstart = ps; end = ve; start = vs; asida = asid; pda = pde_Ptr pd; root_switched = from_bool rv; dc rva xfdc; dc x rv'\<rbrakk> \<Longrightarrow> ccorres (K (K (\<lambda>_. False)) \<currency> dc \<circ> Inr) (liftxf errstate id (K ()) ret__unsigned_long_') (?Q1057 invLabel___int pstart end start asida pda rv root_switched rva xfdc x) (?Q'1057 invLabel___int pstart end start asida pda rv root_switched rva xfdc x rv') [SKIP] (return x) (return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))
 3. \<And>invLabel___int pstart end start asida pda rv root_switched rva xfdc. \<lbrakk>flushtype_relation typ invLabel___int; pstart = ps; end = ve; start = vs; asida = asid; pda = pde_Ptr pd; root_switched = from_bool rv; dc rva xfdc\<rbrakk> \<Longrightarrow> \<lbrace>?R1059 invLabel___int pstart end start asida pda rv root_switched rva\<rbrace> if rv then getCurThread >>= setVMRoot else return () \<lbrace>?Q1057 invLabel___int pstart end start asida pda rv root_switched rva xfdc\<rbrace>
 4. \<And>invLabel___int pstart end start asida pda rv root_switched rva xfdca. \<lbrakk>flushtype_relation typ invLabel___int; pstart = ps; end = ve; start = vs; asida = asid; pda = pde_Ptr pd; root_switched = from_bool rv; dc rva xfdca\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (?Q'1057 invLabel___int pstart end start asida pda rv root_switched rva xfdca)
 5. \<And>invLabel___int pstart end start asida pda rv root_switched. \<lbrakk>flushtype_relation typ invLabel___int; pstart = ps; end = ve; start = vs; asida = asid; pda = pde_Ptr pd; root_switched = from_bool rv\<rbrakk> \<Longrightarrow> \<lbrace>?R1018 invLabel___int pstart end start asida pda rv\<rbrace> doMachineOp (doFlush typ vs ve ps) \<lbrace>\<lambda>rva. (\<lambda>_. True) and (\<lambda>s. rv \<longrightarrow> (\<forall>rv. ksCurThread s = rv \<longrightarrow> (all_invs_but_ct_idle_or_in_cur_domain' and tcb_at' rv) s)) and (\<lambda>s. \<not> rv \<longrightarrow> ?Pf1068 invLabel___int pstart end start asida pda rv root_switched rva s) and ?R1059 invLabel___int pstart end start asida pda rv root_switched rva\<rbrace>
 6. \<And>invLabel___int pstart end start asida pda. \<lbrakk>flushtype_relation typ invLabel___int; pstart = ps; end = ve; start = vs; asida = asid; pda = pde_Ptr pd\<rbrakk> \<Longrightarrow> \<lbrace>?R909 invLabel___int pstart end start asida pda\<rbrace> setVMRootForFlush pd asid \<lbrace>\<lambda>rv. (\<lambda>s. vs \<le> ve \<and> ps \<le> ps + (ve - vs) \<and> vs && mask 5 = ps && mask 5 \<and> unat (ve - vs) \<le> gsMaxObjectSize s) and ?R1018 invLabel___int pstart end start asida pda rv\<rbrace>
 7. \<And>invLabel___int pstart end start asida pda. \<lbrakk>flushtype_relation typ invLabel___int; pstart = ps; end = ve; start = vs; asida = asid; pda = pde_Ptr pd\<rbrakk> \<Longrightarrow> ccorres (K (K (\<lambda>_. False)) \<currency> dc \<circ> Inr) (liftxf errstate id (K ()) ret__unsigned_long_') (?Pf895 invLabel___int pstart end start asida pda) (?Rf895 invLabel___int pstart end start asida pda) [SKIP] (return ()) (SKIP;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))
 8. \<And>invLabel___int pstart end start asida pda s s'. \<lbrakk>flushtype_relation typ invLabel___int; pstart = ps; end = ve; start = vs; asida = asid; pda = pde_Ptr pd; (s, s') \<in> rf_sr; (invs' and (\<lambda>y. asid \<le> mask local.asid_bits) and (\<lambda>s. ps \<le> ps + (ve - vs) \<and> vs && mask 5 = ps && mask 5 \<and> unat (ve - vs) \<le> gsMaxObjectSize s)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. vs < ve \<longrightarrow> (invs' and (\<lambda>s. asid \<le> mask local.asid_bits) and ?R909 invLabel___int pstart end start asida pda) s) and (\<lambda>s. \<not> vs < ve \<longrightarrow> ?Pf895 invLabel___int pstart end start asida pda s)) s \<and> s' \<in> {s. (s \<in> \<lbrace>start < end\<rbrace> \<longrightarrow> s \<in> {s. asid_'_update (\<lambda>_. asida) (pd_'_update (\<lambda>_. pda) s) \<in> UNIV \<inter> \<lbrace>\<acute>pd = pde_Ptr pd\<rbrace> \<inter> \<lbrace>\<acute>asid = asid\<rbrace>} \<inter> {s'. \<forall>t rv. ret__unsigned_long_' t = from_bool rv \<longrightarrow> root_switched_'_update (\<lambda>_. ret__unsigned_long_' t) (s'\<lparr>globals := globals t\<rparr>) \<in> {s. pstart_'_update (\<lambda>_. pstart) (end_'_update (\<lambda>_. end) (start_'_update (\<lambda>_. start) (s\<lparr>invLabel___int_' := invLabel___int\<rparr>))) \<in> \<lbrace>flushtype_relation typ \<acute>invLabel___int\<rbrace> \<inter> \<lbrace>\<acute>start = vs\<rbrace> \<inter> \<lbrace>\<acute>end = ve\<rbrace> \<inter> \<lbrace>\<acute>pstart = ps\<rbrace>} \<inter> {s'. \<forall>ta rva. dc rva (xfdc ta) \<longrightarrow> s'\<lparr>globals := globals ta\<rparr> \<in> {s. (s \<in> \<lbrace>\<^bsup>t\<^esup>ret__unsigned_long \<noteq> 0\<rbrace> \<longrightarrow> s \<in> {s. \<forall>rv. ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr rv \<longrightarrow> s \<in> {s. tcb_'_update (\<lambda>_. ksCurThread_' (globals s)) s \<in> UNIV \<inter> \<lbrace>\<acute>tcb = tcb_ptr_to_ctcb_ptr rv\<rbrace>}}) \<and> (s \<notin> \<lbrace>\<^bsup>t\<^esup>ret__unsigned_long \<noteq> 0\<rbrace> \<longrightarrow> s \<in> ?Rf1064 invLabel___int pstart end start asida pda rv (ret__unsigned_long_' t) rva (xfdc ta))}}}) \<and> (s \<notin> \<lbrace>start < end\<rbrace> \<longrightarrow> s \<in> ?Rf895 invLabel___int pstart end start asida pda)} proof (prove)
goal (7 subgoals):
 1. \<And>invLabel___int pstart end start asida pda rv root_switched rva xfdc x rv'. \<lbrakk>flushtype_relation typ invLabel___int; pstart = ps; end = ve; start = vs; asida = asid; pda = pde_Ptr pd; root_switched = from_bool rv; dc rva xfdc; dc x rv'\<rbrakk> \<Longrightarrow> ccorres (K (K (\<lambda>_. False)) \<currency> dc \<circ> Inr) (liftxf errstate id (K ()) ret__unsigned_long_') (?Q1057 invLabel___int pstart end start asida pda rv root_switched rva xfdc x) (?Q'1057 invLabel___int pstart end start asida pda rv root_switched rva xfdc x rv') [SKIP] (return x) (return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))
 2. \<And>invLabel___int pstart end start asida pda rv root_switched rva xfdc. \<lbrakk>flushtype_relation typ invLabel___int; pstart = ps; end = ve; start = vs; asida = asid; pda = pde_Ptr pd; root_switched = from_bool rv; dc rva xfdc\<rbrakk> \<Longrightarrow> \<lbrace>?R1059 invLabel___int pstart end start asida pda rv root_switched rva\<rbrace> if rv then getCurThread >>= setVMRoot else return () \<lbrace>?Q1057 invLabel___int pstart end start asida pda rv root_switched rva xfdc\<rbrace>
 3. \<And>invLabel___int pstart end start asida pda rv root_switched rva xfdca. \<lbrakk>flushtype_relation typ invLabel___int; pstart = ps; end = ve; start = vs; asida = asid; pda = pde_Ptr pd; root_switched = from_bool rv; dc rva xfdca\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (?Q'1057 invLabel___int pstart end start asida pda rv root_switched rva xfdca)
 4. \<And>invLabel___int pstart end start asida pda rv root_switched. \<lbrakk>flushtype_relation typ invLabel___int; pstart = ps; end = ve; start = vs; asida = asid; pda = pde_Ptr pd; root_switched = from_bool rv\<rbrakk> \<Longrightarrow> \<lbrace>?R1018 invLabel___int pstart end start asida pda rv\<rbrace> doMachineOp (doFlush typ vs ve ps) \<lbrace>\<lambda>rva. (\<lambda>_. True) and (\<lambda>s. rv \<longrightarrow> (\<forall>rv. ksCurThread s = rv \<longrightarrow> (all_invs_but_ct_idle_or_in_cur_domain' and tcb_at' rv) s)) and (\<lambda>s. \<not> rv \<longrightarrow> True) and ?R1059 invLabel___int pstart end start asida pda rv root_switched rva\<rbrace>
 5. \<And>invLabel___int pstart end start asida pda. \<lbrakk>flushtype_relation typ invLabel___int; pstart = ps; end = ve; start = vs; asida = asid; pda = pde_Ptr pd\<rbrakk> \<Longrightarrow> \<lbrace>?R909 invLabel___int pstart end start asida pda\<rbrace> setVMRootForFlush pd asid \<lbrace>\<lambda>rv. (\<lambda>s. vs \<le> ve \<and> ps \<le> ps + (ve - vs) \<and> vs && mask 5 = ps && mask 5 \<and> unat (ve - vs) \<le> gsMaxObjectSize s) and ?R1018 invLabel___int pstart end start asida pda rv\<rbrace>
 6. \<And>invLabel___int pstart end start asida pda. \<lbrakk>flushtype_relation typ invLabel___int; pstart = ps; end = ve; start = vs; asida = asid; pda = pde_Ptr pd\<rbrakk> \<Longrightarrow> ccorres (K (K (\<lambda>_. False)) \<currency> dc \<circ> Inr) (liftxf errstate id (K ()) ret__unsigned_long_') (?Pf895 invLabel___int pstart end start asida pda) (?Rf895 invLabel___int pstart end start asida pda) [SKIP] (return ()) (SKIP;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))
 7. \<And>invLabel___int pstart end start asida pda s s'. \<lbrakk>flushtype_relation typ invLabel___int; pstart = ps; end = ve; start = vs; asida = asid; pda = pde_Ptr pd; (s, s') \<in> rf_sr; (invs' and (\<lambda>y. asid \<le> mask local.asid_bits) and (\<lambda>s. ps \<le> ps + (ve - vs) \<and> vs && mask 5 = ps && mask 5 \<and> unat (ve - vs) \<le> gsMaxObjectSize s)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. vs < ve \<longrightarrow> (invs' and (\<lambda>s. asid \<le> mask local.asid_bits) and ?R909 invLabel___int pstart end start asida pda) s) and (\<lambda>s. \<not> vs < ve \<longrightarrow> ?Pf895 invLabel___int pstart end start asida pda s)) s \<and> s' \<in> {s. (s \<in> \<lbrace>start < end\<rbrace> \<longrightarrow> s \<in> {s. asid_'_update (\<lambda>_. asida) (pd_'_update (\<lambda>_. pda) s) \<in> UNIV \<inter> \<lbrace>\<acute>pd = pde_Ptr pd\<rbrace> \<inter> \<lbrace>\<acute>asid = asid\<rbrace>} \<inter> {s'. \<forall>t rv. ret__unsigned_long_' t = from_bool rv \<longrightarrow> root_switched_'_update (\<lambda>_. ret__unsigned_long_' t) (s'\<lparr>globals := globals t\<rparr>) \<in> {s. pstart_'_update (\<lambda>_. pstart) (end_'_update (\<lambda>_. end) (start_'_update (\<lambda>_. start) (s\<lparr>invLabel___int_' := invLabel___int\<rparr>))) \<in> \<lbrace>flushtype_relation typ \<acute>invLabel___int\<rbrace> \<inter> \<lbrace>\<acute>start = vs\<rbrace> \<inter> \<lbrace>\<acute>end = ve\<rbrace> \<inter> \<lbrace>\<acute>pstart = ps\<rbrace>} \<inter> {s'. \<forall>ta rv. dc rv (xfdc ta) \<longrightarrow> s'\<lparr>globals := globals ta\<rparr> \<in> {s. (s \<in> \<lbrace>\<^bsup>t\<^esup>ret__unsigned_long \<noteq> 0\<rbrace> \<longrightarrow> s \<in> {s. \<forall>rv. ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr rv \<longrightarrow> s \<in> {s. tcb_'_update (\<lambda>_. ksCurThread_' (globals s)) s \<in> UNIV \<inter> \<lbrace>\<acute>tcb = tcb_ptr_to_ctcb_ptr rv\<rbrace>}}) \<and> (s \<notin> \<lbrace>\<^bsup>t\<^esup>ret__unsigned_long \<noteq> 0\<rbrace> \<longrightarrow> s \<in> UNIV)}}}) \<and> (s \<notin> \<lbrace>start < end\<rbrace> \<longrightarrow> s \<in> ?Rf895 invLabel___int pstart end start asida pda)} proof (prove)
goal (7 subgoals):
 1. \<And>invLabel___int pstart end start asida pda rv root_switched rva xfdc x rv'. \<lbrakk>flushtype_relation typ invLabel___int; pstart = ps; end = ve; start = vs; asida = asid; pda = pde_Ptr pd; root_switched = from_bool rv; dc rva xfdc; dc x rv'\<rbrakk> \<Longrightarrow> \<forall>\<sigma>. \<Gamma>\<turnstile> {s. True \<and> s \<in> UNIV \<and> (\<sigma>, s) \<in> rf_sr} return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE) {},{s. \<exists>(rv, \<sigma>')\<in>fst (return x \<sigma>). (\<sigma>', s) \<in> rf_sr \<and> (K (K (\<lambda>_. False)) \<currency> dc \<circ> Inr) rv (liftxf errstate id (K ()) ret__unsigned_long_' s)}
 2. \<And>invLabel___int pstart end start asida pda rv root_switched rva xfdc. \<lbrakk>flushtype_relation typ invLabel___int; pstart = ps; end = ve; start = vs; asida = asid; pda = pde_Ptr pd; root_switched = from_bool rv; dc rva xfdc\<rbrakk> \<Longrightarrow> \<lbrace>?R1059 invLabel___int pstart end start asida pda rv root_switched rva\<rbrace> if rv then getCurThread >>= setVMRoot else return () \<lbrace>\<lambda>x _. True\<rbrace>
 3. \<And>invLabel___int pstart end start asida pda rv root_switched rva xfdca. \<lbrakk>flushtype_relation typ invLabel___int; pstart = ps; end = ve; start = vs; asida = asid; pda = pde_Ptr pd; root_switched = from_bool rv; dc rva xfdca\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (\<lambda>x rv'. UNIV)
 4. \<And>invLabel___int pstart end start asida pda rv root_switched. \<lbrakk>flushtype_relation typ invLabel___int; pstart = ps; end = ve; start = vs; asida = asid; pda = pde_Ptr pd; root_switched = from_bool rv\<rbrakk> \<Longrightarrow> \<lbrace>?R1018 invLabel___int pstart end start asida pda rv\<rbrace> doMachineOp (doFlush typ vs ve ps) \<lbrace>\<lambda>rva. (\<lambda>_. True) and (\<lambda>s. rv \<longrightarrow> (\<forall>rv. ksCurThread s = rv \<longrightarrow> (all_invs_but_ct_idle_or_in_cur_domain' and tcb_at' rv) s)) and (\<lambda>s. \<not> rv \<longrightarrow> True) and ?R1059 invLabel___int pstart end start asida pda rv root_switched rva\<rbrace>
 5. \<And>invLabel___int pstart end start asida pda. \<lbrakk>flushtype_relation typ invLabel___int; pstart = ps; end = ve; start = vs; asida = asid; pda = pde_Ptr pd\<rbrakk> \<Longrightarrow> \<lbrace>?R909 invLabel___int pstart end start asida pda\<rbrace> setVMRootForFlush pd asid \<lbrace>\<lambda>rv. (\<lambda>s. vs \<le> ve \<and> ps \<le> ps + (ve - vs) \<and> vs && mask 5 = ps && mask 5 \<and> unat (ve - vs) \<le> gsMaxObjectSize s) and ?R1018 invLabel___int pstart end start asida pda rv\<rbrace>
 6. \<And>invLabel___int pstart end start asida pda. \<lbrakk>flushtype_relation typ invLabel___int; pstart = ps; end = ve; start = vs; asida = asid; pda = pde_Ptr pd\<rbrakk> \<Longrightarrow> ccorres (K (K (\<lambda>_. False)) \<currency> dc \<circ> Inr) (liftxf errstate id (K ()) ret__unsigned_long_') (?Pf895 invLabel___int pstart end start asida pda) (?Rf895 invLabel___int pstart end start asida pda) [SKIP] (return ()) (SKIP;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))
 7. \<And>invLabel___int pstart end start asida pda s s'. \<lbrakk>flushtype_relation typ invLabel___int; pstart = ps; end = ve; start = vs; asida = asid; pda = pde_Ptr pd; (s, s') \<in> rf_sr; (invs' and (\<lambda>y. asid \<le> mask local.asid_bits) and (\<lambda>s. ps \<le> ps + (ve - vs) \<and> vs && mask 5 = ps && mask 5 \<and> unat (ve - vs) \<le> gsMaxObjectSize s)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. vs < ve \<longrightarrow> (invs' and (\<lambda>s. asid \<le> mask local.asid_bits) and ?R909 invLabel___int pstart end start asida pda) s) and (\<lambda>s. \<not> vs < ve \<longrightarrow> ?Pf895 invLabel___int pstart end start asida pda s)) s \<and> s' \<in> {s. (s \<in> \<lbrace>start < end\<rbrace> \<longrightarrow> s \<in> {s. asid_'_update (\<lambda>_. asida) (pd_'_update (\<lambda>_. pda) s) \<in> UNIV \<inter> \<lbrace>\<acute>pd = pde_Ptr pd\<rbrace> \<inter> \<lbrace>\<acute>asid = asid\<rbrace>} \<inter> {s'. \<forall>t rv. ret__unsigned_long_' t = from_bool rv \<longrightarrow> root_switched_'_update (\<lambda>_. ret__unsigned_long_' t) (s'\<lparr>globals := globals t\<rparr>) \<in> {s. pstart_'_update (\<lambda>_. pstart) (end_'_update (\<lambda>_. end) (start_'_update (\<lambda>_. start) (s\<lparr>invLabel___int_' := invLabel___int\<rparr>))) \<in> \<lbrace>flushtype_relation typ \<acute>invLabel___int\<rbrace> \<inter> \<lbrace>\<acute>start = vs\<rbrace> \<inter> \<lbrace>\<acute>end = ve\<rbrace> \<inter> \<lbrace>\<acute>pstart = ps\<rbrace>} \<inter> {s'. \<forall>ta rv. dc rv (xfdc ta) \<longrightarrow> s'\<lparr>globals := globals ta\<rparr> \<in> {s. (s \<in> \<lbrace>\<^bsup>t\<^esup>ret__unsigned_long \<noteq> 0\<rbrace> \<longrightarrow> s \<in> {s. \<forall>rv. ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr rv \<longrightarrow> s \<in> {s. tcb_'_update (\<lambda>_. ksCurThread_' (globals s)) s \<in> UNIV \<inter> \<lbrace>\<acute>tcb = tcb_ptr_to_ctcb_ptr rv\<rbrace>}}) \<and> (s \<notin> \<lbrace>\<^bsup>t\<^esup>ret__unsigned_long \<noteq> 0\<rbrace> \<longrightarrow> s \<in> UNIV)}}}) \<and> (s \<notin> \<lbrace>start < end\<rbrace> \<longrightarrow> s \<in> ?Rf895 invLabel___int pstart end start asida pda)} proof (prove)
goal (7 subgoals):
 1. \<And>invLabel___int pstart end start asida pda rv root_switched rva xfdc x rv' \<sigma>. \<lbrakk>flushtype_relation typ invLabel___int; pstart = ps; end = ve; start = vs; asida = asid; pda = pde_Ptr pd; root_switched = from_bool rv; dc rva xfdc; dc x rv'\<rbrakk> \<Longrightarrow> {s. True \<and> s \<in> UNIV \<and> (\<sigma>, s) \<in> rf_sr} \<subseteq> {s. \<exists>(rv, \<sigma>')\<in>fst (return x \<sigma>). (\<sigma>', s\<lparr>ret__unsigned_long_' := SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE, global_exn_var_' := Return\<rparr>) \<in> rf_sr \<and> (K (K (\<lambda>_. False)) \<currency> dc) (Inr rv) (liftxf errstate id (K ()) ret__unsigned_long_' (s\<lparr>ret__unsigned_long_' := SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE, global_exn_var_' := Return\<rparr>))}
 2. \<And>invLabel___int pstart end start asida pda rv root_switched rva xfdc. \<lbrakk>flushtype_relation typ invLabel___int; pstart = ps; end = ve; start = vs; asida = asid; pda = pde_Ptr pd; root_switched = from_bool rv; dc rva xfdc\<rbrakk> \<Longrightarrow> \<lbrace>?R1059 invLabel___int pstart end start asida pda rv root_switched rva\<rbrace> if rv then getCurThread >>= setVMRoot else return () \<lbrace>\<lambda>x _. True\<rbrace>
 3. \<And>invLabel___int pstart end start asida pda rv root_switched rva xfdca. \<lbrakk>flushtype_relation typ invLabel___int; pstart = ps; end = ve; start = vs; asida = asid; pda = pde_Ptr pd; root_switched = from_bool rv; dc rva xfdca\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (\<lambda>x rv'. UNIV)
 4. \<And>invLabel___int pstart end start asida pda rv root_switched. \<lbrakk>flushtype_relation typ invLabel___int; pstart = ps; end = ve; start = vs; asida = asid; pda = pde_Ptr pd; root_switched = from_bool rv\<rbrakk> \<Longrightarrow> \<lbrace>?R1018 invLabel___int pstart end start asida pda rv\<rbrace> doMachineOp (doFlush typ vs ve ps) \<lbrace>\<lambda>rva. (\<lambda>_. True) and (\<lambda>s. rv \<longrightarrow> (\<forall>rv. ksCurThread s = rv \<longrightarrow> (all_invs_but_ct_idle_or_in_cur_domain' and tcb_at' rv) s)) and (\<lambda>s. \<not> rv \<longrightarrow> True) and ?R1059 invLabel___int pstart end start asida pda rv root_switched rva\<rbrace>
 5. \<And>invLabel___int pstart end start asida pda. \<lbrakk>flushtype_relation typ invLabel___int; pstart = ps; end = ve; start = vs; asida = asid; pda = pde_Ptr pd\<rbrakk> \<Longrightarrow> \<lbrace>?R909 invLabel___int pstart end start asida pda\<rbrace> setVMRootForFlush pd asid \<lbrace>\<lambda>rv. (\<lambda>s. vs \<le> ve \<and> ps \<le> ps + (ve - vs) \<and> vs && mask 5 = ps && mask 5 \<and> unat (ve - vs) \<le> gsMaxObjectSize s) and ?R1018 invLabel___int pstart end start asida pda rv\<rbrace>
 6. \<And>invLabel___int pstart end start asida pda. \<lbrakk>flushtype_relation typ invLabel___int; pstart = ps; end = ve; start = vs; asida = asid; pda = pde_Ptr pd\<rbrakk> \<Longrightarrow> ccorres (K (K (\<lambda>_. False)) \<currency> dc \<circ> Inr) (liftxf errstate id (K ()) ret__unsigned_long_') (?Pf895 invLabel___int pstart end start asida pda) (?Rf895 invLabel___int pstart end start asida pda) [SKIP] (return ()) (SKIP;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))
 7. \<And>invLabel___int pstart end start asida pda s s'. \<lbrakk>flushtype_relation typ invLabel___int; pstart = ps; end = ve; start = vs; asida = asid; pda = pde_Ptr pd; (s, s') \<in> rf_sr; (invs' and (\<lambda>y. asid \<le> mask local.asid_bits) and (\<lambda>s. ps \<le> ps + (ve - vs) \<and> vs && mask 5 = ps && mask 5 \<and> unat (ve - vs) \<le> gsMaxObjectSize s)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. vs < ve \<longrightarrow> (invs' and (\<lambda>s. asid \<le> mask local.asid_bits) and ?R909 invLabel___int pstart end start asida pda) s) and (\<lambda>s. \<not> vs < ve \<longrightarrow> ?Pf895 invLabel___int pstart end start asida pda s)) s \<and> s' \<in> {s. (s \<in> \<lbrace>start < end\<rbrace> \<longrightarrow> s \<in> {s. asid_'_update (\<lambda>_. asida) (pd_'_update (\<lambda>_. pda) s) \<in> UNIV \<inter> \<lbrace>\<acute>pd = pde_Ptr pd\<rbrace> \<inter> \<lbrace>\<acute>asid = asid\<rbrace>} \<inter> {s'. \<forall>t rv. ret__unsigned_long_' t = from_bool rv \<longrightarrow> root_switched_'_update (\<lambda>_. ret__unsigned_long_' t) (s'\<lparr>globals := globals t\<rparr>) \<in> {s. pstart_'_update (\<lambda>_. pstart) (end_'_update (\<lambda>_. end) (start_'_update (\<lambda>_. start) (s\<lparr>invLabel___int_' := invLabel___int\<rparr>))) \<in> \<lbrace>flushtype_relation typ \<acute>invLabel___int\<rbrace> \<inter> \<lbrace>\<acute>start = vs\<rbrace> \<inter> \<lbrace>\<acute>end = ve\<rbrace> \<inter> \<lbrace>\<acute>pstart = ps\<rbrace>} \<inter> {s'. \<forall>ta rv. dc rv (xfdc ta) \<longrightarrow> s'\<lparr>globals := globals ta\<rparr> \<in> {s. (s \<in> \<lbrace>\<^bsup>t\<^esup>ret__unsigned_long \<noteq> 0\<rbrace> \<longrightarrow> s \<in> {s. \<forall>rv. ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr rv \<longrightarrow> s \<in> {s. tcb_'_update (\<lambda>_. ksCurThread_' (globals s)) s \<in> UNIV \<inter> \<lbrace>\<acute>tcb = tcb_ptr_to_ctcb_ptr rv\<rbrace>}}) \<and> (s \<notin> \<lbrace>\<^bsup>t\<^esup>ret__unsigned_long \<noteq> 0\<rbrace> \<longrightarrow> s \<in> UNIV)}}}) \<and> (s \<notin> \<lbrace>start < end\<rbrace> \<longrightarrow> s \<in> ?Rf895 invLabel___int pstart end start asida pda)} proof (prove)
goal (6 subgoals):
 1. \<And>invLabel___int pstart end start asida pda rv root_switched rva xfdc. \<lbrakk>flushtype_relation typ invLabel___int; pstart = ps; end = ve; start = vs; asida = asid; pda = pde_Ptr pd; root_switched = from_bool rv; dc rva xfdc\<rbrakk> \<Longrightarrow> \<lbrace>?R1059 invLabel___int pstart end start asida pda rv root_switched rva\<rbrace> if rv then getCurThread >>= setVMRoot else return () \<lbrace>\<lambda>x _. True\<rbrace>
 2. \<And>invLabel___int pstart end start asida pda rv root_switched rva xfdca. \<lbrakk>flushtype_relation typ invLabel___int; pstart = ps; end = ve; start = vs; asida = asid; pda = pde_Ptr pd; root_switched = from_bool rv; dc rva xfdca\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (\<lambda>x rv'. UNIV)
 3. \<And>invLabel___int pstart end start asida pda rv root_switched. \<lbrakk>flushtype_relation typ invLabel___int; pstart = ps; end = ve; start = vs; asida = asid; pda = pde_Ptr pd; root_switched = from_bool rv\<rbrakk> \<Longrightarrow> \<lbrace>?R1018 invLabel___int pstart end start asida pda rv\<rbrace> doMachineOp (doFlush typ vs ve ps) \<lbrace>\<lambda>rva. (\<lambda>_. True) and (\<lambda>s. rv \<longrightarrow> (\<forall>rv. ksCurThread s = rv \<longrightarrow> (all_invs_but_ct_idle_or_in_cur_domain' and tcb_at' rv) s)) and (\<lambda>s. \<not> rv \<longrightarrow> True) and ?R1059 invLabel___int pstart end start asida pda rv root_switched rva\<rbrace>
 4. \<And>invLabel___int pstart end start asida pda. \<lbrakk>flushtype_relation typ invLabel___int; pstart = ps; end = ve; start = vs; asida = asid; pda = pde_Ptr pd\<rbrakk> \<Longrightarrow> \<lbrace>?R909 invLabel___int pstart end start asida pda\<rbrace> setVMRootForFlush pd asid \<lbrace>\<lambda>rv. (\<lambda>s. vs \<le> ve \<and> ps \<le> ps + (ve - vs) \<and> vs && mask 5 = ps && mask 5 \<and> unat (ve - vs) \<le> gsMaxObjectSize s) and ?R1018 invLabel___int pstart end start asida pda rv\<rbrace>
 5. \<And>invLabel___int pstart end start asida pda. \<lbrakk>flushtype_relation typ invLabel___int; pstart = ps; end = ve; start = vs; asida = asid; pda = pde_Ptr pd\<rbrakk> \<Longrightarrow> ccorres (K (K (\<lambda>_. False)) \<currency> dc \<circ> Inr) (liftxf errstate id (K ()) ret__unsigned_long_') (?Pf895 invLabel___int pstart end start asida pda) (?Rf895 invLabel___int pstart end start asida pda) [SKIP] (return ()) (SKIP;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))
 6. \<And>invLabel___int pstart end start asida pda s s'. \<lbrakk>flushtype_relation typ invLabel___int; pstart = ps; end = ve; start = vs; asida = asid; pda = pde_Ptr pd; (s, s') \<in> rf_sr; (invs' and (\<lambda>y. asid \<le> mask local.asid_bits) and (\<lambda>s. ps \<le> ps + (ve - vs) \<and> vs && mask 5 = ps && mask 5 \<and> unat (ve - vs) \<le> gsMaxObjectSize s)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. vs < ve \<longrightarrow> (invs' and (\<lambda>s. asid \<le> mask local.asid_bits) and ?R909 invLabel___int pstart end start asida pda) s) and (\<lambda>s. \<not> vs < ve \<longrightarrow> ?Pf895 invLabel___int pstart end start asida pda s)) s \<and> s' \<in> {s. (s \<in> \<lbrace>start < end\<rbrace> \<longrightarrow> s \<in> {s. asid_'_update (\<lambda>_. asida) (pd_'_update (\<lambda>_. pda) s) \<in> UNIV \<inter> \<lbrace>\<acute>pd = pde_Ptr pd\<rbrace> \<inter> \<lbrace>\<acute>asid = asid\<rbrace>} \<inter> {s'. \<forall>t rv. ret__unsigned_long_' t = from_bool rv \<longrightarrow> root_switched_'_update (\<lambda>_. ret__unsigned_long_' t) (s'\<lparr>globals := globals t\<rparr>) \<in> {s. pstart_'_update (\<lambda>_. pstart) (end_'_update (\<lambda>_. end) (start_'_update (\<lambda>_. start) (s\<lparr>invLabel___int_' := invLabel___int\<rparr>))) \<in> \<lbrace>flushtype_relation typ \<acute>invLabel___int\<rbrace> \<inter> \<lbrace>\<acute>start = vs\<rbrace> \<inter> \<lbrace>\<acute>end = ve\<rbrace> \<inter> \<lbrace>\<acute>pstart = ps\<rbrace>} \<inter> {s'. \<forall>ta rv. dc rv (xfdc ta) \<longrightarrow> s'\<lparr>globals := globals ta\<rparr> \<in> {s. (s \<in> \<lbrace>\<^bsup>t\<^esup>ret__unsigned_long \<noteq> 0\<rbrace> \<longrightarrow> s \<in> {s. \<forall>rv. ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr rv \<longrightarrow> s \<in> {s. tcb_'_update (\<lambda>_. ksCurThread_' (globals s)) s \<in> UNIV \<inter> \<lbrace>\<acute>tcb = tcb_ptr_to_ctcb_ptr rv\<rbrace>}}) \<and> (s \<notin> \<lbrace>\<^bsup>t\<^esup>ret__unsigned_long \<noteq> 0\<rbrace> \<longrightarrow> s \<in> UNIV)}}}) \<and> (s \<notin> \<lbrace>start < end\<rbrace> \<longrightarrow> s \<in> ?Rf895 invLabel___int pstart end start asida pda)} proof (prove)
goal (5 subgoals):
 1. \<And>invLabel___int pstart end start asida pda rv root_switched rva xfdca. \<lbrakk>flushtype_relation typ invLabel___int; pstart = ps; end = ve; start = vs; asida = asid; pda = pde_Ptr pd; root_switched = from_bool rv; dc rva xfdca\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (\<lambda>x rv'. UNIV)
 2. \<And>invLabel___int pstart end start asida pda rv root_switched. \<lbrakk>flushtype_relation typ invLabel___int; pstart = ps; end = ve; start = vs; asida = asid; pda = pde_Ptr pd; root_switched = from_bool rv\<rbrakk> \<Longrightarrow> \<lbrace>?R1018 invLabel___int pstart end start asida pda rv\<rbrace> doMachineOp (doFlush typ vs ve ps) \<lbrace>\<lambda>rva. (\<lambda>_. True) and (\<lambda>s. rv \<longrightarrow> (\<forall>rv. ksCurThread s = rv \<longrightarrow> (all_invs_but_ct_idle_or_in_cur_domain' and tcb_at' rv) s)) and (\<lambda>s. \<not> rv \<longrightarrow> True) and (\<lambda>_. True)\<rbrace>
 3. \<And>invLabel___int pstart end start asida pda. \<lbrakk>flushtype_relation typ invLabel___int; pstart = ps; end = ve; start = vs; asida = asid; pda = pde_Ptr pd\<rbrakk> \<Longrightarrow> \<lbrace>?R909 invLabel___int pstart end start asida pda\<rbrace> setVMRootForFlush pd asid \<lbrace>\<lambda>rv. (\<lambda>s. vs \<le> ve \<and> ps \<le> ps + (ve - vs) \<and> vs && mask 5 = ps && mask 5 \<and> unat (ve - vs) \<le> gsMaxObjectSize s) and ?R1018 invLabel___int pstart end start asida pda rv\<rbrace>
 4. \<And>invLabel___int pstart end start asida pda. \<lbrakk>flushtype_relation typ invLabel___int; pstart = ps; end = ve; start = vs; asida = asid; pda = pde_Ptr pd\<rbrakk> \<Longrightarrow> ccorres (K (K (\<lambda>_. False)) \<currency> dc \<circ> Inr) (liftxf errstate id (K ()) ret__unsigned_long_') (?Pf895 invLabel___int pstart end start asida pda) (?Rf895 invLabel___int pstart end start asida pda) [SKIP] (return ()) (SKIP;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))
 5. \<And>invLabel___int pstart end start asida pda s s'. \<lbrakk>flushtype_relation typ invLabel___int; pstart = ps; end = ve; start = vs; asida = asid; pda = pde_Ptr pd; (s, s') \<in> rf_sr; (invs' and (\<lambda>y. asid \<le> mask local.asid_bits) and (\<lambda>s. ps \<le> ps + (ve - vs) \<and> vs && mask 5 = ps && mask 5 \<and> unat (ve - vs) \<le> gsMaxObjectSize s)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. vs < ve \<longrightarrow> (invs' and (\<lambda>s. asid \<le> mask local.asid_bits) and ?R909 invLabel___int pstart end start asida pda) s) and (\<lambda>s. \<not> vs < ve \<longrightarrow> ?Pf895 invLabel___int pstart end start asida pda s)) s \<and> s' \<in> {s. (s \<in> \<lbrace>start < end\<rbrace> \<longrightarrow> s \<in> {s. asid_'_update (\<lambda>_. asida) (pd_'_update (\<lambda>_. pda) s) \<in> UNIV \<inter> \<lbrace>\<acute>pd = pde_Ptr pd\<rbrace> \<inter> \<lbrace>\<acute>asid = asid\<rbrace>} \<inter> {s'. \<forall>t rv. ret__unsigned_long_' t = from_bool rv \<longrightarrow> root_switched_'_update (\<lambda>_. ret__unsigned_long_' t) (s'\<lparr>globals := globals t\<rparr>) \<in> {s. pstart_'_update (\<lambda>_. pstart) (end_'_update (\<lambda>_. end) (start_'_update (\<lambda>_. start) (s\<lparr>invLabel___int_' := invLabel___int\<rparr>))) \<in> \<lbrace>flushtype_relation typ \<acute>invLabel___int\<rbrace> \<inter> \<lbrace>\<acute>start = vs\<rbrace> \<inter> \<lbrace>\<acute>end = ve\<rbrace> \<inter> \<lbrace>\<acute>pstart = ps\<rbrace>} \<inter> {s'. \<forall>ta rv. dc rv (xfdc ta) \<longrightarrow> s'\<lparr>globals := globals ta\<rparr> \<in> {s. (s \<in> \<lbrace>\<^bsup>t\<^esup>ret__unsigned_long \<noteq> 0\<rbrace> \<longrightarrow> s \<in> {s. \<forall>rv. ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr rv \<longrightarrow> s \<in> {s. tcb_'_update (\<lambda>_. ksCurThread_' (globals s)) s \<in> UNIV \<inter> \<lbrace>\<acute>tcb = tcb_ptr_to_ctcb_ptr rv\<rbrace>}}) \<and> (s \<notin> \<lbrace>\<^bsup>t\<^esup>ret__unsigned_long \<noteq> 0\<rbrace> \<longrightarrow> s \<in> UNIV)}}}) \<and> (s \<notin> \<lbrace>start < end\<rbrace> \<longrightarrow> s \<in> ?Rf895 invLabel___int pstart end start asida pda)} proof (prove)
goal (4 subgoals):
 1. \<And>invLabel___int pstart end start asida pda rv root_switched. \<lbrakk>flushtype_relation typ invLabel___int; pstart = ps; end = ve; start = vs; asida = asid; pda = pde_Ptr pd; root_switched = from_bool rv\<rbrakk> \<Longrightarrow> \<lbrace>?R1018 invLabel___int pstart end start asida pda rv\<rbrace> doMachineOp (doFlush typ vs ve ps) \<lbrace>\<lambda>rva. (\<lambda>_. True) and (\<lambda>s. rv \<longrightarrow> (\<forall>rv. ksCurThread s = rv \<longrightarrow> (all_invs_but_ct_idle_or_in_cur_domain' and tcb_at' rv) s)) and (\<lambda>s. \<not> rv \<longrightarrow> True) and (\<lambda>_. True)\<rbrace>
 2. \<And>invLabel___int pstart end start asida pda. \<lbrakk>flushtype_relation typ invLabel___int; pstart = ps; end = ve; start = vs; asida = asid; pda = pde_Ptr pd\<rbrakk> \<Longrightarrow> \<lbrace>?R909 invLabel___int pstart end start asida pda\<rbrace> setVMRootForFlush pd asid \<lbrace>\<lambda>rv. (\<lambda>s. vs \<le> ve \<and> ps \<le> ps + (ve - vs) \<and> vs && mask 5 = ps && mask 5 \<and> unat (ve - vs) \<le> gsMaxObjectSize s) and ?R1018 invLabel___int pstart end start asida pda rv\<rbrace>
 3. \<And>invLabel___int pstart end start asida pda. \<lbrakk>flushtype_relation typ invLabel___int; pstart = ps; end = ve; start = vs; asida = asid; pda = pde_Ptr pd\<rbrakk> \<Longrightarrow> ccorres (K (K (\<lambda>_. False)) \<currency> dc \<circ> Inr) (liftxf errstate id (K ()) ret__unsigned_long_') (?Pf895 invLabel___int pstart end start asida pda) (?Rf895 invLabel___int pstart end start asida pda) [SKIP] (return ()) (SKIP;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))
 4. \<And>invLabel___int pstart end start asida pda s s'. \<lbrakk>flushtype_relation typ invLabel___int; pstart = ps; end = ve; start = vs; asida = asid; pda = pde_Ptr pd; (s, s') \<in> rf_sr; (invs' and (\<lambda>y. asid \<le> mask local.asid_bits) and (\<lambda>s. ps \<le> ps + (ve - vs) \<and> vs && mask 5 = ps && mask 5 \<and> unat (ve - vs) \<le> gsMaxObjectSize s)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. vs < ve \<longrightarrow> (invs' and (\<lambda>s. asid \<le> mask local.asid_bits) and ?R909 invLabel___int pstart end start asida pda) s) and (\<lambda>s. \<not> vs < ve \<longrightarrow> ?Pf895 invLabel___int pstart end start asida pda s)) s \<and> s' \<in> {s. (s \<in> \<lbrace>start < end\<rbrace> \<longrightarrow> s \<in> {s. asid_'_update (\<lambda>_. asida) (pd_'_update (\<lambda>_. pda) s) \<in> UNIV \<inter> \<lbrace>\<acute>pd = pde_Ptr pd\<rbrace> \<inter> \<lbrace>\<acute>asid = asid\<rbrace>} \<inter> {s'. \<forall>t rv. ret__unsigned_long_' t = from_bool rv \<longrightarrow> root_switched_'_update (\<lambda>_. ret__unsigned_long_' t) (s'\<lparr>globals := globals t\<rparr>) \<in> {s. pstart_'_update (\<lambda>_. pstart) (end_'_update (\<lambda>_. end) (start_'_update (\<lambda>_. start) (s\<lparr>invLabel___int_' := invLabel___int\<rparr>))) \<in> \<lbrace>flushtype_relation typ \<acute>invLabel___int\<rbrace> \<inter> \<lbrace>\<acute>start = vs\<rbrace> \<inter> \<lbrace>\<acute>end = ve\<rbrace> \<inter> \<lbrace>\<acute>pstart = ps\<rbrace>} \<inter> {s'. \<forall>ta rv. dc rv (xfdc ta) \<longrightarrow> s'\<lparr>globals := globals ta\<rparr> \<in> {s. (s \<in> \<lbrace>\<^bsup>t\<^esup>ret__unsigned_long \<noteq> 0\<rbrace> \<longrightarrow> s \<in> {s. \<forall>rv. ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr rv \<longrightarrow> s \<in> {s. tcb_'_update (\<lambda>_. ksCurThread_' (globals s)) s \<in> UNIV \<inter> \<lbrace>\<acute>tcb = tcb_ptr_to_ctcb_ptr rv\<rbrace>}}) \<and> (s \<notin> \<lbrace>\<^bsup>t\<^esup>ret__unsigned_long \<noteq> 0\<rbrace> \<longrightarrow> s \<in> UNIV)}}}) \<and> (s \<notin> \<lbrace>start < end\<rbrace> \<longrightarrow> s \<in> ?Rf895 invLabel___int pstart end start asida pda)} proof (prove)
goal (4 subgoals):
 1. \<And>invLabel___int pstart end start asida pda rv root_switched. \<lbrakk>flushtype_relation typ invLabel___int; pstart = ps; end = ve; start = vs; asida = asid; pda = pde_Ptr pd; root_switched = from_bool rv\<rbrakk> \<Longrightarrow> \<lbrace>?R1018 invLabel___int ps ve vs asid (pde_Ptr pd) rv\<rbrace> doMachineOp (doFlush typ vs ve ps) \<lbrace>\<lambda>rva s. rv \<longrightarrow> all_invs_but_ct_idle_or_in_cur_domain' s \<and> cur_tcb' s\<rbrace>
 2. \<And>invLabel___int pstart end start asida pda. \<lbrakk>flushtype_relation typ invLabel___int; pstart = ps; end = ve; start = vs; asida = asid; pda = pde_Ptr pd\<rbrakk> \<Longrightarrow> \<lbrace>?R909 invLabel___int pstart end start asida pda\<rbrace> setVMRootForFlush pd asid \<lbrace>\<lambda>rv. (\<lambda>s. vs \<le> ve \<and> ps \<le> ps + (ve - vs) \<and> vs && mask 5 = ps && mask 5 \<and> unat (ve - vs) \<le> gsMaxObjectSize s) and ?R1018 invLabel___int pstart end start asida pda rv\<rbrace>
 3. \<And>invLabel___int pstart end start asida pda. \<lbrakk>flushtype_relation typ invLabel___int; pstart = ps; end = ve; start = vs; asida = asid; pda = pde_Ptr pd\<rbrakk> \<Longrightarrow> ccorres (K (K (\<lambda>_. False)) \<currency> dc \<circ> Inr) (liftxf errstate id (K ()) ret__unsigned_long_') (?Pf895 invLabel___int pstart end start asida pda) (?Rf895 invLabel___int pstart end start asida pda) [SKIP] (return ()) (SKIP;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))
 4. \<And>invLabel___int pstart end start asida pda s s'. \<lbrakk>flushtype_relation typ invLabel___int; pstart = ps; end = ve; start = vs; asida = asid; pda = pde_Ptr pd; (s, s') \<in> rf_sr; (invs' and (\<lambda>y. asid \<le> mask local.asid_bits) and (\<lambda>s. ps \<le> ps + (ve - vs) \<and> vs && mask 5 = ps && mask 5 \<and> unat (ve - vs) \<le> gsMaxObjectSize s)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. vs < ve \<longrightarrow> (invs' and (\<lambda>s. asid \<le> mask local.asid_bits) and ?R909 invLabel___int pstart end start asida pda) s) and (\<lambda>s. \<not> vs < ve \<longrightarrow> ?Pf895 invLabel___int pstart end start asida pda s)) s \<and> s' \<in> {s. (s \<in> \<lbrace>start < end\<rbrace> \<longrightarrow> s \<in> {s. asid_'_update (\<lambda>_. asida) (pd_'_update (\<lambda>_. pda) s) \<in> UNIV \<inter> \<lbrace>\<acute>pd = pde_Ptr pd\<rbrace> \<inter> \<lbrace>\<acute>asid = asid\<rbrace>} \<inter> {s'. \<forall>t rv. ret__unsigned_long_' t = from_bool rv \<longrightarrow> root_switched_'_update (\<lambda>_. ret__unsigned_long_' t) (s'\<lparr>globals := globals t\<rparr>) \<in> {s. pstart_'_update (\<lambda>_. pstart) (end_'_update (\<lambda>_. end) (start_'_update (\<lambda>_. start) (s\<lparr>invLabel___int_' := invLabel___int\<rparr>))) \<in> \<lbrace>flushtype_relation typ \<acute>invLabel___int\<rbrace> \<inter> \<lbrace>\<acute>start = vs\<rbrace> \<inter> \<lbrace>\<acute>end = ve\<rbrace> \<inter> \<lbrace>\<acute>pstart = ps\<rbrace>} \<inter> {s'. \<forall>ta rv. dc rv (xfdc ta) \<longrightarrow> s'\<lparr>globals := globals ta\<rparr> \<in> {s. (s \<in> \<lbrace>\<^bsup>t\<^esup>ret__unsigned_long \<noteq> 0\<rbrace> \<longrightarrow> s \<in> {s. \<forall>rv. ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr rv \<longrightarrow> s \<in> {s. tcb_'_update (\<lambda>_. ksCurThread_' (globals s)) s \<in> UNIV \<inter> \<lbrace>\<acute>tcb = tcb_ptr_to_ctcb_ptr rv\<rbrace>}}) \<and> (s \<notin> \<lbrace>\<^bsup>t\<^esup>ret__unsigned_long \<noteq> 0\<rbrace> \<longrightarrow> s \<in> UNIV)}}}) \<and> (s \<notin> \<lbrace>start < end\<rbrace> \<longrightarrow> s \<in> ?Rf895 invLabel___int pstart end start asida pda)} proof (prove)
goal (5 subgoals):
 1. \<And>invLabel___int pstart end start asida pda rv root_switched rva s. \<lbrakk>flushtype_relation typ invLabel___int; pstart = ps; end = ve; start = vs; asida = asid; pda = pde_Ptr pd; root_switched = from_bool rv; invs' s \<and> cur_tcb' s\<rbrakk> \<Longrightarrow> rv \<longrightarrow> all_invs_but_ct_idle_or_in_cur_domain' s \<and> cur_tcb' s
 2. \<And>invLabel___int pstart end start asida pda rv root_switched. \<lbrakk>flushtype_relation typ invLabel___int; pstart = ps; end = ve; start = vs; asida = asid; pda = pde_Ptr pd; root_switched = from_bool rv\<rbrakk> \<Longrightarrow> \<lbrace>?R1018 invLabel___int ps ve vs asid (pde_Ptr pd) rv\<rbrace> doMachineOp (doFlush typ vs ve ps) \<lbrace>\<lambda>_ s. invs' s \<and> cur_tcb' s\<rbrace>
 3. \<And>invLabel___int pstart end start asida pda. \<lbrakk>flushtype_relation typ invLabel___int; pstart = ps; end = ve; start = vs; asida = asid; pda = pde_Ptr pd\<rbrakk> \<Longrightarrow> \<lbrace>?R909 invLabel___int pstart end start asida pda\<rbrace> setVMRootForFlush pd asid \<lbrace>\<lambda>rv. (\<lambda>s. vs \<le> ve \<and> ps \<le> ps + (ve - vs) \<and> vs && mask 5 = ps && mask 5 \<and> unat (ve - vs) \<le> gsMaxObjectSize s) and ?R1018 invLabel___int pstart end start asida pda rv\<rbrace>
 4. \<And>invLabel___int pstart end start asida pda. \<lbrakk>flushtype_relation typ invLabel___int; pstart = ps; end = ve; start = vs; asida = asid; pda = pde_Ptr pd\<rbrakk> \<Longrightarrow> ccorres (K (K (\<lambda>_. False)) \<currency> dc \<circ> Inr) (liftxf errstate id (K ()) ret__unsigned_long_') (?Pf895 invLabel___int pstart end start asida pda) (?Rf895 invLabel___int pstart end start asida pda) [SKIP] (return ()) (SKIP;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))
 5. \<And>invLabel___int pstart end start asida pda s s'. \<lbrakk>flushtype_relation typ invLabel___int; pstart = ps; end = ve; start = vs; asida = asid; pda = pde_Ptr pd; (s, s') \<in> rf_sr; (invs' and (\<lambda>y. asid \<le> mask local.asid_bits) and (\<lambda>s. ps \<le> ps + (ve - vs) \<and> vs && mask 5 = ps && mask 5 \<and> unat (ve - vs) \<le> gsMaxObjectSize s)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. vs < ve \<longrightarrow> (invs' and (\<lambda>s. asid \<le> mask local.asid_bits) and ?R909 invLabel___int pstart end start asida pda) s) and (\<lambda>s. \<not> vs < ve \<longrightarrow> ?Pf895 invLabel___int pstart end start asida pda s)) s \<and> s' \<in> {s. (s \<in> \<lbrace>start < end\<rbrace> \<longrightarrow> s \<in> {s. asid_'_update (\<lambda>_. asida) (pd_'_update (\<lambda>_. pda) s) \<in> UNIV \<inter> \<lbrace>\<acute>pd = pde_Ptr pd\<rbrace> \<inter> \<lbrace>\<acute>asid = asid\<rbrace>} \<inter> {s'. \<forall>t rv. ret__unsigned_long_' t = from_bool rv \<longrightarrow> root_switched_'_update (\<lambda>_. ret__unsigned_long_' t) (s'\<lparr>globals := globals t\<rparr>) \<in> {s. pstart_'_update (\<lambda>_. pstart) (end_'_update (\<lambda>_. end) (start_'_update (\<lambda>_. start) (s\<lparr>invLabel___int_' := invLabel___int\<rparr>))) \<in> \<lbrace>flushtype_relation typ \<acute>invLabel___int\<rbrace> \<inter> \<lbrace>\<acute>start = vs\<rbrace> \<inter> \<lbrace>\<acute>end = ve\<rbrace> \<inter> \<lbrace>\<acute>pstart = ps\<rbrace>} \<inter> {s'. \<forall>ta rv. dc rv (xfdc ta) \<longrightarrow> s'\<lparr>globals := globals ta\<rparr> \<in> {s. (s \<in> \<lbrace>\<^bsup>t\<^esup>ret__unsigned_long \<noteq> 0\<rbrace> \<longrightarrow> s \<in> {s. \<forall>rv. ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr rv \<longrightarrow> s \<in> {s. tcb_'_update (\<lambda>_. ksCurThread_' (globals s)) s \<in> UNIV \<inter> \<lbrace>\<acute>tcb = tcb_ptr_to_ctcb_ptr rv\<rbrace>}}) \<and> (s \<notin> \<lbrace>\<^bsup>t\<^esup>ret__unsigned_long \<noteq> 0\<rbrace> \<longrightarrow> s \<in> UNIV)}}}) \<and> (s \<notin> \<lbrace>start < end\<rbrace> \<longrightarrow> s \<in> ?Rf895 invLabel___int pstart end start asida pda)} proof (prove)
goal (4 subgoals):
 1. \<And>invLabel___int pstart end start asida pda rv root_switched. \<lbrakk>flushtype_relation typ invLabel___int; pstart = ps; end = ve; start = vs; asida = asid; pda = pde_Ptr pd; root_switched = from_bool rv\<rbrakk> \<Longrightarrow> \<lbrace>?R1018 invLabel___int ps ve vs asid (pde_Ptr pd) rv\<rbrace> doMachineOp (doFlush typ vs ve ps) \<lbrace>\<lambda>_ s. invs' s \<and> cur_tcb' s\<rbrace>
 2. \<And>invLabel___int pstart end start asida pda. \<lbrakk>flushtype_relation typ invLabel___int; pstart = ps; end = ve; start = vs; asida = asid; pda = pde_Ptr pd\<rbrakk> \<Longrightarrow> \<lbrace>?R909 invLabel___int pstart end start asida pda\<rbrace> setVMRootForFlush pd asid \<lbrace>\<lambda>rv. (\<lambda>s. vs \<le> ve \<and> ps \<le> ps + (ve - vs) \<and> vs && mask 5 = ps && mask 5 \<and> unat (ve - vs) \<le> gsMaxObjectSize s) and ?R1018 invLabel___int pstart end start asida pda rv\<rbrace>
 3. \<And>invLabel___int pstart end start asida pda. \<lbrakk>flushtype_relation typ invLabel___int; pstart = ps; end = ve; start = vs; asida = asid; pda = pde_Ptr pd\<rbrakk> \<Longrightarrow> ccorres (K (K (\<lambda>_. False)) \<currency> dc \<circ> Inr) (liftxf errstate id (K ()) ret__unsigned_long_') (?Pf895 invLabel___int pstart end start asida pda) (?Rf895 invLabel___int pstart end start asida pda) [SKIP] (return ()) (SKIP;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))
 4. \<And>invLabel___int pstart end start asida pda s s'. \<lbrakk>flushtype_relation typ invLabel___int; pstart = ps; end = ve; start = vs; asida = asid; pda = pde_Ptr pd; (s, s') \<in> rf_sr; (invs' and (\<lambda>y. asid \<le> mask local.asid_bits) and (\<lambda>s. ps \<le> ps + (ve - vs) \<and> vs && mask 5 = ps && mask 5 \<and> unat (ve - vs) \<le> gsMaxObjectSize s)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. vs < ve \<longrightarrow> (invs' and (\<lambda>s. asid \<le> mask local.asid_bits) and ?R909 invLabel___int pstart end start asida pda) s) and (\<lambda>s. \<not> vs < ve \<longrightarrow> ?Pf895 invLabel___int pstart end start asida pda s)) s \<and> s' \<in> {s. (s \<in> \<lbrace>start < end\<rbrace> \<longrightarrow> s \<in> {s. asid_'_update (\<lambda>_. asida) (pd_'_update (\<lambda>_. pda) s) \<in> UNIV \<inter> \<lbrace>\<acute>pd = pde_Ptr pd\<rbrace> \<inter> \<lbrace>\<acute>asid = asid\<rbrace>} \<inter> {s'. \<forall>t rv. ret__unsigned_long_' t = from_bool rv \<longrightarrow> root_switched_'_update (\<lambda>_. ret__unsigned_long_' t) (s'\<lparr>globals := globals t\<rparr>) \<in> {s. pstart_'_update (\<lambda>_. pstart) (end_'_update (\<lambda>_. end) (start_'_update (\<lambda>_. start) (s\<lparr>invLabel___int_' := invLabel___int\<rparr>))) \<in> \<lbrace>flushtype_relation typ \<acute>invLabel___int\<rbrace> \<inter> \<lbrace>\<acute>start = vs\<rbrace> \<inter> \<lbrace>\<acute>end = ve\<rbrace> \<inter> \<lbrace>\<acute>pstart = ps\<rbrace>} \<inter> {s'. \<forall>ta rv. dc rv (xfdc ta) \<longrightarrow> s'\<lparr>globals := globals ta\<rparr> \<in> {s. (s \<in> \<lbrace>\<^bsup>t\<^esup>ret__unsigned_long \<noteq> 0\<rbrace> \<longrightarrow> s \<in> {s. \<forall>rv. ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr rv \<longrightarrow> s \<in> {s. tcb_'_update (\<lambda>_. ksCurThread_' (globals s)) s \<in> UNIV \<inter> \<lbrace>\<acute>tcb = tcb_ptr_to_ctcb_ptr rv\<rbrace>}}) \<and> (s \<notin> \<lbrace>\<^bsup>t\<^esup>ret__unsigned_long \<noteq> 0\<rbrace> \<longrightarrow> s \<in> UNIV)}}}) \<and> (s \<notin> \<lbrace>start < end\<rbrace> \<longrightarrow> s \<in> ?Rf895 invLabel___int pstart end start asida pda)} proof (prove)
goal (2 subgoals):
 1. \<And>invLabel___int pstart end start asida pda. \<lbrakk>flushtype_relation typ invLabel___int; pstart = ps; end = ve; start = vs; asida = asid; pda = pde_Ptr pd\<rbrakk> \<Longrightarrow> ccorres (K (K (\<lambda>_. False)) \<currency> dc \<circ> Inr) (liftxf errstate id (K ()) ret__unsigned_long_') (?Pf895 invLabel___int pstart end start asida pda) (?Rf895 invLabel___int pstart end start asida pda) [SKIP] (return ()) (SKIP;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))
 2. \<And>invLabel___int pstart end start asida pda s s'. \<lbrakk>flushtype_relation typ invLabel___int; pstart = ps; end = ve; start = vs; asida = asid; pda = pde_Ptr pd; (s, s') \<in> rf_sr; (invs' and (\<lambda>y. asid \<le> mask local.asid_bits) and (\<lambda>s. ps \<le> ps + (ve - vs) \<and> vs && mask 5 = ps && mask 5 \<and> unat (ve - vs) \<le> gsMaxObjectSize s)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. vs < ve \<longrightarrow> (invs' and (\<lambda>s. asid \<le> mask local.asid_bits) and (\<lambda>s. (vs \<le> ve \<and> ps \<le> ps + (ve - vs) \<and> vs && mask 5 = ps && mask 5 \<and> unat (ve - vs) \<le> gsMaxObjectSize s) \<and> invs' s \<and> cur_tcb' s)) s) and (\<lambda>s. \<not> vs < ve \<longrightarrow> ?Pf895 invLabel___int pstart end start asida pda s)) s \<and> s' \<in> {s. (s \<in> \<lbrace>start < end\<rbrace> \<longrightarrow> s \<in> {s. asid_'_update (\<lambda>_. asida) (pd_'_update (\<lambda>_. pda) s) \<in> UNIV \<inter> \<lbrace>\<acute>pd = pde_Ptr pd\<rbrace> \<inter> \<lbrace>\<acute>asid = asid\<rbrace>} \<inter> {s'. \<forall>t rv. ret__unsigned_long_' t = from_bool rv \<longrightarrow> root_switched_'_update (\<lambda>_. ret__unsigned_long_' t) (s'\<lparr>globals := globals t\<rparr>) \<in> {s. pstart_'_update (\<lambda>_. pstart) (end_'_update (\<lambda>_. end) (start_'_update (\<lambda>_. start) (s\<lparr>invLabel___int_' := invLabel___int\<rparr>))) \<in> \<lbrace>flushtype_relation typ \<acute>invLabel___int\<rbrace> \<inter> \<lbrace>\<acute>start = vs\<rbrace> \<inter> \<lbrace>\<acute>end = ve\<rbrace> \<inter> \<lbrace>\<acute>pstart = ps\<rbrace>} \<inter> {s'. \<forall>ta rv. dc rv (xfdc ta) \<longrightarrow> s'\<lparr>globals := globals ta\<rparr> \<in> {s. (s \<in> \<lbrace>\<^bsup>t\<^esup>ret__unsigned_long \<noteq> 0\<rbrace> \<longrightarrow> s \<in> {s. \<forall>rv. ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr rv \<longrightarrow> s \<in> {s. tcb_'_update (\<lambda>_. ksCurThread_' (globals s)) s \<in> UNIV \<inter> \<lbrace>\<acute>tcb = tcb_ptr_to_ctcb_ptr rv\<rbrace>}}) \<and> (s \<notin> \<lbrace>\<^bsup>t\<^esup>ret__unsigned_long \<noteq> 0\<rbrace> \<longrightarrow> s \<in> UNIV)}}}) \<and> (s \<notin> \<lbrace>start < end\<rbrace> \<longrightarrow> s \<in> ?Rf895 invLabel___int pstart end start asida pda)} proof (prove)
goal (2 subgoals):
 1. \<And>invLabel___int pstart end start asida pda. \<lbrakk>flushtype_relation typ invLabel___int; pstart = ps; end = ve; start = vs; asida = asid; pda = pde_Ptr pd\<rbrakk> \<Longrightarrow> ccorres (K (K (\<lambda>_. False)) \<currency> dc \<circ> Inr) (liftxf errstate id (K ()) ret__unsigned_long_') (?Pf895 invLabel___int ps ve vs asid (pde_Ptr pd)) (?Rf895 invLabel___int ps ve vs asid (pde_Ptr pd)) [SKIP] (return ()) (return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))
 2. \<And>invLabel___int pstart end start asida pda s s'. \<lbrakk>flushtype_relation typ invLabel___int; pstart = ps; end = ve; start = vs; asida = asid; pda = pde_Ptr pd; (s, s') \<in> rf_sr; (invs' and (\<lambda>y. asid \<le> mask local.asid_bits) and (\<lambda>s. ps \<le> ps + (ve - vs) \<and> vs && mask 5 = ps && mask 5 \<and> unat (ve - vs) \<le> gsMaxObjectSize s)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. vs < ve \<longrightarrow> (invs' and (\<lambda>s. asid \<le> mask local.asid_bits) and (\<lambda>s. (vs \<le> ve \<and> ps \<le> ps + (ve - vs) \<and> vs && mask 5 = ps && mask 5 \<and> unat (ve - vs) \<le> gsMaxObjectSize s) \<and> invs' s \<and> cur_tcb' s)) s) and (\<lambda>s. \<not> vs < ve \<longrightarrow> ?Pf895 invLabel___int pstart end start asida pda s)) s \<and> s' \<in> {s. (s \<in> \<lbrace>start < end\<rbrace> \<longrightarrow> s \<in> {s. asid_'_update (\<lambda>_. asida) (pd_'_update (\<lambda>_. pda) s) \<in> UNIV \<inter> \<lbrace>\<acute>pd = pde_Ptr pd\<rbrace> \<inter> \<lbrace>\<acute>asid = asid\<rbrace>} \<inter> {s'. \<forall>t rv. ret__unsigned_long_' t = from_bool rv \<longrightarrow> root_switched_'_update (\<lambda>_. ret__unsigned_long_' t) (s'\<lparr>globals := globals t\<rparr>) \<in> {s. pstart_'_update (\<lambda>_. pstart) (end_'_update (\<lambda>_. end) (start_'_update (\<lambda>_. start) (s\<lparr>invLabel___int_' := invLabel___int\<rparr>))) \<in> \<lbrace>flushtype_relation typ \<acute>invLabel___int\<rbrace> \<inter> \<lbrace>\<acute>start = vs\<rbrace> \<inter> \<lbrace>\<acute>end = ve\<rbrace> \<inter> \<lbrace>\<acute>pstart = ps\<rbrace>} \<inter> {s'. \<forall>ta rv. dc rv (xfdc ta) \<longrightarrow> s'\<lparr>globals := globals ta\<rparr> \<in> {s. (s \<in> \<lbrace>\<^bsup>t\<^esup>ret__unsigned_long \<noteq> 0\<rbrace> \<longrightarrow> s \<in> {s. \<forall>rv. ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr rv \<longrightarrow> s \<in> {s. tcb_'_update (\<lambda>_. ksCurThread_' (globals s)) s \<in> UNIV \<inter> \<lbrace>\<acute>tcb = tcb_ptr_to_ctcb_ptr rv\<rbrace>}}) \<and> (s \<notin> \<lbrace>\<^bsup>t\<^esup>ret__unsigned_long \<noteq> 0\<rbrace> \<longrightarrow> s \<in> UNIV)}}}) \<and> (s \<notin> \<lbrace>start < end\<rbrace> \<longrightarrow> s \<in> ?Rf895 invLabel___int pstart end start asida pda)} proof (prove)
goal (2 subgoals):
 1. \<And>invLabel___int pstart end start asida pda. \<lbrakk>flushtype_relation typ invLabel___int; pstart = ps; end = ve; start = vs; asida = asid; pda = pde_Ptr pd\<rbrakk> \<Longrightarrow> \<forall>\<sigma>. \<Gamma>\<turnstile> {s. True \<and> s \<in> UNIV \<and> (\<sigma>, s) \<in> rf_sr} return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE) {},{s. \<exists>(rv, \<sigma>')\<in>fst (return () \<sigma>). (\<sigma>', s) \<in> rf_sr \<and> (K (K (\<lambda>_. False)) \<currency> dc \<circ> Inr) rv (liftxf errstate id (K ()) ret__unsigned_long_' s)}
 2. \<And>invLabel___int pstart end start asida pda s s'. \<lbrakk>flushtype_relation typ invLabel___int; pstart = ps; end = ve; start = vs; asida = asid; pda = pde_Ptr pd; (s, s') \<in> rf_sr; (invs' and (\<lambda>y. asid \<le> mask local.asid_bits) and (\<lambda>s. ps \<le> ps + (ve - vs) \<and> vs && mask 5 = ps && mask 5 \<and> unat (ve - vs) \<le> gsMaxObjectSize s)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. vs < ve \<longrightarrow> (invs' and (\<lambda>s. asid \<le> mask local.asid_bits) and (\<lambda>s. (vs \<le> ve \<and> ps \<le> ps + (ve - vs) \<and> vs && mask 5 = ps && mask 5 \<and> unat (ve - vs) \<le> gsMaxObjectSize s) \<and> invs' s \<and> cur_tcb' s)) s) and (\<lambda>s. \<not> vs < ve \<longrightarrow> True)) s \<and> s' \<in> {s. (s \<in> \<lbrace>start < end\<rbrace> \<longrightarrow> s \<in> {s. asid_'_update (\<lambda>_. asida) (pd_'_update (\<lambda>_. pda) s) \<in> UNIV \<inter> \<lbrace>\<acute>pd = pde_Ptr pd\<rbrace> \<inter> \<lbrace>\<acute>asid = asid\<rbrace>} \<inter> {s'. \<forall>t rv. ret__unsigned_long_' t = from_bool rv \<longrightarrow> root_switched_'_update (\<lambda>_. ret__unsigned_long_' t) (s'\<lparr>globals := globals t\<rparr>) \<in> {s. pstart_'_update (\<lambda>_. pstart) (end_'_update (\<lambda>_. end) (start_'_update (\<lambda>_. start) (s\<lparr>invLabel___int_' := invLabel___int\<rparr>))) \<in> \<lbrace>flushtype_relation typ \<acute>invLabel___int\<rbrace> \<inter> \<lbrace>\<acute>start = vs\<rbrace> \<inter> \<lbrace>\<acute>end = ve\<rbrace> \<inter> \<lbrace>\<acute>pstart = ps\<rbrace>} \<inter> {s'. \<forall>ta rv. dc rv (xfdc ta) \<longrightarrow> s'\<lparr>globals := globals ta\<rparr> \<in> {s. (s \<in> \<lbrace>\<^bsup>t\<^esup>ret__unsigned_long \<noteq> 0\<rbrace> \<longrightarrow> s \<in> {s. \<forall>rv. ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr rv \<longrightarrow> s \<in> {s. tcb_'_update (\<lambda>_. ksCurThread_' (globals s)) s \<in> UNIV \<inter> \<lbrace>\<acute>tcb = tcb_ptr_to_ctcb_ptr rv\<rbrace>}}) \<and> (s \<notin> \<lbrace>\<^bsup>t\<^esup>ret__unsigned_long \<noteq> 0\<rbrace> \<longrightarrow> s \<in> UNIV)}}}) \<and> (s \<notin> \<lbrace>start < end\<rbrace> \<longrightarrow> s \<in> UNIV)} proof (prove)
goal (2 subgoals):
 1. \<And>invLabel___int pstart end start asida pda \<sigma>. \<lbrakk>flushtype_relation typ invLabel___int; pstart = ps; end = ve; start = vs; asida = asid; pda = pde_Ptr pd\<rbrakk> \<Longrightarrow> {s. True \<and> s \<in> UNIV \<and> (\<sigma>, s) \<in> rf_sr} \<subseteq> {s. \<exists>(rv, \<sigma>')\<in>fst (return () \<sigma>). (\<sigma>', s\<lparr>ret__unsigned_long_' := SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE, global_exn_var_' := Return\<rparr>) \<in> rf_sr \<and> (K (K (\<lambda>_. False)) \<currency> dc) (Inr rv) (liftxf errstate id (K ()) ret__unsigned_long_' (s\<lparr>ret__unsigned_long_' := SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE, global_exn_var_' := Return\<rparr>))}
 2. \<And>invLabel___int pstart end start asida pda s s'. \<lbrakk>flushtype_relation typ invLabel___int; pstart = ps; end = ve; start = vs; asida = asid; pda = pde_Ptr pd; (s, s') \<in> rf_sr; (invs' and (\<lambda>y. asid \<le> mask local.asid_bits) and (\<lambda>s. ps \<le> ps + (ve - vs) \<and> vs && mask 5 = ps && mask 5 \<and> unat (ve - vs) \<le> gsMaxObjectSize s)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. vs < ve \<longrightarrow> (invs' and (\<lambda>s. asid \<le> mask local.asid_bits) and (\<lambda>s. (vs \<le> ve \<and> ps \<le> ps + (ve - vs) \<and> vs && mask 5 = ps && mask 5 \<and> unat (ve - vs) \<le> gsMaxObjectSize s) \<and> invs' s \<and> cur_tcb' s)) s) and (\<lambda>s. \<not> vs < ve \<longrightarrow> True)) s \<and> s' \<in> {s. (s \<in> \<lbrace>start < end\<rbrace> \<longrightarrow> s \<in> {s. asid_'_update (\<lambda>_. asida) (pd_'_update (\<lambda>_. pda) s) \<in> UNIV \<inter> \<lbrace>\<acute>pd = pde_Ptr pd\<rbrace> \<inter> \<lbrace>\<acute>asid = asid\<rbrace>} \<inter> {s'. \<forall>t rv. ret__unsigned_long_' t = from_bool rv \<longrightarrow> root_switched_'_update (\<lambda>_. ret__unsigned_long_' t) (s'\<lparr>globals := globals t\<rparr>) \<in> {s. pstart_'_update (\<lambda>_. pstart) (end_'_update (\<lambda>_. end) (start_'_update (\<lambda>_. start) (s\<lparr>invLabel___int_' := invLabel___int\<rparr>))) \<in> \<lbrace>flushtype_relation typ \<acute>invLabel___int\<rbrace> \<inter> \<lbrace>\<acute>start = vs\<rbrace> \<inter> \<lbrace>\<acute>end = ve\<rbrace> \<inter> \<lbrace>\<acute>pstart = ps\<rbrace>} \<inter> {s'. \<forall>ta rv. dc rv (xfdc ta) \<longrightarrow> s'\<lparr>globals := globals ta\<rparr> \<in> {s. (s \<in> \<lbrace>\<^bsup>t\<^esup>ret__unsigned_long \<noteq> 0\<rbrace> \<longrightarrow> s \<in> {s. \<forall>rv. ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr rv \<longrightarrow> s \<in> {s. tcb_'_update (\<lambda>_. ksCurThread_' (globals s)) s \<in> UNIV \<inter> \<lbrace>\<acute>tcb = tcb_ptr_to_ctcb_ptr rv\<rbrace>}}) \<and> (s \<notin> \<lbrace>\<^bsup>t\<^esup>ret__unsigned_long \<noteq> 0\<rbrace> \<longrightarrow> s \<in> UNIV)}}}) \<and> (s \<notin> \<lbrace>start < end\<rbrace> \<longrightarrow> s \<in> UNIV)} proof (prove)
goal (1 subgoal):
 1. \<And>invLabel___int pstart end start asida pda s s'. \<lbrakk>flushtype_relation typ invLabel___int; pstart = ps; end = ve; start = vs; asida = asid; pda = pde_Ptr pd; (s, s') \<in> rf_sr; (invs' and (\<lambda>y. asid \<le> mask local.asid_bits) and (\<lambda>s. ps \<le> ps + (ve - vs) \<and> vs && mask 5 = ps && mask 5 \<and> unat (ve - vs) \<le> gsMaxObjectSize s)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. vs < ve \<longrightarrow> (invs' and (\<lambda>s. asid \<le> mask local.asid_bits) and (\<lambda>s. (vs \<le> ve \<and> ps \<le> ps + (ve - vs) \<and> vs && mask 5 = ps && mask 5 \<and> unat (ve - vs) \<le> gsMaxObjectSize s) \<and> invs' s \<and> cur_tcb' s)) s) and (\<lambda>s. \<not> vs < ve \<longrightarrow> True)) s \<and> s' \<in> {s. (s \<in> \<lbrace>start < end\<rbrace> \<longrightarrow> s \<in> {s. asid_'_update (\<lambda>_. asida) (pd_'_update (\<lambda>_. pda) s) \<in> UNIV \<inter> \<lbrace>\<acute>pd = pde_Ptr pd\<rbrace> \<inter> \<lbrace>\<acute>asid = asid\<rbrace>} \<inter> {s'. \<forall>t rv. ret__unsigned_long_' t = from_bool rv \<longrightarrow> root_switched_'_update (\<lambda>_. ret__unsigned_long_' t) (s'\<lparr>globals := globals t\<rparr>) \<in> {s. pstart_'_update (\<lambda>_. pstart) (end_'_update (\<lambda>_. end) (start_'_update (\<lambda>_. start) (s\<lparr>invLabel___int_' := invLabel___int\<rparr>))) \<in> \<lbrace>flushtype_relation typ \<acute>invLabel___int\<rbrace> \<inter> \<lbrace>\<acute>start = vs\<rbrace> \<inter> \<lbrace>\<acute>end = ve\<rbrace> \<inter> \<lbrace>\<acute>pstart = ps\<rbrace>} \<inter> {s'. \<forall>ta rv. dc rv (xfdc ta) \<longrightarrow> s'\<lparr>globals := globals ta\<rparr> \<in> {s. (s \<in> \<lbrace>\<^bsup>t\<^esup>ret__unsigned_long \<noteq> 0\<rbrace> \<longrightarrow> s \<in> {s. \<forall>rv. ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr rv \<longrightarrow> s \<in> {s. tcb_'_update (\<lambda>_. ksCurThread_' (globals s)) s \<in> UNIV \<inter> \<lbrace>\<acute>tcb = tcb_ptr_to_ctcb_ptr rv\<rbrace>}}) \<and> (s \<notin> \<lbrace>\<^bsup>t\<^esup>ret__unsigned_long \<noteq> 0\<rbrace> \<longrightarrow> s \<in> UNIV)}}}) \<and> (s \<notin> \<lbrace>start < end\<rbrace> \<longrightarrow> s \<in> UNIV)} proof (prove)
goal:
No subgoals!