Merge branch 'master' into nm/fix-haddock-generation

cabal.project

@@ -24,8 +24,8 @@ source-repository-package
   -- !WARNING!:
   -- MAKE SURE THIS POINTS TO A COMMIT IN `MAlonzo-code` BEFORE MERGE!
   subdir: generated
-  --sha256: sha256-fzvk/UcLDZbC+pe9K6gao8JQ/al+L+KdzyPxAaL1xiM=
-  tag: 098ebf75fc06635bf0a38a82f4086bbd840af7c0
+  --sha256: sha256-CebCHTM0lvIAJ5lx0LRcMEDeU4nGVWJlkvhJPE5tI9Y=
+  tag: 0f9eb79886f4d45a2cbb241af49b9e199735bd37
 
 -- 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

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

@@ -159,3 +159,14 @@ spec = do
         submitFailingTx
           registerHotKeyTx
           (pure . injectFailure $ ConwayCommitteeHasPreviouslyResigned ccCred)
+    it "resigning a nonexistent CC member hotkey" $ do
+      void registerInitialCommittee
+      nonExistentColdKey <- KeyHashObj <$> freshKeyHash
+      let failingTx =
+            mkBasicTx mkBasicTxBody
+              & bodyTxL . certsTxBodyL
+                .~ SSeq.singleton (ResignCommitteeColdTxCert nonExistentColdKey SNothing)
+      submitFailingTx
+        failingTx
+        [ injectFailure $ ConwayCommitteeIsUnknown nonExistentColdKey
+        ]

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

@@ -25,7 +25,7 @@ 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 Data.Map.Strict (Map, keysSet)
 import qualified Data.VMap as VMap
 import Lens.Micro
 import qualified Lib as Agda
@@ -49,11 +49,13 @@ instance
   toSpecRep CertEnv {..} = do
     votes <- askCtx @(VotingProcedures era)
     withdrawals <- askCtx @(Map RewardAccount Coin)
+    let ccColdCreds = foldMap (keysSet . committeeMembers) ceCurrentCommittee
     Agda.MkCertEnv
       <$> toSpecRep ceCurrentEpoch
       <*> toSpecRep cePParams
       <*> toSpecRep votes
       <*> toSpecRep withdrawals
+      <*> toSpecRep ccColdCreds
 
 instance SpecTranslate ctx (CertState era) where
   type SpecRep (CertState era) = Agda.CertState

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

@@ -19,6 +19,7 @@ import Cardano.Ledger.Conway.Core
 import Cardano.Ledger.Conway.Governance
 import Cardano.Ledger.Conway.Rules
 import Data.Functor.Identity (Identity)
+import Data.Map (keysSet)
 import Data.Map.Strict (Map)
 import qualified Lib as Agda
 import Test.Cardano.Ledger.Conformance
@@ -42,8 +43,10 @@ instance
   toSpecRep CertsEnv {..} = do
     votes <- askCtx @(VotingProcedures era)
     withdrawals <- askCtx @(Map RewardAccount Coin)
+    let ccColdCreds = foldMap (keysSet . committeeMembers) certsCurrentCommittee
     Agda.MkCertEnv
       <$> toSpecRep certsCurrentEpoch
       <*> toSpecRep certsPParams
       <*> toSpecRep votes
       <*> toSpecRep withdrawals
+      <*> toSpecRep ccColdCreds

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

@@ -62,7 +62,7 @@ instance SpecTranslate ctx ConwayDelegCert where
   toSpecRep (ConwayUnRegCert c d) =
     Agda.Dereg
       <$> toSpecRep c
-      <*> strictMaybe (pure 0) toSpecRep d
+      <*> toSpecRep d
   toSpecRep (ConwayDelegCert c d) =
     Agda.Delegate
       <$> toSpecRep c

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

@@ -33,8 +33,9 @@ import Cardano.Ledger.Credential (Credential (..))
 import Cardano.Ledger.Shelley.LedgerState
 import Data.Default (Default (..))
 import Data.Functor.Identity (Identity)
-import Data.Map.Strict (Map)
+import Data.Map.Strict (Map, keysSet)
 import qualified Data.Map.Strict as Map
+import Data.Maybe (mapMaybe)
 import qualified Lib as Agda
 import Test.Cardano.Ledger.Conformance.SpecTranslate.Conway.Base
 import Test.Cardano.Ledger.Conformance.SpecTranslate.Core
@@ -78,11 +79,21 @@ instance
   toSpecRep ConwayGovCertEnv {..} = do
     votes <- askCtx @(VotingProcedures era)
     withdrawals <- askCtx @(Map RewardAccount Coin)
