@@ -19,8 +19,8 @@ nextPow2 (S x) = if (S x) == (2 `power` l2x)
19 l2x = log2NZ (S x) SIsNotZ
19 l2x = log2NZ (S x) SIsNotZ
21||| Gets the lowest n for which "8 * 2 ^ n" is larger than or equal to the input.
21||| Gets the lowest n for which "8 * 2 ^ n" is larger than or equal to the input.
22−||| For example, `nextBytes 10 = 16`.
22+||| For example, `nextBytes 10 = 1`.
23−||| Like with nextPow2, the result is not rounded up, so `nextBytes 16 = 16`.
23+||| Like with nextPow2, the result is not rounded up, so `nextBytes 16 = 1`.
24public export
24public export
25nextBytes : Nat -> Nat
25nextBytes : Nat -> Nat
26nextBytes bits = (nextPow2 (divCeilNZ bits 8 SIsNotZ))
26nextBytes bits = (nextPow2 (divCeilNZ bits 8 SIsNotZ))
@@ -368,6 +368,7 @@ complement' {n=n} x with (nextBytes n)
368 prim__complB64 (x `prim__shlB64` pad) `prim__lshrB64` pad
368 prim__complB64 (x `prim__shlB64` pad) `prim__lshrB64` pad
369 | _ = assert_unreachable
369 | _ = assert_unreachable
371+||| Reverse all the bits in the argument.
371complement : %static {n : Nat} -> Bits n -> Bits n
372complement : %static {n : Nat} -> Bits n -> Bits n
372complement (MkBits x) = MkBits (complement' x)
373complement (MkBits x) = MkBits (complement' x)
@@ -386,6 +387,7 @@ zext' {n=n} {m=m} x with (nextBytes n, nextBytes (n+m))
386 | (S (S (S _)), S (S (S _))) = believe_me x
387 | (S (S (S _)), S (S (S _))) = believe_me x
387 | _ = assert_unreachable
388 | _ = assert_unreachable
390+||| Extend the bitstring with zeros, leaving the first n bits unchanged.
389zeroExtend : %static {n : Nat} -> %static {m : Nat} -> Bits n -> Bits (n+m)
391zeroExtend : %static {n : Nat} -> %static {m : Nat} -> Bits n -> Bits (n+m)
390zeroExtend (MkBits x) = MkBits (zext' x)
392zeroExtend (MkBits x) = MkBits (zext' x)
@@ -418,7 +420,7 @@ bitsToInt' {n=n} x with (nextBytes n)
418bitsToInt : %static {n : Nat} -> Bits n -> Integer
420bitsToInt : %static {n : Nat} -> Bits n -> Integer
419bitsToInt (MkBits x) = bitsToInt' x
421bitsToInt (MkBits x) = bitsToInt' x
421−-- Zero out the high bits of a truncated bitstring
423+||| Zero out the high bits of a truncated bitstring
422zeroUnused : %static {n : Nat} -> machineTy (nextBytes n) -> machineTy (nextBytes n)
424zeroUnused : %static {n : Nat} -> machineTy (nextBytes n) -> machineTy (nextBytes n)
423zeroUnused {n} x = x `and'` complement' (intToBits' {n=n} 0)
425zeroUnused {n} x = x `and'` complement' (intToBits' {n=n} 0)
@@ -474,10 +476,13 @@ trunc' {m=m} {n=n} x with (nextBytes n, nextBytes (m+n))
474 | (S (S (S _)), S (S (S _))) = believe_me x
476 | (S (S (S _)), S (S (S _))) = believe_me x
475 | _ = assert_unreachable
477 | _ = assert_unreachable
479+||| Truncate the high bits of a bitstring.
477truncate : %static {m : Nat} -> %static {n : Nat} -> Bits (m+n) -> Bits n
480truncate : %static {m : Nat} -> %static {n : Nat} -> Bits (m+n) -> Bits n
478truncate (MkBits x) = MkBits (zeroUnused (trunc' x))
481truncate (MkBits x) = MkBits (zeroUnused (trunc' x))
483+||| Create a bitstring of length n with the bit given as an argument set to one
484+||| and all other bits set to zero.
480−bitAt : %static {n : Nat} -> Fin n -> Bits n
485+bitAt : %static {n : Nat} -> (at : Fin n) -> Bits n
481bitAt n = intToBits 1 `shiftLeft` intToBits (cast n)
486bitAt n = intToBits 1 `shiftLeft` intToBits (cast n)
483getBit : %static {n : Nat} -> Fin n -> Bits n -> Bool
488getBit : %static {n : Nat} -> Fin n -> Bits n -> Bool