{-# LANGUAGE AllowAmbiguousTypes  #-}
{-# LANGUAGE BlockArguments       #-}
{-# LANGUAGE DerivingStrategies   #-}
{-# LANGUAGE NoStarIsType         #-}
{-# LANGUAGE TypeOperators        #-}
{-# LANGUAGE UndecidableInstances #-}

module ZkFold.Symbolic.Data.FFA (FFA (..), KnownFFA) where

import           Control.DeepSeq                   (NFData)
import           Control.Monad                     (Monad (..))
import           Data.Bits                         (shiftL)
import           Data.Bool                         (otherwise)
import           Data.Function                     (const, ($), (.))
import           Data.Functor                      (($>))
import           Data.Functor.Rep                  (Representable (..))
import           Data.Proxy                        (Proxy (..))
import           Data.Traversable                  (Traversable (..))
import           Data.Type.Equality                (type (~))
import           GHC.Generics                      (Generic, Par1 (..), U1 (..), type (:*:) (..))
import           Numeric.Natural                   (Natural)
import           Prelude                           (Integer)
import qualified Prelude
import           Text.Show                         (Show)

import           ZkFold.Base.Algebra.Basic.Class
import           ZkFold.Base.Algebra.Basic.Field   (Zp)
import           ZkFold.Base.Algebra.Basic.Number  (KnownNat, Prime, type (*), type (^), value)
import           ZkFold.Base.Data.Vector           (Vector)
import           ZkFold.Symbolic.Class             (Arithmetic, Symbolic (..), fromCircuit2F, symbolicF)
import           ZkFold.Symbolic.Data.Bool         (Bool (..), BoolType (..))
import           ZkFold.Symbolic.Data.ByteString   (ByteString)
import           ZkFold.Symbolic.Data.Class        (SymbolicData (..))
import           ZkFold.Symbolic.Data.Combinators  (Ceil, GetRegisterSize, Iso (..), KnownRegisterSize, KnownRegisters,
                                                    NumberOfRegisters, Resize (..))
import           ZkFold.Symbolic.Data.Conditional  (Conditional (..))
import           ZkFold.Symbolic.Data.Eq           (Eq (..))
import           ZkFold.Symbolic.Data.FieldElement (FieldElement (..))
import           ZkFold.Symbolic.Data.Input        (SymbolicInput (..))
import           ZkFold.Symbolic.Data.Ord          (Ord (..))
import           ZkFold.Symbolic.Data.UInt         (OrdWord, UInt (..), natural, register, toNative)
import           ZkFold.Symbolic.Interpreter       (Interpreter (..))
import           ZkFold.Symbolic.MonadCircuit      (MonadCircuit (..), ResidueField (..), Witness (..))

type family FFAUIntSize (p :: Natural) (q :: Natural) :: Natural where
  FFAUIntSize p p = 0
  FFAUIntSize p q = NumberOfBits (Zp (Ceil (p * p) q))

type UIntFFA p r c = UInt (FFAUIntSize p (Order (BaseField c))) r c

data FFA p r c = FFA
  { forall (p :: Natural) (r :: RegisterSize)
       (c :: (Type -> Type) -> Type).
FFA p r c -> FieldElement c
nativeResidue :: FieldElement c
  , forall (p :: Natural) (r :: RegisterSize)
       (c :: (Type -> Type) -> Type).
FFA p r c -> UIntFFA p r c
uintResidue   :: UIntFFA p r c
  }
  deriving ((forall x. FFA p r c -> Rep (FFA p r c) x)
-> (forall x. Rep (FFA p r c) x -> FFA p r c)
-> Generic (FFA p r c)
forall (p :: Natural) (r :: RegisterSize)
       (c :: (Type -> Type) -> Type) x.
Rep (FFA p r c) x -> FFA p r c
forall (p :: Natural) (r :: RegisterSize)
       (c :: (Type -> Type) -> Type) x.
FFA p r c -> Rep (FFA p r c) x
forall x. Rep (FFA p r c) x -> FFA p r c
forall x. FFA p r c -> Rep (FFA p r c) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall (p :: Natural) (r :: RegisterSize)
       (c :: (Type -> Type) -> Type) x.
FFA p r c -> Rep (FFA p r c) x
from :: forall x. FFA p r c -> Rep (FFA p r c) x
$cto :: forall (p :: Natural) (r :: RegisterSize)
       (c :: (Type -> Type) -> Type) x.
Rep (FFA p r c) x -> FFA p r c
to :: forall x. Rep (FFA p r c) x -> FFA p r c
Generic)

type FFAMaxValue p q = q * (2 ^ FFAUIntSize p q)

type FFAMaxBits p c = NumberOfBits (Zp (FFAMaxValue p (Order (BaseField c))))

type KnownFFA p r c =
  ( KnownNat (FFAUIntSize p (Order (BaseField c)))
  , KnownNat p
  , KnownRegisterSize r
  , KnownRegisters c (FFAUIntSize p (Order (BaseField c))) r
  , KnownNat (FFAMaxBits p c)
  , KnownNat (GetRegisterSize (BaseField c) (FFAMaxBits p c) r)
  , KnownRegisters c (FFAMaxBits p c) r
  , KnownNat (Ceil (GetRegisterSize (BaseField c) (FFAMaxBits p c) r) OrdWord)
  , KnownRegisters c (NumberOfBits (Zp p)) r
  , KnownNat (GetRegisterSize (BaseField c) (NumberOfBits (Zp p)) r)
  , KnownNat (NumberOfBits (Zp p)))

instance (Symbolic c, KnownFFA p r c) => SymbolicData (FFA p r c)
instance (Symbolic c, KnownFFA p r c) => SymbolicInput (FFA p r c) where
  isValid :: FFA p r c -> Bool (Context (FFA p r c))
isValid ffa :: FFA p r c
ffa@(FFA FieldElement c
_ UInt (FFAUIntSize p (Order (BaseField c))) r c
ux) =
    UInt (FFAUIntSize p (Order (BaseField c))) r c
-> Bool (Context (UInt (FFAUIntSize p (Order (BaseField c))) r c))
forall d. SymbolicInput d => d -> Bool (Context d)
isValid UInt (FFAUIntSize p (Order (BaseField c))) r c
ux Bool c -> Bool c -> Bool c
forall b. BoolType b => b -> b -> b
&& forall (n :: Natural) (p :: Natural) (r :: RegisterSize)
       (c :: (Type -> Type) -> Type).
(Symbolic c, KnownFFA p r c, KnownNat n,
 KnownNat (NumberOfRegisters (BaseField c) n r),
 KnownNat (GetRegisterSize (BaseField c) n r)) =>
FFA p r c -> UInt n r c
toUInt @(FFAMaxBits p c) FFA p r c
ffa UInt
  (Log2
     ((Order (BaseField c) * (2 ^ FFAUIntSize p (Order (BaseField c))))
      - 1)
   + 1)
  r
  c
-> UInt
     (Log2
        ((Order (BaseField c) * (2 ^ FFAUIntSize p (Order (BaseField c))))
         - 1)
      + 1)
     r
     c
-> BooleanOf
     (UInt
        (Log2
           ((Order (BaseField c) * (2 ^ FFAUIntSize p (Order (BaseField c))))
            - 1)
         + 1)
        r
        c)
forall a. Ord a => a -> a -> BooleanOf a
< Natural
-> UInt
     (Log2
        ((Order (BaseField c) * (2 ^ FFAUIntSize p (Order (BaseField c))))
         - 1)
      + 1)
     r
     c
forall a b. FromConstant a b => a -> b
fromConstant (forall (n :: Natural). KnownNat n => Natural
value @p)
instance (NFData (FieldElement c), NFData (UIntFFA p r c)) => NFData (FFA p r c)
instance (Symbolic c, KnownFFA p r c, b ~ Bool c) => Conditional b (FFA p r c)
instance (Symbolic c, KnownFFA p r c) => Eq (FFA p r c)
deriving stock instance (Show (FieldElement c), Show (UIntFFA p r c)) =>
  Show (FFA p r c)

bezoutFFA ::
  forall p a. (KnownNat p, KnownNat (FFAUIntSize p (Order a))) => Integer
bezoutFFA :: forall (p :: Natural) a.
(KnownNat p, KnownNat (FFAUIntSize p (Order a))) =>
Integer
bezoutFFA =
  Integer -> Integer -> Integer
forall a. Euclidean a => a -> a -> a
bezoutR (Integer
1 Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
`shiftL` Natural -> Int
forall a b. (Integral a, Num b) => a -> b
Prelude.fromIntegral (forall (n :: Natural). KnownNat n => Natural
value @(FFAUIntSize p (Order a))))
          (Natural -> Integer
forall a b. FromConstant a b => a -> b
fromConstant (Natural -> Integer) -> Natural -> Integer
forall a b. (a -> b) -> a -> b
$ forall (n :: Natural). KnownNat n => Natural
value @p)

instance (Arithmetic a, KnownFFA p r (Interpreter a)) =>
    ToConstant (FFA p r (Interpreter a)) where
  type Const (FFA p r (Interpreter a)) = Zp p
  toConstant :: FFA p r (Interpreter a) -> Const (FFA p r (Interpreter a))
toConstant (FFA FieldElement (Interpreter a)
nx UIntFFA p r (Interpreter a)
ux) =
    let n :: Integer
n = Const a -> Integer
forall a b. FromConstant a b => a -> b
fromConstant (a -> Const a
forall a. ToConstant a => a -> Const a
toConstant (FieldElement (Interpreter a)
-> Const (FieldElement (Interpreter a))
forall a. ToConstant a => a -> Const a
toConstant FieldElement (Interpreter a)
nx))
        u :: Integer
u = Const (UInt (FFAUIntSize p (Order a)) r (Interpreter a)) -> Integer
forall a b. FromConstant a b => a -> b
fromConstant (UInt (FFAUIntSize p (Order a)) r (Interpreter a)
-> Const (UInt (FFAUIntSize p (Order a)) r (Interpreter a))
forall a. ToConstant a => a -> Const a
toConstant UInt (FFAUIntSize p (Order a)) r (Interpreter a)
UIntFFA p r (Interpreter a)
ux) :: Integer
        -- x = k|a| + n = l*2^s + u
        -- k|a| - l*2^s = u - n
        k :: Integer
k = (Integer
u Integer -> Integer -> Integer
forall a. AdditiveGroup a => a -> a -> a
- Integer
n) Integer -> Integer -> Integer
forall a. MultiplicativeSemigroup a => a -> a -> a
* forall (p :: Natural) a.
(KnownNat p, KnownNat (FFAUIntSize p (Order a))) =>
Integer
bezoutFFA @p @a
     in Integer -> Zp p
forall a b. FromConstant a b => a -> b
fromConstant (Integer
k Integer -> Integer -> Integer
forall a. MultiplicativeSemigroup a => a -> a -> a
* Natural -> Integer
forall a b. FromConstant a b => a -> b
fromConstant (forall a. Finite a => Natural
order @a) Integer -> Integer -> Integer
forall a. AdditiveSemigroup a => a -> a -> a
+ Integer
n)

instance (Symbolic c, KnownFFA p r c, FromConstant a (Zp p)) =>
    FromConstant a (FFA p r c) where
  fromConstant :: a -> FFA p r c
fromConstant a
c =
    let c' :: Const (Zp p)
c' = Zp p -> Const (Zp p)
forall a. ToConstant a => a -> Const a
toConstant (a -> Zp p
forall a b. FromConstant a b => a -> b
fromConstant a
c :: Zp p)
     in FieldElement c
-> UInt (FFAUIntSize p (Order (BaseField c))) r c -> FFA p r c
forall (p :: Natural) (r :: RegisterSize)
       (c :: (Type -> Type) -> Type).
FieldElement c -> UIntFFA p r c -> FFA p r c
FFA (Natural -> FieldElement c
forall a b. FromConstant a b => a -> b
fromConstant Natural
Const (Zp p)
c') (Natural -> UInt (FFAUIntSize p (Order (BaseField c))) r c
forall a b. FromConstant a b => a -> b
fromConstant Natural
Const (Zp p)
c')

instance {-# OVERLAPPING #-} FromConstant (FFA p r c) (FFA p r c)

instance {-# OVERLAPPING #-}
  (Symbolic c, KnownFFA p r c) => Scale (FFA p r c) (FFA p r c)

valueFFA ::
  forall p r c i a.
  (Symbolic c, KnownFFA p r c, Witness i (WitnessField c), a ~ BaseField c) =>
  (Par1 :*: Vector (NumberOfRegisters a (FFAUIntSize p (Order a)) r)) i ->
  IntegralOf (WitnessField c)
valueFFA :: forall (p :: Natural) (r :: RegisterSize)
       (c :: (Type -> Type) -> Type) i a.
(Symbolic c, KnownFFA p r c, Witness i (WitnessField c),
 a ~ BaseField c) =>
(:*:)
  Par1 (Vector (NumberOfRegisters a (FFAUIntSize p (Order a)) r)) i
-> IntegralOf (WitnessField c)
valueFFA (Par1 i
ni :*: Vector (NumberOfRegisters a (FFAUIntSize p (Order a)) r) i
ui) =
  let n :: IntegralOf (WitnessField c)
n = WitnessField c -> IntegralOf (WitnessField c)
forall a. ResidueField a => a -> IntegralOf a
toIntegral (i -> WitnessField c
forall i w. Witness i w => i -> w
at i
ni :: WitnessField c)
      u :: IntegralOf (WitnessField c)
u = forall (c :: (Type -> Type) -> Type) (n :: Natural)
       (r :: RegisterSize) i.
(Symbolic c, KnownNat n, KnownRegisterSize r,
 Witness i (WitnessField c)) =>
Vector (NumberOfRegisters (BaseField c) n r) i
-> IntegralOf (WitnessField c)
natural @c @(FFAUIntSize p (Order a)) @r Vector (NumberOfRegisters a (FFAUIntSize p (Order a)) r) i
Vector
  (NumberOfRegisters (BaseField c) (FFAUIntSize p (Order a)) r) i
ui
      k :: IntegralOf (WitnessField c)
k = (IntegralOf (WitnessField c)
u IntegralOf (WitnessField c)
-> IntegralOf (WitnessField c) -> IntegralOf (WitnessField c)
forall a. AdditiveGroup a => a -> a -> a
- IntegralOf (WitnessField c)
n) IntegralOf (WitnessField c)
-> IntegralOf (WitnessField c) -> IntegralOf (WitnessField c)
forall a. MultiplicativeSemigroup a => a -> a -> a
* Integer -> IntegralOf (WitnessField c)
forall a b. FromConstant a b => a -> b
fromConstant (forall (p :: Natural) a.
(KnownNat p, KnownNat (FFAUIntSize p (Order a))) =>
Integer
bezoutFFA @p @a)
   in IntegralOf (WitnessField c)
k IntegralOf (WitnessField c)
-> IntegralOf (WitnessField c) -> IntegralOf (WitnessField c)
forall a. MultiplicativeSemigroup a => a -> a -> a
* Natural -> IntegralOf (WitnessField c)
forall a b. FromConstant a b => a -> b
fromConstant (forall a. Finite a => Natural
order @a) IntegralOf (WitnessField c)
-> IntegralOf (WitnessField c) -> IntegralOf (WitnessField c)
forall a. AdditiveSemigroup a => a -> a -> a
+ IntegralOf (WitnessField c)
n

layoutFFA ::
  forall p r c a w.
  (Symbolic c, KnownFFA p r c, a ~ BaseField c, w ~ WitnessField c) =>
  IntegralOf w ->
  (Par1 :*: Vector (NumberOfRegisters a (FFAUIntSize p (Order a)) r)) w
layoutFFA :: forall (p :: Natural) (r :: RegisterSize)
       (c :: (Type -> Type) -> Type) a w.
(Symbolic c, KnownFFA p r c, a ~ BaseField c,
 w ~ WitnessField c) =>
IntegralOf w
-> (:*:)
     Par1 (Vector (NumberOfRegisters a (FFAUIntSize p (Order a)) r)) w
layoutFFA IntegralOf w
c =
  w -> Par1 w
forall p. p -> Par1 p
Par1 (IntegralOf w -> w
forall a. ResidueField a => IntegralOf a -> a
fromIntegral IntegralOf w
c)
  Par1 w
-> Vector (NumberOfRegisters a (FFAUIntSize p (Order a)) r) w
-> (:*:)
     Par1 (Vector (NumberOfRegisters a (FFAUIntSize p (Order a)) r)) w
forall k (f :: k -> Type) (g :: k -> Type) (p :: k).
f p -> g p -> (:*:) f g p
:*: (Rep (Vector (NumberOfRegisters a (FFAUIntSize p (Order a)) r))
 -> w)
-> Vector (NumberOfRegisters a (FFAUIntSize p (Order a)) r) w
forall a.
(Rep (Vector (NumberOfRegisters a (FFAUIntSize p (Order a)) r))
 -> a)
-> Vector (NumberOfRegisters a (FFAUIntSize p (Order a)) r) a
forall (f :: Type -> Type) a.
Representable f =>
(Rep f -> a) -> f a
tabulate (forall (c :: (Type -> Type) -> Type) (n :: Natural)
       (r :: RegisterSize).
(Symbolic c, KnownNat n, KnownRegisterSize r) =>
IntegralOf (WitnessField c)
-> Zp (NumberOfRegisters (BaseField c) n r) -> WitnessField c
register @c @(FFAUIntSize p (Order a)) @r IntegralOf w
IntegralOf (WitnessField c)
c)

fromFFA ::
  forall p r a.
  (Arithmetic a, KnownFFA p r (Interpreter a)) =>
  (Par1 :*: Vector (NumberOfRegisters a (FFAUIntSize p (Order a)) r)) a ->
  Integer
fromFFA :: forall (p :: Natural) (r :: RegisterSize) a.
(Arithmetic a, KnownFFA p r (Interpreter a)) =>
(:*:)
  Par1 (Vector (NumberOfRegisters a (FFAUIntSize p (Order a)) r)) a
-> Integer
fromFFA (Par1 a
x :*: Vector (NumberOfRegisters a (FFAUIntSize p (Order a)) r) a
v) =
  Const (Zp p) -> Integer
forall a b. FromConstant a b => a -> b
fromConstant (Const (Zp p) -> Integer) -> Const (Zp p) -> Integer
forall a b. (a -> b) -> a -> b
$ Zp p -> Const (Zp p)
forall a. ToConstant a => a -> Const a
toConstant (Zp p -> Const (Zp p)) -> Zp p -> Const (Zp p)
forall a b. (a -> b) -> a -> b
$ FFA p r (Interpreter a) -> Const (FFA p r (Interpreter a))
forall a. ToConstant a => a -> Const a
toConstant
    (FFA p r (Interpreter a) -> Const (FFA p r (Interpreter a)))
-> FFA p r (Interpreter a) -> Const (FFA p r (Interpreter a))
forall a b. (a -> b) -> a -> b
$ forall (p :: Natural) (r :: RegisterSize)
       (c :: (Type -> Type) -> Type).
FieldElement c -> UIntFFA p r c -> FFA p r c
FFA @p @r (a -> FieldElement (Interpreter a)
forall a b. FromConstant a b => a -> b
fromConstant a
x) (Interpreter
  a
  (Vector
     (NumberOfRegisters
        (BaseField (Interpreter a)) (FFAUIntSize p (Order a)) r))
-> UInt (FFAUIntSize p (Order a)) r (Interpreter a)
forall (n :: Natural) (r :: RegisterSize)
       (context :: (Type -> Type) -> Type).
context (Vector (NumberOfRegisters (BaseField context) n r))
-> UInt n r context
UInt (Vector (NumberOfRegisters a (FFAUIntSize p (Order a)) r) a
-> Interpreter
     a (Vector (NumberOfRegisters a (FFAUIntSize p (Order a)) r))
forall {k} (a :: k) (f :: k -> Type). f a -> Interpreter a f
Interpreter Vector (NumberOfRegisters a (FFAUIntSize p (Order a)) r) a
v))

toFFA ::
  forall p r a.
  (Arithmetic a, KnownFFA p r (Interpreter a)) =>
  Integer ->
  (Par1 :*: Vector (NumberOfRegisters a (FFAUIntSize p (Order a)) r)) a
toFFA :: forall (p :: Natural) (r :: RegisterSize) a.
(Arithmetic a, KnownFFA p r (Interpreter a)) =>
Integer
-> (:*:)
     Par1 (Vector (NumberOfRegisters a (FFAUIntSize p (Order a)) r)) a
toFFA Integer
n =
  let FFA (FieldElement (Interpreter Par1 a
x)) (UInt (Interpreter Vector
  (NumberOfRegisters
     (BaseField (Interpreter a))
     (FFAUIntSize p (Order (BaseField (Interpreter a))))
     r)
  a
v)) =
        Integer -> FFA p r (Interpreter a)
forall a b. FromConstant a b => a -> b
fromConstant Integer
n :: FFA p r (Interpreter a)
   in Par1 a
x Par1 a
-> Vector (NumberOfRegisters a (FFAUIntSize p (Order a)) r) a
-> (:*:)
     Par1 (Vector (NumberOfRegisters a (FFAUIntSize p (Order a)) r)) a
forall k (f :: k -> Type) (g :: k -> Type) (p :: k).
f p -> g p -> (:*:) f g p
:*: Vector (NumberOfRegisters a (FFAUIntSize p (Order a)) r) a
Vector
  (NumberOfRegisters
     (BaseField (Interpreter a))
     (FFAUIntSize p (Order (BaseField (Interpreter a))))
     r)
  a
v

instance (Symbolic c, KnownFFA p r c) => MultiplicativeSemigroup (FFA p r c) where
  FFA FieldElement c
nx UInt (FFAUIntSize p (Order (BaseField c))) r c
ux * :: FFA p r c -> FFA p r c -> FFA p r c
* FFA FieldElement c
ny UInt (FFAUIntSize p (Order (BaseField c))) r c
uy = FieldElement c
-> UInt (FFAUIntSize p (Order (BaseField c))) r c -> FFA p r c
forall (p :: Natural) (r :: RegisterSize)
       (c :: (Type -> Type) -> Type).
FieldElement c -> UIntFFA p r c -> FFA p r c
FFA FieldElement c
nr UInt (FFAUIntSize p (Order (BaseField c))) r c
ur
    where
      p :: FromConstant Natural a => a
      p :: forall a. FromConstant Natural a => a
p = Natural -> a
forall a b. FromConstant a b => a -> b
fromConstant (forall (n :: Natural). KnownNat n => Natural
value @p)
      -- | Computes unconstrained \(d = ab div p\) and \(m = ab mod p\)
      nd, nm :: FieldElement c
      ud, um :: UIntFFA p r c
      (FieldElement c
nd, UInt (FFAUIntSize p (Order (BaseField c))) r c
ud, FieldElement c
nm, UInt (FFAUIntSize p (Order (BaseField c))) r c
um) = (Support
   (FieldElement c, UInt (FFAUIntSize p (Order (BaseField c))) r c,
    FieldElement c, UInt (FFAUIntSize p (Order (BaseField c))) r c)
 -> (c (Layout
          (FieldElement c, UInt (FFAUIntSize p (Order (BaseField c))) r c,
           FieldElement c, UInt (FFAUIntSize p (Order (BaseField c))) r c)),
     Payload
       (FieldElement c, UInt (FFAUIntSize p (Order (BaseField c))) r c,
        FieldElement c, UInt (FFAUIntSize p (Order (BaseField c))) r c)
       (WitnessField c)))
-> (FieldElement c, UInt (FFAUIntSize p (Order (BaseField c))) r c,
    FieldElement c, UInt (FFAUIntSize p (Order (BaseField c))) r c)
forall x (c :: (Type -> Type) -> Type).
(SymbolicData x, Context x ~ c) =>
(Support x -> (c (Layout x), Payload x (WitnessField c))) -> x
forall (c :: (Type -> Type) -> Type).
(Context
   (FieldElement c, UInt (FFAUIntSize p (Order (BaseField c))) r c,
    FieldElement c, UInt (FFAUIntSize p (Order (BaseField c))) r c)
 ~ c) =>
(Support
   (FieldElement c, UInt (FFAUIntSize p (Order (BaseField c))) r c,
    FieldElement c, UInt (FFAUIntSize p (Order (BaseField c))) r c)
 -> (c (Layout
          (FieldElement c, UInt (FFAUIntSize p (Order (BaseField c))) r c,
           FieldElement c, UInt (FFAUIntSize p (Order (BaseField c))) r c)),
     Payload
       (FieldElement c, UInt (FFAUIntSize p (Order (BaseField c))) r c,
        FieldElement c, UInt (FFAUIntSize p (Order (BaseField c))) r c)
       (WitnessField c)))
-> (FieldElement c, UInt (FFAUIntSize p (Order (BaseField c))) r c,
    FieldElement c, UInt (FFAUIntSize p (Order (BaseField c))) r c)
restore ((Support
    (FieldElement c, UInt (FFAUIntSize p (Order (BaseField c))) r c,
     FieldElement c, UInt (FFAUIntSize p (Order (BaseField c))) r c)
  -> (c (Layout
           (FieldElement c, UInt (FFAUIntSize p (Order (BaseField c))) r c,
            FieldElement c, UInt (FFAUIntSize p (Order (BaseField c))) r c)),
      Payload
        (FieldElement c, UInt (FFAUIntSize p (Order (BaseField c))) r c,
         FieldElement c, UInt (FFAUIntSize p (Order (BaseField c))) r c)
        (WitnessField c)))
 -> (FieldElement c, UInt (FFAUIntSize p (Order (BaseField c))) r c,
     FieldElement c, UInt (FFAUIntSize p (Order (BaseField c))) r c))
-> (Support
      (FieldElement c, UInt (FFAUIntSize p (Order (BaseField c))) r c,
       FieldElement c, UInt (FFAUIntSize p (Order (BaseField c))) r c)
    -> (c (Layout
             (FieldElement c, UInt (FFAUIntSize p (Order (BaseField c))) r c,
              FieldElement c, UInt (FFAUIntSize p (Order (BaseField c))) r c)),
        Payload
          (FieldElement c, UInt (FFAUIntSize p (Order (BaseField c))) r c,
           FieldElement c, UInt (FFAUIntSize p (Order (BaseField c))) r c)
          (WitnessField c)))
-> (FieldElement c, UInt (FFAUIntSize p (Order (BaseField c))) r c,
    FieldElement c, UInt (FFAUIntSize p (Order (BaseField c))) r c)
forall a b. (a -> b) -> a -> b
$ (c ((Par1
     :*: Vector
           (NumberOfRegisters
              (BaseField c) (FFAUIntSize p (Order (BaseField c))) r))
    :*: (Par1
         :*: Vector
               (NumberOfRegisters
                  (BaseField c) (FFAUIntSize p (Order (BaseField c))) r))),
 (:*:) (U1 :*: U1) (U1 :*: U1) (WitnessField c))
-> Proxy c
-> (c ((Par1
        :*: Vector
              (NumberOfRegisters
                 (BaseField c) (FFAUIntSize p (Order (BaseField c))) r))
       :*: (Par1
            :*: Vector
                  (NumberOfRegisters
                     (BaseField c) (FFAUIntSize p (Order (BaseField c))) r))),
    (:*:) (U1 :*: U1) (U1 :*: U1) (WitnessField c))
forall a b. a -> b -> a
const
        ( c ((Par1
    :*: Layout (UInt (FFAUIntSize p (Order (BaseField c))) r c))
   :*: (Par1
        :*: Layout (UInt (FFAUIntSize p (Order (BaseField c))) r c)))
-> ((:*:)
      (Par1 :*: Layout (UInt (FFAUIntSize p (Order (BaseField c))) r c))
      (Par1 :*: Layout (UInt (FFAUIntSize p (Order (BaseField c))) r c))
      (BaseField c)
    -> (:*:)
         (Par1
          :*: Vector
                (NumberOfRegisters
                   (BaseField c) (FFAUIntSize p (Order (BaseField c))) r))
         (Par1
          :*: Vector
                (NumberOfRegisters
                   (BaseField c) (FFAUIntSize p (Order (BaseField c))) r))
         (BaseField c))
-> CircuitFun
     '[(Par1
        :*: Layout (UInt (FFAUIntSize p (Order (BaseField c))) r c))
       :*: (Par1
            :*: Layout (UInt (FFAUIntSize p (Order (BaseField c))) r c))]
     ((Par1
       :*: Vector
             (NumberOfRegisters
                (BaseField c) (FFAUIntSize p (Order (BaseField c))) r))
      :*: (Par1
           :*: Vector
                 (NumberOfRegisters
                    (BaseField c) (FFAUIntSize p (Order (BaseField c))) r)))
     c
-> c ((Par1
       :*: Vector
             (NumberOfRegisters
                (BaseField c) (FFAUIntSize p (Order (BaseField c))) r))
      :*: (Par1
           :*: Vector
                 (NumberOfRegisters
                    (BaseField c) (FFAUIntSize p (Order (BaseField c))) r)))
forall (c :: (Type -> Type) -> Type) a (f :: Type -> Type)
       (g :: Type -> Type).
(Symbolic c, BaseField c ~ a) =>
c f -> (f a -> g a) -> CircuitFun '[f] g c -> c g
symbolicF ((FieldElement c, UInt (FFAUIntSize p (Order (BaseField c))) r c,
 FieldElement c, UInt (FFAUIntSize p (Order (BaseField c))) r c)
-> Support
     (FieldElement c, UInt (FFAUIntSize p (Order (BaseField c))) r c,
      FieldElement c, UInt (FFAUIntSize p (Order (BaseField c))) r c)
-> Context
     (FieldElement c, UInt (FFAUIntSize p (Order (BaseField c))) r c,
      FieldElement c, UInt (FFAUIntSize p (Order (BaseField c))) r c)
     (Layout
        (FieldElement c, UInt (FFAUIntSize p (Order (BaseField c))) r c,
         FieldElement c, UInt (FFAUIntSize p (Order (BaseField c))) r c))
forall x. SymbolicData x => x -> Support x -> Context x (Layout x)
arithmetize (FieldElement c
nx, UInt (FFAUIntSize p (Order (BaseField c))) r c
ux, FieldElement c
ny, UInt (FFAUIntSize p (Order (BaseField c))) r c
uy) Proxy c
Support
  (FieldElement c, UInt (FFAUIntSize p (Order (BaseField c))) r c,
   FieldElement c, UInt (FFAUIntSize p (Order (BaseField c))) r c)
forall {k} (t :: k). Proxy t
Proxy)
            (\((forall (p :: Natural) (r :: RegisterSize) a.
(Arithmetic a, KnownFFA p r (Interpreter a)) =>
(:*:)
  Par1 (Vector (NumberOfRegisters a (FFAUIntSize p (Order a)) r)) a
-> Integer
fromFFA @p @r -> Integer
a) :*: (forall (p :: Natural) (r :: RegisterSize) a.
(Arithmetic a, KnownFFA p r (Interpreter a)) =>
(:*:)
  Par1 (Vector (NumberOfRegisters a (FFAUIntSize p (Order a)) r)) a
-> Integer
fromFFA @p @r -> Integer
b)) ->
              forall (p :: Natural) (r :: RegisterSize) a.
(Arithmetic a, KnownFFA p r (Interpreter a)) =>
Integer
-> (:*:)
     Par1 (Vector (NumberOfRegisters a (FFAUIntSize p (Order a)) r)) a
toFFA @p @r ((Integer
a Integer -> Integer -> Integer
forall a. MultiplicativeSemigroup a => a -> a -> a
* Integer
b) Integer -> Integer -> Integer
forall a. SemiEuclidean a => a -> a -> a
`div` Integer
forall a. FromConstant Natural a => a
p) (:*:)
  Par1
  (Vector
     (NumberOfRegisters
        (BaseField c) (FFAUIntSize p (Order (BaseField c))) r))
  (BaseField c)
-> (:*:)
     Par1
     (Vector
        (NumberOfRegisters
           (BaseField c) (FFAUIntSize p (Order (BaseField c))) r))
     (BaseField c)
-> (:*:)
     (Par1
      :*: Vector
            (NumberOfRegisters
               (BaseField c) (FFAUIntSize p (Order (BaseField c))) r))
     (Par1
      :*: Vector
            (NumberOfRegisters
               (BaseField c) (FFAUIntSize p (Order (BaseField c))) r))
     (BaseField c)
forall k (f :: k -> Type) (g :: k -> Type) (p :: k).
f p -> g p -> (:*:) f g p
:*: forall (p :: Natural) (r :: RegisterSize) a.
(Arithmetic a, KnownFFA p r (Interpreter a)) =>
Integer
-> (:*:)
     Par1 (Vector (NumberOfRegisters a (FFAUIntSize p (Order a)) r)) a
toFFA @p @r ((Integer
a Integer -> Integer -> Integer
forall a. MultiplicativeSemigroup a => a -> a -> a
* Integer
b) Integer -> Integer -> Integer
forall a. SemiEuclidean a => a -> a -> a
`mod` Integer
forall a. FromConstant Natural a => a
p)
            )
            \((forall (p :: Natural) (r :: RegisterSize)
       (c :: (Type -> Type) -> Type) i a.
(Symbolic c, KnownFFA p r c, Witness i (WitnessField c),
 a ~ BaseField c) =>
(:*:)
  Par1 (Vector (NumberOfRegisters a (FFAUIntSize p (Order a)) r)) i
-> IntegralOf (WitnessField c)
valueFFA @p @r @c -> IntegralOf (WitnessField c)
a) :*: (forall (p :: Natural) (r :: RegisterSize)
       (c :: (Type -> Type) -> Type) i a.
(Symbolic c, KnownFFA p r c, Witness i (WitnessField c),
 a ~ BaseField c) =>
(:*:)
  Par1 (Vector (NumberOfRegisters a (FFAUIntSize p (Order a)) r)) i
-> IntegralOf (WitnessField c)
valueFFA @p @r @c -> IntegralOf (WitnessField c)
b)) -> do
              (WitnessField c -> m i)
-> (:*:)
     (Par1
      :*: Vector
            (NumberOfRegisters
               (BaseField c) (FFAUIntSize p (Order (BaseField c))) r))
     (Par1
      :*: Vector
            (NumberOfRegisters
               (BaseField c) (FFAUIntSize p (Order (BaseField c))) r))
     (WitnessField c)
-> m ((:*:)
        (Par1
         :*: Vector
               (NumberOfRegisters
                  (BaseField c) (FFAUIntSize p (Order (BaseField c))) r))
        (Par1
         :*: Vector
               (NumberOfRegisters
                  (BaseField c) (FFAUIntSize p (Order (BaseField c))) r))
        i)
forall (t :: Type -> Type) (f :: Type -> Type) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: Type -> Type) a b.
Applicative f =>
(a -> f b)
-> (:*:)
     (Par1
      :*: Vector
            (NumberOfRegisters
               (BaseField c) (FFAUIntSize p (Order (BaseField c))) r))
     (Par1
      :*: Vector
            (NumberOfRegisters
               (BaseField c) (FFAUIntSize p (Order (BaseField c))) r))
     a
-> f ((:*:)
        (Par1
         :*: Vector
               (NumberOfRegisters
                  (BaseField c) (FFAUIntSize p (Order (BaseField c))) r))
        (Par1
         :*: Vector
               (NumberOfRegisters
                  (BaseField c) (FFAUIntSize p (Order (BaseField c))) r))
        b)
traverse WitnessField c -> m i
forall var a w (m :: Type -> Type).
MonadCircuit var a w m =>
w -> m var
unconstrained
                  ((:*:)
   (Par1
    :*: Vector
          (NumberOfRegisters
             (BaseField c) (FFAUIntSize p (Order (BaseField c))) r))
   (Par1
    :*: Vector
          (NumberOfRegisters
             (BaseField c) (FFAUIntSize p (Order (BaseField c))) r))
   (WitnessField c)
 -> m ((:*:)
         (Par1
          :*: Vector
                (NumberOfRegisters
                   (BaseField c) (FFAUIntSize p (Order (BaseField c))) r))
         (Par1
          :*: Vector
                (NumberOfRegisters
                   (BaseField c) (FFAUIntSize p (Order (BaseField c))) r))
         i))
-> (:*:)
     (Par1
      :*: Vector
            (NumberOfRegisters
               (BaseField c) (FFAUIntSize p (Order (BaseField c))) r))
     (Par1
      :*: Vector
            (NumberOfRegisters
               (BaseField c) (FFAUIntSize p (Order (BaseField c))) r))
     (WitnessField c)
-> m ((:*:)
        (Par1
         :*: Vector
               (NumberOfRegisters
                  (BaseField c) (FFAUIntSize p (Order (BaseField c))) r))
        (Par1
         :*: Vector
               (NumberOfRegisters
                  (BaseField c) (FFAUIntSize p (Order (BaseField c))) r))
        i)
forall a b. (a -> b) -> a -> b
$ forall (p :: Natural) (r :: RegisterSize)
       (c :: (Type -> Type) -> Type) a w.
(Symbolic c, KnownFFA p r c, a ~ BaseField c,
 w ~ WitnessField c) =>
IntegralOf w
-> (:*:)
     Par1 (Vector (NumberOfRegisters a (FFAUIntSize p (Order a)) r)) w
layoutFFA @p @r @c ((IntegralOf (WitnessField c)
a IntegralOf (WitnessField c)
-> IntegralOf (WitnessField c) -> IntegralOf (WitnessField c)
forall a. MultiplicativeSemigroup a => a -> a -> a
* IntegralOf (WitnessField c)
b) IntegralOf (WitnessField c)
-> IntegralOf (WitnessField c) -> IntegralOf (WitnessField c)
forall a. SemiEuclidean a => a -> a -> a
`div` IntegralOf (WitnessField c)
forall a. FromConstant Natural a => a
p)
                  (:*:)
  Par1
  (Vector
     (NumberOfRegisters
        (BaseField c) (FFAUIntSize p (Order (BaseField c))) r))
  (WitnessField c)
-> (:*:)
     Par1
     (Vector
        (NumberOfRegisters
           (BaseField c) (FFAUIntSize p (Order (BaseField c))) r))
     (WitnessField c)
-> (:*:)
     (Par1
      :*: Vector
            (NumberOfRegisters
               (BaseField c) (FFAUIntSize p (Order (BaseField c))) r))
     (Par1
      :*: Vector
            (NumberOfRegisters
               (BaseField c) (FFAUIntSize p (Order (BaseField c))) r))
     (WitnessField c)
forall k (f :: k -> Type) (g :: k -> Type) (p :: k).
f p -> g p -> (:*:) f g p
:*: forall (p :: Natural) (r :: RegisterSize)
       (c :: (Type -> Type) -> Type) a w.
(Symbolic c, KnownFFA p r c, a ~ BaseField c,
 w ~ WitnessField c) =>
IntegralOf w
-> (:*:)
     Par1 (Vector (NumberOfRegisters a (FFAUIntSize p (Order a)) r)) w
layoutFFA @p @r @c ((IntegralOf (WitnessField c)
a IntegralOf (WitnessField c)
-> IntegralOf (WitnessField c) -> IntegralOf (WitnessField c)
forall a. MultiplicativeSemigroup a => a -> a -> a
* IntegralOf (WitnessField c)
b) IntegralOf (WitnessField c)
-> IntegralOf (WitnessField c) -> IntegralOf (WitnessField c)
forall a. SemiEuclidean a => a -> a -> a
`mod` IntegralOf (WitnessField c)
forall a. FromConstant Natural a => a
p)
        , (U1 (WitnessField c)
forall k (p :: k). U1 p
U1 U1 (WitnessField c)
-> U1 (WitnessField c) -> (:*:) U1 U1 (WitnessField c)
forall k (f :: k -> Type) (g :: k -> Type) (p :: k).
f p -> g p -> (:*:) f g p
:*: U1 (WitnessField c)
forall k (p :: k). U1 p
U1) (:*:) U1 U1 (WitnessField c)
-> (:*:) U1 U1 (WitnessField c)
-> (:*:) (U1 :*: U1) (U1 :*: U1) (WitnessField c)
forall k (f :: k -> Type) (g :: k -> Type) (p :: k).
f p -> g p -> (:*:) f g p
:*: (U1 (WitnessField c)
forall k (p :: k). U1 p
U1 U1 (WitnessField c)
-> U1 (WitnessField c) -> (:*:) U1 U1 (WitnessField c)
forall k (f :: k -> Type) (g :: k -> Type) (p :: k).
f p -> g p -> (:*:) f g p
:*: U1 (WitnessField c)
forall k (p :: k). U1 p
U1))
      -- | Constraints:
      -- * UInt registers are indeed registers;
      -- * m < p;
      -- * equation holds modulo basefield;
      -- * equation holds modulo 2^k.
      Bool Context (UInt (FFAUIntSize p (Order (BaseField c))) r c) Par1
ck = (UInt (FFAUIntSize p (Order (BaseField c))) r c, FFA p r c)
-> Bool
     (Context
        (UInt (FFAUIntSize p (Order (BaseField c))) r c, FFA p r c))
forall d. SymbolicInput d => d -> Bool (Context d)
isValid (UInt (FFAUIntSize p (Order (BaseField c))) r c
ud, forall (p :: Natural) (r :: RegisterSize)
       (c :: (Type -> Type) -> Type).
FieldElement c -> UIntFFA p r c -> FFA p r c
FFA @p FieldElement c
nm UInt (FFAUIntSize p (Order (BaseField c))) r c
um)
                Bool (Context (UInt (FFAUIntSize p (Order (BaseField c))) r c))
-> Bool (Context (UInt (FFAUIntSize p (Order (BaseField c))) r c))
-> Bool (Context (UInt (FFAUIntSize p (Order (BaseField c))) r c))
forall b. BoolType b => b -> b -> b
&& (FieldElement c
nx FieldElement c -> FieldElement c -> FieldElement c
forall a. MultiplicativeSemigroup a => a -> a -> a
* FieldElement c
ny FieldElement c -> FieldElement c -> BooleanOf (FieldElement c)
forall a. Eq a => a -> a -> BooleanOf a
== FieldElement c
nd FieldElement c -> FieldElement c -> FieldElement c
forall a. MultiplicativeSemigroup a => a -> a -> a
* FieldElement c
forall a. FromConstant Natural a => a
p FieldElement c -> FieldElement c -> FieldElement c
forall a. AdditiveSemigroup a => a -> a -> a
+ FieldElement c
nm)
                Bool (Context (UInt (FFAUIntSize p (Order (BaseField c))) r c))
-> Bool (Context (UInt (FFAUIntSize p (Order (BaseField c))) r c))
-> Bool (Context (UInt (FFAUIntSize p (Order (BaseField c))) r c))
forall b. BoolType b => b -> b -> b
&& (UInt (FFAUIntSize p (Order (BaseField c))) r c
ux UInt (FFAUIntSize p (Order (BaseField c))) r c
-> UInt (FFAUIntSize p (Order (BaseField c))) r c
-> UInt (FFAUIntSize p (Order (BaseField c))) r c
forall a. MultiplicativeSemigroup a => a -> a -> a
* UInt (FFAUIntSize p (Order (BaseField c))) r c
uy UInt (FFAUIntSize p (Order (BaseField c))) r c
-> UInt (FFAUIntSize p (Order (BaseField c))) r c
-> BooleanOf (UInt (FFAUIntSize p (Order (BaseField c))) r c)
forall a. Eq a => a -> a -> BooleanOf a
== UInt (FFAUIntSize p (Order (BaseField c))) r c
ud UInt (FFAUIntSize p (Order (BaseField c))) r c
-> UInt (FFAUIntSize p (Order (BaseField c))) r c
-> UInt (FFAUIntSize p (Order (BaseField c))) r c
forall a. MultiplicativeSemigroup a => a -> a -> a
* UInt (FFAUIntSize p (Order (BaseField c))) r c
forall a. FromConstant Natural a => a
p UInt (FFAUIntSize p (Order (BaseField c))) r c
-> UInt (FFAUIntSize p (Order (BaseField c))) r c
-> UInt (FFAUIntSize p (Order (BaseField c))) r c
forall a. AdditiveSemigroup a => a -> a -> a
+ UInt (FFAUIntSize p (Order (BaseField c))) r c
um)
      -- | Sew constraints into result.
      (FieldElement c
nr, UInt (FFAUIntSize p (Order (BaseField c))) r c
ur) = (Support
   (FieldElement c, UInt (FFAUIntSize p (Order (BaseField c))) r c)
 -> (c (Layout
          (FieldElement c, UInt (FFAUIntSize p (Order (BaseField c))) r c)),
     Payload
       (FieldElement c, UInt (FFAUIntSize p (Order (BaseField c))) r c)
       (WitnessField c)))
-> (FieldElement c, UInt (FFAUIntSize p (Order (BaseField c))) r c)
forall x (c :: (Type -> Type) -> Type).
(SymbolicData x, Context x ~ c) =>
(Support x -> (c (Layout x), Payload x (WitnessField c))) -> x
forall (c :: (Type -> Type) -> Type).
(Context
   (FieldElement c, UInt (FFAUIntSize p (Order (BaseField c))) r c)
 ~ c) =>
(Support
   (FieldElement c, UInt (FFAUIntSize p (Order (BaseField c))) r c)
 -> (c (Layout
          (FieldElement c, UInt (FFAUIntSize p (Order (BaseField c))) r c)),
     Payload
       (FieldElement c, UInt (FFAUIntSize p (Order (BaseField c))) r c)
       (WitnessField c)))
-> (FieldElement c, UInt (FFAUIntSize p (Order (BaseField c))) r c)
restore ((Support
    (FieldElement c, UInt (FFAUIntSize p (Order (BaseField c))) r c)
  -> (c (Layout
           (FieldElement c, UInt (FFAUIntSize p (Order (BaseField c))) r c)),
      Payload
        (FieldElement c, UInt (FFAUIntSize p (Order (BaseField c))) r c)
        (WitnessField c)))
 -> (FieldElement c,
     UInt (FFAUIntSize p (Order (BaseField c))) r c))
-> (Support
      (FieldElement c, UInt (FFAUIntSize p (Order (BaseField c))) r c)
    -> (c (Layout
             (FieldElement c, UInt (FFAUIntSize p (Order (BaseField c))) r c)),
        Payload
          (FieldElement c, UInt (FFAUIntSize p (Order (BaseField c))) r c)
          (WitnessField c)))
-> (FieldElement c, UInt (FFAUIntSize p (Order (BaseField c))) r c)
forall a b. (a -> b) -> a -> b
$ (c (Par1
    :*: Layout (UInt (FFAUIntSize p (Order (BaseField c))) r c)),
 (:*:) U1 U1 (WitnessField c))
-> Proxy c
-> (c (Par1
       :*: Layout (UInt (FFAUIntSize p (Order (BaseField c))) r c)),
    (:*:) U1 U1 (WitnessField c))
forall a b. a -> b -> a
const
        ( c (Par1
   :*: (Layout (UInt (FFAUIntSize p (Order (BaseField c))) r c)
        :*: Par1))
-> CircuitFun
     '[Par1
       :*: (Layout (UInt (FFAUIntSize p (Order (BaseField c))) r c)
            :*: Par1)]
     (Par1 :*: Layout (UInt (FFAUIntSize p (Order (BaseField c))) r c))
     c
-> c (Par1
      :*: Layout (UInt (FFAUIntSize p (Order (BaseField c))) r c))
forall (f :: Type -> Type) (g :: Type -> Type).
c f -> CircuitFun '[f] g c -> c g
forall (c :: (Type -> Type) -> Type) (f :: Type -> Type)
       (g :: Type -> Type).
Symbolic c =>
c f -> CircuitFun '[f] g c -> c g
fromCircuitF ((FieldElement c, UInt (FFAUIntSize p (Order (BaseField c))) r c,
 Context (UInt (FFAUIntSize p (Order (BaseField c))) r c) Par1)
-> Support
     (FieldElement c, UInt (FFAUIntSize p (Order (BaseField c))) r c,
      Context (UInt (FFAUIntSize p (Order (BaseField c))) r c) Par1)
-> Context
     (FieldElement c, UInt (FFAUIntSize p (Order (BaseField c))) r c,
      Context (UInt (FFAUIntSize p (Order (BaseField c))) r c) Par1)
     (Layout
        (FieldElement c, UInt (FFAUIntSize p (Order (BaseField c))) r c,
         Context (UInt (FFAUIntSize p (Order (BaseField c))) r c) Par1))
forall x. SymbolicData x => x -> Support x -> Context x (Layout x)
arithmetize (FieldElement c
nm, UInt (FFAUIntSize p (Order (BaseField c))) r c
um, Context (UInt (FFAUIntSize p (Order (BaseField c))) r c) Par1
ck) Proxy c
Support
  (FieldElement c, UInt (FFAUIntSize p (Order (BaseField c))) r c,
   Context (UInt (FFAUIntSize p (Order (BaseField c))) r c) Par1)
forall {k} (t :: k). Proxy t
Proxy)
            \(Par1 i
ni :*: Vector
  (NumberOfRegisters
     (BaseField c) (FFAUIntSize p (Order (BaseField c))) r)
  i
ui :*: Par1 i
b) -> do
              ClosedPoly i (BaseField c) -> m ()
forall var a w (m :: Type -> Type).
MonadCircuit var a w m =>
ClosedPoly var a -> m ()
constraint (((i -> x) -> i -> x
forall a b. (a -> b) -> a -> b
$ i
b) ((i -> x) -> x) -> ((i -> x) -> x) -> (i -> x) -> x
forall a. AdditiveGroup a => a -> a -> a
- (i -> x) -> x
forall a. MultiplicativeMonoid a => a
one)
              (:*:)
  Par1
  (Vector
     (NumberOfRegisters
        (BaseField c) (FFAUIntSize p (Order (BaseField c))) r))
  i
-> m ((:*:)
        Par1
        (Vector
           (NumberOfRegisters
              (BaseField c) (FFAUIntSize p (Order (BaseField c))) r))
        i)
forall a. a -> m a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Par1 i
ni Par1 i
-> Vector
     (NumberOfRegisters
        (BaseField c) (FFAUIntSize p (Order (BaseField c))) r)
     i
-> (:*:)
     Par1
     (Vector
        (NumberOfRegisters
           (BaseField c) (FFAUIntSize p (Order (BaseField c))) r))
     i
forall k (f :: k -> Type) (g :: k -> Type) (p :: k).
f p -> g p -> (:*:) f g p
:*: Vector
  (NumberOfRegisters
     (BaseField c) (FFAUIntSize p (Order (BaseField c))) r)
  i
ui)
        , U1 (WitnessField c)
forall k (p :: k). U1 p
U1 U1 (WitnessField c)
-> U1 (WitnessField c) -> (:*:) U1 U1 (WitnessField c)
forall k (f :: k -> Type) (g :: k -> Type) (p :: k).
f p -> g p -> (:*:) f g p
:*: U1 (WitnessField c)
forall k (p :: k). U1 p
U1)

instance (Symbolic c, KnownFFA p r c) => Exponent (FFA p r c) Natural where
  FFA p r c
x ^ :: FFA p r c -> Natural -> FFA p r c
^ Natural
a = FFA p r c
x FFA p r c -> Natural -> FFA p r c
forall a. MultiplicativeMonoid a => a -> Natural -> a
`natPow` (Natural
a Natural -> Natural -> Natural
forall a. SemiEuclidean a => a -> a -> a
`mod` (forall (n :: Natural). KnownNat n => Natural
value @p Natural -> Natural -> Natural
-! Natural
1))

instance (Symbolic c, KnownFFA p r c) => MultiplicativeMonoid (FFA p r c) where
  one :: FFA p r c
one = Zp p -> FFA p r c
forall a b. FromConstant a b => a -> b
fromConstant (Zp p
forall a. MultiplicativeMonoid a => a
one :: Zp p)

instance (Symbolic c, KnownFFA p r c) => AdditiveSemigroup (FFA p r c) where
  FFA FieldElement c
nx UInt (FFAUIntSize p (Order (BaseField c))) r c
ux + :: FFA p r c -> FFA p r c -> FFA p r c
+ FFA FieldElement c
ny UInt (FFAUIntSize p (Order (BaseField c))) r c
uy = FieldElement c
-> UInt (FFAUIntSize p (Order (BaseField c))) r c -> FFA p r c
forall (p :: Natural) (r :: RegisterSize)
       (c :: (Type -> Type) -> Type).
FieldElement c -> UIntFFA p r c -> FFA p r c
FFA FieldElement c
nr UInt (FFAUIntSize p (Order (BaseField c))) r c
ur
    where
      p :: FromConstant Natural a => a
      p :: forall a. FromConstant Natural a => a
p = Natural -> a
forall a b. FromConstant a b => a -> b
fromConstant (forall (n :: Natural). KnownNat n => Natural
value @p)
      -- | Computes unconstrained \(d = ab div p\) and \(m = ab mod p\).
      -- \(d\) must be {0, 1} as addition can only overflow so much.
      d :: Bool c
      nm :: FieldElement c
      um :: UIntFFA p r c
      (Bool c
d, FieldElement c
nm, UInt (FFAUIntSize p (Order (BaseField c))) r c
um) = (Support
   (Bool c, FieldElement c,
    UInt (FFAUIntSize p (Order (BaseField c))) r c)
 -> (c (Layout
          (Bool c, FieldElement c,
           UInt (FFAUIntSize p (Order (BaseField c))) r c)),
     Payload
       (Bool c, FieldElement c,
        UInt (FFAUIntSize p (Order (BaseField c))) r c)
       (WitnessField c)))
-> (Bool c, FieldElement c,
    UInt (FFAUIntSize p (Order (BaseField c))) r c)
forall x (c :: (Type -> Type) -> Type).
(SymbolicData x, Context x ~ c) =>
(Support x -> (c (Layout x), Payload x (WitnessField c))) -> x
forall (c :: (Type -> Type) -> Type).
(Context
   (Bool c, FieldElement c,
    UInt (FFAUIntSize p (Order (BaseField c))) r c)
 ~ c) =>
(Support
   (Bool c, FieldElement c,
    UInt (FFAUIntSize p (Order (BaseField c))) r c)
 -> (c (Layout
          (Bool c, FieldElement c,
           UInt (FFAUIntSize p (Order (BaseField c))) r c)),
     Payload
       (Bool c, FieldElement c,
        UInt (FFAUIntSize p (Order (BaseField c))) r c)
       (WitnessField c)))
-> (Bool c, FieldElement c,
    UInt (FFAUIntSize p (Order (BaseField c))) r c)
restore ((Support
    (Bool c, FieldElement c,
     UInt (FFAUIntSize p (Order (BaseField c))) r c)
  -> (c (Layout
           (Bool c, FieldElement c,
            UInt (FFAUIntSize p (Order (BaseField c))) r c)),
      Payload
        (Bool c, FieldElement c,
         UInt (FFAUIntSize p (Order (BaseField c))) r c)
        (WitnessField c)))
 -> (Bool c, FieldElement c,
     UInt (FFAUIntSize p (Order (BaseField c))) r c))
-> (Support
      (Bool c, FieldElement c,
       UInt (FFAUIntSize p (Order (BaseField c))) r c)
    -> (c (Layout
             (Bool c, FieldElement c,
              UInt (FFAUIntSize p (Order (BaseField c))) r c)),
        Payload
          (Bool c, FieldElement c,
           UInt (FFAUIntSize p (Order (BaseField c))) r c)
          (WitnessField c)))
-> (Bool c, FieldElement c,
    UInt (FFAUIntSize p (Order (BaseField c))) r c)
forall a b. (a -> b) -> a -> b
$ (c (Par1
    :*: (Par1
         :*: Vector
               (NumberOfRegisters
                  (BaseField c) (FFAUIntSize p (Order (BaseField c))) r))),
 (:*:) U1 (U1 :*: U1) (WitnessField c))
-> Proxy c
-> (c (Par1
       :*: (Par1
            :*: Vector
                  (NumberOfRegisters
                     (BaseField c) (FFAUIntSize p (Order (BaseField c))) r))),
    (:*:) U1 (U1 :*: U1) (WitnessField c))
forall a b. a -> b -> a
const
        ( c ((Par1
    :*: Layout (UInt (FFAUIntSize p (Order (BaseField c))) r c))
   :*: (Par1
        :*: Layout (UInt (FFAUIntSize p (Order (BaseField c))) r c)))
-> ((:*:)
      (Par1 :*: Layout (UInt (FFAUIntSize p (Order (BaseField c))) r c))
      (Par1 :*: Layout (UInt (FFAUIntSize p (Order (BaseField c))) r c))
      (BaseField c)
    -> (:*:)
         Par1
         (Par1
          :*: Vector
                (NumberOfRegisters
                   (BaseField c) (FFAUIntSize p (Order (BaseField c))) r))
         (BaseField c))
-> CircuitFun
     '[(Par1
        :*: Layout (UInt (FFAUIntSize p (Order (BaseField c))) r c))
       :*: (Par1
            :*: Layout (UInt (FFAUIntSize p (Order (BaseField c))) r c))]
     (Par1
      :*: (Par1
           :*: Vector
                 (NumberOfRegisters
                    (BaseField c) (FFAUIntSize p (Order (BaseField c))) r)))
     c
-> c (Par1
      :*: (Par1
           :*: Vector
                 (NumberOfRegisters
                    (BaseField c) (FFAUIntSize p (Order (BaseField c))) r)))
forall (c :: (Type -> Type) -> Type) a (f :: Type -> Type)
       (g :: Type -> Type).
(Symbolic c, BaseField c ~ a) =>
c f -> (f a -> g a) -> CircuitFun '[f] g c -> c g
symbolicF ((FieldElement c, UInt (FFAUIntSize p (Order (BaseField c))) r c,
 FieldElement c, UInt (FFAUIntSize p (Order (BaseField c))) r c)
-> Support
     (FieldElement c, UInt (FFAUIntSize p (Order (BaseField c))) r c,
      FieldElement c, UInt (FFAUIntSize p (Order (BaseField c))) r c)
-> Context
     (FieldElement c, UInt (FFAUIntSize p (Order (BaseField c))) r c,
      FieldElement c, UInt (FFAUIntSize p (Order (BaseField c))) r c)
     (Layout
        (FieldElement c, UInt (FFAUIntSize p (Order (BaseField c))) r c,
         FieldElement c, UInt (FFAUIntSize p (Order (BaseField c))) r c))
forall x. SymbolicData x => x -> Support x -> Context x (Layout x)
arithmetize (FieldElement c
nx, UInt (FFAUIntSize p (Order (BaseField c))) r c
ux, FieldElement c
ny, UInt (FFAUIntSize p (Order (BaseField c))) r c
uy) Proxy c
Support
  (FieldElement c, UInt (FFAUIntSize p (Order (BaseField c))) r c,
   FieldElement c, UInt (FFAUIntSize p (Order (BaseField c))) r c)
forall {k} (t :: k). Proxy t
Proxy)
            (\((forall (p :: Natural) (r :: RegisterSize) a.
(Arithmetic a, KnownFFA p r (Interpreter a)) =>
(:*:)
  Par1 (Vector (NumberOfRegisters a (FFAUIntSize p (Order a)) r)) a
-> Integer
fromFFA @p @r -> Integer
a) :*: (forall (p :: Natural) (r :: RegisterSize) a.
(Arithmetic a, KnownFFA p r (Interpreter a)) =>
(:*:)
  Par1 (Vector (NumberOfRegisters a (FFAUIntSize p (Order a)) r)) a
-> Integer
fromFFA @p @r -> Integer
b)) ->
              BaseField c -> Par1 (BaseField c)
forall p. p -> Par1 p
Par1 (if Integer
a Integer -> Integer -> Integer
forall a. AdditiveSemigroup a => a -> a -> a
+ Integer
b Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
Prelude.>= Integer
forall a. FromConstant Natural a => a
p then BaseField c
forall a. MultiplicativeMonoid a => a
one else BaseField c
forall a. AdditiveMonoid a => a
zero)
                Par1 (BaseField c)
-> (:*:)
     Par1
     (Vector
        (NumberOfRegisters
           (BaseField c) (FFAUIntSize p (Order (BaseField c))) r))
     (BaseField c)
-> (:*:)
     Par1
     (Par1
      :*: Vector
            (NumberOfRegisters
               (BaseField c) (FFAUIntSize p (Order (BaseField c))) r))
     (BaseField c)
forall k (f :: k -> Type) (g :: k -> Type) (p :: k).
f p -> g p -> (:*:) f g p
:*: forall (p :: Natural) (r :: RegisterSize) a.
(Arithmetic a, KnownFFA p r (Interpreter a)) =>
Integer
-> (:*:)
     Par1 (Vector (NumberOfRegisters a (FFAUIntSize p (Order a)) r)) a
toFFA @p @r ((Integer
a Integer -> Integer -> Integer
forall a. AdditiveSemigroup a => a -> a -> a
+ Integer
b) Integer -> Integer -> Integer
forall a. SemiEuclidean a => a -> a -> a
`mod` Integer
forall a. FromConstant Natural a => a
p)
            )
            \((forall (p :: Natural) (r :: RegisterSize)
       (c :: (Type -> Type) -> Type) i a.
(Symbolic c, KnownFFA p r c, Witness i (WitnessField c),
 a ~ BaseField c) =>
(:*:)
  Par1 (Vector (NumberOfRegisters a (FFAUIntSize p (Order a)) r)) i
-> IntegralOf (WitnessField c)
valueFFA @p @r @c -> IntegralOf (WitnessField c)
a) :*: (forall (p :: Natural) (r :: RegisterSize)
       (c :: (Type -> Type) -> Type) i a.
(Symbolic c, KnownFFA p r c, Witness i (WitnessField c),
 a ~ BaseField c) =>
(:*:)
  Par1 (Vector (NumberOfRegisters a (FFAUIntSize p (Order a)) r)) i
-> IntegralOf (WitnessField c)
valueFFA @p @r @c -> IntegralOf (WitnessField c)
b)) -> do
              (WitnessField c -> m i)
-> (:*:)
     Par1
     (Par1
      :*: Vector
            (NumberOfRegisters
               (BaseField c) (FFAUIntSize p (Order (BaseField c))) r))
     (WitnessField c)
-> m ((:*:)
        Par1
        (Par1
         :*: Vector
               (NumberOfRegisters
                  (BaseField c) (FFAUIntSize p (Order (BaseField c))) r))
        i)
forall (t :: Type -> Type) (f :: Type -> Type) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: Type -> Type) a b.
Applicative f =>
(a -> f b)
-> (:*:)
     Par1
     (Par1
      :*: Vector
            (NumberOfRegisters
               (BaseField c) (FFAUIntSize p (Order (BaseField c))) r))
     a
-> f ((:*:)
        Par1
        (Par1
         :*: Vector
               (NumberOfRegisters
                  (BaseField c) (FFAUIntSize p (Order (BaseField c))) r))
        b)
traverse WitnessField c -> m i
forall var a w (m :: Type -> Type).
MonadCircuit var a w m =>
w -> m var
unconstrained
                  ((:*:)
   Par1
   (Par1
    :*: Vector
          (NumberOfRegisters
             (BaseField c) (FFAUIntSize p (Order (BaseField c))) r))
   (WitnessField c)
 -> m ((:*:)
         Par1
         (Par1
          :*: Vector
                (NumberOfRegisters
                   (BaseField c) (FFAUIntSize p (Order (BaseField c))) r))
         i))
-> (:*:)
     Par1
     (Par1
      :*: Vector
            (NumberOfRegisters
               (BaseField c) (FFAUIntSize p (Order (BaseField c))) r))
     (WitnessField c)
-> m ((:*:)
        Par1
        (Par1
         :*: Vector
               (NumberOfRegisters
                  (BaseField c) (FFAUIntSize p (Order (BaseField c))) r))
        i)
forall a b. (a -> b) -> a -> b
$ WitnessField c -> Par1 (WitnessField c)
forall p. p -> Par1 p
Par1 (IntegralOf (WitnessField c) -> WitnessField c
forall a. ResidueField a => IntegralOf a -> a
fromIntegral ((IntegralOf (WitnessField c)
a IntegralOf (WitnessField c)
-> IntegralOf (WitnessField c) -> IntegralOf (WitnessField c)
forall a. AdditiveSemigroup a => a -> a -> a
+ IntegralOf (WitnessField c)
b) IntegralOf (WitnessField c)
-> IntegralOf (WitnessField c) -> IntegralOf (WitnessField c)
forall a. SemiEuclidean a => a -> a -> a
`div` IntegralOf (WitnessField c)
forall a. FromConstant Natural a => a
p))
                  Par1 (WitnessField c)
-> (:*:)
     Par1
     (Vector
        (NumberOfRegisters
           (BaseField c) (FFAUIntSize p (Order (BaseField c))) r))
     (WitnessField c)
-> (:*:)
     Par1
     (Par1
      :*: Vector
            (NumberOfRegisters
               (BaseField c) (FFAUIntSize p (Order (BaseField c))) r))
     (WitnessField c)
forall k (f :: k -> Type) (g :: k -> Type) (p :: k).
f p -> g p -> (:*:) f g p
:*: forall (p :: Natural) (r :: RegisterSize)
       (c :: (Type -> Type) -> Type) a w.
(Symbolic c, KnownFFA p r c, a ~ BaseField c,
 w ~ WitnessField c) =>
IntegralOf w
-> (:*:)
     Par1 (Vector (NumberOfRegisters a (FFAUIntSize p (Order a)) r)) w
layoutFFA @p @r @c ((IntegralOf (WitnessField c)
a IntegralOf (WitnessField c)
-> IntegralOf (WitnessField c) -> IntegralOf (WitnessField c)
forall a. AdditiveSemigroup a => a -> a -> a
+ IntegralOf (WitnessField c)
b) IntegralOf (WitnessField c)
-> IntegralOf (WitnessField c) -> IntegralOf (WitnessField c)
forall a. SemiEuclidean a => a -> a -> a
`mod` IntegralOf (WitnessField c)
forall a. FromConstant Natural a => a
p)
        , U1 (WitnessField c)
forall k (p :: k). U1 p
U1 U1 (WitnessField c)
-> (:*:) U1 U1 (WitnessField c)
-> (:*:) U1 (U1 :*: U1) (WitnessField c)
forall k (f :: k -> Type) (g :: k -> Type) (p :: k).
f p -> g p -> (:*:) f g p
:*: (U1 (WitnessField c)
forall k (p :: k). U1 p
U1 U1 (WitnessField c)
-> U1 (WitnessField c) -> (:*:) U1 U1 (WitnessField c)
forall k (f :: k -> Type) (g :: k -> Type) (p :: k).
f p -> g p -> (:*:) f g p
:*: U1 (WitnessField c)
forall k (p :: k). U1 p
U1))
      -- | Constraints:
      -- * boolean is indeed boolean;
      -- * UInt registers are indeed registers;
      -- * m < p;
      -- * equation holds modulo basefield;
      -- * equation holds modulo 2^k.
      Bool c Par1
ck = (Bool c, FFA p r c) -> Bool (Context (Bool c, FFA p r c))
forall d. SymbolicInput d => d -> Bool (Context d)
isValid (Bool c
d, forall (p :: Natural) (r :: RegisterSize)
       (c :: (Type -> Type) -> Type).
FieldElement c -> UIntFFA p r c -> FFA p r c
FFA @p FieldElement c
nm UInt (FFAUIntSize p (Order (BaseField c))) r c
um)
                Bool c -> Bool c -> Bool c
forall b. BoolType b => b -> b -> b
&& (FieldElement c
nx FieldElement c -> FieldElement c -> FieldElement c
forall a. AdditiveSemigroup a => a -> a -> a
+ FieldElement c
ny FieldElement c -> FieldElement c -> BooleanOf (FieldElement c)
forall a. Eq a => a -> a -> BooleanOf a
== FieldElement c -> FieldElement c -> Bool c -> FieldElement c
forall b a. Conditional b a => a -> a -> b -> a
bool FieldElement c
forall a. AdditiveMonoid a => a
zero FieldElement c
forall a. FromConstant Natural a => a
p Bool c
d FieldElement c -> FieldElement c -> FieldElement c
forall a. AdditiveSemigroup a => a -> a -> a
+ FieldElement c
nm)
                Bool c -> Bool c -> Bool c
forall b. BoolType b => b -> b -> b
&& (UInt (FFAUIntSize p (Order (BaseField c))) r c
ux UInt (FFAUIntSize p (Order (BaseField c))) r c
-> UInt (FFAUIntSize p (Order (BaseField c))) r c
-> UInt (FFAUIntSize p (Order (BaseField c))) r c
forall a. AdditiveSemigroup a => a -> a -> a
+ UInt (FFAUIntSize p (Order (BaseField c))) r c
uy UInt (FFAUIntSize p (Order (BaseField c))) r c
-> UInt (FFAUIntSize p (Order (BaseField c))) r c
-> BooleanOf (UInt (FFAUIntSize p (Order (BaseField c))) r c)
forall a. Eq a => a -> a -> BooleanOf a
== UInt (FFAUIntSize p (Order (BaseField c))) r c
-> UInt (FFAUIntSize p (Order (BaseField c))) r c
-> Bool c
-> UInt (FFAUIntSize p (Order (BaseField c))) r c
forall b a. Conditional b a => a -> a -> b -> a
bool UInt (FFAUIntSize p (Order (BaseField c))) r c
forall a. AdditiveMonoid a => a
zero UInt (FFAUIntSize p (Order (BaseField c))) r c
forall a. FromConstant Natural a => a
p Bool c
d UInt (FFAUIntSize p (Order (BaseField c))) r c
-> UInt (FFAUIntSize p (Order (BaseField c))) r c
-> UInt (FFAUIntSize p (Order (BaseField c))) r c
forall a. AdditiveSemigroup a => a -> a -> a
+ UInt (FFAUIntSize p (Order (BaseField c))) r c
um)
      -- | Sew constraints into result.
      (FieldElement c
nr, UInt (FFAUIntSize p (Order (BaseField c))) r c
ur) = (Support
   (FieldElement c, UInt (FFAUIntSize p (Order (BaseField c))) r c)
 -> (c (Layout
          (FieldElement c, UInt (FFAUIntSize p (Order (BaseField c))) r c)),
     Payload
       (FieldElement c, UInt (FFAUIntSize p (Order (BaseField c))) r c)
       (WitnessField c)))
-> (FieldElement c, UInt (FFAUIntSize p (Order (BaseField c))) r c)
forall x (c :: (Type -> Type) -> Type).
(SymbolicData x, Context x ~ c) =>
(Support x -> (c (Layout x), Payload x (WitnessField c))) -> x
forall (c :: (Type -> Type) -> Type).
(Context
   (FieldElement c, UInt (FFAUIntSize p (Order (BaseField c))) r c)
 ~ c) =>
(Support
   (FieldElement c, UInt (FFAUIntSize p (Order (BaseField c))) r c)
 -> (c (Layout
          (FieldElement c, UInt (FFAUIntSize p (Order (BaseField c))) r c)),
     Payload
       (FieldElement c, UInt (FFAUIntSize p (Order (BaseField c))) r c)
       (WitnessField c)))
-> (FieldElement c, UInt (FFAUIntSize p (Order (BaseField c))) r c)
restore ((Support
    (FieldElement c, UInt (FFAUIntSize p (Order (BaseField c))) r c)
  -> (c (Layout
           (FieldElement c, UInt (FFAUIntSize p (Order (BaseField c))) r c)),
      Payload
        (FieldElement c, UInt (FFAUIntSize p (Order (BaseField c))) r c)
        (WitnessField c)))
 -> (FieldElement c,
     UInt (FFAUIntSize p (Order (BaseField c))) r c))
-> (Support
      (FieldElement c, UInt (FFAUIntSize p (Order (BaseField c))) r c)
    -> (c (Layout
             (FieldElement c, UInt (FFAUIntSize p (Order (BaseField c))) r c)),
        Payload
          (FieldElement c, UInt (FFAUIntSize p (Order (BaseField c))) r c)
          (WitnessField c)))
-> (FieldElement c, UInt (FFAUIntSize p (Order (BaseField c))) r c)
forall a b. (a -> b) -> a -> b
$ (c (Par1
    :*: Layout (UInt (FFAUIntSize p (Order (BaseField c))) r c)),
 (:*:) U1 U1 (WitnessField c))
-> Proxy c
-> (c (Par1
       :*: Layout (UInt (FFAUIntSize p (Order (BaseField c))) r c)),
    (:*:) U1 U1 (WitnessField c))
forall a b. a -> b -> a
const
        ( c (Par1
   :*: (Layout (UInt (FFAUIntSize p (Order (BaseField c))) r c)
        :*: Par1))
-> CircuitFun
     '[Par1
       :*: (Layout (UInt (FFAUIntSize p (Order (BaseField c))) r c)
            :*: Par1)]
     (Par1 :*: Layout (UInt (FFAUIntSize p (Order (BaseField c))) r c))
     c
-> c (Par1
      :*: Layout (UInt (FFAUIntSize p (Order (BaseField c))) r c))
forall (f :: Type -> Type) (g :: Type -> Type).
c f -> CircuitFun '[f] g c -> c g
forall (c :: (Type -> Type) -> Type) (f :: Type -> Type)
       (g :: Type -> Type).
Symbolic c =>
c f -> CircuitFun '[f] g c -> c g
fromCircuitF ((FieldElement c, UInt (FFAUIntSize p (Order (BaseField c))) r c,
 c Par1)
-> Support
     (FieldElement c, UInt (FFAUIntSize p (Order (BaseField c))) r c,
      c Par1)
-> Context
     (FieldElement c, UInt (FFAUIntSize p (Order (BaseField c))) r c,
      c Par1)
     (Layout
        (FieldElement c, UInt (FFAUIntSize p (Order (BaseField c))) r c,
         c Par1))
forall x. SymbolicData x => x -> Support x -> Context x (Layout x)
arithmetize (FieldElement c
nm, UInt (FFAUIntSize p (Order (BaseField c))) r c
um, c Par1
ck) Proxy c
Support
  (FieldElement c, UInt (FFAUIntSize p (Order (BaseField c))) r c,
   c Par1)
forall {k} (t :: k). Proxy t
Proxy)
            \(Par1 i
ni :*: Vector
  (NumberOfRegisters
     (BaseField c) (FFAUIntSize p (Order (BaseField c))) r)
  i
ui :*: Par1 i
b) -> do
              ClosedPoly i (BaseField c) -> m ()
forall var a w (m :: Type -> Type).
MonadCircuit var a w m =>
ClosedPoly var a -> m ()
constraint (((i -> x) -> i -> x
forall a b. (a -> b) -> a -> b
$ i
b) ((i -> x) -> x) -> ((i -> x) -> x) -> (i -> x) -> x
forall a. AdditiveGroup a => a -> a -> a
- (i -> x) -> x
forall a. MultiplicativeMonoid a => a
one)
              (:*:)
  Par1
  (Vector
     (NumberOfRegisters
        (BaseField c) (FFAUIntSize p (Order (BaseField c))) r))
  i
-> m ((:*:)
        Par1
        (Vector
           (NumberOfRegisters
              (BaseField c) (FFAUIntSize p (Order (BaseField c))) r))
        i)
forall a. a -> m a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Par1 i
ni Par1 i
-> Vector
     (NumberOfRegisters
        (BaseField c) (FFAUIntSize p (Order (BaseField c))) r)
     i
-> (:*:)
     Par1
     (Vector
        (NumberOfRegisters
           (BaseField c) (FFAUIntSize p (Order (BaseField c))) r))
     i
forall k (f :: k -> Type) (g :: k -> Type) (p :: k).
f p -> g p -> (:*:) f g p
:*: Vector
  (NumberOfRegisters
     (BaseField c) (FFAUIntSize p (Order (BaseField c))) r)
  i
ui)
        , U1 (WitnessField c)
