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

module ZkFold.Symbolic.Data.VarByteString
    ( VarByteString (..)
    , fromNatural
    , fromByteString
    , toAsciiString
    , append
    , (@+)
    , shiftL
    , shiftR
    , wipeUnassigned
    ) where

import           Control.DeepSeq                   (NFData)
import           Control.Monad                     (mapM)
import           Data.Aeson                        (FromJSON (..))
import qualified Data.ByteString                   as Bytes
import           Data.Char                         (chr)
import           Data.Constraint
import           Data.Constraint.Nat
import           Data.Constraint.Unsafe
import           Data.Foldable                     (foldlM, foldrM)
import           Data.Functor.Rep                  (Representable (..))
import           Data.Kind                         (Type)
import           Data.List.Split                   (chunksOf)
import           Data.Proxy                        (Proxy (..))
import           Data.String                       (IsString (..))
import           GHC.Generics                      (Generic, Par1 (..))
import           GHC.TypeLits                      (KnownSymbol (..), symbolVal, withKnownNat)
import           Prelude                           (const, fmap, otherwise, pure, type (~), ($), (.), (<$>), (<>))
import qualified Prelude                           as Haskell
import           Test.QuickCheck                   (Arbitrary (..), chooseInteger)

import           ZkFold.Base.Algebra.Basic.Class
import           ZkFold.Base.Algebra.Basic.Field
import           ZkFold.Base.Algebra.Basic.Number
import           ZkFold.Base.Data.Vector           (Vector, chunks, fromVector, unsafeToVector)
import           ZkFold.Prelude                    (drop, length, replicate, take)
import           ZkFold.Symbolic.Class
import           ZkFold.Symbolic.Data.Bool         (Bool (..))
import           ZkFold.Symbolic.Data.ByteString   (ByteString (..), isSet, orRight)
import           ZkFold.Symbolic.Data.Class        (SymbolicData)
import           ZkFold.Symbolic.Data.Combinators  hiding (regSize)
import           ZkFold.Symbolic.Data.Conditional  (Conditional, bool)
import           ZkFold.Symbolic.Data.Eq           (Eq)
import           ZkFold.Symbolic.Data.FieldElement (FieldElement (..))
import           ZkFold.Symbolic.Data.Input        (SymbolicInput)
import           ZkFold.Symbolic.Interpreter
import           ZkFold.Symbolic.MonadCircuit      (MonadCircuit, newAssigned)

-- | A ByteString that has length unknown at compile time but guaranteed to not exceed @maxLen@.
-- The unassigned buffer space (i.e. bits past @bsLength@) should be set to zero at all times.
--
-- TODO: Declare all the instances ByteString has for VarByteString
--
data VarByteString (maxLen :: Natural) (context :: (Type -> Type) -> Type) =
    VarByteString
        { forall (maxLen :: Natural) (context :: (Type -> Type) -> Type).
VarByteString maxLen context -> FieldElement context
bsLength :: FieldElement context
        , forall (maxLen :: Natural) (context :: (Type -> Type) -> Type).
VarByteString maxLen context -> ByteString maxLen context
bsBuffer :: ByteString maxLen context
        }
    deriving ((forall x.
 VarByteString maxLen context
 -> Rep (VarByteString maxLen context) x)
-> (forall x.
    Rep (VarByteString maxLen context) x
    -> VarByteString maxLen context)
-> Generic (VarByteString maxLen context)
forall (maxLen :: Natural) (context :: (Type -> Type) -> Type) x.
Rep (VarByteString maxLen context) x
-> VarByteString maxLen context
forall (maxLen :: Natural) (context :: (Type -> Type) -> Type) x.
VarByteString maxLen context
-> Rep (VarByteString maxLen context) x
forall x.
Rep (VarByteString maxLen context) x
-> VarByteString maxLen context
forall x.
VarByteString maxLen context
-> Rep (VarByteString maxLen context) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall (maxLen :: Natural) (context :: (Type -> Type) -> Type) x.
VarByteString maxLen context
-> Rep (VarByteString maxLen context) x
from :: forall x.
VarByteString maxLen context
-> Rep (VarByteString maxLen context) x
$cto :: forall (maxLen :: Natural) (context :: (Type -> Type) -> Type) x.
Rep (VarByteString maxLen context) x
-> VarByteString maxLen context
to :: forall x.
Rep (VarByteString maxLen context) x
-> VarByteString maxLen context
Generic)

deriving stock instance (Haskell.Show (ctx (Vector n)), Haskell.Show (ctx Par1)) => Haskell.Show (VarByteString n ctx)
deriving stock instance (Haskell.Eq (ctx (Vector n)), Haskell.Eq (ctx Par1)) => Haskell.Eq (VarByteString n ctx)
deriving anyclass instance (NFData (ctx (Vector n)), NFData (ctx Par1)) => NFData (VarByteString n ctx)
deriving instance (KnownNat n, Symbolic ctx) => SymbolicData (VarByteString n ctx)
deriving instance (KnownNat n, Symbolic ctx) => SymbolicInput (VarByteString n ctx)
deriving instance (Symbolic ctx, KnownNat n) => Eq (VarByteString n ctx)
deriving instance (Symbolic ctx, KnownNat n) => Conditional (Bool ctx) (VarByteString n ctx)

instance (KnownNat maxLen, Symbolic ctx) => Arbitrary (VarByteString maxLen ctx) where
    arbitrary :: Gen (VarByteString maxLen ctx)
arbitrary = do
        Natural
nbits <- Integer -> Natural
forall a b. (Integral a, Num b) => a -> b
Haskell.fromIntegral (Integer -> Natural) -> Gen Integer -> Gen Natural
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> (Integer, Integer) -> Gen Integer
chooseInteger (Integer
0, Natural -> Integer
forall a b. (Integral a, Num b) => a -> b
Haskell.fromIntegral (Natural -> Integer) -> Natural -> Integer
forall a b. (a -> b) -> a -> b
$ forall (n :: Natural). KnownNat n => Natural
value @maxLen)
        Natural
bits  <- Integer -> Natural
forall a b. (Integral a, Num b) => a -> b
Haskell.fromIntegral (Integer -> Natural) -> Gen Integer -> Gen Natural
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> (Integer, Integer) -> Gen Integer
chooseInteger (Integer
0, Natural -> Integer
forall a b. (Integral a, Num b) => a -> b
Haskell.fromIntegral (Natural -> Integer) -> Natural -> Integer
forall a b. (a -> b) -> a -> b
$ Natural
2Natural -> Natural -> Natural
forall a b. Exponent a b => a -> b -> a
^Natural
nbits Natural -> Natural -> Natural
-! Natural
1)
        VarByteString maxLen ctx -> Gen (VarByteString maxLen ctx)
forall a. a -> Gen a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (VarByteString maxLen ctx -> Gen (VarByteString maxLen ctx))
-> VarByteString maxLen ctx -> Gen (VarByteString maxLen ctx)
forall a b. (a -> b) -> a -> b
$ Natural -> Natural -> VarByteString maxLen ctx
forall (n :: Natural) (ctx :: (Type -> Type) -> Type).
(Symbolic ctx, KnownNat n) =>
Natural -> Natural -> VarByteString n ctx
fromNatural Natural
nbits Natural
bits

toAsciiString :: forall n p . (KnownNat (Div n 8), (Div n 8) * 8 ~ n, KnownNat p) => VarByteString n (Interpreter (Zp p)) -> Haskell.String
toAsciiString :: forall (n :: Natural) (p :: Natural).
(KnownNat (Div n 8), (Div n 8 * 8) ~ n, KnownNat p) =>
VarByteString n (Interpreter (Zp p)) -> String
toAsciiString VarByteString{FieldElement (Interpreter (Zp p))
ByteString n (Interpreter (Zp p))
bsLength :: forall (maxLen :: Natural) (context :: (Type -> Type) -> Type).
VarByteString maxLen context -> FieldElement context
bsBuffer :: forall (maxLen :: Natural) (context :: (Type -> Type) -> Type).
VarByteString maxLen context -> ByteString maxLen context
bsLength :: FieldElement (Interpreter (Zp p))
bsBuffer :: ByteString n (Interpreter (Zp p))
..} = Natural -> ShowS
forall a. Natural -> [a] -> [a]
drop Natural
numZeros ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ Vector (Div n 8) Char -> String
forall (size :: Natural) a. Vector size a -> [a]
fromVector Vector (Div n 8) Char
chars
    where
        ByteString (Interpreter Vector n (Zp p)
v) = ByteString n (Interpreter (Zp p))
bsBuffer
        FieldElement (Interpreter (Par1 Zp p
len)) = FieldElement (Interpreter (Zp p))
bsLength
        strLen :: Natural
