proposition: Lemma pseudoHeader_checksum'_ok : forall (srcAddr : ByteBuffer.t 4) (destAddr : ByteBuffer.t 4) (measure : nat) (udpLength : word 16) (protoCode : word 8) {sz} (packet: ByteBuffer.t sz), pseudoHeader_checksum srcAddr destAddr measure udpLength protoCode packet = pseudoHeader_checksum' srcAddr destAddr measure udpLength protoCode packet.
proof: Proof. unfold pseudoHeader_checksum, pseudoHeader_checksum'. intros. repeat explode_vector. Opaque split1. Opaque split2. simpl in *. unfold ByteBuffer_checksum, InternetChecksum.ByteBuffer_checksum_bound, add_w16_into_checksum, add_bytes_into_checksum, ByteBuffer_fold_left16, ByteBuffer_fold_left_pair. fold @ByteBuffer_fold_left_pair. setoid_rewrite Buffer_fold_left16_acc_oneC_plus. rewrite combine_split. rewrite !OneC_plus_wzero_r, !OneC_plus_wzero_l, OneC_plus_comm. repeat (f_equal; [ ]). rewrite <- !OneC_plus_assoc. 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