forall k (p :: k). U1 p
U1 U1 (WitnessField c)
-> U1 (WitnessField c) -> (:*:) U1 U1 (WitnessField c)
forall k (f :: k -> Type) (g :: k -> Type) (p :: k).
f p -> g p -> (:*:) f g p
:*: U1 (WitnessField c)
forall k (p :: k). U1 p
U1)

instance (Symbolic c, KnownFFA p r c, Scale a (Zp p)) => Scale a (FFA p r c) where
  scale :: a -> FFA p r c -> FFA p r c
scale a
k FFA p r c
x = Zp p -> FFA p r c
forall a b. FromConstant a b => a -> b
fromConstant (a -> Zp p -> Zp p
forall b a. Scale b a => b -> a -> a
scale a
k Zp p
forall a. MultiplicativeMonoid a => a
one :: Zp p) FFA p r c -> FFA p r c -> FFA p r c
forall a. MultiplicativeSemigroup a => a -> a -> a
* FFA p r c
x

instance (Symbolic c, KnownFFA p r c) => AdditiveMonoid (FFA p r c) where
  zero :: FFA p r c
zero = Zp p -> FFA p r c
forall a b. FromConstant a b => a -> b
fromConstant (Zp p
forall a. AdditiveMonoid a => a
zero :: Zp p)

