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

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

module ZkFold.Symbolic.Data.ByteString
    ( ByteString(..)
    , ShiftBits (..)
    , reverseEndianness
    , isSet
    , isUnset
    , toWords
    , concat
    , truncate
    , emptyByteString
    , toBsBits
    ) where

import           Control.DeepSeq                    (NFData)
import           Control.Monad                      (replicateM)
import           Data.Aeson                         (FromJSON (..), ToJSON (..))
import qualified Data.Bits                          as B
import qualified Data.ByteString                    as Bytes
import           Data.Foldable                      (foldlM)
import           Data.Kind                          (Type)
import           Data.List                          (reverse, unfoldr)
import           Data.Maybe                         (Maybe (..))
import           Data.String                        (IsString (..))
import           Data.Traversable                   (for)
import           GHC.Generics                       (Generic, Par1 (..))
import           GHC.Natural                        (naturalFromInteger)
import           Numeric                            (readHex, showHex)
import           Prelude                            (Integer, const, drop, fmap, otherwise, pure, return, take,
                                                     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.Data.HFunctor          (HFunctor (..))
import           ZkFold.Base.Data.Package           (packWith, unpackWith)
import           ZkFold.Base.Data.Utils             (zipWithM)
import qualified ZkFold.Base.Data.Vector            as V
import           ZkFold.Base.Data.Vector            (Vector (..))
import           ZkFold.Prelude                     (replicateA, (!!))
import           ZkFold.Symbolic.Class
import           ZkFold.Symbolic.Data.Bool          (Bool (..), BoolType (..))
import           ZkFold.Symbolic.Data.Class         (SymbolicData)
import           ZkFold.Symbolic.Data.Combinators
import           ZkFold.Symbolic.Data.Eq            (Eq)
import           ZkFold.Symbolic.Data.Eq.Structural
import           ZkFold.Symbolic.Data.FieldElement  (FieldElement)
import           ZkFold.Symbolic.Data.Input         (SymbolicInput, isValid)
import           ZkFold.Symbolic.Interpreter        (Interpreter (..))
import           ZkFold.Symbolic.MonadCircuit       (ClosedPoly, MonadCircuit, newAssigned)

-- | A ByteString which stores @n@ bits and uses elements of @a@ as registers, one element per register.
-- Bit layout is Big-endian.
--
newtype ByteString (n :: Natural) (context :: (Type -> Type) -> Type) = ByteString (context (Vector n))
    deriving ((forall x. ByteString n context -> Rep (ByteString n context) x)
-> (forall x. Rep (ByteString n context) x -> ByteString n context)
-> Generic (ByteString n context)
forall (n :: Natural) (context :: (Type -> Type) -> Type) x.
Rep (ByteString n context) x -> ByteString n context
forall (n :: Natural) (context :: (Type -> Type) -> Type) x.
ByteString n context -> Rep (ByteString n context) x
forall x. Rep (ByteString n context) x -> ByteString n context
forall x. ByteString n context -> Rep (ByteString n context) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall (n :: Natural) (context :: (Type -> Type) -> Type) x.
ByteString n context -> Rep (ByteString n context) x
from :: forall x. ByteString n context -> Rep (ByteString n context) x
$cto :: forall (n :: Natural) (context :: (Type -> Type) -> Type) x.
Rep (ByteString n context) x -> ByteString n context
to :: forall x. Rep (ByteString n context) x -> ByteString n context
Generic)

deriving stock instance Haskell.Show (c (Vector n)) => Haskell.Show (ByteString n c)
deriving stock instance Haskell.Eq (c (Vector n)) => Haskell.Eq (ByteString n c)
deriving anyclass instance NFData (c (Vector n)) => NFData (ByteString n c)
deriving newtype instance SymbolicData (ByteString n c)


deriving via (Structural (ByteString n c))
         instance (Symbolic c, KnownNat n) => Eq (Bool c) (ByteString n c)

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

instance
    ( Symbolic c
    , m * 8 ~ n
    ) => FromConstant Bytes.ByteString (ByteString n c) where
    fromConstant :: ByteString -> ByteString n c
fromConstant ByteString
bytes = forall (k :: Natural) (m :: Natural) (c :: (Type -> Type) -> Type).
Symbolic c =>
Vector k (ByteString m c) -> ByteString (k * m) c
concat @_ @8 (Vector m (ByteString 8 c) -> ByteString (m * 8) c)
-> Vector m (ByteString 8 c) -> ByteString (m * 8) c
forall a b. (a -> b) -> a -> b
$ forall a b. FromConstant a b => a -> b
fromConstant @Natural @(ByteString 8 c)
        (Natural -> ByteString 8 c)
-> (Word8 -> Natural) -> Word8 -> ByteString 8 c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> Natural
forall a b. (Integral a, Num b) => a -> b
Haskell.fromIntegral
        (Integer -> Natural) -> (Word8 -> Integer) -> Word8 -> Natural
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Word8 -> Integer
forall a. Integral a => a -> Integer
Haskell.toInteger (Word8 -> ByteString 8 c)
-> Vector m Word8 -> Vector m (ByteString 8 c)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall (size :: Natural) a. [a] -> Vector size a
V.unsafeToVector @m ([Word8] -> Vector m Word8) -> [Word8] -> Vector m Word8
forall a b. (a -> b) -> a -> b
$ ByteString -> [Word8]
Bytes.unpack ByteString
bytes)

emptyByteString :: FromConstant Natural (ByteString 0 c) => ByteString 0 c
emptyByteString :: forall (c :: (Type -> Type) -> Type).
FromConstant Natural (ByteString 0 c) =>
ByteString 0 c
emptyByteString = forall a b. FromConstant a b => a -> b
fromConstant @Natural Natural
0


