{-# LANGUAGE AllowAmbiguousTypes  #-}
{-# LANGUAGE BlockArguments       #-}
{-# LANGUAGE DerivingVia          #-}
{-# LANGUAGE NoDeriveAnyClass     #-}
{-# LANGUAGE ScopedTypeVariables  #-}
{-# 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.Applicative               (Applicative (..))
import           Control.DeepSeq
import           Control.Monad.State               (StateT (..))
import           Data.Aeson                        hiding (Bool)
import           Data.Foldable                     (foldlM, foldr, foldrM, for_)
import           Data.Function                     (on)
import           Data.Functor                      ((<$>))
import           Data.Functor.Rep                  (Representable (..))
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           ZkFold.Base.Control.HApplicative  (HApplicative (..))
import           ZkFold.Base.Data.HFunctor         (HFunctor (..))
import           ZkFold.Base.Data.Product          (fstP, sndP)
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 (..), Witness (..), 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)
deriving newtype instance (KnownRegisters c n r, Symbolic c) => Conditional (Bool c) (UInt n r c)
deriving newtype instance (KnownRegisters c n r, Symbolic c) => Eq (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
ifThenElse (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)
    => 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)) =>
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 -> BooleanOf (UInt n r c)
forall a. Eq a => a -> a -> BooleanOf a
== 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 -> BooleanOf Natural
forall a. Eq a => a -> a -> BooleanOf a
== 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, KnownRegisterSize r
         , KnownRegisters c n r
         , regSize ~ GetRegisterSize (BaseField c) n r
         , KnownNat (Ceil regSize OrdWord)
         ) => SemiEuclidean (UInt n r c) where
    divMod :: UInt n r c -> UInt n r c -> (UInt n r c, UInt n r c)
divMod num :: UInt n r c
num@(UInt c (Vector (NumberOfRegisters (BaseField c) n r))
nm) den :: UInt n r c
den@(UInt c (Vector (NumberOfRegisters (BaseField c) n r))
dn) =
      (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
$ (forall a.
 (:*:)
   (Vector (NumberOfRegisters (BaseField c) n r))
   (Vector (NumberOfRegisters (BaseField c) n r))
   a
 -> Vector (NumberOfRegisters (BaseField c) n r) a)
-> c (Vector (NumberOfRegisters (BaseField c) n r)
      :*: Vector (NumberOfRegisters (BaseField c) n r))
-> c (Vector (NumberOfRegisters (BaseField c) n r))
forall {k} (c :: (k -> Type) -> Type) (f :: k -> Type)
       (g :: k -> Type).
HFunctor c =>
(forall (a :: k). f a -> g a) -> c f -> c g
forall (f :: Type -> Type) (g :: Type -> Type).
(forall a. f a -> g a) -> c f -> c g
hmap (:*:)
  (Vector (NumberOfRegisters (BaseField c) n r))
  (Vector (NumberOfRegisters (BaseField c) n r))
  a
-> Vector (NumberOfRegisters (BaseField c) n r) a
forall a.
(:*:)
  (Vector (NumberOfRegisters (BaseField c) n r))
  (Vector (NumberOfRegisters (BaseField c) n r))
  a
-> Vector (NumberOfRegisters (BaseField c) n r) a
forall {k} (f :: k -> Type) (g :: k -> Type) (a :: k).
(:*:) f g a -> f a
fstP c (Vector (NumberOfRegisters (BaseField c) n r)
   :*: Vector (NumberOfRegisters (BaseField c) n r))
circuit, 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
$ (forall a.
 (:*:)
   (Vector (NumberOfRegisters (BaseField c) n r))
   (Vector (NumberOfRegisters (BaseField c) n r))
   a
 -> Vector (NumberOfRegisters (BaseField c) n r) a)
-> c (Vector (NumberOfRegisters (BaseField c) n r)
      :*: Vector (NumberOfRegisters (BaseField c) n r))
-> c (Vector (NumberOfRegisters (BaseField c) n r))
forall {k} (c :: (k -> Type) -> Type) (f :: k -> Type)
       (g :: k -> Type).
HFunctor c =>
(forall (a :: k). f a -> g a) -> c f -> c g
forall (f :: Type -> Type) (g :: Type -> Type).
(forall a. f a -> g a) -> c f -> c g
hmap (:*:)
  (Vector (NumberOfRegisters (BaseField c) n r))
  (Vector (NumberOfRegisters (BaseField c) n r))
  a
-> Vector (NumberOfRegisters (BaseField c) n r) a
forall a.
(:*:)
  (Vector (NumberOfRegisters (BaseField c) n r))
  (Vector (NumberOfRegisters (BaseField c) n r))
  a
-> Vector (NumberOfRegisters (BaseField c) n r) a
forall {k} (f :: k -> Type) (g :: k -> Type) (a :: k).
(:*:) f g a -> g a
sndP c (Vector (NumberOfRegisters (BaseField c) n r)
   :*: Vector (NumberOfRegisters (BaseField c) n r))
circuit)
      where
        -- | "natural" value from vector of registers.
        natural ::
          forall m i. Witness i (WitnessField c) =>
          Vector m i -> Const (WitnessField c)
        natural :: forall (m :: Natural) i.
Witness i (WitnessField c) =>
Vector m i -> Const (WitnessField c)
natural = (i -> Const (WitnessField c) -> Const (WitnessField c))
-> Const (WitnessField c) -> Vector m i -> Const (WitnessField c)
forall a b. (a -> b -> b) -> b -> Vector m a -> b
forall (t :: Type -> Type) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\i
i Const (WitnessField c)
c -> WitnessField c -> Const (WitnessField c)
forall a. ToConstant a => a -> Const a
toConstant (i -> WitnessField c
forall i w. Witness i w => i -> w
at i
i :: WitnessField c) Const (WitnessField c)
-> Const (WitnessField c) -> Const (WitnessField c)
forall a. AdditiveSemigroup a => a -> a -> a
+ Natural -> Const (WitnessField c)
forall a b. FromConstant a b => a -> b
fromConstant Natural
base Const (WitnessField c)
-> Const (WitnessField c) -> Const (WitnessField c)
forall a. MultiplicativeSemigroup a => a -> a -> a
* Const (WitnessField c)
c) Const (WitnessField c)
forall a. AdditiveMonoid a => a
zero
          where
            base :: Natural
            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 @(BaseField c) @n @r

        -- | @register n i@ returns @i@-th register of @n@.
        register :: forall m. Const (WitnessField c) -> Zp m -> WitnessField c
        register :: forall (m :: Natural).
Const (WitnessField c) -> Zp m -> WitnessField c
register Const (WitnessField c)
c Zp m
i =
          Const (WitnessField c) -> WitnessField c
forall a b. FromConstant a b => a -> b
fromConstant ((Const (WitnessField c)
c Const (WitnessField c)
-> Const (WitnessField c) -> Const (WitnessField c)
forall a. SemiEuclidean a => a -> a -> a
`div` Natural -> Const (WitnessField c)
forall a b. FromConstant a b => a -> b
fromConstant (Natural
2 Natural -> Natural -> Natural
forall a b. Exponent a b => a -> b -> a
^ Natural
shift :: Natural)) Const (WitnessField c)
-> Const (WitnessField c) -> Const (WitnessField c)
forall a. SemiEuclidean a => a -> a -> a
`mod` Const (WitnessField c)
base)
          where
            rs :: Natural
rs = forall a (n :: Natural) (r :: RegisterSize).
(Finite a, KnownNat n, KnownRegisterSize r) =>
Natural
registerSize @(BaseField c) @n @r
            base :: Const (WitnessField c)
base = Natural -> Const (WitnessField c)
forall a b. FromConstant a b => a -> b
fromConstant (Natural
2 Natural -> Natural -> Natural
forall a b. Exponent a b => a -> b -> a
^ Natural
rs :: Natural)
            shift :: Natural
shift = Zp m -> Const (Zp m)
forall a. ToConstant a => a -> Const a
toConstant Zp m
i Natural -> Natural -> Natural
forall a. MultiplicativeSemigroup a => a -> a -> a
* Natural
rs

        -- | Computes unconstrained registers of @div@ and @mod@.
        source :: c (Vector (NumberOfRegisters (BaseField c) n r)
   :*: Vector (NumberOfRegisters (BaseField c) n r))
source = 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))
         (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)
      :*: Vector (NumberOfRegisters (BaseField c) n r))
     c
