No extra redeemers

alonzo/formal-spec/utxo.tex

@@ -120,6 +120,9 @@ \subsection{Combining Scripts with Their Inputs}
   and $\Nothing$ if no associated data is found.
   It uses the script purpose to generate the $\RdmrPtr$ key,
   then find the corresponding entry in the redeemer structure.
+  \item $\fun{rdptr}$ builds a redeemer pointer from a script purpose by
+  setting the tag according to the type of the script purpose, and the index
+  according to the placement of script purpose inside its container (ie. by using $\fun{indexof}$)
 \end{itemize}
 
 
@@ -164,12 +167,14 @@ \subsection{Combining Scripts with Their Inputs}
     &\fun{indexedRdmrs} \in \Tx \to \ScriptPurpose \to (\Redeemer~\times~\ExUnits)^?\\
     &\fun{indexedRdmrs}~tx~sp =
       \begin{cases}
-        (d, \var{eu}) & \var{rdptr} \mapsto (\var{d}, \var{eu}) \in \fun{txrdmrs}~(\fun{txwits}~{tx}) \} \\
+        (d, \var{eu}) & (\fun{rdptr}~txb~sp)~ \mapsto (\var{d}, \var{eu}) \in \fun{txrdmrs}~(\fun{txwits}~{tx}) \} \\
         \Nothing & \text{otherwise}
       \end{cases} \\
     & ~~\where \\
-    & ~~\quad \var{txb} = \txbody{tx} \\
-    & ~~\quad \var{rdptr} = \begin{cases}
+    & ~~\quad \var{txb} = \txbody{tx}
+    \nextdef
+    &\fun{rdptr} ~\in~\TxBody~\to~\ScriptPurpose~ \to~ \RdmrPtr \\
+    &\fun{rdptr}~txb~sp~ =~ \begin{cases}
         (\mathsf{Cert},\fun{indexof}~\var{sp}~(\fun{txcerts}~{txb}))   & \var{sp}~\in~\DCert \\
         (\mathsf{Rewrd},\fun{indexof}~\var{sp}~(\fun{txwdrls}~{txb}))   & \var{sp}~\in~\AddrRWD \\
         (\mathsf{Mint},\fun{indexof}~\var{sp}~(\dom~(\fun{mint}~{txb})))    & \var{sp}~\in~\PolicyID \\
@@ -796,8 +801,8 @@ \subsection{Witnessing}
     & \where \\
     & ~~~~~~~ \var{txb}~=~\txbody{tx}
     \nextdef
-    & \hspace{-1cm}\fun{checkScriptData} \in \Tx \to \UTxO \to (\ScriptPurpose \times \ScriptHash) \to \Bool \\
-    & \hspace{-1cm}\fun{checkScriptData}~\var{tx}~\var{utxo}~(\var{sp},\var{h})~=~ \forall s, (h\mapsto s) \in \fun{txscripts}~(\fun{txwits}~tx),\\
+    & \hspace{-1cm}\fun{checkScriptData} \in \Tx \to (\ScriptPurpose \times \ScriptHash) \to \Bool \\
+    & \hspace{-1cm}\fun{checkScriptData}~\var{tx}~(\var{sp},\var{h})~=~ \forall s, (h\mapsto s) \in \fun{txscripts}~(\fun{txwits}~tx),\\
     & (s \in \ScriptPhTwo~\Rightarrow \fun{txrdmrs}~tx~sp \neq \{\}) \\
     \nextdef
     & \hspace{-1cm}\fun{languages} \in \TxWitness \to \powerset{\Language} \\
@@ -833,10 +838,10 @@ \subsection{Witnessing}
     \item For every item that needs to be validated by a phase-2 script, the transaction contains
       an entry in the indexed redeemer structure (ie. the execution units and redeemer for it are specified);
 
-    \item The size of the set containing script purposes for all phase-2 scripts is the
-    same as the size of the indexed redeemer structure. Combined with the check above,
-    this ensures that there are no additional entries present in the indexed redeemer structure 
-    (ie. those that are not associated with a specific script purpose);
+    \item Each redeemer pointer in the indexed redeemer structure corresponds to
+    a pointer constructed using $\fun{rdptr}$ from some script purpose of the transaction.
+    This ensures that there are no additional entries present in the structure
+    (ie. those that are not required for validation of any script);
 
     \item The signatures of the keys whose hashes are specified in the
     $\fun{reqSignerHashes}$ field in a transaction
@@ -880,9 +885,9 @@ \subsection{Witnessing}
       \hldiff{\var{inputHashes} \subseteq \dom (\fun{txdats}~{txw})} \\~\\
       \hldiff{\dom (\fun{txdats}~{txw}) \subseteq \var{inputHashes} \cup \{h~\mid~ (\wcard, \wcard, h)\in\fun{txouts}\}}
       \\~\\
