theory structures_proofs

lemma (in kernel_all_substitute) pte_pte_small_new_spec:
  "\<forall>s. \<Gamma> \<turnstile> {s}
       \<acute>ret__struct_pte_C :== PROC pte_pte_small_new(\<acute>address, \<acute>nG, \<acute>S, \<acute>APX, \<acute>TEX, \<acute>AP, \<acute>C, \<acute>B, \<acute>XN)
       \<lbrace>pte_pte_small_lift \<acute>ret__struct_pte_C = \<lparr>
          pte_pte_small_CL.address_CL = (\<^bsup>s\<^esup>address___unsigned AND NOT (mask 12)),
          pte_pte_small_CL.nG_CL = (\<^bsup>s\<^esup>nG___unsigned AND mask 1),
          pte_pte_small_CL.S_CL = (\<^bsup>s\<^esup>S___unsigned AND mask 1),
          pte_pte_small_CL.APX_CL = (\<^bsup>s\<^esup>APX___unsigned AND mask 1),
          pte_pte_small_CL.TEX_CL = (\<^bsup>s\<^esup>TEX___unsigned AND mask 3),
          pte_pte_small_CL.AP_CL = (\<^bsup>s\<^esup>AP___unsigned AND mask 2),
          pte_pte_small_CL.C_CL = (\<^bsup>s\<^esup>C___unsigned AND mask 1),
          pte_pte_small_CL.B_CL = (\<^bsup>s\<^esup>B___unsigned AND mask 1),
          pte_pte_small_CL.XN_CL = (\<^bsup>s\<^esup>XN___unsigned AND mask 1) \<rparr> \<and>
        pte_get_tag \<acute>ret__struct_pte_C = scast pte_pte_small\<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_small_def
                         mask_def shift_over_ao_dists word_bw_assocs word_ao_dist) apply (simp add: pte_pte_small_lift_def) apply (erule pte_lift_pte_small[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_small_def))? done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>s. \<Gamma>\<turnstile> {s} Call pte_pte_small_new_'proc \<lbrace>pte_pte_small_lift \<acute>ret__struct_pte_C = \<lparr>pte_pte_small_CL.address_CL = \<^bsup>s\<^esup>address && ~~ mask 12, nG_CL = \<^bsup>s\<^esup>nG && mask 1, S_CL = \<^bsup>s\<^esup>S && mask 1, APX_CL = \<^bsup>s\<^esup>APX && mask 1, TEX_CL = \<^bsup>s\<^esup>TEX && mask 3, AP_CL = \<^bsup>s\<^esup>AP && mask 2, C_CL = \<^bsup>s\<^esup>C && mask 1, B_CL = \<^bsup>s\<^esup>B && mask 1, XN_CL = \<^bsup>s\<^esup>XN && mask 1\<rparr> \<and> pte_get_tag \<acute>ret__struct_pte_C = SCAST(32 signed \<rightarrow> 32) pte_pte_small\<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 6 \<and> 6 <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 0 \<and> 0 <s 0x20 \<and> pte_pte_small_lift (pte_C.words_C_update (\<lambda>v. Arrays.update v (unat 0) ((((((((((SCAST(32 signed \<rightarrow> 32) 0 || (\<acute>address && 0xFFFFF000 >> unat 0)) || (\<acute>nG && 1 << unat 0xB)) || (\<acute>S && 1 << unat 0xA)) || (\<acute>APX && 1 << unat 9)) || (\<acute>TEX && 7 << unat 6)) || (\<acute>AP && 3 << unat 4)) || (\<acute>C && 1 << unat 3)) || (\<acute>B && 1 << unat 2)) || (SCAST(32 signed \<rightarrow> 32) pte_pte_small && 1 << unat 1)) || (\<acute>XN && 1 << unat 0))) v) = \<lparr>pte_pte_small_CL.address_CL = \<^bsup>s\<^esup>address && ~~ mask 12, nG_CL = \<^bsup>s\<^esup>nG && mask 1, S_CL = \<^bsup>s\<^esup>S && mask 1, APX_CL = \<^bsup>s\<^esup>APX && mask 1, TEX_CL = \<^bsup>s\<^esup>TEX && mask 3, AP_CL = \<^bsup>s\<^esup>AP && mask 2, C_CL = \<^bsup>s\<^esup>C && mask 1, B_CL = \<^bsup>s\<^esup>B && mask 1, XN_CL = \<^bsup>s\<^esup>XN && 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 && 0xFFFFF000 >> unat 0)) || (\<acute>nG && 1 << unat 0xB)) || (\<acute>S && 1 << unat 0xA)) || (\<acute>APX && 1 << unat 9)) || (\<acute>TEX && 7 << unat 6)) || (\<acute>AP && 3 << unat 4)) || (\<acute>C && 1 << unat 3)) || (\<acute>B && 1 << unat 2)) || (SCAST(32 signed \<rightarrow> 32) pte_pte_small && 1 << unat 1)) || (\<acute>XN && 1 << unat 0))) v) = SCAST(32 signed \<rightarrow> 32) pte_pte_small\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s v. pte_pte_small_lift (pte_C.words_C_update (\<lambda>v. Arrays.update v 0 (((((((((address_' s && 0xFFFFF000 || (nG_' s << 11) && 0x800) || (S_' s << 10) && 0x400) || (APX_' s << 9) && 0x200) || (TEX_' s << 6) && 0x1C0) || (AP_' s << 4) && 0x30) || (C_' s << 3) && 8) || (B_' s << 2) && 4) || (SCAST(32 signed \<rightarrow> 32) pte_pte_small << Suc 0) && 2) || XN_' s && 1)) v) = \<lparr>pte_pte_small_CL.address_CL = address_' s && 0xFFFFF000, nG_CL = nG_' s && 1, S_CL = S_' s && 1, APX_CL = APX_' s && 1, TEX_CL = TEX_' s && 7, AP_CL = AP_' s && 3, C_CL = C_' s && 1, B_CL = B_' s && 1, XN_CL = XN_' s && 1\<rparr> \<and> pte_get_tag (pte_C.words_C_update (\<lambda>v. Arrays.update v 0 (((((((((address_' s && 0xFFFFF000 || (nG_' s << 11) && 0x800) || (S_' s << 10) && 0x400) || (APX_' s << 9) && 0x200) || (TEX_' s << 6) && 0x1C0) || (AP_' s << 4) && 0x30) || (C_' s << 3) && 8) || (B_' s << 2) && 4) || (SCAST(32 signed \<rightarrow> 32) pte_pte_small << Suc 0) && 2) || XN_' s && 1)) v) = SCAST(32 signed \<rightarrow> 32) pte_pte_small 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 && 0xFFFFF000 || (nG_' s << 11) && 0x800) || (S_' s << 10) && 0x400) || (APX_' s << 9) && 0x200) || (TEX_' s << 6) && 0x1C0) || (AP_' s << 4) && 0x30) || (C_' s << 3) && 8) || (B_' s << 2) && 4) || (SCAST(32 signed \<rightarrow> 32) pte_pte_small << Suc 0) && 2) || XN_' s && 1)) v) = SCAST(32 signed \<rightarrow> 32) pte_pte_small \<Longrightarrow> pte_pte_small_lift (pte_C.words_C_update (\<lambda>v. Arrays.update v 0 (((((((((address_' s && 0xFFFFF000 || (nG_' s << 11) && 0x800) || (S_' s << 10) && 0x400) || (APX_' s << 9) && 0x200) || (TEX_' s << 6) && 0x1C0) || (AP_' s << 4) && 0x30) || (C_' s << 3) && 8) || (B_' s << 2) && 4) || (SCAST(32 signed \<rightarrow> 32) pte_pte_small << Suc 0) && 2) || XN_' s && 1)) v) = \<lparr>pte_pte_small_CL.address_CL = address_' s && 0xFFFFF000, nG_CL = nG_' s && 1, S_CL = S_' s && 1, APX_CL = APX_' s && 1, TEX_CL = TEX_' s && 7, AP_CL = AP_' s && 3, C_CL = C_' s && 1, B_CL = B_' s && 1, XN_CL = XN_' 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 && 0xFFFFF000 || (nG_' s << 11) && 0x800) || (S_' s << 10) && 0x400) || (APX_' s << 9) && 0x200) || (TEX_' s << 6) && 0x1C0) || (AP_' s << 4) && 0x30) || (C_' s << 3) && 8) || (B_' s << 2) && 4) || (SCAST(32 signed \<rightarrow> 32) pte_pte_small << Suc 0) && 2) || XN_' s && 1)) v) = SCAST(32 signed \<rightarrow> 32) pte_pte_small \<Longrightarrow> (case pte_lift (pte_C.words_C_update (\<lambda>v. Arrays.update v 0 (((((((((address_' s && 0xFFFFF000 || (nG_' s << 11) && 0x800) || (S_' s << 10) && 0x400) || (APX_' s << 9) && 0x200) || (TEX_' s << 6) && 0x1C0) || (AP_' s << 4) && 0x30) || (C_' s << 3) && 8) || (B_' s << 2) && 4) || (SCAST(32 signed \<rightarrow> 32) pte_pte_small << Suc 0) && 2) || XN_' s && 1)) v) of Some (Pte_pte_small rec) \<Rightarrow> rec) = \<lparr>pte_pte_small_CL.address_CL = address_' s && 0xFFFFF000, nG_CL = nG_' s && 1, S_CL = S_' s && 1, APX_CL = APX_' s && 1, TEX_CL = TEX_' s && 7, AP_CL = AP_' s && 3, C_CL = C_' s && 1, B_CL = B_' s && 1, XN_CL = XN_' s && 1\<rparr> proof (prove)
goal (1 subgoal):
 1. \<And>s. (((((((((address_' s && 0xFFFFF000 || (nG_' s << 11) && 0x800) || (S_' s << 10) && 0x400) || (APX_' s << 9) && 0x200) || (TEX_' s << 6) && 0x1C0) || (AP_' s << 4) && 0x30) || (C_' s << 3) && 8) || (B_' s << 2) && 4) || (SCAST(32 signed \<rightarrow> 32) pte_pte_small << Suc 0) && 2) || XN_' s && 1) && ~~ mask 12 = address_' s && 0xFFFFF000 \<and> (((((((((address_' s && 0xFFFFF000 || (nG_' s << 11) && 0x800) || (S_' s << 10) && 0x400) || (APX_' s << 9) && 0x200) || (TEX_' s << 6) && 0x1C0) || (AP_' s << 4) && 0x30) || (C_' s << 3) && 8) || (B_' s << 2) && 4) || (SCAST(32 signed \<rightarrow> 32) pte_pte_small << Suc 0) && 2) || XN_' s && 1 >> 11) && 1 = nG_' s && 1 \<and> (((((((((address_' s && 0xFFFFF000 || (nG_' s << 11) && 0x800) || (S_' s << 10) && 0x400) || (APX_' s << 9) && 0x200) || (TEX_' s << 6) && 0x1C0) || (AP_' s << 4) && 0x30) || (C_' s << 3) && 8) || (B_' s << 2) && 4) || (SCAST(32 signed \<rightarrow> 32) pte_pte_small << Suc 0) && 2) || XN_' s && 1 >> 10) && 1 = S_' s && 1 \<and> (((((((((address_' s && 0xFFFFF000 || (nG_' s << 11) && 0x800) || (S_' s << 10) && 0x400) || (APX_' s << 9) && 0x200) || (TEX_' s << 6) && 0x1C0) || (AP_' s << 4) && 0x30) || (C_' s << 3) && 8) || (B_' s << 2) && 4) || (SCAST(32 signed \<rightarrow> 32) pte_pte_small << Suc 0) && 2) || XN_' s && 1 >> 9) && 1 = APX_' s && 1 \<and> (((((((((address_' s && 0xFFFFF000 || (nG_' s << 11) && 0x800) || (S_' s << 10) && 0x400) || (APX_' s << 9) && 0x200) || (TEX_' s << 6) && 0x1C0) || (AP_' s << 4) && 0x30) || (C_' s << 3) && 8) || (B_' s << 2) && 4) || (SCAST(32 signed \<rightarrow> 32) pte_pte_small << Suc 0) && 2) || XN_' s && 1 >> 6) && mask 3 = TEX_' s && 7 \<and> (((((((((address_' s && 0xFFFFF000 || (nG_' s << 11) && 0x800) || (S_' s << 10) && 0x400) || (APX_' s << 9) && 0x200) || (TEX_' s << 6) && 0x1C0) || (AP_' s << 4) && 0x30) || (C_' s << 3) && 8) || (B_' s << 2) && 4) || (SCAST(32 signed \<rightarrow> 32) pte_pte_small << Suc 0) && 2) || XN_' s && 1 >> 4) && mask 2 = AP_' s && 3 \<and> (((((((((address_' s && 0xFFFFF000 || (nG_' s << 11) && 0x800) || (S_' s << 10) && 0x400) || (APX_' s << 9) && 0x200) || (TEX_' s << 6) && 0x1C0) || (AP_' s << 4) && 0x30) || (C_' s << 3) && 8) || (B_' s << 2) && 4) || (SCAST(32 signed \<rightarrow> 32) pte_pte_small << Suc 0) && 2) || XN_' s && 1 >> 3) && 1 = C_' s && 1 \<and> (((((((((address_' s && 0xFFFFF000 || (nG_' s << 11) && 0x800) || (S_' s << 10) && 0x400) || (APX_' s << 9) && 0x200) || (TEX_' s << 6) && 0x1C0) || (AP_' s << 4) && 0x30) || (C_' s << 3) && 8) || (B_' s << 2) && 4) || (SCAST(32 signed \<rightarrow> 32) pte_pte_small << Suc 0) && 2) || XN_' s && 1 >> 2) && 1 = B_' s && 1 \<and> (((((((((address_' s && 0xFFFFF000 || (nG_' s << 11) && 0x800) || (S_' s << 10) && 0x400) || (APX_' s << 9) && 0x200) || (TEX_' s << 6) && 0x1C0) || (AP_' s << 4) && 0x30) || (C_' s << 3) && 8) || (B_' s << 2) && 4) || (SCAST(32 signed \<rightarrow> 32) pte_pte_small << Suc 0) && 2) || XN_' s && 1) && 1 = XN_' s && 1 proof (prove)
goal:
No subgoals!