proposition: Lemma AlignedEncoder_inv' {S} {cache : Cache} (enc' : EncodeM S ByteString) (enc : forall sz, AlignedEncodeM sz) (enc_OK : EncodeMEquivAlignedEncodeM enc' enc) (enc'_aligned : forall s ce t ce', enc' s ce = Some (t, ce') -> padding t = 0) n1 n3 : forall s ce b ce'', enc' s ce = Some (b, ce'') -> forall (t1 : Vector.t Core.char n1) (t2 : Vector.t Core.char (numBytes b)) (t3 : Vector.t Core.char n3) v idx ce', enc _ (t1++t2++t3) n1 s ce = Some (v, idx, ce') -> exists v2, enc _ t2 0 s ce = Some (v2, numBytes b, ce') /\ v = t1 ++ v2 ++ t3 /\ idx = n1 + numBytes b /\ b = build_aligned_ByteString v2 /\ ce'' = ce'.
proof: Proof. intros. edestruct enc_OK as [? _]. edestruct H1; eauto. clear H1. destruct_conjs. rewrite H1 in H0. injections. edestruct enc_OK with (idx:=0) as [? _]. edestruct H0 with (m:=0) (v0:=t2) (v1:=Vector.nil Core.char) (v2:=Vector.nil Core.char); eauto. clear H0. simpl in *. destruct_conjs. revert H0. rewrite Vector_append_nil_r'. generalize (plus_n_O (numBytes b)). destruct e. simpl. intros. assert (b = build_aligned_ByteString x) as L. { rewrite <- H3. rewrite !build_aligned_ByteString_nil. eauto using mempty_left. } eexists; intuition eauto. apply build_aligned_ByteString_inj. rewrite !build_aligned_ByteString_append. rewrite <- H2. repeat f_equal. eauto. 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