+    let propGetCCMembers (UpdateCommittee _ _ x _) = Just $ keysSet x
+        propGetCCMembers _ = Nothing
+        potentialCCMembers =
+          mconcat
+            . mapMaybe (propGetCCMembers . pProcGovAction . gasProposalProcedure)
+            . Map.elems
+        ccColdCreds =
+          foldMap (keysSet . committeeMembers) cgceCurrentCommittee
+            <> potentialCCMembers cgceCommitteeProposals
     Agda.MkCertEnv
       <$> toSpecRep cgceCurrentEpoch
       <*> toSpecRep cgcePParams
       <*> toSpecRep votes
       <*> toSpecRep withdrawals
+      <*> toSpecRep ccColdCreds
 
 instance SpecTranslate ctx (ConwayGovCertPredFailure era) where
   type SpecRep (ConwayGovCertPredFailure era) = OpaqueErrorString

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

@@ -160,7 +160,7 @@ spec =
           -- GOVCERT tests enabling pending on these two issues in spec:
           -- /~https://github.com/IntersectMBO/formal-ledger-specifications/issues/634
           -- /~https://github.com/IntersectMBO/formal-ledger-specifications/issues/633
-          xdescribe "GOVCERT" GovCert.spec
+          describe "GOVCERT" GovCert.spec
           -- LEDGER tests enabling pending (at least) on the implementation of scriptSize in the spec:
           -- /~https://github.com/IntersectMBO/formal-ledger-specifications/issues/620
           xdescribe "LEDGER" Ledger.spec

libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/Instances/Basic.hs

@@ -51,6 +51,7 @@ import Cardano.Ledger.Plutus.CostModels (CostModels)
 import Cardano.Ledger.Plutus.ExUnits
 import Cardano.Ledger.Shelley.PParams (ProposedPPUpdates (..))
 import Constrained hiding (Value)
+import Constrained.Base (genListWithSize)
 import Constrained.Univ ()
 import Control.Monad.Identity (Identity (..))
 import Control.Monad.Trans.Fail.String
@@ -95,6 +96,10 @@ instance BaseUniverse fn => Foldy fn Coin where
   genList s s' = map fromSimpleRep <$> genList @fn @Word64 (toSimpleRepSpec s) (toSimpleRepSpec s')
   theAddFn = addFn
   theZero = Coin 0
+  genSizedList sz elemSpec foldSpec =
+    map fromSimpleRep
+      <$> genListWithSize @fn @Word64 sz (toSimpleRepSpec elemSpec) (toSimpleRepSpec foldSpec)
+  noNegativeValues = True
 
 -- TODO: This is hack to get around the need for `Num` in `NumLike`. We should possibly split
 -- this up so that `NumLike` has its own addition etc. instead?

libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/Instances/Ledger.hs

@@ -128,7 +128,14 @@ import Cardano.Ledger.UTxO
 import Cardano.Ledger.Val (Val)
 import Constrained hiding (Sized, Value)
 import Constrained qualified as C
-import Constrained.Base (Binder (..), HasGenHint (..), Pred (..), Term (..), explainSpecOpt)
+import Constrained.Base (
+  Binder (..),
+  HasGenHint (..),
+  Pred (..),
+  Term (..),
+  explainSpecOpt,
+  genListWithSize,
+ )
 import Constrained.Spec.Map
 import Control.DeepSeq (NFData)
 import Crypto.Hash (Blake2b_224)
@@ -250,6 +257,10 @@ instance IsConwayUniv fn => Foldy fn DeltaCoin where
   genList s s' = map fromSimpleRep <$> genList @fn @Integer (toSimpleRepSpec s) (toSimpleRepSpec s')
   theAddFn = addFn
   theZero = DeltaCoin 0
+  genSizedList sz elemSpec foldSpec =
+    map fromSimpleRep
+      <$> genListWithSize @fn @Integer sz (toSimpleRepSpec elemSpec) (toSimpleRepSpec foldSpec)
+  noNegativeValues = False
 
 deriving via Integer instance Num DeltaCoin
 

libs/constrained-generators/constrained-generators.cabal

@@ -26,6 +26,7 @@ library
     Constrained.Examples.Basic
     Constrained.Examples.CheatSheet
     Constrained.Examples.Either
+    Constrained.Examples.Fold
     Constrained.Examples.List
     Constrained.Examples.Map
     Constrained.Examples.Set
@@ -41,6 +42,7 @@ library
     Constrained.Spec.Map
     Constrained.Spec.Pairs
     Constrained.Spec.Tree
+    Constrained.SumList
     Constrained.Syntax
     Constrained.Univ