{-# 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
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)
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
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)
[[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)))
(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
([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
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
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)
[[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)))
(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
([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
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'
[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)