{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}
-- The STS instance for UTXOW is technically an orphan.
{-# OPTIONS_GHC -Wno-orphans #-}

module Cardano.Ledger.ShelleyMA.Rules.Utxow where

import Cardano.Ledger.Compactible (Compactible (CompactForm))
import qualified Cardano.Ledger.Core as Core
import qualified Cardano.Ledger.Crypto as CryptoClass
import Cardano.Ledger.Era (Crypto)
import Cardano.Ledger.Mary.Value (PolicyID, Value, policies, policyID)
import Cardano.Ledger.Shelley.Constraints (ShelleyBased)
import Cardano.Ledger.ShelleyMA (MaryOrAllegra, ShelleyMAEra)
import Cardano.Ledger.ShelleyMA.AuxiliaryData ()
import Cardano.Ledger.ShelleyMA.Rules.Utxo ()
import Cardano.Ledger.ShelleyMA.TxBody ()
import Cardano.Ledger.Torsor (Torsor (..))
import Cardano.Ledger.Val (DecodeMint, DecodeNonNegative, Val)
import Control.State.Transition.Extended
import Data.Foldable (Foldable (toList))
import qualified Data.Map.Strict as Map
import qualified Data.Maybe as Maybe
import Data.Relation (Relation ((◁)))
import Data.Sequence.Strict (StrictSeq)
import Data.Set (Set)
import qualified Data.Set as Set
import Data.Typeable (Typeable)
import GHC.Records (HasField (..))
import Shelley.Spec.Ledger.BaseTypes
import Shelley.Spec.Ledger.Coin (Coin)
import Shelley.Spec.Ledger.Delegation.Certificates (requiresVKeyWitness)
import Shelley.Spec.Ledger.Keys (DSignable, Hash)
import Shelley.Spec.Ledger.LedgerState (UTxOState)
import Shelley.Spec.Ledger.STS.Utxo
import Shelley.Spec.Ledger.STS.Utxow
  ( UTXOW,
    UtxowPredicateFailure (..),
    initialLedgerStateUTXOW,
    utxoWitnessed,
  )
import Shelley.Spec.Ledger.Scripts (ScriptHash)
import Shelley.Spec.Ledger.Tx (Tx (_body))
import Shelley.Spec.Ledger.TxBody
  ( DCert,
    EraIndependentTxBody,
    RewardAcnt (getRwdCred),
    TxIn,
    TxOut (TxOut),
    Wdrl (unWdrl),
  )
import Shelley.Spec.Ledger.UTxO
  ( UTxO (UTxO),
    getScriptHash,
    scriptCred,
    scriptStakeCred,
    txinsScript,
  )

-- | We want to reuse the same rules for Mary and Allegra. This however relies
-- on being able to get a set of 'PolicyID's from the value. Since a 'Coin' has
-- no policies, we create a small class which returns a null set of 'PolicyID's
-- for 'Coin'.
--
-- This should not escape this module.
class GetPolicies a crypto where
  getPolicies :: a -> Set (PolicyID crypto)

instance GetPolicies Coin crypto where
  getPolicies :: Coin -> Set (PolicyID crypto)
getPolicies = Set (PolicyID crypto) -> Coin -> Set (PolicyID crypto)
forall a b. a -> b -> a
const Set (PolicyID crypto)
forall a. Set a
Set.empty

instance GetPolicies (Value crypto) crypto where
  getPolicies :: Value crypto -> Set (PolicyID crypto)
getPolicies = Value crypto -> Set (PolicyID crypto)
forall crypto. Value crypto -> Set (PolicyID crypto)
policies

-- | Computes the set of script hashes required to unlock the transaction inputs
-- and the withdrawals.
scriptsNeeded ::
  ( ShelleyBased era,
    GetPolicies (Core.Value era) (Crypto era),
    HasField "certs" (Core.TxBody era) (StrictSeq (DCert (Crypto era))),
    HasField "wdrls" (Core.TxBody era) (Wdrl (Crypto era)),
    HasField "inputs" (Core.TxBody era) (Set (TxIn (Crypto era))),
    HasField "mint" (Core.TxBody era) (Core.Value era)
  ) =>
  UTxO era ->
  Tx era ->
  Set (ScriptHash (Crypto era))
scriptsNeeded :: UTxO era -> Tx era -> Set (ScriptHash (Crypto era))
scriptsNeeded UTxO era
u Tx era
tx =
  [ScriptHash (Crypto era)] -> Set (ScriptHash (Crypto era))
forall a. Ord a => [a] -> Set a
Set.fromList (Map (TxIn (Crypto era)) (ScriptHash (Crypto era))
-> [ScriptHash (Crypto era)]
forall k a. Map k a -> [a]
Map.elems (Map (TxIn (Crypto era)) (ScriptHash (Crypto era))
 -> [ScriptHash (Crypto era)])
-> Map (TxIn (Crypto era)) (ScriptHash (Crypto era))
-> [ScriptHash (Crypto era)]
forall a b. (a -> b) -> a -> b
$ (TxOut era -> Maybe (ScriptHash (Crypto era)))
-> Map (TxIn (Crypto era)) (TxOut era)
-> Map (TxIn (Crypto era)) (ScriptHash (Crypto era))
forall a b k. (a -> Maybe b) -> Map k a -> Map k b
Map.mapMaybe (Addr (Crypto era) -> Maybe (ScriptHash (Crypto era))
forall crypto. Addr crypto -> Maybe (ScriptHash crypto)
getScriptHash (Addr (Crypto era) -> Maybe (ScriptHash (Crypto era)))
-> (TxOut era -> Addr (Crypto era))
-> TxOut era
-> Maybe (ScriptHash (Crypto era))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TxOut era -> Addr (Crypto era)
forall era.
(Torsor (Value era), DecodeNonNegative (Value era),
 Compactible (Value era), Val (Value era),
 HashAnnotated (TxBody era) era, FromCBOR (Delta (Value era)),
 FromCBOR (Value era), FromCBOR (CompactForm (Value era)),
 FromCBOR (Annotator (TxBody era)),
 FromCBOR (Annotator (Script era)),
 FromCBOR (Annotator (AuxiliaryData era)),
 ToCBOR (Delta (Value era)), ToCBOR (Value era),
 ToCBOR (TxBody era), ToCBOR (Script era),
 ToCBOR (AuxiliaryData era), ToCBOR (CompactForm (Value era)),
 Show (Delta (Value era)), Show (Value era), Show (TxBody era),
 Show (Script era), Show (AuxiliaryData era),
 Eq (Delta (Value era)), Eq (TxBody era), Eq (Script era),
 Eq (AuxiliaryData era), Eq (CompactForm (Value era)),
 NoThunks (Delta (Value era)), NoThunks (Value era),
 NoThunks (TxBody era), NoThunks (Script era),
 NoThunks (AuxiliaryData era),
 HashIndex (TxBody era) ~ EraIndependentTxBody) =>
TxOut era -> Addr (Crypto era)
unTxOut) Map (TxIn (Crypto era)) (TxOut era)
u'')
    Set (ScriptHash (Crypto era))
-> Set (ScriptHash (Crypto era)) -> Set (ScriptHash (Crypto era))
forall a. Ord a => Set a -> Set a -> Set a
`Set.union` [ScriptHash (Crypto era)] -> Set (ScriptHash (Crypto era))
forall a. Ord a => [a] -> Set a
Set.fromList
      ( (RewardAcnt (Crypto era) -> Maybe (ScriptHash (Crypto era)))
-> [RewardAcnt (Crypto era)] -> [ScriptHash (Crypto era)]
forall a b. (a -> Maybe b) -> [a] -> [b]
Maybe.mapMaybe (Credential 'Staking (Crypto era) -> Maybe (ScriptHash (Crypto era))
forall (kr :: KeyRole) crypto.
Credential kr crypto -> Maybe (ScriptHash crypto)
scriptCred (Credential 'Staking (Crypto era)
 -> Maybe (ScriptHash (Crypto era)))
-> (RewardAcnt (Crypto era) -> Credential 'Staking (Crypto era))
-> RewardAcnt (Crypto era)
-> Maybe (ScriptHash (Crypto era))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RewardAcnt (Crypto era) -> Credential 'Staking (Crypto era)
forall crypto. RewardAcnt crypto -> Credential 'Staking crypto
getRwdCred) ([RewardAcnt (Crypto era)] -> [ScriptHash (Crypto era)])
-> [RewardAcnt (Crypto era)] -> [ScriptHash (Crypto era)]
forall a b. (a -> b) -> a -> b
$
          Map (RewardAcnt (Crypto era)) Coin -> [RewardAcnt (Crypto era)]
forall k a. Map k a -> [k]
Map.keys Map (RewardAcnt (Crypto era)) Coin
withdrawals
      )
    Set (ScriptHash (Crypto era))
-> Set (ScriptHash (Crypto era)) -> Set (ScriptHash (Crypto era))
forall a. Ord a => Set a -> Set a -> Set a
`Set.union` [ScriptHash (Crypto era)] -> Set (ScriptHash (Crypto era))
forall a. Ord a => [a] -> Set a
Set.fromList
      ( (DCert (Crypto era) -> Maybe (ScriptHash (Crypto era)))
-> [DCert (Crypto era)] -> [ScriptHash (Crypto era)]
forall a b. (a -> Maybe b) -> [a] -> [b]
Maybe.mapMaybe
          DCert (Crypto era) -> Maybe (ScriptHash (Crypto era))
forall crypto. DCert crypto -> Maybe (ScriptHash crypto)
scriptStakeCred
          ((DCert (Crypto era) -> Bool)
-> [DCert (Crypto era)] -> [DCert (Crypto era)]
forall a. (a -> Bool) -> [a] -> [a]
filter DCert (Crypto era) -> Bool
forall crypto. DCert crypto -> Bool
requiresVKeyWitness [DCert (Crypto era)]
certificates)
      )
    Set (ScriptHash (Crypto era))
-> Set (ScriptHash (Crypto era)) -> Set (ScriptHash (Crypto era))
forall a. Ord a => Set a -> Set a -> Set a
`Set.union` ((PolicyID (Crypto era) -> ScriptHash (Crypto era)
forall crypto. PolicyID crypto -> ScriptHash crypto
policyID (PolicyID (Crypto era) -> ScriptHash (Crypto era))
-> Set (PolicyID (Crypto era)) -> Set (ScriptHash (Crypto era))
forall b a. Ord b => (a -> b) -> Set a -> Set b
`Set.map` (Value era -> Set (PolicyID (Crypto era))
forall a crypto. GetPolicies a crypto => a -> Set (PolicyID crypto)
getPolicies (Value era -> Set (PolicyID (Crypto era)))
-> Value era -> Set (PolicyID (Crypto era))
forall a b. (a -> b) -> a -> b
$ TxBody era -> Value era
forall k (x :: k) r a. HasField x r a => r -> a
getField @"mint" TxBody era
txb)))
  where
    txb :: TxBody era
txb = Tx era
-> (TxBodyConstraints era, ToCBOR (AuxiliaryData era)) =>
   TxBody era
forall era.
Tx era
-> (TxBodyConstraints era, ToCBOR (AuxiliaryData era)) =>
   TxBody era
_body Tx era
tx
    unTxOut :: TxOut era -> Addr (Crypto era)
unTxOut (TxOut Addr (Crypto era)
a Value era
_) = Addr (Crypto era)
a
    withdrawals :: Map (RewardAcnt (Crypto era)) Coin
withdrawals = Wdrl (Crypto era) -> Map (RewardAcnt (Crypto era)) Coin
forall crypto. Wdrl crypto -> Map (RewardAcnt crypto) Coin
unWdrl (Wdrl (Crypto era) -> Map (RewardAcnt (Crypto era)) Coin)
-> Wdrl (Crypto era) -> Map (RewardAcnt (Crypto era)) Coin
forall a b. (a -> b) -> a -> b
$ TxBody era -> Wdrl (Crypto era)
forall k (x :: k) r a. HasField x r a => r -> a
getField @"wdrls" TxBody era
txb
    UTxO Map (TxIn (Crypto era)) (TxOut era)
u'' = (Set (TxIn (Crypto era)) -> UTxO era -> Set (TxIn (Crypto era))
forall era.
ShelleyBased era =>
Set (TxIn (Crypto era)) -> UTxO era -> Set (TxIn (Crypto era))
txinsScript (TxBody era -> Set (TxIn (Crypto era))
forall k (x :: k) r a. HasField x r a => r -> a
getField @"inputs" TxBody era
txb) UTxO era
u) Set (Domain (UTxO era)) -> UTxO era -> UTxO era
forall m. (Relation m, Ord (Domain m)) => Set (Domain m) -> m -> m
 UTxO era
u
    certificates :: [DCert (Crypto era)]
certificates = (StrictSeq (DCert (Crypto era)) -> [DCert (Crypto era)]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList (StrictSeq (DCert (Crypto era)) -> [DCert (Crypto era)])
-> (TxBody era -> StrictSeq (DCert (Crypto era)))
-> TxBody era
-> [DCert (Crypto era)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k (x :: k) r a. HasField x r a => r -> a
forall r a. HasField "certs" r a => r -> a
getField @"certs") TxBody era
txb

--------------------------------------------------------------------------------
-- UTXOW STS
--------------------------------------------------------------------------------

instance
  forall c (ma :: MaryOrAllegra).
  ( CryptoClass.Crypto c,
    Typeable ma,
    STS (UTXO (ShelleyMAEra ma c)),
    BaseM (UTXO (ShelleyMAEra ma c)) ~ ShelleyBase,
    DecodeMint (Core.Value (ShelleyMAEra ma c)),
    DecodeNonNegative (Core.Value (ShelleyMAEra ma c)),
    Compactible (Core.Value (ShelleyMAEra ma c)),
    Val (Core.Value (ShelleyMAEra ma c)),
    GetPolicies (Core.Value (ShelleyMAEra ma c)) c,
    Eq (CompactForm (Core.Value (ShelleyMAEra ma c))),
    Core.ChainData (Core.Value (ShelleyMAEra ma c)),
    Core.ChainData (Delta (Core.Value (ShelleyMAEra ma c))),
    Core.SerialisableData (Core.Value (ShelleyMAEra ma c)),
    Core.SerialisableData (Delta (Core.Value (ShelleyMAEra ma c))),
    Core.SerialisableData (CompactForm (Core.Value (ShelleyMAEra ma c))),
    Torsor (Core.Value (ShelleyMAEra ma c)),
    DSignable c (Hash c EraIndependentTxBody)
  ) =>
  STS (UTXOW (ShelleyMAEra ma c))
  where
  type State (UTXOW (ShelleyMAEra ma c)) = UTxOState (ShelleyMAEra ma c)
  type Signal (UTXOW (ShelleyMAEra ma c)) = Tx (ShelleyMAEra ma c)
  type Environment (UTXOW (ShelleyMAEra ma c)) = UtxoEnv (ShelleyMAEra ma c)
  type BaseM (UTXOW (ShelleyMAEra ma c)) = ShelleyBase
  type
    PredicateFailure (UTXOW (ShelleyMAEra ma c)) =
      UtxowPredicateFailure (ShelleyMAEra ma c)
  transitionRules :: [TransitionRule (UTXOW (ShelleyMAEra ma c))]
transitionRules = [(UTxO (ShelleyMAEra ma c)
 -> Tx (ShelleyMAEra ma c)
 -> Set (ScriptHash (Crypto (ShelleyMAEra ma c))))
-> TransitionRule (UTXOW (ShelleyMAEra ma c))
forall era.
(ShelleyBased era, ValidateScript era, ValidateAuxiliaryData era,
 STS (UTXOW era), BaseM (UTXOW era) ~ ShelleyBase,
 Embed (UTXO era) (UTXOW era),
 DSignable (Crypto era) (Hash (Crypto era) EraIndependentTxBody),
 Environment (UTXO era) ~ UtxoEnv era,
 State (UTXO era) ~ UTxOState era, Signal (UTXO era) ~ Tx era,
 Environment (UTXOW era) ~ UtxoEnv era,
 State (UTXOW era) ~ UTxOState era, Signal (UTXOW era) ~ Tx era,
 PredicateFailure (UTXOW era) ~ UtxowPredicateFailure era,
 HasField "inputs" (TxBody era) (Set (TxIn (Crypto era))),
 HasField "wdrls" (TxBody era) (Wdrl (Crypto era)),
 HasField "certs" (TxBody era) (StrictSeq (DCert (Crypto era))),
 HasField
   "adHash"
   (TxBody era)
   (StrictMaybe (AuxiliaryDataHash (Crypto era))),
 HasField "update" (TxBody era) (StrictMaybe (Update era))) =>
(UTxO era -> Tx era -> Set (ScriptHash (Crypto era)))
-> TransitionRule (UTXOW era)
utxoWitnessed UTxO (ShelleyMAEra ma c)
-> Tx (ShelleyMAEra ma c)
-> Set (ScriptHash (Crypto (ShelleyMAEra ma c)))
forall era.
(ShelleyBased era, GetPolicies (Value era) (Crypto era),
 HasField "certs" (TxBody era) (StrictSeq (DCert (Crypto era))),
 HasField "wdrls" (TxBody era) (Wdrl (Crypto era)),
 HasField "inputs" (TxBody era) (Set (TxIn (Crypto era))),
 HasField "mint" (TxBody era) (Value era)) =>
UTxO era -> Tx era -> Set (ScriptHash (Crypto era))
scriptsNeeded]
  initialRules :: [InitialRule (UTXOW (ShelleyMAEra ma c))]
initialRules = [InitialRule (UTXOW (ShelleyMAEra ma c))
forall era.
(Embed (UTXO era) (UTXOW era),
 Environment (UTXOW era) ~ UtxoEnv era,
 State (UTXOW era) ~ UTxOState era,
 Environment (UTXO era) ~ UtxoEnv era,
 State (UTXO era) ~ UTxOState era) =>
InitialRule (UTXOW era)
initialLedgerStateUTXOW]

instance
  ( CryptoClass.Crypto c,
    STS (UTXO (ShelleyMAEra ma c)),
    BaseM (UTXO (ShelleyMAEra ma c)) ~ ShelleyBase
  ) =>
  Embed (UTXO (ShelleyMAEra ma c)) (UTXOW (ShelleyMAEra ma c))
  where
  wrapFailed :: PredicateFailure (UTXO (ShelleyMAEra ma c))
-> PredicateFailure (UTXOW (ShelleyMAEra ma c))
wrapFailed = PredicateFailure (UTXO (ShelleyMAEra ma c))
-> PredicateFailure (UTXOW (ShelleyMAEra ma c))
forall era.
PredicateFailure (UTXO era) -> UtxowPredicateFailure era
UtxoFailure