Safe Haskell	Safe-Inferred
Language	Haskell2010

ZkFold.Symbolic.Data.Combinators

Synopsis

mzipWithMRep :: (Representable f, Traversable f, Applicative m) => (a -> b -> m c) -> f a -> f b -> m (f c)
class Iso b a => Iso a b where
- from :: a -> b
class Resize a b where
- resize :: a -> b
toBits :: (MonadCircuit v a w m, Arithmetic a) => [v] -> Natural -> Natural -> m [v]
fromBits :: Natural -> Natural -> forall v w m. MonadCircuit v a w m => [v] -> m [v]
data RegisterSize
- = Auto
- | Fixed Natural
class KnownRegisterSize (r :: RegisterSize) where
- regSize :: RegisterSize
maxOverflow :: forall a n r. (Finite a, KnownNat n, KnownRegisterSize r) => Natural
highRegisterSize :: forall a n r. (Finite a, KnownNat n, KnownRegisterSize r) => Natural
registerSize :: forall a n r. (Finite a, KnownNat n, KnownRegisterSize r) => Natural
type Ceil a b = Div ((a + b) - 1) b
type family GetRegisterSize (a :: Type) (bits :: Natural) (r :: RegisterSize) :: Natural where ...
type KnownRegisters c bits r = KnownNat (NumberOfRegisters (BaseField c) bits r)
type family NumberOfRegisters (a :: Type) (bits :: Natural) (r :: RegisterSize) :: Natural where ...
type family NumberOfRegisters' (a :: Type) (bits :: Natural) (c :: [Natural]) :: Natural where ...
type family BitLimit (a :: Type) :: Natural where ...
type family MaxAdded (regCount :: Natural) :: Natural where ...
type family MaxRegisterSize (a :: Type) (regCount :: Natural) :: Natural where ...
type family ListRange (from :: Natural) (to :: Natural) :: [Natural] where ...
numberOfRegisters :: forall a n r. (Finite a, KnownNat n, KnownRegisterSize r) => Natural
log2 :: Natural -> Double
getNatural :: forall n. KnownNat n => Natural
maxBitsPerFieldElement :: forall p. Finite p => Natural
maxBitsPerRegister :: forall p n. (Finite p, KnownNat n) => Natural
highRegisterBits :: forall p n. (Finite p, KnownNat n) => Natural
minNumberOfRegisters :: forall p n. (Finite p, KnownNat n) => Natural
class IsTypeString (s :: Symbol) a where
- fromType :: a
type family Length (s :: Symbol) :: Natural where ...
type family FromMaybe (a :: k) (mb :: Maybe k) :: k where ...
type family Length' (s :: Maybe (Char, Symbol)) :: Natural where ...
type NextPow2 n = 2 ^ Log2 ((2 * n) - 1)
nextPow2 :: Natural -> Natural
nextNBits :: Natural -> Natural
withNextNBits' :: forall n. KnownNat n :- KnownNat (Log2 ((2 * n) - 1))
withNextNBits :: forall n {r}. KnownNat n => (KnownNat (Log2 ((2 * n) - 1)) => r) -> r
type SecondNextPow2 n = 2 ^ (Log2 ((2 * n) - 1) + 1)
secondNextPow2 :: Natural -> Natural
secondNextNBits :: Natural -> Natural
withSecondNextNBits' :: forall n. KnownNat n :- KnownNat (Log2 ((2 * n) - 1) + 1)
withSecondNextNBits :: forall n {r}. KnownNat n => (KnownNat (Log2 ((2 * n) - 1) + 1) => r) -> r
withNumberOfRegisters' :: forall n r a. (KnownNat n, KnownRegisterSize r, Finite a) :- KnownNat (NumberOfRegisters a n r)
withNumberOfRegisters :: forall n r a {k}. (KnownNat n, KnownRegisterSize r, Finite a) => (KnownNat (NumberOfRegisters a n r) => k) -> k
padNextPow2 :: forall i a w m n. (MonadCircuit i a w m, KnownNat n) => Vector n i -> m (Vector (NextPow2 n) i)
padSecondNextPow2 :: forall i a w m n. (MonadCircuit i a w m, KnownNat n) => Vector n i -> m (Vector (SecondNextPow2 n) i)
expansion :: (MonadCircuit i a w m, Arithmetic a) => Natural -> i -> m [i]
expansionW :: forall r i a w m. (KnownNat r, MonadCircuit i a w m, Arithmetic a) => Natural -> i -> m [i]
bitsOf :: (MonadCircuit i a w m, Arithmetic a) => Natural -> i -> m [i]
wordsOf :: forall r i a w m. (KnownNat r, MonadCircuit i a w m, Arithmetic a) => Natural -> i -> m [i]
hornerW :: forall r i a w m. (KnownNat r, MonadCircuit i a w m) => [i] -> m i
horner :: MonadCircuit i a w m => [i] -> m i
splitExpansion :: (MonadCircuit i a w m, Arithmetic a) => Natural -> Natural -> i -> m (i, i)
runInvert :: (MonadCircuit i a w m, Representable f, Traversable f) => f i -> m (f i, f i)
isZero :: (MonadCircuit i a w m, Representable f, Traversable f) => f i -> m (f i)
ilog2 :: Natural -> Natural

