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

module Test.Cardano.Ledger.Conformance.SpecTranslate.Conway.Ledger () where

import Cardano.Ledger.BaseTypes (Inject)
import Cardano.Ledger.Conway (ConwayEra)
import Cardano.Ledger.Conway.Core (
  AllegraEraTxBody (..),
  AlonzoEraTxBody (..),
  BabbageEraTxBody (..),
  ConwayEraTxBody (..),
  EraPParams (..),
  EraRule,
  EraTxBody (..),
  ScriptHash,
 )
import Cardano.Ledger.Conway.Rules (ConwayLedgerPredFailure, EnactState)
import Cardano.Ledger.Shelley.Rules (LedgerEnv (..))
import Cardano.Ledger.Shelley.State (ChainAccountState (..))
import Cardano.Ledger.TxIn (TxId)
import Control.State.Transition.Extended (STS (..))
import Data.Functor.Identity (Identity)
import Data.Maybe.Strict (StrictMaybe)
import Lens.Micro ((^.))
import qualified MAlonzo.Code.Ledger.Foreign.API as Agda
import Test.Cardano.Ledger.Conformance (OpaqueErrorString (..), askCtx, showOpaqueErrorString)
import Test.Cardano.Ledger.Conformance.SpecTranslate.Conway.Base (SpecTranslate (..))
import Test.Cardano.Ledger.Conformance.SpecTranslate.Conway.Cert ()
import Test.Cardano.Ledger.Conway.TreeDiff (ToExpr (..))

instance
  ( EraPParams era
  , SpecTranslate ctx (PParamsHKD Identity era)
  , SpecRep (PParamsHKD Identity era) ~ Agda.PParams
  , Inject ctx (StrictMaybe ScriptHash)
  , Inject ctx (EnactState era)
  ) =>
  SpecTranslate ctx (LedgerEnv era)
  where
  type SpecRep (LedgerEnv era) = Agda.LEnv

  toSpecRep :: LedgerEnv era -> SpecTransM ctx (SpecRep (LedgerEnv era))
toSpecRep LedgerEnv {Maybe EpochNo
PParams era
ChainAccountState
TxIx
SlotNo
ledgerSlotNo :: SlotNo
ledgerEpochNo :: Maybe EpochNo
ledgerIx :: TxIx
ledgerPp :: PParams era
ledgerAccount :: ChainAccountState
ledgerSlotNo :: forall era. LedgerEnv era -> SlotNo
ledgerEpochNo :: forall era. LedgerEnv era -> Maybe EpochNo
ledgerIx :: forall era. LedgerEnv era -> TxIx
ledgerPp :: forall era. LedgerEnv era -> PParams era
ledgerAccount :: forall era. LedgerEnv era -> ChainAccountState
..} = do
    StrictMaybe ScriptHash
policyHash <- forall b ctx. Inject ctx b => SpecTransM ctx b
askCtx @(StrictMaybe ScriptHash)
    EnactState era
enactState <- forall b ctx. Inject ctx b => SpecTransM ctx b
askCtx @(EnactState era)
    Integer
-> Maybe Integer -> PParams -> EnactState -> Integer -> LEnv
Agda.MkLEnv
      (Integer
 -> Maybe Integer -> PParams -> EnactState -> Integer -> LEnv)
-> SpecTransM ctx Integer
-> SpecTransM
     ctx (Maybe Integer -> PParams -> EnactState -> Integer -> LEnv)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SlotNo -> SpecTransM ctx (SpecRep SlotNo)
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep SlotNo
ledgerSlotNo
      SpecTransM
  ctx (Maybe Integer -> PParams -> EnactState -> Integer -> LEnv)
