Add ZToWord,wordToZ

1 files changed, 13 insertions, 0 deletions

diff --git a/src/Util/FixedWordSizes.v b/src/Util/FixedWordSizes.v
index b49e67c9a..df5d5240d 100644
--- a/src/Util/FixedWordSizes.v
+++ b/src/Util/FixedWordSizes.v
@@ -1,3 +1,4 @@
+Require Import Coq.ZArith.ZArith.
 Require Import Coq.NArith.BinNat.
 Require Import Coq.Arith.Arith.
 Require Import Bedrock.Word.
@@ -19,6 +20,8 @@ Definition word_case {T : nat -> Type} (logsz : nat)
      | logsz' => default _
      end.
 
+Definition ZToWord32 (v : Z) : word32 := NToWord _ (Z.to_N v).
+Definition word32ToZ (v : word32) : Z := Z.of_N (wordToN v).
 Definition wadd32 : word32 -> word32 -> word32 := @wplus _.
 Definition wsub32 : word32 -> word32 -> word32 := @wminus _.
 Definition wmul32 : word32 -> word32 -> word32 := @wmult _.
@@ -27,6 +30,8 @@ Definition wshr32 : word32 -> word32 -> word32 := @wordBin N.shiftr _.
 Definition wland32 : word32 -> word32 -> word32 := @wand _.
 Definition wlor32 : word32 -> word32 -> word32 := @wor _.
 
+Definition ZToWord64 (v : Z) : word64 := NToWord _ (Z.to_N v).
+Definition word64ToZ (v : word64) : Z := Z.of_N (wordToN v).
 Definition wadd64 : word64 -> word64 -> word64 := @wplus _.
 Definition wsub64 : word64 -> word64 -> word64 := @wminus _.
 Definition wmul64 : word64 -> word64 -> word64 := @wmult _.
@@ -35,6 +40,8 @@ Definition wshr64 : word64 -> word64 -> word64 := @wordBin N.shiftr _.
 Definition wland64 : word64 -> word64 -> word64 := @wand _.
 Definition wlor64 : word64 -> word64 -> word64 := @wor _.
 
+Definition ZToWord128 (v : Z) : word128 := NToWord _ (Z.to_N v).
+Definition word128ToZ (v : word128) : Z := Z.of_N (wordToN v).
 Definition wadd128 : word128 -> word128 -> word128 := @wplus _.
 Definition wsub128 : word128 -> word128 -> word128 := @wminus _.
 Definition wmul128 : word128 -> word128 -> word128 := @wmult _.
@@ -43,6 +50,12 @@ Definition wshr128 : word128 -> word128 -> word128 := @wordBin N.shiftr _.
 Definition wland128 : word128 -> word128 -> word128 := @wand _.
 Definition wlor128 : word128 -> word128 -> word128 := @wor _.
 
+Definition ZToWord {logsz}
+  := word_case (T:=fun sz => Z -> word sz)
+               logsz ZToWord32 ZToWord64 ZToWord128 (fun _ v => NToWord _ (Z.to_N v)).
+Definition wordToZ {logsz}
+  := word_case (T:=fun sz => word sz -> Z)
+               logsz word32ToZ word64ToZ word128ToZ (fun _ v => Z.of_N (wordToN v)).
 Definition wadd {logsz}
   := word_case (T:=fun sz => word sz -> word sz -> word sz)
                logsz wadd32 wadd64 wadd128 (fun _ => @wplus _).