{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DerivingVia #-}
{-# LANGUAGE NoDeriveAnyClass #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -freduction-depth=0 #-}
module ZkFold.Symbolic.Data.UInt (
StrictConv(..),
StrictNum(..),
UInt(..),
toConstant,
eea
) where
import Control.DeepSeq
import Control.Monad.State (StateT (..))
import Data.Aeson hiding (Bool)
import Data.Foldable (foldlM, foldr, foldrM, for_)
import Data.Functor ((<$>))
import Data.Kind (Type)
import Data.List (unfoldr, zip)
import Data.Map (fromList, (!))
import Data.Traversable (for, traverse)
import Data.Tuple (swap)
import qualified Data.Zip as Z
import GHC.Generics (Generic, Par1 (..))
import GHC.Natural (naturalFromInteger)
import Prelude (Integer, const, error, flip, otherwise, return, type (~), ($),
(++), (.), (<>), (>>=))
import qualified Prelude as Haskell
import Test.QuickCheck (Arbitrary (..), chooseInteger)
import ZkFold.Base.Algebra.Basic.Class
import ZkFold.Base.Algebra.Basic.Field (Zp)
import ZkFold.Base.Algebra.Basic.Number
import qualified ZkFold.Base.Data.Vector as V
import ZkFold.Base.Data.Vector (Vector (..))
import ZkFold.Prelude (drop, length, replicate, replicateA)
import ZkFold.Symbolic.Class
import ZkFold.Symbolic.Data.Bool
import ZkFold.Symbolic.Data.ByteString
import ZkFold.Symbolic.Data.Class (SymbolicData)
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.FieldElement (FieldElement)
import ZkFold.Symbolic.Data.Input (SymbolicInput, isValid)
import ZkFold.Symbolic.Data.Ord
import ZkFold.Symbolic.Interpreter (Interpreter (..))
import ZkFold.Symbolic.MonadCircuit (MonadCircuit, constraint, newAssigned)
newtype UInt (n :: Natural) (r :: RegisterSize) (context :: (Type -> Type) -> Type) = UInt (context (Vector (NumberOfRegisters (BaseField context) n r)))
deriving instance Generic (UInt n r context)
deriving instance (NFData (context (Vector (NumberOfRegisters (BaseField context) n r)))) => NFData (UInt n r context)
deriving instance (Haskell.Eq (context (Vector (NumberOfRegisters (BaseField context) n r)))) => Haskell.Eq (UInt n r context)
deriving instance (Haskell.Show (BaseField context), Haskell.Show (context (Vector (NumberOfRegisters (BaseField context) n r)))) => Haskell.Show (UInt n r context)
deriving newtype instance SymbolicData (UInt n r c)
instance (Symbolic c, KnownNat n, KnownRegisterSize r) => FromConstant Natural (UInt n r c) where
fromConstant :: Natural -> UInt n r c
fromConstant Natural
c = c (Vector (NumberOfRegisters (BaseField c) n r)) -> UInt n r c
forall (n :: Natural) (r :: RegisterSize)
(context :: (Type -> Type) -> Type).
context (Vector (NumberOfRegisters (BaseField context) n r))
-> UInt n r context
UInt (c (Vector (NumberOfRegisters (BaseField c) n r)) -> UInt n r c)
-> (Vector (NumberOfRegisters (BaseField c) n r) (BaseField c)
-> c (Vector (NumberOfRegisters (BaseField c) n r)))
-> Vector (NumberOfRegisters (BaseField c) n r) (BaseField c)
-> UInt n r c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (c :: (Type -> Type) -> Type) (f :: Type -> Type).
(Symbolic c, Functor f) =>
f (BaseField c) -> c f
embed @c (Vector (NumberOfRegisters (BaseField c) n r) (BaseField c)
-> UInt n r c)
-> Vector (NumberOfRegisters (BaseField c) n r) (BaseField c)
-> UInt n r c
forall a b. (a -> b) -> a -> b
$ forall (c :: (Type -> Type) -> Type) (n :: Natural)
(r :: RegisterSize).
(Symbolic c, KnownNat n, KnownRegisterSize r) =>
Natural
-> Vector (NumberOfRegisters (BaseField c) n r) (BaseField c)
naturalToVector @c @n @r Natural
c
instance (Symbolic c, KnownNat n, KnownRegisterSize r) => FromConstant Integer (UInt n r c) where
fromConstant :: Integer -> UInt n r c
fromConstant = Natural -> UInt n r c
forall a b. FromConstant a b => a -> b
fromConstant (Natural -> UInt n r c)
-> (Integer -> Natural) -> Integer -> UInt n r c
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 (Symbolic c, KnownNat n, KnownRegisterSize r) => Scale Natural (UInt n r c)
instance (Symbolic c, KnownNat n, KnownRegisterSize r) => Scale Integer (UInt n r c)
instance MultiplicativeMonoid (UInt n r c) => Exponent (UInt n r c) Natural where
^ :: UInt n r c -> Natural -> UInt n r c
(^) = UInt n r c -> Natural -> UInt n r c
forall a. MultiplicativeMonoid a => a -> Natural -> a
natPow
cast :: forall a n r . (Arithmetic a, KnownNat n, KnownRegisterSize r) => Natural -> ([Natural], Natural, [Natural])
cast :: forall a (n :: Natural) (r :: RegisterSize).
(Arithmetic a, KnownNat n, KnownRegisterSize r) =>
Natural -> ([Natural], Natural, [Natural])
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) (r :: RegisterSize).
(Finite a, KnownNat n, KnownRegisterSize r) =>
Natural
registerSize @a @n @r
registers :: [Natural]
registers = ((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) (r :: RegisterSize).
(Finite a, KnownNat n, KnownRegisterSize r) =>
Natural
numberOfRegisters @a @n @r Natural -> Natural -> Natural
-! Natural
1
in case Natural -> [Natural] -> ([Natural], [Natural])
forall {a}. Natural -> [a] -> ([a], [a])
greedySplitAt Natural
r [Natural]
registers of
([Natural]
lo, Natural
hi:[Natural]
rest) -> ([Natural]
lo, Natural
hi, [Natural]
rest)
([Natural]
lo, []) -> ([Natural]
lo [Natural] -> [Natural] -> [Natural]
forall a. [a] -> [a] -> [a]
++ Natural -> Natural -> [Natural]
forall a. Natural -> a -> [a]
replicate (Natural
r Natural -> Natural -> Natural
-! [Natural] -> Natural
forall (t :: Type -> Type) a. Foldable t => t a -> Natural
length [Natural]
lo) Natural
forall a. AdditiveMonoid a => a
zero, Natural
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 c r
. Symbolic c
=> SemiEuclidean (UInt n r c)
=> KnownNat n
=> KnownNat (NumberOfRegisters (BaseField c) n r)
=> AdditiveGroup (UInt n r c)
=> Eq (Bool c) (UInt n r c)
=> UInt n r c -> UInt n r c -> (UInt n r c, UInt n r c, UInt n r c)
eea :: forall (n :: Natural) (c :: (Type -> Type) -> Type)
(r :: RegisterSize).
(Symbolic c, SemiEuclidean (UInt n r c), KnownNat n,
KnownNat (NumberOfRegisters (BaseField c) n r),
AdditiveGroup (UInt n r c), Eq (Bool c) (UInt n r c)) =>
UInt n r c -> UInt n r c -> (UInt n r c, UInt n r c, UInt n r c)
eea UInt n r c
a UInt n r c
b = Natural
-> UInt n r c
-> UInt n r c
-> UInt n r c
-> UInt n r c
-> UInt n r c
-> UInt n r c
-> (UInt n r c, UInt n r c, UInt n r c)
eea' Natural
1 UInt n r c
a UInt n r c
b UInt n r c
forall a. MultiplicativeMonoid a => a
one UInt n r c
forall a. AdditiveMonoid a => a
zero UInt n r c
forall a. AdditiveMonoid a => a
zero UInt n r c
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 r c -> UInt n r c -> UInt n r c -> UInt n r c -> UInt n r c -> UInt n r c -> (UInt n r c, UInt n r c, UInt n r c)
eea' :: Natural
-> UInt n r c
-> UInt n r c
-> UInt n r c
-> UInt n r c
-> UInt n r c
-> UInt n r c
-> (UInt n r c, UInt n r c, UInt n r c)
eea' Natural
iteration UInt n r c
oldR UInt n r c
r UInt n r c
oldS UInt n r c
s UInt n r c
oldT UInt n r c
t
| Natural
iteration Natural -> Natural -> Bool
forall a. Eq a => a -> a -> Bool
Haskell.== Natural
iterations = (UInt n r c
oldS, UInt n r c
oldT, UInt n r c
oldR)
| Bool
otherwise = forall b a. Conditional b a => a -> a -> b -> a
bool @(Bool c) (UInt n r c, UInt n r c, UInt n r c)
rec (if Natural -> Bool
forall a. Integral a => a -> Bool
Haskell.even Natural
iteration then UInt n r c
b UInt n r c -> UInt n r c -> UInt n r c
forall a. AdditiveGroup a => a -> a -> a
- UInt n r c
oldS else UInt n r c
oldS, if Natural -> Bool
forall a. Integral a => a -> Bool
Haskell.odd Natural
iteration then UInt n r c
a UInt n r c -> UInt n r c -> UInt n r c
forall a. AdditiveGroup a => a -> a -> a
- UInt n r c
oldT else UInt n r c
oldT, UInt n r c
oldR) (UInt n r c
r UInt n r c -> UInt n r c -> Bool c
forall b a. Eq b a => a -> a -> b
== UInt n r c
forall a. AdditiveMonoid a => a
zero)
where
quotient :: UInt n r c
quotient = UInt n r c
oldR UInt n r c -> UInt n r c -> UInt n r c
forall a. SemiEuclidean a => a -> a -> a
`div` UInt n r c
r
rec :: (UInt n r c, UInt n r c, UInt n r c)
rec = Natural
-> UInt n r c
-> UInt n r c
-> UInt n r c
-> UInt n r c
-> UInt n r c
-> UInt n r c
-> (UInt n r c, UInt n r c, UInt n r c)
eea' (Natural
iteration Natural -> Natural -> Natural
forall a. AdditiveSemigroup a => a -> a -> a
+ Natural
1) UInt n r c
r (UInt n r c
oldR UInt n r c -> UInt n r c -> UInt n r c
forall a. AdditiveGroup a => a -> a -> a
- UInt n r c
quotient UInt n r c -> UInt n r c -> UInt n r c
forall a. MultiplicativeSemigroup a => a -> a -> a
* UInt n r c
r) UInt n r c
s (UInt n r c
quotient UInt n r c -> UInt n r c -> UInt n r c
forall a. MultiplicativeSemigroup a => a -> a -> a
* UInt n r c
s UInt n r c -> UInt n r c -> UInt n r c
forall a. AdditiveSemigroup a => a -> a -> a
+ UInt n r c
oldS) UInt n r c
t (UInt n r c
quotient UInt n r c -> UInt n r c -> UInt n r c
forall a. MultiplicativeSemigroup a => a -> a -> a
* UInt n r c
t UInt n r c -> UInt n r c -> UInt n r c
forall a. AdditiveSemigroup a => a -> a -> a
+ UInt n r c
oldT)
instance (Symbolic (Interpreter (Zp p)), KnownNat n, KnownRegisterSize r) => ToConstant (UInt n r (Interpreter (Zp p))) where
type Const (UInt n r (Interpreter (Zp p))) = Natural
toConstant :: UInt n r (Interpreter (Zp p))
-> Const (UInt n r (Interpreter (Zp p)))
toConstant (UInt (Interpreter Vector
(NumberOfRegisters (BaseField (Interpreter (Zp p))) n r) (Zp p)
xs)) = Vector (NumberOfRegisters (Zp p) n r) (Zp p) -> Natural -> Natural
forall a (n :: Natural).
(ToConstant a, Const a ~ Natural) =>
Vector n a -> Natural -> Natural
vectorToNatural Vector (NumberOfRegisters (Zp p) n r) (Zp p)
Vector
(NumberOfRegisters (BaseField (Interpreter (Zp p))) n r) (Zp p)
xs (forall a (n :: Natural) (r :: RegisterSize).
(Finite a, KnownNat n, KnownRegisterSize r) =>
Natural
registerSize @(Zp p) @n @r)
instance (Symbolic c, KnownNat n, KnownRegisterSize r) => MultiplicativeMonoid (UInt n r c) where
one :: UInt n r c
one = Natural -> UInt n r c
forall a b. FromConstant a b => a -> b
fromConstant (Natural
1 :: Natural)
instance (Symbolic c, KnownNat n, KnownRegisterSize r) => Semiring (UInt n r c)
instance (Symbolic c, KnownNat n, KnownRegisterSize r) => Arbitrary (UInt n r c) where
arbitrary :: Gen (UInt n r c)
arbitrary = do
[BaseField c]
lo <- Natural -> Gen (BaseField c) -> Gen [BaseField c]
forall (f :: Type -> Type) a.
Applicative f =>
Natural -> f a -> f [a]
replicateA (forall a (n :: Natural) (r :: RegisterSize).
(Finite a, KnownNat n, KnownRegisterSize r) =>
Natural
numberOfRegisters @(BaseField c) @n @r Natural -> Natural -> Natural
-! Natural
1) (Natural -> Gen (BaseField c)
forall {b} {b}.
(FromConstant Integer b, Exponent Integer b) =>
b -> Gen b
toss (Natural -> Gen (BaseField c)) -> Natural -> Gen (BaseField c)
forall a b. (a -> b) -> a -> b
$ forall a (n :: Natural) (r :: RegisterSize).
(Finite a, KnownNat n, KnownRegisterSize r) =>
Natural
registerSize @(BaseField c) @n @r)
BaseField c
hi <- Natural -> Gen (BaseField c)
forall {b} {b}.
(FromConstant Integer b, Exponent Integer b) =>
b -> Gen b
toss (forall a (n :: Natural) (r :: RegisterSize).
(Finite a, KnownNat n, KnownRegisterSize r) =>
Natural
highRegisterSize @(BaseField c) @n @r)
UInt n r c -> Gen (UInt n r c)
forall a. a -> Gen a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (UInt n r c -> Gen (UInt n r c)) -> UInt n r c -> Gen (UInt n r c)
forall a b. (a -> b) -> a -> b
$ c (Vector (NumberOfRegisters (BaseField c) n r)) -> UInt n r c
forall (n :: Natural) (r :: RegisterSize)
(context :: (Type -> Type) -> Type).
context (Vector (NumberOfRegisters (BaseField context) n r))
-> UInt n r context
UInt (c (Vector (NumberOfRegisters (BaseField c) n r)) -> UInt n r c)
-> c (Vector (NumberOfRegisters (BaseField c) n r)) -> UInt n r c
forall a b. (a -> b) -> a -> b
$ Vector (NumberOfRegisters (BaseField c) n r) (BaseField c)
-> c (Vector (NumberOfRegisters (BaseField c) n r))
forall (c :: (Type -> Type) -> Type) (f :: Type -> Type).
(Symbolic c, Functor f) =>
f (BaseField c) -> c f
embed (Vector (NumberOfRegisters (BaseField c) n r) (BaseField c)
-> c (Vector (NumberOfRegisters (BaseField c) n r)))
-> Vector (NumberOfRegisters (BaseField c) n r) (BaseField c)
-> c (Vector (NumberOfRegisters (BaseField c) n r))
forall a b. (a -> b) -> a -> b
$ [BaseField c]
-> Vector (NumberOfRegisters (BaseField c) n r) (BaseField c)
forall (size :: Natural) a. [a] -> Vector size a
V.unsafeToVector ([BaseField c]
lo [BaseField c] -> [BaseField c] -> [BaseField c]
forall a. Semigroup a => a -> a -> a
<> [BaseField c
hi])
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 (Symbolic c, KnownNat n, KnownRegisterSize r) => Iso (ByteString n c) (UInt n r c) where
from :: ByteString n c -> UInt n r c
from (ByteString c (Vector n)
b) = c (Vector (NumberOfRegisters (BaseField c) n r)) -> UInt n r c
forall (n :: Natural) (r :: RegisterSize)
(context :: (Type -> Type) -> Type).
context (Vector (NumberOfRegisters (BaseField context) n r))
-> UInt n r context
UInt (c (Vector (NumberOfRegisters (BaseField c) n r)) -> UInt n r c)
-> c (Vector (NumberOfRegisters (BaseField c) n r)) -> UInt n r c
forall a b. (a -> b) -> a -> b
$ c (Vector n)
-> (Vector n (BaseField c)
-> Vector (NumberOfRegisters (BaseField c) n r) (BaseField c))
-> CircuitFun
(Vector n)
(Vector (NumberOfRegisters (BaseField c) n r))
(BaseField c)
-> c (Vector (NumberOfRegisters (BaseField c) n r))
forall a (f :: Type -> Type) (g :: Type -> Type).
(BaseField c ~ a) =>
c f -> (f a -> g a) -> CircuitFun f g a -> c g
forall (c :: (Type -> Type) -> Type) a (f :: Type -> Type)
(g :: Type -> Type).
(Symbolic c, BaseField c ~ a) =>
c f -> (f a -> g a) -> CircuitFun f g a -> c g
symbolicF c (Vector n)
b (forall (c :: (Type -> Type) -> Type) (n :: Natural)
(r :: RegisterSize).
(Symbolic c, KnownNat n, KnownRegisterSize r) =>
Natural
-> Vector (NumberOfRegisters (BaseField c) n r) (BaseField c)
naturalToVector @c @n @r (Natural
-> Vector (NumberOfRegisters (BaseField c) n r) (BaseField c))
-> (Vector n (BaseField c) -> Natural)
-> Vector n (BaseField c)
-> Vector (NumberOfRegisters (BaseField c) n r) (BaseField c)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Natural -> BaseField c -> Natural)
-> Natural -> Vector n (BaseField c) -> Natural
forall b a. (b -> a -> b) -> b -> Vector n a -> b
forall (t :: Type -> Type) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
Haskell.foldl (\Natural
y BaseField c
p -> BaseField c -> Const (BaseField c)
forall a. ToConstant a => a -> Const a
toConstant BaseField c
p Natural -> Natural -> Natural
forall a. AdditiveSemigroup a => a -> a -> a
+ Natural
2 Natural -> Natural -> Natural
forall a. MultiplicativeSemigroup a => a -> a -> a
* Natural
y) Natural
0) Vector n i -> m (Vector (NumberOfRegisters (BaseField c) n r) i)
CircuitFun
(Vector n)
(Vector (NumberOfRegisters (BaseField c) n r))
(BaseField c)
solve
where
solve :: forall i m. MonadCircuit i (BaseField c) m => Vector n i -> m (Vector (NumberOfRegisters (BaseField c) n r) i)
solve :: CircuitFun
(Vector n)
(Vector (NumberOfRegisters (BaseField c) n r))
(BaseField c)
solve Vector n i
bits = do
let bsBits :: [i]
bsBits = Vector n i -> [i]
forall (size :: Natural) a. Vector size a -> [a]
V.fromVector Vector n i
bits
[i] -> Vector (NumberOfRegisters (BaseField c) n r) i
forall (size :: Natural) a. [a] -> Vector size a
V.unsafeToVector ([i] -> Vector (NumberOfRegisters (BaseField c) n r) i)
-> ([i] -> [i])
-> [i]
-> Vector (NumberOfRegisters (BaseField c) n r) i
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [i] -> [i]
forall a. [a] -> [a]
Haskell.reverse ([i] -> Vector (NumberOfRegisters (BaseField c) n r) i)
-> m [i] -> m (Vector (NumberOfRegisters (BaseField c) n r) i)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Natural
-> Natural
-> forall v (m :: Type -> Type).
MonadCircuit v (BaseField c) m =>
[v] -> m [v]
forall a.
Natural
-> Natural
-> forall v (m :: Type -> Type). MonadCircuit v a m => [v] -> m [v]
fromBits (forall a (n :: Natural) (r :: RegisterSize).
(Finite a, KnownNat n, KnownRegisterSize r) =>
Natural
highRegisterSize @(BaseField c) @n @r) (forall a (n :: Natural) (r :: RegisterSize).
(Finite a, KnownNat n, KnownRegisterSize r) =>
Natural
registerSize @(BaseField c) @n @r) [i]
bsBits
instance (Symbolic c, KnownNat n, KnownRegisterSize r) => Iso (UInt n r c) (ByteString n c) where
from :: UInt n r c -> ByteString n c
from (UInt c (Vector (NumberOfRegisters (BaseField c) n r))
u) = c (Vector n) -> ByteString n c
forall (n :: Natural) (context :: (Type -> Type) -> Type).
context (Vector n) -> ByteString n context
ByteString (c (Vector n) -> ByteString n c) -> c (Vector n) -> ByteString n c
forall a b. (a -> b) -> a -> b
$ c (Vector (NumberOfRegisters (BaseField c) n r))
-> (Vector (NumberOfRegisters (BaseField c) n r) (BaseField c)
-> Vector n (BaseField c))
-> CircuitFun
(Vector (NumberOfRegisters (BaseField c) n r))
(Vector n)
(BaseField c)
-> c (Vector n)
forall a (f :: Type -> Type) (g :: Type -> Type).
(BaseField c ~ a) =>
c f -> (f a -> g a) -> CircuitFun f g a -> c g
forall (c :: (Type -> Type) -> Type) a (f :: Type -> Type)
(g :: Type -> Type).
(Symbolic c, BaseField c ~ a) =>
c f -> (f a -> g a) -> CircuitFun f g a -> c g
symbolicF c (Vector (NumberOfRegisters (BaseField c) n r))
u (\ Vector (NumberOfRegisters (BaseField c) n r) (BaseField c)
v -> [BaseField c] -> Vector n (BaseField c)
forall (size :: Natural) a. [a] -> Vector size a
V.unsafeToVector ([BaseField c] -> Vector n (BaseField c))
-> [BaseField c] -> Vector n (BaseField c)
forall a b. (a -> b) -> a -> b
$ Natural -> BaseField c
forall a b. FromConstant a b => a -> b
fromConstant (Natural -> BaseField c) -> [Natural] -> [BaseField c]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Natural -> Natural -> [Natural]
toBsBits (Vector (NumberOfRegisters (BaseField c) n r) (BaseField c)
-> Natural -> Natural
forall a (n :: Natural).
(ToConstant a, Const a ~ Natural) =>
Vector n a -> Natural -> Natural
vectorToNatural Vector (NumberOfRegisters (BaseField c) n r) (BaseField c)
v (forall a (n :: Natural) (r :: RegisterSize).
(Finite a, KnownNat n, KnownRegisterSize r) =>
Natural
registerSize @(BaseField c) @n @r)) (forall (n :: Natural). KnownNat n => Natural
value @n)) Vector (NumberOfRegisters (BaseField c) n r) i -> m (Vector n i)
CircuitFun
(Vector (NumberOfRegisters (BaseField c) n r))
(Vector n)
(BaseField c)
solve
where
solve :: forall i m. MonadCircuit i (BaseField c) m => Vector (NumberOfRegisters (BaseField c) n r) i -> m (Vector n i)
solve :: CircuitFun
(Vector (NumberOfRegisters (BaseField c) n r))
(Vector n)
(BaseField c)
solve Vector (NumberOfRegisters (BaseField c) n r) i
ui = do
let regs :: [i]
regs = Vector (NumberOfRegisters (BaseField c) n r) i -> [i]
forall (size :: Natural) a. Vector size a -> [a]
V.fromVector Vector (NumberOfRegisters (BaseField c) n r) i
ui
[i] -> Vector n i
forall (size :: Natural) a. [a] -> Vector size a
V.unsafeToVector ([i] -> Vector n i) -> m [i] -> m (Vector n i)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> [i] -> Natural -> Natural -> m [i]
forall v a (m :: Type -> Type).
(MonadCircuit v a m, Arithmetic a) =>
[v] -> Natural -> Natural -> m [v]
toBits ([i] -> [i]
forall a. [a] -> [a]
Haskell.reverse [i]
regs) (forall a (n :: Natural) (r :: RegisterSize).
(Finite a, KnownNat n, KnownRegisterSize r) =>
Natural
highRegisterSize @(BaseField c) @n @r) (forall a (n :: Natural) (r :: RegisterSize).
(Finite a, KnownNat n, KnownRegisterSize r) =>
Natural
registerSize @(BaseField c) @n @r)
instance (Symbolic c, KnownRegisterSize r, NumberOfBits (BaseField c) ~ n) => Iso (FieldElement c) (UInt n r c) where
from :: FieldElement c -> UInt n r c
from FieldElement c
a = ByteString n c -> UInt n r c
forall a b. Iso a b => a -> b
from (FieldElement c -> ByteString n c
forall a b. Iso a b => a -> b
from FieldElement c
a :: ByteString n c)
instance (Symbolic c, KnownRegisterSize r, NumberOfBits (BaseField c) ~ n) => Iso (UInt n r c) (FieldElement c) where
from :: UInt n r c -> FieldElement c
from UInt n r c
a = ByteString n c -> FieldElement c
forall a b. Iso a b => a -> b
from (UInt n r c -> ByteString n c
forall a b. Iso a b => a -> b
from UInt n r c
a :: ByteString n c)
instance
( Symbolic c
, KnownNat n
, KnownNat k
, KnownRegisterSize r
, n <= k
) => Extend (UInt n r c) (UInt k r c) where
extend :: UInt n r c -> UInt k r c
extend (UInt c (Vector (NumberOfRegisters (BaseField c) n r))
x) = c (Vector (NumberOfRegisters (BaseField c) k r)) -> UInt k r c
forall (n :: Natural) (r :: RegisterSize)
(context :: (Type -> Type) -> Type).
context (Vector (NumberOfRegisters (BaseField context) n r))
-> UInt n r context
UInt (c (Vector (NumberOfRegisters (BaseField c) k r)) -> UInt k r c)
-> c (Vector (NumberOfRegisters (BaseField c) k r)) -> UInt k r c
forall a b. (a -> b) -> a -> b
$ c (Vector (NumberOfRegisters (BaseField c) n r))
-> (Vector (NumberOfRegisters (BaseField c) n r) (BaseField c)
-> Vector (NumberOfRegisters (BaseField c) k r) (BaseField c))
-> CircuitFun
(Vector (NumberOfRegisters (BaseField c) n r))
(Vector (NumberOfRegisters (BaseField c) k r))
(BaseField c)
-> c (Vector (NumberOfRegisters (BaseField c) k r))
forall a (f :: Type -> Type) (g :: Type -> Type).
(BaseField c ~ a) =>
c f -> (f a -> g a) -> CircuitFun f g a -> c g
forall (c :: (Type -> Type) -> Type) a (f :: Type -> Type)
(g :: Type -> Type).
(Symbolic c, BaseField c ~ a) =>
c f -> (f a -> g a) -> CircuitFun f g a -> c g
symbolicF c (Vector (NumberOfRegisters (BaseField c) n r))
x (\Vector (NumberOfRegisters (BaseField c) n r) (BaseField c)
l -> forall (c :: (Type -> Type) -> Type) (n :: Natural)
(r :: RegisterSize).
(Symbolic c, KnownNat n, KnownRegisterSize r) =>
Natural
-> Vector (NumberOfRegisters (BaseField c) n r) (BaseField c)
naturalToVector @c @k @r (Vector (NumberOfRegisters (BaseField c) n r) (BaseField c)
-> Natural -> Natural
forall a (n :: Natural).
(ToConstant a, Const a ~ Natural) =>
Vector n a -> Natural -> Natural
vectorToNatural Vector (NumberOfRegisters (BaseField c) n r) (BaseField c)
l (forall a (n :: Natural) (r :: RegisterSize).
(Finite a, KnownNat n, KnownRegisterSize r) =>
Natural
registerSize @(BaseField c) @n @r))) Vector (NumberOfRegisters (BaseField c) n r) i
-> m (Vector (NumberOfRegisters (BaseField c) k r) i)
CircuitFun
(Vector (NumberOfRegisters (BaseField c) n r))
(Vector (NumberOfRegisters (BaseField c) k r))
(BaseField c)
solve
where
solve :: MonadCircuit i (BaseField c) m => Vector (NumberOfRegisters (BaseField c) n r) i -> m (Vector (NumberOfRegisters (BaseField c) k r) i)
solve :: CircuitFun
(Vector (NumberOfRegisters (BaseField c) n r))
(Vector (NumberOfRegisters (BaseField c) k r))
(BaseField c)
solve Vector (NumberOfRegisters (BaseField c) n r) i
xv = do
let regs :: [i]
regs = Vector (NumberOfRegisters (BaseField c) n r) i -> [i]
forall (size :: Natural) a. Vector size a -> [a]
V.fromVector Vector (NumberOfRegisters (BaseField c) n r) i
xv
[i]
zeros <- Natural -> m i -> m [i]
forall (f :: Type -> Type) a.
Applicative f =>
Natural -> f a -> f [a]
replicateA (forall (n :: Natural). KnownNat n => Natural
value @k Natural -> Natural -> Natural
-! (forall (n :: Natural). KnownNat n => Natural
value @n)) (ClosedPoly i (BaseField c) -> m i
forall var a (m :: Type -> Type).
MonadCircuit var a m =>
ClosedPoly var a -> m var
newAssigned (x -> (i -> x) -> x
forall a b. a -> b -> a
Haskell.const x
forall a. AdditiveMonoid a => a
zero))
[i]
bsBits <- [i] -> Natural -> Natural -> m [i]
forall v a (m :: Type -> Type).
(MonadCircuit v a m, Arithmetic a) =>
[v] -> Natural -> Natural -> m [v]
toBits ([i] -> [i]
forall a. [a] -> [a]
Haskell.reverse [i]
regs) (forall a (n :: Natural) (r :: RegisterSize).
(Finite a, KnownNat n, KnownRegisterSize r) =>
Natural
highRegisterSize @(BaseField c) @n @r) (forall a (n :: Natural) (r :: RegisterSize).
(Finite a, KnownNat n, KnownRegisterSize r) =>
Natural
registerSize @(BaseField c) @n @r)
[i]
extended <- Natural
-> Natural
-> forall v (m :: Type -> Type).
MonadCircuit v (BaseField c) m =>
[v] -> m [v]
forall a.
Natural
-> Natural
-> forall v (m :: Type -> Type). MonadCircuit v a m => [v] -> m [v]
fromBits (forall a (n :: Natural) (r :: RegisterSize).
(Finite a, KnownNat n, KnownRegisterSize r) =>
Natural
highRegisterSize @(BaseField c) @k @r) (forall a (n :: Natural) (r :: RegisterSize).
(Finite a, KnownNat n, KnownRegisterSize r) =>
Natural
registerSize @(BaseField c) @k @r) ([i]
zeros [i] -> [i] -> [i]
forall a. Semigroup a => a -> a -> a
<> [i]
bsBits)
Vector (NumberOfRegisters (BaseField c) k r) i
-> m (Vector (NumberOfRegisters (BaseField c) k r) i)
forall a. a -> m a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Vector (NumberOfRegisters (BaseField c) k r) i
-> m (Vector (NumberOfRegisters (BaseField c) k r) i))
-> Vector (NumberOfRegisters (BaseField c) k r) i
-> m (Vector (NumberOfRegisters (BaseField c) k r) i)
forall a b. (a -> b) -> a -> b
$ [i] -> Vector (NumberOfRegisters (BaseField c) k r) i
forall (size :: Natural) a. [a] -> Vector size a
V.unsafeToVector ([i] -> Vector (NumberOfRegisters (BaseField c) k r) i)
-> [i] -> Vector (NumberOfRegisters (BaseField c) k r) i
forall a b. (a -> b) -> a -> b
$ [i] -> [i]
forall a. [a] -> [a]
Haskell.reverse [i]
extended
instance
( Symbolic c
, KnownNat n
, KnownNat k
, KnownRegisterSize r
, k <= n
, from ~ NumberOfRegisters (BaseField c) n r
, to ~ NumberOfRegisters (BaseField c) k r
) => Shrink (UInt n r c) (UInt k r c) where
shrink :: UInt n r c -> UInt k r c
shrink (UInt c (Vector (NumberOfRegisters (BaseField c) n r))
ac) = c (Vector (NumberOfRegisters (BaseField c) k r)) -> UInt k r c
forall (n :: Natural) (r :: RegisterSize)
(context :: (Type -> Type) -> Type).
context (Vector (NumberOfRegisters (BaseField context) n r))
-> UInt n r context
UInt (c (Vector (NumberOfRegisters (BaseField c) k r)) -> UInt k r c)
-> c (Vector (NumberOfRegisters (BaseField c) k r)) -> UInt k r c
forall a b. (a -> b) -> a -> b
$ c (Vector from)
-> (Vector from (BaseField c) -> Vector to (BaseField c))
-> CircuitFun (Vector from) (Vector to) (BaseField c)
-> c (Vector to)
forall a (f :: Type -> Type) (g :: Type -> Type).
(BaseField c ~ a) =>
c f -> (f a -> g a) -> CircuitFun f g a -> c g
forall (c :: (Type -> Type) -> Type) a (f :: Type -> Type)
(g :: Type -> Type).
(Symbolic c, BaseField c ~ a) =>
c f -> (f a -> g a) -> CircuitFun f g a -> c g
symbolicF c (Vector from)
c (Vector (NumberOfRegisters (BaseField c) n r))
ac ([BaseField c] -> Vector to (BaseField c)
forall (size :: Natural) a. [a] -> Vector size a
V.unsafeToVector ([BaseField c] -> Vector to (BaseField c))
-> (Vector from (BaseField c) -> [BaseField c])
-> Vector from (BaseField c)
-> Vector to (BaseField c)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Vector from (BaseField c) -> [BaseField c]
forall (size :: Natural) a. Vector size a -> [a]
V.fromVector ) Vector from i -> m (Vector to i)
CircuitFun (Vector from) (Vector to) (BaseField c)
solve
where
solve :: MonadCircuit i (BaseField c) m => Vector from i -> m (Vector to i)
solve :: CircuitFun (Vector from) (Vector to) (BaseField c)
solve Vector from i
xv = do
let regs :: [i]
regs = Vector from i -> [i]
forall (size :: Natural) a. Vector size a -> [a]
V.fromVector Vector from i
xv
[i]
bsBits <- [i] -> Natural -> Natural -> m [i]
forall v a (m :: Type -> Type).
(MonadCircuit v a m, Arithmetic a) =>
[v] -> Natural -> Natural -> m [v]
toBits ([i] -> [i]
forall a. [a] -> [a]
Haskell.reverse [i]
regs) (forall a (n :: Natural) (r :: RegisterSize).
(Finite a, KnownNat n, KnownRegisterSize r) =>
Natural
highRegisterSize @(BaseField c) @n @r) (forall a (n :: Natural) (r :: RegisterSize).
(Finite a, KnownNat n, KnownRegisterSize r) =>
Natural
registerSize @(BaseField c) @n @r)
[i]
shrinked <- Natural
-> Natural
-> forall v (m :: Type -> Type).
MonadCircuit v (BaseField c) m =>
[v] -> m [v]
forall a.
Natural
-> Natural
-> forall v (m :: Type -> Type). MonadCircuit v a m => [v] -> m [v]
fromBits (forall a (n :: Natural) (r :: RegisterSize).
(Finite a, KnownNat n, KnownRegisterSize r) =>
Natural
highRegisterSize @(BaseField c) @k @r) (forall a (n :: Natural) (r :: RegisterSize).
(Finite a, KnownNat n, KnownRegisterSize r) =>
Natural
registerSize @(BaseField c) @k @r) (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)
Vector to i -> m (Vector to i)
forall a. a -> m a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Vector to i -> m (Vector to i)) -> Vector to i -> m (Vector to i)
forall a b. (a -> b) -> a -> b
$ [i] -> Vector to i
forall (size :: Natural) a. [a] -> Vector size a
V.unsafeToVector ([i] -> Vector to i) -> [i] -> Vector to i
forall a b. (a -> b) -> a -> b
$ [i] -> [i]
forall a. [a] -> [a]
Haskell.reverse [i]
shrinked
instance
( Symbolic c
, KnownNat n
, KnownNat r
, KnownRegisterSize rs
, r ~ NumberOfRegisters (BaseField c) n rs
, NFData (c (Vector r))
) => SemiEuclidean (UInt n rs c) where
divMod :: UInt n rs c -> UInt n rs c -> (UInt n rs c, UInt n rs c)
divMod UInt n rs c
numerator UInt n rs c
d = forall b a. Conditional b a => a -> a -> b -> a
bool @(Bool c) (UInt n rs c
q, UInt n rs c
r) (UInt n rs c
forall a. AdditiveMonoid a => a
zero, UInt n rs c
forall a. AdditiveMonoid a => a
zero) (UInt n rs c
d UInt n rs c -> UInt n rs c -> Bool c
forall b a. Eq b a => a -> a -> b
== UInt n rs c
forall a. AdditiveMonoid a => a
zero)
where
(UInt n rs c
q, UInt n rs c
r) = ((UInt n rs c, UInt n rs c)
-> Natural -> (UInt n rs c, UInt n rs c))
-> (UInt n rs c, UInt n rs c)
-> [Natural]
-> (UInt n rs c, UInt n rs c)
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: Type -> Type) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
Haskell.foldl (UInt n rs c, UInt n rs c) -> Natural -> (UInt n rs c, UInt n rs c)
longDivisionStep (UInt n rs c
forall a. AdditiveMonoid a => a
zero, UInt n rs c
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 :: ByteString n c
numeratorBits :: ByteString n c
numeratorBits = UInt n rs c -> ByteString n c
forall a b. Iso a b => a -> b
from UInt n rs c
numerator
addBit :: UInt n rs c -> Natural -> UInt n rs c
addBit :: UInt n rs c -> Natural -> UInt n rs c
addBit UInt n rs c
ui Natural
bs = UInt n rs c
ui UInt n rs c -> UInt n rs c -> UInt n rs c
forall a. AdditiveSemigroup a => a -> a -> a
+ forall b a. Conditional b a => a -> a -> b -> a
bool @(Bool c) UInt n rs c
forall a. AdditiveMonoid a => a
zero UInt n rs c
forall a. MultiplicativeMonoid a => a
one (ByteString n c -> Natural -> Bool c
forall (c :: (Type -> Type) -> Type) (n :: Natural).
Symbolic c =>
ByteString n c -> Natural -> Bool c
isSet ByteString n c
numeratorBits Natural
bs)
longDivisionStep
:: (UInt n rs c, UInt n rs c)
-> Natural
-> (UInt n rs c, UInt n rs c)
longDivisionStep :: (UInt n rs c, UInt n rs c) -> Natural -> (UInt n rs c, UInt n rs c)
longDivisionStep (UInt n rs c
q', UInt n rs c
r') Natural
i =
let rs :: UInt n rs c
rs = UInt n rs c -> UInt n rs c
forall a. NFData a => a -> a
force (UInt n rs c -> UInt n rs c) -> UInt n rs c -> UInt n rs c
forall a b. (a -> b) -> a -> b
$ UInt n rs c -> Natural -> UInt n rs c
addBit (UInt n rs c
r' UInt n rs c -> UInt n rs c -> UInt n rs c
forall a. AdditiveSemigroup a => a -> a -> a
+ UInt n rs c
r') (forall (n :: Natural). KnownNat n => Natural
value @n Natural -> Natural -> Natural
-! Natural
i Natural -> Natural -> Natural
-! Natural
1)
in forall b a. Conditional b a => a -> a -> b -> a
bool @(Bool c) (UInt n rs c
q', UInt n rs c
rs) (UInt n rs c
q' UInt n rs c -> UInt n rs c -> UInt n rs c
forall a. AdditiveSemigroup a => a -> a -> a
+ Natural -> UInt n rs c
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 rs c
rs UInt n rs c -> UInt n rs c -> UInt n rs c
forall a. AdditiveGroup a => a -> a -> a
- UInt n rs c
d) (UInt n rs c
rs UInt n rs c -> UInt n rs c -> Bool c
forall b a. Ord b a => a -> a -> b
>= UInt n rs c
d)
instance ( Symbolic c, KnownNat n, KnownRegisterSize r
, KnownNat (NumberOfRegisters (BaseField c) n r)
) => Ord (Bool c) (UInt n r c) where
UInt n r c
x <= :: UInt n r c -> UInt n r c -> Bool c
<= UInt n r c
y = UInt n r c
y UInt n r c -> UInt n r c -> Bool c
forall b a. Ord b a => a -> a -> b
>= UInt n r c
x
UInt n r c
x < :: UInt n r c -> UInt n r c -> Bool c
< UInt n r c
y = UInt n r c
y UInt n r c -> UInt n r c -> Bool c
forall b a. Ord b a => a -> a -> b
> UInt n r c
x
UInt n r c
u1 >= :: UInt n r c -> UInt n r c -> Bool c
>= UInt n r c
u2 =
let ByteString c (Vector n)
rs1 = UInt n r c -> ByteString n c
forall a b. Iso a b => a -> b
from UInt n r c
u1 :: ByteString n c
ByteString c (Vector n)
rs2 = UInt n r c -> ByteString n c
forall a b. Iso a b => a -> b
from UInt n r c
u2 :: ByteString n c
in forall (r :: Natural) (c :: (Type -> Type) -> Type)
(f :: Type -> Type).
(Symbolic c, Zip f, Foldable f, KnownNat r) =>
c f -> c f -> Bool c
bitwiseGE @1 c (Vector n)
rs1 c (Vector n)
rs2
UInt n r c
u1 > :: UInt n r c -> UInt n r c -> Bool c
> UInt n r c
u2 =
let ByteString c (Vector n)
rs1 = UInt n r c -> ByteString n c
forall a b. Iso a b => a -> b
from UInt n r c
u1 :: ByteString n c
ByteString c (Vector n)
rs2 = UInt n r c -> ByteString n c
forall a b. Iso a b => a -> b
from UInt n r c
u2 :: ByteString n c
in forall (r :: Natural) (c :: (Type -> Type) -> Type)
(f :: Type -> Type).
(Symbolic c, Zip f, Foldable f, KnownNat r) =>
c f -> c f -> Bool c
bitwiseGT @1 c (Vector n)
rs1 c (Vector n)
rs2
max :: UInt n r c -> UInt n r c -> UInt n r c
max UInt n r c
x UInt n r c
y = forall b a. Conditional b a => a -> a -> b -> a
bool @(Bool c) UInt n r c
x UInt n r c
y (Bool c -> UInt n r c) -> Bool c -> UInt n r c
forall a b. (a -> b) -> a -> b
$ UInt n r c
x UInt n r c -> UInt n r c -> Bool c
forall b a. Ord b a => a -> a -> b
< UInt n r c
y
min :: UInt n r c -> UInt n r c -> UInt n r c
min UInt n r c
x UInt n r c
y = forall b a. Conditional b a => a -> a -> b -> a
bool @(Bool c) UInt n r c
x UInt n r c
y (Bool c -> UInt n r c) -> Bool c -> UInt n r c
forall a b. (a -> b) -> a -> b
$ UInt n r c
x UInt n r c -> UInt n r c -> Bool c
forall b a. Ord b a => a -> a -> b
> UInt n r c
y
instance (Symbolic c, KnownNat n, KnownRegisterSize r) => AdditiveSemigroup (UInt n r c) where
UInt c (Vector (NumberOfRegisters (BaseField c) n r))
xc + :: UInt n r c -> UInt n r c -> UInt n r c
+ UInt c (Vector (NumberOfRegisters (BaseField c) n r))
yc = c (Vector (NumberOfRegisters (BaseField c) n r)) -> UInt n r c
forall (n :: Natural) (r :: RegisterSize)
(context :: (Type -> Type) -> Type).
context (Vector (NumberOfRegisters (BaseField context) n r))
-> UInt n r context
UInt (c (Vector (NumberOfRegisters (BaseField c) n r)) -> UInt n r c)
-> c (Vector (NumberOfRegisters (BaseField c) n r)) -> UInt n r c
forall a b. (a -> b) -> a -> b
$ c (Vector (NumberOfRegisters (BaseField c) n r))
-> c (Vector (NumberOfRegisters (BaseField c) n r))
-> (Vector (NumberOfRegisters (BaseField c) n r) (BaseField c)
-> Vector (NumberOfRegisters (BaseField c) n r) (BaseField c)
-> Vector (NumberOfRegisters (BaseField c) n r) (BaseField c))
-> (forall i (m :: Type -> Type).
MonadCircuit i (BaseField c) m =>
Vector (NumberOfRegisters (BaseField c) n r) i
-> Vector (NumberOfRegisters (BaseField c) n r) i
-> m (Vector (NumberOfRegisters (BaseField c) n r) i))
-> c (Vector (NumberOfRegisters (BaseField c) n r))
forall (c :: (Type -> Type) -> Type) a (f :: Type -> Type)
(g :: Type -> Type) (h :: Type -> Type).
(Symbolic c, BaseField c ~ a) =>
c f
-> c g
-> (f a -> g a -> h a)
-> (forall i (m :: Type -> Type).
MonadCircuit i a m =>
f i -> g i -> m (h i))
-> c h
symbolic2F c (Vector (NumberOfRegisters (BaseField c) n r))
xc c (Vector (NumberOfRegisters (BaseField c) n r))
yc (\Vector (NumberOfRegisters (BaseField c) n r) (BaseField c)
u Vector (NumberOfRegisters (BaseField c) n r) (BaseField c)
v -> forall (c :: (Type -> Type) -> Type) (n :: Natural)
(r :: RegisterSize).
(Symbolic c, KnownNat n, KnownRegisterSize r) =>
Natural
-> Vector (NumberOfRegisters (BaseField c) n r) (BaseField c)
naturalToVector @c @n @r (Natural
-> Vector (NumberOfRegisters (BaseField c) n r) (BaseField c))
-> Natural
-> Vector (NumberOfRegisters (BaseField c) n r) (BaseField c)
forall a b. (a -> b) -> a -> b
$ Vector (NumberOfRegisters (BaseField c) n r) (BaseField c)
-> Natural -> Natural
forall a (n :: Natural).
(ToConstant a, Const a ~ Natural) =>
Vector n a -> Natural -> Natural
vectorToNatural Vector (NumberOfRegisters (BaseField c) n r) (BaseField c)
u (forall a (n :: Natural) (r :: RegisterSize).
(Finite a, KnownNat n, KnownRegisterSize r) =>
Natural
registerSize @(BaseField c) @n @r) Natural -> Natural -> Natural
forall a. AdditiveSemigroup a => a -> a -> a
+ Vector (NumberOfRegisters (BaseField c) n r) (BaseField c)
-> Natural -> Natural
forall a (n :: Natural).
(ToConstant a, Const a ~ Natural) =>
Vector n a -> Natural -> Natural
vectorToNatural Vector (NumberOfRegisters (BaseField c) n r) (BaseField c)
v (forall a (n :: Natural) (r :: RegisterSize).
(Finite a, KnownNat n, KnownRegisterSize r) =>
Natural
registerSize @(BaseField c) @n @r)) Vector (NumberOfRegisters (BaseField c) n r) i
-> Vector (NumberOfRegisters (BaseField c) n r) i
-> m (Vector (NumberOfRegisters (BaseField c) n r) i)
forall i (m :: Type -> Type).
MonadCircuit i (BaseField c) m =>
Vector (NumberOfRegisters (BaseField c) n r) i
-> Vector (NumberOfRegisters (BaseField c) n r) i
-> m (Vector (NumberOfRegisters (BaseField c) n r) i)
solve
where
solve :: MonadCircuit i (BaseField c) m => Vector (NumberOfRegisters (BaseField c) n r) i -> Vector (NumberOfRegisters (BaseField c) n r) i -> m (Vector (NumberOfRegisters (BaseField c) n r) i)
solve :: forall i (m :: Type -> Type).
MonadCircuit i (BaseField c) m =>
Vector (NumberOfRegisters (BaseField c) n r) i
-> Vector (NumberOfRegisters (BaseField c) n r) i
-> m (Vector (NumberOfRegisters (BaseField c) n r) i)
solve Vector (NumberOfRegisters (BaseField c) n r) i
xv Vector (NumberOfRegisters (BaseField c) n r) i
yv = do
i
j <- ClosedPoly i (BaseField c) -> m i
forall var a (m :: Type -> Type).
MonadCircuit var a m =>
ClosedPoly var a -> m var
newAssigned (x -> (i -> x) -> x
forall a b. a -> b -> a
Haskell.const x
forall a. AdditiveMonoid a => a
zero)
let xs :: [i]
xs = Vector (NumberOfRegisters (BaseField c) n r) i -> [i]
forall (size :: Natural) a. Vector size a -> [a]
V.fromVector Vector (NumberOfRegisters (BaseField c) n r) i
xv
ys :: [i]
ys = Vector (NumberOfRegisters (BaseField c) n r) i -> [i]
forall (size :: Natural) a. Vector size a -> [a]
V.fromVector Vector (NumberOfRegisters (BaseField c) n r) i
yv
midx :: [i]
midx = [i] -> [i]
forall a. HasCallStack => [a] -> [a]
Haskell.init [i]
xs
z :: i
z = [i] -> i
forall a. HasCallStack => [a] -> a
Haskell.last [i]
xs
midy :: [i]
midy = [i] -> [i]
forall a. HasCallStack => [a] -> [a]
Haskell.init [i]
ys
w :: i
w = [i] -> i
forall a. HasCallStack => [a] -> a
Haskell.last [i]
ys
([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
$
(i -> i -> i -> m (i, i)) -> [i] -> [i] -> [i -> m (i, i)]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
Haskell.zipWith (Natural -> i -> i -> i -> m (i, i)
forall a i (m :: Type -> Type).
(Arithmetic a, MonadCircuit i a m) =>
Natural -> i -> i -> i -> m (i, i)
fullAdder (Natural -> i -> i -> i -> m (i, i))
-> Natural -> i -> i -> i -> m (i, i)
forall a b. (a -> b) -> a -> b
$ forall a (n :: Natural) (r :: RegisterSize).
(Finite a, KnownNat n, KnownRegisterSize r) =>
Natural
registerSize @(BaseField c) @n @r) [i]
midx [i]
midy
i
k <- i -> i -> i -> m i
forall i a (m :: Type -> Type).
MonadCircuit i a m =>
i -> i -> i -> m i
fullAdded i
z i
w i
c
(i
ks, i
_) <- Natural -> Natural -> i -> m (i, i)
forall i a (m :: Type -> Type).
(MonadCircuit i a m, Arithmetic a) =>
Natural -> Natural -> i -> m (i, i)
splitExpansion (forall a (n :: Natural) (r :: RegisterSize).
(Finite a, KnownNat n, KnownRegisterSize r) =>
Natural
highRegisterSize @(BaseField c) @n @r) Natural
1 i
k
Vector (NumberOfRegisters (BaseField c) n r) i
-> m (Vector (NumberOfRegisters (BaseField c) n r) i)
forall a. a -> m a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Vector (NumberOfRegisters (BaseField c) n r) i
-> m (Vector (NumberOfRegisters (BaseField c) n r) i))
-> Vector (NumberOfRegisters (BaseField c) n r) i
-> m (Vector (NumberOfRegisters (BaseField c) n r) i)
forall a b. (a -> b) -> a -> b
$ [i] -> Vector (NumberOfRegisters (BaseField c) n r) i
forall (size :: Natural) a. [a] -> Vector size a
V.unsafeToVector ([i]
zs [i] -> [i] -> [i]
forall a. [a] -> [a] -> [a]
++ [i
ks])
instance (Symbolic c, KnownNat n, KnownRegisterSize r) => AdditiveMonoid (UInt n r c) where
zero :: UInt n r c
zero = Natural -> UInt n r c
forall a b. FromConstant a b => a -> b
fromConstant (Natural
0:: Natural)
instance
(Symbolic c
, KnownNat n
, KnownRegisterSize r
) => AdditiveGroup (UInt n r c) where
UInt c (Vector (NumberOfRegisters (BaseField c) n r))
x - :: UInt n r c -> UInt n r c -> UInt n r c
- UInt c (Vector (NumberOfRegisters (BaseField c) n r))
y = c (Vector (NumberOfRegisters (BaseField c) n r)) -> UInt n r c
forall (n :: Natural) (r :: RegisterSize)
(context :: (Type -> Type) -> Type).
context (Vector (NumberOfRegisters (BaseField context) n r))
-> UInt n r context
UInt (c (Vector (NumberOfRegisters (BaseField c) n r)) -> UInt n r c)
-> c (Vector (NumberOfRegisters (BaseField c) n r)) -> UInt n r c
forall a b. (a -> b) -> a -> b
$ c (Vector (NumberOfRegisters (BaseField c) n r))
-> c (Vector (NumberOfRegisters (BaseField c) n r))
-> (Vector (NumberOfRegisters (BaseField c) n r) (BaseField c)
-> Vector (NumberOfRegisters (BaseField c) n r) (BaseField c)
-> Vector (NumberOfRegisters (BaseField c) n r) (BaseField c))
-> (forall i (m :: Type -> Type).
MonadCircuit i (BaseField c) m =>
Vector (NumberOfRegisters (BaseField c) n r) i
-> Vector (NumberOfRegisters (BaseField c) n r) i
-> m (Vector (NumberOfRegisters (BaseField c) n r) i))
-> c (Vector (NumberOfRegisters (BaseField c) n r))
forall (c :: (Type -> Type) -> Type) a (f :: Type -> Type)
(g :: Type -> Type) (h :: Type -> Type).
(Symbolic c, BaseField c ~ a) =>
c f
-> c g
-> (f a -> g a -> h a)
-> (forall i (m :: Type -> Type).
MonadCircuit i a m =>
f i -> g i -> m (h i))
-> c h
symbolic2F c (Vector (NumberOfRegisters (BaseField c) n r))
x c (Vector (NumberOfRegisters (BaseField c) n r))
y (\Vector (NumberOfRegisters (BaseField c) n r) (BaseField c)
u Vector (NumberOfRegisters (BaseField c) n r) (BaseField c)
v -> forall (c :: (Type -> Type) -> Type) (n :: Natural)
(r :: RegisterSize).
(Symbolic c, KnownNat n, KnownRegisterSize r) =>
Natural
-> Vector (NumberOfRegisters (BaseField c) n r) (BaseField c)
naturalToVector @c @n @r (Natural
-> Vector (NumberOfRegisters (BaseField c) n r) (BaseField c))
-> Natural
-> Vector (NumberOfRegisters (BaseField c) n r) (BaseField c)
forall a b. (a -> b) -> a -> b
$ Vector (NumberOfRegisters (BaseField c) n r) (BaseField c)
-> Natural -> Natural
forall a (n :: Natural).
(ToConstant a, Const a ~ Natural) =>
Vector n a -> Natural -> Natural
vectorToNatural Vector (NumberOfRegisters (BaseField c) n r) (BaseField c)
u (forall a (n :: Natural) (r :: RegisterSize).
(Finite a, KnownNat n, KnownRegisterSize r) =>
Natural
registerSize @(BaseField c) @n @r) 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
value @n) Natural -> Natural -> Natural
-! Vector (NumberOfRegisters (BaseField c) n r) (BaseField c)
-> Natural -> Natural
forall a (n :: Natural).
(ToConstant a, Const a ~ Natural) =>
Vector n a -> Natural -> Natural
vectorToNatural Vector (NumberOfRegisters (BaseField c) n r) (BaseField c)
v (forall a (n :: Natural) (r :: RegisterSize).
(Finite a, KnownNat n, KnownRegisterSize r) =>
Natural
registerSize @(BaseField c) @n @r) ) Vector (NumberOfRegisters (BaseField c) n r) i
-> Vector (NumberOfRegisters (BaseField c) n r) i
-> m (Vector (NumberOfRegisters (BaseField c) n r) i)
forall i (m :: Type -> Type).
MonadCircuit i (BaseField c) m =>
Vector (NumberOfRegisters (BaseField c) n r) i
-> Vector (NumberOfRegisters (BaseField c) n r) i
-> m (Vector (NumberOfRegisters (BaseField c) n r) i)
solve
where
t :: BaseField c
t :: BaseField c
t = (BaseField c
forall a. MultiplicativeMonoid a => a
one BaseField c -> BaseField c -> BaseField c
forall a. AdditiveSemigroup a => a -> a -> a
+ BaseField c
forall a. MultiplicativeMonoid a => a
one) BaseField c -> Natural -> BaseField c
forall a b. Exponent a b => a -> b -> a
^ forall a (n :: Natural) (r :: RegisterSize).
(Finite a, KnownNat n, KnownRegisterSize r) =>
Natural
registerSize @(BaseField c) @n @r BaseField c -> BaseField c -> BaseField c
forall a. AdditiveGroup a => a -> a -> a
- BaseField c
forall a. MultiplicativeMonoid a => a
one
solve :: forall i m. (MonadCircuit i (BaseField c) m) => Vector (NumberOfRegisters (BaseField c) n r) i -> Vector (NumberOfRegisters (BaseField c) n r) i -> m (Vector (NumberOfRegisters (BaseField c) n r) i)
solve :: forall i (m :: Type -> Type).
MonadCircuit i (BaseField c) m =>
Vector (NumberOfRegisters (BaseField c) n r) i
-> Vector (NumberOfRegisters (BaseField c) n r) i
-> m (Vector (NumberOfRegisters (BaseField c) n r) i)
solve Vector (NumberOfRegisters (BaseField c) n r) i
xv Vector (NumberOfRegisters (BaseField c) n r) i
yv = do
let is :: [i]
is = Vector (NumberOfRegisters (BaseField c) n r) i -> [i]
forall (size :: Natural) a. Vector size a -> [a]
V.fromVector Vector (NumberOfRegisters (BaseField c) n r) i
xv
js :: [i]
js = Vector (NumberOfRegisters (BaseField c) n r) i -> [i]
forall (size :: Natural) a. Vector size a -> [a]
V.fromVector Vector (NumberOfRegisters (BaseField c) n r) i
yv
case [i] -> [i] -> [(i, i)]
forall a b. [a] -> [b] -> [(a, b)]
forall (f :: Type -> Type) a b. Zip f => f a -> f b -> f (a, b)
Z.zip [i]
is [i]
js of
[] -> Vector (NumberOfRegisters (BaseField c) n r) i
-> m (Vector (NumberOfRegisters (BaseField c) n r) i)
forall a. a -> m a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Vector (NumberOfRegisters (BaseField c) n r) i
-> m (Vector (NumberOfRegisters (BaseField c) n r) i))
-> Vector (NumberOfRegisters (BaseField c) n r) i
-> m (Vector (NumberOfRegisters (BaseField c) n r) i)
forall a b. (a -> b) -> a -> b
$ [i] -> Vector (NumberOfRegisters (BaseField c) n r) i
forall (size :: Natural) a. [a] -> Vector size a
V.unsafeToVector []
[(i
i, i
j)] -> [i] -> Vector (NumberOfRegisters (BaseField c) n r) i
forall (size :: Natural) a. [a] -> Vector size a
V.unsafeToVector ([i] -> Vector (NumberOfRegisters (BaseField c) n r) i)
-> m [i] -> m (Vector (NumberOfRegisters (BaseField c) n r) i)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> i -> i -> m [i]
forall i (m :: Type -> Type).
MonadCircuit i (BaseField c) m =>
i -> i -> m [i]
solve1 i
i i
j
((i
i, i
j) : [(i, i)]
rest) -> let (i
z, i
w) = [(i, i)] -> (i, i)
forall a. HasCallStack => [a] -> a
Haskell.last [(i, i)]
rest
([i]
ris, [i]
rjs) = [(i, i)] -> ([i], [i])
forall a b. [(a, b)] -> ([a], [b])
Haskell.unzip ([(i, i)] -> ([i], [i])) -> [(i, i)] -> ([i], [i])
forall a b. (a -> b) -> a -> b
$ [(i, i)] -> [(i, i)]
forall a. HasCallStack => [a] -> [a]
Haskell.init [(i, i)]
rest
in [i] -> Vector (NumberOfRegisters (BaseField c) n r) i
forall (size :: Natural) a. [a] -> Vector size a
V.unsafeToVector ([i] -> Vector (NumberOfRegisters (BaseField c) n r) i)
-> m [i] -> m (Vector (NumberOfRegisters (BaseField c) n r) i)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> (i, i) -> ([i], [i]) -> (i, i) -> m [i]
forall i (m :: Type -> Type).
MonadCircuit i (BaseField c) m =>
(i, i) -> ([i], [i]) -> (i, i) -> m [i]
solveN (i
i, i
j) ([i]
ris, [i]
rjs) (i
z, i
w)
solve1 :: MonadCircuit i (BaseField c) m => i -> i -> m [i]
solve1 :: forall i (m :: Type -> Type).
MonadCircuit i (BaseField c) m =>
i -> i -> m [i]
solve1 i
i i
j = do
i
z0 <- ClosedPoly i (BaseField c) -> m i
forall var a (m :: Type -> Type).
MonadCircuit var a m =>
ClosedPoly var a -> m var
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) (r :: RegisterSize).
(Finite a, KnownNat n, KnownRegisterSize r) =>
Natural
registerSize @(BaseField c) @n @r :: Natural))
(i
z, i
_) <- Natural -> Natural -> i -> m (i, i)
forall i a (m :: Type -> Type).
(MonadCircuit i a m, Arithmetic a) =>
Natural -> Natural -> i -> m (i, i)
splitExpansion (forall a (n :: Natural) (r :: RegisterSize).
(Finite a, KnownNat n, KnownRegisterSize r) =>
Natural
highRegisterSize @(BaseField c) @n @r) 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]
solveN :: MonadCircuit i (BaseField c) m => (i, i) -> ([i], [i]) -> (i, i) -> m [i]
solveN :: forall i (m :: Type -> Type).
MonadCircuit i (BaseField c) m =>
(i, i) -> ([i], [i]) -> (i, i) -> m [i]
solveN (i
i, i
j) ([i]
is, [i]
js) (i
i', i
j') = do
i
s <- ClosedPoly i (BaseField c) -> m i
forall var a (m :: Type -> Type).
MonadCircuit var a m =>
ClosedPoly var a -> m var
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
+ BaseField c -> x
forall a b. FromConstant a b => a -> b
fromConstant (BaseField c
t BaseField c -> BaseField c -> BaseField c
forall a. AdditiveSemigroup a => a -> a -> a
+ BaseField c
forall a. MultiplicativeMonoid a => a
one))
(i
k, i
b0) <- Natural -> Natural -> i -> m (i, i)
forall i a (m :: Type -> Type).
(MonadCircuit i a m, Arithmetic a) =>
Natural -> Natural -> i -> m (i, i)
splitExpansion (forall a (n :: Natural) (r :: RegisterSize).
(Finite a, KnownNat n, KnownRegisterSize r) =>
Natural
registerSize @(BaseField c) @n @r) 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 ((i -> i -> i -> m (i, i)) -> [i] -> [i] -> [i -> m (i, i)]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
Haskell.zipWith i -> i -> i -> m (i, i)
forall i (m :: Type -> Type).
MonadCircuit i (BaseField c) m =>
i -> i -> i -> m (i, i)
fullSub [i]
is [i]
js)
i
d <- ClosedPoly i (BaseField c) -> m i
forall var a (m :: Type -> Type).
MonadCircuit var a m =>
ClosedPoly var a -> m var
newAssigned (\i -> x
v -> i -> x
v i
i' x -> x -> x
forall a. AdditiveGroup a => a -> a -> a
- i -> x
v i
j')
i
s'0 <- ClosedPoly i (BaseField c) -> m i
forall var a (m :: Type -> Type).
MonadCircuit var a m =>
ClosedPoly var a -> m var
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
+ BaseField c -> x
forall a b. FromConstant a b => a -> b
fromConstant BaseField c
t)
(i
s', i
_) <- Natural -> Natural -> i -> m (i, i)
forall i a (m :: Type -> Type).
(MonadCircuit i a m, Arithmetic a) =>
Natural -> Natural -> i -> m (i, i)
splitExpansion (forall a (n :: Natural) (r :: RegisterSize).
(Finite a, KnownNat n, KnownRegisterSize r) =>
Natural
highRegisterSize @(BaseField c) @n @r) 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
k i -> [i] -> [i]
forall a. a -> [a] -> [a]
: [i]
zs [i] -> [i] -> [i]
forall a. Semigroup a => a -> a -> a
<> [i
s'])
fullSub :: MonadCircuit i (BaseField c) m => i -> i -> i -> m (i, i)
fullSub :: forall i (m :: Type -> Type).
MonadCircuit i (BaseField c) m =>
i -> i -> i -> m (i, i)
fullSub i
xk i
yk i
b = do
i
d <- ClosedPoly i (BaseField c) -> m i
forall var a (m :: Type -> Type).
MonadCircuit var a m =>
ClosedPoly var a -> m var
newAssigned (\i -> x
v -> i -> x
v i
xk x -> x -> x
forall a. AdditiveGroup a => a -> a -> a
- i -> x
v i
yk)
i
s <- ClosedPoly i (BaseField c) -> m i
forall var a (m :: Type -> Type).
MonadCircuit var a m =>
ClosedPoly var a -> m var
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
+ BaseField c -> x
forall a b. FromConstant a b => a -> b
fromConstant BaseField c
t)
Natural -> Natural -> i -> m (i, i)
forall i a (m :: Type -> Type).
(MonadCircuit i a m, Arithmetic a) =>
Natural -> Natural -> i -> m (i, i)
splitExpansion (forall a (n :: Natural) (r :: RegisterSize).
(Finite a, KnownNat n, KnownRegisterSize r) =>
Natural
registerSize @(BaseField c) @n @r) Natural
1 i
s
negate :: UInt n r c -> UInt n r c
negate :: UInt n r c -> UInt n r c
negate (UInt c (Vector (NumberOfRegisters (BaseField c) n r))
x) = c (Vector (NumberOfRegisters (BaseField c) n r)) -> UInt n r c
forall (n :: Natural) (r :: RegisterSize)
(context :: (Type -> Type) -> Type).
context (Vector (NumberOfRegisters (BaseField context) n r))
-> UInt n r context
UInt (c (Vector (NumberOfRegisters (BaseField c) n r)) -> UInt n r c)
-> c (Vector (NumberOfRegisters (BaseField c) n r)) -> UInt n r c
forall a b. (a -> b) -> a -> b
$ c (Vector (NumberOfRegisters (BaseField c) n r))
-> (Vector (NumberOfRegisters (BaseField c) n r) (BaseField c)
-> Vector (NumberOfRegisters (BaseField c) n r) (BaseField c))
-> CircuitFun
(Vector (NumberOfRegisters (BaseField c) n r))
(Vector (NumberOfRegisters (BaseField c) n r))
(BaseField c)
-> c (Vector (NumberOfRegisters (BaseField c) n r))
forall a (f :: Type -> Type) (g :: Type -> Type).
(BaseField c ~ a) =>
c f -> (f a -> g a) -> CircuitFun f g a -> c g
forall (c :: (Type -> Type) -> Type) a (f :: Type -> Type)
(g :: Type -> Type).
(Symbolic c, BaseField c ~ a) =>
c f -> (f a -> g a) -> CircuitFun f g a -> c g
symbolicF c (Vector (NumberOfRegisters (BaseField c) n r))
x (\Vector (NumberOfRegisters (BaseField c) n r) (BaseField c)
v -> forall (c :: (Type -> Type) -> Type) (n :: Natural)
(r :: RegisterSize).
(Symbolic c, KnownNat n, KnownRegisterSize r) =>
Natural
-> Vector (NumberOfRegisters (BaseField c) n r) (BaseField c)
naturalToVector @c @n @r (Natural
-> Vector (NumberOfRegisters (BaseField c) n r) (BaseField c))
-> Natural
-> Vector (NumberOfRegisters (BaseField c) n r) (BaseField c)
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
value @n) ) Natural -> Natural -> Natural
-! Vector (NumberOfRegisters (BaseField c) n r) (BaseField c)
-> Natural -> Natural
forall a (n :: Natural).
(ToConstant a, Const a ~ Natural) =>
Vector n a -> Natural -> Natural
vectorToNatural Vector (NumberOfRegisters (BaseField c) n r) (BaseField c)
v (forall a (n :: Natural) (r :: RegisterSize).
(Finite a, KnownNat n, KnownRegisterSize r) =>
Natural
registerSize @(BaseField c) @n @r)) Vector (NumberOfRegisters (BaseField c) n r) i
-> m (Vector (NumberOfRegisters (BaseField c) n r) i)
CircuitFun
(Vector (NumberOfRegisters (BaseField c) n r))
(Vector (NumberOfRegisters (BaseField c) n r))
(BaseField c)
solve
where
solve :: MonadCircuit i (BaseField c) m => Vector (NumberOfRegisters (BaseField c) n r) i -> m (Vector (NumberOfRegisters (BaseField c) n r) i)
solve :: CircuitFun
(Vector (NumberOfRegisters (BaseField c) n r))
(Vector (NumberOfRegisters (BaseField c) n r))
(BaseField c)
solve Vector (NumberOfRegisters (BaseField c) n r) i
xv = do
i
j <- ClosedPoly i (BaseField c) -> m i
forall var a (m :: Type -> Type).
MonadCircuit var a m =>
ClosedPoly var a -> m var
newAssigned (x -> (i -> x) -> x
forall a b. a -> b -> a
Haskell.const x
forall a. AdditiveMonoid a => a
zero)
let xs :: [i]
xs = Vector (NumberOfRegisters (BaseField c) n r) i -> [i]
forall (size :: Natural) a. Vector size a -> [a]
V.fromVector Vector (NumberOfRegisters (BaseField c) n r) i
xv
y :: Natural
y = Natural
2 Natural -> Natural -> Natural
forall a b. Exponent a b => a -> b -> a
^ forall a (n :: Natural) (r :: RegisterSize).
(Finite a, KnownNat n, KnownRegisterSize r) =>
Natural
registerSize @(BaseField c) @n @r
ys :: [Natural]
ys = Natural -> Natural -> [Natural]
forall a. Natural -> a -> [a]
replicate (forall a (n :: Natural) (r :: RegisterSize).
(Finite a, KnownNat n, KnownRegisterSize r) =>
Natural
numberOfRegisters @(BaseField c) @n @r Natural -> Natural -> Natural
-! Natural
2) (Natural
2 Natural -> Natural -> Natural
forall a b. Exponent a b => a -> b -> a
^ forall a (n :: Natural) (r :: RegisterSize).
(Finite a, KnownNat n, KnownRegisterSize r) =>
Natural
registerSize @(BaseField c) @n @r Natural -> Natural -> Natural
-! Natural
1)
y' :: Natural
y' = Natural
2 Natural -> Natural -> Natural
forall a b. Exponent a b => a -> b -> a
^ forall a (n :: Natural) (r :: RegisterSize).
(Finite a, KnownNat n, KnownRegisterSize r) =>
Natural
highRegisterSize @(BaseField c) @n @r Natural -> Natural -> Natural
-! Natural
1
ns :: [Natural]
ns
| forall a (n :: Natural) (r :: RegisterSize).
(Finite a, KnownNat n, KnownRegisterSize r) =>
Natural
numberOfRegisters @(BaseField c) @n @r Natural -> Natural -> Bool
forall a. Eq a => a -> a -> Bool
Haskell.== Natural
1 = [Natural
y' Natural -> Natural -> Natural
forall a. AdditiveSemigroup a => a -> a -> a
+ Natural
1]
| Bool
otherwise = (Natural
y Natural -> [Natural] -> [Natural]
forall a. a -> [a] -> [a]
: [Natural]
ys) [Natural] -> [Natural] -> [Natural]
forall a. Semigroup a => a -> a -> a
<> [Natural
y']
([i]
zs, i
_) <- (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 ((Natural -> i -> i -> m (i, i))
-> [Natural] -> [i] -> [i -> m (i, i)]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
Haskell.zipWith Natural -> i -> i -> m (i, i)
forall i (m :: Type -> Type).
MonadCircuit i (BaseField c) m =>
Natural -> i -> i -> m (i, i)
negateN [Natural]
ns [i]
xs)
Vector (NumberOfRegisters (BaseField c) n r) i
-> m (Vector (NumberOfRegisters (BaseField c) n r) i)
forall a. a -> m a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Vector (NumberOfRegisters (BaseField c) n r) i
-> m (Vector (NumberOfRegisters (BaseField c) n r) i))
-> Vector (NumberOfRegisters (BaseField c) n r) i
-> m (Vector (NumberOfRegisters (BaseField c) n r) i)
forall a b. (a -> b) -> a -> b
$ [i] -> Vector (NumberOfRegisters (BaseField c) n r) i
forall (size :: Natural) a. [a] -> Vector size a
V.unsafeToVector [i]
zs
negateN :: MonadCircuit i (BaseField c) m => Natural -> i -> i -> m (i, i)
negateN :: forall i (m :: Type -> Type).
MonadCircuit i (BaseField c) m =>
Natural -> i -> i -> m (i, i)
negateN Natural
n i
i i
b = do
i
r <- ClosedPoly i (BaseField c) -> m i
forall var a (m :: Type -> Type).
MonadCircuit var a m =>
ClosedPoly var a -> m var
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 x -> x -> x
forall a. AdditiveSemigroup a => a -> a -> a
+ i -> x
v i
b)
Natural -> Natural -> i -> m (i, i)
forall i a (m :: Type -> Type).
(MonadCircuit i a m, Arithmetic a) =>
Natural -> Natural -> i -> m (i, i)
splitExpansion (forall a (n :: Natural) (r :: RegisterSize).
(Finite a, KnownNat n, KnownRegisterSize r) =>
Natural
registerSize @(BaseField c) @n @r) Natural
1 i
r
instance (Symbolic c, KnownNat n, KnownRegisterSize rs) => MultiplicativeSemigroup (UInt n rs c) where
UInt c (Vector (NumberOfRegisters (BaseField c) n rs))
x * :: UInt n rs c -> UInt n rs c -> UInt n rs c
* UInt c (Vector (NumberOfRegisters (BaseField c) n rs))
y = c (Vector (NumberOfRegisters (BaseField c) n rs)) -> UInt n rs c
forall (n :: Natural) (r :: RegisterSize)
(context :: (Type -> Type) -> Type).
context (Vector (NumberOfRegisters (BaseField context) n r))
-> UInt n r context
UInt (c (Vector (NumberOfRegisters (BaseField c) n rs)) -> UInt n rs c)
-> c (Vector (NumberOfRegisters (BaseField c) n rs)) -> UInt n rs c
forall a b. (a -> b) -> a -> b
$ c (Vector (NumberOfRegisters (BaseField c) n rs))
-> c (Vector (NumberOfRegisters (BaseField c) n rs))
-> (Vector (NumberOfRegisters (BaseField c) n rs) (BaseField c)
-> Vector (NumberOfRegisters (BaseField c) n rs) (BaseField c)
-> Vector (NumberOfRegisters (BaseField c) n rs) (BaseField c))
-> (forall i (m :: Type -> Type).
MonadCircuit i (BaseField c) m =>
Vector (NumberOfRegisters (BaseField c) n rs) i
-> Vector (NumberOfRegisters (BaseField c) n rs) i
-> m (Vector (NumberOfRegisters (BaseField c) n rs) i))
-> c (Vector (NumberOfRegisters (BaseField c) n rs))
forall (c :: (Type -> Type) -> Type) a (f :: Type -> Type)
(g :: Type -> Type) (h :: Type -> Type).
(Symbolic c, BaseField c ~ a) =>
c f
-> c g
-> (f a -> g a -> h a)
-> (forall i (m :: Type -> Type).
MonadCircuit i a m =>
f i -> g i -> m (h i))
-> c h
symbolic2F c (Vector (NumberOfRegisters (BaseField c) n rs))
x c (Vector (NumberOfRegisters (BaseField c) n rs))
y (\Vector (NumberOfRegisters (BaseField c) n rs) (BaseField c)
u Vector (NumberOfRegisters (BaseField c) n rs) (BaseField c)
v -> forall (c :: (Type -> Type) -> Type) (n :: Natural)
(r :: RegisterSize).
(Symbolic c, KnownNat n, KnownRegisterSize r) =>
Natural
-> Vector (NumberOfRegisters (BaseField c) n r) (BaseField c)
naturalToVector @c @n @rs (Natural
-> Vector (NumberOfRegisters (BaseField c) n rs) (BaseField c))
-> Natural
-> Vector (NumberOfRegisters (BaseField c) n rs) (BaseField c)
forall a b. (a -> b) -> a -> b
$ Vector (NumberOfRegisters (BaseField c) n rs) (BaseField c)
-> Natural -> Natural
forall a (n :: Natural).
(ToConstant a, Const a ~ Natural) =>
Vector n a -> Natural -> Natural
vectorToNatural Vector (NumberOfRegisters (BaseField c) n rs) (BaseField c)
u (forall a (n :: Natural) (r :: RegisterSize).
(Finite a, KnownNat n, KnownRegisterSize r) =>
Natural
registerSize @(BaseField c) @n @rs) Natural -> Natural -> Natural
forall a. MultiplicativeSemigroup a => a -> a -> a
* Vector (NumberOfRegisters (BaseField c) n rs) (BaseField c)
-> Natural -> Natural
forall a (n :: Natural).
(ToConstant a, Const a ~ Natural) =>
Vector n a -> Natural -> Natural
vectorToNatural Vector (NumberOfRegisters (BaseField c) n rs) (BaseField c)
v (forall a (n :: Natural) (r :: RegisterSize).
(Finite a, KnownNat n, KnownRegisterSize r) =>
Natural
registerSize @(BaseField c) @n @rs)) Vector (NumberOfRegisters (BaseField c) n rs) i
-> Vector (NumberOfRegisters (BaseField c) n rs) i
-> m (Vector (NumberOfRegisters (BaseField c) n rs) i)
forall i (m :: Type -> Type).
MonadCircuit i (BaseField c) m =>
Vector (NumberOfRegisters (BaseField c) n rs) i
-> Vector (NumberOfRegisters (BaseField c) n rs) i
-> m (Vector (NumberOfRegisters (BaseField c) n rs) i)
solve
where
solve :: forall i m. (MonadCircuit i (BaseField c) m) => Vector (NumberOfRegisters (BaseField c) n rs) i -> Vector (NumberOfRegisters (BaseField c) n rs) i -> m (Vector (NumberOfRegisters (BaseField c) n rs) i)
solve :: forall i (m :: Type -> Type).
MonadCircuit i (BaseField c) m =>
Vector (NumberOfRegisters (BaseField c) n rs) i
-> Vector (NumberOfRegisters (BaseField c) n rs) i
-> m (Vector (NumberOfRegisters (BaseField c) n rs) i)
solve Vector (NumberOfRegisters (BaseField c) n rs) i
xv Vector (NumberOfRegisters (BaseField c) n rs) i
yv = do
case Vector (NumberOfRegisters (BaseField c) n rs) (i, i) -> [(i, i)]
forall (size :: Natural) a. Vector size a -> [a]
V.fromVector (Vector (NumberOfRegisters (BaseField c) n rs) (i, i) -> [(i, i)])
-> Vector (NumberOfRegisters (BaseField c) n rs) (i, i) -> [(i, i)]
forall a b. (a -> b) -> a -> b
$ Vector (NumberOfRegisters (BaseField c) n rs) i
-> Vector (NumberOfRegisters (BaseField c) n rs) i
-> Vector (NumberOfRegisters (BaseField c) n rs) (i, i)
forall a b.
Vector (NumberOfRegisters (BaseField c) n rs) a
-> Vector (NumberOfRegisters (BaseField c) n rs) b
-> Vector (NumberOfRegisters (BaseField c) n rs) (a, b)
forall (f :: Type -> Type) a b. Zip f => f a -> f b -> f (a, b)
Z.zip Vector (NumberOfRegisters (BaseField c) n rs) i
xv Vector (NumberOfRegisters (BaseField c) n rs) i
yv of
[] -> Vector (NumberOfRegisters (BaseField c) n rs) i
-> m (Vector (NumberOfRegisters (BaseField c) n rs) i)
forall a. a -> m a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Vector (NumberOfRegisters (BaseField c) n rs) i
-> m (Vector (NumberOfRegisters (BaseField c) n rs) i))
-> Vector (NumberOfRegisters (BaseField c) n rs) i
-> m (Vector (NumberOfRegisters (BaseField c) n rs) i)
forall a b. (a -> b) -> a -> b
$ [i] -> Vector (NumberOfRegisters (BaseField c) n rs) i
forall (size :: Natural) a. [a] -> Vector size a
V.unsafeToVector []
[(i
i, i
j)] -> [i] -> Vector (NumberOfRegisters (BaseField c) n rs) i
forall (size :: Natural) a. [a] -> Vector size a
V.unsafeToVector ([i] -> Vector (NumberOfRegisters (BaseField c) n rs) i)
-> m [i] -> m (Vector (NumberOfRegisters (BaseField c) n rs) i)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> i -> i -> m [i]
forall i (m :: Type -> Type).
MonadCircuit i (BaseField c) m =>
i -> i -> m [i]
solve1 i
i i
j
((i
i, i
j) : [(i, i)]
rest) -> let (i
z, i
w) = [(i, i)] -> (i, i)
forall a. HasCallStack => [a] -> a
Haskell.last [(i, i)]
rest
([i]
ris, [i]
rjs) = [(i, i)] -> ([i], [i])
forall a b. [(a, b)] -> ([a], [b])
Haskell.unzip ([(i, i)] -> ([i], [i])) -> [(i, i)] -> ([i], [i])
forall a b. (a -> b) -> a -> b
$ [(i, i)] -> [(i, i)]
forall a. HasCallStack => [a] -> [a]
Haskell.init [(i, i)]
rest
in [i] -> Vector (NumberOfRegisters (BaseField c) n rs) i
forall (size :: Natural) a. [a] -> Vector size a
V.unsafeToVector ([i] -> Vector (NumberOfRegisters (BaseField c) n rs) i)
-> m [i] -> m (Vector (NumberOfRegisters (BaseField c) n rs) i)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> (i, i) -> ([i], [i]) -> (i, i) -> m [i]
forall i (m :: Type -> Type).
MonadCircuit i (BaseField c) m =>
(i, i) -> ([i], [i]) -> (i, i) -> m [i]
solveN (i
i, i
j) ([i]
ris, [i]
rjs) (i
z, i
w)
solve1 :: forall i m. (MonadCircuit i (BaseField c) m) => i -> i -> m [i]
solve1 :: forall i (m :: Type -> Type).
MonadCircuit i (BaseField c) m =>
i -> i -> m [i]
solve1 i
i i
j = do
(i
z, i
_) <- ClosedPoly i (BaseField c) -> m i
forall var a (m :: Type -> Type).
MonadCircuit var a m =>
ClosedPoly var a -> m var
newAssigned (\i -> x
v -> i -> x
v i
i x -> x -> x
forall a. MultiplicativeSemigroup a => a -> a -> a
* i -> x
v i
j) 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).
(MonadCircuit i a m, Arithmetic a) =>
Natural -> Natural -> i -> m (i, i)
splitExpansion (forall a (n :: Natural) (r :: RegisterSize).
(Finite a, KnownNat n, KnownRegisterSize r) =>
Natural
highRegisterSize @(BaseField c) @n @rs) (forall a (n :: Natural) (r :: RegisterSize).
(Finite a, KnownNat n, KnownRegisterSize r) =>
Natural
maxOverflow @(BaseField c) @n @rs)
[i] -> m [i]
forall a. a -> m a
forall (m :: Type -> Type) a. Monad m => a -> m a
return [i
z]
solveN :: forall i m. (MonadCircuit i (BaseField c) m) => (i, i) -> ([i], [i]) -> (i, i) -> m [i]
solveN :: forall i (m :: Type -> Type).
MonadCircuit i (BaseField c) m =>
(i, i) -> ([i], [i]) -> (i, i) -> m [i]
solveN (i
i, i
j) ([i]
is, [i]
js) (i
i', i
j') = do
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) (r :: RegisterSize).
(Finite a, KnownNat n, KnownRegisterSize r) =>
Natural
numberOfRegisters @(BaseField c) @n @rs
i
q <- ClosedPoly i (BaseField c) -> m i
forall var a (m :: Type -> Type).
MonadCircuit var a m =>
ClosedPoly var a -> m var
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 (BaseField c) -> m i
forall var a (m :: Type -> Type).
MonadCircuit var a m =>
ClosedPoly var a -> m var
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).
(MonadCircuit i a m, Arithmetic a) =>
Natural -> Natural -> i -> m (i, i)
splitExpansion (forall a (n :: Natural) (r :: RegisterSize).
(Finite a, KnownNat n, KnownRegisterSize r) =>
Natural
registerSize @(BaseField c) @n @rs) (forall a (n :: Natural) (r :: RegisterSize).
(Finite a, KnownNat n, KnownRegisterSize r) =>
Natural
registerSize @(BaseField c) @n @rs) 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 (BaseField c) -> m i
forall var a (m :: Type -> Type).
MonadCircuit var a m =>
ClosedPoly var a -> m var
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).
(MonadCircuit i a m, Arithmetic a) =>
Natural -> Natural -> i -> m (i, i)
splitExpansion (forall a (n :: Natural) (r :: RegisterSize).
(Finite a, KnownNat n, KnownRegisterSize r) =>
Natural
registerSize @(BaseField c) @n @rs) (forall a (n :: Natural) (r :: RegisterSize).
(Finite a, KnownNat n, KnownRegisterSize r) =>
Natural
maxOverflow @(BaseField c) @n @rs) 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 (BaseField c) -> m i
forall var a (m :: Type -> Type).
MonadCircuit var a m =>
ClosedPoly var a -> m var
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 (BaseField c) -> m i
forall var a (m :: Type -> Type).
MonadCircuit var a m =>
ClosedPoly var a -> m var
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).
(MonadCircuit i a m, Arithmetic a) =>
Natural -> Natural -> i -> m (i, i)
splitExpansion (forall a (n :: Natural) (r :: RegisterSize).
(Finite a, KnownNat n, KnownRegisterSize r) =>
Natural
highRegisterSize @(BaseField c) @n @rs) (forall a (n :: Natural) (r :: RegisterSize).
(Finite a, KnownNat n, KnownRegisterSize r) =>
Natural
maxOverflow @(BaseField c) @n @rs) 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]
ps [i] -> [i] -> [i]
forall a. Semigroup a => a -> a -> a
<> [i
p'])
instance
( Symbolic c
, KnownNat n
, KnownRegisterSize r
) => Ring (UInt n r c)
deriving via (Structural (UInt n rs c))
instance (Symbolic c, KnownNat (NumberOfRegisters (BaseField c) n rs)) =>
Eq (Bool c) (UInt n rs c)
class StrictConv b a where
strictConv :: b -> a
instance (Symbolic c, KnownNat n, KnownRegisterSize rs) => StrictConv Natural (UInt n rs c) where
strictConv :: Natural -> UInt n rs c
strictConv Natural
n = case forall a (n :: Natural) (r :: RegisterSize).
(Arithmetic a, KnownNat n, KnownRegisterSize r) =>
Natural -> ([Natural], Natural, [Natural])
cast @(BaseField c) @n @rs Natural
n of
([Natural]
lo, Natural
hi, []) -> c (Vector (NumberOfRegisters (BaseField c) n rs)) -> UInt n rs c
forall (n :: Natural) (r :: RegisterSize)
(context :: (Type -> Type) -> Type).
context (Vector (NumberOfRegisters (BaseField context) n r))
-> UInt n r context
UInt (c (Vector (NumberOfRegisters (BaseField c) n rs)) -> UInt n rs c)
-> c (Vector (NumberOfRegisters (BaseField c) n rs)) -> UInt n rs c
forall a b. (a -> b) -> a -> b
$ Vector (NumberOfRegisters (BaseField c) n rs) (BaseField c)
-> c (Vector (NumberOfRegisters (BaseField c) n rs))
forall (c :: (Type -> Type) -> Type) (f :: Type -> Type).
(Symbolic c, Functor f) =>
f (BaseField c) -> c f
embed (Vector (NumberOfRegisters (BaseField c) n rs) (BaseField c)
-> c (Vector (NumberOfRegisters (BaseField c) n rs)))
-> Vector (NumberOfRegisters (BaseField c) n rs) (BaseField c)
-> c (Vector (NumberOfRegisters (BaseField c) n rs))
forall a b. (a -> b) -> a -> b
$ [BaseField c]
-> Vector (NumberOfRegisters (BaseField c) n rs) (BaseField c)
forall (size :: Natural) a. [a] -> Vector size a
V.unsafeToVector ([BaseField c]
-> Vector (NumberOfRegisters (BaseField c) n rs) (BaseField c))
-> [BaseField c]
-> Vector (NumberOfRegisters (BaseField c) n rs) (BaseField c)
forall a b. (a -> b) -> a -> b
$ Natural -> BaseField c
forall a b. FromConstant a b => a -> b
fromConstant (Natural -> BaseField c) -> [Natural] -> [BaseField c]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> ([Natural]
lo [Natural] -> [Natural] -> [Natural]
forall a. Semigroup a => a -> a -> a
<> [Natural
hi])
([Natural], Natural, [Natural])
_ -> String -> UInt n rs c
forall a. HasCallStack => String -> a
error String
"strictConv: overflow"
instance (Symbolic c, KnownNat n, KnownRegisterSize r) => StrictConv (Zp p) (UInt n r c) where
strictConv :: Zp p -> UInt n r c
strictConv = Natural -> UInt n r c
forall b a. StrictConv b a => b -> a
strictConv (Natural -> UInt n r c) -> (Zp p -> Natural) -> Zp p -> UInt n r c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Zp p -> Natural
Zp p -> Const (Zp p)
forall a. ToConstant a => a -> Const a
toConstant
instance (Symbolic c, KnownNat n, KnownRegisterSize r) => StrictConv (c Par1) (UInt n r c) where
strictConv :: c Par1 -> UInt n r c
strictConv c Par1
a = c (Vector (NumberOfRegisters (BaseField c) n r)) -> UInt n r c
forall (n :: Natural) (r :: RegisterSize)
(context :: (Type -> Type) -> Type).
context (Vector (NumberOfRegisters (BaseField context) n r))
-> UInt n r context
UInt (c (Vector (NumberOfRegisters (BaseField c) n r)) -> UInt n r c)
-> c (Vector (NumberOfRegisters (BaseField c) n r)) -> UInt n r c
forall a b. (a -> b) -> a -> b
$ c Par1
-> (Par1 (BaseField c)
-> Vector (NumberOfRegisters (BaseField c) n r) (BaseField c))
-> CircuitFun
Par1 (Vector (NumberOfRegisters (BaseField c) n r)) (BaseField c)
-> c (Vector (NumberOfRegisters (BaseField c) n r))
forall a (f :: Type -> Type) (g :: Type -> Type).
(BaseField c ~ a) =>
c f -> (f a -> g a) -> CircuitFun f g a -> c g
forall (c :: (Type -> Type) -> Type) a (f :: Type -> Type)
(g :: Type -> Type).
(Symbolic c, BaseField c ~ a) =>
c f -> (f a -> g a) -> CircuitFun f g a -> c g
symbolicF c Par1
a (\Par1 (BaseField c)
p -> [BaseField c]
-> Vector (NumberOfRegisters (BaseField c) n r) (BaseField c)
forall (size :: Natural) a. [a] -> Vector size a
V.unsafeToVector [Par1 (BaseField c) -> BaseField c
forall p. Par1 p -> p
unPar1 Par1 (BaseField c)
p]) Par1 i -> m (Vector (NumberOfRegisters (BaseField c) n r) i)
CircuitFun
Par1 (Vector (NumberOfRegisters (BaseField c) n r)) (BaseField c)
solve
where
solve :: MonadCircuit i (BaseField c) m => Par1 i -> m (Vector (NumberOfRegisters (BaseField c) n r) i)
solve :: CircuitFun
Par1 (Vector (NumberOfRegisters (BaseField c) n r)) (BaseField c)
solve Par1 i
xv = do
let i :: i
i = Par1 i -> i
forall p. Par1 p -> p
unPar1 Par1 i
xv
len :: Natural
len = Natural -> Natural -> Natural
forall a. Ord a => a -> a -> a
Haskell.min (forall (n :: Natural). KnownNat n => Natural
getNatural @n) (forall a. KnownNat (NumberOfBits a) => Natural
numberOfBits @(BaseField c))
[i]
bits <- [i] -> [i]
forall a. [a] -> [a]
Haskell.reverse ([i] -> [i]) -> m [i] -> m [i]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Natural -> i -> m [i]
forall i a (m :: Type -> Type).
(MonadCircuit i a m, Arithmetic a) =>
Natural -> i -> m [i]
expansion Natural
len i
i
[i] -> Vector (NumberOfRegisters (BaseField c) n r) i
forall (size :: Natural) a. [a] -> Vector size a
V.unsafeToVector ([i] -> Vector (NumberOfRegisters (BaseField c) n r) i)
-> m [i] -> m (Vector (NumberOfRegisters (BaseField c) n r) i)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Natural
-> Natural
-> forall v (m :: Type -> Type).
MonadCircuit v (BaseField c) m =>
[v] -> m [v]
forall a.
Natural
-> Natural
-> forall v (m :: Type -> Type). MonadCircuit v a m => [v] -> m [v]
fromBits (forall a (n :: Natural) (r :: RegisterSize).
(Finite a, KnownNat n, KnownRegisterSize r) =>
Natural
highRegisterSize @(BaseField c) @n @r) (forall a (n :: Natural) (r :: RegisterSize).
(Finite a, KnownNat n, KnownRegisterSize r) =>
Natural
registerSize @(BaseField c) @n @r) [i]
bits
class StrictNum a where
strictAdd :: a -> a -> a
strictSub :: a -> a -> a
strictMul :: a -> a -> a
instance (Symbolic c, KnownNat n, KnownRegisterSize r) => StrictNum (UInt n r c) where
strictAdd :: UInt n r c -> UInt n r c -> UInt n r c
strictAdd (UInt c (Vector (NumberOfRegisters (BaseField c) n r))
x) (UInt c (Vector (NumberOfRegisters (BaseField c) n r))
y) = c (Vector (NumberOfRegisters (BaseField c) n r)) -> UInt n r c
forall (n :: Natural) (r :: RegisterSize)
(context :: (Type -> Type) -> Type).
context (Vector (NumberOfRegisters (BaseField context) n r))
-> UInt n r context
UInt (c (Vector (NumberOfRegisters (BaseField c) n r)) -> UInt n r c)
-> c (Vector (NumberOfRegisters (BaseField c) n r)) -> UInt n r c
forall a b. (a -> b) -> a -> b
$ c (Vector (NumberOfRegisters (BaseField c) n r))
-> c (Vector (NumberOfRegisters (BaseField c) n r))
-> (Vector (NumberOfRegisters (BaseField c) n r) (BaseField c)
-> Vector (NumberOfRegisters (BaseField c) n r) (BaseField c)
-> Vector (NumberOfRegisters (BaseField c) n r) (BaseField c))
-> (forall i (m :: Type -> Type).
MonadCircuit i (BaseField c) m =>
Vector (NumberOfRegisters (BaseField c) n r) i
-> Vector (NumberOfRegisters (BaseField c) n r) i
-> m (Vector (NumberOfRegisters (BaseField c) n r) i))
-> c (Vector (NumberOfRegisters (BaseField c) n r))
forall (c :: (Type -> Type) -> Type) a (f :: Type -> Type)
(g :: Type -> Type) (h :: Type -> Type).
(Symbolic c, BaseField c ~ a) =>
c f
-> c g
-> (f a -> g a -> h a)
-> (forall i (m :: Type -> Type).
MonadCircuit i a m =>
f i -> g i -> m (h i))
-> c h
symbolic2F c (Vector (NumberOfRegisters (BaseField c) n r))
x c (Vector (NumberOfRegisters (BaseField c) n r))
y (\Vector (NumberOfRegisters (BaseField c) n r) (BaseField c)
u Vector (NumberOfRegisters (BaseField c) n r) (BaseField c)
v -> forall (c :: (Type -> Type) -> Type) (n :: Natural)
(r :: RegisterSize).
(Symbolic c, KnownNat n, KnownRegisterSize r) =>
Natural
-> Vector (NumberOfRegisters (BaseField c) n r) (BaseField c)
naturalToVector @c @n @r (Natural
-> Vector (NumberOfRegisters (BaseField c) n r) (BaseField c))
-> Natural
-> Vector (NumberOfRegisters (BaseField c) n r) (BaseField c)
forall a b. (a -> b) -> a -> b
$ Vector (NumberOfRegisters (BaseField c) n r) (BaseField c)
-> Natural -> Natural
forall a (n :: Natural).
(ToConstant a, Const a ~ Natural) =>
Vector n a -> Natural -> Natural
vectorToNatural Vector (NumberOfRegisters (BaseField c) n r) (BaseField c)
u (forall a (n :: Natural) (r :: RegisterSize).
(Finite a, KnownNat n, KnownRegisterSize r) =>
Natural
registerSize @(BaseField c) @n @r) Natural -> Natural -> Natural
forall a. AdditiveSemigroup a => a -> a -> a
+ Vector (NumberOfRegisters (BaseField c) n r) (BaseField c)
-> Natural -> Natural
forall a (n :: Natural).
(ToConstant a, Const a ~ Natural) =>
Vector n a -> Natural -> Natural
vectorToNatural Vector (NumberOfRegisters (BaseField c) n r) (BaseField c)
v (forall a (n :: Natural) (r :: RegisterSize).
(Finite a, KnownNat n, KnownRegisterSize r) =>
Natural
registerSize @(BaseField c) @n @r)) Vector (NumberOfRegisters (BaseField c) n r) i
-> Vector (NumberOfRegisters (BaseField c) n r) i
-> m (Vector (NumberOfRegisters (BaseField c) n r) i)
forall i (m :: Type -> Type).
MonadCircuit i (BaseField c) m =>
Vector (NumberOfRegisters (BaseField c) n r) i
-> Vector (NumberOfRegisters (BaseField c) n r) i
-> m (Vector (NumberOfRegisters (BaseField c) n r) i)
solve
where
solve :: MonadCircuit i (BaseField c) m => Vector (NumberOfRegisters (BaseField c) n r) i -> Vector (NumberOfRegisters (BaseField c) n r) i -> m (Vector (NumberOfRegisters (BaseField c) n r) i)
solve :: forall i (m :: Type -> Type).
MonadCircuit i (BaseField c) m =>
Vector (NumberOfRegisters (BaseField c) n r) i
-> Vector (NumberOfRegisters (BaseField c) n r) i
-> m (Vector (NumberOfRegisters (BaseField c) n r) i)
solve Vector (NumberOfRegisters (BaseField c) n r) i
xv Vector (NumberOfRegisters (BaseField c) n r) i
yv = do
i
j <- ClosedPoly i (BaseField c) -> m i
forall var a (m :: Type -> Type).
MonadCircuit var a m =>
ClosedPoly var a -> m var
newAssigned (x -> (i -> x) -> x
forall a b. a -> b -> a
Haskell.const x
forall a. AdditiveMonoid a => a
zero)
let xs :: [i]
xs = Vector (NumberOfRegisters (BaseField c) n r) i -> [i]
forall (size :: Natural) a. Vector size a -> [a]
V.fromVector Vector (NumberOfRegisters (BaseField c) n r) i
xv
ys :: [i]
ys = Vector (NumberOfRegisters (BaseField c) n r) i -> [i]
forall (size :: Natural) a. Vector size a -> [a]
V.fromVector Vector (NumberOfRegisters (BaseField c) n r) i
yv
z :: i
z = [i] -> i
forall a. HasCallStack => [a] -> a
Haskell.last [i]
xs
w :: i
w = [i] -> i
forall a. HasCallStack => [a] -> a
Haskell.last [i]
ys
midx :: [i]
midx = [i] -> [i]
forall a. HasCallStack => [a] -> [a]
Haskell.init [i]
xs
midy :: [i]
midy = [i] -> [i]
forall a. HasCallStack => [a] -> [a]
Haskell.init [i]
ys
([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
$
(i -> i -> i -> m (i, i)) -> [i] -> [i] -> [i -> m (i, i)]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
Haskell.zipWith (Natural -> i -> i -> i -> m (i, i)
forall a i (m :: Type -> Type).
(Arithmetic a, MonadCircuit i a m) =>
Natural -> i -> i -> i -> m (i, i)
fullAdder (Natural -> i -> i -> i -> m (i, i))
-> Natural -> i -> i -> i -> m (i, i)
forall a b. (a -> b) -> a -> b
$ forall a (n :: Natural) (r :: RegisterSize).
(Finite a, KnownNat n, KnownRegisterSize r) =>
Natural
registerSize @(BaseField c) @n @r) [i]
midx [i]
midy
i
k <- i -> i -> i -> m i
forall i a (m :: Type -> Type).
MonadCircuit i a m =>
i -> i -> i -> m i
fullAdded i
z i
w i
c
(i
ks, i
_) <- Natural -> Natural -> i -> m (i, i)
forall i a (m :: Type -> Type).
(MonadCircuit i a m, Arithmetic a) =>
Natural -> Natural -> i -> m (i, i)
splitExpansion (forall a (n :: Natural) (r :: RegisterSize).
(Finite a, KnownNat n, KnownRegisterSize r) =>
Natural
highRegisterSize @(BaseField c) @n @r) Natural
1 i
k
Vector (NumberOfRegisters (BaseField c) n r) i
-> m (Vector (NumberOfRegisters (BaseField c) n r) i)
forall a. a -> m a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Vector (NumberOfRegisters (BaseField c) n r) i
-> m (Vector (NumberOfRegisters (BaseField c) n r) i))
-> Vector (NumberOfRegisters (BaseField c) n r) i
-> m (Vector (NumberOfRegisters (BaseField c) n r) i)
forall a b. (a -> b) -> a -> b
$ [i] -> Vector (NumberOfRegisters (BaseField c) n r) i
forall (size :: Natural) a. [a] -> Vector size a
V.unsafeToVector ([i]
zs [i] -> [i] -> [i]
forall a. [a] -> [a] -> [a]
++ [i
ks])
strictSub :: UInt n r c -> UInt n r c -> UInt n r c
strictSub (UInt c (Vector (NumberOfRegisters (BaseField c) n r))
x) (UInt c (Vector (NumberOfRegisters (BaseField c) n r))
y) = c (Vector (NumberOfRegisters (BaseField c) n r)) -> UInt n r c
forall (n :: Natural) (r :: RegisterSize)
(context :: (Type -> Type) -> Type).
context (Vector (NumberOfRegisters (BaseField context) n r))
-> UInt n r context
UInt (c (Vector (NumberOfRegisters (BaseField c) n r)) -> UInt n r c)
-> c (Vector (NumberOfRegisters (BaseField c) n r)) -> UInt n r c
forall a b. (a -> b) -> a -> b
$ c (Vector (NumberOfRegisters (BaseField c) n r))
-> c (Vector (NumberOfRegisters (BaseField c) n r))
-> (Vector (NumberOfRegisters (BaseField c) n r) (BaseField c)
-> Vector (NumberOfRegisters (BaseField c) n r) (BaseField c)
-> Vector (NumberOfRegisters (BaseField c) n r) (BaseField c))
-> (forall i (m :: Type -> Type).
MonadCircuit i (BaseField c) m =>
Vector (NumberOfRegisters (BaseField c) n r) i
-> Vector (NumberOfRegisters (BaseField c) n r) i
-> m (Vector (NumberOfRegisters (BaseField c) n r) i))
-> c (Vector (NumberOfRegisters (BaseField c) n r))
forall (c :: (Type -> Type) -> Type) a (f :: Type -> Type)
(g :: Type -> Type) (h :: Type -> Type).
(Symbolic c, BaseField c ~ a) =>
c f
-> c g
-> (f a -> g a -> h a)
-> (forall i (m :: Type -> Type).
MonadCircuit i a m =>
f i -> g i -> m (h i))
-> c h
symbolic2F c (Vector (NumberOfRegisters (BaseField c) n r))
x c (Vector (NumberOfRegisters (BaseField c) n r))
y (\Vector (NumberOfRegisters (BaseField c) n r) (BaseField c)
u Vector (NumberOfRegisters (BaseField c) n r) (BaseField c)
v -> forall (c :: (Type -> Type) -> Type) (n :: Natural)
(r :: RegisterSize).
(Symbolic c, KnownNat n, KnownRegisterSize r) =>
Natural
-> Vector (NumberOfRegisters (BaseField c) n r) (BaseField c)
naturalToVector @c @n @r (Natural
-> Vector (NumberOfRegisters (BaseField c) n r) (BaseField c))
-> Natural
-> Vector (NumberOfRegisters (BaseField c) n r) (BaseField c)
forall a b. (a -> b) -> a -> b
$ Vector (NumberOfRegisters (BaseField c) n r) (BaseField c)
-> Natural -> Natural
forall a (n :: Natural).
(ToConstant a, Const a ~ Natural) =>
Vector n a -> Natural -> Natural
vectorToNatural Vector (NumberOfRegisters (BaseField c) n r) (BaseField c)
u (forall a (n :: Natural) (r :: RegisterSize).
(Finite a, KnownNat n, KnownRegisterSize r) =>
Natural
registerSize @(BaseField c) @n @r) Natural -> Natural -> Natural
-! Vector (NumberOfRegisters (BaseField c) n r) (BaseField c)
-> Natural -> Natural
forall a (n :: Natural).
(ToConstant a, Const a ~ Natural) =>
Vector n a -> Natural -> Natural
vectorToNatural Vector (NumberOfRegisters (BaseField c) n r) (BaseField c)
v (forall a (n :: Natural) (r :: RegisterSize).
(Finite a, KnownNat n, KnownRegisterSize r) =>
Natural
registerSize @(BaseField c) @n @r)) Vector (NumberOfRegisters (BaseField c) n r) i
-> Vector (NumberOfRegisters (BaseField c) n r) i
-> m (Vector (NumberOfRegisters (BaseField c) n r) i)
forall i (m :: Type -> Type).
MonadCircuit i (BaseField c) m =>
Vector (NumberOfRegisters (BaseField c) n r) i
-> Vector (NumberOfRegisters (BaseField c) n r) i
-> m (Vector (NumberOfRegisters (BaseField c) n r) i)
solve
where
t :: BaseField c
t :: BaseField c
t = (BaseField c
forall a. MultiplicativeMonoid a => a
one BaseField c -> BaseField c -> BaseField c
forall a. AdditiveSemigroup a => a -> a -> a
+ BaseField c
forall a. MultiplicativeMonoid a => a
one) BaseField c -> Natural -> BaseField c
forall a b. Exponent a b => a -> b -> a
^ forall a (n :: Natural) (r :: RegisterSize).
(Finite a, KnownNat n, KnownRegisterSize r) =>
Natural
registerSize @(BaseField c) @n @r BaseField c -> BaseField c -> BaseField c
forall a. AdditiveGroup a => a -> a -> a
- BaseField c
forall a. MultiplicativeMonoid a => a
one
solve :: MonadCircuit i (BaseField c) m => Vector (NumberOfRegisters (BaseField c) n r) i -> Vector (NumberOfRegisters (BaseField c) n r) i -> m (Vector (NumberOfRegisters (BaseField c) n r) i)
solve :: forall i (m :: Type -> Type).
MonadCircuit i (BaseField c) m =>
Vector (NumberOfRegisters (BaseField c) n r) i
-> Vector (NumberOfRegisters (BaseField c) n r) i
-> m (Vector (NumberOfRegisters (BaseField c) n r) i)
solve Vector (NumberOfRegisters (BaseField c) n r) i
xv Vector (NumberOfRegisters (BaseField c) n r) i
yv = do
case Vector (NumberOfRegisters (BaseField c) n r) (i, i) -> [(i, i)]
forall (size :: Natural) a. Vector size a -> [a]
V.fromVector (Vector (NumberOfRegisters (BaseField c) n r) (i, i) -> [(i, i)])
-> Vector (NumberOfRegisters (BaseField c) n r) (i, i) -> [(i, i)]
forall a b. (a -> b) -> a -> b
$ Vector (NumberOfRegisters (BaseField c) n r) i
-> Vector (NumberOfRegisters (BaseField c) n r) i
-> Vector (NumberOfRegisters (BaseField c) n r) (i, i)
forall a b.
Vector (NumberOfRegisters (BaseField c) n r) a
-> Vector (NumberOfRegisters (BaseField c) n r) b
-> Vector (NumberOfRegisters (BaseField c) n r) (a, b)
forall (f :: Type -> Type) a b. Zip f => f a -> f b -> f (a, b)
Z.zip Vector (NumberOfRegisters (BaseField c) n r) i
xv Vector (NumberOfRegisters (BaseField c) n r) i
yv of
[] -> Vector (NumberOfRegisters (BaseField c) n r) i
-> m (Vector (NumberOfRegisters (BaseField c) n r) i)
forall a. a -> m a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Vector (NumberOfRegisters (BaseField c) n r) i
-> m (Vector (NumberOfRegisters (BaseField c) n r) i))
-> Vector (NumberOfRegisters (BaseField c) n r) i
-> m (Vector (NumberOfRegisters (BaseField c) n r) i)
forall a b. (a -> b) -> a -> b
$ [i] -> Vector (NumberOfRegisters (BaseField c) n r) i
forall (size :: Natural) a. [a] -> Vector size a
V.unsafeToVector []
[(i
i, i
j)] -> [i] -> Vector (NumberOfRegisters (BaseField c) n r) i
forall (size :: Natural) a. [a] -> Vector size a
V.unsafeToVector ([i] -> Vector (NumberOfRegisters (BaseField c) n r) i)
-> m [i] -> m (Vector (NumberOfRegisters (BaseField c) n r) i)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> i -> i -> m [i]
forall i (m :: Type -> Type).
MonadCircuit i (BaseField c) m =>
i -> i -> m [i]
solve1 i
i i
j
((i
i, i
j) : [(i, i)]
rest) -> let (i
z, i
w) = [(i, i)] -> (i, i)
forall a. HasCallStack => [a] -> a
Haskell.last [(i, i)]
rest
([i]
ris, [i]
rjs) = [(i, i)] -> ([i], [i])
forall a b. [(a, b)] -> ([a], [b])
Haskell.unzip ([(i, i)] -> ([i], [i])) -> [(i, i)] -> ([i], [i])
forall a b. (a -> b) -> a -> b
$ [(i, i)] -> [(i, i)]
forall a. HasCallStack => [a] -> [a]
Haskell.init [(i, i)]
rest
in [i] -> Vector (NumberOfRegisters (BaseField c) n r) i
forall (size :: Natural) a. [a] -> Vector size a
V.unsafeToVector ([i] -> Vector (NumberOfRegisters (BaseField c) n r) i)
-> m [i] -> m (Vector (NumberOfRegisters (BaseField c) n r) i)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> (i, i) -> ([i], [i]) -> (i, i) -> m [i]
forall i (m :: Type -> Type).
MonadCircuit i (BaseField c) m =>
(i, i) -> ([i], [i]) -> (i, i) -> m [i]
solveN (i
i, i
j) ([i]
ris, [i]
rjs) (i
z, i
w)
solve1 :: MonadCircuit i (BaseField c) m => i -> i -> m [i]
solve1 :: forall i (m :: Type -> Type).
MonadCircuit i (BaseField c) m =>
i -> i -> m [i]
solve1 i
i i
j = do
i
z <- ClosedPoly i (BaseField c) -> m i
forall var a (m :: Type -> Type).
MonadCircuit var a m =>
ClosedPoly var a -> m var
newAssigned (\i -> x
v -> i -> x
v i
i x -> x -> x
forall a. AdditiveGroup a => a -> a -> a
- i -> x
v i
j)
[i]
_ <- Natural -> i -> m [i]
forall i a (m :: Type -> Type).
(MonadCircuit i a m, Arithmetic a) =>
Natural -> i -> m [i]
expansion (forall a (n :: Natural) (r :: RegisterSize).
(Finite a, KnownNat n, KnownRegisterSize r) =>
Natural
highRegisterSize @(BaseField c) @n @r) i
z
[i] -> m [i]
forall a. a -> m a
forall (m :: Type -> Type) a. Monad m => a -> m a
return [i
z]
solveN :: MonadCircuit i (BaseField c) m => (i, i) -> ([i], [i]) -> (i, i) -> m [i]
solveN :: forall i (m :: Type -> Type).
MonadCircuit i (BaseField c) m =>
(i, i) -> ([i], [i]) -> (i, i) -> m [i]
solveN (i
i, i
j) ([i]
is, [i]
js) (i
i', i
j') = do
i
s <- ClosedPoly i (BaseField c) -> m i
forall var a (m :: Type -> Type).
MonadCircuit var a m =>
ClosedPoly var a -> m var
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
+ BaseField c -> x
forall a b. FromConstant a b => a -> b
fromConstant (BaseField c
t BaseField c -> BaseField c -> BaseField c
forall a. AdditiveSemigroup a => a -> a -> a
+ BaseField c
forall a. MultiplicativeMonoid a => a
one))
(i
k, i
b0) <- Natural -> Natural -> i -> m (i, i)
forall i a (m :: Type -> Type).
(MonadCircuit i a m, Arithmetic a) =>
Natural -> Natural -> i -> m (i, i)
splitExpansion (forall a (n :: Natural) (r :: RegisterSize).
(Finite a, KnownNat n, KnownRegisterSize r) =>
Natural
registerSize @(BaseField c) @n @r) 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 ((i -> i -> i -> m (i, i)) -> [i] -> [i] -> [i -> m (i, i)]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
Haskell.zipWith i -> i -> i -> m (i, i)
forall i (m :: Type -> Type).
MonadCircuit i (BaseField c) m =>
i -> i -> i -> m (i, i)
fullSub [i]
is [i]
js)
i
k' <- ClosedPoly i (BaseField c) -> m i
forall var a (m :: Type -> Type).
MonadCircuit var a m =>
ClosedPoly var a -> m var
newAssigned (\i -> x
v -> i -> x
v i
i' x -> x -> x
forall a. AdditiveGroup a => a -> a -> a
- i -> x
v i
j')
i
s' <- ClosedPoly i (BaseField c) -> m i
forall var a (m :: Type -> Type).
MonadCircuit var a m =>
ClosedPoly var a -> m var
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).
(MonadCircuit i a m, Arithmetic a) =>
Natural -> i -> m [i]
expansion (forall a (n :: Natural) (r :: RegisterSize).
(Finite a, KnownNat n, KnownRegisterSize r) =>
Natural
highRegisterSize @(BaseField c) @n @r) i
s'
[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]
zs [i] -> [i] -> [i]
forall a. Semigroup a => a -> a -> a
<> [i
s'])
fullSub :: MonadCircuit i (BaseField c) m => i -> i -> i -> m (i, i)
fullSub :: forall i (m :: Type -> Type).
MonadCircuit i (BaseField c) m =>
i -> i -> i -> m (i, i)
fullSub i
xk i
yk i
b = do
i
k <- ClosedPoly i (BaseField c) -> m i
forall var a (m :: Type -> Type).
MonadCircuit var a m =>
ClosedPoly var a -> m var
newAssigned (\i -> x
v -> i -> x
v i
xk x -> x -> x
forall a. AdditiveGroup a => a -> a -> a
- i -> x
v i
yk)
i
s <- ClosedPoly i (BaseField c) -> m i
forall var a (m :: Type -> Type).
MonadCircuit var a m =>
ClosedPoly var a -> m var
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
+ BaseField c -> x
forall a b. FromConstant a b => a -> b
fromConstant BaseField c
t)
Natural -> Natural -> i -> m (i, i)
forall i a (m :: Type -> Type).
(MonadCircuit i a m, Arithmetic a) =>
Natural -> Natural -> i -> m (i, i)
splitExpansion (forall a (n :: Natural) (r :: RegisterSize).
(Finite a, KnownNat n, KnownRegisterSize r) =>
Natural
registerSize @(BaseField c) @n @r) Natural
1 i
s
strictMul :: UInt n r c -> UInt n r c -> UInt n r c
strictMul (UInt c (Vector (NumberOfRegisters (BaseField c) n r))
x) (UInt c (Vector (NumberOfRegisters (BaseField c) n r))
y) = c (Vector (NumberOfRegisters (BaseField c) n r)) -> UInt n r c
forall (n :: Natural) (r :: RegisterSize)
(context :: (Type -> Type) -> Type).
context (Vector (NumberOfRegisters (BaseField context) n r))
-> UInt n r context
UInt (c (Vector (NumberOfRegisters (BaseField c) n r)) -> UInt n r c)
-> c (Vector (NumberOfRegisters (BaseField c) n r)) -> UInt n r c
forall a b. (a -> b) -> a -> b
$ c (Vector (NumberOfRegisters (BaseField c) n r))
-> c (Vector (NumberOfRegisters (BaseField c) n r))
-> (Vector (NumberOfRegisters (BaseField c) n r) (BaseField c)
-> Vector (NumberOfRegisters (BaseField c) n r) (BaseField c)
-> Vector (NumberOfRegisters (BaseField c) n r) (BaseField c))
-> (forall i (m :: Type -> Type).
MonadCircuit i (BaseField c) m =>
Vector (NumberOfRegisters (BaseField c) n r) i
-> Vector (NumberOfRegisters (BaseField c) n r) i
-> m (Vector (NumberOfRegisters (BaseField c) n r) i))
-> c (Vector (NumberOfRegisters (BaseField c) n r))
forall (c :: (Type -> Type) -> Type) a (f :: Type -> Type)
(g :: Type -> Type) (h :: Type -> Type).
(Symbolic c, BaseField c ~ a) =>
c f
-> c g
-> (f a -> g a -> h a)
-> (forall i (m :: Type -> Type).
MonadCircuit i a m =>
f i -> g i -> m (h i))
-> c h
symbolic2F c (Vector (NumberOfRegisters (BaseField c) n r))
x c (Vector (NumberOfRegisters (BaseField c) n r))
y (\Vector (NumberOfRegisters (BaseField c) n r) (BaseField c)
u Vector (NumberOfRegisters (BaseField c) n r) (BaseField c)
v -> forall (c :: (Type -> Type) -> Type) (n :: Natural)
(r :: RegisterSize).
(Symbolic c, KnownNat n, KnownRegisterSize r) =>
Natural
-> Vector (NumberOfRegisters (BaseField c) n r) (BaseField c)
naturalToVector @c @n @r (Natural
-> Vector (NumberOfRegisters (BaseField c) n r) (BaseField c))
-> Natural
-> Vector (NumberOfRegisters (BaseField c) n r) (BaseField c)
forall a b. (a -> b) -> a -> b
$ Vector (NumberOfRegisters (BaseField c) n r) (BaseField c)
-> Natural -> Natural
forall a (n :: Natural).
(ToConstant a, Const a ~ Natural) =>
Vector n a -> Natural -> Natural
vectorToNatural Vector (NumberOfRegisters (BaseField c) n r) (BaseField c)
u (forall a (n :: Natural) (r :: RegisterSize).
(Finite a, KnownNat n, KnownRegisterSize r) =>
Natural
registerSize @(BaseField c) @n @r) Natural -> Natural -> Natural
forall a. MultiplicativeSemigroup a => a -> a -> a
* Vector (NumberOfRegisters (BaseField c) n r) (BaseField c)
-> Natural -> Natural
forall a (n :: Natural).
(ToConstant a, Const a ~ Natural) =>
Vector n a -> Natural -> Natural
vectorToNatural Vector (NumberOfRegisters (BaseField c) n r) (BaseField c)
v (forall a (n :: Natural) (r :: RegisterSize).
(Finite a, KnownNat n, KnownRegisterSize r) =>
Natural
registerSize @(BaseField c) @n @r)) Vector (NumberOfRegisters (BaseField c) n r) i
-> Vector (NumberOfRegisters (BaseField c) n r) i
-> m (Vector (NumberOfRegisters (BaseField c) n r) i)
forall i (m :: Type -> Type).
MonadCircuit i (BaseField c) m =>
Vector (NumberOfRegisters (BaseField c) n r) i
-> Vector (NumberOfRegisters (BaseField c) n r) i
-> m (Vector (NumberOfRegisters (BaseField c) n r) i)
solve
where
solve :: MonadCircuit i (BaseField c) m => Vector (NumberOfRegisters (BaseField c) n r) i -> Vector (NumberOfRegisters (BaseField c) n r) i -> m (Vector (NumberOfRegisters (BaseField c) n r) i)
solve :: forall i (m :: Type -> Type).
MonadCircuit i (BaseField c) m =>
Vector (NumberOfRegisters (BaseField c) n r) i
-> Vector (NumberOfRegisters (BaseField c) n r) i
-> m (Vector (NumberOfRegisters (BaseField c) n r) i)
solve Vector (NumberOfRegisters (BaseField c) n r) i
xv Vector (NumberOfRegisters (BaseField c) n r) i
yv = do
case Vector (NumberOfRegisters (BaseField c) n r) (i, i) -> [(i, i)]
forall (size :: Natural) a. Vector size a -> [a]
V.fromVector (Vector (NumberOfRegisters (BaseField c) n r) (i, i) -> [(i, i)])
-> Vector (NumberOfRegisters (BaseField c) n r) (i, i) -> [(i, i)]
forall a b. (a -> b) -> a -> b
$ Vector (NumberOfRegisters (BaseField c) n r) i
-> Vector (NumberOfRegisters (BaseField c) n r) i
-> Vector (NumberOfRegisters (BaseField c) n r) (i, i)
forall a b.
Vector (NumberOfRegisters (BaseField c) n r) a
-> Vector (NumberOfRegisters (BaseField c) n r) b
-> Vector (NumberOfRegisters (BaseField c) n r) (a, b)
forall (f :: Type -> Type) a b. Zip f => f a -> f b -> f (a, b)
Z.zip Vector (NumberOfRegisters (BaseField c) n r) i
xv Vector (NumberOfRegisters (BaseField c) n r) i
yv of
[] -> Vector (NumberOfRegisters (BaseField c) n r) i
-> m (Vector (NumberOfRegisters (BaseField c) n r) i)
forall a. a -> m a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Vector (NumberOfRegisters (BaseField c) n r) i
-> m (Vector (NumberOfRegisters (BaseField c) n r) i))
-> Vector (NumberOfRegisters (BaseField c) n r) i
-> m (Vector (NumberOfRegisters (BaseField c) n r) i)
forall a b. (a -> b) -> a -> b
$ [i] -> Vector (NumberOfRegisters (BaseField c) n r) i
forall (size :: Natural) a. [a] -> Vector size a
V.unsafeToVector []
[(i
i, i
j)] -> [i] -> Vector (NumberOfRegisters (BaseField c) n r) i
forall (size :: Natural) a. [a] -> Vector size a
V.unsafeToVector ([i] -> Vector (NumberOfRegisters (BaseField c) n r) i)
-> m [i] -> m (Vector (NumberOfRegisters (BaseField c) n r) i)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> i -> i -> m [i]
forall i (m :: Type -> Type).
MonadCircuit i (BaseField c) m =>
i -> i -> m [i]
solve1 i
i i
j
((i
i, i
j) : [(i, i)]
rest) -> let (i
z, i
w) = [(i, i)] -> (i, i)
forall a. HasCallStack => [a] -> a
Haskell.last [(i, i)]
rest
([i]
ris, [i]
rjs) = [(i, i)] -> ([i], [i])
forall a b. [(a, b)] -> ([a], [b])
Haskell.unzip ([(i, i)] -> ([i], [i])) -> [(i, i)] -> ([i], [i])
forall a b. (a -> b) -> a -> b
$ [(i, i)] -> [(i, i)]
forall a. HasCallStack => [a] -> [a]
Haskell.init [(i, i)]
rest
in [i] -> Vector (NumberOfRegisters (BaseField c) n r) i
forall (size :: Natural) a. [a] -> Vector size a
V.unsafeToVector ([i] -> Vector (NumberOfRegisters (BaseField c) n r) i)
-> m [i] -> m (Vector (NumberOfRegisters (BaseField c) n r) i)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> (i, i) -> ([i], [i]) -> (i, i) -> m [i]
forall i (m :: Type -> Type).
MonadCircuit i (BaseField c) m =>
(i, i) -> ([i], [i]) -> (i, i) -> m [i]
solveN (i
i, i
j) ([i]
ris, [i]
rjs) (i
z, i
w)
solve1 :: MonadCircuit i (BaseField c) m => i -> i -> m [i]
solve1 :: forall i (m :: Type -> Type).
MonadCircuit i (BaseField c) m =>
i -> i -> m [i]
solve1 i
i i
j = do
i
z <- ClosedPoly i (BaseField c) -> m i
forall var a (m :: Type -> Type).
MonadCircuit var a m =>
ClosedPoly var a -> m var
newAssigned (ClosedPoly i (BaseField c) -> m i)
-> ClosedPoly i (BaseField c) -> m i
forall a b. (a -> b) -> a -> b
$ \i -> x
v -> i -> x
v i
i x -> x -> x
forall a. MultiplicativeSemigroup a => a -> a -> a
* i -> x
v i
j
[i]
_ <- Natural -> i -> m [i]
forall i a (m :: Type -> Type).
(MonadCircuit i a m, Arithmetic a) =>
Natural -> i -> m [i]
expansion (forall a (n :: Natural) (r :: RegisterSize).
(Finite a, KnownNat n, KnownRegisterSize r) =>
Natural
highRegisterSize @(BaseField c) @n @r) i
z
[i] -> m [i]
forall a. a -> m a
forall (m :: Type -> Type) a. Monad m => a -> m a
return [i
z]
solveN :: MonadCircuit i (BaseField c) m => (i, i) -> ([i], [i]) -> (i, i) -> m [i]
solveN :: forall i (m :: Type -> Type).
MonadCircuit i (BaseField c) m =>
(i, i) -> ([i], [i]) -> (i, i) -> m [i]
solveN (i
i, i
j) ([i]
is, [i]
js) (i
i', i
j') = do
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) (r :: RegisterSize).
(Finite a, KnownNat n, KnownRegisterSize r) =>
Natural
numberOfRegisters @(BaseField c) @n @r
i
q <- ClosedPoly i (BaseField c) -> m i
forall var a (m :: Type -> Type).
MonadCircuit var a m =>
ClosedPoly var a -> m var
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 (BaseField c) -> m i
forall var a (m :: Type -> Type).
MonadCircuit var a m =>
ClosedPoly var a -> m var
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).
(MonadCircuit i a m, Arithmetic a) =>
Natural -> Natural -> i -> m (i, i)
splitExpansion (forall a (n :: Natural) (r :: RegisterSize).
(Finite a, KnownNat n, KnownRegisterSize r) =>
Natural
registerSize @(BaseField c) @n @r) (forall a (n :: Natural) (r :: RegisterSize).
(Finite a, KnownNat n, KnownRegisterSize r) =>
Natural
registerSize @(BaseField c) @n @r) 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 (BaseField c) -> m i
forall var a (m :: Type -> Type).
MonadCircuit var a m =>
ClosedPoly var a -> m var
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).
(MonadCircuit i a m, Arithmetic a) =>
Natural -> Natural -> i -> m (i, i)
splitExpansion (forall a (n :: Natural) (r :: RegisterSize).
(Finite a, KnownNat n, KnownRegisterSize r) =>
Natural
registerSize @(BaseField c) @n @r) (forall a (n :: Natural) (r :: RegisterSize).
(Finite a, KnownNat n, KnownRegisterSize r) =>
Natural
maxOverflow @(BaseField c) @n @r) 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 (BaseField c) -> m i
forall var a (m :: Type -> Type).
MonadCircuit var a m =>
ClosedPoly var a -> m var
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 (BaseField c) -> m i
forall var a (m :: Type -> Type).
MonadCircuit var a m =>
ClosedPoly var a -> m var
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).
(MonadCircuit i a m, Arithmetic a) =>
Natural -> i -> m [i]
expansion (forall a (n :: Natural) (r :: RegisterSize).
(Finite a, KnownNat n, KnownRegisterSize r) =>
Natural
highRegisterSize @(BaseField c) @n @r) 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 (BaseField c) -> m ()
forall var a (m :: Type -> Type).
MonadCircuit var a m =>
ClosedPoly var 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]
ps [i] -> [i] -> [i]
forall a. Semigroup a => a -> a -> a
<> [i
p'])
instance
( Symbolic c
, KnownNat n
, KnownRegisterSize r
, KnownNat (NumberOfRegisters (BaseField c) n r)
) => SymbolicInput (UInt n r c) where
isValid :: UInt n r c -> Bool (Context (UInt n r c))
isValid (UInt c (Vector (NumberOfRegisters (BaseField c) n r))
bits) = Context (UInt n r c) Par1 -> Bool (Context (UInt n r c))
forall (c :: (Type -> Type) -> Type). c Par1 -> Bool c
Bool (Context (UInt n r c) Par1 -> Bool (Context (UInt n r c)))
-> Context (UInt n r c) Par1 -> Bool (Context (UInt n r c))
forall a b. (a -> b) -> a -> b
$ c (Vector (NumberOfRegisters (BaseField c) n r))
-> CircuitFun
(Vector (NumberOfRegisters (BaseField c) n r)) Par1 (BaseField c)
-> c Par1
forall (f :: Type -> Type) (g :: Type -> Type).
c f -> CircuitFun f g (BaseField c) -> c g
forall (c :: (Type -> Type) -> Type) (f :: Type -> Type)
(g :: Type -> Type).
Symbolic c =>
c f -> CircuitFun f g (BaseField c) -> c g
fromCircuitF c (Vector (NumberOfRegisters (BaseField c) n r))
bits Vector (NumberOfRegisters (BaseField c) n r) i -> m (Par1 i)
CircuitFun
(Vector (NumberOfRegisters (BaseField c) n r)) Par1 (BaseField c)
solve
where
solve :: MonadCircuit i (BaseField c) m => Vector (NumberOfRegisters (BaseField c) n r) i -> m (Par1 i)
solve :: CircuitFun
(Vector (NumberOfRegisters (BaseField c) n r)) Par1 (BaseField c)
solve Vector (NumberOfRegisters (BaseField c) n r) i
v = do
let vs :: [i]
vs = Vector (NumberOfRegisters (BaseField c) n r) i -> [i]
forall (size :: Natural) a. Vector size a -> [a]
V.fromVector Vector (NumberOfRegisters (BaseField c) n r) i
v
[i]
bs <- [i] -> Natural -> Natural -> m [i]
forall v a (m :: Type -> Type).
(MonadCircuit v a m, Arithmetic a) =>
[v] -> Natural -> Natural -> m [v]
toBits ([i] -> [i]
forall a. [a] -> [a]
Haskell.reverse [i]
vs) (forall a (n :: Natural) (r :: RegisterSize).
(Finite a, KnownNat n, KnownRegisterSize r) =>
Natural
highRegisterSize @(BaseField c) @n @r) (forall a (n :: Natural) (r :: RegisterSize).
(Finite a, KnownNat n, KnownRegisterSize r) =>
Natural
registerSize @(BaseField c) @n @r)
[i]
ys <- [i] -> [i]
forall a. [a] -> [a]
Haskell.reverse ([i] -> [i]) -> m [i] -> m [i]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Natural
-> Natural
-> forall v (m :: Type -> Type).
MonadCircuit v (BaseField c) m =>
[v] -> m [v]
forall a.
Natural
-> Natural
-> forall v (m :: Type -> Type). MonadCircuit v a m => [v] -> m [v]
fromBits (forall a (n :: Natural) (r :: RegisterSize).
(Finite a, KnownNat n, KnownRegisterSize r) =>
Natural
highRegisterSize @(BaseField c) @n @r) (forall a (n :: Natural) (r :: RegisterSize).
(Finite a, KnownNat n, KnownRegisterSize r) =>
Natural
registerSize @(BaseField c) @n @r) [i]
bs
[i]
difference <- [(i, i)] -> ((i, i) -> 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 ([i] -> [i] -> [(i, i)]
forall a b. [a] -> [b] -> [(a, b)]
zip [i]
vs [i]
ys) (((i, i) -> m i) -> m [i]) -> ((i, i) -> m i) -> m [i]
forall a b. (a -> b) -> a -> b
$ \(i
i, i
j) -> ClosedPoly i (BaseField c) -> m i
forall var a (m :: Type -> Type).
MonadCircuit var a m =>
ClosedPoly var a -> m var
newAssigned (\i -> x
w -> i -> x
w i
i x -> x -> x
forall a. AdditiveGroup a => a -> a -> a
- i -> x
w i
j)
[Par1 i]
isZeros <- [i] -> (i -> m (Par1 i)) -> m [Par1 i]
forall (t :: Type -> Type) (f :: Type -> Type) a b.
(Traversable t, Applicative f) =>
t a -> (a -> f b) -> f (t b)
for [i]
difference ((i -> m (Par1 i)) -> m [Par1 i])
-> (i -> m (Par1 i)) -> m [Par1 i]
forall a b. (a -> b) -> a -> b
$ Par1 i -> m (Par1 i)
forall i a (m :: Type -> Type) (f :: Type -> Type).
(MonadCircuit i a m, Representable f, Traversable f) =>
f i -> m (f i)
isZero (Par1 i -> m (Par1 i)) -> (i -> Par1 i) -> i -> m (Par1 i)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. i -> Par1 i
forall p. p -> Par1 p
Par1
[Par1 i] -> m (Par1 i)
forall i a (m :: Type -> Type).
MonadCircuit i a m =>
[Par1 i] -> m (Par1 i)
helper [Par1 i]
isZeros
helper :: MonadCircuit i a m => [Par1 i] -> m (Par1 i)
helper :: forall i a (m :: Type -> Type).
MonadCircuit i a m =>
[Par1 i] -> m (Par1 i)
helper [Par1 i]
xs = case [Par1 i]
xs of
[] -> i -> Par1 i
forall p. p -> Par1 p
Par1 (i -> Par1 i) -> m i -> m (Par1 i)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> ClosedPoly i a -> m i
forall var a (m :: Type -> Type).
MonadCircuit var a m =>
ClosedPoly var a -> m var
newAssigned (x -> (i -> x) -> x
forall a b. a -> b -> a
const x
forall a. MultiplicativeMonoid a => a
one)
(Par1 i
b : [Par1 i]
bs) -> (Par1 i -> Par1 i -> m (Par1 i))
-> Par1 i -> [Par1 i] -> m (Par1 i)
forall (t :: Type -> Type) (m :: Type -> Type) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldlM (\(Par1 i
v1) (Par1 i
v2) -> i -> Par1 i
forall p. p -> Par1 p
Par1 (i -> Par1 i) -> m i -> m (Par1 i)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> ClosedPoly i a -> m i
forall var a (m :: Type -> Type).
MonadCircuit var a m =>
ClosedPoly var a -> m var
newAssigned (((i -> x) -> i -> x
forall a b. (a -> b) -> a -> b
$ i
v1) ((i -> x) -> x) -> ((i -> x) -> x) -> (i -> x) -> x
forall a. MultiplicativeSemigroup a => a -> a -> a
* ((i -> x) -> i -> x
forall a b. (a -> b) -> a -> b
$ i
v2))) Par1 i
b [Par1 i]
bs
fullAdder :: (Arithmetic a, MonadCircuit i a m) => Natural -> i -> i -> i -> m (i, i)
fullAdder :: forall a i (m :: Type -> Type).
(Arithmetic a, MonadCircuit i a m) =>
Natural -> i -> i -> i -> m (i, i)
fullAdder Natural
r i
xk i
yk i
c = i -> i -> i -> m i
forall i a (m :: Type -> Type).
MonadCircuit i a m =>
i -> i -> i -> m i
fullAdded i
xk i
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).
(MonadCircuit i a m, Arithmetic a) =>
Natural -> Natural -> i -> m (i, i)
splitExpansion Natural
r Natural
1
fullAdded :: MonadCircuit i a m => i -> i -> i -> m i
fullAdded :: forall i a (m :: Type -> Type).
MonadCircuit i a m =>
i -> i -> i -> m i
fullAdded i
i i
j i
c = do
i
k <- ClosedPoly i a -> m i
forall var a (m :: Type -> Type).
MonadCircuit var a m =>
ClosedPoly var a -> m var
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 var a (m :: Type -> Type).
MonadCircuit var a m =>
ClosedPoly var a -> m var
newAssigned (\i -> x
v -> i -> x
v i
k x -> x -> x
forall a. AdditiveSemigroup a => a -> a -> a
+ i -> x
v i
c)
naturalToVector :: forall c n r . (Symbolic c, KnownNat n, KnownRegisterSize r) => Natural -> Vector (NumberOfRegisters (BaseField c) n r) (BaseField c)
naturalToVector :: forall (c :: (Type -> Type) -> Type) (n :: Natural)
(r :: RegisterSize).
(Symbolic c, KnownNat n, KnownRegisterSize r) =>
Natural
-> Vector (NumberOfRegisters (BaseField c) n r) (BaseField c)
naturalToVector Natural
c = let ([Natural]
lo, Natural
hi, [Natural]
_) = forall a (n :: Natural) (r :: RegisterSize).
(Arithmetic a, KnownNat n, KnownRegisterSize r) =>
Natural -> ([Natural], Natural, [Natural])
cast @(BaseField c) @n @r (Natural -> ([Natural], Natural, [Natural]))
-> (Natural -> Natural)
-> Natural
-> ([Natural], Natural, [Natural])
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)) (Natural -> ([Natural], Natural, [Natural]))
-> Natural -> ([Natural], Natural, [Natural])
forall a b. (a -> b) -> a -> b
$ Natural
c
in [BaseField c]
-> Vector (NumberOfRegisters (BaseField c) n r) (BaseField c)
forall (size :: Natural) a. [a] -> Vector size a
V.unsafeToVector ([BaseField c]
-> Vector (NumberOfRegisters (BaseField c) n r) (BaseField c))
-> [BaseField c]
-> Vector (NumberOfRegisters (BaseField c) n r) (BaseField c)
forall a b. (a -> b) -> a -> b
$ (Natural -> BaseField c
forall a b. FromConstant a b => a -> b
fromConstant (Natural -> BaseField c) -> [Natural] -> [BaseField c]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> [Natural]
lo) [BaseField c] -> [BaseField c] -> [BaseField c]
forall a. Semigroup a => a -> a -> a
<> [Natural -> BaseField c
forall a b. FromConstant a b => a -> b
fromConstant Natural
hi]
vectorToNatural :: (ToConstant a, Const a ~ Natural) => Vector n a -> Natural -> Natural
vectorToNatural :: forall a (n :: Natural).
(ToConstant a, Const a ~ Natural) =>
Vector n a -> Natural -> Natural
vectorToNatural Vector n a
v Natural
n = (Natural -> Natural -> Natural) -> Natural -> [Natural] -> 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 (\Natural
l Natural
r -> Natural -> Natural
forall a b. FromConstant a b => a -> b
fromConstant Natural
l Natural -> Natural -> Natural
forall a. AdditiveSemigroup a => a -> a -> a
+ Natural
b Natural -> Natural -> Natural
forall a. MultiplicativeSemigroup a => a -> a -> a
* Natural
r) Natural
0 [Natural]
vs where
vs :: [Natural]
vs = (a -> Natural) -> [a] -> [Natural]
forall a b. (a -> b) -> [a] -> [b]
Haskell.map a -> Natural
a -> Const a
forall a. ToConstant a => a -> Const a
toConstant ([a] -> [Natural]) -> [a] -> [Natural]
forall a b. (a -> b) -> a -> b
$ Vector n a -> [a]
forall (size :: Natural) a. Vector size a -> [a]
V.fromVector Vector n a
v :: [Natural]
b :: Natural
b = Natural
2 Natural -> Natural -> Natural
forall a b. Exponent a b => a -> b -> a
^ Natural
n
instance (Symbolic c, KnownNat n, KnownRegisterSize r) => FromJSON (UInt n r c) where
parseJSON :: Value -> Parser (UInt n r c)
parseJSON = (Natural -> UInt n r c) -> Parser Natural -> Parser (UInt n r c)
forall a b. (a -> b) -> Parser a -> Parser b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
Haskell.fmap Natural -> UInt n r c
forall b a. StrictConv b a => b -> a
strictConv (Parser Natural -> Parser (UInt n r c))
-> (Value -> Parser Natural) -> Value -> Parser (UInt n r c)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. FromJSON a => Value -> Parser a
parseJSON @Natural
instance (Symbolic (Interpreter (Zp p)), KnownNat n, KnownRegisterSize r) => ToJSON (UInt n r (Interpreter (Zp p))) where
toJSON :: UInt n r (Interpreter (Zp p)) -> Value
toJSON = Natural -> Value
forall a. ToJSON a => a -> Value
toJSON (Natural -> Value)
-> (UInt n r (Interpreter (Zp p)) -> Natural)
-> UInt n r (Interpreter (Zp p))
-> Value
forall b c a. (b -> c) -> (a -> b) -> a -> c
. UInt n r (Interpreter (Zp p)) -> Natural
UInt n r (Interpreter (Zp p))
-> Const (UInt n r (Interpreter (Zp p)))
forall a. ToConstant a => a -> Const a
toConstant