Added utxowDebug

IntersectMBO · Nov 18, 2024 · 0d0bc2a · 0d0bc2a
1 parent f93035b
commit 0d0bc2a
Show file tree

Hide file tree

Showing 3 changed files with 28 additions and 7 deletions.
diff --git a/src/Ledger/Conway/Foreign/HSLedger/Utxo.agda b/src/Ledger/Conway/Foreign/HSLedger/Utxo.agda
@@ -14,8 +14,9 @@ open import Ledger.Conway.Foreign.HSLedger.Transaction
 
 open import Foreign.Haskell.Coerce
 
-open import Ledger.Conway.Foreign.HSLedger.BaseTypes
+open import Ledger.Conway.Foreign.HSLedger.BaseTypes hiding (TxWitnesses)
 open import Ledger.Conway.Conformance.Utxo DummyTransactionStructure DummyAbstractFunctions
+open import Ledger.Conway.Conformance.Utxow DummyTransactionStructure DummyAbstractFunctions
 
 instance
   HsTy-UTxOEnv = autoHsType UTxOEnv ⊣ withConstructor "MkUTxOEnv"
@@ -38,11 +39,6 @@ module _ (ext : ExternalFunctions) where
   utxo-step = to (coerce ⦃ TrustMe ⦄ $ compute Computational-UTXO)
 
   {-# COMPILE GHC utxo-step as utxoStep #-}
-
-  utxow-step : HsType (UTxOEnv → UTxOState → Tx → ComputationResult String UTxOState)
-  utxow-step = to (coerce ⦃ TrustMe ⦄ $ compute Computational-UTXOW)
-
-  {-# COMPILE GHC utxow-step as utxowStep #-}
 
   utxo-debug : HsType (UTxOEnv → UTxOState → Tx → String)
   utxo-debug env st tx =
@@ -66,3 +62,26 @@ module _ (ext : ExternalFunctions) where
           []
 
   {-# COMPILE GHC utxo-debug as utxoDebug #-}
+
+  utxow-step : HsType (UTxOEnv → UTxOState → Tx → ComputationResult String UTxOState)
+  utxow-step = to (coerce ⦃ TrustMe ⦄ $ compute Computational-UTXOW)
+
+  {-# COMPILE GHC utxow-step as utxowStep #-}
+
+  utxow-debug : HsType (UTxOEnv → UTxOState → Tx → String)
+  utxow-debug env st tx =
+    let open Tx (from tx)
+        open TxBody body
+        open UTxOState (from st)
+        open UTxOEnv (from env)
+        open TxWitnesses (coerce ⦃ TrustMe ⦄ wits)
+     in unlines
+       $ "witsVKeyNeeded utxo txb = "
+       ∷ show (witsVKeyNeeded utxo body)
+       ∷ "\nwitsKeyHashes = "
+       ∷ show (mapˢ hash (dom vkSigs))
+       --∷ "\ncredsNeeded = "
+       --∷ show (credsNeeded utxo body)
+       ∷ []
+
+  {-# COMPILE GHC utxow-debug as utxowDebug #-}
diff --git a/src/Ledger/ScriptValidation.agda b/src/Ledger/ScriptValidation.agda
@@ -16,6 +16,7 @@ module Ledger.ScriptValidation
   where
 
 open import Ledger.Certs govStructure
+open import Tactic.Derive.Show
 
 instance
   _ = DecEq-Slot

diff --git a/src/Ledger/hs-src/Lib.hs b/src/Ledger/hs-src/Lib.hs
@@ -35,7 +35,8 @@ import MAlonzo.Code.Ledger.Conway.Foreign.HSLedger.NewEpoch    as X
 import MAlonzo.Code.Ledger.Conway.Foreign.HSLedger.Ratify      as X
   (StakeDistrs(..), RatifyEnv(..), RatifyState(..), ratifyStep, ratifyDebug)
 import MAlonzo.Code.Ledger.Conway.Foreign.HSLedger.Utxo        as X
-  (UTxOEnv(..), UTxOState(..), UTxO, utxoStep, utxowStep, Redeemer, utxoDebug)
+  ( UTxOEnv(..), UTxOState(..), UTxO, utxoStep, utxowStep, Redeemer
+  , utxoDebug, utxowDebug)
 import MAlonzo.Code.Ledger.Conway.Foreign.HSLedger.BaseTypes   as X
   (Coin, ExUnits, Epoch)
 import MAlonzo.Code.Ledger.Conway.Foreign.ExternalFunctions    as X