proposition: Lemma optimize_align_format_list {A} (A_OK : A -> Prop) (format_A : A -> CacheFormat -> Comp (ByteString * CacheFormat)) (A_format_align : A -> CacheFormat -> {n : _ & ByteBuffer.t n} * CacheFormat) (A_format_OK : forall a ce, A_OK a -> refine (format_A a ce) (ret (let (v', ce') := A_format_align a ce in (build_aligned_ByteString (projT2 v'), ce')))) : forall (As : list A) (ce : CacheFormat), (forall a, In a As -> A_OK a) -> refine (format_list format_A As ce) (let (v', ce') := (align_format_list A_format_align As ce) in ret (build_aligned_ByteString (projT2 v'), ce')).
proof: Proof. induction As; simpl; intros; simpl. - simpl. repeat f_equiv. eapply ByteString_f_equal. instantiate (1 := eq_refl _); reflexivity. instantiate (1 := eq_refl _); reflexivity. - unfold Bind2. rewrite A_format_OK; eauto; simplify with monad laws. rewrite IHAs. destruct (A_format_align a ce); simpl. destruct (align_format_list A_format_align As c); simplify with monad laws. simpl. rewrite <- build_aligned_ByteString_append. reflexivity. intuition. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.Strings.String Coq.Arith.Mult Coq.Vectors.Vector Fiat.Common.SumType Fiat.Common.BoundedLookup Fiat.Common.ilist Fiat.Common.DecideableEnsembles Fiat.Common.IterateBoundedIndex Fiat.Common.Tactics.CacheStringConstant Fiat.Computation 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.DomainNameOpt Fiat.Narcissus.Formats.Vector Fiat.Narcissus.BinLib.AlignedByteString Fiat.Narcissus.BinLib.AlignWord Fiat.Narcissus.BinLib.AlignedDecoders Fiat.Narcissus.BinLib.AlignedEncodeMonad Fiat.Narcissus.BinLib.AlignedDecodeMonad Fiat.Narcissus.BaseFormats Bedrock.Word