proposition: Lemma AlignedDecodeByteBufferM {C : Type} (n : nat) : forall (t : { n : _ & ByteBuffer.t n } -> DecodeM (C * _) ByteString) (t' : { n : _ & ByteBuffer.t n } -> forall {numBytes}, AlignedDecodeM C numBytes), (forall b, DecodeMEquivAlignedDecodeM (t b) (@t' b)) -> DecodeMEquivAlignedDecodeM (fun v cd => `(b, bs, cd') <- decode_bytebuffer n v cd; t b bs cd') (fun numBytes => b <- ByteBufferAlignedDecodeM n; t' b)%AlignedDecodeM%list.
proof: Proof. intros. eapply DecodeMEquivAlignedDecodeM_trans with (bit_decoder1 := (fun v cd => `(l, bs, cd') <- decode_list decode_word n v cd; t (existT ByteBuffer.t _ (ByteBuffer.of_list l)) bs cd')) (byte_decoder1 := (fun numBytes => l <- ListAlignedDecodeM (fun numBytes : nat => GetCurrentByte) n; fun v idx cd => if (Coq.Init.Nat.leb idx numBytes) then t' (existT ByteBuffer.t _ (ByteBuffer.of_list l)) _ v idx cd else None )%AlignedDecodeM%list). - eapply AlignedDecodeListM; eauto using AlignedDecodeCharM. intros; repeat (eapply conj; intros). + simpl; destruct (Coq.Init.Nat.leb n0 (numBytes_hd)) eqn: ? ; repeat apply_in_hyp Compare_dec.leb_complete; repeat apply_in_hyp Compare_dec.leb_complete_conv; try Omega.omega; simpl; eauto. pattern numBytes_hd, v; apply caseS; simpl; intros. rewrite (proj1 (H _)); reflexivity. + eapply H in H0; eauto. + rewrite (proj1 (proj2 (proj2 (H _)) _ _ _)) in H0; rewrite H0; find_if_inside; reflexivity. + destruct (Coq.Init.Nat.leb 0 n0) eqn: ? ; repeat apply_in_hyp Compare_dec.leb_complete; repeat apply_in_hyp Compare_dec.leb_complete_conv; try Omega.omega; simpl; eauto. apply (proj2 (proj2 (H _)) _ _ _) in H0; eauto. + destruct (Coq.Init.Nat.leb 0 n0) eqn: ? ; repeat apply_in_hyp Compare_dec.leb_complete; repeat apply_in_hyp Compare_dec.leb_complete_conv; try Omega.omega; simpl; eauto. eapply H; eauto. + eapply H; eauto. - clear t' H; revert t; induction n; simpl; intros. + reflexivity. + unfold decode_bytebuffer. destruct (decode_Vector decode_word (S n) b cd) as [ [ [? ?] ? ] | ] eqn: ?; simpl. * unfold decode_Vector in Heqo. destruct (decode_word b cd) as [ [ [? ?] ?] | ]; simpl in *; eauto; try discriminate. fold (decode_Vector (decode_word (sz := 8)) n b1 c0) in Heqo. rewrite DecodeBindOpt2_assoc; simpl. erewrite IHn with (t := fun l => t (existT ByteBuffer.t _ (ByteBuffer.cons w (projT2 l)))). unfold decode_bytebuffer. destruct (decode_Vector decode_word n b1 c0) as [ [ [? ?] ?] | ]; simpl in *; eauto; try discriminate. injections. reflexivity. * unfold decode_Vector in Heqo. destruct (decode_word b cd) as [ [ [? ?] ?] | ]; simpl in *; eauto; try discriminate. fold (decode_Vector (decode_word (sz := 8)) n b0 c) in Heqo. rewrite DecodeBindOpt2_assoc; simpl. erewrite IHn with (t := fun l => t (existT ByteBuffer.t _ (ByteBuffer.cons w (projT2 l)))). unfold decode_bytebuffer. destruct (decode_Vector decode_word n b0 c) as [ [ [? ?] ?] | ]; simpl in *; eauto; try discriminate. - intros n0 v idx; generalize t'; revert addD_addD_plus addD_0 n0 idx v. clear; induction n; simpl; intros. + eapply AlignedDecodeMEquiv_trans. eapply ReturnAlignedDecodeM_LeftUnit. unfold AlignedDecodeMEquiv, ByteBufferAlignedDecodeM, BindAlignedDecodeM; simpl; intros. rewrite <- plus_n_O; find_if_inside; simpl; eauto. unfold bytebuffer_of_bytebuffer_range; simpl. simpl; rewrite addD_0; reflexivity. + eapply AlignedDecodeMEquiv_trans. eapply BindAlignedDecodeM_assoc. eapply AlignedDecodeMEquiv_trans. { instantiate (1 := (a <- GetCurrentByte; l <- ListAlignedDecodeM (fun numBytes : nat => GetCurrentByte) n; (fun (v0 : ByteBuffer.t n0) (idx0 : nat) (cd : CacheDecode) => if Coq.Init.Nat.leb idx0 n0 then t' (existT ByteBuffer.t (| (a :: l) |) (ByteBuffer.of_list (a :: l))) n0 v0 idx0 cd else None))%AlignedDecodeM). intros ? ? ?; f_equal; apply functional_extensionality; intros. unfold AlignedDecodeMEquiv, ByteBufferAlignedDecodeM, BindAlignedDecodeM in *; simpl in *; intros. repeat (apply functional_extensionality; intros). destruct (ListAlignedDecodeM (fun numBytes : nat => GetCurrentByte) n x0 x1 x2); simpl; eauto. } unfold AlignedDecodeMEquiv, ByteBufferAlignedDecodeM, BindAlignedDecodeM in *; simpl in *; intros. unfold GetCurrentByte at 1. destruct (Coq.Init.Nat.leb (idx0 + S n) n0) as [ | ] eqn: ?; simpl; repeat apply_in_hyp Compare_dec.leb_complete; repeat apply_in_hyp Compare_dec.leb_complete_conv; try Omega.omega; simpl; eauto. * destruct (nth_opt_some _ v0 idx0); try Omega.omega; rewrite H; simpl. pose proof (fun t' => IHn addD_addD_plus addD_0 _ (S idx0) v0 t' (addD c0 8)). rewrite (Compare_dec.leb_correct (S idx0 + n) n0) in H0 by Omega.omega; simpl in H0. pose proof (H0 (fun n => t' (existT ByteBuffer.t (S (projT1 n)) (Vector.cons _ x _ (projT2 n))))). cbv beta in H1. simpl projT1 at 1 in H1; simpl projT2 at 1 in H1. simpl projT1 at 1 in H1. unfold ByteBuffer.of_list in *; simpl. revert Heqb H. rewrite H1, addD_addD_plus; clear; intros. unfold bytebuffer_of_bytebuffer_range. unfold projT1; unfold projT2. f_equal; eauto. 2: f_equal; Omega.omega. replace ((skipn idx0 (to_list v0))) with (x :: (skipn (S idx0) (to_list v0))); auto. generalize n0 v0 H; clear. induction idx0; destruct v0; intros. -- compute in H; discriminate. -- compute in H; injections; reflexivity. -- compute in H; discriminate. -- unfold nth_opt in H; simpl in H; apply_in_hyp IHidx0. unfold to_list at 1; fold (@to_list _ n v0). replace (skipn (S (S idx0)) (h :: to_list v0)) with (skipn (S idx0) (to_list v0)) by reflexivity. rewrite H; reflexivity. * destruct (nth_opt v0 idx0); simpl; eauto. assert (Coq.Init.Nat.leb (S idx0 + n) n0 = false) by (apply Compare_dec.leb_correct_conv; Omega.omega). pose proof (fun t' => IHn addD_addD_plus addD_0 _ (S idx0) v0 t' (addD c0 8)). rewrite H in H0; simpl in H0. pose proof (H0 (fun n => t' (existT ByteBuffer.t (S (projT1 n)) (Vector.cons _ c1 _ (projT2 n))))). erewrite <- H1 at -1. f_equal; apply functional_extensionality; intro. 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.BinLib.AlignedList Fiat.Narcissus.BaseFormats Bedrock.Word