theory CSpace_C

lemma generic_frame_cap_get_capFSize_spec:
  "\<forall>s. \<Gamma> \<turnstile> \<lbrace>s. cap_get_tag \<acute>cap = scast cap_small_frame_cap \<or>
                cap_get_tag \<acute>cap = scast cap_frame_cap\<rbrace>
       \<acute>ret__unsigned_long :== PROC generic_frame_cap_get_capFSize(\<acute>cap)
       \<lbrace>\<acute>ret__unsigned_long = generic_frame_cap_get_capFSize_CL (cap_lift \<^bsup>s\<^esup>cap)\<rbrace>" apply vcg apply (clarsimp simp: generic_frame_cap_get_capFSize_CL_def) apply (intro conjI impI) apply (clarsimp simp: cap_lift_small_frame_cap cap_small_frame_cap_lift_def) apply (clarsimp simp: cap_lift_frame_cap cap_frame_cap_lift_def) apply (clarsimp simp: cap_lifts [THEN sym]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>s. \<Gamma>\<turnstile> \<lbrace>s. cap_get_tag \<acute>cap = SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap \<or> cap_get_tag \<acute>cap = SCAST(32 signed \<rightarrow> 32) cap_frame_cap\<rbrace> Call generic_frame_cap_get_capFSize_'proc \<lbrace>\<acute>ret__unsigned_long = generic_frame_cap_get_capFSize_CL (cap_lift \<^bsup>s\<^esup>cap)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>cap. cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap \<or> cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_frame_cap \<Longrightarrow> \<forall>ret__unsigned. ret__unsigned = cap_get_tag cap \<longrightarrow> (cap_small_frame_cap = UCAST(32 \<rightarrow> 32 signed) (cap_get_tag cap) \<longrightarrow> SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSmallPage = generic_frame_cap_get_capFSize_CL (cap_lift cap)) \<and> (cap_small_frame_cap \<noteq> UCAST(32 \<rightarrow> 32 signed) (cap_get_tag cap) \<longrightarrow> (cap_frame_cap = UCAST(32 \<rightarrow> 32 signed) (cap_get_tag cap) \<longrightarrow> cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_frame_cap \<and> (\<forall>ret__unsigned. ret__unsigned = capFSize_CL (cap_frame_cap_lift cap) \<longrightarrow> UCAST(32 \<rightarrow> 32) (capFSize_CL (cap_frame_cap_lift cap)) = generic_frame_cap_get_capFSize_CL (cap_lift cap))) \<and> (cap_frame_cap \<noteq> UCAST(32 \<rightarrow> 32 signed) (cap_get_tag cap) \<longrightarrow> SCAST(32 signed \<rightarrow> 32) 0 = generic_frame_cap_get_capFSize_CL (cap_lift cap))) proof (prove)
goal (1 subgoal):
 1. \<And>cap. cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap \<or> cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_frame_cap \<Longrightarrow> (cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap \<longrightarrow> SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSmallPage = (case cap_lift cap of Some (Cap_small_frame_cap c) \<Rightarrow> SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSmallPage | Some (Cap_frame_cap xa) \<Rightarrow> capFSize_CL xa | Some _ \<Rightarrow> 0)) \<and> (cap_get_tag cap \<noteq> SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap \<longrightarrow> (cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_frame_cap \<longrightarrow> capFSize_CL (cap_frame_cap_lift cap) = (case cap_lift cap of Some (Cap_small_frame_cap c) \<Rightarrow> SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSmallPage | Some (Cap_frame_cap xa) \<Rightarrow> capFSize_CL xa | Some _ \<Rightarrow> 0)) \<and> (cap_get_tag cap \<noteq> SCAST(32 signed \<rightarrow> 32) cap_frame_cap \<longrightarrow> (case cap_lift cap of Some (Cap_small_frame_cap c) \<Rightarrow> SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSmallPage | Some (Cap_frame_cap xa) \<Rightarrow> capFSize_CL xa | Some _ \<Rightarrow> 0) = 0)) proof (prove)
goal (3 subgoals):
 1. \<And>cap. \<lbrakk>cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap \<or> cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_frame_cap; cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap\<rbrakk> \<Longrightarrow> SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSmallPage = (case cap_lift cap of Some (Cap_small_frame_cap c) \<Rightarrow> SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSmallPage | Some (Cap_frame_cap xa) \<Rightarrow> capFSize_CL xa | Some _ \<Rightarrow> 0)
 2. \<And>cap. \<lbrakk>cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap \<or> cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_frame_cap; cap_get_tag cap \<noteq> SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap; cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_frame_cap\<rbrakk> \<Longrightarrow> capFSize_CL (cap_frame_cap_lift cap) = (case cap_lift cap of Some (Cap_small_frame_cap c) \<Rightarrow> SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSmallPage | Some (Cap_frame_cap xa) \<Rightarrow> capFSize_CL xa | Some _ \<Rightarrow> 0)
 3. \<And>cap. \<lbrakk>cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap \<or> cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_frame_cap; cap_get_tag cap \<noteq> SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap; cap_get_tag cap \<noteq> SCAST(32 signed \<rightarrow> 32) cap_frame_cap\<rbrakk> \<Longrightarrow> (case cap_lift cap of Some (Cap_small_frame_cap c) \<Rightarrow> SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSmallPage | Some (Cap_frame_cap xa) \<Rightarrow> capFSize_CL xa | Some _ \<Rightarrow> 0) = 0 proof (prove)
goal (2 subgoals):
 1. \<And>cap. \<lbrakk>cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap \<or> cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_frame_cap; cap_get_tag cap \<noteq> SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap; cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_frame_cap\<rbrakk> \<Longrightarrow> capFSize_CL (cap_frame_cap_lift cap) = (case cap_lift cap of Some (Cap_small_frame_cap c) \<Rightarrow> SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSmallPage | Some (Cap_frame_cap xa) \<Rightarrow> capFSize_CL xa | Some _ \<Rightarrow> 0)
 2. \<And>cap. \<lbrakk>cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap \<or> cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_frame_cap; cap_get_tag cap \<noteq> SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap; cap_get_tag cap \<noteq> SCAST(32 signed \<rightarrow> 32) cap_frame_cap\<rbrakk> \<Longrightarrow> (case cap_lift cap of Some (Cap_small_frame_cap c) \<Rightarrow> SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSmallPage | Some (Cap_frame_cap xa) \<Rightarrow> capFSize_CL xa | Some _ \<Rightarrow> 0) = 0 proof (prove)
goal (1 subgoal):
 1. \<And>cap. \<lbrakk>cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap \<or> cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_frame_cap; cap_get_tag cap \<noteq> SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap; cap_get_tag cap \<noteq> SCAST(32 signed \<rightarrow> 32) cap_frame_cap\<rbrakk> \<Longrightarrow> (case cap_lift cap of Some (Cap_small_frame_cap c) \<Rightarrow> SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSmallPage | Some (Cap_frame_cap xa) \<Rightarrow> capFSize_CL xa | Some _ \<Rightarrow> 0) = 0 proof (prove)
goal:
No subgoals!