proposition: Lemma length_ByteString_unused_word {S} : forall (s : S) (sz : nat) (b : ByteString) (ctx ctx' : CacheFormat), format_unused_word sz s ctx ↝ (b, ctx') -> length_ByteString b = sz.
proof: Proof. unfold format_unused_word, Compose_Format; intros; rewrite unfold_computes in H; destruct_ex; split_and. unfold format_word in H0; computes_to_inv; injections. rewrite length_encode_word'; simpl. unfold ByteString_id, length_ByteString; simpl; 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