theory VSpace_C

lemma generic_frame_cap_get_capFMappedASID_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>
       Call generic_frame_cap_get_capFMappedASID_'proc
       \<lbrace>\<acute>ret__unsigned_long = generic_frame_cap_get_capFMappedASID_CL (cap_lift \<^bsup>s\<^esup>cap)\<rbrace>" apply vcg apply (clarsimp simp: generic_frame_cap_get_capFMappedASID_CL_def  Kernel_C.asidLowBits_def word_sle_def ) apply (intro conjI impI, simp_all) 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) 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_capFMappedASID_'proc \<lbrace>\<acute>ret__unsigned_long = generic_frame_cap_get_capFMappedASID_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> (UCAST(32 \<rightarrow> 32 signed) (cap_get_tag cap) = cap_small_frame_cap \<longrightarrow> cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap \<and> (\<forall>ret__unsigned_long. ret__unsigned_long = (cap_small_frame_cap_CL.capFMappedASIDHigh_CL (cap_small_frame_cap_lift cap) << local.asidLowBits) + cap_small_frame_cap_CL.capFMappedASIDLow_CL (cap_small_frame_cap_lift cap) \<longrightarrow> (cap_small_frame_cap_CL.capFMappedASIDHigh_CL (cap_small_frame_cap_lift cap) << local.asidLowBits) + cap_small_frame_cap_CL.capFMappedASIDLow_CL (cap_small_frame_cap_lift cap) = generic_frame_cap_get_capFMappedASID_CL (cap_lift cap))) \<and> (UCAST(32 \<rightarrow> 32 signed) (cap_get_tag cap) \<noteq> cap_small_frame_cap \<longrightarrow> cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_frame_cap \<and> (\<forall>ret__unsigned_long. ret__unsigned_long = (cap_frame_cap_CL.capFMappedASIDHigh_CL (cap_frame_cap_lift cap) << local.asidLowBits) + cap_frame_cap_CL.capFMappedASIDLow_CL (cap_frame_cap_lift cap) \<longrightarrow> (cap_frame_cap_CL.capFMappedASIDHigh_CL (cap_frame_cap_lift cap) << local.asidLowBits) + cap_frame_cap_CL.capFMappedASIDLow_CL (cap_frame_cap_lift cap) = generic_frame_cap_get_capFMappedASID_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> (cap_small_frame_cap_CL.capFMappedASIDHigh_CL (cap_small_frame_cap_lift cap) << local.asid_low_bits) + cap_small_frame_cap_CL.capFMappedASIDLow_CL (cap_small_frame_cap_lift cap) = (case cap_lift cap of Some (Cap_small_frame_cap c) \<Rightarrow> (cap_small_frame_cap_CL.capFMappedASIDHigh_CL c << local.asidLowBits) + cap_small_frame_cap_CL.capFMappedASIDLow_CL c | Some (Cap_frame_cap c) \<Rightarrow> (cap_frame_cap_CL.capFMappedASIDHigh_CL c << local.asidLowBits) + cap_frame_cap_CL.capFMappedASIDLow_CL c | 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 \<and> (cap_frame_cap_CL.capFMappedASIDHigh_CL (cap_frame_cap_lift cap) << local.asid_low_bits) + cap_frame_cap_CL.capFMappedASIDLow_CL (cap_frame_cap_lift cap) = (case cap_lift cap of Some (Cap_small_frame_cap c) \<Rightarrow> (cap_small_frame_cap_CL.capFMappedASIDHigh_CL c << local.asidLowBits) + cap_small_frame_cap_CL.capFMappedASIDLow_CL c | Some (Cap_frame_cap c) \<Rightarrow> (cap_frame_cap_CL.capFMappedASIDHigh_CL c << local.asidLowBits) + cap_frame_cap_CL.capFMappedASIDLow_CL c | Some _ \<Rightarrow> 0)) proof (prove)
goal (2 subgoals):
 1. \<And>cap. cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap \<Longrightarrow> (cap_small_frame_cap_CL.capFMappedASIDHigh_CL (cap_small_frame_cap_lift cap) << local.asid_low_bits) + cap_small_frame_cap_CL.capFMappedASIDLow_CL (cap_small_frame_cap_lift cap) = (case cap_lift cap of Some (Cap_small_frame_cap c) \<Rightarrow> (cap_small_frame_cap_CL.capFMappedASIDHigh_CL c << local.asidLowBits) + cap_small_frame_cap_CL.capFMappedASIDLow_CL c | Some (Cap_frame_cap c) \<Rightarrow> (cap_frame_cap_CL.capFMappedASIDHigh_CL c << local.asidLowBits) + cap_frame_cap_CL.capFMappedASIDLow_CL c | Some _ \<Rightarrow> 0)
 2. \<And>cap. \<lbrakk>cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_frame_cap; cap_frame_cap \<noteq> cap_small_frame_cap\<rbrakk> \<Longrightarrow> (cap_frame_cap_CL.capFMappedASIDHigh_CL (cap_frame_cap_lift cap) << local.asid_low_bits) + cap_frame_cap_CL.capFMappedASIDLow_CL (cap_frame_cap_lift cap) = (case cap_lift cap of Some (Cap_small_frame_cap c) \<Rightarrow> (cap_small_frame_cap_CL.capFMappedASIDHigh_CL c << local.asidLowBits) + cap_small_frame_cap_CL.capFMappedASIDLow_CL c | Some (Cap_frame_cap c) \<Rightarrow> (cap_frame_cap_CL.capFMappedASIDHigh_CL c << local.asidLowBits) + cap_frame_cap_CL.capFMappedASIDLow_CL c | Some _ \<Rightarrow> 0) proof (prove)
goal (1 subgoal):
 1. \<And>cap. \<lbrakk>cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_frame_cap; cap_frame_cap \<noteq> cap_small_frame_cap\<rbrakk> \<Longrightarrow> (cap_frame_cap_CL.capFMappedASIDHigh_CL (cap_frame_cap_lift cap) << local.asid_low_bits) + cap_frame_cap_CL.capFMappedASIDLow_CL (cap_frame_cap_lift cap) = (case cap_lift cap of Some (Cap_small_frame_cap c) \<Rightarrow> (cap_small_frame_cap_CL.capFMappedASIDHigh_CL c << local.asidLowBits) + cap_small_frame_cap_CL.capFMappedASIDLow_CL c | Some (Cap_frame_cap c) \<Rightarrow> (cap_frame_cap_CL.capFMappedASIDHigh_CL c << local.asidLowBits) + cap_frame_cap_CL.capFMappedASIDLow_CL c | Some _ \<Rightarrow> 0) proof (prove)
goal:
No subgoals!