proposition: Lemma compose_IPChecksum_format_correct : forall (A : Type) (B := ByteString) (trans : Monoid B := monoid) (trans_opt : QueueMonoidOpt trans bool := ByteString_QueueMonoidOpt) (calculate_checksum := IPChecksum) (checksum_Valid := IPChecksum_Valid) (checksum_Valid_dec := IPChecksum_Valid_check) (P : CacheDecode -> Prop) (P_inv : (CacheDecode -> Prop) -> Prop) (decodeChecksum := decode_IPChecksum), cache_inv_Property P P_inv -> forall (predicate : A -> Prop) (format1 : A -> CacheFormat -> Comp (B * CacheFormat)) (format2 : A -> CacheFormat -> Comp (B * CacheFormat)) (formatd_A_measure : B -> nat) (len_format1 : A -> nat) (len_format2 : A -> nat), (forall a' b ctx ctx', computes_to (format1 a' ctx) (b, ctx') -> length_ByteString b = len_format1 a') -> (forall a b ctx ctx', computes_to (format2 a ctx) (b, ctx') -> length_ByteString b = len_format2 a) -> (forall a, NPeano.modulo (len_format1 a) 8 = 0) -> (forall a, NPeano.modulo (len_format2 a) 8 = 0) -> (forall (a : A) (ctx ctx' ctx'' : CacheFormat) c (b b'' ext : B), format1 a ctx ↝ (b, ctx') -> format2 a ctx' ↝ (b'', ctx'') -> predicate a -> len_format1 a + len_format2 a + 16 = formatd_A_measure (mappend (mappend b (mappend (format_checksum _ _ _ 16 c) b'')) ext)) -> forall decodeA : B -> CacheDecode -> option (A * B * CacheDecode), (cache_inv_Property P P_inv -> CorrectDecoder monoid predicate predicate eq (format1 ++ format_unused_word 16 ++ format2)%format decodeA P (format1 ++ format_unused_word 16 ++ format2)%format) -> CorrectDecoder monoid predicate predicate eq (format1 ThenChecksum IPChecksum_Valid OfSize 16 ThenCarryOn format2) (fun (bin : B) (env : CacheDecode) => if checksum_Valid_dec (formatd_A_measure bin) bin then decodeA bin env else None) P (format1 ThenChecksum IPChecksum_Valid OfSize 16 ThenCarryOn format2).
proof: Proof. intros. eapply format_decode_correct_EquivDecoder_Proper with (x := fun bin env => if IPChecksum_Valid_dec (formatd_A_measure bin) bin then decodeA bin env else None). - unfold flip, pointwise_relation, checksum_Valid_dec; intros. destruct (IPChecksum_Valid_dec (formatd_A_measure a)); unfold IPChecksum_Valid, IPChecksum_Valid_check in *. + rewrite i, (proj2 (weqb_true_iff _ _)); eauto. + destruct (weqb (onesComplement (ByteString2ListOfChar (formatd_A_measure a) a)) (wones 16)) eqn: ?; eauto. apply weqb_sound in Heqb; congruence. - eapply composeChecksum_format_correct; eauto. + intros; rewrite !mappend_measure. simpl; rewrite (H0 _ _ _ _ H6). simpl; rewrite (H1 _ _ _ _ H7). erewrite <- H4; eauto; try omega. unfold format_checksum. rewrite length_encode_word'. simpl; omega. + unfold IPChecksum_Valid in *; intros; simpl. rewrite ByteString2ListOfChar_Over. * rewrite ByteString2ListOfChar_Over in H9. eauto. simpl. apply H0 in H7. pose proof (H2 data). rewrite <- H7 in H10. rewrite !ByteString_enqueue_ByteString_padding_eq. rewrite padding_eq_mod_8, H10. pose proof (H3 data). unfold format_checksum. rewrite encode_word'_padding. rewrite <- (H1 _ _ _ _ H8) in H11. rewrite padding_eq_mod_8, H11. reflexivity. * rewrite !ByteString_enqueue_ByteString_padding_eq. apply H0 in H7. pose proof (H2 data). rewrite <- H7 in H10. rewrite padding_eq_mod_8, H10. pose proof (H3 data). unfold format_checksum. rewrite encode_word'_padding. rewrite <- (H1 _ _ _ _ H8) in H11. rewrite padding_eq_mod_8, H11. reflexivity. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.ZArith.ZArith Coq.Strings.String Coq.Vectors.Vector 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.Core Fiat.Narcissus.BinLib.AlignedByteString Fiat.Narcissus.Common.Specs Fiat.Narcissus.Common.WordFacts Fiat.Narcissus.Common.ComposeCheckSum Fiat.Narcissus.Common.ComposeIf Fiat.Narcissus.Common.ComposeOpt Fiat.Narcissus.Formats.Option Fiat.Narcissus.Formats.FixListOpt Fiat.Narcissus.Stores.EmptyStore Fiat.Narcissus.Formats.Bool Fiat.Narcissus.Formats.NatOpt Fiat.Narcissus.Formats.Vector Fiat.Narcissus.Formats.EnumOpt Fiat.Narcissus.Formats.SumTypeOpt Fiat.Narcissus.Formats.InternetChecksum Fiat.Narcissus.Formats.WordOpt Fiat.Narcissus.BaseFormats Bedrock.Word