ZkFold.Symbolic.Data.UInt

Documentation

class StrictConv b a where

Methods

strictConv :: b -> a

Instances

(Symbolic c, KnownNat n, KnownRegisterSize rs) => StrictConv Natural (UInt n rs c)

Defined in ZkFold.Symbolic.Data.UInt

Methods

strictConv :: Natural -> UInt n rs c

(Symbolic c, KnownNat n, KnownRegisterSize r) => StrictConv (Zp p) (UInt n r c)

Defined in ZkFold.Symbolic.Data.UInt

Methods

strictConv :: Zp p -> UInt n r c

(Symbolic c, KnownNat n, KnownRegisterSize r) => StrictConv (c Par1) (UInt n r c)

Defined in ZkFold.Symbolic.Data.UInt

Methods

strictConv :: c Par1 -> UInt n r c

class StrictNum a where

Methods

strictAdd :: a -> a -> a

strictSub :: a -> a -> a

strictMul :: a -> a -> a

Instances

(Symbolic c, KnownNat n, KnownRegisterSize r) => StrictNum (UInt n r c)

Defined in ZkFold.Symbolic.Data.UInt

Methods

strictAdd :: UInt n r c -> UInt n r c -> UInt n r c

strictSub :: UInt n r c -> UInt n r c -> UInt n r c

strictMul :: UInt n r c -> UInt n r c -> UInt n r c

newtype UInt (n :: Natural) (r :: RegisterSize) (context :: (Type -> Type) -> Type)

Constructors

UInt (context (Vector (NumberOfRegisters (BaseField context) n r)))

Instances

(Symbolic c, KnownNat n, KnownRegisterSize r) => FromConstant Integer (UInt n r c)

Defined in ZkFold.Symbolic.Data.UInt

Methods

fromConstant :: Integer -> UInt n r c

(Symbolic c, KnownNat n, KnownRegisterSize r) => FromConstant Natural (UInt n r c)

Defined in ZkFold.Symbolic.Data.UInt

Methods

fromConstant :: Natural -> UInt n r c

(Symbolic c, KnownNat n, KnownRegisterSize r) => Scale Integer (UInt n r c)

Defined in ZkFold.Symbolic.Data.UInt

Methods

scale :: Integer -> UInt n r c -> UInt n r c

(Symbolic c, KnownNat n, KnownRegisterSize r) => Scale Natural (UInt n r c)

Defined in ZkFold.Symbolic.Data.UInt

Methods

scale :: Natural -> UInt n r c -> UInt n r c

(Symbolic c, KnownNat n, KnownRegisterSize rs) => StrictConv Natural (UInt n rs c)

Defined in ZkFold.Symbolic.Data.UInt

Methods

strictConv :: Natural -> UInt n rs c

(Symbolic c, KnownRegisterSize r, NumberOfBits (BaseField c) ~ n) => Iso (FieldElement c) (UInt n r c)

Defined in ZkFold.Symbolic.Data.UInt

Methods

from :: FieldElement c -> UInt n r c

(KnownRegisters c n r, Symbolic c) => Conditional (Bool c) (UInt n r c)

Defined in ZkFold.Symbolic.Data.UInt

Methods

bool :: UInt n r c -> UInt n r c -> Bool c -> UInt n r c

(Symbolic c, KnownNat n, KnownRegisterSize r) => StrictConv (Zp p) (UInt n r c)

Defined in ZkFold.Symbolic.Data.UInt

Methods

strictConv :: Zp p -> UInt n r c

(Symbolic c, KnownNat n, KnownRegisterSize r) => StrictConv (c Par1) (UInt n r c)

Defined in ZkFold.Symbolic.Data.UInt

Methods

strictConv :: c Par1 -> UInt n r c

(Symbolic c, KnownNat n, KnownRegisterSize r) => Iso (ByteString n c) (UInt n r c)

Defined in ZkFold.Symbolic.Data.UInt

Methods

from :: ByteString n c -> UInt n r c

(Symbolic c, KnownNat n, KnownRegisterSize r) => Arbitrary (UInt n r c)

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)

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)))

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)

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)

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)

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)

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)

Defined in ZkFold.Symbolic.Data.UInt

Methods

(-) :: UInt n r c -> UInt n r c -> UInt n r c

negate :: UInt n r c -> UInt n r c

