{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE UndecidableInstances #-}
module ZkFold.Symbolic.Data.FFA (FFA (..), Size, coprimesDownFrom, coprimes) where
import Control.Applicative (pure)
import Control.DeepSeq (NFData)
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
newtype FFA (p :: Natural) c = FFA (c (Vector Size))
deriving newtype instance 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
condSubOF :: forall i a m . (MonadCircuit i a m, Arithmetic a) => Natural -> i -> m (i, i)
condSubOF :: forall i a (m :: Type -> Type).
(MonadCircuit i a m, Arithmetic a) =>
Natural -> i -> m (i, i)
condSubOF Natural
m i
i = do
i
z <- ClosedPoly i a -> m i
forall var a (m :: Type -> Type).
MonadCircuit var a 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 (m :: Type -> Type).
MonadCircuit var a 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 (m :: Type -> Type).
(KnownNat r, MonadCircuit i a 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 (m :: Type -> Type) (f :: Type -> Type).
(Arithmetic a, MonadCircuit i a 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 (m :: Type -> Type).
MonadCircuit var a 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 m, Arithmetic a) => Natural -> i -> m i
condSub :: forall i a (m :: Type -> Type).
(MonadCircuit i a 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 (m :: Type -> Type).
(MonadCircuit i a m, Arithmetic a) =>
Natural -> i -> m (i, i)
condSubOF Natural
m i
x
smallCut :: forall i a m. (Arithmetic a, MonadCircuit i a m) => Vector Size i -> m (Vector Size i)
smallCut :: forall i a (m :: Type -> Type).
(Arithmetic a, MonadCircuit i a 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 (m :: Type -> Type).
(MonadCircuit i a 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 m) => Natural -> i -> m i
bigSub :: forall a i (m :: Type -> Type).
(Arithmetic a, MonadCircuit i a 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 (m :: Type -> Type).
(MonadCircuit i a 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 (m :: Type -> Type).
(MonadCircuit i a m, Arithmetic a) =>
Natural -> Natural -> i -> m (i, i)
splitExpansion Natural
s Natural
s i
i
ClosedPoly i a -> m i
forall var a (m :: Type -> Type).
MonadCircuit var a 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 m. (Arithmetic a, MonadCircuit i a m) => Vector Size i -> m (Vector Size i)
bigCut :: forall i a (m :: Type -> Type).
(Arithmetic a, MonadCircuit i a 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 (m :: Type -> Type).
(Arithmetic a, MonadCircuit i a 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 m. (KnownNat p, Arithmetic a, MonadCircuit i a m) => Vector Size i -> m (Vector Size i)
cast :: forall (p :: Natural) i a (m :: Type -> Type).
(KnownNat p, Arithmetic a, MonadCircuit i a 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 (m :: Type -> Type).
MonadCircuit var a 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 (m :: Type -> Type).
(Arithmetic a, MonadCircuit i a m) =>
Vector Size i -> m (Vector Size i)
bigCut
i
zi <- ClosedPoly i a -> m i
forall var a (m :: Type -> Type).
MonadCircuit var a 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 (m :: Type -> Type).
MonadCircuit var a 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 (m :: Type -> Type).
(MonadCircuit i a m, Arithmetic a) =>
Natural -> i -> m (i, i)
condSubOF @i @a @m Natural
m
i
ci' <- ClosedPoly i a -> m i
forall var a (m :: Type -> Type).
MonadCircuit var a 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 (m :: Type -> Type).
MonadCircuit var a 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 (m :: Type -> Type).
MonadCircuit var a 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 (m :: Type -> Type).
(MonadCircuit i a 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 (m :: Type -> Type).
MonadCircuit var a 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 (m :: Type -> Type).
(Arithmetic a, MonadCircuit i a 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 (m :: Type -> Type).
MonadCircuit var a 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 (m :: Type -> Type).
MonadCircuit var a 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 (m :: Type -> Type).
(Arithmetic a, MonadCircuit i a m) =>
Natural -> i -> m i
bigSub Natural
m
mul :: forall p i a m. (KnownNat p, Arithmetic a, MonadCircuit i a m) => Vector Size i -> Vector Size i -> m (Vector Size i)
mul :: forall (p :: Natural) i a (m :: Type -> Type).
(KnownNat p, Arithmetic a, MonadCircuit i a m) =>
Vector Size i -> Vector Size i -> m (Vector Size i)
mul 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 a -> m i
forall var a (m :: Type -> Type).
MonadCircuit var a 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 (m :: Type -> Type).
(Arithmetic a, MonadCircuit i a 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 (m :: Type -> Type).
(KnownNat p, Arithmetic a, MonadCircuit i a 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 m => m (Vector Size i)
oneM :: forall i a (m :: Type -> Type).
MonadCircuit i a 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 (m :: Type -> Type).
MonadCircuit var a 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))
-> (forall i (m :: Type -> Type).
MonadCircuit i (BaseField c) m =>
Vector Size i -> Vector Size i -> m (Vector Size i))
-> 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)
-> (forall i (m :: Type -> Type).
MonadCircuit i a m =>
f i -> g i -> m (h i))
-> 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 (m :: Type -> Type).
(KnownNat p, Arithmetic a, MonadCircuit i a 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}.
MonadCircuit i (BaseField c) m =>
Vector Size i -> m (Vector Size i))
-> c (Vector Size)
forall a (f :: Type -> Type) (g :: Type -> Type).
(BaseField c ~ a) =>
c f -> (f a -> g a) -> CircuitFun f g a -> c g
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 a -> 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}.
MonadCircuit i (BaseField c) m =>
Vector Size i -> m (Vector Size i))
-> c (Vector Size))
-> (forall {i} {m :: Type -> Type}.
MonadCircuit i (BaseField c) m =>
Vector Size i -> m (Vector Size i))
-> 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 (m :: Type -> Type).
(KnownNat p, Arithmetic a, MonadCircuit i a m) =>
Vector Size i -> Vector Size i -> m (Vector Size i)
mul @p) m (Vector Size i)
forall i a (m :: Type -> Type).
MonadCircuit i a 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}.
MonadCircuit i (BaseField c) m =>
Vector Size i -> Vector Size i -> m (Vector Size i))
-> 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)
-> (forall i (m :: Type -> Type).
MonadCircuit i a m =>
f i -> g i -> m (h i))
-> 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}.
MonadCircuit i (BaseField c) m =>
Vector Size i -> Vector Size i -> m (Vector Size i))
-> c (Vector Size))
-> (forall {i} {m :: Type -> Type}.
MonadCircuit i (BaseField c) m =>
Vector Size i -> Vector Size i -> m (Vector Size i))
-> 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 (m :: Type -> Type).
MonadCircuit var a 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 (m :: Type -> Type).
(Arithmetic a, MonadCircuit i a 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 (m :: Type -> Type).
(KnownNat p, Arithmetic a, MonadCircuit i a 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}.
MonadCircuit i (BaseField c) m =>
Vector Size i -> m (Vector Size i))
-> c (Vector Size)
forall a (f :: Type -> Type) (g :: Type -> Type).
(BaseField c ~ a) =>
c f -> (f a -> g a) -> CircuitFun f g a -> c g
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 a -> 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}.
MonadCircuit i (BaseField c) m =>
Vector Size i -> m (Vector Size i))
-> c (Vector Size))
-> (forall {i} {m :: Type -> Type}.
MonadCircuit i (BaseField c) m =>
Vector Size i -> m (Vector Size i))
-> 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 (m :: Type -> Type).
MonadCircuit var a 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 (m :: Type -> Type).
(KnownNat p, Arithmetic a, MonadCircuit i a 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}.
MonadCircuit i (BaseField c) m =>
Vector Size i -> m (Vector Size i))
-> c (Vector Size)
forall a (f :: Type -> Type) (g :: Type -> Type).
(BaseField c ~ a) =>
c f -> (f a -> g a) -> CircuitFun f g a -> c g
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 a -> 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}.
MonadCircuit i (BaseField c) m =>
Vector Size i -> m (Vector Size i))
-> c (Vector Size))
-> (forall {i} {m :: Type -> Type}.
MonadCircuit i (BaseField c) m =>
Vector Size i -> m (Vector Size i))
-> 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 (m :: Type -> Type).
(KnownNat p, Arithmetic a, MonadCircuit i a m) =>
Vector Size i -> Vector Size i -> m (Vector Size i)
mul @p) m (Vector Size i)
forall i a (m :: Type -> Type).
MonadCircuit i a 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
deriving newtype instance Symbolic c => Eq (Bool c) (FFA p c)
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