{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# 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 (..),
) where

import Cardano.Ledger.Address (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.TxWits (AlonzoTxWits (..), Redeemers (..), TxDats (..), unTxDats)
import Cardano.Ledger.Babbage.TxOut (BabbageTxOut (..))
import Cardano.Ledger.BaseTypes
import Cardano.Ledger.Coin (Coin (..))
import Cardano.Ledger.Conway.Core
import Cardano.Ledger.Conway.Governance
import Cardano.Ledger.Conway.PParams (ConwayEraPParams (..), ConwayPParams (..), THKD (..))
import Cardano.Ledger.Conway.Rules (EnactSignal (..))
import Cardano.Ledger.Conway.Scripts (AlonzoScript (..), ConwayPlutusPurpose (..))
import Cardano.Ledger.Conway.State
import Cardano.Ledger.Credential (Credential (..))
import Cardano.Ledger.HKD (HKD)
import Cardano.Ledger.Shelley.Rules (Identity)
import Cardano.Ledger.Shelley.Scripts (
  pattern RequireAllOf,
  pattern RequireAnyOf,
  pattern RequireMOf,
  pattern RequireSignature,
 )
import Cardano.Ledger.TxIn (TxId (..), TxIn (..))
import Cardano.Ledger.Val (Val (..))
import Control.Monad.Except (MonadError (..))
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.Set as Set
import qualified Data.Text as T
import Data.Traversable (forM)
import qualified GHC.Exts as Exts
import Lens.Micro
import Lens.Micro.Extras (view)
import qualified MAlonzo.Code.Ledger.Foreign.API as Agda
import Test.Cardano.Ledger.Conformance.Orphans ()
import Test.Cardano.Ledger.Conformance.SpecTranslate.Base (
  SpecTransM,
  SpecTranslate (..),
  askCtx,
 )
import Test.Cardano.Ledger.Conformance.SpecTranslate.Core (committeeCredentialToStrictMaybe)
import Test.Cardano.Ledger.Conway.TreeDiff (ToExpr (..), showExpr)

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
$ NativeScript era -> AlonzoScript era
forall era. NativeScript era -> AlonzoScript era
NativeScript Timelock era
NativeScript 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
            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
            pure . Agda.RequireAllOf $ toList tls
          RequireAnyOf StrictSeq (NativeScript era)
ss -> do
            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
            pure . Agda.RequireAnyOf $ toList tls
          RequireMOf Int
m StrictSeq (NativeScript era)
ss -> do
            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
            pure . Agda.RequireMOf (toInteger m) $ toList 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
          NativeScript era
_ -> [Char] -> SpecTransM ctx Timelock
forall a. HasCallStack => [Char] -> a
error [Char]
"Impossible: All NativeScripts should have been accounted for"

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 (NativeScript NativeScript 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
NativeScript 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
    addr' <- Addr -> SpecTransM ctx (SpecRep Addr)
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep Addr
addr
    val' <- toSpecRep val
    datum' <- toSpecRep datum
    script' <- toSpecRep script
    pure (addr', (val', (datum', script')))

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 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
dvtTreasuryWithdrawal :: DRepVotingThresholds -> UnitInterval
dvtPPGovGroup :: DRepVotingThresholds -> UnitInterval
dvtPPTechnicalGroup :: DRepVotingThresholds -> UnitInterval
dvtPPEconomicGroup :: DRepVotingThresholds -> UnitInterval
dvtPPNetworkGroup :: DRepVotingThresholds -> UnitInterval
dvtHardForkInitiation :: DRepVotingThresholds -> UnitInterval
dvtUpdateToConstitution :: DRepVotingThresholds -> UnitInterval
dvtCommitteeNoConfidence :: DRepVotingThresholds -> UnitInterval
dvtCommitteeNormal :: DRepVotingThresholds -> UnitInterval
dvtMotionNoConfidence :: 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
pvtPPSecurityGroup :: PoolVotingThresholds -> UnitInterval
pvtHardForkInitiation :: PoolVotingThresholds -> UnitInterval
pvtCommitteeNoConfidence :: PoolVotingThresholds -> UnitInterval
pvtCommitteeNormal :: PoolVotingThresholds -> UnitInterval
pvtMotionNoConfidence :: 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
  ( ConwayEraPParams era
  , PParamsHKD Identity era ~ ConwayPParams Identity era
  ) =>
  SpecTranslate ctx (ConwayPParams Identity era)
  where
  type SpecRep (ConwayPParams Identity era) = Agda.PParams

  toSpecRep :: ConwayPParams Identity era
-> SpecTransM ctx (SpecRep (ConwayPParams Identity era))
toSpecRep cpp :: ConwayPParams Identity era
cpp@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
  (CompactForm 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
  DRepVotingThresholds
THKD
  ('PPGroups 'GovGroup 'NoStakePoolGroup)
  Identity
  PoolVotingThresholds
THKD ('PPGroups 'GovGroup 'NoStakePoolGroup) Identity EpochInterval
THKD
  ('PPGroups 'GovGroup 'NoStakePoolGroup) Identity (CompactForm Coin)
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
  (CompactForm 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 (CompactForm Coin)
cppDRepActivity :: THKD ('PPGroups 'GovGroup 'NoStakePoolGroup) Identity EpochInterval
cppMinFeeRefScriptCostPerByte :: THKD
  ('PPGroups 'EconomicGroup 'SecurityGroup)
  Identity
  NonNegativeInterval
cppMinFeeRefScriptCostPerByte :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD
     ('PPGroups 'EconomicGroup 'SecurityGroup) f NonNegativeInterval
cppDRepActivity :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD ('PPGroups 'GovGroup 'NoStakePoolGroup) f EpochInterval
cppDRepDeposit :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD
     ('PPGroups 'GovGroup 'NoStakePoolGroup) f (CompactForm Coin)
cppGovActionDeposit :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD ('PPGroups 'GovGroup 'SecurityGroup) f Coin
cppGovActionLifetime :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD ('PPGroups 'GovGroup 'NoStakePoolGroup) f EpochInterval
cppCommitteeMaxTermLength :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD ('PPGroups 'GovGroup 'NoStakePoolGroup) f EpochInterval
cppCommitteeMinSize :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD ('PPGroups 'GovGroup 'NoStakePoolGroup) f Word16
cppDRepVotingThresholds :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD
     ('PPGroups 'GovGroup 'NoStakePoolGroup) f DRepVotingThresholds
cppPoolVotingThresholds :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD
     ('PPGroups 'GovGroup 'NoStakePoolGroup) f PoolVotingThresholds
cppMaxCollateralInputs :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD ('PPGroups 'NetworkGroup 'NoStakePoolGroup) f Word16
cppCollateralPercentage :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD ('PPGroups 'TechnicalGroup 'NoStakePoolGroup) f Word16
cppMaxValSize :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD ('PPGroups 'NetworkGroup 'SecurityGroup) f Word32
cppMaxBlockExUnits :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD ('PPGroups 'NetworkGroup 'SecurityGroup) f OrdExUnits
cppMaxTxExUnits :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD ('PPGroups 'NetworkGroup 'NoStakePoolGroup) f OrdExUnits
cppPrices :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD ('PPGroups 'EconomicGroup 'NoStakePoolGroup) f Prices
cppCostModels :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD ('PPGroups 'TechnicalGroup 'NoStakePoolGroup) f CostModels
cppCoinsPerUTxOByte :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD ('PPGroups 'EconomicGroup 'SecurityGroup) f CoinPerByte
cppMinPoolCost :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD ('PPGroups 'EconomicGroup 'NoStakePoolGroup) f Coin
cppProtocolVersion :: forall (f :: * -> *) era.
ConwayPParams f era -> HKDNoUpdate f ProtVer
cppTau :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD ('PPGroups 'EconomicGroup 'NoStakePoolGroup) f UnitInterval
cppRho :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD ('PPGroups 'EconomicGroup 'NoStakePoolGroup) f UnitInterval
cppA0 :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD
     ('PPGroups 'TechnicalGroup 'NoStakePoolGroup) f NonNegativeInterval
cppNOpt :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD ('PPGroups 'TechnicalGroup 'NoStakePoolGroup) f Word16
cppEMax :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD
     ('PPGroups 'TechnicalGroup 'NoStakePoolGroup) f EpochInterval
cppPoolDeposit :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD
     ('PPGroups 'EconomicGroup 'NoStakePoolGroup) f (CompactForm Coin)
cppKeyDeposit :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD ('PPGroups 'EconomicGroup 'NoStakePoolGroup) f Coin
cppMaxBHSize :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD ('PPGroups 'NetworkGroup 'SecurityGroup) f Word16
cppMaxTxSize :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD ('PPGroups 'NetworkGroup 'SecurityGroup) f Word32
cppMaxBBSize :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD ('PPGroups 'NetworkGroup 'SecurityGroup) f Word32
cppMinFeeB :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD ('PPGroups 'EconomicGroup 'SecurityGroup) f Coin
cppMinFeeA :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD ('PPGroups 'EconomicGroup 'SecurityGroup) f Coin
..} = do
    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
    ppB <- toSpecRep cppMinFeeB
    ppA0 <- toSpecRep cppA0
    ppMinFeeRefScriptCoinsPerByte <- toSpecRep cppMinFeeRefScriptCostPerByte
    ppCollateralPercentage <- toSpecRep cppCollateralPercentage
    let
      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 = 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 = 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
    ppKeyDeposit <- toSpecRep cppKeyDeposit
    ppPoolDeposit <- toSpecRep cppPoolDeposit
    ppEmax <- toSpecRep cppEMax
    ppNopt <- toSpecRep (toInteger $ unTHKD 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
0, Integer
0)
      ppMinUTxOValue = Integer
0 -- minUTxOValue has been deprecated and is not supported in Conway
    ppCoinsPerUTxOByte <- toSpecRep cppCoinsPerUTxOByte
    ppCostmdls <- toSpecRep cppCostModels
    ppPrices <- toSpecRep cppPrices
    let
      pp = PParamsHKD Identity era -> PParams era
forall era. PParamsHKD Identity era -> PParams era
PParams PParamsHKD Identity era
ConwayPParams Identity era
cpp
      ppMaxRefScriptSizePerTx = Word32 -> Integer
forall a. Integral a => a -> Integer
toInteger (Word32 -> Integer) -> Word32 -> Integer
forall a b. (a -> b) -> a -> b
$ PParams era
pp PParams era -> Getting Word32 (PParams era) Word32 -> Word32
forall s a. s -> Getting a s a -> a
^. Getting Word32 (PParams era) Word32
forall era.
ConwayEraPParams era =>
SimpleGetter (PParams era) Word32
SimpleGetter (PParams era) Word32
ppMaxRefScriptSizePerTxG
      ppMaxRefScriptSizePerBlock = Word32 -> Integer
forall a. Integral a => a -> Integer
toInteger (Word32 -> Integer) -> Word32 -> Integer
forall a b. (a -> b) -> a -> b
$ PParams era
pp PParams era -> Getting Word32 (PParams era) Word32 -> Word32
forall s a. s -> Getting a s a -> a
^. Getting Word32 (PParams era) Word32
forall era.
ConwayEraPParams era =>
SimpleGetter (PParams era) Word32
SimpleGetter (PParams era) Word32
ppMaxRefScriptSizePerBlockG
      ppRefScriptCostStride = Word32 -> Integer
forall a. Integral a => a -> Integer
toInteger (Word32 -> Integer)
-> (NonZero Word32 -> Word32) -> NonZero Word32 -> Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NonZero Word32 -> Word32
forall a. NonZero a -> a
unNonZero (NonZero Word32 -> Integer) -> NonZero Word32 -> Integer
forall a b. (a -> b) -> a -> b
$ PParams era
pp PParams era
-> Getting (NonZero Word32) (PParams era) (NonZero Word32)
-> NonZero Word32
forall s a. s -> Getting a s a -> a
^. Getting (NonZero Word32) (PParams era) (NonZero Word32)
forall era.
ConwayEraPParams era =>
SimpleGetter (PParams era) (NonZero Word32)
SimpleGetter (PParams era) (NonZero Word32)
ppRefScriptCostStrideG
      ppRefScriptCostMultiplier = PositiveInterval -> Rational
forall r. BoundedRational r => r -> Rational
unboundRational (PositiveInterval -> Rational) -> PositiveInterval -> Rational
forall a b. (a -> b) -> a -> b
$ PParams era
pp PParams era
-> Getting PositiveInterval (PParams era) PositiveInterval
-> PositiveInterval
forall s a. s -> Getting a s a -> a
^. Getting PositiveInterval (PParams era) PositiveInterval
forall era.
ConwayEraPParams era =>
SimpleGetter (PParams era) PositiveInterval
SimpleGetter (PParams era) PositiveInterval
ppRefScriptCostMultiplierG
    ppMaxTxExUnits <- toSpecRep cppMaxTxExUnits
    ppMaxBlockExUnits <- toSpecRep cppMaxBlockExUnits
    let
      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 = 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
    ppPoolThresholds <- toSpecRep cppPoolVotingThresholds
    ppDrepThresholds <- toSpecRep cppDRepVotingThresholds
    let
      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 = 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
    ppGovActionLifetime <- toSpecRep cppGovActionLifetime
    ppGovActionDeposit <- toSpecRep cppGovActionDeposit
    ppDrepDeposit <- toSpecRep cppDRepDeposit
    ppDrepActivity <- toSpecRep cppDRepActivity
    ppMonetaryExpansion <- toSpecRep cppRho
    ppTreasuryCut <- toSpecRep cppTau

    pure Agda.MkPParams {..}

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 Era era => SpecTranslate ctx (TxDats era) where
  type SpecRep (TxDats era) = Agda.HSSet Agda.Datum

  toSpecRep :: TxDats era -> SpecTransM ctx (SpecRep (TxDats era))
toSpecRep = ([Integer] -> HSSet Integer)
-> SpecTransM ctx [Integer] -> SpecTransM ctx (HSSet 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 [Integer] -> HSSet Integer
forall a. [a] -> HSSet a
Agda.MkHSSet (SpecTransM ctx [Integer] -> SpecTransM ctx (HSSet Integer))
-> (TxDats era -> SpecTransM ctx [Integer])
-> TxDats era
-> SpecTransM ctx (HSSet Integer)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((DataHash, Data era) -> SpecTransM ctx Integer)
-> [(DataHash, Data era)] -> SpecTransM ctx [Integer]
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 (Data era -> SpecTransM ctx Integer
Data era -> SpecTransM ctx (SpecRep (Data era))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep (Data era -> SpecTransM ctx Integer)
-> ((DataHash, Data era) -> Data era)
-> (DataHash, Data era)
-> SpecTransM ctx Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (DataHash, Data era) -> Data era
forall a b. (a, b) -> b
snd) ([(DataHash, Data era)] -> SpecTransM ctx [Integer])
-> (TxDats era -> [(DataHash, Data era)])
-> TxDats era
-> SpecTransM ctx [Integer]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Map DataHash (Data era) -> [(DataHash, Data era)]
forall k a. Map k a -> [(k, a)]
Map.toList (Map DataHash (Data era) -> [(DataHash, Data era)])
-> (TxDats era -> Map DataHash (Data era))
-> TxDats era
-> [(DataHash, Data era)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TxDats era -> Map DataHash (Data era)
forall era. TxDats era -> Map DataHash (Data era)
unTxDats

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
  ( 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)
-> HSSet Integer
-> HSMap (Tag, Integer) (Integer, ExUnits)
-> TxWitnesses
Agda.MkTxWitnesses
      (HSMap HSVKey Integer
 -> HSSet (Either HSTimelock HSPlutusScript)
 -> HSSet Integer
 -> HSMap (Tag, Integer) (Integer, ExUnits)
 -> TxWitnesses)
-> SpecTransM ctx (HSMap HSVKey Integer)
-> SpecTransM
     ctx
     (HSSet (Either HSTimelock HSPlutusScript)
      -> HSSet Integer
      -> HSMap (Tag, Integer) (Integer, ExUnits)
      -> 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)
   -> HSSet Integer
   -> HSMap (Tag, Integer) (Integer, ExUnits)
   -> TxWitnesses)
-> SpecTransM ctx (HSSet (Either HSTimelock HSPlutusScript))
-> SpecTransM
     ctx
     (HSSet Integer
      -> HSMap (Tag, Integer) (Integer, ExUnits) -> 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
  (HSSet Integer
   -> HSMap (Tag, Integer) (Integer, ExUnits) -> TxWitnesses)
-> SpecTransM ctx (HSSet Integer)
-> SpecTransM
     ctx (HSMap (Tag, Integer) (Integer, ExUnits) -> 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, ExUnits) -> TxWitnesses)
-> SpecTransM ctx (HSMap (Tag, Integer) (Integer, ExUnits))
-> 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 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 StakePoolParams where
  type SpecRep StakePoolParams = Agda.StakePoolParams

  toSpecRep :: StakePoolParams -> SpecTransM ctx (SpecRep StakePoolParams)
toSpecRep StakePoolParams {Set (KeyHash Staking)
StrictMaybe PoolMetadata
KeyHash StakePool
VRFVerKeyHash StakePoolVRF
RewardAccount
Coin
UnitInterval
StrictSeq StakePoolRelay
sppId :: KeyHash StakePool
sppVrf :: VRFVerKeyHash StakePoolVRF
sppPledge :: Coin
sppCost :: Coin
sppMargin :: UnitInterval
sppRewardAccount :: RewardAccount
sppOwners :: Set (KeyHash Staking)
sppRelays :: StrictSeq StakePoolRelay
sppMetadata :: StrictMaybe PoolMetadata
sppCost :: StakePoolParams -> Coin
sppId :: StakePoolParams -> KeyHash StakePool
sppMargin :: StakePoolParams -> UnitInterval
sppMetadata :: StakePoolParams -> StrictMaybe PoolMetadata
sppOwners :: StakePoolParams -> Set (KeyHash Staking)
sppPledge :: StakePoolParams -> Coin
sppRelays :: StakePoolParams -> StrictSeq StakePoolRelay
sppRewardAccount :: StakePoolParams -> RewardAccount
sppVrf :: StakePoolParams -> VRFVerKeyHash StakePoolVRF
..} =
    HSSet Integer
-> Integer -> Rational -> Integer -> Credential -> StakePoolParams
Agda.StakePoolParams
      (HSSet Integer
 -> Integer -> Rational -> Integer -> Credential -> StakePoolParams)
-> SpecTransM ctx (HSSet Integer)
-> SpecTransM
     ctx
     (Integer -> Rational -> Integer -> Credential -> StakePoolParams)
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)
sppOwners
      SpecTransM
  ctx
  (Integer -> Rational -> Integer -> Credential -> StakePoolParams)
-> SpecTransM ctx Integer
-> SpecTransM
     ctx (Rational -> Integer -> Credential -> StakePoolParams)
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
sppCost
      SpecTransM
  ctx (Rational -> Integer -> Credential -> StakePoolParams)
-> SpecTransM ctx Rational
-> SpecTransM ctx (Integer -> Credential -> StakePoolParams)
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
sppMargin
      SpecTransM ctx (Integer -> Credential -> StakePoolParams)
-> SpecTransM ctx Integer
-> SpecTransM ctx (Credential -> StakePoolParams)
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
sppPledge
      SpecTransM ctx (Credential -> StakePoolParams)
-> SpecTransM ctx Credential -> SpecTransM ctx StakePoolParams
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
<*> Credential Staking -> SpecTransM ctx (SpecRep (Credential Staking))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep (RewardAccount -> Credential Staking
raCredential RewardAccount
sppRewardAccount)

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

  toSpecRep :: DRep -> SpecTransM ctx (SpecRep DRep)
toSpecRep (DRepCredential Credential DRepRole
c) = Credential -> VDeleg
Agda.VDelegCredential (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.VDelegAbstain
  toSpecRep DRep
DRepAlwaysNoConfidence = VDeleg -> SpecTransM ctx VDeleg
forall a. a -> SpecTransM ctx a
forall (f :: * -> *) a. Applicative f => a -> f a
pure VDeleg
Agda.VDelegNoConfidence

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 Withdrawals where
  type SpecRep Withdrawals = Agda.Withdrawals

  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 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 (GovPurposeId r) where
  type SpecRep (GovPurposeId r) = (Agda.TxId, Integer)

  toSpecRep :: GovPurposeId r -> SpecTransM ctx (SpecRep (GovPurposeId r))
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 (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 (Credential Staking) Coin
StrictMaybe (Committee era)
PParams era
Constitution era
GovRelation StrictMaybe
Coin
ensCommittee :: StrictMaybe (Committee era)
ensConstitution :: Constitution era
ensCurPParams :: PParams era
ensPrevPParams :: PParams era
ensTreasury :: Coin
ensWithdrawals :: Map (Credential Staking) Coin
ensPrevGovActionIds :: GovRelation StrictMaybe
ensPrevGovActionIds :: forall era. EnactState era -> GovRelation StrictMaybe
ensWithdrawals :: forall era. EnactState era -> Map (Credential Staking) Coin
ensTreasury :: forall era. EnactState era -> Coin
ensPrevPParams :: forall era. EnactState era -> PParams era
ensCurPParams :: forall era. EnactState era -> PParams era
ensConstitution :: forall era. EnactState era -> Constitution era
ensCommittee :: forall era. EnactState era -> StrictMaybe (Committee era)
..} =
    (Maybe (HSMap Credential Integer, Rational), ExUnits)
-> ((Integer, Maybe Integer), ExUnits)
-> (ExUnits, ExUnits)
-> (PParams, ExUnits)
-> HSMap RwdAddr Integer
-> EnactState
Agda.MkEnactState
      ((Maybe (HSMap Credential Integer, Rational), ExUnits)
 -> ((Integer, Maybe Integer), ExUnits)
 -> (ExUnits, ExUnits)
 -> (PParams, ExUnits)
 -> HSMap RwdAddr Integer
 -> EnactState)
-> SpecTransM
     ctx (Maybe (HSMap Credential Integer, Rational), ExUnits)
-> SpecTransM
     ctx
     (((Integer, Maybe Integer), ExUnits)
      -> (ExUnits, ExUnits)
      -> (PParams, ExUnits)
      -> HSMap RwdAddr Integer
      -> EnactState)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StrictMaybe (Committee era)
-> StrictMaybe (GovPurposeId 'CommitteePurpose)
-> SpecTransM ctx (SpecRep (StrictMaybe (Committee era)), ExUnits)
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)
grCommittee
      SpecTransM
  ctx
  (((Integer, Maybe Integer), ExUnits)
   -> (ExUnits, ExUnits)
   -> (PParams, ExUnits)
   -> HSMap RwdAddr Integer
   -> EnactState)
-> SpecTransM ctx ((Integer, Maybe Integer), ExUnits)
-> SpecTransM
     ctx
     ((ExUnits, ExUnits)
      -> (PParams, ExUnits) -> 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)
-> SpecTransM ctx (SpecRep (Constitution era), ExUnits)
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)
grConstitution
      SpecTransM
  ctx
  ((ExUnits, ExUnits)
   -> (PParams, ExUnits) -> HSMap RwdAddr Integer -> EnactState)
-> SpecTransM ctx (ExUnits, ExUnits)
-> SpecTransM
     ctx ((PParams, ExUnits) -> 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)
-> SpecTransM ctx (SpecRep ProtVer, ExUnits)
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)
grHardFork
      SpecTransM
  ctx ((PParams, ExUnits) -> HSMap RwdAddr Integer -> EnactState)
-> SpecTransM ctx (PParams, ExUnits)
-> 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)
-> SpecTransM ctx (SpecRep (PParams era), ExUnits)
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)
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 (Credential Staking) 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 (Credential Staking) Coin
ensWithdrawals
    where
      GovRelation {StrictMaybe (GovPurposeId 'PParamUpdatePurpose)
StrictMaybe (GovPurposeId 'HardForkPurpose)
StrictMaybe (GovPurposeId 'CommitteePurpose)
StrictMaybe (GovPurposeId 'ConstitutionPurpose)
grCommittee :: StrictMaybe (GovPurposeId 'CommitteePurpose)
grConstitution :: StrictMaybe (GovPurposeId 'ConstitutionPurpose)
grHardFork :: StrictMaybe (GovPurposeId 'HardForkPurpose)
grPParamUpdate :: StrictMaybe (GovPurposeId 'PParamUpdatePurpose)
grConstitution :: forall (f :: * -> *).
GovRelation f -> f (GovPurposeId 'ConstitutionPurpose)
grCommittee :: forall (f :: * -> *).
GovRelation f -> f (GovPurposeId 'CommitteePurpose)
grHardFork :: forall (f :: * -> *).
GovRelation f -> f (GovPurposeId 'HardForkPurpose)
grPParamUpdate :: forall (f :: * -> *).
GovRelation f -> f (GovPurposeId 'PParamUpdatePurpose)
..} = GovRelation StrictMaybe
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
          agdaCred <- a -> SpecTransM ctx (SpecRep a)
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep a
cred
          network <- toSpecRep Testnet -- TODO where should this really come from?
          pure (Agda.RwdAddr network agdaCred, amount)
      transHashProtected :: a -> StrictMaybe a -> SpecTransM ctx (SpecRep a, (a, b))
transHashProtected a
x StrictMaybe a
h = do
        committee <- a -> SpecTransM ctx (SpecRep a)
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep a
x
        agdaLastId <- case 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)
        pure (committee, agdaLastId)

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

  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
<$> ( ExUnits -> (GovRole, Credential) -> Vote -> Maybe Anchor -> GovVote
Agda.MkGovVote
                  (ExUnits
 -> (GovRole, Credential) -> Vote -> Maybe Anchor -> GovVote)
-> SpecTransM ctx ExUnits
-> 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 (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
  (CompactForm 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
  DRepVotingThresholds
THKD
  ('PPGroups 'GovGroup 'NoStakePoolGroup)
  StrictMaybe
  PoolVotingThresholds
THKD
  ('PPGroups 'GovGroup 'NoStakePoolGroup) StrictMaybe EpochInterval
THKD
  ('PPGroups 'GovGroup 'NoStakePoolGroup)
  StrictMaybe
  (CompactForm Coin)
HKDNoUpdate StrictMaybe ProtVer
cppMinFeeRefScriptCostPerByte :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD
     ('PPGroups 'EconomicGroup 'SecurityGroup) f NonNegativeInterval
cppDRepActivity :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD ('PPGroups 'GovGroup 'NoStakePoolGroup) f EpochInterval
cppDRepDeposit :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD
     ('PPGroups 'GovGroup 'NoStakePoolGroup) f (CompactForm Coin)
cppGovActionDeposit :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD ('PPGroups 'GovGroup 'SecurityGroup) f Coin
cppGovActionLifetime :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD ('PPGroups 'GovGroup 'NoStakePoolGroup) f EpochInterval
cppCommitteeMaxTermLength :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD ('PPGroups 'GovGroup 'NoStakePoolGroup) f EpochInterval
cppCommitteeMinSize :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD ('PPGroups 'GovGroup 'NoStakePoolGroup) f Word16
cppDRepVotingThresholds :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD
     ('PPGroups 'GovGroup 'NoStakePoolGroup) f DRepVotingThresholds
cppPoolVotingThresholds :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD
     ('PPGroups 'GovGroup 'NoStakePoolGroup) f PoolVotingThresholds
cppMaxCollateralInputs :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD ('PPGroups 'NetworkGroup 'NoStakePoolGroup) f Word16
cppCollateralPercentage :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD ('PPGroups 'TechnicalGroup 'NoStakePoolGroup) f Word16
cppMaxValSize :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD ('PPGroups 'NetworkGroup 'SecurityGroup) f Word32
cppMaxBlockExUnits :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD ('PPGroups 'NetworkGroup 'SecurityGroup) f OrdExUnits
cppMaxTxExUnits :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD ('PPGroups 'NetworkGroup 'NoStakePoolGroup) f OrdExUnits
cppPrices :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD ('PPGroups 'EconomicGroup 'NoStakePoolGroup) f Prices
cppCostModels :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD ('PPGroups 'TechnicalGroup 'NoStakePoolGroup) f CostModels
cppCoinsPerUTxOByte :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD ('PPGroups 'EconomicGroup 'SecurityGroup) f CoinPerByte
cppMinPoolCost :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD ('PPGroups 'EconomicGroup 'NoStakePoolGroup) f Coin
cppProtocolVersion :: forall (f :: * -> *) era.
ConwayPParams f era -> HKDNoUpdate f ProtVer
cppTau :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD ('PPGroups 'EconomicGroup 'NoStakePoolGroup) f UnitInterval
cppRho :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD ('PPGroups 'EconomicGroup 'NoStakePoolGroup) f UnitInterval
cppA0 :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD
     ('PPGroups 'TechnicalGroup 'NoStakePoolGroup) f NonNegativeInterval
cppNOpt :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD ('PPGroups 'TechnicalGroup 'NoStakePoolGroup) f Word16
cppEMax :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD
     ('PPGroups 'TechnicalGroup 'NoStakePoolGroup) f EpochInterval
cppPoolDeposit :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD
     ('PPGroups 'EconomicGroup 'NoStakePoolGroup) f (CompactForm Coin)
cppKeyDeposit :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD ('PPGroups 'EconomicGroup 'NoStakePoolGroup) f Coin
cppMaxBHSize :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD ('PPGroups 'NetworkGroup 'SecurityGroup) f Word16
cppMaxTxSize :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD ('PPGroups 'NetworkGroup 'SecurityGroup) f Word32
cppMaxBBSize :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD ('PPGroups 'NetworkGroup 'SecurityGroup) f Word32
cppMinFeeB :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD ('PPGroups 'EconomicGroup 'SecurityGroup) f Coin
cppMinFeeA :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD ('PPGroups 'EconomicGroup 'SecurityGroup) f Coin
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
  (CompactForm 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
  (CompactForm Coin)
cppDRepActivity :: THKD
  ('PPGroups 'GovGroup 'NoStakePoolGroup) StrictMaybe EpochInterval
cppMinFeeRefScriptCostPerByte :: THKD
  ('PPGroups 'EconomicGroup 'SecurityGroup)
  StrictMaybe
  NonNegativeInterval
..}) = do
    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
    ppuB <- toSpecRep cppMinFeeB
    ppuA0 <- toSpecRep cppA0
    ppuMinFeeRefScriptCoinsPerByte <- toSpecRep cppMinFeeRefScriptCostPerByte
    ppuCollateralPercentage <- toSpecRep cppCollateralPercentage
    let
      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 = (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 = (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
    ppuKeyDeposit <- toSpecRep cppKeyDeposit
    ppuPoolDeposit <- toSpecRep cppPoolDeposit
    ppuEmax <- toSpecRep cppEMax
    ppuNopt <- toSpecRep (fmap toInteger . strictMaybeToMaybe $ unTHKD cppNOpt)
    let
      ppuPv = Maybe a
forall a. Maybe a
Nothing
      ppuMinUTxOValue = Maybe a
forall a. Maybe a
Nothing -- minUTxOValue has been deprecated and is not supported in Conway
    ppuCoinsPerUTxOByte <- toSpecRep cppCoinsPerUTxOByte
    ppuCostmdls <- toSpecRep cppCostModels
    ppuPrices <- toSpecRep cppPrices
    let
      ppuMaxRefScriptSizePerTx = Maybe a
forall a. Maybe a
Nothing
      ppuMaxRefScriptSizePerBlock = Maybe a
forall a. Maybe a
Nothing
      ppuRefScriptCostStride = Maybe a
forall a. Maybe a
Nothing
      ppuRefScriptCostMultiplier = Maybe a
forall a. Maybe a
Nothing
    ppuMaxTxExUnits <- toSpecRep cppMaxTxExUnits
    ppuMaxBlockExUnits <- toSpecRep cppMaxBlockExUnits
    let
      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 = (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
    ppuPoolThresholds <- toSpecRep cppPoolVotingThresholds
    ppuDrepThresholds <- toSpecRep cppDRepVotingThresholds
    let
      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 =
        (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
    ppuGovActionLifetime <- toSpecRep cppGovActionLifetime
    ppuGovActionDeposit <- toSpecRep cppGovActionDeposit
    ppuDrepDeposit <- toSpecRep cppDRepDeposit
    ppuDrepActivity <- toSpecRep cppDRepActivity
    ppuMonetaryExpansion <- toSpecRep cppRho
    ppuTreasuryCut <- toSpecRep cppTau

    pure Agda.MkPParamsUpdate {..}

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)
_ 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)
_ ProtVer
pv) = ExUnits -> GovAction
Agda.TriggerHardFork (ExUnits -> GovAction)
-> SpecTransM ctx ExUnits -> 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.TreasuryWithdrawal
      (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)
_) = 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)
_ 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)
_ (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
  ( 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
pProcAnchor :: forall era. ProposalProcedure era -> Anchor
pProcGovAction :: forall era. ProposalProcedure era -> GovAction era
pProcReturnAddr :: forall era. ProposalProcedure era -> RewardAccount
pProcDeposit :: forall era. ProposalProcedure era -> Coin
..} =
    GovAction
-> ExUnits
-> Maybe Integer
-> Integer
-> RwdAddr
-> Anchor
-> GovProposal
Agda.MkGovProposal
      (GovAction
 -> ExUnits
 -> Maybe Integer
 -> Integer
 -> RwdAddr
 -> Anchor
 -> GovProposal)
-> SpecTransM ctx GovAction
-> SpecTransM
     ctx
     (ExUnits
      -> 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
  (ExUnits
   -> Maybe Integer -> Integer -> RwdAddr -> Anchor -> GovProposal)
-> SpecTransM ctx ExUnits
-> 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)
_ 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)
x PParamsUpdate era
_ StrictMaybe ScriptHash
_ -> GovPurposeId 'PParamUpdatePurpose -> GovActionId
forall (p :: GovActionPurpose). GovPurposeId p -> GovActionId
unGovPurposeId (GovPurposeId 'PParamUpdatePurpose -> GovActionId)
-> StrictMaybe (GovPurposeId 'PParamUpdatePurpose)
-> StrictMaybe GovActionId
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StrictMaybe (GovPurposeId 'PParamUpdatePurpose)
x
    HardForkInitiation StrictMaybe (GovPurposeId 'HardForkPurpose)
x ProtVer
_ -> GovPurposeId 'HardForkPurpose -> GovActionId
forall (p :: GovActionPurpose). GovPurposeId p -> GovActionId
unGovPurposeId (GovPurposeId 'HardForkPurpose -> GovActionId)
-> StrictMaybe (GovPurposeId 'HardForkPurpose)
-> StrictMaybe GovActionId
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StrictMaybe (GovPurposeId 'HardForkPurpose)
x
    UpdateCommittee StrictMaybe (GovPurposeId 'CommitteePurpose)
x Set (Credential ColdCommitteeRole)
_ Map (Credential ColdCommitteeRole) EpochNo
_ UnitInterval
_ -> GovPurposeId 'CommitteePurpose -> GovActionId
forall (p :: GovActionPurpose). GovPurposeId p -> GovActionId
unGovPurposeId (GovPurposeId 'CommitteePurpose -> GovActionId)
-> StrictMaybe (GovPurposeId 'CommitteePurpose)
-> StrictMaybe GovActionId
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StrictMaybe (GovPurposeId 'CommitteePurpose)
x
    NoConfidence StrictMaybe (GovPurposeId 'CommitteePurpose)
x -> GovPurposeId 'CommitteePurpose -> GovActionId
forall (p :: GovActionPurpose). GovPurposeId p -> GovActionId
unGovPurposeId (GovPurposeId 'CommitteePurpose -> GovActionId)
-> StrictMaybe (GovPurposeId 'CommitteePurpose)
-> StrictMaybe GovActionId
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StrictMaybe (GovPurposeId 'CommitteePurpose)
x
    NewConstitution StrictMaybe (GovPurposeId 'ConstitutionPurpose)
x Constitution era
_ -> GovPurposeId 'ConstitutionPurpose -> GovActionId
forall (p :: GovActionPurpose). GovPurposeId p -> GovActionId
unGovPurposeId (GovPurposeId 'ConstitutionPurpose -> GovActionId)
-> StrictMaybe (GovPurposeId 'ConstitutionPurpose)
-> StrictMaybe GovActionId
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StrictMaybe (GovPurposeId 'ConstitutionPurpose)
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

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
gasExpiresAfter :: forall era. GovActionState era -> EpochNo
gasProposedIn :: forall era. GovActionState era -> EpochNo
gasProposalProcedure :: forall era. GovActionState era -> ProposalProcedure era
gasStakePoolVotes :: forall era. GovActionState era -> Map (KeyHash StakePool) Vote
gasDRepVotes :: forall era. GovActionState era -> Map (Credential DRepRole) Vote
gasCommitteeVotes :: forall era.
GovActionState era -> Map (Credential HotCommitteeRole) Vote
gasId :: forall era. GovActionState era -> GovActionId
..} = do
    GovVotes
-> RwdAddr -> Integer -> GovAction -> ExUnits -> GovActionState
Agda.MkGovActionState
      (GovVotes
 -> RwdAddr -> Integer -> GovAction -> ExUnits -> GovActionState)
-> SpecTransM ctx GovVotes
-> SpecTransM
     ctx (RwdAddr -> Integer -> GovAction -> ExUnits -> GovActionState)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ( HSMap Credential Vote
-> HSMap Credential Vote -> HSMap Integer Vote -> GovVotes
Agda.GovVotes
              (HSMap Credential Vote
 -> HSMap Credential Vote -> HSMap Integer Vote -> GovVotes)
-> SpecTransM ctx (HSMap Credential Vote)
-> SpecTransM
     ctx (HSMap Credential Vote -> HSMap Integer Vote -> GovVotes)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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
              SpecTransM
  ctx (HSMap Credential Vote -> HSMap Integer Vote -> GovVotes)
-> SpecTransM ctx (HSMap Credential Vote)
-> SpecTransM ctx (HSMap Integer Vote -> GovVotes)
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 (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
              SpecTransM ctx (HSMap Integer Vote -> GovVotes)
-> SpecTransM ctx (HSMap Integer Vote) -> SpecTransM ctx GovVotes
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) 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
          )
      SpecTransM
  ctx (RwdAddr -> Integer -> GovAction -> ExUnits -> GovActionState)
-> SpecTransM ctx RwdAddr
-> SpecTransM
     ctx (Integer -> GovAction -> ExUnits -> 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 -> ExUnits -> GovActionState)
-> SpecTransM ctx Integer
-> SpecTransM ctx (GovAction -> ExUnits -> 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 -> ExUnits -> GovActionState)
-> SpecTransM ctx GovAction
-> SpecTransM ctx (ExUnits -> 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 (ExUnits -> GovActionState)
-> SpecTransM ctx ExUnits -> 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

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 [(ExUnits, 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 [(ExUnits, GovActionState)])
-> (Proposals era -> OMap GovActionId (GovActionState era))
-> Proposals era
-> SpecTransM ctx [(ExUnits, 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
  (Inject ctx Coin, ConwayEraAccounts era) =>
  SpecTranslate ctx (RatifyEnv era)
  where
  type SpecRep (RatifyEnv era) = Agda.RatifyEnv

  toSpecRep :: RatifyEnv era -> SpecTransM ctx (SpecRep (RatifyEnv era))
toSpecRep RatifyEnv {Map (KeyHash StakePool) StakePoolState
Map DRep (CompactForm Coin)
Map (Credential DRepRole) DRepState
Accounts era
CommitteeState era
PoolDistr
InstantStake era
EpochNo
reInstantStake :: InstantStake era
reStakePoolDistr :: PoolDistr
reDRepDistr :: Map DRep (CompactForm Coin)
reDRepState :: Map (Credential DRepRole) DRepState
reCurrentEpoch :: EpochNo
reCommitteeState :: CommitteeState era
reAccounts :: Accounts era
reStakePools :: Map (KeyHash StakePool) StakePoolState
reStakePools :: forall era. RatifyEnv era -> Map (KeyHash StakePool) StakePoolState
reAccounts :: forall era. RatifyEnv era -> Accounts era
reCommitteeState :: forall era. RatifyEnv era -> CommitteeState era
reCurrentEpoch :: forall era. RatifyEnv era -> EpochNo
reDRepState :: forall era. RatifyEnv era -> Map (Credential DRepRole) DRepState
reDRepDistr :: forall era. RatifyEnv era -> Map DRep (CompactForm Coin)
reStakePoolDistr :: forall era. RatifyEnv era -> PoolDistr
reInstantStake :: forall era. RatifyEnv era -> InstantStake era
..} = do
    let
      stakeDistrs :: SpecTransM ctx StakeDistrs
stakeDistrs =
        HSMap VDeleg Integer -> HSMap Integer Integer -> StakeDistrs
Agda.StakeDistrs
          (HSMap VDeleg Integer -> HSMap Integer Integer -> StakeDistrs)
-> SpecTransM ctx (HSMap VDeleg Integer)
-> SpecTransM ctx (HSMap Integer Integer -> StakeDistrs)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Map DRep (CompactForm Coin)
-> SpecTransM ctx (SpecRep (Map DRep (CompactForm Coin)))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep Map DRep (CompactForm Coin)
reDRepDistr
          SpecTransM ctx (HSMap Integer Integer -> StakeDistrs)
-> SpecTransM ctx (HSMap Integer Integer)
-> SpecTransM ctx StakeDistrs
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
<*> PoolDistr -> SpecTransM ctx (SpecRep PoolDistr)
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep PoolDistr
reStakePoolDistr
      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
    treasury <- forall b ctx. Inject ctx b => SpecTransM ctx b
askCtx @Coin
    Agda.MkRatifyEnv
      <$> stakeDistrs
      <*> toSpecRep reCurrentEpoch
      <*> dreps
      <*> toSpecRep reCommitteeState
      <*> toSpecRep treasury
      <*> toSpecRep (Map.mapWithKey stakePoolStateToStakePoolParams reStakePools)
      <*> toSpecRep (Map.mapMaybe (^. dRepDelegationAccountStateL) (reAccounts ^. accountsMapL))

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
rsDelayed :: forall era. RatifyState era -> Bool
rsExpired :: forall era. RatifyState era -> Set GovActionId
rsEnacted :: forall era. RatifyState era -> Seq (GovActionState era)
rsEnactState :: forall era. RatifyState era -> EnactState era
..} = do
    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
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"
    removed <-
      Set.foldr'
        lookupGAS
        (pure Set.empty)
        (rsExpired `Set.union` Set.fromList (gasId <$> toList rsEnacted))
    Agda.MkRatifyState
      <$> toSpecRep rsEnactState
      <*> toSpecRep removed
      <*> toSpecRep 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