diff --git a/cabal.project b/cabal.project index 34e0279d071..4a9ab89c282 100644 --- a/cabal.project +++ b/cabal.project @@ -13,8 +13,8 @@ repository cardano-haskell-packages source-repository-package type: git location: https://github.com/input-output-hk/cardano-ledger-executable-spec.git - tag: 9233cb9f0e15dcdb5ef7ba49a21ee3820ee9aa76 - --sha256: sha256-ea99nQ/j62FJkVdACKffVgLZ5mR1ZKwakSlNcSi5fJA= + tag: 1ffb1d13b8892c0943780cd7bd9e2724b5c20cab + --sha256: sha256-iiC0AwhPce6XnaGYHyQBeMSIttvn2c+Legu0tUgYOEM= index-state: -- Bump this if you need newer packages from Hackage diff --git a/eras/conway/impl/src/Cardano/Ledger/Conway/Rules/Gov.hs b/eras/conway/impl/src/Cardano/Ledger/Conway/Rules/Gov.hs index 50914328c0a..867306103e8 100644 --- a/eras/conway/impl/src/Cardano/Ledger/Conway/Rules/Gov.hs +++ b/eras/conway/impl/src/Cardano/Ledger/Conway/Rules/Gov.hs @@ -71,10 +71,12 @@ import Cardano.Ledger.Conway.Governance ( isCommitteeVotingAllowed, isDRepVotingAllowed, isStakePoolVotingAllowed, + pRootsL, proposalsActionsMap, proposalsAddAction, proposalsAddVote, proposalsLookupId, + toPrevGovActionIds, ) import Cardano.Ledger.Conway.Governance.Procedures (GovAction (..), foldrVotingProcedures) import Cardano.Ledger.Conway.PParams ( @@ -112,6 +114,7 @@ import qualified Data.Sequence.Strict as SSeq import qualified Data.Set as Set import GHC.Generics (Generic) import Lens.Micro +import qualified Lens.Micro as L import NoThunks.Class (NoThunks (..)) import Validation (failureUnless) @@ -121,7 +124,6 @@ data GovEnv era = GovEnv { geTxId :: !(TxId (EraCrypto era)) , geEpoch :: !EpochNo , gePParams :: !(PParams era) - , gePrevGovActionIds :: !(GovRelation StrictMaybe era) , gePPolicy :: !(StrictMaybe (ScriptHash (EraCrypto era))) , geCommitteeState :: !(CommitteeState era) } @@ -330,11 +332,12 @@ govTransition :: TransitionRule (EraRule "GOV" era) govTransition = do TRC - ( GovEnv txid currentEpoch pp prevGovActionIds constitutionPolicy committeeState + ( GovEnv txid currentEpoch pp constitutionPolicy committeeState , st , gp ) <- judgmentContext + let prevGovActionIds = st ^. pRootsL . L.to toPrevGovActionIds expectedNetworkId <- liftSTS $ asks networkId diff --git a/eras/conway/impl/src/Cardano/Ledger/Conway/Rules/Ledger.hs b/eras/conway/impl/src/Cardano/Ledger/Conway/Rules/Ledger.hs index 63f9678576d..ceba9a636dc 100644 --- a/eras/conway/impl/src/Cardano/Ledger/Conway/Rules/Ledger.hs +++ b/eras/conway/impl/src/Cardano/Ledger/Conway/Rules/Ledger.hs @@ -50,9 +50,7 @@ import Cardano.Ledger.Conway.Governance ( GovProcedures (..), Proposals, constitutionScriptL, - pRootsL, proposalsGovStateL, - toPrevGovActionIds, ) import Cardano.Ledger.Conway.Rules.Cert (CertEnv, ConwayCertPredFailure) import Cardano.Ledger.Conway.Rules.Certs ( @@ -383,7 +381,6 @@ ledgerTransition = do (txIdTxBody txBody) currentEpoch pp - (utxoState ^. utxosGovStateL . proposalsGovStateL . pRootsL . L.to toPrevGovActionIds) (utxoState ^. utxosGovStateL . constitutionGovStateL . constitutionScriptL) (certState ^. certVStateL . vsCommitteeStateL) , utxoState ^. utxosGovStateL . proposalsGovStateL diff --git a/eras/conway/impl/testlib/Test/Cardano/Ledger/Conway/Arbitrary.hs b/eras/conway/impl/testlib/Test/Cardano/Ledger/Conway/Arbitrary.hs index 7e03a5d827c..a49f81c9dda 100644 --- a/eras/conway/impl/testlib/Test/Cardano/Ledger/Conway/Arbitrary.hs +++ b/eras/conway/impl/testlib/Test/Cardano/Ledger/Conway/Arbitrary.hs @@ -562,7 +562,6 @@ instance (Era era, Arbitrary (PParamsHKD Identity era)) => Arbitrary (GovEnv era <*> arbitrary <*> arbitrary <*> arbitrary - <*> arbitrary instance Era era => Arbitrary (VotingProcedure era) where arbitrary = VotingProcedure <$> arbitrary <*> arbitrary 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 98eba78d8d1..ae1d9922c3a 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 @@ -6,7 +6,9 @@ module Test.Cardano.Ledger.Conformance.Orphans () where import GHC.Generics (Generic) import Lib +import Numeric (showHex) import Test.Cardano.Ledger.Common (NFData, ToExpr) +import Test.Cardano.Ledger.Conway.TreeDiff (Expr (..), ToExpr (..)) deriving instance Generic GovActionState @@ -62,6 +64,8 @@ deriving instance Eq UTxOEnv instance NFData GovAction +instance NFData TxId + instance NFData UTxOState instance NFData Vote @@ -100,10 +104,19 @@ instance NFData Tx instance NFData UTxOEnv +instance ToExpr Credential where + toExpr (KeyHashObj h) = App "KeyHashObj" [toExpr $ showHex h ""] + toExpr (ScriptObj h) = App "ScriptObj" [toExpr $ showHex h ""] + instance ToExpr GovAction +instance ToExpr GovRole + instance ToExpr Vote +instance ToExpr TxId where + toExpr (MkTxId x) = App "TxId" [toExpr $ showHex x ""] + instance ToExpr GovActionState instance ToExpr GovProposal @@ -112,6 +125,26 @@ instance ToExpr GovVote instance ToExpr GovSignal +instance ToExpr PParams + instance ToExpr GovEnv instance ToExpr EnactState + +instance ToExpr VDeleg + +instance ToExpr TxCert + +instance ToExpr TxBody + +instance ToExpr AgdaEmpty + +instance ToExpr Tag + +instance ToExpr TxWitnesses + +instance ToExpr Tx + +instance ToExpr UTxOState + +instance ToExpr UTxOEnv 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 fe5ef6efec6..fe2752a3c35 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 @@ -61,7 +61,7 @@ import Cardano.Ledger.Conway.Governance ( GovActionIx (..), GovActionState (..), GovProcedures (..), - GovPurposeId (GovPurposeId), + GovPurposeId (..), GovRelation (..), ProposalProcedure (..), Proposals, @@ -69,6 +69,7 @@ import Cardano.Ledger.Conway.Governance ( Voter (..), VotingProcedure (..), VotingProcedures (..), + ensProtVerL, foldrVotingProcedures, gasAction, gasReturnAddr, @@ -613,7 +614,10 @@ instance SpecTranslate ctx (ConwayTxCert era) where <$> toSpecRep c <*> toSpecRep (SNothing @(Credential _ _)) -deriving instance SpecTranslate ctx (TxId era) +instance SpecTranslate ctx (TxId era) where + type SpecRep (TxId era) = Agda.TxId + + toSpecRep (TxId x) = Agda.MkTxId <$> toSpecRep x toAgdaTxBody :: ( SpecRep (TxOut era) ~ Agda.TxOut @@ -731,7 +735,7 @@ instance committee <- toSpecRep x agdaLastId <- case h of SJust lastId -> toSpecRep lastId - SNothing -> pure (0, 0) + SNothing -> pure (Agda.MkTxId 0, 0) pure (committee, agdaLastId) instance @@ -747,12 +751,19 @@ instance toSpecRep GovEnv {..} = do enactState <- askTransCtx @(GovEnv era) + let + protVer = gePParams ^. ppProtocolVersionL + -- TODO express this in agdaConstraints rather than doing it during + -- translation + enactStatePV = + enactState + & ensProtVerL .~ protVer Agda.MkGovEnv <$> toSpecRep geTxId <*> toSpecRep geEpoch <*> toSpecRep gePParams <*> toSpecRep gePPolicy - <*> toSpecRep enactState + <*> toSpecRep enactStatePV instance SpecTranslate ctx (Voter era) where type SpecRep (Voter era) = Agda.Voter @@ -883,15 +894,23 @@ instance instance EraPParams era => SpecTranslate ctx (GovActionState era) where type SpecRep (GovActionState era) = Agda.GovActionState - toSpecRep gas@GovActionState {..} = + toSpecRep gas@GovActionState {..} = do Agda.MkGovActionState <$> agdaVoteMap <*> toSpecRep (gasReturnAddr gas) <*> toSpecRep gasExpiresAfter <*> toSpecRep action - <*> toSpecRep (nullifyIfNotNeeded gasId action) + <*> toSpecRep (nullifyIfNotNeeded prevGovActionId action) where action = gasAction gas + prevGovActionId = + case action of + ParameterChange x _ _ -> unGovPurposeId <$> x + HardForkInitiation x _ -> unGovPurposeId <$> x + UpdateCommittee x _ _ _ -> unGovPurposeId <$> x + NoConfidence x -> unGovPurposeId <$> x + NewConstitution x _ -> unGovPurposeId <$> x + _ -> SNothing agdaVoteMap = do drepVotes <- toSpecRep gasDRepVotes ccVotes <- toSpecRep gasCommitteeVotes @@ -903,7 +922,8 @@ instance EraPParams era => SpecTranslate ctx (GovActionState era) where , first (\h -> (Agda.SPO, Agda.KeyHashObj h)) <$> spoVotes ] nullGovActionId = GovActionId (TxId def) (GovActionIx 0) - nullifyIfNotNeeded gaId = \case + nullifyIfNotNeeded SNothing = const nullGovActionId + nullifyIfNotNeeded (SJust gaId) = \case TreasuryWithdrawals {} -> nullGovActionId InfoAction -> nullGovActionId _ -> gaId diff --git a/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/Gov.hs b/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/Gov.hs index 9181e2fd34d..d5835ef435d 100644 --- a/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/Gov.hs +++ b/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/Gov.hs @@ -26,6 +26,7 @@ import Constrained import Cardano.Ledger.Conway (ConwayEra) import Cardano.Ledger.Conway.Core import Cardano.Ledger.Crypto (StandardCrypto) +import Lens.Micro qualified as L import Test.Cardano.Ledger.Constrained.Conway.Instances import Test.Cardano.Ledger.Constrained.Conway.PParams @@ -33,7 +34,7 @@ govEnvSpec :: IsConwayUniv fn => Specification fn (GovEnv (ConwayEra StandardCrypto)) govEnvSpec = constrained $ \ge -> - match ge $ \_ _ pp _ _ _ -> + match ge $ \_ _ pp _ _ -> satisfies pp pparamsSpec -- NOTE: it is probably OK not to check uniqueness of ids here, because a clash @@ -43,11 +44,11 @@ govProposalsSpec :: IsConwayUniv fn => GovEnv (ConwayEra StandardCrypto) -> Specification fn (Proposals (ConwayEra StandardCrypto)) -govProposalsSpec GovEnv {geEpoch, gePPolicy, gePrevGovActionIds} = +govProposalsSpec GovEnv {geEpoch, gePPolicy} = constrained $ \props -> match props $ \ppupTree hardForkTree committeeTree constitutionTree unorderedProposals -> [ -- Protocol parameter updates - wellFormedChildren (lit $ coerce grPParamUpdate) ppupTree + wellFormedChildren ppupTree , allGASInTree ppupTree $ \gas -> [ isCon @"ParameterChange" (pProcGovAction_ . gasProposalProcedure_ $ gas) , onCon @"ParameterChange" (pProcGovAction_ . gasProposalProcedure_ $ gas) $ @@ -59,7 +60,7 @@ govProposalsSpec GovEnv {geEpoch, gePPolicy, gePrevGovActionIds} = , forAll (snd_ ppupTree) (genHint treeGenHint) , genHint listSizeHint (snd_ ppupTree) , -- Hard forks - wellFormedChildren (lit $ coerce grHardFork) hardForkTree + wellFormedChildren hardForkTree , allGASInTree hardForkTree $ \gas -> isCon @"HardForkInitiation" (pProcGovAction_ . gasProposalProcedure_ $ gas) , allGASAndChildInTree hardForkTree $ \gas gas' -> @@ -82,7 +83,7 @@ govProposalsSpec GovEnv {geEpoch, gePPolicy, gePrevGovActionIds} = , forAll (snd_ hardForkTree) (genHint treeGenHint) , genHint listSizeHint (snd_ hardForkTree) , -- Committee - wellFormedChildren (lit $ coerce grCommittee) committeeTree + wellFormedChildren committeeTree , -- TODO: it would be nice to have a trick like `isCon` that can -- do disjunction without having to write down all the cases. allGASInTree committeeTree $ \gas -> @@ -102,7 +103,7 @@ govProposalsSpec GovEnv {geEpoch, gePPolicy, gePrevGovActionIds} = , forAll (snd_ committeeTree) (genHint treeGenHint) , genHint listSizeHint (snd_ committeeTree) , -- Constitution - wellFormedChildren (lit $ coerce grConstitution) constitutionTree + wellFormedChildren constitutionTree , allGASInTree constitutionTree $ \gas -> isCon @"NewConstitution" (pProcGovAction_ . gasProposalProcedure_ $ gas) , forAll (snd_ constitutionTree) (genHint treeGenHint) @@ -128,7 +129,6 @@ govProposalsSpec GovEnv {geEpoch, gePPolicy, gePrevGovActionIds} = , genHint listSizeHint unorderedProposals ] where - GovRelation {..} = gePrevGovActionIds treeGenHint = (Just 2, 10) listSizeHint = 5 @@ -158,15 +158,13 @@ allGASAndChildInTree t k = wellFormedChildren :: IsConwayUniv fn => - Term fn (StrictMaybe (GovActionId StandardCrypto)) -> Term fn ProposalTree -> Pred fn -wellFormedChildren root rootAndTrees = +wellFormedChildren rootAndTrees = match rootAndTrees $ \root' trees -> - [ assert $ root ==. root' -- The root matches the root given in the environment - , forAll trees $ \t -> + [ forAll trees $ \t -> [ -- Every node just below the root has the root as its parent - withPrevActId (rootLabel_ t) (assert . (==. root)) + withPrevActId (rootLabel_ t) (assert . (==. root')) , -- Every node's children have the id of the node as its parent forAll' t $ \gas children -> [ forAll children $ \t' -> @@ -289,7 +287,7 @@ wfGovAction :: Proposals (ConwayEra StandardCrypto) -> Term fn (GovAction (ConwayEra StandardCrypto)) -> Pred fn -wfGovAction GovEnv {gePPolicy, geEpoch, gePrevGovActionIds, gePParams} ps govAction = +wfGovAction GovEnv {gePPolicy, geEpoch, gePParams} ps govAction = caseOn govAction -- ParameterChange @@ -344,26 +342,27 @@ wfGovAction GovEnv {gePPolicy, geEpoch, gePrevGovActionIds, gePParams} ps govAct -- InfoAction (branch $ \_ -> True) where + prevGovActionIds = ps ^. pRootsL . L.to toPrevGovActionIds constitutionIds = - (gePrevGovActionIds ^. grConstitutionL) + (prevGovActionIds ^. grConstitutionL) : [ SJust $ coerce $ gasId gas | gas <- actions , NewConstitution {} <- [pProcGovAction $ gasProposalProcedure gas] ] committeeIds = - (gePrevGovActionIds ^. grCommitteeL) + (prevGovActionIds ^. grCommitteeL) : [ SJust $ coerce $ gasId gas | gas <- actions , isCommitteeAction (pProcGovAction $ gasProposalProcedure gas) ] ppupIds = - (gePrevGovActionIds ^. grPParamUpdateL) + (prevGovActionIds ^. grPParamUpdateL) : [ SJust $ coerce $ gasId gas | gas <- actions , ParameterChange {} <- [pProcGovAction $ gasProposalProcedure gas] ] hardForkIds = - (gePrevGovActionIds ^. grHardForkL) + (prevGovActionIds ^. grHardForkL) : [ SJust $ coerce $ gasId gas | gas <- actions , HardForkInitiation {} <- [pProcGovAction $ gasProposalProcedure gas] diff --git a/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Generic/PrettyCore.hs b/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Generic/PrettyCore.hs index 02f73c1f6fe..cc722453cef 100644 --- a/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Generic/PrettyCore.hs +++ b/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Generic/PrettyCore.hs @@ -3350,7 +3350,6 @@ pcGovEnv GovEnv {..} = [ ("TxId", pcTxId geTxId) , ("Epoch", ppEpochNo geEpoch) , ("PParams", pcPParams reify gePParams) - , ("PrevGovActionId", pcPrevGovActionIds gePrevGovActionIds) ] instance Reflect era => PrettyA (GovEnv era) where