proposition: Lemma AlignedFormatListThenC {A} (A_OK : A -> Prop) format_A (encode_A : A -> CacheFormat -> {n : nat & t (word 8) n} * CacheFormat) : forall (l : list A) ce (c : _ -> Comp _) (v' : _ -> {n : nat & t (word 8) n}) (ce' : _ -> CacheFormat), (forall (a : A) (ce : CacheFormat), A_OK a -> refine (format_A a ce) (ret (let (v', ce') := encode_A a ce in (build_aligned_ByteString (projT2 v'), ce')))) -> (forall v ce'', format_list format_A l ce ↝ (v, ce'') -> refine (c ce'') (ret (build_aligned_ByteString (projT2 (v' ce'')), ce' ce''))) -> (forall a : A, In a l -> A_OK a) -> refine (((format_list format_A l) ThenC c) ce) (ret (let (v, ce'') := align_format_list encode_A l ce in build_aligned_ByteString (Vector.append (projT2 v) (projT2 (v' ce''))), let (v, ce'') := align_format_list encode_A l ce in ce' ce'')).
proof: Proof. intros. etransitivity. eapply AlignedFormatThenC. rewrite (optimize_align_format_list A_OK format_A encode_A); try eassumption. match goal with |- context [let (v, c) := ?z in ret (@?b v c)] => rewrite (zeta_inside_ret z _) end. rewrite zeta_to_fst; simpl. instantiate (2 := fun ce => fst (_ ce)). instantiate (1 := fun ce => snd (_ ce)). simpl; reflexivity. intros; eapply H0; eauto. simpl. rewrite !zeta_to_fst; simpl; reflexivity. 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