Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

redeemers check mistake #2393

Merged
merged 1 commit into from
Aug 4, 2021
Merged

redeemers check mistake #2393

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
26 changes: 11 additions & 15 deletions alonzo/formal-spec/utxo.tex
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -765,10 +765,6 @@ \subsection{Witnessing}
paired with the hashes of corresponding the witnessing scripts.
This function collects hashes of both phase-1 and phase-2 scripts.

\item $\fun{checkScriptData}$ returns $\True$ if, for the given script purpose,
whenever the script it points to is phase-2, the transaction contains an associated entry
in the indexed redeemers structure.

\item $\fun{languages}$ returns the set of (phase-2) script languages
of all the scripts included in the transaction
\end{itemize}
Expand Down Expand Up @@ -801,10 +797,6 @@ \subsection{Witnessing}
& \where \\
& ~~~~~~~ \var{txb}~=~\txbody{tx}
\nextdef
& \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} \\
& \hspace{-1cm}\fun{languages}~\var{txw}~=~
\{\fun{language}~s \mid s \in \range (\fun{txscripts}~{txw}) \cap \ScriptPhTwo\}
Expand Down Expand Up @@ -835,11 +827,15 @@ \subsection{Witnessing}
the use of subset equality. No additional
datums are permitted.

\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 For every item that needs to be validated by a phase-2 script, and that
phase-2 script is present, the transaction contains
an entry in the indexed redeemer structure (ie. the execution units and redeemer for it are specified).
Note here that if the full script is not present, we cannot tell from the hash
that the script is phase-2, and therefore requires a redeemer;

\item Each redeemer pointer in the indexed redeemer structure corresponds to
a pointer constructed using $\fun{rdptr}$ from some script purpose of the transaction.
a pointer constructed using $\fun{rdptr}$ from some script purpose of a phase-2
script 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);

