theory structures_proofs

lemma (in kernel_all_substitute) cap_frame_cap_new_spec:
  "\<forall>s. \<Gamma> \<turnstile> {s}
       \<acute>ret__struct_cap_C :== PROC cap_frame_cap_new(\<acute>capFSize, \<acute>capFMappedASIDLow, \<acute>capFVMRights, \<acute>capFMappedAddress, \<acute>capFIsDevice, \<acute>capFMappedASIDHigh, \<acute>capFBasePtr)
       \<lbrace>cap_frame_cap_lift \<acute>ret__struct_cap_C = \<lparr>
          cap_frame_cap_CL.capFSize_CL = (\<^bsup>s\<^esup>capFSize___unsigned AND mask 2),
          cap_frame_cap_CL.capFMappedASIDLow_CL = (\<^bsup>s\<^esup>capFMappedASIDLow___unsigned AND mask 10),
          cap_frame_cap_CL.capFVMRights_CL = (\<^bsup>s\<^esup>capFVMRights___unsigned AND mask 2),
          cap_frame_cap_CL.capFMappedAddress_CL = (\<^bsup>s\<^esup>capFMappedAddress___unsigned AND NOT (mask 14)),
          cap_frame_cap_CL.capFIsDevice_CL = (\<^bsup>s\<^esup>capFIsDevice___unsigned AND mask 1),
          cap_frame_cap_CL.capFMappedASIDHigh_CL = (\<^bsup>s\<^esup>capFMappedASIDHigh___unsigned AND mask 7),
          cap_frame_cap_CL.capFBasePtr_CL = (\<^bsup>s\<^esup>capFBasePtr___unsigned 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 simp: guard_simps o_def mask_def shift_over_ao_dists) apply (rule context_conjI[THEN iffD1[OF conj_commute]],
         fastforce simp: cap_get_tag_eq_x cap_frame_cap_def
                         mask_def shift_over_ao_dists word_bw_assocs word_ao_dist) apply (simp add: cap_frame_cap_lift_def) apply (erule cap_lift_frame_cap[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 cap_frame_cap_def))? done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>s. \<Gamma>\<turnstile> {s} Call cap_frame_cap_new_'proc \<lbrace>cap_frame_cap_lift \<acute>ret__struct_cap_C = \<lparr>capFSize_CL = \<^bsup>s\<^esup>capFSize && mask 2, capFMappedASIDLow_CL = \<^bsup>s\<^esup>capFMappedASIDLow && mask 10, capFVMRights_CL = \<^bsup>s\<^esup>capFVMRights && mask 2, capFMappedAddress_CL = \<^bsup>s\<^esup>capFMappedAddress && ~~ mask 14, capFIsDevice_CL = \<^bsup>s\<^esup>capFIsDevice && mask 1, capFMappedASIDHigh_CL = \<^bsup>s\<^esup>capFMappedASIDHigh && mask 7, capFBasePtr_CL = \<^bsup>s\<^esup>capFBasePtr && ~~ 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. {s} \<subseteq> \<lbrace>\<forall>v. 0 <s 2 \<and> 0 \<le>s 0 \<and> 0 <s 0x20 \<and> 0 \<le>s 0xA \<and> 0xA <s 0x20 \<and> 0 \<le>s 0x16 \<and> 0x16 <s 0x20 \<and> 0 \<le>s 0x1D \<and> 0x1D <s 0x20 \<and> 1 <s 2 \<and> 0 \<le>s 1 \<and> 0 \<le>s 0xE \<and> 0xE <s 0x20 \<and> 0 \<le>s 0x12 \<and> 0x12 <s 0x20 \<and> 0 \<le>s 0x14 \<and> 0x14 <s 0x20 \<and> 0 \<le>s 0x1E \<and> 0x1E <s 0x20 \<and> cap_frame_cap_lift (cap_C.words_C_update (\<lambda>v. Arrays.update v (unat 1) ((((SCAST(32 signed \<rightarrow> 32) 0 || (\<acute>capFSize && 3 << unat 0x1E)) || (\<acute>capFMappedASIDLow && 0x3FF << unat 0x14)) || (\<acute>capFVMRights && 3 << unat 0x12)) || (\<acute>capFMappedAddress && 0xFFFFC000 >> unat 0xE))) (cap_C.words_C_update (\<lambda>v. Arrays.update v (unat 0) ((((SCAST(32 signed \<rightarrow> 32) 0 || (\<acute>capFIsDevice && 1 << unat 0x1D)) || (\<acute>capFMappedASIDHigh && 0x7F << unat 0x16)) || (\<acute>capFBasePtr && 0xFFFFC000 >> unat 0xA)) || (SCAST(32 signed \<rightarrow> 32) cap_frame_cap && 0xF << unat 0))) v)) = \<lparr>capFSize_CL = \<^bsup>s\<^esup>capFSize && mask 2, capFMappedASIDLow_CL = \<^bsup>s\<^esup>capFMappedASIDLow && mask 10, capFVMRights_CL = \<^bsup>s\<^esup>capFVMRights && mask 2, capFMappedAddress_CL = \<^bsup>s\<^esup>capFMappedAddress && ~~ mask 14, capFIsDevice_CL = \<^bsup>s\<^esup>capFIsDevice && mask 1, capFMappedASIDHigh_CL = \<^bsup>s\<^esup>capFMappedASIDHigh && mask 7, capFBasePtr_CL = \<^bsup>s\<^esup>capFBasePtr && ~~ mask 14\<rparr> \<and> cap_get_tag (cap_C.words_C_update (\<lambda>v. Arrays.update v (unat 1) ((((SCAST(32 signed \<rightarrow> 32) 0 || (\<acute>capFSize && 3 << unat 0x1E)) || (\<acute>capFMappedASIDLow && 0x3FF << unat 0x14)) || (\<acute>capFVMRights && 3 << unat 0x12)) || (\<acute>capFMappedAddress && 0xFFFFC000 >> unat 0xE))) (cap_C.words_C_update (\<lambda>v. Arrays.update v (unat 0) ((((SCAST(32 signed \<rightarrow> 32) 0 || (\<acute>capFIsDevice && 1 << unat 0x1D)) || (\<acute>capFMappedASIDHigh && 0x7F << unat 0x16)) || (\<acute>capFBasePtr && 0xFFFFC000 >> unat 0xA)) || (SCAST(32 signed \<rightarrow> 32) cap_frame_cap && 0xF << unat 0))) v)) = SCAST(32 signed \<rightarrow> 32) cap_frame_cap\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s v. cap_frame_cap_lift (cap_C.words_C_update (\<lambda>x. Arrays.update (Arrays.update x 0 ((((capFIsDevice_' s << 29) && 0x20000000 || (capFMappedASIDHigh_' s << 22) && 0x1FC00000) || (capFBasePtr_' s >> 10) && 0x3FFFF0) || SCAST(32 signed \<rightarrow> 32) cap_frame_cap && 0xF)) (Suc 0) ((((capFSize_' s << 30) && 0xC0000000 || (capFMappedASIDLow_' s << 20) && 0x3FF00000) || (capFVMRights_' s << 18) && 0xC0000) || (capFMappedAddress_' s >> 14) && 0x3FFFF)) v) = \<lparr>capFSize_CL = capFSize_' s && 3, capFMappedASIDLow_CL = capFMappedASIDLow_' s && 0x3FF, capFVMRights_CL = capFVMRights_' s && 3, capFMappedAddress_CL = capFMappedAddress_' s && 0xFFFFC000, capFIsDevice_CL = capFIsDevice_' s && 1, capFMappedASIDHigh_CL = capFMappedASIDHigh_' s && 0x7F, capFBasePtr_CL = capFBasePtr_' s && 0xFFFFC000\<rparr> \<and> cap_get_tag (cap_C.words_C_update (\<lambda>x. Arrays.update (Arrays.update x 0 ((((capFIsDevice_' s << 29) && 0x20000000 || (capFMappedASIDHigh_' s << 22) && 0x1FC00000) || (capFBasePtr_' s >> 10) && 0x3FFFF0) || SCAST(32 signed \<rightarrow> 32) cap_frame_cap && 0xF)) (Suc 0) ((((capFSize_' s << 30) && 0xC0000000 || (capFMappedASIDLow_' s << 20) && 0x3FF00000) || (capFVMRights_' s << 18) && 0xC0000) || (capFMappedAddress_' s >> 14) && 0x3FFFF)) v) = SCAST(32 signed \<rightarrow> 32) cap_frame_cap proof (prove)
