{-# 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.TxCert (ConwayTxCert)
import Cardano.Ledger.Conway.UTxO (getConwayWitsVKeyNeeded)
import Cardano.Ledger.Core (EraTx (..))
import Cardano.Ledger.Shelley.LedgerState (UTxOState (..))
import Data.Bifunctor (Bifunctor (..))
import qualified Data.Text as T
import Lens.Micro ((^.))
import qualified MAlonzo.Code.Ledger.Foreign.API as Agda
import qualified Prettyprinter as PP
import Test.Cardano.Ledger.Conformance (
  ExecSpecRule (..),
  SpecTranslate,
  runSpecTransM,
  showOpaqueErrorString,
  toSpecRep,
  unComputationResult,
 )
import Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Base (externalFunctions)
import Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Utxo (genUtxoExecContext)
import Test.Cardano.Ledger.Conformance.SpecTranslate.Conway.Base (
  ConwayTxBodyTransContext,
 )
import Test.Cardano.Ledger.Conformance.SpecTranslate.Conway.Utxow ()
import Test.Cardano.Ledger.Constrained.Conway (
  UtxoExecContext,
  utxoEnvSpec,
  utxoStateSpec,
  utxoTxSpec,
 )
import qualified Test.Cardano.Ledger.Generic.PrettyCore as PP
import Test.Cardano.Ledger.Shelley.Utils (runSTS)
import Test.Cardano.Ledger.TreeDiff (showExpr)

instance
  SpecTranslate ConwayTxBodyTransContext (ConwayTxCert ConwayEra) =>
  ExecSpecRule "UTXOW" ConwayEra
  where
  type ExecContext "UTXOW" ConwayEra = UtxoExecContext ConwayEra

  genExecContext :: HasCallStack => Gen (ExecContext "UTXOW" ConwayEra)
genExecContext = Gen (UtxoExecContext ConwayEra)
Gen (ExecContext "UTXOW" ConwayEra)
genUtxoExecContext
  environmentSpec :: HasCallStack =>
ExecContext "UTXOW" ConwayEra
-> Specification (ExecEnvironment "UTXOW" ConwayEra)
environmentSpec = UtxoExecContext ConwayEra -> Specification (UtxoEnv ConwayEra)
ExecContext "UTXOW" ConwayEra
-> Specification (ExecEnvironment "UTXOW" ConwayEra)
utxoEnvSpec
  stateSpec :: HasCallStack =>
ExecContext "UTXOW" ConwayEra
-> ExecEnvironment "UTXOW" ConwayEra
-> Specification (ExecState "UTXOW" ConwayEra)
stateSpec = UtxoExecContext ConwayEra
-> UtxoEnv ConwayEra -> Specification (UTxOState ConwayEra)
ExecContext "UTXOW" ConwayEra
-> ExecEnvironment "UTXOW" ConwayEra
-> Specification (ExecState "UTXOW" ConwayEra)
utxoStateSpec
  signalSpec :: HasCallStack =>
ExecContext "UTXOW" ConwayEra
-> ExecEnvironment "UTXOW" ConwayEra
-> ExecState "UTXOW" ConwayEra
-> Specification (ExecSignal "UTXOW" ConwayEra)
signalSpec ExecContext "UTXOW" ConwayEra
ctx ExecEnvironment "UTXOW" ConwayEra
_ ExecState "UTXOW" ConwayEra
_ = UtxoExecContext ConwayEra -> Specification (AlonzoTx ConwayEra)
forall era.
HasSpec (AlonzoTx era) =>
UtxoExecContext era -> Specification (AlonzoTx era)
utxoTxSpec UtxoExecContext ConwayEra
ExecContext "UTXOW" ConwayEra
ctx
  runAgdaRule :: HasCallStack =>
SpecRep (ExecEnvironment "UTXOW" ConwayEra)
-> SpecRep (ExecState "UTXOW" ConwayEra)
-> SpecRep (ExecSignal "UTXOW" ConwayEra)
-> Either OpaqueErrorString (SpecRep (ExecState "UTXOW" ConwayEra))
runAgdaRule SpecRep (ExecEnvironment "UTXOW" ConwayEra)
env SpecRep (ExecState "UTXOW" ConwayEra)
st SpecRep (ExecSignal "UTXOW" ConwayEra)
sig =
    ComputationResult Text UTxOState
-> Either OpaqueErrorString UTxOState
forall a. ComputationResult Text a -> Either OpaqueErrorString a
unComputationResult (ComputationResult Text UTxOState
 -> Either OpaqueErrorString UTxOState)
-> ComputationResult Text UTxOState
-> Either OpaqueErrorString UTxOState
forall a b. (a -> b) -> a -> b
$ T_ExternalFunctions_8
-> UTxOEnv -> UTxOState -> Tx -> ComputationResult Text UTxOState
Agda.utxowStep T_ExternalFunctions_8
externalFunctions UTxOEnv
SpecRep (ExecEnvironment "UTXOW" ConwayEra)
env UTxOState
SpecRep (ExecState "UTXOW" ConwayEra)
st Tx
SpecRep (ExecSignal "UTXOW" ConwayEra)
sig
  extraInfo :: HasCallStack =>
Globals
-> ExecContext "UTXOW" ConwayEra
-> Environment (EraRule "UTXOW" ConwayEra)
-> State (EraRule "UTXOW" ConwayEra)
-> Signal (EraRule "UTXOW" ConwayEra)
-> Either
     OpaqueErrorString
     (State (EraRule "UTXOW" ConwayEra),
      [Event (EraRule "UTXOW" ConwayEra)])
-> Doc AnsiStyle
extraInfo Globals
globals ExecContext "UTXOW" ConwayEra
ctx Environment (EraRule "UTXOW" ConwayEra)
env State (EraRule "UTXOW" ConwayEra)
st Signal (EraRule "UTXOW" ConwayEra)
sig Either
  OpaqueErrorString
  (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)
-> (SpecTransM (UtxoExecContext ConwayEra) Text
    -> Either Text Text)
-> SpecTransM (UtxoExecContext ConwayEra) Text
-> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. UtxoExecContext ConwayEra
-> SpecTransM (UtxoExecContext ConwayEra) Text -> Either Text Text
forall ctx a. ctx -> SpecTransM ctx a -> Either Text a
runSpecTransM UtxoExecContext ConwayEra
ExecContext "UTXOW" ConwayEra
ctx (SpecTransM (UtxoExecContext ConwayEra) Text -> String)
-> SpecTransM (UtxoExecContext ConwayEra) Text -> String
forall a b. (a -> b) -> a -> b
$
          T_ExternalFunctions_8 -> UTxOEnv -> UTxOState -> Tx -> Text
Agda.utxowDebug T_ExternalFunctions_8
externalFunctions
            (UTxOEnv -> UTxOState -> Tx -> Text)
-> SpecTransM (UtxoExecContext ConwayEra) UTxOEnv
-> SpecTransM (UtxoExecContext ConwayEra) (UTxOState -> Tx -> Text)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> UtxoEnv ConwayEra
-> SpecTransM
     (UtxoExecContext ConwayEra) (SpecRep (UtxoEnv ConwayEra))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep UtxoEnv ConwayEra
Environment (EraRule "UTXOW" ConwayEra)
env
            SpecTransM (UtxoExecContext ConwayEra) (UTxOState -> Tx -> Text)
-> SpecTransM (UtxoExecContext ConwayEra) UTxOState
-> SpecTransM (UtxoExecContext ConwayEra) (Tx -> Text)
forall a b.
SpecTransM (UtxoExecContext ConwayEra) (a -> b)
-> SpecTransM (UtxoExecContext ConwayEra) a
-> SpecTransM (UtxoExecContext ConwayEra) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> UTxOState ConwayEra
-> SpecTransM
     (UtxoExecContext ConwayEra) (SpecRep (UTxOState ConwayEra))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep State (EraRule "UTXOW" ConwayEra)
UTxOState ConwayEra
st
            SpecTransM (UtxoExecContext ConwayEra) (Tx -> Text)
-> SpecTransM (UtxoExecContext ConwayEra) Tx
-> SpecTransM (UtxoExecContext ConwayEra) Text
forall a b.
SpecTransM (UtxoExecContext ConwayEra) (a -> b)
-> SpecTransM (UtxoExecContext ConwayEra) a
-> SpecTransM (UtxoExecContext ConwayEra) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> AlonzoTx ConwayEra
-> SpecTransM
     (UtxoExecContext ConwayEra) (SpecRep (AlonzoTx ConwayEra))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep AlonzoTx ConwayEra
Signal (EraRule "UTXOW" ConwayEra)
sig
      stFinal :: Either
  OpaqueErrorString
  (State (EraRule "UTXO" ConwayEra),
   [Event (EraRule "UTXO" ConwayEra)])
stFinal = (NonEmpty (PredicateFailure (EraRule "UTXO" ConwayEra))
 -> OpaqueErrorString)
-> Either
     (NonEmpty (PredicateFailure (EraRule "UTXO" ConwayEra)))
     (State (EraRule "UTXO" ConwayEra),
      [Event (EraRule "UTXO" ConwayEra)])
-> Either
     OpaqueErrorString
     (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 NonEmpty (PredicateFailure (EraRule "UTXO" ConwayEra))
-> OpaqueErrorString
NonEmpty (ConwayUtxoPredFailure ConwayEra) -> OpaqueErrorString
forall a. ToExpr a => a -> OpaqueErrorString
showOpaqueErrorString (Either
   (NonEmpty (PredicateFailure (EraRule "UTXO" ConwayEra)))
   (State (EraRule "UTXO" ConwayEra),
    [Event (EraRule "UTXO" ConwayEra)])
 -> Either
      OpaqueErrorString
      (State (EraRule "UTXO" ConwayEra),
       [Event (EraRule "UTXO" ConwayEra)]))
-> Either
     (NonEmpty (PredicateFailure (EraRule "UTXO" ConwayEra)))
     (State (EraRule "UTXO" ConwayEra),
      [Event (EraRule "UTXO" ConwayEra)])
-> Either
     OpaqueErrorString
     (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
-> Environment (EraRule rule era)
-> State (EraRule rule era)
-> Signal (EraRule rule era)
-> Either
     OpaqueErrorString
     (State (EraRule rule era), [Event (EraRule rule era)])
-> Doc AnsiStyle
extraInfo @"UTXO" @ConwayEra Globals
globals ExecContext "UTXO" ConwayEra
ExecContext "UTXOW" ConwayEra
ctx 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 Either
  OpaqueErrorString
  (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 a. String -> Doc a
PP.ppString (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.
(EraTx era, ConwayEraTxBody era) =>
UTxO era -> TxBody era -> Set (KeyHash 'Witness)
getConwayWitsVKeyNeeded @ConwayEra (UTxOState ConwayEra -> UTxO ConwayEra
forall era. UTxOState era -> UTxO era
utxosUtxo State (EraRule "UTXOW" ConwayEra)
UTxOState ConwayEra
st) (AlonzoTx ConwayEra
Signal (EraRule "UTXOW" ConwayEra)
sig AlonzoTx ConwayEra
-> Getting
     (TxBody ConwayEra) (AlonzoTx ConwayEra) (TxBody ConwayEra)
-> TxBody ConwayEra
forall s a. s -> Getting a s a -> a
^. (TxBody ConwayEra -> Const (TxBody ConwayEra) (TxBody ConwayEra))
-> Tx ConwayEra -> Const (TxBody ConwayEra) (Tx ConwayEra)
Getting (TxBody ConwayEra) (AlonzoTx ConwayEra) (TxBody ConwayEra)
forall era. EraTx era => Lens' (Tx era) (TxBody era)
Lens' (Tx ConwayEra) (TxBody ConwayEra)
bodyTxL)
        , Doc AnsiStyle
"witsVKeyHashes"
        , Doc AnsiStyle
"Spec:"
        , String -> Doc AnsiStyle
forall a. String -> Doc a
PP.ppString String
result
        , Doc AnsiStyle
forall a. Monoid a => a
mempty
        , Doc AnsiStyle
"UTXO"
        , Doc AnsiStyle
utxoInfo
        ]