theory structures_proofs

lemma (in kernel_all_substitute) pte_pte_large_get_reserved_spec:
  "\<forall>s. \<Gamma> \<turnstile> \<lbrace>s. pte_get_tag \<acute>pte = scast pte_pte_large\<rbrace>
       \<acute>ret__unsigned :== PROC pte_pte_large_get_reserved(\<acute>pte)
       \<lbrace>\<acute>ret__unsigned = pte_pte_large_CL.reserved_CL (pte_pte_large_lift \<^bsup>s\<^esup>pte)\<rbrace>" apply(rule allI, rule conseqPre, vcg) apply (clarsimp simp:guard_simps) apply (simp add:pte_pte_large_lift_def) apply (subst pte_lift_pte_large) apply (simp add: o_def
                    pte_get_tag_def
                    pte_pte_large_def
                    mask_def word_size shift_over_ao_dists) apply (subst pte_lift_pte_large, simp)? apply (simp add: o_def
                   pte_get_tag_def
                   pte_pte_large_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. pte_get_tag \<acute>pte = SCAST(32 signed \<rightarrow> 32) pte_pte_large\<rbrace> Call pte_pte_large_get_reserved_'proc \<lbrace>\<acute>ret__unsigned = reserved_CL (pte_pte_large_lift \<^bsup>s\<^esup>pte)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrace>s. pte_get_tag \<acute>pte = SCAST(32 signed \<rightarrow> 32) pte_pte_large\<rbrace> \<subseteq> \<lbrace>\<forall>v. 0 \<le>s 0 \<and> 0 <s 0x20 \<and> 0 <s 1 \<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 (pte_C.words_C \<acute>pte.[unat 0] && 1 >> unat 0) && (1 << unat 0x1F) \<noteq> 0 then 1 else 0) \<noteq> 0 \<longrightarrow> (pte_C.words_C \<acute>pte.[unat 0] && 1 >> unat 0) || SCAST(32 signed \<rightarrow> 32) 0 = reserved_CL (pte_pte_large_lift \<^bsup>s\<^esup>pte)) \<and> ((if (pte_C.words_C \<acute>pte.[unat 0] && 1 >> unat 0) && (1 << unat 0x1F) \<noteq> 0 then 1 else 0) = 0 \<longrightarrow> pte_C.words_C \<acute>pte.[unat 0] && 1 >> unat 0 = reserved_CL (pte_pte_large_lift \<^bsup>s\<^esup>pte))) \<and> ((if False then 1 else 0) = 0 \<longrightarrow> pte_C.words_C \<acute>pte.[unat 0] && 1 >> unat 0 = reserved_CL (pte_pte_large_lift \<^bsup>s\<^esup>pte))\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x. pte_get_tag (pte_' x) = SCAST(32 signed \<rightarrow> 32) pte_pte_large \<Longrightarrow> pte_C.words_C (pte_' x).[0] && 1 = reserved_CL (pte_pte_large_lift (pte_' x)) proof (prove)
goal (1 subgoal):
 1. \<And>x. pte_get_tag (pte_' x) = SCAST(32 signed \<rightarrow> 32) pte_pte_large \<Longrightarrow> pte_C.words_C (pte_' x).[0] && 1 = reserved_CL (case pte_lift (pte_' x) of Some (Pte_pte_large rec) \<Rightarrow> rec) proof (prove)
goal (2 subgoals):
 1. \<And>x. pte_get_tag (pte_' x) = SCAST(32 signed \<rightarrow> 32) pte_pte_large \<Longrightarrow> pte_get_tag (pte_' x) = SCAST(32 signed \<rightarrow> 32) pte_pte_large
 2. \<And>x. pte_get_tag (pte_' x) = SCAST(32 signed \<rightarrow> 32) pte_pte_large \<Longrightarrow> pte_C.words_C (pte_' x).[0] && 1 = reserved_CL (case Some (Pte_pte_large \<lparr>pte_pte_large_CL.address_CL = (pte_C.words_C (pte_' x).[0] << 0) && ~~ mask 16, XN_CL = (pte_C.words_C (pte_' x).[0] >> 15) && mask 1, TEX_CL = (pte_C.words_C (pte_' x).[0] >> 12) && mask 3, nG_CL = (pte_C.words_C (pte_' x).[0] >> 11) && mask 1, S_CL = (pte_C.words_C (pte_' x).[0] >> 10) && mask 1, APX_CL = (pte_C.words_C (pte_' x).[0] >> 9) && mask 1, AP_CL = (pte_C.words_C (pte_' x).[0] >> 4) && mask 2, C_CL = (pte_C.words_C (pte_' x).[0] >> 3) && mask 1, B_CL = (pte_C.words_C (pte_' x).[0] >> 2) && mask 1, reserved_CL = (pte_C.words_C (pte_' x).[0] >> 0) && mask 1\<rparr>) of Some (Pte_pte_large rec) \<Rightarrow> rec) proof (prove)
goal (1 subgoal):
 1. \<And>x. pte_get_tag (pte_' x) = SCAST(32 signed \<rightarrow> 32) pte_pte_large \<Longrightarrow> pte_C.words_C (pte_' x).[0] && 1 = reserved_CL (case Some (Pte_pte_large \<lparr>pte_pte_large_CL.address_CL = (pte_C.words_C (pte_' x).[0] << 0) && ~~ mask 16, XN_CL = (pte_C.words_C (pte_' x).[0] >> 15) && mask 1, TEX_CL = (pte_C.words_C (pte_' x).[0] >> 12) && mask 3, nG_CL = (pte_C.words_C (pte_' x).[0] >> 11) && mask 1, S_CL = (pte_C.words_C (pte_' x).[0] >> 10) && mask 1, APX_CL = (pte_C.words_C (pte_' x).[0] >> 9) && mask 1, AP_CL = (pte_C.words_C (pte_' x).[0] >> 4) && mask 2, C_CL = (pte_C.words_C (pte_' x).[0] >> 3) && mask 1, B_CL = (pte_C.words_C (pte_' x).[0] >> 2) && mask 1, reserved_CL = (pte_C.words_C (pte_' x).[0] >> 0) && mask 1\<rparr>) of Some (Pte_pte_large rec) \<Rightarrow> rec) proof (prove)
goal (1 subgoal):
 1. \<And>x. pte_get_tag (pte_' x) = SCAST(32 signed \<rightarrow> 32) pte_pte_large \<Longrightarrow> pte_C.words_C (pte_' x).[0] && 1 = reserved_CL (case Some (Pte_pte_large \<lparr>pte_pte_large_CL.address_CL = (pte_C.words_C (pte_' x).[0] << 0) && ~~ mask 16, XN_CL = (pte_C.words_C (pte_' x).[0] >> 15) && mask 1, TEX_CL = (pte_C.words_C (pte_' x).[0] >> 12) && mask 3, nG_CL = (pte_C.words_C (pte_' x).[0] >> 11) && mask 1, S_CL = (pte_C.words_C (pte_' x).[0] >> 10) && mask 1, APX_CL = (pte_C.words_C (pte_' x).[0] >> 9) && mask 1, AP_CL = (pte_C.words_C (pte_' x).[0] >> 4) && mask 2, C_CL = (pte_C.words_C (pte_' x).[0] >> 3) && mask 1, B_CL = (pte_C.words_C (pte_' x).[0] >> 2) && mask 1, reserved_CL = (pte_C.words_C (pte_' x).[0] >> 0) && mask 1\<rparr>) of Some (Pte_pte_large rec) \<Rightarrow> rec) proof (prove)
goal:
No subgoals!