{-# LANGUAGE DeriveAnyClass     #-}
{-# LANGUAGE DeriveGeneric      #-}
{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE FlexibleContexts   #-}
{-# LANGUAGE FlexibleInstances  #-}
{-# LANGUAGE LambdaCase         #-}
{-# LANGUAGE MonoLocalBinds     #-}
{-# LANGUAGE NamedFieldPuns     #-}
{-# LANGUAGE NoImplicitPrelude  #-}
{-# LANGUAGE OverloadedStrings  #-}

module Ledger.Tx.Constraints.ValidityInterval
  ( ValidityInterval(..)
  , interval
  , from
  , lessThan
  , fromPlutusInterval
  , toPlutusInterval
  ) where

import Data.Aeson (FromJSON, ToJSON)
import GHC.Generics (Generic)
import Plutus.V1.Ledger.Interval (Extended (Finite, NegInf, PosInf), Interval (Interval), LowerBound (LowerBound),
                                  UpperBound (UpperBound))
import PlutusTx.Prelude (Bool (False, True), Enum (succ), Functor (fmap), Maybe (Just, Nothing))
import Prelude qualified as Haskell

{- Note [About ValidityInterval]

During the transition from `plutus-apps` ledger validation rules to
`cardano-ledger` validation rules we have found that the `cardano-ledger` has a
problem with the translation from the transaction's upper bound slot to the
'TxInfo' validity range upper bound time. By definition, as given by the ledger
specification, the upper bound should be open (exclusive) but they convert it
as a closed bound.

We encountered this issue by getting a Phase 2 validation error when doing:

@
 txValidityTimeRange `contains` txInfoValidRange scriptContextTxInfo
@

in a Plutus validation script if 'txValidityTimeRange' does not define a lower
bound (using 'NegInf').

We have introduced 'ValidityInterval' type to provide a correct by construction way
for dealing with validity intervals. More details are available in ADR-13 doc/adr/0013-tx-validity-time-range-fix.rst.

For more info on the bug in ledger, see https://github.com/input-output-hk/cardano-ledger/issues/3043.
Note that this bug will be fixed in a future HF (next HF after Vasil -> PlutusV3 or later).
-}

-- | 'ValidityInterval' is a half open interval. Closed (inclusive) on the bottom, open
-- (exclusive) on the top. A 'Nothing' on the bottom is negative infinity, and a 'Nothing'
-- on the top is positive infinity.
data ValidityInterval a = ValidityInterval
  { ValidityInterval a -> Maybe a
invalidBefore    :: !(Maybe a) -- ^ Inclusive lower bound or negative infinity
  , ValidityInterval a -> Maybe a
invalidHereafter :: !(Maybe a) -- ^ Exclusive upper bound or positive infinity
  }
  deriving stock (Int -> ValidityInterval a -> ShowS
[ValidityInterval a] -> ShowS
ValidityInterval a -> String
(Int -> ValidityInterval a -> ShowS)
-> (ValidityInterval a -> String)
-> ([ValidityInterval a] -> ShowS)
-> Show (ValidityInterval a)
forall a. Show a => Int -> ValidityInterval a -> ShowS
forall a. Show a => [ValidityInterval a] -> ShowS
forall a. Show a => ValidityInterval a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [ValidityInterval a] -> ShowS
$cshowList :: forall a. Show a => [ValidityInterval a] -> ShowS
show :: ValidityInterval a -> String
$cshow :: forall a. Show a => ValidityInterval a -> String
showsPrec :: Int -> ValidityInterval a -> ShowS
$cshowsPrec :: forall a. Show a => Int -> ValidityInterval a -> ShowS
Haskell.Show, (forall x. ValidityInterval a -> Rep (ValidityInterval a) x)
-> (forall x. Rep (ValidityInterval a) x -> ValidityInterval a)
-> Generic (ValidityInterval a)
forall x. Rep (ValidityInterval a) x -> ValidityInterval a
forall x. ValidityInterval a -> Rep (ValidityInterval a) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall a x. Rep (ValidityInterval a) x -> ValidityInterval a
forall a x. ValidityInterval a -> Rep (ValidityInterval a) x
$cto :: forall a x. Rep (ValidityInterval a) x -> ValidityInterval a
$cfrom :: forall a x. ValidityInterval a -> Rep (ValidityInterval a) x
Generic, ValidityInterval a -> ValidityInterval a -> Bool
(ValidityInterval a -> ValidityInterval a -> Bool)
-> (ValidityInterval a -> ValidityInterval a -> Bool)
-> Eq (ValidityInterval a)
forall a. Eq a => ValidityInterval a -> ValidityInterval a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: ValidityInterval a -> ValidityInterval a -> Bool
$c/= :: forall a. Eq a => ValidityInterval a -> ValidityInterval a -> Bool
== :: ValidityInterval a -> ValidityInterval a -> Bool
$c== :: forall a. Eq a => ValidityInterval a -> ValidityInterval a -> Bool
Haskell.Eq)
  deriving anyclass ([ValidityInterval a] -> Encoding
[ValidityInterval a] -> Value
ValidityInterval a -> Encoding
ValidityInterval a -> Value
(ValidityInterval a -> Value)
-> (ValidityInterval a -> Encoding)
-> ([ValidityInterval a] -> Value)
-> ([ValidityInterval a] -> Encoding)
-> ToJSON (ValidityInterval a)
forall a. ToJSON a => [ValidityInterval a] -> Encoding
forall a. ToJSON a => [ValidityInterval a] -> Value
forall a. ToJSON a => ValidityInterval a -> Encoding
forall a. ToJSON a => ValidityInterval a -> Value
forall a.
(a -> Value)
-> (a -> Encoding)
-> ([a] -> Value)
-> ([a] -> Encoding)
-> ToJSON a
toEncodingList :: [ValidityInterval a] -> Encoding
$ctoEncodingList :: forall a. ToJSON a => [ValidityInterval a] -> Encoding
toJSONList :: [ValidityInterval a] -> Value
$ctoJSONList :: forall a. ToJSON a => [ValidityInterval a] -> Value
toEncoding :: ValidityInterval a -> Encoding
$ctoEncoding :: forall a. ToJSON a => ValidityInterval a -> Encoding
toJSON :: ValidityInterval a -> Value
$ctoJSON :: forall a. ToJSON a => ValidityInterval a -> Value
ToJSON, Value -> Parser [ValidityInterval a]
Value -> Parser (ValidityInterval a)
(Value -> Parser (ValidityInterval a))
-> (Value -> Parser [ValidityInterval a])
-> FromJSON (ValidityInterval a)
forall a. FromJSON a => Value -> Parser [ValidityInterval a]
forall a. FromJSON a => Value -> Parser (ValidityInterval a)
forall a.
(Value -> Parser a) -> (Value -> Parser [a]) -> FromJSON a
parseJSONList :: Value -> Parser [ValidityInterval a]
$cparseJSONList :: forall a. FromJSON a => Value -> Parser [ValidityInterval a]
parseJSON :: Value -> Parser (ValidityInterval a)
$cparseJSON :: forall a. FromJSON a => Value -> Parser (ValidityInterval a)
FromJSON)

instance Functor ValidityInterval where
  fmap :: (a -> b) -> ValidityInterval a -> ValidityInterval b
fmap a -> b
f (ValidityInterval Maybe a
from' Maybe a
to') = Maybe b -> Maybe b -> ValidityInterval b
forall a. Maybe a -> Maybe a -> ValidityInterval a
ValidityInterval ((a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> b
f Maybe a
from') ((a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> b
f Maybe a
to')

{-# INLINABLE interval #-}
-- | @interval a b@ includes all values that are greater than or equal to @a@
-- and smaller than @b@. In math. notation: [a,b)
interval :: a -> a -> ValidityInterval a
interval :: a -> a -> ValidityInterval a
interval a
s a
s' = Maybe a -> Maybe a -> ValidityInterval a
forall a. Maybe a -> Maybe a -> ValidityInterval a
ValidityInterval (a -> Maybe a
forall a. a -> Maybe a
Just a
s) (a -> Maybe a
forall a. a -> Maybe a
Just a
s')

{-# INLINABLE from #-}
-- | @from a@ is an 'ValidityInterval' that includes all values that are
--  greater than or equal to @a@. In math. notation: [a,+∞]
from :: a -> ValidityInterval a
from :: a -> ValidityInterval a
from a
s = Maybe a -> Maybe a -> ValidityInterval a
forall a. Maybe a -> Maybe a -> ValidityInterval a
ValidityInterval (a -> Maybe a
forall a. a -> Maybe a
Just a
s) Maybe a
forall a. Maybe a
Nothing

{-# INLINABLE lessThan #-}
-- | @lessThan a@ is an 'ValidityInterval' that includes all values that are
--  smaller than @a@. In math. notation: [-∞,a)
lessThan :: a -> ValidityInterval a
lessThan :: a -> ValidityInterval a
lessThan a
s = Maybe a -> Maybe a -> ValidityInterval a
forall a. Maybe a -> Maybe a -> ValidityInterval a
ValidityInterval Maybe a
forall a. Maybe a
Nothing (a -> Maybe a
forall a. a -> Maybe a
Just a
s)

{-# INLINABLE fromLowerBound #-}
fromLowerBound :: Enum a => LowerBound a -> Maybe a
fromLowerBound :: LowerBound a -> Maybe a
fromLowerBound (LowerBound (Finite a
v) Bool
closed) = if Bool
closed then a -> Maybe a
forall a. a -> Maybe a
Just a
v else a -> Maybe a
forall a. a -> Maybe a
Just (a -> a
forall a. Enum a => a -> a
succ a
v)
fromLowerBound LowerBound a
_                              = Maybe a
forall a. Maybe a
Nothing

{-# INLINABLE fromUpperBound #-}
fromUpperBound :: Enum a => UpperBound a -> Maybe a
fromUpperBound :: UpperBound a -> Maybe a
fromUpperBound (UpperBound (Finite a
v) Bool
closed) = if Bool
closed then a -> Maybe a
forall a. a -> Maybe a
Just (a -> a
forall a. Enum a => a -> a
succ a
v) else a -> Maybe a
forall a. a -> Maybe a
Just a
v
fromUpperBound UpperBound a
_                              = Maybe a
forall a. Maybe a
Nothing

{-# INLINABLE fromPlutusInterval #-}
fromPlutusInterval :: Enum a => Interval a -> ValidityInterval a
fromPlutusInterval :: Interval a -> ValidityInterval a
fromPlutusInterval (Interval LowerBound a
from' UpperBound a
to') = Maybe a -> Maybe a -> ValidityInterval a
forall a. Maybe a -> Maybe a -> ValidityInterval a
ValidityInterval (LowerBound a -> Maybe a
forall a. Enum a => LowerBound a -> Maybe a
fromLowerBound LowerBound a
from') (UpperBound a -> Maybe a
forall a. Enum a => UpperBound a -> Maybe a
fromUpperBound UpperBound a
to')

{-# INLINABLE toLowerBound #-}
toLowerBound :: Maybe a -> LowerBound a
toLowerBound :: Maybe a -> LowerBound a
toLowerBound (Just a
v) = Extended a -> Bool -> LowerBound a
forall a. Extended a -> Bool -> LowerBound a
LowerBound (a -> Extended a
forall a. a -> Extended a
Finite a
v) Bool
True
toLowerBound Maybe a
_        = Extended a -> Bool -> LowerBound a
forall a. Extended a -> Bool -> LowerBound a
LowerBound Extended a
forall a. Extended a
NegInf Bool
True

{-# INLINABLE toUpperBound #-}
toUpperBound :: Maybe a -> UpperBound a
toUpperBound :: Maybe a -> UpperBound a
toUpperBound (Just a
v) = Extended a -> Bool -> UpperBound a
forall a. Extended a -> Bool -> UpperBound a
UpperBound (a -> Extended a
forall a. a -> Extended a
Finite a
v) Bool
False
toUpperBound Maybe a
_        = Extended a -> Bool -> UpperBound a
forall a. Extended a -> Bool -> UpperBound a
UpperBound Extended a
forall a. Extended a
PosInf Bool
True

{-# INLINABLE toPlutusInterval #-}
toPlutusInterval :: ValidityInterval a -> Interval a
toPlutusInterval :: ValidityInterval a -> Interval a
toPlutusInterval (ValidityInterval Maybe a
from' Maybe a
to') = LowerBound a -> UpperBound a -> Interval a
forall a. LowerBound a -> UpperBound a -> Interval a
Interval (Maybe a -> LowerBound a
forall a. Maybe a -> LowerBound a
toLowerBound Maybe a
from') (Maybe a -> UpperBound a
forall a. Maybe a -> UpperBound a
toUpperBound Maybe a
to')