-- | A class for data types that support bit shift and bit cyclic shift (rotation) operations.
--
class ShiftBits a where
    {-# MINIMAL (shiftBits | (shiftBitsL, shiftBitsR)), (rotateBits | (rotateBitsL, rotateBitsR)) #-}

    -- | shiftBits performs a left shift when its agrument is greater than zero and a right shift otherwise.
    --
    shiftBits :: a -> Integer -> a
    shiftBits a
a Integer
s
      | Integer
s Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
0     = a -> Natural -> a
forall a. ShiftBits a => a -> Natural -> a
shiftBitsR a
a (Integer -> Natural
forall a b. (Integral a, Num b) => a -> b
Haskell.fromIntegral (Integer -> Natural) -> (Integer -> Integer) -> Integer -> Natural
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> Integer
forall a. AdditiveGroup a => a -> a
negate (Integer -> Natural) -> Integer -> Natural
forall a b. (a -> b) -> a -> b
$ Integer
s)
      | Bool
otherwise = a -> Natural -> a
forall a. ShiftBits a => a -> Natural -> a
shiftBitsL a
a (Integer -> Natural
forall a b. (Integral a, Num b) => a -> b
Haskell.fromIntegral Integer
s)

    shiftBitsL :: a -> Natural -> a
    shiftBitsL a
a Natural
s = a -> Integer -> a
forall a. ShiftBits a => a -> Integer -> a
shiftBits a
a (Natural -> Integer
forall a b. (Integral a, Num b) => a -> b
Haskell.fromIntegral Natural
s)

    shiftBitsR :: a -> Natural -> a
    shiftBitsR a
a Natural
s = a -> Integer -> a
forall a. ShiftBits a => a -> Integer -> a
shiftBits a
a (Integer -> Integer
forall a. AdditiveGroup a => a -> a
negate (Integer -> Integer) -> (Natural -> Integer) -> Natural -> Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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
s)

    -- | rotateBits performs a left cyclic shift when its agrument is greater than zero and a right cyclic shift otherwise.
    --
    rotateBits :: a -> Integer -> a
    rotateBits a
a Integer
s
      | Integer
s Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
0     = a -> Natural -> a
forall a. ShiftBits a => a -> Natural -> a
rotateBitsR a
a (Integer -> Natural
forall a b. (Integral a, Num b) => a -> b
Haskell.fromIntegral (Integer -> Natural) -> (Integer -> Integer) -> Integer -> Natural
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> Integer
forall a. AdditiveGroup a => a -> a
negate (Integer -> Natural) -> Integer -> Natural
forall a b. (a -> b) -> a -> b
$ Integer
s)
      | Bool
otherwise = a -> Natural -> a
forall a. ShiftBits a => a -> Natural -> a
rotateBitsL a
a (Integer -> Natural
forall a b. (Integral a, Num b) => a -> b
Haskell.fromIntegral Integer
s)

    rotateBitsL :: a -> Natural -> a
    rotateBitsL a
a Natural
s = a -> Integer -> a
forall a. ShiftBits a => a -> Integer -> a
rotateBits a
a (Natural -> Integer
forall a b. (Integral a, Num b) => a -> b
Haskell.fromIntegral Natural
s)

    rotateBitsR :: a -> Natural -> a
    rotateBitsR a
a Natural
s = a -> Integer -> a
forall a. ShiftBits a => a -> Integer -> a
rotateBits a
a (Integer -> Integer
forall a. AdditiveGroup a => a -> a
negate (Integer -> Integer) -> (Natural -> Integer) -> Natural -> Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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
s)



instance ToConstant (ByteString n (Interpreter (Zp p))) where
    type Const (ByteString n (Interpreter (Zp p))) = Natural
    toConstant :: ByteString n (Interpreter (Zp p))
-> Const (ByteString n (Interpreter (Zp p)))
toConstant (ByteString (Interpreter Vector n (Zp p)
bits)) = (Natural -> Zp p -> Natural)
-> Natural -> Vector n (Zp p) -> 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 Zp p
p -> Zp p -> Const (Zp p)
forall a. ToConstant a => a -> Const a
toConstant Zp p
p Natural -> Natural -> Natural
forall a. AdditiveSemigroup a => a -> a -> a
+ Natural
base Natural -> Natural -> Natural
forall a. MultiplicativeSemigroup a => a -> a -> a
* Natural
y) Natural
0 Vector n (Zp p)
bits
        where base :: Natural
base = Natural
2


    -- | Pack a ByteString using one field element per bit.
    -- @fromConstant@ discards bits after @n@.
    -- If the constant is greater than @2^n@, only the part modulo @2^n@ will be converted into a ByteString.
instance (Symbolic c, KnownNat n) => FromConstant Natural (ByteString n c) where
    fromConstant :: Natural -> ByteString n c
fromConstant Natural
n = 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)
-> (Vector n (BaseField c) -> c (Vector n))
-> Vector n (BaseField c)
-> ByteString n 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 n (BaseField c) -> ByteString n c)
-> Vector n (BaseField c) -> ByteString n c
forall a b. (a -> b) -> a -> b
$ [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 Natural
n (forall (n :: Natural). KnownNat n => Natural
value @n)

instance (Symbolic c, KnownNat n) => FromConstant Integer (ByteString n c) where
    fromConstant :: Integer -> ByteString n c
fromConstant = Natural -> ByteString n c
forall a b. FromConstant a b => a -> b
fromConstant (Natural -> ByteString n c)
-> (Integer -> Natural) -> Integer -> ByteString n 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) => Arbitrary (ByteString n c) where
    arbitrary :: Gen (ByteString n c)
arbitrary = 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)
-> ([BaseField c] -> c (Vector n))
-> [BaseField c]
-> ByteString n 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 n (BaseField c) -> c (Vector n))
-> ([BaseField c] -> Vector n (BaseField c))
-> [BaseField c]
-> c (Vector n)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [BaseField c] -> Vector n (BaseField c)
forall (size :: Natural) a. [a] -> Vector size a
V.unsafeToVector ([BaseField c] -> ByteString n c)
-> Gen [BaseField c] -> Gen (ByteString n c)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Natural -> Gen (BaseField c) -> Gen [BaseField c]
forall (f :: Type -> Type) a.
Applicative f =>
Natural -> f a -> f [a]
replicateA (forall (n :: Natural). KnownNat n => Natural
value @n) (Natural -> Gen (BaseField c)
forall {b} {b}.
(FromConstant Integer b, Exponent Integer b) =>
b -> Gen b
toss (Natural
1 :: Natural))
        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)

reverseEndianness' :: forall wordSize k m x {n}.
    ( KnownNat wordSize
    , n ~ k * wordSize
    , m * 8 ~ wordSize
    ) => Vector n x -> Vector n x
reverseEndianness' :: forall (wordSize :: Natural) (k :: Natural) (m :: Natural) x
       {n :: Natural}.
(KnownNat wordSize, n ~ (k * wordSize), (m * 8) ~ wordSize) =>
Vector n x -> Vector n x
reverseEndianness' Vector n x
v =
    let chunks :: Vector k (Vector wordSize x)
chunks = forall (m :: Natural) (n :: Natural) a.
KnownNat n =>
Vector (m * n) a -> Vector m (Vector n a)
V.chunks @k @wordSize Vector n x
Vector (k * wordSize) x
v
        chunks' :: Vector k (Vector wordSize x)
chunks' = (Vector wordSize x -> Vector wordSize x)
-> Vector k (Vector wordSize x) -> Vector k (Vector wordSize x)
forall a b. (a -> b) -> Vector k a -> Vector k b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap (Vector m (Vector 8 x) -> Vector wordSize x
Vector m (Vector 8 x) -> Vector (m * 8) x
forall (m :: Natural) (n :: Natural) a.
Vector m (Vector n a) -> Vector (m * n) a
V.concat (Vector m (Vector 8 x) -> Vector wordSize x)
-> (Vector wordSize x -> Vector m (Vector 8 x))
-> Vector wordSize x
-> Vector wordSize x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Vector m (Vector 8 x) -> Vector m (Vector 8 x)
forall (size :: Natural) a. Vector size a -> Vector size a
V.reverse (Vector m (Vector 8 x) -> Vector m (Vector 8 x))
-> (Vector wordSize x -> Vector m (Vector 8 x))
-> Vector wordSize x
-> Vector m (Vector 8 x)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: Natural) (n :: Natural) a.
KnownNat n =>
Vector (m * n) a -> Vector m (Vector n a)
V.chunks @m @8) Vector k (Vector wordSize x)
chunks
     in Vector k (Vector wordSize x) -> Vector (k * wordSize) x
