{-# 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(..),
    OrdWord,
    toConstant,
    asWords,
    expMod,
    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                    (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.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 (KnownRegisters c n r, Symbolic c) => 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

-- | @expMod n pow modulus@ calculates @n^pow % modulus@ where all values are arithmetised
--
expMod
    :: forall c n p m r
    .  Symbolic c
    => KnownRegisterSize r
    => KnownNat p
    => KnownNat n
    => KnownNat m
    => KnownNat (2 * m)
    => KnownRegisters c (2 * m) r
    => KnownNat (Ceil (GetRegisterSize (BaseField c) (2 * m) r) OrdWord)
    => NFData (c (Vector (NumberOfRegisters (BaseField c) (2 * m) r)))
    => UInt n r c
    -> UInt p r c
    -> UInt m r c
    -> UInt m r c
expMod :: forall (c :: (Type -> Type) -> Type) (n :: Natural) (p :: Natural)
       (m :: Natural) (r :: RegisterSize).
(Symbolic c, KnownRegisterSize r, KnownNat p, KnownNat n,
 KnownNat m, KnownNat (2 * m), KnownRegisters c (2 * m) r,
 KnownNat (Ceil (GetRegisterSize (BaseField c) (2 * m) r) OrdWord),
 NFData (c (Vector (NumberOfRegisters (BaseField c) (2 * m) r)))) =>
UInt n r c -> UInt p r c -> UInt m r c -> UInt m r c
expMod UInt n r c
n UInt p r c
pow UInt m r c
modulus = UInt (2 * m) r c -> UInt m r c
forall a b. Resize a b => a -> b
resize UInt (2 * m) r c
result
    where
        bits :: ByteString p c
        bits :: ByteString p c
bits = UInt p r c -> ByteString p c
forall a b. Iso a b => a -> b
from UInt p r c
pow

        m' :: UInt (2 * m) r c
        m' :: UInt (2 * m) r c
m' = UInt m r c -> UInt (2 * m) r c
forall a b. Resize a b => a -> b
resize UInt m r c
modulus

        n' :: UInt (2 * m) r c
        n' :: UInt (2 * m) r c
n' = UInt n r c -> UInt (2 * m) r c
forall a b. Resize a b => a -> b
resize UInt n r c
n UInt (2 * m) r c -> UInt (2 * m) r c -> UInt (2 * m) r c
forall a. SemiEuclidean a => a -> a -> a
`mod` UInt (2 * m) r c
m'

        result :: UInt (2 * m) r c
        result :: UInt (2 * m) r c
result = Natural
-> ByteString p c
-> UInt (2 * m) r c
-> UInt (2 * m) r c
-> UInt (2 * m) r c
-> UInt (2 * m) r c
forall (c :: (Type -> Type) -> Type) (n :: Natural) (p :: Natural)
       (r :: RegisterSize).
(Symbolic c, KnownRegisterSize r, KnownNat n, KnownNat p,
 KnownRegisters c n r,
 KnownNat (Ceil (GetRegisterSize (BaseField c) n r) OrdWord),
 NFData (c (Vector (NumberOfRegisters (BaseField c) n r)))) =>
Natural
-> ByteString p c
-> UInt n r c
-> UInt n r c
-> UInt n r c
-> UInt n r c
bitsPow (forall (n :: Natural). KnownNat n => Natural
value @p) ByteString p c
bits UInt (2 * m) r c
forall a. MultiplicativeMonoid a => a
one UInt (2 * m) r c
n' UInt (2 * m) r c
m'

bitsPow
    :: forall c n p r
    .  Symbolic c
    => KnownRegisterSize r
    => KnownNat n
    => KnownNat p
    => KnownRegisters c n r
    => KnownNat (Ceil (GetRegisterSize (BaseField c) n r) OrdWord)
    => NFData (c (Vector (NumberOfRegisters (BaseField c) n r)))
    => Natural
    -> ByteString p c
    -> UInt n r c
    -> UInt n r c
    -> UInt n r c
    -> UInt n r c
bitsPow :: forall (c :: (Type -> Type) -> Type) (n :: Natural) (p :: Natural)
       (r :: RegisterSize).
(Symbolic c, KnownRegisterSize r, KnownNat n, KnownNat p,
 KnownRegisters c n r,
 KnownNat (Ceil (GetRegisterSize (BaseField c) n r) OrdWord),
 NFData (c (Vector (NumberOfRegisters (BaseField c) n r)))) =>
Natural
-> ByteString p c
-> UInt n r c
-> UInt n r c
-> UInt n r c
-> UInt n r c
bitsPow Natural
0 ByteString p c
_ UInt n r c
res UInt n r c
_ UInt n r c
_ = UInt n r c
res
bitsPow Natural
b ByteString p c
bits UInt n r c
res UInt n r c
n UInt n r c
m = Natural
-> ByteString p c
-> UInt n r c
-> UInt n r c
-> UInt n r c
-> UInt n r c
forall (c :: (Type -> Type) -> Type) (n :: Natural) (p :: Natural)
       (r :: RegisterSize).
(Symbolic c, KnownRegisterSize r, KnownNat n, KnownNat p,
 KnownRegisters c n r,
 KnownNat (Ceil (GetRegisterSize (BaseField c) n r) OrdWord),
 NFData (c (Vector (NumberOfRegisters (BaseField c) n r)))) =>
Natural
-> ByteString p c
-> UInt n r c
-> UInt n r c
-> UInt n r c
-> UInt n r c
bitsPow (Natural
b Natural -> Natural -> Natural
-! Natural
1) ByteString p c
bits UInt n r c
newRes UInt n r c
sq UInt n r c
m
    where
        sq :: UInt n r c
sq = (UInt n r c
n UInt n r c -> UInt n r c -> UInt n r c
forall a. MultiplicativeSemigroup a => a -> a -> a
* UInt n r c
n) UInt n r c -> UInt n r c -> UInt n r c
forall a. SemiEuclidean a => a -> a -> a
`mod` UInt n r c
m
        newRes :: UInt n r c
newRes = UInt n r c -> UInt n r c
forall a. NFData a => a -> a
force (UInt n r c -> UInt n r c) -> UInt n r c -> UInt n r c
forall a b. (a -> b) -> a -> b
$ Bool c -> UInt n r c -> UInt n r c -> UInt n r c
forall b a. Conditional b a => b -> a -> a -> a
gif (ByteString p c -> Natural -> Bool c
forall (c :: (Type -> Type) -> Type) (n :: Natural).
Symbolic c =>
ByteString n c -> Natural -> Bool c
isSet ByteString p c
bits (Natural
b Natural -> Natural -> Natural
-! Natural
1)) ((UInt n r c
res UInt n r c -> UInt n r c -> UInt n r c
forall a. MultiplicativeSemigroup a => a -> a -> a
* UInt n r c
n) UInt n r c -> UInt n r c -> UInt n r c
forall a. SemiEuclidean a => a -> a -> a
`mod` UInt n r c
m) UInt n r c
res


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
    => KnownRegisters 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,
 KnownRegisters 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)) c
