{-# 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 (Conway)
import Cardano.Ledger.Core (EraPParams (..), ppMaxTxSizeL, sizeTxF)
import Cardano.Ledger.Shelley.LedgerState (LedgerState (..), UTxOState (..))
import Cardano.Ledger.Shelley.Rules (UtxoEnv (..))
import Data.Bifunctor (Bifunctor (..))
import qualified Data.List.NonEmpty as NE
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 (..),
  OpaqueErrorString (..),
  SpecTranslate (..),
  computationResultToEither,
  runSpecTransM,
 )
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 Conway)
genUtxoExecContext :: Gen (UtxoExecContext Conway)
genUtxoExecContext = do
  let proof :: Proof Conway
proof = forall era. Reflect era => Proof era
Proof.reify @Conway
  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 Conway
uecUTxO, AlonzoTx Conway
uecTx), GenState Conway
gs) <-
    forall era a.
Reflect era =>
Proof era -> GenSize -> GenRS era a -> Gen (a, GenState era)
runGenRS Proof Conway
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 Conway
proof SlotNo
ueSlot
  let
    txSize :: Coin
txSize = AlonzoTx Conway
uecTx forall s a. s -> Getting a s a -> a
^. forall era. EraTx era => SimpleGetter (Tx era) Coin
sizeTxF
    lState :: LedgerState Conway
lState = forall era. Reflect era => GenState era -> LedgerState era
initialLedgerState GenState Conway
gs
    ueCertState :: CertState Conway
ueCertState = forall era. LedgerState era -> CertState era
lsCertState LedgerState Conway
lState
    uePParams :: PParams Conway
uePParams =
      forall era. GenEnv era -> PParams era
gePParams (forall era. GenState era -> GenEnv era
gsGenEnv GenState Conway
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 Conway
uecUtxoEnv = UtxoEnv {PParams Conway
CertState Conway
SlotNo
ueSlot :: SlotNo
uePParams :: PParams Conway
ueCertState :: CertState Conway
uePParams :: PParams Conway
ueCertState :: CertState Conway
ueSlot :: SlotNo
..}
  forall (f :: * -> *) a. Applicative f => a -> f a
pure UtxoExecContext {AlonzoTx Conway
UTxO Conway
UtxoEnv Conway
uecTx :: AlonzoTx Conway
uecUTxO :: UTxO Conway
uecUtxoEnv :: UtxoEnv Conway
uecUtxoEnv :: UtxoEnv Conway
uecTx :: AlonzoTx Conway
uecUTxO :: UTxO Conway
..}

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

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

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

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

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

  runAgdaRule :: HasCallStack =>
SpecRep (ExecEnvironment fn "UTXO" Conway)
-> SpecRep (ExecState fn "UTXO" Conway)
-> SpecRep (ExecSignal fn "UTXO" Conway)
-> Either
     (NonEmpty (SpecRep (PredicateFailure (EraRule "UTXO" Conway))))
     (SpecRep (ExecState fn "UTXO" Conway))
runAgdaRule SpecRep (ExecEnvironment fn "UTXO" Conway)
env SpecRep (ExecState fn "UTXO" Conway)
st SpecRep (ExecSignal fn "UTXO" Conway)
sig =
    forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first (\T_String_6
e -> String -> OpaqueErrorString
OpaqueErrorString (T_String_6 -> String
T.unpack T_String_6
e) forall a. a -> [a] -> NonEmpty a
NE.:| [])
      forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall e a. ComputationResult e a -> Either e a
computationResultToEither
      forall a b. (a -> b) -> a -> b
$ T_ExternalFunctions_8
-> UTxOEnv
-> UTxOState
-> Tx
-> T_ComputationResult_46 T_String_6 UTxOState
Agda.utxoStep T_ExternalFunctions_8
externalFunctions SpecRep (ExecEnvironment fn "UTXO" Conway)
env SpecRep (ExecState fn "UTXO" Conway)
st SpecRep (ExecSignal fn "UTXO" Conway)
sig

  extraInfo :: HasCallStack =>
ExecContext fn "UTXO" Conway
-> Environment (EraRule "UTXO" Conway)
-> State (EraRule "UTXO" Conway)
-> Signal (EraRule "UTXO" Conway)
-> Either
     (NonEmpty (PredicateFailure (EraRule "UTXO" Conway)))
     (State (EraRule "UTXO" Conway), [Event (EraRule "UTXO" Conway)])
-> Doc AnsiStyle
extraInfo ExecContext fn "UTXO" Conway
ctx env :: Environment (EraRule "UTXO" Conway)
env@UtxoEnv {PParams Conway
CertState Conway
SlotNo
ueCertState :: CertState Conway
uePParams :: PParams Conway
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" Conway)
st@UTxOState {GovState Conway
Coin
UTxO Conway
IncrementalStake (EraCrypto Conway)
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 (EraCrypto era)
utxosDonation :: forall era. UTxOState era -> Coin
utxosDonation :: Coin
utxosStakeDistr :: IncrementalStake (EraCrypto Conway)
utxosGovState :: GovState Conway
utxosFees :: Coin
utxosDeposited :: Coin
utxosUtxo :: UTxO Conway
..} Signal (EraRule "UTXO" Conway)
sig Either
  (NonEmpty (PredicateFailure (EraRule "UTXO" Conway)))
  (State (EraRule "UTXO" Conway), [Event (EraRule "UTXO" Conway)])
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 Conway
uePParams CertState Conway
ueCertState UTxO Conway
utxosUtxo Signal (EraRule "UTXO" Conway)
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" Conway)
st)
      , Doc AnsiStyle
"final TotalAda:  " forall ann. Doc ann -> Doc ann -> Doc ann
<+> case Either
  (NonEmpty (PredicateFailure (EraRule "UTXO" Conway)))
  (State (EraRule "UTXO" Conway), [Event (EraRule "UTXO" Conway)])
st' of
          Right (State (EraRule "UTXO" Conway)
x, [Event (EraRule "UTXO" Conway)]
_) -> 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" Conway)
x)
          Left NonEmpty (PredicateFailure (EraRule "UTXO" Conway))
_ -> 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 T_String_6 -> String
T.unpack forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall ctx a. ctx -> SpecTransM ctx a -> Either T_String_6 a
runSpecTransM ExecContext fn "UTXO" Conway
ctx forall a b. (a -> b) -> a -> b
$
              T_ExternalFunctions_8 -> UTxOEnv -> UTxOState -> Tx -> T_String_6
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" Conway)
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" Conway)
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" Conway)
sig
          )
      ]