{-# 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 = Void -> SpecTransM ctx Void
Void -> SpecTransM ctx (SpecRep Void)
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 = (a -> SpecTransM ctx (SpecRep a))
-> [a] -> SpecTransM ctx [SpecRep a]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse a -> SpecTransM ctx (SpecRep a)
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) = Integer -> SpecTransM ctx Integer
forall a. a -> SpecTransM ctx a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Integer -> SpecTransM ctx Integer)
-> Integer -> SpecTransM ctx Integer
forall a b. (a -> b) -> a -> b
$ Word16 -> Integer
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) = (TxId, TxIx) -> SpecTransM ctx (SpecRep (TxId, 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 StakeCredential
c) = Credential -> Maybe Credential
forall a. a -> Maybe a
Just (Credential -> Maybe Credential)
-> SpecTransM ctx Credential -> SpecTransM ctx (Maybe Credential)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StakeCredential -> SpecTransM ctx (SpecRep StakeCredential)
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep StakeCredential
c
  toSpecRep (StakeRefPtr Ptr
_) = Maybe Credential -> SpecTransM ctx (Maybe Credential)
forall a. a -> SpecTransM ctx a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe Credential
forall a. Maybe a
Nothing
  toSpecRep StakeReference
StakeRefNull = Maybe Credential -> SpecTransM ctx (Maybe Credential)
forall a. a -> SpecTransM ctx a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe Credential
forall a. Maybe a
Nothing

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

  toSpecRep :: BootstrapAddress -> SpecTransM ctx (SpecRep BootstrapAddress)
toSpecRep BootstrapAddress
_ = [Char] -> SpecTransM ctx BootstrapAddr
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) =
    BaseAddr -> Either BaseAddr BootstrapAddr
forall a b. a -> Either a b
Left
      (BaseAddr -> Either BaseAddr BootstrapAddr)
-> SpecTransM ctx BaseAddr
-> SpecTransM ctx (Either BaseAddr BootstrapAddr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Integer -> Credential -> Maybe Credential -> BaseAddr
Agda.BaseAddr (Integer -> Credential -> Maybe Credential -> BaseAddr)
-> SpecTransM ctx Integer
-> SpecTransM ctx (Credential -> Maybe Credential -> BaseAddr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Network -> SpecTransM ctx (SpecRep Network)
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep Network
nw SpecTransM ctx (Credential -> Maybe Credential -> BaseAddr)
-> SpecTransM ctx Credential
-> SpecTransM ctx (Maybe Credential -> BaseAddr)
forall a b.
SpecTransM ctx (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> PaymentCredential -> SpecTransM ctx (SpecRep PaymentCredential)
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep PaymentCredential
pc SpecTransM ctx (Maybe Credential -> BaseAddr)
-> SpecTransM ctx (Maybe Credential) -> SpecTransM ctx BaseAddr
forall a b.
SpecTransM ctx (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> StakeReference -> SpecTransM ctx (SpecRep StakeReference)
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep StakeReference
sr)
  toSpecRep (AddrBootstrap BootstrapAddress
ba) = BootstrapAddr -> Either BaseAddr BootstrapAddr
forall a b. b -> Either a b
Right (BootstrapAddr -> Either BaseAddr BootstrapAddr)
-> SpecTransM ctx BootstrapAddr
-> SpecTransM ctx (Either BaseAddr BootstrapAddr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> BootstrapAddress -> SpecTransM ctx (SpecRep BootstrapAddress)
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 = Integer -> SpecTransM ctx Integer
forall a. a -> SpecTransM ctx a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Integer -> SpecTransM ctx Integer)
-> (Hash a b -> Integer) -> Hash a b -> SpecTransM ctx Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Hash a b -> Integer
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 = Hash HASH a -> SpecTransM ctx Integer
Hash HASH a -> SpecTransM ctx (SpecRep (Hash HASH a))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep (Hash HASH a -> SpecTransM ctx Integer)
-> (SafeHash a -> Hash HASH a)
-> SafeHash a
-> SpecTransM ctx Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SafeHash a -> Hash HASH a
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 = DataHash -> SpecTransM ctx Integer
DataHash -> SpecTransM ctx (SpecRep DataHash)
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep (DataHash -> SpecTransM ctx Integer)
-> (BinaryData era -> DataHash)
-> BinaryData era
-> SpecTransM ctx Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BinaryData era -> DataHash
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 = Maybe (Either Integer Integer)
-> SpecTransM ctx (Maybe (Either Integer Integer))
forall a. a -> SpecTransM ctx a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe (Either Integer Integer)
forall a. Maybe a
Nothing
  toSpecRep (Datum BinaryData era
d) = Either Integer Integer -> Maybe (Either Integer Integer)
forall a. a -> Maybe a
Just (Either Integer Integer -> Maybe (Either Integer Integer))
-> (Integer -> Either Integer Integer)
-> Integer
-> Maybe (Either Integer Integer)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> Either Integer Integer
forall a b. a -> Either a b
Left (Integer -> Maybe (Either Integer Integer))
-> SpecTransM ctx Integer
-> SpecTransM ctx (Maybe (Either Integer Integer))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> BinaryData era -> SpecTransM ctx (SpecRep (BinaryData era))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep BinaryData era
d
  toSpecRep (DatumHash DataHash
h) = Either Integer Integer -> Maybe (Either Integer Integer)
forall a. a -> Maybe a
Just (Either Integer Integer -> Maybe (Either Integer Integer))
-> (Integer -> Either Integer Integer)
-> Integer
-> Maybe (Either Integer Integer)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> Either Integer Integer
forall a b. b -> Either a b
Right (Integer -> Maybe (Either Integer Integer))
-> SpecTransM ctx Integer
-> SpecTransM ctx (Maybe (Either Integer Integer))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> DataHash -> SpecTransM ctx (SpecRep DataHash)
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
      (Timelock -> Integer -> Integer -> HSTimelock)
-> SpecTransM ctx Timelock
-> SpecTransM ctx (Integer -> Integer -> HSTimelock)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NativeScript era -> SpecTransM ctx Timelock
forall {era} {ctx}.
(Assert
   (OrdCond
      (CmpNat (ProtVerLow era) (ProtVerHigh era)) 'True 'True 'False)
   (TypeError ...),
 Assert
   (OrdCond (CmpNat 0 (ProtVerLow era)) 'True 'True 'False)
   (TypeError ...),
 Assert
   (OrdCond (CmpNat 0 (ProtVerHigh era)) 'True 'True 'False)
   (TypeError ...),
 AllegraEraScript era) =>
NativeScript era -> SpecTransM ctx Timelock
timelockToSpecRep Timelock era
NativeScript era
tl
      SpecTransM ctx (Integer -> Integer -> HSTimelock)
-> SpecTransM ctx Integer -> SpecTransM ctx (Integer -> HSTimelock)
forall a b.
SpecTransM ctx (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ScriptHash -> SpecTransM ctx (SpecRep ScriptHash)
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep (forall era. EraScript era => Script era -> ScriptHash
hashScript @era (Script era -> ScriptHash) -> Script era -> ScriptHash
forall a b. (a -> b) -> a -> b
$ Timelock era -> AlonzoScript era
forall era. Timelock era -> AlonzoScript era
TimelockScript Timelock era
tl)
      SpecTransM ctx (Integer -> HSTimelock)
-> SpecTransM ctx Integer -> SpecTransM ctx HSTimelock
forall a b.
SpecTransM ctx (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Integer -> SpecTransM ctx Integer
forall a. a -> SpecTransM ctx a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Int -> Integer) -> Int -> Integer
forall a b. (a -> b) -> a -> b
$ Timelock era -> Int
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 (Integer -> Timelock)
-> SpecTransM ctx Integer -> SpecTransM ctx Timelock
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> KeyHash 'Witness -> SpecTransM ctx (SpecRep (KeyHash 'Witness))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep KeyHash 'Witness
kh
          RequireAllOf StrictSeq (NativeScript era)
ss -> do
            StrictSeq Timelock
tls <- (NativeScript era -> SpecTransM ctx Timelock)
-> StrictSeq (NativeScript era)
-> SpecTransM ctx (StrictSeq Timelock)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> StrictSeq a -> f (StrictSeq b)
traverse NativeScript era -> SpecTransM ctx Timelock
timelockToSpecRep StrictSeq (NativeScript era)
ss
            Timelock -> SpecTransM ctx Timelock
forall a. a -> SpecTransM ctx a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Timelock -> SpecTransM ctx Timelock)
-> ([Timelock] -> Timelock)
-> [Timelock]
-> SpecTransM ctx Timelock
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Timelock] -> Timelock
Agda.RequireAllOf ([Timelock] -> SpecTransM ctx Timelock)
-> [Timelock] -> SpecTransM ctx Timelock
forall a b. (a -> b) -> a -> b
$ StrictSeq Timelock -> [Timelock]
forall a. StrictSeq a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList StrictSeq Timelock
tls
          RequireAnyOf StrictSeq (NativeScript era)
ss -> do
            StrictSeq Timelock
tls <- (NativeScript era -> SpecTransM ctx Timelock)
-> StrictSeq (NativeScript era)
-> SpecTransM ctx (StrictSeq Timelock)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> StrictSeq a -> f (StrictSeq b)
traverse NativeScript era -> SpecTransM ctx Timelock
timelockToSpecRep StrictSeq (NativeScript era)
ss
            Timelock -> SpecTransM ctx Timelock
forall a. a -> SpecTransM ctx a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Timelock -> SpecTransM ctx Timelock)
-> ([Timelock] -> Timelock)
-> [Timelock]
-> SpecTransM ctx Timelock
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Timelock] -> Timelock
Agda.RequireAnyOf ([Timelock] -> SpecTransM ctx Timelock)
-> [Timelock] -> SpecTransM ctx Timelock
forall a b. (a -> b) -> a -> b
$ StrictSeq Timelock -> [Timelock]
forall a. StrictSeq a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList StrictSeq Timelock
tls
          RequireMOf Int
m StrictSeq (NativeScript era)
ss -> do
            StrictSeq Timelock
tls <- (NativeScript era -> SpecTransM ctx Timelock)
-> StrictSeq (NativeScript era)
-> SpecTransM ctx (StrictSeq Timelock)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> StrictSeq a -> f (StrictSeq b)
traverse NativeScript era -> SpecTransM ctx Timelock
timelockToSpecRep StrictSeq (NativeScript era)
ss
            Timelock -> SpecTransM ctx Timelock
forall a. a -> SpecTransM ctx a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Timelock -> SpecTransM ctx Timelock)
-> ([Timelock] -> Timelock)
-> [Timelock]
-> SpecTransM ctx Timelock
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> [Timelock] -> Timelock
Agda.RequireMOf (Int -> Integer
forall a. Integral a => a -> Integer
toInteger Int
m) ([Timelock] -> SpecTransM ctx Timelock)
-> [Timelock] -> SpecTransM ctx Timelock
forall a b. (a -> b) -> a -> b
$ StrictSeq Timelock -> [Timelock]
forall a. StrictSeq a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList StrictSeq Timelock
tls
          RequireTimeExpire SlotNo
slot -> Integer -> Timelock
Agda.RequireTimeExpire (Integer -> Timelock)
-> SpecTransM ctx Integer -> SpecTransM ctx Timelock
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SlotNo -> SpecTransM ctx (SpecRep SlotNo)
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep SlotNo
slot
          RequireTimeStart SlotNo
slot -> Integer -> Timelock
Agda.RequireTimeStart (Integer -> Timelock)
-> SpecTransM ctx Integer -> SpecTransM ctx Timelock
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SlotNo -> SpecTransM ctx (SpecRep SlotNo)
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep SlotNo
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
      (Integer -> Integer -> HSPlutusScript)
-> SpecTransM ctx Integer
-> SpecTransM ctx (Integer -> HSPlutusScript)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ScriptHash -> SpecTransM ctx (SpecRep ScriptHash)
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep (Script era -> ScriptHash
forall era. EraScript era => Script era -> ScriptHash
hashScript (Script era -> ScriptHash) -> Script era -> ScriptHash
forall a b. (a -> b) -> a -> b
$ PlutusScript era -> AlonzoScript era
forall era. PlutusScript era -> AlonzoScript era
PlutusScript PlutusScript era
ps)
      SpecTransM ctx (Integer -> HSPlutusScript)
-> SpecTransM ctx Integer -> SpecTransM ctx HSPlutusScript
forall a b.
SpecTransM ctx (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Integer -> SpecTransM ctx Integer
forall a. a -> SpecTransM ctx a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Int -> Integer) -> Int -> Integer
forall a b. (a -> b) -> a -> b
$ PlutusScript era -> Int
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) = HSTimelock -> Either HSTimelock HSPlutusScript
forall a b. a -> Either a b
Left (HSTimelock -> Either HSTimelock HSPlutusScript)
-> SpecTransM ctx HSTimelock
-> SpecTransM ctx (Either HSTimelock HSPlutusScript)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Timelock era -> SpecTransM ctx (SpecRep (Timelock era))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep Timelock era
s
  toSpecRep (PlutusScript PlutusScript era
s) = HSPlutusScript -> Either HSTimelock HSPlutusScript
forall a b. b -> Either a b
Right (HSPlutusScript -> Either HSTimelock HSPlutusScript)
-> SpecTransM ctx HSPlutusScript
-> SpecTransM ctx (Either HSTimelock HSPlutusScript)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> PlutusScript era -> SpecTransM ctx (SpecRep (PlutusScript era))
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' <- Addr -> SpecTransM ctx (SpecRep Addr)
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep Addr
addr
    Integer
val' <- Value era -> SpecTransM ctx (SpecRep (Value era))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep Value era
val
    Maybe (Either Integer Integer)
datum' <- Datum era -> SpecTransM ctx (SpecRep (Datum era))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep Datum era
datum
    Maybe (Either HSTimelock HSPlutusScript)
script' <- StrictMaybe (AlonzoScript era)
-> SpecTransM ctx (SpecRep (StrictMaybe (AlonzoScript era)))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep StrictMaybe (Script era)
StrictMaybe (AlonzoScript era)
script
    (Either BaseAddr BootstrapAddr,
 (Integer,
  (Maybe (Either Integer Integer),
   Maybe (Either HSTimelock HSPlutusScript))))
-> SpecTransM
     ctx
     (Either BaseAddr BootstrapAddr,
      (Integer,
       (Maybe (Either Integer Integer),
        Maybe (Either HSTimelock HSPlutusScript))))
forall a. a -> SpecTransM ctx a
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 = Integer -> SpecTransM ctx Integer
Integer -> SpecTransM ctx (SpecRep Integer)
forall a. a -> SpecTransM ctx a
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) = Map TxIn (TxOut era)
-> SpecTransM ctx (SpecRep (Map TxIn (TxOut era)))
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 Nat
minor) = (Integer, Integer) -> SpecTransM ctx (Integer, Integer)
forall a. a -> SpecTransM ctx a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Version -> Integer
forall i. Integral i => Version -> i
getVersion Version
ver, Nat -> Integer
forall a. Integral a => a -> Integer
toInteger Nat
minor)

instance SpecTranslate ctx CostModels where
  type SpecRep CostModels = ()

  toSpecRep :: CostModels -> SpecTransM ctx (SpecRep CostModels)
toSpecRep CostModels
_ = () -> SpecTransM ctx ()
forall a. a -> SpecTransM ctx a
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
_ = () -> SpecTransM ctx ()
forall a. a -> SpecTransM ctx a
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 Nat
a Nat
b) = (Integer, Integer) -> SpecTransM ctx (Integer, Integer)
forall a. a -> SpecTransM ctx a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Nat -> Integer
forall a. Integral a => a -> Integer
toInteger Nat
a, Nat -> Integer
forall a. Integral a => a -> Integer
toInteger Nat
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 = HKD f a -> SpecTransM ctx (SpecRep (HKD f a))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep (HKD f a -> SpecTransM ctx (SpecRep (HKD f a)))
-> (THKD r f a -> HKD f a)
-> THKD r f a
-> SpecTransM ctx (SpecRep (HKD f a))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. THKD r f a -> HKD f a
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 :: UnitInterval
dvtCommitteeNormal :: UnitInterval
dvtCommitteeNoConfidence :: UnitInterval
dvtUpdateToConstitution :: UnitInterval
dvtHardForkInitiation :: UnitInterval
dvtPPNetworkGroup :: UnitInterval
dvtPPEconomicGroup :: UnitInterval
dvtPPTechnicalGroup :: UnitInterval
dvtPPGovGroup :: UnitInterval
dvtTreasuryWithdrawal :: 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
..} =
    Rational