-> c (Vector (NumberOfRegisters (BaseField c) n r))
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 c -> 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
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 w (m :: Type -> Type).
   MonadCircuit v (BaseField c) w m =>
   [v] -> m [v]
forall a.
Natural
-> Natural
-> forall v w (m :: Type -> Type).
   MonadCircuit v a w 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) c
-> c (Vector n)
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 c -> 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
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 w (m :: Type -> Type).
(MonadCircuit v a w 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
    ) => Resize (UInt n r c) (UInt k r c) where
    resize :: UInt n r c -> UInt k r c
resize (UInt c (Vector (NumberOfRegisters (BaseField c) n r))
bits) = 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))
     c
-> c (Vector (NumberOfRegisters (BaseField c) k r))
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 c -> c g
symbolicF c (Vector (NumberOfRegisters (BaseField c) n r))
bits
        (\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
v -> 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
v
                ns :: [Natural]
ns = 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
1) Natural
n [Natural] -> [Natural] -> [Natural]
forall a. [a] -> [a] -> [a]
++ [forall a (n :: Natural) (r :: RegisterSize).
(Finite a, KnownNat n, KnownRegisterSize r) =>
Natural
highRegisterSize @(BaseField c) @n @r]
                ks :: [Natural]
ks = 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) @k @r Natural -> Natural -> Natural
-! Natural
1) Natural
k [Natural] -> [Natural] -> [Natural]
forall a. [a] -> [a] -> [a]
++ [forall a (n :: Natural) (r :: RegisterSize).
(Finite a, KnownNat n, KnownRegisterSize r) =>
Natural
highRegisterSize @(BaseField c) @k @r]
                zs :: [(Natural, i)]
zs = [Natural] -> [i] -> [(Natural, i)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Natural]
ns [i]
regs

            [(Natural, i)]
resZ <- [(Natural, i)] -> [Natural] -> m [(Natural, i)]
forall i w (m :: Type -> Type).
MonadCircuit i (BaseField c) w m =>
[(Natural, i)] -> [Natural] -> m [(Natural, i)]
helper [(Natural, i)]
zs [Natural]
ks
            let ([Natural]
_, [i]
res) = [(Natural, i)] -> ([Natural], [i])
forall a b. [(a, b)] -> ([a], [b])
Haskell.unzip [(Natural, i)]
resZ
            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]
res
        )
        where
            n :: Natural
n = forall a (n :: Natural) (r :: RegisterSize).
(Finite a, KnownNat n, KnownRegisterSize r) =>
Natural
registerSize @(BaseField c) @n @r
            k :: Natural
k = forall a (n :: Natural) (r :: RegisterSize).
(Finite a, KnownNat n, KnownRegisterSize r) =>
Natural
registerSize @(BaseField c) @k @r

            helper :: MonadCircuit i (BaseField c) w m => [(Natural, i)] -> [Natural] -> m [(Natural, i)]
            helper :: forall i w (m :: Type -> Type).
