theory VSpace_C

lemma getHWASID_ccorres:
  "ccorres (=) ret__unsigned_char_'
     (all_invs_but_ct_idle_or_in_cur_domain' and (\<lambda>s. asid \<le> mask asid_bits)) (UNIV \<inter> {s. asid_' s = asid}) []
     (getHWASID asid) (Call getHWASID_'proc)" apply (cinit lift: asid_') apply (ctac(no_vcg) add: loadHWASID_ccorres) apply csymbr apply wpc apply (rule ccorres_cond_false) apply (rule ccorres_rhs_assoc)+ apply csymbr apply simp apply (ctac(no_vcg) add: findFreeHWASID_ccorres) apply (ctac(no_vcg) add: storeHWASID_ccorres) apply (rule ccorres_return_C, simp+)[1] apply wp+ apply (strengthen all_invs_but_ct_idle_or_in_cur_domain_valid_pde_mappings') apply (wp findFreeHWASID_invs_no_cicd') apply (rule ccorres_cond_true) apply (rule ccorres_from_vcg_throws[where P=\<top> and P'=UNIV]) apply (rule allI, rule conseqPre, vcg) apply (clarsimp simp: return_def pde_stored_asid_def
                   split: if_split_asm) apply wp apply (clarsimp simp: pde_stored_asid_def) apply (clarsimp simp: to_bool_def split: if_split) apply (auto simp: all_invs_but_ct_idle_or_in_cur_domain'_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres (=) ret__unsigned_char_' (all_invs_but_ct_idle_or_in_cur_domain' and (\<lambda>s. asid \<le> mask local.asid_bits)) (UNIV \<inter> \<lbrace>\<acute>asid = asid\<rbrace>) [] (getHWASID asid) (Call getHWASID_'proc) proof (prove)
goal (2 subgoals):
 1. \<And>asida. asida = asid \<Longrightarrow> ccorres (=) ret__unsigned_char_' (?Q234 asida) (?Q'234 asida) [SKIP] (do maybe_hw_asid <- loadHWASID asid;
case maybe_hw_asid of None \<Rightarrow> do new_hw_asid <- findFreeHWASID;
storeHWASID asid new_hw_asid;
return new_hw_asid
od | Some hw_asid \<Rightarrow> return 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 \<noteq> 0 THEN
  \<acute>ret__unsigned :== CALL pde_pde_invalid_get_stored_hw_asid_'proc(\<acute>stored_hw_asid___struct_pde_C);;
return_C ret__unsigned_char_'_update (\<lambda>s. UCAST(32 \<rightarrow> 8) (ret__unsigned_' s))
ELSE
  lvar_nondet_init new_hw_asid_' new_hw_asid_'_update;;
\<acute>new_hw_asid :== CALL findFreeHWASID_'proc();;
CALL storeHWASID_'proc(asida,\<acute>new_hw_asid);;
return_C ret__unsigned_char_'_update new_hw_asid_'
FI))
 2. \<And>asida s s'. \<lbrakk>asida = asid; (s, s') \<in> rf_sr; (all_invs_but_ct_idle_or_in_cur_domain' and (\<lambda>s. asid \<le> mask local.asid_bits)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q234 asida s \<and> s' \<in> ?Q'234 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 (=) ret__unsigned_char_' (?Q242 asida rv) (?Q'242 asida rv stored_hw_asid___struct_pde_C) [SKIP] (case rv of None \<Rightarrow> do new_hw_asid <- findFreeHWASID;
storeHWASID asid new_hw_asid;
return new_hw_asid
od | Some hw_asid \<Rightarrow> return hw_asid) (\<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);;
return_C ret__unsigned_char_'_update (\<lambda>s. UCAST(32 \<rightarrow> 8) (ret__unsigned_' s))
ELSE
  lvar_nondet_init new_hw_asid_' new_hw_asid_'_update;;
\<acute>new_hw_asid :== CALL findFreeHWASID_'proc();;
CALL storeHWASID_'proc(asida,\<acute>new_hw_asid);;
return_C ret__unsigned_char_'_update new_hw_asid_'
FI)
 2. \<And>asida. asida = asid \<Longrightarrow> \<lbrace>?R242 asida\<rbrace> loadHWASID asid \<lbrace>?Q242 asida\<rbrace>
 3. \<And>asida s s'. \<lbrakk>asida = asid; (s, s') \<in> rf_sr; (all_invs_but_ct_idle_or_in_cur_domain' and (\<lambda>s. asid \<le> mask local.asid_bits)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (valid_pde_mappings' and (\<lambda>_. asid \<le> mask local.asid_bits) and ?R242 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'242 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 (=) ret__unsigned_char_' (?Q242 asida (pde_stored_asid stored_hw_asid___struct_pde_C)) (?G'417 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> do new_hw_asid <- findFreeHWASID;
storeHWASID asid new_hw_asid;
return new_hw_asid
od | Some x \<Rightarrow> return x) (IF ret__unsigned \<noteq> 0 THEN
  \<acute>ret__unsigned :== CALL pde_pde_invalid_get_stored_hw_asid_'proc(stored_hw_asid___struct_pde_C);;
return_C ret__unsigned_char_'_update (\<lambda>s. UCAST(32 \<rightarrow> 8) (ret__unsigned_' s))
ELSE
  lvar_nondet_init new_hw_asid_' new_hw_asid_'_update;;
\<acute>new_hw_asid :== CALL findFreeHWASID_'proc();;
CALL storeHWASID_'proc(asida,\<acute>new_hw_asid);;
return_C ret__unsigned_char_'_update new_hw_asid_'
FI)
 2. \<And>asida. asida = asid \<Longrightarrow> \<lbrace>?R242 asida\<rbrace> loadHWASID asid \<lbrace>?Q242 asida\<rbrace>
 3. \<And>asida s s'. \<lbrakk>asida = asid; (s, s') \<in> rf_sr; (all_invs_but_ct_idle_or_in_cur_domain' and (\<lambda>s. asid \<le> mask local.asid_bits)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (valid_pde_mappings' and (\<lambda>_. asid \<le> mask local.asid_bits) and ?R242 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'417 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); pde_stored_asid stored_hw_asid___struct_pde_C = None\<rbrakk> \<Longrightarrow> ccorres (=) ret__unsigned_char_' (?R570 asida (pde_stored_asid stored_hw_asid___struct_pde_C)) (?R''572 asida (pde_stored_asid stored_hw_asid___struct_pde_C) stored_hw_asid___struct_pde_C ret__unsigned) [SKIP] (do new_hw_asid <- findFreeHWASID;
storeHWASID asid new_hw_asid;
return new_hw_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);;
return_C ret__unsigned_char_'_update (\<lambda>s. UCAST(32 \<rightarrow> 8) (ret__unsigned_' s))
ELSE
  lvar_nondet_init new_hw_asid_' new_hw_asid_'_update;;
\<acute>new_hw_asid :== CALL findFreeHWASID_'proc();;
CALL storeHWASID_'proc(asida,\<acute>new_hw_asid);;
return_C ret__unsigned_char_'_update new_hw_asid_'
FI)
 2. \<And>asida stored_hw_asid___struct_pde_C ret__unsigned x2. \<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); pde_stored_asid stored_hw_asid___struct_pde_C = Some x2\<rbrakk> \<Longrightarrow> ccorres (=) ret__unsigned_char_' (\<lambda>a. ?R569 asida (pde_stored_asid stored_hw_asid___struct_pde_C) a x2) (?R''571 asida (pde_stored_asid stored_hw_asid___struct_pde_C) stored_hw_asid___struct_pde_C ret__unsigned x2) [SKIP] (return x2) (IF ret__unsigned \<noteq> 0 THEN
  \<acute>ret__unsigned :== CALL pde_pde_invalid_get_stored_hw_asid_'proc(stored_hw_asid___struct_pde_C);;
