@@ -26,6 +26,28 @@ machineTy (S O) = Bits16
2626machineTy (S (S O)) = Bits32
2727machineTy (S (S (S _))) = Bits64
2828
29+bitsUsed : Nat -> Nat
30+bitsUsed n = 8 * (2 `power` n)
31+
32+%assert_total
33+natToBits' : machineTy n -> Nat -> machineTy n
34+natToBits' a O = a
35+natToBits' {n=n} a x with n
36+ natToBits' a (S x') | O = natToBits' (prim__addB8 a (prim__intToB8 1)) x'
37+ natToBits' a (S x') | S O = natToBits' (prim__addB16 a (prim__intToB16 1)) x'
38+ natToBits' a (S x') | S (S O) = natToBits' (prim__addB32 a (prim__intToB32 1)) x'
39+ natToBits' a (S x') | S (S (S _)) = natToBits' (prim__addB64 a (prim__intToB64 1)) x'
40+
41+natToBits : Nat -> machineTy n
42+natToBits {n=n} x with n
43+ | O = natToBits' (prim__intToB8 0) x
44+ | S O = natToBits' (prim__intToB16 0) x
45+ | S (S O) = natToBits' (prim__intToB32 0) x
46+ | S (S (S _)) = natToBits' (prim__intToB64 0) x
47+
48+getPad : Nat -> machineTy n
49+getPad n = natToBits ((bitsUsed (nextBytes n)) - n)
50+
2951public
3052data Bits : Nat -> Type where
3153 MkBits : machineTy (nextBytes n) -> Bits n
@@ -33,73 +55,43 @@ data Bits : Nat -> Type where
3355pad8 : Nat -> (Bits8 -> Bits8 -> Bits8) -> Bits8 -> Bits8 -> Bits8
3456pad8 n f x y = prim__lshrB8 (f (prim__shlB8 x pad) (prim__shlB8 y pad)) pad
3557 where
36− pad = (prim__intToB8 (cast (8-n)))
58+ pad = getPad {n=0} n
3759
3860pad16 : Nat -> (Bits16 -> Bits16 -> Bits16) -> Bits16 -> Bits16 -> Bits16
3961pad16 n f x y = prim__lshrB16 (f (prim__shlB16 x pad) (prim__shlB16 y pad)) pad
4062 where
41− pad = (prim__intToB16 (cast (16-n)))
63+ pad = getPad {n=1} n
4264
4365pad32 : Nat -> (Bits32 -> Bits32 -> Bits32) -> Bits32 -> Bits32 -> Bits32
4466pad32 n f x y = prim__lshrB32 (f (prim__shlB32 x pad) (prim__shlB32 y pad)) pad
4567 where
46− pad = (prim__intToB32 (cast (32-n)))
68+ pad = getPad {n=2} n
4769
4870pad64 : Nat -> (Bits64 -> Bits64 -> Bits64) -> Bits64 -> Bits64 -> Bits64
4971pad64 n f x y = prim__lshrB64 (f (prim__shlB64 x pad) (prim__shlB64 y pad)) pad
5072 where
51− pad = (prim__intToB64 (cast (64-n)))
73+ pad = getPad {n=3} n
5274
5375-- These versions only pad the first operand
5476pad8' : Nat -> (Bits8 -> Bits8 -> Bits8) -> Bits8 -> Bits8 -> Bits8
5577pad8' n f x y = prim__lshrB8 (f (prim__shlB8 x pad) y) pad
5678 where
57− pad = (prim__intToB8 (cast (8-n)))
79+ pad = getPad {n=0} n
5880
5981pad16' : Nat -> (Bits16 -> Bits16 -> Bits16) -> Bits16 -> Bits16 -> Bits16
6082pad16' n f x y = prim__lshrB16 (f (prim__shlB16 x pad) y) pad
6183 where
62− pad = (prim__intToB16 (cast (16-n)))
84+ pad = getPad {n=1} n
6385
6486pad32' : Nat -> (Bits32 -> Bits32 -> Bits32) -> Bits32 -> Bits32 -> Bits32
6587pad32' n f x y = prim__lshrB32 (f (prim__shlB32 x pad) y) pad
6688 where
67− pad = (prim__intToB32 (cast (32-n)))
89+ pad = getPad {n=2} n
6890
6991pad64' : Nat -> (Bits64 -> Bits64 -> Bits64) -> Bits64 -> Bits64 -> Bits64
7092pad64' n f x y = prim__lshrB64 (f (prim__shlB64 x pad) y) pad
7193 where
72− pad = (prim__intToB64 (cast (64-n)))
73−
74−%assert_total
75−intToBits' : Int -> machineTy (nextBytes n)
76−intToBits' {n=n} x with (nextBytes n)
77− | O = let pad = (prim__intToB8 (cast (8-n))) in
78− prim__lshrB8 (prim__shlB8 (prim__intToB8 x) pad) pad
79− | S O = let pad = (prim__intToB16 (cast (16-n))) in
80− prim__lshrB16 (prim__shlB16 (prim__intToB16 x) pad) pad
81− | S (S O) = let pad = (prim__intToB32 (cast (32-n))) in
82− prim__lshrB32 (prim__shlB32 (prim__intToB32 x) pad) pad
83− | S (S (S _)) = let pad = (prim__intToB64 (cast (64-n))) in
84− prim__lshrB64 (prim__shlB64 (prim__intToB64 x) pad) pad
85−
86−public
87−intToBits : Int -> Bits n
88−intToBits n = MkBits (intToBits' n)
89−
90−instance Cast Int (Bits n) where
91− cast = intToBits
92−
93−bitsToInt' : machineTy n -> Int
94−bitsToInt' {n=n} x with n
95− | O = prim__B32ToInt (prim__zextB8_32 x)
96− | S O = prim__B32ToInt (prim__zextB16_32 x)
97− | S (S O) = prim__B32ToInt x
98− | S (S (S _)) = prim__B32ToInt (prim__truncB64_32 x)
99−
100−public
101−bitsToInt : Bits n -> Int
102−bitsToInt (MkBits x) = bitsToInt' x
94+ pad = getPad {n=3} n
10395
10496shiftLeft' : machineTy (nextBytes n) -> machineTy (nextBytes n) -> machineTy (nextBytes n)
10597shiftLeft' {n=n} x c with (nextBytes n)
@@ -301,13 +293,13 @@ instance Ord (Bits n) where
301293
302294complement' : machineTy (nextBytes n) -> machineTy (nextBytes n)
303295complement' {n=n} x with (nextBytes n)
304− | O = let pad = prim__intToB8 (8 - cast n) in
296+ | O = let pad = getPad {n=0} n in
305297 prim__complB8 (x `prim__shlB8` pad) `prim__lshrB8` pad
306− | S O = let pad = prim__intToB16 (16 - cast n) in
298+ | S O = let pad = getPad {n=1} n in
307299 prim__complB16 (x `prim__shlB16` pad) `prim__lshrB16` pad
308− | S (S O) = let pad = prim__intToB32 (32 - cast n) in
300+ | S (S O) = let pad = getPad {n=2} n in
309301 prim__complB32 (x `prim__shlB32` pad) `prim__lshrB32` pad
310− | S (S (S _)) = let pad = prim__intToB64 (64 - cast n) in
302+ | S (S (S _)) = let pad = getPad {n=3} n in
311303 prim__complB64 (x `prim__shlB64` pad) `prim__lshrB64` pad
312304
313305public
@@ -315,7 +307,6 @@ complement : Bits n -> Bits n
315307complement (MkBits x) = MkBits (complement' x)
316308
317309-- TODO: Prove
318−%assert_total
319310zext' : machineTy (nextBytes n) -> machineTy (nextBytes (n+m))
320311zext' {n=n} {m=m} x with (nextBytes n, nextBytes (n+m))
321312 | (O, O) = believe_me x
@@ -329,56 +320,100 @@ zext' {n=n} {m=m} x with (nextBytes n, nextBytes (n+m))
329320 | (S (S O), S (S (S _))) = believe_me (prim__zextB32_64 (believe_me x))
330321 | (S (S (S _)), S (S (S _))) = believe_me x
331322
332−public partial
323+public
333324zeroExtend : Bits n -> Bits (n+m)
334325zeroExtend (MkBits x) = MkBits (zext' x)
335326
336−-- Fill in the high bits of a sign-extended bitstring
337−fixupSE : (m : Nat) -> machineTy (nextBytes (n+m)) -> machineTy (nextBytes (n+m))
338−fixupSE m x = x `or'` complement' (zext' {m=m} (complement' (intToBits' 0)))
327+%assert_total
328+intToBits' : Int -> machineTy (nextBytes n)
329+intToBits' {n=n} x with (nextBytes n)
330+ | O = let pad = getPad {n=0} n in
331+ prim__lshrB8 (prim__shlB8 (prim__intToB8 x) pad) pad
332+ | S O = let pad = getPad {n=1} n in
333+ prim__lshrB16 (prim__shlB16 (prim__intToB16 x) pad) pad
334+ | S (S O) = let pad = getPad {n=2} n in
335+ prim__lshrB32 (prim__shlB32 (prim__intToB32 x) pad) pad
336+ | S (S (S _)) = let pad = getPad {n=3} n in
337+ prim__lshrB64 (prim__shlB64 (prim__intToB64 x) pad) pad
338+
339+public
340+intToBits : Int -> Bits n
341+intToBits n = MkBits (intToBits' n)
342+
343+instance Cast Int (Bits n) where
344+ cast = intToBits
345+
346+bitsToInt' : machineTy n -> Int
347+bitsToInt' {n=n} x with n
348+ | O = prim__B32ToInt (prim__zextB8_32 x)
349+ | S O = prim__B32ToInt (prim__zextB16_32 x)
350+ | S (S O) = prim__B32ToInt x
351+ | S (S (S _)) = prim__B32ToInt (prim__truncB64_32 x)
352+
353+public
354+bitsToInt : Bits n -> Int
355+bitsToInt (MkBits x) = bitsToInt' x
356+
357+-- Zero out the high bits of a truncated bitstring
358+zeroUnused : machineTy (nextBytes n) -> machineTy (nextBytes n)
359+zeroUnused x = x `and'` complement' (intToBits' 0)
360+
361+instance Cast Nat (Bits n) where
362+ cast x = MkBits (zeroUnused (natToBits n))
339363
340364-- TODO: Prove
341−%assert_total
342365sext' : machineTy (nextBytes n) -> machineTy (nextBytes (n+m))
343366sext' {n=n} {m=m} x with (nextBytes n, nextBytes (n+m))
344− | (O, O) = fixupSE m (believe_me x)
345− | (O, S O) = fixupSE m (believe_me (prim__sextB8_16 (believe_me x)))
346− | (O, S (S O)) = fixupSE m (believe_me (prim__sextB8_32 (believe_me x)))
347− | (O, S (S (S _))) = fixupSE m (believe_me (prim__sextB8_64 (believe_me x)))
348− | (S O, S O) = fixupSE m (believe_me x)
349− | (S O, S (S O)) = fixupSE m (believe_me (prim__sextB16_32 (believe_me x)))
350− | (S O, S (S (S _))) = fixupSE m (believe_me (prim__sextB16_64 (believe_me x)))
351− | (S (S O), S (S O)) = fixupSE m (believe_me x)
352− | (S (S O), S (S (S _))) = fixupSE m (believe_me (prim__sextB32_64 (believe_me x)))
353− | (S (S (S _)), S (S (S _))) = fixupSE m (believe_me x)
367+ | (O, O) = let pad = getPad {n=0} n in
368+ believe_me (prim__ashrB8 (prim__shlB8 (believe_me x) pad) pad)
369+ | (O, S O) = let pad = getPad {n=0} n in
370+ believe_me (prim__ashrB16 (prim__sextB8_16 (prim__shlB8 (believe_me x) pad))
371+ (prim__zextB8_16 pad))
372+ | (O, S (S O)) = let pad = getPad {n=0} n in
373+ believe_me (prim__ashrB32 (prim__sextB8_32 (prim__shlB8 (believe_me x) pad))
374+ (prim__zextB8_32 pad))
375+ | (O, S (S (S _))) = let pad = getPad {n=0} n in
376+ believe_me (prim__ashrB64 (prim__sextB8_64 (prim__shlB8 (believe_me x) pad))
377+ (prim__zextB8_64 pad))
378+ | (S O, S O) = let pad = getPad {n=1} n in
379+ believe_me (prim__ashrB16 (prim__shlB16 (believe_me x) pad) pad)
380+ | (S O, S (S O)) = let pad = getPad {n=1} n in
381+ believe_me (prim__ashrB32 (prim__sextB16_32 (prim__shlB16 (believe_me x) pad))
382+ (prim__zextB16_32 pad))
383+ | (S O, S (S (S _))) = let pad = getPad {n=1} n in
384+ believe_me (prim__ashrB64 (prim__sextB16_64 (prim__shlB16 (believe_me x) pad))
385+ (prim__zextB16_64 pad))
386+ | (S (S O), S (S O)) = let pad = getPad {n=2} n in
387+ believe_me (prim__ashrB32 (prim__shlB32 (believe_me x) pad) pad)
388+ | (S (S O), S (S (S _))) = let pad = getPad {n=2} n in
389+ believe_me (prim__ashrB64 (prim__sextB32_64 (prim__shlB32 (believe_me x) pad))
390+ (prim__zextB32_64 pad))
391+ | (S (S (S _)), S (S (S _))) = let pad = getPad {n=3} n in
392+ believe_me (prim__ashrB64 (prim__shlB64 (believe_me x) pad) pad)
354393
355−public partial
394+public
356395signExtend : Bits n -> Bits (n+m)
357−signExtend (MkBits x) = MkBits (sext' x)
358−
359−-- Zero out the high bits of a truncated bitstring
360−fixupTR : machineTy (nextBytes n) -> machineTy (nextBytes n)
361−fixupTR x = x `and'` complement' (intToBits' 0)
396+signExtend {m=m} (MkBits x) = MkBits (zeroUnused (sext' x))
362397
363398-- TODO: Prove
364−%assert_total
365399trunc' : machineTy (nextBytes (n+m)) -> machineTy (nextBytes n)
366400trunc' {n=n} {m=m} x with (nextBytes n, nextBytes (n+m))
367− | (O, O) = fixupTR (believe_me x)
401+ | (O, O) = believe_me x
368402 | (O, S O) = believe_me (prim__truncB16_8 (believe_me x))
369403 | (O, S (S O)) = believe_me (prim__truncB32_8 (believe_me x))
370404 | (O, S (S (S _))) = believe_me (prim__truncB64_8 (believe_me x))
371− | (S O, S O) = fixupTR (believe_me x)
405+ | (S O, S O) = believe_me x
372406 | (S O, S (S O)) = believe_me (prim__truncB32_16 (believe_me x))
373407 | (S O, S (S (S _))) = believe_me (prim__truncB64_16 (believe_me x))
374− | (S (S O), S (S O)) = fixupTR (believe_me x)
408+ | (S (S O), S (S O)) = believe_me x
375409 | (S (S O), S (S (S _))) = believe_me (prim__truncB64_32 (believe_me x))
376− | (S (S (S _)), S (S (S _))) = fixupTR (believe_me x)
410+ | (S (S (S _)), S (S (S _))) = believe_me x
377411
378−public partial
412+public
379413truncate : Bits (n+m) -> Bits n
380−truncate (MkBits x) = MkBits (trunc' x)
414+truncate (MkBits x) = MkBits (zeroUnused (trunc' x))
381415
416+public
382417bitAt : Fin n -> Bits n
383418bitAt n = intToBits 1 `shiftLeft` intToBits (cast n)
384419