theory shared_types_proofs

lemma (in kernel_all_substitute) seL4_MessageInfo_new_spec:
  "\<forall> s. \<Gamma> \<turnstile> {s}
       \<acute>ret__struct_seL4_MessageInfo_C :== PROC seL4_MessageInfo_new(\<acute>label, \<acute>capsUnwrapped, \<acute>extraCaps, \<acute>length)
       \<lbrace> seL4_MessageInfo_lift \<acute>ret__struct_seL4_MessageInfo_C = \<lparr>
          seL4_MessageInfo_CL.label_CL = (\<^bsup>s\<^esup>label AND mask 20),
          seL4_MessageInfo_CL.capsUnwrapped_CL = (\<^bsup>s\<^esup>capsUnwrapped AND mask 3),
          seL4_MessageInfo_CL.extraCaps_CL = (\<^bsup>s\<^esup>extraCaps AND mask 2),
          seL4_MessageInfo_CL.length_CL = (\<^bsup>s\<^esup>length AND mask 7) \<rparr> \<rbrace>" apply (rule allI, rule conseqPre, vcg) apply (clarsimp simp: guard_simps) apply (simp add: seL4_MessageInfo_lift_def) 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> {s} Call seL4_MessageInfo_new_'proc \<lbrace>seL4_MessageInfo_lift \<acute>ret__struct_seL4_MessageInfo_C = \<lparr>label_CL = \<^bsup>s\<^esup>label && mask 20, capsUnwrapped_CL = \<^bsup>s\<^esup>capsUnwrapped && mask 3, extraCaps_CL = \<^bsup>s\<^esup>extraCaps && mask 2, length_CL = \<^bsup>s\<^esup>length && mask 7\<rparr>\<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 7 \<and> 7 <s 0x20 \<and> 0 \<le>s 9 \<and> 9 <s 0x20 \<and> 0 \<le>s 0xC \<and> 0xC <s 0x20 \<and> seL4_MessageInfo_lift (seL4_MessageInfo_C.words_C_update (\<lambda>v. Arrays.update v (unat 0) ((((SCAST(32 signed \<rightarrow> 32) 0 || (\<acute>label && 0xFFFFF << unat 0xC)) || (\<acute>capsUnwrapped && 7 << unat 9)) || (\<acute>extraCaps && 3 << unat 7)) || (\<acute>length && 0x7F << unat 0))) v) = \<lparr>label_CL = \<^bsup>s\<^esup>label && mask 20, capsUnwrapped_CL = \<^bsup>s\<^esup>capsUnwrapped && mask 3, extraCaps_CL = \<^bsup>s\<^esup>extraCaps && mask 2, length_CL = \<^bsup>s\<^esup>length && mask 7\<rparr>\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s v. seL4_MessageInfo_lift (seL4_MessageInfo_C.words_C_update (\<lambda>v. Arrays.update v 0 ((((label_' s && 0xFFFFF << 12) || (capsUnwrapped_' s && 7 << 9)) || (extraCaps_' s && 3 << 7)) || length_' s && 0x7F)) v) = \<lparr>label_CL = label_' s && mask 20, capsUnwrapped_CL = capsUnwrapped_' s && mask 3, extraCaps_CL = extraCaps_' s && mask 2, length_CL = length_' s && mask 7\<rparr> proof (prove)
goal (1 subgoal):
 1. \<And>s. ((((label_' s && 0xFFFFF << 12) || (capsUnwrapped_' s && 7 << 9)) || (extraCaps_' s && 3 << 7)) || length_' s && 0x7F >> 12) && mask 20 = label_' s && mask 20 \<and> ((((label_' s && 0xFFFFF << 12) || (capsUnwrapped_' s && 7 << 9)) || (extraCaps_' s && 3 << 7)) || length_' s && 0x7F >> 9) && mask 3 = capsUnwrapped_' s && mask 3 \<and> ((((label_' s && 0xFFFFF << 12) || (capsUnwrapped_' s && 7 << 9)) || (extraCaps_' s && 3 << 7)) || length_' s && 0x7F >> 7) && mask 2 = extraCaps_' s && mask 2 \<and> ((((label_' s && 0xFFFFF << 12) || (capsUnwrapped_' s && 7 << 9)) || (extraCaps_' s && 3 << 7)) || length_' s && 0x7F) && mask 7 = length_' s && mask 7 proof (prove)
goal:
No subgoals!