proposition: Lemma Return_DecodeMEquivAlignedDecodeM {A : Type} (a : A) : DecodeMEquivAlignedDecodeM (fun (b : ByteString) (cd : CacheDecode) => Some (a, b, cd)) (fun numBytes => ReturnAlignedDecodeM a).
proof: Proof. unfold DecodeMEquivAlignedDecodeM; intros; intuition. - injections; eauto. - discriminate. - discriminate. - unfold ReturnAlignedDecodeM, numBytes; injections. simpl; repeat f_equal; omega. - unfold ReturnAlignedDecodeM in H; injections. assert ((n - numBytes (build_aligned_ByteString v)) = 0) by (unfold numBytes; simpl; omega). rewrite H. setoid_rewrite <- build_aligned_ByteString_append. simpl; eexists (@Vector.nil _); reflexivity. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Bedrock.Word Coq.ZArith.ZArith Coq.NArith.NArith Coq.Arith.Arith Coq.Numbers.Natural.Peano.NPeano Coq.Logic.Eqdep_dec Fiat.Narcissus.Common.Specs Fiat.Narcissus.BinLib.Core Fiat.Narcissus.BinLib.AlignedByteString