Skip to content

Commit

Permalink
Bumped spec
Browse files Browse the repository at this point in the history
  • Loading branch information
Soupstraw committed Nov 15, 2024
1 parent 8a090f2 commit b677e0b
Show file tree
Hide file tree
Showing 15 changed files with 152 additions and 45 deletions.
4 changes: 2 additions & 2 deletions cabal.project
Original file line number Diff line number Diff line change
Expand Up @@ -24,8 +24,8 @@ source-repository-package
-- !WARNING!:
-- MAKE SURE THIS POINTS TO A COMMIT IN `MAlonzo-code` BEFORE MERGE!
subdir: generated
tag: 511c5632eff71f4811b48fba71e7aaadfd69211a
--sha256: sha256-J6Sbrr9Klz3N72wT2ZF02z5G6iFHjpwfUH2pFVoJr3c=
tag: cc93692f5a57a9a66956b232662152676f659954
--sha256: sha256-s9ikqfXmz1wBrk4qEFR/iOloKvMOPGTB5IpHO34NSLE=
-- NOTE: If you would like to update the above, look for the `MAlonzo-code`
-- branch in the `formal-ledger-specifications` repo and copy the SHA of
-- the commit you need. The `MAlonzo-code` branch functions like an alternative
Expand Down
2 changes: 2 additions & 0 deletions eras/alonzo/impl/src/Cardano/Ledger/Alonzo/Rules/Utxo.hs
Original file line number Diff line number Diff line change
Expand Up @@ -227,6 +227,8 @@ newtype AlonzoUtxoEvent era
= UtxosEvent (Event (EraRule "UTXOS" era))
deriving (Generic)

deriving instance Show (Event (EraRule "UTXOS" era)) => Show (AlonzoUtxoEvent era)

deriving instance Eq (Event (EraRule "UTXOS" era)) => Eq (AlonzoUtxoEvent era)

instance NFData (Event (EraRule "UTXOS" era)) => NFData (AlonzoUtxoEvent era)
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -14,8 +14,11 @@ import Cardano.Ledger.Alonzo.Scripts
import Cardano.Ledger.Babbage.TxBody (referenceInputsTxBodyL)
import Cardano.Ledger.Babbage.TxOut (referenceScriptTxOutL)
import Cardano.Ledger.BaseTypes
import Cardano.Ledger.CertState (DRep (..))
import Cardano.Ledger.Coin (Coin (..))
import Cardano.Ledger.Conway.PParams (ppMinFeeRefScriptCostPerByteL)
import Cardano.Ledger.Conway.PParams (ppGovActionDepositL, ppMinFeeRefScriptCostPerByteL)
import Cardano.Ledger.Conway.TxCert (Delegatee (..), pattern DelegTxCert)
import Cardano.Ledger.Credential (Credential (..))
import Cardano.Ledger.MemoBytes (getMemoRawBytes)
import Cardano.Ledger.Plutus.Language (SLanguage (..), hashPlutusScript, plutusBinary)
import Cardano.Ledger.Shelley.Core
Expand Down Expand Up @@ -64,6 +67,49 @@ spec =
[fromNativeScript spendingScript, fromNativeScript spendingScript]
++ extraScripts
++ extraScripts

