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
newtype UInt (n :: Natural) (r :: RegisterSize) (context :: (Type -> Type) -> Type) = UInt (context (Vector (NumberOfRegisters (BaseField context) n r)))
toConstant :: ToConstant a => a -> Const a
eea :: forall n c r. Symbolic c => SemiEuclidean (UInt n r c) => KnownNat n => KnownNat (NumberOfRegisters (BaseField 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

Instances details

(Symbolic c, KnownNat n, KnownRegisterSize rs) => StrictConv Natural (UInt n rs c) Source #
Instance details 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 #
Instance details 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 #
Instance details Defined in ZkFold.Symbolic.Data.UInt Methods strictConv :: c Par1 -> UInt n r c 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

(Symbolic c, KnownNat n, KnownRegisterSize r) => StrictNum (UInt n r c) Source #
Instance details Defined in ZkFold.Symbolic.Data.UInt Methods strictAdd :: UInt n r c -> UInt n r c -> UInt n r c Source # strictSub :: UInt n r c -> UInt n r c -> UInt n r c Source # strictMul :: UInt n r c -> UInt n r c -> 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

Instances details

(Symbolic c, KnownNat n, KnownRegisterSize r) => FromConstant Integer (UInt n r c) Source #
Instance details Defined in ZkFold.Symbolic.Data.UInt Methods fromConstant :: Integer -> UInt n r c Source #
(Symbolic c, KnownNat n, KnownRegisterSize r) => FromConstant Natural (UInt n r c) Source #
Instance details Defined in ZkFold.Symbolic.Data.UInt Methods fromConstant :: Natural -> UInt n r c Source #
(Symbolic c, KnownNat n, KnownRegisterSize r) => Scale Integer (UInt n r c) Source #
Instance details Defined in ZkFold.Symbolic.Data.UInt Methods scale :: Integer -> UInt n r c -> UInt n r c Source #
(Symbolic c, KnownNat n, KnownRegisterSize r) => Scale Natural (UInt n r c) Source #
Instance details Defined in ZkFold.Symbolic.Data.UInt Methods scale :: Natural -> UInt n r c -> UInt n r c Source #
(Symbolic c, KnownNat n, KnownRegisterSize rs) => StrictConv Natural (UInt n rs c) Source #
Instance details Defined in ZkFold.Symbolic.Data.UInt Methods strictConv :: Natural -> UInt n rs c Source #
(Symbolic c, KnownRegisterSize r, NumberOfBits (BaseField c) ~ n) => Iso (FieldElement c) (UInt n r c) Source #
Instance details Defined in ZkFold.Symbolic.Data.UInt Methods from :: FieldElement c -> UInt n r c Source #
(Symbolic c, KnownNat (NumberOfRegisters (BaseField c) n rs)) => Eq (Bool c) (UInt n rs c) Source #
Instance details Defined in ZkFold.Symbolic.Data.UInt Methods (==) :: UInt n rs c -> UInt n rs c -> Bool c Source # (/=) :: UInt n rs c -> UInt n rs c -> Bool c Source #
(Symbolic c, KnownNat n, KnownRegisterSize r, KnownNat (NumberOfRegisters (BaseField c) n r)) => Ord (Bool c) (UInt n r c) Source #
Instance details Defined in ZkFold.Symbolic.Data.UInt Methods (<=) :: UInt n r c -> UInt n r c -> Bool c Source # (<) :: UInt n r c -> UInt n r c -> Bool c Source # (>=) :: UInt n r c -> UInt n r c -> Bool c Source # (>) :: UInt n r c -> UInt n r c -> Bool c Source # max :: UInt n r c -> UInt n r c -> UInt n r c Source # min :: UInt n r c -> UInt n r c -> UInt n r c Source #
(Symbolic c, KnownNat n, KnownRegisterSize r) => StrictConv (Zp p) (UInt n r c) Source #
Instance details 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 #
Instance details Defined in ZkFold.Symbolic.Data.UInt Methods strictConv :: c Par1 -> UInt n r c Source #
(Symbolic c, KnownNat n, KnownRegisterSize r) => Iso (ByteString n c) (UInt n r c) Source #
Instance details Defined in ZkFold.Symbolic.Data.UInt Methods from :: ByteString n c -> UInt n r c Source #
(Symbolic c, KnownNat n, KnownRegisterSize r) => Arbitrary (UInt n r c) Source #
Instance details Defined in ZkFold.Symbolic.Data.UInt Methods arbitrary :: Gen (UInt n r c) # shrink :: UInt n r c -> [UInt n r c] #
(Symbolic c, KnownNat n, KnownRegisterSize r) => FromJSON (UInt n r c) Source #
Instance details Defined in ZkFold.Symbolic.Data.UInt Methods parseJSON :: Value -> Parser (UInt n r c) # parseJSONList :: Value -> Parser [UInt n r c] #
(Symbolic (Interpreter (Zp p)), KnownNat n, KnownRegisterSize r) => ToJSON (UInt n r (Interpreter (Zp p))) Source #
Instance details Defined in ZkFold.Symbolic.Data.UInt Methods toJSON :: UInt n r (Interpreter (Zp p)) -> Value # toEncoding :: UInt n r (Interpreter (Zp p)) -> Encoding # toJSONList :: [UInt n r (Interpreter (Zp p))] -> Value # toEncodingList :: [UInt n r (Interpreter (Zp p))] -> Encoding #
Generic (UInt n r context) Source #
Instance details Defined in ZkFold.Symbolic.Data.UInt Associated Types type Rep (UInt n r context) :: Type -> Type # Methods from :: UInt n r context -> Rep (UInt n r context) x # to :: Rep (UInt n r context) x -> UInt n r context #
(Show (BaseField context), Show (context (Vector (NumberOfRegisters (BaseField context) n r)))) => Show (UInt n r context) Source #
Instance details Defined in ZkFold.Symbolic.Data.UInt Methods showsPrec :: Int -> UInt n r context -> ShowS # show :: UInt n r context -> String # showList :: [UInt n r context] -> ShowS #
NFData (context (Vector (NumberOfRegisters (BaseField context) n r))) => NFData (UInt n r context) Source #
Instance details Defined in ZkFold.Symbolic.Data.UInt Methods rnf :: UInt n r context -> () #
Eq (context (Vector (NumberOfRegisters (BaseField context) n r))) => Eq (UInt n r context) Source #
Instance details Defined in ZkFold.Symbolic.Data.UInt Methods (==) :: UInt n r context -> UInt n r context -> Bool # (/=) :: UInt n r context -> UInt n r context -> Bool #
(Symbolic c, KnownNat n, KnownRegisterSize r) => AdditiveGroup (UInt n r c) Source #
Instance details Defined in ZkFold.Symbolic.Data.UInt Methods (-) :: UInt n r c -> UInt n r c -> UInt n r c Source # negate :: UInt n r c -> UInt n r c Source #
(Symbolic c, KnownNat n, KnownRegisterSize r) => AdditiveMonoid (UInt n r c) Source #
Instance details Defined in ZkFold.Symbolic.Data.UInt Methods zero :: UInt n r c Source #
(Symbolic c, KnownNat n, KnownRegisterSize r) => AdditiveSemigroup (UInt n r c) Source #
Instance details Defined in ZkFold.Symbolic.Data.UInt Methods (+) :: UInt n r c -> UInt n r c -> UInt n r c Source #
(Symbolic c, KnownNat n, KnownRegisterSize r) => MultiplicativeMonoid (UInt n r c) Source #
Instance details Defined in ZkFold.Symbolic.Data.UInt Methods one :: UInt n r c Source #
(Symbolic c, KnownNat n, KnownRegisterSize rs) => MultiplicativeSemigroup (UInt n rs c) Source #
Instance details Defined in ZkFold.Symbolic.Data.UInt Methods (*) :: UInt n rs c -> UInt n rs c -> UInt n rs c Source #
(Symbolic c, KnownNat n, KnownRegisterSize r) => Ring (UInt n r c) Source #
Instance details Defined in ZkFold.Symbolic.Data.UInt
(Symbolic c, KnownNat n, KnownNat r, KnownRegisterSize rs, r ~ NumberOfRegisters (BaseField c) n rs, NFData (c (Vector r))) => SemiEuclidean (UInt n rs c) Source #
Instance details Defined in ZkFold.Symbolic.Data.UInt Methods divMod :: UInt n rs c -> UInt n rs c -> (UInt n rs c, UInt n rs c) Source # div :: UInt n rs c -> UInt n rs c -> UInt n rs c Source # mod :: UInt n rs c -> UInt n rs c -> UInt n rs c Source #
(Symbolic c, KnownNat n, KnownRegisterSize r) => Semiring (UInt n r c) Source #
Instance details Defined in ZkFold.Symbolic.Data.UInt
(Symbolic (Interpreter (Zp p)), KnownNat n, KnownRegisterSize r) => ToConstant (UInt n r (Interpreter (Zp p))) Source #
Instance details Defined in ZkFold.Symbolic.Data.UInt Associated Types type Const (UInt n r (Interpreter (Zp p))) Source # Methods toConstant :: UInt n r (Interpreter (Zp p)) -> Const (UInt n r (Interpreter (Zp p))) Source #
SymbolicData (UInt n r c) Source #
Instance details Defined in ZkFold.Symbolic.Data.UInt Associated Types type Context (UInt n r c) :: (Type -> Type) -> Type Source # type Support (UInt n r c) Source # type Layout (UInt n r c) :: Type -> Type Source # Methods pieces :: UInt n r c -> Support (UInt n r c) -> Context (UInt n r c) (Layout (UInt n r c)) Source # restore :: (Support (UInt n r c) -> Context (UInt n r c) (Layout (UInt n r c))) -> UInt n r c Source #
(Symbolic c, KnownNat n, KnownRegisterSize r, KnownNat (NumberOfRegisters (BaseField c) n r)) => SymbolicInput (UInt n r c) Source #
Instance details Defined in ZkFold.Symbolic.Data.UInt Methods isValid :: UInt n r c -> Bool (Context (UInt n r c)) Source #
(Symbolic c, KnownNat n, KnownRegisterSize r) => StrictNum (UInt n r c) Source #
Instance details Defined in ZkFold.Symbolic.Data.UInt Methods strictAdd :: UInt n r c -> UInt n r c -> UInt n r c Source # strictSub :: UInt n r c -> UInt n r c -> UInt n r c Source # strictMul :: UInt n r c -> UInt n r c -> UInt n r c Source #
MultiplicativeMonoid (UInt n r c) => Exponent (UInt n r c) Natural Source #
Instance details Defined in ZkFold.Symbolic.Data.UInt Methods (^) :: UInt n r c -> Natural -> UInt n r c Source #
(Symbolic c, KnownRegisterSize r, NumberOfBits (BaseField c) ~ n) => Iso (UInt n r c) (FieldElement c) Source #
Instance details Defined in ZkFold.Symbolic.Data.UInt Methods from :: UInt n r c -> FieldElement c Source #
(Symbolic c, KnownNat n, KnownRegisterSize r) => Iso (UInt n r c) (ByteString n c) Source #
Instance details Defined in ZkFold.Symbolic.Data.UInt Methods from :: UInt n r c -> ByteString n c Source #
(Symbolic c, KnownNat n, KnownNat k, KnownRegisterSize r, n <= k) => Extend (UInt n r c) (UInt k r c) Source #
Instance details Defined in ZkFold.Symbolic.Data.UInt Methods extend :: UInt n r c -> UInt k r c Source #
(Symbolic c, KnownNat n, KnownNat k, KnownRegisterSize r, k <= n, from ~ NumberOfRegisters (BaseField c) n r, to ~ NumberOfRegisters (BaseField c) k r) => Shrink (UInt n r c) (UInt k r c) Source #
Instance details Defined in ZkFold.Symbolic.Data.UInt Methods shrink :: UInt n r c -> UInt k r c Source #
type Rep (UInt n r context) Source #
Instance details Defined in ZkFold.Symbolic.Data.UInt type Rep (UInt n r context) = D1 ('MetaData "UInt" "ZkFold.Symbolic.Data.UInt" "symbolic-base-0.1.0.0-inplace" 'True) (C1 ('MetaCons "UInt" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (context (Vector (NumberOfRegisters (BaseField context) n r))))))
type Const (UInt n r (Interpreter (Zp p))) Source #
Instance details Defined in ZkFold.Symbolic.Data.UInt type Const (UInt n r (Interpreter (Zp p))) = Natural
type Context (UInt n r c) Source #
Instance details Defined in ZkFold.Symbolic.Data.UInt type Context (UInt n r c) = Context (c (Vector (NumberOfRegisters (BaseField c) n r)))
type Layout (UInt n r c) Source #
Instance details Defined in ZkFold.Symbolic.Data.UInt type Layout (UInt n r c) = Layout (c (Vector (NumberOfRegisters (BaseField c) n r)))
type Support (UInt n r c) Source #
Instance details Defined in ZkFold.Symbolic.Data.UInt type Support (UInt n r c) = Support (c (Vector (NumberOfRegisters (BaseField c) n r)))

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

A way to turn element of a into a Const a. According to the law of ToConstant, has to be right inverse to fromConstant.

eea :: forall n c r. Symbolic c => SemiEuclidean (UInt n r c) => KnownNat n => KnownNat (NumberOfRegisters (BaseField 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.