{-# 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 Lib 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 (
  IsConwayUniv,
  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 <- forall a. Arbitrary a => Gen a
arbitrary
  let
    genSize :: GenSize
genSize =
      GenSize
GenSize.small
        { invalidScriptFreq :: Int
invalidScriptFreq = Int
0 -- TODO make the test work with invalid scripts
        , regCertFreq :: Int
regCertFreq = Int
0
        , delegCertFreq :: Int
delegCertFreq = Int
0
        }
  ((UTxO ConwayEra
uecUTxO, AlonzoTx ConwayEra
uecTx), GenState ConwayEra
gs) <-
    forall era a.
Reflect era =>
Proof era -> GenSize -> GenRS era a -> Gen (a, GenState era)
runGenRS Proof ConwayEra
proof GenSize
genSize forall a b. (a -> b) -> a -> b
$
      forall era.
Reflect era =>
Proof era -> SlotNo -> GenRS era (UTxO era, Tx era)
genAlonzoTx Proof ConwayEra
proof SlotNo
ueSlot
  let
    txSize :: Coin
txSize = AlonzoTx ConwayEra
uecTx forall s a. s -> Getting a s a -> a
^. forall era. EraTx era => SimpleGetter (Tx era) Coin
sizeTxF
    lState :: LedgerState ConwayEra
lState = forall era. Reflect era => GenState era -> LedgerState era
initialLedgerState GenState ConwayEra
gs
    ueCertState :: CertState ConwayEra
ueCertState = forall era. LedgerState era -> CertState era
lsCertState LedgerState ConwayEra
lState
    uePParams :: PParams ConwayEra
uePParams =
      forall era. GenEnv era -> PParams era
gePParams (forall era. GenState era -> GenEnv era
gsGenEnv GenState ConwayEra
gs)
        forall a b. a -> (a -> b) -> b
& forall era. EraPParams era => Lens' (PParams era) Word32
ppMaxTxSizeL forall s t a b. ASetter s t a b -> b -> s -> t
.~ forall a b. (Integral a, Num b) => a -> b
fromIntegral Coin
txSize
        forall a b. a -> (a -> b) -> b
& forall era. EraPParams era => Lens' (PParams era) ProtVer
ppProtocolVersionL 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
uePParams :: PParams ConwayEra
ueCertState :: CertState ConwayEra
uePParams :: PParams ConwayEra
ueCertState :: CertState ConwayEra
ueSlot :: SlotNo
..}
  forall (f :: * -> *) a. Applicative f => a -> f a
pure UtxoExecContext {AlonzoTx ConwayEra
UTxO ConwayEra
UtxoEnv ConwayEra
uecTx :: AlonzoTx ConwayEra
uecUTxO :: UTxO ConwayEra
uecUtxoEnv :: UtxoEnv ConwayEra
uecUtxoEnv :: UtxoEnv ConwayEra
uecTx :: AlonzoTx ConwayEra
uecUTxO :: UTxO ConwayEra
..}

instance
  forall fn.
  IsConwayUniv fn =>
  ExecSpecRule fn "UTXO" ConwayEra
  where
  type ExecContext fn "UTXO" ConwayEra = UtxoExecContext ConwayEra

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

  environmentSpec :: HasCallStack =>
ExecContext fn "UTXO" ConwayEra
-> Specification fn (ExecEnvironment fn "UTXO" ConwayEra)
environmentSpec = forall (fn :: [*] -> * -> *).
IsConwayUniv fn =>
UtxoExecContext ConwayEra -> Specification fn (UtxoEnv ConwayEra)
utxoEnvSpec

  stateSpec :: HasCallStack =>
ExecContext fn "UTXO" ConwayEra
-> ExecEnvironment fn "UTXO" ConwayEra
-> Specification fn (ExecState fn "UTXO" ConwayEra)
stateSpec = forall (fn :: [*] -> * -> *).
IsConwayUniv fn =>
UtxoExecContext ConwayEra
-> UtxoEnv ConwayEra -> Specification fn (UTxOState ConwayEra)
utxoStateSpec

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

  runAgdaRule :: HasCallStack =>
SpecRep (ExecEnvironment fn "UTXO" ConwayEra)
-> SpecRep (ExecState fn "UTXO" ConwayEra)
-> SpecRep (ExecSignal fn "UTXO" ConwayEra)
-> Either
     OpaqueErrorString (SpecRep (ExecState fn "UTXO" ConwayEra))
