proposition: Lemma aligned_decode_unused_char_eq {numBytes} : forall (v : Vector.t _ (S numBytes)), WordOpt.decode_unused_word' (monoidUnit := ByteString_QueueMonoidOpt) 8 (build_aligned_ByteString v) = Some ((), build_aligned_ByteString (Vector.tl v)).
proof: Proof. unfold decode_unused_word'; simpl; intros. etransitivity. apply f_equal with (f := fun z => If_Opt_Then_Else z _ _ ). eapply DecodeBindOpt_under_bind; intros; set_evars; rewrite !DecodeBindOpt_assoc. repeat (unfold H; apply DecodeBindOpt_under_bind; intros; set_evars; rewrite !DecodeBindOpt_assoc). unfold H5; higher_order_reflexivity. simpl. pattern numBytes, v; eapply Vector.caseS; intros; simpl; clear v numBytes. replace (build_aligned_ByteString t) with (ByteString_enqueue_ByteString ByteString_id (build_aligned_ByteString t)). unfold Core.char in h. shatter_word h. pose proof (@dequeue_mappend_opt _ _ _ ByteString_QueueMonoidOpt). rewrite build_aligned_ByteString_cons; simpl. simpl in H7. erewrite H7 with (t := x6) (b' := {| front := WS x (WS x0 (WS x1 (WS x2 (WS x3 (WS x4 (WS x5 WO)))))); byteString := Vector.nil _ |}); simpl. erewrite H7 with (t := x5) (b' := {| front := WS x (WS x0 (WS x1 (WS x2 (WS x3 (WS x4 WO))))); byteString := Vector.nil _ |}); simpl. erewrite H7 with (t := x4) (b' := {| front := WS x (WS x0 (WS x1 (WS x2 (WS x3 WO)))); byteString := Vector.nil _ |}); simpl. erewrite H7 with (t := x3) (b' := {| front := WS x (WS x0 (WS x1 (WS x2 WO))); byteString := Vector.nil _ |}); simpl. erewrite H7 with (t := x2) (b' := {| front := WS x (WS x0 (WS x1 WO)); byteString := Vector.nil _ |}); simpl. erewrite H7 with (t := x1) (b' := {| front := WS x (WS x0 WO); byteString := Vector.nil _ |}); simpl. erewrite H7 with (t := x0) (b' := {| front := WS x WO; byteString := Vector.nil _ |}); simpl. erewrite H7 with (t := x) (b' := {| front := WO; byteString := Vector.nil _ |}); simpl. reflexivity. unfold dequeue_opt. simpl. compute; repeat f_equal; apply Core.le_uniqueness_proof. compute; repeat f_equal; apply Core.le_uniqueness_proof. compute; repeat f_equal; apply Core.le_uniqueness_proof. compute; repeat f_equal; apply Core.le_uniqueness_proof. compute; repeat f_equal; apply Core.le_uniqueness_proof. compute; repeat f_equal; apply Core.le_uniqueness_proof. compute; repeat f_equal; apply Core.le_uniqueness_proof. unfold build_aligned_ByteString. unfold ByteString_dequeue; simpl. repeat f_equal; apply Core.le_uniqueness_proof. apply (@mempty_left _ ByteStringQueueMonoid). 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