proposition: Lemma EncodeMEquivAlignedEncodeMDep {S A} {cache : Cache} (enc1' : EncodeM S ByteString) (enc2' : A -> EncodeM S ByteString) (f' : ByteString -> A) (enc1 : forall sz, AlignedEncodeM sz) (enc2 : A -> forall sz, AlignedEncodeM sz) (f : nat -> forall {sz}, Vector.t (word 8) sz -> nat -> A) (enc1_OK : EncodeMEquivAlignedEncodeM enc1' enc1) (enc2_OK : forall a, EncodeMEquivAlignedEncodeM (enc2' a) (enc2 a)) (enc1'_aligned : forall s ce t ce', enc1' s ce = Some (t, ce') -> padding t = 0) (enc2'_aligned : forall a s ce t ce', enc2' a s ce = Some (t, ce') -> padding t = 0) (enc'_sz_eq : forall s a ce t1 ce1 t2 ce2, enc1' s ce = Some (t1, ce1) -> enc2' a s ce = Some (t2, ce2) -> bin_measure t1 = bin_measure t2) (f_OK : forall (b : ByteString) idx (v1 : Vector.t Core.char idx) m (v2 : Vector.t Core.char m) (v : Vector.t Core.char (idx + ((numBytes b) + m))), ByteString_enqueue_ByteString (build_aligned_ByteString v1) (ByteString_enqueue_ByteString b (build_aligned_ByteString v2)) = build_aligned_ByteString v -> f' b = f (numBytes b) v idx) : EncodeMEquivAlignedEncodeM (fun s ce => `(p, _) <- enc1' s ce; enc2' (f' p) s ce) (fun sz => EncodeAgain (enc1 sz) (fun idx' v idx s => enc2 (f (idx'-idx) v idx) sz v idx s))%AlignedEncodeM.
proof: Proof. repeat split; intros; simpl in *. { destruct enc1' eqn:?; [| discriminate]; destruct_conjs; simpl in *. assert (numBytes b = numBytes t) as L1. { assert (bin_measure b = bin_measure t) by eauto. rewrite !length_ByteString_no_padding in H1 by eauto. omega. } edestruct enc1_OK as [? _]. specialize (H1 _ _ Heqe). revert H1. rewrite L1. intros. edestruct (H1 (enc1'_aligned _ _ _ _ Heqe) v1 v _ v2); eauto. clear H1. destruct_conjs. assert (exists v, v1 ++ v ++ v2 = x) as L2. { destruct L1. edestruct @AlignedEncoder_inv'; eauto; eauto. destruct_conjs. eauto. } destruct L2 as [v' L2]. edestruct enc2_OK as [? _]. specialize (H3 _ _ H). edestruct H3; eauto. clear H3. destruct_conjs. rewrite L2 in H3. eexists. split; eauto. unfold EncodeAgain. rewrite H1. simpl. match goal with | H : enc2 ?a _ _ _ _ _ = _ |- context[enc2 ?a' _ _ _ _ _] => replace a' with a end. rewrite H3. simpl. reflexivity. destruct L1. replace (idx + numBytes b - idx) with (numBytes b) by omega. eauto. } { destruct enc1' eqn:?; [| discriminate]; destruct_conjs; simpl in *. edestruct enc1_OK as [_ [? _]]. eapply H1 in Heqe. unfold EncodeAgain. rewrite Heqe. reflexivity. assert (bin_measure b = bin_measure t) as L1 by eauto. simpl in *. congruence. } { destruct enc1' eqn:?; [| discriminate]; destruct_conjs; simpl in *. exfalso. eauto. } { destruct enc1' eqn:?; destruct_conjs; simpl in *; unfold EncodeAgain. { destruct (Nat.le_decidable (1 + numBytes') (numBytes b + idx)). edestruct enc1_OK as [_ [? _]]. erewrite H1; eauto. rewrite length_ByteString_no_padding by eauto. omega. assert (exists m, numBytes' = idx + (numBytes b + m)). { exists (numBytes' - (idx + numBytes b)). omega. } destruct H1 as [m ?]. subst. edestruct (enc1_OK env s idx) as [? _]; eauto. edestruct H1; eauto. destruct_conjs. match goal with | H : enc1 _ ?v' _ _ _ = _ |- _ => replace v with v' end. rewrite H2. simpl. edestruct enc2_OK as [_ [_ [_ ?]]]. rewrite H4; eauto. simpl. rewrite <- H. f_equal. replace (idx + numBytes b - idx) with (numBytes b) by omega. symmetry. eauto. repeat (rewrite Vector_split_append; f_equal). } { edestruct (enc1_OK env s idx) as [_ [_ [_ ?]]]; eauto. eapply H0 in Heqe; eauto. rewrite Heqe. 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.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