theory Finalise_C

lemma capFSize_eq: "\<lbrakk>ccap_relation (capability.ArchObjectCap (arch_capability.PageCap x31 x32 x33 x34 (Some (a, b)))) cap;
              x34 \<noteq> Wellformed_C.ARMSmallPage\<rbrakk>
  \<Longrightarrow> gen_framesize_to_H (capFSize_CL (cap_frame_cap_lift cap)) = x34" apply (frule (1) cap_get_tag_isCap_unfolded_H_cap) apply (clarsimp simp: cap_frame_cap_lift cap_to_H_def
                            case_option_over_if gen_framesize_to_H_def
                            ARM.pptrBase_def
                            framesize_to_H_def valid_cap'_def
                     elim!: ccap_relationE simp del: Collect_const) apply (subgoal_tac "capFSize_CL (cap_frame_cap_lift cap) \<noteq> scast Kernel_C.ARMSmallPage") apply simp apply (clarsimp simp: c_valid_cap_def cl_valid_cap_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ccap_relation (capability.ArchObjectCap (arch_capability.PageCap x31 x32 x33 x34 (Some (a, b)))) cap; x34 \<noteq> Wellformed_C.ARMSmallPage\<rbrakk> \<Longrightarrow> gen_framesize_to_H (capFSize_CL (cap_frame_cap_lift cap)) = x34 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ccap_relation (capability.ArchObjectCap (arch_capability.PageCap x31 x32 x33 x34 (Some (a, b)))) cap; x34 \<noteq> Wellformed_C.ARMSmallPage; cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_frame_cap\<rbrakk> \<Longrightarrow> gen_framesize_to_H (capFSize_CL (cap_frame_cap_lift cap)) = x34 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(if capFSize_CL (cap_frame_cap_lift cap) = SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMLargePage then Wellformed_C.ARMLargePage else if capFSize_CL (cap_frame_cap_lift cap) = SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSection then Wellformed_C.ARMSection else Wellformed_C.ARMSuperSection) \<noteq> Wellformed_C.ARMSmallPage; cap_lift cap = Some (Cap_frame_cap (cap_frame_cap_lift cap)); c_valid_cap cap; x31 = to_bool (cap_frame_cap_CL.capFIsDevice_CL (cap_frame_cap_lift cap)); x32 = cap_frame_cap_CL.capFBasePtr_CL (cap_frame_cap_lift cap); x33 = vmrights_to_H (cap_frame_cap_CL.capFVMRights_CL (cap_frame_cap_lift cap)); x34 = (if capFSize_CL (cap_frame_cap_lift cap) = SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMLargePage then Wellformed_C.ARMLargePage else if capFSize_CL (cap_frame_cap_lift cap) = SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSection then Wellformed_C.ARMSection else Wellformed_C.ARMSuperSection); Some (a, b) = (if cap_frame_cap_CL.capFMappedASIDHigh_CL (cap_frame_cap_lift cap) = 0 \<and> cap_frame_cap_CL.capFMappedASIDLow_CL (cap_frame_cap_lift cap) = 0 then None else Some ((cap_frame_cap_CL.capFMappedASIDHigh_CL (cap_frame_cap_lift cap) << local.asidLowBits) + cap_frame_cap_CL.capFMappedASIDLow_CL (cap_frame_cap_lift cap), cap_frame_cap_CL.capFMappedAddress_CL (cap_frame_cap_lift cap)))\<rbrakk> \<Longrightarrow> (if capFSize_CL (cap_frame_cap_lift cap) = SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSmallPage then Wellformed_C.ARMSmallPage else if capFSize_CL (cap_frame_cap_lift cap) = SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMLargePage then Wellformed_C.ARMLargePage else if capFSize_CL (cap_frame_cap_lift cap) = SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSection then Wellformed_C.ARMSection else Wellformed_C.ARMSuperSection) = (if capFSize_CL (cap_frame_cap_lift cap) = SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMLargePage then Wellformed_C.ARMLargePage else if capFSize_CL (cap_frame_cap_lift cap) = SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSection then Wellformed_C.ARMSection else Wellformed_C.ARMSuperSection) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>(if capFSize_CL (cap_frame_cap_lift cap) = SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMLargePage then Wellformed_C.ARMLargePage else if capFSize_CL (cap_frame_cap_lift cap) = SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSection then Wellformed_C.ARMSection else Wellformed_C.ARMSuperSection) \<noteq> Wellformed_C.ARMSmallPage; cap_lift cap = Some (Cap_frame_cap (cap_frame_cap_lift cap)); c_valid_cap cap; x31 = to_bool (cap_frame_cap_CL.capFIsDevice_CL (cap_frame_cap_lift cap)); x32 = cap_frame_cap_CL.capFBasePtr_CL (cap_frame_cap_lift cap); x33 = vmrights_to_H (cap_frame_cap_CL.capFVMRights_CL (cap_frame_cap_lift cap)); x34 = (if capFSize_CL (cap_frame_cap_lift cap) = SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMLargePage then Wellformed_C.ARMLargePage else if capFSize_CL (cap_frame_cap_lift cap) = SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSection then Wellformed_C.ARMSection else Wellformed_C.ARMSuperSection); Some (a, b) = (if cap_frame_cap_CL.capFMappedASIDHigh_CL (cap_frame_cap_lift cap) = 0 \<and> cap_frame_cap_CL.capFMappedASIDLow_CL (cap_frame_cap_lift cap) = 0 then None else Some ((cap_frame_cap_CL.capFMappedASIDHigh_CL (cap_frame_cap_lift cap) << local.asidLowBits) + cap_frame_cap_CL.capFMappedASIDLow_CL (cap_frame_cap_lift cap), cap_frame_cap_CL.capFMappedAddress_CL (cap_frame_cap_lift cap))); capFSize_CL (cap_frame_cap_lift cap) \<noteq> SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSmallPage\<rbrakk> \<Longrightarrow> (if capFSize_CL (cap_frame_cap_lift cap) = SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSmallPage then Wellformed_C.ARMSmallPage else if capFSize_CL (cap_frame_cap_lift cap) = SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMLargePage then Wellformed_C.ARMLargePage else if capFSize_CL (cap_frame_cap_lift cap) = SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSection then Wellformed_C.ARMSection else Wellformed_C.ARMSuperSection) = (if capFSize_CL (cap_frame_cap_lift cap) = SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMLargePage then Wellformed_C.ARMLargePage else if capFSize_CL (cap_frame_cap_lift cap) = SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSection then Wellformed_C.ARMSection else Wellformed_C.ARMSuperSection)
 2. \<lbrakk>(if capFSize_CL (cap_frame_cap_lift cap) = SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMLargePage then Wellformed_C.ARMLargePage else if capFSize_CL (cap_frame_cap_lift cap) = SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSection then Wellformed_C.ARMSection else Wellformed_C.ARMSuperSection) \<noteq> Wellformed_C.ARMSmallPage; cap_lift cap = Some (Cap_frame_cap (cap_frame_cap_lift cap)); c_valid_cap cap; x31 = to_bool (cap_frame_cap_CL.capFIsDevice_CL (cap_frame_cap_lift cap)); x32 = cap_frame_cap_CL.capFBasePtr_CL (cap_frame_cap_lift cap); x33 = vmrights_to_H (cap_frame_cap_CL.capFVMRights_CL (cap_frame_cap_lift cap)); x34 = (if capFSize_CL (cap_frame_cap_lift cap) = SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMLargePage then Wellformed_C.ARMLargePage else if capFSize_CL (cap_frame_cap_lift cap) = SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSection then Wellformed_C.ARMSection else Wellformed_C.ARMSuperSection); Some (a, b) = (if cap_frame_cap_CL.capFMappedASIDHigh_CL (cap_frame_cap_lift cap) = 0 \<and> cap_frame_cap_CL.capFMappedASIDLow_CL (cap_frame_cap_lift cap) = 0 then None else Some ((cap_frame_cap_CL.capFMappedASIDHigh_CL (cap_frame_cap_lift cap) << local.asidLowBits) + cap_frame_cap_CL.capFMappedASIDLow_CL (cap_frame_cap_lift cap), cap_frame_cap_CL.capFMappedAddress_CL (cap_frame_cap_lift cap)))\<rbrakk> \<Longrightarrow> capFSize_CL (cap_frame_cap_lift cap) \<noteq> SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSmallPage proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(if capFSize_CL (cap_frame_cap_lift cap) = SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMLargePage then Wellformed_C.ARMLargePage else if capFSize_CL (cap_frame_cap_lift cap) = SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSection then Wellformed_C.ARMSection else Wellformed_C.ARMSuperSection) \<noteq> Wellformed_C.ARMSmallPage; cap_lift cap = Some (Cap_frame_cap (cap_frame_cap_lift cap)); c_valid_cap cap; x31 = to_bool (cap_frame_cap_CL.capFIsDevice_CL (cap_frame_cap_lift cap)); x32 = cap_frame_cap_CL.capFBasePtr_CL (cap_frame_cap_lift cap); x33 = vmrights_to_H (cap_frame_cap_CL.capFVMRights_CL (cap_frame_cap_lift cap)); x34 = (if capFSize_CL (cap_frame_cap_lift cap) = SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMLargePage then Wellformed_C.ARMLargePage else if capFSize_CL (cap_frame_cap_lift cap) = SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSection then Wellformed_C.ARMSection else Wellformed_C.ARMSuperSection); Some (a, b) = (if cap_frame_cap_CL.capFMappedASIDHigh_CL (cap_frame_cap_lift cap) = 0 \<and> cap_frame_cap_CL.capFMappedASIDLow_CL (cap_frame_cap_lift cap) = 0 then None else Some ((cap_frame_cap_CL.capFMappedASIDHigh_CL (cap_frame_cap_lift cap) << local.asidLowBits) + cap_frame_cap_CL.capFMappedASIDLow_CL (cap_frame_cap_lift cap), cap_frame_cap_CL.capFMappedAddress_CL (cap_frame_cap_lift cap)))\<rbrakk> \<Longrightarrow> capFSize_CL (cap_frame_cap_lift cap) \<noteq> SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSmallPage proof (prove)
goal:
No subgoals!