ZkFold.Symbolic.Data.ByteString

Documentation

newtype ByteString (n :: Natural) (context :: (Type -> Type) -> Type)

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

(Symbolic c, (m * 8) ~ n, KnownNat m) => FromConstant ByteString (ByteString n c)

Defined in ZkFold.Symbolic.Data.ByteString

Methods

fromConstant :: ByteString0 -> ByteString n c

(Symbolic c, KnownNat n) => FromConstant Integer (ByteString n c)

Defined in ZkFold.Symbolic.Data.ByteString

Methods

fromConstant :: Integer -> ByteString n c

(Symbolic c, KnownNat n) => FromConstant Natural (ByteString n c)

Pack a ByteString using one field element per bit. fromConstant discards bits after n. If the constant is greater than 2^n, only the part modulo 2^n will be converted into a ByteString.

Defined in ZkFold.Symbolic.Data.ByteString

Methods

fromConstant :: Natural -> ByteString n c

(Symbolic c, NumberOfBits (BaseField c) ~ n) => Iso (FieldElement c) (ByteString n c)

Defined in ZkFold.Symbolic.Data.ByteString

Methods

from :: FieldElement c -> ByteString n c

(Symbolic c, KnownNat n) => Conditional (Bool c) (ByteString n c)

Defined in ZkFold.Symbolic.Data.ByteString

Methods

bool :: ByteString n c -> ByteString n c -> Bool c -> ByteString n c

(Symbolic c, KnownNat n) => Arbitrary (ByteString n c)

Defined in ZkFold.Symbolic.Data.ByteString

Methods

arbitrary :: Gen (ByteString n c)

shrink :: ByteString n c -> [ByteString n c]

(Symbolic c, KnownNat n) => FromJSON (ByteString n c)

Defined in ZkFold.Symbolic.Data.ByteString

Methods

parseJSON :: Value -> Parser (ByteString n c)

parseJSONList :: Value -> Parser [ByteString n c]

Arithmetic a => ToJSON (ByteString n (Interpreter a))

Defined in ZkFold.Symbolic.Data.ByteString

Methods

toJSON :: ByteString n (Interpreter a) -> Value

toEncoding :: ByteString n (Interpreter a) -> Encoding

toJSONList :: [ByteString n (Interpreter a)] -> Value

toEncodingList :: [ByteString n (Interpreter a)] -> Encoding

(Symbolic c, (m * 8) ~ n, KnownNat m) => IsString (ByteString n c)

Defined in ZkFold.Symbolic.Data.ByteString

Methods

fromString :: String -> ByteString n c

Generic (ByteString n context)

Defined in ZkFold.Symbolic.Data.ByteString

Associated Types

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

Methods

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

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

Show (c (Vector n)) => Show (ByteString n c)

Defined in ZkFold.Symbolic.Data.ByteString

Methods

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

show :: ByteString n c -> String

showList :: [ByteString n c] -> ShowS

NFData (c (Vector n)) => NFData (ByteString n c)

Defined in ZkFold.Symbolic.Data.ByteString

Methods

rnf :: ByteString n c -> ()

Eq (c (Vector n)) => Eq (ByteString n c)

Defined in ZkFold.Symbolic.Data.ByteString

Methods

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

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

Arithmetic a => ToConstant (ByteString n (Interpreter a))

Defined in ZkFold.Symbolic.Data.ByteString

Associated Types

type Const (ByteString n (Interpreter a))

Methods

toConstant :: ByteString n (Interpreter a) -> Const (ByteString n (Interpreter a))

(Symbolic c, KnownNat n) => BoolType (ByteString n c)

Defined in ZkFold.Symbolic.Data.ByteString

Methods

true :: ByteString n c

false :: ByteString n c

not :: ByteString n c -> ByteString n c

(&&) :: ByteString n c -> ByteString n c -> ByteString n c

(||) :: ByteString n c -> ByteString n c -> ByteString n c

xor :: ByteString n c -> ByteString n c -> ByteString n c

(Symbolic c, KnownNat n) => ShiftBits (ByteString n c)

Defined in ZkFold.Symbolic.Data.ByteString

Methods

shiftBits :: ByteString n c -> Integer -> ByteString n c

shiftBitsL :: ByteString n c -> Natural -> ByteString n c

shiftBitsR :: ByteString n c -> Natural -> ByteString n c

rotateBits :: ByteString n c -> Integer -> ByteString n c

rotateBitsL :: ByteString n c -> Natural -> ByteString n c

rotateBitsR :: ByteString n c -> Natural -> ByteString n c

(KnownNat n, Symbolic c) => SymbolicData (ByteString n c)

Defined in ZkFold.Symbolic.Data.ByteString

Associated Types

type Context (ByteString n c) :: (Type -> Type) -> Type

type Support (ByteString n c)

type Layout (ByteString n c) :: Type -> Type

type Payload (ByteString n c) :: Type -> Type

Methods

arithmetize :: ByteString n c -> Support (ByteString n c) -> Context (ByteString n c) (Layout (ByteString n c))