return_C ret__unsigned_char_'_update (\<lambda>s. UCAST(32 \<rightarrow> 8) (ret__unsigned_' s))
ELSE
  lvar_nondet_init new_hw_asid_' new_hw_asid_'_update;;
\<acute>new_hw_asid :== CALL findFreeHWASID_'proc();;
CALL storeHWASID_'proc(asida,\<acute>new_hw_asid);;
return_C ret__unsigned_char_'_update new_hw_asid_'
FI)
 3. \<And>asida. asida = asid \<Longrightarrow> \<lbrace>?R242 asida\<rbrace> loadHWASID asid \<lbrace>\<lambda>a b. (a = None \<longrightarrow> ?R570 asida a b) \<and> (\<forall>x. a = Some x \<longrightarrow> ?R569 asida a b x)\<rbrace>
 4. \<And>asida s s'. \<lbrakk>asida = asid; (s, s') \<in> rf_sr; (all_invs_but_ct_idle_or_in_cur_domain' and (\<lambda>s. asid \<le> mask local.asid_bits)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (valid_pde_mappings' and (\<lambda>_. asid \<le> mask local.asid_bits) and ?R242 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. rv = None \<longrightarrow> s \<in> ?R''572 asida rv (ret__struct_pde_C_' t) v} \<inter> {s. \<forall>x. s \<in> {s. rv = Some x \<longrightarrow> s \<in> ?R''571 asida rv (ret__struct_pde_C_' t) v x}}}} \<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); pde_stored_asid stored_hw_asid___struct_pde_C = None\<rbrakk> \<Longrightarrow> ccorres (=) ret__unsigned_char_' (?R570 asida (pde_stored_asid stored_hw_asid___struct_pde_C)) (?R'578 asida (pde_stored_asid stored_hw_asid___struct_pde_C) stored_hw_asid___struct_pde_C ret__unsigned) [SKIP] (do new_hw_asid <- findFreeHWASID;
storeHWASID asid new_hw_asid;
return new_hw_asid
od) (lvar_nondet_init new_hw_asid_' new_hw_asid_'_update;;
\<acute>new_hw_asid :== CALL findFreeHWASID_'proc();;
CALL storeHWASID_'proc(asida,\<acute>new_hw_asid);;
return_C ret__unsigned_char_'_update new_hw_asid_')
 2. \<And>asida stored_hw_asid___struct_pde_C ret__unsigned x2. \<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); pde_stored_asid stored_hw_asid___struct_pde_C = Some x2\<rbrakk> \<Longrightarrow> ccorres (=) ret__unsigned_char_' (\<lambda>a. ?R569 asida (pde_stored_asid stored_hw_asid___struct_pde_C) a x2) (?R''571 asida (pde_stored_asid stored_hw_asid___struct_pde_C) stored_hw_asid___struct_pde_C ret__unsigned x2) [SKIP] (return x2) (IF ret__unsigned \<noteq> 0 THEN
  \<acute>ret__unsigned :== CALL pde_pde_invalid_get_stored_hw_asid_'proc(stored_hw_asid___struct_pde_C);;
return_C ret__unsigned_char_'_update (\<lambda>s. UCAST(32 \<rightarrow> 8) (ret__unsigned_' s))
ELSE
  lvar_nondet_init new_hw_asid_' new_hw_asid_'_update;;
\<acute>new_hw_asid :== CALL findFreeHWASID_'proc();;
CALL storeHWASID_'proc(asida,\<acute>new_hw_asid);;
return_C ret__unsigned_char_'_update new_hw_asid_'
FI)
 3. \<And>asida. asida = asid \<Longrightarrow> \<lbrace>?R242 asida\<rbrace> loadHWASID asid \<lbrace>\<lambda>a b. (a = None \<longrightarrow> ?R570 asida a b) \<and> (\<forall>x. a = Some x \<longrightarrow> ?R569 asida a b x)\<rbrace>
 4. \<And>asida s s'. \<lbrakk>asida = asid; (s, s') \<in> rf_sr; (all_invs_but_ct_idle_or_in_cur_domain' and (\<lambda>s. asid \<le> mask local.asid_bits)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (valid_pde_mappings' and (\<lambda>_. asid \<le> mask local.asid_bits) and ?R242 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. rv = None \<longrightarrow> s \<in> ?R'578 asida rv (ret__struct_pde_C_' t) v \<inter> - \<lbrace>v \<noteq> 0\<rbrace>} \<inter> {s. \<forall>x. s \<in> {s. rv = Some x \<longrightarrow> s \<in> ?R''571 asida rv (ret__struct_pde_C_' t) v x}}}} \<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); pde_stored_asid stored_hw_asid___struct_pde_C = None\<rbrakk> \<Longrightarrow> ccorres (=) ret__unsigned_char_' (?R570 asida (pde_stored_asid stored_hw_asid___struct_pde_C)) (?R'578 asida (pde_stored_asid stored_hw_asid___struct_pde_C) stored_hw_asid___struct_pde_C ret__unsigned) [SKIP] (do new_hw_asid <- findFreeHWASID;
storeHWASID asid new_hw_asid;
return new_hw_asid
od) (lvar_nondet_init new_hw_asid_' new_hw_asid_'_update;;
(\<acute>new_hw_asid :== CALL findFreeHWASID_'proc();;
(CALL storeHWASID_'proc(asida,\<acute>new_hw_asid);;
return_C ret__unsigned_char_'_update new_hw_asid_')))
 2. \<And>asida stored_hw_asid___struct_pde_C ret__unsigned x2. \<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); pde_stored_asid stored_hw_asid___struct_pde_C = Some x2\<rbrakk> \<Longrightarrow> ccorres (=) ret__unsigned_char_' (\<lambda>a. ?R569 asida (pde_stored_asid stored_hw_asid___struct_pde_C) a x2) (?R''571 asida (pde_stored_asid stored_hw_asid___struct_pde_C) stored_hw_asid___struct_pde_C ret__unsigned x2) [SKIP] (return x2) (IF ret__unsigned \<noteq> 0 THEN
  \<acute>ret__unsigned :== CALL pde_pde_invalid_get_stored_hw_asid_'proc(stored_hw_asid___struct_pde_C);;
return_C ret__unsigned_char_'_update (\<lambda>s. UCAST(32 \<rightarrow> 8) (ret__unsigned_' s))
ELSE
  lvar_nondet_init new_hw_asid_' new_hw_asid_'_update;;
