proposition: Lemma decode_unused_word_aligned_ByteString_overflow : forall {sz'} (b : t (word 8) sz') {sz} (cd : CacheDecode), lt sz' sz -> decode_unused_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_unused_word, WordOpt.decode_word, FMapFormat.Compose_Decode in *. rewrite <- mult_n_Sm, plus_comm. rewrite decode_word_plus'. rewrite aligned_decode_char_eq; simpl. destruct (decode_word' (8 * sz) (build_aligned_ByteString b)) as [ [? ?] | ]; simpl in *; eauto. discriminate. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.ZArith.ZArith Coq.Strings.String Coq.Arith.Mult Coq.Vectors.Vector Fiat.Common.SumType Fiat.Common.BoundedLookup Fiat.Common.ilist Fiat.Common.DecideableEnsembles Fiat.Computation Fiat.QueryStructure.Specification.Representation.Notations Fiat.QueryStructure.Specification.Representation.Heading Fiat.QueryStructure.Specification.Representation.Tuple Fiat.Narcissus.BinLib.AlignedEncodeMonad Fiat.Narcissus.BinLib.AlignedByteString Fiat.Narcissus.BinLib.AlignWord Fiat.Narcissus.BinLib.AlignedString Fiat.Narcissus.BinLib.AlignedDecodeMonad Fiat.Narcissus.Common.Specs Fiat.Narcissus.Common.ComposeOpt Fiat.Narcissus.Formats.WordOpt Fiat.Narcissus.Formats.NatOpt Fiat.Narcissus.Formats.StringOpt Fiat.Narcissus.Formats.EnumOpt Fiat.Narcissus.Formats.FixListOpt Fiat.Narcissus.Formats.SumTypeOpt Fiat.Narcissus.Formats.EnumOpt Fiat.Narcissus.Formats.DomainNameOpt Fiat.Common.IterateBoundedIndex Fiat.Common.Tactics.CacheStringConstant Fiat.Narcissus.Formats.IPChecksum Fiat.Narcissus.Common.ComposeCheckSum Bedrock.Word