From ca2296d0347410bc63934ea8c50e1ecfbd1475f6 Mon Sep 17 00:00:00 2001
From: Eitan Chatav <eitan.chatav@gmail.com>
Date: Tue, 26 Nov 2024 12:46:05 -0800
Subject: [PATCH 01/13] Update Eq.hs

---
 symbolic-base/src/ZkFold/Symbolic/Data/Eq.hs | 26 +++++++++++++++++++-
 1 file changed, 25 insertions(+), 1 deletion(-)

diff --git a/symbolic-base/src/ZkFold/Symbolic/Data/Eq.hs b/symbolic-base/src/ZkFold/Symbolic/Data/Eq.hs
index 3be573540..86da3debf 100644
--- a/symbolic-base/src/ZkFold/Symbolic/Data/Eq.hs
+++ b/symbolic-base/src/ZkFold/Symbolic/Data/Eq.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE TypeOperators, UndecidableInstances #-}
 
 module ZkFold.Symbolic.Data.Eq (
     Eq(..),
@@ -9,6 +9,7 @@ import           Data.Bool                        (bool)
 import           Data.Foldable                    (Foldable)
 import           Data.Functor.Rep                 (Representable, mzipRep, mzipWithRep)
 import           Data.Traversable                 (Traversable, for)
+import qualified GHC.Generics                  as G
 import           Prelude                          (return, ($))
 import qualified Prelude                          as Haskell
 
@@ -22,9 +23,13 @@ import           ZkFold.Symbolic.MonadCircuit
 class Eq b a where
     infix 4 ==
     (==) :: a -> a -> b
+    default (==) :: (G.Generic a, GEq b (G.Rep a)) => a -> a -> b
+    x == y = geq (G.from x) (G.from y)
 
     infix 4 /=
     (/=) :: a -> a -> b
+    default (/=) :: (G.Generic a, GEq b (G.Rep a)) => a -> a -> b
+    x /= y = gneq (G.from x) (G.from y)
 
 elem :: (BoolType b, Eq b a, Foldable t) => a -> t a -> b
 elem x = any (== x)
@@ -62,3 +67,22 @@ instance (Symbolic c, Haskell.Eq (BaseField c), Representable f, Traversable f)
         in
             any Bool (unpacked result)
 
+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)
+
+class GEq b u where
+    geq :: u x -> u x -> b
+    gneq :: u x -> u x -> b
+
+instance (BoolType b, GEq b u, GEq b v) => GEq b (u G.:*: v) where
+    geq (x0 G.:*: x1) (y0 G.:*: y1) = geq x0 y0 && geq x1 y1
+    gneq (x0 G.:*: x1) (y0 G.:*: y1) = gneq x0 y0 || gneq x1 y1
+
+instance GEq b v => GEq b (G.M1 i c v) where
+    geq (G.M1 x) (G.M1 y) = geq x y
+    gneq (G.M1 x) (G.M1 y) = gneq x y
+
+instance Eq b x => GEq b (G.Rec0 x) where
+    geq (G.K1 x) (G.K1 y) = x == y
+    gneq (G.K1 x) (G.K1 y) = x /= y

From dab531ccbbc85ad68bbb8f80aee739b423f2e677 Mon Sep 17 00:00:00 2001
From: Eitan Chatav <eitan.chatav@gmail.com>
Date: Tue, 26 Nov 2024 13:30:01 -0800
Subject: [PATCH 02/13] Update Eq.hs

---
 symbolic-base/src/ZkFold/Symbolic/Data/Eq.hs | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/symbolic-base/src/ZkFold/Symbolic/Data/Eq.hs b/symbolic-base/src/ZkFold/Symbolic/Data/Eq.hs
index 86da3debf..e684301dc 100644
--- a/symbolic-base/src/ZkFold/Symbolic/Data/Eq.hs
+++ b/symbolic-base/src/ZkFold/Symbolic/Data/Eq.hs
@@ -2,7 +2,8 @@
 
 module ZkFold.Symbolic.Data.Eq (
     Eq(..),
-    elem
+    elem,
+    GEq (..)
 ) where
 
 import           Data.Bool                        (bool)

From 2df8585968f796cdc20e425f102ed151131a110c Mon Sep 17 00:00:00 2001
From: echatav <echatav@users.noreply.github.com>
Date: Tue, 26 Nov 2024 21:47:06 +0000
Subject: [PATCH 03/13] stylish-haskell auto-commit

---
 symbolic-base/src/ZkFold/Symbolic/Data/Eq.hs | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/symbolic-base/src/ZkFold/Symbolic/Data/Eq.hs b/symbolic-base/src/ZkFold/Symbolic/Data/Eq.hs
