proposition: Lemma format_string_ByteString : forall (s : string) (ce : CacheFormat), refine (FixStringOpt.format_string s ce) (ret (build_aligned_ByteString (StringToBytes s), addE ce (8 * String.length s))).
proof: Proof. induction s; intros; simpl. - f_equiv. f_equal. eapply ByteString_f_equal. instantiate (1 := eq_refl _); reflexivity. instantiate (1 := eq_refl _); reflexivity. - unfold AsciiOpt.format_ascii. unfold Bind2; setoid_rewrite aligned_format_char_eq. simplify with monad laws. rewrite IHs. simplify with monad laws. simpl. rewrite <- build_aligned_ByteString_append; simpl. rewrite !addE_addE_plus. f_equiv; f_equiv; f_equiv; omega. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.ZArith.ZArith Coq.Strings.Ascii Coq.Strings.String Coq.Arith.Mult Coq.Vectors.Vector Fiat.Common.SumType Fiat.Common.BoundedLookup Fiat.Common.ilist Fiat.Common.DecideableEnsembles Fiat.Computation Fiat.Narcissus.Common.Specs Fiat.Narcissus.Common.ComposeOpt Fiat.Narcissus.Formats.FixStringOpt Fiat.Narcissus.Formats.StringOpt Fiat.Narcissus.Formats.EnumOpt Fiat.Narcissus.Formats.FixListOpt Fiat.Narcissus.Formats.SumTypeOpt Fiat.Narcissus.Formats.AsciiOpt Fiat.Narcissus.BinLib.AlignedByteString Fiat.Narcissus.BinLib.AlignWord Fiat.Common.IterateBoundedIndex Fiat.Common.Tactics.CacheStringConstant Bedrock.Word