theory VSpace_C

lemma flushSpace_ccorres:
  "ccorres dc xfdc (valid_pde_mappings' and (\<lambda>_. asid \<le> mask asid_bits)) (UNIV \<inter> {s. asid_' s = asid}) []
       (flushSpace asid) (Call flushSpace_'proc)" apply (rule ccorres_gen_asm) apply (cinit lift: asid_') apply (ctac (no_vcg) add: loadHWASID_ccorres) apply (ctac (no_vcg) add: cleanCaches_PoU_ccorres) apply csymbr apply (simp add: case_option_If2) apply (rule_tac Q=\<top> and Q'=\<top> in ccorres_if_cond_throws2) apply (clarsimp simp: Collect_const_mem pde_stored_asid_def) apply (simp add: if_split_eq1 to_bool_def) apply (rule ccorres_return_void_C) apply csymbr apply (clarsimp simp: pde_stored_asid_def) apply (case_tac "to_bool (stored_asid_valid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C))") prefer 2 apply clarsimp apply clarsimp apply (case_tac "pde_get_tag stored_hw_asid___struct_pde_C = scast pde_pde_invalid") prefer 2 apply clarsimp apply clarsimp apply (rule ccorres_call,
             rule invalidateTranslationASID_ccorres,
             simp+)[1] apply vcg apply wp+ apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres dc xfdc (valid_pde_mappings' and (\<lambda>_. asid \<le> mask local.asid_bits)) (UNIV \<inter> \<lbrace>\<acute>asid = asid\<rbrace>) [] (flushSpace asid) (Call flushSpace_'proc) proof (prove)
goal (1 subgoal):
 1. asid \<le> mask local.asid_bits \<Longrightarrow> ccorres dc xfdc valid_pde_mappings' (UNIV \<inter> \<lbrace>\<acute>asid = asid\<rbrace>) [] (flushSpace asid) (Call flushSpace_'proc) proof (prove)
goal (2 subgoals):
 1. \<And>asida. \<lbrakk>asid \<le> mask local.asid_bits; asida = asid\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q198 asida) (?Q'198 asida) [SKIP] (do maybe_hw_asid <- loadHWASID asid;
y <- doMachineOp cleanCaches_PoU;
case maybe_hw_asid of None \<Rightarrow> return () | Some hw_asid \<Rightarrow> doMachineOp $ invalidateLocalTLB_ASID hw_asid
od) (\<acute>stored_hw_asid___struct_pde_C :== CALL loadHWASID_'proc(asida);;
(CALL cleanCaches_PoU_'proc();;
(\<acute>ret__unsigned :== CALL pde_pde_invalid_get_stored_asid_valid_'proc(\<acute>stored_hw_asid___struct_pde_C);;
(IF \<acute>ret__unsigned = 0 THEN
  return_void_C
FI;;
(\<acute>ret__unsigned :== CALL pde_pde_invalid_get_stored_hw_asid_'proc(\<acute>stored_hw_asid___struct_pde_C);;
CALL invalidateTranslationASID_'proc(UCAST(32 \<rightarrow> 8) \<acute>ret__unsigned))))))
 2. \<And>asida s s'. \<lbrakk>asid \<le> mask local.asid_bits; asida = asid; (s, s') \<in> rf_sr; valid_pde_mappings' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q198 asida s \<and> s' \<in> ?Q'198 asida proof (prove)
goal (3 subgoals):
 1. \<And>asida rv stored_hw_asid___struct_pde_C. \<lbrakk>asid \<le> mask local.asid_bits; asida = asid; rv = pde_stored_asid stored_hw_asid___struct_pde_C \<and> pde_get_tag stored_hw_asid___struct_pde_C = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q206 asida rv) (?Q'206 asida rv stored_hw_asid___struct_pde_C) [SKIP] (do y <- doMachineOp cleanCaches_PoU;
case rv of None \<Rightarrow> return () | Some hw_asid \<Rightarrow> doMachineOp $ invalidateLocalTLB_ASID hw_asid
od) (CALL cleanCaches_PoU_'proc();;
(\<acute>ret__unsigned :== CALL pde_pde_invalid_get_stored_asid_valid_'proc(stored_hw_asid___struct_pde_C);;
(IF \<acute>ret__unsigned = 0 THEN
  return_void_C
FI;;
(\<acute>ret__unsigned :== CALL pde_pde_invalid_get_stored_hw_asid_'proc(stored_hw_asid___struct_pde_C);;
CALL invalidateTranslationASID_'proc(UCAST(32 \<rightarrow> 8) \<acute>ret__unsigned)))))
 2. \<And>asida. \<lbrakk>asid \<le> mask local.asid_bits; asida = asid\<rbrakk> \<Longrightarrow> \<lbrace>?R206 asida\<rbrace> loadHWASID asid \<lbrace>?Q206 asida\<rbrace>
 3. \<And>asida s s'. \<lbrakk>asid \<le> mask local.asid_bits; asida = asid; (s, s') \<in> rf_sr; valid_pde_mappings' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (valid_pde_mappings' and (\<lambda>_. asid \<le> mask local.asid_bits) and ?R206 asida) s \<and> s' \<in> {s. asid_'_update (\<lambda>_. asida) s \<in> UNIV \<inter> \<lbrace>\<acute>asid = asid\<rbrace>} \<inter> {s'. \<forall>t rv. rv = pde_stored_asid (ret__struct_pde_C_' t) \<and> pde_get_tag (ret__struct_pde_C_' t) = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid \<longrightarrow> s'\<lparr>globals := globals t, stored_hw_asid___struct_pde_C_' := ret__struct_pde_C_' t\<rparr> \<in> ?Q'206 asida rv (ret__struct_pde_C_' t)} proof (prove)
goal (4 subgoals):
 1. \<And>asida rv stored_hw_asid___struct_pde_C rva xfdca. \<lbrakk>asid \<le> mask local.asid_bits; asida = asid; rv = pde_stored_asid stored_hw_asid___struct_pde_C \<and> pde_get_tag stored_hw_asid___struct_pde_C = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid; dc rva xfdca\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q352 asida rv stored_hw_asid___struct_pde_C rva) (?Q'352 asida rv stored_hw_asid___struct_pde_C rva xfdca) [SKIP] (case rv of None \<Rightarrow> return () | Some hw_asid \<Rightarrow> doMachineOp $ invalidateLocalTLB_ASID hw_asid) (\<acute>ret__unsigned :== CALL pde_pde_invalid_get_stored_asid_valid_'proc(stored_hw_asid___struct_pde_C);;
(IF \<acute>ret__unsigned = 0 THEN
  return_void_C
FI;;
(\<acute>ret__unsigned :== CALL pde_pde_invalid_get_stored_hw_asid_'proc(stored_hw_asid___struct_pde_C);;
CALL invalidateTranslationASID_'proc(UCAST(32 \<rightarrow> 8) \<acute>ret__unsigned))))
 2. \<And>asida rv stored_hw_asid___struct_pde_C. \<lbrakk>asid \<le> mask local.asid_bits; asida = asid; rv = pde_stored_asid stored_hw_asid___struct_pde_C \<and> pde_get_tag stored_hw_asid___struct_pde_C = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid\<rbrakk> \<Longrightarrow> \<lbrace>?R354 asida rv\<rbrace> doMachineOp cleanCaches_PoU \<lbrace>?Q352 asida rv stored_hw_asid___struct_pde_C\<rbrace>
 3. \<And>asida. \<lbrakk>asid \<le> mask local.asid_bits; asida = asid\<rbrakk> \<Longrightarrow> \<lbrace>?R206 asida\<rbrace> loadHWASID asid \<lbrace>\<lambda>rv. (\<lambda>_. True) and ?R354 asida rv\<rbrace>
 4. \<And>asida s s'. \<lbrakk>asid \<le> mask local.asid_bits; asida = asid; (s, s') \<in> rf_sr; valid_pde_mappings' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (valid_pde_mappings' and (\<lambda>_. asid \<le> mask local.asid_bits) and ?R206 asida) s \<and> s' \<in> {s. asid_'_update (\<lambda>_. asida) s \<in> UNIV \<inter> \<lbrace>\<acute>asid = asid\<rbrace>} \<inter> {s'. \<forall>t rv. rv = pde_stored_asid (ret__struct_pde_C_' t) \<and> pde_get_tag (ret__struct_pde_C_' t) = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid \<longrightarrow> s'\<lparr>globals := globals t, stored_hw_asid___struct_pde_C_' := ret__struct_pde_C_' t\<rparr> \<in> {s. s \<in> UNIV} \<inter> {s'. \<forall>ta rva. dc rva (xfdc ta) \<longrightarrow> s'\<lparr>globals := globals ta\<rparr> \<in> ?Q'352 asida rv (ret__struct_pde_C_' t) rva (xfdc ta)}} proof (prove)
goal (4 subgoals):
 1. \<And>asida stored_hw_asid___struct_pde_C rva xfdca ret__unsigned. \<lbrakk>asid \<le> mask local.asid_bits; asida = asid; pde_get_tag stored_hw_asid___struct_pde_C = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid; dc rva xfdca; ret__unsigned = stored_asid_valid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C)\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q352 asida (pde_stored_asid stored_hw_asid___struct_pde_C) stored_hw_asid___struct_pde_C rva) (?G'379 asida (pde_stored_asid stored_hw_asid___struct_pde_C) stored_hw_asid___struct_pde_C rva xfdca ret__unsigned) [SKIP] (case pde_stored_asid stored_hw_asid___struct_pde_C of None \<Rightarrow> return () | Some hw_asid \<Rightarrow> doMachineOp $ invalidateLocalTLB_ASID hw_asid) (IF ret__unsigned = 0 THEN
  return_void_C
FI;;
(\<acute>ret__unsigned :== CALL pde_pde_invalid_get_stored_hw_asid_'proc(stored_hw_asid___struct_pde_C);;
CALL invalidateTranslationASID_'proc(UCAST(32 \<rightarrow> 8) \<acute>ret__unsigned)))
 2. \<And>asida rv stored_hw_asid___struct_pde_C. \<lbrakk>asid \<le> mask local.asid_bits; asida = asid; rv = pde_stored_asid stored_hw_asid___struct_pde_C \<and> pde_get_tag stored_hw_asid___struct_pde_C = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid\<rbrakk> \<Longrightarrow> \<lbrace>?R354 asida rv\<rbrace> doMachineOp cleanCaches_PoU \<lbrace>?Q352 asida rv stored_hw_asid___struct_pde_C\<rbrace>
 3. \<And>asida. \<lbrakk>asid \<le> mask local.asid_bits; asida = asid\<rbrakk> \<Longrightarrow> \<lbrace>?R206 asida\<rbrace> loadHWASID asid \<lbrace>\<lambda>rv. (\<lambda>_. True) and ?R354 asida rv\<rbrace>
 4. \<And>asida s s'. \<lbrakk>asid \<le> mask local.asid_bits; asida = asid; (s, s') \<in> rf_sr; valid_pde_mappings' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (valid_pde_mappings' and (\<lambda>_. asid \<le> mask local.asid_bits) and ?R206 asida) s \<and> s' \<in> {s. asid_'_update (\<lambda>_. asida) s \<in> UNIV \<inter> \<lbrace>\<acute>asid = asid\<rbrace>} \<inter> {s'. \<forall>t rv. rv = pde_stored_asid (ret__struct_pde_C_' t) \<and> pde_get_tag (ret__struct_pde_C_' t) = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid \<longrightarrow> s'\<lparr>globals := globals t, stored_hw_asid___struct_pde_C_' := ret__struct_pde_C_' t\<rparr> \<in> {s. s \<in> UNIV} \<inter> {s'. \<forall>ta rva. dc rva (xfdc ta) \<longrightarrow> s'\<lparr>globals := globals ta\<rparr> \<in> {s. \<forall>v v'. v = stored_asid_valid_CL (pde_pde_invalid_lift (pde_' (pde_'_update (\<lambda>_. ret__struct_pde_C_' t) s))) \<longrightarrow> s\<lparr>ret__unsigned_' := v\<rparr> \<in> {s. s \<in> ?G'379 asida rv (ret__struct_pde_C_' t) rva (xfdc ta) v}} \<inter> {s. pde_get_tag (pde_' (pde_'_update (\<lambda>_. ret__struct_pde_C_' t) s)) = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid}}} proof (prove)
