proposition: Lemma aligned_Pseudo_checksum_OK_1 (srcAddr : ByteBuffer.t 4) (destAddr : ByteBuffer.t 4) (pktlength : word 16) id measure {sz} : forall (v : t Core.char sz), weqb (InternetChecksum.add_bytes_into_checksum (wzero 8) id (onesComplement(to_list srcAddr ++ to_list destAddr ++ split2 8 8 pktlength :: split1 8 8 pktlength :: (ByteString2ListOfChar (measure * 8) (build_aligned_ByteString v)))%list)) WO~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1 = aligned_Pseudo_checksum srcAddr destAddr pktlength id measure v 0.
proof: Proof. simpl; intros. unfold onesComplement. rewrite <- pseudoHeader_checksum'_ok. rewrite checksum_eq_Vector_checksum. unfold pseudoHeader_checksum. rewrite <- ByteBuffer_checksum_bound_ok. unfold ByteBuffer.t in *. simpl. replace srcAddr with (Vector.hd srcAddr :: Vector.hd (Vector.tl srcAddr) :: Vector.hd (Vector.tl (Vector.tl srcAddr)) :: Vector.hd (Vector.tl (Vector.tl (Vector.tl srcAddr))) :: (@Vector.nil _)) by abstract (pattern srcAddr; repeat (apply caseS'; let t' := fresh in intros ? t'; pattern t'); apply case0; reflexivity). replace destAddr with (Vector.hd destAddr :: Vector.hd (Vector.tl destAddr) :: Vector.hd (Vector.tl (Vector.tl destAddr)) :: Vector.hd (Vector.tl (Vector.tl (Vector.tl destAddr))) :: (@Vector.nil _)) by abstract (pattern destAddr; repeat (apply caseS'; let t' := fresh in intros ? t'; pattern t'); apply case0; reflexivity). simpl. repeat rewrite Vector_checksum_bound_acc. rewrite <- checksum_eq_Vector_checksum. f_equal. rewrite ByteBuffer_checksum_bound_ok. repeat rewrite (add_bytes_into_checksum_swap _ id); f_equal. repeat rewrite (add_bytes_into_checksum_swap _ (Vector.hd (Vector.tl srcAddr))); f_equal. repeat rewrite (add_bytes_into_checksum_swap _ (Vector.hd (Vector.tl (Vector.tl (Vector.tl srcAddr))))); f_equal. repeat rewrite (add_bytes_into_checksum_swap _ (Vector.hd (Vector.tl destAddr))); f_equal. repeat rewrite (add_bytes_into_checksum_swap _ (Vector.hd (Vector.tl (Vector.tl (Vector.tl destAddr))))); f_equal. f_equal. apply InternetChecksum_To_ByteBuffer_Checksum'. 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