forall (m :: Natural) (n :: Natural) a.
Vector m (Vector n a) -> Vector (m * n) a
V.concat Vector k (Vector wordSize x)
chunks'

reverseEndianness :: forall wordSize k c m {n}.
    ( Symbolic c
    , KnownNat wordSize
    , n ~ k * wordSize
    , m * 8 ~ wordSize
    ) => ByteString n c -> ByteString n c
reverseEndianness :: forall (wordSize :: Natural) (k :: Natural)
       (c :: (Type -> Type) -> Type) (m :: Natural) {n :: Natural}.
(Symbolic c, KnownNat wordSize, n ~ (k * wordSize),
 (m * 8) ~ wordSize) =>
ByteString n c -> ByteString n c
reverseEndianness (ByteString c (Vector n)
v) = 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
$ (forall a. Vector n a -> Vector n a)
-> c (Vector n) -> c (Vector n)
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 (forall (wordSize :: Natural) (k :: Natural) (m :: Natural) x
       {n :: Natural}.
(KnownNat wordSize, n ~ (k * wordSize), (m * 8) ~ wordSize) =>
Vector n x -> Vector n x
reverseEndianness' @wordSize @k) c (Vector n)
v

instance (Symbolic c, KnownNat n) => BoolType (ByteString n c) where
    false :: ByteString n c
false = Natural -> ByteString n c
forall a b. FromConstant a b => a -> b
fromConstant (Natural
0 :: Natural)
    true :: ByteString n c
true = ByteString n c -> ByteString n c
forall b. BoolType b => b -> b
not ByteString n c
forall b. BoolType b => b
false

    not :: ByteString n c -> ByteString n c
not (ByteString c (Vector n)
bits) =  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 n)
-> CircuitFun (Vector n) (Vector n) (BaseField c) -> c (Vector n)
forall (f :: Type -> Type) (g :: Type -> Type).
c f -> CircuitFun f g (BaseField c) -> c g
forall (c :: (Type -> Type) -> Type) (f :: Type -> Type)
       (g :: Type -> Type).
Symbolic c =>
c f -> CircuitFun f g (BaseField c) -> c g
fromCircuitF c (Vector n)
bits Vector n i -> m (Vector n i)
CircuitFun (Vector n) (Vector n) (BaseField c)
solve
        where
            solve :: MonadCircuit i (BaseField c) m => Vector n i -> m (Vector n i)
            solve :: CircuitFun (Vector n) (Vector n) (BaseField c)
solve Vector n i
xv = do
                let xs :: [i]
xs = Vector n i -> [i]
forall (size :: Natural) a. Vector size a -> [a]
V.fromVector Vector n i
xv
                [i]
ys <-  [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]
xs ((i -> m i) -> m [i]) -> (i -> m i) -> m [i]
forall a b. (a -> b) -> a -> b
$ \i
i -> ClosedPoly i (BaseField c) -> m i
forall var a (m :: Type -> Type).
MonadCircuit var a m =>
ClosedPoly var a -> m var
newAssigned (\i -> x
p -> x
forall a. MultiplicativeMonoid a => a
one x -> x -> x
forall a. AdditiveGroup a => a -> a -> a
- i -> x
p i
i)
                Vector n i -> m (Vector n i)
forall a. a -> m a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (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
V.unsafeToVector [i]
ys

    ByteString n c
l || :: ByteString n c -> ByteString n c -> ByteString n c
|| ByteString n c
r =  ByteString n c
-> ByteString n c
-> (forall i. i -> i -> ClosedPoly i (BaseField c))
-> ByteString n c
forall (c :: (Type -> Type) -> Type) (n :: Natural).
Symbolic c =>
ByteString n c
-> ByteString n c
-> (forall i. i -> i -> ClosedPoly i (BaseField c))
-> ByteString n c
bitwiseOperation ByteString n c
l ByteString n c
r i -> i -> (i -> x) -> x
forall i. i -> i -> ClosedPoly i (BaseField c)
forall {a} {t}.
(AdditiveGroup a, MultiplicativeSemigroup a) =>
t -> t -> (t -> a) -> a
cons
        where
            cons :: t -> t -> (t -> a) -> a
cons t
i t
j t -> a
x =
                        let xi :: a
xi = t -> a
x t
i
                            xj :: a
xj = t -> a
x t
j
                        in a
xi a -> a -> a
forall a. AdditiveSemigroup a => a -> a -> a
+ a
xj a -> a -> a
forall a. AdditiveGroup a => a -> a -> a
- a
xi a -> a -> a
forall a. MultiplicativeSemigroup a => a -> a -> a
* a
xj

    ByteString n c
l && :: ByteString n c -> ByteString n c -> ByteString n c
&& ByteString n c
r = ByteString n c
-> ByteString n c
-> (forall i. i -> i -> ClosedPoly i (BaseField c))
-> ByteString n c
forall (c :: (Type -> Type) -> Type) (n :: Natural).
Symbolic c =>
ByteString n c
-> ByteString n c
-> (forall i. i -> i -> ClosedPoly i (BaseField c))
-> ByteString n c
bitwiseOperation ByteString n c
l ByteString n c
r i -> i -> (i -> x) -> x
forall i. i -> i -> ClosedPoly i (BaseField c)
forall {a} {t}.
MultiplicativeSemigroup a =>
t -> t -> (t -> a) -> a
cons
        where
            cons :: t -> t -> (t -> a) -> a
cons t
i t
j t -> a
x =
                        let xi :: a
xi = t -> a
x t
i
                            xj :: a
xj = t -> a
x t
j
                        in a
xi a -> a -> a
forall a. MultiplicativeSemigroup a => a -> a -> a
* a
xj

    xor :: ByteString n c -> ByteString n c -> ByteString n c
xor (ByteString c (Vector n)
l) (ByteString c (Vector n)
r) = 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 n)
-> c (Vector n)
-> (Vector n (BaseField c)
    -> Vector n (BaseField c) -> Vector n (BaseField c))
-> (forall i (m :: Type -> Type).
    MonadCircuit i (BaseField c) m =>
    Vector n i -> Vector n i -> m (Vector n i))
-> c (Vector n)
forall (c :: (Type -> Type) -> Type) a (f :: Type -> Type)
       (g :: Type -> Type) (h :: Type -> Type).