instance (Symbolic c, KnownFFA p r c) => AdditiveGroup (FFA p r c) where
  -- | negate cannot overflow if value is nonzero.
  negate :: FFA p r c -> FFA p r c
negate (FFA FieldElement c
nx UInt (FFAUIntSize p (Order (BaseField c))) r c
ux) = FFA p r c -> FFA p r c -> Bool c -> FFA p r c
forall b a. Conditional b a => a -> a -> b -> a
bool
    (FieldElement c
-> UInt (FFAUIntSize p (Order (BaseField c))) r c -> FFA p r c
forall (p :: Natural) (r :: RegisterSize)
       (c :: (Type -> Type) -> Type).
FieldElement c -> UIntFFA p r c -> FFA p r c
FFA (Natural -> FieldElement c
forall a b. FromConstant a b => a -> b
fromConstant (forall (n :: Natural). KnownNat n => Natural
value @p) FieldElement c -> FieldElement c -> FieldElement c
forall a. AdditiveGroup a => a -> a -> a
- FieldElement c
nx) (Natural -> UInt (FFAUIntSize p (Order (BaseField c))) r c
forall a b. FromConstant a b => a -> b
fromConstant (forall (n :: Natural). KnownNat n => Natural
value @p) UInt (FFAUIntSize p (Order (BaseField c))) r c
-> UInt (FFAUIntSize p (Order (BaseField c))) r c
-> UInt (FFAUIntSize p (Order (BaseField c))) r c
forall a. AdditiveGroup a => a -> a -> a
- UInt (FFAUIntSize p (Order (BaseField c))) r c
ux))
    (FieldElement c
-> UInt (FFAUIntSize p (Order (BaseField c))) r c -> FFA p r c
forall (p :: Natural) (r :: RegisterSize)
       (c :: (Type -> Type) -> Type).
FieldElement c -> UIntFFA p r c -> FFA p r c
FFA FieldElement c
nx UInt (FFAUIntSize p (Order (BaseField c))) r c
ux)
    (FieldElement c
nx FieldElement c -> FieldElement c -> BooleanOf (FieldElement c)
forall a. Eq a => a -> a -> BooleanOf a
== FieldElement c
forall a. AdditiveMonoid a => a
zero Bool c -> Bool c -> Bool c
forall b. BoolType b => b -> b -> b
&& UInt (FFAUIntSize p (Order (BaseField c))) r c
ux UInt (FFAUIntSize p (Order (BaseField c))) r c
-> UInt (FFAUIntSize p (Order (BaseField c))) r c
-> BooleanOf (UInt (FFAUIntSize p (Order (BaseField c))) r c)
forall a. Eq a => a -> a -> BooleanOf a
== UInt (FFAUIntSize p (Order (BaseField c))) r c
forall a. AdditiveMonoid a => a
zero)