MonadCircuit i (BaseField c) w m =>
[(Natural, i)] -> [Natural] -> m [(Natural, i)]
helper [(Natural, i)]
_ [] = [(Natural, i)] -> m [(Natural, i)]
forall a. a -> m a
forall (m :: Type -> Type) a. Monad m => a -> m a
return []
            helper [] (Natural
a:[Natural]
as) = do
                ([(Natural
a, forall a b. FromConstant a b => a -> b
fromConstant @(BaseField c) BaseField c
forall a. AdditiveMonoid a => a
zero)] [(Natural, i)] -> [(Natural, i)] -> [(Natural, i)]
forall a. Semigroup a => a -> a -> a
<> ) ([(Natural, i)] -> [(Natural, i)])
-> m [(Natural, i)] -> m [(Natural, i)]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
Haskell.<$> [(Natural, i)] -> [Natural] -> m [(Natural, i)]
forall i w (m :: Type -> Type).
MonadCircuit i (BaseField c) w m =>
[(Natural, i)] -> [Natural] -> m [(Natural, i)]
helper [] [Natural]
as
            helper ((Natural
xN, i
xI) : [(Natural, i)]
xs) acc :: [Natural]
acc@(Natural
a:[Natural]
as)
                | Natural
xN Natural -> Natural -> Bool
forall b a. Ord b a => a -> a -> b
> Natural
a = do
                        (i
l, i
h) <- Natural -> Natural -> i -> m (i, i)
forall i a w (m :: Type -> Type).
(MonadCircuit i a w m, Arithmetic a) =>
Natural -> Natural -> i -> m (i, i)
splitExpansion Natural
a (Natural
xN Natural -> Natural -> Natural
-! Natural
a) i
xI
                        ([(Natural
a, i
l)] [(Natural, i)] -> [(Natural, i)] -> [(Natural, i)]
forall a. Semigroup a => a -> a -> a
<> ) ([(Natural, i)] -> [(Natural, i)])
-> m [(Natural, i)] -> m [(Natural, i)]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
Haskell.<$> [(Natural, i)] -> [Natural] -> m [(Natural, i)]
forall i w (m :: Type -> Type).
MonadCircuit i (BaseField c) w m =>
[(Natural, i)] -> [Natural] -> m [(Natural, i)]
helper ((Natural
xN Natural -> Natural -> Natural
-! Natural
a, i
h) (Natural, i) -> [(Natural, i)] -> [(Natural, i)]
forall a. a -> [a] -> [a]
: [(Natural, i)]
xs) [Natural]
as
                | Natural
xN Natural -> Natural -> Bool
forall b a. Eq b a => a -> a -> b
== Natural
a = ([(Natural
a, i
xI)] [(Natural, i)] -> [(Natural, i)] -> [(Natural, i)]
forall a. Semigroup a => a -> a -> a
<> ) ([(Natural, i)] -> [(Natural, i)])
-> m [(Natural, i)] -> m [(Natural, i)]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
Haskell.<$> [(Natural, i)] -> [Natural] -> m [(Natural, i)]
forall i w (m :: Type -> Type).
MonadCircuit i (BaseField c) w m =>
[(Natural, i)] -> [Natural] -> m [(Natural, i)]
helper [(Natural, i)]
xs [Natural]
as
                | Bool
otherwise = case [(Natural, i)]
xs of
                    [] -> ([(Natural
xN, i
xI)] [(Natural, i)] -> [(Natural, i)] -> [(Natural, i)]
forall a. Semigroup a => a -> a -> a
<> ) ([(Natural, i)] -> [(Natural, i)])
-> m [(Natural, i)] -> m [(Natural, i)]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
Haskell.<$> [(Natural, i)] -> [Natural] -> m [(Natural, i)]
forall i w (m :: Type -> Type).
MonadCircuit i (BaseField c) w m =>
[(Natural, i)] -> [Natural] -> m [(Natural, i)]
helper [] [Natural]
as
                    ((Natural
yN, i
yI) : [(Natural, i)]
ys) -> do
                        let newN :: Natural
newN = Natural
xN Natural -> Natural -> Natural
forall a. AdditiveSemigroup a => a -> a -> a
+ Natural
yN
                        i
newI <- ClosedPoly i (BaseField c) -> m i
forall var a w (m :: Type -> Type).
MonadCircuit var a w m =>
ClosedPoly var a -> m var
newAssigned (\i -> x
j -> i -> x
j i
xI x -> x -> x
forall a. AdditiveSemigroup a => a -> a -> a
+ Natural -> x -> x
forall b a. Scale b a => b -> a -> a
scale ((Natural
2 :: Natural) Natural -> Natural -> Natural
forall a b. Exponent a b => a -> b -> a
^ Natural
xN) (i -> x
j i
yI))
                        [(Natural, i)] -> [Natural] -> m [(Natural, i)]
forall i w (m :: Type -> Type).
MonadCircuit i (BaseField c) w m =>
[(Natural, i)] -> [Natural] -> m [(Natural, i)]
helper ((Natural
newN, i
newI) (Natural, i) -> [(Natural, i)] -> [(Natural, i)]
forall a. a -> [a] -> [a]
: [(Natural, i)]
ys) [Natural]
acc