goal (4 subgoals):
 1. \<And>asida stored_hw_asid___struct_pde_C xfdca ret__unsigned. \<lbrakk>asid \<le> mask local.asid_bits; asida = asid; pde_get_tag stored_hw_asid___struct_pde_C = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid; ret__unsigned = stored_asid_valid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C)\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q352 asid (pde_stored_asid stored_hw_asid___struct_pde_C) stored_hw_asid___struct_pde_C ()) (?G'379 asid (pde_stored_asid stored_hw_asid___struct_pde_C) stored_hw_asid___struct_pde_C () xfdca (stored_asid_valid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C))) [SKIP] (if \<exists>y. pde_stored_asid stored_hw_asid___struct_pde_C = Some y then doMachineOp $ invalidateLocalTLB_ASID (the (pde_stored_asid stored_hw_asid___struct_pde_C)) else return ()) (Cond (if stored_asid_valid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C) = 0 then UNIV else {}) return_void_C SKIP;;
(\<acute>ret__unsigned :== CALL pde_pde_invalid_get_stored_hw_asid_'proc(stored_hw_asid___struct_pde_C);;
CALL invalidateTranslationASID_'proc(UCAST(32 \<rightarrow> 8) \<acute>ret__unsigned)))
 2. \<And>asida rv stored_hw_asid___struct_pde_C. \<lbrakk>asid \<le> mask local.asid_bits; asida = asid; rv = pde_stored_asid stored_hw_asid___struct_pde_C \<and> pde_get_tag stored_hw_asid___struct_pde_C = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid\<rbrakk> \<Longrightarrow> \<lbrace>?R354 asida rv\<rbrace> doMachineOp cleanCaches_PoU \<lbrace>?Q352 asida rv stored_hw_asid___struct_pde_C\<rbrace>
 3. \<And>asida. \<lbrakk>asid \<le> mask local.asid_bits; asida = asid\<rbrakk> \<Longrightarrow> \<lbrace>?R206 asida\<rbrace> loadHWASID asid \<lbrace>\<lambda>rv. (\<lambda>_. True) and ?R354 asida rv\<rbrace>
 4. \<And>asida s s'. \<lbrakk>asid \<le> mask local.asid_bits; asida = asid; (s, s') \<in> rf_sr; valid_pde_mappings' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (valid_pde_mappings' and (\<lambda>_. asid \<le> mask local.asid_bits) and ?R206 asida) s \<and> s' \<in> {s. asid_'_update (\<lambda>_. asida) s \<in> UNIV \<inter> \<lbrace>\<acute>asid = asid\<rbrace>} \<inter> {s'. \<forall>t rv. rv = pde_stored_asid (ret__struct_pde_C_' t) \<and> pde_get_tag (ret__struct_pde_C_' t) = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid \<longrightarrow> s'\<lparr>globals := globals t, stored_hw_asid___struct_pde_C_' := ret__struct_pde_C_' t\<rparr> \<in> {s. s \<in> UNIV} \<inter> {s'. \<forall>ta rva. dc rva (xfdc ta) \<longrightarrow> s'\<lparr>globals := globals ta\<rparr> \<in> {s. \<forall>v v'. v = stored_asid_valid_CL (pde_pde_invalid_lift (pde_' (pde_'_update (\<lambda>_. ret__struct_pde_C_' t) s))) \<longrightarrow> s\<lparr>ret__unsigned_' := v\<rparr> \<in> {s. s \<in> ?G'379 asida rv (ret__struct_pde_C_' t) rva (xfdc ta) v}} \<inter> {s. pde_get_tag (pde_' (pde_'_update (\<lambda>_. ret__struct_pde_C_' t) s)) = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid}}} proof (prove)
goal (7 subgoals):
 1. \<And>asida stored_hw_asid___struct_pde_C xfdc ret__unsigned. \<lbrakk>asid \<le> mask local.asid_bits; asida = asid; pde_get_tag stored_hw_asid___struct_pde_C = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid; ret__unsigned = stored_asid_valid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C)\<rbrakk> \<Longrightarrow> \<forall>s s'. (s, s') \<in> rf_sr \<and> True \<and> True \<longrightarrow> (\<nexists>y. pde_stored_asid stored_hw_asid___struct_pde_C = Some y) = (s' \<in> (if stored_asid_valid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C) = 0 then UNIV else {}))
 2. \<And>asida stored_hw_asid___struct_pde_C xfdca ret__unsigned. \<lbrakk>asid \<le> mask local.asid_bits; asida = asid; pde_get_tag stored_hw_asid___struct_pde_C = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid; ret__unsigned = stored_asid_valid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C); \<nexists>y. pde_stored_asid stored_hw_asid___struct_pde_C = Some y\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?R479 asid (pde_stored_asid stored_hw_asid___struct_pde_C) stored_hw_asid___struct_pde_C ()) (?R'475 asid (pde_stored_asid stored_hw_asid___struct_pde_C) stored_hw_asid___struct_pde_C () xfdca (stored_asid_valid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C))) [SKIP] (return ()) return_void_C
 3. \<And>asida stored_hw_asid___struct_pde_C xfdca ret__unsigned. \<lbrakk>asid \<le> mask local.asid_bits; asida = asid; pde_get_tag stored_hw_asid___struct_pde_C = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid; ret__unsigned = stored_asid_valid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C); \<exists>y. pde_stored_asid stored_hw_asid___struct_pde_C = Some y\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?U477 asid (pde_stored_asid stored_hw_asid___struct_pde_C) stored_hw_asid___struct_pde_C ()) (?U'471 asid (pde_stored_asid stored_hw_asid___struct_pde_C) stored_hw_asid___struct_pde_C () xfdca (stored_asid_valid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C))) [SKIP] (doMachineOp $ invalidateLocalTLB_ASID (the (pde_stored_asid stored_hw_asid___struct_pde_C))) (\<acute>ret__unsigned :== CALL pde_pde_invalid_get_stored_hw_asid_'proc(stored_hw_asid___struct_pde_C);;
CALL invalidateTranslationASID_'proc(UCAST(32 \<rightarrow> 8) \<acute>ret__unsigned))
 4. \<And>asida stored_hw_asid___struct_pde_C xfdc ret__unsigned. \<lbrakk>asid \<le> mask local.asid_bits; asida = asid; pde_get_tag stored_hw_asid___struct_pde_C = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid; ret__unsigned = stored_asid_valid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?PT'473 asid (pde_stored_asid stored_hw_asid___struct_pde_C) stored_hw_asid___struct_pde_C () xfdc (stored_asid_valid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C))) return_void_C {},UNIV
 5. \<And>asida rv stored_hw_asid___struct_pde_C. \<lbrakk>asid \<le> mask local.asid_bits; asida = asid; rv = pde_stored_asid stored_hw_asid___struct_pde_C \<and> pde_get_tag stored_hw_asid___struct_pde_C = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid\<rbrakk> \<Longrightarrow> \<lbrace>?R354 asida rv\<rbrace> doMachineOp cleanCaches_PoU \<lbrace>\<lambda>a. (\<lambda>_. True) and (\<lambda>s. (\<nexists>y. rv = Some y) \<longrightarrow> ?R479 asida rv stored_hw_asid___struct_pde_C a s) and (\<lambda>s. (\<exists>y. rv = Some y) \<longrightarrow> ?U477 asida rv stored_hw_asid___struct_pde_C a s)\<rbrace>
 6. \<And>asida. \<lbrakk>asid \<le> mask local.asid_bits; asida = asid\<rbrakk> \<Longrightarrow> \<lbrace>?R206 asida\<rbrace> loadHWASID asid \<lbrace>\<lambda>rv. (\<lambda>_. True) and ?R354 asida rv\<rbrace>
 7. \<And>asida s s'. \<lbrakk>asid \<le> mask local.asid_bits; asida = asid; (s, s') \<in> rf_sr; valid_pde_mappings' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (valid_pde_mappings' and (\<lambda>_. asid \<le> mask local.asid_bits) and ?R206 asida) s \<and> s' \<in> {s. asid_'_update (\<lambda>_. asida) s \<in> UNIV \<inter> \<lbrace>\<acute>asid = asid\<rbrace>} \<inter> {s'. \<forall>t rv. rv = pde_stored_asid (ret__struct_pde_C_' t) \<and> pde_get_tag (ret__struct_pde_C_' t) = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid \<longrightarrow> s'\<lparr>globals := globals t, stored_hw_asid___struct_pde_C_' := ret__struct_pde_C_' t\<rparr> \<in> {s. s \<in> UNIV} \<inter> {s'. \<forall>ta rva. dc rva (xfdc ta) \<longrightarrow> s'\<lparr>globals := globals ta\<rparr> \<in> {s. \<forall>v v'. v = stored_asid_valid_CL (pde_pde_invalid_lift (pde_' (pde_'_update (\<lambda>_. ret__struct_pde_C_' t) s))) \<longrightarrow> s\<lparr>ret__unsigned_' := v\<rparr> \<in> {s. s \<in> \<lbrace>True\<rbrace> \<inter> {s. (s \<in> (if v = 0 then UNIV else {}) \<longrightarrow> s \<in> ?R'475 asida rv (ret__struct_pde_C_' t) rva (xfdc ta) v \<inter> ?PT'473 asida rv (ret__struct_pde_C_' t) rva (xfdc ta) v) \<and> (s \<notin> (if v = 0 then UNIV else {}) \<longrightarrow> s \<in> ?U'471 asida rv (ret__struct_pde_C_' t) rva (xfdc ta) v)}}} \<inter> {s. pde_get_tag (pde_' (pde_'_update (\<lambda>_. ret__struct_pde_C_' t) s)) = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid}}} proof (prove)
goal (7 subgoals):
 1. \<And>stored_hw_asid___struct_pde_C s s'. \<lbrakk>asid \<le> mask local.asid_bits; pde_get_tag stored_hw_asid___struct_pde_C = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid; (s, s') \<in> rf_sr\<rbrakk> \<Longrightarrow> ((if to_bool (stored_asid_valid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C)) then Some (UCAST(32 \<rightarrow> 8) (stored_hw_asid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C))) else None) = None) = (stored_asid_valid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C) = 0)
 2. \<And>asida stored_hw_asid___struct_pde_C xfdca ret__unsigned. \<lbrakk>asid \<le> mask local.asid_bits; asida = asid; pde_get_tag stored_hw_asid___struct_pde_C = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid; ret__unsigned = stored_asid_valid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C); \<nexists>y. pde_stored_asid stored_hw_asid___struct_pde_C = Some y\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?R479 asid (pde_stored_asid stored_hw_asid___struct_pde_C) stored_hw_asid___struct_pde_C ()) (?R'475 asid (pde_stored_asid stored_hw_asid___struct_pde_C) stored_hw_asid___struct_pde_C () xfdca (stored_asid_valid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C))) [SKIP] (return ()) return_void_C
 3. \<And>asida stored_hw_asid___struct_pde_C xfdca ret__unsigned. \<lbrakk>asid \<le> mask local.asid_bits; asida = asid; pde_get_tag stored_hw_asid___struct_pde_C = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid; ret__unsigned = stored_asid_valid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C); \<exists>y. pde_stored_asid stored_hw_asid___struct_pde_C = Some y\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?U477 asid (pde_stored_asid stored_hw_asid___struct_pde_C) stored_hw_asid___struct_pde_C ()) (?U'471 asid (pde_stored_asid stored_hw_asid___struct_pde_C) stored_hw_asid___struct_pde_C () xfdca (stored_asid_valid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C))) [SKIP] (doMachineOp $ invalidateLocalTLB_ASID (the (pde_stored_asid stored_hw_asid___struct_pde_C))) (\<acute>ret__unsigned :== CALL pde_pde_invalid_get_stored_hw_asid_'proc(stored_hw_asid___struct_pde_C);;
CALL invalidateTranslationASID_'proc(UCAST(32 \<rightarrow> 8) \<acute>ret__unsigned))
 4. \<And>asida stored_hw_asid___struct_pde_C xfdc ret__unsigned. \<lbrakk>asid \<le> mask local.asid_bits; asida = asid; pde_get_tag stored_hw_asid___struct_pde_C = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid; ret__unsigned = stored_asid_valid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?PT'473 asid (pde_stored_asid stored_hw_asid___struct_pde_C) stored_hw_asid___struct_pde_C () xfdc (stored_asid_valid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C))) return_void_C {},UNIV
 5. \<And>asida rv stored_hw_asid___struct_pde_C. \<lbrakk>asid \<le> mask local.asid_bits; asida = asid; rv = pde_stored_asid stored_hw_asid___struct_pde_C \<and> pde_get_tag stored_hw_asid___struct_pde_C = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid\<rbrakk> \<Longrightarrow> \<lbrace>?R354 asida rv\<rbrace> doMachineOp cleanCaches_PoU \<lbrace>\<lambda>a. (\<lambda>_. True) and (\<lambda>s. (\<nexists>y. rv = Some y) \<longrightarrow> ?R479 asida rv stored_hw_asid___struct_pde_C a s) and (\<lambda>s. (\<exists>y. rv = Some y) \<longrightarrow> ?U477 asida rv stored_hw_asid___struct_pde_C a s)\<rbrace>
 6. \<And>asida. \<lbrakk>asid \<le> mask local.asid_bits; asida = asid\<rbrakk> \<Longrightarrow> \<lbrace>?R206 asida\<rbrace> loadHWASID asid \<lbrace>\<lambda>rv. (\<lambda>_. True) and ?R354 asida rv\<rbrace>
 7. \<And>asida s s'. \<lbrakk>asid \<le> mask local.asid_bits; asida = asid; (s, s') \<in> rf_sr; valid_pde_mappings' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (valid_pde_mappings' and (\<lambda>_. asid \<le> mask local.asid_bits) and ?R206 asida) s \<and> s' \<in> {s. asid_'_update (\<lambda>_. asida) s \<in> UNIV \<inter> \<lbrace>\<acute>asid = asid\<rbrace>} \<inter> {s'. \<forall>t rv. rv = pde_stored_asid (ret__struct_pde_C_' t) \<and> pde_get_tag (ret__struct_pde_C_' t) = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid \<longrightarrow> s'\<lparr>globals := globals t, stored_hw_asid___struct_pde_C_' := ret__struct_pde_C_' t\<rparr> \<in> {s. s \<in> UNIV} \<inter> {s'. \<forall>ta rva. dc rva (xfdc ta) \<longrightarrow> s'\<lparr>globals := globals ta\<rparr> \<in> {s. \<forall>v v'. v = stored_asid_valid_CL (pde_pde_invalid_lift (pde_' (pde_'_update (\<lambda>_. ret__struct_pde_C_' t) s))) \<longrightarrow> s\<lparr>ret__unsigned_' := v\<rparr> \<in> {s. s \<in> \<lbrace>True\<rbrace> \<inter> {s. (s \<in> (if v = 0 then UNIV else {}) \<longrightarrow> s \<in> ?R'475 asida rv (ret__struct_pde_C_' t) rva (xfdc ta) v \<inter> ?PT'473 asida rv (ret__struct_pde_C_' t) rva (xfdc ta) v) \<and> (s \<notin> (if v = 0 then UNIV else {}) \<longrightarrow> s \<in> ?U'471 asida rv (ret__struct_pde_C_' t) rva (xfdc ta) v)}}} \<inter> {s. pde_get_tag (pde_' (pde_'_update (\<lambda>_. ret__struct_pde_C_' t) s)) = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid}}} proof (prove)
