proposition: Lemma AlignedFormatThenC : forall ce (c1 : _ -> Comp _) (c2 : _ -> Comp _) (v1 : _ -> {n : nat & t (word 8) n}) (v2 : _ -> {n : nat & t (word 8) n}) (ce2 : _ -> CacheFormat) (ce1 : _ -> CacheFormat), refine (c1 ce) (ret (build_aligned_ByteString (projT2 (v1 ce)), (ce1 ce))) -> (forall v ce', computes_to (c1 ce) (v, ce') -> refine (c2 ce') (ret (build_aligned_ByteString (projT2 (v2 ce')), (ce2 ce')))) -> refine ((c1 ThenC c2) ce) (ret (build_aligned_ByteString (Vector.append (projT2 (v1 ce)) (projT2 (v2 (ce1 ce)))), (ce2 (ce1 ce)))).
proof: Proof. unfold compose; intros. unfold Bind2. etransitivity. apply refine_under_bind_both; eauto. intros [? ?] ?. rewrite H0; try eassumption. simplify with monad laws. simpl. instantiate (1 := fun bc => ret (ByteString_enqueue_ByteString (fst bc) (build_aligned_ByteString (projT2 (v2 (snd bc)))), ce2 (snd bc))); simpl. reflexivity. simplify with monad laws. simpl. rewrite <- build_aligned_ByteString_append. 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