theory structures_proofs

lemma (in kernel_all_substitute) cap_small_frame_cap_get_capFBasePtr_spec:
  "\<forall>s. \<Gamma> \<turnstile> \<lbrace>s. cap_get_tag \<acute>cap = scast cap_small_frame_cap\<rbrace>
       \<acute>ret__unsigned :== PROC cap_small_frame_cap_get_capFBasePtr(\<acute>cap)
       \<lbrace>\<acute>ret__unsigned = cap_small_frame_cap_CL.capFBasePtr_CL (cap_small_frame_cap_lift \<^bsup>s\<^esup>cap)\<rbrace>" apply(rule allI, rule conseqPre, vcg) apply (clarsimp simp:guard_simps) apply (simp add:cap_small_frame_cap_lift_def) apply (subst cap_lift_small_frame_cap) apply (simp add: o_def
                    cap_get_tag_def
                    cap_small_frame_cap_def
                    mask_def word_size shift_over_ao_dists) apply (subst cap_lift_small_frame_cap, simp)? apply (simp add: o_def
                   cap_get_tag_def
                   cap_small_frame_cap_def
                   mask_def word_size shift_over_ao_dists multi_shift_simps
                   word_bw_assocs word_oa_dist word_and_max_simps ucast_def
                   sign_extend_def' nth_is_and_neq_0) 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\<rbrace> Call cap_small_frame_cap_get_capFBasePtr_'proc \<lbrace>\<acute>ret__unsigned = cap_small_frame_cap_CL.capFBasePtr_CL (cap_small_frame_cap_lift \<^bsup>s\<^esup>cap)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrace>s. cap_get_tag \<acute>cap = SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap\<rbrace> \<subseteq> \<lbrace>\<forall>v. 0 \<le>s 8 \<and> 8 <s 0x20 \<and> 0 <s 2 \<and> 0 \<le>s 0 \<and> ((if False then 1 else 0) \<noteq> 0 \<longrightarrow> 0 \<le>s 0x1F \<and> 0x1F <s 0x20 \<and> ((if (cap_C.words_C \<acute>cap.[unat 0] && 0xFFFFF0 << unat 8) && (1 << unat 0x1F) \<noteq> 0 then 1 else 0) \<noteq> 0 \<longrightarrow> (cap_C.words_C \<acute>cap.[unat 0] && 0xFFFFF0 << unat 8) || SCAST(32 signed \<rightarrow> 32) 0 = cap_small_frame_cap_CL.capFBasePtr_CL (cap_small_frame_cap_lift \<^bsup>s\<^esup>cap)) \<and> ((if (cap_C.words_C \<acute>cap.[unat 0] && 0xFFFFF0 << unat 8) && (1 << unat 0x1F) \<noteq> 0 then 1 else 0) = 0 \<longrightarrow> cap_C.words_C \<acute>cap.[unat 0] && 0xFFFFF0 << unat 8 = cap_small_frame_cap_CL.capFBasePtr_CL (cap_small_frame_cap_lift \<^bsup>s\<^esup>cap))) \<and> ((if False then 1 else 0) = 0 \<longrightarrow> cap_C.words_C \<acute>cap.[unat 0] && 0xFFFFF0 << unat 8 = cap_small_frame_cap_CL.capFBasePtr_CL (cap_small_frame_cap_lift \<^bsup>s\<^esup>cap))\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x. cap_get_tag (cap_' x) = SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap \<Longrightarrow> cap_C.words_C (cap_' x).[0] && 0xFFFFF0 << 8 = cap_small_frame_cap_CL.capFBasePtr_CL (cap_small_frame_cap_lift (cap_' x)) proof (prove)
goal (1 subgoal):
 1. \<And>x. cap_get_tag (cap_' x) = SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap \<Longrightarrow> cap_C.words_C (cap_' x).[0] && 0xFFFFF0 << 8 = cap_small_frame_cap_CL.capFBasePtr_CL (case cap_lift (cap_' x) of Some (Cap_small_frame_cap rec) \<Rightarrow> rec) proof (prove)
goal (2 subgoals):
 1. \<And>x. cap_get_tag (cap_' x) = SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap \<Longrightarrow> cap_get_tag (cap_' x) = SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap
 2. \<And>x. cap_get_tag (cap_' x) = SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap \<Longrightarrow> cap_C.words_C (cap_' x).[0] && 0xFFFFF0 << 8 = cap_small_frame_cap_CL.capFBasePtr_CL (case Some (Cap_small_frame_cap \<lparr>cap_small_frame_cap_CL.capFMappedASIDLow_CL = (cap_C.words_C (cap_' x).[1] >> 22) && mask 10, capFVMRights_CL = (cap_C.words_C (cap_' x).[1] >> 20) && mask 2, capFMappedAddress_CL = (cap_C.words_C (cap_' x).[1] << 12) && ~~ mask 12, capFIsDevice_CL = (cap_C.words_C (cap_' x).[0] >> 31) && mask 1, capFMappedASIDHigh_CL = (cap_C.words_C (cap_' x).[0] >> 24) && mask 7, capFBasePtr_CL = (cap_C.words_C (cap_' x).[0] << 8) && ~~ mask 12\<rparr>) of Some (Cap_small_frame_cap rec) \<Rightarrow> rec) proof (prove)
goal (1 subgoal):
 1. \<And>x. cap_get_tag (cap_' x) = SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap \<Longrightarrow> cap_C.words_C (cap_' x).[0] && 0xFFFFF0 << 8 = cap_small_frame_cap_CL.capFBasePtr_CL (case Some (Cap_small_frame_cap \<lparr>cap_small_frame_cap_CL.capFMappedASIDLow_CL = (cap_C.words_C (cap_' x).[1] >> 22) && mask 10, capFVMRights_CL = (cap_C.words_C (cap_' x).[1] >> 20) && mask 2, capFMappedAddress_CL = (cap_C.words_C (cap_' x).[1] << 12) && ~~ mask 12, capFIsDevice_CL = (cap_C.words_C (cap_' x).[0] >> 31) && mask 1, capFMappedASIDHigh_CL = (cap_C.words_C (cap_' x).[0] >> 24) && mask 7, capFBasePtr_CL = (cap_C.words_C (cap_' x).[0] << 8) && ~~ mask 12\<rparr>) of Some (Cap_small_frame_cap rec) \<Rightarrow> rec) proof (prove)
goal (1 subgoal):
 1. \<And>x. cap_get_tag (cap_' x) = SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap \<Longrightarrow> cap_C.words_C (cap_' x).[0] && 0xFFFFF0 << 8 = cap_small_frame_cap_CL.capFBasePtr_CL (case Some (Cap_small_frame_cap \<lparr>cap_small_frame_cap_CL.capFMappedASIDLow_CL = (cap_C.words_C (cap_' x).[1] >> 22) && mask 10, capFVMRights_CL = (cap_C.words_C (cap_' x).[1] >> 20) && mask 2, capFMappedAddress_CL = (cap_C.words_C (cap_' x).[1] << 12) && ~~ mask 12, capFIsDevice_CL = (cap_C.words_C (cap_' x).[0] >> 31) && mask 1, capFMappedASIDHigh_CL = (cap_C.words_C (cap_' x).[0] >> 24) && mask 7, capFBasePtr_CL = (cap_C.words_C (cap_' x).[0] << 8) && ~~ mask 12\<rparr>) of Some (Cap_small_frame_cap rec) \<Rightarrow> rec) proof (prove)
goal:
No subgoals!