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

module ZkFold.Symbolic.Data.Ord (Ord (..), blueprintGE, bitwiseGE, bitwiseGT, getBitsBE) where

import           Control.Monad                    (foldM)
import qualified Data.Bool                        as Haskell
import           Data.Data                        (Proxy (..))
import           Data.Foldable                    (Foldable, concatMap, toList)
import           Data.Function                    ((.))
import           Data.Functor                     (fmap, (<$>))
import           Data.Functor.Rep                 (Representable)
import           Data.List                        (map, reverse)
import           Data.Traversable                 (Traversable (traverse))
import qualified Data.Zip                         as Z
import           GHC.Generics                     (Par1 (..))
import           Prelude                          (type (~), ($))
import qualified Prelude                          as Haskell

import           ZkFold.Base.Algebra.Basic.Class
import           ZkFold.Base.Algebra.Basic.Number
import           ZkFold.Symbolic.Class            (Arithmetic, Symbolic (BaseField), symbolic2F, symbolicF)
import           ZkFold.Symbolic.Data.Bool        (Bool (..))
import           ZkFold.Symbolic.Data.Class
import           ZkFold.Symbolic.Data.Combinators (expansion)
import           ZkFold.Symbolic.Data.Conditional (Conditional (..))
import           ZkFold.Symbolic.MonadCircuit