goal (6 subgoals):
 1. \<And>asida stored_hw_asid___struct_pde_C xfdca ret__unsigned. \<lbrakk>asid \<le> mask local.asid_bits; asida = asid; pde_get_tag stored_hw_asid___struct_pde_C = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid; ret__unsigned = stored_asid_valid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C); \<nexists>y. pde_stored_asid stored_hw_asid___struct_pde_C = Some y\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?R479 asid (pde_stored_asid stored_hw_asid___struct_pde_C) stored_hw_asid___struct_pde_C ()) (?R'475 asid (pde_stored_asid stored_hw_asid___struct_pde_C) stored_hw_asid___struct_pde_C () xfdca (stored_asid_valid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C))) [SKIP] (return ()) return_void_C
 2. \<And>asida stored_hw_asid___struct_pde_C xfdca ret__unsigned. \<lbrakk>asid \<le> mask local.asid_bits; asida = asid; pde_get_tag stored_hw_asid___struct_pde_C = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid; ret__unsigned = stored_asid_valid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C); \<exists>y. pde_stored_asid stored_hw_asid___struct_pde_C = Some y\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?U477 asid (pde_stored_asid stored_hw_asid___struct_pde_C) stored_hw_asid___struct_pde_C ()) (?U'471 asid (pde_stored_asid stored_hw_asid___struct_pde_C) stored_hw_asid___struct_pde_C () xfdca (stored_asid_valid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C))) [SKIP] (doMachineOp $ invalidateLocalTLB_ASID (the (pde_stored_asid stored_hw_asid___struct_pde_C))) (\<acute>ret__unsigned :== CALL pde_pde_invalid_get_stored_hw_asid_'proc(stored_hw_asid___struct_pde_C);;
CALL invalidateTranslationASID_'proc(UCAST(32 \<rightarrow> 8) \<acute>ret__unsigned))
 3. \<And>asida stored_hw_asid___struct_pde_C xfdc ret__unsigned. \<lbrakk>asid \<le> mask local.asid_bits; asida = asid; pde_get_tag stored_hw_asid___struct_pde_C = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid; ret__unsigned = stored_asid_valid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?PT'473 asid (pde_stored_asid stored_hw_asid___struct_pde_C) stored_hw_asid___struct_pde_C () xfdc (stored_asid_valid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C))) return_void_C {},UNIV
 4. \<And>asida rv stored_hw_asid___struct_pde_C. \<lbrakk>asid \<le> mask local.asid_bits; asida = asid; rv = pde_stored_asid stored_hw_asid___struct_pde_C \<and> pde_get_tag stored_hw_asid___struct_pde_C = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid\<rbrakk> \<Longrightarrow> \<lbrace>?R354 asida rv\<rbrace> doMachineOp cleanCaches_PoU \<lbrace>\<lambda>a. (\<lambda>_. True) and (\<lambda>s. (\<nexists>y. rv = Some y) \<longrightarrow> ?R479 asida rv stored_hw_asid___struct_pde_C a s) and (\<lambda>s. (\<exists>y. rv = Some y) \<longrightarrow> ?U477 asida rv stored_hw_asid___struct_pde_C a s)\<rbrace>
 5. \<And>asida. \<lbrakk>asid \<le> mask local.asid_bits; asida = asid\<rbrakk> \<Longrightarrow> \<lbrace>?R206 asida\<rbrace> loadHWASID asid \<lbrace>\<lambda>rv. (\<lambda>_. True) and ?R354 asida rv\<rbrace>
 6. \<And>asida s s'. \<lbrakk>asid \<le> mask local.asid_bits; asida = asid; (s, s') \<in> rf_sr; valid_pde_mappings' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (valid_pde_mappings' and (\<lambda>_. asid \<le> mask local.asid_bits) and ?R206 asida) s \<and> s' \<in> {s. asid_'_update (\<lambda>_. asida) s \<in> UNIV \<inter> \<lbrace>\<acute>asid = asid\<rbrace>} \<inter> {s'. \<forall>t rv. rv = pde_stored_asid (ret__struct_pde_C_' t) \<and> pde_get_tag (ret__struct_pde_C_' t) = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid \<longrightarrow> s'\<lparr>globals := globals t, stored_hw_asid___struct_pde_C_' := ret__struct_pde_C_' t\<rparr> \<in> {s. s \<in> UNIV} \<inter> {s'. \<forall>ta rva. dc rva (xfdc ta) \<longrightarrow> s'\<lparr>globals := globals ta\<rparr> \<in> {s. \<forall>v v'. v = stored_asid_valid_CL (pde_pde_invalid_lift (pde_' (pde_'_update (\<lambda>_. ret__struct_pde_C_' t) s))) \<longrightarrow> s\<lparr>ret__unsigned_' := v\<rparr> \<in> {s. s \<in> \<lbrace>True\<rbrace> \<inter> {s. (s \<in> (if v = 0 then UNIV else {}) \<longrightarrow> s \<in> ?R'475 asida rv (ret__struct_pde_C_' t) rva (xfdc ta) v \<inter> ?PT'473 asida rv (ret__struct_pde_C_' t) rva (xfdc ta) v) \<and> (s \<notin> (if v = 0 then UNIV else {}) \<longrightarrow> s \<in> ?U'471 asida rv (ret__struct_pde_C_' t) rva (xfdc ta) v)}}} \<inter> {s. pde_get_tag (pde_' (pde_'_update (\<lambda>_. ret__struct_pde_C_' t) s)) = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid}}} proof (prove)
goal (5 subgoals):
 1. \<And>asida stored_hw_asid___struct_pde_C xfdca ret__unsigned. \<lbrakk>asid \<le> mask local.asid_bits; asida = asid; pde_get_tag stored_hw_asid___struct_pde_C = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid; ret__unsigned = stored_asid_valid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C); \<exists>y. pde_stored_asid stored_hw_asid___struct_pde_C = Some y\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?U477 asid (pde_stored_asid stored_hw_asid___struct_pde_C) stored_hw_asid___struct_pde_C ()) (?U'471 asid (pde_stored_asid stored_hw_asid___struct_pde_C) stored_hw_asid___struct_pde_C () xfdca (stored_asid_valid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C))) [SKIP] (doMachineOp $ invalidateLocalTLB_ASID (the (pde_stored_asid stored_hw_asid___struct_pde_C))) (\<acute>ret__unsigned :== CALL pde_pde_invalid_get_stored_hw_asid_'proc(stored_hw_asid___struct_pde_C);;
CALL invalidateTranslationASID_'proc(UCAST(32 \<rightarrow> 8) \<acute>ret__unsigned))
 2. \<And>asida stored_hw_asid___struct_pde_C xfdc ret__unsigned. \<lbrakk>asid \<le> mask local.asid_bits; asida = asid; pde_get_tag stored_hw_asid___struct_pde_C = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid; ret__unsigned = stored_asid_valid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?PT'473 asid (pde_stored_asid stored_hw_asid___struct_pde_C) stored_hw_asid___struct_pde_C () xfdc (stored_asid_valid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C))) return_void_C {},UNIV
 3. \<And>asida rv stored_hw_asid___struct_pde_C. \<lbrakk>asid \<le> mask local.asid_bits; asida = asid; rv = pde_stored_asid stored_hw_asid___struct_pde_C \<and> pde_get_tag stored_hw_asid___struct_pde_C = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid\<rbrakk> \<Longrightarrow> \<lbrace>?R354 asida rv\<rbrace> doMachineOp cleanCaches_PoU \<lbrace>\<lambda>a. (\<lambda>_. True) and (\<lambda>s. (\<nexists>y. rv = Some y) \<longrightarrow> True) and (\<lambda>s. (\<exists>y. rv = Some y) \<longrightarrow> ?U477 asida rv stored_hw_asid___struct_pde_C a s)\<rbrace>
 4. \<And>asida. \<lbrakk>asid \<le> mask local.asid_bits; asida = asid\<rbrakk> \<Longrightarrow> \<lbrace>?R206 asida\<rbrace> loadHWASID asid \<lbrace>\<lambda>rv. (\<lambda>_. True) and ?R354 asida rv\<rbrace>
 5. \<And>asida s s'. \<lbrakk>asid \<le> mask local.asid_bits; asida = asid; (s, s') \<in> rf_sr; valid_pde_mappings' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (valid_pde_mappings' and (\<lambda>_. asid \<le> mask local.asid_bits) and ?R206 asida) s \<and> s' \<in> {s. asid_'_update (\<lambda>_. asida) s \<in> UNIV \<inter> \<lbrace>\<acute>asid = asid\<rbrace>} \<inter> {s'. \<forall>t rv. rv = pde_stored_asid (ret__struct_pde_C_' t) \<and> pde_get_tag (ret__struct_pde_C_' t) = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid \<longrightarrow> s'\<lparr>globals := globals t, stored_hw_asid___struct_pde_C_' := ret__struct_pde_C_' t\<rparr> \<in> {s. s \<in> UNIV} \<inter> {s'. \<forall>ta rva. dc rva (xfdc ta) \<longrightarrow> s'\<lparr>globals := globals ta\<rparr> \<in> {s. \<forall>v v'. v = stored_asid_valid_CL (pde_pde_invalid_lift (pde_' (pde_'_update (\<lambda>_. ret__struct_pde_C_' t) s))) \<longrightarrow> s\<lparr>ret__unsigned_' := v\<rparr> \<in> {s. s \<in> \<lbrace>True\<rbrace> \<inter> {s. (s \<in> (if v = 0 then UNIV else {}) \<longrightarrow> s \<in> UNIV \<inter> ?PT'473 asida rv (ret__struct_pde_C_' t) rva (xfdc ta) v) \<and> (s \<notin> (if v = 0 then UNIV else {}) \<longrightarrow> s \<in> ?U'471 asida rv (ret__struct_pde_C_' t) rva (xfdc ta) v)}}} \<inter> {s. pde_get_tag (pde_' (pde_'_update (\<lambda>_. ret__struct_pde_C_' t) s)) = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid}}} proof (prove)
