theory structures_proofs

lemma (in kernel_all_substitute) cap_frame_cap_set_capFMappedAddress_spec:
  "\<forall>s. \<Gamma> \<turnstile> \<lbrace>s. cap_get_tag \<acute>cap = scast cap_frame_cap\<rbrace>
       \<acute>ret__struct_cap_C :== PROC cap_frame_cap_set_capFMappedAddress(\<acute>cap, \<acute>v32)
       \<lbrace>cap_frame_cap_lift \<acute>ret__struct_cap_C = cap_frame_cap_lift \<^bsup>s\<^esup>cap \<lparr> cap_frame_cap_CL.capFMappedAddress_CL :=  (\<^bsup>s\<^esup>v32 AND NOT (mask 14))\<rparr> \<and>
        cap_get_tag \<acute>ret__struct_cap_C = scast cap_frame_cap\<rbrace>" apply (rule allI, rule conseqPre, vcg) apply clarsimp apply (rule context_conjI[THEN iffD1[OF conj_commute]],
         fastforce simp: cap_get_tag_eq_x cap_lift_def cap_tag_defs
                         mask_def shift_over_ao_dists multi_shift_simps word_size
                         word_ao_dist word_bw_assocs) apply (simp add: cap_frame_cap_lift_def cap_lift_def cap_tag_defs) 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))? 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_frame_cap\<rbrace> Call cap_frame_cap_set_capFMappedAddress_'proc \<lbrace>cap_frame_cap_lift \<acute>ret__struct_cap_C = cap_frame_cap_lift \<^bsup>s\<^esup>cap\<lparr>cap_frame_cap_CL.capFMappedAddress_CL := \<^bsup>s\<^esup>v32 && ~~ mask 14\<rparr> \<and> cap_get_tag \<acute>ret__struct_cap_C = SCAST(32 signed \<rightarrow> 32) cap_frame_cap\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrace>s. cap_get_tag \<acute>cap = SCAST(32 signed \<rightarrow> 32) cap_frame_cap\<rbrace> \<subseteq> \<lbrace>1 <s 2 \<and> 0 \<le>s 1 \<and> 1 <s 2 \<and> 0 \<le>s 1 \<and> 1 <s 2 \<and> 0 \<le>s 1 \<and> 0 \<le>s 0xE \<and> 0xE <s 0x20 \<and> 1 <s 2 \<and> 0 \<le>s 1 \<and> cap_frame_cap_lift (cap_C.words_C_update (\<lambda>v. Arrays.update v (unat 1) (v.[unat 1] || (\<acute>v32 >> unat 0xE) && 0x3FFFF)) (cap_C.words_C_update (\<lambda>v. Arrays.update v (unat 1) (v.[unat 1] && ~~ 0x3FFFF)) \<acute>cap)) = cap_frame_cap_lift \<^bsup>s\<^esup>cap\<lparr>cap_frame_cap_CL.capFMappedAddress_CL := \<^bsup>s\<^esup>v32 && ~~ mask 14\<rparr> \<and> cap_get_tag (cap_C.words_C_update (\<lambda>v. Arrays.update v (unat 1) (v.[unat 1] || (\<acute>v32 >> unat 0xE) && 0x3FFFF)) (cap_C.words_C_update (\<lambda>v. Arrays.update v (unat 1) (v.[unat 1] && ~~ 0x3FFFF)) \<acute>cap)) = SCAST(32 signed \<rightarrow> 32) cap_frame_cap\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x. cap_get_tag (cap_' x) = SCAST(32 signed \<rightarrow> 32) cap_frame_cap \<Longrightarrow> cap_frame_cap_lift (cap_C.words_C_update ((\<lambda>v. Arrays.update v (Suc 0) (v.[Suc 0] || (v32_' x >> 14) && 0x3FFFF)) \<circ> (\<lambda>v. Arrays.update v (Suc 0) (v.[Suc 0] && 0xFFFC0000))) (cap_' x)) = cap_frame_cap_lift (cap_' x)\<lparr>cap_frame_cap_CL.capFMappedAddress_CL := v32_' x && ~~ mask 14\<rparr> \<and> cap_get_tag (cap_C.words_C_update ((\<lambda>v. Arrays.update v (Suc 0) (v.[Suc 0] || (v32_' x >> 14) && 0x3FFFF)) \<circ> (\<lambda>v. Arrays.update v (Suc 0) (v.[Suc 0] && 0xFFFC0000))) (cap_' x)) = SCAST(32 signed \<rightarrow> 32) cap_frame_cap proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>cap_get_tag (cap_' x) = SCAST(32 signed \<rightarrow> 32) cap_frame_cap; cap_get_tag (cap_C.words_C_update ((\<lambda>v. Arrays.update v (Suc 0) (v.[Suc 0] || (v32_' x >> 14) && 0x3FFFF)) \<circ> (\<lambda>v. Arrays.update v (Suc 0) (v.[Suc 0] && 0xFFFC0000))) (cap_' x)) = SCAST(32 signed \<rightarrow> 32) cap_frame_cap\<rbrakk> \<Longrightarrow> cap_frame_cap_lift (cap_C.words_C_update ((\<lambda>v. Arrays.update v (Suc 0) (v.[Suc 0] || (v32_' x >> 14) && 0x3FFFF)) \<circ> (\<lambda>v. Arrays.update v (Suc 0) (v.[Suc 0] && 0xFFFC0000))) (cap_' x)) = cap_frame_cap_lift (cap_' x)\<lparr>cap_frame_cap_CL.capFMappedAddress_CL := v32_' x && ~~ mask 14\<rparr> proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>cap_get_tag (cap_' x) = 3; cap_get_tag (cap_C.words_C_update ((\<lambda>v. Arrays.update v (Suc 0) (v.[Suc 0] || (v32_' x >> 14) && 0x3FFFF)) \<circ> (\<lambda>v. Arrays.update v (Suc 0) (v.[Suc 0] && 0xFFFC0000))) (cap_' x)) = 3\<rbrakk> \<Longrightarrow> (cap_C.words_C (cap_' x).[Suc 0] && 0xFFFC0000 || (v32_' x >> 14) && 0x3FFFF >> 30) && mask 2 = (cap_C.words_C (cap_' x).[Suc 0] >> 30) && mask 2 \<and> (cap_C.words_C (cap_' x).[Suc 0] && 0xFFFC0000 || (v32_' x >> 14) && 0x3FFFF >> 20) && mask 10 = (cap_C.words_C (cap_' x).[Suc 0] >> 20) && mask 10 \<and> (cap_C.words_C (cap_' x).[Suc 0] && 0xFFFC0000 || (v32_' x >> 14) && 0x3FFFF >> 18) && mask 2 = (cap_C.words_C (cap_' x).[Suc 0] >> 18) && mask 2 \<and> (cap_C.words_C (cap_' x).[Suc 0] && 0xFFFC0000 || (v32_' x >> 14) && 0x3FFFF << 14) && ~~ mask 14 = v32_' x && ~~ mask 14 proof (prove)
goal:
No subgoals!