Skip to content

Commit

Permalink
Bumped spec
Browse files Browse the repository at this point in the history
  • Loading branch information
Soupstraw committed Jan 20, 2025
1 parent 688430f commit 883e3b7
Show file tree
Hide file tree
Showing 5 changed files with 12 additions and 5 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
--sha256: sha256-fzvk/UcLDZbC+pe9K6gao8JQ/al+L+KdzyPxAaL1xiM=
tag: 098ebf75fc06635bf0a38a82f4086bbd840af7c0
--sha256: sha256-CebCHTM0lvIAJ5lx0LRcMEDeU4nGVWJlkvhJPE5tI9Y=
tag: 0f9eb79886f4d45a2cbb241af49b9e199735bd37

-- 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
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -25,7 +25,7 @@ import Cardano.Ledger.EpochBoundary
import Cardano.Ledger.Shelley.LedgerState
import qualified Data.Foldable as Set
import Data.Functor.Identity (Identity)
import Data.Map.Strict (Map)
import Data.Map.Strict (Map, keysSet)
import qualified Data.VMap as VMap
import Lens.Micro
import qualified Lib as Agda
Expand All @@ -49,11 +49,13 @@ instance
toSpecRep CertEnv {..} = do
votes <- askCtx @(VotingProcedures era)
withdrawals <- askCtx @(Map RewardAccount Coin)
let ccColdCreds = foldMap (keysSet . committeeMembers) ceCurrentCommittee
Agda.MkCertEnv
<$> toSpecRep ceCurrentEpoch
<*> toSpecRep cePParams
<*> toSpecRep votes
<*> toSpecRep withdrawals
<*> toSpecRep ccColdCreds

instance SpecTranslate ctx (CertState era) where
type SpecRep (CertState era) = Agda.CertState
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -19,6 +19,7 @@ import Cardano.Ledger.Conway.Core
import Cardano.Ledger.Conway.Governance
import Cardano.Ledger.Conway.Rules
import Data.Functor.Identity (Identity)
import Data.Map (keysSet)
import Data.Map.Strict (Map)
import qualified Lib as Agda
import Test.Cardano.Ledger.Conformance
Expand All @@ -42,8 +43,10 @@ instance
toSpecRep CertsEnv {..} = do
votes <- askCtx @(VotingProcedures era)
withdrawals <- askCtx @(Map RewardAccount Coin)
let ccColdCreds = foldMap (keysSet . committeeMembers) certsCurrentCommittee
Agda.MkCertEnv
<$> toSpecRep certsCurrentEpoch
<*> toSpecRep certsPParams
<*> toSpecRep votes
<*> toSpecRep withdrawals
<*> toSpecRep ccColdCreds
Original file line number Diff line number Diff line change
Expand Up @@ -62,7 +62,7 @@ instance SpecTranslate ctx ConwayDelegCert where
toSpecRep (ConwayUnRegCert c d) =
Agda.Dereg
<$> toSpecRep c
<*> strictMaybe (pure 0) toSpecRep d
<*> toSpecRep d
toSpecRep (ConwayDelegCert c d) =
Agda.Delegate
<$> toSpecRep c
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -33,7 +33,7 @@ import Cardano.Ledger.Credential (Credential (..))
import Cardano.Ledger.Shelley.LedgerState
import Data.Default (Default (..))
import Data.Functor.Identity (Identity)
import Data.Map.Strict (Map)
import Data.Map.Strict (Map, keysSet)
import qualified Data.Map.Strict as Map
import qualified Lib as Agda
import Test.Cardano.Ledger.Conformance.SpecTranslate.Conway.Base
Expand Down Expand Up @@ -78,11 +78,13 @@ instance
toSpecRep ConwayGovCertEnv {..} = do
votes <- askCtx @(VotingProcedures era)
withdrawals <- askCtx @(Map RewardAccount Coin)
let ccColdCreds = foldMap (keysSet . committeeMembers) cgceCurrentCommittee
Agda.MkCertEnv
<$> toSpecRep cgceCurrentEpoch
<*> toSpecRep cgcePParams
<*> toSpecRep votes
<*> toSpecRep withdrawals
<*> toSpecRep ccColdCreds

instance SpecTranslate ctx (ConwayGovCertPredFailure era) where
type SpecRep (ConwayGovCertPredFailure era) = OpaqueErrorString
Expand Down

0 comments on commit 883e3b7

Please sign in to comment.