proposition: Lemma compose_PseudoChecksum_format_correct' {A} (srcAddr : ByteBuffer.t 4) (destAddr : ByteBuffer.t 4) (udpLength : word 16) protoCode (predicate : A -> Prop) (P : CacheDecode -> Prop) (P_inv : (CacheDecode -> Prop) -> Prop) (P_invM : (CacheDecode -> Prop) -> Prop) (format_A format_B : FormatM A ByteString) (subformat : FormatM A ByteString) (decode_measure : DecodeM (nat * _) _) (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') View_Predicate format_measure : cache_inv_Property P (fun P => P_inv P /\ P_invM P) -> (forall a, NPeano.modulo (len_format_A a) 8 = 0) -> (forall a, NPeano.modulo (len_format_B a) 8 = 0) -> forall decodeA : _ -> CacheDecode -> option (A * _ * CacheDecode), (cache_inv_Property P P_inv -> CorrectDecoder monoid predicate predicate eq (format_A ++ format_unused_word 16 ++ format_B)%format decodeA P (format_A ++ format_unused_word 16 ++ format_B)%format) -> (cache_inv_Property P P_invM -> CorrectRefinedDecoder monoid predicate View_Predicate (fun a n => len_format_A a + 16 + len_format_B a = n * 8) (format_A ++ format_unused_word 16 ++ format_B)%format subformat decode_measure P format_measure) -> (Prefix_Format _ (format_A ++ format_unused_word 16 ++ format_B) subformat)%format-> CorrectDecoder monoid predicate predicate eq (format_A ThenChecksum (Pseudo_Checksum_Valid srcAddr destAddr udpLength protoCode) OfSize 16 ThenCarryOn format_B) (fun (bin : _) (env : CacheDecode) => `(n, _, _) <- decode_measure bin env; if weqb (onesComplement (wzero 8 :: protoCode :: to_list srcAddr ++ to_list destAddr ++ to_list (splitLength udpLength) ++(ByteString2ListOfChar (n * 8) bin))%list) (wones 16) then decodeA bin env else None) P (format_A ThenChecksum (Pseudo_Checksum_Valid srcAddr destAddr udpLength protoCode) OfSize 16 ThenCarryOn format_B).
proof: Proof. intros. rename H4 into H4'; rename H3 into H4; rename H2 into H3. eapply format_decode_correct_alt. Focus 7. { eapply (composeChecksum_format_correct' A _ monoid _ 16 (Pseudo_Checksum_Valid srcAddr destAddr udpLength protoCode)). - eapply H. - 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_format_A a + 16 + len_format_B a = n). eapply H6. + 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 H5; intuition. intros. rewrite unfold_computes in H5; 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 H7; apply unfold_computes in H6. erewrite len_format_A_OK; eauto. erewrite (len_format_B_OK _ b0); eauto. unfold format_checksum; rewrite length_encode_word', measure_mempty. rewrite <- H2; omega. - eauto. - eapply Pseudo_Checksum_Valid_bounded; eauto. } 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 := fun (n : nat) a => weq (onesComplement (wzero 8 :: (protoCode :: to_list srcAddr ++ to_list destAddr ++ to_list (splitLength udpLength) ++ ByteString2ListOfChar n a)%list)) (wones 16)). unfold Compose_Decode. Local Opaque Nat.div. destruct (decode_measure a a0) as [ [ [? ?] ? ] | ]; simpl; eauto. symmetry. find_if_inside. eapply weqb_true_iff in e; rewrite e; eauto. destruct (weqb (add_bytes_into_checksum (wzero 8) protoCode (onesComplement (to_list srcAddr ++ to_list destAddr ++ split2 8 8 udpLength :: (split1 8 8 udpLength :: ByteString2ListOfChar (n * 8) a)%list))) WO~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1) eqn: ? ; eauto. eapply weqb_true_iff in Heqb0. congruence. 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