(Symbolic c, BaseField c ~ a) =>
c f
-> c g
-> (f a -> g a -> h a)
-> (forall i (m :: Type -> Type).
    MonadCircuit i a m =>
    f i -> g i -> m (h i))
-> c h
symbolic2F c (Vector n)
l c (Vector n)
r (\Vector n (BaseField c)
x Vector n (BaseField c)
y -> [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 n (BaseField c) -> Natural
forall a.
(ToConstant a, Const a ~ Natural) =>
Vector n a -> Natural
vecToNat Vector n (BaseField c)
x Natural -> Natural -> Natural
forall a. Bits a => a -> a -> a
`B.xor` Vector n (BaseField c) -> Natural
forall a.
(ToConstant a, Const a ~ Natural) =>
Vector n a -> Natural
vecToNat Vector n (BaseField c)
y) (forall (n :: Natural). KnownNat n => Natural
value @n)) Vector n i -> Vector n i -> m (Vector n i)
forall i (m :: Type -> Type).
MonadCircuit i (BaseField c) m =>
Vector n i -> Vector n i -> m (Vector n i)
solve
        where
            vecToNat :: (ToConstant a, Const a ~ Natural) => Vector n a -> Natural
            vecToNat :: forall a.
(ToConstant a, Const a ~ Natural) =>
Vector n a -> Natural
vecToNat =  (Natural -> a -> Natural) -> Natural -> Vector n a -> 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
x a
p -> a -> Const a
forall a. ToConstant a => a -> Const a
toConstant a
p Natural -> Natural -> Natural
forall a. AdditiveSemigroup a => a -> a -> a
+ Natural
2 Natural -> Natural -> Natural
forall a. MultiplicativeSemigroup a => a -> a -> a
* Natural
x :: Natural) Natural
0

            solve :: MonadCircuit i (BaseField c) m => Vector n i -> Vector n i -> m (Vector n i)
            solve :: forall i (m :: Type -> Type).
MonadCircuit i (BaseField c) m =>
Vector n i -> Vector n i -> m (Vector n i)
solve Vector n i
lv Vector n i
rv = do
                let varsLeft :: Vector n i
varsLeft = Vector n i
lv
                    varsRight :: Vector n i
varsRight = Vector n i
rv
                (i -> i -> m i) -> Vector n i -> Vector n i -> m (Vector n i)
forall (f :: Type -> Type) (m :: Type -> Type) a b c.
(Traversable f, Zip f, Applicative m) =>
(a -> b -> m c) -> f a -> f b -> m (f c)
zipWithM  (\i
i i
j -> ClosedPoly i (BaseField c) -> m i
forall var a (m :: Type -> Type).
MonadCircuit var a m =>
ClosedPoly var a -> m var
newAssigned (ClosedPoly i (BaseField c) -> m i)
-> ClosedPoly i (BaseField c) -> m i
forall a b. (a -> b) -> a -> b
$ i -> i -> (i -> x) -> x
forall {a} {t}.
(AdditiveGroup a, MultiplicativeSemigroup a) =>
t -> t -> (t -> a) -> a
cons i
i i
j) Vector n i
varsLeft Vector n i
varsRight

            cons :: t -> t -> (t -> a) -> a
cons t
i t
j t -> a
x =
                        let xi :: a
xi = t -> a
x t
i
                            xj :: a
xj = t -> a
x t
j
                        in a
xi a -> a -> a
forall a. AdditiveSemigroup a => a -> a -> a
+ a
xj a -> a -> a
forall a. AdditiveGroup a => a -> a -> a
- (a
xi a -> a -> a
forall a. MultiplicativeSemigroup a => a -> a -> a
* a
xj a -> a -> a
forall a. AdditiveSemigroup a => a -> a -> a
+ a
xi a -> a -> a
forall a. MultiplicativeSemigroup a => a -> a -> a
* a
xj)

-- | A ByteString of length @n@ can only be split into words of length @wordSize@ if all of the following conditions are met:
-- 1. @wordSize@ is not greater than @n@;
-- 2. @wordSize@ is not zero;
-- 3. The bytestring is not empty;
-- 4. @wordSize@ divides @n@.
--

toWords :: forall m wordSize c. (Symbolic c, KnownNat wordSize) => ByteString (m * wordSize) c -> Vector m (ByteString wordSize c)
toWords :: forall (m :: Natural) (wordSize :: Natural)
       (c :: (Type -> Type) -> Type).
(Symbolic c, KnownNat wordSize) =>
ByteString (m * wordSize) c -> Vector m (ByteString wordSize c)
toWords (ByteString c (Vector (m * wordSize))
bits) = c (Vector wordSize) -> ByteString wordSize c
forall (n :: Natural) (context :: (Type -> Type) -> Type).
context (Vector n) -> ByteString n context
ByteString (c (Vector wordSize) -> ByteString wordSize c)
-> Vector m (c (Vector wordSize))
-> Vector m (ByteString wordSize c)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall a. Vector (m * wordSize) a -> Vector m (Vector wordSize a))
-> c (Vector (m * wordSize)) -> Vector m (c (Vector wordSize))
forall {k1} (c :: (k1 -> Type) -> Type) (f :: Type -> Type)
       (h :: k1 -> Type) (g :: k1 -> Type).
(Package c, Functor f) =>
(forall (a :: k1). h a -> f (g a)) -> c h -> f (c g)
forall (f :: Type -> Type) (h :: Type -> Type) (g :: Type -> Type).
Functor f =>
(forall a. h a -> f (g a)) -> c h -> f (c g)
unpackWith (forall (m :: Natural) (n :: Natural) a.
KnownNat n =>
Vector (m * n) a -> Vector m (Vector n a)
V.chunks @m @wordSize) c (Vector (m * wordSize))
bits

concat :: forall k m c. (Symbolic c) => Vector k (ByteString m c) -> ByteString (k * m) c
concat :: forall (k :: Natural) (m :: Natural) (c :: (Type -> Type) -> Type).
Symbolic c =>
Vector k (ByteString m c) -> ByteString (k * m) c
concat Vector k (ByteString m c)
bs = c (Vector (k * m)) -> ByteString (k * m) c
forall (n :: Natural) (context :: (Type -> Type) -> Type).
context (Vector n) -> ByteString n context
ByteString (c (Vector (k * m)) -> ByteString (k * m) c)
-> c (Vector (k * m)) -> ByteString (k * m) c
forall a b. (a -> b) -> a -> b
$ (forall a. Vector k (Vector m a) -> Vector (k * m) a)
-> Vector k (c (Vector m)) -> c (Vector (k * m))
forall {k1} (c :: (k1 -> Type) -> Type) (f :: Type -> Type)
       (g :: k1 -> Type) (h :: k1 -> Type).
