proposition: Lemma Bind_DecodeMEquivAlignedDecodeM {A C : Type} (A_decode : DecodeM (A * ByteString) ByteString) (A_decode_aligned : forall {numBytes}, AlignedDecodeM A numBytes) (t : A -> DecodeM (C * ByteString) ByteString) (t' : A -> forall {numBytes}, AlignedDecodeM C numBytes) : DecodeMEquivAlignedDecodeM A_decode (@A_decode_aligned) -> (forall a, DecodeMEquivAlignedDecodeM (t a) (@t' a)) -> DecodeMEquivAlignedDecodeM (fun (b : ByteString) (c : CacheDecode) => `(a, bs, cd') <- A_decode b c; t a bs cd') (fun numBytes => BindAlignedDecodeM A_decode_aligned (fun a => @t' a numBytes)).
proof: Proof. unfold DecodeMEquivAlignedDecodeM; intros; intuition. - unfold BindAlignedDecodeM. rewrite H1. destruct (A_decode_aligned numBytes_hd (Vector.tl v) n cd) as [ [ [? ?] ?] | ]; simpl. + specialize (H0 a); intuition. + reflexivity. - eapply DecodeBindOpt2_inv in H2; destruct_ex; intuition. specialize (H0 x); intuition. eapply H in H4. symmetry in H5; eapply H0 in H5; omega. - destruct (A_decode (build_aligned_ByteString v) cd) as [ [ [? ?] ?] | ] eqn: ?; simpl in *; try discriminate. assert (numBytes b <= n)%nat as nb_le_n. { eapply H in Heqo. unfold build_aligned_ByteString, length_ByteString in Heqo; simpl in Heqo; omega. } unfold BindAlignedDecodeM. apply H3 in Heqo; destruct_ex; intuition; subst; destruct_ex. rewrite H4; simpl; eauto. specialize (H0 a); intuition. generalize (build_aligned_ByteString_split' _ _ _ H5); intros; destruct_ex. rewrite H7 in *. apply H8 in H2. assert ((n - (n - numBytes b)) = numBytes b). { rewrite sub_plus; try omega. rewrite H7; auto. } pose proof (fun v => proper_consumer_t_None (m := n - numBytes b) (t' a) H6 v x _ _ H2). assert (forall v0 : ByteBuffer.t n, build_aligned_ByteString v0 = build_aligned_ByteString (Vector.append x x0) -> t' a n v0 (n - numBytes b) c = None). { revert H10; clear; intro. assert (n = n - numBytes b + (n - (n - numBytes b))) by omega. intros. specialize (H10 (eq_rect _ _ v0 _ H)). destruct H. eapply H10. apply H0. } replace (n - numBytes (build_aligned_ByteString x0)) with (n - numBytes b) by (unfold numBytes at 2; simpl; clear; omega). apply H11. rewrite H5. rewrite build_aligned_ByteString_append; f_equal; assumption. unfold BindAlignedDecodeM; apply H3 in Heqo; rewrite Heqo; reflexivity. - unfold BindAlignedDecodeM in H2. destruct (A_decode (build_aligned_ByteString v) cd) as [ [ [? ?] ?] | ] eqn: ? ; simpl in *; try eauto. assert (numBytes b <= n)%nat as nb_le_n. { eapply H in Heqo. unfold build_aligned_ByteString, length_ByteString in Heqo; simpl in Heqo; omega. } apply H3 in Heqo; destruct_ex; intuition; subst; destruct_ex. rewrite H4 in H2; simpl in H2; eauto. specialize (H0 a); intuition. generalize (build_aligned_ByteString_split' _ _ _ H5); intros; destruct_ex. rewrite H7 in *. apply H8. assert ((n - (n - numBytes b)) = numBytes b). { rewrite sub_plus; try omega. rewrite H7; auto. } assert (n = n - numBytes b + (n - (n - numBytes b))) by omega. eapply proper_consumer_t_None' with (v1 := x) (v0 := (eq_rect _ _ v _ H10)); eauto. revert H2; clear. destruct H10; simpl; intros. rewrite <- H2; f_equal; omega. revert H5 H7; clear; destruct H10; simpl; intros. rewrite H5, build_aligned_ByteString_append; f_equal; assumption. - eapply DecodeBindOpt2_inv in H2; destruct_ex; intuition. assert (numBytes x0 <= n)%nat as nb_le_n. { eapply H in H4. unfold build_aligned_ByteString, length_ByteString in H4; simpl in H4; omega. } assert (numBytes bs' <= numBytes x0)%nat as nbs_le_x0. { symmetry in H5. eapply H0 in H5. eapply H3 in H4; intuition; destruct_ex. generalize (build_aligned_ByteString_split' _ _ _ H4); intros; destruct_ex. rewrite H6 in H5. unfold length_ByteString in H5; simpl in H5. replace (n - (n - numBytes x0)) with (numBytes x0) in H5 by (revert nb_le_n; clear; intro; omega). omega. } assert (numBytes bs' <= n)%nat as nbs_le_n. { etransitivity. apply nbs_le_x0. apply nb_le_n. } eapply H3 in H4. intuition. unfold BindAlignedDecodeM; rewrite H2; simpl; destruct_ex; intuition. symmetry in H5. specialize (H0 x); intuition. generalize (build_aligned_ByteString_split' _ _ _ H4); intros; destruct_ex. rewrite H7 in *|-*. eapply H8 in H5; intuition. unfold numBytes at 1; simpl. destruct_ex; intuition. assert (n = n - numBytes x0 + (n - (n - numBytes x0))) by omega. pose proof (proper_consumer_t_Some _ H6 (eq_rect _ _ v _ H10) x2 x3 _ _ _ _ H9). destruct H10. simpl in H11. assert (n >= numBytes x0)%nat by (rewrite H7; omega). replace (n - (n - numBytes x0)) with (numBytes x0) by omega. rewrite H11. f_equal; f_equal; f_equal. assert (numBytes x0 >= numBytes bs')%nat. rewrite H7; omega. omega. rewrite H4. rewrite build_aligned_ByteString_append; f_equal; eauto. - eapply DecodeBindOpt2_inv in H2; destruct_ex; intuition. assert (numBytes x0 <= n)%nat as nb_le_n. { eapply H in H4. unfold build_aligned_ByteString, length_ByteString in H4; simpl in H4; omega. } assert (numBytes bs' <= n)%nat as nbs_le_n. { symmetry in H5. eapply H0 in H5. eapply H3 in H4; intuition; destruct_ex. generalize (build_aligned_ByteString_split' _ _ _ H4); intros; destruct_ex. etransitivity. 2: apply nb_le_n. rewrite H6 in H5. unfold length_ByteString in H5; simpl in H5. replace (n - (n - numBytes x0)) with (numBytes x0) in H5 by (revert nb_le_n; clear; intro; omega). omega. } eapply H3 in H4; intuition; destruct_ex. setoid_rewrite H4. eapply build_aligned_ByteString_split' in H4; destruct_ex. rewrite H4 in *. symmetry in H5. eapply H0 in H5; intuition; destruct_ex. rewrite H5 in H4. assert ((n - numBytes x0 + (n - (n - numBytes x0) - numBytes bs')) = n - numBytes bs'). { assert (n >= numBytes x0)%nat by (rewrite H4; rewrite H5 in nb_le_n; omega). replace (n - (n - numBytes x0)) with (numBytes x0). assert (numBytes x0 >= numBytes bs')%nat. { rewrite H4. generalize (build_aligned_ByteString_split' _ _ _ H5); intros; destruct_ex. replace (ByteString_enqueue_ByteString (build_aligned_ByteString x4) bs') with (build_aligned_ByteString (Vector.append x4 x5)). generalize x4 x5 H8; clear. generalize (n - (n - numBytes x0) - numBytes bs'). intro. generalize (n - (n - numBytes x0) - n0); intros. rewrite H8. unfold numBytes; simpl; omega. rewrite build_aligned_ByteString_append; f_equal; eauto. } omega. omega. } generalize H7 H4; clear; intros. rewrite <- H7. eexists (Vector.append x2 x4). rewrite build_aligned_ByteString_append. rewrite <- ByteString_enqueue_ByteString_assoc. rewrite <- H4; reflexivity. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Bedrock.Word Coq.ZArith.ZArith Coq.NArith.NArith Coq.Arith.Arith Coq.Numbers.Natural.Peano.NPeano Coq.Logic.Eqdep_dec Fiat.Narcissus.Common.Specs Fiat.Narcissus.BinLib.Core Fiat.Narcissus.BinLib.AlignedByteString