Safe Haskell	Safe-Inferred
Language	Haskell2010

ZkFold.Symbolic.Data.UInt

Synopsis

class StrictConv b a where
- strictConv :: b -> a
class StrictNum a where
- strictAdd :: a -> a -> a
- strictSub :: a -> a -> a
- strictMul :: a -> a -> a
data UInt (n :: Natural) a = UInt ![a] !a
toConstant :: ToConstant a b => a -> b
eea :: forall n a. EuclideanDomain (UInt n a) => KnownNat n => AdditiveGroup (UInt n a) => Eq (Bool a) (UInt n a) => Conditional (Bool a) (UInt n a, UInt n a, UInt n a) => UInt n a -> UInt n a -> (UInt n a, UInt n a, UInt n a)

Documentation

class StrictConv b a where Source #

Methods

strictConv :: b -> a Source #

Instances

Instances details

(FromConstant Natural a, Finite a, AdditiveMonoid a, KnownNat n) => StrictConv Natural (UInt n a) Source #
Instance details Defined in ZkFold.Symbolic.Data.UInt Methods strictConv :: Natural -> UInt n a Source #
(Finite (Zp p), KnownNat n) => StrictConv (Zp p) (UInt n (Zp p)) Source #
Instance details Defined in ZkFold.Symbolic.Data.UInt Methods strictConv :: Zp p -> UInt n (Zp p) Source #
(Arithmetic a, KnownNat n, KnownNat (NumberOfBits a), NumberOfBits a <= n) => StrictConv (ArithmeticCircuit a) (UInt n (ArithmeticCircuit a)) Source #
Instance details Defined in ZkFold.Symbolic.Data.UInt Methods strictConv :: ArithmeticCircuit a -> UInt n (ArithmeticCircuit a) Source #

class StrictNum a where Source #

Methods

strictAdd :: a -> a -> a Source #

strictSub :: a -> a -> a Source #

strictMul :: a -> a -> a Source #

Instances

Instances details

(Finite (Zp p), KnownNat n) => StrictNum (UInt n (Zp p)) Source #
Instance details Defined in ZkFold.Symbolic.Data.UInt Methods strictAdd :: UInt n (Zp p) -> UInt n (Zp p) -> UInt n (Zp p) Source # strictSub :: UInt n (Zp p) -> UInt n (Zp p) -> UInt n (Zp p) Source # strictMul :: UInt n (Zp p) -> UInt n (Zp p) -> UInt n (Zp p) Source #
(Arithmetic a, KnownNat n) => StrictNum (UInt n (ArithmeticCircuit a)) Source #
Instance details Defined in ZkFold.Symbolic.Data.UInt Methods strictAdd :: UInt n (ArithmeticCircuit a) -> UInt n (ArithmeticCircuit a) -> UInt n (ArithmeticCircuit a) Source # strictSub :: UInt n (ArithmeticCircuit a) -> UInt n (ArithmeticCircuit a) -> UInt n (ArithmeticCircuit a) Source # strictMul :: UInt n (ArithmeticCircuit a) -> UInt n (ArithmeticCircuit a) -> UInt n (ArithmeticCircuit a) Source #

data UInt (n :: Natural) a Source #

Constructors

UInt ![a] !a

Instances

Instances details

