blob: b49e67c9a9c3f65dcd0f4afe8bcf83cbe26b971a (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
|
Require Import Coq.NArith.BinNat.
Require Import Coq.Arith.Arith.
Require Import Bedrock.Word.
Definition word32 := word 32. (* 2^5 *)
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
| 5 => case32
| 6 => case64
| 7 => case128
| logsz' => default _
end.
Definition wadd32 : word32 -> word32 -> word32 := @wplus _.
Definition wsub32 : word32 -> word32 -> word32 := @wminus _.
Definition wmul32 : word32 -> word32 -> word32 := @wmult _.
Definition wshl32 : word32 -> word32 -> word32 := @wordBin N.shiftl _.
Definition wshr32 : word32 -> word32 -> word32 := @wordBin N.shiftr _.
Definition wland32 : word32 -> word32 -> word32 := @wand _.
Definition wlor32 : word32 -> word32 -> word32 := @wor _.
Definition wadd64 : word64 -> word64 -> word64 := @wplus _.
Definition wsub64 : word64 -> word64 -> word64 := @wminus _.
Definition wmul64 : word64 -> word64 -> word64 := @wmult _.
Definition wshl64 : word64 -> word64 -> word64 := @wordBin N.shiftl _.
Definition wshr64 : word64 -> word64 -> word64 := @wordBin N.shiftr _.
Definition wland64 : word64 -> word64 -> word64 := @wand _.
Definition wlor64 : word64 -> word64 -> word64 := @wor _.
Definition wadd128 : word128 -> word128 -> word128 := @wplus _.
Definition wsub128 : word128 -> word128 -> word128 := @wminus _.
Definition wmul128 : word128 -> word128 -> word128 := @wmult _.
Definition wshl128 : word128 -> word128 -> word128 := @wordBin N.shiftl _.
Definition wshr128 : word128 -> word128 -> word128 := @wordBin N.shiftr _.
Definition wland128 : word128 -> word128 -> word128 := @wand _.
Definition wlor128 : word128 -> word128 -> word128 := @wor _.
Definition wadd {logsz}
:= word_case (T:=fun sz => word sz -> word sz -> word sz)
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 _).
Definition wmul {logsz}
:= word_case (T:=fun sz => word sz -> word sz -> word sz)
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 _).
Definition wshr {logsz}
:= word_case (T:=fun sz => word sz -> word sz -> word sz)
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 _).
Definition wlor {logsz}
:= word_case (T:=fun sz => word sz -> word sz -> word sz)
logsz wlor32 wlor64 wlor128 (fun _ => @wor _).
|