-- TODO (Issue #23): add `compare`
class Ord b a where
    (<=) :: a -> a -> b

    (<) :: a -> a -> b

    (>=) :: a -> a -> b

    (>) :: a -> a -> b

    max :: a -> a -> a
    -- max x y = bool @b y x $ x <= y

    min :: a -> a -> a
    -- min x y = bool @b y x $ x >= y

instance Haskell.Ord a => Ord Haskell.Bool a where
    <= :: a -> a -> Bool
(<=) = a -> a -> Bool
forall a. Ord a => a -> a -> Bool
(Haskell.<=)

    < :: a -> a -> Bool
(<) = a -> a -> Bool
forall a. Ord a => a -> a -> Bool
(Haskell.<)

    >= :: a -> a -> Bool
(>=) = a -> a -> Bool
forall a. Ord a => a -> a -> Bool
(Haskell.>=)

    > :: a -> a -> Bool
(>) = a -> a -> Bool
forall a. Ord a => a -> a -> Bool
(Haskell.>)

    max :: a -> a -> a
max = a -> a -> a
forall a. Ord a => a -> a -> a
Haskell.max

    min :: a -> a -> a
min = a -> a -> a
forall a. Ord a => a -> a -> a
Haskell.min

-- | Every @SymbolicData@ type can be compared lexicographically.
instance
    ( Symbolic c
    , Representable f
    , Traversable f
    ) => Ord (Bool c) (c f) where

    c f
x <= :: c f -> c f -> Bool c
<= c f
y = c f
y c f -> c f -> Bool c
forall b a. Ord b a => a -> a -> b
>= c f
x

    c f
x < :: c f -> c f -> Bool c
<  c f
y = c f
y c f -> c f -> Bool c
forall b a. Ord b a => a -> a -> b
> c f
x

    c f
x >= :: c f -> c f -> Bool c
>= c f
y = forall (r :: Nat) (c :: (Type -> Type) -> Type)
       (f :: Type -> Type).
(Symbolic c, Zip f, Foldable f, KnownNat r) =>
c f -> c f -> Bool c
bitwiseGE @1 (c f -> c []
forall (c :: (Type -> Type) -> Type) x.
(SymbolicOutput x, Context x ~ c) =>
x -> c []
getBitsBE c f
x) (c f -> c []
forall (c :: (Type -> Type) -> Type) x.
(SymbolicOutput x, Context x ~ c) =>
x -> c []
getBitsBE c f
y)

    c f
x > :: c f -> c f -> Bool c
> c f
y = forall (r :: Nat) (c :: (Type -> Type) -> Type)
       (f :: Type -> Type).
(Symbolic c, Zip f, Foldable f, KnownNat r) =>
c f -> c f -> Bool c
bitwiseGT @1 (c f -> c []
forall (c :: (Type -> Type) -> Type) x.
(SymbolicOutput x, Context x ~ c) =>
x -> c []
getBitsBE c f
x) (c f -> c []
forall (c :: (Type -> Type) -> Type) x.
(SymbolicOutput x, Context x ~ c) =>
x -> c []
getBitsBE c f
y)

    max :: c f -> c f -> c f
max c f
x c f
y = forall b a. Conditional b a => a -> a -> b -> a
bool @(Bool c) c f
x c f
y (Bool c -> c f) -> Bool c -> c f
forall a b. (a -> b) -> a -> b
$ c f
x c f -> c f -> Bool c
forall b a. Ord b a => a -> a -> b
< c f
y

    min :: c f -> c f -> c f
min c f
x c f
y = forall b a. Conditional b a => a -> a -> b -> a
bool @(Bool c) c f
x c f
y (Bool c -> c f) -> Bool c -> c f
forall a b. (a -> b) -> a -> b
$ c f
x c f -> c f -> Bool c
forall b a. Ord b a => a -> a -> b
> c f
y

getBitsBE ::
  forall c x .
  (SymbolicOutput x, Context x ~ c) =>
  x -> c []
-- ^ @getBitsBE x@ returns a list of circuits computing bits of @x@, eldest to
-- youngest.
getBitsBE :: forall (c :: (Type -> Type) -> Type) x.
(SymbolicOutput x, Context x ~ c) =>
x -> c []
getBitsBE x
x = c (Layout x)
-> (Layout x (BaseField c) -> [BaseField c])
-> CircuitFun '[Layout x] [] c
-> c []
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 (x -> Support x -> Context x (Layout x)
forall x. SymbolicData x => x -> Support x -> Context x (Layout x)
arithmetize x
x Proxy c
Support x
forall {k} (t :: k). Proxy t
Proxy)
    ((BaseField c -> [BaseField c])
-> Layout x (BaseField c) -> [BaseField c]
forall (t :: Type -> Type) a b.
Foldable t =>
(a -> [b]) -> t a -> [b]
concatMap ([BaseField c] -> [BaseField c]
forall a. [a] -> [a]
reverse ([BaseField c] -> [BaseField c])
-> (BaseField c -> [BaseField c]) -> BaseField c -> [BaseField c]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Nat -> [BaseField c] -> [BaseField c]
forall a. AdditiveMonoid a => Nat -> [a] -> [a]
padBits Nat
n ([BaseField c] -> [BaseField c])
-> (BaseField c -> [BaseField c]) -> BaseField c -> [BaseField c]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Nat -> BaseField c) -> [Nat] -> [BaseField c]
forall a b. (a -> b) -> [a] -> [b]
map Nat -> BaseField c
forall a b. FromConstant a b => a -> b
fromConstant ([Nat] -> [BaseField c])
-> (BaseField c -> [Nat]) -> BaseField c -> [BaseField c]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Nat -> [Nat]
Nat -> Bits Nat
forall a. BinaryExpansion a => a -> Bits a
binaryExpansion (Nat -> [Nat]) -> (BaseField c -> Nat) -> BaseField c -> [Nat]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BaseField c -> Nat
BaseField c -> Const (BaseField c)
forall a. ToConstant a => a -> Const a
toConstant))
    (([[i]] -> [i]) -> m [[i]] -> m [i]
forall a b. (a -> b) -> m a -> m b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap (([i] -> [i]) -> [[i]] -> [i]
forall (t :: Type -> Type) a b.
Foldable t =>
(a -> [b]) -> t a -> [b]
concatMap [i] -> [i]
forall a. [a] -> [a]
reverse) (m [[i]] -> m [i])
-> (Layout x i -> m [[i]]) -> Layout x i -> m [i]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (i -> m [i]) -> [i] -> m [[i]]
forall (t :: Type -> Type) (f :: Type -> Type) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: Type -> Type) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse (Nat -> i -> m [i]
forall i a w (m :: Type -> Type).
(MonadCircuit i a w m, Arithmetic a) =>
Nat -> i -> m [i]
expansion Nat
n) ([i] -> m [[i]]) -> (Layout x i -> [i]) -> Layout x i -> m [[i]]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Layout x i -> [i]
forall a. Layout x a -> [a]
forall (t :: Type -> Type) a. Foldable t => t a -> [a]
toList)
  where n :: Nat
