{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE NamedFieldPuns #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TupleSections #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -Wno-orphans #-}

module Test.Cardano.Ledger.Conformance.SpecTranslate.Conway.Base (
  committeeCredentialToStrictMaybe,
  SpecTranslate (..),
  SpecTranslationError,
  ConwayExecEnactEnv (..),
  DepositPurpose (..),
  ConwayTxBodyTransContext (..),
  vkeyToInteger,
  vkeyFromInteger,
  signatureToInteger,
  signatureFromInteger,
) where

import Cardano.Crypto.DSIGN (DSIGNAlgorithm (..), SignedDSIGN (..))
import Cardano.Crypto.Util (bytesToNatural, naturalToBytes)
import Cardano.Ledger.Address (Addr (..), BootstrapAddress (..), RewardAccount (..))
import Cardano.Ledger.Allegra.Scripts (
  Timelock,
  pattern RequireTimeExpire,
  pattern RequireTimeStart,
 )
import Cardano.Ledger.Alonzo (AlonzoTxAuxData, MaryValue)
import Cardano.Ledger.Alonzo.PParams (OrdExUnits (OrdExUnits))
import Cardano.Ledger.Alonzo.Scripts (AlonzoPlutusPurpose (..))
import Cardano.Ledger.Alonzo.Tx (AlonzoTx (..), IsValid (..))
import Cardano.Ledger.Alonzo.TxWits (AlonzoTxWits (..), Redeemers (..), TxDats (..))
import Cardano.Ledger.Babbage.TxOut (BabbageTxOut (..))
import Cardano.Ledger.BaseTypes
import Cardano.Ledger.Binary (Sized (..))
import Cardano.Ledger.Coin (Coin (..), CompactForm)
import Cardano.Ledger.Compactible (Compactible)
import Cardano.Ledger.Conway.Core
import Cardano.Ledger.Conway.Governance
import Cardano.Ledger.Conway.PParams (ConwayPParams (..), THKD (..))
import Cardano.Ledger.Conway.Rules (
  ConwayCertPredFailure,
  ConwayGovPredFailure,
  EnactSignal (..),
  maxRefScriptSizePerBlock,
  maxRefScriptSizePerTx,
 )
import Cardano.Ledger.Conway.Scripts (AlonzoScript (..), ConwayPlutusPurpose (..))
import Cardano.Ledger.Conway.Tx (refScriptCostMultiplier, refScriptCostStride)
import Cardano.Ledger.Credential (Credential (..), StakeReference (..))
import Cardano.Ledger.DRep (DRep (..), DRepState (..))
import Cardano.Ledger.HKD (HKD)
import Cardano.Ledger.Keys (VKey (..))
import Cardano.Ledger.Keys.WitVKey (WitVKey (..))
import Cardano.Ledger.Plutus (CostModels, ExUnits (..), Prices)
import Cardano.Ledger.Plutus.Data (BinaryData, Data, Datum (..), hashBinaryData)
import Cardano.Ledger.PoolParams (PoolParams (..))
import Cardano.Ledger.Shelley.Rules (Identity)
import Cardano.Ledger.Shelley.Scripts (
  pattern RequireAllOf,
  pattern RequireAnyOf,
  pattern RequireMOf,
  pattern RequireSignature,
 )
import Cardano.Ledger.State (
  CommitteeAuthorization (..),
  CommitteeState (..),
  IndividualPoolStake (..),
  PoolDistr (..),
  UTxO (..),
 )
import Cardano.Ledger.TxIn (TxId (..), TxIn (..))
import Cardano.Ledger.UMap (fromCompact)
import Cardano.Ledger.Val (Val (..))
import Constrained.API (HasSimpleRep, HasSpec)
import Control.DeepSeq (NFData)
import Control.Monad.Except (MonadError (..))
import Control.State.Transition.Extended (STS (..))
import Data.Bifunctor (Bifunctor (..))
import Data.Bitraversable (bimapM)
import Data.Default (Default (..))
import Data.Foldable (Foldable (..))
import Data.List (sortOn)
import Data.Map.Strict (Map)
import qualified Data.Map.Strict as Map
import Data.OMap.Strict (OMap)
import qualified Data.OMap.Strict as OMap
import Data.OSet.Strict (OSet)
import Data.Sequence (Seq)
import Data.Sequence.Strict (StrictSeq)
import Data.Set (Set)
import qualified Data.Set as Set
import qualified Data.Text as T
import Data.Traversable (forM)
import Data.Void (Void, absurd)
import Data.Word (Word16, Word32, Word64)
import qualified GHC.Exts as Exts
import GHC.Generics (Generic)
import Lens.Micro
import Lens.Micro.Extras (view)
import qualified MAlonzo.Code.Ledger.Foreign.API as Agda
import Test.Cardano.Ledger.Conformance (
  OpaqueErrorString (..),
  SpecTransM,
  SpecTranslate (..),
  SpecTranslationError,
  askCtx,
  hashToInteger,
  showOpaqueErrorString,
  withCtx,
 )
import Test.Cardano.Ledger.Constrained.Conway (DepositPurpose (..))
import Test.Cardano.Ledger.Constrained.Conway.Epoch
import Test.Cardano.Ledger.Conway.TreeDiff (ToExpr (..), showExpr)

instance SpecTranslate ctx Void where
  type SpecRep Void = Void

  toSpecRep :: Void -> SpecTransM ctx (SpecRep Void)
toSpecRep = forall a. Void -> a
absurd

instance SpecTranslate ctx a => SpecTranslate ctx [a] where
  type SpecRep [a] = [SpecRep a]

  toSpecRep :: [a] -> SpecTransM ctx (SpecRep [a])
toSpecRep = forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep

instance SpecTranslate ctx TxIx where
  type SpecRep TxIx = Integer

  toSpecRep :: TxIx -> SpecTransM ctx (SpecRep TxIx)
toSpecRep (TxIx Word16
x) = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall a. Integral a => a -> Integer
toInteger Word16
x

instance SpecTranslate ctx TxIn where
  type SpecRep TxIn = Agda.TxIn

  toSpecRep :: TxIn -> SpecTransM ctx (SpecRep TxIn)
toSpecRep (TxIn TxId
txId TxIx
txIx) = forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep (TxId
txId, TxIx
txIx)

instance SpecTranslate ctx StakeReference where
  type SpecRep StakeReference = Maybe Agda.Credential

  toSpecRep :: StakeReference -> SpecTransM ctx (SpecRep StakeReference)
toSpecRep (StakeRefBase Credential 'Staking
c) = forall a. a -> Maybe a
Just forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep Credential 'Staking
c
  toSpecRep (StakeRefPtr Ptr
_) = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a. Maybe a
Nothing
  toSpecRep StakeReference
StakeRefNull = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a. Maybe a
Nothing

instance SpecTranslate ctx BootstrapAddress where
  type SpecRep BootstrapAddress = Agda.BootstrapAddr

  toSpecRep :: BootstrapAddress -> SpecTransM ctx (SpecRep BootstrapAddress)
toSpecRep BootstrapAddress
_ = forall a. HasCallStack => [Char] -> a
error [Char]
"Cannot translate bootstrap addresses"

instance SpecTranslate ctx Addr where
  type SpecRep Addr = Agda.Addr

  toSpecRep :: Addr -> SpecTransM ctx (SpecRep Addr)
toSpecRep (Addr Network
nw PaymentCredential
pc StakeReference
sr) =
    forall a b. a -> Either a b
Left
      forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Integer -> Credential -> Maybe Credential -> BaseAddr
Agda.BaseAddr forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep Network
nw 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 PaymentCredential
pc 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 StakeReference
sr)
  toSpecRep (AddrBootstrap BootstrapAddress
ba) = forall a b. b -> Either a b
Right forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep BootstrapAddress
ba

instance SpecTranslate ctx (Hash a b) where
  type SpecRep (Hash a b) = Integer

  toSpecRep :: Hash a b -> SpecTransM ctx (SpecRep (Hash a b))
toSpecRep = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. Hash a b -> Integer
hashToInteger

instance SpecTranslate ctx (SafeHash a) where
  type SpecRep (SafeHash a) = Agda.DataHash

  toSpecRep :: SafeHash a -> SpecTransM ctx (SpecRep (SafeHash a))
toSpecRep = forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall i. SafeHash i -> Hash HASH i
extractHash

instance
  ( SpecRep DataHash ~ Agda.DataHash
  , Era era
  ) =>
  SpecTranslate ctx (BinaryData era)
  where
  type SpecRep (BinaryData era) = Agda.DataHash

  toSpecRep :: BinaryData era -> SpecTransM ctx (SpecRep (BinaryData era))
toSpecRep = forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era. BinaryData era -> DataHash
hashBinaryData

instance Era era => SpecTranslate ctx (Datum era) where
  type SpecRep (Datum era) = Maybe (Either Agda.Datum Agda.DataHash)

  toSpecRep :: Datum era -> SpecTransM ctx (SpecRep (Datum era))
toSpecRep Datum era
NoDatum = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a. Maybe a
Nothing
  toSpecRep (Datum BinaryData era
d) = forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. a -> Either a b
Left forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep BinaryData era
d
  toSpecRep (DatumHash DataHash
h) = forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. b -> Either a b
Right forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep DataHash
h

instance
  ( AlonzoEraScript era
  , NativeScript era ~ Timelock era
  , Script era ~ AlonzoScript era
  ) =>
  SpecTranslate ctx (Timelock era)
  where
  type SpecRep (Timelock era) = Agda.HSTimelock

  toSpecRep :: Timelock era -> SpecTransM ctx (SpecRep (Timelock era))
toSpecRep Timelock era
tl =
    Timelock -> Integer -> Integer -> HSTimelock
Agda.HSTimelock
      forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall {era} {ctx}.
AllegraEraScript era =>
NativeScript era -> SpecTransM ctx Timelock
timelockToSpecRep Timelock era
tl
      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 (forall era. EraScript era => Script era -> ScriptHash
hashScript @era forall a b. (a -> b) -> a -> b
$ forall era. Timelock era -> AlonzoScript era
TimelockScript Timelock era
tl)
      forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall a b. (Integral a, Num b) => a -> b
fromIntegral forall a b. (a -> b) -> a -> b
$ forall t. SafeToHash t => t -> Int
originalBytesSize Timelock era
tl)
    where
      timelockToSpecRep :: NativeScript era -> SpecTransM ctx Timelock
timelockToSpecRep NativeScript era
x =
        case NativeScript era
x of
          RequireSignature KeyHash 'Witness
kh ->
            Integer -> Timelock
Agda.RequireSig forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep KeyHash 'Witness
kh
          RequireAllOf StrictSeq (NativeScript era)
ss -> do
            StrictSeq Timelock
tls <- forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse NativeScript era -> SpecTransM ctx Timelock
timelockToSpecRep StrictSeq (NativeScript era)
ss
            forall (f :: * -> *) a. Applicative f => a -> f a
pure forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Timelock] -> Timelock
Agda.RequireAllOf forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. Foldable t => t a -> [a]
toList StrictSeq Timelock
tls
          RequireAnyOf StrictSeq (NativeScript era)
ss -> do
            StrictSeq Timelock
tls <- forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse NativeScript era -> SpecTransM ctx Timelock
timelockToSpecRep StrictSeq (NativeScript era)
ss
            forall (f :: * -> *) a. Applicative f => a -> f a
pure forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Timelock] -> Timelock
Agda.RequireAnyOf forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. Foldable t => t a -> [a]
toList StrictSeq Timelock
tls
          RequireMOf Int
m StrictSeq (NativeScript era)
ss -> do
            StrictSeq Timelock
tls <- forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse NativeScript era -> SpecTransM ctx Timelock
timelockToSpecRep StrictSeq (NativeScript era)
ss
            forall (f :: * -> *) a. Applicative f => a -> f a
pure forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> [Timelock] -> Timelock
Agda.RequireMOf (forall a. Integral a => a -> Integer
toInteger Int
m) forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. Foldable t => t a -> [a]
toList StrictSeq Timelock
tls
          RequireTimeExpire SlotNo
slot -> Integer -> Timelock
Agda.RequireTimeExpire forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep SlotNo
slot
          RequireTimeStart SlotNo
slot -> Integer -> Timelock
Agda.RequireTimeStart forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep SlotNo
slot

instance
  ( AlonzoEraScript era
  , NativeScript era ~ Timelock era
  , Script era ~ AlonzoScript era
  ) =>
  SpecTranslate ctx (PlutusScript era)
  where
  type SpecRep (PlutusScript era) = Agda.HSPlutusScript

  toSpecRep :: PlutusScript era -> SpecTransM ctx (SpecRep (PlutusScript era))
toSpecRep PlutusScript era
ps =
    Integer -> Integer -> HSPlutusScript
Agda.MkHSPlutusScript
      forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep (forall era. EraScript era => Script era -> ScriptHash
hashScript forall a b. (a -> b) -> a -> b
$ forall era. PlutusScript era -> AlonzoScript era
PlutusScript PlutusScript era
ps)
      forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall a b. (Integral a, Num b) => a -> b
fromIntegral forall a b. (a -> b) -> a -> b
$ forall t. SafeToHash t => t -> Int
originalBytesSize PlutusScript era
ps)

instance
  ( AlonzoEraScript era
  , Script era ~ AlonzoScript era
  , NativeScript era ~ Timelock era
  ) =>
  SpecTranslate ctx (AlonzoScript era)
  where
  type SpecRep (AlonzoScript era) = Agda.Script

  toSpecRep :: AlonzoScript era -> SpecTransM ctx (SpecRep (AlonzoScript era))
toSpecRep (TimelockScript Timelock era
s) = forall a b. a -> Either a b
Left forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep Timelock era
s
  toSpecRep (PlutusScript PlutusScript era
s) = forall a b. b -> Either a b
Right forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep PlutusScript era
s

instance
  ( EraTxOut era
  , SpecRep (Value era) ~ Agda.Coin
  , Script era ~ AlonzoScript era
  , SpecTranslate ctx (Value era)
  , SpecTranslate ctx (Script era)
  ) =>
  SpecTranslate ctx (BabbageTxOut era)
  where
  type SpecRep (BabbageTxOut era) = Agda.TxOut

  toSpecRep :: BabbageTxOut era -> SpecTransM ctx (SpecRep (BabbageTxOut era))
toSpecRep (BabbageTxOut Addr
addr Value era
val Datum era
datum StrictMaybe (Script era)
script) = do
    Either BaseAddr BootstrapAddr
addr' <- forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep Addr
addr
    Integer
val' <- forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep Value era
val
    Maybe (Either Integer Integer)
datum' <- forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep Datum era
datum
    Maybe (Either HSTimelock HSPlutusScript)
script' <- forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep StrictMaybe (Script era)
script
    forall (f :: * -> *) a. Applicative f => a -> f a
pure (Either BaseAddr BootstrapAddr
addr', (Integer
val', (Maybe (Either Integer Integer)
datum', Maybe (Either HSTimelock HSPlutusScript)
script')))

instance SpecTranslate ctx Integer where
  type SpecRep Integer = Integer

  toSpecRep :: Integer -> SpecTransM ctx (SpecRep Integer)
toSpecRep = forall (f :: * -> *) a. Applicative f => a -> f a
pure

deriving instance SpecTranslate ctx Coin

instance
  ( SpecTranslate ctx (TxOut era)
  , SpecRep (TxOut era) ~ Agda.TxOut
  ) =>
  SpecTranslate ctx (UTxO era)
  where
  type SpecRep (UTxO era) = SpecRep (Map TxIn (TxOut era))
  toSpecRep :: UTxO era -> SpecTransM ctx (SpecRep (UTxO era))
toSpecRep (UTxO Map TxIn (TxOut era)
m) = forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep Map TxIn (TxOut era)
m

deriving instance SpecTranslate ctx SlotNo

deriving instance SpecTranslate ctx EpochNo

deriving instance SpecTranslate ctx EpochInterval

instance SpecTranslate ctx ProtVer where
  type SpecRep ProtVer = (Integer, Integer)

  toSpecRep :: ProtVer -> SpecTransM ctx (SpecRep ProtVer)
toSpecRep (ProtVer Version
ver Natural
minor) = forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall i. Integral i => Version -> i
getVersion Version
ver, forall a. Integral a => a -> Integer
toInteger Natural
minor)

instance SpecTranslate ctx CostModels where
  type SpecRep CostModels = ()

  toSpecRep :: CostModels -> SpecTransM ctx (SpecRep CostModels)
toSpecRep CostModels
_ = forall (f :: * -> *) a. Applicative f => a -> f a
pure ()

instance SpecTranslate ctx Prices where
  type SpecRep Prices = ()

  toSpecRep :: Prices -> SpecTransM ctx (SpecRep Prices)
toSpecRep Prices
_ = forall (f :: * -> *) a. Applicative f => a -> f a
pure ()

