@@ -31,17 +31,18 @@ bitsUsed n = 8 * (2 `power` n)
3131natToBits' : machineTy n -> Nat -> machineTy n
3232natToBits' a O = a
3333natToBits' {n=n} a x with n
34− natToBits' a (S x') | O = natToBits' (prim__addB8 a (prim__truncInt_B8 1)) x'
35− natToBits' a (S x') | S O = natToBits' (prim__addB16 a (prim__truncInt_B16 1)) x'
36− natToBits' a (S x') | S (S O) = natToBits' (prim__addB32 a (prim__truncInt_B32 1)) x'
37− natToBits' a (S x') | S (S (S _)) = natToBits' (prim__addB64 a (prim__truncInt_B64 1)) x'
34+ -- it seems I have to manually recover the value of n here, instead of being able to reference it
35+ natToBits' a (S x') | O = natToBits' {n=0} (prim__addB8 a (prim__truncInt_B8 1)) x'
36+ natToBits' a (S x') | S O = natToBits' {n=1} (prim__addB16 a (prim__truncInt_B16 1)) x'
37+ natToBits' a (S x') | S (S O) = natToBits' {n=2} (prim__addB32 a (prim__truncInt_B32 1)) x'
38+ natToBits' a (S x') | S (S (S _)) = natToBits' {n=3} (prim__addB64 a (prim__truncInt_B64 1)) x'
3839
3940natToBits : Nat -> machineTy n
4041natToBits {n=n} x with n
41− | O = natToBits' (prim__truncInt_B8 0) x
42− | S O = natToBits' (prim__truncInt_B16 0) x
43− | S (S O) = natToBits' (prim__truncInt_B32 0) x
44− | S (S (S _)) = natToBits' (prim__truncInt_B64 0) x
42+ | O = natToBits' {n=0} (prim__truncInt_B8 0) x
43+ | S O = natToBits' {n=1} (prim__truncInt_B16 0) x
44+ | S (S O) = natToBits' {n=2} (prim__truncInt_B32 0) x
45+ | S (S (S _)) = natToBits' {n=3} (prim__truncInt_B64 0) x
4546
4647getPad : Nat -> machineTy n
4748getPad n = natToBits ((bitsUsed (nextBytes n)) - n)
@@ -156,7 +157,7 @@ xor' {n=n} x y with n
156157
157158public
158159xor : Bits n -> Bits n -> Bits n
159−xor (MkBits x) (MkBits y) = MkBits (xor' x y)
160+xor {n} (MkBits x) (MkBits y) = MkBits {n} (xor' {n=nextBytes n} x y)
160161
161162plus' : machineTy (nextBytes n) -> machineTy (nextBytes n) -> machineTy (nextBytes n)
162163plus' {n=n} x y with (nextBytes n)
@@ -240,36 +241,36 @@ urem : Bits n -> Bits n -> Bits n
240241urem (MkBits x) (MkBits y) = MkBits (urem' x y)
241242
242243-- TODO: Proofy comparisons via postulates
243−lt : machineTy n -> machineTy n -> Int
244−lt {n=n} x y with n
244+lt : machineTy (nextBytes n) -> machineTy (nextBytes n) -> Int
245+lt {n=n} x y with (nextBytes n)
245246 | O = prim__ltB8 x y
246247 | S O = prim__ltB16 x y
247248 | S (S O) = prim__ltB32 x y
248249 | S (S (S _)) = prim__ltB64 x y
249250
250−lte : machineTy n -> machineTy n -> Int
251−lte {n=n} x y with n
251+lte : machineTy (nextBytes n) -> machineTy (nextBytes n) -> Int
252+lte {n=n} x y with (nextBytes n)
252253 | O = prim__lteB8 x y
253254 | S O = prim__lteB16 x y
254255 | S (S O) = prim__lteB32 x y
255256 | S (S (S _)) = prim__lteB64 x y
256257
257−eq : machineTy n -> machineTy n -> Int
258−eq {n=n} x y with n
258+eq : machineTy (nextBytes n) -> machineTy (nextBytes n) -> Int
259+eq {n=n} x y with (nextBytes n)
259260 | O = prim__eqB8 x y
260261 | S O = prim__eqB16 x y
261262 | S (S O) = prim__eqB32 x y
262263 | S (S (S _)) = prim__eqB64 x y
263264
264−gte : machineTy n -> machineTy n -> Int
265−gte {n=n} x y with n
265+gte : machineTy (nextBytes n) -> machineTy (nextBytes n) -> Int
266+gte {n=n} x y with (nextBytes n)
266267 | O = prim__gteB8 x y
267268 | S O = prim__gteB16 x y
268269 | S (S O) = prim__gteB32 x y
269270 | S (S (S _)) = prim__gteB64 x y
270271
271−gt : machineTy n -> machineTy n -> Int
272−gt {n=n} x y with n
272+gt : machineTy (nextBytes n) -> machineTy (nextBytes n) -> Int
273+gt {n=n} x y with (nextBytes n)
273274 | O = prim__gtB8 x y
274275 | S O = prim__gtB16 x y
275276 | S (S O) = prim__gtB32 x y
@@ -342,8 +343,8 @@ intToBits n = MkBits (intToBits' n)
342343instance Cast Int (Bits n) where
343344 cast = intToBits
344345
345−bitsToInt' : machineTy n -> Int
346−bitsToInt' {n=n} x with n
346+bitsToInt' : machineTy (nextBytes n) -> Int
347+bitsToInt' {n=n} x with (nextBytes n)
347348 | O = prim__zextB8_Int x
348349 | S O = prim__zextB16_Int x
349350 | S (S O) = prim__zextB32_Int x
@@ -354,11 +355,11 @@ bitsToInt : Bits n -> Int
354355bitsToInt (MkBits x) = bitsToInt' x
355356
356357-- Zero out the high bits of a truncated bitstring
357−zeroUnused : machineTy (nextBytes n) -> machineTy (nextBytes n)
358−zeroUnused x = x `and'` complement' (intToBits' 0)
358+--zeroUnused : machineTy (nextBytes n) -> machineTy (nextBytes n)
359+--zeroUnused {n} x = x `and'` complement' (intToBits' {n=n} 0)
359360
360−instance Cast Nat (Bits n) where
361− cast x = MkBits (zeroUnused (natToBits n))
361+--instance Cast Nat (Bits n) where
362+-- cast x = MkBits (zeroUnused (natToBits n))
362363
363364-- TODO: Prove
364365sext' : machineTy (nextBytes n) -> machineTy (nextBytes (n+m))
@@ -390,9 +391,9 @@ sext' {n=n} {m=m} x with (nextBytes n, nextBytes (n+m))
390391 | (S (S (S _)), S (S (S _))) = let pad = getPad {n=3} n in
391392 believe_me (prim__ashrB64 (prim__shlB64 (believe_me x) pad) pad)
392393
393−public
394−signExtend : Bits n -> Bits (n+m)
395−signExtend {m=m} (MkBits x) = MkBits (zeroUnused (sext' x))
394+--public
395+--signExtend : Bits n -> Bits (n+m)
396+--signExtend {m=m} (MkBits x) = MkBits (zeroUnused (sext' x))
396397
397398-- TODO: Prove
398399trunc' : machineTy (nextBytes (n+m)) -> machineTy (nextBytes n)
@@ -408,9 +409,9 @@ trunc' {n=n} {m=m} x with (nextBytes n, nextBytes (n+m))
408409 | (S (S O), S (S (S _))) = believe_me (prim__truncB64_B32 (believe_me x))
409410 | (S (S (S _)), S (S (S _))) = believe_me x
410411
411−public
412−truncate : Bits (n+m) -> Bits n
413−truncate (MkBits x) = MkBits (zeroUnused (trunc' x))
412+--public
413+--truncate : Bits (n+m) -> Bits n
414+--truncate (MkBits x) = MkBits (zeroUnused (trunc' x))
414415
415416public
416417bitAt : Fin n -> Bits n