(Package c, Foldable f, Functor f) =>
(forall (a :: k1). f (g a) -> h a) -> f (c g) -> c h
forall (f :: Type -> Type) (g :: Type -> Type) (h :: Type -> Type).
(Foldable f, Functor f) =>
(forall a. f (g a) -> h a) -> f (c g) -> c h
packWith Vector k (Vector m a) -> Vector (k * m) a
forall (m :: Natural) (n :: Natural) a.
Vector m (Vector n a) -> Vector (m * n) a
forall a. Vector k (Vector m a) -> Vector (k * m) a
V.concat ((\(ByteString c (Vector m)
bits) -> c (Vector m)
bits) (ByteString m c -> c (Vector m))
-> Vector k (ByteString m c) -> Vector k (c (Vector m))
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Vector k (ByteString m c)
bs)

-- | Describes types that can be truncated by dropping several bits from the end (i.e. stored in the lower registers)
--

truncate :: forall n m c. (
    Symbolic c
  , KnownNat n
  , n <= m
  ) => ByteString m c -> ByteString n c
truncate :: forall (n :: Natural) (m :: Natural) (c :: (Type -> Type) -> Type).
(Symbolic c, KnownNat n, n <= m) =>
ByteString m c -> ByteString n c
truncate (ByteString c (Vector m)
bits) = 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
$ (forall a. Vector m a -> Vector n a)
-> c (Vector m) -> c (Vector n)
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 (forall (n :: Natural) (size :: Natural) a.
KnownNat n =>
Vector size a -> Vector n a
V.take @n) c (Vector m)
bits

--------------------------------------------------------------------------------
instance (Symbolic c, KnownNat n) => ShiftBits (ByteString n c) where
    shiftBits :: ByteString n c -> Integer -> ByteString n c
shiftBits bs :: ByteString n c
bs@(ByteString c (Vector n)
oldBits) Integer
s
      | Integer
s Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
0 = ByteString n c
bs
      | Integer -> Integer
forall a. Num a => a -> a
Haskell.abs Integer
s Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= Natural -> Integer
forall a b. (Integral a, Num b) => a -> b
Haskell.fromIntegral (forall (n :: Natural). KnownNat n => Natural
getNatural @n) = ByteString n c
forall b. BoolType b => b
false
      | Bool
otherwise = 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 n)
-> (Vector n (BaseField c) -> Vector n (BaseField c))
-> CircuitFun (Vector n) (Vector n) (BaseField c)
-> c (Vector n)
forall a (f :: Type -> Type) (g :: Type -> Type).
(BaseField c ~ a) =>
c f -> (f a -> g a) -> CircuitFun f g a -> c g
forall (c :: (Type -> Type) -> Type) a (f :: Type -> Type)
       (g :: Type -> Type).
(Symbolic c, BaseField c ~ a) =>
c f -> (f a -> g a) -> CircuitFun f g a -> c g
symbolicF c (Vector n)
oldBits (\Vector n (BaseField c)
v ->  Vector n (BaseField c)
-> Integer -> BaseField c -> Vector n (BaseField c)
forall (size :: Natural) a.
KnownNat size =>
Vector size a -> Integer -> a -> Vector size a
V.shift Vector n (BaseField c)
v Integer
s (Integer -> BaseField c
forall a b. FromConstant a b => a -> b
fromConstant (Integer
0 :: Integer))) Vector n i -> m (Vector n i)
CircuitFun (Vector n) (Vector n) (BaseField c)
solve
      where
        solve :: forall a m. MonadCircuit a (BaseField c) m => Vector n a -> m (Vector n a)
        solve :: CircuitFun (Vector n) (Vector n) (BaseField c)
solve Vector n a
bitsV = do
            let bits :: [a]
bits = Vector n a -> [a]
forall (size :: Natural) a. Vector size a -> [a]
V.fromVector Vector n a
bitsV
            [a]
zeros <- Int -> m a -> m [a]
forall (m :: Type -> Type) a. Applicative m => Int -> m a -> m [a]
replicateM (Integer -> Int
forall a b. (Integral a, Num b) => a -> b
Haskell.fromIntegral (Integer -> Int) -> Integer -> Int
forall a b. (a -> b) -> a -> b
$ Integer -> Integer
forall a. Num a => a -> a
Haskell.abs Integer
s) (m a -> m [a]) -> m a -> m [a]
forall a b. (a -> b) -> a -> b
$ ClosedPoly a (BaseField c) -> m a
forall var a (m :: Type -> Type).
MonadCircuit var a m =>
ClosedPoly var a -> m var
newAssigned (x -> (a -> x) -> x
forall a b. a -> b -> a
Haskell.const x
forall a. AdditiveMonoid a => a
zero)

            let newBits :: [a]
newBits = case Integer
s Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
0 of
                        Bool
Haskell.True  -> Int -> [a] -> [a]
forall a. Int -> [a] -> [a]
take (Natural -> Int
forall a b. (Integral a, Num b) => a -> b
Haskell.fromIntegral (Natural -> Int) -> Natural -> Int
forall a b. (a -> b) -> a -> b
$ forall (n :: Natural). KnownNat n => Natural
getNatural @n) ([a] -> [a]) -> [a] -> [a]
forall a b. (a -> b) -> a -> b
$ [a]
zeros [a] -> [a] -> [a]
forall a. Semigroup a => a -> a -> a
<> [a]
bits
                        Bool
Haskell.False -> Int -> [a] -> [a]
forall a. Int -> [a] -> [a]
drop (Integer -> Int
forall a b. (Integral a, Num b) => a -> b
Haskell.fromIntegral Integer
s) ([a] -> [a]) -> [a] -> [a]
forall a b. (a -> b) -> a -> b
$ [a]
bits [a] -> [a] -> [a]
forall a. Semigroup a => a -> a -> a
<> [a]
zeros

            Vector n a -> m (Vector n a)
forall a. a -> m a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Vector n a -> m (Vector n a)) -> Vector n a -> m (Vector n a)
forall a b. (a -> b) -> a -> b
$ [a] -> Vector n a
forall (size :: Natural) a. [a] -> Vector size a
V.unsafeToVector [a]
newBits

    rotateBits :: ByteString n c -> Integer -> ByteString n c
rotateBits (ByteString c (Vector n)
bits) Integer
s = 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
$ (forall a. Vector n a -> Vector n a)
-> c (Vector n) -> c (Vector n)
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 n a -> Integer -> Vector n a
forall (size :: Natural) a.
KnownNat size =>
Vector size a -> Integer -> Vector size a
`V.rotate` Integer
s) c (Vector n)
bits

instance
  ( Symbolic c
  , KnownNat k
  , KnownNat n
  , k <= n
  ) => Extend (ByteString k c) (ByteString n c) where
    extend :: ByteString k c -> ByteString n c