instance
    ( Symbolic c
    , KnownNat n
    , KnownNat r
    , KnownRegisterSize rs
    , r ~ NumberOfRegisters (BaseField c) n rs
    , KnownNat (Ceil (GetRegisterSize (BaseField c) n rs) OrdWord)
    , 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)

asWords
    :: forall wordSize regSize ctx k
    .  Symbolic ctx
    => KnownNat (Ceil regSize wordSize)
    => KnownNat wordSize
    => ctx (Vector k)                           -- @k@ registers of size up to @regSize@
    -> ctx (Vector (k * Ceil regSize wordSize)) -- @k * wordsPerReg@ registers of size @wordSize@
asWords :: forall (wordSize :: Natural) (regSize :: Natural)
       (ctx :: (Type -> Type) -> Type) (k :: Natural).
(Symbolic ctx, KnownNat (Ceil regSize wordSize),
 KnownNat wordSize) =>
ctx (Vector k) -> ctx (Vector (k * Ceil regSize wordSize))
asWords ctx (Vector k)
v = ctx (Vector k)
-> (forall {i} {m :: Type -> Type}.
    (NFData i, MonadCircuit i (BaseField ctx) (WitnessField ctx) m) =>
    FunBody '[Vector k] (Vector (k * Ceil regSize wordSize)) i m)
-> ctx (Vector (k * Ceil regSize wordSize))
forall (f :: Type -> Type) (g :: Type -> Type).
ctx f -> CircuitFun '[f] g ctx -> ctx g
forall (c :: (Type -> Type) -> Type) (f :: Type -> Type)
       (g :: Type -> Type).
Symbolic c =>
c f -> CircuitFun '[f] g c -> c g
fromCircuitF ctx (Vector k)
v ((forall {i} {m :: Type -> Type}.
  (NFData i, MonadCircuit i (BaseField ctx) (WitnessField ctx) m) =>
  FunBody '[Vector k] (Vector (k * Ceil regSize wordSize)) i m)
 -> ctx (Vector (k * Ceil regSize wordSize)))
-> (forall {i} {m :: Type -> Type}.
    (NFData i, MonadCircuit i (BaseField ctx) (WitnessField ctx) m) =>
    FunBody '[Vector k] (Vector (k * Ceil regSize wordSize)) i m)
-> ctx (Vector (k * Ceil regSize wordSize))
forall a b. (a -> b) -> a -> b
$ \Vector k i
regs -> do
    Vector k [i]
words <- (i -> m [i]) -> Vector k i -> m (Vector k [i])
forall (t :: Type -> Type) (m :: Type -> Type) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: Type -> Type) a b.
Monad m =>
(a -> m b) -> Vector k a -> m (Vector k b)
Haskell.mapM (forall (r :: Natural) i a w (m :: Type -> Type).
(KnownNat r, MonadCircuit i a w m, Arithmetic a) =>
Natural -> i -> m [i]
expansionW @wordSize Natural
wordsPerReg) Vector k i
regs
    Vector (k * Ceil regSize wordSize) i
-> m (Vector (k * Ceil regSize wordSize) i)
forall a. a -> m a
forall (f :: Type -> Type) a. Applicative f => a -> f a
Haskell.pure (Vector (k * Ceil regSize wordSize) i
 -> m (Vector (k * Ceil regSize wordSize) i))
-> Vector (k * Ceil regSize wordSize) i
-> m (Vector (k * Ceil regSize wordSize) i)
forall a b. (a -> b) -> a -> b
$ Vector (k * Ceil regSize wordSize) i
-> Vector (k * Ceil regSize wordSize) i
forall (size :: Natural) a. Vector size a -> Vector size a
V.reverse (Vector (k * Ceil regSize wordSize) i
 -> Vector (k * Ceil regSize wordSize) i)
-> (Vector k [i] -> Vector (k * Ceil regSize wordSize) i)
-> Vector k [i]
-> Vector (k * Ceil regSize wordSize) i
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [i] -> Vector (k * Ceil regSize wordSize) i
forall (size :: Natural) a. [a] -> Vector size a
V.unsafeToVector ([i] -> Vector (k * Ceil regSize wordSize) i)
-> (Vector k [i] -> [i])
-> Vector k [i]
-> Vector (k * Ceil regSize wordSize) i
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [[i]] -> [i]
forall (t :: Type -> Type) a. Foldable t => t [a] -> [a]
Haskell.concat ([[i]] -> [i]) -> (Vector k [i] -> [[i]]) -> Vector k [i] -> [i]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Vector k [i] -> [[i]]
forall (size :: Natural) a. Vector size a -> [a]
V.fromVector (Vector k [i] -> Vector (k * Ceil regSize wordSize) i)
-> Vector k [i] -> Vector (k * Ceil regSize wordSize) i
forall a b. (a -> b) -> a -> b
$ Vector k [i]
words
  where
      wordsPerReg :: Natural
      wordsPerReg :: Natural
wordsPerReg = forall (n :: Natural). KnownNat n => Natural
value @(Ceil regSize wordSize)

-- | Word size in bits used in comparisons. Subject to change
type OrdWord = 16

instance ( Symbolic c, KnownNat n, KnownRegisterSize r
         , KnownRegisters c n r
         , regSize ~ GetRegisterSize (BaseField c) n r
         , KnownNat (Ceil regSize OrdWord)
         ) => 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 c (Vector (NumberOfRegisters (BaseField c) n r))
u1) >= :: UInt n r c -> UInt n r c -> Bool c
>= (UInt c (Vector (NumberOfRegisters (BaseField c) n r))
u2) =
        let w1 :: c (Vector
     (NumberOfRegisters (BaseField c) n r * Ceil regSize OrdWord))
w1 = forall (wordSize :: Natural) (regSize :: Natural)
       (ctx :: (Type -> Type) -> Type) (k :: Natural).
(Symbolic ctx, KnownNat (Ceil regSize wordSize),
 KnownNat wordSize) =>
ctx (Vector k) -> ctx (Vector (k * Ceil regSize wordSize))
asWords @OrdWord @regSize c (Vector (NumberOfRegisters (BaseField c) n r))
u1
            w2 :: c (Vector
     (NumberOfRegisters (BaseField c) n r * Ceil regSize OrdWord))
w2 = forall (wordSize :: Natural) (regSize :: Natural)
       (ctx :: (Type -> Type) -> Type) (k :: Natural).
(Symbolic ctx, KnownNat (Ceil regSize wordSize),
 KnownNat wordSize) =>
ctx (Vector k) -> ctx (Vector (k * Ceil regSize wordSize))
asWords @OrdWord @regSize c (Vector (NumberOfRegisters (BaseField c) n r))
u2
         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 @OrdWord c (Vector
     (NumberOfRegisters (BaseField c) n r * Ceil regSize OrdWord))
w1 c (Vector
     (NumberOfRegisters (BaseField c) n r * Ceil regSize OrdWord))
w2

    (UInt c (Vector (NumberOfRegisters (BaseField c) n r))
u1) > :: UInt n r c -> UInt n r c -> Bool c
> (UInt c (Vector (NumberOfRegisters (BaseField c) n r))
u2) =
        let w1 :: c (Vector
     (NumberOfRegisters (BaseField c) n r * Ceil regSize OrdWord))
w1 = forall (wordSize :: Natural) (regSize :: Natural)
       (ctx :: (Type -> Type) -> Type) (k :: Natural).
(Symbolic ctx, KnownNat (Ceil regSize wordSize),
 KnownNat wordSize) =>
ctx (Vector k) -> ctx (Vector (k * Ceil regSize wordSize))
asWords @OrdWord @regSize c (Vector (NumberOfRegisters (BaseField c) n r))
u1
            w2 :: c (Vector
     (NumberOfRegisters (BaseField c) n r * Ceil regSize OrdWord))
w2 = forall (wordSize :: Natural) (regSize :: Natural)
       (ctx :: (Type -> Type) -> Type) (k :: Natural).
(Symbolic ctx, KnownNat (Ceil regSize wordSize),
 KnownNat wordSize) =>
ctx (Vector k) -> ctx (Vector (k * Ceil regSize wordSize))
asWords @OrdWord @regSize c (Vector (NumberOfRegisters (BaseField c) n r))
u2
         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 @OrdWord c (Vector
     (NumberOfRegisters (BaseField c) n r * Ceil regSize OrdWord))
w1 c (Vector
     (NumberOfRegisters (BaseField c) n r * Ceil regSize OrdWord))
w2

    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))
