diff --git a/symbolic-base/src/ZkFold/Data/Eq.hs b/symbolic-base/src/ZkFold/Data/Eq.hs
index 4e5eb0b81..fe758c0ea 100644
--- a/symbolic-base/src/ZkFold/Data/Eq.hs
+++ b/symbolic-base/src/ZkFold/Data/Eq.hs
@@ -14,6 +14,7 @@ import qualified Data.Ord as Haskell
 import Data.Ratio (Rational)
 import Data.String (String)
 import Data.Type.Equality (type (~))
+import GHC.Generics ((:.:))
 import qualified GHC.Generics as G
 import Numeric.Natural (Natural)
 import Prelude (Integer)
@@ -28,14 +29,18 @@ class BoolType (BooleanOf a) => Eq a where
   (==) :: a -> a -> BooleanOf a
   default (==)
     :: (G.Generic a, GEq (G.Rep a), BooleanOf a ~ GBooleanOf (G.Rep a))
-    => a -> a -> BooleanOf a
+    => a
+    -> a
+    -> BooleanOf a
   x == y = geq (G.from x) (G.from y)
 
   infix 4 /=
   (/=) :: a -> a -> BooleanOf a
   default (/=)
     :: (G.Generic a, GEq (G.Rep a), BooleanOf a ~ GBooleanOf (G.Rep a))
-    => a -> a -> BooleanOf a
+    => a
+    -> a
+    -> BooleanOf a
   x /= y = gneq (G.from x) (G.from y)
 
 elem :: (Eq a, Foldable t) => a -> t a -> BooleanOf a
@@ -74,6 +79,8 @@ instance Eq (f a) => Eq (G.Rec1 f a)
 
 instance Eq (f a) => Eq (G.M1 i c f a)
 
