proposition: Lemma AlignedDecodeNUnusedCharM (addD_O : forall cd, addD cd 0 = cd) {m} : DecodeMEquivAlignedDecodeM (decode_unused_word (sz := m * 8)) (fun numBytes => SkipCurrentBytes m).
proof: Proof. induction m. - unfold decode_unused_word; simpl; pose proof (@Return_DecodeMEquivAlignedDecodeM). eapply DecodeMEquivAlignedDecodeM_trans; intros; try rewrite addD_O. eapply H. unfold Compose_Decode, DecodeBindOpt, BindOpt. simpl; rewrite addD_O; reflexivity. simpl; reflexivity. - Local Arguments decode_word' : simpl never. Local Arguments plus : simpl never. unfold decode_unused_word; simpl. eapply DecodeMEquivAlignedDecodeM_trans; intros; try eapply AlignedDecodeMEquiv_refl. Focus 2. { instantiate (1 := fun b cd => `(w, v', cd') <- decode_unused_word (sz := 8) b cd; `(w', v'', cd') <- decode_unused_word (sz := m * 8) v' cd'; Some ((), v'', cd')); simpl. unfold decode_unused_word, Compose_Decode, DecodeBindOpt, BindOpt. unfold decode_word, decode_word'; simpl in *. destruct (ByteString_dequeue b) as [ [? ?] | ]; simpl in *; try discriminate; eauto. destruct (ByteString_dequeue b1) as [ [? ?] | ]; simpl in *; try discriminate; eauto. destruct (ByteString_dequeue b3) as [ [? ?] | ]; simpl in *; try discriminate; eauto. destruct (ByteString_dequeue b5) as [ [? ?] | ]; simpl in *; try discriminate; eauto. destruct (ByteString_dequeue b7) as [ [? ?] | ]; simpl in *; try discriminate; eauto. destruct (ByteString_dequeue b9) as [ [? ?] | ]; simpl in *; try discriminate; eauto. rewrite !DecodeBindOpt_assoc. destruct (ByteString_dequeue b11) as [ [? ?] | ]; simpl in *; try discriminate; eauto. destruct (ByteString_dequeue b13) as [ [? ?] | ]; simpl in *; try discriminate; eauto. destruct (ByteString_dequeue b15) as [ [? ?] | ]; simpl in *; try discriminate; eauto; intros; rewrite !DecodeBindOpt_assoc. simpl; match goal with |- context [DecodeBindOpt ?z] => destruct z as [ [? ?] | ] eqn: ? ; simpl in *; try discriminate end. rewrite addD_addD_plus; reflexivity. eauto. simpl; match goal with |- context [DecodeBindOpt ?z] => destruct z as [ [? ?] | ] eqn: ? ; simpl in *; try discriminate end. rewrite addD_addD_plus; reflexivity. eauto. } all: idtac. repeat (intros; eapply Bind_DecodeMEquivAlignedDecodeM); eauto using @Return_DecodeMEquivAlignedDecodeM. eapply AlignedDecodeUnusedCharM. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.Logic.Eqdep_dec Fiat.Computation Fiat.Narcissus.Common.Specs Fiat.Narcissus.Common.ComposeOpt Fiat.Narcissus.Formats.WordOpt Fiat.Narcissus.Formats.EnumOpt Fiat.Narcissus.Formats.Sequence Fiat.Narcissus.BaseFormats Fiat.Narcissus.BinLib.AlignedEncodeMonad Coq.Vectors.Vector Coq.ZArith.ZArith Bedrock.Word Fiat.Narcissus.BinLib.AlignedByteString Fiat.Narcissus.BinLib.AlignedDecodeMonad