extend (ByteString c (Vector k)
oldBits) = 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 k)
-> (Vector k (BaseField c) -> Vector n (BaseField c))
-> CircuitFun (Vector k) (Vector n) (BaseField c)
-> c (Vector n)
forall a (f :: Type -> Type) (g :: Type -> Type).
(BaseField c ~ a) =>
c f -> (f a -> g a) -> CircuitFun f g a -> c g
forall (c :: (Type -> Type) -> Type) a (f :: Type -> Type)
       (g :: Type -> Type).
(Symbolic c, BaseField c ~ a) =>
c f -> (f a -> g a) -> CircuitFun f g a -> c g
symbolicF c (Vector k)
oldBits (\Vector k (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
$ [BaseField c]
zeroA [BaseField c] -> [BaseField c] -> [BaseField c]
forall a. Semigroup a => a -> a -> a
<> Vector k (BaseField c) -> [BaseField c]
forall (size :: Natural) a. Vector size a -> [a]
V.fromVector Vector k (BaseField c)
v) Vector k i -> m (Vector n i)
CircuitFun (Vector k) (Vector n) (BaseField c)
solve
      where
        solve :: forall i m. MonadCircuit i (BaseField c) m => Vector k i -> m (Vector n i)
        solve :: CircuitFun (Vector k) (Vector n) (BaseField c)
solve Vector k i
bitsV = do
            let bits :: [i]
bits = Vector k i -> [i]
forall (size :: Natural) a. Vector size a -> [a]
V.fromVector Vector k i
bitsV
            [i]
zeros <- Int -> m i -> m [i]
forall (m :: Type -> Type) a. Applicative m => Int -> m a -> m [a]
replicateM Int
diff (m i -> m [i]) -> m i -> m [i]
forall a b. (a -> b) -> a -> b
$ ClosedPoly i (BaseField c) -> m i
forall var a (m :: Type -> Type).
MonadCircuit var a m =>
ClosedPoly var a -> m var
newAssigned (x -> (i -> x) -> x
forall a b. a -> b -> a
Haskell.const x
forall a. AdditiveMonoid a => a
zero)
            Vector n i -> m (Vector n i)
forall a. a -> m a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (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
V.unsafeToVector ([i] -> Vector n i) -> [i] -> Vector n i
forall a b. (a -> b) -> a -> b
$ [i]
zeros [i] -> [i] -> [i]
forall a. Semigroup a => a -> a -> a
<> [i]
bits

        diff :: Haskell.Int
        diff :: Int
diff = Natural -> Int
forall a b. (Integral a, Num b) => a -> b
Haskell.fromIntegral (Natural -> Int) -> Natural -> Int
forall a b. (a -> b) -> a -> b
$ forall (n :: Natural). KnownNat n => Natural
getNatural @n Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
Haskell.- forall (n :: Natural). KnownNat n => Natural
getNatural @k

        zeroA :: [BaseField c]
zeroA = Int -> BaseField c -> [BaseField c]
forall a. Int -> a -> [a]
Haskell.replicate Int
diff (Integer -> BaseField c
forall a b. FromConstant a b => a -> b
fromConstant (Integer
0 :: Integer ))

instance
  ( Symbolic c
  , KnownNat n
  ) => SymbolicInput (ByteString n c) where
  isValid :: ByteString n c -> Bool (Context (ByteString n c))
isValid (ByteString c (Vector n)
bits) = Context (ByteString n c) Par1 -> Bool (Context (ByteString n c))
forall (c :: (Type -> Type) -> Type). c Par1 -> Bool c
Bool (Context (ByteString n c) Par1 -> Bool (Context (ByteString n c)))
-> Context (ByteString n c) Par1 -> Bool (Context (ByteString n c))
forall a b. (a -> b) -> a -> b
$ c (Vector n) -> CircuitFun (Vector n) Par1 (BaseField c) -> c Par1
forall (f :: Type -> Type) (g :: Type -> Type).
c f -> CircuitFun f g (BaseField c) -> c g
forall (c :: (Type -> Type) -> Type) (f :: Type -> Type)
       (g :: Type -> Type).
Symbolic c =>
c f -> CircuitFun f g (BaseField c) -> c g
fromCircuitF c (Vector n)
bits Vector n i -> m (Par1 i)
CircuitFun (Vector n) Par1 (BaseField c)
solve
    where
        solve :: MonadCircuit i (BaseField c) m => Vector n i -> m (Par1 i)
        solve :: CircuitFun (Vector n) Par1 (BaseField c)
solve Vector n i
v = do
            let vs :: [i]
vs = Vector n i -> [i]
forall (size :: Natural) a. Vector size a -> [a]
V.fromVector Vector n i
v
            [i]
ys <- [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]
vs ((i -> m i) -> m [i]) -> (i -> m i) -> m [i]
forall a b. (a -> b) -> a -> b
$ \i
i -> ClosedPoly i (BaseField c) -> m i
forall var a (m :: Type -> Type).
MonadCircuit var a m =>
ClosedPoly var a -> m var
newAssigned (\i -> x
p -> i -> x
p i
i x -> x -> x
forall a. MultiplicativeSemigroup a => a -> a -> a
* (x
forall a. MultiplicativeMonoid a => a
one x -> x -> x
forall a. AdditiveGroup a => a -> a -> a
- i -> x
p i
i))
            [Par1 i]
us <-[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]
ys ((i -> m (Par1 i)) -> m [Par1 i])
-> (i -> m (Par1 i)) -> m [Par1 i]
forall a b. (a -> b) -> a -> b
$ \i
i -> Par1 i -> m (Par1 i)
forall i a (m :: Type -> Type) (f :: Type -> Type).
(MonadCircuit i a m, Representable f, Traversable f) =>
f i -> m (f i)
isZero (Par1 i -> m (Par1 i)) -> Par1 i -> m (Par1 i)
forall a b. (a -> b) -> a -> b
$ i -> Par1 i
forall p. p -> Par1 p
Par1 i
i
            [Par1 i] -> m (Par1 i)
forall i a (m :: Type -> Type).
MonadCircuit i a m =>
[Par1 i] -> m (Par1 i)
helper [Par1 i]
us

        helper :: MonadCircuit i a m => [Par1 i] -> m (Par1 i)
        helper :: forall i a (m :: Type -> Type).
MonadCircuit i a m =>
[Par1 i] -> m (Par1 i)
helper [Par1 i]
xs = case [Par1 i]
xs of
            []       -> i -> Par1 i
forall p. p -> Par1 p
Par1 (i -> Par1 i) -> m i -> m (Par1 i)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> ClosedPoly i a -> m i
forall var a (m :: Type -> Type).
MonadCircuit var a m =>
ClosedPoly var a -> m var
newAssigned (x -> (i -> x) -> x
forall a b. a -> b -> a
const x
forall a. MultiplicativeMonoid a => a
one)
            (Par1 i
b : [Par1 i]
bs) -> (Par1 i -> Par1 i -> m (Par1 i))
-> Par1 i -> [Par1 i] -> m (Par1 i)
forall (t :: Type -> Type) (m :: Type -> Type) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldlM (\(Par1 i
v1) (Par1 i
v2) -> i -> Par1 i
forall p. p -> Par1 p
Par1 (i -> Par1 i) -> m i -> m (Par1 i)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> ClosedPoly i a -> m i
forall var a (m :: Type -> Type).
MonadCircuit var a m =>
ClosedPoly var a -> m var
newAssigned (((i -> x) -> i -> x
forall a b. (a -> b) -> a -> b
$ i
v1) ((i -> x) -> x) -> ((i -> x) -> x) -> (i -> x) -> x
forall a. MultiplicativeSemigroup a => a -> a -> a
* ((i -> x) -> i -> x
forall a b. (a -> b) -> a -> b
$ i
v2))) Par1 i
b [Par1 i]
bs


isSet :: forall c n. Symbolic c => ByteString n c -> Natural -> Bool c
isSet :: forall (c :: (Type -> Type) -> Type) (n :: Natural).
Symbolic c =>
ByteString n c -> Natural -> Bool c
isSet (ByteString c (Vector n)
bits) Natural
ix = c Par1 -> Bool c
forall (c :: (Type -> Type) -> Type). c Par1 -> Bool c
Bool (c Par1 -> Bool c) -> c Par1 -> Bool c
forall a b. (a -> b) -> a -> b
$ c (Vector n) -> CircuitFun (Vector n) Par1 (BaseField c) -> c Par1
forall (f :: Type -> Type) (g :: Type -> Type).
c f -> CircuitFun f g (BaseField c) -> c g
forall (c :: (Type -> Type) -> Type) (f :: Type -> Type)
       (g :: Type -> Type).
Symbolic c =>
c f -> CircuitFun f g (BaseField c) -> c g
fromCircuitF c (Vector n)
bits Vector n i -> m (Par1 i)
CircuitFun (Vector n) Par1 (BaseField c)
solve
    where
        solve :: forall i m . MonadCircuit i (BaseField c) m => Vector n i -> m (Par1 i)
        solve :: CircuitFun (Vector n) Par1 (BaseField c)
solve Vector n i
v = do
            let vs :: [i]
vs = Vector n i -> [i]
forall (size :: Natural) a. Vector size a -> [a]
V.fromVector Vector n i
v
            Par1 i -> m (Par1 i)
forall a. a -> m a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Par1 i -> m (Par1 i)) -> Par1 i -> m (Par1 i)
forall a b. (a -> b) -> a -> b
$ i -> Par1 i
forall p. p -> Par1 p
Par1 (i -> Par1 i) -> i -> Par1 i
forall a b. (a -> b) -> a -> b
$ ([i] -> Natural -> i
forall a. [a] -> Natural -> a
!! Natural
ix) [i]
vs

isUnset :: forall c n. Symbolic c => ByteString n c -> Natural -> Bool c
isUnset :: forall (c :: (Type -> Type) -> Type) (n :: Natural).
Symbolic c =>
ByteString n c -> Natural -> Bool c
isUnset (ByteString c (Vector n)
bits) Natural
ix = c Par1 -> Bool c
forall (c :: (Type -> Type) -> Type). c Par1 -> Bool c
Bool (c Par1 -> Bool c) -> c Par1 -> Bool c
forall a b. (a -> b) -> a -> b
$ c (Vector n) -> CircuitFun (Vector n) Par1 (BaseField c) -> c Par1
forall (f :: Type -> Type) (g :: Type -> Type).
c f -> CircuitFun f g (BaseField c) -> c g
forall (c :: (Type -> Type) -> Type) (f :: Type -> Type)
       (g :: Type -> Type).
Symbolic c =>
c f -> CircuitFun f g (BaseField c) -> c g
fromCircuitF c (Vector n)
bits Vector n i -> m (Par1 i)
CircuitFun (Vector n) Par1 (BaseField c)
solve
    where
        solve :: forall i m . MonadCircuit i (BaseField c) m => Vector n i -> m (Par1 i)
        solve :: CircuitFun (Vector n) Par1 (BaseField c)
solve Vector n i
v = do
            let vs :: [i]
vs = Vector n i -> [i]
forall (size :: Natural) a. Vector size a -> [a]
V.fromVector Vector n i
v
                i :: i
i = ([i] -> Natural -> i
forall a. [a] -> Natural -> a
!! Natural
ix) [i]
vs
            i
j <- ClosedPoly i (BaseField c) -> m i
forall var a (m :: Type -> Type).
MonadCircuit var a m =>
ClosedPoly var a -> m var
newAssigned (ClosedPoly i (BaseField c) -> m i)
-> ClosedPoly i (BaseField c) -> m i
forall a b. (a -> b) -> a -> b
$ \i -> x
p -> x
forall a. MultiplicativeMonoid a => a
one x -> x -> x
forall a. AdditiveGroup a => a -> a -> a
- i -> x
p i
i
            Par1 i -> m (Par1 i)
forall a. a -> m a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Par1 i -> m (Par1 i)) -> Par1 i -> m (Par1 i)
forall a b. (a -> b) -> a -> b
$ i -> Par1 i
forall p. p -> Par1 p
Par1 i
j

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

