kings-crown/FVELER_Isabelle huggingface dataset:
theory structures_defs

lemma cap_lift_irq_control_cap:
  "cap_get_tag cap = scast cap_irq_control_cap \<Longrightarrow>
  cap_lift cap =
  Some (Cap_irq_control_cap)" by (simp add:cap_lift_def cap_tag_defs)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_irq_control_cap \<Longrightarrow> cap_lift cap = Some Cap_irq_control_cap
theory structures_defs

lemma cap_lift_zombie_cap:
  "cap_get_tag cap = scast cap_zombie_cap \<Longrightarrow>
  cap_lift cap =
  Some (Cap_zombie_cap \<lparr> 
       cap_zombie_cap_CL.capZombieID_CL = (((index (cap_C.words_C cap) 1) >> 0)),
       cap_zombie_cap_CL.capZombieType_CL = (((index (cap_C.words_C cap) 0) >> 8) AND mask 6) \<rparr>)" by (simp add:cap_lift_def cap_tag_defs)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_zombie_cap \<Longrightarrow> cap_lift cap = Some (Cap_zombie_cap \<lparr>capZombieID_CL = cap_C.words_C cap.[1] >> 0, capZombieType_CL = (cap_C.words_C cap.[0] >> 8) && mask 6\<rparr>)
theory structures_defs

lemma cap_lift_domain_cap:
  "cap_get_tag cap = scast cap_domain_cap \<Longrightarrow>
  cap_lift cap =
  Some (Cap_domain_cap)" by (simp add:cap_lift_def cap_tag_defs)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_domain_cap \<Longrightarrow> cap_lift cap = Some Cap_domain_cap
theory structures_defs

lemma lookup_fault_get_tag_eq_x:
  "(lookup_fault_get_tag c = x) = ((((index (lookup_fault_C.words_C c) 0) >> 0) AND mask 2) = x)" by (auto simp add: lookup_fault_get_tag_def mask_def word_bw_assocs)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (lookup_fault_get_tag c = x) = ((lookup_fault_C.words_C c.[0] >> 0) && mask 2 = x)
theory structures_defs

lemma lookup_fault_lift_invalid_root:
  "lookup_fault_get_tag lookup_fault = scast lookup_fault_invalid_root \<Longrightarrow>
  lookup_fault_lift lookup_fault =
  Some (Lookup_fault_invalid_root)" by (simp add:lookup_fault_lift_def lookup_fault_tag_defs)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. lookup_fault_get_tag lookup_fault = SCAST(32 signed \<rightarrow> 32) lookup_fault_invalid_root \<Longrightarrow> lookup_fault_lift lookup_fault = Some Lookup_fault_invalid_root
theory structures_defs

lemma lookup_fault_lift_missing_capability:
  "lookup_fault_get_tag lookup_fault = scast lookup_fault_missing_capability \<Longrightarrow>
  lookup_fault_lift lookup_fault =
  Some (Lookup_fault_missing_capability \<lparr> 
       lookup_fault_missing_capability_CL.bitsLeft_CL = (((index (lookup_fault_C.words_C lookup_fault) 0) >> 2) AND mask 6) \<rparr>)" by (simp add:lookup_fault_lift_def lookup_fault_tag_defs)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. lookup_fault_get_tag lookup_fault = SCAST(32 signed \<rightarrow> 32) lookup_fault_missing_capability \<Longrightarrow> lookup_fault_lift lookup_fault = Some (Lookup_fault_missing_capability \<lparr>lookup_fault_missing_capability_CL.bitsLeft_CL = (lookup_fault_C.words_C lookup_fault.[0] >> 2) && mask 6\<rparr>)
theory structures_defs

