From ff6bea477e286a56ca56263524ab883c1f013dea Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Joosep=20J=C3=A4=C3=A4ger?= Date: Thu, 11 Apr 2024 12:40:31 +0300 Subject: [PATCH] WIP --- cabal.project | 4 +- .../Test/Cardano/Ledger/Shelley/ImpTest.hs | 53 +++--- .../testlib/Test/Cardano/Data/TreeDiff.hs | 6 +- .../cardano-ledger-conformance.cabal | 1 + .../Ledger/Conformance/ExecSpecRule/Conway.hs | 152 ++++++++++++++++-- .../Ledger/Conformance/ExecSpecRule/Core.hs | 89 +++++++--- .../Cardano/Ledger/Conformance/Spec/Conway.hs | 7 +- .../Conformance/SpecTranslate/Conway.hs | 117 ++++++++++---- .../Ledger/Constrained/Conway/Instances.hs | 2 +- 9 files changed, 340 insertions(+), 91 deletions(-) diff --git a/cabal.project b/cabal.project index 0268777d8ed..34e0279d071 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: 324fafa887b7b6b38e15d2b505c4eec5a3247176 - --sha256: sha256-zpQToGA04NQ3TfkeWBJXIzisvoGLfYdWNbVQ/2BfeEI= + tag: 9233cb9f0e15dcdb5ef7ba49a21ee3820ee9aa76 + --sha256: sha256-ea99nQ/j62FJkVdACKffVgLZ5mR1ZKwakSlNcSi5fJA= index-state: -- Bump this if you need newer packages from Hackage 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 cb354f84770..21352d27029 100644 --- a/eras/shelley/impl/testlib/Test/Cardano/Ledger/Shelley/ImpTest.hs +++ b/eras/shelley/impl/testlib/Test/Cardano/Ledger/Shelley/ImpTest.hs @@ -577,6 +577,17 @@ newtype ImpTestM era a = ImpTestM {unImpTestM :: ReaderT (ImpTestEnv era) (GenT , MonadReader (ImpTestEnv era) ) +instance + ( Testable a + , ShelleyEraImp era + ) => + Testable (ImpTestM era a) + where + property m = property . fmap ioProperty . runGenT $ do + st <- liftIO mkImpState + res <- liftGen $ runImpTestGenM st m + liftIO $ fst <$> res + instance MonadWriter [SomeSTSEvent era] (ImpTestM era) where writer (x, evs) = (impEventsL %= (<> evs)) $> x listen act = do @@ -1079,26 +1090,21 @@ logEntry e = impLogL %= (<> pretty loc <> "\t" <> pretty e <> line) logToExpr :: (HasCallStack, ToExpr a) => a -> ImpTestM era () logToExpr e = logEntry (showExpr e) -withImpState :: - forall era. - ShelleyEraImp era => - SpecWith (ImpTestState era) -> - Spec -withImpState = - beforeAll $ - execStateT addRootTxOut $ - ImpTestState - { impNES = initImpNES - , impRootTxIn = rootTxIn - , impKeyPairs = mempty - , impByronKeyPairs = mempty - , impNativeScripts = mempty - , impLastTick = 0 - , impGlobals = testGlobals - , impLog = mempty - , impGen = qcGen - , impEvents = mempty - } +mkImpState :: ShelleyEraImp era => IO (ImpTestState era) +mkImpState = + execStateT addRootTxOut $ + ImpTestState + { impNES = initImpNES + , impRootTxIn = rootTxIn + , impKeyPairs = mempty + , impByronKeyPairs = mempty + , impNativeScripts = mempty + , impLastTick = 0 + , impGlobals = testGlobals + , impLog = mempty + , impGen = qcGen + , impEvents = mempty + } where rootCoin = Coin 1_000_000_000 rootTxIn = TxIn (mkTxId 0) minBound @@ -1110,6 +1116,13 @@ withImpState = impNESL . nesEsL . esLStateL . lsUTxOStateL . utxosUtxoL %= (<> UTxO (Map.singleton rootTxIn rootTxOut)) +withImpState :: + forall era. + ShelleyEraImp era => + SpecWith (ImpTestState era) -> + Spec +withImpState = beforeAll mkImpState + -- | Creates a fresh @SafeHash@ freshSafeHash :: Era era => ImpTestM era (SafeHash (EraCrypto era) a) freshSafeHash = arbitrary diff --git a/libs/cardano-data/testlib/Test/Cardano/Data/TreeDiff.hs b/libs/cardano-data/testlib/Test/Cardano/Data/TreeDiff.hs index 03e1e2f1cb0..2ee8b22d349 100644 --- a/libs/cardano-data/testlib/Test/Cardano/Data/TreeDiff.hs +++ b/libs/cardano-data/testlib/Test/Cardano/Data/TreeDiff.hs @@ -5,12 +5,14 @@ module Test.Cardano.Data.TreeDiff where +import Data.Foldable (Foldable (..)) import Data.Foldable qualified as F import Data.OMap.Strict import Data.OSet.Strict -import Test.Cardano.Ledger.Binary.TreeDiff (ToExpr (..)) +import Test.Cardano.Ledger.Binary.TreeDiff (Expr (..), ToExpr (..)) -deriving instance ToExpr a => ToExpr (OSet a) +instance ToExpr a => ToExpr (OSet a) where + toExpr x = App "OSet.fromList" [toExpr $ toList x] instance (HasOKey k v, ToExpr v) => ToExpr (OMap k v) where listToExpr = listToExpr . F.toList diff --git a/libs/cardano-ledger-conformance/cardano-ledger-conformance.cabal b/libs/cardano-ledger-conformance/cardano-ledger-conformance.cabal index af70b1ce977..2e848ac3b9f 100644 --- a/libs/cardano-ledger-conformance/cardano-ledger-conformance.cabal +++ b/libs/cardano-ledger-conformance/cardano-ledger-conformance.cabal @@ -41,6 +41,7 @@ library base >=4.14 && <5, cardano-data, cardano-strict-containers, + data-default-class, microlens, mtl, cardano-ledger-binary, 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 d070588392d..f939c33faa8 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 @@ -15,10 +15,11 @@ module Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway () where -import Cardano.Ledger.BaseTypes (Inject (..)) +import Cardano.Ledger.BaseTypes (Inject (..), StrictMaybe (..)) import Cardano.Ledger.Conway (Conway) -import Cardano.Ledger.Conway.Core (Era (..), EraPParams) -import Cardano.Ledger.Conway.Governance (EnactState) +import Cardano.Ledger.Conway.Core (Era (..), EraPParams, PParamsUpdate) +import Cardano.Ledger.Conway.Governance (EnactState, GovProcedures, ProposalProcedure, Proposals) +import Cardano.Ledger.Conway.PParams (THKD (..)) import Cardano.Ledger.Conway.Rules (ConwayGovPredFailure) import Cardano.Ledger.Conway.Tx (AlonzoTx) import Constrained @@ -26,6 +27,7 @@ import Control.DeepSeq (NFData) import Data.Bifunctor (Bifunctor (..)) import qualified Data.List.NonEmpty as NE import qualified Data.Text as T +import Data.Typeable (Typeable) import GHC.Generics (Generic) import qualified Lib as Agda import Test.Cardano.Ledger.Conformance ( @@ -72,6 +74,118 @@ instance c ~ EraCrypto era => Inject (ConwayGovExecContext era) (GovProceduresSp instance Inject (ConwayGovExecContext era) (EnactState era) where inject (ConwayGovExecContext _ x) = x +agdaCompatiblePPU :: IsConwayUniv fn => Term fn (PParamsUpdate Conway) -> Pred fn +agdaCompatiblePPU ppup = + match ppup $ + \cppMinFeeA + cppMinFeeB + cppMaxBBSize + cppMaxTxSize + cppMaxBHSize + cppKeyDeposit + cppPoolDeposit + cppEMax + cppNOpt + cppA0 + cppRho + cppTau + _cppProtocolVersion + cppMinPoolCost + cppCoinsPerUTxOByte + cppCostModels + cppPrices + cppMaxTxExUnits + cppMaxBlockExUnits + cppMaxValSize + cppCollateralPercentage + cppMaxCollateralInputs + cppPoolVotingThresholds + cppDRepVotingThresholds + cppCommitteeMinSize + cppCommitteeMaxTermLength + cppGovActionLifetime + cppGovActionDeposit + cppDRepDeposit + cppDRepActivity + cppMinFeeRefScriptCostPerByte -> + -- TODO enable pparam updates once they're properly + -- implemented in the spec + mconcat + [ isModified cppMinFeeA + , isUnmodified cppMinFeeB + , isUnmodified cppMaxBBSize + , isUnmodified cppMaxTxSize + , isUnmodified cppMaxBHSize + , isUnmodified cppKeyDeposit + , isUnmodified cppPoolDeposit + , isUnmodified cppEMax + , isUnmodified cppNOpt + , isUnmodified cppA0 + , isUnmodified cppRho + , isUnmodified cppTau + , isUnmodified cppMinPoolCost + , isUnmodified cppCoinsPerUTxOByte + , isUnmodified cppCostModels + , isUnmodified cppPrices + , isUnmodified cppMaxTxExUnits + , isUnmodified cppMaxBlockExUnits + , isUnmodified cppMaxValSize + , isUnmodified cppCollateralPercentage + , isUnmodified cppMaxCollateralInputs + , isUnmodified cppPoolVotingThresholds + , isUnmodified cppDRepVotingThresholds + , isUnmodified cppCommitteeMinSize + , isUnmodified cppCommitteeMaxTermLength + , isUnmodified cppGovActionLifetime + , isUnmodified cppGovActionDeposit + , isUnmodified cppDRepDeposit + , isUnmodified cppDRepActivity + , isUnmodified cppMinFeeRefScriptCostPerByte + ] + where + isUnmodified :: + ( HasSpec fn a + , Typeable gs + , IsNormalType a + , IsConwayUniv fn + ) => + Term fn (THKD gs StrictMaybe a) -> + Pred fn + isUnmodified x = + caseOn + x + (branch $ const True) + (branch $ const False) + isModified :: + ( HasSpec fn a + , Typeable gs + , IsNormalType a + , IsConwayUniv fn + ) => + Term fn (THKD gs StrictMaybe a) -> + Pred fn + isModified x = + caseOn + x + (branch $ const False) + (branch $ const True) + +agdaCompatibleProposal :: + IsConwayUniv fn => + Term fn (ProposalProcedure Conway) -> + Pred fn +agdaCompatibleProposal prop = + match prop $ \_ _ govAction _ -> + caseOn + govAction + (branch $ \_ ppup _ -> agdaCompatiblePPU ppup) + (branch $ \_ _ -> True) + (branch $ \_ _ -> True) + (branch $ const True) + (branch $ \_ _ _ _ -> True) + (branch $ \_ _ -> True) + (branch $ const True) + instance ( NFData (SpecRep (ConwayGovPredFailure Conway)) , IsConwayUniv fn @@ -82,9 +196,20 @@ instance environmentSpec = govEnvSpec - stateSpec = govProposalsSpec + stateSpec env = govProposalsSpec env <> constrained agdaConstraints + where + agdaConstraints :: Term fn (Proposals Conway) -> Pred fn + agdaConstraints props = match @fn props $ \ppups _ _ _ _ -> + match ppups $ \_ ppupForest -> + forAll ppupForest $ \ppupTree -> + forAll' ppupTree $ \gas _ -> + match gas $ \_ _ _ _ prop _ _ -> agdaCompatibleProposal prop - signalSpec = govProceduresSpec + signalSpec env st = govProceduresSpec env st <> constrained agdaConstraints + where + agdaConstraints :: Term fn (GovProcedures Conway) -> Pred fn + agdaConstraints procs = match @fn procs $ \_ props -> + forAll props agdaCompatibleProposal execContextSpec = TrueSpec @@ -127,15 +252,14 @@ instance _ctbCurrentTreasuryValue _ctbTreasuryDonation -> match ctbOutputs $ - \outs -> forAll outs $ - \x -> match x $ - \txOut _ -> match txOut $ - \_ _ dat _ -> - caseOn - dat - (branch $ const True) - (branch $ const True) - (branch $ const False) + \outs -> forAll' outs $ + \txOut _ -> match txOut $ + \_ _ dat _ -> + caseOn + dat + (branch $ const True) + (branch $ const True) + (branch $ const False) runAgdaRule env st sig = first (\e -> OpaqueErrorString (T.unpack e) NE.:| []) diff --git a/libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/ExecSpecRule/Core.hs b/libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/ExecSpecRule/Core.hs index b82cbae363a..ca89a5e990b 100644 --- a/libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/ExecSpecRule/Core.hs +++ b/libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/ExecSpecRule/Core.hs @@ -19,7 +19,7 @@ module Test.Cardano.Ledger.Conformance.ExecSpecRule.Core ( import Cardano.Ledger.BaseTypes (Inject, ShelleyBase) import Cardano.Ledger.Core (EraRule) import qualified Constrained as CV2 -import Constrained.Base (Spec (..)) +import Constrained.Base (Spec (..), shrinkWithSpec) import Control.State.Transition.Extended (STS (..)) import Data.Bifunctor (Bifunctor (..)) import Data.Bitraversable (bimapM) @@ -31,15 +31,19 @@ import Test.Cardano.Ledger.Conformance.SpecTranslate.Core (SpecTranslate (..), r import Test.Cardano.Ledger.Imp.Common ( MonadGen (..), NFData, + Property, ToExpr, + counterexample, + diffExpr, expectRightExpr, - shouldBeExpr, + forAllShrinkShow, + showExpr, ) import Test.Cardano.Ledger.Shelley.ImpTest ( ImpTestM, + ShelleyEraImp, impAnn, logEntry, - logToExpr, tryRunImpRule, ) @@ -98,25 +102,40 @@ class (NonEmpty (SpecRep (PredicateFailure (EraRule rule era)))) (SpecRep (State (EraRule rule era))) -conformsToImpl :: - forall (rule :: Symbol) fn era. +impSpecTrans :: + SpecTranslate ctx a => + ctx -> + a -> + ImpTestM era (SpecRep a) +impSpecTrans ctx x = do + let res = runSpecTransM ctx $ toSpecRep x + expectRightExpr res + +runConformance :: + forall (rule :: Symbol) (fn :: [Type] -> Type -> Type) era. ( ExecSpecRule fn rule era - , NFData (SpecRep (PredicateFailure (EraRule rule era))) + , NFData (SpecRep (Environment (EraRule rule era))) , NFData (SpecRep (State (EraRule rule era))) + , NFData (SpecRep (Signal (EraRule rule era))) ) => - ImpTestM era () -conformsToImpl = impAnn "conformsToImpl" . resize 5 $ do - env <- liftGen . CV2.genFromSpec_ $ environmentSpec @fn @rule @era - logToExpr env - st <- liftGen . CV2.genFromSpec_ $ stateSpec @fn @rule @era env - logToExpr st - sig <- liftGen . CV2.genFromSpec_ $ signalSpec @fn @rule @era env st - logToExpr sig - logEntry . show $ signalSpec @fn @rule @era env st + Environment (EraRule rule era) -> + State (EraRule rule era) -> + Signal (EraRule rule era) -> + ImpTestM + era + ( Either + (NonEmpty (TestRep (PredicateFailure (EraRule rule era)))) + (TestRep (State (EraRule rule era))) + , Either + (NonEmpty (TestRep (PredicateFailure (EraRule rule era)))) + (TestRep (State (EraRule rule era))) + ) +runConformance env st sig = do (execContext :: ctx) <- liftGen . CV2.genFromSpec_ $ execContextSpec @fn @rule @era - agdaRes <- - impAnn "Translating spec values to SpecRep" . expectRightExpr . runSpecTransM execContext $ - runAgdaRule @fn @rule @era <$> toSpecRep env <*> toSpecRep st <*> toSpecRep sig + specEnv <- impAnn "Translating the environment" $ impSpecTrans execContext env + specSt <- impAnn "Translating the state" $ impSpecTrans execContext st + specSig <- impAnn "Translating the signal" $ impSpecTrans execContext sig + let agdaRes = runAgdaRule @fn @rule @era specEnv specSt specSig implRes <- fmap fst <$> tryRunImpRule @rule @era env st sig implResTest <- impAnn "Translating implementation values to SpecRep" . expectRightExpr . runSpecTransM execContext $ @@ -127,7 +146,39 @@ conformsToImpl = impAnn "conformsToImpl" . resize 5 $ do (fmap $ specToTestRep @ctx @(PredicateFailure (EraRule rule era))) (specToTestRep @ctx @(State (EraRule rule era))) agdaRes - agdaResTest `shouldBeExpr` implResTest + pure (implResTest, agdaResTest) + +conformsToImpl :: + forall (rule :: Symbol) fn era. + ( ShelleyEraImp era + , ExecSpecRule fn rule era + , NFData (SpecRep (Environment (EraRule rule era))) + , NFData (SpecRep (State (EraRule rule era))) + , NFData (SpecRep (Signal (EraRule rule era))) + ) => + Property +conformsToImpl = + let envSpec = environmentSpec @fn @rule @era + in forAllShrinkShow (CV2.genFromSpec_ envSpec) (shrinkWithSpec envSpec) showExpr $ \env -> + let stSpec = stateSpec @fn @rule @era env + in forAllShrinkShow (CV2.genFromSpec_ stSpec) (shrinkWithSpec stSpec) showExpr $ \st -> + let sigSpec = signalSpec @fn @rule @era env st + in forAllShrinkShow (CV2.genFromSpec_ sigSpec) (shrinkWithSpec sigSpec) showExpr $ \sig -> + resize 5 $ do + logEntry @era . show $ signalSpec @fn @rule @era env st + (implResTest, agdaResTest) <- runConformance @rule @fn env st sig + let + failMsg = + unlines + [ "" + , "===== DIFF =====" + , diffExpr implResTest agdaResTest + , "" + , "Legend:" + , "\t\ESC[91mImplemenation" + , "\t\ESC[92mSpecification\ESC[39m" + ] + pure . counterexample failMsg $ implResTest == agdaResTest computationResultToEither :: Agda.ComputationResult e a -> Either e a computationResultToEither (Agda.Success x) = Right x diff --git a/libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/Spec/Conway.hs b/libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/Spec/Conway.hs index b51c8166923..fb45b1d6f46 100644 --- a/libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/Spec/Conway.hs +++ b/libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/Spec/Conway.hs @@ -7,11 +7,10 @@ import Cardano.Ledger.Conway (Conway) import Test.Cardano.Ledger.Conformance (conformsToImpl) import Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway () import Test.Cardano.Ledger.Constrained.Conway -import Test.Cardano.Ledger.Conway.ImpTest (withImpState) +import Test.Cardano.Ledger.Conway.ImpTest () import Test.Cardano.Ledger.Imp.Common spec :: Spec spec = describe "Conway conformance tests" $ do - withImpState @Conway $ do - xit "UTXO" . replicateM_ 100 $ conformsToImpl @"UTXO" @ConwayFn - xit "GOV" . replicateM_ 100 $ conformsToImpl @"GOV" @ConwayFn + xprop "UTXO" $ conformsToImpl @"UTXO" @ConwayFn @Conway + prop "GOV" $ conformsToImpl @"GOV" @ConwayFn @Conway 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 ffbdd5cf991..39015ecda13 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 @@ -28,7 +28,7 @@ module Test.Cardano.Ledger.Conformance.SpecTranslate.Conway ( import Cardano.Crypto.DSIGN (DSIGNAlgorithm (..), SignedDSIGN (..)) import Cardano.Crypto.Hash (Hash, hashToBytes) import Cardano.Ledger.Address (Addr (..), RewardAccount (..), serialiseAddr) -import Cardano.Ledger.Alonzo (AlonzoTxAuxData) +import Cardano.Ledger.Alonzo (AlonzoTxAuxData, MaryValue) import Cardano.Ledger.Alonzo.PParams (OrdExUnits (OrdExUnits)) import Cardano.Ledger.Alonzo.Scripts (AlonzoPlutusPurpose (..)) import Cardano.Ledger.Alonzo.Tx (AlonzoTx (..)) @@ -77,7 +77,7 @@ import Cardano.Ledger.Conway.Governance ( ) import Cardano.Ledger.Conway.PParams (ConwayPParams (..), THKD (..)) import Cardano.Ledger.Conway.Rules (ConwayGovPredFailure, GovEnv (..)) -import Cardano.Ledger.Conway.Scripts (ConwayPlutusPurpose (..)) +import Cardano.Ledger.Conway.Scripts (AlonzoScript, ConwayPlutusPurpose (..)) import Cardano.Ledger.Conway.TxCert ( ConwayDelegCert (..), ConwayGovCert (..), @@ -92,7 +92,7 @@ import Cardano.Ledger.HKD (HKD) import Cardano.Ledger.Keys (KeyHash (..), VKey (..)) import Cardano.Ledger.Keys.WitVKey (WitVKey (..)) import Cardano.Ledger.Plutus (CostModels, ExUnits (..), Prices) -import Cardano.Ledger.Plutus.Data (Data, Datum (..)) +import Cardano.Ledger.Plutus.Data (BinaryData, Data, Datum (..), hashBinaryData) import Cardano.Ledger.PoolParams (PoolParams (..)) import Cardano.Ledger.SafeHash (SafeHash, extractHash) import Cardano.Ledger.Shelley.LedgerState (UTxOState (..)) @@ -108,6 +108,7 @@ import Control.State.Transition.Extended (STS (..)) import Data.Bifunctor (Bifunctor (..)) import Data.Bitraversable (bimapM) import Data.Data (Typeable) +import Data.Default.Class (Default (..)) import Data.Foldable (Foldable (..)) import qualified Data.List as L import Data.Map.Strict (Map) @@ -131,7 +132,7 @@ import Test.Cardano.Ledger.Conformance ( askTransCtx, ) import Test.Cardano.Ledger.Constrained.Conway.Instances (IsConwayUniv) -import Test.Cardano.Ledger.Conway.TreeDiff (ToExpr (..)) +import Test.Cardano.Ledger.Conway.TreeDiff (Expr (..), ToExpr (..)) -- | OpaqueErrorString behaves like unit in comparisons, but contains an -- error string that can be displayed. @@ -141,7 +142,11 @@ newtype OpaqueErrorString = OpaqueErrorString String instance Eq OpaqueErrorString where _ == _ = True -instance ToExpr OpaqueErrorString +instance ToExpr OpaqueErrorString where + -- Using `toExpr` on a `String` displays escape codes in place of unicode + -- characters (e.g. "≡" becomes "\8802") + -- TODO figure out a less hacky way to solve this problem + toExpr (OpaqueErrorString x) = App "OpaqueErrorString" [App x []] instance NFData OpaqueErrorString @@ -175,18 +180,48 @@ instance SpecTranslate ctx (SafeHash c EraIndependentTxBody) where toSpecRep = toSpecRep . extractHash -instance EraTxOut era => SpecTranslate ctx (BabbageTxOut era) where +instance + ( SpecRep (DataHash (EraCrypto era)) ~ Agda.DataHash + , Era era + ) => + SpecTranslate ctx (BinaryData era) + where + type SpecRep (BinaryData era) = Agda.DataHash + + toSpecRep = toSpecRep . hashBinaryData + +instance Era era => SpecTranslate ctx (Datum era) where + type SpecRep (Datum era) = Maybe (Either Agda.Datum Agda.DataHash) + + toSpecRep NoDatum = pure Nothing + toSpecRep (Datum d) = Just . Left <$> toSpecRep d + toSpecRep (DatumHash h) = Just . Right <$> toSpecRep h + +instance + Script era ~ AlonzoScript era => + SpecTranslate ctx (AlonzoScript era) + where + type SpecRep (AlonzoScript era) = Agda.DataHash + + toSpecRep _ = pure () + +instance + ( EraTxOut era + , SpecRep (Script era) ~ Agda.DataHash + , SpecRep (Value era) ~ Agda.Coin + , SpecTranslate ctx (Value era) + , SpecTranslate ctx (Script era) + ) => + SpecTranslate ctx (BabbageTxOut era) + where type SpecRep (BabbageTxOut era) = Agda.TxOut - toSpecRep (BabbageTxOut addr val datum _) = - let mkTxOut x = do - addr' <- toSpecRep addr - coin' <- toSpecRep $ coin val - pure (addr', (coin', x)) - in case datum of - NoDatum -> mkTxOut Nothing - DatumHash h -> mkTxOut . Just =<< toSpecRep h - Datum _ -> throwError "Inline datums not supported by spec" + toSpecRep (BabbageTxOut addr val datum script) = do + addr' <- toSpecRep addr + val' <- toSpecRep val + datum' <- toSpecRep datum + script' <- toSpecRep script + pure (addr', (val', (datum', script'))) instance SpecTranslate ctx Integer where type SpecRep Integer = Integer @@ -244,11 +279,9 @@ instance SpecTranslate ctx VotingThresholds where toSpecRep _ = pure () instance SpecTranslate ctx CostModels where - type SpecRep CostModels = Agda.AgdaEmpty + type SpecRep CostModels = () - toSpecRep _ = - pure $ - error "TODO change this to unit once it is fixed in the spec" + toSpecRep _ = pure () instance SpecTranslate ctx Prices where type SpecRep Prices = () @@ -589,7 +622,7 @@ toAgdaTxBody :: ( SpecRep (TxOut era) ~ Agda.TxOut , SpecRep (TxCert era) ~ Agda.TxCert , EraTx era - , AlonzoEraTxBody era + , BabbageEraTxBody era , SpecTranslate ctx (TxOut era) , SpecTranslate ctx (TxCert era) ) => @@ -598,6 +631,7 @@ toAgdaTxBody :: toAgdaTxBody tx = Agda.MkTxBody <$> toSpecRep (tx ^. bodyTxL . inputsTxBodyL) + <*> toSpecRep (tx ^. bodyTxL . referenceInputsTxBodyL) <*> (zip [0 ..] <$> toSpecRep (tx ^. bodyTxL . outputsTxBodyL)) <*> toSpecRep (tx ^. bodyTxL . feeTxBodyL) <*> toSpecRep (tx ^. bodyTxL . vldtTxBodyL) @@ -619,7 +653,7 @@ instance , SpecRep (TxCert era) ~ Agda.TxCert , Tx era ~ AlonzoTx era , EraTx era - , AlonzoEraTxBody era + , BabbageEraTxBody era ) => SpecTranslate ctx (AlonzoTx era) where @@ -658,7 +692,7 @@ instance SpecTranslate ctx (GovPurposeId r c) where toSpecRep (GovPurposeId gaId) = toSpecRep gaId instance SpecTranslate ctx UnitInterval where - type SpecRep UnitInterval = (Integer, Integer) + type SpecRep UnitInterval = Agda.Rational toSpecRep x = pure (numerator r, denominator r) where @@ -760,10 +794,21 @@ instance SpecTranslate ctx (VotingProcedures era) where ) <*> m -instance SpecTranslate ctx (GovAction era) where +instance EraPParams era => SpecTranslate ctx (GovAction era) where type SpecRep (GovAction era) = Agda.GovAction - toSpecRep ParameterChange {} = pure $ Agda.ChangePParams () + -- TODO remove the failure cases once it's possible to update all of the + -- parameters in the spec + toSpecRep (ParameterChange _ ppu _) + | SJust minFeeA <- ppu ^. ppuMinFeeAL = + if ppu == (def & ppuMinFeeAL .~ SJust minFeeA) + then Agda.ChangePParams <$> toSpecRep minFeeA + else + throwError + "Expecting PParamsUpdate to update only minFeeA, but it's also updating something else" + | otherwise = + throwError + "Expecting PParamsUpdate to update minFeeA, but it's not" toSpecRep (HardForkInitiation _ pv) = Agda.TriggerHF <$> toSpecRep pv toSpecRep (TreasuryWithdrawals withdrawals _) = Agda.TreasuryWdrl @@ -781,6 +826,7 @@ instance SpecTranslate ctx (GovAction era) where toSpecRep InfoAction = pure Agda.Info toAgdaProposalProcedure :: + EraPParams era => GovActionId (EraCrypto era) -> StrictMaybe (ScriptHash (EraCrypto era)) -> ProposalProcedure era -> @@ -825,7 +871,9 @@ instance HasSimpleRep (GovProceduresSpecTransCtx c) instance (IsConwayUniv fn, Crypto c) => HasSpec fn (GovProceduresSpecTransCtx c) instance - Inject ctx (GovProceduresSpecTransCtx (EraCrypto era)) => + ( Inject ctx (GovProceduresSpecTransCtx (EraCrypto era)) + , EraPParams era + ) => SpecTranslate ctx (GovProcedures era) where type SpecRep (GovProcedures era) = [Agda.GovSignal] @@ -839,7 +887,7 @@ instance (toAgdaProposalProcedure gaId policy) (toList gpProposalProcedures) -instance SpecTranslate ctx (GovActionState era) where +instance EraPParams era => SpecTranslate ctx (GovActionState era) where type SpecRep (GovActionState era) = Agda.GovActionState toSpecRep gas@GovActionState {..} = @@ -847,9 +895,10 @@ instance SpecTranslate ctx (GovActionState era) where <$> agdaVoteMap <*> toSpecRep (gasReturnAddr gas) <*> toSpecRep gasExpiresAfter - <*> toSpecRep (gasAction gas) - <*> toSpecRep gasId + <*> toSpecRep action + <*> toSpecRep (nullifyIfNotNeeded gasId action) where + action = gasAction gas agdaVoteMap = do drepVotes <- toSpecRep gasDRepVotes ccVotes <- toSpecRep gasCommitteeVotes @@ -860,6 +909,11 @@ instance SpecTranslate ctx (GovActionState era) where , first (Agda.CC,) <$> ccVotes , first (\h -> (Agda.SPO, Agda.KeyHashObj h)) <$> spoVotes ] + nullGovActionId = GovActionId (TxId def) (GovActionIx 0) + nullifyIfNotNeeded gaId = \case + TreasuryWithdrawals {} -> nullGovActionId + InfoAction -> nullGovActionId + _ -> gaId instance SpecTranslate ctx GovActionIx where type SpecRep GovActionIx = Integer @@ -871,7 +925,12 @@ instance SpecTranslate ctx (GovActionId c) where toSpecRep (GovActionId txId gaIx) = toSpecRep (txId, gaIx) -instance SpecTranslate ctx (Proposals era) where +instance EraPParams era => SpecTranslate ctx (Proposals era) where type SpecRep (Proposals era) = Agda.GovState toSpecRep = toSpecRep . view pPropsL + +instance Crypto c => SpecTranslate ctx (MaryValue c) where + type SpecRep (MaryValue c) = Agda.Coin + + toSpecRep = toSpecRep . coin diff --git a/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/Instances.hs b/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/Instances.hs index bc157f2ddc7..c10b8c80dce 100644 --- a/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/Instances.hs +++ b/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/Instances.hs @@ -887,7 +887,7 @@ instance HasSimpleRep (NoUpdate a) instance (IsConwayUniv fn, Typeable a) => HasSpec fn (NoUpdate a) instance HasSimpleRep (THKD tag StrictMaybe a) where - type SimpleRep (THKD tag StrictMaybe a) = SimpleRep (StrictMaybe a) + type SimpleRep (THKD tag StrictMaybe a) = SOP (TheSop (StrictMaybe a)) fromSimpleRep = THKD . fromSimpleRep toSimpleRep (THKD sm) = toSimpleRep sm instance (IsConwayUniv fn, Typeable tag, HasSpec fn a) => HasSpec fn (THKD tag StrictMaybe a)