toBsBits :: Natural -> Natural -> [Natural]
toBsBits :: Natural -> Natural -> [Natural]
toBsBits Natural
num Natural
n = [Natural] -> [Natural]
forall a. [a] -> [a]
reverse [Natural]
bits
    where
        base :: Natural
base = Natural
2

        availableBits :: [Natural]
availableBits = (Natural -> Maybe (Natural, Natural)) -> Natural -> [Natural]
forall b a. (b -> Maybe (a, b)) -> b -> [a]
unfoldr (Natural -> Natural -> Maybe (Natural, Natural)
toBase Natural
base) (Natural
num Natural -> Natural -> Natural
forall a. Integral a => a -> a -> a
`Haskell.mod` (Natural
2 Natural -> Natural -> Natural
forall a b. (Num a, Integral b) => a -> b -> a
Haskell.^ Natural
n)) [Natural] -> [Natural] -> [Natural]
forall a. Semigroup a => a -> a -> a
<> Natural -> [Natural]
forall a. a -> [a]
Haskell.repeat Natural
0

        bits :: [Natural]
bits = Int -> [Natural] -> [Natural]
forall a. Int -> [a] -> [a]
take (Natural -> Int
forall a b. (Integral a, Num b) => a -> b
Haskell.fromIntegral Natural
n) [Natural]
availableBits

-- | Convert a number into @base@-ary system.

toBase :: Natural -> Natural -> Maybe (Natural, Natural)
toBase :: Natural -> Natural -> Maybe (Natural, Natural)
toBase Natural
_ Natural
0    = Maybe (Natural, Natural)
forall a. Maybe a
Nothing
toBase Natural
base Natural
b = let (Natural
d, Natural
m) = Natural
b Natural -> Natural -> (Natural, Natural)
forall a. SemiEuclidean a => a -> a -> (a, a)
`divMod` Natural
base in (Natural, Natural) -> Maybe (Natural, Natural)
forall a. a -> Maybe a
Just (Natural
m, Natural
d)