(FromConstant Natural a, Finite a, AdditiveMonoid a, KnownNat n) => FromConstant Integer (UInt n a) Source #
Instance details Defined in ZkFold.Symbolic.Data.UInt Methods fromConstant :: Integer -> UInt n a Source #
(FromConstant Natural a, Finite a, AdditiveMonoid a, KnownNat n) => FromConstant Natural (UInt n a) Source #
Instance details Defined in ZkFold.Symbolic.Data.UInt Methods fromConstant :: Natural -> UInt n a Source #
(FromConstant Natural a, Finite a, AdditiveMonoid a, KnownNat n, MultiplicativeSemigroup (UInt n a)) => Scale Integer (UInt n a) Source #
Instance details Defined in ZkFold.Symbolic.Data.UInt Methods scale :: Integer -> UInt n a -> UInt n a Source #
(FromConstant Natural a, Finite a, AdditiveMonoid a, KnownNat n, MultiplicativeSemigroup (UInt n a)) => Scale Natural (UInt n a) Source #
Instance details Defined in ZkFold.Symbolic.Data.UInt Methods scale :: Natural -> UInt n a -> UInt n a Source #
(Arithmetic a, KnownNat n) => SymbolicData a (UInt n (ArithmeticCircuit a)) Source #
Instance details Defined in ZkFold.Symbolic.Data.UInt Methods pieces :: UInt n (ArithmeticCircuit a) -> [ArithmeticCircuit a] Source # restore :: [ArithmeticCircuit a] -> UInt n (ArithmeticCircuit a) Source # typeSize :: Natural Source #
(FromConstant Natural a, Finite a, AdditiveMonoid a, KnownNat n) => StrictConv Natural (UInt n a) Source #
Instance details Defined in ZkFold.Symbolic.Data.UInt Methods strictConv :: Natural -> UInt n a Source #
(Finite (Zp p), KnownNat n) => Eq (Bool (Zp p)) (UInt n (Zp p)) Source #
Instance details Defined in ZkFold.Symbolic.Data.UInt Methods (==) :: UInt n (Zp p) -> UInt n (Zp p) -> Bool (Zp p) Source # (/=) :: UInt n (Zp p) -> UInt n (Zp p) -> Bool (Zp p) Source #
(Arithmetic a, KnownNat n) => Eq (Bool (ArithmeticCircuit a)) (UInt n (ArithmeticCircuit a)) Source #
Instance details Defined in ZkFold.Symbolic.Data.UInt Methods (==) :: UInt n (ArithmeticCircuit a) -> UInt n (ArithmeticCircuit a) -> Bool (ArithmeticCircuit a) Source # (/=) :: UInt n (ArithmeticCircuit a) -> UInt n (ArithmeticCircuit a) -> Bool (ArithmeticCircuit a) Source #
(Finite (Zp p), KnownNat n) => Ord (Bool (Zp p)) (UInt n (Zp p)) Source #
Instance details Defined in ZkFold.Symbolic.Data.UInt Methods (<=) :: UInt n (Zp p) -> UInt n (Zp p) -> Bool (Zp p) Source # (<) :: UInt n (Zp p) -> UInt n (Zp p) -> Bool (Zp p) Source # (>=) :: UInt n (Zp p) -> UInt n (Zp p) -> Bool (Zp p) Source # (>) :: UInt n (Zp p) -> UInt n (Zp p) -> Bool (Zp p) Source # max :: UInt n (Zp p) -> UInt n (Zp p) -> UInt n (Zp p) Source # min :: UInt n (Zp p) -> UInt n (Zp p) -> UInt n (Zp p) Source #
(Arithmetic a, KnownNat n) => Ord (Bool (ArithmeticCircuit a)) (UInt n (ArithmeticCircuit a)) Source #
Instance details Defined in ZkFold.Symbolic.Data.UInt Methods (<=) :: UInt n (ArithmeticCircuit a) -> UInt n (ArithmeticCircuit a) -> Bool (ArithmeticCircuit a) Source # (<) :: UInt n (ArithmeticCircuit a) -> UInt n (ArithmeticCircuit a) -> Bool (ArithmeticCircuit a) Source # (>=) :: UInt n (ArithmeticCircuit a) -> UInt n (ArithmeticCircuit a) -> Bool (ArithmeticCircuit a) Source # (>) :: UInt n (ArithmeticCircuit a) -> UInt n (ArithmeticCircuit a) -> Bool (ArithmeticCircuit a) Source # max :: UInt n (ArithmeticCircuit a) -> UInt n (ArithmeticCircuit a) -> UInt n (ArithmeticCircuit a) Source # min :: UInt n (ArithmeticCircuit a) -> UInt n (ArithmeticCircuit a) -> UInt n (ArithmeticCircuit a) Source #
(Finite (Zp p), KnownNat n) => StrictConv (Zp p) (UInt n (Zp p)) Source #
Instance details Defined in ZkFold.Symbolic.Data.UInt Methods strictConv :: Zp p -> UInt n (Zp p) Source #
(Arithmetic a, KnownNat n, KnownNat (NumberOfBits a), NumberOfBits a <= n) => StrictConv (ArithmeticCircuit a) (UInt n (ArithmeticCircuit a)) Source #
Instance details Defined in ZkFold.Symbolic.Data.UInt Methods strictConv :: ArithmeticCircuit a -> UInt n (ArithmeticCircuit a) Source #
(Finite (Zp p), KnownNat n) => Arbitrary (UInt n (Zp p)) Source #
Instance details Defined in ZkFold.Symbolic.Data.UInt Methods arbitrary :: Gen (UInt n (Zp p)) # shrink :: UInt n (Zp p) -> [UInt n (Zp p)] #
(Arithmetic a, KnownNat n) => Arbitrary (UInt n (ArithmeticCircuit a)) Source #
Instance details Defined in ZkFold.Symbolic.Data.UInt Methods arbitrary :: Gen (UInt n (ArithmeticCircuit a)) # shrink :: UInt n (ArithmeticCircuit a) -> [UInt n (ArithmeticCircuit a)] #
Generic (UInt n a) Source #
Instance details Defined in ZkFold.Symbolic.Data.UInt Associated Types type Rep (UInt n a) :: Type -> Type # Methods from :: UInt n a -> Rep (UInt n a) x # to :: Rep (UInt n a) x -> UInt n a #
Show a => Show (UInt n a) Source #
Instance details Defined in ZkFold.Symbolic.Data.UInt Methods showsPrec :: Int -> UInt n a -> ShowS # show :: UInt n a -> String # showList :: [UInt n a] -> ShowS #
NFData a => NFData (UInt n a) Source #
Instance details Defined in ZkFold.Symbolic.Data.UInt Methods rnf :: UInt n a -> () #
Eq a => Eq (UInt n a) Source #
Instance details Defined in ZkFold.Symbolic.Data.UInt Methods (==) :: UInt n a -> UInt n a -> Bool # (/=) :: UInt n a -> UInt n a -> Bool #
(Finite (Zp p), KnownNat n) => AdditiveGroup (UInt n (Zp p)) Source #
Instance details Defined in ZkFold.Symbolic.Data.UInt Methods (-) :: UInt n (Zp p) -> UInt n (Zp p) -> UInt n (Zp p) Source # negate :: UInt n (Zp p) -> UInt n (Zp p) Source #
(Arithmetic a, KnownNat n) => AdditiveGroup (UInt n (ArithmeticCircuit a)) Source #
Instance details Defined in ZkFold.Symbolic.Data.UInt Methods (-) :: UInt n (ArithmeticCircuit a) -> UInt n (ArithmeticCircuit a) -> UInt n (ArithmeticCircuit a) Source # negate :: UInt n (ArithmeticCircuit a) -> UInt n (ArithmeticCircuit a) Source #
(Finite (Zp p), KnownNat n) => AdditiveMonoid (UInt n (Zp p)) Source #
Instance details Defined in ZkFold.Symbolic.Data.UInt Methods zero :: UInt n (Zp p) Source #
(Arithmetic a, KnownNat n) => AdditiveMonoid (UInt n (ArithmeticCircuit a)) Source #
Instance details Defined in ZkFold.Symbolic.Data.UInt Methods zero :: UInt n (ArithmeticCircuit a) Source #
(Finite (Zp p), KnownNat n) => AdditiveSemigroup (UInt n (Zp p)) Source #
Instance details Defined in ZkFold.Symbolic.Data.UInt Methods (+) :: UInt n (Zp p) -> UInt n (Zp p) -> UInt n (Zp p) Source #
(Arithmetic a, KnownNat n) => AdditiveSemigroup (UInt n (ArithmeticCircuit a)) Source #
Instance details Defined in ZkFold.Symbolic.Data.UInt Methods (+) :: UInt n (ArithmeticCircuit a) -> UInt n (ArithmeticCircuit a) -> UInt n (ArithmeticCircuit a) Source #
(Finite (Zp p), KnownNat n) => EuclideanDomain (UInt n (Zp p)) Source #
Instance details Defined in ZkFold.Symbolic.Data.UInt Methods divMod :: UInt n (Zp p) -> UInt n (Zp p) -> (UInt n (Zp p), UInt n (Zp p)) Source # div :: UInt n (Zp p) -> UInt n (Zp p) -> UInt n (Zp p) Source # mod :: UInt n (Zp p) -> UInt n (Zp p) -> UInt n (Zp p) Source #
(Arithmetic a, KnownNat n) => EuclideanDomain (UInt n (ArithmeticCircuit a)) Source #
Instance details Defined in ZkFold.Symbolic.Data.UInt Methods 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 #
(Finite (Zp p), KnownNat n) => MultiplicativeMonoid (UInt n (Zp p)) Source #
Instance details Defined in ZkFold.Symbolic.Data.UInt Methods one :: UInt n (Zp p) Source #
(Arithmetic a, KnownNat n) => MultiplicativeMonoid (UInt n (ArithmeticCircuit a)) Source #
Instance details Defined in ZkFold.Symbolic.Data.UInt Methods one :: UInt n (ArithmeticCircuit a) Source #
(Finite (Zp p), KnownNat n) => MultiplicativeSemigroup (UInt n (Zp p)) Source #
Instance details Defined in ZkFold.Symbolic.Data.UInt Methods (*) :: UInt n (Zp p) -> UInt n (Zp p) -> UInt n (Zp p) Source #
(Arithmetic a, KnownNat n) => MultiplicativeSemigroup (UInt n (ArithmeticCircuit a)) Source #
Instance details Defined in ZkFold.Symbolic.Data.UInt Methods (*) :: UInt n (ArithmeticCircuit a) -> UInt n (ArithmeticCircuit a) -> UInt n (ArithmeticCircuit a) Source #
(Finite (Zp p), KnownNat n) => Ring (UInt n (Zp p)) Source #
Instance details Defined in ZkFold.Symbolic.Data.UInt
(Arithmetic a, KnownNat n) => Ring (UInt n (ArithmeticCircuit a)) Source #
Instance details Defined in ZkFold.Symbolic.Data.UInt
(Finite (Zp p), KnownNat n) => Semiring (UInt n (Zp p)) Source #
Instance details Defined in ZkFold.Symbolic.Data.UInt
(Arithmetic a, KnownNat n) => Semiring (UInt n (ArithmeticCircuit a)) Source #
Instance details Defined in ZkFold.Symbolic.Data.UInt
(Finite (Zp p), KnownNat n) => StrictNum (UInt n (Zp p)) Source #
Instance details Defined in ZkFold.Symbolic.Data.UInt Methods strictAdd :: UInt n (Zp p) -> UInt n (Zp p) -> UInt n (Zp p) Source # strictSub :: UInt n (Zp p) -> UInt n (Zp p) -> UInt n (Zp p) Source # strictMul :: UInt n (Zp p) -> UInt n (Zp p) -> UInt n (Zp p) Source #
(Arithmetic a, KnownNat n) => StrictNum (UInt n (ArithmeticCircuit a)) Source #
Instance details Defined in ZkFold.Symbolic.Data.UInt Methods strictAdd :: UInt n (ArithmeticCircuit a) -> UInt n (ArithmeticCircuit a) -> UInt n (ArithmeticCircuit a) Source # strictSub :: UInt n (ArithmeticCircuit a) -> UInt n (ArithmeticCircuit a) -> UInt n (ArithmeticCircuit a) Source # strictMul :: UInt n (ArithmeticCircuit a) -> UInt n (ArithmeticCircuit a) -> UInt n (ArithmeticCircuit a) Source #
MultiplicativeMonoid (UInt n a) => Exponent (UInt n a) Natural Source #
Instance details Defined in ZkFold.Symbolic.Data.UInt Methods (^) :: UInt n a -> Natural -> UInt n a Source #
(Finite (Zp p), KnownNat n) => ToConstant (UInt n (Zp p)) Integer Source #
Instance details Defined in ZkFold.Symbolic.Data.UInt Methods toConstant :: UInt n (Zp p) -> Integer Source #
(Finite (Zp p), KnownNat n) => ToConstant (UInt n (Zp p)) Natural Source #
Instance details Defined in ZkFold.Symbolic.Data.UInt Methods toConstant :: UInt n (Zp p) -> Natural Source #
(Finite (Zp p), KnownNat n, KnownNat m, n <= m) => Extend (UInt n (Zp p)) (UInt m (Zp p)) Source #
Instance details Defined in ZkFold.Symbolic.Data.UInt Methods extend :: UInt n (Zp p) -> UInt m (Zp p) Source #
(Arithmetic a, KnownNat n, KnownNat m, n <= m) => Extend (UInt n (ArithmeticCircuit a)) (UInt m (ArithmeticCircuit a)) Source #
Instance details Defined in ZkFold.Symbolic.Data.UInt Methods extend :: UInt n (ArithmeticCircuit a) -> UInt m (ArithmeticCircuit a) Source #
(Finite (Zp p), KnownNat n) => Iso (ByteString n (Zp p)) (UInt n (Zp p)) Source #
Instance details Defined in ZkFold.Symbolic.Data.ByteString Methods from :: ByteString n (Zp p) -> UInt n (Zp p) Source #
(Arithmetic a, KnownNat n) => Iso (ByteString n (ArithmeticCircuit a)) (UInt n (ArithmeticCircuit a)) Source #
Instance details Defined in ZkFold.Symbolic.Data.ByteString Methods from :: ByteString n (ArithmeticCircuit a) -> UInt n (ArithmeticCircuit a) Source #
(Finite (Zp p), KnownNat n) => Iso (UInt n (Zp p)) (ByteString n (Zp p)) Source #
Instance details Defined in ZkFold.Symbolic.Data.ByteString Methods from :: UInt n (Zp p) -> ByteString n (Zp p) Source #
(Arithmetic a, KnownNat n) => Iso (UInt n (ArithmeticCircuit a)) (ByteString n (ArithmeticCircuit a)) Source #
Instance details Defined in ZkFold.Symbolic.Data.ByteString Methods from :: UInt n (ArithmeticCircuit a) -> ByteString n (ArithmeticCircuit a) Source #
(Finite (Zp p), KnownNat n, KnownNat m, m <= n) => Shrink (UInt n (Zp p)) (UInt m (Zp p)) Source #
Instance details Defined in ZkFold.Symbolic.Data.UInt Methods shrink :: UInt n (Zp p) -> UInt m (Zp p) Source #
(Arithmetic a, KnownNat n, KnownNat k, k <= n) => Shrink (UInt n (ArithmeticCircuit a)) (UInt k (ArithmeticCircuit a)) Source #
Instance details Defined in ZkFold.Symbolic.Data.UInt Methods shrink :: UInt n (ArithmeticCircuit a) -> UInt k (ArithmeticCircuit a) Source #
type Rep (UInt n a) Source #
Instance details Defined in ZkFold.Symbolic.Data.UInt type Rep (UInt n a) = D1 ('MetaData "UInt" "ZkFold.Symbolic.Data.UInt" "zkfold-base-0.1.0.0-inplace" 'False) (C1 ('MetaCons "UInt" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 [a]) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 a)))

toConstant :: ToConstant a b => a -> b Source #

eea :: forall n a. EuclideanDomain (UInt n a) => KnownNat n => AdditiveGroup (UInt n a) => Eq (Bool a) (UInt n a) => Conditional (Bool a) (UInt n a, UInt n a, UInt n a) => UInt n a -> UInt n a -> (UInt n a, UInt n a, UInt n a) Source #

Extended Euclidean algorithm. Exploits the fact that s_i and t_i change signs in turns on each iteration, so it adjusts the formulas correspondingly and never requires signed arithmetic. (i.e. it calculates x = b - a instead of x = a - b when a - b is negative and changes y - x to y + x on the following iteration) This only affects Bezout coefficients, remainders are calculated without changes as they are always non-negative.

If the algorithm is used to calculate Bezout coefficients, it requires that a and b are coprime, b is not 1 and a is not 0, otherwise the optimisation above is not valid.

If the algorithm is only used to find gcd(a, b) (i.e. s and t will be discarded), a and b can be arbitrary integers.