ZkFold.Symbolic.Data.ByteString

Documentation

newtype ByteString (n :: Natural) a

A ByteString which stores n bits and uses elements of a as registers, one element per register. Bit layout is Big-endian.

Constructors

ByteString [a]

Instances

(FromConstant Natural a, KnownNat n) => FromConstant Integer (ByteString n a)

Defined in ZkFold.Symbolic.Data.ByteString

Methods

fromConstant :: Integer -> ByteString n a

(FromConstant Natural a, KnownNat n) => FromConstant Natural (ByteString n a)

Defined in ZkFold.Symbolic.Data.ByteString

Methods

fromConstant :: Natural -> ByteString n a

(Arithmetic a, KnownNat n) => SymbolicData a (ByteString n (ArithmeticCircuit a))

Defined in ZkFold.Symbolic.Data.ByteString

Methods

pieces :: ByteString n (ArithmeticCircuit a) -> [ArithmeticCircuit a]

restore :: [ArithmeticCircuit a] -> ByteString n (ArithmeticCircuit a)

typeSize :: Natural

(KnownNat n, FromConstant Natural a) => ToWords Natural (ByteString n a)

This allows us to calculate hash of a bytestring represented by a Natural number. This is only useful for testing when the length of the test string is unknown at compile time. This should not be exposed to users (and they probably won't find it useful anyway).

Defined in ZkFold.Symbolic.Algorithms.Hash.SHA2

Methods

toWords :: Natural -> [ByteString n a]

(Finite (Zp p), KnownNat n) => Arbitrary (ByteString n (Zp p))

Defined in ZkFold.Symbolic.Data.ByteString

Methods

arbitrary :: Gen (ByteString n (Zp p))

shrink :: ByteString n (Zp p) -> [ByteString n (Zp p)]

Generic (ByteString n a)

Defined in ZkFold.Symbolic.Data.ByteString

Associated Types

type Rep (ByteString n a) :: Type -> Type

Methods

from :: ByteString n a -> Rep (ByteString n a) x

to :: Rep (ByteString n a) x -> ByteString n a

Show a => Show (ByteString n a)

Defined in ZkFold.Symbolic.Data.ByteString

Methods

showsPrec :: Int -> ByteString n a -> ShowS

show :: ByteString n a -> String

showList :: [ByteString n a] -> ShowS

NFData a => NFData (ByteString n a)

Defined in ZkFold.Symbolic.Data.ByteString

Methods

rnf :: ByteString n a -> ()

Eq a => Eq (ByteString n a)

Defined in ZkFold.Symbolic.Data.ByteString

Methods

(==) :: ByteString n a -> ByteString n a -> Bool

(/=) :: ByteString n a -> ByteString n a -> Bool

(Finite (Zp p), KnownNat n) => BoolType (ByteString n (Zp p))

Defined in ZkFold.Symbolic.Data.ByteString

Methods

true :: ByteString n (Zp p)

false :: ByteString n (Zp p)

not :: ByteString n (Zp p) -> ByteString n (Zp p)

(&&) :: ByteString n (Zp p) -> ByteString n (Zp p) -> ByteString n (Zp p)

(||) :: ByteString n (Zp p) -> ByteString n (Zp p) -> ByteString n (Zp p)

xor :: ByteString n (Zp p) -> ByteString n (Zp p) -> ByteString n (Zp p)

(Arithmetic a, KnownNat n) => BoolType (ByteString n (ArithmeticCircuit a))

Defined in ZkFold.Symbolic.Data.ByteString

Methods

true :: ByteString n (ArithmeticCircuit a)

false :: ByteString n (ArithmeticCircuit a)

not :: ByteString n (ArithmeticCircuit a) -> ByteString n (ArithmeticCircuit a)

(&&) :: ByteString n (ArithmeticCircuit a) -> ByteString n (ArithmeticCircuit a) -> ByteString n (ArithmeticCircuit a)

(||) :: ByteString n (ArithmeticCircuit a) -> ByteString n (ArithmeticCircuit a) -> ByteString n (ArithmeticCircuit a)

xor :: ByteString n (ArithmeticCircuit a) -> ByteString n (ArithmeticCircuit a) -> ByteString n (ArithmeticCircuit a)

(Finite (Zp p), KnownNat n) => ShiftBits (ByteString n (Zp p))

Defined in ZkFold.Symbolic.Data.ByteString

Methods

shiftBits :: ByteString n (Zp p) -> Integer -> ByteString n (Zp p)

shiftBitsL :: ByteString n (Zp p) -> Natural -> ByteString n (Zp p)

shiftBitsR :: ByteString n (Zp p) -> Natural -> ByteString n (Zp p)

rotateBits :: ByteString n (Zp p) -> Integer -> ByteString n (Zp p)

rotateBitsL :: ByteString n (Zp p) -> Natural -> ByteString n (Zp p)

rotateBitsR :: ByteString n (Zp p) -> Natural -> ByteString n (Zp p)

(Arithmetic a, KnownNat n) => ShiftBits (ByteString n (ArithmeticCircuit a))

Defined in ZkFold.Symbolic.Data.ByteString

Methods

shiftBits :: ByteString n (ArithmeticCircuit a) -> Integer -> ByteString n (ArithmeticCircuit a)

shiftBitsL :: ByteString n (ArithmeticCircuit a) -> Natural -> ByteString n (ArithmeticCircuit a)

shiftBitsR :: ByteString n (ArithmeticCircuit a) -> Natural -> ByteString n (ArithmeticCircuit a)

rotateBits :: ByteString n (ArithmeticCircuit a) -> Integer -> ByteString n (ArithmeticCircuit a)

rotateBitsL :: ByteString n (ArithmeticCircuit a) -> Natural -> ByteString n (ArithmeticCircuit a)

rotateBitsR :: ByteString n (ArithmeticCircuit a) -> Natural -> ByteString n (ArithmeticCircuit a)

ToConstant a Natural => ToConstant (ByteString n a) Natural

Defined in ZkFold.Symbolic.Data.ByteString

Methods

toConstant :: ByteString n a -> Natural

(KnownNat n, KnownNat m, m <= n, Mod n m ~ 0, Finite (Zp p)) => Concat (ByteString m (Zp p)) (ByteString n (Zp p))

Unfortunately, Haskell does not support dependent types yet, so we have no possibility to infer the exact type of the result (the list can contain an arbitrary number of words). We can only impose some restrictions on n and m.

Defined in ZkFold.Symbolic.Data.ByteString

Methods

concat :: [ByteString m (Zp p)] -> ByteString n (Zp p)

Mod n m ~ 0 => Concat (ByteString m (ArithmeticCircuit a)) (ByteString n (ArithmeticCircuit a))

Defined in ZkFold.Symbolic.Data.ByteString

Methods

concat :: [ByteString m (ArithmeticCircuit a)] -> ByteString n (ArithmeticCircuit a)

(KnownNat wordSize, KnownNat n, Finite (Zp p), wordSize <= n, 1 <= wordSize, 1 <= n, Mod n wordSize ~ 0) => ToWords (ByteString n (Zp p)) (ByteString wordSize (Zp p))

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.

Defined in ZkFold.Symbolic.Data.ByteString

Methods

toWords :: ByteString n (Zp p) -> [ByteString wordSize (Zp p)]

(KnownNat wordSize, 1 <= wordSize, 1 <= n, Mod n wordSize ~ 0) => ToWords (ByteString n (ArithmeticCircuit a)) (ByteString wordSize (ArithmeticCircuit a))

Defined in ZkFold.Symbolic.Data.ByteString

Methods

toWords :: ByteString n (ArithmeticCircuit a) -> [ByteString wordSize (ArithmeticCircuit a)]

(KnownNat m, KnownNat n, n <= m, Finite (Zp p)) => Truncate (ByteString m (Zp p)) (ByteString n (Zp p))

Only a bigger ByteString can be truncated into a smaller one.

Defined in ZkFold.Symbolic.Data.ByteString

Methods

truncate :: ByteString m (Zp p) -> ByteString n (Zp p)

(KnownNat n, n <= m) => Truncate (ByteString m (ArithmeticCircuit a)) (ByteString n (ArithmeticCircuit a))

Defined in ZkFold.Symbolic.Data.ByteString

Methods

truncate :: ByteString m (ArithmeticCircuit a) -> ByteString n (ArithmeticCircuit a)

(KnownNat n, m <= n, Finite (Zp p)) => Extend (ByteString m (Zp p)) (ByteString n (Zp p))

Only a smaller ByteString can be extended into a bigger one.

Defined in ZkFold.Symbolic.Data.ByteString

Methods

extend :: ByteString m (Zp p) -> ByteString n (Zp p)

(KnownNat m, KnownNat n, m <= n, Arithmetic a) => Extend (ByteString m (ArithmeticCircuit a)) (ByteString n (ArithmeticCircuit a))

Defined in ZkFold.Symbolic.Data.ByteString

Methods

extend :: ByteString m (ArithmeticCircuit a) -> ByteString n (ArithmeticCircuit a)

(Finite (Zp p), KnownNat n) => Iso (ByteString n (Zp p)) (UInt n (Zp p))

Defined in ZkFold.Symbolic.Data.ByteString

Methods

from :: ByteString n (Zp p) -> UInt n (Zp p)

(Arithmetic a, KnownNat n) => Iso (ByteString n (ArithmeticCircuit a)) (UInt n (ArithmeticCircuit a))

Defined in ZkFold.Symbolic.Data.ByteString

Methods

from :: ByteString n (ArithmeticCircuit a) -> UInt n (ArithmeticCircuit a)

(Finite (Zp p), KnownNat n) => Iso (UInt n (Zp p)) (ByteString n (Zp p))

Defined in ZkFold.Symbolic.Data.ByteString

Methods

from :: UInt n (Zp p) -> ByteString n (Zp p)

(Arithmetic a, KnownNat n) => Iso (UInt n (ArithmeticCircuit a)) (ByteString n (ArithmeticCircuit a))

Defined in ZkFold.Symbolic.Data.ByteString

Methods

from :: UInt n (ArithmeticCircuit a) -> ByteString n (ArithmeticCircuit a)

type Rep (ByteString n a)

Defined in ZkFold.Symbolic.Data.ByteString

type Rep (ByteString n a) = D1 ('MetaData "ByteString" "ZkFold.Symbolic.Data.ByteString" "zkfold-base-0.1.0.0-inplace" 'True) (C1 ('MetaCons "ByteString" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [a])))

class ShiftBits a where

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

shiftBits performs a left shift when its agrument is greater than zero and a right shift otherwise.

shiftBitsL :: a -> Natural -> a

shiftBitsR :: a -> Natural -> a

rotateBits :: a -> Integer -> a

rotateBits performs a left cyclic shift when its agrument is greater than zero and a right cyclic shift otherwise.

rotateBitsL :: a -> Natural -> a

rotateBitsR :: a -> Natural -> a

Instances

(Finite (Zp p), KnownNat n) => ShiftBits (ByteString n (Zp p))

Defined in ZkFold.Symbolic.Data.ByteString

Methods

shiftBits :: ByteString n (Zp p) -> Integer -> ByteString n (Zp p)

shiftBitsL :: ByteString n (Zp p) -> Natural -> ByteString n (Zp p)

shiftBitsR :: ByteString n (Zp p) -> Natural -> ByteString n (Zp p)

rotateBits :: ByteString n (Zp p) -> Integer -> ByteString n (Zp p)

rotateBitsL :: ByteString n (Zp p) -> Natural -> ByteString n (Zp p)

rotateBitsR :: ByteString n (Zp p) -> Natural -> ByteString n (Zp p)

(Arithmetic a, KnownNat n) => ShiftBits (ByteString n (ArithmeticCircuit a))

Defined in ZkFold.Symbolic.Data.ByteString

Methods

shiftBits :: ByteString n (ArithmeticCircuit a) -> Integer -> ByteString n (ArithmeticCircuit a)

shiftBitsL :: ByteString n (ArithmeticCircuit a) -> Natural -> ByteString n (ArithmeticCircuit a)

shiftBitsR :: ByteString n (ArithmeticCircuit a) -> Natural -> ByteString n (ArithmeticCircuit a)

rotateBits :: ByteString n (ArithmeticCircuit a) -> Integer -> ByteString n (ArithmeticCircuit a)

rotateBitsL :: ByteString n (ArithmeticCircuit a) -> Natural -> ByteString n (ArithmeticCircuit a)

rotateBitsR :: ByteString n (ArithmeticCircuit a) -> Natural -> ByteString n (ArithmeticCircuit a)

class ToWords a b where

Describes types which can be split into words of equal size. Parameters have to be of different types as ByteString store their lengths on type level and hence after splitting they chagne types.

Methods

toWords :: a -> [b]

Instances

(KnownNat n, FromConstant Natural a) => ToWords Natural (ByteString n a)

This allows us to calculate hash of a bytestring represented by a Natural number. This is only useful for testing when the length of the test string is unknown at compile time. This should not be exposed to users (and they probably won't find it useful anyway).

Defined in ZkFold.Symbolic.Algorithms.Hash.SHA2

Methods

toWords :: Natural -> [ByteString n a]

(KnownNat wordSize, KnownNat n, Finite (Zp p), wordSize <= n, 1 <= wordSize, 1 <= n, Mod n wordSize ~ 0) => ToWords (ByteString n (Zp p)) (ByteString wordSize (Zp p))

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.

Defined in ZkFold.Symbolic.Data.ByteString

Methods

toWords :: ByteString n (Zp p) -> [ByteString wordSize (Zp p)]

(KnownNat wordSize, 1 <= wordSize, 1 <= n, Mod n wordSize ~ 0) => ToWords (ByteString n (ArithmeticCircuit a)) (ByteString wordSize (ArithmeticCircuit a))

Defined in ZkFold.Symbolic.Data.ByteString

Methods

toWords :: ByteString n (ArithmeticCircuit a) -> [ByteString wordSize (ArithmeticCircuit a)]

class Concat a b where

Describes types which can be made by concatenating several words of equal length.

Methods

concat :: [a] -> b

Instances

(KnownNat n, KnownNat m, m <= n, Mod n m ~ 0, Finite (Zp p)) => Concat (ByteString m (Zp p)) (ByteString n (Zp p))

Unfortunately, Haskell does not support dependent types yet, so we have no possibility to infer the exact type of the result (the list can contain an arbitrary number of words). We can only impose some restrictions on n and m.

Defined in ZkFold.Symbolic.Data.ByteString

Methods

concat :: [ByteString m (Zp p)] -> ByteString n (Zp p)

Mod n m ~ 0 => Concat (ByteString m (ArithmeticCircuit a)) (ByteString n (ArithmeticCircuit a))

Defined in ZkFold.Symbolic.Data.ByteString

Methods

concat :: [ByteString m (ArithmeticCircuit a)] -> ByteString n (ArithmeticCircuit a)

class Truncate a b where

Describes types that can be truncated by dropping several bits from the end (i.e. stored in the lower registers)

Methods

truncate :: a -> b

Instances

(KnownNat m, KnownNat n, n <= m, Finite (Zp p)) => Truncate (ByteString m (Zp p)) (ByteString n (Zp p))

Only a bigger ByteString can be truncated into a smaller one.

Defined in ZkFold.Symbolic.Data.ByteString

Methods

truncate :: ByteString m (Zp p) -> ByteString n (Zp p)

(KnownNat n, n <= m) => Truncate (ByteString m (ArithmeticCircuit a)) (ByteString n (ArithmeticCircuit a))

Defined in ZkFold.Symbolic.Data.ByteString

Methods

truncate :: ByteString m (ArithmeticCircuit a) -> ByteString n (ArithmeticCircuit a)