From c07e8d7dd27750737d80c35d0eec124ae48196d9 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Tue, 3 Jan 2017 14:47:45 -0500 Subject: Better word operations --- .../ModularBaseSystemListZOperations.v | 24 +++---- src/Util/FixedWordSizes.v | 79 ++++++++++++++-------- 2 files changed, 61 insertions(+), 42 deletions(-) diff --git a/src/ModularArithmetic/ModularBaseSystemListZOperations.v b/src/ModularArithmetic/ModularBaseSystemListZOperations.v index 60d887df8..a91dddb1f 100644 --- a/src/ModularArithmetic/ModularBaseSystemListZOperations.v +++ b/src/ModularArithmetic/ModularBaseSystemListZOperations.v @@ -14,12 +14,12 @@ Definition cmovne (x y r1 r2 : Z) := if Z.eqb x y then r1 else r2. neg 0 = 0 *) Definition neg (int_width : Z) (b : Z) := if Z.eqb b 1 then Z.ones int_width else 0%Z. -Definition wcmovl_gen {logsz} x y r1 r2 - := @ZToWord logsz (cmovl (@wordToZ logsz x) (@wordToZ logsz y) (@wordToZ logsz r1) (@wordToZ logsz r2)). -Definition wcmovne_gen {logsz} x y r1 r2 - := @ZToWord logsz (cmovne (@wordToZ logsz x) (@wordToZ logsz y) (@wordToZ logsz r1) (@wordToZ logsz r2)). -Definition wneg_gen {logsz} (int_width : Z) b - := @ZToWord logsz (neg int_width (@wordToZ logsz b)). +Definition wcmovl_gen {sz} x y r1 r2 + := @ZToWord_gen sz (cmovl (@wordToZ_gen sz x) (@wordToZ_gen sz y) (@wordToZ_gen sz r1) (@wordToZ_gen sz r2)). +Definition wcmovne_gen {sz} x y r1 r2 + := @ZToWord_gen sz (cmovne (@wordToZ_gen sz x) (@wordToZ_gen sz y) (@wordToZ_gen sz r1) (@wordToZ_gen sz r2)). +Definition wneg_gen {sz} (int_width : Z) b + := @ZToWord_gen sz (neg int_width (@wordToZ_gen sz b)). Definition wcmovl32 x y r1 r2 := ZToWord32 (cmovl (word32ToZ x) (word32ToZ y) (word32ToZ r1) (word32ToZ r2)). Definition wcmovne32 x y r1 r2 := ZToWord32 (cmovne (word32ToZ x) (word32ToZ y) (word32ToZ r1) (word32ToZ r2)). @@ -34,11 +34,11 @@ Definition wcmovne128 x y r1 r2 := ZToWord128 (cmovne (word128ToZ x) (word128ToZ Definition wneg128 (int_width : Z) b := ZToWord128 (neg int_width (word128ToZ b)). Definition wcmovl {logsz} - := word_case (T:=fun sz => word sz -> word sz -> word sz -> word sz -> word sz) - logsz wcmovl32 wcmovl64 wcmovl128 (@wcmovl_gen). + := word_case_dep (T:=fun _ word => word -> word -> word -> word -> word) + logsz wcmovl32 wcmovl64 wcmovl128 (fun _ => @wcmovl_gen _). Definition wcmovne {logsz} - := word_case (T:=fun sz => word sz -> word sz -> word sz -> word sz -> word sz) - logsz wcmovne32 wcmovne64 wcmovne128 (@wcmovne_gen). + := word_case_dep (T:=fun _ word => word -> word -> word -> word -> word) + logsz wcmovne32 wcmovne64 wcmovne128 (fun _ => @wcmovne_gen _). Definition wneg {logsz} - := word_case (T:=fun sz => Z -> word sz -> word sz) - logsz wneg32 wneg64 wneg128 (@wneg_gen). + := word_case_dep (T:=fun _ word => Z -> word -> word) + logsz wneg32 wneg64 wneg128 (fun _ => @wneg_gen _). diff --git a/src/Util/FixedWordSizes.v b/src/Util/FixedWordSizes.v index df5d5240d..8e2484ff6 100644 --- a/src/Util/FixedWordSizes.v +++ b/src/Util/FixedWordSizes.v @@ -8,20 +8,39 @@ Definition word64 := word 64. (* 2^6 *) Definition word128 := word 128. (* 2^7 *) Definition word_case {T : nat -> Type} (logsz : nat) - (case32 : T 32) - (case64 : T 64) - (case128 : T 128) - (default : forall k, T (2^k)) - : T (2^logsz) - := match logsz return T (2^logsz) with + (case32 : T 5) + (case64 : T 6) + (case128 : T 7) + (default : forall k, T k) + : T logsz + := match logsz return T logsz with | 5 => case32 | 6 => case64 | 7 => case128 | logsz' => default _ end. -Definition ZToWord32 (v : Z) : word32 := NToWord _ (Z.to_N v). -Definition word32ToZ (v : word32) : Z := Z.of_N (wordToN v). +Definition wordT logsz := word_case (T:=fun _ => Set) logsz word32 word64 word128 (fun logsz => word (2^logsz)). + +Definition word_case_dep {T : nat -> Set -> Type} (logsz : nat) + (case32 : T 5 word32) + (case64 : T 6 word64) + (case128 : T 7 word128) + (default : forall k, T k (word (2^k))) + : T logsz (wordT logsz) + := match logsz return T logsz (wordT logsz) with + | 5 => case32 + | 6 => case64 + | 7 => case128 + | logsz' => default _ + end. + +Definition ZToWord_gen {sz} (v : Z) : word sz := NToWord _ (Z.to_N v). +Definition wordToZ_gen {sz} (v : word sz) : Z := Z.of_N (wordToN v). + + +Definition ZToWord32 : Z -> word32 := @ZToWord_gen _. +Definition word32ToZ : word32 -> Z := @wordToZ_gen _. Definition wadd32 : word32 -> word32 -> word32 := @wplus _. Definition wsub32 : word32 -> word32 -> word32 := @wminus _. Definition wmul32 : word32 -> word32 -> word32 := @wmult _. @@ -30,8 +49,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 ZToWord64 : Z -> word64 := @ZToWord_gen _. +Definition word64ToZ : word64 -> Z := @wordToZ_gen _. Definition wadd64 : word64 -> word64 -> word64 := @wplus _. Definition wsub64 : word64 -> word64 -> word64 := @wminus _. Definition wmul64 : word64 -> word64 -> word64 := @wmult _. @@ -40,8 +59,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 ZToWord128 : Z -> word128 := @ZToWord_gen _. +Definition word128ToZ : word128 -> Z := @wordToZ_gen _. Definition wadd128 : word128 -> word128 -> word128 := @wplus _. Definition wsub128 : word128 -> word128 -> word128 := @wminus _. Definition wmul128 : word128 -> word128 -> word128 := @wmult _. @@ -51,29 +70,29 @@ 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)). + := word_case_dep (T:=fun _ word => Z -> word) + logsz ZToWord32 ZToWord64 ZToWord128 (fun _ => @ZToWord_gen _). Definition wordToZ {logsz} - := word_case (T:=fun sz => word sz -> Z) - logsz word32ToZ word64ToZ word128ToZ (fun _ v => Z.of_N (wordToN v)). + := word_case_dep (T:=fun _ word => word -> Z) + logsz word32ToZ word64ToZ word128ToZ (fun _ => @wordToZ_gen _). Definition wadd {logsz} - := word_case (T:=fun sz => word sz -> word sz -> word sz) - logsz wadd32 wadd64 wadd128 (fun _ => @wplus _). + := word_case_dep (T:=fun _ word => word -> word -> word) + logsz wadd32 wadd64 wadd128 (fun _ => @wplus _). Definition wsub {logsz} - := word_case (T:=fun sz => word sz -> word sz -> word sz) - logsz wsub32 wsub64 wsub128 (fun _ => @wminus _). + := word_case_dep (T:=fun _ word => word -> word -> word) + logsz wsub32 wsub64 wsub128 (fun _ => @wminus _). Definition wmul {logsz} - := word_case (T:=fun sz => word sz -> word sz -> word sz) - logsz wmul32 wmul64 wmul128 (fun _ => @wmult _). + := word_case_dep (T:=fun _ word => word -> word -> word) + logsz wmul32 wmul64 wmul128 (fun _ => @wmult _). Definition wshl {logsz} - := word_case (T:=fun sz => word sz -> word sz -> word sz) - logsz wshl32 wshl64 wshl128 (fun _ => @wordBin N.shiftl _). + := word_case_dep (T:=fun _ word => word -> word -> word) + logsz wshl32 wshl64 wshl128 (fun _ => @wordBin N.shiftl _). Definition wshr {logsz} - := word_case (T:=fun sz => word sz -> word sz -> word sz) - logsz wshr32 wshr64 wshr128 (fun _ => @wordBin N.shiftr _). + := word_case_dep (T:=fun _ word => word -> word -> word) + logsz wshr32 wshr64 wshr128 (fun _ => @wordBin N.shiftr _). Definition wland {logsz} - := word_case (T:=fun sz => word sz -> word sz -> word sz) - logsz wland32 wland64 wland128 (fun _ => @wand _). + := word_case_dep (T:=fun _ word => word -> word -> word) + logsz wland32 wland64 wland128 (fun _ => @wand _). Definition wlor {logsz} - := word_case (T:=fun sz => word sz -> word sz -> word sz) - logsz wlor32 wlor64 wlor128 (fun _ => @wor _). + := word_case_dep (T:=fun _ word => word -> word -> word) + logsz wlor32 wlor64 wlor128 (fun _ => @wor _). -- cgit v1.2.3