goal (5 subgoals):
 1. \<And>asida stored_hw_asid___struct_pde_C xfdca ret__unsigneda ret__unsigned. \<lbrakk>asid \<le> mask local.asid_bits; asida = asid; pde_get_tag stored_hw_asid___struct_pde_C = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid; ret__unsigneda = stored_asid_valid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C); \<exists>y. pde_stored_asid stored_hw_asid___struct_pde_C = Some y; ret__unsigned = stored_hw_asid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C)\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?U477 asid (pde_stored_asid stored_hw_asid___struct_pde_C) stored_hw_asid___struct_pde_C ()) (?G'500 asid (pde_stored_asid stored_hw_asid___struct_pde_C) stored_hw_asid___struct_pde_C () xfdca (stored_asid_valid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C)) ret__unsigned) [SKIP] (doMachineOp $ invalidateLocalTLB_ASID (the (pde_stored_asid stored_hw_asid___struct_pde_C))) (CALL invalidateTranslationASID_'proc(UCAST(32 \<rightarrow> 8) ret__unsigned))
 2. \<And>asida stored_hw_asid___struct_pde_C xfdc ret__unsigned. \<lbrakk>asid \<le> mask local.asid_bits; asida = asid; pde_get_tag stored_hw_asid___struct_pde_C = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid; ret__unsigned = stored_asid_valid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?PT'473 asid (pde_stored_asid stored_hw_asid___struct_pde_C) stored_hw_asid___struct_pde_C () xfdc (stored_asid_valid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C))) return_void_C {},UNIV
 3. \<And>asida rv stored_hw_asid___struct_pde_C. \<lbrakk>asid \<le> mask local.asid_bits; asida = asid; rv = pde_stored_asid stored_hw_asid___struct_pde_C \<and> pde_get_tag stored_hw_asid___struct_pde_C = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid\<rbrakk> \<Longrightarrow> \<lbrace>?R354 asida rv\<rbrace> doMachineOp cleanCaches_PoU \<lbrace>\<lambda>a. (\<lambda>_. True) and (\<lambda>s. (\<nexists>y. rv = Some y) \<longrightarrow> True) and (\<lambda>s. (\<exists>y. rv = Some y) \<longrightarrow> ?U477 asida rv stored_hw_asid___struct_pde_C a s)\<rbrace>
 4. \<And>asida. \<lbrakk>asid \<le> mask local.asid_bits; asida = asid\<rbrakk> \<Longrightarrow> \<lbrace>?R206 asida\<rbrace> loadHWASID asid \<lbrace>\<lambda>rv. (\<lambda>_. True) and ?R354 asida rv\<rbrace>
 5. \<And>asida s s'. \<lbrakk>asid \<le> mask local.asid_bits; asida = asid; (s, s') \<in> rf_sr; valid_pde_mappings' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (valid_pde_mappings' and (\<lambda>_. asid \<le> mask local.asid_bits) and ?R206 asida) s \<and> s' \<in> {s. asid_'_update (\<lambda>_. asida) s \<in> UNIV \<inter> \<lbrace>\<acute>asid = asid\<rbrace>} \<inter> {s'. \<forall>t rv. rv = pde_stored_asid (ret__struct_pde_C_' t) \<and> pde_get_tag (ret__struct_pde_C_' t) = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid \<longrightarrow> s'\<lparr>globals := globals t, stored_hw_asid___struct_pde_C_' := ret__struct_pde_C_' t\<rparr> \<in> {s. s \<in> UNIV} \<inter> {s'. \<forall>ta rva. dc rva (xfdc ta) \<longrightarrow> s'\<lparr>globals := globals ta\<rparr> \<in> {s. \<forall>v v'. v = stored_asid_valid_CL (pde_pde_invalid_lift (pde_' (pde_'_update (\<lambda>_. ret__struct_pde_C_' t) s))) \<longrightarrow> s\<lparr>ret__unsigned_' := v\<rparr> \<in> {s. s \<in> \<lbrace>True\<rbrace> \<inter> {s. (s \<in> (if v = 0 then UNIV else {}) \<longrightarrow> s \<in> UNIV \<inter> ?PT'473 asida rv (ret__struct_pde_C_' t) rva (xfdc ta) v) \<and> (s \<notin> (if v = 0 then UNIV else {}) \<longrightarrow> s \<in> {s. \<forall>va v'. va = stored_hw_asid_CL (pde_pde_invalid_lift (pde_' (pde_'_update (\<lambda>_. ret__struct_pde_C_' t) s))) \<longrightarrow> s\<lparr>ret__unsigned_' := va\<rparr> \<in> {s. s \<in> ?G'500 asida rv (ret__struct_pde_C_' t) rva (xfdc ta) v va}} \<inter> {s. pde_get_tag (pde_' (pde_'_update (\<lambda>_. ret__struct_pde_C_' t) s)) = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid})}}} \<inter> {s. pde_get_tag (pde_' (pde_'_update (\<lambda>_. ret__struct_pde_C_' t) s)) = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid}}} proof (prove)
goal (5 subgoals):
 1. \<And>stored_hw_asid___struct_pde_C xfdca y. \<lbrakk>asid \<le> mask local.asid_bits; pde_get_tag stored_hw_asid___struct_pde_C = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid; (if to_bool (stored_asid_valid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C)) then Some (UCAST(32 \<rightarrow> 8) (stored_hw_asid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C))) else None) = Some y\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?U477 asid (Some y) stored_hw_asid___struct_pde_C ()) (?G'500 asid (Some y) stored_hw_asid___struct_pde_C () xfdca (stored_asid_valid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C)) (stored_hw_asid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C))) [SKIP] (doMachineOp (invalidateLocalTLB_ASID y)) (CALL invalidateTranslationASID_'proc(UCAST(32 \<rightarrow> 8) (stored_hw_asid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C))))
 2. \<And>asida stored_hw_asid___struct_pde_C xfdc ret__unsigned. \<lbrakk>asid \<le> mask local.asid_bits; asida = asid; pde_get_tag stored_hw_asid___struct_pde_C = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid; ret__unsigned = stored_asid_valid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?PT'473 asid (pde_stored_asid stored_hw_asid___struct_pde_C) stored_hw_asid___struct_pde_C () xfdc (stored_asid_valid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C))) return_void_C {},UNIV
 3. \<And>asida rv stored_hw_asid___struct_pde_C. \<lbrakk>asid \<le> mask local.asid_bits; asida = asid; rv = pde_stored_asid stored_hw_asid___struct_pde_C \<and> pde_get_tag stored_hw_asid___struct_pde_C = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid\<rbrakk> \<Longrightarrow> \<lbrace>?R354 asida rv\<rbrace> doMachineOp cleanCaches_PoU \<lbrace>\<lambda>a. (\<lambda>_. True) and (\<lambda>s. (\<nexists>y. rv = Some y) \<longrightarrow> True) and (\<lambda>s. (\<exists>y. rv = Some y) \<longrightarrow> ?U477 asida rv stored_hw_asid___struct_pde_C a s)\<rbrace>
 4. \<And>asida. \<lbrakk>asid \<le> mask local.asid_bits; asida = asid\<rbrakk> \<Longrightarrow> \<lbrace>?R206 asida\<rbrace> loadHWASID asid \<lbrace>\<lambda>rv. (\<lambda>_. True) and ?R354 asida rv\<rbrace>
 5. \<And>asida s s'. \<lbrakk>asid \<le> mask local.asid_bits; asida = asid; (s, s') \<in> rf_sr; valid_pde_mappings' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (valid_pde_mappings' and (\<lambda>_. asid \<le> mask local.asid_bits) and ?R206 asida) s \<and> s' \<in> {s. asid_'_update (\<lambda>_. asida) s \<in> UNIV \<inter> \<lbrace>\<acute>asid = asid\<rbrace>} \<inter> {s'. \<forall>t rv. rv = pde_stored_asid (ret__struct_pde_C_' t) \<and> pde_get_tag (ret__struct_pde_C_' t) = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid \<longrightarrow> s'\<lparr>globals := globals t, stored_hw_asid___struct_pde_C_' := ret__struct_pde_C_' t\<rparr> \<in> {s. s \<in> UNIV} \<inter> {s'. \<forall>ta rva. dc rva (xfdc ta) \<longrightarrow> s'\<lparr>globals := globals ta\<rparr> \<in> {s. \<forall>v v'. v = stored_asid_valid_CL (pde_pde_invalid_lift (pde_' (pde_'_update (\<lambda>_. ret__struct_pde_C_' t) s))) \<longrightarrow> s\<lparr>ret__unsigned_' := v\<rparr> \<in> {s. s \<in> \<lbrace>True\<rbrace> \<inter> {s. (s \<in> (if v = 0 then UNIV else {}) \<longrightarrow> s \<in> UNIV \<inter> ?PT'473 asida rv (ret__struct_pde_C_' t) rva (xfdc ta) v) \<and> (s \<notin> (if v = 0 then UNIV else {}) \<longrightarrow> s \<in> {s. \<forall>va v'. va = stored_hw_asid_CL (pde_pde_invalid_lift (pde_' (pde_'_update (\<lambda>_. ret__struct_pde_C_' t) s))) \<longrightarrow> s\<lparr>ret__unsigned_' := va\<rparr> \<in> {s. s \<in> ?G'500 asida rv (ret__struct_pde_C_' t) rva (xfdc ta) v va}} \<inter> {s. pde_get_tag (pde_' (pde_'_update (\<lambda>_. ret__struct_pde_C_' t) s)) = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid})}}} \<inter> {s. pde_get_tag (pde_' (pde_'_update (\<lambda>_. ret__struct_pde_C_' t) s)) = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid}}} proof (prove)
