proposition: Lemma boundPeekSome : forall env n m m', peekD env = Some m -> peekD (addD env (n * 8)) = Some m' -> lt (n + (pointerT2Nat m)) (pow2 14).
proof: Proof. simpl; intros; subst. destruct (fst env); simpl in *; try discriminate. injections. find_if_inside; unfold If_Opt_Then_Else in *; try congruence. injections. rewrite !wtl_div in *. rewrite pointerT2Nat_Nat2pointerT in *; try (eapply pow2_div; eassumption). eapply (mult_lt_compat_l' _ _ 8); try omega. - rewrite mult_plus_distr_l. assert (8 <> 0) by omega. pose proof (NPeano.Nat.mul_div_le (wordToNat w) 8 H). apply le_lt_trans with (8 * n + (wordToNat w)). omega. rewrite mult_pow2_8. simpl plus at -1. omega. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.ZArith.ZArith Coq.Lists.List Coq.Strings.String Coq.Arith.Mult Fiat.Common Fiat.Common.DecideableEnsembles Fiat.Narcissus.Common.Specs Fiat.Narcissus.Stores.Cache Fiat.Narcissus.Formats.DomainNameOpt Bedrock.Word