-> CircuitFun
     '[Vector (NumberOfRegisters (BaseField c) n r),
       Vector (NumberOfRegisters (BaseField c) n r)]
     (Vector (NumberOfRegisters (BaseField c) n r))
     c
-> 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) -> CircuitFun '[f, g] h c -> 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
xv Vector (NumberOfRegisters (BaseField c) n r) i
yv -> do
            i
j <- ClosedPoly i (BaseField c) -> m i
forall var a w (m :: Type -> Type).
MonadCircuit var a w 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 w (m :: Type -> Type).
(Arithmetic a, MonadCircuit i a w 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 w (m :: Type -> Type).
MonadCircuit i a w 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 w (m :: Type -> Type).
(MonadCircuit i a w 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))
-> CircuitFun
     '[Vector (NumberOfRegisters (BaseField c) n r),
       Vector (NumberOfRegisters (BaseField c) n r)]
     (Vector (NumberOfRegisters (BaseField c) n r))
     c
-> 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) -> CircuitFun '[f, g] h c -> 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
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 w (m :: Type -> Type).
MonadCircuit i (BaseField c) w 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 w (m :: Type -> Type).
MonadCircuit i (BaseField c) w m =>
(i, i) -> ([i], [i]) -> (i, i) -> m [i]
solveN (i
i, i
j) ([i]
ris, [i]
rjs) (i
z, i
w)
        )
        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

            solve1 :: MonadCircuit i (BaseField c) w m => i -> i -> m [i]
            solve1 :: forall i w (m :: Type -> Type).
MonadCircuit i (BaseField c) w m =>
i -> i -> m [i]
solve1 i
i i
j = do
                i
