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

module Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Utxo (
  genUtxoExecContext,
) where

import Cardano.Ledger.BaseTypes (ProtVer (..), natVersion)
import Cardano.Ledger.Conway (ConwayEra)
import Cardano.Ledger.Core (EraPParams (..), ppMaxTxSizeL, sizeTxF)
import Cardano.Ledger.Shelley.LedgerState (LedgerState (..), UTxOState (..))
import Cardano.Ledger.Shelley.Rules (UtxoEnv (..))
import qualified Data.Text as T
import Lens.Micro ((&), (.~), (^.))
import qualified MAlonzo.Code.Ledger.Foreign.API as Agda
import Prettyprinter ((<+>))
import qualified Prettyprinter as PP
import Test.Cardano.Ledger.Common (Arbitrary (..), Gen, showExpr)
import Test.Cardano.Ledger.Conformance (
  ExecSpecRule (..),
  SpecTranslate (..),
  runSpecTransM,
  unComputationResult,
 )
import Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Base (externalFunctions)
import Test.Cardano.Ledger.Conformance.SpecTranslate.Conway.Cert ()
import Test.Cardano.Ledger.Conformance.SpecTranslate.Conway.Utxo ()
import Test.Cardano.Ledger.Constrained.Conway (
  UtxoExecContext (..),
  utxoEnvSpec,
  utxoStateSpec,
  utxoTxSpec,
 )
import Test.Cardano.Ledger.Conway.ImpTest (showConwayTxBalance)
import Test.Cardano.Ledger.Generic.Functions (TotalAda (..))
import Test.Cardano.Ledger.Generic.GenState (
  GenEnv (..),
  GenSize (..),
  GenState (..),
  initialLedgerState,
  runGenRS,
 )
import qualified Test.Cardano.Ledger.Generic.GenState as GenSize
import qualified Test.Cardano.Ledger.Generic.PrettyCore as PP
import qualified Test.Cardano.Ledger.Generic.Proof as Proof
import Test.Cardano.Ledger.Generic.TxGen (genAlonzoTx)

genUtxoExecContext :: Gen (UtxoExecContext ConwayEra)
genUtxoExecContext :: Gen (UtxoExecContext ConwayEra)
genUtxoExecContext = do
  let proof :: Proof ConwayEra
proof = forall era. Reflect era => Proof era
Proof.reify @ConwayEra
  SlotNo
ueSlot <- Gen SlotNo
forall a. Arbitrary a => Gen a
arbitrary
  let
    genSize :: GenSize
genSize =
      GenSize
GenSize.small
        { invalidScriptFreq = 0 -- TODO make the test work with invalid scripts
        , regCertFreq = 0
        , delegCertFreq = 0
        }
  ((UTxO ConwayEra
uecUTxO, AlonzoTx ConwayEra
uecTx), GenState ConwayEra
gs) <-
    Proof ConwayEra
-> GenSize
-> GenRS ConwayEra (UTxO ConwayEra, AlonzoTx ConwayEra)
-> Gen ((UTxO ConwayEra, AlonzoTx ConwayEra), GenState ConwayEra)
forall era a.
Reflect era =>
Proof era -> GenSize -> GenRS era a -> Gen (a, GenState era)
runGenRS Proof ConwayEra
proof GenSize
genSize (GenRS ConwayEra (UTxO ConwayEra, AlonzoTx ConwayEra)
 -> Gen ((UTxO ConwayEra, AlonzoTx ConwayEra), GenState ConwayEra))
-> GenRS ConwayEra (UTxO ConwayEra, AlonzoTx ConwayEra)
-> Gen ((UTxO ConwayEra, AlonzoTx ConwayEra), GenState ConwayEra)
forall a b. (a -> b) -> a -> b
$
      Proof ConwayEra
-> SlotNo -> GenRS ConwayEra (UTxO ConwayEra, Tx ConwayEra)
forall era.
Reflect era =>
Proof era -> SlotNo -> GenRS era (UTxO era, Tx era)
genAlonzoTx Proof ConwayEra
proof SlotNo
ueSlot
  let
    txSize :: Integer
