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

-- | Ed25519 with @UInt 256 (Zp p)@ as computational backend
--
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))

    -- | Addition casts point coordinates to @Zp Ed25519_Base@ and adds them as if they were points on @Ed25519 Void@
    --
    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)

    -- | Multiplication casts point coordinates to @Zp Ed25519_Base@ and scale factor to @Zp Ed25519_Scalar@,
    --   then scales the point as if it were a point on @Ed25519 Void@
    --
    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

    -- (0, 0) is never on a Twisted Edwards curve for any curve parameters.
    -- We can encode the point at infinity as (0, 0), therefore.
    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

-- | Ed25519 with @UInt 256 (ArithmeticCircuit a)@ as computational backend
--
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)

    -- pointMul uses natScale which converts the scale to Natural.
    -- We can't convert arithmetic circuits to Natural, so we can't use pointMul either.
    --
    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
        -- We will perform multiplications of UInts of up to n bits, therefore we need 2n bits to store the result.
        --
        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)

        -- Calculate the modular inverse using Extended Euclidean algorithm
        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)

        -- Calculate the modular inverse using Extended Euclidean algorithm
        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
        -- We will perform multiplications of UInts of up to n bits, therefore we need 2n bits to store the result.
        --
        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)

        -- Calculate the modular inverse using Extended Euclidean algorithm
        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)

        -- Calculate the modular inverse using Extended Euclidean algorithm
        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