{-# LANGUAGE DuplicateRecordFields #-}
{-# LANGUAGE UndecidableInstances #-}

-- | 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,
  module Hydra.HeadLogic.SnapshotOutcome,
) where

import Hydra.Prelude

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 qualified as ServerOutput
import Hydra.Chain (
  ChainEvent (..),
  ChainStateHistory,
  ChainStateType,
  HeadParameters (..),
  IsChainState (chainStateSlot),
  OnChainTx (..),
  PostChainTx (..),
  initHistory,
  mkHeadParameters,
  pushNewState,
  rollbackHistory,
 )
import Hydra.Crypto (
  Signature,
  Verified (..),
  aggregateInOrder,
  sign,
  verifyMultiSignature,
 )
import Hydra.Environment (Environment (..))
import Hydra.HeadId (HeadId, HeadSeed)
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.SnapshotOutcome (isLeader)
import Hydra.HeadLogic.State (
  ClosedState (..),
  Committed,
  CoordinatedHeadState (..),
  HeadState (..),
  IdleState (IdleState, chainState),
  InitialState (..),
  OpenState (..),
  PendingCommits,
  SeenSnapshot (..),
  seenSnapshotNumber,
  setChainState,
 )
import Hydra.Ledger (
  IsTx,
  Ledger (..),
  TxIdType,
  UTxOType,
  applyTransactions,
  txId,
 )
import Hydra.Network.Message (Message (..))
import Hydra.OnChainId (OnChainId)
import Hydra.Party (Party (vkey))
import Hydra.Snapshot (ConfirmedSnapshot (..), Snapshot (..), SnapshotNumber, getSnapshot)

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

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

  -- 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 =
  -- Spec: Tall ← ̂Tall ∪ { (hash(tx), tx) }
  (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 ≠ ⊥ combined with L̂ ← 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 ->
      -- Spec: if ŝ = s̄ ∧ leader(s̄ + 1) = i
      ( if Bool -> Bool
not Bool
snapshotInFlight Bool -> Bool -> Bool
&& HeadParameters -> Party -> SnapshotNumber -> Bool
isLeader HeadParameters
parameters Party
party SnapshotNumber
nextSn
          then
            StateChanged tx -> Outcome tx
forall tx. StateChanged tx -> Outcome tx
newState TransactionAppliedToLocalUTxO{$sel:tx:HeadInitialized :: tx
tx = tx
tx, UTxOType tx
newLocalUTxO :: UTxOType tx
$sel:newLocalUTxO:HeadInitialized :: UTxOType tx
newLocalUTxO}
              Outcome tx -> Outcome tx -> Outcome tx
forall a. Semigroup a => a -> a -> a
<>
              -- 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.
              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
$ SnapshotNumber -> [TxIdType tx] -> Message tx
forall tx. SnapshotNumber -> [TxIdType tx] -> Message tx
ReqSn 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'))
          else 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}
      )
        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 -> tx -> ServerOutput tx
forall tx. HeadId -> tx -> ServerOutput tx
ServerOutput.TxValid HeadId
headId tx
tx)
 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

  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

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

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

  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 number.
  SnapshotNumber ->
  -- | List of transactions to snapshot.
  [TxIdType tx] ->
  Outcome tx
onOpenNetworkReqSn :: forall tx.
IsTx tx =>
Environment
-> Ledger tx
-> OpenState tx
-> Party
-> SnapshotNumber
-> [TxIdType tx]
-> Outcome tx
onOpenNetworkReqSn Environment
env Ledger tx
ledger OpenState tx
st Party
otherParty SnapshotNumber
sn [TxIdType tx]
requestedTxIds =
  -- TODO: Verify the request is signed by (?) / comes from the leader
  -- (Can we prove a message comes from a given peer, without signature?)

  -- Spec: require s = ŝ + 1 and 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̅ = ŝ
    Outcome tx -> Outcome tx
waitNoSnapshotInFlight (Outcome tx -> Outcome tx) -> Outcome tx -> Outcome tx
forall a b. (a -> b) -> a -> b
$
      -- Spec: wait ∀h ∈ Treq : (h, ·) ∈ Tall
      Outcome tx -> Outcome tx