txSize = AlonzoTx ConwayEra
uecTx AlonzoTx ConwayEra
-> Getting Integer (AlonzoTx ConwayEra) Integer -> Integer
forall s a. s -> Getting a s a -> a
^. Getting Integer (Tx ConwayEra) Integer
Getting Integer (AlonzoTx ConwayEra) Integer
forall era. EraTx era => SimpleGetter (Tx era) Integer
SimpleGetter (Tx ConwayEra) Integer
sizeTxF
    lState :: LedgerState ConwayEra
lState = GenState ConwayEra -> LedgerState ConwayEra
forall era. Reflect era => GenState era -> LedgerState era
initialLedgerState GenState ConwayEra
gs
    ueCertState :: CertState ConwayEra
ueCertState = LedgerState ConwayEra -> CertState ConwayEra
forall era. LedgerState era -> CertState era
lsCertState LedgerState ConwayEra
lState
    uePParams :: PParams ConwayEra
uePParams =
      GenEnv ConwayEra -> PParams ConwayEra
forall era. GenEnv era -> PParams era
gePParams (GenState ConwayEra -> GenEnv ConwayEra
forall era. GenState era -> GenEnv era
gsGenEnv GenState ConwayEra
gs)
        PParams ConwayEra
-> (PParams ConwayEra -> PParams ConwayEra) -> PParams ConwayEra
forall a b. a -> (a -> b) -> b
& (Word32 -> Identity Word32)
-> PParams ConwayEra -> Identity (PParams ConwayEra)
forall era. EraPParams era => Lens' (PParams era) Word32
Lens' (PParams ConwayEra) Word32
ppMaxTxSizeL ((Word32 -> Identity Word32)
 -> PParams ConwayEra -> Identity (PParams ConwayEra))
-> Word32 -> PParams ConwayEra -> PParams ConwayEra
forall s t a b. ASetter s t a b -> b -> s -> t
.~ Integer -> Word32
forall a b. (Integral a, Num b) => a -> b
fromIntegral Integer
txSize
        PParams ConwayEra
-> (PParams ConwayEra -> PParams ConwayEra) -> PParams ConwayEra
forall a b. a -> (a -> b) -> b
& (ProtVer -> Identity ProtVer)
-> PParams ConwayEra -> Identity (PParams ConwayEra)
forall era. EraPParams era => Lens' (PParams era) ProtVer
Lens' (PParams ConwayEra) ProtVer
ppProtocolVersionL ((ProtVer -> Identity ProtVer)
 -> PParams ConwayEra -> Identity (PParams ConwayEra))
-> ProtVer -> PParams ConwayEra -> PParams ConwayEra
forall s t a b. ASetter s t a b -> b -> s -> t
.~ Version -> Natural -> ProtVer
ProtVer (forall (v :: Natural).
(KnownNat v, MinVersion <= v, v <= MaxVersion) =>
Version
natVersion @10) Natural
0
    uecUtxoEnv :: UtxoEnv ConwayEra
uecUtxoEnv = UtxoEnv {PParams ConwayEra
CertState ConwayEra
SlotNo
ueSlot :: SlotNo
ueCertState :: CertState ConwayEra
uePParams :: PParams ConwayEra
ueSlot :: SlotNo
uePParams :: PParams ConwayEra
ueCertState :: CertState ConwayEra
..}
  UtxoExecContext ConwayEra -> Gen (UtxoExecContext ConwayEra)
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure UtxoExecContext {UTxO ConwayEra
AlonzoTx ConwayEra
UtxoEnv ConwayEra
uecUTxO :: UTxO ConwayEra
uecTx :: AlonzoTx ConwayEra
uecUtxoEnv :: UtxoEnv ConwayEra
uecTx :: AlonzoTx ConwayEra
uecUTxO :: UTxO ConwayEra
uecUtxoEnv :: UtxoEnv ConwayEra
..}

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

  genExecContext :: HasCallStack => Gen (ExecContext "UTXO" ConwayEra)
