{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}

-- | 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 for independent Tests
  Inject (..),
  Test,
  runTest,
  runTestOnSignal,
)
where

import Cardano.Ledger.BaseTypes (Inject (..))
import Cardano.Ledger.Core
import Control.State.Transition.Extended
import Data.List.NonEmpty (NonEmpty)
import qualified Data.List.NonEmpty as NE
import Validation

applySTSValidateSuchThat ::
  forall s m rtype.
  (STS s, RuleTypeRep rtype, m ~ BaseM s) =>
  ([Label] -> Bool) ->
  RuleContext rtype s ->
  m (Either (NonEmpty (PredicateFailure s)) (State s))
applySTSValidateSuchThat :: forall s (m :: * -> *) (rtype :: RuleType).
(STS s, RuleTypeRep rtype, m ~ BaseM s) =>
([Label] -> Bool)
-> RuleContext rtype s
-> m (Either (NonEmpty (PredicateFailure s)) (State s))
applySTSValidateSuchThat [Label] -> Bool
cond =
  forall s (m :: * -> *) (rtype :: RuleType) (ep :: EventPolicy).
(STS s, RuleTypeRep rtype, m ~ BaseM s) =>
ApplySTSOpts ep
-> RuleContext rtype s
-> m (Either
        (NonEmpty (PredicateFailure s)) (EventReturnType ep s (State s)))
applySTSOptsEither ApplySTSOpts 'EventPolicyDiscard
opts
  where
    opts :: ApplySTSOpts 'EventPolicyDiscard
opts =
      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 ()
?!# :: forall sts (ctx :: RuleType).
Bool -> PredicateFailure sts -> Rule sts ctx ()
(?!#) = forall sts (ctx :: RuleType).
NonEmpty Label -> Bool -> PredicateFailure sts -> Rule sts ctx ()
labeledPred forall a b. (a -> b) -> a -> b
$ Label
lblStatic 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 ()
?!#: :: forall e sts (ctx :: RuleType).
Either e () -> (e -> PredicateFailure sts) -> Rule sts ctx ()
(?!#:) = forall e sts (ctx :: RuleType).
NonEmpty Label
-> Either e () -> (e -> PredicateFailure sts) -> Rule sts ctx ()
labeledPredE forall a b. (a -> b) -> a -> b
$ Label
lblStatic forall a. a -> [a] -> NonEmpty a
NE.:| []

infix 1 ?!#:

-- | Fail, if static checks are enabled.
failBecauseS :: PredicateFailure sts -> Rule sts ctx ()
failBecauseS :: forall sts (ctx :: RuleType).
PredicateFailure sts -> Rule sts ctx ()
failBecauseS = (Bool
False 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 (NonEmpty (PredicateFailure s)) (State s))
applySTSNonStatic :: forall s (m :: * -> *) (rtype :: RuleType).
(STS s, RuleTypeRep rtype, m ~ BaseM s) =>
RuleContext rtype s
-> m (Either (NonEmpty (PredicateFailure s)) (State s))
applySTSNonStatic = forall s (m :: * -> *) (rtype :: RuleType).
(STS s, RuleTypeRep rtype, m ~ BaseM s) =>
([Label] -> Bool)
-> RuleContext rtype s
-> m (Either (NonEmpty (PredicateFailure s)) (State s))
applySTSValidateSuchThat (forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
notElem Label
lblStatic)

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

type Test failure = Validation (NonEmpty failure) ()

runTest :: InjectRuleFailure rule f era => Test (f era) -> Rule (EraRule rule era) ctx ()
runTest :: forall (rule :: Symbol) (f :: * -> *) era (ctx :: RuleType).
InjectRuleFailure rule f era =>
Test (f era) -> Rule (EraRule rule era) ctx ()
runTest = forall e sts (ctx :: RuleType).
(e -> PredicateFailure sts)
-> Validation (NonEmpty e) () -> Rule sts ctx ()
validateTrans forall (rule :: Symbol) (t :: * -> *) era.
InjectRuleFailure rule t era =>
t era -> EraRuleFailure rule era
injectFailure

runTestOnSignal :: InjectRuleFailure rule f era => Test (f era) -> Rule (EraRule rule era) ctx ()
runTestOnSignal :: forall (rule :: Symbol) (f :: * -> *) era (ctx :: RuleType).
InjectRuleFailure rule f era =>
Test (f era) -> Rule (EraRule rule era) ctx ()
runTestOnSignal = forall e sts (ctx :: RuleType).
(e -> PredicateFailure sts)
-> NonEmpty Label -> Validation (NonEmpty e) () -> Rule sts ctx ()
validateTransLabeled forall (rule :: Symbol) (t :: * -> *) era.
InjectRuleFailure rule t era =>
t era -> EraRuleFailure rule era
injectFailure forall a b. (a -> b) -> a -> b
$ Label
lblStatic forall a. a -> [a] -> NonEmpty a
NE.:| []