From 4294fac9cbfb5134406c77e2f2e69b871086ec80 Mon Sep 17 00:00:00 2001
From: Eitan Chatav <eitan.chatav@gmail.com>
Date: Tue, 10 Dec 2024 14:47:08 -0800
Subject: [PATCH 01/12] zkfold-base EC symbolic

Change the `Point` type and friends so that they may support Symbolic computation.
---
 .../src/ZkFold/Base/Algebra/Basic/Field.hs    |   4 +-
 .../Base/Algebra/EllipticCurve/BLS12_381.hs   |  54 +++--
 .../Base/Algebra/EllipticCurve/BN254.hs       |  22 +-
 .../Base/Algebra/EllipticCurve/Class.hs       | 202 ++++++++++++------
 .../Base/Algebra/EllipticCurve/Ed25519.hs     |  42 ++--
 .../Base/Algebra/EllipticCurve/Pairing.hs     | 108 ++++++----
 .../Base/Algebra/EllipticCurve/Pasta.hs       |  24 +--
 symbolic-base/src/ZkFold/Base/Protocol/KZG.hs |   1 +
 .../src/ZkFold/Base/Protocol/Plonk.hs         |   6 +-
 .../src/ZkFold/Base/Protocol/Plonk/Prover.hs  |   5 +-
 .../ZkFold/Base/Protocol/Plonk/Verifier.hs    |   6 +-
 .../src/ZkFold/Base/Protocol/Plonkup.hs       |   4 +-
 .../src/ZkFold/Base/Protocol/Plonkup/Proof.hs |   3 +-
 .../ZkFold/Base/Protocol/Plonkup/Prover.hs    |   5 +-
 .../Base/Protocol/Plonkup/Prover/Setup.hs     |   2 +
 .../src/ZkFold/Base/Protocol/Plonkup/Setup.hs |   3 +
 .../ZkFold/Base/Protocol/Plonkup/Verifier.hs  |   6 +-
 .../Protocol/Plonkup/Verifier/Commitments.hs  |   3 +-
 .../Base/Protocol/Plonkup/Verifier/Setup.hs   |   3 +
 .../ZkFold/Base/Protocol/Protostar/Commit.hs  |  10 +-
 .../ZkFold/Symbolic/Algorithms/ECDSA/ECDSA.hs |  10 +-
 .../src/ZkFold/Symbolic/Data/Bool.hs          |   3 -
 .../src/ZkFold/Symbolic/Data/Class.hs         |   4 +
 .../src/ZkFold/Symbolic/Data/Conditional.hs   |  61 +++++-
 .../src/ZkFold/Symbolic/Data/Ed25519.hs       |  82 ++-----
 symbolic-base/src/ZkFold/Symbolic/Data/Eq.hs  |  16 +-
 symbolic-base/src/ZkFold/Symbolic/Data/FFA.hs |   3 +
 .../src/ZkFold/Symbolic/Data/FieldElement.hs  |   3 +-
 .../src/ZkFold/Symbolic/Data/Maybe.hs         |  13 +-
 symbolic-base/src/ZkFold/Symbolic/Data/Ord.hs |  17 +-
 .../src/ZkFold/Symbolic/Data/UInt.hs          |   8 +-
 31 files changed, 433 insertions(+), 300 deletions(-)

diff --git a/symbolic-base/src/ZkFold/Base/Algebra/Basic/Field.hs b/symbolic-base/src/ZkFold/Base/Algebra/Basic/Field.hs
index 24fcb6109..a1a5a49f4 100644
--- a/symbolic-base/src/ZkFold/Base/Algebra/Basic/Field.hs
+++ b/symbolic-base/src/ZkFold/Base/Algebra/Basic/Field.hs
@@ -203,7 +203,7 @@ class IrreduciblePoly f (e :: Symbol) | e -> f where
     irreduciblePoly :: Poly f
 
 data Ext2 f (e :: Symbol) = Ext2 f f
-    deriving (Eq, Show)
+    deriving (Eq, Show, Generic)
 
 instance Ord f => Ord (Ext2 f e) where
     Ext2 a b <= Ext2 c d = [b, a] <= ([d, c] :: [f])
