Skip to content

Commit f898ecd

Browse files
committed
Simplify a whole bunch of constraints in Dijkstra
1 parent 53604b1 commit f898ecd

12 files changed

Lines changed: 71 additions & 462 deletions

File tree

eras/dijkstra/impl/src/Cardano/Ledger/Dijkstra/Rules/Bbody.hs

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -404,8 +404,7 @@ conwayToDijkstraBbodyPredFailure = \case
404404
Conway.HeaderProtVerTooHigh {} -> error "Impossible: HeaderProtVerTooHigh cannot be triggered in Dijkstra era"
405405

406406
instance
407-
( Era era
408-
, BaseM ledgers ~ ShelleyBase
407+
( BaseM ledgers ~ ShelleyBase
409408
, ledgers ~ EraRule "LEDGERS" era
410409
, STS ledgers
411410
) =>

eras/dijkstra/impl/src/Cardano/Ledger/Dijkstra/Rules/Cert.hs

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -116,8 +116,7 @@ certTransition = do
116116
TRC (ConwayGovCertEnv pp currentEpoch committee committeeProposals, certState, govCert)
117117

118118
instance
119-
( Era era
120-
, STS (DijkstraGOVCERT era)
119+
( STS (DijkstraGOVCERT era)
121120
, PredicateFailure (EraRule "GOVCERT" era) ~ DijkstraGovCertPredFailure era
122121
) =>
123122
Embed (DijkstraGOVCERT era) (DijkstraCERT era)

eras/dijkstra/impl/src/Cardano/Ledger/Dijkstra/Rules/Certs.hs

Lines changed: 4 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -7,7 +7,6 @@
77

88
module Cardano.Ledger.Dijkstra.Rules.Certs () where
99

10-
import Cardano.Ledger.BaseTypes
1110
import Cardano.Ledger.Conway.Rules (
1211
ConwayCERTS,
1312
ConwayCertEvent (..),
@@ -51,7 +50,6 @@ instance InjectRuleFailure "CERTS" ConwayGovCertPredFailure DijkstraEra where
5150
instance
5251
( Era era
5352
, STS (DijkstraCERT era)
54-
, BaseM (EraRule "CERT" era) ~ ShelleyBase
5553
, Event (EraRule "CERT" era) ~ ConwayCertEvent era
5654
, PredicateFailure (EraRule "CERT" era) ~ ConwayCertPredFailure era
5755
) =>
@@ -61,8 +59,7 @@ instance
6159
wrapEvent = CertEvent
6260

6361
instance
64-
( Era era
65-
, STS (ConwayDELEG era)
62+
( STS (ConwayDELEG era)
6663
, PredicateFailure (EraRule "DELEG" era) ~ ConwayDelegPredFailure era
6764
) =>
6865
Embed (ConwayDELEG era) (DijkstraCERT era)
@@ -71,21 +68,17 @@ instance
7168
wrapEvent = absurd
7269

7370
instance
74-
( Era era
75-
, STS (ShelleyPOOL era)
76-
, Event (EraRule "POOL" era) ~ PoolEvent era
71+
( STS (ShelleyPOOL era)
7772
, PredicateFailure (EraRule "POOL" era) ~ ShelleyPoolPredFailure era
78-
, PredicateFailure (ShelleyPOOL era) ~ ShelleyPoolPredFailure era
79-
, BaseM (ShelleyPOOL era) ~ ShelleyBase
73+
, Event (EraRule "POOL" era) ~ PoolEvent era
8074
) =>
8175
Embed (ShelleyPOOL era) (DijkstraCERT era)
8276
where
8377
wrapFailed = PoolFailure
8478
wrapEvent = PoolEvent
8579

8680
instance
87-
( Era era
88-
, STS (ConwayGOVCERT era)
81+
( STS (ConwayGOVCERT era)
8982
, PredicateFailure (EraRule "GOVCERT" era) ~ ConwayGovCertPredFailure era
9083
) =>
9184
Embed (ConwayGOVCERT era) (DijkstraCERT era)

eras/dijkstra/impl/src/Cardano/Ledger/Dijkstra/Rules/Ledger.hs

Lines changed: 13 additions & 140 deletions
Original file line numberDiff line numberDiff line change
@@ -24,14 +24,13 @@ module Cardano.Ledger.Dijkstra.Rules.Ledger (
2424

2525
import Cardano.Ledger.Allegra.Rules (AllegraUtxoPredFailure)
2626
import Cardano.Ledger.Alonzo (AlonzoScript)
27-
import Cardano.Ledger.Alonzo.Plutus.Context (EraPlutusContext)
2827
import Cardano.Ledger.Alonzo.Rules (
2928
AlonzoUtxoPredFailure,
3029
AlonzoUtxosPredFailure,
3130
AlonzoUtxowEvent,
3231
AlonzoUtxowPredFailure,
3332
)
34-
import Cardano.Ledger.Alonzo.UTxO (AlonzoEraUTxO, AlonzoScriptsNeeded)
33+
import Cardano.Ledger.Alonzo.UTxO (AlonzoScriptsNeeded)
3534
import Cardano.Ledger.Babbage (BabbageTxOut)
3635
import Cardano.Ledger.Babbage.Rules (
3736
BabbageUtxoPredFailure,
@@ -55,14 +54,12 @@ import Cardano.Ledger.Conway.Governance (
5554
proposalsWithPurpose,
5655
)
5756
import Cardano.Ledger.Conway.Rules (
58-
CertEnv,
5957
CertsEnv (..),
6058
ConwayCERTS,
6159
ConwayCertPredFailure (..),
6260
ConwayCertsPredFailure (..),
6361
ConwayDelegPredFailure,
6462
ConwayGovCertPredFailure,
65-
ConwayGovEvent,
6663
ConwayGovPredFailure,
6764
ConwayLedgerPredFailure,
6865
ConwayUtxoPredFailure,
@@ -82,29 +79,16 @@ import Cardano.Ledger.Dijkstra.Era (
8279
DijkstraEra,
8380
DijkstraGOV,
8481
DijkstraLEDGER,
85-
DijkstraSUBCERT,
86-
DijkstraSUBCERTS,
87-
DijkstraSUBDELEG,
88-
DijkstraSUBGOV,
89-
DijkstraSUBGOVCERT,
90-
DijkstraSUBUTXO,
91-
DijkstraSUBUTXOW,
9282
DijkstraUTXOW,
9383
)
9484
import Cardano.Ledger.Dijkstra.Rules.Certs ()
9585
import Cardano.Ledger.Dijkstra.Rules.Gov (DijkstraGovPredFailure)
9686
import Cardano.Ledger.Dijkstra.Rules.GovCert (DijkstraGovCertPredFailure)
97-
import Cardano.Ledger.Dijkstra.Rules.SubDeleg (DijkstraSubDelegPredFailure)
98-
import Cardano.Ledger.Dijkstra.Rules.SubGov (DijkstraSubGovEvent, DijkstraSubGovPredFailure)
99-
import Cardano.Ledger.Dijkstra.Rules.SubGovCert (DijkstraSubGovCertPredFailure)
10087
import Cardano.Ledger.Dijkstra.Rules.SubLedger
10188
import Cardano.Ledger.Dijkstra.Rules.SubLedgers
102-
import Cardano.Ledger.Dijkstra.Rules.SubPool
103-
import Cardano.Ledger.Dijkstra.Rules.SubUtxow (DijkstraSubUtxowPredFailure)
10489
import Cardano.Ledger.Dijkstra.Rules.Utxo (DijkstraUtxoPredFailure)
10590
import Cardano.Ledger.Dijkstra.Rules.Utxow (DijkstraUtxoEnv (..), DijkstraUtxowPredFailure)
10691
import Cardano.Ledger.Dijkstra.TxBody
107-
import Cardano.Ledger.Dijkstra.TxCert
10892
import Cardano.Ledger.Rules.ValidationMode (runTest)
10993
import Cardano.Ledger.Shelley.LedgerState (
11094
LedgerState (..),
@@ -115,7 +99,6 @@ import Cardano.Ledger.Shelley.LedgerState (
11599
)
116100
import Cardano.Ledger.Shelley.Rules (
117101
LedgerEnv (..),
118-
PoolEvent,
119102
ShelleyLEDGERS,
120103
ShelleyLedgerPredFailure (..),
121104
ShelleyLedgersEvent (LedgerEvent),
@@ -538,79 +521,19 @@ instance
538521
wrapEvent = UtxowEvent
539522

540523
instance
541-
( Embed (EraRule "UTXOW" era) (DijkstraLEDGER era)
542-
, Embed (EraRule "CERTS" era) (DijkstraLEDGER era)
543-
, Embed (EraRule "GOV" era) (DijkstraLEDGER era)
544-
, ConwayEraGov era
545-
, AlonzoEraTx era
546-
, AlonzoEraUTxO era
547-
, ConwayEraPParams era
548-
, DijkstraEraTxBody era
549-
, EraPlutusContext era
550-
, GovState era ~ ConwayGovState era
551-
, Environment (EraRule "UTXOW" era) ~ DijkstraUtxoEnv era
552-
, Environment (EraRule "CERTS" era) ~ CertsEnv era
553-
, Signal (EraRule "UTXOW" era) ~ Tx TopTx era
554-
, Signal (EraRule "CERTS" era) ~ Seq (TxCert era)
555-
, State (EraRule "UTXOW" era) ~ UTxOState era
556-
, State (EraRule "CERTS" era) ~ CertState era
557-
, EraRule "GOV" era ~ DijkstraGOV era
558-
, ConwayEraCertState era
559-
, EraRule "LEDGER" era ~ DijkstraLEDGER era
560-
, EraRule "SUBLEDGERS" era ~ DijkstraSUBLEDGERS era
561-
, EraRule "SUBLEDGER" era ~ DijkstraSUBLEDGER era
562-
, EraRule "SUBGOV" era ~ DijkstraSUBGOV era
563-
, EraRule "SUBUTXO" era ~ DijkstraSUBUTXO era
564-
, EraRule "SUBUTXOW" era ~ DijkstraSUBUTXOW era
565-
, EraRule "SUBCERTS" era ~ DijkstraSUBCERTS era
566-
, EraRule "SUBCERT" era ~ DijkstraSUBCERT era
567-
, EraRule "SUBDELEG" era ~ DijkstraSUBDELEG era
568-
, EraRule "SUBPOOL" era ~ DijkstraSUBPOOL era
569-
, EraRule "SUBGOVCERT" era ~ DijkstraSUBGOVCERT era
570-
, InjectRuleFailure "LEDGER" ShelleyLedgerPredFailure era
571-
, InjectRuleFailure "LEDGER" ConwayLedgerPredFailure era
572-
, InjectRuleFailure "LEDGER" DijkstraLedgerPredFailure era
573-
, InjectRuleFailure "LEDGER" DijkstraSubLedgersPredFailure era
574-
, InjectRuleEvent "SUBPOOL" DijkstraSubPoolEvent era
575-
, InjectRuleEvent "SUBPOOL" PoolEvent era
576-
, InjectRuleFailure "SUBPOOL" DijkstraSubPoolPredFailure era
577-
, InjectRuleFailure "SUBPOOL" ShelleyPoolPredFailure era
578-
, InjectRuleFailure "SUBGOVCERT" DijkstraSubGovCertPredFailure era
579-
, InjectRuleFailure "SUBGOVCERT" ConwayGovCertPredFailure era
580-
, InjectRuleFailure "DELEG" ConwayDelegPredFailure era
581-
, InjectRuleFailure "SUBDELEG" ConwayDelegPredFailure era
582-
, InjectRuleFailure "SUBDELEG" DijkstraSubDelegPredFailure era
583-
, InjectRuleEvent "SUBGOV" DijkstraSubGovEvent era
584-
, InjectRuleEvent "SUBGOV" ConwayGovEvent era
585-
, InjectRuleFailure "SUBGOV" DijkstraSubGovPredFailure era
586-
, InjectRuleFailure "SUBGOV" ConwayGovPredFailure era
587-
, InjectRuleFailure "SUBLEDGER" ConwayLedgerPredFailure era
588-
, InjectRuleFailure "SUBUTXOW" DijkstraSubUtxowPredFailure era
589-
, InjectRuleFailure "SUBUTXOW" AlonzoUtxowPredFailure era
590-
, InjectRuleFailure "SUBUTXOW" ShelleyUtxowPredFailure era
591-
, InjectRuleFailure "SUBUTXOW" BabbageUtxowPredFailure era
592-
, InjectRuleFailure "SUBUTXO" ShelleyUtxoPredFailure era
593-
, InjectRuleFailure "SUBUTXO" AllegraUtxoPredFailure era
594-
, InjectRuleFailure "SUBUTXO" AlonzoUtxoPredFailure era
595-
, InjectRuleFailure "SUBUTXO" BabbageUtxoPredFailure era
596-
, InjectRuleFailure "SUBUTXO" DijkstraUtxoPredFailure era
597-
, TxCert era ~ DijkstraTxCert era
598-
, ScriptsNeeded era ~ AlonzoScriptsNeeded era
524+
( STS (DijkstraLEDGER era)
525+
, PredicateFailure (EraRule "LEDGER" era) ~ DijkstraLedgerPredFailure era
526+
, Event (EraRule "LEDGER" era) ~ DijkstraLedgerEvent era
599527
) =>
600528
Embed (DijkstraLEDGER era) (ShelleyLEDGERS era)
601529
where
602530
wrapFailed = LedgerFailure
603531
wrapEvent = LedgerEvent
604532

605533
instance
606-
( ConwayEraCertState era
607-
, ConwayEraTxCert era
608-
, ConwayEraPParams era
609-
, ConwayEraGov era
610-
, EraRule "GOV" era ~ DijkstraGOV era
611-
, InjectRuleFailure "GOV" ConwayGovPredFailure era
612-
, InjectRuleFailure "GOV" DijkstraGovPredFailure era
613-
, InjectRuleEvent "GOV" ConwayGovEvent era
534+
( STS (DijkstraGOV era)
535+
, PredicateFailure (EraRule "GOV" era) ~ DijkstraGovPredFailure era
536+
, Event (EraRule "GOV" era) ~ Conway.ConwayGovEvent era
614537
) =>
615538
Embed (DijkstraGOV era) (DijkstraLEDGER era)
616539
where
@@ -639,69 +562,19 @@ shelleyToDijkstraLedgerPredFailure = \case
639562
ShelleyIncompleteWithdrawals x -> DijkstraIncompleteWithdrawals x
640563

641564
instance
642-
( EraTx era
643-
, ConwayEraTxBody era
644-
, ConwayEraPParams era
645-
, ConwayEraGov era
646-
, Embed (EraRule "CERT" era) (ConwayCERTS era)
647-
, State (EraRule "CERT" era) ~ CertState era
648-
, Environment (EraRule "CERT" era) ~ CertEnv era
649-
, Signal (EraRule "CERT" era) ~ TxCert era
650-
, PredicateFailure (EraRule "CERT" era) ~ ConwayCertPredFailure era
651-
, EraRuleFailure "CERT" era ~ ConwayCertPredFailure era
652-
, EraRule "CERTS" era ~ ConwayCERTS era
653-
, ConwayEraCertState era
565+
( STS (ConwayCERTS era)
566+
, PredicateFailure (EraRule "CERTS" era) ~ ConwayCertsPredFailure era
567+
, Event (EraRule "CERTS" era) ~ Conway.ConwayCertsEvent era
654568
) =>
655569
Embed (ConwayCERTS era) (DijkstraLEDGER era)
656570
where
657571
wrapFailed = DijkstraCertsFailure
658572
wrapEvent = CertsEvent
659573

660574
instance
661-
( AlonzoEraTx era
662-
, AlonzoEraUTxO era
663-
, DijkstraEraTxBody era
664-
, ConwayEraGov era
665-
, ConwayEraCertState era
666-
, EraPlutusContext era
667-
, ConwayEraTxCert era
668-
, ConwayEraPParams era
669-
, EraRule "SUBLEDGERS" era ~ DijkstraSUBLEDGERS era
670-
, EraRule "SUBLEDGER" era ~ DijkstraSUBLEDGER era
671-
, EraRule "SUBGOV" era ~ DijkstraSUBGOV era
672-
, EraRule "SUBUTXO" era ~ DijkstraSUBUTXO era
673-
, EraRule "SUBUTXOW" era ~ DijkstraSUBUTXOW era
674-
, EraRule "SUBCERTS" era ~ DijkstraSUBCERTS era
675-
, EraRule "SUBCERT" era ~ DijkstraSUBCERT era
676-
, EraRule "SUBDELEG" era ~ DijkstraSUBDELEG era
677-
, EraRule "SUBPOOL" era ~ DijkstraSUBPOOL era
678-
, EraRule "SUBGOVCERT" era ~ DijkstraSUBGOVCERT era
679-
, Event (EraRule "LEDGER" era) ~ DijkstraLedgerEvent era
680-
, InjectRuleEvent "SUBPOOL" PoolEvent era
681-
, InjectRuleEvent "SUBPOOL" DijkstraSubPoolEvent era
682-
, InjectRuleFailure "SUBPOOL" ShelleyPoolPredFailure era
683-
, InjectRuleFailure "SUBPOOL" DijkstraSubPoolPredFailure era
684-
, InjectRuleFailure "SUBGOVCERT" DijkstraSubGovCertPredFailure era
685-
, InjectRuleFailure "SUBGOVCERT" ConwayGovCertPredFailure era
686-
, InjectRuleFailure "DELEG" ConwayDelegPredFailure era
687-
, InjectRuleFailure "SUBDELEG" ConwayDelegPredFailure era
688-
, InjectRuleFailure "SUBDELEG" DijkstraSubDelegPredFailure era
689-
, InjectRuleEvent "SUBGOV" DijkstraSubGovEvent era
690-
, InjectRuleEvent "SUBGOV" ConwayGovEvent era
691-
, InjectRuleFailure "SUBGOV" DijkstraSubGovPredFailure era
692-
, InjectRuleFailure "SUBGOV" ConwayGovPredFailure era
693-
, InjectRuleFailure "SUBLEDGER" ConwayLedgerPredFailure era
694-
, InjectRuleFailure "SUBUTXOW" DijkstraSubUtxowPredFailure era
695-
, InjectRuleFailure "SUBUTXOW" AlonzoUtxowPredFailure era
696-
, InjectRuleFailure "SUBUTXOW" ShelleyUtxowPredFailure era
697-
, InjectRuleFailure "SUBUTXOW" BabbageUtxowPredFailure era
698-
, InjectRuleFailure "SUBUTXO" ShelleyUtxoPredFailure era
699-
, InjectRuleFailure "SUBUTXO" AllegraUtxoPredFailure era
700-
, InjectRuleFailure "SUBUTXO" AlonzoUtxoPredFailure era
701-
, InjectRuleFailure "SUBUTXO" BabbageUtxoPredFailure era
702-
, InjectRuleFailure "SUBUTXO" DijkstraUtxoPredFailure era
703-
, TxCert era ~ DijkstraTxCert era
704-
, ScriptsNeeded era ~ AlonzoScriptsNeeded era
575+
( STS (DijkstraSUBLEDGERS era)
576+
, PredicateFailure (EraRule "SUBLEDGERS" era) ~ DijkstraSubLedgersPredFailure era
577+
, Event (EraRule "SUBLEDGERS" era) ~ DijkstraSubLedgersEvent era
705578
) =>
706579
Embed (DijkstraSUBLEDGERS era) (DijkstraLEDGER era)
707580
where

0 commit comments

Comments
 (0)