proposition: Lemma padding_ByteString_queue_into_ByteString : forall l : BitString, padding (queue_into_ByteString l) = (List.length l) mod 8.
proof: Proof. unfold queue_into_ByteString; intro. replace (List.length l mod 8) with ((List.length l mod 8 + (padding ByteString_id) mod 8) mod 8). generalize ByteString_id. induction l. - intros; simpl; rewrite !padding_mod_8; reflexivity. - intros. simpl; rewrite IHl. rewrite <- !Nat.add_mod by omega. destruct (le_lt_dec (padding b) 6). erewrite ByteString_enqueue_simpl; simpl. f_equal; omega. unfold ByteString_enqueue. pose proof (paddingOK b). destruct (eq_nat_dec (padding b) 7); try omega. simpl. rewrite e. replace (S (List.length l + 7)) with (List.length l + 8) by omega. rewrite Nat.add_mod with (b := 8) by omega. unfold modulo at 4; simpl. rewrite Nat.add_mod by omega; f_equal. - rewrite <- !Nat.add_mod by omega. simpl; f_equal; omega. Unshelve. omega. 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.Formats.ByteBuffer Coq.Strings.String Coq.Vectors.Vector Fiat.Narcissus.Formats.WordOpt Fiat.Common.Equality