z0 <- ClosedPoly i (BaseField c) -> m i
forall var a w (m :: Type -> Type).
MonadCircuit var a w 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)
                (i
z, i
_) <- Natural -> Natural -> i -> m (i, i)
forall i a w (m :: Type -> Type).
(MonadCircuit i a w 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) w m => (i, i) -> ([i], [i]) -> (i, i) -> m [i]
            solveN :: forall i w (m :: Type -> Type).
MonadCircuit i (BaseField c) w 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 w (m :: Type -> Type).
MonadCircuit var a w 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)
                let r :: Natural
r = forall a (n :: Natural) (r :: RegisterSize).
(Finite a, KnownNat n, KnownRegisterSize r) =>
Natural
registerSize @(BaseField c) @n @r
                (i
k, i
b0) <- Natural -> Natural -> i -> m (i, i)
forall i a w (m :: Type -> Type).
(MonadCircuit i a w m, Arithmetic a) =>
Natural -> Natural -> i -> m (i, i)
splitExpansion Natural
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 (Natural -> i -> i -> i -> m (i, i)
forall a i w (m :: Type -> Type).
(Arithmetic a, MonadCircuit i a w m) =>
Natural -> i -> i -> i -> m (i, i)
fullSub Natural
r) [i]
is [i]
js)
                i
d <- ClosedPoly i (BaseField c) -> m i
forall var a w (m :: Type -> Type).
MonadCircuit var a w 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 w (m :: Type -> Type).
MonadCircuit var a w 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
+ 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
highRegisterSize @(BaseField c) @n @r Natural -> Natural -> Natural
-! Natural
1 :: Natural))
                (i
s', i
_) <- Natural -> Natural -> i -> m (i, i)
forall i a w (m :: Type -> Type).
(MonadCircuit i a w 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'])

    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))
     c
-> c (Vector (NumberOfRegisters (BaseField c) n r))
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 c -> 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
xv -> do
            i
j <- ClosedPoly i (BaseField c) -> m i
forall var a w (m :: Type -> Type).
MonadCircuit var a w 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 w (m :: Type -> Type).
MonadCircuit i (BaseField c) w 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
        )
        where
            negateN :: MonadCircuit i (BaseField c) w m => Natural -> i -> i -> m (i, i)
            negateN :: forall i w (m :: Type -> Type).
MonadCircuit i (BaseField c) w 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 w (m :: Type -> Type).
MonadCircuit var a w 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 w (m :: Type -> Type).
(MonadCircuit i a w 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))
-> CircuitFun
     '[Vector (NumberOfRegisters (BaseField c) n rs),
       Vector (NumberOfRegisters (BaseField c) n rs)]
     (Vector (NumberOfRegisters (BaseField c) n rs))
     c
-> 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) -> CircuitFun '[f, g] h c -> 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
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 w (m :: Type -> Type).
MonadCircuit i (BaseField c) w 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 w (m :: Type -> Type).
MonadCircuit i (BaseField c) w m =>
(i, i) -> ([i], [i]) -> (i, i) -> m [i]
solveN (i
i, i
j) ([i]
ris, [i]
rjs) (i
z, i
w)
        )
        where
            solve1 :: forall i w m. MonadCircuit i (BaseField c) w m => i -> i -> m [i]
            solve1 :: forall i w (m :: Type -> Type).
MonadCircuit i (BaseField c) w m =>
i -> i -> m [i]
solve1 i
i i
j = do
                (i
z, i
_) <- ClosedPoly i (BaseField c) -> m i
forall var a w (m :: Type -> Type).
MonadCircuit var a w 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 w (m :: Type -> Type).
(MonadCircuit i a w 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 w m. MonadCircuit i (BaseField c) w m => (i, i) -> ([i], [i]) -> (i, i) -> m [i]
            solveN :: forall i w (m :: Type -> Type).
MonadCircuit i (BaseField c) w 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 w (m :: Type -> Type).
MonadCircuit var a w 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 w (m :: Type -> Type).
MonadCircuit var a w 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 w (m :: Type -> Type).
(MonadCircuit i a w 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 w (m :: Type -> Type).
MonadCircuit var a w 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 w (m :: Type -> Type).
(MonadCircuit i a w 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 w (m :: Type -> Type).
MonadCircuit var a w 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 w (m :: Type -> Type).
MonadCircuit var a w 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]
                let highOverflow :: Natural
highOverflow = forall a (n :: Natural) (r :: RegisterSize).
(Finite a, KnownNat n, KnownRegisterSize r) =>
Natural
registerSize @(BaseField c) @n @rs Natural -> Natural -> Natural
forall a. AdditiveSemigroup a => a -> a -> a
+ forall a (n :: Natural) (r :: RegisterSize).
(Finite a, KnownNat n, KnownRegisterSize r) =>
Natural
maxOverflow @(BaseField c) @n @rs Natural -> Natural -> Natural
-! forall a (n :: Natural) (r :: RegisterSize).
(Finite a, KnownNat n, KnownRegisterSize r) =>
Natural
highRegisterSize @(BaseField c) @n @rs
                (i
p', i
_) <- Natural -> Natural -> i -> m (i, i)
forall i a w (m :: Type -> Type).
(MonadCircuit i a w 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) Natural
highOverflow 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 newtype
         instance (Symbolic c, KnownRegisters 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)) c
-> c (Vector (NumberOfRegisters (BaseField c) n r))
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 c -> 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
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 w (m :: Type -> Type).
(MonadCircuit i a w 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 w (m :: Type -> Type).
   MonadCircuit v (BaseField c) w m =>
   [v] -> m [v]
forall a.
Natural
-> Natural
-> forall v w (m :: Type -> Type).
   MonadCircuit v a w 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))
