proposition: Lemma mappend_ByteString_measure : forall bs bs' : ByteString, length_ByteString (ByteString_append bs bs') = length_ByteString bs + length_ByteString bs'.
proof: Proof. destruct bs as [bs_padding bs_front ? bs_byteString]; simpl. induction bs_byteString. - unfold ByteString_append, length_ByteString at 2; simpl. rewrite NPeano.Nat.add_0_r. induction bs_padding. + simpl; eauto. + simpl; intros. rewrite length_ByteString_push; rewrite IHbs_padding; eauto. omega. - unfold ByteString_append in *; simpl in *. unfold length_ByteString at 2. unfold byteString at 1. intros; rewrite <- plus_assoc, <- (length_ByteString_append (a :: bs_byteString) bs'). simpl fold_right. rewrite length_ByteString_push_char, plus_comm. rewrite <- plus_assoc. simpl padding. unfold length_ByteString in IHbs_byteString. simpl byteString in IHbs_byteString. simpl padding in IHbs_byteString. rewrite length_ByteString_append. unfold length_ByteString at 2. replace (8 * length bs_byteString + (padding bs' + 8 * length (byteString bs')) + bs_padding) with (bs_padding + 8 * length bs_byteString + (padding bs' + 8 * length (byteString bs'))) by omega. rewrite <- IHbs_byteString; clear. rewrite !length_ByteString_push_word. rewrite length_ByteString_push_char, plus_comm, plus_assoc. rewrite <- !plus_assoc; f_equal. remember (fold_right ByteString_push_char bs' bs_byteString); clear. induction bs_padding. + unfold length_ByteString; simpl; omega. + rewrite <- plus_n_Sm, (IHbs_padding (wtl bs_front)); clear. rewrite plus_n_Sm. simpl ByteString_push_word. unfold ByteString_push. repeat match goal with | _ => progress simpl in * | _ => progress subst | _ => progress unfold eq_rec_r, eq_rec, eq_rect, eq_sym | _ => progress destruct_matches | [ H : context[padding ?x] |- _ ] => destruct x eqn:? | _ => omega end. 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