\<acute>new_hw_asid :== CALL findFreeHWASID_'proc();;
CALL storeHWASID_'proc(asida,\<acute>new_hw_asid);;
return_C ret__unsigned_char_'_update new_hw_asid_'
FI)
 3. \<And>asida. asida = asid \<Longrightarrow> \<lbrace>?R242 asida\<rbrace> loadHWASID asid \<lbrace>\<lambda>a b. (a = None \<longrightarrow> ?R570 asida a b) \<and> (\<forall>x. a = Some x \<longrightarrow> ?R569 asida a b x)\<rbrace>
 4. \<And>asida s s'. \<lbrakk>asida = asid; (s, s') \<in> rf_sr; (all_invs_but_ct_idle_or_in_cur_domain' and (\<lambda>s. asid \<le> mask local.asid_bits)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (valid_pde_mappings' and (\<lambda>_. asid \<le> mask local.asid_bits) and ?R242 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. rv = None \<longrightarrow> s \<in> ?R'578 asida rv (ret__struct_pde_C_' t) v \<inter> - \<lbrace>v \<noteq> 0\<rbrace>} \<inter> {s. \<forall>x. s \<in> {s. rv = Some x \<longrightarrow> s \<in> ?R''571 asida rv (ret__struct_pde_C_' t) v x}}}} \<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); pde_stored_asid stored_hw_asid___struct_pde_C = None\<rbrakk> \<Longrightarrow> ccorres (=) ret__unsigned_char_' (?R570 asida (pde_stored_asid stored_hw_asid___struct_pde_C)) (?G'593 asida (pde_stored_asid stored_hw_asid___struct_pde_C) stored_hw_asid___struct_pde_C ret__unsigned) [SKIP] (do new_hw_asid <- findFreeHWASID;
storeHWASID asid new_hw_asid;
return new_hw_asid
od) (\<acute>new_hw_asid :== CALL findFreeHWASID_'proc();;
(CALL storeHWASID_'proc(asida,\<acute>new_hw_asid);;
return_C ret__unsigned_char_'_update new_hw_asid_'))
 2. \<And>asida stored_hw_asid___struct_pde_C ret__unsigned x2. \<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); pde_stored_asid stored_hw_asid___struct_pde_C = Some x2\<rbrakk> \<Longrightarrow> ccorres (=) ret__unsigned_char_' (\<lambda>a. ?R569 asida (pde_stored_asid stored_hw_asid___struct_pde_C) a x2) (?R''571 asida (pde_stored_asid stored_hw_asid___struct_pde_C) stored_hw_asid___struct_pde_C ret__unsigned x2) [SKIP] (return x2) (IF ret__unsigned \<noteq> 0 THEN
  \<acute>ret__unsigned :== CALL pde_pde_invalid_get_stored_hw_asid_'proc(stored_hw_asid___struct_pde_C);;
return_C ret__unsigned_char_'_update (\<lambda>s. UCAST(32 \<rightarrow> 8) (ret__unsigned_' s))
ELSE
  lvar_nondet_init new_hw_asid_' new_hw_asid_'_update;;
\<acute>new_hw_asid :== CALL findFreeHWASID_'proc();;
CALL storeHWASID_'proc(asida,\<acute>new_hw_asid);;
return_C ret__unsigned_char_'_update new_hw_asid_'
FI)
 3. \<And>asida. asida = asid \<Longrightarrow> \<lbrace>?R242 asida\<rbrace> loadHWASID asid \<lbrace>\<lambda>a b. (a = None \<longrightarrow> ?R570 asida a b) \<and> (\<forall>x. a = Some x \<longrightarrow> ?R569 asida a b x)\<rbrace>
 4. \<And>asida s s'. \<lbrakk>asida = asid; (s, s') \<in> rf_sr; (all_invs_but_ct_idle_or_in_cur_domain' and (\<lambda>s. asid \<le> mask local.asid_bits)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (valid_pde_mappings' and (\<lambda>_. asid \<le> mask local.asid_bits) and ?R242 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. rv = None \<longrightarrow> s \<in> {s. \<forall>va. new_hw_asid_'_update (\<lambda>_. va) s \<in> ?G'593 asida rv (ret__struct_pde_C_' t) v} \<inter> - \<lbrace>v \<noteq> 0\<rbrace>} \<inter> {s. \<forall>x. s \<in> {s. rv = Some x \<longrightarrow> s \<in> ?R''571 asida rv (ret__struct_pde_C_' t) v x}}}} \<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); pde_stored_asid stored_hw_asid___struct_pde_C = None\<rbrakk> \<Longrightarrow> ccorres (=) ret__unsigned_char_' (?R570 asid None) (?G'593 asid None stored_hw_asid___struct_pde_C (stored_asid_valid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C))) [SKIP] (do new_hw_asid <- findFreeHWASID;
y <- storeHWASID asid new_hw_asid;
return new_hw_asid
od) (\<acute>new_hw_asid :== CALL findFreeHWASID_'proc();;
(CALL storeHWASID_'proc(asid,\<acute>new_hw_asid);;
return_C ret__unsigned_char_'_update new_hw_asid_'))
 2. \<And>asida stored_hw_asid___struct_pde_C ret__unsigned x2. \<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); pde_stored_asid stored_hw_asid___struct_pde_C = Some x2\<rbrakk> \<Longrightarrow> ccorres (=) ret__unsigned_char_' (\<lambda>a. ?R569 asida (pde_stored_asid stored_hw_asid___struct_pde_C) a x2) (?R''571 asida (pde_stored_asid stored_hw_asid___struct_pde_C) stored_hw_asid___struct_pde_C ret__unsigned x2) [SKIP] (return x2) (IF ret__unsigned \<noteq> 0 THEN
  \<acute>ret__unsigned :== CALL pde_pde_invalid_get_stored_hw_asid_'proc(stored_hw_asid___struct_pde_C);;
return_C ret__unsigned_char_'_update (\<lambda>s. UCAST(32 \<rightarrow> 8) (ret__unsigned_' s))
ELSE
  lvar_nondet_init new_hw_asid_' new_hw_asid_'_update;;
\<acute>new_hw_asid :== CALL findFreeHWASID_'proc();;
CALL storeHWASID_'proc(asida,\<acute>new_hw_asid);;
return_C ret__unsigned_char_'_update new_hw_asid_'
FI)
 3. \<And>asida. asida = asid \<Longrightarrow> \<lbrace>?R242 asida\<rbrace> loadHWASID asid \<lbrace>\<lambda>a b. (a = None \<longrightarrow> ?R570 asida a b) \<and> (\<forall>x. a = Some x \<longrightarrow> ?R569 asida a b x)\<rbrace>
 4. \<And>asida s s'. \<lbrakk>asida = asid; (s, s') \<in> rf_sr; (all_invs_but_ct_idle_or_in_cur_domain' and (\<lambda>s. asid \<le> mask local.asid_bits)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (valid_pde_mappings' and (\<lambda>_. asid \<le> mask local.asid_bits) and ?R242 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. rv = None \<longrightarrow> s \<in> {s. \<forall>va. new_hw_asid_'_update (\<lambda>_. va) s \<in> ?G'593 asida rv (ret__struct_pde_C_' t) v} \<inter> - \<lbrace>v \<noteq> 0\<rbrace>} \<inter> {s. \<forall>x. s \<in> {s. rv = Some x \<longrightarrow> s \<in> ?R''571 asida rv (ret__struct_pde_C_' t) v x}}}} \<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 rv new_hw_asid. \<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); pde_stored_asid stored_hw_asid___struct_pde_C = None; rv = new_hw_asid\<rbrakk> \<Longrightarrow> ccorres (=) ret__unsigned_char_' (?Q607 asida stored_hw_asid___struct_pde_C ret__unsigned rv) (?Q'620 stored_hw_asid___struct_pde_C rv new_hw_asid) [SKIP] (do y <- storeHWASID asid rv;
return rv
od) (CALL storeHWASID_'proc(asid,new_hw_asid);;
return_C ret__unsigned_char_'_update (\<lambda>a. new_hw_asid))
 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); pde_stored_asid stored_hw_asid___struct_pde_C = None\<rbrakk> \<Longrightarrow> \<lbrace>?R615 asid None\<rbrace> findFreeHWASID \<lbrace>?Q607 asida stored_hw_asid___struct_pde_C ret__unsigned\<rbrace>
 3. \<And>asida stored_hw_asid___struct_pde_C ret__unsigned x2. \<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); pde_stored_asid stored_hw_asid___struct_pde_C = Some x2\<rbrakk> \<Longrightarrow> ccorres (=) ret__unsigned_char_' (\<lambda>a. ?R569 asida (pde_stored_asid stored_hw_asid___struct_pde_C) a x2) (?R''571 asida (pde_stored_asid stored_hw_asid___struct_pde_C) stored_hw_asid___struct_pde_C ret__unsigned x2) [SKIP] (return x2) (IF ret__unsigned \<noteq> 0 THEN
  \<acute>ret__unsigned :== CALL pde_pde_invalid_get_stored_hw_asid_'proc(stored_hw_asid___struct_pde_C);;
