Merge pull request #5415 from IntersectMBO/fd/epoch-spec-rule

Run the specification rules of EPOCH and NEWEPOCH in conformance tests

Author: facundominguez

CONTRIBUTING.md

@@ -292,9 +292,11 @@ Below are instructions for some common use cases and workflow examples.
 
       - Extract the Haskell package using:
         ```shell
-        nix develop --command fls-shake hs
+        rm -rf dist/hs _build; nix develop --command fls-shake hs
         ```
         This generates the `cardano-ledger-executable-spec` Haskell package in `REPO/dist/hs`
+        Removing the `dist/hs` and `_build` folders ensures that no obsolete
+        modules are left together with the extracted code.
 
       In a local copy of `cardano-ledger` (with the `cabal.project` file _unmodified_):
 

cabal.project

@@ -16,7 +16,7 @@ source-repository-package
   subdir: hs
   -- !WARNING!:
   -- MAKE SURE THIS POINTS TO A COMMIT IN `*-artifacts` BEFORE MERGE!
-  tag: d84538c1ad6d8dc3cff4e59ead574daf84c88117
+  tag: 7a4c75d285595b7d21228a6208a99ca436aa88f4
 
 source-repository-package
   type: git

eras/conway/impl/testlib/Test/Cardano/Ledger/Conway/Imp/DelegSpec.hs

@@ -331,9 +331,7 @@ spec = do
       expectNotDelegatedVote cred
       expectNotDelegatedToAnyPool cred
 
-    -- https://github.com/IntersectMBO/formal-ledger-specifications/issues/917
-    -- TODO: Re-enable after issue is resolved, by removing this override
-    disableInConformanceIt "Delegate vote and unregister after hardfork" $ do
+    it "Delegate vote and unregister after hardfork" $ do
       let
         bootstrapVer = ProtVer (natVersion @9) 0
         setProtVer pv = modifyNES $ nesEsL . curPParamsEpochStateL . ppProtocolVersionL .~ pv
@@ -382,9 +380,7 @@ spec = do
             .~ Withdrawals (Map.singleton rewardAccount withdrawalAmount)
       expectStakeCredNotRegistered cred
       expectNotDelegatedVote cred
-    -- https://github.com/IntersectMBO/formal-ledger-specifications/issues/916
-    -- TODO: Re-enable after issue is resolved, by removing this override
-    disableInConformanceIt "Delegate vote and undelegate after delegating to some stake pools" $ do
+    it "Delegate vote and undelegate after delegating to some stake pools" $ do
       (khSPO, _, _) <- setupPoolWithStake $ Coin 1_000_000
       expectedDeposit <- getsNES $ nesEsL . curPParamsEpochStateL . ppKeyDepositL
       cred <- KeyHashObj <$> freshKeyHash
@@ -412,9 +408,7 @@ spec = do
       expectStakeCredNotRegistered cred
       expectNotDelegatedVote cred
 
-    -- https://github.com/IntersectMBO/formal-ledger-specifications/issues/640
-    -- TODO: Re-enable after issue is resolved, by removing this override
-    disableInConformanceIt "Delegate, retire and re-register pool" $ do
+    it "Delegate, retire and re-register pool" $ do
       expectedDeposit <- getsNES $ nesEsL . curPParamsEpochStateL . ppKeyDepositL
       cred <- KeyHashObj <$> freshKeyHash
       poolKh <- freshKeyHash

eras/conway/impl/testlib/Test/Cardano/Ledger/Conway/Imp/EnactSpec.hs

@@ -104,9 +104,7 @@ treasuryWithdrawalsSpec =
                    ]
       ensTreasury enactState'' `shouldBe` Coin 1
 
-    -- https://github.com/IntersectMBO/formal-ledger-specifications/issues/911
-    -- TODO: Re-enable after issues are resolved, by removing this override
-    disableInConformanceIt "Withdrawals exceeding treasury submitted in a single proposal" $ whenPostBootstrap $ do
+    it "Withdrawals exceeding treasury submitted in a single proposal" $ whenPostBootstrap $ do
       disableTreasuryExpansion
       committeeCs <- registerInitialCommittee
       (drepC, _, _) <- setupSingleDRep 1_000_000