instance SpecTranslate ctx ExUnits where
  type SpecRep ExUnits = Agda.ExUnits

  toSpecRep :: ExUnits -> SpecTransM ctx (SpecRep ExUnits)
toSpecRep (ExUnits Natural
a Natural
b) = forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall a. Integral a => a -> Integer
toInteger Natural
a, forall a. Integral a => a -> Integer
toInteger Natural
b)

deriving instance SpecTranslate ctx OrdExUnits

deriving instance SpecTranslate ctx CoinPerByte

instance
  SpecTranslate ctx (HKD f a) =>
  SpecTranslate ctx (THKD r f a)
  where
  type SpecRep (THKD r f a) = SpecRep (HKD f a)

  toSpecRep :: THKD r f a -> SpecTransM ctx (SpecRep (THKD r f a))
toSpecRep = forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: PPGroups) (f :: * -> *) a. THKD t f a -> HKD f a
unTHKD

instance SpecTranslate ctx DRepVotingThresholds where
  type SpecRep DRepVotingThresholds = Agda.DrepThresholds

  toSpecRep :: DRepVotingThresholds
-> SpecTransM ctx (SpecRep DRepVotingThresholds)
toSpecRep DRepVotingThresholds {UnitInterval
dvtMotionNoConfidence :: DRepVotingThresholds -> UnitInterval
dvtCommitteeNormal :: DRepVotingThresholds -> UnitInterval
dvtCommitteeNoConfidence :: DRepVotingThresholds -> UnitInterval
dvtUpdateToConstitution :: DRepVotingThresholds -> UnitInterval
dvtHardForkInitiation :: DRepVotingThresholds -> UnitInterval
dvtPPNetworkGroup :: DRepVotingThresholds -> UnitInterval
dvtPPEconomicGroup :: DRepVotingThresholds -> UnitInterval
dvtPPTechnicalGroup :: DRepVotingThresholds -> UnitInterval
dvtPPGovGroup :: DRepVotingThresholds -> UnitInterval
dvtTreasuryWithdrawal :: DRepVotingThresholds -> UnitInterval
dvtTreasuryWithdrawal :: UnitInterval
dvtPPGovGroup :: UnitInterval
dvtPPTechnicalGroup :: UnitInterval
dvtPPEconomicGroup :: UnitInterval
dvtPPNetworkGroup :: UnitInterval
dvtHardForkInitiation :: UnitInterval
dvtUpdateToConstitution :: UnitInterval
dvtCommitteeNoConfidence :: UnitInterval
dvtCommitteeNormal :: UnitInterval
dvtMotionNoConfidence :: UnitInterval
..} =
    Rational
-> Rational
-> Rational
-> Rational
-> Rational
-> Rational
-> Rational
-> Rational
-> Rational
-> Rational
-> DrepThresholds
Agda.MkDrepThresholds
      forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep UnitInterval
dvtMotionNoConfidence
      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 UnitInterval
dvtCommitteeNormal
      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 UnitInterval
dvtCommitteeNoConfidence
      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 UnitInterval
dvtUpdateToConstitution
      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 UnitInterval
dvtHardForkInitiation
      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 UnitInterval
dvtPPNetworkGroup
      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 UnitInterval
dvtPPEconomicGroup
      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 UnitInterval
dvtPPTechnicalGroup
      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 UnitInterval
dvtPPGovGroup
      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 UnitInterval
dvtTreasuryWithdrawal

instance SpecTranslate ctx PoolVotingThresholds where
  type SpecRep PoolVotingThresholds = Agda.PoolThresholds

  toSpecRep :: PoolVotingThresholds
-> SpecTransM ctx (SpecRep PoolVotingThresholds)
toSpecRep PoolVotingThresholds {UnitInterval
pvtMotionNoConfidence :: PoolVotingThresholds -> UnitInterval
pvtCommitteeNormal :: PoolVotingThresholds -> UnitInterval
pvtCommitteeNoConfidence :: PoolVotingThresholds -> UnitInterval
pvtHardForkInitiation :: PoolVotingThresholds -> UnitInterval
pvtPPSecurityGroup :: PoolVotingThresholds -> UnitInterval
pvtPPSecurityGroup :: UnitInterval
pvtHardForkInitiation :: UnitInterval
pvtCommitteeNoConfidence :: UnitInterval
pvtCommitteeNormal :: UnitInterval
pvtMotionNoConfidence :: UnitInterval
..} =
    Rational
-> Rational -> Rational -> Rational -> Rational -> PoolThresholds
Agda.MkPoolThresholds
      forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep UnitInterval
pvtMotionNoConfidence
      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 UnitInterval
pvtCommitteeNormal
      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 UnitInterval
pvtCommitteeNoConfidence
      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 UnitInterval
pvtHardForkInitiation
      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 UnitInterval
pvtPPSecurityGroup

instance SpecTranslate ctx (ConwayPParams Identity era) where
  type SpecRep (ConwayPParams Identity era) = Agda.PParams

  toSpecRep :: ConwayPParams Identity era
