proposition: Lemma AlignedDecodeChar {C} {numBytes} : forall (v : ByteBuffer.t (S numBytes)) (t : (word 8 * ByteString * CacheDecode) -> C) (e : C) cd, Ifopt (decode_word (monoidUnit := ByteString_QueueMonoidOpt) (sz := 8) (build_aligned_ByteString v) cd) as w Then t w Else e = LetIn (Vector.nth v Fin.F1) (fun w => t (w, build_aligned_ByteString (snd (Vector_split 1 _ v)), addD cd 8)).
proof: Proof. unfold LetIn; intros. unfold decode_word, WordOpt.decode_word. rewrite aligned_decode_char_eq; simpl. f_equal. pattern numBytes, v; apply Vector.caseS; simpl; intros. reflexivity. 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