(Symbolic c, KnownNat n, KnownRegisterSize r) => AdditiveMonoid (UInt n r c)

Defined in ZkFold.Symbolic.Data.UInt

Methods

zero :: UInt n r c

(Symbolic c, KnownNat n, KnownRegisterSize r) => AdditiveSemigroup (UInt n r c)

Defined in ZkFold.Symbolic.Data.UInt

Methods

(+) :: UInt n r c -> UInt n r c -> UInt n r c

(Symbolic c, KnownNat n, KnownRegisterSize r) => MultiplicativeMonoid (UInt n r c)

Defined in ZkFold.Symbolic.Data.UInt

Methods

one :: UInt n r c

(Symbolic c, KnownNat n, KnownRegisterSize rs) => MultiplicativeSemigroup (UInt n rs c)

Defined in ZkFold.Symbolic.Data.UInt

Methods

(*) :: UInt n rs c -> UInt n rs c -> UInt n rs c

(Symbolic c, KnownNat n, KnownRegisterSize r) => Ring (UInt n r c)

Defined in ZkFold.Symbolic.Data.UInt

(Symbolic c, KnownNat n, KnownRegisterSize r, KnownRegisters c n r, regSize ~ GetRegisterSize (BaseField c) n r, KnownNat (Ceil regSize OrdWord)) => SemiEuclidean (UInt n r c)

Defined in ZkFold.Symbolic.Data.UInt

Methods

divMod :: UInt n r c -> UInt n r c -> (UInt n r c, UInt n r c)

div :: UInt n r c -> UInt n r c -> UInt n r c

mod :: UInt n r c -> UInt n r c -> UInt n r c

(Symbolic c, KnownNat n, KnownRegisterSize r) => Semiring (UInt n r c)

Defined in ZkFold.Symbolic.Data.UInt

(Symbolic (Interpreter a), KnownNat n, KnownRegisterSize r) => ToConstant (UInt n r (Interpreter a))

Defined in ZkFold.Symbolic.Data.UInt

Associated Types

type Const (UInt n r (Interpreter a))

Methods

toConstant :: UInt n r (Interpreter a) -> Const (UInt n r (Interpreter a))

(KnownRegisters c n r, Symbolic c) => SymbolicData (UInt n r c)

Defined in ZkFold.Symbolic.Data.UInt

Associated Types

type Context (UInt n r c) :: (Type -> Type) -> Type

type Support (UInt n r c)

type Layout (UInt n r c) :: Type -> Type

type Payload (UInt n r c) :: Type -> Type

Methods

arithmetize :: UInt n r c -> Support (UInt n r c) -> Context (UInt n r c) (Layout (UInt n r c))

payload :: UInt n r c -> Support (UInt n r c) -> Payload (UInt n r c) (WitnessField (Context (UInt n r c)))

restore :: Context (UInt n r c) ~ c0 => (Support (UInt n r c) -> (c0 (Layout (UInt n r c)), Payload (UInt n r c) (WitnessField c0))) -> UInt n r c

(KnownRegisters c n r, Symbolic c) => Eq (UInt n r c)

Defined in ZkFold.Symbolic.Data.UInt

Associated Types

type BooleanOf (UInt n r c)

Methods

(==) :: UInt n r c -> UInt n r c -> BooleanOf (UInt n r c)

(/=) :: UInt n r c -> UInt n r c -> BooleanOf (UInt n r c)

(Symbolic c, KnownNat n, KnownRegisterSize r, KnownRegisters c n r) => SymbolicInput (UInt n r c)

Defined in ZkFold.Symbolic.Data.UInt

Methods

isValid :: UInt n r c -> Bool (Context (UInt n r c))

(Symbolic c, KnownNat n, KnownRegisterSize r, KnownRegisters c n r, regSize ~ GetRegisterSize (BaseField c) n r, KnownNat (Ceil regSize OrdWord)) => Ord (UInt n r c)

Defined in ZkFold.Symbolic.Data.UInt

Associated Types

type OrderingOf (UInt n r c)

Methods

ordering :: UInt n r c -> UInt n r c -> UInt n r c -> OrderingOf (UInt n r c) -> UInt n r c

compare :: UInt n r c -> UInt n r c -> OrderingOf (UInt n r c)

(<) :: UInt n r c -> UInt n r c -> BooleanOf (UInt n r c)

