theory Recycle_C

lemma invalidateTLBByASID_ccorres:
  "ccorres dc xfdc (valid_pde_mappings' and (\<lambda>_. asid \<le> mask asid_bits))
                   (UNIV \<inter> {s. asid_' s = asid}) []
       (invalidateTLBByASID asid) (Call invalidateTLBByASID_'proc)" apply (cinit lift: asid_') apply (ctac(no_vcg) add: loadHWASID_ccorres) apply csymbr apply (simp add: case_option_If2 del: Collect_const) apply (rule ccorres_if_cond_throws2[where Q=\<top> and Q'=\<top>]) apply (clarsimp simp: pde_stored_asid_def to_bool_def split: if_split) apply (rule ccorres_return_void_C) apply simp apply csymbr apply (ctac add: invalidateTranslationASID_ccorres) apply vcg apply (wp hoare_drop_imps) apply (clarsimp simp: pde_stored_asid_def to_bool_def) 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>) [] (invalidateTLBByASID asid) (Call invalidateTLBByASID_'proc) proof (prove)
goal (2 subgoals):
 1. \<And>asida. asida = asid \<Longrightarrow> ccorres dc xfdc (?Q170 asida) (?Q'170 asida) [SKIP] (do maybe_hw_asid <- loadHWASID asid;
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);;
(\<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>asida = asid; (s, s') \<in> rf_sr; (valid_pde_mappings' and (\<lambda>_. asid \<le> mask local.asid_bits)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q170 asida s \<and> s' \<in> ?Q'170 asida proof (prove)
goal (3 subgoals):
 1. \<And>asida rv stored_hw_asid___struct_pde_C. \<lbrakk>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 (?Q178 asida rv) (?Q'178 asida rv stored_hw_asid___struct_pde_C) [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. asida = asid \<Longrightarrow> \<lbrace>?R178 asida\<rbrace> loadHWASID asid \<lbrace>?Q178 asida\<rbrace>
 3. \<And>asida s s'. \<lbrakk>asida = asid; (s, s') \<in> rf_sr; (valid_pde_mappings' and (\<lambda>_. asid \<le> mask local.asid_bits)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (valid_pde_mappings' and (\<lambda>_. asid \<le> mask local.asid_bits) and ?R178 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'178 asida rv (ret__struct_pde_C_' t)} proof (prove)
goal (3 subgoals):
 1. \<And>asida stored_hw_asid___struct_pde_C ret__unsigned. \<lbrakk>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 (?Q178 asida (pde_stored_asid stored_hw_asid___struct_pde_C)) (?G'299 asida (pde_stored_asid stored_hw_asid___struct_pde_C) stored_hw_asid___struct_pde_C 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. asida = asid \<Longrightarrow> \<lbrace>?R178 asida\<rbrace> loadHWASID asid \<lbrace>?Q178 asida\<rbrace>
 3. \<And>asida s s'. \<lbrakk>asida = asid; (s, s') \<in> rf_sr; (valid_pde_mappings' and (\<lambda>_. asid \<le> mask local.asid_bits)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (valid_pde_mappings' and (\<lambda>_. asid \<le> mask local.asid_bits) and ?R178 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. \<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'299 asida rv (ret__struct_pde_C_' t) 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 (3 subgoals):
 1. \<And>asida stored_hw_asid___struct_pde_C ret__unsigned. \<lbrakk>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 (?Q178 asid (pde_stored_asid stored_hw_asid___struct_pde_C)) (?G'299 asid (pde_stored_asid stored_hw_asid___struct_pde_C) stored_hw_asid___struct_pde_C (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 ()) (IF stored_asid_valid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C) = 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. asida = asid \<Longrightarrow> \<lbrace>?R178 asida\<rbrace> loadHWASID asid \<lbrace>?Q178 asida\<rbrace>
 3. \<And>asida s s'. \<lbrakk>asida = asid; (s, s') \<in> rf_sr; (valid_pde_mappings' and (\<lambda>_. asid \<le> mask local.asid_bits)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (valid_pde_mappings' and (\<lambda>_. asid \<le> mask local.asid_bits) and ?R178 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. \<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'299 asida rv (ret__struct_pde_C_' t) 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 ret__unsigned. \<lbrakk>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> \<lbrace>stored_asid_valid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C) = 0\<rbrace>)
 2. \<And>asida stored_hw_asid___struct_pde_C ret__unsigned. \<lbrakk>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 (?R396 asid (pde_stored_asid stored_hw_asid___struct_pde_C)) (?R'392 asid (pde_stored_asid stored_hw_asid___struct_pde_C) stored_hw_asid___struct_pde_C (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 ret__unsigned. \<lbrakk>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 (?U394 asid (pde_stored_asid stored_hw_asid___struct_pde_C)) (?U'388 asid (pde_stored_asid stored_hw_asid___struct_pde_C) stored_hw_asid___struct_pde_C (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 ret__unsigned. \<lbrakk>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'390 asid (pde_stored_asid stored_hw_asid___struct_pde_C) stored_hw_asid___struct_pde_C (stored_asid_valid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C))) return_void_C {},UNIV
 5. \<And>asida. asida = asid \<Longrightarrow> \<lbrace>?R178 asida\<rbrace> loadHWASID asid \<lbrace>\<lambda>a. (\<lambda>_. True) and (\<lambda>s. (\<nexists>y. a = Some y) \<longrightarrow> ?R396 asida a s) and (\<lambda>s. (\<exists>y. a = Some y) \<longrightarrow> ?U394 asida a s)\<rbrace>
 6. \<And>asida s s'. \<lbrakk>asida = asid; (s, s') \<in> rf_sr; (valid_pde_mappings' and (\<lambda>_. asid \<le> mask local.asid_bits)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (valid_pde_mappings' and (\<lambda>_. asid \<le> mask local.asid_bits) and ?R178 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. \<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> \<lbrace>v = 0\<rbrace> \<longrightarrow> s \<in> ?R'392 asida rv (ret__struct_pde_C_' t) v \<inter> ?PT'390 asida rv (ret__struct_pde_C_' t) v) \<and> (s \<notin> \<lbrace>v = 0\<rbrace> \<longrightarrow> s \<in> ?U'388 asida rv (ret__struct_pde_C_' t) 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 ret__unsigned. \<lbrakk>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 (?R396 asid (pde_stored_asid stored_hw_asid___struct_pde_C)) (?R'392 asid (pde_stored_asid stored_hw_asid___struct_pde_C) stored_hw_asid___struct_pde_C (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 ret__unsigned. \<lbrakk>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 (?U394 asid (pde_stored_asid stored_hw_asid___struct_pde_C)) (?U'388 asid (pde_stored_asid stored_hw_asid___struct_pde_C) stored_hw_asid___struct_pde_C (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 ret__unsigned. \<lbrakk>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'390 asid (pde_stored_asid stored_hw_asid___struct_pde_C) stored_hw_asid___struct_pde_C (stored_asid_valid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C))) return_void_C {},UNIV
 4. \<And>asida. asida = asid \<Longrightarrow> \<lbrace>?R178 asida\<rbrace> loadHWASID asid \<lbrace>\<lambda>a. (\<lambda>_. True) and (\<lambda>s. (\<nexists>y. a = Some y) \<longrightarrow> ?R396 asida a s) and (\<lambda>s. (\<exists>y. a = Some y) \<longrightarrow> ?U394 asida a s)\<rbrace>
 5. \<And>asida s s'. \<lbrakk>asida = asid; (s, s') \<in> rf_sr; (valid_pde_mappings' and (\<lambda>_. asid \<le> mask local.asid_bits)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (valid_pde_mappings' and (\<lambda>_. asid \<le> mask local.asid_bits) and ?R178 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. \<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> \<lbrace>v = 0\<rbrace> \<longrightarrow> s \<in> ?R'392 asida rv (ret__struct_pde_C_' t) v \<inter> ?PT'390 asida rv (ret__struct_pde_C_' t) v) \<and> (s \<notin> \<lbrace>v = 0\<rbrace> \<longrightarrow> s \<in> ?U'388 asida rv (ret__struct_pde_C_' t) 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 ret__unsigned. \<lbrakk>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 (?U394 asid (pde_stored_asid stored_hw_asid___struct_pde_C)) (?U'388 asid (pde_stored_asid stored_hw_asid___struct_pde_C) stored_hw_asid___struct_pde_C (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 ret__unsigned. \<lbrakk>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'390 asid (pde_stored_asid stored_hw_asid___struct_pde_C) stored_hw_asid___struct_pde_C (stored_asid_valid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C))) return_void_C {},UNIV
 3. \<And>asida. asida = asid \<Longrightarrow> \<lbrace>?R178 asida\<rbrace> loadHWASID asid \<lbrace>\<lambda>a. (\<lambda>_. True) and (\<lambda>s. (\<nexists>y. a = Some y) \<longrightarrow> True) and (\<lambda>s. (\<exists>y. a = Some y) \<longrightarrow> ?U394 asida a s)\<rbrace>
 4. \<And>asida s s'. \<lbrakk>asida = asid; (s, s') \<in> rf_sr; (valid_pde_mappings' and (\<lambda>_. asid \<le> mask local.asid_bits)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (valid_pde_mappings' and (\<lambda>_. asid \<le> mask local.asid_bits) and ?R178 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. \<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> \<lbrace>v = 0\<rbrace> \<longrightarrow> s \<in> UNIV \<inter> ?PT'390 asida rv (ret__struct_pde_C_' t) v) \<and> (s \<notin> \<lbrace>v = 0\<rbrace> \<longrightarrow> s \<in> ?U'388 asida rv (ret__struct_pde_C_' t) 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 ret__unsigned. \<lbrakk>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 (?U394 asid (pde_stored_asid stored_hw_asid___struct_pde_C)) (?U'388 asid (pde_stored_asid stored_hw_asid___struct_pde_C) stored_hw_asid___struct_pde_C (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 ret__unsigned. \<lbrakk>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'390 asid (pde_stored_asid stored_hw_asid___struct_pde_C) stored_hw_asid___struct_pde_C (stored_asid_valid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C))) return_void_C {},UNIV
 3. \<And>asida. asida = asid \<Longrightarrow> \<lbrace>?R178 asida\<rbrace> loadHWASID asid \<lbrace>\<lambda>a. (\<lambda>_. True) and (\<lambda>s. (\<nexists>y. a = Some y) \<longrightarrow> True) and (\<lambda>s. (\<exists>y. a = Some y) \<longrightarrow> ?U394 asida a s)\<rbrace>
 4. \<And>asida s s'. \<lbrakk>asida = asid; (s, s') \<in> rf_sr; (valid_pde_mappings' and (\<lambda>_. asid \<le> mask local.asid_bits)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (valid_pde_mappings' and (\<lambda>_. asid \<le> mask local.asid_bits) and ?R178 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. \<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> \<lbrace>v = 0\<rbrace> \<longrightarrow> s \<in> UNIV \<inter> ?PT'390 asida rv (ret__struct_pde_C_' t) v) \<and> (s \<notin> \<lbrace>v = 0\<rbrace> \<longrightarrow> s \<in> ?U'388 asida rv (ret__struct_pde_C_' t) 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 ret__unsigneda ret__unsigned. \<lbrakk>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 (?U394 asid (pde_stored_asid stored_hw_asid___struct_pde_C)) (?G'418 asid (pde_stored_asid stored_hw_asid___struct_pde_C) stored_hw_asid___struct_pde_C (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 ret__unsigned. \<lbrakk>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'390 asid (pde_stored_asid stored_hw_asid___struct_pde_C) stored_hw_asid___struct_pde_C (stored_asid_valid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C))) return_void_C {},UNIV
 3. \<And>asida. asida = asid \<Longrightarrow> \<lbrace>?R178 asida\<rbrace> loadHWASID asid \<lbrace>\<lambda>a. (\<lambda>_. True) and (\<lambda>s. (\<nexists>y. a = Some y) \<longrightarrow> True) and (\<lambda>s. (\<exists>y. a = Some y) \<longrightarrow> ?U394 asida a s)\<rbrace>
 4. \<And>asida s s'. \<lbrakk>asida = asid; (s, s') \<in> rf_sr; (valid_pde_mappings' and (\<lambda>_. asid \<le> mask local.asid_bits)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (valid_pde_mappings' and (\<lambda>_. asid \<le> mask local.asid_bits) and ?R178 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. \<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> \<lbrace>v = 0\<rbrace> \<longrightarrow> s \<in> UNIV \<inter> ?PT'390 asida rv (ret__struct_pde_C_' t) v) \<and> (s \<notin> \<lbrace>v = 0\<rbrace> \<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'418 asida rv (ret__struct_pde_C_' t) 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 (3 subgoals):
 1. \<And>asida stored_hw_asid___struct_pde_C ret__unsigned. \<lbrakk>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'390 asid (pde_stored_asid stored_hw_asid___struct_pde_C) stored_hw_asid___struct_pde_C (stored_asid_valid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C))) return_void_C {},UNIV
 2. \<And>asida. asida = asid \<Longrightarrow> \<lbrace>?R178 asida\<rbrace> loadHWASID asid \<lbrace>\<lambda>a. (\<lambda>_. True) and (\<lambda>s. (\<nexists>y. a = Some y) \<longrightarrow> True) and (\<lambda>s. (\<exists>y. a = Some y) \<longrightarrow> True)\<rbrace>
 3. \<And>asida s s'. \<lbrakk>asida = asid; (s, s') \<in> rf_sr; (valid_pde_mappings' and (\<lambda>_. asid \<le> mask local.asid_bits)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (valid_pde_mappings' and (\<lambda>_. asid \<le> mask local.asid_bits) and ?R178 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. \<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> \<lbrace>v = 0\<rbrace> \<longrightarrow> s \<in> UNIV \<inter> ?PT'390 asida rv (ret__struct_pde_C_' t) v) \<and> (s \<notin> \<lbrace>v = 0\<rbrace> \<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 = the rv\<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 (2 subgoals):
 1. \<And>asida. asida = asid \<Longrightarrow> \<lbrace>?R178 asida\<rbrace> loadHWASID asid \<lbrace>\<lambda>a. (\<lambda>_. True) and (\<lambda>s. (\<nexists>y. a = Some y) \<longrightarrow> True) and (\<lambda>s. (\<exists>y. a = Some y) \<longrightarrow> True)\<rbrace>
 2. \<And>asida s s'. \<lbrakk>asida = asid; (s, s') \<in> rf_sr; (valid_pde_mappings' and (\<lambda>_. asid \<le> mask local.asid_bits)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (valid_pde_mappings' and (\<lambda>_. asid \<le> mask local.asid_bits) and ?R178 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. \<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> \<lbrace>v = 0\<rbrace> \<longrightarrow> s \<in> UNIV \<inter> \<lbrace>True\<rbrace>) \<and> (s \<notin> \<lbrace>v = 0\<rbrace> \<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 = the rv\<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>asida = asid; (s, s') \<in> rf_sr; (valid_pde_mappings' and (\<lambda>_. asid \<le> mask local.asid_bits)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (valid_pde_mappings' and (\<lambda>_. asid \<le> mask local.asid_bits) and (\<lambda>s. ((\<lambda>_. True) and (\<lambda>sa. (\<nexists>y. map_option fst (armKSASIDMap (ksArchState s) asid) = Some y) \<longrightarrow> True) and (\<lambda>sa. (\<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. \<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> \<lbrace>v = 0\<rbrace> \<longrightarrow> s \<in> UNIV \<inter> \<lbrace>True\<rbrace>) \<and> (s \<notin> \<lbrace>v = 0\<rbrace> \<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 = the rv\<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!