From d5faca78d69718cc1c6eea5c151f7a33f777880a Mon Sep 17 00:00:00 2001
From: Ann Hovanskaya <hovanja2011@gmail.com>
Date: Wed, 8 Jan 2025 09:52:57 +0300
Subject: [PATCH 01/15] first

---
 .../src/ZkFold/Symbolic/Data/MerkleTree.hs    | 36 +++++++++++++++++++
 symbolic-base/symbolic-base.cabal             |  1 +
 2 files changed, 37 insertions(+)
 create mode 100644 symbolic-base/src/ZkFold/Symbolic/Data/MerkleTree.hs

diff --git a/symbolic-base/src/ZkFold/Symbolic/Data/MerkleTree.hs b/symbolic-base/src/ZkFold/Symbolic/Data/MerkleTree.hs
new file mode 100644
index 00000000..d2b874fe
--- /dev/null
+++ b/symbolic-base/src/ZkFold/Symbolic/Data/MerkleTree.hs
@@ -0,0 +1,36 @@
+{-# LANGUAGE TypeOperators        #-}
+{-# LANGUAGE UndecidableInstances #-}
+
+module ZkFold.Symbolic.Data.MerkleTree where
+
+
+
+import ZkFold.Symbolic.Data.Class
+import GHC.Generics
+import ZkFold.Symbolic.Data.Payloaded (Payloaded)
+import           GHC.TypeNats
+import           Data.Functor.Rep                 (Representable, distributeRep)
+import           Data.Functor                     (Functor)
+import Data.Distributive (Distributive, distribute)
+
+data Leaf l a = Leaf { leafHash    :: l a }
+  deriving (Functor, Generic1)
+
+instance (Representable l) => Representable (Leaf l)
+
+instance (Representable l) => Distributive (Leaf l) where
+  distribute = distributeRep
+
+
+
+data MerkleTree d x = MerkleTree {
+    mHash    :: Context x (Layout x)
+  , mLeft    :: Payloaded (Par1 :*: Leaf (Layout x) :*: MerkleTree (d - 1)) (Context x)
+  , mRight   :: Payloaded (Par1 :*: Leaf (Layout x) :*: MerkleTree (d - 1)) (Context x)
+  }
+  deriving (Generic)
+
+-- instance Functor (MerkleTree d)
+instance Representable (MerkleTree d)
+
+-- instance (SymbolicData x, c ~ Context x) => SymbolicData (MerkleTree d x)
diff --git a/symbolic-base/symbolic-base.cabal b/symbolic-base/symbolic-base.cabal
index 2c7226e1..ff0607b4 100644
--- a/symbolic-base/symbolic-base.cabal
+++ b/symbolic-base/symbolic-base.cabal
@@ -198,6 +198,7 @@ library
       ZkFold.Symbolic.Data.Input
       ZkFold.Symbolic.Data.List
       ZkFold.Symbolic.Data.Maybe
+      ZkFold.Symbolic.Data.MerkleTree
       ZkFold.Symbolic.Data.Ord
       ZkFold.Symbolic.Data.Payloaded
       ZkFold.Symbolic.Data.UInt

From f541282421fcbaa5299b7b7727c3d12d901d8bf2 Mon Sep 17 00:00:00 2001
From: Ann Hovanskaya <hovanja2011@gmail.com>
Date: Wed, 8 Jan 2025 23:46:42 +0300
Subject: [PATCH 02/15] MerkleTree as vector if leaves

---
 .../src/ZkFold/Symbolic/Data/MerkleTree.hs    | 78 ++++++++++++++-----
 1 file changed, 59 insertions(+), 19 deletions(-)

diff --git a/symbolic-base/src/ZkFold/Symbolic/Data/MerkleTree.hs b/symbolic-base/src/ZkFold/Symbolic/Data/MerkleTree.hs
index d2b874fe..6c991368 100644
--- a/symbolic-base/src/ZkFold/Symbolic/Data/MerkleTree.hs
+++ b/symbolic-base/src/ZkFold/Symbolic/Data/MerkleTree.hs
@@ -1,36 +1,76 @@
+{-# LANGUAGE AllowAmbiguousTypes  #-}
 {-# LANGUAGE TypeOperators        #-}
 {-# LANGUAGE UndecidableInstances #-}
 
-module ZkFold.Symbolic.Data.MerkleTree where
-
 
+module ZkFold.Symbolic.Data.MerkleTree where
 
-import ZkFold.Symbolic.Data.Class
-import GHC.Generics
-import ZkFold.Symbolic.Data.Payloaded (Payloaded)
+import           ZkFold.Symbolic.Data.Class
+import           GHC.Generics                     hiding (Rep)
+import           ZkFold.Symbolic.Data.Payloaded   (Payloaded (..))
+import           Data.Functor.Rep                 (Representable, distributeRep, Rep)
+import           Data.Functor                     (Functor (..))
 import           GHC.TypeNats
-import           Data.Functor.Rep                 (Representable, distributeRep)
-import           Data.Functor                     (Functor)
-import Data.Distributive (Distributive, distribute)
+import           Data.Distributive                (Distributive (..))
+import           ZkFold.Base.Data.Vector
+import           Data.Type.Equality               (type (~))
+import           Prelude                          (const, ($), undefined)
+import           ZkFold.Symbolic.Data.Maybe
+import           ZkFold.Symbolic.Data.Bool        (Bool, true)
+import           Data.Foldable                    (Foldable (foldr))
+import           ZkFold.Symbolic.Data.Input       (SymbolicInput, isValid)
+import           ZkFold.Symbolic.Data.Conditional (bool, Conditional)
+import           Control.DeepSeq                  (NFData)
+import           ZkFold.Base.Data.ByteString      (Binary)
+import           Control.Monad.Representable.Reader (WrappedRep)
 
-data Leaf l a = Leaf { leafHash    :: l a }
+newtype Leaf l a = Leaf { leafHash :: l a }
   deriving (Functor, Generic1)
-
-instance (Representable l) => Representable (Leaf l)
-
 instance (Representable l) => Distributive (Leaf l) where
+  distribute :: (Functor f) => f (Leaf l a) -> Leaf l (f a)
   distribute = distributeRep
 
+instance (Representable l) => Representable (Leaf l)
 
 
-data MerkleTree d x = MerkleTree {
-    mHash    :: Context x (Layout x)
-  , mLeft    :: Payloaded (Par1 :*: Leaf (Layout x) :*: MerkleTree (d - 1)) (Context x)
-  , mRight   :: Payloaded (Par1 :*: Leaf (Layout x) :*: MerkleTree (d - 1)) (Context x)
+data MerkleTree (d :: Natural) a = MerkleTree {
+    mHash     :: (Context a) (Layout a)
+  , mLeaves   :: Payloaded (Vector (2 ^ d) :.: Leaf (Layout a)) (Context a)
   }
   deriving (Generic)
 
--- instance Functor (MerkleTree d)
-instance Representable (MerkleTree d)
+instance (SymbolicData a, KnownNat (2 ^ d)) => SymbolicData (MerkleTree d a)
+instance
+  ( SymbolicData a, SymbolicInput a
+  , NFData (Rep (Layout a))
+  , Binary (Rep (Layout a))
+  , KnownNat (2 ^ d)
+  , Binary (WrappedRep (Layout a)))
+  => SymbolicInput (MerkleTree d a) where
+    isValid _ = true
+
+-- ZkFold.Symbolic.Data.Maybe
+-- | Finds an element satisfying the constraint
+find :: forall a d c.  (Conditional (Bool c) a, Foldable (MerkleTree d), SymbolicInput a, Context a ~ c) =>(a -> Bool c) -> MerkleTree d a -> Maybe c a
+find p = let n = nothing @a @c in
+  foldr (\i r -> maybe @a @_ @c (bool @(Bool c) n (just  @c i) $ p i) (const r) r) n
+
+
+newtype MerkleTreePath (d :: Natural) a = MerkleTreePath { path :: Vector d (Bool (Context a))}
+  deriving (Generic)
+
+-- | Finds a path to an element satisfying the constraint
+findPath :: (x -> Bool (Context x)) -> MerkleTree d x -> Maybe (Context x) (MerkleTreePath d x)
+findPath _ = undefined
+
+-- -- | Returns the element corresponding to a path
+-- lookup :: MerkleTree d x -> MerkleTreePath d x -> x
+
+-- -- | Inserts an element at a specified position in a tree
+-- insert :: MerkleTree d x -> MerkleTreePath d x -> x -> MerkleTree d x
+
+-- -- | Replaces an element satisfying the constraint. A composition of `findPath` and `insert`
+-- replace :: (x -> Bool (Context x)) ->  MerkleTree d x -> x -> MerkleTree d x
 
--- instance (SymbolicData x, c ~ Context x) => SymbolicData (MerkleTree d x)
+-- -- | Returns the next path in a tree
+-- incrementPath :: MerkleTreePath d x -> MerkleTreePath d x
\ No newline at end of file

From 1236fa8a0b55903a0e4c52ef59589a4dc942af9f Mon Sep 17 00:00:00 2001
From: Ann Hovanskaya <hovanja2011@gmail.com>
Date: Thu, 9 Jan 2025 01:48:33 +0300
Subject: [PATCH 03/15] trying MerkleTreePath

---
 .../src/ZkFold/Symbolic/Data/MerkleTree.hs    | 47 +++++++++----------
 1 file changed, 22 insertions(+), 25 deletions(-)

diff --git a/symbolic-base/src/ZkFold/Symbolic/Data/MerkleTree.hs b/symbolic-base/src/ZkFold/Symbolic/Data/MerkleTree.hs
index 6c991368..8260cfe7 100644
--- a/symbolic-base/src/ZkFold/Symbolic/Data/MerkleTree.hs
+++ b/symbolic-base/src/ZkFold/Symbolic/Data/MerkleTree.hs
@@ -8,7 +8,7 @@ module ZkFold.Symbolic.Data.MerkleTree where
 import           ZkFold.Symbolic.Data.Class
 import           GHC.Generics                     hiding (Rep)
 import           ZkFold.Symbolic.Data.Payloaded   (Payloaded (..))
-import           Data.Functor.Rep                 (Representable, distributeRep, Rep)
+import           Data.Functor.Rep                 (Representable, distributeRep, pureRep)
 import           Data.Functor                     (Functor (..))
 import           GHC.TypeNats
 import           Data.Distributive                (Distributive (..))
@@ -16,42 +16,35 @@ import           ZkFold.Base.Data.Vector
 import           Data.Type.Equality               (type (~))
 import           Prelude                          (const, ($), undefined)
 import           ZkFold.Symbolic.Data.Maybe
-import           ZkFold.Symbolic.Data.Bool        (Bool, true)
+import           ZkFold.Symbolic.Data.Bool        (Bool)
 import           Data.Foldable                    (Foldable (foldr))
-import           ZkFold.Symbolic.Data.Input       (SymbolicInput, isValid)
+import           ZkFold.Symbolic.Data.Input       (SymbolicInput)
 import           ZkFold.Symbolic.Data.Conditional (bool, Conditional)
-import           Control.DeepSeq                  (NFData)
-import           ZkFold.Base.Data.ByteString      (Binary)
-import           Control.Monad.Representable.Reader (WrappedRep)
+import ZkFold.Symbolic.Class
+import ZkFold.Base.Algebra.Basic.Class
 
-newtype Leaf l a = Leaf { leafHash :: l a }
+newtype Leaf a = Leaf { leafHash :: a }
   deriving (Functor, Generic1)
-instance (Representable l) => Distributive (Leaf l) where
-  distribute :: (Functor f) => f (Leaf l a) -> Leaf l (f a)
-  distribute = distributeRep
 
-instance (Representable l) => Representable (Leaf l)
+instance Distributive Leaf where
+  distribute :: (Functor f) => f (Leaf a) -> Leaf (f a)
+  distribute = distributeRep
 
+instance Representable Leaf
 
 data MerkleTree (d :: Natural) a = MerkleTree {
-    mHash     :: (Context a) (Layout a)
-  , mLeaves   :: Payloaded (Vector (2 ^ d) :.: Leaf (Layout a)) (Context a)
+    mHash     :: Context a (Layout a)
+  , mLeaves   :: Payloaded (Vector (2 ^ d) :.: Leaf) (Context a)
   }
   deriving (Generic)
 
 instance (SymbolicData a, KnownNat (2 ^ d)) => SymbolicData (MerkleTree d a)
-instance
-  ( SymbolicData a, SymbolicInput a
-  , NFData (Rep (Layout a))
-  , Binary (Rep (Layout a))
-  , KnownNat (2 ^ d)
-  , Binary (WrappedRep (Layout a)))
-  => SymbolicInput (MerkleTree d a) where
-    isValid _ = true
+instance (SymbolicInput a, KnownNat (2 ^ d)) => SymbolicInput (MerkleTree d a)
+
 
 -- ZkFold.Symbolic.Data.Maybe
 -- | Finds an element satisfying the constraint
-find :: forall a d c.  (Conditional (Bool c) a, Foldable (MerkleTree d), SymbolicInput a, Context a ~ c) =>(a -> Bool c) -> MerkleTree d a -> Maybe c a
+find :: forall a d c.  (Conditional (Bool c) a, Foldable (MerkleTree d), SymbolicInput a, Context a ~ c) => (a -> Bool c) -> MerkleTree d a -> Maybe c a
 find p = let n = nothing @a @c in
   foldr (\i r -> maybe @a @_ @c (bool @(Bool c) n (just  @c i) $ p i) (const r) r) n
 
@@ -61,13 +54,17 @@ newtype MerkleTreePath (d :: Natural) a = MerkleTreePath { path :: Vector d (Boo
 
 -- | Finds a path to an element satisfying the constraint
 findPath :: (x -> Bool (Context x)) -> MerkleTree d x -> Maybe (Context x) (MerkleTreePath d x)
-findPath _ = undefined
+findPath p (MerkleTree h ls) = undefined -- MerkleTree h ls
 
 -- -- | Returns the element corresponding to a path
 -- lookup :: MerkleTree d x -> MerkleTreePath d x -> x
 
--- -- | Inserts an element at a specified position in a tree
--- insert :: MerkleTree d x -> MerkleTreePath d x -> x -> MerkleTree d x
+-- | Inserts an element at a specified position in a tree
+insert ::
+  ( Symbolic (Context a)
+  , Representable (Layout a))
+  =>MerkleTree d a -> MerkleTreePath d a -> a -> MerkleTree d a
+insert (MerkleTree h ls) p x = MerkleTree (embed $ pureRep zero) ls
 
 -- -- | Replaces an element satisfying the constraint. A composition of `findPath` and `insert`
 -- replace :: (x -> Bool (Context x)) ->  MerkleTree d x -> x -> MerkleTree d x

From 4be95a44fb59844eef9828969548b4c37397c574 Mon Sep 17 00:00:00 2001
From: Ann Hovanskaya <hovanja2011@gmail.com>
Date: Tue, 14 Jan 2025 04:28:58 +0300
Subject: [PATCH 04/15] findpath and lookup updated

---
 .../src/ZkFold/Symbolic/Data/MerkleTree.hs    | 111 +++++++++++++-----
 1 file changed, 79 insertions(+), 32 deletions(-)

diff --git a/symbolic-base/src/ZkFold/Symbolic/Data/MerkleTree.hs b/symbolic-base/src/ZkFold/Symbolic/Data/MerkleTree.hs
index 8260cfe7..20257486 100644
--- a/symbolic-base/src/ZkFold/Symbolic/Data/MerkleTree.hs
+++ b/symbolic-base/src/ZkFold/Symbolic/Data/MerkleTree.hs
@@ -7,67 +7,114 @@ module ZkFold.Symbolic.Data.MerkleTree where
 
 import           ZkFold.Symbolic.Data.Class
 import           GHC.Generics                     hiding (Rep)
-import           ZkFold.Symbolic.Data.Payloaded   (Payloaded (..))
-import           Data.Functor.Rep                 (Representable, distributeRep, pureRep)
-import           Data.Functor                     (Functor (..))
+import           Data.Functor.Rep                 (Representable, pureRep)
 import           GHC.TypeNats
-import           Data.Distributive                (Distributive (..))
-import           ZkFold.Base.Data.Vector
 import           Data.Type.Equality               (type (~))
-import           Prelude                          (const, ($), undefined)
-import           ZkFold.Symbolic.Data.Maybe
-import           ZkFold.Symbolic.Data.Bool        (Bool)
-import           Data.Foldable                    (Foldable (foldr))
+import           Prelude                          (const, ($), undefined, Traversable, Integer, (==))
+import qualified Prelude                          as P
+import           ZkFold.Symbolic.Data.Bool        (Bool (..), BoolType (..))
+import           ZkFold.Symbolic.Data.Bool        (Bool (..))
+import           Data.Foldable                    (Foldable (..))
 import           ZkFold.Symbolic.Data.Input       (SymbolicInput)
 import           ZkFold.Symbolic.Data.Conditional (bool, Conditional)
 import ZkFold.Symbolic.Class
 import ZkFold.Base.Algebra.Basic.Class
-
-newtype Leaf a = Leaf { leafHash :: a }
-  deriving (Functor, Generic1)
-
-instance Distributive Leaf where
-  distribute :: (Functor f) => f (Leaf a) -> Leaf (f a)
-  distribute = distributeRep
-
-instance Representable Leaf
+import ZkFold.Symbolic.Data.List (List, uncons, emptyList, (.:))
+import ZkFold.Base.Data.Vector (knownNat)
+import ZkFold.Symbolic.Data.Maybe (Maybe, just, nothing, maybe)
+import ZkFold.Base.Protocol.IVC.Accumulator (x)
 
 data MerkleTree (d :: Natural) a = MerkleTree {
-    mHash     :: Context a (Layout a)
-  , mLeaves   :: Payloaded (Vector (2 ^ d) :.: Leaf) (Context a)
+    mHash     :: (Context a) (Layout a)
+  , mLeaves   :: List (Context a) a
   }
   deriving (Generic)
 
 instance (SymbolicData a, KnownNat (2 ^ d)) => SymbolicData (MerkleTree d a)
 instance (SymbolicInput a, KnownNat (2 ^ d)) => SymbolicInput (MerkleTree d a)
 
+instance
+  ( Symbolic c
+  , Context a ~ c
+  , Traversable (Layout a)
+  , Representable (Layout a)
+  , Conditional (Bool c) (List c a)
+  ) => Conditional (Bool c) (MerkleTree d a)
 
--- ZkFold.Symbolic.Data.Maybe
 -- | Finds an element satisfying the constraint
-find :: forall a d c.  (Conditional (Bool c) a, Foldable (MerkleTree d), SymbolicInput a, Context a ~ c) => (a -> Bool c) -> MerkleTree d a -> Maybe c a
+find :: forall a d c.
+  ( Conditional (Bool c) a
+  , Foldable (MerkleTree d)
+  , SymbolicInput a
+  , Context a ~ c)
+  => (a -> Bool c) -> MerkleTree d a -> Maybe c a
 find p = let n = nothing @a @c in
-  foldr (\i r -> maybe @a @_ @c (bool @(Bool c) n (just  @c i) $ p i) (const r) r) n
+  foldr (\i r -> maybe @a @_ @c (bool @(Bool c) n (just @c i) $ p i) (const r) r) n
 
-
-newtype MerkleTreePath (d :: Natural) a = MerkleTreePath { path :: Vector d (Bool (Context a))}
+newtype MerkleTreePath (d :: Natural) b = MerkleTreePath { mPath ::  List (Context b) b}
   deriving (Generic)
 
+instance
+  ( Symbolic c
+  , c ~ Context b
+  , KnownNat d
+  , Conditional (Bool c) (List c b)
+  ) => Conditional (Bool c) (MerkleTreePath d b)
+
 -- | Finds a path to an element satisfying the constraint
-findPath :: (x -> Bool (Context x)) -> MerkleTree d x -> Maybe (Context x) (MerkleTreePath d x)
-findPath p (MerkleTree h ls) = undefined -- MerkleTree h ls
+findPath :: forall x c d.
+  ( Context x ~ c
+  , SymbolicOutput x
+  , Conditional (Bool c) (List c x)
+  , Conditional (Bool c) Integer
+  , KnownNat d
+  , Conditional P.Bool (List c (Bool c)))
+  => (x -> Bool (Context x)) -> MerkleTree d x -> Maybe c (MerkleTreePath d (Bool c))
+findPath p (MerkleTree _ ml) = just @c $ MerkleTreePath (bool path (emptyList @c) (ind P.== 0))
+  where
+    (ind, _) = helper (0, ml)
+
+    helper :: (Integer, List c x) -> (Integer , List c x)
+    helper (i, leaves) = let (l, ls) = uncons @c @x leaves
+      in bool (helper (i + 1, ls)) (i, leaves) (p l)
+
+    d = knownNat @d :: Integer
+
+    path :: List c (Bool c)
+    path = foldl (\nl ni -> Bool (embed (Par1 $ fromConstant ni)) .: nl) (emptyList @c)
+      $ P.map (\i -> mod (div ind (2 P.^ i)) 2) [0 .. d]
+
+
+-- | Returns the element corresponding to a path
+lookup :: forall x c d.
+  ( KnownNat d
+  , SymbolicOutput x
+  , Context x ~ c, Conditional (Bool c) Integer
+  ) => MerkleTree d x -> MerkleTreePath d (Bool c) -> x
+lookup (MerkleTree _ ml) (MerkleTreePath p) = val ml $ ind d 0 p
+  where
+    d = knownNat @d :: Integer
+
+    ind :: Integer -> Integer -> List c (Bool c) -> Integer
+    ind 0 i _ = i
+    ind iter i ps = let (l, ls) = uncons @c ps
+      in bool (ind (iter-1) (2*i) ls) (ind (iter-1) (2*i+1) ls) l
+
+    val :: List c x -> Integer -> x
+    val mt 0 = let (l, _) = uncons @c @x mt in l
+    val mt i = let (_, ls) = uncons @c @x mt in val ls (i-1)
 
--- -- | Returns the element corresponding to a path
--- lookup :: MerkleTree d x -> MerkleTreePath d x -> x
 
 -- | Inserts an element at a specified position in a tree
 insert ::
   ( Symbolic (Context a)
   , Representable (Layout a))
-  =>MerkleTree d a -> MerkleTreePath d a -> a -> MerkleTree d a
+  => MerkleTree d a -> MerkleTreePath d a -> a -> MerkleTree d a
 insert (MerkleTree h ls) p x = MerkleTree (embed $ pureRep zero) ls
 
 -- -- | Replaces an element satisfying the constraint. A composition of `findPath` and `insert`
 -- replace :: (x -> Bool (Context x)) ->  MerkleTree d x -> x -> MerkleTree d x
 
--- -- | Returns the next path in a tree
--- incrementPath :: MerkleTreePath d x -> MerkleTreePath d x
\ No newline at end of file
+-- | Returns the next path in a tree
+incrementPath :: MerkleTreePath d x -> MerkleTreePath d x
+incrementPath = undefined
\ No newline at end of file

From 1cf312c363c39ddade0a530eb15e9b99712734b1 Mon Sep 17 00:00:00 2001
From: Ann Hovanskaya <hovanja2011@gmail.com>
Date: Tue, 14 Jan 2025 14:39:22 +0300
Subject: [PATCH 05/15] rollTree added

---
 .../src/ZkFold/Symbolic/Data/MerkleTree.hs    | 78 ++++++++++++++++---
 1 file changed, 69 insertions(+), 9 deletions(-)

diff --git a/symbolic-base/src/ZkFold/Symbolic/Data/MerkleTree.hs b/symbolic-base/src/ZkFold/Symbolic/Data/MerkleTree.hs
index 20257486..185600c0 100644
--- a/symbolic-base/src/ZkFold/Symbolic/Data/MerkleTree.hs
+++ b/symbolic-base/src/ZkFold/Symbolic/Data/MerkleTree.hs
@@ -10,19 +10,21 @@ import           GHC.Generics                     hiding (Rep)
 import           Data.Functor.Rep                 (Representable, pureRep)
 import           GHC.TypeNats
 import           Data.Type.Equality               (type (~))
-import           Prelude                          (const, ($), undefined, Traversable, Integer, (==))
+import           Prelude                          (const, ($), undefined, Traversable, Integer)
 import qualified Prelude                          as P
-import           ZkFold.Symbolic.Data.Bool        (Bool (..), BoolType (..))
 import           ZkFold.Symbolic.Data.Bool        (Bool (..))
 import           Data.Foldable                    (Foldable (..))
 import           ZkFold.Symbolic.Data.Input       (SymbolicInput)
 import           ZkFold.Symbolic.Data.Conditional (bool, Conditional)
 import ZkFold.Symbolic.Class
 import ZkFold.Base.Algebra.Basic.Class
-import ZkFold.Symbolic.Data.List (List, uncons, emptyList, (.:))
+import ZkFold.Symbolic.Data.List (List (..), uncons, emptyList, (.:), ListItem (..))
 import ZkFold.Base.Data.Vector (knownNat)
 import ZkFold.Symbolic.Data.Maybe (Maybe, just, nothing, maybe)
-import ZkFold.Base.Protocol.IVC.Accumulator (x)
+import ZkFold.Symbolic.Data.Hash (Hashable (hasher))
+import ZkFold.Symbolic.Data.Payloaded
+import Data.List.Infinite (Infinite(..))
+import ZkFold.Symbolic.MonadCircuit
 
 data MerkleTree (d :: Natural) a = MerkleTree {
     mHash     :: (Context a) (Layout a)
@@ -89,7 +91,8 @@ findPath p (MerkleTree _ ml) = just @c $ MerkleTreePath (bool path (emptyList @c
 lookup :: forall x c d.
   ( KnownNat d
   , SymbolicOutput x
-  , Context x ~ c, Conditional (Bool c) Integer
+  , Context x ~ c
+  , Conditional (Bool c) Integer
   ) => MerkleTree d x -> MerkleTreePath d (Bool c) -> x
 lookup (MerkleTree _ ml) (MerkleTreePath p) = val ml $ ind d 0 p
   where
@@ -101,8 +104,30 @@ lookup (MerkleTree _ ml) (MerkleTreePath p) = val ml $ ind d 0 p
       in bool (ind (iter-1) (2*i) ls) (ind (iter-1) (2*i+1) ls) l
 
     val :: List c x -> Integer -> x
-    val mt 0 = let (l, _) = uncons @c @x mt in l
-    val mt i = let (_, ls) = uncons @c @x mt in val ls (i-1)
+    val mt i = let (l, ls) = uncons @c @x mt in
+      case i of
+        0 -> l
+        _ -> val ls (i-1)
+
+
+rollTree :: forall d a c.
+  ( c ~ Context a
+  , SymbolicOutput a
+  , KnownNat d
+  , Hashable a a
+  , AdditiveSemigroup a
+  ) => MerkleTree d a -> MerkleTree (d - 1) a
+rollTree (MerkleTree h l) = MerkleTree h (solve d l)
+  where
+    d = 2 P.^ (knownNat @d :: Integer)
+
+    solve :: Integer -> List c a -> List c a
+    solve 0 _ = emptyList @c
+    solve i lst =
+      let (x1, list1) = uncons lst
+          (x2, olist) = uncons list1
+      in hasher (x1 + x2) .: solve (i - 2) olist
+
 
 
 -- | Inserts an element at a specified position in a tree
@@ -116,5 +141,40 @@ insert (MerkleTree h ls) p x = MerkleTree (embed $ pureRep zero) ls
 -- replace :: (x -> Bool (Context x)) ->  MerkleTree d x -> x -> MerkleTree d x
 
 -- | Returns the next path in a tree
-incrementPath :: MerkleTreePath d x -> MerkleTreePath d x
-incrementPath = undefined
\ No newline at end of file
+incrementPath :: forall c d.
+  ( KnownNat d
+  , Symbolic c
+  , Conditional (Bool c) Integer
+  ) => MerkleTreePath d (Bool c) -> MerkleTreePath d (Bool c)
+incrementPath (MerkleTreePath p) = MerkleTreePath (path $ ind d 0 p + 1)
+  where
+    d = knownNat @d :: Integer
+
+    ind :: Integer -> Integer -> List c (Bool c) -> Integer
+    ind 0 i _ = i
+    ind iter i ps = let (l, ls) = uncons @c ps
+      in bool (ind (iter-1) (2*i) ls) (ind (iter-1) (2*i+1) ls) l
+
+    path :: Integer -> List c (Bool c)
+    path val = foldl (\nl ni -> Bool (embed (Par1 $ fromConstant ni)) .: nl) (emptyList @c)
+      $ P.map (\i -> mod (div val (2 P.^ i)) 2) [0 .. d]
+
+
+-- | Returns the previous path in a tree
+-- decrementPath :: forall c d.
+--   ( KnownNat d
+--   , Symbolic c
+--   , Conditional (Bool c) Integer
+--   ) => MerkleTreePath d (Bool c) -> MerkleTreePath d (Bool c)
+-- decrementPath (MerkleTreePath p) = MerkleTreePath (path $ ind d 0 p - 1)
+--   where
+--     d = knownNat @d :: Integer
+
+--     ind :: Integer -> Integer -> List c (Bool c) -> Integer
+--     ind 0 i _ = i
+--     ind iter i ps = let (l, ls) = uncons @c ps
+--       in bool (ind (iter-1) (2*i) ls) (ind (iter-1) (2*i+1) ls) l
+
+--     path :: Integer -> List c (Bool c)
+--     path val = foldl (\nl ni -> Bool (embed (Par1 $ fromConstant ni)) .: nl) (emptyList @c)
+--       $ P.map (\i -> mod (div val (2 P.^ i)) 2) [0 .. d]

From b0b1f8310f8ed3cdab45fe27a4a47f867f424a9a Mon Sep 17 00:00:00 2001
From: hovanja2011 <hovanja2011@users.noreply.github.com>
Date: Tue, 14 Jan 2025 11:55:40 +0000
Subject: [PATCH 06/15] stylish-haskell auto-commit

---
 .../src/ZkFold/Symbolic/Data/MerkleTree.hs    | 35 ++++++++++---------
 1 file changed, 18 insertions(+), 17 deletions(-)

diff --git a/symbolic-base/src/ZkFold/Symbolic/Data/MerkleTree.hs b/symbolic-base/src/ZkFold/Symbolic/Data/MerkleTree.hs
index 185600c0..1ea460b2 100644
--- a/symbolic-base/src/ZkFold/Symbolic/Data/MerkleTree.hs
+++ b/symbolic-base/src/ZkFold/Symbolic/Data/MerkleTree.hs
@@ -5,30 +5,31 @@
 
 module ZkFold.Symbolic.Data.MerkleTree where
 
-import           ZkFold.Symbolic.Data.Class
-import           GHC.Generics                     hiding (Rep)
+import           Data.Foldable                    (Foldable (..))
 import           Data.Functor.Rep                 (Representable, pureRep)
-import           GHC.TypeNats
+import           Data.List.Infinite               (Infinite (..))
 import           Data.Type.Equality               (type (~))
-import           Prelude                          (const, ($), undefined, Traversable, Integer)
+import           GHC.Generics                     hiding (Rep)
+import           GHC.TypeNats
+import           Prelude                          (Integer, Traversable, const, undefined, ($))
 import qualified Prelude                          as P
+
+import           ZkFold.Base.Algebra.Basic.Class
+import           ZkFold.Base.Data.Vector          (knownNat)
+import           ZkFold.Symbolic.Class
 import           ZkFold.Symbolic.Data.Bool        (Bool (..))
-import           Data.Foldable                    (Foldable (..))
+import           ZkFold.Symbolic.Data.Class
+import           ZkFold.Symbolic.Data.Conditional (Conditional, bool)
+import           ZkFold.Symbolic.Data.Hash        (Hashable (hasher))
 import           ZkFold.Symbolic.Data.Input       (SymbolicInput)
-import           ZkFold.Symbolic.Data.Conditional (bool, Conditional)
-import ZkFold.Symbolic.Class
-import ZkFold.Base.Algebra.Basic.Class
-import ZkFold.Symbolic.Data.List (List (..), uncons, emptyList, (.:), ListItem (..))
-import ZkFold.Base.Data.Vector (knownNat)
-import ZkFold.Symbolic.Data.Maybe (Maybe, just, nothing, maybe)
-import ZkFold.Symbolic.Data.Hash (Hashable (hasher))
-import ZkFold.Symbolic.Data.Payloaded
-import Data.List.Infinite (Infinite(..))
-import ZkFold.Symbolic.MonadCircuit
+import           ZkFold.Symbolic.Data.List        (List (..), ListItem (..), emptyList, uncons, (.:))
+import           ZkFold.Symbolic.Data.Maybe       (Maybe, just, maybe, nothing)
+import           ZkFold.Symbolic.Data.Payloaded
+import           ZkFold.Symbolic.MonadCircuit
 
 data MerkleTree (d :: Natural) a = MerkleTree {
-    mHash     :: (Context a) (Layout a)
-  , mLeaves   :: List (Context a) a
+    mHash   :: (Context a) (Layout a)
+  , mLeaves :: List (Context a) a
   }
   deriving (Generic)
 

From b3e0a7c19158468114aa7a05236e10350f37e5ba Mon Sep 17 00:00:00 2001
From: Ann Hovanskaya <hovanja2011@gmail.com>
Date: Tue, 14 Jan 2025 15:04:57 +0300
Subject: [PATCH 07/15] redundant imports

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

diff --git a/symbolic-base/src/ZkFold/Symbolic/Data/MerkleTree.hs b/symbolic-base/src/ZkFold/Symbolic/Data/MerkleTree.hs
index 1ea460b2..f940b6f8 100644
--- a/symbolic-base/src/ZkFold/Symbolic/Data/MerkleTree.hs
+++ b/symbolic-base/src/ZkFold/Symbolic/Data/MerkleTree.hs
@@ -7,11 +7,10 @@ module ZkFold.Symbolic.Data.MerkleTree where
 
 import           Data.Foldable                    (Foldable (..))
 import           Data.Functor.Rep                 (Representable, pureRep)
-import           Data.List.Infinite               (Infinite (..))
 import           Data.Type.Equality               (type (~))
 import           GHC.Generics                     hiding (Rep)
 import           GHC.TypeNats
-import           Prelude                          (Integer, Traversable, const, undefined, ($))
+import           Prelude                          (Integer, Traversable, const, ($))
 import qualified Prelude                          as P
 
 import           ZkFold.Base.Algebra.Basic.Class
@@ -22,10 +21,8 @@ import           ZkFold.Symbolic.Data.Class
 import           ZkFold.Symbolic.Data.Conditional (Conditional, bool)
 import           ZkFold.Symbolic.Data.Hash        (Hashable (hasher))
 import           ZkFold.Symbolic.Data.Input       (SymbolicInput)
-import           ZkFold.Symbolic.Data.List        (List (..), ListItem (..), emptyList, uncons, (.:))
+import           ZkFold.Symbolic.Data.List        (List (..), emptyList, uncons, (.:))
 import           ZkFold.Symbolic.Data.Maybe       (Maybe, just, maybe, nothing)
-import           ZkFold.Symbolic.Data.Payloaded
-import           ZkFold.Symbolic.MonadCircuit
 
 data MerkleTree (d :: Natural) a = MerkleTree {
     mHash   :: (Context a) (Layout a)
@@ -136,7 +133,7 @@ insert ::
   ( Symbolic (Context a)
   , Representable (Layout a))
   => MerkleTree d a -> MerkleTreePath d a -> a -> MerkleTree d a
-insert (MerkleTree h ls) p x = MerkleTree (embed $ pureRep zero) ls
+insert (MerkleTree _ ls) _ _ = MerkleTree (embed $ pureRep zero) ls
 
 -- -- | Replaces an element satisfying the constraint. A composition of `findPath` and `insert`
 -- replace :: (x -> Bool (Context x)) ->  MerkleTree d x -> x -> MerkleTree d x

From 71b3a7662ba19aea8e18cd9e248766393cb9d989 Mon Sep 17 00:00:00 2001
From: Ann Hovanskaya <hovanja2011@gmail.com>
Date: Thu, 16 Jan 2025 01:34:41 +0300
Subject: [PATCH 08/15] trying circuit

---
 symbolic-base/src/ZkFold/Base/Data/Vector.hs  |   3 +
 .../src/ZkFold/Symbolic/Data/MerkleTree.hs    | 166 ++++++++++--------
 2 files changed, 93 insertions(+), 76 deletions(-)

diff --git a/symbolic-base/src/ZkFold/Base/Data/Vector.hs b/symbolic-base/src/ZkFold/Base/Data/Vector.hs
index 79a36e6e..a154e6fb 100644
--- a/symbolic-base/src/ZkFold/Base/Data/Vector.hs
+++ b/symbolic-base/src/ZkFold/Base/Data/Vector.hs
@@ -84,6 +84,9 @@ reverse (Vector lst) = Vector (V.reverse lst)
 head :: Vector size a -> a
 head (Vector as) = V.head as
 
+last :: Vector size a -> a
+last (Vector as) = V.last as
+
 tail :: Vector size a -> Vector (size - 1) a
 tail (Vector as) = Vector $ V.tail as
 
diff --git a/symbolic-base/src/ZkFold/Symbolic/Data/MerkleTree.hs b/symbolic-base/src/ZkFold/Symbolic/Data/MerkleTree.hs
index f940b6f8..ed8cd863 100644
--- a/symbolic-base/src/ZkFold/Symbolic/Data/MerkleTree.hs
+++ b/symbolic-base/src/ZkFold/Symbolic/Data/MerkleTree.hs
@@ -10,121 +10,135 @@ import           Data.Functor.Rep                 (Representable, pureRep)
 import           Data.Type.Equality               (type (~))
 import           GHC.Generics                     hiding (Rep)
 import           GHC.TypeNats
-import           Prelude                          (Integer, Traversable, const, ($))
+import           Prelude                          (Integer, Traversable, const, ($), return)
 import qualified Prelude                          as P
 
 import           ZkFold.Base.Algebra.Basic.Class
-import           ZkFold.Base.Data.Vector          (knownNat)
+import           ZkFold.Base.Data.Vector
+import qualified ZkFold.Base.Data.Vector as V
 import           ZkFold.Symbolic.Class
 import           ZkFold.Symbolic.Data.Bool        (Bool (..))
 import           ZkFold.Symbolic.Data.Class
 import           ZkFold.Symbolic.Data.Conditional (Conditional, bool)
-import           ZkFold.Symbolic.Data.Hash        (Hashable (hasher))
 import           ZkFold.Symbolic.Data.Input       (SymbolicInput)
-import           ZkFold.Symbolic.Data.List        (List (..), emptyList, uncons, (.:))
+import           ZkFold.Symbolic.Data.List
+import qualified ZkFold.Symbolic.Data.List as L
 import           ZkFold.Symbolic.Data.Maybe       (Maybe, just, maybe, nothing)
-
-data MerkleTree (d :: Natural) a = MerkleTree {
-    mHash   :: (Context a) (Layout a)
-  , mLeaves :: List (Context a) a
+import ZkFold.Symbolic.MonadCircuit
+import Data.Traversable (Traversable(traverse))
+import ZkFold.Base.Control.HApplicative (hunit)
+import Data.Proxy (Proxy(Proxy))
+
+data MerkleTree (d :: Natural) h = MerkleTree {
+    mHash   :: (Context h) (Layout h)
+  , mLevels :: Vector d (List (Context h) h)
   }
   deriving (Generic)
 
-instance (SymbolicData a, KnownNat (2 ^ d)) => SymbolicData (MerkleTree d a)
-instance (SymbolicInput a, KnownNat (2 ^ d)) => SymbolicInput (MerkleTree d a)
+hashAux :: forall i m a w. MonadCircuit i a w m => i -> i -> i -> m i
+hashAux b h g = newAssigned (($ b) * ($ merkleHasher h g) + (one - ($ b)* ($ merkleHasher g h)))
+  where
+    merkleHasher :: i -> i -> i
+    merkleHasher = P.undefined
+
+instance (SymbolicData h, KnownNat d) => SymbolicData (MerkleTree d h)
+instance (SymbolicInput h, KnownNat d) => SymbolicInput (MerkleTree d h)
 
 instance
   ( Symbolic c
-  , Context a ~ c
-  , Traversable (Layout a)
-  , Representable (Layout a)
-  , Conditional (Bool c) (List c a)
-  ) => Conditional (Bool c) (MerkleTree d a)
+  , Context h ~ c
+  , Conditional (Bool c) (List c h)
+  , Traversable (Layout h)
+  , Representable (Layout h)
+  , KnownNat d
+  ) => Conditional (Bool c) (MerkleTree d h)
 
 -- | Finds an element satisfying the constraint
-find :: forall a d c.
-  ( Conditional (Bool c) a
-  , Foldable (MerkleTree d)
-  , SymbolicInput a
-  , Context a ~ c)
-  => (a -> Bool c) -> MerkleTree d a -> Maybe c a
-find p = let n = nothing @a @c in
-  foldr (\i r -> maybe @a @_ @c (bool @(Bool c) n (just @c i) $ p i) (const r) r) n
-
-newtype MerkleTreePath (d :: Natural) b = MerkleTreePath { mPath ::  List (Context b) b}
+find :: forall h d c.
+  ( Conditional (Bool c) h
+  , SymbolicInput h
+  , Context h ~ c
+  , Foldable (List c))
+  => (h -> Bool c) -> MerkleTree d h -> Maybe c h
+find p MerkleTree{..} = let n = nothing @h @c in
+  foldr (\i r -> maybe @h @_ @c (bool @(Bool c) n (just @c i) $ p i) (const r) r) n $ V.last mLevels
+
+newtype MerkleTreePath (d :: Natural) c = MerkleTreePath { mPath :: Vector d (Bool c)}
   deriving (Generic)
 
 instance
   ( Symbolic c
-  , c ~ Context b
+  -- , c ~ Context b
   , KnownNat d
-  , Conditional (Bool c) (List c b)
-  ) => Conditional (Bool c) (MerkleTreePath d b)
+  -- , Conditional (Bool c) b
+  -- , Conditional (Bool c) (List c b)
+  ) => Conditional (Bool c) (MerkleTreePath d c)
 
 -- | Finds a path to an element satisfying the constraint
 findPath :: forall x c d.
   ( Context x ~ c
   , SymbolicOutput x
+  , Symbolic c
   , Conditional (Bool c) (List c x)
   , Conditional (Bool c) Integer
-  , KnownNat d
-  , Conditional P.Bool (List c (Bool c)))
-  => (x -> Bool (Context x)) -> MerkleTree d x -> Maybe c (MerkleTreePath d (Bool c))
-findPath p (MerkleTree _ ml) = just @c $ MerkleTreePath (bool path (emptyList @c) (ind P.== 0))
+  , KnownNat d)
+  => (x -> Bool (Context x)) -> MerkleTree d x -> Maybe c (MerkleTreePath d c)
+findPath p (MerkleTree _ mll) = just @c $ MerkleTreePath path
   where
-    (ind, _) = helper (0, ml)
+    ml = V.last mll
+    (ind', _) = helper (0, ml)
 
     helper :: (Integer, List c x) -> (Integer , List c x)
-    helper (i, leaves) = let (l, ls) = uncons @c @x leaves
+    helper (i, leaves) = let (l, ls) = L.uncons @c @x leaves
       in bool (helper (i + 1, ls)) (i, leaves) (p l)
 
     d = knownNat @d :: Integer
 
-    path :: List c (Bool c)
-    path = foldl (\nl ni -> Bool (embed (Par1 $ fromConstant ni)) .: nl) (emptyList @c)
-      $ P.map (\i -> mod (div ind (2 P.^ i)) 2) [0 .. d]
+    path :: Vector d (Bool c)
+    path = unsafeToVector $ foldl (\nl ni -> Bool (embed @c (Par1 $ fromConstant ni )) : nl) []
+      $ P.map (\i -> mod (div ind' (2 P.^ i)) 2) [1 .. d]
 
 
 -- | Returns the element corresponding to a path
 lookup :: forall x c d.
-  ( KnownNat d
-  , SymbolicOutput x
+  ( SymbolicOutput x
   , Context x ~ c
   , Conditional (Bool c) Integer
-  ) => MerkleTree d x -> MerkleTreePath d (Bool c) -> x
-lookup (MerkleTree _ ml) (MerkleTreePath p) = val ml $ ind d 0 p
+  ) => MerkleTree d x -> MerkleTreePath (d-1) c -> x
+lookup (MerkleTree root nodes) (MerkleTreePath p) = xA
   where
-    d = knownNat @d :: Integer
+    xP = leaf @x (V.last nodes) $ ind p
+
+    xA = restore @x @c $ const
+        ( preimage --fromCircuitF @c hunit $ const (traverse unconstrained (witnessF $ arithmetize xP Proxy) )
+        , payload xP Proxy)
+
+    preimage :: c (Layout x)
+    preimage = fromCircuitVF path $ \p' -> do
+      let Par1 i = P.head p'
+      return i
+      -- fromCircuitF @c hunit $ const (traverse unconstrained (witnessF $ arithmetize xP Proxy))
+
+    path = P.map (\(Bool b) -> b) $ V.fromVector p -- pack $ V.toVector $ P.map embed (unsafeToVector p)
 
-    ind :: Integer -> Integer -> List c (Bool c) -> Integer
-    ind 0 i _ = i
-    ind iter i ps = let (l, ls) = uncons @c ps
-      in bool (ind (iter-1) (2*i) ls) (ind (iter-1) (2*i+1) ls) l
+-- lookup (MerkleTree root hashAux leaves) (MerkleTreePath v) = let x = хэш искомой вершины in
+--   fromCircuit3F v root x $ bs r h1-> do
+--     gs <- traversal . unconstrained $ хэши-соседи к листам вдоль пути
+--     r' <- foldl (\h' (g', b') -> newAssigned (hashAux b' h' g') h1 $ zip gs bs
+--     constraint (r' - r)
+--     return h1
 
-    val :: List c x -> Integer -> x
-    val mt i = let (l, ls) = uncons @c @x mt in
+leaf :: forall x. (SymbolicOutput x) => List (Context x) x -> Integer -> x
+leaf mt i = let (l, ls) = L.uncons mt in
       case i of
         0 -> l
-        _ -> val ls (i-1)
+        _ -> leaf ls (i-1)
 
+ind :: forall d c. (Conditional (Bool c) Integer) => Vector d (Bool c) -> Integer
+ind ps = let ls = V.fromVector ps
+      in foldl (\num b -> bool (num*2 +1) (num*2) b) 0 ls
 
-rollTree :: forall d a c.
-  ( c ~ Context a
-  , SymbolicOutput a
-  , KnownNat d
-  , Hashable a a
-  , AdditiveSemigroup a
-  ) => MerkleTree d a -> MerkleTree (d - 1) a
-rollTree (MerkleTree h l) = MerkleTree h (solve d l)
-  where
-    d = 2 P.^ (knownNat @d :: Integer)
 
-    solve :: Integer -> List c a -> List c a
-    solve 0 _ = emptyList @c
-    solve i lst =
-      let (x1, list1) = uncons lst
-          (x2, olist) = uncons list1
-      in hasher (x1 + x2) .: solve (i - 2) olist
 
 
 
@@ -132,30 +146,30 @@ rollTree (MerkleTree h l) = MerkleTree h (solve d l)
 insert ::
   ( Symbolic (Context a)
   , Representable (Layout a))
-  => MerkleTree d a -> MerkleTreePath d a -> a -> MerkleTree d a
+  => MerkleTree d a -> MerkleTreePath d c -> a -> MerkleTree d a
 insert (MerkleTree _ ls) _ _ = MerkleTree (embed $ pureRep zero) ls
 
 -- -- | Replaces an element satisfying the constraint. A composition of `findPath` and `insert`
 -- replace :: (x -> Bool (Context x)) ->  MerkleTree d x -> x -> MerkleTree d x
 
 -- | Returns the next path in a tree
-incrementPath :: forall c d.
+incrementPath :: forall c d x.
   ( KnownNat d
+  , Context x ~ c
   , Symbolic c
   , Conditional (Bool c) Integer
-  ) => MerkleTreePath d (Bool c) -> MerkleTreePath d (Bool c)
-incrementPath (MerkleTreePath p) = MerkleTreePath (path $ ind d 0 p + 1)
+  ) => MerkleTreePath d c -> MerkleTreePath d c
+incrementPath (MerkleTreePath p) = MerkleTreePath (path $ ind p + 1)
   where
     d = knownNat @d :: Integer
 
-    ind :: Integer -> Integer -> List c (Bool c) -> Integer
-    ind 0 i _ = i
-    ind iter i ps = let (l, ls) = uncons @c ps
-      in bool (ind (iter-1) (2*i) ls) (ind (iter-1) (2*i+1) ls) l
+    ind :: Vector d (Bool c) -> Integer
+    ind ps = let ls = V.fromVector ps
+      in foldl (\num b -> bool (num*2 +1) (num*2) b) 1 ls
 
-    path :: Integer -> List c (Bool c)
-    path val = foldl (\nl ni -> Bool (embed (Par1 $ fromConstant ni)) .: nl) (emptyList @c)
-      $ P.map (\i -> mod (div val (2 P.^ i)) 2) [0 .. d]
+    path :: Integer -> Vector d (Bool c)
+    path val = unsafeToVector $ foldl (\nl ni -> Bool (embed @c (Par1 $ fromConstant ni )) : nl) []
+      $ P.map (\i -> mod (div val (2 P.^ i)) 2) [1 .. d]
 
 
 -- | Returns the previous path in a tree

From 6d25330432674e2e517e7b4c06b26a48454f9ba2 Mon Sep 17 00:00:00 2001
From: Ann Hovanskaya <hovanja2011@gmail.com>
Date: Sat, 18 Jan 2025 03:37:47 +0300
Subject: [PATCH 09/15] lookup ready, but dirty

---
 .../src/ZkFold/Symbolic/Data/MerkleTree.hs    | 143 ++++++++----------
 1 file changed, 61 insertions(+), 82 deletions(-)

diff --git a/symbolic-base/src/ZkFold/Symbolic/Data/MerkleTree.hs b/symbolic-base/src/ZkFold/Symbolic/Data/MerkleTree.hs
index ed8cd863..a942515c 100644
--- a/symbolic-base/src/ZkFold/Symbolic/Data/MerkleTree.hs
+++ b/symbolic-base/src/ZkFold/Symbolic/Data/MerkleTree.hs
@@ -5,12 +5,12 @@
 
 module ZkFold.Symbolic.Data.MerkleTree where
 
-import           Data.Foldable                    (Foldable (..))
-import           Data.Functor.Rep                 (Representable, pureRep)
+import           Data.Foldable                    (Foldable (..), foldlM)
+import Data.Functor.Rep ( pureRep, Representable )
 import           Data.Type.Equality               (type (~))
-import           GHC.Generics                     hiding (Rep)
+import           GHC.Generics                     hiding (Rep, UInt)
 import           GHC.TypeNats
-import           Prelude                          (Integer, Traversable, const, ($), return)
+import           Prelude                          (Integer, Traversable, const, ($), return, zip, (.))
 import qualified Prelude                          as P
 
 import           ZkFold.Base.Algebra.Basic.Class
@@ -23,11 +23,14 @@ import           ZkFold.Symbolic.Data.Conditional (Conditional, bool)
 import           ZkFold.Symbolic.Data.Input       (SymbolicInput)
 import           ZkFold.Symbolic.Data.List
 import qualified ZkFold.Symbolic.Data.List as L
-import           ZkFold.Symbolic.Data.Maybe       (Maybe, just, maybe, nothing)
+import           ZkFold.Symbolic.Data.Maybe       (Maybe, just)
 import ZkFold.Symbolic.MonadCircuit
-import Data.Traversable (Traversable(traverse))
-import ZkFold.Base.Control.HApplicative (hunit)
 import Data.Proxy (Proxy(Proxy))
+import ZkFold.Base.Data.Package
+import ZkFold.Symbolic.Data.Combinators (mzipWithMRep, horner, RegisterSize (Auto))
+import ZkFold.Symbolic.Data.UInt (strictConv, UInt)
+import ZkFold.Base.Control.HApplicative (hpair)
+import qualified Data.List as LL
 
 data MerkleTree (d :: Natural) h = MerkleTree {
     mHash   :: (Context h) (Layout h)
@@ -35,10 +38,13 @@ data MerkleTree (d :: Natural) h = MerkleTree {
   }
   deriving (Generic)
 
-hashAux :: forall i m a w. MonadCircuit i a w m => i -> i -> i -> m i
-hashAux b h g = newAssigned (($ b) * ($ merkleHasher h g) + (one - ($ b)* ($ merkleHasher g h)))
+hashAux :: forall i m a w f. (MonadCircuit i a w m, Representable f, Traversable f) => Par1 i -> f i -> f i -> m (f i)
+hashAux (Par1 b) h g = do
+  v1 <- merkleHasher h g
+  v2 <- merkleHasher g h
+  mzipWithMRep (\wx wy -> newAssigned ((one - ($ b)) * ($ wx) + ($ b) * ($ wy))) v1 v2
   where
-    merkleHasher :: i -> i -> i
+    merkleHasher :: f i -> f i -> m (f i)
     merkleHasher = P.undefined
 
 instance (SymbolicData h, KnownNat d) => SymbolicData (MerkleTree d h)
@@ -54,25 +60,19 @@ instance
   ) => Conditional (Bool c) (MerkleTree d h)
 
 -- | Finds an element satisfying the constraint
-find :: forall h d c.
-  ( Conditional (Bool c) h
-  , SymbolicInput h
-  , Context h ~ c
-  , Foldable (List c))
-  => (h -> Bool c) -> MerkleTree d h -> Maybe c h
-find p MerkleTree{..} = let n = nothing @h @c in
-  foldr (\i r -> maybe @h @_ @c (bool @(Bool c) n (just @c i) $ p i) (const r) r) n $ V.last mLevels
+-- find :: forall h d c.
+--   ( Conditional (Bool c) h
+--   , SymbolicInput h
+--   , Context h ~ c
+--   , Foldable (List c))
+--   => (h -> Bool c) -> MerkleTree d h -> Maybe c h
+-- find p MerkleTree{..} = let n = nothing @h @c in
+--   foldr (\i r -> maybe @h @_ @c (bool @(Bool c) n (just @c i) $ p i) (const r) r) n $ V.last mLevels
 
 newtype MerkleTreePath (d :: Natural) c = MerkleTreePath { mPath :: Vector d (Bool c)}
   deriving (Generic)
 
-instance
-  ( Symbolic c
-  -- , c ~ Context b
-  , KnownNat d
-  -- , Conditional (Bool c) b
-  -- , Conditional (Bool c) (List c b)
-  ) => Conditional (Bool c) (MerkleTreePath d c)
+instance ( Symbolic c, KnownNat d) => Conditional (Bool c) (MerkleTreePath d c)
 
 -- | Finds a path to an element satisfying the constraint
 findPath :: forall x c d.
@@ -103,45 +103,50 @@ findPath p (MerkleTree _ mll) = just @c $ MerkleTreePath path
 lookup :: forall x c d.
   ( SymbolicOutput x
   , Context x ~ c
-  , Conditional (Bool c) Integer
+  , KnownNat (d - 1)
+  , KnownNat d
   ) => MerkleTree d x -> MerkleTreePath (d-1) c -> x
 lookup (MerkleTree root nodes) (MerkleTreePath p) = xA
   where
-    xP = leaf @x (V.last nodes) $ ind p
+    xP = leaf @c @x @d (V.last nodes) $ ind path
 
-    xA = restore @x @c $ const
-        ( preimage --fromCircuitF @c hunit $ const (traverse unconstrained (witnessF $ arithmetize xP Proxy) )
-        , payload xP Proxy)
+    inits = V.unsafeToVector @(d-1) $ LL.unfoldr (\v -> if LL.null v then P.Nothing else P.Just (ind @_ @c (V.unsafeToVector v), LL.init v)) (V.fromVector path)
 
-    preimage :: c (Layout x)
-    preimage = fromCircuitVF path $ \p' -> do
-      let Par1 i = P.head p'
-      return i
-      -- fromCircuitF @c hunit $ const (traverse unconstrained (witnessF $ arithmetize xP Proxy))
+    cinds :: Vector (d-1) (c Par1)
+    cinds = unpacked $ fromCircuit2F (pack path) (pack inits) $ \ps' is' -> do
+      let ps = P.fmap unPar1 (unComp1 ps')
+          is = V.unsafeToVector $ fromConstant @(BaseField c) zero : (P.init . V.fromVector $ P.fmap unPar1 (unComp1 is'))
+      mzipWithMRep (\wp wi -> newAssigned (one - ($ wp) + ($ wi)*(one + one))) ps is
 
-    path = P.map (\(Bool b) -> b) $ V.fromVector p -- pack $ V.toVector $ P.map embed (unsafeToVector p)
+    inds = V.unsafeToVector @(d-1) $ P.zipWith (\l i -> arithmetize (leaf @c @x @d l i) Proxy) (V.fromVector $ V.tail nodes) (V.fromVector cinds)
 
--- lookup (MerkleTree root hashAux leaves) (MerkleTreePath v) = let x = хэш искомой вершины in
---   fromCircuit3F v root x $ bs r h1-> do
---     gs <- traversal . unconstrained $ хэши-соседи к листам вдоль пути
---     r' <- foldl (\h' (g', b') -> newAssigned (hashAux b' h' g') h1 $ zip gs bs
---     constraint (r' - r)
---     return h1
+    xA = restore @x @c $ const (preimage , payload xP Proxy)
 
-leaf :: forall x. (SymbolicOutput x) => List (Context x) x -> Integer -> x
-leaf mt i = let (l, ls) = L.uncons mt in
-      case i of
-        0 -> l
-        _ -> leaf ls (i-1)
+    rootAndH1 :: Context x (Layout x :*: Layout x)
+    rootAndH1 = hpair root (arithmetize xP Proxy)
 
-ind :: forall d c. (Conditional (Bool c) Integer) => Vector d (Bool c) -> Integer
-ind ps = let ls = V.fromVector ps
-      in foldl (\num b -> bool (num*2 +1) (num*2) b) 0 ls
+    preimage :: c (Layout x)
+    preimage = fromCircuit3F (pack inds) (pack path) rootAndH1 $ \ g p' r' -> do
+      let gs = V.fromVector $ unComp1 g
+          bs = V.fromVector $ unComp1 p'
+          (r :*: h1) = r'
+      hd :: Layout x i <- foldlM (\h' (g', b') -> hashAux b' h' g') h1 $ zip gs bs
+      _ <- mzipWithMRep (\wx wy -> constraint (($ wx) - ($ wy))) hd r
+      return h1
 
+    path = P.fmap (\(Bool b) -> b) p
 
 
+leaf :: forall c x d. (SymbolicOutput x, Context x ~ c, KnownNat d) => List c x -> c Par1 -> x
+leaf l i = let num = strictConv @_ @(UInt d Auto c) i in l L.!! num
 
 
+ind :: forall d c. (Symbolic c) => Vector d (c Par1) -> c Par1
+ind vb = fromCircuitF (pack vb) $ \vb' -> do
+  let bs = P.map unPar1 $ V.fromVector $ unComp1 vb'
+  b1n <- P.fmap Par1 . horner $ bs
+  return $ fromConstant b1n
+
 -- | Inserts an element at a specified position in a tree
 insert ::
   ( Symbolic (Context a)
@@ -153,40 +158,14 @@ insert (MerkleTree _ ls) _ _ = MerkleTree (embed $ pureRep zero) ls
 -- replace :: (x -> Bool (Context x)) ->  MerkleTree d x -> x -> MerkleTree d x
 
 -- | Returns the next path in a tree
-incrementPath :: forall c d x.
-  ( KnownNat d
-  , Context x ~ c
-  , Symbolic c
-  , Conditional (Bool c) Integer
-  ) => MerkleTreePath d c -> MerkleTreePath d c
-incrementPath (MerkleTreePath p) = MerkleTreePath (path $ ind p + 1)
-  where
-    d = knownNat @d :: Integer
-
-    ind :: Vector d (Bool c) -> Integer
-    ind ps = let ls = V.fromVector ps
-      in foldl (\num b -> bool (num*2 +1) (num*2) b) 1 ls
-
-    path :: Integer -> Vector d (Bool c)
-    path val = unsafeToVector $ foldl (\nl ni -> Bool (embed @c (Par1 $ fromConstant ni )) : nl) []
-      $ P.map (\i -> mod (div val (2 P.^ i)) 2) [1 .. d]
-
-
--- | Returns the previous path in a tree
--- decrementPath :: forall c d.
+-- incrementPath :: forall c d.
 --   ( KnownNat d
 --   , Symbolic c
---   , Conditional (Bool c) Integer
---   ) => MerkleTreePath d (Bool c) -> MerkleTreePath d (Bool c)
--- decrementPath (MerkleTreePath p) = MerkleTreePath (path $ ind d 0 p - 1)
+--   ) => MerkleTreePath d c -> MerkleTreePath d c
+-- incrementPath (MerkleTreePath p) = MerkleTreePath (path $ ind p +one)
 --   where
 --     d = knownNat @d :: Integer
 
---     ind :: Integer -> Integer -> List c (Bool c) -> Integer
---     ind 0 i _ = i
---     ind iter i ps = let (l, ls) = uncons @c ps
---       in bool (ind (iter-1) (2*i) ls) (ind (iter-1) (2*i+1) ls) l
-
---     path :: Integer -> List c (Bool c)
---     path val = foldl (\nl ni -> Bool (embed (Par1 $ fromConstant ni)) .: nl) (emptyList @c)
---       $ P.map (\i -> mod (div val (2 P.^ i)) 2) [0 .. d]
+--     path :: Natural -> Vector d (Bool c)
+--     path val = unsafeToVector $ foldl (\nl ni -> Bool (embed @c (Par1 $ fromConstant ni )) : nl) []
+--       $ P.map (\i -> mod (div val (2 P.^ i)) 2) [1 .. d]

From af7d1ea797fe7adf53dad7c9d9b7c84490c25030 Mon Sep 17 00:00:00 2001
From: hovanja2011 <hovanja2011@users.noreply.github.com>
Date: Sat, 18 Jan 2025 00:54:24 +0000
Subject: [PATCH 10/15] stylish-haskell auto-commit

---
 .../src/ZkFold/Symbolic/Data/MerkleTree.hs    | 22 +++++++++----------
 1 file changed, 11 insertions(+), 11 deletions(-)

diff --git a/symbolic-base/src/ZkFold/Symbolic/Data/MerkleTree.hs b/symbolic-base/src/ZkFold/Symbolic/Data/MerkleTree.hs
index a942515c..bede8669 100644
--- a/symbolic-base/src/ZkFold/Symbolic/Data/MerkleTree.hs
+++ b/symbolic-base/src/ZkFold/Symbolic/Data/MerkleTree.hs
@@ -6,31 +6,31 @@
 module ZkFold.Symbolic.Data.MerkleTree where
 
 import           Data.Foldable                    (Foldable (..), foldlM)
-import Data.Functor.Rep ( pureRep, Representable )
+import           Data.Functor.Rep                 (Representable, pureRep)
+import qualified Data.List                        as LL
+import           Data.Proxy                       (Proxy (Proxy))
 import           Data.Type.Equality               (type (~))
 import           GHC.Generics                     hiding (Rep, UInt)
 import           GHC.TypeNats
-import           Prelude                          (Integer, Traversable, const, ($), return, zip, (.))
+import           Prelude                          (Integer, Traversable, const, return, zip, ($), (.))
 import qualified Prelude                          as P
 
 import           ZkFold.Base.Algebra.Basic.Class
+import           ZkFold.Base.Control.HApplicative (hpair)
+import           ZkFold.Base.Data.Package
+import qualified ZkFold.Base.Data.Vector          as V
 import           ZkFold.Base.Data.Vector
-import qualified ZkFold.Base.Data.Vector as V
 import           ZkFold.Symbolic.Class
 import           ZkFold.Symbolic.Data.Bool        (Bool (..))
 import           ZkFold.Symbolic.Data.Class
+import           ZkFold.Symbolic.Data.Combinators (RegisterSize (Auto), horner, mzipWithMRep)
 import           ZkFold.Symbolic.Data.Conditional (Conditional, bool)
 import           ZkFold.Symbolic.Data.Input       (SymbolicInput)
+import qualified ZkFold.Symbolic.Data.List        as L
 import           ZkFold.Symbolic.Data.List
-import qualified ZkFold.Symbolic.Data.List as L
 import           ZkFold.Symbolic.Data.Maybe       (Maybe, just)
-import ZkFold.Symbolic.MonadCircuit
-import Data.Proxy (Proxy(Proxy))
-import ZkFold.Base.Data.Package
-import ZkFold.Symbolic.Data.Combinators (mzipWithMRep, horner, RegisterSize (Auto))
-import ZkFold.Symbolic.Data.UInt (strictConv, UInt)
-import ZkFold.Base.Control.HApplicative (hpair)
-import qualified Data.List as LL
+import           ZkFold.Symbolic.Data.UInt        (UInt, strictConv)
+import           ZkFold.Symbolic.MonadCircuit
 
 data MerkleTree (d :: Natural) h = MerkleTree {
     mHash   :: (Context h) (Layout h)

From 7326555101372a564ff03a035a4629132b3de8dd Mon Sep 17 00:00:00 2001
From: Ann Hovanskaya <hovanja2011@gmail.com>
Date: Mon, 20 Jan 2025 11:17:17 +0300
Subject: [PATCH 11/15] functions

---
 .../src/ZkFold/Symbolic/Data/MerkleTree.hs    | 124 ++++++++++--------
 1 file changed, 69 insertions(+), 55 deletions(-)

diff --git a/symbolic-base/src/ZkFold/Symbolic/Data/MerkleTree.hs b/symbolic-base/src/ZkFold/Symbolic/Data/MerkleTree.hs
index bede8669..8350d598 100644
--- a/symbolic-base/src/ZkFold/Symbolic/Data/MerkleTree.hs
+++ b/symbolic-base/src/ZkFold/Symbolic/Data/MerkleTree.hs
@@ -5,12 +5,12 @@
 
 module ZkFold.Symbolic.Data.MerkleTree where
 
-import           Data.Foldable                    (Foldable (..), foldlM)
-import           Data.Functor.Rep                 (Representable, pureRep)
+import           Data.Foldable                    (foldlM)
+import           Data.Functor.Rep                 (Representable)
 import qualified Data.List                        as LL
 import           Data.Proxy                       (Proxy (Proxy))
 import           Data.Type.Equality               (type (~))
-import           GHC.Generics                     hiding (Rep, UInt)
+import           GHC.Generics                     hiding (Rep, UInt, from)
 import           GHC.TypeNats
 import           Prelude                          (Integer, Traversable, const, return, zip, ($), (.))
 import qualified Prelude                          as P
@@ -19,18 +19,21 @@ import           ZkFold.Base.Algebra.Basic.Class
 import           ZkFold.Base.Control.HApplicative (hpair)
 import           ZkFold.Base.Data.Package
 import qualified ZkFold.Base.Data.Vector          as V
-import           ZkFold.Base.Data.Vector
+import           ZkFold.Base.Data.Vector          hiding ((.:))
 import           ZkFold.Symbolic.Class
 import           ZkFold.Symbolic.Data.Bool        (Bool (..))
 import           ZkFold.Symbolic.Data.Class
-import           ZkFold.Symbolic.Data.Combinators (RegisterSize (Auto), horner, mzipWithMRep)
+import           ZkFold.Symbolic.Data.Combinators (RegisterSize (Auto), horner, mzipWithMRep, NumberOfRegisters, Iso (from), expansion)
 import           ZkFold.Symbolic.Data.Conditional (Conditional, bool)
 import           ZkFold.Symbolic.Data.Input       (SymbolicInput)
 import qualified ZkFold.Symbolic.Data.List        as L
 import           ZkFold.Symbolic.Data.List
-import           ZkFold.Symbolic.Data.Maybe       (Maybe, just)
+import           ZkFold.Symbolic.Data.Maybe       (just, nothing, fromMaybe)
+import qualified ZkFold.Symbolic.Data.Maybe       as M
 import           ZkFold.Symbolic.Data.UInt        (UInt, strictConv)
 import           ZkFold.Symbolic.MonadCircuit
+import ZkFold.Symbolic.Data.FieldElement (FieldElement(FieldElement, fromFieldElement))
+
 
 data MerkleTree (d :: Natural) h = MerkleTree {
     mHash   :: (Context h) (Layout h)
@@ -60,43 +63,50 @@ instance
   ) => Conditional (Bool c) (MerkleTree d h)
 
 -- | Finds an element satisfying the constraint
--- find :: forall h d c.
---   ( Conditional (Bool c) h
---   , SymbolicInput h
---   , Context h ~ c
---   , Foldable (List c))
---   => (h -> Bool c) -> MerkleTree d h -> Maybe c h
--- find p MerkleTree{..} = let n = nothing @h @c in
---   foldr (\i r -> maybe @h @_ @c (bool @(Bool c) n (just @c i) $ p i) (const r) r) n $ V.last mLevels
-
-newtype MerkleTreePath (d :: Natural) c = MerkleTreePath { mPath :: Vector d (Bool c)}
+find :: forall h d c.
+  ( Conditional (Bool c) h
+  , SymbolicInput h
+  , Context h ~ c
+  ) => (h -> Bool c) -> MerkleTree d h -> M.Maybe c h
+find p MerkleTree{..} =
+  let leaves = V.last mLevels
+      arr = L.filter p leaves
+  in bool (just $ L.head arr) nothing (L.null arr)
+
+newtype MerkleTreePath (d :: Natural) c = MerkleTreePath { mPath :: Vector (d-1) (Bool c)}
   deriving (Generic)
 
-instance ( Symbolic c, KnownNat d) => Conditional (Bool c) (MerkleTreePath d c)
+instance (Symbolic c, KnownNat (d-1)) => SymbolicData (MerkleTreePath d c)
+instance (Symbolic c, KnownNat (d-1)) => Conditional (Bool c) (MerkleTreePath d c)
 
 -- | Finds a path to an element satisfying the constraint
-findPath :: forall x c d.
-  ( Context x ~ c
-  , SymbolicOutput x
-  , Symbolic c
-  , Conditional (Bool c) (List c x)
-  , Conditional (Bool c) Integer
-  , KnownNat d)
-  => (x -> Bool (Context x)) -> MerkleTree d x -> Maybe c (MerkleTreePath d c)
-findPath p (MerkleTree _ mll) = just @c $ MerkleTreePath path
+findPath :: forall x c d n.
+  ( SymbolicOutput x
+  , Context x ~ c
+  , KnownNat d
+  , KnownNat (d-1)
+  , KnownNat (NumberOfRegisters (BaseField c) n Auto)
+  , NumberOfBits (BaseField c) ~ n
+  ) => (x -> Bool c) -> MerkleTree d x -> M.Maybe c (MerkleTreePath d c)
+findPath p mt@(MerkleTree _ nodes) = bool (nothing @_ @c) (just path) (p $ lookup @x @c mt path)
   where
-    ml = V.last mll
-    (ind', _) = helper (0, ml)
-
-    helper :: (Integer, List c x) -> (Integer , List c x)
-    helper (i, leaves) = let (l, ls) = L.uncons @c @x leaves
-      in bool (helper (i + 1, ls)) (i, leaves) (p l)
-
     d = knownNat @d :: Integer
+    pd = 2 P.^ (d-1) :: Integer
+    leaves = V.last nodes
+    idsL :: List c (UInt n Auto c) = LL.foldr ((.:) . fromConstant) L.emptyList [0..pd]
+    fe = fromFieldElement . from . L.head $ L.filter (p . (leaves L.!!)) idsL
 
-    path :: Vector d (Bool c)
-    path = unsafeToVector $ foldl (\nl ni -> Bool (embed @c (Par1 $ fromConstant ni )) : nl) []
-      $ P.map (\i -> mod (div ind' (2 P.^ i)) 2) [1 .. d]
+    path :: MerkleTreePath d c = MerkleTreePath . P.fmap Bool . unpack $ fromCircuitF fe $ \(Par1 e) -> do
+      ee <- expansion (P.fromIntegral d) e
+      return $ Comp1 (V.unsafeToVector @(d-1) $ P.map Par1 ee)
+
+indToPath :: forall c d.
+  ( Symbolic c
+  , KnownNat d
+  ) => c Par1 -> Vector (d - 1) (Bool c)
+indToPath e = P.fmap Bool . unpack $ fromCircuitF e $ \(Par1 i) -> do
+    ee <- expansion (knownNat @d) i
+    return $ Comp1 (V.unsafeToVector @(d-1) $ P.map Par1 ee)
 
 
 -- | Returns the element corresponding to a path
@@ -105,7 +115,7 @@ lookup :: forall x c d.
   , Context x ~ c
   , KnownNat (d - 1)
   , KnownNat d
-  ) => MerkleTree d x -> MerkleTreePath (d-1) c -> x
+  ) => MerkleTree d x -> MerkleTreePath d c -> x
 lookup (MerkleTree root nodes) (MerkleTreePath p) = xA
   where
     xP = leaf @c @x @d (V.last nodes) $ ind path
@@ -134,6 +144,7 @@ lookup (MerkleTree root nodes) (MerkleTreePath p) = xA
       _ <- mzipWithMRep (\wx wy -> constraint (($ wx) - ($ wy))) hd r
       return h1
 
+    path :: Vector (d - 1) (c Par1)
     path = P.fmap (\(Bool b) -> b) p
 
 
@@ -148,24 +159,27 @@ ind vb = fromCircuitF (pack vb) $ \vb' -> do
   return $ fromConstant b1n
 
 -- | Inserts an element at a specified position in a tree
-insert ::
-  ( Symbolic (Context a)
-  , Representable (Layout a))
-  => MerkleTree d a -> MerkleTreePath d c -> a -> MerkleTree d a
-insert (MerkleTree _ ls) _ _ = MerkleTree (embed $ pureRep zero) ls
+insert :: forall x c d.
+  () => MerkleTree d x -> MerkleTreePath d c -> x -> MerkleTree d x
+insert (MerkleTree _ _) (MerkleTreePath _) _ = P.undefined
+
+
+-- | Replaces an element satisfying the constraint. A composition of `findPath` and `insert`
+replace :: forall x c d n.
+  ( SymbolicOutput x
+  , Context x ~ c
+  , KnownNat d
+  , KnownNat (d-1)
+  , KnownNat (NumberOfRegisters (BaseField c) n Auto)
+  , NumberOfBits (BaseField c) ~ n
+  ) => (x -> Bool (Context x)) -> MerkleTree d x -> x -> MerkleTree d x
+replace p t = insert t (fromMaybe (P.error "That Leaf does not exist") $ findPath @x @c p t)
 
--- -- | Replaces an element satisfying the constraint. A composition of `findPath` and `insert`
--- replace :: (x -> Bool (Context x)) ->  MerkleTree d x -> x -> MerkleTree d x
 
 -- | Returns the next path in a tree
--- incrementPath :: forall c d.
---   ( KnownNat d
---   , Symbolic c
---   ) => MerkleTreePath d c -> MerkleTreePath d c
--- incrementPath (MerkleTreePath p) = MerkleTreePath (path $ ind p +one)
---   where
---     d = knownNat @d :: Integer
-
---     path :: Natural -> Vector d (Bool c)
---     path val = unsafeToVector $ foldl (\nl ni -> Bool (embed @c (Par1 $ fromConstant ni )) : nl) []
---       $ P.map (\i -> mod (div val (2 P.^ i)) 2) [1 .. d]
+incrementPath :: forall c d.
+  ( KnownNat d
+  , Symbolic c
+  ) => MerkleTreePath d c -> MerkleTreePath d c
+incrementPath (MerkleTreePath p) =
+  MerkleTreePath . indToPath @c $ fromFieldElement (FieldElement (ind $ P.fmap (\(Bool b) -> b) p) + one)
\ No newline at end of file

From 4a1e5be822604232c0e8f0de6a25ff61ebf4a6c0 Mon Sep 17 00:00:00 2001
From: hovanja2011 <hovanja2011@users.noreply.github.com>
Date: Mon, 20 Jan 2025 08:20:14 +0000
Subject: [PATCH 12/15] stylish-haskell auto-commit

---
 .../src/ZkFold/Symbolic/Data/MerkleTree.hs    | 43 ++++++++++---------
 1 file changed, 22 insertions(+), 21 deletions(-)

diff --git a/symbolic-base/src/ZkFold/Symbolic/Data/MerkleTree.hs b/symbolic-base/src/ZkFold/Symbolic/Data/MerkleTree.hs
index 8350d598..00e01df2 100644
--- a/symbolic-base/src/ZkFold/Symbolic/Data/MerkleTree.hs
+++ b/symbolic-base/src/ZkFold/Symbolic/Data/MerkleTree.hs
@@ -5,34 +5,35 @@
 
 module ZkFold.Symbolic.Data.MerkleTree where
 
-import           Data.Foldable                    (foldlM)
-import           Data.Functor.Rep                 (Representable)
-import qualified Data.List                        as LL
-import           Data.Proxy                       (Proxy (Proxy))
-import           Data.Type.Equality               (type (~))
-import           GHC.Generics                     hiding (Rep, UInt, from)
+import           Data.Foldable                     (foldlM)
+import           Data.Functor.Rep                  (Representable)
+import qualified Data.List                         as LL
+import           Data.Proxy                        (Proxy (Proxy))
+import           Data.Type.Equality                (type (~))
+import           GHC.Generics                      hiding (Rep, UInt, from)
 import           GHC.TypeNats
-import           Prelude                          (Integer, Traversable, const, return, zip, ($), (.))
-import qualified Prelude                          as P
+import           Prelude                           (Integer, Traversable, const, return, zip, ($), (.))
+import qualified Prelude                           as P
 
 import           ZkFold.Base.Algebra.Basic.Class
-import           ZkFold.Base.Control.HApplicative (hpair)
+import           ZkFold.Base.Control.HApplicative  (hpair)
 import           ZkFold.Base.Data.Package
-import qualified ZkFold.Base.Data.Vector          as V
-import           ZkFold.Base.Data.Vector          hiding ((.:))
+import qualified ZkFold.Base.Data.Vector           as V
+import           ZkFold.Base.Data.Vector           hiding ((.:))
 import           ZkFold.Symbolic.Class
-import           ZkFold.Symbolic.Data.Bool        (Bool (..))
+import           ZkFold.Symbolic.Data.Bool         (Bool (..))
 import           ZkFold.Symbolic.Data.Class
-import           ZkFold.Symbolic.Data.Combinators (RegisterSize (Auto), horner, mzipWithMRep, NumberOfRegisters, Iso (from), expansion)
-import           ZkFold.Symbolic.Data.Conditional (Conditional, bool)
-import           ZkFold.Symbolic.Data.Input       (SymbolicInput)
-import qualified ZkFold.Symbolic.Data.List        as L
+import           ZkFold.Symbolic.Data.Combinators  (Iso (from), NumberOfRegisters, RegisterSize (Auto), expansion,
+                                                    horner, mzipWithMRep)
+import           ZkFold.Symbolic.Data.Conditional  (Conditional, bool)
+import           ZkFold.Symbolic.Data.FieldElement (FieldElement (FieldElement, fromFieldElement))
+import           ZkFold.Symbolic.Data.Input        (SymbolicInput)
+import qualified ZkFold.Symbolic.Data.List         as L
 import           ZkFold.Symbolic.Data.List
-import           ZkFold.Symbolic.Data.Maybe       (just, nothing, fromMaybe)
-import qualified ZkFold.Symbolic.Data.Maybe       as M
-import           ZkFold.Symbolic.Data.UInt        (UInt, strictConv)
+import qualified ZkFold.Symbolic.Data.Maybe        as M
+import           ZkFold.Symbolic.Data.Maybe        (fromMaybe, just, nothing)
+import           ZkFold.Symbolic.Data.UInt         (UInt, strictConv)
 import           ZkFold.Symbolic.MonadCircuit
-import ZkFold.Symbolic.Data.FieldElement (FieldElement(FieldElement, fromFieldElement))
 
 
 data MerkleTree (d :: Natural) h = MerkleTree {
@@ -182,4 +183,4 @@ incrementPath :: forall c d.
   , Symbolic c
   ) => MerkleTreePath d c -> MerkleTreePath d c
 incrementPath (MerkleTreePath p) =
-  MerkleTreePath . indToPath @c $ fromFieldElement (FieldElement (ind $ P.fmap (\(Bool b) -> b) p) + one)
\ No newline at end of file
+  MerkleTreePath . indToPath @c $ fromFieldElement (FieldElement (ind $ P.fmap (\(Bool b) -> b) p) + one)

From 9da3619e510d48f4eccf8f27e2c8f1e40163e6e5 Mon Sep 17 00:00:00 2001
From: Ann Hovanskaya <hovanja2011@gmail.com>
Date: Mon, 27 Jan 2025 16:39:17 +0300
Subject: [PATCH 13/15] last function

---
 .../src/ZkFold/Symbolic/Data/List.hs          | 20 +++++
 .../src/ZkFold/Symbolic/Data/MerkleTree.hs    | 90 ++++++++++++-------
 2 files changed, 80 insertions(+), 30 deletions(-)

diff --git a/symbolic-base/src/ZkFold/Symbolic/Data/List.hs b/symbolic-base/src/ZkFold/Symbolic/Data/List.hs
index bbfd9b4d..f2f6077a 100644
--- a/symbolic-base/src/ZkFold/Symbolic/Data/List.hs
+++ b/symbolic-base/src/ZkFold/Symbolic/Data/List.hs
@@ -246,3 +246,23 @@ concat ::
   List c (List c x) -> List c x
 concat xs = reverse $
   foldl (Morph \(ys, x :: List s (Switch s x)) -> revapp x ys) emptyList xs
+
+findIndex ::
+  forall x c n.
+  (SymbolicOutput x, Context x ~ c, SymbolicFold c) =>
+  (KnownNat n, KnownRegisters c n Auto
+  ) => MorphFrom c x (Bool c) -> List c x -> UInt n Auto c
+findIndex p xs = snd $ foldl (Morph \((m :: UInt n Auto s, y :: UInt n Auto s), x :: Switch s x) ->
+  (m + one, ifThenElse (p @ x :: Bool s) m y))
+  (zero :: UInt n Auto c, zero) xs
+
+insert ::
+  forall x c n.
+  (SymbolicOutput x, Context x ~ c, SymbolicFold c) =>
+  (KnownNat n, KnownRegisters c n Auto) =>
+  List c x -> UInt n Auto c -> x -> List c x
+insert xs n xi =
+  let (_, _, res) = foldr (Morph \(a :: Switch s x, (n' :: UInt n Auto s, xi', l')) ->
+        (n' - one, xi', ifThenElse (n' == zero :: Bool s) (xi' .: l') (a .: l'))) (n, xi, emptyList) xs
+   in res
+
diff --git a/symbolic-base/src/ZkFold/Symbolic/Data/MerkleTree.hs b/symbolic-base/src/ZkFold/Symbolic/Data/MerkleTree.hs
index 00e01df2..4a72acb6 100644
--- a/symbolic-base/src/ZkFold/Symbolic/Data/MerkleTree.hs
+++ b/symbolic-base/src/ZkFold/Symbolic/Data/MerkleTree.hs
@@ -6,13 +6,13 @@
 module ZkFold.Symbolic.Data.MerkleTree where
 
 import           Data.Foldable                     (foldlM)
-import           Data.Functor.Rep                  (Representable)
+import           Data.Functor.Rep                  (Representable, pureRep)
 import qualified Data.List                         as LL
 import           Data.Proxy                        (Proxy (Proxy))
 import           Data.Type.Equality                (type (~))
 import           GHC.Generics                      hiding (Rep, UInt, from)
 import           GHC.TypeNats
-import           Prelude                           (Integer, Traversable, const, return, zip, ($), (.))
+import           Prelude                           (Traversable, const, return, zip, ($), (.))
 import qualified Prelude                           as P
 
 import           ZkFold.Base.Algebra.Basic.Class
@@ -24,7 +24,7 @@ import           ZkFold.Symbolic.Class
 import           ZkFold.Symbolic.Data.Bool         (Bool (..))
 import           ZkFold.Symbolic.Data.Class
 import           ZkFold.Symbolic.Data.Combinators  (Iso (from), NumberOfRegisters, RegisterSize (Auto), expansion,
-                                                    horner, mzipWithMRep)
+                                                    horner, mzipWithMRep, KnownRegisters)
 import           ZkFold.Symbolic.Data.Conditional  (Conditional, bool)
 import           ZkFold.Symbolic.Data.FieldElement (FieldElement (FieldElement, fromFieldElement))
 import           ZkFold.Symbolic.Data.Input        (SymbolicInput)
@@ -32,8 +32,10 @@ import qualified ZkFold.Symbolic.Data.List         as L
 import           ZkFold.Symbolic.Data.List
 import qualified ZkFold.Symbolic.Data.Maybe        as M
 import           ZkFold.Symbolic.Data.Maybe        (fromMaybe, just, nothing)
-import           ZkFold.Symbolic.Data.UInt         (UInt, strictConv)
+import           ZkFold.Symbolic.Data.UInt         (UInt (..), strictConv)
 import           ZkFold.Symbolic.MonadCircuit
+import ZkFold.Symbolic.Fold (SymbolicFold)
+import ZkFold.Symbolic.Data.Morph
 
 
 data MerkleTree (d :: Natural) h = MerkleTree {
@@ -54,21 +56,13 @@ hashAux (Par1 b) h g = do
 instance (SymbolicData h, KnownNat d) => SymbolicData (MerkleTree d h)
 instance (SymbolicInput h, KnownNat d) => SymbolicInput (MerkleTree d h)
 
-instance
-  ( Symbolic c
-  , Context h ~ c
-  , Conditional (Bool c) (List c h)
-  , Traversable (Layout h)
-  , Representable (Layout h)
-  , KnownNat d
-  ) => Conditional (Bool c) (MerkleTree d h)
-
 -- | Finds an element satisfying the constraint
 find :: forall h d c.
   ( Conditional (Bool c) h
   , SymbolicInput h
   , Context h ~ c
-  ) => (h -> Bool c) -> MerkleTree d h -> M.Maybe c h
+  , SymbolicFold c
+  ) => MorphFrom c h (Bool c) -> MerkleTree d h -> M.Maybe c h
 find p MerkleTree{..} =
   let leaves = V.last mLevels
       arr = L.filter p leaves
@@ -88,18 +82,12 @@ findPath :: forall x c d n.
   , KnownNat (d-1)
   , KnownNat (NumberOfRegisters (BaseField c) n Auto)
   , NumberOfBits (BaseField c) ~ n
-  ) => (x -> Bool c) -> MerkleTree d x -> M.Maybe c (MerkleTreePath d c)
-findPath p mt@(MerkleTree _ nodes) = bool (nothing @_ @c) (just path) (p $ lookup @x @c mt path)
+  , SymbolicFold c, KnownRegisters c d Auto
+  ) => MorphFrom c x (Bool c) -> MerkleTree d x -> M.Maybe c (MerkleTreePath d c)
+findPath p mt@(MerkleTree _ nodes) =  bool (nothing @_ @c) (just path) (p @ lookup @x @c mt path :: Bool c)
   where
-    d = knownNat @d :: Integer
-    pd = 2 P.^ (d-1) :: Integer
     leaves = V.last nodes
-    idsL :: List c (UInt n Auto c) = LL.foldr ((.:) . fromConstant) L.emptyList [0..pd]
-    fe = fromFieldElement . from . L.head $ L.filter (p . (leaves L.!!)) idsL
-
-    path :: MerkleTreePath d c = MerkleTreePath . P.fmap Bool . unpack $ fromCircuitF fe $ \(Par1 e) -> do
-      ee <- expansion (P.fromIntegral d) e
-      return $ Comp1 (V.unsafeToVector @(d-1) $ P.map Par1 ee)
+    path = MerkleTreePath . indToPath @c . fromFieldElement . from $ findIndex p leaves
 
 indToPath :: forall c d.
   ( Symbolic c
@@ -116,6 +104,7 @@ lookup :: forall x c d.
   , Context x ~ c
   , KnownNat (d - 1)
   , KnownNat d
+  , SymbolicFold c, KnownRegisters c d Auto
   ) => MerkleTree d x -> MerkleTreePath d c -> x
 lookup (MerkleTree root nodes) (MerkleTreePath p) = xA
   where
@@ -149,7 +138,9 @@ lookup (MerkleTree root nodes) (MerkleTreePath p) = xA
     path = P.fmap (\(Bool b) -> b) p
 
 
-leaf :: forall c x d. (SymbolicOutput x, Context x ~ c, KnownNat d) => List c x -> c Par1 -> x
+leaf :: forall c x d.
+  (SymbolicOutput x, SymbolicFold c, KnownRegisters c d Auto, Context x ~ c, KnownNat d
+  ) => List c x -> c Par1 -> x
 leaf l i = let num = strictConv @_ @(UInt d Auto c) i in l L.!! num
 
 
@@ -160,10 +151,48 @@ ind vb = fromCircuitF (pack vb) $ \vb' -> do
   return $ fromConstant b1n
 
 -- | Inserts an element at a specified position in a tree
-insert :: forall x c d.
-  () => MerkleTree d x -> MerkleTreePath d c -> x -> MerkleTree d x
-insert (MerkleTree _ _) (MerkleTreePath _) _ = P.undefined
+insertLeaf :: forall x c d.
+  ( SymbolicOutput x
+  , Context x ~ c
+  , KnownNat (d - 1)
+  , KnownNat d
+  , SymbolicFold c
+  , KnownRegisters c d Auto
+  ) => MerkleTree d x -> MerkleTreePath d c -> x -> MerkleTree d x
+insertLeaf (MerkleTree root nodes) (MerkleTreePath p) xI = MerkleTree root (V.unsafeToVector z3)
+  where
+    inits = V.unsafeToVector @(d-1) $ LL.unfoldr (\v -> if LL.null v then P.Nothing else P.Just (ind @_ @c (V.unsafeToVector v), LL.init v)) (V.fromVector path)
+
+    cinds :: Vector (d-1) (c Par1)
+    cinds = unpacked $ fromCircuit2F (pack path) (pack inits) $ \ps' is' -> do
+      let ps = P.fmap unPar1 (unComp1 ps')
+          is = V.unsafeToVector $ fromConstant @(BaseField c) zero : (P.init . V.fromVector $ P.fmap unPar1 (unComp1 is'))
+      mzipWithMRep (\wp wi -> newAssigned (one - ($ wp) + ($ wi)*(one + one))) ps is
+
+    inds = V.unsafeToVector @(d-1) $ P.zipWith (\l i -> arithmetize (leaf @c @x @d l i) Proxy) (V.fromVector $ V.tail nodes) (V.fromVector cinds)
+
+    preimage :: Vector (d - 1) (c (Layout x))
+    preimage = unpack $ fromCircuit3F (pack inds) (pack path) (arithmetize xI Proxy) $ \ g p' h' -> do
+      let gs = V.fromVector $ unComp1 g
+          bs = V.fromVector $ unComp1 p'
+          h1 = h'
+      hd <- helper h1 (zip gs bs)
+      return $ Comp1 $ V.unsafeToVector @(d-1) hd
+
+    helper :: forall i m a w f. (MonadCircuit i a w m, Representable f, Traversable f) => f i -> [(f i, Par1 i)] -> m [f i]
+    helper _ [] = return []
+    helper h (pi:ps) = do
+      let (g, b) = pi
+      hN <- hashAux b h g
+      (hN :) P.<$> helper hN ps
+
+    path :: Vector (d - 1) (c Par1)
+    path = P.fmap (\(Bool b) -> b) p
 
+    z3 = P.zipWith3 (\l mtp xi -> L.insert l mtp (restore @_ @c $ const (xi, pureRep zero)))
+          (V.fromVector nodes)
+          (P.map (strictConv @_ @(UInt d Auto c)) $ V.fromVector inits)
+          (V.fromVector preimage)
 
 -- | Replaces an element satisfying the constraint. A composition of `findPath` and `insert`
 replace :: forall x c d n.
@@ -173,8 +202,9 @@ replace :: forall x c d n.
   , KnownNat (d-1)
   , KnownNat (NumberOfRegisters (BaseField c) n Auto)
   , NumberOfBits (BaseField c) ~ n
-  ) => (x -> Bool (Context x)) -> MerkleTree d x -> x -> MerkleTree d x
-replace p t = insert t (fromMaybe (P.error "That Leaf does not exist") $ findPath @x @c p t)
+  , SymbolicFold c, KnownRegisters c d Auto
+  ) => MorphFrom c x (Bool c) -> MerkleTree d x -> x -> MerkleTree d x
+replace p t = insertLeaf t (fromMaybe (P.error "That Leaf does not exist") $ findPath @x @c p t)
 
 
 -- | Returns the next path in a tree

From b3e03d2e2f9af485f3ddfb98cfdafa22a9584658 Mon Sep 17 00:00:00 2001
From: Ann Hovanskaya <hovanja2011@gmail.com>
Date: Mon, 27 Jan 2025 18:03:23 +0300
Subject: [PATCH 14/15] changes

---
 .../src/ZkFold/Symbolic/Data/MerkleTree.hs    | 28 ++++++++++---------
 1 file changed, 15 insertions(+), 13 deletions(-)

diff --git a/symbolic-base/src/ZkFold/Symbolic/Data/MerkleTree.hs b/symbolic-base/src/ZkFold/Symbolic/Data/MerkleTree.hs
index 4a72acb6..8d5bcc0d 100644
--- a/symbolic-base/src/ZkFold/Symbolic/Data/MerkleTree.hs
+++ b/symbolic-base/src/ZkFold/Symbolic/Data/MerkleTree.hs
@@ -110,15 +110,17 @@ lookup (MerkleTree root nodes) (MerkleTreePath p) = xA
   where
     xP = leaf @c @x @d (V.last nodes) $ ind path
 
-    inits = V.unsafeToVector @(d-1) $ LL.unfoldr (\v -> if LL.null v then P.Nothing else P.Just (ind @_ @c (V.unsafeToVector v), LL.init v)) (V.fromVector path)
+    inits = V.unsafeToVector @(d-2) $
+              LL.unfoldr (\v -> let initV = LL.init v
+                                 in if LL.null initV then P.Nothing else P.Just (ind @_ @c (V.unsafeToVector initV), initV)) $ V.fromVector path
 
     cinds :: Vector (d-1) (c Par1)
     cinds = unpacked $ fromCircuit2F (pack path) (pack inits) $ \ps' is' -> do
       let ps = P.fmap unPar1 (unComp1 ps')
-          is = V.unsafeToVector $ fromConstant @(BaseField c) zero : (P.init . V.fromVector $ P.fmap unPar1 (unComp1 is'))
+          is = V.unsafeToVector @(d-1) (fromConstant @(BaseField c) zero : (V.fromVector . P.fmap unPar1 $ unComp1 is'))
       mzipWithMRep (\wp wi -> newAssigned (one - ($ wp) + ($ wi)*(one + one))) ps is
 
-    inds = V.unsafeToVector @(d-1) $ P.zipWith (\l i -> arithmetize (leaf @c @x @d l i) Proxy) (V.fromVector $ V.tail nodes) (V.fromVector cinds)
+    pairs = V.unsafeToVector @(d-1) $ P.zipWith (\l i -> arithmetize (leaf @c @x @d l i) Proxy) (V.fromVector $ V.tail nodes) (V.fromVector cinds)
 
     xA = restore @x @c $ const (preimage , payload xP Proxy)
 
@@ -126,7 +128,7 @@ lookup (MerkleTree root nodes) (MerkleTreePath p) = xA
     rootAndH1 = hpair root (arithmetize xP Proxy)
 
     preimage :: c (Layout x)
-    preimage = fromCircuit3F (pack inds) (pack path) rootAndH1 $ \ g p' r' -> do
+    preimage = fromCircuit3F (pack pairs) (pack path) rootAndH1 $ \ g p' r' -> do
       let gs = V.fromVector $ unComp1 g
           bs = V.fromVector $ unComp1 p'
           (r :*: h1) = r'
@@ -159,23 +161,24 @@ insertLeaf :: forall x c d.
   , SymbolicFold c
   , KnownRegisters c d Auto
   ) => MerkleTree d x -> MerkleTreePath d c -> x -> MerkleTree d x
-insertLeaf (MerkleTree root nodes) (MerkleTreePath p) xI = MerkleTree root (V.unsafeToVector z3)
+insertLeaf (MerkleTree _ nodes) (MerkleTreePath p) xI = MerkleTree (V.head preimage) (V.unsafeToVector z3)
   where
-    inits = V.unsafeToVector @(d-1) $ LL.unfoldr (\v -> if LL.null v then P.Nothing else P.Just (ind @_ @c (V.unsafeToVector v), LL.init v)) (V.fromVector path)
+    inits = V.unsafeToVector @(d-2) $
+              LL.unfoldr (\v -> let initV = LL.init v
+                                 in if LL.null initV then P.Nothing else P.Just (ind @_ @c (V.unsafeToVector initV), initV)) $ V.fromVector path
 
     cinds :: Vector (d-1) (c Par1)
     cinds = unpacked $ fromCircuit2F (pack path) (pack inits) $ \ps' is' -> do
       let ps = P.fmap unPar1 (unComp1 ps')
-          is = V.unsafeToVector $ fromConstant @(BaseField c) zero : (P.init . V.fromVector $ P.fmap unPar1 (unComp1 is'))
+          is = V.unsafeToVector @(d-1) (fromConstant @(BaseField c) zero : (V.fromVector . P.fmap unPar1 $ unComp1 is'))
       mzipWithMRep (\wp wi -> newAssigned (one - ($ wp) + ($ wi)*(one + one))) ps is
 
-    inds = V.unsafeToVector @(d-1) $ P.zipWith (\l i -> arithmetize (leaf @c @x @d l i) Proxy) (V.fromVector $ V.tail nodes) (V.fromVector cinds)
+    pairs = V.unsafeToVector @(d-1) $ P.zipWith (\l i -> arithmetize (leaf @c @x @d l i) Proxy) (V.fromVector $ V.tail nodes) (V.fromVector cinds)
 
     preimage :: Vector (d - 1) (c (Layout x))
-    preimage = unpack $ fromCircuit3F (pack inds) (pack path) (arithmetize xI Proxy) $ \ g p' h' -> do
+    preimage = unpack $ fromCircuit3F (pack pairs) (pack path) (arithmetize xI Proxy) $ \ g p' h1 -> do
       let gs = V.fromVector $ unComp1 g
           bs = V.fromVector $ unComp1 p'
-          h1 = h'
       hd <- helper h1 (zip gs bs)
       return $ Comp1 $ V.unsafeToVector @(d-1) hd
 
@@ -191,8 +194,8 @@ insertLeaf (MerkleTree root nodes) (MerkleTreePath p) xI = MerkleTree root (V.un
 
     z3 = P.zipWith3 (\l mtp xi -> L.insert l mtp (restore @_ @c $ const (xi, pureRep zero)))
           (V.fromVector nodes)
-          (P.map (strictConv @_ @(UInt d Auto c)) $ V.fromVector inits)
-          (V.fromVector preimage)
+          (P.map (strictConv @_ @(UInt d Auto c)) ([embed $ Par1 zero] P.++ V.fromVector inits P.++ [ind path]))
+          (V.fromVector preimage P.<> [arithmetize xI Proxy])
 
 -- | Replaces an element satisfying the constraint. A composition of `findPath` and `insert`
 replace :: forall x c d n.
@@ -206,7 +209,6 @@ replace :: forall x c d n.
   ) => MorphFrom c x (Bool c) -> MerkleTree d x -> x -> MerkleTree d x
 replace p t = insertLeaf t (fromMaybe (P.error "That Leaf does not exist") $ findPath @x @c p t)
 
-
 -- | Returns the next path in a tree
 incrementPath :: forall c d.
   ( KnownNat d

From 71cdcec722c51b201178a682939fef933f71077b Mon Sep 17 00:00:00 2001
From: hovanja2011 <hovanja2011@users.noreply.github.com>
Date: Mon, 27 Jan 2025 15:06:20 +0000
Subject: [PATCH 15/15] stylish-haskell auto-commit

---
 symbolic-base/src/ZkFold/Symbolic/Data/MerkleTree.hs | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/symbolic-base/src/ZkFold/Symbolic/Data/MerkleTree.hs b/symbolic-base/src/ZkFold/Symbolic/Data/MerkleTree.hs
index 8d5bcc0d..c3fb5ca3 100644
--- a/symbolic-base/src/ZkFold/Symbolic/Data/MerkleTree.hs
+++ b/symbolic-base/src/ZkFold/Symbolic/Data/MerkleTree.hs
@@ -23,8 +23,8 @@ import           ZkFold.Base.Data.Vector           hiding ((.:))
 import           ZkFold.Symbolic.Class
 import           ZkFold.Symbolic.Data.Bool         (Bool (..))
 import           ZkFold.Symbolic.Data.Class
-import           ZkFold.Symbolic.Data.Combinators  (Iso (from), NumberOfRegisters, RegisterSize (Auto), expansion,
-                                                    horner, mzipWithMRep, KnownRegisters)
+import           ZkFold.Symbolic.Data.Combinators  (Iso (from), KnownRegisters, NumberOfRegisters, RegisterSize (Auto),
+                                                    expansion, horner, mzipWithMRep)
 import           ZkFold.Symbolic.Data.Conditional  (Conditional, bool)
 import           ZkFold.Symbolic.Data.FieldElement (FieldElement (FieldElement, fromFieldElement))
 import           ZkFold.Symbolic.Data.Input        (SymbolicInput)
@@ -32,10 +32,10 @@ import qualified ZkFold.Symbolic.Data.List         as L
 import           ZkFold.Symbolic.Data.List
 import qualified ZkFold.Symbolic.Data.Maybe        as M
 import           ZkFold.Symbolic.Data.Maybe        (fromMaybe, just, nothing)
+import           ZkFold.Symbolic.Data.Morph
 import           ZkFold.Symbolic.Data.UInt         (UInt (..), strictConv)
+import           ZkFold.Symbolic.Fold              (SymbolicFold)
 import           ZkFold.Symbolic.MonadCircuit
-import ZkFold.Symbolic.Fold (SymbolicFold)
-import ZkFold.Symbolic.Data.Morph
 
 
 data MerkleTree (d :: Natural) h = MerkleTree {