@@ -1,25 +1,439 @@
11module Data.Bits
22
3−%access public
4−%default partial
3+%default total
54
6−infixl 5 .|.
7−infixl 7 .&.
5+divCeil : Nat -> Nat -> Nat
6+divCeil x y = case x `mod` y of
7+ O => x `div` y
8+ S _ => S (x `div` y)
89
9−class Num a => Bits a where
10− (.|.) : a -> a -> a
11− (.&.) : a -> a -> a
10+nextPow2 : Nat -> Nat
11+nextPow2 O = O
12+nextPow2 x = if x == (2 `power` l2x)
13+ then l2x
14+ else S l2x
15+ where
16+ l2x = log2 x
1217
13− xor : a -> a -> a
14− complement : a -> a
15− shiftL : a -> Int -> a
16− shiftR : a -> Int -> a
18+nextBytes : Nat -> Nat
19+nextBytes bits = (nextPow2 (bits `divCeil` 8))
1720
18−instance Bits Int where
19− (.|.) = prim__orInt
20− (.&.) = prim__andInt
21+machineTy : Nat -> Type
22+machineTy O = Bits8
23+machineTy (S O) = Bits16
24+machineTy (S (S O)) = Bits32
25+machineTy (S (S (S _))) = Bits64
2126
22− xor = prim__xorInt
23− complement = prim__complInt
24− shiftL = prim__shLInt
25− shiftR = prim__shRInt
27+bitsUsed : Nat -> Nat
28+bitsUsed n = 8 * (2 `power` n)
29+
30+%assert_total
31+natToBits' : machineTy n -> Nat -> machineTy n
32+natToBits' a O = a
33+natToBits' {n=n} a x with n
34+ natToBits' a (S x') | O = natToBits' (prim__addB8 a (prim__intToB8 1)) x'
35+ natToBits' a (S x') | S O = natToBits' (prim__addB16 a (prim__intToB16 1)) x'
36+ natToBits' a (S x') | S (S O) = natToBits' (prim__addB32 a (prim__intToB32 1)) x'
37+ natToBits' a (S x') | S (S (S _)) = natToBits' (prim__addB64 a (prim__intToB64 1)) x'
38+
39+natToBits : Nat -> machineTy n
40+natToBits {n=n} x with n
41+ | O = natToBits' (prim__intToB8 0) x
42+ | S O = natToBits' (prim__intToB16 0) x
43+ | S (S O) = natToBits' (prim__intToB32 0) x
44+ | S (S (S _)) = natToBits' (prim__intToB64 0) x
45+
46+getPad : Nat -> machineTy n
47+getPad n = natToBits ((bitsUsed (nextBytes n)) - n)
48+
49+public
50+data Bits : Nat -> Type where
51+ MkBits : machineTy (nextBytes n) -> Bits n
52+
53+pad8 : Nat -> (Bits8 -> Bits8 -> Bits8) -> Bits8 -> Bits8 -> Bits8
54+pad8 n f x y = prim__lshrB8 (f (prim__shlB8 x pad) (prim__shlB8 y pad)) pad
55+ where
56+ pad = getPad {n=0} n
57+
58+pad16 : Nat -> (Bits16 -> Bits16 -> Bits16) -> Bits16 -> Bits16 -> Bits16
59+pad16 n f x y = prim__lshrB16 (f (prim__shlB16 x pad) (prim__shlB16 y pad)) pad
60+ where
61+ pad = getPad {n=1} n
62+
63+pad32 : Nat -> (Bits32 -> Bits32 -> Bits32) -> Bits32 -> Bits32 -> Bits32
64+pad32 n f x y = prim__lshrB32 (f (prim__shlB32 x pad) (prim__shlB32 y pad)) pad
65+ where
66+ pad = getPad {n=2} n
67+
68+pad64 : Nat -> (Bits64 -> Bits64 -> Bits64) -> Bits64 -> Bits64 -> Bits64
69+pad64 n f x y = prim__lshrB64 (f (prim__shlB64 x pad) (prim__shlB64 y pad)) pad
70+ where
71+ pad = getPad {n=3} n
72+
73+-- These versions only pad the first operand
74+pad8' : Nat -> (Bits8 -> Bits8 -> Bits8) -> Bits8 -> Bits8 -> Bits8
75+pad8' n f x y = prim__lshrB8 (f (prim__shlB8 x pad) y) pad
76+ where
77+ pad = getPad {n=0} n
78+
79+pad16' : Nat -> (Bits16 -> Bits16 -> Bits16) -> Bits16 -> Bits16 -> Bits16
80+pad16' n f x y = prim__lshrB16 (f (prim__shlB16 x pad) y) pad
81+ where
82+ pad = getPad {n=1} n
83+
84+pad32' : Nat -> (Bits32 -> Bits32 -> Bits32) -> Bits32 -> Bits32 -> Bits32
85+pad32' n f x y = prim__lshrB32 (f (prim__shlB32 x pad) y) pad
86+ where
87+ pad = getPad {n=2} n
88+
89+pad64' : Nat -> (Bits64 -> Bits64 -> Bits64) -> Bits64 -> Bits64 -> Bits64
90+pad64' n f x y = prim__lshrB64 (f (prim__shlB64 x pad) y) pad
91+ where
92+ pad = getPad {n=3} n
93+
94+shiftLeft' : machineTy (nextBytes n) -> machineTy (nextBytes n) -> machineTy (nextBytes n)
95+shiftLeft' {n=n} x c with (nextBytes n)
96+ | O = pad8' n prim__shlB8 x c
97+ | S O = pad16' n prim__shlB16 x c
98+ | S (S O) = pad32' n prim__shlB32 x c
99+ | S (S (S _)) = pad64' n prim__shlB64 x c
100+
101+public
102+shiftLeft : Bits n -> Bits n -> Bits n
103+shiftLeft (MkBits x) (MkBits y) = MkBits (shiftLeft' x y)
104+
105+shiftRightLogical' : machineTy n -> machineTy n -> machineTy n
106+shiftRightLogical' {n=n} x c with n
107+ | O = prim__lshrB8 x c
108+ | S O = prim__lshrB16 x c
109+ | S (S O) = prim__lshrB32 x c
110+ | S (S (S _)) = prim__lshrB64 x c
111+
112+public
113+shiftRightLogical : Bits n -> Bits n -> Bits n
114+shiftRightLogical (MkBits x) (MkBits y) = MkBits (shiftRightLogical' x y)
115+
116+shiftRightArithmetic' : machineTy (nextBytes n) -> machineTy (nextBytes n) -> machineTy (nextBytes n)
117+shiftRightArithmetic' {n=n} x c with (nextBytes n)
118+ | O = pad8' n prim__ashrB8 x c
119+ | S O = pad16' n prim__ashrB16 x c
120+ | S (S O) = pad32' n prim__ashrB32 x c
121+ | S (S (S _)) = pad64' n prim__ashrB64 x c
122+
123+public
124+shiftRightArithmetic : Bits n -> Bits n -> Bits n
125+shiftRightArithmetic (MkBits x) (MkBits y) = MkBits (shiftRightArithmetic' x y)
126+
127+and' : machineTy n -> machineTy n -> machineTy n
128+and' {n=n} x y with n
129+ | O = prim__andB8 x y
130+ | S O = prim__andB16 x y
131+ | S (S O) = prim__andB32 x y
132+ | S (S (S _)) = prim__andB64 x y
133+
134+public
135+and : Bits n -> Bits n -> Bits n
136+and (MkBits x) (MkBits y) = MkBits (and' x y)
137+
138+or' : machineTy n -> machineTy n -> machineTy n
139+or' {n=n} x y with n
140+ | O = prim__orB8 x y
141+ | S O = prim__orB16 x y
142+ | S (S O) = prim__orB32 x y
143+ | S (S (S _)) = prim__orB64 x y
144+
145+public
146+or : Bits n -> Bits n -> Bits n
147+or (MkBits x) (MkBits y) = MkBits (or' x y)
148+
149+xor' : machineTy n -> machineTy n -> machineTy n
150+xor' {n=n} x y with n
151+ | O = prim__xorB8 x y
152+ | S O = prim__xorB16 x y
153+ | S (S O) = prim__xorB32 x y
154+ | S (S (S _)) = prim__xorB64 x y
155+
156+public
157+xor : Bits n -> Bits n -> Bits n
158+xor (MkBits x) (MkBits y) = MkBits (xor' x y)
159+
160+plus' : machineTy (nextBytes n) -> machineTy (nextBytes n) -> machineTy (nextBytes n)
161+plus' {n=n} x y with (nextBytes n)
162+ | O = pad8 n prim__addB8 x y
163+ | S O = pad16 n prim__addB16 x y
164+ | S (S O) = pad32 n prim__addB32 x y
165+ | S (S (S _)) = pad64 n prim__addB64 x y
166+
167+public
168+plus : Bits n -> Bits n -> Bits n
169+plus (MkBits x) (MkBits y) = MkBits (plus' x y)
170+
171+minus' : machineTy (nextBytes n) -> machineTy (nextBytes n) -> machineTy (nextBytes n)
172+minus' {n=n} x y with (nextBytes n)
173+ | O = pad8 n prim__subB8 x y
174+ | S O = pad16 n prim__subB16 x y
175+ | S (S O) = pad32 n prim__subB32 x y
176+ | S (S (S _)) = pad64 n prim__subB64 x y
177+
178+public
179+minus : Bits n -> Bits n -> Bits n
180+minus (MkBits x) (MkBits y) = MkBits (minus' x y)
181+
182+times' : machineTy (nextBytes n) -> machineTy (nextBytes n) -> machineTy (nextBytes n)
183+times' {n=n} x y with (nextBytes n)
184+ | O = pad8 n prim__mulB8 x y
185+ | S O = pad16 n prim__mulB16 x y
186+ | S (S O) = pad32 n prim__mulB32 x y
187+ | S (S (S _)) = pad64 n prim__mulB64 x y
188+
189+public
190+times : Bits n -> Bits n -> Bits n
191+times (MkBits x) (MkBits y) = MkBits (times' x y)
192+
193+partial
194+sdiv' : machineTy (nextBytes n) -> machineTy (nextBytes n) -> machineTy (nextBytes n)
195+sdiv' {n=n} x y with (nextBytes n)
196+ | O = prim__sdivB8 x y
197+ | S O = prim__sdivB16 x y
198+ | S (S O) = prim__sdivB32 x y
199+ | S (S (S _)) = prim__sdivB64 x y
200+
201+public partial
202+sdiv : Bits n -> Bits n -> Bits n
203+sdiv (MkBits x) (MkBits y) = MkBits (sdiv' x y)
204+
205+partial
206+udiv' : machineTy (nextBytes n) -> machineTy (nextBytes n) -> machineTy (nextBytes n)
207+udiv' {n=n} x y with (nextBytes n)
208+ | O = prim__udivB8 x y
209+ | S O = prim__udivB16 x y
210+ | S (S O) = prim__udivB32 x y
211+ | S (S (S _)) = prim__udivB64 x y
212+
213+public partial
214+udiv : Bits n -> Bits n -> Bits n
215+udiv (MkBits x) (MkBits y) = MkBits (udiv' x y)
216+
217+partial
218+srem' : machineTy (nextBytes n) -> machineTy (nextBytes n) -> machineTy (nextBytes n)
219+srem' {n=n} x y with (nextBytes n)
220+ | O = prim__sremB8 x y
221+ | S O = prim__sremB16 x y
222+ | S (S O) = prim__sremB32 x y
223+ | S (S (S _)) = prim__sremB64 x y
224+
225+public partial
226+srem : Bits n -> Bits n -> Bits n
227+srem (MkBits x) (MkBits y) = MkBits (srem' x y)
228+
229+partial
230+urem' : machineTy (nextBytes n) -> machineTy (nextBytes n) -> machineTy (nextBytes n)
231+urem' {n=n} x y with (nextBytes n)
232+ | O = prim__uremB8 x y
233+ | S O = prim__uremB16 x y
234+ | S (S O) = prim__uremB32 x y
235+ | S (S (S _)) = prim__uremB64 x y
236+
237+public partial
238+urem : Bits n -> Bits n -> Bits n
239+urem (MkBits x) (MkBits y) = MkBits (urem' x y)
240+
241+-- TODO: Proofy comparisons via postulates
242+lt : machineTy n -> machineTy n -> Int
243+lt {n=n} x y with n
244+ | O = prim__ltB8 x y
245+ | S O = prim__ltB16 x y
246+ | S (S O) = prim__ltB32 x y
247+ | S (S (S _)) = prim__ltB64 x y
248+
249+lte : machineTy n -> machineTy n -> Int
250+lte {n=n} x y with n
251+ | O = prim__lteB8 x y
252+ | S O = prim__lteB16 x y
253+ | S (S O) = prim__lteB32 x y
254+ | S (S (S _)) = prim__lteB64 x y
255+
256+eq : machineTy n -> machineTy n -> Int
257+eq {n=n} x y with n
258+ | O = prim__eqB8 x y
259+ | S O = prim__eqB16 x y
260+ | S (S O) = prim__eqB32 x y
261+ | S (S (S _)) = prim__eqB64 x y
262+
263+gte : machineTy n -> machineTy n -> Int
264+gte {n=n} x y with n
265+ | O = prim__gteB8 x y
266+ | S O = prim__gteB16 x y
267+ | S (S O) = prim__gteB32 x y
268+ | S (S (S _)) = prim__gteB64 x y
269+
270+gt : machineTy n -> machineTy n -> Int
271+gt {n=n} x y with n
272+ | O = prim__gtB8 x y
273+ | S O = prim__gtB16 x y
274+ | S (S O) = prim__gtB32 x y
275+ | S (S (S _)) = prim__gtB64 x y
276+
277+instance Eq (Bits n) where
278+ (MkBits x) == (MkBits y) = boolOp eq x y
279+
280+instance Ord (Bits n) where
281+ (MkBits x) < (MkBits y) = boolOp lt x y
282+ (MkBits x) <= (MkBits y) = boolOp lte x y
283+ (MkBits x) >= (MkBits y) = boolOp gte x y
284+ (MkBits x) > (MkBits y) = boolOp gt x y
285+ compare (MkBits x) (MkBits y) =
286+ if boolOp lt x y
287+ then LT
288+ else if boolOp eq x y
289+ then EQ
290+ else GT
291+
292+complement' : machineTy (nextBytes n) -> machineTy (nextBytes n)
293+complement' {n=n} x with (nextBytes n)
294+ | O = let pad = getPad {n=0} n in
295+ prim__complB8 (x `prim__shlB8` pad) `prim__lshrB8` pad
296+ | S O = let pad = getPad {n=1} n in
297+ prim__complB16 (x `prim__shlB16` pad) `prim__lshrB16` pad
298+ | S (S O) = let pad = getPad {n=2} n in
299+ prim__complB32 (x `prim__shlB32` pad) `prim__lshrB32` pad
300+ | S (S (S _)) = let pad = getPad {n=3} n in
301+ prim__complB64 (x `prim__shlB64` pad) `prim__lshrB64` pad
302+
303+public
304+complement : Bits n -> Bits n
305+complement (MkBits x) = MkBits (complement' x)
306+
307+-- TODO: Prove
308+zext' : machineTy (nextBytes n) -> machineTy (nextBytes (n+m))
309+zext' {n=n} {m=m} x with (nextBytes n, nextBytes (n+m))
310+ | (O, O) = believe_me x
311+ | (O, S O) = believe_me (prim__zextB8_16 (believe_me x))
312+ | (O, S (S O)) = believe_me (prim__zextB8_32 (believe_me x))
313+ | (O, S (S (S _))) = believe_me (prim__zextB8_64 (believe_me x))
314+ | (S O, S O) = believe_me x
315+ | (S O, S (S O)) = believe_me (prim__zextB16_32 (believe_me x))
316+ | (S O, S (S (S _))) = believe_me (prim__zextB16_64 (believe_me x))
317+ | (S (S O), S (S O)) = believe_me x
318+ | (S (S O), S (S (S _))) = believe_me (prim__zextB32_64 (believe_me x))
319+ | (S (S (S _)), S (S (S _))) = believe_me x
320+
321+public
322+zeroExtend : Bits n -> Bits (n+m)
323+zeroExtend (MkBits x) = MkBits (zext' x)
324+
325+%assert_total
326+intToBits' : Int -> machineTy (nextBytes n)
327+intToBits' {n=n} x with (nextBytes n)
328+ | O = let pad = getPad {n=0} n in
329+ prim__lshrB8 (prim__shlB8 (prim__intToB8 x) pad) pad
330+ | S O = let pad = getPad {n=1} n in
331+ prim__lshrB16 (prim__shlB16 (prim__intToB16 x) pad) pad
332+ | S (S O) = let pad = getPad {n=2} n in
333+ prim__lshrB32 (prim__shlB32 (prim__intToB32 x) pad) pad
334+ | S (S (S _)) = let pad = getPad {n=3} n in
335+ prim__lshrB64 (prim__shlB64 (prim__intToB64 x) pad) pad
336+
337+public
338+intToBits : Int -> Bits n
339+intToBits n = MkBits (intToBits' n)
340+
341+instance Cast Int (Bits n) where
342+ cast = intToBits
343+
344+bitsToInt' : machineTy n -> Int
345+bitsToInt' {n=n} x with n
346+ | O = prim__B32ToInt (prim__zextB8_32 x)
347+ | S O = prim__B32ToInt (prim__zextB16_32 x)
348+ | S (S O) = prim__B32ToInt x
349+ | S (S (S _)) = prim__B32ToInt (prim__truncB64_32 x)
350+
351+public
352+bitsToInt : Bits n -> Int
353+bitsToInt (MkBits x) = bitsToInt' x
354+
355+-- Zero out the high bits of a truncated bitstring
356+zeroUnused : machineTy (nextBytes n) -> machineTy (nextBytes n)
357+zeroUnused x = x `and'` complement' (intToBits' 0)
358+
359+instance Cast Nat (Bits n) where
360+ cast x = MkBits (zeroUnused (natToBits n))
361+
362+-- TODO: Prove
363+sext' : machineTy (nextBytes n) -> machineTy (nextBytes (n+m))
364+sext' {n=n} {m=m} x with (nextBytes n, nextBytes (n+m))
365+ | (O, O) = let pad = getPad {n=0} n in
366+ believe_me (prim__ashrB8 (prim__shlB8 (believe_me x) pad) pad)
367+ | (O, S O) = let pad = getPad {n=0} n in
368+ believe_me (prim__ashrB16 (prim__sextB8_16 (prim__shlB8 (believe_me x) pad))
369+ (prim__zextB8_16 pad))
370+ | (O, S (S O)) = let pad = getPad {n=0} n in
371+ believe_me (prim__ashrB32 (prim__sextB8_32 (prim__shlB8 (believe_me x) pad))
372+ (prim__zextB8_32 pad))
373+ | (O, S (S (S _))) = let pad = getPad {n=0} n in
374+ believe_me (prim__ashrB64 (prim__sextB8_64 (prim__shlB8 (believe_me x) pad))
375+ (prim__zextB8_64 pad))
376+ | (S O, S O) = let pad = getPad {n=1} n in
377+ believe_me (prim__ashrB16 (prim__shlB16 (believe_me x) pad) pad)
378+ | (S O, S (S O)) = let pad = getPad {n=1} n in
379+ believe_me (prim__ashrB32 (prim__sextB16_32 (prim__shlB16 (believe_me x) pad))
380+ (prim__zextB16_32 pad))
381+ | (S O, S (S (S _))) = let pad = getPad {n=1} n in
382+ believe_me (prim__ashrB64 (prim__sextB16_64 (prim__shlB16 (believe_me x) pad))
383+ (prim__zextB16_64 pad))
384+ | (S (S O), S (S O)) = let pad = getPad {n=2} n in
385+ believe_me (prim__ashrB32 (prim__shlB32 (believe_me x) pad) pad)
386+ | (S (S O), S (S (S _))) = let pad = getPad {n=2} n in
387+ believe_me (prim__ashrB64 (prim__sextB32_64 (prim__shlB32 (believe_me x) pad))
388+ (prim__zextB32_64 pad))
389+ | (S (S (S _)), S (S (S _))) = let pad = getPad {n=3} n in
390+ believe_me (prim__ashrB64 (prim__shlB64 (believe_me x) pad) pad)
391+
392+public
393+signExtend : Bits n -> Bits (n+m)
394+signExtend {m=m} (MkBits x) = MkBits (zeroUnused (sext' x))
395+
396+-- TODO: Prove
397+trunc' : machineTy (nextBytes (n+m)) -> machineTy (nextBytes n)
398+trunc' {n=n} {m=m} x with (nextBytes n, nextBytes (n+m))
399+ | (O, O) = believe_me x
400+ | (O, S O) = believe_me (prim__truncB16_8 (believe_me x))
401+ | (O, S (S O)) = believe_me (prim__truncB32_8 (believe_me x))
402+ | (O, S (S (S _))) = believe_me (prim__truncB64_8 (believe_me x))
403+ | (S O, S O) = believe_me x
404+ | (S O, S (S O)) = believe_me (prim__truncB32_16 (believe_me x))
405+ | (S O, S (S (S _))) = believe_me (prim__truncB64_16 (believe_me x))
406+ | (S (S O), S (S O)) = believe_me x
407+ | (S (S O), S (S (S _))) = believe_me (prim__truncB64_32 (believe_me x))
408+ | (S (S (S _)), S (S (S _))) = believe_me x
409+
410+public
411+truncate : Bits (n+m) -> Bits n
412+truncate (MkBits x) = MkBits (zeroUnused (trunc' x))
413+
414+public
415+bitAt : Fin n -> Bits n
416+bitAt n = intToBits 1 `shiftLeft` intToBits (cast n)
417+
418+public
419+getBit : Fin n -> Bits n -> Bool
420+getBit n x = (x `and` (bitAt n)) /= intToBits 0
421+
422+public
423+setBit : Fin n -> Bits n -> Bits n
424+setBit n x = x `or` (bitAt n)
425+
426+public
427+unsetBit : Fin n -> Bits n -> Bits n
428+unsetBit n x = x `and` complement (bitAt n)
429+
430+bitsToStr : Bits n -> String
431+bitsToStr x = pack (helper last x)
432+ where
433+ %assert_total
434+ helper : Fin (S n) -> Bits n -> List Char
435+ helper fO _ = []
436+ helper (fS x) b = (if getBit x b then '1' else '0') :: helper (weaken x) b
437+
438+instance Show (Bits n) where
439+ show = bitsToStr