IntersectMBO · aniketd · Jun 28, 2024 · Jun 24, 2024
@@ -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

@@ -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

@@ -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
@@ -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
@@ -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
@@ -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,16 +1030,16 @@ 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
   type SpecRep (PState era) = Agda.PState
 
   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,16 +1286,40 @@ 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
     where
       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
 

@@ -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
@@ -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
@@ -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)