index e684301dc..93d567837 100644
--- a/symbolic-base/src/ZkFold/Symbolic/Data/Eq.hs
+++ b/symbolic-base/src/ZkFold/Symbolic/Data/Eq.hs
@@ -1,4 +1,5 @@
-{-# LANGUAGE TypeOperators, UndecidableInstances #-}
+{-# LANGUAGE TypeOperators        #-}
+{-# LANGUAGE UndecidableInstances #-}
 
 module ZkFold.Symbolic.Data.Eq (
     Eq(..),
@@ -10,7 +11,7 @@ import           Data.Bool                        (bool)
 import           Data.Foldable                    (Foldable)
 import           Data.Functor.Rep                 (Representable, mzipRep, mzipWithRep)
 import           Data.Traversable                 (Traversable, for)
-import qualified GHC.Generics                  as G
+import qualified GHC.Generics                     as G
 import           Prelude                          (return, ($))
 import qualified Prelude                          as Haskell
 

From 2373d8e693dfcea75b4efd3ee43b4add2e29ea48 Mon Sep 17 00:00:00 2001
From: Eitan Chatav <eitan.chatav@gmail.com>
Date: Wed, 27 Nov 2024 07:09:13 -0800
Subject: [PATCH 04/13] Eq (Bool c) (Bool c)

---
 symbolic-base/src/ZkFold/Symbolic/Data/Eq.hs | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/symbolic-base/src/ZkFold/Symbolic/Data/Eq.hs b/symbolic-base/src/ZkFold/Symbolic/Data/Eq.hs
index 93d567837..df68150da 100644
--- a/symbolic-base/src/ZkFold/Symbolic/Data/Eq.hs
+++ b/symbolic-base/src/ZkFold/Symbolic/Data/Eq.hs
@@ -1,3 +1,4 @@
+{-# LANGUAGE DerivingStrategies   #-}
 {-# LANGUAGE TypeOperators        #-}
 {-# LANGUAGE UndecidableInstances #-}
 
@@ -69,6 +70,8 @@ instance (Symbolic c, Haskell.Eq (BaseField c), Representable f, Traversable f)
         in
             any Bool (unpacked result)
 
+deriving newtype instance Symbolic c => Eq (Bool c) (Bool c)
+
 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)

From b59337119a9cdc7cd664dadcefeac7082dc42e01 Mon Sep 17 00:00:00 2001
From: Eitan Chatav <eitan.chatav@gmail.com>
Date: Wed, 27 Nov 2024 08:09:52 -0800
Subject: [PATCH 05/13] Update Eq.hs

---
 symbolic-base/src/ZkFold/Symbolic/Data/Eq.hs | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/symbolic-base/src/ZkFold/Symbolic/Data/Eq.hs b/symbolic-base/src/ZkFold/Symbolic/Data/Eq.hs
index df68150da..444a718d5 100644
--- a/symbolic-base/src/ZkFold/Symbolic/Data/Eq.hs
+++ b/symbolic-base/src/ZkFold/Symbolic/Data/Eq.hs
@@ -1,4 +1,3 @@
-{-# LANGUAGE DerivingStrategies   #-}
 {-# LANGUAGE TypeOperators        #-}
 {-# LANGUAGE UndecidableInstances #-}
 
@@ -70,7 +69,7 @@ instance (Symbolic c, Haskell.Eq (BaseField c), Representable f, Traversable f)
         in
             any Bool (unpacked result)
 
-deriving newtype instance Symbolic c => Eq (Bool c) (Bool c)
+instance Symbolic c => Eq (Bool c) (Bool c)
 
 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)

From 3ce130558d62f564ff948bd269861fecda8c3079 Mon Sep 17 00:00:00 2001
From: TurtlePU <sokolov.p64@gmail.com>
Date: Sun, 1 Dec 2024 01:45:50 +0300
Subject: [PATCH 06/13] + some minimal tests

---
 symbolic-base/symbolic-base.cabal |  1 +
 symbolic-base/test/Main.hs        |  2 ++
 symbolic-base/test/Tests/List.hs  | 41 +++++++++++++++++++++++++++++++
 3 files changed, 44 insertions(+)
 create mode 100644 symbolic-base/test/Tests/List.hs

diff --git a/symbolic-base/symbolic-base.cabal b/symbolic-base/symbolic-base.cabal
index 71712e49b..305f90ce3 100644
--- a/symbolic-base/symbolic-base.cabal
+++ b/symbolic-base/symbolic-base.cabal
@@ -254,6 +254,7 @@ test-suite symbolic-base-test
       Tests.Field
       Tests.GroebnerBasis
       Tests.Group
+      Tests.List
       Tests.NonInteractiveProof
       Tests.Pairing
       Tests.Permutations
diff --git a/symbolic-base/test/Main.hs b/symbolic-base/test/Main.hs
index dc8d99243..6b5176378 100644
--- a/symbolic-base/test/Main.hs
+++ b/symbolic-base/test/Main.hs
@@ -20,6 +20,7 @@ import           Tests.RSA                 (specRSA)
 import           Tests.SHA2                (specSHA2, specSHA2Natural)
 import           Tests.UInt                (specUInt)
 import           Tests.Univariate          (specUnivariate)
+import Tests.List (specList)
 
 main :: IO ()
 main = do
@@ -38,6 +39,7 @@ main = do
     specCompiler
 
     -- Symbolic types and operations
+    specList
     specUInt
     specFFA
     specByteString
diff --git a/symbolic-base/test/Tests/List.hs b/symbolic-base/test/Tests/List.hs
new file mode 100644
index 000000000..884b11bb5
--- /dev/null
+++ b/symbolic-base/test/Tests/List.hs
@@ -0,0 +1,41 @@
+{-# LANGUAGE AllowAmbiguousTypes #-}
+
+module Tests.List (specList) where
+
+import           Data.Binary                                 (Binary)
+import qualified Data.Eq                                     as Haskell
+import           Data.Function                               (($))
+import           GHC.Generics                                (Par1 (..), U1 (..), type (:*:) (..))
+import           System.IO                                   (IO)
+import           Test.Hspec                                  (describe, hspec)
+import           Test.Hspec.QuickCheck                       (prop)
+import           Test.QuickCheck                             (Arbitrary)
+import           Text.Show                                   (Show)
+
+import           ZkFold.Base.Algebra.Basic.Class             (one)
+import           ZkFold.Base.Algebra.Basic.Field             (Zp)
+import           ZkFold.Base.Algebra.EllipticCurve.BLS12_381 (BLS12_381_Scalar)
+import           ZkFold.Symbolic.Class                       (Arithmetic, Symbolic)
+import           ZkFold.Symbolic.Compiler                    (compile, eval1)
+import           ZkFold.Symbolic.Data.Bool                   (Bool)
+import           ZkFold.Symbolic.Data.Eq                     ((==))
+import           ZkFold.Symbolic.Data.FieldElement           (FieldElement)
+import           ZkFold.Symbolic.Data.List                   (emptyList, head, tail, (.:))
+
+headTest :: Symbolic c => FieldElement c -> FieldElement c -> Bool c
+headTest x y = head (x .: y .: emptyList) == x
+
+tailTest :: Symbolic c => FieldElement c -> FieldElement c -> Bool c
+tailTest x y = head (tail (x .: y .: emptyList)) == y
+
+specList' :: forall a. (Arbitrary a, Arithmetic a, Binary a, Show a) => IO ()
+specList' = hspec $ describe "List spec" $ do
+  prop "Head works fine" $ \x y ->
+    eval1 (compile @a headTest) (U1 :*: U1 :*: U1) (Par1 x :*: Par1 y :*: U1)
+      Haskell.== one
+  prop "Tail works fine" $ \x y ->
+    eval1 (compile @a tailTest) (U1 :*: U1 :*: U1) (Par1 x :*: Par1 y :*: U1)
+      Haskell.== one
+
+specList :: IO ()
+specList = specList' @(Zp BLS12_381_Scalar)

From b27551dbc6f507dcc20af87b15708cab81f53287 Mon Sep 17 00:00:00 2001
From: TurtlePU <TurtlePU@users.noreply.github.com>
Date: Sat, 30 Nov 2024 22:49:36 +0000
Subject: [PATCH 07/13] stylish-haskell auto-commit

---
 symbolic-base/test/Main.hs | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/symbolic-base/test/Main.hs b/symbolic-base/test/Main.hs
index 6b5176378..bade3bed4 100644
--- a/symbolic-base/test/Main.hs
+++ b/symbolic-base/test/Main.hs
@@ -11,6 +11,7 @@ import           Tests.FFA                 (specFFA)
 import           Tests.Field               (specField)
 import           Tests.GroebnerBasis       (specGroebner)
 import           Tests.Group               (specAdditiveGroup)
+import           Tests.List                (specList)
 import           Tests.NonInteractiveProof (specNonInteractiveProof)
 import           Tests.Pairing             (specPairing)
 import           Tests.Permutations        (specPermutations)
@@ -20,7 +21,6 @@ import           Tests.RSA                 (specRSA)
 import           Tests.SHA2                (specSHA2, specSHA2Natural)
 import           Tests.UInt                (specUInt)
 import           Tests.Univariate          (specUnivariate)
-import Tests.List (specList)
 
 main :: IO ()
 main = do

From 60c0b2d5d3799d9fac4d3be17c662785e0bc8f33 Mon Sep 17 00:00:00 2001
From: Eitan Chatav <eitan.chatav@gmail.com>
Date: Sun, 1 Dec 2024 10:13:12 -0800
Subject: [PATCH 08/13] remove Structural

---
 .../src/ZkFold/Symbolic/Data/Eq/Structural.hs | 36 -------------------
 symbolic-base/symbolic-base.cabal             |  1 -
 2 files changed, 37 deletions(-)
 delete mode 100644 symbolic-base/src/ZkFold/Symbolic/Data/Eq/Structural.hs

diff --git a/symbolic-base/src/ZkFold/Symbolic/Data/Eq/Structural.hs b/symbolic-base/src/ZkFold/Symbolic/Data/Eq/Structural.hs
deleted file mode 100644
index f68752554..000000000
--- a/symbolic-base/src/ZkFold/Symbolic/Data/Eq/Structural.hs
+++ /dev/null
@@ -1,36 +0,0 @@
-{-# LANGUAGE TypeOperators        #-}
-{-# LANGUAGE UndecidableInstances #-}
-
-module ZkFold.Symbolic.Data.Eq.Structural where
-
-import           Data.Functor.Rep           (Representable)
-import           Data.Proxy                 (Proxy (..))
-import           Data.Traversable           (Traversable)
-import           Prelude                    (type (~))
-
-import           ZkFold.Symbolic.Class
-import           ZkFold.Symbolic.Data.Bool
-import           ZkFold.Symbolic.Data.Class
-import           ZkFold.Symbolic.Data.Eq
-
-newtype Structural a = Structural a
--- ^ A newtype wrapper for easy definition of Eq instances.
-
-instance
-    ( SymbolicData x
-    , Context x ~ c
-    , Support x ~ Proxy c
-    , Symbolic c
-    , Representable (Layout x)
-    , Traversable (Layout x)
-    ) => Eq (Bool c) (Structural x) where
-
-    Structural x == Structural y =
-        let x' = arithmetize x Proxy
-            y' = arithmetize y Proxy
-         in x' == y'
-
-    Structural x /= Structural y =
-        let x' = arithmetize x Proxy
-            y' = arithmetize y Proxy
-         in x' /= y'
diff --git a/symbolic-base/symbolic-base.cabal b/symbolic-base/symbolic-base.cabal
index f98882049..a2b0e0c57 100644
--- a/symbolic-base/symbolic-base.cabal
+++ b/symbolic-base/symbolic-base.cabal
@@ -184,7 +184,6 @@ library
       ZkFold.Symbolic.Data.DiscreteField
       ZkFold.Symbolic.Data.Ed25519
       ZkFold.Symbolic.Data.Eq
-      ZkFold.Symbolic.Data.Eq.Structural
       ZkFold.Symbolic.Data.FFA
       ZkFold.Symbolic.Data.Input
       ZkFold.Symbolic.Data.List

From ee05b9b0014c51580a224cc617e8eeeef748ceff Mon Sep 17 00:00:00 2001
From: Eitan Chatav <eitan.chatav@gmail.com>
Date: Sun, 1 Dec 2024 10:13:23 -0800
Subject: [PATCH 09/13] Eq Vector

---
 symbolic-base/src/ZkFold/Symbolic/Data/Eq.hs | 9 ++++++++-
 1 file changed, 8 insertions(+), 1 deletion(-)

diff --git a/symbolic-base/src/ZkFold/Symbolic/Data/Eq.hs b/symbolic-base/src/ZkFold/Symbolic/Data/Eq.hs
index 444a718d5..40f68e2a8 100644
--- a/symbolic-base/src/ZkFold/Symbolic/Data/Eq.hs
+++ b/symbolic-base/src/ZkFold/Symbolic/Data/Eq.hs
@@ -1,3 +1,4 @@
+{-# LANGUAGE DerivingStrategies   #-}
 {-# LANGUAGE TypeOperators        #-}
 {-# LANGUAGE UndecidableInstances #-}
 
@@ -11,12 +12,14 @@ import           Data.Bool                        (bool)
 import           Data.Foldable                    (Foldable)
 import           Data.Functor.Rep                 (Representable, mzipRep, mzipWithRep)
 import           Data.Traversable                 (Traversable, for)
+import qualified Data.Vector                      as V
 import qualified GHC.Generics                     as G
 import           Prelude                          (return, ($))
 import qualified Prelude                          as Haskell
 
 import           ZkFold.Base.Algebra.Basic.Class
 import           ZkFold.Base.Data.Package
+import           ZkFold.Base.Data.Vector
 import           ZkFold.Symbolic.Class
 import           ZkFold.Symbolic.Data.Bool        (Bool (Bool), BoolType (..), all, any)
 import           ZkFold.Symbolic.Data.Combinators (runInvert)
@@ -69,7 +72,11 @@ instance (Symbolic c, Haskell.Eq (BaseField c), Representable f, Traversable f)
         in
             any Bool (unpacked result)
 
-instance Symbolic c => Eq (Bool c) (Bool c)
+instance (BoolType b, Eq b x) => Eq b (Vector n x) where
+    u == v = V.foldl (&&) true (V.zipWith (==) (toV u) (toV v))
+    u /= v = V.foldl (||) false (V.zipWith (/=) (toV u) (toV v))
+
+deriving newtype instance Symbolic c => Eq (Bool c) (Bool c)
 
 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)

From df06607f649302292d566e239e814719bc60f405 Mon Sep 17 00:00:00 2001
From: Eitan Chatav <eitan.chatav@gmail.com>
Date: Sun, 1 Dec 2024 10:13:36 -0800
Subject: [PATCH 10/13] instance fixes

---
 symbolic-base/src/ZkFold/Symbolic/Data/ByteString.hs       | 3 +--
 symbolic-base/src/ZkFold/Symbolic/Data/UInt.hs             | 3 +--
 .../src/ZkFold/Symbolic/Cardano/Types/Address.hs           | 4 +---
 .../src/ZkFold/Symbolic/Cardano/Types/Output.hs            | 4 +---
 .../src/ZkFold/Symbolic/Cardano/Types/Value.hs             | 7 +++++++
 5 files changed, 11 insertions(+), 10 deletions(-)

diff --git a/symbolic-base/src/ZkFold/Symbolic/Data/ByteString.hs b/symbolic-base/src/ZkFold/Symbolic/Data/ByteString.hs
index 578ac9143..7468477f1 100644
--- a/symbolic-base/src/ZkFold/Symbolic/Data/ByteString.hs
+++ b/symbolic-base/src/ZkFold/Symbolic/Data/ByteString.hs
@@ -56,7 +56,6 @@ import           ZkFold.Symbolic.Data.Bool          (Bool (..), BoolType (..))
 import           ZkFold.Symbolic.Data.Class         (SymbolicData)
 import           ZkFold.Symbolic.Data.Combinators
 import           ZkFold.Symbolic.Data.Eq            (Eq)
-import           ZkFold.Symbolic.Data.Eq.Structural
 import           ZkFold.Symbolic.Data.FieldElement  (FieldElement)
 import           ZkFold.Symbolic.Data.Input         (SymbolicInput, isValid)
 import           ZkFold.Symbolic.Interpreter        (Interpreter (..))
@@ -74,7 +73,7 @@ deriving anyclass instance NFData (c (Vector n)) => NFData (ByteString n c)
 deriving newtype instance SymbolicData (ByteString n c)
 
 
-deriving via (Structural (ByteString n c))
+deriving newtype
          instance (Symbolic c, KnownNat n) => Eq (Bool c) (ByteString n c)
 
 instance
diff --git a/symbolic-base/src/ZkFold/Symbolic/Data/UInt.hs b/symbolic-base/src/ZkFold/Symbolic/Data/UInt.hs
index ea51af10d..50af93ce0 100644
--- a/symbolic-base/src/ZkFold/Symbolic/Data/UInt.hs
+++ b/symbolic-base/src/ZkFold/Symbolic/Data/UInt.hs
@@ -49,7 +49,6 @@ import           ZkFold.Symbolic.Data.Class         (SymbolicData)
 import           ZkFold.Symbolic.Data.Combinators
 import           ZkFold.Symbolic.Data.Conditional
 import           ZkFold.Symbolic.Data.Eq
-import           ZkFold.Symbolic.Data.Eq.Structural
 import           ZkFold.Symbolic.Data.FieldElement  (FieldElement)
 import           ZkFold.Symbolic.Data.Input         (SymbolicInput, isValid)
 import           ZkFold.Symbolic.Data.Ord
@@ -461,7 +460,7 @@ instance
     , KnownRegisterSize r
     ) => Ring (UInt n r c)
 
-deriving via (Structural (UInt n rs c))
+deriving newtype
          instance (Symbolic c, KnownNat (NumberOfRegisters (BaseField c) n rs)) =>
          Eq (Bool c) (UInt n rs c)
 
diff --git a/symbolic-cardano/src/ZkFold/Symbolic/Cardano/Types/Address.hs b/symbolic-cardano/src/ZkFold/Symbolic/Cardano/Types/Address.hs
index 9a879787a..f68833534 100644
--- a/symbolic-cardano/src/ZkFold/Symbolic/Cardano/Types/Address.hs
+++ b/symbolic-cardano/src/ZkFold/Symbolic/Cardano/Types/Address.hs
@@ -12,7 +12,6 @@ import           ZkFold.Symbolic.Cardano.Types.Basic
 import           ZkFold.Symbolic.Class               (Symbolic)
 import           ZkFold.Symbolic.Data.Class
 import           ZkFold.Symbolic.Data.Eq             (Eq)
-import           ZkFold.Symbolic.Data.Eq.Structural
 import           ZkFold.Symbolic.Data.Input
 
 type AddressType context = ByteString 4 context
@@ -29,8 +28,7 @@ data Address context = Address {
 deriving instance (Haskell.Eq (ByteString 4 context), Haskell.Eq (ByteString 224 context))
     => Haskell.Eq (Address context)
 
-deriving via (Structural (Address context))
-         instance (Symbolic context) => Eq (Bool context) (Address context)
+instance Symbolic context => Eq (Bool context) (Address context)
 
 instance HApplicative context => SymbolicData (Address context)
 instance Symbolic context => SymbolicInput (Address context) where
diff --git a/symbolic-cardano/src/ZkFold/Symbolic/Cardano/Types/Output.hs b/symbolic-cardano/src/ZkFold/Symbolic/Cardano/Types/Output.hs
index 30338f436..e3ec7a11f 100644
--- a/symbolic-cardano/src/ZkFold/Symbolic/Cardano/Types/Output.hs
+++ b/symbolic-cardano/src/ZkFold/Symbolic/Cardano/Types/Output.hs
@@ -22,7 +22,6 @@ import           ZkFold.Symbolic.Class
 import           ZkFold.Symbolic.Data.Class
 import           ZkFold.Symbolic.Data.Combinators           (NumberOfRegisters, RegisterSize (..))
 import           ZkFold.Symbolic.Data.Eq                    (Eq)
-import           ZkFold.Symbolic.Data.Eq.Structural
 import           ZkFold.Symbolic.Data.Input                 (SymbolicInput (..))
 
 data Liability context
@@ -64,8 +63,7 @@ instance
     ) => SymbolicInput (Output tokens datum context) where
     isValid (Output a t d) = isValid (a, t,  d)
 
-deriving via (Structural (Output tokens datum context))
-         instance
+instance
             ( Symbolic context
             , KnownNat tokens
             , KnownNat (NumberOfRegisters (BaseField context) 64 'Auto)
diff --git a/symbolic-cardano/src/ZkFold/Symbolic/Cardano/Types/Value.hs b/symbolic-cardano/src/ZkFold/Symbolic/Cardano/Types/Value.hs
index 048b2b355..fce6bc834 100644
--- a/symbolic-cardano/src/ZkFold/Symbolic/Cardano/Types/Value.hs
+++ b/symbolic-cardano/src/ZkFold/Symbolic/Cardano/Types/Value.hs
@@ -1,3 +1,4 @@
+{-# LANGUAGE DerivingStrategies #-}
 {-# LANGUAGE UndecidableInstances #-}
 {-# OPTIONS_GHC -freduction-depth=0 #-} -- Avoid reduction overflow error caused by NumberOfRegisters
 {-# OPTIONS_GHC -Wno-orphans #-}
@@ -15,6 +16,7 @@ import           ZkFold.Base.Data.Vector
 import           ZkFold.Symbolic.Cardano.Types.Basic
 import           ZkFold.Symbolic.Class               (Symbolic (..))
 import           ZkFold.Symbolic.Data.Class
+import           ZkFold.Symbolic.Data.Eq
 import           ZkFold.Symbolic.Data.Combinators    (NumberOfRegisters, RegisterSize (..))
 import           ZkFold.Symbolic.Data.Input
 
@@ -32,6 +34,11 @@ deriving instance (Haskell.Ord (ByteString 224 context), Haskell.Ord (ByteString
 
 deriving instance (Symbolic context, KnownNat n) => SymbolicData (Value n context)
 
+deriving newtype instance
+  ( Symbolic context
+  , KnownNat (NumberOfRegisters (BaseField context) 64 Auto)
+  ) => Eq (Bool context) (Value n context)
+
 instance
     ( Symbolic context
     , KnownNat n

From a3a7c46e858bfa9a6525dc17da5fe9c66785bd70 Mon Sep 17 00:00:00 2001
From: echatav <echatav@users.noreply.github.com>
Date: Sun, 1 Dec 2024 18:16:40 +0000
Subject: [PATCH 11/13] stylish-haskell auto-commit

---
 .../src/ZkFold/Symbolic/Data/ByteString.hs    | 64 +++++++++----------
 .../src/ZkFold/Symbolic/Data/UInt.hs          | 50 +++++++--------
 .../ZkFold/Symbolic/Cardano/Types/Value.hs    |  4 +-
 3 files changed, 59 insertions(+), 59 deletions(-)

diff --git a/symbolic-base/src/ZkFold/Symbolic/Data/ByteString.hs b/symbolic-base/src/ZkFold/Symbolic/Data/ByteString.hs
index 7468477f1..c803a67c7 100644
--- a/symbolic-base/src/ZkFold/Symbolic/Data/ByteString.hs
+++ b/symbolic-base/src/ZkFold/Symbolic/Data/ByteString.hs
@@ -23,43 +23,43 @@ module ZkFold.Symbolic.Data.ByteString
     , toBsBits
     ) where
 
-import           Control.DeepSeq                    (NFData)
-import           Control.Monad                      (replicateM)
-import           Data.Aeson                         (FromJSON (..), ToJSON (..))
-import qualified Data.Bits                          as B
-import qualified Data.ByteString                    as Bytes
-import           Data.Foldable                      (foldlM)
-import           Data.Kind                          (Type)
-import           Data.List                          (reverse, unfoldr)
-import           Data.Maybe                         (Maybe (..))
-import           Data.String                        (IsString (..))
-import           Data.Traversable                   (for, mapM)
-import           GHC.Generics                       (Generic, Par1 (..))
-import           GHC.Natural                        (naturalFromInteger)
-import           Numeric                            (readHex, showHex)
-import           Prelude                            (Integer, const, drop, fmap, otherwise, pure, return, take,
-                                                     type (~), ($), (.), (<$>), (<), (<>), (==), (>=))
-import qualified Prelude                            as Haskell
-import           Test.QuickCheck                    (Arbitrary (..), chooseInteger)
+import           Control.DeepSeq                   (NFData)
+import           Control.Monad                     (replicateM)
+import           Data.Aeson                        (FromJSON (..), ToJSON (..))
+import qualified Data.Bits                         as B
+import qualified Data.ByteString                   as Bytes
+import           Data.Foldable                     (foldlM)
+import           Data.Kind                         (Type)
+import           Data.List                         (reverse, unfoldr)
+import           Data.Maybe                        (Maybe (..))
+import           Data.String                       (IsString (..))
+import           Data.Traversable                  (for, mapM)
+import           GHC.Generics                      (Generic, Par1 (..))
+import           GHC.Natural                       (naturalFromInteger)
+import           Numeric                           (readHex, showHex)
+import           Prelude                           (Integer, const, drop, fmap, otherwise, pure, return, take, type (~),
+                                                    ($), (.), (<$>), (<), (<>), (==), (>=))
+import qualified Prelude                           as Haskell
+import           Test.QuickCheck                   (Arbitrary (..), chooseInteger)
 
 import           ZkFold.Base.Algebra.Basic.Class
-import           ZkFold.Base.Algebra.Basic.Field    (Zp)
+import           ZkFold.Base.Algebra.Basic.Field   (Zp)
 import           ZkFold.Base.Algebra.Basic.Number
-import           ZkFold.Base.Data.HFunctor          (HFunctor (..))
-import           ZkFold.Base.Data.Package           (packWith, unpackWith)
-import           ZkFold.Base.Data.Utils             (zipWithM)
-import qualified ZkFold.Base.Data.Vector            as V
-import           ZkFold.Base.Data.Vector            (Vector (..))
-import           ZkFold.Prelude                     (replicateA, (!!))
+import           ZkFold.Base.Data.HFunctor         (HFunctor (..))
+import           ZkFold.Base.Data.Package          (packWith, unpackWith)
+import           ZkFold.Base.Data.Utils            (zipWithM)
+import qualified ZkFold.Base.Data.Vector           as V
+import           ZkFold.Base.Data.Vector           (Vector (..))
+import           ZkFold.Prelude                    (replicateA, (!!))
 import           ZkFold.Symbolic.Class
-import           ZkFold.Symbolic.Data.Bool          (Bool (..), BoolType (..))
-import           ZkFold.Symbolic.Data.Class         (SymbolicData)
+import           ZkFold.Symbolic.Data.Bool         (Bool (..), BoolType (..))
+import           ZkFold.Symbolic.Data.Class        (SymbolicData)
 import           ZkFold.Symbolic.Data.Combinators
-import           ZkFold.Symbolic.Data.Eq            (Eq)
-import           ZkFold.Symbolic.Data.FieldElement  (FieldElement)
-import           ZkFold.Symbolic.Data.Input         (SymbolicInput, isValid)
-import           ZkFold.Symbolic.Interpreter        (Interpreter (..))
-import           ZkFold.Symbolic.MonadCircuit       (ClosedPoly, newAssigned)
+import           ZkFold.Symbolic.Data.Eq           (Eq)
+import           ZkFold.Symbolic.Data.FieldElement (FieldElement)
+import           ZkFold.Symbolic.Data.Input        (SymbolicInput, isValid)
+import           ZkFold.Symbolic.Interpreter       (Interpreter (..))
+import           ZkFold.Symbolic.MonadCircuit      (ClosedPoly, newAssigned)
 
 -- | A ByteString which stores @n@ bits and uses elements of @a@ as registers, one element per register.
 -- Bit layout is Big-endian.
diff --git a/symbolic-base/src/ZkFold/Symbolic/Data/UInt.hs b/symbolic-base/src/ZkFold/Symbolic/Data/UInt.hs
index 50af93ce0..024afa00f 100644
--- a/symbolic-base/src/ZkFold/Symbolic/Data/UInt.hs
+++ b/symbolic-base/src/ZkFold/Symbolic/Data/UInt.hs
@@ -19,41 +19,41 @@ module ZkFold.Symbolic.Data.UInt (
 ) where
 
 import           Control.DeepSeq
-import           Control.Monad.State                (StateT (..))
-import           Data.Aeson                         hiding (Bool)
-import           Data.Foldable                      (foldlM, foldr, foldrM, for_)
-import           Data.Functor                       ((<$>))
-import           Data.Kind                          (Type)
-import           Data.List                          (unfoldr, zip)
-import           Data.Map                           (fromList, (!))
-import           Data.Traversable                   (for, traverse)
-import           Data.Tuple                         (swap)
-import qualified Data.Zip                           as Z
-import           GHC.Generics                       (Generic, Par1 (..))
-import           GHC.Natural                        (naturalFromInteger)
-import           Prelude                            (Integer, const, error, flip, otherwise, return, type (~), ($),
-                                                     (++), (.), (<>), (>>=))
-import qualified Prelude                            as Haskell
-import           Test.QuickCheck                    (Arbitrary (..), chooseInteger)
+import           Control.Monad.State               (StateT (..))
+import           Data.Aeson                        hiding (Bool)
+import           Data.Foldable                     (foldlM, foldr, foldrM, for_)
+import           Data.Functor                      ((<$>))
+import           Data.Kind                         (Type)
+import           Data.List                         (unfoldr, zip)
+import           Data.Map                          (fromList, (!))
+import           Data.Traversable                  (for, traverse)
+import           Data.Tuple                        (swap)
+import qualified Data.Zip                          as Z
+import           GHC.Generics                      (Generic, Par1 (..))
+import           GHC.Natural                       (naturalFromInteger)
+import           Prelude                           (Integer, const, error, flip, otherwise, return, type (~), ($), (++),
+                                                    (.), (<>), (>>=))
+import qualified Prelude                           as Haskell
+import           Test.QuickCheck                   (Arbitrary (..), chooseInteger)
 
 import           ZkFold.Base.Algebra.Basic.Class
-import           ZkFold.Base.Algebra.Basic.Field    (Zp)
+import           ZkFold.Base.Algebra.Basic.Field   (Zp)
 import           ZkFold.Base.Algebra.Basic.Number
-import qualified ZkFold.Base.Data.Vector            as V
-import           ZkFold.Base.Data.Vector            (Vector (..))
-import           ZkFold.Prelude                     (length, replicate, replicateA)
+import qualified ZkFold.Base.Data.Vector           as V
+import           ZkFold.Base.Data.Vector           (Vector (..))
+import           ZkFold.Prelude                    (length, replicate, replicateA)
 import           ZkFold.Symbolic.Class
 import           ZkFold.Symbolic.Data.Bool
 import           ZkFold.Symbolic.Data.ByteString
-import           ZkFold.Symbolic.Data.Class         (SymbolicData)
+import           ZkFold.Symbolic.Data.Class        (SymbolicData)
 import           ZkFold.Symbolic.Data.Combinators
 import           ZkFold.Symbolic.Data.Conditional
 import           ZkFold.Symbolic.Data.Eq
-import           ZkFold.Symbolic.Data.FieldElement  (FieldElement)
-import           ZkFold.Symbolic.Data.Input         (SymbolicInput, isValid)
+import           ZkFold.Symbolic.Data.FieldElement (FieldElement)
+import           ZkFold.Symbolic.Data.Input        (SymbolicInput, isValid)
 import           ZkFold.Symbolic.Data.Ord
-import           ZkFold.Symbolic.Interpreter        (Interpreter (..))
-import           ZkFold.Symbolic.MonadCircuit       (MonadCircuit, constraint, newAssigned)
+import           ZkFold.Symbolic.Interpreter       (Interpreter (..))
+import           ZkFold.Symbolic.MonadCircuit      (MonadCircuit, constraint, newAssigned)
 
 
 -- TODO (Issue #18): hide this constructor
diff --git a/symbolic-cardano/src/ZkFold/Symbolic/Cardano/Types/Value.hs b/symbolic-cardano/src/ZkFold/Symbolic/Cardano/Types/Value.hs
index fce6bc834..ad160fa46 100644
--- a/symbolic-cardano/src/ZkFold/Symbolic/Cardano/Types/Value.hs
+++ b/symbolic-cardano/src/ZkFold/Symbolic/Cardano/Types/Value.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE DerivingStrategies #-}
+{-# LANGUAGE DerivingStrategies   #-}
 {-# LANGUAGE UndecidableInstances #-}
 {-# OPTIONS_GHC -freduction-depth=0 #-} -- Avoid reduction overflow error caused by NumberOfRegisters
 {-# OPTIONS_GHC -Wno-orphans #-}
@@ -16,8 +16,8 @@ import           ZkFold.Base.Data.Vector
 import           ZkFold.Symbolic.Cardano.Types.Basic
 import           ZkFold.Symbolic.Class               (Symbolic (..))
 import           ZkFold.Symbolic.Data.Class
-import           ZkFold.Symbolic.Data.Eq
 import           ZkFold.Symbolic.Data.Combinators    (NumberOfRegisters, RegisterSize (..))
+import           ZkFold.Symbolic.Data.Eq
 import           ZkFold.Symbolic.Data.Input
 
 type PolicyId context    = ByteString 224 context

From b2a80a4c646b7813acc0147a75e652a55d1f5b79 Mon Sep 17 00:00:00 2001
From: Eitan Chatav <eitan.chatav@gmail.com>
Date: Sun, 1 Dec 2024 10:53:40 -0800
Subject: [PATCH 12/13] fixes

---
 symbolic-cardano/src/ZkFold/Symbolic/Cardano/Types/Value.hs | 2 +-
 zkfold-uplc/src/ZkFold/Symbolic/UPLC/Data.hs                | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/symbolic-cardano/src/ZkFold/Symbolic/Cardano/Types/Value.hs b/symbolic-cardano/src/ZkFold/Symbolic/Cardano/Types/Value.hs
index 2abaf4829..eea2fb3c0 100644
--- a/symbolic-cardano/src/ZkFold/Symbolic/Cardano/Types/Value.hs
+++ b/symbolic-cardano/src/ZkFold/Symbolic/Cardano/Types/Value.hs
@@ -36,7 +36,7 @@ deriving instance (Symbolic context, KnownNat n, KnownRegisters context 64 Auto)
 
 deriving newtype instance
   ( Symbolic context
-  , KnownNat (NumberOfRegisters (BaseField context) 64 Auto)
+  , KnownRegisters context 64 Auto
   ) => Eq (Bool context) (Value n context)
 
 instance
diff --git a/zkfold-uplc/src/ZkFold/Symbolic/UPLC/Data.hs b/zkfold-uplc/src/ZkFold/Symbolic/UPLC/Data.hs
index 9ffcea800..b9690d12e 100644
--- a/zkfold-uplc/src/ZkFold/Symbolic/UPLC/Data.hs
+++ b/zkfold-uplc/src/ZkFold/Symbolic/UPLC/Data.hs
@@ -16,5 +16,5 @@ import           ZkFold.Symbolic.Data.Input (SymbolicInput)
 -- TODO: Proper symbolic Data type
 newtype Data c = Data (c Par1)
 
-deriving newtype instance SymbolicData (Data c)
+deriving newtype instance Symbolic c => SymbolicData (Data c)
 deriving newtype instance Symbolic c => SymbolicInput (Data c)

From 26213dc144aab785b50abad8207ee587e19caff5 Mon Sep 17 00:00:00 2001
From: Eitan Chatav <eitan.chatav@gmail.com>
Date: Sun, 1 Dec 2024 11:51:45 -0800
Subject: [PATCH 13/13] output implications

---
 symbolic-base/src/ZkFold/Symbolic/Compiler.hs  | 3 +--
 symbolic-base/src/ZkFold/Symbolic/Data/List.hs | 2 +-
 symbolic-base/src/ZkFold/Symbolic/Data/Ord.hs  | 2 +-
 3 files changed, 3 insertions(+), 4 deletions(-)

diff --git a/symbolic-base/src/ZkFold/Symbolic/Compiler.hs b/symbolic-base/src/ZkFold/Symbolic/Compiler.hs
index ff3354963..253dc9b49 100644
--- a/symbolic-base/src/ZkFold/Symbolic/Compiler.hs
+++ b/symbolic-base/src/ZkFold/Symbolic/Compiler.hs
@@ -13,7 +13,6 @@ import           Data.Binary                                (Binary)
 import           Data.Function                              (const, id, (.))
 import           Data.Functor.Rep                           (Rep, Representable)
 import           Data.Ord                                   (Ord)
-import           Data.Proxy                                 (Proxy (..))
 import           Data.Tuple                                 (fst, snd)
 import           GHC.Generics                               (Par1 (Par1), U1 (..))
 import           Prelude                                    (FilePath, IO, Show (..), putStrLn, return, type (~), ($),
@@ -47,7 +46,7 @@ type CompilesWith c s f =
 -- | A constraint defining what it means
 -- for data of type @y@ to be properly restorable.
 type RestoresFrom c y =
-  (SymbolicData y, Context y ~ c, Support y ~ Proxy c, Payload y ~ U1)
+  (SymbolicOutput y, Context y ~ c, Payload y ~ U1)
 
 compileInternal ::
   (CompilesWith c0 s f, RestoresFrom c1 y, c1 ~ ArithmeticCircuit a p i) =>
diff --git a/symbolic-base/src/ZkFold/Symbolic/Data/List.hs b/symbolic-base/src/ZkFold/Symbolic/Data/List.hs
index 4abad9843..66252af01 100644
--- a/symbolic-base/src/ZkFold/Symbolic/Data/List.hs
+++ b/symbolic-base/src/ZkFold/Symbolic/Data/List.hs
@@ -128,7 +128,7 @@ uncons List{..} = case lWitness of
 --
 head ::
   SymbolicOutput x =>
-  Support x ~ Proxy c =>
+  Context x ~ c =>
   List c x -> x
 head = fst . uncons
 
diff --git a/symbolic-base/src/ZkFold/Symbolic/Data/Ord.hs b/symbolic-base/src/ZkFold/Symbolic/Data/Ord.hs
index 84a344fec..1613ecd27 100644
--- a/symbolic-base/src/ZkFold/Symbolic/Data/Ord.hs
+++ b/symbolic-base/src/ZkFold/Symbolic/Data/Ord.hs
@@ -84,7 +84,7 @@ instance
 
 getBitsBE ::
   forall c x .
-  (Symbolic c, SymbolicData x, Context x ~ c, Support x ~ Proxy c) =>
+  (SymbolicOutput x, Context x ~ c) =>
   x -> c []
 -- ^ @getBitsBE x@ returns a list of circuits computing bits of @x@, eldest to
 -- youngest.