Updated spec to fix a conformance failure

cabal.project

@@ -24,8 +24,8 @@ source-repository-package
   -- !WARNING!:
   -- MAKE SURE THIS POINTS TO A COMMIT IN `MAlonzo-code` BEFORE MERGE!
   subdir: generated
-  tag: 511c5632eff71f4811b48fba71e7aaadfd69211a
-  --sha256: sha256-J6Sbrr9Klz3N72wT2ZF02z5G6iFHjpwfUH2pFVoJr3c=
+  tag: cc93692f5a57a9a66956b232662152676f659954
+  --sha256: sha256-s9ikqfXmz1wBrk4qEFR/iOloKvMOPGTB5IpHO34NSLE=
 -- NOTE: If you would like to update the above, look for the `MAlonzo-code`
 -- branch in the `formal-ledger-specifications` repo and copy the SHA of
 -- the commit you need. The `MAlonzo-code` branch functions like an alternative

eras/alonzo/impl/src/Cardano/Ledger/Alonzo/Rules/Utxo.hs

@@ -227,6 +227,8 @@ newtype AlonzoUtxoEvent era
   = UtxosEvent (Event (EraRule "UTXOS" era))
   deriving (Generic)
 
+deriving instance Show (Event (EraRule "UTXOS" era)) => Show (AlonzoUtxoEvent era)
+
 deriving instance Eq (Event (EraRule "UTXOS" era)) => Eq (AlonzoUtxoEvent era)
 
 instance NFData (Event (EraRule "UTXOS" era)) => NFData (AlonzoUtxoEvent era)

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

@@ -29,6 +29,7 @@ import Cardano.Ledger.UMap as UMap
 import Cardano.Ledger.Val (Val (..))
 import Data.Functor ((<&>))
 import qualified Data.Map.Strict as Map
+import qualified Data.Sequence.Strict as SSeq
 import qualified Data.Set as Set
 import Lens.Micro ((%~), (&), (.~))
 import Test.Cardano.Ledger.Conway.Arbitrary ()
@@ -180,6 +181,47 @@ spec = do
                  ]
         expectNotRegistered (KeyHashObj kh)
 
+    it "deregistering returns the deposit" $ do
+      let
+        keyDeposit = Coin 2
+        -- This is paid out as the reward
+        govActionDeposit = Coin 3
+      modifyPParams $ \pp ->
+        pp
+          & ppKeyDepositL .~ keyDeposit
+          & ppGovActionDepositL .~ govActionDeposit
+      stakeCred <- KeyHashObj <$> freshKeyHash
+      rewardAccount <- registerStakeCredential stakeCred
+      otherStakeCred <- KeyHashObj <$> freshKeyHash
+      otherRewardAccount <- registerStakeCredential otherStakeCred
+      khStakePool <- freshKeyHash
+      registerPool khStakePool
+      submitTx_ . mkBasicTx $
+        mkBasicTxBody
+          & certsTxBodyL
+            .~ SSeq.fromList
+              [ DelegTxCert stakeCred (DelegStakeVote khStakePool DRepAlwaysAbstain)
+              , DelegTxCert otherStakeCred (DelegStakeVote khStakePool DRepAlwaysAbstain)
+              ]
+      expectRegisteredRewardAddress rewardAccount
+      expectRegisteredRewardAddress otherRewardAccount
+      submitAndExpireProposalToMakeReward otherStakeCred
+      lookupReward otherStakeCred `shouldReturn` govActionDeposit
+      submitTx_ . mkBasicTx $
+        mkBasicTxBody
+          & certsTxBodyL
+            .~ SSeq.fromList
+              [UnRegTxCert stakeCred]
+          & withdrawalsTxBodyL
+            .~ Withdrawals
+              ( Map.fromList
+                  [ (rewardAccount, Coin 0)
+                  , (otherRewardAccount, govActionDeposit)
+                  ]
+              )
+      lookupReward otherStakeCred `shouldReturn` Coin 0
+      expectNotRegisteredRewardAddress rewardAccount
+
   describe "Delegate stake" $ do
     it "Delegate registered stake credentials to registered pool" $ do
       expectedDeposit <- getsNES $ nesEsL . curPParamsEpochStateL . ppKeyDepositL

