theory structures_proofs

lemma (in kernel_all_substitute) pte_pte_large_new_spec:
  "\<forall>s. \<Gamma> \<turnstile> {s}
       \<acute>ret__struct_pte_C :== PROC pte_pte_large_new(\<acute>address, \<acute>XN, \<acute>TEX, \<acute>nG, \<acute>S, \<acute>APX, \<acute>AP, \<acute>C, \<acute>B, \<acute>reserved)
       \<lbrace>pte_pte_large_lift \<acute>ret__struct_pte_C = \<lparr>
          pte_pte_large_CL.address_CL = (\<^bsup>s\<^esup>address___unsigned AND NOT (mask 16)),
          pte_pte_large_CL.XN_CL = (\<^bsup>s\<^esup>XN___unsigned AND mask 1),
          pte_pte_large_CL.TEX_CL = (\<^bsup>s\<^esup>TEX___unsigned AND mask 3),
          pte_pte_large_CL.nG_CL = (\<^bsup>s\<^esup>nG___unsigned AND mask 1),
          pte_pte_large_CL.S_CL = (\<^bsup>s\<^esup>S___unsigned AND mask 1),
          pte_pte_large_CL.APX_CL = (\<^bsup>s\<^esup>APX___unsigned AND mask 1),
          pte_pte_large_CL.AP_CL = (\<^bsup>s\<^esup>AP___unsigned AND mask 2),
          pte_pte_large_CL.C_CL = (\<^bsup>s\<^esup>C___unsigned AND mask 1),
          pte_pte_large_CL.B_CL = (\<^bsup>s\<^esup>B___unsigned AND mask 1),
          pte_pte_large_CL.reserved_CL = (\<^bsup>s\<^esup>reserved___unsigned AND mask 1) \<rparr> \<and>
        pte_get_tag \<acute>ret__struct_pte_C = scast pte_pte_large\<rbrace>" apply (rule allI, rule conseqPre, vcg) apply (clarsimp simp: guard_simps o_def mask_def shift_over_ao_dists) apply (rule context_conjI[THEN iffD1[OF conj_commute]],
         fastforce simp: pte_get_tag_eq_x pte_pte_large_def
                         mask_def shift_over_ao_dists word_bw_assocs word_ao_dist) apply (simp add: pte_pte_large_lift_def) apply (erule pte_lift_pte_large[THEN subst[OF sym]]; simp?) apply ((intro conjI sign_extend_eq)?;
         (simp add: mask_def shift_over_ao_dists multi_shift_simps word_size
                    word_ao_dist word_bw_assocs word_and_max_simps pte_pte_large_def))? done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>s. \<Gamma>\<turnstile> {s} Call pte_pte_large_new_'proc \<lbrace>pte_pte_large_lift \<acute>ret__struct_pte_C = \<lparr>pte_pte_large_CL.address_CL = \<^bsup>s\<^esup>address && ~~ mask 16, XN_CL = \<^bsup>s\<^esup>XN && mask 1, TEX_CL = \<^bsup>s\<^esup>TEX && mask 3, nG_CL = \<^bsup>s\<^esup>nG && mask 1, S_CL = \<^bsup>s\<^esup>S && mask 1, APX_CL = \<^bsup>s\<^esup>APX && mask 1, AP_CL = \<^bsup>s\<^esup>AP && mask 2, C_CL = \<^bsup>s\<^esup>C && mask 1, B_CL = \<^bsup>s\<^esup>B && mask 1, reserved_CL = \<^bsup>s\<^esup>reserved && mask 1\<rparr> \<and> pte_get_tag \<acute>ret__struct_pte_C = SCAST(32 signed \<rightarrow> 32) pte_pte_large\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. {s} \<subseteq> \<lbrace>\<forall>v. 0 <s 1 \<and> 0 \<le>s 0 \<and> 0 <s 0x20 \<and> 0 \<le>s 1 \<and> 1 <s 0x20 \<and> 0 \<le>s 2 \<and> 2 <s 0x20 \<and> 0 \<le>s 3 \<and> 3 <s 0x20 \<and> 0 \<le>s 4 \<and> 4 <s 0x20 \<and> 0 \<le>s 9 \<and> 9 <s 0x20 \<and> 0 \<le>s 0xA \<and> 0xA <s 0x20 \<and> 0 \<le>s 0xB \<and> 0xB <s 0x20 \<and> 0 \<le>s 0xC \<and> 0xC <s 0x20 \<and> 0 \<le>s 0xF \<and> 0xF <s 0x20 \<and> 0 \<le>s 0 \<and> 0 <s 0x20 \<and> pte_pte_large_lift (pte_C.words_C_update (\<lambda>v. Arrays.update v (unat 0) (((((((((((SCAST(32 signed \<rightarrow> 32) 0 || (\<acute>address && 0xFFFF0000 >> unat 0)) || (\<acute>XN && 1 << unat 0xF)) || (\<acute>TEX && 7 << unat 0xC)) || (\<acute>nG && 1 << unat 0xB)) || (\<acute>S && 1 << unat 0xA)) || (\<acute>APX && 1 << unat 9)) || (\<acute>AP && 3 << unat 4)) || (\<acute>C && 1 << unat 3)) || (\<acute>B && 1 << unat 2)) || (SCAST(32 signed \<rightarrow> 32) pte_pte_large && 1 << unat 1)) || (\<acute>reserved && 1 << unat 0))) v) = \<lparr>pte_pte_large_CL.address_CL = \<^bsup>s\<^esup>address && ~~ mask 16, XN_CL = \<^bsup>s\<^esup>XN && mask 1, TEX_CL = \<^bsup>s\<^esup>TEX && mask 3, nG_CL = \<^bsup>s\<^esup>nG && mask 1, S_CL = \<^bsup>s\<^esup>S && mask 1, APX_CL = \<^bsup>s\<^esup>APX && mask 1, AP_CL = \<^bsup>s\<^esup>AP && mask 2, C_CL = \<^bsup>s\<^esup>C && mask 1, B_CL = \<^bsup>s\<^esup>B && mask 1, reserved_CL = \<^bsup>s\<^esup>reserved && mask 1\<rparr> \<and> pte_get_tag (pte_C.words_C_update (\<lambda>v. Arrays.update v (unat 0) (((((((((((SCAST(32 signed \<rightarrow> 32) 0 || (\<acute>address && 0xFFFF0000 >> unat 0)) || (\<acute>XN && 1 << unat 0xF)) || (\<acute>TEX && 7 << unat 0xC)) || (\<acute>nG && 1 << unat 0xB)) || (\<acute>S && 1 << unat 0xA)) || (\<acute>APX && 1 << unat 9)) || (\<acute>AP && 3 << unat 4)) || (\<acute>C && 1 << unat 3)) || (\<acute>B && 1 << unat 2)) || (SCAST(32 signed \<rightarrow> 32) pte_pte_large && 1 << unat 1)) || (\<acute>reserved && 1 << unat 0))) v) = SCAST(32 signed \<rightarrow> 32) pte_pte_large\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s v. pte_pte_large_lift (pte_C.words_C_update (\<lambda>v. Arrays.update v 0 ((((((((((address_' s && 0xFFFF0000 || (XN_' s << 15) && 0x8000) || (TEX_' s << 12) && 0x7000) || (nG_' s << 11) && 0x800) || (S_' s << 10) && 0x400) || (APX_' s << 9) && 0x200) || (AP_' s << 4) && 0x30) || (C_' s << 3) && 8) || (B_' s << 2) && 4) || (SCAST(32 signed \<rightarrow> 32) pte_pte_large << Suc 0) && 2) || reserved_' s && 1)) v) = \<lparr>pte_pte_large_CL.address_CL = address_' s && 0xFFFF0000, XN_CL = XN_' s && 1, TEX_CL = TEX_' s && 7, nG_CL = nG_' s && 1, S_CL = S_' s && 1, APX_CL = APX_' s && 1, AP_CL = AP_' s && 3, C_CL = C_' s && 1, B_CL = B_' s && 1, reserved_CL = reserved_' s && 1\<rparr> \<and> pte_get_tag (pte_C.words_C_update (\<lambda>v. Arrays.update v 0 ((((((((((address_' s && 0xFFFF0000 || (XN_' s << 15) && 0x8000) || (TEX_' s << 12) && 0x7000) || (nG_' s << 11) && 0x800) || (S_' s << 10) && 0x400) || (APX_' s << 9) && 0x200) || (AP_' s << 4) && 0x30) || (C_' s << 3) && 8) || (B_' s << 2) && 4) || (SCAST(32 signed \<rightarrow> 32) pte_pte_large << Suc 0) && 2) || reserved_' s && 1)) v) = SCAST(32 signed \<rightarrow> 32) pte_pte_large proof (prove)
