diff --git a/hydra-node/src/Hydra/HeadLogic.hs b/hydra-node/src/Hydra/HeadLogic.hs index b93ac0477f4..190883bb18c 100644 --- a/hydra-node/src/Hydra/HeadLogic.hs +++ b/hydra-node/src/Hydra/HeadLogic.hs @@ -273,11 +273,16 @@ onInitialChainCollectTx :: ChainStateType tx -> Outcome tx onInitialChainCollectTx st newChainState = - newState HeadOpened{chainState = newChainState, initialUTxO = u0} - <> cause (ClientEffect $ ServerOutput.HeadIsOpen{headId, utxo = u0}) + -- Spec: 𝑈₀ ← ⋃ⁿⱼ₌₁ 𝑈ⱼ + let u0 = fold committed + in -- Spec: L̂ ← 𝑈₀ + -- S⁻ ← snObj(0, 0, 𝑈₀, ∅, ⊥) + -- vˆ , ŝ ← 0 + -- T̂ ← ∅ + -- txω ← ⊥ + newState HeadOpened{chainState = newChainState, initialUTxO = u0} + <> cause (ClientEffect $ ServerOutput.HeadIsOpen{headId, utxo = u0}) where - u0 = fold committed - -- TODO: Do we want to check whether this even matches our local state? For -- example, we do expect `null remainingParties` but what happens if it's -- untrue? @@ -313,24 +318,17 @@ onOpenNetworkReqTx :: tx -> Outcome tx onOpenNetworkReqTx env ledger st ttl tx = - -- REVIEW: would it brake the retry mechanism - -- if we produce this inside `waitApplyTx`? + -- REVIEW: would it brake the retry mechanism if we produce this inside `waitApplyTx`? + -- Spec Gap: this event is missing (newState TransactionReceived{tx} <>) $ - -- Spec: wait L̂ ◦ tx ≠ ⊥ combined with calculating L̂ ◦ tx + -- Spec: wait L̂ ◦ tx ≠ ⊥ waitApplyTx $ \newLocalUTxO -> - -- Spec: if ŝ = s̄ ∧ leader(s̄ + 1) = i - ( if not snapshotInFlight && isLeader parameters party nextSn - then -- REVIEW: this is done in both branches, can we extract it to - -- make it look closer to spec? - -- Spec: Tall ← ̂Tall ∪ {tx} combined with L̂ ← L̂ ◦ tx - - newState TransactionAppliedToLocalUTxO{tx = tx, newLocalUTxO} - <> newState SnapshotRequestDecided{snapshotNumber = nextSn} - <> - -- Spec: multicast (reqSn, vˆ, s̄ + 1, Tˆ , txω ) - cause (NetworkEffect $ ReqSn version nextSn (txId <$> localTxs') decommitTx) - else -- Spec: Tall ← ̂Tall ∪ {tx} combined with L̂ ← L̂ ◦ tx - newState TransactionAppliedToLocalUTxO{tx, newLocalUTxO} + ( -- Spec: T̂ ← T̂ ⋃ {tx} + -- L̂ ← L̂ ◦ tx + newState TransactionAppliedToLocalUTxO{tx, newLocalUTxO} + -- Spec: if ŝ = S⁻.s ∧ leader(S⁻.s + 1) = i + -- multicast (reqSn, vˆ, S⁻.s + 1, T̂ , txω ) + & maybeEmitSnapshot ) <> cause (ClientEffect $ ServerOutput.TxValid headId tx) where @@ -353,6 +351,17 @@ onOpenNetworkReqTx env ledger st ttl tx = -- from allTxs, we would make the head stuck. cause . ClientEffect $ ServerOutput.TxInvalid headId localUTxO tx err + maybeEmitSnapshot outcome = + -- Spec Gap: how snapshotInFlight is calculated + if not snapshotInFlight && isLeader parameters party nextSn + then -- Spec Gap: this event is missing + + outcome + <> newState SnapshotRequestDecided{snapshotNumber = nextSn} + <> + -- Spec: multicast (reqSn, vˆ, S⁻.s + 1, T̂ , txω ) + cause (NetworkEffect $ ReqSn version nextSn (txId <$> localTxs') decommitTx) + else outcome Environment{party} = env Ledger{applyTransactions} = ledger @@ -402,57 +411,70 @@ onOpenNetworkReqSn :: Maybe tx -> Outcome tx onOpenNetworkReqSn env ledger st otherParty sv sn requestedTxIds mDecommitTx = - -- Spec: require v = vˆ - requireReqSv $ - -- Spec: require s = ŝ + 1 and leader(s) = j - requireReqSn $ - -- Spec: wait s̅ = ŝ - waitNoSnapshotInFlight $ - -- Spec: require Ū ◦ txω /= ⊥ combined with ηω ← combine(outputs(txω)) and Ū_active ← Ū ◦ txω - requireApplicableDecommitTx $ \(activeUTxO, mUtxoToDecommit) -> - -- REVIEW: Gap - -- Spec: wait ∀h ∈ Treq : (h, ·) ∈ Tall - waitResolvableTxs $ do - -- REVIEW: Gap - -- Spec: Treq ← {Tall [h] | h ∈ Treq#} - let requestedTxs = mapMaybe (`Map.lookup` allTxs) requestedTxIds - -- Spec: require Ū_active ◦ Treq /= ⊥ combined with η′ ← combine(Û) and Û ← Ū_active ◦ Treq - requireApplyTxs activeUTxO requestedTxs $ \u -> do - -- Spec: ŝ ← s̅ + 1 - let nextConfSn = confSn + 1 - -- NOTE: confSn == seenSn == sn here - let nextSnapshot = - Snapshot - { headId - , number = nextConfSn - , utxo = u - , confirmed = requestedTxIds - , utxoToDecommit = mUtxoToDecommit - , version = version - } - -- Spec: σᵢ - let snapshotSignature = sign signingKey nextSnapshot - -- Spec: multicast (ackSn, ŝ, σᵢ) - (cause (NetworkEffect $ AckSn snapshotSignature sn) <>) $ - do - -- Spec: for loop which updates T̂ and L̂ - let (newLocalTxs, newLocalUTxO) = pruneTransactions u - -- Spec (in aggregate): Tall ← {tx | ∀tx ∈ Tall : tx ∉ Treq } - newState - SnapshotRequested - { snapshot = nextSnapshot - , requestedTxIds - , newLocalUTxO - , newLocalTxs - } + -- Spec: require v = vˆ ∧ s = ŝ + 1 ∧ leader(s) = j + requireReqSn $ + -- Spec: wait ŝ = S⁻.s + waitNoSnapshotInFlight $ + -- Spec: require S⁻.𝑈 ◦ txω ≠ ⊥ + -- ηω ← combine(outputs(txω)) + -- 𝑈_active ← S⁻.𝑈 ◦ txω + requireApplicableDecommitTx $ \(activeUTxO, mUtxoToDecommit) -> + -- Spec Gap: this is missing + -- Spec: wait ∀h ∈ Treq : (h, ·) ∈ T̂ + waitResolvableTxs $ do + -- Spec Gap: this is missing + -- Spec: Treq ← {T̂ [h] | h ∈ Treq#} + let requestedTxs = mapMaybe (`Map.lookup` allTxs) requestedTxIds + -- Spec: require 𝑈_active ◦ Treq ≠ ⊥ + -- 𝑈 ← 𝑈_active ◦ Treq + -- η ← combine(𝑈) + requireApplyTxs activeUTxO requestedTxs $ \u -> do + -- Spec: ŝ ← S⁻.s + 1 + let nextConfSn = confSn + 1 + -- NOTE: confSn == seenSn == sn here + let nextSnapshot = + Snapshot + { headId + , number = nextConfSn + , utxo = u + , confirmed = requestedTxIds + , utxoToDecommit = mUtxoToDecommit + , version = version + } + -- Spec: σᵢ ← MS-Sign(kₕˢⁱᵍ, (cid‖v‖ŝ‖η‖ηω)) + let snapshotSignature = sign signingKey nextSnapshot + -- Spec Gap: missing Σ̂ ← ∅ + -- Spec: multicast (ackSn, ŝ, σᵢ) + (cause (NetworkEffect $ AckSn snapshotSignature sn) <>) $ + do + -- Spec Gap: missing ∀tx ∈ Treq : output (seen, tx) + -- L̂ ← 𝑈 + -- 𝑋 ← T̂ + -- T̂ ← ∅ + + -- Spec: for tx ∈ 𝑋 : L̂ ◦ tx ≠ ⊥ + -- T̂ ← T̂ ⋃ {tx} + -- L̂ ← L̂ ◦ tx + let (newLocalTxs, newLocalUTxO) = pruneTransactions u + newState + SnapshotRequested + { snapshot = nextSnapshot + , requestedTxIds + , newLocalUTxO + , newLocalTxs + } where + requireReqSn continue = + requireReqSv $ + requireReqSnbr continue + requireReqSv continue | sv /= version = Error $ RequireFailed $ ReqSvNumberInvalid{requestedSv = sv, lastSeenSv = version} | otherwise = continue - requireReqSn continue + requireReqSnbr continue | sn /= seenSn + 1 = Error $ RequireFailed $ ReqSnNumberInvalid{requestedSn = sn, lastSeenSn = seenSn} | not (isLeader parameters otherParty sn) = @@ -475,14 +497,14 @@ onOpenNetworkReqSn env ledger st otherParty sv sn requestedTxIds mDecommitTx = case mDecommitTx of Nothing -> cont (confirmedUTxO, Nothing) Just decommitTx -> - -- Spec: require Ū ◦ txω /= ⊥ + -- Spec: require S⁻.𝑈 ◦ txω /= ⊥ case applyTransactions ledger currentSlot confirmedUTxO [decommitTx] of Left (_, err) -> Error $ RequireFailed $ DecommitDoesNotApply decommitTx err Right newConfirmedUTxO -> do -- Spec: ηω ← combine(outputs(txω)) let utxoToDecommit = utxoFromTx decommitTx - -- Spec: Ū_active ← Ū ◦ txω + -- Spec: 𝑈_active ← S⁻.𝑈 ◦ txω let activeUTxO = newConfirmedUTxO `withoutUTxO` utxoToDecommit cont (activeUTxO, Just utxoToDecommit) @@ -553,34 +575,31 @@ onOpenNetworkAckSn Environment{party} openState otherParty snapshotSignature sn requireValidAckSn $ do -- Spec: wait ŝ = s waitOnSeenSnapshot $ \snapshot sigs -> do - -- Spec: (j,.) ∉ ̂Σ + -- Spec: require (j,⋅) ∉ Σ̂ requireNotSignedYet sigs $ do - -- Spec: if ∀k ∈ [1..n] : (k, ·) ∈ Σ̂ + -- Spec Gap: missing Σ̂[j] ← σⱼ + -- Spec: if ∀k ∈ [1..n] : (k,·) ∈ Σ̂ ifAllMembersHaveSigned snapshot sigs $ \sigs' -> do - -- Spec: σ̃ ← MS-ASig(k_H, ̂Σ̂) + -- Spec: σ̃ ← MS-ASig(kₕˢᵉᵗᵘᵖ,Σ̂) let multisig = aggregateInOrder sigs' parties - -- REVIEW: Gap - -- η ← combine(Uˆ) + -- Spec Gap: missing + -- η ← combine(𝑈ˆ) -- ηω ← combine(outputs(txω )) - - -- Spec: require MS-Verify(k ̃H, (cid||vˆ||ŝ||η′||ηω), σ̃) + -- Spec: require MS-Verify(k ̃H, (cid‖v^‖ŝ‖η‖ηω), σ̃) requireVerifiedMultisignature multisig snapshot $ do - -- Spec: S ̄ ← snObj(vˆ, sˆ, Uˆ, Tˆ , txω ) - -- S ̄.σ ← σ ̃ + -- Spec: S⁻ ← snObj(vˆ, ŝ, 𝑈ˆ, T̂ , txω) + -- S⁻.σ ← σ ̃ newState SnapshotConfirmed{snapshot, signatures = multisig} - -- REVIEW: Gap -- Spec: ∀tx ∈ Treq : output(conf, tx) <> cause (ClientEffect $ ServerOutput.SnapshotConfirmed headId snapshot multisig) - -- REVIEW: Gap - -- Spec: if leader(s̄ + 1) = i ∧ Tˆ ≠ ∅ - -- multicast (reqSn, vˆ, s̄ + 1, Tˆ, txω ) - & maybeEmitSnapshot - -- REVIEW: Gap - -- Spec: if txω ̸= ⊥ - -- postTx (decrement, vˆ, sˆ, η, ηω ) - -- output(conf, txω ) + -- Spec: if txω ≠ ⊥ + -- postTx (decrement, vˆ, ŝ, η, ηω) + -- output (conf, txω ) & maybeEmitDecrementTx snapshot multisig + -- Spec: if leader(s + 1) = i ∧ T̂ ≠ ∅ + -- multicast (reqSn, vˆ, S⁻.s + 1, T̂, txω) + & maybeEmitSnapshot where seenSn = seenSnapshotNumber seenSnapshot @@ -629,6 +648,7 @@ onOpenNetworkAckSn Environment{party} openState otherParty snapshotSignature sn then outcome <> newState SnapshotRequestDecided{snapshotNumber = nextSn} + -- Spec Gap: how S⁻.s + 1 is calculated is not the same as nextSn <> cause (NetworkEffect $ ReqSn version nextSn (txId <$> localTxs) decommitTx) else outcome @@ -746,18 +766,17 @@ onOpenNetworkReqDec :: tx -> Outcome tx onOpenNetworkReqDec env ledger ttl openState decommitTx = - -- Spec: wait txω =⊥ ∧ L̂ ◦ tx ≠ ⊥ combined + -- Spec: wait txω =⊥ ∧ L̂ ◦ tx ≠ ⊥ waitOnApplicableDecommit $ \newLocalUTxO -> let decommitUTxO = utxoFromTx decommitTx activeUTxO = newLocalUTxO `withoutUTxO` decommitUTxO - in -- Spec: txω ← tx combined with L̂ \ inputs(tx) + in -- Spec: L̂ ← L̂ \ inputs(tx) + -- txω ← tx newState (DecommitRecorded decommitTx activeUTxO) <> cause (ClientEffect $ ServerOutput.DecommitRequested headId decommitUTxO) - -- Spec: if ŝ = s̄ ∧ leader(s̄ + 1) = i - <> if isLeader parameters party nextSn - then -- Spec: multicast (reqSn, vˆ, s̄ + 1, Tˆ , txω ) - cause (NetworkEffect (ReqSn version nextSn (txId <$> localTxs) (Just decommitTx))) - else noop + -- Spec: if ŝ = S⁻.s ∧ leader(S⁻.s + 1) = i + -- multicast (reqSn, vˆ, S⁻.s + 1, T̂ , txω ) + <> maybeEmitSnapshot where waitOnApplicableDecommit cont = case mExistingDecommitTx of @@ -785,6 +804,11 @@ onOpenNetworkReqDec env ledger ttl openState decommitTx = -- REVIW: cause . ClientEffect $ ServerOutput.DecommitInvalid Error $ RequireFailed $ DecommitTxInFlight{decommitTx = existingDecommitTx} + maybeEmitSnapshot = + if isLeader parameters party nextSn + then cause (NetworkEffect (ReqSn version nextSn (txId <$> localTxs) (Just decommitTx))) + else noop + Environment{party} = env Ledger{applyTransactions} = ledger @@ -818,15 +842,15 @@ onOpenNetworkReqDec env ledger ttl openState decommitTx = -- __Transition__: 'OpenState' → 'OpenState' onOpenChainDecrementTx :: IsTx tx => Environment -> OpenState tx -> Outcome tx onOpenChainDecrementTx Environment{party} openState - | -- Spec: if outputs(txω) = Uω + | -- Spec: if outputs(txω) = 𝑈ω -- REVIEW: should we get Uω from observation instead of local state? (utxoFromTx <$> decommitTx) == utxoToDecommit = -- Spec: txω ← ⊥ -- vˆ ← v newState DecommitFinalized <> cause (ClientEffect $ ServerOutput.DecommitFinalized{headId}) - -- Spec: if ŝ = s̄ ∧ leader(s̄ + 1) = i - -- multicast (reqSn, vˆ, s̄ + 1, Tˆ , txω ) + -- Spec: if ŝ = S⁻.s ∧ leader(S⁻.s + 1) = i + -- multicast (reqSn, vˆ, S⁻.s + 1, T̂ , txω ) & maybeEmitSnapshot | otherwise = noop where @@ -863,10 +887,10 @@ onOpenClientClose :: OpenState tx -> Outcome tx onOpenClientClose st = - -- Spec: η ← combine(S ̄.U) - -- ηω ← combine(outputs(S ̄.txω)) - -- ξ ← S ̄.σ - -- postTx (close, S ̄.v, S ̄.s, η, ηω,ξ) + -- Spec: η ← combine(S⁻.𝑈) + -- ηω ← combine(outputs(S⁻.txω)) + -- ξ ← S⁻.σ + -- postTx (close, S⁻.v, S⁻.s, η, ηω,ξ) cause OnChainEffect { postChainTx =