-      \hldiff{\forall sph \in \fun{scriptsNeeded}~\var{utxo}~\var{tx},~ \fun{checkScriptData}~tx~utxo~sph} \\
-      \hldiff{\|\{ (sp, h)~ \in~ \fun{scriptsNeeded}~\var{utxo}~\var{tx} ~\vert~h\mapsto s~\in~ \fun{txscripts}~{txw},~
-      \var{s} \in \ScriptPhTwo \}\|~=~\|\fun{txrdmrs}~tx\|}
+      \hldiff{\forall sph \in \fun{scriptsNeeded}~\var{utxo}~\var{tx},~ \fun{checkScriptData}~tx~sph} \\
+      \hldiff{\ \forall~(\var{ptr}\mapsto \wcard)~\in~\fun{txrdmrs}~tx, ~ \var{ptr}~\in~\{~\fun{rdptr}~txb~sp~
+       \vert~ (sp,\wcard)~\in~\fun{scriptsNeeded}~\var{utxo}~\var{tx}~\} }
       \\~\\
       \forall \var{vk} \mapsto \sigma \in \txwitsVKey{txw},
       \mathcal{V}_{\var{vk}}{\serialised{txbodyHash}}_{\sigma} \\

alonzo/impl/src/Cardano/Ledger/Alonzo/PlutusScriptApi.hs

@@ -247,10 +247,9 @@ checkScriptData ::
     HasField "certs" (Core.TxBody era) (StrictSeq (DCert (Crypto era)))
   ) =>
   ValidatedTx era ->
-  -- UTxO era ->   -- TODO check that we really don't use the UTxO
   (ScriptPurpose (Crypto era), ScriptHash (Crypto era)) ->
   Bool
-checkScriptData tx {- utxo -} (sp, h) =
+checkScriptData tx (sp, h) =
   case Map.lookup h (txscripts' (getField @"wits" tx)) of
     Nothing -> False
     Just s -> if isNativeScript @era s then True else isJust (indexedRdmrs tx sp)

alonzo/impl/src/Cardano/Ledger/Alonzo/Rules/Utxow.hs

@@ -31,9 +31,15 @@ import Cardano.Ledger.Alonzo.Tx
     ValidatedTx (..),
     hashWitnessPPData,
     isTwoPhaseScriptAddress,
+    rdptr,
   )
 import Cardano.Ledger.Alonzo.TxBody (WitnessPPDataHash)
