proposition: Lemma EncodeMEquivAlignedEncodeMForChecksum {S A} (enc1' enc2' enc3' : EncodeM S ByteString) (encA' : A -> EncodeM S ByteString) (f' : ByteString -> A) (enc1 enc2 enc3 : forall sz, AlignedEncodeM sz) (encA : A -> forall sz, AlignedEncodeM sz) (f : nat -> forall {sz}, Vector.t (word 8) sz -> nat -> A) (enc1_OK : EncodeMEquivAlignedEncodeM enc1' enc1) (enc2_OK : EncodeMEquivAlignedEncodeM enc2' enc2) (enc3_OK : EncodeMEquivAlignedEncodeM enc3' enc3) (encA_OK : forall a, EncodeMEquivAlignedEncodeM (encA' a) (encA a)) (enc1'_aligned : forall s ce t ce', enc1' s ce = Some (t, ce') -> padding t = 0) (enc2'_aligned : forall s ce t ce', enc2' s ce = Some (t, ce') -> padding t = 0) (enc3'_aligned : forall s ce t ce', enc3' s ce = Some (t, ce') -> padding t = 0) (encA'_aligned : forall a s ce t ce', encA' a s ce = Some (t, ce') -> padding t = 0) (enc'_sz_eq : forall s a ce t1 ce1 t2 ce2, enc2' s ce = Some (t1, ce1) -> encA' a s ce = Some (t2, ce2) -> bin_measure t1 = bin_measure t2) (f_OK : forall (b : ByteString) idx (v1 : Vector.t Core.char idx) m (v2 : Vector.t Core.char m) (v : Vector.t Core.char (idx + ((numBytes b) + m))), ByteString_enqueue_ByteString (build_aligned_ByteString v1) (ByteString_enqueue_ByteString b (build_aligned_ByteString v2)) = build_aligned_ByteString v -> f' b = f (numBytes b) v idx) : EncodeMEquivAlignedEncodeM (fun s ce => `(p, _) <- sequence_Encode enc1' (sequence_Encode enc2' enc3') s ce; (fun a => (sequence_Encode enc1' (sequence_Encode (encA' a) enc3'))) (f' p) s ce) (fun sz => EncodeAgain (enc1 sz >> enc2 sz >> enc3 sz) (fun idx' v idx s => (fun a sz => enc1 sz >> encA a sz >> enc3 sz) (f (idx'-idx) v idx) sz v idx s))%AlignedEncodeM.
proof: Proof. apply EncodeMEquivAlignedEncodeMDep; eauto; intros; repeat (apply Append_EncodeMEquivAlignedEncodeM; eauto); solve_seq_padding. apply sequence_Encoding_inv in H. apply sequence_Encoding_inv in H0. destruct_conjs. apply sequence_Encoding_inv in H9. apply sequence_Encoding_inv in H4. destruct_conjs. subst. rewrite !mappend_measure. simpl in *. destruct_unit. substss. injections. eauto. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.Strings.String Coq.Vectors.Vector Coq.ZArith.ZArith Fiat.Common.SumType Fiat.Common.EnumType Fiat.Common.BoundedLookup Fiat.Common.ilist Fiat.Computation Fiat.QueryStructure.Specification.Representation.Notations Fiat.QueryStructure.Specification.Representation.Heading Fiat.QueryStructure.Specification.Representation.Tuple Fiat.Narcissus.BinLib.AlignedByteString Fiat.Narcissus.BinLib.AlignWord Fiat.Narcissus.BinLib.AlignedList Fiat.Narcissus.BinLib.AlignedDecoders Fiat.Narcissus.BinLib.AlignedDecodeMonad Fiat.Narcissus.BinLib.AlignedEncodeMonad Fiat.Narcissus.Common.Specs Fiat.Narcissus.Common.WordFacts Fiat.Narcissus.Common.ComposeCheckSum Fiat.Narcissus.Common.ComposeIf Fiat.Narcissus.Common.ComposeOpt Fiat.Narcissus.Formats Fiat.Narcissus.BaseFormats Fiat.Narcissus.Stores.EmptyStore Bedrock.Word