Skip to content

Commit

Permalink
Remove Crypto from cardano-ledger-conformance
Browse files Browse the repository at this point in the history
  • Loading branch information
Lucsanszky committed Dec 9, 2024
1 parent 7761195 commit 05ab36c
Show file tree
Hide file tree
Showing 24 changed files with 234 additions and 267 deletions.
Original file line number Diff line number Diff line change
Expand Up @@ -14,7 +14,6 @@
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE ViewPatterns #-}
{-# OPTIONS_GHC -Wno-orphans #-}
Expand Down Expand Up @@ -47,7 +46,7 @@ import Cardano.Ledger.CertState (
CommitteeState (..),
)
import Cardano.Ledger.Coin (Coin (..), CompactForm (..))
import Cardano.Ledger.Conway (Conway)
import Cardano.Ledger.Conway (ConwayEra)
import Cardano.Ledger.Conway.Core (Era (..), EraPParams (..), PParams)
import Cardano.Ledger.Conway.Governance (
Committee (..),
Expand Down Expand Up @@ -122,7 +121,7 @@ import Cardano.Crypto.DSIGN (SignedDSIGN (..), verifySignedDSIGN)
import Cardano.Crypto.Hash (ByteString, Hash)
import Cardano.Ledger.Address (RewardAccount)
import Cardano.Ledger.Credential (Credential)
import Cardano.Ledger.Crypto (Crypto (..), StandardCrypto)
import Cardano.Ledger.Crypto (DSIGN, HASH)
import Cardano.Ledger.Keys (KeyRole (..), VKey (..))
import Data.Either (isRight)
import Data.Maybe (fromMaybe)
Expand All @@ -131,10 +130,10 @@ import Test.Cardano.Ledger.Conway.Arbitrary ()
import Test.Cardano.Ledger.Imp.Common hiding (arbitrary, forAll, prop, var)

data ConwayCertExecContext era = ConwayCertExecContext
{ ccecWithdrawals :: !(Map (RewardAccount (EraCrypto era)) Coin)
, ccecDeposits :: !(Map (DepositPurpose (EraCrypto era)) Coin)
{ ccecWithdrawals :: !(Map (RewardAccount) Coin)
, ccecDeposits :: !(Map (DepositPurpose) Coin)
, ccecVotes :: !(VotingProcedures era)
, ccecDelegatees :: !(Set (Credential 'DRepRole (EraCrypto era)))
, ccecDelegatees :: !(Set (Credential 'DRepRole))
}
deriving (Generic, Eq, Show)

Expand Down Expand Up @@ -165,19 +164,13 @@ instance Era era => DecCBOR (ConwayCertExecContext era) where
<! From
<! From

instance
c ~ EraCrypto era =>
Inject (ConwayCertExecContext era) (Map (RewardAccount c) Coin)
where
instance Inject (ConwayCertExecContext era) (Map RewardAccount Coin) where
inject = ccecWithdrawals

instance Inject (ConwayCertExecContext era) (VotingProcedures era) where
inject = ccecVotes

instance
c ~ EraCrypto era =>
Inject (ConwayCertExecContext era) (Map (DepositPurpose c) Coin)
where
instance Inject (ConwayCertExecContext era) (Map DepositPurpose Coin) where
inject = ccecDeposits

instance Era era => ToExpr (ConwayCertExecContext era)
Expand Down Expand Up @@ -248,11 +241,11 @@ instance EraPParams era => NFData (ConwayRatifyExecContext era)

ratifyEnvSpec ::
( IsConwayUniv fn
, HasSpec fn (RatifyEnv Conway)
, HasSpec fn (SimpleRep (RatifyEnv Conway))
, HasSpec fn (RatifyEnv ConwayEra)
, HasSpec fn (SimpleRep (RatifyEnv ConwayEra))
) =>
ConwayRatifyExecContext Conway ->
Specification fn (RatifyEnv Conway)
ConwayRatifyExecContext ConwayEra ->
Specification fn (RatifyEnv ConwayEra)
ratifyEnvSpec ConwayRatifyExecContext {crecGovActionMap} =
constrained' $ \_ poolDistr drepDistr drepState _ committeeState _ _ ->
[ -- Bias the generator towards generating DReps that have stake and are registered
Expand Down Expand Up @@ -329,9 +322,9 @@ ratifyEnvSpec ConwayRatifyExecContext {crecGovActionMap} =

ratifyStateSpec ::
IsConwayUniv fn =>
ConwayRatifyExecContext Conway ->
RatifyEnv Conway ->
Specification fn (RatifyState Conway)
ConwayRatifyExecContext ConwayEra ->
RatifyEnv ConwayEra ->
Specification fn (RatifyState ConwayEra)
ratifyStateSpec _ RatifyEnv {..} =
constrained' $ \ens enacted expired _ ->
mconcat
Expand Down Expand Up @@ -364,14 +357,14 @@ ratifyStateSpec _ RatifyEnv {..} =
let CommitteeState m = reCommitteeState
in Map.keysSet m
-- Bootstrap is not in the spec
disableBootstrap :: IsConwayUniv fn => Term fn (PParams Conway) -> Pred fn
disableBootstrap :: IsConwayUniv fn => Term fn (PParams ConwayEra) -> Pred fn
disableBootstrap pp = match pp $ \simplepp ->
match (protocolVersion_ simplepp) $ \major _ ->
assert $ not_ (major ==. lit (natVersion @9))

preferSmallerCCMinSizeValues ::
IsConwayUniv fn =>
Term fn (PParams Conway) ->
Term fn (PParams ConwayEra) ->
Pred fn
preferSmallerCCMinSizeValues pp = match pp $ \simplepp ->
satisfies (committeeMinSize_ simplepp) $
Expand All @@ -383,17 +376,17 @@ ratifyStateSpec _ RatifyEnv {..} =

ratifySignalSpec ::
IsConwayUniv fn =>
ConwayRatifyExecContext Conway ->
Specification fn (RatifySignal Conway)
ConwayRatifyExecContext ConwayEra ->
Specification fn (RatifySignal ConwayEra)
ratifySignalSpec ConwayRatifyExecContext {crecGovActionMap} =
constrained $ \sig ->
match sig $ \gasS ->
match gasS $ \gasL ->
forAll gasL $ \gas ->
gas `elem_` lit crecGovActionMap

instance IsConwayUniv fn => ExecSpecRule fn "RATIFY" Conway where
type ExecContext fn "RATIFY" Conway = ConwayRatifyExecContext Conway
instance IsConwayUniv fn => ExecSpecRule fn "RATIFY" ConwayEra where
type ExecContext fn "RATIFY" ConwayEra = ConwayRatifyExecContext ConwayEra

genExecContext = arbitrary

Expand All @@ -411,7 +404,7 @@ instance IsConwayUniv fn => ExecSpecRule fn "RATIFY" Conway where
extraInfo _ ctx env@RatifyEnv {..} st sig@(RatifySignal actions) _ =
PP.vsep $ specExtraInfo : (actionAcceptedRatio <$> toList actions)
where
members = foldMap' (committeeMembers @Conway) $ ensCommittee (rsEnactState st)
members = foldMap' (committeeMembers @ConwayEra) $ ensCommittee (rsEnactState st)
showAccepted True = PP.brackets ""
showAccepted False = PP.brackets "×"
showRatio r = PP.viaShow (numerator r) <> "/" <> PP.viaShow (denominator r)
Expand Down Expand Up @@ -451,7 +444,7 @@ instance IsConwayUniv fn => ExecSpecRule fn "RATIFY" Conway where

testConformance ctx env st@(RatifyState {rsEnactState}) sig@(RatifySignal actions) =
labelRatios $
defaultTestConformance @fn @Conway @"RATIFY" ctx env st sig
defaultTestConformance @fn @ConwayEra @"RATIFY" ctx env st sig
where
bucket r
| r == 0 % 1 = "=0%"
Expand All @@ -463,14 +456,14 @@ instance IsConwayUniv fn => ExecSpecRule fn "RATIFY" Conway where
| r == 1 % 1 = "=100%"
| otherwise = error "ratio is not in the unit interval"
committee = ensCommittee rsEnactState
members = foldMap' (committeeMembers @Conway) committee
members = foldMap' (committeeMembers @ConwayEra) committee
pv = st ^. rsEnactStateL . ensProtVerL
ccBucket a =
"CC yes votes ratio \t"
<> bucket
( committeeAcceptedRatio
members
(gasCommitteeVotes @Conway a)
(gasCommitteeVotes @ConwayEra a)
(reCommitteeState env)
(reCurrentEpoch env)
)
Expand Down Expand Up @@ -512,10 +505,10 @@ instance Era era => EncCBOR (ConwayEnactExecContext era) where

enactSignalSpec ::
IsConwayUniv fn =>
ConwayEnactExecContext Conway ->
ConwayExecEnactEnv Conway ->
EnactState Conway ->
Specification fn (EnactSignal Conway)
ConwayEnactExecContext ConwayEra ->
ConwayExecEnactEnv ConwayEra ->
EnactState ConwayEra ->
Specification fn (EnactSignal ConwayEra)
enactSignalSpec ConwayEnactExecContext {..} ConwayExecEnactEnv {..} EnactState {..} =
constrained' $ \gid action ->
[ assert $ gid ==. lit ceeeGid
Expand Down Expand Up @@ -544,21 +537,21 @@ enactSignalSpec ConwayEnactExecContext {..} ConwayExecEnactEnv {..} EnactState {

enactStateSpec ::
IsConwayUniv fn =>
ConwayEnactExecContext Conway ->
ConwayExecEnactEnv Conway ->
Specification fn (EnactState Conway)
ConwayEnactExecContext ConwayEra ->
ConwayExecEnactEnv ConwayEra ->
Specification fn (EnactState ConwayEra)
enactStateSpec ConwayEnactExecContext {..} ConwayExecEnactEnv {..} =
constrained' $ \_ _ curPParams _ treasury wdrls _ ->
[ match curPParams $ \simplepp -> committeeMaxTermLength_ simplepp ==. lit ceecMaxTerm
, assert $ sum_ (rng_ wdrls) <=. treasury
, assert $ treasury ==. lit ceeeTreasury
]

instance IsConwayUniv fn => ExecSpecRule fn "ENACT" Conway where
type ExecContext fn "ENACT" Conway = ConwayEnactExecContext Conway
type ExecEnvironment fn "ENACT" Conway = ConwayExecEnactEnv Conway
type ExecState fn "ENACT" Conway = EnactState Conway
type ExecSignal fn "ENACT" Conway = EnactSignal Conway
instance IsConwayUniv fn => ExecSpecRule fn "ENACT" ConwayEra where
type ExecContext fn "ENACT" ConwayEra = ConwayEnactExecContext ConwayEra
type ExecEnvironment fn "ENACT" ConwayEra = ConwayExecEnactEnv ConwayEra
type ExecState fn "ENACT" ConwayEra = EnactState ConwayEra
type ExecSignal fn "ENACT" ConwayEra = EnactSignal ConwayEra

environmentSpec _ = TrueSpec
stateSpec = enactStateSpec
Expand All @@ -585,9 +578,9 @@ nameGovAction UpdateCommittee {} = "UpdateCommittee"
nameGovAction NewConstitution {} = "NewConstitution"
nameGovAction InfoAction {} = "InfoAction"

instance IsConwayUniv fn => ExecSpecRule fn "EPOCH" Conway where
type ExecContext fn "EPOCH" Conway = [GovActionState Conway]
type ExecEnvironment fn "EPOCH" Conway = EpochExecEnv Conway
instance IsConwayUniv fn => ExecSpecRule fn "EPOCH" ConwayEra where
type ExecContext fn "EPOCH" ConwayEra = [GovActionState ConwayEra]
type ExecEnvironment fn "EPOCH" ConwayEra = EpochExecEnv ConwayEra

environmentSpec _ = epochEnvSpec

Expand All @@ -605,9 +598,9 @@ instance IsConwayUniv fn => ExecSpecRule fn "EPOCH" Conway where
nameEpoch :: EpochNo -> String
nameEpoch x = show x

instance IsConwayUniv fn => ExecSpecRule fn "NEWEPOCH" Conway where
type ExecContext fn "NEWEPOCH" Conway = [GovActionState Conway]
type ExecEnvironment fn "NEWEPOCH" Conway = EpochExecEnv Conway
instance IsConwayUniv fn => ExecSpecRule fn "NEWEPOCH" ConwayEra where
type ExecContext fn "NEWEPOCH" ConwayEra = [GovActionState ConwayEra]
type ExecEnvironment fn "NEWEPOCH" ConwayEra = EpochExecEnv ConwayEra

environmentSpec _ = epochEnvSpec

Expand All @@ -626,15 +619,15 @@ externalFunctions = Agda.MkExternalFunctions {..}
extIsSigned vk ser sig =
isRight $
verifySignedDSIGN
@(DSIGN StandardCrypto)
@(Hash (HASH StandardCrypto) ByteString)
@DSIGN
@(Hash HASH ByteString)
()
vkey
hash
signature
where
vkey =
unVKey @_ @StandardCrypto
unVKey
. fromMaybe (error "Failed to convert an Agda VKey to a Haskell VKey")
$ vkeyFromInteger vk
hash =
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -2,11 +2,8 @@
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -Wno-orphans #-}

Expand All @@ -17,7 +14,6 @@ import Cardano.Ledger.BaseTypes (Inject)
import Cardano.Ledger.Coin (Coin)
import Cardano.Ledger.Conway
import Cardano.Ledger.Conway.TxCert (ConwayTxCert (..))
import Cardano.Ledger.Crypto (StandardCrypto)
import Constrained (lit)
import Data.Bifunctor (first)
import qualified Data.List.NonEmpty as NE
Expand All @@ -33,11 +29,11 @@ import Test.Cardano.Ledger.Constrained.Conway

instance
( IsConwayUniv fn
, Inject (ConwayCertExecContext Conway) (Map (RewardAccount StandardCrypto) Coin)
, Inject (ConwayCertExecContext ConwayEra) (Map RewardAccount Coin)
) =>
ExecSpecRule fn "CERT" Conway
ExecSpecRule fn "CERT" ConwayEra
where
type ExecContext fn "CERT" Conway = ConwayCertExecContext Conway
type ExecContext fn "CERT" ConwayEra = ConwayCertExecContext ConwayEra
environmentSpec _ = certEnvSpec
stateSpec ctx _ = certStateSpec (lit $ ccecDelegatees ctx)
signalSpec _ = txCertSpec
Expand All @@ -48,7 +44,7 @@ instance

classOf = Just . nameTxCert

nameTxCert :: ConwayTxCert Conway -> String
nameTxCert :: ConwayTxCert ConwayEra -> String
nameTxCert (ConwayTxCertDeleg x) = nameDelegCert x
nameTxCert (ConwayTxCertPool x) = namePoolCert x
nameTxCert (ConwayTxCertGov x) = nameGovCert x
Original file line number Diff line number Diff line change
Expand Up @@ -28,9 +28,9 @@ import Test.Cardano.Ledger.Imp.Common hiding (context)

instance
IsConwayUniv fn =>
ExecSpecRule fn "CERTS" Conway
ExecSpecRule fn "CERTS" ConwayEra
where
type ExecContext fn "CERTS" Conway = ConwayCertExecContext Conway
type ExecContext fn "CERTS" ConwayEra = ConwayCertExecContext ConwayEra

environmentSpec _ = certsEnvSpec

Expand All @@ -55,10 +55,10 @@ 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 @ConwayEra ctx env st sig
case (implResTest, agdaResTest) of
(Right haskell, Right spec) ->
checkConformance @"CERTS" @Conway @fn
checkConformance @"CERTS" @ConwayEra @fn
ctx
env
st
Expand All @@ -74,7 +74,7 @@ instance
credsSet = Set.fromList creds
zeroRewards (Agda.MkHSMap pairs) =
Agda.MkHSMap (map (\(c, r) -> if c `Set.member` credsSet then (c, 0) else (c, r)) pairs)
_ -> checkConformance @"CERTS" @Conway @fn ctx env st sig implResTest agdaResTest
_ -> checkConformance @"CERTS" @ConwayEra @fn ctx env st sig implResTest agdaResTest

nameCerts :: Seq (ConwayTxCert Conway) -> String
nameCerts :: Seq (ConwayTxCert ConwayEra) -> String
nameCerts x = "Certs length " ++ show (length x)
Original file line number Diff line number Diff line change
Expand Up @@ -11,7 +11,6 @@ module Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Deleg (nameDelegCert)
import Cardano.Ledger.Conway
import Cardano.Ledger.Conway.TxCert (ConwayDelegCert (..))
import Cardano.Ledger.Credential (Credential)
import Cardano.Ledger.Crypto (StandardCrypto)
import Cardano.Ledger.Keys (KeyRole (..))
import Constrained (lit)
import Data.Bifunctor (bimap)
Expand All @@ -26,8 +25,8 @@ import Test.Cardano.Ledger.Conformance.SpecTranslate.Conway.Cert ()
import Test.Cardano.Ledger.Conformance.SpecTranslate.Conway.Deleg ()
import Test.Cardano.Ledger.Constrained.Conway

instance IsConwayUniv fn => ExecSpecRule fn "DELEG" Conway where
type ExecContext fn "DELEG" Conway = Set (Credential 'DRepRole StandardCrypto)
instance IsConwayUniv fn => ExecSpecRule fn "DELEG" ConwayEra where
type ExecContext fn "DELEG" ConwayEra = Set (Credential 'DRepRole)

environmentSpec _ = delegEnvSpec

Expand All @@ -44,7 +43,7 @@ instance IsConwayUniv fn => ExecSpecRule fn "DELEG" Conway where

classOf = Just . nameDelegCert

nameDelegCert :: ConwayDelegCert c -> String
nameDelegCert :: ConwayDelegCert -> String
nameDelegCert ConwayRegCert {} = "RegKey"
nameDelegCert ConwayUnRegCert {} = "UnRegKey"
nameDelegCert ConwayDelegCert {} = "DelegateWithKey"
Expand Down
Loading

0 comments on commit 05ab36c

Please sign in to comment.