{-# 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,

  -- * Interface for independent Tests
  Inject (..),
  Test,
  runTest,
  runTestOnSignal,
  failOnJustStatic,

  -- * Validation with injection of predicate failures
  (?!.),
  checkFailOnJust,
  checkFailOnNonEmpty,
  checkFailOnNonEmptySet,
  checkFailOnNonEmptyMap,

  -- ** Static
  (?!#.),
  checkFailOnLeftStatic,
  checkFailOnJustStatic,
) 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 qualified Data.Map.NonEmpty as NEM
import Data.Map.Strict (Map)
import qualified Data.Set.NonEmpty as NES
import Validation

--------------------------------------------------------------------------------
-- 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 ()
(?!#) = 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 ()
?!#: :: forall e sts (ctx :: RuleType).
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 :: forall sts (ctx :: RuleType).
PredicateFailure sts -> Rule sts ctx ()
failBecauseS = (Bool
False Bool -> PredicateFailure sts -> Rule sts ctx ()
forall sts (ctx :: RuleType).
Bool -> PredicateFailure sts -> Rule sts ctx ()
?!#)

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

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 = (f era -> PredicateFailure (EraRule rule era))
-> Validation (NonEmpty (f era)) ()
-> F (Clause (EraRule rule era) ctx) ()
forall e sts (ctx :: RuleType).
(e -> PredicateFailure sts)
-> Validation (NonEmpty e) () -> Rule sts ctx ()
validateTrans f era -> PredicateFailure (EraRule rule era)
f era -> EraRuleFailure rule era
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 = (f era -> PredicateFailure (EraRule rule era))
-> NonEmpty Label
-> Validation (NonEmpty (f era)) ()
-> Rule (EraRule rule era) ctx ()
forall e sts (ctx :: RuleType).
(e -> PredicateFailure sts)
-> NonEmpty Label -> Validation (NonEmpty e) () -> Rule sts ctx ()
validateTransLabeled f era -> PredicateFailure (EraRule rule era)
f era -> EraRuleFailure rule era
forall (rule :: Symbol) (t :: * -> *) era.
InjectRuleFailure rule t era =>
t era -> EraRuleFailure rule era
injectFailure (NonEmpty Label
 -> Validation (NonEmpty (f era)) ()
 -> Rule (EraRule rule era) ctx ())
-> NonEmpty Label
-> Validation (NonEmpty (f era)) ()
-> Rule (EraRule rule era) ctx ()
forall a b. (a -> b) -> a -> b
$ Label
lblStatic Label -> [Label] -> NonEmpty Label
forall a. a -> [a] -> NonEmpty a
NE.:| []

failOnJustStatic :: Maybe a -> (a -> PredicateFailure sts) -> Rule sts ctx ()
failOnJustStatic :: forall a sts (ctx :: RuleType).
Maybe a -> (a -> PredicateFailure sts) -> Rule sts ctx ()
failOnJustStatic Maybe a
cond a -> PredicateFailure sts
onJust =
  (PredicateFailure sts -> PredicateFailure sts)
-> NonEmpty Label
-> Validation (NonEmpty (PredicateFailure sts)) ()
-> Rule sts ctx ()
forall e sts (ctx :: RuleType).
(e -> PredicateFailure sts)
-> NonEmpty Label -> Validation (NonEmpty e) () -> Rule sts ctx ()
validateTransLabeled PredicateFailure sts -> PredicateFailure sts
forall a. a -> a
id (Label
lblStatic Label -> [Label] -> NonEmpty Label
forall a. a -> [a] -> NonEmpty a
NE.:| []) (Validation (NonEmpty (PredicateFailure sts)) ()
 -> Rule sts ctx ())
-> Validation (NonEmpty (PredicateFailure sts)) ()
-> Rule sts ctx ()
forall a b. (a -> b) -> a -> b
$ Maybe a
-> (a -> PredicateFailure sts)
-> Validation (NonEmpty (PredicateFailure sts)) ()
forall a e. Maybe a -> (a -> e) -> Validation (NonEmpty e) ()
failureOnJust Maybe a
cond a -> PredicateFailure sts
onJust
{-# INLINE failOnJustStatic #-}

-- =========== Validation with injection of predicate failures ===========

-- | Same as `?!`, except accepts injectable predicate failure
(?!.) ::
  (InjectRuleFailure rule t era, PredicateFailure sts ~ EraRuleFailure rule era) =>
  Bool -> t era -> Rule sts ctx ()
?!. :: forall (rule :: Symbol) (t :: * -> *) era sts (ctx :: RuleType).
(InjectRuleFailure rule t era,
 PredicateFailure sts ~ EraRuleFailure rule era) =>
Bool -> t era -> Rule sts ctx ()
(?!.) Bool
cond t era
predFailure = Bool
cond Bool -> PredicateFailure sts -> Rule sts ctx ()
forall sts (ctx :: RuleType).
Bool -> PredicateFailure sts -> Rule sts ctx ()
?! t era -> EraRuleFailure rule era
forall (rule :: Symbol) (t :: * -> *) era.
InjectRuleFailure rule t era =>
t era -> EraRuleFailure rule era
injectFailure t era
predFailure
{-# INLINE (?!.) #-}

infix 1 ?!.

-- | Same as `?!#`, except accepts injectable predicate failure
(?!#.) ::
  (InjectRuleFailure rule t era, PredicateFailure sts ~ EraRuleFailure rule era) =>
  Bool -> t era -> Rule sts ctx ()
?!#. :: forall (rule :: Symbol) (t :: * -> *) era sts (ctx :: RuleType).
(InjectRuleFailure rule t era,
 PredicateFailure sts ~ EraRuleFailure rule era) =>
Bool -> t era -> Rule sts ctx ()
(?!#.) Bool
cond t era
predFailure = Bool
cond Bool -> PredicateFailure sts -> Rule sts ctx ()
forall sts (ctx :: RuleType).
Bool -> PredicateFailure sts -> Rule sts ctx ()
?!# t era -> EraRuleFailure rule era
forall (rule :: Symbol) (t :: * -> *) era.
InjectRuleFailure rule t era =>
t era -> EraRuleFailure rule era
injectFailure t era
predFailure
{-# INLINE (?!#.) #-}

infix 1 ?!#.

-- | Same as `failOnJust`, except accepts injectable predicate failure
checkFailOnJust ::
  (InjectRuleFailure rule t era, PredicateFailure sts ~ EraRuleFailure rule era) =>
  Maybe a -> (a -> t era) -> Rule sts ctx ()
checkFailOnJust :: forall (rule :: Symbol) (t :: * -> *) era sts a (ctx :: RuleType).
(InjectRuleFailure rule t era,
 PredicateFailure sts ~ EraRuleFailure rule era) =>
Maybe a -> (a -> t era) -> Rule sts ctx ()
checkFailOnJust Maybe a
cond a -> t era
onJust = Maybe a -> (a -> PredicateFailure sts) -> Rule sts ctx ()
forall a sts (ctx :: RuleType).
Maybe a -> (a -> PredicateFailure sts) -> Rule sts ctx ()
failOnJust Maybe a
cond (t era -> PredicateFailure sts
t era -> EraRuleFailure rule era
forall (rule :: Symbol) (t :: * -> *) era.
InjectRuleFailure rule t era =>
t era -> EraRuleFailure rule era
injectFailure (t era -> PredicateFailure sts)
-> (a -> t era) -> a -> PredicateFailure sts
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> t era
onJust)
{-# INLINE checkFailOnJust #-}

-- | Same as `failOnNonEmpty`, except accepts injectable predicate failure
checkFailOnNonEmpty ::
  ( InjectRuleFailure rule t era
  , PredicateFailure sts ~ EraRuleFailure rule era
  , Foldable f
  ) =>
  f a -> (NonEmpty a -> t era) -> Rule sts ctx ()
checkFailOnNonEmpty :: forall (rule :: Symbol) (t :: * -> *) era sts (f :: * -> *) a
       (ctx :: RuleType).
(InjectRuleFailure rule t era,
 PredicateFailure sts ~ EraRuleFailure rule era, Foldable f) =>
f a -> (NonEmpty a -> t era) -> Rule sts ctx ()
checkFailOnNonEmpty f a
cond NonEmpty a -> t era
onJust = f a -> (NonEmpty a -> PredicateFailure sts) -> Rule sts ctx ()
forall (f :: * -> *) a sts (ctx :: RuleType).
Foldable f =>
f a -> (NonEmpty a -> PredicateFailure sts) -> Rule sts ctx ()
failOnNonEmpty f a
cond (t era -> PredicateFailure sts
t era -> EraRuleFailure rule era
forall (rule :: Symbol) (t :: * -> *) era.
InjectRuleFailure rule t era =>
t era -> EraRuleFailure rule era
injectFailure (t era -> PredicateFailure sts)
-> (NonEmpty a -> t era) -> NonEmpty a -> PredicateFailure sts
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NonEmpty a -> t era
onJust)
{-# INLINE checkFailOnNonEmpty #-}

-- | Same as `failOnNonEmptySet`, except accepts injectable predicate failure
checkFailOnNonEmptySet ::
  ( InjectRuleFailure rule t era
  , PredicateFailure sts ~ EraRuleFailure rule era
  , Foldable f
  , Ord a
  ) =>
  f a -> (NES.NonEmptySet a -> t era) -> Rule sts ctx ()
checkFailOnNonEmptySet :: forall (rule :: Symbol) (t :: * -> *) era sts (f :: * -> *) a
       (ctx :: RuleType).
(InjectRuleFailure rule t era,
 PredicateFailure sts ~ EraRuleFailure rule era, Foldable f,
 Ord a) =>
f a -> (NonEmptySet a -> t era) -> Rule sts ctx ()
checkFailOnNonEmptySet f a
cond NonEmptySet a -> t era
onJust = f a -> (NonEmptySet a -> PredicateFailure sts) -> Rule sts ctx ()
forall (f :: * -> *) a sts (ctx :: RuleType).
(Foldable f, Ord a) =>
f a -> (NonEmptySet a -> PredicateFailure sts) -> Rule sts ctx ()
failOnNonEmptySet f a
cond (t era -> PredicateFailure sts
t era -> EraRuleFailure rule era
forall (rule :: Symbol) (t :: * -> *) era.
InjectRuleFailure rule t era =>
t era -> EraRuleFailure rule era
injectFailure (t era -> PredicateFailure sts)
-> (NonEmptySet a -> t era)
-> NonEmptySet a
-> PredicateFailure sts
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NonEmptySet a -> t era
onJust)
{-# INLINE checkFailOnNonEmptySet #-}

-- | Same as `failOnNonEmptyMap`, except accepts injectable predicate failure
checkFailOnNonEmptyMap ::
  (InjectRuleFailure rule t era, PredicateFailure sts ~ EraRuleFailure rule era) =>
  Map k v -> (NEM.NonEmptyMap k v -> t era) -> Rule sts ctx ()
checkFailOnNonEmptyMap :: forall (rule :: Symbol) (t :: * -> *) era sts k v
       (ctx :: RuleType).
(InjectRuleFailure rule t era,
 PredicateFailure sts ~ EraRuleFailure rule era) =>
Map k v -> (NonEmptyMap k v -> t era) -> Rule sts ctx ()
checkFailOnNonEmptyMap Map k v
cond NonEmptyMap k v -> t era
onJust = Map k v
-> (NonEmptyMap k v -> PredicateFailure sts) -> Rule sts ctx ()
forall k v sts (ctx :: RuleType).
Map k v
-> (NonEmptyMap k v -> PredicateFailure sts) -> Rule sts ctx ()
failOnNonEmptyMap Map k v
cond (t era -> PredicateFailure sts
t era -> EraRuleFailure rule era
forall (rule :: Symbol) (t :: * -> *) era.
InjectRuleFailure rule t era =>
t era -> EraRuleFailure rule era
injectFailure (t era -> PredicateFailure sts)
-> (NonEmptyMap k v -> t era)
-> NonEmptyMap k v
-> PredicateFailure sts
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NonEmptyMap k v -> t era
onJust)
{-# INLINE checkFailOnNonEmptyMap #-}

-- | Same as `?!#:`, except accepts injectable predicate failure and is not designed to be used as
-- infix operator
checkFailOnLeftStatic ::
  (InjectRuleFailure rule t era, PredicateFailure sts ~ EraRuleFailure rule era) =>
  Either e () -> (e -> t era) -> Rule sts ctx ()
checkFailOnLeftStatic :: forall (rule :: Symbol) (t :: * -> *) era sts e (ctx :: RuleType).
(InjectRuleFailure rule t era,
 PredicateFailure sts ~ EraRuleFailure rule era) =>
Either e () -> (e -> t era) -> Rule sts ctx ()
checkFailOnLeftStatic Either e ()
cond e -> t era
predFailure = Either e ()
cond Either e () -> (e -> PredicateFailure sts) -> Rule sts ctx ()
forall e sts (ctx :: RuleType).
Either e () -> (e -> PredicateFailure sts) -> Rule sts ctx ()
?!#: (t era -> PredicateFailure sts
t era -> EraRuleFailure rule era
forall (rule :: Symbol) (t :: * -> *) era.
InjectRuleFailure rule t era =>
t era -> EraRuleFailure rule era
injectFailure (t era -> PredicateFailure sts)
-> (e -> t era) -> e -> PredicateFailure sts
forall b c a. (b -> c) -> (a -> b) -> a -> c
. e -> t era
predFailure)
{-# INLINE checkFailOnLeftStatic #-}

-- | Same as `failOnJustStatic`, except accepts injectable predicate failure
checkFailOnJustStatic ::
  (InjectRuleFailure rule t era, PredicateFailure sts ~ EraRuleFailure rule era) =>
  Maybe a -> (a -> t era) -> Rule sts ctx ()
checkFailOnJustStatic :: forall (rule :: Symbol) (t :: * -> *) era sts a (ctx :: RuleType).
(InjectRuleFailure rule t era,
 PredicateFailure sts ~ EraRuleFailure rule era) =>
Maybe a -> (a -> t era) -> Rule sts ctx ()
checkFailOnJustStatic Maybe a
cond a -> t era
onJust = Maybe a -> (a -> PredicateFailure sts) -> Rule sts ctx ()
forall a sts (ctx :: RuleType).
Maybe a -> (a -> PredicateFailure sts) -> Rule sts ctx ()
failOnJustStatic Maybe a
cond (t era -> PredicateFailure sts
t era -> EraRuleFailure rule era
forall (rule :: Symbol) (t :: * -> *) era.
InjectRuleFailure rule t era =>
t era -> EraRuleFailure rule era
injectFailure (t era -> PredicateFailure sts)
-> (a -> t era) -> a -> PredicateFailure sts
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> t era
onJust)
{-# INLINE checkFailOnJustStatic #-}