proposition: Lemma Buffer_fold_left16_acc_oneC_plus : forall {sz} (packet: ByteBuffer.t sz) acc n, ByteBuffer_fold_left16 add_w16_into_checksum n packet acc = OneC_plus (ByteBuffer_fold_left16 add_w16_into_checksum n packet (wzero 16)) acc.
proof: Proof. fix IH 2. unfold ByteBuffer_fold_left16 in *. destruct packet as [ | hd sz [ | hd' sz' tl ] ]; intros; simpl. - destruct n as [ | [ | ] ]; reflexivity. - destruct n as [ | [ | ] ]; simpl; unfold add_bytes_into_checksum, add_w16_into_checksum; try rewrite OneC_plus_wzero_l, OneC_plus_comm; reflexivity. - destruct n as [ | [ | ] ]; simpl; unfold add_bytes_into_checksum, add_w16_into_checksum; try rewrite OneC_plus_wzero_l, OneC_plus_comm; try reflexivity. rewrite (IH _ tl (hd' +^+ hd ^1+ acc)). rewrite (IH _ tl (hd' +^+ hd)). 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