Cleanup: mostly moving lemmas to Util files, some moving lemmas to more general contexts.

1 files changed, 25 insertions, 0 deletions

diff --git a/src/Util/WordUtil.v b/src/Util/WordUtil.v
index 17d04c60a..d655d046d 100644
--- a/src/Util/WordUtil.v
+++ b/src/Util/WordUtil.v
@@ -1,5 +1,6 @@
 Require Import Coq.Numbers.Natural.Peano.NPeano.
 Require Import Coq.ZArith.ZArith.
+Require Import Crypto.Util.NatUtil.
 Require Import Bedrock.Word.
 
 Local Open Scope nat_scope.
@@ -21,6 +22,30 @@ Proof.
   auto.
 Qed.
 
+Lemma wordToN_NToWord_idempotent : forall sz n, (n < Npow2 sz)%N ->
+  wordToN (NToWord sz n) = n.
+Proof.
+  intros.
+  rewrite wordToN_nat, NToWord_nat.
+  rewrite wordToNat_natToWord_idempotent; rewrite Nnat.N2Nat.id; auto.
+Qed.
+
+Lemma NToWord_wordToN : forall sz w, NToWord sz (wordToN w) = w.
+Proof.
+  intros.
+  rewrite wordToN_nat, NToWord_nat, Nnat.Nat2N.id.
+  apply natToWord_wordToNat.
+Qed.
+
+Lemma bound_check_nat_N : forall x n, (Z.to_nat x < 2 ^ n)%nat -> (Z.to_N x < Npow2 n)%N.
+Proof.
+  intros x n bound_nat.
+  rewrite <- Nnat.N2Nat.id, Npow2_nat.
+  replace (Z.to_N x) with (N.of_nat (Z.to_nat x)) by apply Z_nat_N.
+  apply (Nat2N_inj_lt _ (pow2 n)).
+  rewrite pow2_id; assumption.
+Qed.
+
 Definition wfirstn n {m} (w : Word.word m) {H : n <= m} : Word.word n.
   refine (Word.split1 n (m - n) (match _ in _ = N return Word.word N with
                             | eq_refl => w