Expand Down Expand Up @@ -881,13 +877,13 @@ \subsection{Witnessing}
\hldiff{\var{inputHashes}\leteq \{ h \mid (\_ \mapsto (a, \_, h)) \in \txins{txb} \restrictdom \var{utxo}, \fun{isTwoPhaseScriptAddress}~{tx}~{a}\}} \\~\\
\hldiff{\forall \var{s} \in \range (\fun{txscripts}~{txw}) \cap \ScriptPhOne,
\fun{validateScript}~\var{s}~\var{tx}}\\~\\
\hldiff{\{ s \mid (\_, s) \in \fun{scriptsNeeded}~\var{utxo}~\var{tx}\} = \dom (\fun{txscripts}~{txw})} \\~\\
\hldiff{\{ h \mid (\_, h) \in \fun{scriptsNeeded}~\var{utxo}~\var{tx}\} = \dom (\fun{txscripts}~{txw})} \\~\\
\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~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}~\} }
\hldiff{\ \dom (\fun{txrdmrs}~tx) ~=~\{~\fun{rdptr}~txb~sp~
\vert~ (sp,h)~\in~\fun{scriptsNeeded}~\var{utxo}~\var{tx}, } \\
\hldiff{h\mapsto s~\in~\fun{txscripts}~{txw}, s~\in~\ScriptPhTwo \}}
\\~\\
\forall \var{vk} \mapsto \sigma \in \txwitsVKey{txw},
\mathcal{V}_{\var{vk}}{\serialised{txbodyHash}}_{\sigma} \\
Expand Down
49 changes: 27 additions & 22 deletions alonzo/impl/src/Cardano/Ledger/Alonzo/Rules/Utxow.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -18,11 +18,7 @@ import Cardano.Ledger.Address (Addr (..), bootstrapKeyHash, getRwdCred)
import Cardano.Ledger.Alonzo.Data (DataHash)
import Cardano.Ledger.Alonzo.Language (Language (..))
import Cardano.Ledger.Alonzo.PParams (PParams)
import Cardano.Ledger.Alonzo.PlutusScriptApi
( checkScriptData,
language,
scriptsNeeded,
)
import Cardano.Ledger.Alonzo.PlutusScriptApi (language, scriptsNeeded)
import Cardano.Ledger.Alonzo.Rules.Utxo (AlonzoUTXO)
import qualified Cardano.Ledger.Alonzo.Rules.Utxo as Alonzo (UtxoPredicateFailure)
import Cardano.Ledger.Alonzo.Scripts (Script (..))
Expand Down Expand Up @@ -50,7 +46,6 @@ import Cardano.Ledger.Credential (Credential (KeyHashObj))
import Cardano.Ledger.Era (Crypto, Era, ValidateScript (..))
import Cardano.Ledger.Keys (GenDelegs, KeyHash, KeyRole (..), asWitness)
import Cardano.Ledger.Rules.ValidationMode ((?!#))
import Control.DeepSeq (NFData (..))
import Control.Iterate.SetAlgebra (domain, eval, (⊆), (◁), (➖))
import Control.State.Transition.Extended
import Data.Coders
Expand Down Expand Up @@ -100,7 +95,7 @@ import Shelley.Spec.Ledger.UTxO (UTxO (..), txinLookup)
-- failure type of the Shelley Era, as they share some failure modes.
data AlonzoPredFail era
= WrappedShelleyEraFailure !(UtxowPredicateFailure era)
| UnRedeemableScripts ![(ScriptPurpose (Crypto era), ScriptHash (Crypto era))]
| MissingRedeemers ![(ScriptPurpose (Crypto era), ScriptHash (Crypto era))]
| MissingRequiredDatums
!(Set (DataHash (Crypto era))) -- Set of missing data hashes
!(Set (DataHash (Crypto era))) -- Set of received data hashes
Expand Down Expand Up @@ -158,7 +153,7 @@ encodePredFail ::
AlonzoPredFail era ->
Encode 'Open (AlonzoPredFail era)
encodePredFail (WrappedShelleyEraFailure x) = Sum WrappedShelleyEraFailure 0 !> E toCBOR x
encodePredFail (UnRedeemableScripts x) = Sum UnRedeemableScripts 1 !> To x
encodePredFail (MissingRedeemers x) = Sum MissingRedeemers 1 !> To x
encodePredFail (MissingRequiredDatums x y) = Sum MissingRequiredDatums 2 !> To x !> To y
encodePredFail (NonOutputSupplimentaryDatums x y) = Sum NonOutputSupplimentaryDatums 3 !> To x !> To y
encodePredFail (PPViewHashesDontMatch x y) = Sum PPViewHashesDontMatch 4 !> To x !> To y
Expand All @@ -185,7 +180,7 @@ decodePredFail ::
Word ->
Decode 'Open (AlonzoPredFail era)
decodePredFail 0 = SumD WrappedShelleyEraFailure <! D fromCBOR
decodePredFail 1 = SumD UnRedeemableScripts <! From
decodePredFail 1 = SumD MissingRedeemers <! From
decodePredFail 2 = SumD MissingRequiredDatums <! From <! From
decodePredFail 3 = SumD NonOutputSupplimentaryDatums <! From <! From
decodePredFail 4 = SumD PPViewHashesDontMatch <! From <! From
Expand Down Expand Up @@ -301,20 +296,23 @@ alonzoStyleWitness = do
Set.null notOkSupplimentalDHs
?! NonOutputSupplimentaryDatums notOkSupplimentalDHs okSupplimentalDHs

{- ∀ sph ∈ scriptsNeeded utxo tx, checkScriptData tx utxo ph -}
let sphs :: [(ScriptPurpose (Crypto era), ScriptHash (Crypto era))]
sphs = scriptsNeeded utxo tx
unredeemed =
-- A script is unredeemed, is we can't find the Data that it requires to execute.
let ans = (filter (not . checkScriptData tx) sphs)
in seq (rnf ans) ans
null unredeemed ?! UnRedeemableScripts unredeemed

{- || { (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
{- dom (txrdmrs tx) = { rdptr txb sp | (sp, h) ∈ scriptsNeeded utxo tx,
h \mapsto s ∈ txscripts txw, s ∈ Scriptph2} -}
let redeemersNeeded =
[ (rp, (sp, sh))
| (sp, sh) <- scriptsNeeded utxo tx,
SJust rp <- [rdptr @era txbody sp],
Just script <- [Map.lookup sh (getField @"scriptWits" tx)],
(not . isNativeScript @era) script
]
(extraRdmrs, missingRdmrs) =
extSymmetricDifference
(Map.keys $ unRedeemers $ txrdmrs $ wits tx)
id
redeemersNeeded
fst
null extraRdmrs ?! ExtraRedeemers extraRdmrs
null missingRdmrs ?! MissingRedeemers (map snd missingRdmrs)

{- THIS DOES NOT APPPEAR IN THE SPEC as a separate check, but
witsVKeyNeeded includes the reqSignerHashes in the union -}
Expand Down Expand Up @@ -426,6 +424,13 @@ witsVKeyNeeded utxo' tx genDelegs =
)
genDelegs

extSymmetricDifference :: (Ord k) => [a] -> (a -> k) -> [b] -> (b -> k) -> ([a], [b])
extSymmetricDifference as fa bs fb = (extraA, extraB)
where
intersection = (Set.fromList $ map fa as) `Set.intersection` (Set.fromList $ map fb bs)
extraA = filter (\x -> not $ fa x `Set.member` intersection) as
extraB = filter (\x -> not $ fb x `Set.member` intersection) bs

-- ====================================
-- Make the STS instance

Expand Down
2 changes: 1 addition & 1 deletion alonzo/test/lib/Test/Cardano/Ledger/Alonzo/Serialisation/Generators.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -292,7 +292,7 @@ instance Mock c => Arbitrary (AlonzoPredFail (AlonzoEra c)) where
arbitrary =
oneof
[ WrappedShelleyEraFailure <$> arbitrary,
UnRedeemableScripts <$> arbitrary,
MissingRedeemers <$> arbitrary,
MissingRequiredDatums <$> arbitrary <*> arbitrary,
PPViewHashesDontMatch <$> arbitrary <*> arbitrary
]
Expand Down
33 changes: 10 additions & 23 deletions cardano-ledger-test/src/Test/Cardano/Ledger/Examples/TwoPhaseValidation.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -72,7 +72,6 @@ import Cardano.Ledger.Keys
signedDSIGN,
signedKES,
)
import Cardano.Ledger.Mary.Value (PolicyID (..))
import Cardano.Ledger.SafeHash (hashAnnotated)
import Cardano.Ledger.Serialization (ToCBORGroup)
import Cardano.Ledger.ShelleyMA.Timelocks (ValidityInterval (..))
Expand Down Expand Up @@ -1533,7 +1532,7 @@ alonzoUTXOWexamples =
. UtxosFailure
. CollectErrors
$ [NoRedeemer (Spending (TxIn genesisId 1))],
UnRedeemableScripts
MissingRedeemers
[ ( Spending (TxIn genesisId 1),
(alwaysSucceedsHash 3 pf)
)
Expand Down Expand Up @@ -1568,8 +1567,7 @@ alonzoUTXOWexamples =
NoWitness (timelockHash 0 pf)
],
WrappedShelleyEraFailure . MissingScriptWitnessesUTXOW . Set.singleton $
(timelockHash 0 pf),
UnRedeemableScripts [(Spending $ TxIn genesisId 100, timelockHash 0 pf)]
(timelockHash 0 pf)
]
),
testCase "missing 2-phase script witness" $
Expand All @@ -1583,22 +1581,11 @@ alonzoUTXOWexamples =
],
WrappedShelleyEraFailure . MissingScriptWitnessesUTXOW . Set.singleton $
(alwaysSucceedsHash 2 pf),
UnRedeemableScripts
[ ( Rewarding
( RewardAcnt
{ getRwdNetwork = Testnet,
getRwdCred = ScriptHashObj (alwaysSucceedsHash 2 pf)
}
),
(alwaysSucceedsHash 2 pf)
),
( Certifying . DCertDeleg . DeRegKey . ScriptHashObj $
(alwaysSucceedsHash 2 pf),
(alwaysSucceedsHash 2 pf)
),
( Minting (PolicyID {policyID = (alwaysSucceedsHash 2 pf)}),
(alwaysSucceedsHash 2 pf)
)
-- these redeemers are associated with phase-1 scripts
ExtraRedeemers
[ RdmrPtr Tag.Mint 1,
RdmrPtr Tag.Cert 1,
RdmrPtr Tag.Rewrd 0
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

So this predicate failure is happening because the lack of script witness means that we do not know that the script hash is a plutus script, and hence these look superfluous?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

yes, there is no plutus/phase-2 script validating those three things

]
]
),
Expand All @@ -1611,12 +1598,12 @@ alonzoUTXOWexamples =
. 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
MissingRedeemers
[ ( Spending (TxIn genesisId 1),
(alwaysSucceedsHash 3 pf)
)
]
],
ExtraRedeemers [RdmrPtr Tag.Mint 0]
]
),
testCase "missing datum" $
Expand Down