{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -Wno-orphans #-}
module ZkFold.Symbolic.Data.Ed25519 where
import Data.List (splitAt)
import Data.Void (Void)
import GHC.TypeNats (Natural)
import Prelude (error, otherwise, ($), (.), (<>))
import qualified Prelude as P
import ZkFold.Base.Algebra.Basic.Class
import ZkFold.Base.Algebra.Basic.Field
import ZkFold.Base.Algebra.Basic.Number
import ZkFold.Base.Algebra.EllipticCurve.Class
import ZkFold.Base.Algebra.EllipticCurve.Ed25519
import ZkFold.Prelude (length)
import ZkFold.Symbolic.Compiler hiding (forceZero)
import ZkFold.Symbolic.Data.Bool
import ZkFold.Symbolic.Data.Combinators
import ZkFold.Symbolic.Data.Conditional
import ZkFold.Symbolic.Data.DiscreteField
import ZkFold.Symbolic.Data.Eq
import ZkFold.Symbolic.Data.UInt
zpToEd :: (Finite (Zp p)) => Point (Ed25519 (Zp p)) -> Point (Ed25519 Void)
zpToEd :: forall (p :: Natural).
Finite (Zp p) =>
Point (Ed25519 (Zp p)) -> Point (Ed25519 Void)
zpToEd Point (Ed25519 (Zp p))
Inf = Point (Ed25519 Void)
forall {k} (curve :: k). Point curve
Inf
zpToEd (Point BaseField (Ed25519 (Zp p))
x BaseField (Ed25519 (Zp p))
y) = BaseField (Ed25519 Void)
-> BaseField (Ed25519 Void) -> Point (Ed25519 Void)
forall {k} (curve :: k).
BaseField curve -> BaseField curve -> Point curve
Point (Integer -> BaseField (Ed25519 Void)
Integer -> Zp Ed25519_Base
forall (p :: Natural). KnownNat p => Integer -> Zp p
toZp (Integer -> BaseField (Ed25519 Void))
-> (BaseField (Ed25519 (Zp p)) -> Integer)
-> BaseField (Ed25519 (Zp p))
-> BaseField (Ed25519 Void)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BaseField (Ed25519 (Zp p)) -> Integer
UInt 256 (Zp p) -> Integer
forall a b. ToConstant a b => a -> b
toConstant (BaseField (Ed25519 (Zp p)) -> BaseField (Ed25519 Void))
-> BaseField (Ed25519 (Zp p)) -> BaseField (Ed25519 Void)
forall a b. (a -> b) -> a -> b
$ BaseField (Ed25519 (Zp p))
x) (Integer -> BaseField (Ed25519 Void)
Integer -> Zp Ed25519_Base
forall (p :: Natural). KnownNat p => Integer -> Zp p
toZp (Integer -> BaseField (Ed25519 Void))
-> (BaseField (Ed25519 (Zp p)) -> Integer)
-> BaseField (Ed25519 (Zp p))
-> BaseField (Ed25519 Void)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BaseField (Ed25519 (Zp p)) -> Integer
UInt 256 (Zp p) -> Integer
forall a b. ToConstant a b => a -> b
toConstant (BaseField (Ed25519 (Zp p)) -> BaseField (Ed25519 Void))
-> BaseField (Ed25519 (Zp p)) -> BaseField (Ed25519 Void)
forall a b. (a -> b) -> a -> b
$ BaseField (Ed25519 (Zp p))
y)
edToZp :: (Finite (Zp p)) => Point (Ed25519 Void) -> Point (Ed25519 (Zp p))
edToZp :: forall (p :: Natural).
Finite (Zp p) =>
Point (Ed25519 Void) -> Point (Ed25519 (Zp p))
edToZp Point (Ed25519 Void)
Inf = Point (Ed25519 (Zp p))
forall {k} (curve :: k). Point curve
Inf
edToZp (Point BaseField (Ed25519 Void)
x BaseField (Ed25519 Void)
y) = BaseField (Ed25519 (Zp p))
-> BaseField (Ed25519 (Zp p)) -> Point (Ed25519 (Zp p))
forall {k} (curve :: k).
BaseField curve -> BaseField curve -> Point curve
Point (Natural -> BaseField (Ed25519 (Zp p))
Natural -> UInt 256 (Zp p)
forall a b. FromConstant a b => a -> b
fromConstant (Natural -> BaseField (Ed25519 (Zp p)))
-> (BaseField (Ed25519 Void) -> Natural)
-> BaseField (Ed25519 Void)
-> BaseField (Ed25519 (Zp p))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BaseField (Ed25519 Void) -> Natural
Zp Ed25519_Base -> Natural
forall (p :: Natural). Zp p -> Natural
fromZp (BaseField (Ed25519 Void) -> BaseField (Ed25519 (Zp p)))
-> BaseField (Ed25519 Void) -> BaseField (Ed25519 (Zp p))
forall a b. (a -> b) -> a -> b
$ BaseField (Ed25519 Void)
x) (Natural -> BaseField (Ed25519 (Zp p))
Natural -> UInt 256 (Zp p)
forall a b. FromConstant a b => a -> b
fromConstant (Natural -> BaseField (Ed25519 (Zp p)))
-> (BaseField (Ed25519 Void) -> Natural)
-> BaseField (Ed25519 Void)
-> BaseField (Ed25519 (Zp p))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BaseField (Ed25519 Void) -> Natural
Zp Ed25519_Base -> Natural
forall (p :: Natural). Zp p -> Natural
fromZp (BaseField (Ed25519 Void) -> BaseField (Ed25519 (Zp p)))
-> BaseField (Ed25519 Void) -> BaseField (Ed25519 (Zp p))
forall a b. (a -> b) -> a -> b
$ BaseField (Ed25519 Void)
y)
instance (Finite (Zp p)) => EllipticCurve (Ed25519 (Zp p)) where
type BaseField (Ed25519 (Zp p)) = UInt 256 (Zp p)
type ScalarField (Ed25519 (Zp p)) = UInt 256 (Zp p)
inf :: Point (Ed25519 (Zp p))
inf = Point (Ed25519 (Zp p))
forall {k} (curve :: k). Point curve
Inf
gen :: Point (Ed25519 (Zp p))
gen = BaseField (Ed25519 (Zp p))
-> BaseField (Ed25519 (Zp p)) -> Point (Ed25519 (Zp p))
forall {k} (curve :: k).
BaseField curve -> BaseField curve -> Point curve
Point
(Natural -> UInt 256 (Zp p)
forall a b. FromConstant a b => a -> b
fromConstant (Natural
15112221349535400772501151409588531511454012693041857206046113283949847762202 :: Natural))
(Natural -> UInt 256 (Zp p)
forall a b. FromConstant a b => a -> b
fromConstant (Natural
46316835694926478169428394003475163141307993866256225615783033603165251855960 :: Natural))
add :: Point (Ed25519 (Zp p))
-> Point (Ed25519 (Zp p)) -> Point (Ed25519 (Zp p))
add Point (Ed25519 (Zp p))
p1 Point (Ed25519 (Zp p))
p2 = Point (Ed25519 Void) -> Point (Ed25519 (Zp p))
forall (p :: Natural).
Finite (Zp p) =>
Point (Ed25519 Void) -> Point (Ed25519 (Zp p))
edToZp (Point (Ed25519 Void) -> Point (Ed25519 (Zp p)))
-> Point (Ed25519 Void) -> Point (Ed25519 (Zp p))
forall a b. (a -> b) -> a -> b
$ Point (Ed25519 Void)
-> Point (Ed25519 Void) -> Point (Ed25519 Void)
forall {k} (curve :: k).
EllipticCurve curve =>
Point curve -> Point curve -> Point curve
add (Point (Ed25519 (Zp p)) -> Point (Ed25519 Void)
forall (p :: Natural).
Finite (Zp p) =>
Point (Ed25519 (Zp p)) -> Point (Ed25519 Void)
zpToEd Point (Ed25519 (Zp p))
p1) (Point (Ed25519 (Zp p)) -> Point (Ed25519 Void)
forall (p :: Natural).
Finite (Zp p) =>
Point (Ed25519 (Zp p)) -> Point (Ed25519 Void)
zpToEd Point (Ed25519 (Zp p))
p2)
mul :: ScalarField (Ed25519 (Zp p))
-> Point (Ed25519 (Zp p)) -> Point (Ed25519 (Zp p))
mul ScalarField (Ed25519 (Zp p))
s Point (Ed25519 (Zp p))
p = forall (p :: Natural).
Finite (Zp p) =>
Point (Ed25519 Void) -> Point (Ed25519 (Zp p))
edToZp @p (Point (Ed25519 Void) -> Point (Ed25519 (Zp p)))
-> Point (Ed25519 Void) -> Point (Ed25519 (Zp p))
forall a b. (a -> b) -> a -> b
$ ScalarField (Ed25519 Void)
-> Point (Ed25519 Void) -> Point (Ed25519 Void)
forall {k} (curve :: k).
EllipticCurve curve =>
ScalarField curve -> Point curve -> Point curve
mul (Integer -> ScalarField (Ed25519 Void)
Integer -> Zp Ed25519_Scalar
forall (p :: Natural). KnownNat p => Integer -> Zp p
toZp (Integer -> ScalarField (Ed25519 Void))
-> (ScalarField (Ed25519 (Zp p)) -> Integer)
-> ScalarField (Ed25519 (Zp p))
-> ScalarField (Ed25519 Void)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ScalarField (Ed25519 (Zp p)) -> Integer
UInt 256 (Zp p) -> Integer
forall a b. ToConstant a b => a -> b
toConstant (ScalarField (Ed25519 (Zp p)) -> ScalarField (Ed25519 Void))
-> ScalarField (Ed25519 (Zp p)) -> ScalarField (Ed25519 Void)
forall a b. (a -> b) -> a -> b
$ ScalarField (Ed25519 (Zp p))
s) (forall (p :: Natural).
Finite (Zp p) =>
Point (Ed25519 (Zp p)) -> Point (Ed25519 Void)
zpToEd @p Point (Ed25519 (Zp p))
p)
instance SymbolicData a (UInt 256 (ArithmeticCircuit a)) => SymbolicData a (Point (Ed25519 (ArithmeticCircuit a))) where
pieces :: Point (Ed25519 (ArithmeticCircuit a)) -> [ArithmeticCircuit a]
pieces Point (Ed25519 (ArithmeticCircuit a))
Inf = UInt 256 (ArithmeticCircuit a) -> [ArithmeticCircuit a]
forall a x. SymbolicData a x => x -> [ArithmeticCircuit a]
pieces (UInt 256 (ArithmeticCircuit a)
forall a. AdditiveMonoid a => a
zero :: UInt 256 (ArithmeticCircuit a)) [ArithmeticCircuit a]
-> [ArithmeticCircuit a] -> [ArithmeticCircuit a]
forall a. Semigroup a => a -> a -> a
<> UInt 256 (ArithmeticCircuit a) -> [ArithmeticCircuit a]
forall a x. SymbolicData a x => x -> [ArithmeticCircuit a]
pieces (UInt 256 (ArithmeticCircuit a)
forall a. AdditiveMonoid a => a
zero :: UInt 256 (ArithmeticCircuit a))
pieces (Point BaseField (Ed25519 (ArithmeticCircuit a))
x BaseField (Ed25519 (ArithmeticCircuit a))
y) = UInt 256 (ArithmeticCircuit a) -> [ArithmeticCircuit a]
forall a x. SymbolicData a x => x -> [ArithmeticCircuit a]
pieces BaseField (Ed25519 (ArithmeticCircuit a))
UInt 256 (ArithmeticCircuit a)
x [ArithmeticCircuit a]
-> [ArithmeticCircuit a] -> [ArithmeticCircuit a]
forall a. Semigroup a => a -> a -> a
<> UInt 256 (ArithmeticCircuit a) -> [ArithmeticCircuit a]
forall a x. SymbolicData a x => x -> [ArithmeticCircuit a]
pieces BaseField (Ed25519 (ArithmeticCircuit a))
UInt 256 (ArithmeticCircuit a)
y
restore :: [ArithmeticCircuit a] -> Point (Ed25519 (ArithmeticCircuit a))
restore [ArithmeticCircuit a]
lst
| [ArithmeticCircuit a] -> Natural
forall (t :: Type -> Type) a. Foldable t => t a -> Natural
length [ArithmeticCircuit a]
lst Natural -> Natural -> Bool
forall b a. Eq b a => a -> a -> b
/= (forall a x. SymbolicData a x => Natural
typeSize @a @(Point (Ed25519 (ArithmeticCircuit a)))) = [Char] -> Point (Ed25519 (ArithmeticCircuit a))
forall a. HasCallStack => [Char] -> a
error [Char]
"SymbolicData a (Point (Ed25519 (ArithmeticCircuit a))): wrong number of registers"
| Bool
otherwise =
forall b a. Conditional b a => a -> a -> b -> a
bool @(Bool (ArithmeticCircuit a)) @(Point (Ed25519 (ArithmeticCircuit a))) (BaseField (Ed25519 (ArithmeticCircuit a))
-> BaseField (Ed25519 (ArithmeticCircuit a))
-> Point (Ed25519 (ArithmeticCircuit a))
forall {k} (curve :: k).
BaseField curve -> BaseField curve -> Point curve
Point BaseField (Ed25519 (ArithmeticCircuit a))
UInt 256 (ArithmeticCircuit a)
x BaseField (Ed25519 (ArithmeticCircuit a))
UInt 256 (ArithmeticCircuit a)
y) Point (Ed25519 (ArithmeticCircuit a))
forall {k} (curve :: k). Point curve
Inf ((UInt 256 (ArithmeticCircuit a)
x UInt 256 (ArithmeticCircuit a)
-> UInt 256 (ArithmeticCircuit a) -> Bool (ArithmeticCircuit a)
forall b a. Eq b a => a -> a -> b
== UInt 256 (ArithmeticCircuit a)
forall a. AdditiveMonoid a => a
zero) Bool (ArithmeticCircuit a)
-> Bool (ArithmeticCircuit a) -> Bool (ArithmeticCircuit a)
forall b. BoolType b => b -> b -> b
&& (UInt 256 (ArithmeticCircuit a)
y UInt 256 (ArithmeticCircuit a)
-> UInt 256 (ArithmeticCircuit a) -> Bool (ArithmeticCircuit a)
forall b a. Eq b a => a -> a -> b
== UInt 256 (ArithmeticCircuit a)
forall a. AdditiveMonoid a => a
zero))
where
([ArithmeticCircuit a]
piecesX, [ArithmeticCircuit a]
piecesY) = Int
-> [ArithmeticCircuit a]
-> ([ArithmeticCircuit a], [ArithmeticCircuit a])
forall a. Int -> [a] -> ([a], [a])
splitAt (Natural -> Int
forall a b. (Integral a, Num b) => a -> b
P.fromIntegral ([ArithmeticCircuit a] -> Natural
forall (t :: Type -> Type) a. Foldable t => t a -> Natural
length [ArithmeticCircuit a]
lst) Int -> Int -> Int
forall a. Integral a => a -> a -> a
`P.div` Int
2) [ArithmeticCircuit a]
lst
(UInt 256 (ArithmeticCircuit a)
x, UInt 256 (ArithmeticCircuit a)
y) = ([ArithmeticCircuit a] -> UInt 256 (ArithmeticCircuit a)
forall a x. SymbolicData a x => [ArithmeticCircuit a] -> x
restore [ArithmeticCircuit a]
piecesX, [ArithmeticCircuit a] -> UInt 256 (ArithmeticCircuit a)
forall a x. SymbolicData a x => [ArithmeticCircuit a] -> x
restore [ArithmeticCircuit a]
piecesY)
typeSize :: Natural
typeSize = Natural
2 Natural -> Natural -> Natural
forall a. MultiplicativeSemigroup a => a -> a -> a
* forall a x. SymbolicData a x => Natural
typeSize @a @(UInt 256 (ArithmeticCircuit a))
instance (Ring a, Eq (Bool a) (BaseField (Ed25519 a))) => Eq (Bool a) (Point (Ed25519 a)) where
Point (Ed25519 a)
Inf == :: Point (Ed25519 a) -> Point (Ed25519 a) -> Bool a
== Point (Ed25519 a)
Inf = Bool a
forall b. BoolType b => b
true
Point (Ed25519 a)
Inf == Point (Ed25519 a)
_ = Bool a
forall b. BoolType b => b
false
Point (Ed25519 a)
_ == Point (Ed25519 a)
Inf = Bool a
forall b. BoolType b => b
false
(Point BaseField (Ed25519 a)
x1 BaseField (Ed25519 a)
y1) == (Point BaseField (Ed25519 a)
x2 BaseField (Ed25519 a)
y2) = BaseField (Ed25519 a)
x1 BaseField (Ed25519 a) -> BaseField (Ed25519 a) -> Bool a
forall b a. Eq b a => a -> a -> b
== BaseField (Ed25519 a)
x2 Bool a -> Bool a -> Bool a
forall b. BoolType b => b -> b -> b
&& BaseField (Ed25519 a)
y1 BaseField (Ed25519 a) -> BaseField (Ed25519 a) -> Bool a
forall b a. Eq b a => a -> a -> b
== BaseField (Ed25519 a)
y2
Point (Ed25519 a)
Inf /= :: Point (Ed25519 a) -> Point (Ed25519 a) -> Bool a
/= Point (Ed25519 a)
Inf = Bool a
forall b. BoolType b => b
false
Point (Ed25519 a)
Inf /= Point (Ed25519 a)
_ = Bool a
forall b. BoolType b => b
true
Point (Ed25519 a)
_ /= Point (Ed25519 a)
Inf = Bool a
forall b. BoolType b => b
true
(Point BaseField (Ed25519 a)
x1 BaseField (Ed25519 a)
y1) /= (Point BaseField (Ed25519 a)
x2 BaseField (Ed25519 a)
y2) = BaseField (Ed25519 a)
x1 BaseField (Ed25519 a) -> BaseField (Ed25519 a) -> Bool a
forall b a. Eq b a => a -> a -> b
/= BaseField (Ed25519 a)
x2 Bool a -> Bool a -> Bool a
forall b. BoolType b => b -> b -> b
|| BaseField (Ed25519 a)
y1 BaseField (Ed25519 a) -> BaseField (Ed25519 a) -> Bool a
forall b a. Eq b a => a -> a -> b
/= BaseField (Ed25519 a)
y2
instance
( Arithmetic a
, SymbolicData a (UInt 256 (ArithmeticCircuit a))
, FromConstant Natural (UInt 512 (ArithmeticCircuit a))
, EuclideanDomain (UInt 512 (ArithmeticCircuit a))
, BinaryExpansion (UInt 256 (ArithmeticCircuit a))
) => EllipticCurve (Ed25519 (ArithmeticCircuit a)) where
type BaseField (Ed25519 (ArithmeticCircuit a)) = UInt 256 (ArithmeticCircuit a)
type ScalarField (Ed25519 (ArithmeticCircuit a)) = UInt 256 (ArithmeticCircuit a)
inf :: Point (Ed25519 (ArithmeticCircuit a))
inf = Point (Ed25519 (ArithmeticCircuit a))
forall {k} (curve :: k). Point curve
Inf
gen :: Point (Ed25519 (ArithmeticCircuit a))
gen = BaseField (Ed25519 (ArithmeticCircuit a))
-> BaseField (Ed25519 (ArithmeticCircuit a))
-> Point (Ed25519 (ArithmeticCircuit a))
forall {k} (curve :: k).
BaseField curve -> BaseField curve -> Point curve
Point
(Natural -> UInt 256 (ArithmeticCircuit a)
forall a b. FromConstant a b => a -> b
fromConstant (Natural
15112221349535400772501151409588531511454012693041857206046113283949847762202 :: Natural))
(Natural -> UInt 256 (ArithmeticCircuit a)
forall a b. FromConstant a b => a -> b
fromConstant (Natural
46316835694926478169428394003475163141307993866256225615783033603165251855960 :: Natural))
add :: Point (Ed25519 (ArithmeticCircuit a))
-> Point (Ed25519 (ArithmeticCircuit a))
-> Point (Ed25519 (ArithmeticCircuit a))
add Point (Ed25519 (ArithmeticCircuit a))
x Point (Ed25519 (ArithmeticCircuit a))
y = forall b a. Conditional b a => a -> a -> b -> a
bool @(Bool (ArithmeticCircuit a)) @(Point (Ed25519 (ArithmeticCircuit a))) (Point (Ed25519 (ArithmeticCircuit a))
-> Point (Ed25519 (ArithmeticCircuit a))
-> Point (Ed25519 (ArithmeticCircuit a))
forall a.
(Arithmetic a, EuclideanDomain (UInt 512 (ArithmeticCircuit a))) =>
Point (Ed25519 (ArithmeticCircuit a))
-> Point (Ed25519 (ArithmeticCircuit a))
-> Point (Ed25519 (ArithmeticCircuit a))
acAdd25519 Point (Ed25519 (ArithmeticCircuit a))
x Point (Ed25519 (ArithmeticCircuit a))
y) (Point (Ed25519 (ArithmeticCircuit a))
-> Point (Ed25519 (ArithmeticCircuit a))
forall a.
(Arithmetic a, EuclideanDomain (UInt 512 (ArithmeticCircuit a))) =>
Point (Ed25519 (ArithmeticCircuit a))
-> Point (Ed25519 (ArithmeticCircuit a))
acDouble25519 Point (Ed25519 (ArithmeticCircuit a))
x) (Point (Ed25519 (ArithmeticCircuit a))
x Point (Ed25519 (ArithmeticCircuit a))
-> Point (Ed25519 (ArithmeticCircuit a))
-> Bool (ArithmeticCircuit a)
forall b a. Eq b a => a -> a -> b
== Point (Ed25519 (ArithmeticCircuit a))
y)
mul :: ScalarField (Ed25519 (ArithmeticCircuit a))
-> Point (Ed25519 (ArithmeticCircuit a))
-> Point (Ed25519 (ArithmeticCircuit a))
mul ScalarField (Ed25519 (ArithmeticCircuit a))
sc Point (Ed25519 (ArithmeticCircuit a))
x = [ArithmeticCircuit a]
-> Point (Ed25519 (ArithmeticCircuit a))
-> Point (Ed25519 (ArithmeticCircuit a))
bitsMul (UInt 256 (ArithmeticCircuit a) -> [ArithmeticCircuit a]
uintBits ScalarField (Ed25519 (ArithmeticCircuit a))
UInt 256 (ArithmeticCircuit a)
sc) Point (Ed25519 (ArithmeticCircuit a))
x
where
bitsMul :: [ArithmeticCircuit a] -> Point (Ed25519 (ArithmeticCircuit a)) -> Point (Ed25519 (ArithmeticCircuit a))
bitsMul :: [ArithmeticCircuit a]
-> Point (Ed25519 (ArithmeticCircuit a))
-> Point (Ed25519 (ArithmeticCircuit a))
bitsMul [ArithmeticCircuit a]
bits Point (Ed25519 (ArithmeticCircuit a))
pt = [Point (Ed25519 (ArithmeticCircuit a))]
-> Point (Ed25519 (ArithmeticCircuit a))
forall (t :: Type -> Type) a.
(Foldable t, AdditiveMonoid a) =>
t a -> a
sum ([Point (Ed25519 (ArithmeticCircuit a))]
-> Point (Ed25519 (ArithmeticCircuit a)))
-> [Point (Ed25519 (ArithmeticCircuit a))]
-> Point (Ed25519 (ArithmeticCircuit a))
forall a b. (a -> b) -> a -> b
$ (ArithmeticCircuit a
-> Point (Ed25519 (ArithmeticCircuit a))
-> Point (Ed25519 (ArithmeticCircuit a)))
-> [ArithmeticCircuit a]
-> [Point (Ed25519 (ArithmeticCircuit a))]
-> [Point (Ed25519 (ArithmeticCircuit a))]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
P.zipWith (\ArithmeticCircuit a
b Point (Ed25519 (ArithmeticCircuit a))
p -> forall b a. Conditional b a => a -> a -> b -> a
bool @(Bool (ArithmeticCircuit a)) Point (Ed25519 (ArithmeticCircuit a))
forall a. AdditiveMonoid a => a
zero Point (Ed25519 (ArithmeticCircuit a))
p (ArithmeticCircuit a -> Bool (ArithmeticCircuit a)
forall b a. DiscreteField b a => a -> b
isZero ArithmeticCircuit a
b)) [ArithmeticCircuit a]
bits ((Point (Ed25519 (ArithmeticCircuit a))
-> Point (Ed25519 (ArithmeticCircuit a)))
-> Point (Ed25519 (ArithmeticCircuit a))
-> [Point (Ed25519 (ArithmeticCircuit a))]
forall a. (a -> a) -> a -> [a]
P.iterate (\Point (Ed25519 (ArithmeticCircuit a))
e -> Point (Ed25519 (ArithmeticCircuit a))
e Point (Ed25519 (ArithmeticCircuit a))
-> Point (Ed25519 (ArithmeticCircuit a))
-> Point (Ed25519 (ArithmeticCircuit a))
forall a. AdditiveSemigroup a => a -> a -> a
+ Point (Ed25519 (ArithmeticCircuit a))
e) Point (Ed25519 (ArithmeticCircuit a))
pt)
uintBits :: UInt 256 (ArithmeticCircuit a) -> [ArithmeticCircuit a]
uintBits :: UInt 256 (ArithmeticCircuit a) -> [ArithmeticCircuit a]
uintBits (UInt [ArithmeticCircuit a]
lows ArithmeticCircuit a
hi) = (ArithmeticCircuit a -> [ArithmeticCircuit a])
-> [ArithmeticCircuit a] -> [ArithmeticCircuit a]
forall (t :: Type -> Type) a b.
Foldable t =>
(a -> [b]) -> t a -> [b]
P.concatMap ArithmeticCircuit a -> [ArithmeticCircuit a]
forall a. BinaryExpansion a => a -> [a]
binaryExpansion [ArithmeticCircuit a]
lows [ArithmeticCircuit a]
-> [ArithmeticCircuit a] -> [ArithmeticCircuit a]
forall a. Semigroup a => a -> a -> a
<> ArithmeticCircuit a -> [ArithmeticCircuit a]
forall a. BinaryExpansion a => a -> [a]
binaryExpansion ArithmeticCircuit a
hi
acAdd25519
:: forall a
. Arithmetic a
=> EuclideanDomain (UInt 512 (ArithmeticCircuit a))
=> Point (Ed25519 (ArithmeticCircuit a))
-> Point (Ed25519 (ArithmeticCircuit a))
-> Point (Ed25519 (ArithmeticCircuit a))
acAdd25519 :: forall a.
(Arithmetic a, EuclideanDomain (UInt 512 (ArithmeticCircuit a))) =>
Point (Ed25519 (ArithmeticCircuit a))
-> Point (Ed25519 (ArithmeticCircuit a))
-> Point (Ed25519 (ArithmeticCircuit a))
acAdd25519 Point (Ed25519 (ArithmeticCircuit a))
Inf Point (Ed25519 (ArithmeticCircuit a))
q = Point (Ed25519 (ArithmeticCircuit a))
q
acAdd25519 Point (Ed25519 (ArithmeticCircuit a))
p Point (Ed25519 (ArithmeticCircuit a))
Inf = Point (Ed25519 (ArithmeticCircuit a))
p
acAdd25519 (Point BaseField (Ed25519 (ArithmeticCircuit a))
x1 BaseField (Ed25519 (ArithmeticCircuit a))
y1) (Point BaseField (Ed25519 (ArithmeticCircuit a))
x2 BaseField (Ed25519 (ArithmeticCircuit a))
y2) = BaseField (Ed25519 (ArithmeticCircuit a))
-> BaseField (Ed25519 (ArithmeticCircuit a))
-> Point (Ed25519 (ArithmeticCircuit a))
forall {k} (curve :: k).
BaseField curve -> BaseField curve -> Point curve
Point (UInt 512 (ArithmeticCircuit a) -> UInt 256 (ArithmeticCircuit a)
forall a b. Shrink a b => a -> b
shrink UInt 512 (ArithmeticCircuit a)
x3) (UInt 512 (ArithmeticCircuit a) -> UInt 256 (ArithmeticCircuit a)
forall a b. Shrink a b => a -> b
shrink UInt 512 (ArithmeticCircuit a)
y3)
where
x1e, y1e, x2e, y2e :: UInt 512 (ArithmeticCircuit a)
x1e :: UInt 512 (ArithmeticCircuit a)
x1e = UInt 256 (ArithmeticCircuit a) -> UInt 512 (ArithmeticCircuit a)
forall a b. Extend a b => a -> b
extend BaseField (Ed25519 (ArithmeticCircuit a))
UInt 256 (ArithmeticCircuit a)
x1
y1e :: UInt 512 (ArithmeticCircuit a)
y1e = UInt 256 (ArithmeticCircuit a) -> UInt 512 (ArithmeticCircuit a)
forall a b. Extend a b => a -> b
extend BaseField (Ed25519 (ArithmeticCircuit a))
UInt 256 (ArithmeticCircuit a)
y1
x2e :: UInt 512 (ArithmeticCircuit a)
x2e = UInt 256 (ArithmeticCircuit a) -> UInt 512 (ArithmeticCircuit a)
forall a b. Extend a b => a -> b
extend BaseField (Ed25519 (ArithmeticCircuit a))
UInt 256 (ArithmeticCircuit a)
x2
y2e :: UInt 512 (ArithmeticCircuit a)
y2e = UInt 256 (ArithmeticCircuit a) -> UInt 512 (ArithmeticCircuit a)
forall a b. Extend a b => a -> b
extend BaseField (Ed25519 (ArithmeticCircuit a))
UInt 256 (ArithmeticCircuit a)
y2
m :: UInt 512 (ArithmeticCircuit a)
m :: UInt 512 (ArithmeticCircuit a)
m = Natural -> UInt 512 (ArithmeticCircuit a)
forall a b. FromConstant a b => a -> b
fromConstant (Natural -> UInt 512 (ArithmeticCircuit a))
-> Natural -> UInt 512 (ArithmeticCircuit a)
forall a b. (a -> b) -> a -> b
$ forall (n :: Natural). KnownNat n => Natural
value @Ed25519_Base
plusM :: UInt 512 (ArithmeticCircuit a) -> UInt 512 (ArithmeticCircuit a) -> UInt 512 (ArithmeticCircuit a)
plusM :: UInt 512 (ArithmeticCircuit a)
-> UInt 512 (ArithmeticCircuit a) -> UInt 512 (ArithmeticCircuit a)
plusM UInt 512 (ArithmeticCircuit a)
x UInt 512 (ArithmeticCircuit a)
y = (UInt 512 (ArithmeticCircuit a)
x UInt 512 (ArithmeticCircuit a)
-> UInt 512 (ArithmeticCircuit a) -> UInt 512 (ArithmeticCircuit a)
forall a. AdditiveSemigroup a => a -> a -> a
+ UInt 512 (ArithmeticCircuit a)
y) UInt 512 (ArithmeticCircuit a)
-> UInt 512 (ArithmeticCircuit a) -> UInt 512 (ArithmeticCircuit a)
forall a. EuclideanDomain a => a -> a -> a
`mod` UInt 512 (ArithmeticCircuit a)
m
mulM :: UInt 512 (ArithmeticCircuit a) -> UInt 512 (ArithmeticCircuit a) -> UInt 512 (ArithmeticCircuit a)
mulM :: UInt 512 (ArithmeticCircuit a)
-> UInt 512 (ArithmeticCircuit a) -> UInt 512 (ArithmeticCircuit a)
mulM UInt 512 (ArithmeticCircuit a)
x UInt 512 (ArithmeticCircuit a)
y = (UInt 512 (ArithmeticCircuit a)
x UInt 512 (ArithmeticCircuit a)
-> UInt 512 (ArithmeticCircuit a) -> UInt 512 (ArithmeticCircuit a)
forall a. MultiplicativeSemigroup a => a -> a -> a
* UInt 512 (ArithmeticCircuit a)
y) UInt 512 (ArithmeticCircuit a)
-> UInt 512 (ArithmeticCircuit a) -> UInt 512 (ArithmeticCircuit a)
forall a. EuclideanDomain a => a -> a -> a
`mod` UInt 512 (ArithmeticCircuit a)
m
d :: UInt 512 (ArithmeticCircuit a)
d :: UInt 512 (ArithmeticCircuit a)
d = Natural -> UInt 512 (ArithmeticCircuit a)
forall a b. FromConstant a b => a -> b
fromConstant (Natural -> UInt 512 (ArithmeticCircuit a))
-> Natural -> UInt 512 (ArithmeticCircuit a)
forall a b. (a -> b) -> a -> b
$ forall (p :: Natural). Zp p -> Natural
fromZp @Ed25519_Base (Zp Ed25519_Base -> Natural) -> Zp Ed25519_Base -> Natural
forall a b. (a -> b) -> a -> b
$ (Integer -> Zp Ed25519_Base
forall (p :: Natural). KnownNat p => Integer -> Zp p
toZp (-Integer
121665) Zp Ed25519_Base -> Zp Ed25519_Base -> Zp Ed25519_Base
forall a. Field a => a -> a -> a
// (Integer -> Zp Ed25519_Base
forall (p :: Natural). KnownNat p => Integer -> Zp p
toZp Integer
121666))
x3n :: UInt 512 (ArithmeticCircuit a)
x3n :: UInt 512 (ArithmeticCircuit a)
x3n = (UInt 512 (ArithmeticCircuit a)
x1e UInt 512 (ArithmeticCircuit a)
-> UInt 512 (ArithmeticCircuit a) -> UInt 512 (ArithmeticCircuit a)
`mulM` UInt 512 (ArithmeticCircuit a)
y2e) UInt 512 (ArithmeticCircuit a)
-> UInt 512 (ArithmeticCircuit a) -> UInt 512 (ArithmeticCircuit a)
`plusM` (UInt 512 (ArithmeticCircuit a)
y1e UInt 512 (ArithmeticCircuit a)
-> UInt 512 (ArithmeticCircuit a) -> UInt 512 (ArithmeticCircuit a)
`mulM` UInt 512 (ArithmeticCircuit a)
x2e)
x3d :: UInt 512 (ArithmeticCircuit a)
x3d :: UInt 512 (ArithmeticCircuit a)
x3d = UInt 512 (ArithmeticCircuit a)
forall a. MultiplicativeMonoid a => a
one UInt 512 (ArithmeticCircuit a)
-> UInt 512 (ArithmeticCircuit a) -> UInt 512 (ArithmeticCircuit a)
`plusM` (UInt 512 (ArithmeticCircuit a)
d UInt 512 (ArithmeticCircuit a)
-> UInt 512 (ArithmeticCircuit a) -> UInt 512 (ArithmeticCircuit a)
`mulM` UInt 512 (ArithmeticCircuit a)
x1e UInt 512 (ArithmeticCircuit a)
-> UInt 512 (ArithmeticCircuit a) -> UInt 512 (ArithmeticCircuit a)
`mulM` UInt 512 (ArithmeticCircuit a)
x2e UInt 512 (ArithmeticCircuit a)
-> UInt 512 (ArithmeticCircuit a) -> UInt 512 (ArithmeticCircuit a)
`mulM` UInt 512 (ArithmeticCircuit a)
y1e UInt 512 (ArithmeticCircuit a)
-> UInt 512 (ArithmeticCircuit a) -> UInt 512 (ArithmeticCircuit a)
`mulM` UInt 512 (ArithmeticCircuit a)
y2e)
x3di :: UInt 512 (ArithmeticCircuit a)
(UInt 512 (ArithmeticCircuit a)
x3di, UInt 512 (ArithmeticCircuit a)
_, UInt 512 (ArithmeticCircuit a)
_) = UInt 512 (ArithmeticCircuit a)
-> UInt 512 (ArithmeticCircuit a)
-> (UInt 512 (ArithmeticCircuit a), UInt 512 (ArithmeticCircuit a),
UInt 512 (ArithmeticCircuit a))
forall (n :: Natural) a.
(EuclideanDomain (UInt n a), KnownNat n, AdditiveGroup (UInt n a),
Eq (Bool a) (UInt n a),
Conditional (Bool a) (UInt n a, UInt n a, UInt n a)) =>
UInt n a -> UInt n a -> (UInt n a, UInt n a, UInt n a)
eea UInt 512 (ArithmeticCircuit a)
x3d UInt 512 (ArithmeticCircuit a)
m
x3 :: UInt 512 (ArithmeticCircuit a)
x3 :: UInt 512 (ArithmeticCircuit a)
x3 = UInt 512 (ArithmeticCircuit a)
x3n UInt 512 (ArithmeticCircuit a)
-> UInt 512 (ArithmeticCircuit a) -> UInt 512 (ArithmeticCircuit a)
`mulM` UInt 512 (ArithmeticCircuit a)
x3di
y3n :: UInt 512 (ArithmeticCircuit a)
y3n :: UInt 512 (ArithmeticCircuit a)
y3n = (UInt 512 (ArithmeticCircuit a)
y1e UInt 512 (ArithmeticCircuit a)
-> UInt 512 (ArithmeticCircuit a) -> UInt 512 (ArithmeticCircuit a)
`mulM` UInt 512 (ArithmeticCircuit a)
y2e) UInt 512 (ArithmeticCircuit a)
-> UInt 512 (ArithmeticCircuit a) -> UInt 512 (ArithmeticCircuit a)
`plusM` (UInt 512 (ArithmeticCircuit a)
x1e UInt 512 (ArithmeticCircuit a)
-> UInt 512 (ArithmeticCircuit a) -> UInt 512 (ArithmeticCircuit a)
`mulM` UInt 512 (ArithmeticCircuit a)
x2e)
y3d :: UInt 512 (ArithmeticCircuit a)
y3d :: UInt 512 (ArithmeticCircuit a)
y3d = UInt 512 (ArithmeticCircuit a)
forall a. MultiplicativeMonoid a => a
one UInt 512 (ArithmeticCircuit a)
-> UInt 512 (ArithmeticCircuit a) -> UInt 512 (ArithmeticCircuit a)
`plusM` ((UInt 512 (ArithmeticCircuit a)
m UInt 512 (ArithmeticCircuit a)
-> UInt 512 (ArithmeticCircuit a) -> UInt 512 (ArithmeticCircuit a)
forall a. AdditiveGroup a => a -> a -> a
- UInt 512 (ArithmeticCircuit a)
d) UInt 512 (ArithmeticCircuit a)
-> UInt 512 (ArithmeticCircuit a) -> UInt 512 (ArithmeticCircuit a)
`mulM` UInt 512 (ArithmeticCircuit a)
x1e UInt 512 (ArithmeticCircuit a)
-> UInt 512 (ArithmeticCircuit a) -> UInt 512 (ArithmeticCircuit a)
`mulM` UInt 512 (ArithmeticCircuit a)
x2e UInt 512 (ArithmeticCircuit a)
-> UInt 512 (ArithmeticCircuit a) -> UInt 512 (ArithmeticCircuit a)
`mulM` UInt 512 (ArithmeticCircuit a)
y1e UInt 512 (ArithmeticCircuit a)
-> UInt 512 (ArithmeticCircuit a) -> UInt 512 (ArithmeticCircuit a)
`mulM` UInt 512 (ArithmeticCircuit a)
y2e)
y3di :: UInt 512 (ArithmeticCircuit a)
(UInt 512 (ArithmeticCircuit a)
y3di, UInt 512 (ArithmeticCircuit a)
_, UInt 512 (ArithmeticCircuit a)
_) = UInt 512 (ArithmeticCircuit a)
-> UInt 512 (ArithmeticCircuit a)
-> (UInt 512 (ArithmeticCircuit a), UInt 512 (ArithmeticCircuit a),
UInt 512 (ArithmeticCircuit a))
forall (n :: Natural) a.
(EuclideanDomain (UInt n a), KnownNat n, AdditiveGroup (UInt n a),
Eq (Bool a) (UInt n a),
Conditional (Bool a) (UInt n a, UInt n a, UInt n a)) =>
UInt n a -> UInt n a -> (UInt n a, UInt n a, UInt n a)
eea UInt 512 (ArithmeticCircuit a)
y3d UInt 512 (ArithmeticCircuit a)
m
y3 :: UInt 512 (ArithmeticCircuit a)
y3 :: UInt 512 (ArithmeticCircuit a)
y3 = UInt 512 (ArithmeticCircuit a)
y3n UInt 512 (ArithmeticCircuit a)
-> UInt 512 (ArithmeticCircuit a) -> UInt 512 (ArithmeticCircuit a)
`mulM` UInt 512 (ArithmeticCircuit a)
y3di
acDouble25519
:: forall a
. Arithmetic a
=> EuclideanDomain (UInt 512 (ArithmeticCircuit a))
=> Point (Ed25519 (ArithmeticCircuit a))
-> Point (Ed25519 (ArithmeticCircuit a))
acDouble25519 :: forall a.
(Arithmetic a, EuclideanDomain (UInt 512 (ArithmeticCircuit a))) =>
Point (Ed25519 (ArithmeticCircuit a))
-> Point (Ed25519 (ArithmeticCircuit a))
acDouble25519 Point (Ed25519 (ArithmeticCircuit a))
Inf = Point (Ed25519 (ArithmeticCircuit a))
forall {k} (curve :: k). Point curve
Inf
acDouble25519 (Point BaseField (Ed25519 (ArithmeticCircuit a))
x1 BaseField (Ed25519 (ArithmeticCircuit a))
y1) = BaseField (Ed25519 (ArithmeticCircuit a))
-> BaseField (Ed25519 (ArithmeticCircuit a))
-> Point (Ed25519 (ArithmeticCircuit a))
forall {k} (curve :: k).
BaseField curve -> BaseField curve -> Point curve
Point (UInt 512 (ArithmeticCircuit a) -> UInt 256 (ArithmeticCircuit a)
forall a b. Shrink a b => a -> b
shrink UInt 512 (ArithmeticCircuit a)
x3) (UInt 512 (ArithmeticCircuit a) -> UInt 256 (ArithmeticCircuit a)
forall a b. Shrink a b => a -> b
shrink UInt 512 (ArithmeticCircuit a)
y3)
where
xe, ye :: UInt 512 (ArithmeticCircuit a)
xe :: UInt 512 (ArithmeticCircuit a)
xe = UInt 256 (ArithmeticCircuit a) -> UInt 512 (ArithmeticCircuit a)
forall a b. Extend a b => a -> b
extend BaseField (Ed25519 (ArithmeticCircuit a))
UInt 256 (ArithmeticCircuit a)
x1
ye :: UInt 512 (ArithmeticCircuit a)
ye = UInt 256 (ArithmeticCircuit a) -> UInt 512 (ArithmeticCircuit a)
forall a b. Extend a b => a -> b
extend BaseField (Ed25519 (ArithmeticCircuit a))
UInt 256 (ArithmeticCircuit a)
y1
m :: UInt 512 (ArithmeticCircuit a)
m :: UInt 512 (ArithmeticCircuit a)
m = Natural -> UInt 512 (ArithmeticCircuit a)
forall a b. FromConstant a b => a -> b
fromConstant (Natural -> UInt 512 (ArithmeticCircuit a))
-> Natural -> UInt 512 (ArithmeticCircuit a)
forall a b. (a -> b) -> a -> b
$ forall (n :: Natural). KnownNat n => Natural
value @Ed25519_Base
plusM :: UInt 512 (ArithmeticCircuit a) -> UInt 512 (ArithmeticCircuit a) -> UInt 512 (ArithmeticCircuit a)
plusM :: UInt 512 (ArithmeticCircuit a)
-> UInt 512 (ArithmeticCircuit a) -> UInt 512 (ArithmeticCircuit a)
plusM UInt 512 (ArithmeticCircuit a)
x UInt 512 (ArithmeticCircuit a)
y = (UInt 512 (ArithmeticCircuit a)
x UInt 512 (ArithmeticCircuit a)
-> UInt 512 (ArithmeticCircuit a) -> UInt 512 (ArithmeticCircuit a)
forall a. AdditiveSemigroup a => a -> a -> a
+ UInt 512 (ArithmeticCircuit a)
y) UInt 512 (ArithmeticCircuit a)
-> UInt 512 (ArithmeticCircuit a) -> UInt 512 (ArithmeticCircuit a)
forall a. EuclideanDomain a => a -> a -> a
`mod` UInt 512 (ArithmeticCircuit a)
m
mulM :: UInt 512 (ArithmeticCircuit a) -> UInt 512 (ArithmeticCircuit a) -> UInt 512 (ArithmeticCircuit a)
mulM :: UInt 512 (ArithmeticCircuit a)
-> UInt 512 (ArithmeticCircuit a) -> UInt 512 (ArithmeticCircuit a)
mulM UInt 512 (ArithmeticCircuit a)
x UInt 512 (ArithmeticCircuit a)
y = (UInt 512 (ArithmeticCircuit a)
x UInt 512 (ArithmeticCircuit a)
-> UInt 512 (ArithmeticCircuit a) -> UInt 512 (ArithmeticCircuit a)
forall a. MultiplicativeSemigroup a => a -> a -> a
* UInt 512 (ArithmeticCircuit a)
y) UInt 512 (ArithmeticCircuit a)
-> UInt 512 (ArithmeticCircuit a) -> UInt 512 (ArithmeticCircuit a)
forall a. EuclideanDomain a => a -> a -> a
`mod` UInt 512 (ArithmeticCircuit a)
m
x3n :: UInt 512 (ArithmeticCircuit a)
x3n :: UInt 512 (ArithmeticCircuit a)
x3n = (UInt 512 (ArithmeticCircuit a)
xe UInt 512 (ArithmeticCircuit a)
-> UInt 512 (ArithmeticCircuit a) -> UInt 512 (ArithmeticCircuit a)
`mulM` UInt 512 (ArithmeticCircuit a)
ye) UInt 512 (ArithmeticCircuit a)
-> UInt 512 (ArithmeticCircuit a) -> UInt 512 (ArithmeticCircuit a)
`plusM` (UInt 512 (ArithmeticCircuit a)
xe UInt 512 (ArithmeticCircuit a)
-> UInt 512 (ArithmeticCircuit a) -> UInt 512 (ArithmeticCircuit a)
`mulM` UInt 512 (ArithmeticCircuit a)
ye)
x3d :: UInt 512 (ArithmeticCircuit a)
x3d :: UInt 512 (ArithmeticCircuit a)
x3d = ((UInt 512 (ArithmeticCircuit a)
m UInt 512 (ArithmeticCircuit a)
-> UInt 512 (ArithmeticCircuit a) -> UInt 512 (ArithmeticCircuit a)
forall a. AdditiveGroup a => a -> a -> a
- UInt 512 (ArithmeticCircuit a)
forall a. MultiplicativeMonoid a => a
one) UInt 512 (ArithmeticCircuit a)
-> UInt 512 (ArithmeticCircuit a) -> UInt 512 (ArithmeticCircuit a)
`mulM` UInt 512 (ArithmeticCircuit a)
xe UInt 512 (ArithmeticCircuit a)
-> UInt 512 (ArithmeticCircuit a) -> UInt 512 (ArithmeticCircuit a)
`mulM` UInt 512 (ArithmeticCircuit a)
xe) UInt 512 (ArithmeticCircuit a)
-> UInt 512 (ArithmeticCircuit a) -> UInt 512 (ArithmeticCircuit a)
`plusM` (UInt 512 (ArithmeticCircuit a)
ye UInt 512 (ArithmeticCircuit a)
-> UInt 512 (ArithmeticCircuit a) -> UInt 512 (ArithmeticCircuit a)
`mulM` UInt 512 (ArithmeticCircuit a)
ye)
x3di :: UInt 512 (ArithmeticCircuit a)
(UInt 512 (ArithmeticCircuit a)
x3di, UInt 512 (ArithmeticCircuit a)
_, UInt 512 (ArithmeticCircuit a)
_) = UInt 512 (ArithmeticCircuit a)
-> UInt 512 (ArithmeticCircuit a)
-> (UInt 512 (ArithmeticCircuit a), UInt 512 (ArithmeticCircuit a),
UInt 512 (ArithmeticCircuit a))
forall (n :: Natural) a.
(EuclideanDomain (UInt n a), KnownNat n, AdditiveGroup (UInt n a),
Eq (Bool a) (UInt n a),
Conditional (Bool a) (UInt n a, UInt n a, UInt n a)) =>
UInt n a -> UInt n a -> (UInt n a, UInt n a, UInt n a)
eea UInt 512 (ArithmeticCircuit a)
x3d UInt 512 (ArithmeticCircuit a)
m
x3 :: UInt 512 (ArithmeticCircuit a)
x3 :: UInt 512 (ArithmeticCircuit a)
x3 = UInt 512 (ArithmeticCircuit a)
x3n UInt 512 (ArithmeticCircuit a)
-> UInt 512 (ArithmeticCircuit a) -> UInt 512 (ArithmeticCircuit a)
`mulM` UInt 512 (ArithmeticCircuit a)
x3di
y3n :: UInt 512 (ArithmeticCircuit a)
y3n :: UInt 512 (ArithmeticCircuit a)
y3n = (UInt 512 (ArithmeticCircuit a)
ye UInt 512 (ArithmeticCircuit a)
-> UInt 512 (ArithmeticCircuit a) -> UInt 512 (ArithmeticCircuit a)
`mulM` UInt 512 (ArithmeticCircuit a)
ye) UInt 512 (ArithmeticCircuit a)
-> UInt 512 (ArithmeticCircuit a) -> UInt 512 (ArithmeticCircuit a)
`plusM` (UInt 512 (ArithmeticCircuit a)
xe UInt 512 (ArithmeticCircuit a)
-> UInt 512 (ArithmeticCircuit a) -> UInt 512 (ArithmeticCircuit a)
`mulM` UInt 512 (ArithmeticCircuit a)
xe)
y3d :: UInt 512 (ArithmeticCircuit a)
y3d :: UInt 512 (ArithmeticCircuit a)
y3d = (UInt 512 (ArithmeticCircuit a)
forall a. MultiplicativeMonoid a => a
one UInt 512 (ArithmeticCircuit a)
-> UInt 512 (ArithmeticCircuit a) -> UInt 512 (ArithmeticCircuit a)
forall a. AdditiveSemigroup a => a -> a -> a
+ UInt 512 (ArithmeticCircuit a)
forall a. MultiplicativeMonoid a => a
one) UInt 512 (ArithmeticCircuit a)
-> UInt 512 (ArithmeticCircuit a) -> UInt 512 (ArithmeticCircuit a)
`plusM` (UInt 512 (ArithmeticCircuit a)
xe UInt 512 (ArithmeticCircuit a)
-> UInt 512 (ArithmeticCircuit a) -> UInt 512 (ArithmeticCircuit a)
`mulM` UInt 512 (ArithmeticCircuit a)
xe) UInt 512 (ArithmeticCircuit a)
-> UInt 512 (ArithmeticCircuit a) -> UInt 512 (ArithmeticCircuit a)
`plusM` ((UInt 512 (ArithmeticCircuit a)
m UInt 512 (ArithmeticCircuit a)
-> UInt 512 (ArithmeticCircuit a) -> UInt 512 (ArithmeticCircuit a)
forall a. AdditiveGroup a => a -> a -> a
- UInt 512 (ArithmeticCircuit a)
forall a. MultiplicativeMonoid a => a
one) UInt 512 (ArithmeticCircuit a)
-> UInt 512 (ArithmeticCircuit a) -> UInt 512 (ArithmeticCircuit a)
`mulM` UInt 512 (ArithmeticCircuit a)
ye UInt 512 (ArithmeticCircuit a)
-> UInt 512 (ArithmeticCircuit a) -> UInt 512 (ArithmeticCircuit a)
`mulM` UInt 512 (ArithmeticCircuit a)
ye)
y3di :: UInt 512 (ArithmeticCircuit a)
(UInt 512 (ArithmeticCircuit a)
y3di, UInt 512 (ArithmeticCircuit a)
_, UInt 512 (ArithmeticCircuit a)
_) = UInt 512 (ArithmeticCircuit a)
-> UInt 512 (ArithmeticCircuit a)
-> (UInt 512 (ArithmeticCircuit a), UInt 512 (ArithmeticCircuit a),
UInt 512 (ArithmeticCircuit a))
forall (n :: Natural) a.
(EuclideanDomain (UInt n a), KnownNat n, AdditiveGroup (UInt n a),
Eq (Bool a) (UInt n a),
Conditional (Bool a) (UInt n a, UInt n a, UInt n a)) =>
UInt n a -> UInt n a -> (UInt n a, UInt n a, UInt n a)
eea UInt 512 (ArithmeticCircuit a)
y3d UInt 512 (ArithmeticCircuit a)
m
y3 :: UInt 512 (ArithmeticCircuit a)
y3 :: UInt 512 (ArithmeticCircuit a)
y3 = UInt 512 (ArithmeticCircuit a)
y3n UInt 512 (ArithmeticCircuit a)
-> UInt 512 (ArithmeticCircuit a) -> UInt 512 (ArithmeticCircuit a)
`mulM` UInt 512 (ArithmeticCircuit a)
y3di