proposition: Lemma decode_word_aligned_ByteString_overflow {sz'} : forall (b : t (word 8) sz') {sz : nat} (cd : CacheDecode), lt sz' sz -> decode_word (sz := 8 * sz) (build_aligned_ByteString b) cd = None.
proof: Proof. induction b; intros. - unfold build_aligned_ByteString; simpl. inversion H; subst; reflexivity. - destruct sz; try omega. apply lt_S_n in H. pose proof (IHb _ cd H). unfold decode_word, WordOpt.decode_word. rewrite <- mult_n_Sm, plus_comm. rewrite decode_word_plus'. rewrite (@aligned_decode_char_eq' _ 0). simpl. unfold build_aligned_ByteString, decode_word in *. simpl in H0. first [destruct (decode_word' (sz + (sz + (sz + (sz + (sz + (sz + (sz + (sz + 0)))))))) {| padding := 0; front := WO; paddingOK := build_aligned_ByteString_subproof ; numBytes := n; byteString := b |}) as [ [? ?] | ] | destruct (decode_word' (sz + (sz + (sz + (sz + (sz + (sz + (sz + (sz + 0)))))))) {| padding := 0; front := WO; paddingOK := build_aligned_ByteString_subproof n b; numBytes := n; byteString := b |}) as [ [? ?] | ]] ; simpl in *; try congruence. 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