+instance Eq (f (g a)) => Eq ((:.:) f g a)
+
 instance {-# OVERLAPPING #-} Eq (f a) => Eq ((f G.:*: G.U1) a) where
   (x G.:*: _) == (y G.:*: _) = x == y
   (x G.:*: _) /= (y G.:*: _) = x /= y
diff --git a/symbolic-base/src/ZkFold/Symbolic/Data/MerkleTree.hs b/symbolic-base/src/ZkFold/Symbolic/Data/MerkleTree.hs
index d5d146df0..88741e1a1 100644
--- a/symbolic-base/src/ZkFold/Symbolic/Data/MerkleTree.hs
+++ b/symbolic-base/src/ZkFold/Symbolic/Data/MerkleTree.hs
@@ -7,6 +7,7 @@ module ZkFold.Symbolic.Data.MerkleTree (
   emptyTree,
   fromLeaves,
   toLeaves,
+  MerklePath,
   merklePath,
   rootOnReplace,
   MerkleEntry (..),
@@ -111,7 +112,9 @@ type Index d = Vector (d - 1) :.: Bool
 
 merklePath
   :: (Symbolic c, KnownNat (d - 1))
-  => MerkleTree d c -> Index d c -> MerklePath d c
+  => MerkleTree d c
+  -> Index d c
+  -> MerklePath d c
 merklePath MerkleTree {..} position =
   let baseTree = Base.MerkleTree (toBaseHash mHash) (toBaseLeaves mLeaves)
       path = fromBaseHash <$> Base.merkleProve' baseTree (toBasePosition position)
@@ -130,7 +133,9 @@ data MerkleEntry d c = MerkleEntry
 contains
   :: forall d c
    . (Symbolic c, KnownNat (d - 1))
-  => MerkleTree d c -> MerkleEntry d c -> Bool c
+  => MerkleTree d c
+  -> MerkleEntry d c
+  -> Bool c
 tree `contains` MerkleEntry {..} =
   rootOnReplace (merklePath tree position) value == mHash tree
 
@@ -139,7 +144,9 @@ type Bool' c = BooleanOf (IntegralOf (WitnessField c))
 (!!)
   :: forall d c
    . (Symbolic c, KnownNat (d - 1))
-  => MerkleTree d c -> Index d c -> FieldElement c
+  => MerkleTree d c
+  -> Index d c
+  -> FieldElement c
 tree !! position =
   assert (\value -> tree `contains` MerkleEntry {..}) $
     fromBaseHash $
@@ -172,7 +179,9 @@ search pred tree =
   recSearch
     :: forall n b a
      . (BoolType b, Conditional b a)
-    => (a -> b) -> Vector (2 ^ n) a -> (b, Vector n b, a)
+    => (a -> b)
+    -> Vector (2 ^ n) a
+    -> (b, Vector n b, a)
   recSearch p d =
     let (b, i, x) = doSearch (toV d)
      in (b, unsafeToVector i, x)
@@ -228,7 +237,9 @@ elemIndex elem = findIndex (== elem)
 
 lookup
   :: (Symbolic c, KnownNat (d - 1))
-  => MerkleTree d c -> Index d c -> FieldElement c
+  => MerkleTree d c
+  -> Index d c
+  -> FieldElement c
 lookup = (!!)
 
 search'
@@ -242,7 +253,9 @@ type KnownMerkleTree d = (KnownNat (d - 1), KnownNat (Base.MerkleTreeSize d))
 
 replace
   :: (Symbolic c, KnownMerkleTree d)
-  => MerkleEntry d c -> MerkleTree d c -> MerkleTree d c
+  => MerkleEntry d c
+  -> MerkleTree d c
+  -> MerkleTree d c
 replace entry@MerkleEntry {..} =
   assert (`contains` entry)
     . unconstrainedFromLeaves
@@ -252,12 +265,18 @@ replace entry@MerkleEntry {..} =
  where
   replacer
     :: (FromConstant n i, Eq i, Conditional (BooleanOf i) a)
-    => (i, a) -> n -> a -> a
+    => (i, a)
+    -> n
+    -> a
+    -> a
   replacer (i, a') n = ifThenElse (i == fromConstant n) a'
 
 replaceAt
   :: (Symbolic c, KnownMerkleTree d)
-  => Index d c -> FieldElement c -> MerkleTree d c -> MerkleTree d c
+  => Index d c
+  -> FieldElement c
+  -> MerkleTree d c
+  -> MerkleTree d c
 replaceAt position value = replace MerkleEntry {..}
 
 ---------------------------- conversion functions ------------------------------
diff --git a/symbolic-ledger/src/ZkFold/Symbolic/Ledger/Types.hs b/symbolic-ledger/src/ZkFold/Symbolic/Ledger/Types.hs
index b6c4e4dec..393d57787 100644
--- a/symbolic-ledger/src/ZkFold/Symbolic/Ledger/Types.hs
+++ b/symbolic-ledger/src/ZkFold/Symbolic/Ledger/Types.hs
@@ -3,69 +3,54 @@
 module ZkFold.Symbolic.Ledger.Types (
   module ZkFold.Symbolic.Ledger.Types.Address,
   module ZkFold.Symbolic.Ledger.Types.Hash,
-  module ZkFold.Symbolic.Ledger.Types.Interval,
-  module ZkFold.Symbolic.Ledger.Types.Output,
+  module ZkFold.Symbolic.Ledger.Types.State,
   module ZkFold.Symbolic.Ledger.Types.Transaction,
-  module ZkFold.Symbolic.Ledger.Types.Root,
-  module ZkFold.Symbolic.Ledger.Types.Datum,
   module ZkFold.Symbolic.Ledger.Types.Value,
-  module ZkFold.Symbolic.Ledger.Types.DataAvailability,
-  module ZkFold.Symbolic.Ledger.Types.Circuit,
-  Signature,
+  SignatureTransaction,
+  SignatureTransactionBatch,
+  SignatureState,
 ) where
 
--- Re-exports
-
-import GHC.Generics ((:*:))
-import GHC.TypeLits (KnownNat)
+import GHC.Generics ((:.:))
+import GHC.TypeNats (KnownNat, type (-))
+import ZkFold.Data.MerkleTree (MerkleTreeSize)
+import ZkFold.Data.Vector (Vector)
 import ZkFold.Symbolic.Class (Symbolic (..))
-import ZkFold.Symbolic.Data.Combinators (
-  Ceil,
-  GetRegisterSize,
-  KnownRegisters,
-  RegisterSize (Auto),
- )
+import ZkFold.Symbolic.Data.FieldElement (FieldElement)
 import ZkFold.Symbolic.Data.Hash (Hashable)
-import ZkFold.Symbolic.Data.UInt (OrdWord)
-import ZkFold.Symbolic.Fold (SymbolicFold)
 
 import ZkFold.Symbolic.Ledger.Types.Address
-import ZkFold.Symbolic.Ledger.Types.Circuit
-import ZkFold.Symbolic.Ledger.Types.DataAvailability
-import ZkFold.Symbolic.Ledger.Types.Datum
 import ZkFold.Symbolic.Ledger.Types.Hash
-import ZkFold.Symbolic.Ledger.Types.Interval
-import ZkFold.Symbolic.Ledger.Types.Output
-import ZkFold.Symbolic.Ledger.Types.Root
+import ZkFold.Symbolic.Ledger.Types.State
 import ZkFold.Symbolic.Ledger.Types.Transaction
 import ZkFold.Symbolic.Ledger.Types.Value
 
-{-
-    zkFold's ledger is a UTXO-based ledger. The architecture of the ledger is mostly similar to the Cardano ledger with some key differences:
-
-    - Some transaction data is private and is kept off-chain by the concerned parties.
-
-    - All UTXOs are locked by contracts.
+type SignatureTransaction ud i o a context =
+  ( Symbolic context
+  , KnownRegistersAssetQuantity context
+  , KnownNat i
+  , KnownNat a
+  , KnownNat (ud - 1)
+  , KnownNat (MerkleTreeSize ud)
+  , Hashable (HashSimple context) (Transaction i o a context)
+  , forall s. Hashable (HashSimple s) (Transaction i o a s)
+  , Hashable (HashSimple context) (UTxO a context)
+  , forall s. Hashable (HashSimple s) (UTxO a s)
+  )
 
-    - Stake delegation and governance is implemented through contracts.
--}
+type SignatureTransactionBatch ud i o a t context =
+  ( SignatureTransaction ud i o a context
+  , Hashable (HashSimple context) (TransactionBatch i o a t context)
+  , forall s. Hashable (HashSimple s) (TransactionBatch i o a t s)
+  )
 
-type Signature context =
-  ( KnownRegistersAssetQuantity context
-  , KnownRegistersOutputIndex context
-  , KnownRegisters context 11 Auto
-  , SymbolicFold context
-  , KnownNat (Ceil (GetRegisterSize (BaseField context) 11 Auto) OrdWord)
-  , -- TODO: Can we derive 'Hashable h' based on constituents (using generic)?
-    -- TODO: Remove @ImpredicativeTypes@ extension from symbolic-ledger once above 'Hashable' issue is sorted.
-    Hashable (HashSimple context) (AssetValues context)
-  , Hashable (HashSimple context) (Transaction context)
-  , Hashable (HashSimple context) (TransactionBatch context)
-  , Hashable (HashSimple context) (TransactionBatchData context)
-  , Hashable (HashSimple context) ((Circuit :*: DAIndex :*: DAType) context)
-  , forall s. Hashable (HashSimple s) (AssetValues s)
-  , forall s. Hashable (HashSimple s) (Transaction s)
-  , forall s. Hashable (HashSimple s) (TransactionBatch s)
-  , forall s. Hashable (HashSimple s) (TransactionBatchData s)
-  , forall s. Hashable (HashSimple s) ((Circuit :*: DAIndex :*: DAType) s)
+type SignatureState bi bo ud a context =
+  ( Symbolic context
+  , KnownRegistersAssetQuantity context
+  , Hashable (HashSimple context) (State bi bo ud a context)
+  , forall s. Hashable (HashSimple s) (State bi bo ud a s)
+  , Hashable (HashSimple context) ((Vector bi :.: Output a) context)
+  , Hashable (HashSimple context) ((Vector bo :.: Output a) context)
+  , Hashable (HashSimple context) (FieldElement context)
+  , forall s. Hashable (HashSimple s) (FieldElement s)
   )
diff --git a/symbolic-ledger/src/ZkFold/Symbolic/Ledger/Types/Address.hs b/symbolic-ledger/src/ZkFold/Symbolic/Ledger/Types/Address.hs
index b3339f281..614770be0 100644
--- a/symbolic-ledger/src/ZkFold/Symbolic/Ledger/Types/Address.hs
+++ b/symbolic-ledger/src/ZkFold/Symbolic/Ledger/Types/Address.hs
@@ -1,16 +1,16 @@
 module ZkFold.Symbolic.Ledger.Types.Address (
   Address,
+  nullAddress,
 ) where
 
-import GHC.Generics ((:*:))
-
-import ZkFold.Symbolic.Ledger.Types.Circuit (Circuit)
-import ZkFold.Symbolic.Ledger.Types.DataAvailability
-import ZkFold.Symbolic.Ledger.Types.Hash (Hash)
+import ZkFold.Algebra.Class (Zero (..))
+import ZkFold.Symbolic.Class (Symbolic)
+import ZkFold.Symbolic.Data.FieldElement (FieldElement)
+import Prelude hiding (Bool, Eq, length, splitAt, (*), (+))
 
 -- | Address on the zkFold ledger.
---
--- Circuit describes the smart contract that locks funds at this address.
---
--- Data availability index points to a data availability source that posts data about the address's transactions. The data availability type indicates whether the address is associated with online or offline transactions.
-type Address = Hash (Circuit :*: DAIndex :*: DAType)
+type Address = FieldElement
+
+-- | Null address.
+nullAddress :: Symbolic context => Address context
+nullAddress = zero
diff --git a/symbolic-ledger/src/ZkFold/Symbolic/Ledger/Types/Circuit.hs b/symbolic-ledger/src/ZkFold/Symbolic/Ledger/Types/Circuit.hs
deleted file mode 100644
index dbaabf253..000000000
--- a/symbolic-ledger/src/ZkFold/Symbolic/Ledger/Types/Circuit.hs
+++ /dev/null
@@ -1,13 +0,0 @@
-module ZkFold.Symbolic.Ledger.Types.Circuit (
-  Circuit,
-) where
-
-import ZkFold.Symbolic.Data.FieldElement (FieldElement)
-import Prelude hiding (Bool, Eq, Ord, length, splitAt, (*), (+))
-
--- TODO: Give proper definition of Circuit. For now it is just a FieldElement to help with instances and avoiding extra class constraints.
-
--- | Set of commitments to the constraints of the circuit.
---
--- 'Circuit' is used to represent the smart contract that locks funds at a particular address.
-type Circuit = FieldElement
diff --git a/symbolic-ledger/src/ZkFold/Symbolic/Ledger/Types/DataAvailability.hs b/symbolic-ledger/src/ZkFold/Symbolic/Ledger/Types/DataAvailability.hs
deleted file mode 100644
index 85fc1f4ba..000000000
--- a/symbolic-ledger/src/ZkFold/Symbolic/Ledger/Types/DataAvailability.hs
+++ /dev/null
@@ -1,25 +0,0 @@
-module ZkFold.Symbolic.Ledger.Types.DataAvailability (
-  DAIndex,
-  DAType,
-  isOffline,
-  isOnline,
-) where
-
-import ZkFold.Data.Eq
-import ZkFold.Symbolic.Class (Symbolic)
-import ZkFold.Symbolic.Data.Bool (Bool, BoolType (..))
-import ZkFold.Symbolic.Data.FieldElement (FieldElement)
-
--- | Index associated with a data availability source.
-type DAIndex = FieldElement
-
--- | Denotes data availability type, 'True' corresponds to offline transactions, while 'False' denotes online transactions.
-type DAType = Bool
-
--- | Does 'DAType' correspond to offline transaction?
-isOffline :: forall context. Symbolic context => DAType context -> Bool context
-isOffline t = t == (true :: Bool context)
-
--- | Does 'DAType' correspond to online transaction?
-isOnline :: forall context. Symbolic context => DAType context -> Bool context
-isOnline t = t == (false :: Bool context)
diff --git a/symbolic-ledger/src/ZkFold/Symbolic/Ledger/Types/Datum.hs b/symbolic-ledger/src/ZkFold/Symbolic/Ledger/Types/Datum.hs
deleted file mode 100644
index b6c4dd840..000000000
--- a/symbolic-ledger/src/ZkFold/Symbolic/Ledger/Types/Datum.hs
+++ /dev/null
@@ -1,9 +0,0 @@
-module ZkFold.Symbolic.Ledger.Types.Datum (
-  Datum,
-) where
-
-import ZkFold.Symbolic.Data.FieldElement (FieldElement)
-import Prelude hiding (Bool, Eq, Ord, length, splitAt, (*), (+))
-
--- | Datum that is attached to a transaction output.
-type Datum context = FieldElement context
diff --git a/symbolic-ledger/src/ZkFold/Symbolic/Ledger/Types/Hash.hs b/symbolic-ledger/src/ZkFold/Symbolic/Ledger/Types/Hash.hs
index bb3a18e16..5f45bac35 100644
--- a/symbolic-ledger/src/ZkFold/Symbolic/Ledger/Types/Hash.hs
+++ b/symbolic-ledger/src/ZkFold/Symbolic/Ledger/Types/Hash.hs
@@ -7,7 +7,7 @@ import ZkFold.Symbolic.Data.FieldElement (FieldElement)
 import qualified ZkFold.Symbolic.Data.Hash as Symbolic.Hash
 
 -- | Hash type used in the zkFold ledger.
-type Hash = Symbolic.Hash.Hash FieldElement
+type Hash = Symbolic.Hash.Hash HashSimple
 
 -- TODO: Introduce a phantom type to track hash relation? Also should likely add strong typing than synonyms.
 
diff --git a/symbolic-ledger/src/ZkFold/Symbolic/Ledger/Types/Interval.hs b/symbolic-ledger/src/ZkFold/Symbolic/Ledger/Types/Interval.hs
deleted file mode 100644
index e37e9c4dc..000000000
--- a/symbolic-ledger/src/ZkFold/Symbolic/Ledger/Types/Interval.hs
+++ /dev/null
@@ -1,32 +0,0 @@
-{-# LANGUAGE DeriveAnyClass #-}
-
-module ZkFold.Symbolic.Ledger.Types.Interval (
-  Interval,
-  contains,
-) where
-
-import GHC.Generics (Generic, Generic1)
-import ZkFold.Algebra.Number (KnownNat)
-import ZkFold.Data.Eq (Eq)
-import ZkFold.Symbolic.Class (Symbolic (..))
-import ZkFold.Symbolic.Data.Bool (Bool, BoolType (..))
-import ZkFold.Symbolic.Data.Class (SymbolicData)
-import ZkFold.Symbolic.Data.Combinators
-import ZkFold.Symbolic.Data.Ord
-import ZkFold.Symbolic.Data.UInt (OrdWord)
-import ZkFold.Symbolic.Data.UTCTime (UTCTime)
-import Prelude (type (~))
-
-data Interval context = Interval
-  { start :: UTCTime context
-  , end :: UTCTime context
-  }
-  deriving (Generic, Generic1, SymbolicData)
-
-instance Symbolic c => Eq (Interval c)
-
--- | @a contains b@ is true if @b@ is entirely contained in @a@.
-contains
-  :: (Symbolic c, KnownRegisters c 11 Auto, regSize ~ GetRegisterSize (BaseField c) 11 Auto, KnownNat (Ceil regSize OrdWord))
-  => Interval c -> Interval c -> Bool c
-contains (Interval as ae) (Interval bs be) = as <= bs && be <= ae
diff --git a/symbolic-ledger/src/ZkFold/Symbolic/Ledger/Types/Output.hs b/symbolic-ledger/src/ZkFold/Symbolic/Ledger/Types/Output.hs
deleted file mode 100644
index 5873360bd..000000000
--- a/symbolic-ledger/src/ZkFold/Symbolic/Ledger/Types/Output.hs
+++ /dev/null
@@ -1,28 +0,0 @@
-{-# LANGUAGE DeriveAnyClass #-}
-{-# LANGUAGE UndecidableInstances #-}
-
-module ZkFold.Symbolic.Ledger.Types.Output where
-
-import GHC.Generics (Generic, Generic1)
-import ZkFold.Data.Eq (Eq)
-import ZkFold.Symbolic.Class (Symbolic)
-import ZkFold.Symbolic.Data.Class (SymbolicData)
-import Prelude hiding (Bool, Eq, length, splitAt, (*), (+))
-
-import ZkFold.Symbolic.Ledger.Types.Address (Address)
-import ZkFold.Symbolic.Ledger.Types.Datum (Datum)
-import ZkFold.Symbolic.Ledger.Types.Value (AssetValue, KnownRegistersAssetQuantity)
-
--- | Transaction output.
-data Output context = Output
-  { txoAddress :: Address context
-  -- ^ 'Address' at which the value is locked.
-  , txoValue :: AssetValue context
-  -- ^ 'AssetValue' locked by the output.
-  , txoDatum :: Datum context
-  -- ^ 'Datum' associated with the output.
-  }
-  deriving stock (Generic, Generic1)
-  deriving anyclass SymbolicData
-
-instance (KnownRegistersAssetQuantity context, Symbolic context) => Eq (Output context)
diff --git a/symbolic-ledger/src/ZkFold/Symbolic/Ledger/Types/Root.hs b/symbolic-ledger/src/ZkFold/Symbolic/Ledger/Types/Root.hs
deleted file mode 100644
index 74fff5b51..000000000
--- a/symbolic-ledger/src/ZkFold/Symbolic/Ledger/Types/Root.hs
+++ /dev/null
@@ -1,20 +0,0 @@
-module ZkFold.Symbolic.Ledger.Types.Root (
-  Root,
-  empty,
-  insert,
-) where
-
-import Prelude hiding (Bool, Eq, Ord, length, splitAt, (*), (+))
-
-import ZkFold.Symbolic.Ledger.Types.Hash (Hash)
-
--- TODO: Move from Hash to correct type from symbolic-base.
-
--- | Denotes root of a Merkle tree with leaves of type @t@.
-type Root = Hash
-
-empty :: Root t c
-empty = undefined
-
-insert :: t c -> Root t c -> Root t c
-insert = undefined
diff --git a/symbolic-ledger/src/ZkFold/Symbolic/Ledger/Types/State.hs b/symbolic-ledger/src/ZkFold/Symbolic/Ledger/Types/State.hs
new file mode 100644
index 000000000..53db967ba
--- /dev/null
+++ b/symbolic-ledger/src/ZkFold/Symbolic/Ledger/Types/State.hs
@@ -0,0 +1,42 @@
+{-# LANGUAGE DeriveAnyClass #-}
+{-# LANGUAGE UndecidableInstances #-}
+
+module ZkFold.Symbolic.Ledger.Types.State (
+  State (..),
+) where
+
+import GHC.Generics (Generic, Generic1, (:.:))
+import ZkFold.Data.Eq (Eq)
+import ZkFold.Data.Vector (Vector)
+import ZkFold.Symbolic.Class (Symbolic)
+import ZkFold.Symbolic.Data.Class (SymbolicData (..))
+import ZkFold.Symbolic.Data.FieldElement (FieldElement)
+import ZkFold.Symbolic.Data.MerkleTree (MerkleTree)
+import Prelude hiding (Bool, Eq, length, splitAt, (*), (+))
+
+import ZkFold.Symbolic.Ledger.Types.Hash (Hash, HashSimple)
+import ZkFold.Symbolic.Ledger.Types.Transaction
+import ZkFold.Symbolic.Ledger.Types.Value (KnownRegistersAssetQuantity)
+
+-- | Defines the on-chain representation of the Symbolic Ledger state transition.
+data State bi bo ud a context = State
+  { sPreviousStateHash :: HashSimple context
+  -- ^ Hash of the previous state.
+  , sUTxO :: MerkleTree ud context
+  -- ^ Merkle tree of UTxO set.
+  , sLength :: FieldElement context
+  -- ^ Denotes length of the state chain.
+  , sBridgeIn :: Hash (Vector bi :.: Output a) context
+  -- ^ Outputs that are bridged into the ledger. These lead to creation of new UTxOs where `orTxId` of the output is obtained by hashing `sLength` and `orIndex` is the index of the output in the vector.
+  , sBridgeOut :: Hash (Vector bo :.: Output a) context
+  -- ^ Denotes outputs that are bridged out of the ledger.
+  }
+  deriving stock (Generic, Generic1)
+  deriving anyclass SymbolicData
+
+instance
+  forall bi bo ud a context
+   . ( KnownRegistersAssetQuantity context
+     , Symbolic context
+     )
+  => Eq (State bi bo ud a context)
diff --git a/symbolic-ledger/src/ZkFold/Symbolic/Ledger/Types/Transaction.hs b/symbolic-ledger/src/ZkFold/Symbolic/Ledger/Types/Transaction.hs
index 489136d5b..3c25c5995 100644
--- a/symbolic-ledger/src/ZkFold/Symbolic/Ledger/Types/Transaction.hs
+++ b/symbolic-ledger/src/ZkFold/Symbolic/Ledger/Types/Transaction.hs
@@ -1,9 +1,7 @@
 module ZkFold.Symbolic.Ledger.Types.Transaction (
   module ZkFold.Symbolic.Ledger.Types.Transaction.Core,
   module ZkFold.Symbolic.Ledger.Types.Transaction.Batch,
-  module ZkFold.Symbolic.Ledger.Types.Transaction.BatchData,
 ) where
 
 import ZkFold.Symbolic.Ledger.Types.Transaction.Batch
-import ZkFold.Symbolic.Ledger.Types.Transaction.BatchData
 import ZkFold.Symbolic.Ledger.Types.Transaction.Core
diff --git a/symbolic-ledger/src/ZkFold/Symbolic/Ledger/Types/Transaction/Batch.hs b/symbolic-ledger/src/ZkFold/Symbolic/Ledger/Types/Transaction/Batch.hs
index 29b1ef067..0a90b42e2 100644
--- a/symbolic-ledger/src/ZkFold/Symbolic/Ledger/Types/Transaction/Batch.hs
+++ b/symbolic-ledger/src/ZkFold/Symbolic/Ledger/Types/Transaction/Batch.hs
@@ -5,42 +5,26 @@ module ZkFold.Symbolic.Ledger.Types.Transaction.Batch (
   TransactionBatch (..),
 ) where
 
-import GHC.Generics (Generic, Generic1, (:*:))
+import GHC.Generics (Generic, Generic1)
 import ZkFold.Data.Eq (Eq)
+import ZkFold.Data.Vector (Vector)
 import ZkFold.Symbolic.Class (Symbolic)
 import ZkFold.Symbolic.Data.Class (SymbolicData (..))
-import ZkFold.Symbolic.Data.Combinators (KnownRegisters, RegisterSize (Auto))
-import ZkFold.Symbolic.Data.List (List)
-import Prelude hiding (Bool, Eq, length, splitAt, (*), (+))
 
-import ZkFold.Symbolic.Ledger.Types.DataAvailability (DAIndex)
-import ZkFold.Symbolic.Ledger.Types.Hash (HashSimple)
-import ZkFold.Symbolic.Ledger.Types.Interval (Interval)
-import ZkFold.Symbolic.Ledger.Types.Transaction.Core (KnownRegistersOutputIndex)
+import ZkFold.Symbolic.Ledger.Types.Transaction.Core (Transaction)
 import ZkFold.Symbolic.Ledger.Types.Value (KnownRegistersAssetQuantity)
 
--- TODO: Use POSIXTime instead of UTCTime?
-
--- | Defines the on-chain representation of the Symbolic Ledger state transition.
-data TransactionBatch context = TransactionBatch
-  { tbDataHashes :: List (DAIndex :*: HashSimple) context
-  -- ^ Hash of 'TransactionBatchData' indexed by the corresponding data availability source.
-  , tbBridgeIn :: HashSimple context
-  -- ^ Hash of the 'AssetValues' that are bridged into the ledger.
-  , tbBridgeOut :: HashSimple context
-  -- ^ Hash of the 'AssetValues' that are bridged out of the ledger.
-  , tbValidityInterval :: Interval context
-  -- ^ The validity interval of the transaction batch. The bounds are inclusive.
-  , tbPreviousBatch :: HashSimple context
-  -- ^ Hash of the previous transaction batch.
+-- | Transaction batch.
+newtype TransactionBatch i o a t c = TransactionBatch
+  { tbTransactions :: Vector t (Transaction i o a c)
+  -- ^ Vector of transaction hashes.
   }
   deriving stock (Generic, Generic1)
   deriving anyclass SymbolicData
 
 instance
-  ( KnownRegistersAssetQuantity context
-  , KnownRegistersOutputIndex context
-  , KnownRegisters context 11 Auto
-  , Symbolic context
-  )
-  => Eq (TransactionBatch context)
+  forall i o a t context
+   . ( Symbolic context
+     , KnownRegistersAssetQuantity context
+     )
+  => Eq (TransactionBatch i o a t context)
diff --git a/symbolic-ledger/src/ZkFold/Symbolic/Ledger/Types/Transaction/BatchData.hs b/symbolic-ledger/src/ZkFold/Symbolic/Ledger/Types/Transaction/BatchData.hs
deleted file mode 100644
index 8d5990bbd..000000000
--- a/symbolic-ledger/src/ZkFold/Symbolic/Ledger/Types/Transaction/BatchData.hs
+++ /dev/null
@@ -1,40 +0,0 @@
-{-# LANGUAGE DeriveAnyClass #-}
-{-# LANGUAGE UndecidableInstances #-}
-
-module ZkFold.Symbolic.Ledger.Types.Transaction.BatchData (
-  TransactionBatchData (..),
-) where
-
-import GHC.Generics (Generic, Generic1, (:*:))
-import ZkFold.Data.Eq (Eq)
-import ZkFold.Symbolic.Class (Symbolic)
-import ZkFold.Symbolic.Data.Class (SymbolicData (..))
-import ZkFold.Symbolic.Data.Combinators (KnownRegisters, RegisterSize (Auto))
-import ZkFold.Symbolic.Data.List (List)
-import Prelude hiding (Bool, Eq, length, splitAt, (*), (+))
-
-import ZkFold.Symbolic.Ledger.Types.Address (Address)
-import ZkFold.Symbolic.Ledger.Types.Hash (HashSimple)
-import ZkFold.Symbolic.Ledger.Types.Root (Root)
-import ZkFold.Symbolic.Ledger.Types.Transaction.Core (KnownRegistersOutputIndex)
-import ZkFold.Symbolic.Ledger.Types.Value (KnownRegistersAssetQuantity)
-
--- | Transaction batch data, given to us by a data provider source. Thus all the 'Address' entries here must have same 'DAIndex'.
-data TransactionBatchData context = TransactionBatchData
-  { tbdMerkleRoot :: Root (Address :*: List HashSimple) context
-  -- ^ Merkle tree root of the addresses corresponding to online transactions (represented by their transaction hash) that are associated with a particular data availability source.
-  , tbdOnlineAddresses :: List Address context
-  -- ^ List of addresses included in the batch which correspond to online transactions and are associated with a particular data availability source.
-  , tbdOfflineTransactions :: List (Address :*: List HashSimple) context
-  -- ^ All offline transactions (represented by their transaction hash) associated with a particular data availability source that are included in the batch.
-  }
-  deriving stock (Generic, Generic1)
-  deriving anyclass SymbolicData
-
-instance
-  ( KnownRegistersAssetQuantity context
-  , KnownRegistersOutputIndex context
-  , KnownRegisters context 11 Auto
-  , Symbolic context
-  )
-  => Eq (TransactionBatchData context)
diff --git a/symbolic-ledger/src/ZkFold/Symbolic/Ledger/Types/Transaction/Core.hs b/symbolic-ledger/src/ZkFold/Symbolic/Ledger/Types/Transaction/Core.hs
index 264a54a07..876b4018e 100644
--- a/symbolic-ledger/src/ZkFold/Symbolic/Ledger/Types/Transaction/Core.hs
+++ b/symbolic-ledger/src/ZkFold/Symbolic/Ledger/Types/Transaction/Core.hs
@@ -1,130 +1,131 @@
+{-# LANGUAGE AllowAmbiguousTypes #-}
 {-# LANGUAGE BlockArguments #-}
 {-# LANGUAGE DeriveAnyClass #-}
+{-# LANGUAGE ImportQualifiedPost #-}
+{-# LANGUAGE TypeApplications #-}
 {-# LANGUAGE UndecidableInstances #-}
 
 module ZkFold.Symbolic.Ledger.Types.Transaction.Core (
-  Transaction (txInputs, txOutputs, txValidityInterval, txOwner),
-  mkTransaction,
+  OutputRef (..),
+  nullOutputRef,
+  Output (..),
+  nullOutput,
+  UTxO (..),
+  nullUTxO,
+  nullUTxOHash,
+  Transaction (..),
   TransactionId,
   txId,
-  OutputIndex,
-  KnownRegistersOutputIndex,
-  OutputRef (..),
-  Input (..),
 ) where
 
-import GHC.Generics (Generic, Generic1, type (:*:) (..))
-import ZkFold.Control.Conditional (ifThenElse)
+import Data.Function ((&))
+import GHC.Generics (Generic, Generic1, (:*:), (:.:) (..))
+import GHC.TypeNats (KnownNat)
+import ZkFold.Algebra.Class (Zero (..))
 import ZkFold.Data.Eq (Eq (..))
+import ZkFold.Data.Vector (Vector)
 import ZkFold.Symbolic.Class (Symbolic)
-import ZkFold.Symbolic.Data.Bool (Bool, BoolType (..))
+import ZkFold.Symbolic.Data.Bool (Bool)
 import ZkFold.Symbolic.Data.Class (SymbolicData (..))
-import ZkFold.Symbolic.Data.Combinators (KnownRegisters, RegisterSize (Auto))
+import ZkFold.Symbolic.Data.Combinators (RegisterSize (Auto))
 import ZkFold.Symbolic.Data.Hash (Hashable, hash)
-import ZkFold.Symbolic.Data.List (List)
-import qualified ZkFold.Symbolic.Data.List as Symbolic.List
-import ZkFold.Symbolic.Data.Maybe (Maybe, just, nothing)
+import ZkFold.Symbolic.Data.Hash qualified as Base
 import ZkFold.Symbolic.Data.UInt (UInt)
-import ZkFold.Symbolic.Fold (SymbolicFold)
 import Prelude hiding (Bool, Eq, Maybe, length, splitAt, (*), (+), (==), (||))
-import qualified Prelude as Haskell hiding ((||))
+import Prelude qualified as Haskell hiding ((||))
 
-import ZkFold.Symbolic.Ledger.Types.Address (Address)
+import ZkFold.Symbolic.Ledger.Types.Address (Address, nullAddress)
 import ZkFold.Symbolic.Ledger.Types.Hash (Hash, HashSimple)
-import ZkFold.Symbolic.Ledger.Types.Interval (Interval)
-import ZkFold.Symbolic.Ledger.Types.Output (Output (..))
-import ZkFold.Symbolic.Ledger.Types.Value (KnownRegistersAssetQuantity)
-
--- TODO: Use POSIXTime instead of UTCTime?
+import ZkFold.Symbolic.Ledger.Types.Value (AssetValue, KnownRegistersAssetQuantity)
 
--- | Transaction in our symbolic ledger.
-data Transaction context = Transaction
-  { txInputs :: List Input context
-  -- ^ A list of inputs to the transaction.
-  , txOutputs :: List Output context
-  -- ^ A list of outputs of the transaction.
-  , txValidityInterval :: Interval context
-  -- ^ The validity interval of the transaction. The bounds are inclusive.
-  , txOwner :: Address context
-  -- ^ Inputs belonging to this address are considered spent whereas others are considered to be only referenced by this transaction.
+-- | An output's reference.
+data OutputRef context = OutputRef
+  { orTxId :: HashSimple context
+  -- ^ Transaction ID which created this output.
+  , orIndex :: UInt 32 Auto context
+  -- ^ Index of the output in the transaction.
+  -- TODO: Restrict to represent 'o' outputs instead of 2^32?
   }
   deriving stock (Generic, Generic1)
   deriving anyclass SymbolicData
 
 instance
-  ( KnownRegistersAssetQuantity context
-  , KnownRegistersOutputIndex context
-  , KnownRegisters context 11 Auto
-  , Symbolic context
-  )
-  => Eq (Transaction context)
+  Symbolic context
+  => Eq (OutputRef context)
 
--- | Builds a 'Transaction' validating that there is at least one input belonging to the "owner".
-mkTransaction
-  :: forall context
-   . ( SymbolicFold context
-     , KnownRegistersAssetQuantity context
-     , KnownRegistersOutputIndex context
-     , KnownRegisters context 11 Auto
-     )
-  => List Input context
-  -> List Output context
-  -> Interval context
-  -> Address context
-  -> Maybe Transaction context
-mkTransaction inputs outputs validityInterval owner =
-  let (hasOwnerInput :*: _) =
-        Symbolic.List.foldl
-          (\(accBool :*: owner') x -> (accBool || txoAddress (txiOutput x) == owner') :*: owner')
-          ((false :: Bool context) :*: owner)
-          inputs
-   in ifThenElse
-        hasOwnerInput
-        nothing
-        ( just $
-            Transaction
-              { txInputs = inputs
-              , txOutputs = outputs
-              , txValidityInterval = validityInterval
-              , txOwner = owner
-              }
-        )
+-- | Null output reference.
+nullOutputRef :: Symbolic context => OutputRef context
+nullOutputRef = OutputRef {orTxId = zero, orIndex = zero}
 
--- | Transaction hash.
-type TransactionId = Hash Transaction
-
-txId
-  :: ( Symbolic context
-     , Hashable (HashSimple context) (Transaction context)
-     )
-  => Transaction context -> TransactionId context
-txId = hash
+-- | An output of a transaction.
+data Output a context = Output
+  { oAddress :: Address context
+  -- ^ Address of the output.
+  , oAssets :: (Vector a :.: AssetValue) context
+  -- ^ Assets of the output.
+  }
+  deriving stock (Generic, Generic1)
+  deriving anyclass SymbolicData
 
--- | Index of an output in the transaction's output list.
-type OutputIndex = UInt 32 Auto
+instance
+  ( Symbolic context
+  , KnownRegistersAssetQuantity context
+  )
+  => Eq (Output a context)
 
-type KnownRegistersOutputIndex context = KnownRegisters context 32 Auto
+-- | Null output.
+nullOutput :: forall a context. (Symbolic context, KnownNat a) => Output a context
+nullOutput = Output {oAddress = nullAddress, oAssets = Comp1 zero}
 
--- | Reference to a transaction output.
-data OutputRef context = OutputRef
-  { refId :: HashSimple context
-  -- ^ The transaction id of the transaction that produced the output.
-  , refIdx :: OutputIndex context
-  -- ^ The index of the output in the transaction's output list.
+-- | A UTxO.
+data UTxO a context = UTxO
+  { uRef :: OutputRef context
+  , uOutput :: Output a context
   }
   deriving stock (Generic, Generic1)
   deriving anyclass SymbolicData
 
-instance (KnownRegistersAssetQuantity context, KnownRegistersOutputIndex context, Symbolic context) => Eq (OutputRef context)
+instance
+  ( Symbolic context
+  , KnownRegistersAssetQuantity context
+  )
+  => Eq (UTxO a context)
+
+-- | Null UTxO.
+nullUTxO :: forall a context. (Symbolic context, KnownNat a) => UTxO a context
+nullUTxO = UTxO {uRef = nullOutputRef, uOutput = nullOutput}
+
+-- | Null UTxO's hash.
+nullUTxOHash
+  :: forall a context. (Symbolic context, KnownNat a, Hashable (HashSimple context) (UTxO a context)) => HashSimple context
+nullUTxOHash = hash (nullUTxO @a @context) & Base.hHash
 
--- | Input to a transaction.
-data Input context = Input
-  { txiOutputRef :: OutputRef context
-  -- ^ Reference to the output being spent.
-  , txiOutput :: Output context
-  -- ^ The output being spent.
+-- | Transaction in our symbolic ledger.
+data Transaction i o a context = Transaction
+  { inputs :: (Vector i :.: OutputRef) context
+  -- ^ Inputs.
+  , outputs :: (Vector o :.: (Output a :*: Bool)) context
+  -- ^ Outputs. Boolean denotes whether the output is a bridge out output, in which case `oAddress` denotes Cardano address.
   }
   deriving stock (Generic, Generic1)
   deriving anyclass SymbolicData
 
-instance (KnownRegistersAssetQuantity context, KnownRegistersOutputIndex context, Symbolic context) => Eq (Input context)
+instance
+  forall i o a context
+   . ( Symbolic context
+     , KnownRegistersAssetQuantity context
+     )
+  => Eq (Transaction i o a context)
+
+-- | Transaction hash.
+type TransactionId i o a = Hash (Transaction i o a)
+
+-- | Obtain transaction hash.
+txId
+  :: forall i o a context
+   . ( Symbolic context
+     , Hashable (HashSimple context) (Transaction i o a context)
+     )
+  => Transaction i o a context
+  -> TransactionId i o a context
+txId = hash
diff --git a/symbolic-ledger/src/ZkFold/Symbolic/Ledger/Types/Value.hs b/symbolic-ledger/src/ZkFold/Symbolic/Ledger/Types/Value.hs
index 37318d84b..80efa1844 100644
--- a/symbolic-ledger/src/ZkFold/Symbolic/Ledger/Types/Value.hs
+++ b/symbolic-ledger/src/ZkFold/Symbolic/Ledger/Types/Value.hs
@@ -5,9 +5,12 @@
 
 module ZkFold.Symbolic.Ledger.Types.Value (
   AssetPolicy,
+  adaPolicy,
   AssetName,
+  adaName,
   AssetQuantity,
   AssetValue (..),
+  nullAssetValue,
   AssetValues,
   KnownRegistersAssetQuantity,
 
@@ -33,6 +36,7 @@ import ZkFold.Symbolic.Class (Symbolic)
 import ZkFold.Symbolic.Data.Bool (Bool, BoolType (..))
 import ZkFold.Symbolic.Data.Class (SymbolicData (..))
 import ZkFold.Symbolic.Data.Combinators (KnownRegisters, RegisterSize (Auto))
+import ZkFold.Symbolic.Data.FieldElement (FieldElement)
 import ZkFold.Symbolic.Data.Int (Int)
 import ZkFold.Symbolic.Data.List (List, emptyList, (.:))
 import qualified ZkFold.Symbolic.Data.List as Symbolic.List
@@ -54,20 +58,25 @@ import Prelude hiding (
   (||),
  )
 
-import ZkFold.Symbolic.Ledger.Types.Address (Address)
-import ZkFold.Symbolic.Ledger.Types.Datum (Datum)
+-- | Asset policy.
+type AssetPolicy context = FieldElement context
 
--- | Asset policy is the address of the initial UTxO that contains the asset.
-type AssetPolicy context = Address context
-
--- | Name of the asset. It's the datum of the initial UTxO that contains the asset.
-type AssetName context = Datum context
+-- | Name of the asset.
+type AssetName context = FieldElement context
 
 -- | Quantity of an asset.
 type AssetQuantity context = Int 128 Auto context
 
 type KnownRegistersAssetQuantity context = KnownRegisters context 128 Auto
 
+-- TODO: Replace with actual value, once we finalize how policy names are represented.
+adaPolicy :: AssetPolicy context
+adaPolicy = undefined
+
+-- TODO: Replace with actual value, once we finalize how asset names are represented.
+adaName :: AssetName context
+adaName = undefined
+
 -- | A value represents the details of an asset that is contained in a transaction output.
 data AssetValue context = AssetValue
   { assetPolicy :: AssetPolicy context
@@ -79,6 +88,13 @@ data AssetValue context = AssetValue
 
 instance (KnownRegistersAssetQuantity context, Symbolic context) => Eq (AssetValue context)
 
+-- | Null asset value.
+nullAssetValue :: Symbolic context => AssetValue context
+nullAssetValue = AssetValue {assetPolicy = zero, assetName = zero, assetQuantity = zero}
+
+instance Symbolic context => Zero (AssetValue context) where
+  zero = nullAssetValue
+
 -- | Denotes multiple assets.
 newtype AssetValues context = UnsafeAssetValues (List AssetValue context)
   deriving newtype SymbolicData
diff --git a/symbolic-ledger/src/ZkFold/Symbolic/Ledger/Validation/State.hs b/symbolic-ledger/src/ZkFold/Symbolic/Ledger/Validation/State.hs
new file mode 100644
index 000000000..e4c9dcacf
--- /dev/null
+++ b/symbolic-ledger/src/ZkFold/Symbolic/Ledger/Validation/State.hs
@@ -0,0 +1,121 @@
+{-# LANGUAGE ImportQualifiedPost #-}
+{-# LANGUAGE ImpredicativeTypes #-}
+{-# LANGUAGE OverloadedRecordDot #-}
+
+module ZkFold.Symbolic.Ledger.Validation.State (
+  validateStateUpdate,
+  StateWitness (..),
+) where
+
+import Data.Function ((&))
+import GHC.Generics ((:*:) (..), (:.:) (..))
+import ZkFold.Algebra.Class (MultiplicativeMonoid (..), Zero (..), (+))
+import ZkFold.Control.Conditional (ifThenElse)
+import ZkFold.Data.Eq (Eq (..), (==))
+import ZkFold.Data.Vector (Vector, Zip (..))
+import ZkFold.Prelude (foldl')
+import ZkFold.Symbolic.Data.Bool (Bool, BoolType (..))
+import ZkFold.Symbolic.Data.Hash (Hashable (..), hash, preimage)
+import ZkFold.Symbolic.Data.Hash qualified as Base
+import ZkFold.Symbolic.Data.MerkleTree (MerkleEntry)
+import ZkFold.Symbolic.Data.MerkleTree qualified as MerkleTree
+
+import ZkFold.Symbolic.Ledger.Types
+import ZkFold.Symbolic.Ledger.Validation.Transaction (outputHasAtLeastOneAda)
+import ZkFold.Symbolic.Ledger.Validation.TransactionBatch (TransactionBatchWitness, validateTransactionBatch)
+
+{- Note [State validation]
+
+For validating transactions, we should check:
+
+\* Inputs come from UTxO set.
+\* We subtract inputs UTxOs from the UTxO set.
+\* Outputs are added to the UTxO set if they are not bridge out outputs.
+\* We require signature from addresses corresponding to spent UTxOs.
+\* Bridged out outputs are checked to be same as in bridge out list.
+\* Outputs must have at least one ada.
+\* Transaction is balanced.
+
+For validating batch, we simply apply transaction validation check iteratively.
+
+For validating state, we check following:
+
+\* Previous state hash is correctly set.
+\* New UTxO state is properly computed. For it, we first added UTxOs to the old state corresponding to bridged in assets and then update this set by folding over transactions.
+\* Bridge in outputs have at least one ada.
+\* Transaction batch is valid.
+\* Length is incremented by one.
+\* Bridged out list is correctly computed.
+-}
+
+-- | State witness for validating state update.
+data StateWitness bi bo ud a i o t context = StateWitness
+  { swAddBridgeIn :: (Vector bi :.: MerkleEntry ud) context
+  , swTransactionBatch :: (TransactionBatchWitness ud i o a t) context
+  }
+
+-- | Validate state update. See note [State validation] for details.
+validateStateUpdate
+  :: forall bi bo ud a i o t context
+   . SignatureState bi bo ud a context
+  => SignatureTransactionBatch ud i o a t context
+  => State bi bo ud a context
+  -- ^ Previous state.
+  -> TransactionBatch i o a t context
+  -- ^ The "action" that is applied to the state.
+  -> State bi bo ud a context
+  -- ^ New state.
+  -> StateWitness bi bo ud a i o t context
+  -- ^ Witness for the state.
+  -> Bool context
+validateStateUpdate previousState action newState sw =
+  let
+    initialUTxOTree = previousState.sUTxO
+    bridgeInAssets = preimage newState.sBridgeIn
+    bridgedInAssetsWithWitness = zipWith (:*:) (unComp1 bridgeInAssets) (unComp1 sw.swAddBridgeIn)
+
+    bridgeInHash = newState.sLength & hash & Base.hHash
+    (_ :*: isWitBridgeInValid :*: utxoTreeWithBridgeIn) =
+      foldl'
+        ( \(ix :*: isValidAcc :*: acc) ((output :*: merkleEntry)) ->
+            let nullUTxOHash' = nullUTxOHash @a @context
+                isValid' =
+                  isValidAcc
+                    && ifThenElse
+                      (output == nullOutput)
+                      true
+                      ( (acc `MerkleTree.contains` merkleEntry)
+                          && (merkleEntry.value == nullUTxOHash')
+                          && outputHasAtLeastOneAda output
+                      )
+                utxo = UTxO {uRef = OutputRef {orTxId = bridgeInHash, orIndex = ix}, uOutput = output}
+                utxoHash = hash utxo & Base.hHash
+             in ( (ix + one)
+                    :*: isValid'
+                    :*: ifThenElse
+                      (isValid' && (output /= nullOutput))
+                      ( MerkleTree.replace
+                          ( merkleEntry
+                              { MerkleTree.value = utxoHash
+                              }
+                          )
+                          acc
+                      )
+                      acc
+                )
+        )
+        (zero :*: true :*: initialUTxOTree)
+        bridgedInAssetsWithWitness
+    bridgedOutOutputs = preimage newState.sBridgeOut
+    (isBatchValid :*: utxoTree) = validateTransactionBatch utxoTreeWithBridgeIn bridgedOutOutputs action sw.swTransactionBatch
+   in
+    -- New state correctly links to the previous state.
+    newState.sPreviousStateHash
+      == hasher previousState
+      && newState.sLength
+      == previousState.sLength
+      + one
+      && isWitBridgeInValid
+      && isBatchValid
+      && utxoTree
+      == newState.sUTxO
diff --git a/symbolic-ledger/src/ZkFold/Symbolic/Ledger/Validation/Transaction.hs b/symbolic-ledger/src/ZkFold/Symbolic/Ledger/Validation/Transaction.hs
new file mode 100644
index 000000000..a5f09c1d7
--- /dev/null
+++ b/symbolic-ledger/src/ZkFold/Symbolic/Ledger/Validation/Transaction.hs
@@ -0,0 +1,241 @@
+{-# LANGUAGE ImpredicativeTypes #-}
+{-# LANGUAGE OverloadedRecordDot #-}
+
+module ZkFold.Symbolic.Ledger.Validation.Transaction (
+  TransactionWitness (..),
+  validateTransaction,
+  outputHasAtLeastOneAda,
+) where
+
+import Data.Function ((&))
+import GHC.Generics ((:*:) (..), (:.:) (..))
+import ZkFold.Algebra.Class (
+  AdditiveGroup (..),
+  AdditiveSemigroup (..),
+  FromConstant (fromConstant),
+  MultiplicativeMonoid (..),
+  Zero (..),
+ )
+import ZkFold.Control.Conditional (ifThenElse)
+import ZkFold.Data.Eq
+import ZkFold.Data.Ord ((>=))
+import ZkFold.Data.Vector (Vector, Zip (..), (!!))
+import qualified ZkFold.Data.Vector as Vector
+import ZkFold.Prelude (foldl')
+import ZkFold.Symbolic.Class (Symbolic)
+import ZkFold.Symbolic.Data.Bool (Bool, BoolType (..))
+import ZkFold.Symbolic.Data.FieldElement (FieldElement)
+import ZkFold.Symbolic.Data.Hash (hash)
+import qualified ZkFold.Symbolic.Data.Hash as Base
+import ZkFold.Symbolic.Data.MerkleTree (MerkleEntry, MerkleTree)
+import qualified ZkFold.Symbolic.Data.MerkleTree as MerkleTree
+import qualified Prelude as P
+
+import ZkFold.Symbolic.Ledger.Types
+
+-- | Transaction witness for validating transaction.
+data TransactionWitness ud i o a context = TransactionWitness
+  { twInputs :: (Vector i :.: (MerkleEntry ud :*: UTxO a)) context
+  , twOutputs :: (Vector o :.: MerkleEntry ud) context
+  }
+
+-- | Validate transaction. See note [State validation] for details.
+validateTransaction
+  :: forall ud bo i o a context
+   . SignatureTransaction ud i o a context
+  => MerkleTree ud context
+  -- ^ UTxO tree.
+  -> (Vector bo :.: Output a) context
+  -- ^ Bridged out outputs.
+  -> Transaction i o a context
+  -- ^ Transaction.
+  -> TransactionWitness ud i o a context
+  -- ^ Transaction witness.
+  -> (FieldElement :*: Bool :*: MerkleTree ud) context
+  -- ^ Result of validation. First field denotes number of bridged out outputs in this transaction, second one denotes whether the transaction is valid, third one denotes updated UTxO tree.
+validateTransaction utxoTree bridgedOutOutputs tx txw =
+  let
+    txId' = txId tx & Base.hHash
+    inputAssets = unComp1 txw.twInputs & P.fmap (\(_me :*: utxo) -> utxo.uOutput.oAssets)
+    outputsAssets = unComp1 tx.outputs & P.fmap (\(output :*: _isBridgeOut) -> unComp1 output.oAssets)
+    -- We check if all output assets are covered by inputs.
+    (outAssetsWithinInputs :*: finalInputAssets) =
+      foldl'
+        ( \(isValid1 :*: inputAssetsAcc) outputAssets ->
+            foldl'
+              ( \(isValid2 :*: inputAssetsAcc') outputAsset ->
+                  let
+                    -- Whether an input asset matches the current output asset by policy and name.
+                    sameAsset av = (av.assetPolicy == outputAsset.assetPolicy) && (av.assetName == outputAsset.assetName)
+
+                    -- Given a remaining quantity to cover, compute the remaining after consuming from one input's assets.
+                    remainingAfterInput rem inAssetsComp =
+                      let asVec = unComp1 inAssetsComp
+                       in foldl'
+                            ( \r av ->
+                                ifThenElse
+                                  (sameAsset av)
+                                  ( ifThenElse
+                                      (r >= av.assetQuantity)
+                                      (r + negate av.assetQuantity)
+                                      zero
+                                  )
+                                  r
+                            )
+                            rem
+                            asVec
+
+                    -- Compute remaining before each input using a prefix scan across inputs.
+                    inputsVec = unComp1 inputAssetsAcc'
+                    remsAcrossInputs =
+                      Vector.scanl
+                        remainingAfterInput
+                        outputAsset.assetQuantity
+                        inputsVec
+
+                    -- Update assets for a single input, given the remaining before this input.
+                    updateInputAssets remBefore inAssetsComp =
+                      let asVec = unComp1 inAssetsComp
+                          -- Remaining before each asset within this input.
+                          remsWithinInput =
+                            Vector.scanl
+                              ( \r av ->
+                                  ifThenElse
+                                    (sameAsset av)
+                                    ( ifThenElse
+                                        (r >= av.assetQuantity)
+                                        (r + negate av.assetQuantity)
+                                        zero
+                                    )
+                                    r
+                              )
+                              remBefore
+                              asVec
+                          -- Update each asset using the remaining before that asset.
+                          updatedAs =
+                            Vector.mapWithIx
+                              ( \ix av ->
+                                  let rBefore = remsWithinInput !! ix
+                                   in ifThenElse
+                                        (sameAsset av)
+                                        ( let newQty = ifThenElse (rBefore >= av.assetQuantity) zero (av.assetQuantity + negate rBefore)
+                                           in av {assetQuantity = newQty}
+                                        )
+                                        av
+                              )
+                              asVec
+                       in Comp1 updatedAs
+
+                    -- Build updated inputs by mapping with index and using prefix-remaining per input.
+                    updatedInputs =
+                      Vector.mapWithIx
+                        ( \ix inAssetsComp ->
+                            let remBefore = remsAcrossInputs !! ix
+                             in updateInputAssets remBefore inAssetsComp
+                        )
+                        inputsVec
+
+                    -- Final remaining after all inputs processed for this output asset.
+                    finalRemaining = Vector.last remsAcrossInputs
+                    isValid' = isValid2 && (finalRemaining == zero)
+                   in
+                    (isValid' :*: Comp1 updatedInputs)
+              )
+              (isValid1 :*: inputAssetsAcc)
+              outputAssets
+        )
+        ((true :: Bool context) :*: Comp1 inputAssets)
+        outputsAssets
+    -- We check if all inputs are covered by outputs.
+    inputsConsumed =
+      foldl'
+        ( \acc inAssetsComp ->
+            let asVec = unComp1 inAssetsComp
+             in acc
+                  && foldl'
+                    (\acc2 av -> acc2 && (av.assetQuantity == zero))
+                    true
+                    asVec
+        )
+        true
+        (unComp1 finalInputAssets)
+    inputsWithWitness = zipWith (:*:) (unComp1 tx.inputs) (unComp1 txw.twInputs)
+    (isInsValid :*: updatedUTxOTreeForInputs) =
+      foldl'
+        ( \(isInsValidAcc :*: acc) (inputRef :*: (merkleEntry :*: utxo)) ->
+            let
+              utxoHash :: HashSimple context = hash utxo & Base.hHash
+              isValid' =
+                isInsValidAcc
+                  && (inputRef == utxo.uRef)
+                  && (utxoHash == MerkleTree.value merkleEntry)
+                  && (acc `MerkleTree.contains` merkleEntry)
+             in
+              ( isValid'
+                  :*: MerkleTree.replace
+                    ( merkleEntry
+                        { MerkleTree.value = nullUTxOHash @a @context
+                        }
+                    )
+                    acc
+              )
+        )
+        ((true :: Bool context) :*: utxoTree)
+        inputsWithWitness
+    outputsWithWitness = zipWith (:*:) (unComp1 tx.outputs) (unComp1 txw.twOutputs)
+    (bouts :*: _ :*: outsValid :*: updatedUTxOTreeForOutputs) =
+      foldl'
+        ( \(boutsAcc :*: outputIx :*: outsValidAcc :*: utxoTreeAcc) ((output :*: bout) :*: merkleEntry) ->
+            ifThenElse
+              bout
+              ( (boutsAcc + one)
+                  :*: (outputIx + one)
+                  :*: ( outsValidAcc
+                          && foldl' (\found boutput -> found || output == boutput) false (unComp1 bridgedOutOutputs)
+                      )
+                  :*: utxoTreeAcc
+              )
+              ( boutsAcc
+                  :*: (outputIx + one)
+                  :*: ( outsValidAcc
+                          && ifThenElse
+                            (output == nullOutput)
+                            true
+                            ( (utxoTreeAcc `MerkleTree.contains` merkleEntry)
+                                && (merkleEntry.value == nullUTxOHash @a @context)
+                                && outputHasAtLeastOneAda output
+                            )
+                      )
+                  :*: ( let utxo = UTxO {uRef = OutputRef {orTxId = txId', orIndex = outputIx}, uOutput = output}
+                         in ifThenElse
+                              (output == nullOutput)
+                              utxoTreeAcc
+                              ( MerkleTree.replace
+                                  ( merkleEntry
+                                      { MerkleTree.value = hash utxo & Base.hHash
+                                      }
+                                  )
+                                  utxoTreeAcc
+                              )
+                      )
+              )
+        )
+        (zero :*: zero :*: (true :: Bool context) :*: updatedUTxOTreeForInputs)
+        outputsWithWitness
+   in
+    (bouts :*: (outsValid && isInsValid && outAssetsWithinInputs && inputsConsumed) :*: updatedUTxOTreeForOutputs)
+
+-- | Check if output has at least one ada.
+outputHasAtLeastOneAda
+  :: forall a context
+   . (KnownRegistersAssetQuantity context, Symbolic context)
+  => Output a context
+  -> Bool context
+outputHasAtLeastOneAda output =
+  foldl'
+    ( \found asset ->
+        found
+          || (asset.assetPolicy == adaPolicy && asset.assetName == adaName && asset.assetQuantity >= fromConstant @P.Integer 1_000_000)
+    )
+    false
+    (unComp1 (oAssets output))
diff --git a/symbolic-ledger/src/ZkFold/Symbolic/Ledger/Validation/Transaction/Batch.hs b/symbolic-ledger/src/ZkFold/Symbolic/Ledger/Validation/Transaction/Batch.hs
deleted file mode 100644
index 0a42cec39..000000000
--- a/symbolic-ledger/src/ZkFold/Symbolic/Ledger/Validation/Transaction/Batch.hs
+++ /dev/null
@@ -1,105 +0,0 @@
-{-# LANGUAGE BlockArguments #-}
-{-# LANGUAGE ImpredicativeTypes #-}
-
-module ZkFold.Symbolic.Ledger.Validation.Transaction.Batch (
-  validateTransactionBatch,
-) where
-
-import Data.Function ((.))
-import GHC.Generics ((:*:) (..))
-import ZkFold.Data.Eq
-import ZkFold.Data.Product (sndP)
-import ZkFold.Symbolic.Data.Bool (Bool, BoolType (true), (&&))
-import ZkFold.Symbolic.Data.FieldElement (FieldElement)
-import ZkFold.Symbolic.Data.Hash
-import ZkFold.Symbolic.Data.List (List)
-import qualified ZkFold.Symbolic.Data.List as Symbolic.List
-import Prelude (($))
-
-import ZkFold.Symbolic.Ledger.Types
-import ZkFold.Symbolic.Ledger.Validation.Transaction.BatchData
-
--- | Witness for 'TransactionBatch' validation.
-data TransactionBatchWitness context = TransactionBatchWitness
-  { tbwBatchDatas :: List (TransactionBatchData :*: TransactionBatchDataWitness) context
-  }
-
--- | Validate 'TransactionBatch'.
-validateTransactionBatch
-  :: forall context
-   . Signature context
-  => TransactionBatch context
-  -- ^ Current tip.
-  -> AssetValues context
-  -- ^ Bridged in assets.
-  -> AssetValues context
-  -- ^ Bridged out assets.
-  -> TransactionBatch context
-  -- ^ New batch to be added.
-  -> TransactionBatchWitness context
-  -- ^ Witness used for validation.
-  -> Bool context
-validateTransactionBatch valBridgeIn valBridgeOut prevTB TransactionBatch {..} TransactionBatchWitness {..} =
-  let
-    -- Batch data hashes as computed via provided witness.
-    resBatchAccDataHashes
-      :*: resBatchAccBatchesValid -- Are individual batches valid? And is 'tbValidityInterval' within the interval of transactions present inside these batches?
-      :*: _ =
-        Symbolic.List.foldl
-          ( \( batchAccDataHashes
-                 :*: batchAccBatchesValid
-                 :*: batchAccBatchValidityInterval
-               )
-             (tbd :*: tbdw) ->
-                let (batchValid, batchDAIndex) =
-                      validateTransactionBatchDataWithIx
-                        batchAccBatchValidityInterval
-                        tbd
-                        tbdw
-                 in ((batchDAIndex :*: hasher tbd) Symbolic.List..: batchAccDataHashes)
-                      :*: (batchAccBatchesValid && batchValid)
-                      :*: batchAccBatchValidityInterval
-          )
-          (Symbolic.List.emptyList :*: true :*: tbValidityInterval)
-          tbwBatchDatas
-   in
-    -- 'tbBridgeIn' represents correct hash.
-    -- TODO: We might not need to do this check if this is performed by smart contract. Same for 'tbBridgeOut' and 'tbPreviousBatch'
-    tbBridgeIn
-      == hasher valBridgeIn
-      -- 'tbBridgeOut' represents correct hash.
-      && tbBridgeOut
-      == hasher valBridgeOut
-      -- 'tbPreviousBatch' represents correct hash.
-      && tbPreviousBatch
-      == hasher prevTB
-      -- 'tbDataHashes' is consistent with given batches.
-      && tbDataHashes
-      == resBatchAccDataHashes
-      -- There are no entries with duplicate data availability index.
-      && noDuplicateIndicesInBatch tbDataHashes
-      -- Individual batches are valid and validity interval of batch is within validity interval of batch transactions.
-      && resBatchAccBatchesValid
-
--- TODO: Refactor following once improvements in symbolic list are merged and it supports more utilities like 'elem'.
-
--- | Check if there are no duplicate 'DAIndex' in the given list.
-noDuplicateIndicesInBatch
-  :: forall context
-   . Signature context
-  => List (DAIndex :*: HashSimple) context -> Bool context
-noDuplicateIndicesInBatch =
-  sndP
-    . Symbolic.List.foldl
-      ( \(accList :*: accNoDuplicateIndices) (ix :*: _) ->
-          let curAccNoDuplicateIndices =
-                sndP $
-                  Symbolic.List.foldl
-                    ( \(givenIx :*: accInternalNoDuplicateIndices) ix' ->
-                        givenIx :*: (accInternalNoDuplicateIndices && (givenIx /= ix'))
-                    )
-                    (ix :*: accNoDuplicateIndices)
-                    accList
-           in (ix Symbolic.List..: accList) :*: curAccNoDuplicateIndices
-      )
-      ((Symbolic.List.emptyList :: List FieldElement context) :*: (true :: Bool context))
diff --git a/symbolic-ledger/src/ZkFold/Symbolic/Ledger/Validation/Transaction/BatchData.hs b/symbolic-ledger/src/ZkFold/Symbolic/Ledger/Validation/Transaction/BatchData.hs
deleted file mode 100644
index f4ef57940..000000000
--- a/symbolic-ledger/src/ZkFold/Symbolic/Ledger/Validation/Transaction/BatchData.hs
+++ /dev/null
@@ -1,228 +0,0 @@
-{-# LANGUAGE BlockArguments #-}
-{-# LANGUAGE DeriveAnyClass #-}
-{-# LANGUAGE ImpredicativeTypes #-}
-{-# LANGUAGE UndecidableInstances #-}
-
-module ZkFold.Symbolic.Ledger.Validation.Transaction.BatchData (
-  TransactionBatchDataWitness (..),
-  validateTransactionBatchData,
-  validateTransactionBatchDataWithIx,
-) where
-
-import Data.Function ((&), (.))
-import GHC.Generics (Generic, Generic1, (:*:) (..))
-import ZkFold.Control.Conditional (ifThenElse)
-import ZkFold.Data.Eq (Eq, (==))
-import ZkFold.Data.Product (fstP, sndP)
-import ZkFold.Symbolic.Data.Bool
-import ZkFold.Symbolic.Data.Class (SymbolicData)
-import ZkFold.Symbolic.Data.Hash (Hashable (..), preimage)
-import ZkFold.Symbolic.Data.List (List, emptyList, (.:))
-import qualified ZkFold.Symbolic.Data.List as Symbolic.List
-import ZkFold.Symbolic.Data.Maybe
-import Prelude (fst, undefined, ($))
-
-import ZkFold.Symbolic.Ledger.Types
-import ZkFold.Symbolic.Ledger.Validation.Transaction.Core (validateTransactionWithAssetDiff)
-
--- | Witness needed to validate a 'TransactionBatchData'.
-data TransactionBatchDataWitness context = TransactionBatchDataWitness
-  { tbdwTransactions :: List Transaction context
-  -- REVIEW: Add data availability index here to perhaps make slight simplification?
-  }
-  deriving stock (Generic, Generic1)
-  deriving anyclass SymbolicData
-
-instance Signature context => Eq (TransactionBatchDataWitness context)
-
--- | This function extracts boolean from 'validateTransactionBatchDataWithIx, see it for more details.
-validateTransactionBatchData
-  :: forall context
-   . Signature context
-  => Interval context -> TransactionBatchData context -> TransactionBatchDataWitness context -> Bool context
-validateTransactionBatchData tbInterval tbd tbdw = fst $ validateTransactionBatchDataWithIx tbInterval tbd tbdw
-
--- | Validate a 'TransactionBatchData'.
---
--- To check:
---   * All addresses corresponding to spent inputs have same data availability source.
---   * Merkle root is computed correctly.
---   * Online addresses list is computed correctly.
---   * Offline txs list is computed correctly.
---   * Interval of the overarching transaction batch is within the interval of individual transactions.
---   * Txs are valid.
---   * Batch as a whole is balanced.
-validateTransactionBatchDataWithIx
-  :: forall context
-   . Signature context
-  => Interval context
-  -> TransactionBatchData context
-  -> TransactionBatchDataWitness context
-  -> (Bool context, DAIndex context)
-validateTransactionBatchDataWithIx tbInterval TransactionBatchData {..} TransactionBatchDataWitness {..} =
-  let
-    -- Data availability index for this batch. Must not be @Nothing@.
-    resTxAccIx
-      :*: _resTxAccBatchInterval
-      :*: resTxAccIsConsistent -- Whether all relevant addresses have same data availability index.
-      -- And whether the interval of the batch is within the interval of individual transactions.
-      -- And transactions themselves are valid.
-      :*: resTxAccOnlineAddresses -- List of online addresses corresponding to inputs that are being "spent". Note that this may contain duplicates which we'll need to remove later before comparing it with the field inside batch data.
-      :*: resTxAccOfflineAddrsTxs -- List of offline addresses along with their list of transaction hashes.
-      :*: resTxAccOnlineAddrsTxs -- Tree root for online addresses with their transaction hashes.
-      :*: resTxAccValuesDiff -- Accumulated difference between outputs and inputs across all transactions.
-        =
-        Symbolic.List.foldl
-          ( \( txAccIx
-                 :*: txAccBatchInterval
-                 :*: txAccIsConsistent
-                 :*: txAccOnlineAddresses
-                 :*: txAccOfflineAddrsTxs
-                 :*: txAccOnlineAddrsTxs
-                 :*: txAccValuesDiff
-               )
-             tx ->
-                let txOwner' = txOwner tx
-                    _ownerAddrCir :*: ownerAddrIx :*: ownerAddrType =
-                      txOwner' & preimage
-                    jownerAddrIx = just ownerAddrIx
-                    -- If we haven't yet found any index, we use the index of this owner.
-                    txAccIxFinal = ifThenElse (isNothing txAccIx) jownerAddrIx txAccIx
-                    txHash = hasher tx
-                    -- We assume that there is at least one input in the transaction from the address of the owner for following computation. Else the transaction validity check would fail.
-                    newTxAccOfflineAddrsTxs
-                      :*: newTxAccOnlineAddrsTxs
-                      :*: newTxAccOnlineAddresses =
-                        ifThenElse
-                          (isOffline ownerAddrType)
-                          ( -- Add this tx hash to the list of tx hashes.
-                            let updOwnerAddrTxHashes = txHash .: findAddrTxs txOwner' txAccOfflineAddrsTxs
-                             in -- Update the entry of this address with given list.
-                                -- TODO: We could probably do the findAddrTxs and replace in single folding. Circle back to it once symbolic list API is improved.
-                                updateAddrsTxsList txOwner' updOwnerAddrTxHashes txAccOfflineAddrsTxs
-                                  :*: txAccOnlineAddrsTxs
-                                  :*: txAccOnlineAddresses
-                          )
-                          ( txAccOfflineAddrsTxs
-                              :*: undefined -- TODO: Update once Merkle tree API is available.
-                              :*: (txOwner' .: txAccOnlineAddresses)
-                          )
-                    (isTxValid, txValuesDiff) = validateTransactionWithAssetDiff tx
-                    newTxAccIsConsistent =
-                      txAccIsConsistent
-                        && contains (txValidityInterval tx) txAccBatchInterval
-                        && (txAccIxFinal == jownerAddrIx)
-                        && isTxValid
-                 in txAccIxFinal
-                      :*: txAccBatchInterval
-                      :*: newTxAccIsConsistent
-                      :*: newTxAccOnlineAddresses
-                      :*: newTxAccOfflineAddrsTxs
-                      :*: newTxAccOnlineAddrsTxs
-                      :*: addAssetValues txAccValuesDiff txValuesDiff
-          )
-          ( nothing
-              :*: tbInterval
-              :*: (true :: Bool context)
-              :*: emptyList
-              :*: emptyList
-              :*: empty
-              :*: emptyAssetValues
-          )
-          tbdwTransactions
-   in
-    ( isJust resTxAccIx
-        && resTxAccIsConsistent
-        && (tbdOnlineAddresses == removeDuplicates resTxAccOnlineAddresses)
-        && (tbdOfflineTransactions == resTxAccOfflineAddrsTxs)
-        && (tbdMerkleRoot == resTxAccOnlineAddrsTxs)
-        && (resTxAccValuesDiff == emptyAssetValues)
-    , fromJust resTxAccIx
-    )
-
--- | Update the entry for the given address with given list of transaction hashes.
---
--- If the address does not exist, then it is prepended to this list.
-updateAddrsTxsList
-  :: forall context
-   . Signature context
-  => Address context
-  -> List HashSimple context
-  -> List (Address :*: List HashSimple) context
-  -> List (Address :*: List HashSimple) context
-updateAddrsTxsList addr addrTxs addrsTxs =
-  let _ :*: _ :*: newAddrsTxs :*: addrExists =
-        Symbolic.List.foldr
-          ( \(iterAddr :*: iterAddrTxs)
-             ( accAddrToFind
-                 :*: accAddrTxs
-                 :*: accAddrsTxs
-                 :*: accFound
-               ) ->
-                let elemMatches = accAddrToFind == iterAddr
-                 in accAddrToFind
-                      :*: accAddrTxs
-                      :*: ifThenElse
-                        elemMatches
-                        ((iterAddr :*: accAddrTxs) .: accAddrsTxs)
-                        ((iterAddr :*: iterAddrTxs) .: accAddrsTxs)
-                      :*: (accFound || elemMatches)
-          )
-          (addr :*: addrTxs :*: emptyList :*: (false :: Bool context))
-          addrsTxs
-   in ifThenElse
-        addrExists
-        newAddrsTxs
-        ((addr :*: addrTxs) .: addrsTxs)
-
--- TODO: Refactor following once symbolic list is able to support more generic functions.
-
--- | Find a transaction hash list corresponding to given address.
---
--- If the address is not found, we return an empty list.
-findAddrTxs
-  :: forall context
-   . Signature context
-  => Address context
-  -> List (Address :*: List HashSimple) context
-  -> List HashSimple context
-findAddrTxs a ls =
-  sndP $
-    Symbolic.List.foldl
-      ( \(accToFind :*: accList)
-         (addr :*: addrTxHashes) ->
-            accToFind
-              :*: ifThenElse
-                (accToFind == addr)
-                addrTxHashes
-                accList
-      )
-      (a :*: emptyList)
-      ls
-
--- TODO: Use generic 'elem' from symbolic list module once available.
-
--- | Check if an item is present in the list.
-elem
-  :: forall context
-   . Signature context
-  => Address context
-  -> List Address context
-  -> Bool context
-elem x =
-  fstP
-    . Symbolic.List.foldl
-      (\(acc :*: givenElement) y -> (acc || givenElement == y) :*: givenElement)
-      (false :*: x)
-
--- TODO: Use a generic function once available.
-
--- | Remove duplicates from list.
-removeDuplicates
-  :: forall context
-   . Signature context
-  => List Address context -> List Address context
-removeDuplicates =
-  Symbolic.List.foldr
-    (\l acc -> ifThenElse (l `elem` acc) acc (l .: acc))
-    emptyList
diff --git a/symbolic-ledger/src/ZkFold/Symbolic/Ledger/Validation/Transaction/Core.hs b/symbolic-ledger/src/ZkFold/Symbolic/Ledger/Validation/Transaction/Core.hs
deleted file mode 100644
index 43f9689ab..000000000
--- a/symbolic-ledger/src/ZkFold/Symbolic/Ledger/Validation/Transaction/Core.hs
+++ /dev/null
@@ -1,73 +0,0 @@
-{-# LANGUAGE BlockArguments #-}
-{-# LANGUAGE ImpredicativeTypes #-}
-
-module ZkFold.Symbolic.Ledger.Validation.Transaction.Core (
-  validateTransaction,
-  validateTransactionWithAssetDiff,
-) where
-
-import GHC.Generics ((:*:) (..))
-import ZkFold.Control.Conditional (ifThenElse)
-import ZkFold.Data.Eq ((==))
-import ZkFold.Data.Product (fstP)
-import ZkFold.Symbolic.Data.Bool
-import qualified ZkFold.Symbolic.Data.List as Symbolic.List
-import Prelude (fst, undefined, ($), (.))
-
-import ZkFold.Symbolic.Ledger.Types
-
--- | This function extracts boolean from 'validateTransaction', see it for more details.
-validateTransaction
-  :: forall context
-   . Signature context
-  => Transaction context
-  -- ^ 'Transaction' to validate.
-  -> Bool context
-validateTransaction = fst . validateTransactionWithAssetDiff
-
--- | Validate a 'Transaction'.
---
--- To check:
---   * TODO: write checks.
-validateTransactionWithAssetDiff
-  :: forall context
-   . Signature context
-  => Transaction context
-  -- ^ 'Transaction' to validate.
-  -> (Bool context, AssetValues context)
-  -- ^ Validity of transaction along with value difference between outputs and inputs.
-validateTransactionWithAssetDiff tx =
-  let
-    -- Is transaction valid?
-    resTxAccValidity :: Bool context = undefined
-    -- Generated value.
-    resTxAccOutValues :: AssetValues context =
-      fstP $
-        Symbolic.List.foldl
-          ( \(accOutValues :*: accTxOwner) txOut ->
-              ifThenElse
-                (txoAddress txOut == accTxOwner)
-                accOutValues
-                (addAssetValue (txoValue txOut) accOutValues)
-                :*: accTxOwner
-          )
-          (emptyAssetValues :*: txOwner tx)
-          (txOutputs tx)
-    -- Consumed value.
-    resTxAccInValues :: AssetValues context =
-      fstP $
-        Symbolic.List.foldl
-          ( \(accInValues :*: accTxOwner) txInput ->
-              let out = txiOutput txInput
-               in ifThenElse
-                    (txoAddress out == accTxOwner)
-                    accInValues
-                    (addAssetValue (txoValue $ txiOutput txInput) accInValues)
-                    :*: accTxOwner
-          )
-          (emptyAssetValues :*: txOwner tx)
-          (txInputs tx)
-   in
-    ( resTxAccValidity
-    , addAssetValues resTxAccOutValues (negateAssetValues resTxAccInValues)
-    )
diff --git a/symbolic-ledger/src/ZkFold/Symbolic/Ledger/Validation/TransactionBatch.hs b/symbolic-ledger/src/ZkFold/Symbolic/Ledger/Validation/TransactionBatch.hs
new file mode 100644
index 000000000..582e7e8a4
--- /dev/null
+++ b/symbolic-ledger/src/ZkFold/Symbolic/Ledger/Validation/TransactionBatch.hs
@@ -0,0 +1,58 @@
+{-# LANGUAGE ImpredicativeTypes #-}
+{-# LANGUAGE OverloadedRecordDot #-}
+
+module ZkFold.Symbolic.Ledger.Validation.TransactionBatch (
+  TransactionBatchWitness (..),
+  validateTransactionBatch,
+) where
+
+import GHC.Generics ((:*:) (..), (:.:) (..))
+import ZkFold.Algebra.Class (Zero (..), one, (+))
+import ZkFold.Control.Conditional (ifThenElse)
+import ZkFold.Data.Eq ((==))
+import ZkFold.Data.Vector (Vector, Zip (..))
+import ZkFold.Prelude (foldl')
+import ZkFold.Symbolic.Data.Bool (Bool, BoolType (..))
+import ZkFold.Symbolic.Data.FieldElement (FieldElement)
+import ZkFold.Symbolic.Data.MerkleTree (MerkleTree)
+
+import ZkFold.Symbolic.Ledger.Types
+import ZkFold.Symbolic.Ledger.Validation.Transaction (TransactionWitness, validateTransaction)
+
+-- | Transaction batch witness for validating transaction batch.
+newtype TransactionBatchWitness ud i o a t context = TransactionBatchWitness
+  { tbwTransactions :: (Vector t :.: TransactionWitness ud i o a) context
+  }
+
+-- | Validate transaction batch. See note [State validation] for details.
+validateTransactionBatch
+  :: forall ud bo i o a t context
+   . SignatureTransactionBatch ud i o a t context
+  => MerkleTree ud context
+  -- ^ UTxO tree.
+  -> (Vector bo :.: Output a) context
+  -- ^ Bridged out outputs.
+  -> TransactionBatch i o a t context
+  -- ^ Transaction batch.
+  -> TransactionBatchWitness ud i o a t context
+  -- ^ Witness for the transaction batch.
+  -> (Bool :*: MerkleTree ud) context
+  -- ^ Result of validation. First field denotes whether the transaction batch is valid, second one denotes updated UTxO tree.
+validateTransactionBatch utxoTree bridgedOutOutputs tb tbw =
+  let
+    transactionBatchWithWitness = zipWith (:*:) tb.tbTransactions (unComp1 tbw.tbwTransactions)
+    (boCount :*: isValid :*: updatedUTxOTree) =
+      foldl'
+        ( \(boCountAcc :*: isValidAcc :*: accUTxOTree) (tx :*: txw) ->
+            let (txBOuts :*: isTxValid :*: newAccUTxOTree) = validateTransaction accUTxOTree bridgedOutOutputs tx txw
+             in ((boCountAcc + txBOuts) :*: (isValidAcc && isTxValid) :*: newAccUTxOTree)
+        )
+        ((zero :: FieldElement context) :*: true :*: utxoTree)
+        transactionBatchWithWitness
+    bouts =
+      foldl'
+        (\acc output -> ifThenElse (output == nullOutput @a @context) acc (acc + one))
+        zero
+        (unComp1 bridgedOutOutputs)
+   in
+    ((isValid && (bouts == boCount)) :*: updatedUTxOTree)
diff --git a/symbolic-ledger/symbolic-ledger.cabal b/symbolic-ledger/symbolic-ledger.cabal
index 1827a0a43..9ed84f04a 100644
--- a/symbolic-ledger/symbolic-ledger.cabal
+++ b/symbolic-ledger/symbolic-ledger.cabal
@@ -91,21 +91,15 @@ library
     exposed-modules:
       ZkFold.Symbolic.Ledger.Types
       ZkFold.Symbolic.Ledger.Types.Address
-      ZkFold.Symbolic.Ledger.Types.Circuit
-      ZkFold.Symbolic.Ledger.Types.DataAvailability
-      ZkFold.Symbolic.Ledger.Types.Datum
       ZkFold.Symbolic.Ledger.Types.Hash
-      ZkFold.Symbolic.Ledger.Types.Interval
-      ZkFold.Symbolic.Ledger.Types.Output
-      ZkFold.Symbolic.Ledger.Types.Root
+      ZkFold.Symbolic.Ledger.Types.State
       ZkFold.Symbolic.Ledger.Types.Transaction
       ZkFold.Symbolic.Ledger.Types.Transaction.Batch
-      ZkFold.Symbolic.Ledger.Types.Transaction.BatchData
       ZkFold.Symbolic.Ledger.Types.Transaction.Core
       ZkFold.Symbolic.Ledger.Types.Value
-      ZkFold.Symbolic.Ledger.Validation.Transaction.BatchData
-      ZkFold.Symbolic.Ledger.Validation.Transaction.Batch
-      ZkFold.Symbolic.Ledger.Validation.Transaction.Core
+      ZkFold.Symbolic.Ledger.Validation.State
+      ZkFold.Symbolic.Ledger.Validation.Transaction
+      ZkFold.Symbolic.Ledger.Validation.TransactionBatch
     build-depends:
       base                          >= 4.9 && < 5,
       symbolic-base                              ,