genExecContext = Gen (UtxoExecContext ConwayEra)
Gen (ExecContext "UTXO" ConwayEra)
genUtxoExecContext

  environmentSpec :: HasCallStack =>
ExecContext "UTXO" ConwayEra
-> Specification (ExecEnvironment "UTXO" ConwayEra)
environmentSpec = UtxoExecContext ConwayEra -> Specification (UtxoEnv ConwayEra)
ExecContext "UTXO" ConwayEra
-> Specification (ExecEnvironment "UTXO" ConwayEra)
utxoEnvSpec

  stateSpec :: HasCallStack =>
ExecContext "UTXO" ConwayEra
-> ExecEnvironment "UTXO" ConwayEra
-> Specification (ExecState "UTXO" ConwayEra)
stateSpec = UtxoExecContext ConwayEra
-> UtxoEnv ConwayEra -> Specification (UTxOState ConwayEra)
ExecContext "UTXO" ConwayEra
-> ExecEnvironment "UTXO" ConwayEra
-> Specification (ExecState "UTXO" ConwayEra)
utxoStateSpec

  signalSpec :: HasCallStack =>
ExecContext "UTXO" ConwayEra
-> ExecEnvironment "UTXO" ConwayEra
-> ExecState "UTXO" ConwayEra
-> Specification (ExecSignal "UTXO" ConwayEra)
signalSpec ExecContext "UTXO" ConwayEra
ctx ExecEnvironment "UTXO" ConwayEra
_ ExecState "UTXO" ConwayEra
_ = UtxoExecContext ConwayEra -> Specification (AlonzoTx ConwayEra)
forall era.
HasSpec (AlonzoTx era) =>
UtxoExecContext era -> Specification (AlonzoTx era)
utxoTxSpec UtxoExecContext ConwayEra
ExecContext "UTXO" ConwayEra
ctx

  runAgdaRule :: HasCallStack =>
