Included the hash in plutus script translation

IntersectMBO · Dec 18, 2024 · 9b90011 · 9b90011
1 parent 65ef348
commit 9b90011
Show file tree

Hide file tree

Showing 6 changed files with 33 additions and 9 deletions.
diff --git a/cabal.project b/cabal.project
@@ -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

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
@@ -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 (
@@ -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
@@ -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"

diff --git a/libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/Orphans.hs b/libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/Orphans.hs
@@ -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)
 

diff --git a/...rdano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/SpecTranslate/Conway/Base.hs b/...rdano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/SpecTranslate/Conway/Base.hs
@@ -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

diff --git a/libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/Utils.hs b/libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/Utils.hs
@@ -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
 

diff --git a/libs/cardano-ledger-conformance/test/Test/Cardano/Ledger/Conformance/Imp.hs b/libs/cardano-ledger-conformance/test/Test/Cardano/Ledger/Conformance/Imp.hs
@@ -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