{-# LANGUAGE AllowAmbiguousTypes #-} {-# LANGUAGE DataKinds #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeSynonymInstances #-} {-# LANGUAGE UndecidableInstances #-} {-# OPTIONS_GHC -Wno-orphans #-} module Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Utxow () where import Cardano.Ledger.Conway (Conway, ConwayEra) import Cardano.Ledger.Conway.TxCert (ConwayTxCert) import Cardano.Ledger.Crypto (StandardCrypto) import Data.Bifunctor (Bifunctor (..)) import qualified Data.List.NonEmpty as NE import qualified Data.Text as T import qualified Lib as Agda import Test.Cardano.Ledger.Conformance ( ExecSpecRule (..), OpaqueErrorString (..), SpecTranslate, computationResultToEither, ) 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 ( IsConwayUniv, UtxoExecContext, utxoEnvSpec, utxoStateSpec, utxoTxSpec, ) instance ( IsConwayUniv fn , SpecTranslate (ConwayTxBodyTransContext StandardCrypto) (ConwayTxCert (ConwayEra StandardCrypto)) ) => ExecSpecRule fn "UTXOW" Conway where type ExecContext fn "UTXOW" Conway = UtxoExecContext Conway genExecContext :: HasCallStack => Gen (ExecContext fn "UTXOW" (ConwayEra StandardCrypto)) genExecContext = Gen (UtxoExecContext (ConwayEra StandardCrypto)) genUtxoExecContext environmentSpec :: HasCallStack => ExecContext fn "UTXOW" (ConwayEra StandardCrypto) -> Specification fn (ExecEnvironment fn "UTXOW" (ConwayEra StandardCrypto)) environmentSpec = forall (fn :: [*] -> * -> *). IsConwayUniv fn => UtxoExecContext (ConwayEra StandardCrypto) -> Specification fn (UtxoEnv (ConwayEra StandardCrypto)) utxoEnvSpec stateSpec :: HasCallStack => ExecContext fn "UTXOW" (ConwayEra StandardCrypto) -> ExecEnvironment fn "UTXOW" (ConwayEra StandardCrypto) -> Specification fn (ExecState fn "UTXOW" (ConwayEra StandardCrypto)) stateSpec = forall (fn :: [*] -> * -> *). IsConwayUniv fn => UtxoExecContext (ConwayEra StandardCrypto) -> UtxoEnv (ConwayEra StandardCrypto) -> Specification fn (UTxOState (ConwayEra StandardCrypto)) utxoStateSpec signalSpec :: HasCallStack => ExecContext fn "UTXOW" (ConwayEra StandardCrypto) -> ExecEnvironment fn "UTXOW" (ConwayEra StandardCrypto) -> ExecState fn "UTXOW" (ConwayEra StandardCrypto) -> Specification fn (ExecSignal fn "UTXOW" (ConwayEra StandardCrypto)) signalSpec ExecContext fn "UTXOW" (ConwayEra StandardCrypto) ctx ExecEnvironment fn "UTXOW" (ConwayEra StandardCrypto) _ ExecState fn "UTXOW" (ConwayEra StandardCrypto) _ = forall (fn :: [*] -> * -> *) era. (IsConwayUniv fn, HasSpec fn (AlonzoTx era)) => UtxoExecContext era -> Specification fn (AlonzoTx era) utxoTxSpec ExecContext fn "UTXOW" (ConwayEra StandardCrypto) ctx runAgdaRule :: HasCallStack => SpecRep (ExecEnvironment fn "UTXOW" (ConwayEra StandardCrypto)) -> SpecRep (ExecState fn "UTXOW" (ConwayEra StandardCrypto)) -> SpecRep (ExecSignal fn "UTXOW" (ConwayEra StandardCrypto)) -> Either (NonEmpty (SpecRep (PredicateFailure (EraRule "UTXOW" (ConwayEra StandardCrypto))))) (SpecRep (ExecState fn "UTXOW" (ConwayEra StandardCrypto))) runAgdaRule SpecRep (ExecEnvironment fn "UTXOW" (ConwayEra StandardCrypto)) env SpecRep (ExecState fn "UTXOW" (ConwayEra StandardCrypto)) st SpecRep (ExecSignal fn "UTXOW" (ConwayEra StandardCrypto)) 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 $ UTxOEnv -> UTxOState -> Tx -> T_ComputationResult_48 T_String_6 UTxOState Agda.utxowStep SpecRep (ExecEnvironment fn "UTXOW" (ConwayEra StandardCrypto)) env SpecRep (ExecState fn "UTXOW" (ConwayEra StandardCrypto)) st SpecRep (ExecSignal fn "UTXOW" (ConwayEra StandardCrypto)) sig