SpecRep (ExecEnvironment "UTXO" ConwayEra)
-> SpecRep (ExecState "UTXO" ConwayEra)
-> SpecRep (ExecSignal "UTXO" ConwayEra)
-> Either OpaqueErrorString (SpecRep (ExecState "UTXO" ConwayEra))
runAgdaRule SpecRep (ExecEnvironment "UTXO" ConwayEra)
env SpecRep (ExecState "UTXO" ConwayEra)
st SpecRep (ExecSignal "UTXO" 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.utxoStep T_ExternalFunctions_8
externalFunctions UTxOEnv
SpecRep (ExecEnvironment "UTXO" ConwayEra)
env UTxOState
SpecRep (ExecState "UTXO" ConwayEra)
st Tx
SpecRep (ExecSignal "UTXO" ConwayEra)
sig

  extraInfo :: HasCallStack =>
Globals
-> ExecContext "UTXO" ConwayEra
-> Environment (EraRule "UTXO" ConwayEra)
-> State (EraRule "UTXO" ConwayEra)
-> Signal (EraRule "UTXO" ConwayEra)
-> Either
     OpaqueErrorString
     (State (EraRule "UTXO" ConwayEra),
      [Event (EraRule "UTXO" ConwayEra)])
-> Doc AnsiStyle
extraInfo Globals
_ ExecContext "UTXO" ConwayEra
ctx env :: Environment (EraRule "UTXO" ConwayEra)
env@UtxoEnv {PParams ConwayEra
CertState ConwayEra
SlotNo
ueSlot :: forall era. UtxoEnv era -> SlotNo
uePParams :: forall era. UtxoEnv era -> PParams era
ueCertState :: forall era. UtxoEnv era -> CertState era
ueSlot :: SlotNo
uePParams :: PParams ConwayEra
ueCertState :: CertState ConwayEra
..} st :: State (EraRule "UTXO" ConwayEra)
st@UTxOState {GovState ConwayEra
UTxO ConwayEra
InstantStake ConwayEra
Coin
utxosUtxo :: UTxO ConwayEra
utxosDeposited :: Coin
utxosFees :: Coin
utxosGovState :: GovState ConwayEra
utxosInstantStake :: InstantStake ConwayEra
utxosDonation :: Coin
utxosUtxo :: forall era. UTxOState era -> UTxO era
utxosDeposited :: forall era. UTxOState era -> Coin
utxosFees :: forall era. UTxOState era -> Coin
utxosGovState :: forall era. UTxOState era -> GovState era
utxosInstantStake :: forall era. UTxOState era -> InstantStake era
utxosDonation :: forall era. UTxOState era -> Coin
..} Signal (EraRule "UTXO" ConwayEra)
sig Either
  OpaqueErrorString
  (State (EraRule "UTXO" ConwayEra),
   [Event (EraRule "UTXO" ConwayEra)])
st' =
    [Doc AnsiStyle] -> Doc AnsiStyle
forall ann. [Doc ann] -> Doc ann
PP.vcat
      [ Doc AnsiStyle
"Impl:"
      , String -> Doc AnsiStyle
forall a. String -> Doc a
PP.ppString (PParams ConwayEra
-> CertState ConwayEra
-> UTxO ConwayEra
-> AlonzoTx ConwayEra
-> String
forall era.
(EraUTxO era, ConwayEraTxBody era, Tx era ~ AlonzoTx era,
 ConwayEraCertState era) =>
PParams era -> CertState era -> UTxO era -> AlonzoTx era -> String
showConwayTxBalance PParams ConwayEra
uePParams CertState ConwayEra
ueCertState UTxO ConwayEra
utxosUtxo AlonzoTx ConwayEra
Signal (EraRule "UTXO" ConwayEra)
sig)
      , Doc AnsiStyle
"initial TotalAda:" Doc AnsiStyle -> Doc AnsiStyle -> Doc AnsiStyle
forall ann. Doc ann -> Doc ann -> Doc ann
<+> String -> Doc AnsiStyle
forall a. String -> Doc a
PP.ppString (Coin -> String
forall a. ToExpr a => a -> String
showExpr (Coin -> String) -> Coin -> String
forall a b. (a -> b) -> a -> b
$ UTxOState ConwayEra -> Coin
forall t. TotalAda t => t -> Coin
totalAda State (EraRule "UTXO" ConwayEra)
UTxOState ConwayEra
st)
      , Doc AnsiStyle
"final TotalAda:  " Doc AnsiStyle -> Doc AnsiStyle -> Doc AnsiStyle
forall ann. Doc ann -> Doc ann -> Doc ann
<+> case Either
  OpaqueErrorString
  (State (EraRule "UTXO" ConwayEra),
   [Event (EraRule "UTXO" ConwayEra)])
st' of
          Right (State (EraRule "UTXO" ConwayEra)
x, [Event (EraRule "UTXO" ConwayEra)]
_) -> String -> Doc AnsiStyle
forall a. String -> Doc a
PP.ppString (Coin -> String
forall a. ToExpr a => a -> String
showExpr (Coin -> String) -> Coin -> String
forall a b. (a -> b) -> a -> b
$ UTxOState ConwayEra -> Coin
forall t. TotalAda t => t -> Coin
totalAda State (EraRule "UTXO" ConwayEra)
UTxOState ConwayEra
x)
          Left OpaqueErrorString
_ -> Doc AnsiStyle
"N/A"
      , Doc AnsiStyle
forall a. Monoid a => a
mempty
      , Doc AnsiStyle
"Spec:"
      , String -> Doc AnsiStyle
forall a. String -> Doc a
PP.ppString
          ( (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 "UTXO" 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.utxoDebug 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 "UTXO" 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 "UTXO" 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 "UTXO" ConwayEra)
sig
          )
      ]