proposition: Lemma AlignedDecodeBindEnumM sz {A} {len} : forall (t : Fin.t (S len) -> DecodeM (A * _) ByteString) (t' : Fin.t (S len) -> forall numBytes : nat, AlignedDecodeM A numBytes) (tb : Vector.t (word (sz * 8))%nat (S len)), (forall b2 : Fin.t (S len), DecodeMEquivAlignedDecodeM (t b2) (t' b2)) -> DecodeMEquivAlignedDecodeM (fun (v : ByteString) (cd : CacheDecode) => `(a, b0, cd') <- decode_enum tb v cd; t a b0 cd') (fun numBytes : nat => (b <- Aligned_decode_enumN sz tb numBytes; t' b numBytes)%AlignedDecodeM).
proof: Proof. unfold decode_enum, Aligned_decode_enum. intros; eapply DecodeMEquivAlignedDecodeM_trans. eapply Bind_DecodeMEquivAlignedDecodeM; [ eapply AlignedDecodeNCharM with (m := sz); intros; eauto | ]. Focus 2. { simpl; intros. unfold DecodeBindOpt2, DecodeBindOpt, BindOpt, If_Opt_Then_Else. destruct (decode_word b cd) as [ [ [? ?] ] | ]; eauto. higher_order_reflexivity. } all: idtac. Focus 2. { unfold AlignedDecodeMEquiv; simpl; intros. unfold Aligned_decode_enumN; simpl. unfold BindAlignedDecodeM. destruct (GetCurrentBytes sz v idx c) as [ [ [? ?] ] | ]; simpl; eauto. higher_order_reflexivity. } all: idtac. simpl. intros; destruct (word_indexed a tb); simpl; eauto. eapply AlignedDecode_Throw. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.ZArith.ZArith Coq.Strings.String Coq.Arith.Mult Coq.Vectors.Vector Fiat.Common.SumType Fiat.Common.BoundedLookup Fiat.Common.ilist Fiat.Common.DecideableEnsembles Fiat.Computation Fiat.QueryStructure.Specification.Representation.Notations Fiat.QueryStructure.Specification.Representation.Heading Fiat.QueryStructure.Specification.Representation.Tuple Fiat.Narcissus.BinLib.AlignedEncodeMonad Fiat.Narcissus.BinLib.AlignedByteString Fiat.Narcissus.BinLib.AlignWord Fiat.Narcissus.BinLib.AlignedString Fiat.Narcissus.BinLib.AlignedDecodeMonad Fiat.Narcissus.Common.Specs Fiat.Narcissus.Common.ComposeOpt Fiat.Narcissus.Formats.WordOpt Fiat.Narcissus.Formats.NatOpt Fiat.Narcissus.Formats.StringOpt Fiat.Narcissus.Formats.EnumOpt Fiat.Narcissus.Formats.FixListOpt Fiat.Narcissus.Formats.SumTypeOpt Fiat.Narcissus.Formats.EnumOpt Fiat.Narcissus.Formats.DomainNameOpt Fiat.Common.IterateBoundedIndex Fiat.Common.Tactics.CacheStringConstant Fiat.Narcissus.Formats.IPChecksum Fiat.Narcissus.Common.ComposeCheckSum Bedrock.Word