Documentation

mzipWithMRep :: (Representable f, Traversable f, Applicative m) => (a -> b -> m c) -> f a -> f b -> m (f c) Source #

class Iso b a => Iso a b where Source #

A class for isomorphic types. The Iso b a context ensures that transformations in both directions are defined

Methods

from :: a -> b Source #

Instances

Instances details

(Symbolic c, NumberOfBits (BaseField c) ~ n) => Iso (FieldElement c) (ByteString n c) Source #
Instance details Defined in ZkFold.Symbolic.Data.ByteString Methods from :: FieldElement c -> ByteString n c Source #
(Symbolic c, KnownRegisterSize r, NumberOfBits (BaseField c) ~ n) => Iso (FieldElement c) (UInt n r c) Source #
Instance details Defined in ZkFold.Symbolic.Data.UInt Methods from :: FieldElement c -> UInt n r c Source #
(Symbolic c, NumberOfBits (BaseField c) ~ n) => Iso (ByteString n c) (FieldElement c) Source #
Instance details Defined in ZkFold.Symbolic.Data.ByteString Methods from :: ByteString n c -> FieldElement c Source #
(Symbolic c, KnownNat n, KnownRegisterSize r) => Iso (ByteString n c) (UInt n r c) Source #
Instance details Defined in ZkFold.Symbolic.Data.UInt Methods from :: ByteString n c -> UInt n r c Source #
(Symbolic c, KnownRegisterSize r, NumberOfBits (BaseField c) ~ n) => Iso (UInt n r c) (FieldElement c) Source #
Instance details Defined in ZkFold.Symbolic.Data.UInt Methods from :: UInt n r c -> FieldElement c Source #
(Symbolic c, KnownNat n, KnownRegisterSize r) => Iso (UInt n r c) (ByteString n c) Source #
Instance details Defined in ZkFold.Symbolic.Data.UInt Methods from :: UInt n r c -> ByteString n c Source #

class Resize a b where Source #

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 Source #

Instances

Instances details

(Symbolic c, KnownNat k, KnownNat n) => Resize (ByteString k c) (ByteString n c) Source #
Instance details Defined in ZkFold.Symbolic.Data.ByteString Methods resize :: ByteString k c -> ByteString n c Source #
(Symbolic c, KnownNat n, KnownNat k, KnownRegisterSize r) => Resize (UInt n r c) (UInt k r c) Source #
Instance details Defined in ZkFold.Symbolic.Data.UInt Methods resize :: UInt n r c -> UInt k r c Source #

toBits :: (MonadCircuit v a w m, Arithmetic a) => [v] -> Natural -> Natural -> m [v] Source #

Convert an ArithmeticCircuit to bits and return their corresponding variables.

fromBits :: Natural -> Natural -> forall v w m. MonadCircuit v a w m => [v] -> m [v] Source #

The inverse of toBits.

data RegisterSize Source #

Constructors

Auto
Fixed Natural

Instances

Instances details

Show RegisterSize Source #
Instance details Defined in ZkFold.Symbolic.Data.Combinators Methods showsPrec :: Int -> RegisterSize -> ShowS # show :: RegisterSize -> String # showList :: [RegisterSize] -> ShowS #
Eq RegisterSize Source #
Instance details Defined in ZkFold.Symbolic.Data.Combinators Methods (==) :: RegisterSize -> RegisterSize -> Bool # (/=) :: RegisterSize -> RegisterSize -> Bool #

