{-# LANGUAGE AllowAmbiguousTypes  #-}
{-# LANGUAGE DerivingVia          #-}
{-# LANGUAGE UndecidableInstances #-}

module ZkFold.Symbolic.Data.FieldElement where

import           Control.DeepSeq                  (NFData)
import           Data.Foldable                    (foldr)
import           Data.Function                    (($), (.))
import           Data.Functor                     (fmap, (<$>))
import           Data.Tuple                       (snd)
import           GHC.Generics                     (Generic, Par1 (..))
import           Prelude                          (Integer)
import qualified Prelude                          as Haskell

import           ZkFold.Base.Algebra.Basic.Class
import           ZkFold.Base.Algebra.Basic.Number
import           ZkFold.Base.Data.HFunctor        (hmap)
import           ZkFold.Base.Data.Vector          (Vector, fromVector, unsafeToVector)
import           ZkFold.Symbolic.Class
import           ZkFold.Symbolic.Data.Bool        (Bool, BoolType (true))
import           ZkFold.Symbolic.Data.Class
import           ZkFold.Symbolic.Data.Combinators (expansion, horner, runInvert)
import           ZkFold.Symbolic.Data.Conditional (Conditional)
import           ZkFold.Symbolic.Data.Eq          (Eq)
import           ZkFold.Symbolic.Data.Input
import           ZkFold.Symbolic.Data.Ord
import           ZkFold.Symbolic.Interpreter      (Interpreter (..))
import           ZkFold.Symbolic.MonadCircuit     (newAssigned)

newtype FieldElement c = FieldElement { forall (c :: (Type -> Type) -> Type). FieldElement c -> c Par1
fromFieldElement :: c Par1 }
    deriving (forall x. FieldElement c -> Rep (FieldElement c) x)
-> (forall x. Rep (FieldElement c) x -> FieldElement c)
-> Generic (FieldElement c)
forall x. Rep (FieldElement c) x -> FieldElement c
forall x. FieldElement c -> Rep (FieldElement c) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall (c :: (Type -> Type) -> Type) x.
Rep (FieldElement c) x -> FieldElement c
forall (c :: (Type -> Type) -> Type) x.
FieldElement c -> Rep (FieldElement c) x
$cfrom :: forall (c :: (Type -> Type) -> Type) x.
FieldElement c -> Rep (FieldElement c) x
from :: forall x. FieldElement c -> Rep (FieldElement c) x
$cto :: forall (c :: (Type -> Type) -> Type) x.
Rep (FieldElement c) x -> FieldElement c
to :: forall x. Rep (FieldElement c) x -> FieldElement c
Generic

deriving stock instance Haskell.Show (c Par1) => Haskell.Show (FieldElement c)

deriving stock instance Haskell.Eq (c Par1) => Haskell.Eq (FieldElement c)

deriving stock instance Haskell.Ord (c Par1) => Haskell.Ord (FieldElement c)

deriving newtype instance NFData (c Par1) => NFData (FieldElement c)

deriving newtype instance Symbolic c => SymbolicData (FieldElement c)

deriving newtype instance Symbolic c => Conditional (Bool c) (FieldElement c)

deriving newtype instance Symbolic c => Eq (FieldElement c)

deriving newtype instance Symbolic c => Ord (FieldElement c)

instance {-# INCOHERENT #-} (Symbolic c, FromConstant k (BaseField c)) => FromConstant k (FieldElement c) where
  fromConstant :: k -> FieldElement c
fromConstant = c Par1 -> FieldElement c
forall (c :: (Type -> Type) -> Type). c Par1 -> FieldElement c
FieldElement (c Par1 -> FieldElement c) -> (k -> c Par1) -> k -> FieldElement c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Par1 (BaseField c) -> c Par1
forall (c :: (Type -> Type) -> Type) (f :: Type -> Type).
(Symbolic c, Functor f) =>
f (BaseField c) -> c f
embed (Par1 (BaseField c) -> c Par1)
-> (k -> Par1 (BaseField c)) -> k -> c Par1
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BaseField c -> Par1 (BaseField c)
forall p. p -> Par1 p
Par1 (BaseField c -> Par1 (BaseField c))
-> (k -> BaseField c) -> k -> Par1 (BaseField c)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. k -> BaseField c
forall a b. FromConstant a b => a -> b
fromConstant

instance ToConstant (FieldElement (Interpreter a)) where
  type Const (FieldElement (Interpreter a)) = a
  toConstant :: FieldElement (Interpreter a)
-> Const (FieldElement (Interpreter a))
toConstant (FieldElement (Interpreter (Par1 a
x))) = a
Const (FieldElement (Interpreter a))
x

instance Symbolic c => Exponent (FieldElement c) Natural where
  ^ :: FieldElement c -> Natural -> FieldElement c
(^) = FieldElement c -> Natural -> FieldElement c
forall a. MultiplicativeMonoid a => a -> Natural -> a
natPow

instance Symbolic c => Exponent (FieldElement c) Integer where
  ^ :: FieldElement c -> Integer -> FieldElement c
(^) = FieldElement c -> Integer -> FieldElement c
forall a. Field a => a -> Integer -> a
intPowF

instance (Symbolic c, Scale k (BaseField c)) => Scale k (FieldElement c) where
  scale :: k -> FieldElement c -> FieldElement c
scale k
k (FieldElement c Par1
c) = c Par1 -> FieldElement c
forall (c :: (Type -> Type) -> Type). c Par1 -> FieldElement c
FieldElement (c Par1 -> FieldElement c) -> c Par1 -> FieldElement c
forall a b. (a -> b) -> a -> b
$ c Par1
-> (forall {i} {m :: Type -> Type}.
    (NFData i, MonadCircuit i (BaseField c) (WitnessField c) m) =>
    FunBody '[Par1] Par1 i m)
-> c Par1
forall (f :: Type -> Type) (g :: Type -> Type).
c f -> CircuitFun '[f] g c -> c g
forall (c :: (Type -> Type) -> Type) (f :: Type -> Type)
       (g :: Type -> Type).
Symbolic c =>
c f -> CircuitFun '[f] g c -> c g
fromCircuitF c Par1
c ((forall {i} {m :: Type -> Type}.
  (NFData i, MonadCircuit i (BaseField c) (WitnessField c) m) =>
  FunBody '[Par1] Par1 i m)
 -> c Par1)
-> (forall {i} {m :: Type -> Type}.
    (NFData i, MonadCircuit i (BaseField c) (WitnessField c) m) =>
    FunBody '[Par1] Par1 i m)
-> c Par1
forall a b. (a -> b) -> a -> b
$ \(Par1 i
i) ->
    i -> Par1 i
forall p. p -> Par1 p
Par1 (i -> Par1 i) -> m i -> m (Par1 i)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> ClosedPoly i (BaseField c) -> m i
forall var a w (m :: Type -> Type).
MonadCircuit var a w m =>
ClosedPoly var a -> m var
newAssigned (\i -> x
x -> BaseField c -> x
forall a b. FromConstant a b => a -> b
fromConstant (k -> BaseField c -> BaseField c
forall b a. Scale b a => b -> a -> a
scale k
k BaseField c
forall a. MultiplicativeMonoid a => a
one :: BaseField c) x -> x -> x
forall a. MultiplicativeSemigroup a => a -> a -> a
* i -> x
x i
i)

instance {-# OVERLAPPING #-} FromConstant (FieldElement c) (FieldElement c)

instance {-# OVERLAPPING #-} Symbolic c => Scale (FieldElement c) (FieldElement c)

instance Symbolic c => MultiplicativeSemigroup (FieldElement c) where
  FieldElement c Par1
x * :: FieldElement c -> FieldElement c -> FieldElement c
* FieldElement c Par1
y = c Par1 -> FieldElement c
forall (c :: (Type -> Type) -> Type). c Par1 -> FieldElement c
FieldElement (c Par1 -> FieldElement c) -> c Par1 -> FieldElement c
forall a b. (a -> b) -> a -> b
$ c Par1
-> c Par1
-> (forall {i} {m :: Type -> Type}.
    (NFData i, MonadCircuit i (BaseField c) (WitnessField c) m) =>
    FunBody '[Par1, Par1] Par1 i m)
-> c Par1
forall (c :: (Type -> Type) -> Type) (f :: Type -> Type)
       (g :: Type -> Type) (h :: Type -> Type).
Symbolic c =>
c f -> c g -> CircuitFun '[f, g] h c -> c h
fromCircuit2F c Par1
x c Par1
y
    ((forall {i} {m :: Type -> Type}.
  (NFData i, MonadCircuit i (BaseField c) (WitnessField c) m) =>
  FunBody '[Par1, Par1] Par1 i m)
 -> c Par1)
-> (forall {i} {m :: Type -> Type}.
    (NFData i, MonadCircuit i (BaseField c) (WitnessField c) m) =>
    FunBody '[Par1, Par1] Par1 i m)
-> c Par1
forall a b. (a -> b) -> a -> b
$ \(Par1 i
i) (Par1 i
j) -> i -> Par1 i
forall p. p -> Par1 p
Par1 (i -> Par1 i) -> m i -> m (Par1 i)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> ClosedPoly i (BaseField c) -> m i
forall var a w (m :: Type -> Type).
MonadCircuit var a w m =>
ClosedPoly var a -> m var
newAssigned (\i -> x
w -> i -> x
w i
i x -> x -> x
forall a. MultiplicativeSemigroup a => a -> a -> a
* i -> x
w i
j)

instance Symbolic c => MultiplicativeMonoid (FieldElement c) where
  one :: FieldElement c
one = c Par1 -> FieldElement c
forall (c :: (Type -> Type) -> Type). c Par1 -> FieldElement c
FieldElement (c Par1 -> FieldElement c) -> c Par1 -> FieldElement c
forall a b. (a -> b) -> a -> b
$ Par1 (BaseField c) -> c Par1
forall (c :: (Type -> Type) -> Type) (f :: Type -> Type).
(Symbolic c, Functor f) =>
f (BaseField c) -> c f
embed (BaseField c -> Par1 (BaseField c)
forall p. p -> Par1 p
Par1 BaseField c
forall a. MultiplicativeMonoid a => a
one)

instance Symbolic c => AdditiveSemigroup (FieldElement c) where
  FieldElement c Par1
x + :: FieldElement c -> FieldElement c -> FieldElement c
+ FieldElement c Par1
y = c Par1 -> FieldElement c
forall (c :: (Type -> Type) -> Type). c Par1 -> FieldElement c
FieldElement (c Par1 -> FieldElement c) -> c Par1 -> FieldElement c
forall a b. (a -> b) -> a -> b
$ c Par1
-> c Par1
-> (forall {i} {m :: Type -> Type}.
    (NFData i, MonadCircuit i (BaseField c) (WitnessField c) m) =>
    FunBody '[Par1, Par1] Par1 i m)
-> c Par1
forall (c :: (Type -> Type) -> Type) (f :: Type -> Type)
       (g :: Type -> Type) (h :: Type -> Type).
Symbolic c =>
c f -> c g -> CircuitFun '[f, g] h c -> c h
fromCircuit2F c Par1
x c Par1
y
    ((forall {i} {m :: Type -> Type}.
  (NFData i, MonadCircuit i (BaseField c) (WitnessField c) m) =>
  FunBody '[Par1, Par1] Par1 i m)
 -> c Par1)
-> (forall {i} {m :: Type -> Type}.
    (NFData i, MonadCircuit i (BaseField c) (WitnessField c) m) =>
    FunBody '[Par1, Par1] Par1 i m)
-> c Par1
forall a b. (a -> b) -> a -> b
$ \(Par1 i
i) (Par1 i
j) -> i -> Par1 i
forall p. p -> Par1 p
Par1 (i -> Par1 i) -> m i -> m (Par1 i)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> ClosedPoly i (BaseField c) -> m i
forall var a w (m :: Type -> Type).
MonadCircuit var a w m =>
ClosedPoly var a -> m var
newAssigned (\i -> x
w -> i -> x
w i
i x -> x -> x
forall a. AdditiveSemigroup a => a -> a -> a
+ i -> x
w i
j)

instance Symbolic c => AdditiveMonoid (FieldElement c) where
  zero :: FieldElement c
zero = c Par1 -> FieldElement c
forall (c :: (Type -> Type) -> Type). c Par1 -> FieldElement c
FieldElement (c Par1 -> FieldElement c) -> c Par1 -> FieldElement c
forall a b. (a -> b) -> a -> b
$ Par1 (BaseField c) -> c Par1
forall (c :: (Type -> Type) -> Type) (f :: Type -> Type).
(Symbolic c, Functor f) =>
f (BaseField c) -> c f
embed (BaseField c -> Par1 (BaseField c)
forall p. p -> Par1 p
Par1 BaseField c
forall a. AdditiveMonoid a => a
zero)

instance Symbolic c => AdditiveGroup (FieldElement c) where
  negate :: FieldElement c -> FieldElement c
negate (FieldElement c Par1
x) = c Par1 -> FieldElement c
forall (c :: (Type -> Type) -> Type). c Par1 -> FieldElement c
FieldElement (c Par1 -> FieldElement c) -> c Par1 -> FieldElement c
forall a b. (a -> b) -> a -> b
$ c Par1
-> (forall {i} {m :: Type -> Type}.
    (NFData i, MonadCircuit i (BaseField c) (WitnessField c) m) =>
    FunBody '[Par1] Par1 i m)
-> c Par1
forall (f :: Type -> Type) (g :: Type -> Type).
c f -> CircuitFun '[f] g c -> c g
forall (c :: (Type -> Type) -> Type) (f :: Type -> Type)
       (g :: Type -> Type).
Symbolic c =>
c f -> CircuitFun '[f] g c -> c g
fromCircuitF c Par1
x ((forall {i} {m :: Type -> Type}.
  (NFData i, MonadCircuit i (BaseField c) (WitnessField c) m) =>
  FunBody '[Par1] Par1 i m)
 -> c Par1)
-> (forall {i} {m :: Type -> Type}.
    (NFData i, MonadCircuit i (BaseField c) (WitnessField c) m) =>
    FunBody '[Par1] Par1 i m)
-> c Par1
forall a b. (a -> b) -> a -> b
$ \(Par1 i
i) ->
    i -> Par1 i
forall p. p -> Par1 p
Par1 (i -> Par1 i) -> m i -> m (Par1 i)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> ClosedPoly i (BaseField c) -> m i
forall var a w (m :: Type -> Type).
MonadCircuit var a w m =>
ClosedPoly var a -> m var
newAssigned (\i -> x
w -> x -> x
forall a. AdditiveGroup a => a -> a
negate (i -> x
w i
i))

  FieldElement c Par1
x - :: FieldElement c -> FieldElement c -> FieldElement c
- FieldElement c Par1
y = c Par1 -> FieldElement c
forall (c :: (Type -> Type) -> Type). c Par1 -> FieldElement c
FieldElement (c Par1 -> FieldElement c) -> c Par1 -> FieldElement c
forall a b. (a -> b) -> a -> b
$ c Par1
-> c Par1
-> (forall {i} {m :: Type -> Type}.
    (NFData i, MonadCircuit i (BaseField c) (WitnessField c) m) =>
    FunBody '[Par1, Par1] Par1 i m)
-> c Par1
forall (c :: (Type -> Type) -> Type) (f :: Type -> Type)
       (g :: Type -> Type) (h :: Type -> Type).
Symbolic c =>
c f -> c g -> CircuitFun '[f, g] h c -> c h
fromCircuit2F c Par1
x c Par1
y
    ((forall {i} {m :: Type -> Type}.
  (NFData i, MonadCircuit i (BaseField c) (WitnessField c) m) =>
  FunBody '[Par1, Par1] Par1 i m)
 -> c Par1)
-> (forall {i} {m :: Type -> Type}.
    (NFData i, MonadCircuit i (BaseField c) (WitnessField c) m) =>
    FunBody '[Par1, Par1] Par1 i m)
-> c Par1
forall a b. (a -> b) -> a -> b
$ \(Par1 i
i) (Par1 i
j) -> i -> Par1 i
forall p. p -> Par1 p
Par1 (i -> Par1 i) -> m i -> m (Par1 i)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> ClosedPoly i (BaseField c) -> m i
forall var a w (m :: Type -> Type).
MonadCircuit var a w m =>
ClosedPoly var a -> m var
newAssigned (\i -> x
w -> i -> x
w i
i x -> x -> x
forall a. AdditiveGroup a => a -> a -> a
- i -> x
w i
j)

instance Symbolic c => Semiring (FieldElement c)

instance Symbolic c => Ring (FieldElement c)

instance Symbolic c => Field (FieldElement c) where
  finv :: FieldElement c -> FieldElement c
finv (FieldElement c Par1
x) =
    c Par1 -> FieldElement c
forall (c :: (Type -> Type) -> Type). c Par1 -> FieldElement c
FieldElement (c Par1 -> FieldElement c) -> c Par1 -> FieldElement c
forall a b. (a -> b) -> a -> b
$ c Par1
-> (Par1 (BaseField c) -> Par1 (BaseField c))
-> (forall {i} {m :: Type -> Type}.
    (NFData i, MonadCircuit i (BaseField c) (WitnessField c) m) =>
    FunBody '[Par1] Par1 i m)
-> c Par1
forall (c :: (Type -> Type) -> Type) a (f :: Type -> Type)
       (g :: Type -> Type).
(Symbolic c, BaseField c ~ a) =>
c f -> (f a -> g a) -> CircuitFun '[f] g c -> c g
symbolicF c Par1
x (\(Par1 BaseField c
v) -> BaseField c -> Par1 (BaseField c)
forall p. p -> Par1 p
Par1 (BaseField c -> BaseField c
forall a. Field a => a -> a
finv BaseField c
v))
      ((forall {i} {m :: Type -> Type}.
  (NFData i, MonadCircuit i (BaseField c) (WitnessField c) m) =>
  FunBody '[Par1] Par1 i m)
 -> c Par1)
-> (forall {i} {m :: Type -> Type}.
    (NFData i, MonadCircuit i (BaseField c) (WitnessField c) m) =>
    FunBody '[Par1] Par1 i m)
-> c Par1
forall a b. (a -> b) -> a -> b
$ ((Par1 i, Par1 i) -> Par1 i) -> m (Par1 i, Par1 i) -> m (Par1 i)
forall a b. (a -> b) -> m a -> m b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap (Par1 i, Par1 i) -> Par1 i
forall a b. (a, b) -> b
snd (m (Par1 i, Par1 i) -> m (Par1 i))
-> (Par1 i -> m (Par1 i, Par1 i)) -> Par1 i -> m (Par1 i)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Par1 i -> m (Par1 i, Par1 i)
forall i a w (m :: Type -> Type) (f :: Type -> Type).
(MonadCircuit i a w m, Representable f, Traversable f) =>
f i -> m (f i, f i)
runInvert

instance
    ( KnownNat (Order (FieldElement c))
    , KnownNat (NumberOfBits (FieldElement c))) => Finite (FieldElement c) where
  type Order (FieldElement c) = Order (BaseField c)

instance Symbolic c => BinaryExpansion (FieldElement c) where
  type Bits (FieldElement c) = c (Vector (NumberOfBits (BaseField c)))
  binaryExpansion :: FieldElement c -> Bits (FieldElement c)
binaryExpansion (FieldElement c Par1
c) = (forall a. [a] -> Vector (NumberOfBits (BaseField c)) a)
-> c [] -> c (Vector (NumberOfBits (BaseField c)))
forall {k} (c :: (k -> Type) -> Type) (f :: k -> Type)
       (g :: k -> Type).
HFunctor c =>
(forall (a :: k). f a -> g a) -> c f -> c g
forall (f :: Type -> Type) (g :: Type -> Type).
(forall a. f a -> g a) -> c f -> c g
hmap [a] -> Vector (NumberOfBits (BaseField c)) a
forall (size :: Natural) a. [a] -> Vector size a
forall a. [a] -> Vector (NumberOfBits (BaseField c)) a
unsafeToVector (c [] -> c (Vector (NumberOfBits (BaseField c))))
-> c [] -> c (Vector (NumberOfBits (BaseField c)))
forall a b. (a -> b) -> a -> b
$ c Par1
-> (Par1 (BaseField c) -> [BaseField c])
-> CircuitFun '[Par1] [] c
-> c []
forall (c :: (Type -> Type) -> Type) a (f :: Type -> Type)
       (g :: Type -> Type).
(Symbolic c, BaseField c ~ a) =>
c f -> (f a -> g a) -> CircuitFun '[f] g c -> c g
symbolicF c Par1
c
    (Natural -> [BaseField c] -> [BaseField c]
forall a. AdditiveMonoid a => Natural -> [a] -> [a]
padBits Natural
n ([BaseField c] -> [BaseField c])
-> (Par1 (BaseField c) -> [BaseField c])
-> Par1 (BaseField c)
-> [BaseField c]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Natural -> BaseField c) -> [Natural] -> [BaseField c]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap Natural -> BaseField c
forall a b. FromConstant a b => a -> b
fromConstant ([Natural] -> [BaseField c])
-> (Par1 (BaseField c) -> [Natural])
-> Par1 (BaseField c)
-> [BaseField c]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Natural -> [Natural]
Natural -> Bits Natural
forall a. BinaryExpansion a => a -> Bits a
binaryExpansion (Natural -> [Natural])
-> (Par1 (BaseField c) -> Natural)
-> Par1 (BaseField c)
-> [Natural]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BaseField c -> Natural
BaseField c -> Const (BaseField c)
forall a. ToConstant a => a -> Const a
toConstant (BaseField c -> Natural)
-> (Par1 (BaseField c) -> BaseField c)
-> Par1 (BaseField c)
-> Natural
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Par1 (BaseField c) -> BaseField c
forall p. Par1 p -> p
unPar1)
    (Natural -> i -> m [i]
forall i a w (m :: Type -> Type).
(MonadCircuit i a w m, Arithmetic a) =>
Natural -> i -> m [i]
expansion Natural
n (i -> m [i]) -> (Par1 i -> i) -> Par1 i -> m [i]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Par1 i -> i
forall p. Par1 p -> p
unPar1)
    where n :: Natural
n = forall a. KnownNat (NumberOfBits a) => Natural
numberOfBits @(BaseField c)
  fromBinary :: Bits (FieldElement c) -> FieldElement c
fromBinary Bits (FieldElement c)
bits =
    c Par1 -> FieldElement c
forall (c :: (Type -> Type) -> Type). c Par1 -> FieldElement c
FieldElement (c Par1 -> FieldElement c) -> c Par1 -> FieldElement c
forall a b. (a -> b) -> a -> b
$ c (Vector (NumberOfBits (BaseField c)))
-> (Vector (NumberOfBits (BaseField c)) (BaseField c)
    -> Par1 (BaseField c))
-> (forall {i} {m :: Type -> Type}.
    (NFData i, MonadCircuit i (BaseField c) (WitnessField c) m) =>
    FunBody '[Vector (NumberOfBits (BaseField c))] Par1 i m)
-> c Par1
forall (c :: (Type -> Type) -> Type) a (f :: Type -> Type)
       (g :: Type -> Type).
(Symbolic c, BaseField c ~ a) =>
c f -> (f a -> g a) -> CircuitFun '[f] g c -> c g
symbolicF c (Vector (NumberOfBits (BaseField c)))
Bits (FieldElement c)
bits (BaseField c -> Par1 (BaseField c)
forall p. p -> Par1 p
Par1 (BaseField c -> Par1 (BaseField c))
-> (Vector (NumberOfBits (BaseField c)) (BaseField c)
    -> BaseField c)
-> Vector (NumberOfBits (BaseField c)) (BaseField c)
-> Par1 (BaseField c)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (BaseField c -> BaseField c -> BaseField c)
-> BaseField c
-> Vector (NumberOfBits (BaseField c)) (BaseField c)
-> BaseField c
forall a b.
(a -> b -> b) -> b -> Vector (NumberOfBits (BaseField c)) a -> b
forall (t :: Type -> Type) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\BaseField c
x BaseField c
y -> BaseField c
x BaseField c -> BaseField c -> BaseField c
forall a. AdditiveSemigroup a => a -> a -> a
+ BaseField c
y BaseField c -> BaseField c -> BaseField c
forall a. AdditiveSemigroup a => a -> a -> a
+ BaseField c
y) BaseField c
forall a. AdditiveMonoid a => a
zero)
      ((forall {i} {m :: Type -> Type}.
  (NFData i, MonadCircuit i (BaseField c) (WitnessField c) m) =>
  FunBody '[Vector (NumberOfBits (BaseField c))] Par1 i m)
 -> c Par1)
-> (forall {i} {m :: Type -> Type}.
    (NFData i, MonadCircuit i (BaseField c) (WitnessField c) m) =>
    FunBody '[Vector (NumberOfBits (BaseField c))] Par1 i m)
-> c Par1
forall a b. (a -> b) -> a -> b
$ (i -> Par1 i) -> m i -> m (Par1 i)
forall a b. (a -> b) -> m a -> m b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap i -> Par1 i
forall p. p -> Par1 p
Par1 (m i -> m (Par1 i))
-> (Vector (NumberOfBits (BaseField c)) i -> m i)
-> Vector (NumberOfBits (BaseField c)) i
-> m (Par1 i)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [i] -> m i
forall i a w (m :: Type -> Type).
MonadCircuit i a w m =>
[i] -> m i
horner ([i] -> m i)
-> (Vector (NumberOfBits (BaseField c)) i -> [i])
-> Vector (NumberOfBits (BaseField c)) i
-> m i
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Vector (NumberOfBits (BaseField c)) i -> [i]
forall (size :: Natural) a. Vector size a -> [a]
fromVector

instance (Symbolic c) => SymbolicInput (FieldElement c) where
  isValid :: FieldElement c -> Bool (Context (FieldElement c))
isValid FieldElement c
_ = Bool c
Bool (Context (FieldElement c))
forall b. BoolType b => b
true