proposition: Lemma CorrectAlignedEncoderForFormatByteBuffer (encode_word_OK : forall (a : word (1 * 8)) (l : list (word (1 * 8))) (env : CacheFormat) (tenv' tenv'' : ByteString * CacheFormat), format_word a env ∋ tenv' -> format_list format_word l (snd tenv') ∋ tenv'' -> exists tenv3 tenv4 : ByteString * CacheFormat, projT1 (CorrectAlignedEncoderForFormatNChar addE_addE_plus addE_0) a env = Some tenv3 /\ format_list format_word l (snd tenv3) ∋ tenv4) : CorrectAlignedEncoder format_bytebuffer AlignedEncodeByteBuffer.
proof: Proof. eapply refine_CorrectAlignedEncoder with (format' := fun s env => format_list format_word (ByteBuffer.to_list (projT2 s)) env); [ | eapply CorrectAlignedEncoder_morphism with (encode := fun sz v idx w c => AlignedEncodeList (@SetCurrentByte _ _) sz v idx (ByteBuffer.to_list (projT2 w)) c)]. - intros [? ?]; clear; split. + revert env; induction t; simpl; intros. * reflexivity. * unfold format_bytebuffer in *; simpl in *; apply refine_under_bind; intros. unfold Bind2; rewrite IHt; reflexivity. + unfold format_bytebuffer, Bind2 in *. intros; intro; eapply (H v). clear H; revert env v H0; induction t; simpl; intros. * eapply H0. * unfold Bind2 in *. computes_to_inv. computes_to_econstructor; eauto. computes_to_econstructor; eauto. rewrite H0''; eauto. - apply EquivFormat_reflexive. - intros ? ? ? [n t]; revert sz v idx; induction t. + simpl; intros. unfold buffer_blit_buffer. destruct (Coq.Init.Nat.leb (idx + 0) sz) eqn: ?; intros. * eapply PeanoNat.Nat.leb_le in Heqb. rewrite (proj2 (PeanoNat.Nat.ltb_lt idx (S sz))) by Omega.omega. unfold ReturnAlignedEncodeM. simpl. rewrite <- (addE_0 c) at 2. simpl; repeat f_equal; try Omega.omega. * eapply PeanoNat.Nat.leb_gt in Heqb. rewrite (proj2 (PeanoNat.Nat.ltb_ge idx (S sz))) by Omega.omega. reflexivity. + simpl; intros. unfold buffer_blit_buffer. destruct (Coq.Init.Nat.leb (idx + (S n)) sz) eqn: ?; intros. * eapply PeanoNat.Nat.leb_le in Heqb. unfold SetCurrentByte at 1. rewrite (proj2 (PeanoNat.Nat.ltb_lt idx sz)) by Omega.omega; simpl. rewrite <- IHt. simpl. unfold buffer_blit_buffer. destruct (Coq.Init.Nat.leb (S idx + n) sz) eqn: ?; intros. eapply PeanoNat.Nat.leb_le in Heqb0; simpl; rewrite addE_addE_plus; repeat (f_equal; try Omega.omega). eapply PeanoNat.Nat.leb_gt in Heqb0; Omega.omega. * eapply PeanoNat.Nat.leb_gt in Heqb. unfold SetCurrentByte at 1. destruct (PeanoNat.Nat.ltb idx sz) eqn: ? ; simpl; auto. rewrite <- IHt. unfold AlignedEncodeByteBuffer, buffer_blit_buffer. destruct (Coq.Init.Nat.leb (S idx + n) sz) eqn: ? ; simpl; auto. eapply PeanoNat.Nat.leb_le in Heqb0; eapply PeanoNat.Nat.leb_le in Heqb1; Omega.omega. - eexists (fun s env => _); repeat apply conj; intros; try eapply ((projT2 (CorrectAlignedEncoderForFormatList _ _ (CorrectAlignedEncoderForFormatNChar (sz := 1) addE_addE_plus addE_0) encode_word_OK))); eauto. pose proof (proj2 (proj2 ((projT2 (CorrectAlignedEncoderForFormatList _ _ (CorrectAlignedEncoderForFormatNChar (sz := 1) addE_addE_plus addE_0) encode_word_OK))))). unfold EncodeMEquivAlignedEncodeM in *; intros ? [? ?] ?; simpl in *. intuition. eapply H; eauto. eapply (proj1 (proj2 (H _ _ _))); eauto. eapply (proj1 (proj2 (proj2 (H _ _ _)))); eauto. eapply (proj2 (proj2 (proj2 (H _ _ _)))); eauto. 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.BinLib.AlignedList Fiat.Narcissus.BaseFormats Bedrock.Word