goal (1 subgoal):
 1. \<And>s v. cap_get_tag (cap_C.words_C_update (\<lambda>x. Arrays.update (Arrays.update x 0 ((((capFIsDevice_' s << 29) && 0x20000000 || (capFMappedASIDHigh_' s << 22) && 0x1FC00000) || (capFBasePtr_' s >> 10) && 0x3FFFF0) || SCAST(32 signed \<rightarrow> 32) cap_frame_cap && 0xF)) (Suc 0) ((((capFSize_' s << 30) && 0xC0000000 || (capFMappedASIDLow_' s << 20) && 0x3FF00000) || (capFVMRights_' s << 18) && 0xC0000) || (capFMappedAddress_' s >> 14) && 0x3FFFF)) v) = SCAST(32 signed \<rightarrow> 32) cap_frame_cap \<Longrightarrow> cap_frame_cap_lift (cap_C.words_C_update (\<lambda>x. Arrays.update (Arrays.update x 0 ((((capFIsDevice_' s << 29) && 0x20000000 || (capFMappedASIDHigh_' s << 22) && 0x1FC00000) || (capFBasePtr_' s >> 10) && 0x3FFFF0) || SCAST(32 signed \<rightarrow> 32) cap_frame_cap && 0xF)) (Suc 0) ((((capFSize_' s << 30) && 0xC0000000 || (capFMappedASIDLow_' s << 20) && 0x3FF00000) || (capFVMRights_' s << 18) && 0xC0000) || (capFMappedAddress_' s >> 14) && 0x3FFFF)) v) = \<lparr>capFSize_CL = capFSize_' s && 3, capFMappedASIDLow_CL = capFMappedASIDLow_' s && 0x3FF, capFVMRights_CL = capFVMRights_' s && 3, capFMappedAddress_CL = capFMappedAddress_' s && 0xFFFFC000, capFIsDevice_CL = capFIsDevice_' s && 1, capFMappedASIDHigh_CL = capFMappedASIDHigh_' s && 0x7F, capFBasePtr_CL = capFBasePtr_' s && 0xFFFFC000\<rparr> proof (prove)