instance (Symbolic c, KnownFFA p r c) => Semiring (FFA p r c)

instance (Symbolic c, KnownFFA p r c) => Ring (FFA p r c)

instance (Symbolic c, KnownFFA p r c, Prime p) => Exponent (FFA p r c) Integer where
  FFA p r c
x ^ :: FFA p r c -> Integer -> FFA p r c
^ Integer
a
    | Natural
neg Natural -> Natural -> Bool
forall a. Ord a => a -> a -> Bool
Prelude.< Natural
pos = FFA p r c -> FFA p r c
forall a. Field a => a -> a
finv FFA p r c
x FFA p r c -> Natural -> FFA p r c
forall a b. Exponent a b => a -> b -> a
^ Natural
neg
    | Bool
otherwise = FFA p r c
x FFA p r c -> Natural -> FFA p r c
forall a b. Exponent a b => a -> b -> a
^ Natural
pos
    where
      pos :: Natural
pos = Integer -> Natural
forall a b. (Integral a, Num b) => a -> b
Prelude.fromIntegral (Integer
a Integer -> Integer -> Integer
forall a. SemiEuclidean a => a -> a -> a
`mod` Natural -> Integer
forall a b. (Integral a, Num b) => a -> b
Prelude.fromIntegral (forall (n :: Natural). KnownNat n => Natural
value @p Natural -> Natural -> Natural
-! Natural
1))
      neg :: Natural
