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

Only evaluate Plutus scripts in static checks. #2767

Merged
merged 1 commit into from
May 4, 2022
Merged

Only evaluate Plutus scripts in static checks. #2767

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
29 changes: 16 additions & 13 deletions eras/alonzo/impl/src/Cardano/Ledger/Alonzo/Rules/Utxos.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -5,6 +5,7 @@
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
Expand All @@ -24,7 +25,7 @@ module Cardano.Ledger.Alonzo.Rules.Utxos
invalidBegin,
invalidEnd,
UtxosEvent (..),
(?!##),
when2Phase,
ConcreteAlonzo,
FailureDescription (..),
scriptFailuresToPredicateFailure,
Expand Down Expand Up @@ -81,6 +82,7 @@ import qualified Data.Compact.SplitMap as SplitMap
import Data.Foldable (toList)
import Data.List (intercalate)
import Data.List.NonEmpty (NonEmpty (..))
import qualified Data.List.NonEmpty as NE
import qualified Data.Map.Strict as Map
import Data.Sequence.Strict (StrictSeq)
import Data.Set (Set)
Expand Down Expand Up @@ -192,10 +194,10 @@ scriptsValidateTransition = do

case collectTwoPhaseScriptInputs ei sysSt pp tx utxo of
Right sLst ->
case evalScripts @era (getField @"_protocolVersion" pp) tx sLst of
when2Phase $ case evalScripts @era (getField @"_protocolVersion" pp) tx sLst of
Fails _ps fs ->
False
?!## ValidationTagMismatch
failBecause $
ValidationTagMismatch
(getField @"isValid" tx)
(FailedUnexpectedly (scriptFailuresToPredicateFailure fs))
Passes ps -> tellEvent (SuccessfulPlutusScriptsEvent ps)
Expand Down Expand Up @@ -229,11 +231,14 @@ scriptsNotValidateTransition = do
case collectTwoPhaseScriptInputs ei sysSt pp tx utxo of
Right sLst ->
whenFailureFree $
case evalScripts @era (getField @"_protocolVersion" pp) tx sLst of
Passes _ps -> False ?!## ValidationTagMismatch (getField @"isValid" tx) PassedUnexpectedly
Fails ps fs -> do
tellEvent (SuccessfulPlutusScriptsEvent ps)
tellEvent (FailedPlutusScriptsEvent (scriptFailuresToPlutusDebug fs))
when2Phase $
case evalScripts @era (getField @"_protocolVersion" pp) tx sLst of
Passes _ps ->
failBecause $
ValidationTagMismatch (getField @"isValid" tx) PassedUnexpectedly
Fails ps fs -> do
tellEvent (SuccessfulPlutusScriptsEvent ps)
tellEvent (FailedPlutusScriptsEvent (scriptFailuresToPlutusDebug fs))
Left info -> failBecause (CollectErrors info)

let !_ = traceEvent invalidEnd ()
Expand Down Expand Up @@ -437,10 +442,8 @@ lbl2Phase = "2phase"
-- | Construct a 2-phase predicate check.
--
-- Note that 2-phase predicate checks are by definition static.
(?!##) :: Bool -> PredicateFailure sts -> Rule sts ctx ()
(?!##) = labeledPred [lblStatic, lbl2Phase]

infix 1 ?!##
when2Phase :: Rule sts ctx () -> Rule sts ctx ()
when2Phase = labeled $ lblStatic NE.:| [lbl2Phase]

Comment on lines +445 to 447
Copy link
Contributor

Choose a reason for hiding this comment

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

How about some comment here, explaining exactly what is going on here, and some discussion about the correct use of this function. One might also explain what NE.:| does. It looks like a constructor function?

Copy link
Collaborator

Choose a reason for hiding this comment

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

@TimSheard It is a type constructor for NonEmpty, it comes from base: https://downloads.haskell.org/~ghc/8.10.7/docs/html/libraries/base-4.14.3.0/Data-List-NonEmpty.html#t:NonEmpty

-- =========================================================
-- Inject instances
Expand Down
21 changes: 11 additions & 10 deletions eras/babbage/impl/src/Cardano/Ledger/Babbage/Rules/Utxos.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -26,7 +26,7 @@ import Cardano.Ledger.Alonzo.Rules.Utxos
scriptFailuresToPredicateFailure,
validBegin,
validEnd,
(?!##),
when2Phase,
)
import qualified Cardano.Ledger.Alonzo.Scripts as Alonzo
import Cardano.Ledger.Alonzo.Tx (IsValid (..))
Expand Down Expand Up @@ -168,13 +168,14 @@ scriptsYes = do
Right sLst ->
{- isValid tx = evalScripts tx sLst = True -}
whenFailureFree $
case evalScripts @era (getField @"_protocolVersion" pp) tx sLst of
Fails _ fs ->
False
?!## ValidationTagMismatch
(getField @"isValid" tx)
(FailedUnexpectedly (scriptFailuresToPredicateFailure fs))
Passes _ -> pure ()
when2Phase $
case evalScripts @era (getField @"_protocolVersion" pp) tx sLst of
Fails _ fs ->
failBecause $
ValidationTagMismatch
(getField @"isValid" tx)
(FailedUnexpectedly (scriptFailuresToPredicateFailure fs))
Passes _ -> pure ()
Left info -> failBecause (CollectErrors info)

let !_ = traceEvent validEnd ()
Expand Down Expand Up @@ -203,8 +204,8 @@ scriptsNo = do
Right sLst ->
{- sLst := collectTwoPhaseScriptInputs pp tx utxo -}
{- isValid tx = evalScripts tx sLst = False -}
case evalScripts @era (getField @"_protocolVersion" pp) tx sLst of
Passes _ -> False ?!## ValidationTagMismatch (getField @"isValid" tx) PassedUnexpectedly
when2Phase $ case evalScripts @era (getField @"_protocolVersion" pp) tx sLst of
Passes _ -> failBecause $ ValidationTagMismatch (getField @"isValid" tx) PassedUnexpectedly
Fails ps fs -> do
tellEvent (SuccessfulPlutusScriptsEvent ps)
tellEvent (FailedPlutusScriptsEvent (scriptFailuresToPlutusDebug fs))
Expand Down
6 changes: 3 additions & 3 deletions libs/cardano-ledger-core/src/Cardano/Ledger/Rules/ValidationMode.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -80,7 +80,7 @@ lblStatic = "static"
-- The choice of '#' as a postfix here is made because often these are crypto
-- checks.
(?!#) :: Bool -> PredicateFailure sts -> Rule sts ctx ()
(?!#) = labeledPred [lblStatic]
(?!#) = labeledPred $ lblStatic NE.:| []

infix 1 ?!#

Expand All @@ -89,7 +89,7 @@ infix 1 ?!#
-- The choice of '#' as a postfix here is made because often these are crypto
-- checks.
(?!#:) :: Either e () -> (e -> PredicateFailure sts) -> Rule sts ctx ()
(?!#:) = labeledPredE [lblStatic]
(?!#:) = labeledPredE $ lblStatic NE.:| []

infix 1 ?!#:

Expand Down Expand Up @@ -130,7 +130,7 @@ runTest :: Inject t (PredicateFailure sts) => Test t -> Rule sts ctx ()
runTest = validateTrans inject

runTestOnSignal :: Inject t (PredicateFailure sts) => Test t -> Rule sts ctx ()
runTestOnSignal = validateTransLabeled inject [lblStatic]
runTestOnSignal = validateTransLabeled inject $ lblStatic NE.:| []

runTestMaybe :: InjectMaybe t (PredicateFailure sts) => Test t -> Rule sts ctx ()
runTestMaybe = validate . mapMaybeValidation injectMaybe
55 changes: 33 additions & 22 deletions libs/small-steps/src/Control/State/Transition/Extended.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -45,6 +45,7 @@ module Control.State.Transition.Extended
SingEP (..),
EventPolicy (..),
EventReturnType,
labeled,
labeledPred,
labeledPredE,
ifFailureFree,
Expand Down Expand Up @@ -314,12 +315,18 @@ data Clause sts (rtype :: RuleType) a where
a ->
Clause sts rtype a
Predicate ::
[Label] ->
Validation (NonEmpty e) a ->
-- Type of failure to return if the predicate fails
(e -> PredicateFailure sts) ->
a ->
Clause sts rtype a
-- | Label part of a rule. The interpreter may be configured to only run parts
-- of rules governed by (or by the lack of) certain labels.
Label ::
NonEmpty Label ->
Rule sts rtype a ->
a ->
Clause sts rtype a
IfFailureFree :: Rule sts rtype a -> Rule sts rtype a -> Clause sts rtype a

deriving instance Functor (Clause sts rtype)
Expand All @@ -341,26 +348,28 @@ validateTrans ::
(e -> PredicateFailure sts) ->
Validation (NonEmpty e) () ->
Rule sts ctx ()
validateTrans t v = liftF $ Predicate [] v t ()
validateTrans t v = liftF $ Predicate v t ()

-- | Same as `validation`, except with ability to translate opaque failures
-- into `PredicateFailure`s with a help of supplied function.
validateTransLabeled ::
-- | Transformation function for all errors
(e -> PredicateFailure sts) ->
-- | Supply a list of labels to be used as filters when STS is executed
[Label] ->
NonEmpty Label ->
-- | Actual validations to be executed
Validation (NonEmpty e) () ->
Rule sts ctx ()
validateTransLabeled t labels v = liftF $ Predicate labels v t ()
validateTransLabeled t labels v = liftF $ Label labels (liftF $ Predicate v t ()) ()

-- | Oh noes!
--
-- This takes a condition (a boolean expression) and a failure and results in
-- a clause which will throw that failure if the condition fails.
(?!) :: Bool -> PredicateFailure sts -> Rule sts ctx ()
(?!) = labeledPred []
(?!) cond onFail =
liftF $
Predicate (if cond then Success () else Failure (() :| [])) (const onFail) ()
Copy link
Collaborator

Choose a reason for hiding this comment

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

Just one minor optional suggestion, which doesn't change the semantics, but might make it easier to read the code:

Suggested change
Predicate (if cond then Success () else Failure (() :| [])) (const onFail) ()
Predicate (if cond then Success () else Failure (onFail :| [])) id ()


infix 1 ?!

Expand All @@ -371,27 +380,27 @@ failBecause = (False ?!)
--
-- We interpret this as "What?" "No!" "Because:"
(?!:) :: Either e () -> (e -> PredicateFailure sts) -> Rule sts ctx ()
(?!:) = labeledPredE []
(?!:) cond onFail =
liftF $
Predicate (eitherToValidation $ first pure cond) onFail ()

-- | Labeled predicate. This may be used to control which predicates are run
-- using 'ValidateSuchThat'.
labeledPred :: [Label] -> Bool -> PredicateFailure sts -> Rule sts ctx ()
labeledPred lbls cond orElse =
liftF $
Predicate
lbls
(if cond then Success () else Failure (() :| []))
(const orElse)
()
labeledPred :: NonEmpty Label -> Bool -> PredicateFailure sts -> Rule sts ctx ()
labeledPred lbls cond orElse = labeled lbls (cond ?! orElse)

-- | Labeled predicate with an explanation
labeledPredE ::
[Label] ->
NonEmpty Label ->
Either e () ->
(e -> PredicateFailure sts) ->
Rule sts ctx ()
labeledPredE lbls cond orElse =
liftF $ Predicate lbls (eitherToValidation $ first pure cond) orElse ()
labeledPredE lbls cond orElse = labeled lbls (cond ?!: orElse)

-- | Labeled clause. This will only be executed if the interpreter is set to
-- execute clauses with this label.
labeled :: NonEmpty Label -> Rule sts ctx () -> Rule sts ctx ()
labeled lbls subrule = liftF $ Label lbls subrule ()

trans ::
Embed sub super => RuleContext rtype sub -> Rule super rtype (State sub)
Expand Down Expand Up @@ -582,11 +591,13 @@ applyRuleInternal ep vp goSTS jc r = do
if failureFree
then foldF runClause yesrule
else foldF runClause norule
runClause (Predicate lbls cond orElse val) =
if validateIf lbls
then case cond of
Success x -> pure x
Failure errs -> modify (first (map orElse (reverse (NE.toList errs)) <>)) >> pure val
runClause (Predicate cond orElse val) =
case cond of
Success x -> pure x
Failure errs -> modify (first (map orElse (reverse (NE.toList errs)) <>)) >> pure val
runClause (Label lbls subrule val) =
if validateIf (NE.toList lbls)
then foldF runClause subrule
else pure val
runClause (SubTrans (subCtx :: RuleContext _rtype sub) next) = do
s <- lift $ goSTS subCtx
Expand Down