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) (P_invM : (CacheDecode -> Prop) -> Prop) (decodeChecksum := decode_IPChecksum), cache_inv_Property P (fun P => P_inv P /\ P_invM P) -> forall (predicate : A -> Prop) (format1 : FormatM A B) (format2 : FormatM A B) (subformat : FormatM A B) (format_measure : FormatM nat B) (decode_measure : DecodeM (nat * B) B) (len_format1 : A -> nat) (len_format2 : A -> nat) View_Predicate, (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 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) -> (cache_inv_Property P P_invM -> CorrectRefinedDecoder monoid predicate View_Predicate (fun a n => len_format1 a + 16 + len_format2 a = n * 8) (format1 ++ format_unused_word 16 ++ format2)%format subformat decode_measure P format_measure)%format -> (Prefix_Format _ (format1 ++ format_unused_word 16 ++ format2) subformat)%format -> CorrectDecoder monoid predicate predicate eq (format1 ThenChecksum IPChecksum_Valid OfSize 16 ThenCarryOn format2) (fun (bin : B) (env : CacheDecode) => `(n, _, _) <- decode_measure bin env; if checksum_Valid_dec (n * 8) bin then decodeA bin env else None) P (format1 ThenChecksum IPChecksum_Valid OfSize 16 ThenCarryOn format2).
proof: Proof. intros. eapply format_decode_correct_alt. Focus 7. { eapply (composeChecksum_format_correct' A _ monoid _ 16 IPChecksum_Valid). - eapply H. - rename H6 into H4'; rename H5 into H6; rename H4 into H5; rename H6 into H4. specialize (H4 (proj2 H)). split. 2: eauto. eapply injection_decode_correct with (inj := fun n => mult n 8). 4: simpl. eapply H4. + intros. instantiate (1 := fun a n => len_format1 a + 16 + len_format2 a = n). eapply H8. + intros; instantiate (1 := fun v => View_Predicate (Nat.div v 8)). cbv beta. rewrite Nat.div_mul; eauto. + intros; apply unfold_computes; intros. split. 2: rewrite unfold_computes in H11; intuition. intros. rewrite unfold_computes in H11; intuition. instantiate (1 := fun v env t => format_measure (Nat.div v 8) env t). cbv beta; rewrite Nat.div_mul; eauto. - simpl; intros. destruct t1; destruct t2; simpl fst in *; simpl snd in *. apply unfold_computes in H8; apply unfold_computes in H9. erewrite H0; eauto. apply unfold_computes in H10; erewrite (H1 _ b0); eauto. unfold format_checksum; rewrite length_encode_word', measure_mempty. rewrite <- H7; omega. - eauto. - unfold IPChecksum_Valid in *; intros; simpl. rewrite ByteString2ListOfChar_Over. * rewrite ByteString2ListOfChar_Over in H10. eauto. simpl. apply H0 in H8. pose proof (H2 data). rewrite <- H8 in H11. rewrite !ByteString_enqueue_ByteString_padding_eq. rewrite padding_eq_mod_8, H11. pose proof (H3 data). unfold format_checksum. rewrite encode_word'_padding. rewrite <- (H1 _ _ _ _ H9) in H12. rewrite padding_eq_mod_8, H12. reflexivity. * rewrite !ByteString_enqueue_ByteString_padding_eq. apply H0 in H8. pose proof (H2 data). rewrite <- H8 in H11. rewrite padding_eq_mod_8, H11. pose proof (H3 data). unfold format_checksum. rewrite encode_word'_padding. rewrite <- (H1 _ _ _ _ H9) in H12. rewrite padding_eq_mod_8, H12. reflexivity. } all: try unfold flip, pointwise_relation, impl; intuition eauto using EquivFormat_reflexive. all: try unfold flip, pointwise_relation, impl; intuition eauto using EquivFormat_reflexive. instantiate (1 := IPChecksum_Valid_dec). unfold Compose_Decode. destruct (decode_measure a a0) as [ [ [? ?] ? ] | ]; simpl; eauto. unfold flip, pointwise_relation, checksum_Valid_dec; intros. destruct (IPChecksum_Valid_dec (n * 8) a); unfold IPChecksum_Valid, IPChecksum_Valid_check in *. + rewrite i, (proj2 (weqb_true_iff _ _)); eauto. + destruct (weqb (onesComplement (ByteString2ListOfChar (n * 8) a)) (wones 16)) eqn: ?; eauto. apply weqb_sound in Heqb0; congruence. 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