proposition: Lemma CorrectAlignedEncoderForPseudoChecksumThenC {S} (srcAddr : ByteBuffer.t 4) (destAddr : ByteBuffer.t 4) (udpLength : word 16) (protoCode : word 8) (format_A format_B : FormatM S ByteString) (encode_A : forall sz, AlignedEncodeM sz) (encode_B : forall sz, AlignedEncodeM sz) (encoder_B_OK : CorrectAlignedEncoder format_B encode_B) (encoder_A_OK : CorrectAlignedEncoder format_A encode_A) n1 (format_B_sz_OK' : forall (s : S) (b : ByteString) (env env' : CacheFormat), format_B s env ∋ (b, env') -> bin_measure b = n1) (format_B_sz_OK : n1 mod 16 = 0) (len_format_A : S -> nat) (format_A_sz_OK' : forall (s : S) (b : ByteString) (env env' : CacheFormat), format_A s env ∋ (b, env') -> bin_measure b = len_format_A s) (format_A_sz_OK : forall (s : S), len_format_A s mod 8 = 0) : CorrectAlignedEncoder (format_B ThenChecksum (Pseudo_Checksum_Valid srcAddr destAddr udpLength protoCode) OfSize 16 ThenCarryOn format_A) (AlignedEncoderForChecksum n1 encode_B encode_A (calculate_aligned_Pseudochecksum srcAddr destAddr udpLength protoCode)).
proof: Proof. apply CorrectAlignedEncoderForChecksum'; unfold calculate_aligned_Pseudochecksum; eauto with nocore; intros. - rewrite calculate_aligned_Pseudochecksum_front. rewrite calculate_aligned_Pseudochecksum_tail. reflexivity. - destruct_conjs. assert (bin_measure b1 mod 16 = 0) as L1 by (erewrite format_B_sz_OK'; eauto). assert (padding b3 = 0) as L2 by (rewrite padding_eq_mod_8; erewrite format_A_sz_OK'; eauto). unfold f_bit_aligned_free, Pseudo_Checksum_Valid, onesComplement. rewrite calculate_aligned_Pseudochecksum_equiv. unfold calculate_aligned_Pseudochecksum''. unfold calculate_aligned_IPchecksum'. rewrite <- InternetChecksum_To_ByteBuffer_Checksum'. rewrite ByteString2ListOfChar_Over. rewrite !build_aligned_ByteString_append. rewrite !build_aligned_ByteString_byteString_idem. rewrite Nat.mul_add_distr_r. match goal with | |- context [numBytes ?a * 8] => replace (numBytes a * 8) with (bin_measure a) end. 2 : rewrite length_ByteString_no_padding; try omega. match goal with | |- context [wnot (checksum (ByteString2ListOfChar ?a ?b))] => assert (a = bin_measure b) as L end. { rewrite !@mappend_measure. rewrite !Nat.add_assoc. reflexivity. } rewrite L. clear L. rewrite !ByteString2ListOfChar_append. rewrite !ByteString2ListOfChar_format_checksum. assert (forall n, n mod 16 = 0 -> forall b, exists x, |ByteString2ListOfChar n b| = 2 * x) as L. { clear. intros. apply Nat.mod_divides in H; eauto. destruct H as [x ?]. replace (16 * x) with (8 * (2*x)) in * by omega. subst. rewrite ByteString2ListOfChar_len. eauto. } destruct L with (n:=bin_measure b1) (b:=b1) as [x1 ?]; eauto. clear L. set (ByteString2ListOfChar (bin_measure b1) b1) as l1 in *. set (ByteString2ListOfChar (bin_measure b3) b3) as l3 in *. rewrite !ByteString2ListOfChar_eq'. simpl Core.byteString. unfold ByteBuffer.to_list. unfold hi8, lo8. rewrite split1_wzero, split2_wzero. match goal with | |- checksum (?a :: ?b :: ?l)%list = _ => replace (a :: b :: l)%list with (to_list (a :: [b])%vector ++ l)%list by reflexivity end. rewrite !app_assoc. unfold Core.char in *. match goal with | |- context [(?a ++ l1)%list] => set (a ++ l1)%list as l1' end. assert (exists x, | l1' | = 2 * x) as L'. { subst l1'. simpl. rewrite !app_length. rewrite <- !ByteBuffer.to_list_length. rewrite H7. exists (6+x1). omega. } destruct L' as [x L']. rewrite <- !app_assoc. match goal with | |- context [wnot (checksum ?a)] => assert (checksum a = checksum (l1' ++ l3))%list as L end. { rewrite !checksum_split; eauto. exists 1. reflexivity. } rewrite L. clear L. rewrite checksum_split; eauto. rewrite checksum_split; eauto. match goal with | |- context [?a ^1+ (?b ^1+ ?c)] => assert (a ^1+ (b ^1+ c) = b ^1+ a ^1+ c) as L end. { rewrite <- !OneC_plus_assoc. rewrite OneC_plus_comm. rewrite <- !OneC_plus_assoc. f_equal. rewrite OneC_plus_comm. reflexivity. } rewrite L. clear L. rewrite <- !checksum_split; eauto. apply checksum_correct. rewrite !app_length. rewrite L'. simpl. exists (1+x). omega. simpl. exists 1. omega. simpl. exists 1. omega. all : destruct_conjs; simpl. all : repeat match goal with | |- padding (ByteString_enqueue_ByteString _ _) = _ => rewrite !padding_ByteString_enqueue_aligned_ByteString | |- padding (format_checksum _ _ _ _ _) = _ => unfold format_checksum; rewrite encode_word'_padding | _ => eauto using ByteString_mod_16_padding end. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.Strings.String Coq.Vectors.Vector Coq.ZArith.ZArith Fiat.Common.SumType Fiat.Common.EnumType Fiat.Common.BoundedLookup Fiat.Common.ilist Fiat.Computation Fiat.QueryStructure.Specification.Representation.Notations Fiat.QueryStructure.Specification.Representation.Heading Fiat.QueryStructure.Specification.Representation.Tuple Fiat.Narcissus.BinLib.AlignedByteString Fiat.Narcissus.BinLib.AlignWord Fiat.Narcissus.BinLib.AlignedList Fiat.Narcissus.BinLib.AlignedDecoders Fiat.Narcissus.BinLib.AlignedDecodeMonad Fiat.Narcissus.BinLib.AlignedEncodeMonad Fiat.Narcissus.Common.Specs Fiat.Narcissus.Common.WordFacts Fiat.Narcissus.Common.ComposeCheckSum Fiat.Narcissus.Common.ComposeIf Fiat.Narcissus.Common.ComposeOpt Fiat.Narcissus.Formats Fiat.Narcissus.BaseFormats Fiat.Narcissus.Stores.EmptyStore Bedrock.Word