@@ -138,43 +136,40 @@ treasuryWithdrawalsSpec =
       void $ enactTreasuryWithdrawals withdrawals drepC committeeCs
       checkNoWithdrawal initialTreasury withdrawals
 
-    -- https://github.com/IntersectMBO/formal-ledger-specifications/issues/912
-    -- TODO: Re-enable after issues are resolved, by removing this override
-    disableInConformanceIt
-      "Withdrawals exceeding treasury submitted in several proposals within the same epoch"
-      $ whenPostBootstrap
-      $ do
-        disableTreasuryExpansion
-        committeeCs <- registerInitialCommittee
-        (drepC, _, _) <- setupSingleDRep 1_000_000
-        donateToTreasury $ Coin 5_000_000
-        initialTreasury <- getsNES treasuryL
-        numWithdrawals <- choose (1, 10)
-        withdrawals <- genWithdrawalsExceeding initialTreasury numWithdrawals
-
-        impAnn "submit in individual proposals in the same epoch" $ do
-          traverse_
-            ( \w -> do
-                gaId <- submitTreasuryWithdrawals @era [w]
-                submitYesVote_ (DRepVoter drepC) gaId
-                submitYesVoteCCs_ committeeCs gaId
-            )
-            withdrawals
-          passNEpochs 2
+    it "Withdrawals exceeding treasury submitted in several proposals within the same epoch" $
+      whenPostBootstrap $
+        do
+          disableTreasuryExpansion
+          committeeCs <- registerInitialCommittee
+          (drepC, _, _) <- setupSingleDRep 1_000_000
+          donateToTreasury $ Coin 5_000_000
+          initialTreasury <- getsNES treasuryL
+          numWithdrawals <- choose (1, 10)
+          withdrawals <- genWithdrawalsExceeding initialTreasury numWithdrawals
+
+          impAnn "submit in individual proposals in the same epoch" $ do
+            traverse_
+              ( \w -> do
+                  gaId <- submitTreasuryWithdrawals @era [w]
+                  submitYesVote_ (DRepVoter drepC) gaId
+                  submitYesVoteCCs_ committeeCs gaId
+              )
+              withdrawals
+            passNEpochs 2
+
+            let expectedTreasury =
+                  F.foldl'
+                    ( \acc (_, x) ->
+                        if acc >= x
+                          then acc <-> x
+                          else acc
+                    )
+                    initialTreasury
+                    withdrawals
 
-          let expectedTreasury =
-                F.foldl'
-                  ( \acc (_, x) ->
-                      if acc >= x
-                        then acc <-> x
-                        else acc
-                  )
-                  initialTreasury
-                  withdrawals
-
-          getsNES treasuryL `shouldReturn` expectedTreasury
-          -- check that the sum of the rewards matches what was spent from the treasury
-          sumRewardAccounts withdrawals `shouldReturn` (initialTreasury <-> expectedTreasury)
+            getsNES treasuryL `shouldReturn` expectedTreasury
+            -- check that the sum of the rewards matches what was spent from the treasury
+            sumRewardAccounts withdrawals `shouldReturn` (initialTreasury <-> expectedTreasury)
   where
     sumRewardAccounts withdrawals = mconcat <$> traverse (getAccountBalance . fst) withdrawals
     genWithdrawalsExceeding (Coin val) n = do

eras/conway/impl/testlib/Test/Cardano/Ledger/Conway/Imp/UtxoSpec.hs

@@ -40,9 +40,7 @@ import Test.Cardano.Ledger.Plutus.Examples (alwaysSucceedsNoDatum)
 spec :: forall era. ConwayEraImp era => SpecWith (ImpInit (LedgerSpec era))
 spec = do
   describe "Certificates" $ do
