fact: Fixpoint Vector_checksum {sz} (bytes: ByteBuffer.t sz) : W16 := match bytes with | @Vector.nil _ => wzero _ | @Vector.cons _ x _ (@Vector.nil _) => add_bytes_into_checksum x (wzero _) (wzero _) | @Vector.cons _ x _ (@Vector.cons _ y _ t) => add_bytes_into_checksum x y (Vector_checksum t) end.
imports: Fiat.Common.Coq__8_4__8_5__Compat List Bedrock.Word Coq.ZArith.ZArith Coq.micromega.Psatz NArith NArithRing ZArith ZArithRing Program Coq.micromega.Psatz AlignedByteString