proposition: Lemma encode_word'_padding' : forall sz (w : word sz) bs, padding (encode_word' _ w bs) = NPeano.modulo (sz + padding bs) 8.
proof: Proof. intros. rewrite <- padding_mod_8. revert bs; induction w; intros. - reflexivity. - simpl encode_word'. rewrite ByteString_enqueue_padding_eq. replace (S n + padding bs) with (1 + (n + padding bs)) by omega. rewrite <- Nat.add_mod_idemp_r by omega. rewrite <- IHw. rewrite !Nat.add_mod_idemp_r by omega. replace (S (padding (encode_word' n w bs))) with (1 + (padding (encode_word' n w bs))) by omega. rewrite <- Nat.add_mod_idemp_r at 1 by omega. rewrite NPeano.Nat.mod_mod by omega. rewrite Nat.add_mod_idemp_r by omega; reflexivity. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.ZArith.ZArith Coq.Strings.String Coq.Vectors.Vector Fiat.Common.SumType Fiat.Common.EnumType Fiat.Common.BoundedLookup Fiat.Common.ilist Fiat.Computation Fiat.QueryStructure.Specification.Representation.Notations Fiat.QueryStructure.Specification.Representation.Heading Fiat.QueryStructure.Specification.Representation.Tuple Fiat.Narcissus.BinLib.Core Fiat.Narcissus.BinLib.AlignedByteString Fiat.Narcissus.Common.Specs Fiat.Narcissus.Common.WordFacts Fiat.Narcissus.Common.ComposeCheckSum Fiat.Narcissus.Common.ComposeIf Fiat.Narcissus.Common.ComposeOpt Fiat.Narcissus.Formats.Option Fiat.Narcissus.Formats.FixListOpt Fiat.Narcissus.Stores.EmptyStore Fiat.Narcissus.Formats.Bool Fiat.Narcissus.Formats.NatOpt Fiat.Narcissus.Formats.Vector Fiat.Narcissus.Formats.EnumOpt Fiat.Narcissus.Formats.SumTypeOpt Fiat.Narcissus.Formats.InternetChecksum Fiat.Narcissus.Formats.WordOpt Fiat.Narcissus.BaseFormats Bedrock.Word