goal (1 subgoal):
 1. \<And>s v. pte_get_tag (pte_C.words_C_update (\<lambda>v. Arrays.update v 0 ((((((((((address_' s && 0xFFFF0000 || (XN_' s << 15) && 0x8000) || (TEX_' s << 12) && 0x7000) || (nG_' s << 11) && 0x800) || (S_' s << 10) && 0x400) || (APX_' s << 9) && 0x200) || (AP_' s << 4) && 0x30) || (C_' s << 3) && 8) || (B_' s << 2) && 4) || (SCAST(32 signed \<rightarrow> 32) pte_pte_large << Suc 0) && 2) || reserved_' s && 1)) v) = SCAST(32 signed \<rightarrow> 32) pte_pte_large \<Longrightarrow> pte_pte_large_lift (pte_C.words_C_update (\<lambda>v. Arrays.update v 0 ((((((((((address_' s && 0xFFFF0000 || (XN_' s << 15) && 0x8000) || (TEX_' s << 12) && 0x7000) || (nG_' s << 11) && 0x800) || (S_' s << 10) && 0x400) || (APX_' s << 9) && 0x200) || (AP_' s << 4) && 0x30) || (C_' s << 3) && 8) || (B_' s << 2) && 4) || (SCAST(32 signed \<rightarrow> 32) pte_pte_large << Suc 0) && 2) || reserved_' s && 1)) v) = \<lparr>pte_pte_large_CL.address_CL = address_' s && 0xFFFF0000, XN_CL = XN_' s && 1, TEX_CL = TEX_' s && 7, nG_CL = nG_' s && 1, S_CL = S_' s && 1, APX_CL = APX_' s && 1, AP_CL = AP_' s && 3, C_CL = C_' s && 1, B_CL = B_' s && 1, reserved_CL = reserved_' s && 1\<rparr> proof (prove)
goal (1 subgoal):
 1. \<And>s v. pte_get_tag (pte_C.words_C_update (\<lambda>v. Arrays.update v 0 ((((((((((address_' s && 0xFFFF0000 || (XN_' s << 15) && 0x8000) || (TEX_' s << 12) && 0x7000) || (nG_' s << 11) && 0x800) || (S_' s << 10) && 0x400) || (APX_' s << 9) && 0x200) || (AP_' s << 4) && 0x30) || (C_' s << 3) && 8) || (B_' s << 2) && 4) || (SCAST(32 signed \<rightarrow> 32) pte_pte_large << Suc 0) && 2) || reserved_' s && 1)) v) = SCAST(32 signed \<rightarrow> 32) pte_pte_large \<Longrightarrow> (case pte_lift (pte_C.words_C_update (\<lambda>v. Arrays.update v 0 ((((((((((address_' s && 0xFFFF0000 || (XN_' s << 15) && 0x8000) || (TEX_' s << 12) && 0x7000) || (nG_' s << 11) && 0x800) || (S_' s << 10) && 0x400) || (APX_' s << 9) && 0x200) || (AP_' s << 4) && 0x30) || (C_' s << 3) && 8) || (B_' s << 2) && 4) || (SCAST(32 signed \<rightarrow> 32) pte_pte_large << Suc 0) && 2) || reserved_' s && 1)) v) of Some (Pte_pte_large rec) \<Rightarrow> rec) = \<lparr>pte_pte_large_CL.address_CL = address_' s && 0xFFFF0000, XN_CL = XN_' s && 1, TEX_CL = TEX_' s && 7, nG_CL = nG_' s && 1, S_CL = S_' s && 1, APX_CL = APX_' s && 1, AP_CL = AP_' s && 3, C_CL = C_' s && 1, B_CL = B_' s && 1, reserved_CL = reserved_' s && 1\<rparr> proof (prove)
goal (1 subgoal):
 1. \<And>s. ((((((((((address_' s && 0xFFFF0000 || (XN_' s << 15) && 0x8000) || (TEX_' s << 12) && 0x7000) || (nG_' s << 11) && 0x800) || (S_' s << 10) && 0x400) || (APX_' s << 9) && 0x200) || (AP_' s << 4) && 0x30) || (C_' s << 3) && 8) || (B_' s << 2) && 4) || (SCAST(32 signed \<rightarrow> 32) pte_pte_large << Suc 0) && 2) || reserved_' s && 1) && ~~ mask 16 = address_' s && 0xFFFF0000 \<and> ((((((((((address_' s && 0xFFFF0000 || (XN_' s << 15) && 0x8000) || (TEX_' s << 12) && 0x7000) || (nG_' s << 11) && 0x800) || (S_' s << 10) && 0x400) || (APX_' s << 9) && 0x200) || (AP_' s << 4) && 0x30) || (C_' s << 3) && 8) || (B_' s << 2) && 4) || (SCAST(32 signed \<rightarrow> 32) pte_pte_large << Suc 0) && 2) || reserved_' s && 1 >> 15) && 1 = XN_' s && 1 \<and> ((((((((((address_' s && 0xFFFF0000 || (XN_' s << 15) && 0x8000) || (TEX_' s << 12) && 0x7000) || (nG_' s << 11) && 0x800) || (S_' s << 10) && 0x400) || (APX_' s << 9) && 0x200) || (AP_' s << 4) && 0x30) || (C_' s << 3) && 8) || (B_' s << 2) && 4) || (SCAST(32 signed \<rightarrow> 32) pte_pte_large << Suc 0) && 2) || reserved_' s && 1 >> 12) && mask 3 = TEX_' s && 7 \<and> ((((((((((address_' s && 0xFFFF0000 || (XN_' s << 15) && 0x8000) || (TEX_' s << 12) && 0x7000) || (nG_' s << 11) && 0x800) || (S_' s << 10) && 0x400) || (APX_' s << 9) && 0x200) || (AP_' s << 4) && 0x30) || (C_' s << 3) && 8) || (B_' s << 2) && 4) || (SCAST(32 signed \<rightarrow> 32) pte_pte_large << Suc 0) && 2) || reserved_' s && 1 >> 11) && 1 = nG_' s && 1 \<and> ((((((((((address_' s && 0xFFFF0000 || (XN_' s << 15) && 0x8000) || (TEX_' s << 12) && 0x7000) || (nG_' s << 11) && 0x800) || (S_' s << 10) && 0x400) || (APX_' s << 9) && 0x200) || (AP_' s << 4) && 0x30) || (C_' s << 3) && 8) || (B_' s << 2) && 4) || (SCAST(32 signed \<rightarrow> 32) pte_pte_large << Suc 0) && 2) || reserved_' s && 1 >> 10) && 1 = S_' s && 1 \<and> ((((((((((address_' s && 0xFFFF0000 || (XN_' s << 15) && 0x8000) || (TEX_' s << 12) && 0x7000) || (nG_' s << 11) && 0x800) || (S_' s << 10) && 0x400) || (APX_' s << 9) && 0x200) || (AP_' s << 4) && 0x30) || (C_' s << 3) && 8) || (B_' s << 2) && 4) || (SCAST(32 signed \<rightarrow> 32) pte_pte_large << Suc 0) && 2) || reserved_' s && 1 >> 9) && 1 = APX_' s && 1 \<and> ((((((((((address_' s && 0xFFFF0000 || (XN_' s << 15) && 0x8000) || (TEX_' s << 12) && 0x7000) || (nG_' s << 11) && 0x800) || (S_' s << 10) && 0x400) || (APX_' s << 9) && 0x200) || (AP_' s << 4) && 0x30) || (C_' s << 3) && 8) || (B_' s << 2) && 4) || (SCAST(32 signed \<rightarrow> 32) pte_pte_large << Suc 0) && 2) || reserved_' s && 1 >> 4) && mask 2 = AP_' s && 3 \<and> ((((((((((address_' s && 0xFFFF0000 || (XN_' s << 15) && 0x8000) || (TEX_' s << 12) && 0x7000) || (nG_' s << 11) && 0x800) || (S_' s << 10) && 0x400) || (APX_' s << 9) && 0x200) || (AP_' s << 4) && 0x30) || (C_' s << 3) && 8) || (B_' s << 2) && 4) || (SCAST(32 signed \<rightarrow> 32) pte_pte_large << Suc 0) && 2) || reserved_' s && 1 >> 3) && 1 = C_' s && 1 \<and> ((((((((((address_' s && 0xFFFF0000 || (XN_' s << 15) && 0x8000) || (TEX_' s << 12) && 0x7000) || (nG_' s << 11) && 0x800) || (S_' s << 10) && 0x400) || (APX_' s << 9) && 0x200) || (AP_' s << 4) && 0x30) || (C_' s << 3) && 8) || (B_' s << 2) && 4) || (SCAST(32 signed \<rightarrow> 32) pte_pte_large << Suc 0) && 2) || reserved_' s && 1 >> 2) && 1 = B_' s && 1 \<and> ((((((((((address_' s && 0xFFFF0000 || (XN_' s << 15) && 0x8000) || (TEX_' s << 12) && 0x7000) || (nG_' s << 11) && 0x800) || (S_' s << 10) && 0x400) || (APX_' s << 9) && 0x200) || (AP_' s << 4) && 0x30) || (C_' s << 3) && 8) || (B_' s << 2) && 4) || (SCAST(32 signed \<rightarrow> 32) pte_pte_large << Suc 0) && 2) || reserved_' s && 1) && 1 = reserved_' s && 1 proof (prove)
goal:
No subgoals!