proposition: Theorem ByteBuffer_decode_correct : forall n, CorrectDecoder monoid (fun ls => projT1 ls = n) (fun ls => projT1 ls = n) eq format_bytebuffer (decode_bytebuffer n) P format_bytebuffer.
proof: Proof. unfold format_bytebuffer; split; intros. { eapply (fun H' => proj1 (Vector_decode_correct (fun _ => True) _ decode_word P H' _)) in H1; eauto. instantiate (1 := ext) in H1; destruct H1 as [? [? ?] ]; eexists _, _; split; eauto. split_and; unfold id in *; destruct s; unfold decode_bytebuffer; subst; rewrite H2; simpl in *; intuition eauto. intuition eauto. subst; eauto. apply Word_decode_correct; eauto. } { destruct v; simpl in *. unfold decode_bytebuffer in H1. destruct (decode_Vector decode_word n t env') as [ [ [? ?] ? ] | ] eqn: H'; try discriminate; injection H1; intros; subst; clear H1. apply inj_pair2_eq_dec in H4; try decide equality; subst. eapply (fun H' H'' => proj2 (Vector_decode_correct (fun _ => True) format_word decode_word P H' H'')) in H'; try eassumption; destruct H'; destruct_ex; split_and; subst; intuition eauto. unfold id in *; subst; eexists _, _; simpl; intuition eauto. apply Word_decode_correct; eauto. } Defined.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.Arith.Peano_dec Coq.Logic.Eqdep_dec Coq.ZArith.ZArith Fiat.Narcissus.Common.Specs Fiat.Narcissus.Formats.WordOpt Fiat.Narcissus.Formats.Vector Fiat.Narcissus.BinLib.Core Bedrock.Word