neg = forall (n :: Natural). KnownNat n => Natural
value @p Natural -> Natural -> Natural
-! (Natural
pos Natural -> Natural -> Natural
forall a. AdditiveSemigroup a => a -> a -> a
+ Natural
1)

instance (Symbolic c, KnownFFA p r c, Prime p) => Field (FFA p r c) where
  finv :: FFA p r c -> FFA p r c
finv (FFA FieldElement c
nx UInt (FFAUIntSize p (Order (BaseField c))) r c
ux) = FieldElement c
-> UInt (FFAUIntSize p (Order (BaseField c))) r c -> FFA p r c
forall (p :: Natural) (r :: RegisterSize)
       (c :: (Type -> Type) -> Type).
FieldElement c -> UIntFFA p r c -> FFA p r c
FFA FieldElement c
ny UInt (FFAUIntSize p (Order (BaseField c))) r c
uy
    where
      p :: FromConstant Natural a => a
      p :: forall a. FromConstant Natural a => a
p = Natural -> a
forall a b. FromConstant a b => a -> b
fromConstant (forall (n :: Natural). KnownNat n => Natural
value @p)
      -- | Computes unconstrained Bezout coefficients.
      nl, nr :: FieldElement c
      ul, ur :: UIntFFA p r c
      (FieldElement c
nl, UInt (FFAUIntSize p (Order (BaseField c))) r c
ul, FieldElement c
nr, UInt (FFAUIntSize p (Order (BaseField c))) r c
ur) = (Support
   (FieldElement c, UInt (FFAUIntSize p (Order (BaseField c))) r c,
    FieldElement c, UInt (FFAUIntSize p (Order (BaseField c))) r c)
 -> (c (Layout
          (FieldElement c, UInt (FFAUIntSize p (Order (BaseField c))) r c,
           FieldElement c, UInt (FFAUIntSize p (Order (BaseField c))) r c)),
     Payload
       (FieldElement c, UInt (FFAUIntSize p (Order (BaseField c))) r c,
        FieldElement c, UInt (FFAUIntSize p (Order (BaseField c))) r c)
       (WitnessField c)))
