proposition: Lemma CorrectAlignedEncoderForChecksum {S} checksum_sz (checksum_valid : nat -> ByteString -> Prop) (format_A format_B : FormatM S ByteString) (encode_A encode_B : forall sz, AlignedEncodeM sz) (encode_C' : forall sz, AlignedEncodeM sz) (encode_C : word checksum_sz -> forall sz, AlignedEncodeM sz) (encoder_A_OK : CorrectAlignedEncoder format_A encode_A) (encoder_B_OK : CorrectAlignedEncoder format_B encode_B) (f : nat -> forall {sz}, Vector.t (word 8) sz -> nat -> word checksum_sz) (f_OK : forall idx n m (t : Vector.t Core.char n) (v1 : Vector.t Core.char idx) (v2 : Vector.t Core.char m), f n t 0 = f n (v1 ++ t ++ v2) idx) (enc2' : EncodeM S ByteString) (enc2_OK : EncodeMEquivAlignedEncodeM enc2' encode_C') (encode_C_OK : forall a, EncodeMEquivAlignedEncodeM ((fun a _ ce => Some (format_checksum _ _ _ _ a, ce)) a) (encode_C a)) (enc2'_aligned : forall s ce t ce', enc2' s ce = Some (t, ce') -> padding t = 0) n1 (format_B_sz_eq : forall s ce t ce', format_B s ce ∋ (t, ce') -> bin_measure t = n1) (checksum_sz_OK : checksum_sz mod 8 = 0) (checksum_sz_OK' : forall s ce t ce', enc2' s ce = Some (t, ce') -> checksum_sz = bin_measure t) (checksum_OK : forall s ce b' ce', enc2' s ce = Some (b', ce') -> forall b1 b3 ext, (exists s ce ce', format_B s ce ∋ (b1, ce')) -> (exists s ce ce', format_A s ce ∋ (b3, ce')) -> let a := (f_bit_aligned_free f) (mappend b1 (mappend b' b3)) in let b2 := format_checksum _ _ _ checksum_sz a in checksum_valid (bin_measure (mappend b1 (mappend b2 b3))) (mappend (mappend b1 (mappend b2 b3)) ext)) (checksum_OK' : forall s ce, enc2' s ce = None -> forall b1 b2 b3 ext, ~checksum_valid (bin_measure (mappend b1 (mappend b2 b3))) (mappend (mappend b1 (mappend b2 b3)) ext)) : CorrectAlignedEncoder (format_B ThenChecksum checksum_valid OfSize checksum_sz ThenCarryOn format_A) (fun sz => EncodeAgain (encode_B sz >> encode_C' sz >> encode_A sz) (fun idx' v idx s => encode_C (f (idx'-idx) v idx) sz v (idx+n1/8) s))%AlignedEncodeM.
proof: Proof. destruct encoder_A_OK as [enc3' [HA1 [HA2 HA3]]]. destruct encoder_B_OK as [enc1' [HB1 [HB2 HB3]]]. exists (fun s ce => `(p, _) <- sequence_Encode enc1' (sequence_Encode enc2' enc3') s ce; (fun a => (sequence_Encode enc1' (sequence_Encode ((fun a _ ce => Some (format_checksum _ _ _ _ a, ce)) a) enc3'))) ((f_bit_aligned_free f) p) s ce). split; [| split]; intros. - unfold composeChecksum, sequence_Encode. split; intros; simpl in *. + intros [? ?]. intros. computes_to_inv. injections. destruct enc1' eqn:Henc1; [| discriminate]; destruct_conjs; simpl in *. destruct enc2' eqn:Henc2; [| discriminate]; destruct_conjs; simpl in *. destruct enc3' eqn:Henc3; [| discriminate]; destruct_conjs; simpl in *. destruct_unit. rewrite Henc3 in H. simpl in *. injections. repeat computes_to_econstructor; eauto. edestruct HB1. apply H in Henc1. apply Henc1. repeat computes_to_econstructor; eauto. simpl. edestruct HA1. apply H in Henc3. apply Henc3. repeat computes_to_econstructor; eauto. intros. eapply checksum_OK; eauto. repeat eexists. simpl. apply HB1 in Henc1. eauto. repeat eexists. simpl. apply HA1 in Henc3. eauto. simpl. apply eq_ret_compute. repeat f_equal. + intro. unfold Bind2 in H0. computes_to_inv. destruct_conjs. injections. simpl in *. destruct_unit. destruct enc1' eqn:Henc1; destruct_conjs; simpl in *; destruct_unit. destruct enc2' eqn:Henc2; destruct_conjs; simpl in *; destruct_unit. destruct enc3' eqn:Henc3; destruct_conjs; simpl in *; destruct_unit. discriminate. edestruct HA1. intuition eauto. intuition eauto. edestruct HB1. intuition eauto. - destruct sequence_Encode; [| discriminate]; destruct_conjs; simpl in *. eapply sequence_Encoding_padding_0; try apply H; eauto. intros. eapply sequence_Encoding_padding_0; try apply H0; eauto. intros. simpl in *. injections. unfold format_checksum. rewrite encode_word'_padding. eauto. - eapply EncodeMEquivAlignedEncodeM_morphism; cycle 1. apply EncodeMEquivAlignedEncodeMForChecksum with (encA' := (fun a _ ce => Some (format_checksum _ _ _ _ a, ce))); eauto. + intros. injections. unfold format_checksum. rewrite encode_word'_padding. eauto. + intros. injections. unfold format_checksum. rewrite length_encode_word'. rewrite measure_mempty. apply checksum_sz_OK' in H. omega. + unfold f_bit_aligned_free. instantiate (1:=f). intros. assert (padding b = 0) as L1. { apply (f_equal padding) in H. simpl in H. rewrite padding_ByteString_enqueue_aligned_ByteString in H; eauto. rewrite ByteString_enqueue_ByteString_padding_eq in H. simpl padding in H. rewrite (Nat.mod_add _ 0 8) in H; eauto. rewrite Nat.mod_small in H; eauto. destruct b. simpl in *. auto. } assert (b = build_aligned_ByteString (byteString b)) as L2. { revert L1. clear. intros. destruct b. simpl. unfold build_aligned_ByteString. simpl in *. subst. f_equal. eauto using shatter_word_0. apply Core.le_uniqueness_proof. } revert L2 H. revert v. generalize (byteString b). generalize (numBytes b). intros. rewrite L2 in H. rewrite <- !build_aligned_ByteString_append in H. apply build_aligned_ByteString_inj in H. subst. eauto. + intros. unfold EncodeAgain. set (fun sz => encode_C' sz >> encode_A sz)%AlignedEncodeM as enc'. set (fun sz => encode_B sz >> enc' sz)%AlignedEncodeM as enc. match goal with | |- context[Ifopt ?b _ _ _ _ as _ Then _ Else _] => replace b with (enc sz) by reflexivity end. destruct enc eqn:?; eauto. destruct_conjs. simpl. unfold AppendAlignedEncodeM. edestruct @AlignedEncoder_inv2 as [n2 [n3 [t1 [t23 [v23 ?]]]]]; try apply Heqa. apply Append_EncodeMEquivAlignedEncodeM. 2 : eauto. eauto. apply Append_EncodeMEquivAlignedEncodeM. 2 : eauto. eauto. eauto. solve_seq_padding. destruct_conjs. subst. simpl in *. edestruct @AlignedEncoder_append_inv with (enc1:=encode_B) as [nB [nC [nC3 [tB [tC3 [vB [vC3 [?ce ?]]]]]]]]. 5 : apply H0. 3 : apply Append_EncodeMEquivAlignedEncodeM. all : eauto. solve_seq_padding. destruct_conjs. subst. simpl in *. destruct H. simpl in *. assert (encode_B (idx + (nB + (nC + nC3))) (t1 ++ vB ++ vC3) idx w c = Some (t1 ++ vB ++ vC3, idx+nB, ce)). { assert (idx + nB + (nC + nC3) = idx + (nB + (nC + nC3))) as L by omega. rewrite Vector_append_assoc with (H:=L). destruct L. simpl. epose proof AlignedEncoder_extr as H'. eapply H'; eauto. clear H'. eapply @AlignedEncoder_fixed; eauto. eapply AlignedEncoder_extl; eauto. } rewrite H. simpl. assert (nB = n1/8). { erewrite <- format_B_sz_eq; eauto. epose proof AlignedEncoder_inv0 as L. eapply L in H1; eauto. clear L. instantiate (1:=build_aligned_ByteString vB). rewrite length_ByteString_no_padding; eauto. rewrite Nat.mul_comm. rewrite Nat.div_mul by auto. reflexivity. eapply HB1; eauto. eauto using AlignedEncoder_inv0. } destruct H3. destruct_unit. destruct encode_C eqn:?; eauto. destruct_conjs. simpl in *. edestruct @AlignedEncoder_append_inv with (enc1:=encode_C') as [nC' [nA [nA3 [tC [tA3 [vC [vA3 [?ce ?]]]]]]]]; try apply H2; eauto. destruct_conjs. subst. simpl in *. destruct H3. simpl in *. rename nC' into nC. match goal with | H : encode_C ?a _ _ _ _ _ = _ |- _ => edestruct @AlignedEncoder_inv with (enc:=(encode_C a)) as [nC' [n3' [t1C [tC' [tC3 [vC' ?]]]]]] end; eauto. intros. simpl in *. injections. unfold format_checksum. rewrite encode_word'_padding. eauto. destruct_conjs. assert (nC = nC'). { injections. assert (checksum_sz = 8 * nC'). eapply (f_equal bin_measure) in H12. simpl in *. unfold format_checksum in H12. rewrite length_encode_word' in H12. rewrite measure_mempty in H12. unfold length_ByteString in H12. simpl in H12. omega. assert (checksum_sz = 8 * nC). epose proof AlignedEncoder_inv0 as L. eapply L in H4; eauto. clear L. apply checksum_sz_OK' in H4. unfold length_ByteString in H4. simpl in H4. omega. omega. } subst nC'. assert (n3' = nA + nA3) as L by omega. subst n3'. assert (encode_A (idx + (nB + (nC + (nA + nA3)))) t n w c = Some (t, n+nA, c)). { rewrite (Vector_append_assoc _ _ _ H3) in H8. clear Heqa0. destruct H3. simpl in *. subst. apply Vector_append_inj in H8. destruct_conjs. apply Vector_append_inj in H7. destruct_conjs. subst. assert (idx + nB + nC + (nA + nA3) = idx + nB + (nC + (nA + nA3))) as L by omega. rewrite (Vector_append_assoc _ _ _ L). destruct L. simpl. epose proof AlignedEncoder_extl as L. eapply L; eauto. clear L. destruct_unit. eapply @AlignedEncoder_fixed; eauto. } rewrite H11. simpl. reflexivity. Unshelve. 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