goal (6 subgoals):
 1. \<And>stored_hw_asid___struct_pde_C xfdca y. \<lbrakk>asid \<le> mask local.asid_bits; pde_get_tag stored_hw_asid___struct_pde_C = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid; (if to_bool (stored_asid_valid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C)) then Some (UCAST(32 \<rightarrow> 8) (stored_hw_asid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C))) else None) = Some y; to_bool (stored_asid_valid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C))\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?U477 asid (Some y) stored_hw_asid___struct_pde_C ()) (?G'500 asid (Some y) stored_hw_asid___struct_pde_C () xfdca (stored_asid_valid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C)) (stored_hw_asid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C))) [SKIP] (doMachineOp (invalidateLocalTLB_ASID y)) (CALL invalidateTranslationASID_'proc(UCAST(32 \<rightarrow> 8) (stored_hw_asid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C))))
 2. \<And>stored_hw_asid___struct_pde_C xfdca y. \<lbrakk>asid \<le> mask local.asid_bits; pde_get_tag stored_hw_asid___struct_pde_C = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid; (if to_bool (stored_asid_valid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C)) then Some (UCAST(32 \<rightarrow> 8) (stored_hw_asid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C))) else None) = Some y; \<not> to_bool (stored_asid_valid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C))\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?U477 asid (Some y) stored_hw_asid___struct_pde_C ()) (?G'500 asid (Some y) stored_hw_asid___struct_pde_C () xfdca (stored_asid_valid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C)) (stored_hw_asid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C))) [SKIP] (doMachineOp (invalidateLocalTLB_ASID y)) (CALL invalidateTranslationASID_'proc(UCAST(32 \<rightarrow> 8) (stored_hw_asid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C))))
 3. \<And>asida stored_hw_asid___struct_pde_C xfdc ret__unsigned. \<lbrakk>asid \<le> mask local.asid_bits; asida = asid; pde_get_tag stored_hw_asid___struct_pde_C = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid; ret__unsigned = stored_asid_valid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?PT'473 asid (pde_stored_asid stored_hw_asid___struct_pde_C) stored_hw_asid___struct_pde_C () xfdc (stored_asid_valid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C))) return_void_C {},UNIV
 4. \<And>asida rv stored_hw_asid___struct_pde_C. \<lbrakk>asid \<le> mask local.asid_bits; asida = asid; rv = pde_stored_asid stored_hw_asid___struct_pde_C \<and> pde_get_tag stored_hw_asid___struct_pde_C = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid\<rbrakk> \<Longrightarrow> \<lbrace>?R354 asida rv\<rbrace> doMachineOp cleanCaches_PoU \<lbrace>\<lambda>a. (\<lambda>_. True) and (\<lambda>s. (\<nexists>y. rv = Some y) \<longrightarrow> True) and (\<lambda>s. (\<exists>y. rv = Some y) \<longrightarrow> ?U477 asida rv stored_hw_asid___struct_pde_C a s)\<rbrace>
 5. \<And>asida. \<lbrakk>asid \<le> mask local.asid_bits; asida = asid\<rbrakk> \<Longrightarrow> \<lbrace>?R206 asida\<rbrace> loadHWASID asid \<lbrace>\<lambda>rv. (\<lambda>_. True) and ?R354 asida rv\<rbrace>
 6. \<And>asida s s'. \<lbrakk>asid \<le> mask local.asid_bits; asida = asid; (s, s') \<in> rf_sr; valid_pde_mappings' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (valid_pde_mappings' and (\<lambda>_. asid \<le> mask local.asid_bits) and ?R206 asida) s \<and> s' \<in> {s. asid_'_update (\<lambda>_. asida) s \<in> UNIV \<inter> \<lbrace>\<acute>asid = asid\<rbrace>} \<inter> {s'. \<forall>t rv. rv = pde_stored_asid (ret__struct_pde_C_' t) \<and> pde_get_tag (ret__struct_pde_C_' t) = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid \<longrightarrow> s'\<lparr>globals := globals t, stored_hw_asid___struct_pde_C_' := ret__struct_pde_C_' t\<rparr> \<in> {s. s \<in> UNIV} \<inter> {s'. \<forall>ta rva. dc rva (xfdc ta) \<longrightarrow> s'\<lparr>globals := globals ta\<rparr> \<in> {s. \<forall>v v'. v = stored_asid_valid_CL (pde_pde_invalid_lift (pde_' (pde_'_update (\<lambda>_. ret__struct_pde_C_' t) s))) \<longrightarrow> s\<lparr>ret__unsigned_' := v\<rparr> \<in> {s. s \<in> \<lbrace>True\<rbrace> \<inter> {s. (s \<in> (if v = 0 then UNIV else {}) \<longrightarrow> s \<in> UNIV \<inter> ?PT'473 asida rv (ret__struct_pde_C_' t) rva (xfdc ta) v) \<and> (s \<notin> (if v = 0 then UNIV else {}) \<longrightarrow> s \<in> {s. \<forall>va v'. va = stored_hw_asid_CL (pde_pde_invalid_lift (pde_' (pde_'_update (\<lambda>_. ret__struct_pde_C_' t) s))) \<longrightarrow> s\<lparr>ret__unsigned_' := va\<rparr> \<in> {s. s \<in> ?G'500 asida rv (ret__struct_pde_C_' t) rva (xfdc ta) v va}} \<inter> {s. pde_get_tag (pde_' (pde_'_update (\<lambda>_. ret__struct_pde_C_' t) s)) = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid})}}} \<inter> {s. pde_get_tag (pde_' (pde_'_update (\<lambda>_. ret__struct_pde_C_' t) s)) = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid}}} proof (prove)
goal (6 subgoals):
 1. \<And>stored_hw_asid___struct_pde_C xfdca y. \<lbrakk>asid \<le> mask local.asid_bits; pde_get_tag stored_hw_asid___struct_pde_C = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid; (if to_bool (stored_asid_valid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C)) then Some (UCAST(32 \<rightarrow> 8) (stored_hw_asid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C))) else None) = Some y; \<not> to_bool (stored_asid_valid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C))\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?U477 asid (Some y) stored_hw_asid___struct_pde_C ()) (?G'500 asid (Some y) stored_hw_asid___struct_pde_C () xfdca (stored_asid_valid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C)) (stored_hw_asid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C))) [SKIP] (doMachineOp (invalidateLocalTLB_ASID y)) (CALL invalidateTranslationASID_'proc(UCAST(32 \<rightarrow> 8) (stored_hw_asid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C))))
 2. \<And>stored_hw_asid___struct_pde_C xfdca y. \<lbrakk>asid \<le> mask local.asid_bits; pde_get_tag stored_hw_asid___struct_pde_C = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid; (if to_bool (stored_asid_valid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C)) then Some (UCAST(32 \<rightarrow> 8) (stored_hw_asid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C))) else None) = Some y; to_bool (stored_asid_valid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C))\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?U477 asid (Some y) stored_hw_asid___struct_pde_C ()) (?G'500 asid (Some y) stored_hw_asid___struct_pde_C () xfdca (stored_asid_valid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C)) (stored_hw_asid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C))) [SKIP] (doMachineOp (invalidateLocalTLB_ASID y)) (CALL invalidateTranslationASID_'proc(UCAST(32 \<rightarrow> 8) (stored_hw_asid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C))))
 3. \<And>asida stored_hw_asid___struct_pde_C xfdc ret__unsigned. \<lbrakk>asid \<le> mask local.asid_bits; asida = asid; pde_get_tag stored_hw_asid___struct_pde_C = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid; ret__unsigned = stored_asid_valid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?PT'473 asid (pde_stored_asid stored_hw_asid___struct_pde_C) stored_hw_asid___struct_pde_C () xfdc (stored_asid_valid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C))) return_void_C {},UNIV
 4. \<And>asida rv stored_hw_asid___struct_pde_C. \<lbrakk>asid \<le> mask local.asid_bits; asida = asid; rv = pde_stored_asid stored_hw_asid___struct_pde_C \<and> pde_get_tag stored_hw_asid___struct_pde_C = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid\<rbrakk> \<Longrightarrow> \<lbrace>?R354 asida rv\<rbrace> doMachineOp cleanCaches_PoU \<lbrace>\<lambda>a. (\<lambda>_. True) and (\<lambda>s. (\<nexists>y. rv = Some y) \<longrightarrow> True) and (\<lambda>s. (\<exists>y. rv = Some y) \<longrightarrow> ?U477 asida rv stored_hw_asid___struct_pde_C a s)\<rbrace>
 5. \<And>asida. \<lbrakk>asid \<le> mask local.asid_bits; asida = asid\<rbrakk> \<Longrightarrow> \<lbrace>?R206 asida\<rbrace> loadHWASID asid \<lbrace>\<lambda>rv. (\<lambda>_. True) and ?R354 asida rv\<rbrace>
 6. \<And>asida s s'. \<lbrakk>asid \<le> mask local.asid_bits; asida = asid; (s, s') \<in> rf_sr; valid_pde_mappings' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (valid_pde_mappings' and (\<lambda>_. asid \<le> mask local.asid_bits) and ?R206 asida) s \<and> s' \<in> {s. asid_'_update (\<lambda>_. asida) s \<in> UNIV \<inter> \<lbrace>\<acute>asid = asid\<rbrace>} \<inter> {s'. \<forall>t rv. rv = pde_stored_asid (ret__struct_pde_C_' t) \<and> pde_get_tag (ret__struct_pde_C_' t) = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid \<longrightarrow> s'\<lparr>globals := globals t, stored_hw_asid___struct_pde_C_' := ret__struct_pde_C_' t\<rparr> \<in> {s. s \<in> UNIV} \<inter> {s'. \<forall>ta rva. dc rva (xfdc ta) \<longrightarrow> s'\<lparr>globals := globals ta\<rparr> \<in> {s. \<forall>v v'. v = stored_asid_valid_CL (pde_pde_invalid_lift (pde_' (pde_'_update (\<lambda>_. ret__struct_pde_C_' t) s))) \<longrightarrow> s\<lparr>ret__unsigned_' := v\<rparr> \<in> {s. s \<in> \<lbrace>True\<rbrace> \<inter> {s. (s \<in> (if v = 0 then UNIV else {}) \<longrightarrow> s \<in> UNIV \<inter> ?PT'473 asida rv (ret__struct_pde_C_' t) rva (xfdc ta) v) \<and> (s \<notin> (if v = 0 then UNIV else {}) \<longrightarrow> s \<in> {s. \<forall>va v'. va = stored_hw_asid_CL (pde_pde_invalid_lift (pde_' (pde_'_update (\<lambda>_. ret__struct_pde_C_' t) s))) \<longrightarrow> s\<lparr>ret__unsigned_' := va\<rparr> \<in> {s. s \<in> ?G'500 asida rv (ret__struct_pde_C_' t) rva (xfdc ta) v va}} \<inter> {s. pde_get_tag (pde_' (pde_'_update (\<lambda>_. ret__struct_pde_C_' t) s)) = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid})}}} \<inter> {s. pde_get_tag (pde_' (pde_'_update (\<lambda>_. ret__struct_pde_C_' t) s)) = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid}}} proof (prove)
goal (5 subgoals):
 1. \<And>stored_hw_asid___struct_pde_C xfdca y. \<lbrakk>asid \<le> mask local.asid_bits; pde_get_tag stored_hw_asid___struct_pde_C = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid; (if to_bool (stored_asid_valid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C)) then Some (UCAST(32 \<rightarrow> 8) (stored_hw_asid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C))) else None) = Some y; to_bool (stored_asid_valid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C))\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?U477 asid (Some y) stored_hw_asid___struct_pde_C ()) (?G'500 asid (Some y) stored_hw_asid___struct_pde_C () xfdca (stored_asid_valid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C)) (stored_hw_asid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C))) [SKIP] (doMachineOp (invalidateLocalTLB_ASID y)) (CALL invalidateTranslationASID_'proc(UCAST(32 \<rightarrow> 8) (stored_hw_asid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C))))
 2. \<And>asida stored_hw_asid___struct_pde_C xfdc ret__unsigned. \<lbrakk>asid \<le> mask local.asid_bits; asida = asid; pde_get_tag stored_hw_asid___struct_pde_C = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid; ret__unsigned = stored_asid_valid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?PT'473 asid (pde_stored_asid stored_hw_asid___struct_pde_C) stored_hw_asid___struct_pde_C () xfdc (stored_asid_valid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C))) return_void_C {},UNIV
 3. \<And>asida rv stored_hw_asid___struct_pde_C. \<lbrakk>asid \<le> mask local.asid_bits; asida = asid; rv = pde_stored_asid stored_hw_asid___struct_pde_C \<and> pde_get_tag stored_hw_asid___struct_pde_C = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid\<rbrakk> \<Longrightarrow> \<lbrace>?R354 asida rv\<rbrace> doMachineOp cleanCaches_PoU \<lbrace>\<lambda>a. (\<lambda>_. True) and (\<lambda>s. (\<nexists>y. rv = Some y) \<longrightarrow> True) and (\<lambda>s. (\<exists>y. rv = Some y) \<longrightarrow> ?U477 asida rv stored_hw_asid___struct_pde_C a s)\<rbrace>
 4. \<And>asida. \<lbrakk>asid \<le> mask local.asid_bits; asida = asid\<rbrakk> \<Longrightarrow> \<lbrace>?R206 asida\<rbrace> loadHWASID asid \<lbrace>\<lambda>rv. (\<lambda>_. True) and ?R354 asida rv\<rbrace>
 5. \<And>asida s s'. \<lbrakk>asid \<le> mask local.asid_bits; asida = asid; (s, s') \<in> rf_sr; valid_pde_mappings' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (valid_pde_mappings' and (\<lambda>_. asid \<le> mask local.asid_bits) and ?R206 asida) s \<and> s' \<in> {s. asid_'_update (\<lambda>_. asida) s \<in> UNIV \<inter> \<lbrace>\<acute>asid = asid\<rbrace>} \<inter> {s'. \<forall>t rv. rv = pde_stored_asid (ret__struct_pde_C_' t) \<and> pde_get_tag (ret__struct_pde_C_' t) = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid \<longrightarrow> s'\<lparr>globals := globals t, stored_hw_asid___struct_pde_C_' := ret__struct_pde_C_' t\<rparr> \<in> {s. s \<in> UNIV} \<inter> {s'. \<forall>ta rva. dc rva (xfdc ta) \<longrightarrow> s'\<lparr>globals := globals ta\<rparr> \<in> {s. \<forall>v v'. v = stored_asid_valid_CL (pde_pde_invalid_lift (pde_' (pde_'_update (\<lambda>_. ret__struct_pde_C_' t) s))) \<longrightarrow> s\<lparr>ret__unsigned_' := v\<rparr> \<in> {s. s \<in> \<lbrace>True\<rbrace> \<inter> {s. (s \<in> (if v = 0 then UNIV else {}) \<longrightarrow> s \<in> UNIV \<inter> ?PT'473 asida rv (ret__struct_pde_C_' t) rva (xfdc ta) v) \<and> (s \<notin> (if v = 0 then UNIV else {}) \<longrightarrow> s \<in> {s. \<forall>va v'. va = stored_hw_asid_CL (pde_pde_invalid_lift (pde_' (pde_'_update (\<lambda>_. ret__struct_pde_C_' t) s))) \<longrightarrow> s\<lparr>ret__unsigned_' := va\<rparr> \<in> {s. s \<in> ?G'500 asida rv (ret__struct_pde_C_' t) rva (xfdc ta) v va}} \<inter> {s. pde_get_tag (pde_' (pde_'_update (\<lambda>_. ret__struct_pde_C_' t) s)) = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid})}}} \<inter> {s. pde_get_tag (pde_' (pde_'_update (\<lambda>_. ret__struct_pde_C_' t) s)) = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid}}} proof (prove)