-> (FieldElement c, UInt (FFAUIntSize p (Order (BaseField c))) r c,
    FieldElement c, UInt (FFAUIntSize p (Order (BaseField c))) r c)
forall x (c :: (Type -> Type) -> Type).
(SymbolicData x, Context x ~ c) =>
(Support x -> (c (Layout x), Payload x (WitnessField c))) -> x
forall (c :: (Type -> Type) -> Type).
(Context
   (FieldElement c, UInt (FFAUIntSize p (Order (BaseField c))) r c,
    FieldElement c, UInt (FFAUIntSize p (Order (BaseField c))) r c)
 ~ c) =>
(Support
   (FieldElement c, UInt (FFAUIntSize p (Order (BaseField c))) r c,
    FieldElement c, UInt (FFAUIntSize p (Order (BaseField c))) r c)
 -> (c (Layout
          (FieldElement c, UInt (FFAUIntSize p (Order (BaseField c))) r c,
           FieldElement c, UInt (FFAUIntSize p (Order (BaseField c))) r c)),
     Payload
       (FieldElement c, UInt (FFAUIntSize p (Order (BaseField c))) r c,
        FieldElement c, UInt (FFAUIntSize p (Order (BaseField c))) r c)
       (WitnessField c)))
-> (FieldElement c, UInt (FFAUIntSize p (Order (BaseField c))) r c,
    FieldElement c, UInt (FFAUIntSize p (Order (BaseField c))) r c)
restore ((Support
    (FieldElement c, UInt (FFAUIntSize p (Order (BaseField c))) r c,
     FieldElement c, UInt (FFAUIntSize p (Order (BaseField c))) r c)
  -> (c (Layout
           (FieldElement c, UInt (FFAUIntSize p (Order (BaseField c))) r c,
            FieldElement c, UInt (FFAUIntSize p (Order (BaseField c))) r c)),
      Payload
        (FieldElement c, UInt (FFAUIntSize p (Order (BaseField c))) r c,
         FieldElement c, UInt (FFAUIntSize p (Order (BaseField c))) r c)
        (WitnessField c)))
 -> (FieldElement c, UInt (FFAUIntSize p (Order (BaseField c))) r c,
     FieldElement c, UInt (FFAUIntSize p (Order (BaseField c))) r c))
-> (Support
      (FieldElement c, UInt (FFAUIntSize p (Order (BaseField c))) r c,
       FieldElement c, UInt (FFAUIntSize p (Order (BaseField c))) r c)
    -> (c (Layout
             (FieldElement c, UInt (FFAUIntSize p (Order (BaseField c))) r c,
              FieldElement c, UInt (FFAUIntSize p (Order (BaseField c))) r c)),
        Payload
          (FieldElement c, UInt (FFAUIntSize p (Order (BaseField c))) r c,
           FieldElement c, UInt (FFAUIntSize p (Order (BaseField c))) r c)
          (WitnessField c)))
-> (FieldElement c, UInt (FFAUIntSize p (Order (BaseField c))) r c,
    FieldElement c, UInt (FFAUIntSize p (Order (BaseField c))) r c)
forall a b. (a -> b) -> a -> b
$ (c ((Par1
     :*: Vector
           (NumberOfRegisters
              (BaseField c) (FFAUIntSize p (Order (BaseField c))) r))
    :*: (Par1
         :*: Vector
               (NumberOfRegisters
                  (BaseField c) (FFAUIntSize p (Order (BaseField c))) r))),
 (:*:) (U1 :*: U1) (U1 :*: U1) (WitnessField c))
-> Proxy c
-> (c ((Par1
        :*: Vector
              (NumberOfRegisters
                 (BaseField c) (FFAUIntSize p (Order (BaseField c))) r))
       :*: (Par1
            :*: Vector
                  (NumberOfRegisters
                     (BaseField c) (FFAUIntSize p (Order (BaseField c))) r))),
    (:*:) (U1 :*: U1) (U1 :*: U1) (WitnessField c))
forall a b. a -> b -> a
const
        ( c (Par1
   :*: Layout (UInt (FFAUIntSize p (Order (BaseField c))) r c))
-> ((:*:)
      Par1
      (Layout (UInt (FFAUIntSize p (Order (BaseField c))) r c))
      (BaseField c)
    -> (:*:)
         (Par1
          :*: Vector
                (NumberOfRegisters
                   (BaseField c) (FFAUIntSize p (Order (BaseField c))) r))
         (Par1
          :*: Vector
                (NumberOfRegisters
                   (BaseField c) (FFAUIntSize p (Order (BaseField c))) r))
         (BaseField c))
-> CircuitFun
     '[Par1 :*: Layout (UInt (FFAUIntSize p (Order (BaseField c))) r c)]
     ((Par1
       :*: Vector
             (NumberOfRegisters
                (BaseField c) (FFAUIntSize p (Order (BaseField c))) r))
      :*: (Par1
           :*: Vector
                 (NumberOfRegisters
                    (BaseField c) (FFAUIntSize p (Order (BaseField c))) r)))
     c
-> c ((Par1
       :*: Vector
             (NumberOfRegisters
                (BaseField c) (FFAUIntSize p (Order (BaseField c))) r))
      :*: (Par1
           :*: Vector
                 (NumberOfRegisters
                    (BaseField c) (FFAUIntSize p (Order (BaseField c))) r)))
forall (c :: (Type -> Type) -> Type) a (f :: Type -> Type)
       (g :: Type -> Type).
(Symbolic c, BaseField c ~ a) =>
c f -> (f a -> g a) -> CircuitFun '[f] g c -> c g
symbolicF ((FieldElement c, UInt (FFAUIntSize p (Order (BaseField c))) r c)
-> Support
     (FieldElement c, UInt (FFAUIntSize p (Order (BaseField c))) r c)
-> Context
     (FieldElement c, UInt (FFAUIntSize p (Order (BaseField c))) r c)
     (Layout
        (FieldElement c, UInt (FFAUIntSize p (Order (BaseField c))) r c))
forall x. SymbolicData x => x -> Support x -> Context x (Layout x)
arithmetize (FieldElement c
nx, UInt (FFAUIntSize p (Order (BaseField c))) r c
ux) Proxy c
Support
  (FieldElement c, UInt (FFAUIntSize p (Order (BaseField c))) r c)
forall {k} (t :: k). Proxy t
Proxy)
            (\(forall (p :: Natural) (r :: RegisterSize) a.
(Arithmetic a, KnownFFA p r (Interpreter a)) =>
(:*:)
  Par1 (Vector (NumberOfRegisters a (FFAUIntSize p (Order a)) r)) a
-> Integer
fromFFA @p @r -> Integer
x) ->
              let l0 :: Integer
l0 = Integer -> Integer
forall a. AdditiveGroup a => a -> a
negate (Integer -> Integer -> Integer
forall a. Euclidean a => a -> a -> a
bezoutL Integer
forall a. FromConstant Natural a => a
p Integer
x)
                  r0 :: Integer
r0 = Integer -> Integer -> Integer
forall a. Euclidean a => a -> a -> a
bezoutR Integer
forall a. FromConstant Natural a => a
p Integer
x
                  (Integer
l, Integer
r) = if Integer
r0 Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
Prelude.< Integer
0 then (Integer
l0 Integer -> Integer -> Integer
forall a. AdditiveSemigroup a => a -> a -> a
+ Integer
x, Integer
r0 Integer -> Integer -> Integer
forall a. AdditiveSemigroup a => a -> a -> a
+ Integer
forall a. FromConstant Natural a => a
p) else (Integer
l0, Integer
r0)
               in forall (p :: Natural) (r :: RegisterSize) a.
(Arithmetic a, KnownFFA p r (Interpreter a)) =>
Integer
-> (:*:)
     Par1 (Vector (NumberOfRegisters a (FFAUIntSize p (Order a)) r)) a
toFFA @p @r Integer
l (:*:)
  Par1
  (Vector
     (NumberOfRegisters
        (BaseField c) (FFAUIntSize p (Order (BaseField c))) r))
  (BaseField c)
-> (:*:)
     Par1
     (Vector
        (NumberOfRegisters
           (BaseField c) (FFAUIntSize p (Order (BaseField c))) r))
     (BaseField c)
-> (:*:)
     (Par1
      :*: Vector
            (NumberOfRegisters
               (BaseField c) (FFAUIntSize p (Order (BaseField c))) r))
     (Par1
      :*: Vector
            (NumberOfRegisters
               (BaseField c) (FFAUIntSize p (Order (BaseField c))) r))
     (BaseField c)
forall k (f :: k -> Type) (g :: k -> Type) (p :: k).
f p -> g p -> (:*:) f g p
:*: forall (p :: Natural) (r :: RegisterSize) a.
(Arithmetic a, KnownFFA p r (Interpreter a)) =>
Integer
-> (:*:)
     Par1 (Vector (NumberOfRegisters a (FFAUIntSize p (Order a)) r)) a
toFFA @p @r Integer
r
            )
            \(forall (p :: Natural) (r :: RegisterSize)
       (c :: (Type -> Type) -> Type) i a.
(Symbolic c, KnownFFA p r c, Witness i (WitnessField c),
 a ~ BaseField c) =>
(:*:)
  Par1 (Vector (NumberOfRegisters a (FFAUIntSize p (Order a)) r)) i
-> IntegralOf (WitnessField c)
valueFFA @p @r @c -> IntegralOf (WitnessField c)
x) -> do
              let l0 :: IntegralOf (WitnessField c)
l0 = IntegralOf (WitnessField c) -> IntegralOf (WitnessField c)
forall a. AdditiveGroup a => a -> a
negate (IntegralOf (WitnessField c)
-> IntegralOf (WitnessField c) -> IntegralOf (WitnessField c)
forall a. Euclidean a => a -> a -> a
bezoutL IntegralOf (WitnessField c)
forall a. FromConstant Natural a => a
p IntegralOf (WitnessField c)
x)
                  r0 :: IntegralOf (WitnessField c)
r0 = IntegralOf (WitnessField c)
-> IntegralOf (WitnessField c) -> IntegralOf (WitnessField c)
forall a. Euclidean a => a -> a -> a
bezoutR IntegralOf (WitnessField c)
forall a. FromConstant Natural a => a
p IntegralOf (WitnessField c)
x
                  s :: IntegralOf (WitnessField c)
s  = IntegralOf (WitnessField c)
r0 IntegralOf (WitnessField c)
-> IntegralOf (WitnessField c) -> IntegralOf (WitnessField c)
forall a. SemiEuclidean a => a -> a -> a
`div` IntegralOf (WitnessField c)
forall a. FromConstant Natural a => a
p -- -1 when negative, 0 when positive
                  l :: IntegralOf (WitnessField c)
l  = IntegralOf (WitnessField c)
l0 IntegralOf (WitnessField c)
-> IntegralOf (WitnessField c) -> IntegralOf (WitnessField c)
forall a. AdditiveGroup a => a -> a -> a
- IntegralOf (WitnessField c)
s IntegralOf (WitnessField c)
-> IntegralOf (WitnessField c) -> IntegralOf (WitnessField c)
forall a. MultiplicativeSemigroup a => a -> a -> a
* IntegralOf (WitnessField c)
x
                  r :: IntegralOf (WitnessField c)
r  = IntegralOf (WitnessField c)
r0 IntegralOf (WitnessField c)
-> IntegralOf (WitnessField c) -> IntegralOf (WitnessField c)
forall a. AdditiveGroup a => a -> a -> a
- IntegralOf (WitnessField c)
s IntegralOf (WitnessField c)
-> IntegralOf (WitnessField c) -> IntegralOf (WitnessField c)
forall a. MultiplicativeSemigroup a => a -> a -> a
* IntegralOf (WitnessField c)
forall a. FromConstant Natural a => a
p
              (WitnessField c -> m i)
-> (:*:)
     (Par1
      :*: Vector
            (NumberOfRegisters
               (BaseField c) (FFAUIntSize p (Order (BaseField c))) r))
     (Par1
      :*: Vector
            (NumberOfRegisters
               (BaseField c) (FFAUIntSize p (Order (BaseField c))) r))
     (WitnessField c)
-> m ((:*:)
        (Par1
         :*: Vector
               (NumberOfRegisters
                  (BaseField c) (FFAUIntSize p (Order (BaseField c))) r))
        (Par1
         :*: Vector
               (NumberOfRegisters
                  (BaseField c) (FFAUIntSize p (Order (BaseField c))) r))
        i)
forall (t :: Type -> Type) (f :: Type -> Type) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: Type -> Type) a b.
Applicative f =>
(a -> f b)
-> (:*:)
     (Par1
      :*: Vector
            (NumberOfRegisters
               (BaseField c) (FFAUIntSize p (Order (BaseField c))) r))
     (Par1
      :*: Vector
            (NumberOfRegisters
               (BaseField c) (FFAUIntSize p (Order (BaseField c))) r))
     a
