{-# LANGUAGE AllowAmbiguousTypes  #-}
{-# LANGUAGE DerivingStrategies   #-}
{-# LANGUAGE UndecidableInstances #-}

module ZkFold.Symbolic.Data.FFA (FFA (..), Size, coprimesDownFrom, coprimes) where

import           Control.Applicative              (pure)
import           Control.DeepSeq                  (NFData, force)
import           Control.Monad                    (Monad, forM, return, (>>=))
import           Data.Foldable                    (any, foldlM)
import           Data.Function                    (const, ($), (.))
import           Data.Functor                     (fmap, (<$>))
import           Data.List                        (dropWhile, (++))
import           Data.Ratio                       ((%))
import           Data.Traversable                 (for, traverse)
import           Data.Tuple                       (fst, snd, uncurry)
import           Data.Zip                         (zipWith)
import           Prelude                          (Integer, error)
import qualified Prelude                          as Haskell

import           ZkFold.Base.Algebra.Basic.Class
import           ZkFold.Base.Algebra.Basic.Field  (Zp, inv)
import           ZkFold.Base.Algebra.Basic.Number
import           ZkFold.Base.Data.Utils           (zipWithM)
import           ZkFold.Base.Data.Vector
import           ZkFold.Prelude                   (iterateM, length)
import           ZkFold.Symbolic.Class
import           ZkFold.Symbolic.Data.Bool        (Bool, BoolType (..))
import           ZkFold.Symbolic.Data.Class
import           ZkFold.Symbolic.Data.Combinators (expansionW, log2, maxBitsPerFieldElement, splitExpansion)
import           ZkFold.Symbolic.Data.Eq
import           ZkFold.Symbolic.Data.Input
import           ZkFold.Symbolic.Data.Ord         (blueprintGE)
import           ZkFold.Symbolic.Interpreter
import           ZkFold.Symbolic.MonadCircuit     (MonadCircuit, newAssigned)

type Size = 7

-- | Foreign-field arithmetic based on https://cr.yp.to/papers/mmecrt.pdf
newtype FFA (p :: Natural) c = FFA (c (Vector Size))

deriving newtype instance Symbolic c => SymbolicData (FFA p c)
deriving newtype instance NFData (c (Vector Size)) => NFData (FFA p c)
deriving newtype instance Haskell.Show (c (Vector Size)) => Haskell.Show (FFA p c)

coprimesDownFrom :: KnownNat n => Natural -> Vector n Natural
coprimesDownFrom :: forall (n :: Natural). KnownNat n => Natural -> Vector n Natural
coprimesDownFrom Natural
n = (([Natural], [Natural]) -> (Natural, ([Natural], [Natural])))
-> ([Natural], [Natural]) -> Vector n Natural
forall (size :: Natural) a b.
KnownNat size =>
(b -> (a, b)) -> b -> Vector size a
unfold (([Natural] -> [Natural] -> (Natural, ([Natural], [Natural])))
-> ([Natural], [Natural]) -> (Natural, ([Natural], [Natural]))
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry [Natural] -> [Natural] -> (Natural, ([Natural], [Natural]))
forall {a}. Integral a => [a] -> [a] -> (a, ([a], [a]))
step) ([], [Natural
n,Natural
nNatural -> Natural -> Natural
-!Natural
1..Natural
0])
  where
    step :: [a] -> [a] -> (a, ([a], [a]))
step [a]
ans [a]
xs =
      case (a -> Bool) -> [a] -> [a]
forall a. (a -> Bool) -> [a] -> [a]
dropWhile (\a
x -> (a -> Bool) -> [a] -> Bool
forall (t :: Type -> Type) a.
Foldable t =>
(a -> Bool) -> t a -> Bool
any ((a -> a -> Bool
forall a. Eq a => a -> a -> Bool
Haskell./= a
1) (a -> Bool) -> (a -> a) -> a -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> a -> a
forall a. Integral a => a -> a -> a
Haskell.gcd a
x) [a]
ans) [a]
xs of
        []      -> String -> (a, ([a], [a]))
forall a. HasCallStack => String -> a
error String
"no options left"
        (a
x:[a]
xs') -> (a
x, ([a]
ans [a] -> [a] -> [a]
forall a. [a] -> [a] -> [a]
++ [a
x], [a]
xs'))

coprimes :: forall a. Finite a => Vector Size Natural
coprimes :: forall a. Finite a => Vector Size Natural
coprimes = forall (n :: Natural). KnownNat n => Natural -> Vector n Natural
coprimesDownFrom @Size (Natural -> Vector Size Natural) -> Natural -> Vector Size Natural
forall a b. (a -> b) -> a -> b
$ Natural
2 Natural -> Natural -> Natural
forall a b. Exponent a b => a -> b -> a
^ (forall p. Finite p => Natural
maxBitsPerFieldElement @a Natural -> Natural -> Natural
forall a. SemiEuclidean a => a -> a -> a
`div` Natural
2)

sigma :: Natural
sigma :: Natural
sigma = Double -> Natural
forall b. Integral b => Double -> b
forall a b. (RealFrac a, Integral b) => a -> b
Haskell.ceiling (Natural -> Double
log2 (Natural -> Double) -> Natural -> Double
forall a b. (a -> b) -> a -> b
$ forall (n :: Natural). KnownNat n => Natural
value @Size) Natural -> Natural -> Natural
forall a. AdditiveSemigroup a => a -> a -> a
+ Natural
1 :: Natural

mprod0 :: forall a. Finite a => Natural
mprod0 :: forall p. Finite p => Natural
mprod0 = Vector Size Natural -> Natural
forall (t :: Type -> Type) a.
(Foldable t, MultiplicativeMonoid a) =>
t a -> a
product (forall a. Finite a => Vector Size Natural
coprimes @a)

mprod :: forall a p . (Finite a, KnownNat p) => Natural
mprod :: forall a (p :: Natural). (Finite a, KnownNat p) => Natural
mprod = forall p. Finite p => Natural
mprod0 @a Natural -> Natural -> Natural
forall a. SemiEuclidean a => a -> a -> a
`mod` forall (n :: Natural). KnownNat n => Natural
value @p

mis0 :: forall a. Finite a => Vector Size Natural
mis0 :: forall a. Finite a => Vector Size Natural
mis0 = let (Vector Size Natural
c, Natural
m) = (forall a. Finite a => Vector Size Natural
coprimes @a, forall p. Finite p => Natural
mprod0 @a) in (Natural
m Natural -> Natural -> Natural
forall a. SemiEuclidean a => a -> a -> a
`div`) (Natural -> Natural) -> Vector Size Natural -> Vector Size Natural
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Vector Size Natural
c

mis :: forall a p. (Finite a, KnownNat p) => Vector Size Natural
mis :: forall a (p :: Natural).
(Finite a, KnownNat p) =>
Vector Size Natural
mis = (Natural -> Natural -> Natural
forall a. SemiEuclidean a => a -> a -> a
`mod` forall (n :: Natural). KnownNat n => Natural
value @p) (Natural -> Natural) -> Vector Size Natural -> Vector Size Natural
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. Finite a => Vector Size Natural
mis0 @a

minv :: forall a. Finite a => Vector Size Natural
minv :: forall a. Finite a => Vector Size Natural
minv = (Natural -> Natural -> Natural)
-> Vector Size Natural
-> Vector Size Natural
-> Vector Size Natural
forall a b c.
(a -> b -> c) -> Vector Size a -> Vector Size b -> Vector Size c
forall (f :: Type -> Type) a b c.
Zip f =>
(a -> b -> c) -> f a -> f b -> f c
zipWith (\Natural
x Natural
p -> Natural -> Integer
forall a b. FromConstant a b => a -> b
fromConstant Natural
x Integer -> Natural -> Natural
`inv` Natural
p) (forall a. Finite a => Vector Size Natural
mis0 @a) (forall a. Finite a => Vector Size Natural
coprimes @a)

wordExpansion :: forall r. KnownNat r => Natural -> [Natural]
wordExpansion :: forall (r :: Natural). KnownNat r => Natural -> [Natural]
wordExpansion Natural
0 = []
wordExpansion Natural
x = (Natural
x Natural -> Natural -> Natural
forall a. SemiEuclidean a => a -> a -> a
`mod` Natural
wordSize) Natural -> [Natural] -> [Natural]
forall a. a -> [a] -> [a]
: forall (r :: Natural). KnownNat r => Natural -> [Natural]
wordExpansion @r (Natural
x Natural -> Natural -> Natural
forall a. SemiEuclidean a => a -> a -> a
`div` Natural
wordSize)
    where
        wordSize :: Natural
wordSize = Natural
2 Natural -> Natural -> Natural
forall a b. Exponent a b => a -> b -> a
^ forall (n :: Natural). KnownNat n => Natural
value @r

toZp :: forall p a. (Arithmetic a, KnownNat p) => Vector Size a -> Zp p
toZp :: forall (p :: Natural) a.
(Arithmetic a, KnownNat p) =>
Vector Size a -> Zp p
toZp = Natural -> Zp p
forall a b. FromConstant a b => a -> b
fromConstant (Natural -> Zp p)
-> (Vector Size a -> Natural) -> Vector Size a -> Zp p
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Vector Size a -> Natural
impl
  where
    mods :: Vector Size Natural
mods = forall a. Finite a => Vector Size Natural
coprimes @a
    binary :: a -> a -> a
binary a
g a
m = (a -> a
forall a b. FromConstant a b => a -> b
fromConstant a
g a -> a -> a
forall a. MultiplicativeSemigroup a => a -> a -> a
* a
2 a -> Natural -> a
forall a b. Exponent a b => a -> b -> a
^ Natural
sigma) a -> a -> a
forall a. SemiEuclidean a => a -> a -> a
`div` a -> a
forall a b. FromConstant a b => a -> b
fromConstant a
m
    impl :: Vector Size a -> Natural
impl Vector Size a
xs =
      let gs0 :: Vector Size Natural
gs0 = (a -> Natural -> Natural)
-> Vector Size a -> Vector Size Natural -> Vector Size Natural
forall a b c.
(a -> b -> c) -> Vector Size a -> Vector Size b -> Vector Size c
forall (f :: Type -> Type) a b c.
Zip f =>
(a -> b -> c) -> f a -> f b -> f c
zipWith (\a
x Natural
y -> a -> Const a
forall a. ToConstant a => a -> Const a
toConstant a
x Natural -> Natural -> Natural
forall a. MultiplicativeSemigroup a => a -> a -> a
* Natural
y) Vector Size a
xs (Vector Size Natural -> Vector Size Natural)
-> Vector Size Natural -> Vector Size Natural
forall a b. (a -> b) -> a -> b
$ forall a. Finite a => Vector Size Natural
minv @a
          gs :: Vector Size Natural
gs = (Natural -> Natural -> Natural)
-> Vector Size Natural
-> Vector Size Natural
-> Vector Size Natural
forall a b c.
(a -> b -> c) -> Vector Size a -> Vector Size b -> Vector Size c
forall (f :: Type -> Type) a b c.
Zip f =>
(a -> b -> c) -> f a -> f b -> f c
zipWith Natural -> Natural -> Natural
forall a. SemiEuclidean a => a -> a -> a
mod Vector Size Natural
gs0 Vector Size Natural
mods
          residue :: Natural
residue = Rational -> Natural
floorN ((Integer
3 Integer -> Integer -> Rational
forall a. Integral a => a -> a -> Ratio a
% Integer
4) Rational -> Rational -> Rational
forall a. AdditiveSemigroup a => a -> a -> a
+ Vector Size Integer -> Integer
forall (t :: Type -> Type) a.
(Foldable t, AdditiveMonoid a) =>
t a -> a
sum ((Natural -> Natural -> Integer)
-> Vector Size Natural
-> Vector Size Natural
-> Vector Size Integer
forall a b c.
(a -> b -> c) -> Vector Size a -> Vector Size b -> Vector Size c
forall (f :: Type -> Type) a b c.
Zip f =>
(a -> b -> c) -> f a -> f b -> f c
zipWith Natural -> Natural -> Integer
forall {a} {a} {a}.
(SemiEuclidean a, Num a, FromConstant a a, FromConstant a a) =>
a -> a -> a
binary Vector Size Natural
gs Vector Size Natural
mods) Integer -> Integer -> Rational
forall a. Integral a => a -> a -> Ratio a
% (Integer
2 Integer -> Natural -> Integer
forall a b. Exponent a b => a -> b -> a
^ Natural
sigma))
       in Vector Size Natural -> Vector Size Natural -> Natural
forall (size :: Natural) a.
Semiring a =>
Vector size a -> Vector size a -> a
vectorDotProduct Vector Size Natural
gs (forall a (p :: Natural).
(Finite a, KnownNat p) =>
Vector Size Natural
mis @a @p) Natural -> Natural -> Natural
-! forall a (p :: Natural). (Finite a, KnownNat p) => Natural
mprod @a @p Natural -> Natural -> Natural
forall a. MultiplicativeSemigroup a => a -> a -> a
* Natural
residue

fromZp :: forall p a. Arithmetic a => Zp p -> Vector Size a
fromZp :: forall (p :: Natural) a. Arithmetic a => Zp p -> Vector Size a
fromZp = (\(FFA (Interpreter Vector Size a
xs) :: FFA p (Interpreter a)) -> Vector Size a
xs) (FFA p (Interpreter a) -> Vector Size a)
-> (Zp p -> FFA p (Interpreter a)) -> Zp p -> Vector Size a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Zp p -> FFA p (Interpreter a)
forall a b. FromConstant a b => a -> b
fromConstant

-- | Subtracts @m@ from @i@ if @i@ is not less than @m@
--
condSubOF :: forall i a w m . (MonadCircuit i a w m, Arithmetic a) => Natural -> i -> m (i, i)
condSubOF :: forall i a w (m :: Type -> Type).
(MonadCircuit i a w m, Arithmetic a) =>
Natural -> i -> m (i, i)
condSubOF Natural
m i
i = do
  i
z <- ClosedPoly i a -> m i
forall var a w (m :: Type -> Type).
MonadCircuit var a w m =>
ClosedPoly var a -> m var
newAssigned (i -> x) -> x
ClosedPoly i a
forall a. AdditiveMonoid a => a
zero
  [i]
bm <- [Natural] -> (Natural -> m i) -> m [i]
forall (t :: Type -> Type) (m :: Type -> Type) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM (forall (r :: Natural). KnownNat r => Natural -> [Natural]
wordExpansion @8 Natural
m [Natural] -> [Natural] -> [Natural]
forall a. [a] -> [a] -> [a]
++ [Natural
0]) ((Natural -> m i) -> m [i]) -> (Natural -> m i) -> m [i]
forall a b. (a -> b) -> a -> b
$ \Natural
x -> if Natural
x Natural -> Natural -> Bool
forall a. Eq a => a -> a -> Bool
Haskell.== Natural
0 then i -> m i
forall a. a -> m a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure i
z else ClosedPoly i a -> m i
forall var a w (m :: Type -> Type).
MonadCircuit var a w m =>
ClosedPoly var a -> m var
newAssigned (Natural -> (i -> x) -> x
forall a b. FromConstant a b => a -> b
fromConstant Natural
x)
  [i]
bi <- forall (r :: Natural) i a w (m :: Type -> Type).
(KnownNat r, MonadCircuit i a w m, Arithmetic a) =>
Natural -> i -> m [i]
expansionW @8 ([i] -> Natural
forall (t :: Type -> Type) a. Foldable t => t a -> Natural
length [i]
bm) i
i
  i
ovf <- forall (r :: Natural) i a w (m :: Type -> Type)
       (f :: Type -> Type).
(Arithmetic a, MonadCircuit i a w m, Zip f, Foldable f,
 KnownNat r) =>
f i -> f i -> m i
blueprintGE @8 ([i] -> [i]
forall a. [a] -> [a]
Haskell.reverse [i]
bi) ([i] -> [i]
forall a. [a] -> [a]
Haskell.reverse [i]
bm)
  i
res <- ClosedPoly i a -> m i
forall var a w (m :: Type -> Type).
MonadCircuit var a w m =>
ClosedPoly var a -> m var
newAssigned (((i -> x) -> i -> x
forall a b. (a -> b) -> a -> b
$ i
i) ((i -> x) -> x) -> ((i -> x) -> x) -> (i -> x) -> x
forall a. AdditiveGroup a => a -> a -> a
- ((i -> x) -> i -> x
forall a b. (a -> b) -> a -> b
$ i
ovf) ((i -> x) -> x) -> ((i -> x) -> x) -> (i -> x) -> x
forall a. MultiplicativeSemigroup a => a -> a -> a
* Natural -> (i -> x) -> x
forall a b. FromConstant a b => a -> b
fromConstant Natural
m)
  (i, i) -> m (i, i)
forall a. a -> m a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (i
res, i
ovf)

condSub :: (MonadCircuit i a w m, Arithmetic a) => Natural -> i -> m i
condSub :: forall i a w (m :: Type -> Type).
(MonadCircuit i a w m, Arithmetic a) =>
Natural -> i -> m i
condSub Natural
m i
x = (i, i) -> i
forall a b. (a, b) -> a
fst ((i, i) -> i) -> m (i, i) -> m i
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Natural -> i -> m (i, i)
forall i a w (m :: Type -> Type).
(MonadCircuit i a w m, Arithmetic a) =>
Natural -> i -> m (i, i)
condSubOF Natural
m i
x

smallCut :: forall i a w m. (Arithmetic a, MonadCircuit i a w m) => Vector Size i -> m (Vector Size i)
smallCut :: forall i a w (m :: Type -> Type).
(Arithmetic a, MonadCircuit i a w m) =>
Vector Size i -> m (Vector Size i)
smallCut = (Natural -> i -> m i)
-> Vector Size Natural -> Vector Size i -> m (Vector Size i)
forall (f :: Type -> Type) (m :: Type -> Type) a b c.
(Traversable f, Zip f, Applicative m) =>
(a -> b -> m c) -> f a -> f b -> m (f c)
zipWithM Natural -> i -> m i
forall i a w (m :: Type -> Type).
(MonadCircuit i a w m, Arithmetic a) =>
Natural -> i -> m i
condSub (Vector Size Natural -> Vector Size i -> m (Vector Size i))
-> Vector Size Natural -> Vector Size i -> m (Vector Size i)
forall a b. (a -> b) -> a -> b
$ forall a. Finite a => Vector Size Natural
coprimes @a

bigSub :: (Arithmetic a, MonadCircuit i a w m) => Natural -> i -> m i
bigSub :: forall a i w (m :: Type -> Type).
(Arithmetic a, MonadCircuit i a w m) =>
Natural -> i -> m i
bigSub Natural
m i
j = i -> m i
trimPow i
j m i -> (i -> m i) -> m i
forall a b. m a -> (a -> m b) -> m b
forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
>>= i -> m i
trimPow m i -> (i -> m i) -> m i
forall a b. m a -> (a -> m b) -> m b
forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
>>= Natural -> i -> m i
forall i a w (m :: Type -> Type).
(MonadCircuit i a w m, Arithmetic a) =>
Natural -> i -> m i
condSub Natural
m
  where
    s :: Natural
s = Double -> Natural
forall b. Integral b => Double -> b
forall a b. (RealFrac a, Integral b) => a -> b
Haskell.ceiling (Natural -> Double
log2 Natural
m) :: Natural
    trimPow :: i -> m i
trimPow i
i = do
      (i
l, i
h) <- Natural -> Natural -> i -> m (i, i)
forall i a w (m :: Type -> Type).
(MonadCircuit i a w m, Arithmetic a) =>
Natural -> Natural -> i -> m (i, i)
splitExpansion Natural
s Natural
s i
i
      ClosedPoly i a -> m i
forall var a w (m :: Type -> Type).
MonadCircuit var a w m =>
ClosedPoly var a -> m var
newAssigned (((i -> x) -> i -> x
forall a b. (a -> b) -> a -> b
$ i
l) ((i -> x) -> x) -> ((i -> x) -> x) -> (i -> x) -> x
forall a. AdditiveSemigroup a => a -> a -> a
+ ((i -> x) -> i -> x
forall a b. (a -> b) -> a -> b
$ i
h) ((i -> x) -> x) -> ((i -> x) -> x) -> (i -> x) -> x
forall a. MultiplicativeSemigroup a => a -> a -> a
* Natural -> (i -> x) -> x
forall a b. FromConstant a b => a -> b
fromConstant ((Natural
2 Natural -> Natural -> Natural
forall a b. Exponent a b => a -> b -> a
^ Natural
s) Natural -> Natural -> Natural
-! Natural
m))

bigCut :: forall i a w m. (Arithmetic a, MonadCircuit i a w m) => Vector Size i -> m (Vector Size i)
bigCut :: forall i a w (m :: Type -> Type).
(Arithmetic a, MonadCircuit i a w m) =>
Vector Size i -> m (Vector Size i)
bigCut = (Natural -> i -> m i)
-> Vector Size Natural -> Vector Size i -> m (Vector Size i)
forall (f :: Type -> Type) (m :: Type -> Type) a b c.
(Traversable f, Zip f, Applicative m) =>
(a -> b -> m c) -> f a -> f b -> m (f c)
zipWithM Natural -> i -> m i
forall a i w (m :: Type -> Type).
(Arithmetic a, MonadCircuit i a w m) =>
Natural -> i -> m i
bigSub (Vector Size Natural -> Vector Size i -> m (Vector Size i))
-> Vector Size Natural -> Vector Size i -> m (Vector Size i)
forall a b. (a -> b) -> a -> b
$ forall a. Finite a => Vector Size Natural
coprimes @a

cast :: forall p i a w m. (KnownNat p, Arithmetic a, MonadCircuit i a w m) => Vector Size i -> m (Vector Size i)
cast :: forall (p :: Natural) i a w (m :: Type -> Type).
(KnownNat p, Arithmetic a, MonadCircuit i a w m) =>
Vector Size i -> m (Vector Size i)
cast Vector Size i
xs = do
  Vector Size i
gs <- (i -> Natural -> m i)
-> Vector Size i -> Vector Size Natural -> m (Vector Size i)
forall (f :: Type -> Type) (m :: Type -> Type) a b c.
(Traversable f, Zip f, Applicative m) =>
(a -> b -> m c) -> f a -> f b -> m (f c)
zipWithM (\i
i Natural
m -> ClosedPoly i a -> m i
forall var a w (m :: Type -> Type).
MonadCircuit var a w m =>
ClosedPoly var a -> m var
newAssigned (ClosedPoly i a -> m i) -> ClosedPoly i a -> m i
forall a b. (a -> b) -> a -> b
$ ((i -> x) -> i -> x
forall a b. (a -> b) -> a -> b
$ i
i) ((i -> x) -> x) -> ((i -> x) -> x) -> (i -> x) -> x
forall a. MultiplicativeSemigroup a => a -> a -> a
* Natural -> (i -> x) -> x
forall a b. FromConstant a b => a -> b
fromConstant Natural
m) Vector Size i
xs (forall a. Finite a => Vector Size Natural
minv @a) m (Vector Size i)
-> (Vector Size i -> m (Vector Size i)) -> m (Vector Size i)
forall a b. m a -> (a -> m b) -> m b
forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
>>= Vector Size i -> m (Vector Size i)
forall i a w (m :: Type -> Type).
(Arithmetic a, MonadCircuit i a w m) =>
Vector Size i -> m (Vector Size i)
bigCut
  i
zi <- ClosedPoly i a -> m i
forall var a w (m :: Type -> Type).
MonadCircuit var a w m =>
ClosedPoly var a -> m var
newAssigned (x -> (i -> x) -> x
forall a b. a -> b -> a
const x
forall a. AdditiveMonoid a => a
zero)
  let binary :: i -> Natural -> m i
binary i
g Natural
m = (i, i) -> i
forall a b. (a, b) -> b
snd ((i, i) -> i) -> m (i, i) -> m i
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Natural -> ((i, i) -> m (i, i)) -> (i, i) -> m (i, i)
forall (m :: Type -> Type) a.
Monad m =>
Natural -> (a -> m a) -> a -> m a
iterateM Natural
sigma (Natural -> (i, i) -> m (i, i)
binstep Natural
m) (i
g, i
zi)
      binstep :: Natural -> (i, i) -> m (i, i)
binstep Natural
m (i
i, i
ci) = do
        (i
i', i
j) <- ClosedPoly i a -> m i
forall var a w (m :: Type -> Type).
MonadCircuit var a w m =>
ClosedPoly var a -> m var
newAssigned (((i -> x) -> i -> x
forall a b. (a -> b) -> a -> b
$ i
i) ((i -> x) -> x) -> ((i -> x) -> x) -> (i -> x) -> x
forall a. AdditiveSemigroup a => a -> a -> a
+ ((i -> x) -> i -> x
forall a b. (a -> b) -> a -> b
$ i
i)) m i -> (i -> m (i, i)) -> m (i, i)
forall a b. m a -> (a -> m b) -> m b
forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall i a w (m :: Type -> Type).
(MonadCircuit i a w m, Arithmetic a) =>
Natural -> i -> m (i, i)
condSubOF @i @a @w @m Natural
m
        i
ci' <- ClosedPoly i a -> m i
forall var a w (m :: Type -> Type).
MonadCircuit var a w m =>
ClosedPoly var a -> m var
newAssigned (((i -> x) -> i -> x
forall a b. (a -> b) -> a -> b
$ i
ci) ((i -> x) -> x) -> ((i -> x) -> x) -> (i -> x) -> x
forall a. AdditiveSemigroup a => a -> a -> a
+ ((i -> x) -> i -> x
forall a b. (a -> b) -> a -> b
$ i
ci) ((i -> x) -> x) -> ((i -> x) -> x) -> (i -> x) -> x
forall a. AdditiveSemigroup a => a -> a -> a
+ ((i -> x) -> i -> x
forall a b. (a -> b) -> a -> b
$ i
j))
        (i, i) -> m (i, i)
forall a. a -> m a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (i
i', i
ci')
  i
base <- ClosedPoly i a -> m i
forall var a w (m :: Type -> Type).
MonadCircuit var a w m =>
ClosedPoly var a -> m var
newAssigned (Natural -> (i -> x) -> x
forall a b. FromConstant a b => a -> b
fromConstant (Natural
3 Natural -> Natural -> Natural
forall a. MultiplicativeSemigroup a => a -> a -> a
* (Natural
2 Natural -> Natural -> Natural
forall a b. Exponent a b => a -> b -> a
^ (Natural
sigma Natural -> Natural -> Natural
-! Natural
2)) :: Natural))
  let ms :: Vector Size Natural
ms = forall a. Finite a => Vector Size Natural
coprimes @a
  i
residue <- (i -> Natural -> m i)
-> Vector Size i -> Vector Size Natural -> m (Vector Size i)
forall (f :: Type -> Type) (m :: Type -> Type) a b c.
(Traversable f, Zip f, Applicative m) =>
(a -> b -> m c) -> f a -> f b -> m (f c)
zipWithM i -> Natural -> m i
binary Vector Size i
gs Vector Size Natural
ms
        m (Vector Size i) -> (Vector Size i -> m i) -> m i
forall a b. m a -> (a -> m b) -> m b
forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
>>= (i -> i -> m i) -> i -> Vector Size i -> m i
forall (t :: Type -> Type) (m :: Type -> Type) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldlM (\i
i i
j -> ClosedPoly i a -> m i
forall var a w (m :: Type -> Type).
MonadCircuit var a w m =>
ClosedPoly var a -> m var
newAssigned (((i -> x) -> i -> x
forall a b. (a -> b) -> a -> b
$ i
i) ((i -> x) -> x) -> ((i -> x) -> x) -> (i -> x) -> x
forall a. AdditiveSemigroup a => a -> a -> a
+ ((i -> x) -> i -> x
forall a b. (a -> b) -> a -> b
$ i
j))) i
base
        m i -> (i -> m i) -> m i
forall a b. m a -> (a -> m b) -> m b
forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
>>= (((i, i) -> i) -> m (i, i) -> m 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, i) -> i
forall a b. (a, b) -> b
snd (m (i, i) -> m i) -> (i -> m (i, i)) -> i -> m i
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Natural -> Natural -> i -> m (i, i)
forall i a w (m :: Type -> Type).
(MonadCircuit i a w m, Arithmetic a) =>
Natural -> Natural -> i -> m (i, i)
splitExpansion Natural
sigma (forall a. KnownNat (NumberOfBits a) => Natural
numberOfBits @a Natural -> Natural -> Natural
-! Natural
sigma))
  Vector Size Natural -> (Natural -> m i) -> m (Vector Size i)
forall (t :: Type -> Type) (f :: Type -> Type) a b.
(Traversable t, Applicative f) =>
t a -> (a -> f b) -> f (t b)
for Vector Size Natural
ms ((Natural -> m i) -> m (Vector Size i))
-> (Natural -> m i) -> m (Vector Size i)
forall a b. (a -> b) -> a -> b
$ \Natural
m -> do
    i
dot <- (i -> Natural -> m i)
-> Vector Size i -> Vector Size Natural -> m (Vector Size i)
forall (f :: Type -> Type) (m :: Type -> Type) a b c.
(Traversable f, Zip f, Applicative m) =>
(a -> b -> m c) -> f a -> f b -> m (f c)
zipWithM (\i
i Natural
x -> ClosedPoly i a -> m i
forall var a w (m :: Type -> Type).
MonadCircuit var a w m =>
ClosedPoly var a -> m var
newAssigned (((i -> x) -> i -> x
forall a b. (a -> b) -> a -> b
$ i
i) ((i -> x) -> x) -> ((i -> x) -> x) -> (i -> x) -> x
forall a. MultiplicativeSemigroup a => a -> a -> a
* Natural -> (i -> x) -> x
forall a b. FromConstant a b => a -> b
fromConstant (Natural
x Natural -> Natural -> Natural
forall a. SemiEuclidean a => a -> a -> a
`mod` Natural
m))) Vector Size i
gs (forall a (p :: Natural).
(Finite a, KnownNat p) =>
Vector Size Natural
mis @a @p)
            m (Vector Size i)
-> (Vector Size i -> m (Vector Size i)) -> m (Vector Size i)
forall a b. m a -> (a -> m b) -> m b
forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
>>= (i -> m i) -> Vector Size i -> m (Vector Size i)
forall (t :: Type -> Type) (f :: Type -> Type) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: Type -> Type) a b.
Applicative f =>
(a -> f b) -> Vector Size a -> f (Vector Size b)
traverse (Natural -> i -> m i
forall a i w (m :: Type -> Type).
(Arithmetic a, MonadCircuit i a w m) =>
Natural -> i -> m i
bigSub Natural
m)
            m (Vector Size i) -> (Vector Size i -> m i) -> m i
forall a b. m a -> (a -> m b) -> m b
forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
>>= (i -> i -> m i) -> i -> Vector Size i -> m i
forall (t :: Type -> Type) (m :: Type -> Type) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldlM (\i
i i
j -> ClosedPoly i a -> m i
forall var a w (m :: Type -> Type).
MonadCircuit var a w m =>
ClosedPoly var a -> m var
newAssigned (((i -> x) -> i -> x
forall a b. (a -> b) -> a -> b
$ i
i) ((i -> x) -> x) -> ((i -> x) -> x) -> (i -> x) -> x
forall a. AdditiveSemigroup a => a -> a -> a
+ ((i -> x) -> i -> x
forall a b. (a -> b) -> a -> b
$ i
j))) i
zi
    ClosedPoly i a -> m i
forall var a w (m :: Type -> Type).
MonadCircuit var a w m =>
ClosedPoly var a -> m var
newAssigned (((i -> x) -> i -> x
forall a b. (a -> b) -> a -> b
$ i
dot) ((i -> x) -> x) -> ((i -> x) -> x) -> (i -> x) -> x
forall a. AdditiveSemigroup a => a -> a -> a
+ Natural -> (i -> x) -> x
forall a b. FromConstant a b => a -> b
fromConstant (Natural
m Natural -> Natural -> Natural
-! (forall a (p :: Natural). (Finite a, KnownNat p) => Natural
mprod @a @p Natural -> Natural -> Natural
forall a. SemiEuclidean a => a -> a -> a
`mod` Natural
m)) ((i -> x) -> x) -> ((i -> x) -> x) -> (i -> x) -> x
forall a. MultiplicativeSemigroup a => a -> a -> a
* ((i -> x) -> i -> x
forall a b. (a -> b) -> a -> b
$ i
residue))
        m i -> (i -> m i) -> m i
forall a b. m a -> (a -> m b) -> m b
forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
>>= Natural -> i -> m i
forall a i w (m :: Type -> Type).
(Arithmetic a, MonadCircuit i a w m) =>
Natural -> i -> m i
bigSub Natural
m

mul :: forall p i a w m. (KnownNat p, Arithmetic a, NFData i, MonadCircuit i a w m) => Vector Size i -> Vector Size i -> m (Vector Size i)
mul :: forall (p :: Natural) i a w (m :: Type -> Type).
(KnownNat p, Arithmetic a, NFData i, MonadCircuit i a w m) =>
Vector Size i -> Vector Size i -> m (Vector Size i)
mul Vector Size i
xs Vector Size i
ys = (Vector Size i -> Vector Size i)
-> m (Vector Size i) -> m (Vector Size i)
forall a b. (a -> b) -> m a -> m b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
Haskell.fmap Vector Size i -> Vector Size i
forall a. NFData a => a -> a
force (m (Vector Size i) -> m (Vector Size i))
-> m (Vector Size i) -> m (Vector Size i)
forall a b. (a -> b) -> a -> b
$ (i -> i -> m i)
-> Vector Size i -> Vector Size i -> m (Vector Size i)
forall (f :: Type -> Type) (m :: Type -> Type) a b c.
(Traversable f, Zip f, Applicative m) =>
(a -> b -> m c) -> f a -> f b -> m (f c)
zipWithM (\i
i i
j -> ClosedPoly i a -> 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)) Vector Size i
xs Vector Size i
ys m (Vector Size i)
-> (Vector Size i -> m (Vector Size i)) -> m (Vector Size i)
forall a b. m a -> (a -> m b) -> m b
forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
>>= Vector Size i -> m (Vector Size i)
forall i a w (m :: Type -> Type).
(Arithmetic a, MonadCircuit i a w m) =>
Vector Size i -> m (Vector Size i)
bigCut m (Vector Size i)
-> (Vector Size i -> m (Vector Size i)) -> m (Vector Size i)
forall a b. m a -> (a -> m b) -> m b
forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall (p :: Natural) i a w (m :: Type -> Type).
(KnownNat p, Arithmetic a, MonadCircuit i a w m) =>
Vector Size i -> m (Vector Size i)
cast @p

natPowM :: Monad m => (a -> a -> m a) -> m a -> Natural -> a -> m a
natPowM :: forall (m :: Type -> Type) a.
Monad m =>
(a -> a -> m a) -> m a -> Natural -> a -> m a
natPowM a -> a -> m a
_ m a
z Natural
0 a
_ = m a
z
natPowM a -> a -> m a
_ m a
_ Natural
1 a
x = a -> m a
forall a. a -> m a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure a
x
natPowM a -> a -> m a
f m a
z Natural
n a
x
  | Natural -> Bool
forall a. Integral a => a -> Bool
Haskell.even Natural
n    = (a -> a -> m a) -> m a -> Natural -> a -> m a
forall (m :: Type -> Type) a.
Monad m =>
(a -> a -> m a) -> m a -> Natural -> a -> m a
natPowM a -> a -> m a
f m a
z (Natural
n Natural -> Natural -> Natural
forall a. SemiEuclidean a => a -> a -> a
`div` Natural
2) a
x m a -> (a -> m a) -> m a
forall a b. m a -> (a -> m b) -> m b
forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
>>= \a
y -> a -> a -> m a
f a
y a
y
  | Bool
Haskell.otherwise = (a -> a -> m a) -> m a -> Natural -> a -> m a
forall (m :: Type -> Type) a.
Monad m =>
(a -> a -> m a) -> m a -> Natural -> a -> m a
natPowM a -> a -> m a
f m a
z (Natural
n Natural -> Natural -> Natural
-! Natural
1) a
x m a -> (a -> m a) -> m a
forall a b. m a -> (a -> m b) -> m b
forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
>>= a -> a -> m a
f a
x

oneM :: MonadCircuit i a w m => m (Vector Size i)
oneM :: forall i a w (m :: Type -> Type).
MonadCircuit i a w m =>
m (Vector Size i)
oneM = i -> Vector Size i
forall a. a -> Vector Size a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (i -> Vector Size i) -> m i -> m (Vector Size i)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> ClosedPoly i a -> m i
forall var a w (m :: Type -> Type).
MonadCircuit var a w m =>
ClosedPoly var a -> m var
newAssigned (x -> (i -> x) -> x
forall a b. a -> b -> a
const x
forall a. MultiplicativeMonoid a => a
one)

instance (KnownNat p, Arithmetic a) => ToConstant (FFA p (Interpreter a)) where
  type Const (FFA p (Interpreter a)) = Zp p
  toConstant :: FFA p (Interpreter a) -> Const (FFA p (Interpreter a))
toConstant (FFA (Interpreter Vector Size a
rs)) = Vector Size a -> Zp p
forall (p :: Natural) a.
(Arithmetic a, KnownNat p) =>
Vector Size a -> Zp p
toZp Vector Size a
rs

instance (FromConstant a (Zp p), Symbolic c) => FromConstant a (FFA p c) where
  fromConstant :: a -> FFA p c
fromConstant = c (Vector Size) -> FFA p c
forall (p :: Natural) (c :: (Type -> Type) -> Type).
c (Vector Size) -> FFA p c
FFA (c (Vector Size) -> FFA p c)
-> (a -> c (Vector Size)) -> a -> FFA p c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Vector Size (BaseField c) -> c (Vector Size)
forall (c :: (Type -> Type) -> Type) (f :: Type -> Type).
(Symbolic c, Functor f) =>
f (BaseField c) -> c f
embed (Vector Size (BaseField c) -> c (Vector Size))
-> (a -> Vector Size (BaseField c)) -> a -> c (Vector Size)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Natural -> Vector Size (BaseField c)
impl (Natural -> Vector Size (BaseField c))
-> (a -> Natural) -> a -> Vector Size (BaseField c)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Zp p -> Natural
Zp p -> Const (Zp p)
forall a. ToConstant a => a -> Const a
toConstant (Zp p -> Natural) -> (a -> Zp p) -> a -> Natural
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> Zp p
forall a b. FromConstant a b => a -> b
fromConstant :: a -> Zp p)
    where
      impl :: Natural -> Vector Size (BaseField c)
      impl :: Natural -> Vector Size (BaseField c)
impl Natural
x = Natural -> BaseField c
forall a b. FromConstant a b => a -> b
fromConstant (Natural -> BaseField c)
-> (Natural -> Natural) -> Natural -> BaseField c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Natural
x Natural -> Natural -> Natural
forall a. SemiEuclidean a => a -> a -> a
`mod`) (Natural -> BaseField c)
-> Vector Size Natural -> Vector Size (BaseField c)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. Finite a => Vector Size Natural
coprimes @(BaseField c)

instance {-# OVERLAPPING #-} FromConstant (FFA p c) (FFA p c)

instance {-# OVERLAPPING #-} (KnownNat p, Symbolic c) => Scale (FFA p c) (FFA p c)

instance (KnownNat p, Symbolic c) => MultiplicativeSemigroup (FFA p c) where
  FFA c (Vector Size)
x * :: FFA p c -> FFA p c -> FFA p c
* FFA c (Vector Size)
y =
    c (Vector Size) -> FFA p c
forall (p :: Natural) (c :: (Type -> Type) -> Type).
c (Vector Size) -> FFA p c
FFA (c (Vector Size) -> FFA p c) -> c (Vector Size) -> FFA p c
forall a b. (a -> b) -> a -> b
$ c (Vector Size)
-> c (Vector Size)
-> (Vector Size (BaseField c)
    -> Vector Size (BaseField c) -> Vector Size (BaseField c))
-> CircuitFun '[Vector Size, Vector Size] (Vector Size) c
-> c (Vector Size)
forall (c :: (Type -> Type) -> Type) a (f :: Type -> Type)
       (g :: Type -> Type) (h :: Type -> Type).
(Symbolic c, BaseField c ~ a) =>
c f -> c g -> (f a -> g a -> h a) -> CircuitFun '[f, g] h c -> c h
symbolic2F c (Vector Size)
x c (Vector Size)
y (\Vector Size (BaseField c)
u Vector Size (BaseField c)
v -> Zp p -> Vector Size (BaseField c)
forall (p :: Natural) a. Arithmetic a => Zp p -> Vector Size a
fromZp (Vector Size (BaseField c) -> Zp p
forall (p :: Natural) a.
(Arithmetic a, KnownNat p) =>
Vector Size a -> Zp p
toZp Vector Size (BaseField c)
u Zp p -> Zp p -> Zp p
forall a. MultiplicativeSemigroup a => a -> a -> a
* Vector Size (BaseField c) -> Zp p
forall (p :: Natural) a.
(Arithmetic a, KnownNat p) =>
Vector Size a -> Zp p
toZp Vector Size (BaseField c)
v :: Zp p)) (forall (p :: Natural) i a w (m :: Type -> Type).
(KnownNat p, Arithmetic a, NFData i, MonadCircuit i a w m) =>
Vector Size i -> Vector Size i -> m (Vector Size i)
mul @p)

instance (KnownNat p, Symbolic c) => Exponent (FFA p c) Natural where
  FFA c (Vector Size)
x ^ :: FFA p c -> Natural -> FFA p c
^ Natural
a =
    c (Vector Size) -> FFA p c
forall (p :: Natural) (c :: (Type -> Type) -> Type).
c (Vector Size) -> FFA p c
FFA (c (Vector Size) -> FFA p c) -> c (Vector Size) -> FFA p c
forall a b. (a -> b) -> a -> b
$ c (Vector Size)
-> (Vector Size (BaseField c) -> Vector Size (BaseField c))
-> (forall {i} {m :: Type -> Type}.
    (NFData i, MonadCircuit i (BaseField c) (WitnessField c) m) =>
    FunBody '[Vector Size] (Vector Size) i m)
-> c (Vector Size)
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 Size)
x (\Vector Size (BaseField c)
v -> Zp p -> Vector Size (BaseField c)
forall (p :: Natural) a. Arithmetic a => Zp p -> Vector Size a
fromZp (Vector Size (BaseField c) -> Zp p
forall (p :: Natural) a.
(Arithmetic a, KnownNat p) =>
Vector Size a -> Zp p
toZp Vector Size (BaseField c)
v Zp p -> Natural -> Zp p
forall a b. Exponent a b => a -> b -> a
^ Natural
a :: Zp p)) ((forall {i} {m :: Type -> Type}.
  (NFData i, MonadCircuit i (BaseField c) (WitnessField c) m) =>
  FunBody '[Vector Size] (Vector Size) i m)
 -> c (Vector Size))
-> (forall {i} {m :: Type -> Type}.
    (NFData i, MonadCircuit i (BaseField c) (WitnessField c) m) =>
    FunBody '[Vector Size] (Vector Size) i m)
-> c (Vector Size)
forall a b. (a -> b) -> a -> b
$ (Vector Size i -> Vector Size i -> m (Vector Size i))
-> m (Vector Size i)
-> Natural
-> Vector Size i
-> m (Vector Size i)
forall (m :: Type -> Type) a.
Monad m =>
(a -> a -> m a) -> m a -> Natural -> a -> m a
natPowM (forall (p :: Natural) i a w (m :: Type -> Type).
(KnownNat p, Arithmetic a, NFData i, MonadCircuit i a w m) =>
Vector Size i -> Vector Size i -> m (Vector Size i)
mul @p) m (Vector Size i)
forall i a w (m :: Type -> Type).
MonadCircuit i a w m =>
m (Vector Size i)
oneM Natural
a

instance (KnownNat p, Symbolic c) => MultiplicativeMonoid (FFA p c) where
  one :: FFA p c
one = Zp p -> FFA p c
forall a b. FromConstant a b => a -> b
fromConstant (Zp p
forall a. MultiplicativeMonoid a => a
one :: Zp p)

instance (KnownNat p, Symbolic c) => AdditiveSemigroup (FFA p c) where
  FFA c (Vector Size)
x + :: FFA p c -> FFA p c -> FFA p c
+ FFA c (Vector Size)
y =
    c (Vector Size) -> FFA p c
forall (p :: Natural) (c :: (Type -> Type) -> Type).
c (Vector Size) -> FFA p c
FFA (c (Vector Size) -> FFA p c) -> c (Vector Size) -> FFA p c
forall a b. (a -> b) -> a -> b
$ c (Vector Size)
-> c (Vector Size)
-> (Vector Size (BaseField c)
    -> Vector Size (BaseField c) -> Vector Size (BaseField c))
-> (forall {i} {m :: Type -> Type}.
    (NFData i, MonadCircuit i (BaseField c) (WitnessField c) m) =>
    FunBody '[Vector Size, Vector Size] (Vector Size) i m)
-> c (Vector Size)
forall (c :: (Type -> Type) -> Type) a (f :: Type -> Type)
       (g :: Type -> Type) (h :: Type -> Type).
(Symbolic c, BaseField c ~ a) =>
c f -> c g -> (f a -> g a -> h a) -> CircuitFun '[f, g] h c -> c h
symbolic2F c (Vector Size)
x c (Vector Size)
y (\Vector Size (BaseField c)
u Vector Size (BaseField c)
v -> Zp p -> Vector Size (BaseField c)
forall (p :: Natural) a. Arithmetic a => Zp p -> Vector Size a
fromZp (Vector Size (BaseField c) -> Zp p
forall (p :: Natural) a.
(Arithmetic a, KnownNat p) =>
Vector Size a -> Zp p
toZp Vector Size (BaseField c)
u Zp p -> Zp p -> Zp p
forall a. AdditiveSemigroup a => a -> a -> a
+ Vector Size (BaseField c) -> Zp p
forall (p :: Natural) a.
(Arithmetic a, KnownNat p) =>
Vector Size a -> Zp p
toZp Vector Size (BaseField c)
v :: Zp p)) ((forall {i} {m :: Type -> Type}.
  (NFData i, MonadCircuit i (BaseField c) (WitnessField c) m) =>
  FunBody '[Vector Size, Vector Size] (Vector Size) i m)
 -> c (Vector Size))
-> (forall {i} {m :: Type -> Type}.
    (NFData i, MonadCircuit i (BaseField c) (WitnessField c) m) =>
    FunBody '[Vector Size, Vector Size] (Vector Size) i m)
-> c (Vector Size)
forall a b. (a -> b) -> a -> b
$ \Vector Size i
xs Vector Size i
ys ->
      (i -> i -> m i)
-> Vector Size i -> Vector Size i -> m (Vector Size i)
forall (f :: Type -> Type) (m :: Type -> Type) a b c.
(Traversable f, Zip f, Applicative m) =>
(a -> b -> m c) -> f a -> f b -> m (f c)
zipWithM (\i
i i
j -> 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)) Vector Size i
xs Vector Size i
ys m (Vector Size i)
-> (Vector Size i -> m (Vector Size i)) -> m (Vector Size i)
forall a b. m a -> (a -> m b) -> m b
forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
>>= Vector Size i -> m (Vector Size i)
forall i a w (m :: Type -> Type).
(Arithmetic a, MonadCircuit i a w m) =>
Vector Size i -> m (Vector Size i)
smallCut m (Vector Size i)
-> (Vector Size i -> m (Vector Size i)) -> m (Vector Size i)
forall a b. m a -> (a -> m b) -> m b
forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall (p :: Natural) i a w (m :: Type -> Type).
(KnownNat p, Arithmetic a, MonadCircuit i a w m) =>
Vector Size i -> m (Vector Size i)
cast @p

instance (KnownNat p, Scale a (Zp p), Symbolic c) => Scale a (FFA p c) where
  scale :: a -> FFA p c -> FFA p c
scale a
k FFA p c
x = Zp p -> FFA p c
forall a b. FromConstant a b => a -> b
fromConstant (a -> Zp p -> Zp p
forall b a. Scale b a => b -> a -> a
scale a
k Zp p
forall a. MultiplicativeMonoid a => a
one :: Zp p) FFA p c -> FFA p c -> FFA p c
forall a. MultiplicativeSemigroup a => a -> a -> a
* FFA p c
x

instance (KnownNat p, Symbolic c) => AdditiveMonoid (FFA p c) where
  zero :: FFA p c
zero = Zp p -> FFA p c
forall a b. FromConstant a b => a -> b
fromConstant (Zp p
forall a. AdditiveMonoid a => a
zero :: Zp p)

instance (KnownNat p, Symbolic c) => AdditiveGroup (FFA p c) where
  negate :: FFA p c -> FFA p c
negate (FFA c (Vector Size)
x) = c (Vector Size) -> FFA p c
forall (p :: Natural) (c :: (Type -> Type) -> Type).
c (Vector Size) -> FFA p c
FFA (c (Vector Size) -> FFA p c) -> c (Vector Size) -> FFA p c
forall a b. (a -> b) -> a -> b
$ c (Vector Size)
-> (Vector Size (BaseField c) -> Vector Size (BaseField c))
-> (forall {i} {m :: Type -> Type}.
    (NFData i, MonadCircuit i (BaseField c) (WitnessField c) m) =>
    FunBody '[Vector Size] (Vector Size) i m)
-> c (Vector Size)
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 Size)
x (Zp p -> Vector Size (BaseField c)
forall (p :: Natural) a. Arithmetic a => Zp p -> Vector Size a
fromZp (Zp p -> Vector Size (BaseField c))
-> (Vector Size (BaseField c) -> Zp p)
-> Vector Size (BaseField c)
-> Vector Size (BaseField c)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Zp p -> Zp p
forall a. AdditiveGroup a => a -> a
negate (Zp p -> Zp p)
-> (Vector Size (BaseField c) -> Zp p)
-> Vector Size (BaseField c)
-> Zp p
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (p :: Natural) a.
(Arithmetic a, KnownNat p) =>
Vector Size a -> Zp p
toZp @p) ((forall {i} {m :: Type -> Type}.
  (NFData i, MonadCircuit i (BaseField c) (WitnessField c) m) =>
  FunBody '[Vector Size] (Vector Size) i m)
 -> c (Vector Size))
-> (forall {i} {m :: Type -> Type}.
    (NFData i, MonadCircuit i (BaseField c) (WitnessField c) m) =>
    FunBody '[Vector Size] (Vector Size) i m)
-> c (Vector Size)
forall a b. (a -> b) -> a -> b
$ \Vector Size i
xs -> do
    let cs :: Vector Size Natural
cs = forall a. Finite a => Vector Size Natural
coprimes @(BaseField c)
    Vector Size i
ys <- (i -> Natural -> m i)
-> Vector Size i -> Vector Size Natural -> m (Vector Size i)
forall (f :: Type -> Type) (m :: Type -> Type) a b c.
(Traversable f, Zip f, Applicative m) =>
(a -> b -> m c) -> f a -> f b -> m (f c)
zipWithM (\i
i Natural
m -> ClosedPoly i (BaseField c) -> m i
forall var a w (m :: Type -> Type).
MonadCircuit var a w m =>
ClosedPoly var a -> m var
newAssigned (ClosedPoly i (BaseField c) -> m i)
-> ClosedPoly i (BaseField c) -> m i
forall a b. (a -> b) -> a -> b
$ Natural -> (i -> x) -> x
forall a b. FromConstant a b => a -> b
fromConstant Natural
m ((i -> x) -> x) -> ((i -> x) -> x) -> (i -> x) -> x
forall a. AdditiveGroup a => a -> a -> a
- ((i -> x) -> i -> x
forall a b. (a -> b) -> a -> b
$ i
i)) Vector Size i
xs Vector Size Natural
cs
    forall (p :: Natural) i a w (m :: Type -> Type).
(KnownNat p, Arithmetic a, MonadCircuit i a w m) =>
Vector Size i -> m (Vector Size i)
cast @p Vector Size i
ys

instance (KnownNat p, Symbolic c) => Semiring (FFA p c)

instance (KnownNat p, Symbolic c) => Ring (FFA p c)

instance (Prime p, Symbolic c) => Exponent (FFA p c) Integer where
  FFA p c
x ^ :: FFA p c -> Integer -> FFA p c
^ Integer
a = FFA p c
x FFA p c -> Integer -> FFA p c
forall a. Field a => a -> Integer -> a
`intPowF` (Integer
a Integer -> Integer -> Integer
forall a. SemiEuclidean a => a -> a -> a
`mod` Natural -> Integer
forall a b. FromConstant a b => a -> b
fromConstant (forall (n :: Natural). KnownNat n => Natural
value @p Natural -> Natural -> Natural
-! Natural
1))

instance (Prime p, Symbolic c) => Field (FFA p c) where
  finv :: FFA p c -> FFA p c
finv (FFA c (Vector Size)
x) =
    c (Vector Size) -> FFA p c
forall (p :: Natural) (c :: (Type -> Type) -> Type).
c (Vector Size) -> FFA p c
FFA (c (Vector Size) -> FFA p c) -> c (Vector Size) -> FFA p c
forall a b. (a -> b) -> a -> b
$ c (Vector Size)
-> (Vector Size (BaseField c) -> Vector Size (BaseField c))
-> (forall {i} {m :: Type -> Type}.
    (NFData i, MonadCircuit i (BaseField c) (WitnessField c) m) =>
    FunBody '[Vector Size] (Vector Size) i m)
-> c (Vector Size)
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 Size)
x (Zp p -> Vector Size (BaseField c)
forall (p :: Natural) a. Arithmetic a => Zp p -> Vector Size a
fromZp (Zp p -> Vector Size (BaseField c))
-> (Vector Size (BaseField c) -> Zp p)
-> Vector Size (BaseField c)
-> Vector Size (BaseField c)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Field a => a -> a
finv @(Zp p) (Zp p -> Zp p)
-> (Vector Size (BaseField c) -> Zp p)
-> Vector Size (BaseField c)
-> Zp p
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Vector Size (BaseField c) -> Zp p
forall (p :: Natural) a.
(Arithmetic a, KnownNat p) =>
Vector Size a -> Zp p
toZp)
      ((forall {i} {m :: Type -> Type}.
  (NFData i, MonadCircuit i (BaseField c) (WitnessField c) m) =>
  FunBody '[Vector Size] (Vector Size) i m)
 -> c (Vector Size))
-> (forall {i} {m :: Type -> Type}.
    (NFData i, MonadCircuit i (BaseField c) (WitnessField c) m) =>
    FunBody '[Vector Size] (Vector Size) i m)
-> c (Vector Size)
forall a b. (a -> b) -> a -> b
$ (Vector Size i -> Vector Size i -> m (Vector Size i))
-> m (Vector Size i)
-> Natural
-> Vector Size i
-> m (Vector Size i)
forall (m :: Type -> Type) a.
Monad m =>
(a -> a -> m a) -> m a -> Natural -> a -> m a
natPowM (forall (p :: Natural) i a w (m :: Type -> Type).
(KnownNat p, Arithmetic a, NFData i, MonadCircuit i a w m) =>
Vector Size i -> Vector Size i -> m (Vector Size i)
mul @p) m (Vector Size i)
forall i a w (m :: Type -> Type).
MonadCircuit i a w m =>
m (Vector Size i)
oneM (forall (n :: Natural). KnownNat n => Natural
value @p Natural -> Natural -> Natural
-! Natural
2)

instance Finite (Zp p) => Finite (FFA p b) where
  type Order (FFA p b) = p

-- FIXME: This Eq instance is wrong
deriving newtype instance Symbolic c => Eq (Bool c) (FFA p c)

-- | TODO: fix when rewrite is done
instance (Symbolic c) => SymbolicInput (FFA p c) where
  isValid :: FFA p c -> Bool (Context (FFA p c))
isValid FFA p c
_ = Bool c
Bool (Context (FFA p c))
forall b. BoolType b => b
true