goal (5 subgoals):
 1. \<And>stored_hw_asid___struct_pde_C xfdca. \<lbrakk>asid \<le> mask local.asid_bits; pde_get_tag stored_hw_asid___struct_pde_C = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid; to_bool (stored_asid_valid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C))\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?U477 asid (Some (UCAST(32 \<rightarrow> 8) (stored_hw_asid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C)))) stored_hw_asid___struct_pde_C ()) (?G'500 asid (Some (UCAST(32 \<rightarrow> 8) (stored_hw_asid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C)))) stored_hw_asid___struct_pde_C () xfdca (stored_asid_valid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C)) (stored_hw_asid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C))) [SKIP] (doMachineOp (invalidateLocalTLB_ASID (UCAST(32 \<rightarrow> 8) (stored_hw_asid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C))))) (CALL invalidateTranslationASID_'proc(UCAST(32 \<rightarrow> 8) (stored_hw_asid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C))))
 2. \<And>asida stored_hw_asid___struct_pde_C xfdc ret__unsigned. \<lbrakk>asid \<le> mask local.asid_bits; asida = asid; pde_get_tag stored_hw_asid___struct_pde_C = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid; ret__unsigned = stored_asid_valid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?PT'473 asid (pde_stored_asid stored_hw_asid___struct_pde_C) stored_hw_asid___struct_pde_C () xfdc (stored_asid_valid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C))) return_void_C {},UNIV
 3. \<And>asida rv stored_hw_asid___struct_pde_C. \<lbrakk>asid \<le> mask local.asid_bits; asida = asid; rv = pde_stored_asid stored_hw_asid___struct_pde_C \<and> pde_get_tag stored_hw_asid___struct_pde_C = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid\<rbrakk> \<Longrightarrow> \<lbrace>?R354 asida rv\<rbrace> doMachineOp cleanCaches_PoU \<lbrace>\<lambda>a. (\<lambda>_. True) and (\<lambda>s. (\<nexists>y. rv = Some y) \<longrightarrow> True) and (\<lambda>s. (\<exists>y. rv = Some y) \<longrightarrow> ?U477 asida rv stored_hw_asid___struct_pde_C a s)\<rbrace>
 4. \<And>asida. \<lbrakk>asid \<le> mask local.asid_bits; asida = asid\<rbrakk> \<Longrightarrow> \<lbrace>?R206 asida\<rbrace> loadHWASID asid \<lbrace>\<lambda>rv. (\<lambda>_. True) and ?R354 asida rv\<rbrace>
 5. \<And>asida s s'. \<lbrakk>asid \<le> mask local.asid_bits; asida = asid; (s, s') \<in> rf_sr; valid_pde_mappings' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (valid_pde_mappings' and (\<lambda>_. asid \<le> mask local.asid_bits) and ?R206 asida) s \<and> s' \<in> {s. asid_'_update (\<lambda>_. asida) s \<in> UNIV \<inter> \<lbrace>\<acute>asid = asid\<rbrace>} \<inter> {s'. \<forall>t rv. rv = pde_stored_asid (ret__struct_pde_C_' t) \<and> pde_get_tag (ret__struct_pde_C_' t) = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid \<longrightarrow> s'\<lparr>globals := globals t, stored_hw_asid___struct_pde_C_' := ret__struct_pde_C_' t\<rparr> \<in> {s. s \<in> UNIV} \<inter> {s'. \<forall>ta rva. dc rva (xfdc ta) \<longrightarrow> s'\<lparr>globals := globals ta\<rparr> \<in> {s. \<forall>v v'. v = stored_asid_valid_CL (pde_pde_invalid_lift (pde_' (pde_'_update (\<lambda>_. ret__struct_pde_C_' t) s))) \<longrightarrow> s\<lparr>ret__unsigned_' := v\<rparr> \<in> {s. s \<in> \<lbrace>True\<rbrace> \<inter> {s. (s \<in> (if v = 0 then UNIV else {}) \<longrightarrow> s \<in> UNIV \<inter> ?PT'473 asida rv (ret__struct_pde_C_' t) rva (xfdc ta) v) \<and> (s \<notin> (if v = 0 then UNIV else {}) \<longrightarrow> s \<in> {s. \<forall>va v'. va = stored_hw_asid_CL (pde_pde_invalid_lift (pde_' (pde_'_update (\<lambda>_. ret__struct_pde_C_' t) s))) \<longrightarrow> s\<lparr>ret__unsigned_' := va\<rparr> \<in> {s. s \<in> ?G'500 asida rv (ret__struct_pde_C_' t) rva (xfdc ta) v va}} \<inter> {s. pde_get_tag (pde_' (pde_'_update (\<lambda>_. ret__struct_pde_C_' t) s)) = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid})}}} \<inter> {s. pde_get_tag (pde_' (pde_'_update (\<lambda>_. ret__struct_pde_C_' t) s)) = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid}}} proof (prove)
goal (6 subgoals):
 1. \<And>stored_hw_asid___struct_pde_C xfdca. \<lbrakk>asid \<le> mask local.asid_bits; pde_get_tag stored_hw_asid___struct_pde_C = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid; to_bool (stored_asid_valid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C)); pde_get_tag stored_hw_asid___struct_pde_C = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?U477 asid (Some (UCAST(32 \<rightarrow> 8) (stored_hw_asid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C)))) stored_hw_asid___struct_pde_C ()) (?G'500 asid (Some (UCAST(32 \<rightarrow> 8) (stored_hw_asid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C)))) stored_hw_asid___struct_pde_C () xfdca (stored_asid_valid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C)) (stored_hw_asid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C))) [SKIP] (doMachineOp (invalidateLocalTLB_ASID (UCAST(32 \<rightarrow> 8) (stored_hw_asid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C))))) (CALL invalidateTranslationASID_'proc(UCAST(32 \<rightarrow> 8) (stored_hw_asid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C))))
 2. \<And>stored_hw_asid___struct_pde_C xfdca. \<lbrakk>asid \<le> mask local.asid_bits; pde_get_tag stored_hw_asid___struct_pde_C = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid; to_bool (stored_asid_valid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C)); pde_get_tag stored_hw_asid___struct_pde_C \<noteq> SCAST(32 signed \<rightarrow> 32) pde_pde_invalid\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?U477 asid (Some (UCAST(32 \<rightarrow> 8) (stored_hw_asid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C)))) stored_hw_asid___struct_pde_C ()) (?G'500 asid (Some (UCAST(32 \<rightarrow> 8) (stored_hw_asid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C)))) stored_hw_asid___struct_pde_C () xfdca (stored_asid_valid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C)) (stored_hw_asid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C))) [SKIP] (doMachineOp (invalidateLocalTLB_ASID (UCAST(32 \<rightarrow> 8) (stored_hw_asid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C))))) (CALL invalidateTranslationASID_'proc(UCAST(32 \<rightarrow> 8) (stored_hw_asid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C))))
 3. \<And>asida stored_hw_asid___struct_pde_C xfdc ret__unsigned. \<lbrakk>asid \<le> mask local.asid_bits; asida = asid; pde_get_tag stored_hw_asid___struct_pde_C = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid; ret__unsigned = stored_asid_valid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?PT'473 asid (pde_stored_asid stored_hw_asid___struct_pde_C) stored_hw_asid___struct_pde_C () xfdc (stored_asid_valid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C))) return_void_C {},UNIV
 4. \<And>asida rv stored_hw_asid___struct_pde_C. \<lbrakk>asid \<le> mask local.asid_bits; asida = asid; rv = pde_stored_asid stored_hw_asid___struct_pde_C \<and> pde_get_tag stored_hw_asid___struct_pde_C = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid\<rbrakk> \<Longrightarrow> \<lbrace>?R354 asida rv\<rbrace> doMachineOp cleanCaches_PoU \<lbrace>\<lambda>a. (\<lambda>_. True) and (\<lambda>s. (\<nexists>y. rv = Some y) \<longrightarrow> True) and (\<lambda>s. (\<exists>y. rv = Some y) \<longrightarrow> ?U477 asida rv stored_hw_asid___struct_pde_C a s)\<rbrace>
 5. \<And>asida. \<lbrakk>asid \<le> mask local.asid_bits; asida = asid\<rbrakk> \<Longrightarrow> \<lbrace>?R206 asida\<rbrace> loadHWASID asid \<lbrace>\<lambda>rv. (\<lambda>_. True) and ?R354 asida rv\<rbrace>
 6. \<And>asida s s'. \<lbrakk>asid \<le> mask local.asid_bits; asida = asid; (s, s') \<in> rf_sr; valid_pde_mappings' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (valid_pde_mappings' and (\<lambda>_. asid \<le> mask local.asid_bits) and ?R206 asida) s \<and> s' \<in> {s. asid_'_update (\<lambda>_. asida) s \<in> UNIV \<inter> \<lbrace>\<acute>asid = asid\<rbrace>} \<inter> {s'. \<forall>t rv. rv = pde_stored_asid (ret__struct_pde_C_' t) \<and> pde_get_tag (ret__struct_pde_C_' t) = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid \<longrightarrow> s'\<lparr>globals := globals t, stored_hw_asid___struct_pde_C_' := ret__struct_pde_C_' t\<rparr> \<in> {s. s \<in> UNIV} \<inter> {s'. \<forall>ta rva. dc rva (xfdc ta) \<longrightarrow> s'\<lparr>globals := globals ta\<rparr> \<in> {s. \<forall>v v'. v = stored_asid_valid_CL (pde_pde_invalid_lift (pde_' (pde_'_update (\<lambda>_. ret__struct_pde_C_' t) s))) \<longrightarrow> s\<lparr>ret__unsigned_' := v\<rparr> \<in> {s. s \<in> \<lbrace>True\<rbrace> \<inter> {s. (s \<in> (if v = 0 then UNIV else {}) \<longrightarrow> s \<in> UNIV \<inter> ?PT'473 asida rv (ret__struct_pde_C_' t) rva (xfdc ta) v) \<and> (s \<notin> (if v = 0 then UNIV else {}) \<longrightarrow> s \<in> {s. \<forall>va v'. va = stored_hw_asid_CL (pde_pde_invalid_lift (pde_' (pde_'_update (\<lambda>_. ret__struct_pde_C_' t) s))) \<longrightarrow> s\<lparr>ret__unsigned_' := va\<rparr> \<in> {s. s \<in> ?G'500 asida rv (ret__struct_pde_C_' t) rva (xfdc ta) v va}} \<inter> {s. pde_get_tag (pde_' (pde_'_update (\<lambda>_. ret__struct_pde_C_' t) s)) = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid})}}} \<inter> {s. pde_get_tag (pde_' (pde_'_update (\<lambda>_. ret__struct_pde_C_' t) s)) = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid}}} proof (prove)
