proposition: Lemma CorrectDecodeEncode' {S T} {cache : Cache.Cache} {monoid : Monoid T} : forall Invariant (FormatSpec : Specs.FormatM S T) (encoder : Specs.CorrectEncoderFor FormatSpec) (decoder : Specs.CorrectDecoderFor Invariant FormatSpec), forall a envE envD b envE', Cache.Equiv envE envD -> Invariant a -> snd (proj1_sig decoder) envD -> projT1 encoder a envE = Some (b, envE') -> forall ext, exists envD', fst (proj1_sig decoder) (mappend b ext) envD = Some (a, ext, envD').
proof: Proof. intros. destruct encoder as [encoder encoder_OK]. destruct decoder as [decoder [Inv [decoder_OK Inv_cd] ] ]; simpl in *. specialize (proj1 (encoder_OK a envE) _ H2); intro. specialize (decoder_OK Inv_cd). destruct decoder_OK as [decoder_OK _]. unfold Specs.cache_inv_Property in Inv_cd. eapply decoder_OK with (ext := ext) in H3; eauto. destruct H3 as [? [? ?] ]; intuition. subst; eauto. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Fiat.Narcissus.Common.Monoid Bedrock.Word Fiat.Narcissus.BinLib.AlignedByteString Fiat.Narcissus.BinLib.AlignedByteBuffer Fiat.Narcissus.BinLib.AlignWord Fiat.Narcissus.BinLib.AlignedList Fiat.Narcissus.BinLib.AlignedDecoders Fiat.Narcissus.BinLib.AlignedDecodeMonad Fiat.Narcissus.BinLib.AlignedEncodeMonad Fiat.Narcissus.BinLib.AlignedIPChecksum