proposition: Lemma decode_word_add_ptr_OK : forall sz env xenv n env' b b' x x1 l, add_ptr_OK (l, n) env xenv -> decode_word (sz := sz) b xenv = Some (x, b', x1) -> add_ptr_OK (l, n) env' x1.
proof: Proof. intros. unfold decode_word in H0. destruct (decode_word' sz b); simpl in *; try discriminate. injections. unfold add_ptr_OK. 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