goal (6 subgoals):
 1. \<And>stored_hw_asid___struct_pde_C xfdca. \<lbrakk>asid \<le> mask local.asid_bits; pde_get_tag stored_hw_asid___struct_pde_C = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid; to_bool (stored_asid_valid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C)); pde_get_tag stored_hw_asid___struct_pde_C \<noteq> SCAST(32 signed \<rightarrow> 32) pde_pde_invalid\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?U477 asid (Some (UCAST(32 \<rightarrow> 8) (stored_hw_asid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C)))) stored_hw_asid___struct_pde_C ()) (?G'500 asid (Some (UCAST(32 \<rightarrow> 8) (stored_hw_asid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C)))) stored_hw_asid___struct_pde_C () xfdca (stored_asid_valid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C)) (stored_hw_asid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C))) [SKIP] (doMachineOp (invalidateLocalTLB_ASID (UCAST(32 \<rightarrow> 8) (stored_hw_asid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C))))) (CALL invalidateTranslationASID_'proc(UCAST(32 \<rightarrow> 8) (stored_hw_asid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C))))
 2. \<And>stored_hw_asid___struct_pde_C xfdca. \<lbrakk>asid \<le> mask local.asid_bits; pde_get_tag stored_hw_asid___struct_pde_C = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid; to_bool (stored_asid_valid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C)); pde_get_tag stored_hw_asid___struct_pde_C = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?U477 asid (Some (UCAST(32 \<rightarrow> 8) (stored_hw_asid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C)))) stored_hw_asid___struct_pde_C ()) (?G'500 asid (Some (UCAST(32 \<rightarrow> 8) (stored_hw_asid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C)))) stored_hw_asid___struct_pde_C () xfdca (stored_asid_valid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C)) (stored_hw_asid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C))) [SKIP] (doMachineOp (invalidateLocalTLB_ASID (UCAST(32 \<rightarrow> 8) (stored_hw_asid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C))))) (CALL invalidateTranslationASID_'proc(UCAST(32 \<rightarrow> 8) (stored_hw_asid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C))))
 3. \<And>asida stored_hw_asid___struct_pde_C xfdc ret__unsigned. \<lbrakk>asid \<le> mask local.asid_bits; asida = asid; pde_get_tag stored_hw_asid___struct_pde_C = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid; ret__unsigned = stored_asid_valid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?PT'473 asid (pde_stored_asid stored_hw_asid___struct_pde_C) stored_hw_asid___struct_pde_C () xfdc (stored_asid_valid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C))) return_void_C {},UNIV
 4. \<And>asida rv stored_hw_asid___struct_pde_C. \<lbrakk>asid \<le> mask local.asid_bits; asida = asid; rv = pde_stored_asid stored_hw_asid___struct_pde_C \<and> pde_get_tag stored_hw_asid___struct_pde_C = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid\<rbrakk> \<Longrightarrow> \<lbrace>?R354 asida rv\<rbrace> doMachineOp cleanCaches_PoU \<lbrace>\<lambda>a. (\<lambda>_. True) and (\<lambda>s. (\<nexists>y. rv = Some y) \<longrightarrow> True) and (\<lambda>s. (\<exists>y. rv = Some y) \<longrightarrow> ?U477 asida rv stored_hw_asid___struct_pde_C a s)\<rbrace>
 5. \<And>asida. \<lbrakk>asid \<le> mask local.asid_bits; asida = asid\<rbrakk> \<Longrightarrow> \<lbrace>?R206 asida\<rbrace> loadHWASID asid \<lbrace>\<lambda>rv. (\<lambda>_. True) and ?R354 asida rv\<rbrace>
 6. \<And>asida s s'. \<lbrakk>asid \<le> mask local.asid_bits; asida = asid; (s, s') \<in> rf_sr; valid_pde_mappings' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (valid_pde_mappings' and (\<lambda>_. asid \<le> mask local.asid_bits) and ?R206 asida) s \<and> s' \<in> {s. asid_'_update (\<lambda>_. asida) s \<in> UNIV \<inter> \<lbrace>\<acute>asid = asid\<rbrace>} \<inter> {s'. \<forall>t rv. rv = pde_stored_asid (ret__struct_pde_C_' t) \<and> pde_get_tag (ret__struct_pde_C_' t) = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid \<longrightarrow> s'\<lparr>globals := globals t, stored_hw_asid___struct_pde_C_' := ret__struct_pde_C_' t\<rparr> \<in> {s. s \<in> UNIV} \<inter> {s'. \<forall>ta rva. dc rva (xfdc ta) \<longrightarrow> s'\<lparr>globals := globals ta\<rparr> \<in> {s. \<forall>v v'. v = stored_asid_valid_CL (pde_pde_invalid_lift (pde_' (pde_'_update (\<lambda>_. ret__struct_pde_C_' t) s))) \<longrightarrow> s\<lparr>ret__unsigned_' := v\<rparr> \<in> {s. s \<in> \<lbrace>True\<rbrace> \<inter> {s. (s \<in> (if v = 0 then UNIV else {}) \<longrightarrow> s \<in> UNIV \<inter> ?PT'473 asida rv (ret__struct_pde_C_' t) rva (xfdc ta) v) \<and> (s \<notin> (if v = 0 then UNIV else {}) \<longrightarrow> s \<in> {s. \<forall>va v'. va = stored_hw_asid_CL (pde_pde_invalid_lift (pde_' (pde_'_update (\<lambda>_. ret__struct_pde_C_' t) s))) \<longrightarrow> s\<lparr>ret__unsigned_' := va\<rparr> \<in> {s. s \<in> ?G'500 asida rv (ret__struct_pde_C_' t) rva (xfdc ta) v va}} \<inter> {s. pde_get_tag (pde_' (pde_'_update (\<lambda>_. ret__struct_pde_C_' t) s)) = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid})}}} \<inter> {s. pde_get_tag (pde_' (pde_'_update (\<lambda>_. ret__struct_pde_C_' t) s)) = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid}}} proof (prove)
goal (5 subgoals):
 1. \<And>stored_hw_asid___struct_pde_C xfdca. \<lbrakk>asid \<le> mask local.asid_bits; pde_get_tag stored_hw_asid___struct_pde_C = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid; to_bool (stored_asid_valid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C)); pde_get_tag stored_hw_asid___struct_pde_C = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?U477 asid (Some (UCAST(32 \<rightarrow> 8) (stored_hw_asid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C)))) stored_hw_asid___struct_pde_C ()) (?G'500 asid (Some (UCAST(32 \<rightarrow> 8) (stored_hw_asid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C)))) stored_hw_asid___struct_pde_C () xfdca (stored_asid_valid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C)) (stored_hw_asid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C))) [SKIP] (doMachineOp (invalidateLocalTLB_ASID (UCAST(32 \<rightarrow> 8) (stored_hw_asid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C))))) (CALL invalidateTranslationASID_'proc(UCAST(32 \<rightarrow> 8) (stored_hw_asid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C))))
 2. \<And>asida stored_hw_asid___struct_pde_C xfdc ret__unsigned. \<lbrakk>asid \<le> mask local.asid_bits; asida = asid; pde_get_tag stored_hw_asid___struct_pde_C = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid; ret__unsigned = stored_asid_valid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?PT'473 asid (pde_stored_asid stored_hw_asid___struct_pde_C) stored_hw_asid___struct_pde_C () xfdc (stored_asid_valid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C))) return_void_C {},UNIV
 3. \<And>asida rv stored_hw_asid___struct_pde_C. \<lbrakk>asid \<le> mask local.asid_bits; asida = asid; rv = pde_stored_asid stored_hw_asid___struct_pde_C \<and> pde_get_tag stored_hw_asid___struct_pde_C = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid\<rbrakk> \<Longrightarrow> \<lbrace>?R354 asida rv\<rbrace> doMachineOp cleanCaches_PoU \<lbrace>\<lambda>a. (\<lambda>_. True) and (\<lambda>s. (\<nexists>y. rv = Some y) \<longrightarrow> True) and (\<lambda>s. (\<exists>y. rv = Some y) \<longrightarrow> ?U477 asida rv stored_hw_asid___struct_pde_C a s)\<rbrace>
 4. \<And>asida. \<lbrakk>asid \<le> mask local.asid_bits; asida = asid\<rbrakk> \<Longrightarrow> \<lbrace>?R206 asida\<rbrace> loadHWASID asid \<lbrace>\<lambda>rv. (\<lambda>_. True) and ?R354 asida rv\<rbrace>
 5. \<And>asida s s'. \<lbrakk>asid \<le> mask local.asid_bits; asida = asid; (s, s') \<in> rf_sr; valid_pde_mappings' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (valid_pde_mappings' and (\<lambda>_. asid \<le> mask local.asid_bits) and ?R206 asida) s \<and> s' \<in> {s. asid_'_update (\<lambda>_. asida) s \<in> UNIV \<inter> \<lbrace>\<acute>asid = asid\<rbrace>} \<inter> {s'. \<forall>t rv. rv = pde_stored_asid (ret__struct_pde_C_' t) \<and> pde_get_tag (ret__struct_pde_C_' t) = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid \<longrightarrow> s'\<lparr>globals := globals t, stored_hw_asid___struct_pde_C_' := ret__struct_pde_C_' t\<rparr> \<in> {s. s \<in> UNIV} \<inter> {s'. \<forall>ta rva. dc rva (xfdc ta) \<longrightarrow> s'\<lparr>globals := globals ta\<rparr> \<in> {s. \<forall>v v'. v = stored_asid_valid_CL (pde_pde_invalid_lift (pde_' (pde_'_update (\<lambda>_. ret__struct_pde_C_' t) s))) \<longrightarrow> s\<lparr>ret__unsigned_' := v\<rparr> \<in> {s. s \<in> \<lbrace>True\<rbrace> \<inter> {s. (s \<in> (if v = 0 then UNIV else {}) \<longrightarrow> s \<in> UNIV \<inter> ?PT'473 asida rv (ret__struct_pde_C_' t) rva (xfdc ta) v) \<and> (s \<notin> (if v = 0 then UNIV else {}) \<longrightarrow> s \<in> {s. \<forall>va v'. va = stored_hw_asid_CL (pde_pde_invalid_lift (pde_' (pde_'_update (\<lambda>_. ret__struct_pde_C_' t) s))) \<longrightarrow> s\<lparr>ret__unsigned_' := va\<rparr> \<in> {s. s \<in> ?G'500 asida rv (ret__struct_pde_C_' t) rva (xfdc ta) v va}} \<inter> {s. pde_get_tag (pde_' (pde_'_update (\<lambda>_. ret__struct_pde_C_' t) s)) = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid})}}} \<inter> {s. pde_get_tag (pde_' (pde_'_update (\<lambda>_. ret__struct_pde_C_' t) s)) = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid}}} proof (prove)
goal (5 subgoals):
 1. \<And>stored_hw_asid___struct_pde_C xfdca. \<lbrakk>asid \<le> mask local.asid_bits; to_bool (stored_asid_valid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C)); pde_get_tag stored_hw_asid___struct_pde_C = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?U477 asid (Some (UCAST(32 \<rightarrow> 8) (stored_hw_asid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C)))) stored_hw_asid___struct_pde_C ()) (?G'500 asid (Some (UCAST(32 \<rightarrow> 8) (stored_hw_asid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C)))) stored_hw_asid___struct_pde_C () xfdca (stored_asid_valid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C)) (stored_hw_asid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C))) [SKIP] (doMachineOp (invalidateLocalTLB_ASID (UCAST(32 \<rightarrow> 8) (stored_hw_asid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C))))) (CALL invalidateTranslationASID_'proc(UCAST(32 \<rightarrow> 8) (stored_hw_asid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C))))
 2. \<And>asida stored_hw_asid___struct_pde_C xfdc ret__unsigned. \<lbrakk>asid \<le> mask local.asid_bits; asida = asid; pde_get_tag stored_hw_asid___struct_pde_C = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid; ret__unsigned = stored_asid_valid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?PT'473 asid (pde_stored_asid stored_hw_asid___struct_pde_C) stored_hw_asid___struct_pde_C () xfdc (stored_asid_valid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C))) return_void_C {},UNIV
 3. \<And>asida rv stored_hw_asid___struct_pde_C. \<lbrakk>asid \<le> mask local.asid_bits; asida = asid; rv = pde_stored_asid stored_hw_asid___struct_pde_C \<and> pde_get_tag stored_hw_asid___struct_pde_C = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid\<rbrakk> \<Longrightarrow> \<lbrace>?R354 asida rv\<rbrace> doMachineOp cleanCaches_PoU \<lbrace>\<lambda>a. (\<lambda>_. True) and (\<lambda>s. (\<nexists>y. rv = Some y) \<longrightarrow> True) and (\<lambda>s. (\<exists>y. rv = Some y) \<longrightarrow> ?U477 asida rv stored_hw_asid___struct_pde_C a s)\<rbrace>
 4. \<And>asida. \<lbrakk>asid \<le> mask local.asid_bits; asida = asid\<rbrakk> \<Longrightarrow> \<lbrace>?R206 asida\<rbrace> loadHWASID asid \<lbrace>\<lambda>rv. (\<lambda>_. True) and ?R354 asida rv\<rbrace>
 5. \<And>asida s s'. \<lbrakk>asid \<le> mask local.asid_bits; asida = asid; (s, s') \<in> rf_sr; valid_pde_mappings' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (valid_pde_mappings' and (\<lambda>_. asid \<le> mask local.asid_bits) and ?R206 asida) s \<and> s' \<in> {s. asid_'_update (\<lambda>_. asida) s \<in> UNIV \<inter> \<lbrace>\<acute>asid = asid\<rbrace>} \<inter> {s'. \<forall>t rv. rv = pde_stored_asid (ret__struct_pde_C_' t) \<and> pde_get_tag (ret__struct_pde_C_' t) = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid \<longrightarrow> s'\<lparr>globals := globals t, stored_hw_asid___struct_pde_C_' := ret__struct_pde_C_' t\<rparr> \<in> {s. s \<in> UNIV} \<inter> {s'. \<forall>ta rva. dc rva (xfdc ta) \<longrightarrow> s'\<lparr>globals := globals ta\<rparr> \<in> {s. \<forall>v v'. v = stored_asid_valid_CL (pde_pde_invalid_lift (pde_' (pde_'_update (\<lambda>_. ret__struct_pde_C_' t) s))) \<longrightarrow> s\<lparr>ret__unsigned_' := v\<rparr> \<in> {s. s \<in> \<lbrace>True\<rbrace> \<inter> {s. (s \<in> (if v = 0 then UNIV else {}) \<longrightarrow> s \<in> UNIV \<inter> ?PT'473 asida rv (ret__struct_pde_C_' t) rva (xfdc ta) v) \<and> (s \<notin> (if v = 0 then UNIV else {}) \<longrightarrow> s \<in> {s. \<forall>va v'. va = stored_hw_asid_CL (pde_pde_invalid_lift (pde_' (pde_'_update (\<lambda>_. ret__struct_pde_C_' t) s))) \<longrightarrow> s\<lparr>ret__unsigned_' := va\<rparr> \<in> {s. s \<in> ?G'500 asida rv (ret__struct_pde_C_' t) rva (xfdc ta) v va}} \<inter> {s. pde_get_tag (pde_' (pde_'_update (\<lambda>_. ret__struct_pde_C_' t) s)) = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid})}}} \<inter> {s. pde_get_tag (pde_' (pde_'_update (\<lambda>_. ret__struct_pde_C_' t) s)) = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid}}} proof (prove)
