proposition: Lemma Nat2pointerT_pointerT2Nat : forall p, Nat2pointerT (pointerT2Nat p) = p.
proof: Proof. destruct p as [[upper_p upper_p_OK] lower_p]. unfold pointerT2Nat; simpl. unfold Nat2pointerT; f_equal. assert ((natToWord 8 (NPeano.modulo (NPeano.div ((wordToNat upper_p - 192) * 256 + wordToNat lower_p) 256) 64 + 192)) = upper_p). - rewrite NPeano.Nat.div_add_l; auto with arith. rewrite NPeano.Nat.div_small, NPeano.Nat.add_0_r. rewrite NPeano.Nat.mod_eq by omega. replace (64 * NPeano.div (wordToNat upper_p - 192) 64) with 0. rewrite <- Minus.minus_n_O, NPeano.Nat.sub_add. apply natToWord_wordToNat. apply WordFacts.wordToNat_lt in upper_p_OK; eauto. rewrite div_eq by omega. apply WordFacts.wordToNat_lt in upper_p_OK; simpl in upper_p_OK. revert upper_p_OK; clear. shatter_word upper_p. abstract (destruct x; destruct x0; destruct x1; destruct x2; destruct x3; destruct x4; destruct x5; destruct x6; simpl; intro; try omega). apply wordToNat_bound. - generalize (Nat2pointerT_pf ((wordToNat upper_p - 192) * 256 + wordToNat lower_p)); rewrite H; intros. f_equal. apply UIP_dec. decide equality. - rewrite Plus.plus_comm, NPeano.Nat.mod_add by omega. rewrite NPeano.Nat.mod_eq by omega. rewrite NPeano.Nat.div_small by apply wordToNat_bound. simpl mult; rewrite <- Minus.minus_n_O. apply natToWord_wordToNat. 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