@@ -28,7 +28,7 @@ bitsUsed : Nat -> Nat
2828bitsUsed n = 8 * (2 `power` n)
2929
3030%assert_total
31−natToBits' : machineTy n -> Nat -> machineTy n
31+natToBits' : [static] {n : Nat} -> machineTy n -> Nat -> machineTy n
3232natToBits' a Z = a
3333natToBits' {n=n} a x with (n)
3434 -- it seems I have to manually recover the value of n here, instead of being able to reference it
@@ -37,14 +37,14 @@ natToBits' {n=n} a x with (n)
3737 natToBits' a (S x') | S (S Z) = natToBits' {n=2} (prim__addB32 a (prim__truncInt_B32 1)) x'
3838 natToBits' a (S x') | S (S (S _)) = natToBits' {n=3} (prim__addB64 a (prim__truncInt_B64 1)) x'
3939
40−natToBits : Nat -> machineTy n
40+natToBits : [static] {n : Nat} -> Nat -> machineTy n
4141natToBits {n=n} x with (n)
4242 | Z = natToBits' {n=0} (prim__truncInt_B8 0) x
4343 | S Z = natToBits' {n=1} (prim__truncInt_B16 0) x
4444 | S (S Z) = natToBits' {n=2} (prim__truncInt_B32 0) x
4545 | S (S (S _)) = natToBits' {n=3} (prim__truncInt_B64 0) x
4646
47−getPad : Nat -> machineTy n
47+getPad : [static] {n : Nat} -> Nat -> machineTy n
4848getPad n = natToBits (minus (bitsUsed (nextBytes n)) n)
4949
5050public
@@ -92,7 +92,7 @@ pad64' n f x y = prim__lshrB64 (f (prim__shlB64 x pad) y) pad
9292 where
9393 pad = getPad {n=3} n
9494
95−shiftLeft' : machineTy (nextBytes n) -> machineTy (nextBytes n) -> machineTy (nextBytes n)
95+shiftLeft' : [static] {n : Nat} -> machineTy (nextBytes n) -> machineTy (nextBytes n) -> machineTy (nextBytes n)
9696shiftLeft' {n=n} x c with (nextBytes n)
9797 | Z = pad8' n prim__shlB8 x c
9898 | S Z = pad16' n prim__shlB16 x c
@@ -100,10 +100,10 @@ shiftLeft' {n=n} x c with (nextBytes n)
100100 | S (S (S _)) = pad64' n prim__shlB64 x c
101101
102102public
103−shiftLeft : Bits n -> Bits n -> Bits n
103+shiftLeft : [static] {n : Nat} -> Bits n -> Bits n -> Bits n
104104shiftLeft (MkBits x) (MkBits y) = MkBits (shiftLeft' x y)
105105
106−shiftRightLogical' : machineTy n -> machineTy n -> machineTy n
106+shiftRightLogical' : [static] {n : Nat} -> machineTy n -> machineTy n -> machineTy n
107107shiftRightLogical' {n=n} x c with (n)
108108 | Z = prim__lshrB8 x c
109109 | S Z = prim__lshrB16 x c
@@ -111,11 +111,11 @@ shiftRightLogical' {n=n} x c with (n)
111111 | S (S (S _)) = prim__lshrB64 x c
112112
113113public
114−shiftRightLogical : Bits n -> Bits n -> Bits n
114+shiftRightLogical : [static] {n : Nat} -> Bits n -> Bits n -> Bits n
115115shiftRightLogical {n} (MkBits x) (MkBits y)
116116 = MkBits {n} (shiftRightLogical' {n=nextBytes n} x y)
117117
118−shiftRightArithmetic' : machineTy (nextBytes n) -> machineTy (nextBytes n) -> machineTy (nextBytes n)
118+shiftRightArithmetic' : [static] {n : Nat} -> machineTy (nextBytes n) -> machineTy (nextBytes n) -> machineTy (nextBytes n)
119119shiftRightArithmetic' {n=n} x c with (nextBytes n)
120120 | Z = pad8' n prim__ashrB8 x c
121121 | S Z = pad16' n prim__ashrB16 x c
@@ -123,10 +123,10 @@ shiftRightArithmetic' {n=n} x c with (nextBytes n)
123123 | S (S (S _)) = pad64' n prim__ashrB64 x c
124124
125125public
126−shiftRightArithmetic : Bits n -> Bits n -> Bits n
126+shiftRightArithmetic : [static] {n : Nat} -> Bits n -> Bits n -> Bits n
127127shiftRightArithmetic (MkBits x) (MkBits y) = MkBits (shiftRightArithmetic' x y)
128128
129−and' : machineTy n -> machineTy n -> machineTy n
129+and' : [static] {n : Nat} -> machineTy n -> machineTy n -> machineTy n
130130and' {n=n} x y with (n)
131131 | Z = prim__andB8 x y
132132 | S Z = prim__andB16 x y
@@ -134,10 +134,10 @@ and' {n=n} x y with (n)
134134 | S (S (S _)) = prim__andB64 x y
135135
136136public
137−and : Bits n -> Bits n -> Bits n
137+and : [static] {n : Nat} -> Bits n -> Bits n -> Bits n
138138and {n} (MkBits x) (MkBits y) = MkBits (and' {n=nextBytes n} x y)
139139
140−or' : machineTy n -> machineTy n -> machineTy n
140+or' : [static] {n : Nat} -> machineTy n -> machineTy n -> machineTy n
141141or' {n=n} x y with (n)
142142 | Z = prim__orB8 x y
143143 | S Z = prim__orB16 x y
@@ -145,10 +145,10 @@ or' {n=n} x y with (n)
145145 | S (S (S _)) = prim__orB64 x y
146146
147147public
148−or : Bits n -> Bits n -> Bits n
148+or : [static] {n : Nat} -> Bits n -> Bits n -> Bits n
149149or {n} (MkBits x) (MkBits y) = MkBits (or' {n=nextBytes n} x y)
150150
151−xor' : machineTy n -> machineTy n -> machineTy n
151+xor' : [static] {n : Nat} -> machineTy n -> machineTy n -> machineTy n
152152xor' {n=n} x y with (n)
153153 | Z = prim__xorB8 x y
154154 | S Z = prim__xorB16 x y
@@ -156,7 +156,7 @@ xor' {n=n} x y with (n)
156156 | S (S (S _)) = prim__xorB64 x y
157157
158158public
159−xor : Bits n -> Bits n -> Bits n
159+xor : [static] {n : Nat} -> Bits n -> Bits n -> Bits n
160160xor {n} (MkBits x) (MkBits y) = MkBits {n} (xor' {n=nextBytes n} x y)
161161
162162plus' : machineTy (nextBytes n) -> machineTy (nextBytes n) -> machineTy (nextBytes n)
@@ -167,7 +167,7 @@ plus' {n=n} x y with (nextBytes n)
167167 | S (S (S _)) = pad64 n prim__addB64 x y
168168
169169public
170−plus : Bits n -> Bits n -> Bits n
170+plus : [static] {n : Nat} -> Bits n -> Bits n -> Bits n
171171plus (MkBits x) (MkBits y) = MkBits (plus' x y)
172172
173173minus' : machineTy (nextBytes n) -> machineTy (nextBytes n) -> machineTy (nextBytes n)
@@ -178,7 +178,7 @@ minus' {n=n} x y with (nextBytes n)
178178 | S (S (S _)) = pad64 n prim__subB64 x y
179179
180180public
181−minus : Bits n -> Bits n -> Bits n
181+minus : [static] {n : Nat} -> Bits n -> Bits n -> Bits n
182182minus (MkBits x) (MkBits y) = MkBits (minus' x y)
183183
184184times' : machineTy (nextBytes n) -> machineTy (nextBytes n) -> machineTy (nextBytes n)
@@ -189,7 +189,7 @@ times' {n=n} x y with (nextBytes n)
189189 | S (S (S _)) = pad64 n prim__mulB64 x y
190190
191191public
192−times : Bits n -> Bits n -> Bits n
192+times : [static] {n : Nat} -> Bits n -> Bits n -> Bits n
193193times (MkBits x) (MkBits y) = MkBits (times' x y)
194194
195195partial
@@ -201,7 +201,7 @@ sdiv' {n=n} x y with (nextBytes n)
201201 | S (S (S _)) = prim__sdivB64 x y
202202
203203public partial
204−sdiv : Bits n -> Bits n -> Bits n
204+sdiv : [static] {n : Nat} -> Bits n -> Bits n -> Bits n
205205sdiv (MkBits x) (MkBits y) = MkBits (sdiv' x y)
206206
207207partial
@@ -213,11 +213,11 @@ udiv' {n=n} x y with (nextBytes n)
213213 | S (S (S _)) = prim__udivB64 x y
214214
215215public partial
216−udiv : Bits n -> Bits n -> Bits n
216+udiv : [static] {n : Nat} -> Bits n -> Bits n -> Bits n
217217udiv (MkBits x) (MkBits y) = MkBits (udiv' x y)
218218
219219partial
220−srem' : machineTy (nextBytes n) -> machineTy (nextBytes n) -> machineTy (nextBytes n)
220+srem' : [static] {n : Nat} -> machineTy (nextBytes n) -> machineTy (nextBytes n) -> machineTy (nextBytes n)
221221srem' {n=n} x y with (nextBytes n)
222222 | Z = prim__sremB8 x y
223223 | S Z = prim__sremB16 x y
@@ -225,11 +225,11 @@ srem' {n=n} x y with (nextBytes n)
225225 | S (S (S _)) = prim__sremB64 x y
226226
227227public partial
228−srem : Bits n -> Bits n -> Bits n
228+srem : [static] {n : Nat} -> Bits n -> Bits n -> Bits n
229229srem (MkBits x) (MkBits y) = MkBits (srem' x y)
230230
231231partial
232−urem' : machineTy (nextBytes n) -> machineTy (nextBytes n) -> machineTy (nextBytes n)
232+urem' : [static] {n : Nat} -> machineTy (nextBytes n) -> machineTy (nextBytes n) -> machineTy (nextBytes n)
233233urem' {n=n} x y with (nextBytes n)
234234 | Z = prim__uremB8 x y
235235 | S Z = prim__uremB16 x y
@@ -237,39 +237,39 @@ urem' {n=n} x y with (nextBytes n)
237237 | S (S (S _)) = prim__uremB64 x y
238238
239239public partial
240−urem : Bits n -> Bits n -> Bits n
240+urem : [static] {n : Nat} -> Bits n -> Bits n -> Bits n
241241urem (MkBits x) (MkBits y) = MkBits (urem' x y)
242242
243243-- TODO: Proofy comparisons via postulates
244−lt : machineTy (nextBytes n) -> machineTy (nextBytes n) -> Int
244+lt : [static] {n : Nat} -> machineTy (nextBytes n) -> machineTy (nextBytes n) -> Int
245245lt {n=n} x y with (nextBytes n)
246246 | Z = prim__ltB8 x y
247247 | S Z = prim__ltB16 x y
248248 | S (S Z) = prim__ltB32 x y
249249 | S (S (S _)) = prim__ltB64 x y
250250
251−lte : machineTy (nextBytes n) -> machineTy (nextBytes n) -> Int
251+lte : [static] {n : Nat} -> machineTy (nextBytes n) -> machineTy (nextBytes n) -> Int
252252lte {n=n} x y with (nextBytes n)
253253 | Z = prim__lteB8 x y
254254 | S Z = prim__lteB16 x y
255255 | S (S Z) = prim__lteB32 x y
256256 | S (S (S _)) = prim__lteB64 x y
257257
258−eq : machineTy (nextBytes n) -> machineTy (nextBytes n) -> Int
258+eq : [static] {n : Nat} -> machineTy (nextBytes n) -> machineTy (nextBytes n) -> Int
259259eq {n=n} x y with (nextBytes n)
260260 | Z = prim__eqB8 x y
261261 | S Z = prim__eqB16 x y
262262 | S (S Z) = prim__eqB32 x y
263263 | S (S (S _)) = prim__eqB64 x y
264264
265−gte : machineTy (nextBytes n) -> machineTy (nextBytes n) -> Int
265+gte : [static] {n : Nat} -> machineTy (nextBytes n) -> machineTy (nextBytes n) -> Int
266266gte {n=n} x y with (nextBytes n)
267267 | Z = prim__gteB8 x y
268268 | S Z = prim__gteB16 x y
269269 | S (S Z) = prim__gteB32 x y
270270 | S (S (S _)) = prim__gteB64 x y
271271
272−gt : machineTy (nextBytes n) -> machineTy (nextBytes n) -> Int
272+gt : [static] {n : Nat} -> machineTy (nextBytes n) -> machineTy (nextBytes n) -> Int
273273gt {n=n} x y with (nextBytes n)
274274 | Z = prim__gtB8 x y
275275 | S Z = prim__gtB16 x y
@@ -291,7 +291,7 @@ implementation Ord (Bits n) where
291291 then EQ
292292 else GT
293293
294−complement' : machineTy (nextBytes n) -> machineTy (nextBytes n)
294+complement' : [static] {n : Nat} -> machineTy (nextBytes n) -> machineTy (nextBytes n)
295295complement' {n=n} x with (nextBytes n)
296296 | Z = let pad = getPad {n=0} n in
297297 prim__complB8 (x `prim__shlB8` pad) `prim__lshrB8` pad
@@ -303,12 +303,12 @@ complement' {n=n} x with (nextBytes n)
303303 prim__complB64 (x `prim__shlB64` pad) `prim__lshrB64` pad
304304
305305public
306−complement : Bits n -> Bits n
306+complement : [static] {n : Nat} -> Bits n -> Bits n
307307complement (MkBits x) = MkBits (complement' x)
308308
309309-- TODO: Prove
310310%assert_total -- can't verify coverage of with block
311−zext' : machineTy (nextBytes n) -> machineTy (nextBytes (n+m))
311+zext' : [static] {n : Nat} -> [static] {m : Nat} -> machineTy (nextBytes n) -> machineTy (nextBytes (n+m))
312312zext' {n=n} {m=m} x with (nextBytes n, nextBytes (n+m))
313313 | (Z, Z) = believe_me x
314314 | (Z, S Z) = believe_me (prim__zextB8_B16 (believe_me x))
@@ -322,11 +322,11 @@ zext' {n=n} {m=m} x with (nextBytes n, nextBytes (n+m))
322322 | (S (S (S _)), S (S (S _))) = believe_me x
323323
324324public
325−zeroExtend : Bits n -> Bits (n+m)
325+zeroExtend : [static] {n : Nat} -> [static] {m : Nat} -> Bits n -> Bits (n+m)
326326zeroExtend (MkBits x) = MkBits (zext' x)
327327
328328%assert_total
329−intToBits' : Integer -> machineTy (nextBytes n)
329+intToBits' : [static] {n : Nat} -> Integer -> machineTy (nextBytes n)
330330intToBits' {n=n} x with (nextBytes n)
331331 | Z = let pad = getPad {n=0} n in
332332 prim__lshrB8 (prim__shlB8 (prim__truncBigInt_B8 x) pad) pad
@@ -338,13 +338,13 @@ intToBits' {n=n} x with (nextBytes n)
338338 prim__lshrB64 (prim__shlB64 (prim__truncBigInt_B64 x) pad) pad
339339
340340public
341−intToBits : Integer -> Bits n
341+intToBits : [static] {n : Nat} -> Integer -> Bits n
342342intToBits n = MkBits (intToBits' n)
343343
344344implementation Cast Integer (Bits n) where
345345 cast = intToBits
346346
347−bitsToInt' : machineTy (nextBytes n) -> Integer
347+bitsToInt' : [static] {n : Nat} -> machineTy (nextBytes n) -> Integer
348348bitsToInt' {n=n} x with (nextBytes n)
349349 | Z = prim__zextB8_BigInt x
350350 | S Z = prim__zextB16_BigInt x
@@ -352,11 +352,11 @@ bitsToInt' {n=n} x with (nextBytes n)
352352 | S (S (S _)) = prim__zextB64_BigInt x
353353
354354public
355−bitsToInt : Bits n -> Integer
355+bitsToInt : [static] {n : Nat} -> Bits n -> Integer
356356bitsToInt (MkBits x) = bitsToInt' x
357357
358358-- Zero out the high bits of a truncated bitstring
359−zeroUnused : machineTy (nextBytes n) -> machineTy (nextBytes n)
359+zeroUnused : [static] {n : Nat} -> machineTy (nextBytes n) -> machineTy (nextBytes n)
360360zeroUnused {n} x = x `and'` complement' (intToBits' {n=n} 0)
361361
362362--implementation Cast Nat (Bits n) where
@@ -364,7 +364,7 @@ zeroUnused {n} x = x `and'` complement' (intToBits' {n=n} 0)
364364
365365-- TODO: Prove
366366%assert_total -- can't verify coverage of with block
367−sext' : machineTy (nextBytes n) -> machineTy (nextBytes (n+m))
367+sext' : [static] {n : Nat} -> machineTy (nextBytes n) -> machineTy (nextBytes (n+m))
368368sext' {n=n} {m=m} x with (nextBytes n, nextBytes (n+m))
369369 | (Z, Z) = let pad = getPad {n=0} n in
370370 believe_me (prim__ashrB8 (prim__shlB8 (believe_me x) pad) pad)
@@ -399,7 +399,7 @@ sext' {n=n} {m=m} x with (nextBytes n, nextBytes (n+m))
399399
400400-- TODO: Prove
401401%assert_total -- can't verify coverage of with block
402−trunc' : machineTy (nextBytes (m+n)) -> machineTy (nextBytes n)
402+trunc' : [static] {m : Nat} -> [static] {n : Nat} -> machineTy (nextBytes (m+n)) -> machineTy (nextBytes n)
403403trunc' {m=m} {n=n} x with (nextBytes n, nextBytes (m+n))
404404 | (Z, Z) = believe_me x
405405 | (Z, S Z) = believe_me (prim__truncB16_B8 (believe_me x))
@@ -413,30 +413,30 @@ trunc' {m=m} {n=n} x with (nextBytes n, nextBytes (m+n))
413413 | (S (S (S _)), S (S (S _))) = believe_me x
414414
415415public
416−truncate : Bits (m+n) -> Bits n
416+truncate : [static] {m : Nat} -> [static] {n : Nat} -> Bits (m+n) -> Bits n
417417truncate (MkBits x) = MkBits (zeroUnused (trunc' x))
418418
419419public
420−bitAt : Fin n -> Bits n
420+bitAt : [static] {n : Nat} -> Fin n -> Bits n
421421bitAt n = intToBits 1 `shiftLeft` intToBits (cast n)
422422
423423public
424−getBit : Fin n -> Bits n -> Bool
424+getBit : [static] {n : Nat} -> Fin n -> Bits n -> Bool
425425getBit n x = (x `and` (bitAt n)) /= intToBits 0
426426
427427public
428−setBit : Fin n -> Bits n -> Bits n
428+setBit : [static] {n : Nat} -> Fin n -> Bits n -> Bits n
429429setBit n x = x `or` (bitAt n)
430430
431431public
432−unsetBit : Fin n -> Bits n -> Bits n
432+unsetBit : [static] {n : Nat} -> Fin n -> Bits n -> Bits n
433433unsetBit n x = x `and` complement (bitAt n)
434434
435−bitsToStr : Bits n -> String
435+bitsToStr : [static] {n : Nat} -> Bits n -> String
436436bitsToStr x = pack (helper last x)
437437 where
438438 %assert_total
439− helper : Fin (S n) -> Bits n -> List Char
439+ helper : [static] {n : Nat} -> Fin (S n) -> Bits n -> List Char
440440 helper FZ _ = []
441441 helper (FS x) b = (if getBit x b then '1' else '0') :: helper (weaken x) b
442442