{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}

-- | Describes modes under which we might validate certain rules in the ledger.
--
--   What does this mean? Sometimes, we will want to check only certain
--   conditions specified in the rules. For example, when replaying a previously
--   validated chain, we do not care about rerunning _any_ checks, only making
--   the relevant changes to the ledger state.
module Cardano.Ledger.Rules.ValidationMode
  ( -- $static
    lblStatic,
    (?!#),
    (?!#:),
    failBecauseS,
    applySTSNonStatic,
    applySTSValidateSuchThat,

    -- * Interface with validation-selective libarary
    mapMaybeValidation,

    -- * Interface for independent Tests
    Inject (..),
    InjectMaybe (..),
    Test,
    runTest,
    runTestMaybe,
    runTestOnSignal,
  )
where

import Control.State.Transition.Extended
import Data.Bifunctor (first)
import Data.List.NonEmpty (NonEmpty)
import qualified Data.List.NonEmpty as NE
import Data.Maybe (mapMaybe)
import Validation

applySTSValidateSuchThat ::
  forall s m rtype.
  (STS s, RuleTypeRep rtype, m ~ BaseM s) =>
  ([Label] -> Bool) ->
  RuleContext rtype s ->
  m (Either [PredicateFailure s] (State s))
applySTSValidateSuchThat :: ([Label] -> Bool)
-> RuleContext rtype s -> m (Either [PredicateFailure s] (State s))
applySTSValidateSuchThat [Label] -> Bool
cond =
  ApplySTSOpts 'EventPolicyDiscard
-> RuleContext rtype s
-> m (Either
        [PredicateFailure s]
        (EventReturnType 'EventPolicyDiscard s (State s)))
forall s (m :: * -> *) (rtype :: RuleType) (ep :: EventPolicy).
(STS s, RuleTypeRep rtype, m ~ BaseM s) =>
ApplySTSOpts ep
-> RuleContext rtype s
-> m (Either [PredicateFailure s] (EventReturnType ep s (State s)))
applySTSOptsEither ApplySTSOpts 'EventPolicyDiscard
opts
  where
    opts :: ApplySTSOpts 'EventPolicyDiscard
opts =
      ApplySTSOpts :: forall (ep :: EventPolicy).
AssertionPolicy -> ValidationPolicy -> SingEP ep -> ApplySTSOpts ep
ApplySTSOpts
        { asoAssertions :: AssertionPolicy
asoAssertions = AssertionPolicy
AssertionsOff,
          asoValidation :: ValidationPolicy
asoValidation = ([Label] -> Bool) -> ValidationPolicy
ValidateSuchThat [Label] -> Bool
cond,
          asoEvents :: SingEP 'EventPolicyDiscard
asoEvents = SingEP 'EventPolicyDiscard
EPDiscard
        }

--------------------------------------------------------------------------------
-- Static checks
--------------------------------------------------------------------------------

-- * Static checks

--

-- $static
--
-- Static checks are used to indicate that a particular predicate depends only
-- on the signal to the transition, rather than the state or environment. This
-- is particularly relevant where the signal is something such as a transaction,
-- which is fixed, whereas the state and environment depend upon the chain tip
-- upon which we are trying to build a block.

-- | Indicates that this check depends only upon the signal to the transition,
-- not the state or environment.
lblStatic :: Label
lblStatic :: Label
lblStatic = Label
"static"

-- | Construct a static predicate check.
--
--   The choice of '#' as a postfix here is made because often these are crypto
--   checks.
(?!#) :: Bool -> PredicateFailure sts -> Rule sts ctx ()
?!# :: Bool -> PredicateFailure sts -> Rule sts ctx ()
(?!#) = NonEmpty Label -> Bool -> PredicateFailure sts -> Rule sts ctx ()
forall sts (ctx :: RuleType).
NonEmpty Label -> Bool -> PredicateFailure sts -> Rule sts ctx ()
labeledPred (NonEmpty Label -> Bool -> PredicateFailure sts -> Rule sts ctx ())
-> NonEmpty Label
-> Bool
-> PredicateFailure sts
-> Rule sts ctx ()
forall a b. (a -> b) -> a -> b
$ Label
lblStatic Label -> [Label] -> NonEmpty Label
forall a. a -> [a] -> NonEmpty a
NE.:| []

infix 1 ?!#

-- | Construct a static predicate check with an explanation.
--
--   The choice of '#' as a postfix here is made because often these are crypto
--   checks.
(?!#:) :: Either e () -> (e -> PredicateFailure sts) -> Rule sts ctx ()
?!#: :: Either e () -> (e -> PredicateFailure sts) -> Rule sts ctx ()
(?!#:) = NonEmpty Label
-> Either e () -> (e -> PredicateFailure sts) -> Rule sts ctx ()
forall e sts (ctx :: RuleType).
NonEmpty Label
-> Either e () -> (e -> PredicateFailure sts) -> Rule sts ctx ()
labeledPredE (NonEmpty Label
 -> Either e () -> (e -> PredicateFailure sts) -> Rule sts ctx ())
-> NonEmpty Label
-> Either e ()
-> (e -> PredicateFailure sts)
-> Rule sts ctx ()
forall a b. (a -> b) -> a -> b
$ Label
lblStatic Label -> [Label] -> NonEmpty Label
forall a. a -> [a] -> NonEmpty a
NE.:| []

infix 1 ?!#:

-- | Fail, if static checks are enabled.
failBecauseS :: PredicateFailure sts -> Rule sts ctx ()
failBecauseS :: PredicateFailure sts -> Rule sts ctx ()
failBecauseS = (Bool
False Bool -> PredicateFailure sts -> Rule sts ctx ()
forall sts (ctx :: RuleType).
Bool -> PredicateFailure sts -> Rule sts ctx ()
?!#)

-- | Apply an STS system and do not validate any static checks.
applySTSNonStatic ::
  forall s m rtype.
  (STS s, RuleTypeRep rtype, m ~ BaseM s) =>
  RuleContext rtype s ->
  m (Either [PredicateFailure s] (State s))
applySTSNonStatic :: RuleContext rtype s -> m (Either [PredicateFailure s] (State s))
applySTSNonStatic = ([Label] -> Bool)
-> RuleContext rtype s -> m (Either [PredicateFailure s] (State s))
forall s (m :: * -> *) (rtype :: RuleType).
(STS s, RuleTypeRep rtype, m ~ BaseM s) =>
([Label] -> Bool)
-> RuleContext rtype s -> m (Either [PredicateFailure s] (State s))
applySTSValidateSuchThat (Label -> [Label] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
notElem Label
lblStatic)

-- | Helper function to filter out unused failures
mapMaybeValidation ::
  (e -> Maybe e') ->
  Validation (NonEmpty e) () ->
  Validation (NonEmpty e') ()
mapMaybeValidation :: (e -> Maybe e')
-> Validation (NonEmpty e) () -> Validation (NonEmpty e') ()
mapMaybeValidation e -> Maybe e'
toPredicateFailureMaybe =
  Validation (NonEmpty e') ()
-> (NonEmpty e' -> Validation (NonEmpty e') ())
-> Maybe (NonEmpty e')
-> Validation (NonEmpty e') ()
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (() -> Validation (NonEmpty e') ()
forall e a. a -> Validation e a
Success ()) NonEmpty e' -> Validation (NonEmpty e') ()
forall e a. e -> Validation e a
Failure
    (Maybe (NonEmpty e') -> Validation (NonEmpty e') ())
-> (Validation (NonEmpty e) () -> Maybe (NonEmpty e'))
-> Validation (NonEmpty e) ()
-> Validation (NonEmpty e') ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [e'] -> Maybe (NonEmpty e')
forall a. [a] -> Maybe (NonEmpty a)
NE.nonEmpty
    ([e'] -> Maybe (NonEmpty e'))
-> (Validation (NonEmpty e) () -> [e'])
-> Validation (NonEmpty e) ()
-> Maybe (NonEmpty e')
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [e'] -> Validation [e'] () -> [e']
forall e a. e -> Validation e a -> e
fromFailure []
    (Validation [e'] () -> [e'])
-> (Validation (NonEmpty e) () -> Validation [e'] ())
-> Validation (NonEmpty e) ()
-> [e']
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (NonEmpty e -> [e'])
-> Validation (NonEmpty e) () -> Validation [e'] ()
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first ((e -> Maybe e') -> [e] -> [e']
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe e -> Maybe e'
toPredicateFailureMaybe ([e] -> [e']) -> (NonEmpty e -> [e]) -> NonEmpty e -> [e']
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NonEmpty e -> [e]
forall a. NonEmpty a -> [a]
NE.toList)

-- ===========================================================

class Inject t s where
  inject :: t -> s

class InjectMaybe t s where
  injectMaybe :: t -> Maybe s

type Test failure = Validation (NonEmpty failure) ()

runTest :: Inject t (PredicateFailure sts) => Test t -> Rule sts ctx ()
runTest :: Test t -> Rule sts ctx ()
runTest = (t -> PredicateFailure sts) -> Test t -> Rule sts ctx ()
forall e sts (ctx :: RuleType).
(e -> PredicateFailure sts)
-> Validation (NonEmpty e) () -> Rule sts ctx ()
validateTrans t -> PredicateFailure sts
forall t s. Inject t s => t -> s
inject

runTestOnSignal :: Inject t (PredicateFailure sts) => Test t -> Rule sts ctx ()
runTestOnSignal :: Test t -> Rule sts ctx ()
runTestOnSignal = (t -> PredicateFailure sts)
-> NonEmpty Label -> Test t -> Rule sts ctx ()
forall e sts (ctx :: RuleType).
(e -> PredicateFailure sts)
-> NonEmpty Label -> Validation (NonEmpty e) () -> Rule sts ctx ()
validateTransLabeled t -> PredicateFailure sts
forall t s. Inject t s => t -> s
inject (NonEmpty Label -> Test t -> Rule sts ctx ())
-> NonEmpty Label -> Test t -> Rule sts ctx ()
forall a b. (a -> b) -> a -> b
$ Label
lblStatic Label -> [Label] -> NonEmpty Label
forall a. a -> [a] -> NonEmpty a
NE.:| []

runTestMaybe :: InjectMaybe t (PredicateFailure sts) => Test t -> Rule sts ctx ()
runTestMaybe :: Test t -> Rule sts ctx ()
runTestMaybe = Validation (NonEmpty (PredicateFailure sts)) () -> Rule sts ctx ()
forall sts (ctx :: RuleType).
Validation (NonEmpty (PredicateFailure sts)) () -> Rule sts ctx ()
validate (Validation (NonEmpty (PredicateFailure sts)) ()
 -> Rule sts ctx ())
-> (Test t -> Validation (NonEmpty (PredicateFailure sts)) ())
-> Test t
-> Rule sts ctx ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (t -> Maybe (PredicateFailure sts))
-> Test t -> Validation (NonEmpty (PredicateFailure sts)) ()
forall e e'.
(e -> Maybe e')
-> Validation (NonEmpty e) () -> Validation (NonEmpty e') ()
mapMaybeValidation t -> Maybe (PredicateFailure sts)
forall t s. InjectMaybe t s => t -> Maybe s
injectMaybe