proposition: Lemma checksum_split : forall bs1 bs2, (exists x, length bs1 = 2 * x)%nat -> checksum (bs1 ++ bs2) = checksum bs1 ^1+ checksum bs2.
proof: Proof. fix IH 1. destruct bs1; intros. - reflexivity. - destruct bs1; destruct H; simpl in *. + omega. + rewrite IH. * unfold add_bytes_into_checksum, add_w16_into_checksum. rewrite <- !OneC_plus_assoc. f_equal. rewrite OneC_plus_comm. reflexivity. * exists (pred x). omega. Qed.
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 Permutation