| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
ZkFold.Symbolic.Data.Combinators
Synopsis
- class Iso b a => Iso a b where
- from :: a -> b
- class Extend a b where
- extend :: a -> b
- class Shrink a b where
- shrink :: a -> b
- toBits :: forall v a m. (MonadCircuit v a m, Arithmetic a) => [v] -> Natural -> Natural -> m [v]
- fromBits :: forall a. Natural -> Natural -> forall v m. MonadCircuit v a m => [v] -> m [v]
- data RegisterSize
- class KnownRegisterSize (r :: RegisterSize) where
- 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 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
- expansion :: (MonadCircuit i a m, Arithmetic a) => Natural -> i -> m [i]
- expansionW :: forall r i a m. (KnownNat r, MonadCircuit i a m, Arithmetic a) => Natural -> i -> m [i]
- bitsOf :: (MonadCircuit i a m, Arithmetic a) => Natural -> i -> m [i]
- wordsOf :: forall r i a m. (KnownNat r, MonadCircuit i a m, Arithmetic a) => Natural -> i -> m [i]
- hornerW :: forall r i a m. (KnownNat r, MonadCircuit i a m) => [i] -> m i
- horner :: MonadCircuit i a m => [i] -> m i
- splitExpansion :: (MonadCircuit i a m, Arithmetic a) => Natural -> Natural -> i -> m (i, i)
- runInvert :: (MonadCircuit i a m, Representable f, Traversable f) => f i -> m (f i, f i)
- isZero :: (MonadCircuit i a m, Representable f, Traversable f) => f i -> m (f i)
Documentation
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
Instances
class Extend a b where Source #
Describes types that can increase their capacity by adding zero bits to the beginning (i.e. before the higher register).
Instances
| (Symbolic c, KnownNat k, KnownNat n, k <= n) => Extend (ByteString k c) (ByteString n c) Source # | |
Defined in ZkFold.Symbolic.Data.ByteString Methods extend :: ByteString k c -> ByteString n c Source # | |
| (Symbolic c, KnownNat n, KnownNat k, KnownRegisterSize r, n <= k) => Extend (UInt n r c) (UInt k r c) Source # | |
class Shrink a b where Source #
Describes types that can shrink their capacity by removing higher bits.
toBits :: forall v a m. (MonadCircuit v a m, Arithmetic a) => [v] -> Natural -> Natural -> m [v] Source #
Convert an ArithmeticCircuit to bits and return their corresponding variables.
fromBits :: forall a. Natural -> Natural -> forall v m. MonadCircuit v a m => [v] -> m [v] Source #
The inverse of toBits.
class KnownRegisterSize (r :: RegisterSize) where Source #
Methods
Instances
| KnownRegisterSize 'Auto Source # | |
Defined in ZkFold.Symbolic.Data.Combinators Methods | |
| KnownNat n => KnownRegisterSize ('Fixed n) Source # | |
Defined in ZkFold.Symbolic.Data.Combinators Methods | |
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 family NumberOfRegisters (a :: Type) (bits :: Natural) (r :: RegisterSize) :: Natural where ... Source #
Equations
| 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 MaxRegisterSize (a :: Type) (regCount :: Natural) :: Natural where ... Source #
Equations
| MaxRegisterSize a regCount = Div (BitLimit a - MaxAdded regCount) 2 |
numberOfRegisters :: forall a n r. (Finite a, KnownNat n, KnownRegisterSize r) => Natural 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.
expansion :: (MonadCircuit i a 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 m. (KnownNat r, MonadCircuit i a m, Arithmetic a) => Natural -> i -> m [i] Source #
bitsOf :: (MonadCircuit i a 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 m. (KnownNat r, MonadCircuit i a 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 m. (KnownNat r, MonadCircuit i a 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 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 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 m, Representable f, Traversable f) => f i -> m (f i, f i) Source #
isZero :: (MonadCircuit i a m, Representable f, Traversable f) => f i -> m (f i) Source #