-> SpecTransM ctx (SpecRep (ConwayPParams Identity era))
toSpecRep ConwayPParams {THKD ('PPGroups 'GovGroup 'NoStakePoolGroup) Identity Word16
THKD ('PPGroups 'GovGroup 'NoStakePoolGroup) Identity Coin
THKD
  ('PPGroups 'GovGroup 'NoStakePoolGroup)
  Identity
  PoolVotingThresholds
THKD
  ('PPGroups 'GovGroup 'NoStakePoolGroup)
  Identity
  DRepVotingThresholds
THKD ('PPGroups 'GovGroup 'NoStakePoolGroup) Identity EpochInterval
THKD ('PPGroups 'GovGroup 'SecurityGroup) Identity Coin
THKD ('PPGroups 'TechnicalGroup 'NoStakePoolGroup) Identity Word16
THKD
  ('PPGroups 'TechnicalGroup 'NoStakePoolGroup) Identity CostModels
THKD
  ('PPGroups 'TechnicalGroup 'NoStakePoolGroup)
  Identity
  NonNegativeInterval
THKD
  ('PPGroups 'TechnicalGroup 'NoStakePoolGroup)
  Identity
  EpochInterval
THKD ('PPGroups 'EconomicGroup 'NoStakePoolGroup) Identity Prices
THKD ('PPGroups 'EconomicGroup 'NoStakePoolGroup) Identity Coin
THKD
  ('PPGroups 'EconomicGroup 'NoStakePoolGroup) Identity UnitInterval
THKD ('PPGroups 'EconomicGroup 'SecurityGroup) Identity Coin
THKD ('PPGroups 'EconomicGroup 'SecurityGroup) Identity CoinPerByte
THKD
  ('PPGroups 'EconomicGroup 'SecurityGroup)
  Identity
  NonNegativeInterval
THKD ('PPGroups 'NetworkGroup 'NoStakePoolGroup) Identity Word16
THKD
  ('PPGroups 'NetworkGroup 'NoStakePoolGroup) Identity OrdExUnits
THKD ('PPGroups 'NetworkGroup 'SecurityGroup) Identity Word16
THKD ('PPGroups 'NetworkGroup 'SecurityGroup) Identity Word32
THKD ('PPGroups 'NetworkGroup 'SecurityGroup) Identity OrdExUnits
HKDNoUpdate Identity ProtVer
cppMinFeeA :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD ('PPGroups 'EconomicGroup 'SecurityGroup) f Coin
cppMinFeeB :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD ('PPGroups 'EconomicGroup 'SecurityGroup) f Coin
cppMaxBBSize :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD ('PPGroups 'NetworkGroup 'SecurityGroup) f Word32
cppMaxTxSize :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD ('PPGroups 'NetworkGroup 'SecurityGroup) f Word32
cppMaxBHSize :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD ('PPGroups 'NetworkGroup 'SecurityGroup) f Word16
cppKeyDeposit :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD ('PPGroups 'EconomicGroup 'NoStakePoolGroup) f Coin
cppPoolDeposit :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD ('PPGroups 'EconomicGroup 'NoStakePoolGroup) f Coin
cppEMax :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD
     ('PPGroups 'TechnicalGroup 'NoStakePoolGroup) f EpochInterval
cppNOpt :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD ('PPGroups 'TechnicalGroup 'NoStakePoolGroup) f Word16
cppA0 :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD
     ('PPGroups 'TechnicalGroup 'NoStakePoolGroup) f NonNegativeInterval
cppRho :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD ('PPGroups 'EconomicGroup 'NoStakePoolGroup) f UnitInterval
cppTau :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD ('PPGroups 'EconomicGroup 'NoStakePoolGroup) f UnitInterval
cppProtocolVersion :: forall (f :: * -> *) era.
ConwayPParams f era -> HKDNoUpdate f ProtVer
cppMinPoolCost :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD ('PPGroups 'EconomicGroup 'NoStakePoolGroup) f Coin
cppCoinsPerUTxOByte :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD ('PPGroups 'EconomicGroup 'SecurityGroup) f CoinPerByte
cppCostModels :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD ('PPGroups 'TechnicalGroup 'NoStakePoolGroup) f CostModels
cppPrices :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD ('PPGroups 'EconomicGroup 'NoStakePoolGroup) f Prices
cppMaxTxExUnits :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD ('PPGroups 'NetworkGroup 'NoStakePoolGroup) f OrdExUnits
cppMaxBlockExUnits :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD ('PPGroups 'NetworkGroup 'SecurityGroup) f OrdExUnits
cppMaxValSize :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD ('PPGroups 'NetworkGroup 'SecurityGroup) f Word32
cppCollateralPercentage :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD ('PPGroups 'TechnicalGroup 'NoStakePoolGroup) f Word16
cppMaxCollateralInputs :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD ('PPGroups 'NetworkGroup 'NoStakePoolGroup) f Word16
cppPoolVotingThresholds :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD
     ('PPGroups 'GovGroup 'NoStakePoolGroup) f PoolVotingThresholds
cppDRepVotingThresholds :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD
     ('PPGroups 'GovGroup 'NoStakePoolGroup) f DRepVotingThresholds
cppCommitteeMinSize :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD ('PPGroups 'GovGroup 'NoStakePoolGroup) f Word16
cppCommitteeMaxTermLength :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD ('PPGroups 'GovGroup 'NoStakePoolGroup) f EpochInterval
cppGovActionLifetime :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD ('PPGroups 'GovGroup 'NoStakePoolGroup) f EpochInterval
cppGovActionDeposit :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD ('PPGroups 'GovGroup 'SecurityGroup) f Coin
cppDRepDeposit :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD ('PPGroups 'GovGroup 'NoStakePoolGroup) f Coin
cppDRepActivity :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD ('PPGroups 'GovGroup 'NoStakePoolGroup) f EpochInterval
cppMinFeeRefScriptCostPerByte :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD
     ('PPGroups 'EconomicGroup 'SecurityGroup) f NonNegativeInterval
cppMinFeeRefScriptCostPerByte :: THKD
  ('PPGroups 'EconomicGroup 'SecurityGroup)
  Identity
  NonNegativeInterval
cppDRepActivity :: THKD ('PPGroups 'GovGroup 'NoStakePoolGroup) Identity EpochInterval
cppDRepDeposit :: THKD ('PPGroups 'GovGroup 'NoStakePoolGroup) Identity Coin
cppGovActionDeposit :: THKD ('PPGroups 'GovGroup 'SecurityGroup) Identity Coin
cppGovActionLifetime :: THKD ('PPGroups 'GovGroup 'NoStakePoolGroup) Identity EpochInterval
cppCommitteeMaxTermLength :: THKD ('PPGroups 'GovGroup 'NoStakePoolGroup) Identity EpochInterval
cppCommitteeMinSize :: THKD ('PPGroups 'GovGroup 'NoStakePoolGroup) Identity Word16
cppDRepVotingThresholds :: THKD
  ('PPGroups 'GovGroup 'NoStakePoolGroup)
  Identity
  DRepVotingThresholds
cppPoolVotingThresholds :: THKD
  ('PPGroups 'GovGroup 'NoStakePoolGroup)
  Identity
  PoolVotingThresholds
cppMaxCollateralInputs :: THKD ('PPGroups 'NetworkGroup 'NoStakePoolGroup) Identity Word16
cppCollateralPercentage :: THKD ('PPGroups 'TechnicalGroup 'NoStakePoolGroup) Identity Word16
cppMaxValSize :: THKD ('PPGroups 'NetworkGroup 'SecurityGroup) Identity Word32
cppMaxBlockExUnits :: THKD ('PPGroups 'NetworkGroup 'SecurityGroup) Identity OrdExUnits
cppMaxTxExUnits :: THKD
  ('PPGroups 'NetworkGroup 'NoStakePoolGroup) Identity OrdExUnits
cppPrices :: THKD ('PPGroups 'EconomicGroup 'NoStakePoolGroup) Identity Prices
cppCostModels :: THKD
  ('PPGroups 'TechnicalGroup 'NoStakePoolGroup) Identity CostModels
cppCoinsPerUTxOByte :: THKD ('PPGroups 'EconomicGroup 'SecurityGroup) Identity CoinPerByte
cppMinPoolCost :: THKD ('PPGroups 'EconomicGroup 'NoStakePoolGroup) Identity Coin
cppProtocolVersion :: HKDNoUpdate Identity ProtVer
cppTau :: THKD
  ('PPGroups 'EconomicGroup 'NoStakePoolGroup) Identity UnitInterval
cppRho :: THKD
  ('PPGroups 'EconomicGroup 'NoStakePoolGroup) Identity UnitInterval
cppA0 :: THKD
  ('PPGroups 'TechnicalGroup 'NoStakePoolGroup)
  Identity
  NonNegativeInterval
cppNOpt :: THKD ('PPGroups 'TechnicalGroup 'NoStakePoolGroup) Identity Word16
cppEMax :: THKD
  ('PPGroups 'TechnicalGroup 'NoStakePoolGroup)
  Identity
  EpochInterval
cppPoolDeposit :: THKD ('PPGroups 'EconomicGroup 'NoStakePoolGroup) Identity Coin
cppKeyDeposit :: THKD ('PPGroups 'EconomicGroup 'NoStakePoolGroup) Identity Coin
cppMaxBHSize :: THKD ('PPGroups 'NetworkGroup 'SecurityGroup) Identity Word16
cppMaxTxSize :: THKD ('PPGroups 'NetworkGroup 'SecurityGroup) Identity Word32
cppMaxBBSize :: THKD ('PPGroups 'NetworkGroup 'SecurityGroup) Identity Word32
cppMinFeeB :: THKD ('PPGroups 'EconomicGroup 'SecurityGroup) Identity Coin
cppMinFeeA :: THKD ('PPGroups 'EconomicGroup 'SecurityGroup) Identity Coin
..} = do
    Integer
ppA <- forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep THKD ('PPGroups 'EconomicGroup 'SecurityGroup) Identity Coin
cppMinFeeA
    Integer
ppB <- forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep THKD ('PPGroups 'EconomicGroup 'SecurityGroup) Identity Coin
cppMinFeeB
    Rational
ppA0 <- forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep THKD
  ('PPGroups 'TechnicalGroup 'NoStakePoolGroup)
  Identity
  NonNegativeInterval
cppA0
    Rational
ppMinFeeRefScriptCoinsPerByte <- forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep THKD
  ('PPGroups 'EconomicGroup 'SecurityGroup)
  Identity
  NonNegativeInterval
cppMinFeeRefScriptCostPerByte
    Integer
ppCollateralPercentage <- forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep THKD ('PPGroups 'TechnicalGroup 'NoStakePoolGroup) Identity Word16
cppCollateralPercentage
    let
      ppMaxBlockSize :: Integer
ppMaxBlockSize = forall a. Integral a => a -> Integer
toInteger forall a b. (a -> b) -> a -> b
$ forall (t :: PPGroups) (f :: * -> *) a. THKD t f a -> HKD f a
unTHKD THKD ('PPGroups 'NetworkGroup 'SecurityGroup) Identity Word32
cppMaxBBSize
      ppMaxTxSize :: Integer
ppMaxTxSize = forall a. Integral a => a -> Integer
toInteger forall a b. (a -> b) -> a -> b
$ forall (t :: PPGroups) (f :: * -> *) a. THKD t f a -> HKD f a
unTHKD THKD ('PPGroups 'NetworkGroup 'SecurityGroup) Identity Word32
cppMaxTxSize
      ppMaxHeaderSize :: Integer
ppMaxHeaderSize = forall a. Integral a => a -> Integer
toInteger forall a b. (a -> b) -> a -> b
$ forall (t :: PPGroups) (f :: * -> *) a. THKD t f a -> HKD f a
unTHKD THKD ('PPGroups 'NetworkGroup 'SecurityGroup) Identity Word16
cppMaxBHSize
    Integer
ppKeyDeposit <- forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep THKD ('PPGroups 'EconomicGroup 'NoStakePoolGroup) Identity Coin
cppKeyDeposit
    Integer
ppPoolDeposit <- forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep THKD ('PPGroups 'EconomicGroup 'NoStakePoolGroup) Identity Coin
cppPoolDeposit
    Integer
ppEmax <- forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep THKD
  ('PPGroups 'TechnicalGroup 'NoStakePoolGroup)
  Identity
  EpochInterval
cppEMax
    Integer
ppNopt <- forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep (forall a. Integral a => a -> Integer
toInteger forall a b. (a -> b) -> a -> b
$ forall (t :: PPGroups) (f :: * -> *) a. THKD t f a -> HKD f a
unTHKD THKD ('PPGroups 'TechnicalGroup 'NoStakePoolGroup) Identity Word16
cppNOpt)
    let
      -- We don't really care about `ppPv` in conformance testing, because
      -- the actual protocol version is stored elsewhere starting from Conway
      -- and this is just here for backwards compatibility
      ppPv :: ExUnits
ppPv = (Integer
0, Integer
0)
      ppMinUTxOValue :: Integer
ppMinUTxOValue = Integer
0 -- minUTxOValue has been deprecated and is not supported in Conway
    Integer
ppCoinsPerUTxOByte <- forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep THKD ('PPGroups 'EconomicGroup 'SecurityGroup) Identity CoinPerByte
cppCoinsPerUTxOByte
    ()
ppCostmdls <- forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep THKD
  ('PPGroups 'TechnicalGroup 'NoStakePoolGroup) Identity CostModels
cppCostModels
    ()
ppPrices <- forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep THKD ('PPGroups 'EconomicGroup 'NoStakePoolGroup) Identity Prices
cppPrices
    let
      ppMaxRefScriptSizePerTx :: Integer
ppMaxRefScriptSizePerTx = forall a. Integral a => a -> Integer
toInteger Int
maxRefScriptSizePerTx
      ppMaxRefScriptSizePerBlock :: Integer
ppMaxRefScriptSizePerBlock = forall a. Integral a => a -> Integer
toInteger Int
maxRefScriptSizePerBlock
      ppRefScriptCostStride :: Integer
ppRefScriptCostStride = forall a. Integral a => a -> Integer
toInteger Int
refScriptCostStride
      ppRefScriptCostMultiplier :: Rational
ppRefScriptCostMultiplier = Rational
refScriptCostMultiplier
    ExUnits
ppMaxTxExUnits <- forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep THKD
  ('PPGroups 'NetworkGroup 'NoStakePoolGroup) Identity OrdExUnits
cppMaxTxExUnits
    ExUnits
ppMaxBlockExUnits <- forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep THKD ('PPGroups 'NetworkGroup 'SecurityGroup) Identity OrdExUnits
cppMaxBlockExUnits
    let
      ppMaxValSize :: Integer
ppMaxValSize = forall a. Integral a => a -> Integer
toInteger forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: PPGroups) (f :: * -> *) a. THKD t f a -> HKD f a
unTHKD forall a b. (a -> b) -> a -> b
$ THKD ('PPGroups 'NetworkGroup 'SecurityGroup) Identity Word32
cppMaxValSize
      ppMaxCollateralInputs :: Integer
ppMaxCollateralInputs = forall a. Integral a => a -> Integer
toInteger forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: PPGroups) (f :: * -> *) a. THKD t f a -> HKD f a
unTHKD forall a b. (a -> b) -> a -> b
$ THKD ('PPGroups 'NetworkGroup 'NoStakePoolGroup) Identity Word16
cppMaxCollateralInputs
    PoolThresholds
ppPoolThresholds <- forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep THKD
  ('PPGroups 'GovGroup 'NoStakePoolGroup)
  Identity
  PoolVotingThresholds
cppPoolVotingThresholds
    DrepThresholds
ppDrepThresholds <- forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep THKD
  ('PPGroups 'GovGroup 'NoStakePoolGroup)
  Identity
  DRepVotingThresholds
cppDRepVotingThresholds
    let
      ppCcMinSize :: Integer
ppCcMinSize = forall a. Integral a => a -> Integer
toInteger forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: PPGroups) (f :: * -> *) a. THKD t f a -> HKD f a
unTHKD forall a b. (a -> b) -> a -> b
$ THKD ('PPGroups 'GovGroup 'NoStakePoolGroup) Identity Word16
cppCommitteeMinSize
      ppCcMaxTermLength :: Integer
ppCcMaxTermLength = forall a. Integral a => a -> Integer
toInteger forall b c a. (b -> c) -> (a -> b) -> a -> c
. EpochInterval -> Word32
unEpochInterval forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: PPGroups) (f :: * -> *) a. THKD t f a -> HKD f a
unTHKD forall a b. (a -> b) -> a -> b
$ THKD ('PPGroups 'GovGroup 'NoStakePoolGroup) Identity EpochInterval
cppCommitteeMaxTermLength
    Integer
ppGovActionLifetime <- forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep THKD ('PPGroups 'GovGroup 'NoStakePoolGroup) Identity EpochInterval
cppGovActionLifetime
    Integer
ppGovActionDeposit <- forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep THKD ('PPGroups 'GovGroup 'SecurityGroup) Identity Coin
cppGovActionDeposit
    Integer
ppDrepDeposit <- forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep THKD ('PPGroups 'GovGroup 'NoStakePoolGroup) Identity Coin
cppDRepDeposit
    Integer
ppDrepActivity <- forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep THKD ('PPGroups 'GovGroup 'NoStakePoolGroup) Identity EpochInterval
cppDRepActivity
    Rational
ppMonetaryExpansion <- forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep THKD
  ('PPGroups 'EconomicGroup 'NoStakePoolGroup) Identity UnitInterval
cppRho
    Rational
ppTreasuryCut <- forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep THKD
  ('PPGroups 'EconomicGroup 'NoStakePoolGroup) Identity UnitInterval
cppTau

    forall (f :: * -> *) a. Applicative f => a -> f a
pure Agda.MkPParams {Integer
Rational
()
ExUnits
DrepThresholds
PoolThresholds
ppMaxBlockSize :: Integer
ppMaxTxSize :: Integer
ppMaxHeaderSize :: Integer
ppMaxTxExUnits :: ExUnits
ppMaxBlockExUnits :: ExUnits
ppMaxValSize :: Integer
ppMaxCollateralInputs :: Integer
ppPv :: ExUnits
ppA :: Integer
ppB :: Integer
ppKeyDeposit :: Integer
ppPoolDeposit :: Integer
ppMonetaryExpansion :: Rational
ppTreasuryCut :: Rational
ppCoinsPerUTxOByte :: Integer
ppPrices :: ()
ppMinFeeRefScriptCoinsPerByte :: Rational
ppMaxRefScriptSizePerTx :: Integer
ppMaxRefScriptSizePerBlock :: Integer
ppRefScriptCostStride :: Integer
ppRefScriptCostMultiplier :: Rational
ppMinUTxOValue :: Integer
ppEmax :: Integer
ppNopt :: Integer
ppA0 :: Rational
ppCollateralPercentage :: Integer
ppCostmdls :: ()
ppPoolThresholds :: PoolThresholds
ppDrepThresholds :: DrepThresholds
ppCcMinSize :: Integer
ppCcMaxTermLength :: Integer
ppGovActionLifetime :: Integer
ppGovActionDeposit :: Integer
ppDrepDeposit :: Integer
ppDrepActivity :: Integer
ppTreasuryCut :: Rational
ppMonetaryExpansion :: Rational
ppDrepActivity :: Integer
ppDrepDeposit :: Integer
ppGovActionDeposit :: Integer
ppGovActionLifetime :: Integer
ppCcMaxTermLength :: Integer
ppCcMinSize :: Integer
ppDrepThresholds :: DrepThresholds
ppPoolThresholds :: PoolThresholds
ppMaxCollateralInputs :: Integer
ppMaxValSize :: Integer
ppMaxBlockExUnits :: ExUnits
ppMaxTxExUnits :: ExUnits
ppRefScriptCostMultiplier :: Rational
ppRefScriptCostStride :: Integer
ppMaxRefScriptSizePerBlock :: Integer
ppMaxRefScriptSizePerTx :: Integer
ppPrices :: ()
ppCostmdls :: ()
ppCoinsPerUTxOByte :: Integer
ppMinUTxOValue :: Integer
ppPv :: ExUnits
ppNopt :: Integer
ppEmax :: Integer
ppPoolDeposit :: Integer
ppKeyDeposit :: Integer
ppMaxHeaderSize :: Integer
ppMaxTxSize :: Integer
ppMaxBlockSize :: Integer
ppCollateralPercentage :: Integer
ppMinFeeRefScriptCoinsPerByte :: Rational
ppA0 :: Rational
ppB :: Integer
ppA :: Integer
..}

instance
  SpecTranslate ctx (PParamsHKD Identity era) =>
  SpecTranslate ctx (PParams era)
  where
  type SpecRep (PParams era) = SpecRep (PParamsHKD Identity era)

  toSpecRep :: PParams era -> SpecTransM ctx (SpecRep (PParams era))
toSpecRep (PParams PParamsHKD Identity era
x) = forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep PParamsHKD Identity era
x

instance SpecTranslate ctx a => SpecTranslate ctx (Set a) where
  type SpecRep (Set a) = Agda.HSSet (SpecRep a)

  toSpecRep :: Set a -> SpecTransM ctx (SpecRep (Set a))
toSpecRep = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. [a] -> HSSet a
Agda.MkHSSet forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Set a -> [a]
Set.toList

instance SpecTranslate ctx a => SpecTranslate ctx (StrictSeq a) where
  type SpecRep (StrictSeq a) = [SpecRep a]

  toSpecRep :: StrictSeq a -> SpecTransM ctx (SpecRep (StrictSeq a))
toSpecRep = forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) a. Foldable t => t a -> [a]
toList

instance SpecTranslate ctx a => SpecTranslate ctx (Seq a) where
  type SpecRep (Seq a) = [SpecRep a]

  toSpecRep :: Seq a -> SpecTransM ctx (SpecRep (Seq a))
toSpecRep = forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) a. Foldable t => t a -> [a]
toList

instance SpecTranslate ctx a => SpecTranslate ctx (Sized a) where
  type SpecRep (Sized a) = SpecRep a

  toSpecRep :: Sized a -> SpecTransM ctx (SpecRep (Sized a))
toSpecRep (Sized a
x Int64
_) = forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep a
x

instance SpecTranslate ctx ValidityInterval where
  type SpecRep ValidityInterval = (Maybe Integer, Maybe Integer)

  toSpecRep :: ValidityInterval -> SpecTransM ctx (SpecRep ValidityInterval)
toSpecRep (ValidityInterval StrictMaybe SlotNo
lo StrictMaybe SlotNo
hi) = forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep (StrictMaybe SlotNo
lo, StrictMaybe SlotNo
hi)

instance SpecTranslate ctx (KeyHash r) where
  type SpecRep (KeyHash r) = Integer

  toSpecRep :: KeyHash r -> SpecTransM ctx (SpecRep (KeyHash r))
toSpecRep (KeyHash Hash ADDRHASH (VerKeyDSIGN DSIGN)
h) = forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep Hash ADDRHASH (VerKeyDSIGN DSIGN)
h

vkeyToInteger :: VKey kd -> Integer
vkeyToInteger :: forall (kd :: KeyRole). VKey kd -> Integer
vkeyToInteger = forall a. Integral a => a -> Integer
toInteger forall b c a. (b -> c) -> (a -> b) -> a -> c
. ByteString -> Natural
bytesToNatural forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall v. DSIGNAlgorithm v => VerKeyDSIGN v -> ByteString
rawSerialiseVerKeyDSIGN forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (kd :: KeyRole). VKey kd -> VerKeyDSIGN DSIGN
unVKey

vkeyFromInteger :: Integer -> Maybe (VKey kd)
vkeyFromInteger :: forall (kd :: KeyRole). Integer -> Maybe (VKey kd)
vkeyFromInteger = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall (kd :: KeyRole). VerKeyDSIGN DSIGN -> VKey kd
VKey forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall v. DSIGNAlgorithm v => ByteString -> Maybe (VerKeyDSIGN v)
rawDeserialiseVerKeyDSIGN forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Natural -> ByteString
naturalToBytes Int
32 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Num a => Integer -> a
fromInteger

signatureToInteger :: DSIGNAlgorithm v => SigDSIGN v -> Integer
signatureToInteger :: forall v. DSIGNAlgorithm v => SigDSIGN v -> Integer
signatureToInteger = forall a. Integral a => a -> Integer
toInteger forall b c a. (b -> c) -> (a -> b) -> a -> c
. ByteString -> Natural
bytesToNatural forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall v. DSIGNAlgorithm v => SigDSIGN v -> ByteString
rawSerialiseSigDSIGN

signatureFromInteger :: DSIGNAlgorithm v => Integer -> Maybe (SigDSIGN v)
signatureFromInteger :: forall v. DSIGNAlgorithm v => Integer -> Maybe (SigDSIGN v)
signatureFromInteger = forall v. DSIGNAlgorithm v => ByteString -> Maybe (SigDSIGN v)
rawDeserialiseSigDSIGN forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Natural -> ByteString
naturalToBytes Int
64 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Num a => Integer -> a
fromInteger

instance SpecTranslate ctx (VKey k) where
  type SpecRep (VKey k) = Agda.HSVKey

  toSpecRep :: VKey k -> SpecTransM ctx (SpecRep (VKey k))
toSpecRep VKey k
x = do
    let hvkVKey :: Integer
hvkVKey = forall (kd :: KeyRole). VKey kd -> Integer
vkeyToInteger VKey k
x
    Integer
hvkStoredHash <- forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep (forall v h.
(DSIGNAlgorithm v, HashAlgorithm h) =>
VerKeyDSIGN v -> Hash h (VerKeyDSIGN v)
hashVerKeyDSIGN @_ @ADDRHASH forall a b. (a -> b) -> a -> b
$ forall (kd :: KeyRole). VKey kd -> VerKeyDSIGN DSIGN
unVKey VKey k
x)
    forall (f :: * -> *) a. Applicative f => a -> f a
pure Agda.MkHSVKey {Integer
hvkVKey :: Integer
hvkStoredHash :: Integer
hvkStoredHash :: Integer
hvkVKey :: Integer
..}

instance DSIGNAlgorithm v => SpecTranslate ctx (SignedDSIGN v a) where
  type SpecRep (SignedDSIGN v a) = Integer

  toSpecRep :: SignedDSIGN v a -> SpecTransM ctx (SpecRep (SignedDSIGN v a))
toSpecRep (SignedDSIGN SigDSIGN v
x) = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall v. DSIGNAlgorithm v => SigDSIGN v -> Integer
signatureToInteger SigDSIGN v
x

instance SpecTranslate ctx (WitVKey k) where
  type SpecRep (WitVKey k) = (SpecRep (VKey k), Integer)

  toSpecRep :: WitVKey k -> SpecTransM ctx (SpecRep (WitVKey k))
toSpecRep (WitVKey VKey k
vk SignedDSIGN DSIGN (Hash HASH EraIndependentTxBody)
sk) = forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep (VKey k
vk, SignedDSIGN DSIGN (Hash HASH EraIndependentTxBody)
sk)

instance Era era => SpecTranslate ctx (TxDats era) where
  type SpecRep (TxDats era) = Agda.HSMap Agda.DataHash Agda.Datum

  toSpecRep :: TxDats era -> SpecTransM ctx (SpecRep (TxDats era))
toSpecRep (TxDats Map DataHash (Data era)
x) = forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep Map DataHash (Data era)
x

instance
  ( SpecTranslate ctx k
  , SpecTranslate ctx v
  ) =>
  SpecTranslate ctx (Map k v)
  where
  type SpecRep (Map k v) = Agda.HSMap (SpecRep k) (SpecRep v)

  toSpecRep :: Map k v -> SpecTransM ctx (SpecRep (Map k v))
toSpecRep = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall k v. [(k, v)] -> HSMap k v
Agda.MkHSMap forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (forall (t :: * -> * -> *) (f :: * -> *) a c b d.
(Bitraversable t, Applicative f) =>
(a -> f c) -> (b -> f d) -> t a b -> f (t c d)
bimapM forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k a. Map k a -> [(k, a)]
Map.toList

instance SpecTranslate ctx Word64 where
  type SpecRep Word64 = Integer

  toSpecRep :: Word64 -> SpecTransM ctx (SpecRep Word64)
toSpecRep = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Integral a => a -> Integer
toInteger

instance SpecTranslate ctx Word32 where
  type SpecRep Word32 = Integer

  toSpecRep :: Word32 -> SpecTransM ctx (SpecRep Word32)
toSpecRep = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Integral a => a -> Integer
toInteger

instance SpecTranslate ctx (AlonzoPlutusPurpose AsIx era) where
  type SpecRep (AlonzoPlutusPurpose AsIx era) = Agda.RdmrPtr

  toSpecRep :: AlonzoPlutusPurpose AsIx era
-> SpecTransM ctx (SpecRep (AlonzoPlutusPurpose AsIx era))
toSpecRep = \case
    AlonzoSpending (AsIx Word32
i) -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (Tag
Agda.Spend, forall a. Integral a => a -> Integer
toInteger Word32
i)
    AlonzoMinting (AsIx Word32
i) -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (Tag
Agda.Mint, forall a. Integral a => a -> Integer
toInteger Word32
i)
    AlonzoCertifying (AsIx Word32
i) -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (Tag
Agda.Cert, forall a. Integral a => a -> Integer
toInteger Word32
i)
    AlonzoRewarding (AsIx Word32
i) -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (Tag
Agda.Rewrd, forall a. Integral a => a -> Integer
toInteger Word32
i)

instance SpecTranslate ctx (ConwayPlutusPurpose AsIx era) where
  type SpecRep (ConwayPlutusPurpose AsIx era) = Agda.RdmrPtr

  toSpecRep :: ConwayPlutusPurpose AsIx era
-> SpecTransM ctx (SpecRep (ConwayPlutusPurpose AsIx era))
toSpecRep = \case
    ConwaySpending (AsIx Word32
i) -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (Tag
Agda.Spend, forall a. Integral a => a -> Integer
toInteger Word32
i)
    ConwayMinting (AsIx Word32
i) -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (Tag
Agda.Mint, forall a. Integral a => a -> Integer
toInteger Word32
i)
    ConwayCertifying (AsIx Word32
i) -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (Tag
Agda.Cert, forall a. Integral a => a -> Integer
toInteger Word32
i)
    ConwayRewarding (AsIx Word32
i) -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (Tag
Agda.Rewrd, forall a. Integral a => a -> Integer
toInteger Word32
i)
    ConwayVoting (AsIx Word32
i) -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (Tag
Agda.Vote, forall a. Integral a => a -> Integer
toInteger Word32
i)
    ConwayProposing (AsIx Word32
i) -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (Tag
Agda.Propose, forall a. Integral a => a -> Integer
toInteger Word32
i)

instance
  ( SpecTranslate ctx a
  , SpecTranslate ctx b
  ) =>
  SpecTranslate ctx (a, b)
  where
  type SpecRep (a, b) = (SpecRep a, SpecRep b)

  toSpecRep :: (a, b) -> SpecTransM ctx (SpecRep (a, b))
toSpecRep (a
x, b
y) = (,) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep a
x 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 b
y

instance Era era => SpecTranslate ctx (Data era) where
  type SpecRep (Data era) = Agda.DataHash

  toSpecRep :: Data era -> SpecTransM ctx (SpecRep (Data era))
toSpecRep = forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall x i. HashAnnotated x i => x -> SafeHash i
hashAnnotated

instance
  ( AlonzoEraScript era
  , SpecTranslate ctx (PlutusPurpose AsIx era)
  ) =>
  SpecTranslate ctx (Redeemers era)
  where
  type
    SpecRep (Redeemers era) =
      Agda.HSMap (SpecRep (PlutusPurpose AsIx era)) (Agda.Redeemer, Agda.ExUnits)

  toSpecRep :: Redeemers era -> SpecTransM ctx (SpecRep (Redeemers era))
toSpecRep (Redeemers Map (PlutusPurpose AsIx era) (Data era, ExUnits)
x) = forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep Map (PlutusPurpose AsIx era) (Data era, ExUnits)
x

instance
  ( AlonzoEraScript era
  , SpecTranslate ctx (PlutusPurpose AsIx era)
  , SpecRep (PlutusPurpose AsIx era) ~ Agda.RdmrPtr
  , Script era ~ AlonzoScript era
  , NativeScript era ~ Timelock era
  ) =>
  SpecTranslate ctx (AlonzoTxWits era)
  where
  type SpecRep (AlonzoTxWits era) = Agda.TxWitnesses

  toSpecRep :: AlonzoTxWits era -> SpecTransM ctx (SpecRep (AlonzoTxWits era))
toSpecRep AlonzoTxWits era
x =
    HSMap HSVKey Integer
-> HSSet (Either HSTimelock HSPlutusScript)
-> HSMap Integer Integer
-> HSMap RdmrPtr (Integer, ExUnits)
-> TxWitnesses
Agda.MkTxWitnesses
      forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall k v. [(k, v)] -> HSMap k v
Agda.MkHSMap (forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep [WitVKey 'Witness]
txWitsMap)
      forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. [a] -> HSSet a
Agda.MkHSSet (forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep (forall k a. Map k a -> [a]
Map.elems forall a b. (a -> b) -> a -> b
$ forall era.
AlonzoEraScript era =>
AlonzoTxWits era -> Map ScriptHash (Script era)
txscripts AlonzoTxWits era
x))
      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 (forall era. AlonzoEraScript era => AlonzoTxWits era -> TxDats era
txdats AlonzoTxWits era
x)
      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 (forall era.
AlonzoEraScript era =>
AlonzoTxWits era -> Redeemers era
txrdmrs AlonzoTxWits era
x)
    where
      txWitsMap :: [WitVKey 'Witness]
txWitsMap = forall (t :: * -> *) a. Foldable t => t a -> [a]
toList (forall era.
AlonzoEraScript era =>
AlonzoTxWits era -> Set (WitVKey 'Witness)
txwitsVKey AlonzoTxWits era
x)

instance SpecTranslate ctx a => SpecTranslate ctx (StrictMaybe a) where
  type SpecRep (StrictMaybe a) = Maybe (SpecRep a)

  toSpecRep :: StrictMaybe a -> SpecTransM ctx (SpecRep (StrictMaybe a))
toSpecRep = forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. StrictMaybe a -> Maybe a
strictMaybeToMaybe

instance SpecTranslate ctx a => SpecTranslate ctx (Maybe a) where
  type SpecRep (Maybe a) = Maybe (SpecRep a)

  toSpecRep :: Maybe a -> SpecTransM ctx (SpecRep (Maybe a))
toSpecRep = forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep

instance Era era => SpecTranslate ctx (AlonzoTxAuxData era) where
  type SpecRep (AlonzoTxAuxData era) = Agda.AuxiliaryData

  toSpecRep :: AlonzoTxAuxData era
-> SpecTransM ctx (SpecRep (AlonzoTxAuxData era))
toSpecRep = forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall x i. HashAnnotated x i => x -> SafeHash i
hashAnnotated

instance SpecTranslate ctx ScriptHash where
  type SpecRep ScriptHash = Integer

  toSpecRep :: ScriptHash -> SpecTransM ctx (SpecRep ScriptHash)
toSpecRep (ScriptHash Hash ADDRHASH EraIndependentScript
h) = forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep Hash ADDRHASH EraIndependentScript
h

instance SpecTranslate ctx (Credential k) where
  type SpecRep (Credential k) = Agda.Credential

  toSpecRep :: Credential k -> SpecTransM ctx (SpecRep (Credential k))
toSpecRep (KeyHashObj KeyHash k
h) = Integer -> Credential
Agda.KeyHashObj forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep KeyHash k
h
  toSpecRep (ScriptHashObj ScriptHash
h) = Integer -> Credential
Agda.ScriptObj forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep ScriptHash
h

instance SpecTranslate ctx Network where
  type SpecRep Network = Integer

  toSpecRep :: Network -> SpecTransM ctx (SpecRep Network)
toSpecRep = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (Integral a, Num b) => a -> b
fromIntegral forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Enum a => a -> Int
fromEnum

instance SpecTranslate ctx RewardAccount where
  type SpecRep RewardAccount = Agda.RwdAddr

  toSpecRep :: RewardAccount -> SpecTransM ctx (SpecRep RewardAccount)
toSpecRep (RewardAccount Network
n Credential 'Staking
c) = Integer -> Credential -> RwdAddr
Agda.RwdAddr forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep Network
n 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 Credential 'Staking
c

instance SpecTranslate ctx PoolParams where
  type SpecRep PoolParams = Agda.PoolParams

  toSpecRep :: PoolParams -> SpecTransM ctx (SpecRep PoolParams)
toSpecRep PoolParams {Set (KeyHash 'Staking)
VRFVerKeyHash 'StakePoolVRF
KeyHash 'StakePool
StrictMaybe PoolMetadata
Coin
RewardAccount
StrictSeq StakePoolRelay
UnitInterval
ppId :: PoolParams -> KeyHash 'StakePool
ppVrf :: PoolParams -> VRFVerKeyHash 'StakePoolVRF
ppPledge :: PoolParams -> Coin
ppCost :: PoolParams -> Coin
ppMargin :: PoolParams -> UnitInterval
ppRewardAccount :: PoolParams -> RewardAccount
ppOwners :: PoolParams -> Set (KeyHash 'Staking)
ppRelays :: PoolParams -> StrictSeq StakePoolRelay
ppMetadata :: PoolParams -> StrictMaybe PoolMetadata
ppMetadata :: StrictMaybe PoolMetadata
ppRelays :: StrictSeq StakePoolRelay
ppOwners :: Set (KeyHash 'Staking)
ppRewardAccount :: RewardAccount
ppMargin :: UnitInterval
ppCost :: Coin
ppPledge :: Coin
ppVrf :: VRFVerKeyHash 'StakePoolVRF
ppId :: KeyHash 'StakePool
..} = Credential -> PoolParams
Agda.PoolParams forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep (forall (kr :: KeyRole). KeyHash kr -> Credential kr
KeyHashObj KeyHash 'StakePool
ppId)

instance SpecTranslate ctx DRep where
  type SpecRep DRep = Agda.VDeleg

  toSpecRep :: DRep -> SpecTransM ctx (SpecRep DRep)
toSpecRep (DRepCredential Credential 'DRepRole
c) = GovRole -> Credential -> VDeleg
Agda.CredVoter GovRole
Agda.DRep forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep Credential 'DRepRole
c
  toSpecRep DRep
DRepAlwaysAbstain = forall (f :: * -> *) a. Applicative f => a -> f a
pure VDeleg
Agda.AbstainRep
  toSpecRep DRep
DRepAlwaysNoConfidence = forall (f :: * -> *) a. Applicative f => a -> f a
pure VDeleg
Agda.NoConfidenceRep

instance SpecTranslate ctx Url where
  type SpecRep Url = T.Text
  toSpecRep :: Url -> SpecTransM ctx (SpecRep Url)
toSpecRep = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall b c a. (b -> c) -> (a -> b) -> a -> c
. Url -> Text
urlToText

instance SpecTranslate ctx Anchor where
  type SpecRep Anchor = Agda.Anchor
  toSpecRep :: Anchor -> SpecTransM ctx (SpecRep Anchor)
toSpecRep (Anchor Url
url SafeHash AnchorData
h) = Text -> Integer -> Anchor
Agda.Anchor forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep Url
url 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 SafeHash AnchorData
h

instance SpecTranslate ctx TxId where
  type SpecRep TxId = Agda.TxId

  toSpecRep :: TxId -> SpecTransM ctx (SpecRep TxId)
toSpecRep (TxId SafeHash EraIndependentTxBody
x) = forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep SafeHash EraIndependentTxBody
x

instance SpecTranslate ctx Withdrawals where
  type SpecRep Withdrawals = Agda.Wdrl

  toSpecRep :: Withdrawals -> SpecTransM ctx (SpecRep Withdrawals)
toSpecRep (Withdrawals Map RewardAccount Coin
w) = forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep Map RewardAccount Coin
w

instance SpecTranslate ctx TxAuxDataHash where
  type SpecRep TxAuxDataHash = Agda.DataHash

  toSpecRep :: TxAuxDataHash -> SpecTransM ctx (SpecRep TxAuxDataHash)
toSpecRep (TxAuxDataHash SafeHash EraIndependentTxAuxData
x) = forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep SafeHash EraIndependentTxAuxData
x

data ConwayTxBodyTransContext = ConwayTxBodyTransContext
  { ConwayTxBodyTransContext -> Integer
ctbtcSizeTx :: !Integer
  , ConwayTxBodyTransContext -> TxId
ctbtcTxId :: !TxId
  }

instance Inject ConwayTxBodyTransContext Integer where
  inject :: ConwayTxBodyTransContext -> Integer
inject = ConwayTxBodyTransContext -> Integer
ctbtcSizeTx

instance Inject ConwayTxBodyTransContext TxId where
  inject :: ConwayTxBodyTransContext -> TxId
inject = ConwayTxBodyTransContext -> TxId
ctbtcTxId

instance SpecTranslate ctx IsValid where
  type SpecRep IsValid = Bool

  toSpecRep :: IsValid -> SpecTransM ctx (SpecRep IsValid)
toSpecRep (IsValid Bool
b) = forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
b

instance
  ( SpecTranslate ctx (TxWits era)
  , SpecTranslate ctx (TxAuxData era)
  , SpecTranslate ConwayTxBodyTransContext (TxBody era)
  , SpecRep (TxWits era) ~ Agda.TxWitnesses
  , SpecRep (TxAuxData era) ~ Agda.AuxiliaryData
  , SpecRep (TxBody era) ~ Agda.TxBody
  , Tx era ~ AlonzoTx era
  , EraTx era
  , BabbageEraTxBody era
  ) =>
  SpecTranslate ctx (AlonzoTx era)
  where
  type SpecRep (AlonzoTx era) = Agda.Tx

  toSpecRep :: AlonzoTx era -> SpecTransM ctx (SpecRep (AlonzoTx era))
toSpecRep AlonzoTx era
tx =
    TxBody -> TxWitnesses -> Bool -> Maybe Integer -> Tx
Agda.MkTx
      forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall ctx a ctx'. ctx -> SpecTransM ctx a -> SpecTransM ctx' a
withCtx
        (Integer -> TxId -> ConwayTxBodyTransContext
ConwayTxBodyTransContext (AlonzoTx era
tx forall s a. s -> Getting a s a -> a
^. forall era. EraTx era => SimpleGetter (Tx era) Integer
sizeTxF) (forall era. EraTx era => Tx era -> TxId
txIdTx AlonzoTx era
tx))
        (forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep (forall era. AlonzoTx era -> TxBody era
body AlonzoTx era
tx))
      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 (forall era. AlonzoTx era -> TxWits era
wits AlonzoTx era
tx)
      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 (forall era. AlonzoTx era -> IsValid
isValid AlonzoTx era
tx)
      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 (forall era. AlonzoTx era -> StrictMaybe (TxAuxData era)
auxiliaryData AlonzoTx era
tx)

instance
  ( EraPParams era
  , ToExpr (PParamsHKD StrictMaybe era)
  ) =>
  SpecTranslate ctx (ConwayGovPredFailure era)
  where
  type SpecRep (ConwayGovPredFailure era) = OpaqueErrorString

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

instance SpecTranslate ctx (GovPurposeId r c) where
  type SpecRep (GovPurposeId r c) = (Agda.TxId, Integer)

  toSpecRep :: GovPurposeId r c -> SpecTransM ctx (SpecRep (GovPurposeId r c))
toSpecRep (GovPurposeId GovActionId
gaId) = forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep GovActionId
gaId

instance SpecTranslate ctx UnitInterval where
  type SpecRep UnitInterval = Agda.Rational

  toSpecRep :: UnitInterval -> SpecTransM ctx (SpecRep UnitInterval)
toSpecRep = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall r. BoundedRational r => r -> Rational
unboundRational

instance SpecTranslate ctx (Committee era) where
  type SpecRep (Committee era) = (Agda.HSMap Agda.Credential Agda.Epoch, Agda.Rational)

  toSpecRep :: Committee era -> SpecTransM ctx (SpecRep (Committee era))
toSpecRep (Committee Map (Credential 'ColdCommitteeRole) EpochNo
members UnitInterval
threshold) = forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep (Map (Credential 'ColdCommitteeRole) EpochNo
members, UnitInterval
threshold)

instance SpecTranslate ctx (Constitution era) where
  type SpecRep (Constitution era) = (Agda.DataHash, Maybe Agda.ScriptHash)

  toSpecRep :: Constitution era -> SpecTransM ctx (SpecRep (Constitution era))
toSpecRep (Constitution (Anchor Url
_ SafeHash AnchorData
h) StrictMaybe ScriptHash
policy) = forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep (SafeHash AnchorData
h, StrictMaybe ScriptHash
policy)

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

  toSpecRep :: EnactState era -> SpecTransM ctx (SpecRep (EnactState era))
toSpecRep EnactState {Map (Credential 'Staking) Coin
PParams era
StrictMaybe (Committee era)
Coin
Constitution era
GovRelation StrictMaybe era
ensPrevGovActionIds :: forall era. EnactState era -> GovRelation StrictMaybe era
ensWithdrawals :: forall era. EnactState era -> Map (Credential 'Staking) Coin
ensTreasury :: forall era. EnactState era -> Coin
ensPrevPParams :: forall era. EnactState era -> PParams era
ensCurPParams :: forall era. EnactState era -> PParams era
ensConstitution :: forall era. EnactState era -> Constitution era
ensCommittee :: forall era. EnactState era -> StrictMaybe (Committee era)
ensPrevGovActionIds :: GovRelation StrictMaybe era
ensWithdrawals :: Map (Credential 'Staking) Coin
ensTreasury :: Coin
ensPrevPParams :: PParams era
ensCurPParams :: PParams era
ensConstitution :: Constitution era
ensCommittee :: StrictMaybe (Committee era)
..} =
    (Maybe (HSMap Credential Integer, Rational), ExUnits)
-> ((Integer, Maybe Integer), ExUnits)
-> (ExUnits, ExUnits)
-> (PParams, ExUnits)
-> HSMap RwdAddr Integer
-> EnactState
Agda.MkEnactState
      forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall {a} {a} {b} {ctx} {a}.
(SpecRep a ~ (a, b), SpecTranslate ctx a, SpecTranslate ctx a,
 Num a, Num b) =>
a -> StrictMaybe a -> SpecTransM ctx (SpecRep a, (a, b))
transHashProtected StrictMaybe (Committee era)
ensCommittee StrictMaybe (GovPurposeId 'CommitteePurpose era)
grCommittee
      forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall {a} {a} {b} {ctx} {a}.
(SpecRep a ~ (a, b), SpecTranslate ctx a, SpecTranslate ctx a,
 Num a, Num b) =>
a -> StrictMaybe a -> SpecTransM ctx (SpecRep a, (a, b))
transHashProtected Constitution era
ensConstitution StrictMaybe (GovPurposeId 'ConstitutionPurpose era)
grConstitution
      forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall {a} {a} {b} {ctx} {a}.
(SpecRep a ~ (a, b), SpecTranslate ctx a, SpecTranslate ctx a,
 Num a, Num b) =>
a -> StrictMaybe a -> SpecTransM ctx (SpecRep a, (a, b))
transHashProtected (PParams era
ensCurPParams forall s a. s -> Getting a s a -> a
^. forall era. EraPParams era => Lens' (PParams era) ProtVer
ppProtocolVersionL) StrictMaybe (GovPurposeId 'HardForkPurpose era)
grHardFork
      forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall {a} {a} {b} {ctx} {a}.
(SpecRep a ~ (a, b), SpecTranslate ctx a, SpecTranslate ctx a,
 Num a, Num b) =>
a -> StrictMaybe a -> SpecTransM ctx (SpecRep a, (a, b))
transHashProtected PParams era
ensCurPParams StrictMaybe (GovPurposeId 'PParamUpdatePurpose era)
grPParamUpdate
      forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall {a} {ctx}.
(SpecRep a ~ Credential, SpecTranslate ctx a) =>
Map a Coin -> SpecTransM ctx (HSMap RwdAddr Integer)
transWithdrawals Map (Credential 'Staking) Coin
ensWithdrawals
    where
      GovRelation {StrictMaybe (GovPurposeId 'PParamUpdatePurpose era)
StrictMaybe (GovPurposeId 'HardForkPurpose era)
StrictMaybe (GovPurposeId 'CommitteePurpose era)
StrictMaybe (GovPurposeId 'ConstitutionPurpose era)
grConstitution :: forall (f :: * -> *) era.
GovRelation f era -> f (GovPurposeId 'ConstitutionPurpose era)
grCommittee :: forall (f :: * -> *) era.
GovRelation f era -> f (GovPurposeId 'CommitteePurpose era)
grHardFork :: forall (f :: * -> *) era.
GovRelation f era -> f (GovPurposeId 'HardForkPurpose era)
grPParamUpdate :: forall (f :: * -> *) era.
GovRelation f era -> f (GovPurposeId 'PParamUpdatePurpose era)
grPParamUpdate :: StrictMaybe (GovPurposeId 'PParamUpdatePurpose era)
grHardFork :: StrictMaybe (GovPurposeId 'HardForkPurpose era)
grConstitution :: StrictMaybe (GovPurposeId 'ConstitutionPurpose era)
grCommittee :: StrictMaybe (GovPurposeId 'CommitteePurpose era)
..} = GovRelation StrictMaybe era
ensPrevGovActionIds
      transWithdrawals :: Map a Coin -> SpecTransM ctx (HSMap RwdAddr Integer)
transWithdrawals Map a Coin
ws = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall k v. [(k, v)] -> HSMap k v
Agda.MkHSMap forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM (forall k a. Map k a -> [(k, a)]
Map.toList Map a Coin
ws) forall a b. (a -> b) -> a -> b
$
        \(a
cred, Coin Integer
amount) -> do
          Credential
agdaCred <- forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep a
cred
          Integer
network <- forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep Network
Testnet -- TODO where should this really come from?
          forall (f :: * -> *) a. Applicative f => a -> f a
pure (Integer -> Credential -> RwdAddr
Agda.RwdAddr Integer
network Credential
agdaCred, Integer
amount)
      transHashProtected :: a -> StrictMaybe a -> SpecTransM ctx (SpecRep a, (a, b))
transHashProtected a
x StrictMaybe a
h = do
        SpecRep a
committee <- forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep a
x
        (a, b)
agdaLastId <- case StrictMaybe a
h of
          SJust a
lastId -> forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep a
lastId
          StrictMaybe a
SNothing -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (a
0, b
0)
        forall (f :: * -> *) a. Applicative f => a -> f a
pure (SpecRep a
committee, (a, b)
agdaLastId)

instance SpecTranslate ctx Voter where
  type SpecRep Voter = Agda.Voter

  toSpecRep :: Voter -> SpecTransM ctx (SpecRep Voter)
toSpecRep (CommitteeVoter Credential 'HotCommitteeRole
c) = (GovRole
Agda.CC,) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep Credential 'HotCommitteeRole
c
  toSpecRep (DRepVoter Credential 'DRepRole
c) = (GovRole
Agda.DRep,) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep Credential 'DRepRole
c
  toSpecRep (StakePoolVoter KeyHash 'StakePool
kh) = (GovRole
Agda.SPO,) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep (forall (kr :: KeyRole). KeyHash kr -> Credential kr
KeyHashObj KeyHash 'StakePool
kh)

instance SpecTranslate ctx Vote where
  type SpecRep Vote = Agda.Vote

  toSpecRep :: Vote -> SpecTransM ctx (SpecRep Vote)
toSpecRep Vote
VoteYes = forall (f :: * -> *) a. Applicative f => a -> f a
pure Vote
Agda.Yes
  toSpecRep Vote
VoteNo = forall (f :: * -> *) a. Applicative f => a -> f a
pure Vote
Agda.No
  toSpecRep Vote
Abstain = forall (f :: * -> *) a. Applicative f => a -> f a
pure Vote
Agda.Abstain

instance SpecTranslate ctx (VotingProcedures era) where
  type SpecRep (VotingProcedures era) = [Agda.GovVote]

  toSpecRep :: VotingProcedures era
-> SpecTransM ctx (SpecRep (VotingProcedures era))
toSpecRep = forall era c.
(Voter -> GovActionId -> VotingProcedure era -> c -> c)
-> c -> VotingProcedures era -> c
foldrVotingProcedures Voter
-> GovActionId
-> VotingProcedure era
-> SpecTransM ctx [GovVote]
-> SpecTransM ctx [GovVote]
go (forall (f :: * -> *) a. Applicative f => a -> f a
pure [])
    where
      go ::
        Voter ->
        GovActionId ->
        VotingProcedure era ->
        SpecTransM ctx [Agda.GovVote] ->
        SpecTransM ctx [Agda.GovVote]
      go :: Voter
-> GovActionId
-> VotingProcedure era
-> SpecTransM ctx [GovVote]
-> SpecTransM ctx [GovVote]
go Voter
voter GovActionId
gaId VotingProcedure era
votingProcedure SpecTransM ctx [GovVote]
m =
        (:)
          forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ( ExUnits -> (GovRole, Credential) -> Vote -> Maybe Anchor -> GovVote
Agda.GovVote
                  forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep GovActionId
gaId
                  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 Voter
voter
                  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 (forall era. VotingProcedure era -> Vote
vProcVote VotingProcedure era
votingProcedure)
                  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 (forall era. VotingProcedure era -> StrictMaybe Anchor
vProcAnchor VotingProcedure era
votingProcedure)
              )
          forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> SpecTransM ctx [GovVote]
m

instance SpecTranslate ctx Word16 where
  type SpecRep Word16 = Integer

  toSpecRep :: Word16 -> SpecTransM ctx (SpecRep Word16)
toSpecRep = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Integral a => a -> Integer
toInteger

instance SpecTranslate ctx NonNegativeInterval where
  type SpecRep NonNegativeInterval = Agda.Rational

  toSpecRep :: NonNegativeInterval -> SpecTransM ctx (SpecRep NonNegativeInterval)
toSpecRep = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall r. BoundedRational r => r -> Rational
unboundRational

instance SpecTranslate ctx (ConwayPParams StrictMaybe era) where
  type SpecRep (ConwayPParams StrictMaybe era) = Agda.PParamsUpdate

  toSpecRep :: ConwayPParams StrictMaybe era
-> SpecTransM ctx (SpecRep (ConwayPParams StrictMaybe era))
toSpecRep (ConwayPParams {THKD ('PPGroups 'GovGroup 'NoStakePoolGroup) StrictMaybe Word16
THKD ('PPGroups 'GovGroup 'NoStakePoolGroup) StrictMaybe Coin
THKD
  ('PPGroups 'GovGroup 'NoStakePoolGroup)
  StrictMaybe
  PoolVotingThresholds
THKD
  ('PPGroups 'GovGroup 'NoStakePoolGroup)
  StrictMaybe
  DRepVotingThresholds
THKD
  ('PPGroups 'GovGroup 'NoStakePoolGroup) StrictMaybe EpochInterval
THKD ('PPGroups 'GovGroup 'SecurityGroup) StrictMaybe Coin
THKD
  ('PPGroups 'TechnicalGroup 'NoStakePoolGroup) StrictMaybe Word16
THKD
  ('PPGroups 'TechnicalGroup 'NoStakePoolGroup)
  StrictMaybe
  CostModels
THKD
  ('PPGroups 'TechnicalGroup 'NoStakePoolGroup)
  StrictMaybe
  NonNegativeInterval
THKD
  ('PPGroups 'TechnicalGroup 'NoStakePoolGroup)
  StrictMaybe
  EpochInterval
THKD
  ('PPGroups 'EconomicGroup 'NoStakePoolGroup) StrictMaybe Prices
THKD ('PPGroups 'EconomicGroup 'NoStakePoolGroup) StrictMaybe Coin
THKD
  ('PPGroups 'EconomicGroup 'NoStakePoolGroup)
  StrictMaybe
  UnitInterval
THKD ('PPGroups 'EconomicGroup 'SecurityGroup) StrictMaybe Coin
THKD
  ('PPGroups 'EconomicGroup 'SecurityGroup) StrictMaybe CoinPerByte
THKD
  ('PPGroups 'EconomicGroup 'SecurityGroup)
  StrictMaybe
  NonNegativeInterval
THKD ('PPGroups 'NetworkGroup 'NoStakePoolGroup) StrictMaybe Word16
THKD
  ('PPGroups 'NetworkGroup 'NoStakePoolGroup) StrictMaybe OrdExUnits
THKD ('PPGroups 'NetworkGroup 'SecurityGroup) StrictMaybe Word16
THKD ('PPGroups 'NetworkGroup 'SecurityGroup) StrictMaybe Word32
THKD
  ('PPGroups 'NetworkGroup 'SecurityGroup) StrictMaybe OrdExUnits
HKDNoUpdate StrictMaybe ProtVer
cppMinFeeRefScriptCostPerByte :: THKD
  ('PPGroups 'EconomicGroup 'SecurityGroup)
  StrictMaybe
  NonNegativeInterval
cppDRepActivity :: THKD
  ('PPGroups 'GovGroup 'NoStakePoolGroup) StrictMaybe EpochInterval
cppDRepDeposit :: THKD ('PPGroups 'GovGroup 'NoStakePoolGroup) StrictMaybe Coin
cppGovActionDeposit :: THKD ('PPGroups 'GovGroup 'SecurityGroup) StrictMaybe Coin
cppGovActionLifetime :: THKD
  ('PPGroups 'GovGroup 'NoStakePoolGroup) StrictMaybe EpochInterval
cppCommitteeMaxTermLength :: THKD
  ('PPGroups 'GovGroup 'NoStakePoolGroup) StrictMaybe EpochInterval
cppCommitteeMinSize :: THKD ('PPGroups 'GovGroup 'NoStakePoolGroup) StrictMaybe Word16
cppDRepVotingThresholds :: THKD
  ('PPGroups 'GovGroup 'NoStakePoolGroup)
  StrictMaybe
  DRepVotingThresholds
cppPoolVotingThresholds :: THKD
  ('PPGroups 'GovGroup 'NoStakePoolGroup)
  StrictMaybe
  PoolVotingThresholds
cppMaxCollateralInputs :: THKD ('PPGroups 'NetworkGroup 'NoStakePoolGroup) StrictMaybe Word16
cppCollateralPercentage :: THKD
  ('PPGroups 'TechnicalGroup 'NoStakePoolGroup) StrictMaybe Word16
cppMaxValSize :: THKD ('PPGroups 'NetworkGroup 'SecurityGroup) StrictMaybe Word32
cppMaxBlockExUnits :: THKD
  ('PPGroups 'NetworkGroup 'SecurityGroup) StrictMaybe OrdExUnits
cppMaxTxExUnits :: THKD
  ('PPGroups 'NetworkGroup 'NoStakePoolGroup) StrictMaybe OrdExUnits
cppPrices :: THKD
  ('PPGroups 'EconomicGroup 'NoStakePoolGroup) StrictMaybe Prices
cppCostModels :: THKD
  ('PPGroups 'TechnicalGroup 'NoStakePoolGroup)
  StrictMaybe
  CostModels
cppCoinsPerUTxOByte :: THKD
  ('PPGroups 'EconomicGroup 'SecurityGroup) StrictMaybe CoinPerByte
cppMinPoolCost :: THKD ('PPGroups 'EconomicGroup 'NoStakePoolGroup) StrictMaybe Coin
cppProtocolVersion :: HKDNoUpdate StrictMaybe ProtVer
cppTau :: THKD
  ('PPGroups 'EconomicGroup 'NoStakePoolGroup)
  StrictMaybe
  UnitInterval
cppRho :: THKD
  ('PPGroups 'EconomicGroup 'NoStakePoolGroup)
  StrictMaybe
  UnitInterval
cppA0 :: THKD
  ('PPGroups 'TechnicalGroup 'NoStakePoolGroup)
  StrictMaybe
  NonNegativeInterval
cppNOpt :: THKD
  ('PPGroups 'TechnicalGroup 'NoStakePoolGroup) StrictMaybe Word16
cppEMax :: THKD
  ('PPGroups 'TechnicalGroup 'NoStakePoolGroup)
  StrictMaybe
  EpochInterval
cppPoolDeposit :: THKD ('PPGroups 'EconomicGroup 'NoStakePoolGroup) StrictMaybe Coin
cppKeyDeposit :: THKD ('PPGroups 'EconomicGroup 'NoStakePoolGroup) StrictMaybe Coin
cppMaxBHSize :: THKD ('PPGroups 'NetworkGroup 'SecurityGroup) StrictMaybe Word16
cppMaxTxSize :: THKD ('PPGroups 'NetworkGroup 'SecurityGroup) StrictMaybe Word32
cppMaxBBSize :: THKD ('PPGroups 'NetworkGroup 'SecurityGroup) StrictMaybe Word32
cppMinFeeB :: THKD ('PPGroups 'EconomicGroup 'SecurityGroup) StrictMaybe Coin
cppMinFeeA :: THKD ('PPGroups 'EconomicGroup 'SecurityGroup) StrictMaybe Coin
cppMinFeeA :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD ('PPGroups 'EconomicGroup 'SecurityGroup) f Coin
cppMinFeeB :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD ('PPGroups 'EconomicGroup 'SecurityGroup) f Coin
cppMaxBBSize :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD ('PPGroups 'NetworkGroup 'SecurityGroup) f Word32
cppMaxTxSize :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD ('PPGroups 'NetworkGroup 'SecurityGroup) f Word32
cppMaxBHSize :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD ('PPGroups 'NetworkGroup 'SecurityGroup) f Word16
cppKeyDeposit :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD ('PPGroups 'EconomicGroup 'NoStakePoolGroup) f Coin
cppPoolDeposit :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD ('PPGroups 'EconomicGroup 'NoStakePoolGroup) f Coin
cppEMax :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD
     ('PPGroups 'TechnicalGroup 'NoStakePoolGroup) f EpochInterval
cppNOpt :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD ('PPGroups 'TechnicalGroup 'NoStakePoolGroup) f Word16
cppA0 :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD
     ('PPGroups 'TechnicalGroup 'NoStakePoolGroup) f NonNegativeInterval
cppRho :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD ('PPGroups 'EconomicGroup 'NoStakePoolGroup) f UnitInterval
cppTau :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD ('PPGroups 'EconomicGroup 'NoStakePoolGroup) f UnitInterval
cppProtocolVersion :: forall (f :: * -> *) era.
ConwayPParams f era -> HKDNoUpdate f ProtVer
cppMinPoolCost :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD ('PPGroups 'EconomicGroup 'NoStakePoolGroup) f Coin
cppCoinsPerUTxOByte :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD ('PPGroups 'EconomicGroup 'SecurityGroup) f CoinPerByte
cppCostModels :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD ('PPGroups 'TechnicalGroup 'NoStakePoolGroup) f CostModels
cppPrices :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD ('PPGroups 'EconomicGroup 'NoStakePoolGroup) f Prices
cppMaxTxExUnits :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD ('PPGroups 'NetworkGroup 'NoStakePoolGroup) f OrdExUnits
cppMaxBlockExUnits :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD ('PPGroups 'NetworkGroup 'SecurityGroup) f OrdExUnits
cppMaxValSize :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD ('PPGroups 'NetworkGroup 'SecurityGroup) f Word32
cppCollateralPercentage :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD ('PPGroups 'TechnicalGroup 'NoStakePoolGroup) f Word16
cppMaxCollateralInputs :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD ('PPGroups 'NetworkGroup 'NoStakePoolGroup) f Word16
cppPoolVotingThresholds :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD
     ('PPGroups 'GovGroup 'NoStakePoolGroup) f PoolVotingThresholds
cppDRepVotingThresholds :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD
     ('PPGroups 'GovGroup 'NoStakePoolGroup) f DRepVotingThresholds
cppCommitteeMinSize :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD ('PPGroups 'GovGroup 'NoStakePoolGroup) f Word16
cppCommitteeMaxTermLength :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD ('PPGroups 'GovGroup 'NoStakePoolGroup) f EpochInterval
cppGovActionLifetime :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD ('PPGroups 'GovGroup 'NoStakePoolGroup) f EpochInterval
cppGovActionDeposit :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD ('PPGroups 'GovGroup 'SecurityGroup) f Coin
cppDRepDeposit :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD ('PPGroups 'GovGroup 'NoStakePoolGroup) f Coin
cppDRepActivity :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD ('PPGroups 'GovGroup 'NoStakePoolGroup) f EpochInterval
cppMinFeeRefScriptCostPerByte :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD
     ('PPGroups 'EconomicGroup 'SecurityGroup) f NonNegativeInterval
..}) = do
    Maybe Integer
ppuA <- forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep THKD ('PPGroups 'EconomicGroup 'SecurityGroup) StrictMaybe Coin
cppMinFeeA
    Maybe Integer
ppuB <- forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep THKD ('PPGroups 'EconomicGroup 'SecurityGroup) StrictMaybe Coin
cppMinFeeB
    Maybe Rational
ppuA0 <- forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep THKD
  ('PPGroups 'TechnicalGroup 'NoStakePoolGroup)
  StrictMaybe
  NonNegativeInterval
cppA0
    Maybe Rational
ppuMinFeeRefScriptCoinsPerByte <- forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep THKD
  ('PPGroups 'EconomicGroup 'SecurityGroup)
  StrictMaybe
  NonNegativeInterval
cppMinFeeRefScriptCostPerByte
    Maybe Integer
ppuCollateralPercentage <- forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep THKD
  ('PPGroups 'TechnicalGroup 'NoStakePoolGroup) StrictMaybe Word16
cppCollateralPercentage
    let
      ppuMaxBlockSize :: Maybe Integer
ppuMaxBlockSize = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. Integral a => a -> Integer
toInteger forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. StrictMaybe a -> Maybe a
strictMaybeToMaybe forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: PPGroups) (f :: * -> *) a. THKD t f a -> HKD f a
unTHKD forall a b. (a -> b) -> a -> b
$ THKD ('PPGroups 'NetworkGroup 'SecurityGroup) StrictMaybe Word32
cppMaxBBSize
      ppuMaxTxSize :: Maybe Integer
ppuMaxTxSize = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. Integral a => a -> Integer
toInteger forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. StrictMaybe a -> Maybe a
strictMaybeToMaybe forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: PPGroups) (f :: * -> *) a. THKD t f a -> HKD f a
unTHKD forall a b. (a -> b) -> a -> b
$ THKD ('PPGroups 'NetworkGroup 'SecurityGroup) StrictMaybe Word32
cppMaxTxSize
      ppuMaxHeaderSize :: Maybe Integer
ppuMaxHeaderSize = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. Integral a => a -> Integer
toInteger forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. StrictMaybe a -> Maybe a
strictMaybeToMaybe forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: PPGroups) (f :: * -> *) a. THKD t f a -> HKD f a
unTHKD forall a b. (a -> b) -> a -> b
$ THKD ('PPGroups 'NetworkGroup 'SecurityGroup) StrictMaybe Word16
cppMaxBHSize
    Maybe Integer
ppuKeyDeposit <- forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep THKD ('PPGroups 'EconomicGroup 'NoStakePoolGroup) StrictMaybe Coin
cppKeyDeposit
    Maybe Integer
ppuPoolDeposit <- forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep THKD ('PPGroups 'EconomicGroup 'NoStakePoolGroup) StrictMaybe Coin
cppPoolDeposit
    Maybe Integer
ppuEmax <- forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep THKD
  ('PPGroups 'TechnicalGroup 'NoStakePoolGroup)
  StrictMaybe
  EpochInterval
cppEMax
    Maybe Integer
ppuNopt <- forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. Integral a => a -> Integer
toInteger forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. StrictMaybe a -> Maybe a
strictMaybeToMaybe forall a b. (a -> b) -> a -> b
$ forall (t :: PPGroups) (f :: * -> *) a. THKD t f a -> HKD f a
unTHKD THKD
  ('PPGroups 'TechnicalGroup 'NoStakePoolGroup) StrictMaybe Word16
cppNOpt)
    let
      ppuPv :: Maybe a
ppuPv = forall a. Maybe a
Nothing
      ppuMinUTxOValue :: Maybe a
ppuMinUTxOValue = forall a. Maybe a
Nothing -- minUTxOValue has been deprecated and is not supported in Conway
    Maybe Integer
ppuCoinsPerUTxOByte <- forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep THKD
  ('PPGroups 'EconomicGroup 'SecurityGroup) StrictMaybe CoinPerByte
cppCoinsPerUTxOByte
    Maybe ()
ppuCostmdls <- forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep THKD
  ('PPGroups 'TechnicalGroup 'NoStakePoolGroup)
  StrictMaybe
  CostModels
cppCostModels
    Maybe ()
ppuPrices <- forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep THKD
  ('PPGroups 'EconomicGroup 'NoStakePoolGroup) StrictMaybe Prices
cppPrices
    let
      ppuMaxRefScriptSizePerTx :: Maybe a
ppuMaxRefScriptSizePerTx = forall a. Maybe a
Nothing
      ppuMaxRefScriptSizePerBlock :: Maybe a
ppuMaxRefScriptSizePerBlock = forall a. Maybe a
Nothing
      ppuRefScriptCostStride :: Maybe a
ppuRefScriptCostStride = forall a. Maybe a
Nothing
      ppuRefScriptCostMultiplier :: Maybe a
ppuRefScriptCostMultiplier = forall a. Maybe a
Nothing
    Maybe ExUnits
ppuMaxTxExUnits <- forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep THKD
  ('PPGroups 'NetworkGroup 'NoStakePoolGroup) StrictMaybe OrdExUnits
cppMaxTxExUnits
    Maybe ExUnits
ppuMaxBlockExUnits <- forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep THKD
  ('PPGroups 'NetworkGroup 'SecurityGroup) StrictMaybe OrdExUnits
cppMaxBlockExUnits
    let
      ppuMaxValSize :: Maybe Integer
ppuMaxValSize = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. Integral a => a -> Integer
toInteger forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. StrictMaybe a -> Maybe a
strictMaybeToMaybe forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: PPGroups) (f :: * -> *) a. THKD t f a -> HKD f a
unTHKD forall a b. (a -> b) -> a -> b
$ THKD ('PPGroups 'NetworkGroup 'SecurityGroup) StrictMaybe Word32
cppMaxValSize
      ppuMaxCollateralInputs :: Maybe Integer
ppuMaxCollateralInputs = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. Integral a => a -> Integer
toInteger forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. StrictMaybe a -> Maybe a
strictMaybeToMaybe forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: PPGroups) (f :: * -> *) a. THKD t f a -> HKD f a
unTHKD forall a b. (a -> b) -> a -> b
$ THKD ('PPGroups 'NetworkGroup 'NoStakePoolGroup) StrictMaybe Word16
cppMaxCollateralInputs
    Maybe PoolThresholds
ppuPoolThresholds <- forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep THKD
  ('PPGroups 'GovGroup 'NoStakePoolGroup)
  StrictMaybe
  PoolVotingThresholds
cppPoolVotingThresholds
    Maybe DrepThresholds
ppuDrepThresholds <- forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep THKD
  ('PPGroups 'GovGroup 'NoStakePoolGroup)
  StrictMaybe
  DRepVotingThresholds
cppDRepVotingThresholds
    let
      ppuCcMinSize :: Maybe Integer
ppuCcMinSize = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. Integral a => a -> Integer
toInteger forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. StrictMaybe a -> Maybe a
strictMaybeToMaybe forall a b. (a -> b) -> a -> b
$ forall (t :: PPGroups) (f :: * -> *) a. THKD t f a -> HKD f a
unTHKD THKD ('PPGroups 'GovGroup 'NoStakePoolGroup) StrictMaybe Word16
cppCommitteeMinSize
      ppuCcMaxTermLength :: Maybe Integer
ppuCcMaxTermLength =
        forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall a. Integral a => a -> Integer
toInteger forall b c a. (b -> c) -> (a -> b) -> a -> c
. EpochInterval -> Word32
unEpochInterval) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. StrictMaybe a -> Maybe a
strictMaybeToMaybe forall a b. (a -> b) -> a -> b
$ forall (t :: PPGroups) (f :: * -> *) a. THKD t f a -> HKD f a
unTHKD THKD
  ('PPGroups 'GovGroup 'NoStakePoolGroup) StrictMaybe EpochInterval
cppCommitteeMaxTermLength
    Maybe Integer
ppuGovActionLifetime <- forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep THKD
  ('PPGroups 'GovGroup 'NoStakePoolGroup) StrictMaybe EpochInterval
cppGovActionLifetime
    Maybe Integer
ppuGovActionDeposit <- forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep THKD ('PPGroups 'GovGroup 'SecurityGroup) StrictMaybe Coin
cppGovActionDeposit
    Maybe Integer
ppuDrepDeposit <- forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep THKD ('PPGroups 'GovGroup 'NoStakePoolGroup) StrictMaybe Coin
cppDRepDeposit
    Maybe Integer
ppuDrepActivity <- forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep THKD
  ('PPGroups 'GovGroup 'NoStakePoolGroup) StrictMaybe EpochInterval
cppDRepActivity
    Maybe Rational
ppuMonetaryExpansion <- forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep THKD
  ('PPGroups 'EconomicGroup 'NoStakePoolGroup)
  StrictMaybe
  UnitInterval
cppRho
    Maybe Rational
ppuTreasuryCut <- forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep THKD
  ('PPGroups 'EconomicGroup 'NoStakePoolGroup)
  StrictMaybe
  UnitInterval
cppTau

    forall (f :: * -> *) a. Applicative f => a -> f a
pure Agda.MkPParamsUpdate {Maybe Integer
Maybe Rational
Maybe ()
Maybe ExUnits
Maybe DrepThresholds
Maybe PoolThresholds
forall a. Maybe a
ppuMaxBlockSize :: Maybe Integer
ppuMaxTxSize :: Maybe Integer
ppuMaxHeaderSize :: Maybe Integer
ppuMaxValSize :: Maybe Integer
ppuMaxCollateralInputs :: Maybe Integer
ppuMaxTxExUnits :: Maybe ExUnits
ppuMaxBlockExUnits :: Maybe ExUnits
ppuPv :: Maybe ExUnits
ppuA :: Maybe Integer
ppuB :: Maybe Integer
ppuKeyDeposit :: Maybe Integer
ppuPoolDeposit :: Maybe Integer
ppuMonetaryExpansion :: Maybe Rational
ppuTreasuryCut :: Maybe Rational
ppuCoinsPerUTxOByte :: Maybe Integer
ppuPrices :: Maybe ()
ppuMinFeeRefScriptCoinsPerByte :: Maybe Rational
ppuMaxRefScriptSizePerTx :: Maybe Integer
ppuMaxRefScriptSizePerBlock :: Maybe Integer
ppuRefScriptCostStride :: Maybe Integer
ppuRefScriptCostMultiplier :: Maybe Rational
ppuMinUTxOValue :: Maybe Integer
ppuA0 :: Maybe Rational
ppuEmax :: Maybe Integer
ppuNopt :: Maybe Integer
ppuCollateralPercentage :: Maybe Integer
ppuCostmdls :: Maybe ()
ppuDrepThresholds :: Maybe DrepThresholds
ppuPoolThresholds :: Maybe PoolThresholds
ppuGovActionLifetime :: Maybe Integer
ppuGovActionDeposit :: Maybe Integer
ppuDrepDeposit :: Maybe Integer
ppuDrepActivity :: Maybe Integer
ppuCcMinSize :: Maybe Integer
ppuCcMaxTermLength :: Maybe Integer
ppuTreasuryCut :: Maybe Rational
ppuMonetaryExpansion :: Maybe Rational
ppuDrepActivity :: Maybe Integer
ppuDrepDeposit :: Maybe Integer
ppuGovActionDeposit :: Maybe Integer
ppuGovActionLifetime :: Maybe Integer
ppuCcMaxTermLength :: Maybe Integer
ppuCcMinSize :: Maybe Integer
ppuDrepThresholds :: Maybe DrepThresholds
ppuPoolThresholds :: Maybe PoolThresholds
ppuMaxCollateralInputs :: Maybe Integer
ppuMaxValSize :: Maybe Integer
ppuMaxBlockExUnits :: Maybe ExUnits
ppuMaxTxExUnits :: Maybe ExUnits
ppuRefScriptCostMultiplier :: forall a. Maybe a
ppuRefScriptCostStride :: forall a. Maybe a
ppuMaxRefScriptSizePerBlock :: forall a. Maybe a
ppuMaxRefScriptSizePerTx :: forall a. Maybe a
ppuPrices :: Maybe ()
ppuCostmdls :: Maybe ()
ppuCoinsPerUTxOByte :: Maybe Integer
ppuMinUTxOValue :: forall a. Maybe a
ppuPv :: forall a. Maybe a
ppuNopt :: Maybe Integer
ppuEmax :: Maybe Integer
ppuPoolDeposit :: Maybe Integer
ppuKeyDeposit :: Maybe Integer
ppuMaxHeaderSize :: Maybe Integer
ppuMaxTxSize :: Maybe Integer
ppuMaxBlockSize :: Maybe Integer
ppuCollateralPercentage :: Maybe Integer
ppuMinFeeRefScriptCoinsPerByte :: Maybe Rational
ppuA0 :: Maybe Rational
ppuB :: Maybe Integer
ppuA :: Maybe Integer
..}

instance
  SpecTranslate ctx (PParamsHKD StrictMaybe era) =>
  SpecTranslate ctx (PParamsUpdate era)
  where
  type SpecRep (PParamsUpdate era) = SpecRep (PParamsHKD StrictMaybe era)

  toSpecRep :: PParamsUpdate era -> SpecTransM ctx (SpecRep (PParamsUpdate era))
toSpecRep (PParamsUpdate PParamsHKD StrictMaybe era
ppu) = forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep PParamsHKD StrictMaybe era
ppu

instance
  ( EraPParams era
  , SpecTranslate ctx (PParamsHKD StrictMaybe era)
  , SpecRep (PParamsHKD StrictMaybe era) ~ Agda.PParamsUpdate
  ) =>
  SpecTranslate ctx (GovAction era)
  where
  type SpecRep (GovAction era) = Agda.GovAction

  toSpecRep :: GovAction era -> SpecTransM ctx (SpecRep (GovAction era))
toSpecRep (ParameterChange StrictMaybe (GovPurposeId 'PParamUpdatePurpose era)
_ PParamsUpdate era
ppu StrictMaybe ScriptHash
_) = PParamsUpdate -> GovAction
Agda.ChangePParams forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep PParamsUpdate era
ppu
  toSpecRep (HardForkInitiation StrictMaybe (GovPurposeId 'HardForkPurpose era)
_ ProtVer
pv) = ExUnits -> GovAction
Agda.TriggerHF forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep ProtVer
pv
  toSpecRep (TreasuryWithdrawals Map RewardAccount Coin
withdrawals StrictMaybe ScriptHash
_) =
    HSMap RwdAddr Integer -> GovAction
Agda.TreasuryWdrl
      forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep Map RewardAccount Coin
withdrawals
  toSpecRep (NoConfidence StrictMaybe (GovPurposeId 'CommitteePurpose era)
_) = forall (f :: * -> *) a. Applicative f => a -> f a
pure GovAction
Agda.NoConfidence
  toSpecRep (UpdateCommittee StrictMaybe (GovPurposeId 'CommitteePurpose era)
_ Set (Credential 'ColdCommitteeRole)
remove Map (Credential 'ColdCommitteeRole) EpochNo
add UnitInterval
threshold) =
    HSMap Credential Integer
-> HSSet Credential -> Rational -> GovAction
Agda.UpdateCommittee
      forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep Map (Credential 'ColdCommitteeRole) EpochNo
add
      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 Set (Credential 'ColdCommitteeRole)
remove
      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 UnitInterval
threshold
  toSpecRep (NewConstitution StrictMaybe (GovPurposeId 'ConstitutionPurpose era)
_ (Constitution (Anchor Url
_ SafeHash AnchorData
h) StrictMaybe ScriptHash
policy)) =
    Integer -> Maybe Integer -> GovAction
Agda.NewConstitution
      forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep SafeHash AnchorData
h
      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 StrictMaybe ScriptHash
policy
  toSpecRep GovAction era
InfoAction = forall (f :: * -> *) a. Applicative f => a -> f a
pure GovAction
Agda.Info

instance SpecTranslate ctx a => SpecTranslate ctx (OSet a) where
  type SpecRep (OSet a) = [SpecRep a]

  toSpecRep :: OSet a -> SpecTransM ctx (SpecRep (OSet a))
toSpecRep = forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) a. Foldable t => t a -> [a]
toList

instance
  ( SpecTranslate ctx k
  , SpecTranslate ctx v
  , Ord k
  ) =>
  SpecTranslate ctx (OMap k v)
  where
  type SpecRep (OMap k v) = [(SpecRep k, SpecRep v)]

  toSpecRep :: OMap k v -> SpecTransM ctx (SpecRep (OMap k v))
toSpecRep = forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (forall (t :: * -> * -> *) (f :: * -> *) a c b d.
(Bitraversable t, Applicative f) =>
(a -> f c) -> (b -> f d) -> t a b -> f (t c d)
bimapM forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k v. Ord k => OMap k v -> [(k, v)]
OMap.assocList

instance
  ( EraPParams era
  , SpecTranslate ctx (PParamsHKD StrictMaybe era)
  , SpecRep (PParamsHKD StrictMaybe era) ~ Agda.PParamsUpdate
  ) =>
  SpecTranslate ctx (ProposalProcedure era)
  where
  type SpecRep (ProposalProcedure era) = Agda.GovProposal

  toSpecRep :: ProposalProcedure era
-> SpecTransM ctx (SpecRep (ProposalProcedure era))
toSpecRep ProposalProcedure {Anchor
Coin
RewardAccount
GovAction era
pProcAnchor :: forall era. ProposalProcedure era -> Anchor
pProcGovAction :: forall era. ProposalProcedure era -> GovAction era
pProcReturnAddr :: forall era. ProposalProcedure era -> RewardAccount
pProcDeposit :: forall era. ProposalProcedure era -> Coin
pProcAnchor :: Anchor
pProcGovAction :: GovAction era
pProcReturnAddr :: RewardAccount
pProcDeposit :: Coin
..} =
    GovAction
-> ExUnits
-> Maybe Integer
-> Integer
-> RwdAddr
-> Anchor
-> GovProposal
Agda.MkGovProposal
      forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep GovAction era
pProcGovAction
      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 (forall era. StrictMaybe GovActionId -> GovAction era -> GovActionId
nullifyIfNotNeeded StrictMaybe GovActionId
prevActionId GovAction era
pProcGovAction)
      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 StrictMaybe ScriptHash
policy
      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 Coin
pProcDeposit
      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 RewardAccount
pProcReturnAddr
      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 Anchor
pProcAnchor
    where
      prevActionId :: StrictMaybe GovActionId
prevActionId = forall era. GovAction era -> StrictMaybe GovActionId
prevGovActionId GovAction era
pProcGovAction
      policy :: StrictMaybe ScriptHash
policy =
        case GovAction era
pProcGovAction of
          TreasuryWithdrawals Map RewardAccount Coin
_ StrictMaybe ScriptHash
sh -> StrictMaybe ScriptHash
sh
          ParameterChange StrictMaybe (GovPurposeId 'PParamUpdatePurpose era)
_ PParamsUpdate era
_ StrictMaybe ScriptHash
sh -> StrictMaybe ScriptHash
sh
          GovAction era
_ -> forall a. StrictMaybe a
SNothing

prevGovActionId :: GovAction era -> StrictMaybe GovActionId
prevGovActionId :: forall era. GovAction era -> StrictMaybe GovActionId
prevGovActionId GovAction era
action =
  case GovAction era
action of
    ParameterChange StrictMaybe (GovPurposeId 'PParamUpdatePurpose era)
x PParamsUpdate era
_ StrictMaybe ScriptHash
_ -> forall (p :: GovActionPurpose) era.
GovPurposeId p era -> GovActionId
unGovPurposeId forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StrictMaybe (GovPurposeId 'PParamUpdatePurpose era)
x
    HardForkInitiation StrictMaybe (GovPurposeId 'HardForkPurpose era)
x ProtVer
_ -> forall (p :: GovActionPurpose) era.
GovPurposeId p era -> GovActionId
unGovPurposeId forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StrictMaybe (GovPurposeId 'HardForkPurpose era)
x
    UpdateCommittee StrictMaybe (GovPurposeId 'CommitteePurpose era)
x Set (Credential 'ColdCommitteeRole)
_ Map (Credential 'ColdCommitteeRole) EpochNo
_ UnitInterval
_ -> forall (p :: GovActionPurpose) era.
GovPurposeId p era -> GovActionId
unGovPurposeId forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StrictMaybe (GovPurposeId 'CommitteePurpose era)
x
    NoConfidence StrictMaybe (GovPurposeId 'CommitteePurpose era)
x -> forall (p :: GovActionPurpose) era.
GovPurposeId p era -> GovActionId
unGovPurposeId forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StrictMaybe (GovPurposeId 'CommitteePurpose era)
x
    NewConstitution StrictMaybe (GovPurposeId 'ConstitutionPurpose era)
x Constitution era
_ -> forall (p :: GovActionPurpose) era.
GovPurposeId p era -> GovActionId
unGovPurposeId forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StrictMaybe (GovPurposeId 'ConstitutionPurpose era)
x
    GovAction era
_ -> forall a. StrictMaybe a
SNothing

nullGovActionId :: GovActionId
nullGovActionId :: GovActionId
nullGovActionId = TxId -> GovActionIx -> GovActionId
GovActionId (SafeHash EraIndependentTxBody -> TxId
TxId forall a. Default a => a
def) (Word16 -> GovActionIx
GovActionIx Word16
0)

nullifyIfNotNeeded :: StrictMaybe GovActionId -> GovAction era -> GovActionId
nullifyIfNotNeeded :: forall era. StrictMaybe GovActionId -> GovAction era -> GovActionId
nullifyIfNotNeeded StrictMaybe GovActionId
SNothing = forall a b. a -> b -> a
const GovActionId
nullGovActionId
nullifyIfNotNeeded (SJust GovActionId
gaId) = \case
  TreasuryWithdrawals {} -> GovActionId
nullGovActionId
  GovAction era
InfoAction -> GovActionId
nullGovActionId
  GovAction era
_ -> GovActionId
gaId

unionsHSMaps :: [Agda.HSMap k v] -> Agda.HSMap k v
unionsHSMaps :: forall k v. [HSMap k v] -> HSMap k v
unionsHSMaps [] = forall k v. [(k, v)] -> HSMap k v
Agda.MkHSMap []
unionsHSMaps ((Agda.MkHSMap [(k, v)]
x) : [HSMap k v]
xs) =
  let Agda.MkHSMap [(k, v)]
xs' = forall k v. [HSMap k v] -> HSMap k v
unionsHSMaps [HSMap k v]
xs
   in forall k v. [(k, v)] -> HSMap k v
Agda.MkHSMap forall a b. (a -> b) -> a -> b
$ [(k, v)]
x forall a. Semigroup a => a -> a -> a
<> [(k, v)]
xs'

mapHSMapKey :: (k -> l) -> Agda.HSMap k v -> Agda.HSMap l v
mapHSMapKey :: forall k l v. (k -> l) -> HSMap k v -> HSMap l v
mapHSMapKey k -> l
f (Agda.MkHSMap [(k, v)]
l) = forall k v. [(k, v)] -> HSMap k v
Agda.MkHSMap forall a b. (a -> b) -> a -> b
$ forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first k -> l
f forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(k, v)]
l

instance
  ( EraPParams era
  , SpecTranslate ctx (PParamsHKD StrictMaybe era)
  , SpecRep (PParamsHKD StrictMaybe era) ~ Agda.PParamsUpdate
  ) =>
  SpecTranslate ctx (GovActionState era)
  where
  type SpecRep (GovActionState era) = Agda.GovActionState

  toSpecRep :: GovActionState era -> SpecTransM ctx (SpecRep (GovActionState era))
toSpecRep gas :: GovActionState era
gas@GovActionState {Map (KeyHash 'StakePool) Vote
Map (Credential 'DRepRole) Vote
Map (Credential 'HotCommitteeRole) Vote
ProposalProcedure era
GovActionId
EpochNo
gasExpiresAfter :: forall era. GovActionState era -> EpochNo
gasProposedIn :: forall era. GovActionState era -> EpochNo
gasProposalProcedure :: forall era. GovActionState era -> ProposalProcedure era
gasStakePoolVotes :: forall era. GovActionState era -> Map (KeyHash 'StakePool) Vote
gasDRepVotes :: forall era. GovActionState era -> Map (Credential 'DRepRole) Vote
gasCommitteeVotes :: forall era.
GovActionState era -> Map (Credential 'HotCommitteeRole) Vote
gasId :: forall era. GovActionState era -> GovActionId
gasExpiresAfter :: EpochNo
gasProposedIn :: EpochNo
gasProposalProcedure :: ProposalProcedure era
gasStakePoolVotes :: Map (KeyHash 'StakePool) Vote
gasDRepVotes :: Map (Credential 'DRepRole) Vote
gasCommitteeVotes :: Map (Credential 'HotCommitteeRole) Vote
gasId :: GovActionId
..} = do
    HSMap (GovRole, Credential) Vote
-> RwdAddr -> Integer -> GovAction -> ExUnits -> GovActionState
Agda.MkGovActionState
      forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SpecTransM ctx (HSMap (GovRole, Credential) Vote)
agdaVoteMap
      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 (forall era. GovActionState era -> RewardAccount
gasReturnAddr GovActionState era
gas)
      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 EpochNo
gasExpiresAfter
      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 GovAction era
action
      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 (forall era. StrictMaybe GovActionId -> GovAction era -> GovActionId
nullifyIfNotNeeded (forall era. GovAction era -> StrictMaybe GovActionId
prevGovActionId GovAction era
action) GovAction era
action)
    where
      action :: GovAction era
action = forall era. GovActionState era -> GovAction era
gasAction GovActionState era
gas
      agdaVoteMap :: SpecTransM ctx (Agda.HSMap (Agda.GovRole, Agda.Credential) Agda.Vote)
      agdaVoteMap :: SpecTransM ctx (HSMap (GovRole, Credential) Vote)
agdaVoteMap = do
        HSMap Credential Vote
drepVotes <- forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep Map (Credential 'DRepRole) Vote
gasDRepVotes
        HSMap Credential Vote
ccVotes <- forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep Map (Credential 'HotCommitteeRole) Vote
gasCommitteeVotes
        HSMap Integer Vote
spoVotes <- forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep Map (KeyHash 'StakePool) Vote
gasStakePoolVotes
        forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$
          forall k v. [HSMap k v] -> HSMap k v
unionsHSMaps
            [ forall k l v. (k -> l) -> HSMap k v -> HSMap l v
mapHSMapKey (GovRole
Agda.DRep,) HSMap Credential Vote
drepVotes
            , forall k l v. (k -> l) -> HSMap k v -> HSMap l v
mapHSMapKey (GovRole
Agda.CC,) HSMap Credential Vote
ccVotes
            , forall k l v. (k -> l) -> HSMap k v -> HSMap l v
mapHSMapKey (\Integer
h -> (GovRole
Agda.SPO, Integer -> Credential
Agda.KeyHashObj Integer
h)) HSMap Integer Vote
spoVotes
            ]

instance SpecTranslate ctx GovActionIx where
  type SpecRep GovActionIx = Integer

  toSpecRep :: GovActionIx -> SpecTransM ctx (SpecRep GovActionIx)
toSpecRep = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (Integral a, Num b) => a -> b
fromIntegral forall b c a. (b -> c) -> (a -> b) -> a -> c
. GovActionIx -> Word16
unGovActionIx

instance SpecTranslate ctx GovActionId where
  type SpecRep GovActionId = Agda.GovActionID

  toSpecRep :: GovActionId -> SpecTransM ctx (SpecRep GovActionId)
toSpecRep (GovActionId TxId
txId GovActionIx
gaIx) = forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep (TxId
txId, GovActionIx
gaIx)

instance
  ( EraPParams era
  , SpecTranslate ctx (PParamsHKD StrictMaybe era)
  , SpecRep (PParamsHKD StrictMaybe era) ~ Agda.PParamsUpdate
  ) =>
  SpecTranslate ctx (Proposals era)
  where
  type SpecRep (Proposals era) = Agda.GovState

  -- TODO get rid of `prioritySort` once we've changed the implementation so
  -- that the proposals are always sorted
  toSpecRep :: Proposals era -> SpecTransM ctx (SpecRep (Proposals era))
toSpecRep = forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep forall b c a. (b -> c) -> (a -> b) -> a -> c
. OMap GovActionId (GovActionState era)
-> OMap GovActionId (GovActionState era)
prioritySort forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a s. Getting a s a -> s -> a
view forall era.
Lens' (Proposals era) (OMap GovActionId (GovActionState era))
pPropsL
    where
      prioritySort ::
        OMap GovActionId (GovActionState era) ->
        OMap GovActionId (GovActionState era)
      prioritySort :: OMap GovActionId (GovActionState era)
-> OMap GovActionId (GovActionState era)
prioritySort = forall l. IsList l => [Item l] -> l
Exts.fromList forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall b a. Ord b => (a -> b) -> [a] -> [a]
sortOn (forall era. GovAction era -> Int
actionPriority forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era. GovActionState era -> GovAction era
gasAction) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall l. IsList l => l -> [Item l]
Exts.toList

instance SpecTranslate ctx MaryValue where
  type SpecRep MaryValue = Agda.Coin

  toSpecRep :: MaryValue -> SpecTransM ctx (SpecRep MaryValue)
toSpecRep = forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t. Val t => t -> Coin
coin

instance
  ( ToExpr (PredicateFailure (EraRule "DELEG" era))
  , ToExpr (PredicateFailure (EraRule "GOVCERT" era))
  , ToExpr (PredicateFailure (EraRule "POOL" era))
  ) =>
  SpecTranslate ctx (ConwayCertPredFailure era)
  where
  type SpecRep (ConwayCertPredFailure era) = OpaqueErrorString

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

instance (SpecTranslate ctx a, Compactible a) => SpecTranslate ctx (CompactForm a) where
  type SpecRep (CompactForm a) = SpecRep a

  toSpecRep :: CompactForm a -> SpecTransM ctx (SpecRep (CompactForm a))
toSpecRep = forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Compactible a => CompactForm a -> a
fromCompact

instance SpecTranslate ctx CommitteeAuthorization where
  type
    SpecRep CommitteeAuthorization =
      SpecRep (Maybe (Credential 'HotCommitteeRole))

  toSpecRep :: CommitteeAuthorization
-> SpecTransM ctx (SpecRep CommitteeAuthorization)
toSpecRep (CommitteeHotCredential Credential 'HotCommitteeRole
c) = forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just Credential 'HotCommitteeRole
c
  toSpecRep (CommitteeMemberResigned StrictMaybe Anchor
_) =
    forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep forall a b. (a -> b) -> a -> b
$
      forall a. Maybe a
Nothing @(Credential 'HotCommitteeRole)

instance SpecTranslate ctx (CommitteeState era) where
  type
    SpecRep (CommitteeState era) =
      SpecRep (Map (Credential 'ColdCommitteeRole) CommitteeAuthorization)

  toSpecRep :: CommitteeState era -> SpecTransM ctx (SpecRep (CommitteeState era))
toSpecRep = forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era.
CommitteeState era
-> Map (Credential 'ColdCommitteeRole) CommitteeAuthorization
csCommitteeCreds

instance SpecTranslate ctx IndividualPoolStake where
  type SpecRep IndividualPoolStake = SpecRep Coin

  toSpecRep :: IndividualPoolStake -> SpecTransM ctx (SpecRep IndividualPoolStake)
toSpecRep (IndividualPoolStake Rational
_ CompactForm Coin
c VRFVerKeyHash 'StakePoolVRF
_) = forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep CompactForm Coin
c

instance SpecTranslate ctx PoolDistr where
  type SpecRep PoolDistr = Agda.HSMap Agda.VDeleg Agda.Coin

  toSpecRep :: PoolDistr -> SpecTransM ctx (SpecRep PoolDistr)
toSpecRep (PoolDistr Map (KeyHash 'StakePool) IndividualPoolStake
ps CompactForm Coin
_) = do
    Agda.MkHSMap [ExUnits]
l <- forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep Map (KeyHash 'StakePool) IndividualPoolStake
ps
    forall (f :: * -> *) a. Applicative f => a -> f a
pure forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k v. [(k, v)] -> HSMap k v
Agda.MkHSMap forall a b. (a -> b) -> a -> b
$ forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first (GovRole -> Credential -> VDeleg
Agda.CredVoter GovRole
Agda.SPO forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> Credential
Agda.KeyHashObj) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [ExUnits]
l

instance
  Inject ctx Coin =>
  SpecTranslate ctx (RatifyEnv era)
  where
  type SpecRep (RatifyEnv era) = Agda.RatifyEnv

  toSpecRep :: RatifyEnv era -> SpecTransM ctx (SpecRep (RatifyEnv era))
toSpecRep RatifyEnv {Map DRep (CompactForm Coin)
Map (KeyHash 'StakePool) PoolParams
Map (Credential 'Staking) DRep
Map (Credential 'DRepRole) DRepState
PoolDistr
CommitteeState era
InstantStake era
EpochNo
reInstantStake :: forall era. RatifyEnv era -> InstantStake era
reStakePoolDistr :: forall era. RatifyEnv era -> PoolDistr
reDRepDistr :: forall era. RatifyEnv era -> Map DRep (CompactForm Coin)
reDRepState :: forall era. RatifyEnv era -> Map (Credential 'DRepRole) DRepState
reCurrentEpoch :: forall era. RatifyEnv era -> EpochNo
reCommitteeState :: forall era. RatifyEnv era -> CommitteeState era
reDelegatees :: forall era. RatifyEnv era -> Map (Credential 'Staking) DRep
rePoolParams :: forall era. RatifyEnv era -> Map (KeyHash 'StakePool) PoolParams
rePoolParams :: Map (KeyHash 'StakePool) PoolParams
reDelegatees :: Map (Credential 'Staking) DRep
reCommitteeState :: CommitteeState era
reCurrentEpoch :: EpochNo
reDRepState :: Map (Credential 'DRepRole) DRepState
reDRepDistr :: Map DRep (CompactForm Coin)
reStakePoolDistr :: PoolDistr
reInstantStake :: InstantStake era
..} = do
    let
      stakeDistrs :: SpecTransM ctx StakeDistrs
stakeDistrs = do
        Agda.MkHSMap [(VDeleg, Integer)]
stakeDistrsMap <- forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep PoolDistr
reStakePoolDistr
        [(VDeleg, Integer)]
drepDistrsMap <- forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep forall a b. (a -> b) -> a -> b
$ forall k a. Map k a -> [(k, a)]
Map.toList Map DRep (CompactForm Coin)
reDRepDistr
        forall (f :: * -> *) a. Applicative f => a -> f a
pure forall b c a. (b -> c) -> (a -> b) -> a -> c
. HSMap VDeleg Integer -> StakeDistrs
Agda.StakeDistrs forall a b. (a -> b) -> a -> b
$ forall k v. [(k, v)] -> HSMap k v
Agda.MkHSMap ([(VDeleg, Integer)]
stakeDistrsMap forall a. Semigroup a => a -> a -> a
<> [(VDeleg, Integer)]
drepDistrsMap)
      dreps :: SpecTransM ctx (SpecRep (Map (Credential 'DRepRole) EpochNo))
dreps = forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep forall a b. (a -> b) -> a -> b
$ forall a b k. (a -> b) -> Map k a -> Map k b
Map.map DRepState -> EpochNo
drepExpiry Map (Credential 'DRepRole) DRepState
reDRepState
    Coin
treasury <- forall b ctx. Inject ctx b => SpecTransM ctx b
askCtx @Coin
    StakeDistrs
-> Integer
-> HSMap Credential Integer
-> HSMap Credential (Maybe Credential)
-> Integer
-> HSMap Integer PoolParams
-> HSMap Credential VDeleg
-> RatifyEnv
Agda.MkRatifyEnv
      forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SpecTransM ctx StakeDistrs
stakeDistrs
      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 EpochNo
reCurrentEpoch
      forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> SpecTransM ctx (SpecRep (Map (Credential 'DRepRole) EpochNo))
dreps
      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 CommitteeState era
reCommitteeState
      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 Coin
treasury
      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 Map (KeyHash 'StakePool) PoolParams
rePoolParams
      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 Map (Credential 'Staking) DRep
reDelegatees

instance SpecTranslate ctx Bool where
  type SpecRep Bool = Bool

  toSpecRep :: Bool -> SpecTransM ctx (SpecRep Bool)
toSpecRep = forall (f :: * -> *) a. Applicative f => a -> f a
pure

instance
  ( EraPParams era
  , SpecRep (PParamsHKD Identity era) ~ Agda.PParams
  , SpecTranslate ctx (PParamsHKD Identity era)
  , Inject ctx [GovActionState era]
  , ToExpr (PParamsHKD StrictMaybe era)
  , SpecRep (PParamsHKD StrictMaybe era) ~ Agda.PParamsUpdate
  , SpecTranslate ctx (PParamsHKD StrictMaybe era)
  ) =>
  SpecTranslate ctx (RatifyState era)
  where
  type SpecRep (RatifyState era) = Agda.RatifyState

  toSpecRep :: RatifyState era -> SpecTransM ctx (SpecRep (RatifyState era))
toSpecRep RatifyState {Bool
Set GovActionId
EnactState era
Seq (GovActionState era)
rsDelayed :: forall era. RatifyState era -> Bool
rsExpired :: forall era. RatifyState era -> Set GovActionId
rsEnacted :: forall era. RatifyState era -> Seq (GovActionState era)
rsEnactState :: forall era. RatifyState era -> EnactState era
rsDelayed :: Bool
rsExpired :: Set GovActionId
rsEnacted :: Seq (GovActionState era)
rsEnactState :: EnactState era
..} = do
    Map GovActionId (GovActionState era)
govActionMap <-
      forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' (\Map GovActionId (GovActionState era)
acc GovActionState era
gas -> forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert (forall era. GovActionState era -> GovActionId
gasId GovActionState era
gas) GovActionState era
gas Map GovActionId (GovActionState era)
acc) forall a. Monoid a => a
mempty
        forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall b ctx. Inject ctx b => SpecTransM ctx b
askCtx @[GovActionState era]
    let
      lookupGAS :: GovActionId
-> SpecTransM ctx (Set (GovActionId, GovActionState era))
-> SpecTransM ctx (Set (GovActionId, GovActionState era))
lookupGAS GovActionId
gaId SpecTransM ctx (Set (GovActionId, GovActionState era))
m = do
        case forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup GovActionId
gaId Map GovActionId (GovActionState era)
govActionMap of
          Just GovActionState era
x -> forall a. Ord a => a -> Set a -> Set a
Set.insert (GovActionId
gaId, GovActionState era
x) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SpecTransM ctx (Set (GovActionId, GovActionState era))
m
          Maybe (GovActionState era)
Nothing ->
            forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError forall a b. (a -> b) -> a -> b
$
              Text
"gaId: "
                forall a. Semigroup a => a -> a -> a
<> [Char] -> Text
T.pack (forall a. ToExpr a => a -> [Char]
showExpr GovActionId
gaId)
                forall a. Semigroup a => a -> a -> a
<> Text
"\n\ngovActionMap: "
                forall a. Semigroup a => a -> a -> a
<> [Char] -> Text
T.pack (forall a. ToExpr a => a -> [Char]
showExpr Map GovActionId (GovActionState era)
govActionMap)
                forall a. Semigroup a => a -> a -> a
<> Text
"\n\nGovActionId is not contained in the govActionMap"
    Set (GovActionId, GovActionState era)
removed <-
      forall a b. (a -> b -> b) -> b -> Set a -> b
Set.foldr'
        GovActionId
-> SpecTransM ctx (Set (GovActionId, GovActionState era))
-> SpecTransM ctx (Set (GovActionId, GovActionState era))
lookupGAS
        (forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a. Set a
Set.empty)
        (Set GovActionId
rsExpired forall a. Ord a => Set a -> Set a -> Set a
`Set.union` forall a. Ord a => [a] -> Set a
Set.fromList (forall era. GovActionState era -> GovActionId
gasId forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) a. Foldable t => t a -> [a]
toList Seq (GovActionState era)
rsEnacted))
    EnactState
-> HSSet (ExUnits, GovActionState) -> Bool -> RatifyState
Agda.MkRatifyState
      forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep EnactState era
rsEnactState
      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 Set (GovActionId, GovActionState era)
removed
      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 Bool
rsDelayed

instance
  ( EraPParams era
  , SpecTranslate ctx (PParamsHKD StrictMaybe era)
  , SpecRep (PParamsHKD StrictMaybe era) ~ Agda.PParamsUpdate
  ) =>
  SpecTranslate ctx (RatifySignal era)
  where
  type
    SpecRep (RatifySignal era) =
      SpecRep [(GovActionId, GovActionState era)]

  toSpecRep :: RatifySignal era -> SpecTransM ctx (SpecRep (RatifySignal era))
toSpecRep (RatifySignal StrictSeq (GovActionState era)
x) =
    forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep forall a b. (a -> b) -> a -> b
$
      (\gas :: GovActionState era
gas@GovActionState {GovActionId
gasId :: GovActionId
gasId :: forall era. GovActionState era -> GovActionId
gasId} -> (GovActionId
gasId, GovActionState era
gas)) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StrictSeq (GovActionState era)
x

instance
  ( EraPParams era
  , SpecTranslate ctx (PParamsHKD StrictMaybe era)
  , SpecRep (PParamsHKD StrictMaybe era) ~ Agda.PParamsUpdate
  ) =>
  SpecTranslate ctx (EnactSignal era)
  where
  type SpecRep (EnactSignal era) = SpecRep (GovAction era)

  toSpecRep :: EnactSignal era -> SpecTransM ctx (SpecRep (EnactSignal era))
toSpecRep (EnactSignal GovActionId
_ GovAction era
ga) = forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep GovAction era
ga

instance ToExpr (EpochExecEnv era)
instance Era era => NFData (EpochExecEnv era)

instance HasSimpleRep (EpochExecEnv era)
instance Era era => HasSpec (EpochExecEnv era)

instance SpecTranslate ctx (EpochExecEnv era) where
  type SpecRep (EpochExecEnv era) = ()

  toSpecRep :: EpochExecEnv era -> SpecTransM ctx (SpecRep (EpochExecEnv era))
toSpecRep EpochExecEnv era
_ = forall (f :: * -> *) a. Applicative f => a -> f a
pure ()

-- | This type is used as the Env only in the Agda Spec
data ConwayExecEnactEnv era = ConwayExecEnactEnv
  { forall era. ConwayExecEnactEnv era -> GovActionId
ceeeGid :: GovActionId
  , forall era. ConwayExecEnactEnv era -> Coin
ceeeTreasury :: Coin
  , forall era. ConwayExecEnactEnv era -> EpochNo
ceeeEpoch :: EpochNo
  }
  deriving (forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall era x.
Rep (ConwayExecEnactEnv era) x -> ConwayExecEnactEnv era
forall era x.
ConwayExecEnactEnv era -> Rep (ConwayExecEnactEnv era) x
$cto :: forall era x.
Rep (ConwayExecEnactEnv era) x -> ConwayExecEnactEnv era
$cfrom :: forall era x.
ConwayExecEnactEnv era -> Rep (ConwayExecEnactEnv era) x
Generic, ConwayExecEnactEnv era -> ConwayExecEnactEnv era -> Bool
forall era.
ConwayExecEnactEnv era -> ConwayExecEnactEnv era -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: ConwayExecEnactEnv era -> ConwayExecEnactEnv era -> Bool
$c/= :: forall era.
ConwayExecEnactEnv era -> ConwayExecEnactEnv era -> Bool
== :: ConwayExecEnactEnv era -> ConwayExecEnactEnv era -> Bool
$c== :: forall era.
ConwayExecEnactEnv era -> ConwayExecEnactEnv era -> Bool
Eq, Int -> ConwayExecEnactEnv era -> ShowS
forall era. Int -> ConwayExecEnactEnv era -> ShowS
forall era. [ConwayExecEnactEnv era] -> ShowS
forall era. ConwayExecEnactEnv era -> [Char]
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
showList :: [ConwayExecEnactEnv era] -> ShowS
$cshowList :: forall era. [ConwayExecEnactEnv era] -> ShowS
show :: ConwayExecEnactEnv era -> [Char]
$cshow :: forall era. ConwayExecEnactEnv era -> [Char]
showsPrec :: Int -> ConwayExecEnactEnv era -> ShowS
$cshowsPrec :: forall era. Int -> ConwayExecEnactEnv era -> ShowS
Show)

-- | Here we inject the Agda Spec Env into the STS rule Environment, which is ().
instance Inject (ConwayExecEnactEnv era) () where
  inject :: ConwayExecEnactEnv era -> ()
inject ConwayExecEnactEnv era
_ = ()

instance ToExpr (ConwayExecEnactEnv era)
instance Era era => NFData (ConwayExecEnactEnv era)

instance HasSimpleRep (ConwayExecEnactEnv era)
instance Era era => HasSpec (ConwayExecEnactEnv era)

instance SpecTranslate ctx (ConwayExecEnactEnv era) where
  type SpecRep (ConwayExecEnactEnv era) = Agda.EnactEnv

  toSpecRep :: ConwayExecEnactEnv era
-> SpecTransM ctx (SpecRep (ConwayExecEnactEnv era))
toSpecRep ConwayExecEnactEnv {Coin
GovActionId
EpochNo
ceeeEpoch :: EpochNo
ceeeTreasury :: Coin
ceeeGid :: GovActionId
ceeeEpoch :: forall era. ConwayExecEnactEnv era -> EpochNo
ceeeTreasury :: forall era. ConwayExecEnactEnv era -> Coin
ceeeGid :: forall era. ConwayExecEnactEnv era -> GovActionId
..} =
    ExUnits -> Integer -> Integer -> EnactEnv
Agda.MkEnactEnv
      forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep GovActionId
ceeeGid
      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 Coin
ceeeTreasury
      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 EpochNo
ceeeEpoch

committeeCredentialToStrictMaybe ::
  CommitteeAuthorization ->
  StrictMaybe (Credential 'HotCommitteeRole)
committeeCredentialToStrictMaybe :: CommitteeAuthorization
-> StrictMaybe (Credential 'HotCommitteeRole)
committeeCredentialToStrictMaybe (CommitteeHotCredential Credential 'HotCommitteeRole
c) = forall a. a -> StrictMaybe a
SJust Credential 'HotCommitteeRole
c
committeeCredentialToStrictMaybe (CommitteeMemberResigned StrictMaybe Anchor
_) = forall a. StrictMaybe a
SNothing

instance SpecTranslate ctx DepositPurpose where
  type SpecRep DepositPurpose = Agda.DepositPurpose
  toSpecRep :: DepositPurpose -> SpecTransM ctx (SpecRep DepositPurpose)
toSpecRep (CredentialDeposit Credential 'Staking
cred) =
    Credential -> DepositPurpose
Agda.CredentialDeposit forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep Credential 'Staking
cred
  toSpecRep (PoolDeposit KeyHash 'StakePool
kh) =
    Integer -> DepositPurpose
Agda.PoolDeposit forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep KeyHash 'StakePool
kh
  toSpecRep (DRepDeposit Credential 'DRepRole
cred) =
    Credential -> DepositPurpose
Agda.DRepDeposit forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep Credential 'DRepRole
cred
  toSpecRep (GovActionDeposit GovActionId
gid) =
    ExUnits -> DepositPurpose
Agda.GovActionDeposit forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep GovActionId
gid