class KnownRegisterSize (r :: RegisterSize) where Source #

Methods

regSize :: RegisterSize Source #

Instances

Instances details

KnownRegisterSize 'Auto Source #
Instance details Defined in ZkFold.Symbolic.Data.Combinators Methods regSize :: RegisterSize Source #
KnownNat n => KnownRegisterSize ('Fixed n) Source #
Instance details Defined in ZkFold.Symbolic.Data.Combinators Methods regSize :: RegisterSize Source #

maxOverflow :: forall a n r. (Finite a, KnownNat n, KnownRegisterSize r) => Natural Source #

highRegisterSize :: forall a n r. (Finite a, KnownNat n, KnownRegisterSize r) => Natural Source #

registerSize :: forall a n r. (Finite a, KnownNat n, KnownRegisterSize r) => Natural Source #

type Ceil a b = Div ((a + b) - 1) b Source #

type family GetRegisterSize (a :: Type) (bits :: Natural) (r :: RegisterSize) :: Natural where ... Source #

Equations

GetRegisterSize _ 0 _ = 0
GetRegisterSize a bits (Fixed rs) = rs
GetRegisterSize a bits Auto = Ceil bits (NumberOfRegisters a bits Auto)

type KnownRegisters c bits r = KnownNat (NumberOfRegisters (BaseField c) bits r) Source #

type family NumberOfRegisters (a :: Type) (bits :: Natural) (r :: RegisterSize) :: Natural where ... Source #

Equations

NumberOfRegisters _ 0 _ = 0
NumberOfRegisters a bits (Fixed bits) = 1
NumberOfRegisters a bits (Fixed rs) = If (Mod bits rs >? 0) (Div bits rs + 1) (Div bits rs)
NumberOfRegisters a bits Auto = NumberOfRegisters' a bits (ListRange 1 50)

type family NumberOfRegisters' (a :: Type) (bits :: Natural) (c :: [Natural]) :: Natural where ... Source #

Equations

NumberOfRegisters' a bits '[] = 0
NumberOfRegisters' a bits (x ': xs) = OrdCond (CmpNat bits (x * MaxRegisterSize a x)) x x (NumberOfRegisters' a bits xs)

type family BitLimit (a :: Type) :: Natural where ... Source #

Equations

BitLimit a = Log2 (Order a)

type family MaxAdded (regCount :: Natural) :: Natural where ... Source #

Equations

MaxAdded regCount = OrdCond (CmpNat regCount (2 ^ Log2 regCount)) (TypeError (Text "Impossible")) (Log2 regCount) (1 + Log2 regCount)

type family MaxRegisterSize (a :: Type) (regCount :: Natural) :: Natural where ... Source #

Equations

MaxRegisterSize a regCount = Div (BitLimit a - MaxAdded regCount) 2

type family ListRange (from :: Natural) (to :: Natural) :: [Natural] where ... Source #

Equations

ListRange from from = '[from]
ListRange from to = from ': ListRange (from + 1) to

numberOfRegisters :: forall a n r. (Finite a, KnownNat n, KnownRegisterSize r) => Natural Source #

log2 :: Natural -> Double Source #

getNatural :: forall n. KnownNat n => Natural Source #

maxBitsPerFieldElement :: forall p. Finite p => Natural Source #

The maximum number of bits a Field element can encode.

maxBitsPerRegister :: forall p n. (Finite p, KnownNat n) => Natural Source #

The maximum number of bits it makes sense to encode in a register. That is, if the field elements can encode more bits than required, choose the smaller number.

highRegisterBits :: forall p n. (Finite p, KnownNat n) => Natural Source #

The number of bits remaining for the higher register assuming that all smaller registers have the same optimal number of bits.

minNumberOfRegisters :: forall p n. (Finite p, KnownNat n) => Natural Source #

The lowest possible number of registers to encode n bits using Field elements from p assuming that each register storest the largest possible number of bits.

class IsTypeString (s :: Symbol) a where Source #

Convert a type-level string into a term. Useful for ByteStrings and VarByteStrings as it will calculate their length automatically

Methods

fromType :: a Source #

Instances

Instances details

(Symbolic ctx, KnownSymbol s, m ~ Length s, (m * 8) ~ l, KnownNat m) => IsTypeString s (VarByteString l ctx) Source #	Construct a VarByteString from a type-level string calculating its length automatically
Instance details Defined in ZkFold.Symbolic.Data.VarByteString Methods fromType :: VarByteString l ctx Source #

type family Length (s :: Symbol) :: Natural where ... Source #

Equations

Length s = Length' (UnconsSymbol s)

type family FromMaybe (a :: k) (mb :: Maybe k) :: k where ... Source #

Equations

FromMaybe def Nothing = def
FromMaybe def (Just a) = a

type family Length' (s :: Maybe (Char, Symbol)) :: Natural where ... Source #

Equations

Length' 'Nothing = 0
Length' ('Just '(c, rest)) = 1 + Length' (UnconsSymbol rest)

type NextPow2 n = 2 ^ Log2 ((2 * n) - 1) Source #

Types and helper axioms for padding vectors

nextPow2 :: Natural -> Natural Source #

nextNBits :: Natural -> Natural Source #

withNextNBits' :: forall n. KnownNat n :- KnownNat (Log2 ((2 * n) - 1)) Source #

withNextNBits :: forall n {r}. KnownNat n => (KnownNat (Log2 ((2 * n) - 1)) => r) -> r Source #

type SecondNextPow2 n = 2 ^ (Log2 ((2 * n) - 1) + 1) Source #

secondNextPow2 :: Natural -> Natural Source #

secondNextNBits :: Natural -> Natural Source #

withSecondNextNBits' :: forall n. KnownNat n :- KnownNat (Log2 ((2 * n) - 1) + 1) Source #

withSecondNextNBits :: forall n {r}. KnownNat n => (KnownNat (Log2 ((2 * n) - 1) + 1) => r) -> r Source #

withNumberOfRegisters' :: forall n r a. (KnownNat n, KnownRegisterSize r, Finite a) :- KnownNat (NumberOfRegisters a n r) Source #

withNumberOfRegisters :: forall n r a {k}. (KnownNat n, KnownRegisterSize r, Finite a) => (KnownNat (NumberOfRegisters a n r) => k) -> k Source #

padNextPow2 :: forall i a w m n. (MonadCircuit i a w m, KnownNat n) => Vector n i -> m (Vector (NextPow2 n) i) Source #

padSecondNextPow2 :: forall i a w m n. (MonadCircuit i a w m, KnownNat n) => Vector n i -> m (Vector (SecondNextPow2 n) i) Source #

expansion :: (MonadCircuit i a w m, Arithmetic a) => Natural -> i -> m [i] Source #

expansion n k computes a binary expansion of k if it fits in n bits.

expansionW :: forall r i a w m. (KnownNat r, MonadCircuit i a w m, Arithmetic a) => Natural -> i -> m [i] Source #

bitsOf :: (MonadCircuit i a w m, Arithmetic a) => Natural -> i -> m [i] Source #

bitsOf n k creates n bits and sets their witnesses equal to n smaller bits of k.

wordsOf :: forall r i a w m. (KnownNat r, MonadCircuit i a w m, Arithmetic a) => Natural -> i -> m [i] Source #

wordsOf n k creates n r-bit words and sets their witnesses equal to n smaller words of k.

hornerW :: forall r i a w m. (KnownNat r, MonadCircuit i a w m) => [i] -> m i Source #

horner [b0,...,bn] computes the sum b0 + (2^r) b1 + ... + 2^rn bn using Horner's scheme.

horner :: MonadCircuit i a w m => [i] -> m i Source #

horner [b0,...,bn] computes the sum b0 + 2 b1 + ... + 2^n bn using Horner's scheme.

splitExpansion :: (MonadCircuit i a w m, Arithmetic a) => Natural -> Natural -> i -> m (i, i) Source #

splitExpansion n1 n2 k computes two values (l, h) such that k = 2^n1 h + l, l fits in n1 bits and h fits in n2 bits (if such values exist).

runInvert :: (MonadCircuit i a w m, Representable f, Traversable f) => f i -> m (f i, f i) Source #

isZero :: (MonadCircuit i a w m, Representable f, Traversable f) => f i -> m (f i) Source #

ilog2 :: Natural -> Natural Source #