goal (1 subgoal):
 1. \<And>s v. cap_get_tag (cap_C.words_C_update (\<lambda>x. Arrays.update (Arrays.update x 0 ((((capFIsDevice_' s << 29) && 0x20000000 || (capFMappedASIDHigh_' s << 22) && 0x1FC00000) || (capFBasePtr_' s >> 10) && 0x3FFFF0) || SCAST(32 signed \<rightarrow> 32) cap_frame_cap && 0xF)) (Suc 0) ((((capFSize_' s << 30) && 0xC0000000 || (capFMappedASIDLow_' s << 20) && 0x3FF00000) || (capFVMRights_' s << 18) && 0xC0000) || (capFMappedAddress_' s >> 14) && 0x3FFFF)) v) = SCAST(32 signed \<rightarrow> 32) cap_frame_cap \<Longrightarrow> (case cap_lift (cap_C.words_C_update (\<lambda>x. Arrays.update (Arrays.update x 0 ((((capFIsDevice_' s << 29) && 0x20000000 || (capFMappedASIDHigh_' s << 22) && 0x1FC00000) || (capFBasePtr_' s >> 10) && 0x3FFFF0) || SCAST(32 signed \<rightarrow> 32) cap_frame_cap && 0xF)) (Suc 0) ((((capFSize_' s << 30) && 0xC0000000 || (capFMappedASIDLow_' s << 20) && 0x3FF00000) || (capFVMRights_' s << 18) && 0xC0000) || (capFMappedAddress_' s >> 14) && 0x3FFFF)) v) of Some (Cap_frame_cap rec) \<Rightarrow> rec) = \<lparr>capFSize_CL = capFSize_' s && 3, capFMappedASIDLow_CL = capFMappedASIDLow_' s && 0x3FF, capFVMRights_CL = capFVMRights_' s && 3, capFMappedAddress_CL = capFMappedAddress_' s && 0xFFFFC000, capFIsDevice_CL = capFIsDevice_' s && 1, capFMappedASIDHigh_CL = capFMappedASIDHigh_' s && 0x7F, capFBasePtr_CL = capFBasePtr_' s && 0xFFFFC000\<rparr> proof (prove)
