{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -Wno-orphans #-}

module Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Utxow () where

import Cardano.Ledger.Conway (ConwayEra)
import Cardano.Ledger.Conway.Core (EraTx (..), txStAnnTxG)
import Cardano.Ledger.Conway.UTxO (getConwayWitsVKeyNeeded)
import Cardano.Ledger.Shelley.LedgerState (UTxOState (..))
import Cardano.Ledger.Shelley.Rules (utxoEnvCertStateL)
import Control.State.Transition.Extended (TRC (..))
import Data.Bifunctor (Bifunctor (..))
import Data.Coerce (coerce)
import qualified Data.Text as T
import Lens.Micro ((^.))
import Lens.Micro.Extras (view)
import qualified MAlonzo.Code.Ledger.Conway.Foreign.API as Agda
import qualified Prettyprinter as PP
import Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Base (externalFunctions)
import Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Utxo ()
import Test.Cardano.Ledger.Conformance.ExecSpecRule.Core (
  ExecSpecRule (..),
  SpecTRC (..),
  runFromAgdaFunction,
 )
import Test.Cardano.Ledger.Conformance.SpecTranslate.Base (
  SpecTranslate (..),
  runSpecTransM,
  withCtxSpecTransM,
  withSpecTransM,
 )
import Test.Cardano.Ledger.Constrained.Conway (
  UtxoExecContext (..),
 )
import Test.Cardano.Ledger.Conway.TreeDiff (showExpr)
import Test.Cardano.Ledger.Shelley.Utils (runSTS)

instance ExecSpecRule "UTXOW" ConwayEra where
  type ExecContext "UTXOW" ConwayEra = UtxoExecContext ConwayEra

  translateInputs :: HasCallStack =>
TRC (EraRule "UTXOW" ConwayEra)
-> SpecTransM
     ConwayEra
     (ExecContext "UTXOW" ConwayEra)
     (SpecTRC "UTXOW" ConwayEra)
translateInputs (TRC (Environment (EraRule "UTXOW" ConwayEra)
env, State (EraRule "UTXOW" ConwayEra)
st, Signal (EraRule "UTXOW" ConwayEra)
sig)) = do
    agdaEnv <- ()
-> SpecTransM ConwayEra () (SpecRep ConwayEra (UtxoEnv ConwayEra))
-> SpecTransM
     ConwayEra
     (UtxoExecContext ConwayEra)
     (SpecRep ConwayEra (UtxoEnv ConwayEra))
forall ctx era a ctx'.
ctx -> SpecTransM era ctx a -> SpecTransM era ctx' a
withCtxSpecTransM () (SpecTransM ConwayEra () (SpecRep ConwayEra (UtxoEnv ConwayEra))
 -> SpecTransM
      ConwayEra
      (UtxoExecContext ConwayEra)
      (SpecRep ConwayEra (UtxoEnv ConwayEra)))
-> SpecTransM ConwayEra () (SpecRep ConwayEra (UtxoEnv ConwayEra))
-> SpecTransM
     ConwayEra
     (UtxoExecContext ConwayEra)
     (SpecRep ConwayEra (UtxoEnv ConwayEra))
forall a b. (a -> b) -> a -> b
$ UtxoEnv ConwayEra
-> SpecTransM
     ConwayEra
     (SpecContext ConwayEra (UtxoEnv ConwayEra))
     (SpecRep ConwayEra (UtxoEnv ConwayEra))
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep UtxoEnv ConwayEra
Environment (EraRule "UTXOW" ConwayEra)
env
    agdaSt <- withSpecTransM (view utxoEnvCertStateL . uecUtxoEnv) $ toSpecRep st
    agdaSig <- withCtxSpecTransM () $ toSpecRep sig
    pure $ SpecTRC agdaEnv agdaSt agdaSig

  translateOutput :: TRC (EraRule "UTXOW" ConwayEra)
-> State (EraRule "UTXOW" ConwayEra)
-> SpecTransM
     ConwayEra
     (ExecContext "UTXOW" ConwayEra)
     (SpecState "UTXOW" ConwayEra)
translateOutput TRC (EraRule "UTXOW" ConwayEra)
_ =
    (UtxoExecContext ConwayEra -> ConwayCertState ConwayEra)
-> SpecTransM ConwayEra (ConwayCertState ConwayEra) UTxOState
-> SpecTransM ConwayEra (UtxoExecContext ConwayEra) UTxOState
forall ctx ctx' era a.
(ctx -> ctx') -> SpecTransM era ctx' a -> SpecTransM era ctx a
withSpecTransM (Getting
  (ConwayCertState ConwayEra)
  (UtxoEnv ConwayEra)
  (ConwayCertState ConwayEra)
-> UtxoEnv ConwayEra -> ConwayCertState ConwayEra
forall a s. Getting a s a -> s -> a
view (CertState ConwayEra
 -> Const (ConwayCertState ConwayEra) (CertState ConwayEra))
-> UtxoEnv ConwayEra
-> Const (ConwayCertState ConwayEra) (UtxoEnv ConwayEra)
Getting
  (ConwayCertState ConwayEra)
  (UtxoEnv ConwayEra)
  (ConwayCertState ConwayEra)
forall era (f :: * -> *).
Functor f =>
(CertState era -> f (CertState era))
-> UtxoEnv era -> f (UtxoEnv era)
utxoEnvCertStateL (UtxoEnv ConwayEra -> ConwayCertState ConwayEra)
-> (UtxoExecContext ConwayEra -> UtxoEnv ConwayEra)
-> UtxoExecContext ConwayEra
-> ConwayCertState ConwayEra
forall b c a. (b -> c) -> (a -> b) -> a -> c
. UtxoExecContext ConwayEra -> UtxoEnv ConwayEra
forall era. UtxoExecContext era -> UtxoEnv era
uecUtxoEnv) (SpecTransM ConwayEra (ConwayCertState ConwayEra) UTxOState
 -> SpecTransM ConwayEra (UtxoExecContext ConwayEra) UTxOState)
-> (UTxOState ConwayEra
    -> SpecTransM ConwayEra (ConwayCertState ConwayEra) UTxOState)
-> UTxOState ConwayEra
-> SpecTransM ConwayEra (UtxoExecContext ConwayEra) UTxOState
forall b c a. (b -> c) -> (a -> b) -> a -> c
. UTxOState ConwayEra
-> SpecTransM ConwayEra (ConwayCertState ConwayEra) UTxOState
UTxOState ConwayEra
-> SpecTransM
     ConwayEra
     (SpecContext ConwayEra (UTxOState ConwayEra))
     (SpecRep ConwayEra (UTxOState ConwayEra))
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep

  runAgdaRule :: HasCallStack =>
SpecTRC "UTXOW" ConwayEra
-> Either Text (SpecState "UTXOW" ConwayEra)
runAgdaRule = (SpecEnvironment "UTXOW" ConwayEra
 -> SpecState "UTXOW" ConwayEra
 -> SpecSignal "UTXOW" ConwayEra
 -> ComputationResult Text (SpecState "UTXOW" ConwayEra))
-> SpecTRC "UTXOW" ConwayEra
-> Either Text (SpecState "UTXOW" ConwayEra)
forall (rule :: Symbol) era.
(SpecEnvironment rule era
 -> SpecState rule era
 -> SpecSignal rule era
 -> ComputationResult Text (SpecState rule era))
-> SpecTRC rule era -> Either Text (SpecState rule era)
runFromAgdaFunction (T_ExternalFunctions_8
-> UTxOEnv
-> UTxOState
-> Tx
-> T_HSComputationResult_110 Text UTxOState
Agda.utxowStep T_ExternalFunctions_8
externalFunctions)

  extraInfo :: HasCallStack =>
Globals
-> ExecContext "UTXOW" ConwayEra
-> TRC (EraRule "UTXOW" ConwayEra)
-> Either
     Text
     (State (EraRule "UTXOW" ConwayEra),
      [Event (EraRule "UTXOW" ConwayEra)])
-> Doc AnsiStyle
extraInfo Globals
globals ExecContext "UTXOW" ConwayEra
ctx trc :: TRC (EraRule "UTXOW" ConwayEra)
trc@(TRC (Environment (EraRule "UTXOW" ConwayEra)
env, State (EraRule "UTXOW" ConwayEra)
st, Signal (EraRule "UTXOW" ConwayEra)
sig)) Either
  Text
  (State (EraRule "UTXOW" ConwayEra),
   [Event (EraRule "UTXOW" ConwayEra)])
_ =
    let
      result :: String
result = (Text -> String) -> (Text -> String) -> Either Text Text -> String
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either Text -> String
forall a. Show a => a -> String
show Text -> String
T.unpack (Either Text Text -> String) -> Either Text Text -> String
forall a b. (a -> b) -> a -> b
$ do
        agdaEnv <- () -> SpecTransM ConwayEra () UTxOEnv -> Either Text UTxOEnv
forall era ctx a. ctx -> SpecTransM era ctx a -> Either Text a
runSpecTransM () (SpecTransM ConwayEra () UTxOEnv -> Either Text UTxOEnv)
-> SpecTransM ConwayEra () UTxOEnv -> Either Text UTxOEnv
forall a b. (a -> b) -> a -> b
$ forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep @ConwayEra UtxoEnv ConwayEra
Environment (EraRule "UTXOW" ConwayEra)
env
        agdaSt <- runSpecTransM (uecUtxoEnv ctx ^. utxoEnvCertStateL) $ toSpecRep @ConwayEra st
        agdaSig <- runSpecTransM () $ toSpecRep @ConwayEra sig
        pure $ Agda.utxowDebug externalFunctions agdaEnv agdaSt agdaSig
      stFinal :: Either
  Text
  (State (EraRule "UTXO" ConwayEra),
   [Event (EraRule "UTXO" ConwayEra)])
stFinal = (NonEmpty (PredicateFailure (EraRule "UTXO" ConwayEra)) -> Text)
-> Either
     (NonEmpty (PredicateFailure (EraRule "UTXO" ConwayEra)))
     (State (EraRule "UTXO" ConwayEra),
      [Event (EraRule "UTXO" ConwayEra)])
-> Either
     Text
     (State (EraRule "UTXO" ConwayEra),
      [Event (EraRule "UTXO" ConwayEra)])
forall a b c. (a -> b) -> Either a c -> Either b c
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first (String -> Text
T.pack (String -> Text)
-> (NonEmpty (ConwayUtxoPredFailure ConwayEra) -> String)
-> NonEmpty (ConwayUtxoPredFailure ConwayEra)
-> Text
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NonEmpty (ConwayUtxoPredFailure ConwayEra) -> String
forall a. Show a => a -> String
show) (Either
   (NonEmpty (PredicateFailure (EraRule "UTXO" ConwayEra)))
   (State (EraRule "UTXO" ConwayEra),
    [Event (EraRule "UTXO" ConwayEra)])
 -> Either
      Text
      (State (EraRule "UTXO" ConwayEra),
       [Event (EraRule "UTXO" ConwayEra)]))
-> Either
     (NonEmpty (PredicateFailure (EraRule "UTXO" ConwayEra)))
     (State (EraRule "UTXO" ConwayEra),
      [Event (EraRule "UTXO" ConwayEra)])
-> Either
     Text
     (State (EraRule "UTXO" ConwayEra),
      [Event (EraRule "UTXO" ConwayEra)])
forall a b. (a -> b) -> a -> b
$ forall (rule :: Symbol) era.
(BaseM (EraRule rule era) ~ ShelleyBase, STS (EraRule rule era)) =>
Globals
-> Environment (EraRule rule era)
-> State (EraRule rule era)
-> Signal (EraRule rule era)
-> Either
     (NonEmpty (PredicateFailure (EraRule rule era)))
     (State (EraRule rule era), [Event (EraRule rule era)])
runSTS @"UTXO" @ConwayEra Globals
globals Environment (EraRule "UTXO" ConwayEra)
Environment (EraRule "UTXOW" ConwayEra)
env State (EraRule "UTXO" ConwayEra)
State (EraRule "UTXOW" ConwayEra)
st Signal (EraRule "UTXO" ConwayEra)
Signal (EraRule "UTXOW" ConwayEra)
sig
      utxoInfo :: Doc AnsiStyle
utxoInfo = forall (rule :: Symbol) era.
(ExecSpecRule rule era, HasCallStack) =>
Globals
-> ExecContext rule era
-> TRC (EraRule rule era)
-> Either
     Text (State (EraRule rule era), [Event (EraRule rule era)])
-> Doc AnsiStyle
extraInfo @"UTXO" @ConwayEra Globals
globals ExecContext "UTXO" ConwayEra
ExecContext "UTXOW" ConwayEra
ctx (TRC (ConwayUTXOW ConwayEra) -> TRC (ConwayUTXO ConwayEra)
forall a b. Coercible a b => a -> b
coerce TRC (EraRule "UTXOW" ConwayEra)
TRC (ConwayUTXOW ConwayEra)
trc) Either
  Text
  (State (EraRule "UTXO" ConwayEra),
   [Event (EraRule "UTXO" ConwayEra)])
stFinal
     in
      [Doc AnsiStyle] -> Doc AnsiStyle
forall ann. [Doc ann] -> Doc ann
PP.vcat
        [ Doc AnsiStyle
"UTXOW"
        , Doc AnsiStyle
"Impl:"
        , Doc AnsiStyle
"witsVKeyNeeded"
        , String -> Doc AnsiStyle
forall ann. String -> Doc ann
forall a ann. Pretty a => a -> Doc ann
PP.pretty (String -> Doc AnsiStyle)
-> (Set (KeyHash Witness) -> String)
-> Set (KeyHash Witness)
-> Doc AnsiStyle
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set (KeyHash Witness) -> String
forall a. ToExpr a => a -> String
showExpr (Set (KeyHash Witness) -> Doc AnsiStyle)
-> Set (KeyHash Witness) -> Doc AnsiStyle
forall a b. (a -> b) -> a -> b
$
            forall era (l :: TxLevel).
(EraTx era, ConwayEraTxBody era) =>
UTxO era -> TxBody l era -> Set (KeyHash Witness)
getConwayWitsVKeyNeeded @ConwayEra (UTxOState ConwayEra -> UTxO ConwayEra
forall era. UTxOState era -> UTxO era
utxosUtxo State (EraRule "UTXOW" ConwayEra)
UTxOState ConwayEra
st) (AlonzoStAnnTx TopTx ConwayEra
Signal (EraRule "UTXOW" ConwayEra)
sig AlonzoStAnnTx TopTx ConwayEra
-> Getting
     (TxBody TopTx ConwayEra)
     (AlonzoStAnnTx TopTx ConwayEra)
     (TxBody TopTx ConwayEra)
-> TxBody TopTx ConwayEra
forall s a. s -> Getting a s a -> a
^. Getting
  (TxBody TopTx ConwayEra)
  (StAnnTx TopTx ConwayEra)
  (Tx TopTx ConwayEra)
(Tx TopTx ConwayEra
 -> Const (TxBody TopTx ConwayEra) (Tx TopTx ConwayEra))
-> AlonzoStAnnTx TopTx ConwayEra
-> Const (TxBody TopTx ConwayEra) (AlonzoStAnnTx TopTx ConwayEra)
forall era (l :: TxLevel).
EraTx era =>
SimpleGetter (StAnnTx l era) (Tx l era)
forall (l :: TxLevel).
SimpleGetter (StAnnTx l ConwayEra) (Tx l ConwayEra)
txStAnnTxG ((Tx TopTx ConwayEra
  -> Const (TxBody TopTx ConwayEra) (Tx TopTx ConwayEra))
 -> AlonzoStAnnTx TopTx ConwayEra
 -> Const (TxBody TopTx ConwayEra) (AlonzoStAnnTx TopTx ConwayEra))
-> ((TxBody TopTx ConwayEra
     -> Const (TxBody TopTx ConwayEra) (TxBody TopTx ConwayEra))
    -> Tx TopTx ConwayEra
    -> Const (TxBody TopTx ConwayEra) (Tx TopTx ConwayEra))
-> Getting
     (TxBody TopTx ConwayEra)
     (AlonzoStAnnTx TopTx ConwayEra)
     (TxBody TopTx ConwayEra)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (TxBody TopTx ConwayEra
 -> Const (TxBody TopTx ConwayEra) (TxBody TopTx ConwayEra))
-> Tx TopTx ConwayEra
-> Const (TxBody TopTx ConwayEra) (Tx TopTx ConwayEra)
forall era (l :: TxLevel).
EraTx era =>
Lens' (Tx l era) (TxBody l era)
forall (l :: TxLevel). Lens' (Tx l ConwayEra) (TxBody l ConwayEra)
bodyTxL)
        , Doc AnsiStyle
"witsVKeyHashes"
        , Doc AnsiStyle
"Spec:"
        , String -> Doc AnsiStyle
forall ann. String -> Doc ann
forall a ann. Pretty a => a -> Doc ann
PP.pretty String
result
        , Doc AnsiStyle
forall a. Monoid a => a
mempty
        , Doc AnsiStyle
"UTXO"
        , Doc AnsiStyle
utxoInfo
        ]