-import Cardano.Ledger.Alonzo.TxWitness (TxWitness (..), unTxDats)
+import Cardano.Ledger.Alonzo.TxWitness
+  ( RdmrPtr,
+    TxWitness (..),
+    unRedeemers,
+    unTxDats,
+  )
 import Cardano.Ledger.BaseTypes
   ( ShelleyBase,
     StrictMaybe (..),
@@ -108,6 +114,7 @@ data AlonzoPredFail era
       -- ^ Computed from the current Protocol Parameters
   | MissingRequiredSigners (Set (KeyHash 'Witness (Crypto era)))
   | UnspendableUTxONoDatumHash (Set (TxIn (Crypto era)))
+  | ExtraRedeemers ![RdmrPtr]
   deriving (Generic)
 
 deriving instance
@@ -157,6 +164,7 @@ encodePredFail (NonOutputSupplimentaryDatums x y) = Sum NonOutputSupplimentaryDa
 encodePredFail (PPViewHashesDontMatch x y) = Sum PPViewHashesDontMatch 4 !> To x !> To y
 encodePredFail (MissingRequiredSigners x) = Sum MissingRequiredSigners 5 !> To x
 encodePredFail (UnspendableUTxONoDatumHash x) = Sum UnspendableUTxONoDatumHash 6 !> To x
+encodePredFail (ExtraRedeemers x) = Sum ExtraRedeemers 7 !> To x
 
 instance
   ( Era era,
@@ -183,6 +191,7 @@ decodePredFail 3 = SumD NonOutputSupplimentaryDatums <! From <! From
 decodePredFail 4 = SumD PPViewHashesDontMatch <! From <! From
 decodePredFail 5 = SumD MissingRequiredSigners <! From
 decodePredFail 6 = SumD UnspendableUTxONoDatumHash <! From
+decodePredFail 7 = SumD ExtraRedeemers <! From
 decodePredFail n = Invalid n
 
 -- =============================================
@@ -301,7 +310,14 @@ alonzoStyleWitness = do
          in seq (rnf ans) ans
   null unredeemed ?! UnRedeemableScripts unredeemed
 
-  {-  THIS DOES NOT APPPEAR IN THE SPEC  -}
+  {-  || { (sp, h) ∈ \fun{scriptsNeeded} utxo tx | h\mapsto s ∈ txscripts txw, s ∈ ScriptPhTwo } || = || fun{txrdmrs} tx ||  -}
+  let rdptrs = Set.fromList [el | (sp, _) <- sphs, SJust el <- [rdptr @era txbody sp]]
+      extraRdmrs :: [RdmrPtr]
+      extraRdmrs = Map.keys $ Map.withoutKeys (unRedeemers $ txrdmrs $ wits tx) rdptrs
+  null extraRdmrs ?! ExtraRedeemers extraRdmrs
+
+  {-  THIS DOES NOT APPPEAR IN THE SPEC as a separate check, but
+      witsVKeyNeeded includes the reqSignerHashes in the union   -}
   let reqSignerHashes' = getField @"reqSignerHashes" txbody
   eval (reqSignerHashes' ⊆ witsKeyHashes)
     ?!# MissingRequiredSigners (eval $ reqSignerHashes' ➖ witsKeyHashes)

alonzo/impl/src/Cardano/Ledger/Alonzo/TxWitness.hs

@@ -103,6 +103,13 @@ data RdmrPtr
 
 instance NoThunks RdmrPtr
 
+-- ToCBOR and FromCBOR for RdmrPtr is used in UTXOW for error reporting
+instance FromCBOR RdmrPtr where
+  fromCBOR = RdmrPtr <$> fromCBOR <*> fromCBOR
+
+instance ToCBOR RdmrPtr where
+  toCBOR (RdmrPtr t w) = toCBOR t <> toCBOR w
+
 instance ToCBORGroup RdmrPtr where
   listLen _ = 2
   listLenBound _ = 2

cardano-ledger-test/src/Test/Cardano/Ledger/Examples/TwoPhaseValidation.hs

@@ -47,7 +47,7 @@ import Cardano.Ledger.Alonzo.Tx
     hashWitnessPPData,
   )
 import Cardano.Ledger.Alonzo.TxInfo (txInfo, valContext)
-import Cardano.Ledger.Alonzo.TxWitness (RdmrPtr (..), Redeemers (..), TxDats (..))
+import Cardano.Ledger.Alonzo.TxWitness (RdmrPtr (..), Redeemers (..), TxDats (..), unRedeemers)
 import Cardano.Ledger.BaseTypes (Network (..), Seed, StrictMaybe (..), textToUrl)
 import Cardano.Ledger.Coin (Coin (..))
 import Cardano.Ledger.Core (EraRule)
@@ -334,6 +334,43 @@ validatingRedeemersEx1 =
   Redeemers $
     Map.singleton (RdmrPtr Tag.Spend 0) (redeemerExample1, ExUnits 5000 5000)
 
+extraRedeemersEx :: Era era => Redeemers era
+extraRedeemersEx =
+  Redeemers $
+    Map.insert (RdmrPtr Tag.Spend 7) (redeemerExample1, ExUnits 432 444) (unRedeemers validatingRedeemersEx1)
+
+extraRedeemersBody :: Scriptic era => Proof era -> Core.TxBody era
+extraRedeemersBody pf =
+  newTxBody
+    Override
+    pf
+    [ Inputs [TxIn genesisId 1],
+      Collateral [TxIn genesisId 11],
+      Outputs [outEx1 pf],
+      Txfee (Coin 5),
+      WppHash (newWppHash pf (pp pf) [PlutusV1] extraRedeemersEx txDatsExample1)
+    ]
+
+extraRedeemersTx ::
+  forall era.
+  ( Scriptic era,
+    SignBody era
+  ) =>
+  Proof era ->
+  Core.Tx era
+extraRedeemersTx pf =
+  newTx
+    Override
+    pf
+    [ Body (extraRedeemersBody pf),
+      Witnesses'
+        [ AddrWits [makeWitnessVKey (hashAnnotated (validatingBody pf)) (someKeys pf)],
+          ScriptWits [always 3 pf],
+          DataWits [datumExample1],
+          RdmrWits extraRedeemersEx
+        ]
+    ]
+
 outEx1 :: Scriptic era => Proof era -> Core.TxOut era
 outEx1 pf = newTxOut Override pf [Address (someAddr pf), Amount (inject $ Coin 4995)]
 
@@ -1573,6 +1610,8 @@ alonzoUTXOWexamples =
                       . UtxosFailure
                       . CollectErrors
                       $ [NoRedeemer (Spending (TxIn genesisId 1))],
+                    -- now "wrong redeemer label" means there are both unredeemable scripts and extra redeemers
+                    ExtraRedeemers [RdmrPtr Tag.Mint 0],
                     UnRedeemableScripts
                       [ ( Spending (TxIn genesisId 1),
                           (alwaysSucceedsHash 3 pf)
@@ -1658,6 +1697,14 @@ alonzoUTXOWexamples =
                       (Set.singleton $ hashData @A totallyIrrelevantDatum)
                       mempty
                   ]
+              ),
+          testCase "unacceptable extra redeemer" $
+            testUTXOW
+              (trustMe True $ extraRedeemersTx pf)
+              ( Left
+                  [ ExtraRedeemers
+                      [RdmrPtr Tag.Spend 7]
+                  ]
               )
         ]
     ]