From 46e60fdd83b8e29133f03047f9aea688025aabf7 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Joosep=20J=C3=A4=C3=A4ger?= <joosep.jaager@iohk.io>
Date: Mon, 16 Dec 2024 15:40:53 +0200
Subject: [PATCH] Added witnessing for collateral

---
 CHANGELOG.md                                 |  2 ++
 src/Ledger/Certs.lagda                       | 12 +++++++++++-
 src/Ledger/Conway/Foreign/HSLedger/Core.agda |  7 ++++---
 src/Ledger/Conway/Foreign/HSLedger/Utxo.agda | 13 ++++++++++++-
 src/Ledger/Utxow.lagda                       |  2 +-
 5 files changed, 30 insertions(+), 6 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 1540aadd9..65104a1e7 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -4,6 +4,8 @@
 
 ### WIP
 
+- Require witnessing of `reg` credential if the deposit is non-zero
+- Add witnessing of collaterals
 - Rename `ccTermLimit` to `ccMaxTermLength`
 - Add `Vote` and `Propose` script purposes
 - Well-formed parameter updates can't be empty
diff --git a/src/Ledger/Certs.lagda b/src/Ledger/Certs.lagda
index c1eacb640..a5c68d3a8 100644
--- a/src/Ledger/Certs.lagda
+++ b/src/Ledger/Certs.lagda
@@ -57,6 +57,11 @@ data DCert : Type where
   ccreghot    : Credential → Maybe Credential → DCert
 \end{code}
 \begin{code}[hide]
+  -- The `reg` cert is deprecated in Conway, but it's still present in this era 
+  -- for backwards compatibility. This has been added to the spec to make 
+  -- conformance testing work properly. We don't talk about this certificate
+  -- in the pdf because it has been deprecated and we want to discourage people 
+  -- from using it.
   reg         : Credential → Coin → DCert
 \end{code}
 \begin{NoConway}
@@ -71,7 +76,12 @@ cwitness (deregdrep c _)     = just c
 cwitness (ccreghot c _)      = just c
 \end{code}
 \begin{code}[hide]
-cwitness (reg _ _)           = nothing
+-- The implementation requires the `reg` cert to be witnessed only if the 
+-- deposit is set. There didn't use to be a field for the deposit, but that was 
+-- added in the Conway era to make it easier to determine, just by looking at 
+-- the transaction, how much deposit was paid for that certificate. 
+cwitness (reg _ zero)        = nothing
+cwitness (reg c (suc _))     = just c
 \end{code}
 \end{NoConway}
 \end{AgdaMultiCode}
diff --git a/src/Ledger/Conway/Foreign/HSLedger/Core.agda b/src/Ledger/Conway/Foreign/HSLedger/Core.agda
index 81ddf4d22..319df2cf5 100644
--- a/src/Ledger/Conway/Foreign/HSLedger/Core.agda
+++ b/src/Ledger/Conway/Foreign/HSLedger/Core.agda
@@ -1,5 +1,3 @@
-open import Ledger.Conway.Foreign.ExternalFunctions
-
 module Ledger.Conway.Foreign.HSLedger.Core where
 
 open import Ledger.Prelude hiding (ε) renaming (fromList to fromListˢ) public
@@ -81,7 +79,7 @@ module Implementation where
   toData : ∀ {A : Type} → A → Data
   toData _ = 0
 
-  PlutusScript = ⊤
+  PlutusScript = ℕ × ⊤
   ExUnits      = ℕ × ℕ
   ExUnit-CommutativeMonoid = CommutativeMonoid 0ℓ 0ℓ ExUnits ∋ (Conversion.fromBundle record
     { Carrier = ExUnits
@@ -96,6 +94,9 @@ module Implementation where
   instance
     Show-ExUnits : Show ExUnits
     Show-ExUnits = Show-×
+    
+    Hashable-PlutusScript : Hashable PlutusScript ℕ
+    Hashable-PlutusScript .hash (h , _) = h
 
   CostModel    = ⊤
   Language     = ⊤
diff --git a/src/Ledger/Conway/Foreign/HSLedger/Utxo.agda b/src/Ledger/Conway/Foreign/HSLedger/Utxo.agda
index 6f036773f..d695f2ce5 100644
--- a/src/Ledger/Conway/Foreign/HSLedger/Utxo.agda
+++ b/src/Ledger/Conway/Foreign/HSLedger/Utxo.agda
@@ -14,7 +14,7 @@ open import Ledger.Conway.Foreign.HSLedger.Transaction
 
 open import Foreign.Haskell.Coerce
 
-open import Ledger.Conway.Foreign.HSLedger.BaseTypes hiding (TxWitnesses)
+open import Ledger.Conway.Foreign.HSLedger.BaseTypes hiding (TxWitnesses; refScripts)
 open import Ledger.Conway.Conformance.Utxo DummyTransactionStructure DummyAbstractFunctions
 open import Ledger.Conway.Conformance.Utxow DummyTransactionStructure DummyAbstractFunctions
   renaming (module L to LW)
@@ -76,11 +76,22 @@ module _ (ext : ExternalFunctions) where
         open UTxOState (from st)
         open UTxOEnv (from env)
         open TxWitnesses (coerce ⦃ TrustMe ⦄ wits)
+        neededHashes = LW.scriptsNeeded utxo body
+        refScriptHashes = mapˢ 
+          hash 
+          (refScripts (coerce ⦃ TrustMe ⦄ (from tx)) (coerce ⦃ TrustMe ⦄ utxo))
+        witsScriptHashes  = mapˢ hash scripts
      in unlines
        $ "witsVKeyNeeded utxo txb = "
        ∷ show (LW.witsVKeyNeeded utxo body)
        ∷ "\nwitsKeyHashes = "
        ∷ show (mapˢ hash (dom vkSigs))
+       ∷ "\nneededHashes = "
+       ∷ show neededHashes
+       ∷ "\nrefScriptHashes = "
+       ∷ show refScriptHashes
+       ∷ "\nwitsScriptHashes = "
+       ∷ show witsScriptHashes
        ∷ []
 
   {-# COMPILE GHC utxow-debug as utxowDebug #-}
diff --git a/src/Ledger/Utxow.lagda b/src/Ledger/Utxow.lagda
index 6bad8ce4f..350f0df0a 100644
--- a/src/Ledger/Utxow.lagda
+++ b/src/Ledger/Utxow.lagda
@@ -99,7 +99,7 @@ getScripts = mapPartial isScriptObj
 
 credsNeeded : UTxO → TxBody → ℙ (ScriptPurpose × Credential)
 credsNeeded utxo txb
-  =  mapˢ (λ (i , o)  → (Spend  i , payCred (proj₁ o))) ((utxo ∣ txins) ˢ)
+  =  mapˢ (λ (i , o)  → (Spend  i , payCred (proj₁ o))) ((utxo ∣ (txins ∪ collateral)) ˢ)
   ∪  mapˢ (λ a        → (Rwrd   a , stake a)) (dom (txwdrls .proj₁))
   ∪  mapPartial (λ c  → (Cert   c ,_) <$> cwitness c) (fromList txcerts)
   ∪  mapˢ (λ x        → (Mint   x , ScriptObj x)) (policies mint)