| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
ZkFold.Symbolic.Data.ByteString
Synopsis
- newtype ByteString (n :: Natural) (context :: (Type -> Type) -> Type) = ByteString (context (Vector n))
- class ShiftBits a where
- shiftBits :: a -> Integer -> a
- shiftBitsL :: a -> Natural -> a
- shiftBitsR :: a -> Natural -> a
- rotateBits :: a -> Integer -> a
- rotateBitsL :: a -> Natural -> a
- rotateBitsR :: a -> Natural -> a
- reverseEndianness :: forall wordSize k c m {n}. (Symbolic c, KnownNat wordSize, n ~ (k * wordSize), (m * 8) ~ wordSize) => ByteString n c -> ByteString n c
- isSet :: forall c n. Symbolic c => ByteString n c -> Natural -> Bool c
- isUnset :: forall c n. Symbolic c => ByteString n c -> Natural -> Bool c
- toWords :: forall m wordSize c. (Symbolic c, KnownNat wordSize) => ByteString (m * wordSize) c -> Vector m (ByteString wordSize c)
- concat :: forall k m c. Symbolic c => Vector k (ByteString m c) -> ByteString (k * m) c
- truncate :: forall n m c. (Symbolic c, KnownNat n, n <= m) => ByteString m c -> ByteString n c
- emptyByteString :: FromConstant Natural (ByteString 0 c) => ByteString 0 c
- toBsBits :: Natural -> Natural -> [Natural]
Documentation
newtype ByteString (n :: Natural) (context :: (Type -> Type) -> Type) Source #
A ByteString which stores n bits and uses elements of a as registers, one element per register.
Bit layout is Big-endian.
Constructors
| ByteString (context (Vector n)) |
Instances
class ShiftBits a where Source #
A class for data types that support bit shift and bit cyclic shift (rotation) operations.
Minimal complete definition
(shiftBits | shiftBitsL, shiftBitsR), (rotateBits | rotateBitsL, rotateBitsR)
Methods
shiftBits :: a -> Integer -> a Source #
shiftBits performs a left shift when its agrument is greater than zero and a right shift otherwise.
shiftBitsL :: a -> Natural -> a Source #
shiftBitsR :: a -> Natural -> a Source #
rotateBits :: a -> Integer -> a Source #
rotateBits performs a left cyclic shift when its agrument is greater than zero and a right cyclic shift otherwise.
rotateBitsL :: a -> Natural -> a Source #
rotateBitsR :: a -> Natural -> a Source #
Instances
| (Symbolic c, KnownNat n) => ShiftBits (ByteString n c) Source # | |
Defined in ZkFold.Symbolic.Data.ByteString Methods shiftBits :: ByteString n c -> Integer -> ByteString n c Source # shiftBitsL :: ByteString n c -> Natural -> ByteString n c Source # shiftBitsR :: ByteString n c -> Natural -> ByteString n c Source # rotateBits :: ByteString n c -> Integer -> ByteString n c Source # rotateBitsL :: ByteString n c -> Natural -> ByteString n c Source # rotateBitsR :: ByteString n c -> Natural -> ByteString n c Source # | |
reverseEndianness :: forall wordSize k c m {n}. (Symbolic c, KnownNat wordSize, n ~ (k * wordSize), (m * 8) ~ wordSize) => ByteString n c -> ByteString n c Source #
toWords :: forall m wordSize c. (Symbolic c, KnownNat wordSize) => ByteString (m * wordSize) c -> Vector m (ByteString wordSize c) Source #
A ByteString of length n can only be split into words of length wordSize if all of the following conditions are met:
1. wordSize is not greater than n;
2. wordSize is not zero;
3. The bytestring is not empty;
4. wordSize divides n.
concat :: forall k m c. Symbolic c => Vector k (ByteString m c) -> ByteString (k * m) c Source #
truncate :: forall n m c. (Symbolic c, KnownNat n, n <= m) => ByteString m c -> ByteString n c Source #
Describes types that can be truncated by dropping several bits from the end (i.e. stored in the lower registers)
emptyByteString :: FromConstant Natural (ByteString 0 c) => ByteString 0 c Source #