-> CircuitFun
     '[Vector (NumberOfRegisters (BaseField c) n r),
       Vector (NumberOfRegisters (BaseField c) n r)]
     (Vector (NumberOfRegisters (BaseField c) n r))
     c
-> 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) -> CircuitFun '[f, g] h c -> 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
xv Vector (NumberOfRegisters (BaseField c) n r) i
yv -> do
            i
j <- ClosedPoly i (BaseField c) -> m i
forall var a w (m :: Type -> Type).
MonadCircuit var a w 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 w (m :: Type -> Type).
(Arithmetic a, MonadCircuit i a w 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 w (m :: Type -> Type).
MonadCircuit i a w 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 w (m :: Type -> Type).
(MonadCircuit i a w 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))
-> CircuitFun
     '[Vector (NumberOfRegisters (BaseField c) n r),
       Vector (NumberOfRegisters (BaseField c) n r)]
     (Vector (NumberOfRegisters (BaseField c) n r))
     c
-> 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) -> CircuitFun '[f, g] h c -> 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
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 w (m :: Type -> Type).
MonadCircuit i (BaseField c) w 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 w (m :: Type -> Type).
MonadCircuit i (BaseField c) w m =>
(i, i) -> ([i], [i]) -> (i, i) -> m [i]
solveN (i
i, i
j) ([i]
ris, [i]
rjs) (i
z, i
w)
        )
        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

            solve1 :: MonadCircuit i (BaseField c) w m => i -> i -> m [i]
            solve1 :: forall i w (m :: Type -> Type).
MonadCircuit i (BaseField c) w m =>
i -> i -> m [i]
solve1 i
i i
j = do
                i
z <- ClosedPoly i (BaseField c) -> m i
forall var a w (m :: Type -> Type).
MonadCircuit var a w 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 w (m :: Type -> Type).
(MonadCircuit i a w 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) w m => (i, i) -> ([i], [i]) -> (i, i) -> m [i]
            solveN :: forall i w (m :: Type -> Type).
MonadCircuit i (BaseField c) w 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 w (m :: Type -> Type).
MonadCircuit var a w 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))
                let r :: Natural
r = forall a (n :: Natural) (r :: RegisterSize).
(Finite a, KnownNat n, KnownRegisterSize r) =>
Natural
registerSize @(BaseField c) @n @r
                (i
k, i
b0) <- Natural -> Natural -> i -> m (i, i)
forall i a w (m :: Type -> Type).
(MonadCircuit i a w m, Arithmetic a) =>
Natural -> Natural -> i -> m (i, i)
splitExpansion Natural
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 (Natural -> i -> i -> i -> m (i, i)
forall a i w (m :: Type -> Type).
(Arithmetic a, MonadCircuit i a w m) =>
Natural -> i -> i -> i -> m (i, i)
fullSub Natural
r) [i]
is [i]
js)
                i
k' <- ClosedPoly i (BaseField c) -> m i
forall var a w (m :: Type -> Type).
MonadCircuit var a w 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 w (m :: Type -> Type).
MonadCircuit var a w 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 w (m :: Type -> Type).
(MonadCircuit i a w 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'])

    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))
-> CircuitFun
     '[Vector (NumberOfRegisters (BaseField c) n r),
       Vector (NumberOfRegisters (BaseField c) n r)]
     (Vector (NumberOfRegisters (BaseField c) n r))
     c
-> 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) -> CircuitFun '[f, g] h c -> 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
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 w (m :: Type -> Type).
MonadCircuit i (BaseField c) w 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 w (m :: Type -> Type).
MonadCircuit i (BaseField c) w m =>
(i, i) -> ([i], [i]) -> (i, i) -> m [i]
solveN (i
i, i
j) ([i]
ris, [i]
rjs) (i
z, i
w)
        )
        where
            solve1 :: MonadCircuit i (BaseField c) w m => i -> i -> m [i]
            solve1 :: forall i w (m :: Type -> Type).
MonadCircuit i (BaseField c) w m =>
i -> i -> m [i]
solve1 i
i i
j = do
                i
z <- ClosedPoly i (BaseField c) -> m i
forall var a w (m :: Type -> Type).
MonadCircuit var a w 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 w (m :: Type -> Type).
(MonadCircuit i a w 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) w m => (i, i) -> ([i], [i]) -> (i, i) -> m [i]
            solveN :: forall i w (m :: Type -> Type).
