From 96b3a7f3239ff48a7d9ef6c11d6d0b2f94f56e73 Mon Sep 17 00:00:00 2001
From: Eitan Chatav <eitan.chatav@gmail.com>
Date: Fri, 12 Jul 2024 16:09:25 -0700
Subject: [PATCH 01/51] structured i/o

---
 src/ZkFold/Symbolic/Base/Circuit.hs    | 188 +++++++
 src/ZkFold/Symbolic/Base/Function.hs   |   3 +
 src/ZkFold/Symbolic/Base/Num.hs        | 714 +++++++++++++++++++++++++
 src/ZkFold/Symbolic/Base/Polynomial.hs | 162 ++++++
 src/ZkFold/Symbolic/Base/Vector.hs     | 249 +++++++++
 zkfold-base.cabal                      |   6 +
 6 files changed, 1322 insertions(+)
 create mode 100644 src/ZkFold/Symbolic/Base/Circuit.hs
 create mode 100644 src/ZkFold/Symbolic/Base/Function.hs
 create mode 100644 src/ZkFold/Symbolic/Base/Num.hs
 create mode 100644 src/ZkFold/Symbolic/Base/Polynomial.hs
 create mode 100644 src/ZkFold/Symbolic/Base/Vector.hs

diff --git a/src/ZkFold/Symbolic/Base/Circuit.hs b/src/ZkFold/Symbolic/Base/Circuit.hs
new file mode 100644
index 000000000..29c4d3483
--- /dev/null
+++ b/src/ZkFold/Symbolic/Base/Circuit.hs
@@ -0,0 +1,188 @@
+{-# LANGUAGE
+AllowAmbiguousTypes
+, DerivingStrategies
+, DerivingVia
+, QuantifiedConstraints
+, RankNTypes
+, TypeOperators
+, UndecidableInstances
+#-}
+
+module ZkFold.Symbolic.Base.Circuit
+  ( Circuit (..)
+  , SysVar (..)
+  , OutVar (..)
+  , MonadCircuit (..)
+  , evalC
+  , idC
+  , applyC
+  ) where
+
+import Control.Applicative
+import Control.Category
+import Data.Either
+import Data.Eq
+import Data.Function (($))
+import Data.Functor
+import Data.IntMap (IntMap)
+import qualified Data.IntMap as IntMap
+import Data.Maybe
+import Data.Monoid
+import Data.Ord
+import Data.Semigroup
+import Data.Set (Set)
+import qualified Data.Set as Set
+import Data.Type.Equality
+
+import ZkFold.Symbolic.Base.Num
+import ZkFold.Symbolic.Base.Polynomial
+import ZkFold.Symbolic.Base.Vector
+
+data Circuit x i o = Circuit
+  { systemC :: Set (Poly (SysVar x i) Natural x)
+    -- ^ The system of polynomial constraints,
+    -- each polynomial constitutes a "multi-edge" of the circuit graph,
+    -- whose "vertices" are variables.
+    -- Polynomials constrain input variables and new variables.
+    -- Constant variables are absorbed into the polynomial coefficients.
+  , witnessC :: IntMap (i x -> x)
+    -- ^ The witness generation map,
+    -- witness functions for new variables.
+    -- Input and constant variables don't need witness functions.
+  , outputC :: o (OutVar x i)
+    -- ^ The output variables,
+    -- they can be input, constant or new variables.
+  }
+
+data SysVar x i
+  = InVar (Basis x i)
+  | NewVar Int
+deriving stock instance Eq (Basis x i) => Eq (SysVar x i)
+deriving stock instance Ord (Basis x i) => Ord (SysVar x i)
+
+data OutVar x i
+  = SysVar (SysVar x i)
+  | ConstVar x
+deriving stock instance (Eq x, Eq (Basis x i)) => Eq (OutVar x i)
+deriving stock instance (Ord x, Ord (Basis x i)) => Ord (OutVar x i)
+
+witnessIndex
+  :: VectorSpace x i
+  => i x -> IntMap (i x -> x) -> OutVar x i -> x
+witnessIndex inp witnessMap = \case
+  SysVar (InVar basisIx) -> indexV inp basisIx
+  SysVar (NewVar ix) -> fromMaybe zero (($ inp) <$> witnessMap IntMap.!? ix)
+  ConstVar x -> x
+
+instance (Ord x, VectorSpace x i, o ~ U1) => Monoid (Circuit x i o) where
+  mempty = Circuit mempty mempty U1
+instance (Ord x, VectorSpace x i, o ~ U1) => Semigroup (Circuit x i o) where
+  c0 <> c1 = Circuit
+    { systemC = systemC c0 <> systemC c1
+    , witnessC = witnessC c0 <> witnessC c1
+    , outputC = U1
+    }
+
+evalC :: (VectorSpace x i, Functor o) => Circuit x i o -> i x -> o x
+evalC c i = fmap (witnessIndex i (witnessC c)) (outputC c)
+
+applyC
+  :: (Ord x, Algebra x x, VectorSpace x i, VectorSpace x j, Functor o)
+  => i x -> Circuit x (i :*: j) o -> Circuit x j o
+applyC i c = c
+  { systemC = Set.map (mapPoly sysF) (systemC c)
+  , witnessC = fmap witF (witnessC c)
+  , outputC = fmap outF (outputC c)
+  } where
+      sysF = \case
+        InVar (Left bi) -> Left (indexV i bi)
+        InVar (Right bj) -> Right (InVar bj)
+        NewVar n -> Right (NewVar n)
+      witF f j = f (i :*: j)
+      outF = \case
+        SysVar (InVar (Left bi)) -> ConstVar (indexV i bi)
+        SysVar (InVar (Right bj)) -> SysVar (InVar bj)
+        SysVar (NewVar n) -> SysVar (NewVar n)
+        ConstVar x -> ConstVar x
+
+newInputC
+  :: (Ord x, Algebra x x, VectorSpace x i, VectorSpace x j, Functor o)
+  => Circuit x j o -> Circuit x (i :*: j) o
+newInputC c = c
+  { systemC = Set.map (mapPoly sysF) (systemC c)
+  , witnessC = fmap witF (witnessC c)
+  , outputC = fmap outF (outputC c)
+  } where
+    sysF = \case
+      InVar bj -> Right (InVar (Right bj))
+      NewVar n -> Right (NewVar n)
+    witF f (_ :*: j) = f j
+    outF = \case
+      SysVar (InVar bj) -> SysVar (InVar (Right bj))
+      SysVar (NewVar n) -> SysVar (NewVar n)
+      ConstVar k -> ConstVar k
+
+inputC :: forall x i. VectorSpace x i => i (OutVar x i)
+inputC = fmap (SysVar . InVar) (basisV @x)
+
+idC :: forall x i. (Ord x, VectorSpace x i) => Circuit x i i
+idC = mempty {outputC = inputC}
+
+class (forall i j. Functor (m i j))
+  => MonadCircuit x m | m -> x where
+    apply :: (VectorSpace x i, VectorSpace x j) => i x -> m (i :*: j) j ()
+    newInput :: (VectorSpace x i, VectorSpace x j) => m j (i :*: j) ()
+    return :: r -> m i i r
+    (>>=) :: m i j r -> (r -> m j k s) -> m i k s
+    (>>) :: m i j r -> m j k s -> m i k s
+    x >> y = x >>= \_ -> y
+    (<¢>) :: m i j (r -> s) -> m j k r -> m i k s
+    f <¢> x = f >>= (<$> x)
+    input :: VectorSpace x i => m i i (i (OutVar x i))
+    input = return (inputC @x)
+    eval :: (VectorSpace x i, Functor o) => m i i (o (OutVar x i)) -> i x -> o x
+    runCircuit :: VectorSpace x i => Circuit x i o -> m i i (o (OutVar x i))
+    constraint
+      :: VectorSpace x i
+      => (forall a. Algebra x a => (SysVar x i -> a) -> a)
+      -> m i i ()
+    newConstrained
+      :: VectorSpace x i
+      => (forall a. Algebra x a => (Int -> a) -> Int -> a)
+      -> ((Int -> x) -> x)
+      -> m i i (OutVar x i)
+
+newtype Blueprint x i j r = Blueprint
+  {runBlueprint :: Circuit x i U1 -> (r, Circuit x j U1)}
+  deriving Functor
+
+instance (Algebra x x, Ord x) => Applicative (Blueprint x i i) where
+  pure = return
+  (<*>) = (<¢>)
+
+instance (Algebra x x, Ord x) => MonadCircuit x (Blueprint x) where
+  return x = Blueprint $ \c -> (x,c)
+  m >>= f = Blueprint $ \c ->
+    let
+      (x, c') = runBlueprint m c
+    in
+      runBlueprint (f x) c'
+  apply i = Blueprint $ \c -> ((), applyC i c)
+  newInput = Blueprint $ \c -> ((), newInputC c)
+  eval x i = case runBlueprint x mempty of
+    (o, c) -> evalC (c {outputC = o}) i
+  runCircuit c = Blueprint $ \c' ->
+    (outputC c, c {outputC = U1} <> c')
+  constraint p = Blueprint $ \c ->
+    ((), c { systemC = Set.insert (p var) (systemC c) })
+  newConstrained p w = Blueprint $ \c ->
+    let
+      (maxIndex, _) = IntMap.findMax (witnessC c)
+      newIndex = maxIndex + 1
+      newWitness i = w (fromMaybe zero . ((($ i) <$> witnessC c) IntMap.!?))
+     in
+      ( SysVar (NewVar newIndex)
+      , c { systemC = Set.insert (p (var . NewVar) newIndex) (systemC c)
+          , witnessC = IntMap.insert newIndex newWitness (witnessC c)
+          }
+      )
diff --git a/src/ZkFold/Symbolic/Base/Function.hs b/src/ZkFold/Symbolic/Base/Function.hs
new file mode 100644
index 000000000..1e68cb99a
--- /dev/null
+++ b/src/ZkFold/Symbolic/Base/Function.hs
@@ -0,0 +1,3 @@
+module ZkFold.Symbolic.Base.Function
+  (
+  ) where
diff --git a/src/ZkFold/Symbolic/Base/Num.hs b/src/ZkFold/Symbolic/Base/Num.hs
new file mode 100644
index 000000000..1bfbed941
--- /dev/null
+++ b/src/ZkFold/Symbolic/Base/Num.hs
@@ -0,0 +1,714 @@
+{-# LANGUAGE
+AllowAmbiguousTypes
+, DerivingStrategies
+, MagicHash
+, TypeOperators
+, UndecidableInstances
+, UndecidableSuperClasses
+#-}
+
+module ZkFold.Symbolic.Base.Num
+  ( -- * Numeric types
+    Integer
+  , Natural
+  , Rational
+  , Int
+    -- * Arithmetic constraints
+  , Arithmetic
+  , PrimeField
+    -- * Algebraic constraints
+  , AdditiveMonoid (..)
+  , MultiplicativeMonoid (..)
+  , AdditiveGroup (..)
+  , MultiplicativeGroup (..)
+  , Semiring
+  , Ring
+  , Field
+  , Algebra
+  , Real
+  , SemiIntegral
+  , Integral
+  , Modular
+  , Euclidean (..)
+  , Discrete (..)
+  , Comparable (..)
+    -- * Algebraic inter-constraints
+  , From (..)
+  , Into (..)
+  , fromSemiIntegral
+  , Exponent (..), (^), (^^), (**)
+  , Scalar (..)
+    -- * Type level numbers
+  , KnownNat
+  , Prime
+  , Finite (..)
+  , FiniteChr (..)
+    -- * Numeric combinators
+  , sum
+  , product
+  , even
+  , odd
+  , knownNat
+  , order
+  , characteristic
+  , combineN
+  , combineZ
+  , evalMonoN
+  ) where
+
+import Control.Category
+import Control.Applicative
+import Data.Bool
+import Data.Eq
+import Data.Foldable hiding (product, sum, toList)
+import Data.Functor
+import Data.Kind
+import Data.Type.Bool
+import Data.Type.Equality
+import GHC.Exts (proxy#)
+import Data.Ord
+import Data.Ratio
+import GHC.TypeLits (ErrorMessage (..), TypeError)
+import GHC.TypeNats hiding (Mod)
+import qualified GHC.TypeNats as Type
+import qualified Prelude
+import Prelude (Int, Integer)
+
+-- Arithmetic algebras should include:
+-- PrimeField x => Arithmetic x x
+-- PrimeField x => Arithmetic x (i -> x)
+-- PrimeField x => Arithmetic x (Circuit x i Par1)
+type Arithmetic x a =
+  ( Algebra x a
+  , Comparable a
+  , FiniteChr a
+  , 3 <= Chr x
+  )
+
+-- Prime fields should only include:
+-- (SemiIntegral int, Prime p) => PrimeField (int `Mod` p)
+-- and newtypes of int `Mod` p.
+type PrimeField x =
+  ( Modular x
+  , Arithmetic x x
+  , Finite x
+  , Field x
+  , FiniteChr x
+  , Order x ~ Chr x
+  )
+
+class AdditiveMonoid a where
+  (+) :: a -> a -> a
+  zero :: a
+
+sum :: (Foldable t, AdditiveMonoid a) => t a -> a
+sum = foldl' (+) zero
+
+class AdditiveMonoid a => AdditiveGroup a where
+  negate :: a -> a
+  (-) :: a -> a -> a
+
+class MultiplicativeMonoid a where
+  (*) :: a -> a -> a
+  one :: a
+
+product :: (Foldable t, MultiplicativeMonoid a) => t a -> a
+product = foldl' (*) one
+
+class MultiplicativeMonoid a => MultiplicativeGroup a where
+  (/) :: a -> a -> a
+
+-- from @Natural is the unique homomorphism from the free Semiring
+-- from @Integer is the unique homomorphism from the free Ring
+-- from @Rational is the unique homomorphism from the free Field
+--
+-- prop> from . from = from
+-- prop> from @a @a = id
+class From x a where
+  from :: x -> a
+  default from :: x ~ a => x -> a
+  from = id
+
+type Semiring a =
+  ( AdditiveMonoid a
+  , MultiplicativeMonoid a
+  , From Natural a
+  , From a a
+  , Scalar Natural a
+  , Scalar a a
+  , Exponent Natural a
+  )
+
+type Ring a =
+  ( AdditiveGroup a
+  , MultiplicativeMonoid a
+  , From Natural a
+  , From Integer a
+  , From a a
+  , Scalar Natural a
+  , Scalar Integer a
+  , Scalar a a
+  , Exponent Natural a
+  )
+
+type Field a =
+  ( AdditiveGroup a
+  , MultiplicativeGroup a
+  , From Natural a
+  , From Integer a
+  , From Rational a
+  , From a a
+  , Scalar Natural a
+  , Scalar Integer a
+  , Scalar Rational a
+  , Scalar a a
+  , Exponent Natural a
+  , Exponent Integer a
+  )
+
+type Algebra x a = (Ring x, Ring a, From x a, Scalar x a)
+
+class Semiring a => Euclidean a where
+  diff :: a -> a -> a
+  divMod :: a -> a -> (a,a)
+  quotRem :: a -> a -> (a,a)
+  eea :: a -> a -> (a,a,a)
+  default eea :: SemiIntegral a => a -> a -> (a,a,a)
+  eea = xEuclid one zero zero one where
+    xEuclid x0 y0 x1 y1 u v
+      | v == zero = (u,x0,y0)
+      | otherwise =
+        let
+          (q , r) = u `divMod` v
+          x2 = x0 `diff` (q * x1)
+          y2 = y0 `diff` (q * y1)
+        in
+          xEuclid x1 y1 x2 y2 v r
+  gcd :: a -> a -> a
+  gcd a b = let (d,_,_) = eea a b in d
+
+  div :: a -> a -> a
+  div a b = let (divisor,_) = divMod a b in divisor
+
+  mod :: a -> a -> a
+  mod a b = let (_,modulus) = divMod a b in modulus
+
+even :: SemiIntegral a => a -> Bool
+even a = a `mod` (from @Natural 2) == zero
+
+odd :: SemiIntegral a => a -> Bool
+odd a = a `mod` (from @Natural 2) == one
+
+class Ring a => Discrete a where
+  dichotomy :: a -> a -> a
+  default dichotomy :: Eq a => a -> a -> a
+  dichotomy a b = if a == b then one else zero
+
+class Discrete a => Comparable a where
+  trichotomy :: a -> a -> a
+  default trichotomy :: Ord a => a -> a -> a
+  trichotomy a b = case compare a b of
+    LT -> negate one
+    EQ -> zero
+    GT -> one
+
+-- prop> to . from = id
+-- prop> to . to = to
+-- prop> to @a @a = id
+class Into y a where
+  to :: a -> y
+  default to :: y ~ a => a -> y
+  to = id
+
+-- e.g. `Rational`, `Integer`, `Natural`, `Zp p`
+type Real a = (Prelude.Ord a, Semiring a, Into Rational a)
+-- e.g. `Integer`, `Natural`, `Zp p`
+type SemiIntegral a = (Real a, Euclidean a, Into Integer a)
+-- e.g. `Integer`, `Zp p`
+type Integral a = (SemiIntegral a, Ring a)
+-- `Zp p` and its newtypes, also `Word8`, `Word16`, `Word32` and `Word64`
+type Modular a = (Integral a, Into Natural a)
+
+fromSemiIntegral :: (SemiIntegral a, From Integer b) => a -> b
+fromSemiIntegral = from . to @Integer
+
+-- Type level numbers ---------------------------------------------------------
+
+knownNat :: forall n. KnownNat n => Natural
+knownNat = natVal' (proxy# @n)
+
+class
+  ( KnownNat (Order a)
+  ) => Finite a where
+    type Order a :: Natural
+
+order :: forall a. Finite a => Natural
+order = knownNat @(Order a)
+
+class
+  ( KnownNat (Chr a)
+  , Semiring a
+  ) => FiniteChr a where
+    type Chr a :: Natural
+
+characteristic :: forall a. FiniteChr a => Natural
+characteristic = knownNat @(Chr a)
+
+-- Use orphan instances for large publicly verified primes
+class KnownNat p => Prime p
+-- Use this overlappable instance for small enough primes and testing
+instance {-# OVERLAPPABLE #-} (KnownNat p, KnownPrime p) => Prime p
+
+type family KnownPrime p where
+  KnownPrime p = If (IsPrime p) (() :: Constraint) (TypeError (NotPrimeError p))
+
+type NotPrimeError p =
+  'Text "Error: " ':<>: 'ShowType p ':<>: 'Text " is not a prime number."
+
+type family IsPrime p where
+  IsPrime 0 = 'False
+  IsPrime 1 = 'False
+  IsPrime 2 = 'True
+  IsPrime 3 = 'True
+  IsPrime n = NotDividesFromTo n 2 (AtLeastSqrt n)
+
+type family NotZero n where
+  NotZero 0 = 'False
+  NotZero n = 'True
+
+type family NotDividesFromTo dividend divisor0 divisor1 where
+  NotDividesFromTo dividend divisor divisor = NotZero (dividend `Type.Mod` divisor)
+  NotDividesFromTo dividend divisor0 divisor1 =
+    NotZero (dividend `Type.Mod` divisor0) && NotDividesFromTo dividend (divisor0 + 1) divisor1
+
+type family AtLeastSqrt n where
+  AtLeastSqrt 0 = 0
+  AtLeastSqrt n = 2 ^ (Log2 n `Div` 2 + 1)
+
+-- Rational -------------------------------------------------------------------
+
+instance AdditiveMonoid Rational where
+  (+) = (Prelude.+)
+  zero = 0
+
+instance AdditiveGroup Rational where
+  negate = Prelude.negate
+  (-) = (Prelude.-)
+
+instance MultiplicativeMonoid Rational where
+  (*) = (Prelude.*)
+  one = 1
+
+instance MultiplicativeGroup Rational where
+  (/) = (Prelude./)
+
+instance Scalar Natural Rational where
+  scale n q = to n * q
+  combine = combineN
+instance Scalar Integer Rational where
+  scale i q = to i * q
+  combine = combineZ
+instance Scalar Rational Rational where
+  scale = (*)
+  combine terms =
+    let
+      coefs = [c | (c,_) <- terms]
+      commonDenom :: Integer = product (fmap (denominator . to) coefs)
+      clearDenom c = (numerator c * commonDenom) `div` commonDenom
+      numerators = fmap (\(c,a) -> (clearDenom (to c), a)) terms
+    in
+      combine numerators / from commonDenom
+
+instance Exponent Natural Rational where
+  exponent = (Prelude.^)
+  evalMono = evalMonoN
+instance Exponent Integer Rational where
+  exponent = (Prelude.^^)
+  evalMono = evalMonoN . fmap absPow where
+    absPow (a,p) =
+      let
+        pZ = to @Integer p
+      in
+        if pZ >= 0
+        then (a, Prelude.fromIntegral pZ :: Natural)
+        else (one / a, Prelude.fromIntegral (negate pZ))
+
+instance From Rational Rational
+instance From Natural Rational where from = Prelude.fromIntegral
+instance From Integer Rational where from = Prelude.fromInteger
+instance Into Rational Rational
+
+instance Discrete Rational
+instance Comparable Rational
+
+-- Integer --------------------------------------------------------------------
+
+instance AdditiveMonoid Integer where
+  (+) = (Prelude.+)
+  zero = 0
+
+instance AdditiveGroup Integer where
+  negate = Prelude.negate
+  (-) = (Prelude.-)
+
+instance MultiplicativeMonoid Integer where
+  (*) = (Prelude.*)
+  one = 1
+
+instance Scalar Natural Integer where
+  scale n z = to n * z
+  combine = combineN
+instance Scalar Integer Integer where
+  scale = (*)
+  combine = combineZ
+
+instance Exponent Natural Integer where
+  exponent = (Prelude.^)
+  evalMono = evalMonoN
+
+instance From Integer Integer
+instance From Natural Integer where from = Prelude.fromIntegral
+instance Into Rational Integer where to = Prelude.toRational
+instance Into Integer Integer
+
+instance Discrete Integer
+instance Comparable Integer
+
+instance Euclidean Integer where
+  diff = (Prelude.-)
+  divMod = Prelude.divMod
+  quotRem = Prelude.quotRem
+
+-- Natural --------------------------------------------------------------------
+
+instance AdditiveMonoid Natural where
+  (+) = (Prelude.+)
+  zero = 0
+
+instance MultiplicativeMonoid Natural where
+  (*) = (Prelude.*)
+  one = 1
+
+instance Scalar Natural Natural where
+  scale = (*)
+  combine = combineN
+
+instance Exponent Natural Natural where
+  exponent = (Prelude.^)
+  evalMono = evalMonoN
+
+instance From Natural Natural
+instance Into Integer Natural where to = Prelude.toInteger
+instance Into Rational Natural where to = Prelude.toRational
+instance Into Natural Natural
+
+instance Euclidean Natural where
+  diff a b = case compare a b of
+    LT -> b Prelude.- a
+    EQ -> 0
+    GT -> a Prelude.- b
+  divMod = Prelude.divMod
+  quotRem = Prelude.quotRem
+
+-- Int ------------------------------------------------------------------------
+
+instance AdditiveMonoid Int where
+  (+) = (Prelude.+)
+  zero = 0
+
+instance AdditiveGroup Int where
+  negate = Prelude.negate
+  (-) = (Prelude.-)
+
+instance MultiplicativeMonoid Int where
+  (*) = (Prelude.*)
+  one = 1
+
+instance Scalar Natural Int where
+  scale n z = from n * z
+  combine = combineN
+instance Scalar Integer Int where
+  scale n z = from n * z
+  combine = combineZ
+instance Scalar Int Int where
+  scale = (*)
+  combine terms =
+    combineZ [(to @Integer c,x) | (c,x) <- terms]
+
+instance Exponent Natural Int where
+  exponent = (Prelude.^)
+  evalMono = evalMonoN
+
+instance From Int Int
+instance From Natural Int where from = Prelude.fromIntegral
+instance From Integer Int where from = Prelude.fromIntegral
+instance Into Rational Int where to = Prelude.toRational
+instance Into Integer Int where to = Prelude.fromIntegral
+instance Into Int Int
+
+instance Discrete Int
+instance Comparable Int
+
+instance Euclidean Int where
+  diff = (Prelude.-)
+  divMod = Prelude.divMod
+  quotRem = Prelude.quotRem
+
+-- Function -------------------------------------------------------------------
+
+instance {-# OVERLAPPING #-} Semiring a
+  => AdditiveMonoid (i -> a) where
+    zero = pure zero
+    (+) = liftA2 (+)
+
+instance Ring a => AdditiveGroup (i -> a) where
+  negate = fmap negate
+  (-) = liftA2 (-)
+
+instance MultiplicativeMonoid a => MultiplicativeMonoid (i -> a) where
+  one = pure one
+  (*) = liftA2 (*)
+
+instance (Scalar c a, Scalar c c, Scalar a a)
+  => Scalar (i -> c) (i -> a) where
+    scale c a i = scale (c i) (a i)
+    combine terms i = combine (fmap (\(c,f) -> (c i, f i)) terms)
+
+instance Semiring a => Scalar Natural (i -> a) where
+  scale c f = scale c . f
+  combine terms i = combine (fmap (\(c,f) -> (c, f i)) terms)
+
+instance (Semiring a, Scalar Integer a)
+  => Scalar Integer (i -> a) where
+    scale c f = scale c . f
+    combine terms i = combine (fmap (\(c,f) -> (c, f i)) terms)
+
+instance (Semiring a, Scalar Rational a)
+  => Scalar Rational (i -> a) where
+    scale c f = scale c . f
+    combine terms i = combine (fmap (\(c,f) -> (c, f i)) terms)
+
+instance (Exponent pow a) => Exponent pow (i -> a) where
+  exponent a p i = exponent (a i) p
+  evalMono factors i = evalMono (fmap (\(f,p) -> (f i, p)) factors)
+
+instance MultiplicativeGroup a => MultiplicativeGroup (i -> a) where
+  (/) = liftA2 (/)
+
+instance From Natural a => From Natural (i -> a) where
+  from = pure . from
+
+instance From Integer a => From Integer (i -> a) where
+  from = pure . from
+
+instance From Rational a => From Rational (i -> a) where
+  from = pure . from
+
+instance From (i -> a) (i -> a)
+
+instance Discrete a => Discrete (i -> a) where
+  dichotomy = liftA2 dichotomy
+
+instance Comparable a => Comparable (i -> a) where
+  trichotomy = liftA2 trichotomy
+
+-- Mod ------------------------------------------------------------------------
+newtype Mod int n = UnsafeMod {fromMod :: int}
+  deriving newtype (Eq, Ord, Prelude.Show)
+
+instance (SemiIntegral int, KnownNat n)
+  => AdditiveMonoid (Mod int n) where
+    a + b = from (to @Integer a + to b)
+    zero = UnsafeMod zero
+
+instance (SemiIntegral int, KnownNat n)
+  => AdditiveGroup (Mod int n) where
+    negate = from . negate . to @Integer
+    a - b = from (to @Integer a - to b)
+
+instance (SemiIntegral int, KnownNat n)
+  => MultiplicativeMonoid (Mod int n) where
+    a * b = from (to @Integer a * to b)
+    one = UnsafeMod one
+
+instance (SemiIntegral int, Prime p)
+  => MultiplicativeGroup (Mod int p) where
+    a / b = case eea (to @Integer a) (to b) of
+      (_,q,_) -> from q
+
+instance (SemiIntegral int, KnownNat n)
+  => Euclidean (Mod int n) where
+    diff a b = from (diff (to @Natural a) (to b))
+    divMod a b = case divMod (to @Natural a) (to b) of
+      (d,m) -> (from d, from m)
+    quotRem a b = case quotRem (to @Natural a) (to b) of
+      (q,r) -> (from q, from r)
+
+residue :: forall n int. (Euclidean int, KnownNat n) => int -> int
+residue int = int `mod` from (knownNat @n)
+
+instance From (Mod int n) (Mod int n) where from = id
+
+instance (Euclidean int, KnownNat n) => From int (Mod int n) where
+  from int = UnsafeMod (residue @n int)
+
+instance (From Natural int, Euclidean int, KnownNat n)
+  => From Natural (Mod int n) where
+    from nat = UnsafeMod (residue @n (from nat))
+
+instance (SemiIntegral int, KnownNat n)
+  => From Integer (Mod int n) where
+    from int =
+      let
+        r = residue @n (to @Integer int)
+        n = from (knownNat @n)
+        zToN = from @Natural . Prelude.fromIntegral
+      in
+        case compare r zero of
+          LT -> zToN (n + r)
+          EQ -> zero
+          GT -> zToN (n - r)
+
+instance (SemiIntegral int, Prime p)
+  => From Rational (Mod int p) where
+    from q =
+      let
+        top = numerator q
+        bot = denominator q
+      in
+        from top / from bot
+
+instance Into (Mod int n) (Mod int n) where
+  to = id
+
+instance Into int (Mod int n) where
+  to = fromMod
+
+instance Into Rational int
+  => Into Rational (Mod int n) where
+    to = to . fromMod
+
+instance Into Integer int
+  => Into Integer (Mod int n) where
+    to = to . fromMod
+
+instance (SemiIntegral int, KnownNat n)
+  => Into Natural (Mod int n) where
+    to r =
+      let
+        int = to @Integer r
+        n = from (knownNat @n)
+        zToN = Prelude.fromIntegral
+      in
+        case compare int zero of
+          LT -> zToN (n + int)
+          EQ -> zero
+          GT -> zToN (n - int)
+
+instance (SemiIntegral int, KnownNat n)
+  => Scalar Natural (Mod int n) where
+    scale n z = from n * z
+    combine = combine . fmap (\(c,a) -> (from @_ @Natural c, a))
+instance (SemiIntegral int, KnownNat n)
+  => Scalar Integer (Mod int n) where
+    scale n z = from n * z
+    combine = combine . fmap (\(c,a) -> (from @_ @Integer c, a))
+instance (SemiIntegral int, Prime p)
+  => Scalar Rational (Mod int p) where
+    scale n z = from n * z
+    combine = combine . fmap (\(c,a) -> (from @_ @Rational c, a))
+instance (SemiIntegral int, KnownNat n)
+  => Scalar (Mod int n) (Mod int n) where
+    scale = (*)
+    combine = combineN . fmap (\(c,a) -> (to @Natural c, a))
+
+instance (SemiIntegral int, KnownNat n)
+  => Exponent Natural (Mod int n) where
+    exponent a q = exponent a (from @_ @(Mod int n) q)
+    evalMono = evalMono . fmap (\(a,q) -> (a,from @_ @(Mod int n) q))
+
+instance (SemiIntegral int, Prime p)
+  => Exponent Integer (Mod int p) where
+    exponent a q =
+      if q >= zero
+      then exponent a (from @_ @(Mod int p) q)
+      else one / exponent a (from @_ @(Mod int p) (negate q))
+    evalMono = evalMono . fmap absPow where
+      absPow (a,p) =
+        if p >= 0
+        then (a, from @_ @(Mod int p) p)
+        else (one / a, from (negate p))
+
+instance (SemiIntegral int, KnownNat n)
+  => Exponent (Mod int n) (Mod int n) where
+    exponent a q = from (to @Natural a ^ to @Natural q)
+    evalMono
+      = from
+      . evalMono
+      . fmap (\(a,q) -> (to @Natural a, to @Natural q))
+
+instance (SemiIntegral int, KnownNat n) => Discrete (Mod int n)
+instance (SemiIntegral int, KnownNat n) => Comparable (Mod int n)
+
+-- Scalar ------------------------------------------------------------------
+class (Semiring c, AdditiveMonoid a)
+  => Scalar c a where
+    scale :: c -> a -> a
+    default scale :: c ~ a => c -> a -> a
+    scale = (*)
+    combine :: [(c,a)] -> a
+    default combine :: c ~ a => [(c,a)] -> a
+    combine = product . fmap (Prelude.uncurry (*))
+
+combineN
+  :: (Into Natural c, AdditiveMonoid a)
+  => [(c,a)] -> a
+combineN combination = combineNat naturalized where
+  naturalized = [(to @Natural c, a) | (c,a) <- combination]
+  combineNat [] = zero
+  combineNat terms =
+    let
+      halves = combineNat [(c `div` 2, a) | (c,a) <- terms, c > 1]
+      halveNots = sum [a | (c,a) <- terms, Prelude.odd c]
+    in
+      halves + halves + halveNots
+
+combineZ
+  :: (Into Integer c, AdditiveGroup a)
+  => [(c,a)] -> a
+combineZ = combineN . fmap absCoeff where
+  absCoeff (c,a) =
+    let
+      cZ = to @Integer c
+    in
+      if cZ >= 0
+      then (Prelude.fromIntegral cZ :: Natural, a)
+      else (Prelude.fromIntegral (negate cZ), negate a)
+
+-- Exponent -------------------------------------------------------------------
+class (Semiring pow, MultiplicativeMonoid a)
+  => Exponent pow a where
+    exponent :: a -> pow -> a
+    evalMono :: [(a,pow)] -> a
+
+(^) :: (Exponent Natural a, Into Natural pow) => a -> pow -> a
+a ^ b = exponent @Natural a (to b)
+
+(^^) :: (Exponent Integer a, Into Integer pow) => a -> pow -> a
+a ^^ b = exponent @Integer a (to b)
+
+(**) :: (Exponent Rational a, Into Rational pow) => a -> pow -> a
+a ** b = exponent @Rational a (to b)
+
+evalMonoN
+  :: (Into Natural p, MultiplicativeMonoid a)
+  => [(a,p)] -> a
+evalMonoN monomial = evalMonoNat naturalized where
+  naturalized = [(a, to @Natural p) | (a,p) <- monomial]
+  evalMonoNat [] = one
+  evalMonoNat factors =
+    let
+      sqrts = evalMonoNat [(a,p `div` 2) | (a,p) <- factors, p > 1]
+      sqrtNots = product [a | (a,p) <- factors, Prelude.odd p]
+    in
+      sqrts * sqrts * sqrtNots
diff --git a/src/ZkFold/Symbolic/Base/Polynomial.hs b/src/ZkFold/Symbolic/Base/Polynomial.hs
new file mode 100644
index 000000000..aad151711
--- /dev/null
+++ b/src/ZkFold/Symbolic/Base/Polynomial.hs
@@ -0,0 +1,162 @@
+{-# LANGUAGE
+AllowAmbiguousTypes
+, DerivingStrategies
+, TypeOperators
+, UndecidableInstances
+, UndecidableSuperClasses
+#-}
+
+module ZkFold.Symbolic.Base.Polynomial
+  ( Poly
+  , Mono (..), mono
+  , Combo (..), combo
+  , var
+  , varSet
+  , evalPoly
+  , mapPoly
+  ) where
+
+import Control.Category
+import Data.Eq
+import Data.Ord
+import Data.Either
+import Data.Foldable hiding (toList, sum, product)
+import Data.Functor
+import Data.Map.Strict (Map)
+import qualified Data.Map.Strict as Map
+import Data.Set (Set)
+import qualified Data.Set as Set
+import qualified Prelude
+import GHC.IsList
+import GHC.TypeNats
+
+import ZkFold.Symbolic.Base.Num
+
+newtype Mono var pow = UnsafeMono {fromMono :: Map var pow}
+  deriving (Eq, Ord, Functor)
+
+mono :: (AdditiveMonoid pow, Eq pow) => Map var pow -> Mono var pow
+mono = UnsafeMono . Map.filter (/= zero)
+
+instance (Ord var, AdditiveMonoid pow, Eq pow)
+  => IsList (Mono var pow) where
+    type Item (Mono var pow) = (var,pow)
+    toList (UnsafeMono m) = toList m
+    fromList l =
+      let
+        inserter m (v, pow) = Map.insertWith (+) v pow m
+      in
+        mono (foldl' inserter Map.empty l)
+
+instance (Ord var, Semiring pow, Eq pow)
+  => MultiplicativeMonoid (Mono var pow) where
+    one = UnsafeMono Map.empty
+    UnsafeMono x * UnsafeMono y = mono (Map.unionWith (+) x y)
+
+instance (Ord var, Semiring pow, Ord pow)
+  => Exponent Natural (Mono var pow) where
+    exponent a p = evalMono [(a,p)]
+    evalMono = evalMonoN
+
+newtype Combo var coef = UnsafeCombo {fromCombo :: Map var coef}
+  deriving (Eq, Ord, Functor)
+
+combo :: (AdditiveMonoid coef, Eq coef) => Map var coef -> Combo var coef
+combo = UnsafeCombo . Map.filter (/= zero)
+
+instance (Ord var, Semiring coef, Eq coef)
+  => AdditiveMonoid (Combo var coef) where
+    zero = UnsafeCombo Map.empty
+    UnsafeCombo x + UnsafeCombo y = combo (Map.unionWith (+) x y)
+
+instance (Ord var, Ring coef, Eq coef)
+  => AdditiveGroup (Combo var coef) where
+    negate (UnsafeCombo x) = UnsafeCombo (Map.map negate x)
+    UnsafeCombo x - UnsafeCombo y = combo (Map.unionWith (-) x y)
+
+instance (Ord var, AdditiveMonoid coef, Eq coef)
+  => IsList (Combo var coef) where
+    type Item (Combo var coef) = (coef,var)
+    toList (UnsafeCombo m) = [(c,v) | (v,c) <- toList m]
+    fromList l =
+      let
+        inserter m (c,v) = Map.insertWith (+) v c m
+      in
+        combo (foldl' inserter Map.empty l)
+
+type Poly var pow = Combo (Mono var pow)
+instance (Ord var, Ord pow, Semiring pow, Semiring coef, Eq coef)
+  => From coef (Poly var pow coef) where
+    from coef = fromList [(coef,one)]
+instance (Ord var, Ord pow, Semiring pow, Semiring coef, Eq coef)
+  => From Natural (Poly var pow coef) where
+    from = from @coef . from
+instance (Ord var, Ord pow, Semiring pow, Ring coef, Eq coef)
+  => From Integer (Poly var pow coef) where
+    from = from @coef . from
+instance (Ord var, Ord pow, Semiring pow, Field coef, Eq coef)
+  => From Rational (Poly var pow coef) where
+    from = from @coef . from
+instance From (Poly var pow coef) (Poly var pow coef)
+instance (Ord var, Ord pow, Semiring pow, Semiring coef, Eq coef)
+  => MultiplicativeMonoid (Poly var pow coef) where
+    one = fromList [(one, one)]
+    x * y = fromList
+      [ (xCoef * yCoef, xMono * yMono)
+      | (xCoef, xMono) <- toList x
+      , (yCoef, yMono) <- toList y
+      ]
+instance (Ord var, Ord pow, Semiring pow, Semiring coef, Ord coef)
+  => Exponent Natural (Poly var pow coef) where
+    exponent x p = evalMono [(x,p)]
+    evalMono = evalMonoN
+instance (Ord var, Ord pow, Semiring pow, Semiring x, Eq x)
+  => Scalar x (Poly var pow x) where
+    scale c = if c == zero then Prelude.const zero else fmap (c *)
+    combine polys = product [scale c p | (c,p) <- polys]
+    -- TODO: consider how to optimize combine
+    -- using an additional Scalar x x constraint
+    -- since then we can hopefully applicatively apply combine
+    -- to monomials...
+instance (Ord var, Ord pow, Semiring x, Eq x)
+  => Scalar Natural (Poly var pow x) where
+    scale c = if c == zero then Prelude.const zero else fmap (from c *)
+    combine = combineN
+instance (Ord var, Ord pow, Ring x, Eq x)
+  => Scalar Integer (Poly var pow x) where
+    scale c = if c == zero then Prelude.const zero else fmap (from c *)
+    combine = combineZ
+instance (Ord var, Ord pow, Semiring pow, Semiring x, Ord x)
+  => Scalar (Poly var pow x) (Poly var pow x)
+
+var
+  :: (Ord var, Ord pow, Semiring pow, Semiring coef, Eq coef)
+  => var -> Poly var pow coef
+var x = fromList [(one, fromList [(x,one)])]
+
+varSet :: Ord var => Poly var pow coef -> Set var
+varSet
+  = Set.unions
+  . Set.map (Map.keysSet . fromMono)
+  . Map.keysSet
+  . fromCombo
+
+-- evaluate a polynomial in its field of coefficients
+evalPoly :: (Ord x, Semiring x) => Poly x Natural x -> x
+evalPoly x = combine [(c, evalMono (toList m)) | (c,m) <- toList x]
+
+-- map a polynomial to new variables and evaluate some variables
+mapPoly
+  :: (Eq x, Ord var0, Ord var1, Semiring x)
+  => (var0 -> Either x var1)
+  -> Poly var0 Natural x -> Poly var1 Natural x
+mapPoly f varPoly = fromList
+  [
+    let
+      (coefs, varList) = partitionEithers
+        [(,p) <$> f v0 | (v0,p) <- toList varMono]
+    in
+      (c * product coefs, fromList varList)
+
+  | (c, varMono) <- toList varPoly
+  ]
diff --git a/src/ZkFold/Symbolic/Base/Vector.hs b/src/ZkFold/Symbolic/Base/Vector.hs
new file mode 100644
index 000000000..6bf0d8ce1
--- /dev/null
+++ b/src/ZkFold/Symbolic/Base/Vector.hs
@@ -0,0 +1,249 @@
+
+{-# LANGUAGE AllowAmbiguousTypes  #-}
+{-# LANGUAGE DerivingStrategies   #-}
+{-# LANGUAGE DerivingVia          #-}
+{-# LANGUAGE TypeOperators        #-}
+{-# LANGUAGE QuantifiedConstraints, UndecidableInstances, UndecidableSuperClasses #-}
+
+module ZkFold.Symbolic.Base.Vector
+  ( -- * VectorSpace
+    VectorSpace (..)
+    -- * Vector types
+  , Vector (..)
+  , SparseV (..), sparseV
+  , Gen.U1 (..)
+  , Gen.Par1 (..)
+  , (Gen.:*:) (..)
+  , (Gen.:.:) (..)
+    -- * Structure combinators
+  , constV
+  , zipWithV
+    -- * VectorSpace combinators
+  , zeroV
+  , addV
+  , subtractV
+  , negateV
+  , scaleV
+  , dotV
+  ) where
+
+import Control.Category
+import Control.Monad
+import Data.Bool
+import Data.Distributive
+import Data.Either
+import Data.Eq
+import Data.Ord
+import Data.Foldable hiding (sum)
+import Data.Function (const, ($))
+import Data.Functor
+import Data.Functor.Rep
+import Data.Traversable
+import Data.Kind (Type)
+import Data.IntMap (IntMap)
+import qualified Data.IntMap as IntMap
+import Data.Maybe
+import Data.Type.Equality
+import qualified Data.Vector as V
+import Data.Void
+import qualified GHC.Generics as Gen
+import qualified Prelude
+
+import ZkFold.Symbolic.Base.Num
+
+{- |
+Class of vector spaces with a basis.
+
+`VectorSpace` is a known sized "monorepresentable" class,
+similar to `Representable` plus `Traversable`,
+but with a fixed element type that is a `Field`.
+
+A "vector" in a `VectorSpace` can be thought of as a
+tuple of numbers @(x1,..,xn)@.
+-}
+class
+  ( Field a
+  , Traversable v
+  , Eq (Basis a v)
+  , Ord (Basis a v)
+  ) => VectorSpace a v where
+    {- | The `Basis` for a `VectorSpace`. More accurately,
+    `Basis` will be a spanning set with "out-of-bounds"
+    basis elements corresponding with zero.
+    -}
+
+    type Basis a v :: Type
+    type Basis a v = Basis a (Gen.Rep1 v)
+
+    tabulateV :: (Basis a v -> a) -> v a
+    default tabulateV
+      :: ( Gen.Generic1 v
+         , VectorSpace a (Gen.Rep1 v)
+         , Basis a v ~ Basis a (Gen.Rep1 v)
+         )
+      => (Basis a v -> a) -> v a
+    tabulateV = Gen.to1 . tabulateV
+
+    indexV :: v a -> Basis a v -> a
+    default indexV
+      :: ( Gen.Generic1 v
+         , VectorSpace a (Gen.Rep1 v)
+         , Basis a v ~ Basis a (Gen.Rep1 v)
+         )
+      => v a -> Basis a v -> a
+    indexV = indexV . Gen.from1
+
+    dimV :: Natural
+    default dimV :: VectorSpace a (Gen.Rep1 v) => Natural
+    dimV = dimV @a @(Gen.Rep1 v)
+
+    basisV :: v (Basis a v)
+    default basisV
+      :: ( Gen.Generic1 v
+         , VectorSpace a (Gen.Rep1 v)
+         , Basis a v ~ Basis a (Gen.Rep1 v)
+         )
+      => v (Basis a v)
+    basisV = Gen.to1 (basisV @a @(Gen.Rep1 v))
+
+constV :: VectorSpace a v => a -> v a
+constV = tabulateV . const
+
+zipWithV :: VectorSpace a v => (a -> a -> a) -> v a -> v a -> v a
+zipWithV f as bs = tabulateV $ \k ->
+  f (indexV as k) (indexV bs k)
+
+zeroV :: VectorSpace a v => v a
+zeroV = constV zero
+
+addV :: VectorSpace a v => v a -> v a -> v a
+addV = zipWithV (+)
+
+subtractV :: VectorSpace a v => v a -> v a -> v a
+subtractV = zipWithV (-)
+
+negateV :: VectorSpace a v => v a -> v a
+negateV = fmap negate
+
+scaleV :: VectorSpace a v => a -> v a -> v a
+scaleV c = fmap (c *)
+
+-- | dot product
+dotV :: VectorSpace a v => v a -> v a -> a
+v `dotV` w = sum (zipWithV (*) v w)
+
+-- generic vector space
+instance VectorSpace a v
+  => VectorSpace a (Gen.M1 i c v) where
+    type Basis a (Gen.M1 i c v) = Basis a v
+    indexV (Gen.M1 v) = indexV v
+    tabulateV f = Gen.M1 (tabulateV f)
+    dimV = dimV @a @v
+    basisV = Gen.M1 (basisV @a @v)
+
+-- zero dimensional vector space
+instance Field a => VectorSpace a Gen.U1 where
+  type Basis a Gen.U1 = Void
+  tabulateV = tabulate
+  indexV = index
+  dimV = zero
+  basisV = Gen.U1
+
+-- one dimensional vector space
+instance Field a => VectorSpace a Gen.Par1 where
+  type Basis a Gen.Par1 = ()
+  tabulateV = tabulate
+  indexV = index
+  dimV = one
+  basisV = Gen.Par1 ()
+
+-- direct sum of vector spaces
+instance (VectorSpace a v, VectorSpace a u)
+  => VectorSpace a (v Gen.:*: u) where
+    type Basis a (v Gen.:*: u) = Either (Basis a v) (Basis a u)
+    tabulateV f = tabulateV (f . Left) Gen.:*: tabulateV (f . Right)
+    indexV (a Gen.:*: _) (Left  i) = indexV a i
+    indexV (_ Gen.:*: b) (Right j) = indexV b j
+    dimV = dimV @a @v + dimV @a @u
+    basisV = fmap Left (basisV @a @v) Gen.:*: fmap Right (basisV @a @u)
+
+-- tensor product of vector spaces
+instance
+  ( VectorSpace a v
+  , VectorSpace a u
+  , Representable v
+  , Basis a v ~ Rep v
+  ) => VectorSpace a (v Gen.:.: u) where
+    type Basis a (v Gen.:.: u) = (Basis a v, Basis a u)
+    tabulateV = Gen.Comp1 . tabulate . fmap tabulateV . Prelude.curry
+    indexV (Gen.Comp1 fg) (i, j) = indexV (index fg i) j
+    dimV = dimV @a @v * dimV @a @u
+    basisV = Gen.Comp1
+      (basisV @a @v <&> \bv -> basisV @a @u <&> \bu -> (bv,bu))
+
+-- | concrete vectors
+newtype Vector (n :: Natural) a = UnsafeV (V.Vector a)
+  deriving stock
+    (Functor, Foldable, Traversable, Eq, Ord)
+
+instance (KnownNat n, Prelude.Show a)
+  => Prelude.Show (Vector n a) where
+    showsPrec d v
+      = Prelude.showParen (d > 10)
+      $ Prelude.showString "fromV "
+      . Prelude.showsPrec 11 (toList v)
+
+instance KnownNat n => Representable (Vector n) where
+  type Rep (Vector n) = Prelude.Int
+  index (UnsafeV v) i = v V.! i
+  tabulate = UnsafeV . V.generate (from (knownNat @n))
+
+instance KnownNat n => Distributive (Vector n) where
+  distribute = distributeRep
+  collect = collectRep
+
+instance (Field a, KnownNat n) => VectorSpace a (Vector n) where
+  type Basis a (Vector n) = Prelude.Int
+  indexV (UnsafeV v) i = fromMaybe zero (v V.!? i)
+  tabulateV = tabulate
+  dimV = knownNat @n
+  basisV = tabulate id
+
+-- | sparse vectors
+newtype SparseV (n :: Natural) a =
+  UnsafeSparseV {fromSparseV :: IntMap a}
+    deriving stock
+      (Functor, Traversable, Eq, Ord)
+
+instance Foldable (SparseV n) where
+  foldMap f v = foldMap f (fromSparseV v)
+  toList _ = Prelude.error "toList @(SparseV _) is an error, use `toListV`."
+
+instance Prelude.Show a => Prelude.Show (SparseV n a) where
+  showsPrec d v
+    = Prelude.showParen (d > 10)
+    $ Prelude.showString "sparseV "
+    . Prelude.showsPrec 11 (fromSparseV v)
+
+sparseV :: forall a n. (Eq a, Field a, KnownNat n) => IntMap a -> SparseV n a
+sparseV intMap = UnsafeSparseV (IntMap.foldMapWithKey sparsify intMap) where
+  sparsify int a =
+    if a == zero || int < 0 || int >= from (knownNat @n)
+    then IntMap.empty
+    else IntMap.singleton int a
+
+instance (Eq a, Field a, KnownNat n) => VectorSpace a (SparseV n) where
+  type Basis a (SparseV n) = Prelude.Int
+  indexV v i = fromMaybe zero (fromSparseV v IntMap.!? i)
+  tabulateV f = UnsafeSparseV $
+    IntMap.fromList
+      [ (i, f i)
+      | i <- [0 .. from (knownNat @n) - 1]
+      , f i /= zero
+      ]
+  dimV = knownNat @n
+  basisV = UnsafeSparseV $
+    IntMap.fromList
+      [ (i, i)
+      | i <- [0 .. from (knownNat @n) - 1]
+      ]
diff --git a/zkfold-base.cabal b/zkfold-base.cabal
index 2d59a9a58..4eeabca95 100644
--- a/zkfold-base.cabal
+++ b/zkfold-base.cabal
@@ -125,6 +125,11 @@ library
       ZkFold.Symbolic.Algorithms.Hash.MiMC.Constants
       ZkFold.Symbolic.Algorithms.Hash.SHA2
       ZkFold.Symbolic.Algorithms.Hash.SHA2.Constants
+      ZkFold.Symbolic.Base.Circuit
+      ZkFold.Symbolic.Base.Function
+      ZkFold.Symbolic.Base.Num
+      ZkFold.Symbolic.Base.Polynomial
+      ZkFold.Symbolic.Base.Vector
       ZkFold.Symbolic.Cardano.Wrapper
       ZkFold.Symbolic.Cardano.Contracts.BatchTransfer
       ZkFold.Symbolic.Cardano.Contracts.RandomOracle
@@ -194,6 +199,7 @@ library
       containers                            < 0.7,
       cryptohash-sha256                    < 0.12,
       deepseq                          <= 1.5.0.0,
+      distributive                          < 0.7,
       mtl                                   < 2.4,
       optics                                < 0.5,
       parallel                          < 3.2.3.0,

From 6ca0fc5654b10d22d2c05fb35467b6ab8ccdbbfe Mon Sep 17 00:00:00 2001
From: Eitan Chatav <eitan.chatav@gmail.com>
Date: Fri, 12 Jul 2024 16:23:31 -0700
Subject: [PATCH 02/51] Update Polynomial.hs

---
 src/ZkFold/Symbolic/Base/Polynomial.hs | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/ZkFold/Symbolic/Base/Polynomial.hs b/src/ZkFold/Symbolic/Base/Polynomial.hs
index aad151711..a399cc348 100644
--- a/src/ZkFold/Symbolic/Base/Polynomial.hs
+++ b/src/ZkFold/Symbolic/Base/Polynomial.hs
@@ -17,6 +17,7 @@ module ZkFold.Symbolic.Base.Polynomial
   ) where
 
 import Control.Category
+import Data.Bifunctor
 import Data.Eq
 import Data.Ord
 import Data.Either
@@ -154,9 +155,8 @@ mapPoly f varPoly = fromList
   [
     let
       (coefs, varList) = partitionEithers
-        [(,p) <$> f v0 | (v0,p) <- toList varMono]
+        [bimap (^p) (,p) (f v0) | (v0,p) <- toList varMono]
     in
       (c * product coefs, fromList varList)
-
   | (c, varMono) <- toList varPoly
   ]

From cfceca4c2512bf437d11028668a398091a4a4ee5 Mon Sep 17 00:00:00 2001
From: Eitan Chatav <eitan.chatav@gmail.com>
Date: Fri, 12 Jul 2024 16:25:00 -0700
Subject: [PATCH 03/51] Update Vector.hs

---
 src/ZkFold/Symbolic/Base/Vector.hs | 1 -
 1 file changed, 1 deletion(-)

diff --git a/src/ZkFold/Symbolic/Base/Vector.hs b/src/ZkFold/Symbolic/Base/Vector.hs
index 6bf0d8ce1..25eec7bef 100644
--- a/src/ZkFold/Symbolic/Base/Vector.hs
+++ b/src/ZkFold/Symbolic/Base/Vector.hs
@@ -1,4 +1,3 @@
-
 {-# LANGUAGE AllowAmbiguousTypes  #-}
 {-# LANGUAGE DerivingStrategies   #-}
 {-# LANGUAGE DerivingVia          #-}

From c34460fad9692576962d447d1c3d9afae97ed4df Mon Sep 17 00:00:00 2001
From: Eitan Chatav <eitan.chatav@gmail.com>
Date: Fri, 12 Jul 2024 16:28:21 -0700
Subject: [PATCH 04/51] Update Vector.hs

---
 src/ZkFold/Symbolic/Base/Vector.hs | 1 -
 1 file changed, 1 deletion(-)

diff --git a/src/ZkFold/Symbolic/Base/Vector.hs b/src/ZkFold/Symbolic/Base/Vector.hs
index 25eec7bef..4b94b5ce0 100644
--- a/src/ZkFold/Symbolic/Base/Vector.hs
+++ b/src/ZkFold/Symbolic/Base/Vector.hs
@@ -63,7 +63,6 @@ tuple of numbers @(x1,..,xn)@.
 class
   ( Field a
   , Traversable v
-  , Eq (Basis a v)
   , Ord (Basis a v)
   ) => VectorSpace a v where
     {- | The `Basis` for a `VectorSpace`. More accurately,

From e66b5feef5d19b9a42efc309e9908ba5dbf63ab1 Mon Sep 17 00:00:00 2001
From: Eitan Chatav <eitan.chatav@gmail.com>
Date: Fri, 12 Jul 2024 16:37:51 -0700
Subject: [PATCH 05/51] Update Circuit.hs

---
 src/ZkFold/Symbolic/Base/Circuit.hs | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/src/ZkFold/Symbolic/Base/Circuit.hs b/src/ZkFold/Symbolic/Base/Circuit.hs
index 29c4d3483..ad1705594 100644
--- a/src/ZkFold/Symbolic/Base/Circuit.hs
+++ b/src/ZkFold/Symbolic/Base/Circuit.hs
@@ -57,14 +57,14 @@ data Circuit x i o = Circuit
 data SysVar x i
   = InVar (Basis x i)
   | NewVar Int
-deriving stock instance Eq (Basis x i) => Eq (SysVar x i)
-deriving stock instance Ord (Basis x i) => Ord (SysVar x i)
+deriving stock instance VectorSpace x i => Eq (SysVar x i)
+deriving stock instance VectorSpace x i => Ord (SysVar x i)
 
 data OutVar x i
   = SysVar (SysVar x i)
   | ConstVar x
-deriving stock instance (Eq x, Eq (Basis x i)) => Eq (OutVar x i)
-deriving stock instance (Ord x, Ord (Basis x i)) => Ord (OutVar x i)
+deriving stock instance (Eq x, VectorSpace x i) => Eq (OutVar x i)
+deriving stock instance (Ord x, VectorSpace x i) => Ord (OutVar x i)
 
 witnessIndex
   :: VectorSpace x i

From 7b4eb43107dd5ac8cba7f213ee59530f4560a97e Mon Sep 17 00:00:00 2001
From: echatav <echatav@users.noreply.github.com>
Date: Fri, 12 Jul 2024 23:52:49 +0000
Subject: [PATCH 06/51] stylish-haskell auto-commit

---
 src/ZkFold/Symbolic/Base/Circuit.hs    | 58 +++++++++++++-------------
 src/ZkFold/Symbolic/Base/Num.hs        | 46 ++++++++++----------
 src/ZkFold/Symbolic/Base/Polynomial.hs | 40 +++++++++---------
 src/ZkFold/Symbolic/Base/Vector.hs     | 54 ++++++++++++------------
 4 files changed, 97 insertions(+), 101 deletions(-)

diff --git a/src/ZkFold/Symbolic/Base/Circuit.hs b/src/ZkFold/Symbolic/Base/Circuit.hs
index ad1705594..5141ab081 100644
--- a/src/ZkFold/Symbolic/Base/Circuit.hs
+++ b/src/ZkFold/Symbolic/Base/Circuit.hs
@@ -1,12 +1,10 @@
-{-# LANGUAGE
-AllowAmbiguousTypes
-, DerivingStrategies
-, DerivingVia
-, QuantifiedConstraints
-, RankNTypes
-, TypeOperators
-, UndecidableInstances
-#-}
+{-# LANGUAGE AllowAmbiguousTypes   #-}
+{-# LANGUAGE DerivingStrategies    #-}
+{-# LANGUAGE DerivingVia           #-}
+{-# LANGUAGE QuantifiedConstraints #-}
+{-# LANGUAGE RankNTypes            #-}
+{-# LANGUAGE TypeOperators         #-}
+{-# LANGUAGE UndecidableInstances  #-}
 
 module ZkFold.Symbolic.Base.Circuit
   ( Circuit (..)
@@ -18,28 +16,28 @@ module ZkFold.Symbolic.Base.Circuit
   , applyC
   ) where
 
-import Control.Applicative
-import Control.Category
-import Data.Either
-import Data.Eq
-import Data.Function (($))
-import Data.Functor
-import Data.IntMap (IntMap)
-import qualified Data.IntMap as IntMap
-import Data.Maybe
-import Data.Monoid
-import Data.Ord
-import Data.Semigroup
-import Data.Set (Set)
-import qualified Data.Set as Set
-import Data.Type.Equality
-
-import ZkFold.Symbolic.Base.Num
-import ZkFold.Symbolic.Base.Polynomial
-import ZkFold.Symbolic.Base.Vector
+import           Control.Applicative
+import           Control.Category
+import           Data.Either
+import           Data.Eq
+import           Data.Function                   (($))
+import           Data.Functor
+import           Data.IntMap                     (IntMap)
+import qualified Data.IntMap                     as IntMap
+import           Data.Maybe
+import           Data.Monoid
+import           Data.Ord
+import           Data.Semigroup
+import           Data.Set                        (Set)
+import qualified Data.Set                        as Set
+import           Data.Type.Equality
+
+import           ZkFold.Symbolic.Base.Num
+import           ZkFold.Symbolic.Base.Polynomial
+import           ZkFold.Symbolic.Base.Vector
 
 data Circuit x i o = Circuit
-  { systemC :: Set (Poly (SysVar x i) Natural x)
+  { systemC  :: Set (Poly (SysVar x i) Natural x)
     -- ^ The system of polynomial constraints,
     -- each polynomial constitutes a "multi-edge" of the circuit graph,
     -- whose "vertices" are variables.
@@ -49,7 +47,7 @@ data Circuit x i o = Circuit
     -- ^ The witness generation map,
     -- witness functions for new variables.
     -- Input and constant variables don't need witness functions.
-  , outputC :: o (OutVar x i)
+  , outputC  :: o (OutVar x i)
     -- ^ The output variables,
     -- they can be input, constant or new variables.
   }
diff --git a/src/ZkFold/Symbolic/Base/Num.hs b/src/ZkFold/Symbolic/Base/Num.hs
index 1bfbed941..e80c02316 100644
--- a/src/ZkFold/Symbolic/Base/Num.hs
+++ b/src/ZkFold/Symbolic/Base/Num.hs
@@ -1,11 +1,9 @@
-{-# LANGUAGE
-AllowAmbiguousTypes
-, DerivingStrategies
-, MagicHash
-, TypeOperators
-, UndecidableInstances
-, UndecidableSuperClasses
-#-}
+{-# LANGUAGE AllowAmbiguousTypes     #-}
+{-# LANGUAGE DerivingStrategies      #-}
+{-# LANGUAGE MagicHash               #-}
+{-# LANGUAGE TypeOperators           #-}
+{-# LANGUAGE UndecidableInstances    #-}
+{-# LANGUAGE UndecidableSuperClasses #-}
 
 module ZkFold.Symbolic.Base.Num
   ( -- * Numeric types
@@ -56,23 +54,23 @@ module ZkFold.Symbolic.Base.Num
   , evalMonoN
   ) where
 
-import Control.Category
-import Control.Applicative
-import Data.Bool
-import Data.Eq
-import Data.Foldable hiding (product, sum, toList)
-import Data.Functor
-import Data.Kind
-import Data.Type.Bool
-import Data.Type.Equality
-import GHC.Exts (proxy#)
-import Data.Ord
-import Data.Ratio
-import GHC.TypeLits (ErrorMessage (..), TypeError)
-import GHC.TypeNats hiding (Mod)
-import qualified GHC.TypeNats as Type
+import           Control.Applicative
+import           Control.Category
+import           Data.Bool
+import           Data.Eq
+import           Data.Foldable       hiding (product, sum, toList)
+import           Data.Functor
+import           Data.Kind
+import           Data.Ord
+import           Data.Ratio
+import           Data.Type.Bool
+import           Data.Type.Equality
+import           GHC.Exts            (proxy#)
+import           GHC.TypeLits        (ErrorMessage (..), TypeError)
+import           GHC.TypeNats        hiding (Mod)
+import qualified GHC.TypeNats        as Type
+import           Prelude             (Int, Integer)
 import qualified Prelude
-import Prelude (Int, Integer)
 
 -- Arithmetic algebras should include:
 -- PrimeField x => Arithmetic x x
diff --git a/src/ZkFold/Symbolic/Base/Polynomial.hs b/src/ZkFold/Symbolic/Base/Polynomial.hs
index a399cc348..2aa9902e4 100644
--- a/src/ZkFold/Symbolic/Base/Polynomial.hs
+++ b/src/ZkFold/Symbolic/Base/Polynomial.hs
@@ -1,10 +1,8 @@
-{-# LANGUAGE
-AllowAmbiguousTypes
-, DerivingStrategies
-, TypeOperators
-, UndecidableInstances
-, UndecidableSuperClasses
-#-}
+{-# LANGUAGE AllowAmbiguousTypes     #-}
+{-# LANGUAGE DerivingStrategies      #-}
+{-# LANGUAGE TypeOperators           #-}
+{-# LANGUAGE UndecidableInstances    #-}
+{-# LANGUAGE UndecidableSuperClasses #-}
 
 module ZkFold.Symbolic.Base.Polynomial
   ( Poly
@@ -16,22 +14,22 @@ module ZkFold.Symbolic.Base.Polynomial
   , mapPoly
   ) where
 
-import Control.Category
-import Data.Bifunctor
-import Data.Eq
-import Data.Ord
-import Data.Either
-import Data.Foldable hiding (toList, sum, product)
-import Data.Functor
-import Data.Map.Strict (Map)
-import qualified Data.Map.Strict as Map
-import Data.Set (Set)
-import qualified Data.Set as Set
+import           Control.Category
+import           Data.Bifunctor
+import           Data.Either
+import           Data.Eq
+import           Data.Foldable            hiding (product, sum, toList)
+import           Data.Functor
+import           Data.Map.Strict          (Map)
+import qualified Data.Map.Strict          as Map
+import           Data.Ord
+import           Data.Set                 (Set)
+import qualified Data.Set                 as Set
+import           GHC.IsList
+import           GHC.TypeNats
 import qualified Prelude
-import GHC.IsList
-import GHC.TypeNats
 
-import ZkFold.Symbolic.Base.Num
+import           ZkFold.Symbolic.Base.Num
 
 newtype Mono var pow = UnsafeMono {fromMono :: Map var pow}
   deriving (Eq, Ord, Functor)
diff --git a/src/ZkFold/Symbolic/Base/Vector.hs b/src/ZkFold/Symbolic/Base/Vector.hs
index 4b94b5ce0..094fb1f06 100644
--- a/src/ZkFold/Symbolic/Base/Vector.hs
+++ b/src/ZkFold/Symbolic/Base/Vector.hs
@@ -1,8 +1,10 @@
-{-# LANGUAGE AllowAmbiguousTypes  #-}
-{-# LANGUAGE DerivingStrategies   #-}
-{-# LANGUAGE DerivingVia          #-}
-{-# LANGUAGE TypeOperators        #-}
-{-# LANGUAGE QuantifiedConstraints, UndecidableInstances, UndecidableSuperClasses #-}
+{-# LANGUAGE AllowAmbiguousTypes     #-}
+{-# LANGUAGE DerivingStrategies      #-}
+{-# LANGUAGE DerivingVia             #-}
+{-# LANGUAGE QuantifiedConstraints   #-}
+{-# LANGUAGE TypeOperators           #-}
+{-# LANGUAGE UndecidableInstances    #-}
+{-# LANGUAGE UndecidableSuperClasses #-}
 
 module ZkFold.Symbolic.Base.Vector
   ( -- * VectorSpace
@@ -26,29 +28,29 @@ module ZkFold.Symbolic.Base.Vector
   , dotV
   ) where
 
-import Control.Category
-import Control.Monad
-import Data.Bool
-import Data.Distributive
-import Data.Either
-import Data.Eq
-import Data.Ord
-import Data.Foldable hiding (sum)
-import Data.Function (const, ($))
-import Data.Functor
-import Data.Functor.Rep
-import Data.Traversable
-import Data.Kind (Type)
-import Data.IntMap (IntMap)
-import qualified Data.IntMap as IntMap
-import Data.Maybe
-import Data.Type.Equality
-import qualified Data.Vector as V
-import Data.Void
-import qualified GHC.Generics as Gen
+import           Control.Category
+import           Control.Monad
+import           Data.Bool
+import           Data.Distributive
+import           Data.Either
+import           Data.Eq
+import           Data.Foldable            hiding (sum)
+import           Data.Function            (const, ($))
+import           Data.Functor
+import           Data.Functor.Rep
+import           Data.IntMap              (IntMap)
+import qualified Data.IntMap              as IntMap
+import           Data.Kind                (Type)
+import           Data.Maybe
+import           Data.Ord
+import           Data.Traversable
+import           Data.Type.Equality
+import qualified Data.Vector              as V
+import           Data.Void
+import qualified GHC.Generics             as Gen
 import qualified Prelude
 
-import ZkFold.Symbolic.Base.Num
+import           ZkFold.Symbolic.Base.Num
 
 {- |
 Class of vector spaces with a basis.

From 9ae9e5d2a4b941cc695041b892d264e8adc22a54 Mon Sep 17 00:00:00 2001
From: Eitan Chatav <eitan.chatav@gmail.com>
Date: Fri, 12 Jul 2024 17:47:27 -0700
Subject: [PATCH 07/51] use indexed transformers

---
 src/ZkFold/Symbolic/Base/Circuit.hs | 204 +++++++++++++++-------------
 zkfold-base.cabal                   |   1 +
 2 files changed, 107 insertions(+), 98 deletions(-)

diff --git a/src/ZkFold/Symbolic/Base/Circuit.hs b/src/ZkFold/Symbolic/Base/Circuit.hs
index ad1705594..a6e18573b 100644
--- a/src/ZkFold/Symbolic/Base/Circuit.hs
+++ b/src/ZkFold/Symbolic/Base/Circuit.hs
@@ -6,24 +6,26 @@ AllowAmbiguousTypes
 , RankNTypes
 , TypeOperators
 , UndecidableInstances
+, UndecidableSuperClasses
 #-}
 
 module ZkFold.Symbolic.Base.Circuit
-  ( Circuit (..)
+  ( Circuit (..), circuit, evalC
   , SysVar (..)
   , OutVar (..)
   , MonadCircuit (..)
-  , evalC
-  , idC
-  , applyC
+  , IxMonadCircuit (..)
+  , Blueprint (..)
   ) where
 
 import Control.Applicative
 import Control.Category
+import Control.Monad
+import Control.Monad.Trans
+import Control.Monad.Trans.Indexed
 import Data.Either
 import Data.Eq
 import Data.Function (($))
-import Data.Functor
 import Data.IntMap (IntMap)
 import qualified Data.IntMap as IntMap
 import Data.Maybe
@@ -33,6 +35,7 @@ import Data.Semigroup
 import Data.Set (Set)
 import qualified Data.Set as Set
 import Data.Type.Equality
+import qualified Prelude
 
 import ZkFold.Symbolic.Base.Num
 import ZkFold.Symbolic.Base.Polynomial
@@ -54,6 +57,16 @@ data Circuit x i o = Circuit
     -- they can be input, constant or new variables.
   }
 
+circuit
+  :: (Ord x, VectorSpace x i)
+  => (forall t m. (IxMonadCircuit x t, Monad m) => t i i m (o (OutVar x i)))
+  -> Circuit x i o
+circuit m = case unPar1 (runBlueprint m mempty) of
+  (o, c) -> c {outputC = o}
+
+evalC :: (VectorSpace x i, Functor o) => Circuit x i o -> i x -> o x
+evalC c i = fmap (witnessIndex i (witnessC c)) (outputC c)
+
 data SysVar x i
   = InVar (Basis x i)
   | NewVar Int
@@ -83,106 +96,101 @@ instance (Ord x, VectorSpace x i, o ~ U1) => Semigroup (Circuit x i o) where
     , outputC = U1
     }
 
-evalC :: (VectorSpace x i, Functor o) => Circuit x i o -> i x -> o x
-evalC c i = fmap (witnessIndex i (witnessC c)) (outputC c)
-
-applyC
-  :: (Ord x, Algebra x x, VectorSpace x i, VectorSpace x j, Functor o)
-  => i x -> Circuit x (i :*: j) o -> Circuit x j o
-applyC i c = c
-  { systemC = Set.map (mapPoly sysF) (systemC c)
-  , witnessC = fmap witF (witnessC c)
-  , outputC = fmap outF (outputC c)
-  } where
-      sysF = \case
-        InVar (Left bi) -> Left (indexV i bi)
-        InVar (Right bj) -> Right (InVar bj)
-        NewVar n -> Right (NewVar n)
-      witF f j = f (i :*: j)
-      outF = \case
-        SysVar (InVar (Left bi)) -> ConstVar (indexV i bi)
-        SysVar (InVar (Right bj)) -> SysVar (InVar bj)
-        SysVar (NewVar n) -> SysVar (NewVar n)
-        ConstVar x -> ConstVar x
-
-newInputC
-  :: (Ord x, Algebra x x, VectorSpace x i, VectorSpace x j, Functor o)
-  => Circuit x j o -> Circuit x (i :*: j) o
-newInputC c = c
-  { systemC = Set.map (mapPoly sysF) (systemC c)
-  , witnessC = fmap witF (witnessC c)
-  , outputC = fmap outF (outputC c)
-  } where
-    sysF = \case
-      InVar bj -> Right (InVar (Right bj))
-      NewVar n -> Right (NewVar n)
-    witF f (_ :*: j) = f j
-    outF = \case
-      SysVar (InVar bj) -> SysVar (InVar (Right bj))
-      SysVar (NewVar n) -> SysVar (NewVar n)
-      ConstVar k -> ConstVar k
-
-inputC :: forall x i. VectorSpace x i => i (OutVar x i)
-inputC = fmap (SysVar . InVar) (basisV @x)
-
-idC :: forall x i. (Ord x, VectorSpace x i) => Circuit x i i
-idC = mempty {outputC = inputC}
-
-class (forall i j. Functor (m i j))
-  => MonadCircuit x m | m -> x where
-    apply :: (VectorSpace x i, VectorSpace x j) => i x -> m (i :*: j) j ()
-    newInput :: (VectorSpace x i, VectorSpace x j) => m j (i :*: j) ()
-    return :: r -> m i i r
-    (>>=) :: m i j r -> (r -> m j k s) -> m i k s
-    (>>) :: m i j r -> m j k s -> m i k s
-    x >> y = x >>= \_ -> y
-    (<¢>) :: m i j (r -> s) -> m j k r -> m i k s
-    f <¢> x = f >>= (<$> x)
-    input :: VectorSpace x i => m i i (i (OutVar x i))
-    input = return (inputC @x)
-    eval :: (VectorSpace x i, Functor o) => m i i (o (OutVar x i)) -> i x -> o x
-    runCircuit :: VectorSpace x i => Circuit x i o -> m i i (o (OutVar x i))
+class Monad m
+  => MonadCircuit x i m | m -> x, m -> i where
+    runCircuit
+      :: VectorSpace x i
+      => Circuit x i o -> m (o (OutVar x i))
+    input :: VectorSpace x i => m (i (OutVar x i))
+    input = return (fmap (SysVar . InVar) (basisV @x))
     constraint
       :: VectorSpace x i
-      => (forall a. Algebra x a => (SysVar x i -> a) -> a)
-      -> m i i ()
+      => (forall a. Algebra x a => (SysVar x i -> a) -> a) -> m ()
     newConstrained
       :: VectorSpace x i
       => (forall a. Algebra x a => (Int -> a) -> Int -> a)
       -> ((Int -> x) -> x)
-      -> m i i (OutVar x i)
-
-newtype Blueprint x i j r = Blueprint
-  {runBlueprint :: Circuit x i U1 -> (r, Circuit x j U1)}
+      -> m (OutVar x i)
+
+class
+  ( forall i m. Monad m => MonadCircuit x i (t i i m)
+  , IxMonadTrans t
+  ) => IxMonadCircuit x t | t -> x where
+    apply
+      :: (VectorSpace x i, VectorSpace x j, Monad m)
+      => i x -> t (i :*: j) j m ()
+    newInput
+      :: (VectorSpace x i, VectorSpace x j, Monad m)
+      => t j (i :*: j) m ()
+
+newtype Blueprint x i j m r = Blueprint
+  {runBlueprint :: Circuit x i U1 -> m (r, Circuit x j U1)}
   deriving Functor
 
-instance (Algebra x x, Ord x) => Applicative (Blueprint x i i) where
-  pure = return
-  (<*>) = (<¢>)
-
-instance (Algebra x x, Ord x) => MonadCircuit x (Blueprint x) where
-  return x = Blueprint $ \c -> (x,c)
-  m >>= f = Blueprint $ \c ->
-    let
-      (x, c') = runBlueprint m c
-    in
-      runBlueprint (f x) c'
-  apply i = Blueprint $ \c -> ((), applyC i c)
-  newInput = Blueprint $ \c -> ((), newInputC c)
-  eval x i = case runBlueprint x mempty of
-    (o, c) -> evalC (c {outputC = o}) i
-  runCircuit c = Blueprint $ \c' ->
-    (outputC c, c {outputC = U1} <> c')
-  constraint p = Blueprint $ \c ->
-    ((), c { systemC = Set.insert (p var) (systemC c) })
-  newConstrained p w = Blueprint $ \c ->
-    let
-      (maxIndex, _) = IntMap.findMax (witnessC c)
-      newIndex = maxIndex + 1
-      newWitness i = w (fromMaybe zero . ((($ i) <$> witnessC c) IntMap.!?))
-     in
-      ( SysVar (NewVar newIndex)
-      , c { systemC = Set.insert (p (var . NewVar) newIndex) (systemC c)
-          , witnessC = IntMap.insert newIndex newWitness (witnessC c)
+instance (Field x, Ord x, Monad m)
+  => Applicative (Blueprint x i i m) where
+    pure x = Blueprint $ \c -> return (x,c)
+    (<*>) = apIx
+
+instance (Field x, Ord x, Monad m)
+  => Monad (Blueprint x i i m) where
+    return = pure
+    (>>=) = Prelude.flip bindIx
+
+instance (Field x, Ord x, Monad m)
+  => MonadCircuit x i (Blueprint x i i m) where
+
+    runCircuit c = Blueprint $ \c' -> return
+      (outputC c, c {outputC = U1} <> c')
+
+    constraint p = Blueprint $ \c -> return
+      ((), c {systemC = Set.insert (p var) (systemC c)})
+
+    newConstrained p w = Blueprint $ \c ->
+      let
+        (maxIndex, _) = IntMap.findMax (witnessC c)
+        newIndex = maxIndex + 1
+        newWitness i = w (fromMaybe zero . ((($ i) <$> witnessC c) IntMap.!?))
+      in return
+        ( SysVar (NewVar newIndex)
+        , c { systemC = Set.insert (p (var . NewVar) newIndex) (systemC c)
+            , witnessC = IntMap.insert newIndex newWitness (witnessC c)
+            }
+        )
+
+instance (i ~ j, Ord x, Field x)
+  => MonadTrans (Blueprint x i j) where
+    lift m = Blueprint $ \c -> (, c) <$> m
+
+instance (Field x, Ord x) => IxMonadTrans (Blueprint x) where
+  joinIx (Blueprint f) = Blueprint $ \c -> do
+    (Blueprint g, c') <- f c
+    g c'
+
+instance (Field x, Ord x)
+  => IxMonadCircuit x (Blueprint x) where
+    apply i = Blueprint $ \c -> return
+      ( ()
+      , c { systemC = Set.map (mapPoly sysF) (systemC c)
+          , witnessC = fmap witF (witnessC c)
+          , outputC = U1
+          }
+      ) where
+          sysF = \case
+            InVar (Left bi) -> Left (indexV i bi)
+            InVar (Right bj) -> Right (InVar bj)
+            NewVar n -> Right (NewVar n)
+          witF f j = f (i :*: j)
+
+    newInput = Blueprint $ \c -> return
+      ( ()
+      , c { systemC = Set.map (mapPoly sysF) (systemC c)
+          , witnessC = fmap witF (witnessC c)
+          , outputC = U1
           }
       )
+      where
+          sysF = \case
+            InVar bj -> Right (InVar (Right bj))
+            NewVar n -> Right (NewVar n)
+          witF f (_ :*: j) = f j
diff --git a/zkfold-base.cabal b/zkfold-base.cabal
index 4eeabca95..eba45974f 100644
--- a/zkfold-base.cabal
+++ b/zkfold-base.cabal
@@ -200,6 +200,7 @@ library
       cryptohash-sha256                    < 0.12,
       deepseq                          <= 1.5.0.0,
       distributive                          < 0.7,
+      indexed-transformers                  < 0.2,
       mtl                                   < 2.4,
       optics                                < 0.5,
       parallel                          < 3.2.3.0,

From 96923e8e5f6c1d61f3e6fc2ca70038f1f511cc8e Mon Sep 17 00:00:00 2001
From: Eitan Chatav <eitan.chatav@gmail.com>
Date: Fri, 12 Jul 2024 19:00:30 -0700
Subject: [PATCH 08/51] Update main-pull.yml

---
 .github/workflows/main-pull.yml | 1 +
 1 file changed, 1 insertion(+)

diff --git a/.github/workflows/main-pull.yml b/.github/workflows/main-pull.yml
index 75f847334..5a528d860 100644
--- a/.github/workflows/main-pull.yml
+++ b/.github/workflows/main-pull.yml
@@ -32,6 +32,7 @@ jobs:
 
     - name: Configure Cabal
       run: |
+        cabal update
         cabal configure --enable-tests --enable-benchmarks --enable-documentation
     
     - name: Generate cache key

From c6fae32b7027b27cdef3b26f6b50af276aa0fee5 Mon Sep 17 00:00:00 2001
From: Eitan Chatav <eitan.chatav@gmail.com>
Date: Sat, 13 Jul 2024 10:43:55 -0700
Subject: [PATCH 09/51] Update main-pull.yml

---
 .github/workflows/main-pull.yml | 1 -
 1 file changed, 1 deletion(-)

diff --git a/.github/workflows/main-pull.yml b/.github/workflows/main-pull.yml
index 5a528d860..75f847334 100644
--- a/.github/workflows/main-pull.yml
+++ b/.github/workflows/main-pull.yml
@@ -32,7 +32,6 @@ jobs:
 
     - name: Configure Cabal
       run: |
-        cabal update
         cabal configure --enable-tests --enable-benchmarks --enable-documentation
     
     - name: Generate cache key

From 0608f4333b0ae3650a03518c7de4eea883e86a3a Mon Sep 17 00:00:00 2001
From: Eitan Chatav <eitan.chatav@gmail.com>
Date: Sat, 13 Jul 2024 11:13:47 -0700
Subject: [PATCH 10/51] newAssigned

also `from` and `AdditiveMonoid` and some renaming
---
 src/ZkFold/Symbolic/Base/Circuit.hs | 72 +++++++++++++++++++----------
 1 file changed, 47 insertions(+), 25 deletions(-)

diff --git a/src/ZkFold/Symbolic/Base/Circuit.hs b/src/ZkFold/Symbolic/Base/Circuit.hs
index 017c72ceb..a64cbb9e5 100644
--- a/src/ZkFold/Symbolic/Base/Circuit.hs
+++ b/src/ZkFold/Symbolic/Base/Circuit.hs
@@ -15,7 +15,7 @@ module ZkFold.Symbolic.Base.Circuit
   , OutVar (..)
   , MonadCircuit (..)
   , IxMonadCircuit (..)
-  , Blueprint (..)
+  , CircuitIx (..)
   ) where
 
 import Control.Applicative
@@ -61,7 +61,7 @@ circuit
   :: (Ord x, VectorSpace x i)
   => (forall t m. (IxMonadCircuit x t, Monad m) => t i i m (o (OutVar x i)))
   -> Circuit x i o
-circuit m = case unPar1 (runBlueprint m mempty) of
+circuit m = case unPar1 (runCircuitIx m mempty) of
   (o, c) -> c {outputC = o}
 
 evalC :: (VectorSpace x i, Functor o) => Circuit x i o -> i x -> o x
@@ -105,12 +105,18 @@ class Monad m
     input = return (fmap (SysVar . InVar) (basisV @x))
     constraint
       :: VectorSpace x i
-      => (forall a. Algebra x a => (SysVar x i -> a) -> a) -> m ()
+      => (forall a. Algebra x a => (SysVar x i -> a) -> a)
+      -> m ()
     newConstrained
       :: VectorSpace x i
-      => (forall a. Algebra x a => (Int -> a) -> Int -> a)
-      -> ((Int -> x) -> x)
+      => (forall a. Algebra x a => (OutVar x i -> a) -> OutVar x i -> a)
+      -> ((OutVar x i -> x) -> x)
       -> m (OutVar x i)
+    newAssigned
+      :: VectorSpace x i
+      => (forall a. Algebra x a => (OutVar x i -> a) -> a)
+      -> m (OutVar x i)
+    newAssigned p = newConstrained (\x i -> p x - x i) p
 
 class
   ( forall i m. Monad m => MonadCircuit x i (t i i m)
@@ -123,53 +129,57 @@ class
       :: (VectorSpace x i, VectorSpace x j, Monad m)
       => t j (i :*: j) m ()
 
-newtype Blueprint x i j m r = Blueprint
-  {runBlueprint :: Circuit x i U1 -> m (r, Circuit x j U1)}
+newtype CircuitIx x i j m r = UnsafeCircuitIx
+  {runCircuitIx :: Circuit x i U1 -> m (r, Circuit x j U1)}
   deriving Functor
 
 instance (Field x, Ord x, Monad m)
-  => Applicative (Blueprint x i i m) where
-    pure x = Blueprint $ \c -> return (x,c)
+  => Applicative (CircuitIx x i i m) where
+    pure x = UnsafeCircuitIx $ \c -> return (x,c)
     (<*>) = apIx
 
 instance (Field x, Ord x, Monad m)
-  => Monad (Blueprint x i i m) where
+  => Monad (CircuitIx x i i m) where
     return = pure
     (>>=) = Prelude.flip bindIx
 
 instance (Field x, Ord x, Monad m)
-  => MonadCircuit x i (Blueprint x i i m) where
+  => MonadCircuit x i (CircuitIx x i i m) where
 
-    runCircuit c = Blueprint $ \c' -> return
+    runCircuit c = UnsafeCircuitIx $ \c' -> return
       (outputC c, c {outputC = U1} <> c')
 
-    constraint p = Blueprint $ \c -> return
+    constraint p = UnsafeCircuitIx $ \c -> return
       ((), c {systemC = Set.insert (p var) (systemC c)})
 
-    newConstrained p w = Blueprint $ \c ->
+    newConstrained p w = UnsafeCircuitIx $ \c ->
       let
         (maxIndex, _) = IntMap.findMax (witnessC c)
         newIndex = maxIndex + 1
-        newWitness i = w (fromMaybe zero . ((($ i) <$> witnessC c) IntMap.!?))
+        newWitness i = w (witnessIndex i (witnessC c))
+        varF = \case
+          ConstVar x -> Left x
+          SysVar v -> Right v
+        outVar = SysVar (NewVar newIndex)
       in return
-        ( SysVar (NewVar newIndex)
-        , c { systemC = Set.insert (p (var . NewVar) newIndex) (systemC c)
+        ( outVar
+        , c { systemC = Set.insert (mapPoly varF (p var outVar)) (systemC c)
             , witnessC = IntMap.insert newIndex newWitness (witnessC c)
             }
         )
 
 instance (i ~ j, Ord x, Field x)
-  => MonadTrans (Blueprint x i j) where
-    lift m = Blueprint $ \c -> (, c) <$> m
+  => MonadTrans (CircuitIx x i j) where
+    lift m = UnsafeCircuitIx $ \c -> (, c) <$> m
 
-instance (Field x, Ord x) => IxMonadTrans (Blueprint x) where
-  joinIx (Blueprint f) = Blueprint $ \c -> do
-    (Blueprint g, c') <- f c
+instance (Field x, Ord x) => IxMonadTrans (CircuitIx x) where
+  joinIx (UnsafeCircuitIx f) = UnsafeCircuitIx $ \c -> do
+    (UnsafeCircuitIx g, c') <- f c
     g c'
 
 instance (Field x, Ord x)
-  => IxMonadCircuit x (Blueprint x) where
-    apply i = Blueprint $ \c -> return
+  => IxMonadCircuit x (CircuitIx x) where
+    apply i = UnsafeCircuitIx $ \c -> return
       ( ()
       , c { systemC = Set.map (mapPoly sysF) (systemC c)
           , witnessC = fmap witF (witnessC c)
@@ -182,7 +192,7 @@ instance (Field x, Ord x)
             NewVar n -> Right (NewVar n)
           witF f j = f (i :*: j)
 
-    newInput = Blueprint $ \c -> return
+    newInput = UnsafeCircuitIx $ \c -> return
       ( ()
       , c { systemC = Set.map (mapPoly sysF) (systemC c)
           , witnessC = fmap witF (witnessC c)
@@ -194,3 +204,15 @@ instance (Field x, Ord x)
             InVar bj -> Right (InVar (Right bj))
             NewVar n -> Right (NewVar n)
           witF f (_ :*: j) = f j
+
+instance (Ord x, VectorSpace x i)
+  => From x (Circuit x i Par1) where
+    from x = mempty { outputC = Par1 (ConstVar x) }
+
+instance (Ord x, VectorSpace x i)
+  => AdditiveMonoid (Circuit x i Par1) where
+    zero = from @x zero
+    c0 + c1 = circuit $ do
+      Par1 v0 <- runCircuit c0
+      Par1 v1 <- runCircuit c1
+      Par1 <$> newAssigned (\x -> x v0 + x v1)

From 8d872fa0f1cbc6ce48ae43155b27199a73515311 Mon Sep 17 00:00:00 2001
From: Eitan Chatav <eitan.chatav@gmail.com>
Date: Sat, 13 Jul 2024 11:21:25 -0700
Subject: [PATCH 11/51] Update Circuit.hs

---
 src/ZkFold/Symbolic/Base/Circuit.hs | 20 ++++++++++----------
 1 file changed, 10 insertions(+), 10 deletions(-)

diff --git a/src/ZkFold/Symbolic/Base/Circuit.hs b/src/ZkFold/Symbolic/Base/Circuit.hs
index a64cbb9e5..9e255a5d5 100644
--- a/src/ZkFold/Symbolic/Base/Circuit.hs
+++ b/src/ZkFold/Symbolic/Base/Circuit.hs
@@ -152,21 +152,21 @@ instance (Field x, Ord x, Monad m)
     constraint p = UnsafeCircuitIx $ \c -> return
       ((), c {systemC = Set.insert (p var) (systemC c)})
 
-    newConstrained p w = UnsafeCircuitIx $ \c ->
+    newConstrained p w = UnsafeCircuitIx $ \c -> return $
       let
-        (maxIndex, _) = IntMap.findMax (witnessC c)
-        newIndex = maxIndex + 1
+        maxIndexMaybe = IntMap.lookupMax (witnessC c)
+        newIndex = maybe 0 ((1 +) . Prelude.fst) maxIndexMaybe
         newWitness i = w (witnessIndex i (witnessC c))
-        varF = \case
+        evalConst = \case
           ConstVar x -> Left x
           SysVar v -> Right v
         outVar = SysVar (NewVar newIndex)
-      in return
-        ( outVar
-        , c { systemC = Set.insert (mapPoly varF (p var outVar)) (systemC c)
-            , witnessC = IntMap.insert newIndex newWitness (witnessC c)
-            }
-        )
+        newSystemC =
+          Set.insert (mapPoly evalConst (p var outVar)) (systemC c)
+        newWitnessC =
+          IntMap.insert newIndex newWitness (witnessC c)
+      in
+        (outVar, c {systemC = newSystemC, witnessC = newWitnessC})
 
 instance (i ~ j, Ord x, Field x)
   => MonadTrans (CircuitIx x i j) where

From 331c28513d45e7c29424ab11c84954ae1dd5749a Mon Sep 17 00:00:00 2001
From: Eitan Chatav <eitan.chatav@gmail.com>
Date: Sat, 13 Jul 2024 11:22:36 -0700
Subject: [PATCH 12/51] golfin

---
 src/ZkFold/Symbolic/Base/Circuit.hs | 8 +++-----
 1 file changed, 3 insertions(+), 5 deletions(-)

diff --git a/src/ZkFold/Symbolic/Base/Circuit.hs b/src/ZkFold/Symbolic/Base/Circuit.hs
index 9e255a5d5..187d878e6 100644
--- a/src/ZkFold/Symbolic/Base/Circuit.hs
+++ b/src/ZkFold/Symbolic/Base/Circuit.hs
@@ -157,14 +157,12 @@ instance (Field x, Ord x, Monad m)
         maxIndexMaybe = IntMap.lookupMax (witnessC c)
         newIndex = maybe 0 ((1 +) . Prelude.fst) maxIndexMaybe
         newWitness i = w (witnessIndex i (witnessC c))
-        evalConst = \case
+        evalConst = mapPoly $ \case
           ConstVar x -> Left x
           SysVar v -> Right v
         outVar = SysVar (NewVar newIndex)
-        newSystemC =
-          Set.insert (mapPoly evalConst (p var outVar)) (systemC c)
-        newWitnessC =
-          IntMap.insert newIndex newWitness (witnessC c)
+        newSystemC = Set.insert (evalConst (p var outVar)) (systemC c)
+        newWitnessC = IntMap.insert newIndex newWitness (witnessC c)
       in
         (outVar, c {systemC = newSystemC, witnessC = newWitnessC})
 

From 42ebbebd32504722ee79f5bbc6b5f7f44f5b70b2 Mon Sep 17 00:00:00 2001
From: Eitan Chatav <eitan.chatav@gmail.com>
Date: Sat, 13 Jul 2024 11:31:44 -0700
Subject: [PATCH 13/51] Update Circuit.hs

---
 src/ZkFold/Symbolic/Base/Circuit.hs | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/src/ZkFold/Symbolic/Base/Circuit.hs b/src/ZkFold/Symbolic/Base/Circuit.hs
index 187d878e6..731a7f4c3 100644
--- a/src/ZkFold/Symbolic/Base/Circuit.hs
+++ b/src/ZkFold/Symbolic/Base/Circuit.hs
@@ -41,7 +41,7 @@ import           ZkFold.Symbolic.Base.Num
 import           ZkFold.Symbolic.Base.Polynomial
 import           ZkFold.Symbolic.Base.Vector
 
-data Circuit x i o = Circuit
+data Circuit x i o = UnsafeCircuit
   { systemC  :: Set (Poly (SysVar x i) Natural x)
     -- ^ The system of polynomial constraints,
     -- each polynomial constitutes a "multi-edge" of the circuit graph,
@@ -88,9 +88,9 @@ witnessIndex inp witnessMap = \case
   ConstVar x -> x
 
 instance (Ord x, VectorSpace x i, o ~ U1) => Monoid (Circuit x i o) where
-  mempty = Circuit mempty mempty U1
+  mempty = UnsafeCircuit mempty mempty U1
 instance (Ord x, VectorSpace x i, o ~ U1) => Semigroup (Circuit x i o) where
-  c0 <> c1 = Circuit
+  c0 <> c1 = UnsafeCircuit
     { systemC = systemC c0 <> systemC c1
     , witnessC = witnessC c0 <> witnessC c1
     , outputC = U1

From 0d5f9f2ddfcb827a653d3d4c68ece6241127b866 Mon Sep 17 00:00:00 2001
From: Eitan Chatav <eitan.chatav@gmail.com>
Date: Sat, 13 Jul 2024 12:35:34 -0700
Subject: [PATCH 14/51] Update Circuit.hs

---
 src/ZkFold/Symbolic/Base/Circuit.hs | 20 ++++++++++++++------
 1 file changed, 14 insertions(+), 6 deletions(-)

diff --git a/src/ZkFold/Symbolic/Base/Circuit.hs b/src/ZkFold/Symbolic/Base/Circuit.hs
index 731a7f4c3..3381ba59c 100644
--- a/src/ZkFold/Symbolic/Base/Circuit.hs
+++ b/src/ZkFold/Symbolic/Base/Circuit.hs
@@ -11,11 +11,11 @@ AllowAmbiguousTypes
 
 module ZkFold.Symbolic.Base.Circuit
   ( Circuit (..), circuit, evalC
-  , SysVar (..)
-  , OutVar (..)
   , MonadCircuit (..)
   , IxMonadCircuit (..)
   , CircuitIx (..)
+  , SysVar (..)
+  , OutVar (..)
   ) where
 
 import Control.Applicative
@@ -198,10 +198,10 @@ instance (Field x, Ord x)
           }
       )
       where
-          sysF = \case
-            InVar bj -> Right (InVar (Right bj))
-            NewVar n -> Right (NewVar n)
-          witF f (_ :*: j) = f j
+        sysF = \case
+          InVar bj -> Right (InVar (Right bj))
+          NewVar n -> Right (NewVar n)
+        witF f (_ :*: j) = f j
 
 instance (Ord x, VectorSpace x i)
   => From x (Circuit x i Par1) where
@@ -214,3 +214,11 @@ instance (Ord x, VectorSpace x i)
       Par1 v0 <- runCircuit c0
       Par1 v1 <- runCircuit c1
       Par1 <$> newAssigned (\x -> x v0 + x v1)
+
+instance (Ord x, VectorSpace x i)
+  => MultiplicativeMonoid (Circuit x i Par1) where
+    one = from @x one
+    c0 * c1 = circuit $ do
+      Par1 v0 <- runCircuit c0
+      Par1 v1 <- runCircuit c1
+      Par1 <$> newAssigned (\x -> x v0 * x v1)

From c13d4e4221f66099fa72f7cc3b0c8b93113aa6d9 Mon Sep 17 00:00:00 2001
From: Eitan Chatav <eitan.chatav@gmail.com>
Date: Sat, 13 Jul 2024 13:08:38 -0700
Subject: [PATCH 15/51] Update Polynomial.hs

---
 src/ZkFold/Symbolic/Base/Polynomial.hs | 17 ++++++++++-------
 1 file changed, 10 insertions(+), 7 deletions(-)

diff --git a/src/ZkFold/Symbolic/Base/Polynomial.hs b/src/ZkFold/Symbolic/Base/Polynomial.hs
index 2aa9902e4..e4739572f 100644
--- a/src/ZkFold/Symbolic/Base/Polynomial.hs
+++ b/src/ZkFold/Symbolic/Base/Polynomial.hs
@@ -112,11 +112,14 @@ instance (Ord var, Ord pow, Semiring pow, Semiring coef, Ord coef)
 instance (Ord var, Ord pow, Semiring pow, Semiring x, Eq x)
   => Scalar x (Poly var pow x) where
     scale c = if c == zero then Prelude.const zero else fmap (c *)
-    combine polys = product [scale c p | (c,p) <- polys]
-    -- TODO: consider how to optimize combine
-    -- using an additional Scalar x x constraint
-    -- since then we can hopefully applicatively apply combine
-    -- to monomials...
+    combine polys =
+      let
+        -- TODO: calculate more efficiently.
+        -- try to collect like monomials with
+        -- their inner and outer coefficients.
+        -- Then apply combine to their coefficients.
+      in
+        sum [scale c p | (c,p) <- polys]
 instance (Ord var, Ord pow, Semiring x, Eq x)
   => Scalar Natural (Poly var pow x) where
     scale c = if c == zero then Prelude.const zero else fmap (from c *)
@@ -140,11 +143,11 @@ varSet
   . Map.keysSet
   . fromCombo
 
--- evaluate a polynomial in its field of coefficients
+-- evaluate a polynomial in its semiring of coefficients
 evalPoly :: (Ord x, Semiring x) => Poly x Natural x -> x
 evalPoly x = combine [(c, evalMono (toList m)) | (c,m) <- toList x]
 
--- map a polynomial to new variables and evaluate some variables
+-- map a polynomial to new variables, evaluating some variables
 mapPoly
   :: (Eq x, Ord var0, Ord var1, Semiring x)
   => (var0 -> Either x var1)

From 5ddd7a2794d220d9b553e832e335a46c22a608b3 Mon Sep 17 00:00:00 2001
From: Eitan Chatav <eitan.chatav@gmail.com>
Date: Sat, 13 Jul 2024 13:32:54 -0700
Subject: [PATCH 16/51] evalConst

---
 src/ZkFold/Symbolic/Base/Circuit.hs | 18 ++++++++++++------
 1 file changed, 12 insertions(+), 6 deletions(-)

diff --git a/src/ZkFold/Symbolic/Base/Circuit.hs b/src/ZkFold/Symbolic/Base/Circuit.hs
index 3381ba59c..77e84eb5d 100644
--- a/src/ZkFold/Symbolic/Base/Circuit.hs
+++ b/src/ZkFold/Symbolic/Base/Circuit.hs
@@ -79,6 +79,14 @@ data OutVar x i
 deriving stock instance (Eq x, VectorSpace x i) => Eq (OutVar x i)
 deriving stock instance (Ord x, VectorSpace x i) => Ord (OutVar x i)
 
+evalConst
+  :: (Ord x, VectorSpace x i)
+  => Poly (OutVar x i) Natural x
+  -> Poly (SysVar x i) Natural x
+evalConst = mapPoly $ \case
+  ConstVar x -> Left x
+  SysVar v -> Right v
+  
 witnessIndex
   :: VectorSpace x i
   => i x -> IntMap (i x -> x) -> OutVar x i -> x
@@ -105,7 +113,7 @@ class Monad m
     input = return (fmap (SysVar . InVar) (basisV @x))
     constraint
       :: VectorSpace x i
-      => (forall a. Algebra x a => (SysVar x i -> a) -> a)
+      => (forall a. Algebra x a => (OutVar x i -> a) -> a)
       -> m ()
     newConstrained
       :: VectorSpace x i
@@ -150,18 +158,16 @@ instance (Field x, Ord x, Monad m)
       (outputC c, c {outputC = U1} <> c')
 
     constraint p = UnsafeCircuitIx $ \c -> return
-      ((), c {systemC = Set.insert (p var) (systemC c)})
+      ((), c {systemC = Set.insert (evalConst (p var)) (systemC c)})
 
     newConstrained p w = UnsafeCircuitIx $ \c -> return $
       let
         maxIndexMaybe = IntMap.lookupMax (witnessC c)
         newIndex = maybe 0 ((1 +) . Prelude.fst) maxIndexMaybe
         newWitness i = w (witnessIndex i (witnessC c))
-        evalConst = mapPoly $ \case
-          ConstVar x -> Left x
-          SysVar v -> Right v
         outVar = SysVar (NewVar newIndex)
-        newSystemC = Set.insert (evalConst (p var outVar)) (systemC c)
+        newConstraint = evalConst (p var outVar)
+        newSystemC = Set.insert newConstraint (systemC c)
         newWitnessC = IntMap.insert newIndex newWitness (witnessC c)
       in
         (outVar, c {systemC = newSystemC, witnessC = newWitnessC})

From f979709bb23965e6c7be4590ac6e7da83c79503d Mon Sep 17 00:00:00 2001
From: Eitan Chatav <eitan.chatav@gmail.com>
Date: Sat, 13 Jul 2024 14:27:18 -0700
Subject: [PATCH 17/51] fix -

---
 src/ZkFold/Symbolic/Base/Polynomial.hs | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/ZkFold/Symbolic/Base/Polynomial.hs b/src/ZkFold/Symbolic/Base/Polynomial.hs
index e4739572f..16fd7cea4 100644
--- a/src/ZkFold/Symbolic/Base/Polynomial.hs
+++ b/src/ZkFold/Symbolic/Base/Polynomial.hs
@@ -71,7 +71,7 @@ instance (Ord var, Semiring coef, Eq coef)
 instance (Ord var, Ring coef, Eq coef)
   => AdditiveGroup (Combo var coef) where
     negate (UnsafeCombo x) = UnsafeCombo (Map.map negate x)
-    UnsafeCombo x - UnsafeCombo y = combo (Map.unionWith (-) x y)
+    x - y = x + negate y
 
 instance (Ord var, AdditiveMonoid coef, Eq coef)
   => IsList (Combo var coef) where

From 9bedfb210df790135d939f46278f15e47d3df56b Mon Sep 17 00:00:00 2001
From: Eitan Chatav <eitan.chatav@gmail.com>
Date: Sat, 13 Jul 2024 14:27:22 -0700
Subject: [PATCH 18/51] fixity

---
 src/ZkFold/Symbolic/Base/Num.hs | 6 ++++++
 1 file changed, 6 insertions(+)

diff --git a/src/ZkFold/Symbolic/Base/Num.hs b/src/ZkFold/Symbolic/Base/Num.hs
index e80c02316..4de376ce9 100644
--- a/src/ZkFold/Symbolic/Base/Num.hs
+++ b/src/ZkFold/Symbolic/Base/Num.hs
@@ -96,6 +96,7 @@ type PrimeField x =
   )
 
 class AdditiveMonoid a where
+  infixl 6 +
   (+) :: a -> a -> a
   zero :: a
 
@@ -104,9 +105,11 @@ sum = foldl' (+) zero
 
 class AdditiveMonoid a => AdditiveGroup a where
   negate :: a -> a
+  infixl 6 -
   (-) :: a -> a -> a
 
 class MultiplicativeMonoid a where
+  infixl 7 *
   (*) :: a -> a -> a
   one :: a
 
@@ -114,6 +117,7 @@ product :: (Foldable t, MultiplicativeMonoid a) => t a -> a
 product = foldl' (*) one
 
 class MultiplicativeMonoid a => MultiplicativeGroup a where
+  infixl 7 /
   (/) :: a -> a -> a
 
 -- from @Natural is the unique homomorphism from the free Semiring
@@ -689,9 +693,11 @@ class (Semiring pow, MultiplicativeMonoid a)
     exponent :: a -> pow -> a
     evalMono :: [(a,pow)] -> a
 
+infixr 8 ^
 (^) :: (Exponent Natural a, Into Natural pow) => a -> pow -> a
 a ^ b = exponent @Natural a (to b)
 
+infixr 8 ^^
 (^^) :: (Exponent Integer a, Into Integer pow) => a -> pow -> a
 a ^^ b = exponent @Integer a (to b)
 

From d1c0181b41cd34a6cfda9599d138067016aab294 Mon Sep 17 00:00:00 2001
From: Eitan Chatav <eitan.chatav@gmail.com>
Date: Sat, 13 Jul 2024 15:03:40 -0700
Subject: [PATCH 19/51] efficient linear combination of polynomials

---
 src/ZkFold/Symbolic/Base/Polynomial.hs | 13 +++++++------
 1 file changed, 7 insertions(+), 6 deletions(-)

diff --git a/src/ZkFold/Symbolic/Base/Polynomial.hs b/src/ZkFold/Symbolic/Base/Polynomial.hs
index 16fd7cea4..9b3294a6d 100644
--- a/src/ZkFold/Symbolic/Base/Polynomial.hs
+++ b/src/ZkFold/Symbolic/Base/Polynomial.hs
@@ -22,6 +22,7 @@ import           Data.Foldable            hiding (product, sum, toList)
 import           Data.Functor
 import           Data.Map.Strict          (Map)
 import qualified Data.Map.Strict          as Map
+import           Data.Monoid
 import           Data.Ord
 import           Data.Set                 (Set)
 import qualified Data.Set                 as Set
@@ -109,17 +110,17 @@ instance (Ord var, Ord pow, Semiring pow, Semiring coef, Ord coef)
   => Exponent Natural (Poly var pow coef) where
     exponent x p = evalMono [(x,p)]
     evalMono = evalMonoN
-instance (Ord var, Ord pow, Semiring pow, Semiring x, Eq x)
+instance (Ord var, Ord pow, Semiring x, Eq x)
   => Scalar x (Poly var pow x) where
     scale c = if c == zero then Prelude.const zero else fmap (c *)
     combine polys =
       let
-        -- TODO: calculate more efficiently.
-        -- try to collect like monomials with
-        -- their inner and outer coefficients.
-        -- Then apply combine to their coefficients.
+        monos =
+          [(m,(c,c')) | (c,p) <- polys, (c',m) <- toList p]
+        insertCoefs mMap (m,cs) = Map.insertWith (<>) m [cs] mMap
+        monoMap = foldl' insertCoefs Map.empty monos
       in
-        sum [scale c p | (c,p) <- polys]
+        combo (fmap combine monoMap)
 instance (Ord var, Ord pow, Semiring x, Eq x)
   => Scalar Natural (Poly var pow x) where
     scale c = if c == zero then Prelude.const zero else fmap (from c *)

From dd0db51cedf7d2139f59f21435afb385fc905b87 Mon Sep 17 00:00:00 2001
From: Eitan Chatav <eitan.chatav@gmail.com>
Date: Sat, 13 Jul 2024 16:38:34 -0700
Subject: [PATCH 20/51] Mod

---
 src/ZkFold/Symbolic/Base/Num.hs | 1 +
 1 file changed, 1 insertion(+)

diff --git a/src/ZkFold/Symbolic/Base/Num.hs b/src/ZkFold/Symbolic/Base/Num.hs
index 4de376ce9..3dc5dcfd0 100644
--- a/src/ZkFold/Symbolic/Base/Num.hs
+++ b/src/ZkFold/Symbolic/Base/Num.hs
@@ -11,6 +11,7 @@ module ZkFold.Symbolic.Base.Num
   , Natural
   , Rational
   , Int
+  , Mod
     -- * Arithmetic constraints
   , Arithmetic
   , PrimeField

From cf5a1ba8f4651829ffbd995f7c6555fc96cff881 Mon Sep 17 00:00:00 2001
From: Eitan Chatav <eitan.chatav@gmail.com>
Date: Sat, 13 Jul 2024 17:02:19 -0700
Subject: [PATCH 21/51] Update Num.hs

---
 src/ZkFold/Symbolic/Base/Num.hs | 25 ++++++-------------------
 1 file changed, 6 insertions(+), 19 deletions(-)

diff --git a/src/ZkFold/Symbolic/Base/Num.hs b/src/ZkFold/Symbolic/Base/Num.hs
index 3dc5dcfd0..d80288ce6 100644
--- a/src/ZkFold/Symbolic/Base/Num.hs
+++ b/src/ZkFold/Symbolic/Base/Num.hs
@@ -552,34 +552,21 @@ residue int = int `mod` from (knownNat @n)
 
 instance From (Mod int n) (Mod int n) where from = id
 
-instance (Euclidean int, KnownNat n) => From int (Mod int n) where
-  from int = UnsafeMod (residue @n int)
+instance (Euclidean int, KnownNat n)
+  => From int (Mod int n) where
+    from = UnsafeMod . residue @n
 
 instance (From Natural int, Euclidean int, KnownNat n)
   => From Natural (Mod int n) where
-    from nat = UnsafeMod (residue @n (from nat))
+    from = UnsafeMod . residue @n . from
 
 instance (SemiIntegral int, KnownNat n)
   => From Integer (Mod int n) where
-    from int =
-      let
-        r = residue @n (to @Integer int)
-        n = from (knownNat @n)
-        zToN = from @Natural . Prelude.fromIntegral
-      in
-        case compare r zero of
-          LT -> zToN (n + r)
-          EQ -> zero
-          GT -> zToN (n - r)
+    from = UnsafeMod . from @Natural . Prelude.fromIntegral . residue @n
 
 instance (SemiIntegral int, Prime p)
   => From Rational (Mod int p) where
-    from q =
-      let
-        top = numerator q
-        bot = denominator q
-      in
-        from top / from bot
+    from q = from (numerator q) / from (denominator q)
 
 instance Into (Mod int n) (Mod int n) where
   to = id

From 5f0a40b60c6ca8d2929631e751229da4248588b4 Mon Sep 17 00:00:00 2001
From: Eitan Chatav <eitan.chatav@gmail.com>
Date: Sat, 13 Jul 2024 17:08:08 -0700
Subject: [PATCH 22/51] Update Num.hs

---
 src/ZkFold/Symbolic/Base/Num.hs | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/ZkFold/Symbolic/Base/Num.hs b/src/ZkFold/Symbolic/Base/Num.hs
index d80288ce6..9efdaa4e7 100644
--- a/src/ZkFold/Symbolic/Base/Num.hs
+++ b/src/ZkFold/Symbolic/Base/Num.hs
@@ -550,7 +550,7 @@ instance (SemiIntegral int, KnownNat n)
 residue :: forall n int. (Euclidean int, KnownNat n) => int -> int
 residue int = int `mod` from (knownNat @n)
 
-instance From (Mod int n) (Mod int n) where from = id
+instance From (Mod int n) (Mod int n)
 
 instance (Euclidean int, KnownNat n)
   => From int (Mod int n) where

From b29699f4f1271773a523e661aaccb7b84ed7ec17 Mon Sep 17 00:00:00 2001
From: Eitan Chatav <eitan.chatav@gmail.com>
Date: Sat, 13 Jul 2024 17:16:53 -0700
Subject: [PATCH 23/51] Update Num.hs

---
 src/ZkFold/Symbolic/Base/Num.hs | 34 ++++++++++++---------------------
 1 file changed, 12 insertions(+), 22 deletions(-)

diff --git a/src/ZkFold/Symbolic/Base/Num.hs b/src/ZkFold/Symbolic/Base/Num.hs
index 9efdaa4e7..1f72b2a70 100644
--- a/src/ZkFold/Symbolic/Base/Num.hs
+++ b/src/ZkFold/Symbolic/Base/Num.hs
@@ -24,17 +24,16 @@ module ZkFold.Symbolic.Base.Num
   , Ring
   , Field
   , Algebra
+  , Euclidean (..)
   , Real
   , SemiIntegral
   , Integral
   , Modular
-  , Euclidean (..)
   , Discrete (..)
   , Comparable (..)
     -- * Algebraic inter-constraints
   , From (..)
   , Into (..)
-  , fromSemiIntegral
   , Exponent (..), (^), (^^), (**)
   , Scalar (..)
     -- * Type level numbers
@@ -47,6 +46,7 @@ module ZkFold.Symbolic.Base.Num
   , product
   , even
   , odd
+  , fromSemiIntegral
   , knownNat
   , order
   , characteristic
@@ -172,7 +172,7 @@ type Field a =
 type Algebra x a = (Ring x, Ring a, From x a, Scalar x a)
 
 class Semiring a => Euclidean a where
-  diff :: a -> a -> a
+  absDiff :: a -> a -> a
   divMod :: a -> a -> (a,a)
   quotRem :: a -> a -> (a,a)
   eea :: a -> a -> (a,a,a)
@@ -183,8 +183,8 @@ class Semiring a => Euclidean a where
       | otherwise =
         let
           (q , r) = u `divMod` v
-          x2 = x0 `diff` (q * x1)
-          y2 = y0 `diff` (q * y1)
+          x2 = x0 `absDiff` (q * x1)
+          y2 = y0 `absDiff` (q * y1)
         in
           xEuclid x1 y1 x2 y2 v r
   gcd :: a -> a -> a
@@ -378,7 +378,7 @@ instance Discrete Integer
 instance Comparable Integer
 
 instance Euclidean Integer where
-  diff = (Prelude.-)
+  absDiff = (Prelude.-)
   divMod = Prelude.divMod
   quotRem = Prelude.quotRem
 
@@ -406,7 +406,7 @@ instance Into Rational Natural where to = Prelude.toRational
 instance Into Natural Natural
 
 instance Euclidean Natural where
-  diff a b = case compare a b of
+  absDiff a b = case compare a b of
     LT -> b Prelude.- a
     EQ -> 0
     GT -> a Prelude.- b
@@ -453,7 +453,7 @@ instance Discrete Int
 instance Comparable Int
 
 instance Euclidean Int where
-  diff = (Prelude.-)
+  absDiff = (Prelude.-)
   divMod = Prelude.divMod
   quotRem = Prelude.quotRem
 
@@ -541,7 +541,7 @@ instance (SemiIntegral int, Prime p)
 
 instance (SemiIntegral int, KnownNat n)
   => Euclidean (Mod int n) where
-    diff a b = from (diff (to @Natural a) (to b))
+    absDiff a b = from (absDiff (to @Natural a) (to b))
     divMod a b = case divMod (to @Natural a) (to b) of
       (d,m) -> (from d, from m)
     quotRem a b = case quotRem (to @Natural a) (to b) of
@@ -568,8 +568,7 @@ instance (SemiIntegral int, Prime p)
   => From Rational (Mod int p) where
     from q = from (numerator q) / from (denominator q)
 
-instance Into (Mod int n) (Mod int n) where
-  to = id
+instance Into (Mod int n) (Mod int n)
 
 instance Into int (Mod int n) where
   to = fromMod
@@ -582,18 +581,9 @@ instance Into Integer int
   => Into Integer (Mod int n) where
     to = to . fromMod
 
-instance (SemiIntegral int, KnownNat n)
+instance SemiIntegral int
   => Into Natural (Mod int n) where
-    to r =
-      let
-        int = to @Integer r
-        n = from (knownNat @n)
-        zToN = Prelude.fromIntegral
-      in
-        case compare int zero of
-          LT -> zToN (n + int)
-          EQ -> zero
-          GT -> zToN (n - int)
+    to = Prelude.fromInteger . to
 
 instance (SemiIntegral int, KnownNat n)
   => Scalar Natural (Mod int n) where

From 3d46f61476ca63e2b5e367c8358bc19ced77df78 Mon Sep 17 00:00:00 2001
From: Eitan Chatav <eitan.chatav@gmail.com>
Date: Sat, 13 Jul 2024 17:27:29 -0700
Subject: [PATCH 24/51] Update Circuit.hs

---
 src/ZkFold/Symbolic/Base/Circuit.hs | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

diff --git a/src/ZkFold/Symbolic/Base/Circuit.hs b/src/ZkFold/Symbolic/Base/Circuit.hs
index 77e84eb5d..930cde18e 100644
--- a/src/ZkFold/Symbolic/Base/Circuit.hs
+++ b/src/ZkFold/Symbolic/Base/Circuit.hs
@@ -14,6 +14,7 @@ module ZkFold.Symbolic.Base.Circuit
   , MonadCircuit (..)
   , IxMonadCircuit (..)
   , CircuitIx (..)
+  , Blueprint
   , SysVar (..)
   , OutVar (..)
   ) where
@@ -57,9 +58,12 @@ data Circuit x i o = UnsafeCircuit
     -- they can be input, constant or new variables.
   }
 
+type Blueprint x i o =
+  forall t m. (IxMonadCircuit x t, Monad m) => t i i m (o (OutVar x i))
+
 circuit
   :: (Ord x, VectorSpace x i)
-  => (forall t m. (IxMonadCircuit x t, Monad m) => t i i m (o (OutVar x i)))
+  => Blueprint x i o
   -> Circuit x i o
 circuit m = case unPar1 (runCircuitIx m mempty) of
   (o, c) -> c {outputC = o}

From f85c6e60461718a91d40b2c2bd284d24d5006f04 Mon Sep 17 00:00:00 2001
From: Eitan Chatav <eitan.chatav@gmail.com>
Date: Sat, 13 Jul 2024 17:30:56 -0700
Subject: [PATCH 25/51] Update Circuit.hs

---
 src/ZkFold/Symbolic/Base/Circuit.hs | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/src/ZkFold/Symbolic/Base/Circuit.hs b/src/ZkFold/Symbolic/Base/Circuit.hs
index 930cde18e..2e0f023b2 100644
--- a/src/ZkFold/Symbolic/Base/Circuit.hs
+++ b/src/ZkFold/Symbolic/Base/Circuit.hs
@@ -69,7 +69,7 @@ circuit m = case unPar1 (runCircuitIx m mempty) of
   (o, c) -> c {outputC = o}
 
 evalC :: (VectorSpace x i, Functor o) => Circuit x i o -> i x -> o x
-evalC c i = fmap (witnessIndex i (witnessC c)) (outputC c)
+evalC c i = fmap (indexW i (witnessC c)) (outputC c)
 
 data SysVar x i
   = InVar (Basis x i)
@@ -91,10 +91,10 @@ evalConst = mapPoly $ \case
   ConstVar x -> Left x
   SysVar v -> Right v
   
-witnessIndex
+indexW
   :: VectorSpace x i
   => i x -> IntMap (i x -> x) -> OutVar x i -> x
-witnessIndex inp witnessMap = \case
+indexW inp witnessMap = \case
   SysVar (InVar basisIx) -> indexV inp basisIx
   SysVar (NewVar ix) -> fromMaybe zero (($ inp) <$> witnessMap IntMap.!? ix)
   ConstVar x -> x
@@ -168,7 +168,7 @@ instance (Field x, Ord x, Monad m)
       let
         maxIndexMaybe = IntMap.lookupMax (witnessC c)
         newIndex = maybe 0 ((1 +) . Prelude.fst) maxIndexMaybe
-        newWitness i = w (witnessIndex i (witnessC c))
+        newWitness i = w (indexW i (witnessC c))
         outVar = SysVar (NewVar newIndex)
         newConstraint = evalConst (p var outVar)
         newSystemC = Set.insert newConstraint (systemC c)

From b25696024da38dafe04bf17d5dac362dc567a26f Mon Sep 17 00:00:00 2001
From: Eitan Chatav <eitan.chatav@gmail.com>
Date: Sat, 13 Jul 2024 17:41:32 -0700
Subject: [PATCH 26/51] Update Circuit.hs

---
 src/ZkFold/Symbolic/Base/Circuit.hs | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/src/ZkFold/Symbolic/Base/Circuit.hs b/src/ZkFold/Symbolic/Base/Circuit.hs
index 2e0f023b2..c4cebdc93 100644
--- a/src/ZkFold/Symbolic/Base/Circuit.hs
+++ b/src/ZkFold/Symbolic/Base/Circuit.hs
@@ -69,7 +69,7 @@ circuit m = case unPar1 (runCircuitIx m mempty) of
   (o, c) -> c {outputC = o}
 
 evalC :: (VectorSpace x i, Functor o) => Circuit x i o -> i x -> o x
-evalC c i = fmap (indexW i (witnessC c)) (outputC c)
+evalC c i = fmap (indexW (witnessC c) i) (outputC c)
 
 data SysVar x i
   = InVar (Basis x i)
@@ -93,8 +93,8 @@ evalConst = mapPoly $ \case
   
 indexW
   :: VectorSpace x i
-  => i x -> IntMap (i x -> x) -> OutVar x i -> x
-indexW inp witnessMap = \case
+  => IntMap (i x -> x) -> i x -> OutVar x i -> x
+indexW witnessMap inp = \case
   SysVar (InVar basisIx) -> indexV inp basisIx
   SysVar (NewVar ix) -> fromMaybe zero (($ inp) <$> witnessMap IntMap.!? ix)
   ConstVar x -> x
@@ -168,7 +168,7 @@ instance (Field x, Ord x, Monad m)
       let
         maxIndexMaybe = IntMap.lookupMax (witnessC c)
         newIndex = maybe 0 ((1 +) . Prelude.fst) maxIndexMaybe
-        newWitness i = w (indexW i (witnessC c))
+        newWitness = w . indexW (witnessC c)
         outVar = SysVar (NewVar newIndex)
         newConstraint = evalConst (p var outVar)
         newSystemC = Set.insert newConstraint (systemC c)

From 51e59a8521fff79925531a066ca608e374679884 Mon Sep 17 00:00:00 2001
From: Eitan Chatav <eitan.chatav@gmail.com>
Date: Sat, 13 Jul 2024 19:46:05 -0700
Subject: [PATCH 27/51] Update Vector.hs

---
 src/ZkFold/Symbolic/Base/Vector.hs | 19 +------------------
 1 file changed, 1 insertion(+), 18 deletions(-)

diff --git a/src/ZkFold/Symbolic/Base/Vector.hs b/src/ZkFold/Symbolic/Base/Vector.hs
index 094fb1f06..149515b31 100644
--- a/src/ZkFold/Symbolic/Base/Vector.hs
+++ b/src/ZkFold/Symbolic/Base/Vector.hs
@@ -186,13 +186,6 @@ newtype Vector (n :: Natural) a = UnsafeV (V.Vector a)
   deriving stock
     (Functor, Foldable, Traversable, Eq, Ord)
 
-instance (KnownNat n, Prelude.Show a)
-  => Prelude.Show (Vector n a) where
-    showsPrec d v
-      = Prelude.showParen (d > 10)
-      $ Prelude.showString "fromV "
-      . Prelude.showsPrec 11 (toList v)
-
 instance KnownNat n => Representable (Vector n) where
   type Rep (Vector n) = Prelude.Int
   index (UnsafeV v) i = v V.! i
@@ -213,17 +206,7 @@ instance (Field a, KnownNat n) => VectorSpace a (Vector n) where
 newtype SparseV (n :: Natural) a =
   UnsafeSparseV {fromSparseV :: IntMap a}
     deriving stock
-      (Functor, Traversable, Eq, Ord)
-
-instance Foldable (SparseV n) where
-  foldMap f v = foldMap f (fromSparseV v)
-  toList _ = Prelude.error "toList @(SparseV _) is an error, use `toListV`."
-
-instance Prelude.Show a => Prelude.Show (SparseV n a) where
-  showsPrec d v
-    = Prelude.showParen (d > 10)
-    $ Prelude.showString "sparseV "
-    . Prelude.showsPrec 11 (fromSparseV v)
+      (Functor, Foldable, Traversable, Eq, Ord)
 
 sparseV :: forall a n. (Eq a, Field a, KnownNat n) => IntMap a -> SparseV n a
 sparseV intMap = UnsafeSparseV (IntMap.foldMapWithKey sparsify intMap) where

From b1141977d178f98dab9659ec8373c807762ca9c4 Mon Sep 17 00:00:00 2001
From: Eitan Chatav <eitan.chatav@gmail.com>
Date: Sat, 13 Jul 2024 19:53:55 -0700
Subject: [PATCH 28/51] Update Vector.hs

---
 src/ZkFold/Symbolic/Base/Vector.hs | 17 +++++++++++++++--
 1 file changed, 15 insertions(+), 2 deletions(-)

diff --git a/src/ZkFold/Symbolic/Base/Vector.hs b/src/ZkFold/Symbolic/Base/Vector.hs
index 149515b31..1a35887d6 100644
--- a/src/ZkFold/Symbolic/Base/Vector.hs
+++ b/src/ZkFold/Symbolic/Base/Vector.hs
@@ -10,7 +10,7 @@ module ZkFold.Symbolic.Base.Vector
   ( -- * VectorSpace
     VectorSpace (..)
     -- * Vector types
-  , Vector (..)
+  , Vector (..), vector
   , SparseV (..), sparseV
   , Gen.U1 (..)
   , Gen.Par1 (..)
@@ -42,6 +42,7 @@ import           Data.IntMap              (IntMap)
 import qualified Data.IntMap              as IntMap
 import           Data.Kind                (Type)
 import           Data.Maybe
+import           Data.Monoid
 import           Data.Ord
 import           Data.Traversable
 import           Data.Type.Equality
@@ -182,10 +183,22 @@ instance
       (basisV @a @v <&> \bv -> basisV @a @u <&> \bu -> (bv,bu))
 
 -- | concrete vectors
-newtype Vector (n :: Natural) a = UnsafeV (V.Vector a)
+newtype Vector (n :: Natural) a = UnsafeV {fromV :: V.Vector a}
   deriving stock
     (Functor, Foldable, Traversable, Eq, Ord)
 
+vector :: forall a n. (AdditiveMonoid a, KnownNat n) => V.Vector a -> Vector n a
+vector v =
+  let
+    len = V.length v
+    n = from (knownNat @n)
+  in
+    case compare len n of
+      EQ -> UnsafeV v
+      GT -> UnsafeV (V.take n v)
+      LT -> UnsafeV (v <> V.replicate (n - len) zero)
+    
+
 instance KnownNat n => Representable (Vector n) where
   type Rep (Vector n) = Prelude.Int
   index (UnsafeV v) i = v V.! i

From 84611b33e8cb906fc43c4fce26e41400085f02a9 Mon Sep 17 00:00:00 2001
From: Eitan Chatav <eitan.chatav@gmail.com>
Date: Sat, 13 Jul 2024 19:54:38 -0700
Subject: [PATCH 29/51] Update Vector.hs

---
 src/ZkFold/Symbolic/Base/Vector.hs | 1 -
 1 file changed, 1 deletion(-)

diff --git a/src/ZkFold/Symbolic/Base/Vector.hs b/src/ZkFold/Symbolic/Base/Vector.hs
index 1a35887d6..0cb178ede 100644
--- a/src/ZkFold/Symbolic/Base/Vector.hs
+++ b/src/ZkFold/Symbolic/Base/Vector.hs
@@ -197,7 +197,6 @@ vector v =
       EQ -> UnsafeV v
       GT -> UnsafeV (V.take n v)
       LT -> UnsafeV (v <> V.replicate (n - len) zero)
-    
 
 instance KnownNat n => Representable (Vector n) where
   type Rep (Vector n) = Prelude.Int

From f3a06b23c5fc3f00b656b1c9b0b2c5d8eb2763ed Mon Sep 17 00:00:00 2001
From: Eitan Chatav <eitan.chatav@gmail.com>
Date: Sat, 13 Jul 2024 19:55:04 -0700
Subject: [PATCH 30/51] Update Vector.hs

---
 src/ZkFold/Symbolic/Base/Vector.hs | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/src/ZkFold/Symbolic/Base/Vector.hs b/src/ZkFold/Symbolic/Base/Vector.hs
index 0cb178ede..d14794cb0 100644
--- a/src/ZkFold/Symbolic/Base/Vector.hs
+++ b/src/ZkFold/Symbolic/Base/Vector.hs
@@ -187,7 +187,9 @@ newtype Vector (n :: Natural) a = UnsafeV {fromV :: V.Vector a}
   deriving stock
     (Functor, Foldable, Traversable, Eq, Ord)
 
-vector :: forall a n. (AdditiveMonoid a, KnownNat n) => V.Vector a -> Vector n a
+vector
+  :: forall a n. (AdditiveMonoid a, KnownNat n)
+  => V.Vector a -> Vector n a
 vector v =
   let
     len = V.length v

From 47ba9dbd356e3b9e07a6b31920186a318836101b Mon Sep 17 00:00:00 2001
From: Eitan Chatav <eitan.chatav@gmail.com>
Date: Sat, 13 Jul 2024 21:14:30 -0700
Subject: [PATCH 31/51] Update Num.hs

---
 src/ZkFold/Symbolic/Base/Num.hs | 6 ++++++
 1 file changed, 6 insertions(+)

diff --git a/src/ZkFold/Symbolic/Base/Num.hs b/src/ZkFold/Symbolic/Base/Num.hs
index 1f72b2a70..5ca278fa5 100644
--- a/src/ZkFold/Symbolic/Base/Num.hs
+++ b/src/ZkFold/Symbolic/Base/Num.hs
@@ -196,6 +196,12 @@ class Semiring a => Euclidean a where
   mod :: a -> a -> a
   mod a b = let (_,modulus) = divMod a b in modulus
 
+  quot :: a -> a -> a
+  quot a b = let (quotient,_) = quotRem a b in quotient
+
+  rem :: a -> a -> a
+  rem a b = let (_,remainder) = quotRem a b in remainder
+
 even :: SemiIntegral a => a -> Bool
 even a = a `mod` (from @Natural 2) == zero
 

From 33e0f7c80176123b1850a1f5e313835742cf847a Mon Sep 17 00:00:00 2001
From: Eitan Chatav <eitan.chatav@gmail.com>
Date: Sat, 13 Jul 2024 21:32:46 -0700
Subject: [PATCH 32/51] Update Num.hs

---
 src/ZkFold/Symbolic/Base/Num.hs | 26 ++++++++++----------------
 1 file changed, 10 insertions(+), 16 deletions(-)

diff --git a/src/ZkFold/Symbolic/Base/Num.hs b/src/ZkFold/Symbolic/Base/Num.hs
index 5ca278fa5..834ab015a 100644
--- a/src/ZkFold/Symbolic/Base/Num.hs
+++ b/src/ZkFold/Symbolic/Base/Num.hs
@@ -174,8 +174,18 @@ type Algebra x a = (Ring x, Ring a, From x a, Scalar x a)
 class Semiring a => Euclidean a where
   absDiff :: a -> a -> a
   divMod :: a -> a -> (a,a)
+  div :: a -> a -> a
+  div a b = let (divisor,_) = divMod a b in divisor
+  mod :: a -> a -> a
+  mod a b = let (_,modulus) = divMod a b in modulus
   quotRem :: a -> a -> (a,a)
+  quot :: a -> a -> a
+  quot a b = let (quotient,_) = quotRem a b in quotient
+  rem :: a -> a -> a
+  rem a b = let (_,remainder) = quotRem a b in remainder
   eea :: a -> a -> (a,a,a)
+
+  -- TODO: Fix & test
   default eea :: SemiIntegral a => a -> a -> (a,a,a)
   eea = xEuclid one zero zero one where
     xEuclid x0 y0 x1 y1 u v
@@ -190,18 +200,6 @@ class Semiring a => Euclidean a where
   gcd :: a -> a -> a
   gcd a b = let (d,_,_) = eea a b in d
 
-  div :: a -> a -> a
-  div a b = let (divisor,_) = divMod a b in divisor
-
-  mod :: a -> a -> a
-  mod a b = let (_,modulus) = divMod a b in modulus
-
-  quot :: a -> a -> a
-  quot a b = let (quotient,_) = quotRem a b in quotient
-
-  rem :: a -> a -> a
-  rem a b = let (_,remainder) = quotRem a b in remainder
-
 even :: SemiIntegral a => a -> Bool
 even a = a `mod` (from @Natural 2) == zero
 
@@ -558,10 +556,6 @@ residue int = int `mod` from (knownNat @n)
 
 instance From (Mod int n) (Mod int n)
 
-instance (Euclidean int, KnownNat n)
-  => From int (Mod int n) where
-    from = UnsafeMod . residue @n
-
 instance (From Natural int, Euclidean int, KnownNat n)
   => From Natural (Mod int n) where
     from = UnsafeMod . residue @n . from

From 800679e8ee7de5ede50c57934e0bdb1d6e6346be Mon Sep 17 00:00:00 2001
From: Eitan Chatav <eitan.chatav@gmail.com>
Date: Mon, 15 Jul 2024 10:36:01 -0700
Subject: [PATCH 33/51] Update Polynomial.hs

---
 src/ZkFold/Symbolic/Base/Polynomial.hs | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

diff --git a/src/ZkFold/Symbolic/Base/Polynomial.hs b/src/ZkFold/Symbolic/Base/Polynomial.hs
index 9b3294a6d..0155306a3 100644
--- a/src/ZkFold/Symbolic/Base/Polynomial.hs
+++ b/src/ZkFold/Symbolic/Base/Polynomial.hs
@@ -153,12 +153,12 @@ mapPoly
   :: (Eq x, Ord var0, Ord var1, Semiring x)
   => (var0 -> Either x var1)
   -> Poly var0 Natural x -> Poly var1 Natural x
-mapPoly f varPoly = fromList
+mapPoly f polynomial = fromList
   [
     let
-      (coefs, varList) = partitionEithers
-        [bimap (^p) (,p) (f v0) | (v0,p) <- toList varMono]
+      (coefMono, varMono) = partitionEithers
+        [bimap (,p) (,p) (f v0) | (v0,p) <- toList monomial]
     in
-      (c * product coefs, fromList varList)
-  | (c, varMono) <- toList varPoly
+      (c * evalMono coefMono, fromList varMono)
+  | (c, monomial) <- toList polynomial
   ]

From 31cead9939aef029b8b8347e67b94d5a4c125068 Mon Sep 17 00:00:00 2001
From: Eitan Chatav <eitan.chatav@gmail.com>
Date: Mon, 15 Jul 2024 12:28:17 -0700
Subject: [PATCH 34/51] split up euclidean again

---
 src/ZkFold/Symbolic/Base/Num.hs | 46 ++++++++++++++++-----------------
 1 file changed, 23 insertions(+), 23 deletions(-)

diff --git a/src/ZkFold/Symbolic/Base/Num.hs b/src/ZkFold/Symbolic/Base/Num.hs
index 834ab015a..4b3bbffbb 100644
--- a/src/ZkFold/Symbolic/Base/Num.hs
+++ b/src/ZkFold/Symbolic/Base/Num.hs
@@ -24,6 +24,7 @@ module ZkFold.Symbolic.Base.Num
   , Ring
   , Field
   , Algebra
+  , SemiEuclidean (..)
   , Euclidean (..)
   , Real
   , SemiIntegral
@@ -106,8 +107,10 @@ sum = foldl' (+) zero
 
 class AdditiveMonoid a => AdditiveGroup a where
   negate :: a -> a
+  negate a = zero - a
   infixl 6 -
   (-) :: a -> a -> a
+  a - b = a + negate b
 
 class MultiplicativeMonoid a where
   infixl 7 *
@@ -118,8 +121,11 @@ product :: (Foldable t, MultiplicativeMonoid a) => t a -> a
 product = foldl' (*) one
 
 class MultiplicativeMonoid a => MultiplicativeGroup a where
+  recip :: a -> a
+  recip a = one / a
   infixl 7 /
   (/) :: a -> a -> a
+  a / b = a * recip b
 
 -- from @Natural is the unique homomorphism from the free Semiring
 -- from @Integer is the unique homomorphism from the free Ring
@@ -171,8 +177,7 @@ type Field a =
 
 type Algebra x a = (Ring x, Ring a, From x a, Scalar x a)
 
-class Semiring a => Euclidean a where
-  absDiff :: a -> a -> a
+class Semiring a => SemiEuclidean a where
   divMod :: a -> a -> (a,a)
   div :: a -> a -> a
   div a b = let (divisor,_) = divMod a b in divisor
@@ -183,18 +188,18 @@ class Semiring a => Euclidean a where
   quot a b = let (quotient,_) = quotRem a b in quotient
   rem :: a -> a -> a
   rem a b = let (_,remainder) = quotRem a b in remainder
-  eea :: a -> a -> (a,a,a)
 
-  -- TODO: Fix & test
-  default eea :: SemiIntegral a => a -> a -> (a,a,a)
+class (SemiEuclidean a, Ring a) => Euclidean a where
+  eea :: a -> a -> (a,a,a)
+  default eea :: Eq a => a -> a -> (a,a,a)
   eea = xEuclid one zero zero one where
     xEuclid x0 y0 x1 y1 u v
       | v == zero = (u,x0,y0)
       | otherwise =
         let
           (q , r) = u `divMod` v
-          x2 = x0 `absDiff` (q * x1)
-          y2 = y0 `absDiff` (q * y1)
+          x2 = x0 - q * x1
+          y2 = y0 - q * y1
         in
           xEuclid x1 y1 x2 y2 v r
   gcd :: a -> a -> a
@@ -230,9 +235,9 @@ class Into y a where
 -- e.g. `Rational`, `Integer`, `Natural`, `Zp p`
 type Real a = (Prelude.Ord a, Semiring a, Into Rational a)
 -- e.g. `Integer`, `Natural`, `Zp p`
-type SemiIntegral a = (Real a, Euclidean a, Into Integer a)
+type SemiIntegral a = (Real a, SemiEuclidean a, Into Integer a)
 -- e.g. `Integer`, `Zp p`
-type Integral a = (SemiIntegral a, Ring a)
+type Integral a = (SemiIntegral a, Euclidean a)
 -- `Zp p` and its newtypes, also `Word8`, `Word16`, `Word32` and `Word64`
 type Modular a = (Integral a, Into Natural a)
 
@@ -381,10 +386,10 @@ instance Into Integer Integer
 instance Discrete Integer
 instance Comparable Integer
 
-instance Euclidean Integer where
-  absDiff = (Prelude.-)
+instance SemiEuclidean Integer where
   divMod = Prelude.divMod
   quotRem = Prelude.quotRem
+instance Euclidean Integer
 
 -- Natural --------------------------------------------------------------------
 
@@ -409,11 +414,7 @@ instance Into Integer Natural where to = Prelude.toInteger
 instance Into Rational Natural where to = Prelude.toRational
 instance Into Natural Natural
 
-instance Euclidean Natural where
-  absDiff a b = case compare a b of
-    LT -> b Prelude.- a
-    EQ -> 0
-    GT -> a Prelude.- b
+instance SemiEuclidean Natural where
   divMod = Prelude.divMod
   quotRem = Prelude.quotRem
 
@@ -456,10 +457,10 @@ instance Into Int Int
 instance Discrete Int
 instance Comparable Int
 
-instance Euclidean Int where
-  absDiff = (Prelude.-)
+instance SemiEuclidean Int where
   divMod = Prelude.divMod
   quotRem = Prelude.quotRem
+instance Euclidean Int
 
 -- Function -------------------------------------------------------------------
 
@@ -540,23 +541,22 @@ instance (SemiIntegral int, KnownNat n)
 
 instance (SemiIntegral int, Prime p)
   => MultiplicativeGroup (Mod int p) where
-    a / b = case eea (to @Integer a) (to b) of
+    recip a = case eea (to @Integer a) (from (knownNat @p)) of
       (_,q,_) -> from q
 
 instance (SemiIntegral int, KnownNat n)
-  => Euclidean (Mod int n) where
-    absDiff a b = from (absDiff (to @Natural a) (to b))
+  => SemiEuclidean (Mod int n) where
     divMod a b = case divMod (to @Natural a) (to b) of
       (d,m) -> (from d, from m)
     quotRem a b = case quotRem (to @Natural a) (to b) of
       (q,r) -> (from q, from r)
 
-residue :: forall n int. (Euclidean int, KnownNat n) => int -> int
+residue :: forall n int. (SemiEuclidean int, KnownNat n) => int -> int
 residue int = int `mod` from (knownNat @n)
 
 instance From (Mod int n) (Mod int n)
 
-instance (From Natural int, Euclidean int, KnownNat n)
+instance (From Natural int, SemiEuclidean int, KnownNat n)
   => From Natural (Mod int n) where
     from = UnsafeMod . residue @n . from
 

From e2ebecb0488057b6053940aaa3ddd1459db75bac Mon Sep 17 00:00:00 2001
From: Eitan Chatav <eitan.chatav@gmail.com>
Date: Mon, 15 Jul 2024 12:43:09 -0700
Subject: [PATCH 35/51] Update Num.hs

---
 src/ZkFold/Symbolic/Base/Num.hs | 44 +++++++++++++++++++++++++++------
 1 file changed, 36 insertions(+), 8 deletions(-)

diff --git a/src/ZkFold/Symbolic/Base/Num.hs b/src/ZkFold/Symbolic/Base/Num.hs
index 4b3bbffbb..f1e814cac 100644
--- a/src/ZkFold/Symbolic/Base/Num.hs
+++ b/src/ZkFold/Symbolic/Base/Num.hs
@@ -232,14 +232,34 @@ class Into y a where
   default to :: y ~ a => a -> y
   to = id
 
--- e.g. `Rational`, `Integer`, `Natural`, `Zp p`
-type Real a = (Prelude.Ord a, Semiring a, Into Rational a)
--- e.g. `Integer`, `Natural`, `Zp p`
-type SemiIntegral a = (Real a, SemiEuclidean a, Into Integer a)
--- e.g. `Integer`, `Zp p`
-type Integral a = (SemiIntegral a, Euclidean a)
--- `Zp p` and its newtypes, also `Word8`, `Word16`, `Word32` and `Word64`
-type Modular a = (Integral a, Into Natural a)
+-- e.g. `Rational`, `Integer`, `Natural`, `Mod int`
+type Real a =
+  ( Prelude.Ord a
+  , Semiring a
+  , Into Rational a
+  )
+-- e.g. `Integer`, `Natural`, `Mod int`
+type SemiIntegral a =
+  ( Prelude.Ord a
+  , SemiEuclidean a
+  , Into Rational a
+  , Into Integer a
+  )
+-- e.g. `Integer`, `Mod int`
+type Integral a =
+  ( Prelude.Ord a
+  , Euclidean a
+  , Into Rational a
+  , Into Integer a
+  )
+-- e.g. `Mod int` & fixed-width unsigned integer types
+type Modular a =
+  ( Prelude.Ord a
+  , Euclidean a
+  , Into Rational a
+  , Into Integer a
+  , Into Natural a
+  )
 
 fromSemiIntegral :: (SemiIntegral a, From Integer b) => a -> b
 fromSemiIntegral = from . to @Integer
@@ -551,6 +571,14 @@ instance (SemiIntegral int, KnownNat n)
     quotRem a b = case quotRem (to @Natural a) (to b) of
       (q,r) -> (from q, from r)
 
+instance (SemiIntegral int, KnownNat n)
+  => Euclidean (Mod int n) where
+    eea a b =
+      let
+        (d,b0,b1) = eea (to @Integer a) (to b)
+      in
+        (from d, from b0, from b1)
+
 residue :: forall n int. (SemiEuclidean int, KnownNat n) => int -> int
 residue int = int `mod` from (knownNat @n)
 

From ced989b0c816ecb94f6a0757a8f40a6922079586 Mon Sep 17 00:00:00 2001
From: Eitan Chatav <eitan.chatav@gmail.com>
Date: Mon, 15 Jul 2024 12:45:06 -0700
Subject: [PATCH 36/51] remove things

---
 src/ZkFold/Symbolic/Base/Num.hs | 12 +-----------
 1 file changed, 1 insertion(+), 11 deletions(-)

diff --git a/src/ZkFold/Symbolic/Base/Num.hs b/src/ZkFold/Symbolic/Base/Num.hs
index f1e814cac..4808f5600 100644
--- a/src/ZkFold/Symbolic/Base/Num.hs
+++ b/src/ZkFold/Symbolic/Base/Num.hs
@@ -26,7 +26,6 @@ module ZkFold.Symbolic.Base.Num
   , Algebra
   , SemiEuclidean (..)
   , Euclidean (..)
-  , Real
   , SemiIntegral
   , Integral
   , Modular
@@ -35,7 +34,7 @@ module ZkFold.Symbolic.Base.Num
     -- * Algebraic inter-constraints
   , From (..)
   , Into (..)
-  , Exponent (..), (^), (^^), (**)
+  , Exponent (..), (^), (^^)
   , Scalar (..)
     -- * Type level numbers
   , KnownNat
@@ -232,12 +231,6 @@ class Into y a where
   default to :: y ~ a => a -> y
   to = id
 
--- e.g. `Rational`, `Integer`, `Natural`, `Mod int`
-type Real a =
-  ( Prelude.Ord a
-  , Semiring a
-  , Into Rational a
-  )
 -- e.g. `Integer`, `Natural`, `Mod int`
 type SemiIntegral a =
   ( Prelude.Ord a
@@ -707,9 +700,6 @@ infixr 8 ^^
 (^^) :: (Exponent Integer a, Into Integer pow) => a -> pow -> a
 a ^^ b = exponent @Integer a (to b)
 
-(**) :: (Exponent Rational a, Into Rational pow) => a -> pow -> a
-a ** b = exponent @Rational a (to b)
-
 evalMonoN
   :: (Into Natural p, MultiplicativeMonoid a)
   => [(a,p)] -> a

From 143addd6cedf93aa2b7c7b1fda16434791c0559b Mon Sep 17 00:00:00 2001
From: Eitan Chatav <eitan.chatav@gmail.com>
Date: Mon, 15 Jul 2024 12:48:36 -0700
Subject: [PATCH 37/51] Update Num.hs

---
 src/ZkFold/Symbolic/Base/Num.hs | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/src/ZkFold/Symbolic/Base/Num.hs b/src/ZkFold/Symbolic/Base/Num.hs
index 4808f5600..4f1230251 100644
--- a/src/ZkFold/Symbolic/Base/Num.hs
+++ b/src/ZkFold/Symbolic/Base/Num.hs
@@ -81,7 +81,7 @@ type Arithmetic x a =
   ( Algebra x a
   , Comparable a
   , FiniteChr a
-  , 3 <= Chr x
+  , 3 <= Chr a
   )
 
 -- Prime fields should only include:
@@ -92,7 +92,6 @@ type PrimeField x =
   , Arithmetic x x
   , Finite x
   , Field x
-  , FiniteChr x
   , Order x ~ Chr x
   )
 

From 8072953e0040129eaf0421ca9f5a98d140674723 Mon Sep 17 00:00:00 2001
From: Eitan Chatav <eitan.chatav@gmail.com>
Date: Mon, 15 Jul 2024 12:55:09 -0700
Subject: [PATCH 38/51] Update Num.hs

---
 src/ZkFold/Symbolic/Base/Num.hs | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/src/ZkFold/Symbolic/Base/Num.hs b/src/ZkFold/Symbolic/Base/Num.hs
index 4f1230251..d19f25bc7 100644
--- a/src/ZkFold/Symbolic/Base/Num.hs
+++ b/src/ZkFold/Symbolic/Base/Num.hs
@@ -46,6 +46,7 @@ module ZkFold.Symbolic.Base.Num
   , product
   , even
   , odd
+  , fromInteger
   , fromSemiIntegral
   , knownNat
   , order
@@ -256,6 +257,9 @@ type Modular a =
 fromSemiIntegral :: (SemiIntegral a, From Integer b) => a -> b
 fromSemiIntegral = from . to @Integer
 
+fromInteger :: From Integer b => Integer -> b
+fromInteger = from
+
 -- Type level numbers ---------------------------------------------------------
 
 knownNat :: forall n. KnownNat n => Natural

From 5d46c89894b4e210ad357fc3d29dbddb0748e585 Mon Sep 17 00:00:00 2001
From: Eitan Chatav <eitan.chatav@gmail.com>
Date: Mon, 15 Jul 2024 16:31:05 -0700
Subject: [PATCH 39/51] Update Circuit.hs

---
 src/ZkFold/Symbolic/Base/Circuit.hs | 41 ++++++++++++++---------------
 1 file changed, 20 insertions(+), 21 deletions(-)

diff --git a/src/ZkFold/Symbolic/Base/Circuit.hs b/src/ZkFold/Symbolic/Base/Circuit.hs
index c4cebdc93..21f0c3dda 100644
--- a/src/ZkFold/Symbolic/Base/Circuit.hs
+++ b/src/ZkFold/Symbolic/Base/Circuit.hs
@@ -108,27 +108,26 @@ instance (Ord x, VectorSpace x i, o ~ U1) => Semigroup (Circuit x i o) where
     , outputC = U1
     }
 
-class Monad m
-  => MonadCircuit x i m | m -> x, m -> i where
-    runCircuit
-      :: VectorSpace x i
-      => Circuit x i o -> m (o (OutVar x i))
-    input :: VectorSpace x i => m (i (OutVar x i))
-    input = return (fmap (SysVar . InVar) (basisV @x))
-    constraint
-      :: VectorSpace x i
-      => (forall a. Algebra x a => (OutVar x i -> a) -> a)
-      -> m ()
-    newConstrained
-      :: VectorSpace x i
-      => (forall a. Algebra x a => (OutVar x i -> a) -> OutVar x i -> a)
-      -> ((OutVar x i -> x) -> x)
-      -> m (OutVar x i)
-    newAssigned
-      :: VectorSpace x i
-      => (forall a. Algebra x a => (OutVar x i -> a) -> a)
-      -> m (OutVar x i)
-    newAssigned p = newConstrained (\x i -> p x - x i) p
+class Monad m => MonadCircuit x i m | m -> x, m -> i where
+  runCircuit
+    :: VectorSpace x i
+    => Circuit x i o -> m (o (OutVar x i))
+  input :: VectorSpace x i => m (i (OutVar x i))
+  input = return (fmap (SysVar . InVar) (basisV @x))
+  constraint
+    :: VectorSpace x i
+    => (forall a. Algebra x a => (OutVar x i -> a) -> a)
+    -> m ()
+  newConstrained
+    :: VectorSpace x i
+    => (forall a. Algebra x a => (OutVar x i -> a) -> OutVar x i -> a)
+    -> ((OutVar x i -> x) -> x)
+    -> m (OutVar x i)
+  newAssigned
+    :: VectorSpace x i
+    => (forall a. Algebra x a => (OutVar x i -> a) -> a)
+    -> m (OutVar x i)
+  newAssigned p = newConstrained (\x i -> p x - x i) p
 
 class
   ( forall i m. Monad m => MonadCircuit x i (t i i m)

From ec2dd025194f22d77295b5ec7299024231221230 Mon Sep 17 00:00:00 2001
From: Eitan Chatav <eitan.chatav@gmail.com>
Date: Mon, 15 Jul 2024 16:31:08 -0700
Subject: [PATCH 40/51] Update Num.hs

---
 src/ZkFold/Symbolic/Base/Num.hs | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/ZkFold/Symbolic/Base/Num.hs b/src/ZkFold/Symbolic/Base/Num.hs
index d19f25bc7..92689dfd4 100644
--- a/src/ZkFold/Symbolic/Base/Num.hs
+++ b/src/ZkFold/Symbolic/Base/Num.hs
@@ -662,7 +662,7 @@ class (Semiring c, AdditiveMonoid a)
     scale = (*)
     combine :: [(c,a)] -> a
     default combine :: c ~ a => [(c,a)] -> a
-    combine = product . fmap (Prelude.uncurry (*))
+    combine = sum . fmap (Prelude.uncurry (*))
 
 combineN
   :: (Into Natural c, AdditiveMonoid a)

From 8af5d8b569ce449e7189260769a2be8b3586751a Mon Sep 17 00:00:00 2001
From: Eitan Chatav <eitan.chatav@gmail.com>
Date: Mon, 15 Jul 2024 21:26:38 -0700
Subject: [PATCH 41/51] Update Num.hs

---
 src/ZkFold/Symbolic/Base/Num.hs | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/ZkFold/Symbolic/Base/Num.hs b/src/ZkFold/Symbolic/Base/Num.hs
index 92689dfd4..6a3418af3 100644
--- a/src/ZkFold/Symbolic/Base/Num.hs
+++ b/src/ZkFold/Symbolic/Base/Num.hs
@@ -673,7 +673,7 @@ combineN combination = combineNat naturalized where
   combineNat terms =
     let
       halves = combineNat [(c `div` 2, a) | (c,a) <- terms, c > 1]
-      halveNots = sum [a | (c,a) <- terms, Prelude.odd c]
+      halveNots = sum [a | (c,a) <- terms, odd c]
     in
       halves + halves + halveNots
 
@@ -712,6 +712,6 @@ evalMonoN monomial = evalMonoNat naturalized where
   evalMonoNat factors =
     let
       sqrts = evalMonoNat [(a,p `div` 2) | (a,p) <- factors, p > 1]
-      sqrtNots = product [a | (a,p) <- factors, Prelude.odd p]
+      sqrtNots = product [a | (a,p) <- factors, odd p]
     in
       sqrts * sqrts * sqrtNots

From 06214287512338f6d05cecc4d663836756e8b9f0 Mon Sep 17 00:00:00 2001
From: TurtlePU <sokolov.p64@gmail.com>
Date: Tue, 16 Jul 2024 21:37:33 +0300
Subject: [PATCH 42/51] + some algebra instances for Circuit

---
 src/ZkFold/Symbolic/Base/Circuit.hs | 74 +++++++++++++++++++++++++++++
 src/ZkFold/Symbolic/Base/Num.hs     |  3 ++
 2 files changed, 77 insertions(+)

diff --git a/src/ZkFold/Symbolic/Base/Circuit.hs b/src/ZkFold/Symbolic/Base/Circuit.hs
index 21f0c3dda..856f2a9f0 100644
--- a/src/ZkFold/Symbolic/Base/Circuit.hs
+++ b/src/ZkFold/Symbolic/Base/Circuit.hs
@@ -224,6 +224,28 @@ instance (Ord x, VectorSpace x i)
       Par1 v1 <- runCircuit c1
       Par1 <$> newAssigned (\x -> x v0 + x v1)
 
+instance (Ord x, VectorSpace x i)
+  => AdditiveGroup (Circuit x i Par1) where
+    negate c = circuit $ do
+      Par1 v <- runCircuit c
+      Par1 <$> newAssigned (\x -> negate (x v))
+    c0 - c1 = circuit $ do
+      Par1 v0 <- runCircuit c0
+      Par1 v1 <- runCircuit c1
+      Par1 <$> newAssigned (\x -> x v0 - x v1)
+
+instance (Ord x, VectorSpace x i)
+  => From Natural (Circuit x i Par1) where
+    from = from @x . from
+
+instance (Ord x, VectorSpace x i)
+  => From Integer (Circuit x i Par1) where
+    from = from @x . from
+
+instance (Ord x, VectorSpace x i)
+  => From Rational (Circuit x i Par1) where
+    from = from @x . from
+
 instance (Ord x, VectorSpace x i)
   => MultiplicativeMonoid (Circuit x i Par1) where
     one = from @x one
@@ -231,3 +253,55 @@ instance (Ord x, VectorSpace x i)
       Par1 v0 <- runCircuit c0
       Par1 v1 <- runCircuit c1
       Par1 <$> newAssigned (\x -> x v0 * x v1)
+
+instance (Ord x, Discrete x, VectorSpace x i)
+  => MultiplicativeGroup (Circuit x i Par1) where
+    recip c = let c'@(UnsafeCircuit _ _ (_ :*: i)) = invertC c in c' { outputC = i }
+
+instance From (Circuit x i Par1) (Circuit x i Par1)
+
+instance (Ord x, VectorSpace x i)
+  => Scalar Natural (Circuit x i Par1) where
+    scale = scale @x . from
+    combine = combineN
+
+instance (Ord x, VectorSpace x i)
+  => Scalar Integer (Circuit x i Par1) where
+    scale = scale @x . from
+    combine = combineZ
+
+instance (Ord x, VectorSpace x i)
+  => Scalar Rational (Circuit x i Par1) where
+    scale = scale @x . from
+    combine xs = sum [ scale k x | (k, x) <- xs ]
+
+instance (Ord x, VectorSpace x i)
+  => Scalar x (Circuit x i Par1) where
+    scale k c = circuit $ do
+      Par1 v <- runCircuit c
+      Par1 <$> newAssigned (\x -> k `scale` x v)
+    combine xs = sum [ scale k x | (k, x) <- xs ]
+
+instance (Ord x, VectorSpace x i)
+  => Scalar (Circuit x i Par1) (Circuit x i Par1)
+
+instance (Ord x, VectorSpace x i)
+  => Exponent Natural (Circuit x i Par1) where
+    exponent x p = evalMono [(x, p)]
+    evalMono = evalMonoN
+
+instance (Ord x, Discrete x, VectorSpace x i)
+  => Discrete (Circuit x i Par1) where
+    dichotomy x y = isZero (x - y)
+    isZero c = let c'@(UnsafeCircuit _ _ (z :*: _)) = invertC c in c' { outputC = z }
+
+invertC :: (Ord x, Discrete x, VectorSpace x i) => Circuit x i Par1 -> Circuit x i (Par1 :*: Par1)
+invertC c = circuit $ do
+  Par1 v <- runCircuit c
+  isZ <- newConstrained
+    (\x i -> let xi = x i in xi * (xi - one))
+    (\x -> isZero (x v))
+  inv <- newConstrained
+    (\x i -> x i * x v + x isZ - one)
+    (\x -> recip (x v))
+  return (Par1 isZ :*: Par1 inv)
diff --git a/src/ZkFold/Symbolic/Base/Num.hs b/src/ZkFold/Symbolic/Base/Num.hs
index 6a3418af3..7c674276a 100644
--- a/src/ZkFold/Symbolic/Base/Num.hs
+++ b/src/ZkFold/Symbolic/Base/Num.hs
@@ -214,6 +214,9 @@ class Ring a => Discrete a where
   dichotomy :: a -> a -> a
   default dichotomy :: Eq a => a -> a -> a
   dichotomy a b = if a == b then one else zero
+  isZero :: a -> a
+  default isZero :: a -> a
+  isZero = dichotomy zero
 
 class Discrete a => Comparable a where
   trichotomy :: a -> a -> a

From e26055ffbd0dff6ecfc3b78b942c36db9cf2c001 Mon Sep 17 00:00:00 2001
From: Eitan Chatav <eitan.chatav@gmail.com>
Date: Tue, 16 Jul 2024 12:16:58 -0700
Subject: [PATCH 43/51] horner

---
 src/ZkFold/Symbolic/Base/Circuit.hs | 41 +++++++++++++++++++++--------
 1 file changed, 30 insertions(+), 11 deletions(-)

diff --git a/src/ZkFold/Symbolic/Base/Circuit.hs b/src/ZkFold/Symbolic/Base/Circuit.hs
index 856f2a9f0..a8abd9752 100644
--- a/src/ZkFold/Symbolic/Base/Circuit.hs
+++ b/src/ZkFold/Symbolic/Base/Circuit.hs
@@ -26,6 +26,7 @@ import Control.Monad.Trans
 import Control.Monad.Trans.Indexed
 import Data.Either
 import Data.Eq
+import Data.Foldable hiding (sum, product)
 import Data.Function (($))
 import Data.IntMap (IntMap)
 import qualified Data.IntMap as IntMap
@@ -90,7 +91,7 @@ evalConst
 evalConst = mapPoly $ \case
   ConstVar x -> Left x
   SysVar v -> Right v
-  
+
 indexW
   :: VectorSpace x i
   => IntMap (i x -> x) -> i x -> OutVar x i -> x
@@ -254,10 +255,6 @@ instance (Ord x, VectorSpace x i)
       Par1 v1 <- runCircuit c1
       Par1 <$> newAssigned (\x -> x v0 * x v1)
 
-instance (Ord x, Discrete x, VectorSpace x i)
-  => MultiplicativeGroup (Circuit x i Par1) where
-    recip c = let c'@(UnsafeCircuit _ _ (_ :*: i)) = invertC c in c' { outputC = i }
-
 instance From (Circuit x i Par1) (Circuit x i Par1)
 
 instance (Ord x, VectorSpace x i)
@@ -290,12 +287,9 @@ instance (Ord x, VectorSpace x i)
     exponent x p = evalMono [(x, p)]
     evalMono = evalMonoN
 
-instance (Ord x, Discrete x, VectorSpace x i)
-  => Discrete (Circuit x i Par1) where
-    dichotomy x y = isZero (x - y)
-    isZero c = let c'@(UnsafeCircuit _ _ (z :*: _)) = invertC c in c' { outputC = z }
-
-invertC :: (Ord x, Discrete x, VectorSpace x i) => Circuit x i Par1 -> Circuit x i (Par1 :*: Par1)
+invertC
+  :: (Ord x, Discrete x, VectorSpace x i)
+  => Circuit x i Par1 -> Circuit x i (Par1 :*: Par1)
 invertC c = circuit $ do
   Par1 v <- runCircuit c
   isZ <- newConstrained
@@ -305,3 +299,28 @@ invertC c = circuit $ do
     (\x i -> x i * x v + x isZ - one)
     (\x -> recip (x v))
   return (Par1 isZ :*: Par1 inv)
+
+instance (Ord x, Discrete x, VectorSpace x i)
+  => Discrete (Circuit x i Par1) where
+    dichotomy x y = isZero (x - y)
+      let
+        cInv = invertC c
+        oZ :*: _ = outputC cInv
+      in
+        cInv { outputC = oZ }
+
+instance (Ord x, Discrete x, VectorSpace x i)
+  => MultiplicativeGroup (Circuit x i Par1) where
+    recip c =
+      let
+        cInv = invertC c
+        _ :*: oInv = outputC cInv
+      in
+        cInv { outputC = oInv }
+
+horner :: (VectorSpace x i, MonadCircuit x i m) => [OutVar x i] -> m (OutVar x i)
+-- ^ @horner [b0,...,bn]@ computes the sum @b0 + 2 b1 + ... + 2^n bn@ using
+-- Horner's scheme.
+horner xs = case Prelude.reverse xs of
+  []       -> newAssigned (Prelude.const zero)
+  (b : bs) -> foldlM (\a i -> newAssigned (\x -> let xa = x a in x i + xa + xa)) b bs

From 31db6f54e4c6912d78024e91be0bb831e947d8ef Mon Sep 17 00:00:00 2001
From: Eitan Chatav <eitan.chatav@gmail.com>
Date: Thu, 18 Jul 2024 12:10:52 -0700
Subject: [PATCH 44/51] binary expansion

---
 src/ZkFold/Symbolic/Base/Circuit.hs | 123 ++++++++++++++++++++--------
 src/ZkFold/Symbolic/Base/Num.hs     |  33 +++++---
 2 files changed, 109 insertions(+), 47 deletions(-)

diff --git a/src/ZkFold/Symbolic/Base/Circuit.hs b/src/ZkFold/Symbolic/Base/Circuit.hs
index a8abd9752..a4dd2dfee 100644
--- a/src/ZkFold/Symbolic/Base/Circuit.hs
+++ b/src/ZkFold/Symbolic/Base/Circuit.hs
@@ -16,7 +16,9 @@ module ZkFold.Symbolic.Base.Circuit
   , CircuitIx (..)
   , Blueprint
   , SysVar (..)
-  , OutVar (..)
+  , Var (..)
+  , Register (..)
+  , binaryExpansion
   ) where
 
 import Control.Applicative
@@ -36,7 +38,9 @@ import Data.Ord
 import Data.Semigroup
 import Data.Set (Set)
 import qualified Data.Set as Set
+import Data.Traversable
 import Data.Type.Equality
+import qualified Data.Vector as V
 import qualified Prelude
 
 import           ZkFold.Symbolic.Base.Num
@@ -54,13 +58,13 @@ data Circuit x i o = UnsafeCircuit
     -- ^ The witness generation map,
     -- witness functions for new variables.
     -- Input and constant variables don't need witness functions.
-  , outputC  :: o (OutVar x i)
+  , outputC  :: o (Var x i)
     -- ^ The output variables,
     -- they can be input, constant or new variables.
   }
 
 type Blueprint x i o =
-  forall t m. (IxMonadCircuit x t, Monad m) => t i i m (o (OutVar x i))
+  forall t m. (IxMonadCircuit x t, Monad m) => t i i m (o (Var x i))
 
 circuit
   :: (Ord x, VectorSpace x i)
@@ -78,15 +82,15 @@ data SysVar x i
 deriving stock instance VectorSpace x i => Eq (SysVar x i)
 deriving stock instance VectorSpace x i => Ord (SysVar x i)
 
-data OutVar x i
+data Var x i
   = SysVar (SysVar x i)
   | ConstVar x
-deriving stock instance (Eq x, VectorSpace x i) => Eq (OutVar x i)
-deriving stock instance (Ord x, VectorSpace x i) => Ord (OutVar x i)
+deriving stock instance (Eq x, VectorSpace x i) => Eq (Var x i)
+deriving stock instance (Ord x, VectorSpace x i) => Ord (Var x i)
 
 evalConst
   :: (Ord x, VectorSpace x i)
-  => Poly (OutVar x i) Natural x
+  => Poly (Var x i) Natural x
   -> Poly (SysVar x i) Natural x
 evalConst = mapPoly $ \case
   ConstVar x -> Left x
@@ -94,7 +98,7 @@ evalConst = mapPoly $ \case
 
 indexW
   :: VectorSpace x i
-  => IntMap (i x -> x) -> i x -> OutVar x i -> x
+  => IntMap (i x -> x) -> i x -> Var x i -> x
 indexW witnessMap inp = \case
   SysVar (InVar basisIx) -> indexV inp basisIx
   SysVar (NewVar ix) -> fromMaybe zero (($ inp) <$> witnessMap IntMap.!? ix)
@@ -112,22 +116,22 @@ instance (Ord x, VectorSpace x i, o ~ U1) => Semigroup (Circuit x i o) where
 class Monad m => MonadCircuit x i m | m -> x, m -> i where
   runCircuit
     :: VectorSpace x i
-    => Circuit x i o -> m (o (OutVar x i))
-  input :: VectorSpace x i => m (i (OutVar x i))
+    => Circuit x i o -> m (o (Var x i))
+  input :: VectorSpace x i => m (i (Var x i))
   input = return (fmap (SysVar . InVar) (basisV @x))
   constraint
     :: VectorSpace x i
-    => (forall a. Algebra x a => (OutVar x i -> a) -> a)
+    => (forall a. Algebra x a => (Var x i -> a) -> a)
     -> m ()
   newConstrained
     :: VectorSpace x i
-    => (forall a. Algebra x a => (OutVar x i -> a) -> OutVar x i -> a)
-    -> ((OutVar x i -> x) -> x)
-    -> m (OutVar x i)
+    => (forall a. Algebra x a => (Var x i -> a) -> Var x i -> a)
+    -> ((Var x i -> x) -> x)
+    -> m (Var x i)
   newAssigned
     :: VectorSpace x i
-    => (forall a. Algebra x a => (OutVar x i -> a) -> a)
-    -> m (OutVar x i)
+    => (forall a. Algebra x a => (Var x i -> a) -> a)
+    -> m (Var x i)
   newAssigned p = newConstrained (\x i -> p x - x i) p
 
 class
@@ -287,6 +291,25 @@ instance (Ord x, VectorSpace x i)
     exponent x p = evalMono [(x, p)]
     evalMono = evalMonoN
 
+instance (Ord x, Discrete x, VectorSpace x i)
+  => MultiplicativeGroup (Circuit x i Par1) where
+    recip c =
+      let
+        cInv = invertC c
+        _ :*: oInv = outputC cInv
+      in
+        cInv { outputC = oInv }
+
+instance (Ord x, Discrete x, VectorSpace x i)
+  => Discrete (Circuit x i Par1) where
+    dichotomy x y = isZero (x - y)
+    isZero c =
+      let
+        cInv = invertC c
+        isZ :*: _ = outputC cInv
+      in
+        cInv { outputC = isZ }
+
 invertC
   :: (Ord x, Discrete x, VectorSpace x i)
   => Circuit x i Par1 -> Circuit x i (Par1 :*: Par1)
@@ -300,27 +323,55 @@ invertC c = circuit $ do
     (\x -> recip (x v))
   return (Par1 isZ :*: Par1 inv)
 
-instance (Ord x, Discrete x, VectorSpace x i)
-  => Discrete (Circuit x i Par1) where
-    dichotomy x y = isZero (x - y)
-      let
-        cInv = invertC c
-        oZ :*: _ = outputC cInv
-      in
-        cInv { outputC = oZ }
-
-instance (Ord x, Discrete x, VectorSpace x i)
-  => MultiplicativeGroup (Circuit x i Par1) where
-    recip c =
-      let
-        cInv = invertC c
-        _ :*: oInv = outputC cInv
-      in
-        cInv { outputC = oInv }
+-- A list of bits whose length is the number of bits
+-- needed to represent an element of
+-- the arithmetic field of a symbolic field extension.
+newtype Register a = UnsafeRegister {fromRegister :: V.Vector a}
+  deriving stock (Functor, Foldable, Traversable)
+instance Symbolic a => VectorSpace a Register where
+  type Basis a Register = Int
+  indexV (UnsafeRegister v) ix = fromMaybe zero (v V.!? ix)
+  dimV = numberOfBits @(Arithmetic a)
+  basisV = UnsafeRegister (V.generate (from (dimV @a @Register)) id)
+  tabulateV f = UnsafeRegister (V.generate (from (dimV @a @Register)) f)
+
+binaryExpansion
+  :: forall x i. (PrimeField x, VectorSpace x i)
+  => Circuit x i Par1
+  -> Circuit x i Register
+binaryExpansion c = circuit $ do
+  Par1 v <- runCircuit c
+  lst <- expansion (from (numberOfBits @x)) v
+  return (UnsafeRegister (V.fromList lst))
 
-horner :: (VectorSpace x i, MonadCircuit x i m) => [OutVar x i] -> m (OutVar x i)
+horner
+  :: (VectorSpace x i, MonadCircuit x i m)
+  => [Var x i] -> m (Var x i)
 -- ^ @horner [b0,...,bn]@ computes the sum @b0 + 2 b1 + ... + 2^n bn@ using
 -- Horner's scheme.
 horner xs = case Prelude.reverse xs of
-  []       -> newAssigned (Prelude.const zero)
-  (b : bs) -> foldlM (\a i -> newAssigned (\x -> let xa = x a in x i + xa + xa)) b bs
+  []       -> return (ConstVar zero)
+  (b : bs) ->
+    foldlM (\a i -> newAssigned (\x -> let xa = x a in x i + xa + xa)) b bs
+
+bitsOf
+  :: (SemiEuclidean x, VectorSpace x i, MonadCircuit x i m)
+  => Int -> Var x i -> m [Var x i]
+-- ^ @bitsOf n k@ creates @n@ bits and
+-- sets their witnesses equal to @n@ smaller bits of @k@.
+bitsOf n k = for [0 .. n - 1] $ \j -> newConstrained
+  (\x i -> let xi = x i in xi * (xi - one))
+  ((Prelude.!! j) . expand . ($ k))
+    where
+      two = from (2 :: Natural)
+      expand x = let (d,m) = divMod x two in m : expand d
+
+expansion
+  :: (SemiEuclidean x, VectorSpace x i, MonadCircuit x i m)
+  => Int -> Var x i -> m [Var x i]
+-- ^ @expansion n k@ computes a binary expansion of @k@ if it fits in @n@ bits.
+expansion n k = do
+    bits <- bitsOf n k
+    k' <- horner bits
+    constraint (\x -> x k - x k')
+    return bits
diff --git a/src/ZkFold/Symbolic/Base/Num.hs b/src/ZkFold/Symbolic/Base/Num.hs
index 7c674276a..0c48f6221 100644
--- a/src/ZkFold/Symbolic/Base/Num.hs
+++ b/src/ZkFold/Symbolic/Base/Num.hs
@@ -13,7 +13,7 @@ module ZkFold.Symbolic.Base.Num
   , Int
   , Mod
     -- * Arithmetic constraints
-  , Arithmetic
+  , Symbolic (..)
   , PrimeField
     -- * Algebraic constraints
   , AdditiveMonoid (..)
@@ -50,6 +50,7 @@ module ZkFold.Symbolic.Base.Num
   , fromSemiIntegral
   , knownNat
   , order
+  , numberOfBits
   , characteristic
   , combineN
   , combineZ
@@ -74,26 +75,30 @@ import qualified GHC.TypeNats        as Type
 import           Prelude             (Int, Integer)
 import qualified Prelude
 
--- Arithmetic algebras should include:
--- PrimeField x => Arithmetic x x
--- PrimeField x => Arithmetic x (i -> x)
--- PrimeField x => Arithmetic x (Circuit x i Par1)
-type Arithmetic x a =
-  ( Algebra x a
+-- Symbolic field extensions [Arithmetic a : a] should include:
+-- PrimeField x => Symbolic x
+-- PrimeField x => Symbolic (i -> x)
+-- PrimeField x => Symbolic (Circuit x i Par1)
+class
+  ( Field a
   , Comparable a
   , FiniteChr a
   , 3 <= Chr a
-  )
+  , PrimeField (Arithmetic a)
+  , Algebra (Arithmetic a) a
+  , Chr a ~ Order (Arithmetic a)
+  ) => Symbolic a where
+  type Arithmetic a
 
 -- Prime fields should only include:
 -- (SemiIntegral int, Prime p) => PrimeField (int `Mod` p)
 -- and newtypes of int `Mod` p.
+-- p = 2 is ruled out to allow/require trichotomy.
 type PrimeField x =
   ( Modular x
-  , Arithmetic x x
+  , Arithmetic x ~ x
   , Finite x
-  , Field x
-  , Order x ~ Chr x
+  , Symbolic x
   )
 
 class AdditiveMonoid a where
@@ -270,12 +275,18 @@ knownNat = natVal' (proxy# @n)
 
 class
   ( KnownNat (Order a)
+  , KnownNat (NumberOfBits a)
   ) => Finite a where
     type Order a :: Natural
 
 order :: forall a. Finite a => Natural
 order = knownNat @(Order a)
 
+type NumberOfBits a = Log2 (Order a - 1) + 1
+
+numberOfBits :: forall a. Finite a => Natural
+numberOfBits = knownNat @(NumberOfBits a)
+
 class
   ( KnownNat (Chr a)
   , Semiring a

From 6dee49ee91be2ee9e2b0ff11ffb1164eb0f37c87 Mon Sep 17 00:00:00 2001
From: Eitan Chatav <eitan.chatav@gmail.com>
Date: Thu, 18 Jul 2024 13:04:00 -0700
Subject: [PATCH 45/51] Update Circuit.hs

---
 src/ZkFold/Symbolic/Base/Circuit.hs | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/src/ZkFold/Symbolic/Base/Circuit.hs b/src/ZkFold/Symbolic/Base/Circuit.hs
index a4dd2dfee..9d21eae47 100644
--- a/src/ZkFold/Symbolic/Base/Circuit.hs
+++ b/src/ZkFold/Symbolic/Base/Circuit.hs
@@ -296,9 +296,9 @@ instance (Ord x, Discrete x, VectorSpace x i)
     recip c =
       let
         cInv = invertC c
-        _ :*: oInv = outputC cInv
+        _ :*: inv = outputC cInv
       in
-        cInv { outputC = oInv }
+        cInv { outputC = inv }
 
 instance (Ord x, Discrete x, VectorSpace x i)
   => Discrete (Circuit x i Par1) where
@@ -325,7 +325,7 @@ invertC c = circuit $ do
 
 -- A list of bits whose length is the number of bits
 -- needed to represent an element of
--- the arithmetic field of a symbolic field extension.
+-- the Arithmetic field of a Symbolic field extension.
 newtype Register a = UnsafeRegister {fromRegister :: V.Vector a}
   deriving stock (Functor, Foldable, Traversable)
 instance Symbolic a => VectorSpace a Register where

From 2eb906a1c417cb84aaeed18c2ee53a41d11b011c Mon Sep 17 00:00:00 2001
From: Eitan Chatav <eitan.chatav@gmail.com>
Date: Fri, 19 Jul 2024 11:33:02 -0700
Subject: [PATCH 46/51] functions and compile

---
 src/ZkFold/Symbolic/Base/Circuit.hs  | 29 +++++++++++++++
 src/ZkFold/Symbolic/Base/Function.hs | 53 +++++++++++++++++++++++++++-
 2 files changed, 81 insertions(+), 1 deletion(-)

diff --git a/src/ZkFold/Symbolic/Base/Circuit.hs b/src/ZkFold/Symbolic/Base/Circuit.hs
index 9d21eae47..651b40cbc 100644
--- a/src/ZkFold/Symbolic/Base/Circuit.hs
+++ b/src/ZkFold/Symbolic/Base/Circuit.hs
@@ -19,6 +19,9 @@ module ZkFold.Symbolic.Base.Circuit
   , Var (..)
   , Register (..)
   , binaryExpansion
+  , compileC
+  , desolderC
+  , solderC
   ) where
 
 import Control.Applicative
@@ -43,6 +46,7 @@ import Data.Type.Equality
 import qualified Data.Vector as V
 import qualified Prelude
 
+import           ZkFold.Symbolic.Base.Function
 import           ZkFold.Symbolic.Base.Num
 import           ZkFold.Symbolic.Base.Polynomial
 import           ZkFold.Symbolic.Base.Vector
@@ -375,3 +379,28 @@ expansion n k = do
     k' <- horner bits
     constraint (\x -> x k - x k')
     return bits
+
+solderC
+  :: (Ord x, VectorSpace x i, Functor o, Foldable o)
+  => o (Circuit x i Par1)
+  -> Circuit x i o
+solderC cs = (fold (fmap (\c -> c {outputC = U1}) cs))
+  { outputC = fmap (unPar1 . outputC) cs }
+
+desolderC
+  :: (Functor o)
+  => Circuit x i o
+  -> o (Circuit x i Par1)
+desolderC c = fmap (\o -> c {outputC = Par1 o}) (outputC c)
+
+compileC
+  :: ( FunctionSpace (Circuit x i Par1) f
+     , i ~ InputSpace (Circuit x i Par1) f
+     , o ~ OutputSpace (Circuit x i Par1) f
+     , VectorSpace x i
+     , Functor o
+     , Foldable o
+     , Ord x
+     )
+  => f -> Circuit x i o
+compileC f = solderC (uncurryF f (desolderC (circuit input)))
diff --git a/src/ZkFold/Symbolic/Base/Function.hs b/src/ZkFold/Symbolic/Base/Function.hs
index 1e68cb99a..13bd29d78 100644
--- a/src/ZkFold/Symbolic/Base/Function.hs
+++ b/src/ZkFold/Symbolic/Base/Function.hs
@@ -1,3 +1,54 @@
+{-# LANGUAGE AllowAmbiguousTypes     #-}
+{-# LANGUAGE DerivingStrategies      #-}
+{-# LANGUAGE MagicHash               #-}
+{-# LANGUAGE TypeOperators           #-}
+{-# LANGUAGE UndecidableInstances    #-}
+{-# LANGUAGE UndecidableSuperClasses #-}
+
 module ZkFold.Symbolic.Base.Function
-  (
+  ( FunctionSpace (..)
+  , InputSpace
+  , OutputSpace
   ) where
+
+import Control.Category
+import Data.Type.Equality
+
+import ZkFold.Symbolic.Base.Vector
+
+{- | `FunctionSpace` class of functions over variables.
+
+The type @FunctionSpace a f => f@ should be equal to some
+
+@vN a -> .. -> v1 a -> v0 a@
+
+which via multiple-uncurrying is equivalent to
+
+@(vN :*: .. :*: v1 :*: U1) a -> v0 a@
+-}
+class FunctionSpace a f where
+  uncurryF :: f -> InputSpace a f a -> OutputSpace a f a
+  curryF :: (InputSpace a f a -> OutputSpace a f a) -> f
+
+type family InputSpace a f where
+  InputSpace a (x a -> f) = x :*: InputSpace a f
+  InputSpace a (y a) = U1
+
+type family OutputSpace a f where
+  OutputSpace a (x a -> f) = OutputSpace a f
+  OutputSpace a (y a) = y
+
+instance {-# OVERLAPPABLE #-}
+  ( OutputSpace a (y a) ~ y
+  , InputSpace a (y a) ~ U1
+  ) => FunctionSpace a (y a) where
+    uncurryF f _ = f
+    curryF k = k U1
+
+instance {-# OVERLAPPING #-}
+  ( OutputSpace a (x a -> f) ~ OutputSpace a f
+  , InputSpace a (x a -> f) ~ x :*: InputSpace a f
+  , FunctionSpace a f
+  ) => FunctionSpace a (x a -> f) where
+    uncurryF f (i :*: j) = uncurryF (f i) j
+    curryF k x = curryF (k . (:*:) x)

From 429cee874a470ad3a09468d78d19cf32ecc6d1d2 Mon Sep 17 00:00:00 2001
From: Eitan Chatav <eitan.chatav@gmail.com>
Date: Fri, 19 Jul 2024 13:29:58 -0700
Subject: [PATCH 47/51] symbolic class

---
 src/ZkFold/Symbolic/Base/Circuit.hs | 10 +++++-----
 src/ZkFold/Symbolic/Base/Num.hs     | 14 ++++++--------
 2 files changed, 11 insertions(+), 13 deletions(-)

diff --git a/src/ZkFold/Symbolic/Base/Circuit.hs b/src/ZkFold/Symbolic/Base/Circuit.hs
index 651b40cbc..be2162faa 100644
--- a/src/ZkFold/Symbolic/Base/Circuit.hs
+++ b/src/ZkFold/Symbolic/Base/Circuit.hs
@@ -332,12 +332,12 @@ invertC c = circuit $ do
 -- the Arithmetic field of a Symbolic field extension.
 newtype Register a = UnsafeRegister {fromRegister :: V.Vector a}
   deriving stock (Functor, Foldable, Traversable)
-instance Symbolic a => VectorSpace a Register where
+instance Symbolic x a => VectorSpace a Register where
   type Basis a Register = Int
   indexV (UnsafeRegister v) ix = fromMaybe zero (v V.!? ix)
-  dimV = numberOfBits @(Arithmetic a)
-  basisV = UnsafeRegister (V.generate (from (dimV @a @Register)) id)
-  tabulateV f = UnsafeRegister (V.generate (from (dimV @a @Register)) f)
+  dimV = numberOfBits @x
+  basisV = UnsafeRegister (V.generate (from (numberOfBits @x)) id)
+  tabulateV f = UnsafeRegister (V.generate (from (numberOfBits @x)) f)
 
 binaryExpansion
   :: forall x i. (PrimeField x, VectorSpace x i)
@@ -388,7 +388,7 @@ solderC cs = (fold (fmap (\c -> c {outputC = U1}) cs))
   { outputC = fmap (unPar1 . outputC) cs }
 
 desolderC
-  :: (Functor o)
+  :: Functor o
   => Circuit x i o
   -> o (Circuit x i Par1)
 desolderC c = fmap (\o -> c {outputC = Par1 o}) (outputC c)
diff --git a/src/ZkFold/Symbolic/Base/Num.hs b/src/ZkFold/Symbolic/Base/Num.hs
index 0c48f6221..03d9b03c3 100644
--- a/src/ZkFold/Symbolic/Base/Num.hs
+++ b/src/ZkFold/Symbolic/Base/Num.hs
@@ -13,7 +13,7 @@ module ZkFold.Symbolic.Base.Num
   , Int
   , Mod
     -- * Arithmetic constraints
-  , Symbolic (..)
+  , Symbolic
   , PrimeField
     -- * Algebraic constraints
   , AdditiveMonoid (..)
@@ -84,11 +84,10 @@ class
   , Comparable a
   , FiniteChr a
   , 3 <= Chr a
-  , PrimeField (Arithmetic a)
-  , Algebra (Arithmetic a) a
-  , Chr a ~ Order (Arithmetic a)
-  ) => Symbolic a where
-  type Arithmetic a
+  , PrimeField x
+  , Algebra x a
+  , Chr a ~ Order x
+  ) => Symbolic x a | x -> a where
 
 -- Prime fields should only include:
 -- (SemiIntegral int, Prime p) => PrimeField (int `Mod` p)
@@ -96,9 +95,8 @@ class
 -- p = 2 is ruled out to allow/require trichotomy.
 type PrimeField x =
   ( Modular x
-  , Arithmetic x ~ x
   , Finite x
-  , Symbolic x
+  , Symbolic x x
   )
 
 class AdditiveMonoid a where

From 5fe67979a7800e92460ac9e674ceb1d3ab0beb91 Mon Sep 17 00:00:00 2001
From: Eitan Chatav <eitan.chatav@gmail.com>
Date: Thu, 25 Jul 2024 09:36:14 -0700
Subject: [PATCH 48/51] evalMonoZ

---
 src/ZkFold/Symbolic/Base/Num.hs | 38 ++++++++++++++++++++++-----------
 1 file changed, 26 insertions(+), 12 deletions(-)

diff --git a/src/ZkFold/Symbolic/Base/Num.hs b/src/ZkFold/Symbolic/Base/Num.hs
index 03d9b03c3..e7367856b 100644
--- a/src/ZkFold/Symbolic/Base/Num.hs
+++ b/src/ZkFold/Symbolic/Base/Num.hs
@@ -55,6 +55,7 @@ module ZkFold.Symbolic.Base.Num
   , combineN
   , combineZ
   , evalMonoN
+  , evalMonoZ
   ) where
 
 import           Control.Applicative
@@ -87,7 +88,7 @@ class
   , PrimeField x
   , Algebra x a
   , Chr a ~ Order x
-  ) => Symbolic x a | x -> a where
+  ) => Symbolic x a | a -> x where
 
 -- Prime fields should only include:
 -- (SemiIntegral int, Prime p) => PrimeField (int `Mod` p)
@@ -364,14 +365,7 @@ instance Exponent Natural Rational where
   evalMono = evalMonoN
 instance Exponent Integer Rational where
   exponent = (Prelude.^^)
-  evalMono = evalMonoN . fmap absPow where
-    absPow (a,p) =
-      let
-        pZ = to @Integer p
-      in
-        if pZ >= 0
-        then (a, Prelude.fromIntegral pZ :: Natural)
-        else (one / a, Prelude.fromIntegral (negate pZ))
+  evalMono = evalMonoZ
 
 instance From Rational Rational
 instance From Natural Rational where from = Prelude.fromIntegral
@@ -606,9 +600,6 @@ instance (SemiIntegral int, Prime p)
 
 instance Into (Mod int n) (Mod int n)
 
-instance Into int (Mod int n) where
-  to = fromMod
-
 instance Into Rational int
   => Into Rational (Mod int n) where
     to = to . fromMod
@@ -666,6 +657,17 @@ instance (SemiIntegral int, KnownNat n)
 instance (SemiIntegral int, KnownNat n) => Discrete (Mod int n)
 instance (SemiIntegral int, KnownNat n) => Comparable (Mod int n)
 
+instance (KnownNat n, KnownNat (Log2 (n - 1) + 1))
+  => Finite (Mod int n) where
+    type Order (Mod int n) = n
+
+instance (SemiIntegral int, KnownNat n)
+  => FiniteChr (Mod int n) where
+    type Chr (Mod int n) = n
+
+instance (SemiIntegral int, Prime p, KnownNat (Log2 (p - 1) + 1), 3 <= p)
+  => Symbolic (Mod int p) (Mod int p)
+
 -- Scalar ------------------------------------------------------------------
 class (Semiring c, AdditiveMonoid a)
   => Scalar c a where
@@ -727,3 +729,15 @@ evalMonoN monomial = evalMonoNat naturalized where
       sqrtNots = product [a | (a,p) <- factors, odd p]
     in
       sqrts * sqrts * sqrtNots
+
+evalMonoZ
+  :: (Into Integer p, MultiplicativeGroup a)
+  => [(a,p)] -> a
+evalMonoZ = evalMonoN . fmap absPow where
+  absPow (a,p) =
+    let
+      pZ = to @Integer p
+    in
+      if pZ >= 0
+      then (a, Prelude.fromIntegral pZ :: Natural)
+      else (one / a, Prelude.fromIntegral (negate pZ))

From 0d09671e04b7c498a0ca6abba9d9bbd8e7da80e5 Mon Sep 17 00:00:00 2001
From: Eitan Chatav <eitan.chatav@gmail.com>
Date: Thu, 25 Jul 2024 09:36:21 -0700
Subject: [PATCH 49/51] Symbolic instance

---
 src/ZkFold/Symbolic/Base/Circuit.hs | 22 ++++++++++++++++++++++
 1 file changed, 22 insertions(+)

diff --git a/src/ZkFold/Symbolic/Base/Circuit.hs b/src/ZkFold/Symbolic/Base/Circuit.hs
index be2162faa..c3d794e09 100644
--- a/src/ZkFold/Symbolic/Base/Circuit.hs
+++ b/src/ZkFold/Symbolic/Base/Circuit.hs
@@ -295,6 +295,11 @@ instance (Ord x, VectorSpace x i)
     exponent x p = evalMono [(x, p)]
     evalMono = evalMonoN
 
+instance (Ord x, Discrete x, VectorSpace x i)
+  => Exponent Integer (Circuit x i Par1) where
+    exponent x p = evalMono [(x, p)]
+    evalMono = evalMonoZ
+
 instance (Ord x, Discrete x, VectorSpace x i)
   => MultiplicativeGroup (Circuit x i Par1) where
     recip c =
@@ -327,6 +332,23 @@ invertC c = circuit $ do
     (\x -> recip (x v))
   return (Par1 isZ :*: Par1 inv)
 
+instance (PrimeField x, VectorSpace x i)
+  => Comparable (Circuit x i Par1) where
+    trichotomy c0 c1 = circuit $ do
+      UnsafeRegister v0 <- runCircuit (binaryExpansion c0)
+      UnsafeRegister v1 <- runCircuit (binaryExpansion c1)
+      let reverseLexicographical a b = b * b * (b - a) + a
+      v <- newAssigned $ \x ->
+        V.foldl reverseLexicographical zero
+          (V.zipWith (\i0 i1 -> x i0 - x i1) v0 v1)
+      return (Par1 v)
+
+instance (Ord x, FiniteChr x, VectorSpace x i)
+  => FiniteChr (Circuit x i Par1) where
+    type Chr (Circuit x i Par1) = Chr x
+
+instance (PrimeField x, VectorSpace x i) => Symbolic x (Circuit x i Par1)
+
 -- A list of bits whose length is the number of bits
 -- needed to represent an element of
 -- the Arithmetic field of a Symbolic field extension.

From bc25271659c30c20d720f6994aa671fd5e944351 Mon Sep 17 00:00:00 2001
From: Eitan Chatav <eitan.chatav@gmail.com>
Date: Thu, 1 Aug 2024 08:17:55 -0700
Subject: [PATCH 50/51] Update Circuit.hs

---
 src/ZkFold/Symbolic/Base/Circuit.hs | 21 ++++++++++++++++-----
 1 file changed, 16 insertions(+), 5 deletions(-)

diff --git a/src/ZkFold/Symbolic/Base/Circuit.hs b/src/ZkFold/Symbolic/Base/Circuit.hs
index c3d794e09..486962aa6 100644
--- a/src/ZkFold/Symbolic/Base/Circuit.hs
+++ b/src/ZkFold/Symbolic/Base/Circuit.hs
@@ -22,6 +22,7 @@ module ZkFold.Symbolic.Base.Circuit
   , compileC
   , desolderC
   , solderC
+  , varNum
   ) where
 
 import Control.Applicative
@@ -67,6 +68,9 @@ data Circuit x i o = UnsafeCircuit
     -- they can be input, constant or new variables.
   }
 
+varNum :: Circuit x i o -> Int
+varNum c = maybe 0 Prelude.fst (IntMap.lookupMax (witnessC c))
+
 type Blueprint x i o =
   forall t m. (IxMonadCircuit x t, Monad m) => t i i m (o (Var x i))
 
@@ -111,11 +115,18 @@ indexW witnessMap inp = \case
 instance (Ord x, VectorSpace x i, o ~ U1) => Monoid (Circuit x i o) where
   mempty = UnsafeCircuit mempty mempty U1
 instance (Ord x, VectorSpace x i, o ~ U1) => Semigroup (Circuit x i o) where
-  c0 <> c1 = UnsafeCircuit
-    { systemC = systemC c0 <> systemC c1
-    , witnessC = witnessC c0 <> witnessC c1
-    , outputC = U1
-    }
+  c0 <> c1 =
+    let
+      varMax = maybe 0 Prelude.fst (IntMap.lookupMax (witnessC c0))
+      sysF = \case
+        InVar ix -> Right (InVar ix)
+        NewVar ix -> Right (NewVar (varMax + ix))
+    in
+      UnsafeCircuit
+        { systemC = systemC c0 <> Set.map (mapPoly sysF) (systemC c1)
+        , witnessC = witnessC c0 <> IntMap.mapKeys (varMax +) (witnessC c1)
+        , outputC = U1
+        }
 
 class Monad m => MonadCircuit x i m | m -> x, m -> i where
   runCircuit

From 7f610775db43db0ddffe3c6f88946486d37f6ba8 Mon Sep 17 00:00:00 2001
From: Eitan Chatav <eitan.chatav@gmail.com>
Date: Thu, 1 Aug 2024 08:41:15 -0700
Subject: [PATCH 51/51] Update Circuit.hs

---
 src/ZkFold/Symbolic/Base/Circuit.hs | 20 ++++++++++++--------
 1 file changed, 12 insertions(+), 8 deletions(-)

diff --git a/src/ZkFold/Symbolic/Base/Circuit.hs b/src/ZkFold/Symbolic/Base/Circuit.hs
index 486962aa6..9ed77c0f8 100644
--- a/src/ZkFold/Symbolic/Base/Circuit.hs
+++ b/src/ZkFold/Symbolic/Base/Circuit.hs
@@ -22,7 +22,7 @@ module ZkFold.Symbolic.Base.Circuit
   , compileC
   , desolderC
   , solderC
-  , varNum
+  , newVarsC
   ) where
 
 import Control.Applicative
@@ -68,8 +68,8 @@ data Circuit x i o = UnsafeCircuit
     -- they can be input, constant or new variables.
   }
 
-varNum :: Circuit x i o -> Int
-varNum c = maybe 0 Prelude.fst (IntMap.lookupMax (witnessC c))
+newVarsC :: Circuit x i o -> Int
+newVarsC c = maybe 0 Prelude.fst (IntMap.lookupMax (witnessC c))
 
 type Blueprint x i o =
   forall t m. (IxMonadCircuit x t, Monad m) => t i i m (o (Var x i))
@@ -117,7 +117,7 @@ instance (Ord x, VectorSpace x i, o ~ U1) => Monoid (Circuit x i o) where
 instance (Ord x, VectorSpace x i, o ~ U1) => Semigroup (Circuit x i o) where
   c0 <> c1 =
     let
-      varMax = maybe 0 Prelude.fst (IntMap.lookupMax (witnessC c0))
+      varMax = newVarsC c0
       sysF = \case
         InVar ix -> Right (InVar ix)
         NewVar ix -> Right (NewVar (varMax + ix))
@@ -130,7 +130,7 @@ instance (Ord x, VectorSpace x i, o ~ U1) => Semigroup (Circuit x i o) where
 
 class Monad m => MonadCircuit x i m | m -> x, m -> i where
   runCircuit
-    :: VectorSpace x i
+    :: (VectorSpace x i, Functor o)
     => Circuit x i o -> m (o (Var x i))
   input :: VectorSpace x i => m (i (Var x i))
   input = return (fmap (SysVar . InVar) (basisV @x))
@@ -177,8 +177,12 @@ instance (Field x, Ord x, Monad m)
 instance (Field x, Ord x, Monad m)
   => MonadCircuit x i (CircuitIx x i i m) where
 
-    runCircuit c = UnsafeCircuitIx $ \c' -> return
-      (outputC c, c {outputC = U1} <> c')
+    runCircuit c1 = UnsafeCircuitIx $ \c0 -> do
+      let
+        outF = \case
+          SysVar (NewVar ix) -> SysVar (NewVar (newVarsC c0 + ix))
+          v -> v
+      return (fmap outF (outputC c1), c0 <> c1 {outputC = U1})
 
     constraint p = UnsafeCircuitIx $ \c -> return
       ((), c {systemC = Set.insert (evalConst (p var)) (systemC c)})
@@ -350,7 +354,7 @@ instance (PrimeField x, VectorSpace x i)
       UnsafeRegister v1 <- runCircuit (binaryExpansion c1)
       let reverseLexicographical a b = b * b * (b - a) + a
       v <- newAssigned $ \x ->
-        V.foldl reverseLexicographical zero
+        V.foldl reverseLexicographical one
           (V.zipWith (\i0 i1 -> x i0 - x i1) v0 v1)
       return (Par1 v)