proposition: Lemma Pseudo_Checksum_Valid_bounded {A} (srcAddr : ByteBuffer.t 4) (destAddr : ByteBuffer.t 4) (udpLength : word 16) protoCode (predicate : A -> Prop) (format_A format_B : FormatM A ByteString) (len_format_A : A -> nat) (len_format_A_OK : forall a' b ctx ctx', computes_to (format_A a' ctx) (b, ctx') -> length_ByteString b = len_format_A a') (len_format_B : A -> nat) (len_format_B_OK : forall a' b ctx ctx', computes_to (format_B a' ctx) (b, ctx') -> length_ByteString b = len_format_B a') (byte_aligned_A : forall a : A, len_format_A a mod 8 = 0) (byte_aligned_B : forall a : A, len_format_B a mod 8 = 0) : forall (data : A) (x : ByteString) (x0 : CacheFormat) (x1 : ByteString) (x2 : CacheFormat) (ext ext' : ByteString) (env : CacheFormat) (c : word 16), predicate data -> format_A data env ∋ (x, x0) -> format_B data (addE x0 16) ∋ (x1, x2) -> Pseudo_Checksum_Valid srcAddr destAddr udpLength protoCode (bin_measure (mappend x (mappend (format_checksum ByteString monoid ByteString_QueueMonoidOpt 16 c) x1))) (mappend (mappend x (mappend (format_checksum ByteString monoid ByteString_QueueMonoidOpt 16 c) x1)) ext) -> Pseudo_Checksum_Valid srcAddr destAddr udpLength protoCode (bin_measure (mappend x (mappend (format_checksum ByteString monoid ByteString_QueueMonoidOpt 16 c) x1))) (mappend (mappend x (mappend (format_checksum ByteString monoid ByteString_QueueMonoidOpt 16 c) x1)) ext').
proof: Proof. intros. unfold Pseudo_Checksum_Valid in *. revert H2. rewrite !ByteString2ListOfChar_Over; eauto. simpl; rewrite padding_eq_mod_8. rewrite !length_ByteString_enqueue_ByteString. rewrite Nat.add_mod by omega. apply len_format_A_OK in H0. apply len_format_B_OK in H1. unfold format_checksum; rewrite length_encode_word', measure_mempty. rewrite H0, byte_aligned_A, plus_O_n, NPeano.Nat.mod_mod, Nat.add_mod by omega. rewrite H1, byte_aligned_B, <- plus_n_O, NPeano.Nat.mod_mod by omega. reflexivity. simpl; rewrite padding_eq_mod_8. rewrite !length_ByteString_enqueue_ByteString. rewrite Nat.add_mod by omega. apply len_format_A_OK in H0. apply len_format_B_OK in H1. rewrite H0, byte_aligned_A, plus_O_n, NPeano.Nat.mod_mod, Nat.add_mod by omega. rewrite H1, byte_aligned_B, <- plus_n_O, NPeano.Nat.mod_mod by omega. unfold format_checksum; rewrite length_encode_word'; 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