eras/conway/impl/testlib/Test/Cardano/Ledger/Conway/ImpTest.hs

@@ -158,8 +158,11 @@ import Cardano.Ledger.BaseTypes (
 import Cardano.Ledger.CertState (
   CertState,
   CommitteeAuthorization (..),
+  certDStateL,
   certPStateL,
   csCommitteeCredsL,
+  lookupDepositDState,
+  lookupDepositVState,
   psStakePoolParamsL,
   vsActualDRepExpiry,
   vsNumDormantEpochsL,
@@ -190,7 +193,7 @@ import Cardano.Ledger.Crypto (Crypto (..))
 import Cardano.Ledger.DRep
 import Cardano.Ledger.Keys (KeyHash, KeyRole (..))
 import Cardano.Ledger.Plutus.Language (Language (..), SLanguage (..), hashPlutusScript)
-import Cardano.Ledger.PoolParams (ppRewardAccount)
+import Cardano.Ledger.PoolParams (PoolParams (..), ppRewardAccount)
 import qualified Cardano.Ledger.Shelley.HardForks as HardForks (bootstrapPhase)
 import Cardano.Ledger.Shelley.LedgerState (
   IncrementalStake (..),
@@ -1756,25 +1759,28 @@ showConwayTxBalance ::
   String
 showConwayTxBalance pp certState utxo tx =
   unlines
-    [ "Consumed:   \t"
+    [ "Consumed:"
     , "\tInputs:     \t" <> show (coin inputs)
-    , -- , "Refunds:    \t" <> show refunds
-      "\tWithdrawals \t" <> show withdrawals
+    , "\tRefunds:    \t" <> show refunds
+    , "\tWithdrawals \t" <> show withdrawals
     , "\tTotal:      \t" <> (show . coin $ consumed pp certState utxo txBody)
     , ""
-    , "Produced:  \t"
+    , "Produced:"
     , "\tOutputs:   \t" <> show (coin $ sumAllValue (txBody ^. outputsTxBodyL))
     , "\tDonations: \t" <> show (txBody ^. treasuryDonationTxBodyL)
     , "\tDeposits:  \t" <> show (getTotalDepositsTxBody pp isRegPoolId txBody)
     , "\tFees:      \t" <> show (txBody ^. feeTxBodyL)
     , "\tTotal:     \t" <> (show . coin $ produced pp certState txBody)
     ]
   where
-    -- lookupStakingDeposit c = certState ^. certPStateL . psStakePoolParamsL
-    -- lookupDRepDeposit c = undefined
     txBody = tx ^. bodyTxL
     inputs = balance (txInsFilter utxo (txBody ^. inputsTxBodyL))
-    -- refunds = getTotalRefundsTxBody pp lookupStakingDeposit lookupDRepDeposit txBody
+    refunds =
+      getTotalRefundsTxBody
+        pp
+        (lookupDepositDState $ certState ^. certDStateL)
+        (lookupDepositVState $ certState ^. certVStateL)
+        txBody
     isRegPoolId = (`Map.member` (certState ^. certPStateL . psStakePoolParamsL))
     withdrawals = fold . unWithdrawals $ txBody ^. withdrawalsTxBodyL
 

eras/shelley/impl/CHANGELOG.md

@@ -35,6 +35,7 @@
 
 ### `testlib`
 
+* Added `tryLookupReward`
 * Switch to using `ImpSpec` package
 * Remove: `runImpTestM`, `runImpTestM_`, `evalImpTestM`, `execImpTestM`, `runImpTestGenM`, `runImpTestGenM_`, `evalImpTestGenM`, `execImpTestGenM`, `withImpState` and `withImpStateModified`.
 * Add `LedgerSpec`, `modifyImpInitProtVer`.

eras/shelley/impl/src/Cardano/Ledger/Shelley/Rules/Utxo.hs

@@ -127,6 +127,14 @@ instance EraPParams era => EncCBOR (UtxoEnv era) where
             !> To uePParams
             !> To ueCertState
 
+instance EraPParams era => DecCBOR (UtxoEnv era) where
+  decCBOR =
+    decode $
+      RecD UtxoEnv
+        <! From
+        <! From
+        <! D decNoShareCBOR
+
 utxoEnvSlotL :: Lens' (UtxoEnv era) SlotNo
 utxoEnvSlotL = lens ueSlot $ \x y -> x {ueSlot = y}
 

eras/shelley/impl/testlib/Test/Cardano/Ledger/Shelley/ImpTest.hs

@@ -71,6 +71,7 @@ module Test.Cardano.Ledger.Shelley.ImpTest (
   registerRewardAccount,
   registerStakeCredential,
   getRewardAccountFor,
+  tryLookupReward,
   lookupReward,
   poolParams,
   registerPool,
@@ -1447,17 +1448,22 @@ registerRewardAccount = do
   khDelegator <- freshKeyHash
   registerStakeCredential (KeyHashObj khDelegator)
 
+tryLookupReward :: Credential 'Staking (EraCrypto era) -> ImpTestM era (Maybe Coin)
+tryLookupReward stakingCredential = do
+  umap <- getsNES (nesEsL . epochStateUMapL)
+  pure $ fromCompact . rdReward <$> UMap.lookup stakingCredential (RewDepUView umap)
+
 lookupReward :: HasCallStack => Credential 'Staking (EraCrypto era) -> ImpTestM era Coin
 lookupReward stakingCredential = do
-  umap <- getsNES (nesEsL . epochStateUMapL)
-  case UMap.lookup stakingCredential (RewDepUView umap) of
+  mbyRwd <- tryLookupReward stakingCredential
+  case mbyRwd of
+    Just c -> pure c
     Nothing ->
       error $
         "Staking Credential is not found in the state: "
           <> show stakingCredential
           <> "\nMake sure you have the reward account registered with `registerRewardAccount` "
           <> "or by some other means."
-    Just rd -> pure $ fromCompact (rdReward rd)
 
 poolParams ::
   ShelleyEraImp era =>

libs/cardano-ledger-api/testlib/Test/Cardano/Ledger/Api/DebugTools.hs

@@ -1,23 +1,46 @@
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE OverloadedStrings #-}
 {-# LANGUAGE RankNTypes #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE TypeApplications #-}
 
 module Test.Cardano.Ledger.Api.DebugTools where
 
-import Cardano.Ledger.Binary (DecCBOR, EncCBOR, Version, decodeFull')
+import Cardano.Ledger.Binary (
+  Annotator,
+  DecCBOR (..),
+  DecShareCBOR,
+  EncCBOR,
+  Version,
+  decNoShareCBOR,
+  decodeFull',
+  decodeFullAnnotator,
+  decodeFullDecoder',
+ )
 import Cardano.Ledger.Binary.Encoding (serialize')
 import Cardano.Ledger.Core (Era, eraProtVerLow)
-import Control.Exception (throwIO)
+import Control.Exception (Exception, throwIO)
 import Control.Monad.IO.Class (MonadIO (..))
 import qualified Data.ByteString as BS
+import qualified Data.ByteString.Lazy as LBS
 
-readCBOR :: (DecCBOR a, MonadIO m) => Version -> FilePath -> m a
-readCBOR version path = liftIO $ do
+readCBORWith ::
+  (MonadIO m, Exception e) => (Version -> BS.ByteString -> Either e a) -> Version -> FilePath -> m a
+readCBORWith dec version path = liftIO $ do
   dat <- BS.readFile path
-  case decodeFull' version dat of
+  case dec version dat of
     Right x -> pure x
     Left err -> throwIO err
 
+readCBOR :: (DecCBOR a, MonadIO m) => Version -> FilePath -> m a
+readCBOR = readCBORWith decodeFull'
+
+readCBORNoShare :: (MonadIO m, DecShareCBOR a) => Version -> FilePath -> m a
+readCBORNoShare = readCBORWith (\v bs -> decodeFullDecoder' v "DecodeNoShare" decNoShareCBOR bs)
+
+readCBORAnnotated :: (MonadIO m, DecCBOR (Annotator a)) => Version -> FilePath -> m a
+readCBORAnnotated = readCBORWith (\v bs -> decodeFullAnnotator v "DecodeAnnotated" decCBOR (LBS.fromStrict bs))
+
 writeCBOR :: (EncCBOR a, MonadIO m) => Version -> FilePath -> a -> m ()
 writeCBOR version path = liftIO . BS.writeFile path . serialize' version
 

libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/ExecSpecRule/Conway/Base.hs

@@ -408,7 +408,7 @@ instance IsConwayUniv fn => ExecSpecRule fn "RATIFY" Conway where
       . computationResultToEither
       $ Agda.ratifyStep env st sig
 
-  extraInfo ctx env@RatifyEnv {..} st sig@(RatifySignal actions) =
+  extraInfo ctx env@RatifyEnv {..} st sig@(RatifySignal actions) _ =
     PP.vsep $ specExtraInfo : (actionAcceptedRatio <$> toList actions)
     where
       members = foldMap' (committeeMembers @Conway) $ ensCommittee (rsEnactState st)

libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/ExecSpecRule/Conway/Certs.hs

@@ -55,7 +55,7 @@ instance
     -- The results of runConformance are Agda types, the `ctx` is a Haskell type, we extract and translate the Withdrawal keys.
     specWithdrawalCredSet <-
       translateWithContext () (Map.keysSet (Map.mapKeys raCredential (ccecWithdrawals ctx)))
-    (implResTest, agdaResTest) <- runConformance @"CERTS" @fn @Conway ctx env st sig
+    (implResTest, agdaResTest, _) <- runConformance @"CERTS" @fn @Conway ctx env st sig
     case (implResTest, agdaResTest) of
       (Right haskell, Right spec) ->
         checkConformance @"CERTS" @Conway @fn

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

@@ -175,7 +175,7 @@ instance
         expectRightExpr $
           runSpecTransM ctx $
             bimapM (traverse toTestRep) (toTestRep . inject @_ @(ExecState fn "LEDGER" Conway) . fst) implRes
-    let extra = extraInfo @fn @"LEDGER" @Conway ctx (inject env) (inject st) (inject sig)
+    let extra = extraInfo @fn @"LEDGER" @Conway ctx (inject env) (inject st) (inject sig) implRes
     logDoc extra
     checkConformance @"LEDGER" @Conway @fn
       ctx

libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/ExecSpecRule/Conway/Utxo.hs

@@ -24,7 +24,9 @@ import qualified Data.List.NonEmpty as NE
 import qualified Data.Text as T
 import Lens.Micro ((&), (.~), (^.))
 import qualified Lib as Agda
-import Test.Cardano.Ledger.Common (Arbitrary (..), Gen)
+import Prettyprinter ((<+>))
+import qualified Prettyprinter as PP
+import Test.Cardano.Ledger.Common (Arbitrary (..), Gen, showExpr)
 import Test.Cardano.Ledger.Conformance (
   ExecSpecRule (..),
   OpaqueErrorString (..),
@@ -43,6 +45,7 @@ import Test.Cardano.Ledger.Constrained.Conway (
   utxoTxSpec,
  )
 import Test.Cardano.Ledger.Conway.ImpTest (showConwayTxBalance)
+import Test.Cardano.Ledger.Generic.Functions (TotalAda (..))
 import Test.Cardano.Ledger.Generic.GenState (
   GenEnv (..),
   GenSize (..),
@@ -100,14 +103,21 @@ instance
       . computationResultToEither
       $ Agda.utxoStep externalFunctions env st sig
 
-  extraInfo ctx env@UtxoEnv {..} st@UTxOState {..} sig =
-    "Impl:\n"
-      <> PP.ppString (showConwayTxBalance uePParams ueCertState utxosUtxo sig)
-      <> "\n\nSpec:\n"
-      <> PP.ppString
-        ( either show T.unpack . runSpecTransM ctx $
-            Agda.utxoDebug externalFunctions
-              <$> toSpecRep env
-              <*> toSpecRep st
-              <*> toSpecRep sig
-        )
+  extraInfo ctx env@UtxoEnv {..} st@UTxOState {..} sig st' =
+    PP.vcat
+      [ "Impl:"
+      , PP.ppString (showConwayTxBalance uePParams ueCertState utxosUtxo sig)
+      , "initial TotalAda:" <+> PP.ppString (showExpr $ totalAda st)
+      , "final TotalAda:  " <+> case st' of
+          Right (x, _) -> PP.ppString (showExpr $ totalAda x)
+          Left _ -> "N/A"
+      , mempty
+      , "Spec:"
+      , PP.ppString
+          ( either show T.unpack . runSpecTransM ctx $
+              Agda.utxoDebug externalFunctions
+                <$> toSpecRep env
+                <*> toSpecRep st
+                <*> toSpecRep sig
+          )
+      ]

libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/ExecSpecRule/Core.hs

@@ -213,8 +213,11 @@ class
     Environment (EraRule rule era) ->
     State (EraRule rule era) ->
     Signal (EraRule rule era) ->
+    Either
+      (NonEmpty (PredicateFailure (EraRule rule era)))
+      (State (EraRule rule era), [Event (EraRule rule era)]) ->
     Doc AnsiStyle
-  extraInfo _ _ _ _ = mempty
+  extraInfo _ _ _ _ _ = mempty
 
 dumpCbor ::
   forall era a.
@@ -266,10 +269,6 @@ checkConformance ctx env st sig implResTest agdaResTest = do
       annotate (color Yellow) . vsep $
         [ "===== DIFF ====="
         , ppEditExpr conformancePretty (ediff implResTest agdaResTest)
-        , ""
-        , "Legend:"
-        , indent 2 $ annotate (color delColor) "-Implementation"
-        , indent 2 $ annotate (color insColor) "+Specification"
         ]
   unless (implResTest == agdaResTest) $ do
     let envVarName = "CONFORMANCE_CBOR_DUMP_PATH"
@@ -315,8 +314,8 @@ defaultTestConformance ::
   ExecSignal fn rule era ->
   Property
 defaultTestConformance ctx env st sig = property $ do
-  (implResTest, agdaResTest) <- runConformance @rule @fn @era ctx env st sig
-  let extra = extraInfo @fn @rule @era ctx (inject env) (inject st) (inject sig)
+  (implResTest, agdaResTest, implRes) <- runConformance @rule @fn @era ctx env st sig
+  let extra = extraInfo @fn @rule @era ctx (inject env) (inject st) (inject sig) implRes
   logDoc extra
   checkConformance @rule @_ @fn ctx (inject env) (inject st) (inject sig) implResTest agdaResTest
 
@@ -345,6 +344,9 @@ runConformance ::
     , Either
         (NonEmpty (SpecRep (PredicateFailure (EraRule rule era))))
         (SpecRep (ExecState fn rule era))
+    , Either
+        (NonEmpty (PredicateFailure (EraRule rule era)))
+        (State (EraRule rule era), [Event (EraRule rule era)])
     )
 runConformance execContext env st sig = do
   (specEnv, specSt, specSig) <-
@@ -368,7 +370,7 @@ runConformance execContext env st sig = do
       expectRightExpr $
         runSpecTransM execContext $
           bimapM (traverse toTestRep) (toTestRep . inject @_ @(ExecState fn rule era) . fst) implRes
-  pure (implResTest, agdaResTest)
+  pure (implResTest, agdaResTest, implRes)
 
 conformsToImpl ::
   forall (rule :: Symbol) fn era.

libs/cardano-ledger-conformance/test/Test/Cardano/Ledger/Conformance/Imp/Ratify.hs

@@ -133,7 +133,7 @@ spec = withImpInit @(LedgerSpec Conway) $ describe "RATIFY" $ modifyImpInitProtV
     let
       ratSt = getRatifyState govSt
       ratSig = RatifySignal (constitutionGAS SSeq.:<| mempty)
-    (implRes, agdaRes) <-
+    (implRes, agdaRes, implRes') <-
       runConformance @"RATIFY" @ConwayFn @Conway
         execCtx
         ratEnv
@@ -158,4 +158,5 @@ spec = withImpInit @(LedgerSpec Conway) $ describe "RATIFY" $ modifyImpInitProtV
         ratEnv
         ratSt
         ratSig
+        implRes'
     impAnn "Conformance failed" $ implRes `shouldBeExpr` agdaRes

libs/cardano-ledger-repl-environment/cardano-ledger-repl-environment.cabal

@@ -25,4 +25,5 @@ library
         constrained-generators,
         data-default,
         QuickCheck,
+        ImpSpec,
         microlens