return_C ret__unsigned_char_'_update (\<lambda>s. UCAST(32 \<rightarrow> 8) (ret__unsigned_' s))
ELSE
  lvar_nondet_init new_hw_asid_' new_hw_asid_'_update;;
\<acute>new_hw_asid :== CALL findFreeHWASID_'proc();;
CALL storeHWASID_'proc(asida,\<acute>new_hw_asid);;
return_C ret__unsigned_char_'_update new_hw_asid_'
FI)
 4. \<And>asida. asida = asid \<Longrightarrow> \<lbrace>?R242 asida\<rbrace> loadHWASID asid \<lbrace>\<lambda>a b. (a = None \<longrightarrow> (valid_arch_state' and valid_pde_mappings' and ?R615 asida a) b) \<and> (\<forall>x. a = Some x \<longrightarrow> ?R569 asida a b x)\<rbrace>
 5. \<And>asida s s'. \<lbrakk>asida = asid; (s, s') \<in> rf_sr; (all_invs_but_ct_idle_or_in_cur_domain' and (\<lambda>s. asid \<le> mask local.asid_bits)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (valid_pde_mappings' and (\<lambda>_. asid \<le> mask local.asid_bits) and ?R242 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. rv = None \<longrightarrow> s \<in> {s. \<forall>va. new_hw_asid_'_update (\<lambda>_. va) s \<in> {s. s \<in> UNIV} \<inter> {s'. \<forall>ta rva. rva = ret__unsigned_char_' ta \<longrightarrow> new_hw_asid_'_update (\<lambda>_. ret__unsigned_char_' ta) (s'\<lparr>globals := globals ta\<rparr>) \<in> ?Q'619 asida rv (ret__struct_pde_C_' t) v ta rva}} \<inter> - \<lbrace>v \<noteq> 0\<rbrace>} \<inter> {s. \<forall>x. s \<in> {s. rv = Some x \<longrightarrow> s \<in> ?R''571 asida rv (ret__struct_pde_C_' t) v x}}}} \<inter> {s. pde_get_tag (pde_' (pde_'_update (\<lambda>_. ret__struct_pde_C_' t) s)) = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid}}
flex-flex pairs:
\<lambda>stored_hw_asid___struct_pde_C t rv. ?Q'620 stored_hw_asid___struct_pde_C rv (ret__unsigned_char_' t) \<equiv>\<^sup>? \<lambda>stored_hw_asid___struct_pde_C. ?Q'619 asid None stored_hw_asid___struct_pde_C (stored_asid_valid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C)) proof (prove)
goal (6 subgoals):
 1. \<And>asida stored_hw_asid___struct_pde_C ret__unsigned rv new_hw_asid rva xfdc. \<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); pde_stored_asid stored_hw_asid___struct_pde_C = None; rv = new_hw_asid; dc rva xfdc\<rbrakk> \<Longrightarrow> ccorres (=) ret__unsigned_char_' (?Q701 asida stored_hw_asid___struct_pde_C ret__unsigned rv new_hw_asid rva) (?Q'719 stored_hw_asid___struct_pde_C rv new_hw_asid rva xfdc) [SKIP] (return rv) (return_C ret__unsigned_char_'_update (\<lambda>a. new_hw_asid))
 2. \<And>asida stored_hw_asid___struct_pde_C ret__unsigned rv new_hw_asid. \<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); pde_stored_asid stored_hw_asid___struct_pde_C = None; rv = new_hw_asid\<rbrakk> \<Longrightarrow> \<lbrace>?R714 asida stored_hw_asid___struct_pde_C ret__unsigned rv\<rbrace> storeHWASID asid rv \<lbrace>?Q701 asida stored_hw_asid___struct_pde_C ret__unsigned rv new_hw_asid\<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); pde_stored_asid stored_hw_asid___struct_pde_C = None\<rbrakk> \<Longrightarrow> \<lbrace>?R615 asid None\<rbrace> findFreeHWASID \<lbrace>\<lambda>a. valid_pde_mappings' and (\<lambda>_. asid \<le> mask local.asid_bits) and ?R714 asida stored_hw_asid___struct_pde_C ret__unsigned a\<rbrace>
 4. \<And>asida stored_hw_asid___struct_pde_C ret__unsigned x2. \<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); pde_stored_asid stored_hw_asid___struct_pde_C = Some x2\<rbrakk> \<Longrightarrow> ccorres (=) ret__unsigned_char_' (\<lambda>a. ?R569 asida (pde_stored_asid stored_hw_asid___struct_pde_C) a x2) (?R''571 asida (pde_stored_asid stored_hw_asid___struct_pde_C) stored_hw_asid___struct_pde_C ret__unsigned x2) [SKIP] (return x2) (IF ret__unsigned \<noteq> 0 THEN
  \<acute>ret__unsigned :== CALL pde_pde_invalid_get_stored_hw_asid_'proc(stored_hw_asid___struct_pde_C);;
return_C ret__unsigned_char_'_update (\<lambda>s. UCAST(32 \<rightarrow> 8) (ret__unsigned_' s))
ELSE
  lvar_nondet_init new_hw_asid_' new_hw_asid_'_update;;
