proposition: Lemma Start_CorrectAlignedDecoderFor {S : Type} Invariant FormatSpec (decoder decoder_opt : DecodeM (S * _) ByteString) (decoderM : forall sz, AlignedDecodeM S sz) (cache_inv : CacheDecode -> Prop) (P_inv : (CacheDecode -> Prop) -> Prop) (decoder_OK : cache_inv_Property cache_inv P_inv -> CorrectDecoder (S := S) _ Invariant Invariant eq FormatSpec decoder cache_inv FormatSpec) (cache_inv_OK : cache_inv_Property cache_inv P_inv) (decoder_opt_OK : forall b cd, decoder b cd = decoder_opt b cd) (monadized_decoder : DecodeMEquivAlignedDecodeM decoder_opt decoderM) : @CorrectAlignedDecoderFor S Invariant FormatSpec.
proof: Proof. exists decoderM. exists (decoder_opt, cache_inv); split. exists P_inv; split; simpl; eauto. unfold CorrectDecoder in *; intuition; intros. - destruct (H1 _ _ _ _ _ ext env_OK H0 H3 H4 ). rewrite decoder_opt_OK in H5; eauto. - rewrite <- decoder_opt_OK in H4; destruct (H2 _ _ _ _ _ _ H0 H3 H4); eauto. - rewrite <- decoder_opt_OK in H4; destruct (H2 _ _ _ _ _ _ H0 H3 H4); eauto. - apply monadized_decoder. Defined.
imports: Fiat.Common.Coq__8_4__8_5__Compat Bedrock.Word Coq.ZArith.ZArith Coq.NArith.NArith Coq.Arith.Arith Coq.Numbers.Natural.Peano.NPeano Coq.Logic.Eqdep_dec Fiat.Narcissus.Common.Specs Fiat.Narcissus.BinLib.Core Fiat.Narcissus.BinLib.AlignedByteString