diff --git a/cabal.project b/cabal.project index 5343f9e2cab..3f5ea89111d 100644 --- a/cabal.project +++ b/cabal.project @@ -17,8 +17,8 @@ repository cardano-haskell-packages source-repository-package type: git location: https://github.com/input-output-hk/cardano-ledger-executable-spec.git - tag: cb9359ade4dd20a13a0e5c384b04411de29b0329 - --sha256: sha256-ADPVfitVyXn3AXJTYfLK8rHVIzCj4APMrCghgoi35cE= + tag: cca9017a658435af2416367d7c9314f7e3b4e643 + --sha256: sha256-SkWjjjET2Ou1e1iFupemb5icBToM1ezS4XMEzLzumBQ= index-state: -- Bump this if you need newer packages from Hackage diff --git a/libs/cardano-ledger-conformance/cardano-ledger-conformance.cabal b/libs/cardano-ledger-conformance/cardano-ledger-conformance.cabal index e83e33fecc9..986294af270 100644 --- a/libs/cardano-ledger-conformance/cardano-ledger-conformance.cabal +++ b/libs/cardano-ledger-conformance/cardano-ledger-conformance.cabal @@ -62,7 +62,8 @@ library deepseq, small-steps >=1.1, text, - unliftio + unliftio, + vector-map if !impl(ghc >=9.2) ghc-options: -Wno-incomplete-patterns diff --git a/libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance.hs b/libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance.hs index e386572239e..087a89f11be 100644 --- a/libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance.hs +++ b/libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance.hs @@ -1,8 +1,10 @@ module Test.Cardano.Ledger.Conformance ( module Test.Cardano.Ledger.Conformance.ExecSpecRule.Core, module Test.Cardano.Ledger.Conformance.SpecTranslate.Core, + module Test.Cardano.Ledger.Conformance.Utils, ) where import Test.Cardano.Ledger.Conformance.ExecSpecRule.Core import Test.Cardano.Ledger.Conformance.Orphans () import Test.Cardano.Ledger.Conformance.SpecTranslate.Core +import Test.Cardano.Ledger.Conformance.Utils diff --git a/libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/Orphans.hs b/libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/Orphans.hs index b184ba6e641..83569245597 100644 --- a/libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/Orphans.hs +++ b/libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/Orphans.hs @@ -63,6 +63,10 @@ deriving instance Generic NewEpochEnv deriving instance Generic EpochState +deriving instance Generic Snapshots + +deriving instance Generic Snapshot + deriving instance Generic LedgerState deriving instance Generic Acnt @@ -141,6 +145,10 @@ deriving instance Eq RatifyState deriving instance Eq EpochState +deriving instance Eq Snapshots + +deriving instance Eq Snapshot + deriving instance Eq Acnt deriving instance Eq LedgerState @@ -221,6 +229,10 @@ instance NFData NewEpochEnv instance NFData EpochState +instance NFData Snapshots + +instance NFData Snapshot + instance NFData Acnt instance NFData LedgerState @@ -304,6 +316,10 @@ instance ToExpr NewEpochEnv instance ToExpr EpochState +instance ToExpr Snapshots + +instance ToExpr Snapshot + instance ToExpr LedgerState instance ToExpr Acnt @@ -386,6 +402,10 @@ instance FixupSpecRep RatifyState instance FixupSpecRep EpochState +instance FixupSpecRep Snapshots + +instance FixupSpecRep Snapshot + instance FixupSpecRep Acnt instance FixupSpecRep LedgerState diff --git a/libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/Spec/Conway.hs b/libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/Spec/Conway.hs index 5332eb5ad8d..e1eaea3e6df 100644 --- a/libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/Spec/Conway.hs +++ b/libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/Spec/Conway.hs @@ -13,16 +13,7 @@ import Test.Cardano.Ledger.Conway.ImpTest () import Test.Cardano.Ledger.Imp.Common spec :: Spec -spec = describe "Conway conformance tests" $ do - xprop "UTXO" $ conformsToImpl @"UTXO" @ConwayFn @Conway - prop "GOV" $ conformsToImpl @"GOV" @ConwayFn @Conway - prop "CERT" $ conformsToImpl @"CERT" @ConwayFn @Conway - xprop "RATIFY" $ conformsToImpl @"RATIFY" @ConwayFn @Conway - xprop "GOVCERT" $ conformsToImpl @"GOVCERT" @ConwayFn @Conway - xprop "ENACT" $ conformsToImpl @"ENACT" @ConwayFn @Conway - prop "DELEG" $ conformsToImpl @"DELEG" @ConwayFn @Conway - prop "POOL" $ conformsToImpl @"POOL" @ConwayFn @Conway - xprop "EPOCH" $ conformsToImpl @"EPOCH" @ConwayFn @Conway +spec = do describe "Generators" $ do let genEnv = do @@ -40,3 +31,16 @@ spec = describe "Conway conformance tests" $ do genEnv `generatesWithin` 3_000_000 genSt `generatesWithin` 40_000_000 genSig `generatesWithin` 60_000_000 + describe "Conformance" $ do + describe "Ticks transition graph" $ do + xprop "ENACT" $ conformsToImpl @"ENACT" @ConwayFn @Conway + xprop "RATIFY" $ conformsToImpl @"RATIFY" @ConwayFn @Conway + xprop "EPOCH" $ conformsToImpl @"EPOCH" @ConwayFn @Conway + xprop "NEWEPOCH" $ conformsToImpl @"EPOCH" @ConwayFn @Conway + describe "Blocks transition graph" $ do + prop "DELEG" $ conformsToImpl @"DELEG" @ConwayFn @Conway + xprop "GOVCERT" $ conformsToImpl @"GOVCERT" @ConwayFn @Conway + prop "POOL" $ conformsToImpl @"POOL" @ConwayFn @Conway + prop "CERT" $ conformsToImpl @"CERT" @ConwayFn @Conway + prop "GOV" $ conformsToImpl @"GOV" @ConwayFn @Conway + xprop "UTXO" $ conformsToImpl @"UTXO" @ConwayFn @Conway diff --git a/libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/SpecTranslate/Conway.hs b/libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/SpecTranslate/Conway.hs index 046947f54ef..58dfd251596 100644 --- a/libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/SpecTranslate/Conway.hs +++ b/libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/SpecTranslate/Conway.hs @@ -25,7 +25,7 @@ module Test.Cardano.Ledger.Conformance.SpecTranslate.Conway ( ) where import Cardano.Crypto.DSIGN (DSIGNAlgorithm (..), SignedDSIGN (..)) -import Cardano.Crypto.Hash (Hash, hashToBytes) +import Cardano.Crypto.Hash (Hash) import Cardano.Crypto.Util (bytesToNatural) import Cardano.Ledger.Address (Addr (..), RewardAccount (..), serialiseAddr) import Cardano.Ledger.Alonzo (AlonzoTxAuxData, MaryValue) @@ -65,6 +65,7 @@ import Cardano.Ledger.Conway.TxCert ( import Cardano.Ledger.Credential (Credential (..)) import Cardano.Ledger.Crypto (Crypto (..)) import Cardano.Ledger.DRep (DRep (..), DRepState (..)) +import Cardano.Ledger.EpochBoundary (SnapShot (..), SnapShots (..), Stake (..)) import Cardano.Ledger.HKD (HKD) import Cardano.Ledger.Keys (KeyHash (..), KeyRole (..), VKey (..)) import Cardano.Ledger.Keys.WitVKey (WitVKey (..)) @@ -97,6 +98,7 @@ import Data.Set (Set) import qualified Data.Set as Set import qualified Data.Text as T import Data.Traversable (forM) +import qualified Data.VMap as VMap import Data.Void (Void, absurd) import Data.Word (Word32, Word64) import GHC.Generics (Generic) @@ -109,6 +111,7 @@ import Test.Cardano.Ledger.Conformance ( SpecTranslate (..), SpecTranslationError, askCtx, + hashToInteger, ) import Test.Cardano.Ledger.Constrained.Conway (IsConwayUniv) import Test.Cardano.Ledger.Constrained.Conway.Epoch @@ -343,6 +346,7 @@ instance Agda.MkUTxOEnv <$> toSpecRep (ueSlot x) <*> toSpecRep (uePParams x) + <*> toSpecRep (Coin 10000000) -- TODO: Fix generating types instance SpecTranslate ctx a => SpecTranslate ctx (Set a) where type SpecRep (Set a) = Agda.HSSet (SpecRep a) @@ -366,8 +370,7 @@ instance SpecTranslate ctx ValidityInterval where instance SpecTranslate ctx (Hash a b) where type SpecRep (Hash a b) = Agda.Hash - - toSpecRep = pure . toInteger . bytesToNatural . hashToBytes + toSpecRep = pure . hashToInteger deriving instance SpecTranslate ctx (KeyHash r c) @@ -534,13 +537,13 @@ instance SpecTranslate ctx (ConwayTxCert era) where instance SpecTranslate ctx (PoolCert c) where type SpecRep (PoolCert c) = Agda.TxCert - toSpecRep (RegPool p@PoolParams {ppId}) = + toSpecRep (RegPool p@PoolParams {ppId = KeyHash ppHash}) = Agda.RegPool - <$> toSpecRep (KeyHashObj ppId) + <$> toSpecRep ppHash <*> toSpecRep p - toSpecRep (RetirePool kh e) = + toSpecRep (RetirePool (KeyHash ppHash) e) = Agda.RetirePool - <$> toSpecRep (KeyHashObj kh) + <$> toSpecRep ppHash <*> toSpecRep e instance SpecTranslate ctx (ConwayGovCert c) where @@ -1027,7 +1030,7 @@ instance SpecTranslate ctx (DState era) where toSpecRep DState {..} = Agda.MkDState <$> toSpecRep (dRepMap dsUnified) - <*> toSpecRep (KeyHashObj <$> sPoolMap dsUnified) + <*> toSpecRep (sPoolMap dsUnified) <*> toSpecRep (rewardMap dsUnified) instance SpecTranslate ctx (PState era) where @@ -1035,8 +1038,8 @@ instance SpecTranslate ctx (PState era) where toSpecRep PState {..} = Agda.MkPState - <$> toSpecRep (mapKeys KeyHashObj psStakePoolParams) - <*> toSpecRep (mapKeys KeyHashObj psRetiring) + <$> toSpecRep (mapKeys (hashToInteger . unKeyHash) psStakePoolParams) + <*> toSpecRep (mapKeys (hashToInteger . unKeyHash) psRetiring) committeeCredentialToStrictMaybe :: CommitteeAuthorization c -> @@ -1187,17 +1190,8 @@ instance HasSimpleRep (EpochExecEnv era) instance (IsConwayUniv fn, Era era) => HasSpec fn (EpochExecEnv era) instance SpecTranslate ctx (EpochExecEnv era) where - type SpecRep (EpochExecEnv era) = Agda.NewEpochEnv - - toSpecRep (EpochExecEnv stakeDistr) = do - let - transStakeDistr (c, s) = do - c' <- toSpecRep c - s' <- toSpecRep s - pure (Agda.CredVoter Agda.SPO c', s') - stakeDistrsMap = traverse transStakeDistr $ Map.toList stakeDistr - stakeDistrs = Agda.MkStakeDistrs . Agda.MkHSMap <$> stakeDistrsMap - Agda.MkNewEpochEnv <$> stakeDistrs + type SpecRep (EpochExecEnv era) = () + toSpecRep _ = pure () data ConwayExecEnactEnv era = ConwayExecEnactEnv { ceeeGid :: GovActionId (EraCrypto era) @@ -1235,7 +1229,7 @@ instance toSpecRep ConwayDelegEnv {..} = Agda.MkDelegEnv <$> toSpecRep cdePParams - <*> toSpecRep (Map.mapKeys KeyHashObj cdePools) + <*> toSpecRep (Map.mapKeys (hashToInteger . unKeyHash) cdePools) instance SpecTranslate ctx (ConwayDelegCert c) where type SpecRep (ConwayDelegCert c) = Agda.TxCert @@ -1247,13 +1241,13 @@ instance SpecTranslate ctx (ConwayDelegCert c) where Agda.Delegate <$> toSpecRep c <*> toSpecRep (getVoteDelegatee d) - <*> toSpecRep (KeyHashObj <$> getStakePoolDelegatee d) + <*> toSpecRep (hashToInteger . unKeyHash <$> getStakePoolDelegatee d) <*> pure 0 toSpecRep (ConwayRegDelegCert s d c) = Agda.Delegate <$> toSpecRep s <*> toSpecRep (getVoteDelegatee d) - <*> toSpecRep (KeyHashObj <$> getStakePoolDelegatee d) + <*> toSpecRep (hashToInteger . unKeyHash <$> getStakePoolDelegatee d) <*> toSpecRep c instance SpecTranslate ctx (ConwayDelegPredFailure era) where @@ -1292,9 +1286,10 @@ instance where type SpecRep (EpochState era) = Agda.EpochState - toSpecRep (EpochState {esLState = esLState@LedgerState {..}, ..}) = + toSpecRep (EpochState {esLState = esLState@LedgerState {lsUTxOState}, ..}) = Agda.MkEpochState <$> toSpecRep esAccountState + <*> toSpecRep esSnapshots <*> toSpecRep esLState <*> toSpecRep enactState <*> toSpecRep ratifyState @@ -1302,6 +1297,29 @@ instance enactState = mkEnactState $ utxosGovState lsUTxOState ratifyState = RatifyState enactState mempty mempty False +instance SpecTranslate ctx (SnapShots c) where + type SpecRep (SnapShots c) = Agda.Snapshots + + toSpecRep (SnapShots {..}) = + Agda.MkSnapshots + <$> toSpecRep ssStakeMark + <*> toSpecRep ssStakeSet + <*> toSpecRep ssStakeGo + <*> toSpecRep ssFee + +instance SpecTranslate ctx (SnapShot c) where + type SpecRep (SnapShot c) = Agda.Snapshot + + toSpecRep (SnapShot {..}) = + Agda.MkSnapshot + <$> toSpecRep ssStake + <*> toSpecRep (VMap.toMap ssDelegations) + +instance SpecTranslate ctx (Stake c) where + type SpecRep (Stake c) = Agda.HSMap Agda.Credential Agda.Coin + + toSpecRep (Stake stake) = toSpecRep $ VMap.toMap stake + instance SpecTranslate ctx AccountState where type SpecRep AccountState = Agda.Acnt diff --git a/libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/Utils.hs b/libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/Utils.hs index 6cefb7d367e..03fd62eb31b 100644 --- a/libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/Utils.hs +++ b/libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/Utils.hs @@ -1,7 +1,7 @@ module Test.Cardano.Ledger.Conformance.Utils where -import Cardano.Crypto.Hash (ByteString) -import Cardano.Crypto.Util (naturalToBytes) +import Cardano.Crypto.Hash (ByteString, Hash, hashToBytes) +import Cardano.Crypto.Util (bytesToNatural, naturalToBytes) import qualified Data.ByteString.Base16 as B16 import Test.Cardano.Ledger.TreeDiff (Expr, ToExpr (..)) @@ -10,3 +10,6 @@ agdaHashToBytes hashSize = B16.encode . naturalToBytes hashSize . fromInteger agdaHashToExpr :: Int -> Integer -> Expr agdaHashToExpr hashSize = toExpr . agdaHashToBytes hashSize + +hashToInteger :: Hash a b -> Integer +hashToInteger = toInteger . bytesToNatural . hashToBytes diff --git a/libs/cardano-ledger-conformance/test/Main.hs b/libs/cardano-ledger-conformance/test/Main.hs index 40a8af13dc7..d74c135b695 100644 --- a/libs/cardano-ledger-conformance/test/Main.hs +++ b/libs/cardano-ledger-conformance/test/Main.hs @@ -10,6 +10,5 @@ import qualified Test.Cardano.Ledger.Conformance.Spec.Conway as Conway main :: IO () main = ledgerTestMain $ do - describe "Conformance" $ do - Conway.spec - ConformanceSpec.spec + describe "ConformaceSpec" $ ConformanceSpec.spec + describe "Conway" $ Conway.spec diff --git a/libs/cardano-ledger-core/src/Cardano/Ledger/Keys/Internal.hs b/libs/cardano-ledger-core/src/Cardano/Ledger/Keys/Internal.hs index 9d0916b50fb..5c2fd62701f 100644 --- a/libs/cardano-ledger-core/src/Cardano/Ledger/Keys/Internal.hs +++ b/libs/cardano-ledger-core/src/Cardano/Ledger/Keys/Internal.hs @@ -226,8 +226,8 @@ hashSignature = Hash.hashWith (DSIGN.rawSerialiseSigDSIGN . coerce) -------------------------------------------------------------------------------- -- | Discriminated hash of public Key -newtype KeyHash (discriminator :: KeyRole) c - = KeyHash (Hash.Hash (ADDRHASH c) (DSIGN.VerKeyDSIGN (DSIGN c))) +newtype KeyHash (discriminator :: KeyRole) c = KeyHash + {unKeyHash :: Hash.Hash (ADDRHASH c) (DSIGN.VerKeyDSIGN (DSIGN c))} deriving (Show, Eq, Ord) deriving newtype (NFData, NoThunks, Generic)