proposition: Lemma InternetChecksum_To_ByteBuffer_Checksum': forall (sz m : nat) (v : t Core.char sz), checksum (ByteString2ListOfChar (m * 8) (build_aligned_ByteString v)) = ByteBuffer_checksum_bound m v.
proof: Proof. intros. assert ((exists m', m = 2 * m') \/ (exists m', m = S (2 * m'))). { induction m; eauto. destruct IHm; destruct_ex; subst; eauto. left; exists (S x); omega. } destruct H as [ [? ?] | [? ?] ]; subst. - rewrite (mult_comm 2). apply InternetChecksum_To_ByteBuffer_Checksum. - revert sz v. induction x. + intros; destruct v. * reflexivity. * rewrite dequeue_byte_ByteString2ListOfChar. reflexivity. + intros; destruct v. * replace (S (2 * S x)) with ((S (S (S (2 * x))))) by omega. rewrite ByteString2ListOfChar_overflow. rewrite ByteString2ListOfChar_overflow. unfold checksum; fold checksum. rewrite IHx. unfold ByteBuffer_checksum_bound, ByteBuffer_fold_left16. simpl. destruct (2 * x); eauto. * rewrite dequeue_byte_ByteString2ListOfChar. destruct v. replace (2 * S x * 8) with ((S (S (2 * x))) * 8) by omega. rewrite ByteString2ListOfChar_overflow. unfold checksum; fold checksum. rewrite IHx. rewrite <- !ByteBuffer_checksum_bound_ok. simpl. destruct (2 * x); eauto. replace (2 * S x * 8) with ((S (S (2 * x))) * 8) by omega. rewrite dequeue_byte_ByteString2ListOfChar. replace (checksum (h :: (h0 :: ByteString2ListOfChar (S (2 * x) * 8) (build_aligned_ByteString v))%list)) with (add_bytes_into_checksum h h0 (checksum (ByteString2ListOfChar (S (2 * x) * 8) (build_aligned_ByteString v))%list)) by reflexivity. rewrite IHx. rewrite <- !ByteBuffer_checksum_bound_ok. replace (2 * S x) with (S (S ( 2 * x))) by omega. rewrite <- Vector_checksum_bound_acc; reflexivity. 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