theory Finalise_C

lemma invalidateASIDEntry_ccorres:
  "ccorres dc xfdc (\<lambda>s. valid_pde_mappings' s \<and> asid \<le> mask asid_bits)
      (UNIV \<inter> {s. asid_' s = asid}) []
      (invalidateASIDEntry asid) (Call invalidateASIDEntry_'proc)" apply (cinit lift: asid_') apply (ctac(no_vcg) add: loadHWASID_ccorres) apply csymbr apply (simp(no_asm) add: when_def del: Collect_const) apply (rule ccorres_split_nothrow_novcg_dc) apply (rule ccorres_cond2[where R=\<top>]) apply (clarsimp simp: Collect_const_mem pde_stored_asid_def to_bool_def
                        split: if_split) apply csymbr apply (rule ccorres_Guard)+ apply (rule_tac P="pde_stored_asid stored_hw_asid___struct_pde_C \<noteq> None" in ccorres_gen_asm) apply (ctac(no_simp) add: invalidateHWASIDEntry_ccorres) apply (clarsimp simp: pde_stored_asid_def unat_ucast
                       split: if_split_asm) apply (rule sym, rule nat_mod_eq') apply (simp add: pde_pde_invalid_lift_def pde_lift_def) apply (rule unat_less_power[where sz=8, simplified]) apply (simp add: word_bits_conv) apply (rule order_le_less_trans, rule word_and_le1) apply (simp add: mask_def) apply (rule ccorres_return_Skip) apply (ctac add: invalidateASID_ccorres) apply wp apply (simp add: guard_is_UNIV_def) apply wp apply (clarsimp simp: Collect_const_mem pde_pde_invalid_lift_def pde_lift_def
                   order_le_less_trans[OF word_and_le1] mask_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres dc xfdc (\<lambda>s. valid_pde_mappings' s \<and> asid \<le> mask local.asid_bits) (UNIV \<inter> \<lbrace>\<acute>asid = asid\<rbrace>) [] (invalidateASIDEntry asid) (Call invalidateASIDEntry_'proc) proof (prove)
goal (2 subgoals):
 1. \<And>asida. asida = asid \<Longrightarrow> ccorres dc xfdc (?Q177 asida) (?Q'177 asida) [SKIP] (do maybeHWASID <- loadHWASID asid;
y <- when (\<exists>y. maybeHWASID = Some y) (invalidateHWASIDEntry (the maybeHWASID));
invalidateASID 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 \<noteq> 0 THEN
  \<acute>ret__unsigned :== CALL pde_pde_invalid_get_stored_hw_asid_'proc(\<acute>stored_hw_asid___struct_pde_C);;
Guard ArrayBounds \<lbrace>\<acute>ret__unsigned < 0x100\<rbrace> (\<acute>armKSHWASIDTable :== Arrays.update \<acute>armKSHWASIDTable (unat \<acute>ret__unsigned) (SCAST(32 signed \<rightarrow> 32) asidInvalid))
FI;;
CALL invalidateASID_'proc(asida))))
 2. \<And>asida s s'. \<lbrakk>asida = asid; (s, s') \<in> rf_sr; valid_pde_mappings' s \<and> asid \<le> mask local.asid_bits; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q177 asida s \<and> s' \<in> ?Q'177 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 (?Q185 asida rv) (?Q'185 asida rv stored_hw_asid___struct_pde_C) [SKIP] (do y <- when (\<exists>y. rv = Some y) (invalidateHWASIDEntry (the rv));
invalidateASID asid
od) (\<acute>ret__unsigned :== CALL pde_pde_invalid_get_stored_asid_valid_'proc(stored_hw_asid___struct_pde_C);;
(IF \<acute>ret__unsigned \<noteq> 0 THEN
  \<acute>ret__unsigned :== CALL pde_pde_invalid_get_stored_hw_asid_'proc(stored_hw_asid___struct_pde_C);;
Guard ArrayBounds \<lbrace>\<acute>ret__unsigned < 0x100\<rbrace> (\<acute>armKSHWASIDTable :== Arrays.update \<acute>armKSHWASIDTable (unat \<acute>ret__unsigned) (SCAST(32 signed \<rightarrow> 32) asidInvalid))
FI;;
CALL invalidateASID_'proc(asida)))
 2. \<And>asida. asida = asid \<Longrightarrow> \<lbrace>?R185 asida\<rbrace> loadHWASID asid \<lbrace>?Q185 asida\<rbrace>
 3. \<And>asida s s'. \<lbrakk>asida = asid; (s, s') \<in> rf_sr; valid_pde_mappings' s \<and> asid \<le> mask local.asid_bits; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (valid_pde_mappings' and (\<lambda>_. asid \<le> mask local.asid_bits) and ?R185 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'185 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 (?Q185 asida (pde_stored_asid stored_hw_asid___struct_pde_C)) (?G'314 asida (pde_stored_asid stored_hw_asid___struct_pde_C) stored_hw_asid___struct_pde_C ret__unsigned) [SKIP] (do y <- when (\<exists>y. pde_stored_asid stored_hw_asid___struct_pde_C = Some y) (invalidateHWASIDEntry (the (pde_stored_asid stored_hw_asid___struct_pde_C)));
invalidateASID asid
od) (IF ret__unsigned \<noteq> 0 THEN
  \<acute>ret__unsigned :== CALL pde_pde_invalid_get_stored_hw_asid_'proc(stored_hw_asid___struct_pde_C);;
Guard ArrayBounds \<lbrace>\<acute>ret__unsigned < 0x100\<rbrace> (\<acute>armKSHWASIDTable :== Arrays.update \<acute>armKSHWASIDTable (unat \<acute>ret__unsigned) (SCAST(32 signed \<rightarrow> 32) asidInvalid))
FI;;
CALL invalidateASID_'proc(asida))
 2. \<And>asida. asida = asid \<Longrightarrow> \<lbrace>?R185 asida\<rbrace> loadHWASID asid \<lbrace>?Q185 asida\<rbrace>
 3. \<And>asida s s'. \<lbrakk>asida = asid; (s, s') \<in> rf_sr; valid_pde_mappings' s \<and> asid \<le> mask local.asid_bits; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (valid_pde_mappings' and (\<lambda>_. asid \<le> mask local.asid_bits) and ?R185 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'314 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 (?Q185 asida (pde_stored_asid stored_hw_asid___struct_pde_C)) (?G'314 asida (pde_stored_asid stored_hw_asid___struct_pde_C) stored_hw_asid___struct_pde_C ret__unsigned) [SKIP] (do y <- if \<exists>y. pde_stored_asid stored_hw_asid___struct_pde_C = Some y then invalidateHWASIDEntry (the (pde_stored_asid stored_hw_asid___struct_pde_C)) else return ();
invalidateASID asid
od) (IF ret__unsigned \<noteq> 0 THEN
  \<acute>ret__unsigned :== CALL pde_pde_invalid_get_stored_hw_asid_'proc(stored_hw_asid___struct_pde_C);;
Guard ArrayBounds \<lbrace>\<acute>ret__unsigned < 0x100\<rbrace> (\<acute>armKSHWASIDTable :== Arrays.update \<acute>armKSHWASIDTable (unat \<acute>ret__unsigned) (SCAST(32 signed \<rightarrow> 32) asidInvalid))
FI;;
CALL invalidateASID_'proc(asida))
 2. \<And>asida. asida = asid \<Longrightarrow> \<lbrace>?R185 asida\<rbrace> loadHWASID asid \<lbrace>?Q185 asida\<rbrace>
 3. \<And>asida s s'. \<lbrakk>asida = asid; (s, s') \<in> rf_sr; valid_pde_mappings' s \<and> asid \<le> mask local.asid_bits; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (valid_pde_mappings' and (\<lambda>_. asid \<le> mask local.asid_bits) and ?R185 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'314 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> ccorres dc xfdc (?P400 asida (pde_stored_asid stored_hw_asid___struct_pde_C)) (?G'314 asida (pde_stored_asid stored_hw_asid___struct_pde_C) stored_hw_asid___struct_pde_C ret__unsigned) [] (if \<exists>y. pde_stored_asid stored_hw_asid___struct_pde_C = Some y then invalidateHWASIDEntry (the (pde_stored_asid stored_hw_asid___struct_pde_C)) else return ()) (IF ret__unsigned \<noteq> 0 THEN
  \<acute>ret__unsigned :== CALL pde_pde_invalid_get_stored_hw_asid_'proc(stored_hw_asid___struct_pde_C);;
Guard ArrayBounds \<lbrace>\<acute>ret__unsigned < 0x100\<rbrace> (\<acute>armKSHWASIDTable :== Arrays.update \<acute>armKSHWASIDTable (unat \<acute>ret__unsigned) (SCAST(32 signed \<rightarrow> 32) asidInvalid))
FI)
 2. \<And>asida stored_hw_asid___struct_pde_C ret__unsigned y rv'. \<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); dc y rv'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q395 asida stored_hw_asid___struct_pde_C ret__unsigned y) (?Q'395 asida stored_hw_asid___struct_pde_C ret__unsigned y rv') [SKIP] (invalidateASID asid) (CALL invalidateASID_'proc(asida))
 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> \<lbrace>?R398 asida (pde_stored_asid stored_hw_asid___struct_pde_C)\<rbrace> if \<exists>y. pde_stored_asid stored_hw_asid___struct_pde_C = Some y then invalidateHWASIDEntry (the (pde_stored_asid stored_hw_asid___struct_pde_C)) else return () \<lbrace>?Q395 asida stored_hw_asid___struct_pde_C ret__unsigned\<rbrace>
 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> guard_is_UNIV dc xfdc (?Q'395 asida stored_hw_asid___struct_pde_C ret__unsigned)
 5. \<And>asida. asida = asid \<Longrightarrow> \<lbrace>?R185 asida\<rbrace> loadHWASID asid \<lbrace>\<lambda>a. ?P400 asida a and ?R398 asida a\<rbrace>
 6. \<And>asida s s'. \<lbrakk>asida = asid; (s, s') \<in> rf_sr; valid_pde_mappings' s \<and> asid \<le> mask local.asid_bits; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (valid_pde_mappings' and (\<lambda>_. asid \<le> mask local.asid_bits) and ?R185 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'314 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 (8 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 \<longrightarrow> (\<exists>y. pde_stored_asid stored_hw_asid___struct_pde_C = Some y) = (s' \<in> \<lbrace>ret__unsigned \<noteq> 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)\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Pt415 asida (pde_stored_asid stored_hw_asid___struct_pde_C)) (?Rt412 asida (pde_stored_asid stored_hw_asid___struct_pde_C) stored_hw_asid___struct_pde_C ret__unsigned) [] (invalidateHWASIDEntry (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);;
Guard ArrayBounds \<lbrace>\<acute>ret__unsigned < 0x100\<rbrace> (\<acute>armKSHWASIDTable :== Arrays.update \<acute>armKSHWASIDTable (unat \<acute>ret__unsigned) (SCAST(32 signed \<rightarrow> 32) asidInvalid)))
 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> ccorres dc xfdc (?Pf413 asida (pde_stored_asid stored_hw_asid___struct_pde_C)) (?Rf411 asida (pde_stored_asid stored_hw_asid___struct_pde_C) stored_hw_asid___struct_pde_C ret__unsigned) [] (return ()) SKIP
 4. \<And>asida stored_hw_asid___struct_pde_C ret__unsigned y rv'. \<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); dc y rv'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q395 asida stored_hw_asid___struct_pde_C ret__unsigned y) (?Q'395 asida stored_hw_asid___struct_pde_C ret__unsigned y rv') [SKIP] (invalidateASID asid) (CALL invalidateASID_'proc(asida))
 5. \<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> \<lbrace>?R398 asida (pde_stored_asid stored_hw_asid___struct_pde_C)\<rbrace> if \<exists>y. pde_stored_asid stored_hw_asid___struct_pde_C = Some y then invalidateHWASIDEntry (the (pde_stored_asid stored_hw_asid___struct_pde_C)) else return () \<lbrace>?Q395 asida stored_hw_asid___struct_pde_C ret__unsigned\<rbrace>
 6. \<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> guard_is_UNIV dc xfdc (?Q'395 asida stored_hw_asid___struct_pde_C ret__unsigned)
 7. \<And>asida. asida = asid \<Longrightarrow> \<lbrace>?R185 asida\<rbrace> loadHWASID asid \<lbrace>\<lambda>a. (\<lambda>_. True) and (\<lambda>s. (\<exists>y. a = Some y) \<longrightarrow> ?Pt415 asida a s) and (\<lambda>s. (\<nexists>y. a = Some y) \<longrightarrow> ?Pf413 asida a s) and ?R398 asida a\<rbrace>
 8. \<And>asida s s'. \<lbrakk>asida = asid; (s, s') \<in> rf_sr; valid_pde_mappings' s \<and> asid \<le> mask local.asid_bits; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (valid_pde_mappings' and (\<lambda>_. asid \<le> mask local.asid_bits) and ?R185 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> {s. (s \<in> \<lbrace>v \<noteq> 0\<rbrace> \<longrightarrow> s \<in> ?Rt412 asida rv (ret__struct_pde_C_' t) v) \<and> (s \<notin> \<lbrace>v \<noteq> 0\<rbrace> \<longrightarrow> s \<in> ?Rf411 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 (7 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 (?Pt415 asida (pde_stored_asid stored_hw_asid___struct_pde_C)) (?Rt412 asida (pde_stored_asid stored_hw_asid___struct_pde_C) stored_hw_asid___struct_pde_C ret__unsigned) [] (invalidateHWASIDEntry (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);;
Guard ArrayBounds \<lbrace>\<acute>ret__unsigned < 0x100\<rbrace> (\<acute>armKSHWASIDTable :== Arrays.update \<acute>armKSHWASIDTable (unat \<acute>ret__unsigned) (SCAST(32 signed \<rightarrow> 32) asidInvalid)))
 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> ccorres dc xfdc (?Pf413 asida (pde_stored_asid stored_hw_asid___struct_pde_C)) (?Rf411 asida (pde_stored_asid stored_hw_asid___struct_pde_C) stored_hw_asid___struct_pde_C ret__unsigned) [] (return ()) SKIP
 3. \<And>asida stored_hw_asid___struct_pde_C ret__unsigned y rv'. \<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); dc y rv'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q395 asida stored_hw_asid___struct_pde_C ret__unsigned y) (?Q'395 asida stored_hw_asid___struct_pde_C ret__unsigned y rv') [SKIP] (invalidateASID asid) (CALL invalidateASID_'proc(asida))
 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> \<lbrace>?R398 asida (pde_stored_asid stored_hw_asid___struct_pde_C)\<rbrace> if \<exists>y. pde_stored_asid stored_hw_asid___struct_pde_C = Some y then invalidateHWASIDEntry (the (pde_stored_asid stored_hw_asid___struct_pde_C)) else return () \<lbrace>?Q395 asida stored_hw_asid___struct_pde_C ret__unsigned\<rbrace>
 5. \<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> guard_is_UNIV dc xfdc (?Q'395 asida stored_hw_asid___struct_pde_C ret__unsigned)
 6. \<And>asida. asida = asid \<Longrightarrow> \<lbrace>?R185 asida\<rbrace> loadHWASID asid \<lbrace>\<lambda>a. (\<lambda>_. True) and (\<lambda>s. (\<exists>y. a = Some y) \<longrightarrow> ?Pt415 asida a s) and (\<lambda>s. (\<nexists>y. a = Some y) \<longrightarrow> ?Pf413 asida a s) and ?R398 asida a\<rbrace>
 7. \<And>asida s s'. \<lbrakk>asida = asid; (s, s') \<in> rf_sr; valid_pde_mappings' s \<and> asid \<le> mask local.asid_bits; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (valid_pde_mappings' and (\<lambda>_. asid \<le> mask local.asid_bits) and ?R185 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> {s. (s \<in> \<lbrace>v \<noteq> 0\<rbrace> \<longrightarrow> s \<in> ?Rt412 asida rv (ret__struct_pde_C_' t) v) \<and> (s \<notin> \<lbrace>v \<noteq> 0\<rbrace> \<longrightarrow> s \<in> ?Rf411 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 (7 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); ret__unsigned = stored_hw_asid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C)\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Pt415 asida (pde_stored_asid stored_hw_asid___struct_pde_C)) (?G'433 asida (pde_stored_asid stored_hw_asid___struct_pde_C) stored_hw_asid___struct_pde_C ret__unsigneda ret__unsigned) [] (invalidateHWASIDEntry (the (pde_stored_asid stored_hw_asid___struct_pde_C))) (Guard ArrayBounds \<lbrace>ret__unsigned < 0x100\<rbrace> (\<acute>armKSHWASIDTable :== Arrays.update \<acute>armKSHWASIDTable (unat ret__unsigned) (SCAST(32 signed \<rightarrow> 32) asidInvalid)))
 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> ccorres dc xfdc (?Pf413 asida (pde_stored_asid stored_hw_asid___struct_pde_C)) (?Rf411 asida (pde_stored_asid stored_hw_asid___struct_pde_C) stored_hw_asid___struct_pde_C ret__unsigned) [] (return ()) SKIP
 3. \<And>asida stored_hw_asid___struct_pde_C ret__unsigned y rv'. \<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); dc y rv'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q395 asida stored_hw_asid___struct_pde_C ret__unsigned y) (?Q'395 asida stored_hw_asid___struct_pde_C ret__unsigned y rv') [SKIP] (invalidateASID asid) (CALL invalidateASID_'proc(asida))
 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> \<lbrace>?R398 asida (pde_stored_asid stored_hw_asid___struct_pde_C)\<rbrace> if \<exists>y. pde_stored_asid stored_hw_asid___struct_pde_C = Some y then invalidateHWASIDEntry (the (pde_stored_asid stored_hw_asid___struct_pde_C)) else return () \<lbrace>?Q395 asida stored_hw_asid___struct_pde_C ret__unsigned\<rbrace>
 5. \<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> guard_is_UNIV dc xfdc (?Q'395 asida stored_hw_asid___struct_pde_C ret__unsigned)
 6. \<And>asida. asida = asid \<Longrightarrow> \<lbrace>?R185 asida\<rbrace> loadHWASID asid \<lbrace>\<lambda>a. (\<lambda>_. True) and (\<lambda>s. (\<exists>y. a = Some y) \<longrightarrow> ?Pt415 asida a s) and (\<lambda>s. (\<nexists>y. a = Some y) \<longrightarrow> ?Pf413 asida a s) and ?R398 asida a\<rbrace>
 7. \<And>asida s s'. \<lbrakk>asida = asid; (s, s') \<in> rf_sr; valid_pde_mappings' s \<and> asid \<le> mask local.asid_bits; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (valid_pde_mappings' and (\<lambda>_. asid \<le> mask local.asid_bits) and ?R185 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> {s. (s \<in> \<lbrace>v \<noteq> 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'433 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}) \<and> (s \<notin> \<lbrace>v \<noteq> 0\<rbrace> \<longrightarrow> s \<in> ?Rf411 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 (7 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); ret__unsigned = stored_hw_asid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C)\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Pt415 asida (pde_stored_asid stored_hw_asid___struct_pde_C)) (?C'471 asida (pde_stored_asid stored_hw_asid___struct_pde_C) stored_hw_asid___struct_pde_C ret__unsigneda ret__unsigned) [] (invalidateHWASIDEntry (the (pde_stored_asid stored_hw_asid___struct_pde_C))) (\<acute>armKSHWASIDTable :== Arrays.update \<acute>armKSHWASIDTable (unat ret__unsigned) (SCAST(32 signed \<rightarrow> 32) asidInvalid))
 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> ccorres dc xfdc (?Pf413 asida (pde_stored_asid stored_hw_asid___struct_pde_C)) (?Rf411 asida (pde_stored_asid stored_hw_asid___struct_pde_C) stored_hw_asid___struct_pde_C ret__unsigned) [] (return ()) SKIP
 3. \<And>asida stored_hw_asid___struct_pde_C ret__unsigned y rv'. \<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); dc y rv'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q395 asida stored_hw_asid___struct_pde_C ret__unsigned y) (?Q'395 asida stored_hw_asid___struct_pde_C ret__unsigned y rv') [SKIP] (invalidateASID asid) (CALL invalidateASID_'proc(asida))
 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> \<lbrace>?R398 asida (pde_stored_asid stored_hw_asid___struct_pde_C)\<rbrace> if \<exists>y. pde_stored_asid stored_hw_asid___struct_pde_C = Some y then invalidateHWASIDEntry (the (pde_stored_asid stored_hw_asid___struct_pde_C)) else return () \<lbrace>?Q395 asida stored_hw_asid___struct_pde_C ret__unsigned\<rbrace>
 5. \<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> guard_is_UNIV dc xfdc (?Q'395 asida stored_hw_asid___struct_pde_C ret__unsigned)
 6. \<And>asida. asida = asid \<Longrightarrow> \<lbrace>?R185 asida\<rbrace> loadHWASID asid \<lbrace>\<lambda>a. (\<lambda>_. True) and (\<lambda>s. (\<exists>y. a = Some y) \<longrightarrow> ?Pt415 asida a s) and (\<lambda>s. (\<nexists>y. a = Some y) \<longrightarrow> ?Pf413 asida a s) and ?R398 asida a\<rbrace>
 7. \<And>asida s s'. \<lbrakk>asida = asid; (s, s') \<in> rf_sr; valid_pde_mappings' s \<and> asid \<le> mask local.asid_bits; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (valid_pde_mappings' and (\<lambda>_. asid \<le> mask local.asid_bits) and ?R185 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> {s. (s \<in> \<lbrace>v \<noteq> 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> ?C'471 asida rv (ret__struct_pde_C_' t) v va \<inter> \<lbrace>va < 0x100\<rbrace>}} \<inter> {s. pde_get_tag (pde_' (pde_'_update (\<lambda>_. ret__struct_pde_C_' t) s)) = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid}) \<and> (s \<notin> \<lbrace>v \<noteq> 0\<rbrace> \<longrightarrow> s \<in> ?Rf411 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 (7 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); ret__unsigned = stored_hw_asid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C); pde_stored_asid stored_hw_asid___struct_pde_C \<noteq> None\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?G476 asida (pde_stored_asid stored_hw_asid___struct_pde_C)) (?C'471 asida (pde_stored_asid stored_hw_asid___struct_pde_C) stored_hw_asid___struct_pde_C ret__unsigneda ret__unsigned) [] (invalidateHWASIDEntry (the (pde_stored_asid stored_hw_asid___struct_pde_C))) (\<acute>armKSHWASIDTable :== Arrays.update \<acute>armKSHWASIDTable (unat ret__unsigned) (SCAST(32 signed \<rightarrow> 32) asidInvalid))
 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> ccorres dc xfdc (?Pf413 asida (pde_stored_asid stored_hw_asid___struct_pde_C)) (?Rf411 asida (pde_stored_asid stored_hw_asid___struct_pde_C) stored_hw_asid___struct_pde_C ret__unsigned) [] (return ()) SKIP
 3. \<And>asida stored_hw_asid___struct_pde_C ret__unsigned y rv'. \<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); dc y rv'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q395 asida stored_hw_asid___struct_pde_C ret__unsigned y) (?Q'395 asida stored_hw_asid___struct_pde_C ret__unsigned y rv') [SKIP] (invalidateASID asid) (CALL invalidateASID_'proc(asida))
 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> \<lbrace>?R398 asida (pde_stored_asid stored_hw_asid___struct_pde_C)\<rbrace> if \<exists>y. pde_stored_asid stored_hw_asid___struct_pde_C = Some y then invalidateHWASIDEntry (the (pde_stored_asid stored_hw_asid___struct_pde_C)) else return () \<lbrace>?Q395 asida stored_hw_asid___struct_pde_C ret__unsigned\<rbrace>
 5. \<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> guard_is_UNIV dc xfdc (?Q'395 asida stored_hw_asid___struct_pde_C ret__unsigned)
 6. \<And>asida. asida = asid \<Longrightarrow> \<lbrace>?R185 asida\<rbrace> loadHWASID asid \<lbrace>\<lambda>a. (\<lambda>_. True) and (\<lambda>s. (\<exists>y. a = Some y) \<longrightarrow> (?G476 asida a and (\<lambda>_. a \<noteq> None)) s) and (\<lambda>s. (\<nexists>y. a = Some y) \<longrightarrow> ?Pf413 asida a s) and ?R398 asida a\<rbrace>
 7. \<And>asida s s'. \<lbrakk>asida = asid; (s, s') \<in> rf_sr; valid_pde_mappings' s \<and> asid \<le> mask local.asid_bits; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (valid_pde_mappings' and (\<lambda>_. asid \<le> mask local.asid_bits) and ?R185 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> {s. (s \<in> \<lbrace>v \<noteq> 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> ?C'471 asida rv (ret__struct_pde_C_' t) v va \<inter> \<lbrace>va < 0x100\<rbrace>}} \<inter> {s. pde_get_tag (pde_' (pde_'_update (\<lambda>_. ret__struct_pde_C_' t) s)) = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid}) \<and> (s \<notin> \<lbrace>v \<noteq> 0\<rbrace> \<longrightarrow> s \<in> ?Rf411 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 (7 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); ret__unsigned = stored_hw_asid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C); pde_stored_asid stored_hw_asid___struct_pde_C \<noteq> None\<rbrakk> \<Longrightarrow> unat ret__unsigned = unat (the (pde_stored_asid stored_hw_asid___struct_pde_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)\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Pf413 asida (pde_stored_asid stored_hw_asid___struct_pde_C)) (?Rf411 asida (pde_stored_asid stored_hw_asid___struct_pde_C) stored_hw_asid___struct_pde_C ret__unsigned) [] (return ()) SKIP
 3. \<And>asida stored_hw_asid___struct_pde_C ret__unsigned y rv'. \<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); dc y rv'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q395 asida stored_hw_asid___struct_pde_C ret__unsigned y) (?Q'395 asida stored_hw_asid___struct_pde_C ret__unsigned y rv') [SKIP] (invalidateASID asid) (CALL invalidateASID_'proc(asida))
 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> \<lbrace>?R398 asida (pde_stored_asid stored_hw_asid___struct_pde_C)\<rbrace> if \<exists>y. pde_stored_asid stored_hw_asid___struct_pde_C = Some y then invalidateHWASIDEntry (the (pde_stored_asid stored_hw_asid___struct_pde_C)) else return () \<lbrace>?Q395 asida stored_hw_asid___struct_pde_C ret__unsigned\<rbrace>
 5. \<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> guard_is_UNIV dc xfdc (?Q'395 asida stored_hw_asid___struct_pde_C ret__unsigned)
 6. \<And>asida. asida = asid \<Longrightarrow> \<lbrace>?R185 asida\<rbrace> loadHWASID asid \<lbrace>\<lambda>a. (\<lambda>_. True) and (\<lambda>s. (\<exists>y. a = Some y) \<longrightarrow> ((\<lambda>a. True) and (\<lambda>_. a \<noteq> None)) s) and (\<lambda>s. (\<nexists>y. a = Some y) \<longrightarrow> ?Pf413 asida a s) and ?R398 asida a\<rbrace>
 7. \<And>asida s s'. \<lbrakk>asida = asid; (s, s') \<in> rf_sr; valid_pde_mappings' s \<and> asid \<le> mask local.asid_bits; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (valid_pde_mappings' and (\<lambda>_. asid \<le> mask local.asid_bits) and ?R185 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> {s. (s \<in> \<lbrace>v \<noteq> 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> UNIV \<inter> \<lbrace>v < 0x100\<rbrace>}} \<inter> {s. pde_get_tag (pde_' (pde_'_update (\<lambda>_. ret__struct_pde_C_' t) s)) = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid}) \<and> (s \<notin> \<lbrace>v \<noteq> 0\<rbrace> \<longrightarrow> s \<in> ?Rf411 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 (7 subgoals):
 1. \<And>stored_hw_asid___struct_pde_C. \<lbrakk>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> unat (stored_hw_asid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C)) = unat (stored_hw_asid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C)) mod 256
 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> ccorres dc xfdc (?Pf413 asida (pde_stored_asid stored_hw_asid___struct_pde_C)) (?Rf411 asida (pde_stored_asid stored_hw_asid___struct_pde_C) stored_hw_asid___struct_pde_C ret__unsigned) [] (return ()) SKIP
 3. \<And>asida stored_hw_asid___struct_pde_C ret__unsigned y rv'. \<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); dc y rv'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q395 asida stored_hw_asid___struct_pde_C ret__unsigned y) (?Q'395 asida stored_hw_asid___struct_pde_C ret__unsigned y rv') [SKIP] (invalidateASID asid) (CALL invalidateASID_'proc(asida))
 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> \<lbrace>?R398 asida (pde_stored_asid stored_hw_asid___struct_pde_C)\<rbrace> if \<exists>y. pde_stored_asid stored_hw_asid___struct_pde_C = Some y then invalidateHWASIDEntry (the (pde_stored_asid stored_hw_asid___struct_pde_C)) else return () \<lbrace>?Q395 asida stored_hw_asid___struct_pde_C ret__unsigned\<rbrace>
 5. \<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> guard_is_UNIV dc xfdc (?Q'395 asida stored_hw_asid___struct_pde_C ret__unsigned)
 6. \<And>asida. asida = asid \<Longrightarrow> \<lbrace>?R185 asida\<rbrace> loadHWASID asid \<lbrace>\<lambda>a. (\<lambda>_. True) and (\<lambda>s. (\<exists>y. a = Some y) \<longrightarrow> ((\<lambda>a. True) and (\<lambda>_. a \<noteq> None)) s) and (\<lambda>s. (\<nexists>y. a = Some y) \<longrightarrow> ?Pf413 asida a s) and ?R398 asida a\<rbrace>
 7. \<And>asida s s'. \<lbrakk>asida = asid; (s, s') \<in> rf_sr; valid_pde_mappings' s \<and> asid \<le> mask local.asid_bits; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (valid_pde_mappings' and (\<lambda>_. asid \<le> mask local.asid_bits) and ?R185 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> {s. (s \<in> \<lbrace>v \<noteq> 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> UNIV \<inter> \<lbrace>v < 0x100\<rbrace>}} \<inter> {s. pde_get_tag (pde_' (pde_'_update (\<lambda>_. ret__struct_pde_C_' t) s)) = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid}) \<and> (s \<notin> \<lbrace>v \<noteq> 0\<rbrace> \<longrightarrow> s \<in> ?Rf411 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 (7 subgoals):
 1. \<And>stored_hw_asid___struct_pde_C. \<lbrakk>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> unat (stored_hw_asid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C)) < 256
 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> ccorres dc xfdc (?Pf413 asida (pde_stored_asid stored_hw_asid___struct_pde_C)) (?Rf411 asida (pde_stored_asid stored_hw_asid___struct_pde_C) stored_hw_asid___struct_pde_C ret__unsigned) [] (return ()) SKIP
 3. \<And>asida stored_hw_asid___struct_pde_C ret__unsigned y rv'. \<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); dc y rv'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q395 asida stored_hw_asid___struct_pde_C ret__unsigned y) (?Q'395 asida stored_hw_asid___struct_pde_C ret__unsigned y rv') [SKIP] (invalidateASID asid) (CALL invalidateASID_'proc(asida))
 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> \<lbrace>?R398 asida (pde_stored_asid stored_hw_asid___struct_pde_C)\<rbrace> if \<exists>y. pde_stored_asid stored_hw_asid___struct_pde_C = Some y then invalidateHWASIDEntry (the (pde_stored_asid stored_hw_asid___struct_pde_C)) else return () \<lbrace>?Q395 asida stored_hw_asid___struct_pde_C ret__unsigned\<rbrace>
 5. \<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> guard_is_UNIV dc xfdc (?Q'395 asida stored_hw_asid___struct_pde_C ret__unsigned)
 6. \<And>asida. asida = asid \<Longrightarrow> \<lbrace>?R185 asida\<rbrace> loadHWASID asid \<lbrace>\<lambda>a. (\<lambda>_. True) and (\<lambda>s. (\<exists>y. a = Some y) \<longrightarrow> ((\<lambda>a. True) and (\<lambda>_. a \<noteq> None)) s) and (\<lambda>s. (\<nexists>y. a = Some y) \<longrightarrow> ?Pf413 asida a s) and ?R398 asida a\<rbrace>
 7. \<And>asida s s'. \<lbrakk>asida = asid; (s, s') \<in> rf_sr; valid_pde_mappings' s \<and> asid \<le> mask local.asid_bits; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (valid_pde_mappings' and (\<lambda>_. asid \<le> mask local.asid_bits) and ?R185 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> {s. (s \<in> \<lbrace>v \<noteq> 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> UNIV \<inter> \<lbrace>v < 0x100\<rbrace>}} \<inter> {s. pde_get_tag (pde_' (pde_'_update (\<lambda>_. ret__struct_pde_C_' t) s)) = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid}) \<and> (s \<notin> \<lbrace>v \<noteq> 0\<rbrace> \<longrightarrow> s \<in> ?Rf411 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 (7 subgoals):
 1. \<And>stored_hw_asid___struct_pde_C. \<lbrakk>pde_get_tag stored_hw_asid___struct_pde_C = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid; to_bool ((pde_C.words_C stored_hw_asid___struct_pde_C.[0] >> 23) && 1)\<rbrakk> \<Longrightarrow> unat ((pde_C.words_C stored_hw_asid___struct_pde_C.[0] >> 24) && mask 8) < 256
 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> ccorres dc xfdc (?Pf413 asida (pde_stored_asid stored_hw_asid___struct_pde_C)) (?Rf411 asida (pde_stored_asid stored_hw_asid___struct_pde_C) stored_hw_asid___struct_pde_C ret__unsigned) [] (return ()) SKIP
 3. \<And>asida stored_hw_asid___struct_pde_C ret__unsigned y rv'. \<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); dc y rv'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q395 asida stored_hw_asid___struct_pde_C ret__unsigned y) (?Q'395 asida stored_hw_asid___struct_pde_C ret__unsigned y rv') [SKIP] (invalidateASID asid) (CALL invalidateASID_'proc(asida))
 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> \<lbrace>?R398 asida (pde_stored_asid stored_hw_asid___struct_pde_C)\<rbrace> if \<exists>y. pde_stored_asid stored_hw_asid___struct_pde_C = Some y then invalidateHWASIDEntry (the (pde_stored_asid stored_hw_asid___struct_pde_C)) else return () \<lbrace>?Q395 asida stored_hw_asid___struct_pde_C ret__unsigned\<rbrace>
 5. \<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> guard_is_UNIV dc xfdc (?Q'395 asida stored_hw_asid___struct_pde_C ret__unsigned)
 6. \<And>asida. asida = asid \<Longrightarrow> \<lbrace>?R185 asida\<rbrace> loadHWASID asid \<lbrace>\<lambda>a. (\<lambda>_. True) and (\<lambda>s. (\<exists>y. a = Some y) \<longrightarrow> ((\<lambda>a. True) and (\<lambda>_. a \<noteq> None)) s) and (\<lambda>s. (\<nexists>y. a = Some y) \<longrightarrow> ?Pf413 asida a s) and ?R398 asida a\<rbrace>
 7. \<And>asida s s'. \<lbrakk>asida = asid; (s, s') \<in> rf_sr; valid_pde_mappings' s \<and> asid \<le> mask local.asid_bits; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (valid_pde_mappings' and (\<lambda>_. asid \<le> mask local.asid_bits) and ?R185 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> {s. (s \<in> \<lbrace>v \<noteq> 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> UNIV \<inter> \<lbrace>v < 0x100\<rbrace>}} \<inter> {s. pde_get_tag (pde_' (pde_'_update (\<lambda>_. ret__struct_pde_C_' t) s)) = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid}) \<and> (s \<notin> \<lbrace>v \<noteq> 0\<rbrace> \<longrightarrow> s \<in> ?Rf411 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 (8 subgoals):
 1. \<And>stored_hw_asid___struct_pde_C. \<lbrakk>pde_get_tag stored_hw_asid___struct_pde_C = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid; to_bool ((pde_C.words_C stored_hw_asid___struct_pde_C.[0] >> 23) && 1)\<rbrakk> \<Longrightarrow> 8 < LENGTH(32)
 2. \<And>stored_hw_asid___struct_pde_C. \<lbrakk>pde_get_tag stored_hw_asid___struct_pde_C = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid; to_bool ((pde_C.words_C stored_hw_asid___struct_pde_C.[0] >> 23) && 1)\<rbrakk> \<Longrightarrow> (pde_C.words_C stored_hw_asid___struct_pde_C.[0] >> 24) && mask 8 < 0x100
 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> ccorres dc xfdc (?Pf413 asida (pde_stored_asid stored_hw_asid___struct_pde_C)) (?Rf411 asida (pde_stored_asid stored_hw_asid___struct_pde_C) stored_hw_asid___struct_pde_C ret__unsigned) [] (return ()) SKIP
 4. \<And>asida stored_hw_asid___struct_pde_C ret__unsigned y rv'. \<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); dc y rv'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q395 asida stored_hw_asid___struct_pde_C ret__unsigned y) (?Q'395 asida stored_hw_asid___struct_pde_C ret__unsigned y rv') [SKIP] (invalidateASID asid) (CALL invalidateASID_'proc(asida))
 5. \<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> \<lbrace>?R398 asida (pde_stored_asid stored_hw_asid___struct_pde_C)\<rbrace> if \<exists>y. pde_stored_asid stored_hw_asid___struct_pde_C = Some y then invalidateHWASIDEntry (the (pde_stored_asid stored_hw_asid___struct_pde_C)) else return () \<lbrace>?Q395 asida stored_hw_asid___struct_pde_C ret__unsigned\<rbrace>
 6. \<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> guard_is_UNIV dc xfdc (?Q'395 asida stored_hw_asid___struct_pde_C ret__unsigned)
 7. \<And>asida. asida = asid \<Longrightarrow> \<lbrace>?R185 asida\<rbrace> loadHWASID asid \<lbrace>\<lambda>a. (\<lambda>_. True) and (\<lambda>s. (\<exists>y. a = Some y) \<longrightarrow> ((\<lambda>a. True) and (\<lambda>_. a \<noteq> None)) s) and (\<lambda>s. (\<nexists>y. a = Some y) \<longrightarrow> ?Pf413 asida a s) and ?R398 asida a\<rbrace>
 8. \<And>asida s s'. \<lbrakk>asida = asid; (s, s') \<in> rf_sr; valid_pde_mappings' s \<and> asid \<le> mask local.asid_bits; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (valid_pde_mappings' and (\<lambda>_. asid \<le> mask local.asid_bits) and ?R185 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> {s. (s \<in> \<lbrace>v \<noteq> 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> UNIV \<inter> \<lbrace>v < 0x100\<rbrace>}} \<inter> {s. pde_get_tag (pde_' (pde_'_update (\<lambda>_. ret__struct_pde_C_' t) s)) = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid}) \<and> (s \<notin> \<lbrace>v \<noteq> 0\<rbrace> \<longrightarrow> s \<in> ?Rf411 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 (7 subgoals):
 1. \<And>stored_hw_asid___struct_pde_C. \<lbrakk>pde_get_tag stored_hw_asid___struct_pde_C = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid; to_bool ((pde_C.words_C stored_hw_asid___struct_pde_C.[0] >> 23) && 1)\<rbrakk> \<Longrightarrow> (pde_C.words_C stored_hw_asid___struct_pde_C.[0] >> 24) && mask 8 < 0x100
 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> ccorres dc xfdc (?Pf413 asida (pde_stored_asid stored_hw_asid___struct_pde_C)) (?Rf411 asida (pde_stored_asid stored_hw_asid___struct_pde_C) stored_hw_asid___struct_pde_C ret__unsigned) [] (return ()) SKIP
 3. \<And>asida stored_hw_asid___struct_pde_C ret__unsigned y rv'. \<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); dc y rv'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q395 asida stored_hw_asid___struct_pde_C ret__unsigned y) (?Q'395 asida stored_hw_asid___struct_pde_C ret__unsigned y rv') [SKIP] (invalidateASID asid) (CALL invalidateASID_'proc(asida))
 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> \<lbrace>?R398 asida (pde_stored_asid stored_hw_asid___struct_pde_C)\<rbrace> if \<exists>y. pde_stored_asid stored_hw_asid___struct_pde_C = Some y then invalidateHWASIDEntry (the (pde_stored_asid stored_hw_asid___struct_pde_C)) else return () \<lbrace>?Q395 asida stored_hw_asid___struct_pde_C ret__unsigned\<rbrace>
 5. \<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> guard_is_UNIV dc xfdc (?Q'395 asida stored_hw_asid___struct_pde_C ret__unsigned)
 6. \<And>asida. asida = asid \<Longrightarrow> \<lbrace>?R185 asida\<rbrace> loadHWASID asid \<lbrace>\<lambda>a. (\<lambda>_. True) and (\<lambda>s. (\<exists>y. a = Some y) \<longrightarrow> ((\<lambda>a. True) and (\<lambda>_. a \<noteq> None)) s) and (\<lambda>s. (\<nexists>y. a = Some y) \<longrightarrow> ?Pf413 asida a s) and ?R398 asida a\<rbrace>
 7. \<And>asida s s'. \<lbrakk>asida = asid; (s, s') \<in> rf_sr; valid_pde_mappings' s \<and> asid \<le> mask local.asid_bits; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (valid_pde_mappings' and (\<lambda>_. asid \<le> mask local.asid_bits) and ?R185 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> {s. (s \<in> \<lbrace>v \<noteq> 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> UNIV \<inter> \<lbrace>v < 0x100\<rbrace>}} \<inter> {s. pde_get_tag (pde_' (pde_'_update (\<lambda>_. ret__struct_pde_C_' t) s)) = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid}) \<and> (s \<notin> \<lbrace>v \<noteq> 0\<rbrace> \<longrightarrow> s \<in> ?Rf411 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 (7 subgoals):
 1. \<And>stored_hw_asid___struct_pde_C. \<lbrakk>pde_get_tag stored_hw_asid___struct_pde_C = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid; to_bool ((pde_C.words_C stored_hw_asid___struct_pde_C.[0] >> 23) && 1)\<rbrakk> \<Longrightarrow> mask 8 < 0x100
 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> ccorres dc xfdc (?Pf413 asida (pde_stored_asid stored_hw_asid___struct_pde_C)) (?Rf411 asida (pde_stored_asid stored_hw_asid___struct_pde_C) stored_hw_asid___struct_pde_C ret__unsigned) [] (return ()) SKIP
 3. \<And>asida stored_hw_asid___struct_pde_C ret__unsigned y rv'. \<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); dc y rv'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q395 asida stored_hw_asid___struct_pde_C ret__unsigned y) (?Q'395 asida stored_hw_asid___struct_pde_C ret__unsigned y rv') [SKIP] (invalidateASID asid) (CALL invalidateASID_'proc(asida))
 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> \<lbrace>?R398 asida (pde_stored_asid stored_hw_asid___struct_pde_C)\<rbrace> if \<exists>y. pde_stored_asid stored_hw_asid___struct_pde_C = Some y then invalidateHWASIDEntry (the (pde_stored_asid stored_hw_asid___struct_pde_C)) else return () \<lbrace>?Q395 asida stored_hw_asid___struct_pde_C ret__unsigned\<rbrace>
 5. \<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> guard_is_UNIV dc xfdc (?Q'395 asida stored_hw_asid___struct_pde_C ret__unsigned)
 6. \<And>asida. asida = asid \<Longrightarrow> \<lbrace>?R185 asida\<rbrace> loadHWASID asid \<lbrace>\<lambda>a. (\<lambda>_. True) and (\<lambda>s. (\<exists>y. a = Some y) \<longrightarrow> ((\<lambda>a. True) and (\<lambda>_. a \<noteq> None)) s) and (\<lambda>s. (\<nexists>y. a = Some y) \<longrightarrow> ?Pf413 asida a s) and ?R398 asida a\<rbrace>
 7. \<And>asida s s'. \<lbrakk>asida = asid; (s, s') \<in> rf_sr; valid_pde_mappings' s \<and> asid \<le> mask local.asid_bits; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (valid_pde_mappings' and (\<lambda>_. asid \<le> mask local.asid_bits) and ?R185 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> {s. (s \<in> \<lbrace>v \<noteq> 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> UNIV \<inter> \<lbrace>v < 0x100\<rbrace>}} \<inter> {s. pde_get_tag (pde_' (pde_'_update (\<lambda>_. ret__struct_pde_C_' t) s)) = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid}) \<and> (s \<notin> \<lbrace>v \<noteq> 0\<rbrace> \<longrightarrow> s \<in> ?Rf411 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> ccorres dc xfdc (?Pf413 asida (pde_stored_asid stored_hw_asid___struct_pde_C)) (?Rf411 asida (pde_stored_asid stored_hw_asid___struct_pde_C) stored_hw_asid___struct_pde_C ret__unsigned) [] (return ()) SKIP
 2. \<And>asida stored_hw_asid___struct_pde_C ret__unsigned y rv'. \<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); dc y rv'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q395 asida stored_hw_asid___struct_pde_C ret__unsigned y) (?Q'395 asida stored_hw_asid___struct_pde_C ret__unsigned y rv') [SKIP] (invalidateASID asid) (CALL invalidateASID_'proc(asida))
 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> \<lbrace>?R398 asida (pde_stored_asid stored_hw_asid___struct_pde_C)\<rbrace> if \<exists>y. pde_stored_asid stored_hw_asid___struct_pde_C = Some y then invalidateHWASIDEntry (the (pde_stored_asid stored_hw_asid___struct_pde_C)) else return () \<lbrace>?Q395 asida stored_hw_asid___struct_pde_C ret__unsigned\<rbrace>
 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> guard_is_UNIV dc xfdc (?Q'395 asida stored_hw_asid___struct_pde_C ret__unsigned)
 5. \<And>asida. asida = asid \<Longrightarrow> \<lbrace>?R185 asida\<rbrace> loadHWASID asid \<lbrace>\<lambda>a. (\<lambda>_. True) and (\<lambda>s. (\<exists>y. a = Some y) \<longrightarrow> ((\<lambda>a. True) and (\<lambda>_. a \<noteq> None)) s) and (\<lambda>s. (\<nexists>y. a = Some y) \<longrightarrow> ?Pf413 asida a s) and ?R398 asida a\<rbrace>
 6. \<And>asida s s'. \<lbrakk>asida = asid; (s, s') \<in> rf_sr; valid_pde_mappings' s \<and> asid \<le> mask local.asid_bits; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (valid_pde_mappings' and (\<lambda>_. asid \<le> mask local.asid_bits) and ?R185 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> {s. (s \<in> \<lbrace>v \<noteq> 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> UNIV \<inter> \<lbrace>v < 0x100\<rbrace>}} \<inter> {s. pde_get_tag (pde_' (pde_'_update (\<lambda>_. ret__struct_pde_C_' t) s)) = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid}) \<and> (s \<notin> \<lbrace>v \<noteq> 0\<rbrace> \<longrightarrow> s \<in> ?Rf411 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 y rv'. \<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); dc y rv'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q395 asida stored_hw_asid___struct_pde_C ret__unsigned y) (?Q'395 asida stored_hw_asid___struct_pde_C ret__unsigned y rv') [SKIP] (invalidateASID asid) (CALL invalidateASID_'proc(asida))
 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> \<lbrace>?R398 asida (pde_stored_asid stored_hw_asid___struct_pde_C)\<rbrace> if \<exists>y. pde_stored_asid stored_hw_asid___struct_pde_C = Some y then invalidateHWASIDEntry (the (pde_stored_asid stored_hw_asid___struct_pde_C)) else return () \<lbrace>?Q395 asida stored_hw_asid___struct_pde_C ret__unsigned\<rbrace>
 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> guard_is_UNIV dc xfdc (?Q'395 asida stored_hw_asid___struct_pde_C ret__unsigned)
 4. \<And>asida. asida = asid \<Longrightarrow> \<lbrace>?R185 asida\<rbrace> loadHWASID asid \<lbrace>\<lambda>a. (\<lambda>_. True) and (\<lambda>s. (\<exists>y. a = Some y) \<longrightarrow> ((\<lambda>a. True) and (\<lambda>_. a \<noteq> None)) s) and (\<lambda>s. (\<nexists>y. a = Some y) \<longrightarrow> True) and ?R398 asida a\<rbrace>
 5. \<And>asida s s'. \<lbrakk>asida = asid; (s, s') \<in> rf_sr; valid_pde_mappings' s \<and> asid \<le> mask local.asid_bits; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (valid_pde_mappings' and (\<lambda>_. asid \<le> mask local.asid_bits) and ?R185 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> {s. (s \<in> \<lbrace>v \<noteq> 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> UNIV \<inter> \<lbrace>v < 0x100\<rbrace>}} \<inter> {s. pde_get_tag (pde_' (pde_'_update (\<lambda>_. ret__struct_pde_C_' t) s)) = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid}) \<and> (s \<notin> \<lbrace>v \<noteq> 0\<rbrace> \<longrightarrow> s \<in> UNIV)}}} \<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)\<rbrakk> \<Longrightarrow> \<lbrace>?R398 asida (pde_stored_asid stored_hw_asid___struct_pde_C)\<rbrace> if \<exists>y. pde_stored_asid stored_hw_asid___struct_pde_C = Some y then invalidateHWASIDEntry (the (pde_stored_asid stored_hw_asid___struct_pde_C)) else return () \<lbrace>\<lambda>y. valid_pde_mappings' and (\<lambda>_. asid \<le> mask local.asid_bits)\<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)\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (\<lambda>y rv'. {s. asid_'_update (\<lambda>_. asida) s \<in> UNIV \<inter> \<lbrace>\<acute>asid = asid\<rbrace>})
 3. \<And>asida. asida = asid \<Longrightarrow> \<lbrace>?R185 asida\<rbrace> loadHWASID asid \<lbrace>\<lambda>a. (\<lambda>_. True) and (\<lambda>s. (\<exists>y. a = Some y) \<longrightarrow> ((\<lambda>a. True) and (\<lambda>_. a \<noteq> None)) s) and (\<lambda>s. (\<nexists>y. a = Some y) \<longrightarrow> True) and ?R398 asida a\<rbrace>
 4. \<And>asida s s'. \<lbrakk>asida = asid; (s, s') \<in> rf_sr; valid_pde_mappings' s \<and> asid \<le> mask local.asid_bits; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (valid_pde_mappings' and (\<lambda>_. asid \<le> mask local.asid_bits) and ?R185 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> {s. (s \<in> \<lbrace>v \<noteq> 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> UNIV \<inter> \<lbrace>v < 0x100\<rbrace>}} \<inter> {s. pde_get_tag (pde_' (pde_'_update (\<lambda>_. ret__struct_pde_C_' t) s)) = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid}) \<and> (s \<notin> \<lbrace>v \<noteq> 0\<rbrace> \<longrightarrow> s \<in> UNIV)}}} \<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> guard_is_UNIV dc xfdc (\<lambda>y rv'. {s. asid_'_update (\<lambda>_. asida) s \<in> UNIV \<inter> \<lbrace>\<acute>asid = asid\<rbrace>})
 2. \<And>asida. asida = asid \<Longrightarrow> \<lbrace>?R185 asida\<rbrace> loadHWASID asid \<lbrace>\<lambda>a. (\<lambda>_. True) and (\<lambda>s. (\<exists>y. a = Some y) \<longrightarrow> ((\<lambda>a. True) and (\<lambda>_. a \<noteq> None)) s) and (\<lambda>s. (\<nexists>y. a = Some y) \<longrightarrow> True) and (\<lambda>b. ((\<exists>y. a = Some y) \<longrightarrow> valid_pde_mappings' b \<and> asid \<le> mask local.asid_bits) \<and> ((\<nexists>y. a = Some y) \<longrightarrow> valid_pde_mappings' b \<and> asid \<le> mask local.asid_bits))\<rbrace>
 3. \<And>asida s s'. \<lbrakk>asida = asid; (s, s') \<in> rf_sr; valid_pde_mappings' s \<and> asid \<le> mask local.asid_bits; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (valid_pde_mappings' and (\<lambda>_. asid \<le> mask local.asid_bits) and ?R185 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> {s. (s \<in> \<lbrace>v \<noteq> 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> UNIV \<inter> \<lbrace>v < 0x100\<rbrace>}} \<inter> {s. pde_get_tag (pde_' (pde_'_update (\<lambda>_. ret__struct_pde_C_' t) s)) = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid}) \<and> (s \<notin> \<lbrace>v \<noteq> 0\<rbrace> \<longrightarrow> s \<in> UNIV)}}} \<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>?R185 asida\<rbrace> loadHWASID asid \<lbrace>\<lambda>a. (\<lambda>_. True) and (\<lambda>s. (\<exists>y. a = Some y) \<longrightarrow> ((\<lambda>a. True) and (\<lambda>_. a \<noteq> None)) s) and (\<lambda>s. (\<nexists>y. a = Some y) \<longrightarrow> True) and (\<lambda>b. ((\<exists>y. a = Some y) \<longrightarrow> valid_pde_mappings' b \<and> asid \<le> mask local.asid_bits) \<and> ((\<nexists>y. a = Some y) \<longrightarrow> valid_pde_mappings' b \<and> asid \<le> mask local.asid_bits))\<rbrace>
 2. \<And>asida s s'. \<lbrakk>asida = asid; (s, s') \<in> rf_sr; valid_pde_mappings' s \<and> asid \<le> mask local.asid_bits; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (valid_pde_mappings' and (\<lambda>_. asid \<le> mask local.asid_bits) and ?R185 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> {s. (s \<in> \<lbrace>v \<noteq> 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> UNIV \<inter> \<lbrace>v < 0x100\<rbrace>}} \<inter> {s. pde_get_tag (pde_' (pde_'_update (\<lambda>_. ret__struct_pde_C_' t) s)) = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid}) \<and> (s \<notin> \<lbrace>v \<noteq> 0\<rbrace> \<longrightarrow> s \<in> UNIV)}}} \<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' s \<and> asid \<le> mask local.asid_bits; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (valid_pde_mappings' and (\<lambda>_. asid \<le> mask local.asid_bits) and (\<lambda>s. ((\<lambda>_. True) and (\<lambda>sa. (\<exists>y. map_option fst (armKSASIDMap (ksArchState s) asid) = Some y) \<longrightarrow> ((\<lambda>a. True) and (\<lambda>_. map_option fst (armKSASIDMap (ksArchState s) asid) \<noteq> None)) sa) and (\<lambda>sa. (\<nexists>y. map_option fst (armKSASIDMap (ksArchState s) asid) = Some y) \<longrightarrow> True) and (\<lambda>a. ((\<exists>y. map_option fst (armKSASIDMap (ksArchState s) asid) = Some y) \<longrightarrow> valid_pde_mappings' a \<and> asid \<le> mask local.asid_bits) \<and> ((\<nexists>y. map_option fst (armKSASIDMap (ksArchState s) asid) = Some y) \<longrightarrow> valid_pde_mappings' a \<and> asid \<le> mask local.asid_bits))) 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> {s. (s \<in> \<lbrace>v \<noteq> 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> UNIV \<inter> \<lbrace>v < 0x100\<rbrace>}} \<inter> {s. pde_get_tag (pde_' (pde_'_update (\<lambda>_. ret__struct_pde_C_' t) s)) = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid}) \<and> (s \<notin> \<lbrace>v \<noteq> 0\<rbrace> \<longrightarrow> s \<in> UNIV)}}} \<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!