\<acute>new_hw_asid :== CALL findFreeHWASID_'proc();;
CALL storeHWASID_'proc(asida,\<acute>new_hw_asid);;
return_C ret__unsigned_char_'_update new_hw_asid_'
FI)
 5. \<And>asida. asida = asid \<Longrightarrow> \<lbrace>?R242 asida\<rbrace> loadHWASID asid \<lbrace>\<lambda>a b. (a = None \<longrightarrow> (valid_arch_state' and valid_pde_mappings' and ?R615 asida a) b) \<and> (\<forall>x. a = Some x \<longrightarrow> ?R569 asida a b x)\<rbrace>
 6. \<And>asida s s'. \<lbrakk>asida = asid; (s, s') \<in> rf_sr; (all_invs_but_ct_idle_or_in_cur_domain' and (\<lambda>s. asid \<le> mask local.asid_bits)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (valid_pde_mappings' and (\<lambda>_. asid \<le> mask local.asid_bits) and ?R242 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. rv = None \<longrightarrow> s \<in> {s. \<forall>va. new_hw_asid_'_update (\<lambda>_. va) s \<in> {s. s \<in> UNIV} \<inter> {s'. \<forall>ta rva. rva = ret__unsigned_char_' ta \<longrightarrow> new_hw_asid_'_update (\<lambda>_. ret__unsigned_char_' ta) (s'\<lparr>globals := globals ta\<rparr>) \<in> {s. hw_asid_'_update (\<lambda>_. ret__unsigned_char_' ta) (asid_'_update (\<lambda>_. asida) s) \<in> UNIV \<inter> \<lbrace>\<acute>asid = asida\<rbrace> \<inter> \<lbrace>\<acute>hw_asid = UCAST(8 \<rightarrow> 8) rva\<rbrace>} \<inter> {s'. \<forall>tb rvb. dc rvb (xfdc tb) \<longrightarrow> s'\<lparr>globals := globals tb\<rparr> \<in> ?Q'720 asida rv (ret__struct_pde_C_' t) v ta rva tb rvb}}} \<inter> - \<lbrace>v \<noteq> 0\<rbrace>} \<inter> {s. \<forall>x. s \<in> {s. rv = Some x \<longrightarrow> s \<in> ?R''571 asida rv (ret__struct_pde_C_' t) v x}}}} \<inter> {s. pde_get_tag (pde_' (pde_'_update (\<lambda>_. ret__struct_pde_C_' t) s)) = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid}}
flex-flex pairs:
\<lambda>stored_hw_asid___struct_pde_C. ?Q'720 asid None stored_hw_asid___struct_pde_C (stored_asid_valid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C)) \<equiv>\<^sup>? \<lambda>stored_hw_asid___struct_pde_C t rv ta rva. ?Q'719 stored_hw_asid___struct_pde_C rv (ret__unsigned_char_' t) rva (xfdc ta) proof (prove)
goal (5 subgoals):
 1. \<And>asida stored_hw_asid___struct_pde_C ret__unsigned rv new_hw_asid. \<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); pde_stored_asid stored_hw_asid___struct_pde_C = None; rv = new_hw_asid\<rbrakk> \<Longrightarrow> \<lbrace>?R714 asida stored_hw_asid___struct_pde_C ret__unsigned rv\<rbrace> storeHWASID asid rv \<lbrace>\<lambda>a b. True\<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); pde_stored_asid stored_hw_asid___struct_pde_C = None\<rbrakk> \<Longrightarrow> \<lbrace>?R615 asid None\<rbrace> findFreeHWASID \<lbrace>\<lambda>a. valid_pde_mappings' and (\<lambda>_. asid \<le> mask local.asid_bits) and ?R714 asida stored_hw_asid___struct_pde_C ret__unsigned a\<rbrace>
 3. \<And>asida stored_hw_asid___struct_pde_C ret__unsigned x2. \<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); pde_stored_asid stored_hw_asid___struct_pde_C = Some x2\<rbrakk> \<Longrightarrow> ccorres (=) ret__unsigned_char_' (\<lambda>a. ?R569 asida (pde_stored_asid stored_hw_asid___struct_pde_C) a x2) (?R''571 asida (pde_stored_asid stored_hw_asid___struct_pde_C) stored_hw_asid___struct_pde_C ret__unsigned x2) [SKIP] (return x2) (IF ret__unsigned \<noteq> 0 THEN
  \<acute>ret__unsigned :== CALL pde_pde_invalid_get_stored_hw_asid_'proc(stored_hw_asid___struct_pde_C);;
return_C ret__unsigned_char_'_update (\<lambda>s. UCAST(32 \<rightarrow> 8) (ret__unsigned_' s))
ELSE
  lvar_nondet_init new_hw_asid_' new_hw_asid_'_update;;
\<acute>new_hw_asid :== CALL findFreeHWASID_'proc();;
CALL storeHWASID_'proc(asida,\<acute>new_hw_asid);;
return_C ret__unsigned_char_'_update new_hw_asid_'
FI)
 4. \<And>asida. asida = asid \<Longrightarrow> \<lbrace>?R242 asida\<rbrace> loadHWASID asid \<lbrace>\<lambda>a b. (a = None \<longrightarrow> (valid_arch_state' and valid_pde_mappings' and ?R615 asida a) b) \<and> (\<forall>x. a = Some x \<longrightarrow> ?R569 asida a b x)\<rbrace>
 5. \<And>asida s s'. \<lbrakk>asida = asid; (s, s') \<in> rf_sr; (all_invs_but_ct_idle_or_in_cur_domain' and (\<lambda>s. asid \<le> mask local.asid_bits)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (valid_pde_mappings' and (\<lambda>_. asid \<le> mask local.asid_bits) and ?R242 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. rv = None \<longrightarrow> s \<in> {s. \<forall>v. new_hw_asid_'_update (\<lambda>_. v) s \<in> {s. s \<in> UNIV} \<inter> {s'. \<forall>t rv. rv = ret__unsigned_char_' t \<longrightarrow> new_hw_asid_'_update (\<lambda>_. ret__unsigned_char_' t) (s'\<lparr>globals := globals t\<rparr>) \<in> {s. hw_asid_'_update (\<lambda>_. ret__unsigned_char_' t) (asid_'_update (\<lambda>_. asida) s) \<in> UNIV \<inter> \<lbrace>\<acute>asid = asida\<rbrace> \<inter> \<lbrace>\<acute>hw_asid = UCAST(8 \<rightarrow> 8) rv\<rbrace>} \<inter> {s'. \<forall>ta rva. dc rva (xfdc ta) \<longrightarrow> s'\<lparr>globals := globals ta\<rparr> \<in> \<lbrace>rv = \<^bsup>t\<^esup>ret__unsigned_char\<rbrace>}}} \<inter> - \<lbrace>v \<noteq> 0\<rbrace>} \<inter> {s. \<forall>x. s \<in> {s. rv = Some x \<longrightarrow> s \<in> ?R''571 asida rv (ret__struct_pde_C_' t) v x}}}} \<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); pde_stored_asid stored_hw_asid___struct_pde_C = None\<rbrakk> \<Longrightarrow> \<lbrace>?R615 asid (ds_id None)\<rbrace> findFreeHWASID \<lbrace>\<lambda>rv s. valid_pde_mappings' s \<and> asid \<le> mask local.asid_bits \<and> True\<rbrace>
 2. \<And>asida stored_hw_asid___struct_pde_C ret__unsigned x2. \<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); pde_stored_asid stored_hw_asid___struct_pde_C = Some x2\<rbrakk> \<Longrightarrow> ccorres (=) ret__unsigned_char_' (\<lambda>a. ?R569 asida (pde_stored_asid stored_hw_asid___struct_pde_C) a x2) (?R''571 asida (pde_stored_asid stored_hw_asid___struct_pde_C) stored_hw_asid___struct_pde_C ret__unsigned x2) [SKIP] (return x2) (IF ret__unsigned \<noteq> 0 THEN
  \<acute>ret__unsigned :== CALL pde_pde_invalid_get_stored_hw_asid_'proc(stored_hw_asid___struct_pde_C);;
return_C ret__unsigned_char_'_update (\<lambda>s. UCAST(32 \<rightarrow> 8) (ret__unsigned_' s))
ELSE
  lvar_nondet_init new_hw_asid_' new_hw_asid_'_update;;