goal (4 subgoals):
 1. \<And>asida stored_hw_asid___struct_pde_C xfdc ret__unsigned. \<lbrakk>asid \<le> mask local.asid_bits; asida = asid; pde_get_tag stored_hw_asid___struct_pde_C = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid; ret__unsigned = stored_asid_valid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?PT'473 asid (pde_stored_asid stored_hw_asid___struct_pde_C) stored_hw_asid___struct_pde_C () xfdc (stored_asid_valid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C))) return_void_C {},UNIV
 2. \<And>asida rv stored_hw_asid___struct_pde_C. \<lbrakk>asid \<le> mask local.asid_bits; asida = asid; rv = pde_stored_asid stored_hw_asid___struct_pde_C \<and> pde_get_tag stored_hw_asid___struct_pde_C = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid\<rbrakk> \<Longrightarrow> \<lbrace>?R354 asida rv\<rbrace> doMachineOp cleanCaches_PoU \<lbrace>\<lambda>a. (\<lambda>_. True) and (\<lambda>s. (\<nexists>y. rv = Some y) \<longrightarrow> True) and (\<lambda>s. (\<exists>y. rv = Some y) \<longrightarrow> True)\<rbrace>
 3. \<And>asida. \<lbrakk>asid \<le> mask local.asid_bits; asida = asid\<rbrakk> \<Longrightarrow> \<lbrace>?R206 asida\<rbrace> loadHWASID asid \<lbrace>\<lambda>rv. (\<lambda>_. True) and ?R354 asida rv\<rbrace>
 4. \<And>asida s s'. \<lbrakk>asid \<le> mask local.asid_bits; asida = asid; (s, s') \<in> rf_sr; valid_pde_mappings' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (valid_pde_mappings' and (\<lambda>_. asid \<le> mask local.asid_bits) and ?R206 asida) s \<and> s' \<in> {s. asid_'_update (\<lambda>_. asida) s \<in> UNIV \<inter> \<lbrace>\<acute>asid = asid\<rbrace>} \<inter> {s'. \<forall>t rv. rv = pde_stored_asid (ret__struct_pde_C_' t) \<and> pde_get_tag (ret__struct_pde_C_' t) = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid \<longrightarrow> s'\<lparr>globals := globals t, stored_hw_asid___struct_pde_C_' := ret__struct_pde_C_' t\<rparr> \<in> {s. s \<in> UNIV} \<inter> {s'. \<forall>ta rva. dc rva (xfdc ta) \<longrightarrow> s'\<lparr>globals := globals ta\<rparr> \<in> {s. \<forall>v v'. v = stored_asid_valid_CL (pde_pde_invalid_lift (pde_' (pde_'_update (\<lambda>_. ret__struct_pde_C_' t) s))) \<longrightarrow> s\<lparr>ret__unsigned_' := v\<rparr> \<in> {s. s \<in> \<lbrace>True\<rbrace> \<inter> {s. (s \<in> (if v = 0 then UNIV else {}) \<longrightarrow> s \<in> UNIV \<inter> ?PT'473 asida rv (ret__struct_pde_C_' t) rva (xfdc ta) v) \<and> (s \<notin> (if v = 0 then UNIV else {}) \<longrightarrow> s \<in> {s. \<forall>v v'. v = stored_hw_asid_CL (pde_pde_invalid_lift (pde_' (pde_'_update (\<lambda>_. ret__struct_pde_C_' t) s))) \<longrightarrow> s\<lparr>ret__unsigned_' := v\<rparr> \<in> {s. s \<in> {s. hw_asid_'_update (\<lambda>_. UCAST(32 \<rightarrow> 8) v) s \<in> \<lbrace>\<acute>hw_asid = UCAST(32 \<rightarrow> 8) v\<rbrace>}}} \<inter> {s. pde_get_tag (pde_' (pde_'_update (\<lambda>_. ret__struct_pde_C_' t) s)) = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid})}}} \<inter> {s. pde_get_tag (pde_' (pde_'_update (\<lambda>_. ret__struct_pde_C_' t) s)) = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid}}} proof (prove)
goal (3 subgoals):
 1. \<And>asida rv stored_hw_asid___struct_pde_C. \<lbrakk>asid \<le> mask local.asid_bits; asida = asid; rv = pde_stored_asid stored_hw_asid___struct_pde_C \<and> pde_get_tag stored_hw_asid___struct_pde_C = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid\<rbrakk> \<Longrightarrow> \<lbrace>?R354 asida rv\<rbrace> doMachineOp cleanCaches_PoU \<lbrace>\<lambda>a. (\<lambda>_. True) and (\<lambda>s. (\<nexists>y. rv = Some y) \<longrightarrow> True) and (\<lambda>s. (\<exists>y. rv = Some y) \<longrightarrow> True)\<rbrace>
 2. \<And>asida. \<lbrakk>asid \<le> mask local.asid_bits; asida = asid\<rbrakk> \<Longrightarrow> \<lbrace>?R206 asida\<rbrace> loadHWASID asid \<lbrace>\<lambda>rv. (\<lambda>_. True) and ?R354 asida rv\<rbrace>
 3. \<And>asida s s'. \<lbrakk>asid \<le> mask local.asid_bits; asida = asid; (s, s') \<in> rf_sr; valid_pde_mappings' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (valid_pde_mappings' and (\<lambda>_. asid \<le> mask local.asid_bits) and ?R206 asida) s \<and> s' \<in> {s. asid_'_update (\<lambda>_. asida) s \<in> UNIV \<inter> \<lbrace>\<acute>asid = asid\<rbrace>} \<inter> {s'. \<forall>t rv. rv = pde_stored_asid (ret__struct_pde_C_' t) \<and> pde_get_tag (ret__struct_pde_C_' t) = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid \<longrightarrow> s'\<lparr>globals := globals t, stored_hw_asid___struct_pde_C_' := ret__struct_pde_C_' t\<rparr> \<in> {s. s \<in> UNIV} \<inter> {s'. \<forall>ta rv. dc rv (xfdc ta) \<longrightarrow> s'\<lparr>globals := globals ta\<rparr> \<in> {s. \<forall>v v'. v = stored_asid_valid_CL (pde_pde_invalid_lift (pde_' (pde_'_update (\<lambda>_. ret__struct_pde_C_' t) s))) \<longrightarrow> s\<lparr>ret__unsigned_' := v\<rparr> \<in> {s. s \<in> \<lbrace>True\<rbrace> \<inter> {s. (s \<in> (if v = 0 then UNIV else {}) \<longrightarrow> s \<in> UNIV \<inter> \<lbrace>True\<rbrace>) \<and> (s \<notin> (if v = 0 then UNIV else {}) \<longrightarrow> s \<in> {s. \<forall>v v'. v = stored_hw_asid_CL (pde_pde_invalid_lift (pde_' (pde_'_update (\<lambda>_. ret__struct_pde_C_' t) s))) \<longrightarrow> s\<lparr>ret__unsigned_' := v\<rparr> \<in> {s. s \<in> {s. hw_asid_'_update (\<lambda>_. UCAST(32 \<rightarrow> 8) v) s \<in> \<lbrace>\<acute>hw_asid = UCAST(32 \<rightarrow> 8) v\<rbrace>}}} \<inter> {s. pde_get_tag (pde_' (pde_'_update (\<lambda>_. ret__struct_pde_C_' t) s)) = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid})}}} \<inter> {s. pde_get_tag (pde_' (pde_'_update (\<lambda>_. ret__struct_pde_C_' t) s)) = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid}}} proof (prove)
goal (1 subgoal):
 1. \<And>asida s s'. \<lbrakk>asid \<le> mask local.asid_bits; asida = asid; (s, s') \<in> rf_sr; valid_pde_mappings' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (valid_pde_mappings' and (\<lambda>_. asid \<le> mask local.asid_bits) and (\<lambda>s. ((\<lambda>_. True) and (\<lambda>a. True \<and> ((\<nexists>y. map_option fst (armKSASIDMap (ksArchState s) asid) = Some y) \<longrightarrow> True) \<and> ((\<exists>y. map_option fst (armKSASIDMap (ksArchState s) asid) = Some y) \<longrightarrow> True))) s)) s \<and> s' \<in> {s. asid_'_update (\<lambda>_. asida) s \<in> UNIV \<inter> \<lbrace>\<acute>asid = asid\<rbrace>} \<inter> {s'. \<forall>t rv. rv = pde_stored_asid (ret__struct_pde_C_' t) \<and> pde_get_tag (ret__struct_pde_C_' t) = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid \<longrightarrow> s'\<lparr>globals := globals t, stored_hw_asid___struct_pde_C_' := ret__struct_pde_C_' t\<rparr> \<in> {s. s \<in> UNIV} \<inter> {s'. \<forall>ta rv. dc rv (xfdc ta) \<longrightarrow> s'\<lparr>globals := globals ta\<rparr> \<in> {s. \<forall>v v'. v = stored_asid_valid_CL (pde_pde_invalid_lift (pde_' (pde_'_update (\<lambda>_. ret__struct_pde_C_' t) s))) \<longrightarrow> s\<lparr>ret__unsigned_' := v\<rparr> \<in> {s. s \<in> \<lbrace>True\<rbrace> \<inter> {s. (s \<in> (if v = 0 then UNIV else {}) \<longrightarrow> s \<in> UNIV \<inter> \<lbrace>True\<rbrace>) \<and> (s \<notin> (if v = 0 then UNIV else {}) \<longrightarrow> s \<in> {s. \<forall>v v'. v = stored_hw_asid_CL (pde_pde_invalid_lift (pde_' (pde_'_update (\<lambda>_. ret__struct_pde_C_' t) s))) \<longrightarrow> s\<lparr>ret__unsigned_' := v\<rparr> \<in> {s. s \<in> {s. hw_asid_'_update (\<lambda>_. UCAST(32 \<rightarrow> 8) v) s \<in> \<lbrace>\<acute>hw_asid = UCAST(32 \<rightarrow> 8) v\<rbrace>}}} \<inter> {s. pde_get_tag (pde_' (pde_'_update (\<lambda>_. ret__struct_pde_C_' t) s)) = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid})}}} \<inter> {s. pde_get_tag (pde_' (pde_'_update (\<lambda>_. ret__struct_pde_C_' t) s)) = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid}}} proof (prove)
goal:
No subgoals!