runAgdaRule SpecRep (ExecEnvironment fn "UTXO" ConwayEra)
env SpecRep (ExecState fn "UTXO" ConwayEra)
st SpecRep (ExecSignal fn "UTXO" ConwayEra)
sig =
    forall a. ComputationResult Text a -> Either OpaqueErrorString a
unComputationResult forall a b. (a -> b) -> a -> b
$
      T_ExternalFunctions_8
-> UTxOEnv
-> UTxOState
-> Tx
-> T_ComputationResult_46 Text UTxOState
Agda.utxoStep T_ExternalFunctions_8
externalFunctions SpecRep (ExecEnvironment fn "UTXO" ConwayEra)
env SpecRep (ExecState fn "UTXO" ConwayEra)
st SpecRep (ExecSignal fn "UTXO" ConwayEra)
sig

  extraInfo :: HasCallStack =>
Globals
-> ExecContext fn "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 fn "UTXO" ConwayEra
ctx env :: Environment (EraRule "UTXO" ConwayEra)
env@UtxoEnv {PParams ConwayEra
CertState ConwayEra
SlotNo
ueCertState :: CertState ConwayEra
uePParams :: PParams ConwayEra
ueSlot :: SlotNo
ueSlot :: forall era. UtxoEnv era -> SlotNo
uePParams :: forall era. UtxoEnv era -> PParams era
ueCertState :: forall era. UtxoEnv era -> CertState era
..} st :: State (EraRule "UTXO" ConwayEra)
st@UTxOState {GovState ConwayEra
Coin
UTxO ConwayEra
IncrementalStake
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
utxosStakeDistr :: forall era. UTxOState era -> IncrementalStake
utxosDonation :: forall era. UTxOState era -> Coin
utxosDonation :: Coin
utxosStakeDistr :: IncrementalStake
utxosGovState :: GovState ConwayEra
utxosFees :: Coin
utxosDeposited :: Coin
utxosUtxo :: UTxO ConwayEra
..} Signal (EraRule "UTXO" ConwayEra)
sig Either
  OpaqueErrorString
  (State (EraRule "UTXO" ConwayEra),
   [Event (EraRule "UTXO" ConwayEra)])
st' =
    forall ann. [Doc ann] -> Doc ann
PP.vcat
      [ Doc AnsiStyle
"Impl:"
      , forall a. String -> Doc a
PP.ppString (forall era.
(EraUTxO era, ConwayEraTxBody era, Tx era ~ AlonzoTx era) =>
PParams era -> CertState era -> UTxO era -> AlonzoTx era -> String
showConwayTxBalance PParams ConwayEra
uePParams CertState ConwayEra
ueCertState UTxO ConwayEra
utxosUtxo Signal (EraRule "UTXO" ConwayEra)
sig)
      , Doc AnsiStyle
"initial TotalAda:" forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall a. String -> Doc a
PP.ppString (forall a. ToExpr a => a -> String
showExpr forall a b. (a -> b) -> a -> b
$ forall t. TotalAda t => t -> Coin
totalAda State (EraRule "UTXO" ConwayEra)
st)
      , Doc AnsiStyle
"final TotalAda:  " 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)]
_) -> forall a. String -> Doc a
PP.ppString (forall a. ToExpr a => a -> String
showExpr forall a b. (a -> b) -> a -> b
$ forall t. TotalAda t => t -> Coin
totalAda State (EraRule "UTXO" ConwayEra)
x)
          Left OpaqueErrorString
_ -> Doc AnsiStyle
"N/A"
      , forall a. Monoid a => a
mempty
      , Doc AnsiStyle
"Spec:"
      , forall a. String -> Doc a
PP.ppString
          ( forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either forall a. Show a => a -> String
show Text -> String
T.unpack forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall ctx a. ctx -> SpecTransM ctx a -> Either Text a
runSpecTransM ExecContext fn "UTXO" ConwayEra
ctx forall a b. (a -> b) -> a -> b
$
              T_ExternalFunctions_8 -> UTxOEnv -> UTxOState -> Tx -> Text
Agda.utxoDebug T_ExternalFunctions_8
externalFunctions
                forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep Environment (EraRule "UTXO" ConwayEra)
env
                forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep State (EraRule "UTXO" ConwayEra)
st
                forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep Signal (EraRule "UTXO" ConwayEra)
sig
          )
      ]