kings-crown/FVELER_Isabelle huggingface dataset:
theory structures_defs

lemma pte_pte_large_lift:
  "(pte_get_tag c = scast pte_pte_large) = (pte_lift c = Some (Pte_pte_large (pte_pte_large_lift c)))" unfolding pte_lift_def pte_pte_large_lift_def by (clarsimp simp: pte_tag_defs Let_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (pte_get_tag c = SCAST(32 signed \<rightarrow> 32) pte_pte_large) = (pte_lift c = Some (Pte_pte_large (pte_pte_large_lift c))) proof (prove)
goal (1 subgoal):
 1. (pte_get_tag c = SCAST(32 signed \<rightarrow> 32) pte_pte_large) = ((let tag = pte_get_tag c in if tag = SCAST(32 signed \<rightarrow> 32) pte_pte_large then Some (Pte_pte_large \<lparr>pte_pte_large_CL.address_CL = (pte_C.words_C c.[0] << 0) && ~~ mask 16, XN_CL = (pte_C.words_C c.[0] >> 15) && mask 1, TEX_CL = (pte_C.words_C c.[0] >> 12) && mask 3, nG_CL = (pte_C.words_C c.[0] >> 11) && mask 1, S_CL = (pte_C.words_C c.[0] >> 10) && mask 1, APX_CL = (pte_C.words_C c.[0] >> 9) && mask 1, AP_CL = (pte_C.words_C c.[0] >> 4) && mask 2, C_CL = (pte_C.words_C c.[0] >> 3) && mask 1, B_CL = (pte_C.words_C c.[0] >> 2) && mask 1, reserved_CL = (pte_C.words_C c.[0] >> 0) && mask 1\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) pte_pte_small then Some (Pte_pte_small \<lparr>pte_pte_small_CL.address_CL = (pte_C.words_C c.[0] << 0) && ~~ mask 12, nG_CL = (pte_C.words_C c.[0] >> 11) && mask 1, S_CL = (pte_C.words_C c.[0] >> 10) && mask 1, APX_CL = (pte_C.words_C c.[0] >> 9) && mask 1, TEX_CL = (pte_C.words_C c.[0] >> 6) && mask 3, AP_CL = (pte_C.words_C c.[0] >> 4) && mask 2, C_CL = (pte_C.words_C c.[0] >> 3) && mask 1, B_CL = (pte_C.words_C c.[0] >> 2) && mask 1, XN_CL = (pte_C.words_C c.[0] >> 0) && mask 1\<rparr>) else None) = Some (Pte_pte_large (case let tag = pte_get_tag c in if tag = SCAST(32 signed \<rightarrow> 32) pte_pte_large then Some (Pte_pte_large \<lparr>pte_pte_large_CL.address_CL = (pte_C.words_C c.[0] << 0) && ~~ mask 16, XN_CL = (pte_C.words_C c.[0] >> 15) && mask 1, TEX_CL = (pte_C.words_C c.[0] >> 12) && mask 3, nG_CL = (pte_C.words_C c.[0] >> 11) && mask 1, S_CL = (pte_C.words_C c.[0] >> 10) && mask 1, APX_CL = (pte_C.words_C c.[0] >> 9) && mask 1, AP_CL = (pte_C.words_C c.[0] >> 4) && mask 2, C_CL = (pte_C.words_C c.[0] >> 3) && mask 1, B_CL = (pte_C.words_C c.[0] >> 2) && mask 1, reserved_CL = (pte_C.words_C c.[0] >> 0) && mask 1\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) pte_pte_small then Some (Pte_pte_small \<lparr>pte_pte_small_CL.address_CL = (pte_C.words_C c.[0] << 0) && ~~ mask 12, nG_CL = (pte_C.words_C c.[0] >> 11) && mask 1, S_CL = (pte_C.words_C c.[0] >> 10) && mask 1, APX_CL = (pte_C.words_C c.[0] >> 9) && mask 1, TEX_CL = (pte_C.words_C c.[0] >> 6) && mask 3, AP_CL = (pte_C.words_C c.[0] >> 4) && mask 2, C_CL = (pte_C.words_C c.[0] >> 3) && mask 1, B_CL = (pte_C.words_C c.[0] >> 2) && mask 1, XN_CL = (pte_C.words_C c.[0] >> 0) && mask 1\<rparr>) else None of Some (Pte_pte_large rec) \<Rightarrow> rec)))
theory structures_defs

lemma pte_pte_small_lift:
  "(pte_get_tag c = scast pte_pte_small) = (pte_lift c = Some (Pte_pte_small (pte_pte_small_lift c)))" unfolding pte_lift_def pte_pte_small_lift_def by (clarsimp simp: pte_tag_defs Let_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (pte_get_tag c = SCAST(32 signed \<rightarrow> 32) pte_pte_small) = (pte_lift c = Some (Pte_pte_small (pte_pte_small_lift c))) proof (prove)
goal (1 subgoal):
 1. (pte_get_tag c = SCAST(32 signed \<rightarrow> 32) pte_pte_small) = ((let tag = pte_get_tag c in if tag = SCAST(32 signed \<rightarrow> 32) pte_pte_large then Some (Pte_pte_large \<lparr>pte_pte_large_CL.address_CL = (pte_C.words_C c.[0] << 0) && ~~ mask 16, XN_CL = (pte_C.words_C c.[0] >> 15) && mask 1, TEX_CL = (pte_C.words_C c.[0] >> 12) && mask 3, nG_CL = (pte_C.words_C c.[0] >> 11) && mask 1, S_CL = (pte_C.words_C c.[0] >> 10) && mask 1, APX_CL = (pte_C.words_C c.[0] >> 9) && mask 1, AP_CL = (pte_C.words_C c.[0] >> 4) && mask 2, C_CL = (pte_C.words_C c.[0] >> 3) && mask 1, B_CL = (pte_C.words_C c.[0] >> 2) && mask 1, reserved_CL = (pte_C.words_C c.[0] >> 0) && mask 1\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) pte_pte_small then Some (Pte_pte_small \<lparr>pte_pte_small_CL.address_CL = (pte_C.words_C c.[0] << 0) && ~~ mask 12, nG_CL = (pte_C.words_C c.[0] >> 11) && mask 1, S_CL = (pte_C.words_C c.[0] >> 10) && mask 1, APX_CL = (pte_C.words_C c.[0] >> 9) && mask 1, TEX_CL = (pte_C.words_C c.[0] >> 6) && mask 3, AP_CL = (pte_C.words_C c.[0] >> 4) && mask 2, C_CL = (pte_C.words_C c.[0] >> 3) && mask 1, B_CL = (pte_C.words_C c.[0] >> 2) && mask 1, XN_CL = (pte_C.words_C c.[0] >> 0) && mask 1\<rparr>) else None) = Some (Pte_pte_small (case let tag = pte_get_tag c in if tag = SCAST(32 signed \<rightarrow> 32) pte_pte_large then Some (Pte_pte_large \<lparr>pte_pte_large_CL.address_CL = (pte_C.words_C c.[0] << 0) && ~~ mask 16, XN_CL = (pte_C.words_C c.[0] >> 15) && mask 1, TEX_CL = (pte_C.words_C c.[0] >> 12) && mask 3, nG_CL = (pte_C.words_C c.[0] >> 11) && mask 1, S_CL = (pte_C.words_C c.[0] >> 10) && mask 1, APX_CL = (pte_C.words_C c.[0] >> 9) && mask 1, AP_CL = (pte_C.words_C c.[0] >> 4) && mask 2, C_CL = (pte_C.words_C c.[0] >> 3) && mask 1, B_CL = (pte_C.words_C c.[0] >> 2) && mask 1, reserved_CL = (pte_C.words_C c.[0] >> 0) && mask 1\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) pte_pte_small then Some (Pte_pte_small \<lparr>pte_pte_small_CL.address_CL = (pte_C.words_C c.[0] << 0) && ~~ mask 12, nG_CL = (pte_C.words_C c.[0] >> 11) && mask 1, S_CL = (pte_C.words_C c.[0] >> 10) && mask 1, APX_CL = (pte_C.words_C c.[0] >> 9) && mask 1, TEX_CL = (pte_C.words_C c.[0] >> 6) && mask 3, AP_CL = (pte_C.words_C c.[0] >> 4) && mask 2, C_CL = (pte_C.words_C c.[0] >> 3) && mask 1, B_CL = (pte_C.words_C c.[0] >> 2) && mask 1, XN_CL = (pte_C.words_C c.[0] >> 0) && mask 1\<rparr>) else None of Some (Pte_pte_small rec) \<Rightarrow> rec)))
theory structures_defs

lemma seL4_Fault_get_tag_eq_x:
  "(seL4_Fault_get_tag c = x) = ((((index (seL4_Fault_C.words_C c) 0) >> 0) AND mask 4) = x)" by (auto simp add: seL4_Fault_get_tag_def mask_def word_bw_assocs)

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

lemma seL4_Fault_lift_NullFault:
  "seL4_Fault_get_tag seL4_Fault = scast seL4_Fault_NullFault \<Longrightarrow>
  seL4_Fault_lift seL4_Fault =
  Some (SeL4_Fault_NullFault)" by (simp add:seL4_Fault_lift_def seL4_Fault_tag_defs)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. seL4_Fault_get_tag seL4_Fault = SCAST(32 signed \<rightarrow> 32) seL4_Fault_NullFault \<Longrightarrow> seL4_Fault_lift seL4_Fault = Some SeL4_Fault_NullFault
theory structures_defs

lemma seL4_Fault_lift_CapFault:
  "seL4_Fault_get_tag seL4_Fault = scast seL4_Fault_CapFault \<Longrightarrow>
  seL4_Fault_lift seL4_Fault =
  Some (SeL4_Fault_CapFault \<lparr> 
       seL4_Fault_CapFault_CL.address_CL = (((index (seL4_Fault_C.words_C seL4_Fault) 1) >> 0)),
       seL4_Fault_CapFault_CL.inReceivePhase_CL = (((index (seL4_Fault_C.words_C seL4_Fault) 0) >> 31) AND mask 1) \<rparr>)" by (simp add:seL4_Fault_lift_def seL4_Fault_tag_defs)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. seL4_Fault_get_tag seL4_Fault = SCAST(32 signed \<rightarrow> 32) seL4_Fault_CapFault \<Longrightarrow> seL4_Fault_lift seL4_Fault = Some (SeL4_Fault_CapFault \<lparr>seL4_Fault_CapFault_CL.address_CL = seL4_Fault_C.words_C seL4_Fault.[1] >> 0, inReceivePhase_CL = (seL4_Fault_C.words_C seL4_Fault.[0] >> 31) && mask 1\<rparr>)
theory structures_defs

lemma seL4_Fault_lift_UnknownSyscall:
  "seL4_Fault_get_tag seL4_Fault = scast seL4_Fault_UnknownSyscall \<Longrightarrow>
  seL4_Fault_lift seL4_Fault =
  Some (SeL4_Fault_UnknownSyscall \<lparr> 
       seL4_Fault_UnknownSyscall_CL.syscallNumber_CL = (((index (seL4_Fault_C.words_C seL4_Fault) 1) >> 0)) \<rparr>)" by (simp add:seL4_Fault_lift_def seL4_Fault_tag_defs)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. seL4_Fault_get_tag seL4_Fault = SCAST(32 signed \<rightarrow> 32) seL4_Fault_UnknownSyscall \<Longrightarrow> seL4_Fault_lift seL4_Fault = Some (SeL4_Fault_UnknownSyscall \<lparr>syscallNumber_CL = seL4_Fault_C.words_C seL4_Fault.[1] >> 0\<rparr>)
theory structures_defs

lemma seL4_Fault_lift_UserException:
  "seL4_Fault_get_tag seL4_Fault = scast seL4_Fault_UserException \<Longrightarrow>
  seL4_Fault_lift seL4_Fault =
  Some (SeL4_Fault_UserException \<lparr> 
       seL4_Fault_UserException_CL.number_CL = (((index (seL4_Fault_C.words_C seL4_Fault) 1) >> 0)),
       seL4_Fault_UserException_CL.code_CL = (((index (seL4_Fault_C.words_C seL4_Fault) 0) >> 4) AND mask 28) \<rparr>)" by (simp add:seL4_Fault_lift_def seL4_Fault_tag_defs)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. seL4_Fault_get_tag seL4_Fault = SCAST(32 signed \<rightarrow> 32) seL4_Fault_UserException \<Longrightarrow> seL4_Fault_lift seL4_Fault = Some (SeL4_Fault_UserException \<lparr>number_CL = seL4_Fault_C.words_C seL4_Fault.[1] >> 0, code_CL = (seL4_Fault_C.words_C seL4_Fault.[0] >> 4) && mask 28\<rparr>)
theory structures_defs

lemma seL4_Fault_lift_VMFault:
  "seL4_Fault_get_tag seL4_Fault = scast seL4_Fault_VMFault \<Longrightarrow>
  seL4_Fault_lift seL4_Fault =
  Some (SeL4_Fault_VMFault \<lparr> 
       seL4_Fault_VMFault_CL.address_CL = (((index (seL4_Fault_C.words_C seL4_Fault) 1) >> 0)),
       seL4_Fault_VMFault_CL.FSR_CL = (((index (seL4_Fault_C.words_C seL4_Fault) 0) >> 18) AND mask 14),
       seL4_Fault_VMFault_CL.instructionFault_CL = (((index (seL4_Fault_C.words_C seL4_Fault) 0) >> 17) AND mask 1) \<rparr>)" by (simp add:seL4_Fault_lift_def seL4_Fault_tag_defs)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. seL4_Fault_get_tag seL4_Fault = SCAST(32 signed \<rightarrow> 32) seL4_Fault_VMFault \<Longrightarrow> seL4_Fault_lift seL4_Fault = Some (SeL4_Fault_VMFault \<lparr>seL4_Fault_VMFault_CL.address_CL = seL4_Fault_C.words_C seL4_Fault.[1] >> 0, FSR_CL = (seL4_Fault_C.words_C seL4_Fault.[0] >> 18) && mask 14, instructionFault_CL = (seL4_Fault_C.words_C seL4_Fault.[0] >> 17) && mask 1\<rparr>)
theory structures_defs

lemma seL4_Fault_CapFault_lift:
  "(seL4_Fault_get_tag c = scast seL4_Fault_CapFault) = (seL4_Fault_lift c = Some (SeL4_Fault_CapFault (seL4_Fault_CapFault_lift c)))" unfolding seL4_Fault_lift_def seL4_Fault_CapFault_lift_def by (clarsimp simp: seL4_Fault_tag_defs Let_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (seL4_Fault_get_tag c = SCAST(32 signed \<rightarrow> 32) seL4_Fault_CapFault) = (seL4_Fault_lift c = Some (SeL4_Fault_CapFault (seL4_Fault_CapFault_lift c))) proof (prove)
goal (1 subgoal):
 1. (seL4_Fault_get_tag c = SCAST(32 signed \<rightarrow> 32) seL4_Fault_CapFault) = ((let tag = seL4_Fault_get_tag c in if tag = SCAST(32 signed \<rightarrow> 32) seL4_Fault_NullFault then Some SeL4_Fault_NullFault else if tag = SCAST(32 signed \<rightarrow> 32) seL4_Fault_CapFault then Some (SeL4_Fault_CapFault \<lparr>seL4_Fault_CapFault_CL.address_CL = seL4_Fault_C.words_C c.[1] >> 0, inReceivePhase_CL = (seL4_Fault_C.words_C c.[0] >> 31) && mask 1\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) seL4_Fault_UnknownSyscall then Some (SeL4_Fault_UnknownSyscall \<lparr>syscallNumber_CL = seL4_Fault_C.words_C c.[1] >> 0\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) seL4_Fault_UserException then Some (SeL4_Fault_UserException \<lparr>number_CL = seL4_Fault_C.words_C c.[1] >> 0, code_CL = (seL4_Fault_C.words_C c.[0] >> 4) && mask 28\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) seL4_Fault_VMFault then Some (SeL4_Fault_VMFault \<lparr>seL4_Fault_VMFault_CL.address_CL = seL4_Fault_C.words_C c.[1] >> 0, FSR_CL = (seL4_Fault_C.words_C c.[0] >> 18) && mask 14, instructionFault_CL = (seL4_Fault_C.words_C c.[0] >> 17) && mask 1\<rparr>) else None) = Some (SeL4_Fault_CapFault (case let tag = seL4_Fault_get_tag c in if tag = SCAST(32 signed \<rightarrow> 32) seL4_Fault_NullFault then Some SeL4_Fault_NullFault else if tag = SCAST(32 signed \<rightarrow> 32) seL4_Fault_CapFault then Some (SeL4_Fault_CapFault \<lparr>seL4_Fault_CapFault_CL.address_CL = seL4_Fault_C.words_C c.[1] >> 0, inReceivePhase_CL = (seL4_Fault_C.words_C c.[0] >> 31) && mask 1\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) seL4_Fault_UnknownSyscall then Some (SeL4_Fault_UnknownSyscall \<lparr>syscallNumber_CL = seL4_Fault_C.words_C c.[1] >> 0\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) seL4_Fault_UserException then Some (SeL4_Fault_UserException \<lparr>number_CL = seL4_Fault_C.words_C c.[1] >> 0, code_CL = (seL4_Fault_C.words_C c.[0] >> 4) && mask 28\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) seL4_Fault_VMFault then Some (SeL4_Fault_VMFault \<lparr>seL4_Fault_VMFault_CL.address_CL = seL4_Fault_C.words_C c.[1] >> 0, FSR_CL = (seL4_Fault_C.words_C c.[0] >> 18) && mask 14, instructionFault_CL = (seL4_Fault_C.words_C c.[0] >> 17) && mask 1\<rparr>) else None of Some (SeL4_Fault_CapFault rec) \<Rightarrow> rec)))
theory structures_defs

lemma seL4_Fault_UnknownSyscall_lift:
  "(seL4_Fault_get_tag c = scast seL4_Fault_UnknownSyscall) = (seL4_Fault_lift c = Some (SeL4_Fault_UnknownSyscall (seL4_Fault_UnknownSyscall_lift c)))" unfolding seL4_Fault_lift_def seL4_Fault_UnknownSyscall_lift_def by (clarsimp simp: seL4_Fault_tag_defs Let_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (seL4_Fault_get_tag c = SCAST(32 signed \<rightarrow> 32) seL4_Fault_UnknownSyscall) = (seL4_Fault_lift c = Some (SeL4_Fault_UnknownSyscall (seL4_Fault_UnknownSyscall_lift c))) proof (prove)
goal (1 subgoal):
 1. (seL4_Fault_get_tag c = SCAST(32 signed \<rightarrow> 32) seL4_Fault_UnknownSyscall) = ((let tag = seL4_Fault_get_tag c in if tag = SCAST(32 signed \<rightarrow> 32) seL4_Fault_NullFault then Some SeL4_Fault_NullFault else if tag = SCAST(32 signed \<rightarrow> 32) seL4_Fault_CapFault then Some (SeL4_Fault_CapFault \<lparr>seL4_Fault_CapFault_CL.address_CL = seL4_Fault_C.words_C c.[1] >> 0, inReceivePhase_CL = (seL4_Fault_C.words_C c.[0] >> 31) && mask 1\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) seL4_Fault_UnknownSyscall then Some (SeL4_Fault_UnknownSyscall \<lparr>syscallNumber_CL = seL4_Fault_C.words_C c.[1] >> 0\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) seL4_Fault_UserException then Some (SeL4_Fault_UserException \<lparr>number_CL = seL4_Fault_C.words_C c.[1] >> 0, code_CL = (seL4_Fault_C.words_C c.[0] >> 4) && mask 28\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) seL4_Fault_VMFault then Some (SeL4_Fault_VMFault \<lparr>seL4_Fault_VMFault_CL.address_CL = seL4_Fault_C.words_C c.[1] >> 0, FSR_CL = (seL4_Fault_C.words_C c.[0] >> 18) && mask 14, instructionFault_CL = (seL4_Fault_C.words_C c.[0] >> 17) && mask 1\<rparr>) else None) = Some (SeL4_Fault_UnknownSyscall (case let tag = seL4_Fault_get_tag c in if tag = SCAST(32 signed \<rightarrow> 32) seL4_Fault_NullFault then Some SeL4_Fault_NullFault else if tag = SCAST(32 signed \<rightarrow> 32) seL4_Fault_CapFault then Some (SeL4_Fault_CapFault \<lparr>seL4_Fault_CapFault_CL.address_CL = seL4_Fault_C.words_C c.[1] >> 0, inReceivePhase_CL = (seL4_Fault_C.words_C c.[0] >> 31) && mask 1\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) seL4_Fault_UnknownSyscall then Some (SeL4_Fault_UnknownSyscall \<lparr>syscallNumber_CL = seL4_Fault_C.words_C c.[1] >> 0\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) seL4_Fault_UserException then Some (SeL4_Fault_UserException \<lparr>number_CL = seL4_Fault_C.words_C c.[1] >> 0, code_CL = (seL4_Fault_C.words_C c.[0] >> 4) && mask 28\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) seL4_Fault_VMFault then Some (SeL4_Fault_VMFault \<lparr>seL4_Fault_VMFault_CL.address_CL = seL4_Fault_C.words_C c.[1] >> 0, FSR_CL = (seL4_Fault_C.words_C c.[0] >> 18) && mask 14, instructionFault_CL = (seL4_Fault_C.words_C c.[0] >> 17) && mask 1\<rparr>) else None of Some (SeL4_Fault_UnknownSyscall rec) \<Rightarrow> rec)))
theory structures_defs

lemma seL4_Fault_UserException_lift:
  "(seL4_Fault_get_tag c = scast seL4_Fault_UserException) = (seL4_Fault_lift c = Some (SeL4_Fault_UserException (seL4_Fault_UserException_lift c)))" unfolding seL4_Fault_lift_def seL4_Fault_UserException_lift_def by (clarsimp simp: seL4_Fault_tag_defs Let_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (seL4_Fault_get_tag c = SCAST(32 signed \<rightarrow> 32) seL4_Fault_UserException) = (seL4_Fault_lift c = Some (SeL4_Fault_UserException (seL4_Fault_UserException_lift c))) proof (prove)
goal (1 subgoal):
 1. (seL4_Fault_get_tag c = SCAST(32 signed \<rightarrow> 32) seL4_Fault_UserException) = ((let tag = seL4_Fault_get_tag c in if tag = SCAST(32 signed \<rightarrow> 32) seL4_Fault_NullFault then Some SeL4_Fault_NullFault else if tag = SCAST(32 signed \<rightarrow> 32) seL4_Fault_CapFault then Some (SeL4_Fault_CapFault \<lparr>seL4_Fault_CapFault_CL.address_CL = seL4_Fault_C.words_C c.[1] >> 0, inReceivePhase_CL = (seL4_Fault_C.words_C c.[0] >> 31) && mask 1\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) seL4_Fault_UnknownSyscall then Some (SeL4_Fault_UnknownSyscall \<lparr>syscallNumber_CL = seL4_Fault_C.words_C c.[1] >> 0\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) seL4_Fault_UserException then Some (SeL4_Fault_UserException \<lparr>number_CL = seL4_Fault_C.words_C c.[1] >> 0, code_CL = (seL4_Fault_C.words_C c.[0] >> 4) && mask 28\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) seL4_Fault_VMFault then Some (SeL4_Fault_VMFault \<lparr>seL4_Fault_VMFault_CL.address_CL = seL4_Fault_C.words_C c.[1] >> 0, FSR_CL = (seL4_Fault_C.words_C c.[0] >> 18) && mask 14, instructionFault_CL = (seL4_Fault_C.words_C c.[0] >> 17) && mask 1\<rparr>) else None) = Some (SeL4_Fault_UserException (case let tag = seL4_Fault_get_tag c in if tag = SCAST(32 signed \<rightarrow> 32) seL4_Fault_NullFault then Some SeL4_Fault_NullFault else if tag = SCAST(32 signed \<rightarrow> 32) seL4_Fault_CapFault then Some (SeL4_Fault_CapFault \<lparr>seL4_Fault_CapFault_CL.address_CL = seL4_Fault_C.words_C c.[1] >> 0, inReceivePhase_CL = (seL4_Fault_C.words_C c.[0] >> 31) && mask 1\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) seL4_Fault_UnknownSyscall then Some (SeL4_Fault_UnknownSyscall \<lparr>syscallNumber_CL = seL4_Fault_C.words_C c.[1] >> 0\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) seL4_Fault_UserException then Some (SeL4_Fault_UserException \<lparr>number_CL = seL4_Fault_C.words_C c.[1] >> 0, code_CL = (seL4_Fault_C.words_C c.[0] >> 4) && mask 28\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) seL4_Fault_VMFault then Some (SeL4_Fault_VMFault \<lparr>seL4_Fault_VMFault_CL.address_CL = seL4_Fault_C.words_C c.[1] >> 0, FSR_CL = (seL4_Fault_C.words_C c.[0] >> 18) && mask 14, instructionFault_CL = (seL4_Fault_C.words_C c.[0] >> 17) && mask 1\<rparr>) else None of Some (SeL4_Fault_UserException rec) \<Rightarrow> rec)))
theory structures_defs

lemma seL4_Fault_VMFault_lift:
  "(seL4_Fault_get_tag c = scast seL4_Fault_VMFault) = (seL4_Fault_lift c = Some (SeL4_Fault_VMFault (seL4_Fault_VMFault_lift c)))" unfolding seL4_Fault_lift_def seL4_Fault_VMFault_lift_def by (clarsimp simp: seL4_Fault_tag_defs Let_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (seL4_Fault_get_tag c = SCAST(32 signed \<rightarrow> 32) seL4_Fault_VMFault) = (seL4_Fault_lift c = Some (SeL4_Fault_VMFault (seL4_Fault_VMFault_lift c))) proof (prove)
goal (1 subgoal):
 1. (seL4_Fault_get_tag c = SCAST(32 signed \<rightarrow> 32) seL4_Fault_VMFault) = ((let tag = seL4_Fault_get_tag c in if tag = SCAST(32 signed \<rightarrow> 32) seL4_Fault_NullFault then Some SeL4_Fault_NullFault else if tag = SCAST(32 signed \<rightarrow> 32) seL4_Fault_CapFault then Some (SeL4_Fault_CapFault \<lparr>seL4_Fault_CapFault_CL.address_CL = seL4_Fault_C.words_C c.[1] >> 0, inReceivePhase_CL = (seL4_Fault_C.words_C c.[0] >> 31) && mask 1\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) seL4_Fault_UnknownSyscall then Some (SeL4_Fault_UnknownSyscall \<lparr>syscallNumber_CL = seL4_Fault_C.words_C c.[1] >> 0\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) seL4_Fault_UserException then Some (SeL4_Fault_UserException \<lparr>number_CL = seL4_Fault_C.words_C c.[1] >> 0, code_CL = (seL4_Fault_C.words_C c.[0] >> 4) && mask 28\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) seL4_Fault_VMFault then Some (SeL4_Fault_VMFault \<lparr>seL4_Fault_VMFault_CL.address_CL = seL4_Fault_C.words_C c.[1] >> 0, FSR_CL = (seL4_Fault_C.words_C c.[0] >> 18) && mask 14, instructionFault_CL = (seL4_Fault_C.words_C c.[0] >> 17) && mask 1\<rparr>) else None) = Some (SeL4_Fault_VMFault (case let tag = seL4_Fault_get_tag c in if tag = SCAST(32 signed \<rightarrow> 32) seL4_Fault_NullFault then Some SeL4_Fault_NullFault else if tag = SCAST(32 signed \<rightarrow> 32) seL4_Fault_CapFault then Some (SeL4_Fault_CapFault \<lparr>seL4_Fault_CapFault_CL.address_CL = seL4_Fault_C.words_C c.[1] >> 0, inReceivePhase_CL = (seL4_Fault_C.words_C c.[0] >> 31) && mask 1\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) seL4_Fault_UnknownSyscall then Some (SeL4_Fault_UnknownSyscall \<lparr>syscallNumber_CL = seL4_Fault_C.words_C c.[1] >> 0\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) seL4_Fault_UserException then Some (SeL4_Fault_UserException \<lparr>number_CL = seL4_Fault_C.words_C c.[1] >> 0, code_CL = (seL4_Fault_C.words_C c.[0] >> 4) && mask 28\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) seL4_Fault_VMFault then Some (SeL4_Fault_VMFault \<lparr>seL4_Fault_VMFault_CL.address_CL = seL4_Fault_C.words_C c.[1] >> 0, FSR_CL = (seL4_Fault_C.words_C c.[0] >> 18) && mask 14, instructionFault_CL = (seL4_Fault_C.words_C c.[0] >> 17) && mask 1\<rparr>) else None of Some (SeL4_Fault_VMFault rec) \<Rightarrow> rec)))
theory structures_proofs

lemma endpoint_ptr_words_NULL:
  "c_guard (p::endpoint_C ptr) \<Longrightarrow>
   0 < &(p\<rightarrow>[''words_C''])" by (fastforce intro:c_guard_NULL_fl simp:typ_uinfo_t_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. c_guard p \<Longrightarrow> 0 < &(p\<rightarrow>[''words_C''])
theory structures_proofs

lemma endpoint_ptr_words_ptr_safe:
  "ptr_safe (p::endpoint_C ptr) d \<Longrightarrow>
   ptr_safe (Ptr &(p\<rightarrow>[''words_C''])::((word32[4]) ptr)) d" by (fastforce intro:ptr_safe_mono simp:typ_uinfo_t_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ptr_safe p d \<Longrightarrow> ptr_safe (PTR(32 word[4]) &(p\<rightarrow>[''words_C''])) d
theory structures_proofs

lemma mdb_node_ptr_words_NULL:
  "c_guard (p::mdb_node_C ptr) \<Longrightarrow>
   0 < &(p\<rightarrow>[''words_C''])" by (fastforce intro:c_guard_NULL_fl simp:typ_uinfo_t_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. c_guard p \<Longrightarrow> 0 < &(p\<rightarrow>[''words_C''])
theory structures_proofs

lemma mdb_node_ptr_words_aligned:
  "c_guard (p::mdb_node_C ptr) \<Longrightarrow>
   ptr_aligned ((Ptr &(p\<rightarrow>[''words_C'']))::((word32[2]) ptr))" by (fastforce intro:c_guard_ptr_aligned_fl simp:typ_uinfo_t_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. c_guard p \<Longrightarrow> ptr_aligned (PTR(32 word[2]) &(p\<rightarrow>[''words_C'']))