strLen = Zp p -> Natural
forall (p :: Natural). Zp p -> Natural
fromZp Zp p
len Natural -> Natural -> Natural
forall a. SemiEuclidean a => a -> a -> a
`div` Natural
8
        chars :: Vector (Div n 8) Char
chars = Int -> Char
chr (Int -> Char)
-> (Vector 8 (Zp p) -> Int) -> Vector 8 (Zp p) -> Char
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Natural -> Int
forall a b. (Integral a, Num b) => a -> b
Haskell.fromIntegral (Natural -> Int)
-> (Vector 8 (Zp p) -> Natural) -> Vector 8 (Zp p) -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Zp p -> Natural
forall (p :: Natural). Zp p -> Natural
fromZp (Zp p -> Natural)
-> (Vector 8 (Zp p) -> Zp p) -> Vector 8 (Zp p) -> Natural
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Zp p -> Zp p -> Zp p) -> Zp p -> Vector 8 (Zp p) -> Zp p
forall b a. (b -> a -> b) -> b -> Vector 8 a -> b
forall (t :: Type -> Type) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
Haskell.foldl (\Zp p
b Zp p
a -> Zp p
b Zp p -> Zp p -> Zp p
forall a. AdditiveSemigroup a => a -> a -> a
+ Zp p
b Zp p -> Zp p -> Zp p
forall a. AdditiveSemigroup a => a -> a -> a
+ Zp p
a) Zp p
forall a. AdditiveMonoid a => a
zero (Vector 8 (Zp p) -> Char)
-> Vector (Div n 8) (Vector 8 (Zp p)) -> Vector (Div n 8) Char
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: Natural) (n :: Natural) a.
KnownNat n =>
Vector (m * n) a -> Vector m (Vector n a)
chunks @(Div n 8) @8 Vector n (Zp p)
Vector (Div n 8 * 8) (Zp p)
v
        numZeros :: Natural
numZeros = forall (n :: Natural). KnownNat n => Natural
value @(Div n 8) Natural -> Natural -> Natural
-! Natural
strLen

instance
    ( Symbolic ctx
    , m * 8 ~ n
    , KnownNat m
    ) => IsString (VarByteString n ctx) where
    fromString :: String -> VarByteString n ctx
fromString = ByteString -> VarByteString n ctx
forall a b. FromConstant a b => a -> b
fromConstant (ByteString -> VarByteString n ctx)
-> (String -> ByteString) -> String -> VarByteString n ctx
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. IsString a => String -> a
fromString @Bytes.ByteString

instance
    ( Symbolic ctx
    , m * 8 ~ n
    , KnownNat m
    ) => FromConstant Bytes.ByteString (VarByteString n ctx) where
    fromConstant :: ByteString -> VarByteString n ctx
fromConstant ByteString
bytes = FieldElement ctx -> ByteString n ctx -> VarByteString n ctx
forall (maxLen :: Natural) (context :: (Type -> Type) -> Type).
FieldElement context
-> ByteString maxLen context -> VarByteString maxLen context
VarByteString (forall a b. FromConstant a b => a -> b
fromConstant @Natural (Natural -> FieldElement ctx)
-> (Int -> Natural) -> Int -> FieldElement ctx
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Natural -> Natural -> Natural
forall a. MultiplicativeSemigroup a => a -> a -> a
*Natural
8) (Natural -> Natural) -> (Int -> Natural) -> Int -> Natural
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Natural
forall a b. (Integral a, Num b) => a -> b
Haskell.fromIntegral (Int -> FieldElement ctx) -> Int -> FieldElement ctx
forall a b. (a -> b) -> a -> b
$ ByteString -> Int
Bytes.length ByteString
bytes) (ByteString -> ByteString n ctx
forall a b. FromConstant a b => a -> b
fromConstant ByteString
bytes)

instance (Symbolic ctx, KnownNat n) => FromConstant Natural (VarByteString n ctx) where
    fromConstant :: Natural -> VarByteString n ctx
fromConstant Natural
0 = FieldElement ctx -> ByteString n ctx -> VarByteString n ctx
forall (maxLen :: Natural) (context :: (Type -> Type) -> Type).
FieldElement context
-> ByteString maxLen context -> VarByteString maxLen context
VarByteString FieldElement ctx
forall a. AdditiveMonoid a => a
zero (forall a b. FromConstant a b => a -> b
fromConstant @Natural Natural
0)
    fromConstant Natural
n = FieldElement ctx -> ByteString n ctx -> VarByteString n ctx
forall (maxLen :: Natural) (context :: (Type -> Type) -> Type).
FieldElement context
-> ByteString maxLen context -> VarByteString maxLen context
VarByteString (Natural -> FieldElement ctx
forall a b. FromConstant a b => a -> b
fromConstant (Natural -> FieldElement ctx) -> Natural -> FieldElement ctx
forall a b. (a -> b) -> a -> b
$ Natural -> Natural -> Natural
forall a. Ord a => a -> a -> a
Haskell.min (forall (n :: Natural). KnownNat n => Natural
value @n) (Natural -> Natural
ilog2 Natural
n Natural -> Natural -> Natural
forall a. AdditiveSemigroup a => a -> a -> a
+ Natural
1)) (Natural -> ByteString n ctx
forall a b. FromConstant a b => a -> b
fromConstant Natural
n)

fromNatural :: forall n ctx . (Symbolic ctx, KnownNat n) => Natural -> Natural -> VarByteString n ctx
fromNatural :: forall (n :: Natural) (ctx :: (Type -> Type) -> Type).
(Symbolic ctx, KnownNat n) =>
Natural -> Natural -> VarByteString n ctx
fromNatural Natural
numBits Natural
n = FieldElement ctx -> ByteString n ctx -> VarByteString n ctx
forall (maxLen :: Natural) (context :: (Type -> Type) -> Type).
FieldElement context
-> ByteString maxLen context -> VarByteString maxLen context
VarByteString (Natural -> FieldElement ctx
forall a b. FromConstant a b => a -> b
fromConstant Natural
numBits) (Natural -> ByteString n ctx
forall a b. FromConstant a b => a -> b
fromConstant Natural
n)

fromByteString :: forall n ctx . (Symbolic ctx, KnownNat n) => ByteString n ctx -> VarByteString n ctx
fromByteString :: forall (n :: Natural) (ctx :: (Type -> Type) -> Type).
(Symbolic ctx, KnownNat n) =>
ByteString n ctx -> VarByteString n ctx
fromByteString ByteString n ctx
bs = FieldElement ctx -> ByteString n ctx -> VarByteString n ctx
forall (maxLen :: Natural) (context :: (Type -> Type) -> Type).
FieldElement context
-> ByteString maxLen context -> VarByteString maxLen context
VarByteString (Natural -> FieldElement ctx
forall a b. FromConstant a b => a -> b
fromConstant (Natural -> FieldElement ctx) -> Natural -> FieldElement ctx
forall a b. (a -> b) -> a -> b
$ forall (n :: Natural). KnownNat n => Natural
value @n) ByteString n ctx
bs

instance (Symbolic ctx, KnownNat m, m * 8 ~ n) => FromJSON (VarByteString n ctx) where
    parseJSON :: Value -> Parser (VarByteString n ctx)
parseJSON Value
v = String -> VarByteString n ctx
forall a. IsString a => String -> a
fromString (String -> VarByteString n ctx)
-> Parser String -> Parser (VarByteString n ctx)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Value -> Parser String
forall a. FromJSON a => Value -> Parser a
parseJSON Value
v

-- | Construct a VarByteString from a type-level string calculating its length automatically
--
instance
    ( Symbolic ctx
    , KnownSymbol s
    , m ~ Length s
    , m * 8 ~ l
    , KnownNat m
    ) => IsTypeString s (VarByteString l ctx) where
    fromType :: VarByteString l ctx
fromType = String -> VarByteString l ctx
forall a. IsString a => String -> a
fromString (String -> VarByteString l ctx) -> String -> VarByteString l ctx
forall a b. (a -> b) -> a -> b
$ Proxy s -> String
forall (n :: Symbol) (proxy :: Symbol -> Type).
KnownSymbol n =>
proxy n -> String
symbolVal (forall {k} (t :: k). Proxy t
forall (t :: Symbol). Proxy t
Proxy @s)

