theory structures_defs

lemma pde_pde_section_lift:
  "(pde_get_tag c = scast pde_pde_section) = (pde_lift c = Some (Pde_pde_section (pde_pde_section_lift c)))" unfolding pde_lift_def pde_pde_section_lift_def by (clarsimp simp: pde_tag_defs Let_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (pde_get_tag c = SCAST(32 signed \<rightarrow> 32) pde_pde_section) = (pde_lift c = Some (Pde_pde_section (pde_pde_section_lift c))) proof (prove)
goal (1 subgoal):
 1. (pde_get_tag c = SCAST(32 signed \<rightarrow> 32) pde_pde_section) = ((let tag = pde_get_tag c in if tag = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid then Some (Pde_pde_invalid \<lparr>stored_hw_asid_CL = (pde_C.words_C c.[0] >> 24) && mask 8, stored_asid_valid_CL = (pde_C.words_C c.[0] >> 23) && mask 1\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) pde_pde_coarse then Some (Pde_pde_coarse \<lparr>pde_pde_coarse_CL.address_CL = (pde_C.words_C c.[0] << 0) && ~~ mask 10, P_CL = (pde_C.words_C c.[0] >> 9) && mask 1, Domain_CL = (pde_C.words_C c.[0] >> 5) && mask 4\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) pde_pde_section then Some (Pde_pde_section \<lparr>pde_pde_section_CL.address_CL = (pde_C.words_C c.[0] << 0) && ~~ mask 20, size_CL = (pde_C.words_C c.[0] >> 18) && mask 1, nG_CL = (pde_C.words_C c.[0] >> 17) && mask 1, S_CL = (pde_C.words_C c.[0] >> 16) && mask 1, APX_CL = (pde_C.words_C c.[0] >> 15) && mask 1, TEX_CL = (pde_C.words_C c.[0] >> 12) && mask 3, AP_CL = (pde_C.words_C c.[0] >> 10) && mask 2, P_CL = (pde_C.words_C c.[0] >> 9) && mask 1, Domain_CL = (pde_C.words_C c.[0] >> 5) && mask 4, XN_CL = (pde_C.words_C c.[0] >> 4) && mask 1, C_CL = (pde_C.words_C c.[0] >> 3) && mask 1, B_CL = (pde_C.words_C c.[0] >> 2) && mask 1\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) pde_pde_reserved then Some Pde_pde_reserved else None) = Some (Pde_pde_section (case let tag = pde_get_tag c in if tag = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid then Some (Pde_pde_invalid \<lparr>stored_hw_asid_CL = (pde_C.words_C c.[0] >> 24) && mask 8, stored_asid_valid_CL = (pde_C.words_C c.[0] >> 23) && mask 1\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) pde_pde_coarse then Some (Pde_pde_coarse \<lparr>pde_pde_coarse_CL.address_CL = (pde_C.words_C c.[0] << 0) && ~~ mask 10, P_CL = (pde_C.words_C c.[0] >> 9) && mask 1, Domain_CL = (pde_C.words_C c.[0] >> 5) && mask 4\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) pde_pde_section then Some (Pde_pde_section \<lparr>pde_pde_section_CL.address_CL = (pde_C.words_C c.[0] << 0) && ~~ mask 20, size_CL = (pde_C.words_C c.[0] >> 18) && mask 1, nG_CL = (pde_C.words_C c.[0] >> 17) && mask 1, S_CL = (pde_C.words_C c.[0] >> 16) && mask 1, APX_CL = (pde_C.words_C c.[0] >> 15) && mask 1, TEX_CL = (pde_C.words_C c.[0] >> 12) && mask 3, AP_CL = (pde_C.words_C c.[0] >> 10) && mask 2, P_CL = (pde_C.words_C c.[0] >> 9) && mask 1, Domain_CL = (pde_C.words_C c.[0] >> 5) && mask 4, XN_CL = (pde_C.words_C c.[0] >> 4) && mask 1, C_CL = (pde_C.words_C c.[0] >> 3) && mask 1, B_CL = (pde_C.words_C c.[0] >> 2) && mask 1\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) pde_pde_reserved then Some Pde_pde_reserved else None of Some (Pde_pde_section rec) \<Rightarrow> rec)))