-> SpecTransM ctx (Maybe Integer)
-> SpecTransM ctx (PParams -> EnactState -> Integer -> LEnv)
forall a b.
SpecTransM ctx (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> StrictMaybe ScriptHash
-> SpecTransM ctx (SpecRep (StrictMaybe ScriptHash))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep StrictMaybe ScriptHash
policyHash
      SpecTransM ctx (PParams -> EnactState -> Integer -> LEnv)
-> SpecTransM ctx PParams
-> SpecTransM ctx (EnactState -> Integer -> LEnv)
forall a b.
SpecTransM ctx (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> PParams era -> SpecTransM ctx (SpecRep (PParams era))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep PParams era
ledgerPp
      SpecTransM ctx (EnactState -> Integer -> LEnv)
-> SpecTransM ctx EnactState -> SpecTransM ctx (Integer -> LEnv)
forall a b.
SpecTransM ctx (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> EnactState era -> SpecTransM ctx (SpecRep (EnactState era))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep EnactState era
enactState
      SpecTransM ctx (Integer -> LEnv)
-> SpecTransM ctx Integer -> SpecTransM ctx LEnv
forall a b.
SpecTransM ctx (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Coin -> SpecTransM ctx (SpecRep Coin)
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep (ChainAccountState -> Coin
casTreasury ChainAccountState
ledgerAccount)

instance
  ( ToExpr (PredicateFailure (EraRule "GOV" era))
  , ToExpr (PredicateFailure (EraRule "CERTS" era))
  , ToExpr (PredicateFailure (EraRule "UTXOW" era))
  ) =>
  SpecTranslate ctx (ConwayLedgerPredFailure era)
  where
  type SpecRep (ConwayLedgerPredFailure era) = OpaqueErrorString

  toSpecRep :: ConwayLedgerPredFailure era
-> SpecTransM ctx (SpecRep (ConwayLedgerPredFailure era))
toSpecRep = OpaqueErrorString -> SpecTransM ctx OpaqueErrorString
forall a. a -> SpecTransM ctx a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (OpaqueErrorString -> SpecTransM ctx OpaqueErrorString)
-> (ConwayLedgerPredFailure era -> OpaqueErrorString)
-> ConwayLedgerPredFailure era
-> SpecTransM ctx OpaqueErrorString
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ConwayLedgerPredFailure era -> OpaqueErrorString
forall a. ToExpr a => a -> OpaqueErrorString
showOpaqueErrorString

instance
  ( Inject ctx Integer
  , Inject ctx TxId
  ) =>
  SpecTranslate ctx (TxBody ConwayEra)
  where
  type SpecRep (TxBody ConwayEra) = Agda.TxBody

  toSpecRep :: TxBody ConwayEra -> SpecTransM ctx (SpecRep (TxBody ConwayEra))
toSpecRep TxBody ConwayEra
txb = do
    Integer
sizeTx <- SpecTransM ctx Integer
forall b ctx. Inject ctx b => SpecTransM ctx b
askCtx
    TxId
txId <- forall b ctx. Inject ctx b => SpecTransM ctx b
askCtx @TxId
    HSSet (Integer, Integer)
-> HSSet (Integer, Integer)
-> HSMap
     Integer
     (Either BaseAddr BootstrapAddr,
      (Integer,
       (Maybe (Either Integer Integer),
        Maybe (Either HSTimelock HSPlutusScript))))
-> Integer
-> Integer
-> (Maybe Integer, Maybe Integer)
-> [DCert]
-> HSMap RwdAddr Integer
-> [GovVote]
-> [GovProposal]
-> Integer
-> Maybe (HSMap Integer PParamsUpdate, Integer)
-> Maybe Integer
-> Maybe Integer
-> Maybe Integer
-> Integer
-> Integer
-> HSSet (Integer, Integer)
-> HSSet Integer
-> Maybe Integer
-> TxBody
Agda.MkTxBody
      (HSSet (Integer, Integer)
 -> HSSet (Integer, Integer)
 -> HSMap
      Integer
      (Either BaseAddr BootstrapAddr,
       (Integer,
        (Maybe (Either Integer Integer),
         Maybe (Either HSTimelock HSPlutusScript))))
 -> Integer
 -> Integer
 -> (Maybe Integer, Maybe Integer)
 -> [DCert]
 -> HSMap RwdAddr Integer
 -> [GovVote]
 -> [GovProposal]
 -> Integer
 -> Maybe (HSMap Integer PParamsUpdate, Integer)
 -> Maybe Integer
 -> Maybe Integer
 -> Maybe Integer
 -> Integer
 -> Integer
 -> HSSet (Integer, Integer)
 -> HSSet Integer
 -> Maybe Integer
 -> TxBody)
-> SpecTransM ctx (HSSet (Integer, Integer))
-> SpecTransM
     ctx
     (HSSet (Integer, Integer)
      -> HSMap
           Integer
           (Either BaseAddr BootstrapAddr,
            (Integer,
             (Maybe (Either Integer Integer),
              Maybe (Either HSTimelock HSPlutusScript))))
      -> Integer
      -> Integer
      -> (Maybe Integer, Maybe Integer)
      -> [DCert]
      -> HSMap RwdAddr Integer
      -> [GovVote]
      -> [GovProposal]
      -> Integer
      -> Maybe (HSMap Integer PParamsUpdate, Integer)
      -> Maybe Integer
      -> Maybe Integer
      -> Maybe Integer
      -> Integer
      -> Integer
      -> HSSet (Integer, Integer)
      -> HSSet Integer
      -> Maybe Integer
      -> TxBody)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Set TxIn -> SpecTransM ctx (SpecRep (Set TxIn))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep (TxBody ConwayEra
txb TxBody ConwayEra
-> Getting (Set TxIn) (TxBody ConwayEra) (Set TxIn) -> Set TxIn
forall s a. s -> Getting a s a -> a
^. Getting (Set TxIn) (TxBody ConwayEra) (Set TxIn)
forall era. EraTxBody era => Lens' (TxBody era) (Set TxIn)
Lens' (TxBody ConwayEra) (Set TxIn)
inputsTxBodyL)
      SpecTransM
  ctx
  (HSSet (Integer, Integer)
   -> HSMap
        Integer
        (Either BaseAddr BootstrapAddr,
         (Integer,
          (Maybe (Either Integer Integer),
           Maybe (Either HSTimelock HSPlutusScript))))
   -> Integer
   -> Integer
   -> (Maybe Integer, Maybe Integer)
   -> [DCert]
   -> HSMap RwdAddr Integer
   -> [GovVote]
   -> [GovProposal]
   -> Integer
   -> Maybe (HSMap Integer PParamsUpdate, Integer)
   -> Maybe Integer
   -> Maybe Integer
   -> Maybe Integer
   -> Integer
   -> Integer
   -> HSSet (Integer, Integer)
   -> HSSet Integer
   -> Maybe Integer
   -> TxBody)
-> SpecTransM ctx (HSSet (Integer, Integer))
-> SpecTransM
     ctx
     (HSMap
        Integer
        (Either BaseAddr BootstrapAddr,
         (Integer,
          (Maybe (Either Integer Integer),
           Maybe (Either HSTimelock HSPlutusScript))))
      -> Integer
      -> Integer
      -> (Maybe Integer, Maybe Integer)
      -> [DCert]
      -> HSMap RwdAddr Integer
      -> [GovVote]
      -> [GovProposal]
      -> Integer
      -> Maybe (HSMap Integer PParamsUpdate, Integer)
      -> Maybe Integer
      -> Maybe Integer
      -> Maybe Integer
      -> Integer
      -> Integer
      -> HSSet (Integer, Integer)
      -> HSSet Integer
      -> Maybe Integer
      -> TxBody)
forall a b.
SpecTransM ctx (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Set TxIn -> SpecTransM ctx (SpecRep (Set TxIn))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep (TxBody ConwayEra
txb TxBody ConwayEra
-> Getting (Set TxIn) (TxBody ConwayEra) (Set TxIn) -> Set TxIn
forall s a. s -> Getting a s a -> a
^. Getting (Set TxIn) (TxBody ConwayEra) (Set TxIn)
forall era. BabbageEraTxBody era => Lens' (TxBody era) (Set TxIn)
Lens' (TxBody ConwayEra) (Set TxIn)
referenceInputsTxBodyL)
      SpecTransM
  ctx
  (HSMap
     Integer
     (Either BaseAddr BootstrapAddr,
      (Integer,
       (Maybe (Either Integer Integer),
        Maybe (Either HSTimelock HSPlutusScript))))
   -> Integer
   -> Integer
   -> (Maybe Integer, Maybe Integer)
   -> [DCert]
   -> HSMap RwdAddr Integer
   -> [GovVote]
   -> [GovProposal]
   -> Integer
   -> Maybe (HSMap Integer PParamsUpdate, Integer)
   -> Maybe Integer
   -> Maybe Integer
   -> Maybe Integer
   -> Integer
   -> Integer
   -> HSSet (Integer, Integer)
   -> HSSet Integer
   -> Maybe Integer
   -> TxBody)
-> SpecTransM
     ctx
     (HSMap
        Integer
        (Either BaseAddr BootstrapAddr,
         (Integer,
          (Maybe (Either Integer Integer),
           Maybe (Either HSTimelock HSPlutusScript)))))
-> SpecTransM
     ctx
     (Integer
      -> Integer
      -> (Maybe Integer, Maybe Integer)
      -> [DCert]
      -> HSMap RwdAddr Integer
      -> [GovVote]
      -> [GovProposal]
      -> Integer
      -> Maybe (HSMap Integer PParamsUpdate, Integer)
      -> Maybe Integer
      -> Maybe Integer
      -> Maybe Integer
      -> Integer
      -> Integer
      -> HSSet (Integer, Integer)
      -> HSSet Integer
      -> Maybe Integer
      -> TxBody)
forall a b.
SpecTransM ctx (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ([(Integer,
  (Either BaseAddr BootstrapAddr,
   (Integer,
    (Maybe (Either Integer Integer),
     Maybe (Either HSTimelock HSPlutusScript)))))]
-> HSMap
     Integer
     (Either BaseAddr BootstrapAddr,
      (Integer,
       (Maybe (Either Integer Integer),
        Maybe (Either HSTimelock HSPlutusScript))))
forall k v. [(k, v)] -> HSMap k v
Agda.MkHSMap ([(Integer,
   (Either BaseAddr BootstrapAddr,
    (Integer,
     (Maybe (Either Integer Integer),
      Maybe (Either HSTimelock HSPlutusScript)))))]
 -> HSMap
      Integer
      (Either BaseAddr BootstrapAddr,
       (Integer,
        (Maybe (Either Integer Integer),
         Maybe (Either HSTimelock HSPlutusScript)))))
-> ([(Either BaseAddr BootstrapAddr,
      (Integer,
       (Maybe (Either Integer Integer),
        Maybe (Either HSTimelock HSPlutusScript))))]
    -> [(Integer,
         (Either BaseAddr BootstrapAddr,
          (Integer,
           (Maybe (Either Integer Integer),
            Maybe (Either HSTimelock HSPlutusScript)))))])
-> [(Either BaseAddr BootstrapAddr,
     (Integer,
      (Maybe (Either Integer Integer),
       Maybe (Either HSTimelock HSPlutusScript))))]
-> HSMap
     Integer
     (Either BaseAddr BootstrapAddr,
      (Integer,
       (Maybe (Either Integer Integer),
        Maybe (Either HSTimelock HSPlutusScript))))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Integer]
-> [(Either BaseAddr BootstrapAddr,
     (Integer,
      (Maybe (Either Integer Integer),
       Maybe (Either HSTimelock HSPlutusScript))))]
-> [(Integer,
     (Either BaseAddr BootstrapAddr,
      (Integer,
       (Maybe (Either Integer Integer),
        Maybe (Either HSTimelock HSPlutusScript)))))]
forall a b. [a] -> [b] -> [(a, b)]
zip [Integer
0 ..] ([(Either BaseAddr BootstrapAddr,
   (Integer,
    (Maybe (Either Integer Integer),
     Maybe (Either HSTimelock HSPlutusScript))))]
 -> HSMap
      Integer
      (Either BaseAddr BootstrapAddr,
       (Integer,
        (Maybe (Either Integer Integer),
         Maybe (Either HSTimelock HSPlutusScript)))))
-> SpecTransM
     ctx
     [(Either BaseAddr BootstrapAddr,
       (Integer,
        (Maybe (Either Integer Integer),
         Maybe (Either HSTimelock HSPlutusScript))))]
-> SpecTransM
     ctx
     (HSMap
        Integer
        (Either BaseAddr BootstrapAddr,
         (Integer,
          (Maybe (Either Integer Integer),
           Maybe (Either HSTimelock HSPlutusScript)))))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StrictSeq (BabbageTxOut ConwayEra)
-> SpecTransM ctx (SpecRep (StrictSeq (BabbageTxOut ConwayEra)))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep (TxBody ConwayEra
txb TxBody ConwayEra
-> Getting
     (StrictSeq (BabbageTxOut ConwayEra))
     (TxBody ConwayEra)
     (StrictSeq (BabbageTxOut ConwayEra))
-> StrictSeq (BabbageTxOut ConwayEra)
forall s a. s -> Getting a s a -> a
^. (StrictSeq (TxOut ConwayEra)
 -> Const
      (StrictSeq (BabbageTxOut ConwayEra)) (StrictSeq (TxOut ConwayEra)))
-> TxBody ConwayEra
-> Const (StrictSeq (BabbageTxOut ConwayEra)) (TxBody ConwayEra)
Getting
  (StrictSeq (BabbageTxOut ConwayEra))
  (TxBody ConwayEra)
  (StrictSeq (BabbageTxOut ConwayEra))
forall era.
EraTxBody era =>
Lens' (TxBody era) (StrictSeq (TxOut era))
Lens' (TxBody ConwayEra) (StrictSeq (TxOut ConwayEra))
outputsTxBodyL))
      SpecTransM
  ctx
  (Integer
   -> Integer
   -> (Maybe Integer, Maybe Integer)
   -> [DCert]
   -> HSMap RwdAddr Integer
   -> [GovVote]
   -> [GovProposal]
   -> Integer
   -> Maybe (HSMap Integer PParamsUpdate, Integer)
   -> Maybe Integer
   -> Maybe Integer
   -> Maybe Integer
   -> Integer
   -> Integer
   -> HSSet (Integer, Integer)
   -> HSSet Integer
   -> Maybe Integer
   -> TxBody)
-> SpecTransM ctx Integer
-> SpecTransM
     ctx
     (Integer
      -> (Maybe Integer, Maybe Integer)
      -> [DCert]
      -> HSMap RwdAddr Integer
      -> [GovVote]
      -> [GovProposal]
      -> Integer
      -> Maybe (HSMap Integer PParamsUpdate, Integer)
      -> Maybe Integer
      -> Maybe Integer
      -> Maybe Integer
      -> Integer
      -> Integer
      -> HSSet (Integer, Integer)
      -> HSSet Integer
      -> Maybe Integer
      -> TxBody)
forall a b.
SpecTransM ctx (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Coin -> SpecTransM ctx (SpecRep Coin)
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep (TxBody ConwayEra
txb TxBody ConwayEra -> Getting Coin (TxBody ConwayEra) Coin -> Coin
forall s a. s -> Getting a s a -> a
^. Getting Coin (TxBody ConwayEra) Coin
forall era. EraTxBody era => Lens' (TxBody era) Coin
Lens' (TxBody ConwayEra) Coin
feeTxBodyL)
      SpecTransM
  ctx
  (Integer
   -> (Maybe Integer, Maybe Integer)
   -> [DCert]
   -> HSMap RwdAddr Integer
   -> [GovVote]
   -> [GovProposal]
   -> Integer
   -> Maybe (HSMap Integer PParamsUpdate, Integer)
   -> Maybe Integer
   -> Maybe Integer
   -> Maybe Integer
   -> Integer
   -> Integer
   -> HSSet (Integer, Integer)
   -> HSSet Integer
   -> Maybe Integer
   -> TxBody)
-> SpecTransM ctx Integer
-> SpecTransM
     ctx
     ((Maybe Integer, Maybe Integer)
      -> [DCert]
      -> HSMap RwdAddr Integer
      -> [GovVote]
      -> [GovProposal]
      -> Integer
      -> Maybe (HSMap Integer PParamsUpdate, Integer)
      -> Maybe Integer
      -> Maybe Integer
      -> Maybe Integer
      -> Integer
      -> Integer
      -> HSSet (Integer, Integer)
      -> HSSet Integer
      -> Maybe Integer
      -> TxBody)
forall a b.
SpecTransM ctx (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Integer -> SpecTransM ctx Integer
forall a. a -> SpecTransM ctx a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Integer
0
      SpecTransM
  ctx
  ((Maybe Integer, Maybe Integer)
   -> [DCert]
   -> HSMap RwdAddr Integer
   -> [GovVote]
   -> [GovProposal]
   -> Integer
   -> Maybe (HSMap Integer PParamsUpdate, Integer)
   -> Maybe Integer
   -> Maybe Integer
   -> Maybe Integer
   -> Integer
   -> Integer
   -> HSSet (Integer, Integer)
   -> HSSet Integer
   -> Maybe Integer
   -> TxBody)
-> SpecTransM ctx (Maybe Integer, Maybe Integer)
-> SpecTransM
     ctx
     ([DCert]
      -> HSMap RwdAddr Integer
      -> [GovVote]
      -> [GovProposal]
      -> Integer
      -> Maybe (HSMap Integer PParamsUpdate, Integer)
      -> Maybe Integer
      -> Maybe Integer
      -> Maybe Integer
      -> Integer
      -> Integer
      -> HSSet (Integer, Integer)
      -> HSSet Integer
      -> Maybe Integer
      -> TxBody)
forall a b.
SpecTransM ctx (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ValidityInterval -> SpecTransM ctx (SpecRep ValidityInterval)
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep (TxBody ConwayEra
txb TxBody ConwayEra
-> Getting ValidityInterval (TxBody ConwayEra) ValidityInterval
-> ValidityInterval
forall s a. s -> Getting a s a -> a
^. Getting ValidityInterval (TxBody ConwayEra) ValidityInterval
forall era.
AllegraEraTxBody era =>
Lens' (TxBody era) ValidityInterval
Lens' (TxBody ConwayEra) ValidityInterval
vldtTxBodyL)
      SpecTransM
  ctx
  ([DCert]
   -> HSMap RwdAddr Integer
   -> [GovVote]
   -> [GovProposal]
   -> Integer
   -> Maybe (HSMap Integer PParamsUpdate, Integer)
   -> Maybe Integer
   -> Maybe Integer
   -> Maybe Integer
   -> Integer
   -> Integer
   -> HSSet (Integer, Integer)
   -> HSSet Integer
   -> Maybe Integer
   -> TxBody)
-> SpecTransM ctx [DCert]
-> SpecTransM
     ctx
     (HSMap RwdAddr Integer
      -> [GovVote]
      -> [GovProposal]
      -> Integer
      -> Maybe (HSMap Integer PParamsUpdate, Integer)
      -> Maybe Integer
      -> Maybe Integer
      -> Maybe Integer
      -> Integer
      -> Integer
      -> HSSet (Integer, Integer)
      -> HSSet Integer
      -> Maybe Integer
      -> TxBody)
forall a b.
SpecTransM ctx (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> StrictSeq (ConwayTxCert ConwayEra)
-> SpecTransM ctx (SpecRep (StrictSeq (ConwayTxCert ConwayEra)))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep (TxBody ConwayEra
txb TxBody ConwayEra
-> Getting
     (StrictSeq (ConwayTxCert ConwayEra))
     (TxBody ConwayEra)
     (StrictSeq (ConwayTxCert ConwayEra))
-> StrictSeq (ConwayTxCert ConwayEra)
forall s a. s -> Getting a s a -> a
^. (StrictSeq (TxCert ConwayEra)
 -> Const
      (StrictSeq (ConwayTxCert ConwayEra))
      (StrictSeq (TxCert ConwayEra)))
-> TxBody ConwayEra
-> Const (StrictSeq (ConwayTxCert ConwayEra)) (TxBody ConwayEra)
Getting
  (StrictSeq (ConwayTxCert ConwayEra))
  (TxBody ConwayEra)
  (StrictSeq (ConwayTxCert ConwayEra))
forall era.
EraTxBody era =>
Lens' (TxBody era) (StrictSeq (TxCert era))
Lens' (TxBody ConwayEra) (StrictSeq (TxCert ConwayEra))
certsTxBodyL)
      SpecTransM
  ctx
  (HSMap RwdAddr Integer
   -> [GovVote]
   -> [GovProposal]
   -> Integer
   -> Maybe (HSMap Integer PParamsUpdate, Integer)
   -> Maybe Integer
   -> Maybe Integer
   -> Maybe Integer
   -> Integer
   -> Integer
   -> HSSet (Integer, Integer)
   -> HSSet Integer
   -> Maybe Integer
   -> TxBody)
-> SpecTransM ctx (HSMap RwdAddr Integer)
-> SpecTransM
     ctx
     ([GovVote]
      -> [GovProposal]
      -> Integer
      -> Maybe (HSMap Integer PParamsUpdate, Integer)
      -> Maybe Integer
      -> Maybe Integer
      -> Maybe Integer
      -> Integer
      -> Integer
      -> HSSet (Integer, Integer)
      -> HSSet Integer
      -> Maybe Integer
      -> TxBody)
forall a b.
SpecTransM ctx (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Withdrawals -> SpecTransM ctx (SpecRep Withdrawals)
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep (TxBody ConwayEra
txb TxBody ConwayEra
-> Getting Withdrawals (TxBody ConwayEra) Withdrawals
-> Withdrawals
forall s a. s -> Getting a s a -> a
^. Getting Withdrawals (TxBody ConwayEra) Withdrawals
forall era. EraTxBody era => Lens' (TxBody era) Withdrawals
Lens' (TxBody ConwayEra) Withdrawals
withdrawalsTxBodyL)
      SpecTransM
  ctx
  ([GovVote]
   -> [GovProposal]
   -> Integer
   -> Maybe (HSMap Integer PParamsUpdate, Integer)
   -> Maybe Integer
   -> Maybe Integer
   -> Maybe Integer
   -> Integer
   -> Integer
   -> HSSet (Integer, Integer)
   -> HSSet Integer
   -> Maybe Integer
   -> TxBody)
-> SpecTransM ctx [GovVote]
-> SpecTransM
     ctx
     ([GovProposal]
      -> Integer
      -> Maybe (HSMap Integer PParamsUpdate, Integer)
      -> Maybe Integer
      -> Maybe Integer
      -> Maybe Integer
      -> Integer
      -> Integer
      -> HSSet (Integer, Integer)
      -> HSSet Integer
      -> Maybe Integer
      -> TxBody)
forall a b.
SpecTransM ctx (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> VotingProcedures ConwayEra
-> SpecTransM ctx (SpecRep (VotingProcedures ConwayEra))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep (TxBody ConwayEra
txb TxBody ConwayEra
-> Getting
     (VotingProcedures ConwayEra)
     (TxBody ConwayEra)
     (VotingProcedures ConwayEra)
-> VotingProcedures ConwayEra
forall s a. s -> Getting a s a -> a
^. Getting
  (VotingProcedures ConwayEra)
  (TxBody ConwayEra)
  (VotingProcedures ConwayEra)
forall era.
ConwayEraTxBody era =>
Lens' (TxBody era) (VotingProcedures era)
Lens' (TxBody ConwayEra) (VotingProcedures ConwayEra)
votingProceduresTxBodyL)
      SpecTransM
  ctx
  ([GovProposal]
   -> Integer
   -> Maybe (HSMap Integer PParamsUpdate, Integer)
   -> Maybe Integer
   -> Maybe Integer
   -> Maybe Integer
   -> Integer
   -> Integer
   -> HSSet (Integer, Integer)
   -> HSSet Integer
   -> Maybe Integer
   -> TxBody)
-> SpecTransM ctx [GovProposal]
-> SpecTransM
     ctx
     (Integer
      -> Maybe (HSMap Integer PParamsUpdate, Integer)
      -> Maybe Integer
      -> Maybe Integer
      -> Maybe Integer
      -> Integer
      -> Integer
      -> HSSet (Integer, Integer)
      -> HSSet Integer
      -> Maybe Integer
      -> TxBody)
forall a b.
SpecTransM ctx (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> OSet (ProposalProcedure ConwayEra)
-> SpecTransM ctx (SpecRep (OSet (ProposalProcedure ConwayEra)))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep (TxBody ConwayEra
txb TxBody ConwayEra
-> Getting
     (OSet (ProposalProcedure ConwayEra))
     (TxBody ConwayEra)
     (OSet (ProposalProcedure ConwayEra))
-> OSet (ProposalProcedure ConwayEra)
forall s a. s -> Getting a s a -> a
^. Getting
  (OSet (ProposalProcedure ConwayEra))
  (TxBody ConwayEra)
  (OSet (ProposalProcedure ConwayEra))
forall era.
ConwayEraTxBody era =>
Lens' (TxBody era) (OSet (ProposalProcedure era))
Lens' (TxBody ConwayEra) (OSet (ProposalProcedure ConwayEra))
proposalProceduresTxBodyL)
      SpecTransM
  ctx
  (Integer
   -> Maybe (HSMap Integer PParamsUpdate, Integer)
   -> Maybe Integer
   -> Maybe Integer
   -> Maybe Integer
   -> Integer
   -> Integer
   -> HSSet (Integer, Integer)
   -> HSSet Integer
   -> Maybe Integer
   -> TxBody)
-> SpecTransM ctx Integer
-> SpecTransM
     ctx
     (Maybe (HSMap Integer PParamsUpdate, Integer)
      -> Maybe Integer
      -> Maybe Integer
      -> Maybe Integer
      -> Integer
      -> Integer
      -> HSSet (Integer, Integer)
      -> HSSet Integer
      -> Maybe Integer
      -> TxBody)
forall a b.
SpecTransM ctx (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Coin -> SpecTransM ctx (SpecRep Coin)
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep (TxBody ConwayEra
txb TxBody ConwayEra -> Getting Coin (TxBody ConwayEra) Coin -> Coin
forall s a. s -> Getting a s a -> a
^. Getting Coin (TxBody ConwayEra) Coin
forall era. ConwayEraTxBody era => Lens' (TxBody era) Coin
Lens' (TxBody ConwayEra) Coin
treasuryDonationTxBodyL)
      SpecTransM
  ctx
  (Maybe (HSMap Integer PParamsUpdate, Integer)
   -> Maybe Integer
   -> Maybe Integer
   -> Maybe Integer
   -> Integer
   -> Integer
   -> HSSet (Integer, Integer)
   -> HSSet Integer
   -> Maybe Integer
   -> TxBody)
-> SpecTransM ctx (Maybe (HSMap Integer PParamsUpdate, Integer))
-> SpecTransM
     ctx
     (Maybe Integer
      -> Maybe Integer
      -> Maybe Integer
      -> Integer
      -> Integer
      -> HSSet (Integer, Integer)
      -> HSSet Integer
      -> Maybe Integer
      -> TxBody)
forall a b.
SpecTransM ctx (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Maybe (HSMap Integer PParamsUpdate, Integer)
-> SpecTransM ctx (Maybe (HSMap Integer PParamsUpdate, Integer))
forall a. a -> SpecTransM ctx a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe (HSMap Integer PParamsUpdate, Integer)
forall a. Maybe a
Nothing -- TODO implement this properly
      SpecTransM
  ctx
  (Maybe Integer
   -> Maybe Integer
   -> Maybe Integer
   -> Integer
   -> Integer
   -> HSSet (Integer, Integer)
   -> HSSet Integer
   -> Maybe Integer
   -> TxBody)
-> SpecTransM ctx (Maybe Integer)
-> SpecTransM
     ctx
     (Maybe Integer
      -> Maybe Integer
      -> Integer
      -> Integer
      -> HSSet (Integer, Integer)
      -> HSSet Integer
      -> Maybe Integer
      -> TxBody)
forall a b.
SpecTransM ctx (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> StrictMaybe TxAuxDataHash
-> SpecTransM ctx (SpecRep (StrictMaybe TxAuxDataHash))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep (TxBody ConwayEra
txb TxBody ConwayEra
-> Getting
     (StrictMaybe TxAuxDataHash)
     (TxBody ConwayEra)
     (StrictMaybe TxAuxDataHash)
-> StrictMaybe TxAuxDataHash
forall s a. s -> Getting a s a -> a
^. Getting
  (StrictMaybe TxAuxDataHash)
  (TxBody ConwayEra)
  (StrictMaybe TxAuxDataHash)
forall era.
EraTxBody era =>
Lens' (TxBody era) (StrictMaybe TxAuxDataHash)
Lens' (TxBody ConwayEra) (StrictMaybe TxAuxDataHash)
auxDataHashTxBodyL)
      SpecTransM
  ctx
  (Maybe Integer
   -> Maybe Integer
   -> Integer
   -> Integer
   -> HSSet (Integer, Integer)
   -> HSSet Integer
   -> Maybe Integer
   -> TxBody)
-> SpecTransM ctx (Maybe Integer)
-> SpecTransM
     ctx
     (Maybe Integer
      -> Integer
      -> Integer
      -> HSSet (Integer, Integer)
      -> HSSet Integer
      -> Maybe Integer
      -> TxBody)
forall a b.
SpecTransM ctx (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> StrictMaybe Network
-> SpecTransM ctx (SpecRep (StrictMaybe Network))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep (TxBody ConwayEra
txb TxBody ConwayEra
-> Getting
     (StrictMaybe Network) (TxBody ConwayEra) (StrictMaybe Network)
-> StrictMaybe Network
forall s a. s -> Getting a s a -> a
^. Getting
  (StrictMaybe Network) (TxBody ConwayEra) (StrictMaybe Network)
forall era.
AlonzoEraTxBody era =>
Lens' (TxBody era) (StrictMaybe Network)
Lens' (TxBody ConwayEra) (StrictMaybe Network)
networkIdTxBodyL)
      SpecTransM
  ctx
  (Maybe Integer
   -> Integer
   -> Integer
   -> HSSet (Integer, Integer)
   -> HSSet Integer
   -> Maybe Integer
   -> TxBody)
-> SpecTransM ctx (Maybe Integer)
-> SpecTransM
     ctx
     (Integer
      -> Integer
      -> HSSet (Integer, Integer)
      -> HSSet Integer
      -> Maybe Integer
      -> TxBody)
forall a b.
SpecTransM ctx (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> StrictMaybe Coin -> SpecTransM ctx (SpecRep (StrictMaybe Coin))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep (TxBody ConwayEra
txb TxBody ConwayEra
-> Getting (StrictMaybe Coin) (TxBody ConwayEra) (StrictMaybe Coin)
-> StrictMaybe Coin
forall s a. s -> Getting a s a -> a
^. Getting (StrictMaybe Coin) (TxBody ConwayEra) (StrictMaybe Coin)
forall era.
ConwayEraTxBody era =>
Lens' (TxBody era) (StrictMaybe Coin)
Lens' (TxBody ConwayEra) (StrictMaybe Coin)
currentTreasuryValueTxBodyL)
      SpecTransM
  ctx
  (Integer
   -> Integer
   -> HSSet (Integer, Integer)
   -> HSSet Integer
   -> Maybe Integer
   -> TxBody)
-> SpecTransM ctx Integer
-> SpecTransM
     ctx
     (Integer
      -> HSSet (Integer, Integer)
      -> HSSet Integer
      -> Maybe Integer
      -> TxBody)
forall a b.
SpecTransM ctx (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Integer -> SpecTransM ctx Integer
forall a. a -> SpecTransM ctx a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Integer
sizeTx
      SpecTransM
  ctx
  (Integer
   -> HSSet (Integer, Integer)
   -> HSSet Integer
   -> Maybe Integer
   -> TxBody)
-> SpecTransM ctx Integer
-> SpecTransM
     ctx
     (HSSet (Integer, Integer)
      -> HSSet Integer -> Maybe Integer -> TxBody)
forall a b.
SpecTransM ctx (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> TxId -> SpecTransM ctx (SpecRep TxId)
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep TxId
txId
      SpecTransM
  ctx
  (HSSet (Integer, Integer)
   -> HSSet Integer -> Maybe Integer -> TxBody)
-> SpecTransM ctx (HSSet (Integer, Integer))
-> SpecTransM ctx (HSSet Integer -> Maybe Integer -> TxBody)
forall a b.
SpecTransM ctx (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Set TxIn -> SpecTransM ctx (SpecRep (Set TxIn))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep (TxBody ConwayEra
txb TxBody ConwayEra
-> Getting (Set TxIn) (TxBody ConwayEra) (Set TxIn) -> Set TxIn
forall s a. s -> Getting a s a -> a
^. Getting (Set TxIn) (TxBody ConwayEra) (Set TxIn)
forall era. AlonzoEraTxBody era => Lens' (TxBody era) (Set TxIn)
Lens' (TxBody ConwayEra) (Set TxIn)
collateralInputsTxBodyL)
      SpecTransM ctx (HSSet Integer -> Maybe Integer -> TxBody)
-> SpecTransM ctx (HSSet Integer)
-> SpecTransM ctx (Maybe Integer -> TxBody)
forall a b.
SpecTransM ctx (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Set (KeyHash 'Witness)
-> SpecTransM ctx (SpecRep (Set (KeyHash 'Witness)))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep (TxBody ConwayEra
txb TxBody ConwayEra
-> Getting
     (Set (KeyHash 'Witness))
     (TxBody ConwayEra)
     (Set (KeyHash 'Witness))
-> Set (KeyHash 'Witness)
forall s a. s -> Getting a s a -> a
^. Getting
  (Set (KeyHash 'Witness))
  (TxBody ConwayEra)
  (Set (KeyHash 'Witness))
forall era.
AlonzoEraTxBody era =>
Lens' (TxBody era) (Set (KeyHash 'Witness))
Lens' (TxBody ConwayEra) (Set (KeyHash 'Witness))
reqSignerHashesTxBodyL)
      SpecTransM ctx (Maybe Integer -> TxBody)
-> SpecTransM ctx (Maybe Integer) -> SpecTransM ctx TxBody
forall a b.
SpecTransM ctx (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> StrictMaybe ScriptIntegrityHash
-> SpecTransM ctx (SpecRep (StrictMaybe ScriptIntegrityHash))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep (TxBody ConwayEra
txb TxBody ConwayEra
-> Getting
     (StrictMaybe ScriptIntegrityHash)
     (TxBody ConwayEra)
     (StrictMaybe ScriptIntegrityHash)
-> StrictMaybe ScriptIntegrityHash
forall s a. s -> Getting a s a -> a
^. Getting
  (StrictMaybe ScriptIntegrityHash)
  (TxBody ConwayEra)
  (StrictMaybe ScriptIntegrityHash)
forall era.
AlonzoEraTxBody era =>
Lens' (TxBody era) (StrictMaybe ScriptIntegrityHash)
Lens' (TxBody ConwayEra) (StrictMaybe ScriptIntegrityHash)
scriptIntegrityHashTxBodyL)