@@ -271,7 +271,7 @@ instance (Field f, Eq f, IrreduciblePoly f e, Arbitrary f) => Arbitrary (Ext2 f
     arbitrary = Ext2 <$> arbitrary <*> arbitrary
 
 data Ext3 f (e :: Symbol) = Ext3 f f f
-    deriving (Eq, Show)
+    deriving (Eq, Show, Generic)
 
 instance Ord f => Ord (Ext3 f e) where
     Ext3 a b c <= Ext3 d e f = [c, b, a] <= ([f, e, d] :: [f])
diff --git a/symbolic-base/src/ZkFold/Base/Algebra/EllipticCurve/BLS12_381.hs b/symbolic-base/src/ZkFold/Base/Algebra/EllipticCurve/BLS12_381.hs
index 7c95b98bc..13da9a879 100644
--- a/symbolic-base/src/ZkFold/Base/Algebra/EllipticCurve/BLS12_381.hs
+++ b/symbolic-base/src/ZkFold/Base/Algebra/EllipticCurve/BLS12_381.hs
@@ -67,9 +67,7 @@ instance EllipticCurve BLS12_381_G1 where
 
     type BaseField BLS12_381_G1 = Fq
 
-    inf = Inf
-
-    gen = Point
+    gen = point
         0x17f1d3a73197d7942695638c4fa9ac0fc3688c4f9774b905a14e3a3f171bac586c55e83ff97a1aeffb3af00adb22c6bb
         0x8b3f481e3aaa0f1a09e30ed741d8ae4fcf5e095d5d00af600db18cb2c04b3edd03cc744a2888ae40caa232946c5e7e1
 
@@ -93,9 +91,7 @@ instance EllipticCurve BLS12_381_G2 where
 
     type BaseField BLS12_381_G2 = Fq2
 
-    inf = Inf
-
-    gen = Point
+    gen = point
         (Ext2
             0x24aa2b2f08f0a91260805272dc51051c6e47ad4fa403b02b4510b647ae3d1770bac0326a805bbefd48056c8c121bdb8
             0x13e02b6052719f607dacd3a088274f65596bd0d09920b61ab5da61bbdc7f5049334cf11213945d57e5ac7d055d042b7e)
@@ -138,30 +134,31 @@ ofBytes
   . foldl' (\n w8 -> n * 256 + fromIntegral w8) 0
 
 instance Binary (Point BLS12_381_G1) where
-    put Inf         = foldMap putWord8 (bitReverse8 (bit 1) : replicate 95 0)
-    put (Point x y) = foldMap putWord8 (bytesOf 48 x <> bytesOf 48 y)
+    put (Point x y isInf) =
+        if isInf then foldMap putWord8 (bitReverse8 (bit 1) : replicate 95 0)
+                 else foldMap putWord8 (bytesOf 48 x <> bytesOf 48 y)
     get = do
         byte <- bitReverse8 <$> getWord8
         let compressed = testBit byte 0
             infinite = testBit byte 1
         if infinite then do
             skip (if compressed then 47 else 95)
-            return Inf
+            return inf
         else do
             let byteXhead = bitReverse8 $ clearBit (clearBit (clearBit byte 0) 1) 2
             bytesXtail <- replicateM 47 getWord8
             let x = ofBytes (byteXhead:bytesXtail)
                 bigY = testBit byte 2
-            if compressed then return (decompress (PointCompressed x bigY))
+            if compressed then return (decompress (pointCompressed x bigY))
             else do
                 bytesY <- replicateM 48 getWord8
                 let y = ofBytes bytesY
-                return (Point x y)
+                return (point x y)
 
 instance Binary (PointCompressed BLS12_381_G1) where
-    put InfCompressed            =
-        foldMap putWord8 (bitReverse8 (bit 0 .|. bit 1) : replicate 47 0)
-    put (PointCompressed x bigY) =
+    put (PointCompressed x bigY isInf) =
+        if isInf then foldMap putWord8 (bitReverse8 (bit 0 .|. bit 1) : replicate 47 0)
+        else
         let
             flags = bitReverse8 $ if bigY then bit 0 .|. bit 2 else bit 0
             bytes = bytesOf 48 x
@@ -172,23 +169,23 @@ instance Binary (PointCompressed BLS12_381_G1) where
             infinite = testBit byte 1
         if infinite then do
             skip (if compressed then 47 else 95)
-            return InfCompressed
+            return inf
         else do
             let byteXhead = bitReverse8 $ clearBit (clearBit (clearBit byte 0) 1) 2
             bytesXtail <- replicateM 47 getWord8
             let x = ofBytes (byteXhead:bytesXtail)
                 bigY = testBit byte 2
-            if compressed then return (PointCompressed x bigY)
+            if compressed then return (pointCompressed x bigY)
             else do
                 bytesY <- replicateM 48 getWord8
                 let y :: Fq = ofBytes bytesY
                     bigY' = y > negate y
-                return (PointCompressed x bigY')
+                return (pointCompressed x bigY')
 
 instance Binary (Point BLS12_381_G2) where
-    put Inf                               =
-        foldMap putWord8 (bitReverse8 (bit 1) : replicate 191  0)
-    put (Point (Ext2 x0 x1) (Ext2 y0 y1)) =
+    put (Point (Ext2 x0 x1) (Ext2 y0 y1) isInf) =
+        if isInf then foldMap putWord8 (bitReverse8 (bit 1) : replicate 191  0)
+        else
         let
             bytes = bytesOf 48 x1
               <> bytesOf 48 x0
@@ -202,7 +199,7 @@ instance Binary (Point BLS12_381_G2) where
             infinite = testBit byte 1
         if infinite then do
             skip (if compressed then 95 else 191)
-            return Inf
+            return inf
         else do
             let byteX1head = bitReverse8 $ clearBit (clearBit (clearBit byte 0) 1) 2
             bytesX1tail <- replicateM 47 getWord8
@@ -210,17 +207,18 @@ instance Binary (Point BLS12_381_G2) where
             let x1 = ofBytes (byteX1head:bytesX1tail)
                 x0 = ofBytes bytesX0
                 bigY = testBit byte 2
-            if compressed then return (decompress (PointCompressed (Ext2 x0 x1) bigY))
+            if compressed then return (decompress (pointCompressed (Ext2 x0 x1) bigY))
             else do
                 bytesY1 <- replicateM 48 getWord8
                 bytesY0 <- replicateM 48 getWord8
                 let y0 = ofBytes bytesY0
                     y1 = ofBytes bytesY1
-                return (Point (Ext2 x0 x1) (Ext2 y0 y1))
+                return (point (Ext2 x0 x1) (Ext2 y0 y1))
 
 instance Binary (PointCompressed BLS12_381_G2) where
-    put InfCompressed = foldMap putWord8 (bitReverse8 (bit 0 .|. bit 1) : replicate 95 0)
-    put (PointCompressed (Ext2 x0 x1) bigY) =
+    put (PointCompressed (Ext2 x0 x1) bigY isInf) =
+        if isInf then foldMap putWord8 (bitReverse8 (bit 0 .|. bit 1) : replicate 95 0)
+        else
         let
             flags = bitReverse8 $ if bigY then bit 0 .|. bit 2 else bit 0
             bytes = bytesOf 48 x1 <> bytesOf 48 x0
@@ -232,7 +230,7 @@ instance Binary (PointCompressed BLS12_381_G2) where
             infinite = testBit byte 1
         if infinite then do
             skip (if compressed then 95 else 191)
-            return InfCompressed
+            return inf
         else do
             let byteX1head = bitReverse8 $ clearBit (clearBit (clearBit byte 0) 1) 2
             bytesX1tail <- replicateM 47 getWord8
@@ -241,7 +239,7 @@ instance Binary (PointCompressed BLS12_381_G2) where
                 x0 = ofBytes bytesX0
                 x = Ext2 x0 x1
                 bigY = testBit byte 2
-            if compressed then return (PointCompressed (Ext2 x0 x1) bigY)
+            if compressed then return (pointCompressed (Ext2 x0 x1) bigY)
             else do
                 bytesY1 <- replicateM 48 getWord8
                 bytesY0 <- replicateM 48 getWord8
@@ -249,7 +247,7 @@ instance Binary (PointCompressed BLS12_381_G2) where
                     y1 = ofBytes bytesY1
                     y :: Fq2 = Ext2 y0 y1
                     bigY' = y > negate y
-                return (PointCompressed x bigY')
+                return (pointCompressed x bigY')
 
 --------------------------------------- Pairing ---------------------------------------
 
diff --git a/symbolic-base/src/ZkFold/Base/Algebra/EllipticCurve/BN254.hs b/symbolic-base/src/ZkFold/Base/Algebra/EllipticCurve/BN254.hs
index ac3699548..4af9b167d 100644
--- a/symbolic-base/src/ZkFold/Base/Algebra/EllipticCurve/BN254.hs
+++ b/symbolic-base/src/ZkFold/Base/Algebra/EllipticCurve/BN254.hs
@@ -70,8 +70,7 @@ data BN254_G1
 instance EllipticCurve BN254_G1 where
   type ScalarField BN254_G1 = Fr
   type BaseField BN254_G1 = Fp
-  inf = Inf
-  gen = Point 1 2
+  gen = point 1 2
   add = addPoints
   mul = pointMul
 
@@ -86,8 +85,7 @@ data BN254_G2
 instance EllipticCurve BN254_G2 where
   type ScalarField BN254_G2 = Fr
   type BaseField BN254_G2 = Fp2
-  inf = Inf
-  gen = Point
+  gen = point
     (Ext2 0x1800deef121f1e76426a00665e5c4479674322d4f75edadd46debd5cd992f6ed
           0x198e9393920d483a7260bfb731fb5d25f1aa493335a9e71297e485b7aef312c2)
     (Ext2 0x12c85ea5db8c6deb4aab71808dcb408fe3d1e7690c43d37b4ce6cc0166fa7daa
@@ -134,23 +132,23 @@ instance Pairing BN254_G1 BN254_G2 where
 ------------------------------ Encoding ----------------------------------------
 
 instance Binary (Point BN254_G1) where
-  put Inf           = put (Point @BN254_G1 zero zero)
-  put (Point xp yp) = put xp >> put yp
+  put (Point xp yp isInf) =
+    if isInf then put @(Point BN254_G1) (point zero zero) else put xp >> put yp
   get = do
     xp <- get
     yp <- get
     return $
       if xp == zero && yp == zero
-      then Inf
-      else Point xp yp
+      then inf
+      else point xp yp
 
 instance Binary (Point BN254_G2) where
-  put Inf           = put (Point @BN254_G2 zero zero)
-  put (Point xp yp) = put xp >> put yp
+  put (Point xp yp isInf) =
+    if isInf then put @(Point BN254_G2) (point zero zero) else put xp >> put yp
   get = do
     xp <- get
     yp <- get
     return $
       if xp == zero && yp == zero
-      then Inf
-      else Point xp yp
+      then inf
+      else point xp yp
diff --git a/symbolic-base/src/ZkFold/Base/Algebra/EllipticCurve/Class.hs b/symbolic-base/src/ZkFold/Base/Algebra/EllipticCurve/Class.hs
index de42cce31..ebc1207bb 100644
--- a/symbolic-base/src/ZkFold/Base/Algebra/EllipticCurve/Class.hs
+++ b/symbolic-base/src/ZkFold/Base/Algebra/EllipticCurve/Class.hs
@@ -1,32 +1,95 @@
 {-# LANGUAGE AllowAmbiguousTypes  #-}
 {-# LANGUAGE DeriveAnyClass       #-}
+{-# LANGUAGE DuplicateRecordFields #-}
+{-# LANGUAGE RebindableSyntax     #-}
 {-# LANGUAGE TypeOperators        #-}
 {-# LANGUAGE UndecidableInstances #-}
 
 module ZkFold.Base.Algebra.EllipticCurve.Class where
 
-import           Control.DeepSeq                  (NFData)
 import           Data.Functor                     ((<&>))
 import           Data.Kind                        (Type)
+import           Data.String                      (fromString)
 import           GHC.Generics                     (Generic)
-import           Prelude                          hiding (Num (..), sum, (/), (^))
+import           Prelude                          (fromInteger, Integer, Show (..), (++), (.), (<$>), type (~))
 import qualified Prelude                          as P
 import           Test.QuickCheck                  hiding (scale)
 
 import           ZkFold.Base.Algebra.Basic.Class
 import           ZkFold.Base.Algebra.Basic.Number
-
-data Point curve = Point { _x :: BaseField curve, _y :: BaseField curve } | Inf
-    deriving (Generic)
-
-deriving instance NFData (BaseField curve) => NFData (Point curve)
-
-class EllipticCurve curve where
+import           ZkFold.Symbolic.Class            (Symbolic)
+import           ZkFold.Symbolic.Data.Bool
+import           ZkFold.Symbolic.Data.Class
+import           ZkFold.Symbolic.Data.Conditional
+import           ZkFold.Symbolic.Data.Eq
+import           ZkFold.Symbolic.Data.Ord
+
+data Point (curve :: Type) = Point
+  { _x :: BaseField curve
+  , _y :: BaseField curve
+  , _isInf :: BooleanOf curve
+  } deriving (Generic)
+
+instance
+  ( EllipticCurve curve
+  , bool ~ BooleanOf curve
+  ) => Conditional bool (Point curve)
+
+instance
+  ( EllipticCurve curve
+  , bool ~ BooleanOf curve
+  ) => Eq bool (Point curve)
+
+instance
+  ( Symbolic ctx
+  , SymbolicOutput bool
+  , SymbolicOutput field
+  , bool ~ BooleanOf curve
+  , field ~ BaseField curve
+  , Context bool ~ ctx
+  , Context field ~ ctx
+  ) => SymbolicData (Point curve)
+
+class Planar field plane where
+  point :: field -> field -> plane
+
+instance
+  ( field ~ BaseField curve
+  , bool ~ BooleanOf curve
+  , BoolType bool
+  ) => Planar field (Point curve) where
+  point x y = Point x y false
+
+class ProjectivePlanar plane where
+  inf :: plane
+
+instance
+  ( field ~ BaseField curve
+  , BoolType (BooleanOf curve)
+  , AdditiveMonoid field
+  ) => ProjectivePlanar (Point curve) where
+  inf = Point zero zero true
+
+instance
+  ( field ~ BaseField curve
+  , BoolType (BooleanOf curve)
+  , AdditiveMonoid field
+  ) => ProjectivePlanar (PointCompressed curve) where
+  inf = PointCompressed zero false true
+
+class
+    ( BoolType (BooleanOf curve)
+    , AdditiveMonoid (BaseField curve)
+    , Conditional (BooleanOf curve) (BaseField curve)
+    , Conditional (BooleanOf curve) (BooleanOf curve)
+    , Eq (BooleanOf curve) (BaseField curve)
+    , Eq (BooleanOf curve) (BooleanOf curve)
+    ) => EllipticCurve curve where
 
     type BaseField curve :: Type
     type ScalarField curve :: Type
-
-    inf :: Point curve
+    type BooleanOf curve :: Type
+    type BooleanOf curve = P.Bool
 
     gen :: Point curve
 
@@ -34,22 +97,20 @@ class EllipticCurve curve where
 
     mul :: ScalarField curve -> Point curve -> Point curve
 
-instance (EllipticCurve curve, Show (BaseField curve)) => Show (Point curve) where
-    show Inf         = "Inf"
-    show (Point x y) = "(" ++ show x ++ ", " ++ show y ++ ")"
-
-instance (EllipticCurve curve, Eq (BaseField curve)) => Eq (Point curve) where
-    Inf         == Inf         = True
-    Inf         == _           = False
-    _           == Inf         = False
-    Point x1 y1 == Point x2 y2 = x1 == x2 && y1 == y2
+instance
+  ( EllipticCurve curve
+  , Show (BaseField curve)
+  , Conditional (BooleanOf curve) P.String
+  ) => Show (Point curve) where
+    show (Point x y isInf) = if isInf then "Inf" else "(" ++ show x ++ ", " ++ show y ++ ")"
 
 instance EllipticCurve curve => AdditiveSemigroup (Point curve) where
     (+) = add
 
 instance {-# OVERLAPPABLE #-}
     ( EllipticCurve curve
-    , Eq s
+    , BooleanOf curve ~ P.Bool
+    , P.Eq s
     , BinaryExpansion s
     , Bits s ~ [s]
     ) => Scale s (Point curve) where
@@ -59,7 +120,7 @@ instance EllipticCurve curve => Scale Natural (Point curve) where
     scale = natScale
 
 instance EllipticCurve curve => AdditiveMonoid (Point curve) where
-    zero = Inf
+    zero = inf
 
 instance (EllipticCurve curve, AdditiveGroup (BaseField curve)) => Scale Integer (Point curve) where
     scale = intScale
@@ -71,32 +132,32 @@ instance (EllipticCurve curve, Arbitrary (ScalarField curve)) => Arbitrary (Poin
     arbitrary = arbitrary <&> (`mul` gen)
 
 class (EllipticCurve curve1, EllipticCurve curve2, ScalarField curve1 ~ ScalarField curve2,
-        Eq (TargetGroup curve1 curve2), MultiplicativeGroup (TargetGroup curve1 curve2),
+        MultiplicativeGroup (TargetGroup curve1 curve2),
         Exponent (TargetGroup curve1 curve2) (ScalarField curve1)) => Pairing curve1 curve2 where
     type TargetGroup curve1 curve2 :: Type
     pairing :: Point curve1 -> Point curve2 -> TargetGroup curve1 curve2
 
 pointAdd
-    :: Field (BaseField curve)
-    => Eq (BaseField curve)
+    :: EllipticCurve curve
+    => Field (BaseField curve)
     => Point curve
     -> Point curve
     -> Point curve
-pointAdd p   Inf     = p
-pointAdd Inf q       = q
-pointAdd (Point x1 y1) (Point x2 y2)
-  | x1 == x2  = Inf
-  | otherwise = Point x3 y3
+pointAdd p@(Point x1 y1 isInf1) q@(Point x2 y2 isInf2) =
+  if isInf2 then p
+  else if isInf1 then q
+  else if x1 == x2 then inf
+  else point x3 y3
   where
     slope  = (y1 - y2) // (x1 - x2)
     x3 = slope * slope - x1 - x2
     y3 = slope * (x1 - x3) - y1
 
 pointDouble
-    :: Field (BaseField curve)
+    :: EllipticCurve curve
+    => Field (BaseField curve)
     => Point curve -> Point curve
-pointDouble Inf = Inf
-pointDouble (Point x y) = Point x' y'
+pointDouble (Point x y isInf) = if isInf then inf else point x' y'
   where
     slope = (x * x + x * x + x * x) // (y + y)
     x' = slope * slope - x - x
@@ -105,26 +166,23 @@ pointDouble (Point x y) = Point x' y'
 addPoints
     :: EllipticCurve curve
     => Field (BaseField curve)
-    => Eq (BaseField curve)
     => Point curve
     -> Point curve
     -> Point curve
-addPoints p1 p2
-    | p1 == p2  = pointDouble p1
-    | otherwise = pointAdd p1 p2
+addPoints p1 p2 = if p1 == p2 then pointDouble p1 else pointAdd p1 p2
 
 pointNegate
-    :: AdditiveGroup (BaseField curve)
+    :: EllipticCurve curve
+    => AdditiveGroup (BaseField curve)
     => Point curve -> Point curve
-pointNegate Inf         = Inf
-pointNegate (Point x y) = Point x (negate y)
+pointNegate (Point x y isInf) = if isInf then inf else point x (negate y)
 
 pointMul
     :: forall curve s
     .  EllipticCurve curve
     => BinaryExpansion (s)
     => Bits s ~ [s]
-    => Eq s
+    => P.Eq s
     => s
     -> Point curve
     -> Point curve
@@ -135,42 +193,66 @@ class EllipticCurve curve => StandardEllipticCurve curve where
     aParameter :: BaseField curve
     bParameter :: BaseField curve
 
-data PointCompressed curve = PointCompressed (BaseField curve) Bool | InfCompressed
-
-instance Show (BaseField curve) => Show (PointCompressed curve) where
-    show InfCompressed            = "InfCompressed"
-    show (PointCompressed x bigY) = "(" ++ show x ++ ", " ++ show bigY ++ ")"
-
-deriving instance Eq (BaseField curve) => Eq (PointCompressed curve)
-
-instance (Arbitrary (Point curve), AdditiveGroup (BaseField curve), Ord (BaseField curve)
-        ) => Arbitrary (PointCompressed curve) where
+data PointCompressed curve = PointCompressed
+  { _x :: BaseField curve
+  , _bigY :: BooleanOf curve
+  , _inf :: BooleanOf curve
+  } deriving Generic
+
+pointCompressed :: BoolType (BooleanOf curve) => BaseField curve -> BooleanOf curve -> PointCompressed curve
+pointCompressed x bigY = PointCompressed x bigY false
+
+instance
+  ( EllipticCurve curve
+  , bool ~ BooleanOf curve
+  ) => Conditional bool (PointCompressed curve)
+
+instance
+  ( EllipticCurve curve
+  , bool ~ BooleanOf curve
+  ) => Eq bool (PointCompressed curve)
+
+instance
+  ( Show (BaseField curve)
+  , Conditional (BooleanOf curve) P.String
+  , Show (BooleanOf curve)
+  ) => Show (PointCompressed curve) where
+    show (PointCompressed x bigY isInf) =
+      if isInf then "InfCompressed" else "(" ++ show x ++ ", " ++ show bigY ++ ")"
+
+instance
+  ( EllipticCurve curve
+  , AdditiveGroup (BaseField curve)
+  , Ord (BooleanOf curve) (BaseField curve)
+  , Arbitrary (ScalarField curve)
+  ) => Arbitrary (PointCompressed curve) where
     arbitrary = compress <$> arbitrary
 
 compress
   :: ( AdditiveGroup (BaseField curve)
-     , Ord (BaseField curve)
+     , EllipticCurve curve
+     , Ord (BooleanOf curve) (BaseField curve)
      )
   => Point curve -> PointCompressed curve
 compress = \case
-  Inf -> InfCompressed
-  Point x y -> PointCompressed x (y > negate y)
+  Point x y isInf -> if isInf then inf else PointCompressed x (y > negate y) false
 
 decompress
   :: forall curve .
      ( StandardEllipticCurve curve
      , FiniteField (BaseField curve)
-     , Ord (BaseField curve)
+     , Ord (BooleanOf curve) (BaseField curve)
      )
   => PointCompressed curve -> Point curve
-decompress = \case
-  InfCompressed -> Inf
-  PointCompressed x bigY ->
+decompress (PointCompressed x bigY isInf) =
+  if isInf then inf
+  else
     let a = aParameter @curve
         b = bParameter @curve
         p = order @(BaseField curve)
         sqrt_ z = z ^ ((p + 1) `P.div` 2)
         y' = sqrt_ (x * x * x + a * x + b)
-        y = (if bigY then maximum else minimum) [y', negate y']
+        y'' = negate y'
+        y = if bigY then max @(BooleanOf curve) y' y'' else min @(BooleanOf curve) y' y''
     in
-        Point x y
+        point x y
diff --git a/symbolic-base/src/ZkFold/Base/Algebra/EllipticCurve/Ed25519.hs b/symbolic-base/src/ZkFold/Base/Algebra/EllipticCurve/Ed25519.hs
index 61482c7fc..3c5a8abae 100644
--- a/symbolic-base/src/ZkFold/Base/Algebra/EllipticCurve/Ed25519.hs
+++ b/symbolic-base/src/ZkFold/Base/Algebra/EllipticCurve/Ed25519.hs
@@ -1,19 +1,19 @@
+{-# LANGUAGE RebindableSyntax     #-}
 {-# OPTIONS_GHC -Wno-orphans #-}
 
 module ZkFold.Base.Algebra.EllipticCurve.Ed25519  where
 
-import           Data.Void                               (Void)
-import           Prelude                                 (otherwise, ($), (==))
+import           Prelude                                 (($), fromInteger)
 
 import           ZkFold.Base.Algebra.Basic.Class
 import           ZkFold.Base.Algebra.Basic.Field
 import           ZkFold.Base.Algebra.Basic.Number
 import           ZkFold.Base.Algebra.EllipticCurve.Class
+import           ZkFold.Symbolic.Data.Conditional
+import           ZkFold.Symbolic.Data.Eq
 
 -- | The Ed25519 curve used in EdDSA signature scheme.
--- @c@ represents the "computational context" used to store and perform operations on curve points.
---
-data Ed25519 c
+data Ed25519
 
 -- | 2^252 + 27742317777372353535851937790883648493 is the order of the multiplicative group in Ed25519
 -- with the generator point defined below in @instance EllipticCurve (Ed25519 Void r)@
@@ -29,42 +29,36 @@ instance Prime Ed25519_Base
 -- | The purely mathematical implementation of Ed25519.
 -- It is available for use as-is and serves as "backend" for the @UInt 256 (Zp p)@ implementation as well.
 --
-instance EllipticCurve (Ed25519 Void) where
-    type BaseField (Ed25519 Void) = Zp Ed25519_Base
-    type ScalarField (Ed25519 Void) = Zp Ed25519_Scalar
-
-    inf = Inf
+instance EllipticCurve Ed25519 where
+    type BaseField Ed25519 = Zp Ed25519_Base
+    type ScalarField Ed25519 = Zp Ed25519_Scalar
 
-    gen = Point
+    gen = point
             (toZp @Ed25519_Base $ 15112221349535400772501151409588531511454012693041857206046113283949847762202)
             (toZp @Ed25519_Base $ 46316835694926478169428394003475163141307993866256225615783033603165251855960)
 
-    add p1 p2
-      | p1 == p2  = ed25519Double p1
-      | otherwise = ed25519Add p1 p2
+    add p1 p2 = if p1 == p2 then ed25519Double p1 else ed25519Add p1 p2
 
     mul = pointMul
 
 
-ed25519Add :: Point (Ed25519 Void) -> Point (Ed25519 Void) -> Point (Ed25519 Void)
-ed25519Add p Inf = p
-ed25519Add Inf q = q
-ed25519Add (Point x1 y1) (Point x2 y2) = Point x3 y3
+ed25519Add :: Point Ed25519 -> Point Ed25519 -> Point Ed25519
+ed25519Add p@(Point x1 y1 isInf1) q@(Point x2 y2 isInf2) =
+    if isInf2 then p else if isInf1 then q else point x3 y3
     where
-        d :: BaseField (Ed25519 Void)
+        d :: BaseField Ed25519
         d = negate $ toZp 121665 // toZp 121666
 
-        a :: BaseField (Ed25519 Void)
+        a :: BaseField Ed25519
         a = negate $ toZp 1
 
         x3 = (x1 * y2 + y1 * x2) // (toZp 1 + d * x1 * x2 * y1 * y2)
         y3 = (y1 * y2 - a * x1 * x2) // (toZp 1 - d * x1 * x2 * y1 * y2)
 
-ed25519Double :: Point (Ed25519 Void) -> Point (Ed25519 Void)
-ed25519Double Inf = Inf
-ed25519Double (Point x y) = Point x3 y3
+ed25519Double :: Point Ed25519 -> Point Ed25519
+ed25519Double (Point x y isInf) = if isInf then inf else point x3 y3
     where
-        a :: BaseField (Ed25519 Void)
+        a :: BaseField Ed25519
         a = negate $ toZp 1
 
         x3 = 2 * x * y // (a * x * x + y * y)
diff --git a/symbolic-base/src/ZkFold/Base/Algebra/EllipticCurve/Pairing.hs b/symbolic-base/src/ZkFold/Base/Algebra/EllipticCurve/Pairing.hs
index d149ec579..44e3d86a6 100644
--- a/symbolic-base/src/ZkFold/Base/Algebra/EllipticCurve/Pairing.hs
+++ b/symbolic-base/src/ZkFold/Base/Algebra/EllipticCurve/Pairing.hs
@@ -1,4 +1,5 @@
 {-# LANGUAGE AllowAmbiguousTypes #-}
+{-# LANGUAGE RebindableSyntax    #-}
 {-# LANGUAGE TypeOperators       #-}
 
 module ZkFold.Base.Algebra.EllipticCurve.Pairing
@@ -7,19 +8,23 @@ module ZkFold.Base.Algebra.EllipticCurve.Pairing
   , finalExponentiation
   ) where
 
-import           Data.Bool                               (otherwise)
-import           Data.Eq                                 (Eq (..))
+import qualified Data.Bool                               as H
+-- import           Data.Eq                                 (Eq (..))
 import           Data.Function                           (($), (.))
 import           Data.Functor                            ((<$>))
 import           Data.Int                                (Int8)
-import           Data.Ord                                ((>))
 import           Data.Tuple                              (snd)
 import           Data.Type.Equality                      (type (~))
 import           Numeric.Natural                         (Natural)
+import qualified Prelude
+import           Prelude                                 (fromInteger)
 
 import           ZkFold.Base.Algebra.Basic.Class
 import           ZkFold.Base.Algebra.Basic.Field
 import           ZkFold.Base.Algebra.EllipticCurve.Class
+import           ZkFold.Symbolic.Data.Bool               hiding (Bool)
+import           ZkFold.Symbolic.Data.Conditional
+import           ZkFold.Symbolic.Data.Eq
 
 -- Ate pairing implementation adapted from:
 -- https://github.com/sdiehl/pairing/blob/master/src/Data/Pairing/Ate.hs
@@ -37,30 +42,42 @@ finalExponentiation x = x ^ ((p ^ (12 :: Natural) -! 1) `div` r)
     r = order @(ScalarField c)
 
 millerAlgorithmBLS12 ::
-  (Field (BaseField c), Scale (BaseField c) (BaseField d)) =>
-  (Field (BaseField d), Eq (BaseField d)) =>
-  (EllipticCurve d, Untwisted d i j ~ g, Field g) =>
+  Field (BaseField c) =>
+  Field (BaseField d) =>
+  Scale (BaseField c) (BaseField d) =>
+  EllipticCurve d =>
+  Untwisted d i j ~ g =>
+  Field g =>
+  BooleanOf c ~ BooleanOf d =>
   [Int8] -> Point c -> Point d -> g
 millerAlgorithmBLS12 (x:xs) p q = snd $
-  millerLoop p q xs (if x > 0 then q else negate q, one)
+  millerLoop p q xs (H.bool (negate q) q (x Prelude.> 0), one)
 millerAlgorithmBLS12 _ _ _ = one
 
 millerAlgorithmBN ::
-  (PrimeField (BaseField c), Scale (BaseField c) (BaseField d)) =>
-  (Field (BaseField d), Eq (BaseField d)) =>
-  (EllipticCurve d, Untwisted d i j ~ g, Field g) =>
+  PrimeField (BaseField c) =>
+  Field (BaseField d) =>
+  Scale (BaseField c) (BaseField d) =>
+  EllipticCurve d =>
+  Untwisted d i j ~ g =>
+  Field g =>
+  BooleanOf c ~ BooleanOf d =>
   BaseField d -> [Int8] -> Point c -> Point d -> g
 millerAlgorithmBN xi (x:xs) p q = finalStepBN xi p q $
-  millerLoop p q xs (if x > 0 then q else negate q, one)
+  millerLoop p q xs (H.bool (negate q) q (x Prelude.> 0), one)
 millerAlgorithmBN _ _ _ _ = one
 
 --------------------------------------------------------------------------------
 
 finalStepBN ::
   forall c d i j g.
-  (PrimeField (BaseField c), Scale (BaseField c) (BaseField d)) =>
-  (Field (BaseField d), Eq (BaseField d)) =>
-  (EllipticCurve d, Untwisted d i j ~ g, Field g) =>
+  PrimeField (BaseField c) =>
+  Field (BaseField d) =>
+  Scale (BaseField c) (BaseField d) =>
+  EllipticCurve d =>
+  Untwisted d i j ~ g =>
+  Field g =>
+  BooleanOf c ~ BooleanOf d =>
   BaseField d -> Point c -> Point d -> (Point d, g) -> g
 finalStepBN xi p q (t, f) = f * f' * f''
   where
@@ -71,53 +88,67 @@ finalStepBN xi p q (t, f) = f * f' * f''
     (_, f'') = lineFunction p t' q2
 
 millerLoop ::
-  (Field (BaseField c), Scale (BaseField c) (BaseField d)) =>
-  (EllipticCurve d, Field (BaseField d), Eq (BaseField d)) =>
-  (Untwisted d i j ~ g, Field g) =>
+  Field (BaseField c) =>
+  Field (BaseField d) =>
+  Scale (BaseField c) (BaseField d) =>
+  EllipticCurve d =>
+  Untwisted d i j ~ g =>
+  Field g =>
+  BooleanOf c ~ BooleanOf d =>
   Point c -> Point d -> [Int8] -> (Point d, g) -> (Point d, g)
 millerLoop p q = impl
   where impl []     tf = tf
         impl (x:xs) tf
-          | x == 0    = impl xs tf2
-          | x == 1    = impl xs $ additionStep p q tf2
-          | otherwise = impl xs $ additionStep p (negate q) tf2
+          | x Prelude.== 0    = impl xs tf2
+          | x Prelude.== 1    = impl xs $ additionStep p q tf2
+          | H.otherwise = impl xs $ additionStep p (negate q) tf2
           where tf2 = doublingStep p tf
 
 --------------------------------------------------------------------------------
 
 frobTwisted ::
-  forall c. Field (BaseField c) => Natural -> BaseField c -> Point c -> Point c
-frobTwisted q xi (Point x y) = Point ((x ^ q) * (xi ^ tx)) ((y ^ q) * (xi ^ ty))
+  forall c. (EllipticCurve c, Field (BaseField c)) => Natural -> BaseField c -> Point c -> Point c
+frobTwisted q xi (Point x y isInf) =
+  if isInf then inf else point ((x ^ q) * (xi ^ tx)) ((y ^ q) * (xi ^ ty))
   where
     tx = (q -! 1) `div` 3
     ty = q `div` 2
-frobTwisted _ _ _ = Inf
 
 additionStep ::
-  (Field (BaseField c), Scale (BaseField c) (BaseField d)) =>
-  (Field (BaseField d), Eq (BaseField d)) =>
-  (Untwisted d i j ~ g, Field g) =>
+  Field (BaseField c) =>
+  Field (BaseField d) =>
+  Scale (BaseField c) (BaseField d) =>
+  EllipticCurve d =>
+  Untwisted d i j ~ g =>
+  Field g =>
+  BooleanOf c ~ BooleanOf d =>
   Point c -> Point d -> (Point d, g) -> (Point d, g)
 additionStep p q (t, f) = (* f) <$> lineFunction p q t
 
 doublingStep ::
-  (Field (BaseField c), Scale (BaseField c) (BaseField d)) =>
-  (Field (BaseField d), Eq (BaseField d)) =>
-  (Untwisted d i j ~ g, Field g) =>
+  Field (BaseField c) =>
+  Field (BaseField d) =>
+  Scale (BaseField c) (BaseField d) =>
+  EllipticCurve d =>
+  Untwisted d i j ~ g =>
+  Field g =>
+  BooleanOf c ~ BooleanOf d =>
   Point c -> (Point d, g) -> (Point d, g)
 doublingStep p (t, f) = (* f) . (* f) <$> lineFunction p t t
 
 lineFunction ::
-  (Field (BaseField c), Scale (BaseField c) (BaseField d)) =>
-  (Untwisted d i j ~ g, Field (BaseField d), Eq (BaseField d)) =>
+  EllipticCurve d =>
+  Field (BaseField c) =>
+  Field (BaseField d) =>
+  Scale (BaseField c) (BaseField d) =>
+  BooleanOf c ~ BooleanOf d =>
+  Untwisted d i j ~ g =>
   Point c -> Point d -> Point d -> (Point d, g)
-lineFunction (Point x y) (Point x1 y1) (Point x2 y2)
-  | x1 /= x2 =
-    (Point x3 y3, untwist (negate y) (x `scale` l) (y1 - l * x1))
-  | y1 + y2 == zero =
-    (Inf, untwist x (negate x1) zero)
-  | otherwise =
-    (Point x3' y3', untwist (negate y) (x `scale` l') (y1 - l' * x1))
+lineFunction (Point x y isInf) (Point x1 y1 isInf1) (Point x2 y2 isInf2) =
+  if isInf || isInf1 || isInf2 then (inf, Ext2 (Ext3 one zero zero) zero)
+  else if x1 /= x2 then (point x3 y3, untwist (negate y) (x `scale` l) (y1 - l * x1))
+  else if y1 + y2 == zero then (inf, untwist x (negate x1) zero)
+  else (point x3' y3', untwist (negate y) (x `scale` l') (y1 - l' * x1))
   where
     l   = (y2 - y1) // (x2 - x1)
     x3  = l * l - x1 - x2
@@ -127,4 +158,3 @@ lineFunction (Point x y) (Point x1 y1) (Point x2 y2)
     x3' = l' * l' - x1 - x2
     y3' = l' * (x1 - x3') - y1
     untwist a b c = Ext2 (Ext3 (a `scale` one) zero zero) (Ext3 b c zero)
-lineFunction _ _ _ = (Inf, Ext2 (Ext3 one zero zero) zero)
diff --git a/symbolic-base/src/ZkFold/Base/Algebra/EllipticCurve/Pasta.hs b/symbolic-base/src/ZkFold/Base/Algebra/EllipticCurve/Pasta.hs
index 98bf57db8..ab2f08eea 100644
--- a/symbolic-base/src/ZkFold/Base/Algebra/EllipticCurve/Pasta.hs
+++ b/symbolic-base/src/ZkFold/Base/Algebra/EllipticCurve/Pasta.hs
@@ -31,9 +31,7 @@ instance EllipticCurve Pallas where
 
     type BaseField Pallas = Fp
 
-    inf = Inf
-
-    gen = Point
+    gen = point
         0x40000000000000000000000000000000224698fc094cf91b992d30ed00000000
         0x02
 
@@ -56,9 +54,7 @@ instance EllipticCurve Vesta where
 
     type BaseField Vesta = Fq
 
-    inf = Inf
-
-    gen = Point
+    gen = point
         0x40000000000000000000000000000000224698fc0994a8dd8c46eb2100000000
         0x02
 
@@ -74,23 +70,23 @@ instance StandardEllipticCurve Vesta where
 ------------------------------------ Encoding ------------------------------------
 
 instance Binary (Point Pallas) where
-  put Inf           = put (Point @Pallas zero zero)
-  put (Point xp yp) = put xp >> put yp
+  put (Point xp yp isInf) =
+    if isInf then put @(Point Pallas) (point zero zero) else put xp >> put yp
   get = do
     xp <- get
     yp <- get
     return $
       if xp == zero && yp == zero
-      then Inf
-      else Point xp yp
+      then inf
+      else point xp yp
 
 instance Binary (Point Vesta) where
-  put Inf           = put (Point @Vesta zero zero)
-  put (Point xp yp) = put xp >> put yp
+  put (Point xp yp isInf) =
+    if isInf then put @(Point Vesta) (point zero zero) else put xp >> put yp
   get = do
     xp <- get
     yp <- get
     return $
       if xp == zero && yp == zero
-      then Inf
-      else Point xp yp
+      then inf
+      else point xp yp
diff --git a/symbolic-base/src/ZkFold/Base/Protocol/KZG.hs b/symbolic-base/src/ZkFold/Base/Protocol/KZG.hs
index 0bae1ade6..eeb1017e8 100644
--- a/symbolic-base/src/ZkFold/Base/Protocol/KZG.hs
+++ b/symbolic-base/src/ZkFold/Base/Protocol/KZG.hs
@@ -54,6 +54,7 @@ instance forall (c1 :: Type) (c2 :: Type) d kzg f g1 core.
     , Binary (Point c1)
     , Pairing c1 c2
     , CoreFunction c1 core
+    , Eq (TargetGroup c1 c2)
     ) => NonInteractiveProof (KZG c1 c2 d) core where
     type Transcript (KZG c1 c2 d)  = ByteString
     type SetupProve (KZG c1 c2 d)  = V.Vector (Point c1)
diff --git a/symbolic-base/src/ZkFold/Base/Protocol/Plonk.hs b/symbolic-base/src/ZkFold/Base/Protocol/Plonk.hs
index e68c0a799..2fd042fe2 100644
--- a/symbolic-base/src/ZkFold/Base/Protocol/Plonk.hs
+++ b/symbolic-base/src/ZkFold/Base/Protocol/Plonk.hs
@@ -17,7 +17,7 @@ import           Test.QuickCheck                                     (Arbitrary
 
 import           ZkFold.Base.Algebra.Basic.Class                     (AdditiveGroup)
 import           ZkFold.Base.Algebra.Basic.Number
-import           ZkFold.Base.Algebra.EllipticCurve.Class             (EllipticCurve (..), Pairing, PointCompressed)
+import           ZkFold.Base.Algebra.EllipticCurve.Class
 import           ZkFold.Base.Protocol.NonInteractiveProof
 import           ZkFold.Base.Protocol.Plonk.Prover                   (plonkProve)
 import           ZkFold.Base.Protocol.Plonk.Verifier                 (plonkVerify)
@@ -29,6 +29,7 @@ import           ZkFold.Base.Protocol.Plonkup.Verifier
 import           ZkFold.Base.Protocol.Plonkup.Witness
 import           ZkFold.Symbolic.Compiler                            (desugarRanges)
 import           ZkFold.Symbolic.Compiler.ArithmeticCircuit.Internal
+import qualified ZkFold.Symbolic.Data.Ord                            as Sym
 
 {-| Based on the paper https://eprint.iacr.org/2019/953.pdf -}
 
@@ -71,7 +72,7 @@ instance forall p i n l c1 c2 (ts :: Type) core .
         , Proof (Plonkup p i n l c1 c2 ts) ~ PlonkupProof c1
         , KnownNat n
         , Foldable l
-        , Ord (BaseField c1)
+        , Sym.Ord (BooleanOf c1) (BaseField c1)
         , AdditiveGroup (BaseField c1)
         , Pairing c1 c2
         , Arithmetic (ScalarField c1)
@@ -80,6 +81,7 @@ instance forall p i n l c1 c2 (ts :: Type) core .
         , ToTranscript ts (PointCompressed c1)
         , FromTranscript ts (ScalarField c1)
         , CoreFunction c1 core
+        , Eq (TargetGroup c1 c2)
         ) => NonInteractiveProof (Plonk p i n l c1 c2 ts) core where
     type Transcript (Plonk p i n l c1 c2 ts)  = ts
     type SetupProve (Plonk p i n l c1 c2 ts)  = PlonkupProverSetup p i n l c1 c2
diff --git a/symbolic-base/src/ZkFold/Base/Protocol/Plonk/Prover.hs b/symbolic-base/src/ZkFold/Base/Protocol/Plonk/Prover.hs
index 12841bc7e..b2b47202a 100644
--- a/symbolic-base/src/ZkFold/Base/Protocol/Plonk/Prover.hs
+++ b/symbolic-base/src/ZkFold/Base/Protocol/Plonk/Prover.hs
@@ -9,7 +9,7 @@ import qualified Data.Vector                                         as V
 import           Data.Word                                           (Word8)
 import           GHC.IsList                                          (IsList (..))
 import           Prelude                                             hiding (Num (..), drop, length, pi, sum, take,
-                                                                      (!!), (/), (^))
+                                                                      (!!), (/), (^), Ord)
 
 import           ZkFold.Base.Algebra.Basic.Class
 import           ZkFold.Base.Algebra.Basic.Number                    (KnownNat, Natural, value)
@@ -29,11 +29,12 @@ import           ZkFold.Base.Protocol.Plonkup.Testing                (PlonkupPro
 import           ZkFold.Base.Protocol.Plonkup.Utils                  (sortByList)
 import           ZkFold.Base.Protocol.Plonkup.Witness
 import           ZkFold.Symbolic.Compiler.ArithmeticCircuit.Internal
+import           ZkFold.Symbolic.Data.Ord
 
 plonkProve :: forall p i n l c1 c2 ts core .
     ( KnownNat n
     , Foldable l
-    , Ord (BaseField c1)
+    , Ord (BooleanOf c1) (BaseField c1)
     , AdditiveGroup (BaseField c1)
     , Arithmetic (ScalarField c1)
     , ToTranscript ts Word8
diff --git a/symbolic-base/src/ZkFold/Base/Protocol/Plonk/Verifier.hs b/symbolic-base/src/ZkFold/Base/Protocol/Plonk/Verifier.hs
index e70aed795..d322e13ab 100644
--- a/symbolic-base/src/ZkFold/Base/Protocol/Plonk/Verifier.hs
+++ b/symbolic-base/src/ZkFold/Base/Protocol/Plonk/Verifier.hs
@@ -8,7 +8,7 @@ module ZkFold.Base.Protocol.Plonk.Verifier
 import           Data.Word                                           (Word8)
 import           GHC.IsList                                          (IsList (..))
 import           Prelude                                             hiding (Num (..), drop, length, sum, take, (!!),
-                                                                      (/), (^))
+                                                                      (/), (^), Ord)
 
 import           ZkFold.Base.Algebra.Basic.Class
 import           ZkFold.Base.Algebra.Basic.Number                    (KnownNat, Natural, value)
@@ -21,18 +21,20 @@ import           ZkFold.Base.Protocol.Plonkup.Proof
 import           ZkFold.Base.Protocol.Plonkup.Verifier.Commitments
 import           ZkFold.Base.Protocol.Plonkup.Verifier.Setup
 import           ZkFold.Symbolic.Compiler.ArithmeticCircuit.Internal
+import           ZkFold.Symbolic.Data.Ord
 
 plonkVerify :: forall p i n l c1 c2 ts .
     ( KnownNat n
     , Foldable l
     , Pairing c1 c2
-    , Ord (BaseField c1)
+    , Ord (BooleanOf c1) (BaseField c1)
     , AdditiveGroup (BaseField c1)
     , Arithmetic (ScalarField c1)
     , ToTranscript ts Word8
     , ToTranscript ts (ScalarField c1)
     , ToTranscript ts (PointCompressed c1)
     , FromTranscript ts (ScalarField c1)
+    , Eq (TargetGroup c1 c2)
     ) => PlonkupVerifierSetup p i n l c1 c2 -> PlonkupInput l c1 -> PlonkupProof c1 -> Bool
 plonkVerify
     PlonkupVerifierSetup {..}
diff --git a/symbolic-base/src/ZkFold/Base/Protocol/Plonkup.hs b/symbolic-base/src/ZkFold/Base/Protocol/Plonkup.hs
index 3f5ad1f90..700ca1525 100644
--- a/symbolic-base/src/ZkFold/Base/Protocol/Plonkup.hs
+++ b/symbolic-base/src/ZkFold/Base/Protocol/Plonkup.hs
@@ -25,6 +25,7 @@ import           ZkFold.Base.Protocol.Plonkup.Setup
 import           ZkFold.Base.Protocol.Plonkup.Verifier
 import           ZkFold.Base.Protocol.Plonkup.Witness
 import           ZkFold.Symbolic.Compiler.ArithmeticCircuit.Internal
+import qualified ZkFold.Symbolic.Data.Ord                            as Sym
 
 {-| Based on the paper https://eprint.iacr.org/2022/086.pdf -}
 
@@ -35,7 +36,7 @@ instance forall p i n l c1 c2 ts core.
         , Representable l
         , Foldable l
         , Ord (Rep i)
-        , Ord (BaseField c1)
+        , Sym.Ord (BooleanOf c1) (BaseField c1)
         , AdditiveGroup (BaseField c1)
         , Pairing c1 c2
         , Arithmetic (ScalarField c1)
@@ -44,6 +45,7 @@ instance forall p i n l c1 c2 ts core.
         , ToTranscript ts (PointCompressed c1)
         , FromTranscript ts (ScalarField c1)
         , CoreFunction c1 core
+        , Eq (TargetGroup c1 c2)
         ) => NonInteractiveProof (Plonkup p i n l c1 c2 ts) core where
     type Transcript (Plonkup p i n l c1 c2 ts)  = ts
     type SetupProve (Plonkup p i n l c1 c2 ts)  = PlonkupProverSetup p i n l c1 c2
diff --git a/symbolic-base/src/ZkFold/Base/Protocol/Plonkup/Proof.hs b/symbolic-base/src/ZkFold/Base/Protocol/Plonkup/Proof.hs
index 0e6a628b2..14fe3bf14 100644
--- a/symbolic-base/src/ZkFold/Base/Protocol/Plonkup/Proof.hs
+++ b/symbolic-base/src/ZkFold/Base/Protocol/Plonkup/Proof.hs
@@ -1,3 +1,4 @@
+{-# LANGUAGE TypeOperators #-}
 {-# LANGUAGE UndecidableInstances #-}
 
 module ZkFold.Base.Protocol.Plonkup.Proof where
@@ -35,7 +36,7 @@ data PlonkupProof c = PlonkupProof {
         l1_xi   :: ScalarField c
         -- ^ The denominator in the L_1 polynomial evaluation
     }
-instance (Show (ScalarField c), Show (BaseField c), EllipticCurve c) => Show (PlonkupProof c) where
+instance (Show (ScalarField c), Show (BaseField c), EllipticCurve c, BooleanOf c ~ Bool) => Show (PlonkupProof c) where
     show PlonkupProof {..} =
         "Plonkup Proof: "
         ++ show cmA ++ " "
diff --git a/symbolic-base/src/ZkFold/Base/Protocol/Plonkup/Prover.hs b/symbolic-base/src/ZkFold/Base/Protocol/Plonkup/Prover.hs
index dd3d74765..936146ee1 100644
--- a/symbolic-base/src/ZkFold/Base/Protocol/Plonkup/Prover.hs
+++ b/symbolic-base/src/ZkFold/Base/Protocol/Plonkup/Prover.hs
@@ -12,7 +12,7 @@ import qualified Data.Vector                                         as V
 import           Data.Word                                           (Word8)
 import           GHC.IsList                                          (IsList (..))
 import           Prelude                                             hiding (Num (..), drop, length, pi, sum, take,
-                                                                      (!!), (/), (^))
+                                                                      (!!), (/), (^), Ord (..))
 
 import           ZkFold.Base.Algebra.Basic.Class
 import           ZkFold.Base.Algebra.Basic.Number                    (KnownNat, Natural, value)
@@ -31,12 +31,13 @@ import           ZkFold.Base.Protocol.Plonkup.Testing                (PlonkupPro
 import           ZkFold.Base.Protocol.Plonkup.Utils                  (sortByList)
 import           ZkFold.Base.Protocol.Plonkup.Witness
 import           ZkFold.Symbolic.Compiler.ArithmeticCircuit.Internal
+import           ZkFold.Symbolic.Data.Ord
 
 plonkupProve :: forall p i n l c1 c2 ts core .
     ( KnownNat n
     , KnownNat (PlonkupPolyExtendedLength n)
     , Foldable l
-    , Ord (BaseField c1)
+    , Ord (BooleanOf c1) (BaseField c1)
     , AdditiveGroup (BaseField c1)
     , Arithmetic (ScalarField c1)
     , ToTranscript ts Word8
diff --git a/symbolic-base/src/ZkFold/Base/Protocol/Plonkup/Prover/Setup.hs b/symbolic-base/src/ZkFold/Base/Protocol/Plonkup/Prover/Setup.hs
index 987963c09..516a59592 100644
--- a/symbolic-base/src/ZkFold/Base/Protocol/Plonkup/Prover/Setup.hs
+++ b/symbolic-base/src/ZkFold/Base/Protocol/Plonkup/Prover/Setup.hs
@@ -1,3 +1,4 @@
+{-# LANGUAGE TypeOperators #-}
 {-# LANGUAGE UndecidableInstances #-}
 
 module ZkFold.Base.Protocol.Plonkup.Prover.Setup where
@@ -30,6 +31,7 @@ instance
         , Show (BaseField c2)
         , Show (ScalarField c1)
         , Show (PlonkupRelation p i n l (ScalarField c1))
+        , BooleanOf c1 ~ Bool
         ) => Show (PlonkupProverSetup p i n l c1 c2) where
     show PlonkupProverSetup {..} =
         "Prover setup: "
diff --git a/symbolic-base/src/ZkFold/Base/Protocol/Plonkup/Setup.hs b/symbolic-base/src/ZkFold/Base/Protocol/Plonkup/Setup.hs
index e2436c66c..b6e128e7e 100644
--- a/symbolic-base/src/ZkFold/Base/Protocol/Plonkup/Setup.hs
+++ b/symbolic-base/src/ZkFold/Base/Protocol/Plonkup/Setup.hs
@@ -1,4 +1,5 @@
 {-# LANGUAGE AllowAmbiguousTypes  #-}
+{-# LANGUAGE TypeOperators #-}
 {-# LANGUAGE UndecidableInstances #-}
 
 module ZkFold.Base.Protocol.Plonkup.Setup where
@@ -44,6 +45,8 @@ instance
         , Show (BaseField c2)
         , Show (ScalarField c1)
         , Show (PlonkupRelation p i n l (ScalarField c1))
+        , BooleanOf c1 ~ Bool
+        , BooleanOf c2 ~ Bool
         ) => Show (PlonkupSetup p i n l c1 c2) where
     show PlonkupSetup {..} =
         "Setup: "
diff --git a/symbolic-base/src/ZkFold/Base/Protocol/Plonkup/Verifier.hs b/symbolic-base/src/ZkFold/Base/Protocol/Plonkup/Verifier.hs
index d637b8f27..9380534fa 100644
--- a/symbolic-base/src/ZkFold/Base/Protocol/Plonkup/Verifier.hs
+++ b/symbolic-base/src/ZkFold/Base/Protocol/Plonkup/Verifier.hs
@@ -10,7 +10,7 @@ module ZkFold.Base.Protocol.Plonkup.Verifier
 import           Data.Word                                           (Word8)
 import           GHC.IsList                                          (IsList (..))
 import           Prelude                                             hiding (Num (..), drop, length, sum, take, (!!),
-                                                                      (/), (^))
+                                                                      (/), (^), Ord (..))
 
 import           ZkFold.Base.Algebra.Basic.Class
 import           ZkFold.Base.Algebra.Basic.Number                    (KnownNat, Natural, value)
@@ -23,19 +23,21 @@ import           ZkFold.Base.Protocol.Plonkup.Proof
 import           ZkFold.Base.Protocol.Plonkup.Verifier.Commitments
 import           ZkFold.Base.Protocol.Plonkup.Verifier.Setup
 import           ZkFold.Symbolic.Compiler.ArithmeticCircuit.Internal
+import           ZkFold.Symbolic.Data.Ord
 
 plonkupVerify :: forall p i n l c1 c2 ts .
     ( KnownNat n
     , KnownNat (PlonkupPolyExtendedLength n)
     , Foldable l
     , Pairing c1 c2
-    , Ord (BaseField c1)
+    , Ord (BooleanOf c1) (BaseField c1)
     , AdditiveGroup (BaseField c1)
     , Arithmetic (ScalarField c1)
     , ToTranscript ts Word8
     , ToTranscript ts (ScalarField c1)
     , ToTranscript ts (PointCompressed c1)
     , FromTranscript ts (ScalarField c1)
+    , Eq (TargetGroup c1 c2)
     ) => PlonkupVerifierSetup p i n l c1 c2 -> PlonkupInput l c1 -> PlonkupProof c1 -> Bool
 plonkupVerify
     PlonkupVerifierSetup {..}
diff --git a/symbolic-base/src/ZkFold/Base/Protocol/Plonkup/Verifier/Commitments.hs b/symbolic-base/src/ZkFold/Base/Protocol/Plonkup/Verifier/Commitments.hs
index 5fbc11f88..d82186d32 100644
--- a/symbolic-base/src/ZkFold/Base/Protocol/Plonkup/Verifier/Commitments.hs
+++ b/symbolic-base/src/ZkFold/Base/Protocol/Plonkup/Verifier/Commitments.hs
@@ -1,3 +1,4 @@
+{-# LANGUAGE TypeOperators #-}
 {-# LANGUAGE UndecidableInstances #-}
 
 module ZkFold.Base.Protocol.Plonkup.Verifier.Commitments where
@@ -18,7 +19,7 @@ data PlonkupCircuitCommitments c = PlonkupCircuitCommitments {
         cmS3 :: Point c,
         cmT1 :: Point c
     }
-instance (Show (BaseField c), EllipticCurve c) => Show (PlonkupCircuitCommitments c) where
+instance (Show (BaseField c), EllipticCurve c, BooleanOf c ~ Bool) => Show (PlonkupCircuitCommitments c) where
     show PlonkupCircuitCommitments {..} =
         "Plonkup Circuit Commitments: "
         ++ show cmQl ++ " "
diff --git a/symbolic-base/src/ZkFold/Base/Protocol/Plonkup/Verifier/Setup.hs b/symbolic-base/src/ZkFold/Base/Protocol/Plonkup/Verifier/Setup.hs
index 66ffcca15..f75b4f4bf 100644
--- a/symbolic-base/src/ZkFold/Base/Protocol/Plonkup/Verifier/Setup.hs
+++ b/symbolic-base/src/ZkFold/Base/Protocol/Plonkup/Verifier/Setup.hs
@@ -1,3 +1,4 @@
+{-# LANGUAGE TypeOperators #-}
 {-# LANGUAGE UndecidableInstances #-}
 
 module ZkFold.Base.Protocol.Plonkup.Verifier.Setup where
@@ -29,6 +30,8 @@ instance
         , Show (BaseField c2)
         , Show (ScalarField c1)
         , Show (PlonkupRelation p i n l (ScalarField c1))
+        , BooleanOf c1 ~ Bool
+        , BooleanOf c2 ~ Bool
         ) => Show (PlonkupVerifierSetup p i n l c1 c2) where
     show PlonkupVerifierSetup {..} =
         "Verifier setup: "
diff --git a/symbolic-base/src/ZkFold/Base/Protocol/Protostar/Commit.hs b/symbolic-base/src/ZkFold/Base/Protocol/Protostar/Commit.hs
index a50136bca..33ea962ec 100644
--- a/symbolic-base/src/ZkFold/Base/Protocol/Protostar/Commit.hs
+++ b/symbolic-base/src/ZkFold/Base/Protocol/Protostar/Commit.hs
@@ -2,8 +2,6 @@
 
 module ZkFold.Base.Protocol.Protostar.Commit (Commit (..), HomomorphicCommit (..), PedersonSetup (..)) where
 
-import           Control.DeepSeq                             (NFData)
-import           Data.Void                                   (Void)
 import           Data.Zip                                    (zipWith)
 import           GHC.IsList                                  (IsList (..))
 import           Prelude                                     hiding (Num (..), sum, take, zipWith)
@@ -18,9 +16,6 @@ import           ZkFold.Base.Algebra.EllipticCurve.Ed25519
 import           ZkFold.Base.Data.Vector                     (Vector)
 import           ZkFold.Base.Protocol.Protostar.Oracle
 import           ZkFold.Prelude                              (take)
-import           ZkFold.Symbolic.Class                       (Symbolic)
-import           ZkFold.Symbolic.Data.Ed25519                ()
-import           ZkFold.Symbolic.Data.FFA                    (Size)
 
 -- | Commit to the object @a@ with commitment key @ck@ and results of type @f@
 --
@@ -44,11 +39,10 @@ instance KnownNat n => PedersonSetup n (Point BLS12_381_G1) where
         let x = fst $ random $ mkStdGen 0 :: Zp BLS12_381_Scalar
         in fromList $ take (value @n) $ iterate (scale x) gen
 
-instance (KnownNat n, Symbolic c, NFData (c (Vector Size)))
-        => PedersonSetup n (Point (Ed25519 c)) where
+instance KnownNat n => PedersonSetup n (Point Ed25519) where
     groupElements =
         -- TODO: This is just for testing purposes! Not to be used in production
-        let x = fst $ random $ mkStdGen 0 :: ScalarField (Ed25519 Void)
+        let x = fst $ random $ mkStdGen 0 :: ScalarField Ed25519
         in fromList $ take (value @n) $ iterate (scale x) gen
 
 instance (PedersonSetup n c, Scale f c, AdditiveGroup c) => HomomorphicCommit (Vector n f) c where
diff --git a/symbolic-base/src/ZkFold/Symbolic/Algorithms/ECDSA/ECDSA.hs b/symbolic-base/src/ZkFold/Symbolic/Algorithms/ECDSA/ECDSA.hs
index 7fc47604a..202977063 100644
--- a/symbolic-base/src/ZkFold/Symbolic/Algorithms/ECDSA/ECDSA.hs
+++ b/symbolic-base/src/ZkFold/Symbolic/Algorithms/ECDSA/ECDSA.hs
@@ -1,4 +1,5 @@
 {-# LANGUAGE AllowAmbiguousTypes #-}
+{-# LANGUAGE RebindableSyntax #-}
 {-# LANGUAGE TypeOperators       #-}
 module ZkFold.Symbolic.Algorithms.ECDSA.ECDSA where
 import           Data.Type.Equality
@@ -8,11 +9,12 @@ import qualified GHC.TypeNats
 
 import           ZkFold.Base.Algebra.Basic.Class
 import           ZkFold.Base.Algebra.Basic.Number        (value)
-import           ZkFold.Base.Algebra.EllipticCurve.Class (EllipticCurve (BaseField, gen), Point (Inf, Point))
+import           ZkFold.Base.Algebra.EllipticCurve.Class
 import qualified ZkFold.Symbolic.Class                   as S
 import           ZkFold.Symbolic.Data.Bool
 import           ZkFold.Symbolic.Data.ByteString         (ByteString)
 import           ZkFold.Symbolic.Data.Combinators        (Iso (..), NumberOfRegisters, RegisterSize (Auto))
+import           ZkFold.Symbolic.Data.Conditional
 import           ZkFold.Symbolic.Data.Eq
 import           ZkFold.Symbolic.Data.FieldElement       (FieldElement)
 import           ZkFold.Symbolic.Data.UInt               (UInt, eea)
@@ -26,14 +28,14 @@ ecdsaVerify :: forall curve n c . (
     , Log2 (Order (S.BaseField c) GHC.TypeNats.- 1) ~ 255
     , SemiEuclidean (UInt 256 'Auto c)
     , KnownNat (NumberOfRegisters (S.BaseField c) 256 'Auto)
+    , BooleanOf curve ~ Bool c
     )
     => Point curve
     -> ByteString 256 c
     -> (UInt 256 'Auto c, UInt 256 'Auto c)
     -> Bool c
-ecdsaVerify publicKey message (r, s) = case c of
-                Inf       -> false
-                Point x _ -> r == (x `mod` n)
+ecdsaVerify publicKey message (r, s) =
+    case c of Point x _ isInf  -> if isInf then false else r == (x `mod` n)
     where
         n = fromConstant $ value @n
 
diff --git a/symbolic-base/src/ZkFold/Symbolic/Data/Bool.hs b/symbolic-base/src/ZkFold/Symbolic/Data/Bool.hs
index f3e7f3c03..d1199037f 100644
--- a/symbolic-base/src/ZkFold/Symbolic/Data/Bool.hs
+++ b/symbolic-base/src/ZkFold/Symbolic/Data/Bool.hs
@@ -22,7 +22,6 @@ import           Text.Show                       (Show)
 
 import           ZkFold.Base.Algebra.Basic.Class
 import           ZkFold.Symbolic.Class
-import           ZkFold.Symbolic.Data.Class      (SymbolicData)
 import           ZkFold.Symbolic.Interpreter     (Interpreter (..))
 import           ZkFold.Symbolic.MonadCircuit    (newAssigned)
 
@@ -65,8 +64,6 @@ deriving instance Show (c Par1) => Show (Bool c)
 instance {-# OVERLAPPING #-} (Eq a, MultiplicativeMonoid a) => Show (Bool (Interpreter a)) where
     show (fromBool -> x) = if x == one then "True" else "False"
 
-deriving newtype instance Symbolic c => SymbolicData (Bool c)
-
 instance Symbolic c => BoolType (Bool c) where
     true = Bool $ embed (Par1 one)
 
diff --git a/symbolic-base/src/ZkFold/Symbolic/Data/Class.hs b/symbolic-base/src/ZkFold/Symbolic/Data/Class.hs
index c1ee1f572..6d7bc2151 100644
--- a/symbolic-base/src/ZkFold/Symbolic/Data/Class.hs
+++ b/symbolic-base/src/ZkFold/Symbolic/Data/Class.hs
@@ -1,3 +1,4 @@
+{-# LANGUAGE DerivingStrategies   #-}
 {-# LANGUAGE TypeOperators        #-}
 {-# LANGUAGE UndecidableInstances #-}
 
@@ -27,6 +28,7 @@ import           ZkFold.Base.Data.Package         (Package, pack)
 import           ZkFold.Base.Data.Product         (fstP, sndP)
 import           ZkFold.Base.Data.Vector          (Vector)
 import           ZkFold.Symbolic.Class            (Symbolic (WitnessField))
+import           ZkFold.Symbolic.Data.Bool        (Bool (Bool))
 
 -- | A class for Symbolic data types.
 class
@@ -101,6 +103,8 @@ instance
     payload _ _ = U1
     restore f = fst (f Proxy)
 
+deriving newtype instance Symbolic c => SymbolicData (Bool c)
+
 instance Symbolic c => SymbolicData (Proxy (c :: (Type -> Type) -> Type)) where
     type Context (Proxy c) = c
     type Support (Proxy c) = Proxy c
diff --git a/symbolic-base/src/ZkFold/Symbolic/Data/Conditional.hs b/symbolic-base/src/ZkFold/Symbolic/Data/Conditional.hs
index 2f66c5ad6..e588dab40 100644
--- a/symbolic-base/src/ZkFold/Symbolic/Data/Conditional.hs
+++ b/symbolic-base/src/ZkFold/Symbolic/Data/Conditional.hs
@@ -1,15 +1,18 @@
+{-# LANGUAGE DerivingStrategies   #-}
 {-# LANGUAGE TypeOperators        #-}
 {-# LANGUAGE UndecidableInstances #-}
 
 module ZkFold.Symbolic.Data.Conditional where
 
 import           Control.Monad.Representable.Reader (Representable, mzipWithRep)
+import qualified Data.Bool                          as H
 import           Data.Function                      (($))
 import           Data.Traversable                   (Traversable)
-import           Data.Type.Equality                 (type (~))
-import           GHC.Generics                       (Par1 (Par1))
+import qualified Prelude
+import           GHC.Generics
 
 import           ZkFold.Base.Algebra.Basic.Class
+import           ZkFold.Base.Algebra.Basic.Field
 import           ZkFold.Symbolic.Class
 import           ZkFold.Symbolic.Data.Bool          (Bool (Bool), BoolType)
 import           ZkFold.Symbolic.Data.Class
@@ -23,17 +26,19 @@ class BoolType b => Conditional b a where
     --
     -- [On false] @bool onFalse onTrue 'false' == onFalse@
     bool :: a -> a -> b -> a
+    default bool :: (Generic a, GConditional b (Rep a)) => a -> a -> b -> a
+    bool f t b = to (gbool (from f) (from t) b)
 
-gif :: Conditional b a => b -> a -> a -> a
-gif b x y = bool y x b
+ifThenElse :: Conditional b a => b -> a -> a -> a
+ifThenElse b x y = bool y x b
 
 (?) :: Conditional b a => b -> a -> a -> a
-(?) = gif
+(?) = ifThenElse
 
-instance ( SymbolicData x, Context x ~ c, Symbolic c
-         , Representable (Layout x), Traversable (Layout x)
-         , Representable (Payload x)
-         ) => Conditional (Bool c) x where
+instance ( Symbolic c
+         , Traversable f
+         , Representable f
+         ) => Conditional (Bool c) (c f) where
     bool x y (Bool b) = restore $ \s ->
       ( fromCircuit3F b (arithmetize x s) (arithmetize y s) $ \(Par1 c) ->
           mzipWithMRep $ \i j -> do
@@ -46,3 +51,41 @@ instance ( SymbolicData x, Context x ~ c, Symbolic c
               (payload x s)
               (payload y s)
       )
+
+deriving newtype instance Symbolic c => Conditional (Bool c) (Bool c)
+
+instance Conditional Prelude.Bool Prelude.Bool where bool = H.bool
+instance Conditional Prelude.Bool Prelude.String where bool = H.bool
+instance Conditional Prelude.Bool (Zp n) where bool = H.bool
+instance Conditional bool field => Conditional bool (Ext2 field i)
+instance Conditional bool field => Conditional bool (Ext3 field i)
+
+instance
+  ( Conditional b x0
+  , Conditional b x1
+  ) => Conditional b (x0,x1)
+
+instance
+  ( Conditional b x0
+  , Conditional b x1
+  , Conditional b x2
+  ) => Conditional b (x0,x1,x2)
+
+instance
+  ( Conditional b x0
+  , Conditional b x1
+  , Conditional b x2
+  , Conditional b x3
+  ) => Conditional b (x0,x1,x2,x3)
+
+class BoolType b => GConditional b u where
+    gbool :: u x -> u x -> b -> u x
+
+instance (BoolType b, GConditional b u, GConditional b v) => GConditional b (u :*: v) where
+  gbool (f0 :*: f1) (t0 :*: t1) b = gbool f0 t0 b :*: gbool f1 t1 b
+
+instance GConditional b v => GConditional b (M1 i c v) where
+  gbool (M1 f) (M1 t) b = M1 (gbool f t b)
+
+instance Conditional b x => GConditional b (Rec0 x) where
+  gbool (K1 f) (K1 t) b = K1 (bool f t b)
diff --git a/symbolic-base/src/ZkFold/Symbolic/Data/Ed25519.hs b/symbolic-base/src/ZkFold/Symbolic/Data/Ed25519.hs
index 8f727182f..7b18bc26f 100644
--- a/symbolic-base/src/ZkFold/Symbolic/Data/Ed25519.hs
+++ b/symbolic-base/src/ZkFold/Symbolic/Data/Ed25519.hs
@@ -1,14 +1,13 @@
+{-# LANGUAGE RebindableSyntax #-}
 {-# LANGUAGE TypeOperators        #-}
 {-# LANGUAGE UndecidableInstances #-}
 
 {-# OPTIONS_GHC -Wno-orphans #-}
 
-module ZkFold.Symbolic.Data.Ed25519 () where
+module ZkFold.Symbolic.Data.Ed25519 (AcEd25519) where
 
 import           Control.DeepSeq                           (NFData, force)
-import           Data.Functor.Rep                          (Representable)
-import           Data.Traversable                          (Traversable)
-import           Prelude                                   (type (~), ($))
+import           Prelude                                   (type (~), ($), fromInteger)
 import qualified Prelude                                   as P
 
 import           ZkFold.Base.Algebra.Basic.Class
@@ -26,60 +25,24 @@ import           ZkFold.Symbolic.Data.Eq
 import           ZkFold.Symbolic.Data.FFA
 import           ZkFold.Symbolic.Data.FieldElement
 
-
-instance
-    ( Symbolic c
-    , S.BaseField c ~ a
-    ) => SymbolicData (Point (Ed25519 c)) where
-
-    type Context (Point (Ed25519 c)) = c
-    type Support (Point (Ed25519 c)) = Support (FFA Ed25519_Base c)
-    type Layout (Point (Ed25519 c)) = Layout (FFA Ed25519_Base c, FFA Ed25519_Base c)
-    type Payload (Point (Ed25519 c)) = Payload (FFA Ed25519_Base c, FFA Ed25519_Base c)
-
-    -- (0, 0) is never on a Twisted Edwards curve for any curve parameters.
-    -- We can encode the point at infinity as (0, 0), therefore.
-    -- Moreover, (0, 0) acts as the point at infinity when used in the addition formula.
-    -- We can restore Inf as (0, 0) since we can't arithmetise sum-types.
-    -- It will need additional checks in pointDouble because of the denominator becoming zero, though.
-    -- TODO: Think of a better solution
-    --
-    arithmetize Inf         = arithmetize (zero :: FFA Ed25519_Base c, zero :: FFA Ed25519_Base c)
-    arithmetize (Point x y) = arithmetize (x, y)
-    payload Inf         = payload (zero :: FFA Ed25519_Base c, zero :: FFA Ed25519_Base c)
-    payload (Point x y) = payload (x, y)
-    restore f = Point x y
-        where
-            (x, y) = restore f
-
-instance (Symbolic c) => Eq (Bool c) (Point (Ed25519 c)) where
-    Inf == Inf                     = true
-    Inf == _                       = false
-    _ == Inf                       = false
-    (Point x1 y1) == (Point x2 y2) = x1 == x2 && y1 == y2
-
-    Inf /= Inf                     = false
-    Inf /= _                       = true
-    _ /= Inf                       = true
-    (Point x1 y1) /= (Point x2 y2) = x1 /= x2 || y1 /= y2
+data AcEd25519 c
 
 -- | Ed25519 with @UInt 256 ArithmeticCircuit a@ as computational backend
 --
 instance
     ( Symbolic c
     , NFData (c (V.Vector Size))
-    ) => EllipticCurve (Ed25519 c)  where
-
-    type BaseField (Ed25519 c) = FFA Ed25519_Base c
-    type ScalarField (Ed25519 c) = FieldElement c
+    ) => EllipticCurve (AcEd25519 c)  where
 
-    inf = Inf
+    type BaseField (AcEd25519 c) = FFA Ed25519_Base c
+    type ScalarField (AcEd25519 c) = FieldElement c
+    type BooleanOf (AcEd25519 c) = Bool c
 
-    gen = Point
+    gen = point
             (fromConstant (15112221349535400772501151409588531511454012693041857206046113283949847762202 :: Natural))
             (fromConstant (46316835694926478169428394003475163141307993866256225615783033603165251855960 :: Natural))
 
-    add x y = bool @(Bool c) @(Point (Ed25519 c)) (acAdd25519 x y) (acDouble25519 x) (x == y)
+    add x y = if x == y then acDouble25519 x else acAdd25519 x y
 
     -- pointMul uses natScale which converts the scale to Natural.
     -- We can't convert arithmetic circuits to Natural, so we can't use pointMul either.
@@ -90,13 +53,11 @@ instance
     ( EllipticCurve c
     , SymbolicData (Point c)
     , l ~ Layout (Point c)
-    , Representable l
-    , Traversable l
-    , Representable (Payload (Point c))
     , ctx ~ Context (Point c)
     , Symbolic ctx
     , a ~ S.BaseField ctx
     , bits ~ NumberOfBits a
+    , BooleanOf c ~ Bool ctx
     ) => Scale (FieldElement ctx) (Point c) where
 
     scale sc x = sum $ P.zipWith (\b p -> bool @(Bool ctx) zero p (isSet bits b)) [upper, upper -! 1 .. 0] (P.iterate (\e -> e + e) x)
@@ -117,12 +78,13 @@ acAdd25519
     :: forall c
     .  Symbolic c
     => NFData (c (V.Vector Size))
-    => Point (Ed25519 c)
-    -> Point (Ed25519 c)
-    -> Point (Ed25519 c)
-acAdd25519 Inf q = q
-acAdd25519 p Inf = p
-acAdd25519 (Point x1 y1) (Point x2 y2) = Point x3 y3
+    => Point (AcEd25519 c)
+    -> Point (AcEd25519 c)
+    -> Point (AcEd25519 c)
+acAdd25519 p@(Point x1 y1 isInf1) q@(Point x2 y2 isInf2) =
+    if isInf1 then q
+    else if isInf2 then p
+    else point x3 y3
     where
         prodx = x1 * x2
         prody = y1 * y2
@@ -134,10 +96,10 @@ acDouble25519
     :: forall c
     .  Symbolic c
     => NFData (c (V.Vector Size))
-    => Point (Ed25519 c)
-    -> Point (Ed25519 c)
-acDouble25519 Inf = Inf
-acDouble25519 (Point x1 y1) = Point x3 y3
+    => Point (AcEd25519 c)
+    -> Point (AcEd25519 c)
+acDouble25519 (Point x1 y1 isInf) =
+    if isInf then inf else point x3 y3
     where
         xsq = x1 * x1
         ysq = y1 * y1
diff --git a/symbolic-base/src/ZkFold/Symbolic/Data/Eq.hs b/symbolic-base/src/ZkFold/Symbolic/Data/Eq.hs
index 40f68e2a8..86b15adde 100644
--- a/symbolic-base/src/ZkFold/Symbolic/Data/Eq.hs
+++ b/symbolic-base/src/ZkFold/Symbolic/Data/Eq.hs
@@ -18,6 +18,8 @@ import           Prelude                          (return, ($))
 import qualified Prelude                          as Haskell
 
 import           ZkFold.Base.Algebra.Basic.Class
+import           ZkFold.Base.Algebra.Basic.Field
+import           ZkFold.Base.Algebra.Basic.Number
 import           ZkFold.Base.Data.Package
 import           ZkFold.Base.Data.Vector
 import           ZkFold.Symbolic.Class
@@ -39,7 +41,16 @@ class Eq b a where
 elem :: (BoolType b, Eq b a, Foldable t) => a -> t a -> b
 elem x = any (== x)
 
-instance Haskell.Eq a => Eq Haskell.Bool a where
+instance Eq Haskell.Bool Natural where
+    (==) = (Haskell.==)
+    (/=) = (Haskell./=)
+instance Eq Haskell.Bool Haskell.Bool where
+    (==) = (Haskell.==)
+    (/=) = (Haskell./=)
+instance Eq Haskell.Bool Haskell.String where
+    (==) = (Haskell.==)
+    (/=) = (Haskell./=)
+instance KnownNat n => Eq Haskell.Bool (Zp n) where
     (==) = (Haskell.==)
     (/=) = (Haskell./=)
 
@@ -82,6 +93,9 @@ instance (BoolType b, Eq b x0, Eq b x1) => Eq b (x0,x1)
 instance (BoolType b, Eq b x0, Eq b x1, Eq b x2) => Eq b (x0,x1,x2)
 instance (BoolType b, Eq b x0, Eq b x1, Eq b x2, Eq b x3) => Eq b (x0,x1,x2,x3)
 
+instance (BoolType bool, Eq bool field) => Eq bool (Ext2 field i)
+instance (BoolType bool, Eq bool field) => Eq bool (Ext3 field i)
+
 class GEq b u where
     geq :: u x -> u x -> b
     gneq :: u x -> u x -> b
diff --git a/symbolic-base/src/ZkFold/Symbolic/Data/FFA.hs b/symbolic-base/src/ZkFold/Symbolic/Data/FFA.hs
index 440176025..5ea1a142d 100644
--- a/symbolic-base/src/ZkFold/Symbolic/Data/FFA.hs
+++ b/symbolic-base/src/ZkFold/Symbolic/Data/FFA.hs
@@ -28,6 +28,7 @@ import           ZkFold.Symbolic.Class
 import           ZkFold.Symbolic.Data.Bool        (Bool, BoolType (..))
 import           ZkFold.Symbolic.Data.Class
 import           ZkFold.Symbolic.Data.Combinators (expansionW, log2, maxBitsPerFieldElement, splitExpansion)
+import           ZkFold.Symbolic.Data.Conditional
 import           ZkFold.Symbolic.Data.Eq
 import           ZkFold.Symbolic.Data.Input
 import           ZkFold.Symbolic.Data.Ord         (blueprintGE)
@@ -214,6 +215,8 @@ instance Finite (Zp p) => Finite (FFA p b) where
 -- FIXME: This Eq instance is wrong
 deriving newtype instance Symbolic c => Eq (Bool c) (FFA p c)
 
+deriving newtype instance Symbolic c => Conditional (Bool c) (FFA p c)
+
 -- | TODO: fix when rewrite is done
 instance (Symbolic c) => SymbolicInput (FFA p c) where
   isValid _ = true
diff --git a/symbolic-base/src/ZkFold/Symbolic/Data/FieldElement.hs b/symbolic-base/src/ZkFold/Symbolic/Data/FieldElement.hs
index bb6a4184b..6dcb47d17 100644
--- a/symbolic-base/src/ZkFold/Symbolic/Data/FieldElement.hs
+++ b/symbolic-base/src/ZkFold/Symbolic/Data/FieldElement.hs
@@ -41,8 +41,7 @@ deriving newtype instance Symbolic c => SymbolicData (FieldElement c)
 
 deriving newtype instance Symbolic c => Eq (Bool c) (FieldElement c)
 
-deriving via (Lexicographical (FieldElement c))
-  instance Symbolic c => Ord (Bool c) (FieldElement c)
+deriving newtype instance Symbolic c => Ord (Bool c) (FieldElement c)
 
 instance {-# INCOHERENT #-} (Symbolic c, FromConstant k (BaseField c)) => FromConstant k (FieldElement c) where
   fromConstant = FieldElement . embed . Par1 . fromConstant
diff --git a/symbolic-base/src/ZkFold/Symbolic/Data/Maybe.hs b/symbolic-base/src/ZkFold/Symbolic/Data/Maybe.hs
index 19716491b..b7753d9f7 100644
--- a/symbolic-base/src/ZkFold/Symbolic/Data/Maybe.hs
+++ b/symbolic-base/src/ZkFold/Symbolic/Data/Maybe.hs
@@ -18,6 +18,7 @@ import           ZkFold.Symbolic.Class
 import           ZkFold.Symbolic.Data.Bool
 import           ZkFold.Symbolic.Data.Class
 import           ZkFold.Symbolic.Data.Conditional
+import           ZkFold.Symbolic.Data.Eq
 
 data Maybe context x = Maybe { isJust :: Bool context, fromJust :: x }
   deriving stock
@@ -29,6 +30,10 @@ data Maybe context x = Maybe { isJust :: Bool context, fromJust :: x }
 
 deriving stock instance (Haskell.Eq (context Par1), Haskell.Eq x) => Haskell.Eq (Maybe context x)
 
+instance (SymbolicOutput x, Context x ~ c) => SymbolicData (Maybe c x) where
+instance (SymbolicOutput x, Context x ~ c, Conditional (Bool c) x) => Conditional (Bool c) (Maybe c x)
+instance (SymbolicOutput x, Context x ~ c, Eq (Bool c) x) => Eq (Bool c) (Maybe c x)
+
 just :: Symbolic c => x -> Maybe c x
 just = Maybe true
 
@@ -41,22 +46,20 @@ nothing =
 
 fromMaybe ::
   forall c x .
-  (SymbolicData x, Context x ~ c) =>
+  Conditional (Bool c) x =>
   x -> Maybe c x -> x
 fromMaybe a (Maybe j t) = bool a t j
 
 isNothing :: Symbolic c => Maybe c x -> Bool c
 isNothing (Maybe h _) = not h
 
-instance (SymbolicOutput x, Context x ~ c) => SymbolicData (Maybe c x) where
-
 maybe :: forall a b c .
-    (SymbolicData b, Context b ~ c) =>
+    Conditional (Bool c) b =>
     b -> (a -> b) -> Maybe c a -> b
 maybe d h m = fromMaybe d (h <$> m)
 
 find :: forall a c t .
-    ( SymbolicOutput a, Context a ~ c, Haskell.Foldable t) =>
+    (SymbolicOutput a, Context a ~ c, Haskell.Foldable t, Conditional (Bool c) a) =>
     (a -> Bool c) -> t a -> Maybe c a
 find p = let n = nothing in
     foldr (\i r -> maybe @a @_ @c (bool @(Bool c) n (just i) $ p i) (Haskell.const r) r) n
diff --git a/symbolic-base/src/ZkFold/Symbolic/Data/Ord.hs b/symbolic-base/src/ZkFold/Symbolic/Data/Ord.hs
index 1613ecd27..d3e22e239 100644
--- a/symbolic-base/src/ZkFold/Symbolic/Data/Ord.hs
+++ b/symbolic-base/src/ZkFold/Symbolic/Data/Ord.hs
@@ -4,7 +4,7 @@
 {-# LANGUAGE TypeOperators        #-}
 {-# LANGUAGE UndecidableInstances #-}
 
-module ZkFold.Symbolic.Data.Ord (Ord (..), Lexicographical (..), blueprintGE, bitwiseGE, bitwiseGT, getBitsBE) where
+module ZkFold.Symbolic.Data.Ord (Ord (..), blueprintGE, bitwiseGE, bitwiseGT, getBitsBE) where
 
 import           Control.Monad                    (foldM)
 import qualified Data.Bool                        as Haskell
@@ -12,8 +12,9 @@ import           Data.Data                        (Proxy (..))
 import           Data.Foldable                    (Foldable, concatMap, toList)
 import           Data.Function                    ((.))
 import           Data.Functor                     (fmap, (<$>))
+import           Data.Functor.Rep                 (Representable)
 import           Data.List                        (map, reverse)
-import           Data.Traversable                 (traverse)
+import           Data.Traversable                 (Traversable (traverse))
 import qualified Data.Zip                         as Z
 import           GHC.Generics                     (Par1 (..))
 import           Prelude                          (type (~), ($))
@@ -57,18 +58,12 @@ instance Haskell.Ord a => Ord Haskell.Bool a where
 
     min = Haskell.min
 
-newtype Lexicographical a = Lexicographical a
--- ^ A newtype wrapper for easy definition of Ord instances
--- (though not necessarily a most effective one)
-
-deriving newtype instance SymbolicData a => SymbolicData (Lexicographical a)
-
 -- | Every @SymbolicData@ type can be compared lexicographically.
 instance
     ( Symbolic c
-    , SymbolicOutput x
-    , Context x ~ c
-    ) => Ord (Bool c) (Lexicographical x) where
+    , Representable f
+    , Traversable f
+    ) => Ord (Bool c) (c f) where
 
     x <= y = y >= x
 
diff --git a/symbolic-base/src/ZkFold/Symbolic/Data/UInt.hs b/symbolic-base/src/ZkFold/Symbolic/Data/UInt.hs
index adad935b4..7c9639101 100644
--- a/symbolic-base/src/ZkFold/Symbolic/Data/UInt.hs
+++ b/symbolic-base/src/ZkFold/Symbolic/Data/UInt.hs
@@ -64,6 +64,8 @@ deriving instance (NFData (context (Vector (NumberOfRegisters (BaseField context
 deriving instance (Haskell.Eq (context (Vector (NumberOfRegisters (BaseField context) n r)))) => Haskell.Eq (UInt n r context)
 deriving instance (Haskell.Show (BaseField context), Haskell.Show (context (Vector (NumberOfRegisters (BaseField context) n r)))) => Haskell.Show (UInt n r context)
 deriving newtype instance (KnownRegisters c n r, Symbolic c) => SymbolicData (UInt n r c)
+deriving newtype instance (KnownRegisters c n r, Symbolic c) => Conditional (Bool c) (UInt n r c)
+deriving newtype instance (KnownRegisters c n r, Symbolic c) => Eq (Bool c) (UInt n r c)
 
 instance (Symbolic c, KnownNat n, KnownRegisterSize r) => FromConstant Natural (UInt n r c) where
     fromConstant c = UInt . embed @c $ naturalToVector @c @n @r c
@@ -128,7 +130,7 @@ bitsPow 0 _ res _ _ = res
 bitsPow b bits res n m = bitsPow (b -! 1) bits newRes sq m
     where
         sq = (n * n) `mod` m
-        newRes = force $ gif (isSet bits (b -! 1)) ((res * n) `mod` m) res
+        newRes = force $ ifThenElse (isSet bits (b -! 1)) ((res * n) `mod` m) res
 
 
 cast :: forall a n r . (Arithmetic a, KnownNat n, KnownRegisterSize r) => Natural -> ([Natural], Natural, [Natural])
@@ -461,10 +463,6 @@ instance
     , KnownRegisterSize r
     ) => Ring (UInt n r c)
 
-deriving newtype
-         instance (Symbolic c, KnownRegisters c n rs) =>
-         Eq (Bool c) (UInt n rs c)
-
 --------------------------------------------------------------------------------
 
 class StrictConv b a where

From ac2d6c953e15d66cd080a67f7be7a9d54e3b94f2 Mon Sep 17 00:00:00 2001
From: echatav <echatav@users.noreply.github.com>
Date: Tue, 10 Dec 2024 23:02:54 +0000
Subject: [PATCH 02/12] stylish-haskell auto-commit

---
 .../Base/Algebra/EllipticCurve/Class.hs       | 20 +++++++++----------
 .../Base/Algebra/EllipticCurve/Ed25519.hs     |  4 ++--
 .../Base/Algebra/EllipticCurve/Pairing.hs     |  3 +--
 .../src/ZkFold/Base/Protocol/Plonk/Prover.hs  |  4 ++--
 .../ZkFold/Base/Protocol/Plonk/Verifier.hs    |  4 ++--
 .../src/ZkFold/Base/Protocol/Plonkup/Proof.hs |  2 +-
 .../ZkFold/Base/Protocol/Plonkup/Prover.hs    |  4 ++--
 .../Base/Protocol/Plonkup/Prover/Setup.hs     |  2 +-
 .../src/ZkFold/Base/Protocol/Plonkup/Setup.hs |  2 +-
 .../ZkFold/Base/Protocol/Plonkup/Verifier.hs  |  4 ++--
 .../Protocol/Plonkup/Verifier/Commitments.hs  |  2 +-
 .../Base/Protocol/Plonkup/Verifier/Setup.hs   |  2 +-
 .../ZkFold/Symbolic/Algorithms/ECDSA/ECDSA.hs |  2 +-
 .../src/ZkFold/Symbolic/Data/Conditional.hs   |  2 +-
 .../src/ZkFold/Symbolic/Data/Ed25519.hs       |  4 ++--
 15 files changed, 30 insertions(+), 31 deletions(-)

diff --git a/symbolic-base/src/ZkFold/Base/Algebra/EllipticCurve/Class.hs b/symbolic-base/src/ZkFold/Base/Algebra/EllipticCurve/Class.hs
index ebc1207bb..ce41700ac 100644
--- a/symbolic-base/src/ZkFold/Base/Algebra/EllipticCurve/Class.hs
+++ b/symbolic-base/src/ZkFold/Base/Algebra/EllipticCurve/Class.hs
@@ -1,9 +1,9 @@
-{-# LANGUAGE AllowAmbiguousTypes  #-}
-{-# LANGUAGE DeriveAnyClass       #-}
+{-# LANGUAGE AllowAmbiguousTypes   #-}
+{-# LANGUAGE DeriveAnyClass        #-}
 {-# LANGUAGE DuplicateRecordFields #-}
-{-# LANGUAGE RebindableSyntax     #-}
-{-# LANGUAGE TypeOperators        #-}
-{-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE RebindableSyntax      #-}
+{-# LANGUAGE TypeOperators         #-}
+{-# LANGUAGE UndecidableInstances  #-}
 
 module ZkFold.Base.Algebra.EllipticCurve.Class where
 
@@ -11,7 +11,7 @@ import           Data.Functor                     ((<&>))
 import           Data.Kind                        (Type)
 import           Data.String                      (fromString)
 import           GHC.Generics                     (Generic)
-import           Prelude                          (fromInteger, Integer, Show (..), (++), (.), (<$>), type (~))
+import           Prelude                          (Integer, Show (..), fromInteger, type (~), (++), (.), (<$>))
 import qualified Prelude                          as P
 import           Test.QuickCheck                  hiding (scale)
 
@@ -25,8 +25,8 @@ import           ZkFold.Symbolic.Data.Eq
 import           ZkFold.Symbolic.Data.Ord
 
 data Point (curve :: Type) = Point
-  { _x :: BaseField curve
-  , _y :: BaseField curve
+  { _x     :: BaseField curve
+  , _y     :: BaseField curve
   , _isInf :: BooleanOf curve
   } deriving (Generic)
 
@@ -194,9 +194,9 @@ class EllipticCurve curve => StandardEllipticCurve curve where
     bParameter :: BaseField curve
 
 data PointCompressed curve = PointCompressed
-  { _x :: BaseField curve
+  { _x    :: BaseField curve
   , _bigY :: BooleanOf curve
-  , _inf :: BooleanOf curve
+  , _inf  :: BooleanOf curve
   } deriving Generic
 
 pointCompressed :: BoolType (BooleanOf curve) => BaseField curve -> BooleanOf curve -> PointCompressed curve
diff --git a/symbolic-base/src/ZkFold/Base/Algebra/EllipticCurve/Ed25519.hs b/symbolic-base/src/ZkFold/Base/Algebra/EllipticCurve/Ed25519.hs
index 3c5a8abae..f9edf00ea 100644
--- a/symbolic-base/src/ZkFold/Base/Algebra/EllipticCurve/Ed25519.hs
+++ b/symbolic-base/src/ZkFold/Base/Algebra/EllipticCurve/Ed25519.hs
@@ -1,9 +1,9 @@
-{-# LANGUAGE RebindableSyntax     #-}
+{-# LANGUAGE RebindableSyntax #-}
 {-# OPTIONS_GHC -Wno-orphans #-}
 
 module ZkFold.Base.Algebra.EllipticCurve.Ed25519  where
 
-import           Prelude                                 (($), fromInteger)
+import           Prelude                                 (fromInteger, ($))
 
 import           ZkFold.Base.Algebra.Basic.Class
 import           ZkFold.Base.Algebra.Basic.Field
diff --git a/symbolic-base/src/ZkFold/Base/Algebra/EllipticCurve/Pairing.hs b/symbolic-base/src/ZkFold/Base/Algebra/EllipticCurve/Pairing.hs
index 44e3d86a6..b888c0c37 100644
--- a/symbolic-base/src/ZkFold/Base/Algebra/EllipticCurve/Pairing.hs
+++ b/symbolic-base/src/ZkFold/Base/Algebra/EllipticCurve/Pairing.hs
@@ -9,15 +9,14 @@ module ZkFold.Base.Algebra.EllipticCurve.Pairing
   ) where
 
 import qualified Data.Bool                               as H
--- import           Data.Eq                                 (Eq (..))
 import           Data.Function                           (($), (.))
 import           Data.Functor                            ((<$>))
 import           Data.Int                                (Int8)
 import           Data.Tuple                              (snd)
 import           Data.Type.Equality                      (type (~))
 import           Numeric.Natural                         (Natural)
-import qualified Prelude
 import           Prelude                                 (fromInteger)
+import qualified Prelude
 
 import           ZkFold.Base.Algebra.Basic.Class
 import           ZkFold.Base.Algebra.Basic.Field
diff --git a/symbolic-base/src/ZkFold/Base/Protocol/Plonk/Prover.hs b/symbolic-base/src/ZkFold/Base/Protocol/Plonk/Prover.hs
index b2b47202a..f1e395bf0 100644
--- a/symbolic-base/src/ZkFold/Base/Protocol/Plonk/Prover.hs
+++ b/symbolic-base/src/ZkFold/Base/Protocol/Plonk/Prover.hs
@@ -8,8 +8,8 @@ import           Data.Bool                                           (bool)
 import qualified Data.Vector                                         as V
 import           Data.Word                                           (Word8)
 import           GHC.IsList                                          (IsList (..))
-import           Prelude                                             hiding (Num (..), drop, length, pi, sum, take,
-                                                                      (!!), (/), (^), Ord)
+import           Prelude                                             hiding (Num (..), Ord, drop, length, pi, sum, take,
+                                                                      (!!), (/), (^))
 
 import           ZkFold.Base.Algebra.Basic.Class
 import           ZkFold.Base.Algebra.Basic.Number                    (KnownNat, Natural, value)
diff --git a/symbolic-base/src/ZkFold/Base/Protocol/Plonk/Verifier.hs b/symbolic-base/src/ZkFold/Base/Protocol/Plonk/Verifier.hs
index d322e13ab..3c6176288 100644
--- a/symbolic-base/src/ZkFold/Base/Protocol/Plonk/Verifier.hs
+++ b/symbolic-base/src/ZkFold/Base/Protocol/Plonk/Verifier.hs
@@ -7,8 +7,8 @@ module ZkFold.Base.Protocol.Plonk.Verifier
 
 import           Data.Word                                           (Word8)
 import           GHC.IsList                                          (IsList (..))
-import           Prelude                                             hiding (Num (..), drop, length, sum, take, (!!),
-                                                                      (/), (^), Ord)
+import           Prelude                                             hiding (Num (..), Ord, drop, length, sum, take,
+                                                                      (!!), (/), (^))
 
 import           ZkFold.Base.Algebra.Basic.Class
 import           ZkFold.Base.Algebra.Basic.Number                    (KnownNat, Natural, value)
diff --git a/symbolic-base/src/ZkFold/Base/Protocol/Plonkup/Proof.hs b/symbolic-base/src/ZkFold/Base/Protocol/Plonkup/Proof.hs
index 14fe3bf14..f0c4487da 100644
--- a/symbolic-base/src/ZkFold/Base/Protocol/Plonkup/Proof.hs
+++ b/symbolic-base/src/ZkFold/Base/Protocol/Plonkup/Proof.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE TypeOperators        #-}
 {-# LANGUAGE UndecidableInstances #-}
 
 module ZkFold.Base.Protocol.Plonkup.Proof where
diff --git a/symbolic-base/src/ZkFold/Base/Protocol/Plonkup/Prover.hs b/symbolic-base/src/ZkFold/Base/Protocol/Plonkup/Prover.hs
index 936146ee1..3596713c8 100644
--- a/symbolic-base/src/ZkFold/Base/Protocol/Plonkup/Prover.hs
+++ b/symbolic-base/src/ZkFold/Base/Protocol/Plonkup/Prover.hs
@@ -11,8 +11,8 @@ import           Data.Bool                                           (bool)
 import qualified Data.Vector                                         as V
 import           Data.Word                                           (Word8)
 import           GHC.IsList                                          (IsList (..))
-import           Prelude                                             hiding (Num (..), drop, length, pi, sum, take,
-                                                                      (!!), (/), (^), Ord (..))
+import           Prelude                                             hiding (Num (..), Ord (..), drop, length, pi, sum,
+                                                                      take, (!!), (/), (^))
 
 import           ZkFold.Base.Algebra.Basic.Class
 import           ZkFold.Base.Algebra.Basic.Number                    (KnownNat, Natural, value)
diff --git a/symbolic-base/src/ZkFold/Base/Protocol/Plonkup/Prover/Setup.hs b/symbolic-base/src/ZkFold/Base/Protocol/Plonkup/Prover/Setup.hs
index 516a59592..3d4552d6d 100644
--- a/symbolic-base/src/ZkFold/Base/Protocol/Plonkup/Prover/Setup.hs
+++ b/symbolic-base/src/ZkFold/Base/Protocol/Plonkup/Prover/Setup.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE TypeOperators        #-}
 {-# LANGUAGE UndecidableInstances #-}
 
 module ZkFold.Base.Protocol.Plonkup.Prover.Setup where
diff --git a/symbolic-base/src/ZkFold/Base/Protocol/Plonkup/Setup.hs b/symbolic-base/src/ZkFold/Base/Protocol/Plonkup/Setup.hs
index b6e128e7e..701e87af3 100644
--- a/symbolic-base/src/ZkFold/Base/Protocol/Plonkup/Setup.hs
+++ b/symbolic-base/src/ZkFold/Base/Protocol/Plonkup/Setup.hs
@@ -1,5 +1,5 @@
 {-# LANGUAGE AllowAmbiguousTypes  #-}
-{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE TypeOperators        #-}
 {-# LANGUAGE UndecidableInstances #-}
 
 module ZkFold.Base.Protocol.Plonkup.Setup where
diff --git a/symbolic-base/src/ZkFold/Base/Protocol/Plonkup/Verifier.hs b/symbolic-base/src/ZkFold/Base/Protocol/Plonkup/Verifier.hs
index 9380534fa..b742c1279 100644
--- a/symbolic-base/src/ZkFold/Base/Protocol/Plonkup/Verifier.hs
+++ b/symbolic-base/src/ZkFold/Base/Protocol/Plonkup/Verifier.hs
@@ -9,8 +9,8 @@ module ZkFold.Base.Protocol.Plonkup.Verifier
 
 import           Data.Word                                           (Word8)
 import           GHC.IsList                                          (IsList (..))
-import           Prelude                                             hiding (Num (..), drop, length, sum, take, (!!),
-                                                                      (/), (^), Ord (..))
+import           Prelude                                             hiding (Num (..), Ord (..), drop, length, sum,
+                                                                      take, (!!), (/), (^))
 
 import           ZkFold.Base.Algebra.Basic.Class
 import           ZkFold.Base.Algebra.Basic.Number                    (KnownNat, Natural, value)
diff --git a/symbolic-base/src/ZkFold/Base/Protocol/Plonkup/Verifier/Commitments.hs b/symbolic-base/src/ZkFold/Base/Protocol/Plonkup/Verifier/Commitments.hs
index d82186d32..cb057c01f 100644
--- a/symbolic-base/src/ZkFold/Base/Protocol/Plonkup/Verifier/Commitments.hs
+++ b/symbolic-base/src/ZkFold/Base/Protocol/Plonkup/Verifier/Commitments.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE TypeOperators        #-}
 {-# LANGUAGE UndecidableInstances #-}
 
 module ZkFold.Base.Protocol.Plonkup.Verifier.Commitments where
diff --git a/symbolic-base/src/ZkFold/Base/Protocol/Plonkup/Verifier/Setup.hs b/symbolic-base/src/ZkFold/Base/Protocol/Plonkup/Verifier/Setup.hs
index f75b4f4bf..67bd3ac4b 100644
--- a/symbolic-base/src/ZkFold/Base/Protocol/Plonkup/Verifier/Setup.hs
+++ b/symbolic-base/src/ZkFold/Base/Protocol/Plonkup/Verifier/Setup.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE TypeOperators        #-}
 {-# LANGUAGE UndecidableInstances #-}
 
 module ZkFold.Base.Protocol.Plonkup.Verifier.Setup where
diff --git a/symbolic-base/src/ZkFold/Symbolic/Algorithms/ECDSA/ECDSA.hs b/symbolic-base/src/ZkFold/Symbolic/Algorithms/ECDSA/ECDSA.hs
index 202977063..243a1083b 100644
--- a/symbolic-base/src/ZkFold/Symbolic/Algorithms/ECDSA/ECDSA.hs
+++ b/symbolic-base/src/ZkFold/Symbolic/Algorithms/ECDSA/ECDSA.hs
@@ -1,5 +1,5 @@
 {-# LANGUAGE AllowAmbiguousTypes #-}
-{-# LANGUAGE RebindableSyntax #-}
+{-# LANGUAGE RebindableSyntax    #-}
 {-# LANGUAGE TypeOperators       #-}
 module ZkFold.Symbolic.Algorithms.ECDSA.ECDSA where
 import           Data.Type.Equality
diff --git a/symbolic-base/src/ZkFold/Symbolic/Data/Conditional.hs b/symbolic-base/src/ZkFold/Symbolic/Data/Conditional.hs
index e588dab40..9e19c915e 100644
--- a/symbolic-base/src/ZkFold/Symbolic/Data/Conditional.hs
+++ b/symbolic-base/src/ZkFold/Symbolic/Data/Conditional.hs
@@ -8,8 +8,8 @@ import           Control.Monad.Representable.Reader (Representable, mzipWithRep)
 import qualified Data.Bool                          as H
 import           Data.Function                      (($))
 import           Data.Traversable                   (Traversable)
-import qualified Prelude
 import           GHC.Generics
+import qualified Prelude
 
 import           ZkFold.Base.Algebra.Basic.Class
 import           ZkFold.Base.Algebra.Basic.Field
diff --git a/symbolic-base/src/ZkFold/Symbolic/Data/Ed25519.hs b/symbolic-base/src/ZkFold/Symbolic/Data/Ed25519.hs
index 7b18bc26f..0b1142f0c 100644
--- a/symbolic-base/src/ZkFold/Symbolic/Data/Ed25519.hs
+++ b/symbolic-base/src/ZkFold/Symbolic/Data/Ed25519.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE RebindableSyntax #-}
+{-# LANGUAGE RebindableSyntax     #-}
 {-# LANGUAGE TypeOperators        #-}
 {-# LANGUAGE UndecidableInstances #-}
 
@@ -7,7 +7,7 @@
 module ZkFold.Symbolic.Data.Ed25519 (AcEd25519) where
 
 import           Control.DeepSeq                           (NFData, force)
-import           Prelude                                   (type (~), ($), fromInteger)
+import           Prelude                                   (fromInteger, type (~), ($))
 import qualified Prelude                                   as P
 
 import           ZkFold.Base.Algebra.Basic.Class

From 2383fbc763834c6074e45fe4425a69ff7cc6d9d3 Mon Sep 17 00:00:00 2001
From: Eitan Chatav <eitan.chatav@gmail.com>
Date: Tue, 10 Dec 2024 15:33:36 -0800
Subject: [PATCH 03/12] fixes

---
 .../ZkFold/Base/Algebra/EllipticCurve/Class.hs  | 16 +++++++++++++++-
 .../src/ZkFold/Base/Protocol/Plonkup.hs         |  1 -
 .../ZkFold/Base/Protocol/Plonkup/Verifier.hs    |  1 -
 .../src/ZkFold/Symbolic/Data/ByteString.hs      |  7 +++----
 .../src/ZkFold/Symbolic/Data/Conditional.hs     |  8 +++++++-
 .../src/ZkFold/Symbolic/Data/FieldElement.hs    |  3 +++
 symbolic-base/test/Tests/Pairing.hs             |  4 ++--
 .../ZkFold/Symbolic/Cardano/Contracts/ZkPass.hs | 11 +++++++----
 .../ZkFold/Symbolic/Cardano/Types/Address.hs    |  3 ++-
 .../src/ZkFold/Symbolic/Cardano/Types/Basic.hs  |  8 ++------
 .../src/ZkFold/Symbolic/Cardano/Types/Input.hs  | 17 +++++++++++++++++
 .../src/ZkFold/Symbolic/Cardano/Types/Output.hs | 15 +++++++++++----
 .../ZkFold/Symbolic/Cardano/Types/OutputRef.hs  |  8 ++++++++
 .../src/ZkFold/Symbolic/Cardano/Types/Value.hs  |  7 +++++++
 symbolic-examples/src/Examples/Commitment.hs    |  8 ++++----
 symbolic-examples/src/Examples/Ed25519.hs       |  6 +++---
 .../src/ZkFold/Symbolic/Ledger/Types/Value.hs   |  3 +--
 .../ZkFold/Symbolic/Ledger/Validation/Update.hs |  3 ++-
 18 files changed, 94 insertions(+), 35 deletions(-)

diff --git a/symbolic-base/src/ZkFold/Base/Algebra/EllipticCurve/Class.hs b/symbolic-base/src/ZkFold/Base/Algebra/EllipticCurve/Class.hs
index ce41700ac..27e4ed160 100644
--- a/symbolic-base/src/ZkFold/Base/Algebra/EllipticCurve/Class.hs
+++ b/symbolic-base/src/ZkFold/Base/Algebra/EllipticCurve/Class.hs
@@ -40,6 +40,13 @@ instance
   , bool ~ BooleanOf curve
   ) => Eq bool (Point curve)
 
+instance
+  ( EllipticCurve curve
+  , BooleanOf curve ~ P.Bool
+  ) => P.Eq (Point curve) where
+  (==) = (==)
+  (/=) = (/=)
+
 instance
   ( Symbolic ctx
   , SymbolicOutput bool
@@ -132,7 +139,7 @@ instance (EllipticCurve curve, Arbitrary (ScalarField curve)) => Arbitrary (Poin
     arbitrary = arbitrary <&> (`mul` gen)
 
 class (EllipticCurve curve1, EllipticCurve curve2, ScalarField curve1 ~ ScalarField curve2,
-        MultiplicativeGroup (TargetGroup curve1 curve2),
+        P.Eq (TargetGroup curve1 curve2), MultiplicativeGroup (TargetGroup curve1 curve2),
         Exponent (TargetGroup curve1 curve2) (ScalarField curve1)) => Pairing curve1 curve2 where
     type TargetGroup curve1 curve2 :: Type
     pairing :: Point curve1 -> Point curve2 -> TargetGroup curve1 curve2
@@ -212,6 +219,13 @@ instance
   , bool ~ BooleanOf curve
   ) => Eq bool (PointCompressed curve)
 
+instance
+  ( EllipticCurve curve
+  , BooleanOf curve ~ P.Bool
+  ) => P.Eq (PointCompressed curve) where
+  (==) = (==)
+  (/=) = (/=)
+
 instance
   ( Show (BaseField curve)
   , Conditional (BooleanOf curve) P.String
diff --git a/symbolic-base/src/ZkFold/Base/Protocol/Plonkup.hs b/symbolic-base/src/ZkFold/Base/Protocol/Plonkup.hs
index 700ca1525..32afddbf0 100644
--- a/symbolic-base/src/ZkFold/Base/Protocol/Plonkup.hs
+++ b/symbolic-base/src/ZkFold/Base/Protocol/Plonkup.hs
@@ -45,7 +45,6 @@ instance forall p i n l c1 c2 ts core.
         , ToTranscript ts (PointCompressed c1)
         , FromTranscript ts (ScalarField c1)
         , CoreFunction c1 core
-        , Eq (TargetGroup c1 c2)
         ) => NonInteractiveProof (Plonkup p i n l c1 c2 ts) core where
     type Transcript (Plonkup p i n l c1 c2 ts)  = ts
     type SetupProve (Plonkup p i n l c1 c2 ts)  = PlonkupProverSetup p i n l c1 c2
diff --git a/symbolic-base/src/ZkFold/Base/Protocol/Plonkup/Verifier.hs b/symbolic-base/src/ZkFold/Base/Protocol/Plonkup/Verifier.hs
index b742c1279..080703782 100644
--- a/symbolic-base/src/ZkFold/Base/Protocol/Plonkup/Verifier.hs
+++ b/symbolic-base/src/ZkFold/Base/Protocol/Plonkup/Verifier.hs
@@ -37,7 +37,6 @@ plonkupVerify :: forall p i n l c1 c2 ts .
     , ToTranscript ts (ScalarField c1)
     , ToTranscript ts (PointCompressed c1)
     , FromTranscript ts (ScalarField c1)
-    , Eq (TargetGroup c1 c2)
     ) => PlonkupVerifierSetup p i n l c1 c2 -> PlonkupInput l c1 -> PlonkupProof c1 -> Bool
 plonkupVerify
     PlonkupVerifierSetup {..}
diff --git a/symbolic-base/src/ZkFold/Symbolic/Data/ByteString.hs b/symbolic-base/src/ZkFold/Symbolic/Data/ByteString.hs
index 877af028d..3f14c8e75 100644
--- a/symbolic-base/src/ZkFold/Symbolic/Data/ByteString.hs
+++ b/symbolic-base/src/ZkFold/Symbolic/Data/ByteString.hs
@@ -55,6 +55,7 @@ import           ZkFold.Symbolic.Class
 import           ZkFold.Symbolic.Data.Bool         (Bool (..), BoolType (..))
 import           ZkFold.Symbolic.Data.Class        (SymbolicData)
 import           ZkFold.Symbolic.Data.Combinators
+import           ZkFold.Symbolic.Data.Conditional  (Conditional)
 import           ZkFold.Symbolic.Data.Eq           (Eq)
 import           ZkFold.Symbolic.Data.FieldElement (FieldElement)
 import           ZkFold.Symbolic.Data.Input        (SymbolicInput, isValid)
@@ -71,10 +72,8 @@ deriving stock instance Haskell.Show (c (Vector n)) => Haskell.Show (ByteString
 deriving stock instance Haskell.Eq (c (Vector n)) => Haskell.Eq (ByteString n c)
 deriving anyclass instance NFData (c (Vector n)) => NFData (ByteString n c)
 deriving newtype instance (KnownNat n, Symbolic c) => SymbolicData (ByteString n c)
-
-
-deriving newtype
-         instance (Symbolic c, KnownNat n) => Eq (Bool c) (ByteString n c)
+deriving newtype instance (Symbolic c, KnownNat n) => Eq (Bool c) (ByteString n c)
+deriving newtype instance (Symbolic c, KnownNat n) => Conditional (Bool c) (ByteString n c)
 
 instance
     ( Symbolic c
diff --git a/symbolic-base/src/ZkFold/Symbolic/Data/Conditional.hs b/symbolic-base/src/ZkFold/Symbolic/Data/Conditional.hs
index 9e19c915e..4730d2e9b 100644
--- a/symbolic-base/src/ZkFold/Symbolic/Data/Conditional.hs
+++ b/symbolic-base/src/ZkFold/Symbolic/Data/Conditional.hs
@@ -4,7 +4,7 @@
 
 module ZkFold.Symbolic.Data.Conditional where
 
-import           Control.Monad.Representable.Reader (Representable, mzipWithRep)
+import           Data.Functor.Rep                   (Representable, mzipWithRep)
 import qualified Data.Bool                          as H
 import           Data.Function                      (($))
 import           Data.Traversable                   (Traversable)
@@ -13,6 +13,8 @@ import qualified Prelude
 
 import           ZkFold.Base.Algebra.Basic.Class
 import           ZkFold.Base.Algebra.Basic.Field
+import           ZkFold.Base.Algebra.Basic.Number
+import           ZkFold.Base.Data.Vector
 import           ZkFold.Symbolic.Class
 import           ZkFold.Symbolic.Data.Bool          (Bool (Bool), BoolType)
 import           ZkFold.Symbolic.Data.Class
@@ -57,6 +59,10 @@ deriving newtype instance Symbolic c => Conditional (Bool c) (Bool c)
 instance Conditional Prelude.Bool Prelude.Bool where bool = H.bool
 instance Conditional Prelude.Bool Prelude.String where bool = H.bool
 instance Conditional Prelude.Bool (Zp n) where bool = H.bool
+
+instance (KnownNat n, Conditional bool x) => Conditional bool (Vector n x) where
+  bool fv tv b = mzipWithRep (\f t -> bool f t b) fv tv
+
 instance Conditional bool field => Conditional bool (Ext2 field i)
 instance Conditional bool field => Conditional bool (Ext3 field i)
 
diff --git a/symbolic-base/src/ZkFold/Symbolic/Data/FieldElement.hs b/symbolic-base/src/ZkFold/Symbolic/Data/FieldElement.hs
index 6dcb47d17..519c2a435 100644
--- a/symbolic-base/src/ZkFold/Symbolic/Data/FieldElement.hs
+++ b/symbolic-base/src/ZkFold/Symbolic/Data/FieldElement.hs
@@ -22,6 +22,7 @@ import           ZkFold.Symbolic.Data.Bool        (Bool, BoolType (true))
 import           ZkFold.Symbolic.Data.Class
 import           ZkFold.Symbolic.Data.Combinators (expansion, horner, runInvert)
 import           ZkFold.Symbolic.Data.Eq          (Eq)
+import           ZkFold.Symbolic.Data.Conditional (Conditional)
 import           ZkFold.Symbolic.Data.Input
 import           ZkFold.Symbolic.Data.Ord
 import           ZkFold.Symbolic.MonadCircuit     (newAssigned)
@@ -39,6 +40,8 @@ deriving newtype instance NFData (c Par1) => NFData (FieldElement c)
 
 deriving newtype instance Symbolic c => SymbolicData (FieldElement c)
 
+deriving newtype instance Symbolic c => Conditional (Bool c) (FieldElement c)
+
 deriving newtype instance Symbolic c => Eq (Bool c) (FieldElement c)
 
 deriving newtype instance Symbolic c => Ord (Bool c) (FieldElement c)
diff --git a/symbolic-base/test/Tests/Pairing.hs b/symbolic-base/test/Tests/Pairing.hs
index 51d621a0f..1a0eedd94 100644
--- a/symbolic-base/test/Tests/Pairing.hs
+++ b/symbolic-base/test/Tests/Pairing.hs
@@ -62,11 +62,11 @@ specPairing'
     => Eq f
     => Show f
     => Arbitrary f
-    => Eq (BaseField c2)
     => Show (BaseField c2)
     => AdditiveGroup (BaseField c1)
-    => Eq (BaseField c1)
     => Show (BaseField c1)
+    => BooleanOf c1 ~ Bool
+    => BooleanOf c2 ~ Bool
     => IO ()
 specPairing' = hspec $ do
     describe "Elliptic curve pairing specification (SLOW)" $ do
diff --git a/symbolic-cardano/src/ZkFold/Symbolic/Cardano/Contracts/ZkPass.hs b/symbolic-cardano/src/ZkFold/Symbolic/Cardano/Contracts/ZkPass.hs
index eb7b1f83d..fbf7390f2 100644
--- a/symbolic-cardano/src/ZkFold/Symbolic/Cardano/Contracts/ZkPass.hs
+++ b/symbolic-cardano/src/ZkFold/Symbolic/Cardano/Contracts/ZkPass.hs
@@ -10,7 +10,7 @@ import           Prelude                                   hiding (Bool, Eq (..)
                                                             (&&), (*), (+))
 
 import           ZkFold.Base.Algebra.Basic.Class
-import           ZkFold.Base.Algebra.EllipticCurve.Class   (EllipticCurve (BaseField), Point (Point))
+import           ZkFold.Base.Algebra.EllipticCurve.Class   (EllipticCurve (BaseField, BooleanOf), Point, point)
 import           ZkFold.Base.Algebra.EllipticCurve.Ed25519
 import qualified ZkFold.Base.Data.Vector                   as V
 import           ZkFold.Base.Data.Vector                   hiding (concat)
@@ -21,6 +21,7 @@ import           ZkFold.Symbolic.Class                     (Symbolic)
 import           ZkFold.Symbolic.Data.Bool
 import           ZkFold.Symbolic.Data.ByteString           (ByteString, concat, toWords)
 import           ZkFold.Symbolic.Data.Combinators          (Iso (..), NumberOfRegisters, RegisterSize (..), resize)
+import           ZkFold.Symbolic.Data.Ed25519
 import           ZkFold.Symbolic.Data.Eq
 import           ZkFold.Symbolic.Data.FieldElement         (FieldElement)
 import           ZkFold.Symbolic.Data.UInt                 (UInt)
@@ -55,6 +56,7 @@ verifyAllocatorSignature :: forall curve context n . (
     , Log2 (Order (S.BaseField context) GHC.TypeNats.- 1) ~ 255
     , KnownNat (NumberOfRegisters (S.BaseField context) 256 'Auto)
     , SHA2N "SHA512/256" context
+    , BooleanOf curve ~ Bool context
     )
     => ByteString 256 context
     -> ByteString 256 context
@@ -75,7 +77,7 @@ verifyAllocatorSignature taskId validatorAddress allocatorAddress allocatorSigna
         (x, y) = splitAt (toWords publicKey) :: (Vector 1 (ByteString 256 context), Vector 1 (ByteString 256 context))
 
         verifyVerdict :: Bool context
-        verifyVerdict = ecdsaVerify @curve @n @context (Point (from $ item x) (from $ item y)) encodedParams (r, s)
+        verifyVerdict = ecdsaVerify @curve @n @context (point (from $ item x) (from $ item y)) encodedParams (r, s)
 
 verifyValidatorSignature :: forall curve context n . (
     EllipticCurve curve
@@ -86,6 +88,7 @@ verifyValidatorSignature :: forall curve context n . (
     , Log2 (Order (S.BaseField context) GHC.TypeNats.- 1) ~ 255
     , KnownNat (NumberOfRegisters (S.BaseField context) 256 'Auto)
     , SHA2N "SHA512/256" context
+    , BooleanOf curve ~ Bool context
     )
     => ByteString 256 context
     -> ByteString 256 context
@@ -107,7 +110,7 @@ verifyValidatorSignature taskId uHash publicFieldsHash validatorAddress validato
         (x, y) = splitAt (toWords publicKey) :: (Vector 1 (ByteString 256 context), Vector 1 (ByteString 256 context))
 
         verifyVerdict :: Bool context
-        verifyVerdict = ecdsaVerify @curve @n @context (Point (from $ item x) (from $ item y)) encodedParams (r, s)
+        verifyVerdict = ecdsaVerify @curve @n @context (point (from $ item x) (from $ item y)) encodedParams (r, s)
 
 extractSignature :: forall context . (Symbolic context)
     => ByteString 520 context
@@ -124,7 +127,7 @@ extractSignature sign = (from $ concat r', from $ concat s', item v')
 
 zkPassSymbolicVerifier ::
     forall context curve n . (
-    curve ~ Ed25519 context -- probably another ec is needed here, for example, secp256k1
+    curve ~ AcEd25519 context -- probably another ec is needed here, for example, secp256k1
     , n ~ Ed25519_Base
     , EllipticCurve curve
     , BaseField curve ~ UInt 256 Auto context
diff --git a/symbolic-cardano/src/ZkFold/Symbolic/Cardano/Types/Address.hs b/symbolic-cardano/src/ZkFold/Symbolic/Cardano/Types/Address.hs
index 1394cd840..e8070a475 100644
--- a/symbolic-cardano/src/ZkFold/Symbolic/Cardano/Types/Address.hs
+++ b/symbolic-cardano/src/ZkFold/Symbolic/Cardano/Types/Address.hs
@@ -10,6 +10,7 @@ import qualified Prelude                             as Haskell
 import           ZkFold.Symbolic.Cardano.Types.Basic
 import           ZkFold.Symbolic.Class               (Symbolic)
 import           ZkFold.Symbolic.Data.Class
+import           ZkFold.Symbolic.Data.Conditional (Conditional)
 import           ZkFold.Symbolic.Data.Eq             (Eq)
 import           ZkFold.Symbolic.Data.Input
 
@@ -28,7 +29,7 @@ deriving instance (Haskell.Eq (ByteString 4 context), Haskell.Eq (ByteString 224
     => Haskell.Eq (Address context)
 
 instance Symbolic context => Eq (Bool context) (Address context)
-
+instance Symbolic context => Conditional (Bool context) (Address context)
 instance Symbolic context => SymbolicData (Address context)
 instance Symbolic context => SymbolicInput (Address context) where
     isValid (Address a p s) = isValid (a, p, s)
diff --git a/symbolic-cardano/src/ZkFold/Symbolic/Cardano/Types/Basic.hs b/symbolic-cardano/src/ZkFold/Symbolic/Cardano/Types/Basic.hs
index 6486169ff..c7badd29b 100644
--- a/symbolic-cardano/src/ZkFold/Symbolic/Cardano/Types/Basic.hs
+++ b/symbolic-cardano/src/ZkFold/Symbolic/Cardano/Types/Basic.hs
@@ -1,6 +1,6 @@
 module ZkFold.Symbolic.Cardano.Types.Basic
-    ( FieldElement
-    , Bool
+    ( Symbolic.FieldElement
+    , Symbolic.Bool
     , Symbolic.ByteString
     , Symbolic.UInt
     , Symbolic.UTCTime
@@ -13,7 +13,3 @@ import qualified ZkFold.Symbolic.Data.ByteString   as Symbolic
 import qualified ZkFold.Symbolic.Data.FieldElement as Symbolic
 import qualified ZkFold.Symbolic.Data.UInt         as Symbolic
 import qualified ZkFold.Symbolic.Data.UTCTime      as Symbolic
-
-type FieldElement context     = Symbolic.FieldElement context
-
-type Bool context = Symbolic.Bool context
diff --git a/symbolic-cardano/src/ZkFold/Symbolic/Cardano/Types/Input.hs b/symbolic-cardano/src/ZkFold/Symbolic/Cardano/Types/Input.hs
index 5e437dcab..056b3f341 100644
--- a/symbolic-cardano/src/ZkFold/Symbolic/Cardano/Types/Input.hs
+++ b/symbolic-cardano/src/ZkFold/Symbolic/Cardano/Types/Input.hs
@@ -14,8 +14,11 @@ import           ZkFold.Symbolic.Cardano.Types.Output    (DatumHash, Output, txo
 import           ZkFold.Symbolic.Cardano.Types.OutputRef (OutputRef)
 import           ZkFold.Symbolic.Cardano.Types.Value     (Value)
 import           ZkFold.Symbolic.Class
+import           ZkFold.Symbolic.Data.Bool
 import           ZkFold.Symbolic.Data.Class
 import           ZkFold.Symbolic.Data.Combinators        (KnownRegisters, RegisterSize (..))
+import           ZkFold.Symbolic.Data.Conditional
+import           ZkFold.Symbolic.Data.Eq
 import           ZkFold.Symbolic.Data.Input              (SymbolicInput, isValid)
 
 data Input tokens datum context = Input  {
@@ -24,6 +27,20 @@ data Input tokens datum context = Input  {
     }
     deriving (Generic)
 
+instance
+    ( Symbolic context
+    , KnownNat tokens
+    , KnownRegisters context 32 Auto
+    , KnownRegisters context 64 Auto
+    ) => Conditional (Bool context) (Input tokens datum context)
+
+instance
+    ( Symbolic context
+    , KnownNat tokens
+    , KnownRegisters context 32 Auto
+    , KnownRegisters context 64 Auto
+    ) => Eq (Bool context) (Input tokens datum context)
+
 deriving instance
     ( Haskell.Eq (OutputRef context)
     , Haskell.Eq (Output tokens datum context)
diff --git a/symbolic-cardano/src/ZkFold/Symbolic/Cardano/Types/Output.hs b/symbolic-cardano/src/ZkFold/Symbolic/Cardano/Types/Output.hs
index f43756482..ee8debfe8 100644
--- a/symbolic-cardano/src/ZkFold/Symbolic/Cardano/Types/Output.hs
+++ b/symbolic-cardano/src/ZkFold/Symbolic/Cardano/Types/Output.hs
@@ -21,6 +21,7 @@ import           ZkFold.Symbolic.Cardano.Types.Value        (SingleAsset, Value)
 import           ZkFold.Symbolic.Class
 import           ZkFold.Symbolic.Data.Class
 import           ZkFold.Symbolic.Data.Combinators           (KnownRegisters, RegisterSize (..))
+import           ZkFold.Symbolic.Data.Conditional           (Conditional)
 import           ZkFold.Symbolic.Data.Eq                    (Eq)
 import           ZkFold.Symbolic.Data.Input                 (SymbolicInput (..))
 
@@ -64,8 +65,14 @@ instance
     isValid (Output a t d) = isValid (a, t,  d)
 
 instance
-            ( Symbolic context
-            , KnownNat tokens
-            , KnownRegisters context 64 Auto
-            ) => Eq (Bool context) (Output tokens datum context)
+    ( Symbolic context
+    , KnownNat tokens
+    , KnownRegisters context 64 Auto
+    ) => Conditional (Bool context) (Output tokens datum context)
+
+instance
+    ( Symbolic context
+    , KnownNat tokens
+    , KnownRegisters context 64 Auto
+    ) => Eq (Bool context) (Output tokens datum context)
 
diff --git a/symbolic-cardano/src/ZkFold/Symbolic/Cardano/Types/OutputRef.hs b/symbolic-cardano/src/ZkFold/Symbolic/Cardano/Types/OutputRef.hs
index 3573b31b2..81a249370 100644
--- a/symbolic-cardano/src/ZkFold/Symbolic/Cardano/Types/OutputRef.hs
+++ b/symbolic-cardano/src/ZkFold/Symbolic/Cardano/Types/OutputRef.hs
@@ -11,6 +11,8 @@ import qualified Prelude                             as Haskell
 import           ZkFold.Symbolic.Cardano.Types.Basic
 import           ZkFold.Symbolic.Class               (Symbolic (..))
 import           ZkFold.Symbolic.Data.Class
+import           ZkFold.Symbolic.Data.Conditional
+import           ZkFold.Symbolic.Data.Eq
 import           ZkFold.Symbolic.Data.Combinators    (KnownRegisters, RegisterSize (..))
 import           ZkFold.Symbolic.Data.Input          (SymbolicInput)
 
@@ -33,3 +35,9 @@ instance (Symbolic context, KnownRegisters context 32 Auto)
 
 instance (Symbolic context, KnownRegisters context 32 Auto)
     => SymbolicInput (OutputRef context) where
+
+instance (Symbolic context, KnownRegisters context 32 Auto)
+    => Conditional (Bool context) (OutputRef context) where
+
+instance (Symbolic context, KnownRegisters context 32 Auto)
+    => Eq (Bool context) (OutputRef context) where
diff --git a/symbolic-cardano/src/ZkFold/Symbolic/Cardano/Types/Value.hs b/symbolic-cardano/src/ZkFold/Symbolic/Cardano/Types/Value.hs
index eea2fb3c0..30a1ee7f4 100644
--- a/symbolic-cardano/src/ZkFold/Symbolic/Cardano/Types/Value.hs
+++ b/symbolic-cardano/src/ZkFold/Symbolic/Cardano/Types/Value.hs
@@ -17,6 +17,7 @@ import           ZkFold.Symbolic.Cardano.Types.Basic
 import           ZkFold.Symbolic.Class               (Symbolic (..))
 import           ZkFold.Symbolic.Data.Class
 import           ZkFold.Symbolic.Data.Combinators    (KnownRegisters, RegisterSize (..))
+import           ZkFold.Symbolic.Data.Conditional
 import           ZkFold.Symbolic.Data.Eq
 import           ZkFold.Symbolic.Data.Input
 
@@ -39,6 +40,12 @@ deriving newtype instance
   , KnownRegisters context 64 Auto
   ) => Eq (Bool context) (Value n context)
 
+deriving newtype instance
+  ( Symbolic context
+  , KnownRegisters context 64 Auto
+  , KnownNat n
+  ) => Conditional (Bool context) (Value n context)
+
 instance
     ( Symbolic context
     , KnownNat n
diff --git a/symbolic-examples/src/Examples/Commitment.hs b/symbolic-examples/src/Examples/Commitment.hs
index c0a7d49e3..211f7340b 100644
--- a/symbolic-examples/src/Examples/Commitment.hs
+++ b/symbolic-examples/src/Examples/Commitment.hs
@@ -3,12 +3,12 @@ module Examples.Commitment (
   ) where
 
 import           ZkFold.Base.Algebra.EllipticCurve.Class
-import           ZkFold.Base.Algebra.EllipticCurve.Ed25519
 import           ZkFold.Base.Data.Vector                   (Vector)
 import           ZkFold.Base.Protocol.Protostar.Commit     (HomomorphicCommit (..))
+import           ZkFold.Symbolic.Data.Ed25519
 
 exampleCommitment
-    :: HomomorphicCommit (Vector 1 (ScalarField (Ed25519 c))) (Point (Ed25519 c))
-    => Vector 1 (ScalarField (Ed25519 c))
-    -> Point (Ed25519 c)
+    :: HomomorphicCommit (Vector 1 (ScalarField (AcEd25519 c))) (Point (AcEd25519 c))
+    => Vector 1 (ScalarField (AcEd25519 c))
+    -> Point (AcEd25519 c)
 exampleCommitment = hcommit
diff --git a/symbolic-examples/src/Examples/Ed25519.hs b/symbolic-examples/src/Examples/Ed25519.hs
index 5d163177d..153d5381e 100644
--- a/symbolic-examples/src/Examples/Ed25519.hs
+++ b/symbolic-examples/src/Examples/Ed25519.hs
@@ -8,7 +8,7 @@ import           Control.DeepSeq                           (NFData)
 
 import           ZkFold.Base.Algebra.Basic.Class
 import           ZkFold.Base.Algebra.EllipticCurve.Class
-import           ZkFold.Base.Algebra.EllipticCurve.Ed25519
+import           ZkFold.Symbolic.Data.Ed25519
 import           ZkFold.Base.Data.Vector                   (Vector)
 import           ZkFold.Symbolic.Class                     (Symbolic)
 import           ZkFold.Symbolic.Data.Ed25519              ()
@@ -19,6 +19,6 @@ exampleEd25519Scale
     :: Symbolic c
     => NFData (c (Vector Size))
     => FieldElement c
-    -> Point (Ed25519 c)
-    -> Point (Ed25519 c)
+    -> Point (AcEd25519 c)
+    -> Point (AcEd25519 c)
 exampleEd25519Scale = scale
diff --git a/zkfold-ledger/src/ZkFold/Symbolic/Ledger/Types/Value.hs b/zkfold-ledger/src/ZkFold/Symbolic/Ledger/Types/Value.hs
index 4f06935b9..85c87f8ce 100644
--- a/zkfold-ledger/src/ZkFold/Symbolic/Ledger/Types/Value.hs
+++ b/zkfold-ledger/src/ZkFold/Symbolic/Ledger/Types/Value.hs
@@ -67,9 +67,8 @@ addValue val (UnsafeMultiAssetValue valList) =
 multiValueAsset ::
      Symbolic context
   => SymbolicOutput (Value context)
-  => SymbolicData (MultiAssetValue context)
   => Context (Value context) ~ context
-  => Context (MultiAssetValue context) ~ context
+  => Conditional (Bool context) (MultiAssetValue context)
   => Eq (Bool context) (CurrencySymbol context)
   => Foldable (List context)
   => List context (Value context)
diff --git a/zkfold-ledger/src/ZkFold/Symbolic/Ledger/Validation/Update.hs b/zkfold-ledger/src/ZkFold/Symbolic/Ledger/Validation/Update.hs
index 458b027f3..660740e5d 100644
--- a/zkfold-ledger/src/ZkFold/Symbolic/Ledger/Validation/Update.hs
+++ b/zkfold-ledger/src/ZkFold/Symbolic/Ledger/Validation/Update.hs
@@ -8,7 +8,7 @@ import           Prelude                                       hiding (Bool, Eq
 
 import           ZkFold.Symbolic.Data.Bool                     (Bool, (&&))
 import           ZkFold.Symbolic.Data.Class                    (SymbolicData (..), SymbolicOutput)
-import           ZkFold.Symbolic.Data.Conditional              (bool)
+import           ZkFold.Symbolic.Data.Conditional              (bool, Conditional)
 import           ZkFold.Symbolic.Data.Eq                       (Eq (..))
 import           ZkFold.Symbolic.Data.List                     (List, concat, singleton, (++))
 import           ZkFold.Symbolic.Ledger.Types
@@ -87,6 +87,7 @@ updateIsValid ::
   => Context (Value context) ~ context
   => Context (MultiAssetValue context) ~ context
   => Eq (Bool context) (MultiAssetValue context)
+  => Conditional (Bool context) (MultiAssetValue context)
   => Hash context
   -> Update context
   -> UpdateWitness context

From 3c7b36fcd72545e428d1f30cbcf249b84ca72a27 Mon Sep 17 00:00:00 2001
From: echatav <echatav@users.noreply.github.com>
Date: Tue, 10 Dec 2024 23:36:56 +0000
Subject: [PATCH 04/12] stylish-haskell auto-commit

---
 .../src/ZkFold/Symbolic/Data/Conditional.hs        | 14 +++++++-------
 .../src/ZkFold/Symbolic/Data/FieldElement.hs       |  2 +-
 .../src/ZkFold/Symbolic/Cardano/Types/Address.hs   |  2 +-
 .../src/ZkFold/Symbolic/Cardano/Types/OutputRef.hs |  2 +-
 symbolic-examples/src/Examples/Commitment.hs       |  4 ++--
 symbolic-examples/src/Examples/Ed25519.hs          |  8 ++++----
 .../ZkFold/Symbolic/Ledger/Validation/Update.hs    |  2 +-
 7 files changed, 17 insertions(+), 17 deletions(-)

diff --git a/symbolic-base/src/ZkFold/Symbolic/Data/Conditional.hs b/symbolic-base/src/ZkFold/Symbolic/Data/Conditional.hs
index 4730d2e9b..dc50b3945 100644
--- a/symbolic-base/src/ZkFold/Symbolic/Data/Conditional.hs
+++ b/symbolic-base/src/ZkFold/Symbolic/Data/Conditional.hs
@@ -4,10 +4,10 @@
 
 module ZkFold.Symbolic.Data.Conditional where
 
-import           Data.Functor.Rep                   (Representable, mzipWithRep)
-import qualified Data.Bool                          as H
-import           Data.Function                      (($))
-import           Data.Traversable                   (Traversable)
+import qualified Data.Bool                        as H
+import           Data.Function                    (($))
+import           Data.Functor.Rep                 (Representable, mzipWithRep)
+import           Data.Traversable                 (Traversable)
 import           GHC.Generics
 import qualified Prelude
 
@@ -16,10 +16,10 @@ import           ZkFold.Base.Algebra.Basic.Field
 import           ZkFold.Base.Algebra.Basic.Number
 import           ZkFold.Base.Data.Vector
 import           ZkFold.Symbolic.Class
-import           ZkFold.Symbolic.Data.Bool          (Bool (Bool), BoolType)
+import           ZkFold.Symbolic.Data.Bool        (Bool (Bool), BoolType)
 import           ZkFold.Symbolic.Data.Class
-import           ZkFold.Symbolic.Data.Combinators   (mzipWithMRep)
-import           ZkFold.Symbolic.MonadCircuit       (newAssigned)
+import           ZkFold.Symbolic.Data.Combinators (mzipWithMRep)
+import           ZkFold.Symbolic.MonadCircuit     (newAssigned)
 
 class BoolType b => Conditional b a where
     -- | Properties:
diff --git a/symbolic-base/src/ZkFold/Symbolic/Data/FieldElement.hs b/symbolic-base/src/ZkFold/Symbolic/Data/FieldElement.hs
index 519c2a435..cd49ba674 100644
--- a/symbolic-base/src/ZkFold/Symbolic/Data/FieldElement.hs
+++ b/symbolic-base/src/ZkFold/Symbolic/Data/FieldElement.hs
@@ -21,8 +21,8 @@ import           ZkFold.Symbolic.Class
 import           ZkFold.Symbolic.Data.Bool        (Bool, BoolType (true))
 import           ZkFold.Symbolic.Data.Class
 import           ZkFold.Symbolic.Data.Combinators (expansion, horner, runInvert)
-import           ZkFold.Symbolic.Data.Eq          (Eq)
 import           ZkFold.Symbolic.Data.Conditional (Conditional)
+import           ZkFold.Symbolic.Data.Eq          (Eq)
 import           ZkFold.Symbolic.Data.Input
 import           ZkFold.Symbolic.Data.Ord
 import           ZkFold.Symbolic.MonadCircuit     (newAssigned)
diff --git a/symbolic-cardano/src/ZkFold/Symbolic/Cardano/Types/Address.hs b/symbolic-cardano/src/ZkFold/Symbolic/Cardano/Types/Address.hs
index e8070a475..98a7676ad 100644
--- a/symbolic-cardano/src/ZkFold/Symbolic/Cardano/Types/Address.hs
+++ b/symbolic-cardano/src/ZkFold/Symbolic/Cardano/Types/Address.hs
@@ -10,7 +10,7 @@ import qualified Prelude                             as Haskell
 import           ZkFold.Symbolic.Cardano.Types.Basic
 import           ZkFold.Symbolic.Class               (Symbolic)
 import           ZkFold.Symbolic.Data.Class
-import           ZkFold.Symbolic.Data.Conditional (Conditional)
+import           ZkFold.Symbolic.Data.Conditional    (Conditional)
 import           ZkFold.Symbolic.Data.Eq             (Eq)
 import           ZkFold.Symbolic.Data.Input
 
diff --git a/symbolic-cardano/src/ZkFold/Symbolic/Cardano/Types/OutputRef.hs b/symbolic-cardano/src/ZkFold/Symbolic/Cardano/Types/OutputRef.hs
index 81a249370..f5b2ba061 100644
--- a/symbolic-cardano/src/ZkFold/Symbolic/Cardano/Types/OutputRef.hs
+++ b/symbolic-cardano/src/ZkFold/Symbolic/Cardano/Types/OutputRef.hs
@@ -11,9 +11,9 @@ import qualified Prelude                             as Haskell
 import           ZkFold.Symbolic.Cardano.Types.Basic
 import           ZkFold.Symbolic.Class               (Symbolic (..))
 import           ZkFold.Symbolic.Data.Class
+import           ZkFold.Symbolic.Data.Combinators    (KnownRegisters, RegisterSize (..))
 import           ZkFold.Symbolic.Data.Conditional
 import           ZkFold.Symbolic.Data.Eq
-import           ZkFold.Symbolic.Data.Combinators    (KnownRegisters, RegisterSize (..))
 import           ZkFold.Symbolic.Data.Input          (SymbolicInput)
 
 type TxRefId context = ByteString 256 context
diff --git a/symbolic-examples/src/Examples/Commitment.hs b/symbolic-examples/src/Examples/Commitment.hs
index 211f7340b..323403d48 100644
--- a/symbolic-examples/src/Examples/Commitment.hs
+++ b/symbolic-examples/src/Examples/Commitment.hs
@@ -3,8 +3,8 @@ module Examples.Commitment (
   ) where
 
 import           ZkFold.Base.Algebra.EllipticCurve.Class
-import           ZkFold.Base.Data.Vector                   (Vector)
-import           ZkFold.Base.Protocol.Protostar.Commit     (HomomorphicCommit (..))
+import           ZkFold.Base.Data.Vector                 (Vector)
+import           ZkFold.Base.Protocol.Protostar.Commit   (HomomorphicCommit (..))
 import           ZkFold.Symbolic.Data.Ed25519
 
 exampleCommitment
diff --git a/symbolic-examples/src/Examples/Ed25519.hs b/symbolic-examples/src/Examples/Ed25519.hs
index 153d5381e..f6ffc3089 100644
--- a/symbolic-examples/src/Examples/Ed25519.hs
+++ b/symbolic-examples/src/Examples/Ed25519.hs
@@ -4,14 +4,14 @@ module Examples.Ed25519 (
     exampleEd25519Scale
   ) where
 
-import           Control.DeepSeq                           (NFData)
+import           Control.DeepSeq                         (NFData)
 
 import           ZkFold.Base.Algebra.Basic.Class
 import           ZkFold.Base.Algebra.EllipticCurve.Class
+import           ZkFold.Base.Data.Vector                 (Vector)
+import           ZkFold.Symbolic.Class                   (Symbolic)
 import           ZkFold.Symbolic.Data.Ed25519
-import           ZkFold.Base.Data.Vector                   (Vector)
-import           ZkFold.Symbolic.Class                     (Symbolic)
-import           ZkFold.Symbolic.Data.Ed25519              ()
+import           ZkFold.Symbolic.Data.Ed25519            ()
 import           ZkFold.Symbolic.Data.FFA
 import           ZkFold.Symbolic.Data.FieldElement
 
diff --git a/zkfold-ledger/src/ZkFold/Symbolic/Ledger/Validation/Update.hs b/zkfold-ledger/src/ZkFold/Symbolic/Ledger/Validation/Update.hs
index 660740e5d..4ebd4120d 100644
--- a/zkfold-ledger/src/ZkFold/Symbolic/Ledger/Validation/Update.hs
+++ b/zkfold-ledger/src/ZkFold/Symbolic/Ledger/Validation/Update.hs
@@ -8,7 +8,7 @@ import           Prelude                                       hiding (Bool, Eq
 
 import           ZkFold.Symbolic.Data.Bool                     (Bool, (&&))
 import           ZkFold.Symbolic.Data.Class                    (SymbolicData (..), SymbolicOutput)
-import           ZkFold.Symbolic.Data.Conditional              (bool, Conditional)
+import           ZkFold.Symbolic.Data.Conditional              (Conditional, bool)
 import           ZkFold.Symbolic.Data.Eq                       (Eq (..))
 import           ZkFold.Symbolic.Data.List                     (List, concat, singleton, (++))
 import           ZkFold.Symbolic.Ledger.Types

From 9b1ec3f499ed55aa40fc1d9bb164adda655777cb Mon Sep 17 00:00:00 2001
From: Eitan Chatav <eitan.chatav@gmail.com>
Date: Tue, 10 Dec 2024 15:38:36 -0800
Subject: [PATCH 05/12] Update Verifier.hs

---
 symbolic-base/src/ZkFold/Base/Protocol/Plonk/Verifier.hs | 1 -
 1 file changed, 1 deletion(-)

diff --git a/symbolic-base/src/ZkFold/Base/Protocol/Plonk/Verifier.hs b/symbolic-base/src/ZkFold/Base/Protocol/Plonk/Verifier.hs
index 3c6176288..4cf302ce7 100644
--- a/symbolic-base/src/ZkFold/Base/Protocol/Plonk/Verifier.hs
+++ b/symbolic-base/src/ZkFold/Base/Protocol/Plonk/Verifier.hs
@@ -34,7 +34,6 @@ plonkVerify :: forall p i n l c1 c2 ts .
     , ToTranscript ts (ScalarField c1)
     , ToTranscript ts (PointCompressed c1)
     , FromTranscript ts (ScalarField c1)
-    , Eq (TargetGroup c1 c2)
     ) => PlonkupVerifierSetup p i n l c1 c2 -> PlonkupInput l c1 -> PlonkupProof c1 -> Bool
 plonkVerify
     PlonkupVerifierSetup {..}

From f4192718bbd08ab92a9f756b499b438eace21b9d Mon Sep 17 00:00:00 2001
From: Eitan Chatav <eitan.chatav@gmail.com>
Date: Tue, 10 Dec 2024 15:41:37 -0800
Subject: [PATCH 06/12] Update Plonk.hs

---
 symbolic-base/src/ZkFold/Base/Protocol/Plonk.hs | 1 -
 1 file changed, 1 deletion(-)

diff --git a/symbolic-base/src/ZkFold/Base/Protocol/Plonk.hs b/symbolic-base/src/ZkFold/Base/Protocol/Plonk.hs
index 2fd042fe2..8a0297023 100644
--- a/symbolic-base/src/ZkFold/Base/Protocol/Plonk.hs
+++ b/symbolic-base/src/ZkFold/Base/Protocol/Plonk.hs
@@ -81,7 +81,6 @@ instance forall p i n l c1 c2 (ts :: Type) core .
         , ToTranscript ts (PointCompressed c1)
         , FromTranscript ts (ScalarField c1)
         , CoreFunction c1 core
-        , Eq (TargetGroup c1 c2)
         ) => NonInteractiveProof (Plonk p i n l c1 c2 ts) core where
     type Transcript (Plonk p i n l c1 c2 ts)  = ts
     type SetupProve (Plonk p i n l c1 c2 ts)  = PlonkupProverSetup p i n l c1 c2

From 5fb505487ab398d3e5f25f5d989913ac5e8fd210 Mon Sep 17 00:00:00 2001
From: Eitan Chatav <eitan.chatav@gmail.com>
Date: Tue, 10 Dec 2024 17:29:35 -0800
Subject: [PATCH 07/12] fixes

---
 symbolic-base/src/ZkFold/Symbolic/Data/Conditional.hs | 6 ++++++
 zkfold-uplc/src/ZkFold/Symbolic/UPLC/Data.hs          | 4 ++++
 zkfold-uplc/src/ZkFold/Symbolic/UPLC/Evaluation.hs    | 5 +++--
 3 files changed, 13 insertions(+), 2 deletions(-)

diff --git a/symbolic-base/src/ZkFold/Symbolic/Data/Conditional.hs b/symbolic-base/src/ZkFold/Symbolic/Data/Conditional.hs
index dc50b3945..3f09e7223 100644
--- a/symbolic-base/src/ZkFold/Symbolic/Data/Conditional.hs
+++ b/symbolic-base/src/ZkFold/Symbolic/Data/Conditional.hs
@@ -7,6 +7,7 @@ module ZkFold.Symbolic.Data.Conditional where
 import qualified Data.Bool                        as H
 import           Data.Function                    (($))
 import           Data.Functor.Rep                 (Representable, mzipWithRep)
+import           Data.Proxy
 import           Data.Traversable                 (Traversable)
 import           GHC.Generics
 import qualified Prelude
@@ -56,8 +57,13 @@ instance ( Symbolic c
 
 deriving newtype instance Symbolic c => Conditional (Bool c) (Bool c)
 
+instance Symbolic c => Conditional (Bool c) (Proxy c) where
+  bool _ _ _ = Proxy
+
 instance Conditional Prelude.Bool Prelude.Bool where bool = H.bool
+
 instance Conditional Prelude.Bool Prelude.String where bool = H.bool
+
 instance Conditional Prelude.Bool (Zp n) where bool = H.bool
 
 instance (KnownNat n, Conditional bool x) => Conditional bool (Vector n x) where
diff --git a/zkfold-uplc/src/ZkFold/Symbolic/UPLC/Data.hs b/zkfold-uplc/src/ZkFold/Symbolic/UPLC/Data.hs
index b9690d12e..2d7076047 100644
--- a/zkfold-uplc/src/ZkFold/Symbolic/UPLC/Data.hs
+++ b/zkfold-uplc/src/ZkFold/Symbolic/UPLC/Data.hs
@@ -1,5 +1,6 @@
 {-# LANGUAGE DerivingStrategies         #-}
 {-# LANGUAGE GeneralizedNewtypeDeriving #-}
+{-# LANGUAGE MultiParamTypeClasses      #-}
 {-# LANGUAGE StandaloneDeriving         #-}
 {-# LANGUAGE TypeFamilies               #-}
 {-# LANGUAGE UndecidableInstances       #-}
@@ -9,7 +10,9 @@ module ZkFold.Symbolic.UPLC.Data where
 import           GHC.Generics               (Par1)
 
 import           ZkFold.Symbolic.Class      (Symbolic)
+import           ZkFold.Symbolic.Data.Bool (Bool)
 import           ZkFold.Symbolic.Data.Class (SymbolicData (..))
+import           ZkFold.Symbolic.Data.Conditional (Conditional)
 import           ZkFold.Symbolic.Data.Input (SymbolicInput)
 
 -- | Plutus Core's Data as a Symbolic datatype.
@@ -18,3 +21,4 @@ newtype Data c = Data (c Par1)
 
 deriving newtype instance Symbolic c => SymbolicData (Data c)
 deriving newtype instance Symbolic c => SymbolicInput (Data c)
+deriving newtype instance Symbolic c => Conditional (Bool c) (Data c)
diff --git a/zkfold-uplc/src/ZkFold/Symbolic/UPLC/Evaluation.hs b/zkfold-uplc/src/ZkFold/Symbolic/UPLC/Evaluation.hs
index db6c2d4c5..4e6883622 100644
--- a/zkfold-uplc/src/ZkFold/Symbolic/UPLC/Evaluation.hs
+++ b/zkfold-uplc/src/ZkFold/Symbolic/UPLC/Evaluation.hs
@@ -31,7 +31,7 @@ import           ZkFold.Prelude                   ((!!))
 import           ZkFold.Symbolic.Class            (Symbolic)
 import           ZkFold.Symbolic.Data.Bool        (Bool, BoolType (..))
 import           ZkFold.Symbolic.Data.Class       (SymbolicData (..))
-import           ZkFold.Symbolic.Data.Conditional (bool)
+import           ZkFold.Symbolic.Data.Conditional (Conditional, bool)
 import qualified ZkFold.Symbolic.Data.Maybe       as Symbolic
 import qualified ZkFold.Symbolic.UPLC.Data        as Symbolic
 import           ZkFold.UPLC.BuiltinFunction
@@ -50,6 +50,7 @@ class
     ( Typeable v, SymbolicData v
     , Context v ~ c, Support v ~ Proxy c
     -- TODO: Remove after Conditional becomes part of SymbolicData
+    , Conditional (Bool c) v
     , Representable (Layout v)
     , Traversable (Layout v)
     , Representable (Payload v)
@@ -235,7 +236,7 @@ instance
 --
 -- Be careful with two layers of Maybe! Think about which errors do you wish to
 -- propagate.
-applyPoly :: Sym c => Env c -> BuiltinPolyFunction s t -> [Arg c] -> SomeValue c
+applyPoly :: forall c s t. Sym c => Env c -> BuiltinPolyFunction s t -> [Arg c] -> SomeValue c
 applyPoly ctx IfThenElse (ct:tt:et:args) = do
   MaybeValue c0 <- evalArg ctx ct []
   withArms (evalArg ctx tt args) (evalArg ctx et args) $ \t e0 -> do

From 415faf00cea2105cec7dfc427570ace7b65c5d9a Mon Sep 17 00:00:00 2001
From: echatav <echatav@users.noreply.github.com>
Date: Wed, 11 Dec 2024 01:32:50 +0000
Subject: [PATCH 08/12] stylish-haskell auto-commit

---
 zkfold-uplc/src/ZkFold/Symbolic/UPLC/Data.hs | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

diff --git a/zkfold-uplc/src/ZkFold/Symbolic/UPLC/Data.hs b/zkfold-uplc/src/ZkFold/Symbolic/UPLC/Data.hs
index 2d7076047..3067a735e 100644
--- a/zkfold-uplc/src/ZkFold/Symbolic/UPLC/Data.hs
+++ b/zkfold-uplc/src/ZkFold/Symbolic/UPLC/Data.hs
@@ -7,13 +7,13 @@
 
 module ZkFold.Symbolic.UPLC.Data where
 
-import           GHC.Generics               (Par1)
+import           GHC.Generics                     (Par1)
 
-import           ZkFold.Symbolic.Class      (Symbolic)
-import           ZkFold.Symbolic.Data.Bool (Bool)
-import           ZkFold.Symbolic.Data.Class (SymbolicData (..))
+import           ZkFold.Symbolic.Class            (Symbolic)
+import           ZkFold.Symbolic.Data.Bool        (Bool)
+import           ZkFold.Symbolic.Data.Class       (SymbolicData (..))
 import           ZkFold.Symbolic.Data.Conditional (Conditional)
-import           ZkFold.Symbolic.Data.Input (SymbolicInput)
+import           ZkFold.Symbolic.Data.Input       (SymbolicInput)
 
 -- | Plutus Core's Data as a Symbolic datatype.
 -- TODO: Proper symbolic Data type

From 6f481b45b8064668f265819678f9558191a993c3 Mon Sep 17 00:00:00 2001
From: Eitan Chatav <eitan.chatav@gmail.com>
Date: Tue, 10 Dec 2024 17:36:29 -0800
Subject: [PATCH 09/12] Update KZG.hs

---
 symbolic-base/src/ZkFold/Base/Protocol/KZG.hs | 1 -
 1 file changed, 1 deletion(-)

diff --git a/symbolic-base/src/ZkFold/Base/Protocol/KZG.hs b/symbolic-base/src/ZkFold/Base/Protocol/KZG.hs
index eeb1017e8..0bae1ade6 100644
--- a/symbolic-base/src/ZkFold/Base/Protocol/KZG.hs
+++ b/symbolic-base/src/ZkFold/Base/Protocol/KZG.hs
@@ -54,7 +54,6 @@ instance forall (c1 :: Type) (c2 :: Type) d kzg f g1 core.
     , Binary (Point c1)
     , Pairing c1 c2
     , CoreFunction c1 core
-    , Eq (TargetGroup c1 c2)
     ) => NonInteractiveProof (KZG c1 c2 d) core where
     type Transcript (KZG c1 c2 d)  = ByteString
     type SetupProve (KZG c1 c2 d)  = V.Vector (Point c1)

From dc3f6486adf8f043bee9c2e1ddee812f2f5788af Mon Sep 17 00:00:00 2001
From: Eitan Chatav <eitan.chatav@gmail.com>
Date: Tue, 10 Dec 2024 17:55:44 -0800
Subject: [PATCH 10/12] fix

---
 symbolic-base/bench/BenchEC.hs                                | 4 ++--
 zkfold-ledger/src/ZkFold/Symbolic/Ledger/Validation/Update.hs | 2 --
 2 files changed, 2 insertions(+), 4 deletions(-)

diff --git a/symbolic-base/bench/BenchEC.hs b/symbolic-base/bench/BenchEC.hs
index 85f4d1935..d080af601 100644
--- a/symbolic-base/bench/BenchEC.hs
+++ b/symbolic-base/bench/BenchEC.hs
@@ -16,13 +16,13 @@ import           ZkFold.Base.Algebra.EllipticCurve.BLS12_381
 import           ZkFold.Base.Algebra.EllipticCurve.Class
 import           ZkFold.Base.Algebra.EllipticCurve.Ed25519
 import           ZkFold.Symbolic.Compiler.ArithmeticCircuit
-import           ZkFold.Symbolic.Data.Ed25519                ()
+import           ZkFold.Symbolic.Data.Ed25519
 import           ZkFold.Symbolic.Data.FFA
 import           ZkFold.Symbolic.Interpreter
 
 type I = Interpreter (Zp BLS12_381_Scalar)
 type A = ArithmeticCircuit (Zp BLS12_381_Scalar) U1 U1
-type PtFFA c = Point (Ed25519 c)
+type PtFFA c = Point (AcEd25519 c)
 
 benchOps :: NFData a => String -> a -> (Natural-> a -> a) -> Benchmark
 benchOps desc p0 op = env (fromIntegral <$> randomRIO (1 :: Integer, 3)) $ \ ~n ->
diff --git a/zkfold-ledger/src/ZkFold/Symbolic/Ledger/Validation/Update.hs b/zkfold-ledger/src/ZkFold/Symbolic/Ledger/Validation/Update.hs
index 4ebd4120d..f636c8ab8 100644
--- a/zkfold-ledger/src/ZkFold/Symbolic/Ledger/Validation/Update.hs
+++ b/zkfold-ledger/src/ZkFold/Symbolic/Ledger/Validation/Update.hs
@@ -80,12 +80,10 @@ updateIsValid ::
   => SymbolicOutput (Output context)
   => SymbolicOutput (ContractData context)
   => SymbolicOutput (Value context)
-  => SymbolicData (MultiAssetValue context)
   => Context (AddressIndex context) ~ context
   => Context (Output context) ~ context
   => Context (ContractData context) ~ context
   => Context (Value context) ~ context
-  => Context (MultiAssetValue context) ~ context
   => Eq (Bool context) (MultiAssetValue context)
   => Conditional (Bool context) (MultiAssetValue context)
   => Hash context

From 88ed54b71ca7b53b3f51e097581904e12aa705c0 Mon Sep 17 00:00:00 2001
From: Eitan Chatav <eitan.chatav@gmail.com>
Date: Tue, 10 Dec 2024 17:59:32 -0800
Subject: [PATCH 11/12] Update BLS12_381.hs

---
 .../src/ZkFold/Base/Algebra/EllipticCurve/BLS12_381.hs   | 9 +++------
 1 file changed, 3 insertions(+), 6 deletions(-)

diff --git a/symbolic-base/src/ZkFold/Base/Algebra/EllipticCurve/BLS12_381.hs b/symbolic-base/src/ZkFold/Base/Algebra/EllipticCurve/BLS12_381.hs
index 13da9a879..16303a74c 100644
--- a/symbolic-base/src/ZkFold/Base/Algebra/EllipticCurve/BLS12_381.hs
+++ b/symbolic-base/src/ZkFold/Base/Algebra/EllipticCurve/BLS12_381.hs
@@ -157,8 +157,7 @@ instance Binary (Point BLS12_381_G1) where
 
 instance Binary (PointCompressed BLS12_381_G1) where
     put (PointCompressed x bigY isInf) =
-        if isInf then foldMap putWord8 (bitReverse8 (bit 0 .|. bit 1) : replicate 47 0)
-        else
+        if isInf then foldMap putWord8 (bitReverse8 (bit 0 .|. bit 1) : replicate 47 0) else
         let
             flags = bitReverse8 $ if bigY then bit 0 .|. bit 2 else bit 0
             bytes = bytesOf 48 x
@@ -184,8 +183,7 @@ instance Binary (PointCompressed BLS12_381_G1) where
 
 instance Binary (Point BLS12_381_G2) where
     put (Point (Ext2 x0 x1) (Ext2 y0 y1) isInf) =
-        if isInf then foldMap putWord8 (bitReverse8 (bit 1) : replicate 191  0)
-        else
+        if isInf then foldMap putWord8 (bitReverse8 (bit 1) : replicate 191  0) else
         let
             bytes = bytesOf 48 x1
               <> bytesOf 48 x0
@@ -217,8 +215,7 @@ instance Binary (Point BLS12_381_G2) where
 
 instance Binary (PointCompressed BLS12_381_G2) where
     put (PointCompressed (Ext2 x0 x1) bigY isInf) =
-        if isInf then foldMap putWord8 (bitReverse8 (bit 0 .|. bit 1) : replicate 95 0)
-        else
+        if isInf then foldMap putWord8 (bitReverse8 (bit 0 .|. bit 1) : replicate 95 0) else
         let
             flags = bitReverse8 $ if bigY then bit 0 .|. bit 2 else bit 0
             bytes = bytesOf 48 x1 <> bytesOf 48 x0

From 8b0d6a5f82376b7e31e1d745873b8ebb91b9ff8c Mon Sep 17 00:00:00 2001
From: Eitan Chatav <eitan.chatav@gmail.com>
Date: Tue, 10 Dec 2024 18:05:37 -0800
Subject: [PATCH 12/12] Update Class.hs

---
 symbolic-base/src/ZkFold/Base/Algebra/EllipticCurve/Class.hs | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/symbolic-base/src/ZkFold/Base/Algebra/EllipticCurve/Class.hs b/symbolic-base/src/ZkFold/Base/Algebra/EllipticCurve/Class.hs
index 27e4ed160..6c1eef765 100644
--- a/symbolic-base/src/ZkFold/Base/Algebra/EllipticCurve/Class.hs
+++ b/symbolic-base/src/ZkFold/Base/Algebra/EllipticCurve/Class.hs
@@ -259,8 +259,7 @@ decompress
      )
   => PointCompressed curve -> Point curve
 decompress (PointCompressed x bigY isInf) =
-  if isInf then inf
-  else
+  if isInf then inf else
     let a = aParameter @curve
         b = bParameter @curve
         p = order @(BaseField curve)