\<acute>new_hw_asid :== CALL findFreeHWASID_'proc();;
CALL storeHWASID_'proc(asida,\<acute>new_hw_asid);;
return_C ret__unsigned_char_'_update new_hw_asid_'
FI)
 3. \<And>asida. asida = asid \<Longrightarrow> \<lbrace>?R242 asida\<rbrace> loadHWASID asid \<lbrace>\<lambda>a b. (a = None \<longrightarrow> (valid_arch_state' and valid_pde_mappings' and ?R615 asida a) b) \<and> (\<forall>x. a = Some x \<longrightarrow> ?R569 asida a b x)\<rbrace>
 4. \<And>asida s s'. \<lbrakk>asida = asid; (s, s') \<in> rf_sr; (all_invs_but_ct_idle_or_in_cur_domain' and (\<lambda>s. asid \<le> mask local.asid_bits)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (valid_pde_mappings' and (\<lambda>_. asid \<le> mask local.asid_bits) and ?R242 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. rv = None \<longrightarrow> s \<in> {s. \<forall>v. new_hw_asid_'_update (\<lambda>_. v) s \<in> {s. s \<in> UNIV} \<inter> {s'. \<forall>t rv. rv = ret__unsigned_char_' t \<longrightarrow> new_hw_asid_'_update (\<lambda>_. ret__unsigned_char_' t) (s'\<lparr>globals := globals t\<rparr>) \<in> {s. hw_asid_'_update (\<lambda>_. ret__unsigned_char_' t) (asid_'_update (\<lambda>_. asida) s) \<in> UNIV \<inter> \<lbrace>\<acute>asid = asida\<rbrace> \<inter> \<lbrace>\<acute>hw_asid = UCAST(8 \<rightarrow> 8) rv\<rbrace>} \<inter> {s'. \<forall>ta rva. dc rva (xfdc ta) \<longrightarrow> s'\<lparr>globals := globals ta\<rparr> \<in> \<lbrace>rv = \<^bsup>t\<^esup>ret__unsigned_char\<rbrace>}}} \<inter> - \<lbrace>v \<noteq> 0\<rbrace>} \<inter> {s. \<forall>x. s \<in> {s. rv = Some x \<longrightarrow> s \<in> ?R''571 asida rv (ret__struct_pde_C_' t) v x}}}} \<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); pde_stored_asid stored_hw_asid___struct_pde_C = None\<rbrakk> \<Longrightarrow> \<lbrace>?R615 asid (ds_id None)\<rbrace> findFreeHWASID \<lbrace>\<lambda>r s. all_invs_but_ct_idle_or_in_cur_domain' s \<and> asid \<le> mask local.asid_bits \<and> True\<rbrace>
 2. \<And>asida stored_hw_asid___struct_pde_C ret__unsigned x2. \<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); pde_stored_asid stored_hw_asid___struct_pde_C = Some x2\<rbrakk> \<Longrightarrow> ccorres (=) ret__unsigned_char_' (\<lambda>a. ?R569 asida (pde_stored_asid stored_hw_asid___struct_pde_C) a x2) (?R''571 asida (pde_stored_asid stored_hw_asid___struct_pde_C) stored_hw_asid___struct_pde_C ret__unsigned x2) [SKIP] (return x2) (IF ret__unsigned \<noteq> 0 THEN
  \<acute>ret__unsigned :== CALL pde_pde_invalid_get_stored_hw_asid_'proc(stored_hw_asid___struct_pde_C);;
return_C ret__unsigned_char_'_update (\<lambda>s. UCAST(32 \<rightarrow> 8) (ret__unsigned_' s))
ELSE
  lvar_nondet_init new_hw_asid_' new_hw_asid_'_update;;
\<acute>new_hw_asid :== CALL findFreeHWASID_'proc();;
CALL storeHWASID_'proc(asida,\<acute>new_hw_asid);;
return_C ret__unsigned_char_'_update new_hw_asid_'
FI)
 3. \<And>asida. asida = asid \<Longrightarrow> \<lbrace>?R242 asida\<rbrace> loadHWASID asid \<lbrace>\<lambda>a b. (a = None \<longrightarrow> (valid_arch_state' and valid_pde_mappings' and ?R615 asida a) b) \<and> (\<forall>x. a = Some x \<longrightarrow> ?R569 asida a b x)\<rbrace>
 4. \<And>asida s s'. \<lbrakk>asida = asid; (s, s') \<in> rf_sr; (all_invs_but_ct_idle_or_in_cur_domain' and (\<lambda>s. asid \<le> mask local.asid_bits)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (valid_pde_mappings' and (\<lambda>_. asid \<le> mask local.asid_bits) and ?R242 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. rv = None \<longrightarrow> s \<in> {s. \<forall>v. new_hw_asid_'_update (\<lambda>_. v) s \<in> {s. s \<in> UNIV} \<inter> {s'. \<forall>t rv. rv = ret__unsigned_char_' t \<longrightarrow> new_hw_asid_'_update (\<lambda>_. ret__unsigned_char_' t) (s'\<lparr>globals := globals t\<rparr>) \<in> {s. hw_asid_'_update (\<lambda>_. ret__unsigned_char_' t) (asid_'_update (\<lambda>_. asida) s) \<in> UNIV \<inter> \<lbrace>\<acute>asid = asida\<rbrace> \<inter> \<lbrace>\<acute>hw_asid = UCAST(8 \<rightarrow> 8) rv\<rbrace>} \<inter> {s'. \<forall>ta rva. dc rva (xfdc ta) \<longrightarrow> s'\<lparr>globals := globals ta\<rparr> \<in> \<lbrace>rv = \<^bsup>t\<^esup>ret__unsigned_char\<rbrace>}}} \<inter> - \<lbrace>v \<noteq> 0\<rbrace>} \<inter> {s. \<forall>x. s \<in> {s. rv = Some x \<longrightarrow> s \<in> ?R''571 asida rv (ret__struct_pde_C_' t) v x}}}} \<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 x2. \<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); pde_stored_asid stored_hw_asid___struct_pde_C = Some x2\<rbrakk> \<Longrightarrow> ccorres (=) ret__unsigned_char_' (\<lambda>a. ?R569 asida (pde_stored_asid stored_hw_asid___struct_pde_C) a x2) (?R''571 asida (pde_stored_asid stored_hw_asid___struct_pde_C) stored_hw_asid___struct_pde_C ret__unsigned x2) [SKIP] (return x2) (IF ret__unsigned \<noteq> 0 THEN
  \<acute>ret__unsigned :== CALL pde_pde_invalid_get_stored_hw_asid_'proc(stored_hw_asid___struct_pde_C);;
return_C ret__unsigned_char_'_update (\<lambda>s. UCAST(32 \<rightarrow> 8) (ret__unsigned_' s))
ELSE
  lvar_nondet_init new_hw_asid_' new_hw_asid_'_update;;
