proposition: Lemma format_string_peekE : forall l env b' env', computes_to (format_string l env) (b', env') -> peekE env' = peekE (addE env (String.length l * 8)).
proof: Proof. induction l; simpl; unfold format_ascii, format_word; intros; computes_to_inv; injections; eauto. unfold Bind2 in *; computes_to_inv; injections; simpl in *; eauto. destruct v0; simpl in *; eauto. eapply IHl in H'. rewrite H'. destruct (peekE env) eqn: ?. - destruct (addPeekE _ (1 + (String.length l)) _ Heqy) as [ [? ?] | ?]. destruct (addPeekESome _ 1 _ Heqy) as [? [? ?] ] ; try omega. destruct (addPeekESome _ (String.length l) _ H1) as [? [? ?] ] ; try omega. + simpl in *; rewrite H, H3. f_equal. apply (f_equal Nat2pointerT) in H4. rewrite Nat2pointerT_pointerT2Nat in H4. apply (f_equal Nat2pointerT) in H2. rewrite Nat2pointerT_pointerT2Nat in H2. subst. rewrite pointerT2Nat_Nat2pointerT; auto. omega. + destruct (addPeekE _ 1 _ Heqy) as [ [? ?] | ?]. * destruct (addPeekE _ (String.length l) _ H0) as [ [? ?] | ?]. destruct (addPeekESome _ (S (String.length l)) _ Heqy) as [? [? ?] ]. rewrite pointerT2Nat_Nat2pointerT in H2, H3; try omega. simpl in *; congruence. simpl in *; congruence. * eapply addPeekENone in H0; simpl in *; rewrite H, H0; auto. - rewrite !addPeekENone; auto. 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