{-# LANGUAGE AllowAmbiguousTypes  #-}
{-# LANGUAGE DeriveAnyClass       #-}
{-# LANGUAGE DerivingStrategies   #-}
{-# LANGUAGE DerivingVia          #-}
{-# LANGUAGE TypeApplications     #-}
{-# LANGUAGE TypeOperators        #-}
{-# LANGUAGE UndecidableInstances #-}

module ZkFold.Symbolic.Data.UInt (
    StrictConv(..),
    StrictNum(..),
    UInt(..),
    toConstant,
    eea
) where

import           Control.Applicative                                       ((<*>))
import           Control.DeepSeq
import           Control.Monad.State                                       (StateT (..))
import           Data.Foldable                                             (foldr, foldrM, for_)
import           Data.Functor                                              ((<$>))
import           Data.List                                                 (map, unfoldr, zip, zipWith)
import           Data.Map                                                  (fromList, (!))
import           Data.Traversable                                          (for, traverse)
import           Data.Tuple                                                (swap)
import           GHC.Generics                                              (Generic)
import           GHC.Natural                                               (naturalFromInteger)
import           GHC.TypeNats                                              (Natural)
import           Prelude                                                   (Integer, concatMap, error, flip, foldl,
                                                                            otherwise, return, ($), (++), (.), (<>),
                                                                            (>>=))
import qualified Prelude                                                   as Haskell
import           Test.QuickCheck                                           (Arbitrary (..), chooseInteger)

import           ZkFold.Base.Algebra.Basic.Class
import           ZkFold.Base.Algebra.Basic.Field                           (Zp, fromZp, toZp)
import           ZkFold.Base.Algebra.Basic.Number
import           ZkFold.Prelude                                            (drop, length, replicate, replicateA,
                                                                            splitAt, take, (!!))
import           ZkFold.Symbolic.Compiler                                  hiding (forceZero)
import           ZkFold.Symbolic.Compiler.ArithmeticCircuit.Combinators    (expansion, splitExpansion)
import           ZkFold.Symbolic.Compiler.ArithmeticCircuit.MonadBlueprint
import           ZkFold.Symbolic.Data.Bool
import           ZkFold.Symbolic.Data.Combinators
import           ZkFold.Symbolic.Data.Conditional
import           ZkFold.Symbolic.Data.Eq
import           ZkFold.Symbolic.Data.Eq.Structural
import           ZkFold.Symbolic.Data.Ord

-- TODO (Issue #18): hide this constructor
data UInt (n :: Natural) a = UInt ![a] !a
    deriving (Int -> UInt n a -> ShowS
[UInt n a] -> ShowS
UInt n a -> String
(Int -> UInt n a -> ShowS)
-> (UInt n a -> String) -> ([UInt n a] -> ShowS) -> Show (UInt n a)
forall (n :: Natural) a. Show a => Int -> UInt n a -> ShowS
forall (n :: Natural) a. Show a => [UInt n a] -> ShowS
forall (n :: Natural) a. Show a => UInt n a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall (n :: Natural) a. Show a => Int -> UInt n a -> ShowS
showsPrec :: Int -> UInt n a -> ShowS
$cshow :: forall (n :: Natural) a. Show a => UInt n a -> String
show :: UInt n a -> String
$cshowList :: forall (n :: Natural) a. Show a => [UInt n a] -> ShowS
showList :: [UInt n a] -> ShowS
Haskell.Show, UInt n a -> UInt n a -> Bool
(UInt n a -> UInt n a -> Bool)
-> (UInt n a -> UInt n a -> Bool) -> Eq (UInt n a)
forall (n :: Natural) a. Eq a => UInt n a -> UInt n a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall (n :: Natural) a. Eq a => UInt n a -> UInt n a -> Bool
== :: UInt n a -> UInt n a -> Bool
$c/= :: forall (n :: Natural) a. Eq a => UInt n a -> UInt n a -> Bool
/= :: UInt n a -> UInt n a -> Bool
Haskell.Eq, (forall x. UInt n a -> Rep (UInt n a) x)
-> (forall x. Rep (UInt n a) x -> UInt n a) -> Generic (UInt n a)
forall (n :: Natural) a x. Rep (UInt n a) x -> UInt n a
forall (n :: Natural) a x. UInt n a -> Rep (UInt n a) x
forall x. Rep (UInt n a) x -> UInt n a
forall x. UInt n a -> Rep (UInt n a) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall (n :: Natural) a x. UInt n a -> Rep (UInt n a) x
from :: forall x. UInt n a -> Rep (UInt n a) x
$cto :: forall (n :: Natural) a x. Rep (UInt n a) x -> UInt n a
to :: forall x. Rep (UInt n a) x -> UInt n a
Generic, UInt n a -> ()
(UInt n a -> ()) -> NFData (UInt n a)
forall (n :: Natural) a. NFData a => UInt n a -> ()
forall a. (a -> ()) -> NFData a
$crnf :: forall (n :: Natural) a. NFData a => UInt n a -> ()
rnf :: UInt n a -> ()
NFData)

instance (FromConstant Natural a, Finite a, AdditiveMonoid a, KnownNat n) => FromConstant Natural (UInt n a) where
    fromConstant :: Natural -> UInt n a
fromConstant = (UInt n a, [a]) -> UInt n a
forall a b. (a, b) -> a
Haskell.fst ((UInt n a, [a]) -> UInt n a)
-> (Natural -> (UInt n a, [a])) -> Natural -> UInt n a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a (n :: Natural).
(FromConstant Natural a, Finite a, AdditiveMonoid a, KnownNat n) =>
Natural -> (UInt n a, [a])
cast @a @n (Natural -> (UInt n a, [a]))
-> (Natural -> Natural) -> Natural -> (UInt n a, [a])
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Natural -> Natural -> Natural
forall a. Integral a => a -> a -> a
`Haskell.mod` (Natural
2 Natural -> Natural -> Natural
forall a b. Exponent a b => a -> b -> a
^ forall (n :: Natural). KnownNat n => Natural
getNatural @n))

instance (FromConstant Natural a, Finite a, AdditiveMonoid a, KnownNat n) => FromConstant Integer (UInt n a) where
    fromConstant :: Integer -> UInt n a
fromConstant = Natural -> UInt n a
forall a b. FromConstant a b => a -> b
fromConstant (Natural -> UInt n a)
-> (Integer -> Natural) -> Integer -> UInt n a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> Natural
naturalFromInteger (Integer -> Natural) -> (Integer -> Integer) -> Integer -> Natural
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`Haskell.mod` (Integer
2 Integer -> Natural -> Integer
forall a b. Exponent a b => a -> b -> a
^ forall (n :: Natural). KnownNat n => Natural
getNatural @n))

instance (FromConstant Natural a, Finite a, AdditiveMonoid a, KnownNat n, MultiplicativeSemigroup (UInt n a)) => Scale Natural (UInt n a)

instance (FromConstant Natural a, Finite a, AdditiveMonoid a, KnownNat n, MultiplicativeSemigroup (UInt n a)) => Scale Integer (UInt n a)

instance MultiplicativeMonoid (UInt n a) => Exponent (UInt n a) Natural where
    ^ :: UInt n a -> Natural -> UInt n a
(^) = UInt n a -> Natural -> UInt n a
forall a. MultiplicativeMonoid a => a -> Natural -> a
natPow

cast :: forall a n . (FromConstant Natural a, Finite a, AdditiveMonoid a, KnownNat n) => Natural -> (UInt n a, [a])
cast :: forall a (n :: Natural).
(FromConstant Natural a, Finite a, AdditiveMonoid a, KnownNat n) =>
Natural -> (UInt n a, [a])
cast Natural
n =
    let base :: Natural
base = Natural
2 Natural -> Natural -> Natural
forall a b. Exponent a b => a -> b -> a
^ forall a (n :: Natural). (Finite a, KnownNat n) => Natural
registerSize @a @n
        registers :: [a]
registers = (Natural -> a) -> [Natural] -> [a]
forall a b. (a -> b) -> [a] -> [b]
map Natural -> a
forall a b. FromConstant a b => a -> b
fromConstant ([Natural] -> [a]) -> [Natural] -> [a]
forall a b. (a -> b) -> a -> b
$ ((Natural -> Maybe (Natural, Natural)) -> Natural -> [Natural])
-> Natural -> (Natural -> Maybe (Natural, Natural)) -> [Natural]
forall a b c. (a -> b -> c) -> b -> a -> c
flip (Natural -> Maybe (Natural, Natural)) -> Natural -> [Natural]
forall b a. (b -> Maybe (a, b)) -> b -> [a]
unfoldr Natural
n ((Natural -> Maybe (Natural, Natural)) -> [Natural])
-> (Natural -> Maybe (Natural, Natural)) -> [Natural]
forall a b. (a -> b) -> a -> b
$ \case
            Natural
0 -> Maybe (Natural, Natural)
forall a. Maybe a
Haskell.Nothing
            Natural
x -> (Natural, Natural) -> Maybe (Natural, Natural)
forall a. a -> Maybe a
Haskell.Just ((Natural, Natural) -> (Natural, Natural)
forall a b. (a, b) -> (b, a)
swap ((Natural, Natural) -> (Natural, Natural))
-> (Natural, Natural) -> (Natural, Natural)
forall a b. (a -> b) -> a -> b
$ Natural
x Natural -> Natural -> (Natural, Natural)
forall a. Integral a => a -> a -> (a, a)
`Haskell.divMod` Natural
base)
        r :: Natural
r = forall a (n :: Natural). (Finite a, KnownNat n) => Natural
numberOfRegisters @a @n Natural -> Natural -> Natural
-! Natural
1
     in case Natural -> [a] -> ([a], [a])
forall {a}. Natural -> [a] -> ([a], [a])
greedySplitAt Natural
r [a]
registers of
        ([a]
lo, a
hi:[a]
rest) -> ([a] -> a -> UInt n a
forall (n :: Natural) a. [a] -> a -> UInt n a
UInt [a]
lo a
hi, [a]
rest)
        ([a]
lo, [])      -> ([a] -> a -> UInt n a
forall (n :: Natural) a. [a] -> a -> UInt n a
UInt ([a]
lo [a] -> [a] -> [a]
forall a. [a] -> [a] -> [a]
++ Natural -> a -> [a]
forall a. Natural -> a -> [a]
replicate (Natural
r Natural -> Natural -> Natural
-! [a] -> Natural
forall (t :: Type -> Type) a. Foldable t => t a -> Natural
length [a]
lo) a
forall a. AdditiveMonoid a => a
zero) a
forall a. AdditiveMonoid a => a
zero, [])
    where
        greedySplitAt :: Natural -> [a] -> ([a], [a])
greedySplitAt Natural
0 [a]
xs = ([], [a]
xs)
        greedySplitAt Natural
_ [] = ([], [])
        greedySplitAt Natural
m (a
x : [a]
xs) =
            let ([a]
ys, [a]
zs) = Natural -> [a] -> ([a], [a])
greedySplitAt (Natural
m Natural -> Natural -> Natural
-! Natural
1) [a]
xs
             in (a
x a -> [a] -> [a]
forall a. a -> [a] -> [a]
: [a]
ys, [a]
zs)

-- | Extended Euclidean algorithm.
-- Exploits the fact that @s_i@ and @t_i@ change signs in turns on each iteration, so it adjusts the formulas correspondingly
-- and never requires signed arithmetic.
-- (i.e. it calculates @x = b - a@ instead of @x = a - b@ when @a - b@ is negative
-- and changes @y - x@ to @y + x@ on the following iteration)
-- This only affects Bezout coefficients, remainders are calculated without changes as they are always non-negative.
--
-- If the algorithm is used to calculate Bezout coefficients,
-- it requires that @a@ and @b@ are coprime, @b@ is not 1 and @a@ is not 0, otherwise the optimisation above is not valid.
--
-- If the algorithm is only used to find @gcd(a, b)@ (i.e. @s@ and @t@ will be discarded), @a@ and @b@ can be arbitrary integers.
--
eea
    :: forall n 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 :: 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 n a
a UInt n a
b = Natural
-> UInt n 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' Natural
1 UInt n a
a UInt n a
b UInt n a
forall a. MultiplicativeMonoid a => a
one UInt n a
forall a. AdditiveMonoid a => a
zero UInt n a
forall a. AdditiveMonoid a => a
zero UInt n a
forall a. MultiplicativeMonoid a => a
one
    where
        iterations :: Natural
        iterations :: Natural
iterations = forall (n :: Natural). KnownNat n => Natural
value @n Natural -> Natural -> Natural
forall a. MultiplicativeSemigroup a => a -> a -> a
* Natural
2 Natural -> Natural -> Natural
forall a. AdditiveSemigroup a => a -> a -> a
+ Natural
1

        eea' :: Natural -> UInt n 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' :: Natural
-> UInt n 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' Natural
iteration UInt n a
oldR UInt n a
r UInt n a
oldS UInt n a
s UInt n a
oldT UInt n a
t
          | Natural
iteration Natural -> Natural -> Bool
forall b a. Eq b a => a -> a -> b
== Natural
iterations = (UInt n a
oldS, UInt n a
oldT, UInt n a
oldR)
          | Bool
otherwise = forall b a. Conditional b a => a -> a -> b -> a
bool @(Bool a) (UInt n a, UInt n a, UInt n a)
rec (if Natural -> Bool
forall a. Integral a => a -> Bool
Haskell.even Natural
iteration then UInt n a
b UInt n a -> UInt n a -> UInt n a
forall a. AdditiveGroup a => a -> a -> a
- UInt n a
oldS else UInt n a
oldS, if Natural -> Bool
forall a. Integral a => a -> Bool
Haskell.odd Natural
iteration then UInt n a
a UInt n a -> UInt n a -> UInt n a
forall a. AdditiveGroup a => a -> a -> a
- UInt n a
oldT else UInt n a
oldT, UInt n a
oldR) (UInt n a
r UInt n a -> UInt n a -> Bool a
forall b a. Eq b a => a -> a -> b
== UInt n a
forall a. AdditiveMonoid a => a
zero)
            where
                quotient :: UInt n a
quotient = UInt n a
oldR UInt n a -> UInt n a -> UInt n a
forall a. EuclideanDomain a => a -> a -> a
`div` UInt n a
r

                rec :: (UInt n a, UInt n a, UInt n a)
rec = Natural
-> UInt n 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' (Natural
iteration Natural -> Natural -> Natural
forall a. AdditiveSemigroup a => a -> a -> a
+ Natural
1) UInt n a
r (UInt n a
oldR UInt n a -> UInt n a -> UInt n a
forall a. AdditiveGroup a => a -> a -> a
- UInt n a
quotient UInt n a -> UInt n a -> UInt n a
forall a. MultiplicativeSemigroup a => a -> a -> a
* UInt n a
r) UInt n a
s (UInt n a
quotient UInt n a -> UInt n a -> UInt n a
forall a. MultiplicativeSemigroup a => a -> a -> a
* UInt n a
s UInt n a -> UInt n a -> UInt n a
forall a. AdditiveSemigroup a => a -> a -> a
+ UInt n a
oldS) UInt n a
t (UInt n a
quotient UInt n a -> UInt n a -> UInt n a
forall a. MultiplicativeSemigroup a => a -> a -> a
* UInt n a
t UInt n a -> UInt n a -> UInt n a
forall a. AdditiveSemigroup a => a -> a -> a
+ UInt n a
oldT)

--------------------------------------------------------------------------------

instance (Finite (Zp p), KnownNat n, KnownNat m, n <= m) => Extend (UInt n (Zp p)) (UInt m (Zp p)) where
    extend :: UInt n (Zp p) -> UInt m (Zp p)
extend = forall a b. FromConstant a b => a -> b
fromConstant @Natural (Natural -> UInt m (Zp p))
-> (UInt n (Zp p) -> Natural) -> UInt n (Zp p) -> UInt m (Zp p)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. UInt n (Zp p) -> Natural
forall a b. ToConstant a b => a -> b
toConstant

instance (Finite (Zp p), KnownNat n, KnownNat m, m <= n) => Shrink (UInt n (Zp p)) (UInt m (Zp p)) where
    shrink :: UInt n (Zp p) -> UInt m (Zp p)
shrink = forall a b. FromConstant a b => a -> b
fromConstant @Natural (Natural -> UInt m (Zp p))
-> (UInt n (Zp p) -> Natural) -> UInt n (Zp p) -> UInt m (Zp p)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. UInt n (Zp p) -> Natural
forall a b. ToConstant a b => a -> b
toConstant

instance (Finite (Zp p), KnownNat n) => EuclideanDomain (UInt n (Zp p)) where
    divMod :: UInt n (Zp p) -> UInt n (Zp p) -> (UInt n (Zp p), UInt n (Zp p))
divMod UInt n (Zp p)
n UInt n (Zp p)
d = let (Natural
q, Natural
r) = Natural -> Natural -> (Natural, Natural)
forall a. Integral a => a -> a -> (a, a)
Haskell.divMod (UInt n (Zp p) -> Natural
forall a b. ToConstant a b => a -> b
toConstant UInt n (Zp p)
n :: Natural) (UInt n (Zp p) -> Natural
forall a b. ToConstant a b => a -> b
toConstant UInt n (Zp p)
d :: Natural)
                  in (Natural -> UInt n (Zp p)
forall a b. FromConstant a b => a -> b
fromConstant Natural
q, Natural -> UInt n (Zp p)
forall a b. FromConstant a b => a -> b
fromConstant Natural
r)

instance (Finite (Zp p), KnownNat n) => Eq (Bool (Zp p)) (UInt n (Zp p)) where
    UInt n (Zp p)
x == :: UInt n (Zp p) -> UInt n (Zp p) -> Bool (Zp p)
== UInt n (Zp p)
y = Zp p -> Bool (Zp p)
forall x. x -> Bool x
Bool (Zp p -> Bool (Zp p)) -> (Bool -> Zp p) -> Bool -> Bool (Zp p)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> Zp p
forall (p :: Natural). KnownNat p => Integer -> Zp p
toZp (Integer -> Zp p) -> (Bool -> Integer) -> Bool -> Zp p
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Integer
forall a b. (Integral a, Num b) => a -> b
Haskell.fromIntegral (Int -> Integer) -> (Bool -> Int) -> Bool -> Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool -> Int
forall a. Enum a => a -> Int
Haskell.fromEnum (Bool -> Bool (Zp p)) -> Bool -> Bool (Zp p)
forall a b. (a -> b) -> a -> b
$ forall a b. ToConstant a b => a -> b
toConstant @_ @Natural UInt n (Zp p)
x Natural -> Natural -> Bool
forall a. Eq a => a -> a -> Bool
Haskell.== UInt n (Zp p) -> Natural
forall a b. ToConstant a b => a -> b
toConstant UInt n (Zp p)
y
    UInt n (Zp p)
x /= :: UInt n (Zp p) -> UInt n (Zp p) -> Bool (Zp p)
/= UInt n (Zp p)
y = Zp p -> Bool (Zp p)
forall x. x -> Bool x
Bool (Zp p -> Bool (Zp p)) -> (Bool -> Zp p) -> Bool -> Bool (Zp p)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> Zp p
forall (p :: Natural). KnownNat p => Integer -> Zp p
toZp (Integer -> Zp p) -> (Bool -> Integer) -> Bool -> Zp p
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Integer
forall a b. (Integral a, Num b) => a -> b
Haskell.fromIntegral (Int -> Integer) -> (Bool -> Int) -> Bool -> Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool -> Int
forall a. Enum a => a -> Int
Haskell.fromEnum (Bool -> Bool (Zp p)) -> Bool -> Bool (Zp p)
forall a b. (a -> b) -> a -> b
$ forall a b. ToConstant a b => a -> b
toConstant @_ @Natural UInt n (Zp p)
x Natural -> Natural -> Bool
forall a. Eq a => a -> a -> Bool
Haskell./= UInt n (Zp p) -> Natural
forall a b. ToConstant a b => a -> b
toConstant UInt n (Zp p)
y

instance (Finite (Zp p), KnownNat n) => Ord (Bool (Zp p)) (UInt n (Zp p)) where
    UInt n (Zp p)
x <= :: UInt n (Zp p) -> UInt n (Zp p) -> Bool (Zp p)
<= UInt n (Zp p)
y = Zp p -> Bool (Zp p)
forall x. x -> Bool x
Bool (Zp p -> Bool (Zp p)) -> (Bool -> Zp p) -> Bool -> Bool (Zp p)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> Zp p
forall (p :: Natural). KnownNat p => Integer -> Zp p
toZp (Integer -> Zp p) -> (Bool -> Integer) -> Bool -> Zp p
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Integer
forall a b. (Integral a, Num b) => a -> b
Haskell.fromIntegral (Int -> Integer) -> (Bool -> Int) -> Bool -> Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool -> Int
forall a. Enum a => a -> Int
Haskell.fromEnum (Bool -> Bool (Zp p)) -> Bool -> Bool (Zp p)
forall a b. (a -> b) -> a -> b
$ forall a b. ToConstant a b => a -> b
toConstant @_ @Natural UInt n (Zp p)
x Natural -> Natural -> Bool
forall a. Ord a => a -> a -> Bool
Haskell.<= UInt n (Zp p) -> Natural
forall a b. ToConstant a b => a -> b
toConstant UInt n (Zp p)
y
    UInt n (Zp p)
x < :: UInt n (Zp p) -> UInt n (Zp p) -> Bool (Zp p)
< UInt n (Zp p)
y  = Zp p -> Bool (Zp p)
forall x. x -> Bool x
Bool (Zp p -> Bool (Zp p)) -> (Bool -> Zp p) -> Bool -> Bool (Zp p)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> Zp p
forall (p :: Natural). KnownNat p => Integer -> Zp p
toZp (Integer -> Zp p) -> (Bool -> Integer) -> Bool -> Zp p
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Integer
forall a b. (Integral a, Num b) => a -> b
Haskell.fromIntegral (Int -> Integer) -> (Bool -> Int) -> Bool -> Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool -> Int
forall a. Enum a => a -> Int
Haskell.fromEnum (Bool -> Bool (Zp p)) -> Bool -> Bool (Zp p)
forall a b. (a -> b) -> a -> b
$ forall a b. ToConstant a b => a -> b
toConstant @_ @Natural UInt n (Zp p)
x Natural -> Natural -> Bool
forall a. Ord a => a -> a -> Bool
Haskell.< UInt n (Zp p) -> Natural
forall a b. ToConstant a b => a -> b
toConstant UInt n (Zp p)
y
    UInt n (Zp p)
x >= :: UInt n (Zp p) -> UInt n (Zp p) -> Bool (Zp p)
>= UInt n (Zp p)
y = Zp p -> Bool (Zp p)
forall x. x -> Bool x
Bool (Zp p -> Bool (Zp p)) -> (Bool -> Zp p) -> Bool -> Bool (Zp p)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> Zp p
forall (p :: Natural). KnownNat p => Integer -> Zp p
toZp (Integer -> Zp p) -> (Bool -> Integer) -> Bool -> Zp p
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Integer
forall a b. (Integral a, Num b) => a -> b
Haskell.fromIntegral (Int -> Integer) -> (Bool -> Int) -> Bool -> Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool -> Int
forall a. Enum a => a -> Int
Haskell.fromEnum (Bool -> Bool (Zp p)) -> Bool -> Bool (Zp p)
forall a b. (a -> b) -> a -> b
$ forall a b. ToConstant a b => a -> b
toConstant @_ @Natural UInt n (Zp p)
x Natural -> Natural -> Bool
forall a. Ord a => a -> a -> Bool
Haskell.>= UInt n (Zp p) -> Natural
forall a b. ToConstant a b => a -> b
toConstant UInt n (Zp p)
y
    UInt n (Zp p)
x > :: UInt n (Zp p) -> UInt n (Zp p) -> Bool (Zp p)
> UInt n (Zp p)
y  = Zp p -> Bool (Zp p)
forall x. x -> Bool x
Bool (Zp p -> Bool (Zp p)) -> (Bool -> Zp p) -> Bool -> Bool (Zp p)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> Zp p
forall (p :: Natural). KnownNat p => Integer -> Zp p
toZp (Integer -> Zp p) -> (Bool -> Integer) -> Bool -> Zp p
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Integer
forall a b. (Integral a, Num b) => a -> b
Haskell.fromIntegral (Int -> Integer) -> (Bool -> Int) -> Bool -> Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool -> Int
forall a. Enum a => a -> Int
Haskell.fromEnum (Bool -> Bool (Zp p)) -> Bool -> Bool (Zp p)
forall a b. (a -> b) -> a -> b
$ forall a b. ToConstant a b => a -> b
toConstant @_ @Natural UInt n (Zp p)
x Natural -> Natural -> Bool
forall a. Ord a => a -> a -> Bool
Haskell.> UInt n (Zp p) -> Natural
forall a b. ToConstant a b => a -> b
toConstant UInt n (Zp p)
y
    max :: UInt n (Zp p) -> UInt n (Zp p) -> UInt n (Zp p)
max UInt n (Zp p)
x UInt n (Zp p)
y = Natural -> UInt n (Zp p)
forall a b. FromConstant a b => a -> b
fromConstant (Natural -> UInt n (Zp p)) -> Natural -> UInt n (Zp p)
forall a b. (a -> b) -> a -> b
$ Natural -> Natural -> Natural
forall a. Ord a => a -> a -> a
Haskell.max (forall a b. ToConstant a b => a -> b
toConstant @_ @Natural UInt n (Zp p)
x) (UInt n (Zp p) -> Natural
forall a b. ToConstant a b => a -> b
toConstant UInt n (Zp p)
y)
    min :: UInt n (Zp p) -> UInt n (Zp p) -> UInt n (Zp p)
min UInt n (Zp p)
x UInt n (Zp p)
y = Natural -> UInt n (Zp p)
forall a b. FromConstant a b => a -> b
fromConstant (Natural -> UInt n (Zp p)) -> Natural -> UInt n (Zp p)
forall a b. (a -> b) -> a -> b
$ Natural -> Natural -> Natural
forall a. Ord a => a -> a -> a
Haskell.min (forall a b. ToConstant a b => a -> b
toConstant @_ @Natural UInt n (Zp p)
x) (UInt n (Zp p) -> Natural
forall a b. ToConstant a b => a -> b
toConstant UInt n (Zp p)
y)

instance (Finite (Zp p), KnownNat n) => ToConstant (UInt n (Zp p)) Natural where
    toConstant :: UInt n (Zp p) -> Natural
toConstant (UInt [Zp p]
xs Zp p
x) = (Zp p -> Natural -> Natural) -> Natural -> [Zp p] -> Natural
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: Type -> Type) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\Zp p
p Natural
y -> Zp p -> Natural
forall (p :: Natural). Zp p -> Natural
fromZp Zp p
p Natural -> Natural -> Natural
forall a. AdditiveSemigroup a => a -> a -> a
+ Natural
base Natural -> Natural -> Natural
forall a. MultiplicativeSemigroup a => a -> a -> a
* Natural
y) Natural
0 ([Zp p]
xs [Zp p] -> [Zp p] -> [Zp p]
forall a. [a] -> [a] -> [a]
++ [Zp p
x])
        where base :: Natural
base = Natural
2 Natural -> Natural -> Natural
forall a b. Exponent a b => a -> b -> a
^ forall a (n :: Natural). (Finite a, KnownNat n) => Natural
registerSize @(Zp p) @n

instance (Finite (Zp p), KnownNat n) => ToConstant (UInt n (Zp p)) Integer where
    toConstant :: UInt n (Zp p) -> Integer
toConstant = forall a b. (Integral a, Num b) => a -> b
Haskell.fromIntegral @Natural (Natural -> Integer)
-> (UInt n (Zp p) -> Natural) -> UInt n (Zp p) -> Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. UInt n (Zp p) -> Natural
forall a b. ToConstant a b => a -> b
toConstant

instance (Finite (Zp p), KnownNat n) => AdditiveSemigroup (UInt n (Zp p)) where
    UInt n (Zp p)
x + :: UInt n (Zp p) -> UInt n (Zp p) -> UInt n (Zp p)
+ UInt n (Zp p)
y = Natural -> UInt n (Zp p)
forall a b. FromConstant a b => a -> b
fromConstant (Natural -> UInt n (Zp p)) -> Natural -> UInt n (Zp p)
forall a b. (a -> b) -> a -> b
$ UInt n (Zp p) -> Natural
forall a b. ToConstant a b => a -> b
toConstant UInt n (Zp p)
x Natural -> Natural -> Natural
forall a. AdditiveSemigroup a => a -> a -> a
+ forall a b. ToConstant a b => a -> b
toConstant @_ @Natural UInt n (Zp p)
y

instance (Finite (Zp p), KnownNat n) => AdditiveMonoid (UInt n (Zp p)) where
    zero :: UInt n (Zp p)
zero = Natural -> UInt n (Zp p)
forall a b. FromConstant a b => a -> b
fromConstant (Natural
0 :: Natural)

instance (Finite (Zp p), KnownNat n) => AdditiveGroup (UInt n (Zp p)) where
    UInt n (Zp p)
x - :: UInt n (Zp p) -> UInt n (Zp p) -> UInt n (Zp p)
- UInt n (Zp p)
y = Natural -> UInt n (Zp p)
forall a b. FromConstant a b => a -> b
fromConstant (Natural -> UInt n (Zp p)) -> Natural -> UInt n (Zp p)
forall a b. (a -> b) -> a -> b
$ UInt n (Zp p) -> Natural
forall a b. ToConstant a b => a -> b
toConstant UInt n (Zp p)
x Natural -> Natural -> Natural
forall a. AdditiveSemigroup a => a -> a -> a
+ Natural
2 Natural -> Natural -> Natural
forall a b. Exponent a b => a -> b -> a
^ forall (n :: Natural). KnownNat n => Natural
getNatural @n Natural -> Natural -> Natural
-! UInt n (Zp p) -> Natural
forall a b. ToConstant a b => a -> b
toConstant UInt n (Zp p)
y
    negate :: UInt n (Zp p) -> UInt n (Zp p)
negate UInt n (Zp p)
x = Natural -> UInt n (Zp p)
forall a b. FromConstant a b => a -> b
fromConstant (Natural -> UInt n (Zp p)) -> Natural -> UInt n (Zp p)
forall a b. (a -> b) -> a -> b
$ Natural
2 Natural -> Natural -> Natural
forall a b. Exponent a b => a -> b -> a
^ forall (n :: Natural). KnownNat n => Natural
getNatural @n Natural -> Natural -> Natural
-! UInt n (Zp p) -> Natural
forall a b. ToConstant a b => a -> b
toConstant UInt n (Zp p)
x

instance (Finite (Zp p), KnownNat n) => MultiplicativeSemigroup (UInt n (Zp p)) where
    UInt n (Zp p)
x * :: UInt n (Zp p) -> UInt n (Zp p) -> UInt n (Zp p)
* UInt n (Zp p)
y = Natural -> UInt n (Zp p)
forall a b. FromConstant a b => a -> b
fromConstant (Natural -> UInt n (Zp p)) -> Natural -> UInt n (Zp p)
forall a b. (a -> b) -> a -> b
$ UInt n (Zp p) -> Natural
forall a b. ToConstant a b => a -> b
toConstant UInt n (Zp p)
x Natural -> Natural -> Natural
forall a. MultiplicativeSemigroup a => a -> a -> a
* forall a b. ToConstant a b => a -> b
toConstant @_ @Natural UInt n (Zp p)
y

instance (Finite (Zp p), KnownNat n) => MultiplicativeMonoid (UInt n (Zp p)) where
    one :: UInt n (Zp p)
one = Natural -> UInt n (Zp p)
forall a b. FromConstant a b => a -> b
fromConstant (Natural
1 :: Natural)

instance (Finite (Zp p), KnownNat n) => Semiring (UInt n (Zp p))

instance (Finite (Zp p), KnownNat n) => Ring (UInt n (Zp p))

instance (Finite (Zp p), KnownNat n) => Arbitrary (UInt n (Zp p)) where
    arbitrary :: Gen (UInt n (Zp p))
arbitrary = [Zp p] -> Zp p -> UInt n (Zp p)
forall (n :: Natural) a. [a] -> a -> UInt n a
UInt
        ([Zp p] -> Zp p -> UInt n (Zp p))
-> Gen [Zp p] -> Gen (Zp p -> UInt n (Zp p))
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Natural -> Gen (Zp p) -> Gen [Zp p]
forall (f :: Type -> Type) a.
Applicative f =>
Natural -> f a -> f [a]
replicateA (forall a (n :: Natural). (Finite a, KnownNat n) => Natural
numberOfRegisters @(Zp p) @n Natural -> Natural -> Natural
-! Natural
1) (Natural -> Gen (Zp p)
forall {b} {b}.
(FromConstant Integer b, Exponent Integer b) =>
b -> Gen b
toss (Natural -> Gen (Zp p)) -> Natural -> Gen (Zp p)
forall a b. (a -> b) -> a -> b
$ forall a (n :: Natural). (Finite a, KnownNat n) => Natural
registerSize @(Zp p) @n)
        Gen (Zp p -> UInt n (Zp p)) -> Gen (Zp p) -> Gen (UInt n (Zp p))
forall a b. Gen (a -> b) -> Gen a -> Gen b
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> Natural -> Gen (Zp p)
forall {b} {b}.
(FromConstant Integer b, Exponent Integer b) =>
b -> Gen b
toss (forall a (n :: Natural). (Finite a, KnownNat n) => Natural
highRegisterSize @(Zp p) @n)
        where toss :: b -> Gen b
toss b
b = Integer -> b
forall a b. FromConstant a b => a -> b
fromConstant (Integer -> b) -> Gen Integer -> Gen b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> (Integer, Integer) -> Gen Integer
chooseInteger (Integer
0, Integer
2 Integer -> b -> Integer
forall a b. Exponent a b => a -> b -> a
^ b
b Integer -> Integer -> Integer
forall a. AdditiveGroup a => a -> a -> a
- Integer
1)

--------------------------------------------------------------------------------

instance (Arithmetic a, KnownNat n) => SymbolicData a (UInt n (ArithmeticCircuit a)) where
    pieces :: UInt n (ArithmeticCircuit a) -> [ArithmeticCircuit a]
pieces (UInt [ArithmeticCircuit a]
as ArithmeticCircuit a
a) = [ArithmeticCircuit a]
as [ArithmeticCircuit a]
-> [ArithmeticCircuit a] -> [ArithmeticCircuit a]
forall a. [a] -> [a] -> [a]
++ [ArithmeticCircuit a
a]

    restore :: [ArithmeticCircuit a] -> UInt n (ArithmeticCircuit a)
restore [ArithmeticCircuit a]
as = case Natural
-> [ArithmeticCircuit a]
-> ([ArithmeticCircuit a], [ArithmeticCircuit a])
forall {a}. Natural -> [a] -> ([a], [a])
splitAt (forall a (n :: Natural). (Finite a, KnownNat n) => Natural
numberOfRegisters @a @n Natural -> Natural -> Natural
-! Natural
1) [ArithmeticCircuit a]
as of
        ([ArithmeticCircuit a]
lo, [ArithmeticCircuit a
hi]) -> [ArithmeticCircuit a]
-> ArithmeticCircuit a -> UInt n (ArithmeticCircuit a)
forall (n :: Natural) a. [a] -> a -> UInt n a
UInt [ArithmeticCircuit a]
lo ArithmeticCircuit a
hi
        ([ArithmeticCircuit a]
_, [ArithmeticCircuit a]
_)     -> String -> UInt n (ArithmeticCircuit a)
forall a. HasCallStack => String -> a
error String
"UInt: invalid number of values"

    typeSize :: Natural
typeSize = forall a (n :: Natural). (Finite a, KnownNat n) => Natural
numberOfRegisters @a @n

instance (Arithmetic a, KnownNat n, KnownNat m, n <= m) => Extend (UInt n (ArithmeticCircuit a)) (UInt m (ArithmeticCircuit a)) where
    extend :: UInt n (ArithmeticCircuit a) -> UInt m (ArithmeticCircuit a)
extend (UInt [ArithmeticCircuit a]
rlows ArithmeticCircuit a
rhi) =
        case forall a (n :: Natural). (Finite a, KnownNat n) => Natural
numberOfRegisters @a @m Natural -> Natural -> Natural
-! forall a (n :: Natural). (Finite a, KnownNat n) => Natural
numberOfRegisters @a @n of
          Natural
0    -> [ArithmeticCircuit a]
-> ArithmeticCircuit a -> UInt m (ArithmeticCircuit a)
forall (n :: Natural) a. [a] -> a -> UInt n a
UInt [ArithmeticCircuit a]
rlows ArithmeticCircuit a
rhi
          Natural
diff -> [ArithmeticCircuit a]
-> ArithmeticCircuit a -> UInt m (ArithmeticCircuit a)
forall (n :: Natural) a. [a] -> a -> UInt n a
UInt ([ArithmeticCircuit a]
rlows [ArithmeticCircuit a]
-> [ArithmeticCircuit a] -> [ArithmeticCircuit a]
forall a. Semigroup a => a -> a -> a
<> [ArithmeticCircuit a
rhi] [ArithmeticCircuit a]
-> [ArithmeticCircuit a] -> [ArithmeticCircuit a]
forall a. Semigroup a => a -> a -> a
<> Natural -> ArithmeticCircuit a -> [ArithmeticCircuit a]
forall a. Natural -> a -> [a]
replicate (Natural
diff Natural -> Natural -> Natural
-! Natural
1) ArithmeticCircuit a
forall a. AdditiveMonoid a => a
zero) ArithmeticCircuit a
forall a. AdditiveMonoid a => a
zero

instance (Arithmetic a, KnownNat n, KnownNat k, k <= n) => Shrink (UInt n (ArithmeticCircuit a)) (UInt k (ArithmeticCircuit a)) where
    shrink :: UInt n (ArithmeticCircuit a) -> UInt k (ArithmeticCircuit a)
shrink (UInt [ArithmeticCircuit a]
rlows ArithmeticCircuit a
rhi) =
        case (forall i (m :: Type -> Type). MonadBlueprint i a m => m [i])
-> [ArithmeticCircuit a]
forall a (f :: Type -> Type).
(Arithmetic a, Functor f) =>
(forall i (m :: Type -> Type). MonadBlueprint i a m => m (f i))
-> f (ArithmeticCircuit a)
circuits m [i]
forall i (m :: Type -> Type). MonadBlueprint i a m => m [i]
solve of
             (ArithmeticCircuit a
x:[ArithmeticCircuit a]
xs) -> [ArithmeticCircuit a]
-> ArithmeticCircuit a -> UInt k (ArithmeticCircuit a)
forall (n :: Natural) a. [a] -> a -> UInt n a
UInt ([ArithmeticCircuit a] -> [ArithmeticCircuit a]
forall a. [a] -> [a]
Haskell.reverse [ArithmeticCircuit a]
xs) ArithmeticCircuit a
x
             [ArithmeticCircuit a]
_      -> String -> UInt k (ArithmeticCircuit a)
forall a. HasCallStack => String -> a
error String
"Iso ByteString UInt : unreachable"
        where
            solve :: forall i m. MonadBlueprint i a m => m [i]
            solve :: forall i (m :: Type -> Type). MonadBlueprint i a m => m [i]
solve = do
                [i]
bsBits <- ArithmeticCircuit a
-> [ArithmeticCircuit a]
-> Natural
-> Natural
-> forall i (m :: Type -> Type). MonadBlueprint i a m => m [i]
forall a.
ArithmeticCircuit a
-> [ArithmeticCircuit a]
-> Natural
-> Natural
-> forall i (m :: Type -> Type). MonadBlueprint i a m => m [i]
toBits ArithmeticCircuit a
rhi ([ArithmeticCircuit a] -> [ArithmeticCircuit a]
forall a. [a] -> [a]
Haskell.reverse [ArithmeticCircuit a]
rlows) (forall a (n :: Natural). (Finite a, KnownNat n) => Natural
highRegisterSize @a @n) (forall a (n :: Natural). (Finite a, KnownNat n) => Natural
registerSize @a @n)
                Natural
-> Natural
-> forall i (m :: Type -> Type).
   MonadBlueprint i a m =>
   [i] -> m [i]
forall a.
Natural
-> Natural
-> forall i (m :: Type -> Type).
   MonadBlueprint i a m =>
   [i] -> m [i]
fromBits (forall a (n :: Natural). (Finite a, KnownNat n) => Natural
highRegisterSize @a @k) (forall a (n :: Natural). (Finite a, KnownNat n) => Natural
registerSize @a @k) (Natural -> [i] -> [i]
forall a. Natural -> [a] -> [a]
drop (forall (n :: Natural). KnownNat n => Natural
value @n Natural -> Natural -> Natural
-! (forall (n :: Natural). KnownNat n => Natural
value @k)) [i]
bsBits)

instance (Arithmetic a, KnownNat n) => EuclideanDomain (UInt n (ArithmeticCircuit a)) where
    divMod :: UInt n (ArithmeticCircuit a)
-> UInt n (ArithmeticCircuit a)
-> (UInt n (ArithmeticCircuit a), UInt n (ArithmeticCircuit a))
divMod (UInt [ArithmeticCircuit a]
rlows ArithmeticCircuit a
rhi) UInt n (ArithmeticCircuit a)
d = forall b a. Conditional b a => a -> a -> b -> a
bool @(Bool (ArithmeticCircuit a)) (UInt n (ArithmeticCircuit a)
q, UInt n (ArithmeticCircuit a)
r) (UInt n (ArithmeticCircuit a)
forall a. AdditiveMonoid a => a
zero, UInt n (ArithmeticCircuit a)
forall a. AdditiveMonoid a => a
zero) (UInt n (ArithmeticCircuit a)
d UInt n (ArithmeticCircuit a)
-> UInt n (ArithmeticCircuit a) -> Bool (ArithmeticCircuit a)
forall b a. Eq b a => a -> a -> b
== UInt n (ArithmeticCircuit a)
forall a. AdditiveMonoid a => a
zero)
        where
            (UInt n (ArithmeticCircuit a)
q, UInt n (ArithmeticCircuit a)
r) = ((UInt n (ArithmeticCircuit a), UInt n (ArithmeticCircuit a))
 -> Natural
 -> (UInt n (ArithmeticCircuit a), UInt n (ArithmeticCircuit a)))
-> (UInt n (ArithmeticCircuit a), UInt n (ArithmeticCircuit a))
-> [Natural]
-> (UInt n (ArithmeticCircuit a), UInt n (ArithmeticCircuit a))
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: Type -> Type) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (UInt n (ArithmeticCircuit a), UInt n (ArithmeticCircuit a))
-> Natural
-> (UInt n (ArithmeticCircuit a), UInt n (ArithmeticCircuit a))
longDivisionStep (UInt n (ArithmeticCircuit a)
forall a. AdditiveMonoid a => a
zero, UInt n (ArithmeticCircuit a)
forall a. AdditiveMonoid a => a
zero) [forall (n :: Natural). KnownNat n => Natural
value @n Natural -> Natural -> Natural
-! Natural
1, forall (n :: Natural). KnownNat n => Natural
value @n Natural -> Natural -> Natural
-! Natural
2 .. Natural
0]

            numeratorBits :: [ArithmeticCircuit a]
            numeratorBits :: [ArithmeticCircuit a]
numeratorBits =
                (ArithmeticCircuit a -> [ArithmeticCircuit a])
-> [ArithmeticCircuit a] -> [ArithmeticCircuit a]
forall (t :: Type -> Type) a b.
Foldable t =>
(a -> [b]) -> t a -> [b]
concatMap (Natural -> [ArithmeticCircuit a] -> [ArithmeticCircuit a]
forall a. Natural -> [a] -> [a]
take (forall a (n :: Natural). (Finite a, KnownNat n) => Natural
registerSize @a @n) ([ArithmeticCircuit a] -> [ArithmeticCircuit a])
-> (ArithmeticCircuit a -> [ArithmeticCircuit a])
-> ArithmeticCircuit a
-> [ArithmeticCircuit a]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ArithmeticCircuit a -> [ArithmeticCircuit a]
forall a. BinaryExpansion a => a -> [a]
binaryExpansion) [ArithmeticCircuit a]
rlows [ArithmeticCircuit a]
-> [ArithmeticCircuit a] -> [ArithmeticCircuit a]
forall a. Semigroup a => a -> a -> a
<>
                Natural -> [ArithmeticCircuit a] -> [ArithmeticCircuit a]
forall a. Natural -> [a] -> [a]
take (forall a (n :: Natural). (Finite a, KnownNat n) => Natural
highRegisterSize @a @n) (ArithmeticCircuit a -> [ArithmeticCircuit a]
forall a. BinaryExpansion a => a -> [a]
binaryExpansion ArithmeticCircuit a
rhi)

            addBit :: UInt n (ArithmeticCircuit a) -> ArithmeticCircuit a -> UInt n (ArithmeticCircuit a)
            addBit :: UInt n (ArithmeticCircuit a)
-> ArithmeticCircuit a -> UInt n (ArithmeticCircuit a)
addBit (UInt [] ArithmeticCircuit a
hr) ArithmeticCircuit a
bit         = ([ArithmeticCircuit a]
-> ArithmeticCircuit a -> UInt n (ArithmeticCircuit a)
forall (n :: Natural) a. [a] -> a -> UInt n a
UInt [] (ArithmeticCircuit a -> UInt n (ArithmeticCircuit a))
-> ArithmeticCircuit a -> UInt n (ArithmeticCircuit a)
forall a b. (a -> b) -> a -> b
$ ArithmeticCircuit a
hr ArithmeticCircuit a -> ArithmeticCircuit a -> ArithmeticCircuit a
forall a. AdditiveSemigroup a => a -> a -> a
+ ArithmeticCircuit a
bit)
            addBit (UInt (ArithmeticCircuit a
low:[ArithmeticCircuit a]
lows) ArithmeticCircuit a
hr) ArithmeticCircuit a
bit = [ArithmeticCircuit a]
-> ArithmeticCircuit a -> UInt n (ArithmeticCircuit a)
forall (n :: Natural) a. [a] -> a -> UInt n a
UInt ((ArithmeticCircuit a
low ArithmeticCircuit a -> ArithmeticCircuit a -> ArithmeticCircuit a
forall a. AdditiveSemigroup a => a -> a -> a
+ ArithmeticCircuit a
bit) ArithmeticCircuit a
-> [ArithmeticCircuit a] -> [ArithmeticCircuit a]
forall a. a -> [a] -> [a]
: [ArithmeticCircuit a]
lows) ArithmeticCircuit a
hr

            longDivisionStep
                :: (UInt n (ArithmeticCircuit a), UInt n (ArithmeticCircuit a))
                -> Natural
                -> (UInt n (ArithmeticCircuit a), UInt n (ArithmeticCircuit a))
            longDivisionStep :: (UInt n (ArithmeticCircuit a), UInt n (ArithmeticCircuit a))
-> Natural
-> (UInt n (ArithmeticCircuit a), UInt n (ArithmeticCircuit a))
longDivisionStep (UInt n (ArithmeticCircuit a)
q', UInt n (ArithmeticCircuit a)
r') Natural
i =
                let rs :: UInt n (ArithmeticCircuit a)
rs = UInt n (ArithmeticCircuit a)
-> ArithmeticCircuit a -> UInt n (ArithmeticCircuit a)
addBit (UInt n (ArithmeticCircuit a)
r' UInt n (ArithmeticCircuit a)
-> UInt n (ArithmeticCircuit a) -> UInt n (ArithmeticCircuit a)
forall a. AdditiveSemigroup a => a -> a -> a
+ UInt n (ArithmeticCircuit a)
r') ([ArithmeticCircuit a]
numeratorBits [ArithmeticCircuit a] -> Natural -> ArithmeticCircuit a
forall a. [a] -> Natural -> a
!! Natural
i)
                 in forall b a. Conditional b a => a -> a -> b -> a
bool @(Bool (ArithmeticCircuit a)) (UInt n (ArithmeticCircuit a)
q', UInt n (ArithmeticCircuit a)
rs) (UInt n (ArithmeticCircuit a)
q' UInt n (ArithmeticCircuit a)
-> UInt n (ArithmeticCircuit a) -> UInt n (ArithmeticCircuit a)
forall a. AdditiveSemigroup a => a -> a -> a
+ Natural -> UInt n (ArithmeticCircuit a)
forall a b. FromConstant a b => a -> b
fromConstant ((Natural
2 :: Natural) Natural -> Natural -> Natural
forall a b. Exponent a b => a -> b -> a
^ Natural
i), UInt n (ArithmeticCircuit a)
rs UInt n (ArithmeticCircuit a)
-> UInt n (ArithmeticCircuit a) -> UInt n (ArithmeticCircuit a)
forall a. AdditiveGroup a => a -> a -> a
- UInt n (ArithmeticCircuit a)
d) (UInt n (ArithmeticCircuit a)
rs UInt n (ArithmeticCircuit a)
-> UInt n (ArithmeticCircuit a) -> Bool (ArithmeticCircuit a)
forall b a. Ord b a => a -> a -> b
>= UInt n (ArithmeticCircuit a)
d)

instance (Arithmetic a, KnownNat n) => Ord (Bool (ArithmeticCircuit a)) (UInt n (ArithmeticCircuit a)) where
    UInt n (ArithmeticCircuit a)
x <= :: UInt n (ArithmeticCircuit a)
-> UInt n (ArithmeticCircuit a) -> Bool (ArithmeticCircuit a)
<= UInt n (ArithmeticCircuit a)
y = UInt n (ArithmeticCircuit a)
y UInt n (ArithmeticCircuit a)
-> UInt n (ArithmeticCircuit a) -> Bool (ArithmeticCircuit a)
forall b a. Ord b a => a -> a -> b
>= UInt n (ArithmeticCircuit a)
x

    UInt n (ArithmeticCircuit a)
x < :: UInt n (ArithmeticCircuit a)
-> UInt n (ArithmeticCircuit a) -> Bool (ArithmeticCircuit a)
<  UInt n (ArithmeticCircuit a)
y = UInt n (ArithmeticCircuit a)
y UInt n (ArithmeticCircuit a)
-> UInt n (ArithmeticCircuit a) -> Bool (ArithmeticCircuit a)
forall b a. Ord b a => a -> a -> b
> UInt n (ArithmeticCircuit a)
x

    (UInt [ArithmeticCircuit a]
rs1 ArithmeticCircuit a
r1) >= :: UInt n (ArithmeticCircuit a)
-> UInt n (ArithmeticCircuit a) -> Bool (ArithmeticCircuit a)
>= (UInt [ArithmeticCircuit a]
rs2 ArithmeticCircuit a
r2) =
        [ArithmeticCircuit a]
-> [ArithmeticCircuit a] -> Bool (ArithmeticCircuit a)
forall a.
Arithmetic a =>
[ArithmeticCircuit a]
-> [ArithmeticCircuit a] -> Bool (ArithmeticCircuit a)
circuitGE
            (ArithmeticCircuit a -> [ArithmeticCircuit a]
forall a x. SymbolicData a x => x -> [ArithmeticCircuit a]
getBitsBE ArithmeticCircuit a
r1 [ArithmeticCircuit a]
-> [ArithmeticCircuit a] -> [ArithmeticCircuit a]
forall a. Semigroup a => a -> a -> a
<> [ArithmeticCircuit a] -> [ArithmeticCircuit a]
forall a. [a] -> [a]
Haskell.reverse ((ArithmeticCircuit a -> [ArithmeticCircuit a])
-> [ArithmeticCircuit a] -> [ArithmeticCircuit a]
forall (t :: Type -> Type) a b.
Foldable t =>
(a -> [b]) -> t a -> [b]
concatMap ArithmeticCircuit a -> [ArithmeticCircuit a]
forall a x. SymbolicData a x => x -> [ArithmeticCircuit a]
getBitsBE [ArithmeticCircuit a]
rs1))
            (ArithmeticCircuit a -> [ArithmeticCircuit a]
forall a x. SymbolicData a x => x -> [ArithmeticCircuit a]
getBitsBE ArithmeticCircuit a
r2 [ArithmeticCircuit a]
-> [ArithmeticCircuit a] -> [ArithmeticCircuit a]
forall a. Semigroup a => a -> a -> a
<> [ArithmeticCircuit a] -> [ArithmeticCircuit a]
forall a. [a] -> [a]
Haskell.reverse ((ArithmeticCircuit a -> [ArithmeticCircuit a])
-> [ArithmeticCircuit a] -> [ArithmeticCircuit a]
forall (t :: Type -> Type) a b.
Foldable t =>
(a -> [b]) -> t a -> [b]
concatMap ArithmeticCircuit a -> [ArithmeticCircuit a]
forall a x. SymbolicData a x => x -> [ArithmeticCircuit a]
getBitsBE [ArithmeticCircuit a]
rs2))

    (UInt [ArithmeticCircuit a]
rs1 ArithmeticCircuit a
r1) > :: UInt n (ArithmeticCircuit a)
-> UInt n (ArithmeticCircuit a) -> Bool (ArithmeticCircuit a)
> (UInt [ArithmeticCircuit a]
rs2 ArithmeticCircuit a
r2) =
        [ArithmeticCircuit a]
-> [ArithmeticCircuit a] -> Bool (ArithmeticCircuit a)
forall a.
Arithmetic a =>
[ArithmeticCircuit a]
-> [ArithmeticCircuit a] -> Bool (ArithmeticCircuit a)
circuitGT
            (ArithmeticCircuit a -> [ArithmeticCircuit a]
forall a x. SymbolicData a x => x -> [ArithmeticCircuit a]
getBitsBE ArithmeticCircuit a
r1 [ArithmeticCircuit a]
-> [ArithmeticCircuit a] -> [ArithmeticCircuit a]
forall a. Semigroup a => a -> a -> a
<> [ArithmeticCircuit a] -> [ArithmeticCircuit a]
forall a. [a] -> [a]
Haskell.reverse ((ArithmeticCircuit a -> [ArithmeticCircuit a])
-> [ArithmeticCircuit a] -> [ArithmeticCircuit a]
forall (t :: Type -> Type) a b.
Foldable t =>
(a -> [b]) -> t a -> [b]
concatMap ArithmeticCircuit a -> [ArithmeticCircuit a]
forall a x. SymbolicData a x => x -> [ArithmeticCircuit a]
getBitsBE [ArithmeticCircuit a]
rs1))
            (ArithmeticCircuit a -> [ArithmeticCircuit a]
forall a x. SymbolicData a x => x -> [ArithmeticCircuit a]
getBitsBE ArithmeticCircuit a
r2 [ArithmeticCircuit a]
-> [ArithmeticCircuit a] -> [ArithmeticCircuit a]
forall a. Semigroup a => a -> a -> a
<> [ArithmeticCircuit a] -> [ArithmeticCircuit a]
forall a. [a] -> [a]
Haskell.reverse ((ArithmeticCircuit a -> [ArithmeticCircuit a])
-> [ArithmeticCircuit a] -> [ArithmeticCircuit a]
forall (t :: Type -> Type) a b.
Foldable t =>
(a -> [b]) -> t a -> [b]
concatMap ArithmeticCircuit a -> [ArithmeticCircuit a]
forall a x. SymbolicData a x => x -> [ArithmeticCircuit a]
getBitsBE [ArithmeticCircuit a]
rs2))

    max :: UInt n (ArithmeticCircuit a)
-> UInt n (ArithmeticCircuit a) -> UInt n (ArithmeticCircuit a)
max UInt n (ArithmeticCircuit a)
x UInt n (ArithmeticCircuit a)
y = forall b a. Conditional b a => a -> a -> b -> a
bool @(Bool (ArithmeticCircuit a)) UInt n (ArithmeticCircuit a)
x UInt n (ArithmeticCircuit a)
y (Bool (ArithmeticCircuit a) -> UInt n (ArithmeticCircuit a))
-> Bool (ArithmeticCircuit a) -> UInt n (ArithmeticCircuit a)
forall a b. (a -> b) -> a -> b
$ UInt n (ArithmeticCircuit a)
x UInt n (ArithmeticCircuit a)
-> UInt n (ArithmeticCircuit a) -> Bool (ArithmeticCircuit a)
forall b a. Ord b a => a -> a -> b
< UInt n (ArithmeticCircuit a)
y

    min :: UInt n (ArithmeticCircuit a)
-> UInt n (ArithmeticCircuit a) -> UInt n (ArithmeticCircuit a)
min UInt n (ArithmeticCircuit a)
x UInt n (ArithmeticCircuit a)
y = forall b a. Conditional b a => a -> a -> b -> a
bool @(Bool (ArithmeticCircuit a)) UInt n (ArithmeticCircuit a)
x UInt n (ArithmeticCircuit a)
y (Bool (ArithmeticCircuit a) -> UInt n (ArithmeticCircuit a))
-> Bool (ArithmeticCircuit a) -> UInt n (ArithmeticCircuit a)
forall a b. (a -> b) -> a -> b
$ UInt n (ArithmeticCircuit a)
x UInt n (ArithmeticCircuit a)
-> UInt n (ArithmeticCircuit a) -> Bool (ArithmeticCircuit a)
forall b a. Ord b a => a -> a -> b
> UInt n (ArithmeticCircuit a)
y


instance (Arithmetic a, KnownNat n) => AdditiveSemigroup (UInt n (ArithmeticCircuit a)) where
    UInt [] ArithmeticCircuit a
x + :: UInt n (ArithmeticCircuit a)
-> UInt n (ArithmeticCircuit a) -> UInt n (ArithmeticCircuit a)
+ UInt [] ArithmeticCircuit a
y = [ArithmeticCircuit a]
-> ArithmeticCircuit a -> UInt n (ArithmeticCircuit a)
forall (n :: Natural) a. [a] -> a -> UInt n a
UInt [] (ArithmeticCircuit a -> UInt n (ArithmeticCircuit a))
-> ArithmeticCircuit a -> UInt n (ArithmeticCircuit a)
forall a b. (a -> b) -> a -> b
$ (forall i (m :: Type -> Type). MonadBlueprint i a m => m i)
-> ArithmeticCircuit a
forall a.
Arithmetic a =>
(forall i (m :: Type -> Type). MonadBlueprint i a m => m i)
-> ArithmeticCircuit a
circuit ((forall i (m :: Type -> Type). MonadBlueprint i a m => m i)
 -> ArithmeticCircuit a)
-> (forall i (m :: Type -> Type). MonadBlueprint i a m => m i)
-> ArithmeticCircuit a
forall a b. (a -> b) -> a -> b
$ do
        (i
z, i
_) <- ArithmeticCircuit a -> m i
forall i a (m :: Type -> Type).
MonadBlueprint i a m =>
ArithmeticCircuit a -> m i
runCircuit (ArithmeticCircuit a
x ArithmeticCircuit a -> ArithmeticCircuit a -> ArithmeticCircuit a
forall a. AdditiveSemigroup a => a -> a -> a
+ ArithmeticCircuit a
y) 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
>>= Natural -> Natural -> i -> m (i, i)
forall i a (m :: Type -> Type).
MonadBlueprint i a m =>
Natural -> Natural -> i -> m (i, i)
splitExpansion (forall a (n :: Natural). (Finite a, KnownNat n) => Natural
highRegisterSize @a @n) Natural
1
        i -> m i
forall a. a -> m a
forall (m :: Type -> Type) a. Monad m => a -> m a
return i
z

    UInt (ArithmeticCircuit a
x : [ArithmeticCircuit a]
xs) ArithmeticCircuit a
z + UInt (ArithmeticCircuit a
y : [ArithmeticCircuit a]
ys) ArithmeticCircuit a
w =
        let solve :: MonadBlueprint i a m => m [i]
            solve :: forall i (m :: Type -> Type). MonadBlueprint i a m => m [i]
solve = do
                (i
i, i
j) <- ArithmeticCircuit a -> m i
forall i a (m :: Type -> Type).
MonadBlueprint i a m =>
ArithmeticCircuit a -> m i
runCircuit (ArithmeticCircuit a
x ArithmeticCircuit a -> ArithmeticCircuit a -> ArithmeticCircuit a
forall a. AdditiveSemigroup a => a -> a -> a
+ ArithmeticCircuit a
y) 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
>>= Natural -> Natural -> i -> m (i, i)
forall i a (m :: Type -> Type).
MonadBlueprint i a m =>
Natural -> Natural -> i -> m (i, i)
splitExpansion (forall a (n :: Natural). (Finite a, KnownNat n) => Natural
registerSize @a @n) Natural
1
                ([i]
zs, i
c) <- (StateT i m [i] -> i -> m ([i], i))
-> i -> StateT i m [i] -> m ([i], i)
forall a b c. (a -> b -> c) -> b -> a -> c
flip StateT i m [i] -> i -> m ([i], i)
forall s (m :: Type -> Type) a. StateT s m a -> s -> m (a, s)
runStateT i
j (StateT i m [i] -> m ([i], i)) -> StateT i m [i] -> m ([i], i)
forall a b. (a -> b) -> a -> b
$ ((i -> m (i, i)) -> StateT i m i)
-> [i -> m (i, i)] -> StateT i m [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) -> [a] -> f [b]
traverse (i -> m (i, i)) -> StateT i m i
forall s (m :: Type -> Type) a. (s -> m (a, s)) -> StateT s m a
StateT ([i -> m (i, i)] -> StateT i m [i])
-> [i -> m (i, i)] -> StateT i m [i]
forall a b. (a -> b) -> a -> b
$
                    (ArithmeticCircuit a -> ArithmeticCircuit a -> i -> m (i, i))
-> [ArithmeticCircuit a]
-> [ArithmeticCircuit a]
-> [i -> m (i, i)]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (Natural
-> ArithmeticCircuit a -> ArithmeticCircuit a -> i -> m (i, i)
forall i a (m :: Type -> Type).
MonadBlueprint i a m =>
Natural
-> ArithmeticCircuit a -> ArithmeticCircuit a -> i -> m (i, i)
fullAdder (Natural
 -> ArithmeticCircuit a -> ArithmeticCircuit a -> i -> m (i, i))
-> Natural
-> ArithmeticCircuit a
-> ArithmeticCircuit a
-> i
-> m (i, i)
forall a b. (a -> b) -> a -> b
$ forall a (n :: Natural). (Finite a, KnownNat n) => Natural
registerSize @a @n) [ArithmeticCircuit a]
xs [ArithmeticCircuit a]
ys
                (i
k, i
_) <- Natural
-> ArithmeticCircuit a -> ArithmeticCircuit a -> i -> m (i, i)
forall i a (m :: Type -> Type).
MonadBlueprint i a m =>
Natural
-> ArithmeticCircuit a -> ArithmeticCircuit a -> i -> m (i, i)
fullAdder (forall a (n :: Natural). (Finite a, KnownNat n) => Natural
highRegisterSize @a @n) ArithmeticCircuit a
z ArithmeticCircuit a
w i
c
                [i] -> m [i]
forall a. a -> m a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (i
k i -> [i] -> [i]
forall a. a -> [a] -> [a]
: i
i i -> [i] -> [i]
forall a. a -> [a] -> [a]
: [i]
zs)

         in case (forall i (m :: Type -> Type). MonadBlueprint i a m => m [i])
-> [ArithmeticCircuit a]
forall a (f :: Type -> Type).
(Arithmetic a, Functor f) =>
(forall i (m :: Type -> Type). MonadBlueprint i a m => m (f i))
-> f (ArithmeticCircuit a)
circuits m [i]
forall i (m :: Type -> Type). MonadBlueprint i a m => m [i]
solve of
            (ArithmeticCircuit a
hi : [ArithmeticCircuit a]
lo) -> [ArithmeticCircuit a]
-> ArithmeticCircuit a -> UInt n (ArithmeticCircuit a)
forall (n :: Natural) a. [a] -> a -> UInt n a
UInt [ArithmeticCircuit a]
lo ArithmeticCircuit a
hi
            []        -> String -> UInt n (ArithmeticCircuit a)
forall a. HasCallStack => String -> a
error String
"UInt: unreachable"

    UInt [ArithmeticCircuit a]
_ ArithmeticCircuit a
_ + UInt [ArithmeticCircuit a]
_ ArithmeticCircuit a
_ = String -> UInt n (ArithmeticCircuit a)
forall a. HasCallStack => String -> a
error String
"UInt: unreachable"

instance (Arithmetic a, KnownNat n) => AdditiveMonoid (UInt n (ArithmeticCircuit a)) where
    zero :: UInt n (ArithmeticCircuit a)
zero = [ArithmeticCircuit a]
-> ArithmeticCircuit a -> UInt n (ArithmeticCircuit a)
forall (n :: Natural) a. [a] -> a -> UInt n a
UInt (Natural -> ArithmeticCircuit a -> [ArithmeticCircuit a]
forall a. Natural -> a -> [a]
replicate (forall a (n :: Natural). (Finite a, KnownNat n) => Natural
numberOfRegisters @a @n Natural -> Natural -> Natural
-! Natural
1) ArithmeticCircuit a
forall a. AdditiveMonoid a => a
zero) ArithmeticCircuit a
forall a. AdditiveMonoid a => a
zero

instance (Arithmetic a, KnownNat n) => AdditiveGroup (UInt n (ArithmeticCircuit a)) where
    UInt [] ArithmeticCircuit a
x - :: UInt n (ArithmeticCircuit a)
-> UInt n (ArithmeticCircuit a) -> UInt n (ArithmeticCircuit a)
- UInt [] ArithmeticCircuit a
y = [ArithmeticCircuit a]
-> ArithmeticCircuit a -> UInt n (ArithmeticCircuit a)
forall (n :: Natural) a. [a] -> a -> UInt n a
UInt [] (ArithmeticCircuit a -> UInt n (ArithmeticCircuit a))
-> ArithmeticCircuit a -> UInt n (ArithmeticCircuit a)
forall a b. (a -> b) -> a -> b
$ (forall i (m :: Type -> Type). MonadBlueprint i a m => m i)
-> ArithmeticCircuit a
forall a.
Arithmetic a =>
(forall i (m :: Type -> Type). MonadBlueprint i a m => m i)
-> ArithmeticCircuit a
circuit ((forall i (m :: Type -> Type). MonadBlueprint i a m => m i)
 -> ArithmeticCircuit a)
-> (forall i (m :: Type -> Type). MonadBlueprint i a m => m i)
-> ArithmeticCircuit a
forall a b. (a -> b) -> a -> b
$ do
        i
i <- ArithmeticCircuit a -> m i
forall i a (m :: Type -> Type).
MonadBlueprint i a m =>
ArithmeticCircuit a -> m i
runCircuit ArithmeticCircuit a
x
        i
j <- ArithmeticCircuit a -> m i
forall i a (m :: Type -> Type).
MonadBlueprint i a m =>
ArithmeticCircuit a -> m i
runCircuit ArithmeticCircuit a
y
        i
z0 <- ClosedPoly i a -> m i
forall i a (m :: Type -> Type).
MonadBlueprint i a m =>
ClosedPoly i a -> m i
newAssigned (\i -> x
v -> i -> x
v i
i x -> x -> x
forall a. AdditiveGroup a => a -> a -> a
- i -> x
v i
j x -> x -> x
forall a. AdditiveSemigroup a => a -> a -> a
+ Natural -> x
forall a b. FromConstant a b => a -> b
fromConstant (Natural
2 Natural -> Natural -> Natural
forall a b. Exponent a b => a -> b -> a
^ forall a (n :: Natural). (Finite a, KnownNat n) => Natural
registerSize @a @n :: Natural))
        (i
z, i
_) <- Natural -> Natural -> i -> m (i, i)
forall i a (m :: Type -> Type).
MonadBlueprint i a m =>
Natural -> Natural -> i -> m (i, i)
splitExpansion (forall a (n :: Natural). (Finite a, KnownNat n) => Natural
highRegisterSize @a @n) Natural
1 i
z0
        i -> m i
forall a. a -> m a
forall (m :: Type -> Type) a. Monad m => a -> m a
return i
z

    UInt (ArithmeticCircuit a
x : [ArithmeticCircuit a]
xs) ArithmeticCircuit a
z - UInt (ArithmeticCircuit a
y : [ArithmeticCircuit a]
ys) ArithmeticCircuit a
w =
        let t :: a
            t :: a
t = (a
forall a. MultiplicativeMonoid a => a
one a -> a -> a
forall a. AdditiveSemigroup a => a -> a -> a
+ a
forall a. MultiplicativeMonoid a => a
one) a -> Natural -> a
forall a b. Exponent a b => a -> b -> a
^ forall a (n :: Natural). (Finite a, KnownNat n) => Natural
registerSize @a @n a -> a -> a
forall a. AdditiveGroup a => a -> a -> a
- a
forall a. MultiplicativeMonoid a => a
one

            solve :: MonadBlueprint i a m => m [i]
            solve :: forall i (m :: Type -> Type). MonadBlueprint i a m => m [i]
solve = do
                i
i <- ArithmeticCircuit a -> m i
forall i a (m :: Type -> Type).
MonadBlueprint i a m =>
ArithmeticCircuit a -> m i
runCircuit ArithmeticCircuit a
x
                i
j <- ArithmeticCircuit a -> m i
forall i a (m :: Type -> Type).
MonadBlueprint i a m =>
ArithmeticCircuit a -> m i
runCircuit ArithmeticCircuit a
y
                i
s <- ClosedPoly i a -> m i
forall i a (m :: Type -> Type).
MonadBlueprint i a m =>
ClosedPoly i a -> m i
newAssigned (\i -> x
v -> i -> x
v i
i x -> x -> x
forall a. AdditiveGroup a => a -> a -> a
- i -> x
v i
j x -> x -> x
forall a. AdditiveSemigroup a => a -> a -> a
+ a -> x
forall a b. FromConstant a b => a -> b
fromConstant (a
t a -> a -> a
forall a. AdditiveSemigroup a => a -> a -> a
+ a
forall a. MultiplicativeMonoid a => a
one))
                (i
k, i
b0) <- Natural -> Natural -> i -> m (i, i)
forall i a (m :: Type -> Type).
MonadBlueprint i a m =>
Natural -> Natural -> i -> m (i, i)
splitExpansion (forall a (n :: Natural). (Finite a, KnownNat n) => Natural
registerSize @a @n) Natural
1 i
s
                ([i]
zs, i
b) <- (StateT i m [i] -> i -> m ([i], i))
-> i -> StateT i m [i] -> m ([i], i)
forall a b c. (a -> b -> c) -> b -> a -> c
flip StateT i m [i] -> i -> m ([i], i)
forall s (m :: Type -> Type) a. StateT s m a -> s -> m (a, s)
runStateT i
b0 (StateT i m [i] -> m ([i], i)) -> StateT i m [i] -> m ([i], i)
forall a b. (a -> b) -> a -> b
$ ((i -> m (i, i)) -> StateT i m i)
-> [i -> m (i, i)] -> StateT i m [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) -> [a] -> f [b]
traverse (i -> m (i, i)) -> StateT i m i
forall s (m :: Type -> Type) a. (s -> m (a, s)) -> StateT s m a
StateT ((ArithmeticCircuit a -> ArithmeticCircuit a -> i -> m (i, i))
-> [ArithmeticCircuit a]
-> [ArithmeticCircuit a]
-> [i -> m (i, i)]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith ArithmeticCircuit a -> ArithmeticCircuit a -> i -> m (i, i)
forall i (m :: Type -> Type).
MonadBlueprint i a m =>
ArithmeticCircuit a -> ArithmeticCircuit a -> i -> m (i, i)
fullSub [ArithmeticCircuit a]
xs [ArithmeticCircuit a]
ys)
                i
d <- ArithmeticCircuit a -> m i
forall i a (m :: Type -> Type).
MonadBlueprint i a m =>
ArithmeticCircuit a -> m i
runCircuit (ArithmeticCircuit a
z ArithmeticCircuit a -> ArithmeticCircuit a -> ArithmeticCircuit a
forall a. AdditiveGroup a => a -> a -> a
- ArithmeticCircuit a
w)
                i
s'0 <- ClosedPoly i a -> m i
forall i a (m :: Type -> Type).
MonadBlueprint i a m =>
ClosedPoly i a -> m i
newAssigned (\i -> x
v -> i -> x
v i
d x -> x -> x
forall a. AdditiveSemigroup a => a -> a -> a
+ i -> x
v i
b x -> x -> x
forall a. AdditiveSemigroup a => a -> a -> a
+ a -> x
forall a b. FromConstant a b => a -> b
fromConstant a
t)
                (i
s', i
_) <- Natural -> Natural -> i -> m (i, i)
forall i a (m :: Type -> Type).
MonadBlueprint i a m =>
Natural -> Natural -> i -> m (i, i)
splitExpansion (forall a (n :: Natural). (Finite a, KnownNat n) => Natural
highRegisterSize @a @n) Natural
1 i
s'0
                [i] -> m [i]
forall a. a -> m a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (i
s' i -> [i] -> [i]
forall a. a -> [a] -> [a]
: i
k i -> [i] -> [i]
forall a. a -> [a] -> [a]
: [i]
zs)

            fullSub :: MonadBlueprint i a m => ArithmeticCircuit a -> ArithmeticCircuit a -> i -> m (i, i)
            fullSub :: forall i (m :: Type -> Type).
MonadBlueprint i a m =>
ArithmeticCircuit a -> ArithmeticCircuit a -> i -> m (i, i)
fullSub ArithmeticCircuit a
xk ArithmeticCircuit a
yk i
b = do
                i
d <- ArithmeticCircuit a -> m i
forall i a (m :: Type -> Type).
MonadBlueprint i a m =>
ArithmeticCircuit a -> m i
runCircuit (ArithmeticCircuit a
xk ArithmeticCircuit a -> ArithmeticCircuit a -> ArithmeticCircuit a
forall a. AdditiveGroup a => a -> a -> a
- ArithmeticCircuit a
yk)
                i
s <- ClosedPoly i a -> m i
forall i a (m :: Type -> Type).
MonadBlueprint i a m =>
ClosedPoly i a -> m i
newAssigned (\i -> x
v -> i -> x
v i
d x -> x -> x
forall a. AdditiveSemigroup a => a -> a -> a
+ i -> x
v i
b x -> x -> x
forall a. AdditiveSemigroup a => a -> a -> a
+ a -> x
forall a b. FromConstant a b => a -> b
fromConstant a
t)
                Natural -> Natural -> i -> m (i, i)
forall i a (m :: Type -> Type).
MonadBlueprint i a m =>
Natural -> Natural -> i -> m (i, i)
splitExpansion (forall a (n :: Natural). (Finite a, KnownNat n) => Natural
registerSize @a @n) Natural
1 i
s

         in case (forall i (m :: Type -> Type). MonadBlueprint i a m => m [i])
-> [ArithmeticCircuit a]
forall a (f :: Type -> Type).
(Arithmetic a, Functor f) =>
(forall i (m :: Type -> Type). MonadBlueprint i a m => m (f i))
-> f (ArithmeticCircuit a)
circuits m [i]
forall i (m :: Type -> Type). MonadBlueprint i a m => m [i]
solve of
            (ArithmeticCircuit a
hi : [ArithmeticCircuit a]
lo) -> [ArithmeticCircuit a]
-> ArithmeticCircuit a -> UInt n (ArithmeticCircuit a)
forall (n :: Natural) a. [a] -> a -> UInt n a
UInt [ArithmeticCircuit a]
lo ArithmeticCircuit a
hi
            []        -> String -> UInt n (ArithmeticCircuit a)
forall a. HasCallStack => String -> a
error String
"UInt: unreachable"

    UInt [ArithmeticCircuit a]
_ ArithmeticCircuit a
_ - UInt [ArithmeticCircuit a]
_ ArithmeticCircuit a
_ = String -> UInt n (ArithmeticCircuit a)
forall a. HasCallStack => String -> a
error String
"UInt: unreachable"

    negate :: UInt n (ArithmeticCircuit a) -> UInt n (ArithmeticCircuit a)
negate UInt n (ArithmeticCircuit a)
uint = forall b a. Conditional b a => a -> a -> b -> a
bool @(Bool (ArithmeticCircuit a)) (UInt n (ArithmeticCircuit a) -> UInt n (ArithmeticCircuit a)
negate' UInt n (ArithmeticCircuit a)
uint) UInt n (ArithmeticCircuit a)
forall a. AdditiveMonoid a => a
zero (UInt n (ArithmeticCircuit a)
uint UInt n (ArithmeticCircuit a)
-> UInt n (ArithmeticCircuit a) -> Bool (ArithmeticCircuit a)
forall b a. Eq b a => a -> a -> b
== UInt n (ArithmeticCircuit a)
forall a. AdditiveMonoid a => a
zero)
        where
            negate' :: UInt n (ArithmeticCircuit a) -> UInt n (ArithmeticCircuit a)
negate' (UInt [] ArithmeticCircuit a
x) = [ArithmeticCircuit a]
-> ArithmeticCircuit a -> UInt n (ArithmeticCircuit a)
forall (n :: Natural) a. [a] -> a -> UInt n a
UInt [] (Natural -> ArithmeticCircuit a -> ArithmeticCircuit a
forall a.
Arithmetic a =>
Natural -> ArithmeticCircuit a -> ArithmeticCircuit a
negateN (Natural
2 Natural -> Natural -> Natural
forall a b. Exponent a b => a -> b -> a
^ forall a (n :: Natural). (Finite a, KnownNat n) => Natural
highRegisterSize @a @n) ArithmeticCircuit a
x)
            negate' (UInt (ArithmeticCircuit a
x : [ArithmeticCircuit a]
xs) ArithmeticCircuit a
x') =
                let y :: ArithmeticCircuit a
y = Natural -> ArithmeticCircuit a -> ArithmeticCircuit a
forall a.
Arithmetic a =>
Natural -> ArithmeticCircuit a -> ArithmeticCircuit a
negateN (Natural
2 Natural -> Natural -> Natural
forall a b. Exponent a b => a -> b -> a
^ forall a (n :: Natural). (Finite a, KnownNat n) => Natural
registerSize @a @n) ArithmeticCircuit a
x
                    ys :: [ArithmeticCircuit a]
ys = (ArithmeticCircuit a -> ArithmeticCircuit a)
-> [ArithmeticCircuit a] -> [ArithmeticCircuit a]
forall a b. (a -> b) -> [a] -> [b]
map (Natural -> ArithmeticCircuit a -> ArithmeticCircuit a
forall a.
Arithmetic a =>
Natural -> ArithmeticCircuit a -> ArithmeticCircuit a
negateN (Natural -> ArithmeticCircuit a -> ArithmeticCircuit a)
-> Natural -> ArithmeticCircuit a -> ArithmeticCircuit a
forall a b. (a -> b) -> a -> b
$ Natural
2 Natural -> Natural -> Natural
forall a b. Exponent a b => a -> b -> a
^ forall a (n :: Natural). (Finite a, KnownNat n) => Natural
registerSize @a @n Natural -> Natural -> Natural
-! Natural
1) [ArithmeticCircuit a]
xs
                    y' :: ArithmeticCircuit a
y' = Natural -> ArithmeticCircuit a -> ArithmeticCircuit a
forall a.
Arithmetic a =>
Natural -> ArithmeticCircuit a -> ArithmeticCircuit a
negateN (Natural
2 Natural -> Natural -> Natural
forall a b. Exponent a b => a -> b -> a
^ forall a (n :: Natural). (Finite a, KnownNat n) => Natural
highRegisterSize @a @n Natural -> Natural -> Natural
-! Natural
1) ArithmeticCircuit a
x'
                 in [ArithmeticCircuit a]
-> ArithmeticCircuit a -> UInt n (ArithmeticCircuit a)
forall (n :: Natural) a. [a] -> a -> UInt n a
UInt (ArithmeticCircuit a
y ArithmeticCircuit a
-> [ArithmeticCircuit a] -> [ArithmeticCircuit a]
forall a. a -> [a] -> [a]
: [ArithmeticCircuit a]
ys) ArithmeticCircuit a
y'

negateN :: Arithmetic a => Natural -> ArithmeticCircuit a -> ArithmeticCircuit a
negateN :: forall a.
Arithmetic a =>
Natural -> ArithmeticCircuit a -> ArithmeticCircuit a
negateN Natural
n ArithmeticCircuit a
r = (forall i (m :: Type -> Type). MonadBlueprint i a m => m i)
-> ArithmeticCircuit a
forall a.
Arithmetic a =>
(forall i (m :: Type -> Type). MonadBlueprint i a m => m i)
-> ArithmeticCircuit a
circuit ((forall i (m :: Type -> Type). MonadBlueprint i a m => m i)
 -> ArithmeticCircuit a)
-> (forall i (m :: Type -> Type). MonadBlueprint i a m => m i)
-> ArithmeticCircuit a
forall a b. (a -> b) -> a -> b
$ do
    i
i <- ArithmeticCircuit a -> m i
forall i a (m :: Type -> Type).
MonadBlueprint i a m =>
ArithmeticCircuit a -> m i
runCircuit ArithmeticCircuit a
r
    ClosedPoly i a -> m i
forall i a (m :: Type -> Type).
MonadBlueprint i a m =>
ClosedPoly i a -> m i
newAssigned (\i -> x
v -> Natural -> x
forall a b. FromConstant a b => a -> b
fromConstant Natural
n x -> x -> x
forall a. AdditiveGroup a => a -> a -> a
- i -> x
v i
i)

instance (Arithmetic a, KnownNat n) => MultiplicativeSemigroup (UInt n (ArithmeticCircuit a)) where
    UInt [] ArithmeticCircuit a
x * :: UInt n (ArithmeticCircuit a)
-> UInt n (ArithmeticCircuit a) -> UInt n (ArithmeticCircuit a)
* UInt [] ArithmeticCircuit a
y = [ArithmeticCircuit a]
-> ArithmeticCircuit a -> UInt n (ArithmeticCircuit a)
forall (n :: Natural) a. [a] -> a -> UInt n a
UInt [] (ArithmeticCircuit a -> UInt n (ArithmeticCircuit a))
-> ArithmeticCircuit a -> UInt n (ArithmeticCircuit a)
forall a b. (a -> b) -> a -> b
$ (forall i (m :: Type -> Type). MonadBlueprint i a m => m i)
-> ArithmeticCircuit a
forall a.
Arithmetic a =>
(forall i (m :: Type -> Type). MonadBlueprint i a m => m i)
-> ArithmeticCircuit a
circuit ((forall i (m :: Type -> Type). MonadBlueprint i a m => m i)
 -> ArithmeticCircuit a)
-> (forall i (m :: Type -> Type). MonadBlueprint i a m => m i)
-> ArithmeticCircuit a
forall a b. (a -> b) -> a -> b
$ do
        (i
z, i
_) <- ArithmeticCircuit a -> m i
forall i a (m :: Type -> Type).
MonadBlueprint i a m =>
ArithmeticCircuit a -> m i
runCircuit (ArithmeticCircuit a
x ArithmeticCircuit a -> ArithmeticCircuit a -> ArithmeticCircuit a
forall a. MultiplicativeSemigroup a => a -> a -> a
* ArithmeticCircuit a
y) 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
>>= Natural -> Natural -> i -> m (i, i)
forall i a (m :: Type -> Type).
MonadBlueprint i a m =>
Natural -> Natural -> i -> m (i, i)
splitExpansion (forall a (n :: Natural). (Finite a, KnownNat n) => Natural
highRegisterSize @a @n) (forall a (n :: Natural). (Finite a, KnownNat n) => Natural
maxOverflow @a @n)
        i -> m i
forall a. a -> m a
forall (m :: Type -> Type) a. Monad m => a -> m a
return i
z

    UInt (ArithmeticCircuit a
x : [ArithmeticCircuit a]
xs) ArithmeticCircuit a
z * UInt (ArithmeticCircuit a
y : [ArithmeticCircuit a]
ys) ArithmeticCircuit a
w =
        let solve :: MonadBlueprint i a m => m [i]
            solve :: forall i (m :: Type -> Type). MonadBlueprint i a m => m [i]
solve = do
                i
i <- ArithmeticCircuit a -> m i
forall i a (m :: Type -> Type).
MonadBlueprint i a m =>
ArithmeticCircuit a -> m i
runCircuit ArithmeticCircuit a
x
                i
j <- ArithmeticCircuit a -> m i
forall i a (m :: Type -> Type).
MonadBlueprint i a m =>
ArithmeticCircuit a -> m i
runCircuit ArithmeticCircuit a
y
                [i]
is <- [ArithmeticCircuit a] -> (ArithmeticCircuit a -> m i) -> m [i]
forall (t :: Type -> Type) (f :: Type -> Type) a b.
(Traversable t, Applicative f) =>
t a -> (a -> f b) -> f (t b)
for [ArithmeticCircuit a]
xs ArithmeticCircuit a -> m i
forall i a (m :: Type -> Type).
MonadBlueprint i a m =>
ArithmeticCircuit a -> m i
runCircuit
                [i]
js <- [ArithmeticCircuit a] -> (ArithmeticCircuit a -> m i) -> m [i]
forall (t :: Type -> Type) (f :: Type -> Type) a b.
(Traversable t, Applicative f) =>
t a -> (a -> f b) -> f (t b)
for [ArithmeticCircuit a]
ys ArithmeticCircuit a -> m i
forall i a (m :: Type -> Type).
MonadBlueprint i a m =>
ArithmeticCircuit a -> m i
runCircuit
                i
i' <- ArithmeticCircuit a -> m i
forall i a (m :: Type -> Type).
MonadBlueprint i a m =>
ArithmeticCircuit a -> m i
runCircuit ArithmeticCircuit a
z
                i
j' <- ArithmeticCircuit a -> m i
forall i a (m :: Type -> Type).
MonadBlueprint i a m =>
ArithmeticCircuit a -> m i
runCircuit ArithmeticCircuit a
w
                let cs :: Map Natural i
cs = [(Natural, i)] -> Map Natural i
forall k a. Ord k => [(k, a)] -> Map k a
fromList ([(Natural, i)] -> Map Natural i)
-> [(Natural, i)] -> Map Natural i
forall a b. (a -> b) -> a -> b
$ [Natural] -> [i] -> [(Natural, i)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Natural
0..] (i
i i -> [i] -> [i]
forall a. a -> [a] -> [a]
: [i]
is [i] -> [i] -> [i]
forall a. [a] -> [a] -> [a]
++ [i
i'])
                    ds :: Map Natural i
ds = [(Natural, i)] -> Map Natural i
forall k a. Ord k => [(k, a)] -> Map k a
fromList ([(Natural, i)] -> Map Natural i)
-> [(Natural, i)] -> Map Natural i
forall a b. (a -> b) -> a -> b
$ [Natural] -> [i] -> [(Natural, i)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Natural
0..] (i
j i -> [i] -> [i]
forall a. a -> [a] -> [a]
: [i]
js [i] -> [i] -> [i]
forall a. [a] -> [a] -> [a]
++ [i
j'])
                    r :: Natural
r  = forall a (n :: Natural). (Finite a, KnownNat n) => Natural
numberOfRegisters @a @n
                -- single addend for lower register
                i
q <- ClosedPoly i a -> m i
forall i a (m :: Type -> Type).
MonadBlueprint i a m =>
ClosedPoly i a -> m i
newAssigned (\i -> x
v -> i -> x
v i
i x -> x -> x
forall a. MultiplicativeSemigroup a => a -> a -> a
* i -> x
v i
j)
                -- multiple addends for middle registers
                [[i]]
qs <- [Natural] -> (Natural -> m [i]) -> m [[i]]
forall (t :: Type -> Type) (f :: Type -> Type) a b.
(Traversable t, Applicative f) =>
t a -> (a -> f b) -> f (t b)
for [Natural
1 .. Natural
r Natural -> Natural -> Natural
-! Natural
2] ((Natural -> m [i]) -> m [[i]]) -> (Natural -> m [i]) -> m [[i]]
forall a b. (a -> b) -> a -> b
$ \Natural
k ->
                    [Natural] -> (Natural -> m i) -> m [i]
forall (t :: Type -> Type) (f :: Type -> Type) a b.
(Traversable t, Applicative f) =>
t a -> (a -> f b) -> f (t b)
for [Natural
0 .. Natural
k] ((Natural -> m i) -> m [i]) -> (Natural -> m i) -> m [i]
forall a b. (a -> b) -> a -> b
$ \Natural
l ->
                        ClosedPoly i a -> m i
forall i a (m :: Type -> Type).
MonadBlueprint i a m =>
ClosedPoly i a -> m i
newAssigned (\i -> x
v -> i -> x
v (Map Natural i
cs Map Natural i -> Natural -> i
forall k a. Ord k => Map k a -> k -> a
! Natural
l) x -> x -> x
forall a. MultiplicativeSemigroup a => a -> a -> a
* i -> x
v (Map Natural i
ds Map Natural i -> Natural -> i
forall k a. Ord k => Map k a -> k -> a
! (Natural
k Natural -> Natural -> Natural
-! Natural
l)))
                -- lower register
                (i
p, i
c) <- Natural -> Natural -> i -> m (i, i)
forall i a (m :: Type -> Type).
MonadBlueprint i a m =>
Natural -> Natural -> i -> m (i, i)
splitExpansion (forall a (n :: Natural). (Finite a, KnownNat n) => Natural
registerSize @a @n) (forall a (n :: Natural). (Finite a, KnownNat n) => Natural
registerSize @a @n) i
q
                -- middle registers
                ([i]
ps, i
c') <- (StateT i m [i] -> i -> m ([i], i))
-> i -> StateT i m [i] -> m ([i], i)
forall a b c. (a -> b -> c) -> b -> a -> c
flip StateT i m [i] -> i -> m ([i], i)
forall s (m :: Type -> Type) a. StateT s m a -> s -> m (a, s)
runStateT i
c (StateT i m [i] -> m ([i], i)) -> StateT i m [i] -> m ([i], i)
forall a b. (a -> b) -> a -> b
$ [[i]] -> ([i] -> StateT i m i) -> StateT i m [i]
forall (t :: Type -> Type) (f :: Type -> Type) a b.
(Traversable t, Applicative f) =>
t a -> (a -> f b) -> f (t b)
for [[i]]
qs (([i] -> StateT i m i) -> StateT i m [i])
-> ([i] -> StateT i m i) -> StateT i m [i]
forall a b. (a -> b) -> a -> b
$ (i -> m (i, i)) -> StateT i m i
forall s (m :: Type -> Type) a. (s -> m (a, s)) -> StateT s m a
StateT ((i -> m (i, i)) -> StateT i m i)
-> ([i] -> i -> m (i, i)) -> [i] -> StateT i m i
forall b c a. (b -> c) -> (a -> b) -> a -> c
. \[i]
rs i
c' -> do
                    i
s <- (i -> i -> m i) -> i -> [i] -> m i
forall (t :: Type -> Type) (m :: Type -> Type) a b.
(Foldable t, Monad m) =>
(a -> b -> m b) -> b -> t a -> m b
foldrM (\i
k i
l -> ClosedPoly i a -> m i
forall i a (m :: Type -> Type).
MonadBlueprint i a m =>
ClosedPoly i a -> m i
newAssigned (\i -> x
v -> i -> x
v i
k x -> x -> x
forall a. AdditiveSemigroup a => a -> a -> a
+ i -> x
v i
l)) i
c' [i]
rs
                    Natural -> Natural -> i -> m (i, i)
forall i a (m :: Type -> Type).
MonadBlueprint i a m =>
Natural -> Natural -> i -> m (i, i)
splitExpansion (forall a (n :: Natural). (Finite a, KnownNat n) => Natural
registerSize @a @n) (forall a (n :: Natural). (Finite a, KnownNat n) => Natural
maxOverflow @a @n) i
s
                -- high register
                i
p'0 <- (Natural -> i -> m i) -> i -> [Natural] -> m i
forall (t :: Type -> Type) (m :: Type -> Type) a b.
(Foldable t, Monad m) =>
(a -> b -> m b) -> b -> t a -> m b
foldrM (\Natural
k i
l -> do
                    i
k' <- ClosedPoly i a -> m i
forall i a (m :: Type -> Type).
MonadBlueprint i a m =>
ClosedPoly i a -> m i
newAssigned (\i -> x
v -> i -> x
v (Map Natural i
cs Map Natural i -> Natural -> i
forall k a. Ord k => Map k a -> k -> a
! Natural
k) x -> x -> x
forall a. MultiplicativeSemigroup a => a -> a -> a
* i -> x
v (Map Natural i
ds Map Natural i -> Natural -> i
forall k a. Ord k => Map k a -> k -> a
! (Natural
r Natural -> Natural -> Natural
-! (Natural
k Natural -> Natural -> Natural
forall a. AdditiveSemigroup a => a -> a -> a
+ Natural
1))))
                    ClosedPoly i a -> m i
forall i a (m :: Type -> Type).
MonadBlueprint i a m =>
ClosedPoly i a -> m i
newAssigned (\i -> x
v -> i -> x
v i
k' x -> x -> x
forall a. AdditiveSemigroup a => a -> a -> a
+ i -> x
v i
l)) i
c' [Natural
0 .. Natural
r Natural -> Natural -> Natural
-! Natural
1]
                (i
p', i
_) <- Natural -> Natural -> i -> m (i, i)
forall i a (m :: Type -> Type).
MonadBlueprint i a m =>
Natural -> Natural -> i -> m (i, i)
splitExpansion (forall a (n :: Natural). (Finite a, KnownNat n) => Natural
highRegisterSize @a @n) (forall a (n :: Natural). (Finite a, KnownNat n) => Natural
maxOverflow @a @n) i
p'0
                [i] -> m [i]
forall a. a -> m a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (i
p' i -> [i] -> [i]
forall a. a -> [a] -> [a]
: i
p i -> [i] -> [i]
forall a. a -> [a] -> [a]
: [i]
ps)

         in case (forall i (m :: Type -> Type). MonadBlueprint i a m => m [i])
-> [ArithmeticCircuit a]
forall a (f :: Type -> Type).
(Arithmetic a, Functor f) =>
(forall i (m :: Type -> Type). MonadBlueprint i a m => m (f i))
-> f (ArithmeticCircuit a)
circuits m [i]
forall i (m :: Type -> Type). MonadBlueprint i a m => m [i]
solve of
            (ArithmeticCircuit a
hi : [ArithmeticCircuit a]
lo) -> [ArithmeticCircuit a]
-> ArithmeticCircuit a -> UInt n (ArithmeticCircuit a)
forall (n :: Natural) a. [a] -> a -> UInt n a
UInt [ArithmeticCircuit a]
lo ArithmeticCircuit a
hi
            []        -> String -> UInt n (ArithmeticCircuit a)
forall a. HasCallStack => String -> a
error String
"UInt: unreachable"

    UInt [ArithmeticCircuit a]
_ ArithmeticCircuit a
_ * UInt [ArithmeticCircuit a]
_ ArithmeticCircuit a
_ = String -> UInt n (ArithmeticCircuit a)
forall a. HasCallStack => String -> a
error String
"UInt: unreachable"

instance (Arithmetic a, KnownNat n) => MultiplicativeMonoid (UInt n (ArithmeticCircuit a)) where
    one :: UInt n (ArithmeticCircuit a)
one | forall a (n :: Natural). (Finite a, KnownNat n) => Natural
numberOfRegisters @a @n Natural -> Natural -> Bool
forall a. Eq a => a -> a -> Bool
Haskell.== Natural
1 = [ArithmeticCircuit a]
-> ArithmeticCircuit a -> UInt n (ArithmeticCircuit a)
forall (n :: Natural) a. [a] -> a -> UInt n a
UInt [] ArithmeticCircuit a
forall a. MultiplicativeMonoid a => a
one
        | Bool
otherwise = [ArithmeticCircuit a]
-> ArithmeticCircuit a -> UInt n (ArithmeticCircuit a)
forall (n :: Natural) a. [a] -> a -> UInt n a
UInt (ArithmeticCircuit a
forall a. MultiplicativeMonoid a => a
one ArithmeticCircuit a
-> [ArithmeticCircuit a] -> [ArithmeticCircuit a]
forall a. a -> [a] -> [a]
: Natural -> ArithmeticCircuit a -> [ArithmeticCircuit a]
forall a. Natural -> a -> [a]
replicate (forall a (n :: Natural). (Finite a, KnownNat n) => Natural
numberOfRegisters @a @n Natural -> Natural -> Natural
-! Natural
2) ArithmeticCircuit a
forall a. AdditiveMonoid a => a
zero) ArithmeticCircuit a
forall a. AdditiveMonoid a => a
zero

instance (Arithmetic a, KnownNat n) => Semiring (UInt n (ArithmeticCircuit a))

instance (Arithmetic a, KnownNat n) => Ring (UInt n (ArithmeticCircuit a))

deriving via (Structural (UInt n (ArithmeticCircuit a)))
         instance (Arithmetic a, KnownNat n) =>
         Eq (Bool (ArithmeticCircuit a)) (UInt n (ArithmeticCircuit a))

instance (Arithmetic a, KnownNat n) => Arbitrary (UInt n (ArithmeticCircuit a)) where
    arbitrary :: Gen (UInt n (ArithmeticCircuit a))
arbitrary = [ArithmeticCircuit a]
-> ArithmeticCircuit a -> UInt n (ArithmeticCircuit a)
forall (n :: Natural) a. [a] -> a -> UInt n a
UInt
        ([ArithmeticCircuit a]
 -> ArithmeticCircuit a -> UInt n (ArithmeticCircuit a))
-> Gen [ArithmeticCircuit a]
-> Gen (ArithmeticCircuit a -> UInt n (ArithmeticCircuit a))
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Natural -> Gen (ArithmeticCircuit a) -> Gen [ArithmeticCircuit a]
forall (f :: Type -> Type) a.
Applicative f =>
Natural -> f a -> f [a]
replicateA (forall a (n :: Natural). (Finite a, KnownNat n) => Natural
numberOfRegisters @a @n Natural -> Natural -> Natural
-! Natural
1) (Natural -> Gen (ArithmeticCircuit a)
forall {b} {b}.
(FromConstant Integer b, Exponent Integer b) =>
b -> Gen b
toss (Natural -> Gen (ArithmeticCircuit a))
-> Natural -> Gen (ArithmeticCircuit a)
forall a b. (a -> b) -> a -> b
$ forall a (n :: Natural). (Finite a, KnownNat n) => Natural
registerSize @a @n)
        Gen (ArithmeticCircuit a -> UInt n (ArithmeticCircuit a))
-> Gen (ArithmeticCircuit a) -> Gen (UInt n (ArithmeticCircuit a))
forall a b. Gen (a -> b) -> Gen a -> Gen b
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> Natural -> Gen (ArithmeticCircuit a)
forall {b} {b}.
(FromConstant Integer b, Exponent Integer b) =>
b -> Gen b
toss (forall a (n :: Natural). (Finite a, KnownNat n) => Natural
highRegisterSize @a @n)
        where toss :: b -> Gen b
toss b
b = Integer -> b
forall a b. FromConstant a b => a -> b
fromConstant (Integer -> b) -> Gen Integer -> Gen b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> (Integer, Integer) -> Gen Integer
chooseInteger (Integer
0, Integer
2 Integer -> b -> Integer
forall a b. Exponent a b => a -> b -> a
^ b
b Integer -> Integer -> Integer
forall a. AdditiveGroup a => a -> a -> a
- Integer
1)

--------------------------------------------------------------------------------

class StrictConv b a where
    strictConv :: b -> a

instance (FromConstant Natural a, Finite a, AdditiveMonoid a, KnownNat n) => StrictConv Natural (UInt n a) where
    strictConv :: Natural -> UInt n a
strictConv Natural
n = case forall a (n :: Natural).
(FromConstant Natural a, Finite a, AdditiveMonoid a, KnownNat n) =>
Natural -> (UInt n a, [a])
cast @a @n Natural
n of
        (UInt n a
x, []) -> UInt n a
x
        (UInt n a
_, [a]
_)  -> String -> UInt n a
forall a. HasCallStack => String -> a
error String
"strictConv: overflow"

instance (Finite (Zp p), KnownNat n) => StrictConv (Zp p) (UInt n (Zp p)) where
    strictConv :: Zp p -> UInt n (Zp p)
strictConv = Natural -> UInt n (Zp p)
forall b a. StrictConv b a => b -> a
strictConv (Natural -> UInt n (Zp p))
-> (Zp p -> Natural) -> Zp p -> UInt n (Zp p)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. ToConstant a b => a -> b
toConstant @_ @Natural

instance (Arithmetic a, KnownNat n, KnownNat (NumberOfBits a), NumberOfBits a <= n) => StrictConv (ArithmeticCircuit a) (UInt n (ArithmeticCircuit a)) where
    strictConv :: ArithmeticCircuit a -> UInt n (ArithmeticCircuit a)
strictConv ArithmeticCircuit a
a =
        let ([ArithmeticCircuit a]
lo, ArithmeticCircuit a
hi) = [ArithmeticCircuit a]
-> ([ArithmeticCircuit a], ArithmeticCircuit a)
forall {a}. [a] -> ([a], a)
unsnoc ([ArithmeticCircuit a]
 -> ([ArithmeticCircuit a], ArithmeticCircuit a))
-> [ArithmeticCircuit a]
-> ([ArithmeticCircuit a], ArithmeticCircuit a)
forall a b. (a -> b) -> a -> b
$ Natural -> [ArithmeticCircuit a] -> [ArithmeticCircuit a]
forall a. Natural -> [a] -> [a]
take (forall a (n :: Natural). (Finite a, KnownNat n) => Natural
numberOfRegisters @a @n) ([ArithmeticCircuit a] -> [ArithmeticCircuit a])
-> [ArithmeticCircuit a] -> [ArithmeticCircuit a]
forall a b. (a -> b) -> a -> b
$
                            ((ArithmeticCircuit a
  -> Maybe (ArithmeticCircuit a, ArithmeticCircuit a))
 -> ArithmeticCircuit a -> [ArithmeticCircuit a])
-> ArithmeticCircuit a
-> (ArithmeticCircuit a
    -> Maybe (ArithmeticCircuit a, ArithmeticCircuit a))
-> [ArithmeticCircuit a]
forall a b c. (a -> b -> c) -> b -> a -> c
flip (ArithmeticCircuit a
 -> Maybe (ArithmeticCircuit a, ArithmeticCircuit a))
-> ArithmeticCircuit a -> [ArithmeticCircuit a]
forall b a. (b -> Maybe (a, b)) -> b -> [a]
unfoldr ArithmeticCircuit a
a ((ArithmeticCircuit a
  -> Maybe (ArithmeticCircuit a, ArithmeticCircuit a))
 -> [ArithmeticCircuit a])
-> (ArithmeticCircuit a
    -> Maybe (ArithmeticCircuit a, ArithmeticCircuit a))
-> [ArithmeticCircuit a]
forall a b. (a -> b) -> a -> b
$ (ArithmeticCircuit a, ArithmeticCircuit a)
-> Maybe (ArithmeticCircuit a, ArithmeticCircuit a)
forall a. a -> Maybe a
Haskell.Just ((ArithmeticCircuit a, ArithmeticCircuit a)
 -> Maybe (ArithmeticCircuit a, ArithmeticCircuit a))
-> (ArithmeticCircuit a
    -> (ArithmeticCircuit a, ArithmeticCircuit a))
-> ArithmeticCircuit a
-> Maybe (ArithmeticCircuit a, ArithmeticCircuit a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ArithmeticCircuit a -> (ArithmeticCircuit a, ArithmeticCircuit a)
expand
         in [ArithmeticCircuit a]
-> ArithmeticCircuit a -> UInt n (ArithmeticCircuit a)
forall (n :: Natural) a. [a] -> a -> UInt n a
UInt [ArithmeticCircuit a]
lo ArithmeticCircuit a
hi
        where
            unsnoc :: [a] -> ([a], a)
unsnoc []       = String -> ([a], a)
forall a. HasCallStack => String -> a
error String
"unsnoc: empty list"
            unsnoc [a
x]      = ([], a
x)
            unsnoc (a
x : [a]
xs) = let ([a]
ys, a
z) = [a] -> ([a], a)
unsnoc [a]
xs in (a
x a -> [a] -> [a]
forall a. a -> [a] -> [a]
: [a]
ys, a
z)

            bitSize :: Natural
bitSize = forall a. KnownNat (NumberOfBits a) => Natural
numberOfBits @a
            regSize :: Natural
regSize = forall a (n :: Natural). (Finite a, KnownNat n) => Natural
registerSize @a @n

            expand :: ArithmeticCircuit a -> (ArithmeticCircuit a, ArithmeticCircuit a)
            expand :: ArithmeticCircuit a -> (ArithmeticCircuit a, ArithmeticCircuit a)
expand ArithmeticCircuit a
x = case (forall i (m :: Type -> Type). MonadBlueprint i a m => m [i])
-> [ArithmeticCircuit a]
forall a (f :: Type -> Type).
(Arithmetic a, Functor f) =>
(forall i (m :: Type -> Type). MonadBlueprint i a m => m (f i))
-> f (ArithmeticCircuit a)
circuits ((forall i (m :: Type -> Type). MonadBlueprint i a m => m [i])
 -> [ArithmeticCircuit a])
-> (forall i (m :: Type -> Type). MonadBlueprint i a m => m [i])
-> [ArithmeticCircuit a]
forall a b. (a -> b) -> a -> b
$ do
                i
i <- ArithmeticCircuit a -> m i
forall i a (m :: Type -> Type).
MonadBlueprint i a m =>
ArithmeticCircuit a -> m i
runCircuit ArithmeticCircuit a
x
                (i
j, i
k) <- Natural -> Natural -> i -> m (i, i)
forall i a (m :: Type -> Type).
MonadBlueprint i a m =>
Natural -> Natural -> i -> m (i, i)
splitExpansion Natural
regSize (Natural
bitSize Natural -> Natural -> Natural
-! Natural
regSize) i
i
                [i] -> m [i]
forall a. a -> m a
forall (m :: Type -> Type) a. Monad m => a -> m a
return [i
j, i
k]
              of
                [ArithmeticCircuit a
y, ArithmeticCircuit a
z] -> (ArithmeticCircuit a
y, ArithmeticCircuit a
z)
                [ArithmeticCircuit a]
_      -> String -> (ArithmeticCircuit a, ArithmeticCircuit a)
forall a. HasCallStack => String -> a
error String
"expand: impossible"


class StrictNum a where
    strictAdd :: a -> a -> a
    strictSub :: a -> a -> a
    strictMul :: a -> a -> a

instance (Finite (Zp p), KnownNat n) => StrictNum (UInt n (Zp p)) where
    strictAdd :: UInt n (Zp p) -> UInt n (Zp p) -> UInt n (Zp p)
strictAdd UInt n (Zp p)
x UInt n (Zp p)
y = Natural -> UInt n (Zp p)
forall b a. StrictConv b a => b -> a
strictConv (Natural -> UInt n (Zp p)) -> Natural -> UInt n (Zp p)
forall a b. (a -> b) -> a -> b
$ UInt n (Zp p) -> Natural
forall a b. ToConstant a b => a -> b
toConstant UInt n (Zp p)
x Natural -> Natural -> Natural
forall a. AdditiveSemigroup a => a -> a -> a
+ forall a b. ToConstant a b => a -> b
toConstant @_ @Natural UInt n (Zp p)
y
    strictSub :: UInt n (Zp p) -> UInt n (Zp p) -> UInt n (Zp p)
strictSub UInt n (Zp p)
x UInt n (Zp p)
y = Natural -> UInt n (Zp p)
forall b a. StrictConv b a => b -> a
strictConv (Natural -> UInt n (Zp p)) -> Natural -> UInt n (Zp p)
forall a b. (a -> b) -> a -> b
$ UInt n (Zp p) -> Natural
forall a b. ToConstant a b => a -> b
toConstant UInt n (Zp p)
x Natural -> Natural -> Natural
-! UInt n (Zp p) -> Natural
forall a b. ToConstant a b => a -> b
toConstant UInt n (Zp p)
y
    strictMul :: UInt n (Zp p) -> UInt n (Zp p) -> UInt n (Zp p)
strictMul UInt n (Zp p)
x UInt n (Zp p)
y = Natural -> UInt n (Zp p)
forall b a. StrictConv b a => b -> a
strictConv (Natural -> UInt n (Zp p)) -> Natural -> UInt n (Zp p)
forall a b. (a -> b) -> a -> b
$ UInt n (Zp p) -> Natural
forall a b. ToConstant a b => a -> b
toConstant UInt n (Zp p)
x Natural -> Natural -> Natural
forall a. MultiplicativeSemigroup a => a -> a -> a
* forall a b. ToConstant a b => a -> b
toConstant @_ @Natural UInt n (Zp p)
y

instance (Arithmetic a, KnownNat n) => StrictNum (UInt n (ArithmeticCircuit a)) where
    strictAdd :: UInt n (ArithmeticCircuit a)
-> UInt n (ArithmeticCircuit a) -> UInt n (ArithmeticCircuit a)
strictAdd (UInt [] ArithmeticCircuit a
x) (UInt [] ArithmeticCircuit a
y) = [ArithmeticCircuit a]
-> ArithmeticCircuit a -> UInt n (ArithmeticCircuit a)
forall (n :: Natural) a. [a] -> a -> UInt n a
UInt [] (ArithmeticCircuit a -> UInt n (ArithmeticCircuit a))
-> ArithmeticCircuit a -> UInt n (ArithmeticCircuit a)
forall a b. (a -> b) -> a -> b
$ (forall i (m :: Type -> Type). MonadBlueprint i a m => m i)
-> ArithmeticCircuit a
forall a.
Arithmetic a =>
(forall i (m :: Type -> Type). MonadBlueprint i a m => m i)
-> ArithmeticCircuit a
circuit ((forall i (m :: Type -> Type). MonadBlueprint i a m => m i)
 -> ArithmeticCircuit a)
-> (forall i (m :: Type -> Type). MonadBlueprint i a m => m i)
-> ArithmeticCircuit a
forall a b. (a -> b) -> a -> b
$ do
        i
z <- ArithmeticCircuit a -> m i
forall i a (m :: Type -> Type).
MonadBlueprint i a m =>
ArithmeticCircuit a -> m i
runCircuit (ArithmeticCircuit a
x ArithmeticCircuit a -> ArithmeticCircuit a -> ArithmeticCircuit a
forall a. AdditiveSemigroup a => a -> a -> a
+ ArithmeticCircuit a
y)
        [i]
_ <- Natural -> i -> m [i]
forall i a (m :: Type -> Type).
MonadBlueprint i a m =>
Natural -> i -> m [i]
expansion (forall a (n :: Natural). (Finite a, KnownNat n) => Natural
highRegisterSize @a @n) i
z
        i -> m i
forall a. a -> m a
forall (m :: Type -> Type) a. Monad m => a -> m a
return i
z

    strictAdd (UInt (ArithmeticCircuit a
x : [ArithmeticCircuit a]
xs) ArithmeticCircuit a
z) (UInt (ArithmeticCircuit a
y : [ArithmeticCircuit a]
ys) ArithmeticCircuit a
w) =
        let solve :: MonadBlueprint i a m => m [i]
            solve :: forall i (m :: Type -> Type). MonadBlueprint i a m => m [i]
solve = do
                (i
i, i
j) <- ArithmeticCircuit a -> m i
forall i a (m :: Type -> Type).
MonadBlueprint i a m =>
ArithmeticCircuit a -> m i
runCircuit (ArithmeticCircuit a
x ArithmeticCircuit a -> ArithmeticCircuit a -> ArithmeticCircuit a
forall a. AdditiveSemigroup a => a -> a -> a
+ ArithmeticCircuit a
y) 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
>>= Natural -> Natural -> i -> m (i, i)
forall i a (m :: Type -> Type).
MonadBlueprint i a m =>
Natural -> Natural -> i -> m (i, i)
splitExpansion (forall a (n :: Natural). (Finite a, KnownNat n) => Natural
registerSize @a @n) Natural
1
                ([i]
zs, i
c) <- (StateT i m [i] -> i -> m ([i], i))
-> i -> StateT i m [i] -> m ([i], i)
forall a b c. (a -> b -> c) -> b -> a -> c
flip StateT i m [i] -> i -> m ([i], i)
forall s (m :: Type -> Type) a. StateT s m a -> s -> m (a, s)
runStateT i
j (StateT i m [i] -> m ([i], i)) -> StateT i m [i] -> m ([i], i)
forall a b. (a -> b) -> a -> b
$ ((i -> m (i, i)) -> StateT i m i)
-> [i -> m (i, i)] -> StateT i m [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) -> [a] -> f [b]
traverse (i -> m (i, i)) -> StateT i m i
forall s (m :: Type -> Type) a. (s -> m (a, s)) -> StateT s m a
StateT ([i -> m (i, i)] -> StateT i m [i])
-> [i -> m (i, i)] -> StateT i m [i]
forall a b. (a -> b) -> a -> b
$
                    (ArithmeticCircuit a -> ArithmeticCircuit a -> i -> m (i, i))
-> [ArithmeticCircuit a]
-> [ArithmeticCircuit a]
-> [i -> m (i, i)]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (Natural
-> ArithmeticCircuit a -> ArithmeticCircuit a -> i -> m (i, i)
forall i a (m :: Type -> Type).
MonadBlueprint i a m =>
Natural
-> ArithmeticCircuit a -> ArithmeticCircuit a -> i -> m (i, i)
fullAdder (Natural
 -> ArithmeticCircuit a -> ArithmeticCircuit a -> i -> m (i, i))
-> Natural
-> ArithmeticCircuit a
-> ArithmeticCircuit a
-> i
-> m (i, i)
forall a b. (a -> b) -> a -> b
$ forall a (n :: Natural). (Finite a, KnownNat n) => Natural
registerSize @a @n) [ArithmeticCircuit a]
xs [ArithmeticCircuit a]
ys
                i
k <- ArithmeticCircuit a -> ArithmeticCircuit a -> i -> m i
forall i a (m :: Type -> Type).
MonadBlueprint i a m =>
ArithmeticCircuit a -> ArithmeticCircuit a -> i -> m i
fullAdded ArithmeticCircuit a
z ArithmeticCircuit a
w i
c
                [i]
_ <- Natural -> i -> m [i]
forall i a (m :: Type -> Type).
MonadBlueprint i a m =>
Natural -> i -> m [i]
expansion (forall a (n :: Natural). (Finite a, KnownNat n) => Natural
highRegisterSize @a @n) i
k
                [i] -> m [i]
forall a. a -> m a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (i
k i -> [i] -> [i]
forall a. a -> [a] -> [a]
: i
i i -> [i] -> [i]
forall a. a -> [a] -> [a]
: [i]
zs)

         in case (forall i (m :: Type -> Type). MonadBlueprint i a m => m [i])
-> [ArithmeticCircuit a]
forall a (f :: Type -> Type).
(Arithmetic a, Functor f) =>
(forall i (m :: Type -> Type). MonadBlueprint i a m => m (f i))
-> f (ArithmeticCircuit a)
circuits m [i]
forall i (m :: Type -> Type). MonadBlueprint i a m => m [i]
solve of
            (ArithmeticCircuit a
hi : [ArithmeticCircuit a]
lo) -> [ArithmeticCircuit a]
-> ArithmeticCircuit a -> UInt n (ArithmeticCircuit a)
forall (n :: Natural) a. [a] -> a -> UInt n a
UInt [ArithmeticCircuit a]
lo ArithmeticCircuit a
hi
            []        -> String -> UInt n (ArithmeticCircuit a)
forall a. HasCallStack => String -> a
error String
"UInt: unreachable"

    strictAdd (UInt [ArithmeticCircuit a]
_ ArithmeticCircuit a
_) (UInt [ArithmeticCircuit a]
_ ArithmeticCircuit a
_) = String -> UInt n (ArithmeticCircuit a)
forall a. HasCallStack => String -> a
error String
"UInt: unreachable"

    strictSub :: UInt n (ArithmeticCircuit a)
-> UInt n (ArithmeticCircuit a) -> UInt n (ArithmeticCircuit a)
strictSub (UInt [] ArithmeticCircuit a
x) (UInt [] ArithmeticCircuit a
y) = [ArithmeticCircuit a]
-> ArithmeticCircuit a -> UInt n (ArithmeticCircuit a)
forall (n :: Natural) a. [a] -> a -> UInt n a
UInt [] (ArithmeticCircuit a -> UInt n (ArithmeticCircuit a))
-> ArithmeticCircuit a -> UInt n (ArithmeticCircuit a)
forall a b. (a -> b) -> a -> b
$ (forall i (m :: Type -> Type). MonadBlueprint i a m => m i)
-> ArithmeticCircuit a
forall a.
Arithmetic a =>
(forall i (m :: Type -> Type). MonadBlueprint i a m => m i)
-> ArithmeticCircuit a
circuit ((forall i (m :: Type -> Type). MonadBlueprint i a m => m i)
 -> ArithmeticCircuit a)
-> (forall i (m :: Type -> Type). MonadBlueprint i a m => m i)
-> ArithmeticCircuit a
forall a b. (a -> b) -> a -> b
$ do
        i
z <- ArithmeticCircuit a -> m i
forall i a (m :: Type -> Type).
MonadBlueprint i a m =>
ArithmeticCircuit a -> m i
runCircuit (ArithmeticCircuit a
x ArithmeticCircuit a -> ArithmeticCircuit a -> ArithmeticCircuit a
forall a. AdditiveGroup a => a -> a -> a
- ArithmeticCircuit a
y)
        [i]
_ <- Natural -> i -> m [i]
forall i a (m :: Type -> Type).
MonadBlueprint i a m =>
Natural -> i -> m [i]
expansion (forall a (n :: Natural). (Finite a, KnownNat n) => Natural
highRegisterSize @a @n) i
z
        i -> m i
forall a. a -> m a
forall (m :: Type -> Type) a. Monad m => a -> m a
return i
z

    strictSub (UInt (ArithmeticCircuit a
x : [ArithmeticCircuit a]
xs) ArithmeticCircuit a
z) (UInt (ArithmeticCircuit a
y : [ArithmeticCircuit a]
ys) ArithmeticCircuit a
w) =
        let t :: a
            t :: a
t = (a
forall a. MultiplicativeMonoid a => a
one a -> a -> a
forall a. AdditiveSemigroup a => a -> a -> a
+ a
forall a. MultiplicativeMonoid a => a
one) a -> Natural -> a
forall a b. Exponent a b => a -> b -> a
^ forall a (n :: Natural). (Finite a, KnownNat n) => Natural
registerSize @a @n a -> a -> a
forall a. AdditiveGroup a => a -> a -> a
- a
forall a. MultiplicativeMonoid a => a
one

            solve :: MonadBlueprint i a m => m [i]
            solve :: forall i (m :: Type -> Type). MonadBlueprint i a m => m [i]
solve = do
                i
i <- ArithmeticCircuit a -> m i
forall i a (m :: Type -> Type).
MonadBlueprint i a m =>
ArithmeticCircuit a -> m i
runCircuit ArithmeticCircuit a
x
                i
j <- ArithmeticCircuit a -> m i
forall i a (m :: Type -> Type).
MonadBlueprint i a m =>
ArithmeticCircuit a -> m i
runCircuit ArithmeticCircuit a
y
                i
s <- ClosedPoly i a -> m i
forall i a (m :: Type -> Type).
MonadBlueprint i a m =>
ClosedPoly i a -> m i
newAssigned (\i -> x
v -> i -> x
v i
i x -> x -> x
forall a. AdditiveGroup a => a -> a -> a
- i -> x
v i
j x -> x -> x
forall a. AdditiveSemigroup a => a -> a -> a
+ a -> x
forall a b. FromConstant a b => a -> b
fromConstant (a
t a -> a -> a
forall a. AdditiveSemigroup a => a -> a -> a
+ a
forall a. MultiplicativeMonoid a => a
one))
                (i
k, i
b0) <- Natural -> Natural -> i -> m (i, i)
forall i a (m :: Type -> Type).
MonadBlueprint i a m =>
Natural -> Natural -> i -> m (i, i)
splitExpansion (forall a (n :: Natural). (Finite a, KnownNat n) => Natural
registerSize @a @n) Natural
1 i
s
                ([i]
zs, i
b) <- (StateT i m [i] -> i -> m ([i], i))
-> i -> StateT i m [i] -> m ([i], i)
forall a b c. (a -> b -> c) -> b -> a -> c
flip StateT i m [i] -> i -> m ([i], i)
forall s (m :: Type -> Type) a. StateT s m a -> s -> m (a, s)
runStateT i
b0 (StateT i m [i] -> m ([i], i)) -> StateT i m [i] -> m ([i], i)
forall a b. (a -> b) -> a -> b
$ ((i -> m (i, i)) -> StateT i m i)
-> [i -> m (i, i)] -> StateT i m [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) -> [a] -> f [b]
traverse (i -> m (i, i)) -> StateT i m i
forall s (m :: Type -> Type) a. (s -> m (a, s)) -> StateT s m a
StateT ((ArithmeticCircuit a -> ArithmeticCircuit a -> i -> m (i, i))
-> [ArithmeticCircuit a]
-> [ArithmeticCircuit a]
-> [i -> m (i, i)]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith ArithmeticCircuit a -> ArithmeticCircuit a -> i -> m (i, i)
forall i (m :: Type -> Type).
MonadBlueprint i a m =>
ArithmeticCircuit a -> ArithmeticCircuit a -> i -> m (i, i)
fullSub [ArithmeticCircuit a]
xs [ArithmeticCircuit a]
ys)
                i
k' <- ArithmeticCircuit a -> m i
forall i a (m :: Type -> Type).
MonadBlueprint i a m =>
ArithmeticCircuit a -> m i
runCircuit (ArithmeticCircuit a
z ArithmeticCircuit a -> ArithmeticCircuit a -> ArithmeticCircuit a
forall a. AdditiveGroup a => a -> a -> a
- ArithmeticCircuit a
w)
                i
s' <- ClosedPoly i a -> m i
forall i a (m :: Type -> Type).
MonadBlueprint i a m =>
ClosedPoly i a -> m i
newAssigned (\i -> x
v -> i -> x
v i
k' x -> x -> x
forall a. AdditiveSemigroup a => a -> a -> a
+ i -> x
v i
b x -> x -> x
forall a. AdditiveGroup a => a -> a -> a
- x
forall a. MultiplicativeMonoid a => a
one)
                [i]
_ <- Natural -> i -> m [i]
forall i a (m :: Type -> Type).
MonadBlueprint i a m =>
Natural -> i -> m [i]
expansion (forall a (n :: Natural). (Finite a, KnownNat n) => Natural
highRegisterSize @a @n) i
s'
                [i] -> m [i]
forall a. a -> m a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (i
s' i -> [i] -> [i]
forall a. a -> [a] -> [a]
: i
k i -> [i] -> [i]
forall a. a -> [a] -> [a]
: [i]
zs)

            fullSub :: MonadBlueprint i a m => ArithmeticCircuit a -> ArithmeticCircuit a -> i -> m (i, i)
            fullSub :: forall i (m :: Type -> Type).
MonadBlueprint i a m =>
ArithmeticCircuit a -> ArithmeticCircuit a -> i -> m (i, i)
fullSub ArithmeticCircuit a
xk ArithmeticCircuit a
yk i
b = do
                i
k <- ArithmeticCircuit a -> m i
forall i a (m :: Type -> Type).
MonadBlueprint i a m =>
ArithmeticCircuit a -> m i
runCircuit (ArithmeticCircuit a
xk ArithmeticCircuit a -> ArithmeticCircuit a -> ArithmeticCircuit a
forall a. AdditiveGroup a => a -> a -> a
- ArithmeticCircuit a
yk)
                i
s <- ClosedPoly i a -> m i
forall i a (m :: Type -> Type).
MonadBlueprint i a m =>
ClosedPoly i a -> m i
newAssigned (\i -> x
v -> i -> x
v i
k x -> x -> x
forall a. AdditiveSemigroup a => a -> a -> a
+ i -> x
v i
b x -> x -> x
forall a. AdditiveSemigroup a => a -> a -> a
+ a -> x
forall a b. FromConstant a b => a -> b
fromConstant a
t)
                Natural -> Natural -> i -> m (i, i)
forall i a (m :: Type -> Type).
MonadBlueprint i a m =>
Natural -> Natural -> i -> m (i, i)
splitExpansion (forall a (n :: Natural). (Finite a, KnownNat n) => Natural
registerSize @a @n) Natural
1 i
s

         in case (forall i (m :: Type -> Type). MonadBlueprint i a m => m [i])
-> [ArithmeticCircuit a]
forall a (f :: Type -> Type).
(Arithmetic a, Functor f) =>
(forall i (m :: Type -> Type). MonadBlueprint i a m => m (f i))
-> f (ArithmeticCircuit a)
circuits m [i]
forall i (m :: Type -> Type). MonadBlueprint i a m => m [i]
solve of
            (ArithmeticCircuit a
hi : [ArithmeticCircuit a]
lo) -> [ArithmeticCircuit a]
-> ArithmeticCircuit a -> UInt n (ArithmeticCircuit a)
forall (n :: Natural) a. [a] -> a -> UInt n a
UInt [ArithmeticCircuit a]
lo ArithmeticCircuit a
hi
            []        -> String -> UInt n (ArithmeticCircuit a)
forall a. HasCallStack => String -> a
error String
"UInt: unreachable"

    strictSub (UInt [ArithmeticCircuit a]
_ ArithmeticCircuit a
_) (UInt [ArithmeticCircuit a]
_ ArithmeticCircuit a
_) = String -> UInt n (ArithmeticCircuit a)
forall a. HasCallStack => String -> a
error String
"UInt: unreachable"

    strictMul :: UInt n (ArithmeticCircuit a)
-> UInt n (ArithmeticCircuit a) -> UInt n (ArithmeticCircuit a)
strictMul (UInt [] ArithmeticCircuit a
x) (UInt [] ArithmeticCircuit a
y) = [ArithmeticCircuit a]
-> ArithmeticCircuit a -> UInt n (ArithmeticCircuit a)
forall (n :: Natural) a. [a] -> a -> UInt n a
UInt [] (ArithmeticCircuit a -> UInt n (ArithmeticCircuit a))
-> ArithmeticCircuit a -> UInt n (ArithmeticCircuit a)
forall a b. (a -> b) -> a -> b
$ (forall i (m :: Type -> Type). MonadBlueprint i a m => m i)
-> ArithmeticCircuit a
forall a.
Arithmetic a =>
(forall i (m :: Type -> Type). MonadBlueprint i a m => m i)
-> ArithmeticCircuit a
circuit ((forall i (m :: Type -> Type). MonadBlueprint i a m => m i)
 -> ArithmeticCircuit a)
-> (forall i (m :: Type -> Type). MonadBlueprint i a m => m i)
-> ArithmeticCircuit a
forall a b. (a -> b) -> a -> b
$ do
        i
z <- ArithmeticCircuit a -> m i
forall i a (m :: Type -> Type).
MonadBlueprint i a m =>
ArithmeticCircuit a -> m i
runCircuit (ArithmeticCircuit a
x ArithmeticCircuit a -> ArithmeticCircuit a -> ArithmeticCircuit a
forall a. MultiplicativeSemigroup a => a -> a -> a
* ArithmeticCircuit a
y)
        [i]
_ <- Natural -> i -> m [i]
forall i a (m :: Type -> Type).
MonadBlueprint i a m =>
Natural -> i -> m [i]
expansion (forall a (n :: Natural). (Finite a, KnownNat n) => Natural
highRegisterSize @a @n) i
z
        i -> m i
forall a. a -> m a
forall (m :: Type -> Type) a. Monad m => a -> m a
return i
z

    strictMul (UInt (ArithmeticCircuit a
x : [ArithmeticCircuit a]
xs) ArithmeticCircuit a
z) (UInt (ArithmeticCircuit a
y : [ArithmeticCircuit a]
ys) ArithmeticCircuit a
w) =
        let solve :: MonadBlueprint i a m => m [i]
            solve :: forall i (m :: Type -> Type). MonadBlueprint i a m => m [i]
solve = do
                i
i <- ArithmeticCircuit a -> m i
forall i a (m :: Type -> Type).
MonadBlueprint i a m =>
ArithmeticCircuit a -> m i
runCircuit ArithmeticCircuit a
x
                i
j <- ArithmeticCircuit a -> m i
forall i a (m :: Type -> Type).
MonadBlueprint i a m =>
ArithmeticCircuit a -> m i
runCircuit ArithmeticCircuit a
y
                [i]
is <- [ArithmeticCircuit a] -> (ArithmeticCircuit a -> m i) -> m [i]
forall (t :: Type -> Type) (f :: Type -> Type) a b.
(Traversable t, Applicative f) =>
t a -> (a -> f b) -> f (t b)
for [ArithmeticCircuit a]
xs ArithmeticCircuit a -> m i
forall i a (m :: Type -> Type).
MonadBlueprint i a m =>
ArithmeticCircuit a -> m i
runCircuit
                [i]
js <- [ArithmeticCircuit a] -> (ArithmeticCircuit a -> m i) -> m [i]
forall (t :: Type -> Type) (f :: Type -> Type) a b.
(Traversable t, Applicative f) =>
t a -> (a -> f b) -> f (t b)
for [ArithmeticCircuit a]
ys ArithmeticCircuit a -> m i
forall i a (m :: Type -> Type).
MonadBlueprint i a m =>
ArithmeticCircuit a -> m i
runCircuit
                i
i' <- ArithmeticCircuit a -> m i
forall i a (m :: Type -> Type).
MonadBlueprint i a m =>
ArithmeticCircuit a -> m i
runCircuit ArithmeticCircuit a
z
                i
j' <- ArithmeticCircuit a -> m i
forall i a (m :: Type -> Type).
MonadBlueprint i a m =>
ArithmeticCircuit a -> m i
runCircuit ArithmeticCircuit a
w
                let cs :: Map Natural i
cs = [(Natural, i)] -> Map Natural i
forall k a. Ord k => [(k, a)] -> Map k a
fromList ([(Natural, i)] -> Map Natural i)
-> [(Natural, i)] -> Map Natural i
forall a b. (a -> b) -> a -> b
$ [Natural] -> [i] -> [(Natural, i)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Natural
0..] (i
i i -> [i] -> [i]
forall a. a -> [a] -> [a]
: [i]
is [i] -> [i] -> [i]
forall a. [a] -> [a] -> [a]
++ [i
i'])
                    ds :: Map Natural i
ds = [(Natural, i)] -> Map Natural i
forall k a. Ord k => [(k, a)] -> Map k a
fromList ([(Natural, i)] -> Map Natural i)
-> [(Natural, i)] -> Map Natural i
forall a b. (a -> b) -> a -> b
$ [Natural] -> [i] -> [(Natural, i)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Natural
0..] (i
j i -> [i] -> [i]
forall a. a -> [a] -> [a]
: [i]
js [i] -> [i] -> [i]
forall a. [a] -> [a] -> [a]
++ [i
j'])
                    r :: Natural
r  = forall a (n :: Natural). (Finite a, KnownNat n) => Natural
numberOfRegisters @a @n
                -- single addend for lower register
                i
q <- ClosedPoly i a -> m i
forall i a (m :: Type -> Type).
MonadBlueprint i a m =>
ClosedPoly i a -> m i
newAssigned (\i -> x
v -> i -> x
v i
i x -> x -> x
forall a. MultiplicativeSemigroup a => a -> a -> a
* i -> x
v i
j)
                -- multiple addends for middle registers
                [[i]]
qs <- [Natural] -> (Natural -> m [i]) -> m [[i]]
forall (t :: Type -> Type) (f :: Type -> Type) a b.
(Traversable t, Applicative f) =>
t a -> (a -> f b) -> f (t b)
for [Natural
1 .. Natural
r Natural -> Natural -> Natural
-! Natural
2] ((Natural -> m [i]) -> m [[i]]) -> (Natural -> m [i]) -> m [[i]]
forall a b. (a -> b) -> a -> b
$ \Natural
k ->
                    [Natural] -> (Natural -> m i) -> m [i]
forall (t :: Type -> Type) (f :: Type -> Type) a b.
(Traversable t, Applicative f) =>
t a -> (a -> f b) -> f (t b)
for [Natural
0 .. Natural
k] ((Natural -> m i) -> m [i]) -> (Natural -> m i) -> m [i]
forall a b. (a -> b) -> a -> b
$ \Natural
l ->
                        ClosedPoly i a -> m i
forall i a (m :: Type -> Type).
MonadBlueprint i a m =>
ClosedPoly i a -> m i
newAssigned (\i -> x
v -> i -> x
v (Map Natural i
cs Map Natural i -> Natural -> i
forall k a. Ord k => Map k a -> k -> a
! Natural
l) x -> x -> x
forall a. MultiplicativeSemigroup a => a -> a -> a
* i -> x
v (Map Natural i
ds Map Natural i -> Natural -> i
forall k a. Ord k => Map k a -> k -> a
! (Natural
k Natural -> Natural -> Natural
-! Natural
l)))
                -- lower register
                (i
p, i
c) <- Natural -> Natural -> i -> m (i, i)
forall i a (m :: Type -> Type).
MonadBlueprint i a m =>
Natural -> Natural -> i -> m (i, i)
splitExpansion (forall a (n :: Natural). (Finite a, KnownNat n) => Natural
registerSize @a @n) (forall a (n :: Natural). (Finite a, KnownNat n) => Natural
registerSize @a @n) i
q
                -- middle registers
                ([i]
ps, i
c') <- (StateT i m [i] -> i -> m ([i], i))
-> i -> StateT i m [i] -> m ([i], i)
forall a b c. (a -> b -> c) -> b -> a -> c
flip StateT i m [i] -> i -> m ([i], i)
forall s (m :: Type -> Type) a. StateT s m a -> s -> m (a, s)
runStateT i
c (StateT i m [i] -> m ([i], i)) -> StateT i m [i] -> m ([i], i)
forall a b. (a -> b) -> a -> b
$ [[i]] -> ([i] -> StateT i m i) -> StateT i m [i]
forall (t :: Type -> Type) (f :: Type -> Type) a b.
(Traversable t, Applicative f) =>
t a -> (a -> f b) -> f (t b)
for [[i]]
qs (([i] -> StateT i m i) -> StateT i m [i])
-> ([i] -> StateT i m i) -> StateT i m [i]
forall a b. (a -> b) -> a -> b
$ (i -> m (i, i)) -> StateT i m i
forall s (m :: Type -> Type) a. (s -> m (a, s)) -> StateT s m a
StateT ((i -> m (i, i)) -> StateT i m i)
-> ([i] -> i -> m (i, i)) -> [i] -> StateT i m i
forall b c a. (b -> c) -> (a -> b) -> a -> c
. \[i]
rs i
c' -> do
                    i
s <- (i -> i -> m i) -> i -> [i] -> m i
forall (t :: Type -> Type) (m :: Type -> Type) a b.
(Foldable t, Monad m) =>
(a -> b -> m b) -> b -> t a -> m b
foldrM (\i
k i
l -> ClosedPoly i a -> m i
forall i a (m :: Type -> Type).
MonadBlueprint i a m =>
ClosedPoly i a -> m i
newAssigned (\i -> x
v -> i -> x
v i
k x -> x -> x
forall a. AdditiveSemigroup a => a -> a -> a
+ i -> x
v i
l)) i
c' [i]
rs
                    Natural -> Natural -> i -> m (i, i)
forall i a (m :: Type -> Type).
MonadBlueprint i a m =>
Natural -> Natural -> i -> m (i, i)
splitExpansion (forall a (n :: Natural). (Finite a, KnownNat n) => Natural
registerSize @a @n) (forall a (n :: Natural). (Finite a, KnownNat n) => Natural
maxOverflow @a @n) i
s
                -- high register
                i
p' <- (Natural -> i -> m i) -> i -> [Natural] -> m i
forall (t :: Type -> Type) (m :: Type -> Type) a b.
(Foldable t, Monad m) =>
(a -> b -> m b) -> b -> t a -> m b
foldrM (\Natural
k i
l -> do
                    i
k' <- ClosedPoly i a -> m i
forall i a (m :: Type -> Type).
MonadBlueprint i a m =>
ClosedPoly i a -> m i
newAssigned (\i -> x
v -> i -> x
v (Map Natural i
cs Map Natural i -> Natural -> i
forall k a. Ord k => Map k a -> k -> a
! Natural
k) x -> x -> x
forall a. MultiplicativeSemigroup a => a -> a -> a
* i -> x
v (Map Natural i
ds Map Natural i -> Natural -> i
forall k a. Ord k => Map k a -> k -> a
! (Natural
r Natural -> Natural -> Natural
-! (Natural
k Natural -> Natural -> Natural
forall a. AdditiveSemigroup a => a -> a -> a
+ Natural
1))))
                    ClosedPoly i a -> m i
forall i a (m :: Type -> Type).
MonadBlueprint i a m =>
ClosedPoly i a -> m i
newAssigned (\i -> x
v -> i -> x
v i
l x -> x -> x
forall a. AdditiveSemigroup a => a -> a -> a
+ i -> x
v i
k')) i
c' [Natural
0 .. Natural
r Natural -> Natural -> Natural
-! Natural
1]
                [i]
_ <- Natural -> i -> m [i]
forall i a (m :: Type -> Type).
MonadBlueprint i a m =>
Natural -> i -> m [i]
expansion (forall a (n :: Natural). (Finite a, KnownNat n) => Natural
highRegisterSize @a @n) i
p'
                -- all addends higher should be zero
                [Natural] -> (Natural -> m ()) -> m ()
forall (t :: Type -> Type) (f :: Type -> Type) a b.
(Foldable t, Applicative f) =>
t a -> (a -> f b) -> f ()
for_ [Natural
r .. Natural
r Natural -> Natural -> Natural
forall a. MultiplicativeSemigroup a => a -> a -> a
* Natural
2 Natural -> Natural -> Natural
-! Natural
2] ((Natural -> m ()) -> m ()) -> (Natural -> m ()) -> m ()
forall a b. (a -> b) -> a -> b
$ \Natural
k ->
                    [Natural] -> (Natural -> m ()) -> m ()
forall (t :: Type -> Type) (f :: Type -> Type) a b.
(Foldable t, Applicative f) =>
t a -> (a -> f b) -> f ()
for_ [Natural
k Natural -> Natural -> Natural
-! Natural
r Natural -> Natural -> Natural
forall a. AdditiveSemigroup a => a -> a -> a
+ Natural
1 .. Natural
r Natural -> Natural -> Natural
-! Natural
1] ((Natural -> m ()) -> m ()) -> (Natural -> m ()) -> m ()
forall a b. (a -> b) -> a -> b
$ \Natural
l ->
                        ClosedPoly i a -> m ()
forall i a (m :: Type -> Type).
MonadBlueprint i a m =>
ClosedPoly i a -> m ()
constraint (\i -> x
v -> i -> x
v (Map Natural i
cs Map Natural i -> Natural -> i
forall k a. Ord k => Map k a -> k -> a
! Natural
l) x -> x -> x
forall a. MultiplicativeSemigroup a => a -> a -> a
* i -> x
v (Map Natural i
ds Map Natural i -> Natural -> i
forall k a. Ord k => Map k a -> k -> a
! (Natural
k Natural -> Natural -> Natural
-! Natural
l)))
                [i] -> m [i]
forall a. a -> m a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (i
p' i -> [i] -> [i]
forall a. a -> [a] -> [a]
: i
p i -> [i] -> [i]
forall a. a -> [a] -> [a]
: [i]
ps)

         in case (forall i (m :: Type -> Type). MonadBlueprint i a m => m [i])
-> [ArithmeticCircuit a]
forall a (f :: Type -> Type).
(Arithmetic a, Functor f) =>
(forall i (m :: Type -> Type). MonadBlueprint i a m => m (f i))
-> f (ArithmeticCircuit a)
circuits m [i]
forall i (m :: Type -> Type). MonadBlueprint i a m => m [i]
solve of
            (ArithmeticCircuit a
hi : [ArithmeticCircuit a]
lo) -> [ArithmeticCircuit a]
-> ArithmeticCircuit a -> UInt n (ArithmeticCircuit a)
forall (n :: Natural) a. [a] -> a -> UInt n a
UInt [ArithmeticCircuit a]
lo ArithmeticCircuit a
hi
            []        -> String -> UInt n (ArithmeticCircuit a)
forall a. HasCallStack => String -> a
error String
"UInt: unreachable"

    strictMul (UInt [ArithmeticCircuit a]
_ ArithmeticCircuit a
_) (UInt [ArithmeticCircuit a]
_ ArithmeticCircuit a
_) = String -> UInt n (ArithmeticCircuit a)
forall a. HasCallStack => String -> a
error String
"UInt: unreachable"

--------------------------------------------------------------------------------

fullAdder :: MonadBlueprint i a m => Natural -> ArithmeticCircuit a -> ArithmeticCircuit a -> i -> m (i, i)
fullAdder :: forall i a (m :: Type -> Type).
MonadBlueprint i a m =>
Natural
-> ArithmeticCircuit a -> ArithmeticCircuit a -> i -> m (i, i)
fullAdder Natural
r ArithmeticCircuit a
xk ArithmeticCircuit a
yk i
c = ArithmeticCircuit a -> ArithmeticCircuit a -> i -> m i
forall i a (m :: Type -> Type).
MonadBlueprint i a m =>
ArithmeticCircuit a -> ArithmeticCircuit a -> i -> m i
fullAdded ArithmeticCircuit a
xk ArithmeticCircuit a
yk i
c 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
>>= Natural -> Natural -> i -> m (i, i)
forall i a (m :: Type -> Type).
MonadBlueprint i a m =>
Natural -> Natural -> i -> m (i, i)
splitExpansion Natural
r Natural
1

fullAdded :: MonadBlueprint i a m => ArithmeticCircuit a -> ArithmeticCircuit a -> i -> m i
fullAdded :: forall i a (m :: Type -> Type).
MonadBlueprint i a m =>
ArithmeticCircuit a -> ArithmeticCircuit a -> i -> m i
fullAdded ArithmeticCircuit a
xk ArithmeticCircuit a
yk i
c = do
    i
i <- ArithmeticCircuit a -> m i
forall i a (m :: Type -> Type).
MonadBlueprint i a m =>
ArithmeticCircuit a -> m i
runCircuit ArithmeticCircuit a
xk
    i
j <- ArithmeticCircuit a -> m i
forall i a (m :: Type -> Type).
MonadBlueprint i a m =>
ArithmeticCircuit a -> m i
runCircuit ArithmeticCircuit a
yk
    i
k <- ClosedPoly i a -> m i
forall i a (m :: Type -> Type).
MonadBlueprint i a m =>
ClosedPoly i a -> m i
newAssigned (\i -> x
v -> i -> x
v i
i x -> x -> x
forall a. AdditiveSemigroup a => a -> a -> a
+ i -> x
v i
j)
    ClosedPoly i a -> m i
forall i a (m :: Type -> Type).
MonadBlueprint i a m =>
ClosedPoly i a -> m i
newAssigned (\i -> x
v -> i -> x
v i
k x -> x -> x
forall a. AdditiveSemigroup a => a -> a -> a
+ i -> x
v i
c)