Added witnessing for collateral

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

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}

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     = ⊤

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 #-}

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)