MonadCircuit i (BaseField c) w 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 w (m :: Type -> Type).
MonadCircuit var a w 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 w (m :: Type -> Type).
MonadCircuit var a w 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 w (m :: Type -> Type).
(MonadCircuit i a w 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 w (m :: Type -> Type).
MonadCircuit var a w 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 w (m :: Type -> Type).
(MonadCircuit i a w 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 w (m :: Type -> Type).
MonadCircuit var a w 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 w (m :: Type -> Type).
MonadCircuit var a w 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 w (m :: Type -> Type).
(MonadCircuit i a w 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 w (m :: Type -> Type).
MonadCircuit var a w 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
  , KnownRegisters 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
$ Context (UInt n r c) (Vector (NumberOfRegisters (BaseField c) n r))
-> (forall {i} {m :: Type -> Type}.
    (NFData i,
     MonadCircuit
       i
       (BaseField (Context (UInt n r c)))
       (WitnessField (Context (UInt n r c)))
       m) =>
    FunBody '[Vector (NumberOfRegisters (BaseField c) n r)] Par1 i m)
-> Context (UInt n r c) Par1
forall (f :: Type -> Type) (g :: Type -> Type).
Context (UInt n r c) f
-> CircuitFun '[f] g (Context (UInt n r c))
-> Context (UInt n r c) g
forall (c :: (Type -> Type) -> Type) (f :: Type -> Type)
       (g :: Type -> Type).
Symbolic c =>
c f -> CircuitFun '[f] g c -> c g
fromCircuitF c (Vector (NumberOfRegisters (BaseField c) n r))
Context (UInt n r c) (Vector (NumberOfRegisters (BaseField c) n r))
bits ((forall {i} {m :: Type -> Type}.
  (NFData i,
   MonadCircuit
     i
     (BaseField (Context (UInt n r c)))
     (WitnessField (Context (UInt n r c)))
     m) =>
  FunBody '[Vector (NumberOfRegisters (BaseField c) n r)] Par1 i m)
 -> Context (UInt n r c) Par1)
-> (forall {i} {m :: Type -> Type}.
    (NFData i,
     MonadCircuit
       i
       (BaseField (Context (UInt n r c)))
       (WitnessField (Context (UInt n r c)))
       m) =>
    FunBody '[Vector (NumberOfRegisters (BaseField c) n r)] Par1 i m)
-> Context (UInt n r c) Par1
forall a b. (a -> b) -> a -> b
$ \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 w (m :: Type -> Type).
(MonadCircuit v a w 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 w (m :: Type -> Type).
   MonadCircuit v (BaseField c) w m =>
   [v] -> m [v]
forall a.
Natural
-> Natural
-> forall v w (m :: Type -> Type).
   MonadCircuit v a w 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 w (m :: Type -> Type).
MonadCircuit var a w 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 w (m :: Type -> Type) (f :: Type -> Type).
(MonadCircuit i a w 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
        case [Par1 i]
isZeros 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 (BaseField c) -> m i
forall var a w (m :: Type -> Type).
MonadCircuit var a w 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
z : [Par1 i]
zs) -> (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 (BaseField c) -> m i
forall var a w (m :: Type -> Type).
MonadCircuit var a w 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
z [Par1 i]
zs

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

fullAdder :: (Arithmetic a, MonadCircuit i a w m) => Natural -> i -> i -> i -> m (i, i)
fullAdder :: forall a i w (m :: Type -> Type).
(Arithmetic a, MonadCircuit i a w 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 w (m :: Type -> Type).
MonadCircuit i a w 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 w (m :: Type -> Type).
(MonadCircuit i a w m, Arithmetic a) =>
Natural -> Natural -> i -> m (i, i)
splitExpansion Natural
r Natural
1

fullAdded :: MonadCircuit i a w m => i -> i -> i -> m i
fullAdded :: forall i a w (m :: Type -> Type).
MonadCircuit i a w m =>
i -> i -> i -> m i
fullAdded i
i i
j i
c = do
    i
k <- ClosedPoly i a -> m i
forall var a w (m :: Type -> Type).
MonadCircuit var a w 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 w (m :: Type -> Type).
MonadCircuit var a w 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)

fullSub :: (Arithmetic a, MonadCircuit i a w m) => Natural -> i -> i -> i -> m (i, i)
fullSub :: forall a i w (m :: Type -> Type).
(Arithmetic a, MonadCircuit i a w m) =>
Natural -> i -> i -> i -> m (i, i)
fullSub Natural
r i
xk i
yk i
b = do
    i
d <- ClosedPoly i a -> m i
forall var a w (m :: Type -> Type).
MonadCircuit var a w 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 a -> m i
forall var a w (m :: Type -> Type).
MonadCircuit var a w 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
+ (x
forall a. MultiplicativeMonoid a => a
one x -> x -> x
forall a. AdditiveSemigroup a => a -> a -> a
+ x
forall a. MultiplicativeMonoid a => a
one) x -> Natural -> x
forall a b. Exponent a b => a -> b -> a
^ Natural
r x -> x -> x
forall a. AdditiveGroup a => a -> a -> a
- x
forall a. MultiplicativeMonoid a => a
one)
    Natural -> Natural -> i -> m (i, i)
forall i a w (m :: Type -> Type).
(MonadCircuit i a w m, Arithmetic a) =>
Natural -> Natural -> i -> m (i, i)
splitExpansion Natural
r Natural
1 i
s

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