| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
ZkFold.Base.Algebra.Basic.Class
Synopsis
- class FromConstant a b where
- fromConstant :: a -> b
- class ToConstant a where
- type Const a :: Type
- toConstant :: a -> Const a
- class Scale b a where
- scale :: b -> a -> a
- class (FromConstant a a, Scale a a) => MultiplicativeSemigroup a where
- (*) :: a -> a -> a
- product1 :: (Foldable t, MultiplicativeSemigroup a) => t a -> a
- class 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 a, Exponent a Integer) => MultiplicativeGroup a where
- intPow :: MultiplicativeGroup a => a -> Integer -> a
- class FromConstant a a => 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 => SemiEuclidean 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
- type Bits a :: Type
- binaryExpansion :: a -> Bits a
- fromBinary :: Bits a -> a
- padBits :: forall a. AdditiveMonoid a => Natural -> [a] -> [a]
- castBits :: (Semiring a, Eq a, Semiring b) => [a] -> [b]
- newtype NonZero a = NonZero a
- (-!) :: Natural -> Natural -> Natural
- floorN :: Rational -> 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.
Minimal complete definition
Nothing
Methods
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
default fromConstant :: a ~ b => a -> b Source #
Instances
class ToConstant a where Source #
A class of algebraic structures which can be converted to "constant type" related with it: natural numbers, integers, rationals etc. Subject to the following law:
- Inverse
fromConstant(toConstantx) == x
Associated Types
One of "constant types" related with a.
Typically the smallest type among them by inclusion.
Methods
toConstant :: a -> Const a Source #
A way to turn element of a into a Const aToConstantfromConstant
Instances
class Scale b a where Source #
A class for actions where multiplicative notation is the most natural (including multiplication by constant itself).
Minimal complete definition
Nothing
Methods
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 (FromConstant a a, Scale a a) => MultiplicativeSemigroup a where Source #
A class of types with a binary associative operation with a multiplicative feel to it. Not necessarily commutative.
Methods
(*) :: 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 Exponent a b where Source #
A class for actions on types where exponential notation is the most natural (including an exponentiation itself).
Methods
A right action on a type.
If exponents form a semigroup, 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 natPowExponent
- 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)
Methods
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)oneExponent Natural a
product :: (Foldable t, MultiplicativeMonoid a) => t a -> a Source #
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 intPow
Methods
(/) :: 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 Methods (/) :: BLS12_381_GT -> BLS12_381_GT -> BLS12_381_GT Source # invert :: BLS12_381_GT -> BLS12_381_GT Source # | |
| MultiplicativeGroup BN254_GT Source # | |
| MultiplicativeGroup Bool Source # | |
| Field a => MultiplicativeGroup (NonZero a) Source # | |
| MultiplicativeGroup a => MultiplicativeGroup [a] Source # | |
| (Monomial i j, Ring j) => MultiplicativeGroup (Mono i j) Source # | |
| MultiplicativeGroup a => MultiplicativeGroup (p -> a) Source # | |
intPow :: MultiplicativeGroup a => a -> Integer -> a Source #
class FromConstant a a => AdditiveSemigroup a where Source #
A class of types with a binary associative, commutative operation.
Methods
(+) :: 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 natScale
Instances
natScale :: AdditiveMonoid a => Natural -> a -> a Source #
A default implementation for natural scaling. Uses only ( and
AdditiveSemigroup)zeroScale 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 intScale
Methods
(-) :: 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 => SemiEuclidean a where Source #
A semi-Euclidean-domain a is a semiring without zero divisors which can
be endowed with at least one function f : a{0} -> R+ s.t. if x and y are
in a and y is nonzero, then there exist q and r in a such that
x = qy + r and either r = 0 or f(r) < f(y).
q and r are called respectively a quotient and a remainder of the division
(or Euclidean division) of x by y.
The function divMod associated with this class produces q and r
given a and b.
This is a generalization of a notion of Euclidean domains to semirings.
Instances
| SemiEuclidean Integer Source # | |
| SemiEuclidean Natural Source # | |
| KnownNat p => SemiEuclidean (Zp p) Source # | |
| SemiEuclidean (MerkleHash ('Nothing :: Maybe Natural)) Source # | |
Defined in ZkFold.Symbolic.Compiler.ArithmeticCircuit.MerkleHash Methods divMod :: MerkleHash 'Nothing -> MerkleHash 'Nothing -> (MerkleHash 'Nothing, MerkleHash 'Nothing) Source # div :: MerkleHash 'Nothing -> MerkleHash 'Nothing -> MerkleHash 'Nothing Source # mod :: MerkleHash 'Nothing -> MerkleHash 'Nothing -> MerkleHash 'Nothing Source # | |
| (Symbolic c, KnownNat n, KnownNat r, KnownRegisterSize rs, r ~ NumberOfRegisters (BaseField c) n rs, NFData (c (Vector r))) => SemiEuclidean (UInt n rs c) 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
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 intPowF
Methods
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 xandm < n,x ^ (2 ^ m) /= one - All roots
- If
rootOfUnity n == Just xandm < n,rootOfUnity m /= Nothing
Instances
| Field Rational Source # | |
| Prime p => Field (Zp p) Source # | |
| Field (MerkleHash ('Just n)) Source # | |
Defined in ZkFold.Symbolic.Compiler.ArithmeticCircuit.MerkleHash Methods (//) :: MerkleHash ('Just n) -> MerkleHash ('Just n) -> MerkleHash ('Just n) Source # finv :: MerkleHash ('Just n) -> MerkleHash ('Just n) Source # rootOfUnity :: Natural -> Maybe (MerkleHash ('Just n)) Source # | |
| Symbolic c => Field (FieldElement c) Source # | |
Defined in ZkFold.Symbolic.Data.FieldElement Methods (//) :: FieldElement c -> FieldElement c -> FieldElement c Source # finv :: FieldElement c -> FieldElement c Source # rootOfUnity :: Natural -> Maybe (FieldElement c) 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 # | |
| (Prime p, Symbolic c) => Field (FFA p c) 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 Associated Types type Order BLS12_381_GT :: Natural Source # | |
| Finite BN254_GT Source # | |
| (KnownNat (Order (NonZero a)), KnownNat (NumberOfBits (NonZero a))) => Finite (NonZero a) Source # | |
| (KnownNat p, KnownNat (NumberOfBits (Zp p))) => Finite (Zp p) Source # | |
| Finite (Zp n) => Finite (MerkleHash ('Just n)) Source # | |
| (KnownNat (Order (FieldElement c)), KnownNat (NumberOfBits (FieldElement c))) => Finite (FieldElement c) Source # | |
Defined in ZkFold.Symbolic.Data.FieldElement Associated Types type Order (FieldElement c) :: 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 (Zp p) => Finite (FFA p b) 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.
Minimal complete definition
Nothing
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
Minimal complete definition
Nothing
Instances
| Prime p => TrichotomyField (Zp p) Source # | |
Defined in ZkFold.Base.Algebra.Basic.Field | |
class Semiring a => BinaryExpansion a where Source #
Class of semirings where a binary expansion of elements can be computed.
The methods store binary expansion of a as objects of type b.
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
Minimal complete definition
Instances
| BinaryExpansion Natural Source # | |
| BinaryExpansion Bool Source # | |
| Prime p => BinaryExpansion (Zp p) Source # | |
| Symbolic c => BinaryExpansion (FieldElement c) Source # | |
Defined in ZkFold.Symbolic.Data.FieldElement Associated Types type Bits (FieldElement c) Source # Methods binaryExpansion :: FieldElement c -> Bits (FieldElement c) Source # fromBinary :: Bits (FieldElement c) -> FieldElement c Source # | |
padBits :: forall a. AdditiveMonoid a => Natural -> [a] -> [a] Source #
A multiplicative subgroup of nonzero elements of a field. TODO: hide constructor
Constructors
| 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 | |