proposition: Lemma addPeek : forall env n m, peekD env = Some m -> (peekD (addD env (n * 8)) = Some (Nat2pointerT (n + (pointerT2Nat m))) /\ n + (pointerT2Nat m) < pow2 14)%nat \/ peekD (addD env (n * 8)) = None.
proof: Proof. intros; destruct (Compare_dec.lt_dec (n + pointerT2Nat m) (pow2 14)). - left; pose proof (addPeekSome _ n _ H) as H'; eauto. destruct H' as [p' [H' H''] ]; eauto. split. * rewrite H', <- H''. f_equal. rewrite Nat2pointerT_pointerT2Nat; reflexivity. * eapply boundPeekSome; eauto. - right; eapply addPeekNone' in H; 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