payload :: ByteString n c -> Support (ByteString n c) -> Payload (ByteString n c) (WitnessField (Context (ByteString n c)))

restore :: Context (ByteString n c) ~ c0 => (Support (ByteString n c) -> (c0 (Layout (ByteString n c)), Payload (ByteString n c) (WitnessField c0))) -> ByteString n c

(Symbolic c, KnownNat n) => Eq (ByteString n c)

Defined in ZkFold.Symbolic.Data.ByteString

Associated Types

type BooleanOf (ByteString n c)

Methods

(==) :: ByteString n c -> ByteString n c -> BooleanOf (ByteString n c)

(/=) :: ByteString n c -> ByteString n c -> BooleanOf (ByteString n c)

(Symbolic c, KnownNat n) => SymbolicInput (ByteString n c)

Defined in ZkFold.Symbolic.Data.ByteString

Methods

isValid :: ByteString n c -> Bool (Context (ByteString n c))

(Symbolic c, NumberOfBits (BaseField c) ~ n) => Iso (ByteString n c) (FieldElement c)

Defined in ZkFold.Symbolic.Data.ByteString

Methods

from :: ByteString n c -> FieldElement c

(Symbolic c, KnownNat k, KnownNat n) => Resize (ByteString k c) (ByteString n c)

Defined in ZkFold.Symbolic.Data.ByteString

Methods

resize :: ByteString k c -> ByteString n c

(Symbolic c, KnownNat n, KnownRegisterSize r) => Iso (ByteString n c) (UInt n r c)

Defined in ZkFold.Symbolic.Data.UInt

Methods

from :: ByteString n c -> UInt n r c

(Symbolic c, KnownNat n, KnownRegisterSize r) => Iso (UInt n r c) (ByteString n c)

Defined in ZkFold.Symbolic.Data.UInt

Methods

from :: UInt n r c -> ByteString n c

type Rep (ByteString n context)

Defined in ZkFold.Symbolic.Data.ByteString

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

type Const (ByteString n (Interpreter a))

Defined in ZkFold.Symbolic.Data.ByteString

type Const (ByteString n (Interpreter a)) = Natural

type Context (ByteString n c)

Defined in ZkFold.Symbolic.Data.ByteString

type Context (ByteString n c) = Context (c (Vector n))

type Layout (ByteString n c)

Defined in ZkFold.Symbolic.Data.ByteString

type Layout (ByteString n c) = Layout (c (Vector n))

type Payload (ByteString n c)

Defined in ZkFold.Symbolic.Data.ByteString

type Payload (ByteString n c) = Payload (c (Vector n))

type Support (ByteString n c)

Defined in ZkFold.Symbolic.Data.ByteString

type Support (ByteString n c) = Support (c (Vector n))

type BooleanOf (ByteString n c)

Defined in ZkFold.Symbolic.Data.ByteString

type BooleanOf (ByteString n c) = BooleanOf (c (Vector n))

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

(Symbolic c, KnownNat n) => ShiftBits (ByteString n c)

Defined in ZkFold.Symbolic.Data.ByteString

Methods

shiftBits :: ByteString n c -> Integer -> ByteString n c

shiftBitsL :: ByteString n c -> Natural -> ByteString n c

shiftBitsR :: ByteString n c -> Natural -> ByteString n c

rotateBits :: ByteString n c -> Integer -> ByteString n c

rotateBitsL :: ByteString n c -> Natural -> ByteString n c

rotateBitsR :: ByteString n c -> Natural -> ByteString n c

class Resize a b where

Describes types that can increase or shrink their capacity by adding zero bits to the beginning (i.e. before the higher register) or removing higher bits.

Methods

resize :: a -> b

Instances

(Symbolic c, KnownNat k, KnownNat n) => Resize (ByteString k c) (ByteString n c)

Defined in ZkFold.Symbolic.Data.ByteString

Methods

resize :: ByteString k c -> ByteString n c

(Symbolic c, KnownNat n, KnownNat k, KnownRegisterSize r) => Resize (UInt n r c) (UInt k r c)

Defined in ZkFold.Symbolic.Data.UInt

Methods

resize :: UInt n r c -> UInt k r c

reverseEndianness :: forall wordSize k c m {n}. (Symbolic c, KnownNat wordSize, n ~ (k * wordSize), (m * 8) ~ wordSize) => ByteString n c -> ByteString n c

set :: forall c n. (Symbolic c, KnownNat n) => ByteString n c -> Natural -> ByteString n c

unset :: forall c n. (Symbolic c, KnownNat n) => ByteString n c -> Natural -> 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)

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

truncate :: forall m n c. (Symbolic c, KnownNat n, n <= m) => ByteString m c -> ByteString n c

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

append :: forall m n c. Symbolic c => KnownNat m => KnownNat n => ByteString m c -> ByteString n c -> ByteString (m + n) c

emptyByteString :: FromConstant Natural (ByteString 0 c) => ByteString 0 c

toBsBits :: Natural -> Natural -> [Natural]

orRight :: forall m n c. Symbolic c => ByteString m c -> ByteString n c -> ByteString (Max m n) c