Safe Haskell | Safe-Inferred |
---|---|
Language | Haskell2010 |
Synopsis
- class FromConstant a b where
- fromConstant :: a -> b
- class ToConstant a b where
- toConstant :: a -> b
- class MultiplicativeSemigroup a where
- (*) :: a -> a -> a
- product1 :: (Foldable t, MultiplicativeSemigroup a) => t a -> a
- class MultiplicativeSemigroup b => Exponent a b where
- (^) :: a -> b -> a
- class (MultiplicativeSemigroup a, Exponent a Natural) => MultiplicativeMonoid a where
- one :: a
- natPow :: MultiplicativeMonoid a => a -> Natural -> a
- product :: (Foldable t, MultiplicativeMonoid a) => t a -> a
- multiExp :: (MultiplicativeMonoid a, Exponent a b, Foldable t) => a -> t b -> a
- class MultiplicativeMonoid b => Scale b a where
- scale :: b -> a -> a
- class (MultiplicativeMonoid a, Exponent a Integer) => MultiplicativeGroup a where
- intPow :: MultiplicativeGroup a => a -> Integer -> a
- class AdditiveSemigroup a where
- (+) :: a -> a -> a
- class (AdditiveSemigroup a, Scale Natural a) => AdditiveMonoid a where
- zero :: a
- natScale :: AdditiveMonoid a => Natural -> a -> a
- sum :: (Foldable t, AdditiveMonoid a) => t a -> a
- class (AdditiveMonoid a, Scale Integer a) => AdditiveGroup a where
- intScale :: AdditiveGroup a => Integer -> a -> a
- class (AdditiveMonoid a, MultiplicativeMonoid a, FromConstant Natural a) => Semiring a
- class Semiring a => EuclideanDomain a where
- class (Semiring a, AdditiveGroup a, FromConstant Integer a) => Ring a
- type Algebra b a = (Ring a, Scale b a, FromConstant b a)
- class (Ring a, Exponent a Integer) => Field a where
- (//) :: a -> a -> a
- finv :: a -> a
- rootOfUnity :: Natural -> Maybe a
- intPowF :: Field a => a -> Integer -> a
- class (KnownNat (Order a), KnownNat (NumberOfBits a)) => Finite (a :: Type) where
- order :: forall a. Finite a => Natural
- type NumberOfBits a = Log2 (Order a - 1) + 1
- numberOfBits :: forall a. KnownNat (NumberOfBits a) => Natural
- type FiniteAdditiveGroup a = (Finite a, AdditiveGroup a)
- type FiniteMultiplicativeGroup a = (Finite a, MultiplicativeGroup a)
- type FiniteField a = (Finite a, Field a)
- type PrimeField a = (FiniteField a, Prime (Order a))
- class Field a => DiscreteField' a where
- equal :: a -> a -> a
- class DiscreteField' a => TrichotomyField a where
- trichotomy :: a -> a -> a
- class Semiring a => BinaryExpansion a where
- binaryExpansion :: a -> [a]
- fromBinary :: [a] -> a
- padBits :: forall a. BinaryExpansion a => Natural -> [a] -> [a]
- castBits :: (Semiring a, Eq a, Semiring b) => [a] -> [b]
- newtype NonZero a = NonZero a
- (-!) :: Natural -> Natural -> Natural
Documentation
class FromConstant a b where Source #
Every algebraic structure has a handful of "constant types" related with it: natural numbers, integers, field of constants etc. This typeclass captures this relation.
fromConstant :: a -> b Source #
Builds an element of an algebraic structure from a constant.
fromConstant
should preserve algebraic structure, e.g. if both the
structure and the type of constants are additive monoids, the following
should hold:
- Homomorphism
fromConstant (c + d) == fromConstant c + fromConstant d
Instances
class ToConstant a b where Source #
toConstant :: a -> b Source #
Instances
ToConstant a a Source # | |
Defined in ZkFold.Base.Algebra.Basic.Class toConstant :: a -> a Source # | |
ToConstant (Zp p) Natural Source # | |
Defined in ZkFold.Base.Algebra.Basic.Field toConstant :: Zp p -> Natural Source # | |
ToConstant a Natural => ToConstant (ByteString n a) Natural Source # | |
Defined in ZkFold.Symbolic.Data.ByteString toConstant :: ByteString n a -> Natural Source # | |
(Finite (Zp p), KnownNat n) => ToConstant (UInt n (Zp p)) Integer Source # | |
Defined in ZkFold.Symbolic.Data.UInt | |
(Finite (Zp p), KnownNat n) => ToConstant (UInt n (Zp p)) Natural Source # | |
Defined in ZkFold.Symbolic.Data.UInt |
class MultiplicativeSemigroup a where Source #
A class of types with a binary associative operation with a multiplicative feel to it. Not necessarily commutative.
(*) :: a -> a -> a infixl 7 Source #
A binary associative operation. The following should hold:
- Associativity
x * (y * z) == (x * y) * z
Instances
product1 :: (Foldable t, MultiplicativeSemigroup a) => t a -> a Source #
class MultiplicativeSemigroup b => Exponent a b where Source #
A class for semigroup (and monoid) actions on types where exponential notation is the most natural (including an exponentiation itself).
A right semigroup action on a type. The following should hold:
- Compatibility
a ^ (m * n) == (a ^ m) ^ n
If exponents form a monoid, the following should also hold:
- Right identity
a ^ one == a
NOTE, however, that even if exponents form a semigroup, left
distributivity (that a ^ (m + n) == (a ^ m) * (a ^ n)
) is desirable but
not required: otherwise instance for Bool as exponent could not be made
lawful.
Instances
class (MultiplicativeSemigroup a, Exponent a Natural) => MultiplicativeMonoid a where Source #
A class of types with a binary associative operation with a multiplicative feel to it and an identity element. Not necessarily commutative.
While exponentiation by a natural is specified as a constraint, a default
implementation is provided as a
function. You can provide a faster
alternative, but do not forget to check that it satisfies the following
(in addition to the properties already stated in natPow
documentation):Exponent
- Left identity
one ^ n == one
- Absorption
a ^ 0 == one
- Left distributivity
a ^ (m + n) == (a ^ m) * (a ^ n)
Finally, if the base monoid operation is commutative, power should
distribute over (
:MultiplicativeSemigroup
)
- Right distributivity
(a * b) ^ n == (a ^ n) * (b ^ n)
An identity with respect to multiplication:
- Left identity
one * x == x
- Right identity
x * one == x
Instances
natPow :: MultiplicativeMonoid a => a -> Natural -> a Source #
A default implementation for natural exponentiation. Uses only (
and
MultiplicativeSemigroup
)
so doesn't loop via an one
instance.Exponent
Natural a
product :: (Foldable t, MultiplicativeMonoid a) => t a -> a Source #
class MultiplicativeMonoid b => Scale b a where Source #
A class for monoid actions where multiplicative notation is the most natural (including multiplication by constant itself).
Nothing
A left monoid action on a type. Should satisfy the following:
- Compatibility
scale (c * d) a == scale c (scale d a)
- Left identity
scale one a == a
If, in addition, a cast from constant is defined, they should agree:
- Scale agrees
scale c a == fromConstant c * a
- Cast agrees
fromConstant c == scale c one
If the action is on an abelian structure, scaling should respect it:
- Left distributivity
scale c (a + b) == scale c a + scale c b
- Right absorption
scale c zero == zero
If, in addition, the scaling itself is abelian, this structure should propagate:
- Right distributivity
scale (c + d) a == scale c a + scale d a
- Left absorption
scale zero a == zero
The default implementation is the multiplication by a constant.
default scale :: (FromConstant b a, MultiplicativeSemigroup a) => b -> a -> a Source #
Instances
class (MultiplicativeMonoid a, Exponent a Integer) => MultiplicativeGroup a where Source #
A class of groups in a multiplicative notation.
While exponentiation by an integer is specified in a constraint, a default
implementation is provided as an
function. You can provide a faster
alternative yourself, but do not forget to check that your implementation
computes the same results on all inputs.intPow
(/) :: a -> a -> a infixl 7 Source #
Division in a group. The following should hold:
- Division
x / x == one
- Cancellation
(y / x) * x == y
- Agreement
x / y == x * invert y
Inverse in a group. The following should hold:
- Left inverse
invert x * x == one
- Right inverse
x * invert x == one
- Agreement
invert x == one / x
Instances
MultiplicativeGroup BLS12_381_GT Source # | |
Defined in ZkFold.Base.Algebra.EllipticCurve.BLS12_381 (/) :: BLS12_381_GT -> BLS12_381_GT -> BLS12_381_GT Source # invert :: BLS12_381_GT -> BLS12_381_GT Source # | |
MultiplicativeGroup Bool Source # | |
Field a => MultiplicativeGroup (NonZero a) Source # | |
MultiplicativeGroup a => MultiplicativeGroup [a] Source # | |
MultiplicativeGroup a => MultiplicativeGroup (p -> a) Source # | |
Ord i => MultiplicativeGroup (Sources a i) Source # | |
(Monomial i j, Ring j) => MultiplicativeGroup (M i j (Map i j)) Source # | |
intPow :: MultiplicativeGroup a => a -> Integer -> a Source #
class AdditiveSemigroup a where Source #
A class of types with a binary associative, commutative operation.
(+) :: a -> a -> a infixl 6 Source #
A binary associative commutative operation. The following should hold:
- Associativity
x + (y + z) == (x + y) + z
- Commutativity
x + y == y + x
Instances
class (AdditiveSemigroup a, Scale Natural a) => AdditiveMonoid a where Source #
A class of types with a binary associative, commutative operation and with an identity element.
While scaling by a natural is specified as a constraint, a default
implementation is provided as a
function.natScale
Instances
natScale :: AdditiveMonoid a => Natural -> a -> a Source #
A default implementation for natural scaling. Uses only (
and
AdditiveSemigroup
)
so doesn't loop via a zero
instance.Scale
Natural a
sum :: (Foldable t, AdditiveMonoid a) => t a -> a Source #
class (AdditiveMonoid a, Scale Integer a) => AdditiveGroup a where Source #
A class of abelian groups.
While scaling by an integer is specified in a constraint, a default
implementation is provided as an
function.intScale
(-) :: a -> a -> a infixl 6 Source #
Subtraction in an abelian group. The following should hold:
- Subtraction
x - x == zero
- Agreement
x - y == x + negate y
Inverse in an abelian group. The following should hold:
- Negative
x + negate x == zero
- Agreement
negate x == zero - x
Instances
intScale :: AdditiveGroup a => Integer -> a -> a Source #
class (AdditiveMonoid a, MultiplicativeMonoid a, FromConstant Natural a) => Semiring a Source #
Class of semirings with both 0 and 1. The following should hold:
- Left distributivity
a * (b + c) == a * b + a * c
- Right distributivity
(a + b) * c == a * c + b * c
Instances
class Semiring a => EuclideanDomain a where Source #
A Euclidean domain R
is an integral domain which can be endowed
with at least one function f : R{0} -> R+
s.t.
If a
and b
are in R
and b
is nonzero, then there exist q
and r
in R
such that
a = bq + r
and either r = 0
or f(r) < f(b)
.
q
and r
are called respectively a quotient and a remainder of the division (or Euclidean division) of a
by b
.
The function divMod
associated with this class produces q
and r
given a
and b
.
Instances
EuclideanDomain Integer Source # | |
EuclideanDomain Natural Source # | |
KnownNat p => EuclideanDomain (Zp p) Source # | |
(Finite (Zp p), KnownNat n) => EuclideanDomain (UInt n (Zp p)) Source # | |
(Arithmetic a, KnownNat n) => EuclideanDomain (UInt n (ArithmeticCircuit a)) Source # | |
Defined in ZkFold.Symbolic.Data.UInt divMod :: UInt n (ArithmeticCircuit a) -> UInt n (ArithmeticCircuit a) -> (UInt n (ArithmeticCircuit a), UInt n (ArithmeticCircuit a)) Source # div :: UInt n (ArithmeticCircuit a) -> UInt n (ArithmeticCircuit a) -> UInt n (ArithmeticCircuit a) Source # mod :: UInt n (ArithmeticCircuit a) -> UInt n (ArithmeticCircuit a) -> UInt n (ArithmeticCircuit a) Source # |
class (Semiring a, AdditiveGroup a, FromConstant Integer a) => Ring a Source #
Class of rings with both 0, 1 and additive inverses. The following should hold:
- Left distributivity
a * (b - c) == a * b - a * c
- Right distributivity
(a - b) * c == a * c - b * c
Instances
Ring Integer Source # | |
Defined in ZkFold.Base.Algebra.Basic.Class | |
Ring Bool Source # | |
Defined in ZkFold.Base.Algebra.Basic.Class | |
KnownNat p => Ring (Zp p) Source # | |
Defined in ZkFold.Base.Algebra.Basic.Field | |
Arithmetic a => Ring (ArithmeticCircuit a) Source # | |
Ring a => Ring [a] Source # | |
Defined in ZkFold.Base.Algebra.Basic.Class | |
(Field f, Eq f, IrreduciblePoly f e) => Ring (Ext2 f e) Source # | |
Defined in ZkFold.Base.Algebra.Basic.Field | |
(Field f, Eq f, IrreduciblePoly f e) => Ring (Ext3 f e) Source # | |
Defined in ZkFold.Base.Algebra.Basic.Field | |
(Finite (Zp p), KnownNat n) => Ring (UInt n (Zp p)) Source # | |
Defined in ZkFold.Symbolic.Data.UInt | |
(Arithmetic a, KnownNat n) => Ring (UInt n (ArithmeticCircuit a)) Source # | |
Defined in ZkFold.Symbolic.Data.UInt | |
Ring a => Ring (p -> a) Source # | |
Defined in ZkFold.Base.Algebra.Basic.Class | |
Ord i => Ring (Sources a i) Source # | |
Defined in ZkFold.Base.Algebra.Basic.Sources |
type Algebra b a = (Ring a, Scale b a, FromConstant b a) Source #
Type of modules/algebras over the base type of constants b
. As all the
required laws are implied by the constraints, this is simply an alias rather
than a typeclass in its own right.
Note the following useful facts:
class (Ring a, Exponent a Integer) => Field a where Source #
Class of fields. As a ring, each field is commutative, that is:
- Commutativity
x * y == y * x
While exponentiation by an integer is specified in a constraint, a default
implementation is provided as an
function. You can provide a faster
alternative yourself, but do not forget to check that your implementation
computes the same results on all inputs.intPowF
Division in a field. The following should hold:
- Division
- If
x /= 0
,x // x == one
- Div by 0
x // zero == zero
- Agreement
x // y == x * finv y
Inverse in a field. The following should hold:
- Inverse
- If
x /= 0
,x * inverse x == one
- Inv of 0
inverse zero == zero
- Agreement
finv x == one // x
rootOfUnity :: Natural -> Maybe a Source #
rootOfUnity n
is an element of a characteristic 2^n
, that is,
- Root of 0
rootOfUnity 0 == Just one
- Root property
- If
rootOfUnity n == Just x
,x ^ (2 ^ n) == one
- Smallest root
- If
rootOfUnity n == Just x
andm < n
,x ^ (2 ^ m) /= one
- All roots
- If
rootOfUnity n == Just x
andm < n
,rootOfUnity m /= Nothing
Instances
Prime p => Field (Zp p) Source # | |
Arithmetic a => Field (ArithmeticCircuit a) Source # | |
Defined in ZkFold.Symbolic.Compiler.ArithmeticCircuit.Instance (//) :: ArithmeticCircuit a -> ArithmeticCircuit a -> ArithmeticCircuit a Source # finv :: ArithmeticCircuit a -> ArithmeticCircuit a Source # rootOfUnity :: Natural -> Maybe (ArithmeticCircuit a) Source # | |
(Field f, Eq f, IrreduciblePoly f e) => Field (Ext2 f e) Source # | |
(Field f, Eq f, IrreduciblePoly f e) => Field (Ext3 f e) Source # | |
Ord i => Field (Sources a i) Source # | |
class (KnownNat (Order a), KnownNat (NumberOfBits a)) => Finite (a :: Type) Source #
Class of finite structures. Order a
should be the actual number of
elements in the type, identified up to the associated equality relation.
Instances
Finite BLS12_381_GT Source # | |
Defined in ZkFold.Base.Algebra.EllipticCurve.BLS12_381 type Order BLS12_381_GT :: Natural Source # | |
(KnownNat (Order (NonZero a)), KnownNat (NumberOfBits (NonZero a))) => Finite (NonZero a) Source # | |
(KnownNat p, KnownNat (NumberOfBits (Zp p))) => Finite (Zp p) Source # | |
FiniteField a => Finite (ArithmeticCircuit a) Source # | |
Defined in ZkFold.Symbolic.Compiler.ArithmeticCircuit.Instance type Order (ArithmeticCircuit a) :: Natural Source # | |
(KnownNat (Order (Ext2 f e)), KnownNat (NumberOfBits (Ext2 f e))) => Finite (Ext2 f e) Source # | |
(KnownNat (Order (Ext3 f e)), KnownNat (NumberOfBits (Ext3 f e))) => Finite (Ext3 f e) Source # | |
Finite a => Finite (Sources a i) Source # | |
numberOfBits :: forall a. KnownNat (NumberOfBits a) => Natural Source #
type FiniteAdditiveGroup a = (Finite a, AdditiveGroup a) Source #
type FiniteMultiplicativeGroup a = (Finite a, MultiplicativeGroup a) Source #
type FiniteField a = (Finite a, Field a) Source #
type PrimeField a = (FiniteField a, Prime (Order a)) Source #
class Field a => DiscreteField' a where Source #
A field is a commutative ring in which an element is invertible if and only if it is nonzero. In a discrete field an element is invertible xor it equals zero. That is equivalent in classical logic but stronger in constructive logic. Every element is either 0 or invertible, and 0 ≠ 1.
We represent a discrete field as a field with an
internal equality function which returns one
for equal field elements and zero
for distinct field elements.
Nothing
Instances
Prime p => DiscreteField' (Zp p) Source # | |
Arithmetic a => DiscreteField' (ArithmeticCircuit a) Source # | |
Defined in ZkFold.Symbolic.Compiler.ArithmeticCircuit.Instance equal :: ArithmeticCircuit a -> ArithmeticCircuit a -> ArithmeticCircuit a Source # |
class DiscreteField' a => TrichotomyField a where Source #
An ordering of a field is usually required to have compatibility laws with
respect to addition and multiplication. However, we can drop that requirement and
define a trichotomy field as one with an internal total ordering.
We represent a trichotomy field as a discrete field with an internal comparison of
field elements returning negate
one
for <, zero
for =, and one
for >. The law of trichotomy is that for any two field elements, exactly one
of the relations =, or holds. Thus we require that -1, 0 and 1 are distinct
field elements.
equal a b = one - (trichotomy a b)^2
Nothing
trichotomy :: a -> a -> a Source #
default trichotomy :: Ord a => a -> a -> a Source #
Instances
Prime p => TrichotomyField (Zp p) Source # | |
Defined in ZkFold.Base.Algebra.Basic.Field | |
Arithmetic a => TrichotomyField (ArithmeticCircuit a) Source # | |
Defined in ZkFold.Symbolic.Compiler.ArithmeticCircuit.Instance trichotomy :: ArithmeticCircuit a -> ArithmeticCircuit a -> ArithmeticCircuit a Source # |
class Semiring a => BinaryExpansion a where Source #
Class of semirings where a binary expansion of elements can be computed. Note: numbers should convert to Little-endian bit representation.
The following should hold:
fromBinary . binaryExpansion == id
fromBinary xs == foldr (x y -> x + y + y) zero xs
binaryExpansion :: a -> [a] Source #
fromBinary :: [a] -> a Source #
Instances
BinaryExpansion Natural Source # | |
Defined in ZkFold.Base.Algebra.Basic.Class binaryExpansion :: Natural -> [Natural] Source # fromBinary :: [Natural] -> Natural Source # | |
BinaryExpansion Bool Source # | |
Defined in ZkFold.Base.Algebra.Basic.Class binaryExpansion :: Bool -> [Bool] Source # fromBinary :: [Bool] -> Bool Source # | |
Prime p => BinaryExpansion (Zp p) Source # | |
Defined in ZkFold.Base.Algebra.Basic.Field binaryExpansion :: Zp p -> [Zp p] Source # fromBinary :: [Zp p] -> Zp p Source # | |
Arithmetic a => BinaryExpansion (ArithmeticCircuit a) Source # | |
Defined in ZkFold.Symbolic.Compiler.ArithmeticCircuit.Instance binaryExpansion :: ArithmeticCircuit a -> [ArithmeticCircuit a] Source # fromBinary :: [ArithmeticCircuit a] -> ArithmeticCircuit a Source # | |
(Finite a, Ord i) => BinaryExpansion (Sources a i) Source # | |
Defined in ZkFold.Base.Algebra.Basic.Sources binaryExpansion :: Sources a i -> [Sources a i] Source # fromBinary :: [Sources a i] -> Sources a i Source # |
padBits :: forall a. BinaryExpansion a => Natural -> [a] -> [a] Source #
A multiplicative subgroup of nonzero elements of a field. TODO: hide constructor
NonZero a |
Instances
(KnownNat (Order (NonZero a)), KnownNat (NumberOfBits (NonZero a))) => Finite (NonZero a) Source # | |
Field a => MultiplicativeGroup (NonZero a) Source # | |
MultiplicativeMonoid a => MultiplicativeMonoid (NonZero a) Source # | |
Defined in ZkFold.Base.Algebra.Basic.Class | |
MultiplicativeSemigroup a => MultiplicativeSemigroup (NonZero a) Source # | |
Exponent a b => Exponent (NonZero a) b Source # | |
type Order (NonZero a) Source # | |
Defined in ZkFold.Base.Algebra.Basic.Class |