waitResolvableTxs (Outcome tx -> Outcome tx) -> Outcome tx -> Outcome tx
forall a b. (a -> b) -> a -> b
$ do
        -- Spec: Treq ← {Tall [h] | h ∈ Treq#}
        let requestedTxs :: [tx]
requestedTxs = (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
        -- Spec: require U̅ ◦ Treq /= ⊥ combined with Û ← Ū̅ ◦ Treq
        [tx] -> (UTxOType tx -> Outcome tx) -> Outcome tx
requireApplyTxs [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
          -- NOTE: confSn == seenSn == sn here
          let nextSnapshot :: Snapshot tx
nextSnapshot = HeadId
-> SnapshotNumber -> UTxOType tx -> [TxIdType tx] -> Snapshot tx
forall tx.
HeadId
-> SnapshotNumber -> UTxOType tx -> [TxIdType tx] -> Snapshot tx
Snapshot HeadId
headId (SnapshotNumber
confSn SnapshotNumber -> SnapshotNumber -> SnapshotNumber
forall a. Num a => a -> a -> a
+ SnapshotNumber
1) UTxOType tx
u [TxIdType tx]
requestedTxIds
          -- Spec: σᵢ
          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
          (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: for loop which updates T̂ and L̂
              let ([tx]
newLocalTxs, UTxOType tx
newLocalUTxO) = UTxOType tx -> ([tx], UTxOType tx)
pruneTransactions UTxOType tx
u
              -- Spec (in aggregate): Tall ← {tx | ∀tx ∈ Tall : tx ∉ Treq }
              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
    | 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

  waitResolvableTxs :: Outcome tx -> Outcome tx
waitResolvableTxs 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
      [] -> Outcome tx
continue
      [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

  -- 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 :: [tx] -> (UTxOType tx -> Outcome tx) -> Outcome tx
requireApplyTxs [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
confirmedUTxO [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
    (tx -> ([tx], UTxOType tx) -> ([tx], UTxOType tx))
-> ([tx], UTxOType tx) -> [tx] -> ([tx], UTxOType tx)
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr tx -> ([tx], UTxOType tx) -> ([tx], UTxOType tx)
go ([], UTxOType tx
utxo) [tx]
localTxs
   where
    go :: tx -> ([tx], UTxOType tx) -> ([tx], UTxOType tx)
go tx
tx ([tx]
txs, UTxOType tx
u) =
      -- 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

  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
utxo :: UTxOType tx
$sel:utxo:Snapshot :: forall tx. Snapshot tx -> 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} = 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 =
  -- TODO: verify authenticity of message and whether otherParty is part of the head
  -- 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: (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
        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_H, ̂Σ̂)
          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
          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
              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)
              Outcome tx -> (Outcome tx -> Outcome tx) -> Outcome tx
forall a b. a -> (a -> b) -> b
& Outcome tx -> Outcome tx
maybeEmitSnapshot
 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}

  maybeEmitSnapshot :: Outcome tx -> Outcome tx
maybeEmitSnapshot 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
$ SnapshotNumber -> [TxIdType tx] -> Message tx
forall tx. SnapshotNumber -> [TxIdType tx] -> Message tx
ReqSn 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))
      else Outcome tx
outcome

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

  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

  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} = CoordinatedHeadState tx
coordinatedHeadState

-- ** 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 =
  Effect tx -> Outcome tx
forall tx. Effect tx -> Outcome tx
cause OnChainEffect{$sel:postChainTx:ClientEffect :: PostChainTx tx
postChainTx = HeadId -> HeadParameters -> ConfirmedSnapshot tx -> PostChainTx tx
forall tx.
HeadId -> HeadParameters -> ConfirmedSnapshot tx -> PostChainTx tx
CloseTx HeadId
headId HeadParameters
parameters ConfirmedSnapshot tx
confirmedSnapshot}
 where
  CoordinatedHeadState{ConfirmedSnapshot tx
$sel:confirmedSnapshot:CoordinatedHeadState :: forall tx. CoordinatedHeadState tx -> ConfirmedSnapshot tx
confirmedSnapshot :: ConfirmedSnapshot tx
confirmedSnapshot} = 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
causes
      ( Effect tx
notifyClient
          Effect tx -> [Effect tx] -> [Effect tx]
forall a. a -> [a] -> [a]
: [ OnChainEffect
              { $sel:postChainTx:ClientEffect :: PostChainTx tx
postChainTx = ContestTx{HeadId
$sel:headId:InitTx :: HeadId
headId :: HeadId
headId, HeadParameters
$sel:headParameters:InitTx :: HeadParameters
headParameters :: HeadParameters
headParameters, ConfirmedSnapshot tx
confirmedSnapshot :: ConfirmedSnapshot tx
$sel:confirmedSnapshot:InitTx :: ConfirmedSnapshot tx
confirmedSnapshot}
              }
            | Bool
doContest
            ]
      )
 where
  doContest :: Bool
doContest =
    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

  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} = 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
      | 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) ->
          Effect tx -> Outcome tx
forall tx. Effect tx -> Outcome tx
cause Effect tx
notifyClients
            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, ConfirmedSnapshot tx
$sel:confirmedSnapshot:InitTx :: ConfirmedSnapshot tx
confirmedSnapshot :: 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} = 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 ::
  ClosedState tx ->
  Outcome tx
onClosedClientFanout :: forall 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, 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} = 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} = 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
  (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 Party
_ (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
_ Party
otherParty (ReqSn SnapshotNumber
sn [TxIdType tx]
txIds)) ->
    -- XXX: ttl == 0 not handled for ReqSn
    Environment
-> Ledger tx
-> OpenState tx
-> Party
-> SnapshotNumber
-> [TxIdType tx]
-> Outcome tx
forall tx.
IsTx tx =>
Environment
-> Ledger tx
-> OpenState tx
-> Party
-> SnapshotNumber
-> [TxIdType tx]
-> Outcome tx
onOpenNetworkReqSn Environment
env Ledger tx
ledger OpenState tx
openState Party
otherParty SnapshotNumber
sn [TxIdType tx]
txIds
  (Open OpenState tx
openState, NetworkInput TTL
_ Party
otherParty (AckSn Signature (Snapshot tx)
snapshotSignature SnapshotNumber
sn)) ->
    -- XXX: ttl == 0 not handled for AckSn
    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
otherParty 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
  -- 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. 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 =
                -- Spec: Tall ← ̂Tall ∪ { (hash(tx), tx) }
                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
                  , 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
  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
              }
          , 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
              }
      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} ->
        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
            }
      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
                  }
            , 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{Snapshot tx
$sel:snapshot:HeadInitialized :: forall tx. StateChanged tx -> Snapshot tx
snapshot :: Snapshot tx
snapshot, 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 = 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 = SeenSnapshot snapshot sigs}
              }
         where
          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
party Signature (Snapshot tx)
signature Map Party (Signature (Snapshot tx))
signatories
      HeadState tx
_otherState -> HeadState tx
st
  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
    SnapshotRequestDecided{} -> ChainStateHistory tx
history
    SnapshotRequested{} -> ChainStateHistory tx
history
    TransactionReceived{} -> ChainStateHistory tx
history
    PartySignedSnapshot{} -> ChainStateHistory tx
history
    SnapshotConfirmed{} -> 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