From 5e6b82cb2e51860cd5c9c20e724c8ad7b8f56f92 Mon Sep 17 00:00:00 2001 From: Zachary Churchill Date: Tue, 6 Jul 2021 11:20:58 -0400 Subject: [PATCH 1/4] add Event type family --- .../src/Cardano/Ledger/Alonzo/Rules/Bbody.hs | 7 + .../src/Cardano/Ledger/Alonzo/Rules/Ledger.hs | 18 +- .../src/Cardano/Ledger/Alonzo/Rules/Utxo.hs | 1 + .../src/Cardano/Ledger/Alonzo/Rules/Utxos.hs | 1 + .../src/Cardano/Ledger/Alonzo/Rules/Utxow.hs | 1 + .../test/Test/Cardano/Ledger/Alonzo/Trials.hs | 6 +- .../src/Byron/Spec/Chain/STS/Rule/BBody.hs | 5 +- .../src/Byron/Spec/Chain/STS/Rule/Bupi.hs | 5 +- .../src/Byron/Spec/Chain/STS/Rule/Chain.hs | 5 + .../src/Byron/Spec/Chain/STS/Rule/Epoch.hs | 2 + .../src/Byron/Spec/Chain/STS/Rule/Pbft.hs | 2 + .../src/Byron/Spec/Chain/STS/Rule/SigCnt.hs | 1 + .../crypto/test/Test/Cardano/Crypto/Limits.hs | 2 +- .../src/Byron/Spec/Ledger/Delegation.hs | 7 +- .../src/Byron/Spec/Ledger/STS/UTXOW.hs | 3 +- .../src/Byron/Spec/Ledger/STS/UTXOWS.hs | 5 +- .../src/Byron/Spec/Ledger/Update.hs | 13 +- .../Spec/Ledger/Delegation/Properties.hs | 3 +- .../Byron/Spec/Ledger/Update/Properties.hs | 5 +- .../test/Test/Cardano/Chain/Update/Gen.hs | 2 +- .../Cardano/Ledger/Rules/ValidationMode.hs | 2 +- semantics/executable-spec/small-steps.cabal | 1 + .../src/Control/State/Transition/Extended.hs | 165 ++++++++++++++---- .../src/Control/State/Transition/Trace.hs | 2 +- .../State/Transition/Examples/CommitReveal.hs | 1 + .../State/Transition/Examples/GlobalSum.hs | 1 + .../Control/State/Transition/Examples/Sum.hs | 1 + .../Cardano/Ledger/ShelleyMA/Rules/Utxo.hs | 1 + .../Cardano/Ledger/ShelleyMA/Rules/Utxow.hs | 6 +- .../Test/Cardano/Ledger/TranslationTools.hs | 2 +- .../src/Shelley/Spec/Ledger/STS/Bbody.hs | 8 + .../src/Shelley/Spec/Ledger/STS/Chain.hs | 22 ++- .../src/Shelley/Spec/Ledger/STS/Delegs.hs | 11 +- .../src/Shelley/Spec/Ledger/STS/Delpl.hs | 8 + .../src/Shelley/Spec/Ledger/STS/Epoch.hs | 3 + .../src/Shelley/Spec/Ledger/STS/Ledger.hs | 17 +- .../src/Shelley/Spec/Ledger/STS/Ledgers.hs | 10 +- .../src/Shelley/Spec/Ledger/STS/NewEpoch.hs | 2 + .../src/Shelley/Spec/Ledger/STS/Overlay.hs | 1 + .../src/Shelley/Spec/Ledger/STS/Pool.hs | 13 +- .../src/Shelley/Spec/Ledger/STS/Prtcl.hs | 2 + .../src/Shelley/Spec/Ledger/STS/Tick.hs | 3 + .../src/Shelley/Spec/Ledger/STS/Upec.hs | 1 + .../src/Shelley/Spec/Ledger/STS/Utxo.hs | 2 + .../src/Shelley/Spec/Ledger/STS/Utxow.hs | 6 + .../Spec/Ledger/Generator/Trace/DCert.hs | 13 +- .../src/Test/Shelley/Spec/Ledger/Utils.hs | 2 +- 47 files changed, 328 insertions(+), 72 deletions(-) diff --git a/alonzo/impl/src/Cardano/Ledger/Alonzo/Rules/Bbody.hs b/alonzo/impl/src/Cardano/Ledger/Alonzo/Rules/Bbody.hs index 26c9a2b38b9..4ad13b34634 100644 --- a/alonzo/impl/src/Cardano/Ledger/Alonzo/Rules/Bbody.hs +++ b/alonzo/impl/src/Cardano/Ledger/Alonzo/Rules/Bbody.hs @@ -15,6 +15,7 @@ module Cardano.Ledger.Alonzo.Rules.Bbody ( AlonzoBBODY, AlonzoBbodyPredFail (..), + AlonzoBbodyEvent (..), bbodyTransition, ) where @@ -64,6 +65,7 @@ import Shelley.Spec.Ledger.LedgerState (LedgerState) import Shelley.Spec.Ledger.OverlaySchedule (isOverlaySlot) import Shelley.Spec.Ledger.STS.Bbody ( BbodyEnv (..), + BbodyEvent (..), BbodyPredicateFailure (..), BbodyState (..), ) @@ -82,6 +84,9 @@ data AlonzoBbodyPredFail era -- ^ Maximum allowed by protocal parameters deriving (Generic) +data AlonzoBbodyEvent era + = ShelleyInAlonzoEvent (BbodyEvent era) + deriving instance (Era era, Show (PredicateFailure (Core.EraRule "LEDGERS" era))) => Show (AlonzoBbodyPredFail era) @@ -230,6 +235,7 @@ instance type BaseM (AlonzoBBODY era) = ShelleyBase type PredicateFailure (AlonzoBBODY era) = AlonzoBbodyPredFail era + type Event (AlonzoBBODY era) = AlonzoBbodyEvent era initialRules = [] transitionRules = [bbodyTransition @AlonzoBBODY] @@ -245,3 +251,4 @@ instance Embed ledgers (AlonzoBBODY era) where wrapFailed = ShelleyInAlonzoPredFail . LedgersFailure + wrapEvent = ShelleyInAlonzoEvent . LedgersEvent diff --git a/alonzo/impl/src/Cardano/Ledger/Alonzo/Rules/Ledger.hs b/alonzo/impl/src/Cardano/Ledger/Alonzo/Rules/Ledger.hs index 7b9868bf543..c4dfb134c28 100644 --- a/alonzo/impl/src/Cardano/Ledger/Alonzo/Rules/Ledger.hs +++ b/alonzo/impl/src/Cardano/Ledger/Alonzo/Rules/Ledger.hs @@ -42,6 +42,7 @@ import Data.Kind (Type) import Data.Sequence (Seq) import Data.Sequence.Strict (StrictSeq) import qualified Data.Sequence.Strict as StrictSeq +import Data.Void (Void) import GHC.Records (HasField, getField) import Shelley.Spec.Ledger.EpochBoundary (obligation) import Shelley.Spec.Ledger.LedgerState @@ -50,8 +51,8 @@ import Shelley.Spec.Ledger.LedgerState PState (..), UTxOState (..), ) -import Shelley.Spec.Ledger.STS.Delegs (DELEGS, DelegsEnv (..), DelegsPredicateFailure) -import Shelley.Spec.Ledger.STS.Ledger (LedgerEnv (..), LedgerPredicateFailure (..)) +import Shelley.Spec.Ledger.STS.Delegs (DELEGS, DelegsEnv (..), DelegsEvent, DelegsPredicateFailure) +import Shelley.Spec.Ledger.STS.Ledger (LedgerEnv (..), LedgerEvent (..), LedgerPredicateFailure (..)) import qualified Shelley.Spec.Ledger.STS.Ledgers as Shelley import Shelley.Spec.Ledger.STS.Utxo ( UtxoEnv (..), @@ -143,6 +144,7 @@ instance type Environment (AlonzoLEDGER era) = LedgerEnv era type BaseM (AlonzoLEDGER era) = ShelleyBase type PredicateFailure (AlonzoLEDGER era) = LedgerPredicateFailure era + type Event (AlonzoLEDGER era) = LedgerEvent era initialRules = [] transitionRules = [ledgerTransition @AlonzoLEDGER] @@ -167,26 +169,32 @@ instance instance ( Era era, STS (DELEGS era), - PredicateFailure (Core.EraRule "DELEGS" era) ~ DelegsPredicateFailure era + PredicateFailure (Core.EraRule "DELEGS" era) ~ DelegsPredicateFailure era, + Event (Core.EraRule "DELEGS" era) ~ DelegsEvent era ) => Embed (DELEGS era) (AlonzoLEDGER era) where wrapFailed = DelegsFailure + wrapEvent = DelegsEvent instance ( Era era, STS (AlonzoUTXOW era), - PredicateFailure (Core.EraRule "UTXOW" era) ~ AlonzoPredFail era + PredicateFailure (Core.EraRule "UTXOW" era) ~ AlonzoPredFail era, + Event (Core.EraRule "UTXOW" era) ~ Void ) => Embed (AlonzoUTXOW era) (AlonzoLEDGER era) where wrapFailed = UtxowFailure + wrapEvent = UtxowEvent instance ( Era era, STS (AlonzoLEDGER era), - PredicateFailure (Core.EraRule "LEDGER" era) ~ LedgerPredicateFailure era + PredicateFailure (Core.EraRule "LEDGER" era) ~ LedgerPredicateFailure era, + Event (Core.EraRule "LEDGER" era) ~ LedgerEvent era ) => Embed (AlonzoLEDGER era) (Shelley.LEDGERS era) where wrapFailed = Shelley.LedgerFailure + wrapEvent = Shelley.LedgerEvent diff --git a/alonzo/impl/src/Cardano/Ledger/Alonzo/Rules/Utxo.hs b/alonzo/impl/src/Cardano/Ledger/Alonzo/Rules/Utxo.hs index e0106673f72..569dc9791bf 100644 --- a/alonzo/impl/src/Cardano/Ledger/Alonzo/Rules/Utxo.hs +++ b/alonzo/impl/src/Cardano/Ledger/Alonzo/Rules/Utxo.hs @@ -518,6 +518,7 @@ instance Embed (UTXOS era) (AlonzoUTXO era) where wrapFailed = UtxosFailure + wrapEvent = id -------------------------------------------------------------------------------- -- Serialisation diff --git a/alonzo/impl/src/Cardano/Ledger/Alonzo/Rules/Utxos.hs b/alonzo/impl/src/Cardano/Ledger/Alonzo/Rules/Utxos.hs index c1b12085351..587bd761b85 100644 --- a/alonzo/impl/src/Cardano/Ledger/Alonzo/Rules/Utxos.hs +++ b/alonzo/impl/src/Cardano/Ledger/Alonzo/Rules/Utxos.hs @@ -294,6 +294,7 @@ instance Embed (PPUP era) (UTXOS era) where wrapFailed = UpdateFailure + wrapEvent = id -- ================================================================= diff --git a/alonzo/impl/src/Cardano/Ledger/Alonzo/Rules/Utxow.hs b/alonzo/impl/src/Cardano/Ledger/Alonzo/Rules/Utxow.hs index 6468ce7da56..1b1bf26cfcd 100644 --- a/alonzo/impl/src/Cardano/Ledger/Alonzo/Rules/Utxow.hs +++ b/alonzo/impl/src/Cardano/Ledger/Alonzo/Rules/Utxow.hs @@ -456,3 +456,4 @@ instance Embed (AlonzoUTXO era) (AlonzoUTXOW era) where wrapFailed = WrappedShelleyEraFailure . UtxoFailure + wrapEvent = id diff --git a/alonzo/test/test/Test/Cardano/Ledger/Alonzo/Trials.hs b/alonzo/test/test/Test/Cardano/Ledger/Alonzo/Trials.hs index 2344dfbb97f..014ebc98cea 100644 --- a/alonzo/test/test/Test/Cardano/Ledger/Alonzo/Trials.hs +++ b/alonzo/test/test/Test/Cardano/Ledger/Alonzo/Trials.hs @@ -81,8 +81,8 @@ import Shelley.Spec.Ledger.LedgerState UTxOState, ) import Shelley.Spec.Ledger.PParams (PParams' (..)) -import Shelley.Spec.Ledger.STS.Chain (CHAIN, ChainPredicateFailure (..), ChainState (..)) -import Shelley.Spec.Ledger.STS.Ledger (LEDGER, LedgerEnv (..), LedgerPredicateFailure (UtxowFailure)) +import Shelley.Spec.Ledger.STS.Chain (CHAIN, ChainEvent (..), ChainPredicateFailure (..), ChainState (..)) +import Shelley.Spec.Ledger.STS.Ledger (LEDGER, LedgerEnv (..), LedgerEvent (..), LedgerPredicateFailure (UtxowFailure)) import System.Timeout import Test.Cardano.Ledger.Alonzo.AlonzoEraGen () import Test.Cardano.Ledger.EraBuffet (TestCrypto) @@ -118,9 +118,11 @@ import Test.Tasty.QuickCheck instance Embed (AlonzoBBODY (AlonzoEra TestCrypto)) (CHAIN (AlonzoEra TestCrypto)) where wrapFailed = BbodyFailure + wrapEvent = BbodyEvent instance Embed (AlonzoUTXOW (AlonzoEra TestCrypto)) (LEDGER (AlonzoEra TestCrypto)) where wrapFailed = UtxowFailure + wrapEvent = UtxowEvent -- ====================================================================================== -- It is incredably hard to debug property test generators. These functions mimic the diff --git a/byron/chain/executable-spec/src/Byron/Spec/Chain/STS/Rule/BBody.hs b/byron/chain/executable-spec/src/Byron/Spec/Chain/STS/Rule/BBody.hs index 5c437e143e1..d2e7a817c11 100644 --- a/byron/chain/executable-spec/src/Byron/Spec/Chain/STS/Rule/BBody.hs +++ b/byron/chain/executable-spec/src/Byron/Spec/Chain/STS/Rule/BBody.hs @@ -22,7 +22,7 @@ import Byron.Spec.Ledger.Update (PParams, UPIState, maxBkSz) import Byron.Spec.Ledger.UTxO (UTxO) import Control.State.Transition (Embed, Environment, STS (..), Signal, State, TRC (TRC), initialRules, judgmentContext, trans, transitionRules, wrapFailed, - (?!)) + (?!), wrapEvent) import Byron.Spec.Chain.STS.Block @@ -93,9 +93,12 @@ instance STS BBODY where instance Embed BUPI BBODY where wrapFailed = BUPIFailure + wrapEvent = id instance Embed DELEG BBODY where wrapFailed = DelegationFailure + wrapEvent = id instance Embed UTXOWS BBODY where wrapFailed = UTXOWSFailure + wrapEvent = id diff --git a/byron/chain/executable-spec/src/Byron/Spec/Chain/STS/Rule/Bupi.hs b/byron/chain/executable-spec/src/Byron/Spec/Chain/STS/Rule/Bupi.hs index e704796632a..d3ad5a9b553 100644 --- a/byron/chain/executable-spec/src/Byron/Spec/Chain/STS/Rule/Bupi.hs +++ b/byron/chain/executable-spec/src/Byron/Spec/Chain/STS/Rule/Bupi.hs @@ -10,7 +10,7 @@ import Data.Data (Data, Typeable) import Control.State.Transition (Embed, Environment, PredicateFailure, STS, Signal, State, TRC (TRC), TransitionRule, initialRules, judgmentContext, trans, - transitionRules, wrapFailed) + transitionRules, wrapFailed, wrapEvent) import Byron.Spec.Ledger.Core (VKey) import Byron.Spec.Ledger.Update (ProtVer, UPIEND, UPIEnv, UPIREG, UPIState, UPIVOTES, UProp, Vote) @@ -67,9 +67,12 @@ instance STS BUPI where instance Embed UPIREG BUPI where wrapFailed = UPIREGFailure + wrapEvent = id instance Embed UPIVOTES BUPI where wrapFailed = UPIVOTESFailure + wrapEvent = id instance Embed UPIEND BUPI where wrapFailed = UPIENDFailure + wrapEvent = id diff --git a/byron/chain/executable-spec/src/Byron/Spec/Chain/STS/Rule/Chain.hs b/byron/chain/executable-spec/src/Byron/Spec/Chain/STS/Rule/Chain.hs index b7b3ad52ec4..17d83f9dc10 100644 --- a/byron/chain/executable-spec/src/Byron/Spec/Chain/STS/Rule/Chain.hs +++ b/byron/chain/executable-spec/src/Byron/Spec/Chain/STS/Rule/Chain.hs @@ -162,18 +162,23 @@ instance STS CHAIN where instance Embed EPOCH CHAIN where wrapFailed = EpochFailure + wrapEvent = id instance Embed BBODY CHAIN where wrapFailed = BBodyFailure + wrapEvent = id instance Embed PBFT CHAIN where wrapFailed = PBFTFailure + wrapEvent = id instance Embed DELEG CHAIN where wrapFailed = LedgerDelegationFailure + wrapEvent = id instance Embed UTXOWS CHAIN where wrapFailed = LedgerUTxOFailure + wrapEvent = id isHeaderSizeTooBigFailure :: PredicateFailure CHAIN -> Bool isHeaderSizeTooBigFailure (HeaderSizeTooBig _ _ _) = True diff --git a/byron/chain/executable-spec/src/Byron/Spec/Chain/STS/Rule/Epoch.hs b/byron/chain/executable-spec/src/Byron/Spec/Chain/STS/Rule/Epoch.hs index 7f08ae732fb..8c0c992cc82 100644 --- a/byron/chain/executable-spec/src/Byron/Spec/Chain/STS/Rule/Epoch.hs +++ b/byron/chain/executable-spec/src/Byron/Spec/Chain/STS/Rule/Epoch.hs @@ -42,6 +42,7 @@ instance STS EPOCH where type Signal EPOCH = Slot type PredicateFailure EPOCH = EpochPredicateFailure + initialRules = [] transitionRules = @@ -57,3 +58,4 @@ instance STS EPOCH where instance Embed UPIEC EPOCH where wrapFailed = UPIECFailure + wrapEvent = id diff --git a/byron/chain/executable-spec/src/Byron/Spec/Chain/STS/Rule/Pbft.hs b/byron/chain/executable-spec/src/Byron/Spec/Chain/STS/Rule/Pbft.hs index fcd43800f92..911b175d459 100644 --- a/byron/chain/executable-spec/src/Byron/Spec/Chain/STS/Rule/Pbft.hs +++ b/byron/chain/executable-spec/src/Byron/Spec/Chain/STS/Rule/Pbft.hs @@ -43,6 +43,7 @@ instance STS PBFT where type PredicateFailure PBFT = PbftPredicateFailure + initialRules = [] transitionRules = @@ -61,3 +62,4 @@ instance STS PBFT where instance Embed SIGCNT PBFT where wrapFailed = SigCountFailure + wrapEvent = id diff --git a/byron/chain/executable-spec/src/Byron/Spec/Chain/STS/Rule/SigCnt.hs b/byron/chain/executable-spec/src/Byron/Spec/Chain/STS/Rule/SigCnt.hs index a042a32707b..7dff0778fe6 100644 --- a/byron/chain/executable-spec/src/Byron/Spec/Chain/STS/Rule/SigCnt.hs +++ b/byron/chain/executable-spec/src/Byron/Spec/Chain/STS/Rule/SigCnt.hs @@ -44,6 +44,7 @@ instance STS SIGCNT where type Signal SIGCNT = VKey type PredicateFailure SIGCNT = SigcntPredicateFailure + initialRules = [] transitionRules = diff --git a/byron/crypto/test/Test/Cardano/Crypto/Limits.hs b/byron/crypto/test/Test/Cardano/Crypto/Limits.hs index 9fdf3d556a5..e02d14b4c10 100644 --- a/byron/crypto/test/Test/Cardano/Crypto/Limits.hs +++ b/byron/crypto/test/Test/Cardano/Crypto/Limits.hs @@ -45,7 +45,7 @@ tests = checkParallel $$discover -- is almost certainly amiss. newtype Limit t = Limit - { getLimit :: Word32 + { getLimit :: Word32 } deriving (Eq, Ord, Show, Num, Enum, Real, Integral) instance Functor Limit where diff --git a/byron/ledger/executable-spec/src/Byron/Spec/Ledger/Delegation.hs b/byron/ledger/executable-spec/src/Byron/Spec/Ledger/Delegation.hs index 4d972895d2c..c41d277059d 100644 --- a/byron/ledger/executable-spec/src/Byron/Spec/Ledger/Delegation.hs +++ b/byron/ledger/executable-spec/src/Byron/Spec/Ledger/Delegation.hs @@ -114,7 +114,7 @@ import Lens.Micro (Lens', lens, to, (%~), (&), (.~), (<>~), (^.), _1) import Lens.Micro.TH (makeFields) import NoThunks.Class (NoThunks (..), allNoThunks, noThunksInKeysAndValues) -import Control.State.Transition (Embed, Environment, IRC (IRC), PredicateFailure, STS, +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, SignalGenerator, envGen, genTrace, @@ -451,6 +451,7 @@ instance STS SDELEGS where instance Embed SDELEG SDELEGS where wrapFailed = SDelegFailure + wrapEvent = id -- | Delegation rules sequencing data ADELEGS deriving (Data, Typeable) @@ -484,6 +485,7 @@ instance STS ADELEGS where instance Embed ADELEG ADELEGS where wrapFailed = ADelegFailure + wrapEvent = id -- | Delegation interface data DELEG deriving (Data, Typeable) @@ -528,9 +530,11 @@ instance STS DELEG where instance Embed SDELEGS DELEG where wrapFailed = SDelegSFailure + wrapEvent = id instance Embed ADELEGS DELEG where wrapFailed = ADelegSFailure + wrapEvent = id -------------------------------------------------------------------------------- -- Generators @@ -623,6 +627,7 @@ instance STS MSDELEG where instance Embed SDELEG MSDELEG where wrapFailed = SDELEGFailure + wrapEvent = id instance HasTrace MSDELEG where diff --git a/byron/ledger/executable-spec/src/Byron/Spec/Ledger/STS/UTXOW.hs b/byron/ledger/executable-spec/src/Byron/Spec/Ledger/STS/UTXOW.hs index 439081c6451..b14543632d9 100644 --- a/byron/ledger/executable-spec/src/Byron/Spec/Ledger/STS/UTXOW.hs +++ b/byron/ledger/executable-spec/src/Byron/Spec/Ledger/STS/UTXOW.hs @@ -25,7 +25,7 @@ import qualified Hedgehog.Gen as Gen import Hedgehog.Internal.Property (CoverPercentage) import qualified Hedgehog.Range as Range -import Control.State.Transition (Embed, Environment, IRC (IRC), STS (..), +import Control.State.Transition (Embed(..), Environment, IRC (IRC), STS (..), Signal, State, TRC (TRC), initialRules, judgmentContext, trans, transitionRules, wrapFailed, (?!)) import Control.State.Transition.Generator (HasTrace, SignalGenerator, coverFailures, @@ -93,6 +93,7 @@ witnessed (Tx tx wits) utxo = instance Embed UTXO UTXOW where wrapFailed = UtxoFailure + wrapEvent = id -- | Constant list of addresses intended to be used in the generators. traceAddrs :: [Addr] diff --git a/byron/ledger/executable-spec/src/Byron/Spec/Ledger/STS/UTXOWS.hs b/byron/ledger/executable-spec/src/Byron/Spec/Ledger/STS/UTXOWS.hs index c87834773bc..20692a3c51a 100644 --- a/byron/ledger/executable-spec/src/Byron/Spec/Ledger/STS/UTXOWS.hs +++ b/byron/ledger/executable-spec/src/Byron/Spec/Ledger/STS/UTXOWS.hs @@ -20,9 +20,9 @@ import GHC.Generics (Generic) import Byron.Spec.Ledger.STS.UTXO (UTxOEnv, UTxOState) import Byron.Spec.Ledger.STS.UTXOW (UTXOW) import Byron.Spec.Ledger.UTxO (Tx) -import Control.State.Transition (Embed, Environment, IRC (IRC), PredicateFailure, STS, +import Control.State.Transition (Embed, Environment, IRC (IRC), PredicateFailure, STS(..), Signal, State, TRC (TRC), initialRules, judgmentContext, trans, - transitionRules, wrapFailed) + transitionRules, wrapFailed, wrapEvent) import Control.State.Transition.Generator (HasTrace, envGen, genTrace, sigGen) import Control.State.Transition.Trace (TraceOrder (OldestFirst), traceSignals) @@ -57,6 +57,7 @@ instance STS UTXOWS where instance Embed UTXOW UTXOWS where wrapFailed = UtxowFailure + wrapEvent = id instance HasTrace UTXOWS where envGen = envGen @UTXOW diff --git a/byron/ledger/executable-spec/src/Byron/Spec/Ledger/Update.hs b/byron/ledger/executable-spec/src/Byron/Spec/Ledger/Update.hs index 1c22a5421af..3e122de07bd 100644 --- a/byron/ledger/executable-spec/src/Byron/Spec/Ledger/Update.hs +++ b/byron/ledger/executable-spec/src/Byron/Spec/Ledger/Update.hs @@ -465,7 +465,6 @@ instance STS UPV where type Signal UPV = UProp type PredicateFailure UPV = UpvPredicateFailure - initialRules = [] transitionRules = [ do @@ -500,9 +499,11 @@ instance STS UPV where instance Embed UPPVV UPV where wrapFailed = UPPVVFailure + wrapEvent = id instance Embed UPSVV UPV where wrapFailed = UPSVVFailure + wrapEvent = id data UPREG deriving (Generic, Data, Typeable) -- | These `PredicateFailure`s are all throwable. @@ -544,6 +545,7 @@ instance STS UPREG where instance Embed UPV UPREG where wrapFailed = UPVFailure + wrapEvent = id ------------------------------------------------------------------------ -- Update voting @@ -669,6 +671,7 @@ instance STS UPVOTE where instance Embed ADDVOTE UPVOTE where wrapFailed = ADDVOTEFailure + wrapEvent = id ------------------------------------------------------------------------ -- Update voting @@ -810,6 +813,7 @@ instance STS UPEND where instance Embed FADS UPEND where wrapFailed = error "No possible failures in FADS" + wrapEvent = id ------------------------------------------------------------------------ -- Update interface @@ -981,6 +985,7 @@ instance STS UPIREG where instance Embed UPREG UPIREG where wrapFailed = UPREGFailure + wrapEvent = id instance HasTrace UPIREG where @@ -1364,6 +1369,7 @@ instance STS UPIVOTE where instance Embed UPVOTE UPIVOTE where wrapFailed = UPVOTEFailure + wrapEvent = id data APPLYVOTES deriving (Generic, Data, Typeable) @@ -1393,6 +1399,7 @@ instance STS APPLYVOTES where instance Embed UPIVOTE APPLYVOTES where wrapFailed = UpivoteFailure + wrapEvent = id data UPIVOTES deriving (Generic, Data, Typeable) @@ -1451,6 +1458,7 @@ instance STS UPIVOTES where instance Embed APPLYVOTES UPIVOTES where wrapFailed = ApplyVotesFailure + wrapEvent = id instance HasTrace UPIVOTES where @@ -1590,6 +1598,7 @@ instance STS UPIEND where instance Embed UPEND UPIEND where wrapFailed = UPENDFailure + wrapEvent = id -- | Given a list of protocol versions and keys endorsing those versions, -- generate a protocol-version endorsement, or 'Nothing' if the list of @@ -1632,6 +1641,7 @@ instance STS PVBUMP where type Signal PVBUMP = () type PredicateFailure PVBUMP = PvbumpPredicateFailure + initialRules = [] transitionRules = [ do @@ -1691,6 +1701,7 @@ instance STS UPIEC where instance Embed PVBUMP UPIEC where wrapFailed = PVBUMPFailure + wrapEvent = id -- | Generate an optional update-proposal and a list of votes, given an update -- environment and state. diff --git a/byron/ledger/executable-spec/test/Test/Byron/Spec/Ledger/Delegation/Properties.hs b/byron/ledger/executable-spec/test/Test/Byron/Spec/Ledger/Delegation/Properties.hs index 15006d60784..86fe751ac38 100644 --- a/byron/ledger/executable-spec/test/Test/Byron/Spec/Ledger/Delegation/Properties.hs +++ b/byron/ledger/executable-spec/test/Test/Byron/Spec/Ledger/Delegation/Properties.hs @@ -41,7 +41,7 @@ import Lens.Micro.TH (makeLenses) import Control.State.Transition (Embed, Environment, IRC (IRC), PredicateFailure, STS, Signal, State, TRC (TRC), applySTS, initialRules, judgmentContext, trans, - transitionRules, wrapFailed, (?!)) + transitionRules, wrapFailed, (?!), wrapEvent) import Control.State.Transition.Generator (HasSizeInfo, HasTrace, SignalGenerator, TraceProfile (TraceProfile), classifySize, classifyTraceLength, envGen, failures, isTrivial, nonTrivialTrace, proportionOfValidSignals, sigGen, @@ -132,6 +132,7 @@ instance STS DBLOCK where instance Embed DELEG DBLOCK where wrapFailed = DPF + wrapEvent = id -- | Check that all the delegation certificates in the trace were correctly -- applied. diff --git a/byron/ledger/executable-spec/test/Test/Byron/Spec/Ledger/Update/Properties.hs b/byron/ledger/executable-spec/test/Test/Byron/Spec/Ledger/Update/Properties.hs index 95543ed0748..94cb65e1555 100644 --- a/byron/ledger/executable-spec/test/Test/Byron/Spec/Ledger/Update/Properties.hs +++ b/byron/ledger/executable-spec/test/Test/Byron/Spec/Ledger/Update/Properties.hs @@ -36,7 +36,7 @@ import Numeric.Natural (Natural) import Control.State.Transition (Embed, Environment, IRC (IRC), PredicateFailure, STS, Signal, State, TRC (TRC), initialRules, judgmentContext, trans, - transitionRules, wrapFailed, (?!)) + transitionRules, wrapFailed, (?!), wrapEvent) import Control.State.Transition.Generator (HasTrace, SignalGenerator, envGen, randomTraceOfSize, ratio, sigGen, trace, traceLengthsAreClassified, traceOfLength) @@ -351,12 +351,15 @@ instance STS UBLOCK where instance Embed UPIREG UBLOCK where wrapFailed = UPIREGFailure + wrapEvent = id instance Embed UPIVOTES UBLOCK where wrapFailed = UPIVOTESFailure + wrapEvent = id instance Embed UPIEND UBLOCK where wrapFailed = UPIENDFailure + wrapEvent = id instance HasTrace UBLOCK where envGen _ = diff --git a/byron/ledger/impl/test/Test/Cardano/Chain/Update/Gen.hs b/byron/ledger/impl/test/Test/Cardano/Chain/Update/Gen.hs index fea96c4afbb..456cdb37d0a 100644 --- a/byron/ledger/impl/test/Test/Cardano/Chain/Update/Gen.hs +++ b/byron/ledger/impl/test/Test/Cardano/Chain/Update/Gen.hs @@ -250,6 +250,6 @@ genEndorsementError = Endorsement.MultipleProposalsForProtocolVersion <$> genProtocolVersion genRegistrationTooLarge :: Gen (Registration.TooLarge Int) -genRegistrationTooLarge = Registration.TooLarge +genRegistrationTooLarge = Registration.TooLarge <$> Gen.int Range.constantBounded <*> Gen.int Range.constantBounded diff --git a/cardano-ledger-core/src/Cardano/Ledger/Rules/ValidationMode.hs b/cardano-ledger-core/src/Cardano/Ledger/Rules/ValidationMode.hs index 5652542a874..cba9cbcf9cf 100644 --- a/cardano-ledger-core/src/Cardano/Ledger/Rules/ValidationMode.hs +++ b/cardano-ledger-core/src/Cardano/Ledger/Rules/ValidationMode.hs @@ -29,7 +29,7 @@ applySTSValidateSuchThat :: RuleContext rtype s -> m (Either [[PredicateFailure s]] (State s)) applySTSValidateSuchThat cond ctx = - applySTSOpts opts ctx <&> \case + applySTSOpts EPDiscard opts ctx <&> \case (st, []) -> Right st (_, pfs) -> Left pfs where diff --git a/semantics/executable-spec/small-steps.cabal b/semantics/executable-spec/small-steps.cabal index 585e7e125a4..a26dac2e16e 100644 --- a/semantics/executable-spec/small-steps.cabal +++ b/semantics/executable-spec/small-steps.cabal @@ -69,6 +69,7 @@ library , strict-containers , text , transformers >= 0.5 + , writer-cps-mtl -- IOHK deps , cardano-crypto-class , cardano-binary diff --git a/semantics/executable-spec/src/Control/State/Transition/Extended.hs b/semantics/executable-spec/src/Control/State/Transition/Extended.hs index 9f072b0dd48..340f6a194fb 100644 --- a/semantics/executable-spec/src/Control/State/Transition/Extended.hs +++ b/semantics/executable-spec/src/Control/State/Transition/Extended.hs @@ -38,12 +38,18 @@ module Control.State.Transition.Extended (?!), (?!:), Label, + SingEP(..), + EventPolicy(..), + EventReturnType, + EventConstraintType, labeledPred, labeledPredE, failBecause, judgmentContext, trans, liftSTS, + tellEvent, + tellEvents, -- * Apply STS AssertionPolicy (..), @@ -71,17 +77,20 @@ import Control.Monad (when) import Control.Monad.Except (MonadError (..)) import Control.Monad.Free.Church import Control.Monad.Identity (Identity (..)) -import Control.Monad.Trans.Class (lift) -import Control.Monad.Trans.State.Strict (modify, runStateT) -import qualified Control.Monad.Trans.State.Strict as MonadState +import Control.Monad.Trans.Class (lift, MonadTrans) +import Control.Monad.Trans.State.Strict (StateT(..)) +import Control.Monad.Writer.CPS (WriterT, runWriterT) +import Control.Monad.Writer.Class (MonadWriter (..)) +import Control.Monad.State.Class (MonadState (..), modify) import Data.Data (Data, Typeable) import Data.Default.Class (Default, def) import Data.Foldable (find, traverse_) -import Data.Functor ((<&>)) -import Data.Kind (Type) +import Data.Functor ((<&>), ($>)) +import Data.Kind (Type, Constraint) import Data.Proxy (Proxy (..)) import Data.Typeable (typeRep) import NoThunks.Class (NoThunks (..)) +import Data.Void (Void) data RuleType = Initial @@ -178,6 +187,11 @@ class type BaseM a = Identity + -- | Event type. + + type Event a :: Type + type Event a = Void + -- | Descriptive type for the possible failures which might cause a transition -- to fail. -- @@ -215,9 +229,37 @@ class class (STS sub, BaseM sub ~ BaseM super) => Embed sub super where -- | Wrap a predicate failure of the subsystem in a failure of the super-system. wrapFailed :: PredicateFailure sub -> PredicateFailure super + wrapEvent :: Event sub -> Event super instance STS sts => Embed sts sts where wrapFailed = id + wrapEvent = id + +data EventPolicy + = EventPolicyReturn + | EventPolicyDiscard + +data SingEP ep where + EPReturn :: SingEP 'EventPolicyReturn + EPDiscard :: SingEP 'EventPolicyDiscard + +type family EventReturnType ep sts a :: Type where + EventReturnType 'EventPolicyReturn sts a = (a, [Event sts]) + EventReturnType _ _ a = a + +type family EventConstraintType e sts m :: Constraint where + EventConstraintType 'EventPolicyReturn sts m = MonadWriter [Event sts] m + EventConstraintType _ _ _ = () + +discardEvents :: forall ep a. SingEP ep -> forall s. EventReturnType ep s a -> a +discardEvents ep = case ep of + EPReturn -> fst + EPDiscard -> id + +getEvents :: forall ep. SingEP ep -> forall s a. EventReturnType ep s a -> [Event s] +getEvents ep ert = case ep of + EPReturn -> snd ert + EPDiscard -> [] data Clause sts (rtype :: RuleType) a where Lift :: @@ -234,6 +276,10 @@ data Clause sts (rtype :: RuleType) a where -- Subsequent computation with state introduced (State sub -> a) -> Clause sts rtype a + Writer :: + [Event sts] -> + a -> + Clause sts rtype a Predicate :: [Label] -> Either e a -> @@ -330,32 +376,33 @@ data ApplySTSOpts = ApplySTSOpts asoValidation :: ValidationPolicy } -type STSInterpreter = +type STSInterpreter ep = forall s m rtype. (STS s, RuleTypeRep rtype, m ~ BaseM s) => RuleContext rtype s -> - m (State s, [[PredicateFailure s]]) + m (EventReturnType ep s (State s, [[PredicateFailure s]])) -type RuleInterpreter = +type RuleInterpreter ep = forall s m rtype. (STS s, RuleTypeRep rtype, m ~ BaseM s) => RuleContext rtype s -> Rule s rtype (State s) -> - m (State s, [PredicateFailure s]) + m (EventReturnType ep s (State s, [PredicateFailure s])) -- | Apply an STS with options. Note that this returns both the final state and -- the list of predicate failures. applySTSOpts :: - forall s m rtype. + forall s m rtype ep. (STS s, RuleTypeRep rtype, m ~ BaseM s) => + SingEP ep -> ApplySTSOpts -> RuleContext rtype s -> - m (State s, [[PredicateFailure s]]) -applySTSOpts ApplySTSOpts {asoAssertions, asoValidation} ctx = - let goRule :: RuleInterpreter - goRule = applyRuleInternal asoValidation goSTS - goSTS :: STSInterpreter - goSTS = applySTSInternal asoAssertions goRule + m (EventReturnType ep s (State s, [[PredicateFailure s]])) +applySTSOpts ep ApplySTSOpts {asoAssertions, asoValidation} ctx = + let goRule :: RuleInterpreter ep + goRule = applyRuleInternal ep asoValidation goSTS + goSTS :: STSInterpreter ep + goSTS = applySTSInternal ep asoAssertions goRule in goSTS ctx applySTS :: @@ -364,7 +411,7 @@ applySTS :: RuleContext rtype s -> m (Either [[PredicateFailure s]] (State s)) applySTS ctx = - applySTSOpts defaultOpts ctx <&> \case + applySTSOpts EPDiscard defaultOpts ctx <&> \case (st, []) -> Right st (_, pfs) -> Left pfs where @@ -394,7 +441,7 @@ reapplySTS :: RuleContext rtype s -> m (State s) reapplySTS ctx = - applySTSOpts defaultOpts ctx <&> fst + applySTSOpts EPDiscard defaultOpts ctx <&> fst where defaultOpts = ApplySTSOpts @@ -408,7 +455,7 @@ applySTSIndifferently :: RuleContext rtype s -> m (State s, [[PredicateFailure s]]) applySTSIndifferently = - applySTSOpts opts + applySTSOpts EPDiscard opts where opts = ApplySTSOpts @@ -416,22 +463,46 @@ applySTSIndifferently = asoValidation = ValidateAll } +newtype RuleEventLoggerT s m a = RuleEventLoggerT (StateT [PredicateFailure s] (WriterT [Event s] m) a) + deriving (Monad, Applicative, Functor) + + +deriving instance (e ~ [Event s], Monad m) => MonadWriter e (RuleEventLoggerT s m) +deriving instance (f ~ [PredicateFailure s], Monad m) => MonadState f (RuleEventLoggerT s m) + +instance MonadTrans (RuleEventLoggerT s) where + lift = RuleEventLoggerT . lift . lift + +runRuleEventLoggerT :: forall s m a. RuleEventLoggerT s m a -> [PredicateFailure s] -> m ((a, [PredicateFailure s]), [Event s]) +runRuleEventLoggerT (RuleEventLoggerT m) s = runWriterT $ runStateT m s + -- | Apply a rule even if its predicates fail. -- -- If the rule successfully applied, the list of predicate failures will be -- empty. applyRuleInternal :: - forall s m rtype. + forall (ep :: EventPolicy) s m rtype. (STS s, RuleTypeRep rtype, m ~ BaseM s) => + SingEP ep -> ValidationPolicy -> -- | Interpreter for subsystems - STSInterpreter -> + STSInterpreter ep -> RuleContext rtype s -> Rule s rtype (State s) -> - m (State s, [PredicateFailure s]) -applyRuleInternal vp goSTS jc r = flip runStateT [] $ foldF runClause r + m (EventReturnType ep s (State s, [PredicateFailure s])) +applyRuleInternal ep vp goSTS jc r = + case ep of + EPReturn -> flip (runRuleEventLoggerT @s) [] $ foldF runClause r + EPDiscard -> flip runStateT [] $ foldF runClause r where - runClause :: Clause s rtype a -> MonadState.StateT [PredicateFailure s] m a + runClause :: forall f t a. + ( f ~ t m + , MonadState [PredicateFailure s] f + , EventConstraintType ep s f + , MonadTrans t + ) + => Clause s rtype a + -> t m a runClause (Lift f next) = next <$> lift f runClause (GetCtx next) = pure $ next jc runClause (Predicate lbls cond orElse val) = @@ -442,38 +513,52 @@ applyRuleInternal vp goSTS jc r = flip runStateT [] $ foldF runClause r Right x -> pure x else pure val runClause (SubTrans (subCtx :: RuleContext _rtype sub) next) = do - (ss, sfails) <- lift $ goSTS subCtx + s <- lift $ goSTS subCtx + let ss :: State sub + sfails :: [[PredicateFailure sub]] + (ss, sfails) = (discardEvents ep @sub) s traverse_ (\a -> modify (a :)) $ wrapFailed @sub @s <$> concat sfails + runClause $ Writer (wrapEvent @sub @s <$> getEvents ep @sub @(State sub, [[PredicateFailure sub]]) s) () pure $ next ss - + runClause (Writer w a) = case ep of + EPReturn -> tell w $> a + EPDiscard -> pure a validateIf lbls = case vp of ValidateAll -> True ValidateNone -> False ValidateSuchThat f -> f lbls applySTSInternal :: - forall s m rtype. + forall s m rtype ep. (STS s, RuleTypeRep rtype, m ~ BaseM s) => + SingEP ep -> AssertionPolicy -> -- | Interpreter for rules - RuleInterpreter -> + RuleInterpreter ep -> RuleContext rtype s -> - m (State s, [[PredicateFailure s]]) -applySTSInternal ap goRule ctx = + m (EventReturnType ep s (State s, [[PredicateFailure s]])) +applySTSInternal ep ap goRule ctx = successOrFirstFailure <$> applySTSInternal' rTypeRep ctx where + successOrFirstFailure :: + [EventReturnType ep s (State s, [PredicateFailure s])] + -> EventReturnType ep s (State s, [[PredicateFailure s]]) successOrFirstFailure xs = - case find (null . snd) xs of + case find (\x -> null $ snd $ (discardEvents ep @s x :: (State s, [PredicateFailure s]))) xs of Nothing -> case xs of [] -> error "applySTSInternal was called with an empty set of rules" - (s, _) : _ -> (s, snd <$> xs) - Just (s, _) -> (s, []) + s' : _ -> case ep of + EPDiscard -> (fst s', snd <$> xs) + EPReturn -> ((fst $ fst s', (snd . fst) <$> xs), snd s') + Just s' -> case ep of + EPDiscard -> (fst s', []) + EPReturn -> ((fst $ fst s', []), snd s') applySTSInternal' :: SRuleType rtype -> RuleContext rtype s -> - m [(State s, [PredicateFailure s])] + m [EventReturnType ep s (State s, [PredicateFailure s])] applySTSInternal' SInitial env = goRule env `traverse` initialRules applySTSInternal' STransition jc = do @@ -498,7 +583,7 @@ applySTSInternal ap goRule ctx = res <- goRule jc `traverse` transitionRules -- We only care about running postconditions if the state transition was -- successful. - !_ <- case (assertPost ap, successOrFirstFailure res) of + !_ <- case (assertPost ap, discardEvents ep @s (successOrFirstFailure res) :: (State s, [[PredicateFailure s]])) of (True, (st, [])) -> sfor_ (assertions @s) $! ( \case @@ -588,3 +673,13 @@ straverse_ f = foldr c (pure ()) sfor_ :: (Foldable t, Applicative f) => t a -> (a -> f b) -> f () {-# INLINE sfor_ #-} sfor_ = flip straverse_ + +tellEvent :: + Event sts -> + Rule sts ctx () +tellEvent e = tellEvents [e] + +tellEvents :: + [Event sts] -> + Rule sts ctx () +tellEvents es = liftF $ Writer es () diff --git a/semantics/small-steps-test/src/Control/State/Transition/Trace.hs b/semantics/small-steps-test/src/Control/State/Transition/Trace.hs index 28ad95b9b26..31f0c3db1a8 100644 --- a/semantics/small-steps-test/src/Control/State/Transition/Trace.hs +++ b/semantics/small-steps-test/src/Control/State/Transition/Trace.hs @@ -496,7 +496,7 @@ applySTSTest :: RuleContext rtype s -> m (Either [[PredicateFailure s]] (State s)) applySTSTest ctx = - applySTSOpts defaultOpts ctx <&> \case + applySTSOpts EPDiscard defaultOpts ctx <&> \case (st, []) -> Right st (_, pfs) -> Left pfs where diff --git a/semantics/small-steps-test/test/Control/State/Transition/Examples/CommitReveal.hs b/semantics/small-steps-test/test/Control/State/Transition/Examples/CommitReveal.hs index d9f282422ac..a41a3ea7086 100644 --- a/semantics/small-steps-test/test/Control/State/Transition/Examples/CommitReveal.hs +++ b/semantics/small-steps-test/test/Control/State/Transition/Examples/CommitReveal.hs @@ -137,6 +137,7 @@ instance PredicateFailure (CR hashAlgo hashToDataMap commitData) = CRPredicateFailure hashAlgo hashToDataMap commitData + initialRules = [ pure $! CRSt diff --git a/semantics/small-steps-test/test/Control/State/Transition/Examples/GlobalSum.hs b/semantics/small-steps-test/test/Control/State/Transition/Examples/GlobalSum.hs index 8f3615ba9cd..eac6c332a5a 100644 --- a/semantics/small-steps-test/test/Control/State/Transition/Examples/GlobalSum.hs +++ b/semantics/small-steps-test/test/Control/State/Transition/Examples/GlobalSum.hs @@ -33,6 +33,7 @@ instance STS GSUM where type PredicateFailure GSUM = NoFailure + initialRules = [pure 0] transitionRules = diff --git a/semantics/small-steps-test/test/Control/State/Transition/Examples/Sum.hs b/semantics/small-steps-test/test/Control/State/Transition/Examples/Sum.hs index 2486f140131..cb621729bee 100644 --- a/semantics/small-steps-test/test/Control/State/Transition/Examples/Sum.hs +++ b/semantics/small-steps-test/test/Control/State/Transition/Examples/Sum.hs @@ -34,6 +34,7 @@ instance STS SUM where type PredicateFailure SUM = NoFailure + initialRules = [pure 0] transitionRules = diff --git a/shelley-ma/impl/src/Cardano/Ledger/ShelleyMA/Rules/Utxo.hs b/shelley-ma/impl/src/Cardano/Ledger/ShelleyMA/Rules/Utxo.hs index eceb56a9646..36ef249cc90 100644 --- a/shelley-ma/impl/src/Cardano/Ledger/ShelleyMA/Rules/Utxo.hs +++ b/shelley-ma/impl/src/Cardano/Ledger/ShelleyMA/Rules/Utxo.hs @@ -390,6 +390,7 @@ instance Embed (PPUP era) (UTXO era) where wrapFailed = UpdateFailure + wrapEvent = id -------------------------------------------------------------------------------- -- Serialisation diff --git a/shelley-ma/impl/src/Cardano/Ledger/ShelleyMA/Rules/Utxow.hs b/shelley-ma/impl/src/Cardano/Ledger/ShelleyMA/Rules/Utxow.hs index 142f27dd592..528aa7b2657 100644 --- a/shelley-ma/impl/src/Cardano/Ledger/ShelleyMA/Rules/Utxow.hs +++ b/shelley-ma/impl/src/Cardano/Ledger/ShelleyMA/Rules/Utxow.hs @@ -66,6 +66,7 @@ instance type PredicateFailure (UTXOW era) = UtxowPredicateFailure era + transitionRules = [shelleyStyleWitness witsVKeyNeeded id] -- The ShelleyMA Era uses the same PredicateFailure type @@ -80,12 +81,15 @@ instance Embed (UTXO era) (UTXOW era) where wrapFailed = UtxoFailure + wrapEvent = id instance ( Era era, STS (UTXOW era), - PredicateFailure (Core.EraRule "UTXOW" era) ~ UtxowPredicateFailure era + PredicateFailure (Core.EraRule "UTXOW" era) ~ UtxowPredicateFailure era, + Event (Core.EraRule "UTXOW" era) ~ Event (UTXOW era) ) => Embed (UTXOW era) (Shelley.LEDGER era) where wrapFailed = Shelley.UtxowFailure + wrapEvent = Shelley.UtxowEvent diff --git a/shelley-ma/shelley-ma-test/src/Test/Cardano/Ledger/TranslationTools.hs b/shelley-ma/shelley-ma-test/src/Test/Cardano/Ledger/TranslationTools.hs index b1829ade9ab..b3c52e54799 100644 --- a/shelley-ma/shelley-ma-test/src/Test/Cardano/Ledger/TranslationTools.hs +++ b/shelley-ma/shelley-ma-test/src/Test/Cardano/Ledger/TranslationTools.hs @@ -79,7 +79,7 @@ decodeTestAnn _ x = let bytes = serialize x decoded = decodeAnnotator mempty fromCBOR bytes :: Either DecoderError b in case decoded of - Left e -> assertFailure $ + Left e -> assertFailure $ "\nerror: " <> show e <> "\nbytes: " <> show (B16.encode bytes) <> "\n" Right _ -> return () diff --git a/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Bbody.hs b/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Bbody.hs index 91289e937d6..d223b57b7c4 100644 --- a/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Bbody.hs +++ b/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Bbody.hs @@ -16,6 +16,7 @@ module Shelley.Spec.Ledger.STS.Bbody BbodyState (..), BbodyEnv (..), BbodyPredicateFailure (..), + BbodyEvent (..), PredicateFailure, State, ) @@ -93,6 +94,9 @@ data BbodyPredicateFailure era | LedgersFailure (PredicateFailure (Core.EraRule "LEDGERS" era)) -- Subtransition Failures deriving (Generic) +data BbodyEvent era + = LedgersEvent (Event (Core.EraRule "LEDGERS" era)) + deriving stock instance ( Era era, Show (PredicateFailure (Core.EraRule "LEDGERS" era)) @@ -138,6 +142,8 @@ instance type PredicateFailure (BBODY era) = BbodyPredicateFailure era + type Event (BBODY era) = BbodyEvent era + initialRules = [] transitionRules = [bbodyTransition] @@ -193,6 +199,7 @@ bbodyTransition = ) instance + forall era ledgers. ( Era era, BaseM ledgers ~ ShelleyBase, ledgers ~ Core.EraRule "LEDGERS" era, @@ -203,3 +210,4 @@ instance Embed ledgers (BBODY era) where wrapFailed = LedgersFailure + wrapEvent = LedgersEvent diff --git a/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Chain.hs b/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Chain.hs index 81552002053..bdc5ff45ee0 100644 --- a/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Chain.hs +++ b/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Chain.hs @@ -18,6 +18,7 @@ module Shelley.Spec.Ledger.STS.Chain ( CHAIN, ChainState (..), ChainPredicateFailure (..), + ChainEvent (..), PredicateFailure, AdaPots (..), initialShelleyState, @@ -72,6 +73,7 @@ import Data.Default.Class (Default, def) import Data.Foldable (fold) import Data.Map.Strict (Map) import qualified Data.Map.Strict as Map +import Data.Void (Void) import Data.Word (Word64) import GHC.Generics (Generic) import GHC.Records @@ -158,6 +160,12 @@ data ChainPredicateFailure era | PrtclSeqFailure !(PrtlSeqFailure (Crypto era)) -- Subtransition Failures deriving (Generic) +data ChainEvent era + = BbodyEvent !(Event (Core.EraRule "BBODY" era)) + | TickEvent !(Event (Core.EraRule "TICK" era)) + | TicknEvent !(Event (Core.EraRule "TICKN" era)) + | PrtclEvent !(Event (PRTCL (Crypto era))) + deriving stock instance ( Era era, Show (PredicateFailure (Core.EraRule "BBODY" era)), @@ -269,6 +277,7 @@ instance type BaseM (CHAIN era) = ShelleyBase type PredicateFailure (CHAIN era) = ChainPredicateFailure era + type Event (CHAIN era) = ChainEvent era initialRules = [] transitionRules = [chainTransition] @@ -412,30 +421,36 @@ instance ( Era era, Era era, STS (BBODY era), - PredicateFailure (Core.EraRule "BBODY" era) ~ BbodyPredicateFailure era + PredicateFailure (Core.EraRule "BBODY" era) ~ BbodyPredicateFailure era, + Event (Core.EraRule "BBODY" era) ~ Event (BBODY era) ) => Embed (BBODY era) (CHAIN era) where wrapFailed = BbodyFailure + wrapEvent = BbodyEvent instance ( Era era, Era era, - PredicateFailure (Core.EraRule "TICKN" era) ~ TicknPredicateFailure + PredicateFailure (Core.EraRule "TICKN" era) ~ TicknPredicateFailure, + Event (Core.EraRule "TICKN" era) ~ Void ) => Embed TICKN (CHAIN era) where wrapFailed = TicknFailure + wrapEvent = TicknEvent instance ( Era era, Era era, STS (TICK era), - PredicateFailure (Core.EraRule "TICK" era) ~ TickPredicateFailure era + PredicateFailure (Core.EraRule "TICK" era) ~ TickPredicateFailure era, + Event (Core.EraRule "TICK" era) ~ Void ) => Embed (TICK era) (CHAIN era) where wrapFailed = TickFailure + wrapEvent = TickEvent instance ( Era era, @@ -446,6 +461,7 @@ instance Embed (PRTCL c) (CHAIN era) where wrapFailed = PrtclFailure + wrapEvent = PrtclEvent data AdaPots = AdaPots { treasuryAdaPot :: Coin, diff --git a/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Delegs.hs b/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Delegs.hs index eb76bd6f4d7..90c40dae068 100644 --- a/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Delegs.hs +++ b/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Delegs.hs @@ -17,6 +17,7 @@ module Shelley.Spec.Ledger.STS.Delegs ( DELEGS, DelegsEnv (..), DelegsPredicateFailure (..), + DelegsEvent (..), PredicateFailure, ) where @@ -72,7 +73,7 @@ import Shelley.Spec.Ledger.LedgerState _pParams, _rewards, ) -import Shelley.Spec.Ledger.STS.Delpl (DELPL, DelplEnv (..), DelplPredicateFailure) +import Shelley.Spec.Ledger.STS.Delpl (DELPL, DelplEnv (..), DelplEvent, DelplPredicateFailure) import Shelley.Spec.Ledger.Tx (Tx (..)) import Shelley.Spec.Ledger.TxBody ( DCert (..), @@ -108,6 +109,9 @@ data DelegsPredicateFailure era | DelplFailure (PredicateFailure (Core.EraRule "DELPL" era)) -- Subtransition Failures deriving (Generic) +data DelegsEvent era + = DelplEvent (Event (Core.EraRule "DELPL" era)) + deriving stock instance ( Show (PredicateFailure (Core.EraRule "DELPL" era)) ) => @@ -136,6 +140,7 @@ instance type PredicateFailure (DELEGS era) = DelegsPredicateFailure era + type Event _ = DelegsEvent era transitionRules = [delegsTransition] @@ -257,8 +262,10 @@ delegsTransition = do instance ( Era era, STS (DELPL era), - PredicateFailure (Core.EraRule "DELPL" era) ~ DelplPredicateFailure era + PredicateFailure (Core.EraRule "DELPL" era) ~ DelplPredicateFailure era, + Event (Core.EraRule "DELPL" era) ~ DelplEvent era ) => Embed (DELPL era) (DELEGS era) where wrapFailed = DelplFailure + wrapEvent = DelplEvent diff --git a/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Delpl.hs b/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Delpl.hs index 9af49edc555..393b5906bc8 100644 --- a/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Delpl.hs +++ b/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Delpl.hs @@ -17,6 +17,7 @@ module Shelley.Spec.Ledger.STS.Delpl ( DELPL, DelplEnv (..), DelplPredicateFailure (..), + DelplEvent, PredicateFailure, ) where @@ -70,6 +71,10 @@ data DelplPredicateFailure era | DelegFailure (PredicateFailure (Core.EraRule "DELEG" era)) -- Subtransition Failures deriving (Generic) +data DelplEvent era + = PoolEvent (Event (POOL era)) + | DelegEvent (Event (DELEG era)) + deriving stock instance ( Eq (PredicateFailure (Core.EraRule "DELEG" era)), Eq (PredicateFailure (Core.EraRule "POOL" era)) @@ -106,6 +111,7 @@ instance type Environment (DELPL era) = DelplEnv era type BaseM (DELPL era) = ShelleyBase type PredicateFailure (DELPL era) = DelplPredicateFailure era + type Event (DELPL era) = DelplEvent era transitionRules = [delplTransition] @@ -197,6 +203,7 @@ instance Embed (POOL era) (DELPL era) where wrapFailed = PoolFailure + wrapEvent = PoolEvent instance ( Era era, @@ -206,3 +213,4 @@ instance Embed (DELEG era) (DELPL era) where wrapFailed = DelegFailure + wrapEvent = DelegEvent diff --git a/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Epoch.hs b/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Epoch.hs index dc6fec09af9..35736bd27ab 100644 --- a/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Epoch.hs +++ b/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Epoch.hs @@ -206,6 +206,7 @@ instance Embed (SNAP era) (EPOCH era) where wrapFailed = SnapFailure + wrapEvent = id instance ( Era era, @@ -215,6 +216,7 @@ instance Embed (POOLREAP era) (EPOCH era) where wrapFailed = PoolReapFailure + wrapEvent = id instance ( Era era, @@ -224,3 +226,4 @@ instance Embed (UPEC era) (EPOCH era) where wrapFailed = UpecFailure + wrapEvent = id diff --git a/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Ledger.hs b/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Ledger.hs index 8aaf6117588..1bc94d59ef8 100644 --- a/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Ledger.hs +++ b/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Ledger.hs @@ -19,6 +19,8 @@ module Shelley.Spec.Ledger.STS.Ledger ( LEDGER, LedgerEnv (..), LedgerPredicateFailure (..), + LedgerEvent (..), + Event, PredicateFailure, ) where @@ -61,7 +63,7 @@ import Shelley.Spec.Ledger.LedgerState PState (..), UTxOState (..), ) -import Shelley.Spec.Ledger.STS.Delegs (DELEGS, DelegsEnv (..), DelegsPredicateFailure) +import Shelley.Spec.Ledger.STS.Delegs (DELEGS, DelegsEnv (..), DelegsEvent, DelegsPredicateFailure) import Shelley.Spec.Ledger.STS.Utxo ( UtxoEnv (..), ) @@ -84,6 +86,10 @@ data LedgerPredicateFailure era | DelegsFailure (PredicateFailure (Core.EraRule "DELEGS" era)) -- Subtransition Failures deriving (Generic) +data LedgerEvent era + = UtxowEvent (Event (Core.EraRule "UTXOW" era)) + | DelegsEvent (Event (Core.EraRule "DELEGS" era)) + deriving stock instance ( Show (PredicateFailure (Core.EraRule "DELEGS" era)), Show (PredicateFailure (Core.EraRule "UTXOW" era)), @@ -162,6 +168,7 @@ instance type Environment (LEDGER era) = LedgerEnv era type BaseM (LEDGER era) = ShelleyBase type PredicateFailure (LEDGER era) = LedgerPredicateFailure era + type Event (LEDGER era) = LedgerEvent era initialRules = [] transitionRules = [ledgerTransition] @@ -224,17 +231,21 @@ ledgerTransition = do instance ( Era era, STS (DELEGS era), - PredicateFailure (Core.EraRule "DELEGS" era) ~ DelegsPredicateFailure era + PredicateFailure (Core.EraRule "DELEGS" era) ~ DelegsPredicateFailure era, + Event (Core.EraRule "DELEGS" era) ~ DelegsEvent era ) => Embed (DELEGS era) (LEDGER era) where wrapFailed = DelegsFailure + wrapEvent = DelegsEvent instance ( Era era, STS (UTXOW era), - PredicateFailure (Core.EraRule "UTXOW" era) ~ UtxowPredicateFailure era + PredicateFailure (Core.EraRule "UTXOW" era) ~ UtxowPredicateFailure era, + Event (Core.EraRule "UTXOW" era) ~ Event (UTXOW era) ) => Embed (UTXOW era) (LEDGER era) where wrapFailed = UtxowFailure + wrapEvent = UtxowEvent diff --git a/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Ledgers.hs b/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Ledgers.hs index c2bf099b2d5..b3c13dabfb3 100644 --- a/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Ledgers.hs +++ b/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Ledgers.hs @@ -15,6 +15,7 @@ module Shelley.Spec.Ledger.STS.Ledgers ( LEDGERS, LedgersEnv (..), LedgersPredicateFailure (..), + LedgersEvent (..), PredicateFailure, ) where @@ -51,6 +52,7 @@ import Shelley.Spec.Ledger.LedgerState import Shelley.Spec.Ledger.STS.Ledger ( LEDGER, LedgerEnv (..), + LedgerEvent, LedgerPredicateFailure, ) import Shelley.Spec.Ledger.TxBody (EraIndependentTxBody) @@ -67,6 +69,9 @@ data LedgersPredicateFailure era = LedgerFailure (PredicateFailure (Core.EraRule "LEDGER" era)) -- Subtransition Failures deriving (Generic) +data LedgersEvent era + = LedgerEvent (Event (Core.EraRule "LEDGER" era)) + deriving stock instance ( ShelleyBased era, Show (PredicateFailure (Core.EraRule "LEDGER" era)) @@ -118,6 +123,7 @@ instance type Environment (LEDGERS era) = LedgersEnv era type BaseM (LEDGERS era) = ShelleyBase type PredicateFailure (LEDGERS era) = LedgersPredicateFailure era + type Event (LEDGERS era) = LedgersEvent era transitionRules = [ledgersTransition] @@ -147,8 +153,10 @@ ledgersTransition = do instance ( Era era, STS (LEDGER era), - PredicateFailure (Core.EraRule "LEDGER" era) ~ LedgerPredicateFailure era + PredicateFailure (Core.EraRule "LEDGER" era) ~ LedgerPredicateFailure era, + Event (Core.EraRule "LEDGER" era) ~ LedgerEvent era ) => Embed (LEDGER era) (LEDGERS era) where wrapFailed = LedgerFailure + wrapEvent = LedgerEvent diff --git a/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/NewEpoch.hs b/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/NewEpoch.hs index 5aa777b4469..f93b67cf5d6 100644 --- a/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/NewEpoch.hs +++ b/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/NewEpoch.hs @@ -186,6 +186,7 @@ instance Embed (EPOCH era) (NEWEPOCH era) where wrapFailed = EpochFailure + wrapEvent = id instance ( Era era, @@ -195,3 +196,4 @@ instance Embed (MIR era) (NEWEPOCH era) where wrapFailed = MirFailure + wrapEvent = id diff --git a/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Overlay.hs b/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Overlay.hs index 953d0c63063..9430eef0efb 100644 --- a/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Overlay.hs +++ b/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Overlay.hs @@ -293,3 +293,4 @@ instance Embed (OCERT crypto) (OVERLAY crypto) where wrapFailed = OcertFailure + wrapEvent = id diff --git a/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Pool.hs b/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Pool.hs index 5518b6bcc42..dd0f037e643 100644 --- a/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Pool.hs +++ b/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Pool.hs @@ -14,6 +14,7 @@ module Shelley.Spec.Ledger.STS.Pool ( POOL, + PoolEvent (..), PoolEnv (..), PredicateFailure, PoolPredicateFailure (..), @@ -52,6 +53,7 @@ import Control.State.Transition failBecause, judgmentContext, liftSTS, + tellEvent, (?!), ) import qualified Data.ByteString as BS @@ -121,9 +123,14 @@ instance type BaseM (POOL era) = ShelleyBase type PredicateFailure (POOL era) = PoolPredicateFailure era + type Event (POOL era) = PoolEvent era transitionRules = [poolDelegationTransition] +data PoolEvent era + = RegisterPool (KeyHash 'StakePool (Crypto era)) + | ReregisterPool (KeyHash 'StakePool (Crypto era)) + instance (Typeable era, Era era) => ToCBOR (PoolPredicateFailure era) @@ -209,13 +216,15 @@ poolDelegationTransition = do let hk = _poolId poolParam if eval (hk ∉ dom stpools) - then -- register new, Pool-Reg - + then do + -- register new, Pool-Reg + tellEvent $ RegisterPool hk pure $ ps { _pParams = eval (_pParams ps ∪ singleton hk poolParam) } else do + tellEvent $ ReregisterPool hk pure $ ps { _fPParams = eval (_fPParams ps ⨃ singleton hk poolParam), diff --git a/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Prtcl.hs b/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Prtcl.hs index 0f745662a58..38cb7c32dfb 100644 --- a/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Prtcl.hs +++ b/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Prtcl.hs @@ -199,6 +199,7 @@ instance Embed (OVERLAY crypto) (PRTCL crypto) where wrapFailed = OverlayFailure + wrapEvent = id instance ( Crypto crypto, @@ -209,6 +210,7 @@ instance Embed (UPDN crypto) (PRTCL crypto) where wrapFailed = UpdnFailure + wrapEvent = id data PrtlSeqFailure crypto = WrongSlotIntervalPrtclSeq diff --git a/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Tick.hs b/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Tick.hs index 41e41f99556..5ad6adde606 100644 --- a/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Tick.hs +++ b/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Tick.hs @@ -192,6 +192,7 @@ instance Embed (NEWEPOCH era) (TICK era) where wrapFailed = NewEpochFailure + wrapEvent = id instance ( Era era, @@ -201,6 +202,7 @@ instance Embed (RUPD era) (TICK era) where wrapFailed = RupdFailure + wrapEvent = id {------------------------------------------------------------------------------ -- TICKF transition @@ -270,3 +272,4 @@ instance Embed (NEWEPOCH era) (TICKF era) where wrapFailed = TickfNewEpochFailure + wrapEvent = id diff --git a/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Upec.hs b/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Upec.hs index 018d9b05814..cf94e545059 100644 --- a/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Upec.hs +++ b/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Upec.hs @@ -156,3 +156,4 @@ instance Embed (NEWPP era) (UPEC era) where wrapFailed = NewPpFailure + wrapEvent = id diff --git a/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Utxo.hs b/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Utxo.hs index e2988381780..9dd469e3a94 100644 --- a/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Utxo.hs +++ b/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Utxo.hs @@ -73,6 +73,7 @@ import Control.State.Transition judgmentContext, liftSTS, trans, + wrapEvent, wrapFailed, (?!), ) @@ -438,3 +439,4 @@ instance Embed (PPUP era) (UTXO era) where wrapFailed = UpdateFailure + wrapEvent = id diff --git a/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Utxow.hs b/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Utxow.hs index 0660ea1faff..c96874762e2 100644 --- a/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Utxow.hs +++ b/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Utxow.hs @@ -75,6 +75,7 @@ import Control.State.Transition judgmentContext, liftSTS, trans, + wrapEvent, wrapFailed, (?!), (?!:), @@ -143,6 +144,9 @@ data UtxowPredicateFailure era | InvalidMetadata deriving (Generic) +data UtxowEvent era + = UtxoEvent (Event (UTXO era)) + instance ( NoThunks (PredicateFailure (Core.EraRule "UTXO" era)), Era era @@ -387,6 +391,7 @@ instance Embed (UTXO era) (UTXOW era) where wrapFailed = UtxoFailure + wrapEvent = UtxoEvent instance ( -- Fix Core.Witnesses to the Shelley Era @@ -409,5 +414,6 @@ instance type Environment (UTXOW era) = UtxoEnv era type BaseM (UTXOW era) = ShelleyBase type PredicateFailure (UTXOW era) = UtxowPredicateFailure era + type Event _ = UtxowEvent era transitionRules = [shelleyStyleWitness witsVKeyNeeded id] initialRules = [initialLedgerStateUTXOW] diff --git a/shelley/chain-and-ledger/shelley-spec-ledger-test/src/Test/Shelley/Spec/Ledger/Generator/Trace/DCert.hs b/shelley/chain-and-ledger/shelley-spec-ledger-test/src/Test/Shelley/Spec/Ledger/Generator/Trace/DCert.hs index e04ae1166ea..f598acce690 100644 --- a/shelley/chain-and-ledger/shelley-spec-ledger-test/src/Test/Shelley/Spec/Ledger/Generator/Trace/DCert.hs +++ b/shelley/chain-and-ledger/shelley-spec-ledger-test/src/Test/Shelley/Spec/Ledger/Generator/Trace/DCert.hs @@ -31,6 +31,7 @@ import Control.State.Transition Environment, PredicateFailure, STS, + Event, Signal, State, TRC (..), @@ -39,7 +40,7 @@ import Control.State.Transition judgmentContext, trans, transitionRules, - wrapFailed, + wrapFailed, wrapEvent ) import Control.State.Transition.Trace (TraceOrder (OldestFirst), lastState, traceSignals) import qualified Control.State.Transition.Trace.Generator.QuickCheck as QC @@ -66,7 +67,7 @@ import Shelley.Spec.Ledger.API import Cardano.Ledger.BaseTypes (Globals, ShelleyBase) import Shelley.Spec.Ledger.Delegation.Certificates (isDeRegKey) import Cardano.Ledger.Keys (HasKeyRole (coerceKeyRole), asWitness) -import Shelley.Spec.Ledger.STS.Delpl (DelplPredicateFailure) +import Shelley.Spec.Ledger.STS.Delpl (DelplPredicateFailure, DelplEvent) import Cardano.Ledger.Slot (SlotNo (..)) import Shelley.Spec.Ledger.TxBody (Ix) import Shelley.Spec.Ledger.UTxO (totalDeposits) @@ -87,6 +88,9 @@ newtype CertsPredicateFailure era = CertsFailure (PredicateFailure (Core.EraRule "DELPL" era)) deriving (Generic) +newtype CertsEvent era + = CertsEvent (Event (Core.EraRule "DELPL" era)) + deriving stock instance ( Eq (PredicateFailure (Core.EraRule "DELPL" era)) ) => @@ -110,6 +114,7 @@ instance type State (CERTS era) = (DPState (Crypto era), Ix) type Signal (CERTS era) = Maybe (DCert (Crypto era), CertCred era) type PredicateFailure (CERTS era) = CertsPredicateFailure era + type Event (CERTS era) = CertsEvent era type BaseM (CERTS era) = ShelleyBase @@ -146,11 +151,13 @@ certsTransition = do instance ( Era era, STS (DELPL era), - PredicateFailure (Core.EraRule "DELPL" era) ~ DelplPredicateFailure era + PredicateFailure (Core.EraRule "DELPL" era) ~ DelplPredicateFailure era, + Event (Core.EraRule "DELPL" era) ~ DelplEvent era ) => Embed (DELPL era) (CERTS era) where wrapFailed = CertsFailure + wrapEvent = CertsEvent instance ( EraGen era, diff --git a/shelley/chain-and-ledger/shelley-spec-ledger-test/src/Test/Shelley/Spec/Ledger/Utils.hs b/shelley/chain-and-ledger/shelley-spec-ledger-test/src/Test/Shelley/Spec/Ledger/Utils.hs index 54109dc76c9..098d0d6f2b3 100644 --- a/shelley/chain-and-ledger/shelley-spec-ledger-test/src/Test/Shelley/Spec/Ledger/Utils.hs +++ b/shelley/chain-and-ledger/shelley-spec-ledger-test/src/Test/Shelley/Spec/Ledger/Utils.hs @@ -330,7 +330,7 @@ applySTSTest :: RuleContext rtype s -> m (Either [[PredicateFailure s]] (State s)) applySTSTest ctx = - applySTSOpts defaultOpts ctx <&> \case + applySTSOpts EPDiscard defaultOpts ctx <&> \case (st, []) -> Right st (_, pfs) -> Left pfs where From be9b8cc4ac04e893e37817676b0c21e7fc000191 Mon Sep 17 00:00:00 2001 From: Zachary Churchill Date: Thu, 8 Jul 2021 15:38:52 -0400 Subject: [PATCH 2/4] add sum of the deposits in a transaction event --- .../src/Shelley/Spec/Ledger/STS/Utxo.hs | 18 +++++++++++++++--- 1 file changed, 15 insertions(+), 3 deletions(-) diff --git a/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Utxo.hs b/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Utxo.hs index 9dd469e3a94..fe3516cf33f 100644 --- a/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Utxo.hs +++ b/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Utxo.hs @@ -18,6 +18,7 @@ module Shelley.Spec.Ledger.STS.Utxo ( UTXO, UtxoEnv (..), UtxoPredicateFailure (..), + UtxoEvent (..), PredicateFailure, ) where @@ -72,6 +73,7 @@ import Control.State.Transition TransitionRule, judgmentContext, liftSTS, + tellEvent, trans, wrapEvent, wrapFailed, @@ -83,6 +85,7 @@ import qualified Data.Map.Strict as Map import Data.Sequence.Strict (StrictSeq) import Data.Set (Set) import qualified Data.Set as Set +import Data.Void (Void) import Data.Word (Word8) import GHC.Generics (Generic) import GHC.Records (HasField (..)) @@ -128,6 +131,10 @@ data UtxoEnv era deriving instance Show (Core.PParams era) => Show (UtxoEnv era) +data UtxoEvent era + = TotalDeposits Coin + | UpdateEvent (Event (Core.EraRule "PPUP" era)) + data UtxoPredicateFailure era = BadInputsUTxO !(Set (TxIn (Crypto era))) -- The bad transaction inputs @@ -296,6 +303,7 @@ instance type Environment (UTXO era) = UtxoEnv era type BaseM (UTXO era) = ShelleyBase type PredicateFailure (UTXO era) = UtxoPredicateFailure era + type Event (UTXO era) = UtxoEvent era transitionRules = [utxoInductive] @@ -337,6 +345,7 @@ utxoInductive :: State (utxo era) ~ UTxOState era, Signal (utxo era) ~ Tx era, PredicateFailure (utxo era) ~ UtxoPredicateFailure era, + Event (utxo era) ~ UtxoEvent era, Environment (Core.EraRule "PPUP" era) ~ PPUPEnv era, State (Core.EraRule "PPUP" era) ~ PPUPState era, Signal (Core.EraRule "PPUP" era) ~ Maybe (Update era), @@ -421,7 +430,9 @@ utxoInductive = do let refunded = keyRefunds pp txb let txCerts = toList $ getField @"certs" txb - let depositChange = totalDeposits pp (`Map.notMember` stakepools) txCerts <-> refunded + let totalDeposits' = totalDeposits pp (`Map.notMember` stakepools) txCerts + tellEvent $ TotalDeposits totalDeposits' + let depositChange = totalDeposits' <-> refunded pure UTxOState @@ -434,9 +445,10 @@ utxoInductive = do instance ( Era era, STS (PPUP era), - PredicateFailure (Core.EraRule "PPUP" era) ~ PpupPredicateFailure era + PredicateFailure (Core.EraRule "PPUP" era) ~ PpupPredicateFailure era, + Event (Core.EraRule "PPUP" era) ~ Void ) => Embed (PPUP era) (UTXO era) where wrapFailed = UpdateFailure - wrapEvent = id + wrapEvent = UpdateEvent From 3eae38f824775c5a80b398fcd6c6e1d5b96059ce Mon Sep 17 00:00:00 2001 From: Zachary Churchill Date: Thu, 15 Jul 2021 17:05:13 -0700 Subject: [PATCH 3/4] default wrapEvent --- alonzo/impl/src/Cardano/Ledger/Alonzo/Rules/Utxo.hs | 1 - alonzo/impl/src/Cardano/Ledger/Alonzo/Rules/Utxos.hs | 1 - alonzo/impl/src/Cardano/Ledger/Alonzo/Rules/Utxow.hs | 1 - .../src/Byron/Spec/Chain/STS/Rule/BBody.hs | 5 +---- .../src/Byron/Spec/Chain/STS/Rule/Bupi.hs | 5 +---- .../src/Byron/Spec/Chain/STS/Rule/Chain.hs | 5 ----- .../src/Byron/Spec/Chain/STS/Rule/Epoch.hs | 1 - .../src/Byron/Spec/Chain/STS/Rule/Pbft.hs | 1 - .../src/Byron/Spec/Ledger/Delegation.hs | 5 ----- .../src/Byron/Spec/Ledger/STS/UTXOW.hs | 1 - .../src/Byron/Spec/Ledger/STS/UTXOWS.hs | 3 +-- .../executable-spec/src/Byron/Spec/Ledger/Update.hs | 11 ----------- .../Test/Byron/Spec/Ledger/Delegation/Properties.hs | 3 +-- .../test/Test/Byron/Spec/Ledger/Update/Properties.hs | 5 +---- .../src/Control/State/Transition/Extended.hs | 4 +++- .../impl/src/Cardano/Ledger/ShelleyMA/Rules/Utxo.hs | 1 - .../impl/src/Cardano/Ledger/ShelleyMA/Rules/Utxow.hs | 1 - .../src/Shelley/Spec/Ledger/STS/Epoch.hs | 3 --- .../src/Shelley/Spec/Ledger/STS/NewEpoch.hs | 2 -- .../src/Shelley/Spec/Ledger/STS/Overlay.hs | 1 - .../src/Shelley/Spec/Ledger/STS/Prtcl.hs | 2 -- .../src/Shelley/Spec/Ledger/STS/Tick.hs | 3 --- .../src/Shelley/Spec/Ledger/STS/Upec.hs | 1 - 23 files changed, 8 insertions(+), 58 deletions(-) diff --git a/alonzo/impl/src/Cardano/Ledger/Alonzo/Rules/Utxo.hs b/alonzo/impl/src/Cardano/Ledger/Alonzo/Rules/Utxo.hs index 569dc9791bf..e0106673f72 100644 --- a/alonzo/impl/src/Cardano/Ledger/Alonzo/Rules/Utxo.hs +++ b/alonzo/impl/src/Cardano/Ledger/Alonzo/Rules/Utxo.hs @@ -518,7 +518,6 @@ instance Embed (UTXOS era) (AlonzoUTXO era) where wrapFailed = UtxosFailure - wrapEvent = id -------------------------------------------------------------------------------- -- Serialisation diff --git a/alonzo/impl/src/Cardano/Ledger/Alonzo/Rules/Utxos.hs b/alonzo/impl/src/Cardano/Ledger/Alonzo/Rules/Utxos.hs index 587bd761b85..c1b12085351 100644 --- a/alonzo/impl/src/Cardano/Ledger/Alonzo/Rules/Utxos.hs +++ b/alonzo/impl/src/Cardano/Ledger/Alonzo/Rules/Utxos.hs @@ -294,7 +294,6 @@ instance Embed (PPUP era) (UTXOS era) where wrapFailed = UpdateFailure - wrapEvent = id -- ================================================================= diff --git a/alonzo/impl/src/Cardano/Ledger/Alonzo/Rules/Utxow.hs b/alonzo/impl/src/Cardano/Ledger/Alonzo/Rules/Utxow.hs index 1b1bf26cfcd..6468ce7da56 100644 --- a/alonzo/impl/src/Cardano/Ledger/Alonzo/Rules/Utxow.hs +++ b/alonzo/impl/src/Cardano/Ledger/Alonzo/Rules/Utxow.hs @@ -456,4 +456,3 @@ instance Embed (AlonzoUTXO era) (AlonzoUTXOW era) where wrapFailed = WrappedShelleyEraFailure . UtxoFailure - wrapEvent = id diff --git a/byron/chain/executable-spec/src/Byron/Spec/Chain/STS/Rule/BBody.hs b/byron/chain/executable-spec/src/Byron/Spec/Chain/STS/Rule/BBody.hs index d2e7a817c11..5c437e143e1 100644 --- a/byron/chain/executable-spec/src/Byron/Spec/Chain/STS/Rule/BBody.hs +++ b/byron/chain/executable-spec/src/Byron/Spec/Chain/STS/Rule/BBody.hs @@ -22,7 +22,7 @@ import Byron.Spec.Ledger.Update (PParams, UPIState, maxBkSz) import Byron.Spec.Ledger.UTxO (UTxO) import Control.State.Transition (Embed, Environment, STS (..), Signal, State, TRC (TRC), initialRules, judgmentContext, trans, transitionRules, wrapFailed, - (?!), wrapEvent) + (?!)) import Byron.Spec.Chain.STS.Block @@ -93,12 +93,9 @@ instance STS BBODY where instance Embed BUPI BBODY where wrapFailed = BUPIFailure - wrapEvent = id instance Embed DELEG BBODY where wrapFailed = DelegationFailure - wrapEvent = id instance Embed UTXOWS BBODY where wrapFailed = UTXOWSFailure - wrapEvent = id diff --git a/byron/chain/executable-spec/src/Byron/Spec/Chain/STS/Rule/Bupi.hs b/byron/chain/executable-spec/src/Byron/Spec/Chain/STS/Rule/Bupi.hs index d3ad5a9b553..e704796632a 100644 --- a/byron/chain/executable-spec/src/Byron/Spec/Chain/STS/Rule/Bupi.hs +++ b/byron/chain/executable-spec/src/Byron/Spec/Chain/STS/Rule/Bupi.hs @@ -10,7 +10,7 @@ import Data.Data (Data, Typeable) import Control.State.Transition (Embed, Environment, PredicateFailure, STS, Signal, State, TRC (TRC), TransitionRule, initialRules, judgmentContext, trans, - transitionRules, wrapFailed, wrapEvent) + transitionRules, wrapFailed) import Byron.Spec.Ledger.Core (VKey) import Byron.Spec.Ledger.Update (ProtVer, UPIEND, UPIEnv, UPIREG, UPIState, UPIVOTES, UProp, Vote) @@ -67,12 +67,9 @@ instance STS BUPI where instance Embed UPIREG BUPI where wrapFailed = UPIREGFailure - wrapEvent = id instance Embed UPIVOTES BUPI where wrapFailed = UPIVOTESFailure - wrapEvent = id instance Embed UPIEND BUPI where wrapFailed = UPIENDFailure - wrapEvent = id diff --git a/byron/chain/executable-spec/src/Byron/Spec/Chain/STS/Rule/Chain.hs b/byron/chain/executable-spec/src/Byron/Spec/Chain/STS/Rule/Chain.hs index 17d83f9dc10..b7b3ad52ec4 100644 --- a/byron/chain/executable-spec/src/Byron/Spec/Chain/STS/Rule/Chain.hs +++ b/byron/chain/executable-spec/src/Byron/Spec/Chain/STS/Rule/Chain.hs @@ -162,23 +162,18 @@ instance STS CHAIN where instance Embed EPOCH CHAIN where wrapFailed = EpochFailure - wrapEvent = id instance Embed BBODY CHAIN where wrapFailed = BBodyFailure - wrapEvent = id instance Embed PBFT CHAIN where wrapFailed = PBFTFailure - wrapEvent = id instance Embed DELEG CHAIN where wrapFailed = LedgerDelegationFailure - wrapEvent = id instance Embed UTXOWS CHAIN where wrapFailed = LedgerUTxOFailure - wrapEvent = id isHeaderSizeTooBigFailure :: PredicateFailure CHAIN -> Bool isHeaderSizeTooBigFailure (HeaderSizeTooBig _ _ _) = True diff --git a/byron/chain/executable-spec/src/Byron/Spec/Chain/STS/Rule/Epoch.hs b/byron/chain/executable-spec/src/Byron/Spec/Chain/STS/Rule/Epoch.hs index 8c0c992cc82..d3295bc8ff9 100644 --- a/byron/chain/executable-spec/src/Byron/Spec/Chain/STS/Rule/Epoch.hs +++ b/byron/chain/executable-spec/src/Byron/Spec/Chain/STS/Rule/Epoch.hs @@ -58,4 +58,3 @@ instance STS EPOCH where instance Embed UPIEC EPOCH where wrapFailed = UPIECFailure - wrapEvent = id diff --git a/byron/chain/executable-spec/src/Byron/Spec/Chain/STS/Rule/Pbft.hs b/byron/chain/executable-spec/src/Byron/Spec/Chain/STS/Rule/Pbft.hs index 911b175d459..25593d5767f 100644 --- a/byron/chain/executable-spec/src/Byron/Spec/Chain/STS/Rule/Pbft.hs +++ b/byron/chain/executable-spec/src/Byron/Spec/Chain/STS/Rule/Pbft.hs @@ -62,4 +62,3 @@ instance STS PBFT where instance Embed SIGCNT PBFT where wrapFailed = SigCountFailure - wrapEvent = id diff --git a/byron/ledger/executable-spec/src/Byron/Spec/Ledger/Delegation.hs b/byron/ledger/executable-spec/src/Byron/Spec/Ledger/Delegation.hs index c41d277059d..bdb5a433318 100644 --- a/byron/ledger/executable-spec/src/Byron/Spec/Ledger/Delegation.hs +++ b/byron/ledger/executable-spec/src/Byron/Spec/Ledger/Delegation.hs @@ -451,7 +451,6 @@ instance STS SDELEGS where instance Embed SDELEG SDELEGS where wrapFailed = SDelegFailure - wrapEvent = id -- | Delegation rules sequencing data ADELEGS deriving (Data, Typeable) @@ -485,7 +484,6 @@ instance STS ADELEGS where instance Embed ADELEG ADELEGS where wrapFailed = ADelegFailure - wrapEvent = id -- | Delegation interface data DELEG deriving (Data, Typeable) @@ -530,11 +528,9 @@ instance STS DELEG where instance Embed SDELEGS DELEG where wrapFailed = SDelegSFailure - wrapEvent = id instance Embed ADELEGS DELEG where wrapFailed = ADelegSFailure - wrapEvent = id -------------------------------------------------------------------------------- -- Generators @@ -627,7 +623,6 @@ instance STS MSDELEG where instance Embed SDELEG MSDELEG where wrapFailed = SDELEGFailure - wrapEvent = id instance HasTrace MSDELEG where diff --git a/byron/ledger/executable-spec/src/Byron/Spec/Ledger/STS/UTXOW.hs b/byron/ledger/executable-spec/src/Byron/Spec/Ledger/STS/UTXOW.hs index b14543632d9..8e38bee2e58 100644 --- a/byron/ledger/executable-spec/src/Byron/Spec/Ledger/STS/UTXOW.hs +++ b/byron/ledger/executable-spec/src/Byron/Spec/Ledger/STS/UTXOW.hs @@ -93,7 +93,6 @@ witnessed (Tx tx wits) utxo = instance Embed UTXO UTXOW where wrapFailed = UtxoFailure - wrapEvent = id -- | Constant list of addresses intended to be used in the generators. traceAddrs :: [Addr] diff --git a/byron/ledger/executable-spec/src/Byron/Spec/Ledger/STS/UTXOWS.hs b/byron/ledger/executable-spec/src/Byron/Spec/Ledger/STS/UTXOWS.hs index 20692a3c51a..4beda4b71f2 100644 --- a/byron/ledger/executable-spec/src/Byron/Spec/Ledger/STS/UTXOWS.hs +++ b/byron/ledger/executable-spec/src/Byron/Spec/Ledger/STS/UTXOWS.hs @@ -22,7 +22,7 @@ import Byron.Spec.Ledger.STS.UTXOW (UTXOW) import Byron.Spec.Ledger.UTxO (Tx) import Control.State.Transition (Embed, Environment, IRC (IRC), PredicateFailure, STS(..), Signal, State, TRC (TRC), initialRules, judgmentContext, trans, - transitionRules, wrapFailed, wrapEvent) + transitionRules, wrapFailed) import Control.State.Transition.Generator (HasTrace, envGen, genTrace, sigGen) import Control.State.Transition.Trace (TraceOrder (OldestFirst), traceSignals) @@ -57,7 +57,6 @@ instance STS UTXOWS where instance Embed UTXOW UTXOWS where wrapFailed = UtxowFailure - wrapEvent = id instance HasTrace UTXOWS where envGen = envGen @UTXOW diff --git a/byron/ledger/executable-spec/src/Byron/Spec/Ledger/Update.hs b/byron/ledger/executable-spec/src/Byron/Spec/Ledger/Update.hs index 3e122de07bd..8e05fff4c98 100644 --- a/byron/ledger/executable-spec/src/Byron/Spec/Ledger/Update.hs +++ b/byron/ledger/executable-spec/src/Byron/Spec/Ledger/Update.hs @@ -499,11 +499,9 @@ instance STS UPV where instance Embed UPPVV UPV where wrapFailed = UPPVVFailure - wrapEvent = id instance Embed UPSVV UPV where wrapFailed = UPSVVFailure - wrapEvent = id data UPREG deriving (Generic, Data, Typeable) -- | These `PredicateFailure`s are all throwable. @@ -545,7 +543,6 @@ instance STS UPREG where instance Embed UPV UPREG where wrapFailed = UPVFailure - wrapEvent = id ------------------------------------------------------------------------ -- Update voting @@ -671,7 +668,6 @@ instance STS UPVOTE where instance Embed ADDVOTE UPVOTE where wrapFailed = ADDVOTEFailure - wrapEvent = id ------------------------------------------------------------------------ -- Update voting @@ -813,7 +809,6 @@ instance STS UPEND where instance Embed FADS UPEND where wrapFailed = error "No possible failures in FADS" - wrapEvent = id ------------------------------------------------------------------------ -- Update interface @@ -985,7 +980,6 @@ instance STS UPIREG where instance Embed UPREG UPIREG where wrapFailed = UPREGFailure - wrapEvent = id instance HasTrace UPIREG where @@ -1369,7 +1363,6 @@ instance STS UPIVOTE where instance Embed UPVOTE UPIVOTE where wrapFailed = UPVOTEFailure - wrapEvent = id data APPLYVOTES deriving (Generic, Data, Typeable) @@ -1399,7 +1392,6 @@ instance STS APPLYVOTES where instance Embed UPIVOTE APPLYVOTES where wrapFailed = UpivoteFailure - wrapEvent = id data UPIVOTES deriving (Generic, Data, Typeable) @@ -1458,7 +1450,6 @@ instance STS UPIVOTES where instance Embed APPLYVOTES UPIVOTES where wrapFailed = ApplyVotesFailure - wrapEvent = id instance HasTrace UPIVOTES where @@ -1598,7 +1589,6 @@ instance STS UPIEND where instance Embed UPEND UPIEND where wrapFailed = UPENDFailure - wrapEvent = id -- | Given a list of protocol versions and keys endorsing those versions, -- generate a protocol-version endorsement, or 'Nothing' if the list of @@ -1701,7 +1691,6 @@ instance STS UPIEC where instance Embed PVBUMP UPIEC where wrapFailed = PVBUMPFailure - wrapEvent = id -- | Generate an optional update-proposal and a list of votes, given an update -- environment and state. diff --git a/byron/ledger/executable-spec/test/Test/Byron/Spec/Ledger/Delegation/Properties.hs b/byron/ledger/executable-spec/test/Test/Byron/Spec/Ledger/Delegation/Properties.hs index 86fe751ac38..15006d60784 100644 --- a/byron/ledger/executable-spec/test/Test/Byron/Spec/Ledger/Delegation/Properties.hs +++ b/byron/ledger/executable-spec/test/Test/Byron/Spec/Ledger/Delegation/Properties.hs @@ -41,7 +41,7 @@ import Lens.Micro.TH (makeLenses) import Control.State.Transition (Embed, Environment, IRC (IRC), PredicateFailure, STS, Signal, State, TRC (TRC), applySTS, initialRules, judgmentContext, trans, - transitionRules, wrapFailed, (?!), wrapEvent) + transitionRules, wrapFailed, (?!)) import Control.State.Transition.Generator (HasSizeInfo, HasTrace, SignalGenerator, TraceProfile (TraceProfile), classifySize, classifyTraceLength, envGen, failures, isTrivial, nonTrivialTrace, proportionOfValidSignals, sigGen, @@ -132,7 +132,6 @@ instance STS DBLOCK where instance Embed DELEG DBLOCK where wrapFailed = DPF - wrapEvent = id -- | Check that all the delegation certificates in the trace were correctly -- applied. diff --git a/byron/ledger/executable-spec/test/Test/Byron/Spec/Ledger/Update/Properties.hs b/byron/ledger/executable-spec/test/Test/Byron/Spec/Ledger/Update/Properties.hs index 94cb65e1555..95543ed0748 100644 --- a/byron/ledger/executable-spec/test/Test/Byron/Spec/Ledger/Update/Properties.hs +++ b/byron/ledger/executable-spec/test/Test/Byron/Spec/Ledger/Update/Properties.hs @@ -36,7 +36,7 @@ import Numeric.Natural (Natural) import Control.State.Transition (Embed, Environment, IRC (IRC), PredicateFailure, STS, Signal, State, TRC (TRC), initialRules, judgmentContext, trans, - transitionRules, wrapFailed, (?!), wrapEvent) + transitionRules, wrapFailed, (?!)) import Control.State.Transition.Generator (HasTrace, SignalGenerator, envGen, randomTraceOfSize, ratio, sigGen, trace, traceLengthsAreClassified, traceOfLength) @@ -351,15 +351,12 @@ instance STS UBLOCK where instance Embed UPIREG UBLOCK where wrapFailed = UPIREGFailure - wrapEvent = id instance Embed UPIVOTES UBLOCK where wrapFailed = UPIVOTESFailure - wrapEvent = id instance Embed UPIEND UBLOCK where wrapFailed = UPIENDFailure - wrapEvent = id instance HasTrace UBLOCK where envGen _ = diff --git a/semantics/executable-spec/src/Control/State/Transition/Extended.hs b/semantics/executable-spec/src/Control/State/Transition/Extended.hs index 340f6a194fb..3d5e3f1d175 100644 --- a/semantics/executable-spec/src/Control/State/Transition/Extended.hs +++ b/semantics/executable-spec/src/Control/State/Transition/Extended.hs @@ -91,6 +91,7 @@ import Data.Proxy (Proxy (..)) import Data.Typeable (typeRep) import NoThunks.Class (NoThunks (..)) import Data.Void (Void) +import Data.Coerce (coerce, Coercible) data RuleType = Initial @@ -230,10 +231,11 @@ class (STS sub, BaseM sub ~ BaseM super) => Embed sub super where -- | Wrap a predicate failure of the subsystem in a failure of the super-system. wrapFailed :: PredicateFailure sub -> PredicateFailure super wrapEvent :: Event sub -> Event super + default wrapEvent :: Coercible (Event sub) (Event super) => Event sub -> Event super + wrapEvent = coerce instance STS sts => Embed sts sts where wrapFailed = id - wrapEvent = id data EventPolicy = EventPolicyReturn diff --git a/shelley-ma/impl/src/Cardano/Ledger/ShelleyMA/Rules/Utxo.hs b/shelley-ma/impl/src/Cardano/Ledger/ShelleyMA/Rules/Utxo.hs index 36ef249cc90..eceb56a9646 100644 --- a/shelley-ma/impl/src/Cardano/Ledger/ShelleyMA/Rules/Utxo.hs +++ b/shelley-ma/impl/src/Cardano/Ledger/ShelleyMA/Rules/Utxo.hs @@ -390,7 +390,6 @@ instance Embed (PPUP era) (UTXO era) where wrapFailed = UpdateFailure - wrapEvent = id -------------------------------------------------------------------------------- -- Serialisation diff --git a/shelley-ma/impl/src/Cardano/Ledger/ShelleyMA/Rules/Utxow.hs b/shelley-ma/impl/src/Cardano/Ledger/ShelleyMA/Rules/Utxow.hs index 528aa7b2657..7737a3e3d16 100644 --- a/shelley-ma/impl/src/Cardano/Ledger/ShelleyMA/Rules/Utxow.hs +++ b/shelley-ma/impl/src/Cardano/Ledger/ShelleyMA/Rules/Utxow.hs @@ -81,7 +81,6 @@ instance Embed (UTXO era) (UTXOW era) where wrapFailed = UtxoFailure - wrapEvent = id instance ( Era era, diff --git a/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Epoch.hs b/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Epoch.hs index 35736bd27ab..dc6fec09af9 100644 --- a/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Epoch.hs +++ b/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Epoch.hs @@ -206,7 +206,6 @@ instance Embed (SNAP era) (EPOCH era) where wrapFailed = SnapFailure - wrapEvent = id instance ( Era era, @@ -216,7 +215,6 @@ instance Embed (POOLREAP era) (EPOCH era) where wrapFailed = PoolReapFailure - wrapEvent = id instance ( Era era, @@ -226,4 +224,3 @@ instance Embed (UPEC era) (EPOCH era) where wrapFailed = UpecFailure - wrapEvent = id diff --git a/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/NewEpoch.hs b/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/NewEpoch.hs index f93b67cf5d6..5aa777b4469 100644 --- a/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/NewEpoch.hs +++ b/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/NewEpoch.hs @@ -186,7 +186,6 @@ instance Embed (EPOCH era) (NEWEPOCH era) where wrapFailed = EpochFailure - wrapEvent = id instance ( Era era, @@ -196,4 +195,3 @@ instance Embed (MIR era) (NEWEPOCH era) where wrapFailed = MirFailure - wrapEvent = id diff --git a/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Overlay.hs b/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Overlay.hs index 9430eef0efb..953d0c63063 100644 --- a/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Overlay.hs +++ b/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Overlay.hs @@ -293,4 +293,3 @@ instance Embed (OCERT crypto) (OVERLAY crypto) where wrapFailed = OcertFailure - wrapEvent = id diff --git a/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Prtcl.hs b/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Prtcl.hs index 38cb7c32dfb..0f745662a58 100644 --- a/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Prtcl.hs +++ b/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Prtcl.hs @@ -199,7 +199,6 @@ instance Embed (OVERLAY crypto) (PRTCL crypto) where wrapFailed = OverlayFailure - wrapEvent = id instance ( Crypto crypto, @@ -210,7 +209,6 @@ instance Embed (UPDN crypto) (PRTCL crypto) where wrapFailed = UpdnFailure - wrapEvent = id data PrtlSeqFailure crypto = WrongSlotIntervalPrtclSeq diff --git a/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Tick.hs b/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Tick.hs index 5ad6adde606..41e41f99556 100644 --- a/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Tick.hs +++ b/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Tick.hs @@ -192,7 +192,6 @@ instance Embed (NEWEPOCH era) (TICK era) where wrapFailed = NewEpochFailure - wrapEvent = id instance ( Era era, @@ -202,7 +201,6 @@ instance Embed (RUPD era) (TICK era) where wrapFailed = RupdFailure - wrapEvent = id {------------------------------------------------------------------------------ -- TICKF transition @@ -272,4 +270,3 @@ instance Embed (NEWEPOCH era) (TICKF era) where wrapFailed = TickfNewEpochFailure - wrapEvent = id diff --git a/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Upec.hs b/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Upec.hs index cf94e545059..018d9b05814 100644 --- a/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Upec.hs +++ b/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Upec.hs @@ -156,4 +156,3 @@ instance Embed (NEWPP era) (UPEC era) where wrapFailed = NewPpFailure - wrapEvent = id From 7f085ca0aae00707f5c17ddafcd0e870c41e3ee5 Mon Sep 17 00:00:00 2001 From: Zachary Churchill Date: Mon, 19 Jul 2021 11:08:13 -0700 Subject: [PATCH 4/4] rm EventConstraintType and writer cps mtl --- semantics/executable-spec/small-steps.cabal | 1 - .../src/Control/State/Transition/Extended.hs | 39 +++++-------------- 2 files changed, 10 insertions(+), 30 deletions(-) diff --git a/semantics/executable-spec/small-steps.cabal b/semantics/executable-spec/small-steps.cabal index a26dac2e16e..585e7e125a4 100644 --- a/semantics/executable-spec/small-steps.cabal +++ b/semantics/executable-spec/small-steps.cabal @@ -69,7 +69,6 @@ library , strict-containers , text , transformers >= 0.5 - , writer-cps-mtl -- IOHK deps , cardano-crypto-class , cardano-binary diff --git a/semantics/executable-spec/src/Control/State/Transition/Extended.hs b/semantics/executable-spec/src/Control/State/Transition/Extended.hs index 818a91b07f6..7ffa9b9a761 100644 --- a/semantics/executable-spec/src/Control/State/Transition/Extended.hs +++ b/semantics/executable-spec/src/Control/State/Transition/Extended.hs @@ -42,7 +42,6 @@ module Control.State.Transition.Extended SingEP (..), EventPolicy (..), EventReturnType, - EventConstraintType, labeledPred, labeledPredE, failBecause, @@ -82,14 +81,13 @@ import Control.Monad.State.Class (MonadState (..), modify) import Control.Monad.Trans.Class (MonadTrans, lift) import Control.Monad.Trans.Except import Control.Monad.Trans.State.Strict (StateT (..)) -import Control.Monad.Writer.CPS (WriterT, runWriterT) -import Control.Monad.Writer.Class (MonadWriter (..)) +import Data.Bifunctor (Bifunctor (second), first) import Data.Coerce (Coercible, coerce) import Data.Data (Data, Typeable) import Data.Default.Class (Default, def) import Data.Foldable (find, traverse_) import Data.Functor (($>), (<&>)) -import Data.Kind (Constraint, Type) +import Data.Kind (Type) import Data.Typeable (typeRep) import Data.Void (Void) import NoThunks.Class (NoThunks (..)) @@ -255,10 +253,6 @@ type family EventReturnType ep sts a :: Type where EventReturnType 'EventPolicyReturn sts a = (a, [Event sts]) EventReturnType _ _ a = a -type family EventConstraintType e sts m :: Constraint where - EventConstraintType 'EventPolicyReturn sts m = MonadWriter [Event sts] m - EventConstraintType _ _ _ = () - discardEvents :: forall ep a. SingEP ep -> forall s. EventReturnType ep s a -> a discardEvents ep = case ep of EPReturn -> fst @@ -478,19 +472,6 @@ applySTSIndifferently = asoValidation = ValidateAll } -newtype RuleEventLoggerT s m a = RuleEventLoggerT (StateT [PredicateFailure s] (WriterT [Event s] m) a) - deriving (Monad, Applicative, Functor) - -deriving instance (e ~ [Event s], Monad m) => MonadWriter e (RuleEventLoggerT s m) - -deriving instance (f ~ [PredicateFailure s], Monad m) => MonadState f (RuleEventLoggerT s m) - -instance MonadTrans (RuleEventLoggerT s) where - lift = RuleEventLoggerT . lift . lift - -runRuleEventLoggerT :: forall s m a. RuleEventLoggerT s m a -> [PredicateFailure s] -> m ((a, [PredicateFailure s]), [Event s]) -runRuleEventLoggerT (RuleEventLoggerT m) s = runWriterT $ runStateT m s - -- | Apply a rule even if its predicates fail. -- -- If the rule successfully applied, the list of predicate failures will be @@ -505,16 +486,16 @@ applyRuleInternal :: RuleContext rtype s -> Rule s rtype (State s) -> m (EventReturnType ep s (State s, [PredicateFailure s])) -applyRuleInternal ep vp goSTS jc r = +applyRuleInternal ep vp goSTS jc r = do + (s, er) <- flip runStateT ([], []) $ foldF runClause r case ep of - EPReturn -> flip (runRuleEventLoggerT @s) [] $ foldF runClause r - EPDiscard -> flip runStateT [] $ foldF runClause r + EPDiscard -> pure (s, fst er) + EPReturn -> pure ((s, fst er), snd er) where runClause :: forall f t a. ( f ~ t m, - MonadState [PredicateFailure s] f, - EventConstraintType ep s f, + MonadState ([PredicateFailure s], [Event s]) f, MonadTrans t ) => Clause s rtype a -> @@ -524,7 +505,7 @@ applyRuleInternal ep vp goSTS jc r = runClause (Predicate lbls cond orElse val) = if validateIf lbls then case cond of - Left err -> modify (orElse err :) >> pure val + Left err -> modify (first (orElse err :)) >> pure val Right x -> pure x else pure val runClause (SubTrans (subCtx :: RuleContext _rtype sub) next) = do @@ -534,11 +515,11 @@ applyRuleInternal ep vp goSTS jc r = sevs :: [Event sub] (ss, sfails) = discardEvents ep @sub s sevs = getEvents ep @sub @(State sub, [PredicateFailure sub]) s - traverse_ (\a -> modify (a :)) $ wrapFailed @sub @s <$> sfails + traverse_ (\a -> modify (first (a :))) $ wrapFailed @sub @s <$> sfails runClause $ Writer (wrapEvent @sub @s <$> sevs) () pure $ next ss runClause (Writer w a) = case ep of - EPReturn -> tell w $> a + EPReturn -> modify (second (\es -> es <> w)) $> a EPDiscard -> pure a validateIf lbls = case vp of ValidateAll -> True