/
UTXOWS.hs
59 lines (48 loc) · 1.94 KB
/
UTXOWS.hs
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
-- | Transition system that models the application of multiple transactions to
-- the UTxO part of the ledger state.
module Cardano.Ledger.Spec.STS.UTXOWS where
import Data.Data (Data, Typeable)
import Cardano.Ledger.Spec.STS.UTXO (UTxOEnv, UTxOState)
import Cardano.Ledger.Spec.STS.UTXOW (UTXOW)
import Control.State.Transition (Embed, Environment, IRC (IRC), PredicateFailure, STS,
Signal, State, TRC (TRC), initialRules, judgmentContext, trans,
transitionRules, wrapFailed)
import Control.State.Transition.Generator (HasTrace, envGen, genTrace, sigGen)
import Control.State.Transition.Trace (TraceOrder (OldestFirst), traceSignals)
import Ledger.UTxO (TxWits)
data UTXOWS deriving (Data, Typeable)
instance STS UTXOWS where
type State UTXOWS = UTxOState
type Signal UTXOWS = [TxWits]
type Environment UTXOWS = UTxOEnv
data PredicateFailure UTXOWS
= UtxowFailure (PredicateFailure UTXOW)
deriving (Eq, Show, Data, Typeable)
initialRules =
[ do
IRC env <- judgmentContext
trans @UTXOW $ IRC env
]
transitionRules =
[ do
TRC (env, utxo, txWits) <- judgmentContext
case (txWits :: [TxWits]) of
[] -> return utxo
(tx:gamma) -> do
utxo' <- trans @UTXOW $ TRC (env, utxo, tx)
utxo'' <- trans @UTXOWS $ TRC (env, utxo', gamma)
return utxo''
]
instance Embed UTXOW UTXOWS where
wrapFailed = UtxowFailure
instance HasTrace UTXOWS where
envGen = envGen @UTXOW
-- We generate signal for UTXOWS as a list of signals from UTXOW
sigGen env st =
traceSignals OldestFirst <$> genTrace @UTXOW () 20 env st (sigGen @UTXOW)