-> f ((:*:)
        (Par1
         :*: Vector
               (NumberOfRegisters
                  (BaseField c) (FFAUIntSize p (Order (BaseField c))) r))
        (Par1
         :*: Vector
               (NumberOfRegisters
                  (BaseField c) (FFAUIntSize p (Order (BaseField c))) r))
        b)
traverse WitnessField c -> m i
forall var a w (m :: Type -> Type).
MonadCircuit var a w m =>
w -> m var
unconstrained ((:*:)
   (Par1
    :*: Vector
          (NumberOfRegisters
             (BaseField c) (FFAUIntSize p (Order (BaseField c))) r))
   (Par1
    :*: Vector
          (NumberOfRegisters
             (BaseField c) (FFAUIntSize p (Order (BaseField c))) r))
   (WitnessField c)
 -> m ((:*:)
         (Par1
          :*: Vector
                (NumberOfRegisters
                   (BaseField c) (FFAUIntSize p (Order (BaseField c))) r))
         (Par1
          :*: Vector
                (NumberOfRegisters
                   (BaseField c) (FFAUIntSize p (Order (BaseField c))) r))
         i))
-> (:*:)
     (Par1
      :*: Vector
            (NumberOfRegisters
               (BaseField c) (FFAUIntSize p (Order (BaseField c))) r))
     (Par1
      :*: Vector
            (NumberOfRegisters
               (BaseField c) (FFAUIntSize p (Order (BaseField c))) r))
     (WitnessField c)
-> m ((:*:)
        (Par1
         :*: Vector
               (NumberOfRegisters
                  (BaseField c) (FFAUIntSize p (Order (BaseField c))) r))
        (Par1
         :*: Vector
               (NumberOfRegisters
                  (BaseField c) (FFAUIntSize p (Order (BaseField c))) r))
        i)
forall a b. (a -> b) -> a -> b
$
                forall (p :: Natural) (r :: RegisterSize)
       (c :: (Type -> Type) -> Type) a w.
(Symbolic c, KnownFFA p r c, a ~ BaseField c,
 w ~ WitnessField c) =>
IntegralOf w
-> (:*:)
     Par1 (Vector (NumberOfRegisters a (FFAUIntSize p (Order a)) r)) w
layoutFFA @p @r @c IntegralOf (WitnessField c)
l (:*:)
  Par1
  (Vector
     (NumberOfRegisters
        (BaseField c) (FFAUIntSize p (Order (BaseField c))) r))
  (WitnessField c)
-> (:*:)
     Par1
     (Vector
        (NumberOfRegisters
           (BaseField c) (FFAUIntSize p (Order (BaseField c))) r))
     (WitnessField c)
-> (:*:)
     (Par1
      :*: Vector
            (NumberOfRegisters
               (BaseField c) (FFAUIntSize p (Order (BaseField c))) r))
     (Par1
      :*: Vector
            (NumberOfRegisters
               (BaseField c) (FFAUIntSize p (Order (BaseField c))) r))
     (WitnessField c)
forall k (f :: k -> Type) (g :: k -> Type) (p :: k).
f p -> g p -> (:*:) f g p
:*: forall (p :: Natural) (r :: RegisterSize)
       (c :: (Type -> Type) -> Type) a w.
(Symbolic c, KnownFFA p r c, a ~ BaseField c,
 w ~ WitnessField c) =>
IntegralOf w
-> (:*:)
     Par1 (Vector (NumberOfRegisters a (FFAUIntSize p (Order a)) r)) w
layoutFFA @p @r @c IntegralOf (WitnessField c)
r
        , (U1 (WitnessField c)
forall k (p :: k). U1 p
U1 U1 (WitnessField c)
-> U1 (WitnessField c) -> (:*:) U1 U1 (WitnessField c)
forall k (f :: k -> Type) (g :: k -> Type) (p :: k).
f p -> g p -> (:*:) f g p
:*: U1 (WitnessField c)
forall k (p :: k). U1 p
U1) (:*:) U1 U1 (WitnessField c)
-> (:*:) U1 U1 (WitnessField c)
-> (:*:) (U1 :*: U1) (U1 :*: U1) (WitnessField c)
forall k (f :: k -> Type) (g :: k -> Type) (p :: k).
f p -> g p -> (:*:) f g p
:*: (U1 (WitnessField c)
forall k (p :: k). U1 p
U1 U1 (WitnessField c)
-> U1 (WitnessField c) -> (:*:) U1 U1 (WitnessField c)
forall k (f :: k -> Type) (g :: k -> Type) (p :: k).
f p -> g p -> (:*:) f g p
:*: U1 (WitnessField c)
forall k (p :: k). U1 p
U1))
      -- | Constraints:
      -- * UInt registers are indeed registers;
      -- * r < p;
      -- * equation holds modulo basefield;
      -- * equation holds modulo 2^k.
      Bool Context (UInt (FFAUIntSize p (Order (BaseField c))) r c) Par1
ck = (UInt (FFAUIntSize p (Order (BaseField c))) r c, FFA p r c)
-> Bool
     (Context
        (UInt (FFAUIntSize p (Order (BaseField c))) r c, FFA p r c))
forall d. SymbolicInput d => d -> Bool (Context d)
isValid (UInt (FFAUIntSize p (Order (BaseField c))) r c
ur, forall (p :: Natural) (r :: RegisterSize)
       (c :: (Type -> Type) -> Type).
FieldElement c -> UIntFFA p r c -> FFA p r c
FFA @p FieldElement c
nl UInt (FFAUIntSize p (Order (BaseField c))) r c
ul)
                Bool (Context (UInt (FFAUIntSize p (Order (BaseField c))) r c))
-> Bool (Context (UInt (FFAUIntSize p (Order (BaseField c))) r c))
-> Bool (Context (UInt (FFAUIntSize p (Order (BaseField c))) r c))
forall b. BoolType b => b -> b -> b
&& (FieldElement c
nr FieldElement c -> FieldElement c -> FieldElement c
forall a. MultiplicativeSemigroup a => a -> a -> a
* FieldElement c
nx FieldElement c -> FieldElement c -> BooleanOf (FieldElement c)
forall a. Eq a => a -> a -> BooleanOf a
== FieldElement c
nl FieldElement c -> FieldElement c -> FieldElement c
forall a. MultiplicativeSemigroup a => a -> a -> a
* FieldElement c
forall a. FromConstant Natural a => a
p FieldElement c -> FieldElement c -> FieldElement c
forall a. AdditiveSemigroup a => a -> a -> a
+ FieldElement c
forall a. MultiplicativeMonoid a => a
one)
                Bool (Context (UInt (FFAUIntSize p (Order (BaseField c))) r c))
-> Bool (Context (UInt (FFAUIntSize p (Order (BaseField c))) r c))
-> Bool (Context (UInt (FFAUIntSize p (Order (BaseField c))) r c))
forall b. BoolType b => b -> b -> b
&& (UInt (FFAUIntSize p (Order (BaseField c))) r c
ur UInt (FFAUIntSize p (Order (BaseField c))) r c
-> UInt (FFAUIntSize p (Order (BaseField c))) r c
-> UInt (FFAUIntSize p (Order (BaseField c))) r c
forall a. MultiplicativeSemigroup a => a -> a -> a
* UInt (FFAUIntSize p (Order (BaseField c))) r c
ux UInt (FFAUIntSize p (Order (BaseField c))) r c
-> UInt (FFAUIntSize p (Order (BaseField c))) r c
-> BooleanOf (UInt (FFAUIntSize p (Order (BaseField c))) r c)
forall a. Eq a => a -> a -> BooleanOf a
== UInt (FFAUIntSize p (Order (BaseField c))) r c
ul UInt (FFAUIntSize p (Order (BaseField c))) r c
-> UInt (FFAUIntSize p (Order (BaseField c))) r c
-> UInt (FFAUIntSize p (Order (BaseField c))) r c
forall a. MultiplicativeSemigroup a => a -> a -> a
* UInt (FFAUIntSize p (Order (BaseField c))) r c
forall a. FromConstant Natural a => a
p UInt (FFAUIntSize p (Order (BaseField c))) r c
-> UInt (FFAUIntSize p (Order (BaseField c))) r c
-> UInt (FFAUIntSize p (Order (BaseField c))) r c
forall a. AdditiveSemigroup a => a -> a -> a
+ UInt (FFAUIntSize p (Order (BaseField c))) r c
forall a. MultiplicativeMonoid a => a
one)
      -- | Sew constraints into result.
      (FieldElement c
ny, UInt (FFAUIntSize p (Order (BaseField c))) r c
uy) = (Support
   (FieldElement c, UInt (FFAUIntSize p (Order (BaseField c))) r c)
 -> (c (Layout
          (FieldElement c, UInt (FFAUIntSize p (Order (BaseField c))) r c)),
     Payload
       (FieldElement c, UInt (FFAUIntSize p (Order (BaseField c))) r c)
       (WitnessField c)))
-> (FieldElement c, UInt (FFAUIntSize p (Order (BaseField c))) r c)
forall x (c :: (Type -> Type) -> Type).
(SymbolicData x, Context x ~ c) =>
(Support x -> (c (Layout x), Payload x (WitnessField c))) -> x
forall (c :: (Type -> Type) -> Type).
(Context
   (FieldElement c, UInt (FFAUIntSize p (Order (BaseField c))) r c)
 ~ c) =>
(Support
   (FieldElement c, UInt (FFAUIntSize p (Order (BaseField c))) r c)
 -> (c (Layout
          (FieldElement c, UInt (FFAUIntSize p (Order (BaseField c))) r c)),
     Payload
       (FieldElement c, UInt (FFAUIntSize p (Order (BaseField c))) r c)
       (WitnessField c)))
-> (FieldElement c, UInt (FFAUIntSize p (Order (BaseField c))) r c)
restore ((Support
    (FieldElement c, UInt (FFAUIntSize p (Order (BaseField c))) r c)
  -> (c (Layout
           (FieldElement c, UInt (FFAUIntSize p (Order (BaseField c))) r c)),
      Payload
        (FieldElement c, UInt (FFAUIntSize p (Order (BaseField c))) r c)
        (WitnessField c)))
 -> (FieldElement c,
     UInt (FFAUIntSize p (Order (BaseField c))) r c))
-> (Support
      (FieldElement c, UInt (FFAUIntSize p (Order (BaseField c))) r c)
    -> (c (Layout
             (FieldElement c, UInt (FFAUIntSize p (Order (BaseField c))) r c)),
        Payload
          (FieldElement c, UInt (FFAUIntSize p (Order (BaseField c))) r c)
          (WitnessField c)))
-> (FieldElement c, UInt (FFAUIntSize p (Order (BaseField c))) r c)
forall a b. (a -> b) -> a -> b
$ (c (Par1
    :*: Layout (UInt (FFAUIntSize p (Order (BaseField c))) r c)),
 (:*:) U1 U1 (WitnessField c))
-> Proxy c
-> (c (Par1
       :*: Layout (UInt (FFAUIntSize p (Order (BaseField c))) r c)),
    (:*:) U1 U1 (WitnessField c))
forall a b. a -> b -> a
const
        ( c (Par1
   :*: (Layout (UInt (FFAUIntSize p (Order (BaseField c))) r c)
        :*: Par1))
-> CircuitFun
     '[Par1
       :*: (Layout (UInt (FFAUIntSize p (Order (BaseField c))) r c)
            :*: Par1)]
     (Par1 :*: Layout (UInt (FFAUIntSize p (Order (BaseField c))) r c))
     c
-> c (Par1
      :*: Layout (UInt (FFAUIntSize p (Order (BaseField c))) r c))
forall (f :: Type -> Type) (g :: Type -> Type).
c f -> CircuitFun '[f] g c -> c g
forall (c :: (Type -> Type) -> Type) (f :: Type -> Type)
       (g :: Type -> Type).
Symbolic c =>
c f -> CircuitFun '[f] g c -> c g
fromCircuitF ((FieldElement c, UInt (FFAUIntSize p (Order (BaseField c))) r c,
 Context (UInt (FFAUIntSize p (Order (BaseField c))) r c) Par1)
-> Support
     (FieldElement c, UInt (FFAUIntSize p (Order (BaseField c))) r c,
      Context (UInt (FFAUIntSize p (Order (BaseField c))) r c) Par1)
-> Context
     (FieldElement c, UInt (FFAUIntSize p (Order (BaseField c))) r c,
      Context (UInt (FFAUIntSize p (Order (BaseField c))) r c) Par1)
     (Layout
        (FieldElement c, UInt (FFAUIntSize p (Order (BaseField c))) r c,
         Context (UInt (FFAUIntSize p (Order (BaseField c))) r c) Par1))
forall x. SymbolicData x => x -> Support x -> Context x (Layout x)
arithmetize (FieldElement c
nr, UInt (FFAUIntSize p (Order (BaseField c))) r c
ur, Context (UInt (FFAUIntSize p (Order (BaseField c))) r c) Par1
ck) Proxy c
Support
  (FieldElement c, UInt (FFAUIntSize p (Order (BaseField c))) r c,
   Context (UInt (FFAUIntSize p (Order (BaseField c))) r c) Par1)
forall {k} (t :: k). Proxy t
Proxy)
            \(Par1 i
ni :*: Vector
  (NumberOfRegisters
     (BaseField c) (FFAUIntSize p (Order (BaseField c))) r)
  i
ui :*: Par1 i
b) -> do
              ClosedPoly i (BaseField c) -> m ()
