proposition: Lemma AlignedFormat32Char {numBytes} : forall (w : word 32) ce ce' (c : _ -> Comp _) (v : Vector.t _ numBytes), refine (c (addE ce 32)) (ret (build_aligned_ByteString v, ce')) -> refine (((format_word (monoidUnit := ByteString_QueueMonoidOpt) w) ThenC c) ce) (ret (build_aligned_ByteString (Vector.cons _ (split2 24 8 w) _ (Vector.cons _ (split2 16 8 (split1 24 8 w)) _ (Vector.cons _ (split2 8 8 (split1 16 16 w)) _ (Vector.cons _ (split1 8 24 w) _ v)))), ce')).
proof: Proof. unfold compose, Bind2; intros. intros; setoid_rewrite (@format_words _ _ 8 24 addE_addE_plus w). rewrite (@AlignedFormatChar _ _ 3). simplify with monad laws. unfold snd. rewrite H. simplify with monad laws. unfold fst. unfold mappend. unfold ByteStringQueueMonoid. rewrite <- build_aligned_ByteString_append. instantiate (1 := Vector.cons _ _ _ (Vector.cons _ _ _ (Vector.cons _ _ _ (Vector.nil _)))). unfold append. reflexivity. setoid_rewrite (@format_words _ _ 8 16 addE_addE_plus _). rewrite (@AlignedFormatChar _ _ 2). reflexivity. setoid_rewrite (@format_words _ _ 8 8). rewrite (@AlignedFormatChar _ _ 1) by apply aligned_format_char_eq. rewrite !addE_addE_plus; simpl plus. f_equiv. eauto. 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