proposition: Lemma CorrectAlignedEncoderForThenC (format_A format_B : FormatM S ByteString) (encode_A : forall sz, AlignedEncodeM sz) (encode_B : forall sz, AlignedEncodeM sz) (encoder_A_OK : CorrectAlignedEncoder format_A encode_A) (encoder_B_OK : CorrectAlignedEncoder format_B encode_B) (encoder_A_OK' : forall (s : S) (env : CacheFormat) (tenv' tenv'' : ByteString * CacheFormat), format_B s env ∋ tenv' -> format_A s (snd tenv') ∋ tenv'' -> exists tenv3 tenv4 : _ * CacheFormat, projT1 encoder_B_OK s env = Some tenv3 /\ format_A s (snd tenv3) ∋ tenv4) : CorrectAlignedEncoder (format_B ++ format_A) (fun sz => AppendAlignedEncodeM (encode_B sz) (encode_A sz)).
proof: Proof. unfold CorrectAlignedEncoder; intros. destruct encoder_A_OK as [encoder_A ?], encoder_B_OK as [encoder_B ?]; intuition. destruct a0 as [? [? ?] ]. eexists (sequence_Encode encoder_B encoder_A); split; [ | split]; intros; simpl in *. 3: eapply Append_EncodeMEquivAlignedEncodeM. 4: apply e0. 4: apply H2. 3: apply e. pose proof (fun H a => CorrectEncoder_sequence format_B format_A encoder_B encoder_A H encoder_A_OK' a). destruct H0. - unfold CorrectEncoder; split; intros. specialize (proj1 (a _ _) _ _ H0); intro. unfold refine in H3; eauto. specialize (proj2 (a _ _) H0); intro. intro. eapply H3; eauto. - unfold CorrectEncoder; split; intros. specialize (proj1 (H _ _) _ _ H0); intro. unfold refine in H3; eauto. specialize (proj2 (H _ _) H0); intro. intro. eapply H3; eauto. - split; intros. + apply H0 in H4. intros ? ?; computes_to_inv; subst. eauto. + destruct benv'. eapply H3 in H4. eauto. - unfold sequence_Format, sequence_Encode, Bind2 in *. apply_in_hyp DecodeBindOpt_inv; destruct_ex; split_and. symmetry in H4. apply_in_hyp DecodeBindOpt_inv; destruct_ex; split_and. injections. rewrite padding_ByteString_enqueue_aligned_ByteString; eauto. Defined.
imports: Fiat.Common.Coq__8_4__8_5__Compat Bedrock.Word Coq.ZArith.ZArith Coq.NArith.NArith Coq.Arith.Arith Coq.Numbers.Natural.Peano.NPeano Coq.Logic.Eqdep_dec Fiat.Common.BoundedLookup Fiat.Narcissus.Common.Specs Fiat.Narcissus.Common.ComposeOpt Fiat.Narcissus.Common.ComposeIf Fiat.Narcissus.BaseFormats Fiat.Narcissus.BinLib.Core Fiat.Narcissus.BinLib.AlignedByteString