proposition: Lemma Append_EncodeMEquivAlignedEncodeM (encode1 encode2 : EncodeM S ByteString) (encode1_aligned encode2_aligned : forall {numBytes}, AlignedEncodeM numBytes) (encode1_OK : forall s env t env', encode1 s env = Some (t, env') -> padding t = 0) : EncodeMEquivAlignedEncodeM encode1 (@encode1_aligned) -> EncodeMEquivAlignedEncodeM encode2 (@encode2_aligned) -> EncodeMEquivAlignedEncodeM (sequence_Encode encode1 encode2) (fun numBytes => AppendAlignedEncodeM encode1_aligned encode2_aligned).
proof: Proof. unfold EncodeMEquivAlignedEncodeM; intros; specialize (encode1_OK s env); repeat split; intros. - destruct (H env s idx) as [ H' [? ?] ]. revert H1 v H' H2 H3 H4; unfold sequence_Encode; destruct (encode1 s env) as [ [t1 env''] | ] eqn: ? ; [ | intros; try discriminate]; simpl; destruct (encode2 s env'') as [ [t2 env'''] | ] eqn: ? ; simpl in *; try (intros; discriminate); intro; injection H1; intros ? ?; subst; simpl; rewrite numBytes_ByteString_enqueue_ByteString; intros; eauto. destruct (H0 env'' s (idx + (numBytes t1))) as [H0' [? [? ?] ] ]. specialize (H0' _ _ Heqo0). erewrite <- padding_ByteString_enqueue_aligned_ByteString in H0'. destruct (H' _ _ (eq_refl _) (encode1_OK _ _ (eq_refl _)) v1 (fst (Vector_split _ _ v)) _ (Vector.append (snd (Vector_split _ _ v)) v2)) as [? [? ?] ]. assert (idx + (numBytes t1 + (numBytes t2 + m)) = (idx + numBytes t1) + (numBytes t2 + m)) by omega; simpl in *. destruct (H0' H2 (fst (Vector_split _ _ (eq_rect _ (Vector.t char) x _ H10))) (fst (Vector_split _ _ (snd (Vector_split _ _ (eq_rect _ (Vector.t char) x _ H10))))) _ (snd (Vector_split _ _ (snd (Vector_split _ _ (eq_rect _ (Vector.t char) x _ H10))))) ). assert (idx + numBytes t1 + (numBytes t2 + m) = idx + (numBytes t1 + numBytes t2 + m)) as H11' by omega. assert (idx + (numBytes t1 + (numBytes t2 + m)) = (idx + (numBytes t1 + numBytes t2 + m))) by omega; simpl in *. unfold AppendAlignedEncodeM. replace (encode1_aligned (idx + ((numBytes t1 + numBytes t2) + m)) (Vector.append v1 (Vector.append v v2)) idx s env) with (Some (eq_rect _ (Vector.t char) x _ H12, idx + numBytes t1, env'')); simpl. + revert H12; rewrite <- H11'; intros. rewrite (plus_assoc idx (numBytes t1) (numBytes t2)). eexists _; intuition. * etransitivity; [ | apply H4]. f_equal. rewrite <- !Vector_split_append. f_equal; eapply UIP_dec; intros; decide equality. * rewrite <- H15. rewrite ByteString_enqueue_ByteString_assoc. rewrite ByteString_enqueue_ByteString_assoc. rewrite <- ByteString_enqueue_ByteString_assoc. symmetry in H9; destruct (build_aligned_ByteString_split' _ _ _ H9) as [? H'']; symmetry in H''; destruct (build_aligned_ByteString_split _ _ _ H''). revert H16 H9; clear. intro. revert H10 x v. assert (idx + (numBytes t1 + (numBytes t2 + m)) - idx - (numBytes t2 + m) = numBytes t1) as H''' by omega; revert x2 H16; rewrite H'''; clear H'''. generalize (numBytes t1); intros; subst. rewrite <- !build_aligned_ByteString_append in H9; apply build_aligned_ByteString_inj in H9; subst. rewrite <- !build_aligned_ByteString_append; repeat f_equal. erewrite Vector_append_assoc. rewrite <- Equality.transport_pp. erewrite (UIP_dec _ _ (eq_refl _)); simpl. rewrite <- Vector_append_split_fst; reflexivity. erewrite Vector_append_assoc. rewrite <- Equality.transport_pp. erewrite (UIP_dec _ _ (eq_refl _)); simpl. rewrite <- !Vector_append_split_snd; reflexivity. + generalize x H8 H12; clear; intros. replace (Some (eq_rect (idx + (numBytes t1 + (numBytes t2 + m))) (Vector.t char) x (idx + (numBytes t1 + numBytes t2 + m)) H12, idx + numBytes t1, env'')) with (eq_rect _ (fun x => option ((Vector.t char x) * nat * CacheFormat))%type (Some (x, idx + numBytes t1, env'')) _ H12). rewrite <- H8. assert (idx + (numBytes t1 + numBytes t2 + m) = idx + (numBytes t1 + (numBytes t2 + m))) by omega. replace (Vector.append v1 (Vector.append (fst (Vector_split (numBytes t1) (numBytes t2) v)) (Vector.append (snd (Vector_split (numBytes t1) (numBytes t2) v)) v2))) with (eq_rect _ (Vector.t char) (Vector.append v1 (Vector.append v v2)) _ H). assert (forall n m (H' : n = m) (v : Vector.t char n), encode1_aligned m (eq_rect n (Vector.t char) v _ H') idx s env = eq_rect n (fun x => option ((Vector.t char x) * nat * CacheFormat))%type (encode1_aligned _ v idx s env) _ H') as H' by (intros ? ? H'; rewrite H'; reflexivity). rewrite H', <- Equality.transport_pp. erewrite (UIP_dec _ _ (eq_refl _)); reflexivity. assert (numBytes t1 + numBytes t2 + m = numBytes t1 + (numBytes t2 + m)) by omega. replace (Vector.append (fst (Vector_split (numBytes t1) (numBytes t2) v)) (Vector.append (snd (Vector_split (numBytes t1) (numBytes t2) v)) v2)) with (eq_rect _ (Vector.t char) (Vector.append v v2) _ H0) by (erewrite Vector_append_assoc, <- Vector_split_append; reflexivity). erewrite Vector_append_assoc', Vector_append_assoc, <- Equality.transport_pp. reflexivity. destruct H12; reflexivity. + eapply encode1_OK; eauto. - specialize (H env s idx); unfold sequence_Encode in *; destruct (encode1 s env) as [ [t1 env''] | ] eqn: ? ; simpl in *; [ | intros; try discriminate]; simpl; destruct (encode2 s env'') as [ [t2 env'''] | ] eqn: ? ; simpl in *; try (intros; discriminate). pose proof (proj1 H _ _ (eq_refl _) (encode1_OK _ _ (eq_refl _))). injections. rewrite length_ByteString_enqueue_ByteString in H2. unfold AppendAlignedEncodeM; destruct (encode1_aligned numBytes' v idx s env) eqn: ? ; simpl; eauto. destruct (le_lt_dec (8 + 8 * numBytes') (length_ByteString t1 + 8 * idx)). { eauto; simpl in l; eapply (proj1 (proj2 H)) in l; eauto; rewrite Heqo1 in l; discriminate. } rewrite length_ByteString_no_padding in l by eauto. pose proof (proj1 (proj2 (H0 env'' s (snd (fst p))))) as H'. assert (numBytes t1 + idx < Datatypes.S numBytes')%nat by omega; clear l. assert (idx + numBytes t1 <= numBytes')%nat by omega. destruct (Vector_split_lt _ _ H4 v) as [? [? [? [? ?] ] ] ]. pose proof (proj1 (proj2 (H))) as H'' . destruct (H3 (fst (Vector_split _ _ x0)) (snd (Vector_split _ _ x0)) _ x1) as [v' [? ?] ]. erewrite <- H'; f_equal; clear H'. + revert p Heqo1 H6. rewrite H5. rewrite <- x2; simpl; clear. rewrite Vector_append_assoc with (H := sym_eq (plus_assoc idx (numBytes t1) x)), <- Vector_split_append. generalize v' (eq_sym (plus_assoc idx (numBytes t1) x)). rewrite (plus_assoc idx (numBytes t1) x). intros. erewrite (UIP_dec _ _ (eq_refl _)) in H6; simpl in H6. rewrite Heqo1 in H6; destruct p as [ [? ?] ?]; simpl in *; congruence. + rewrite Heqo0; simpl; eauto. + replace (8 * snd (fst p)) with (length_ByteString t1 + 8 * idx); try omega. rewrite length_ByteString_no_padding by eauto. revert p Heqo1 H6. rewrite H5. rewrite <- x2; simpl; clear. rewrite Vector_append_assoc with (H := sym_eq (plus_assoc idx (numBytes t1) x)), <- Vector_split_append. generalize v' (eq_sym (plus_assoc idx (numBytes t1) x)). rewrite (plus_assoc idx (numBytes t1) x). intros. erewrite (UIP_dec _ _ (eq_refl _)) in H6; simpl in H6. rewrite Heqo1 in H6; destruct p as [ [? ?] ?]; simpl in *; injections. omega. - specialize (H env s idx); unfold sequence_Encode in *; destruct (encode1 s env) as [ [t1 env''] | ] eqn: ? ; simpl in *; [ | intros; try discriminate]; simpl; destruct (encode2 s env'') as [ [t2 env'''] | ] eqn: ? ; simpl in *; try (intros; discriminate); injections. pose proof (proj1 H _ _ (eq_refl _) (encode1_OK _ _ (eq_refl _))). rewrite padding_ByteString_enqueue_aligned_ByteString in H2 by eauto. unfold AppendAlignedEncodeM; destruct (encode1_aligned numBytes' v idx s env) eqn: ? ; simpl; eauto. destruct (le_lt_dec (8 + 8 * numBytes') (length_ByteString t1 + 8 * idx)). { eauto; simpl in l; eapply (proj1 (proj2 H)) in l; eauto; rewrite l in Heqo1; discriminate. } rewrite length_ByteString_no_padding in l by eauto. pose proof (proj1 (proj2 (proj2 (H0 env'' s (snd (fst p)))))) as H'. assert (numBytes t1 + idx < Datatypes.S numBytes')%nat by omega; clear l. assert (idx + numBytes t1 <= numBytes')%nat by omega. destruct (Vector_split_lt _ _ H4 v) as [? [? [? [? ?] ] ] ]. pose proof (proj2 (proj2 (H))) as H'' . destruct (H1 (fst (Vector_split _ _ x0)) (snd (Vector_split _ _ x0)) _ x1) as [v' [? ?] ]. erewrite <- H'; f_equal; clear H'; eauto. * revert p Heqo1 H6. rewrite H5. rewrite <- x2; simpl; clear. rewrite Vector_append_assoc with (H := sym_eq (plus_assoc idx (numBytes t1) x)), <- Vector_split_append. generalize v' (eq_sym (plus_assoc idx (numBytes t1) x)). rewrite (plus_assoc idx (numBytes t1) x). intros. erewrite (UIP_dec _ _ (eq_refl _)) in H6; simpl in H6. rewrite Heqo1 in H6; destruct p as [ [? ?] ?]; simpl in *; try congruence. - specialize (H env s idx); unfold sequence_Encode in *; destruct (encode1 s env) as [ [t1 env''] | ] eqn: ? ; simpl in *. + destruct (encode2 s env'') as [ [t2 env'''] | ] eqn: ? ; simpl in *; try discriminate. unfold AppendAlignedEncodeM. destruct (Nat.le_decidable (8 + 8 * numBytes') (length_ByteString t1 + 8 * idx)). erewrite (proj1 (proj2 H)); eauto. destruct (PeanoNat.Nat.eq_dec (padding t1) 0). unfold length_ByteString in H2; rewrite e in H2; simpl in H2. assert (exists m, numBytes' = idx + (numBytes t1 + m)). exists (numBytes' - (idx + numBytes t1)). omega. destruct H3. pose proof (proj1 H _ _ (eq_refl _) (encode1_OK _ _ (eq_refl _))) as H'. destruct (H' (fst (Vector_split _ _ (eq_rect _ _ v _ H3))) (fst (Vector_split _ _ (snd (Vector_split _ _ (eq_rect _ _ v _ H3))))) _ (snd (Vector_split _ _ (snd (Vector_split _ _ (eq_rect _ _ v _ H3)))))) as [v' [? ?] ]. replace (encode1_aligned _ v idx s env) with (Some (eq_rect _ (Vector.t char) v' _ (sym_eq H3), idx + numBytes t1, env'')). * simpl; eapply H0; rewrite <- Heqo0; f_equal. * generalize v' H3 H4; clear; intros. revert v v' H4; rewrite H3; intros; simpl; f_equal. unfold ByteBuffer.t in *. rewrite <- H4; f_equal. rewrite <- !Vector_split_append; reflexivity. * erewrite (proj1 (proj2 (proj2 H))); eauto. + unfold AppendAlignedEncodeM; rewrite (proj2 (proj2 (proj2 H))); simpl; eauto. Unshelve. omega. decide equality. omega. decide equality. decide equality. omega. decide equality. decide equality. decide equality. 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.Common.BoundedLookup Fiat.Narcissus.Common.Specs Fiat.Narcissus.Common.ComposeOpt Fiat.Narcissus.Common.ComposeIf Fiat.Narcissus.BaseFormats Fiat.Narcissus.BinLib.Core Fiat.Narcissus.BinLib.AlignedByteString