proposition: Lemma length_ByteString_bytebuffer : forall (ctx : CacheFormat) (b : ByteString) (ctx' : CacheFormat) (bb : { n : nat & ByteBuffer.t n}), format_bytebuffer bb ctx ∋ (b, ctx') -> length_ByteString b = 8 * projT1 bb.
proof: Proof. intros. destruct bb; simpl in *. unfold format_bytebuffer in H. revert ctx b ctx' H; induction t; intros. - simpl in *; computes_to_inv; subst; injections. reflexivity. - simpl in *; unfold Bind2 in *; computes_to_inv; subst; injections; destruct v; simpl in *. destruct v0. rewrite length_ByteString_enqueue_ByteString. apply IHt in H'. simpl; rewrite H'. apply length_ByteString_word in H; subst; omega. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.ZArith.ZArith Fiat.Narcissus.BinLib Fiat.Narcissus.Common.Specs Fiat.Narcissus.Common.ComposeOpt Fiat.Narcissus.Common.ComposeCheckSum Fiat.Narcissus.Common.ComposeIf Fiat.Narcissus.Formats Fiat.Narcissus.BaseFormats Fiat.Narcissus.Automation.Solver Fiat.Narcissus.Automation.NormalizeFormats Bedrock.Word