Merge pull request #704 from zkFold/689-utxo

feat(#689): updates to symbolic-ledger in sync with 2nd milestone

Author: vlasin

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

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 ------------------------------

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)
   )

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

symbolic-ledger/src/ZkFold/Symbolic/Ledger/Types/Circuit.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.