theory structures_proofs

lemma (in kernel_all_substitute) cap_endpoint_cap_new_spec:
  "\<forall>s. \<Gamma> \<turnstile> {s}
       \<acute>ret__struct_cap_C :== PROC cap_endpoint_cap_new(\<acute>capEPBadge, \<acute>capCanGrantReply, \<acute>capCanGrant, \<acute>capCanSend, \<acute>capCanReceive, \<acute>capEPPtr)
       \<lbrace>cap_endpoint_cap_lift \<acute>ret__struct_cap_C = \<lparr>
          cap_endpoint_cap_CL.capEPBadge_CL = (\<^bsup>s\<^esup>capEPBadge___unsigned AND mask 28),
          cap_endpoint_cap_CL.capCanGrantReply_CL = (\<^bsup>s\<^esup>capCanGrantReply___unsigned AND mask 1),
          cap_endpoint_cap_CL.capCanGrant_CL = (\<^bsup>s\<^esup>capCanGrant___unsigned AND mask 1),
          cap_endpoint_cap_CL.capCanSend_CL = (\<^bsup>s\<^esup>capCanSend___unsigned AND mask 1),
          cap_endpoint_cap_CL.capCanReceive_CL = (\<^bsup>s\<^esup>capCanReceive___unsigned AND mask 1),
          cap_endpoint_cap_CL.capEPPtr_CL = (\<^bsup>s\<^esup>capEPPtr___unsigned AND NOT (mask 4)) \<rparr> \<and>
        cap_get_tag \<acute>ret__struct_cap_C = scast cap_endpoint_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_endpoint_cap_def
                         mask_def shift_over_ao_dists word_bw_assocs word_ao_dist) apply (simp add: cap_endpoint_cap_lift_def) apply (erule cap_lift_endpoint_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_endpoint_cap_def))? done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>s. \<Gamma>\<turnstile> {s} Call cap_endpoint_cap_new_'proc \<lbrace>cap_endpoint_cap_lift \<acute>ret__struct_cap_C = \<lparr>capEPBadge_CL = \<^bsup>s\<^esup>capEPBadge && mask 28, capCanGrantReply_CL = \<^bsup>s\<^esup>capCanGrantReply && mask 1, capCanGrant_CL = \<^bsup>s\<^esup>capCanGrant && mask 1, capCanSend_CL = \<^bsup>s\<^esup>capCanSend && mask 1, capCanReceive_CL = \<^bsup>s\<^esup>capCanReceive && mask 1, capEPPtr_CL = \<^bsup>s\<^esup>capEPPtr && ~~ mask 4\<rparr> \<and> cap_get_tag \<acute>ret__struct_cap_C = SCAST(32 signed \<rightarrow> 32) cap_endpoint_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 4 \<and> 4 <s 0x20 \<and> 1 <s 2 \<and> 0 \<le>s 1 \<and> 0 \<le>s 0 \<and> 0 <s 0x20 \<and> 0 \<le>s 1 \<and> 1 <s 0x20 \<and> 0 \<le>s 0 \<and> 0 <s 0x20 \<and> 0 \<le>s 2 \<and> 2 <s 0x20 \<and> 0 \<le>s 3 \<and> 3 <s 0x20 \<and> cap_endpoint_cap_lift (cap_C.words_C_update (\<lambda>v. Arrays.update v (unat 1) (((((SCAST(32 signed \<rightarrow> 32) 0 || (\<acute>capCanGrantReply && 1 << unat 3)) || (\<acute>capCanGrant && 1 << unat 2)) || (\<acute>capCanSend && 1 << unat 0)) || (\<acute>capCanReceive && 1 << unat 1)) || (\<acute>capEPPtr && 0xFFFFFFF0 >> unat 0))) (cap_C.words_C_update (\<lambda>v. Arrays.update v (unat 0) ((SCAST(32 signed \<rightarrow> 32) 0 || (\<acute>capEPBadge && 0xFFFFFFF << unat 4)) || (SCAST(32 signed \<rightarrow> 32) cap_endpoint_cap && 0xF << unat 0))) v)) = \<lparr>capEPBadge_CL = \<^bsup>s\<^esup>capEPBadge && mask 28, capCanGrantReply_CL = \<^bsup>s\<^esup>capCanGrantReply && mask 1, capCanGrant_CL = \<^bsup>s\<^esup>capCanGrant && mask 1, capCanSend_CL = \<^bsup>s\<^esup>capCanSend && mask 1, capCanReceive_CL = \<^bsup>s\<^esup>capCanReceive && mask 1, capEPPtr_CL = \<^bsup>s\<^esup>capEPPtr && ~~ mask 4\<rparr> \<and> cap_get_tag (cap_C.words_C_update (\<lambda>v. Arrays.update v (unat 1) (((((SCAST(32 signed \<rightarrow> 32) 0 || (\<acute>capCanGrantReply && 1 << unat 3)) || (\<acute>capCanGrant && 1 << unat 2)) || (\<acute>capCanSend && 1 << unat 0)) || (\<acute>capCanReceive && 1 << unat 1)) || (\<acute>capEPPtr && 0xFFFFFFF0 >> unat 0))) (cap_C.words_C_update (\<lambda>v. Arrays.update v (unat 0) ((SCAST(32 signed \<rightarrow> 32) 0 || (\<acute>capEPBadge && 0xFFFFFFF << unat 4)) || (SCAST(32 signed \<rightarrow> 32) cap_endpoint_cap && 0xF << unat 0))) v)) = SCAST(32 signed \<rightarrow> 32) cap_endpoint_cap\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s v. cap_endpoint_cap_lift (cap_C.words_C_update (\<lambda>x. Arrays.update (Arrays.update x 0 ((capEPBadge_' s << 4) && 0xFFFFFFF0 || SCAST(32 signed \<rightarrow> 32) cap_endpoint_cap && 0xF)) (Suc 0) (((((capCanGrantReply_' s << 3) && 8 || (capCanGrant_' s << 2) && 4) || capCanSend_' s && 1) || (capCanReceive_' s << Suc 0) && 2) || capEPPtr_' s && 0xFFFFFFF0)) v) = \<lparr>capEPBadge_CL = capEPBadge_' s && 0xFFFFFFF, capCanGrantReply_CL = capCanGrantReply_' s && 1, capCanGrant_CL = capCanGrant_' s && 1, capCanSend_CL = capCanSend_' s && 1, capCanReceive_CL = capCanReceive_' s && 1, capEPPtr_CL = capEPPtr_' s && 0xFFFFFFF0\<rparr> \<and> cap_get_tag (cap_C.words_C_update (\<lambda>x. Arrays.update (Arrays.update x 0 ((capEPBadge_' s << 4) && 0xFFFFFFF0 || SCAST(32 signed \<rightarrow> 32) cap_endpoint_cap && 0xF)) (Suc 0) (((((capCanGrantReply_' s << 3) && 8 || (capCanGrant_' s << 2) && 4) || capCanSend_' s && 1) || (capCanReceive_' s << Suc 0) && 2) || capEPPtr_' s && 0xFFFFFFF0)) v) = SCAST(32 signed \<rightarrow> 32) cap_endpoint_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 ((capEPBadge_' s << 4) && 0xFFFFFFF0 || SCAST(32 signed \<rightarrow> 32) cap_endpoint_cap && 0xF)) (Suc 0) (((((capCanGrantReply_' s << 3) && 8 || (capCanGrant_' s << 2) && 4) || capCanSend_' s && 1) || (capCanReceive_' s << Suc 0) && 2) || capEPPtr_' s && 0xFFFFFFF0)) v) = SCAST(32 signed \<rightarrow> 32) cap_endpoint_cap \<Longrightarrow> cap_endpoint_cap_lift (cap_C.words_C_update (\<lambda>x. Arrays.update (Arrays.update x 0 ((capEPBadge_' s << 4) && 0xFFFFFFF0 || SCAST(32 signed \<rightarrow> 32) cap_endpoint_cap && 0xF)) (Suc 0) (((((capCanGrantReply_' s << 3) && 8 || (capCanGrant_' s << 2) && 4) || capCanSend_' s && 1) || (capCanReceive_' s << Suc 0) && 2) || capEPPtr_' s && 0xFFFFFFF0)) v) = \<lparr>capEPBadge_CL = capEPBadge_' s && 0xFFFFFFF, capCanGrantReply_CL = capCanGrantReply_' s && 1, capCanGrant_CL = capCanGrant_' s && 1, capCanSend_CL = capCanSend_' s && 1, capCanReceive_CL = capCanReceive_' s && 1, capEPPtr_CL = capEPPtr_' s && 0xFFFFFFF0\<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 ((capEPBadge_' s << 4) && 0xFFFFFFF0 || SCAST(32 signed \<rightarrow> 32) cap_endpoint_cap && 0xF)) (Suc 0) (((((capCanGrantReply_' s << 3) && 8 || (capCanGrant_' s << 2) && 4) || capCanSend_' s && 1) || (capCanReceive_' s << Suc 0) && 2) || capEPPtr_' s && 0xFFFFFFF0)) v) = SCAST(32 signed \<rightarrow> 32) cap_endpoint_cap \<Longrightarrow> (case cap_lift (cap_C.words_C_update (\<lambda>x. Arrays.update (Arrays.update x 0 ((capEPBadge_' s << 4) && 0xFFFFFFF0 || SCAST(32 signed \<rightarrow> 32) cap_endpoint_cap && 0xF)) (Suc 0) (((((capCanGrantReply_' s << 3) && 8 || (capCanGrant_' s << 2) && 4) || capCanSend_' s && 1) || (capCanReceive_' s << Suc 0) && 2) || capEPPtr_' s && 0xFFFFFFF0)) v) of Some (Cap_endpoint_cap rec) \<Rightarrow> rec) = \<lparr>capEPBadge_CL = capEPBadge_' s && 0xFFFFFFF, capCanGrantReply_CL = capCanGrantReply_' s && 1, capCanGrant_CL = capCanGrant_' s && 1, capCanSend_CL = capCanSend_' s && 1, capCanReceive_CL = capCanReceive_' s && 1, capEPPtr_CL = capEPPtr_' s && 0xFFFFFFF0\<rparr> proof (prove)
goal (1 subgoal):
 1. \<And>s. ((capEPBadge_' s << 4) && 0xFFFFFFF0 || SCAST(32 signed \<rightarrow> 32) cap_endpoint_cap && 0xF >> 4) && mask 28 = capEPBadge_' s && 0xFFFFFFF \<and> (((((capCanGrantReply_' s << 3) && 8 || (capCanGrant_' s << 2) && 4) || capCanSend_' s && 1) || (capCanReceive_' s << Suc 0) && 2) || capEPPtr_' s && 0xFFFFFFF0 >> 3) && 1 = capCanGrantReply_' s && 1 \<and> (((((capCanGrantReply_' s << 3) && 8 || (capCanGrant_' s << 2) && 4) || capCanSend_' s && 1) || (capCanReceive_' s << Suc 0) && 2) || capEPPtr_' s && 0xFFFFFFF0 >> 2) && 1 = capCanGrant_' s && 1 \<and> (((((capCanGrantReply_' s << 3) && 8 || (capCanGrant_' s << 2) && 4) || capCanSend_' s && 1) || (capCanReceive_' s << Suc 0) && 2) || capEPPtr_' s && 0xFFFFFFF0) && 1 = capCanSend_' s && 1 \<and> (((((capCanGrantReply_' s << 3) && 8 || (capCanGrant_' s << 2) && 4) || capCanSend_' s && 1) || (capCanReceive_' s << Suc 0) && 2) || capEPPtr_' s && 0xFFFFFFF0 >> Suc 0) && 1 = capCanReceive_' s && 1 \<and> (((((capCanGrantReply_' s << 3) && 8 || (capCanGrant_' s << 2) && 4) || capCanSend_' s && 1) || (capCanReceive_' s << Suc 0) && 2) || capEPPtr_' s && 0xFFFFFFF0) && ~~ mask 4 = capEPPtr_' s && 0xFFFFFFF0 proof (prove)
goal:
No subgoals!