Add wordToZ_ZToWord_mod

2 files changed, 33 insertions, 0 deletions

diff --git a/src/Util/FixedWordSizesEquality.v b/src/Util/FixedWordSizesEquality.v
index c8f37c86b..2371eda1a 100644
--- a/src/Util/FixedWordSizesEquality.v
+++ b/src/Util/FixedWordSizesEquality.v
@@ -120,6 +120,16 @@ Proof.
   assumption.
 Qed.
 
+Lemma wordToZ_gen_ZToWord_gen_mod : forall {sz} w, (0 <= w)%Z -> wordToZ_gen (@ZToWord_gen sz w) = (w mod (2^Z.of_nat sz))%Z.
+Proof.
+  unfold ZToWord_gen, wordToZ_gen.
+  intros.
+  rewrite wordToN_NToWord_mod.
+  rewrite N2Z.inj_mod by (destruct sz; simpl; congruence).
+  rewrite Z2N.id, N2Z.inj_pow, nat_N_Z by assumption.
+  reflexivity.
+Qed.
+
 Lemma ZToWord_gen_wordToZ_gen_ZToWord_gen : forall {sz1 sz2} v,
     (sz2 <= sz1)%nat -> @ZToWord_gen sz2 (wordToZ_gen (@ZToWord_gen sz1 v)) = ZToWord_gen v.
 Proof.
@@ -162,6 +172,13 @@ Proof.
     assumption.
 Qed.
 
+Lemma wordToZ_ZToWord_mod : forall {sz} v, (0 <= v)%Z -> wordToZ (@ZToWord sz v) = (v mod (2^Z.of_nat (2^sz)))%Z.
+Proof.
+  unfold wordToZ, ZToWord, word_case_dep.
+  intros; break_match; apply wordToZ_gen_ZToWord_gen_mod;
+    assumption.
+Qed.
+
 Local Ltac handle_le :=
   repeat match goal with
          | [ |- (S ?a <= 2^?b)%nat ]
diff --git a/src/Util/WordUtil.v b/src/Util/WordUtil.v
index fc1ac28a6..839defb03 100644
--- a/src/Util/WordUtil.v
+++ b/src/Util/WordUtil.v
@@ -464,6 +464,22 @@ Section WordToN.
     reflexivity.
   Qed.
 
+  Lemma wordToN_NToWord_mod : forall sz w, wordToN (NToWord sz w) = N.modulo w (2^N.of_nat sz).
+  Proof.
+    intros.
+    apply N.bits_inj; intro k.
+    repeat match goal with
+           | _ => reflexivity
+           | _ => progress rewrite ?wordToN_testbit, ?wbit_NToWord, ?N2Nat.id
+           | _ => rewrite N.mod_pow2_bits_low by lia
+           | _ => rewrite N.mod_pow2_bits_high by lia
+           | _ => progress break_match
+           | [ H : (_ <? _) = true |- _ ] => apply Nat.ltb_lt in H
+           | [ H : (_ <? _) = false |- _ ] => apply Nat.ltb_ge in H
+           | _ => omega
+           end.
+  Qed.
+
   Lemma wordToN_split1: forall {n m} x,
     wordToN (@split1 n m x) = N.land (wordToN x) (wordToN (wones n)).
   Proof.