\<acute>new_hw_asid :== CALL findFreeHWASID_'proc();;
CALL storeHWASID_'proc(asida,\<acute>new_hw_asid);;
return_C ret__unsigned_char_'_update new_hw_asid_'
FI)
 2. \<And>asida. asida = asid \<Longrightarrow> \<lbrace>?R242 asida\<rbrace> loadHWASID asid \<lbrace>\<lambda>a b. (a = None \<longrightarrow> (valid_arch_state' and valid_pde_mappings' and (\<lambda>a. all_invs_but_ct_idle_or_in_cur_domain' a \<and> asida \<le> mask local.asid_bits \<and> True)) b) \<and> (\<forall>x. a = Some x \<longrightarrow> ?R569 asida a b x)\<rbrace>
 3. \<And>asida s s'. \<lbrakk>asida = asid; (s, s') \<in> rf_sr; (all_invs_but_ct_idle_or_in_cur_domain' and (\<lambda>s. asid \<le> mask local.asid_bits)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (valid_pde_mappings' and (\<lambda>_. asid \<le> mask local.asid_bits) and ?R242 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. rv = None \<longrightarrow> s \<in> {s. \<forall>v. new_hw_asid_'_update (\<lambda>_. v) s \<in> {s. s \<in> UNIV} \<inter> {s'. \<forall>t rv. rv = ret__unsigned_char_' t \<longrightarrow> new_hw_asid_'_update (\<lambda>_. ret__unsigned_char_' t) (s'\<lparr>globals := globals t\<rparr>) \<in> {s. hw_asid_'_update (\<lambda>_. ret__unsigned_char_' t) (asid_'_update (\<lambda>_. asida) s) \<in> UNIV \<inter> \<lbrace>\<acute>asid = asida\<rbrace> \<inter> \<lbrace>\<acute>hw_asid = UCAST(8 \<rightarrow> 8) rv\<rbrace>} \<inter> {s'. \<forall>ta rva. dc rva (xfdc ta) \<longrightarrow> s'\<lparr>globals := globals ta\<rparr> \<in> \<lbrace>rv = \<^bsup>t\<^esup>ret__unsigned_char\<rbrace>}}} \<inter> - \<lbrace>v \<noteq> 0\<rbrace>} \<inter> {s. \<forall>x. s \<in> {s. rv = Some x \<longrightarrow> s \<in> ?R''571 asida rv (ret__struct_pde_C_' t) v x}}}} \<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 x2. \<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); pde_stored_asid stored_hw_asid___struct_pde_C = Some x2\<rbrakk> \<Longrightarrow> ccorres (=) ret__unsigned_char_' (?R785 asida (pde_stored_asid stored_hw_asid___struct_pde_C) x2) (?R'783 asida (pde_stored_asid stored_hw_asid___struct_pde_C) stored_hw_asid___struct_pde_C ret__unsigned x2) [SKIP] (return x2) (\<acute>ret__unsigned :== CALL pde_pde_invalid_get_stored_hw_asid_'proc(stored_hw_asid___struct_pde_C);;
return_C ret__unsigned_char_'_update (\<lambda>s. UCAST(32 \<rightarrow> 8) (ret__unsigned_' s)))
 2. \<And>asida. asida = asid \<Longrightarrow> \<lbrace>?R242 asida\<rbrace> loadHWASID asid \<lbrace>\<lambda>a b. (a = None \<longrightarrow> (valid_arch_state' and valid_pde_mappings' and (\<lambda>a. all_invs_but_ct_idle_or_in_cur_domain' a \<and> asida \<le> mask local.asid_bits \<and> True)) b) \<and> (\<forall>x. a = Some x \<longrightarrow> ?R785 asida a x b)\<rbrace>
 3. \<And>asida s s'. \<lbrakk>asida = asid; (s, s') \<in> rf_sr; (all_invs_but_ct_idle_or_in_cur_domain' and (\<lambda>s. asid \<le> mask local.asid_bits)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (valid_pde_mappings' and (\<lambda>_. asid \<le> mask local.asid_bits) and ?R242 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. rv = None \<longrightarrow> s \<in> {s. \<forall>v. new_hw_asid_'_update (\<lambda>_. v) s \<in> {s. s \<in> UNIV} \<inter> {s'. \<forall>t rv. rv = ret__unsigned_char_' t \<longrightarrow> new_hw_asid_'_update (\<lambda>_. ret__unsigned_char_' t) (s'\<lparr>globals := globals t\<rparr>) \<in> {s. hw_asid_'_update (\<lambda>_. ret__unsigned_char_' t) (asid_'_update (\<lambda>_. asida) s) \<in> UNIV \<inter> \<lbrace>\<acute>asid = asida\<rbrace> \<inter> \<lbrace>\<acute>hw_asid = UCAST(8 \<rightarrow> 8) rv\<rbrace>} \<inter> {s'. \<forall>ta rva. dc rva (xfdc ta) \<longrightarrow> s'\<lparr>globals := globals ta\<rparr> \<in> \<lbrace>rv = \<^bsup>t\<^esup>ret__unsigned_char\<rbrace>}}} \<inter> - \<lbrace>v \<noteq> 0\<rbrace>} \<inter> {s. \<forall>x. s \<in> {s. rv = Some x \<longrightarrow> s \<in> ?R'783 asida rv (ret__struct_pde_C_' t) v x \<inter> \<lbrace>v \<noteq> 0\<rbrace>}}}} \<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 x2. \<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); pde_stored_asid stored_hw_asid___struct_pde_C = Some x2\<rbrakk> \<Longrightarrow> \<forall>\<sigma>. \<Gamma>\<turnstile> {s. True \<and> s \<in> UNIV \<and> (\<sigma>, s) \<in> rf_sr} \<acute>ret__unsigned :== CALL pde_pde_invalid_get_stored_hw_asid_'proc(stored_hw_asid___struct_pde_C);;
return_C ret__unsigned_char_'_update (\<lambda>s. UCAST(32 \<rightarrow> 8) (ret__unsigned_' s)) {},{s. \<exists>(rv, \<sigma>')\<in>fst (return x2 \<sigma>). (\<sigma>', s) \<in> rf_sr \<and> rv = ret__unsigned_char_' s}
 2. \<And>asida. asida = asid \<Longrightarrow> \<lbrace>?R242 asida\<rbrace> loadHWASID asid \<lbrace>\<lambda>a b. (a = None \<longrightarrow> (valid_arch_state' and valid_pde_mappings' and (\<lambda>a. all_invs_but_ct_idle_or_in_cur_domain' a \<and> asida \<le> mask local.asid_bits \<and> True)) b) \<and> (\<forall>x. a = Some x \<longrightarrow> True)\<rbrace>
 3. \<And>asida s s'. \<lbrakk>asida = asid; (s, s') \<in> rf_sr; (all_invs_but_ct_idle_or_in_cur_domain' and (\<lambda>s. asid \<le> mask local.asid_bits)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (valid_pde_mappings' and (\<lambda>_. asid \<le> mask local.asid_bits) and ?R242 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. rv = None \<longrightarrow> s \<in> {s. \<forall>v. new_hw_asid_'_update (\<lambda>_. v) s \<in> {s. s \<in> UNIV} \<inter> {s'. \<forall>t rv. rv = ret__unsigned_char_' t \<longrightarrow> new_hw_asid_'_update (\<lambda>_. ret__unsigned_char_' t) (s'\<lparr>globals := globals t\<rparr>) \<in> {s. hw_asid_'_update (\<lambda>_. ret__unsigned_char_' t) (asid_'_update (\<lambda>_. asida) s) \<in> UNIV \<inter> \<lbrace>\<acute>asid = asida\<rbrace> \<inter> \<lbrace>\<acute>hw_asid = UCAST(8 \<rightarrow> 8) rv\<rbrace>} \<inter> {s'. \<forall>ta rva. dc rva (xfdc ta) \<longrightarrow> s'\<lparr>globals := globals ta\<rparr> \<in> \<lbrace>rv = \<^bsup>t\<^esup>ret__unsigned_char\<rbrace>}}} \<inter> - \<lbrace>v \<noteq> 0\<rbrace>} \<inter> {s. \<forall>x. s \<in> {s. rv = Some x \<longrightarrow> s \<in> UNIV \<inter> \<lbrace>v \<noteq> 0\<rbrace>}}}} \<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 x2 \<sigma>. \<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); pde_stored_asid stored_hw_asid___struct_pde_C = Some x2\<rbrakk> \<Longrightarrow> {s. True \<and> s \<in> UNIV \<and> (\<sigma>, s) \<in> rf_sr} \<subseteq> {s. pde_get_tag stored_hw_asid___struct_pde_C = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid \<and> (\<forall>t. ret__unsigned_' t = stored_hw_asid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C) \<longrightarrow> (\<exists>(rv, \<sigma>')\<in>fst (return x2 \<sigma>). (\<sigma>', s\<lparr>ret__unsigned_' := stored_hw_asid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C), ret__unsigned_char_' := UCAST(32 \<rightarrow> 8) (stored_hw_asid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C)), global_exn_var_' := Return\<rparr>) \<in> rf_sr \<and> rv = UCAST(32 \<rightarrow> 8) (stored_hw_asid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C))))}
 2. \<And>asida. asida = asid \<Longrightarrow> \<lbrace>?R242 asida\<rbrace> loadHWASID asid \<lbrace>\<lambda>a b. (a = None \<longrightarrow> (valid_arch_state' and valid_pde_mappings' and (\<lambda>a. all_invs_but_ct_idle_or_in_cur_domain' a \<and> asida \<le> mask local.asid_bits \<and> True)) b) \<and> (\<forall>x. a = Some x \<longrightarrow> True)\<rbrace>
 3. \<And>asida s s'. \<lbrakk>asida = asid; (s, s') \<in> rf_sr; (all_invs_but_ct_idle_or_in_cur_domain' and (\<lambda>s. asid \<le> mask local.asid_bits)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (valid_pde_mappings' and (\<lambda>_. asid \<le> mask local.asid_bits) and ?R242 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. rv = None \<longrightarrow> s \<in> {s. \<forall>v. new_hw_asid_'_update (\<lambda>_. v) s \<in> {s. s \<in> UNIV} \<inter> {s'. \<forall>t rv. rv = ret__unsigned_char_' t \<longrightarrow> new_hw_asid_'_update (\<lambda>_. ret__unsigned_char_' t) (s'\<lparr>globals := globals t\<rparr>) \<in> {s. hw_asid_'_update (\<lambda>_. ret__unsigned_char_' t) (asid_'_update (\<lambda>_. asida) s) \<in> UNIV \<inter> \<lbrace>\<acute>asid = asida\<rbrace> \<inter> \<lbrace>\<acute>hw_asid = UCAST(8 \<rightarrow> 8) rv\<rbrace>} \<inter> {s'. \<forall>ta rva. dc rva (xfdc ta) \<longrightarrow> s'\<lparr>globals := globals ta\<rparr> \<in> \<lbrace>rv = \<^bsup>t\<^esup>ret__unsigned_char\<rbrace>}}} \<inter> - \<lbrace>v \<noteq> 0\<rbrace>} \<inter> {s. \<forall>x. s \<in> {s. rv = Some x \<longrightarrow> s \<in> UNIV \<inter> \<lbrace>v \<noteq> 0\<rbrace>}}}} \<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>?R242 asida\<rbrace> loadHWASID asid \<lbrace>\<lambda>a b. (a = None \<longrightarrow> (valid_arch_state' and valid_pde_mappings' and (\<lambda>a. all_invs_but_ct_idle_or_in_cur_domain' a \<and> asida \<le> mask local.asid_bits \<and> True)) b) \<and> (\<forall>x. a = Some x \<longrightarrow> True)\<rbrace>
 2. \<And>asida s s'. \<lbrakk>asida = asid; (s, s') \<in> rf_sr; (all_invs_but_ct_idle_or_in_cur_domain' and (\<lambda>s. asid \<le> mask local.asid_bits)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (valid_pde_mappings' and (\<lambda>_. asid \<le> mask local.asid_bits) and ?R242 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. rv = None \<longrightarrow> s \<in> {s. \<forall>v. new_hw_asid_'_update (\<lambda>_. v) s \<in> {s. s \<in> UNIV} \<inter> {s'. \<forall>t rv. rv = ret__unsigned_char_' t \<longrightarrow> new_hw_asid_'_update (\<lambda>_. ret__unsigned_char_' t) (s'\<lparr>globals := globals t\<rparr>) \<in> {s. hw_asid_'_update (\<lambda>_. ret__unsigned_char_' t) (asid_'_update (\<lambda>_. asida) s) \<in> UNIV \<inter> \<lbrace>\<acute>asid = asida\<rbrace> \<inter> \<lbrace>\<acute>hw_asid = UCAST(8 \<rightarrow> 8) rv\<rbrace>} \<inter> {s'. \<forall>ta rva. dc rva (xfdc ta) \<longrightarrow> s'\<lparr>globals := globals ta\<rparr> \<in> \<lbrace>rv = \<^bsup>t\<^esup>ret__unsigned_char\<rbrace>}}} \<inter> - \<lbrace>v \<noteq> 0\<rbrace>} \<inter> {s. \<forall>x. s \<in> {s. rv = Some x \<longrightarrow> s \<in> UNIV \<inter> \<lbrace>v \<noteq> 0\<rbrace>}}}} \<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; (all_invs_but_ct_idle_or_in_cur_domain' and (\<lambda>s. 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. (map_option fst (armKSASIDMap (ksArchState s) asid) = None \<longrightarrow> (valid_arch_state' and valid_pde_mappings' and (\<lambda>a. all_invs_but_ct_idle_or_in_cur_domain' a \<and> asida \<le> mask local.asid_bits \<and> True)) s) \<and> (\<forall>x. map_option fst (armKSASIDMap (ksArchState s) asid) = Some x \<longrightarrow> True))) 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. rv = None \<longrightarrow> s \<in> {s. \<forall>v. new_hw_asid_'_update (\<lambda>_. v) s \<in> {s. s \<in> UNIV} \<inter> {s'. \<forall>t rv. rv = ret__unsigned_char_' t \<longrightarrow> new_hw_asid_'_update (\<lambda>_. ret__unsigned_char_' t) (s'\<lparr>globals := globals t\<rparr>) \<in> {s. hw_asid_'_update (\<lambda>_. ret__unsigned_char_' t) (asid_'_update (\<lambda>_. asida) s) \<in> UNIV \<inter> \<lbrace>\<acute>asid = asida\<rbrace> \<inter> \<lbrace>\<acute>hw_asid = UCAST(8 \<rightarrow> 8) rv\<rbrace>} \<inter> {s'. \<forall>ta rva. dc rva (xfdc ta) \<longrightarrow> s'\<lparr>globals := globals ta\<rparr> \<in> \<lbrace>rv = \<^bsup>t\<^esup>ret__unsigned_char\<rbrace>}}} \<inter> - \<lbrace>v \<noteq> 0\<rbrace>} \<inter> {s. \<forall>x. s \<in> {s. rv = Some x \<longrightarrow> s \<in> UNIV \<inter> \<lbrace>v \<noteq> 0\<rbrace>}}}} \<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>s s'. \<lbrakk>(s, s') \<in> rf_sr; all_invs_but_ct_idle_or_in_cur_domain' s; asid \<le> mask local.asid_bits\<rbrakk> \<Longrightarrow> valid_pde_mappings' s \<and> (armKSASIDMap (ksArchState s) asid = None \<longrightarrow> valid_arch_state' s \<and> valid_pde_mappings' s) \<and> (\<forall>t. pde_get_tag (ret__struct_pde_C_' t) = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid \<longrightarrow> ((if to_bool (stored_asid_valid_CL (pde_pde_invalid_lift (ret__struct_pde_C_' t))) then Some (UCAST(32 \<rightarrow> 8) (stored_hw_asid_CL (pde_pde_invalid_lift (ret__struct_pde_C_' t)))) else None) = None \<longrightarrow> s'\<lparr>globals := globals t, stored_hw_asid___struct_pde_C_' := ret__struct_pde_C_' t, ret__unsigned_' := stored_asid_valid_CL (pde_pde_invalid_lift (ret__struct_pde_C_' t))\<rparr> \<notin> (if stored_asid_valid_CL (pde_pde_invalid_lift (ret__struct_pde_C_' t)) \<noteq> 0 then UNIV else {})) \<and> ((\<exists>x. (if to_bool (stored_asid_valid_CL (pde_pde_invalid_lift (ret__struct_pde_C_' t))) then Some (UCAST(32 \<rightarrow> 8) (stored_hw_asid_CL (pde_pde_invalid_lift (ret__struct_pde_C_' t)))) else None) = Some x) \<longrightarrow> s'\<lparr>globals := globals t, stored_hw_asid___struct_pde_C_' := ret__struct_pde_C_' t, ret__unsigned_' := stored_asid_valid_CL (pde_pde_invalid_lift (ret__struct_pde_C_' t))\<rparr> \<in> (if stored_asid_valid_CL (pde_pde_invalid_lift (ret__struct_pde_C_' t)) \<noteq> 0 then UNIV else {}))) proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; all_invs_but_ct_idle_or_in_cur_domain' s; asid \<le> mask local.asid_bits\<rbrakk> \<Longrightarrow> valid_pde_mappings' s \<and> (armKSASIDMap (ksArchState s) asid = None \<longrightarrow> valid_arch_state' s \<and> valid_pde_mappings' s) proof (prove)
goal:
No subgoals!