| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
ZkFold.Symbolic.Data.UInt
Synopsis
- class StrictConv b a where
- strictConv :: b -> a
- class StrictNum a where
- newtype UInt (n :: Natural) (r :: RegisterSize) (context :: (Type -> Type) -> Type) = UInt (context (Vector (NumberOfRegisters (BaseField context) n r)))
- type OrdWord = 16
- toConstant :: ToConstant a => a -> Const a
- asWords :: forall wordSize regSize ctx k. Symbolic ctx => KnownNat (Ceil regSize wordSize) => KnownNat wordSize => ctx (Vector k) -> ctx (Vector (k * Ceil regSize wordSize))
- expMod :: forall c n p m r. Symbolic c => KnownRegisterSize r => KnownNat p => KnownNat n => KnownNat m => KnownNat (2 * m) => KnownRegisters c (2 * m) r => KnownNat (Ceil (GetRegisterSize (BaseField c) (2 * m) r) OrdWord) => NFData (c (Vector (NumberOfRegisters (BaseField c) (2 * m) r))) => UInt n r c -> UInt p r c -> UInt m r c -> UInt m r c
- eea :: forall n c r. Symbolic c => SemiEuclidean (UInt n r c) => KnownNat n => KnownRegisters c n r => AdditiveGroup (UInt n r c) => Eq (Bool c) (UInt n r c) => UInt n r c -> UInt n r c -> (UInt n r c, UInt n r c, UInt n r c)
Documentation
class StrictConv b a where Source #
Methods
strictConv :: b -> a Source #
Instances
| (Symbolic c, KnownNat n, KnownRegisterSize rs) => StrictConv Natural (UInt n rs c) Source # | |
Defined in ZkFold.Symbolic.Data.UInt Methods strictConv :: Natural -> UInt n rs c Source # | |
| (Symbolic c, KnownNat n, KnownRegisterSize r) => StrictConv (Zp p) (UInt n r c) Source # | |
Defined in ZkFold.Symbolic.Data.UInt Methods strictConv :: Zp p -> UInt n r c Source # | |
| (Symbolic c, KnownNat n, KnownRegisterSize r) => StrictConv (c Par1) (UInt n r c) Source # | |
Defined in ZkFold.Symbolic.Data.UInt Methods strictConv :: c Par1 -> UInt n r c Source # | |
newtype UInt (n :: Natural) (r :: RegisterSize) (context :: (Type -> Type) -> Type) Source #
Constructors
| UInt (context (Vector (NumberOfRegisters (BaseField context) n r))) |
Instances
toConstant :: ToConstant a => a -> Const a Source #
A way to turn element of a into a Const aToConstantfromConstant
asWords :: forall wordSize regSize ctx k. Symbolic ctx => KnownNat (Ceil regSize wordSize) => KnownNat wordSize => ctx (Vector k) -> ctx (Vector (k * Ceil regSize wordSize)) Source #
expMod :: forall c n p m r. Symbolic c => KnownRegisterSize r => KnownNat p => KnownNat n => KnownNat m => KnownNat (2 * m) => KnownRegisters c (2 * m) r => KnownNat (Ceil (GetRegisterSize (BaseField c) (2 * m) r) OrdWord) => NFData (c (Vector (NumberOfRegisters (BaseField c) (2 * m) r))) => UInt n r c -> UInt p r c -> UInt m r c -> UInt m r c Source #
expMod n pow modulus calculates n^pow % modulus where all values are arithmetised
eea :: forall n c r. Symbolic c => SemiEuclidean (UInt n r c) => KnownNat n => KnownRegisters c n r => AdditiveGroup (UInt n r c) => Eq (Bool c) (UInt n r c) => UInt n r c -> UInt n r c -> (UInt n r c, UInt n r c, UInt n r c) 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.