Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Updated SpecTranslate instance of AlonzoScript, debug info improvements #4801

Open
wants to merge 1 commit into
base: master
Choose a base branch
from
Open
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
8 changes: 4 additions & 4 deletions cabal.project
Original file line number Diff line number Diff line change
Expand Up @@ -20,12 +20,12 @@ repository cardano-haskell-packages
-- $ nix-prefetch-git https://github.com/intersectmbo/formal-ledger-specifications --rev <GIT_SHA> | jq .hash
source-repository-package
type: git
location: https://github.com/IntersectMBO/formal-ledger-specifications.git
location: https://github.com/Soupstraw/exec-spec-temporary.git
-- !WARNING!:
-- MAKE SURE THIS POINTS TO A COMMIT IN `MAlonzo-code` BEFORE MERGE!
subdir: generated
--sha256: sha256-by921yC1MaZI58kyrtEGGKqmt9jMnVsPLfQtP4raJPw=
tag: be51adff014214c15fed718d396bb8a6d955f9e1
--subdir: generated
--sha256: sha256-fzjlu3MJ3AsainURwPrvM2ZJLXYCiHnuTLlCWgVzs1c=
tag: 6f00dc6b50617b8d959e9c43cde4ff0b7507817d

-- 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 @@ -14,8 +14,12 @@ module Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Utxow () where

import Cardano.Ledger.Conway (ConwayEra)
import Cardano.Ledger.Conway.TxCert (ConwayTxCert)
import Cardano.Ledger.Conway.UTxO (getConwayWitsVKeyNeeded)
import Cardano.Ledger.Core (EraTx (..))
import Cardano.Ledger.Shelley.LedgerState (UTxOState (..))
import Data.Bifunctor (Bifunctor (..))
import qualified Data.Text as T
import Lens.Micro ((^.))
import qualified Lib as Agda
import qualified Prettyprinter as PP
import Test.Cardano.Ledger.Conformance (
Expand All @@ -41,6 +45,7 @@ import Test.Cardano.Ledger.Constrained.Conway (
)
import qualified Test.Cardano.Ledger.Generic.PrettyCore as PP
import Test.Cardano.Ledger.Shelley.Utils (runSTS)
import Test.Cardano.Ledger.TreeDiff (showExpr)

instance
( IsConwayUniv fn
Expand Down Expand Up @@ -69,6 +74,12 @@ instance
in
PP.vcat
[ "UTXOW"
, "Impl:"
, "witsVKeyNeeded"
, PP.ppString . showExpr $
getConwayWitsVKeyNeeded @ConwayEra (utxosUtxo st) (sig ^. bodyTxL)
, "witsVKeyHashes"
, "Spec:"
, PP.ppString result
, mempty
, "UTXO"
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -149,8 +149,18 @@ instance NFData LEnv
instance ToExpr a => ToExpr (HSSet a)

instance ToExpr Credential where
toExpr (KeyHashObj h) = App "KeyHashObj" [agdaHashToExpr standardHashSize h]
toExpr (ScriptObj h) = App "ScriptObj" [agdaHashToExpr standardHashSize h]
toExpr (KeyHashObj h) =
App
"KeyHashObj"
[ agdaHashToExpr standardAddrHashSize h
, toExpr h
]
toExpr (ScriptObj h) =
App
"ScriptObj"
[ agdaHashToExpr standardAddrHashSize h
, toExpr h
]

instance (ToExpr k, ToExpr v) => ToExpr (HSMap k v)

Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -249,7 +249,7 @@ instance
type SpecRep (AlonzoScript era) = Agda.Script

toSpecRep (TimelockScript s) = Left <$> toSpecRep s
toSpecRep (PlutusScript _) = pure $ Right ()
toSpecRep (PlutusScript s) = Right . (,()) <$> toSpecRep s

instance
( EraTxOut era
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -6,14 +6,17 @@ module Test.Cardano.Ledger.Conformance.Utils where

import Cardano.Crypto.Hash (ByteString, Hash, HashAlgorithm, hashFromBytes, hashToBytes, sizeHash)
import Cardano.Crypto.Util (bytesToNatural, naturalToBytes)
import Cardano.Ledger.Crypto (HASH)
import Cardano.Ledger.Crypto (ADDRHASH, HASH)
import qualified Data.ByteString.Base16 as B16
import Data.Data (Proxy (..))
import Test.Cardano.Ledger.TreeDiff (Expr, ToExpr (..))

standardHashSize :: Int
standardHashSize = fromIntegral . sizeHash $ Proxy @HASH

standardAddrHashSize :: Int
standardAddrHashSize = fromIntegral . sizeHash $ Proxy @ADDRHASH

agdaHashToBytes :: Int -> Integer -> ByteString
agdaHashToBytes hs = B16.encode . naturalToBytes hs . fromInteger

Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -140,4 +140,4 @@ spec =
it "Submit constitution" $ do
_ <- submitConstitution @ConwayEra SNothing
passNEpochs 2
xdescribe "Conway Imp conformance" $ ConwayImp.conwaySpec @ConwayEra
describe "Conway Imp conformance" $ ConwayImp.conwaySpec @ConwayEra
Loading