proposition: Lemma optimize_align_decode_list {A} (A_decode : ByteString -> CacheDecode -> option (A * ByteString * CacheDecode)) (A_decode_align : forall n, ByteBuffer.t n -> CacheDecode -> option (A * {n : _ & Vector.t _ n} * CacheDecode)) (A_decode_OK : forall n (v : Vector.t _ n) cd, A_decode (build_aligned_ByteString v) cd = Ifopt A_decode_align n v cd as a Then Some (fst (fst a), build_aligned_ByteString (projT2 (snd (fst a))), snd a) Else None) : forall (n : nat) {sz} (v : ByteBuffer.t sz) (cd : CacheDecode), decode_list A_decode n (build_aligned_ByteString v) cd = Ifopt align_decode_list A_decode_align n v cd as a Then Some (fst (fst a), build_aligned_ByteString (projT2 (snd (fst a))), snd a) Else None.
proof: Proof. induction n; simpl; intros; eauto. rewrite A_decode_OK. rewrite (If_Opt_Then_Else_DecodeBindOpt). destruct (A_decode_align sz v cd) as [ [ [? [? ?] ] ?] | ]; simpl; eauto. rewrite IHn. rewrite (If_Opt_Then_Else_DecodeBindOpt). destruct (align_decode_list A_decode_align n t c) as [ [ [? [? ?] ] ?] | ]; simpl; eauto. 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