-- | A generic bitwise operation on two ByteStrings.
-- TODO: Shall we expose it to users? Can they do something malicious having such function? AFAIK there are checks that constrain each bit to 0 or 1.
--
bitwiseOperation
    :: forall c n
    .  Symbolic c
    => ByteString n c
    -> ByteString n c
    -> (forall i. i -> i -> ClosedPoly i (BaseField c))
    -> ByteString n c
bitwiseOperation :: forall (c :: (Type -> Type) -> Type) (n :: Natural).
Symbolic c =>
ByteString n c
-> ByteString n c
-> (forall i. i -> i -> ClosedPoly i (BaseField c))
-> ByteString n c
bitwiseOperation (ByteString c (Vector n)
bits1) (ByteString c (Vector n)
bits2) forall i. i -> i -> ClosedPoly i (BaseField c)
cons = 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 n)
-> c (Vector n)
-> (forall i (m :: Type -> Type).
    MonadCircuit i (BaseField c) m =>
    Vector n i -> Vector n i -> m (Vector n i))
-> c (Vector n)
forall (c :: (Type -> Type) -> Type) (f :: Type -> Type)
       (g :: Type -> Type) (h :: Type -> Type).
Symbolic c =>
c f
-> c g
-> (forall i (m :: Type -> Type).
    MonadCircuit i (BaseField c) m =>
    f i -> g i -> m (h i))
-> c h
fromCircuit2F c (Vector n)
bits1 c (Vector n)
bits2 Vector n i -> Vector n i -> m (Vector n i)
forall i (m :: Type -> Type).
MonadCircuit i (BaseField c) m =>
Vector n i -> Vector n i -> m (Vector n i)
solve
    where
        solve :: MonadCircuit i (BaseField c) m => Vector n i -> Vector n i -> m (Vector n i)
        solve :: forall i (m :: Type -> Type).
MonadCircuit i (BaseField c) m =>
Vector n i -> Vector n i -> m (Vector n i)
solve Vector n i
lv Vector n i
rv = do
            let varsLeft :: Vector n i
varsLeft = Vector n i
lv
                varsRight :: Vector n i
varsRight = Vector n i
rv
            (i -> i -> m i) -> Vector n i -> Vector n i -> m (Vector n i)
forall (f :: Type -> Type) (m :: Type -> Type) a b c.
(Traversable f, Zip f, Applicative m) =>
(a -> b -> m c) -> f a -> f b -> m (f c)
zipWithM  (\i
i i
j -> ClosedPoly i (BaseField c) -> m i
forall var a (m :: Type -> Type).
MonadCircuit var a m =>
ClosedPoly var a -> m var
newAssigned (ClosedPoly i (BaseField c) -> m i)
-> ClosedPoly i (BaseField c) -> m i
forall a b. (a -> b) -> a -> b
$ i -> i -> ClosedPoly i (BaseField c)
forall i. i -> i -> ClosedPoly i (BaseField c)
cons i
i i
j) Vector n i
varsLeft Vector n i
varsRight

instance (Symbolic c, NumberOfBits (BaseField c) ~ n) => Iso (FieldElement c) (ByteString n c) where
  from :: FieldElement c -> ByteString n c
from = 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)
-> (FieldElement c -> c (Vector n))
-> FieldElement c
-> ByteString n c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FieldElement c -> c (Vector n)
FieldElement c -> Bits (FieldElement c)
forall a. BinaryExpansion a => a -> Bits a
binaryExpansion

instance (Symbolic c, NumberOfBits (BaseField c) ~ n) => Iso (ByteString n c) (FieldElement c) where
  from :: ByteString n c -> FieldElement c
from (ByteString c (Vector n)
a) = Bits (FieldElement c) -> FieldElement c
forall a. BinaryExpansion a => Bits a -> a
fromBinary c (Vector n)
Bits (FieldElement c)
a

instance (Symbolic c, KnownNat n)
    => FromJSON (ByteString n c) where
    parseJSON :: Value -> Parser (ByteString n c)
parseJSON Value
val = do
        String
str <- Value -> Parser String
forall a. FromJSON a => Value -> Parser a
parseJSON Value
val
        case forall (c :: (Type -> Type) -> Type) (n :: Natural).
(Symbolic c, KnownNat n) =>
String -> Maybe (ByteString n c)
hexToByteString @c @n String
str of
            Maybe (ByteString n c)
Nothing -> String -> Parser (ByteString n c)
forall a. String -> Parser a
forall (m :: Type -> Type) a. MonadFail m => String -> m a
Haskell.fail String
"bad bytestring!"
            Just ByteString n c
a  -> ByteString n c -> Parser (ByteString n c)
forall a. a -> Parser a
forall (m :: Type -> Type) a. Monad m => a -> m a
return ByteString n c
a

instance ToJSON (ByteString n (Interpreter (Zp p))) where
    toJSON :: ByteString n (Interpreter (Zp p)) -> Value
toJSON = String -> Value
forall a. ToJSON a => a -> Value
toJSON (String -> Value)
-> (ByteString n (Interpreter (Zp p)) -> String)
-> ByteString n (Interpreter (Zp p))
-> Value
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ByteString n (Interpreter (Zp p)) -> String
forall (n :: Natural) (p :: Natural).
ByteString n (Interpreter (Zp p)) -> String
byteStringToHex

byteStringToHex :: ByteString n (Interpreter (Zp p)) -> Haskell.String
byteStringToHex :: forall (n :: Natural) (p :: Natural).
ByteString n (Interpreter (Zp p)) -> String
byteStringToHex ByteString n (Interpreter (Zp p))
bytes = Natural -> ShowS
forall a. Integral a => a -> ShowS
showHex (ByteString n (Interpreter (Zp p))
-> Const (ByteString n (Interpreter (Zp p)))
forall a. ToConstant a => a -> Const a
toConstant ByteString n (Interpreter (Zp p))
bytes :: Natural) String
""

hexToByteString :: (Symbolic c, KnownNat n) => Haskell.String -> Maybe (ByteString n c)
hexToByteString :: forall (c :: (Type -> Type) -> Type) (n :: Natural).
(Symbolic c, KnownNat n) =>
String -> Maybe (ByteString n c)
hexToByteString String
str = case ReadS Natural
forall a. (Eq a, Num a) => ReadS a
readHex String
str of
    [(Natural
n, String
"")] -> ByteString n c -> Maybe (ByteString n c)
forall a. a -> Maybe a
Just (forall a b. FromConstant a b => a -> b
fromConstant @Natural Natural
n)
    [(Natural, String)]
_         -> Maybe (ByteString n c)
forall a. Maybe a
Nothing