proposition: Lemma checksum_correct : forall bytes, let chk := checksum bytes in let neg := wnot chk in checksum ((hi8 neg) :: (lo8 neg) :: bytes) = wones _.
proof: Proof. repeat match goal with | _ => progress intros | _ => progress unfold lo8, hi8, add_bytes_into_checksum | _ => progress (unfold checksum; fold checksum) | _ => rewrite combine_split | [ H := _ |- _ ] => unfold H in *; clear H | _ => eauto using OneC_plus_wnot end. 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