proposition: Lemma pointerT2Nat_Nat2pointerT : forall n, (n < pow2 14)%nat -> pointerT2Nat (Nat2pointerT n) = n.
proof: Proof. intros. unfold Nat2pointerT. unfold pointerT2Nat, fst, snd, proj1_sig. rewrite (NPeano.Nat.div_mod n 256) at 3 by omega. rewrite Mult.mult_comm. f_equal. - f_equal. rewrite wordToNat_natToWord_idempotent. rewrite NPeano.Nat.add_sub. rewrite NPeano.Nat.mod_eq by omega. replace (NPeano.div (NPeano.div n 256) 64) with 0. omega. rewrite NPeano.Nat.div_div by omega. replace (256 * 64) with (pow2 14) by reflexivity. symmetry; apply NPeano.Nat.div_small; auto. replace (Npow2 8) with (BinNat.N.of_nat 256) by reflexivity. eapply Nomega.Nlt_in. rewrite !Nnat.Nat2N.id. assert (64 <> 0) by omega. pose proof (NPeano.Nat.mod_upper_bound (NPeano.div n 256) _ H0). omega. - rewrite wordToNat_natToWord_idempotent; auto. replace (Npow2 8) with (BinNat.N.of_nat 256) by reflexivity. eapply Nomega.Nlt_in. rewrite !Nnat.Nat2N.id. apply NPeano.Nat.mod_upper_bound; omega. 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