Add "update validation" to the Symbolic Ledger library

src/ZkFold/Symbolic/Ledger/Validation/Common.hs

@@ -0,0 +1,12 @@
+module ZkFold.Symbolic.Ledger.Validation.Common where
+
+import           Prelude                      hiding (Bool, Eq (..), all, length, splitAt, zip, (&&),
+                                                (*), (+), (==))
+
+import           ZkFold.Symbolic.Ledger.Types
+
+-- | References in the chain of updates are consistent.
+updateChainIsValid ::
+      UpdateChain context
+   -> Bool context
+updateChainIsValid _ = undefined

src/ZkFold/Symbolic/Ledger/Validation/PrivateInput.hs

@@ -7,7 +7,7 @@ import           ZkFold.Symbolic.Data.Bool                (all, any, (&&))
 import           ZkFold.Symbolic.Data.Eq                  (Eq (..))
 import           ZkFold.Symbolic.Data.List                (filter, last, (.:), head, emptyList)
 import           ZkFold.Symbolic.Ledger.Types
-import           ZkFold.Symbolic.Ledger.Validation.Update (updateChainIsValid)
+import           ZkFold.Symbolic.Ledger.Validation.Common (updateChainIsValid)
 
 -- | Witness data that is required to prove the validity of a private transaction input.
 type PrivateInputWitness context =

src/ZkFold/Symbolic/Ledger/Validation/PublicInput.hs

@@ -7,7 +7,7 @@ import           ZkFold.Symbolic.Data.Bool                (all, any, (&&))
 import           ZkFold.Symbolic.Data.Eq                  (Eq (..))
 import           ZkFold.Symbolic.Data.List                (last, head)
 import           ZkFold.Symbolic.Ledger.Types
-import           ZkFold.Symbolic.Ledger.Validation.Update (updateChainIsValid)
+import           ZkFold.Symbolic.Ledger.Validation.Common (updateChainIsValid)
 
 -- | Witness data that is required to prove the validity of a public transaction input.
 type PublicInputWitness context = UpdateChain context

src/ZkFold/Symbolic/Ledger/Validation/Update.hs

@@ -1,12 +1,25 @@
 module ZkFold.Symbolic.Ledger.Validation.Update where
 
-import           Prelude                                       hiding (Bool, Eq (..), all, length, splitAt, zip, (&&),
-                                                                (*), (+), (==))
+import           Prelude                                 hiding (Bool, Eq (..), all, length, splitAt, zip, (&&),
+                                                            (*), (+), (==))
 
+import           ZkFold.Symbolic.Data.Bool               (BoolType(..))
+import           ZkFold.Symbolic.Data.Eq                 (Eq(..))
 import           ZkFold.Symbolic.Ledger.Types
+import           ZkFold.Symbolic.Ledger.Validation.Block (BlockWitness, newBlockIsValid)
 
--- | References in the chain of updates are consistent.
-updateChainIsValid ::
-      UpdateChain context
+type UpdateWitness context = (Block context, BlockWitness context)
+
+-- | Check if a new update is valid given the latest valid update.
+newUpdateIsValid ::
+      Signature context
+   => UpdateId context
+   -- ^ The id of the latest valid update.
+   -> Update context
+   -- ^ The new update to check.
+   -> UpdateWitness context
+   -- ^ The witness data for the new update.
    -> Bool context
-updateChainIsValid _ = undefined
+newUpdateIsValid lastUpdateId Update {..} (wBlock, wBlockWitness) =
+      lastUpdateId == updateReference
+   && newBlockIsValid lastUpdateId wBlock wBlockWitness

zkfold-base.cabal

@@ -190,6 +190,7 @@ library
       ZkFold.Symbolic.Ledger.Types.Value
       ZkFold.Symbolic.Ledger.Validation.Block
       ZkFold.Symbolic.Ledger.Validation.Contract
+      ZkFold.Symbolic.Ledger.Validation.Common
       ZkFold.Symbolic.Ledger.Validation.PrivateInput
       ZkFold.Symbolic.Ledger.Validation.PublicInput
       ZkFold.Symbolic.Ledger.Validation.Transaction