-> Rational
-> Rational
-> Rational
-> Rational
-> Rational
-> Rational
-> Rational
-> Rational
-> Rational
-> DrepThresholds
Agda.MkDrepThresholds
      (Rational
 -> Rational
 -> Rational
 -> Rational
 -> Rational
 -> Rational
 -> Rational
 -> Rational
 -> Rational
 -> Rational
 -> DrepThresholds)
-> SpecTransM ctx Rational
-> SpecTransM
     ctx
     (Rational
      -> Rational
      -> Rational
      -> Rational
      -> Rational
      -> Rational
      -> Rational
      -> Rational
      -> Rational
      -> DrepThresholds)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> UnitInterval -> SpecTransM ctx (SpecRep UnitInterval)
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep UnitInterval
dvtMotionNoConfidence
      SpecTransM
  ctx
  (Rational
   -> Rational
   -> Rational
   -> Rational
   -> Rational
   -> Rational
   -> Rational
   -> Rational
   -> Rational
   -> DrepThresholds)
-> SpecTransM ctx Rational
-> SpecTransM
     ctx
     (Rational
      -> Rational
      -> Rational
      -> Rational
      -> Rational
      -> Rational
      -> Rational
      -> Rational
      -> DrepThresholds)
forall a b.
SpecTransM ctx (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> UnitInterval -> SpecTransM ctx (SpecRep UnitInterval)
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep UnitInterval
dvtCommitteeNormal
      SpecTransM
  ctx
  (Rational
   -> Rational
   -> Rational
   -> Rational
   -> Rational
   -> Rational
   -> Rational
   -> Rational
   -> DrepThresholds)
-> SpecTransM ctx Rational
-> SpecTransM
     ctx
     (Rational
      -> Rational
      -> Rational
      -> Rational
      -> Rational
      -> Rational
      -> Rational
      -> DrepThresholds)
forall a b.
SpecTransM ctx (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> UnitInterval -> SpecTransM ctx (SpecRep UnitInterval)
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep UnitInterval
dvtCommitteeNoConfidence
      SpecTransM
  ctx
  (Rational
   -> Rational
   -> Rational
   -> Rational
   -> Rational
   -> Rational
   -> Rational
   -> DrepThresholds)
-> SpecTransM ctx Rational
-> SpecTransM
     ctx
     (Rational
      -> Rational
      -> Rational
      -> Rational
      -> Rational
      -> Rational
      -> DrepThresholds)
forall a b.
SpecTransM ctx (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> UnitInterval -> SpecTransM ctx (SpecRep UnitInterval)
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep UnitInterval
dvtUpdateToConstitution
      SpecTransM
  ctx
  (Rational
   -> Rational
   -> Rational
   -> Rational
   -> Rational
   -> Rational
   -> DrepThresholds)
-> SpecTransM ctx Rational
-> SpecTransM
     ctx
     (Rational
      -> Rational -> Rational -> Rational -> Rational -> DrepThresholds)
forall a b.
SpecTransM ctx (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> UnitInterval -> SpecTransM ctx (SpecRep UnitInterval)
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep UnitInterval
dvtHardForkInitiation
      SpecTransM
  ctx
  (Rational
   -> Rational -> Rational -> Rational -> Rational -> DrepThresholds)
-> SpecTransM ctx Rational
-> SpecTransM
     ctx
     (Rational -> Rational -> Rational -> Rational -> DrepThresholds)
forall a b.
SpecTransM ctx (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> UnitInterval -> SpecTransM ctx (SpecRep UnitInterval)
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep UnitInterval
dvtPPNetworkGroup
      SpecTransM
  ctx
  (Rational -> Rational -> Rational -> Rational -> DrepThresholds)
-> SpecTransM ctx Rational
-> SpecTransM
     ctx (Rational -> Rational -> Rational -> DrepThresholds)
forall a b.
SpecTransM ctx (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> UnitInterval -> SpecTransM ctx (SpecRep UnitInterval)
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep UnitInterval
dvtPPEconomicGroup
      SpecTransM ctx (Rational -> Rational -> Rational -> DrepThresholds)
-> SpecTransM ctx Rational
-> SpecTransM ctx (Rational -> Rational -> DrepThresholds)
forall a b.
SpecTransM ctx (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> UnitInterval -> SpecTransM ctx (SpecRep UnitInterval)
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep UnitInterval
dvtPPTechnicalGroup
      SpecTransM ctx (Rational -> Rational -> DrepThresholds)
-> SpecTransM ctx Rational
-> SpecTransM ctx (Rational -> DrepThresholds)
forall a b.
SpecTransM ctx (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> UnitInterval -> SpecTransM ctx (SpecRep UnitInterval)
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep UnitInterval
dvtPPGovGroup
      SpecTransM ctx (Rational -> DrepThresholds)
-> SpecTransM ctx Rational -> SpecTransM ctx DrepThresholds
forall a b.
SpecTransM ctx (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> UnitInterval -> SpecTransM ctx (SpecRep UnitInterval)
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 :: UnitInterval
pvtCommitteeNormal :: UnitInterval
pvtCommitteeNoConfidence :: UnitInterval
pvtHardForkInitiation :: UnitInterval
pvtPPSecurityGroup :: UnitInterval
pvtMotionNoConfidence :: PoolVotingThresholds -> UnitInterval
pvtCommitteeNormal :: PoolVotingThresholds -> UnitInterval
pvtCommitteeNoConfidence :: PoolVotingThresholds -> UnitInterval
pvtHardForkInitiation :: PoolVotingThresholds -> UnitInterval
pvtPPSecurityGroup :: PoolVotingThresholds -> UnitInterval
..} =
    Rational
-> Rational -> Rational -> Rational -> Rational -> PoolThresholds
Agda.MkPoolThresholds
      (Rational
 -> Rational -> Rational -> Rational -> Rational -> PoolThresholds)
-> SpecTransM ctx Rational
-> SpecTransM
     ctx
     (Rational -> Rational -> Rational -> Rational -> PoolThresholds)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> UnitInterval -> SpecTransM ctx (SpecRep UnitInterval)
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep UnitInterval
pvtMotionNoConfidence
      SpecTransM
  ctx
  (Rational -> Rational -> Rational -> Rational -> PoolThresholds)
-> SpecTransM ctx Rational
-> SpecTransM
     ctx (Rational -> Rational -> Rational -> PoolThresholds)
forall a b.
SpecTransM ctx (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> UnitInterval -> SpecTransM ctx (SpecRep UnitInterval)
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep UnitInterval
pvtCommitteeNormal
      SpecTransM ctx (Rational -> Rational -> Rational -> PoolThresholds)
-> SpecTransM ctx Rational
-> SpecTransM ctx (Rational -> Rational -> PoolThresholds)
forall a b.
SpecTransM ctx (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> UnitInterval -> SpecTransM ctx (SpecRep UnitInterval)
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep UnitInterval
pvtCommitteeNoConfidence
      SpecTransM ctx (Rational -> Rational -> PoolThresholds)
-> SpecTransM ctx Rational
-> SpecTransM ctx (Rational -> PoolThresholds)
forall a b.
SpecTransM ctx (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> UnitInterval -> SpecTransM ctx (SpecRep UnitInterval)
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep UnitInterval
pvtHardForkInitiation
      SpecTransM ctx (Rational -> PoolThresholds)
-> SpecTransM ctx Rational -> SpecTransM ctx PoolThresholds
forall a b.
SpecTransM ctx (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> UnitInterval -> SpecTransM ctx (SpecRep UnitInterval)
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 'NetworkGroup 'SecurityGroup) Identity Word16
THKD ('PPGroups 'NetworkGroup 'SecurityGroup) Identity Word32
THKD ('PPGroups 'NetworkGroup 'SecurityGroup) Identity OrdExUnits
THKD ('PPGroups 'NetworkGroup 'NoStakePoolGroup) Identity Word16
THKD
  ('PPGroups 'NetworkGroup 'NoStakePoolGroup) Identity OrdExUnits
THKD ('PPGroups 'EconomicGroup 'SecurityGroup) Identity CoinPerByte
THKD ('PPGroups 'EconomicGroup 'SecurityGroup) Identity Coin
THKD
  ('PPGroups 'EconomicGroup 'SecurityGroup)
  Identity
  NonNegativeInterval
THKD ('PPGroups 'EconomicGroup 'NoStakePoolGroup) Identity Prices
THKD ('PPGroups 'EconomicGroup 'NoStakePoolGroup) Identity Coin
THKD
  ('PPGroups 'EconomicGroup 'NoStakePoolGroup) Identity UnitInterval
THKD ('PPGroups 'TechnicalGroup 'NoStakePoolGroup) Identity Word16
THKD
  ('PPGroups 'TechnicalGroup 'NoStakePoolGroup) Identity CostModels
THKD
  ('PPGroups 'TechnicalGroup 'NoStakePoolGroup)
  Identity
  EpochInterval
THKD
  ('PPGroups 'TechnicalGroup 'NoStakePoolGroup)
  Identity
  NonNegativeInterval
THKD ('PPGroups 'GovGroup 'SecurityGroup) Identity Coin
THKD ('PPGroups 'GovGroup 'NoStakePoolGroup) Identity Word16
THKD ('PPGroups 'GovGroup 'NoStakePoolGroup) Identity Coin
THKD
  ('PPGroups 'GovGroup 'NoStakePoolGroup)
  Identity
  DRepVotingThresholds
THKD
  ('PPGroups 'GovGroup 'NoStakePoolGroup)
  Identity
  PoolVotingThresholds
THKD ('PPGroups 'GovGroup 'NoStakePoolGroup) Identity EpochInterval
HKDNoUpdate Identity ProtVer
cppMinFeeA :: THKD ('PPGroups 'EconomicGroup 'SecurityGroup) Identity Coin
cppMinFeeB :: THKD ('PPGroups 'EconomicGroup 'SecurityGroup) Identity Coin
cppMaxBBSize :: THKD ('PPGroups 'NetworkGroup 'SecurityGroup) Identity Word32
cppMaxTxSize :: THKD ('PPGroups 'NetworkGroup 'SecurityGroup) Identity Word32
cppMaxBHSize :: THKD ('PPGroups 'NetworkGroup 'SecurityGroup) Identity Word16
cppKeyDeposit :: THKD ('PPGroups 'EconomicGroup 'NoStakePoolGroup) Identity Coin
cppPoolDeposit :: THKD ('PPGroups 'EconomicGroup 'NoStakePoolGroup) Identity Coin
cppEMax :: THKD
  ('PPGroups 'TechnicalGroup 'NoStakePoolGroup)
  Identity
  EpochInterval
cppNOpt :: THKD ('PPGroups 'TechnicalGroup 'NoStakePoolGroup) Identity Word16
cppA0 :: THKD
  ('PPGroups 'TechnicalGroup 'NoStakePoolGroup)
  Identity
  NonNegativeInterval
cppRho :: THKD
  ('PPGroups 'EconomicGroup 'NoStakePoolGroup) Identity UnitInterval
cppTau :: THKD
  ('PPGroups 'EconomicGroup 'NoStakePoolGroup) Identity UnitInterval
cppProtocolVersion :: HKDNoUpdate Identity ProtVer
cppMinPoolCost :: THKD ('PPGroups 'EconomicGroup 'NoStakePoolGroup) Identity Coin
cppCoinsPerUTxOByte :: THKD ('PPGroups 'EconomicGroup 'SecurityGroup) Identity CoinPerByte
cppCostModels :: THKD
  ('PPGroups 'TechnicalGroup 'NoStakePoolGroup) Identity CostModels
cppPrices :: THKD ('PPGroups 'EconomicGroup 'NoStakePoolGroup) Identity Prices
cppMaxTxExUnits :: THKD
  ('PPGroups 'NetworkGroup 'NoStakePoolGroup) Identity OrdExUnits
cppMaxBlockExUnits :: THKD ('PPGroups 'NetworkGroup 'SecurityGroup) Identity OrdExUnits
cppMaxValSize :: THKD ('PPGroups 'NetworkGroup 'SecurityGroup) Identity Word32
cppCollateralPercentage :: THKD ('PPGroups 'TechnicalGroup 'NoStakePoolGroup) Identity Word16
cppMaxCollateralInputs :: THKD ('PPGroups 'NetworkGroup 'NoStakePoolGroup) Identity Word16
cppPoolVotingThresholds :: THKD
  ('PPGroups 'GovGroup 'NoStakePoolGroup)
  Identity
  PoolVotingThresholds
cppDRepVotingThresholds :: THKD
  ('PPGroups 'GovGroup 'NoStakePoolGroup)
  Identity
  DRepVotingThresholds
cppCommitteeMinSize :: THKD ('PPGroups 'GovGroup 'NoStakePoolGroup) Identity Word16
cppCommitteeMaxTermLength :: THKD ('PPGroups 'GovGroup 'NoStakePoolGroup) Identity EpochInterval
cppGovActionLifetime :: THKD ('PPGroups 'GovGroup 'NoStakePoolGroup) Identity EpochInterval
cppGovActionDeposit :: THKD ('PPGroups 'GovGroup 'SecurityGroup) Identity Coin
cppDRepDeposit :: THKD ('PPGroups 'GovGroup 'NoStakePoolGroup) Identity Coin
cppDRepActivity :: THKD ('PPGroups 'GovGroup 'NoStakePoolGroup) Identity EpochInterval
cppMinFeeRefScriptCostPerByte :: THKD
  ('PPGroups 'EconomicGroup 'SecurityGroup)
  Identity
  NonNegativeInterval
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
    Integer
ppA <- THKD ('PPGroups 'EconomicGroup 'SecurityGroup) Identity Coin
-> SpecTransM
     ctx
     (SpecRep
        (THKD ('PPGroups 'EconomicGroup 'SecurityGroup) Identity Coin))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep THKD ('PPGroups 'EconomicGroup 'SecurityGroup) Identity Coin
cppMinFeeA
    Integer
ppB <- THKD ('PPGroups 'EconomicGroup 'SecurityGroup) Identity Coin
-> SpecTransM
     ctx
     (SpecRep
        (THKD ('PPGroups 'EconomicGroup 'SecurityGroup) Identity Coin))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep THKD ('PPGroups 'EconomicGroup 'SecurityGroup) Identity Coin
cppMinFeeB
    Rational
ppA0 <- THKD
  ('PPGroups 'TechnicalGroup 'NoStakePoolGroup)
  Identity
  NonNegativeInterval
-> SpecTransM
     ctx
     (SpecRep
        (THKD
           ('PPGroups 'TechnicalGroup 'NoStakePoolGroup)
           Identity
           NonNegativeInterval))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep THKD
  ('PPGroups 'TechnicalGroup 'NoStakePoolGroup)
  Identity
  NonNegativeInterval
cppA0
    Rational
ppMinFeeRefScriptCoinsPerByte <- THKD
  ('PPGroups 'EconomicGroup 'SecurityGroup)
  Identity
  NonNegativeInterval
-> SpecTransM
     ctx
     (SpecRep
        (THKD
           ('PPGroups 'EconomicGroup 'SecurityGroup)
           Identity
           NonNegativeInterval))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep THKD
  ('PPGroups 'EconomicGroup 'SecurityGroup)
  Identity
  NonNegativeInterval
cppMinFeeRefScriptCostPerByte
    Integer
ppCollateralPercentage <- THKD ('PPGroups 'TechnicalGroup 'NoStakePoolGroup) Identity Word16
-> SpecTransM
     ctx
     (SpecRep
        (THKD
           ('PPGroups 'TechnicalGroup 'NoStakePoolGroup) Identity Word16))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep THKD ('PPGroups 'TechnicalGroup 'NoStakePoolGroup) Identity Word16
cppCollateralPercentage
    let
      ppMaxBlockSize :: Integer
ppMaxBlockSize = Word32 -> Integer
forall a. Integral a => a -> Integer
toInteger (Word32 -> Integer) -> Word32 -> Integer
forall a b. (a -> b) -> a -> b
$ THKD ('PPGroups 'NetworkGroup 'SecurityGroup) Identity Word32
-> HKD Identity Word32
forall (t :: PPGroups) (f :: * -> *) a. THKD t f a -> HKD f a
unTHKD THKD ('PPGroups 'NetworkGroup 'SecurityGroup) Identity Word32
cppMaxBBSize
      ppMaxTxSize :: Integer
ppMaxTxSize = Word32 -> Integer
forall a. Integral a => a -> Integer
toInteger (Word32 -> Integer) -> Word32 -> Integer
forall a b. (a -> b) -> a -> b
$ THKD ('PPGroups 'NetworkGroup 'SecurityGroup) Identity Word32
-> HKD Identity Word32
forall (t :: PPGroups) (f :: * -> *) a. THKD t f a -> HKD f a
unTHKD THKD ('PPGroups 'NetworkGroup 'SecurityGroup) Identity Word32
cppMaxTxSize
      ppMaxHeaderSize :: Integer
ppMaxHeaderSize = Word16 -> Integer
forall a. Integral a => a -> Integer
toInteger (Word16 -> Integer) -> Word16 -> Integer
forall a b. (a -> b) -> a -> b
$ THKD ('PPGroups 'NetworkGroup 'SecurityGroup) Identity Word16
-> HKD Identity Word16
forall (t :: PPGroups) (f :: * -> *) a. THKD t f a -> HKD f a
unTHKD THKD ('PPGroups 'NetworkGroup 'SecurityGroup) Identity Word16
cppMaxBHSize
    Integer
ppKeyDeposit <- THKD ('PPGroups 'EconomicGroup 'NoStakePoolGroup) Identity Coin
-> SpecTransM
     ctx
     (SpecRep
        (THKD ('PPGroups 'EconomicGroup 'NoStakePoolGroup) Identity Coin))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep THKD ('PPGroups 'EconomicGroup 'NoStakePoolGroup) Identity Coin
cppKeyDeposit
    Integer
ppPoolDeposit <- THKD ('PPGroups 'EconomicGroup 'NoStakePoolGroup) Identity Coin
-> SpecTransM
     ctx
     (SpecRep
        (THKD ('PPGroups 'EconomicGroup 'NoStakePoolGroup) Identity Coin))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep THKD ('PPGroups 'EconomicGroup 'NoStakePoolGroup) Identity Coin
cppPoolDeposit
    Integer
ppEmax <- THKD
  ('PPGroups 'TechnicalGroup 'NoStakePoolGroup)
  Identity
  EpochInterval
-> SpecTransM
     ctx
     (SpecRep
        (THKD
           ('PPGroups 'TechnicalGroup 'NoStakePoolGroup)
           Identity
           EpochInterval))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep THKD
  ('PPGroups 'TechnicalGroup 'NoStakePoolGroup)
  Identity
  EpochInterval
cppEMax
    Integer
ppNopt <- Integer -> SpecTransM ctx (SpecRep Integer)
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep (Word16 -> Integer
forall a. Integral a => a -> Integer
toInteger (Word16 -> Integer) -> Word16 -> Integer
forall a b. (a -> b) -> a -> b
$ THKD ('PPGroups 'TechnicalGroup 'NoStakePoolGroup) Identity Word16
-> HKD Identity Word16
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 :: (Integer, Integer)
ppPv = (Integer
0, Integer
0)
      ppMinUTxOValue :: Integer
ppMinUTxOValue = Integer
0 -- minUTxOValue has been deprecated and is not supported in Conway
    Integer
ppCoinsPerUTxOByte <- THKD ('PPGroups 'EconomicGroup 'SecurityGroup) Identity CoinPerByte
-> SpecTransM
     ctx
     (SpecRep
        (THKD
           ('PPGroups 'EconomicGroup 'SecurityGroup) Identity CoinPerByte))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep THKD ('PPGroups 'EconomicGroup 'SecurityGroup) Identity CoinPerByte
cppCoinsPerUTxOByte
    ()
ppCostmdls <- THKD
  ('PPGroups 'TechnicalGroup 'NoStakePoolGroup) Identity CostModels
-> SpecTransM
     ctx
     (SpecRep
        (THKD
           ('PPGroups 'TechnicalGroup 'NoStakePoolGroup) Identity CostModels))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep THKD
  ('PPGroups 'TechnicalGroup 'NoStakePoolGroup) Identity CostModels
cppCostModels
    ()
ppPrices <- THKD ('PPGroups 'EconomicGroup 'NoStakePoolGroup) Identity Prices
-> SpecTransM
     ctx
     (SpecRep
        (THKD
           ('PPGroups 'EconomicGroup 'NoStakePoolGroup) Identity Prices))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep THKD ('PPGroups 'EconomicGroup 'NoStakePoolGroup) Identity Prices
cppPrices
    let
      ppMaxRefScriptSizePerTx :: Integer
ppMaxRefScriptSizePerTx = Int -> Integer
forall a. Integral a => a -> Integer
toInteger Int
maxRefScriptSizePerTx
      ppMaxRefScriptSizePerBlock :: Integer
ppMaxRefScriptSizePerBlock = Int -> Integer
forall a. Integral a => a -> Integer
toInteger Int
maxRefScriptSizePerBlock
      ppRefScriptCostStride :: Integer
ppRefScriptCostStride = Int -> Integer
forall a. Integral a => a -> Integer
toInteger Int
refScriptCostStride
      ppRefScriptCostMultiplier :: Rational
ppRefScriptCostMultiplier = Rational
refScriptCostMultiplier
    (Integer, Integer)
ppMaxTxExUnits <- THKD
  ('PPGroups 'NetworkGroup 'NoStakePoolGroup) Identity OrdExUnits
-> SpecTransM
     ctx
     (SpecRep
        (THKD
           ('PPGroups 'NetworkGroup 'NoStakePoolGroup) Identity OrdExUnits))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep THKD
  ('PPGroups 'NetworkGroup 'NoStakePoolGroup) Identity OrdExUnits
cppMaxTxExUnits
    (Integer, Integer)
ppMaxBlockExUnits <- THKD ('PPGroups 'NetworkGroup 'SecurityGroup) Identity OrdExUnits
-> SpecTransM
     ctx
     (SpecRep
        (THKD
           ('PPGroups 'NetworkGroup 'SecurityGroup) Identity OrdExUnits))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep THKD ('PPGroups 'NetworkGroup 'SecurityGroup) Identity OrdExUnits
cppMaxBlockExUnits
    let
      ppMaxValSize :: Integer
ppMaxValSize = Word32 -> Integer
forall a. Integral a => a -> Integer
toInteger (Word32 -> Integer)
-> (THKD ('PPGroups 'NetworkGroup 'SecurityGroup) Identity Word32
    -> Word32)
-> THKD ('PPGroups 'NetworkGroup 'SecurityGroup) Identity Word32
-> Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. THKD ('PPGroups 'NetworkGroup 'SecurityGroup) Identity Word32
-> Word32
THKD ('PPGroups 'NetworkGroup 'SecurityGroup) Identity Word32
-> HKD Identity Word32
forall (t :: PPGroups) (f :: * -> *) a. THKD t f a -> HKD f a
unTHKD (THKD ('PPGroups 'NetworkGroup 'SecurityGroup) Identity Word32
 -> Integer)
-> THKD ('PPGroups 'NetworkGroup 'SecurityGroup) Identity Word32
-> Integer
forall a b. (a -> b) -> a -> b
$ THKD ('PPGroups 'NetworkGroup 'SecurityGroup) Identity Word32
cppMaxValSize
      ppMaxCollateralInputs :: Integer
ppMaxCollateralInputs = Word16 -> Integer
forall a. Integral a => a -> Integer
toInteger (Word16 -> Integer)
-> (THKD
      ('PPGroups 'NetworkGroup 'NoStakePoolGroup) Identity Word16
    -> Word16)
-> THKD ('PPGroups 'NetworkGroup 'NoStakePoolGroup) Identity Word16
-> Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. THKD ('PPGroups 'NetworkGroup 'NoStakePoolGroup) Identity Word16
-> Word16
THKD ('PPGroups 'NetworkGroup 'NoStakePoolGroup) Identity Word16
-> HKD Identity Word16
forall (t :: PPGroups) (f :: * -> *) a. THKD t f a -> HKD f a
unTHKD (THKD ('PPGroups 'NetworkGroup 'NoStakePoolGroup) Identity Word16
 -> Integer)
-> THKD ('PPGroups 'NetworkGroup 'NoStakePoolGroup) Identity Word16
-> Integer
forall a b. (a -> b) -> a -> b
$ THKD ('PPGroups 'NetworkGroup 'NoStakePoolGroup) Identity Word16
cppMaxCollateralInputs
    PoolThresholds
ppPoolThresholds <- THKD
  ('PPGroups 'GovGroup 'NoStakePoolGroup)
  Identity
  PoolVotingThresholds
-> SpecTransM
     ctx
     (SpecRep
        (THKD
           ('PPGroups 'GovGroup 'NoStakePoolGroup)
           Identity
           PoolVotingThresholds))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep THKD
  ('PPGroups 'GovGroup 'NoStakePoolGroup)
  Identity
  PoolVotingThresholds
cppPoolVotingThresholds
    DrepThresholds
ppDrepThresholds <- THKD
  ('PPGroups 'GovGroup 'NoStakePoolGroup)
  Identity
  DRepVotingThresholds
-> SpecTransM
     ctx
     (SpecRep
        (THKD
           ('PPGroups 'GovGroup 'NoStakePoolGroup)
           Identity
           DRepVotingThresholds))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep THKD
  ('PPGroups 'GovGroup 'NoStakePoolGroup)
  Identity
  DRepVotingThresholds
cppDRepVotingThresholds
    let
      ppCcMinSize :: Integer
ppCcMinSize = Word16 -> Integer
forall a. Integral a => a -> Integer
toInteger (Word16 -> Integer)
-> (THKD ('PPGroups 'GovGroup 'NoStakePoolGroup) Identity Word16
    -> Word16)
-> THKD ('PPGroups 'GovGroup 'NoStakePoolGroup) Identity Word16
-> Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. THKD ('PPGroups 'GovGroup 'NoStakePoolGroup) Identity Word16
-> Word16
THKD ('PPGroups 'GovGroup 'NoStakePoolGroup) Identity Word16
-> HKD Identity Word16
forall (t :: PPGroups) (f :: * -> *) a. THKD t f a -> HKD f a
unTHKD (THKD ('PPGroups 'GovGroup 'NoStakePoolGroup) Identity Word16
 -> Integer)
-> THKD ('PPGroups 'GovGroup 'NoStakePoolGroup) Identity Word16
-> Integer
forall a b. (a -> b) -> a -> b
$ THKD ('PPGroups 'GovGroup 'NoStakePoolGroup) Identity Word16
cppCommitteeMinSize
      ppCcMaxTermLength :: Integer
ppCcMaxTermLength = Word32 -> Integer
forall a. Integral a => a -> Integer
toInteger (Word32 -> Integer)
-> (THKD
      ('PPGroups 'GovGroup 'NoStakePoolGroup) Identity EpochInterval
    -> Word32)
-> THKD
     ('PPGroups 'GovGroup 'NoStakePoolGroup) Identity EpochInterval
-> Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. EpochInterval -> Word32
unEpochInterval (EpochInterval -> Word32)
-> (THKD
      ('PPGroups 'GovGroup 'NoStakePoolGroup) Identity EpochInterval
    -> EpochInterval)
-> THKD
     ('PPGroups 'GovGroup 'NoStakePoolGroup) Identity EpochInterval
-> Word32
forall b c a. (b -> c) -> (a -> b) -> a -> c
. THKD ('PPGroups 'GovGroup 'NoStakePoolGroup) Identity EpochInterval
-> EpochInterval
THKD ('PPGroups 'GovGroup 'NoStakePoolGroup) Identity EpochInterval
-> HKD Identity EpochInterval
forall (t :: PPGroups) (f :: * -> *) a. THKD t f a -> HKD f a
unTHKD (THKD
   ('PPGroups 'GovGroup 'NoStakePoolGroup) Identity EpochInterval
 -> Integer)
-> THKD
     ('PPGroups 'GovGroup 'NoStakePoolGroup) Identity EpochInterval
-> Integer
forall a b. (a -> b) -> a -> b
$ THKD ('PPGroups 'GovGroup 'NoStakePoolGroup) Identity EpochInterval
cppCommitteeMaxTermLength
    Integer
ppGovActionLifetime <- THKD ('PPGroups 'GovGroup 'NoStakePoolGroup) Identity EpochInterval
-> SpecTransM
     ctx
     (SpecRep
        (THKD
           ('PPGroups 'GovGroup 'NoStakePoolGroup) Identity EpochInterval))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep THKD ('PPGroups 'GovGroup 'NoStakePoolGroup) Identity EpochInterval
cppGovActionLifetime
    Integer
ppGovActionDeposit <- THKD ('PPGroups 'GovGroup 'SecurityGroup) Identity Coin
-> SpecTransM
     ctx
     (SpecRep (THKD ('PPGroups 'GovGroup 'SecurityGroup) Identity Coin))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep THKD ('PPGroups 'GovGroup 'SecurityGroup) Identity Coin
cppGovActionDeposit
    Integer
ppDrepDeposit <- THKD ('PPGroups 'GovGroup 'NoStakePoolGroup) Identity Coin
-> SpecTransM
     ctx
     (SpecRep
        (THKD ('PPGroups 'GovGroup 'NoStakePoolGroup) Identity Coin))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep THKD ('PPGroups 'GovGroup 'NoStakePoolGroup) Identity Coin
cppDRepDeposit
    Integer
ppDrepActivity <- THKD ('PPGroups 'GovGroup 'NoStakePoolGroup) Identity EpochInterval
-> SpecTransM
     ctx
     (SpecRep
        (THKD
           ('PPGroups 'GovGroup 'NoStakePoolGroup) Identity EpochInterval))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep THKD ('PPGroups 'GovGroup 'NoStakePoolGroup) Identity EpochInterval
cppDRepActivity
    Rational
ppMonetaryExpansion <- THKD
  ('PPGroups 'EconomicGroup 'NoStakePoolGroup) Identity UnitInterval
-> SpecTransM
     ctx
     (SpecRep
        (THKD
           ('PPGroups 'EconomicGroup 'NoStakePoolGroup)
           Identity
           UnitInterval))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep THKD
  ('PPGroups 'EconomicGroup 'NoStakePoolGroup) Identity UnitInterval
cppRho
    Rational
ppTreasuryCut <- THKD
  ('PPGroups 'EconomicGroup 'NoStakePoolGroup) Identity UnitInterval
-> SpecTransM
     ctx
     (SpecRep
        (THKD
           ('PPGroups 'EconomicGroup 'NoStakePoolGroup)
           Identity
           UnitInterval))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep THKD
  ('PPGroups 'EconomicGroup 'NoStakePoolGroup) Identity UnitInterval
cppTau

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

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) = PParamsHKD Identity era
-> SpecTransM ctx (SpecRep (PParamsHKD Identity era))
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 = ([SpecRep a] -> HSSet (SpecRep a))
-> SpecTransM ctx [SpecRep a] -> SpecTransM ctx (HSSet (SpecRep a))
forall a b. (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [SpecRep a] -> HSSet (SpecRep a)
forall a. [a] -> HSSet a
Agda.MkHSSet (SpecTransM ctx [SpecRep a] -> SpecTransM ctx (HSSet (SpecRep a)))
-> (Set a -> SpecTransM ctx [SpecRep a])
-> Set a
-> SpecTransM ctx (HSSet (SpecRep a))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> SpecTransM ctx (SpecRep a))
-> [a] -> SpecTransM ctx [SpecRep a]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse a -> SpecTransM ctx (SpecRep a)
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep ([a] -> SpecTransM ctx [SpecRep a])
-> (Set a -> [a]) -> Set a -> SpecTransM ctx [SpecRep a]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set a -> [a]
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 = (a -> SpecTransM ctx (SpecRep a))
-> [a] -> SpecTransM ctx [SpecRep a]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse a -> SpecTransM ctx (SpecRep a)
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep ([a] -> SpecTransM ctx [SpecRep a])
-> (StrictSeq a -> [a])
-> StrictSeq a
-> SpecTransM ctx [SpecRep a]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. StrictSeq a -> [a]
forall a. StrictSeq a -> [a]
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 = (a -> SpecTransM ctx (SpecRep a))
-> [a] -> SpecTransM ctx [SpecRep a]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse a -> SpecTransM ctx (SpecRep a)
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep ([a] -> SpecTransM ctx [SpecRep a])
-> (Seq a -> [a]) -> Seq a -> SpecTransM ctx [SpecRep a]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Seq a -> [a]
forall a. Seq a -> [a]
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
_) = a -> SpecTransM ctx (SpecRep a)
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) = (StrictMaybe SlotNo, StrictMaybe SlotNo)
-> SpecTransM
     ctx (SpecRep (StrictMaybe SlotNo, StrictMaybe SlotNo))
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) = Hash ADDRHASH (VerKeyDSIGN DSIGN)
-> SpecTransM ctx (SpecRep (Hash ADDRHASH (VerKeyDSIGN DSIGN)))
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 = Nat -> Integer
forall a. Integral a => a -> Integer
toInteger (Nat -> Integer) -> (VKey kd -> Nat) -> VKey kd -> Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ByteString -> Nat
bytesToNatural (ByteString -> Nat) -> (VKey kd -> ByteString) -> VKey kd -> Nat
forall b c a. (b -> c) -> (a -> b) -> a -> c
. VerKeyDSIGN DSIGN -> ByteString
forall v. DSIGNAlgorithm v => VerKeyDSIGN v -> ByteString
rawSerialiseVerKeyDSIGN (VerKeyDSIGN DSIGN -> ByteString)
-> (VKey kd -> VerKeyDSIGN DSIGN) -> VKey kd -> ByteString
forall b c a. (b -> c) -> (a -> b) -> a -> c
. VKey kd -> VerKeyDSIGN DSIGN
forall (kd :: KeyRole). VKey kd -> VerKeyDSIGN DSIGN
unVKey

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

signatureToInteger :: DSIGNAlgorithm v => SigDSIGN v -> Integer
signatureToInteger :: forall v. DSIGNAlgorithm v => SigDSIGN v -> Integer
signatureToInteger = Nat -> Integer
forall a. Integral a => a -> Integer
toInteger (Nat -> Integer) -> (SigDSIGN v -> Nat) -> SigDSIGN v -> Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ByteString -> Nat
bytesToNatural (ByteString -> Nat)
-> (SigDSIGN v -> ByteString) -> SigDSIGN v -> Nat
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SigDSIGN v -> ByteString
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 = ByteString -> Maybe (SigDSIGN v)
forall v. DSIGNAlgorithm v => ByteString -> Maybe (SigDSIGN v)
rawDeserialiseSigDSIGN (ByteString -> Maybe (SigDSIGN v))
-> (Integer -> ByteString) -> Integer -> Maybe (SigDSIGN v)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Nat -> ByteString
naturalToBytes Int
64 (Nat -> ByteString) -> (Integer -> Nat) -> Integer -> ByteString
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> Nat
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 = VKey k -> Integer
forall (kd :: KeyRole). VKey kd -> Integer
vkeyToInteger VKey k
x
    Integer
hvkStoredHash <- Hash ADDRHASH (VerKeyDSIGN DSIGN)
-> SpecTransM ctx (SpecRep (Hash ADDRHASH (VerKeyDSIGN DSIGN)))
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 (VerKeyDSIGN DSIGN -> Hash ADDRHASH (VerKeyDSIGN DSIGN))
-> VerKeyDSIGN DSIGN -> Hash ADDRHASH (VerKeyDSIGN DSIGN)
forall a b. (a -> b) -> a -> b
$ VKey k -> VerKeyDSIGN DSIGN
forall (kd :: KeyRole). VKey kd -> VerKeyDSIGN DSIGN
unVKey VKey k
x)
    HSVKey -> SpecTransM ctx HSVKey
forall a. a -> SpecTransM ctx a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Agda.MkHSVKey {Integer
hvkVKey :: Integer
hvkStoredHash :: Integer
hvkVKey :: Integer
hvkStoredHash :: 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) = Integer -> SpecTransM ctx Integer
forall a. a -> SpecTransM ctx a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Integer -> SpecTransM ctx Integer)
-> Integer -> SpecTransM ctx Integer
forall a b. (a -> b) -> a -> b
$ SigDSIGN v -> Integer
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) = (VKey k, SignedDSIGN DSIGN (Hash HASH EraIndependentTxBody))
-> SpecTransM
     ctx
     (SpecRep
        (VKey k, SignedDSIGN DSIGN (Hash HASH EraIndependentTxBody)))
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) = Map DataHash (Data era)
-> SpecTransM ctx (SpecRep (Map DataHash (Data era)))
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 = ([(SpecRep k, SpecRep v)] -> HSMap (SpecRep k) (SpecRep v))
-> SpecTransM ctx [(SpecRep k, SpecRep v)]
-> SpecTransM ctx (HSMap (SpecRep k) (SpecRep v))
forall a b. (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [(SpecRep k, SpecRep v)] -> HSMap (SpecRep k) (SpecRep v)
forall k v. [(k, v)] -> HSMap k v
Agda.MkHSMap (SpecTransM ctx [(SpecRep k, SpecRep v)]
 -> SpecTransM ctx (HSMap (SpecRep k) (SpecRep v)))
-> (Map k v -> SpecTransM ctx [(SpecRep k, SpecRep v)])
-> Map k v
-> SpecTransM ctx (HSMap (SpecRep k) (SpecRep v))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((k, v) -> SpecTransM ctx (SpecRep k, SpecRep v))
-> [(k, v)] -> SpecTransM ctx [(SpecRep k, SpecRep v)]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse ((k -> SpecTransM ctx (SpecRep k))
-> (v -> SpecTransM ctx (SpecRep v))
-> (k, v)
-> SpecTransM ctx (SpecRep k, SpecRep v)
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 k -> SpecTransM ctx (SpecRep k)
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep v -> SpecTransM ctx (SpecRep v)
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep) ([(k, v)] -> SpecTransM ctx [(SpecRep k, SpecRep v)])
-> (Map k v -> [(k, v)])
-> Map k v
-> SpecTransM ctx [(SpecRep k, SpecRep v)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Map k v -> [(k, v)]
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 = Integer -> SpecTransM ctx Integer
forall a. a -> SpecTransM ctx a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Integer -> SpecTransM ctx Integer)
-> (Word64 -> Integer) -> Word64 -> SpecTransM ctx Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Word64 -> Integer
forall a. Integral a => a -> Integer
toInteger

instance SpecTranslate ctx Word32 where
  type SpecRep Word32 = Integer

  toSpecRep :: Word32 -> SpecTransM ctx (SpecRep Word32)
toSpecRep = Integer -> SpecTransM ctx Integer
forall a. a -> SpecTransM ctx a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Integer -> SpecTransM ctx Integer)
-> (Word32 -> Integer) -> Word32 -> SpecTransM ctx Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Word32 -> Integer
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) -> (Tag, Integer) -> SpecTransM ctx (Tag, Integer)
forall a. a -> SpecTransM ctx a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Tag
Agda.Spend, Word32 -> Integer
forall a. Integral a => a -> Integer
toInteger Word32
i)
    AlonzoMinting (AsIx Word32
i) -> (Tag, Integer) -> SpecTransM ctx (Tag, Integer)
forall a. a -> SpecTransM ctx a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Tag
Agda.Mint, Word32 -> Integer
forall a. Integral a => a -> Integer
toInteger Word32
i)
    AlonzoCertifying (AsIx Word32
i) -> (Tag, Integer) -> SpecTransM ctx (Tag, Integer)
forall a. a -> SpecTransM ctx a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Tag
Agda.Cert, Word32 -> Integer
forall a. Integral a => a -> Integer
toInteger Word32
i)
    AlonzoRewarding (AsIx Word32
i) -> (Tag, Integer) -> SpecTransM ctx (Tag, Integer)
forall a. a -> SpecTransM ctx a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Tag
Agda.Rewrd, Word32 -> Integer
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) -> (Tag, Integer) -> SpecTransM ctx (Tag, Integer)
forall a. a -> SpecTransM ctx a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Tag
Agda.Spend, Word32 -> Integer
forall a. Integral a => a -> Integer
toInteger Word32
i)
    ConwayMinting (AsIx Word32
i) -> (Tag, Integer) -> SpecTransM ctx (Tag, Integer)
forall a. a -> SpecTransM ctx a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Tag
Agda.Mint, Word32 -> Integer
forall a. Integral a => a -> Integer
toInteger Word32
i)
    ConwayCertifying (AsIx Word32
i) -> (Tag, Integer) -> SpecTransM ctx (Tag, Integer)
forall a. a -> SpecTransM ctx a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Tag
Agda.Cert, Word32 -> Integer
forall a. Integral a => a -> Integer
toInteger Word32
i)
    ConwayRewarding (AsIx Word32
i) -> (Tag, Integer) -> SpecTransM ctx (Tag, Integer)
forall a. a -> SpecTransM ctx a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Tag
Agda.Rewrd, Word32 -> Integer
forall a. Integral a => a -> Integer
toInteger Word32
i)
    ConwayVoting (AsIx Word32
i) -> (Tag, Integer) -> SpecTransM ctx (Tag, Integer)
forall a. a -> SpecTransM ctx a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Tag
Agda.Vote, Word32 -> Integer
forall a. Integral a => a -> Integer
toInteger Word32
i)
    ConwayProposing (AsIx Word32
i) -> (Tag, Integer) -> SpecTransM ctx (Tag, Integer)
forall a. a -> SpecTransM ctx a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Tag
Agda.Propose, Word32 -> Integer
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) = (,) (SpecRep a -> SpecRep b -> (SpecRep a, SpecRep b))
-> SpecTransM ctx (SpecRep a)
-> SpecTransM ctx (SpecRep b -> (SpecRep a, SpecRep b))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> SpecTransM ctx (SpecRep a)
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep a
x SpecTransM ctx (SpecRep b -> (SpecRep a, SpecRep b))
-> SpecTransM ctx (SpecRep b)
-> SpecTransM ctx (SpecRep a, SpecRep b)
forall a b.
SpecTransM ctx (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> b -> SpecTransM ctx (SpecRep 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 = DataHash -> SpecTransM ctx Integer
DataHash -> SpecTransM ctx (SpecRep DataHash)
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep (DataHash -> SpecTransM ctx Integer)
-> (Data era -> DataHash) -> Data era -> SpecTransM ctx Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Data era -> DataHash
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) = Map (PlutusPurpose AsIx era) (Data era, ExUnits)
-> SpecTransM
     ctx (SpecRep (Map (PlutusPurpose AsIx era) (Data era, ExUnits)))
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 (Tag, Integer) (Integer, (Integer, Integer))
-> TxWitnesses
Agda.MkTxWitnesses
      (HSMap HSVKey Integer
 -> HSSet (Either HSTimelock HSPlutusScript)
 -> HSMap Integer Integer
 -> HSMap (Tag, Integer) (Integer, (Integer, Integer))
 -> TxWitnesses)
-> SpecTransM ctx (HSMap HSVKey Integer)
-> SpecTransM
     ctx
     (HSSet (Either HSTimelock HSPlutusScript)
      -> HSMap Integer Integer
      -> HSMap (Tag, Integer) (Integer, (Integer, Integer))
      -> TxWitnesses)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ([(HSVKey, Integer)] -> HSMap HSVKey Integer)
-> SpecTransM ctx [(HSVKey, Integer)]
-> SpecTransM ctx (HSMap HSVKey Integer)
forall a b. (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [(HSVKey, Integer)] -> HSMap HSVKey Integer
forall k v. [(k, v)] -> HSMap k v
Agda.MkHSMap ([WitVKey 'Witness] -> SpecTransM ctx (SpecRep [WitVKey 'Witness])
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep [WitVKey 'Witness]
txWitsMap)
      SpecTransM
  ctx
  (HSSet (Either HSTimelock HSPlutusScript)
   -> HSMap Integer Integer
   -> HSMap (Tag, Integer) (Integer, (Integer, Integer))
   -> TxWitnesses)
-> SpecTransM ctx (HSSet (Either HSTimelock HSPlutusScript))
-> SpecTransM
     ctx
     (HSMap Integer Integer
      -> HSMap (Tag, Integer) (Integer, (Integer, Integer))
      -> TxWitnesses)
forall a b.
SpecTransM ctx (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ([Either HSTimelock HSPlutusScript]
 -> HSSet (Either HSTimelock HSPlutusScript))
-> SpecTransM ctx [Either HSTimelock HSPlutusScript]
-> SpecTransM ctx (HSSet (Either HSTimelock HSPlutusScript))
forall a b. (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [Either HSTimelock HSPlutusScript]
-> HSSet (Either HSTimelock HSPlutusScript)
forall a. [a] -> HSSet a
Agda.MkHSSet ([AlonzoScript era] -> SpecTransM ctx (SpecRep [AlonzoScript era])
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep (Map ScriptHash (AlonzoScript era) -> [AlonzoScript era]
forall k a. Map k a -> [a]
Map.elems (Map ScriptHash (AlonzoScript era) -> [AlonzoScript era])
-> Map ScriptHash (AlonzoScript era) -> [AlonzoScript era]
forall a b. (a -> b) -> a -> b
$ AlonzoTxWits era -> Map ScriptHash (Script era)
forall era.
AlonzoEraScript era =>
AlonzoTxWits era -> Map ScriptHash (Script era)
txscripts AlonzoTxWits era
x))
      SpecTransM
  ctx
  (HSMap Integer Integer
   -> HSMap (Tag, Integer) (Integer, (Integer, Integer))
   -> TxWitnesses)
-> SpecTransM ctx (HSMap Integer Integer)
-> SpecTransM
     ctx
     (HSMap (Tag, Integer) (Integer, (Integer, Integer)) -> TxWitnesses)
forall a b.
SpecTransM ctx (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> TxDats era -> SpecTransM ctx (SpecRep (TxDats era))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep (AlonzoTxWits era -> TxDats era
forall era. AlonzoEraScript era => AlonzoTxWits era -> TxDats era
txdats AlonzoTxWits era
x)
      SpecTransM
  ctx
  (HSMap (Tag, Integer) (Integer, (Integer, Integer)) -> TxWitnesses)
-> SpecTransM
     ctx (HSMap (Tag, Integer) (Integer, (Integer, Integer)))
-> SpecTransM ctx TxWitnesses
forall a b.
SpecTransM ctx (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Redeemers era -> SpecTransM ctx (SpecRep (Redeemers era))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep (AlonzoTxWits era -> Redeemers era
forall era.
AlonzoEraScript era =>
AlonzoTxWits era -> Redeemers era
txrdmrs AlonzoTxWits era
x)
    where
      txWitsMap :: [WitVKey 'Witness]
txWitsMap = Set (WitVKey 'Witness) -> [WitVKey 'Witness]
forall a. Set a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList (AlonzoTxWits era -> Set (WitVKey 'Witness)
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 = Maybe a -> SpecTransM ctx (Maybe (SpecRep a))
Maybe a -> SpecTransM ctx (SpecRep (Maybe a))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep (Maybe a -> SpecTransM ctx (Maybe (SpecRep a)))
-> (StrictMaybe a -> Maybe a)
-> StrictMaybe a
-> SpecTransM ctx (Maybe (SpecRep a))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. StrictMaybe a -> Maybe a
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 = (a -> SpecTransM ctx (SpecRep a))
-> Maybe a -> SpecTransM ctx (Maybe (SpecRep a))
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Maybe a -> f (Maybe b)
traverse a -> SpecTransM ctx (SpecRep a)
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 = SafeHash EraIndependentTxAuxData -> SpecTransM ctx Integer
SafeHash EraIndependentTxAuxData
-> SpecTransM ctx (SpecRep (SafeHash EraIndependentTxAuxData))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep (SafeHash EraIndependentTxAuxData -> SpecTransM ctx Integer)
-> (AlonzoTxAuxData era -> SafeHash EraIndependentTxAuxData)
-> AlonzoTxAuxData era
-> SpecTransM ctx Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AlonzoTxAuxData era -> SafeHash EraIndependentTxAuxData
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) = Hash ADDRHASH EraIndependentScript
-> SpecTransM ctx (SpecRep (Hash ADDRHASH EraIndependentScript))
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 (Integer -> Credential)
-> SpecTransM ctx Integer -> SpecTransM ctx Credential
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> KeyHash k -> SpecTransM ctx (SpecRep (KeyHash k))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep KeyHash k
h
  toSpecRep (ScriptHashObj ScriptHash
h) = Integer -> Credential
Agda.ScriptObj (Integer -> Credential)
-> SpecTransM ctx Integer -> SpecTransM ctx Credential
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ScriptHash -> SpecTransM ctx (SpecRep ScriptHash)
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 = Integer -> SpecTransM ctx Integer
forall a. a -> SpecTransM ctx a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Integer -> SpecTransM ctx Integer)
-> (Network -> Integer) -> Network -> SpecTransM ctx Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Int -> Integer) -> (Network -> Int) -> Network -> Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Network -> Int
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 StakeCredential
c) = Integer -> Credential -> RwdAddr
Agda.RwdAddr (Integer -> Credential -> RwdAddr)
-> SpecTransM ctx Integer -> SpecTransM ctx (Credential -> RwdAddr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Network -> SpecTransM ctx (SpecRep Network)
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep Network
n SpecTransM ctx (Credential -> RwdAddr)
-> SpecTransM ctx Credential -> SpecTransM ctx RwdAddr
forall a b.
SpecTransM ctx (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> StakeCredential -> SpecTransM ctx (SpecRep StakeCredential)
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep StakeCredential
c

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

  toSpecRep :: PoolParams -> SpecTransM ctx (SpecRep PoolParams)
toSpecRep PoolParams {Set (KeyHash 'Staking)
StrictMaybe PoolMetadata
KeyHash 'StakePool
VRFVerKeyHash 'StakePoolVRF
RewardAccount
Coin
StrictSeq StakePoolRelay
UnitInterval
ppId :: KeyHash 'StakePool
ppVrf :: VRFVerKeyHash 'StakePoolVRF
ppPledge :: Coin
ppCost :: Coin
ppMargin :: UnitInterval
ppRewardAccount :: RewardAccount
ppOwners :: Set (KeyHash 'Staking)
ppRelays :: StrictSeq StakePoolRelay
ppMetadata :: StrictMaybe PoolMetadata
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
..} =
    HSSet Integer
-> Integer -> Rational -> Integer -> Credential -> PoolParams
Agda.PoolParams
      (HSSet Integer
 -> Integer -> Rational -> Integer -> Credential -> PoolParams)
-> SpecTransM ctx (HSSet Integer)
-> SpecTransM
     ctx (Integer -> Rational -> Integer -> Credential -> PoolParams)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Set (KeyHash 'Staking)
-> SpecTransM ctx (SpecRep (Set (KeyHash 'Staking)))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep Set (KeyHash 'Staking)
ppOwners
      SpecTransM
  ctx (Integer -> Rational -> Integer -> Credential -> PoolParams)
-> SpecTransM ctx Integer
-> SpecTransM ctx (Rational -> Integer -> Credential -> PoolParams)
forall a b.
SpecTransM ctx (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Coin -> SpecTransM ctx (SpecRep Coin)
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep Coin
ppCost
      SpecTransM ctx (Rational -> Integer -> Credential -> PoolParams)
-> SpecTransM ctx Rational
-> SpecTransM ctx (Integer -> Credential -> PoolParams)
forall a b.
SpecTransM ctx (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> UnitInterval -> SpecTransM ctx (SpecRep UnitInterval)
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep UnitInterval
ppMargin
      SpecTransM ctx (Integer -> Credential -> PoolParams)
-> SpecTransM ctx Integer
-> SpecTransM ctx (Credential -> PoolParams)
forall a b.
SpecTransM ctx (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Coin -> SpecTransM ctx (SpecRep Coin)
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep Coin
ppPledge
      SpecTransM ctx (Credential -> PoolParams)
-> SpecTransM ctx Credential -> SpecTransM ctx PoolParams
forall a b.
SpecTransM ctx (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> StakeCredential -> SpecTransM ctx (SpecRep StakeCredential)
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep (RewardAccount -> StakeCredential
raCredential RewardAccount
ppRewardAccount)

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 (Credential -> VDeleg)
-> SpecTransM ctx Credential -> SpecTransM ctx VDeleg
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Credential 'DRepRole
-> SpecTransM ctx (SpecRep (Credential 'DRepRole))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep Credential 'DRepRole
c
  toSpecRep DRep
DRepAlwaysAbstain = VDeleg -> SpecTransM ctx VDeleg
forall a. a -> SpecTransM ctx a
forall (f :: * -> *) a. Applicative f => a -> f a
pure VDeleg
Agda.AbstainRep
  toSpecRep DRep
DRepAlwaysNoConfidence = VDeleg -> SpecTransM ctx VDeleg
forall a. a -> SpecTransM ctx a
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 = Text -> SpecTransM ctx Text
forall a. a -> SpecTransM ctx a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Text -> SpecTransM ctx Text)
-> (Url -> Text) -> Url -> SpecTransM ctx Text
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 (Text -> Integer -> Anchor)
-> SpecTransM ctx Text -> SpecTransM ctx (Integer -> Anchor)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Url -> SpecTransM ctx (SpecRep Url)
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep Url
url SpecTransM ctx (Integer -> Anchor)
-> SpecTransM ctx Integer -> SpecTransM ctx Anchor
forall a b.
SpecTransM ctx (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> SafeHash AnchorData
-> SpecTransM ctx (SpecRep (SafeHash AnchorData))
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) = SafeHash EraIndependentTxBody
-> SpecTransM ctx (SpecRep (SafeHash EraIndependentTxBody))
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) = Map RewardAccount Coin
-> SpecTransM ctx (SpecRep (Map RewardAccount Coin))
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) = SafeHash EraIndependentTxAuxData
-> SpecTransM ctx (SpecRep (SafeHash EraIndependentTxAuxData))
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) = Bool -> SpecTransM ctx Bool
forall a. a -> SpecTransM ctx a
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
      (TxBody -> TxWitnesses -> Bool -> Maybe Integer -> Tx)
-> SpecTransM ctx TxBody
-> SpecTransM ctx (TxWitnesses -> Bool -> Maybe Integer -> Tx)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ConwayTxBodyTransContext
-> SpecTransM ConwayTxBodyTransContext TxBody
-> SpecTransM ctx TxBody
forall ctx a ctx'. ctx -> SpecTransM ctx a -> SpecTransM ctx' a
withCtx
        (Integer -> TxId -> ConwayTxBodyTransContext
ConwayTxBodyTransContext (AlonzoTx era
tx AlonzoTx era -> Getting Integer (AlonzoTx era) Integer -> Integer
forall s a. s -> Getting a s a -> a
^. Getting Integer (Tx era) Integer
Getting Integer (AlonzoTx era) Integer
forall era. EraTx era => SimpleGetter (Tx era) Integer
SimpleGetter (Tx era) Integer
sizeTxF) (Tx era -> TxId
forall era. EraTx era => Tx era -> TxId
txIdTx Tx era
AlonzoTx era
tx))
        (TxBody era
-> SpecTransM ConwayTxBodyTransContext (SpecRep (TxBody era))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep (AlonzoTx era -> TxBody era
forall era. AlonzoTx era -> TxBody era
body AlonzoTx era
tx))
      SpecTransM ctx (TxWitnesses -> Bool -> Maybe Integer -> Tx)
-> SpecTransM ctx TxWitnesses
-> SpecTransM ctx (Bool -> Maybe Integer -> Tx)
forall a b.
SpecTransM ctx (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> TxWits era -> SpecTransM ctx (SpecRep (TxWits era))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep (AlonzoTx era -> TxWits era
forall era. AlonzoTx era -> TxWits era
wits AlonzoTx era
tx)
      SpecTransM ctx (Bool -> Maybe Integer -> Tx)
-> SpecTransM ctx Bool -> SpecTransM ctx (Maybe Integer -> Tx)
forall a b.
SpecTransM ctx (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> IsValid -> SpecTransM ctx (SpecRep IsValid)
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep (AlonzoTx era -> IsValid
forall era. AlonzoTx era -> IsValid
isValid AlonzoTx era
tx)
      SpecTransM ctx (Maybe Integer -> Tx)
-> SpecTransM ctx (Maybe Integer) -> SpecTransM ctx Tx
forall a b.
SpecTransM ctx (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> StrictMaybe (TxAuxData era)
-> SpecTransM ctx (SpecRep (StrictMaybe (TxAuxData era)))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep (AlonzoTx era -> StrictMaybe (TxAuxData era)
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 = OpaqueErrorString -> SpecTransM ctx OpaqueErrorString
forall a. a -> SpecTransM ctx a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (OpaqueErrorString -> SpecTransM ctx OpaqueErrorString)
-> (ConwayGovPredFailure era -> OpaqueErrorString)
-> ConwayGovPredFailure era
-> SpecTransM ctx OpaqueErrorString
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ConwayGovPredFailure era -> OpaqueErrorString
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) = GovActionId -> SpecTransM ctx (SpecRep GovActionId)
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 = Rational -> SpecTransM ctx Rational
forall a. a -> SpecTransM ctx a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rational -> SpecTransM ctx Rational)
-> (UnitInterval -> Rational)
-> UnitInterval
-> SpecTransM ctx Rational
forall b c a. (b -> c) -> (a -> b) -> a -> c
. UnitInterval -> Rational
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) = (Map (Credential 'ColdCommitteeRole) EpochNo, UnitInterval)
-> SpecTransM
     ctx
     (SpecRep
        (Map (Credential 'ColdCommitteeRole) EpochNo, UnitInterval))
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) = (SafeHash AnchorData, StrictMaybe ScriptHash)
-> SpecTransM
     ctx (SpecRep (SafeHash AnchorData, StrictMaybe ScriptHash))
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 StakeCredential Coin
StrictMaybe (Committee era)
PParams era
Constitution era
GovRelation StrictMaybe era
Coin
ensCommittee :: StrictMaybe (Committee era)
ensConstitution :: Constitution era
ensCurPParams :: PParams era
ensPrevPParams :: PParams era
ensTreasury :: Coin
ensWithdrawals :: Map StakeCredential Coin
ensPrevGovActionIds :: GovRelation StrictMaybe era
ensCommittee :: forall era. EnactState era -> StrictMaybe (Committee era)
ensConstitution :: forall era. EnactState era -> Constitution era
ensCurPParams :: forall era. EnactState era -> PParams era
ensPrevPParams :: forall era. EnactState era -> PParams era
ensTreasury :: forall era. EnactState era -> Coin
ensWithdrawals :: forall era. EnactState era -> Map StakeCredential Coin
ensPrevGovActionIds :: forall era. EnactState era -> GovRelation StrictMaybe era
..} =
    (Maybe (HSMap Credential Integer, Rational), (Integer, Integer))
-> ((Integer, Maybe Integer), (Integer, Integer))
-> ((Integer, Integer), (Integer, Integer))
-> (PParams, (Integer, Integer))
-> HSMap RwdAddr Integer
-> EnactState
Agda.MkEnactState
      ((Maybe (HSMap Credential Integer, Rational), (Integer, Integer))
 -> ((Integer, Maybe Integer), (Integer, Integer))
 -> ((Integer, Integer), (Integer, Integer))
 -> (PParams, (Integer, Integer))
 -> HSMap RwdAddr Integer
 -> EnactState)
-> SpecTransM
     ctx
     (Maybe (HSMap Credential Integer, Rational), (Integer, Integer))
-> SpecTransM
     ctx
     (((Integer, Maybe Integer), (Integer, Integer))
      -> ((Integer, Integer), (Integer, Integer))
      -> (PParams, (Integer, Integer))
      -> HSMap RwdAddr Integer
      -> EnactState)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StrictMaybe (Committee era)
-> StrictMaybe (GovPurposeId 'CommitteePurpose era)
-> SpecTransM
     ctx (SpecRep (StrictMaybe (Committee era)), (Integer, Integer))
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
      SpecTransM
  ctx
  (((Integer, Maybe Integer), (Integer, Integer))
   -> ((Integer, Integer), (Integer, Integer))
   -> (PParams, (Integer, Integer))
   -> HSMap RwdAddr Integer
   -> EnactState)
-> SpecTransM ctx ((Integer, Maybe Integer), (Integer, Integer))
-> SpecTransM
     ctx
     (((Integer, Integer), (Integer, Integer))
      -> (PParams, (Integer, Integer))
      -> HSMap RwdAddr Integer
      -> EnactState)
forall a b.
SpecTransM ctx (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Constitution era
-> StrictMaybe (GovPurposeId 'ConstitutionPurpose era)
-> SpecTransM ctx (SpecRep (Constitution era), (Integer, Integer))
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
      SpecTransM
  ctx
  (((Integer, Integer), (Integer, Integer))
   -> (PParams, (Integer, Integer))
   -> HSMap RwdAddr Integer
   -> EnactState)
-> SpecTransM ctx ((Integer, Integer), (Integer, Integer))
-> SpecTransM
     ctx
     ((PParams, (Integer, Integer))
      -> HSMap RwdAddr Integer -> EnactState)
forall a b.
SpecTransM ctx (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ProtVer
-> StrictMaybe (GovPurposeId 'HardForkPurpose era)
-> SpecTransM ctx (SpecRep ProtVer, (Integer, Integer))
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 PParams era -> Getting ProtVer (PParams era) ProtVer -> ProtVer
forall s a. s -> Getting a s a -> a
^. Getting ProtVer (PParams era) ProtVer
forall era. EraPParams era => Lens' (PParams era) ProtVer
Lens' (PParams era) ProtVer
ppProtocolVersionL) StrictMaybe (GovPurposeId 'HardForkPurpose era)
grHardFork
      SpecTransM
  ctx
  ((PParams, (Integer, Integer))
   -> HSMap RwdAddr Integer -> EnactState)
-> SpecTransM ctx (PParams, (Integer, Integer))
-> SpecTransM ctx (HSMap RwdAddr Integer -> EnactState)
forall a b.
SpecTransM ctx (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> PParams era
-> StrictMaybe (GovPurposeId 'PParamUpdatePurpose era)
-> SpecTransM ctx (SpecRep (PParams era), (Integer, Integer))
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
      SpecTransM ctx (HSMap RwdAddr Integer -> EnactState)
-> SpecTransM ctx (HSMap RwdAddr Integer)
-> SpecTransM ctx EnactState
forall a b.
SpecTransM ctx (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Map StakeCredential Coin -> SpecTransM ctx (HSMap RwdAddr Integer)
forall {a} {ctx}.
(SpecRep a ~ Credential, SpecTranslate ctx a) =>
Map a Coin -> SpecTransM ctx (HSMap RwdAddr Integer)
transWithdrawals Map StakeCredential Coin
ensWithdrawals
    where
      GovRelation {StrictMaybe (GovPurposeId 'PParamUpdatePurpose era)
StrictMaybe (GovPurposeId 'HardForkPurpose era)
StrictMaybe (GovPurposeId 'CommitteePurpose era)
StrictMaybe (GovPurposeId 'ConstitutionPurpose era)
grCommittee :: StrictMaybe (GovPurposeId 'CommitteePurpose era)
grConstitution :: StrictMaybe (GovPurposeId 'ConstitutionPurpose era)
grHardFork :: StrictMaybe (GovPurposeId 'HardForkPurpose era)
grPParamUpdate :: StrictMaybe (GovPurposeId 'PParamUpdatePurpose era)
grPParamUpdate :: forall (f :: * -> *) era.
GovRelation f era -> f (GovPurposeId 'PParamUpdatePurpose era)
grHardFork :: forall (f :: * -> *) era.
GovRelation f era -> f (GovPurposeId 'HardForkPurpose era)
grCommittee :: forall (f :: * -> *) era.
GovRelation f era -> f (GovPurposeId 'CommitteePurpose era)
grConstitution :: forall (f :: * -> *) era.
GovRelation f era -> f (GovPurposeId 'ConstitutionPurpose era)
..} = GovRelation StrictMaybe era
ensPrevGovActionIds
      transWithdrawals :: Map a Coin -> SpecTransM ctx (HSMap RwdAddr Integer)
transWithdrawals Map a Coin
ws = ([(RwdAddr, Integer)] -> HSMap RwdAddr Integer)
-> SpecTransM ctx [(RwdAddr, Integer)]
-> SpecTransM ctx (HSMap RwdAddr Integer)
forall a b. (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [(RwdAddr, Integer)] -> HSMap RwdAddr Integer
forall k v. [(k, v)] -> HSMap k v
Agda.MkHSMap (SpecTransM ctx [(RwdAddr, Integer)]
 -> SpecTransM ctx (HSMap RwdAddr Integer))
-> (((a, Coin) -> SpecTransM ctx (RwdAddr, Integer))
    -> SpecTransM ctx [(RwdAddr, Integer)])
-> ((a, Coin) -> SpecTransM ctx (RwdAddr, Integer))
-> SpecTransM ctx (HSMap RwdAddr Integer)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(a, Coin)]
-> ((a, Coin) -> SpecTransM ctx (RwdAddr, Integer))
-> SpecTransM ctx [(RwdAddr, Integer)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM (Map a Coin -> [(a, Coin)]
forall k a. Map k a -> [(k, a)]
Map.toList Map a Coin
ws) (((a, Coin) -> SpecTransM ctx (RwdAddr, Integer))
 -> SpecTransM ctx (HSMap RwdAddr Integer))
-> ((a, Coin) -> SpecTransM ctx (RwdAddr, Integer))
-> SpecTransM ctx (HSMap RwdAddr Integer)
forall a b. (a -> b) -> a -> b
$
        \(a
cred, Coin Integer
amount) -> do
          Credential
agdaCred <- a -> SpecTransM ctx (SpecRep a)
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep a
cred
          Integer
network <- Network -> SpecTransM ctx (SpecRep Network)
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep Network
Testnet -- TODO where should this really come from?
          (RwdAddr, Integer) -> SpecTransM ctx (RwdAddr, Integer)
forall a. a -> SpecTransM ctx a
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 <- a -> SpecTransM ctx (SpecRep a)
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 -> a -> SpecTransM ctx (SpecRep a)
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep a
lastId
          StrictMaybe a
SNothing -> (a, b) -> SpecTransM ctx (a, b)
forall a. a -> SpecTransM ctx a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (a
0, b
0)
        (SpecRep a, (a, b)) -> SpecTransM ctx (SpecRep a, (a, b))
forall a. a -> SpecTransM ctx a
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,) (Credential -> (GovRole, Credential))
-> SpecTransM ctx Credential
-> SpecTransM ctx (GovRole, Credential)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Credential 'HotCommitteeRole
-> SpecTransM ctx (SpecRep (Credential 'HotCommitteeRole))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep Credential 'HotCommitteeRole
c
  toSpecRep (DRepVoter Credential 'DRepRole
c) = (GovRole
Agda.DRep,) (Credential -> (GovRole, Credential))
-> SpecTransM ctx Credential
-> SpecTransM ctx (GovRole, Credential)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Credential 'DRepRole
-> SpecTransM ctx (SpecRep (Credential 'DRepRole))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep Credential 'DRepRole
c
  toSpecRep (StakePoolVoter KeyHash 'StakePool
kh) = (GovRole
Agda.SPO,) (Credential -> (GovRole, Credential))
-> SpecTransM ctx Credential
-> SpecTransM ctx (GovRole, Credential)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Credential 'StakePool
-> SpecTransM ctx (SpecRep (Credential 'StakePool))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep (KeyHash 'StakePool -> Credential 'StakePool
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 = Vote -> SpecTransM ctx Vote
forall a. a -> SpecTransM ctx a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Vote
Agda.Yes
  toSpecRep Vote
VoteNo = Vote -> SpecTransM ctx Vote
forall a. a -> SpecTransM ctx a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Vote
Agda.No
  toSpecRep Vote
Abstain = Vote -> SpecTransM ctx Vote
forall a. a -> SpecTransM ctx a
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 = (Voter
 -> GovActionId
 -> VotingProcedure era
 -> SpecTransM ctx [GovVote]
 -> SpecTransM ctx [GovVote])
-> SpecTransM ctx [GovVote]
-> VotingProcedures era
-> SpecTransM ctx [GovVote]
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 ([GovVote] -> SpecTransM ctx [GovVote]
forall a. a -> SpecTransM ctx a
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 =
        (:)
          (GovVote -> [GovVote] -> [GovVote])
-> SpecTransM ctx GovVote
-> SpecTransM ctx ([GovVote] -> [GovVote])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ( (Integer, Integer)
-> (GovRole, Credential) -> Vote -> Maybe Anchor -> GovVote
Agda.GovVote
                  ((Integer, Integer)
 -> (GovRole, Credential) -> Vote -> Maybe Anchor -> GovVote)
-> SpecTransM ctx (Integer, Integer)
-> SpecTransM
     ctx ((GovRole, Credential) -> Vote -> Maybe Anchor -> GovVote)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> GovActionId -> SpecTransM ctx (SpecRep GovActionId)
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep GovActionId
gaId
                  SpecTransM
  ctx ((GovRole, Credential) -> Vote -> Maybe Anchor -> GovVote)
-> SpecTransM ctx (GovRole, Credential)
-> SpecTransM ctx (Vote -> Maybe Anchor -> GovVote)
forall a b.
SpecTransM ctx (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Voter -> SpecTransM ctx (SpecRep Voter)
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep Voter
voter
                  SpecTransM ctx (Vote -> Maybe Anchor -> GovVote)
-> SpecTransM ctx Vote -> SpecTransM ctx (Maybe Anchor -> GovVote)
forall a b.
SpecTransM ctx (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Vote -> SpecTransM ctx (SpecRep Vote)
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep (VotingProcedure era -> Vote
forall era. VotingProcedure era -> Vote
vProcVote VotingProcedure era
votingProcedure)
                  SpecTransM ctx (Maybe Anchor -> GovVote)
-> SpecTransM ctx (Maybe Anchor) -> SpecTransM ctx GovVote
forall a b.
SpecTransM ctx (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> StrictMaybe Anchor -> SpecTransM ctx (SpecRep (StrictMaybe Anchor))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep (VotingProcedure era -> StrictMaybe Anchor
forall era. VotingProcedure era -> StrictMaybe Anchor
vProcAnchor VotingProcedure era
votingProcedure)
              )
          SpecTransM ctx ([GovVote] -> [GovVote])
-> SpecTransM ctx [GovVote] -> SpecTransM ctx [GovVote]
forall a b.
SpecTransM ctx (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> SpecTransM ctx [GovVote]
m

instance SpecTranslate ctx Word16 where
  type SpecRep Word16 = Integer

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

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

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

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

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) = PParamsHKD StrictMaybe era
-> SpecTransM ctx (SpecRep (PParamsHKD StrictMaybe era))
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 (PParamsUpdate -> GovAction)
-> SpecTransM ctx PParamsUpdate -> SpecTransM ctx GovAction
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> PParamsUpdate era -> SpecTransM ctx (SpecRep (PParamsUpdate era))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep PParamsUpdate era
ppu
  toSpecRep (HardForkInitiation StrictMaybe (GovPurposeId 'HardForkPurpose era)
_ ProtVer
pv) = (Integer, Integer) -> GovAction
Agda.TriggerHF ((Integer, Integer) -> GovAction)
-> SpecTransM ctx (Integer, Integer) -> SpecTransM ctx GovAction
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ProtVer -> SpecTransM ctx (SpecRep ProtVer)
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
      (HSMap RwdAddr Integer -> GovAction)
-> SpecTransM ctx (HSMap RwdAddr Integer)
-> SpecTransM ctx GovAction
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Map RewardAccount Coin
-> SpecTransM ctx (SpecRep (Map RewardAccount Coin))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep Map RewardAccount Coin
withdrawals
  toSpecRep (NoConfidence StrictMaybe (GovPurposeId 'CommitteePurpose era)
_) = GovAction -> SpecTransM ctx GovAction
forall a. a -> SpecTransM ctx a
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
      (HSMap Credential Integer
 -> HSSet Credential -> Rational -> GovAction)
-> SpecTransM ctx (HSMap Credential Integer)
-> SpecTransM ctx (HSSet Credential -> Rational -> GovAction)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Map (Credential 'ColdCommitteeRole) EpochNo
-> SpecTransM
     ctx (SpecRep (Map (Credential 'ColdCommitteeRole) EpochNo))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep Map (Credential 'ColdCommitteeRole) EpochNo
add
      SpecTransM ctx (HSSet Credential -> Rational -> GovAction)
-> SpecTransM ctx (HSSet Credential)
-> SpecTransM ctx (Rational -> GovAction)
forall a b.
SpecTransM ctx (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Set (Credential 'ColdCommitteeRole)
-> SpecTransM ctx (SpecRep (Set (Credential 'ColdCommitteeRole)))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep Set (Credential 'ColdCommitteeRole)
remove
      SpecTransM ctx (Rational -> GovAction)
-> SpecTransM ctx Rational -> SpecTransM ctx GovAction
forall a b.
SpecTransM ctx (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> UnitInterval -> SpecTransM ctx (SpecRep UnitInterval)
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
      (Integer -> Maybe Integer -> GovAction)
-> SpecTransM ctx Integer
-> SpecTransM ctx (Maybe Integer -> GovAction)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SafeHash AnchorData
-> SpecTransM ctx (SpecRep (SafeHash AnchorData))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep SafeHash AnchorData
h
      SpecTransM ctx (Maybe Integer -> GovAction)
-> SpecTransM ctx (Maybe Integer) -> SpecTransM ctx GovAction
forall a b.
SpecTransM ctx (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> StrictMaybe ScriptHash
-> SpecTransM ctx (SpecRep (StrictMaybe ScriptHash))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep StrictMaybe ScriptHash
policy
  toSpecRep GovAction era
InfoAction = GovAction -> SpecTransM ctx GovAction
forall a. a -> SpecTransM ctx a
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 = (a -> SpecTransM ctx (SpecRep a))
-> [a] -> SpecTransM ctx [SpecRep a]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse a -> SpecTransM ctx (SpecRep a)
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep ([a] -> SpecTransM ctx [SpecRep a])
-> (OSet a -> [a]) -> OSet a -> SpecTransM ctx [SpecRep a]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. OSet a -> [a]
forall a. OSet a -> [a]
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 = ((k, v) -> SpecTransM ctx (SpecRep k, SpecRep v))
-> [(k, v)] -> SpecTransM ctx [(SpecRep k, SpecRep v)]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse ((k -> SpecTransM ctx (SpecRep k))
-> (v -> SpecTransM ctx (SpecRep v))
-> (k, v)
-> SpecTransM ctx (SpecRep k, SpecRep v)
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 k -> SpecTransM ctx (SpecRep k)
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep v -> SpecTransM ctx (SpecRep v)
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep) ([(k, v)] -> SpecTransM ctx [(SpecRep k, SpecRep v)])
-> (OMap k v -> [(k, v)])
-> OMap k v
-> SpecTransM ctx [(SpecRep k, SpecRep v)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. OMap k v -> [(k, v)]
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
GovAction era
RewardAccount
Coin
pProcDeposit :: Coin
pProcReturnAddr :: RewardAccount
pProcGovAction :: GovAction era
pProcAnchor :: Anchor
pProcDeposit :: forall era. ProposalProcedure era -> Coin
pProcReturnAddr :: forall era. ProposalProcedure era -> RewardAccount
pProcGovAction :: forall era. ProposalProcedure era -> GovAction era
pProcAnchor :: forall era. ProposalProcedure era -> Anchor
..} =
    GovAction
-> (Integer, Integer)
-> Maybe Integer
-> Integer
-> RwdAddr
-> Anchor
-> GovProposal
Agda.MkGovProposal
      (GovAction
 -> (Integer, Integer)
 -> Maybe Integer
 -> Integer
 -> RwdAddr
 -> Anchor
 -> GovProposal)
-> SpecTransM ctx GovAction
-> SpecTransM
     ctx
     ((Integer, Integer)
      -> Maybe Integer -> Integer -> RwdAddr -> Anchor -> GovProposal)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> GovAction era -> SpecTransM ctx (SpecRep (GovAction era))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep GovAction era
pProcGovAction
      SpecTransM
  ctx
  ((Integer, Integer)
   -> Maybe Integer -> Integer -> RwdAddr -> Anchor -> GovProposal)
-> SpecTransM ctx (Integer, Integer)
-> SpecTransM
     ctx (Maybe Integer -> Integer -> RwdAddr -> Anchor -> GovProposal)
forall a b.
SpecTransM ctx (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> GovActionId -> SpecTransM ctx (SpecRep GovActionId)
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep (StrictMaybe GovActionId -> GovAction era -> GovActionId
forall era. StrictMaybe GovActionId -> GovAction era -> GovActionId
nullifyIfNotNeeded StrictMaybe GovActionId
prevActionId GovAction era
pProcGovAction)
      SpecTransM
  ctx (Maybe Integer -> Integer -> RwdAddr -> Anchor -> GovProposal)
-> SpecTransM ctx (Maybe Integer)
-> SpecTransM ctx (Integer -> RwdAddr -> Anchor -> GovProposal)
forall a b.
SpecTransM ctx (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> StrictMaybe ScriptHash
-> SpecTransM ctx (SpecRep (StrictMaybe ScriptHash))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep StrictMaybe ScriptHash
policy
      SpecTransM ctx (Integer -> RwdAddr -> Anchor -> GovProposal)
-> SpecTransM ctx Integer
-> SpecTransM ctx (RwdAddr -> Anchor -> GovProposal)
forall a b.
SpecTransM ctx (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Coin -> SpecTransM ctx (SpecRep Coin)
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep Coin
pProcDeposit
      SpecTransM ctx (RwdAddr -> Anchor -> GovProposal)
-> SpecTransM ctx RwdAddr -> SpecTransM ctx (Anchor -> GovProposal)
forall a b.
SpecTransM ctx (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> RewardAccount -> SpecTransM ctx (SpecRep RewardAccount)
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep RewardAccount
pProcReturnAddr
      SpecTransM ctx (Anchor -> GovProposal)
-> SpecTransM ctx Anchor -> SpecTransM ctx GovProposal
forall a b.
SpecTransM ctx (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Anchor -> SpecTransM ctx (SpecRep Anchor)
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep Anchor
pProcAnchor
    where
      prevActionId :: StrictMaybe GovActionId
prevActionId = GovAction era -> StrictMaybe GovActionId
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
_ -> StrictMaybe ScriptHash
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
_ -> GovPurposeId 'PParamUpdatePurpose era -> GovActionId
forall (p :: GovActionPurpose) era.
GovPurposeId p era -> GovActionId
unGovPurposeId (GovPurposeId 'PParamUpdatePurpose era -> GovActionId)
-> StrictMaybe (GovPurposeId 'PParamUpdatePurpose era)
-> StrictMaybe GovActionId
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StrictMaybe (GovPurposeId 'PParamUpdatePurpose era)
x
    HardForkInitiation StrictMaybe (GovPurposeId 'HardForkPurpose era)
x ProtVer
_ -> GovPurposeId 'HardForkPurpose era -> GovActionId
forall (p :: GovActionPurpose) era.
GovPurposeId p era -> GovActionId
unGovPurposeId (GovPurposeId 'HardForkPurpose era -> GovActionId)
-> StrictMaybe (GovPurposeId 'HardForkPurpose era)
-> StrictMaybe GovActionId
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
_ -> GovPurposeId 'CommitteePurpose era -> GovActionId
forall (p :: GovActionPurpose) era.
GovPurposeId p era -> GovActionId
unGovPurposeId (GovPurposeId 'CommitteePurpose era -> GovActionId)
-> StrictMaybe (GovPurposeId 'CommitteePurpose era)
-> StrictMaybe GovActionId
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StrictMaybe (GovPurposeId 'CommitteePurpose era)
x
    NoConfidence StrictMaybe (GovPurposeId 'CommitteePurpose era)
x -> GovPurposeId 'CommitteePurpose era -> GovActionId
forall (p :: GovActionPurpose) era.
GovPurposeId p era -> GovActionId
unGovPurposeId (GovPurposeId 'CommitteePurpose era -> GovActionId)
-> StrictMaybe (GovPurposeId 'CommitteePurpose era)
-> StrictMaybe GovActionId
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
_ -> GovPurposeId 'ConstitutionPurpose era -> GovActionId
forall (p :: GovActionPurpose) era.
GovPurposeId p era -> GovActionId
unGovPurposeId (GovPurposeId 'ConstitutionPurpose era -> GovActionId)
-> StrictMaybe (GovPurposeId 'ConstitutionPurpose era)
-> StrictMaybe GovActionId
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StrictMaybe (GovPurposeId 'ConstitutionPurpose era)
x
    GovAction era
_ -> StrictMaybe GovActionId
forall a. StrictMaybe a
SNothing

nullGovActionId :: GovActionId
nullGovActionId :: GovActionId
nullGovActionId = TxId -> GovActionIx -> GovActionId
GovActionId (SafeHash EraIndependentTxBody -> TxId
TxId SafeHash EraIndependentTxBody
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 = GovActionId -> GovAction era -> GovActionId
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 [] = [(k, v)] -> HSMap k v
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' = [HSMap k v] -> HSMap k v
forall k v. [HSMap k v] -> HSMap k v
unionsHSMaps [HSMap k v]
xs
   in [(k, v)] -> HSMap k v
forall k v. [(k, v)] -> HSMap k v
Agda.MkHSMap ([(k, v)] -> HSMap k v) -> [(k, v)] -> HSMap k v
forall a b. (a -> b) -> a -> b
$ [(k, v)]
x [(k, v)] -> [(k, v)] -> [(k, v)]
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) = [(l, v)] -> HSMap l v
forall k v. [(k, v)] -> HSMap k v
Agda.MkHSMap ([(l, v)] -> HSMap l v) -> [(l, v)] -> HSMap l v
forall a b. (a -> b) -> a -> b
$ (k -> l) -> (k, v) -> (l, v)
forall a b c. (a -> b) -> (a, c) -> (b, c)
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first k -> l
f ((k, v) -> (l, v)) -> [(k, v)] -> [(l, v)]
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
gasId :: GovActionId
gasCommitteeVotes :: Map (Credential 'HotCommitteeRole) Vote
gasDRepVotes :: Map (Credential 'DRepRole) Vote
gasStakePoolVotes :: Map (KeyHash 'StakePool) Vote
gasProposalProcedure :: ProposalProcedure era
gasProposedIn :: EpochNo
gasExpiresAfter :: EpochNo
gasId :: forall era. GovActionState era -> GovActionId
gasCommitteeVotes :: forall era.
GovActionState era -> Map (Credential 'HotCommitteeRole) Vote
gasDRepVotes :: forall era. GovActionState era -> Map (Credential 'DRepRole) Vote
gasStakePoolVotes :: forall era. GovActionState era -> Map (KeyHash 'StakePool) Vote
gasProposalProcedure :: forall era. GovActionState era -> ProposalProcedure era
gasProposedIn :: forall era. GovActionState era -> EpochNo
gasExpiresAfter :: forall era. GovActionState era -> EpochNo
..} = do
    HSMap (GovRole, Credential) Vote
-> RwdAddr
-> Integer
-> GovAction
-> (Integer, Integer)
-> GovActionState
Agda.MkGovActionState
      (HSMap (GovRole, Credential) Vote
 -> RwdAddr
 -> Integer
 -> GovAction
 -> (Integer, Integer)
 -> GovActionState)
-> SpecTransM ctx (HSMap (GovRole, Credential) Vote)
-> SpecTransM
     ctx
     (RwdAddr
      -> Integer -> GovAction -> (Integer, Integer) -> GovActionState)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SpecTransM ctx (HSMap (GovRole, Credential) Vote)
agdaVoteMap
      SpecTransM
  ctx
  (RwdAddr
   -> Integer -> GovAction -> (Integer, Integer) -> GovActionState)
-> SpecTransM ctx RwdAddr
-> SpecTransM
     ctx (Integer -> GovAction -> (Integer, Integer) -> GovActionState)
forall a b.
SpecTransM ctx (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> RewardAccount -> SpecTransM ctx (SpecRep RewardAccount)
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep (GovActionState era -> RewardAccount
forall era. GovActionState era -> RewardAccount
gasReturnAddr GovActionState era
gas)
      SpecTransM
  ctx (Integer -> GovAction -> (Integer, Integer) -> GovActionState)
-> SpecTransM ctx Integer
-> SpecTransM
     ctx (GovAction -> (Integer, Integer) -> GovActionState)
forall a b.
SpecTransM ctx (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> EpochNo -> SpecTransM ctx (SpecRep EpochNo)
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep EpochNo
gasExpiresAfter
      SpecTransM ctx (GovAction -> (Integer, Integer) -> GovActionState)
-> SpecTransM ctx GovAction
-> SpecTransM ctx ((Integer, Integer) -> GovActionState)
forall a b.
SpecTransM ctx (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> GovAction era -> SpecTransM ctx (SpecRep (GovAction era))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep GovAction era
action
      SpecTransM ctx ((Integer, Integer) -> GovActionState)
-> SpecTransM ctx (Integer, Integer)
-> SpecTransM ctx GovActionState
forall a b.
SpecTransM ctx (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> GovActionId -> SpecTransM ctx (SpecRep GovActionId)
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep (StrictMaybe GovActionId -> GovAction era -> GovActionId
forall era. StrictMaybe GovActionId -> GovAction era -> GovActionId
nullifyIfNotNeeded (GovAction era -> StrictMaybe GovActionId
forall era. GovAction era -> StrictMaybe GovActionId
prevGovActionId GovAction era
action) GovAction era
action)
    where
      action :: GovAction era
action = GovActionState era -> GovAction era
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 <- Map (Credential 'DRepRole) Vote
-> SpecTransM ctx (SpecRep (Map (Credential 'DRepRole) Vote))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep Map (Credential 'DRepRole) Vote
gasDRepVotes
        HSMap Credential Vote
ccVotes <- Map (Credential 'HotCommitteeRole) Vote
-> SpecTransM
     ctx (SpecRep (Map (Credential 'HotCommitteeRole) Vote))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep Map (Credential 'HotCommitteeRole) Vote
gasCommitteeVotes
        HSMap Integer Vote
spoVotes <- Map (KeyHash 'StakePool) Vote
-> SpecTransM ctx (SpecRep (Map (KeyHash 'StakePool) Vote))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep Map (KeyHash 'StakePool) Vote
gasStakePoolVotes
        HSMap (GovRole, Credential) Vote
-> SpecTransM ctx (HSMap (GovRole, Credential) Vote)
forall a. a -> SpecTransM ctx a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (HSMap (GovRole, Credential) Vote
 -> SpecTransM ctx (HSMap (GovRole, Credential) Vote))
-> HSMap (GovRole, Credential) Vote
-> SpecTransM ctx (HSMap (GovRole, Credential) Vote)
forall a b. (a -> b) -> a -> b
$
          [HSMap (GovRole, Credential) Vote]
-> HSMap (GovRole, Credential) Vote
forall k v. [HSMap k v] -> HSMap k v
unionsHSMaps
            [ (Credential -> (GovRole, Credential))
-> HSMap Credential Vote -> HSMap (GovRole, Credential) Vote
forall k l v. (k -> l) -> HSMap k v -> HSMap l v
mapHSMapKey (GovRole
Agda.DRep,) HSMap Credential Vote
drepVotes
            , (Credential -> (GovRole, Credential))
-> HSMap Credential Vote -> HSMap (GovRole, Credential) Vote
forall k l v. (k -> l) -> HSMap k v -> HSMap l v
mapHSMapKey (GovRole
Agda.CC,) HSMap Credential Vote
ccVotes
            , (Integer -> (GovRole, Credential))
-> HSMap Integer Vote -> HSMap (GovRole, Credential) Vote
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 = Integer -> SpecTransM ctx Integer
forall a. a -> SpecTransM ctx a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Integer -> SpecTransM ctx Integer)
-> (GovActionIx -> Integer)
-> GovActionIx
-> SpecTransM ctx Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Word16 -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Word16 -> Integer)
-> (GovActionIx -> Word16) -> GovActionIx -> Integer
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) = (TxId, GovActionIx) -> SpecTransM ctx (SpecRep (TxId, GovActionIx))
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 = OMap GovActionId (GovActionState era)
-> SpecTransM ctx [((Integer, Integer), GovActionState)]
OMap GovActionId (GovActionState era)
-> SpecTransM ctx (SpecRep (OMap GovActionId (GovActionState era)))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep (OMap GovActionId (GovActionState era)
 -> SpecTransM ctx [((Integer, Integer), GovActionState)])
-> (Proposals era -> OMap GovActionId (GovActionState era))
-> Proposals era
-> SpecTransM ctx [((Integer, Integer), GovActionState)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. OMap GovActionId (GovActionState era)
-> OMap GovActionId (GovActionState era)
prioritySort (OMap GovActionId (GovActionState era)
 -> OMap GovActionId (GovActionState era))
-> (Proposals era -> OMap GovActionId (GovActionState era))
-> Proposals era
-> OMap GovActionId (GovActionState era)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Getting
  (OMap GovActionId (GovActionState era))
  (Proposals era)
  (OMap GovActionId (GovActionState era))
-> Proposals era -> OMap GovActionId (GovActionState era)
forall a s. Getting a s a -> s -> a
view Getting
  (OMap GovActionId (GovActionState era))
  (Proposals era)
  (OMap GovActionId (GovActionState era))
forall era (f :: * -> *).
Functor f =>
(OMap GovActionId (GovActionState era)
 -> f (OMap GovActionId (GovActionState era)))
-> Proposals era -> f (Proposals era)
pPropsL
    where
      prioritySort ::
        OMap GovActionId (GovActionState era) ->
        OMap GovActionId (GovActionState era)
      prioritySort :: OMap GovActionId (GovActionState era)
-> OMap GovActionId (GovActionState era)
prioritySort = [Item (OMap GovActionId (GovActionState era))]
-> OMap GovActionId (GovActionState era)
[GovActionState era] -> OMap GovActionId (GovActionState era)
forall l. IsList l => [Item l] -> l
Exts.fromList ([GovActionState era] -> OMap GovActionId (GovActionState era))
-> (OMap GovActionId (GovActionState era) -> [GovActionState era])
-> OMap GovActionId (GovActionState era)
-> OMap GovActionId (GovActionState era)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (GovActionState era -> Int)
-> [GovActionState era] -> [GovActionState era]
forall b a. Ord b => (a -> b) -> [a] -> [a]
sortOn (GovAction era -> Int
forall era. GovAction era -> Int
actionPriority (GovAction era -> Int)
-> (GovActionState era -> GovAction era)
-> GovActionState era
-> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. GovActionState era -> GovAction era
forall era. GovActionState era -> GovAction era
gasAction) ([GovActionState era] -> [GovActionState era])
-> (OMap GovActionId (GovActionState era) -> [GovActionState era])
-> OMap GovActionId (GovActionState era)
-> [GovActionState era]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. OMap GovActionId (GovActionState era)
-> [Item (OMap GovActionId (GovActionState era))]
OMap GovActionId (GovActionState era) -> [GovActionState era]
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 = Coin -> SpecTransM ctx Integer
Coin -> SpecTransM ctx (SpecRep Coin)
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep (Coin -> SpecTransM ctx Integer)
-> (MaryValue -> Coin) -> MaryValue -> SpecTransM ctx Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MaryValue -> Coin
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 = OpaqueErrorString -> SpecTransM ctx OpaqueErrorString
forall a. a -> SpecTransM ctx a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (OpaqueErrorString -> SpecTransM ctx OpaqueErrorString)
-> (ConwayCertPredFailure era -> OpaqueErrorString)
-> ConwayCertPredFailure era
-> SpecTransM ctx OpaqueErrorString
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ConwayCertPredFailure era -> OpaqueErrorString
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 = a -> SpecTransM ctx (SpecRep a)
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep (a -> SpecTransM ctx (SpecRep a))
-> (CompactForm a -> a)
-> CompactForm a
-> SpecTransM ctx (SpecRep a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CompactForm a -> a
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) = Maybe (Credential 'HotCommitteeRole)
-> SpecTransM ctx (SpecRep (Maybe (Credential 'HotCommitteeRole)))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep (Maybe (Credential 'HotCommitteeRole)
 -> SpecTransM ctx (SpecRep (Maybe (Credential 'HotCommitteeRole))))
-> Maybe (Credential 'HotCommitteeRole)
-> SpecTransM ctx (SpecRep (Maybe (Credential 'HotCommitteeRole)))
forall a b. (a -> b) -> a -> b
$ Credential 'HotCommitteeRole
-> Maybe (Credential 'HotCommitteeRole)
forall a. a -> Maybe a
Just Credential 'HotCommitteeRole
c
  toSpecRep (CommitteeMemberResigned StrictMaybe Anchor
_) =
    Maybe (Credential 'HotCommitteeRole)
-> SpecTransM ctx (SpecRep (Maybe (Credential 'HotCommitteeRole)))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep (Maybe (Credential 'HotCommitteeRole)
 -> SpecTransM ctx (SpecRep (Maybe (Credential 'HotCommitteeRole))))
-> Maybe (Credential 'HotCommitteeRole)
-> SpecTransM ctx (SpecRep (Maybe (Credential 'HotCommitteeRole)))
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 = Map (Credential 'ColdCommitteeRole) CommitteeAuthorization
-> SpecTransM ctx (HSMap Credential (Maybe Credential))
Map (Credential 'ColdCommitteeRole) CommitteeAuthorization
-> SpecTransM
     ctx
     (SpecRep
        (Map (Credential 'ColdCommitteeRole) CommitteeAuthorization))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep (Map (Credential 'ColdCommitteeRole) CommitteeAuthorization
 -> SpecTransM ctx (HSMap Credential (Maybe Credential)))
-> (CommitteeState era
    -> Map (Credential 'ColdCommitteeRole) CommitteeAuthorization)
-> CommitteeState era
-> SpecTransM ctx (HSMap Credential (Maybe Credential))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CommitteeState era
-> Map (Credential 'ColdCommitteeRole) CommitteeAuthorization
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
_) = CompactForm Coin -> SpecTransM ctx (SpecRep (CompactForm Coin))
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 [(Integer, Integer)]
l <- Map (KeyHash 'StakePool) IndividualPoolStake
-> SpecTransM
     ctx (SpecRep (Map (KeyHash 'StakePool) IndividualPoolStake))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep Map (KeyHash 'StakePool) IndividualPoolStake
ps
    HSMap VDeleg Integer -> SpecTransM ctx (HSMap VDeleg Integer)
forall a. a -> SpecTransM ctx a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (HSMap VDeleg Integer -> SpecTransM ctx (HSMap VDeleg Integer))
-> ([(VDeleg, Integer)] -> HSMap VDeleg Integer)
-> [(VDeleg, Integer)]
-> SpecTransM ctx (HSMap VDeleg Integer)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(VDeleg, Integer)] -> HSMap VDeleg Integer
forall k v. [(k, v)] -> HSMap k v
Agda.MkHSMap ([(VDeleg, Integer)] -> SpecTransM ctx (HSMap VDeleg Integer))
-> [(VDeleg, Integer)] -> SpecTransM ctx (HSMap VDeleg Integer)
forall a b. (a -> b) -> a -> b
$ (Integer -> VDeleg) -> (Integer, Integer) -> (VDeleg, Integer)
forall a b c. (a -> b) -> (a, c) -> (b, c)
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first (GovRole -> Credential -> VDeleg
Agda.CredVoter GovRole
Agda.SPO (Credential -> VDeleg)
-> (Integer -> Credential) -> Integer -> VDeleg
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> Credential
Agda.KeyHashObj) ((Integer, Integer) -> (VDeleg, Integer))
-> [(Integer, Integer)] -> [(VDeleg, Integer)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Integer, Integer)]
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 (KeyHash 'StakePool) PoolParams
Map DRep (CompactForm Coin)
Map StakeCredential DRep
Map (Credential 'DRepRole) DRepState
PoolDistr
CommitteeState era
InstantStake era
EpochNo
reInstantStake :: InstantStake era
reStakePoolDistr :: PoolDistr
reDRepDistr :: Map DRep (CompactForm Coin)
reDRepState :: Map (Credential 'DRepRole) DRepState
reCurrentEpoch :: EpochNo
reCommitteeState :: CommitteeState era
reDelegatees :: Map StakeCredential DRep
rePoolParams :: Map (KeyHash 'StakePool) PoolParams
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 StakeCredential DRep
rePoolParams :: forall era. RatifyEnv era -> Map (KeyHash 'StakePool) PoolParams
..} = do
    let
      stakeDistrs :: SpecTransM ctx StakeDistrs
stakeDistrs = do
        Agda.MkHSMap [(VDeleg, Integer)]
stakeDistrsMap <- PoolDistr -> SpecTransM ctx (SpecRep PoolDistr)
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep PoolDistr
reStakePoolDistr
        [(VDeleg, Integer)]
drepDistrsMap <- [(DRep, CompactForm Coin)]
-> SpecTransM ctx (SpecRep [(DRep, CompactForm Coin)])
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep ([(DRep, CompactForm Coin)]
 -> SpecTransM ctx (SpecRep [(DRep, CompactForm Coin)]))
-> [(DRep, CompactForm Coin)]
-> SpecTransM ctx (SpecRep [(DRep, CompactForm Coin)])
forall a b. (a -> b) -> a -> b
$ Map DRep (CompactForm Coin) -> [(DRep, CompactForm Coin)]
forall k a. Map k a -> [(k, a)]
Map.toList Map DRep (CompactForm Coin)
reDRepDistr
        StakeDistrs -> SpecTransM ctx StakeDistrs
forall a. a -> SpecTransM ctx a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (StakeDistrs -> SpecTransM ctx StakeDistrs)
-> (HSMap VDeleg Integer -> StakeDistrs)
-> HSMap VDeleg Integer
-> SpecTransM ctx StakeDistrs
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HSMap VDeleg Integer -> StakeDistrs
Agda.StakeDistrs (HSMap VDeleg Integer -> SpecTransM ctx StakeDistrs)
-> HSMap VDeleg Integer -> SpecTransM ctx StakeDistrs
forall a b. (a -> b) -> a -> b
$ [(VDeleg, Integer)] -> HSMap VDeleg Integer
forall k v. [(k, v)] -> HSMap k v
Agda.MkHSMap ([(VDeleg, Integer)]
stakeDistrsMap [(VDeleg, Integer)] -> [(VDeleg, Integer)] -> [(VDeleg, Integer)]
forall a. Semigroup a => a -> a -> a
<> [(VDeleg, Integer)]
drepDistrsMap)
      dreps :: SpecTransM ctx (SpecRep (Map (Credential 'DRepRole) EpochNo))
dreps = Map (Credential 'DRepRole) EpochNo
-> SpecTransM ctx (SpecRep (Map (Credential 'DRepRole) EpochNo))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep (Map (Credential 'DRepRole) EpochNo
 -> SpecTransM ctx (SpecRep (Map (Credential 'DRepRole) EpochNo)))
-> Map (Credential 'DRepRole) EpochNo
-> SpecTransM ctx (SpecRep (Map (Credential 'DRepRole) EpochNo))
forall a b. (a -> b) -> a -> b
$ (DRepState -> EpochNo)
-> Map (Credential 'DRepRole) DRepState
-> Map (Credential 'DRepRole) EpochNo
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
      (StakeDistrs
 -> Integer
 -> HSMap Credential Integer
 -> HSMap Credential (Maybe Credential)
 -> Integer
 -> HSMap Integer PoolParams
 -> HSMap Credential VDeleg
 -> RatifyEnv)
-> SpecTransM ctx StakeDistrs
-> SpecTransM
     ctx
     (Integer
      -> HSMap Credential Integer
      -> HSMap Credential (Maybe Credential)
      -> Integer
      -> HSMap Integer PoolParams
      -> HSMap Credential VDeleg
      -> RatifyEnv)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SpecTransM ctx StakeDistrs
stakeDistrs
      SpecTransM
  ctx
  (Integer
   -> HSMap Credential Integer
   -> HSMap Credential (Maybe Credential)
   -> Integer
   -> HSMap Integer PoolParams
   -> HSMap Credential VDeleg
   -> RatifyEnv)
-> SpecTransM ctx Integer
-> SpecTransM
     ctx
     (HSMap Credential Integer
      -> HSMap Credential (Maybe Credential)
      -> Integer
      -> HSMap Integer PoolParams
      -> HSMap Credential VDeleg
      -> RatifyEnv)
forall a b.
SpecTransM ctx (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> EpochNo -> SpecTransM ctx (SpecRep EpochNo)
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep EpochNo
reCurrentEpoch
      SpecTransM
  ctx
  (HSMap Credential Integer
   -> HSMap Credential (Maybe Credential)
   -> Integer
   -> HSMap Integer PoolParams
   -> HSMap Credential VDeleg
   -> RatifyEnv)
-> SpecTransM ctx (HSMap Credential Integer)
-> SpecTransM
     ctx
     (HSMap Credential (Maybe Credential)
      -> Integer
      -> HSMap Integer PoolParams
      -> HSMap Credential VDeleg
      -> RatifyEnv)
forall a b.
SpecTransM ctx (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> SpecTransM ctx (HSMap Credential Integer)
SpecTransM ctx (SpecRep (Map (Credential 'DRepRole) EpochNo))
dreps
      SpecTransM
  ctx
  (HSMap Credential (Maybe Credential)
   -> Integer
   -> HSMap Integer PoolParams
   -> HSMap Credential VDeleg
   -> RatifyEnv)
-> SpecTransM ctx (HSMap Credential (Maybe Credential))
-> SpecTransM
     ctx
     (Integer
      -> HSMap Integer PoolParams
      -> HSMap Credential VDeleg
      -> RatifyEnv)
forall a b.
SpecTransM ctx (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> CommitteeState era -> SpecTransM ctx (SpecRep (CommitteeState era))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep CommitteeState era
reCommitteeState
      SpecTransM
  ctx
  (Integer
   -> HSMap Integer PoolParams
   -> HSMap Credential VDeleg
   -> RatifyEnv)
-> SpecTransM ctx Integer
-> SpecTransM
     ctx
     (HSMap Integer PoolParams -> HSMap Credential VDeleg -> RatifyEnv)
forall a b.
SpecTransM ctx (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Coin -> SpecTransM ctx (SpecRep Coin)
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep Coin
treasury
      SpecTransM
  ctx
  (HSMap Integer PoolParams -> HSMap Credential VDeleg -> RatifyEnv)
-> SpecTransM ctx (HSMap Integer PoolParams)
-> SpecTransM ctx (HSMap Credential VDeleg -> RatifyEnv)
forall a b.
SpecTransM ctx (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Map (KeyHash 'StakePool) PoolParams
-> SpecTransM ctx (SpecRep (Map (KeyHash 'StakePool) PoolParams))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep Map (KeyHash 'StakePool) PoolParams
rePoolParams
      SpecTransM ctx (HSMap Credential VDeleg -> RatifyEnv)
-> SpecTransM ctx (HSMap Credential VDeleg)
-> SpecTransM ctx RatifyEnv
forall a b.
SpecTransM ctx (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Map StakeCredential DRep
-> SpecTransM ctx (SpecRep (Map StakeCredential DRep))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep Map StakeCredential DRep
reDelegatees

instance SpecTranslate ctx Bool where
  type SpecRep Bool = Bool

  toSpecRep :: Bool -> SpecTransM ctx (SpecRep Bool)
toSpecRep = Bool -> SpecTransM ctx Bool
Bool -> SpecTransM ctx (SpecRep Bool)
forall a. a -> SpecTransM ctx a
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)
rsEnactState :: EnactState era
rsEnacted :: Seq (GovActionState era)
rsExpired :: Set GovActionId
rsDelayed :: Bool
rsEnactState :: forall era. RatifyState era -> EnactState era
rsEnacted :: forall era. RatifyState era -> Seq (GovActionState era)
rsExpired :: forall era. RatifyState era -> Set GovActionId
rsDelayed :: forall era. RatifyState era -> Bool
..} = do
    Map GovActionId (GovActionState era)
govActionMap <-
      (Map GovActionId (GovActionState era)
 -> GovActionState era -> Map GovActionId (GovActionState era))
-> Map GovActionId (GovActionState era)
-> [GovActionState era]
-> Map GovActionId (GovActionState era)
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' (\Map GovActionId (GovActionState era)
acc GovActionState era
gas -> GovActionId
-> GovActionState era
-> Map GovActionId (GovActionState era)
-> Map GovActionId (GovActionState era)
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert (GovActionState era -> GovActionId
forall era. GovActionState era -> GovActionId
gasId GovActionState era
gas) GovActionState era
gas Map GovActionId (GovActionState era)
acc) Map GovActionId (GovActionState era)
forall a. Monoid a => a
mempty
        ([GovActionState era] -> Map GovActionId (GovActionState era))
-> SpecTransM ctx [GovActionState era]
-> SpecTransM ctx (Map GovActionId (GovActionState era))
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 GovActionId
-> Map GovActionId (GovActionState era)
-> Maybe (GovActionState era)
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 -> (GovActionId, GovActionState era)
-> Set (GovActionId, GovActionState era)
-> Set (GovActionId, GovActionState era)
forall a. Ord a => a -> Set a -> Set a
Set.insert (GovActionId
gaId, GovActionState era
x) (Set (GovActionId, GovActionState era)
 -> Set (GovActionId, GovActionState era))
-> SpecTransM ctx (Set (GovActionId, GovActionState era))
-> SpecTransM ctx (Set (GovActionId, GovActionState era))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SpecTransM ctx (Set (GovActionId, GovActionState era))
m
          Maybe (GovActionState era)
Nothing ->
            Text -> SpecTransM ctx (Set (GovActionId, GovActionState era))
forall a. Text -> SpecTransM ctx a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (Text -> SpecTransM ctx (Set (GovActionId, GovActionState era)))
-> Text -> SpecTransM ctx (Set (GovActionId, GovActionState era))
forall a b. (a -> b) -> a -> b
$
              Text
"gaId: "
                Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> [Char] -> Text
T.pack (GovActionId -> [Char]
forall a. ToExpr a => a -> [Char]
showExpr GovActionId
gaId)
                Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
"\n\ngovActionMap: "
                Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> [Char] -> Text
T.pack (Map GovActionId (GovActionState era) -> [Char]
forall a. ToExpr a => a -> [Char]
showExpr Map GovActionId (GovActionState era)
govActionMap)
                Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
"\n\nGovActionId is not contained in the govActionMap"
    Set (GovActionId, GovActionState era)
removed <-
      (GovActionId
 -> SpecTransM ctx (Set (GovActionId, GovActionState era))
 -> SpecTransM ctx (Set (GovActionId, GovActionState era)))
-> SpecTransM ctx (Set (GovActionId, GovActionState era))
-> Set GovActionId
-> SpecTransM ctx (Set (GovActionId, GovActionState era))
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
        (Set (GovActionId, GovActionState era)
-> SpecTransM ctx (Set (GovActionId, GovActionState era))
forall a. a -> SpecTransM ctx a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Set (GovActionId, GovActionState era)
forall a. Set a
Set.empty)
        (Set GovActionId
rsExpired Set GovActionId -> Set GovActionId -> Set GovActionId
forall a. Ord a => Set a -> Set a -> Set a
`Set.union` [GovActionId] -> Set GovActionId
forall a. Ord a => [a] -> Set a
Set.fromList (GovActionState era -> GovActionId
forall era. GovActionState era -> GovActionId
gasId (GovActionState era -> GovActionId)
-> [GovActionState era] -> [GovActionId]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Seq (GovActionState era) -> [GovActionState era]
forall a. Seq a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList Seq (GovActionState era)
rsEnacted))
    EnactState
-> HSSet ((Integer, Integer), GovActionState)
-> Bool
-> RatifyState
Agda.MkRatifyState
      (EnactState
 -> HSSet ((Integer, Integer), GovActionState)
 -> Bool
 -> RatifyState)
-> SpecTransM ctx EnactState
-> SpecTransM
     ctx
     (HSSet ((Integer, Integer), GovActionState) -> Bool -> RatifyState)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> EnactState era -> SpecTransM ctx (SpecRep (EnactState era))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep EnactState era
rsEnactState
      SpecTransM
  ctx
  (HSSet ((Integer, Integer), GovActionState) -> Bool -> RatifyState)
-> SpecTransM ctx (HSSet ((Integer, Integer), GovActionState))
-> SpecTransM ctx (Bool -> RatifyState)
forall a b.
SpecTransM ctx (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Set (GovActionId, GovActionState era)
-> SpecTransM ctx (SpecRep (Set (GovActionId, GovActionState era)))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep Set (GovActionId, GovActionState era)
removed
      SpecTransM ctx (Bool -> RatifyState)
-> SpecTransM ctx Bool -> SpecTransM ctx RatifyState
forall a b.
SpecTransM ctx (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Bool -> SpecTransM ctx (SpecRep Bool)
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) =
    StrictSeq (GovActionId, GovActionState era)
-> SpecTransM
     ctx (SpecRep (StrictSeq (GovActionId, GovActionState era)))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep (StrictSeq (GovActionId, GovActionState era)
 -> SpecTransM
      ctx (SpecRep (StrictSeq (GovActionId, GovActionState era))))
-> StrictSeq (GovActionId, GovActionState era)
-> SpecTransM
     ctx (SpecRep (StrictSeq (GovActionId, GovActionState era)))
forall a b. (a -> b) -> a -> b
$
      (\gas :: GovActionState era
gas@GovActionState {GovActionId
gasId :: forall era. GovActionState era -> GovActionId
gasId :: GovActionId
gasId} -> (GovActionId
gasId, GovActionState era
gas)) (GovActionState era -> (GovActionId, GovActionState era))
-> StrictSeq (GovActionState era)
-> StrictSeq (GovActionId, GovActionState era)
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) = GovAction era -> SpecTransM ctx (SpecRep (GovAction era))
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
_ = () -> SpecTransM ctx ()
forall a. a -> SpecTransM ctx a
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 x.
 ConwayExecEnactEnv era -> Rep (ConwayExecEnactEnv era) x)
-> (forall x.
    Rep (ConwayExecEnactEnv era) x -> ConwayExecEnactEnv era)
-> Generic (ConwayExecEnactEnv era)
forall x. Rep (ConwayExecEnactEnv era) x -> ConwayExecEnactEnv era
forall x. ConwayExecEnactEnv era -> Rep (ConwayExecEnactEnv era) x
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
$cfrom :: forall era x.
ConwayExecEnactEnv era -> Rep (ConwayExecEnactEnv era) x
from :: forall x. ConwayExecEnactEnv era -> Rep (ConwayExecEnactEnv era) x
$cto :: forall era x.
Rep (ConwayExecEnactEnv era) x -> ConwayExecEnactEnv era
to :: forall x. Rep (ConwayExecEnactEnv era) x -> ConwayExecEnactEnv era
Generic, ConwayExecEnactEnv era -> ConwayExecEnactEnv era -> Bool
(ConwayExecEnactEnv era -> ConwayExecEnactEnv era -> Bool)
-> (ConwayExecEnactEnv era -> ConwayExecEnactEnv era -> Bool)
-> Eq (ConwayExecEnactEnv era)
forall era.
ConwayExecEnactEnv era -> ConwayExecEnactEnv era -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall era.
ConwayExecEnactEnv era -> ConwayExecEnactEnv era -> Bool
== :: ConwayExecEnactEnv era -> ConwayExecEnactEnv era -> Bool
$c/= :: forall era.
ConwayExecEnactEnv era -> ConwayExecEnactEnv era -> Bool
/= :: ConwayExecEnactEnv era -> ConwayExecEnactEnv era -> Bool
Eq, Int -> ConwayExecEnactEnv era -> ShowS
[ConwayExecEnactEnv era] -> ShowS
ConwayExecEnactEnv era -> [Char]
(Int -> ConwayExecEnactEnv era -> ShowS)
-> (ConwayExecEnactEnv era -> [Char])
-> ([ConwayExecEnactEnv era] -> ShowS)
-> Show (ConwayExecEnactEnv era)
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
$cshowsPrec :: forall era. Int -> ConwayExecEnactEnv era -> ShowS
showsPrec :: Int -> ConwayExecEnactEnv era -> ShowS
$cshow :: forall era. ConwayExecEnactEnv era -> [Char]
show :: ConwayExecEnactEnv era -> [Char]
$cshowList :: forall era. [ConwayExecEnactEnv era] -> ShowS
showList :: [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 {GovActionId
Coin
EpochNo
ceeeGid :: forall era. ConwayExecEnactEnv era -> GovActionId
ceeeTreasury :: forall era. ConwayExecEnactEnv era -> Coin
ceeeEpoch :: forall era. ConwayExecEnactEnv era -> EpochNo
ceeeGid :: GovActionId
ceeeTreasury :: Coin
ceeeEpoch :: EpochNo
..} =
    (Integer, Integer) -> Integer -> Integer -> EnactEnv
Agda.MkEnactEnv
      ((Integer, Integer) -> Integer -> Integer -> EnactEnv)
-> SpecTransM ctx (Integer, Integer)
-> SpecTransM ctx (Integer -> Integer -> EnactEnv)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> GovActionId -> SpecTransM ctx (SpecRep GovActionId)
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep GovActionId
ceeeGid
      SpecTransM ctx (Integer -> Integer -> EnactEnv)
-> SpecTransM ctx Integer -> SpecTransM ctx (Integer -> EnactEnv)
forall a b.
SpecTransM ctx (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Coin -> SpecTransM ctx (SpecRep Coin)
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep Coin
ceeeTreasury
      SpecTransM ctx (Integer -> EnactEnv)
-> SpecTransM ctx Integer -> SpecTransM ctx EnactEnv
forall a b.
SpecTransM ctx (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> EpochNo -> SpecTransM ctx (SpecRep EpochNo)
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) = Credential 'HotCommitteeRole
-> StrictMaybe (Credential 'HotCommitteeRole)
forall a. a -> StrictMaybe a
SJust Credential 'HotCommitteeRole
c
committeeCredentialToStrictMaybe (CommitteeMemberResigned StrictMaybe Anchor
_) = StrictMaybe (Credential 'HotCommitteeRole)
forall a. StrictMaybe a
SNothing

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