proposition: Lemma decode_string_add_ptr_OK : forall n env xenv n' xenv'' b b' l l', add_ptr_OK (l', n') env xenv -> decode_string n b xenv = Some (l, b', xenv'') -> add_ptr_OK (l', n') env xenv''.
proof: Proof. unfold add_ptr_OK in *; induction n; simpl; intros. - injections; eauto. rewrite IndependentCaches; eauto. - apply DecodeBindOpt2_inv in H0; destruct H0 as [? [? [? [? ?] ] ] ]; injections; subst. destruct (decode_string n x0 x1) eqn: ?; simpl in *; try discriminate. destruct p; destruct p; injections. eapply IHn in Heqo; eauto. unfold decode_ascii in H0. apply DecodeBindOpt2_inv in H0; destruct H0 as [? [? [? [? ?] ] ] ]; injections; subst. unfold decode_word in H0. destruct (decode_word' 8 b); simpl in *; try discriminate; injections. 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