lemma lookup_fault_lift_depth_mismatch:
  "lookup_fault_get_tag lookup_fault = scast lookup_fault_depth_mismatch \<Longrightarrow>
  lookup_fault_lift lookup_fault =
  Some (Lookup_fault_depth_mismatch \<lparr> 
       lookup_fault_depth_mismatch_CL.bitsFound_CL = (((index (lookup_fault_C.words_C lookup_fault) 0) >> 8) AND mask 6),
       lookup_fault_depth_mismatch_CL.bitsLeft_CL = (((index (lookup_fault_C.words_C lookup_fault) 0) >> 2) AND mask 6) \<rparr>)" by (simp add:lookup_fault_lift_def lookup_fault_tag_defs)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. lookup_fault_get_tag lookup_fault = SCAST(32 signed \<rightarrow> 32) lookup_fault_depth_mismatch \<Longrightarrow> lookup_fault_lift lookup_fault = Some (Lookup_fault_depth_mismatch \<lparr>lookup_fault_depth_mismatch_CL.bitsFound_CL = (lookup_fault_C.words_C lookup_fault.[0] >> 8) && mask 6, bitsLeft_CL = (lookup_fault_C.words_C lookup_fault.[0] >> 2) && mask 6\<rparr>)
theory structures_defs

lemma lookup_fault_lift_guard_mismatch:
  "lookup_fault_get_tag lookup_fault = scast lookup_fault_guard_mismatch \<Longrightarrow>
  lookup_fault_lift lookup_fault =
  Some (Lookup_fault_guard_mismatch \<lparr> 
       lookup_fault_guard_mismatch_CL.guardFound_CL = (((index (lookup_fault_C.words_C lookup_fault) 1) >> 0)),
       lookup_fault_guard_mismatch_CL.bitsLeft_CL = (((index (lookup_fault_C.words_C lookup_fault) 0) >> 8) AND mask 6),
       lookup_fault_guard_mismatch_CL.bitsFound_CL = (((index (lookup_fault_C.words_C lookup_fault) 0) >> 2) AND mask 6) \<rparr>)" by (simp add:lookup_fault_lift_def lookup_fault_tag_defs)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. lookup_fault_get_tag lookup_fault = SCAST(32 signed \<rightarrow> 32) lookup_fault_guard_mismatch \<Longrightarrow> lookup_fault_lift lookup_fault = Some (Lookup_fault_guard_mismatch \<lparr>guardFound_CL = lookup_fault_C.words_C lookup_fault.[1] >> 0, bitsLeft_CL = (lookup_fault_C.words_C lookup_fault.[0] >> 8) && mask 6, bitsFound_CL = (lookup_fault_C.words_C lookup_fault.[0] >> 2) && mask 6\<rparr>)
theory structures_defs

