proposition: Lemma CorrectAlignedEncoderForFormatVector {sz} {S} : forall (format_S : FormatM S ByteString) (encode_S : forall numBytes : nat, AlignedEncodeM numBytes) (encode_S_OK : CorrectAlignedEncoder format_S encode_S) (encode_A_OK' : forall (s : S) sz (l : Vector.t S sz) (env : CacheFormat) (tenv' tenv'' : ByteString * CacheFormat), format_S s env ∋ tenv' -> Vector.format_Vector format_S l (snd tenv') ∋ tenv'' -> exists tenv3 tenv4 : _ * CacheFormat, projT1 encode_S_OK s env = Some tenv3 /\ Vector.format_Vector format_S l (snd tenv3) ∋ tenv4), CorrectAlignedEncoder (Vector.format_Vector format_S) (AlignedEncodeVector encode_S (sz := sz)).
proof: Proof. intros; induction sz. - eapply refine_CorrectAlignedEncoder with (format' := fun s env => ret (mempty, env)). intros. pattern s; eapply Vector.case0; split. + reflexivity. + intros; intro. eapply H; eauto. + unfold AlignedEncodeVector; simpl. eapply CorrectAlignedEncoderForDoneC. - eapply refine_CorrectAlignedEncoder with (format' := SequenceFormat.sequence_Format (FMapFormat.Projection_Format format_S Vector.hd) (FMapFormat.Projection_Format (Vector.format_Vector format_S) Vector.tl)). + intros; pattern sz, s; eapply Vector.caseS; intros; simpl; split. * unfold SequenceFormat.sequence_Format; simpl. unfold compose, Bind2. f_equiv; [ apply FMapFormat.EquivFormat_Projection_Format | intro]. f_equiv; apply FMapFormat.EquivFormat_Projection_Format. * unfold SequenceFormat.sequence_Format; simpl; unfold compose, Bind2; intros; intro. computes_to_inv. eapply H. computes_to_econstructor. eapply (proj1 (FMapFormat.EquivFormat_Projection_Format _ _ _ _)). simpl; eauto. computes_to_econstructor. eapply (proj1 (FMapFormat.EquivFormat_Projection_Format _ _ _ _)). simpl; eauto. eauto. + unfold AlignedEncodeVector. eapply CorrectAlignedEncoder_morphism. apply EquivFormat_reflexive. 2: eapply CorrectAlignedEncoderForThenC. 2: eapply CorrectAlignedEncoderProjection; eauto. intros. pattern sz, w; apply Vector.caseS; intros. unfold AppendAlignedEncodeM, Projection_AlignedEncodeM, AlignedEncodeVector; simpl. destruct (encode_S sz0 v idx h c) as [ [ [? ?] ?] | ] eqn: ?; simpl; eauto. assert (forall n' m (t1 : Vector.t S m) n (t2 : Vector.t S n) sz0 t0 k idx cf, AlignedEncodeVector' n' (k + m) encode_S sz0 t0 idx (Vector.append t1 t2) cf = AlignedEncodeVector' n' k encode_S sz0 t0 idx t2 cf). { clear; induction n'; simpl; intros; eauto. rewrite Vector_nth_opt_append; simpl. destruct (Vector_nth_opt t2 k); simpl; eauto. destruct (encode_S sz0 t0 idx s cf) as [ [ [? ?] ?] | ] eqn: ?; simpl; eauto. erewrite <- IHn' with (k := 1 + k); simpl; reflexivity. } instantiate (1 := fun sz v idx v' c => encode_S sz v idx (Vector.hd v') c). simpl; rewrite Heqo; simpl. erewrite <- H with (k := 0) (m := 1) (t1 := Vector.cons _ h _ (Vector.nil _)). reflexivity. simpl; rewrite Heqo; reflexivity. instantiate (1 := CorrectAlignedEncoderProjection _ _ _ encode_S_OK). intros. match goal with |- exists _ _, (projT1 ?H) ?s ?env = _ /\ _ => destruct (projT1 H s env) eqn: ? ; generalize (proj1 (projT2 H) s env); intros end. * apply proj1 in H1. destruct p. eapply H1 in Heqo. eapply (proj2 (FMapFormat.EquivFormat_Projection_Format _ _ _ _)) in H. eapply (proj2 (FMapFormat.EquivFormat_Projection_Format _ _ _ _)) in H0. specialize (encode_A_OK' _ _ _ _ _ _ H H0). destruct_ex; intuition; subst. destruct encode_S_OK. destruct a. destruct a0. unfold CorrectAlignedEncoderProjection; simpl in *. eexists _, _; split. unfold Basics.compose; eauto. eapply FMapFormat.EquivFormat_Projection_Format. eauto. * apply proj2 in H1. eapply H1 in Heqo. eapply Heqo in H; intuition. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.ZArith.ZArith Coq.Strings.String Coq.Arith.Mult Coq.Vectors.Vector Fiat.Common.SumType Fiat.Common.BoundedLookup Fiat.Common.ilist Fiat.Common.DecideableEnsembles Fiat.Computation Fiat.QueryStructure.Specification.Representation.Notations Fiat.QueryStructure.Specification.Representation.Heading Fiat.QueryStructure.Specification.Representation.Tuple Fiat.Narcissus.BinLib.AlignedEncodeMonad Fiat.Narcissus.BinLib.AlignedByteString Fiat.Narcissus.BinLib.AlignWord Fiat.Narcissus.BinLib.AlignedString Fiat.Narcissus.BinLib.AlignedDecodeMonad Fiat.Narcissus.Common.Specs Fiat.Narcissus.Common.ComposeOpt Fiat.Narcissus.Formats.WordOpt Fiat.Narcissus.Formats.NatOpt Fiat.Narcissus.Formats.StringOpt Fiat.Narcissus.Formats.EnumOpt Fiat.Narcissus.Formats.FixListOpt Fiat.Narcissus.Formats.SumTypeOpt Fiat.Narcissus.Formats.EnumOpt Fiat.Narcissus.Formats.DomainNameOpt Fiat.Common.IterateBoundedIndex Fiat.Common.Tactics.CacheStringConstant Fiat.Narcissus.Formats.IPChecksum Fiat.Narcissus.Common.ComposeCheckSum Bedrock.Word