@@ -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' : [static] {n : Nat} -> 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 : [static] {n : Nat} -> 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 : [static] {n : Nat} -> Nat -> machineTy n
48+getPad : %static {n : Nat} -> Nat -> machineTy n
4849getPad n = natToBits (minus (bitsUsed (nextBytes n)) n)
4950
5051public export
@@ -92,81 +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' : [static] {n : Nat} -> 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 : [static] {n : Nat} -> 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' : [static] {n : Nat} -> 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 : [static] {n : Nat} -> 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' : [static] {n : Nat} -> 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 : [static] {n : Nat} -> 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' : [static] {n : Nat} -> 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 : [static] {n : Nat} -> 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−or' : [static] {n : Nat} -> machineTy n -> machineTy n -> machineTy n
139+or' : %static {n : Nat} -> machineTy n -> machineTy n -> machineTy n
148140or' {n=n} x y with (n)
149141 | Z = prim__orB8 x y
150142 | S Z = prim__orB16 x y
151143 | S (S Z) = prim__orB32 x y
152144 | S (S (S _)) = prim__orB64 x y
153145
154−public export
155−or : [static] {n : Nat} -> Bits n -> Bits n -> Bits n
146+or : %static {n : Nat} -> Bits n -> Bits n -> Bits n
156147or {n} (MkBits x) (MkBits y) = MkBits (or' {n=nextBytes n} x y)
157148
158−xor' : [static] {n : Nat} -> machineTy n -> machineTy n -> machineTy n
149+xor' : %static {n : Nat} -> machineTy n -> machineTy n -> machineTy n
159150xor' {n=n} x y with (n)
160151 | Z = prim__xorB8 x y
161152 | S Z = prim__xorB16 x y
162153 | S (S Z) = prim__xorB32 x y
163154 | S (S (S _)) = prim__xorB64 x y
164155
165−public export
166−xor : [static] {n : Nat} -> Bits n -> Bits n -> Bits n
156+xor : %static {n : Nat} -> Bits n -> Bits n -> Bits n
167157xor {n} (MkBits x) (MkBits y) = MkBits {n} (xor' {n=nextBytes n} x y)
168158
169−public export
170159plus' : machineTy (nextBytes n) -> machineTy (nextBytes n) -> machineTy (nextBytes n)
171160plus' {n=n} x y with (nextBytes n)
172161 | Z = pad8 n prim__addB8 x y
@@ -174,11 +163,9 @@ plus' {n=n} x y with (nextBytes n)
174163 | S (S Z) = pad32 n prim__addB32 x y
175164 | S (S (S _)) = pad64 n prim__addB64 x y
176165
177−public export
178−plus : [static] {n : Nat} -> Bits n -> Bits n -> Bits n
166+plus : %static {n : Nat} -> Bits n -> Bits n -> Bits n
179167plus (MkBits x) (MkBits y) = MkBits (plus' x y)
180168
181−public export
182169minus' : machineTy (nextBytes n) -> machineTy (nextBytes n) -> machineTy (nextBytes n)
183170minus' {n=n} x y with (nextBytes n)
184171 | Z = pad8 n prim__subB8 x y
@@ -186,11 +173,9 @@ minus' {n=n} x y with (nextBytes n)
186173 | S (S Z) = pad32 n prim__subB32 x y
187174 | S (S (S _)) = pad64 n prim__subB64 x y
188175
189−public export
190−minus : [static] {n : Nat} -> Bits n -> Bits n -> Bits n
176+minus : %static {n : Nat} -> Bits n -> Bits n -> Bits n
191177minus (MkBits x) (MkBits y) = MkBits (minus' x y)
192178
193−public export
194179times' : machineTy (nextBytes n) -> machineTy (nextBytes n) -> machineTy (nextBytes n)
195180times' {n=n} x y with (nextBytes n)
196181 | Z = pad8 n prim__mulB8 x y
@@ -198,12 +183,10 @@ times' {n=n} x y with (nextBytes n)
198183 | S (S Z) = pad32 n prim__mulB32 x y
199184 | S (S (S _)) = pad64 n prim__mulB64 x y
200185
201−public export
202−times : [static] {n : Nat} -> Bits n -> Bits n -> Bits n
186+times : %static {n : Nat} -> Bits n -> Bits n -> Bits n
203187times (MkBits x) (MkBits y) = MkBits (times' x y)
204188
205189partial
206−public export
207190sdiv' : machineTy (nextBytes n) -> machineTy (nextBytes n) -> machineTy (nextBytes n)
208191sdiv' {n=n} x y with (nextBytes n)
209192 | Z = prim__sdivB8 x y
@@ -211,88 +194,85 @@ sdiv' {n=n} x y with (nextBytes n)
211194 | S (S Z) = prim__sdivB32 x y
212195 | S (S (S _)) = prim__sdivB64 x y
213196
214−public export partial
215−sdiv : [static] {n : Nat} -> Bits n -> Bits n -> Bits n
197+partial
198+sdiv : %static {n : Nat} -> Bits n -> Bits n -> Bits n
216199sdiv (MkBits x) (MkBits y) = MkBits (sdiv' x y)
217200
218201partial
219−public export
220−udiv' : [static] {n : Nat} -> machineTy (nextBytes n) -> machineTy (nextBytes n) -> machineTy (nextBytes n)
202+udiv' : %static {n : Nat} -> machineTy (nextBytes n) -> machineTy (nextBytes n) -> machineTy (nextBytes n)
221203udiv' {n=n} x y with (nextBytes n)
222204 | Z = prim__udivB8 x y
223205 | S Z = prim__udivB16 x y
224206 | S (S Z) = prim__udivB32 x y
225207 | S (S (S _)) = prim__udivB64 x y
226208
227−public export partial
228−udiv : [static] {n : Nat} -> Bits n -> Bits n -> Bits n
209+partial
210+udiv : %static {n : Nat} -> Bits n -> Bits n -> Bits n
229211udiv (MkBits x) (MkBits y) = MkBits (udiv' x y)
230212
231−public export partial
232−srem' : [static] {n : Nat} -> 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)
233215srem' {n=n} x y with (nextBytes n)
234216 | Z = prim__sremB8 x y
235217 | S Z = prim__sremB16 x y
236218 | S (S Z) = prim__sremB32 x y
237219 | S (S (S _)) = prim__sremB64 x y
238220
239−public export partial
240−srem : [static] {n : Nat} -> Bits n -> Bits n -> Bits n
221+partial
222+srem : %static {n : Nat} -> Bits n -> Bits n -> Bits n
241223srem (MkBits x) (MkBits y) = MkBits (srem' x y)
242224
243−public export partial
244−urem' : [static] {n : Nat} -> 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)
245227urem' {n=n} x y with (nextBytes n)
246228 | Z = prim__uremB8 x y
247229 | S Z = prim__uremB16 x y
248230 | S (S Z) = prim__uremB32 x y
249231 | S (S (S _)) = prim__uremB64 x y
250232
251−public export partial
252−urem : [static] {n : Nat} -> Bits n -> Bits n -> Bits n
233+partial
234+urem : %static {n : Nat} -> Bits n -> Bits n -> Bits n
253235urem (MkBits x) (MkBits y) = MkBits (urem' x y)
254236
255237-- TODO: Proofy comparisons via postulates
256−lt : [static] {n : Nat} -> machineTy (nextBytes n) -> machineTy (nextBytes n) -> Int
238+lt : %static {n : Nat} -> machineTy (nextBytes n) -> machineTy (nextBytes n) -> Int
257239lt {n=n} x y with (nextBytes n)
258240 | Z = prim__ltB8 x y
259241 | S Z = prim__ltB16 x y
260242 | S (S Z) = prim__ltB32 x y
261243 | S (S (S _)) = prim__ltB64 x y
262244
263−lte : [static] {n : Nat} -> machineTy (nextBytes n) -> machineTy (nextBytes n) -> Int
245+lte : %static {n : Nat} -> machineTy (nextBytes n) -> machineTy (nextBytes n) -> Int
264246lte {n=n} x y with (nextBytes n)
265247 | Z = prim__lteB8 x y
266248 | S Z = prim__lteB16 x y
267249 | S (S Z) = prim__lteB32 x y
268250 | S (S (S _)) = prim__lteB64 x y
269251
270−eq : [static] {n : Nat} -> machineTy (nextBytes n) -> machineTy (nextBytes n) -> Int
252+eq : %static {n : Nat} -> machineTy (nextBytes n) -> machineTy (nextBytes n) -> Int
271253eq {n=n} x y with (nextBytes n)
272254 | Z = prim__eqB8 x y
273255 | S Z = prim__eqB16 x y
274256 | S (S Z) = prim__eqB32 x y
275257 | S (S (S _)) = prim__eqB64 x y
276258
277−gte : [static] {n : Nat} -> machineTy (nextBytes n) -> machineTy (nextBytes n) -> Int
259+gte : %static {n : Nat} -> machineTy (nextBytes n) -> machineTy (nextBytes n) -> Int
278260gte {n=n} x y with (nextBytes n)
279261 | Z = prim__gteB8 x y
280262 | S Z = prim__gteB16 x y
281263 | S (S Z) = prim__gteB32 x y
282264 | S (S (S _)) = prim__gteB64 x y
283265
284−gt : [static] {n : Nat} -> machineTy (nextBytes n) -> machineTy (nextBytes n) -> Int
266+gt : %static {n : Nat} -> machineTy (nextBytes n) -> machineTy (nextBytes n) -> Int
285267gt {n=n} x y with (nextBytes n)
286268 | Z = prim__gtB8 x y
287269 | S Z = prim__gtB16 x y
288270 | S (S Z) = prim__gtB32 x y
289271 | S (S (S _)) = prim__gtB64 x y
290272
291−public export
292273implementation Eq (Bits n) where
293274 (MkBits x) == (MkBits y) = boolOp eq x y
294275
295−public export
296276implementation Ord (Bits n) where
297277 (MkBits x) < (MkBits y) = boolOp lt x y
298278 (MkBits x) <= (MkBits y) = boolOp lte x y
@@ -305,8 +285,7 @@ implementation Ord (Bits n) where
305285 then EQ
306286 else GT
307287
308−public export
309−complement' : [static] {n : Nat} -> machineTy (nextBytes n) -> machineTy (nextBytes n)
288+complement' : %static {n : Nat} -> machineTy (nextBytes n) -> machineTy (nextBytes n)
310289complement' {n=n} x with (nextBytes n)
311290 | Z = let pad = getPad {n=0} n in
312291 prim__complB8 (x `prim__shlB8` pad) `prim__lshrB8` pad
@@ -317,13 +296,12 @@ complement' {n=n} x with (nextBytes n)
317296 | S (S (S _)) = let pad = getPad {n=3} n in
318297 prim__complB64 (x `prim__shlB64` pad) `prim__lshrB64` pad
319298
320−public export
321−complement : [static] {n : Nat} -> Bits n -> Bits n
299+complement : %static {n : Nat} -> Bits n -> Bits n
322300complement (MkBits x) = MkBits (complement' x)
323301
324302-- TODO: Prove
325303%assert_total -- can't verify coverage of with block
326−zext' : [static] {n : Nat} -> [static] {m : Nat} -> machineTy (nextBytes n) -> machineTy (nextBytes (n+m))
304+zext' : %static {n : Nat} -> %static {m : Nat} -> machineTy (nextBytes n) -> machineTy (nextBytes (n+m))
327305zext' {n=n} {m=m} x with (nextBytes n, nextBytes (n+m))
328306 | (Z, Z) = believe_me x
329307 | (Z, S Z) = believe_me (prim__zextB8_B16 (believe_me x))
@@ -336,14 +314,11 @@ zext' {n=n} {m=m} x with (nextBytes n, nextBytes (n+m))
336314 | (S (S Z), S (S (S _))) = believe_me (prim__zextB32_B64 (believe_me x))
337315 | (S (S (S _)), S (S (S _))) = believe_me x
338316
339−public export
340−zeroExtend : [static] {n : Nat} -> [static] {m : Nat} -> Bits n -> Bits (n+m)
317+zeroExtend : %static {n : Nat} -> %static {m : Nat} -> Bits n -> Bits (n+m)
341318zeroExtend (MkBits x) = MkBits (zext' x)
342319
343−public export
344320%assert_total
345−intToBits' : [static] {n : Nat} -> Integer -> machineTy (nextBytes n)
346−intToBits' : Integer -> machineTy (nextBytes n)
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,27 +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 : [static] {n : Nat} -> 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' : [static] {n : Nat} -> 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 : [static] {n : Nat} -> 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−zeroUnused : [static] {n : Nat} -> machineTy (nextBytes n) -> machineTy (nextBytes n)
349+zeroUnused : %static {n : Nat} -> machineTy (nextBytes n) -> machineTy (nextBytes n)
378350zeroUnused {n} x = x `and'` complement' (intToBits' {n=n} 0)
379351
380352--implementation Cast Nat (Bits n) where
@@ -382,7 +354,7 @@ zeroUnused {n} x = x `and'` complement' (intToBits' {n=n} 0)
382354
383355-- TODO: Prove
384356%assert_total -- can't verify coverage of with block
385−sext' : [static] {n : Nat} -> machineTy (nextBytes n) -> machineTy (nextBytes (n+m))
357+sext' : %static {n : Nat} -> machineTy (nextBytes n) -> machineTy (nextBytes (n+m))
386358sext' {n=n} {m=m} x with (nextBytes n, nextBytes (n+m))
387359 | (Z, Z) = let pad = getPad {n=0} n in
388360 believe_me (prim__ashrB8 (prim__shlB8 (believe_me x) pad) pad)
@@ -411,14 +383,12 @@ sext' {n=n} {m=m} x with (nextBytes n, nextBytes (n+m))
411383 | (S (S (S _)), S (S (S _))) = let pad = getPad {n=3} n in
412384 believe_me (prim__ashrB64 (prim__shlB64 (believe_me x) pad) pad)
413385
414−--public export
415−--signExtend : Bits n -> Bits (n+m)
386+----signExtend : Bits n -> Bits (n+m)
416387--signExtend {m=m} (MkBits x) = MkBits (zeroUnused (sext' x))
417388
418389-- TODO: Prove
419−public export
420390%assert_total -- can't verify coverage of with block
421−trunc' : [static] {m : Nat} -> [static] {n : Nat} -> machineTy (nextBytes (m+n)) -> machineTy (nextBytes n)
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 : [static] {m : Nat} -> [static] {n : Nat} -> 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 : [static] {n : Nat} -> 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 : [static] {n : Nat} -> 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 : [static] {n : Nat} -> 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 : [static] {n : Nat} -> 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 : [static] {n : Nat} -> Bits n -> String
419+bitsToStr : %static {n : Nat} -> Bits n -> String
455420bitsToStr x = pack (helper last x)
456421 where
457422 %assert_total
458− helper : [static] {n : Nat} -> 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