proposition: Lemma CorrectAlignedEncoderForFormatList {A} format_A encode_A (encode_A_OK : CorrectAlignedEncoder format_A encode_A) (encode_A_OK' : forall (a : A) l (env : CacheFormat) (tenv' tenv'' : ByteString * CacheFormat), format_A a env ∋ tenv' -> format_list format_A l (snd tenv') ∋ tenv'' -> exists tenv3 tenv4 : _ * CacheFormat, projT1 encode_A_OK a env = Some tenv3 /\ format_list format_A l (snd tenv3) ∋ tenv4) : CorrectAlignedEncoder (format_list format_A) (@AlignedEncodeList A encode_A).
proof: Proof. unfold CorrectAlignedEncoder; intros. rename encode_A_OK into X. eexists ((fix AlignedEncodeList (As : list A) env := match As with | nil => Some (mempty, env) | a :: As' => `(t1, env') <- projT1 X a env; `(t2, env'') <- AlignedEncodeList As' env'; Some (mappend t1 t2, env'') end)); split; [ split | split ]. - revert env; induction s; intros; simpl; eauto. + injections; reflexivity. + destruct X as [encode_A' [? [? ?] ] ]; simpl in *. destruct (encode_A' a env) as [ [? ?] | ] eqn: ?; simpl in *; try discriminate. unfold Bind2. rewrite (proj1 (a0 _ _)), refineEquiv_bind_unit; eauto. destruct ((fix AlignedEncodeList (As : list A) (env : CacheFormat) {struct As} : option (ByteString * CacheFormat) := match As with | [] => Some (ByteString_id, env) | a :: As' => `(t1, env') <- encode_A' a env; `(t2, env'') <- AlignedEncodeList As' env'; Some (ByteString_enqueue_ByteString t1 t2, env'') end)) as [ [? ?] | ] eqn: ?; simpl in *; try discriminate. rewrite IHs, refineEquiv_bind_unit; simpl; eauto. injections; reflexivity. - revert env; induction s; intros; simpl; eauto; try discriminate. destruct X as [encode_A' [? [? ?] ] ]; simpl in *. destruct (encode_A' a env) as [ [? ?] | ] eqn: ?; simpl in *; try discriminate; unfold Bind2; intros ?; computes_to_inv. + destruct (encode_A_OK' _ _ _ _ _ H0 H0') as [ [? ?] [ [? ?] [? ?] ] ]. rewrite H1 in Heqo; injections. destruct ((fix AlignedEncodeList (As : list A) (env : CacheFormat) {struct As} : option (ByteString * CacheFormat) := match As with | [] => Some (ByteString_id, env) | a :: As' => `(t1, env') <- encode_A' a env; `(t2, env'') <- AlignedEncodeList As' env'; Some (ByteString_enqueue_ByteString t1 t2, env'') end) s c) as [ [? ?] | ] eqn: ?; simpl in *; try discriminate. eapply IHs; eauto. + eapply a0; eauto. - induction s; intros; simpl; eauto. + injections; reflexivity. + destruct X as [encode_A' [? [? ?] ] ]; simpl in *. destruct (encode_A' a env) as [ [? ?] | ] eqn: ?; simpl in *; try discriminate. destruct ((fix AlignedEncodeList (As : list A) (env : CacheFormat) {struct As} : option (ByteString * CacheFormat) := match As with | [] => Some (ByteString_id, env) | a :: As' => `(t1, env') <- encode_A' a env; `(t2, env'') <- AlignedEncodeList As' env'; Some (ByteString_enqueue_ByteString t1 t2, env'') end)) as [ [? ?] | ] eqn: ?; simpl in *; try discriminate. injections. erewrite padding_ByteString_enqueue_ByteString, e, IHs; eauto. - unfold EncodeMEquivAlignedEncodeM; intros. generalize (le_refl (length s)); remember (length s) eqn: s_eq; rewrite s_eq at 1; clear s_eq. revert s env idx. induction n; intros ? ? ? le_s. + destruct s; simpl in le_s; try solve [inversion le_s]. repeat apply conj; intros. * injections; simpl in v; pattern v; apply case0; simpl. setoid_rewrite (proj2 (PeanoNat.Nat.ltb_lt idx (S idx + m))); try Omega.omega. eexists _; split. revert v1; rewrite <- (plus_n_O idx); intro; reflexivity. pose proof mempty_left as H'; simpl in H'; rewrite H', build_aligned_ByteString_append; reflexivity. * injections; rewrite length_ByteString_ByteString_id in H0. unfold AlignedEncodeList; simpl. destruct (NPeano.Nat.ltb idx (S numBytes')) eqn: ?; eauto. apply PeanoNat.Nat.ltb_lt in Heqb; Omega.omega. * injections; simpl in H0; congruence. * discriminate. + destruct s; simpl in le_s; try solve [inversion le_s]. * repeat apply conj; intros. -- injections; simpl in v; pattern v; apply case0; simpl. setoid_rewrite (proj2 (PeanoNat.Nat.ltb_lt idx (S idx + m))); try Omega.omega. eexists _; split. revert v1; rewrite <- (plus_n_O idx); intro; reflexivity. pose proof mempty_left as H'; simpl in H'; rewrite H', build_aligned_ByteString_append; reflexivity. -- injections; rewrite length_ByteString_ByteString_id in H0. unfold AlignedEncodeList; simpl. destruct (NPeano.Nat.ltb idx (S numBytes')) eqn: ?; eauto. apply PeanoNat.Nat.ltb_lt in Heqb; Omega.omega. -- injections; simpl in H0; congruence. -- discriminate. * assert ((forall (s : A * {As : list A & le (length As) n} ) (env : CacheFormat) (t : ByteString) (env' : CacheFormat), (projT1 X ∘ fst) s env = Some (t, env') -> padding t = 0)) as H'. { destruct X; clear IHn; simpl in *; intuition eauto. } assert (EncodeMEquivAlignedEncodeM (projT1 X ∘ fst) (fun (sz : nat) (t : ByteBuffer.t sz) (idx : nat) (s : A * {As : list A & le (length As) n}) (env : CacheFormat) => encode_A sz t idx (fst s) env)) as H''. { destruct X; clear IHn; simpl in *; intuition eauto. unfold EncodeMEquivAlignedEncodeM; intros ? [? ?] ?; unfold Basics.compose; simpl. apply H2; eauto. } assert (EncodeMEquivAlignedEncodeM (S := A * {As : list A & le (length As) n}) ((fix AlignedEncodeList (As : list A) (env : CacheFormat) {struct As} : option (ByteString * CacheFormat) := match As with | [] => Some (mempty, env) | a :: As' => `(t1, env') <- projT1 X a env; `(t2, env'') <- AlignedEncodeList As' env'; Some (mappend t1 t2, env'') end) ∘ (@projT1 _ _) ∘ snd ) (fun (sz : nat) (t : ByteBuffer.t sz) (idx : nat) (s : A * {As : list A & le (length As) n}) (env : CacheFormat) => AlignedEncodeList encode_A sz t idx (projT1 (snd s)) env)) as H'''. { unfold EncodeMEquivAlignedEncodeM; intros ? [? [? ?] ] ?; simpl; eauto. } apply le_S_n in le_s. pose proof (Append_EncodeMEquivAlignedEncodeM _ _ _ _ H' H'' H''' env (a, existT _ s le_s) idx); clear H' H'' H'''. intuition. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.Strings.String Coq.Arith.Mult Coq.Vectors.Vector Fiat.Common.SumType Fiat.Common.BoundedLookup Fiat.Common.ilist Fiat.Common.DecideableEnsembles Fiat.Common.IterateBoundedIndex Fiat.Common.Tactics.CacheStringConstant Fiat.Computation 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.DomainNameOpt Fiat.Narcissus.Formats.Vector Fiat.Narcissus.BinLib.AlignedByteString Fiat.Narcissus.BinLib.AlignWord Fiat.Narcissus.BinLib.AlignedDecoders Fiat.Narcissus.BinLib.AlignedEncodeMonad Fiat.Narcissus.BinLib.AlignedDecodeMonad Fiat.Narcissus.BaseFormats Bedrock.Word