From c53879c2292e3fc62be6c0e90ee460416e72cd10 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Joosep=20J=C3=A4=C3=A4ger?= Date: Fri, 4 Oct 2024 16:35:44 +0300 Subject: [PATCH] Reorganize UTXO conformance tests Added LEDGER conformance test --- cabal.project | 4 +- .../Ledger/Conway/Governance/Proposals.hs | 12 +- eras/shelley/impl/CHANGELOG.md | 9 +- .../shelley/impl/cardano-ledger-shelley.cabal | 2 +- .../src/Cardano/Ledger/Shelley/AdaPots.hs | 3 +- .../Cardano/Ledger/Shelley/Rules/Ledger.hs | 13 ++ .../Test/Cardano/Ledger/Shelley/ImpTest.hs | 34 +++- .../Test/Cardano/Ledger/Shelley/TreeDiff.hs | 2 + .../cardano-ledger-conformance.cabal | 6 + .../Ledger/Conformance/ExecSpecRule/Conway.hs | 3 + .../Conformance/ExecSpecRule/Conway/Base.hs | 111 +---------- .../Conformance/ExecSpecRule/Conway/Ledger.hs | 186 ++++++++++++++++++ .../Conformance/ExecSpecRule/Conway/Utxo.hs | 112 +++++++++++ .../Conformance/ExecSpecRule/Conway/Utxow.hs | 52 +++++ .../Cardano/Ledger/Conformance/Orphans.hs | 4 + .../Conformance/SpecTranslate/Conway.hs | 2 + .../Conformance/SpecTranslate/Conway/Base.hs | 51 +---- .../Conformance/SpecTranslate/Conway/Cert.hs | 30 ++- .../SpecTranslate/Conway/Ledger.hs | 58 ++++++ .../Conformance/SpecTranslate/Conway/Utxo.hs | 49 +++++ .../Conformance/SpecTranslate/Conway/Utxow.hs | 29 +++ .../Cardano/Ledger/Conformance/Spec/Conway.hs | 2 + .../Cardano/Ledger/Constrained/Conway/Utxo.hs | 3 + .../Test/Cardano/Ledger/Generic/GenState.hs | 6 + .../src/Test/Cardano/Ledger/Generic/TxGen.hs | 9 +- 25 files changed, 619 insertions(+), 173 deletions(-) create mode 100644 libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/ExecSpecRule/Conway/Ledger.hs create mode 100644 libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/ExecSpecRule/Conway/Utxo.hs create mode 100644 libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/ExecSpecRule/Conway/Utxow.hs create mode 100644 libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/SpecTranslate/Conway/Ledger.hs create mode 100644 libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/SpecTranslate/Conway/Utxo.hs create mode 100644 libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/SpecTranslate/Conway/Utxow.hs diff --git a/cabal.project b/cabal.project index 40592ffb43a..bf1afab04af 100644 --- a/cabal.project +++ b/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: 544ab20985e3374a1d672354e25d8ca0ca89e7e4 - --sha256: sha256-bhh09OZkHazXCPjsiU/50Hrmfg52i+6UORTZ6/bAx6c= + tag: 50a653f7a74791833268b648500c3677a84e7ea1 + --sha256: sha256-jkFo6nIMXLbNcrqSfbhdoemnmGZMVZOt3YQ5Mag8YlM= -- 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 diff --git a/eras/conway/impl/src/Cardano/Ledger/Conway/Governance/Proposals.hs b/eras/conway/impl/src/Cardano/Ledger/Conway/Governance/Proposals.hs index ca0ca1562a2..0511dc468a6 100644 --- a/eras/conway/impl/src/Cardano/Ledger/Conway/Governance/Proposals.hs +++ b/eras/conway/impl/src/Cardano/Ledger/Conway/Governance/Proposals.hs @@ -332,7 +332,7 @@ mkProposals pgais omap = do -- -- WARNING: Should only be used for testing! unsafeMkProposals :: - HasCallStack => + (HasCallStack, EraPParams era) => GovRelation StrictMaybe era -> OMap.OMap (GovActionId (EraCrypto era)) (GovActionState era) -> Proposals era @@ -342,7 +342,15 @@ unsafeMkProposals pgais omap = F.foldl' unsafeProposalsAddAction initialProposal unsafeProposalsAddAction ps gas = case runProposalsAddAction gas ps of Just p -> p - Nothing -> error $ "unsafeMkProposals: runProposalsAddAction failed for " ++ show (gas ^. gasIdL) + Nothing -> + error $ + unlines + [ "unsafeMkProposals: runProposalsAddAction failed for " ++ show (gas ^. gasIdL) + , "Proposals:" + , show ps + , "GovActionState:" + , show gas + ] instance EraPParams era => EncCBOR (Proposals era) where encCBOR ps = diff --git a/eras/shelley/impl/CHANGELOG.md b/eras/shelley/impl/CHANGELOG.md index e8559f8af3b..27e47264f22 100644 --- a/eras/shelley/impl/CHANGELOG.md +++ b/eras/shelley/impl/CHANGELOG.md @@ -1,8 +1,13 @@ # Version history for `cardano-ledger-shelley` -## 1.14.1.1 +## 1.14.2.0 -* +* Added `EncCBOR` instance for `LedgerEnv` + +### `testlib` + +* Added `ToExpr` instance for `LedgerEnv` +* Added `tryRunImpRuleNoAssertions` to `ImpTest` ## 1.14.1.0 diff --git a/eras/shelley/impl/cardano-ledger-shelley.cabal b/eras/shelley/impl/cardano-ledger-shelley.cabal index 9f01110e995..6e72da01320 100644 --- a/eras/shelley/impl/cardano-ledger-shelley.cabal +++ b/eras/shelley/impl/cardano-ledger-shelley.cabal @@ -1,6 +1,6 @@ cabal-version: 3.0 name: cardano-ledger-shelley -version: 1.14.1.0 +version: 1.14.2.0 license: Apache-2.0 maintainer: operations@iohk.io author: IOHK diff --git a/eras/shelley/impl/src/Cardano/Ledger/Shelley/AdaPots.hs b/eras/shelley/impl/src/Cardano/Ledger/Shelley/AdaPots.hs index a31e629d7a9..c80718b2291 100644 --- a/eras/shelley/impl/src/Cardano/Ledger/Shelley/AdaPots.hs +++ b/eras/shelley/impl/src/Cardano/Ledger/Shelley/AdaPots.hs @@ -153,7 +153,8 @@ consumedTxBody :: Consumed consumedTxBody txBody pp dpstate utxo = Consumed - { conInputs = coinBalance (txInsFilter utxo (txBody ^. inputsTxBodyL)) + { conInputs = + coinBalance (txInsFilter utxo (txBody ^. inputsTxBodyL)) , conRefunds = certsTotalRefundsTxBody pp dpstate txBody , conWithdrawals = fold . unWithdrawals $ txBody ^. withdrawalsTxBodyL } diff --git a/eras/shelley/impl/src/Cardano/Ledger/Shelley/Rules/Ledger.hs b/eras/shelley/impl/src/Cardano/Ledger/Shelley/Rules/Ledger.hs index 480aa58d075..9257917f14b 100644 --- a/eras/shelley/impl/src/Cardano/Ledger/Shelley/Rules/Ledger.hs +++ b/eras/shelley/impl/src/Cardano/Ledger/Shelley/Rules/Ledger.hs @@ -7,6 +7,7 @@ {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE NamedFieldPuns #-} {-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE RecordWildCards #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE StandaloneDeriving #-} {-# LANGUAGE TypeApplications #-} @@ -35,6 +36,7 @@ import Cardano.Ledger.Binary ( decodeRecordSum, encodeListLen, ) +import Cardano.Ledger.Binary.Coders (Encode (..), encode, (!>)) import Cardano.Ledger.Keys (DSignable, Hash) import Cardano.Ledger.Shelley.AdaPots (consumedTxBody, producedTxBody) import Cardano.Ledger.Shelley.Core @@ -98,6 +100,17 @@ deriving instance Eq (PParams era) => Eq (LedgerEnv era) instance NFData (PParams era) => NFData (LedgerEnv era) where rnf (LedgerEnv _slotNo _ix pp _account _mempool) = rnf pp +instance EraPParams era => EncCBOR (LedgerEnv era) where + encCBOR env@(LedgerEnv _ _ _ _ _) = + let LedgerEnv {..} = env + in encode $ + Rec LedgerEnv + !> To ledgerSlotNo + !> To ledgerIx + !> To ledgerPp + !> To ledgerAccount + !> To ledgerMempool + data ShelleyLedgerPredFailure era = UtxowFailure (PredicateFailure (EraRule "UTXOW" era)) -- Subtransition Failures | DelegsFailure (PredicateFailure (EraRule "DELEGS" era)) -- Subtransition Failures diff --git a/eras/shelley/impl/testlib/Test/Cardano/Ledger/Shelley/ImpTest.hs b/eras/shelley/impl/testlib/Test/Cardano/Ledger/Shelley/ImpTest.hs index a84a9f6a1b3..1ce4dc71441 100644 --- a/eras/shelley/impl/testlib/Test/Cardano/Ledger/Shelley/ImpTest.hs +++ b/eras/shelley/impl/testlib/Test/Cardano/Ledger/Shelley/ImpTest.hs @@ -73,6 +73,7 @@ module Test.Cardano.Ledger.Shelley.ImpTest ( impLogToExpr, runImpRule, tryRunImpRule, + tryRunImpRuleNoAssertions, delegateStake, registerRewardAccount, registerStakeCredential, @@ -1295,14 +1296,43 @@ tryRunImpRule :: (NonEmpty (PredicateFailure (EraRule rule era))) (State (EraRule rule era), [Event (EraRule rule era)]) ) -tryRunImpRule stsEnv stsState stsSignal = do +tryRunImpRule = tryRunImpRule' @rule AssertionsAll + +tryRunImpRuleNoAssertions :: + forall rule era. + (STS (EraRule rule era), BaseM (EraRule rule era) ~ ShelleyBase) => + Environment (EraRule rule era) -> + State (EraRule rule era) -> + Signal (EraRule rule era) -> + ImpTestM + era + ( Either + (NonEmpty (PredicateFailure (EraRule rule era))) + (State (EraRule rule era), [Event (EraRule rule era)]) + ) +tryRunImpRuleNoAssertions = tryRunImpRule' @rule AssertionsOff + +tryRunImpRule' :: + forall rule era. + (STS (EraRule rule era), BaseM (EraRule rule era) ~ ShelleyBase) => + AssertionPolicy -> + Environment (EraRule rule era) -> + State (EraRule rule era) -> + Signal (EraRule rule era) -> + ImpTestM + era + ( Either + (NonEmpty (PredicateFailure (EraRule rule era))) + (State (EraRule rule era), [Event (EraRule rule era)]) + ) +tryRunImpRule' assertionPolicy stsEnv stsState stsSignal = do let trc = TRC (stsEnv, stsState, stsSignal) let stsOpts = ApplySTSOpts { asoValidation = ValidateAll , asoEvents = EPReturn - , asoAssertions = AssertionsAll + , asoAssertions = assertionPolicy } runShelleyBase (applySTSOptsEither @(EraRule rule era) stsOpts trc) diff --git a/eras/shelley/impl/testlib/Test/Cardano/Ledger/Shelley/TreeDiff.hs b/eras/shelley/impl/testlib/Test/Cardano/Ledger/Shelley/TreeDiff.hs index 8db9f950f40..98cc7db04bc 100644 --- a/eras/shelley/impl/testlib/Test/Cardano/Ledger/Shelley/TreeDiff.hs +++ b/eras/shelley/impl/testlib/Test/Cardano/Ledger/Shelley/TreeDiff.hs @@ -269,3 +269,5 @@ instance ToExpr (ShelleyMirEvent era) instance ToExpr (RupdEvent era) instance ToExpr (PParamsHKD Identity era) => ToExpr (UtxoEnv era) + +instance ToExpr (PParamsHKD Identity era) => ToExpr (LedgerEnv era) diff --git a/libs/cardano-ledger-conformance/cardano-ledger-conformance.cabal b/libs/cardano-ledger-conformance/cardano-ledger-conformance.cabal index 771953e5170..acbfcb36de5 100644 --- a/libs/cardano-ledger-conformance/cardano-ledger-conformance.cabal +++ b/libs/cardano-ledger-conformance/cardano-ledger-conformance.cabal @@ -36,12 +36,18 @@ library Test.Cardano.Ledger.Conformance.SpecTranslate.Conway.Certs Test.Cardano.Ledger.Conformance.SpecTranslate.Conway.Gov Test.Cardano.Ledger.Conformance.SpecTranslate.Conway.GovCert + Test.Cardano.Ledger.Conformance.SpecTranslate.Conway.Utxo + Test.Cardano.Ledger.Conformance.SpecTranslate.Conway.Utxow + Test.Cardano.Ledger.Conformance.SpecTranslate.Conway.Ledger Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Deleg Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Pool Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Cert Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Certs Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Gov Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.GovCert + Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Utxo + Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Utxow + Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Ledger Test.Cardano.Ledger.Conformance.Orphans Test.Cardano.Ledger.Conformance.Utils diff --git a/libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/ExecSpecRule/Conway.hs b/libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/ExecSpecRule/Conway.hs index 3c5ce111848..1548e9b14e5 100644 --- a/libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/ExecSpecRule/Conway.hs +++ b/libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/ExecSpecRule/Conway.hs @@ -16,4 +16,7 @@ import Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Certs as X (nameCerts import Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Deleg as X (nameDelegCert) import Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Gov as X () import Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.GovCert as X (nameGovCert) +import Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Ledger as X () import Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Pool as X (namePoolCert) +import Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Utxo as X () +import Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Utxow as X () diff --git a/libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/ExecSpecRule/Conway/Base.hs b/libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/ExecSpecRule/Conway/Base.hs index 03f716c3ca9..adfba2e346b 100644 --- a/libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/ExecSpecRule/Conway/Base.hs +++ b/libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/ExecSpecRule/Conway/Base.hs @@ -4,7 +4,6 @@ {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE GADTs #-} -{-# LANGUAGE InstanceSigs #-} {-# LANGUAGE LambdaCase #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE NamedFieldPuns #-} @@ -28,13 +27,13 @@ module Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Base ( nameGovAction, crecTreasuryL, crecGovActionMapL, + enactStateSpec, ) where import Cardano.Ledger.BaseTypes ( EpochInterval (..), EpochNo (..), Inject (..), - ProtVer (..), StrictMaybe (..), addEpochInterval, natVersion, @@ -47,7 +46,7 @@ import Cardano.Ledger.CertState ( ) import Cardano.Ledger.Coin (Coin (..), CompactForm (..)) import Cardano.Ledger.Conway (Conway) -import Cardano.Ledger.Conway.Core (Era (..), EraPParams (..), PParams, ppMaxTxSizeL, sizeTxF) +import Cardano.Ledger.Conway.Core (Era (..), EraPParams (..), PParams) import Cardano.Ledger.Conway.Governance ( Committee (..), EnactState (..), @@ -78,26 +77,21 @@ import Cardano.Ledger.PoolDistr (IndividualPoolStake (..)) import Constrained hiding (inject) import Data.Bifunctor (Bifunctor (..)) import Data.Foldable (Foldable (..)) -import qualified Data.List.NonEmpty as NE import Data.Map.Strict (Map) import qualified Data.Map.Strict as Map import Data.Ratio (denominator, numerator, (%)) import qualified Data.Sequence.Strict as SSeq import qualified Data.Set as Set -import qualified Data.Text as T import GHC.Generics (Generic) -import Lens.Micro (Lens', lens, (&), (.~), (^.)) +import Lens.Micro (Lens', lens, (^.)) import qualified Lib as Agda import qualified Prettyprinter as PP import Test.Cardano.Ledger.Binary.TreeDiff (tableDoc) import Test.Cardano.Ledger.Common (Arbitrary (..)) import Test.Cardano.Ledger.Conformance ( ExecSpecRule (..), - OpaqueErrorString (..), SpecTranslate (..), - checkConformance, computationResultToEither, - runConformance, runSpecTransM, ) import Test.Cardano.Ledger.Conformance.ExecSpecRule.Core (defaultTestConformance) @@ -107,18 +101,13 @@ import Test.Cardano.Ledger.Conformance.SpecTranslate.Conway.Base ( DepositPurpose, ) import Test.Cardano.Ledger.Constrained.Conway ( - ConwayFn, EpochExecEnv, IsConwayUniv, - UtxoExecContext (..), coerce_, epochEnvSpec, epochSignalSpec, epochStateSpec, newEpochStateSpec, - utxoEnvSpec, - utxoStateSpec, - utxoTxSpec, ) import Test.Cardano.Ledger.Constrained.Conway.SimplePParams ( committeeMaxTermLength_, @@ -127,93 +116,9 @@ import Test.Cardano.Ledger.Constrained.Conway.SimplePParams ( ) import Cardano.Ledger.Address (RewardAccount) -import Cardano.Ledger.Shelley.LedgerState (UTxOState (..)) -import Cardano.Ledger.Shelley.Rules (UtxoEnv (..)) import Test.Cardano.Ledger.Conway.Arbitrary () -import Test.Cardano.Ledger.Conway.ImpTest (logDoc, showConwayTxBalance) -import Test.Cardano.Ledger.Generic.GenState ( - GenEnv (..), - GenState (..), - invalidScriptFreq, - runGenRS, - ) -import qualified Test.Cardano.Ledger.Generic.GenState as GenSize -import qualified Test.Cardano.Ledger.Generic.PrettyCore as PP -import qualified Test.Cardano.Ledger.Generic.Proof as Proof -import Test.Cardano.Ledger.Generic.TxGen (genAlonzoTx) import Test.Cardano.Ledger.Imp.Common hiding (arbitrary, forAll, prop, var) -instance - forall fn. - IsConwayUniv fn => - ExecSpecRule fn "UTXO" Conway - where - type ExecContext fn "UTXO" Conway = UtxoExecContext Conway - - genExecContext = do - let proof = Proof.reify @Conway - ueSlot <- arbitrary - let - genSize = - GenSize.small - { invalidScriptFreq = 0 -- TODO make the test work with invalid scripts - } - ((uecUTxO, uecTx), gs) <- - runGenRS proof genSize $ - genAlonzoTx proof ueSlot - ueCertState <- arbitrary - let txSize = uecTx ^. sizeTxF - let - uePParams = - gePParams (gsGenEnv gs) - & ppMaxTxSizeL .~ fromIntegral txSize - & ppProtocolVersionL .~ ProtVer (natVersion @10) 0 - uecUtxoEnv = UtxoEnv {..} - pure UtxoExecContext {..} - - environmentSpec = utxoEnvSpec - - stateSpec = utxoStateSpec - - signalSpec ctx _ _ = utxoTxSpec ctx - - runAgdaRule env st sig = - first (\e -> OpaqueErrorString (T.unpack e) NE.:| []) - . computationResultToEither - $ Agda.utxoStep 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 - <$> toSpecRep env - <*> toSpecRep st - <*> toSpecRep sig - ) - - testConformance ctx env st sig = property $ do - (implResTest, agdaResTest) <- runConformance @"UTXO" @ConwayFn @Conway ctx env st sig - let extra = extraInfo @ConwayFn @"UTXO" @Conway ctx (inject env) (inject st) (inject sig) - logDoc extra - let - -- TODO make the deposit map updates match up exactly between the spec and - -- the implmentation - eraseDeposits Agda.MkUTxOState {..} = - Agda.MkUTxOState {deposits = Agda.MkHSMap mempty, ..} - checkConformance - @"UTXO" - @Conway - @ConwayFn - ctx - (inject env) - (inject st) - (inject sig) - (second eraseDeposits implResTest) - (second eraseDeposits agdaResTest) - data ConwayCertExecContext era = ConwayCertExecContext { ccecWithdrawals :: !(Map (RewardAccount (EraCrypto era)) Coin) , ccecDeposits :: !(Map (DepositPurpose (EraCrypto era)) Coin) @@ -663,10 +568,7 @@ nameGovAction UpdateCommittee {} = "UpdateCommittee" nameGovAction NewConstitution {} = "NewConstitution" nameGovAction InfoAction {} = "InfoAction" -instance - IsConwayUniv fn => - ExecSpecRule fn "EPOCH" Conway - where +instance IsConwayUniv fn => ExecSpecRule fn "EPOCH" Conway where type ExecContext fn "EPOCH" Conway = [GovActionState Conway] type ExecEnvironment fn "EPOCH" Conway = EpochExecEnv Conway @@ -686,10 +588,7 @@ instance nameEpoch :: EpochNo -> String nameEpoch x = show x -instance - IsConwayUniv fn => - ExecSpecRule fn "NEWEPOCH" Conway - where +instance IsConwayUniv fn => ExecSpecRule fn "NEWEPOCH" Conway where type ExecContext fn "NEWEPOCH" Conway = [GovActionState Conway] type ExecEnvironment fn "NEWEPOCH" Conway = EpochExecEnv Conway diff --git a/libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/ExecSpecRule/Conway/Ledger.hs b/libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/ExecSpecRule/Conway/Ledger.hs new file mode 100644 index 00000000000..ab4c218b4b6 --- /dev/null +++ b/libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/ExecSpecRule/Conway/Ledger.hs @@ -0,0 +1,186 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE DeriveGeneric #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE RecordWildCards #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE UndecidableInstances #-} +{-# OPTIONS_GHC -Wno-orphans #-} + +module Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Ledger () where + +import Data.Bifunctor (Bifunctor (..)) +import Data.Functor.Identity (Identity) +import qualified Data.List.NonEmpty as NE + +import Cardano.Ledger.BaseTypes (Inject (..), StrictMaybe) +import Cardano.Ledger.Conway.Core ( + Era (..), + EraPParams (..), + EraTx, + EraTxAuxData (..), + EraTxBody (..), + EraTxOut (..), + EraTxWits (..), + ScriptHash, + ) +import Cardano.Ledger.Conway.Rules (EnactState) + +import Test.Cardano.Ledger.Conformance ( + ExecSpecRule (..), + FixupSpecRep (..), + OpaqueErrorString (..), + checkConformance, + computationResultToEither, + runSpecTransM, + toTestRep, + ) +import Test.Cardano.Ledger.Conformance.SpecTranslate.Conway () +import Test.Cardano.Ledger.Constrained.Conway (IsConwayUniv, UtxoExecContext (..), utxoStateSpec) +import Test.Cardano.Ledger.Conway.Arbitrary () + +import Cardano.Ledger.Conway (Conway) +import Constrained ( + Specification (..), + assert, + constrained, + constrained', + genFromSpec, + lit, + satisfies, + (==.), + ) + +import Cardano.Ledger.Binary (EncCBOR (..)) +import Cardano.Ledger.Binary.Coders (Encode (..), encode, (!>)) +import Cardano.Ledger.Shelley.Rules (UtxoEnv (..)) +import Data.Bitraversable (bimapM) +import qualified Data.Text as T +import GHC.Generics (Generic) +import qualified Lib as Agda +import Test.Cardano.Ledger.Common (Arbitrary (..), NFData, Testable (..), ToExpr, ansiExpr) +import Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Base (enactStateSpec) +import Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Utxo (genUtxoExecContext) +import Test.Cardano.Ledger.Conway.ImpTest (impAnn, logDoc, tryRunImpRuleNoAssertions) +import Test.Cardano.Ledger.Imp.Common (expectRightExpr) +import UnliftIO (evaluateDeep) + +data ConwayLedgerExecContext era + = ConwayLedgerExecContext + { clecPolicyHash :: StrictMaybe (ScriptHash (EraCrypto era)) + , clecEnactState :: EnactState era + , clecUtxoExecContext :: UtxoExecContext era + } + deriving (Generic) + +instance + c ~ EraCrypto era => + Inject (ConwayLedgerExecContext era) (StrictMaybe (ScriptHash c)) + where + inject = clecPolicyHash + +instance Inject (ConwayLedgerExecContext Conway) (EnactState Conway) where + inject = clecEnactState + +instance + ( EraPParams era + , EraTx era + , NFData (TxWits era) + , NFData (TxAuxData era) + ) => + NFData (ConwayLedgerExecContext era) + +instance + ( EraTx era + , ToExpr (TxOut era) + , ToExpr (TxBody era) + , ToExpr (TxWits era) + , ToExpr (TxAuxData era) + , ToExpr (PParamsHKD Identity era) + ) => + ToExpr (ConwayLedgerExecContext era) + +instance EraPParams era => EncCBOR (ConwayLedgerExecContext era) where + encCBOR ConwayLedgerExecContext {..} = + encode $ + Rec ConwayLedgerExecContext + !> To clecPolicyHash + !> To clecEnactState + +instance + forall fn. + IsConwayUniv fn => + ExecSpecRule fn "LEDGER" Conway + where + type ExecContext fn "LEDGER" Conway = ConwayLedgerExecContext Conway + + genExecContext = do + ctx <- arbitrary + env <- genFromSpec @fn TrueSpec + ConwayLedgerExecContext + <$> arbitrary + <*> genFromSpec @fn (enactStateSpec ctx env) + <*> genUtxoExecContext + + environmentSpec ConwayLedgerExecContext {..} = + let UtxoExecContext {..} = clecUtxoExecContext + in constrained' $ \slotNo _txIx pp _acntSt _mempool -> + [ assert $ pp ==. lit (uePParams uecUtxoEnv) + , assert $ slotNo ==. lit (ueSlot uecUtxoEnv) + ] + + stateSpec ConwayLedgerExecContext {..} _ = + let UtxoExecContext {..} = clecUtxoExecContext + in constrained' $ \utxos certState -> + [ utxos `satisfies` utxoStateSpec clecUtxoExecContext uecUtxoEnv + , assert $ certState ==. lit (ueCertState uecUtxoEnv) + ] + + signalSpec ConwayLedgerExecContext {..} _ _ = + let UtxoExecContext {..} = clecUtxoExecContext + in constrained (==. lit uecTx) + + runAgdaRule env st sig = + first (\e -> OpaqueErrorString (T.unpack e) NE.:| []) + . computationResultToEither + $ Agda.ledgerStep env st sig + + testConformance ctx env st sig = property $ do + (specEnv, specSt, specSig) <- + impAnn "Translating the inputs" $ + translateInputs @fn @"LEDGER" @Conway env st sig ctx + logDoc $ "ctx:\n" <> ansiExpr ctx + logDoc $ "implEnv:\n" <> ansiExpr env + logDoc $ "implSt:\n" <> ansiExpr st + logDoc $ "implSig:\n" <> ansiExpr sig + logDoc $ "specEnv:\n" <> ansiExpr specEnv + logDoc $ "specSt:\n" <> ansiExpr specSt + logDoc $ "specSig:\n" <> ansiExpr specSig + agdaResTest <- + fmap (bimap (fixup <$>) fixup) $ + impAnn "Deep evaluating Agda output" $ + evaluateDeep $ + runAgdaRule @fn @"LEDGER" @Conway specEnv specSt specSig + -- TODO figure out why assertions are failing and then we can remove this + -- whole method + implRes <- tryRunImpRuleNoAssertions @"LEDGER" @Conway (inject env) (inject st) (inject sig) + implResTest <- + impAnn "Translating implementation values to SpecRep" $ + 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) + logDoc extra + checkConformance @"LEDGER" @Conway @fn + ctx + (inject env) + (inject st) + (inject sig) + implResTest + agdaResTest diff --git a/libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/ExecSpecRule/Conway/Utxo.hs b/libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/ExecSpecRule/Conway/Utxo.hs new file mode 100644 index 00000000000..60b13885f04 --- /dev/null +++ b/libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/ExecSpecRule/Conway/Utxo.hs @@ -0,0 +1,112 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE RecordWildCards #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE UndecidableInstances #-} +{-# OPTIONS_GHC -Wno-orphans #-} + +module Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Utxo ( + genUtxoExecContext, +) where + +import Cardano.Ledger.BaseTypes (ProtVer (..), natVersion) +import Cardano.Ledger.Conway (Conway) +import Cardano.Ledger.Core (EraPParams (..), ppMaxTxSizeL, sizeTxF) +import Cardano.Ledger.Shelley.LedgerState (LedgerState (..), UTxOState (..)) +import Cardano.Ledger.Shelley.Rules (UtxoEnv (..)) +import Data.Bifunctor (Bifunctor (..)) +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 Test.Cardano.Ledger.Conformance ( + ExecSpecRule (..), + OpaqueErrorString (..), + SpecTranslate (..), + computationResultToEither, + runSpecTransM, + ) +import Test.Cardano.Ledger.Conformance.SpecTranslate.Conway.Cert () +import Test.Cardano.Ledger.Conformance.SpecTranslate.Conway.Utxo () +import Test.Cardano.Ledger.Constrained.Conway ( + IsConwayUniv, + UtxoExecContext (..), + utxoEnvSpec, + utxoStateSpec, + utxoTxSpec, + ) +import Test.Cardano.Ledger.Conway.ImpTest (showConwayTxBalance) +import Test.Cardano.Ledger.Generic.GenState ( + GenEnv (..), + GenSize (..), + GenState (..), + initialLedgerState, + runGenRS, + ) +import qualified Test.Cardano.Ledger.Generic.GenState as GenSize +import qualified Test.Cardano.Ledger.Generic.PrettyCore as PP +import qualified Test.Cardano.Ledger.Generic.Proof as Proof +import Test.Cardano.Ledger.Generic.TxGen (genAlonzoTx) + +genUtxoExecContext :: Gen (UtxoExecContext Conway) +genUtxoExecContext = do + let proof = Proof.reify @Conway + ueSlot <- arbitrary + let + genSize = + GenSize.small + { invalidScriptFreq = 0 -- TODO make the test work with invalid scripts + , regCertFreq = 0 + , delegCertFreq = 0 + } + ((uecUTxO, uecTx), gs) <- + runGenRS proof genSize $ + genAlonzoTx proof ueSlot + let + txSize = uecTx ^. sizeTxF + lState = initialLedgerState gs + ueCertState = lsCertState lState + uePParams = + gePParams (gsGenEnv gs) + & ppMaxTxSizeL .~ fromIntegral txSize + & ppProtocolVersionL .~ ProtVer (natVersion @10) 0 + uecUtxoEnv = UtxoEnv {..} + pure UtxoExecContext {..} + +instance + forall fn. + IsConwayUniv fn => + ExecSpecRule fn "UTXO" Conway + where + type ExecContext fn "UTXO" Conway = UtxoExecContext Conway + + genExecContext = genUtxoExecContext + + environmentSpec = utxoEnvSpec + + stateSpec = utxoStateSpec + + signalSpec ctx _ _ = utxoTxSpec ctx + + runAgdaRule env st sig = + first (\e -> OpaqueErrorString (T.unpack e) NE.:| []) + . computationResultToEither + $ Agda.utxoStep 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 + <$> toSpecRep env + <*> toSpecRep st + <*> toSpecRep sig + ) diff --git a/libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/ExecSpecRule/Conway/Utxow.hs b/libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/ExecSpecRule/Conway/Utxow.hs new file mode 100644 index 00000000000..aa50601d380 --- /dev/null +++ b/libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/ExecSpecRule/Conway/Utxow.hs @@ -0,0 +1,52 @@ +{-# LANGUAGE AllowAmbiguousTypes #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeSynonymInstances #-} +{-# LANGUAGE UndecidableInstances #-} +{-# OPTIONS_GHC -Wno-orphans #-} + +module Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Utxow () where + +import Cardano.Ledger.Conway (Conway, ConwayEra) +import Cardano.Ledger.Conway.TxCert (ConwayTxCert) +import Cardano.Ledger.Crypto (StandardCrypto) +import Data.Bifunctor (Bifunctor (..)) +import qualified Data.List.NonEmpty as NE +import qualified Data.Text as T +import qualified Lib as Agda +import Test.Cardano.Ledger.Conformance ( + ExecSpecRule (..), + OpaqueErrorString (..), + SpecTranslate, + computationResultToEither, + ) +import Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Utxo (genUtxoExecContext) +import Test.Cardano.Ledger.Conformance.SpecTranslate.Conway.Base (ConwayTxBodyTransContext) +import Test.Cardano.Ledger.Conformance.SpecTranslate.Conway.Utxow () +import Test.Cardano.Ledger.Constrained.Conway ( + IsConwayUniv, + UtxoExecContext, + utxoEnvSpec, + utxoStateSpec, + utxoTxSpec, + ) + +instance + ( IsConwayUniv fn + , SpecTranslate (ConwayTxBodyTransContext StandardCrypto) (ConwayTxCert (ConwayEra StandardCrypto)) + ) => + ExecSpecRule fn "UTXOW" Conway + where + type ExecContext fn "UTXOW" Conway = UtxoExecContext Conway + + genExecContext = genUtxoExecContext + environmentSpec = utxoEnvSpec + stateSpec = utxoStateSpec + signalSpec ctx _ _ = utxoTxSpec ctx + runAgdaRule env st sig = + first (\e -> OpaqueErrorString (T.unpack e) NE.:| []) + . computationResultToEither + $ Agda.utxowStep env st sig 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 ab980df7b3d..6c7106113ea 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 @@ -140,6 +140,8 @@ instance NFData HsRewardUpdate instance NFData NewEpochState +instance NFData LEnv + instance ToExpr a => ToExpr (HSSet a) instance ToExpr Credential where @@ -238,6 +240,8 @@ instance ToExpr HsRewardUpdate instance ToExpr NewEpochState +instance ToExpr LEnv + instance Default (HSMap k v) instance FixupSpecRep Void 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 61acc446f3f..3249af8ae88 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 @@ -6,4 +6,6 @@ import Test.Cardano.Ledger.Conformance.SpecTranslate.Conway.Certs () import Test.Cardano.Ledger.Conformance.SpecTranslate.Conway.Deleg () import Test.Cardano.Ledger.Conformance.SpecTranslate.Conway.Gov () import Test.Cardano.Ledger.Conformance.SpecTranslate.Conway.GovCert () +import Test.Cardano.Ledger.Conformance.SpecTranslate.Conway.Ledger () import Test.Cardano.Ledger.Conformance.SpecTranslate.Conway.Pool () +import Test.Cardano.Ledger.Conformance.SpecTranslate.Conway.Utxo () diff --git a/libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/SpecTranslate/Conway/Base.hs b/libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/SpecTranslate/Conway/Base.hs index 09dc4b99570..be0cf5ec665 100644 --- a/libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/SpecTranslate/Conway/Base.hs +++ b/libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/SpecTranslate/Conway/Base.hs @@ -7,7 +7,6 @@ {-# LANGUAGE LambdaCase #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE NamedFieldPuns #-} -{-# LANGUAGE NumericUnderscores #-} {-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE PatternSynonyms #-} {-# LANGUAGE RecordWildCards #-} @@ -26,6 +25,7 @@ module Test.Cardano.Ledger.Conformance.SpecTranslate.Conway.Base ( SpecTranslationError, ConwayExecEnactEnv (..), DepositPurpose (..), + ConwayTxBodyTransContext (..), ) where import Cardano.Crypto.DSIGN (DSIGNAlgorithm (..), SignedDSIGN (..)) @@ -55,7 +55,6 @@ import Cardano.Ledger.Conway.PParams (ConwayPParams (..), THKD (..)) import Cardano.Ledger.Conway.Rules ( ConwayCertPredFailure, ConwayGovPredFailure, - ConwayUtxoPredFailure, EnactSignal (..), maxRefScriptSizePerBlock, maxRefScriptSizePerTx, @@ -75,8 +74,7 @@ import Cardano.Ledger.Plutus.Data (BinaryData, Data, Datum (..), hashBinaryData) import Cardano.Ledger.PoolDistr (IndividualPoolStake (..), PoolDistr (..)) import Cardano.Ledger.PoolParams (PoolParams (..)) import Cardano.Ledger.SafeHash (SafeHash, extractHash) -import Cardano.Ledger.Shelley.LedgerState -import Cardano.Ledger.Shelley.Rules (Identity, UtxoEnv (..)) +import Cardano.Ledger.Shelley.Rules (Identity) import Cardano.Ledger.Shelley.Scripts ( pattern RequireAllOf, pattern RequireAnyOf, @@ -297,26 +295,6 @@ instance type SpecRep (UTxO era) = SpecRep (Map (TxIn (EraCrypto era)) (TxOut era)) toSpecRep (UTxO m) = toSpecRep m -instance - ( SpecTranslate ctx (TxOut era) - , SpecRep (TxOut era) ~ Agda.TxOut - , GovState era ~ ConwayGovState era - ) => - SpecTranslate ctx (UTxOState era) - where - type SpecRep (UTxOState era) = Agda.UTxOState - - toSpecRep UTxOState {..} = do - let - gasDeposits = - Map.fromList . fmap (bimap GovActionDeposit gasDeposit) $ - OMap.assocList (utxosGovState ^. cgsProposalsL . pPropsL) - Agda.MkUTxOState - <$> toSpecRep utxosUtxo - <*> toSpecRep utxosFees - <*> toSpecRep gasDeposits - <*> toSpecRep utxosDonation - deriving instance SpecTranslate ctx SlotNo deriving instance SpecTranslate ctx EpochNo @@ -438,20 +416,6 @@ instance toSpecRep (PParams x) = toSpecRep x -instance - ( SpecRep (PParams era) ~ Agda.PParams - , SpecTranslate ctx (PParamsHKD Identity era) - ) => - SpecTranslate ctx (UtxoEnv era) - where - type SpecRep (UtxoEnv era) = Agda.UTxOEnv - - toSpecRep x = - Agda.MkUTxOEnv - <$> toSpecRep (ueSlot x) - <*> toSpecRep (uePParams x) - <*> toSpecRep (Coin 10_000_000) -- TODO: Fix generating types - instance SpecTranslate ctx a => SpecTranslate ctx (Set a) where type SpecRep (Set a) = Agda.HSSet (SpecRep a) @@ -744,17 +708,6 @@ instance <*> toSpecRep (isValid tx) <*> toSpecRep (auxiliaryData tx) -instance - ( ToExpr (Value era) - , ToExpr (TxOut era) - , ToExpr (PredicateFailure (EraRule "UTXOS" era)) - ) => - SpecTranslate ctx (ConwayUtxoPredFailure era) - where - type SpecRep (ConwayUtxoPredFailure era) = OpaqueErrorString - - toSpecRep e = pure . OpaqueErrorString . show $ toExpr e - instance ( EraPParams era , ToExpr (PParamsHKD StrictMaybe era) diff --git a/libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/SpecTranslate/Conway/Cert.hs b/libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/SpecTranslate/Conway/Cert.hs index 78e1a933a84..c56aa57e09b 100644 --- a/libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/SpecTranslate/Conway/Cert.hs +++ b/libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/SpecTranslate/Conway/Cert.hs @@ -29,7 +29,6 @@ import qualified Data.VMap as VMap import Lens.Micro import qualified Lib as Agda import Test.Cardano.Ledger.Conformance -import Test.Cardano.Ledger.Conformance.SpecTranslate.Conway.Base import Test.Cardano.Ledger.Conformance.SpecTranslate.Conway.Deleg () import Test.Cardano.Ledger.Conformance.SpecTranslate.Conway.GovCert () import Test.Cardano.Ledger.Conformance.SpecTranslate.Conway.Pool () @@ -69,14 +68,35 @@ instance Era era => SpecTranslate ctx (ConwayTxCert era) where toSpecRep (ConwayTxCertGov c) = toSpecRep c toSpecRep (ConwayTxCertDeleg x) = toSpecRep x +instance + ( SpecTranslate ctx (TxOut era) + , SpecRep (TxOut era) ~ Agda.TxOut + , GovState era ~ ConwayGovState era + , Inject ctx (CertState era) + ) => + SpecTranslate ctx (UTxOState era) + where + type SpecRep (UTxOState era) = Agda.UTxOState + + toSpecRep UTxOState {..} = do + certState <- askCtx @(CertState era) + let + props = utxosGovState ^. cgsProposalsL + deposits = depositsMap certState props + Agda.MkUTxOState + <$> toSpecRep utxosUtxo + <*> toSpecRep utxosFees + <*> toSpecRep deposits + <*> toSpecRep utxosDonation + instance ( ConwayEraGov era , SpecRep (PParamsHKD Identity era) ~ Agda.PParams , SpecTranslate ctx (PParamsHKD StrictMaybe era) , SpecRep (PParamsHKD StrictMaybe era) ~ Agda.PParamsUpdate , SpecRep (TxOut era) ~ Agda.TxOut - , SpecTranslate (Map (DepositPurpose (EraCrypto era)) Coin) (TxOut era) , GovState era ~ ConwayGovState era + , SpecTranslate (CertState era) (TxOut era) ) => SpecTranslate ctx (LedgerState era) where @@ -87,7 +107,7 @@ instance props = utxosGovState lsUTxOState ^. proposalsGovStateL deposits = depositsMap lsCertState props Agda.MkLState - <$> withCtx deposits (toSpecRep lsUTxOState) + <$> withCtx lsCertState (toSpecRep lsUTxOState) <*> toSpecRep props <*> withCtx deposits (toSpecRep lsCertState) @@ -101,8 +121,8 @@ instance , Inject ctx [GovActionState era] , ToExpr (PParamsHKD StrictMaybe era) , SpecRep (TxOut era) ~ Agda.TxOut - , SpecTranslate (Map (DepositPurpose (EraCrypto era)) Coin) (TxOut era) , GovState era ~ ConwayGovState era + , SpecTranslate (CertState era) (TxOut era) ) => SpecTranslate ctx (EpochState era) where @@ -160,8 +180,8 @@ instance , Inject ctx [GovActionState era] , ToExpr (PParamsHKD StrictMaybe era) , SpecRep (TxOut era) ~ Agda.TxOut - , SpecTranslate (Map (DepositPurpose (EraCrypto era)) Coin) (TxOut era) , GovState era ~ ConwayGovState era + , SpecTranslate (CertState era) (TxOut era) ) => SpecTranslate ctx (NewEpochState era) where diff --git a/libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/SpecTranslate/Conway/Ledger.hs b/libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/SpecTranslate/Conway/Ledger.hs new file mode 100644 index 00000000000..20e41521ac8 --- /dev/null +++ b/libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/SpecTranslate/Conway/Ledger.hs @@ -0,0 +1,58 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE RecordWildCards #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE UndecidableInstances #-} +{-# OPTIONS_GHC -Wno-orphans #-} + +module Test.Cardano.Ledger.Conformance.SpecTranslate.Conway.Ledger () where + +import Cardano.Ledger.BaseTypes (Inject) +import Cardano.Ledger.Conway.Core (Era (..), EraPParams (..), EraRule, ScriptHash) +import Cardano.Ledger.Conway.Rules (ConwayLedgerPredFailure, EnactState) +import Cardano.Ledger.Shelley.LedgerState (AccountState (..)) +import Cardano.Ledger.Shelley.Rules (LedgerEnv (..)) +import Control.State.Transition.Extended (STS (..)) +import Data.Functor.Identity (Identity) +import Data.Maybe.Strict (StrictMaybe) +import qualified Lib as Agda +import Test.Cardano.Ledger.Conformance (OpaqueErrorString (..), askCtx) +import Test.Cardano.Ledger.Conformance.SpecTranslate.Conway.Base (SpecTranslate (..)) +import Test.Cardano.Ledger.Conway.TreeDiff (ToExpr (..)) + +instance + ( EraPParams era + , SpecTranslate ctx (PParamsHKD Identity era) + , SpecRep (PParamsHKD Identity era) ~ Agda.PParams + , Inject ctx (StrictMaybe (ScriptHash (EraCrypto era))) + , Inject ctx (EnactState era) + ) => + SpecTranslate ctx (LedgerEnv era) + where + type SpecRep (LedgerEnv era) = Agda.LEnv + + toSpecRep LedgerEnv {..} = do + policyHash <- askCtx @(StrictMaybe (ScriptHash (EraCrypto era))) + enactState <- askCtx @(EnactState era) + Agda.MkLEnv + <$> toSpecRep ledgerSlotNo + <*> toSpecRep policyHash + <*> toSpecRep ledgerPp + <*> toSpecRep enactState + <*> toSpecRep (asTreasury ledgerAccount) + +instance + ( ToExpr (PredicateFailure (EraRule "GOV" era)) + , ToExpr (PredicateFailure (EraRule "CERTS" era)) + , ToExpr (PredicateFailure (EraRule "UTXOW" era)) + ) => + SpecTranslate ctx (ConwayLedgerPredFailure era) + where + type SpecRep (ConwayLedgerPredFailure era) = OpaqueErrorString + + toSpecRep e = pure . OpaqueErrorString . show $ toExpr e diff --git a/libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/SpecTranslate/Conway/Utxo.hs b/libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/SpecTranslate/Conway/Utxo.hs new file mode 100644 index 00000000000..208942ce139 --- /dev/null +++ b/libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/SpecTranslate/Conway/Utxo.hs @@ -0,0 +1,49 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE NumericUnderscores #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE UndecidableInstances #-} +{-# OPTIONS_GHC -Wno-orphans #-} + +module Test.Cardano.Ledger.Conformance.SpecTranslate.Conway.Utxo () where + +import Cardano.Ledger.Coin (Coin (..)) +import Cardano.Ledger.Conway.Core (EraPParams (..), EraRule, PParams, Value) +import Cardano.Ledger.Conway.Rules (ConwayUtxoPredFailure) +import Cardano.Ledger.Core (EraTxOut (..)) +import Cardano.Ledger.Shelley.Rules (UtxoEnv (..)) +import Control.State.Transition.Extended (STS (..)) +import Data.Functor.Identity (Identity) +import qualified Lib as Agda +import Test.Cardano.Ledger.Conformance (OpaqueErrorString (..)) +import Test.Cardano.Ledger.Conformance.SpecTranslate.Conway.Base (SpecTranslate (..)) +import Test.Cardano.Ledger.Conformance.SpecTranslate.Conway.Cert () +import Test.Cardano.Ledger.Conway.TreeDiff (ToExpr (..)) + +instance + ( SpecRep (PParams era) ~ Agda.PParams + , SpecTranslate ctx (PParamsHKD Identity era) + ) => + SpecTranslate ctx (UtxoEnv era) + where + type SpecRep (UtxoEnv era) = Agda.UTxOEnv + + toSpecRep x = + Agda.MkUTxOEnv + <$> toSpecRep (ueSlot x) + <*> toSpecRep (uePParams x) + <*> toSpecRep (Coin 10_000_000) -- TODO: Fix generating types + +instance + ( ToExpr (Value era) + , ToExpr (TxOut era) + , ToExpr (PredicateFailure (EraRule "UTXOS" era)) + ) => + SpecTranslate ctx (ConwayUtxoPredFailure era) + where + type SpecRep (ConwayUtxoPredFailure era) = OpaqueErrorString + + toSpecRep e = pure . OpaqueErrorString . show $ toExpr e diff --git a/libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/SpecTranslate/Conway/Utxow.hs b/libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/SpecTranslate/Conway/Utxow.hs new file mode 100644 index 00000000000..5f45e169ea6 --- /dev/null +++ b/libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/SpecTranslate/Conway/Utxow.hs @@ -0,0 +1,29 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE UndecidableInstances #-} +{-# OPTIONS_GHC -Wno-orphans #-} + +module Test.Cardano.Ledger.Conformance.SpecTranslate.Conway.Utxow () where + +import Cardano.Ledger.Conway.Core (AlonzoEraScript (..), AsItem, AsIx, Era, EraRule, EraTxCert (..)) +import Cardano.Ledger.Conway.Rules (ConwayUtxowPredFailure, PredicateFailure) +import Test.Cardano.Ledger.Conformance (OpaqueErrorString (..), SpecTranslate (..)) +import Test.Cardano.Ledger.Conway.TreeDiff (ToExpr, showExpr) + +import Test.Cardano.Ledger.Conformance.SpecTranslate.Conway.Utxo () + +instance + ( Era era + , ToExpr (PlutusPurpose AsIx era) + , ToExpr (PlutusPurpose AsItem era) + , ToExpr (PredicateFailure (EraRule "UTXO" era)) + , ToExpr (TxCert era) + ) => + SpecTranslate ctx (ConwayUtxowPredFailure era) + where + type SpecRep (ConwayUtxowPredFailure era) = OpaqueErrorString + + toSpecRep = pure . OpaqueErrorString . showExpr diff --git a/libs/cardano-ledger-conformance/test/Test/Cardano/Ledger/Conformance/Spec/Conway.hs b/libs/cardano-ledger-conformance/test/Test/Cardano/Ledger/Conformance/Spec/Conway.hs index f192acc3294..498d08ae060 100644 --- a/libs/cardano-ledger-conformance/test/Test/Cardano/Ledger/Conformance/Spec/Conway.hs +++ b/libs/cardano-ledger-conformance/test/Test/Cardano/Ledger/Conformance/Spec/Conway.hs @@ -33,5 +33,7 @@ spec = do prop "CERTS" $ conformsToImpl @"CERTS" @ConwayFn @Conway prop "GOV" $ conformsToImpl @"GOV" @ConwayFn @Conway prop "UTXO" $ conformsToImpl @"UTXO" @ConwayFn @Conway + xprop "UTXOW" $ conformsToImpl @"UTXOW" @ConwayFn @Conway + xprop "LEDGER" $ conformsToImpl @"LEDGER" @ConwayFn @Conway describe "ImpTests" $ do RatifyImp.spec diff --git a/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/Utxo.hs b/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/Utxo.hs index d229cea6861..1bd816670fd 100644 --- a/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/Utxo.hs +++ b/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/Utxo.hs @@ -171,6 +171,9 @@ instance !> To uecUTxO !> To uecUtxoEnv +instance Inject (UtxoExecContext era) (CertState era) where + inject = ueCertState . uecUtxoEnv + utxoTxSpec :: ( IsConwayUniv fn , HasSpec fn (AlonzoTx era) diff --git a/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Generic/GenState.hs b/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Generic/GenState.hs index b0a46d856a6..aad413a2bc1 100644 --- a/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Generic/GenState.hs +++ b/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Generic/GenState.hs @@ -211,6 +211,8 @@ data GenSize = GenSize , oldUtxoPercent :: !Int -- between 0-100, 10 means pick an old UTxO 10% of the time , maxStablePools :: !Int , invalidScriptFreq :: !Int -- percentage + , regCertFreq :: !Int + , delegCertFreq :: !Int } deriving (Show) @@ -285,6 +287,8 @@ instance Default GenSize where , withdrawalMax = 10 , maxStablePools = 5 , invalidScriptFreq = 5 + , regCertFreq = 75 + , delegCertFreq = 50 } small :: GenSize @@ -304,6 +308,8 @@ small = , withdrawalMax = 2 , maxStablePools = 4 , invalidScriptFreq = 5 + , regCertFreq = 75 + , delegCertFreq = 50 } data PlutusPurposeTag diff --git a/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Generic/TxGen.hs b/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Generic/TxGen.hs index 20e1415a321..7d036eb77d7 100644 --- a/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Generic/TxGen.hs +++ b/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Generic/TxGen.hs @@ -113,6 +113,7 @@ import Test.Cardano.Ledger.Generic.Functions import Test.Cardano.Ledger.Generic.GenState ( GenEnv (..), GenRS, + GenSize (..), GenState (..), PlutusPurposeTag (..), elementsT, @@ -579,11 +580,13 @@ chooseGood bad n xs = do -- Generating Certificates, May add to the Model genShelleyDelegCert :: forall era. Reflect era => GenRS era (TxCert era) -genShelleyDelegCert = +genShelleyDelegCert = do + regCertFreq <- asks $ regCertFreq . geSize + delegCertFreq <- asks $ delegCertFreq . geSize frequencyT - [ (75, genShelleyRegCert) + [ (regCertFreq, genShelleyRegCert) , (25, genShelleyUnRegCert) - , (50, genDelegation) + , (delegCertFreq, genDelegation) ] where genShelleyRegCert = RegTxCert <$> genFreshRegCred @era Certifying