forall var a w (m :: Type -> Type).
MonadCircuit var a w m =>
ClosedPoly var a -> m ()
constraint (((i -> x) -> i -> x
forall a b. (a -> b) -> a -> b
$ i
b) ((i -> x) -> x) -> ((i -> x) -> x) -> (i -> x) -> x
forall a. AdditiveGroup a => a -> a -> a
- (i -> x) -> x
forall a. MultiplicativeMonoid a => a
one)
              (:*:)
  Par1
  (Vector
     (NumberOfRegisters
        (BaseField c) (FFAUIntSize p (Order (BaseField c))) r))
  i
-> m ((:*:)
        Par1
        (Vector
           (NumberOfRegisters
              (BaseField c) (FFAUIntSize p (Order (BaseField c))) r))
        i)
forall a. a -> m a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Par1 i
ni Par1 i
-> Vector
     (NumberOfRegisters
        (BaseField c) (FFAUIntSize p (Order (BaseField c))) r)
     i
-> (:*:)
     Par1
     (Vector
        (NumberOfRegisters
           (BaseField c) (FFAUIntSize p (Order (BaseField c))) r))
     i
forall k (f :: k -> Type) (g :: k -> Type) (p :: k).
f p -> g p -> (:*:) f g p
:*: Vector
  (NumberOfRegisters
     (BaseField c) (FFAUIntSize p (Order (BaseField c))) r)
  i
ui)
        , U1 (WitnessField c)
forall k (p :: k). U1 p
U1 U1 (WitnessField c)
-> U1 (WitnessField c) -> (:*:) U1 U1 (WitnessField c)
forall k (f :: k -> Type) (g :: k -> Type) (p :: k).
f p -> g p -> (:*:) f g p
:*: U1 (WitnessField c)
forall k (p :: k). U1 p
U1)

instance Finite (Zp p) => Finite (FFA p r c) where
  type Order (FFA p r c) = p

instance (Symbolic c, KnownFFA p r c) => BinaryExpansion (FFA p r c) where
  type Bits (FFA p r c) = ByteString (NumberOfBits (Zp p)) c
  binaryExpansion :: FFA p r c -> Bits (FFA p r c)
binaryExpansion = UInt (Log2 (p - 1) + 1) r c -> ByteString (Log2 (p - 1) + 1) c
forall a b. Iso a b => a -> b
from (UInt (Log2 (p - 1) + 1) r c -> ByteString (Log2 (p - 1) + 1) c)
-> (FFA p r c -> UInt (Log2 (p - 1) + 1) r c)
-> FFA p r c
-> ByteString (Log2 (p - 1) + 1) c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (n :: Natural) (p :: Natural) (r :: RegisterSize)
       (c :: (Type -> Type) -> Type).
(Symbolic c, KnownFFA p r c, KnownNat n,
 KnownNat (NumberOfRegisters (BaseField c) n r),
 KnownNat (GetRegisterSize (BaseField c) n r)) =>
FFA p r c -> UInt n r c
toUInt @(NumberOfBits (Zp p))
  fromBinary :: Bits (FFA p r c) -> FFA p r c
fromBinary = forall (n :: Natural) (p :: Natural) (r :: RegisterSize)
       (c :: (Type -> Type) -> Type).
(Symbolic c, KnownFFA p r c, KnownNat n,
 KnownNat (GetRegisterSize (BaseField c) n r)) =>
UInt n r c -> FFA p r c
fromUInt @(NumberOfBits (Zp p)) (UInt (Log2 (p - 1) + 1) r c -> FFA p r c)
-> (ByteString (Log2 (p - 1) + 1) c -> UInt (Log2 (p - 1) + 1) r c)
-> ByteString (Log2 (p - 1) + 1) c
-> FFA p r c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ByteString (Log2 (p - 1) + 1) c -> UInt (Log2 (p - 1) + 1) r c
forall a b. Iso a b => a -> b
from

fromUInt ::
  forall n p r c.
  (Symbolic c, KnownFFA p r c) =>
  (KnownNat n, KnownNat (GetRegisterSize (BaseField c) n r)) =>
  UInt n r c -> FFA p r c
fromUInt :: forall (n :: Natural) (p :: Natural) (r :: RegisterSize)
       (c :: (Type -> Type) -> Type).
(Symbolic c, KnownFFA p r c, KnownNat n,
 KnownNat (GetRegisterSize (BaseField c) n r)) =>
UInt n r c -> FFA p r c
fromUInt UInt n r c
ux = FieldElement c
-> UInt (FFAUIntSize p (Order (BaseField c))) r c -> FFA p r c
forall (p :: Natural) (r :: RegisterSize)
       (c :: (Type -> Type) -> Type).
FieldElement c -> UIntFFA p r c -> FFA p r c
FFA (UInt n r c -> FieldElement c
forall (n :: Natural) (r :: RegisterSize)
       (c :: (Type -> Type) -> Type) a.
(Symbolic c, KnownNat n, KnownRegisterSize r, BaseField c ~ a,
 KnownNat (GetRegisterSize a n r)) =>
UInt n r c -> FieldElement c
toNative UInt n r c
ux) (UInt n r c -> UInt (FFAUIntSize p (Order (BaseField c))) r c
forall a b. Resize a b => a -> b
resize UInt n r c
ux)

toUInt ::
  forall n p r c.
  (Symbolic c, KnownFFA p r c) =>
  (KnownNat n, KnownNat (NumberOfRegisters (BaseField c) n r)) =>
  (KnownNat (GetRegisterSize (BaseField c) n r)) =>
  FFA p r c -> UInt n r c
toUInt :: forall (n :: Natural) (p :: Natural) (r :: RegisterSize)
       (c :: (Type -> Type) -> Type).
(Symbolic c, KnownFFA p r c, KnownNat n,
 KnownNat (NumberOfRegisters (BaseField c) n r),
 KnownNat (GetRegisterSize (BaseField c) n r)) =>
FFA p r c -> UInt n r c
toUInt FFA p r c
x = UInt n r c
uy
  where
    -- | Computes unconstrained UInt value
    us :: UInt n r c
    us :: UInt n r c
us = (Support (UInt n r c)
 -> (c (Layout (UInt n r c)),
     Payload (UInt n r c) (WitnessField c)))
-> UInt n r c
forall x (c :: (Type -> Type) -> Type).
(SymbolicData x, Context x ~ c) =>
(Support x -> (c (Layout x), Payload x (WitnessField c))) -> x
forall (c :: (Type -> Type) -> Type).
(Context (UInt n r c) ~ c) =>
(Support (UInt n r c)
 -> (c (Layout (UInt n r c)),
     Payload (UInt n r c) (WitnessField c)))
-> UInt n r c
restore ((Support (UInt n r c)
  -> (c (Layout (UInt n r c)),
      Payload (UInt n r c) (WitnessField c)))
 -> UInt n r c)
-> (Support (UInt n r c)
    -> (c (Layout (UInt n r c)),
        Payload (UInt n r c) (WitnessField c)))
-> UInt n r c
forall a b. (a -> b) -> a -> b
$ (c (Vector (NumberOfRegisters (BaseField c) n r)),
 U1 (WitnessField c))
-> Proxy c
-> (c (Vector (NumberOfRegisters (BaseField c) n r)),
    U1 (WitnessField c))
forall a b. a -> b -> a
const
      ( c (Par1
   :*: Vector
         (NumberOfRegisters
            (BaseField c) (FFAUIntSize p (Order (BaseField c))) r))
-> ((:*:)
      Par1
      (Vector
         (NumberOfRegisters
            (BaseField c) (FFAUIntSize p (Order (BaseField c))) r))
      (BaseField c)
    -> Vector (NumberOfRegisters (BaseField c) n r) (BaseField c))
-> CircuitFun
     '[Par1
       :*: Vector
             (NumberOfRegisters
                (BaseField c) (FFAUIntSize p (Order (BaseField c))) r)]
     (Vector (NumberOfRegisters (BaseField c) n r))
     c
-> c (Vector (NumberOfRegisters (BaseField c) n r))
forall (c :: (Type -> Type) -> Type) a (f :: Type -> Type)
       (g :: Type -> Type).
(Symbolic c, BaseField c ~ a) =>
c f -> (f a -> g a) -> CircuitFun '[f] g c -> c g
symbolicF (FFA p r c
-> Support (FFA p r c) -> Context (FFA p r c) (Layout (FFA p r c))
forall x. SymbolicData x => x -> Support x -> Context x (Layout x)
arithmetize FFA p r c
x Proxy c
Support (FFA p r c)
forall {k} (t :: k). Proxy t
Proxy)
          (\(forall (p :: Natural) (r :: RegisterSize) a.
(Arithmetic a, KnownFFA p r (Interpreter a)) =>
(:*:)
  Par1 (Vector (NumberOfRegisters a (FFAUIntSize p (Order a)) r)) a
-> Integer
fromFFA @p @r -> Integer
v) ->
            let UInt (Interpreter Vector
  (NumberOfRegisters (BaseField (Interpreter (BaseField c))) n r)
  (BaseField c)
f) = Integer -> UInt n r (Interpreter (BaseField c))
forall a b. FromConstant a b => a -> b
fromConstant Integer
v
                  :: UInt n r (Interpreter (BaseField c))
             in Vector (NumberOfRegisters (BaseField c) n r) (BaseField c)
Vector
  (NumberOfRegisters (BaseField (Interpreter (BaseField c))) n r)
  (BaseField c)
f
          )
          \(forall (p :: Natural) (r :: RegisterSize)
       (c :: (Type -> Type) -> Type) i a.
(Symbolic c, KnownFFA p r c, Witness i (WitnessField c),
 a ~ BaseField c) =>
(:*:)
  Par1 (Vector (NumberOfRegisters a (FFAUIntSize p (Order a)) r)) i
-> IntegralOf (WitnessField c)
valueFFA @p @r @c -> IntegralOf (WitnessField c)
v) ->
            (WitnessField c -> m i)
-> Vector (NumberOfRegisters (BaseField c) n r) (WitnessField c)
-> m (Vector (NumberOfRegisters (BaseField c) n r) i)
forall (t :: Type -> Type) (f :: Type -> Type) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: Type -> Type) a b.
Applicative f =>
(a -> f b)
-> Vector (NumberOfRegisters (BaseField c) n r) a
-> f (Vector (NumberOfRegisters (BaseField c) n r) b)
traverse WitnessField c -> m i
forall var a w (m :: Type -> Type).
MonadCircuit var a w m =>
w -> m var
unconstrained (Vector (NumberOfRegisters (BaseField c) n r) (WitnessField c)
 -> m (Vector (NumberOfRegisters (BaseField c) n r) i))
-> Vector (NumberOfRegisters (BaseField c) n r) (WitnessField c)
-> m (Vector (NumberOfRegisters (BaseField c) n r) i)
forall a b. (a -> b) -> a -> b
$ (Rep (Vector (NumberOfRegisters (BaseField c) n r))
 -> WitnessField c)
-> Vector (NumberOfRegisters (BaseField c) n r) (WitnessField c)
forall a.
(Rep (Vector (NumberOfRegisters (BaseField c) n r)) -> a)
-> Vector (NumberOfRegisters (BaseField c) n r) a
forall (f :: Type -> Type) a.
Representable f =>
(Rep f -> a) -> f a
tabulate (forall (c :: (Type -> Type) -> Type) (n :: Natural)
       (r :: RegisterSize).
(Symbolic c, KnownNat n, KnownRegisterSize r) =>
IntegralOf (WitnessField c)
-> Zp (NumberOfRegisters (BaseField c) n r) -> WitnessField c
register @c @n @r IntegralOf (WitnessField c)
v)
      , U1 (WitnessField c)
forall k (p :: k). U1 p
U1)
    -- | Constraints:
    -- * UInt registers are indeed registers;
    -- * casting back yields source residues.
    Bool c Par1
ck = UInt n r c -> Bool (Context (UInt n r c))
forall d. SymbolicInput d => d -> Bool (Context d)
isValid UInt n r c
us Bool c -> Bool c -> Bool c
forall b. BoolType b => b -> b -> b
&& UInt n r c -> FFA p r c
forall (n :: Natural) (p :: Natural) (r :: RegisterSize)
       (c :: (Type -> Type) -> Type).
(Symbolic c, KnownFFA p r c, KnownNat n,
 KnownNat (GetRegisterSize (BaseField c) n r)) =>
UInt n r c -> FFA p r c
fromUInt UInt n r c
us FFA p r c -> FFA p r c -> BooleanOf (FFA p r c)
forall a. Eq a => a -> a -> BooleanOf a
== FFA p r c
x
    -- | Sew constraints into result.
    uy :: UInt n r c
uy = (Support (UInt n r c)
 -> (c (Layout (UInt n r c)),
     Payload (UInt n r c) (WitnessField c)))
-> UInt n r c
forall x (c :: (Type -> Type) -> Type).
(SymbolicData x, Context x ~ c) =>
(Support x -> (c (Layout x), Payload x (WitnessField c))) -> x
forall (c :: (Type -> Type) -> Type).
(Context (UInt n r c) ~ c) =>
(Support (UInt n r c)
 -> (c (Layout (UInt n r c)),
     Payload (UInt n r c) (WitnessField c)))
-> UInt n r c
restore ((Support (UInt n r c)
  -> (c (Layout (UInt n r c)),
      Payload (UInt n r c) (WitnessField c)))
 -> UInt n r c)
-> (Support (UInt n r c)
    -> (c (Layout (UInt n r c)),
        Payload (UInt n r c) (WitnessField c)))
-> UInt n r c
forall a b. (a -> b) -> a -> b
$ (c (Vector (NumberOfRegisters (BaseField c) n r)),
 U1 (WitnessField c))
-> Proxy c
-> (c (Vector (NumberOfRegisters (BaseField c) n r)),
    U1 (WitnessField c))
forall a b. a -> b -> a
const
      ( c (Vector (NumberOfRegisters (BaseField c) n r))
-> c Par1
-> CircuitFun
     '[Vector (NumberOfRegisters (BaseField c) n r), Par1]
     (Vector (NumberOfRegisters (BaseField c) n r))
     c
-> c (Vector (NumberOfRegisters (BaseField c) n r))
forall (c :: (Type -> Type) -> Type) (f :: Type -> Type)
       (g :: Type -> Type) (h :: Type -> Type).
Symbolic c =>
c f -> c g -> CircuitFun '[f, g] h c -> c h
fromCircuit2F (UInt n r c
-> Support (UInt n r c)
-> Context (UInt n r c) (Layout (UInt n r c))
forall x. SymbolicData x => x -> Support x -> Context x (Layout x)
arithmetize UInt n r c
us Proxy c
Support (UInt n r c)
forall {k} (t :: k). Proxy t
Proxy) c Par1
ck
          \Vector (NumberOfRegisters (BaseField c) n r) i
xi (Par1 i
b) -> ClosedPoly i (BaseField c) -> m ()
forall var a w (m :: Type -> Type).
MonadCircuit var a w m =>
ClosedPoly var a -> m ()
constraint (((i -> x) -> i -> x
forall a b. (a -> b) -> a -> b
$ i
b) ((i -> x) -> x) -> ((i -> x) -> x) -> (i -> x) -> x
forall a. AdditiveGroup a => a -> a -> a
- (i -> x) -> x
forall a. MultiplicativeMonoid a => a
one) m ()
-> Vector (NumberOfRegisters (BaseField c) n r) i
-> m (Vector (NumberOfRegisters (BaseField c) n r) i)
forall (f :: Type -> Type) a b. Functor f => f a -> b -> f b
$> Vector (NumberOfRegisters (BaseField c) n r) i
xi
      , U1 (WitnessField c)
forall k (p :: k). U1 p
U1)