proposition: Lemma CorrectEncodeDecode {S} {cache : Cache.Cache} : forall Invariant (FormatSpec : Specs.FormatM S ByteString) (decoder : CorrectAlignedDecoderFor Invariant FormatSpec), forall sz v' ce cd cd' s idx', Cache.Equiv ce cd -> snd (projT1 (projT2 decoder)) cd -> (projT1 decoder sz) v' 0 cd = Some (s, idx', cd') -> Invariant s /\ exists ce' (v1 : Vector.t (word 8) idx') (v2 : Vector.t (word 8) (sz - idx')) H, Guarded_Vector_split idx' sz v' = eq_rect _ _ (Vector.append v1 v2) _ H /\ Cache.Equiv ce' cd' /\ FormatSpec s ce (build_aligned_ByteString v1, ce').
proof: Proof. intros. pose proof (Specs.CorrectEncodeDecode _ _ (CorrectAlignedDecoder2CorrectDecoder _ _ decoder)). simpl in *. destruct (fst (projT1 (projT2 decoder)) (build_aligned_ByteString v') cd) as [ [ [? ?] ?] | ] eqn: ?. - specialize (H2 _ _ _ _ _ _ H H0 Heqo); destruct H2 as [? [? [? [? [? ?] ] ] ] ]. pose proof (proj2 (projT2 (projT2 decoder))). destruct H6 as [_ [? [? ?] ] ]. specialize (H8 _ _ _ Heqo). specialize (H6 _ _ _ _ _ Heqo). destruct H8 as [? [? ?] ]. rewrite H8 in H1; injection H1; intros; subst. intuition. assert (sz >= numBytes b)%nat. { revert H6; unfold length_ByteString; simpl. generalize (paddingOK b); clear; intros; Omega.omega. } assert (sz - numBytes b + (sz - (sz - numBytes b)) = sz - numBytes b + (sz - (sz - numBytes b))). Omega.omega. assert ((sz - (sz - numBytes b)) = numBytes b) by Omega.omega. eexists _, (fst (Vector_split _ _ (Guarded_Vector_split (sz - numBytes b) sz v'))), (snd (Vector_split _ _ (Guarded_Vector_split (sz - numBytes b) sz v'))), H12; intuition eauto. rewrite <- Vector_split_append. revert H12. destruct H13; intros. clear. intros; rewrite <- Eqdep_dec.eq_rect_eq_dec; eauto. decide equality. destruct (build_aligned_ByteString_split' _ _ _ H9). rewrite H14 in H3. destruct (build_aligned_ByteString_split _ _ _ H3). subst. rewrite <- build_aligned_ByteString_append in H3. rewrite build_aligned_ByteString_eq_split' with (n := sz - numBytes b) in H3; eauto. replace (build_aligned_ByteString (fst (Vector_split (sz - numBytes b) (sz - (sz - numBytes b)) (Guarded_Vector_split (sz - numBytes b) sz v')))) with (build_aligned_ByteString x3); eauto. revert x2 x3 H3 H5 H14. generalize (Guarded_Vector_split (sz - numBytes b) sz v'). rewrite H13. intros. apply build_aligned_ByteString_inj in H3; subst. rewrite <- Vector_append_split_fst; eauto. clear; Omega.omega. - pose proof (proj2 (projT2 (projT2 decoder))). destruct H3 as [_ [? [? ?] ] ]. apply H4 in Heqo. congruence. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Fiat.Narcissus.Common.Monoid Bedrock.Word Fiat.Narcissus.BinLib.AlignedByteString Fiat.Narcissus.BinLib.AlignedByteBuffer Fiat.Narcissus.BinLib.AlignWord Fiat.Narcissus.BinLib.AlignedList Fiat.Narcissus.BinLib.AlignedDecoders Fiat.Narcissus.BinLib.AlignedDecodeMonad Fiat.Narcissus.BinLib.AlignedEncodeMonad Fiat.Narcissus.BinLib.AlignedIPChecksum