| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
ZkFold.Symbolic.Data.Combinators
Synopsis
- 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
- 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 Ceil a b = Div ((a + b) - 1) b
- type family GetRegisterSize (a :: Type) (bits :: Natural) (r :: RegisterSize) :: Natural where ...
- 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 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)
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 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.
Instances
| (Symbolic c, KnownNat k, KnownNat n) => Resize (ByteString k c) (ByteString n c) Source # | |
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 # | |
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 #
Instances
| Eq RegisterSize Source # | |
Defined in ZkFold.Symbolic.Data.Combinators | |
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 GetRegisterSize (a :: Type) (bits :: Natural) (r :: RegisterSize) :: Natural where ... Source #
Equations
| GetRegisterSize a bits (Fixed rs) = rs | |
| GetRegisterSize a bits Auto = Ceil bits (NumberOfRegisters a bits Auto) |
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 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 #