{-# LANGUAGE DuplicateRecordFields #-}
{-# OPTIONS_GHC -Wno-ambiguous-fields #-}

-- | Implements the Head Protocol's /state machine/ as /pure functions/ in an event sourced manner.
--
-- More specifically, the 'update' will handle 'Input's (or rather "commands" in
-- event sourcing speak) and convert that into a list of side-'Effect's and
-- 'StateChanged' events, which in turn are 'aggregate'd into a single
-- 'HeadState'.
--
-- As the specification is using a more imperative way of specifying the protocl
-- behavior, one would find the decision logic in 'update' while state updates
-- can be found in the corresponding 'aggregate' branch.
module Hydra.HeadLogic (
  module Hydra.HeadLogic,
  module Hydra.HeadLogic.Input,
  module Hydra.HeadLogic.Error,
  module Hydra.HeadLogic.State,
  module Hydra.HeadLogic.Outcome,
) where

import Hydra.Prelude

import Data.List (elemIndex)
import Data.Map.Strict qualified as Map
import Data.Set ((\\))
import Data.Set qualified as Set
import GHC.Records (getField)
import Hydra.API.ClientInput (ClientInput (..))
import Hydra.API.ServerOutput (DecommitInvalidReason (..))
import Hydra.API.ServerOutput qualified as ServerOutput
import Hydra.Chain (
  ChainEvent (..),
  ChainStateHistory,
  OnChainTx (..),
  PostChainTx (..),
  initHistory,
  pushNewState,
  rollbackHistory,
 )
import Hydra.Chain.ChainState (ChainSlot, IsChainState (..))
import Hydra.HeadLogic.Error (
  LogicError (..),
  RequirementFailure (..),
 )
import Hydra.HeadLogic.Input (Input (..), TTL)
import Hydra.HeadLogic.Outcome (
  Effect (..),
  Outcome (..),
  StateChanged (..),
  WaitReason (..),
  cause,
  causes,
  newState,
  noop,
  wait,
 )
import Hydra.HeadLogic.State (
  ClosedState (..),
  Committed,
  CoordinatedHeadState (..),
  HeadState (..),
  IdleState (IdleState, chainState),
  InitialState (..),
  OpenState (..),
  PendingCommits,
  SeenSnapshot (..),
  seenSnapshotNumber,
  setChainState,
 )
import Hydra.Ledger (
  Ledger (..),
  applyTransactions,
  outputsOfTx,
 )
import Hydra.Network.Message (Connectivity (..), HydraVersionedProtocolNumber (..), KnownHydraVersions (..), Message (..), NetworkEvent (..))
import Hydra.Tx (
  HeadId,
  HeadSeed,
  IsTx (..),
  TxIdType,
  UTxOType,
  mkHeadParameters,
  txId,
  utxoFromTx,
  withoutUTxO,
 )
import Hydra.Tx.Crypto (
  Signature,
  Verified (..),
  aggregateInOrder,
  sign,
  verifyMultiSignature,
 )
import Hydra.Tx.Environment (Environment (..))
import Hydra.Tx.HeadParameters (HeadParameters (..))
import Hydra.Tx.OnChainId (OnChainId)
import Hydra.Tx.Party (Party (vkey))
import Hydra.Tx.Snapshot (ConfirmedSnapshot (..), Snapshot (..), SnapshotNumber, SnapshotVersion, getSnapshot)

defaultTTL :: TTL
defaultTTL :: TTL
defaultTTL = TTL
5

onConnectionEvent :: Connectivity -> Outcome tx
onConnectionEvent :: forall tx. Connectivity -> Outcome tx
onConnectionEvent = \case
  Connected{NodeId
nodeId :: NodeId
$sel:nodeId:Connected :: Connectivity -> NodeId
nodeId} ->
    [Effect tx] -> Outcome tx
forall tx. [Effect tx] -> Outcome tx
causes [ServerOutput tx -> Effect tx
forall tx. ServerOutput tx -> Effect tx
ClientEffect (NodeId -> ServerOutput tx
forall tx. NodeId -> ServerOutput tx
ServerOutput.PeerConnected NodeId
nodeId)]
  Disconnected{NodeId
$sel:nodeId:Connected :: Connectivity -> NodeId
nodeId :: NodeId
nodeId} ->
    [Effect tx] -> Outcome tx
forall tx. [Effect tx] -> Outcome tx
causes [ServerOutput tx -> Effect tx
forall tx. ServerOutput tx -> Effect tx
ClientEffect (NodeId -> ServerOutput tx
forall tx. NodeId -> ServerOutput tx
ServerOutput.PeerDisconnected NodeId
nodeId)]
  HandshakeFailure{Host
remoteHost :: Host
$sel:remoteHost:Connected :: Connectivity -> Host
remoteHost, HydraVersionedProtocolNumber
ourVersion :: HydraVersionedProtocolNumber
$sel:ourVersion:Connected :: Connectivity -> HydraVersionedProtocolNumber
ourVersion, KnownHydraVersions
theirVersions :: KnownHydraVersions
$sel:theirVersions:Connected :: Connectivity -> KnownHydraVersions
theirVersions} ->
    [Effect tx] -> Outcome tx
forall tx. [Effect tx] -> Outcome tx
causes
      [ ServerOutput tx -> Effect tx
forall tx. ServerOutput tx -> Effect tx
ClientEffect
          ( ServerOutput.PeerHandshakeFailure
              { Host
remoteHost :: Host
$sel:remoteHost:PeerConnected :: Host
remoteHost
              , $sel:ourVersion:PeerConnected :: TTL
ourVersion = HydraVersionedProtocolNumber -> TTL
getVersion HydraVersionedProtocolNumber
ourVersion
              , $sel:theirVersions:PeerConnected :: [TTL]
theirVersions = KnownHydraVersions -> [TTL]
getKnownVersions KnownHydraVersions
theirVersions
              }
          )
      ]
   where
    getVersion :: HydraVersionedProtocolNumber -> TTL
getVersion MkHydraVersionedProtocolNumber{TTL
hydraVersionedProtocolNumber :: TTL
$sel:hydraVersionedProtocolNumber:MkHydraVersionedProtocolNumber :: HydraVersionedProtocolNumber -> TTL
hydraVersionedProtocolNumber} = TTL
hydraVersionedProtocolNumber

    getKnownVersions :: KnownHydraVersions -> [TTL]
getKnownVersions = \case
      KnownHydraVersions
NoKnownHydraVersions -> []
      KnownHydraVersions{[HydraVersionedProtocolNumber]
fromKnownHydraVersions :: [HydraVersionedProtocolNumber]
$sel:fromKnownHydraVersions:KnownHydraVersions :: KnownHydraVersions -> [HydraVersionedProtocolNumber]
fromKnownHydraVersions} -> HydraVersionedProtocolNumber -> TTL
getVersion (HydraVersionedProtocolNumber -> TTL)
-> [HydraVersionedProtocolNumber] -> [TTL]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [HydraVersionedProtocolNumber]
fromKnownHydraVersions

-- * The Coordinated Head protocol

-- ** On-Chain Protocol

-- | Client request to init the head. This leads to an init transaction on chain,
-- containing the head parameters.
--
-- __Transition__: 'IdleState' → 'IdleState'
onIdleClientInit ::
  Environment ->
  Outcome tx
onIdleClientInit :: forall tx. Environment -> Outcome tx
onIdleClientInit Environment
env =
  Effect tx -> Outcome tx
forall tx. Effect tx -> Outcome tx
cause OnChainEffect{$sel:postChainTx:ClientEffect :: PostChainTx tx
postChainTx = InitTx{[OnChainId]
participants :: [OnChainId]
$sel:participants:InitTx :: [OnChainId]
participants, HeadParameters
headParameters :: HeadParameters
$sel:headParameters:InitTx :: HeadParameters
headParameters}}
 where
  headParameters :: HeadParameters
headParameters = Environment -> HeadParameters
mkHeadParameters Environment
env

  Environment{[OnChainId]
participants :: [OnChainId]
$sel:participants:Environment :: Environment -> [OnChainId]
participants} = Environment
env

-- | Observe an init transaction, initialize parameters in an 'InitialState' and
-- notify clients that they can now commit.
--
-- __Transition__: 'IdleState' → 'InitialState'
onIdleChainInitTx ::
  Environment ->
  -- | New chain state.
  ChainStateType tx ->
  HeadId ->
  HeadSeed ->
  HeadParameters ->
  [OnChainId] ->
  Outcome tx
onIdleChainInitTx :: forall tx.
Environment
-> ChainStateType tx
-> HeadId
-> HeadSeed
-> HeadParameters
-> [OnChainId]
-> Outcome tx
onIdleChainInitTx Environment
env ChainStateType tx
newChainState HeadId
headId HeadSeed
headSeed HeadParameters
headParameters [OnChainId]
participants
  | Set Party
configuredParties Set Party -> Set Party -> Bool
forall a. Eq a => a -> a -> Bool
== Set Party
initializedParties
      Bool -> Bool -> Bool
&& Key (Set Party)
Party
party Key (Set Party) -> Set Party -> Bool
forall t. StaticMap t => Key t -> t -> Bool
`member` Set Party
initializedParties
      Bool -> Bool -> Bool
&& ContestationPeriod
configuredContestationPeriod ContestationPeriod -> ContestationPeriod -> Bool
forall a. Eq a => a -> a -> Bool
== ContestationPeriod
contestationPeriod
      Bool -> Bool -> Bool
&& [OnChainId] -> Set OnChainId
forall a. Ord a => [a] -> Set a
Set.fromList [OnChainId]
configuredParticipants Set OnChainId -> Set OnChainId -> Bool
forall a. Eq a => a -> a -> Bool
== [OnChainId] -> Set OnChainId
forall a. Ord a => [a] -> Set a
Set.fromList [OnChainId]
participants =
      StateChanged tx -> Outcome tx
forall tx. StateChanged tx -> Outcome tx
newState
        HeadInitialized
          { $sel:parameters:HeadInitialized :: HeadParameters
parameters = HeadParameters
headParameters
          , $sel:chainState:HeadInitialized :: ChainStateType tx
chainState = ChainStateType tx
newChainState
          , HeadId
headId :: HeadId
$sel:headId:HeadInitialized :: HeadId
headId
          , HeadSeed
headSeed :: HeadSeed
$sel:headSeed:HeadInitialized :: HeadSeed
headSeed
          }
        Outcome tx -> Outcome tx -> Outcome tx
forall a. Semigroup a => a -> a -> a
<> Effect tx -> Outcome tx
forall tx. Effect tx -> Outcome tx
cause (ServerOutput tx -> Effect tx
forall tx. ServerOutput tx -> Effect tx
ClientEffect (ServerOutput tx -> Effect tx) -> ServerOutput tx -> Effect tx
forall a b. (a -> b) -> a -> b
$ ServerOutput.HeadIsInitializing{HeadId
headId :: HeadId
$sel:headId:PeerConnected :: HeadId
headId, [Party]
parties :: [Party]
$sel:parties:PeerConnected :: [Party]
parties})
  | Bool
otherwise =
      Effect tx -> Outcome tx
forall tx. Effect tx -> Outcome tx
cause
        (Effect tx -> Outcome tx)
-> (ServerOutput tx -> Effect tx) -> ServerOutput tx -> Outcome tx
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ServerOutput tx -> Effect tx
forall tx. ServerOutput tx -> Effect tx
ClientEffect
        (ServerOutput tx -> Outcome tx) -> ServerOutput tx -> Outcome tx
forall a b. (a -> b) -> a -> b
$ ServerOutput.IgnoredHeadInitializing
          { HeadId
headId :: HeadId
$sel:headId:PeerConnected :: HeadId
headId
          , ContestationPeriod
contestationPeriod :: ContestationPeriod
$sel:contestationPeriod:PeerConnected :: ContestationPeriod
contestationPeriod
          , [Party]
parties :: [Party]
$sel:parties:PeerConnected :: [Party]
parties
          , [OnChainId]
participants :: [OnChainId]
$sel:participants:PeerConnected :: [OnChainId]
participants
          }
 where
  initializedParties :: Set Party
initializedParties = [Party] -> Set Party
forall a. Ord a => [a] -> Set a
Set.fromList [Party]
parties

  configuredParties :: Set Party
configuredParties = [Party] -> Set Party
forall a. Ord a => [a] -> Set a
Set.fromList (Party
party Party -> [Party] -> [Party]
forall a. a -> [a] -> [a]
: [Party]
otherParties)

  HeadParameters{[Party]
parties :: [Party]
$sel:parties:HeadParameters :: HeadParameters -> [Party]
parties, ContestationPeriod
contestationPeriod :: ContestationPeriod
$sel:contestationPeriod:HeadParameters :: HeadParameters -> ContestationPeriod
contestationPeriod} = HeadParameters
headParameters

  Environment
    { Party
party :: Party
$sel:party:Environment :: Environment -> Party
party
    , [Party]
otherParties :: [Party]
$sel:otherParties:Environment :: Environment -> [Party]
otherParties
    , $sel:contestationPeriod:Environment :: Environment -> ContestationPeriod
contestationPeriod = ContestationPeriod
configuredContestationPeriod
    , $sel:participants:Environment :: Environment -> [OnChainId]
participants = [OnChainId]
configuredParticipants
    } = Environment
env

-- | Observe a commit transaction and record the committed UTxO in the state.
-- Also, if this is the last commit to be observed, post a collect-com
-- transaction on-chain.
--
-- __Transition__: 'InitialState' → 'InitialState'
onInitialChainCommitTx ::
  Monoid (UTxOType tx) =>
  InitialState tx ->
  -- | New chain state
  ChainStateType tx ->
  -- | Comitting party
  Party ->
  -- | Committed UTxO
  UTxOType tx ->
  Outcome tx
onInitialChainCommitTx :: forall tx.
Monoid (UTxOType tx) =>
InitialState tx
-> ChainStateType tx -> Party -> UTxOType tx -> Outcome tx
onInitialChainCommitTx InitialState tx
st ChainStateType tx
newChainState Party
pt UTxOType tx
utxo =
  StateChanged tx -> Outcome tx
forall tx. StateChanged tx -> Outcome tx
newState CommittedUTxO{$sel:party:HeadInitialized :: Party
party = Party
pt, $sel:committedUTxO:HeadInitialized :: UTxOType tx
committedUTxO = UTxOType tx
utxo, $sel:chainState:HeadInitialized :: ChainStateType tx
chainState = ChainStateType tx
newChainState}
    Outcome tx -> Outcome tx -> Outcome tx
forall a. Semigroup a => a -> a -> a
<> [Effect tx] -> Outcome tx
forall tx. [Effect tx] -> Outcome tx
causes
      ( Effect tx
notifyClient
          Effect tx -> [Effect tx] -> [Effect tx]
forall a. a -> [a] -> [a]
: [Effect tx
postCollectCom | Bool
canCollectCom]
      )
 where
  notifyClient :: Effect tx
notifyClient = ServerOutput tx -> Effect tx
forall tx. ServerOutput tx -> Effect tx
ClientEffect (ServerOutput tx -> Effect tx) -> ServerOutput tx -> Effect tx
forall a b. (a -> b) -> a -> b
$ ServerOutput.Committed{HeadId
$sel:headId:PeerConnected :: HeadId
headId :: HeadId
headId, $sel:party:PeerConnected :: Party
party = Party
pt, UTxOType tx
utxo :: UTxOType tx
$sel:utxo:PeerConnected :: UTxOType tx
utxo}

  postCollectCom :: Effect tx
postCollectCom =
    OnChainEffect
      { $sel:postChainTx:ClientEffect :: PostChainTx tx
postChainTx =
          CollectComTx
            { $sel:utxo:InitTx :: UTxOType tx
utxo = Map Party (UTxOType tx) -> UTxOType tx
forall m. Monoid m => Map Party m -> m
forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m
fold Map Party (UTxOType tx)
newCommitted
            , HeadId
headId :: HeadId
$sel:headId:InitTx :: HeadId
headId
            , $sel:headParameters:InitTx :: HeadParameters
headParameters = HeadParameters
parameters
            }
      }

  canCollectCom :: Bool
canCollectCom = Set Party -> Bool
forall a. Set a -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null Set Party
remainingParties

  remainingParties :: Set Party
remainingParties = Party -> Set Party -> Set Party
forall a. Ord a => a -> Set a -> Set a
Set.delete Party
pt Set Party
pendingCommits

  newCommitted :: Map Party (UTxOType tx)
newCommitted = Party
-> UTxOType tx
-> Map Party (UTxOType tx)
-> Map Party (UTxOType tx)
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Party
pt UTxOType tx
utxo Map Party (UTxOType tx)
committed

  InitialState{Set Party
pendingCommits :: Set Party
$sel:pendingCommits:InitialState :: forall tx. InitialState tx -> Set Party
pendingCommits, Map Party (UTxOType tx)
committed :: Map Party (UTxOType tx)
$sel:committed:InitialState :: forall tx. InitialState tx -> Committed tx
committed, HeadId
headId :: HeadId
$sel:headId:InitialState :: forall tx. InitialState tx -> HeadId
headId, HeadParameters
parameters :: HeadParameters
$sel:parameters:InitialState :: forall tx. InitialState tx -> HeadParameters
parameters} = InitialState tx
st

-- | Client request to abort the head. This leads to an abort transaction on
-- chain, reimbursing already committed UTxOs.
--
-- __Transition__: 'InitialState' → 'InitialState'
onInitialClientAbort ::
  Monoid (UTxOType tx) =>
  InitialState tx ->
  Outcome tx
onInitialClientAbort :: forall tx. Monoid (UTxOType tx) => InitialState tx -> Outcome tx
onInitialClientAbort InitialState tx
st =
  Effect tx -> Outcome tx
forall tx. Effect tx -> Outcome tx
cause OnChainEffect{$sel:postChainTx:ClientEffect :: PostChainTx tx
postChainTx = AbortTx{$sel:utxo:InitTx :: UTxOType tx
utxo = Map Party (UTxOType tx) -> UTxOType tx
forall m. Monoid m => Map Party m -> m
forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m
fold Map Party (UTxOType tx)
committed, HeadSeed
headSeed :: HeadSeed
$sel:headSeed:InitTx :: HeadSeed
headSeed}}
 where
  InitialState{Map Party (UTxOType tx)
$sel:committed:InitialState :: forall tx. InitialState tx -> Committed tx
committed :: Map Party (UTxOType tx)
committed, HeadSeed
headSeed :: HeadSeed
$sel:headSeed:InitialState :: forall tx. InitialState tx -> HeadSeed
headSeed} = InitialState tx
st

-- | Observe an abort transaction by switching the state and notifying clients
-- about it.
--
-- __Transition__: 'InitialState' → 'IdleState'
onInitialChainAbortTx ::
  Monoid (UTxOType tx) =>
  -- | New chain state
  ChainStateType tx ->
  Committed tx ->
  HeadId ->
  Outcome tx
onInitialChainAbortTx :: forall tx.
Monoid (UTxOType tx) =>
ChainStateType tx -> Committed tx -> HeadId -> Outcome tx
onInitialChainAbortTx ChainStateType tx
newChainState Committed tx
committed HeadId
headId =
  StateChanged tx -> Outcome tx
forall tx. StateChanged tx -> Outcome tx
newState HeadAborted{$sel:chainState:HeadInitialized :: ChainStateType tx
chainState = ChainStateType tx
newChainState}
    Outcome tx -> Outcome tx -> Outcome tx
forall a. Semigroup a => a -> a -> a
<> Effect tx -> Outcome tx
forall tx. Effect tx -> Outcome tx
cause (ServerOutput tx -> Effect tx
forall tx. ServerOutput tx -> Effect tx
ClientEffect (ServerOutput tx -> Effect tx) -> ServerOutput tx -> Effect tx
forall a b. (a -> b) -> a -> b
$ ServerOutput.HeadIsAborted{HeadId
$sel:headId:PeerConnected :: HeadId
headId :: HeadId
headId, $sel:utxo:PeerConnected :: UTxOType tx
utxo = Committed tx -> UTxOType tx
forall m. Monoid m => Map Party m -> m
forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m
fold Committed tx
committed})

-- | Observe a collectCom transaction. We initialize the 'OpenState' using the
-- head parameters from 'IdleState' and construct an 'InitialSnapshot' holding
-- @u0@ from the committed UTxOs.
--
-- __Transition__: 'InitialState' → 'OpenState'
onInitialChainCollectTx ::
  IsChainState tx =>
  InitialState tx ->
  -- | New chain state
  ChainStateType tx ->
  Outcome tx
onInitialChainCollectTx :: forall tx.
IsChainState tx =>
InitialState tx -> ChainStateType tx -> Outcome tx
onInitialChainCollectTx InitialState tx
st ChainStateType tx
newChainState =
  -- Spec: 𝑈₀  ← ⋃ⁿⱼ₌₁ 𝑈ⱼ
  let u0 :: UTxOType tx
u0 = Map Party (UTxOType tx) -> UTxOType tx
forall m. Monoid m => Map Party m -> m
forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m
fold Map Party (UTxOType tx)
committed
   in -- Spec: L̂  ← 𝑈₀
      --       ̅S  ← snObj(0, 0, 𝑈₀, ∅, ⊥)
      --       v , ŝ ← 0
      --       T̂  ← ∅
      --       txω ← ⊥
      StateChanged tx -> Outcome tx
forall tx. StateChanged tx -> Outcome tx
newState HeadOpened{$sel:chainState:HeadInitialized :: ChainStateType tx
chainState = ChainStateType tx
newChainState, $sel:initialUTxO:HeadInitialized :: UTxOType tx
initialUTxO = UTxOType tx
u0}
        Outcome tx -> Outcome tx -> Outcome tx
forall a. Semigroup a => a -> a -> a
<> Effect tx -> Outcome tx
forall tx. Effect tx -> Outcome tx
cause (ServerOutput tx -> Effect tx
forall tx. ServerOutput tx -> Effect tx
ClientEffect (ServerOutput tx -> Effect tx) -> ServerOutput tx -> Effect tx
forall a b. (a -> b) -> a -> b
$ ServerOutput.HeadIsOpen{HeadId
$sel:headId:PeerConnected :: HeadId
headId :: HeadId
headId, $sel:utxo:PeerConnected :: UTxOType tx
utxo = UTxOType tx
u0})
 where
  -- 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?
  InitialState{Map Party (UTxOType tx)
$sel:committed:InitialState :: forall tx. InitialState tx -> Committed tx
committed :: Map Party (UTxOType tx)
committed, HeadId
$sel:headId:InitialState :: forall tx. InitialState tx -> HeadId
headId :: HeadId
headId} = InitialState tx
st

-- ** Off-chain protocol

-- | Client request to ingest a new transaction into the head.
--
-- __Transition__: 'OpenState' → 'OpenState'
onOpenClientNewTx ::
  -- | The transaction to be submitted to the head.
  tx ->
  Outcome tx
onOpenClientNewTx :: forall tx. tx -> Outcome tx
onOpenClientNewTx tx
tx =
  Effect tx -> Outcome tx
forall tx. Effect tx -> Outcome tx
cause (Effect tx -> Outcome tx)
-> (Message tx -> Effect tx) -> Message tx -> Outcome tx
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Message tx -> Effect tx
forall tx. Message tx -> Effect tx
NetworkEffect (Message tx -> Outcome tx) -> Message tx -> Outcome tx
forall a b. (a -> b) -> a -> b
$ tx -> Message tx
forall tx. tx -> Message tx
ReqTx tx
tx

-- | Process a transaction request ('ReqTx') from a party.
--
-- We apply this transaction to the seen utxo (ledger state). If not applicable,
-- we wait and retry later. If it applies, this yields an updated seen ledger
-- state. Then, we check whether we are the leader for the next snapshot and
-- emit a snapshot request 'ReqSn' including this transaction if needed.
--
-- __Transition__: 'OpenState' → 'OpenState'
onOpenNetworkReqTx ::
  IsTx tx =>
  Environment ->
  Ledger tx ->
  OpenState tx ->
  TTL ->
  -- | The transaction to be submitted to the head.
  tx ->
  Outcome tx
onOpenNetworkReqTx :: forall tx.
IsTx tx =>
Environment -> Ledger tx -> OpenState tx -> TTL -> tx -> Outcome tx
onOpenNetworkReqTx Environment
env Ledger tx
ledger OpenState tx
st TTL
ttl tx
tx =
  -- Keep track of transactions by-id
  (StateChanged tx -> Outcome tx
forall tx. StateChanged tx -> Outcome tx
newState TransactionReceived{tx
tx :: tx
$sel:tx:HeadInitialized :: tx
tx} <>) (Outcome tx -> Outcome tx) -> Outcome tx -> Outcome tx
forall a b. (a -> b) -> a -> b
$
    -- Spec: wait L̂ ◦ tx ≠ ⊥
    (UTxOType tx -> Outcome tx) -> Outcome tx
waitApplyTx ((UTxOType tx -> Outcome tx) -> Outcome tx)
-> (UTxOType tx -> Outcome tx) -> Outcome tx
forall a b. (a -> b) -> a -> b
$ \UTxOType tx
newLocalUTxO ->
      (Effect tx -> Outcome tx
forall tx. Effect tx -> Outcome tx
cause (ServerOutput tx -> Effect tx
forall tx. ServerOutput tx -> Effect tx
ClientEffect (ServerOutput tx -> Effect tx) -> ServerOutput tx -> Effect tx
forall a b. (a -> b) -> a -> b
$ HeadId -> TxIdType tx -> ServerOutput tx
forall tx. HeadId -> TxIdType tx -> ServerOutput tx
ServerOutput.TxValid HeadId
headId (tx -> TxIdType tx
forall tx. IsTx tx => tx -> TxIdType tx
txId tx
tx)) <>) (Outcome tx -> Outcome tx) -> Outcome tx -> Outcome tx
forall a b. (a -> b) -> a -> b
$
        -- Spec: T̂ ← T̂ ⋃ {tx}
        --       L̂  ← L̂ ◦ tx
        StateChanged tx -> Outcome tx
forall tx. StateChanged tx -> Outcome tx
newState TransactionAppliedToLocalUTxO{tx
tx :: tx
$sel:tx:HeadInitialized :: tx
tx, UTxOType tx
newLocalUTxO :: UTxOType tx
$sel:newLocalUTxO:HeadInitialized :: UTxOType tx
newLocalUTxO}
          -- Spec: if ŝ = ̅S.s ∧ leader(̅S.s + 1) = i
          --         multicast (reqSn, v, ̅S.s + 1, T̂ , txω )
          Outcome tx -> (Outcome tx -> Outcome tx) -> Outcome tx
forall a b. a -> (a -> b) -> b
& SnapshotNumber -> Outcome tx -> Outcome tx
maybeRequestSnapshot (SnapshotNumber
confirmedSn SnapshotNumber -> SnapshotNumber -> SnapshotNumber
forall a. Num a => a -> a -> a
+ SnapshotNumber
1)
 where
  waitApplyTx :: (UTxOType tx -> Outcome tx) -> Outcome tx
waitApplyTx UTxOType tx -> Outcome tx
cont =
    case ChainSlot
-> UTxOType tx
-> [tx]
-> Either (tx, ValidationError) (UTxOType tx)
applyTransactions ChainSlot
currentSlot UTxOType tx
localUTxO [tx
tx] of
      Right UTxOType tx
utxo' -> UTxOType tx -> Outcome tx
cont UTxOType tx
utxo'
      Left (tx
_, ValidationError
err)
        | TTL
ttl TTL -> TTL -> Bool
forall a. Ord a => a -> a -> Bool
> TTL
0 ->
            WaitReason tx -> Outcome tx
forall tx. WaitReason tx -> Outcome tx
wait (ValidationError -> WaitReason tx
forall tx. ValidationError -> WaitReason tx
WaitOnNotApplicableTx ValidationError
err)
        | Bool
otherwise ->
            -- XXX: We might want to remove invalid txs from allTxs here to
            -- prevent them piling up infinitely. However, this is not really
            -- covered by the spec and this could be problematic in case of
            -- conflicting transactions paired with network latency and/or
            -- message resubmission. For example: Assume tx2 depends on tx1, but
            -- only tx2 is seen by a participant and eventually times out
            -- because of network latency when receiving tx1. The leader,
            -- however, saw both as valid and requests a snapshot including
            -- both. This is a valid request and if we would have removed tx2
            -- from allTxs, we would make the head stuck.
            Effect tx -> Outcome tx
forall tx. Effect tx -> Outcome tx
cause (Effect tx -> Outcome tx)
-> (ServerOutput tx -> Effect tx) -> ServerOutput tx -> Outcome tx
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ServerOutput tx -> Effect tx
forall tx. ServerOutput tx -> Effect tx
ClientEffect (ServerOutput tx -> Outcome tx) -> ServerOutput tx -> Outcome tx
forall a b. (a -> b) -> a -> b
$ HeadId -> UTxOType tx -> tx -> ValidationError -> ServerOutput tx
forall tx.
HeadId -> UTxOType tx -> tx -> ValidationError -> ServerOutput tx
ServerOutput.TxInvalid HeadId
headId UTxOType tx
localUTxO tx
tx ValidationError
err

  maybeRequestSnapshot :: SnapshotNumber -> Outcome tx -> Outcome tx
maybeRequestSnapshot SnapshotNumber
nextSn Outcome tx
outcome =
    if Bool -> Bool
not Bool
snapshotInFlight Bool -> Bool -> Bool
&& HeadParameters -> Party -> SnapshotNumber -> Bool
isLeader HeadParameters
parameters Party
party SnapshotNumber
nextSn
      then
        Outcome tx
outcome
          -- XXX: This state update has no equivalence in the
          -- spec. Do we really need to store that we have
          -- requested a snapshot? If yes, should update spec.
          Outcome tx -> Outcome tx -> Outcome tx
forall a. Semigroup a => a -> a -> a
<> StateChanged tx -> Outcome tx
forall tx. StateChanged tx -> Outcome tx
newState SnapshotRequestDecided{$sel:snapshotNumber:HeadInitialized :: SnapshotNumber
snapshotNumber = SnapshotNumber
nextSn}
          Outcome tx -> Outcome tx -> Outcome tx
forall a. Semigroup a => a -> a -> a
<> Effect tx -> Outcome tx
forall tx. Effect tx -> Outcome tx
cause (Message tx -> Effect tx
forall tx. Message tx -> Effect tx
NetworkEffect (Message tx -> Effect tx) -> Message tx -> Effect tx
forall a b. (a -> b) -> a -> b
$ SnapshotVersion
-> SnapshotNumber
-> [TxIdType tx]
-> Maybe tx
-> Maybe (UTxOType tx)
-> Message tx
forall tx.
SnapshotVersion
-> SnapshotNumber
-> [TxIdType tx]
-> Maybe tx
-> Maybe (UTxOType tx)
-> Message tx
ReqSn SnapshotVersion
version SnapshotNumber
nextSn (tx -> TxIdType tx
forall tx. IsTx tx => tx -> TxIdType tx
txId (tx -> TxIdType tx) -> [tx] -> [TxIdType tx]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [tx]
localTxs') Maybe tx
decommitTx Maybe (UTxOType tx)
pendingDeposit)
      else Outcome tx
outcome

  Environment{Party
$sel:party:Environment :: Environment -> Party
party :: Party
party} = Environment
env

  Ledger{ChainSlot
-> UTxOType tx
-> [tx]
-> Either (tx, ValidationError) (UTxOType tx)
$sel:applyTransactions:Ledger :: forall tx.
Ledger tx
-> ChainSlot
-> UTxOType tx
-> [tx]
-> Either (tx, ValidationError) (UTxOType tx)
applyTransactions :: ChainSlot
-> UTxOType tx
-> [tx]
-> Either (tx, ValidationError) (UTxOType tx)
applyTransactions} = Ledger tx
ledger

  pendingDeposit :: Maybe (UTxOType tx)
pendingDeposit =
    case Map (TxIdType tx) (UTxOType tx) -> [(TxIdType tx, UTxOType tx)]
forall k a. Map k a -> [(k, a)]
Map.toList Map (TxIdType tx) (UTxOType tx)
pendingDeposits of
      [] -> Maybe (UTxOType tx)
forall a. Maybe a
Nothing
      (TxIdType tx
_, UTxOType tx
depositUTxO) : [(TxIdType tx, UTxOType tx)]
_ -> UTxOType tx -> Maybe (UTxOType tx)
forall a. a -> Maybe a
Just UTxOType tx
depositUTxO

  CoordinatedHeadState{[tx]
localTxs :: [tx]
$sel:localTxs:CoordinatedHeadState :: forall tx. CoordinatedHeadState tx -> [tx]
localTxs, UTxOType tx
localUTxO :: UTxOType tx
$sel:localUTxO:CoordinatedHeadState :: forall tx. CoordinatedHeadState tx -> UTxOType tx
localUTxO, ConfirmedSnapshot tx
confirmedSnapshot :: ConfirmedSnapshot tx
$sel:confirmedSnapshot:CoordinatedHeadState :: forall tx. CoordinatedHeadState tx -> ConfirmedSnapshot tx
confirmedSnapshot, SeenSnapshot tx
seenSnapshot :: SeenSnapshot tx
$sel:seenSnapshot:CoordinatedHeadState :: forall tx. CoordinatedHeadState tx -> SeenSnapshot tx
seenSnapshot, Maybe tx
decommitTx :: Maybe tx
$sel:decommitTx:CoordinatedHeadState :: forall tx. CoordinatedHeadState tx -> Maybe tx
decommitTx, SnapshotVersion
version :: SnapshotVersion
$sel:version:CoordinatedHeadState :: forall tx. CoordinatedHeadState tx -> SnapshotVersion
version, Map (TxIdType tx) (UTxOType tx)
pendingDeposits :: Map (TxIdType tx) (UTxOType tx)
$sel:pendingDeposits:CoordinatedHeadState :: forall tx.
CoordinatedHeadState tx -> Map (TxIdType tx) (UTxOType tx)
pendingDeposits} = CoordinatedHeadState tx
coordinatedHeadState

  Snapshot{$sel:number:Snapshot :: forall tx. Snapshot tx -> SnapshotNumber
number = SnapshotNumber
confirmedSn} = ConfirmedSnapshot tx -> Snapshot tx
forall tx. ConfirmedSnapshot tx -> Snapshot tx
getSnapshot ConfirmedSnapshot tx
confirmedSnapshot

  OpenState{CoordinatedHeadState tx
coordinatedHeadState :: CoordinatedHeadState tx
$sel:coordinatedHeadState:OpenState :: forall tx. OpenState tx -> CoordinatedHeadState tx
coordinatedHeadState, HeadId
headId :: HeadId
$sel:headId:OpenState :: forall tx. OpenState tx -> HeadId
headId, ChainSlot
currentSlot :: ChainSlot
$sel:currentSlot:OpenState :: forall tx. OpenState tx -> ChainSlot
currentSlot, HeadParameters
parameters :: HeadParameters
$sel:parameters:OpenState :: forall tx. OpenState tx -> HeadParameters
parameters} = OpenState tx
st

  snapshotInFlight :: Bool
snapshotInFlight = case SeenSnapshot tx
seenSnapshot of
    SeenSnapshot tx
NoSeenSnapshot -> Bool
False
    LastSeenSnapshot{} -> Bool
False
    RequestedSnapshot{} -> Bool
True
    SeenSnapshot{} -> Bool
True

  -- NOTE: Order of transactions is important here. See also
  -- 'pruneTransactions'.
  localTxs' :: [tx]
localTxs' = [tx]
localTxs [tx] -> [tx] -> [tx]
forall a. Semigroup a => a -> a -> a
<> [tx
tx]

-- | Process a snapshot request ('ReqSn') from party.
--
-- This checks that s is the next snapshot number and that the party is
-- responsible for leading that snapshot. Then, we potentially wait until the
-- previous snapshot is confirmed (no snapshot is in flight), before we apply
-- (or wait until applicable) the requested transactions to the last confirmed
-- snapshot. Only then, we start tracking this new "seen" snapshot, compute a
-- signature of it and send the corresponding 'AckSn' to all parties. Finally,
-- the pending transaction set gets pruned to only contain still applicable
-- transactions.
--
-- __Transition__: 'OpenState' → 'OpenState'
onOpenNetworkReqSn ::
  IsTx tx =>
  Environment ->
  Ledger tx ->
  OpenState tx ->
  -- | Party which sent the ReqSn.
  Party ->
  -- | Requested snapshot version.
  SnapshotVersion ->
  -- | Requested snapshot number.
  SnapshotNumber ->
  -- | List of transactions to snapshot.
  [TxIdType tx] ->
  -- | Optional decommit transaction of removing funds from the head.
  Maybe tx ->
  Maybe (UTxOType tx) ->
  Outcome tx
onOpenNetworkReqSn :: forall tx.
IsTx tx =>
Environment
-> Ledger tx
-> OpenState tx
-> Party
-> SnapshotVersion
-> SnapshotNumber
-> [TxIdType tx]
-> Maybe tx
-> Maybe (UTxOType tx)
-> Outcome tx
onOpenNetworkReqSn Environment
env Ledger tx
ledger OpenState tx
st Party
otherParty SnapshotVersion
sv SnapshotNumber
sn [TxIdType tx]
requestedTxIds Maybe tx
mDecommitTx Maybe (UTxOType tx)
mIncrementUTxO =
  -- Spec: require s = ŝ + 1 ∧ leader(s) = j
  Outcome tx -> Outcome tx
requireReqSn (Outcome tx -> Outcome tx) -> Outcome tx -> Outcome tx
forall a b. (a -> b) -> a -> b
$
    -- Spec: wait ŝ = ̅S.s
    Outcome tx -> Outcome tx
waitNoSnapshotInFlight (Outcome tx -> Outcome tx) -> Outcome tx -> Outcome tx
forall a b. (a -> b) -> a -> b
$
      -- Spec: wait v = v̂
      Outcome tx -> Outcome tx
waitOnSnapshotVersion (Outcome tx -> Outcome tx) -> Outcome tx -> Outcome tx
forall a b. (a -> b) -> a -> b
$
        ((UTxOType tx, Maybe (UTxOType tx)) -> Outcome tx) -> Outcome tx
requireApplicableDecommitTx (((UTxOType tx, Maybe (UTxOType tx)) -> Outcome tx) -> Outcome tx)
-> ((UTxOType tx, Maybe (UTxOType tx)) -> Outcome tx) -> Outcome tx
forall a b. (a -> b) -> a -> b
$ \(UTxOType tx
activeUTxOAfterDecommit, Maybe (UTxOType tx)
mUtxoToDecommit) ->
          UTxOType tx
-> ((UTxOType tx, Maybe (UTxOType tx)) -> Outcome tx) -> Outcome tx
requireApplicableCommit UTxOType tx
activeUTxOAfterDecommit (((UTxOType tx, Maybe (UTxOType tx)) -> Outcome tx) -> Outcome tx)
-> ((UTxOType tx, Maybe (UTxOType tx)) -> Outcome tx) -> Outcome tx
forall a b. (a -> b) -> a -> b
$ \(UTxOType tx
activeUTxO, Maybe (UTxOType tx)
mUtxoToCommit) ->
            -- Resolve transactions by-id
            ([tx] -> Outcome tx) -> Outcome tx
waitResolvableTxs (([tx] -> Outcome tx) -> Outcome tx)
-> ([tx] -> Outcome tx) -> Outcome tx
forall a b. (a -> b) -> a -> b
$ \[tx]
requestedTxs -> do
              -- Spec: require 𝑈_active ◦ Treq ≠ ⊥
              --       𝑈 ← 𝑈_active ◦ Treq
              UTxOType tx -> [tx] -> (UTxOType tx -> Outcome tx) -> Outcome tx
requireApplyTxs UTxOType tx
activeUTxO [tx]
requestedTxs ((UTxOType tx -> Outcome tx) -> Outcome tx)
-> (UTxOType tx -> Outcome tx) -> Outcome tx
forall a b. (a -> b) -> a -> b
$ \UTxOType tx
u -> do
                -- Spec: ŝ ← ̅S.s + 1
                -- NOTE: confSn == seenSn == sn here
                let nextSnapshot :: Snapshot tx
nextSnapshot =
                      Snapshot
                        { HeadId
headId :: HeadId
$sel:headId:Snapshot :: HeadId
headId
                        , $sel:version:Snapshot :: SnapshotVersion
version = SnapshotVersion
version
                        , $sel:number:Snapshot :: SnapshotNumber
number = SnapshotNumber
sn
                        , $sel:confirmed:Snapshot :: [tx]
confirmed = [tx]
requestedTxs
                        , $sel:utxo:Snapshot :: UTxOType tx
utxo = UTxOType tx
u
                        , $sel:utxoToCommit:Snapshot :: Maybe (UTxOType tx)
utxoToCommit = Maybe (UTxOType tx)
mUtxoToCommit
                        , $sel:utxoToDecommit:Snapshot :: Maybe (UTxOType tx)
utxoToDecommit = Maybe (UTxOType tx)
mUtxoToDecommit
                        }
                -- Spec: η ← combine(𝑈)
                --       σᵢ ← MS-Sign(kₕˢⁱᵍ, (cid‖v‖ŝ‖η‖ηω))
                let snapshotSignature :: Signature (Snapshot tx)
snapshotSignature = SigningKey HydraKey -> Snapshot tx -> Signature (Snapshot tx)
forall a.
SignableRepresentation a =>
SigningKey HydraKey -> a -> Signature a
sign SigningKey HydraKey
signingKey Snapshot tx
nextSnapshot
                -- Spec: multicast (ackSn, ŝ, σᵢ)
                (Effect tx -> Outcome tx
forall tx. Effect tx -> Outcome tx
cause (Message tx -> Effect tx
forall tx. Message tx -> Effect tx
NetworkEffect (Message tx -> Effect tx) -> Message tx -> Effect tx
forall a b. (a -> b) -> a -> b
$ Signature (Snapshot tx) -> SnapshotNumber -> Message tx
forall tx. Signature (Snapshot tx) -> SnapshotNumber -> Message tx
AckSn Signature (Snapshot tx)
snapshotSignature SnapshotNumber
sn) <>) (Outcome tx -> Outcome tx) -> Outcome tx -> Outcome tx
forall a b. (a -> b) -> a -> b
$ do
                  -- Spec: ̂Σ ← ∅
                  --       L̂ ← 𝑈
                  --       𝑋 ← T
                  --       T̂ ← ∅
                  --       for tx ∈ 𝑋 : L̂ ◦ tx ≠ ⊥
                  --         T̂ ← T̂ ⋃ {tx}
                  --         L̂ ← L̂ ◦ tx
                  let ([tx]
newLocalTxs, UTxOType tx
newLocalUTxO) = UTxOType tx -> ([tx], UTxOType tx)
pruneTransactions UTxOType tx
u
                  StateChanged tx -> Outcome tx
forall tx. StateChanged tx -> Outcome tx
newState
                    SnapshotRequested
                      { $sel:snapshot:HeadInitialized :: Snapshot tx
snapshot = Snapshot tx
nextSnapshot
                      , [TxIdType tx]
requestedTxIds :: [TxIdType tx]
$sel:requestedTxIds:HeadInitialized :: [TxIdType tx]
requestedTxIds
                      , UTxOType tx
$sel:newLocalUTxO:HeadInitialized :: UTxOType tx
newLocalUTxO :: UTxOType tx
newLocalUTxO
                      , [tx]
newLocalTxs :: [tx]
$sel:newLocalTxs:HeadInitialized :: [tx]
newLocalTxs
                      }
 where
  requireReqSn :: Outcome tx -> Outcome tx
requireReqSn Outcome tx
continue
    | SnapshotVersion
sv SnapshotVersion -> SnapshotVersion -> Bool
forall a. Eq a => a -> a -> Bool
/= SnapshotVersion
version =
        LogicError tx -> Outcome tx
forall tx. LogicError tx -> Outcome tx
Error (LogicError tx -> Outcome tx) -> LogicError tx -> Outcome tx
forall a b. (a -> b) -> a -> b
$ RequirementFailure tx -> LogicError tx
forall tx. RequirementFailure tx -> LogicError tx
RequireFailed (RequirementFailure tx -> LogicError tx)
-> RequirementFailure tx -> LogicError tx
forall a b. (a -> b) -> a -> b
$ ReqSvNumberInvalid{$sel:requestedSv:ReqSnNumberInvalid :: SnapshotVersion
requestedSv = SnapshotVersion
sv, $sel:lastSeenSv:ReqSnNumberInvalid :: SnapshotVersion
lastSeenSv = SnapshotVersion
version}
    | SnapshotNumber
sn SnapshotNumber -> SnapshotNumber -> Bool
forall a. Eq a => a -> a -> Bool
/= SnapshotNumber
seenSn SnapshotNumber -> SnapshotNumber -> SnapshotNumber
forall a. Num a => a -> a -> a
+ SnapshotNumber
1 =
        LogicError tx -> Outcome tx
forall tx. LogicError tx -> Outcome tx
Error (LogicError tx -> Outcome tx) -> LogicError tx -> Outcome tx
forall a b. (a -> b) -> a -> b
$ RequirementFailure tx -> LogicError tx
forall tx. RequirementFailure tx -> LogicError tx
RequireFailed (RequirementFailure tx -> LogicError tx)
-> RequirementFailure tx -> LogicError tx
forall a b. (a -> b) -> a -> b
$ ReqSnNumberInvalid{$sel:requestedSn:ReqSnNumberInvalid :: SnapshotNumber
requestedSn = SnapshotNumber
sn, $sel:lastSeenSn:ReqSnNumberInvalid :: SnapshotNumber
lastSeenSn = SnapshotNumber
seenSn}
    | Bool -> Bool
not (HeadParameters -> Party -> SnapshotNumber -> Bool
isLeader HeadParameters
parameters Party
otherParty SnapshotNumber
sn) =
        LogicError tx -> Outcome tx
forall tx. LogicError tx -> Outcome tx
Error (LogicError tx -> Outcome tx) -> LogicError tx -> Outcome tx
forall a b. (a -> b) -> a -> b
$ RequirementFailure tx -> LogicError tx
forall tx. RequirementFailure tx -> LogicError tx
RequireFailed (RequirementFailure tx -> LogicError tx)
-> RequirementFailure tx -> LogicError tx
forall a b. (a -> b) -> a -> b
$ ReqSnNotLeader{$sel:requestedSn:ReqSnNumberInvalid :: SnapshotNumber
requestedSn = SnapshotNumber
sn, $sel:leader:ReqSnNumberInvalid :: Party
leader = Party
otherParty}
    | Bool
otherwise =
        Outcome tx
continue

  waitNoSnapshotInFlight :: Outcome tx -> Outcome tx
waitNoSnapshotInFlight Outcome tx
continue
    | SnapshotNumber
confSn SnapshotNumber -> SnapshotNumber -> Bool
forall a. Eq a => a -> a -> Bool
== SnapshotNumber
seenSn =
        Outcome tx
continue
    | Bool
otherwise =
        WaitReason tx -> Outcome tx
forall tx. WaitReason tx -> Outcome tx
wait (WaitReason tx -> Outcome tx) -> WaitReason tx -> Outcome tx
forall a b. (a -> b) -> a -> b
$ SnapshotNumber -> WaitReason tx
forall tx. SnapshotNumber -> WaitReason tx
WaitOnSnapshotNumber SnapshotNumber
seenSn

  waitOnSnapshotVersion :: Outcome tx -> Outcome tx
waitOnSnapshotVersion Outcome tx
continue
    | SnapshotVersion
version SnapshotVersion -> SnapshotVersion -> Bool
forall a. Eq a => a -> a -> Bool
== SnapshotVersion
sv =
        Outcome tx
continue
    | Bool
otherwise =
        WaitReason tx -> Outcome tx
forall tx. WaitReason tx -> Outcome tx
wait (WaitReason tx -> Outcome tx) -> WaitReason tx -> Outcome tx
forall a b. (a -> b) -> a -> b
$ SnapshotVersion -> WaitReason tx
forall tx. SnapshotVersion -> WaitReason tx
WaitOnSnapshotVersion SnapshotVersion
sv

  waitResolvableTxs :: ([tx] -> Outcome tx) -> Outcome tx
waitResolvableTxs [tx] -> Outcome tx
continue =
    case Set (TxIdType tx) -> [TxIdType tx]
forall a. Set a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList ([Item (Set (TxIdType tx))] -> Set (TxIdType tx)
forall l. IsList l => [Item l] -> l
fromList [Item (Set (TxIdType tx))]
[TxIdType tx]
requestedTxIds Set (TxIdType tx) -> Set (TxIdType tx) -> Set (TxIdType tx)
forall a. Ord a => Set a -> Set a -> Set a
\\ Map (TxIdType tx) tx -> Set (TxIdType tx)
forall k a. Map k a -> Set k
Map.keysSet Map (TxIdType tx) tx
allTxs) of
      [] -> [tx] -> Outcome tx
continue ([tx] -> Outcome tx) -> [tx] -> Outcome tx
forall a b. (a -> b) -> a -> b
$ (TxIdType tx -> Maybe tx) -> [TxIdType tx] -> [tx]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (TxIdType tx -> Map (TxIdType tx) tx -> Maybe tx
forall k a. Ord k => k -> Map k a -> Maybe a
`Map.lookup` Map (TxIdType tx) tx
allTxs) [TxIdType tx]
requestedTxIds
      [TxIdType tx]
unseen -> WaitReason tx -> Outcome tx
forall tx. WaitReason tx -> Outcome tx
wait (WaitReason tx -> Outcome tx) -> WaitReason tx -> Outcome tx
forall a b. (a -> b) -> a -> b
$ [TxIdType tx] -> WaitReason tx
forall tx. [TxIdType tx] -> WaitReason tx
WaitOnTxs [TxIdType tx]
unseen

  requireApplicableCommit :: UTxOType tx
-> ((UTxOType tx, Maybe (UTxOType tx)) -> Outcome tx) -> Outcome tx
requireApplicableCommit UTxOType tx
activeUTxOAfterDecommit (UTxOType tx, Maybe (UTxOType tx)) -> Outcome tx
cont =
    case Maybe (UTxOType tx)
mIncrementUTxO of
      Maybe (UTxOType tx)
Nothing -> (UTxOType tx, Maybe (UTxOType tx)) -> Outcome tx
cont (UTxOType tx
activeUTxOAfterDecommit, Maybe (UTxOType tx)
forall a. Maybe a
Nothing)
      Just UTxOType tx
utxo ->
        if SnapshotVersion
sv SnapshotVersion -> SnapshotVersion -> Bool
forall a. Eq a => a -> a -> Bool
== SnapshotVersion
confVersion Bool -> Bool -> Bool
&& Maybe (UTxOType tx) -> Bool
forall a. Maybe a -> Bool
isJust Maybe (UTxOType tx)
confUTxOToCommit
          then
            if Maybe (UTxOType tx)
confUTxOToCommit Maybe (UTxOType tx) -> Maybe (UTxOType tx) -> Bool
forall a. Eq a => a -> a -> Bool
== UTxOType tx -> Maybe (UTxOType tx)
forall a. a -> Maybe a
Just UTxOType tx
utxo
              then (UTxOType tx, Maybe (UTxOType tx)) -> Outcome tx
cont (UTxOType tx
activeUTxOAfterDecommit UTxOType tx -> UTxOType tx -> UTxOType tx
forall a. Semigroup a => a -> a -> a
<> UTxOType tx -> Maybe (UTxOType tx) -> UTxOType tx
forall a. a -> Maybe a -> a
fromMaybe UTxOType tx
forall a. Monoid a => a
mempty Maybe (UTxOType tx)
confUTxOToCommit, Maybe (UTxOType tx)
confUTxOToCommit)
              else LogicError tx -> Outcome tx
forall tx. LogicError tx -> Outcome tx
Error (LogicError tx -> Outcome tx) -> LogicError tx -> Outcome tx
forall a b. (a -> b) -> a -> b
$ RequirementFailure tx -> LogicError tx
forall tx. RequirementFailure tx -> LogicError tx
RequireFailed RequirementFailure tx
forall tx. RequirementFailure tx
ReqSnCommitNotSettled
          else do
            let activeUTxOAfterCommit :: UTxOType tx
activeUTxOAfterCommit = UTxOType tx
activeUTxOAfterDecommit UTxOType tx -> UTxOType tx -> UTxOType tx
forall a. Semigroup a => a -> a -> a
<> UTxOType tx
utxo
            (UTxOType tx, Maybe (UTxOType tx)) -> Outcome tx
cont (UTxOType tx
activeUTxOAfterCommit, UTxOType tx -> Maybe (UTxOType tx)
forall a. a -> Maybe a
Just UTxOType tx
utxo)

  requireApplicableDecommitTx :: ((UTxOType tx, Maybe (UTxOType tx)) -> Outcome tx) -> Outcome tx
requireApplicableDecommitTx (UTxOType tx, Maybe (UTxOType tx)) -> Outcome tx
cont =
    case Maybe tx
mDecommitTx of
      Maybe tx
Nothing -> (UTxOType tx, Maybe (UTxOType tx)) -> Outcome tx
cont (UTxOType tx
confirmedUTxO, Maybe (UTxOType tx)
forall a. Maybe a
Nothing)
      Just tx
decommitTx ->
        -- Spec:
        -- if v = S̄.v ∧ S̄.txω ̸= ⊥
        --   require S̄.txω = txω
        --   Uactive ← S̄.U
        --   Uω ← S̄.Uω
        -- else
        --   require S̄.U ◦ txω ̸= ⊥
        --   Uactive ← S̄.U ◦ txω \ outputs(txω )
        --   Uω ← outputs(txω )
        if SnapshotVersion
sv SnapshotVersion -> SnapshotVersion -> Bool
forall a. Eq a => a -> a -> Bool
== SnapshotVersion
confVersion Bool -> Bool -> Bool
&& Maybe (UTxOType tx) -> Bool
forall a. Maybe a -> Bool
isJust Maybe (UTxOType tx)
confUTxOToDecommit
          then
            if Maybe (UTxOType tx)
confUTxOToDecommit Maybe (UTxOType tx) -> Maybe (UTxOType tx) -> Bool
forall a. Eq a => a -> a -> Bool
== UTxOType tx -> Maybe (UTxOType tx)
forall a. a -> Maybe a
Just (tx -> UTxOType tx
forall tx. IsTx tx => tx -> UTxOType tx
utxoFromTx tx
decommitTx)
              then (UTxOType tx, Maybe (UTxOType tx)) -> Outcome tx
cont (UTxOType tx
confirmedUTxO, Maybe (UTxOType tx)
confUTxOToDecommit)
              else LogicError tx -> Outcome tx
forall tx. LogicError tx -> Outcome tx
Error (LogicError tx -> Outcome tx) -> LogicError tx -> Outcome tx
forall a b. (a -> b) -> a -> b
$ RequirementFailure tx -> LogicError tx
forall tx. RequirementFailure tx -> LogicError tx
RequireFailed RequirementFailure tx
forall tx. RequirementFailure tx
ReqSnDecommitNotSettled
          else case Ledger tx
-> ChainSlot
-> UTxOType tx
-> [tx]
-> Either (tx, ValidationError) (UTxOType tx)
forall tx.
Ledger tx
-> ChainSlot
-> UTxOType tx
-> [tx]
-> Either (tx, ValidationError) (UTxOType tx)
applyTransactions Ledger tx
ledger ChainSlot
currentSlot UTxOType tx
confirmedUTxO [tx
decommitTx] of
            Left (tx
_, ValidationError
err) ->
              LogicError tx -> Outcome tx
forall tx. LogicError tx -> Outcome tx
Error (LogicError tx -> Outcome tx) -> LogicError tx -> Outcome tx
forall a b. (a -> b) -> a -> b
$ RequirementFailure tx -> LogicError tx
forall tx. RequirementFailure tx -> LogicError tx
RequireFailed (RequirementFailure tx -> LogicError tx)
-> RequirementFailure tx -> LogicError tx
forall a b. (a -> b) -> a -> b
$ SnapshotNumber
-> TxIdType tx -> ValidationError -> RequirementFailure tx
forall tx.
SnapshotNumber
-> TxIdType tx -> ValidationError -> RequirementFailure tx
SnapshotDoesNotApply SnapshotNumber
sn (tx -> TxIdType tx
forall tx. IsTx tx => tx -> TxIdType tx
txId tx
decommitTx) ValidationError
err
            Right UTxOType tx
newConfirmedUTxO -> do
              let utxoToDecommit :: UTxOType tx
utxoToDecommit = tx -> UTxOType tx
forall tx. IsTx tx => tx -> UTxOType tx
utxoFromTx tx
decommitTx
              let activeUTxO :: UTxOType tx
activeUTxO = UTxOType tx
newConfirmedUTxO UTxOType tx -> UTxOType tx -> UTxOType tx
forall tx. IsTx tx => UTxOType tx -> UTxOType tx -> UTxOType tx
`withoutUTxO` UTxOType tx
utxoToDecommit
              (UTxOType tx, Maybe (UTxOType tx)) -> Outcome tx
cont (UTxOType tx
activeUTxO, UTxOType tx -> Maybe (UTxOType tx)
forall a. a -> Maybe a
Just UTxOType tx
utxoToDecommit)

  -- NOTE: at this point we know those transactions apply on the localUTxO because they
  -- are part of the localTxs. The snapshot can contain less transactions than the ones
  -- we have seen at this stage, but they all _must_ apply correctly to the latest
  -- snapshot's UTxO set, eg. it's illegal for a snapshot leader to request a snapshot
  -- containing transactions that do not apply cleanly.
  requireApplyTxs :: UTxOType tx -> [tx] -> (UTxOType tx -> Outcome tx) -> Outcome tx
requireApplyTxs UTxOType tx
utxo [tx]
requestedTxs UTxOType tx -> Outcome tx
cont =
    case Ledger tx
-> ChainSlot
-> UTxOType tx
-> [tx]
-> Either (tx, ValidationError) (UTxOType tx)
forall tx.
Ledger tx
-> ChainSlot
-> UTxOType tx
-> [tx]
-> Either (tx, ValidationError) (UTxOType tx)
applyTransactions Ledger tx
ledger ChainSlot
currentSlot UTxOType tx
utxo [tx]
requestedTxs of
      Left (tx
tx, ValidationError
err) ->
        LogicError tx -> Outcome tx
forall tx. LogicError tx -> Outcome tx
Error (LogicError tx -> Outcome tx) -> LogicError tx -> Outcome tx
forall a b. (a -> b) -> a -> b
$ RequirementFailure tx -> LogicError tx
forall tx. RequirementFailure tx -> LogicError tx
RequireFailed (RequirementFailure tx -> LogicError tx)
-> RequirementFailure tx -> LogicError tx
forall a b. (a -> b) -> a -> b
$ SnapshotNumber
-> TxIdType tx -> ValidationError -> RequirementFailure tx
forall tx.
SnapshotNumber
-> TxIdType tx -> ValidationError -> RequirementFailure tx
SnapshotDoesNotApply SnapshotNumber
sn (tx -> TxIdType tx
forall tx. IsTx tx => tx -> TxIdType tx
txId tx
tx) ValidationError
err
      Right UTxOType tx
u -> UTxOType tx -> Outcome tx
cont UTxOType tx
u

  pruneTransactions :: UTxOType tx -> ([tx], UTxOType tx)
pruneTransactions UTxOType tx
utxo = do
    -- NOTE: Using foldl' is important to apply transacations in the correct
    -- order. That is, left-associative as new transactions are first validated
    -- and then appended to `localTxs` (when aggregating
    -- 'TransactionAppliedToLocalUTxO').
    (([tx], UTxOType tx) -> tx -> ([tx], UTxOType tx))
-> ([tx], UTxOType tx) -> [tx] -> ([tx], UTxOType tx)
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' ([tx], UTxOType tx) -> tx -> ([tx], UTxOType tx)
go ([], UTxOType tx
utxo) [tx]
localTxs
   where
    go :: ([tx], UTxOType tx) -> tx -> ([tx], UTxOType tx)
go ([tx]
txs, UTxOType tx
u) tx
tx =
      -- XXX: We prune transactions on any error, while only some of them are
      -- actually expected.
      -- For example: `OutsideValidityIntervalUTxO` ledger errors are expected
      -- here when a tx becomes invalid.
      case Ledger tx
-> ChainSlot
-> UTxOType tx
-> [tx]
-> Either (tx, ValidationError) (UTxOType tx)
forall tx.
Ledger tx
-> ChainSlot
-> UTxOType tx
-> [tx]
-> Either (tx, ValidationError) (UTxOType tx)
applyTransactions Ledger tx
ledger ChainSlot
currentSlot UTxOType tx
u [tx
tx] of
        Left (tx
_, ValidationError
_) -> ([tx]
txs, UTxOType tx
u)
        Right UTxOType tx
u' -> ([tx]
txs [tx] -> [tx] -> [tx]
forall a. Semigroup a => a -> a -> a
<> [tx
tx], UTxOType tx
u')

  confSn :: SnapshotNumber
confSn = case ConfirmedSnapshot tx
confirmedSnapshot of
    InitialSnapshot{} -> SnapshotNumber
0
    ConfirmedSnapshot{$sel:snapshot:InitialSnapshot :: forall tx. ConfirmedSnapshot tx -> Snapshot tx
snapshot = Snapshot{SnapshotNumber
$sel:number:Snapshot :: forall tx. Snapshot tx -> SnapshotNumber
number :: SnapshotNumber
number}} -> SnapshotNumber
number

  Snapshot{$sel:version:Snapshot :: forall tx. Snapshot tx -> SnapshotVersion
version = SnapshotVersion
confVersion} = ConfirmedSnapshot tx -> Snapshot tx
forall tx. ConfirmedSnapshot tx -> Snapshot tx
getSnapshot ConfirmedSnapshot tx
confirmedSnapshot

  confUTxOToCommit :: Maybe (UTxOType tx)
confUTxOToCommit = case ConfirmedSnapshot tx
confirmedSnapshot of
    InitialSnapshot{} -> Maybe (UTxOType tx)
forall a. Maybe a
Nothing
    ConfirmedSnapshot{$sel:snapshot:InitialSnapshot :: forall tx. ConfirmedSnapshot tx -> Snapshot tx
snapshot = Snapshot{Maybe (UTxOType tx)
$sel:utxoToCommit:Snapshot :: forall tx. Snapshot tx -> Maybe (UTxOType tx)
utxoToCommit :: Maybe (UTxOType tx)
utxoToCommit}} -> Maybe (UTxOType tx)
utxoToCommit

  confUTxOToDecommit :: Maybe (UTxOType tx)
confUTxOToDecommit = case ConfirmedSnapshot tx
confirmedSnapshot of
    InitialSnapshot{} -> Maybe (UTxOType tx)
forall a. Maybe a
Nothing
    ConfirmedSnapshot{$sel:snapshot:InitialSnapshot :: forall tx. ConfirmedSnapshot tx -> Snapshot tx
snapshot = Snapshot{Maybe (UTxOType tx)
$sel:utxoToDecommit:Snapshot :: forall tx. Snapshot tx -> Maybe (UTxOType tx)
utxoToDecommit :: Maybe (UTxOType tx)
utxoToDecommit}} -> Maybe (UTxOType tx)
utxoToDecommit

  seenSn :: SnapshotNumber
seenSn = SeenSnapshot tx -> SnapshotNumber
forall tx. SeenSnapshot tx -> SnapshotNumber
seenSnapshotNumber SeenSnapshot tx
seenSnapshot

  confirmedUTxO :: UTxOType tx
confirmedUTxO = case ConfirmedSnapshot tx
confirmedSnapshot of
    InitialSnapshot{UTxOType tx
initialUTxO :: UTxOType tx
$sel:initialUTxO:InitialSnapshot :: forall tx. ConfirmedSnapshot tx -> UTxOType tx
initialUTxO} -> UTxOType tx
initialUTxO
    ConfirmedSnapshot{$sel:snapshot:InitialSnapshot :: forall tx. ConfirmedSnapshot tx -> Snapshot tx
snapshot = Snapshot{UTxOType tx
$sel:utxo:Snapshot :: forall tx. Snapshot tx -> UTxOType tx
utxo :: UTxOType tx
utxo}} -> UTxOType tx
utxo

  CoordinatedHeadState{ConfirmedSnapshot tx
$sel:confirmedSnapshot:CoordinatedHeadState :: forall tx. CoordinatedHeadState tx -> ConfirmedSnapshot tx
confirmedSnapshot :: ConfirmedSnapshot tx
confirmedSnapshot, SeenSnapshot tx
$sel:seenSnapshot:CoordinatedHeadState :: forall tx. CoordinatedHeadState tx -> SeenSnapshot tx
seenSnapshot :: SeenSnapshot tx
seenSnapshot, Map (TxIdType tx) tx
allTxs :: Map (TxIdType tx) tx
$sel:allTxs:CoordinatedHeadState :: forall tx. CoordinatedHeadState tx -> Map (TxIdType tx) tx
allTxs, [tx]
$sel:localTxs:CoordinatedHeadState :: forall tx. CoordinatedHeadState tx -> [tx]
localTxs :: [tx]
localTxs, SnapshotVersion
$sel:version:CoordinatedHeadState :: forall tx. CoordinatedHeadState tx -> SnapshotVersion
version :: SnapshotVersion
version} = CoordinatedHeadState tx
coordinatedHeadState

  OpenState{HeadParameters
$sel:parameters:OpenState :: forall tx. OpenState tx -> HeadParameters
parameters :: HeadParameters
parameters, CoordinatedHeadState tx
$sel:coordinatedHeadState:OpenState :: forall tx. OpenState tx -> CoordinatedHeadState tx
coordinatedHeadState :: CoordinatedHeadState tx
coordinatedHeadState, ChainSlot
$sel:currentSlot:OpenState :: forall tx. OpenState tx -> ChainSlot
currentSlot :: ChainSlot
currentSlot, HeadId
$sel:headId:OpenState :: forall tx. OpenState tx -> HeadId
headId :: HeadId
headId} = OpenState tx
st

  Environment{SigningKey HydraKey
signingKey :: SigningKey HydraKey
$sel:signingKey:Environment :: Environment -> SigningKey HydraKey
signingKey} = Environment
env

-- | Process a snapshot acknowledgement ('AckSn') from a party.
--
-- We do require that the is from the last seen or next expected snapshot, and
-- potentially wait wait for the corresponding 'ReqSn' before proceeding. If the
-- party hasn't sent us a signature yet, we store it. Once a signature from each
-- party has been collected, we aggregate a multi-signature and verify it is
-- correct. If everything is fine, the snapshot can be considered as the latest
-- confirmed one. Similar to processing a 'ReqTx', we check whether we are
-- leading the next snapshot and craft a corresponding 'ReqSn' if needed.
--
-- __Transition__: 'OpenState' → 'OpenState'
onOpenNetworkAckSn ::
  IsTx tx =>
  Environment ->
  OpenState tx ->
  -- | Party which sent the AckSn.
  Party ->
  -- | Signature from other party.
  Signature (Snapshot tx) ->
  -- | Snapshot number of this AckSn.
  SnapshotNumber ->
  Outcome tx
onOpenNetworkAckSn :: forall tx.
IsTx tx =>
Environment
-> OpenState tx
-> Party
-> Signature (Snapshot tx)
-> SnapshotNumber
-> Outcome tx
onOpenNetworkAckSn Environment{Party
$sel:party:Environment :: Environment -> Party
party :: Party
party} OpenState tx
openState Party
otherParty Signature (Snapshot tx)
snapshotSignature SnapshotNumber
sn =
  -- Spec: require s ∈ {ŝ, ŝ + 1}
  Outcome tx -> Outcome tx
requireValidAckSn (Outcome tx -> Outcome tx) -> Outcome tx -> Outcome tx
forall a b. (a -> b) -> a -> b
$ do
    -- Spec: wait ŝ = s
    (Snapshot tx -> Map Party (Signature (Snapshot tx)) -> Outcome tx)
-> Outcome tx
waitOnSeenSnapshot ((Snapshot tx -> Map Party (Signature (Snapshot tx)) -> Outcome tx)
 -> Outcome tx)
-> (Snapshot tx
    -> Map Party (Signature (Snapshot tx)) -> Outcome tx)
-> Outcome tx
forall a b. (a -> b) -> a -> b
$ \Snapshot tx
snapshot Map Party (Signature (Snapshot tx))
sigs -> do
      -- Spec: require (j,⋅) ∉ ̂Σ
      Map Party (Signature (Snapshot tx)) -> Outcome tx -> Outcome tx
requireNotSignedYet Map Party (Signature (Snapshot tx))
sigs (Outcome tx -> Outcome tx) -> Outcome tx -> Outcome tx
forall a b. (a -> b) -> a -> b
$ do
        -- Spec: ̂Σ[j] ← σⱼ
        (StateChanged tx -> Outcome tx
forall tx. StateChanged tx -> Outcome tx
newState PartySignedSnapshot{Snapshot tx
$sel:snapshot:HeadInitialized :: Snapshot tx
snapshot :: Snapshot tx
snapshot, $sel:party:HeadInitialized :: Party
party = Party
otherParty, $sel:signature:HeadInitialized :: Signature (Snapshot tx)
signature = Signature (Snapshot tx)
snapshotSignature} <>) (Outcome tx -> Outcome tx) -> Outcome tx -> Outcome tx
forall a b. (a -> b) -> a -> b
$
          --       if ∀k ∈ [1..n] : (k,·) ∈ ̂Σ
          Snapshot tx
-> Map Party (Signature (Snapshot tx))
-> (Map Party (Signature (Snapshot tx)) -> Outcome tx)
-> Outcome tx
ifAllMembersHaveSigned Snapshot tx
snapshot Map Party (Signature (Snapshot tx))
sigs ((Map Party (Signature (Snapshot tx)) -> Outcome tx) -> Outcome tx)
-> (Map Party (Signature (Snapshot tx)) -> Outcome tx)
-> Outcome tx
forall a b. (a -> b) -> a -> b
$ \Map Party (Signature (Snapshot tx))
sigs' -> do
            -- Spec: σ̃ ← MS-ASig(kₕˢᵉᵗᵘᵖ,̂Σ)
            let multisig :: MultiSignature (Snapshot tx)
multisig = Map Party (Signature (Snapshot tx))
-> [Party] -> MultiSignature (Snapshot tx)
forall {k1} k2 (a :: k1).
Ord k2 =>
Map k2 (Signature a) -> [k2] -> MultiSignature a
aggregateInOrder Map Party (Signature (Snapshot tx))
sigs' [Party]
parties
            -- Spec: η ← combine(𝑈ˆ)
            --       ηω ← combine(outputs(txω))
            --       require MS-Verify(k ̃H, (cid‖v̂‖ŝ‖η‖ηω), σ̃)
            MultiSignature (Snapshot tx)
-> Snapshot tx -> Outcome tx -> Outcome tx
requireVerifiedMultisignature MultiSignature (Snapshot tx)
multisig Snapshot tx
snapshot (Outcome tx -> Outcome tx) -> Outcome tx -> Outcome tx
forall a b. (a -> b) -> a -> b
$
              do
                -- Spec: ̅S ← snObj(v̂, ŝ, Û, T̂, txω)
                --       ̅S.σ ← ̃σ
                StateChanged tx -> Outcome tx
forall tx. StateChanged tx -> Outcome tx
newState SnapshotConfirmed{Snapshot tx
$sel:snapshot:HeadInitialized :: Snapshot tx
snapshot :: Snapshot tx
snapshot, $sel:signatures:HeadInitialized :: MultiSignature (Snapshot tx)
signatures = MultiSignature (Snapshot tx)
multisig}
                Outcome tx -> Outcome tx -> Outcome tx
forall a. Semigroup a => a -> a -> a
<> Effect tx -> Outcome tx
forall tx. Effect tx -> Outcome tx
cause (ServerOutput tx -> Effect tx
forall tx. ServerOutput tx -> Effect tx
ClientEffect (ServerOutput tx -> Effect tx) -> ServerOutput tx -> Effect tx
forall a b. (a -> b) -> a -> b
$ HeadId
-> Snapshot tx -> MultiSignature (Snapshot tx) -> ServerOutput tx
forall tx.
HeadId
-> Snapshot tx -> MultiSignature (Snapshot tx) -> ServerOutput tx
ServerOutput.SnapshotConfirmed HeadId
headId Snapshot tx
snapshot MultiSignature (Snapshot tx)
multisig)
                -- Spec: if txω ≠ ⊥
                --         postTx (decrement, v̂, ŝ, η, ηω)
                Outcome tx -> (Outcome tx -> Outcome tx) -> Outcome tx
forall a b. a -> (a -> b) -> b
& Snapshot tx
-> MultiSignature (Snapshot tx) -> Outcome tx -> Outcome tx
maybePostIncrementTx Snapshot tx
snapshot MultiSignature (Snapshot tx)
multisig
                Outcome tx -> (Outcome tx -> Outcome tx) -> Outcome tx
forall a b. a -> (a -> b) -> b
& Snapshot tx
-> MultiSignature (Snapshot tx) -> Outcome tx -> Outcome tx
maybePostDecrementTx Snapshot tx
snapshot MultiSignature (Snapshot tx)
multisig
                -- Spec: if leader(s + 1) = i ∧ T̂ ≠ ∅
                --         multicast (reqSn, v, ̅S.s + 1, T̂, txω)
                Outcome tx -> (Outcome tx -> Outcome tx) -> Outcome tx
forall a b. a -> (a -> b) -> b
& SnapshotNumber -> Outcome tx -> Outcome tx
maybeRequestNextSnapshot (Snapshot tx -> SnapshotNumber
forall tx. Snapshot tx -> SnapshotNumber
number Snapshot tx
snapshot SnapshotNumber -> SnapshotNumber -> SnapshotNumber
forall a. Num a => a -> a -> a
+ SnapshotNumber
1)
 where
  seenSn :: SnapshotNumber
seenSn = SeenSnapshot tx -> SnapshotNumber
forall tx. SeenSnapshot tx -> SnapshotNumber
seenSnapshotNumber SeenSnapshot tx
seenSnapshot

  requireValidAckSn :: Outcome tx -> Outcome tx
requireValidAckSn Outcome tx
continue =
    if SnapshotNumber
sn SnapshotNumber -> [SnapshotNumber] -> Bool
forall (f :: * -> *) a.
(Foldable f, DisallowElem f, Eq a) =>
a -> f a -> Bool
`elem` [SnapshotNumber
seenSn, SnapshotNumber
seenSn SnapshotNumber -> SnapshotNumber -> SnapshotNumber
forall a. Num a => a -> a -> a
+ SnapshotNumber
1]
      then Outcome tx
continue
      else LogicError tx -> Outcome tx
forall tx. LogicError tx -> Outcome tx
Error (LogicError tx -> Outcome tx) -> LogicError tx -> Outcome tx
forall a b. (a -> b) -> a -> b
$ RequirementFailure tx -> LogicError tx
forall tx. RequirementFailure tx -> LogicError tx
RequireFailed (RequirementFailure tx -> LogicError tx)
-> RequirementFailure tx -> LogicError tx
forall a b. (a -> b) -> a -> b
$ AckSnNumberInvalid{$sel:requestedSn:ReqSnNumberInvalid :: SnapshotNumber
requestedSn = SnapshotNumber
sn, $sel:lastSeenSn:ReqSnNumberInvalid :: SnapshotNumber
lastSeenSn = SnapshotNumber
seenSn}

  waitOnSeenSnapshot :: (Snapshot tx -> Map Party (Signature (Snapshot tx)) -> Outcome tx)
-> Outcome tx
waitOnSeenSnapshot Snapshot tx -> Map Party (Signature (Snapshot tx)) -> Outcome tx
continue =
    case SeenSnapshot tx
seenSnapshot of
      SeenSnapshot Snapshot tx
snapshot Map Party (Signature (Snapshot tx))
sigs
        | SnapshotNumber
seenSn SnapshotNumber -> SnapshotNumber -> Bool
forall a. Eq a => a -> a -> Bool
== SnapshotNumber
sn -> Snapshot tx -> Map Party (Signature (Snapshot tx)) -> Outcome tx
continue Snapshot tx
snapshot Map Party (Signature (Snapshot tx))
sigs
      SeenSnapshot tx
_ -> WaitReason tx -> Outcome tx
forall tx. WaitReason tx -> Outcome tx
wait WaitReason tx
forall tx. WaitReason tx
WaitOnSeenSnapshot

  requireNotSignedYet :: Map Party (Signature (Snapshot tx)) -> Outcome tx -> Outcome tx
requireNotSignedYet Map Party (Signature (Snapshot tx))
sigs Outcome tx
continue =
    if Bool -> Bool
not (Party -> Map Party (Signature (Snapshot tx)) -> Bool
forall k a. Ord k => k -> Map k a -> Bool
Map.member Party
otherParty Map Party (Signature (Snapshot tx))
sigs)
      then Outcome tx
continue
      else LogicError tx -> Outcome tx
forall tx. LogicError tx -> Outcome tx
Error (LogicError tx -> Outcome tx) -> LogicError tx -> Outcome tx
forall a b. (a -> b) -> a -> b
$ RequirementFailure tx -> LogicError tx
forall tx. RequirementFailure tx -> LogicError tx
RequireFailed (RequirementFailure tx -> LogicError tx)
-> RequirementFailure tx -> LogicError tx
forall a b. (a -> b) -> a -> b
$ SnapshotAlreadySigned{$sel:knownSignatures:ReqSnNumberInvalid :: [Party]
knownSignatures = Map Party (Signature (Snapshot tx)) -> [Party]
forall k a. Map k a -> [k]
Map.keys Map Party (Signature (Snapshot tx))
sigs, $sel:receivedSignature:ReqSnNumberInvalid :: Party
receivedSignature = Party
otherParty}

  ifAllMembersHaveSigned :: Snapshot tx
-> Map Party (Signature (Snapshot tx))
-> (Map Party (Signature (Snapshot tx)) -> Outcome tx)
-> Outcome tx
ifAllMembersHaveSigned Snapshot tx
snapshot Map Party (Signature (Snapshot tx))
sigs Map Party (Signature (Snapshot tx)) -> Outcome tx
cont =
    let sigs' :: Map Party (Signature (Snapshot tx))
sigs' = Party
-> Signature (Snapshot tx)
-> Map Party (Signature (Snapshot tx))
-> Map Party (Signature (Snapshot tx))
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Party
otherParty Signature (Snapshot tx)
snapshotSignature Map Party (Signature (Snapshot tx))
sigs
     in if Map Party (Signature (Snapshot tx)) -> Set Party
forall k a. Map k a -> Set k
Map.keysSet Map Party (Signature (Snapshot tx))
sigs' Set Party -> Set Party -> Bool
forall a. Eq a => a -> a -> Bool
== [Party] -> Set Party
forall a. Ord a => [a] -> Set a
Set.fromList [Party]
parties
          then Map Party (Signature (Snapshot tx)) -> Outcome tx
cont Map Party (Signature (Snapshot tx))
sigs'
          else
            StateChanged tx -> Outcome tx
forall tx. StateChanged tx -> Outcome tx
newState
              PartySignedSnapshot
                { Snapshot tx
$sel:snapshot:HeadInitialized :: Snapshot tx
snapshot :: Snapshot tx
snapshot
                , $sel:party:HeadInitialized :: Party
party = Party
otherParty
                , $sel:signature:HeadInitialized :: Signature (Snapshot tx)
signature = Signature (Snapshot tx)
snapshotSignature
                }

  requireVerifiedMultisignature :: MultiSignature (Snapshot tx)
-> Snapshot tx -> Outcome tx -> Outcome tx
requireVerifiedMultisignature MultiSignature (Snapshot tx)
multisig Snapshot tx
msg Outcome tx
cont =
    case [VerificationKey HydraKey]
-> MultiSignature (Snapshot tx) -> Snapshot tx -> Verified
forall a.
SignableRepresentation a =>
[VerificationKey HydraKey] -> MultiSignature a -> a -> Verified
verifyMultiSignature [VerificationKey HydraKey]
vkeys MultiSignature (Snapshot tx)
multisig Snapshot tx
msg of
      Verified
Verified -> Outcome tx
cont
      FailedKeys [VerificationKey HydraKey]
failures ->
        LogicError tx -> Outcome tx
forall tx. LogicError tx -> Outcome tx
Error (LogicError tx -> Outcome tx) -> LogicError tx -> Outcome tx
forall a b. (a -> b) -> a -> b
$
          RequirementFailure tx -> LogicError tx
forall tx. RequirementFailure tx -> LogicError tx
RequireFailed (RequirementFailure tx -> LogicError tx)
-> RequirementFailure tx -> LogicError tx
forall a b. (a -> b) -> a -> b
$
            InvalidMultisignature{$sel:multisig:ReqSnNumberInvalid :: Text
multisig = MultiSignature (Snapshot tx) -> Text
forall b a. (Show a, IsString b) => a -> b
show MultiSignature (Snapshot tx)
multisig, $sel:vkeys:ReqSnNumberInvalid :: [VerificationKey HydraKey]
vkeys = [VerificationKey HydraKey]
failures}
      Verified
KeyNumberMismatch ->
        LogicError tx -> Outcome tx
forall tx. LogicError tx -> Outcome tx
Error (LogicError tx -> Outcome tx) -> LogicError tx -> Outcome tx
forall a b. (a -> b) -> a -> b
$
          RequirementFailure tx -> LogicError tx
forall tx. RequirementFailure tx -> LogicError tx
RequireFailed (RequirementFailure tx -> LogicError tx)
-> RequirementFailure tx -> LogicError tx
forall a b. (a -> b) -> a -> b
$
            InvalidMultisignature{$sel:multisig:ReqSnNumberInvalid :: Text
multisig = MultiSignature (Snapshot tx) -> Text
forall b a. (Show a, IsString b) => a -> b
show MultiSignature (Snapshot tx)
multisig, [VerificationKey HydraKey]
vkeys :: [VerificationKey HydraKey]
$sel:vkeys:ReqSnNumberInvalid :: [VerificationKey HydraKey]
vkeys}

  maybeRequestNextSnapshot :: SnapshotNumber -> Outcome tx -> Outcome tx
maybeRequestNextSnapshot SnapshotNumber
nextSn Outcome tx
outcome =
    if HeadParameters -> Party -> SnapshotNumber -> Bool
isLeader HeadParameters
parameters Party
party SnapshotNumber
nextSn Bool -> Bool -> Bool
&& Bool -> Bool
not ([tx] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [tx]
localTxs)
      then
        Outcome tx
outcome
          Outcome tx -> Outcome tx -> Outcome tx
forall a. Semigroup a => a -> a -> a
<> StateChanged tx -> Outcome tx
forall tx. StateChanged tx -> Outcome tx
newState SnapshotRequestDecided{$sel:snapshotNumber:HeadInitialized :: SnapshotNumber
snapshotNumber = SnapshotNumber
nextSn}
          Outcome tx -> Outcome tx -> Outcome tx
forall a. Semigroup a => a -> a -> a
<> Effect tx -> Outcome tx
forall tx. Effect tx -> Outcome tx
cause (Message tx -> Effect tx
forall tx. Message tx -> Effect tx
NetworkEffect (Message tx -> Effect tx) -> Message tx -> Effect tx
forall a b. (a -> b) -> a -> b
$ SnapshotVersion
-> SnapshotNumber
-> [TxIdType tx]
-> Maybe tx
-> Maybe (UTxOType tx)
-> Message tx
forall tx.
SnapshotVersion
-> SnapshotNumber
-> [TxIdType tx]
-> Maybe tx
-> Maybe (UTxOType tx)
-> Message tx
ReqSn SnapshotVersion
version SnapshotNumber
nextSn (tx -> TxIdType tx
forall tx. IsTx tx => tx -> TxIdType tx
txId (tx -> TxIdType tx) -> [tx] -> [TxIdType tx]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [tx]
localTxs) Maybe tx
decommitTx Maybe (UTxOType tx)
pendingDeposit)
      else Outcome tx
outcome

  maybePostIncrementTx :: Snapshot tx
-> MultiSignature (Snapshot tx) -> Outcome tx -> Outcome tx
maybePostIncrementTx snapshot :: Snapshot tx
snapshot@Snapshot{Maybe (UTxOType tx)
$sel:utxoToCommit:Snapshot :: forall tx. Snapshot tx -> Maybe (UTxOType tx)
utxoToCommit :: Maybe (UTxOType tx)
utxoToCommit} MultiSignature (Snapshot tx)
signatures Outcome tx
outcome =
    case ((TxIdType tx, UTxOType tx) -> Bool)
-> [(TxIdType tx, UTxOType tx)] -> Maybe (TxIdType tx, UTxOType tx)
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
find (\(TxIdType tx
_, UTxOType tx
depositUTxO) -> UTxOType tx -> Maybe (UTxOType tx)
forall a. a -> Maybe a
Just UTxOType tx
depositUTxO Maybe (UTxOType tx) -> Maybe (UTxOType tx) -> Bool
forall a. Eq a => a -> a -> Bool
== Maybe (UTxOType tx)
utxoToCommit) (Map (TxIdType tx) (UTxOType tx) -> [(TxIdType tx, UTxOType tx)]
forall k a. Map k a -> [(k, a)]
Map.assocs Map (TxIdType tx) (UTxOType tx)
pendingDeposits) of
      Just (TxIdType tx
depositTxId, UTxOType tx
depositUTxO) ->
        Outcome tx
outcome
          Outcome tx -> Outcome tx -> Outcome tx
forall a. Semigroup a => a -> a -> a
<> [Effect tx] -> Outcome tx
forall tx. [Effect tx] -> Outcome tx
causes
            [ ServerOutput tx -> Effect tx
forall tx. ServerOutput tx -> Effect tx
ClientEffect (ServerOutput tx -> Effect tx) -> ServerOutput tx -> Effect tx
forall a b. (a -> b) -> a -> b
$
                ServerOutput.CommitApproved
                  { HeadId
$sel:headId:PeerConnected :: HeadId
headId :: HeadId
headId
                  , $sel:utxoToCommit:PeerConnected :: UTxOType tx
utxoToCommit = UTxOType tx
depositUTxO
                  }
            , OnChainEffect
                { $sel:postChainTx:ClientEffect :: PostChainTx tx
postChainTx =
                    IncrementTx
                      { HeadId
$sel:headId:InitTx :: HeadId
headId :: HeadId
headId
                      , $sel:headParameters:InitTx :: HeadParameters
headParameters = HeadParameters
parameters
                      , $sel:incrementingSnapshot:InitTx :: ConfirmedSnapshot tx
incrementingSnapshot = ConfirmedSnapshot{Snapshot tx
$sel:snapshot:InitialSnapshot :: Snapshot tx
snapshot :: Snapshot tx
snapshot, MultiSignature (Snapshot tx)
signatures :: MultiSignature (Snapshot tx)
$sel:signatures:InitialSnapshot :: MultiSignature (Snapshot tx)
signatures}
                      , TxIdType tx
depositTxId :: TxIdType tx
$sel:depositTxId:InitTx :: TxIdType tx
depositTxId
                      }
                }
            ]
      Maybe (TxIdType tx, UTxOType tx)
_ -> Outcome tx
outcome -- TODO: output some error here?
  maybePostDecrementTx :: Snapshot tx
-> MultiSignature (Snapshot tx) -> Outcome tx -> Outcome tx
maybePostDecrementTx snapshot :: Snapshot tx
snapshot@Snapshot{Maybe (UTxOType tx)
$sel:utxoToDecommit:Snapshot :: forall tx. Snapshot tx -> Maybe (UTxOType tx)
utxoToDecommit :: Maybe (UTxOType tx)
utxoToDecommit} MultiSignature (Snapshot tx)
signatures Outcome tx
outcome =
    case (Maybe tx
decommitTx, Maybe (UTxOType tx)
utxoToDecommit) of
      (Just tx
tx, Just UTxOType tx
utxo) ->
        Outcome tx
outcome
          Outcome tx -> Outcome tx -> Outcome tx
forall a. Semigroup a => a -> a -> a
<> [Effect tx] -> Outcome tx
forall tx. [Effect tx] -> Outcome tx
causes
            [ ServerOutput tx -> Effect tx
forall tx. ServerOutput tx -> Effect tx
ClientEffect (ServerOutput tx -> Effect tx) -> ServerOutput tx -> Effect tx
forall a b. (a -> b) -> a -> b
$
                ServerOutput.DecommitApproved
                  { HeadId
$sel:headId:PeerConnected :: HeadId
headId :: HeadId
headId
                  , $sel:decommitTxId:PeerConnected :: TxIdType tx
decommitTxId = tx -> TxIdType tx
forall tx. IsTx tx => tx -> TxIdType tx
txId tx
tx
                  , $sel:utxoToDecommit:PeerConnected :: UTxOType tx
utxoToDecommit = UTxOType tx
utxo
                  }
            , OnChainEffect
                { $sel:postChainTx:ClientEffect :: PostChainTx tx
postChainTx =
                    DecrementTx
                      { HeadId
$sel:headId:InitTx :: HeadId
headId :: HeadId
headId
                      , $sel:headParameters:InitTx :: HeadParameters
headParameters = HeadParameters
parameters
                      , $sel:decrementingSnapshot:InitTx :: ConfirmedSnapshot tx
decrementingSnapshot = ConfirmedSnapshot{Snapshot tx
$sel:snapshot:InitialSnapshot :: Snapshot tx
snapshot :: Snapshot tx
snapshot, MultiSignature (Snapshot tx)
$sel:signatures:InitialSnapshot :: MultiSignature (Snapshot tx)
signatures :: MultiSignature (Snapshot tx)
signatures}
                      }
                }
            ]
      (Maybe tx, Maybe (UTxOType tx))
_ -> Outcome tx
outcome

  vkeys :: [VerificationKey HydraKey]
vkeys = Party -> VerificationKey HydraKey
vkey (Party -> VerificationKey HydraKey)
-> [Party] -> [VerificationKey HydraKey]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Party]
parties

  OpenState
    { $sel:parameters:OpenState :: forall tx. OpenState tx -> HeadParameters
parameters = parameters :: HeadParameters
parameters@HeadParameters{[Party]
$sel:parties:HeadParameters :: HeadParameters -> [Party]
parties :: [Party]
parties}
    , CoordinatedHeadState tx
$sel:coordinatedHeadState:OpenState :: forall tx. OpenState tx -> CoordinatedHeadState tx
coordinatedHeadState :: CoordinatedHeadState tx
coordinatedHeadState
    , HeadId
$sel:headId:OpenState :: forall tx. OpenState tx -> HeadId
headId :: HeadId
headId
    } = OpenState tx
openState

  pendingDeposit :: Maybe (UTxOType tx)
pendingDeposit =
    case Map (TxIdType tx) (UTxOType tx) -> [(TxIdType tx, UTxOType tx)]
forall k a. Map k a -> [(k, a)]
Map.toList Map (TxIdType tx) (UTxOType tx)
pendingDeposits of
      [] -> Maybe (UTxOType tx)
forall a. Maybe a
Nothing
      (TxIdType tx
_, UTxOType tx
depositUTxO) : [(TxIdType tx, UTxOType tx)]
_ -> UTxOType tx -> Maybe (UTxOType tx)
forall a. a -> Maybe a
Just UTxOType tx
depositUTxO

  CoordinatedHeadState{SeenSnapshot tx
$sel:seenSnapshot:CoordinatedHeadState :: forall tx. CoordinatedHeadState tx -> SeenSnapshot tx
seenSnapshot :: SeenSnapshot tx
seenSnapshot, [tx]
$sel:localTxs:CoordinatedHeadState :: forall tx. CoordinatedHeadState tx -> [tx]
localTxs :: [tx]
localTxs, Maybe tx
$sel:decommitTx:CoordinatedHeadState :: forall tx. CoordinatedHeadState tx -> Maybe tx
decommitTx :: Maybe tx
decommitTx, Map (TxIdType tx) (UTxOType tx)
$sel:pendingDeposits:CoordinatedHeadState :: forall tx.
CoordinatedHeadState tx -> Map (TxIdType tx) (UTxOType tx)
pendingDeposits :: Map (TxIdType tx) (UTxOType tx)
pendingDeposits, SnapshotVersion
$sel:version:CoordinatedHeadState :: forall tx. CoordinatedHeadState tx -> SnapshotVersion
version :: SnapshotVersion
version} = CoordinatedHeadState tx
coordinatedHeadState

-- | Client request to recover deposited UTxO.
--
-- __Transition__: 'OpenState' → 'OpenState'
onOpenClientRecover ::
  IsTx tx =>
  HeadId ->
  ChainSlot ->
  CoordinatedHeadState tx ->
  TxIdType tx ->
  Outcome tx
onOpenClientRecover :: forall tx.
IsTx tx =>
HeadId
-> ChainSlot
-> CoordinatedHeadState tx
-> TxIdType tx
-> Outcome tx
onOpenClientRecover HeadId
headId ChainSlot
currentSlot CoordinatedHeadState tx
coordinatedHeadState TxIdType tx
recoverTxId =
  case TxIdType tx
-> Map (TxIdType tx) (UTxOType tx) -> Maybe (UTxOType tx)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup TxIdType tx
recoverTxId Map (TxIdType tx) (UTxOType tx)
pendingDeposits of
    Maybe (UTxOType tx)
Nothing ->
      LogicError tx -> Outcome tx
forall tx. LogicError tx -> Outcome tx
Error (LogicError tx -> Outcome tx) -> LogicError tx -> Outcome tx
forall a b. (a -> b) -> a -> b
$ RequirementFailure tx -> LogicError tx
forall tx. RequirementFailure tx -> LogicError tx
RequireFailed RequirementFailure tx
forall tx. RequirementFailure tx
RecoverNotMatchingDeposit
    Just UTxOType tx
_ ->
      [Effect tx] -> Outcome tx
forall tx. [Effect tx] -> Outcome tx
causes
        [ OnChainEffect
            { $sel:postChainTx:ClientEffect :: PostChainTx tx
postChainTx =
                RecoverTx
                  { HeadId
$sel:headId:InitTx :: HeadId
headId :: HeadId
headId
                  , $sel:recoverTxId:InitTx :: TxIdType tx
recoverTxId = TxIdType tx
recoverTxId
                  , $sel:deadline:InitTx :: ChainSlot
deadline = ChainSlot
currentSlot
                  }
            }
        ]
 where
  CoordinatedHeadState{Map (TxIdType tx) (UTxOType tx)
$sel:pendingDeposits:CoordinatedHeadState :: forall tx.
CoordinatedHeadState tx -> Map (TxIdType tx) (UTxOType tx)
pendingDeposits :: Map (TxIdType tx) (UTxOType tx)
pendingDeposits} = CoordinatedHeadState tx
coordinatedHeadState

-- | Client request to decommit UTxO from the head.
--
-- Only possible if there is no decommit _in flight_ and if the tx applies
-- cleanly to the local ledger state.
--
-- __Transition__: 'OpenState' → 'OpenState'
onOpenClientDecommit ::
  IsTx tx =>
  HeadId ->
  Ledger tx ->
  ChainSlot ->
  CoordinatedHeadState tx ->
  -- | Decommit transaction.
  tx ->
  Outcome tx
onOpenClientDecommit :: forall tx.
IsTx tx =>
HeadId
-> Ledger tx
-> ChainSlot
-> CoordinatedHeadState tx
-> tx
-> Outcome tx
onOpenClientDecommit HeadId
headId Ledger tx
ledger ChainSlot
currentSlot CoordinatedHeadState tx
coordinatedHeadState tx
decommitTx =
  Outcome tx -> Outcome tx
checkNoDecommitInFlight (Outcome tx -> Outcome tx) -> Outcome tx -> Outcome tx
forall a b. (a -> b) -> a -> b
$
    Outcome tx -> Outcome tx
checkValidDecommitTx (Outcome tx -> Outcome tx) -> Outcome tx -> Outcome tx
forall a b. (a -> b) -> a -> b
$
      Effect tx -> Outcome tx
forall tx. Effect tx -> Outcome tx
cause (Message tx -> Effect tx
forall tx. Message tx -> Effect tx
NetworkEffect ReqDec{$sel:transaction:ReqTx :: tx
transaction = tx
decommitTx})
 where
  checkNoDecommitInFlight :: Outcome tx -> Outcome tx
checkNoDecommitInFlight Outcome tx
continue =
    case Maybe tx
mExistingDecommitTx of
      Just tx
existingDecommitTx ->
        Effect tx -> Outcome tx
forall tx. Effect tx -> Outcome tx
cause
          ( ServerOutput tx -> Effect tx
forall tx. ServerOutput tx -> Effect tx
ClientEffect
              ServerOutput.DecommitInvalid
                { HeadId
$sel:headId:PeerConnected :: HeadId
headId :: HeadId
headId
                , tx
decommitTx :: tx
$sel:decommitTx:PeerConnected :: tx
decommitTx
                , $sel:decommitInvalidReason:PeerConnected :: DecommitInvalidReason tx
decommitInvalidReason =
                    ServerOutput.DecommitAlreadyInFlight
                      { $sel:otherDecommitTxId:DecommitTxInvalid :: TxIdType tx
otherDecommitTxId = tx -> TxIdType tx
forall tx. IsTx tx => tx -> TxIdType tx
txId tx
existingDecommitTx
                      }
                }
          )
      Maybe tx
Nothing -> Outcome tx
continue

  checkValidDecommitTx :: Outcome tx -> Outcome tx
checkValidDecommitTx Outcome tx
cont =
    case Ledger tx
-> ChainSlot
-> UTxOType tx
-> [tx]
-> Either (tx, ValidationError) (UTxOType tx)
forall tx.
Ledger tx
-> ChainSlot
-> UTxOType tx
-> [tx]
-> Either (tx, ValidationError) (UTxOType tx)
applyTransactions Ledger tx
ledger ChainSlot
currentSlot UTxOType tx
localUTxO [tx
decommitTx] of
      Left (tx
_, ValidationError
err) ->
        Effect tx -> Outcome tx
forall tx. Effect tx -> Outcome tx
cause
          ( ServerOutput tx -> Effect tx
forall tx. ServerOutput tx -> Effect tx
ClientEffect
              ServerOutput.DecommitInvalid
                { HeadId
$sel:headId:PeerConnected :: HeadId
headId :: HeadId
headId
                , tx
decommitTx :: tx
$sel:decommitTx:PeerConnected :: tx
decommitTx
                , $sel:decommitInvalidReason:PeerConnected :: DecommitInvalidReason tx
decommitInvalidReason =
                    ServerOutput.DecommitTxInvalid
                      { UTxOType tx
localUTxO :: UTxOType tx
$sel:localUTxO:DecommitTxInvalid :: UTxOType tx
localUTxO
                      , $sel:validationError:DecommitTxInvalid :: ValidationError
validationError = ValidationError
err
                      }
                }
          )
      Right UTxOType tx
_ -> Outcome tx
cont

  CoordinatedHeadState{$sel:decommitTx:CoordinatedHeadState :: forall tx. CoordinatedHeadState tx -> Maybe tx
decommitTx = Maybe tx
mExistingDecommitTx, UTxOType tx
$sel:localUTxO:CoordinatedHeadState :: forall tx. CoordinatedHeadState tx -> UTxOType tx
localUTxO :: UTxOType tx
localUTxO} = CoordinatedHeadState tx
coordinatedHeadState

-- | Process the request 'ReqDec' to decommit something from the Open head.
--
-- __Transition__: 'OpenState' → 'OpenState'
--
-- When node receives 'ReqDec' network message it should:
-- - Check there is no decommit in flight:
--   - Alter it's state to record what is to be decommitted
--   - Issue a server output 'DecommitRequested' with the relevant utxo
--   - Issue a 'ReqSn' since all parties need to agree in order for decommit to
--   be taken out of a Head.
-- - Check if we are the leader
onOpenNetworkReqDec ::
  IsTx tx =>
  Environment ->
  Ledger tx ->
  TTL ->
  OpenState tx ->
  tx ->
  Outcome tx
onOpenNetworkReqDec :: forall tx.
IsTx tx =>
Environment -> Ledger tx -> TTL -> OpenState tx -> tx -> Outcome tx
onOpenNetworkReqDec Environment
env Ledger tx
ledger TTL
ttl OpenState tx
openState tx
decommitTx =
  -- Spec: wait txω =⊥ ∧ L̂ ◦ tx ≠ ⊥
  (UTxOType tx -> Outcome tx) -> Outcome tx
waitOnApplicableDecommit ((UTxOType tx -> Outcome tx) -> Outcome tx)
-> (UTxOType tx -> Outcome tx) -> Outcome tx
forall a b. (a -> b) -> a -> b
$ \UTxOType tx
newLocalUTxO -> do
    -- Spec: L̂ ← L̂ ◦ tx \ outputs(tx)
    let decommitUTxO :: UTxOType tx
decommitUTxO = tx -> UTxOType tx
forall tx. IsTx tx => tx -> UTxOType tx
utxoFromTx tx
decommitTx
        activeUTxO :: UTxOType tx
activeUTxO = UTxOType tx
newLocalUTxO UTxOType tx -> UTxOType tx -> UTxOType tx
forall tx. IsTx tx => UTxOType tx -> UTxOType tx -> UTxOType tx
`withoutUTxO` UTxOType tx
decommitUTxO
    -- Spec: txω ← tx
    StateChanged tx -> Outcome tx
forall tx. StateChanged tx -> Outcome tx
newState DecommitRecorded{tx
decommitTx :: tx
$sel:decommitTx:HeadInitialized :: tx
decommitTx, $sel:newLocalUTxO:HeadInitialized :: UTxOType tx
newLocalUTxO = UTxOType tx
activeUTxO}
      Outcome tx -> Outcome tx -> Outcome tx
forall a. Semigroup a => a -> a -> a
<> Effect tx -> Outcome tx
forall tx. Effect tx -> Outcome tx
cause
        ( ServerOutput tx -> Effect tx
forall tx. ServerOutput tx -> Effect tx
ClientEffect (ServerOutput tx -> Effect tx) -> ServerOutput tx -> Effect tx
forall a b. (a -> b) -> a -> b
$
            ServerOutput.DecommitRequested
              { HeadId
$sel:headId:PeerConnected :: HeadId
headId :: HeadId
headId
              , $sel:decommitTx:PeerConnected :: tx
decommitTx = tx
decommitTx
              , $sel:utxoToDecommit:PeerConnected :: UTxOType tx
utxoToDecommit = UTxOType tx
decommitUTxO
              }
        )
      -- Spec: if ŝ = ̅S.s ∧ leader(̅S.s + 1) = i
      --         multicast (reqSn, v, ̅S.s + 1, T̂ , txω )
      Outcome tx -> Outcome tx -> Outcome tx
forall a. Semigroup a => a -> a -> a
<> Outcome tx
maybeRequestSnapshot
 where
  waitOnApplicableDecommit :: (UTxOType tx -> Outcome tx) -> Outcome tx
waitOnApplicableDecommit UTxOType tx -> Outcome tx
cont =
    case Maybe tx
mExistingDecommitTx of
      Maybe tx
Nothing ->
        case ChainSlot
-> UTxOType tx
-> [tx]
-> Either (tx, ValidationError) (UTxOType tx)
applyTransactions ChainSlot
currentSlot UTxOType tx
localUTxO [tx
decommitTx] of
          Right UTxOType tx
utxo' -> UTxOType tx -> Outcome tx
cont UTxOType tx
utxo'
          Left (tx
_, ValidationError
validationError)
            | TTL
ttl TTL -> TTL -> Bool
forall a. Ord a => a -> a -> Bool
> TTL
0 ->
                WaitReason tx -> Outcome tx
forall tx. WaitReason tx -> Outcome tx
wait (WaitReason tx -> Outcome tx) -> WaitReason tx -> Outcome tx
forall a b. (a -> b) -> a -> b
$
                  DecommitInvalidReason tx -> WaitReason tx
forall tx. DecommitInvalidReason tx -> WaitReason tx
WaitOnNotApplicableDecommitTx
                    ServerOutput.DecommitTxInvalid{UTxOType tx
$sel:localUTxO:DecommitTxInvalid :: UTxOType tx
localUTxO :: UTxOType tx
localUTxO, ValidationError
$sel:validationError:DecommitTxInvalid :: ValidationError
validationError :: ValidationError
validationError}
            | Bool
otherwise ->
                Effect tx -> Outcome tx
forall tx. Effect tx -> Outcome tx
cause (Effect tx -> Outcome tx)
-> (ServerOutput tx -> Effect tx) -> ServerOutput tx -> Outcome tx
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ServerOutput tx -> Effect tx
forall tx. ServerOutput tx -> Effect tx
ClientEffect (ServerOutput tx -> Outcome tx) -> ServerOutput tx -> Outcome tx
forall a b. (a -> b) -> a -> b
$
                  ServerOutput.DecommitInvalid
                    { HeadId
$sel:headId:PeerConnected :: HeadId
headId :: HeadId
headId
                    , tx
$sel:decommitTx:PeerConnected :: tx
decommitTx :: tx
decommitTx
                    , $sel:decommitInvalidReason:PeerConnected :: DecommitInvalidReason tx
decommitInvalidReason =
                        ServerOutput.DecommitTxInvalid{UTxOType tx
$sel:localUTxO:DecommitTxInvalid :: UTxOType tx
localUTxO :: UTxOType tx
localUTxO, ValidationError
$sel:validationError:DecommitTxInvalid :: ValidationError
validationError :: ValidationError
validationError}
                    }
      Just tx
existingDecommitTx
        | TTL
ttl TTL -> TTL -> Bool
forall a. Ord a => a -> a -> Bool
> TTL
0 ->
            WaitReason tx -> Outcome tx
forall tx. WaitReason tx -> Outcome tx
wait (WaitReason tx -> Outcome tx) -> WaitReason tx -> Outcome tx
forall a b. (a -> b) -> a -> b
$
              DecommitInvalidReason tx -> WaitReason tx
forall tx. DecommitInvalidReason tx -> WaitReason tx
WaitOnNotApplicableDecommitTx
                DecommitAlreadyInFlight{$sel:otherDecommitTxId:DecommitTxInvalid :: TxIdType tx
otherDecommitTxId = tx -> TxIdType tx
forall tx. IsTx tx => tx -> TxIdType tx
txId tx
existingDecommitTx}
        | Bool
otherwise ->
            Effect tx -> Outcome tx
forall tx. Effect tx -> Outcome tx
cause (Effect tx -> Outcome tx)
-> (ServerOutput tx -> Effect tx) -> ServerOutput tx -> Outcome tx
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ServerOutput tx -> Effect tx
forall tx. ServerOutput tx -> Effect tx
ClientEffect (ServerOutput tx -> Outcome tx) -> ServerOutput tx -> Outcome tx
forall a b. (a -> b) -> a -> b
$
              ServerOutput.DecommitInvalid
                { HeadId
$sel:headId:PeerConnected :: HeadId
headId :: HeadId
headId
                , tx
$sel:decommitTx:PeerConnected :: tx
decommitTx :: tx
decommitTx
                , $sel:decommitInvalidReason:PeerConnected :: DecommitInvalidReason tx
decommitInvalidReason =
                    DecommitAlreadyInFlight{$sel:otherDecommitTxId:DecommitTxInvalid :: TxIdType tx
otherDecommitTxId = tx -> TxIdType tx
forall tx. IsTx tx => tx -> TxIdType tx
txId tx
existingDecommitTx}
                }

  maybeRequestSnapshot :: Outcome tx
maybeRequestSnapshot =
    if Bool -> Bool
not Bool
snapshotInFlight Bool -> Bool -> Bool
&& HeadParameters -> Party -> SnapshotNumber -> Bool
isLeader HeadParameters
parameters Party
party SnapshotNumber
nextSn
      then Effect tx -> Outcome tx
forall tx. Effect tx -> Outcome tx
cause (Message tx -> Effect tx
forall tx. Message tx -> Effect tx
NetworkEffect (SnapshotVersion
-> SnapshotNumber
-> [TxIdType tx]
-> Maybe tx
-> Maybe (UTxOType tx)
-> Message tx
forall tx.
SnapshotVersion
-> SnapshotNumber
-> [TxIdType tx]
-> Maybe tx
-> Maybe (UTxOType tx)
-> Message tx
ReqSn SnapshotVersion
version SnapshotNumber
nextSn (tx -> TxIdType tx
forall tx. IsTx tx => tx -> TxIdType tx
txId (tx -> TxIdType tx) -> [tx] -> [TxIdType tx]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [tx]
localTxs) (tx -> Maybe tx
forall a. a -> Maybe a
Just tx
decommitTx) Maybe (UTxOType tx)
forall a. Maybe a
Nothing))
      else Outcome tx
forall tx. Outcome tx
noop

  Environment{Party
$sel:party:Environment :: Environment -> Party
party :: Party
party} = Environment
env

  Ledger{ChainSlot
-> UTxOType tx
-> [tx]
-> Either (tx, ValidationError) (UTxOType tx)
$sel:applyTransactions:Ledger :: forall tx.
Ledger tx
-> ChainSlot
-> UTxOType tx
-> [tx]
-> Either (tx, ValidationError) (UTxOType tx)
applyTransactions :: ChainSlot
-> UTxOType tx
-> [tx]
-> Either (tx, ValidationError) (UTxOType tx)
applyTransactions} = Ledger tx
ledger

  Snapshot{SnapshotNumber
$sel:number:Snapshot :: forall tx. Snapshot tx -> SnapshotNumber
number :: SnapshotNumber
number} = ConfirmedSnapshot tx -> Snapshot tx
forall tx. ConfirmedSnapshot tx -> Snapshot tx
getSnapshot ConfirmedSnapshot tx
confirmedSnapshot

  nextSn :: SnapshotNumber
nextSn = SnapshotNumber
number SnapshotNumber -> SnapshotNumber -> SnapshotNumber
forall a. Num a => a -> a -> a
+ SnapshotNumber
1

  snapshotInFlight :: Bool
snapshotInFlight = case SeenSnapshot tx
seenSnapshot of
    SeenSnapshot tx
NoSeenSnapshot -> Bool
False
    LastSeenSnapshot{} -> Bool
False
    RequestedSnapshot{} -> Bool
True
    SeenSnapshot{} -> Bool
True

  CoordinatedHeadState
    { $sel:decommitTx:CoordinatedHeadState :: forall tx. CoordinatedHeadState tx -> Maybe tx
decommitTx = Maybe tx
mExistingDecommitTx
    , ConfirmedSnapshot tx
$sel:confirmedSnapshot:CoordinatedHeadState :: forall tx. CoordinatedHeadState tx -> ConfirmedSnapshot tx
confirmedSnapshot :: ConfirmedSnapshot tx
confirmedSnapshot
    , [tx]
$sel:localTxs:CoordinatedHeadState :: forall tx. CoordinatedHeadState tx -> [tx]
localTxs :: [tx]
localTxs
    , UTxOType tx
$sel:localUTxO:CoordinatedHeadState :: forall tx. CoordinatedHeadState tx -> UTxOType tx
localUTxO :: UTxOType tx
localUTxO
    , SnapshotVersion
$sel:version:CoordinatedHeadState :: forall tx. CoordinatedHeadState tx -> SnapshotVersion
version :: SnapshotVersion
version
    , SeenSnapshot tx
$sel:seenSnapshot:CoordinatedHeadState :: forall tx. CoordinatedHeadState tx -> SeenSnapshot tx
seenSnapshot :: SeenSnapshot tx
seenSnapshot
    } = CoordinatedHeadState tx
coordinatedHeadState

  OpenState
    { HeadId
$sel:headId:OpenState :: forall tx. OpenState tx -> HeadId
headId :: HeadId
headId
    , HeadParameters
$sel:parameters:OpenState :: forall tx. OpenState tx -> HeadParameters
parameters :: HeadParameters
parameters
    , CoordinatedHeadState tx
$sel:coordinatedHeadState:OpenState :: forall tx. OpenState tx -> CoordinatedHeadState tx
coordinatedHeadState :: CoordinatedHeadState tx
coordinatedHeadState
    , ChainSlot
$sel:currentSlot:OpenState :: forall tx. OpenState tx -> ChainSlot
currentSlot :: ChainSlot
currentSlot
    } = OpenState tx
openState

onOpenChainDepositTx ::
  IsTx tx =>
  HeadId ->
  Environment ->
  OpenState tx ->
  -- | Deposited UTxO
  UTxOType tx ->
  -- | Deposit 'TxId'
  TxIdType tx ->
  -- | Deposit deadline
  UTCTime ->
  Outcome tx
onOpenChainDepositTx :: forall tx.
IsTx tx =>
HeadId
-> Environment
-> OpenState tx
-> UTxOType tx
-> TxIdType tx
-> UTCTime
-> Outcome tx
onOpenChainDepositTx HeadId
headId Environment
env OpenState tx
st UTxOType tx
deposited TxIdType tx
depositTxId UTCTime
deadline =
  -- TODO: We should check for deadline and only request snapshots that have deadline further in the future so
  -- we don't end up with a snapshot that is already outdated.
  Outcome tx -> Outcome tx
waitOnUnresolvedDecommit (Outcome tx -> Outcome tx) -> Outcome tx -> Outcome tx
forall a b. (a -> b) -> a -> b
$
    StateChanged tx -> Outcome tx
forall tx. StateChanged tx -> Outcome tx
newState CommitRecorded{pendingDeposits :: Map (TxIdType tx) (UTxOType tx)
pendingDeposits = TxIdType tx -> UTxOType tx -> Map (TxIdType tx) (UTxOType tx)
forall k a. k -> a -> Map k a
Map.singleton TxIdType tx
depositTxId UTxOType tx
deposited, $sel:newLocalUTxO:HeadInitialized :: UTxOType tx
newLocalUTxO = UTxOType tx
localUTxO UTxOType tx -> UTxOType tx -> UTxOType tx
forall a. Semigroup a => a -> a -> a
<> UTxOType tx
deposited}
      Outcome tx -> Outcome tx -> Outcome tx
forall a. Semigroup a => a -> a -> a
<> Effect tx -> Outcome tx
forall tx. Effect tx -> Outcome tx
cause (ServerOutput tx -> Effect tx
forall tx. ServerOutput tx -> Effect tx
ClientEffect (ServerOutput tx -> Effect tx) -> ServerOutput tx -> Effect tx
forall a b. (a -> b) -> a -> b
$ ServerOutput.CommitRecorded{HeadId
$sel:headId:PeerConnected :: HeadId
headId :: HeadId
headId, $sel:utxoToCommit:PeerConnected :: UTxOType tx
utxoToCommit = UTxOType tx
deposited, $sel:pendingDeposit:PeerConnected :: TxIdType tx
pendingDeposit = TxIdType tx
depositTxId, UTCTime
deadline :: UTCTime
$sel:deadline:PeerConnected :: UTCTime
deadline})
      Outcome tx -> Outcome tx -> Outcome tx
forall a. Semigroup a => a -> a -> a
<> if Bool -> Bool
not Bool
snapshotInFlight Bool -> Bool -> Bool
&& HeadParameters -> Party -> SnapshotNumber -> Bool
isLeader HeadParameters
parameters Party
party SnapshotNumber
nextSn
        then
          Effect tx -> Outcome tx
forall tx. Effect tx -> Outcome tx
cause (Message tx -> Effect tx
forall tx. Message tx -> Effect tx
NetworkEffect (Message tx -> Effect tx) -> Message tx -> Effect tx
forall a b. (a -> b) -> a -> b
$ SnapshotVersion
-> SnapshotNumber
-> [TxIdType tx]
-> Maybe tx
-> Maybe (UTxOType tx)
-> Message tx
forall tx.
SnapshotVersion
-> SnapshotNumber
-> [TxIdType tx]
-> Maybe tx
-> Maybe (UTxOType tx)
-> Message tx
ReqSn SnapshotVersion
version SnapshotNumber
nextSn (tx -> TxIdType tx
forall tx. IsTx tx => tx -> TxIdType tx
txId (tx -> TxIdType tx) -> [tx] -> [TxIdType tx]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [tx]
localTxs) Maybe tx
forall a. Maybe a
Nothing (UTxOType tx -> Maybe (UTxOType tx)
forall a. a -> Maybe a
Just UTxOType tx
deposited))
        else Outcome tx
forall tx. Outcome tx
noop
 where
  waitOnUnresolvedDecommit :: Outcome tx -> Outcome tx
waitOnUnresolvedDecommit Outcome tx
cont =
    case Maybe tx
decommitTx of
      Maybe tx
Nothing -> Outcome tx
cont
      Just tx
tx -> WaitReason tx -> Outcome tx
forall tx. WaitReason tx -> Outcome tx
wait (WaitReason tx -> Outcome tx) -> WaitReason tx -> Outcome tx
forall a b. (a -> b) -> a -> b
$ WaitOnUnresolvedDecommit{$sel:decommitTx:WaitOnNotApplicableTx :: tx
decommitTx = tx
tx}

  nextSn :: SnapshotNumber
nextSn = SnapshotNumber
confirmedSn SnapshotNumber -> SnapshotNumber -> SnapshotNumber
forall a. Num a => a -> a -> a
+ SnapshotNumber
1

  Environment{Party
$sel:party:Environment :: Environment -> Party
party :: Party
party} = Environment
env

  CoordinatedHeadState{[tx]
$sel:localTxs:CoordinatedHeadState :: forall tx. CoordinatedHeadState tx -> [tx]
localTxs :: [tx]
localTxs, ConfirmedSnapshot tx
$sel:confirmedSnapshot:CoordinatedHeadState :: forall tx. CoordinatedHeadState tx -> ConfirmedSnapshot tx
confirmedSnapshot :: ConfirmedSnapshot tx
confirmedSnapshot, SeenSnapshot tx
$sel:seenSnapshot:CoordinatedHeadState :: forall tx. CoordinatedHeadState tx -> SeenSnapshot tx
seenSnapshot :: SeenSnapshot tx
seenSnapshot, SnapshotVersion
$sel:version:CoordinatedHeadState :: forall tx. CoordinatedHeadState tx -> SnapshotVersion
version :: SnapshotVersion
version, Maybe tx
$sel:decommitTx:CoordinatedHeadState :: forall tx. CoordinatedHeadState tx -> Maybe tx
decommitTx :: Maybe tx
decommitTx, UTxOType tx
$sel:localUTxO:CoordinatedHeadState :: forall tx. CoordinatedHeadState tx -> UTxOType tx
localUTxO :: UTxOType tx
localUTxO} = CoordinatedHeadState tx
coordinatedHeadState

  Snapshot{$sel:number:Snapshot :: forall tx. Snapshot tx -> SnapshotNumber
number = SnapshotNumber
confirmedSn} = ConfirmedSnapshot tx -> Snapshot tx
forall tx. ConfirmedSnapshot tx -> Snapshot tx
getSnapshot ConfirmedSnapshot tx
confirmedSnapshot

  OpenState{CoordinatedHeadState tx
$sel:coordinatedHeadState:OpenState :: forall tx. OpenState tx -> CoordinatedHeadState tx
coordinatedHeadState :: CoordinatedHeadState tx
coordinatedHeadState, HeadParameters
$sel:parameters:OpenState :: forall tx. OpenState tx -> HeadParameters
parameters :: HeadParameters
parameters} = OpenState tx
st

  snapshotInFlight :: Bool
snapshotInFlight = case SeenSnapshot tx
seenSnapshot of
    SeenSnapshot tx
NoSeenSnapshot -> Bool
False
    LastSeenSnapshot{} -> Bool
False
    RequestedSnapshot{} -> Bool
True
    SeenSnapshot{} -> Bool
True

onOpenChainRecoverTx ::
  IsTx tx =>
  HeadId ->
  OpenState tx ->
  TxIdType tx ->
  Outcome tx
onOpenChainRecoverTx :: forall tx.
IsTx tx =>
HeadId -> OpenState tx -> TxIdType tx -> Outcome tx
onOpenChainRecoverTx HeadId
headId OpenState tx
st TxIdType tx
recoveredTxId =
  case TxIdType tx
-> Map (TxIdType tx) (UTxOType tx) -> Maybe (UTxOType tx)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup TxIdType tx
recoveredTxId Map (TxIdType tx) (UTxOType tx)
pendingDeposits of
    Maybe (UTxOType tx)
Nothing -> LogicError tx -> Outcome tx
forall tx. LogicError tx -> Outcome tx
Error (LogicError tx -> Outcome tx) -> LogicError tx -> Outcome tx
forall a b. (a -> b) -> a -> b
$ RequirementFailure tx -> LogicError tx
forall tx. RequirementFailure tx -> LogicError tx
RequireFailed RequirementFailure tx
forall tx. RequirementFailure tx
RecoverNotMatchingDeposit
    Just UTxOType tx
recoveredUTxO ->
      StateChanged tx -> Outcome tx
forall tx. StateChanged tx -> Outcome tx
newState CommitRecovered{UTxOType tx
recoveredUTxO :: UTxOType tx
$sel:recoveredUTxO:HeadInitialized :: UTxOType tx
recoveredUTxO, $sel:newLocalUTxO:HeadInitialized :: UTxOType tx
newLocalUTxO = UTxOType tx
localUTxO UTxOType tx -> UTxOType tx -> UTxOType tx
forall tx. IsTx tx => UTxOType tx -> UTxOType tx -> UTxOType tx
`withoutUTxO` UTxOType tx
recoveredUTxO, TxIdType tx
recoveredTxId :: TxIdType tx
$sel:recoveredTxId:HeadInitialized :: TxIdType tx
recoveredTxId}
        Outcome tx -> Outcome tx -> Outcome tx
forall a. Semigroup a => a -> a -> a
<> Effect tx -> Outcome tx
forall tx. Effect tx -> Outcome tx
cause
          ( ServerOutput tx -> Effect tx
forall tx. ServerOutput tx -> Effect tx
ClientEffect
              ServerOutput.CommitRecovered
                { HeadId
$sel:headId:PeerConnected :: HeadId
headId :: HeadId
headId
                , TxIdType tx
recoveredTxId :: TxIdType tx
$sel:recoveredTxId:PeerConnected :: TxIdType tx
recoveredTxId
                , UTxOType tx
recoveredUTxO :: UTxOType tx
$sel:recoveredUTxO:PeerConnected :: UTxOType tx
recoveredUTxO
                }
          )
 where
  OpenState{CoordinatedHeadState tx
$sel:coordinatedHeadState:OpenState :: forall tx. OpenState tx -> CoordinatedHeadState tx
coordinatedHeadState :: CoordinatedHeadState tx
coordinatedHeadState} = OpenState tx
st

  CoordinatedHeadState{UTxOType tx
$sel:localUTxO:CoordinatedHeadState :: forall tx. CoordinatedHeadState tx -> UTxOType tx
localUTxO :: UTxOType tx
localUTxO, Map (TxIdType tx) (UTxOType tx)
$sel:pendingDeposits:CoordinatedHeadState :: forall tx.
CoordinatedHeadState tx -> Map (TxIdType tx) (UTxOType tx)
pendingDeposits :: Map (TxIdType tx) (UTxOType tx)
pendingDeposits} = CoordinatedHeadState tx
coordinatedHeadState

-- | Observe a increment transaction. If the outputs match the ones of the
-- pending commit UTxO, then we consider the deposit/increment finalized, and remove the
-- increment UTxO from 'pendingDeposits' from the local state.
--
-- __Transition__: 'OpenState' → 'OpenState'
onOpenChainIncrementTx ::
  OpenState tx ->
  -- | New open state version
  SnapshotVersion ->
  -- | Deposit TxId
  TxIdType tx ->
  Outcome tx
onOpenChainIncrementTx :: forall tx.
OpenState tx -> SnapshotVersion -> TxIdType tx -> Outcome tx
onOpenChainIncrementTx OpenState tx
openState SnapshotVersion
newVersion TxIdType tx
depositTxId =
  StateChanged tx -> Outcome tx
forall tx. StateChanged tx -> Outcome tx
newState CommitFinalized{SnapshotVersion
newVersion :: SnapshotVersion
$sel:newVersion:HeadInitialized :: SnapshotVersion
newVersion, TxIdType tx
depositTxId :: TxIdType tx
$sel:depositTxId:HeadInitialized :: TxIdType tx
depositTxId}
    Outcome tx -> Outcome tx -> Outcome tx
forall a. Semigroup a => a -> a -> a
<> Effect tx -> Outcome tx
forall tx. Effect tx -> Outcome tx
cause (ServerOutput tx -> Effect tx
forall tx. ServerOutput tx -> Effect tx
ClientEffect (ServerOutput tx -> Effect tx) -> ServerOutput tx -> Effect tx
forall a b. (a -> b) -> a -> b
$ ServerOutput.CommitFinalized{HeadId
$sel:headId:PeerConnected :: HeadId
headId :: HeadId
headId, $sel:theDeposit:PeerConnected :: TxIdType tx
theDeposit = TxIdType tx
depositTxId})
 where
  OpenState{HeadId
$sel:headId:OpenState :: forall tx. OpenState tx -> HeadId
headId :: HeadId
headId} = OpenState tx
openState

-- | Observe a decrement transaction. If the outputs match the ones of the
-- pending decommit tx, then we consider the decommit finalized, and remove the
-- decommit tx in flight.
--
-- Finally, if the client observing happens to be the leader, then a new ReqSn
-- is broadcasted.
--
-- __Transition__: 'OpenState' → 'OpenState'
onOpenChainDecrementTx ::
  IsTx tx =>
  OpenState tx ->
  -- | New open state version
  SnapshotVersion ->
  -- | Outputs removed by the decrement
  [TxOutType tx] ->
  Outcome tx
onOpenChainDecrementTx :: forall tx.
IsTx tx =>
OpenState tx -> SnapshotVersion -> [TxOutType tx] -> Outcome tx
onOpenChainDecrementTx OpenState tx
openState SnapshotVersion
newVersion [TxOutType tx]
distributedTxOuts =
  -- Spec: if outputs(txω) = 𝑈ω
  case Maybe tx
decommitTx of
    Maybe tx
Nothing -> LogicError tx -> Outcome tx
forall tx. LogicError tx -> Outcome tx
Error (LogicError tx -> Outcome tx) -> LogicError tx -> Outcome tx
forall a b. (a -> b) -> a -> b
$ Text -> LogicError tx
forall tx. Text -> LogicError tx
AssertionFailed Text
"decrement observed but no decommit pending"
    Just tx
tx
      | tx -> [TxOutType tx]
forall tx. IsTx tx => tx -> [TxOutType tx]
outputsOfTx tx
tx [TxOutType tx] -> [TxOutType tx] -> Bool
forall a. Eq a => a -> a -> Bool
== [TxOutType tx]
distributedTxOuts ->
          -- Spec: txω ← ⊥
          --       v  ← v
          StateChanged tx -> Outcome tx
forall tx. StateChanged tx -> Outcome tx
newState DecommitFinalized{SnapshotVersion
$sel:newVersion:HeadInitialized :: SnapshotVersion
newVersion :: SnapshotVersion
newVersion}
            Outcome tx -> Outcome tx -> Outcome tx
forall a. Semigroup a => a -> a -> a
<> Effect tx -> Outcome tx
forall tx. Effect tx -> Outcome tx
cause (ServerOutput tx -> Effect tx
forall tx. ServerOutput tx -> Effect tx
ClientEffect (ServerOutput tx -> Effect tx) -> ServerOutput tx -> Effect tx
forall a b. (a -> b) -> a -> b
$ ServerOutput.DecommitFinalized{HeadId
$sel:headId:PeerConnected :: HeadId
headId :: HeadId
headId, $sel:decommitTxId:PeerConnected :: TxIdType tx
decommitTxId = tx -> TxIdType tx
forall tx. IsTx tx => tx -> TxIdType tx
txId tx
tx})
      | Bool
otherwise -> LogicError tx -> Outcome tx
forall tx. LogicError tx -> Outcome tx
Error (LogicError tx -> Outcome tx) -> LogicError tx -> Outcome tx
forall a b. (a -> b) -> a -> b
$ Text -> LogicError tx
forall tx. Text -> LogicError tx
AssertionFailed Text
"decrement not matching pending decommit"
 where
  OpenState{CoordinatedHeadState tx
$sel:coordinatedHeadState:OpenState :: forall tx. OpenState tx -> CoordinatedHeadState tx
coordinatedHeadState :: CoordinatedHeadState tx
coordinatedHeadState, HeadId
$sel:headId:OpenState :: forall tx. OpenState tx -> HeadId
headId :: HeadId
headId} = OpenState tx
openState

  CoordinatedHeadState{Maybe tx
$sel:decommitTx:CoordinatedHeadState :: forall tx. CoordinatedHeadState tx -> Maybe tx
decommitTx :: Maybe tx
decommitTx} = CoordinatedHeadState tx
coordinatedHeadState

isLeader :: HeadParameters -> Party -> SnapshotNumber -> Bool
isLeader :: HeadParameters -> Party -> SnapshotNumber -> Bool
isLeader HeadParameters{[Party]
$sel:parties:HeadParameters :: HeadParameters -> [Party]
parties :: [Party]
parties} Party
p SnapshotNumber
sn =
  case Party
p Party -> [Party] -> Maybe Int
forall a. Eq a => a -> [a] -> Maybe Int
`elemIndex` [Party]
parties of
    Just Int
i -> ((SnapshotNumber -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral SnapshotNumber
sn Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) Int -> Int -> Int
forall a. Integral a => a -> a -> a
`mod` [Party] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Party]
parties) Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
i
    Maybe Int
_ -> Bool
False

-- ** Closing the Head

-- | Client request to close the head. This leads to a close transaction on
-- chain using the latest confirmed snaphshot of the 'OpenState'.
--
-- __Transition__: 'OpenState' → 'OpenState'
onOpenClientClose ::
  OpenState tx ->
  Outcome tx
onOpenClientClose :: forall tx. OpenState tx -> Outcome tx
onOpenClientClose OpenState tx
st =
  -- Spec: η ← combine(̅S.𝑈)
  --       ηω ← combine(outputs(̅S.txω))
  --       ξ ← ̅S.σ
  --       postTx (close, ̅S.v, ̅S.s, η, ηω,ξ)
  Effect tx -> Outcome tx
forall tx. Effect tx -> Outcome tx
cause
    OnChainEffect
      { $sel:postChainTx:ClientEffect :: PostChainTx tx
postChainTx =
          CloseTx
            { HeadId
$sel:headId:InitTx :: HeadId
headId :: HeadId
headId
            , $sel:headParameters:InitTx :: HeadParameters
headParameters = HeadParameters
parameters
            , $sel:openVersion:InitTx :: SnapshotVersion
openVersion = SnapshotVersion
version
            , $sel:closingSnapshot:InitTx :: ConfirmedSnapshot tx
closingSnapshot = ConfirmedSnapshot tx
confirmedSnapshot
            }
      }
 where
  CoordinatedHeadState{ConfirmedSnapshot tx
$sel:confirmedSnapshot:CoordinatedHeadState :: forall tx. CoordinatedHeadState tx -> ConfirmedSnapshot tx
confirmedSnapshot :: ConfirmedSnapshot tx
confirmedSnapshot, SnapshotVersion
$sel:version:CoordinatedHeadState :: forall tx. CoordinatedHeadState tx -> SnapshotVersion
version :: SnapshotVersion
version} = CoordinatedHeadState tx
coordinatedHeadState

  OpenState{CoordinatedHeadState tx
$sel:coordinatedHeadState:OpenState :: forall tx. OpenState tx -> CoordinatedHeadState tx
coordinatedHeadState :: CoordinatedHeadState tx
coordinatedHeadState, HeadId
$sel:headId:OpenState :: forall tx. OpenState tx -> HeadId
headId :: HeadId
headId, HeadParameters
$sel:parameters:OpenState :: forall tx. OpenState tx -> HeadParameters
parameters :: HeadParameters
parameters} = OpenState tx
st

-- | Observe a close transaction. If the closed snapshot number is smaller than
-- our last confirmed, we post a contest transaction. Also, we do schedule a
-- notification for clients to fanout at the deadline.
--
-- __Transition__: 'OpenState' → 'ClosedState'
onOpenChainCloseTx ::
  OpenState tx ->
  -- | New chain state.
  ChainStateType tx ->
  -- | Closed snapshot number.
  SnapshotNumber ->
  -- | Contestation deadline.
  UTCTime ->
  Outcome tx
onOpenChainCloseTx :: forall tx.
OpenState tx
-> ChainStateType tx -> SnapshotNumber -> UTCTime -> Outcome tx
onOpenChainCloseTx OpenState tx
openState ChainStateType tx
newChainState SnapshotNumber
closedSnapshotNumber UTCTime
contestationDeadline =
  StateChanged tx -> Outcome tx
forall tx. StateChanged tx -> Outcome tx
newState HeadClosed{$sel:chainState:HeadInitialized :: ChainStateType tx
chainState = ChainStateType tx
newChainState, UTCTime
contestationDeadline :: UTCTime
$sel:contestationDeadline:HeadInitialized :: UTCTime
contestationDeadline}
    Outcome tx -> Outcome tx -> Outcome tx
forall a. Semigroup a => a -> a -> a
<> Effect tx -> Outcome tx
forall tx. Effect tx -> Outcome tx
cause Effect tx
notifyClient
    Outcome tx -> (Outcome tx -> Outcome tx) -> Outcome tx
forall a b. a -> (a -> b) -> b
& Outcome tx -> Outcome tx
maybePostContest
 where
  maybePostContest :: Outcome tx -> Outcome tx
maybePostContest Outcome tx
outcome =
    -- Spec: if ̅S.s > sc
    if Snapshot tx -> SnapshotNumber
forall tx. Snapshot tx -> SnapshotNumber
number (ConfirmedSnapshot tx -> Snapshot tx
forall tx. ConfirmedSnapshot tx -> Snapshot tx
getSnapshot ConfirmedSnapshot tx
confirmedSnapshot) SnapshotNumber -> SnapshotNumber -> Bool
forall a. Ord a => a -> a -> Bool
> SnapshotNumber
closedSnapshotNumber
      then
        Outcome tx
outcome
          -- XXX: As we use 'version' in the contest here, this is implies
          -- that our last 'confirmedSnapshot' must match version or
          -- version-1. Assert this fact?
          -- Spec: η ← combine(̅S.𝑈)
          --       ηω ← combine(outputs(̅S.txω))
          --       ξ ← ̅S.σ
          --       postTx (contest, ̅S.v, ̅S.s, η, ηω, ξ)
          Outcome tx -> Outcome tx -> Outcome tx
forall a. Semigroup a => a -> a -> a
<> Effect tx -> Outcome tx
forall tx. Effect tx -> Outcome tx
cause
            OnChainEffect
              { $sel:postChainTx:ClientEffect :: PostChainTx tx
postChainTx =
                  ContestTx
                    { HeadId
$sel:headId:InitTx :: HeadId
headId :: HeadId
headId
                    , HeadParameters
$sel:headParameters:InitTx :: HeadParameters
headParameters :: HeadParameters
headParameters
                    , $sel:openVersion:InitTx :: SnapshotVersion
openVersion = SnapshotVersion
version
                    , $sel:contestingSnapshot:InitTx :: ConfirmedSnapshot tx
contestingSnapshot = ConfirmedSnapshot tx
confirmedSnapshot
                    }
              }
      else Outcome tx
outcome

  notifyClient :: Effect tx
notifyClient =
    ServerOutput tx -> Effect tx
forall tx. ServerOutput tx -> Effect tx
ClientEffect (ServerOutput tx -> Effect tx) -> ServerOutput tx -> Effect tx
forall a b. (a -> b) -> a -> b
$
      ServerOutput.HeadIsClosed
        { HeadId
$sel:headId:PeerConnected :: HeadId
headId :: HeadId
headId
        , $sel:snapshotNumber:PeerConnected :: SnapshotNumber
snapshotNumber = SnapshotNumber
closedSnapshotNumber
        , UTCTime
contestationDeadline :: UTCTime
$sel:contestationDeadline:PeerConnected :: UTCTime
contestationDeadline
        }

  CoordinatedHeadState{ConfirmedSnapshot tx
$sel:confirmedSnapshot:CoordinatedHeadState :: forall tx. CoordinatedHeadState tx -> ConfirmedSnapshot tx
confirmedSnapshot :: ConfirmedSnapshot tx
confirmedSnapshot, SnapshotVersion
$sel:version:CoordinatedHeadState :: forall tx. CoordinatedHeadState tx -> SnapshotVersion
version :: SnapshotVersion
version} = CoordinatedHeadState tx
coordinatedHeadState

  OpenState{$sel:parameters:OpenState :: forall tx. OpenState tx -> HeadParameters
parameters = HeadParameters
headParameters, HeadId
$sel:headId:OpenState :: forall tx. OpenState tx -> HeadId
headId :: HeadId
headId, CoordinatedHeadState tx
$sel:coordinatedHeadState:OpenState :: forall tx. OpenState tx -> CoordinatedHeadState tx
coordinatedHeadState :: CoordinatedHeadState tx
coordinatedHeadState} = OpenState tx
openState

-- | Observe a contest transaction. If the contested snapshot number is smaller
-- than our last confirmed snapshot, we post a contest transaction.
--
-- __Transition__: 'ClosedState' → 'ClosedState'
onClosedChainContestTx ::
  ClosedState tx ->
  -- | New chain state.
  ChainStateType tx ->
  SnapshotNumber ->
  -- | Contestation deadline.
  UTCTime ->
  Outcome tx
onClosedChainContestTx :: forall tx.
ClosedState tx
-> ChainStateType tx -> SnapshotNumber -> UTCTime -> Outcome tx
onClosedChainContestTx ClosedState tx
closedState ChainStateType tx
newChainState SnapshotNumber
snapshotNumber UTCTime
contestationDeadline =
  StateChanged tx -> Outcome tx
forall tx. StateChanged tx -> Outcome tx
newState HeadContested{$sel:chainState:HeadInitialized :: ChainStateType tx
chainState = ChainStateType tx
newChainState, UTCTime
$sel:contestationDeadline:HeadInitialized :: UTCTime
contestationDeadline :: UTCTime
contestationDeadline}
    Outcome tx -> Outcome tx -> Outcome tx
forall a. Semigroup a => a -> a -> a
<> if
      | -- Spec: if ̅S.s > sc
        Snapshot tx -> SnapshotNumber
forall tx. Snapshot tx -> SnapshotNumber
number (ConfirmedSnapshot tx -> Snapshot tx
forall tx. ConfirmedSnapshot tx -> Snapshot tx
getSnapshot ConfirmedSnapshot tx
confirmedSnapshot) SnapshotNumber -> SnapshotNumber -> Bool
forall a. Ord a => a -> a -> Bool
> SnapshotNumber
snapshotNumber ->
          Effect tx -> Outcome tx
forall tx. Effect tx -> Outcome tx
cause Effect tx
notifyClients
            -- XXX: As we use 'version' in the contest here, this is implies
            -- that our last 'confirmedSnapshot' must match version or
            -- version-1. Assert this fact?
            -- Spec: η ← combine(̅S.𝑈)
            --       ηω ← combine(outputs(̅S.txω))
            --       ξ ← ̅S.σ
            --       postTx (contest, ̅S.v, ̅S.s, η, ηω, ξ)
            Outcome tx -> Outcome tx -> Outcome tx
forall a. Semigroup a => a -> a -> a
<> Effect tx -> Outcome tx
forall tx. Effect tx -> Outcome tx
cause
              OnChainEffect
                { $sel:postChainTx:ClientEffect :: PostChainTx tx
postChainTx =
                    ContestTx
                      { HeadId
$sel:headId:InitTx :: HeadId
headId :: HeadId
headId
                      , HeadParameters
$sel:headParameters:InitTx :: HeadParameters
headParameters :: HeadParameters
headParameters
                      , $sel:openVersion:InitTx :: SnapshotVersion
openVersion = SnapshotVersion
version
                      , $sel:contestingSnapshot:InitTx :: ConfirmedSnapshot tx
contestingSnapshot = ConfirmedSnapshot tx
confirmedSnapshot
                      }
                }
      | SnapshotNumber
snapshotNumber SnapshotNumber -> SnapshotNumber -> Bool
forall a. Ord a => a -> a -> Bool
> Snapshot tx -> SnapshotNumber
forall tx. Snapshot tx -> SnapshotNumber
number (ConfirmedSnapshot tx -> Snapshot tx
forall tx. ConfirmedSnapshot tx -> Snapshot tx
getSnapshot ConfirmedSnapshot tx
confirmedSnapshot) ->
          -- TODO: A more recent snapshot number was succesfully contested, we will
          -- not be able to fanout! We might want to communicate that to the client!
          Effect tx -> Outcome tx
forall tx. Effect tx -> Outcome tx
cause Effect tx
notifyClients
      | Bool
otherwise ->
          Effect tx -> Outcome tx
forall tx. Effect tx -> Outcome tx
cause Effect tx
notifyClients
 where
  notifyClients :: Effect tx
notifyClients =
    ServerOutput tx -> Effect tx
forall tx. ServerOutput tx -> Effect tx
ClientEffect
      ServerOutput.HeadIsContested
        { SnapshotNumber
$sel:snapshotNumber:PeerConnected :: SnapshotNumber
snapshotNumber :: SnapshotNumber
snapshotNumber
        , HeadId
$sel:headId:PeerConnected :: HeadId
headId :: HeadId
headId
        , UTCTime
$sel:contestationDeadline:PeerConnected :: UTCTime
contestationDeadline :: UTCTime
contestationDeadline
        }

  ClosedState{$sel:parameters:ClosedState :: forall tx. ClosedState tx -> HeadParameters
parameters = HeadParameters
headParameters, ConfirmedSnapshot tx
confirmedSnapshot :: ConfirmedSnapshot tx
$sel:confirmedSnapshot:ClosedState :: forall tx. ClosedState tx -> ConfirmedSnapshot tx
confirmedSnapshot, HeadId
headId :: HeadId
$sel:headId:ClosedState :: forall tx. ClosedState tx -> HeadId
headId, SnapshotVersion
version :: SnapshotVersion
$sel:version:ClosedState :: forall tx. ClosedState tx -> SnapshotVersion
version} = ClosedState tx
closedState

-- | Client request to fanout leads to a fanout transaction on chain using the
-- latest confirmed snapshot from 'ClosedState'.
--
-- __Transition__: 'ClosedState' → 'ClosedState'
onClosedClientFanout ::
  Monoid (UTxOType tx) =>
  ClosedState tx ->
  Outcome tx
onClosedClientFanout :: forall tx. Monoid (UTxOType tx) => ClosedState tx -> Outcome tx
onClosedClientFanout ClosedState tx
closedState =
  Effect tx -> Outcome tx
forall tx. Effect tx -> Outcome tx
cause
    OnChainEffect
      { $sel:postChainTx:ClientEffect :: PostChainTx tx
postChainTx =
          FanoutTx
            { UTxOType tx
$sel:utxo:InitTx :: UTxOType tx
utxo :: UTxOType tx
utxo
            , $sel:utxoToDecommit:InitTx :: Maybe (UTxOType tx)
utxoToDecommit =
                if SnapshotVersion -> Integer
forall a. Integral a => a -> Integer
toInteger SnapshotVersion
snapshotVersion Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer -> Integer -> Integer
forall a. Ord a => a -> a -> a
max (SnapshotVersion -> Integer
forall a. Integral a => a -> Integer
toInteger SnapshotVersion
version Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
1) Integer
0
                  then Maybe (UTxOType tx)
forall a. Monoid a => a
mempty
                  else Maybe (UTxOType tx)
utxoToDecommit
            , HeadSeed
$sel:headSeed:InitTx :: HeadSeed
headSeed :: HeadSeed
headSeed
            , UTCTime
contestationDeadline :: UTCTime
$sel:contestationDeadline:InitTx :: UTCTime
contestationDeadline
            }
      }
 where
  Snapshot{UTxOType tx
$sel:utxo:Snapshot :: forall tx. Snapshot tx -> UTxOType tx
utxo :: UTxOType tx
utxo, Maybe (UTxOType tx)
$sel:utxoToDecommit:Snapshot :: forall tx. Snapshot tx -> Maybe (UTxOType tx)
utxoToDecommit :: Maybe (UTxOType tx)
utxoToDecommit, $sel:version:Snapshot :: forall tx. Snapshot tx -> SnapshotVersion
version = SnapshotVersion
snapshotVersion} = ConfirmedSnapshot tx -> Snapshot tx
forall tx. ConfirmedSnapshot tx -> Snapshot tx
getSnapshot ConfirmedSnapshot tx
confirmedSnapshot

  ClosedState{HeadSeed
headSeed :: HeadSeed
$sel:headSeed:ClosedState :: forall tx. ClosedState tx -> HeadSeed
headSeed, ConfirmedSnapshot tx
$sel:confirmedSnapshot:ClosedState :: forall tx. ClosedState tx -> ConfirmedSnapshot tx
confirmedSnapshot :: ConfirmedSnapshot tx
confirmedSnapshot, UTCTime
contestationDeadline :: UTCTime
$sel:contestationDeadline:ClosedState :: forall tx. ClosedState tx -> UTCTime
contestationDeadline, SnapshotVersion
$sel:version:ClosedState :: forall tx. ClosedState tx -> SnapshotVersion
version :: SnapshotVersion
version} = ClosedState tx
closedState

-- | Observe a fanout transaction by finalize the head state and notifying
-- clients about it.
--
-- __Transition__: 'ClosedState' → 'IdleState'
onClosedChainFanoutTx ::
  ClosedState tx ->
  -- | New chain state
  ChainStateType tx ->
  Outcome tx
onClosedChainFanoutTx :: forall tx. ClosedState tx -> ChainStateType tx -> Outcome tx
onClosedChainFanoutTx ClosedState tx
closedState ChainStateType tx
newChainState =
  StateChanged tx -> Outcome tx
forall tx. StateChanged tx -> Outcome tx
newState HeadFannedOut{$sel:chainState:HeadInitialized :: ChainStateType tx
chainState = ChainStateType tx
newChainState}
    Outcome tx -> Outcome tx -> Outcome tx
forall a. Semigroup a => a -> a -> a
<> Effect tx -> Outcome tx
forall tx. Effect tx -> Outcome tx
cause (ServerOutput tx -> Effect tx
forall tx. ServerOutput tx -> Effect tx
ClientEffect (ServerOutput tx -> Effect tx) -> ServerOutput tx -> Effect tx
forall a b. (a -> b) -> a -> b
$ ServerOutput.HeadIsFinalized{HeadId
$sel:headId:PeerConnected :: HeadId
headId :: HeadId
headId, UTxOType tx
$sel:utxo:PeerConnected :: UTxOType tx
utxo :: UTxOType tx
utxo})
 where
  Snapshot{UTxOType tx
$sel:utxo:Snapshot :: forall tx. Snapshot tx -> UTxOType tx
utxo :: UTxOType tx
utxo} = ConfirmedSnapshot tx -> Snapshot tx
forall tx. ConfirmedSnapshot tx -> Snapshot tx
getSnapshot ConfirmedSnapshot tx
confirmedSnapshot

  ClosedState{ConfirmedSnapshot tx
$sel:confirmedSnapshot:ClosedState :: forall tx. ClosedState tx -> ConfirmedSnapshot tx
confirmedSnapshot :: ConfirmedSnapshot tx
confirmedSnapshot, HeadId
$sel:headId:ClosedState :: forall tx. ClosedState tx -> HeadId
headId :: HeadId
headId} = ClosedState tx
closedState

-- | Handles inputs and converts them into 'StateChanged' events along with
-- 'Effect's, in case it is processed succesfully. Later, the Node will
-- 'aggregate' the events, resulting in a new 'HeadState'.
update ::
  IsChainState tx =>
  Environment ->
  Ledger tx ->
  -- | Current HeadState to validate the command against.
  HeadState tx ->
  -- | Input to be processed.
  Input tx ->
  Outcome tx
update :: forall tx.
IsChainState tx =>
Environment -> Ledger tx -> HeadState tx -> Input tx -> Outcome tx
update Environment
env Ledger tx
ledger HeadState tx
st Input tx
ev = case (HeadState tx
st, Input tx
ev) of
  (HeadState tx
_, NetworkInput TTL
_ (ConnectivityEvent Connectivity
conn)) ->
    Connectivity -> Outcome tx
forall tx. Connectivity -> Outcome tx
onConnectionEvent Connectivity
conn
  (Idle IdleState tx
_, ClientInput ClientInput tx
Init) ->
    Environment -> Outcome tx
forall tx. Environment -> Outcome tx
onIdleClientInit Environment
env
  (Idle IdleState tx
_, ChainInput Observation{$sel:observedTx:Observation :: forall tx. ChainEvent tx -> OnChainTx tx
observedTx = OnInitTx{HeadId
headId :: HeadId
$sel:headId:OnInitTx :: forall tx. OnChainTx tx -> HeadId
headId, HeadSeed
headSeed :: HeadSeed
$sel:headSeed:OnInitTx :: forall tx. OnChainTx tx -> HeadSeed
headSeed, HeadParameters
headParameters :: HeadParameters
$sel:headParameters:OnInitTx :: forall tx. OnChainTx tx -> HeadParameters
headParameters, [OnChainId]
participants :: [OnChainId]
$sel:participants:OnInitTx :: forall tx. OnChainTx tx -> [OnChainId]
participants}, ChainStateType tx
newChainState :: ChainStateType tx
$sel:newChainState:Observation :: forall tx. ChainEvent tx -> ChainStateType tx
newChainState}) ->
    Environment
-> ChainStateType tx
-> HeadId
-> HeadSeed
-> HeadParameters
-> [OnChainId]
-> Outcome tx
forall tx.
Environment
-> ChainStateType tx
-> HeadId
-> HeadSeed
-> HeadParameters
-> [OnChainId]
-> Outcome tx
onIdleChainInitTx Environment
env ChainStateType tx
newChainState HeadId
headId HeadSeed
headSeed HeadParameters
headParameters [OnChainId]
participants
  (Initial initialState :: InitialState tx
initialState@InitialState{$sel:headId:InitialState :: forall tx. InitialState tx -> HeadId
headId = HeadId
ourHeadId}, ChainInput Observation{$sel:observedTx:Observation :: forall tx. ChainEvent tx -> OnChainTx tx
observedTx = OnCommitTx{HeadId
$sel:headId:OnInitTx :: forall tx. OnChainTx tx -> HeadId
headId :: HeadId
headId, $sel:party:OnInitTx :: forall tx. OnChainTx tx -> Party
party = Party
pt, $sel:committed:OnInitTx :: forall tx. OnChainTx tx -> UTxOType tx
committed = UTxOType tx
utxo}, ChainStateType tx
$sel:newChainState:Observation :: forall tx. ChainEvent tx -> ChainStateType tx
newChainState :: ChainStateType tx
newChainState})
    | HeadId
ourHeadId HeadId -> HeadId -> Bool
forall a. Eq a => a -> a -> Bool
== HeadId
headId -> InitialState tx
-> ChainStateType tx -> Party -> UTxOType tx -> Outcome tx
forall tx.
Monoid (UTxOType tx) =>
InitialState tx
-> ChainStateType tx -> Party -> UTxOType tx -> Outcome tx
onInitialChainCommitTx InitialState tx
initialState ChainStateType tx
newChainState Party
pt UTxOType tx
utxo
    | Bool
otherwise -> LogicError tx -> Outcome tx
forall tx. LogicError tx -> Outcome tx
Error NotOurHead{HeadId
ourHeadId :: HeadId
$sel:ourHeadId:UnhandledInput :: HeadId
ourHeadId, $sel:otherHeadId:UnhandledInput :: HeadId
otherHeadId = HeadId
headId}
  (Initial InitialState tx
initialState, ClientInput ClientInput tx
Abort) ->
    InitialState tx -> Outcome tx
forall tx. Monoid (UTxOType tx) => InitialState tx -> Outcome tx
onInitialClientAbort InitialState tx
initialState
  (Initial initialState :: InitialState tx
initialState@InitialState{$sel:headId:InitialState :: forall tx. InitialState tx -> HeadId
headId = HeadId
ourHeadId}, ChainInput Observation{$sel:observedTx:Observation :: forall tx. ChainEvent tx -> OnChainTx tx
observedTx = OnCollectComTx{HeadId
$sel:headId:OnInitTx :: forall tx. OnChainTx tx -> HeadId
headId :: HeadId
headId}, ChainStateType tx
$sel:newChainState:Observation :: forall tx. ChainEvent tx -> ChainStateType tx
newChainState :: ChainStateType tx
newChainState})
    | HeadId
ourHeadId HeadId -> HeadId -> Bool
forall a. Eq a => a -> a -> Bool
== HeadId
headId -> InitialState tx -> ChainStateType tx -> Outcome tx
forall tx.
IsChainState tx =>
InitialState tx -> ChainStateType tx -> Outcome tx
onInitialChainCollectTx InitialState tx
initialState ChainStateType tx
newChainState
    | Bool
otherwise -> LogicError tx -> Outcome tx
forall tx. LogicError tx -> Outcome tx
Error NotOurHead{HeadId
$sel:ourHeadId:UnhandledInput :: HeadId
ourHeadId :: HeadId
ourHeadId, $sel:otherHeadId:UnhandledInput :: HeadId
otherHeadId = HeadId
headId}
  (Initial InitialState{$sel:headId:InitialState :: forall tx. InitialState tx -> HeadId
headId = HeadId
ourHeadId, Committed tx
$sel:committed:InitialState :: forall tx. InitialState tx -> Committed tx
committed :: Committed tx
committed}, ChainInput Observation{$sel:observedTx:Observation :: forall tx. ChainEvent tx -> OnChainTx tx
observedTx = OnAbortTx{HeadId
$sel:headId:OnInitTx :: forall tx. OnChainTx tx -> HeadId
headId :: HeadId
headId}, ChainStateType tx
$sel:newChainState:Observation :: forall tx. ChainEvent tx -> ChainStateType tx
newChainState :: ChainStateType tx
newChainState})
    | HeadId
ourHeadId HeadId -> HeadId -> Bool
forall a. Eq a => a -> a -> Bool
== HeadId
headId -> ChainStateType tx -> Committed tx -> HeadId -> Outcome tx
forall tx.
Monoid (UTxOType tx) =>
ChainStateType tx -> Committed tx -> HeadId -> Outcome tx
onInitialChainAbortTx ChainStateType tx
newChainState Committed tx
committed HeadId
headId
    | Bool
otherwise -> LogicError tx -> Outcome tx
forall tx. LogicError tx -> Outcome tx
Error NotOurHead{HeadId
$sel:ourHeadId:UnhandledInput :: HeadId
ourHeadId :: HeadId
ourHeadId, $sel:otherHeadId:UnhandledInput :: HeadId
otherHeadId = HeadId
headId}
  (Initial InitialState{Committed tx
$sel:committed:InitialState :: forall tx. InitialState tx -> Committed tx
committed :: Committed tx
committed, HeadId
$sel:headId:InitialState :: forall tx. InitialState tx -> HeadId
headId :: HeadId
headId}, ClientInput ClientInput tx
GetUTxO) ->
    Effect tx -> Outcome tx
forall tx. Effect tx -> Outcome tx
cause (ServerOutput tx -> Effect tx
forall tx. ServerOutput tx -> Effect tx
ClientEffect (ServerOutput tx -> Effect tx)
-> (UTxOType tx -> ServerOutput tx) -> UTxOType tx -> Effect tx
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HeadId -> UTxOType tx -> ServerOutput tx
forall tx. HeadId -> UTxOType tx -> ServerOutput tx
ServerOutput.GetUTxOResponse HeadId
headId (UTxOType tx -> Effect tx) -> UTxOType tx -> Effect tx
forall a b. (a -> b) -> a -> b
$ Committed tx -> UTxOType tx
forall m. Monoid m => Map Party m -> m
forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m
fold Committed tx
committed)
  -- Open
  (Open OpenState tx
openState, ClientInput ClientInput tx
Close) ->
    OpenState tx -> Outcome tx
forall tx. OpenState tx -> Outcome tx
onOpenClientClose OpenState tx
openState
  (Open{}, ClientInput (NewTx tx
tx)) ->
    tx -> Outcome tx
forall tx. tx -> Outcome tx
onOpenClientNewTx tx
tx
  (Open OpenState tx
openState, NetworkInput TTL
ttl (ReceivedMessage{$sel:msg:ConnectivityEvent :: forall msg. NetworkEvent msg -> msg
msg = ReqTx tx
tx})) ->
    Environment -> Ledger tx -> OpenState tx -> TTL -> tx -> Outcome tx
forall tx.
IsTx tx =>
Environment -> Ledger tx -> OpenState tx -> TTL -> tx -> Outcome tx
onOpenNetworkReqTx Environment
env Ledger tx
ledger OpenState tx
openState TTL
ttl tx
tx
  (Open OpenState tx
openState, NetworkInput TTL
_ (ReceivedMessage{Party
sender :: Party
$sel:sender:ConnectivityEvent :: forall msg. NetworkEvent msg -> Party
sender, $sel:msg:ConnectivityEvent :: forall msg. NetworkEvent msg -> msg
msg = ReqSn SnapshotVersion
sv SnapshotNumber
sn [TxIdType tx]
txIds Maybe tx
decommitTx Maybe (UTxOType tx)
incrementUTxO})) ->
    Environment
-> Ledger tx
-> OpenState tx
-> Party
-> SnapshotVersion
-> SnapshotNumber
-> [TxIdType tx]
-> Maybe tx
-> Maybe (UTxOType tx)
-> Outcome tx
forall tx.
IsTx tx =>
Environment
-> Ledger tx
-> OpenState tx
-> Party
-> SnapshotVersion
-> SnapshotNumber
-> [TxIdType tx]
-> Maybe tx
-> Maybe (UTxOType tx)
-> Outcome tx
onOpenNetworkReqSn Environment
env Ledger tx
ledger OpenState tx
openState Party
sender SnapshotVersion
sv SnapshotNumber
sn [TxIdType tx]
txIds Maybe tx
decommitTx Maybe (UTxOType tx)
incrementUTxO
  (Open OpenState tx
openState, NetworkInput TTL
_ (ReceivedMessage{Party
$sel:sender:ConnectivityEvent :: forall msg. NetworkEvent msg -> Party
sender :: Party
sender, $sel:msg:ConnectivityEvent :: forall msg. NetworkEvent msg -> msg
msg = AckSn Signature (Snapshot tx)
snapshotSignature SnapshotNumber
sn})) ->
    Environment
-> OpenState tx
-> Party
-> Signature (Snapshot tx)
-> SnapshotNumber
-> Outcome tx
forall tx.
IsTx tx =>
Environment
-> OpenState tx
-> Party
-> Signature (Snapshot tx)
-> SnapshotNumber
-> Outcome tx
onOpenNetworkAckSn Environment
env OpenState tx
openState Party
sender Signature (Snapshot tx)
snapshotSignature SnapshotNumber
sn
  ( Open openState :: OpenState tx
openState@OpenState{$sel:headId:OpenState :: forall tx. OpenState tx -> HeadId
headId = HeadId
ourHeadId}
    , ChainInput Observation{$sel:observedTx:Observation :: forall tx. ChainEvent tx -> OnChainTx tx
observedTx = OnCloseTx{HeadId
$sel:headId:OnInitTx :: forall tx. OnChainTx tx -> HeadId
headId :: HeadId
headId, $sel:snapshotNumber:OnInitTx :: forall tx. OnChainTx tx -> SnapshotNumber
snapshotNumber = SnapshotNumber
closedSnapshotNumber, UTCTime
contestationDeadline :: UTCTime
$sel:contestationDeadline:OnInitTx :: forall tx. OnChainTx tx -> UTCTime
contestationDeadline}, ChainStateType tx
$sel:newChainState:Observation :: forall tx. ChainEvent tx -> ChainStateType tx
newChainState :: ChainStateType tx
newChainState}
    )
      | HeadId
ourHeadId HeadId -> HeadId -> Bool
forall a. Eq a => a -> a -> Bool
== HeadId
headId ->
          OpenState tx
-> ChainStateType tx -> SnapshotNumber -> UTCTime -> Outcome tx
forall tx.
OpenState tx
-> ChainStateType tx -> SnapshotNumber -> UTCTime -> Outcome tx
onOpenChainCloseTx OpenState tx
openState ChainStateType tx
newChainState SnapshotNumber
closedSnapshotNumber UTCTime
contestationDeadline
      | Bool
otherwise ->
          LogicError tx -> Outcome tx
forall tx. LogicError tx -> Outcome tx
Error NotOurHead{HeadId
$sel:ourHeadId:UnhandledInput :: HeadId
ourHeadId :: HeadId
ourHeadId, $sel:otherHeadId:UnhandledInput :: HeadId
otherHeadId = HeadId
headId}
  (Open OpenState{$sel:coordinatedHeadState:OpenState :: forall tx. OpenState tx -> CoordinatedHeadState tx
coordinatedHeadState = CoordinatedHeadState{ConfirmedSnapshot tx
$sel:confirmedSnapshot:CoordinatedHeadState :: forall tx. CoordinatedHeadState tx -> ConfirmedSnapshot tx
confirmedSnapshot :: ConfirmedSnapshot tx
confirmedSnapshot}, HeadId
$sel:headId:OpenState :: forall tx. OpenState tx -> HeadId
headId :: HeadId
headId}, ClientInput ClientInput tx
GetUTxO) ->
    -- TODO: Is it really intuitive that we respond from the confirmed ledger if
    -- transactions are validated against the seen ledger?
    Effect tx -> Outcome tx
forall tx. Effect tx -> Outcome tx
cause (ServerOutput tx -> Effect tx
forall tx. ServerOutput tx -> Effect tx
ClientEffect (ServerOutput tx -> Effect tx)
-> (UTxOType tx -> ServerOutput tx) -> UTxOType tx -> Effect tx
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HeadId -> UTxOType tx -> ServerOutput tx
forall tx. HeadId -> UTxOType tx -> ServerOutput tx
ServerOutput.GetUTxOResponse HeadId
headId (UTxOType tx -> Effect tx) -> UTxOType tx -> Effect tx
forall a b. (a -> b) -> a -> b
$ forall {k} (x :: k) r a. HasField x r a => r -> a
forall (x :: Symbol) r a. HasField x r a => r -> a
getField @"utxo" (Snapshot tx -> UTxOType tx) -> Snapshot tx -> UTxOType tx
forall a b. (a -> b) -> a -> b
$ ConfirmedSnapshot tx -> Snapshot tx
forall tx. ConfirmedSnapshot tx -> Snapshot tx
getSnapshot ConfirmedSnapshot tx
confirmedSnapshot)
  -- NOTE: If posting the collectCom transaction failed in the open state, then
  -- another party likely opened the head before us and it's okay to ignore.
  (Open{}, ChainInput PostTxError{$sel:postChainTx:Observation :: forall tx. ChainEvent tx -> PostChainTx tx
postChainTx = CollectComTx{}}) ->
    Outcome tx
forall tx. Outcome tx
noop
  (Open OpenState{HeadId
$sel:headId:OpenState :: forall tx. OpenState tx -> HeadId
headId :: HeadId
headId, CoordinatedHeadState tx
$sel:coordinatedHeadState:OpenState :: forall tx. OpenState tx -> CoordinatedHeadState tx
coordinatedHeadState :: CoordinatedHeadState tx
coordinatedHeadState, ChainSlot
$sel:currentSlot:OpenState :: forall tx. OpenState tx -> ChainSlot
currentSlot :: ChainSlot
currentSlot}, ClientInput Recover{TxIdType tx
recoverTxId :: TxIdType tx
$sel:recoverTxId:Init :: forall tx. ClientInput tx -> TxIdType tx
recoverTxId}) -> do
    HeadId
-> ChainSlot
-> CoordinatedHeadState tx
-> TxIdType tx
-> Outcome tx
forall tx.
IsTx tx =>
HeadId
-> ChainSlot
-> CoordinatedHeadState tx
-> TxIdType tx
-> Outcome tx
onOpenClientRecover HeadId
headId ChainSlot
currentSlot CoordinatedHeadState tx
coordinatedHeadState TxIdType tx
recoverTxId
  (Open OpenState{HeadId
$sel:headId:OpenState :: forall tx. OpenState tx -> HeadId
headId :: HeadId
headId, CoordinatedHeadState tx
$sel:coordinatedHeadState:OpenState :: forall tx. OpenState tx -> CoordinatedHeadState tx
coordinatedHeadState :: CoordinatedHeadState tx
coordinatedHeadState, ChainSlot
$sel:currentSlot:OpenState :: forall tx. OpenState tx -> ChainSlot
currentSlot :: ChainSlot
currentSlot}, ClientInput Decommit{tx
decommitTx :: tx
$sel:decommitTx:Init :: forall tx. ClientInput tx -> tx
decommitTx}) -> do
    HeadId
-> Ledger tx
-> ChainSlot
-> CoordinatedHeadState tx
-> tx
-> Outcome tx
forall tx.
IsTx tx =>
HeadId
-> Ledger tx
-> ChainSlot
-> CoordinatedHeadState tx
-> tx
-> Outcome tx
onOpenClientDecommit HeadId
headId Ledger tx
ledger ChainSlot
currentSlot CoordinatedHeadState tx
coordinatedHeadState tx
decommitTx
  (Open OpenState tx
openState, NetworkInput TTL
ttl (ReceivedMessage{$sel:msg:ConnectivityEvent :: forall msg. NetworkEvent msg -> msg
msg = ReqDec{tx
$sel:transaction:ReqTx :: forall tx. Message tx -> tx
transaction :: tx
transaction}})) ->
    Environment -> Ledger tx -> TTL -> OpenState tx -> tx -> Outcome tx
forall tx.
IsTx tx =>
Environment -> Ledger tx -> TTL -> OpenState tx -> tx -> Outcome tx
onOpenNetworkReqDec Environment
env Ledger tx
ledger TTL
ttl OpenState tx
openState tx
transaction
  (Open openState :: OpenState tx
openState@OpenState{$sel:headId:OpenState :: forall tx. OpenState tx -> HeadId
headId = HeadId
ourHeadId}, ChainInput Observation{$sel:observedTx:Observation :: forall tx. ChainEvent tx -> OnChainTx tx
observedTx = OnDepositTx{HeadId
$sel:headId:OnInitTx :: forall tx. OnChainTx tx -> HeadId
headId :: HeadId
headId, UTxOType tx
deposited :: UTxOType tx
$sel:deposited:OnInitTx :: forall tx. OnChainTx tx -> UTxOType tx
deposited, TxIdType tx
depositTxId :: TxIdType tx
$sel:depositTxId:OnInitTx :: forall tx. OnChainTx tx -> TxIdType tx
depositTxId, UTCTime
deadline :: UTCTime
$sel:deadline:OnInitTx :: forall tx. OnChainTx tx -> UTCTime
deadline}})
    | HeadId
ourHeadId HeadId -> HeadId -> Bool
forall a. Eq a => a -> a -> Bool
== HeadId
headId -> HeadId
-> Environment
-> OpenState tx
-> UTxOType tx
-> TxIdType tx
-> UTCTime
-> Outcome tx
forall tx.
IsTx tx =>
HeadId
-> Environment
-> OpenState tx
-> UTxOType tx
-> TxIdType tx
-> UTCTime
-> Outcome tx
onOpenChainDepositTx HeadId
headId Environment
env OpenState tx
openState UTxOType tx
deposited TxIdType tx
depositTxId UTCTime
deadline
    | Bool
otherwise ->
        LogicError tx -> Outcome tx
forall tx. LogicError tx -> Outcome tx
Error NotOurHead{HeadId
$sel:ourHeadId:UnhandledInput :: HeadId
ourHeadId :: HeadId
ourHeadId, $sel:otherHeadId:UnhandledInput :: HeadId
otherHeadId = HeadId
headId}
  (Open openState :: OpenState tx
openState@OpenState{$sel:headId:OpenState :: forall tx. OpenState tx -> HeadId
headId = HeadId
ourHeadId}, ChainInput Observation{$sel:observedTx:Observation :: forall tx. ChainEvent tx -> OnChainTx tx
observedTx = OnRecoverTx{HeadId
$sel:headId:OnInitTx :: forall tx. OnChainTx tx -> HeadId
headId :: HeadId
headId, TxIdType tx
recoveredTxId :: TxIdType tx
$sel:recoveredTxId:OnInitTx :: forall tx. OnChainTx tx -> TxIdType tx
recoveredTxId}})
    | HeadId
ourHeadId HeadId -> HeadId -> Bool
forall a. Eq a => a -> a -> Bool
== HeadId
headId -> HeadId -> OpenState tx -> TxIdType tx -> Outcome tx
forall tx.
IsTx tx =>
HeadId -> OpenState tx -> TxIdType tx -> Outcome tx
onOpenChainRecoverTx HeadId
headId OpenState tx
openState TxIdType tx
recoveredTxId
    | Bool
otherwise ->
        LogicError tx -> Outcome tx
forall tx. LogicError tx -> Outcome tx
Error NotOurHead{HeadId
$sel:ourHeadId:UnhandledInput :: HeadId
ourHeadId :: HeadId
ourHeadId, $sel:otherHeadId:UnhandledInput :: HeadId
otherHeadId = HeadId
headId}
  (Open openState :: OpenState tx
openState@OpenState{$sel:headId:OpenState :: forall tx. OpenState tx -> HeadId
headId = HeadId
ourHeadId}, ChainInput Observation{$sel:observedTx:Observation :: forall tx. ChainEvent tx -> OnChainTx tx
observedTx = OnIncrementTx{HeadId
$sel:headId:OnInitTx :: forall tx. OnChainTx tx -> HeadId
headId :: HeadId
headId, SnapshotVersion
newVersion :: SnapshotVersion
$sel:newVersion:OnInitTx :: forall tx. OnChainTx tx -> SnapshotVersion
newVersion, TxIdType tx
$sel:depositTxId:OnInitTx :: forall tx. OnChainTx tx -> TxIdType tx
depositTxId :: TxIdType tx
depositTxId}})
    | HeadId
ourHeadId HeadId -> HeadId -> Bool
forall a. Eq a => a -> a -> Bool
== HeadId
headId ->
        OpenState tx -> SnapshotVersion -> TxIdType tx -> Outcome tx
forall tx.
OpenState tx -> SnapshotVersion -> TxIdType tx -> Outcome tx
onOpenChainIncrementTx OpenState tx
openState SnapshotVersion
newVersion TxIdType tx
depositTxId
    | Bool
otherwise ->
        LogicError tx -> Outcome tx
forall tx. LogicError tx -> Outcome tx
Error NotOurHead{HeadId
$sel:ourHeadId:UnhandledInput :: HeadId
ourHeadId :: HeadId
ourHeadId, $sel:otherHeadId:UnhandledInput :: HeadId
otherHeadId = HeadId
headId}
  (Open openState :: OpenState tx
openState@OpenState{$sel:headId:OpenState :: forall tx. OpenState tx -> HeadId
headId = HeadId
ourHeadId}, ChainInput Observation{$sel:observedTx:Observation :: forall tx. ChainEvent tx -> OnChainTx tx
observedTx = OnDecrementTx{HeadId
$sel:headId:OnInitTx :: forall tx. OnChainTx tx -> HeadId
headId :: HeadId
headId, SnapshotVersion
$sel:newVersion:OnInitTx :: forall tx. OnChainTx tx -> SnapshotVersion
newVersion :: SnapshotVersion
newVersion, [TxOutType tx]
distributedOutputs :: [TxOutType tx]
$sel:distributedOutputs:OnInitTx :: forall tx. OnChainTx tx -> [TxOutType tx]
distributedOutputs}})
    -- TODO: What happens if observed decrement tx get's rolled back?
    | HeadId
ourHeadId HeadId -> HeadId -> Bool
forall a. Eq a => a -> a -> Bool
== HeadId
headId ->
        OpenState tx -> SnapshotVersion -> [TxOutType tx] -> Outcome tx
forall tx.
IsTx tx =>
OpenState tx -> SnapshotVersion -> [TxOutType tx] -> Outcome tx
onOpenChainDecrementTx OpenState tx
openState SnapshotVersion
newVersion [TxOutType tx]
distributedOutputs
    | Bool
otherwise ->
        LogicError tx -> Outcome tx
forall tx. LogicError tx -> Outcome tx
Error NotOurHead{HeadId
$sel:ourHeadId:UnhandledInput :: HeadId
ourHeadId :: HeadId
ourHeadId, $sel:otherHeadId:UnhandledInput :: HeadId
otherHeadId = HeadId
headId}
  -- Closed
  (Closed closedState :: ClosedState tx
closedState@ClosedState{$sel:headId:ClosedState :: forall tx. ClosedState tx -> HeadId
headId = HeadId
ourHeadId}, ChainInput Observation{$sel:observedTx:Observation :: forall tx. ChainEvent tx -> OnChainTx tx
observedTx = OnContestTx{HeadId
$sel:headId:OnInitTx :: forall tx. OnChainTx tx -> HeadId
headId :: HeadId
headId, SnapshotNumber
$sel:snapshotNumber:OnInitTx :: forall tx. OnChainTx tx -> SnapshotNumber
snapshotNumber :: SnapshotNumber
snapshotNumber, UTCTime
$sel:contestationDeadline:OnInitTx :: forall tx. OnChainTx tx -> UTCTime
contestationDeadline :: UTCTime
contestationDeadline}, ChainStateType tx
$sel:newChainState:Observation :: forall tx. ChainEvent tx -> ChainStateType tx
newChainState :: ChainStateType tx
newChainState})
    | HeadId
ourHeadId HeadId -> HeadId -> Bool
forall a. Eq a => a -> a -> Bool
== HeadId
headId ->
        ClosedState tx
-> ChainStateType tx -> SnapshotNumber -> UTCTime -> Outcome tx
forall tx.
ClosedState tx
-> ChainStateType tx -> SnapshotNumber -> UTCTime -> Outcome tx
onClosedChainContestTx ClosedState tx
closedState ChainStateType tx
newChainState SnapshotNumber
snapshotNumber UTCTime
contestationDeadline
    | Bool
otherwise ->
        LogicError tx -> Outcome tx
forall tx. LogicError tx -> Outcome tx
Error NotOurHead{HeadId
$sel:ourHeadId:UnhandledInput :: HeadId
ourHeadId :: HeadId
ourHeadId, $sel:otherHeadId:UnhandledInput :: HeadId
otherHeadId = HeadId
headId}
  (Closed ClosedState{UTCTime
$sel:contestationDeadline:ClosedState :: forall tx. ClosedState tx -> UTCTime
contestationDeadline :: UTCTime
contestationDeadline, Bool
readyToFanoutSent :: Bool
$sel:readyToFanoutSent:ClosedState :: forall tx. ClosedState tx -> Bool
readyToFanoutSent, HeadId
$sel:headId:ClosedState :: forall tx. ClosedState tx -> HeadId
headId :: HeadId
headId}, ChainInput Tick{UTCTime
chainTime :: UTCTime
$sel:chainTime:Observation :: forall tx. ChainEvent tx -> UTCTime
chainTime})
    | UTCTime
chainTime UTCTime -> UTCTime -> Bool
forall a. Ord a => a -> a -> Bool
> UTCTime
contestationDeadline Bool -> Bool -> Bool
&& Bool -> Bool
not Bool
readyToFanoutSent ->
        StateChanged tx -> Outcome tx
forall tx. StateChanged tx -> Outcome tx
newState StateChanged tx
forall tx. StateChanged tx
HeadIsReadyToFanout
          Outcome tx -> Outcome tx -> Outcome tx
forall a. Semigroup a => a -> a -> a
<> Effect tx -> Outcome tx
forall tx. Effect tx -> Outcome tx
cause (ServerOutput tx -> Effect tx
forall tx. ServerOutput tx -> Effect tx
ClientEffect (ServerOutput tx -> Effect tx) -> ServerOutput tx -> Effect tx
forall a b. (a -> b) -> a -> b
$ HeadId -> ServerOutput tx
forall tx. HeadId -> ServerOutput tx
ServerOutput.ReadyToFanout HeadId
headId)
  (Closed ClosedState tx
closedState, ClientInput ClientInput tx
Fanout) ->
    ClosedState tx -> Outcome tx
forall tx. Monoid (UTxOType tx) => ClosedState tx -> Outcome tx
onClosedClientFanout ClosedState tx
closedState
  (Closed closedState :: ClosedState tx
closedState@ClosedState{$sel:headId:ClosedState :: forall tx. ClosedState tx -> HeadId
headId = HeadId
ourHeadId}, ChainInput Observation{$sel:observedTx:Observation :: forall tx. ChainEvent tx -> OnChainTx tx
observedTx = OnFanoutTx{HeadId
$sel:headId:OnInitTx :: forall tx. OnChainTx tx -> HeadId
headId :: HeadId
headId}, ChainStateType tx
$sel:newChainState:Observation :: forall tx. ChainEvent tx -> ChainStateType tx
newChainState :: ChainStateType tx
newChainState})
    | HeadId
ourHeadId HeadId -> HeadId -> Bool
forall a. Eq a => a -> a -> Bool
== HeadId
headId ->
        ClosedState tx -> ChainStateType tx -> Outcome tx
forall tx. ClosedState tx -> ChainStateType tx -> Outcome tx
onClosedChainFanoutTx ClosedState tx
closedState ChainStateType tx
newChainState
    | Bool
otherwise ->
        LogicError tx -> Outcome tx
forall tx. LogicError tx -> Outcome tx
Error NotOurHead{HeadId
$sel:ourHeadId:UnhandledInput :: HeadId
ourHeadId :: HeadId
ourHeadId, $sel:otherHeadId:UnhandledInput :: HeadId
otherHeadId = HeadId
headId}
  -- General
  (HeadState tx
_, ChainInput Rollback{ChainStateType tx
rolledBackChainState :: ChainStateType tx
$sel:rolledBackChainState:Observation :: forall tx. ChainEvent tx -> ChainStateType tx
rolledBackChainState}) ->
    StateChanged tx -> Outcome tx
forall tx. StateChanged tx -> Outcome tx
newState ChainRolledBack{$sel:chainState:HeadInitialized :: ChainStateType tx
chainState = ChainStateType tx
rolledBackChainState}
  (HeadState tx
_, ChainInput Tick{ChainSlot
chainSlot :: ChainSlot
$sel:chainSlot:Observation :: forall tx. ChainEvent tx -> ChainSlot
chainSlot}) ->
    StateChanged tx -> Outcome tx
forall tx. StateChanged tx -> Outcome tx
newState TickObserved{ChainSlot
chainSlot :: ChainSlot
$sel:chainSlot:HeadInitialized :: ChainSlot
chainSlot}
  (HeadState tx
_, ChainInput PostTxError{PostChainTx tx
$sel:postChainTx:Observation :: forall tx. ChainEvent tx -> PostChainTx tx
postChainTx :: PostChainTx tx
postChainTx, PostTxError tx
postTxError :: PostTxError tx
$sel:postTxError:Observation :: forall tx. ChainEvent tx -> PostTxError tx
postTxError}) ->
    Effect tx -> Outcome tx
forall tx. Effect tx -> Outcome tx
cause (Effect tx -> Outcome tx)
-> (ServerOutput tx -> Effect tx) -> ServerOutput tx -> Outcome tx
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ServerOutput tx -> Effect tx
forall tx. ServerOutput tx -> Effect tx
ClientEffect (ServerOutput tx -> Outcome tx) -> ServerOutput tx -> Outcome tx
forall a b. (a -> b) -> a -> b
$ ServerOutput.PostTxOnChainFailed{PostChainTx tx
postChainTx :: PostChainTx tx
$sel:postChainTx:PeerConnected :: PostChainTx tx
postChainTx, PostTxError tx
postTxError :: PostTxError tx
$sel:postTxError:PeerConnected :: PostTxError tx
postTxError}
  (HeadState tx
_, ClientInput{ClientInput tx
clientInput :: ClientInput tx
$sel:clientInput:ClientInput :: forall tx. Input tx -> ClientInput tx
clientInput}) ->
    Effect tx -> Outcome tx
forall tx. Effect tx -> Outcome tx
cause (Effect tx -> Outcome tx)
-> (ServerOutput tx -> Effect tx) -> ServerOutput tx -> Outcome tx
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ServerOutput tx -> Effect tx
forall tx. ServerOutput tx -> Effect tx
ClientEffect (ServerOutput tx -> Outcome tx) -> ServerOutput tx -> Outcome tx
forall a b. (a -> b) -> a -> b
$ ClientInput tx -> HeadState tx -> ServerOutput tx
forall tx. ClientInput tx -> HeadState tx -> ServerOutput tx
ServerOutput.CommandFailed ClientInput tx
clientInput HeadState tx
st
  (HeadState tx, Input tx)
_ ->
    LogicError tx -> Outcome tx
forall tx. LogicError tx -> Outcome tx
Error (LogicError tx -> Outcome tx) -> LogicError tx -> Outcome tx
forall a b. (a -> b) -> a -> b
$ Input tx -> HeadState tx -> LogicError tx
forall tx. Input tx -> HeadState tx -> LogicError tx
UnhandledInput Input tx
ev HeadState tx
st

-- * HeadState aggregate

-- | Reflect 'StateChanged' events onto the 'HeadState' aggregate.
aggregate :: IsChainState tx => HeadState tx -> StateChanged tx -> HeadState tx
aggregate :: forall tx.
IsChainState tx =>
HeadState tx -> StateChanged tx -> HeadState tx
aggregate HeadState tx
st = \case
  HeadInitialized{$sel:parameters:HeadInitialized :: forall tx. StateChanged tx -> HeadParameters
parameters = parameters :: HeadParameters
parameters@HeadParameters{[Party]
$sel:parties:HeadParameters :: HeadParameters -> [Party]
parties :: [Party]
parties}, HeadId
$sel:headId:HeadInitialized :: forall tx. StateChanged tx -> HeadId
headId :: HeadId
headId, HeadSeed
$sel:headSeed:HeadInitialized :: forall tx. StateChanged tx -> HeadSeed
headSeed :: HeadSeed
headSeed, ChainStateType tx
$sel:chainState:HeadInitialized :: forall tx. StateChanged tx -> ChainStateType tx
chainState :: ChainStateType tx
chainState} ->
    InitialState tx -> HeadState tx
forall tx. InitialState tx -> HeadState tx
Initial
      InitialState
        { $sel:parameters:InitialState :: HeadParameters
parameters = HeadParameters
parameters
        , $sel:pendingCommits:InitialState :: Set Party
pendingCommits = [Party] -> Set Party
forall a. Ord a => [a] -> Set a
Set.fromList [Party]
parties
        , $sel:committed:InitialState :: Map Party (UTxOType tx)
committed = Map Party (UTxOType tx)
forall a. Monoid a => a
mempty
        , ChainStateType tx
chainState :: ChainStateType tx
$sel:chainState:InitialState :: ChainStateType tx
chainState
        , HeadId
$sel:headId:InitialState :: HeadId
headId :: HeadId
headId
        , HeadSeed
$sel:headSeed:InitialState :: HeadSeed
headSeed :: HeadSeed
headSeed
        }
  CommittedUTxO{UTxOType tx
$sel:committedUTxO:HeadInitialized :: forall tx. StateChanged tx -> UTxOType tx
committedUTxO :: UTxOType tx
committedUTxO, ChainStateType tx
$sel:chainState:HeadInitialized :: forall tx. StateChanged tx -> ChainStateType tx
chainState :: ChainStateType tx
chainState, Party
$sel:party:HeadInitialized :: forall tx. StateChanged tx -> Party
party :: Party
party} ->
    case HeadState tx
st of
      Initial InitialState{HeadParameters
$sel:parameters:InitialState :: forall tx. InitialState tx -> HeadParameters
parameters :: HeadParameters
parameters, Set Party
$sel:pendingCommits:InitialState :: forall tx. InitialState tx -> Set Party
pendingCommits :: Set Party
pendingCommits, Map Party (UTxOType tx)
$sel:committed:InitialState :: forall tx. InitialState tx -> Committed tx
committed :: Map Party (UTxOType tx)
committed, HeadId
$sel:headId:InitialState :: forall tx. InitialState tx -> HeadId
headId :: HeadId
headId, HeadSeed
$sel:headSeed:InitialState :: forall tx. InitialState tx -> HeadSeed
headSeed :: HeadSeed
headSeed} ->
        InitialState tx -> HeadState tx
forall tx. InitialState tx -> HeadState tx
Initial
          InitialState
            { HeadParameters
$sel:parameters:InitialState :: HeadParameters
parameters :: HeadParameters
parameters
            , $sel:pendingCommits:InitialState :: Set Party
pendingCommits = Set Party
remainingParties
            , $sel:committed:InitialState :: Map Party (UTxOType tx)
committed = Map Party (UTxOType tx)
newCommitted
            , ChainStateType tx
$sel:chainState:InitialState :: ChainStateType tx
chainState :: ChainStateType tx
chainState
            , HeadId
$sel:headId:InitialState :: HeadId
headId :: HeadId
headId
            , HeadSeed
$sel:headSeed:InitialState :: HeadSeed
headSeed :: HeadSeed
headSeed
            }
       where
        newCommitted :: Map Party (UTxOType tx)
newCommitted = Party
-> UTxOType tx
-> Map Party (UTxOType tx)
-> Map Party (UTxOType tx)
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Party
party UTxOType tx
committedUTxO Map Party (UTxOType tx)
committed
        remainingParties :: Set Party
remainingParties = Party -> Set Party -> Set Party
forall a. Ord a => a -> Set a -> Set a
Set.delete Party
party Set Party
pendingCommits
      HeadState tx
_otherState -> HeadState tx
st
  TransactionReceived{tx
$sel:tx:HeadInitialized :: forall tx. StateChanged tx -> tx
tx :: tx
tx} ->
    case HeadState tx
st of
      Open os :: OpenState tx
os@OpenState{CoordinatedHeadState tx
$sel:coordinatedHeadState:OpenState :: forall tx. OpenState tx -> CoordinatedHeadState tx
coordinatedHeadState :: CoordinatedHeadState tx
coordinatedHeadState} ->
        OpenState tx -> HeadState tx
forall tx. OpenState tx -> HeadState tx
Open
          OpenState tx
os
            { coordinatedHeadState =
                coordinatedHeadState
                  { allTxs = allTxs <> fromList [(txId tx, tx)]
                  }
            }
       where
        CoordinatedHeadState{Map (TxIdType tx) tx
$sel:allTxs:CoordinatedHeadState :: forall tx. CoordinatedHeadState tx -> Map (TxIdType tx) tx
allTxs :: Map (TxIdType tx) tx
allTxs} = CoordinatedHeadState tx
coordinatedHeadState
      HeadState tx
_otherState -> HeadState tx
st
  TransactionAppliedToLocalUTxO{tx
$sel:tx:HeadInitialized :: forall tx. StateChanged tx -> tx
tx :: tx
tx, UTxOType tx
$sel:newLocalUTxO:HeadInitialized :: forall tx. StateChanged tx -> UTxOType tx
newLocalUTxO :: UTxOType tx
newLocalUTxO} ->
    case HeadState tx
st of
      Open os :: OpenState tx
os@OpenState{CoordinatedHeadState tx
$sel:coordinatedHeadState:OpenState :: forall tx. OpenState tx -> CoordinatedHeadState tx
coordinatedHeadState :: CoordinatedHeadState tx
coordinatedHeadState} ->
        OpenState tx -> HeadState tx
forall tx. OpenState tx -> HeadState tx
Open
          OpenState tx
os
            { coordinatedHeadState =
                coordinatedHeadState
                  { localUTxO = newLocalUTxO
                  , -- NOTE: Order of transactions is important here. See also
                    -- 'pruneTransactions'.
                    localTxs = localTxs <> [tx]
                  }
            }
       where
        CoordinatedHeadState{[tx]
$sel:localTxs:CoordinatedHeadState :: forall tx. CoordinatedHeadState tx -> [tx]
localTxs :: [tx]
localTxs} = CoordinatedHeadState tx
coordinatedHeadState
      HeadState tx
_otherState -> HeadState tx
st
  CommitRecorded{Map (TxIdType tx) (UTxOType tx)
pendingDeposits :: forall tx. StateChanged tx -> Map (TxIdType tx) (UTxOType tx)
pendingDeposits :: Map (TxIdType tx) (UTxOType tx)
pendingDeposits, UTxOType tx
$sel:newLocalUTxO:HeadInitialized :: forall tx. StateChanged tx -> UTxOType tx
newLocalUTxO :: UTxOType tx
newLocalUTxO} -> case HeadState tx
st of
    Open
      os :: OpenState tx
os@OpenState{CoordinatedHeadState tx
$sel:coordinatedHeadState:OpenState :: forall tx. OpenState tx -> CoordinatedHeadState tx
coordinatedHeadState :: CoordinatedHeadState tx
coordinatedHeadState} ->
        OpenState tx -> HeadState tx
forall tx. OpenState tx -> HeadState tx
Open
          OpenState tx
os
            { coordinatedHeadState =
                coordinatedHeadState
                  { localUTxO = newLocalUTxO
                  , pendingDeposits = pendingDeposits `Map.union` existingDeposits
                  }
            }
       where
        CoordinatedHeadState{$sel:pendingDeposits:CoordinatedHeadState :: forall tx.
CoordinatedHeadState tx -> Map (TxIdType tx) (UTxOType tx)
pendingDeposits = Map (TxIdType tx) (UTxOType tx)
existingDeposits} = CoordinatedHeadState tx
coordinatedHeadState
    HeadState tx
_otherState -> HeadState tx
st
  CommitRecovered{UTxOType tx
$sel:newLocalUTxO:HeadInitialized :: forall tx. StateChanged tx -> UTxOType tx
newLocalUTxO :: UTxOType tx
newLocalUTxO, TxIdType tx
$sel:recoveredTxId:HeadInitialized :: forall tx. StateChanged tx -> TxIdType tx
recoveredTxId :: TxIdType tx
recoveredTxId} -> case HeadState tx
st of
    Open
      os :: OpenState tx
os@OpenState{CoordinatedHeadState tx
$sel:coordinatedHeadState:OpenState :: forall tx. OpenState tx -> CoordinatedHeadState tx
coordinatedHeadState :: CoordinatedHeadState tx
coordinatedHeadState} ->
        OpenState tx -> HeadState tx
forall tx. OpenState tx -> HeadState tx
Open
          OpenState tx
os
            { coordinatedHeadState =
                coordinatedHeadState
                  { localUTxO = newLocalUTxO
                  , pendingDeposits = Map.delete recoveredTxId existingDeposits
                  }
            }
       where
        CoordinatedHeadState{$sel:pendingDeposits:CoordinatedHeadState :: forall tx.
CoordinatedHeadState tx -> Map (TxIdType tx) (UTxOType tx)
pendingDeposits = Map (TxIdType tx) (UTxOType tx)
existingDeposits} = CoordinatedHeadState tx
coordinatedHeadState
    HeadState tx
_otherState -> HeadState tx
st
  DecommitRecorded{tx
$sel:decommitTx:HeadInitialized :: forall tx. StateChanged tx -> tx
decommitTx :: tx
decommitTx, UTxOType tx
$sel:newLocalUTxO:HeadInitialized :: forall tx. StateChanged tx -> UTxOType tx
newLocalUTxO :: UTxOType tx
newLocalUTxO} -> case HeadState tx
st of
    Open
      os :: OpenState tx
os@OpenState{CoordinatedHeadState tx
$sel:coordinatedHeadState:OpenState :: forall tx. OpenState tx -> CoordinatedHeadState tx
coordinatedHeadState :: CoordinatedHeadState tx
coordinatedHeadState} ->
        OpenState tx -> HeadState tx
forall tx. OpenState tx -> HeadState tx
Open
          OpenState tx
os
            { coordinatedHeadState =
                coordinatedHeadState
                  { localUTxO = newLocalUTxO
                  , decommitTx = Just decommitTx
                  }
            }
    HeadState tx
_otherState -> HeadState tx
st
  SnapshotRequestDecided{SnapshotNumber
$sel:snapshotNumber:HeadInitialized :: forall tx. StateChanged tx -> SnapshotNumber
snapshotNumber :: SnapshotNumber
snapshotNumber} ->
    case HeadState tx
st of
      Open os :: OpenState tx
os@OpenState{CoordinatedHeadState tx
$sel:coordinatedHeadState:OpenState :: forall tx. OpenState tx -> CoordinatedHeadState tx
coordinatedHeadState :: CoordinatedHeadState tx
coordinatedHeadState} ->
        OpenState tx -> HeadState tx
forall tx. OpenState tx -> HeadState tx
Open
          OpenState tx
os
            { coordinatedHeadState =
                coordinatedHeadState
                  { seenSnapshot =
                      RequestedSnapshot
                        { lastSeen = seenSnapshotNumber seenSnapshot
                        , requested = snapshotNumber
                        }
                  }
            }
       where
        CoordinatedHeadState{SeenSnapshot tx
$sel:seenSnapshot:CoordinatedHeadState :: forall tx. CoordinatedHeadState tx -> SeenSnapshot tx
seenSnapshot :: SeenSnapshot tx
seenSnapshot} = CoordinatedHeadState tx
coordinatedHeadState
      HeadState tx
_otherState -> HeadState tx
st
  SnapshotRequested{Snapshot tx
$sel:snapshot:HeadInitialized :: forall tx. StateChanged tx -> Snapshot tx
snapshot :: Snapshot tx
snapshot, [TxIdType tx]
$sel:requestedTxIds:HeadInitialized :: forall tx. StateChanged tx -> [TxIdType tx]
requestedTxIds :: [TxIdType tx]
requestedTxIds, UTxOType tx
$sel:newLocalUTxO:HeadInitialized :: forall tx. StateChanged tx -> UTxOType tx
newLocalUTxO :: UTxOType tx
newLocalUTxO, [tx]
$sel:newLocalTxs:HeadInitialized :: forall tx. StateChanged tx -> [tx]
newLocalTxs :: [tx]
newLocalTxs} ->
    case HeadState tx
st of
      Open os :: OpenState tx
os@OpenState{CoordinatedHeadState tx
$sel:coordinatedHeadState:OpenState :: forall tx. OpenState tx -> CoordinatedHeadState tx
coordinatedHeadState :: CoordinatedHeadState tx
coordinatedHeadState} ->
        OpenState tx -> HeadState tx
forall tx. OpenState tx -> HeadState tx
Open
          OpenState tx
os
            { coordinatedHeadState =
                coordinatedHeadState
                  { seenSnapshot = SeenSnapshot snapshot mempty
                  , localTxs = newLocalTxs
                  , localUTxO = newLocalUTxO
                  , allTxs = foldr Map.delete allTxs requestedTxIds
                  }
            }
       where
        CoordinatedHeadState{Map (TxIdType tx) tx
$sel:allTxs:CoordinatedHeadState :: forall tx. CoordinatedHeadState tx -> Map (TxIdType tx) tx
allTxs :: Map (TxIdType tx) tx
allTxs} = CoordinatedHeadState tx
coordinatedHeadState
      HeadState tx
_otherState -> HeadState tx
st
  HeadAborted{ChainStateType tx
$sel:chainState:HeadInitialized :: forall tx. StateChanged tx -> ChainStateType tx
chainState :: ChainStateType tx
chainState} ->
    IdleState tx -> HeadState tx
forall tx. IdleState tx -> HeadState tx
Idle (IdleState tx -> HeadState tx) -> IdleState tx -> HeadState tx
forall a b. (a -> b) -> a -> b
$
      IdleState
        { ChainStateType tx
$sel:chainState:IdleState :: ChainStateType tx
chainState :: ChainStateType tx
chainState
        }
  HeadClosed{ChainStateType tx
$sel:chainState:HeadInitialized :: forall tx. StateChanged tx -> ChainStateType tx
chainState :: ChainStateType tx
chainState, UTCTime
$sel:contestationDeadline:HeadInitialized :: forall tx. StateChanged tx -> UTCTime
contestationDeadline :: UTCTime
contestationDeadline} ->
    case HeadState tx
st of
      Open
        OpenState
          { HeadParameters
$sel:parameters:OpenState :: forall tx. OpenState tx -> HeadParameters
parameters :: HeadParameters
parameters
          , $sel:coordinatedHeadState:OpenState :: forall tx. OpenState tx -> CoordinatedHeadState tx
coordinatedHeadState =
            CoordinatedHeadState
              { ConfirmedSnapshot tx
$sel:confirmedSnapshot:CoordinatedHeadState :: forall tx. CoordinatedHeadState tx -> ConfirmedSnapshot tx
confirmedSnapshot :: ConfirmedSnapshot tx
confirmedSnapshot
              , SnapshotVersion
$sel:version:CoordinatedHeadState :: forall tx. CoordinatedHeadState tx -> SnapshotVersion
version :: SnapshotVersion
version
              }
          , HeadId
$sel:headId:OpenState :: forall tx. OpenState tx -> HeadId
headId :: HeadId
headId
          , HeadSeed
headSeed :: HeadSeed
$sel:headSeed:OpenState :: forall tx. OpenState tx -> HeadSeed
headSeed
          } ->
          ClosedState tx -> HeadState tx
forall tx. ClosedState tx -> HeadState tx
Closed
            ClosedState
              { HeadParameters
$sel:parameters:ClosedState :: HeadParameters
parameters :: HeadParameters
parameters
              , ConfirmedSnapshot tx
$sel:confirmedSnapshot:ClosedState :: ConfirmedSnapshot tx
confirmedSnapshot :: ConfirmedSnapshot tx
confirmedSnapshot
              , UTCTime
$sel:contestationDeadline:ClosedState :: UTCTime
contestationDeadline :: UTCTime
contestationDeadline
              , $sel:readyToFanoutSent:ClosedState :: Bool
readyToFanoutSent = Bool
False
              , ChainStateType tx
chainState :: ChainStateType tx
$sel:chainState:ClosedState :: ChainStateType tx
chainState
              , HeadId
$sel:headId:ClosedState :: HeadId
headId :: HeadId
headId
              , HeadSeed
$sel:headSeed:ClosedState :: HeadSeed
headSeed :: HeadSeed
headSeed
              , SnapshotVersion
$sel:version:ClosedState :: SnapshotVersion
version :: SnapshotVersion
version
              }
      HeadState tx
_otherState -> HeadState tx
st
  HeadContested{ChainStateType tx
$sel:chainState:HeadInitialized :: forall tx. StateChanged tx -> ChainStateType tx
chainState :: ChainStateType tx
chainState, UTCTime
$sel:contestationDeadline:HeadInitialized :: forall tx. StateChanged tx -> UTCTime
contestationDeadline :: UTCTime
contestationDeadline} ->
    case HeadState tx
st of
      Closed ClosedState{HeadParameters
$sel:parameters:ClosedState :: forall tx. ClosedState tx -> HeadParameters
parameters :: HeadParameters
parameters, ConfirmedSnapshot tx
$sel:confirmedSnapshot:ClosedState :: forall tx. ClosedState tx -> ConfirmedSnapshot tx
confirmedSnapshot :: ConfirmedSnapshot tx
confirmedSnapshot, Bool
$sel:readyToFanoutSent:ClosedState :: forall tx. ClosedState tx -> Bool
readyToFanoutSent :: Bool
readyToFanoutSent, HeadId
$sel:headId:ClosedState :: forall tx. ClosedState tx -> HeadId
headId :: HeadId
headId, HeadSeed
$sel:headSeed:ClosedState :: forall tx. ClosedState tx -> HeadSeed
headSeed :: HeadSeed
headSeed, SnapshotVersion
$sel:version:ClosedState :: forall tx. ClosedState tx -> SnapshotVersion
version :: SnapshotVersion
version} ->
        ClosedState tx -> HeadState tx
forall tx. ClosedState tx -> HeadState tx
Closed
          ClosedState
            { HeadParameters
$sel:parameters:ClosedState :: HeadParameters
parameters :: HeadParameters
parameters
            , ConfirmedSnapshot tx
$sel:confirmedSnapshot:ClosedState :: ConfirmedSnapshot tx
confirmedSnapshot :: ConfirmedSnapshot tx
confirmedSnapshot
            , UTCTime
$sel:contestationDeadline:ClosedState :: UTCTime
contestationDeadline :: UTCTime
contestationDeadline
            , Bool
$sel:readyToFanoutSent:ClosedState :: Bool
readyToFanoutSent :: Bool
readyToFanoutSent
            , ChainStateType tx
$sel:chainState:ClosedState :: ChainStateType tx
chainState :: ChainStateType tx
chainState
            , HeadId
$sel:headId:ClosedState :: HeadId
headId :: HeadId
headId
            , HeadSeed
$sel:headSeed:ClosedState :: HeadSeed
headSeed :: HeadSeed
headSeed
            , SnapshotVersion
$sel:version:ClosedState :: SnapshotVersion
version :: SnapshotVersion
version
            }
      HeadState tx
_otherState -> HeadState tx
st
  HeadFannedOut{ChainStateType tx
$sel:chainState:HeadInitialized :: forall tx. StateChanged tx -> ChainStateType tx
chainState :: ChainStateType tx
chainState} ->
    case HeadState tx
st of
      Closed ClosedState tx
_ ->
        IdleState tx -> HeadState tx
forall tx. IdleState tx -> HeadState tx
Idle (IdleState tx -> HeadState tx) -> IdleState tx -> HeadState tx
forall a b. (a -> b) -> a -> b
$
          IdleState
            { ChainStateType tx
$sel:chainState:IdleState :: ChainStateType tx
chainState :: ChainStateType tx
chainState
            }
      HeadState tx
_otherState -> HeadState tx
st
  HeadOpened{ChainStateType tx
$sel:chainState:HeadInitialized :: forall tx. StateChanged tx -> ChainStateType tx
chainState :: ChainStateType tx
chainState, UTxOType tx
$sel:initialUTxO:HeadInitialized :: forall tx. StateChanged tx -> UTxOType tx
initialUTxO :: UTxOType tx
initialUTxO} ->
    case HeadState tx
st of
      Initial InitialState{HeadParameters
$sel:parameters:InitialState :: forall tx. InitialState tx -> HeadParameters
parameters :: HeadParameters
parameters, HeadId
$sel:headId:InitialState :: forall tx. InitialState tx -> HeadId
headId :: HeadId
headId, HeadSeed
$sel:headSeed:InitialState :: forall tx. InitialState tx -> HeadSeed
headSeed :: HeadSeed
headSeed} ->
        OpenState tx -> HeadState tx
forall tx. OpenState tx -> HeadState tx
Open
          OpenState
            { HeadParameters
$sel:parameters:OpenState :: HeadParameters
parameters :: HeadParameters
parameters
            , $sel:coordinatedHeadState:OpenState :: CoordinatedHeadState tx
coordinatedHeadState =
                CoordinatedHeadState
                  { $sel:localUTxO:CoordinatedHeadState :: UTxOType tx
localUTxO = UTxOType tx
initialUTxO
                  , $sel:allTxs:CoordinatedHeadState :: Map (TxIdType tx) tx
allTxs = Map (TxIdType tx) tx
forall a. Monoid a => a
mempty
                  , $sel:localTxs:CoordinatedHeadState :: [tx]
localTxs = [tx]
forall a. Monoid a => a
mempty
                  , $sel:confirmedSnapshot:CoordinatedHeadState :: ConfirmedSnapshot tx
confirmedSnapshot = InitialSnapshot{HeadId
headId :: HeadId
$sel:headId:InitialSnapshot :: HeadId
headId, UTxOType tx
$sel:initialUTxO:InitialSnapshot :: UTxOType tx
initialUTxO :: UTxOType tx
initialUTxO}
                  , $sel:seenSnapshot:CoordinatedHeadState :: SeenSnapshot tx
seenSnapshot = SeenSnapshot tx
forall tx. SeenSnapshot tx
NoSeenSnapshot
                  , $sel:pendingDeposits:CoordinatedHeadState :: Map (TxIdType tx) (UTxOType tx)
pendingDeposits = Map (TxIdType tx) (UTxOType tx)
forall a. Monoid a => a
mempty
                  , $sel:decommitTx:CoordinatedHeadState :: Maybe tx
decommitTx = Maybe tx
forall a. Maybe a
Nothing
                  , $sel:version:CoordinatedHeadState :: SnapshotVersion
version = SnapshotVersion
0
                  }
            , ChainStateType tx
chainState :: ChainStateType tx
$sel:chainState:OpenState :: ChainStateType tx
chainState
            , HeadId
$sel:headId:OpenState :: HeadId
headId :: HeadId
headId
            , HeadSeed
$sel:headSeed:OpenState :: HeadSeed
headSeed :: HeadSeed
headSeed
            , $sel:currentSlot:OpenState :: ChainSlot
currentSlot = ChainStateType tx -> ChainSlot
forall tx. IsChainState tx => ChainStateType tx -> ChainSlot
chainStateSlot ChainStateType tx
chainState
            }
      HeadState tx
_otherState -> HeadState tx
st
  SnapshotConfirmed{Snapshot tx
$sel:snapshot:HeadInitialized :: forall tx. StateChanged tx -> Snapshot tx
snapshot :: Snapshot tx
snapshot, MultiSignature (Snapshot tx)
$sel:signatures:HeadInitialized :: forall tx. StateChanged tx -> MultiSignature (Snapshot tx)
signatures :: MultiSignature (Snapshot tx)
signatures} ->
    case HeadState tx
st of
      Open os :: OpenState tx
os@OpenState{CoordinatedHeadState tx
$sel:coordinatedHeadState:OpenState :: forall tx. OpenState tx -> CoordinatedHeadState tx
coordinatedHeadState :: CoordinatedHeadState tx
coordinatedHeadState} ->
        OpenState tx -> HeadState tx
forall tx. OpenState tx -> HeadState tx
Open
          OpenState tx
os
            { coordinatedHeadState =
                coordinatedHeadState
                  { confirmedSnapshot =
                      ConfirmedSnapshot
                        { snapshot
                        , signatures
                        }
                  , seenSnapshot = LastSeenSnapshot number
                  }
            }
       where
        Snapshot{SnapshotNumber
$sel:number:Snapshot :: forall tx. Snapshot tx -> SnapshotNumber
number :: SnapshotNumber
number} = Snapshot tx
snapshot
      HeadState tx
_otherState -> HeadState tx
st
  PartySignedSnapshot{Party
$sel:party:HeadInitialized :: forall tx. StateChanged tx -> Party
party :: Party
party, Signature (Snapshot tx)
$sel:signature:HeadInitialized :: forall tx. StateChanged tx -> Signature (Snapshot tx)
signature :: Signature (Snapshot tx)
signature} ->
    case HeadState tx
st of
      Open
        os :: OpenState tx
os@OpenState
          { $sel:coordinatedHeadState:OpenState :: forall tx. OpenState tx -> CoordinatedHeadState tx
coordinatedHeadState =
            chs :: CoordinatedHeadState tx
chs@CoordinatedHeadState
              { $sel:seenSnapshot:CoordinatedHeadState :: forall tx. CoordinatedHeadState tx -> SeenSnapshot tx
seenSnapshot = ss :: SeenSnapshot tx
ss@SeenSnapshot{Map Party (Signature (Snapshot tx))
signatories :: Map Party (Signature (Snapshot tx))
$sel:signatories:NoSeenSnapshot :: forall tx. SeenSnapshot tx -> Map Party (Signature (Snapshot tx))
signatories}
              }
          } ->
          OpenState tx -> HeadState tx
forall tx. OpenState tx -> HeadState tx
Open
            OpenState tx
os
              { coordinatedHeadState =
                  chs
                    { seenSnapshot =
                        ss
                          { signatories = Map.insert party signature signatories
                          }
                    }
              }
      HeadState tx
_otherState -> HeadState tx
st
  CommitFinalized{SnapshotVersion
$sel:newVersion:HeadInitialized :: forall tx. StateChanged tx -> SnapshotVersion
newVersion :: SnapshotVersion
newVersion, TxIdType tx
$sel:depositTxId:HeadInitialized :: forall tx. StateChanged tx -> TxIdType tx
depositTxId :: TxIdType tx
depositTxId} ->
    case HeadState tx
st of
      Open
        os :: OpenState tx
os@OpenState{CoordinatedHeadState tx
$sel:coordinatedHeadState:OpenState :: forall tx. OpenState tx -> CoordinatedHeadState tx
coordinatedHeadState :: CoordinatedHeadState tx
coordinatedHeadState} ->
          OpenState tx -> HeadState tx
forall tx. OpenState tx -> HeadState tx
Open
            OpenState tx
os
              { coordinatedHeadState =
                  coordinatedHeadState
                    { pendingDeposits = Map.delete depositTxId existingDeposits
                    , version = newVersion
                    }
              }
         where
          CoordinatedHeadState{$sel:pendingDeposits:CoordinatedHeadState :: forall tx.
CoordinatedHeadState tx -> Map (TxIdType tx) (UTxOType tx)
pendingDeposits = Map (TxIdType tx) (UTxOType tx)
existingDeposits} = CoordinatedHeadState tx
coordinatedHeadState
      HeadState tx
_otherState -> HeadState tx
st
  DecommitFinalized{SnapshotVersion
$sel:newVersion:HeadInitialized :: forall tx. StateChanged tx -> SnapshotVersion
newVersion :: SnapshotVersion
newVersion} ->
    case HeadState tx
st of
      Open
        os :: OpenState tx
os@OpenState{CoordinatedHeadState tx
$sel:coordinatedHeadState:OpenState :: forall tx. OpenState tx -> CoordinatedHeadState tx
coordinatedHeadState :: CoordinatedHeadState tx
coordinatedHeadState} ->
          OpenState tx -> HeadState tx
forall tx. OpenState tx -> HeadState tx
Open
            OpenState tx
os
              { coordinatedHeadState =
                  coordinatedHeadState
                    { decommitTx = Nothing
                    , version = newVersion
                    }
              }
      HeadState tx
_otherState -> HeadState tx
st
  StateChanged tx
HeadIsReadyToFanout ->
    case HeadState tx
st of
      Closed ClosedState tx
cst -> ClosedState tx -> HeadState tx
forall tx. ClosedState tx -> HeadState tx
Closed ClosedState tx
cst{readyToFanoutSent = True}
      HeadState tx
_otherState -> HeadState tx
st
  ChainRolledBack{ChainStateType tx
$sel:chainState:HeadInitialized :: forall tx. StateChanged tx -> ChainStateType tx
chainState :: ChainStateType tx
chainState} ->
    ChainStateType tx -> HeadState tx -> HeadState tx
forall tx. ChainStateType tx -> HeadState tx -> HeadState tx
setChainState ChainStateType tx
chainState HeadState tx
st
  TickObserved{ChainSlot
$sel:chainSlot:HeadInitialized :: forall tx. StateChanged tx -> ChainSlot
chainSlot :: ChainSlot
chainSlot} ->
    case HeadState tx
st of
      Open ost :: OpenState tx
ost@OpenState{} -> OpenState tx -> HeadState tx
forall tx. OpenState tx -> HeadState tx
Open OpenState tx
ost{currentSlot = chainSlot}
      HeadState tx
_otherState -> HeadState tx
st

aggregateState ::
  IsChainState tx =>
  HeadState tx ->
  Outcome tx ->
  HeadState tx
aggregateState :: forall tx.
IsChainState tx =>
HeadState tx -> Outcome tx -> HeadState tx
aggregateState HeadState tx
s Outcome tx
outcome =
  HeadState tx -> [StateChanged tx] -> HeadState tx
forall (t :: * -> *) tx.
(Foldable t, IsChainState tx) =>
HeadState tx -> t (StateChanged tx) -> HeadState tx
recoverState HeadState tx
s ([StateChanged tx] -> HeadState tx)
-> [StateChanged tx] -> HeadState tx
forall a b. (a -> b) -> a -> b
$ Outcome tx -> [StateChanged tx]
forall {tx}. Outcome tx -> [StateChanged tx]
collectStateChanged Outcome tx
outcome
 where
  collectStateChanged :: Outcome tx -> [StateChanged tx]
collectStateChanged = \case
    Error{} -> []
    Wait{[StateChanged tx]
stateChanges :: [StateChanged tx]
$sel:stateChanges:Continue :: forall {tx}. Outcome tx -> [StateChanged tx]
stateChanges} -> [StateChanged tx]
stateChanges
    Continue{[StateChanged tx]
$sel:stateChanges:Continue :: forall {tx}. Outcome tx -> [StateChanged tx]
stateChanges :: [StateChanged tx]
stateChanges} -> [StateChanged tx]
stateChanges

recoverChainStateHistory ::
  (Foldable t, IsChainState tx) =>
  ChainStateType tx ->
  t (StateChanged tx) ->
  ChainStateHistory tx
recoverChainStateHistory :: forall (t :: * -> *) tx.
(Foldable t, IsChainState tx) =>
ChainStateType tx -> t (StateChanged tx) -> ChainStateHistory tx
recoverChainStateHistory ChainStateType tx
initialChainState =
  (ChainStateHistory tx -> StateChanged tx -> ChainStateHistory tx)
-> ChainStateHistory tx
-> t (StateChanged tx)
-> ChainStateHistory tx
forall b a. (b -> a -> b) -> b -> t a -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' ChainStateHistory tx -> StateChanged tx -> ChainStateHistory tx
forall {tx}.
IsChainState tx =>
ChainStateHistory tx -> StateChanged tx -> ChainStateHistory tx
aggregateChainStateHistory (ChainStateType tx -> ChainStateHistory tx
forall tx. ChainStateType tx -> ChainStateHistory tx
initHistory ChainStateType tx
initialChainState)
 where
  aggregateChainStateHistory :: ChainStateHistory tx -> StateChanged tx -> ChainStateHistory tx
aggregateChainStateHistory ChainStateHistory tx
history = \case
    HeadInitialized{ChainStateType tx
$sel:chainState:HeadInitialized :: forall tx. StateChanged tx -> ChainStateType tx
chainState :: ChainStateType tx
chainState} -> ChainStateType tx -> ChainStateHistory tx -> ChainStateHistory tx
forall tx.
ChainStateType tx -> ChainStateHistory tx -> ChainStateHistory tx
pushNewState ChainStateType tx
chainState ChainStateHistory tx
history
    CommittedUTxO{ChainStateType tx
$sel:chainState:HeadInitialized :: forall tx. StateChanged tx -> ChainStateType tx
chainState :: ChainStateType tx
chainState} -> ChainStateType tx -> ChainStateHistory tx -> ChainStateHistory tx
forall tx.
ChainStateType tx -> ChainStateHistory tx -> ChainStateHistory tx
pushNewState ChainStateType tx
chainState ChainStateHistory tx
history
    HeadAborted{ChainStateType tx
$sel:chainState:HeadInitialized :: forall tx. StateChanged tx -> ChainStateType tx
chainState :: ChainStateType tx
chainState} -> ChainStateType tx -> ChainStateHistory tx -> ChainStateHistory tx
forall tx.
ChainStateType tx -> ChainStateHistory tx -> ChainStateHistory tx
pushNewState ChainStateType tx
chainState ChainStateHistory tx
history
    HeadOpened{ChainStateType tx
$sel:chainState:HeadInitialized :: forall tx. StateChanged tx -> ChainStateType tx
chainState :: ChainStateType tx
chainState} -> ChainStateType tx -> ChainStateHistory tx -> ChainStateHistory tx
forall tx.
ChainStateType tx -> ChainStateHistory tx -> ChainStateHistory tx
pushNewState ChainStateType tx
chainState ChainStateHistory tx
history
    TransactionAppliedToLocalUTxO{} -> ChainStateHistory tx
history
    CommitRecovered{} -> ChainStateHistory tx
history
    CommitRecorded{} -> ChainStateHistory tx
history
    DecommitRecorded{} -> ChainStateHistory tx
history
    SnapshotRequestDecided{} -> ChainStateHistory tx
history
    SnapshotRequested{} -> ChainStateHistory tx
history
    TransactionReceived{} -> ChainStateHistory tx
history
    PartySignedSnapshot{} -> ChainStateHistory tx
history
    SnapshotConfirmed{} -> ChainStateHistory tx
history
    CommitFinalized{} -> ChainStateHistory tx
history
    DecommitFinalized{} -> ChainStateHistory tx
history
    HeadClosed{ChainStateType tx
$sel:chainState:HeadInitialized :: forall tx. StateChanged tx -> ChainStateType tx
chainState :: ChainStateType tx
chainState} -> ChainStateType tx -> ChainStateHistory tx -> ChainStateHistory tx
forall tx.
ChainStateType tx -> ChainStateHistory tx -> ChainStateHistory tx
pushNewState ChainStateType tx
chainState ChainStateHistory tx
history
    HeadContested{ChainStateType tx
$sel:chainState:HeadInitialized :: forall tx. StateChanged tx -> ChainStateType tx
chainState :: ChainStateType tx
chainState} -> ChainStateType tx -> ChainStateHistory tx -> ChainStateHistory tx
forall tx.
ChainStateType tx -> ChainStateHistory tx -> ChainStateHistory tx
pushNewState ChainStateType tx
chainState ChainStateHistory tx
history
    HeadIsReadyToFanout{} -> ChainStateHistory tx
history
    HeadFannedOut{ChainStateType tx
$sel:chainState:HeadInitialized :: forall tx. StateChanged tx -> ChainStateType tx
chainState :: ChainStateType tx
chainState} -> ChainStateType tx -> ChainStateHistory tx -> ChainStateHistory tx
forall tx.
ChainStateType tx -> ChainStateHistory tx -> ChainStateHistory tx
pushNewState ChainStateType tx
chainState ChainStateHistory tx
history
    ChainRolledBack{ChainStateType tx
$sel:chainState:HeadInitialized :: forall tx. StateChanged tx -> ChainStateType tx
chainState :: ChainStateType tx
chainState} ->
      ChainSlot -> ChainStateHistory tx -> ChainStateHistory tx
forall tx.
IsChainState tx =>
ChainSlot -> ChainStateHistory tx -> ChainStateHistory tx
rollbackHistory (ChainStateType tx -> ChainSlot
forall tx. IsChainState tx => ChainStateType tx -> ChainSlot
chainStateSlot ChainStateType tx
chainState) ChainStateHistory tx
history
    TickObserved{} -> ChainStateHistory tx
history

recoverState ::
  (Foldable t, IsChainState tx) =>
  HeadState tx ->
  t (StateChanged tx) ->
  HeadState tx
recoverState :: forall (t :: * -> *) tx.
(Foldable t, IsChainState tx) =>
HeadState tx -> t (StateChanged tx) -> HeadState tx
recoverState = (HeadState tx -> StateChanged tx -> HeadState tx)
-> HeadState tx -> t (StateChanged tx) -> HeadState tx
forall b a. (b -> a -> b) -> b -> t a -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' HeadState tx -> StateChanged tx -> HeadState tx
forall tx.
IsChainState tx =>
HeadState tx -> StateChanged tx -> HeadState tx
aggregate