{-# LANGUAGE DataKinds           #-}
{-# LANGUAGE DeriveAnyClass      #-}
{-# LANGUAGE DerivingStrategies  #-}
{-# LANGUAGE NamedFieldPuns      #-}
{-# LANGUAGE NoImplicitPrelude   #-}
{-# LANGUAGE OverloadedStrings   #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications    #-}
{-# LANGUAGE TypeFamilies        #-}
{-# OPTIONS_GHC -fno-specialise #-}
{-# OPTIONS_GHC -fno-omit-interface-pragmas #-}
{-# OPTIONS_GHC -fno-ignore-interface-pragmas #-}

-- | On-chain code fragments for creating a state machine. First
--   define a @StateMachine s i@ with input type @i@ and state type @s@. Then
--   use 'mkValidator' in on-chain code to check the required hashes and
--   validate the transition, and 'mkRedeemer' to make redeemer scripts.
module Plutus.Contract.StateMachine.OnChain(
      StateMachine(..)
    , StateMachineInstance (..)
    , State(..)
    , mkStateMachine
    , machineAddress
    , mkValidator
    , threadTokenValueOrZero
    ) where

import Cardano.Node.Emulator.Internal.Node.Params (testnet)
import Data.Aeson (FromJSON, ToJSON)
import Data.Void (Void)
import GHC.Generics (Generic)
import Ledger (CardanoAddress)
import Ledger.Tx.Constraints (TxConstraints (txOwnOutputs), mustPayToTheScriptWithInlineDatum)
import Ledger.Tx.Constraints.OnChain.V2 (checkScriptContext)
import Ledger.Typed.Scripts (DatumType, RedeemerType, ValidatorTypes, validatorCardanoAddress, validatorHash)
import Plutus.Script.Utils.V2.Typed.Scripts (TypedValidator, ValidatorType)
import Plutus.Script.Utils.Value (Value, isZero)
import Plutus.V2.Ledger.Api (ValidatorHash)
import Plutus.V2.Ledger.Contexts (ScriptContext, TxInInfo (txInInfoResolved), findOwnInput, ownHash)
import Plutus.V2.Ledger.Tx qualified as PV2
import PlutusTx qualified
import PlutusTx.Prelude hiding (check)
import Prelude qualified as Haskell

import Plutus.Contract.StateMachine.ThreadToken qualified as TT

data State s = State { State s -> s
stateData :: s, State s -> Value
stateValue :: Value }
    deriving stock (State s -> State s -> Bool
(State s -> State s -> Bool)
-> (State s -> State s -> Bool) -> Eq (State s)
forall s. Eq s => State s -> State s -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: State s -> State s -> Bool
$c/= :: forall s. Eq s => State s -> State s -> Bool
== :: State s -> State s -> Bool
$c== :: forall s. Eq s => State s -> State s -> Bool
Haskell.Eq, Int -> State s -> ShowS
[State s] -> ShowS
State s -> String
(Int -> State s -> ShowS)
-> (State s -> String) -> ([State s] -> ShowS) -> Show (State s)
forall s. Show s => Int -> State s -> ShowS
forall s. Show s => [State s] -> ShowS
forall s. Show s => State s -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [State s] -> ShowS
$cshowList :: forall s. Show s => [State s] -> ShowS
show :: State s -> String
$cshow :: forall s. Show s => State s -> String
showsPrec :: Int -> State s -> ShowS
$cshowsPrec :: forall s. Show s => Int -> State s -> ShowS
Haskell.Show, (forall x. State s -> Rep (State s) x)
-> (forall x. Rep (State s) x -> State s) -> Generic (State s)
forall x. Rep (State s) x -> State s
forall x. State s -> Rep (State s) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall s x. Rep (State s) x -> State s
forall s x. State s -> Rep (State s) x
$cto :: forall s x. Rep (State s) x -> State s
$cfrom :: forall s x. State s -> Rep (State s) x
Generic)
    deriving anyclass ([State s] -> Encoding
[State s] -> Value
State s -> Encoding
State s -> Value
(State s -> Value)
-> (State s -> Encoding)
-> ([State s] -> Value)
-> ([State s] -> Encoding)
-> ToJSON (State s)
forall s. ToJSON s => [State s] -> Encoding
forall s. ToJSON s => [State s] -> Value
forall s. ToJSON s => State s -> Encoding
forall s. ToJSON s => State s -> Value
forall a.
(a -> Value)
-> (a -> Encoding)
-> ([a] -> Value)
-> ([a] -> Encoding)
-> ToJSON a
toEncodingList :: [State s] -> Encoding
$ctoEncodingList :: forall s. ToJSON s => [State s] -> Encoding
toJSONList :: [State s] -> Value
$ctoJSONList :: forall s. ToJSON s => [State s] -> Value
toEncoding :: State s -> Encoding
$ctoEncoding :: forall s. ToJSON s => State s -> Encoding
toJSON :: State s -> Value
$ctoJSON :: forall s. ToJSON s => State s -> Value
ToJSON, Value -> Parser [State s]
Value -> Parser (State s)
(Value -> Parser (State s))
-> (Value -> Parser [State s]) -> FromJSON (State s)
forall s. FromJSON s => Value -> Parser [State s]
forall s. FromJSON s => Value -> Parser (State s)
forall a.
(Value -> Parser a) -> (Value -> Parser [a]) -> FromJSON a
parseJSONList :: Value -> Parser [State s]
$cparseJSONList :: forall s. FromJSON s => Value -> Parser [State s]
parseJSON :: Value -> Parser (State s)
$cparseJSON :: forall s. FromJSON s => Value -> Parser (State s)
FromJSON)

-- | Specification of a state machine, consisting of a transition function that determines the
-- next state from the current state and an input, and a checking function that checks the validity
-- of the transition in the context of the current transaction.
data StateMachine s i = StateMachine {
      -- | The transition function of the state machine. 'Nothing' indicates an invalid transition from the current state.
      StateMachine s i
-> State s -> i -> Maybe (TxConstraints Void Void, State s)
smTransition  :: State s -> i -> Maybe (TxConstraints Void Void, State s),

      -- | Check whether a state is the final state
      StateMachine s i -> s -> Bool
smFinal       :: s -> Bool,

      -- | The condition checking function. Can be used to perform
      --   checks on the pending transaction that aren't covered by the
      --   constraints. 'smCheck' is always run in addition to checking the
      --   constraints, so the default implementation always returns true.
      StateMachine s i -> s -> i -> ScriptContext -> Bool
smCheck       :: s -> i -> ScriptContext -> Bool,

      -- | The 'ThreadToken' that identifies the contract instance.
      --   Make one with 'getThreadToken' and pass it on to 'mkStateMachine'.
      --   Initialising the machine will then mint a thread token value.
      StateMachine s i -> Maybe ThreadToken
smThreadToken :: Maybe TT.ThreadToken
    }

{-# INLINABLE threadTokenValueInner #-}
threadTokenValueInner :: Maybe TT.ThreadToken -> ValidatorHash -> Value
threadTokenValueInner :: Maybe ThreadToken -> ValidatorHash -> Value
threadTokenValueInner = (ValidatorHash -> Value)
-> (ThreadToken -> ValidatorHash -> Value)
-> Maybe ThreadToken
-> ValidatorHash
-> Value
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (Value -> ValidatorHash -> Value
forall a b. a -> b -> a
const Value
forall a. Monoid a => a
mempty) (CurrencySymbol -> ValidatorHash -> Value
TT.threadTokenValue (CurrencySymbol -> ValidatorHash -> Value)
-> (ThreadToken -> CurrencySymbol)
-> ThreadToken
-> ValidatorHash
-> Value
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ThreadToken -> CurrencySymbol
TT.ttCurrencySymbol)

{-# INLINABLE threadTokenValueOrZero #-}
-- | The 'Value' containing exactly the thread token, if one has been specified.
threadTokenValueOrZero :: StateMachineInstance s i -> Value
threadTokenValueOrZero :: StateMachineInstance s i -> Value
threadTokenValueOrZero StateMachineInstance{StateMachine s i
stateMachine :: forall s i. StateMachineInstance s i -> StateMachine s i
stateMachine :: StateMachine s i
stateMachine,TypedValidator (StateMachine s i)
typedValidator :: forall s i.
StateMachineInstance s i -> TypedValidator (StateMachine s i)
typedValidator :: TypedValidator (StateMachine s i)
typedValidator} =
    Maybe ThreadToken -> ValidatorHash -> Value
threadTokenValueInner (StateMachine s i -> Maybe ThreadToken
forall s i. StateMachine s i -> Maybe ThreadToken
smThreadToken StateMachine s i
stateMachine) (TypedValidator (StateMachine s i) -> ValidatorHash
forall a. TypedValidator a -> ValidatorHash
validatorHash TypedValidator (StateMachine s i)
typedValidator)

-- | A state machine that does not perform any additional checks on the
--   'ScriptContext' (beyond enforcing the constraints)
mkStateMachine
    :: Maybe TT.ThreadToken
    -> (State s -> i -> Maybe (TxConstraints Void Void, State s))
    -> (s -> Bool)
    -> StateMachine s i
mkStateMachine :: Maybe ThreadToken
-> (State s -> i -> Maybe (TxConstraints Void Void, State s))
-> (s -> Bool)
-> StateMachine s i
mkStateMachine Maybe ThreadToken
smThreadToken State s -> i -> Maybe (TxConstraints Void Void, State s)
smTransition s -> Bool
smFinal =
    StateMachine :: forall s i.
(State s -> i -> Maybe (TxConstraints Void Void, State s))
-> (s -> Bool)
-> (s -> i -> ScriptContext -> Bool)
-> Maybe ThreadToken
-> StateMachine s i
StateMachine
        { State s -> i -> Maybe (TxConstraints Void Void, State s)
smTransition :: State s -> i -> Maybe (TxConstraints Void Void, State s)
smTransition :: State s -> i -> Maybe (TxConstraints Void Void, State s)
smTransition
        , s -> Bool
smFinal :: s -> Bool
smFinal :: s -> Bool
smFinal
        , smCheck :: s -> i -> ScriptContext -> Bool
smCheck = \s
_ i
_ ScriptContext
_ -> Bool
True
        , Maybe ThreadToken
smThreadToken :: Maybe ThreadToken
smThreadToken :: Maybe ThreadToken
smThreadToken
        }

instance ValidatorTypes (StateMachine s i) where
    type instance RedeemerType (StateMachine s i) = i
    type instance DatumType (StateMachine s i) = s

data StateMachineInstance s i = StateMachineInstance {
    -- | The state machine specification.
    StateMachineInstance s i -> StateMachine s i
stateMachine   :: StateMachine s i,
    -- | The validator code for this state machine.
    StateMachineInstance s i -> TypedValidator (StateMachine s i)
typedValidator :: TypedValidator (StateMachine s i)
    }

-- | TODO StateMachine can be use only on a testnet at the moment, to enable it on another network, we need to
-- parametrise the networkId
machineAddress :: StateMachineInstance s i -> CardanoAddress
machineAddress :: StateMachineInstance s i -> CardanoAddress
machineAddress = NetworkId -> TypedValidator (StateMachine s i) -> CardanoAddress
forall a. NetworkId -> TypedValidator a -> CardanoAddress
validatorCardanoAddress NetworkId
testnet (TypedValidator (StateMachine s i) -> CardanoAddress)
-> (StateMachineInstance s i -> TypedValidator (StateMachine s i))
-> StateMachineInstance s i
-> CardanoAddress
forall b c a. (b -> c) -> (a -> b) -> a -> c
. StateMachineInstance s i -> TypedValidator (StateMachine s i)
forall s i.
StateMachineInstance s i -> TypedValidator (StateMachine s i)
typedValidator

{-# INLINABLE mkValidator #-}
-- | Turn a state machine into a validator script.
mkValidator :: forall s i. (PlutusTx.ToData s) => StateMachine s i -> ValidatorType (StateMachine s i)
mkValidator :: StateMachine s i -> ValidatorType (StateMachine s i)
mkValidator (StateMachine State s -> i -> Maybe (TxConstraints Void Void, State s)
step s -> Bool
isFinal s -> i -> ScriptContext -> Bool
check Maybe ThreadToken
threadToken) DatumType (StateMachine s i)
currentState RedeemerType (StateMachine s i)
input ScriptContext
ptx =
    let vl :: Value
vl = Value -> (TxInInfo -> Value) -> Maybe TxInInfo -> Value
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (BuiltinString -> Value
forall a. BuiltinString -> a
traceError BuiltinString
"S0" {-"Can't find validation input"-}) (TxOut -> Value
PV2.txOutValue (TxOut -> Value) -> (TxInInfo -> TxOut) -> TxInInfo -> Value
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TxInInfo -> TxOut
txInInfoResolved) (ScriptContext -> Maybe TxInInfo
findOwnInput ScriptContext
ptx)
        checkOk :: Bool
checkOk =
            BuiltinString -> Bool -> Bool
traceIfFalse BuiltinString
"S1" {-"State transition invalid - checks failed"-} (s -> i -> ScriptContext -> Bool
check s
DatumType (StateMachine s i)
currentState i
RedeemerType (StateMachine s i)
input ScriptContext
ptx)
            Bool -> Bool -> Bool
&& BuiltinString -> Bool -> Bool
traceIfFalse BuiltinString
"S2" {-"Thread token not found"-} (Maybe ThreadToken -> ValidatorHash -> Value -> Integer -> Bool
TT.checkThreadToken Maybe ThreadToken
threadToken (ScriptContext -> ValidatorHash
ownHash ScriptContext
ptx) Value
vl Integer
1)
        oldState :: State s
oldState = State :: forall s. s -> Value -> State s
State
            { stateData :: s
stateData = s
DatumType (StateMachine s i)
currentState
              -- The thread token value is hidden from the client code
            , stateValue :: Value
stateValue = Value
vl Value -> Value -> Value
forall a. Semigroup a => a -> a -> a
<> Value -> Value
forall a. Group a => a -> a
inv (Maybe ThreadToken -> ValidatorHash -> Value
threadTokenValueInner Maybe ThreadToken
threadToken (ScriptContext -> ValidatorHash
ownHash ScriptContext
ptx))
            }
        stateAndOutputsOk :: Bool
stateAndOutputsOk = case State s -> i -> Maybe (TxConstraints Void Void, State s)
step State s
oldState i
RedeemerType (StateMachine s i)
input of
            Just (TxConstraints Void Void
newConstraints, State{stateData :: forall s. State s -> s
stateData=s
newData, stateValue :: forall s. State s -> Value
stateValue=Value
newValue})
                | s -> Bool
isFinal s
newData ->
                    BuiltinString -> Bool -> Bool
traceIfFalse BuiltinString
"S3" {-"Non-zero value allocated in final state"-} (Value -> Bool
isZero Value
newValue)
                    Bool -> Bool -> Bool
&& BuiltinString -> Bool -> Bool
traceIfFalse BuiltinString
"S4" {-"State transition invalid - constraints not satisfied by ScriptContext"-} (TxConstraints Void Void -> ScriptContext -> Bool
forall i o.
(ToData i, ToData o) =>
TxConstraints i o -> ScriptContext -> Bool
checkScriptContext TxConstraints Void Void
newConstraints ScriptContext
ptx)
                | Bool
otherwise ->
                    let -- Check that the thread token value is still there
                        valueWithToken :: Value
valueWithToken = Value
newValue Value -> Value -> Value
forall a. Semigroup a => a -> a -> a
<> Maybe ThreadToken -> ValidatorHash -> Value
threadTokenValueInner Maybe ThreadToken
threadToken (ScriptContext -> ValidatorHash
ownHash ScriptContext
ptx)
                        -- Type annotation is required to compile validator when profiling is activated.
                        -- If 'Void' is not explicitly set, the plutus plugin can't handle the free type variable.
                        constraint :: TxConstraints Void s
constraint = s -> Value -> TxConstraints Void s
forall o i. o -> Value -> TxConstraints i o
mustPayToTheScriptWithInlineDatum @s @Void s
newData Value
valueWithToken
                        txc :: TxConstraints Void s
txc = TxConstraints Void Void
newConstraints { txOwnOutputs :: [ScriptOutputConstraint s]
txOwnOutputs = TxConstraints Void s -> [ScriptOutputConstraint s]
forall i o. TxConstraints i o -> [ScriptOutputConstraint o]
txOwnOutputs TxConstraints Void s
constraint }
                    in BuiltinString -> Bool -> Bool
traceIfFalse BuiltinString
"S5" {-"State transition invalid - constraints not satisfied by ScriptContext"-} (TxConstraints Void s -> ScriptContext -> Bool
forall i o.
(ToData i, ToData o) =>
TxConstraints i o -> ScriptContext -> Bool
checkScriptContext @_ @s TxConstraints Void s
txc ScriptContext
ptx)
            Maybe (TxConstraints Void Void, State s)
Nothing -> BuiltinString -> Bool -> Bool
forall a. BuiltinString -> a -> a
trace BuiltinString
"S6" {-"State transition invalid - input is not a valid transition at the current state"-} Bool
False
    in Bool
checkOk Bool -> Bool -> Bool
&& Bool
stateAndOutputsOk