theory Fastpath_C

lemma fastpath_mi_check_spec:
  "\<forall>s. \<Gamma> \<turnstile> \<lbrace>s. True\<rbrace> Call fastpath_mi_check_'proc
           \<lbrace>(\<acute>ret__int = 0) = (msgExtraCaps (messageInfoFromWord \<^bsup>s\<^esup>msgInfo) = 0
              \<and> msgLength (messageInfoFromWord \<^bsup>s\<^esup>msgInfo) \<le> scast n_msgRegisters
              \<and> seL4_MessageInfo_lift (seL4_MessageInfo_C (FCP (K \<^bsup>s\<^esup>msgInfo)))
                  = mi_from_H (messageInfoFromWord \<^bsup>s\<^esup>msgInfo))\<rbrace>" apply (rule allI, rule conseqPre, vcg) apply (clarsimp simp: seL4_MsgLengthBits_def seL4_MsgExtraCapBits_def
                        word_sle_def if_1_0_0) apply (cut_tac mi="msgInfo_' s" in fastpath_mi_check) apply (simp add: mask_def) apply (auto intro: mi_check_messageInfo_raw[unfolded K_def]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>s. \<Gamma>\<turnstile> \<lbrace>s. True\<rbrace> Call fastpath_mi_check_'proc \<lbrace>(\<acute>ret__int = 0) = (msgExtraCaps (messageInfoFromWord \<^bsup>s\<^esup>msgInfo) = 0 \<and> msgLength (messageInfoFromWord \<^bsup>s\<^esup>msgInfo) \<le> SCAST(32 signed \<rightarrow> 32) n_msgRegisters \<and> seL4_MessageInfo_lift (seL4_MessageInfo_C (FCP (K \<^bsup>s\<^esup>msgInfo))) = mi_from_H (messageInfoFromWord \<^bsup>s\<^esup>msgInfo))\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrace>s. True\<rbrace> \<subseteq> \<lbrace>0 \<le>s 3 \<and> 3 <s 0x20 \<and> 0 \<le>s seL4_MsgLengthBits + seL4_MsgExtraCapBits \<and> seL4_MsgLengthBits + seL4_MsgExtraCapBits <s 0x20 \<and> - 2147483648 \<le> sint seL4_MsgLengthBits + sint seL4_MsgExtraCapBits \<and> sint seL4_MsgLengthBits + sint seL4_MsgExtraCapBits \<le> 2147483647 \<and> (UCAST(32 \<rightarrow> 32 signed) ((\<acute>msgInfo && (1 << unat (seL4_MsgLengthBits + seL4_MsgExtraCapBits)) - 1) + SCAST(32 signed \<rightarrow> 32) 3 && ~~ ((1 << unat 3) - 1)) = 0) = (msgExtraCaps (messageInfoFromWord \<^bsup>s\<^esup>msgInfo) = 0 \<and> msgLength (messageInfoFromWord \<^bsup>s\<^esup>msgInfo) \<le> SCAST(32 signed \<rightarrow> 32) n_msgRegisters \<and> seL4_MessageInfo_lift (seL4_MessageInfo_C (FCP (K \<^bsup>s\<^esup>msgInfo))) = mi_from_H (messageInfoFromWord \<^bsup>s\<^esup>msgInfo))\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. ((msgInfo_' s && 0x1FF) + 3 && 0xFFFFFFF8 = 0) = (msgExtraCaps (messageInfoFromWord (msgInfo_' s)) = 0 \<and> msgLength (messageInfoFromWord (msgInfo_' s)) \<le> SCAST(32 signed \<rightarrow> 32) n_msgRegisters \<and> seL4_MessageInfo_lift (seL4_MessageInfo_C (ARRAY i. msgInfo_' s)) = mi_from_H (messageInfoFromWord (msgInfo_' s))) proof (prove)
goal (1 subgoal):
 1. \<And>s. ((msgInfo_' s && mask 9) + 3 && ~~ mask 3 = 0) = (msgExtraCaps (messageInfoFromWord (msgInfo_' s)) = 0 \<and> msgLength (messageInfoFromWord (msgInfo_' s)) \<le> SCAST(32 signed \<rightarrow> 32) n_msgRegisters \<and> length_CL (seL4_MessageInfo_lift (seL4_MessageInfo_C (FCP (K (msgInfo_' s))))) \<le> SCAST(32 signed \<rightarrow> 32) n_msgRegisters) \<Longrightarrow> ((msgInfo_' s && 0x1FF) + 3 && 0xFFFFFFF8 = 0) = (msgExtraCaps (messageInfoFromWord (msgInfo_' s)) = 0 \<and> msgLength (messageInfoFromWord (msgInfo_' s)) \<le> SCAST(32 signed \<rightarrow> 32) n_msgRegisters \<and> seL4_MessageInfo_lift (seL4_MessageInfo_C (ARRAY i. msgInfo_' s)) = mi_from_H (messageInfoFromWord (msgInfo_' s))) proof (prove)
goal (1 subgoal):
 1. \<And>s. ((msgInfo_' s && 0x1FF) + 3 && 0xFFFFFFF8 = 0) = (msgExtraCaps (messageInfoFromWord (msgInfo_' s)) = 0 \<and> msgLength (messageInfoFromWord (msgInfo_' s)) \<le> SCAST(32 signed \<rightarrow> 32) n_msgRegisters \<and> length_CL (seL4_MessageInfo_lift (seL4_MessageInfo_C (ARRAY i. msgInfo_' s))) \<le> SCAST(32 signed \<rightarrow> 32) n_msgRegisters) \<Longrightarrow> (msgExtraCaps (messageInfoFromWord (msgInfo_' s)) = 0 \<and> msgLength (messageInfoFromWord (msgInfo_' s)) \<le> SCAST(32 signed \<rightarrow> 32) n_msgRegisters \<and> length_CL (seL4_MessageInfo_lift (seL4_MessageInfo_C (ARRAY i. msgInfo_' s))) \<le> SCAST(32 signed \<rightarrow> 32) n_msgRegisters) = (msgExtraCaps (messageInfoFromWord (msgInfo_' s)) = 0 \<and> msgLength (messageInfoFromWord (msgInfo_' s)) \<le> SCAST(32 signed \<rightarrow> 32) n_msgRegisters \<and> seL4_MessageInfo_lift (seL4_MessageInfo_C (ARRAY i. msgInfo_' s)) = mi_from_H (messageInfoFromWord (msgInfo_' s))) proof (prove)
goal:
No subgoals!