proposition: Lemma CorrectDecodeEncode {A} {cache : Cache.Cache} {sz} : forall Invariant (FormatSpec : Specs.FormatM A _) (encoder : CorrectAlignedEncoderFor FormatSpec) (decoder : CorrectAlignedDecoderFor Invariant FormatSpec), forall a ce cd v, Cache.Equiv ce cd -> Invariant a -> snd (projT1 (projT2 decoder)) cd -> forall idx ce' v', projT1 encoder sz v 0 a ce = Some (v', idx, ce') -> exists cd' idx', (projT1 decoder sz) v' 0 cd = Some (a, idx', cd').
proof: Proof. intros. destruct (projT1 (projT2 encoder) a ce) as [ [? ?] | ] eqn: ?. - generalize Heqo; intro. eapply (@CorrectDecodeEncode' _ _ _ _ _ _ (CorrectAlignedEncoder2CorrectEncoder _ encoder) (CorrectAlignedDecoder2CorrectDecoder _ _ decoder)) in Heqo; eauto. destruct Heqo. simpl in H3. pose proof (projT2 (projT2 encoder)); simpl in *. destruct H4. pose proof (proj1 H5 _ _ _ _ Heqo0). assert (numBytes b <= sz)%nat. { destruct (Compare_dec.le_gt_dec (8 + 8 * sz) (length_ByteString b + 8 * 0)); eauto. apply @proj2 in H5. eapply proj2 in H5. eapply proj1 in H5. specialize (H5 _ _ _ v Heqo0 l). congruence. unfold length_ByteString in g. rewrite H6 in g. unfold gt in g. Omega.omega. } apply @proj2 in H5. eapply proj1 in H5. generalize H7; intros H7'. assert (numBytes b + (sz - numBytes b) = sz) as sz_eq by Omega.omega. eapply (build_aligned_ByteString_eq_split _ _ v) in H7. instantiate (1 := sz_eq) in H7. eapply (build_aligned_ByteString_eq_split _ _ v') in H7'. instantiate (1 := sz_eq) in H7'. specialize (H5 _ _ Heqo0 H6 (Vector.nil _) (fst (Vector_split _ _ (Guarded_Vector_split (numBytes b) sz v))) _ (snd (Vector_split _ _ (Guarded_Vector_split (numBytes b) sz v)))). destruct H5 as [? [? ?] ]. simpl in *. rewrite <- Vector_split_append in H5. pose proof mempty_left; simpl in H9. rewrite build_aligned_ByteString_nil, H9 in H8. symmetry in H8. destruct (build_aligned_ByteString_split _ _ _ H8). symmetry in H8. rewrite H10 in H8 at 1. rewrite <- build_aligned_ByteString_append in H8. subst. assert (numBytes b + (sz - numBytes b) - (sz - numBytes b) = numBytes b) by Omega.omega. revert x1 H8 H10. rewrite H11; intros. assert (Some ((Guarded_Vector_split (numBytes b) sz v'), idx, ce') = Some (Vector.append x1 (snd (Vector_split (numBytes b) (sz - numBytes b) (Guarded_Vector_split (numBytes b) sz v))), numBytes b, c)). apply build_aligned_ByteString_inj in H8; subst. apply build_aligned_ByteString_inj in H7; subst. apply build_aligned_ByteString_inj in H7'; subst. revert H2. rewrite H7 at 1. rewrite H7' at 1. simpl. simpl in *; unfold ByteBuffer.t in H5. rewrite <- H5. rewrite <- sz_eq. simpl; unfold ByteBuffer.t, Core.char; intros. rewrite <- H2. reflexivity. injection H12; intros; subst; clear H12. instantiate (1 := build_aligned_ByteString (snd (Vector_split (numBytes b) (sz - numBytes b) (Guarded_Vector_split (numBytes b) sz v)))) in H3. apply build_aligned_ByteString_inj in H7'; subst. rewrite H10 in H3 at 1. rewrite <- build_aligned_ByteString_append in H3. rewrite <- H15 in H3. pose proof (proj2 (projT2 (projT2 decoder))). eapply H12 in H3. simpl in H3; destruct H3. eexists _, _. rewrite <- H3. rewrite H7' at 1. generalize sz_eq v'; clear; intros. rewrite <- sz_eq; simpl; reflexivity. - pose proof (projT2 (projT2 encoder)); simpl in *. destruct H3 as [? [? ?] ]. specialize (H5 ce a 0); intuition. eapply H9 in Heqo. rewrite Heqo in H2; discriminate. 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