proposition: Lemma format_string_add_ptr_OK : forall s env b' env' p z, ~ In p (getE env z) -> computes_to (format_string s env) (b', env') -> ~ In p (getE env' z).
proof: Proof. induction s; simpl; unfold format_ascii, format_word; intros; computes_to_inv; injections; try rewrite IndependentCaches'; eauto. unfold Bind2 in *; computes_to_inv; injections; simpl in *; eauto. destruct v0; simpl in *; eauto. eapply IHs in H0'. eassumption. unfold not; rewrite IndependentCaches'; eauto. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Bedrock.Word Coq.ZArith.ZArith Coq.Strings.Ascii Coq.Strings.String Coq.Logic.Eqdep_dec Fiat.Computation.Core Fiat.Computation.FixComp Fiat.Computation.Notations Fiat.Computation.Refinements.General Fiat.Common.DecideableEnsembles Fiat.Narcissus.Common.Specs Fiat.Narcissus.Formats.FixStringOpt Fiat.Narcissus.Formats.NatOpt Fiat.Narcissus.Formats.WordOpt Fiat.Narcissus.Formats.AsciiOpt