@@ -4,14 +4,21 @@ import Prelude.Strings
44
55%default total
66
7−log2ceil : Nat -> Nat
8−log2ceil n = let x = log2 n in
9− if x == log2 (n-1)
10− then x+1
11− else x
7+divCeil : Nat -> Nat -> Nat
8+divCeil x y = case x `mod` y of
9+ O => x `div` y
10+ S _ => S (x `div` y)
11+
12+nextPow2 : Nat -> Nat
13+nextPow2 O = O
14+nextPow2 x = if x == (2 `power` l2x)
15+ then l2x
16+ else S l2x
17+ where
18+ l2x = log2 x
1219
13−log2Bytes : Nat -> Nat
14−log2Bytes bits = (log2ceil (bits `div` 8))
20+nextBytes : Nat -> Nat
21+nextBytes bits = (nextPow2 (bits `divCeil` 8))
1522
1623machineTy : Nat -> Type
1724machineTy O = Bits8
@@ -21,7 +28,7 @@ machineTy (S (S (S _))) = Bits64
2128
2229public
2330data Bits : Nat -> Type where
24− MkBits : machineTy (log2Bytes n) -> Bits n
31+ MkBits : machineTy (nextBytes n) -> Bits n
2532
2633pad8 : Nat -> (Bits8 -> Bits8 -> Bits8) -> Bits8 -> Bits8 -> Bits8
2734pad8 n f x y = prim__lshrB8 (f (prim__shlB8 x pad) (prim__shlB8 y pad)) pad
@@ -65,8 +72,8 @@ pad64' n f x y = prim__lshrB64 (f (prim__shlB64 x pad) y) pad
6572 pad = (prim__intToB64 (cast (64-n)))
6673
6774%assert_total
68−intToBits' : Int -> machineTy (log2Bytes n)
69−intToBits' {n=n} x with (log2Bytes n)
75+intToBits' : Int -> machineTy (nextBytes n)
76+intToBits' {n=n} x with (nextBytes n)
7077 | O = let pad = (prim__intToB8 (cast (8-n))) in
7178 prim__lshrB8 (prim__shlB8 (prim__intToB8 x) pad) pad
7279 | S O = let pad = (prim__intToB16 (cast (16-n))) in
@@ -94,8 +101,8 @@ public
94101bitsToInt : Bits n -> Int
95102bitsToInt (MkBits x) = bitsToInt' x
96103
97−shiftLeft' : machineTy (log2Bytes n) -> machineTy (log2Bytes n) -> machineTy (log2Bytes n)
98−shiftLeft' {n=n} x c with (log2Bytes n)
104+shiftLeft' : machineTy (nextBytes n) -> machineTy (nextBytes n) -> machineTy (nextBytes n)
105+shiftLeft' {n=n} x c with (nextBytes n)
99106 | O = pad8' n prim__shlB8 x c
100107 | S O = pad16' n prim__shlB16 x c
101108 | S (S O) = pad32' n prim__shlB32 x c
@@ -116,8 +123,8 @@ public
116123shiftRightLogical : Bits n -> Bits n -> Bits n
117124shiftRightLogical (MkBits x) (MkBits y) = MkBits (shiftRightLogical' x y)
118125
119−shiftRightArithmetic' : machineTy (log2Bytes n) -> machineTy (log2Bytes n) -> machineTy (log2Bytes n)
120−shiftRightArithmetic' {n=n} x c with (log2Bytes n)
126+shiftRightArithmetic' : machineTy (nextBytes n) -> machineTy (nextBytes n) -> machineTy (nextBytes n)
127+shiftRightArithmetic' {n=n} x c with (nextBytes n)
121128 | O = pad8' n prim__ashrB8 x c
122129 | S O = pad16' n prim__ashrB16 x c
123130 | S (S O) = pad32' n prim__ashrB32 x c
@@ -160,8 +167,8 @@ public
160167xor : Bits n -> Bits n -> Bits n
161168xor (MkBits x) (MkBits y) = MkBits (xor' x y)
162169
163−plus' : machineTy (log2Bytes n) -> machineTy (log2Bytes n) -> machineTy (log2Bytes n)
164−plus' {n=n} x y with (log2Bytes n)
170+plus' : machineTy (nextBytes n) -> machineTy (nextBytes n) -> machineTy (nextBytes n)
171+plus' {n=n} x y with (nextBytes n)
165172 | O = pad8 n prim__addB8 x y
166173 | S O = pad16 n prim__addB16 x y
167174 | S (S O) = pad32 n prim__addB32 x y
@@ -171,8 +178,8 @@ public
171178plus : Bits n -> Bits n -> Bits n
172179plus (MkBits x) (MkBits y) = MkBits (plus' x y)
173180
174−minus' : machineTy (log2Bytes n) -> machineTy (log2Bytes n) -> machineTy (log2Bytes n)
175−minus' {n=n} x y with (log2Bytes n)
181+minus' : machineTy (nextBytes n) -> machineTy (nextBytes n) -> machineTy (nextBytes n)
182+minus' {n=n} x y with (nextBytes n)
176183 | O = pad8 n prim__subB8 x y
177184 | S O = pad16 n prim__subB16 x y
178185 | S (S O) = pad32 n prim__subB32 x y
@@ -182,8 +189,8 @@ public
182189minus : Bits n -> Bits n -> Bits n
183190minus (MkBits x) (MkBits y) = MkBits (minus' x y)
184191
185−times' : machineTy (log2Bytes n) -> machineTy (log2Bytes n) -> machineTy (log2Bytes n)
186−times' {n=n} x y with (log2Bytes n)
192+times' : machineTy (nextBytes n) -> machineTy (nextBytes n) -> machineTy (nextBytes n)
193+times' {n=n} x y with (nextBytes n)
187194 | O = pad8 n prim__mulB8 x y
188195 | S O = pad16 n prim__mulB16 x y
189196 | S (S O) = pad32 n prim__mulB32 x y
@@ -194,8 +201,8 @@ times : Bits n -> Bits n -> Bits n
194201times (MkBits x) (MkBits y) = MkBits (times' x y)
195202
196203partial
197−sdiv' : machineTy (log2Bytes n) -> machineTy (log2Bytes n) -> machineTy (log2Bytes n)
198−sdiv' {n=n} x y with (log2Bytes n)
204+sdiv' : machineTy (nextBytes n) -> machineTy (nextBytes n) -> machineTy (nextBytes n)
205+sdiv' {n=n} x y with (nextBytes n)
199206 | O = prim__sdivB8 x y
200207 | S O = prim__sdivB16 x y
201208 | S (S O) = prim__sdivB32 x y
@@ -206,8 +213,8 @@ sdiv : Bits n -> Bits n -> Bits n
206213sdiv (MkBits x) (MkBits y) = MkBits (sdiv' x y)
207214
208215partial
209−udiv' : machineTy (log2Bytes n) -> machineTy (log2Bytes n) -> machineTy (log2Bytes n)
210−udiv' {n=n} x y with (log2Bytes n)
216+udiv' : machineTy (nextBytes n) -> machineTy (nextBytes n) -> machineTy (nextBytes n)
217+udiv' {n=n} x y with (nextBytes n)
211218 | O = prim__udivB8 x y
212219 | S O = prim__udivB16 x y
213220 | S (S O) = prim__udivB32 x y
@@ -218,8 +225,8 @@ udiv : Bits n -> Bits n -> Bits n
218225udiv (MkBits x) (MkBits y) = MkBits (udiv' x y)
219226
220227partial
221−srem' : machineTy (log2Bytes n) -> machineTy (log2Bytes n) -> machineTy (log2Bytes n)
222−srem' {n=n} x y with (log2Bytes n)
228+srem' : machineTy (nextBytes n) -> machineTy (nextBytes n) -> machineTy (nextBytes n)
229+srem' {n=n} x y with (nextBytes n)
223230 | O = prim__sremB8 x y
224231 | S O = prim__sremB16 x y
225232 | S (S O) = prim__sremB32 x y
@@ -230,8 +237,8 @@ srem : Bits n -> Bits n -> Bits n
230237srem (MkBits x) (MkBits y) = MkBits (srem' x y)
231238
232239partial
233−urem' : machineTy (log2Bytes n) -> machineTy (log2Bytes n) -> machineTy (log2Bytes n)
234−urem' {n=n} x y with (log2Bytes n)
240+urem' : machineTy (nextBytes n) -> machineTy (nextBytes n) -> machineTy (nextBytes n)
241+urem' {n=n} x y with (nextBytes n)
235242 | O = prim__uremB8 x y
236243 | S O = prim__uremB16 x y
237244 | S (S O) = prim__uremB32 x y
@@ -292,8 +299,8 @@ instance Ord (Bits n) where
292299 then EQ
293300 else GT
294301
295−complement' : machineTy (log2Bytes n) -> machineTy (log2Bytes n)
296−complement' {n=n} x with (log2Bytes n)
302+complement' : machineTy (nextBytes n) -> machineTy (nextBytes n)
303+complement' {n=n} x with (nextBytes n)
297304 | O = let pad = prim__intToB8 (8 - cast n) in
298305 prim__complB8 (x `prim__shlB8` pad) `prim__lshrB8` pad
299306 | S O = let pad = prim__intToB16 (16 - cast n) in
@@ -309,8 +316,8 @@ complement (MkBits x) = MkBits (complement' x)
309316
310317-- TODO: Prove
311318%assert_total
312−zext' : machineTy (log2Bytes n) -> machineTy (log2Bytes (n+m))
313−zext' {n=n} {m=m} x with (log2Bytes n, log2Bytes (n+m))
319+zext' : machineTy (nextBytes n) -> machineTy (nextBytes (n+m))
320+zext' {n=n} {m=m} x with (nextBytes n, nextBytes (n+m))
314321 | (O, O) = believe_me x
315322 | (O, S O) = believe_me (prim__zextB8_16 (believe_me x))
316323 | (O, S (S O)) = believe_me (prim__zextB8_32 (believe_me x))
@@ -327,13 +334,13 @@ zeroExtend : Bits n -> Bits (n+m)
327334zeroExtend (MkBits x) = MkBits (zext' x)
328335
329336-- Fill in the high bits of a sign-extended bitstring
330−fixupSE : (m : Nat) -> machineTy (log2Bytes (n+m)) -> machineTy (log2Bytes (n+m))
337+fixupSE : (m : Nat) -> machineTy (nextBytes (n+m)) -> machineTy (nextBytes (n+m))
331338fixupSE m x = x `or'` complement' (zext' {m=m} (complement' (intToBits' 0)))
332339
333340-- TODO: Prove
334341%assert_total
335−sext' : machineTy (log2Bytes n) -> machineTy (log2Bytes (n+m))
336−sext' {n=n} {m=m} x with (log2Bytes n, log2Bytes (n+m))
342+sext' : machineTy (nextBytes n) -> machineTy (nextBytes (n+m))
343+sext' {n=n} {m=m} x with (nextBytes n, nextBytes (n+m))
337344 | (O, O) = fixupSE m (believe_me x)
338345 | (O, S O) = fixupSE m (believe_me (prim__sextB8_16 (believe_me x)))
339346 | (O, S (S O)) = fixupSE m (believe_me (prim__sextB8_32 (believe_me x)))
@@ -350,13 +357,13 @@ signExtend : Bits n -> Bits (n+m)
350357signExtend (MkBits x) = MkBits (sext' x)
351358
352359-- Zero out the high bits of a truncated bitstring
353−fixupTR : machineTy (log2Bytes n) -> machineTy (log2Bytes n)
360+fixupTR : machineTy (nextBytes n) -> machineTy (nextBytes n)
354361fixupTR x = x `and'` complement' (intToBits' 0)
355362
356363-- TODO: Prove
357364%assert_total
358−trunc' : machineTy (log2Bytes (n+m)) -> machineTy (log2Bytes n)
359−trunc' {n=n} {m=m} x with (log2Bytes n, log2Bytes (n+m))
365+trunc' : machineTy (nextBytes (n+m)) -> machineTy (nextBytes n)
366+trunc' {n=n} {m=m} x with (nextBytes n, nextBytes (n+m))
360367 | (O, O) = fixupTR (believe_me x)
361368 | (O, S O) = believe_me (prim__truncB16_8 (believe_me x))
362369 | (O, S (S O)) = believe_me (prim__truncB32_8 (believe_me x))