monoMax :: forall (m :: Natural) (n :: Natural) . Dict (Max (m + n) n ~ (m + n))
monoMax :: forall (m :: Natural) (n :: Natural).
Dict (Max (m + n) n ~ (m + n))
monoMax = Dict
  (If (OrdCond (CmpNat n (m + n)) 'True 'True 'False) (m + n) n
   ~ (m + n))
Dict (Max (m + n) n ~ (m + n))
forall (c :: Constraint). Dict c
unsafeAxiom

withMax :: forall (m :: Natural) (n :: Natural) {r}. ((Max (m + n) n ~ (m + n)) => r) -> r
withMax :: forall (m :: Natural) (n :: Natural) {r}.
((Max (m + n) n ~ (m + n)) => r) -> r
withMax = Dict
  (If (OrdCond (CmpNat n (m + n)) 'True 'True 'False) (m + n) n
   ~ (m + n))
-> ((If (OrdCond (CmpNat n (m + n)) 'True 'True 'False) (m + n) n
     ~ (m + n)) =>
    r)
-> r
forall (c :: Constraint) e r. HasDict c e => e -> (c => r) -> r
withDict (forall (m :: Natural) (n :: Natural).
Dict (Max (m + n) n ~ (m + n))
monoMax @m @n)

-- | Join two variable-length ByteStrings and move all the unsaaigned space towards lower indices.
-- Let @u@ denote the unassigned space. Then,
-- uu1010 `append` u10010 == uuu101010010
--
append
    :: forall m n ctx
    .  Symbolic ctx
    => KnownNat m
    => KnownNat (m + n)
    => VarByteString m ctx
    -> VarByteString n ctx
    -> VarByteString (m + n) ctx
append :: forall (m :: Natural) (n :: Natural)
       (ctx :: (Type -> Type) -> Type).
(Symbolic ctx, KnownNat m, KnownNat (m + n)) =>
VarByteString m ctx
-> VarByteString n ctx -> VarByteString (m + n) ctx
append (VarByteString FieldElement ctx
l1 ByteString m ctx
bs1) (VarByteString FieldElement ctx
l2 ByteString n ctx
bs2) = FieldElement ctx
-> ByteString (m + n) ctx -> VarByteString (m + n) ctx
forall (maxLen :: Natural) (context :: (Type -> Type) -> Type).
FieldElement context
-> ByteString maxLen context -> VarByteString maxLen context
VarByteString (FieldElement ctx
l1 FieldElement ctx -> FieldElement ctx -> FieldElement ctx
forall a. AdditiveSemigroup a => a -> a -> a
+ FieldElement ctx
l2) (ByteString (m + n) ctx -> VarByteString (m + n) ctx)
-> ByteString (m + n) ctx -> VarByteString (m + n) ctx
forall a b. (a -> b) -> a -> b
$ forall (m :: Natural) (n :: Natural) {r}.
((Max (m + n) n ~ (m + n)) => r) -> r
withMax @m @n ByteString (m + n) ctx
ByteString (Max (m + n) n) ctx
(Max (m + n) n ~ (m + n)) => ByteString (m + n) ctx
newBs
    where
        ex1 :: ByteString (m + n) ctx
        ex1 :: ByteString (m + n) ctx
ex1 = ByteString m ctx -> ByteString (m + n) ctx
forall a b. Resize a b => a -> b
resize ByteString m ctx
bs1

        newBs :: ByteString (Max (m + n) n) ctx
newBs = (ByteString (m + n) ctx
ex1 ByteString (m + n) ctx
-> FieldElement ctx -> ByteString (m + n) ctx
forall (n :: Natural) (ctx :: (Type -> Type) -> Type).
(Symbolic ctx, KnownNat n) =>
ByteString n ctx -> FieldElement ctx -> ByteString n ctx
`shiftL` FieldElement ctx
l2) ByteString (m + n) ctx
-> ByteString n ctx -> ByteString (Max (m + n) n) ctx
forall (m :: Natural) (n :: Natural) (c :: (Type -> Type) -> Type).
Symbolic c =>
ByteString m c -> ByteString n c -> ByteString (Max m n) c
`orRight` ByteString n ctx
bs2

infixl 6 @+
(@+)
    :: forall m n ctx
    .  Symbolic ctx
    => KnownNat m
    => KnownNat (m + n)
    => VarByteString m ctx
    -> VarByteString n ctx
    -> VarByteString (m + n) ctx
@+ :: forall (m :: Natural) (n :: Natural)
       (ctx :: (Type -> Type) -> Type).
(Symbolic ctx, KnownNat m, KnownNat (m + n)) =>
VarByteString m ctx
-> VarByteString n ctx -> VarByteString (m + n) ctx
(@+) = VarByteString m ctx
-> VarByteString n ctx -> VarByteString (m + n) ctx
forall (m :: Natural) (n :: Natural)
       (ctx :: (Type -> Type) -> Type).
(Symbolic ctx, KnownNat m, KnownNat (m + n)) =>
VarByteString m ctx
-> VarByteString n ctx -> VarByteString (m + n) ctx
append

shift
    :: forall n ctx
    .  Symbolic ctx
    => KnownNat n
    => (Words n ctx -> Natural -> Words n ctx)
    -> ByteString n ctx
    -> FieldElement ctx
    -> ByteString n ctx
shift :: forall (n :: Natural) (ctx :: (Type -> Type) -> Type).
(Symbolic ctx, KnownNat n) =>
(Words n ctx -> Natural -> Words n ctx)
-> ByteString n ctx -> FieldElement ctx -> ByteString n ctx
shift Words n ctx -> Natural -> Words n ctx
sh ByteString n ctx
bs (FieldElement ctx Par1
el) = Words n ctx -> ByteString n ctx
forall a b. Iso a b => a -> b
from (Words n ctx -> ByteString n ctx)
-> Words n ctx -> ByteString n ctx
forall a b. (a -> b) -> a -> b
$ (Natural -> Words n ctx -> Words n ctx)
-> Words n ctx -> [Natural] -> Words n ctx
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: Type -> Type) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
Haskell.foldr (\Natural
s Words n ctx
b -> forall (n :: Natural) (ctx :: (Type -> Type) -> Type) {r}.
(KnownNat n, KnownNat (Order (BaseField ctx))) =>
(KnownNat (WordCount n ctx) => r) -> r
withWordCount @n @ctx ((KnownNat (WordCount n ctx) => Words n ctx) -> Words n ctx)
-> (KnownNat (WordCount n ctx) => Words n ctx) -> Words n ctx
forall a b. (a -> b) -> a -> b
$ Words n ctx -> Words n ctx -> Bool ctx -> Words n ctx
forall b a. Conditional b a => a -> a -> b -> a
bool Words n ctx
b (Words n ctx
b Words n ctx -> Natural -> Words n ctx
`sh` (Natural
2Natural -> Natural -> Natural
forall a b. Exponent a b => a -> b -> a
^Natural
s)) (ByteString (Log2 n + 1) ctx -> Natural -> Bool ctx
forall (c :: (Type -> Type) -> Type) (n :: Natural).
Symbolic c =>
ByteString n c -> Natural -> Bool c
isSet ByteString (Log2 n + 1) ctx
elBits Natural
s)) Words n ctx
w [Natural
0 .. Natural
nbits]
    where
        elBits :: ByteString (Log2 n + 1) ctx
        elBits :: ByteString (Log2 n + 1) ctx
elBits = ctx (Vector (Log2 n + 1)) -> ByteString (Log2 n + 1) ctx
forall (n :: Natural) (context :: (Type -> Type) -> Type).
context (Vector n) -> ByteString n context
ByteString (ctx (Vector (Log2 n + 1)) -> ByteString (Log2 n + 1) ctx)
-> ctx (Vector (Log2 n + 1)) -> ByteString (Log2 n + 1) ctx
forall a b. (a -> b) -> a -> b
$ ctx Par1
-> (forall {i} {m :: Type -> Type}.
    (NFData i, MonadCircuit i (BaseField ctx) (WitnessField ctx) m) =>
    FunBody '[Par1] (Vector (Log2 n + 1)) i m)
-> ctx (Vector (Log2 n + 1))
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 Par1
el ((forall {i} {m :: Type -> Type}.
  (NFData i, MonadCircuit i (BaseField ctx) (WitnessField ctx) m) =>
  FunBody '[Par1] (Vector (Log2 n + 1)) i m)
 -> ctx (Vector (Log2 n + 1)))
-> (forall {i} {m :: Type -> Type}.
    (NFData i, MonadCircuit i (BaseField ctx) (WitnessField ctx) m) =>
    FunBody '[Par1] (Vector (Log2 n + 1)) i m)
-> ctx (Vector (Log2 n + 1))
forall a b. (a -> b) -> a -> b
$ ([i] -> Vector (Log2 n + 1) i)
-> m [i] -> m (Vector (Log2 n + 1) i)
forall a b. (a -> b) -> m a -> m b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap [i] -> Vector (Log2 n + 1) i
forall (size :: Natural) a. [a] -> Vector size a
unsafeToVector (m [i] -> m (Vector (Log2 n + 1) i))
-> (Par1 i -> m [i]) -> Par1 i -> m (Vector (Log2 n + 1) i)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Natural -> i -> m [i]
forall i a w (m :: Type -> Type).
(MonadCircuit i a w m, Arithmetic a) =>
Natural -> i -> m [i]
expansion (Natural
nbits Natural -> Natural -> Natural
forall a. AdditiveSemigroup a => a -> a -> a
+ Natural
1) (i -> m [i]) -> (Par1 i -> i) -> Par1 i -> m [i]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Par1 i -> i
forall p. Par1 p -> p
unPar1

        w :: Words n ctx
        w :: Words n ctx
w = ByteString n ctx -> Words n ctx
forall a b. Iso a b => a -> b
from ByteString n ctx
bs

        -- No need to perform more shifts than this.
        -- The bytestring will be all zeros beyond this iteration.
        nbits :: Natural
nbits = Natural -> Natural
ilog2 (Natural -> Natural) -> Natural -> Natural
forall a b. (a -> b) -> a -> b
$ forall (n :: Natural). KnownNat n => Natural
value @n

shiftL
    :: forall n ctx
    .  Symbolic ctx
    => KnownNat n
    => ByteString n ctx
    -> FieldElement ctx
    -> ByteString n ctx
shiftL :: forall (n :: Natural) (ctx :: (Type -> Type) -> Type).
(Symbolic ctx, KnownNat n) =>
ByteString n ctx -> FieldElement ctx -> ByteString n ctx
shiftL = (Words n ctx -> Natural -> Words n ctx)
-> ByteString n ctx -> FieldElement ctx -> ByteString n ctx
forall (n :: Natural) (ctx :: (Type -> Type) -> Type).
(Symbolic ctx, KnownNat n) =>
(Words n ctx -> Natural -> Words n ctx)
-> ByteString n ctx -> FieldElement ctx -> ByteString n ctx
shift Words n ctx -> Natural -> Words n ctx
forall (n :: Natural) (ctx :: (Type -> Type) -> Type).
(Symbolic ctx, KnownNat n) =>
Words n ctx -> Natural -> Words n ctx
shiftWordsL

shiftR
    :: forall n ctx
    .  Symbolic ctx
    => KnownNat n
    => ByteString n ctx
    -> FieldElement ctx
    -> ByteString n ctx
shiftR :: forall (n :: Natural) (ctx :: (Type -> Type) -> Type).
(Symbolic ctx, KnownNat n) =>
ByteString n ctx -> FieldElement ctx -> ByteString n ctx
shiftR = (Words n ctx -> Natural -> Words n ctx)
-> ByteString n ctx -> FieldElement ctx -> ByteString n ctx
forall (n :: Natural) (ctx :: (Type -> Type) -> Type).
(Symbolic ctx, KnownNat n) =>
(Words n ctx -> Natural -> Words n ctx)
-> ByteString n ctx -> FieldElement ctx -> ByteString n ctx
shift Words n ctx -> Natural -> Words n ctx
forall (n :: Natural) (ctx :: (Type -> Type) -> Type).
(Symbolic ctx, KnownNat n) =>
Words n ctx -> Natural -> Words n ctx
shiftWordsR

-- | Set all the unassigned bits to zero
--
wipeUnassigned
    :: forall n ctx
    .  Symbolic ctx
    => KnownNat n
    => VarByteString n ctx -> VarByteString n ctx
wipeUnassigned :: forall (n :: Natural) (ctx :: (Type -> Type) -> Type).
(Symbolic ctx, KnownNat n) =>
VarByteString n ctx -> VarByteString n ctx
wipeUnassigned VarByteString{FieldElement ctx
ByteString n ctx
bsLength :: forall (maxLen :: Natural) (context :: (Type -> Type) -> Type).
VarByteString maxLen context -> FieldElement context
bsBuffer :: forall (maxLen :: Natural) (context :: (Type -> Type) -> Type).
VarByteString maxLen context -> ByteString maxLen context
bsLength :: FieldElement ctx
bsBuffer :: ByteString n ctx
..} = FieldElement ctx -> ByteString n ctx -> VarByteString n ctx
forall (maxLen :: Natural) (context :: (Type -> Type) -> Type).
FieldElement context
-> ByteString maxLen context -> VarByteString maxLen context
VarByteString FieldElement ctx
bsLength ((ByteString n ctx -> FieldElement ctx -> ByteString n ctx
forall (n :: Natural) (ctx :: (Type -> Type) -> Type).
(Symbolic ctx, KnownNat n) =>
ByteString n ctx -> FieldElement ctx -> ByteString n ctx
`shiftR` FieldElement ctx
unassigned) (ByteString n ctx -> ByteString n ctx)
-> (ByteString n ctx -> ByteString n ctx)
-> ByteString n ctx
-> ByteString n ctx
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ByteString n ctx -> FieldElement ctx -> ByteString n ctx
forall (n :: Natural) (ctx :: (Type -> Type) -> Type).
(Symbolic ctx, KnownNat n) =>
ByteString n ctx -> FieldElement ctx -> ByteString n ctx
`shiftL` FieldElement ctx
unassigned) (ByteString n ctx -> ByteString n ctx)
-> ByteString n ctx -> ByteString n ctx
forall a b. (a -> b) -> a -> b
$ ByteString n ctx
bsBuffer)
    where
        unassigned :: FieldElement ctx
        unassigned :: FieldElement ctx
unassigned = Natural -> FieldElement ctx
forall a b. FromConstant a b => a -> b
fromConstant (forall (n :: Natural). KnownNat n => Natural
value @n) FieldElement ctx -> FieldElement ctx -> FieldElement ctx
forall a. AdditiveGroup a => a -> a -> a
- FieldElement ctx
bsLength


-----------------------------------------------------------------------------------------------------------------------
-- Helper types and functions for internal usage.
-- They optimise shifting by working with words rather than bits
-----------------------------------------------------------------------------------------------------------------------


type WordSize ctx = Div (NumberOfBits (BaseField ctx)) 2

natWordSize :: Natural -> Natural
natWordSize :: Natural -> Natural
natWordSize Natural
n = (Natural -> Natural
ilog2 (Natural
n Natural -> Natural -> Natural
-! Natural
1) Natural -> Natural -> Natural
forall a. AdditiveSemigroup a => a -> a -> a
+ Natural
1) Natural -> Natural -> Natural
forall a. SemiEuclidean a => a -> a -> a
`div` Natural
2

withWordSize' :: forall a . (KnownNat (Order (BaseField a))) :- KnownNat (WordSize a)
withWordSize' :: forall (a :: (Type -> Type) -> Type).
KnownNat (Order (BaseField a)) :- KnownNat (WordSize a)
withWordSize' = (KnownNat (Order (BaseField a)) => Dict (KnownNat (WordSize a)))
-> KnownNat (Order (BaseField a)) :- KnownNat (WordSize a)
forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
Sub ((KnownNat (Order (BaseField a)) => Dict (KnownNat (WordSize a)))
 -> KnownNat (Order (BaseField a)) :- KnownNat (WordSize a))
-> (KnownNat (Order (BaseField a)) => Dict (KnownNat (WordSize a)))
-> KnownNat (Order (BaseField a)) :- KnownNat (WordSize a)
forall a b. (a -> b) -> a -> b
$ forall (n :: Natural) r. SNat n -> (KnownNat n => r) -> r
withKnownNat @(WordSize a) (Natural -> SNat (WordSize a)
forall (n :: Natural). Natural -> SNat n
unsafeSNat (Natural -> Natural
natWordSize (forall (n :: Natural). KnownNat n => Natural
value @(Order (BaseField a))))) Dict (KnownNat (WordSize a))
KnownNat (WordSize a) => Dict (KnownNat (WordSize a))
forall (a :: Constraint). a => Dict a
Dict

withWordSize :: forall a {r}. (KnownNat (Order (BaseField a))) => (KnownNat (WordSize a) => r) -> r
withWordSize :: forall (a :: (Type -> Type) -> Type) {r}.
KnownNat (Order (BaseField a)) =>
(KnownNat (WordSize a) => r) -> r
withWordSize = (KnownNat (Order (BaseField a))
 :- KnownNat (Div (Log2 (Order (BaseField a) - 1) + 1) 2))
-> (KnownNat (Div (Log2 (Order (BaseField a) - 1) + 1) 2) => r)
-> r
forall (c :: Constraint) e r. HasDict c e => e -> (c => r) -> r
withDict (forall (a :: (Type -> Type) -> Type).
KnownNat (Order (BaseField a)) :- KnownNat (WordSize a)
withWordSize' @a)

type WordCount n ctx = Div (n + WordSize ctx - 1) (WordSize ctx)

withWordCount
    :: forall n ctx {r}
    .  KnownNat n
    => KnownNat (Order (BaseField ctx))
    => (KnownNat (WordCount n ctx) => r) -> r
withWordCount :: forall (n :: Natural) (ctx :: (Type -> Type) -> Type) {r}.
(KnownNat n, KnownNat (Order (BaseField ctx))) =>
(KnownNat (WordCount n ctx) => r) -> r
withWordCount =
    forall (a :: (Type -> Type) -> Type) {r}.
KnownNat (Order (BaseField a)) =>
(KnownNat (WordSize a) => r) -> r
withWordSize @ctx ((KnownNat (WordSize ctx) =>
  (KnownNat (WordCount n ctx) => r) -> r)
 -> (KnownNat (WordCount n ctx) => r) -> r)
-> (KnownNat (WordSize ctx) =>
    (KnownNat (WordCount n ctx) => r) -> r)
-> (KnownNat (WordCount n ctx) => r)
-> r
forall a b. (a -> b) -> a -> b
$
        Dict
  (Assert
     (OrdCond (CmpNat 1 (WordSize ctx)) 'True 'True 'False)
     (TypeError ...))
-> (Assert
      (OrdCond (CmpNat 1 (WordSize ctx)) 'True 'True 'False)
      (TypeError ...) =>
    (KnownNat (WordCount n ctx) => r) -> r)
-> (KnownNat (WordCount n ctx) => r)
-> r
forall (c :: Constraint) e r. HasDict c e => e -> (c => r) -> r
withDict (forall (c :: Constraint). Dict c
unsafeAxiom @(1 <= WordSize ctx)) ((Assert
    (OrdCond (CmpNat 1 (WordSize ctx)) 'True 'True 'False)
    (TypeError ...) =>
  (KnownNat (WordCount n ctx) => r) -> r)
 -> (KnownNat (WordCount n ctx) => r) -> r)
-> (Assert
      (OrdCond (CmpNat 1 (WordSize ctx)) 'True 'True 'False)
      (TypeError ...) =>
    (KnownNat (WordCount n ctx) => r) -> r)
-> (KnownNat (WordCount n ctx) => r)
-> r
forall a b. (a -> b) -> a -> b
$
            Dict
  (Assert
     (OrdCond (CmpNat 1 (n + WordSize ctx)) 'True 'True 'False)
     (TypeError ...))
-> (Assert
      (OrdCond (CmpNat 1 (n + WordSize ctx)) 'True 'True 'False)
      (TypeError ...) =>
    (KnownNat (WordCount n ctx) => r) -> r)
-> (KnownNat (WordCount n ctx) => r)
-> r
forall (c :: Constraint) e r. HasDict c e => e -> (c => r) -> r
withDict (forall (c :: Constraint). Dict c
unsafeAxiom @(1 <= n + WordSize ctx)) ((Assert
    (OrdCond (CmpNat 1 (n + WordSize ctx)) 'True 'True 'False)
    (TypeError ...) =>
  (KnownNat (WordCount n ctx) => r) -> r)
 -> (KnownNat (WordCount n ctx) => r) -> r)
-> (Assert
      (OrdCond (CmpNat 1 (n + WordSize ctx)) 'True 'True 'False)
      (TypeError ...) =>
    (KnownNat (WordCount n ctx) => r) -> r)
-> (KnownNat (WordCount n ctx) => r)
-> r
forall a b. (a -> b) -> a -> b
$
                ((KnownNat n, KnownNat (WordSize ctx))
 :- KnownNat (n + WordSize ctx))
-> (KnownNat (n + WordSize ctx) =>
    (KnownNat (WordCount n ctx) => r) -> r)
-> (KnownNat (WordCount n ctx) => r)
-> r
forall (c :: Constraint) e r. HasDict c e => e -> (c => r) -> r
withDict (forall (n :: Natural) (m :: Natural).
(KnownNat n, KnownNat m) :- KnownNat (n + m)
plusNat @n @(WordSize ctx)) ((KnownNat (n + WordSize ctx) =>
  (KnownNat (WordCount n ctx) => r) -> r)
 -> (KnownNat (WordCount n ctx) => r) -> r)
-> (KnownNat (n + WordSize ctx) =>
    (KnownNat (WordCount n ctx) => r) -> r)
-> (KnownNat (WordCount n ctx) => r)
-> r
forall a b. (a -> b) -> a -> b
$
                    ((KnownNat (n + WordSize ctx), KnownNat 1,
  Assert
    (OrdCond (CmpNat 1 (n + WordSize ctx)) 'True 'True 'False)
    (TypeError ...))
 :- KnownNat ((n + WordSize ctx) - 1))
-> (KnownNat ((n + WordSize ctx) - 1) =>
    (KnownNat (WordCount n ctx) => r) -> r)
-> (KnownNat (WordCount n ctx) => r)
-> r
forall (c :: Constraint) e r. HasDict c e => e -> (c => r) -> r
withDict (forall (n :: Natural) (m :: Natural).
(KnownNat n, KnownNat m, m <= n) :- KnownNat (n - m)
minusNat @(n + WordSize ctx) @1) ((KnownNat ((n + WordSize ctx) - 1) =>
  (KnownNat (WordCount n ctx) => r) -> r)
 -> (KnownNat (WordCount n ctx) => r) -> r)
-> (KnownNat ((n + WordSize ctx) - 1) =>
    (KnownNat (WordCount n ctx) => r) -> r)
-> (KnownNat (WordCount n ctx) => r)
-> r
forall a b. (a -> b) -> a -> b
$
                        ((KnownNat ((n + WordSize ctx) - 1), KnownNat (WordSize ctx),
  Assert
    (OrdCond (CmpNat 1 (WordSize ctx)) 'True 'True 'False)
    (TypeError ...))
 :- KnownNat (WordCount n ctx))
-> (KnownNat (WordCount n ctx) => r) -> r
forall (c :: Constraint) e r. HasDict c e => e -> (c => r) -> r
withDict (forall (n :: Natural) (m :: Natural).
(KnownNat n, KnownNat m, 1 <= m) :- KnownNat (Div n m)
divNat @(n + WordSize ctx - 1) @(WordSize ctx))

newtype Words n ctx = Words (ctx (Vector (WordCount n ctx)))
    deriving (forall x. Words n ctx -> Rep (Words n ctx) x)
-> (forall x. Rep (Words n ctx) x -> Words n ctx)
-> Generic (Words n ctx)
forall (n :: Natural) (ctx :: (Type -> Type) -> Type) x.
Rep (Words n ctx) x -> Words n ctx
forall (n :: Natural) (ctx :: (Type -> Type) -> Type) x.
Words n ctx -> Rep (Words n ctx) x
forall x. Rep (Words n ctx) x -> Words n ctx
forall x. Words n ctx -> Rep (Words n ctx) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall (n :: Natural) (ctx :: (Type -> Type) -> Type) x.
Words n ctx -> Rep (Words n ctx) x
from :: forall x. Words n ctx -> Rep (Words n ctx) x
$cto :: forall (n :: Natural) (ctx :: (Type -> Type) -> Type) x.
Rep (Words n ctx) x -> Words n ctx
to :: forall x. Rep (Words n ctx) x -> Words n ctx
Generic

deriving newtype instance NFData (ctx (Vector (WordCount n ctx))) => NFData (Words n ctx)
deriving newtype instance Haskell.Show (ctx (Vector (WordCount n ctx))) => Haskell.Show (Words n ctx)
deriving newtype instance (KnownNat (WordCount n ctx), Symbolic ctx) => SymbolicData (Words n ctx)
deriving newtype instance (KnownNat (WordCount n ctx), Symbolic ctx) => Conditional (Bool ctx) (Words n ctx)

instance
  ( Symbolic ctx
  , KnownNat n
  ) => Iso (Words n ctx) (ByteString n ctx) where
    from :: Words n ctx -> ByteString n ctx
from (Words ctx (Vector (WordCount n ctx))
regs) = ctx (Vector n) -> ByteString n ctx
forall (n :: Natural) (context :: (Type -> Type) -> Type).
context (Vector n) -> ByteString n context
ByteString (ctx (Vector n) -> ByteString n ctx)
-> ctx (Vector n) -> ByteString n ctx
forall a b. (a -> b) -> a -> b
$ ctx (Vector (WordCount n ctx))
-> (forall {i} {m :: Type -> Type}.
    (NFData i, MonadCircuit i (BaseField ctx) (WitnessField ctx) m) =>
    FunBody '[Vector (WordCount n ctx)] (Vector n) i m)
-> ctx (Vector n)
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 (WordCount n ctx))
regs ((forall {i} {m :: Type -> Type}.
  (NFData i, MonadCircuit i (BaseField ctx) (WitnessField ctx) m) =>
  FunBody '[Vector (WordCount n ctx)] (Vector n) i m)
 -> ctx (Vector n))
-> (forall {i} {m :: Type -> Type}.
    (NFData i, MonadCircuit i (BaseField ctx) (WitnessField ctx) m) =>
    FunBody '[Vector (WordCount n ctx)] (Vector n) i m)
-> ctx (Vector n)
forall a b. (a -> b) -> a -> b
$ \Vector (WordCount n ctx) i
r -> do
        let v :: [i]
v = Vector (WordCount n ctx) i -> [i]
forall (size :: Natural) a. Vector size a -> [a]
fromVector Vector (WordCount n ctx) i
r
            (i
w, [i]
ws) = ([i] -> i
forall a. HasCallStack => [a] -> a
Haskell.head [i]
v, [i] -> [i]
forall a. HasCallStack => [a] -> [a]
Haskell.tail [i]
v)
            regSize :: Natural
regSize = forall (a :: (Type -> Type) -> Type) {r}.
KnownNat (Order (BaseField a)) =>
(KnownNat (WordSize a) => r) -> r
withWordSize @ctx ((KnownNat (WordSize ctx) => Natural) -> Natural)
-> (KnownNat (WordSize ctx) => Natural) -> Natural
forall a b. (a -> b) -> a -> b
$ forall (n :: Natural). KnownNat n => Natural
value @(WordSize ctx)
            hiRegSize :: Natural
hiRegSize = forall (n :: Natural). KnownNat n => Natural
value @n Natural -> Natural -> Natural
-! Natural
regSize Natural -> Natural -> Natural
forall a. MultiplicativeSemigroup a => a -> a -> a
* (forall (n :: Natural) (ctx :: (Type -> Type) -> Type) {r}.
(KnownNat n, KnownNat (Order (BaseField ctx))) =>
(KnownNat (WordCount n ctx) => r) -> r
withWordCount @n @ctx ((KnownNat (WordCount n ctx) => Natural) -> Natural)
-> (KnownNat (WordCount n ctx) => Natural) -> Natural
forall a b. (a -> b) -> a -> b
$ forall (n :: Natural). KnownNat n => Natural
value @(WordCount n ctx) Natural -> Natural -> Natural
-! Natural
1)
        [i]
lows <- ([i] -> [i]) -> [[i]] -> [i]
forall (t :: Type -> Type) a b.
Foldable t =>
(a -> [b]) -> t a -> [b]
Haskell.concatMap [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
<$> (i -> m [i]) -> [i] -> m [[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) -> [a] -> m [b]
mapM (Natural -> i -> m [i]
forall i a w (m :: Type -> Type).
(MonadCircuit i a w m, Arithmetic a) =>
Natural -> i -> m [i]
expansion Natural
regSize) [i]
ws
        [i]
hi <- [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
hiRegSize i
w
        Vector n i -> m (Vector n i)
forall a. a -> m a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Vector n i -> m (Vector n i)) -> Vector n i -> m (Vector n i)
forall a b. (a -> b) -> a -> b
$ [i] -> Vector n i
forall (size :: Natural) a. [a] -> Vector size a
unsafeToVector ([i]
hi [i] -> [i] -> [i]
forall a. Semigroup a => a -> a -> a
<> [i]
lows)

instance
  ( Symbolic ctx
  , KnownNat n
  ) => Iso (ByteString n ctx) (Words n ctx) where
    from :: ByteString n ctx -> Words n ctx
from (ByteString ctx (Vector n)
bits) = ctx (Vector (WordCount n ctx)) -> Words n ctx
forall (n :: Natural) (ctx :: (Type -> Type) -> Type).
ctx (Vector (WordCount n ctx)) -> Words n ctx
Words (ctx (Vector (WordCount n ctx)) -> Words n ctx)
-> ctx (Vector (WordCount n ctx)) -> Words n ctx
forall a b. (a -> b) -> a -> b
$ ctx (Vector n)
-> (forall {i} {m :: Type -> Type}.
    (NFData i, MonadCircuit i (BaseField ctx) (WitnessField ctx) m) =>
    FunBody '[Vector n] (Vector (WordCount n ctx)) i m)
-> ctx (Vector (WordCount n ctx))
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 n)
bits ((forall {i} {m :: Type -> Type}.
  (NFData i, MonadCircuit i (BaseField ctx) (WitnessField ctx) m) =>
  FunBody '[Vector n] (Vector (WordCount n ctx)) i m)
 -> ctx (Vector (WordCount n ctx)))
-> (forall {i} {m :: Type -> Type}.
    (NFData i, MonadCircuit i (BaseField ctx) (WitnessField ctx) m) =>
    FunBody '[Vector n] (Vector (WordCount n ctx)) i m)
-> ctx (Vector (WordCount n ctx))
forall a b. (a -> b) -> a -> b
$ \Vector n i
b -> do
        let bs :: [i]
bs = Vector n i -> [i]
forall (size :: Natural) a. Vector size a -> [a]
fromVector Vector n i
b
            regSize :: Natural
regSize = forall (a :: (Type -> Type) -> Type) {r}.
KnownNat (Order (BaseField a)) =>
(KnownNat (WordSize a) => r) -> r
withWordSize @ctx ((KnownNat (WordSize ctx) => Natural) -> Natural)
-> (KnownNat (WordSize ctx) => Natural) -> Natural
forall a b. (a -> b) -> a -> b
$ forall (n :: Natural). KnownNat n => Natural
value @(WordSize ctx)
            hiRegSize :: Natural
hiRegSize = forall (n :: Natural). KnownNat n => Natural
value @n Natural -> Natural -> Natural
-! Natural
regSize Natural -> Natural -> Natural
forall a. MultiplicativeSemigroup a => a -> a -> a
* (forall (n :: Natural) (ctx :: (Type -> Type) -> Type) {r}.
(KnownNat n, KnownNat (Order (BaseField ctx))) =>
(KnownNat (WordCount n ctx) => r) -> r
withWordCount @n @ctx ((KnownNat (WordCount n ctx) => Natural) -> Natural)
-> (KnownNat (WordCount n ctx) => Natural) -> Natural
forall a b. (a -> b) -> a -> b
$ forall (n :: Natural). KnownNat n => Natural
value @(WordCount n ctx) Natural -> Natural -> Natural
-! Natural
1)
            his :: [i]
his = Natural -> [i] -> [i]
forall a. HasCallStack => Natural -> [a] -> [a]
take Natural
hiRegSize [i]
bs
            lows :: [[i]]
lows = Int -> [i] -> [[i]]
forall e. Int -> [e] -> [[e]]
chunksOf (Natural -> Int
forall a b. (Integral a, Num b) => a -> b
Haskell.fromIntegral Natural
regSize) ([i] -> [[i]]) -> [i] -> [[i]]
forall a b. (a -> b) -> a -> b
$ Natural -> [i] -> [i]
forall a. Natural -> [a] -> [a]
drop Natural
hiRegSize [i]
bs
        i
hi <- [i] -> m i
forall i a w (m :: Type -> Type).
MonadCircuit i a w m =>
[i] -> m i
horner ([i] -> m i) -> [i] -> m i
forall a b. (a -> b) -> a -> b
$ [i] -> [i]
forall a. [a] -> [a]
Haskell.reverse [i]
his
        [i]
lo <- ([i] -> m i) -> [[i]] -> m [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) -> [a] -> m [b]
mapM ([i] -> m i
forall i a w (m :: Type -> Type).
MonadCircuit i a w m =>
[i] -> m i
horner ([i] -> m i) -> ([i] -> [i]) -> [i] -> m i
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [i] -> [i]
forall a. [a] -> [a]
Haskell.reverse) [[i]]
lows
        Vector (WordCount n ctx) i -> m (Vector (WordCount n ctx) i)
forall a. a -> m a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Vector (WordCount n ctx) i -> m (Vector (WordCount n ctx) i))
-> Vector (WordCount n ctx) i -> m (Vector (WordCount n ctx) i)
forall a b. (a -> b) -> a -> b
$ [i] -> Vector (WordCount n ctx) i
forall (size :: Natural) a. [a] -> Vector size a
unsafeToVector (i
hii -> [i] -> [i]
forall a. a -> [a] -> [a]
:[i]
lo)


-- | shift a vector of words left by a power of two
--
shiftWordsL
    :: forall n ctx
    .  Symbolic ctx
    => KnownNat n
    => Words n ctx -> Natural -> Words n ctx
shiftWordsL :: forall (n :: Natural) (ctx :: (Type -> Type) -> Type).
(Symbolic ctx, KnownNat n) =>
Words n ctx -> Natural -> Words n ctx
shiftWordsL (Words ctx (Vector (WordCount n ctx))
regs) Natural
p2
  | Natural
p2 Natural -> Natural -> Bool
forall a. Ord a => a -> a -> Bool
Haskell.>= (forall (n :: Natural). KnownNat n => Natural
value @n) = ctx (Vector (WordCount n ctx)) -> Words n ctx
forall (n :: Natural) (ctx :: (Type -> Type) -> Type).
ctx (Vector (WordCount n ctx)) -> Words n ctx
Words (ctx (Vector (WordCount n ctx)) -> Words n ctx)
-> ctx (Vector (WordCount n ctx)) -> Words n ctx
forall a b. (a -> b) -> a -> b
$ forall (n :: Natural) (ctx :: (Type -> Type) -> Type) {r}.
(KnownNat n, KnownNat (Order (BaseField ctx))) =>
(KnownNat (WordCount n ctx) => r) -> r
withWordCount @n @ctx ((KnownNat (WordCount n ctx) => ctx (Vector (WordCount n ctx)))
 -> ctx (Vector (WordCount n ctx)))
-> (KnownNat (WordCount n ctx) => ctx (Vector (WordCount n ctx)))
-> ctx (Vector (WordCount n ctx))
forall a b. (a -> b) -> a -> b
$ Vector (WordCount n ctx) (BaseField ctx)
-> ctx (Vector (WordCount n ctx))
forall (c :: (Type -> Type) -> Type) (f :: Type -> Type).
(Symbolic c, Functor f) =>
f (BaseField c) -> c f
embed ((Rep (Vector (WordCount n ctx)) -> BaseField ctx)
-> Vector (WordCount n ctx) (BaseField ctx)
forall a.
(Rep (Vector (WordCount n ctx)) -> a) -> Vector (WordCount n ctx) a
forall (f :: Type -> Type) a.
Representable f =>
(Rep f -> a) -> f a
tabulate Rep (Vector (WordCount n ctx)) -> BaseField ctx
Zp (WordCount n ctx) -> BaseField ctx
forall a. AdditiveMonoid a => a
zero)
  | Natural
p2 Natural -> Natural -> Bool
forall a. Eq a => a -> a -> Bool
Haskell.== Natural
0 = ctx (Vector (WordCount n ctx)) -> Words n ctx
forall (n :: Natural) (ctx :: (Type -> Type) -> Type).
ctx (Vector (WordCount n ctx)) -> Words n ctx
Words ctx (Vector (WordCount n ctx))
regs
  | Bool
otherwise = ctx (Vector (WordCount n ctx)) -> Words n ctx
forall (n :: Natural) (ctx :: (Type -> Type) -> Type).
ctx (Vector (WordCount n ctx)) -> Words n ctx
Words ctx (Vector (WordCount n ctx))
shifted
    where
        regSize :: Natural
        regSize :: Natural
regSize = forall (a :: (Type -> Type) -> Type) {r}.
KnownNat (Order (BaseField a)) =>
(KnownNat (WordSize a) => r) -> r
withWordSize @ctx ((KnownNat (WordSize ctx) => Natural) -> Natural)
-> (KnownNat (WordSize ctx) => Natural) -> Natural
forall a b. (a -> b) -> a -> b
$ forall (n :: Natural). KnownNat n => Natural
value @(WordSize ctx)

        hiRegSize :: Natural
        hiRegSize :: Natural
hiRegSize = forall (n :: Natural). KnownNat n => Natural
value @n Natural -> Natural -> Natural
forall a. SemiEuclidean a => a -> a -> a
`mod` Natural
regSize

        -- How many registers will be empty after the shift
        (Natural
zeroRegs, Natural
remShift) = Natural
p2 Natural -> Natural -> (Natural, Natural)
forall a. SemiEuclidean a => a -> a -> (a, a)
`divMod` Natural
regSize

        shifted :: ctx (Vector (WordCount n ctx))
shifted = ctx (Vector (WordCount n ctx))
-> CircuitFun
     '[Vector (WordCount n ctx)] (Vector (WordCount n ctx)) ctx
-> ctx (Vector (WordCount n ctx))
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 (WordCount n ctx))
regs (CircuitFun
   '[Vector (WordCount n ctx)] (Vector (WordCount n ctx)) ctx
 -> ctx (Vector (WordCount n ctx)))
-> CircuitFun
     '[Vector (WordCount n ctx)] (Vector (WordCount n ctx)) ctx
-> ctx (Vector (WordCount n ctx))
forall a b. (a -> b) -> a -> b
$ \Vector (WordCount n ctx) i
r -> do
            let lst :: [i]
lst = Vector (WordCount n ctx) i -> [i]
forall (size :: Natural) a. Vector size a -> [a]
fromVector Vector (WordCount n ctx) i
r
                v :: [i]
v = Natural -> [i] -> [i]
forall a. Natural -> [a] -> [a]
drop Natural
zeroRegs [i]
lst
                (i
hi, [i]
lows) = ([i] -> i
forall a. HasCallStack => [a] -> a
Haskell.head [i]
v, [i] -> [i]
forall a. HasCallStack => [a] -> [a]
Haskell.tail [i]
v)

            i
z <- ClosedPoly i (BaseField ctx) -> 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. AdditiveMonoid a => a
zero)
            ([i]
newRegs, i
carry) <- (i -> ([i], i) -> m ([i], i)) -> ([i], i) -> [i] -> m ([i], 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 -> ([i], i) -> m ([i], i)
forall i w (m :: Type -> Type).
MonadCircuit i (BaseField ctx) w m =>
i -> ([i], i) -> m ([i], i)
shiftCarry ([], i
z) [i]
lows

            i
s <- ClosedPoly i (BaseField ctx) -> m i
forall var a w (m :: Type -> Type).
MonadCircuit var a w m =>
ClosedPoly var a -> m var
newAssigned (ClosedPoly i (BaseField ctx) -> m i)
-> ClosedPoly i (BaseField ctx) -> m i
forall a b. (a -> b) -> a -> b
$ \i -> x
p -> 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
remShift) (i -> x
p i
hi) x -> x -> x
forall a. AdditiveSemigroup a => a -> a -> a
+ i -> x
p i
carry
            (i
newHi, 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 Natural
hiRegSize Natural
regSize i
s
            Vector (WordCount n ctx) i -> m (Vector (WordCount n ctx) i)
forall a. a -> m a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Vector (WordCount n ctx) i -> m (Vector (WordCount n ctx) i))
-> Vector (WordCount n ctx) i -> m (Vector (WordCount n ctx) i)
forall a b. (a -> b) -> a -> b
$ [i] -> Vector (WordCount n ctx) i
forall (size :: Natural) a. [a] -> Vector size a
unsafeToVector ((i
newHi i -> [i] -> [i]
forall a. a -> [a] -> [a]
: [i]
newRegs) [i] -> [i] -> [i]
forall a. Semigroup a => a -> a -> a
<> Natural -> i -> [i]
forall a. Natural -> a -> [a]
replicate Natural
zeroRegs i
z)

        shiftCarry :: MonadCircuit i (BaseField ctx) w m => i -> ([i], i) -> m ([i], i)
        shiftCarry :: forall i w (m :: Type -> Type).
MonadCircuit i (BaseField ctx) w m =>
i -> ([i], i) -> m ([i], i)
shiftCarry i
r ([i]
acc, i
carry) = do
            i
s <- ClosedPoly i (BaseField ctx) -> m i
forall var a w (m :: Type -> Type).
MonadCircuit var a w m =>
ClosedPoly var a -> m var
newAssigned (ClosedPoly i (BaseField ctx) -> m i)
-> ClosedPoly i (BaseField ctx) -> m i
forall a b. (a -> b) -> a -> b
$ \i -> x
p -> 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
remShift) (i -> x
p i
r) x -> x -> x
forall a. AdditiveSemigroup a => a -> a -> a
+ i -> x
p i
carry
            (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
regSize Natural
regSize i
s
            ([i], i) -> m ([i], i)
forall a. a -> m a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (i
l i -> [i] -> [i]
forall a. a -> [a] -> [a]
: [i]
acc, i
h)

shiftWordsR
    :: forall n ctx
    .  Symbolic ctx
    => KnownNat n
    => Words n ctx -> Natural -> Words n ctx
shiftWordsR :: forall (n :: Natural) (ctx :: (Type -> Type) -> Type).
(Symbolic ctx, KnownNat n) =>
Words n ctx -> Natural -> Words n ctx
shiftWordsR (Words ctx (Vector (WordCount n ctx))
regs) Natural
p2
  | Natural
p2 Natural -> Natural -> Bool
forall a. Ord a => a -> a -> Bool
Haskell.>= (forall (n :: Natural). KnownNat n => Natural
value @n) = ctx (Vector (WordCount n ctx)) -> Words n ctx
forall (n :: Natural) (ctx :: (Type -> Type) -> Type).
ctx (Vector (WordCount n ctx)) -> Words n ctx
Words (ctx (Vector (WordCount n ctx)) -> Words n ctx)
-> ctx (Vector (WordCount n ctx)) -> Words n ctx
forall a b. (a -> b) -> a -> b
$ forall (n :: Natural) (ctx :: (Type -> Type) -> Type) {r}.
(KnownNat n, KnownNat (Order (BaseField ctx))) =>
(KnownNat (WordCount n ctx) => r) -> r
withWordCount @n @ctx ((KnownNat (WordCount n ctx) => ctx (Vector (WordCount n ctx)))
 -> ctx (Vector (WordCount n ctx)))
-> (KnownNat (WordCount n ctx) => ctx (Vector (WordCount n ctx)))
-> ctx (Vector (WordCount n ctx))
forall a b. (a -> b) -> a -> b
$ Vector (WordCount n ctx) (BaseField ctx)
-> ctx (Vector (WordCount n ctx))
forall (c :: (Type -> Type) -> Type) (f :: Type -> Type).
(Symbolic c, Functor f) =>
f (BaseField c) -> c f
embed ((Rep (Vector (WordCount n ctx)) -> BaseField ctx)
-> Vector (WordCount n ctx) (BaseField ctx)
forall a.
(Rep (Vector (WordCount n ctx)) -> a) -> Vector (WordCount n ctx) a
forall (f :: Type -> Type) a.
Representable f =>
(Rep f -> a) -> f a
tabulate Rep (Vector (WordCount n ctx)) -> BaseField ctx
Zp (WordCount n ctx) -> BaseField ctx
forall a. AdditiveMonoid a => a
zero)
  | Natural
p2 Natural -> Natural -> Bool
forall a. Eq a => a -> a -> Bool
Haskell.== Natural
0 = ctx (Vector (WordCount n ctx)) -> Words n ctx
forall (n :: Natural) (ctx :: (Type -> Type) -> Type).
ctx (Vector (WordCount n ctx)) -> Words n ctx
Words ctx (Vector (WordCount n ctx))
regs
  | Bool
otherwise = ctx (Vector (WordCount n ctx)) -> Words n ctx
forall (n :: Natural) (ctx :: (Type -> Type) -> Type).
ctx (Vector (WordCount n ctx)) -> Words n ctx
Words ctx (Vector (WordCount n ctx))
shifted
    where
        regSize :: Natural
        regSize :: Natural
regSize = forall (a :: (Type -> Type) -> Type) {r}.
KnownNat (Order (BaseField a)) =>
(KnownNat (WordSize a) => r) -> r
withWordSize @ctx ((KnownNat (WordSize ctx) => Natural) -> Natural)
-> (KnownNat (WordSize ctx) => Natural) -> Natural
forall a b. (a -> b) -> a -> b
$ forall (n :: Natural). KnownNat n => Natural
value @(WordSize ctx)

        hiRegSize :: Natural
        hiRegSize :: Natural
hiRegSize = forall (n :: Natural). KnownNat n => Natural
value @n Natural -> Natural -> Natural
forall a. SemiEuclidean a => a -> a -> a
`mod` Natural
regSize

        -- How many registers will be empty after the shift
        (Natural
zeroRegs, Natural
remShift) = Natural
p2 Natural -> Natural -> (Natural, Natural)
forall a. SemiEuclidean a => a -> a -> (a, a)
`divMod` Natural
regSize

        shifted :: ctx (Vector (WordCount n ctx))
shifted = ctx (Vector (WordCount n ctx))
-> CircuitFun
     '[Vector (WordCount n ctx)] (Vector (WordCount n ctx)) ctx
-> ctx (Vector (WordCount n ctx))
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 (WordCount n ctx))
regs (CircuitFun
   '[Vector (WordCount n ctx)] (Vector (WordCount n ctx)) ctx
 -> ctx (Vector (WordCount n ctx)))
-> CircuitFun
     '[Vector (WordCount n ctx)] (Vector (WordCount n ctx)) ctx
-> ctx (Vector (WordCount n ctx))
forall a b. (a -> b) -> a -> b
$ \Vector (WordCount n ctx) i
r -> do
            let lst :: [i]
lst = Vector (WordCount n ctx) i -> [i]
forall (size :: Natural) a. Vector size a -> [a]
fromVector Vector (WordCount n ctx) i
r
                v :: [i]
v = Natural -> [i] -> [i]
forall a. HasCallStack => Natural -> [a] -> [a]
take ([i] -> Natural
forall (t :: Type -> Type) a. Foldable t => t a -> Natural
length [i]
lst Natural -> Natural -> Natural
-! Natural
zeroRegs) [i]
lst
                (i
hi, [i]
lows) = ([i] -> i
forall a. HasCallStack => [a] -> a
Haskell.head [i]
v, [i] -> [i]
forall a. HasCallStack => [a] -> [a]
Haskell.tail [i]
v)

            i
z <- ClosedPoly i (BaseField ctx) -> 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. AdditiveMonoid a => a
zero)

            (i
carry, i
newHi) <- case (Natural
hiRegSize Natural -> Natural -> Bool
forall a. Ord a => a -> a -> Bool
Haskell.> Natural
remShift) of
                                Bool
Haskell.True -> 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
remShift (Natural
hiRegSize Natural -> Natural -> Natural
-! Natural
remShift) i
hi
                                Bool
_            -> (i, i) -> m (i, i)
forall a. a -> m a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (i
hi, i
z)

            ([i]
newRegs, i
_) <- (([i], i) -> i -> m ([i], i)) -> ([i], i) -> [i] -> m ([i], i)
forall (t :: Type -> Type) (m :: Type -> Type) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldlM ([i], i) -> i -> m ([i], i)
forall i w (m :: Type -> Type).
MonadCircuit i (BaseField ctx) w m =>
([i], i) -> i -> m ([i], i)
shiftCarry ([], i
carry) [i]
lows

            Vector (WordCount n ctx) i -> m (Vector (WordCount n ctx) i)
forall a. a -> m a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Vector (WordCount n ctx) i -> m (Vector (WordCount n ctx) i))
-> Vector (WordCount n ctx) i -> m (Vector (WordCount n ctx) i)
forall a b. (a -> b) -> a -> b
$ [i] -> Vector (WordCount n ctx) i
forall (size :: Natural) a. [a] -> Vector size a
unsafeToVector (Natural -> i -> [i]
forall a. Natural -> a -> [a]
replicate Natural
zeroRegs i
z [i] -> [i] -> [i]
forall a. Semigroup a => a -> a -> a
<> (i
newHi i -> [i] -> [i]
forall a. a -> [a] -> [a]
: [i] -> [i]
forall a. [a] -> [a]
Haskell.reverse [i]
newRegs))

        shiftCarry :: MonadCircuit i (BaseField ctx) w m => ([i], i) -> i -> m ([i], i)
        shiftCarry :: forall i w (m :: Type -> Type).
MonadCircuit i (BaseField ctx) w m =>
([i], i) -> i -> m ([i], i)
shiftCarry ([i]
acc, i
carry) i
r = 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
remShift (Natural
regSize Natural -> Natural -> Natural
-! Natural
remShift) i
r
            i
s <- ClosedPoly i (BaseField ctx) -> m i
forall var a w (m :: Type -> Type).
MonadCircuit var a w m =>
ClosedPoly var a -> m var
newAssigned (ClosedPoly i (BaseField ctx) -> m i)
-> ClosedPoly i (BaseField ctx) -> m i
forall a b. (a -> b) -> a -> b
$ \i -> x
p ->  i -> x
p i
h 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
regSize Natural -> Natural -> Natural
-! Natural
remShift)) (i -> x
p i
carry)
            ([i], i) -> m ([i], i)
forall a. a -> m a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (i
s i -> [i] -> [i]
forall a. a -> [a] -> [a]
: [i]
acc, i
l)