(<=) :: UInt n r c -> UInt n r c -> BooleanOf (UInt n r c)

(>) :: UInt n r c -> UInt n r c -> BooleanOf (UInt n r c)

(>=) :: UInt n r c -> UInt n r c -> BooleanOf (UInt n r c)

max :: UInt n r c -> UInt n r c -> UInt n r c

min :: UInt n r c -> UInt n r c -> UInt n r c

(Symbolic c, KnownNat n, KnownRegisterSize r) => StrictNum (UInt n r c)

Defined in ZkFold.Symbolic.Data.UInt

Methods

strictAdd :: UInt n r c -> UInt n r c -> UInt n r c

strictSub :: UInt n r c -> UInt n r c -> UInt n r c

strictMul :: UInt n r c -> UInt n r c -> UInt n r c

MultiplicativeMonoid (UInt n r c) => Exponent (UInt n r c) Natural

Defined in ZkFold.Symbolic.Data.UInt

Methods

(^) :: UInt n r c -> Natural -> UInt n r c

(Symbolic c, KnownRegisterSize r, NumberOfBits (BaseField c) ~ n) => Iso (UInt n r c) (FieldElement c)

Defined in ZkFold.Symbolic.Data.UInt

Methods

from :: UInt n r c -> FieldElement c

(Symbolic c, KnownNat n, KnownRegisterSize r) => Iso (UInt n r c) (ByteString n c)

Defined in ZkFold.Symbolic.Data.UInt

Methods

from :: UInt n r c -> ByteString n c

(Symbolic c, KnownNat n, KnownNat k, KnownRegisterSize r) => Resize (UInt n r c) (UInt k r c)

Defined in ZkFold.Symbolic.Data.UInt

Methods

resize :: UInt n r c -> UInt k r c

type Rep (UInt n r context)

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 a))

Defined in ZkFold.Symbolic.Data.UInt

type Const (UInt n r (Interpreter a)) = Natural

type Context (UInt n r c)

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)

Defined in ZkFold.Symbolic.Data.UInt

type Layout (UInt n r c) = Layout (c (Vector (NumberOfRegisters (BaseField c) n r)))

type Payload (UInt n r c)

Defined in ZkFold.Symbolic.Data.UInt

type Payload (UInt n r c) = Payload (c (Vector (NumberOfRegisters (BaseField c) n r)))

type Support (UInt n r c)

Defined in ZkFold.Symbolic.Data.UInt

type Support (UInt n r c) = Support (c (Vector (NumberOfRegisters (BaseField c) n r)))

type BooleanOf (UInt n r c)

Defined in ZkFold.Symbolic.Data.UInt

type BooleanOf (UInt n r c) = BooleanOf (c (Vector (NumberOfRegisters (BaseField c) n r)))

type OrderingOf (UInt n r c)

Defined in ZkFold.Symbolic.Data.UInt

type OrderingOf (UInt n r c) = Ordering c

type OrdWord = 16

Word size in bits used in comparisons. Subject to change

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

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

toNative :: forall n r c a. (Symbolic c, KnownNat n, KnownRegisterSize r, BaseField c ~ a) => KnownNat (GetRegisterSize a n r) => UInt n r c -> FieldElement c

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

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) => UInt n r c -> UInt n r c -> (UInt n r c, UInt n r c, UInt n r c)

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.

natural :: forall c n r i. (Symbolic c, KnownNat n, KnownRegisterSize r, Witness i (WitnessField c)) => Vector (NumberOfRegisters (BaseField c) n r) i -> IntegralOf (WitnessField c)

"natural" value from vector of registers.

register :: forall c n r. (Symbolic c, KnownNat n, KnownRegisterSize r) => IntegralOf (WitnessField c) -> Zp (NumberOfRegisters (BaseField c) n r) -> WitnessField c

register n i returns i-th register of n.

productMod :: forall c n r. Symbolic c => KnownRegisterSize r => KnownNat n => KnownRegisters c n r => KnownNat (Ceil (GetRegisterSize (BaseField c) n r) OrdWord) => UInt n r c -> UInt n r c -> UInt n r c -> (UInt n r c, UInt n r c)

Calculate a * b divMod m using less constraints than would've been required by these operations used consequently

blueprintGE :: forall r i a w m f. (Arithmetic a, MonadCircuit i a w m, Zip f, Foldable f, KnownNat r) => f i -> f i -> m i