@@ -3,6 +3,7 @@ module Data.Bits
33import Data.Fin
44
55%default total
6+%access export
67
78public export
89nextPow2 : Nat -> Nat
@@ -28,7 +29,7 @@ bitsUsed : Nat -> Nat
2829bitsUsed n = 8 * (2 `power` n)
2930
3031%assert_total
31−natToBits' : machineTy n -> Nat -> machineTy n
32+natToBits' : %static {n : Nat} -> machineTy n -> Nat -> machineTy n
3233natToBits' a Z = a
3334natToBits' {n=n} a x with (n)
3435 -- it seems I have to manually recover the value of n here, instead of being able to reference it
@@ -37,14 +38,14 @@ natToBits' {n=n} a x with (n)
3738 natToBits' a (S x') | S (S Z) = natToBits' {n=2} (prim__addB32 a (prim__truncInt_B32 1)) x'
3839 natToBits' a (S x') | S (S (S _)) = natToBits' {n=3} (prim__addB64 a (prim__truncInt_B64 1)) x'
3940
40−natToBits : Nat -> machineTy n
41+natToBits : %static {n : Nat} -> Nat -> machineTy n
4142natToBits {n=n} x with (n)
4243 | Z = natToBits' {n=0} (prim__truncInt_B8 0) x
4344 | S Z = natToBits' {n=1} (prim__truncInt_B16 0) x
4445 | S (S Z) = natToBits' {n=2} (prim__truncInt_B32 0) x
4546 | S (S (S _)) = natToBits' {n=3} (prim__truncInt_B64 0) x
4647
47−getPad : Nat -> machineTy n
48+getPad : %static {n : Nat} -> Nat -> machineTy n
4849getPad n = natToBits (minus (bitsUsed (nextBytes n)) n)
4950
5051public export
@@ -92,83 +93,69 @@ pad64' n f x y = prim__lshrB64 (f (prim__shlB64 x pad) y) pad
9293 where
9394 pad = getPad {n=3} n
9495
95−-- TODO: This (and all the other functions along these lings) is public export
96−-- because it is used by public export things. Do they really need to be
96+-- TODO: This (and all the other functions along these lings) is -- because it is used by things. Do they really need to be
9797-- public export, or is export good enough?
98−public export
99−shiftLeft' : machineTy (nextBytes n) -> machineTy (nextBytes n) -> machineTy (nextBytes n)
98+shiftLeft' : %static {n : Nat} -> machineTy (nextBytes n) -> machineTy (nextBytes n) -> machineTy (nextBytes n)
10099shiftLeft' {n=n} x c with (nextBytes n)
101100 | Z = pad8' n prim__shlB8 x c
102101 | S Z = pad16' n prim__shlB16 x c
103102 | S (S Z) = pad32' n prim__shlB32 x c
104103 | S (S (S _)) = pad64' n prim__shlB64 x c
105104
106−public export
107−shiftLeft : Bits n -> Bits n -> Bits n
105+shiftLeft : %static {n : Nat} -> Bits n -> Bits n -> Bits n
108106shiftLeft (MkBits x) (MkBits y) = MkBits (shiftLeft' x y)
109107
110−public export
111−shiftRightLogical' : machineTy n -> machineTy n -> machineTy n
108+shiftRightLogical' : %static {n : Nat} -> machineTy n -> machineTy n -> machineTy n
112109shiftRightLogical' {n=n} x c with (n)
113110 | Z = prim__lshrB8 x c
114111 | S Z = prim__lshrB16 x c
115112 | S (S Z) = prim__lshrB32 x c
116113 | S (S (S _)) = prim__lshrB64 x c
117114
118−public export
119−shiftRightLogical : Bits n -> Bits n -> Bits n
115+shiftRightLogical : %static {n : Nat} -> Bits n -> Bits n -> Bits n
120116shiftRightLogical {n} (MkBits x) (MkBits y)
121117 = MkBits {n} (shiftRightLogical' {n=nextBytes n} x y)
122118
123−public export
124−shiftRightArithmetic' : machineTy (nextBytes n) -> machineTy (nextBytes n) -> machineTy (nextBytes n)
119+shiftRightArithmetic' : %static {n : Nat} -> machineTy (nextBytes n) -> machineTy (nextBytes n) -> machineTy (nextBytes n)
125120shiftRightArithmetic' {n=n} x c with (nextBytes n)
126121 | Z = pad8' n prim__ashrB8 x c
127122 | S Z = pad16' n prim__ashrB16 x c
128123 | S (S Z) = pad32' n prim__ashrB32 x c
129124 | S (S (S _)) = pad64' n prim__ashrB64 x c
130125
131−public export
132−shiftRightArithmetic : Bits n -> Bits n -> Bits n
126+shiftRightArithmetic : %static {n : Nat} -> Bits n -> Bits n -> Bits n
133127shiftRightArithmetic (MkBits x) (MkBits y) = MkBits (shiftRightArithmetic' x y)
134128
135−public export
136−and' : machineTy n -> machineTy n -> machineTy n
129+and' : %static {n : Nat} -> machineTy n -> machineTy n -> machineTy n
137130and' {n=n} x y with (n)
138131 | Z = prim__andB8 x y
139132 | S Z = prim__andB16 x y
140133 | S (S Z) = prim__andB32 x y
141134 | S (S (S _)) = prim__andB64 x y
142135
143−public export
144−and : Bits n -> Bits n -> Bits n
136+and : %static {n : Nat} -> Bits n -> Bits n -> Bits n
145137and {n} (MkBits x) (MkBits y) = MkBits (and' {n=nextBytes n} x y)
146138
147−public export
148−or' : machineTy n -> machineTy n -> machineTy n
139+or' : %static {n : Nat} -> machineTy n -> machineTy n -> machineTy n
149140or' {n=n} x y with (n)
150141 | Z = prim__orB8 x y
151142 | S Z = prim__orB16 x y
152143 | S (S Z) = prim__orB32 x y
153144 | S (S (S _)) = prim__orB64 x y
154145
155−public export
156−or : Bits n -> Bits n -> Bits n
146+or : %static {n : Nat} -> Bits n -> Bits n -> Bits n
157147or {n} (MkBits x) (MkBits y) = MkBits (or' {n=nextBytes n} x y)
158148
159−public export
160−xor' : machineTy n -> machineTy n -> machineTy n
149+xor' : %static {n : Nat} -> machineTy n -> machineTy n -> machineTy n
161150xor' {n=n} x y with (n)
162151 | Z = prim__xorB8 x y
163152 | S Z = prim__xorB16 x y
164153 | S (S Z) = prim__xorB32 x y
165154 | S (S (S _)) = prim__xorB64 x y
166155
167−public export
168−xor : Bits n -> Bits n -> Bits n
156+xor : %static {n : Nat} -> Bits n -> Bits n -> Bits n
169157xor {n} (MkBits x) (MkBits y) = MkBits {n} (xor' {n=nextBytes n} x y)
170158
171−public export
172159plus' : machineTy (nextBytes n) -> machineTy (nextBytes n) -> machineTy (nextBytes n)
173160plus' {n=n} x y with (nextBytes n)
174161 | Z = pad8 n prim__addB8 x y
@@ -176,11 +163,9 @@ plus' {n=n} x y with (nextBytes n)
176163 | S (S Z) = pad32 n prim__addB32 x y
177164 | S (S (S _)) = pad64 n prim__addB64 x y
178165
179−public export
180−plus : Bits n -> Bits n -> Bits n
166+plus : %static {n : Nat} -> Bits n -> Bits n -> Bits n
181167plus (MkBits x) (MkBits y) = MkBits (plus' x y)
182168
183−public export
184169minus' : machineTy (nextBytes n) -> machineTy (nextBytes n) -> machineTy (nextBytes n)
185170minus' {n=n} x y with (nextBytes n)
186171 | Z = pad8 n prim__subB8 x y
@@ -188,11 +173,9 @@ minus' {n=n} x y with (nextBytes n)
188173 | S (S Z) = pad32 n prim__subB32 x y
189174 | S (S (S _)) = pad64 n prim__subB64 x y
190175
191−public export
192−minus : Bits n -> Bits n -> Bits n
176+minus : %static {n : Nat} -> Bits n -> Bits n -> Bits n
193177minus (MkBits x) (MkBits y) = MkBits (minus' x y)
194178
195−public export
196179times' : machineTy (nextBytes n) -> machineTy (nextBytes n) -> machineTy (nextBytes n)
197180times' {n=n} x y with (nextBytes n)
198181 | Z = pad8 n prim__mulB8 x y
@@ -200,12 +183,10 @@ times' {n=n} x y with (nextBytes n)
200183 | S (S Z) = pad32 n prim__mulB32 x y
201184 | S (S (S _)) = pad64 n prim__mulB64 x y
202185
203−public export
204−times : Bits n -> Bits n -> Bits n
186+times : %static {n : Nat} -> Bits n -> Bits n -> Bits n
205187times (MkBits x) (MkBits y) = MkBits (times' x y)
206188
207189partial
208−public export
209190sdiv' : machineTy (nextBytes n) -> machineTy (nextBytes n) -> machineTy (nextBytes n)
210191sdiv' {n=n} x y with (nextBytes n)
211192 | Z = prim__sdivB8 x y
@@ -213,88 +194,85 @@ sdiv' {n=n} x y with (nextBytes n)
213194 | S (S Z) = prim__sdivB32 x y
214195 | S (S (S _)) = prim__sdivB64 x y
215196
216−public export partial
217−sdiv : Bits n -> Bits n -> Bits n
197+partial
198+sdiv : %static {n : Nat} -> Bits n -> Bits n -> Bits n
218199sdiv (MkBits x) (MkBits y) = MkBits (sdiv' x y)
219200
220201partial
221−public export
222−udiv' : machineTy (nextBytes n) -> machineTy (nextBytes n) -> machineTy (nextBytes n)
202+udiv' : %static {n : Nat} -> machineTy (nextBytes n) -> machineTy (nextBytes n) -> machineTy (nextBytes n)
223203udiv' {n=n} x y with (nextBytes n)
224204 | Z = prim__udivB8 x y
225205 | S Z = prim__udivB16 x y
226206 | S (S Z) = prim__udivB32 x y
227207 | S (S (S _)) = prim__udivB64 x y
228208
229−public export partial
230−udiv : Bits n -> Bits n -> Bits n
209+partial
210+udiv : %static {n : Nat} -> Bits n -> Bits n -> Bits n
231211udiv (MkBits x) (MkBits y) = MkBits (udiv' x y)
232212
233−public export partial
234−srem' : machineTy (nextBytes n) -> machineTy (nextBytes n) -> machineTy (nextBytes n)
213+partial
214+srem' : %static {n : Nat} -> machineTy (nextBytes n) -> machineTy (nextBytes n) -> machineTy (nextBytes n)
235215srem' {n=n} x y with (nextBytes n)
236216 | Z = prim__sremB8 x y
237217 | S Z = prim__sremB16 x y
238218 | S (S Z) = prim__sremB32 x y
239219 | S (S (S _)) = prim__sremB64 x y
240220
241−public export partial
242−srem : Bits n -> Bits n -> Bits n
221+partial
222+srem : %static {n : Nat} -> Bits n -> Bits n -> Bits n
243223srem (MkBits x) (MkBits y) = MkBits (srem' x y)
244224
245−public export partial
246−urem' : machineTy (nextBytes n) -> machineTy (nextBytes n) -> machineTy (nextBytes n)
225+partial
226+urem' : %static {n : Nat} -> machineTy (nextBytes n) -> machineTy (nextBytes n) -> machineTy (nextBytes n)
247227urem' {n=n} x y with (nextBytes n)
248228 | Z = prim__uremB8 x y
249229 | S Z = prim__uremB16 x y
250230 | S (S Z) = prim__uremB32 x y
251231 | S (S (S _)) = prim__uremB64 x y
252232
253−public export partial
254−urem : Bits n -> Bits n -> Bits n
233+partial
234+urem : %static {n : Nat} -> Bits n -> Bits n -> Bits n
255235urem (MkBits x) (MkBits y) = MkBits (urem' x y)
256236
257237-- TODO: Proofy comparisons via postulates
258−lt : machineTy (nextBytes n) -> machineTy (nextBytes n) -> Int
238+lt : %static {n : Nat} -> machineTy (nextBytes n) -> machineTy (nextBytes n) -> Int
259239lt {n=n} x y with (nextBytes n)
260240 | Z = prim__ltB8 x y
261241 | S Z = prim__ltB16 x y
262242 | S (S Z) = prim__ltB32 x y
263243 | S (S (S _)) = prim__ltB64 x y
264244
265−lte : machineTy (nextBytes n) -> machineTy (nextBytes n) -> Int
245+lte : %static {n : Nat} -> machineTy (nextBytes n) -> machineTy (nextBytes n) -> Int
266246lte {n=n} x y with (nextBytes n)
267247 | Z = prim__lteB8 x y
268248 | S Z = prim__lteB16 x y
269249 | S (S Z) = prim__lteB32 x y
270250 | S (S (S _)) = prim__lteB64 x y
271251
272−eq : machineTy (nextBytes n) -> machineTy (nextBytes n) -> Int
252+eq : %static {n : Nat} -> machineTy (nextBytes n) -> machineTy (nextBytes n) -> Int
273253eq {n=n} x y with (nextBytes n)
274254 | Z = prim__eqB8 x y
275255 | S Z = prim__eqB16 x y
276256 | S (S Z) = prim__eqB32 x y
277257 | S (S (S _)) = prim__eqB64 x y
278258
279−gte : machineTy (nextBytes n) -> machineTy (nextBytes n) -> Int
259+gte : %static {n : Nat} -> machineTy (nextBytes n) -> machineTy (nextBytes n) -> Int
280260gte {n=n} x y with (nextBytes n)
281261 | Z = prim__gteB8 x y
282262 | S Z = prim__gteB16 x y
283263 | S (S Z) = prim__gteB32 x y
284264 | S (S (S _)) = prim__gteB64 x y
285265
286−gt : machineTy (nextBytes n) -> machineTy (nextBytes n) -> Int
266+gt : %static {n : Nat} -> machineTy (nextBytes n) -> machineTy (nextBytes n) -> Int
287267gt {n=n} x y with (nextBytes n)
288268 | Z = prim__gtB8 x y
289269 | S Z = prim__gtB16 x y
290270 | S (S Z) = prim__gtB32 x y
291271 | S (S (S _)) = prim__gtB64 x y
292272
293−public export
294273implementation Eq (Bits n) where
295274 (MkBits x) == (MkBits y) = boolOp eq x y
296275
297−public export
298276implementation Ord (Bits n) where
299277 (MkBits x) < (MkBits y) = boolOp lt x y
300278 (MkBits x) <= (MkBits y) = boolOp lte x y
@@ -307,8 +285,7 @@ implementation Ord (Bits n) where
307285 then EQ
308286 else GT
309287
310−public export
311−complement' : machineTy (nextBytes n) -> machineTy (nextBytes n)
288+complement' : %static {n : Nat} -> machineTy (nextBytes n) -> machineTy (nextBytes n)
312289complement' {n=n} x with (nextBytes n)
313290 | Z = let pad = getPad {n=0} n in
314291 prim__complB8 (x `prim__shlB8` pad) `prim__lshrB8` pad
@@ -319,13 +296,12 @@ complement' {n=n} x with (nextBytes n)
319296 | S (S (S _)) = let pad = getPad {n=3} n in
320297 prim__complB64 (x `prim__shlB64` pad) `prim__lshrB64` pad
321298
322−public export
323−complement : Bits n -> Bits n
299+complement : %static {n : Nat} -> Bits n -> Bits n
324300complement (MkBits x) = MkBits (complement' x)
325301
326302-- TODO: Prove
327−public export %assert_total -- can't verify coverage of with block
328−zext' : machineTy (nextBytes n) -> machineTy (nextBytes (n+m))
303+%assert_total -- can't verify coverage of with block
304+zext' : %static {n : Nat} -> %static {m : Nat} -> machineTy (nextBytes n) -> machineTy (nextBytes (n+m))
329305zext' {n=n} {m=m} x with (nextBytes n, nextBytes (n+m))
330306 | (Z, Z) = believe_me x
331307 | (Z, S Z) = believe_me (prim__zextB8_B16 (believe_me x))
@@ -338,12 +314,11 @@ zext' {n=n} {m=m} x with (nextBytes n, nextBytes (n+m))
338314 | (S (S Z), S (S (S _))) = believe_me (prim__zextB32_B64 (believe_me x))
339315 | (S (S (S _)), S (S (S _))) = believe_me x
340316
341−public export
342−zeroExtend : Bits n -> Bits (n+m)
317+zeroExtend : %static {n : Nat} -> %static {m : Nat} -> Bits n -> Bits (n+m)
343318zeroExtend (MkBits x) = MkBits (zext' x)
344319
345−public export %assert_total
346−intToBits' : Integer -> machineTy (nextBytes n)
320+%assert_total
321+intToBits' : %static {n : Nat} -> Integer -> machineTy (nextBytes n)
347322intToBits' {n=n} x with (nextBytes n)
348323 | Z = let pad = getPad {n=0} n in
349324 prim__lshrB8 (prim__shlB8 (prim__truncBigInt_B8 x) pad) pad
@@ -354,28 +329,24 @@ intToBits' {n=n} x with (nextBytes n)
354329 | S (S (S _)) = let pad = getPad {n=3} n in
355330 prim__lshrB64 (prim__shlB64 (prim__truncBigInt_B64 x) pad) pad
356331
357−public export
358−intToBits : Integer -> Bits n
332+intToBits : %static {n : Nat} -> Integer -> Bits n
359333intToBits n = MkBits (intToBits' n)
360334
361335implementation Cast Integer (Bits n) where
362336 cast = intToBits
363337
364−public export
365−bitsToInt' : machineTy (nextBytes n) -> Integer
338+bitsToInt' : %static {n : Nat} -> machineTy (nextBytes n) -> Integer
366339bitsToInt' {n=n} x with (nextBytes n)
367340 | Z = prim__zextB8_BigInt x
368341 | S Z = prim__zextB16_BigInt x
369342 | S (S Z) = prim__zextB32_BigInt x
370343 | S (S (S _)) = prim__zextB64_BigInt x
371344
372−public export
373−bitsToInt : Bits n -> Integer
345+bitsToInt : %static {n : Nat} -> Bits n -> Integer
374346bitsToInt (MkBits x) = bitsToInt' x
375347
376348-- Zero out the high bits of a truncated bitstring
377−public export
378−zeroUnused : machineTy (nextBytes n) -> machineTy (nextBytes n)
349+zeroUnused : %static {n : Nat} -> machineTy (nextBytes n) -> machineTy (nextBytes n)
379350zeroUnused {n} x = x `and'` complement' (intToBits' {n=n} 0)
380351
381352--implementation Cast Nat (Bits n) where
@@ -383,7 +354,7 @@ zeroUnused {n} x = x `and'` complement' (intToBits' {n=n} 0)
383354
384355-- TODO: Prove
385356%assert_total -- can't verify coverage of with block
386−sext' : machineTy (nextBytes n) -> machineTy (nextBytes (n+m))
357+sext' : %static {n : Nat} -> machineTy (nextBytes n) -> machineTy (nextBytes (n+m))
387358sext' {n=n} {m=m} x with (nextBytes n, nextBytes (n+m))
388359 | (Z, Z) = let pad = getPad {n=0} n in
389360 believe_me (prim__ashrB8 (prim__shlB8 (believe_me x) pad) pad)
@@ -412,13 +383,12 @@ sext' {n=n} {m=m} x with (nextBytes n, nextBytes (n+m))
412383 | (S (S (S _)), S (S (S _))) = let pad = getPad {n=3} n in
413384 believe_me (prim__ashrB64 (prim__shlB64 (believe_me x) pad) pad)
414385
415−--public export
416−--signExtend : Bits n -> Bits (n+m)
386+----signExtend : Bits n -> Bits (n+m)
417387--signExtend {m=m} (MkBits x) = MkBits (zeroUnused (sext' x))
418388
419389-- TODO: Prove
420−public export %assert_total -- can't verify coverage of with block
421−trunc' : machineTy (nextBytes (m+n)) -> machineTy (nextBytes n)
390+%assert_total -- can't verify coverage of with block
391+trunc' : %static {m : Nat} -> %static {n : Nat} -> machineTy (nextBytes (m+n)) -> machineTy (nextBytes n)
422392trunc' {m=m} {n=n} x with (nextBytes n, nextBytes (m+n))
423393 | (Z, Z) = believe_me x
424394 | (Z, S Z) = believe_me (prim__truncB16_B8 (believe_me x))
@@ -431,31 +401,26 @@ trunc' {m=m} {n=n} x with (nextBytes n, nextBytes (m+n))
431401 | (S (S Z), S (S (S _))) = believe_me (prim__truncB64_B32 (believe_me x))
432402 | (S (S (S _)), S (S (S _))) = believe_me x
433403
434−public export
435−truncate : Bits (m+n) -> Bits n
404+truncate : %static {m : Nat} -> %static {n : Nat} -> Bits (m+n) -> Bits n
436405truncate (MkBits x) = MkBits (zeroUnused (trunc' x))
437406
438−public export
439−bitAt : Fin n -> Bits n
407+bitAt : %static {n : Nat} -> Fin n -> Bits n
440408bitAt n = intToBits 1 `shiftLeft` intToBits (cast n)
441409
442−public export
443−getBit : Fin n -> Bits n -> Bool
410+getBit : %static {n : Nat} -> Fin n -> Bits n -> Bool
444411getBit n x = (x `and` (bitAt n)) /= intToBits 0
445412
446−public export
447−setBit : Fin n -> Bits n -> Bits n
413+setBit : %static {n : Nat} -> Fin n -> Bits n -> Bits n
448414setBit n x = x `or` (bitAt n)
449415
450−public export
451−unsetBit : Fin n -> Bits n -> Bits n
416+unsetBit : %static {n : Nat} -> Fin n -> Bits n -> Bits n
452417unsetBit n x = x `and` complement (bitAt n)
453418
454−bitsToStr : Bits n -> String
419+bitsToStr : %static {n : Nat} -> Bits n -> String
455420bitsToStr x = pack (helper last x)
456421 where
457422 %assert_total
458− helper : Fin (S n) -> Bits n -> List Char
423+ helper : %static {n : Nat} -> Fin (S n) -> Bits n -> List Char
459424 helper FZ _ = []
460425 helper (FS x) b = (if getBit x b then '1' else '0') :: helper (weaken x) b
461426