n = forall a. KnownNat (NumberOfBits a) => Nat
numberOfBits @(BaseField c)

bitwiseGE :: forall r c f . (Symbolic c, Z.Zip f, Foldable f, KnownNat r) => c f -> c f -> Bool c
-- ^ Given two lists of bits of equal length, compares them lexicographically.
bitwiseGE :: forall (r :: Nat) (c :: (Type -> Type) -> Type)
       (f :: Type -> Type).
(Symbolic c, Zip f, Foldable f, KnownNat r) =>
c f -> c f -> Bool c
bitwiseGE c f
xs c f
ys = c Par1 -> Bool c
forall (c :: (Type -> Type) -> Type). c Par1 -> Bool c
Bool (c Par1 -> Bool c) -> c Par1 -> Bool c
forall a b. (a -> b) -> a -> b
$
  c f
-> c f
-> (f (BaseField c) -> f (BaseField c) -> Par1 (BaseField c))
-> (forall {i} {m :: Type -> Type}.
    (NFData i, MonadCircuit i (BaseField c) (WitnessField c) m) =>
    FunBody '[f, f] Par1 i m)
-> c Par1
forall (c :: (Type -> Type) -> Type) a (f :: Type -> Type)
       (g :: Type -> Type) (h :: Type -> Type).
(Symbolic c, BaseField c ~ a) =>
c f -> c g -> (f a -> g a -> h a) -> CircuitFun '[f, g] h c -> c h
symbolic2F c f
xs c f
ys
    (\f (BaseField c)
us f (BaseField c)
vs -> BaseField c -> Par1 (BaseField c)
forall p. p -> Par1 p
Par1 (BaseField c -> Par1 (BaseField c))
-> BaseField c -> Par1 (BaseField c)
forall a b. (a -> b) -> a -> b
$ BaseField c -> BaseField c -> Bool -> BaseField c
forall a. a -> a -> Bool -> a
Haskell.bool BaseField c
forall a. AdditiveMonoid a => a
zero BaseField c
forall a. MultiplicativeMonoid a => a
one (f (BaseField c) -> [BaseField c]
forall a. f a -> [a]
forall (t :: Type -> Type) a. Foldable t => t a -> [a]
toList f (BaseField c)
us [BaseField c] -> [BaseField c] -> Bool
forall a. Ord a => a -> a -> Bool
Haskell.>= f (BaseField c) -> [BaseField c]
forall a. f a -> [a]
forall (t :: Type -> Type) a. Foldable t => t a -> [a]
toList f (BaseField c)
vs))
    ((forall {i} {m :: Type -> Type}.
  (NFData i, MonadCircuit i (BaseField c) (WitnessField c) m) =>
  FunBody '[f, f] Par1 i m)
 -> c Par1)
-> (forall {i} {m :: Type -> Type}.
    (NFData i, MonadCircuit i (BaseField c) (WitnessField c) m) =>
    FunBody '[f, f] Par1 i m)
-> c Par1
forall a b. (a -> b) -> a -> b
$ \f i
is f i
js -> i -> Par1 i
forall p. p -> Par1 p
Par1 (i -> Par1 i) -> m i -> m (Par1 i)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (r :: Nat) i a w (m :: Type -> Type) (f :: Type -> Type).
(Arithmetic a, MonadCircuit i a w m, Zip f, Foldable f,
 KnownNat r) =>
f i -> f i -> m i
blueprintGE @r f i
is f i
js

blueprintGE :: forall r i a w m f . (Arithmetic a, MonadCircuit i a w m, Z.Zip f, Foldable f, KnownNat r) => f i -> f i -> m i
blueprintGE :: forall (r :: Nat) i a w (m :: Type -> Type) (f :: Type -> Type).
(Arithmetic a, MonadCircuit i a w m, Zip f, Foldable f,
 KnownNat r) =>
f i -> f i -> m i
blueprintGE f i
xs f i
ys = do
  (i
_, i
hasNegOne) <- forall (r :: Nat) i a w (m :: Type -> Type) (f :: Type -> Type).
(Arithmetic a, MonadCircuit i a w m, Zip f, Foldable f,
 KnownNat r) =>
f i -> f i -> m (i, i)
circuitDelta @r f i
xs f i
ys
  ClosedPoly i a -> m i
forall var a w (m :: Type -> Type).
MonadCircuit var a w m =>
ClosedPoly var a -> m var
newAssigned (ClosedPoly i a -> m i) -> ClosedPoly i a -> m i
forall a b. (a -> b) -> a -> b
$ \i -> x
p -> x
forall a. MultiplicativeMonoid a => a
one x -> x -> x
forall a. AdditiveGroup a => a -> a -> a
- i -> x
p i
hasNegOne

bitwiseGT :: forall r c f . (Symbolic c, Z.Zip f, Foldable f, KnownNat r) => c f -> c f -> Bool c
-- ^ Given two lists of bits of equal length, compares them lexicographically.
bitwiseGT :: forall (r :: Nat) (c :: (Type -> Type) -> Type)
       (f :: Type -> Type).
(Symbolic c, Zip f, Foldable f, KnownNat r) =>
c f -> c f -> Bool c
bitwiseGT c f
xs c f
ys = c Par1 -> Bool c
forall (c :: (Type -> Type) -> Type). c Par1 -> Bool c
Bool (c Par1 -> Bool c) -> c Par1 -> Bool c
forall a b. (a -> b) -> a -> b
$
  c f
-> c f
-> (f (BaseField c) -> f (BaseField c) -> Par1 (BaseField c))
-> (forall {i} {m :: Type -> Type}.
    (NFData i, MonadCircuit i (BaseField c) (WitnessField c) m) =>
    FunBody '[f, f] Par1 i m)
-> c Par1
forall (c :: (Type -> Type) -> Type) a (f :: Type -> Type)
       (g :: Type -> Type) (h :: Type -> Type).
(Symbolic c, BaseField c ~ a) =>
c f -> c g -> (f a -> g a -> h a) -> CircuitFun '[f, g] h c -> c h
symbolic2F c f
xs c f
ys
    (\f (BaseField c)
us f (BaseField c)
vs -> BaseField c -> Par1 (BaseField c)
forall p. p -> Par1 p
Par1 (BaseField c -> Par1 (BaseField c))
-> BaseField c -> Par1 (BaseField c)
forall a b. (a -> b) -> a -> b
$ BaseField c -> BaseField c -> Bool -> BaseField c
forall a. a -> a -> Bool -> a
Haskell.bool BaseField c
forall a. AdditiveMonoid a => a
zero BaseField c
forall a. MultiplicativeMonoid a => a
one (f (BaseField c) -> [BaseField c]
forall a. f a -> [a]
forall (t :: Type -> Type) a. Foldable t => t a -> [a]
toList f (BaseField c)
us [BaseField c] -> [BaseField c] -> Bool
forall a. Ord a => a -> a -> Bool
Haskell.> f (BaseField c) -> [BaseField c]
forall a. f a -> [a]
forall (t :: Type -> Type) a. Foldable t => t a -> [a]
toList f (BaseField c)
vs))
    ((forall {i} {m :: Type -> Type}.
  (NFData i, MonadCircuit i (BaseField c) (WitnessField c) m) =>
  FunBody '[f, f] Par1 i m)
 -> c Par1)
-> (forall {i} {m :: Type -> Type}.
    (NFData i, MonadCircuit i (BaseField c) (WitnessField c) m) =>
    FunBody '[f, f] Par1 i m)
-> c Par1
forall a b. (a -> b) -> a -> b
$ \f i
is f i
js -> do
      (i
hasOne, i
hasNegOne) <- forall (r :: Nat) i a w (m :: Type -> Type) (f :: Type -> Type).
(Arithmetic a, MonadCircuit i a w m, Zip f, Foldable f,
 KnownNat r) =>
f i -> f i -> m (i, i)
circuitDelta @r f i
is f i
js
      i -> Par1 i
forall p. p -> Par1 p
Par1 (i -> Par1 i) -> m i -> m (Par1 i)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> ClosedPoly i (BaseField c) -> m i
forall var a w (m :: Type -> Type).
MonadCircuit var a w m =>
ClosedPoly var a -> m var
newAssigned (\i -> x
p -> i -> x
p i
hasOne x -> x -> x
forall a. MultiplicativeSemigroup a => a -> a -> a
* (x
forall a. MultiplicativeMonoid a => a
one x -> x -> x
forall a. AdditiveGroup a => a -> a -> a
- i -> x
p i
hasNegOne))

-- | Compare two sets of r-bit words lexicographically
--
circuitDelta :: forall r i a w m f . (Arithmetic a, MonadCircuit i a w m, Z.Zip f, Foldable f, KnownNat r) => f i -> f i -> m (i, i)
circuitDelta :: forall (r :: Nat) i a w (m :: Type -> Type) (f :: Type -> Type).
(Arithmetic a, MonadCircuit i a w m, Zip f, Foldable f,
 KnownNat r) =>
f i -> f i -> m (i, i)
circuitDelta f i
l f i
r = do
    i
z1 <- ClosedPoly i a -> m i
forall var a w (m :: Type -> Type).
MonadCircuit var a w m =>
ClosedPoly var a -> m var
newAssigned (x -> (i -> x) -> x
forall a b. a -> b -> a
Haskell.const x
forall a. AdditiveMonoid a => a
zero)
    i
z2 <- ClosedPoly i a -> m i
forall var a w (m :: Type -> Type).
MonadCircuit var a w m =>
ClosedPoly var a -> m var
newAssigned (x -> (i -> x) -> x
forall a b. a -> b -> a
Haskell.const x
forall a. AdditiveMonoid a => a
zero)
    ((i, i) -> (i, i) -> m (i, i)) -> (i, i) -> f (i, i) -> m (i, i)
forall (t :: Type -> Type) (m :: Type -> Type) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM (i, i) -> (i, i) -> m (i, i)
update (i
z1, i
z2) (f (i, i) -> m (i, i)) -> f (i, i) -> m (i, i)
forall a b. (a -> b) -> a -> b
$ f i -> f i -> f (i, i)
forall a b. f a -> f b -> f (a, b)
forall (f :: Type -> Type) a b. Zip f => f a -> f b -> f (a, b)
Z.zip f i
l f i
r
        where
            bound :: a
bound = Nat -> a -> a
forall b a. Scale b a => b -> a -> a
scale ((Nat
2 Nat -> Nat -> Nat
forall a b. Exponent a b => a -> b -> a
^ forall (n :: Nat). KnownNat n => Nat
value @r) Nat -> Nat -> Nat
-! Nat
1) a
forall a. MultiplicativeMonoid a => a
one

            -- | If @z1@ is set, there was an index i where @xs[i] == 1@ and @ys[i] == 0@ and @xs[j] == ys[j]@ for all j < i.
            -- In this case, no matter what bit states are after this index, @z1@ and @z2@ are not updated.
            --
            --   If @z2@ is set, there was an index i where @xs[i] == 0@ and @ys[i] == 1@ and @xs[j] == ys[j]@ for all j < i.
            -- In the same manner, @z1@ and @z2@ won't be updated afterwards.
            update :: (i, i) -> (i, i) -> m (i, i)
            update :: (i, i) -> (i, i) -> m (i, i)
update (i
z1, i
z2) (i
x, i
y) = do
                -- @f1@ is one if and only if @x > y@ and zero otherwise.
                -- @(y + 1) `div` (x + 1)@ is zero if and only if @y < x@ regardless of whether @x@ is zero.
                -- @x@ and @y@ are expected to be of at most @r@ bits where @r << NumberOfBits a@, so @x + 1@ will not be zero either.
                -- Because of our laws for @finv@, @q // q@ is 1 if @q@ is not zero, and zero otherwise.
                -- This is exactly the opposite of what @f1@ should be.
                i
f1 <- a -> w -> m i
forall var a w (m :: Type -> Type).
MonadCircuit var a w m =>
a -> w -> m var
newRanged a
forall a. MultiplicativeMonoid a => a
one (w -> m i) -> w -> m i
forall a b. (a -> b) -> a -> b
$
                    let q :: w
q = Const w -> w
forall a b. FromConstant a b => a -> b
fromConstant (w -> Const w
forall a. ToConstant a => a -> Const a
toConstant (i -> w
forall i w. Witness i w => i -> w
at i
y w -> w -> w
forall a. AdditiveSemigroup a => a -> a -> a
+ forall a. MultiplicativeMonoid a => a
one @w) Const w -> Const w -> Const w
forall a. SemiEuclidean a => a -> a -> a
`div` w -> Const w
forall a. ToConstant a => a -> Const a
toConstant (i -> w
forall i w. Witness i w => i -> w
at i
x w -> w -> w
forall a. AdditiveSemigroup a => a -> a -> a
+ forall a. MultiplicativeMonoid a => a
one @w))
                     in w
forall a. MultiplicativeMonoid a => a
one w -> w -> w
forall a. AdditiveGroup a => a -> a -> a
- w
q w -> w -> w
forall a. Field a => a -> a -> a
// w
q

                -- f2 is one if and only if y > x and zero otherwise
                i
f2 <- a -> w -> m i
forall var a w (m :: Type -> Type).
MonadCircuit var a w m =>
a -> w -> m var
newRanged a
forall a. MultiplicativeMonoid a => a
one (w -> m i) -> w -> m i
forall a b. (a -> b) -> a -> b
$
                    let q :: w
q = Const w -> w
forall a b. FromConstant a b => a -> b
fromConstant (w -> Const w
forall a. ToConstant a => a -> Const a
toConstant (i -> w
forall i w. Witness i w => i -> w
at i
x w -> w -> w
forall a. AdditiveSemigroup a => a -> a -> a
+ forall a. MultiplicativeMonoid a => a
one @w) Const w -> Const w -> Const w
forall a. SemiEuclidean a => a -> a -> a
`div` w -> Const w
forall a. ToConstant a => a -> Const a
toConstant (i -> w
forall i w. Witness i w => i -> w
at i
y w -> w -> w
forall a. AdditiveSemigroup a => a -> a -> a
+ forall a. MultiplicativeMonoid a => a
one @w))
                     in w
forall a. MultiplicativeMonoid a => a
one w -> w -> w
forall a. AdditiveGroup a => a -> a -> a
- w
q w -> w -> w
forall a. Field a => a -> a -> a
// w
q

                i
dxy <- ClosedPoly i a -> m i
forall var a w (m :: Type -> Type).
MonadCircuit var a w m =>
ClosedPoly var a -> m var
newAssigned (\i -> x
p -> i -> x
p i
x x -> x -> x
forall a. AdditiveGroup a => a -> a -> a
- i -> x
p i
y)

                i
d1  <- ClosedPoly i a -> m i
forall var a w (m :: Type -> Type).
MonadCircuit var a w m =>
ClosedPoly var a -> m var
newAssigned (\i -> x
p -> i -> x
p i
f1 x -> x -> x
forall a. MultiplicativeSemigroup a => a -> a -> a
* i -> x
p i
dxy x -> x -> x
forall a. AdditiveGroup a => a -> a -> a
- i -> x
p i
f1)
                i
d1' <- ClosedPoly i a -> m i
forall var a w (m :: Type -> Type).
MonadCircuit var a w m =>
ClosedPoly var a -> m var
newAssigned (\i -> x
p -> (x
forall a. MultiplicativeMonoid a => a
one x -> x -> x
forall a. AdditiveGroup a => a -> a -> a
- i -> x
p i
f1) x -> x -> x
forall a. MultiplicativeSemigroup a => a -> a -> a
* x -> x
forall a. AdditiveGroup a => a -> a
negate (i -> x
p i
dxy))
                i -> a -> m ()
forall var a w (m :: Type -> Type).
MonadCircuit var a w m =>
var -> a -> m ()
rangeConstraint i
d1  a
bound
                i -> a -> m ()
forall var a w (m :: Type -> Type).
MonadCircuit var a w m =>
var -> a -> m ()
rangeConstraint i
d1' a
bound

                i
d2  <- ClosedPoly i a -> m i
forall var a w (m :: Type -> Type).
MonadCircuit var a w m =>
ClosedPoly var a -> m var
newAssigned (\i -> x
p -> i -> x
p i
f2 x -> x -> x
forall a. MultiplicativeSemigroup a => a -> a -> a
* (x -> x
forall a. AdditiveGroup a => a -> a
negate x
forall a. MultiplicativeMonoid a => a
one x -> x -> x
forall a. AdditiveGroup a => a -> a -> a
- i -> x
p i
dxy))
                i
d2' <- ClosedPoly i a -> m i
forall var a w (m :: Type -> Type).
MonadCircuit var a w m =>
ClosedPoly var a -> m var
newAssigned (\i -> x
p -> i -> x
p i
dxy x -> x -> x
forall a. AdditiveGroup a => a -> a -> a
- i -> x
p i
f2 x -> x -> x
forall a. MultiplicativeSemigroup a => a -> a -> a
* i -> x
p i
dxy)
                i -> a -> m ()
forall var a w (m :: Type -> Type).
MonadCircuit var a w m =>
var -> a -> m ()
rangeConstraint i
d2  a
bound
                i -> a -> m ()
forall var a w (m :: Type -> Type).
MonadCircuit var a w m =>
var -> a -> m ()
rangeConstraint i
d2' a
bound

                i
bothZero <- ClosedPoly i a -> m i
forall var a w (m :: Type -> Type).
MonadCircuit var a w m =>
ClosedPoly var a -> m var
newAssigned (ClosedPoly i a -> m i) -> ClosedPoly i a -> m i
forall a b. (a -> b) -> a -> b
$ \i -> x
p -> (x
forall a. MultiplicativeMonoid a => a
one x -> x -> x
forall a. AdditiveGroup a => a -> a -> a
- i -> x
p i
z1) x -> x -> x
forall a. MultiplicativeSemigroup a => a -> a -> a
* (x
forall a. MultiplicativeMonoid a => a
one x -> x -> x
forall a. AdditiveGroup a => a -> a -> a
- i -> x
p i
z2)

                i
f1z <- ClosedPoly i a -> m i
forall var a w (m :: Type -> Type).
MonadCircuit var a w m =>
ClosedPoly var a -> m var
newAssigned (ClosedPoly i a -> m i) -> ClosedPoly i a -> m i
forall a b. (a -> b) -> a -> b
$ \i -> x
p -> i -> x
p i
bothZero x -> x -> x
forall a. MultiplicativeSemigroup a => a -> a -> a
* i -> x
p i
f1
                i
f2z <- ClosedPoly i a -> m i
forall var a w (m :: Type -> Type).
MonadCircuit var a w m =>
ClosedPoly var a -> m var
newAssigned (ClosedPoly i a -> m i) -> ClosedPoly i a -> m i
forall a b. (a -> b) -> a -> b
$ \i -> x
p -> i -> x
p i
bothZero x -> x -> x
forall a. MultiplicativeSemigroup a => a -> a -> a
* i -> x
p i
f2

                i
z1' <- ClosedPoly i a -> m i
forall var a w (m :: Type -> Type).
MonadCircuit var a w m =>
ClosedPoly var a -> m var
newAssigned (ClosedPoly i a -> m i) -> ClosedPoly i a -> m i
forall a b. (a -> b) -> a -> b
$ \i -> x
p -> i -> x
p i
z1 x -> x -> x
forall a. AdditiveSemigroup a => a -> a -> a
+ i -> x
p i
f1z
                i
z2' <- ClosedPoly i a -> m i
forall var a w (m :: Type -> Type).
MonadCircuit var a w m =>
ClosedPoly var a -> m var
newAssigned (ClosedPoly i a -> m i) -> ClosedPoly i a -> m i
forall a b. (a -> b) -> a -> b
$ \i -> x
p -> i -> x
p i
z2 x -> x -> x
forall a. AdditiveSemigroup a => a -> a -> a
+ i -> x
p i
f2z

                (i, i) -> m (i, i)
forall a. a -> m a
forall (m :: Type -> Type) a. Monad m => a -> m a
Haskell.return (i
z1', i
z2')