Updated spec and align some details

Author: ch1bo

flake.lock

@@ -9,7 +9,8 @@
     flake-parts.url = "github:hercules-ci/flake-parts";
     haskellNix.url = "github:input-output-hk/haskell.nix";
     hydra-coding-standards.url = "github:cardano-scaling/hydra-coding-standards/0.6.0";
-    hydra-spec.url = "github:cardano-scaling/hydra-formal-specification";
+    # TODO: update to master
+    hydra-spec.url = "github:cardano-scaling/hydra-formal-specification/deposit-protocol-changes";
     iohk-nix.url = "github:input-output-hk/iohk-nix";
     lint-utils = {
       url = "github:homotopic/lint-utils";

flake.nix

@@ -70,7 +70,6 @@ import Hydra.Tx (
   HeadParameters (..),
   UTxOType,
   headSeedToTxIn,
-  txInToHeadSeed,
  )
 import Hydra.Tx.ContestationPeriod (toNominalDiffTime)
 import Hydra.Tx.Deposit (DepositObservation (..), depositTx)
@@ -179,7 +178,7 @@ mkChain tracer queryTimeHandle wallet ctx LocalChainState{getLatest} submitTx =
           validBefore <- case currentPointInTime timeHandle of
             -- XXX: We only need the current slot and this would never fail
             Left failureReason -> throwError FailedToConstructDepositTx{failureReason}
-            Right (s, _) -> pure $ s + 200 -- XXX: configurable and unify with maxGraceTime
+            Right (s, _) -> pure $ s + fromInteger (truncate maxGraceTime)
           lift . finalizeTx wallet ctx spendableUTxO lookupUTxO $
             depositTx (networkId ctx) headId commitBlueprintTx validBefore deadline
     , -- Submit a cardano transaction to the cardano-node using the

hydra-node/src/Hydra/Chain/Direct/Handlers.hs

@@ -91,7 +91,6 @@ import Hydra.Tx (
   mkSimpleBlueprintTx,
   partyToChain,
   registryUTxO,
-  txInToHeadSeed,
   utxoFromTx,
  )
 import Hydra.Tx.Abort (AbortTxError (..), abortTx)
@@ -798,7 +797,7 @@ observeInit _ctx _allVerificationKeys tx = do
 
 -- | Observe an commit transition using a 'InitialState' and 'observeCommitTx'.
 -- NOTE: This function is a bit fragile as it assumes commit output on first
--- output whilte the underlying observeCommitTx could deal with commit outputs
+-- output while the underlying observeCommitTx could deal with commit outputs
 -- at any index. Only use this function in tests and benchmarks.
 observeCommit ::
   ChainContext ->

hydra-node/src/Hydra/Chain/Direct/State.hs

@@ -403,15 +403,17 @@ onOpenNetworkReqSn ::
   Maybe (TxIdType tx) ->
   Outcome tx
 onOpenNetworkReqSn env ledger st otherParty sv sn requestedTxIds mDecommitTx mDepositTxId =
-  -- Spec: require s = ŝ + 1 ∧ leader(s) = j
+  -- Spec: require v = v̂ ∧ s = ŝ + 1 ∧ leader(s) = j
   requireReqSn $
     -- Spec: wait ŝ = ̅S.s
     waitNoSnapshotInFlight $
+      -- TODO: is this really needed?
       -- Spec: wait v = v̂
       waitOnSnapshotVersion $
-        -- Spec: require tx𝜔 = ⊥ ∨ 𝑈𝛼 = ∅
+        -- TODO: this is missing!? Spec: require tx𝜔 = ⊥ ∨ tx𝛼 = ⊥
+        -- Require any pending utxo to decommit to be consistent
         requireApplicableDecommitTx $ \(activeUTxOAfterDecommit, mUtxoToDecommit) ->
-          -- TODO: Spec updates for these checks in here
+          -- Wait for the deposit and require any pending commit to be consistent
           waitForDeposit activeUTxOAfterDecommit $ \(activeUTxO, mUtxoToCommit) ->
             -- Resolve transactions by-id
             waitResolvableTxs $ \requestedTxs -> do
@@ -487,14 +489,11 @@ onOpenNetworkReqSn env ledger st otherParty sv sn requestedTxIds mDecommitTx mDe
     case mDepositTxId of
       Nothing -> cont (activeUTxOAfterDecommit, Nothing)
       Just depositTxId ->
+        -- XXX: We may need to wait quite long here and this makes losing
+        -- the 'ReqSn' due to a restart (fail-recovery) quite likely
         case Map.lookup depositTxId pendingDeposits of
-          -- REVIEW: Is this also a wait? It could be that another node has such
-          -- low deposit period that we have not yet seen the deposit on chain?
-          Nothing -> Error $ RequireFailed NoMatchingDeposit
+          Nothing -> wait WaitOnDepositObserved{depositTxId}
           Just Deposit{status, deposited}
-            -- TODO: this needs to go into the spec!
-            -- XXX: We may need to wait quite long here and this makes losing
-            -- the 'ReqSn' due to a restart (fail-recovery) quite likely
             | status == Inactive -> wait WaitOnDepositActivation{depositTxId}
             | status == Expired -> Error $ RequireFailed RequestedDepositExpired{depositTxId}
             | otherwise ->
@@ -503,7 +502,7 @@ onOpenNetworkReqSn env ledger st otherParty sv sn requestedTxIds mDecommitTx mDe
                 if sv == confVersion && isJust confUTxOToCommit
                   then
                     if confUTxOToCommit == Just deposited
-                      then cont (activeUTxOAfterDecommit <> fromMaybe mempty confUTxOToCommit, confUTxOToCommit)
+                      then cont (activeUTxOAfterDecommit <> deposited, confUTxOToCommit)
                       else Error $ RequireFailed ReqSnCommitNotSettled
                   else do
                     let activeUTxOAfterCommit = activeUTxOAfterDecommit <> deposited

hydra-node/src/Hydra/HeadLogic.hs

@@ -233,6 +233,7 @@ data WaitReason tx
   | WaitOnNotApplicableDecommitTx {notApplicableReason :: DecommitInvalidReason tx}
   | WaitOnUnresolvedCommit {commitUTxO :: UTxOType tx}
   | WaitOnUnresolvedDecommit {decommitTx :: tx}
+  | WaitOnDepositObserved {depositTxId :: TxIdType tx}
   | WaitOnDepositActivation {depositTxId :: TxIdType tx}
   deriving stock (Generic)