{-# LANGUAGE AllowAmbiguousTypes  #-}
{-# LANGUAGE DerivingVia          #-}
{-# LANGUAGE NoDeriveAnyClass     #-}
{-# LANGUAGE TypeApplications     #-}
{-# LANGUAGE TypeOperators        #-}
{-# LANGUAGE UndecidableInstances #-}

{-# OPTIONS_GHC -freduction-depth=0 #-} -- Avoid reduction overflow error caused by NumberOfRegisters

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)


-- TODO (Issue #18): hide this constructor
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)

-- | Extended Euclidean algorithm.
-- Exploits the fact that @s_i@ and @t_i@ change signs in turns on each iteration, so it adjusts the formulas correspondingly
-- and never requires signed arithmetic.
-- (i.e. it calculates @x = b - a@ instead of @x = a - b@ when @a - b@ is negative
-- and changes @y - x@ to @y + x@ on the following iteration)
-- This only affects Bezout coefficients, remainders are calculated without changes as they are always non-negative.
--
-- If the algorithm is used to calculate Bezout coefficients,
-- it requires that @a@ and @b@ are coprime, @b@ is not 1 and @a@ is not 0, otherwise the optimisation above is not valid.
--
-- If the algorithm is only used to find @gcd(a, b)@ (i.e. @s@ and @t@ will be discarded), @a@ and @b@ can be arbitrary integers.
--
eea
    :: forall n 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
                -- single addend for lower register
                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)
                -- multiple addends for middle registers
                [[i]]
qs <- [Natural] -> (Natural -> m [i]) -> m [[i]]
forall (t :: Type -> Type) (f :: Type -> Type) a b.
(Traversable t, Applicative f) =>
t a -> (a -> f b) -> f (t b)
for [Natural
1 .. Natural
r Natural -> Natural -> Natural
-! Natural
2] ((Natural -> m [i]) -> m [[i]]) -> (Natural -> m [i]) -> m [[i]]
forall a b. (a -> b) -> a -> b
$ \Natural
k ->
                    [Natural] -> (Natural -> m i) -> m [i]
forall (t :: Type -> Type) (f :: Type -> Type) a b.
(Traversable t, Applicative f) =>
t a -> (a -> f b) -> f (t b)
for [Natural
0 .. Natural
k] ((Natural -> m i) -> m [i]) -> (Natural -> m i) -> m [i]
forall a b. (a -> b) -> a -> b
$ \Natural
l ->
                        ClosedPoly i (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)))
                -- lower register
                (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
                -- middle registers
                ([i]
ps, i
c') <- (StateT i m [i] -> i -> m ([i], i))
-> i -> StateT i m [i] -> m ([i], i)
forall a b c. (a -> b -> c) -> b -> a -> c
flip StateT i m [i] -> i -> m ([i], i)
forall s (m :: Type -> Type) a. StateT s m a -> s -> m (a, s)
runStateT i
c (StateT i m [i] -> m ([i], i)) -> StateT i m [i] -> m ([i], i)
forall a b. (a -> b) -> a -> b
$ [[i]] -> ([i] -> StateT i m i) -> StateT i m [i]
forall (t :: Type -> Type) (f :: Type -> Type) a b.
(Traversable t, Applicative f) =>
t a -> (a -> f b) -> f (t b)
for [[i]]
qs (([i] -> StateT i m i) -> StateT i m [i])
-> ([i] -> StateT i m i) -> StateT i m [i]
forall a b. (a -> b) -> a -> b
$ (i -> m (i, i)) -> StateT i m i
forall s (m :: Type -> Type) a. (s -> m (a, s)) -> StateT s m a
StateT ((i -> m (i, i)) -> StateT i m i)
-> ([i] -> i -> m (i, i)) -> [i] -> StateT i m i
forall b c a. (b -> c) -> (a -> b) -> a -> c
. \[i]
rs i
c' -> do
                    i
s <- (i -> i -> m i) -> i -> [i] -> m i
forall (t :: Type -> Type) (m :: Type -> Type) a b.
(Foldable t, Monad m) =>
(a -> b -> m b) -> b -> t a -> m b
foldrM (\i
k i
l -> ClosedPoly i (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
                -- high register
                i
p'0 <- (Natural -> i -> m i) -> i -> [Natural] -> m i
forall (t :: Type -> Type) (m :: Type -> Type) a b.
(Foldable t, Monad m) =>
(a -> b -> m b) -> b -> t a -> m b
foldrM (\Natural
k i
l -> do
                    i
k' <- ClosedPoly i (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
                -- single addend for lower register
                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)
                -- multiple addends for middle registers
                [[i]]
qs <- [Natural] -> (Natural -> m [i]) -> m [[i]]
forall (t :: Type -> Type) (f :: Type -> Type) a b.
(Traversable t, Applicative f) =>
t a -> (a -> f b) -> f (t b)
for [Natural
1 .. Natural
r Natural -> Natural -> Natural
-! Natural
2] ((Natural -> m [i]) -> m [[i]]) -> (Natural -> m [i]) -> m [[i]]
forall a b. (a -> b) -> a -> b
$ \Natural
k ->
                    [Natural] -> (Natural -> m i) -> m [i]
forall (t :: Type -> Type) (f :: Type -> Type) a b.
(Traversable t, Applicative f) =>
t a -> (a -> f b) -> f (t b)
for [Natural
0 .. Natural
k] ((Natural -> m i) -> m [i]) -> (Natural -> m i) -> m [i]
forall a b. (a -> b) -> a -> b
$ \Natural
l ->
                        ClosedPoly i (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)))
                -- lower register
                (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
                -- middle registers
                ([i]
ps, i
c') <- (StateT i m [i] -> i -> m ([i], i))
-> i -> StateT i m [i] -> m ([i], i)
forall a b c. (a -> b -> c) -> b -> a -> c
flip StateT i m [i] -> i -> m ([i], i)
forall s (m :: Type -> Type) a. StateT s m a -> s -> m (a, s)
runStateT i
c (StateT i m [i] -> m ([i], i)) -> StateT i m [i] -> m ([i], i)
forall a b. (a -> b) -> a -> b
$ [[i]] -> ([i] -> StateT i m i) -> StateT i m [i]
forall (t :: Type -> Type) (f :: Type -> Type) a b.
(Traversable t, Applicative f) =>
t a -> (a -> f b) -> f (t b)
for [[i]]
qs (([i] -> StateT i m i) -> StateT i m [i])
-> ([i] -> StateT i m i) -> StateT i m [i]
forall a b. (a -> b) -> a -> b
$ (i -> m (i, i)) -> StateT i m i
forall s (m :: Type -> Type) a. (s -> m (a, s)) -> StateT s m a
StateT ((i -> m (i, i)) -> StateT i m i)
-> ([i] -> i -> m (i, i)) -> [i] -> StateT i m i
forall b c a. (b -> c) -> (a -> b) -> a -> c
. \[i]
rs i
c' -> do
                    i
s <- (i -> i -> m i) -> i -> [i] -> m i
forall (t :: Type -> Type) (m :: Type -> Type) a b.
(Foldable t, Monad m) =>
(a -> b -> m b) -> b -> t a -> m b
foldrM (\i
k i
l -> ClosedPoly i (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
                -- high register
                i
p' <- (Natural -> i -> m i) -> i -> [Natural] -> m i
forall (t :: Type -> Type) (m :: Type -> Type) a b.
(Foldable t, Monad m) =>
(a -> b -> m b) -> b -> t a -> m b
foldrM (\Natural
k i
l -> do
                    i
k' <- ClosedPoly i (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'
                -- all addends higher should be zero
                [Natural] -> (Natural -> m ()) -> m ()
forall (t :: Type -> Type) (f :: Type -> Type) a b.
(Foldable t, Applicative f) =>
t a -> (a -> f b) -> f ()
for_ [Natural
r .. Natural
r Natural -> Natural -> Natural
forall a. MultiplicativeSemigroup a => a -> a -> a
* Natural
2 Natural -> Natural -> Natural
-! Natural
2] ((Natural -> m ()) -> m ()) -> (Natural -> m ()) -> m ()
forall a b. (a -> b) -> a -> b
$ \Natural
k ->
                    [Natural] -> (Natural -> m ()) -> m ()
forall (t :: Type -> Type) (f :: Type -> Type) a b.
(Foldable t, Applicative f) =>
t a -> (a -> f b) -> f ()
for_ [Natural
k Natural -> Natural -> Natural
-! Natural
r Natural -> Natural -> Natural
forall a. AdditiveSemigroup a => a -> a -> a
+ Natural
1 .. Natural
r Natural -> Natural -> Natural
-! Natural
1] ((Natural -> m ()) -> m ()) -> (Natural -> m ()) -> m ()
forall a b. (a -> b) -> a -> b
$ \Natural
l ->
                        ClosedPoly i (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