{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DerivingVia #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
module ZkFold.Symbolic.Data.Ord (Ord (..), Lexicographical (..), 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, symbolicF), symbolic2F)
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 (MonadCircuit, newAssigned, newRanged, rangeConstraint)
class Ord b a where
(<=) :: a -> a -> b
(<) :: a -> a -> b
(>=) :: a -> a -> b
(>) :: a -> a -> b
max :: a -> a -> a
min :: a -> a -> a
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
newtype Lexicographical a = Lexicographical a
deriving newtype instance SymbolicData a => SymbolicData (Lexicographical a)
instance
( Symbolic c
, SymbolicData x
, Context x ~ c
, Support x ~ Proxy c
, Representable (Layout x)
, Traversable (Layout x)
) => Ord (Bool c) (Lexicographical x) where
Lexicographical x
x <= :: Lexicographical x -> Lexicographical x -> Bool c
<= Lexicographical x
y = Lexicographical x
y Lexicographical x -> Lexicographical x -> Bool c
forall b a. Ord b a => a -> a -> b
>= Lexicographical x
x
Lexicographical x
x < :: Lexicographical x -> Lexicographical x -> Bool c
< Lexicographical x
y = Lexicographical x
y Lexicographical x -> Lexicographical x -> Bool c
forall b a. Ord b a => a -> a -> b
> Lexicographical x
x
Lexicographical x
x >= :: Lexicographical x -> Lexicographical x -> Bool c
>= Lexicographical x
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 (Lexicographical x -> c []
forall (c :: (Type -> Type) -> Type) x.
(Symbolic c, SymbolicData x, Context x ~ c, Support x ~ Proxy c,
Foldable (Layout x)) =>
x -> c []
getBitsBE Lexicographical x
x) (Lexicographical x -> c []
forall (c :: (Type -> Type) -> Type) x.
(Symbolic c, SymbolicData x, Context x ~ c, Support x ~ Proxy c,
Foldable (Layout x)) =>
x -> c []
getBitsBE Lexicographical x
y)
Lexicographical x
x > :: Lexicographical x -> Lexicographical x -> Bool c
> Lexicographical x
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 (Lexicographical x -> c []
forall (c :: (Type -> Type) -> Type) x.
(Symbolic c, SymbolicData x, Context x ~ c, Support x ~ Proxy c,
Foldable (Layout x)) =>
x -> c []
getBitsBE Lexicographical x
x) (Lexicographical x -> c []
forall (c :: (Type -> Type) -> Type) x.
(Symbolic c, SymbolicData x, Context x ~ c, Support x ~ Proxy c,
Foldable (Layout x)) =>
x -> c []
getBitsBE Lexicographical x
y)
max :: Lexicographical x -> Lexicographical x -> Lexicographical x
max Lexicographical x
x Lexicographical x
y = forall b a. Conditional b a => a -> a -> b -> a
bool @(Bool c) Lexicographical x
x Lexicographical x
y (Bool c -> Lexicographical x) -> Bool c -> Lexicographical x
forall a b. (a -> b) -> a -> b
$ Lexicographical x
x Lexicographical x -> Lexicographical x -> Bool c
forall b a. Ord b a => a -> a -> b
< Lexicographical x
y
min :: Lexicographical x -> Lexicographical x -> Lexicographical x
min Lexicographical x
x Lexicographical x
y = forall b a. Conditional b a => a -> a -> b -> a
bool @(Bool c) Lexicographical x
x Lexicographical x
y (Bool c -> Lexicographical x) -> Bool c -> Lexicographical x
forall a b. (a -> b) -> a -> b
$ Lexicographical x
x Lexicographical x -> Lexicographical x -> Bool c
forall b a. Ord b a => a -> a -> b
> Lexicographical x
y
getBitsBE ::
forall c x .
(Symbolic c, SymbolicData x, Context x ~ c, Support x ~ Proxy c, Foldable (Layout x)) =>
x -> c []
getBitsBE :: forall (c :: (Type -> Type) -> Type) x.
(Symbolic c, SymbolicData x, Context x ~ c, Support x ~ Proxy c,
Foldable (Layout x)) =>
x -> c []
getBitsBE x
x = c (Layout x)
-> (Layout x (BaseField c) -> [BaseField c])
-> CircuitFun (Layout x) [] (BaseField c)
-> c []
forall a (f :: Type -> Type) (g :: Type -> Type).
(BaseField c ~ a) =>
c f -> (f a -> g a) -> CircuitFun f g a -> c g
forall (c :: (Type -> Type) -> Type) a (f :: Type -> Type)
(g :: Type -> Type).
(Symbolic c, BaseField c ~ a) =>
c f -> (f a -> g a) -> CircuitFun f g a -> c g
symbolicF (x -> Support x -> Context x (Layout x)
forall x. SymbolicData x => x -> Support x -> Context x (Layout x)
pieces 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 (m :: Type -> Type).
(MonadCircuit i a 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
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}.
MonadCircuit i (BaseField c) m =>
f i -> f i -> m (Par1 i))
-> 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)
-> (forall i (m :: Type -> Type).
MonadCircuit i a m =>
f i -> g i -> m (h i))
-> 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}.
MonadCircuit i (BaseField c) m =>
f i -> f i -> m (Par1 i))
-> c Par1)
-> (forall {i} {m :: Type -> Type}.
MonadCircuit i (BaseField c) m =>
f i -> f i -> m (Par1 i))
-> 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 (m :: Type -> Type) (f :: Type -> Type).
(Arithmetic a, MonadCircuit i a 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 m f . (Arithmetic a, MonadCircuit i a m, Z.Zip f, Foldable f, KnownNat r) => f i -> f i -> m i
blueprintGE :: forall (r :: Nat) i a (m :: Type -> Type) (f :: Type -> Type).
(Arithmetic a, MonadCircuit i a 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 (m :: Type -> Type) (f :: Type -> Type).
(Arithmetic a, MonadCircuit i a 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 (m :: Type -> Type).
MonadCircuit var a 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
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}.
MonadCircuit i (BaseField c) m =>
f i -> f i -> m (Par1 i))
-> 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)
-> (forall i (m :: Type -> Type).
MonadCircuit i a m =>
f i -> g i -> m (h i))
-> 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}.
MonadCircuit i (BaseField c) m =>
f i -> f i -> m (Par1 i))
-> c Par1)
-> (forall {i} {m :: Type -> Type}.
MonadCircuit i (BaseField c) m =>
f i -> f i -> m (Par1 i))
-> 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 (m :: Type -> Type) (f :: Type -> Type).
(Arithmetic a, MonadCircuit i a 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 (m :: Type -> Type).
MonadCircuit var a 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))
circuitDelta :: forall r i a m f . (Arithmetic a, MonadCircuit i a m, Z.Zip f, Foldable f, KnownNat r) => f i -> f i -> m (i, i)
circuitDelta :: forall (r :: Nat) i a (m :: Type -> Type) (f :: Type -> Type).
(Arithmetic a, MonadCircuit i a 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 (m :: Type -> Type).
MonadCircuit var a m =>
ClosedPoly var a -> m var
newAssigned (x -> (i -> x) -> x
forall a b. a -> b -> a
Haskell.const x
forall a. AdditiveMonoid a => a
zero)
i
z2 <- ClosedPoly i a -> m i
forall var a (m :: Type -> Type).
MonadCircuit var a m =>
ClosedPoly var a -> m var
newAssigned (x -> (i -> x) -> x
forall a b. a -> b -> a
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
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
i
f1 <- a
-> (forall {x} {n}.
(Algebra a x, WitnessField n x) =>
(i -> x) -> x)
-> m i
forall var a (m :: Type -> Type).
MonadCircuit var a m =>
a -> Witness var a -> m var
newRanged a
forall a. MultiplicativeMonoid a => a
one ((forall {x} {n}. (Algebra a x, WitnessField n x) => (i -> x) -> x)
-> m i)
-> (forall {x} {n}.
(Algebra a x, WitnessField n x) =>
(i -> x) -> x)
-> m i
forall a b. (a -> b) -> a -> b
$
\i -> x
p -> let q :: x
q = n -> x
forall a b. FromConstant a b => a -> b
fromConstant (n -> x) -> n -> x
forall a b. (a -> b) -> a -> b
$ (x -> Const x
forall a. ToConstant a => a -> Const a
toConstant (i -> x
p i
y x -> x -> x
forall a. AdditiveSemigroup a => a -> a -> a
+ x
forall a. MultiplicativeMonoid a => a
one) n -> n -> n
forall a. SemiEuclidean a => a -> a -> a
`div` x -> Const x
forall a. ToConstant a => a -> Const a
toConstant (i -> x
p i
x x -> x -> x
forall a. AdditiveSemigroup a => a -> a -> a
+ x
forall a. MultiplicativeMonoid a => a
one))
in x
forall a. MultiplicativeMonoid a => a
one x -> x -> x
forall a. AdditiveGroup a => a -> a -> a
- x
q x -> x -> x
forall a. Field a => a -> a -> a
// x
q
i
f2 <- a
-> (forall {x} {n}.
(Algebra a x, WitnessField n x) =>
(i -> x) -> x)
-> m i
forall var a (m :: Type -> Type).
MonadCircuit var a m =>
a -> Witness var a -> m var
newRanged a
forall a. MultiplicativeMonoid a => a
one ((forall {x} {n}. (Algebra a x, WitnessField n x) => (i -> x) -> x)
-> m i)
-> (forall {x} {n}.
(Algebra a x, WitnessField n x) =>
(i -> x) -> x)
-> m i
forall a b. (a -> b) -> a -> b
$
\i -> x
p -> let q :: x
q = n -> x
forall a b. FromConstant a b => a -> b
fromConstant (n -> x) -> n -> x
forall a b. (a -> b) -> a -> b
$ (x -> Const x
forall a. ToConstant a => a -> Const a
toConstant (i -> x
p i
x x -> x -> x
forall a. AdditiveSemigroup a => a -> a -> a
+ x
forall a. MultiplicativeMonoid a => a
one) n -> n -> n
forall a. SemiEuclidean a => a -> a -> a
`div` x -> Const x
forall a. ToConstant a => a -> Const a
toConstant (i -> x
p i
y x -> x -> x
forall a. AdditiveSemigroup a => a -> a -> a
+ x
forall a. MultiplicativeMonoid a => a
one))
in x
forall a. MultiplicativeMonoid a => a
one x -> x -> x
forall a. AdditiveGroup a => a -> a -> a
- x
q x -> x -> x
forall a. Field a => a -> a -> a
// x
q
i
dxy <- ClosedPoly i a -> m i
forall var a (m :: Type -> Type).
MonadCircuit var a m =>
ClosedPoly var a -> m var
newAssigned (\i -> x
p -> i -> x
p i
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 (m :: Type -> Type).
MonadCircuit var a 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 (m :: Type -> Type).
MonadCircuit var a m =>
ClosedPoly var a -> m var
newAssigned (\i -> x
p -> (x
forall a. MultiplicativeMonoid a => a
one x -> x -> x
forall a. AdditiveGroup a => a -> a -> a
- i -> x
p i
f1) x -> x -> x
forall a. MultiplicativeSemigroup a => a -> a -> a
* (x -> x
forall a. AdditiveGroup a => a -> a
negate (x -> x) -> x -> x
forall a b. (a -> b) -> a -> b
$ i -> x
p i
dxy))
i -> a -> m ()
forall var a (m :: Type -> Type).
MonadCircuit var a m =>
var -> a -> m ()
rangeConstraint i
d1 a
bound
i -> a -> m ()
forall var a (m :: Type -> Type).
MonadCircuit var a m =>
var -> a -> m ()
rangeConstraint i
d1' a
bound
i
d2 <- ClosedPoly i a -> m i
forall var a (m :: Type -> Type).
MonadCircuit var a m =>
ClosedPoly var a -> m var
newAssigned (\i -> x
p -> i -> x
p i
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 (m :: Type -> Type).
MonadCircuit var a 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 (m :: Type -> Type).
MonadCircuit var a m =>
var -> a -> m ()
rangeConstraint i
d2 a
bound
i -> a -> m ()
forall var a (m :: Type -> Type).
MonadCircuit var a m =>
var -> a -> m ()
rangeConstraint i
d2' a
bound
i
bothZero <- ClosedPoly i a -> m i
forall var a (m :: Type -> Type).
MonadCircuit var a 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 (m :: Type -> Type).
MonadCircuit var a 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 (m :: Type -> Type).
MonadCircuit var a 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 (m :: Type -> Type).
MonadCircuit var a 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 (m :: Type -> Type).
MonadCircuit var a 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')