Bumped spec

IntersectMBO · Nov 12, 2024 · 85a7379 · 85a7379
1 parent f5cffc3
commit 85a7379
Show file tree

Hide file tree

Showing 19 changed files with 162 additions and 118 deletions.
diff --git 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: bc70df238ef53d30eb79a9de526c4e181b291c71
-  --sha256: sha256-NMcuS0hJFIkqonoIl5+jOSBjeaFWXOtB25xN5tUmUWc=
+  tag: 0909247e93410fca93180ca8a5d8e25ce4adb1e5
+  --sha256: sha256-iwFwUqI9qqGmMMwp9uu4CCsoVLbC235IcsxAl8XnBz0=
 -- 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/...ardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/ExecSpecRule/Conway/Base.hs b/...ardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/ExecSpecRule/Conway/Base.hs
@@ -28,12 +28,14 @@ module Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Base (
   crecTreasuryL,
   crecGovActionMapL,
   enactStateSpec,
+  externalFunctions,
 ) where
 
 import Cardano.Ledger.BaseTypes (
   EpochInterval (..),
   EpochNo (..),
   Inject (..),
+  Network (..),
   StrictMaybe (..),
   addEpochInterval,
   natVersion,
@@ -55,7 +57,6 @@ import Cardano.Ledger.Conway.Governance (
   RatifyEnv (..),
   RatifySignal (..),
   RatifyState (..),
-  Vote (Abstain),
   VotingProcedures,
   ensProtVerL,
   gasAction,
@@ -92,13 +93,15 @@ import Test.Cardano.Ledger.Conformance (
   ExecSpecRule (..),
   SpecTranslate (..),
   computationResultToEither,
+  integerToHash,
   runSpecTransM,
  )
 import Test.Cardano.Ledger.Conformance.ExecSpecRule.Core (defaultTestConformance)
-import Test.Cardano.Ledger.Conformance.SpecTranslate.Conway ()
+import Test.Cardano.Ledger.Conformance.SpecTranslate.Conway (vkeyFromInteger)
 import Test.Cardano.Ledger.Conformance.SpecTranslate.Conway.Base (
   ConwayExecEnactEnv (..),
   DepositPurpose,
+  signatureFromInteger,
  )
 import Test.Cardano.Ledger.Constrained.Conway (
   EpochExecEnv,
@@ -115,14 +118,23 @@ import Test.Cardano.Ledger.Constrained.Conway.Instances.PParams (
   protocolVersion_,
  )
 
+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.Keys (KeyRole (..), VKey (..))
+import Data.Either (isRight)
+import Data.Maybe (fromMaybe)
+import Data.Set (Set)
 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)
   , ccecVotes :: !(VotingProcedures era)
+  , ccecDelegatees :: !(Set (Credential 'DRepRole (EraCrypto era)))
   }
   deriving (Generic, Eq, Show)
 
@@ -132,15 +144,17 @@ instance Era era => Arbitrary (ConwayCertExecContext era) where
       <$> arbitrary
       <*> arbitrary
       <*> arbitrary
+      <*> arbitrary
 
 instance Era era => EncCBOR (ConwayCertExecContext era) where
-  encCBOR x@(ConwayCertExecContext _ _ _) =
+  encCBOR x@(ConwayCertExecContext _ _ _ _) =
     let ConwayCertExecContext {..} = x
      in encode $
           Rec ConwayCertExecContext
             !> To ccecWithdrawals
             !> To ccecDeposits
             !> To ccecVotes
+            !> To ccecDelegatees
 
 instance Era era => DecCBOR (ConwayCertExecContext era) where
   decCBOR =
@@ -149,6 +163,7 @@ instance Era era => DecCBOR (ConwayCertExecContext era) where
         <! From
         <! From
         <! From
+        <! From
 
 instance
   c ~ EraCrypto era =>
@@ -300,9 +315,7 @@ ratifyEnvSpec ConwayRatifyExecContext {crecGovActionMap} =
     spoVotes =
       foldr'
         ( \GovActionState {gasStakePoolVotes} s ->
-            -- TODO: Remove the filter when
-            -- https://github.com/IntersectMBO/formal-ledger-specifications/issues/578 is resolved
-            Map.keysSet (Map.filter (== Abstain) gasStakePoolVotes) <> s
+            Map.keysSet gasStakePoolVotes <> s
         )
         mempty
         crecGovActionMap
@@ -514,7 +527,11 @@ enactSignalSpec ConwayEnactExecContext {..} ConwayExecEnactEnv {..} EnactState {
         (branch $ \_ _ _ -> True)
         (branch $ \_ _ -> True)
         ( branch $ \newWdrls _ ->
-            sum_ (rng_ newWdrls) + lit (sum ensWithdrawals) <=. lit ceeeTreasury
+            [ assert $ sum_ (rng_ newWdrls) + lit (sum ensWithdrawals) <=. lit ceeeTreasury
+            , assert $ forAll' newWdrls $ \acct _ ->
+                match acct $ \network _ ->
+                  network ==. lit Testnet
+            ]
         )
         (branch $ \_ -> True)
         ( branch $ \_ _ newMembers _ ->
@@ -602,3 +619,30 @@ instance IsConwayUniv fn => ExecSpecRule fn "NEWEPOCH" Conway where
     first (\case {})
       . computationResultToEither
       $ Agda.newEpochStep env st sig
+
+externalFunctions :: Agda.ExternalFunctions
+externalFunctions = Agda.MkExternalFunctions {..}
+  where
+    extIsSigned vk ser sig =
+      isRight $
+        verifySignedDSIGN
+          @(DSIGN StandardCrypto)
+          @(Hash (HASH StandardCrypto) ByteString)
+          ()
+          vkey
+          hash
+          signature
+      where
+        vkey =
+          unVKey @_ @StandardCrypto
+            . fromMaybe (error "Failed to convert an Agda VKey to a Haskell VKey")
+            $ vkeyFromInteger vk
+        hash =
+          fromMaybe
+            (error $ "Failed to get hash from integer:\n" <> show ser)
+            $ integerToHash ser
+        signature =
+          SignedDSIGN
+            . fromMaybe
+              (error "Failed to decode the signature")
+            $ signatureFromInteger sig
diff --git a/...ardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/ExecSpecRule/Conway/Cert.hs b/...ardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/ExecSpecRule/Conway/Cert.hs
@@ -18,6 +18,7 @@ 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
 import Data.Map.Strict (Map)
@@ -38,7 +39,7 @@ instance
   where
   type ExecContext fn "CERT" Conway = ConwayCertExecContext Conway
   environmentSpec _ = certEnvSpec
-  stateSpec _ _ = certStateSpec
+  stateSpec ctx _ = certStateSpec (lit $ ccecDelegatees ctx)
   signalSpec _ = txCertSpec
   runAgdaRule env st sig =
     first (\e -> OpaqueErrorString (T.unpack e) NE.:| [])

diff --git a/...rdano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/ExecSpecRule/Conway/Certs.hs b/...rdano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/ExecSpecRule/Conway/Certs.hs
@@ -37,10 +37,10 @@ instance
   stateSpec context _ =
     constrained $ \x ->
       match x $ \vstate pstate dstate ->
-        [ satisfies vstate vStateSpec
+        [ satisfies vstate (vStateSpec (lit $ ccecDelegatees context))
         , satisfies pstate pStateSpec
         , -- temporary workaround because Spec does some extra tests, that the implementation does not, in the bootstrap phase.
-          satisfies dstate (bootstrapDStateSpec (ccecWithdrawals context))
+          satisfies dstate (bootstrapDStateSpec (ccecDelegatees context) (ccecWithdrawals context))
         ]
 
   signalSpec _ = txCertsSpec

diff --git a/...rdano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/ExecSpecRule/Conway/Deleg.hs b/...rdano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/ExecSpecRule/Conway/Deleg.hs
@@ -2,15 +2,21 @@
 {-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE FlexibleInstances #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE UndecidableInstances #-}
 {-# OPTIONS_GHC -Wno-orphans #-}
 
 module Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Deleg (nameDelegCert) where
 
 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)
 import qualified Data.List.NonEmpty as NE
+import Data.Set (Set)
 import qualified Data.Text as T
 import qualified Lib as Agda
 import Test.Cardano.Ledger.Conformance
@@ -21,9 +27,11 @@ 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)
+
   environmentSpec _ = delegEnvSpec
 
-  stateSpec _ _ = certStateSpec
+  stateSpec ctx _ = certStateSpec (lit ctx)
 
   signalSpec _ = conwayDelegCertSpec
 

diff --git a/...ano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/ExecSpecRule/Conway/GovCert.hs b/...ano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/ExecSpecRule/Conway/GovCert.hs
@@ -20,6 +20,7 @@ import Cardano.Ledger.Coin (Coin)
 import Cardano.Ledger.Conway
 import Cardano.Ledger.Conway.TxCert
 import Cardano.Ledger.Crypto (StandardCrypto)
+import Constrained (lit)
 import Data.Bifunctor (Bifunctor (..))
 import qualified Data.List.NonEmpty as NE
 import Data.Map.Strict (Map)
@@ -39,7 +40,7 @@ instance
 
   environmentSpec _ctx = govCertEnvSpec
 
-  stateSpec _ctx _env = certStateSpec
+  stateSpec ctx _env = certStateSpec (lit $ ccecDelegatees ctx)
 
   signalSpec _ctx = govCertSpec
 

diff --git a/...ardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/ExecSpecRule/Conway/Utxo.hs b/...ardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/ExecSpecRule/Conway/Utxo.hs
@@ -32,6 +32,7 @@ import Test.Cardano.Ledger.Conformance (
   computationResultToEither,
   runSpecTransM,
  )
+import Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Base (externalFunctions)
 import Test.Cardano.Ledger.Conformance.SpecTranslate.Conway.Cert ()
 import Test.Cardano.Ledger.Conformance.SpecTranslate.Conway.Utxo ()
 import Test.Cardano.Ledger.Constrained.Conway (
@@ -97,15 +98,15 @@ instance
   runAgdaRule env st sig =
     first (\e -> OpaqueErrorString (T.unpack e) NE.:| [])
       . computationResultToEither
-      $ Agda.utxoStep env st sig
+      $ 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
+            Agda.utxoDebug externalFunctions
               <$> toSpecRep env
               <*> toSpecRep st
               <*> toSpecRep sig

diff --git a/...rdano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/ExecSpecRule/Conway/Utxow.hs b/...rdano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/ExecSpecRule/Conway/Utxow.hs
@@ -12,30 +12,23 @@
 
 module Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Utxow () where
 
-import Cardano.Crypto.DSIGN.Class (SignedDSIGN (..), verifySignedDSIGN)
-import Cardano.Crypto.Hash (ByteString, Hash)
 import Cardano.Ledger.Conway (Conway, ConwayEra)
 import Cardano.Ledger.Conway.TxCert (ConwayTxCert)
-import Cardano.Ledger.Crypto (Crypto (..), StandardCrypto)
-import Cardano.Ledger.Keys (VKey (..))
+import Cardano.Ledger.Crypto (StandardCrypto)
 import Data.Bifunctor (Bifunctor (..))
-import Data.Either (isRight)
 import qualified Data.List.NonEmpty as NE
-import Data.Maybe (fromMaybe)
 import qualified Data.Text as T
 import qualified Lib as Agda
 import Test.Cardano.Ledger.Conformance (
   ExecSpecRule (..),
   OpaqueErrorString (..),
   SpecTranslate,
   computationResultToEither,
-  integerToHash,
  )
+import Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Base (externalFunctions)
 import Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Utxo (genUtxoExecContext)
 import Test.Cardano.Ledger.Conformance.SpecTranslate.Conway.Base (
   ConwayTxBodyTransContext,
-  signatureFromInteger,
-  vkeyFromInteger,
  )
 import Test.Cardano.Ledger.Conformance.SpecTranslate.Conway.Utxow ()
 import Test.Cardano.Ledger.Constrained.Conway (
@@ -46,33 +39,6 @@ import Test.Cardano.Ledger.Constrained.Conway (
   utxoTxSpec,
  )
 
-externalFunctions :: Agda.ExternalFunctions
-externalFunctions = Agda.MkExternalFunctions {..}
-  where
-    extIsSigned vk ser sig =
-      isRight $
-        verifySignedDSIGN
-          @(DSIGN StandardCrypto)
-          @(Hash (HASH StandardCrypto) ByteString)
-          ()
-          vkey
-          hash
-          signature
-      where
-        vkey =
-          unVKey @_ @StandardCrypto
-            . fromMaybe (error "Failed to convert an Agda VKey to a Haskell VKey")
-            $ vkeyFromInteger vk
-        hash =
-          fromMaybe
-            (error $ "Failed to get hash from integer:\n" <> show ser)
-            $ integerToHash ser
-        signature =
-          SignedDSIGN
-            . fromMaybe
-              (error "Failed to decode the signature")
-            $ signatureFromInteger sig
-
 instance
   ( IsConwayUniv fn
   , SpecTranslate (ConwayTxBodyTransContext StandardCrypto) (ConwayTxCert (ConwayEra StandardCrypto))