it "deregistering returns the deposit" $ do
let
keyDeposit = Coin 2
-- This is paid out as the reward
govActionDeposit = Coin 3
modifyPParams $ \pp ->
pp
& ppKeyDepositL .~ keyDeposit
& ppGovActionDepositL .~ govActionDeposit
stakeCred <- KeyHashObj <$> freshKeyHash
rewardAccount <- registerStakeCredential stakeCred
otherStakeCred <- KeyHashObj <$> freshKeyHash
otherRewardAccount <- registerStakeCredential otherStakeCred
khStakePool <- freshKeyHash
registerPool khStakePool
submitTx_ . mkBasicTx $
mkBasicTxBody
& certsTxBodyL
.~ SSeq.fromList
[ DelegTxCert stakeCred (DelegStakeVote khStakePool DRepAlwaysAbstain)
, DelegTxCert otherStakeCred (DelegStakeVote khStakePool DRepAlwaysAbstain)
]
_ <- tryLookupReward stakeCred
expectRegisteredRewardAddress rewardAccount
expectRegisteredRewardAddress otherRewardAccount
submitAndExpireProposalToMakeReward otherStakeCred
lookupReward otherStakeCred `shouldReturn` govActionDeposit
submitTx_ . mkBasicTx $
mkBasicTxBody
& certsTxBodyL
.~ SSeq.fromList
[UnRegTxCert stakeCred]
& withdrawalsTxBodyL
.~ Withdrawals
( Map.fromList
[ (rewardAccount, Coin 0)
, (otherRewardAccount, govActionDeposit)
]
)
lookupReward otherStakeCred `shouldReturn` Coin 0
expectNotRegisteredRewardAddress rewardAccount
pure ()
where
checkMinFee :: HasCallStack => NativeScript era -> [Script era] -> ImpTestM era ()
checkMinFee scriptToSpend refScripts = do
Expand Down
22 changes: 14 additions & 8 deletions eras/conway/impl/testlib/Test/Cardano/Ledger/Conway/ImpTest.hs
Original file line number Diff line number Diff line change
Expand Up @@ -158,8 +158,11 @@ import Cardano.Ledger.BaseTypes (
import Cardano.Ledger.CertState (
CertState,
CommitteeAuthorization (..),
certDStateL,
certPStateL,
csCommitteeCredsL,
lookupDepositDState,
lookupDepositVState,
psStakePoolParamsL,
vsActualDRepExpiry,
vsNumDormantEpochsL,
Expand Down Expand Up @@ -190,7 +193,7 @@ import Cardano.Ledger.Crypto (Crypto (..))
import Cardano.Ledger.DRep
import Cardano.Ledger.Keys (KeyHash, KeyRole (..))
import Cardano.Ledger.Plutus.Language (Language (..), SLanguage (..), hashPlutusScript)
import Cardano.Ledger.PoolParams (ppRewardAccount)
import Cardano.Ledger.PoolParams (PoolParams (..), ppRewardAccount)
import qualified Cardano.Ledger.Shelley.HardForks as HardForks (bootstrapPhase)
import Cardano.Ledger.Shelley.LedgerState (
IncrementalStake (..),
Expand Down Expand Up @@ -1756,25 +1759,28 @@ showConwayTxBalance ::
String
showConwayTxBalance pp certState utxo tx =
unlines
[ "Consumed: \t"
[ "Consumed:"
, "\tInputs: \t" <> show (coin inputs)
, -- , "Refunds: \t" <> show refunds
"\tWithdrawals \t" <> show withdrawals
, "\tRefunds: \t" <> show refunds
, "\tWithdrawals \t" <> show withdrawals
, "\tTotal: \t" <> (show . coin $ consumed pp certState utxo txBody)
, ""
, "Produced: \t"
, "Produced:"
, "\tOutputs: \t" <> show (coin $ sumAllValue (txBody ^. outputsTxBodyL))
, "\tDonations: \t" <> show (txBody ^. treasuryDonationTxBodyL)
, "\tDeposits: \t" <> show (getTotalDepositsTxBody pp isRegPoolId txBody)
, "\tFees: \t" <> show (txBody ^. feeTxBodyL)
, "\tTotal: \t" <> (show . coin $ produced pp certState txBody)
]
where
-- lookupStakingDeposit c = certState ^. certPStateL . psStakePoolParamsL
-- lookupDRepDeposit c = undefined
txBody = tx ^. bodyTxL
inputs = balance (txInsFilter utxo (txBody ^. inputsTxBodyL))
-- refunds = getTotalRefundsTxBody pp lookupStakingDeposit lookupDRepDeposit txBody
refunds =
getTotalRefundsTxBody
pp
(lookupDepositDState $ certState ^. certDStateL)
(lookupDepositVState $ certState ^. certVStateL)
txBody
isRegPoolId = (`Map.member` (certState ^. certPStateL . psStakePoolParamsL))
withdrawals = fold . unWithdrawals $ txBody ^. withdrawalsTxBodyL

Expand Down
8 changes: 8 additions & 0 deletions eras/shelley/impl/src/Cardano/Ledger/Shelley/Rules/Utxo.hs
Original file line number Diff line number Diff line change
Expand Up @@ -127,6 +127,14 @@ instance EraPParams era => EncCBOR (UtxoEnv era) where
!> To uePParams
!> To ueCertState

instance EraPParams era => DecCBOR (UtxoEnv era) where
decCBOR =
decode $
RecD UtxoEnv
<! From
<! From
<! D decNoShareCBOR

utxoEnvSlotL :: Lens' (UtxoEnv era) SlotNo
utxoEnvSlotL = lens ueSlot $ \x y -> x {ueSlot = y}

Expand Down
12 changes: 9 additions & 3 deletions eras/shelley/impl/testlib/Test/Cardano/Ledger/Shelley/ImpTest.hs
Original file line number Diff line number Diff line change
Expand Up @@ -71,6 +71,7 @@ module Test.Cardano.Ledger.Shelley.ImpTest (
registerRewardAccount,
registerStakeCredential,
getRewardAccountFor,
tryLookupReward,
lookupReward,
poolParams,
registerPool,
Expand Down Expand Up @@ -1444,17 +1445,22 @@ registerRewardAccount = do
khDelegator <- freshKeyHash
registerStakeCredential (KeyHashObj khDelegator)

tryLookupReward :: Credential 'Staking (EraCrypto era) -> ImpTestM era (Maybe Coin)
tryLookupReward stakingCredential = do
umap <- getsNES (nesEsL . epochStateUMapL)
pure $ fromCompact . rdReward <$> UMap.lookup stakingCredential (RewDepUView umap)

lookupReward :: HasCallStack => Credential 'Staking (EraCrypto era) -> ImpTestM era Coin
lookupReward stakingCredential = do
umap <- getsNES (nesEsL . epochStateUMapL)
case UMap.lookup stakingCredential (RewDepUView umap) of
mbyRwd <- tryLookupReward stakingCredential
case mbyRwd of
Just c -> pure c
Nothing ->
error $
"Staking Credential is not found in the state: "
<> show stakingCredential
<> "\nMake sure you have the reward account registered with `registerRewardAccount` "
<> "or by some other means."
Just rd -> pure $ fromCompact (rdReward rd)

poolParams ::
ShelleyEraImp era =>
Expand Down
Original file line number Diff line number Diff line change
@@ -1,23 +1,46 @@
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}

module Test.Cardano.Ledger.Api.DebugTools where

import Cardano.Ledger.Binary (DecCBOR, EncCBOR, Version, decodeFull')
import Cardano.Ledger.Binary (
Annotator,
DecCBOR (..),
DecShareCBOR,
EncCBOR,
Version,
decNoShareCBOR,
decodeFull',
decodeFullAnnotator,
decodeFullDecoder',
)
import Cardano.Ledger.Binary.Encoding (serialize')
import Cardano.Ledger.Core (Era, eraProtVerLow)
import Control.Exception (throwIO)
import Control.Exception (Exception, throwIO)
import Control.Monad.IO.Class (MonadIO (..))
import qualified Data.ByteString as BS
import qualified Data.ByteString.Lazy as LBS

readCBOR :: (DecCBOR a, MonadIO m) => Version -> FilePath -> m a
readCBOR version path = liftIO $ do
readCBORWith ::
(MonadIO m, Exception e) => (Version -> BS.ByteString -> Either e a) -> Version -> FilePath -> m a
readCBORWith dec version path = liftIO $ do
dat <- BS.readFile path
case decodeFull' version dat of
case dec version dat of
Right x -> pure x
Left err -> throwIO err

readCBOR :: (DecCBOR a, MonadIO m) => Version -> FilePath -> m a
readCBOR = readCBORWith decodeFull'

readCBORNoShare :: (MonadIO m, DecShareCBOR a) => Version -> FilePath -> m a
readCBORNoShare = readCBORWith (\v bs -> decodeFullDecoder' v "DecodeNoShare" decNoShareCBOR bs)

readCBORAnnotated :: (MonadIO m, DecCBOR (Annotator a)) => Version -> FilePath -> m a
readCBORAnnotated = readCBORWith (\v bs -> decodeFullAnnotator v "DecodeAnnotated" decCBOR (LBS.fromStrict bs))

writeCBOR :: (EncCBOR a, MonadIO m) => Version -> FilePath -> a -> m ()
writeCBOR version path = liftIO . BS.writeFile path . serialize' version

Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -408,7 +408,7 @@ instance IsConwayUniv fn => ExecSpecRule fn "RATIFY" Conway where
. computationResultToEither
$ Agda.ratifyStep env st sig

extraInfo ctx env@RatifyEnv {..} st sig@(RatifySignal actions) =
extraInfo ctx env@RatifyEnv {..} st sig@(RatifySignal actions) _ =
PP.vsep $ specExtraInfo : (actionAcceptedRatio <$> toList actions)
where
members = foldMap' (committeeMembers @Conway) $ ensCommittee (rsEnactState st)
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -55,7 +55,7 @@ instance
-- The results of runConformance are Agda types, the `ctx` is a Haskell type, we extract and translate the Withdrawal keys.
specWithdrawalCredSet <-
translateWithContext () (Map.keysSet (Map.mapKeys raCredential (ccecWithdrawals ctx)))
(implResTest, agdaResTest) <- runConformance @"CERTS" @fn @Conway ctx env st sig
(implResTest, agdaResTest, _) <- runConformance @"CERTS" @fn @Conway ctx env st sig
case (implResTest, agdaResTest) of
(Right haskell, Right spec) ->
checkConformance @"CERTS" @Conway @fn
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -175,7 +175,7 @@ instance
expectRightExpr $
runSpecTransM ctx $
bimapM (traverse toTestRep) (toTestRep . inject @_ @(ExecState fn "LEDGER" Conway) . fst) implRes
let extra = extraInfo @fn @"LEDGER" @Conway ctx (inject env) (inject st) (inject sig)
let extra = extraInfo @fn @"LEDGER" @Conway ctx (inject env) (inject st) (inject sig) implRes
logDoc extra
checkConformance @"LEDGER" @Conway @fn
ctx
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -24,7 +24,9 @@ import qualified Data.List.NonEmpty as NE
import qualified Data.Text as T
import Lens.Micro ((&), (.~), (^.))
import qualified Lib as Agda
import Test.Cardano.Ledger.Common (Arbitrary (..), Gen)
import Prettyprinter ((<+>))
import qualified Prettyprinter as PP
import Test.Cardano.Ledger.Common (Arbitrary (..), Gen, showExpr)
import Test.Cardano.Ledger.Conformance (
ExecSpecRule (..),
OpaqueErrorString (..),
Expand All @@ -43,6 +45,7 @@ import Test.Cardano.Ledger.Constrained.Conway (
utxoTxSpec,
)
import Test.Cardano.Ledger.Conway.ImpTest (showConwayTxBalance)
import Test.Cardano.Ledger.Generic.Functions (TotalAda (..))
import Test.Cardano.Ledger.Generic.GenState (
GenEnv (..),
GenSize (..),
Expand Down Expand Up @@ -100,14 +103,21 @@ instance
. computationResultToEither
$ Agda.utxoStep externalFunctions env st sig

extraInfo ctx env@UtxoEnv {..} st@UTxOState {..} sig =
"Impl:\n"
<> PP.ppString (showConwayTxBalance uePParams ueCertState utxosUtxo sig)
<> "\n\nSpec:\n"
<> PP.ppString
( either show T.unpack . runSpecTransM ctx $
Agda.utxoDebug externalFunctions
<$> toSpecRep env
<*> toSpecRep st
<*> toSpecRep sig
)
extraInfo ctx env@UtxoEnv {..} st@UTxOState {..} sig st' =
PP.vcat
[ "Impl:"
, PP.ppString (showConwayTxBalance uePParams ueCertState utxosUtxo sig)
, "initial TotalAda:" <+> PP.ppString (showExpr $ totalAda st)
, "final TotalAda: " <+> case st' of
Right (x, _) -> PP.ppString (showExpr $ totalAda x)
Left _ -> "N/A"
, mempty
, "Spec:"
, PP.ppString
( either show T.unpack . runSpecTransM ctx $
Agda.utxoDebug externalFunctions
<$> toSpecRep env
<*> toSpecRep st
<*> toSpecRep sig
)
]
Original file line number Diff line number Diff line change
Expand Up @@ -213,8 +213,11 @@ class
Environment (EraRule rule era) ->
State (EraRule rule era) ->
Signal (EraRule rule era) ->
Either
(NonEmpty (PredicateFailure (EraRule rule era)))
(State (EraRule rule era), [Event (EraRule rule era)]) ->
Doc AnsiStyle
extraInfo _ _ _ _ = mempty
extraInfo _ _ _ _ _ = mempty

dumpCbor ::
forall era a.
Expand Down Expand Up @@ -266,10 +269,6 @@ checkConformance ctx env st sig implResTest agdaResTest = do
annotate (color Yellow) . vsep $
[ "===== DIFF ====="
, ppEditExpr conformancePretty (ediff implResTest agdaResTest)
, ""
, "Legend:"
, indent 2 $ annotate (color delColor) "-Implementation"
, indent 2 $ annotate (color insColor) "+Specification"
]
unless (implResTest == agdaResTest) $ do
let envVarName = "CONFORMANCE_CBOR_DUMP_PATH"
Expand Down Expand Up @@ -315,8 +314,8 @@ defaultTestConformance ::
ExecSignal fn rule era ->
Property
defaultTestConformance ctx env st sig = property $ do
(implResTest, agdaResTest) <- runConformance @rule @fn @era ctx env st sig
let extra = extraInfo @fn @rule @era ctx (inject env) (inject st) (inject sig)
(implResTest, agdaResTest, implRes) <- runConformance @rule @fn @era ctx env st sig
let extra = extraInfo @fn @rule @era ctx (inject env) (inject st) (inject sig) implRes
logDoc extra
checkConformance @rule @_ @fn ctx (inject env) (inject st) (inject sig) implResTest agdaResTest

Expand Down Expand Up @@ -345,6 +344,9 @@ runConformance ::
, Either
(NonEmpty (SpecRep (PredicateFailure (EraRule rule era))))
(SpecRep (ExecState fn rule era))
, Either
(NonEmpty (PredicateFailure (EraRule rule era)))
(State (EraRule rule era), [Event (EraRule rule era)])
)
runConformance execContext env st sig = do
(specEnv, specSt, specSig) <-
Expand All @@ -368,7 +370,7 @@ runConformance execContext env st sig = do
expectRightExpr $
runSpecTransM execContext $
bimapM (traverse toTestRep) (toTestRep . inject @_ @(ExecState fn rule era) . fst) implRes
pure (implResTest, agdaResTest)
pure (implResTest, agdaResTest, implRes)

conformsToImpl ::
forall (rule :: Symbol) fn era.
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -133,7 +133,7 @@ spec = withImpInit @(LedgerSpec Conway) $ describe "RATIFY" $ modifyImpInitProtV
let
ratSt = getRatifyState govSt
ratSig = RatifySignal (constitutionGAS SSeq.:<| mempty)
(implRes, agdaRes) <-
(implRes, agdaRes, implRes') <-
runConformance @"RATIFY" @ConwayFn @Conway
execCtx
ratEnv
Expand All @@ -158,4 +158,5 @@ spec = withImpInit @(LedgerSpec Conway) $ describe "RATIFY" $ modifyImpInitProtV
ratEnv
ratSt
ratSig
implRes'
impAnn "Conformance failed" $ implRes `shouldBeExpr` agdaRes
Original file line number Diff line number Diff line change
Expand Up @@ -25,4 +25,5 @@ library
constrained-generators,
data-default,
QuickCheck,
ImpSpec,
microlens
Loading

0 comments on commit b677e0b

Please sign in to comment.