Skip to content

Commit

Permalink
Merge pull request #4729 from IntersectMBO/jj/conformance-spo-voting
Browse files Browse the repository at this point in the history
Added `RewardUpdate` spec translation
  • Loading branch information
lehins authored Oct 29, 2024
2 parents 9461512 + df28ca8 commit 9ec1e6b
Show file tree
Hide file tree
Showing 4 changed files with 25 additions and 2 deletions.
Original file line number Diff line number Diff line change
Expand Up @@ -69,6 +69,7 @@ library
cardano-ledger-binary:{cardano-ledger-binary, testlib},
cardano-ledger-core,
cardano-ledger-shelley:{cardano-ledger-shelley, testlib},
cardano-ledger-shelley-test,
cardano-ledger-alonzo,
cardano-ledger-allegra,
cardano-ledger-babbage,
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -23,6 +23,7 @@ import Cardano.Ledger.Conway.Rules
import Cardano.Ledger.Conway.TxCert
import Cardano.Ledger.EpochBoundary
import Cardano.Ledger.Shelley.LedgerState
import qualified Data.Foldable as Set
import Data.Functor.Identity (Identity)
import Data.Map.Strict (Map)
import qualified Data.VMap as VMap
Expand All @@ -34,6 +35,7 @@ import Test.Cardano.Ledger.Conformance.SpecTranslate.Conway.GovCert ()
import Test.Cardano.Ledger.Conformance.SpecTranslate.Conway.Pool ()
import Test.Cardano.Ledger.Constrained.Conway.Utxo (depositsMap)
import Test.Cardano.Ledger.Conway.TreeDiff
import Test.Cardano.Ledger.Shelley.Utils (runShelleyBase)

instance
( SpecTranslate ctx (PParamsHKD Identity era)
Expand Down Expand Up @@ -170,6 +172,24 @@ instance SpecTranslate ctx AccountState where
<$> toSpecRep asTreasury
<*> toSpecRep asReserves

instance SpecTranslate ctx DeltaCoin where
type SpecRep DeltaCoin = Integer

toSpecRep (DeltaCoin x) = pure x

instance SpecTranslate ctx (PulsingRewUpdate c) where
type SpecRep (PulsingRewUpdate c) = Agda.HsRewardUpdate

toSpecRep x =
Agda.MkRewardUpdate
<$> toSpecRep deltaT
<*> toSpecRep deltaR
<*> toSpecRep deltaF
<*> toSpecRep rwds
where
(RewardUpdate {..}, _) = runShelleyBase $ completeRupd x
rwds = Set.foldMap rewardAmount <$> rs

instance
( EraPParams era
, ConwayEraGov era
Expand All @@ -191,8 +211,7 @@ instance
Agda.MkNewEpochState
<$> toSpecRep nesEL
<*> toSpecRep nesEs
-- TODO: replace with RewardUpdate
<*> pure Nothing
<*> toSpecRep nesRu

instance SpecTranslate ctx (ConwayNewEpochPredFailure era) where
type SpecRep (ConwayNewEpochPredFailure era) = OpaqueErrorString
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -22,6 +22,7 @@ library
cardano-ledger-conway:{cardano-ledger-conway, testlib},
cardano-ledger-conformance,
cardano-ledger-test,
constrained-generators,
data-default,
QuickCheck,
microlens
2 changes: 2 additions & 0 deletions libs/cardano-ledger-repl-environment/src/ReplEnvironment.hs
Original file line number Diff line number Diff line change
Expand Up @@ -50,3 +50,5 @@ import Test.Cardano.Ledger.Conway.ImpTest
import Test.Cardano.Ledger.Core.Rational

import Test.QuickCheck

import Constrained

0 comments on commit 9ec1e6b

Please sign in to comment.