-
Notifications
You must be signed in to change notification settings - Fork 7
/
operations.v
211 lines (165 loc) · 8.45 KB
/
operations.v
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
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
(*===========================================================================
Arithmetic and logical operations on n-bit words
For proofs of properties of operations see bitsopsprops.v
===========================================================================*)
Require Import mathcomp.ssreflect.ssreflect.
From mathcomp Require Import ssrfun ssrbool eqtype ssrnat seq tuple.
Require Import spec.
Set Implicit Arguments.
Unset Strict Implicit.
Import Prenex Implicits.
(*---------------------------------------------------------------------------
Increment and decrement operations
---------------------------------------------------------------------------*)
Notation eta_expand x := (fst x, snd x).
Fixpoint incB {n} : BITS n -> BITS n :=
if n is n.+1
then fun p => let (p,b) := eta_expand (splitlsb p) in
if b then joinlsb (incB p, false) else joinlsb (p, true)
else fun _ => nilB.
Fixpoint decB {n} : BITS n -> BITS n :=
if n is _.+1
then fun p => let (p,b) := eta_expand (splitlsb p) in
if b then joinlsb (p, false) else joinlsb (decB p, true)
else fun _ => nilB.
(*---------------------------------------------------------------------------
Bitwise logical operations
---------------------------------------------------------------------------*)
(* Lift a unary operation on booleans to one on n-bit values *)
Definition liftUnOp {n} op (p: BITS n): BITS n := map_tuple op p.
(* Lift a binary operation on booleans to one on n-bit values *)
Definition liftBinOp {n} op (p1 p2: BITS n) : BITS n :=
map_tuple (fun pair => op pair.1 pair.2) (zip_tuple p1 p2).
Definition invB {n} := liftUnOp (n:=n) negb.
Definition andB {n} := liftBinOp (n:=n) andb.
Definition orB {n} := liftBinOp (n:=n) orb.
Definition xorB {n} := liftBinOp (n:=n) xorb.
(* Negation (two's complement) *)
Definition negB {n} (p: BITS n) := incB (invB p).
(*---------------------------------------------------------------------------
Addition
---------------------------------------------------------------------------*)
Definition fullAdder carry b1 b2 : bool * bool :=
match carry, b1, b2 with
| false, false, false => (false, false)
| true, false, false | false, true, false | false, false, true => (false, true)
| true, true, false | false, true, true | true, false, true => (true, false)
| true, true, true => (true, true)
end.
(* Add with carry, producing a word one bit larger than the inputs *)
Fixpoint adcBmain n carry : BITS n -> BITS n -> BITS n.+1 :=
if n is _.+1 then
fun p1 p2 => let (p1,b1) := eta_expand (splitlsb p1) in let (p2,b2) := eta_expand (splitlsb p2) in
let (carry',b) := fullAdder carry b1 b2 in
joinlsb (adcBmain carry' p1 p2, b)
else fun _ _ => singleBit carry.
Definition adcB {n} carry (p1 p2: BITS n) := splitmsb (adcBmain carry p1 p2).
(* Add with carry=0 and ignore carry out *)
Notation carry_addB p1 p2 := (adcB false p1 p2).1.
Notation addB p1 p2 := (adcB false p1 p2).2.
(* Take a page from ssreflect's book of ssrfun *)
Notation "@ 'addB' n" := (fun p1 p2 : BITS n => addB p1 p2)
(at level 10, n at level 8, only parsing) : function_scope.
(*(** Don't simpl unless everything is a constructor. *)
Global Arguments adcB {!n} !carry !p1 !p2 / .*)
(** Don't ever simpl adcB *)
Global Opaque adcB.
(* Add with carry=0 and return None on overflow *)
Definition addBovf n (p1 p2: BITS n) :=
if carry_addB p1 p2 then None else Some (addB p1 p2).
Definition computeOverflow n (arg1 arg2 res: BITS n) :=
match (msb arg1,msb arg2,msb res) with
| (true,true,false) | (false,false,true) => true | _ => false
end.
(* Some handy notation *)
Notation "b +# n" := (addB b #n) (at level 50, left associativity).
(*---------------------------------------------------------------------------
Subtraction
---------------------------------------------------------------------------*)
Definition sbbB {n} borrow (arg1 arg2: BITS n) :=
let (carry, res) := eta_expand (adcB (~~borrow) arg1 (invB arg2)) in
(~~carry, res).
Notation carry_subB p1 p2 := (sbbB false p1 p2).1.
Notation subB p1 p2 := (sbbB false p1 p2).2.
Notation "@ 'subB' n" := (fun p1 p2 : BITS n => subB p1 p2)
(at level 10, n at level 8, only parsing) : function_scope.
(** Don't ever simpl [sbbB]. *)
(*Global Arguments sbbB {!n} !borrow !arg1 !arg2 / .*)
Global Opaque sbbB.
Notation "b -# n" := (subB b #n) (at level 50, left associativity).
(*---------------------------------------------------------------------------
Unsigned comparison
---------------------------------------------------------------------------*)
Fixpoint ltB {n} : BITS n -> BITS n -> bool :=
if n is n.+1
then fun p1 p2 => let (q1,b1) := eta_expand (splitlsb p1) in
let (q2,b2) := eta_expand (splitlsb p2) in
(ltB q1 q2 || ((q1 == q2) && (~~b1) && b2))
else fun p1 p2 => false.
Definition leB {n} (p1 p2: BITS n) := ltB p1 p2 || (p1 == p2).
(*---------------------------------------------------------------------------
Multiplication
---------------------------------------------------------------------------*)
Fixpoint fullmulB n1 n2 : BITS n1 -> BITS n2 -> BITS (n1+n2) :=
if n1 is n.+1 return BITS n1 -> BITS n2 -> BITS (n1+n2)
then (fun p1 p2 => let (p,b) := eta_expand (splitlsb p1) in
if b then addB (joinlsb (fullmulB p p2, false)) (zeroExtendAux n.+1 p2)
else joinlsb (fullmulB p p2, false))
else (fun p1 p2 => #0).
Definition mulB {n} (p1 p2: BITS n) :=
low n (fullmulB p1 p2).
Notation "b *# n" := (mulB b #n) (at level 40, left associativity).
(*---------------------------------------------------------------------------
Shift and rotation operations
---------------------------------------------------------------------------*)
(* Rotate right: lsb goes into msb, everything else gets shifted right *)
Definition rorB {n} (p: BITS n.+1) : BITS n.+1 := let (p, b) := eta_expand (splitlsb p) in joinmsb (b, p).
(* Rotate left: msb goes into lsb, everything else gets shifted left *)
Definition rolB {n} (p: BITS n.+1) := let (b, p) := eta_expand (splitmsb p) in joinlsb (p, b).
(* Shift right: shift everything right and put 0 in msb *)
Definition shrB {n} : BITS n -> BITS n :=
if n is n.+1 then fun p => joinmsb0 (droplsb (n:=n) p) else fun p => nilB.
Definition shrBn {n} (p: BITS n)(k: nat): BITS n := iter k shrB p.
(* Arithmetic shift right: shift one bit to the right, copy msb *)
Definition sarB {n} (p: BITS n.+1) := joinmsb (msb p, droplsb p).
(* Lossless shift left: shift one bit to the left, put 0 in lsb *)
Definition shlBaux {n} (p: BITS n) : BITS n.+1 := joinlsb (p, false).
(* Shift left: shift one bit to the left, put 0 in lsb, lose msb *)
Definition shlB {n} (p: BITS n) := dropmsb (shlBaux p).
Definition shlBn {n} (p: BITS n)(k: nat): BITS n := iter k shlB p.
(*---------------------------------------------------------------------------
Iteration and ranges
---------------------------------------------------------------------------*)
(* Iteration *)
Fixpoint bIter {n A} : BITS n -> (A -> A) -> A -> A :=
if n is m.+1
then fun p f x => if p == zero _ then x
else let (p,b) := eta_expand (splitlsb p) in
if b then let r := bIter p f (f x) in bIter p f r
else let r := bIter p f x in bIter p f r
else fun p f x => x.
Definition bIterFrom {n A} (p c: BITS n) (f: BITS n -> A -> A) x :=
let (p',r) := bIter c (fun pair : BITS n * A => let (p,r) := pair in (incB p, f p r)) (p,x)
in r.
(* Ranges *)
Definition bIota {n} (p m: BITS n) : seq (BITS n) := rev (bIterFrom p m cons nil).
Definition bRange {n} (p q: BITS n) := bIota p (subB q p).
(*---------------------------------------------------------------------------
Notations
---------------------------------------------------------------------------*)
Declare Scope bits_scope.
Module BitsNotations.
Infix "<<" := shlBn (at level 30, no associativity) : bits_scope.
Infix ">>" := shrBn (at level 30, no associativity) : bits_scope.
Infix "|" := orB (at level 40, left associativity) : bits_scope.
Infix "&" := andB (at level 40, left associativity) : bits_scope.
(*Infix "^" := xorB (at level 40, left associativity) : bits_scope.*)
Notation "n + m" := (addB n m) : bits_scope.
Notation "m .+1" := (incB m) : bits_scope.
Notation "m .-1" := (decB m) : bits_scope.
Notation "- m" := (negB m) : bits_scope.
Notation "~ m" := (invB m) : bits_scope.
End BitsNotations.
Open Scope bits_scope.
Delimit Scope bits_scope with bits.
Bind Scope bits_scope with BITS.