proposition: Lemma addPeekSome : forall env n m, peekD env = Some m -> lt (n + (pointerT2Nat m)) (pow2 14) -> exists p', peekD (addD env (n * 8)) = Some p' /\ pointerT2Nat p' = n + (pointerT2Nat m).
proof: Proof. simpl; intros; subst. destruct (fst env); simpl in *; try discriminate. injections. find_if_inside. - rewrite !wtl_div in *. rewrite pointerT2Nat_Nat2pointerT in *; try (eapply pow2_div; eassumption). unfold If_Opt_Then_Else. eexists; split; try reflexivity. rewrite wtl_div. rewrite wordToNat_natToWord_idempotent. rewrite pointerT2Nat_Nat2pointerT in *; try omega. rewrite NPeano.Nat.div_add; try omega. rewrite NPeano.Nat.div_add; try omega. apply Nomega.Nlt_in. rewrite Nnat.Nat2N.id, Npow2_nat; auto. - exfalso; apply n0. rewrite !wtl_div in *. rewrite pointerT2Nat_Nat2pointerT in *. rewrite (NPeano.div_mod (wordToNat w) 8); try omega. pose proof (mult_pow2_8 14) as H'; simpl plus in H'; rewrite <- H'. replace (8 * NPeano.div (wordToNat w) 8 + NPeano.modulo (wordToNat w) 8 + n * 8) with (8 * (NPeano.div (wordToNat w) 8 + n) + NPeano.modulo (wordToNat w) 8) by omega. eapply mult_lt_compat_l''; try omega. apply NPeano.Nat.mod_upper_bound; omega. eapply (mult_lt_compat_l' _ _ 8); try omega. eapply le_lt_trans. apply NPeano.Nat.mul_div_le; omega. rewrite mult_pow2_8; simpl. apply wordToNat_bound. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.Strings.String Coq.Arith.Mult Coq.Vectors.Vector Fiat.Common.SumType Fiat.Common.BoundedLookup Fiat.Common.ilist Fiat.Common.DecideableEnsembles Fiat.Common.IterateBoundedIndex Fiat.Common.Tactics.CacheStringConstant Fiat.Computation Fiat.QueryStructure.Specification.Representation.Notations Fiat.QueryStructure.Specification.Representation.Heading Fiat.QueryStructure.Specification.Representation.Tuple Fiat.Narcissus.BinLib.Core Fiat.Narcissus.Common.Specs Fiat.Narcissus.Common.ComposeOpt Fiat.Narcissus.Automation.Solver Fiat.Narcissus.Formats.WordOpt Fiat.Narcissus.Formats.NatOpt Fiat.Narcissus.Formats.StringOpt Fiat.Narcissus.Formats.EnumOpt Fiat.Narcissus.Formats.FixListOpt Fiat.Narcissus.Formats.SumTypeOpt Fiat.Narcissus.Formats.DomainNameOpt Fiat.Narcissus.Examples.DNS.DNSPacket Bedrock.Word