lemma lookup_fault_missing_capability_lift:
  "(lookup_fault_get_tag c = scast lookup_fault_missing_capability) = (lookup_fault_lift c = Some (Lookup_fault_missing_capability (lookup_fault_missing_capability_lift c)))" unfolding lookup_fault_lift_def lookup_fault_missing_capability_lift_def by (clarsimp simp: lookup_fault_tag_defs Let_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (lookup_fault_get_tag c = SCAST(32 signed \<rightarrow> 32) lookup_fault_missing_capability) = (lookup_fault_lift c = Some (Lookup_fault_missing_capability (lookup_fault_missing_capability_lift c))) proof (prove)
goal (1 subgoal):
 1. (lookup_fault_get_tag c = SCAST(32 signed \<rightarrow> 32) lookup_fault_missing_capability) = ((let tag = lookup_fault_get_tag c in if tag = SCAST(32 signed \<rightarrow> 32) lookup_fault_invalid_root then Some Lookup_fault_invalid_root else if tag = SCAST(32 signed \<rightarrow> 32) lookup_fault_missing_capability then Some (Lookup_fault_missing_capability \<lparr>lookup_fault_missing_capability_CL.bitsLeft_CL = (lookup_fault_C.words_C c.[0] >> 2) && mask 6\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) lookup_fault_depth_mismatch then Some (Lookup_fault_depth_mismatch \<lparr>lookup_fault_depth_mismatch_CL.bitsFound_CL = (lookup_fault_C.words_C c.[0] >> 8) && mask 6, bitsLeft_CL = (lookup_fault_C.words_C c.[0] >> 2) && mask 6\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) lookup_fault_guard_mismatch then Some (Lookup_fault_guard_mismatch \<lparr>guardFound_CL = lookup_fault_C.words_C c.[1] >> 0, bitsLeft_CL = (lookup_fault_C.words_C c.[0] >> 8) && mask 6, bitsFound_CL = (lookup_fault_C.words_C c.[0] >> 2) && mask 6\<rparr>) else None) = Some (Lookup_fault_missing_capability (case let tag = lookup_fault_get_tag c in if tag = SCAST(32 signed \<rightarrow> 32) lookup_fault_invalid_root then Some Lookup_fault_invalid_root else if tag = SCAST(32 signed \<rightarrow> 32) lookup_fault_missing_capability then Some (Lookup_fault_missing_capability \<lparr>lookup_fault_missing_capability_CL.bitsLeft_CL = (lookup_fault_C.words_C c.[0] >> 2) && mask 6\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) lookup_fault_depth_mismatch then Some (Lookup_fault_depth_mismatch \<lparr>lookup_fault_depth_mismatch_CL.bitsFound_CL = (lookup_fault_C.words_C c.[0] >> 8) && mask 6, bitsLeft_CL = (lookup_fault_C.words_C c.[0] >> 2) && mask 6\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) lookup_fault_guard_mismatch then Some (Lookup_fault_guard_mismatch \<lparr>guardFound_CL = lookup_fault_C.words_C c.[1] >> 0, bitsLeft_CL = (lookup_fault_C.words_C c.[0] >> 8) && mask 6, bitsFound_CL = (lookup_fault_C.words_C c.[0] >> 2) && mask 6\<rparr>) else None of Some (Lookup_fault_missing_capability rec) \<Rightarrow> rec)))
theory structures_defs

lemma lookup_fault_depth_mismatch_lift:
  "(lookup_fault_get_tag c = scast lookup_fault_depth_mismatch) = (lookup_fault_lift c = Some (Lookup_fault_depth_mismatch (lookup_fault_depth_mismatch_lift c)))" unfolding lookup_fault_lift_def lookup_fault_depth_mismatch_lift_def by (clarsimp simp: lookup_fault_tag_defs Let_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (lookup_fault_get_tag c = SCAST(32 signed \<rightarrow> 32) lookup_fault_depth_mismatch) = (lookup_fault_lift c = Some (Lookup_fault_depth_mismatch (lookup_fault_depth_mismatch_lift c))) proof (prove)
goal (1 subgoal):
 1. (lookup_fault_get_tag c = SCAST(32 signed \<rightarrow> 32) lookup_fault_depth_mismatch) = ((let tag = lookup_fault_get_tag c in if tag = SCAST(32 signed \<rightarrow> 32) lookup_fault_invalid_root then Some Lookup_fault_invalid_root else if tag = SCAST(32 signed \<rightarrow> 32) lookup_fault_missing_capability then Some (Lookup_fault_missing_capability \<lparr>lookup_fault_missing_capability_CL.bitsLeft_CL = (lookup_fault_C.words_C c.[0] >> 2) && mask 6\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) lookup_fault_depth_mismatch then Some (Lookup_fault_depth_mismatch \<lparr>lookup_fault_depth_mismatch_CL.bitsFound_CL = (lookup_fault_C.words_C c.[0] >> 8) && mask 6, bitsLeft_CL = (lookup_fault_C.words_C c.[0] >> 2) && mask 6\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) lookup_fault_guard_mismatch then Some (Lookup_fault_guard_mismatch \<lparr>guardFound_CL = lookup_fault_C.words_C c.[1] >> 0, bitsLeft_CL = (lookup_fault_C.words_C c.[0] >> 8) && mask 6, bitsFound_CL = (lookup_fault_C.words_C c.[0] >> 2) && mask 6\<rparr>) else None) = Some (Lookup_fault_depth_mismatch (case let tag = lookup_fault_get_tag c in if tag = SCAST(32 signed \<rightarrow> 32) lookup_fault_invalid_root then Some Lookup_fault_invalid_root else if tag = SCAST(32 signed \<rightarrow> 32) lookup_fault_missing_capability then Some (Lookup_fault_missing_capability \<lparr>lookup_fault_missing_capability_CL.bitsLeft_CL = (lookup_fault_C.words_C c.[0] >> 2) && mask 6\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) lookup_fault_depth_mismatch then Some (Lookup_fault_depth_mismatch \<lparr>lookup_fault_depth_mismatch_CL.bitsFound_CL = (lookup_fault_C.words_C c.[0] >> 8) && mask 6, bitsLeft_CL = (lookup_fault_C.words_C c.[0] >> 2) && mask 6\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) lookup_fault_guard_mismatch then Some (Lookup_fault_guard_mismatch \<lparr>guardFound_CL = lookup_fault_C.words_C c.[1] >> 0, bitsLeft_CL = (lookup_fault_C.words_C c.[0] >> 8) && mask 6, bitsFound_CL = (lookup_fault_C.words_C c.[0] >> 2) && mask 6\<rparr>) else None of Some (Lookup_fault_depth_mismatch rec) \<Rightarrow> rec)))
theory structures_defs

lemma lookup_fault_guard_mismatch_lift:
  "(lookup_fault_get_tag c = scast lookup_fault_guard_mismatch) = (lookup_fault_lift c = Some (Lookup_fault_guard_mismatch (lookup_fault_guard_mismatch_lift c)))" unfolding lookup_fault_lift_def lookup_fault_guard_mismatch_lift_def by (clarsimp simp: lookup_fault_tag_defs Let_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (lookup_fault_get_tag c = SCAST(32 signed \<rightarrow> 32) lookup_fault_guard_mismatch) = (lookup_fault_lift c = Some (Lookup_fault_guard_mismatch (lookup_fault_guard_mismatch_lift c))) proof (prove)
goal (1 subgoal):
 1. (lookup_fault_get_tag c = SCAST(32 signed \<rightarrow> 32) lookup_fault_guard_mismatch) = ((let tag = lookup_fault_get_tag c in if tag = SCAST(32 signed \<rightarrow> 32) lookup_fault_invalid_root then Some Lookup_fault_invalid_root else if tag = SCAST(32 signed \<rightarrow> 32) lookup_fault_missing_capability then Some (Lookup_fault_missing_capability \<lparr>lookup_fault_missing_capability_CL.bitsLeft_CL = (lookup_fault_C.words_C c.[0] >> 2) && mask 6\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) lookup_fault_depth_mismatch then Some (Lookup_fault_depth_mismatch \<lparr>lookup_fault_depth_mismatch_CL.bitsFound_CL = (lookup_fault_C.words_C c.[0] >> 8) && mask 6, bitsLeft_CL = (lookup_fault_C.words_C c.[0] >> 2) && mask 6\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) lookup_fault_guard_mismatch then Some (Lookup_fault_guard_mismatch \<lparr>guardFound_CL = lookup_fault_C.words_C c.[1] >> 0, bitsLeft_CL = (lookup_fault_C.words_C c.[0] >> 8) && mask 6, bitsFound_CL = (lookup_fault_C.words_C c.[0] >> 2) && mask 6\<rparr>) else None) = Some (Lookup_fault_guard_mismatch (case let tag = lookup_fault_get_tag c in if tag = SCAST(32 signed \<rightarrow> 32) lookup_fault_invalid_root then Some Lookup_fault_invalid_root else if tag = SCAST(32 signed \<rightarrow> 32) lookup_fault_missing_capability then Some (Lookup_fault_missing_capability \<lparr>lookup_fault_missing_capability_CL.bitsLeft_CL = (lookup_fault_C.words_C c.[0] >> 2) && mask 6\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) lookup_fault_depth_mismatch then Some (Lookup_fault_depth_mismatch \<lparr>lookup_fault_depth_mismatch_CL.bitsFound_CL = (lookup_fault_C.words_C c.[0] >> 8) && mask 6, bitsLeft_CL = (lookup_fault_C.words_C c.[0] >> 2) && mask 6\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) lookup_fault_guard_mismatch then Some (Lookup_fault_guard_mismatch \<lparr>guardFound_CL = lookup_fault_C.words_C c.[1] >> 0, bitsLeft_CL = (lookup_fault_C.words_C c.[0] >> 8) && mask 6, bitsFound_CL = (lookup_fault_C.words_C c.[0] >> 2) && mask 6\<rparr>) else None of Some (Lookup_fault_guard_mismatch rec) \<Rightarrow> rec)))
theory structures_defs

lemma pde_get_tag_eq_x:
  "(pde_get_tag c = x) = ((((index (pde_C.words_C c) 0) >> 0) AND mask 2) = x)" by (auto simp add: pde_get_tag_def mask_def word_bw_assocs)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (pde_get_tag c = x) = ((pde_C.words_C c.[0] >> 0) && mask 2 = x)
theory structures_defs

lemma pde_lift_pde_invalid:
  "pde_get_tag pde = scast pde_pde_invalid \<Longrightarrow>
  pde_lift pde =
  Some (Pde_pde_invalid \<lparr> 
       pde_pde_invalid_CL.stored_hw_asid_CL = (((index (pde_C.words_C pde) 0) >> 24) AND mask 8),
       pde_pde_invalid_CL.stored_asid_valid_CL = (((index (pde_C.words_C pde) 0) >> 23) AND mask 1) \<rparr>)" by (simp add:pde_lift_def pde_tag_defs)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. pde_get_tag pde = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid \<Longrightarrow> pde_lift pde = Some (Pde_pde_invalid \<lparr>stored_hw_asid_CL = (pde_C.words_C pde.[0] >> 24) && mask 8, stored_asid_valid_CL = (pde_C.words_C pde.[0] >> 23) && mask 1\<rparr>)
theory structures_defs

lemma pde_lift_pde_coarse:
  "pde_get_tag pde = scast pde_pde_coarse \<Longrightarrow>
  pde_lift pde =
  Some (Pde_pde_coarse \<lparr> 
       pde_pde_coarse_CL.address_CL = (((index (pde_C.words_C pde) 0) << 0) AND NOT (mask 10)),
       pde_pde_coarse_CL.P_CL = (((index (pde_C.words_C pde) 0) >> 9) AND mask 1),
       pde_pde_coarse_CL.Domain_CL = (((index (pde_C.words_C pde) 0) >> 5) AND mask 4) \<rparr>)" by (simp add:pde_lift_def pde_tag_defs)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. pde_get_tag pde = SCAST(32 signed \<rightarrow> 32) pde_pde_coarse \<Longrightarrow> pde_lift pde = Some (Pde_pde_coarse \<lparr>pde_pde_coarse_CL.address_CL = (pde_C.words_C pde.[0] << 0) && ~~ mask 10, P_CL = (pde_C.words_C pde.[0] >> 9) && mask 1, Domain_CL = (pde_C.words_C pde.[0] >> 5) && mask 4\<rparr>)
theory structures_defs

lemma pde_lift_pde_section:
  "pde_get_tag pde = scast pde_pde_section \<Longrightarrow>
  pde_lift pde =
  Some (Pde_pde_section \<lparr> 
       pde_pde_section_CL.address_CL = (((index (pde_C.words_C pde) 0) << 0) AND NOT (mask 20)),
       pde_pde_section_CL.size_CL = (((index (pde_C.words_C pde) 0) >> 18) AND mask 1),
       pde_pde_section_CL.nG_CL = (((index (pde_C.words_C pde) 0) >> 17) AND mask 1),
       pde_pde_section_CL.S_CL = (((index (pde_C.words_C pde) 0) >> 16) AND mask 1),
       pde_pde_section_CL.APX_CL = (((index (pde_C.words_C pde) 0) >> 15) AND mask 1),
       pde_pde_section_CL.TEX_CL = (((index (pde_C.words_C pde) 0) >> 12) AND mask 3),
       pde_pde_section_CL.AP_CL = (((index (pde_C.words_C pde) 0) >> 10) AND mask 2),
       pde_pde_section_CL.P_CL = (((index (pde_C.words_C pde) 0) >> 9) AND mask 1),
       pde_pde_section_CL.Domain_CL = (((index (pde_C.words_C pde) 0) >> 5) AND mask 4),
       pde_pde_section_CL.XN_CL = (((index (pde_C.words_C pde) 0) >> 4) AND mask 1),
       pde_pde_section_CL.C_CL = (((index (pde_C.words_C pde) 0) >> 3) AND mask 1),
       pde_pde_section_CL.B_CL = (((index (pde_C.words_C pde) 0) >> 2) AND mask 1) \<rparr>)" by (simp add:pde_lift_def pde_tag_defs)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. pde_get_tag pde = SCAST(32 signed \<rightarrow> 32) pde_pde_section \<Longrightarrow> pde_lift pde = Some (Pde_pde_section \<lparr>pde_pde_section_CL.address_CL = (pde_C.words_C pde.[0] << 0) && ~~ mask 20, size_CL = (pde_C.words_C pde.[0] >> 18) && mask 1, nG_CL = (pde_C.words_C pde.[0] >> 17) && mask 1, S_CL = (pde_C.words_C pde.[0] >> 16) && mask 1, APX_CL = (pde_C.words_C pde.[0] >> 15) && mask 1, TEX_CL = (pde_C.words_C pde.[0] >> 12) && mask 3, AP_CL = (pde_C.words_C pde.[0] >> 10) && mask 2, P_CL = (pde_C.words_C pde.[0] >> 9) && mask 1, Domain_CL = (pde_C.words_C pde.[0] >> 5) && mask 4, XN_CL = (pde_C.words_C pde.[0] >> 4) && mask 1, C_CL = (pde_C.words_C pde.[0] >> 3) && mask 1, B_CL = (pde_C.words_C pde.[0] >> 2) && mask 1\<rparr>)
theory structures_defs

lemma pde_lift_pde_reserved:
  "pde_get_tag pde = scast pde_pde_reserved \<Longrightarrow>
  pde_lift pde =
  Some (Pde_pde_reserved)" by (simp add:pde_lift_def pde_tag_defs)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. pde_get_tag pde = SCAST(32 signed \<rightarrow> 32) pde_pde_reserved \<Longrightarrow> pde_lift pde = Some Pde_pde_reserved
theory structures_defs

lemma pte_get_tag_eq_x:
  "(pte_get_tag c = x) = ((((index (pte_C.words_C c) 0) >> 1) AND mask 1) = x)" by (auto simp add: pte_get_tag_def mask_def word_bw_assocs)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (pte_get_tag c = x) = ((pte_C.words_C c.[0] >> 1) && mask 1 = x)
theory structures_defs

lemma pte_lift_pte_large:
  "pte_get_tag pte = scast pte_pte_large \<Longrightarrow>
  pte_lift pte =
  Some (Pte_pte_large \<lparr> 
       pte_pte_large_CL.address_CL = (((index (pte_C.words_C pte) 0) << 0) AND NOT (mask 16)),
       pte_pte_large_CL.XN_CL = (((index (pte_C.words_C pte) 0) >> 15) AND mask 1),
       pte_pte_large_CL.TEX_CL = (((index (pte_C.words_C pte) 0) >> 12) AND mask 3),
       pte_pte_large_CL.nG_CL = (((index (pte_C.words_C pte) 0) >> 11) AND mask 1),
       pte_pte_large_CL.S_CL = (((index (pte_C.words_C pte) 0) >> 10) AND mask 1),
       pte_pte_large_CL.APX_CL = (((index (pte_C.words_C pte) 0) >> 9) AND mask 1),
       pte_pte_large_CL.AP_CL = (((index (pte_C.words_C pte) 0) >> 4) AND mask 2),
       pte_pte_large_CL.C_CL = (((index (pte_C.words_C pte) 0) >> 3) AND mask 1),
       pte_pte_large_CL.B_CL = (((index (pte_C.words_C pte) 0) >> 2) AND mask 1),
       pte_pte_large_CL.reserved_CL = (((index (pte_C.words_C pte) 0) >> 0) AND mask 1) \<rparr>)" by (simp add:pte_lift_def pte_tag_defs)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. pte_get_tag pte = SCAST(32 signed \<rightarrow> 32) pte_pte_large \<Longrightarrow> pte_lift pte = Some (Pte_pte_large \<lparr>pte_pte_large_CL.address_CL = (pte_C.words_C pte.[0] << 0) && ~~ mask 16, XN_CL = (pte_C.words_C pte.[0] >> 15) && mask 1, TEX_CL = (pte_C.words_C pte.[0] >> 12) && mask 3, nG_CL = (pte_C.words_C pte.[0] >> 11) && mask 1, S_CL = (pte_C.words_C pte.[0] >> 10) && mask 1, APX_CL = (pte_C.words_C pte.[0] >> 9) && mask 1, AP_CL = (pte_C.words_C pte.[0] >> 4) && mask 2, C_CL = (pte_C.words_C pte.[0] >> 3) && mask 1, B_CL = (pte_C.words_C pte.[0] >> 2) && mask 1, reserved_CL = (pte_C.words_C pte.[0] >> 0) && mask 1\<rparr>)
theory structures_defs

lemma pte_lift_pte_small:
  "pte_get_tag pte = scast pte_pte_small \<Longrightarrow>
  pte_lift pte =
  Some (Pte_pte_small \<lparr> 
       pte_pte_small_CL.address_CL = (((index (pte_C.words_C pte) 0) << 0) AND NOT (mask 12)),
       pte_pte_small_CL.nG_CL = (((index (pte_C.words_C pte) 0) >> 11) AND mask 1),
       pte_pte_small_CL.S_CL = (((index (pte_C.words_C pte) 0) >> 10) AND mask 1),
       pte_pte_small_CL.APX_CL = (((index (pte_C.words_C pte) 0) >> 9) AND mask 1),
       pte_pte_small_CL.TEX_CL = (((index (pte_C.words_C pte) 0) >> 6) AND mask 3),
       pte_pte_small_CL.AP_CL = (((index (pte_C.words_C pte) 0) >> 4) AND mask 2),
       pte_pte_small_CL.C_CL = (((index (pte_C.words_C pte) 0) >> 3) AND mask 1),
       pte_pte_small_CL.B_CL = (((index (pte_C.words_C pte) 0) >> 2) AND mask 1),
       pte_pte_small_CL.XN_CL = (((index (pte_C.words_C pte) 0) >> 0) AND mask 1) \<rparr>)" by (simp add:pte_lift_def pte_tag_defs)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. pte_get_tag pte = SCAST(32 signed \<rightarrow> 32) pte_pte_small \<Longrightarrow> pte_lift pte = Some (Pte_pte_small \<lparr>pte_pte_small_CL.address_CL = (pte_C.words_C pte.[0] << 0) && ~~ mask 12, nG_CL = (pte_C.words_C pte.[0] >> 11) && mask 1, S_CL = (pte_C.words_C pte.[0] >> 10) && mask 1, APX_CL = (pte_C.words_C pte.[0] >> 9) && mask 1, TEX_CL = (pte_C.words_C pte.[0] >> 6) && mask 3, AP_CL = (pte_C.words_C pte.[0] >> 4) && mask 2, C_CL = (pte_C.words_C pte.[0] >> 3) && mask 1, B_CL = (pte_C.words_C pte.[0] >> 2) && mask 1, XN_CL = (pte_C.words_C pte.[0] >> 0) && mask 1\<rparr>)