@@ -31,17 +31,18 @@ bitsUsed n = 8 * (2 `power` n)
31natToBits' : machineTy n -> Nat -> machineTy n
31natToBits' : machineTy n -> Nat -> machineTy n
32natToBits' a O = a
32natToBits' a O = a
33natToBits' {n=n} a x with n
33natToBits' {n=n} a x with n
34+ -- it seems I have to manually recover the value of n here, instead of being able to reference it
34− natToBits' a (S x') | O = natToBits' (prim__addB8 a (prim__truncInt_B8 1)) x'
35+ natToBits' a (S x') | O = natToBits' {n=0} (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 O = natToBits' {n=1} (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 O) = natToBits' {n=2} (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'
38+ natToBits' a (S x') | S (S (S _)) = natToBits' {n=3} (prim__addB64 a (prim__truncInt_B64 1)) x'
39natToBits : Nat -> machineTy n
40natToBits : Nat -> machineTy n
40natToBits {n=n} x with n
41natToBits {n=n} x with n
41− | O = natToBits' (prim__truncInt_B8 0) x
42+ | O = natToBits' {n=0} (prim__truncInt_B8 0) x
42− | S O = natToBits' (prim__truncInt_B16 0) x
43+ | S O = natToBits' {n=1} (prim__truncInt_B16 0) x
43− | S (S O) = natToBits' (prim__truncInt_B32 0) x
44+ | S (S O) = natToBits' {n=2} (prim__truncInt_B32 0) x
44− | S (S (S _)) = natToBits' (prim__truncInt_B64 0) x
45+ | S (S (S _)) = natToBits' {n=3} (prim__truncInt_B64 0) x
46getPad : Nat -> machineTy n
47getPad : Nat -> machineTy n
47getPad n = natToBits ((bitsUsed (nextBytes n)) - n)
48getPad n = natToBits ((bitsUsed (nextBytes n)) - n)
@@ -156,7 +157,7 @@ xor' {n=n} x y with n
158xor : Bits n -> Bits n -> Bits n
159xor : 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)
161plus' : machineTy (nextBytes n) -> machineTy (nextBytes n) -> machineTy (nextBytes n)
162plus' : machineTy (nextBytes n) -> machineTy (nextBytes n) -> machineTy (nextBytes n)
162plus' {n=n} x y with (nextBytes n)
163plus' {n=n} x y with (nextBytes n)
@@ -240,36 +241,36 @@ urem : Bits n -> Bits n -> Bits n
240urem (MkBits x) (MkBits y) = MkBits (urem' x y)
241urem (MkBits x) (MkBits y) = MkBits (urem' x y)
242-- TODO: Proofy comparisons via postulates
243-- TODO: Proofy comparisons via postulates
243−lt : machineTy n -> machineTy n -> Int
244+lt : machineTy (nextBytes n) -> machineTy (nextBytes n) -> Int
244−lt {n=n} x y with n
245+lt {n=n} x y with (nextBytes n)
245 | O = prim__ltB8 x y
246 | O = prim__ltB8 x y
246 | S O = prim__ltB16 x y
247 | S O = prim__ltB16 x y
247 | S (S O) = prim__ltB32 x y
248 | S (S O) = prim__ltB32 x y
248 | S (S (S _)) = prim__ltB64 x y
249 | S (S (S _)) = prim__ltB64 x y
250−lte : machineTy n -> machineTy n -> Int
251+lte : machineTy (nextBytes n) -> machineTy (nextBytes n) -> Int
251−lte {n=n} x y with n
252+lte {n=n} x y with (nextBytes n)
252 | O = prim__lteB8 x y
253 | O = prim__lteB8 x y
253 | S O = prim__lteB16 x y
254 | S O = prim__lteB16 x y
254 | S (S O) = prim__lteB32 x y
255 | S (S O) = prim__lteB32 x y
255 | S (S (S _)) = prim__lteB64 x y
256 | S (S (S _)) = prim__lteB64 x y
257−eq : machineTy n -> machineTy n -> Int
258+eq : machineTy (nextBytes n) -> machineTy (nextBytes n) -> Int
258−eq {n=n} x y with n
259+eq {n=n} x y with (nextBytes n)
259 | O = prim__eqB8 x y
260 | O = prim__eqB8 x y
260 | S O = prim__eqB16 x y
261 | S O = prim__eqB16 x y
261 | S (S O) = prim__eqB32 x y
262 | S (S O) = prim__eqB32 x y
262 | S (S (S _)) = prim__eqB64 x y
263 | S (S (S _)) = prim__eqB64 x y
264−gte : machineTy n -> machineTy n -> Int
265+gte : machineTy (nextBytes n) -> machineTy (nextBytes n) -> Int
265−gte {n=n} x y with n
266+gte {n=n} x y with (nextBytes n)
266 | O = prim__gteB8 x y
267 | O = prim__gteB8 x y
267 | S O = prim__gteB16 x y
268 | S O = prim__gteB16 x y
268 | S (S O) = prim__gteB32 x y
269 | S (S O) = prim__gteB32 x y
269 | S (S (S _)) = prim__gteB64 x y
270 | S (S (S _)) = prim__gteB64 x y
271−gt : machineTy n -> machineTy n -> Int
272+gt : machineTy (nextBytes n) -> machineTy (nextBytes n) -> Int
272−gt {n=n} x y with n
273+gt {n=n} x y with (nextBytes n)
273 | O = prim__gtB8 x y
274 | O = prim__gtB8 x y
274 | S O = prim__gtB16 x y
275 | S O = prim__gtB16 x y
275 | S (S O) = prim__gtB32 x y
276 | S (S O) = prim__gtB32 x y
@@ -342,8 +343,8 @@ intToBits n = MkBits (intToBits' n)
342instance Cast Int (Bits n) where
343instance Cast Int (Bits n) where
343 cast = intToBits
344 cast = intToBits
345−bitsToInt' : machineTy n -> Int
346+bitsToInt' : machineTy (nextBytes n) -> Int
346−bitsToInt' {n=n} x with n
347+bitsToInt' {n=n} x with (nextBytes n)
347 | O = prim__zextB8_Int x
348 | O = prim__zextB8_Int x
348 | S O = prim__zextB16_Int x
349 | S O = prim__zextB16_Int x
349 | S (S O) = prim__zextB32_Int x
350 | S (S O) = prim__zextB32_Int x
@@ -354,11 +355,11 @@ bitsToInt : Bits n -> Int
354bitsToInt (MkBits x) = bitsToInt' x
355bitsToInt (MkBits x) = bitsToInt' x
356-- Zero out the high bits of a truncated bitstring
357-- Zero out the high bits of a truncated bitstring
357−zeroUnused : machineTy (nextBytes n) -> machineTy (nextBytes n)
358+--zeroUnused : machineTy (nextBytes n) -> machineTy (nextBytes n)
358−zeroUnused x = x `and'` complement' (intToBits' 0)
359+--zeroUnused {n} x = x `and'` complement' (intToBits' {n=n} 0)
360−instance Cast Nat (Bits n) where
361+--instance Cast Nat (Bits n) where
361− cast x = MkBits (zeroUnused (natToBits n))
362+-- cast x = MkBits (zeroUnused (natToBits n))
363-- TODO: Prove
364-- TODO: Prove
364sext' : machineTy (nextBytes n) -> machineTy (nextBytes (n+m))
365sext' : machineTy (nextBytes n) -> machineTy (nextBytes (n+m))
@@ -390,9 +391,9 @@ sext' {n=n} {m=m} x with (nextBytes n, nextBytes (n+m))
390 | (S (S (S _)), S (S (S _))) = let pad = getPad {n=3} n in
391 | (S (S (S _)), S (S (S _))) = let pad = getPad {n=3} n in
391 believe_me (prim__ashrB64 (prim__shlB64 (believe_me x) pad) pad)
392 believe_me (prim__ashrB64 (prim__shlB64 (believe_me x) pad) pad)
394−signExtend : Bits n -> Bits (n+m)
395+--signExtend : Bits n -> Bits (n+m)
395−signExtend {m=m} (MkBits x) = MkBits (zeroUnused (sext' x))
396+--signExtend {m=m} (MkBits x) = MkBits (zeroUnused (sext' x))
397-- TODO: Prove
398-- TODO: Prove
398trunc' : machineTy (nextBytes (n+m)) -> machineTy (nextBytes n)
399trunc' : machineTy (nextBytes (n+m)) -> machineTy (nextBytes n)
@@ -408,9 +409,9 @@ trunc' {n=n} {m=m} x with (nextBytes n, nextBytes (n+m))
408 | (S (S O), S (S (S _))) = believe_me (prim__truncB64_B32 (believe_me x))
409 | (S (S O), S (S (S _))) = believe_me (prim__truncB64_B32 (believe_me x))
409 | (S (S (S _)), S (S (S _))) = believe_me x
410 | (S (S (S _)), S (S (S _))) = believe_me x
412−truncate : Bits (n+m) -> Bits n
413+--truncate : Bits (n+m) -> Bits n
413−truncate (MkBits x) = MkBits (zeroUnused (trunc' x))
414+--truncate (MkBits x) = MkBits (zeroUnused (trunc' x))
416bitAt : Fin n -> Bits n
417bitAt : Fin n -> Bits n