proposition: Lemma AlignedDecodeBind3CharM: (forall (cd : CacheDecode) (n m : nat), addD (addD cd n) m = addD cd (n + m)) -> forall (C : Type) (t : word 24 -> DecodeM (C * _) ByteString) (t' : word 24 -> forall numBytes : nat, AlignedDecodeM C numBytes), (forall b : word 24, DecodeMEquivAlignedDecodeM (t b) (t' b)) -> DecodeMEquivAlignedDecodeM (fun (v : ByteString) (cd : CacheDecode) => `(a, b0, cd') <- decode_word v cd; t a b0 cd') (fun numBytes : nat => (b1 <- GetCurrentByte; b2 <- GetCurrentByte; b3 <- GetCurrentByte; w <- return (Core.append_word b3 (Core.append_word b2 b1)); t' w numBytes)%AlignedDecodeM).
proof: Proof. intros; eapply DecodeMEquivAlignedDecodeM_trans. - eapply AlignedDecodeBindCharM; intros. eapply AlignedDecodeBindCharM; intros. eapply AlignedDecodeBindCharM; intros. eapply H0. - simpl; intros. unfold decode_word; rewrite (decode_word_plus' 8 16). unfold DecodeBindOpt2, DecodeBindOpt, BindOpt, If_Opt_Then_Else. destruct (decode_word' 8 b) as [ [? ?] | ]; eauto. unfold decode_word; rewrite (decode_word_plus' 8 8). unfold DecodeBindOpt2, DecodeBindOpt, BindOpt, If_Opt_Then_Else. destruct (decode_word' 8 b0) as [ [? ?] | ]; eauto. destruct (decode_word' 8 b1) as [ [? ?] | ]; eauto. rewrite !addD_addD_plus; simpl plus. higher_order_reflexivity. - intros; reflexivity. 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