goal (1 subgoal):
 1. \<And>s. ((((capFSize_' s << 30) && 0xC0000000 || (capFMappedASIDLow_' s << 20) && 0x3FF00000) || (capFVMRights_' s << 18) && 0xC0000) || (capFMappedAddress_' s >> 14) && 0x3FFFF >> 30) && mask 2 = capFSize_' s && 3 \<and> ((((capFSize_' s << 30) && 0xC0000000 || (capFMappedASIDLow_' s << 20) && 0x3FF00000) || (capFVMRights_' s << 18) && 0xC0000) || (capFMappedAddress_' s >> 14) && 0x3FFFF >> 20) && mask 10 = capFMappedASIDLow_' s && 0x3FF \<and> ((((capFSize_' s << 30) && 0xC0000000 || (capFMappedASIDLow_' s << 20) && 0x3FF00000) || (capFVMRights_' s << 18) && 0xC0000) || (capFMappedAddress_' s >> 14) && 0x3FFFF >> 18) && mask 2 = capFVMRights_' s && 3 \<and> ((((capFSize_' s << 30) && 0xC0000000 || (capFMappedASIDLow_' s << 20) && 0x3FF00000) || (capFVMRights_' s << 18) && 0xC0000) || (capFMappedAddress_' s >> 14) && 0x3FFFF << 14) && ~~ mask 14 = capFMappedAddress_' s && 0xFFFFC000 \<and> ((((capFIsDevice_' s << 29) && 0x20000000 || (capFMappedASIDHigh_' s << 22) && 0x1FC00000) || (capFBasePtr_' s >> 10) && 0x3FFFF0) || SCAST(32 signed \<rightarrow> 32) cap_frame_cap && 0xF >> 29) && 1 = capFIsDevice_' s && 1 \<and> ((((capFIsDevice_' s << 29) && 0x20000000 || (capFMappedASIDHigh_' s << 22) && 0x1FC00000) || (capFBasePtr_' s >> 10) && 0x3FFFF0) || SCAST(32 signed \<rightarrow> 32) cap_frame_cap && 0xF >> 22) && mask 7 = capFMappedASIDHigh_' s && 0x7F \<and> ((((capFIsDevice_' s << 29) && 0x20000000 || (capFMappedASIDHigh_' s << 22) && 0x1FC00000) || (capFBasePtr_' s >> 10) && 0x3FFFF0) || SCAST(32 signed \<rightarrow> 32) cap_frame_cap && 0xF << 10) && ~~ mask 14 = capFBasePtr_' s && 0xFFFFC000 proof (prove)
goal:
No subgoals!