Add ZToWord_wordToZ_ZToWord_small

2 files changed, 45 insertions, 0 deletions

diff --git a/src/Util/FixedWordSizesEquality.v b/src/Util/FixedWordSizesEquality.v
index e1a8f1f79..c8f37c86b 100644
--- a/src/Util/FixedWordSizesEquality.v
+++ b/src/Util/FixedWordSizesEquality.v
@@ -129,6 +129,18 @@ Proof.
   reflexivity.
 Qed.
 
+Lemma ZToWord_gen_wordToZ_gen_ZToWord_gen_small : forall {sz1 sz2} v,
+    (wordToZ_gen (@ZToWord_gen sz2 v) < 2^(Z.of_nat sz1))%Z
+    -> @ZToWord_gen sz2 (wordToZ_gen (@ZToWord_gen sz1 v)) = ZToWord_gen v.
+Proof.
+  unfold ZToWord_gen, wordToZ_gen.
+  intros sz1 sz2 v H.
+  change 2%Z with (Z.of_nat 2) in H.
+  rewrite <- !nat_N_Z, <- N2Z.inj_pow, <- N2Z.inj_lt in H.
+  rewrite N2Z.id, NToWord_wordToN_NToWord_small by assumption.
+  reflexivity.
+Qed.
+
 Lemma wordToZ_gen_ZToWord_gen_wordToZ_gen sz1 sz2 w
   : (sz1 <= sz2)%nat -> wordToZ_gen (@ZToWord_gen sz2 (@wordToZ_gen sz1 w)) = wordToZ_gen w.
 Proof.
@@ -171,6 +183,14 @@ Proof.
     handle_le.
 Qed.
 
+Lemma ZToWord_wordToZ_ZToWord_small : forall {sz1 sz2} v,
+    (wordToZ (@ZToWord sz2 v) < 2^Z.of_nat (2^sz1))%Z -> @ZToWord sz2 (wordToZ (@ZToWord sz1 v)) = ZToWord v.
+Proof.
+  unfold wordToZ, ZToWord, word_case_dep.
+  intros sz1 sz2; break_match; intros; apply ZToWord_gen_wordToZ_gen_ZToWord_gen_small;
+    handle_le; try omega.
+Qed.
+
 Lemma wordToZ_ZToWord_wordToZ : forall sz1 sz2 w, (sz1 <= sz2)%nat -> wordToZ (@ZToWord sz2 (@wordToZ sz1 w)) = wordToZ w.
 Proof.
   unfold wordToZ, ZToWord, word_case_dep.
diff --git a/src/Util/WordUtil.v b/src/Util/WordUtil.v
index 4833f0df6..fc1ac28a6 100644
--- a/src/Util/WordUtil.v
+++ b/src/Util/WordUtil.v
@@ -414,6 +414,31 @@ Section WordToN.
             reflexivity. } }
   Qed.
 
+  Lemma NToWord_wordToN_NToWord_small : forall sz1 sz2 w,
+      (wordToN (NToWord sz2 w) < 2^N.of_nat sz1)%N
+      -> NToWord sz2 (wordToN (NToWord sz1 w)) = NToWord sz2 w.
+  Proof.
+    intros sz1 sz2 w H.
+    apply wbit_inj_iff_lt; intros k Hlt.
+    rewrite !wbit_NToWord, wordToN_testbit, wbit_NToWord, Nat2N.id.
+    destruct (N.eq_dec (wordToN (NToWord sz2 w)) 0) as [H'|H'];
+      [ apply N.bits_inj_iff in H'; specialize (H' (N.of_nat k));
+        rewrite wordToN_testbit, wbit_NToWord, N2Nat.id, Nat2N.id in H'; simpl in *
+      | assert (H'' : sz1 <= k -> N.testbit (wordToN (NToWord sz2 w)) (N.of_nat k) = false);
+        [ intro;
+          apply N.log2_lt_pow2 in H; [ | lia.. ]
+        | rewrite wordToN_testbit, wbit_NToWord, N2Nat.id, Nat2N.id in H'' ] ];
+    break_match; try reflexivity;
+      repeat match goal with
+             | [ H : (_ <? _) = true |- _ ] => apply Nat.ltb_lt in H
+             | [ H : (_ <? _) = false |- _ ] => apply Nat.ltb_ge in H
+             | _ => omega
+             | _ => congruence
+             | _ => rewrite N.bits_above_log2 by lia
+             | _ => solve [ symmetry; auto ]
+             end.
+  Qed.
+
   Lemma NToWord_wordToN_NToWord : forall sz1 sz2 w,
       sz2 <= sz1 -> NToWord sz2 (wordToN (NToWord sz1 w)) = NToWord sz2 w.
   Proof.