-    -- https://github.com/IntersectMBO/formal-ledger-specifications/issues/926
-    -- TODO: Re-enable after issues are resolved, by removing this override
-    disableInConformanceIt "Reg/UnReg collect and refund correct amounts" $ do
+    it "Reg/UnReg collect and refund correct amounts" $ do
       utxoStart <- getUTxO
       accountDeposit <- getsPParams ppKeyDepositL
       stakePoolDeposit <- getsPParams ppPoolDepositL

eras/shelley/impl/testlib/Test/Cardano/Ledger/Shelley/Imp/DelegSpec.hs

@@ -189,10 +189,7 @@ spec = do
           )
           [injectFailure $ StakeKeyNotRegisteredDELEG (KeyHashObj kh)]
 
-    -- https://github.com/IntersectMBO/formal-ledger-specifications/issues/917
-    -- impacts `registerAndRetirePoolToMakeReward`
-    -- TODO: Re-enable after issue is resolved, by removing this override
-    disableInConformanceIt "With non-zero reward balance" $ do
+    it "With non-zero reward balance" $ do
       cred <- KeyHashObj <$> freshKeyHash
       regTxCert <- genRegTxCert cred
 

flake.lock

@@ -253,5 +253,17 @@ instance
   toSpecRep (NewEpochState {..}) =
     Agda.MkNewEpochState
       <$> toSpecRep nesEL
+      <*> toSpecRep nesBprev
+      <*> toSpecRep nesBcur
       <*> toSpecRep nesEs
       <*> toSpecRep nesRu
+      <*> (filterZeroEntries <$> toSpecRep nesPd)
+    where
+      -- The specification does not include zero entries in general
+      -- while the implementation might. So we filter them out here for the sake
+      -- of comparing results.
+      --
+      -- The discrepancy is discussed here:
+      -- https://github.com/IntersectMBO/cardano-ledger/issues/5306
+      filterZeroEntries (Agda.MkHSMap lst) =
+        Agda.MkHSMap $ filter ((/= 0) . snd) lst

libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/SpecTranslate/Conway/Cert.hs

@@ -24,6 +24,7 @@ import Cardano.Crypto.DSIGN (DSIGNAlgorithm (..), SignedDSIGN (..))
 import Cardano.Crypto.Util (bytesToNatural, naturalToBytes)
 import Cardano.Ledger.Address (Addr (..), BootstrapAddress (..), RewardAccount (..))
 import Cardano.Ledger.BaseTypes (
+  BlocksMade (..),
   EpochInterval (..),
   EpochNo (..),
   Network (..),
@@ -57,10 +58,13 @@ import Cardano.Ledger.Plutus.CostModels (CostModels)
 import Cardano.Ledger.Plutus.Data (BinaryData, Data, Datum (..), hashBinaryData)
 import Cardano.Ledger.Plutus.ExUnits (ExUnits (..), Prices)
 import Cardano.Ledger.TxIn (TxId (..), TxIn (..))
+import Control.Monad (forM)
 import Control.Monad.Except (throwError)
 import Data.Functor.Identity (Identity (..))
 import Data.Map (Map)
+import qualified Data.Map as Map
 import Data.Maybe.Strict (StrictMaybe (..))
+import GHC.Natural (naturalToInteger)
 import qualified MAlonzo.Code.Ledger.Foreign.API as Agda
 import Test.Cardano.Ledger.Conformance.SpecTranslate.Base (
   SpecTranslate (..),
@@ -271,3 +275,12 @@ instance SpecTranslate ctx PoolDistr where
   type SpecRep PoolDistr = Agda.HSMap (SpecRep (KeyHash StakePool)) Agda.Coin
 
   toSpecRep (PoolDistr ps _) = toSpecRep ps
+
+instance SpecTranslate ctx BlocksMade where
+  type SpecRep BlocksMade = Agda.HSMap Integer Integer
+
+  toSpecRep (BlocksMade m) = do
+    xs <- forM (Map.toList m) $ \(k, v) -> do
+      k' <- toSpecRep k
+      pure (k', naturalToInteger v)
+    pure $ Agda.MkHSMap xs