-> c (Vector (NumberOfRegisters (BaseField c) n r)
      :*: 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))
nm c (Vector (NumberOfRegisters (BaseField c) n r))
dn
          (\Vector (NumberOfRegisters (BaseField c) n r) (BaseField c)
n Vector (NumberOfRegisters (BaseField c) n r) (BaseField c)
d ->
            let r :: Natural
r = forall a (n :: Natural) (r :: RegisterSize).
(Finite a, KnownNat n, KnownRegisterSize r) =>
Natural
registerSize @(BaseField c) @n @r
                n' :: Natural
n' = 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)
n Natural
r
                d' :: Natural
d' = 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)
d Natural
r
            in 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
n' Natural -> Natural -> Natural
forall a. SemiEuclidean a => a -> a -> a
`div` Natural
d')
                Vector (NumberOfRegisters (BaseField c) n r) (BaseField c)
-> Vector (NumberOfRegisters (BaseField c) n r) (BaseField c)
-> (:*:)
     (Vector (NumberOfRegisters (BaseField c) n r))
     (Vector (NumberOfRegisters (BaseField c) n r))
     (BaseField c)
forall k (f :: k -> Type) (g :: k -> Type) (p :: k).
f p -> g p -> (:*:) f g p
:*: 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
n' Natural -> Natural -> Natural
forall a. SemiEuclidean a => a -> a -> a
`mod` Natural
d'))
          \Vector (NumberOfRegisters (BaseField c) n r) i
n Vector (NumberOfRegisters (BaseField c) n r) i
d -> ((Vector (NumberOfRegisters (BaseField c) n r) i
 -> Vector (NumberOfRegisters (BaseField c) n r) i
 -> (:*:)
      (Vector (NumberOfRegisters (BaseField c) n r))
      (Vector (NumberOfRegisters (BaseField c) n r))
      i)
-> m (Vector (NumberOfRegisters (BaseField c) n r) i)
-> m (Vector (NumberOfRegisters (BaseField c) n r) i)
-> m ((:*:)
        (Vector (NumberOfRegisters (BaseField c) n r))
        (Vector (NumberOfRegisters (BaseField c) n r))
        i)
forall a b c. (a -> b -> c) -> m a -> m b -> m c
forall (f :: Type -> Type) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 Vector (NumberOfRegisters (BaseField c) n r) i
-> Vector (NumberOfRegisters (BaseField c) n r) i
-> (:*:)
     (Vector (NumberOfRegisters (BaseField c) n r))
     (Vector (NumberOfRegisters (BaseField c) n r))
     i
forall k (f :: k -> Type) (g :: k -> Type) (p :: k).
f p -> g p -> (:*:) f g p
(:*:) (m (Vector (NumberOfRegisters (BaseField c) n r) i)
 -> m (Vector (NumberOfRegisters (BaseField c) n r) i)
 -> m ((:*:)
         (Vector (NumberOfRegisters (BaseField c) n r))
         (Vector (NumberOfRegisters (BaseField c) n r))
         i))
-> (Vector (NumberOfRegisters (BaseField c) n r) (WitnessField c)
    -> m (Vector (NumberOfRegisters (BaseField c) n r) i))
-> Vector (NumberOfRegisters (BaseField c) n r) (WitnessField c)
-> Vector (NumberOfRegisters (BaseField c) n r) (WitnessField c)
-> m ((:*:)
        (Vector (NumberOfRegisters (BaseField c) n r))
        (Vector (NumberOfRegisters (BaseField c) n r))
        i)
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` (WitnessField c -> m i)
-> Vector (NumberOfRegisters (BaseField c) n r) (WitnessField c)
-> m (Vector (NumberOfRegisters (BaseField c) n r) 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)
-> Vector (NumberOfRegisters (BaseField c) n r) a
-> f (Vector (NumberOfRegisters (BaseField c) n r) b)
traverse WitnessField c -> m i
forall var a w (m :: Type -> Type).
MonadCircuit var a w m =>
w -> m var
unconstrained)
            ((Rep (Vector (NumberOfRegisters (BaseField c) n r))
 -> WitnessField c)
-> Vector (NumberOfRegisters (BaseField c) n r) (WitnessField c)
forall a.
(Rep (Vector (NumberOfRegisters (BaseField c) n r)) -> a)
-> Vector (NumberOfRegisters (BaseField c) n r) a
forall (f :: Type -> Type) a.
Representable f =>
(Rep f -> a) -> f a
tabulate ((Rep (Vector (NumberOfRegisters (BaseField c) n r))
  -> WitnessField c)
 -> Vector (NumberOfRegisters (BaseField c) n r) (WitnessField c))
-> (Rep (Vector (NumberOfRegisters (BaseField c) n r))
    -> WitnessField c)
-> Vector (NumberOfRegisters (BaseField c) n r) (WitnessField c)
forall a b. (a -> b) -> a -> b
$ Const (WitnessField c)
-> Zp (NumberOfRegisters (BaseField c) n r) -> WitnessField c
forall (m :: Natural).
Const (WitnessField c) -> Zp m -> WitnessField c
register (Vector (NumberOfRegisters (BaseField c) n r) i
-> Const (WitnessField c)
forall (m :: Natural) i.
Witness i (WitnessField c) =>
Vector m i -> Const (WitnessField c)
natural Vector (NumberOfRegisters (BaseField c) n r) i
n Const (WitnessField c)
-> Const (WitnessField c) -> Const (WitnessField c)
forall a. SemiEuclidean a => a -> a -> a
`div` Vector (NumberOfRegisters (BaseField c) n r) i
-> Const (WitnessField c)
forall (m :: Natural) i.
Witness i (WitnessField c) =>
Vector m i -> Const (WitnessField c)
natural Vector (NumberOfRegisters (BaseField c) n r) i
d))
            ((Rep (Vector (NumberOfRegisters (BaseField c) n r))
 -> WitnessField c)
-> Vector (NumberOfRegisters (BaseField c) n r) (WitnessField c)
forall a.
(Rep (Vector (NumberOfRegisters (BaseField c) n r)) -> a)
-> Vector (NumberOfRegisters (BaseField c) n r) a
forall (f :: Type -> Type) a.
Representable f =>
(Rep f -> a) -> f a
tabulate ((Rep (Vector (NumberOfRegisters (BaseField c) n r))
  -> WitnessField c)
 -> Vector (NumberOfRegisters (BaseField c) n r) (WitnessField c))
-> (Rep (Vector (NumberOfRegisters (BaseField c) n r))
    -> WitnessField c)
-> Vector (NumberOfRegisters (BaseField c) n r) (WitnessField c)
forall a b. (a -> b) -> a -> b
$ Const (WitnessField c)
-> Zp (NumberOfRegisters (BaseField c) n r) -> WitnessField c
forall (m :: Natural).
Const (WitnessField c) -> Zp m -> WitnessField c
register (Vector (NumberOfRegisters (BaseField c) n r) i
-> Const (WitnessField c)
forall (m :: Natural) i.
Witness i (WitnessField c) =>
Vector m i -> Const (WitnessField c)
natural Vector (NumberOfRegisters (BaseField c) n r) i
n Const (WitnessField c)
-> Const (WitnessField c) -> Const (WitnessField c)
forall a. SemiEuclidean a => a -> a -> a
`mod` Vector (NumberOfRegisters (BaseField c) n r) i
-> Const (WitnessField c)
forall (m :: Natural) i.
Witness i (WitnessField c) =>
Vector m i -> Const (WitnessField c)
natural Vector (NumberOfRegisters (BaseField c) n r) i
d))

        -- | Unconstrained @div@ part.
        dv :: c (Vector (NumberOfRegisters (BaseField c) n r))
dv = (forall a.
 (:*:)
   (Vector (NumberOfRegisters (BaseField c) n r))
   (Vector (NumberOfRegisters (BaseField c) n r))
   a
 -> Vector (NumberOfRegisters (BaseField c) n r) a)
-> c (Vector (NumberOfRegisters (BaseField c) n r)
      :*: Vector (NumberOfRegisters (BaseField c) n r))
-> c (Vector (NumberOfRegisters (BaseField c) n r))
forall {k} (c :: (k -> Type) -> Type) (f :: k -> Type)
       (g :: k -> Type).
HFunctor c =>
(forall (a :: k). f a -> g a) -> c f -> c g
forall (f :: Type -> Type) (g :: Type -> Type).
(forall a. f a -> g a) -> c f -> c g
hmap (:*:)
  (Vector (NumberOfRegisters (BaseField c) n r))
  (Vector (NumberOfRegisters (BaseField c) n r))
  a
-> Vector (NumberOfRegisters (BaseField c) n r) a
forall a.
(:*:)
  (Vector (NumberOfRegisters (BaseField c) n r))
  (Vector (NumberOfRegisters (BaseField c) n r))
  a
-> Vector (NumberOfRegisters (BaseField c) n r) a
forall {k} (f :: k -> Type) (g :: k -> Type) (a :: k).
(:*:) f g a -> f a
fstP c (Vector (NumberOfRegisters (BaseField c) n r)
   :*: Vector (NumberOfRegisters (BaseField c) n r))
source

        -- | Unconstrained @mod@ part.
        md :: c (Vector (NumberOfRegisters (BaseField c) n r))
md = (forall a.
 (:*:)
   (Vector (NumberOfRegisters (BaseField c) n r))
   (Vector (NumberOfRegisters (BaseField c) n r))
   a
 -> Vector (NumberOfRegisters (BaseField c) n r) a)
-> c (Vector (NumberOfRegisters (BaseField c) n r)
      :*: Vector (NumberOfRegisters (BaseField c) n r))
-> c (Vector (NumberOfRegisters (BaseField c) n r))
forall {k} (c :: (k -> Type) -> Type) (f :: k -> Type)
       (g :: k -> Type).
HFunctor c =>
(forall (a :: k). f a -> g a) -> c f -> c g
forall (f :: Type -> Type) (g :: Type -> Type).
(forall a. f a -> g a) -> c f -> c g
hmap (:*:)
  (Vector (NumberOfRegisters (BaseField c) n r))
  (Vector (NumberOfRegisters (BaseField c) n r))
  a
-> Vector (NumberOfRegisters (BaseField c) n r) a
forall a.
(:*:)
  (Vector (NumberOfRegisters (BaseField c) n r))
  (Vector (NumberOfRegisters (BaseField c) n r))
  a
-> Vector (NumberOfRegisters (BaseField c) n r) a
forall {k} (f :: k -> Type) (g :: k -> Type) (a :: k).
(:*:) f g a -> g a
sndP c (Vector (NumberOfRegisters (BaseField c) n r)
   :*: Vector (NumberOfRegisters (BaseField c) n r))
source

        -- | divMod first constraint: @numerator = denominator * div + mod@.
        -- This should always be true.
        Bool c Par1
eq = UInt n r c
den UInt n r c -> UInt n r c -> UInt n r c
forall a. MultiplicativeSemigroup a => a -> a -> 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))
dv UInt n r c -> UInt n r c -> UInt n r c
forall a. AdditiveSemigroup a => a -> a -> 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))
md UInt n r c -> UInt n r c -> BooleanOf (UInt n r c)
forall a. Eq a => a -> a -> BooleanOf a
== UInt n r c
num

        -- | divMod second constraint: @0 <= mod < denominator@.
        -- This should always be true.
        Bool c Par1
lt = 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))
md UInt n r c -> UInt n r c -> Bool c
forall b a. Ord b a => a -> a -> b
< UInt n r c
den

        -- | Computes properly constrained registers of @div@ and @mod@.
        circuit :: c (Vector (NumberOfRegisters (BaseField c) n r)
   :*: Vector (NumberOfRegisters (BaseField c) n r))
circuit = c Par1
-> c Par1
-> c (Vector (NumberOfRegisters (BaseField c) n r)
      :*: Vector (NumberOfRegisters (BaseField c) n r))
-> CircuitFun
     '[Par1, Par1,
       Vector (NumberOfRegisters (BaseField c) n r)
       :*: 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)
      :*: Vector (NumberOfRegisters (BaseField c) n r))
forall (c :: (Type -> Type) -> Type) (f :: Type -> Type)
       (g :: Type -> Type) (h :: Type -> Type) (k :: Type -> Type).
Symbolic c =>
c f -> c g -> c h -> CircuitFun '[f, g, h] k c -> c k
fromCircuit3F c Par1
eq c Par1
lt (c (Vector (NumberOfRegisters (BaseField c) n r))
dv c (Vector (NumberOfRegisters (BaseField c) n r))
-> c (Vector (NumberOfRegisters (BaseField c) n r))
-> c (Vector (NumberOfRegisters (BaseField c) n r)
      :*: Vector (NumberOfRegisters (BaseField c) n r))
forall {k} (c :: (k -> Type) -> Type) (f :: k -> Type)
       (g :: k -> Type).
HApplicative c =>
c f -> c g -> c (f :*: g)
forall (f :: Type -> Type) (g :: Type -> Type).
c f -> c g -> c (f :*: g)
`hpair` c (Vector (NumberOfRegisters (BaseField c) n r))
md) \(Par1 i
e) (Par1 i
l) (:*:)
  (Vector (NumberOfRegisters (BaseField c) n r))
  (Vector (NumberOfRegisters (BaseField c) n r))
  i
dm -> do
          ClosedPoly i (BaseField c) -> m ()
forall var a w (m :: Type -> Type).
MonadCircuit var a w m =>
ClosedPoly var a -> m ()
constraint (((i -> x) -> i -> x
forall a b. (a -> b) -> a -> b
$ i
e) ((i -> x) -> x) -> ((i -> x) -> x) -> (i -> x) -> x
forall a. AdditiveGroup a => a -> a -> a
- (i -> x) -> x
forall a. MultiplicativeMonoid a => a
one)
          ClosedPoly i (BaseField c) -> m ()
forall var a w (m :: Type -> Type).
MonadCircuit var a w m =>
ClosedPoly var a -> m ()
constraint (((i -> x) -> i -> x
forall a b. (a -> b) -> a -> b
$ i
l) ((i -> x) -> x) -> ((i -> x) -> x) -> (i -> x) -> x
forall a. AdditiveGroup a => a -> a -> a
- (i -> x) -> x
forall a. MultiplicativeMonoid a => a
one)
          (:*:)
  (Vector (NumberOfRegisters (BaseField c) n r))
  (Vector (NumberOfRegisters (BaseField c) n r))
  i
-> m ((:*:)
        (Vector (NumberOfRegisters (BaseField c) n r))
        (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))
  (Vector (NumberOfRegisters (BaseField c) n r))
  i
dm

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)

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

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