proposition: Lemma computes_to_compose_proj_decode_unused_word {S} : forall s sz (f : S -> word sz) (ctx ctx'' : CacheFormat) (rest : CacheFormat -> Comp (ByteString * CacheFormat)) (b : ByteString), computes_to ((((WordOpt.format_word ◦ f) s) ThenC rest) ctx) (b, ctx'') -> exists b' ctx', computes_to (rest ctx') (b', ctx'') /\ forall ext, decode_unused_word' sz (mappend b ext) = Some ((), mappend b' ext).
proof: Proof. unfold composeChecksum, compose, Bind2; intros; computes_to_inv; injections. eapply EquivFormat_Projection_Format in H. unfold format_word in *; computes_to_inv; subst. destruct v0; simpl in *; do 2 eexists; repeat split; eauto. unfold decode_unused_word'; intros. rewrite <- !ByteString_enqueue_ByteString_assoc. pose proof (monoid_dequeue_encode_word' (T := ByteString)) as H''; simpl in H''. intros; rewrite H''; reflexivity. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.ZArith.ZArith Coq.Strings.String Coq.Vectors.Vector 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.Core Fiat.Narcissus.BinLib.AlignedByteString Fiat.Narcissus.Common.Specs Fiat.Narcissus.Common.WordFacts Fiat.Narcissus.Common.ComposeCheckSum Fiat.Narcissus.Common.ComposeIf Fiat.Narcissus.Common.ComposeOpt Fiat.Narcissus.Formats.Option Fiat.Narcissus.Formats.FixListOpt Fiat.Narcissus.Stores.EmptyStore Fiat.Narcissus.Formats.Bool Fiat.Narcissus.Formats.NatOpt Fiat.Narcissus.Formats.Vector Fiat.Narcissus.Formats.EnumOpt Fiat.Narcissus.Formats.SumTypeOpt Fiat.Narcissus.Formats.InternetChecksum Fiat.Narcissus.Formats.WordOpt Fiat.Narcissus.BaseFormats Bedrock.Word