{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE NamedFieldPuns #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TupleSections #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -Wno-orphans #-}
module Test.Cardano.Ledger.Conformance.SpecTranslate.Conway.Base (
committeeCredentialToStrictMaybe,
SpecTranslate (..),
SpecTranslationError,
ConwayExecEnactEnv (..),
DepositPurpose (..),
ConwayTxBodyTransContext (..),
vkeyToInteger,
vkeyFromInteger,
signatureToInteger,
signatureFromInteger,
) where
import Cardano.Crypto.DSIGN (DSIGNAlgorithm (..), SignedDSIGN (..))
import Cardano.Crypto.Util (bytesToNatural, naturalToBytes)
import Cardano.Ledger.Address (Addr (..), BootstrapAddress (..), RewardAccount (..))
import Cardano.Ledger.Allegra.Scripts (
Timelock,
pattern RequireTimeExpire,
pattern RequireTimeStart,
)
import Cardano.Ledger.Alonzo (AlonzoTxAuxData, MaryValue)
import Cardano.Ledger.Alonzo.PParams (OrdExUnits (OrdExUnits))
import Cardano.Ledger.Alonzo.Scripts (AlonzoPlutusPurpose (..))
import Cardano.Ledger.Alonzo.Tx (AlonzoTx (..), IsValid (..))
import Cardano.Ledger.Alonzo.TxWits (AlonzoTxWits (..), Redeemers (..), TxDats (..))
import Cardano.Ledger.Babbage.TxOut (BabbageTxOut (..))
import Cardano.Ledger.BaseTypes
import Cardano.Ledger.Binary (Sized (..))
import Cardano.Ledger.Coin (Coin (..), CompactForm)
import Cardano.Ledger.Compactible (Compactible)
import Cardano.Ledger.Conway.Core
import Cardano.Ledger.Conway.Governance
import Cardano.Ledger.Conway.PParams (ConwayPParams (..), THKD (..))
import Cardano.Ledger.Conway.Rules (
ConwayCertPredFailure,
ConwayGovPredFailure,
EnactSignal (..),
maxRefScriptSizePerBlock,
maxRefScriptSizePerTx,
)
import Cardano.Ledger.Conway.Scripts (AlonzoScript (..), ConwayPlutusPurpose (..))
import Cardano.Ledger.Conway.Tx (refScriptCostMultiplier, refScriptCostStride)
import Cardano.Ledger.Credential (Credential (..), StakeReference (..))
import Cardano.Ledger.DRep (DRep (..), DRepState (..))
import Cardano.Ledger.HKD (HKD)
import Cardano.Ledger.Keys (VKey (..))
import Cardano.Ledger.Keys.WitVKey (WitVKey (..))
import Cardano.Ledger.Plutus (CostModels, ExUnits (..), Prices)
import Cardano.Ledger.Plutus.Data (BinaryData, Data, Datum (..), hashBinaryData)
import Cardano.Ledger.PoolParams (PoolParams (..))
import Cardano.Ledger.Shelley.Rules (Identity)
import Cardano.Ledger.Shelley.Scripts (
pattern RequireAllOf,
pattern RequireAnyOf,
pattern RequireMOf,
pattern RequireSignature,
)
import Cardano.Ledger.State (
CommitteeAuthorization (..),
CommitteeState (..),
IndividualPoolStake (..),
PoolDistr (..),
UTxO (..),
)
import Cardano.Ledger.TxIn (TxId (..), TxIn (..))
import Cardano.Ledger.UMap (fromCompact)
import Cardano.Ledger.Val (Val (..))
import Constrained.API (HasSimpleRep, HasSpec)
import Control.DeepSeq (NFData)
import Control.Monad.Except (MonadError (..))
import Control.State.Transition.Extended (STS (..))
import Data.Bifunctor (Bifunctor (..))
import Data.Bitraversable (bimapM)
import Data.Default (Default (..))
import Data.Foldable (Foldable (..))
import Data.List (sortOn)
import Data.Map.Strict (Map)
import qualified Data.Map.Strict as Map
import Data.OMap.Strict (OMap)
import qualified Data.OMap.Strict as OMap
import Data.OSet.Strict (OSet)
import Data.Sequence (Seq)
import Data.Sequence.Strict (StrictSeq)
import Data.Set (Set)
import qualified Data.Set as Set
import qualified Data.Text as T
import Data.Traversable (forM)
import Data.Void (Void, absurd)
import Data.Word (Word16, Word32, Word64)
import qualified GHC.Exts as Exts
import GHC.Generics (Generic)
import Lens.Micro
import Lens.Micro.Extras (view)
import qualified MAlonzo.Code.Ledger.Foreign.API as Agda
import Test.Cardano.Ledger.Conformance (
OpaqueErrorString (..),
SpecTransM,
SpecTranslate (..),
SpecTranslationError,
askCtx,
hashToInteger,
showOpaqueErrorString,
withCtx,
)
import Test.Cardano.Ledger.Constrained.Conway (DepositPurpose (..))
import Test.Cardano.Ledger.Constrained.Conway.Epoch
import Test.Cardano.Ledger.Conway.TreeDiff (ToExpr (..), showExpr)
instance SpecTranslate ctx Void where
type SpecRep Void = Void
toSpecRep :: Void -> SpecTransM ctx (SpecRep Void)
toSpecRep = Void -> SpecTransM ctx Void
Void -> SpecTransM ctx (SpecRep Void)
forall a. Void -> a
absurd
instance SpecTranslate ctx a => SpecTranslate ctx [a] where
type SpecRep [a] = [SpecRep a]
toSpecRep :: [a] -> SpecTransM ctx (SpecRep [a])
toSpecRep = (a -> SpecTransM ctx (SpecRep a))
-> [a] -> SpecTransM ctx [SpecRep a]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse a -> SpecTransM ctx (SpecRep a)
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep
instance SpecTranslate ctx TxIx where
type SpecRep TxIx = Integer
toSpecRep :: TxIx -> SpecTransM ctx (SpecRep TxIx)
toSpecRep (TxIx Word16
x) = Integer -> SpecTransM ctx Integer
forall a. a -> SpecTransM ctx a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Integer -> SpecTransM ctx Integer)
-> Integer -> SpecTransM ctx Integer
forall a b. (a -> b) -> a -> b
$ Word16 -> Integer
forall a. Integral a => a -> Integer
toInteger Word16
x
instance SpecTranslate ctx TxIn where
type SpecRep TxIn = Agda.TxIn
toSpecRep :: TxIn -> SpecTransM ctx (SpecRep TxIn)
toSpecRep (TxIn TxId
txId TxIx
txIx) = (TxId, TxIx) -> SpecTransM ctx (SpecRep (TxId, TxIx))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep (TxId
txId, TxIx
txIx)
instance SpecTranslate ctx StakeReference where
type SpecRep StakeReference = Maybe Agda.Credential
toSpecRep :: StakeReference -> SpecTransM ctx (SpecRep StakeReference)
toSpecRep (StakeRefBase StakeCredential
c) = Credential -> Maybe Credential
forall a. a -> Maybe a
Just (Credential -> Maybe Credential)
-> SpecTransM ctx Credential -> SpecTransM ctx (Maybe Credential)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StakeCredential -> SpecTransM ctx (SpecRep StakeCredential)
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep StakeCredential
c
toSpecRep (StakeRefPtr Ptr
_) = Maybe Credential -> SpecTransM ctx (Maybe Credential)
forall a. a -> SpecTransM ctx a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe Credential
forall a. Maybe a
Nothing
toSpecRep StakeReference
StakeRefNull = Maybe Credential -> SpecTransM ctx (Maybe Credential)
forall a. a -> SpecTransM ctx a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe Credential
forall a. Maybe a
Nothing
instance SpecTranslate ctx BootstrapAddress where
type SpecRep BootstrapAddress = Agda.BootstrapAddr
toSpecRep :: BootstrapAddress -> SpecTransM ctx (SpecRep BootstrapAddress)
toSpecRep BootstrapAddress
_ = [Char] -> SpecTransM ctx BootstrapAddr
forall a. HasCallStack => [Char] -> a
error [Char]
"Cannot translate bootstrap addresses"
instance SpecTranslate ctx Addr where
type SpecRep Addr = Agda.Addr
toSpecRep :: Addr -> SpecTransM ctx (SpecRep Addr)
toSpecRep (Addr Network
nw PaymentCredential
pc StakeReference
sr) =
BaseAddr -> Either BaseAddr BootstrapAddr
forall a b. a -> Either a b
Left
(BaseAddr -> Either BaseAddr BootstrapAddr)
-> SpecTransM ctx BaseAddr
-> SpecTransM ctx (Either BaseAddr BootstrapAddr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Integer -> Credential -> Maybe Credential -> BaseAddr
Agda.BaseAddr (Integer -> Credential -> Maybe Credential -> BaseAddr)
-> SpecTransM ctx Integer
-> SpecTransM ctx (Credential -> Maybe Credential -> BaseAddr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Network -> SpecTransM ctx (SpecRep Network)
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep Network
nw SpecTransM ctx (Credential -> Maybe Credential -> BaseAddr)
-> SpecTransM ctx Credential
-> SpecTransM ctx (Maybe Credential -> BaseAddr)
forall a b.
SpecTransM ctx (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> PaymentCredential -> SpecTransM ctx (SpecRep PaymentCredential)
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep PaymentCredential
pc SpecTransM ctx (Maybe Credential -> BaseAddr)
-> SpecTransM ctx (Maybe Credential) -> SpecTransM ctx BaseAddr
forall a b.
SpecTransM ctx (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> StakeReference -> SpecTransM ctx (SpecRep StakeReference)
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep StakeReference
sr)
toSpecRep (AddrBootstrap BootstrapAddress
ba) = BootstrapAddr -> Either BaseAddr BootstrapAddr
forall a b. b -> Either a b
Right (BootstrapAddr -> Either BaseAddr BootstrapAddr)
-> SpecTransM ctx BootstrapAddr
-> SpecTransM ctx (Either BaseAddr BootstrapAddr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> BootstrapAddress -> SpecTransM ctx (SpecRep BootstrapAddress)
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep BootstrapAddress
ba
instance SpecTranslate ctx (Hash a b) where
type SpecRep (Hash a b) = Integer
toSpecRep :: Hash a b -> SpecTransM ctx (SpecRep (Hash a b))
toSpecRep = Integer -> SpecTransM ctx Integer
forall a. a -> SpecTransM ctx a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Integer -> SpecTransM ctx Integer)
-> (Hash a b -> Integer) -> Hash a b -> SpecTransM ctx Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Hash a b -> Integer
forall a b. Hash a b -> Integer
hashToInteger
instance SpecTranslate ctx (SafeHash a) where
type SpecRep (SafeHash a) = Agda.DataHash
toSpecRep :: SafeHash a -> SpecTransM ctx (SpecRep (SafeHash a))
toSpecRep = Hash HASH a -> SpecTransM ctx Integer
Hash HASH a -> SpecTransM ctx (SpecRep (Hash HASH a))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep (Hash HASH a -> SpecTransM ctx Integer)
-> (SafeHash a -> Hash HASH a)
-> SafeHash a
-> SpecTransM ctx Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SafeHash a -> Hash HASH a
forall i. SafeHash i -> Hash HASH i
extractHash
instance
( SpecRep DataHash ~ Agda.DataHash
, Era era
) =>
SpecTranslate ctx (BinaryData era)
where
type SpecRep (BinaryData era) = Agda.DataHash
toSpecRep :: BinaryData era -> SpecTransM ctx (SpecRep (BinaryData era))
toSpecRep = DataHash -> SpecTransM ctx Integer
DataHash -> SpecTransM ctx (SpecRep DataHash)
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep (DataHash -> SpecTransM ctx Integer)
-> (BinaryData era -> DataHash)
-> BinaryData era
-> SpecTransM ctx Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BinaryData era -> DataHash
forall era. BinaryData era -> DataHash
hashBinaryData
instance Era era => SpecTranslate ctx (Datum era) where
type SpecRep (Datum era) = Maybe (Either Agda.Datum Agda.DataHash)
toSpecRep :: Datum era -> SpecTransM ctx (SpecRep (Datum era))
toSpecRep Datum era
NoDatum = Maybe (Either Integer Integer)
-> SpecTransM ctx (Maybe (Either Integer Integer))
forall a. a -> SpecTransM ctx a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe (Either Integer Integer)
forall a. Maybe a
Nothing
toSpecRep (Datum BinaryData era
d) = Either Integer Integer -> Maybe (Either Integer Integer)
forall a. a -> Maybe a
Just (Either Integer Integer -> Maybe (Either Integer Integer))
-> (Integer -> Either Integer Integer)
-> Integer
-> Maybe (Either Integer Integer)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> Either Integer Integer
forall a b. a -> Either a b
Left (Integer -> Maybe (Either Integer Integer))
-> SpecTransM ctx Integer
-> SpecTransM ctx (Maybe (Either Integer Integer))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> BinaryData era -> SpecTransM ctx (SpecRep (BinaryData era))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep BinaryData era
d
toSpecRep (DatumHash DataHash
h) = Either Integer Integer -> Maybe (Either Integer Integer)
forall a. a -> Maybe a
Just (Either Integer Integer -> Maybe (Either Integer Integer))
-> (Integer -> Either Integer Integer)
-> Integer
-> Maybe (Either Integer Integer)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> Either Integer Integer
forall a b. b -> Either a b
Right (Integer -> Maybe (Either Integer Integer))
-> SpecTransM ctx Integer
-> SpecTransM ctx (Maybe (Either Integer Integer))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> DataHash -> SpecTransM ctx (SpecRep DataHash)
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep DataHash
h
instance
( AlonzoEraScript era
, NativeScript era ~ Timelock era
, Script era ~ AlonzoScript era
) =>
SpecTranslate ctx (Timelock era)
where
type SpecRep (Timelock era) = Agda.HSTimelock
toSpecRep :: Timelock era -> SpecTransM ctx (SpecRep (Timelock era))
toSpecRep Timelock era
tl =
Timelock -> Integer -> Integer -> HSTimelock
Agda.HSTimelock
(Timelock -> Integer -> Integer -> HSTimelock)
-> SpecTransM ctx Timelock
-> SpecTransM ctx (Integer -> Integer -> HSTimelock)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NativeScript era -> SpecTransM ctx Timelock
forall {era} {ctx}.
(Assert
(OrdCond
(CmpNat (ProtVerLow era) (ProtVerHigh era)) 'True 'True 'False)
(TypeError ...),
Assert
(OrdCond (CmpNat 0 (ProtVerLow era)) 'True 'True 'False)
(TypeError ...),
Assert
(OrdCond (CmpNat 0 (ProtVerHigh era)) 'True 'True 'False)
(TypeError ...),
AllegraEraScript era) =>
NativeScript era -> SpecTransM ctx Timelock
timelockToSpecRep Timelock era
NativeScript era
tl
SpecTransM ctx (Integer -> Integer -> HSTimelock)
-> SpecTransM ctx Integer -> SpecTransM ctx (Integer -> HSTimelock)
forall a b.
SpecTransM ctx (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ScriptHash -> SpecTransM ctx (SpecRep ScriptHash)
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep (forall era. EraScript era => Script era -> ScriptHash
hashScript @era (Script era -> ScriptHash) -> Script era -> ScriptHash
forall a b. (a -> b) -> a -> b
$ Timelock era -> AlonzoScript era
forall era. Timelock era -> AlonzoScript era
TimelockScript Timelock era
tl)
SpecTransM ctx (Integer -> HSTimelock)
-> SpecTransM ctx Integer -> SpecTransM ctx HSTimelock
forall a b.
SpecTransM ctx (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Integer -> SpecTransM ctx Integer
forall a. a -> SpecTransM ctx a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Int -> Integer) -> Int -> Integer
forall a b. (a -> b) -> a -> b
$ Timelock era -> Int
forall t. SafeToHash t => t -> Int
originalBytesSize Timelock era
tl)
where
timelockToSpecRep :: NativeScript era -> SpecTransM ctx Timelock
timelockToSpecRep NativeScript era
x =
case NativeScript era
x of
RequireSignature KeyHash 'Witness
kh ->
Integer -> Timelock
Agda.RequireSig (Integer -> Timelock)
-> SpecTransM ctx Integer -> SpecTransM ctx Timelock
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> KeyHash 'Witness -> SpecTransM ctx (SpecRep (KeyHash 'Witness))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep KeyHash 'Witness
kh
RequireAllOf StrictSeq (NativeScript era)
ss -> do
StrictSeq Timelock
tls <- (NativeScript era -> SpecTransM ctx Timelock)
-> StrictSeq (NativeScript era)
-> SpecTransM ctx (StrictSeq Timelock)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> StrictSeq a -> f (StrictSeq b)
traverse NativeScript era -> SpecTransM ctx Timelock
timelockToSpecRep StrictSeq (NativeScript era)
ss
Timelock -> SpecTransM ctx Timelock
forall a. a -> SpecTransM ctx a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Timelock -> SpecTransM ctx Timelock)
-> ([Timelock] -> Timelock)
-> [Timelock]
-> SpecTransM ctx Timelock
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Timelock] -> Timelock
Agda.RequireAllOf ([Timelock] -> SpecTransM ctx Timelock)
-> [Timelock] -> SpecTransM ctx Timelock
forall a b. (a -> b) -> a -> b
$ StrictSeq Timelock -> [Timelock]
forall a. StrictSeq a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList StrictSeq Timelock
tls
RequireAnyOf StrictSeq (NativeScript era)
ss -> do
StrictSeq Timelock
tls <- (NativeScript era -> SpecTransM ctx Timelock)
-> StrictSeq (NativeScript era)
-> SpecTransM ctx (StrictSeq Timelock)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> StrictSeq a -> f (StrictSeq b)
traverse NativeScript era -> SpecTransM ctx Timelock
timelockToSpecRep StrictSeq (NativeScript era)
ss
Timelock -> SpecTransM ctx Timelock
forall a. a -> SpecTransM ctx a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Timelock -> SpecTransM ctx Timelock)
-> ([Timelock] -> Timelock)
-> [Timelock]
-> SpecTransM ctx Timelock
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Timelock] -> Timelock
Agda.RequireAnyOf ([Timelock] -> SpecTransM ctx Timelock)
-> [Timelock] -> SpecTransM ctx Timelock
forall a b. (a -> b) -> a -> b
$ StrictSeq Timelock -> [Timelock]
forall a. StrictSeq a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList StrictSeq Timelock
tls
RequireMOf Int
m StrictSeq (NativeScript era)
ss -> do
StrictSeq Timelock
tls <- (NativeScript era -> SpecTransM ctx Timelock)
-> StrictSeq (NativeScript era)
-> SpecTransM ctx (StrictSeq Timelock)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> StrictSeq a -> f (StrictSeq b)
traverse NativeScript era -> SpecTransM ctx Timelock
timelockToSpecRep StrictSeq (NativeScript era)
ss
Timelock -> SpecTransM ctx Timelock
forall a. a -> SpecTransM ctx a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Timelock -> SpecTransM ctx Timelock)
-> ([Timelock] -> Timelock)
-> [Timelock]
-> SpecTransM ctx Timelock
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> [Timelock] -> Timelock
Agda.RequireMOf (Int -> Integer
forall a. Integral a => a -> Integer
toInteger Int
m) ([Timelock] -> SpecTransM ctx Timelock)
-> [Timelock] -> SpecTransM ctx Timelock
forall a b. (a -> b) -> a -> b
$ StrictSeq Timelock -> [Timelock]
forall a. StrictSeq a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList StrictSeq Timelock
tls
RequireTimeExpire SlotNo
slot -> Integer -> Timelock
Agda.RequireTimeExpire (Integer -> Timelock)
-> SpecTransM ctx Integer -> SpecTransM ctx Timelock
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SlotNo -> SpecTransM ctx (SpecRep SlotNo)
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep SlotNo
slot
RequireTimeStart SlotNo
slot -> Integer -> Timelock
Agda.RequireTimeStart (Integer -> Timelock)
-> SpecTransM ctx Integer -> SpecTransM ctx Timelock
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SlotNo -> SpecTransM ctx (SpecRep SlotNo)
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep SlotNo
slot
instance
( AlonzoEraScript era
, NativeScript era ~ Timelock era
, Script era ~ AlonzoScript era
) =>
SpecTranslate ctx (PlutusScript era)
where
type SpecRep (PlutusScript era) = Agda.HSPlutusScript
toSpecRep :: PlutusScript era -> SpecTransM ctx (SpecRep (PlutusScript era))
toSpecRep PlutusScript era
ps =
Integer -> Integer -> HSPlutusScript
Agda.MkHSPlutusScript
(Integer -> Integer -> HSPlutusScript)
-> SpecTransM ctx Integer
-> SpecTransM ctx (Integer -> HSPlutusScript)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ScriptHash -> SpecTransM ctx (SpecRep ScriptHash)
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep (Script era -> ScriptHash
forall era. EraScript era => Script era -> ScriptHash
hashScript (Script era -> ScriptHash) -> Script era -> ScriptHash
forall a b. (a -> b) -> a -> b
$ PlutusScript era -> AlonzoScript era
forall era. PlutusScript era -> AlonzoScript era
PlutusScript PlutusScript era
ps)
SpecTransM ctx (Integer -> HSPlutusScript)
-> SpecTransM ctx Integer -> SpecTransM ctx HSPlutusScript
forall a b.
SpecTransM ctx (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Integer -> SpecTransM ctx Integer
forall a. a -> SpecTransM ctx a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Int -> Integer) -> Int -> Integer
forall a b. (a -> b) -> a -> b
$ PlutusScript era -> Int
forall t. SafeToHash t => t -> Int
originalBytesSize PlutusScript era
ps)
instance
( AlonzoEraScript era
, Script era ~ AlonzoScript era
, NativeScript era ~ Timelock era
) =>
SpecTranslate ctx (AlonzoScript era)
where
type SpecRep (AlonzoScript era) = Agda.Script
toSpecRep :: AlonzoScript era -> SpecTransM ctx (SpecRep (AlonzoScript era))
toSpecRep (TimelockScript Timelock era
s) = HSTimelock -> Either HSTimelock HSPlutusScript
forall a b. a -> Either a b
Left (HSTimelock -> Either HSTimelock HSPlutusScript)
-> SpecTransM ctx HSTimelock
-> SpecTransM ctx (Either HSTimelock HSPlutusScript)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Timelock era -> SpecTransM ctx (SpecRep (Timelock era))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep Timelock era
s
toSpecRep (PlutusScript PlutusScript era
s) = HSPlutusScript -> Either HSTimelock HSPlutusScript
forall a b. b -> Either a b
Right (HSPlutusScript -> Either HSTimelock HSPlutusScript)
-> SpecTransM ctx HSPlutusScript
-> SpecTransM ctx (Either HSTimelock HSPlutusScript)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> PlutusScript era -> SpecTransM ctx (SpecRep (PlutusScript era))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep PlutusScript era
s
instance
( EraTxOut era
, SpecRep (Value era) ~ Agda.Coin
, Script era ~ AlonzoScript era
, SpecTranslate ctx (Value era)
, SpecTranslate ctx (Script era)
) =>
SpecTranslate ctx (BabbageTxOut era)
where
type SpecRep (BabbageTxOut era) = Agda.TxOut
toSpecRep :: BabbageTxOut era -> SpecTransM ctx (SpecRep (BabbageTxOut era))
toSpecRep (BabbageTxOut Addr
addr Value era
val Datum era
datum StrictMaybe (Script era)
script) = do
Either BaseAddr BootstrapAddr
addr' <- Addr -> SpecTransM ctx (SpecRep Addr)
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep Addr
addr
Integer
val' <- Value era -> SpecTransM ctx (SpecRep (Value era))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep Value era
val
Maybe (Either Integer Integer)
datum' <- Datum era -> SpecTransM ctx (SpecRep (Datum era))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep Datum era
datum
Maybe (Either HSTimelock HSPlutusScript)
script' <- StrictMaybe (AlonzoScript era)
-> SpecTransM ctx (SpecRep (StrictMaybe (AlonzoScript era)))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep StrictMaybe (Script era)
StrictMaybe (AlonzoScript era)
script
(Either BaseAddr BootstrapAddr,
(Integer,
(Maybe (Either Integer Integer),
Maybe (Either HSTimelock HSPlutusScript))))
-> SpecTransM
ctx
(Either BaseAddr BootstrapAddr,
(Integer,
(Maybe (Either Integer Integer),
Maybe (Either HSTimelock HSPlutusScript))))
forall a. a -> SpecTransM ctx a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Either BaseAddr BootstrapAddr
addr', (Integer
val', (Maybe (Either Integer Integer)
datum', Maybe (Either HSTimelock HSPlutusScript)
script')))
instance SpecTranslate ctx Integer where
type SpecRep Integer = Integer
toSpecRep :: Integer -> SpecTransM ctx (SpecRep Integer)
toSpecRep = Integer -> SpecTransM ctx Integer
Integer -> SpecTransM ctx (SpecRep Integer)
forall a. a -> SpecTransM ctx a
forall (f :: * -> *) a. Applicative f => a -> f a
pure
deriving instance SpecTranslate ctx Coin
instance
( SpecTranslate ctx (TxOut era)
, SpecRep (TxOut era) ~ Agda.TxOut
) =>
SpecTranslate ctx (UTxO era)
where
type SpecRep (UTxO era) = SpecRep (Map TxIn (TxOut era))
toSpecRep :: UTxO era -> SpecTransM ctx (SpecRep (UTxO era))
toSpecRep (UTxO Map TxIn (TxOut era)
m) = Map TxIn (TxOut era)
-> SpecTransM ctx (SpecRep (Map TxIn (TxOut era)))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep Map TxIn (TxOut era)
m
deriving instance SpecTranslate ctx SlotNo
deriving instance SpecTranslate ctx EpochNo
deriving instance SpecTranslate ctx EpochInterval
instance SpecTranslate ctx ProtVer where
type SpecRep ProtVer = (Integer, Integer)
toSpecRep :: ProtVer -> SpecTransM ctx (SpecRep ProtVer)
toSpecRep (ProtVer Version
ver Nat
minor) = (Integer, Integer) -> SpecTransM ctx (Integer, Integer)
forall a. a -> SpecTransM ctx a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Version -> Integer
forall i. Integral i => Version -> i
getVersion Version
ver, Nat -> Integer
forall a. Integral a => a -> Integer
toInteger Nat
minor)
instance SpecTranslate ctx CostModels where
type SpecRep CostModels = ()
toSpecRep :: CostModels -> SpecTransM ctx (SpecRep CostModels)
toSpecRep CostModels
_ = () -> SpecTransM ctx ()
forall a. a -> SpecTransM ctx a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
instance SpecTranslate ctx Prices where
type SpecRep Prices = ()
toSpecRep :: Prices -> SpecTransM ctx (SpecRep Prices)
toSpecRep Prices
_ = () -> SpecTransM ctx ()
forall a. a -> SpecTransM ctx a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
instance SpecTranslate ctx ExUnits where
type SpecRep ExUnits = Agda.ExUnits
toSpecRep :: ExUnits -> SpecTransM ctx (SpecRep ExUnits)
toSpecRep (ExUnits Nat
a Nat
b) = (Integer, Integer) -> SpecTransM ctx (Integer, Integer)
forall a. a -> SpecTransM ctx a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Nat -> Integer
forall a. Integral a => a -> Integer
toInteger Nat
a, Nat -> Integer
forall a. Integral a => a -> Integer
toInteger Nat
b)
deriving instance SpecTranslate ctx OrdExUnits
deriving instance SpecTranslate ctx CoinPerByte
instance
SpecTranslate ctx (HKD f a) =>
SpecTranslate ctx (THKD r f a)
where
type SpecRep (THKD r f a) = SpecRep (HKD f a)
toSpecRep :: THKD r f a -> SpecTransM ctx (SpecRep (THKD r f a))
toSpecRep = HKD f a -> SpecTransM ctx (SpecRep (HKD f a))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep (HKD f a -> SpecTransM ctx (SpecRep (HKD f a)))
-> (THKD r f a -> HKD f a)
-> THKD r f a
-> SpecTransM ctx (SpecRep (HKD f a))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. THKD r f a -> HKD f a
forall (t :: PPGroups) (f :: * -> *) a. THKD t f a -> HKD f a
unTHKD
instance SpecTranslate ctx DRepVotingThresholds where
type SpecRep DRepVotingThresholds = Agda.DrepThresholds
toSpecRep :: DRepVotingThresholds
-> SpecTransM ctx (SpecRep DRepVotingThresholds)
toSpecRep DRepVotingThresholds {UnitInterval
dvtMotionNoConfidence :: UnitInterval
dvtCommitteeNormal :: UnitInterval
dvtCommitteeNoConfidence :: UnitInterval
dvtUpdateToConstitution :: UnitInterval
dvtHardForkInitiation :: UnitInterval
dvtPPNetworkGroup :: UnitInterval
dvtPPEconomicGroup :: UnitInterval
dvtPPTechnicalGroup :: UnitInterval
dvtPPGovGroup :: UnitInterval
dvtTreasuryWithdrawal :: UnitInterval
dvtMotionNoConfidence :: DRepVotingThresholds -> UnitInterval
dvtCommitteeNormal :: DRepVotingThresholds -> UnitInterval
dvtCommitteeNoConfidence :: DRepVotingThresholds -> UnitInterval
dvtUpdateToConstitution :: DRepVotingThresholds -> UnitInterval
dvtHardForkInitiation :: DRepVotingThresholds -> UnitInterval
dvtPPNetworkGroup :: DRepVotingThresholds -> UnitInterval
dvtPPEconomicGroup :: DRepVotingThresholds -> UnitInterval
dvtPPTechnicalGroup :: DRepVotingThresholds -> UnitInterval
dvtPPGovGroup :: DRepVotingThresholds -> UnitInterval
dvtTreasuryWithdrawal :: DRepVotingThresholds -> UnitInterval
..} =
Rational
-> Rational
-> Rational
-> Rational
-> Rational
-> Rational
-> Rational
-> Rational
-> Rational
-> Rational
-> DrepThresholds
Agda.MkDrepThresholds
(Rational
-> Rational
-> Rational
-> Rational
-> Rational
-> Rational
-> Rational
-> Rational
-> Rational
-> Rational
-> DrepThresholds)
-> SpecTransM ctx Rational
-> SpecTransM
ctx
(Rational
-> Rational
-> Rational
-> Rational
-> Rational
-> Rational
-> Rational
-> Rational
-> Rational
-> DrepThresholds)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> UnitInterval -> SpecTransM ctx (SpecRep UnitInterval)
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep UnitInterval
dvtMotionNoConfidence
SpecTransM
ctx
(Rational
-> Rational
-> Rational
-> Rational
-> Rational
-> Rational
-> Rational
-> Rational
-> Rational
-> DrepThresholds)
-> SpecTransM ctx Rational
-> SpecTransM
ctx
(Rational
-> Rational
-> Rational
-> Rational
-> Rational
-> Rational
-> Rational
-> Rational
-> DrepThresholds)
forall a b.
SpecTransM ctx (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> UnitInterval -> SpecTransM ctx (SpecRep UnitInterval)
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep UnitInterval
dvtCommitteeNormal
SpecTransM
ctx
(Rational
-> Rational
-> Rational
-> Rational
-> Rational
-> Rational
-> Rational
-> Rational
-> DrepThresholds)
-> SpecTransM ctx Rational
-> SpecTransM
ctx
(Rational
-> Rational
-> Rational
-> Rational
-> Rational
-> Rational
-> Rational
-> DrepThresholds)
forall a b.
SpecTransM ctx (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> UnitInterval -> SpecTransM ctx (SpecRep UnitInterval)
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep UnitInterval
dvtCommitteeNoConfidence
SpecTransM
ctx
(Rational
-> Rational
-> Rational
-> Rational
-> Rational
-> Rational
-> Rational
-> DrepThresholds)
-> SpecTransM ctx Rational
-> SpecTransM
ctx
(Rational
-> Rational
-> Rational
-> Rational
-> Rational
-> Rational
-> DrepThresholds)
forall a b.
SpecTransM ctx (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> UnitInterval -> SpecTransM ctx (SpecRep UnitInterval)
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep UnitInterval
dvtUpdateToConstitution
SpecTransM
ctx
(Rational
-> Rational
-> Rational
-> Rational
-> Rational
-> Rational
-> DrepThresholds)
-> SpecTransM ctx Rational
-> SpecTransM
ctx
(Rational
-> Rational -> Rational -> Rational -> Rational -> DrepThresholds)
forall a b.
SpecTransM ctx (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> UnitInterval -> SpecTransM ctx (SpecRep UnitInterval)
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep UnitInterval
dvtHardForkInitiation
SpecTransM
ctx
(Rational
-> Rational -> Rational -> Rational -> Rational -> DrepThresholds)
-> SpecTransM ctx Rational
-> SpecTransM
ctx
(Rational -> Rational -> Rational -> Rational -> DrepThresholds)
forall a b.
SpecTransM ctx (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> UnitInterval -> SpecTransM ctx (SpecRep UnitInterval)
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep UnitInterval
dvtPPNetworkGroup
SpecTransM
ctx
(Rational -> Rational -> Rational -> Rational -> DrepThresholds)
-> SpecTransM ctx Rational
-> SpecTransM
ctx (Rational -> Rational -> Rational -> DrepThresholds)
forall a b.
SpecTransM ctx (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> UnitInterval -> SpecTransM ctx (SpecRep UnitInterval)
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep UnitInterval
dvtPPEconomicGroup
SpecTransM ctx (Rational -> Rational -> Rational -> DrepThresholds)
-> SpecTransM ctx Rational
-> SpecTransM ctx (Rational -> Rational -> DrepThresholds)
forall a b.
SpecTransM ctx (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> UnitInterval -> SpecTransM ctx (SpecRep UnitInterval)
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep UnitInterval
dvtPPTechnicalGroup
SpecTransM ctx (Rational -> Rational -> DrepThresholds)
-> SpecTransM ctx Rational
-> SpecTransM ctx (Rational -> DrepThresholds)
forall a b.
SpecTransM ctx (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> UnitInterval -> SpecTransM ctx (SpecRep UnitInterval)
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep UnitInterval
dvtPPGovGroup
SpecTransM ctx (Rational -> DrepThresholds)
-> SpecTransM ctx Rational -> SpecTransM ctx DrepThresholds
forall a b.
SpecTransM ctx (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> UnitInterval -> SpecTransM ctx (SpecRep UnitInterval)
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep UnitInterval
dvtTreasuryWithdrawal
instance SpecTranslate ctx PoolVotingThresholds where
type SpecRep PoolVotingThresholds = Agda.PoolThresholds
toSpecRep :: PoolVotingThresholds
-> SpecTransM ctx (SpecRep PoolVotingThresholds)
toSpecRep PoolVotingThresholds {UnitInterval
pvtMotionNoConfidence :: UnitInterval
pvtCommitteeNormal :: UnitInterval
pvtCommitteeNoConfidence :: UnitInterval
pvtHardForkInitiation :: UnitInterval
pvtPPSecurityGroup :: UnitInterval
pvtMotionNoConfidence :: PoolVotingThresholds -> UnitInterval
pvtCommitteeNormal :: PoolVotingThresholds -> UnitInterval
pvtCommitteeNoConfidence :: PoolVotingThresholds -> UnitInterval
pvtHardForkInitiation :: PoolVotingThresholds -> UnitInterval
pvtPPSecurityGroup :: PoolVotingThresholds -> UnitInterval
..} =
Rational
-> Rational -> Rational -> Rational -> Rational -> PoolThresholds
Agda.MkPoolThresholds
(Rational
-> Rational -> Rational -> Rational -> Rational -> PoolThresholds)
-> SpecTransM ctx Rational
-> SpecTransM
ctx
(Rational -> Rational -> Rational -> Rational -> PoolThresholds)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> UnitInterval -> SpecTransM ctx (SpecRep UnitInterval)
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep UnitInterval
pvtMotionNoConfidence
SpecTransM
ctx
(Rational -> Rational -> Rational -> Rational -> PoolThresholds)
-> SpecTransM ctx Rational
-> SpecTransM
ctx (Rational -> Rational -> Rational -> PoolThresholds)
forall a b.
SpecTransM ctx (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> UnitInterval -> SpecTransM ctx (SpecRep UnitInterval)
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep UnitInterval
pvtCommitteeNormal
SpecTransM ctx (Rational -> Rational -> Rational -> PoolThresholds)
-> SpecTransM ctx Rational
-> SpecTransM ctx (Rational -> Rational -> PoolThresholds)
forall a b.
SpecTransM ctx (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> UnitInterval -> SpecTransM ctx (SpecRep UnitInterval)
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep UnitInterval
pvtCommitteeNoConfidence
SpecTransM ctx (Rational -> Rational -> PoolThresholds)
-> SpecTransM ctx Rational
-> SpecTransM ctx (Rational -> PoolThresholds)
forall a b.
SpecTransM ctx (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> UnitInterval -> SpecTransM ctx (SpecRep UnitInterval)
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep UnitInterval
pvtHardForkInitiation
SpecTransM ctx (Rational -> PoolThresholds)
-> SpecTransM ctx Rational -> SpecTransM ctx PoolThresholds
forall a b.
SpecTransM ctx (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> UnitInterval -> SpecTransM ctx (SpecRep UnitInterval)
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep UnitInterval
pvtPPSecurityGroup
instance SpecTranslate ctx (ConwayPParams Identity era) where
type SpecRep (ConwayPParams Identity era) = Agda.PParams
toSpecRep :: ConwayPParams Identity era
-> SpecTransM ctx (SpecRep (ConwayPParams Identity era))
toSpecRep ConwayPParams {THKD ('PPGroups 'NetworkGroup 'SecurityGroup) Identity Word16
THKD ('PPGroups 'NetworkGroup 'SecurityGroup) Identity Word32
THKD ('PPGroups 'NetworkGroup 'SecurityGroup) Identity OrdExUnits
THKD ('PPGroups 'NetworkGroup 'NoStakePoolGroup) Identity Word16
THKD
('PPGroups 'NetworkGroup 'NoStakePoolGroup) Identity OrdExUnits
THKD ('PPGroups 'EconomicGroup 'SecurityGroup) Identity CoinPerByte
THKD ('PPGroups 'EconomicGroup 'SecurityGroup) Identity Coin
THKD
('PPGroups 'EconomicGroup 'SecurityGroup)
Identity
NonNegativeInterval
THKD ('PPGroups 'EconomicGroup 'NoStakePoolGroup) Identity Prices
THKD ('PPGroups 'EconomicGroup 'NoStakePoolGroup) Identity Coin
THKD
('PPGroups 'EconomicGroup 'NoStakePoolGroup) Identity UnitInterval
THKD ('PPGroups 'TechnicalGroup 'NoStakePoolGroup) Identity Word16
THKD
('PPGroups 'TechnicalGroup 'NoStakePoolGroup) Identity CostModels
THKD
('PPGroups 'TechnicalGroup 'NoStakePoolGroup)
Identity
EpochInterval
THKD
('PPGroups 'TechnicalGroup 'NoStakePoolGroup)
Identity
NonNegativeInterval
THKD ('PPGroups 'GovGroup 'SecurityGroup) Identity Coin
THKD ('PPGroups 'GovGroup 'NoStakePoolGroup) Identity Word16
THKD ('PPGroups 'GovGroup 'NoStakePoolGroup) Identity Coin
THKD
('PPGroups 'GovGroup 'NoStakePoolGroup)
Identity
DRepVotingThresholds
THKD
('PPGroups 'GovGroup 'NoStakePoolGroup)
Identity
PoolVotingThresholds
THKD ('PPGroups 'GovGroup 'NoStakePoolGroup) Identity EpochInterval
HKDNoUpdate Identity ProtVer
cppMinFeeA :: THKD ('PPGroups 'EconomicGroup 'SecurityGroup) Identity Coin
cppMinFeeB :: THKD ('PPGroups 'EconomicGroup 'SecurityGroup) Identity Coin
cppMaxBBSize :: THKD ('PPGroups 'NetworkGroup 'SecurityGroup) Identity Word32
cppMaxTxSize :: THKD ('PPGroups 'NetworkGroup 'SecurityGroup) Identity Word32
cppMaxBHSize :: THKD ('PPGroups 'NetworkGroup 'SecurityGroup) Identity Word16
cppKeyDeposit :: THKD ('PPGroups 'EconomicGroup 'NoStakePoolGroup) Identity Coin
cppPoolDeposit :: THKD ('PPGroups 'EconomicGroup 'NoStakePoolGroup) Identity Coin
cppEMax :: THKD
('PPGroups 'TechnicalGroup 'NoStakePoolGroup)
Identity
EpochInterval
cppNOpt :: THKD ('PPGroups 'TechnicalGroup 'NoStakePoolGroup) Identity Word16
cppA0 :: THKD
('PPGroups 'TechnicalGroup 'NoStakePoolGroup)
Identity
NonNegativeInterval
cppRho :: THKD
('PPGroups 'EconomicGroup 'NoStakePoolGroup) Identity UnitInterval
cppTau :: THKD
('PPGroups 'EconomicGroup 'NoStakePoolGroup) Identity UnitInterval
cppProtocolVersion :: HKDNoUpdate Identity ProtVer
cppMinPoolCost :: THKD ('PPGroups 'EconomicGroup 'NoStakePoolGroup) Identity Coin
cppCoinsPerUTxOByte :: THKD ('PPGroups 'EconomicGroup 'SecurityGroup) Identity CoinPerByte
cppCostModels :: THKD
('PPGroups 'TechnicalGroup 'NoStakePoolGroup) Identity CostModels
cppPrices :: THKD ('PPGroups 'EconomicGroup 'NoStakePoolGroup) Identity Prices
cppMaxTxExUnits :: THKD
('PPGroups 'NetworkGroup 'NoStakePoolGroup) Identity OrdExUnits
cppMaxBlockExUnits :: THKD ('PPGroups 'NetworkGroup 'SecurityGroup) Identity OrdExUnits
cppMaxValSize :: THKD ('PPGroups 'NetworkGroup 'SecurityGroup) Identity Word32
cppCollateralPercentage :: THKD ('PPGroups 'TechnicalGroup 'NoStakePoolGroup) Identity Word16
cppMaxCollateralInputs :: THKD ('PPGroups 'NetworkGroup 'NoStakePoolGroup) Identity Word16
cppPoolVotingThresholds :: THKD
('PPGroups 'GovGroup 'NoStakePoolGroup)
Identity
PoolVotingThresholds
cppDRepVotingThresholds :: THKD
('PPGroups 'GovGroup 'NoStakePoolGroup)
Identity
DRepVotingThresholds
cppCommitteeMinSize :: THKD ('PPGroups 'GovGroup 'NoStakePoolGroup) Identity Word16
cppCommitteeMaxTermLength :: THKD ('PPGroups 'GovGroup 'NoStakePoolGroup) Identity EpochInterval
cppGovActionLifetime :: THKD ('PPGroups 'GovGroup 'NoStakePoolGroup) Identity EpochInterval
cppGovActionDeposit :: THKD ('PPGroups 'GovGroup 'SecurityGroup) Identity Coin
cppDRepDeposit :: THKD ('PPGroups 'GovGroup 'NoStakePoolGroup) Identity Coin
cppDRepActivity :: THKD ('PPGroups 'GovGroup 'NoStakePoolGroup) Identity EpochInterval
cppMinFeeRefScriptCostPerByte :: THKD
('PPGroups 'EconomicGroup 'SecurityGroup)
Identity
NonNegativeInterval
cppMinFeeA :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD ('PPGroups 'EconomicGroup 'SecurityGroup) f Coin
cppMinFeeB :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD ('PPGroups 'EconomicGroup 'SecurityGroup) f Coin
cppMaxBBSize :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD ('PPGroups 'NetworkGroup 'SecurityGroup) f Word32
cppMaxTxSize :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD ('PPGroups 'NetworkGroup 'SecurityGroup) f Word32
cppMaxBHSize :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD ('PPGroups 'NetworkGroup 'SecurityGroup) f Word16
cppKeyDeposit :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD ('PPGroups 'EconomicGroup 'NoStakePoolGroup) f Coin
cppPoolDeposit :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD ('PPGroups 'EconomicGroup 'NoStakePoolGroup) f Coin
cppEMax :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD
('PPGroups 'TechnicalGroup 'NoStakePoolGroup) f EpochInterval
cppNOpt :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD ('PPGroups 'TechnicalGroup 'NoStakePoolGroup) f Word16
cppA0 :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD
('PPGroups 'TechnicalGroup 'NoStakePoolGroup) f NonNegativeInterval
cppRho :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD ('PPGroups 'EconomicGroup 'NoStakePoolGroup) f UnitInterval
cppTau :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD ('PPGroups 'EconomicGroup 'NoStakePoolGroup) f UnitInterval
cppProtocolVersion :: forall (f :: * -> *) era.
ConwayPParams f era -> HKDNoUpdate f ProtVer
cppMinPoolCost :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD ('PPGroups 'EconomicGroup 'NoStakePoolGroup) f Coin
cppCoinsPerUTxOByte :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD ('PPGroups 'EconomicGroup 'SecurityGroup) f CoinPerByte
cppCostModels :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD ('PPGroups 'TechnicalGroup 'NoStakePoolGroup) f CostModels
cppPrices :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD ('PPGroups 'EconomicGroup 'NoStakePoolGroup) f Prices
cppMaxTxExUnits :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD ('PPGroups 'NetworkGroup 'NoStakePoolGroup) f OrdExUnits
cppMaxBlockExUnits :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD ('PPGroups 'NetworkGroup 'SecurityGroup) f OrdExUnits
cppMaxValSize :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD ('PPGroups 'NetworkGroup 'SecurityGroup) f Word32
cppCollateralPercentage :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD ('PPGroups 'TechnicalGroup 'NoStakePoolGroup) f Word16
cppMaxCollateralInputs :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD ('PPGroups 'NetworkGroup 'NoStakePoolGroup) f Word16
cppPoolVotingThresholds :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD
('PPGroups 'GovGroup 'NoStakePoolGroup) f PoolVotingThresholds
cppDRepVotingThresholds :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD
('PPGroups 'GovGroup 'NoStakePoolGroup) f DRepVotingThresholds
cppCommitteeMinSize :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD ('PPGroups 'GovGroup 'NoStakePoolGroup) f Word16
cppCommitteeMaxTermLength :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD ('PPGroups 'GovGroup 'NoStakePoolGroup) f EpochInterval
cppGovActionLifetime :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD ('PPGroups 'GovGroup 'NoStakePoolGroup) f EpochInterval
cppGovActionDeposit :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD ('PPGroups 'GovGroup 'SecurityGroup) f Coin
cppDRepDeposit :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD ('PPGroups 'GovGroup 'NoStakePoolGroup) f Coin
cppDRepActivity :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD ('PPGroups 'GovGroup 'NoStakePoolGroup) f EpochInterval
cppMinFeeRefScriptCostPerByte :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD
('PPGroups 'EconomicGroup 'SecurityGroup) f NonNegativeInterval
..} = do
Integer
ppA <- THKD ('PPGroups 'EconomicGroup 'SecurityGroup) Identity Coin
-> SpecTransM
ctx
(SpecRep
(THKD ('PPGroups 'EconomicGroup 'SecurityGroup) Identity Coin))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep THKD ('PPGroups 'EconomicGroup 'SecurityGroup) Identity Coin
cppMinFeeA
Integer
ppB <- THKD ('PPGroups 'EconomicGroup 'SecurityGroup) Identity Coin
-> SpecTransM
ctx
(SpecRep
(THKD ('PPGroups 'EconomicGroup 'SecurityGroup) Identity Coin))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep THKD ('PPGroups 'EconomicGroup 'SecurityGroup) Identity Coin
cppMinFeeB
Rational
ppA0 <- THKD
('PPGroups 'TechnicalGroup 'NoStakePoolGroup)
Identity
NonNegativeInterval
-> SpecTransM
ctx
(SpecRep
(THKD
('PPGroups 'TechnicalGroup 'NoStakePoolGroup)
Identity
NonNegativeInterval))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep THKD
('PPGroups 'TechnicalGroup 'NoStakePoolGroup)
Identity
NonNegativeInterval
cppA0
Rational
ppMinFeeRefScriptCoinsPerByte <- THKD
('PPGroups 'EconomicGroup 'SecurityGroup)
Identity
NonNegativeInterval
-> SpecTransM
ctx
(SpecRep
(THKD
('PPGroups 'EconomicGroup 'SecurityGroup)
Identity
NonNegativeInterval))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep THKD
('PPGroups 'EconomicGroup 'SecurityGroup)
Identity
NonNegativeInterval
cppMinFeeRefScriptCostPerByte
Integer
ppCollateralPercentage <- THKD ('PPGroups 'TechnicalGroup 'NoStakePoolGroup) Identity Word16
-> SpecTransM
ctx
(SpecRep
(THKD
('PPGroups 'TechnicalGroup 'NoStakePoolGroup) Identity Word16))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep THKD ('PPGroups 'TechnicalGroup 'NoStakePoolGroup) Identity Word16
cppCollateralPercentage
let
ppMaxBlockSize :: Integer
ppMaxBlockSize = Word32 -> Integer
forall a. Integral a => a -> Integer
toInteger (Word32 -> Integer) -> Word32 -> Integer
forall a b. (a -> b) -> a -> b
$ THKD ('PPGroups 'NetworkGroup 'SecurityGroup) Identity Word32
-> HKD Identity Word32
forall (t :: PPGroups) (f :: * -> *) a. THKD t f a -> HKD f a
unTHKD THKD ('PPGroups 'NetworkGroup 'SecurityGroup) Identity Word32
cppMaxBBSize
ppMaxTxSize :: Integer
ppMaxTxSize = Word32 -> Integer
forall a. Integral a => a -> Integer
toInteger (Word32 -> Integer) -> Word32 -> Integer
forall a b. (a -> b) -> a -> b
$ THKD ('PPGroups 'NetworkGroup 'SecurityGroup) Identity Word32
-> HKD Identity Word32
forall (t :: PPGroups) (f :: * -> *) a. THKD t f a -> HKD f a
unTHKD THKD ('PPGroups 'NetworkGroup 'SecurityGroup) Identity Word32
cppMaxTxSize
ppMaxHeaderSize :: Integer
ppMaxHeaderSize = Word16 -> Integer
forall a. Integral a => a -> Integer
toInteger (Word16 -> Integer) -> Word16 -> Integer
forall a b. (a -> b) -> a -> b
$ THKD ('PPGroups 'NetworkGroup 'SecurityGroup) Identity Word16
-> HKD Identity Word16
forall (t :: PPGroups) (f :: * -> *) a. THKD t f a -> HKD f a
unTHKD THKD ('PPGroups 'NetworkGroup 'SecurityGroup) Identity Word16
cppMaxBHSize
Integer
ppKeyDeposit <- THKD ('PPGroups 'EconomicGroup 'NoStakePoolGroup) Identity Coin
-> SpecTransM
ctx
(SpecRep
(THKD ('PPGroups 'EconomicGroup 'NoStakePoolGroup) Identity Coin))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep THKD ('PPGroups 'EconomicGroup 'NoStakePoolGroup) Identity Coin
cppKeyDeposit
Integer
ppPoolDeposit <- THKD ('PPGroups 'EconomicGroup 'NoStakePoolGroup) Identity Coin
-> SpecTransM
ctx
(SpecRep
(THKD ('PPGroups 'EconomicGroup 'NoStakePoolGroup) Identity Coin))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep THKD ('PPGroups 'EconomicGroup 'NoStakePoolGroup) Identity Coin
cppPoolDeposit
Integer
ppEmax <- THKD
('PPGroups 'TechnicalGroup 'NoStakePoolGroup)
Identity
EpochInterval
-> SpecTransM
ctx
(SpecRep
(THKD
('PPGroups 'TechnicalGroup 'NoStakePoolGroup)
Identity
EpochInterval))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep THKD
('PPGroups 'TechnicalGroup 'NoStakePoolGroup)
Identity
EpochInterval
cppEMax
Integer
ppNopt <- Integer -> SpecTransM ctx (SpecRep Integer)
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep (Word16 -> Integer
forall a. Integral a => a -> Integer
toInteger (Word16 -> Integer) -> Word16 -> Integer
forall a b. (a -> b) -> a -> b
$ THKD ('PPGroups 'TechnicalGroup 'NoStakePoolGroup) Identity Word16
-> HKD Identity Word16
forall (t :: PPGroups) (f :: * -> *) a. THKD t f a -> HKD f a
unTHKD THKD ('PPGroups 'TechnicalGroup 'NoStakePoolGroup) Identity Word16
cppNOpt)
let
ppPv :: (Integer, Integer)
ppPv = (Integer
0, Integer
0)
ppMinUTxOValue :: Integer
ppMinUTxOValue = Integer
0
Integer
ppCoinsPerUTxOByte <- THKD ('PPGroups 'EconomicGroup 'SecurityGroup) Identity CoinPerByte
-> SpecTransM
ctx
(SpecRep
(THKD
('PPGroups 'EconomicGroup 'SecurityGroup) Identity CoinPerByte))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep THKD ('PPGroups 'EconomicGroup 'SecurityGroup) Identity CoinPerByte
cppCoinsPerUTxOByte
()
ppCostmdls <- THKD
('PPGroups 'TechnicalGroup 'NoStakePoolGroup) Identity CostModels
-> SpecTransM
ctx
(SpecRep
(THKD
('PPGroups 'TechnicalGroup 'NoStakePoolGroup) Identity CostModels))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep THKD
('PPGroups 'TechnicalGroup 'NoStakePoolGroup) Identity CostModels
cppCostModels
()
ppPrices <- THKD ('PPGroups 'EconomicGroup 'NoStakePoolGroup) Identity Prices
-> SpecTransM
ctx
(SpecRep
(THKD
('PPGroups 'EconomicGroup 'NoStakePoolGroup) Identity Prices))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep THKD ('PPGroups 'EconomicGroup 'NoStakePoolGroup) Identity Prices
cppPrices
let
ppMaxRefScriptSizePerTx :: Integer
ppMaxRefScriptSizePerTx = Int -> Integer
forall a. Integral a => a -> Integer
toInteger Int
maxRefScriptSizePerTx
ppMaxRefScriptSizePerBlock :: Integer
ppMaxRefScriptSizePerBlock = Int -> Integer
forall a. Integral a => a -> Integer
toInteger Int
maxRefScriptSizePerBlock
ppRefScriptCostStride :: Integer
ppRefScriptCostStride = Int -> Integer
forall a. Integral a => a -> Integer
toInteger Int
refScriptCostStride
ppRefScriptCostMultiplier :: Rational
ppRefScriptCostMultiplier = Rational
refScriptCostMultiplier
(Integer, Integer)
ppMaxTxExUnits <- THKD
('PPGroups 'NetworkGroup 'NoStakePoolGroup) Identity OrdExUnits
-> SpecTransM
ctx
(SpecRep
(THKD
('PPGroups 'NetworkGroup 'NoStakePoolGroup) Identity OrdExUnits))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep THKD
('PPGroups 'NetworkGroup 'NoStakePoolGroup) Identity OrdExUnits
cppMaxTxExUnits
(Integer, Integer)
ppMaxBlockExUnits <- THKD ('PPGroups 'NetworkGroup 'SecurityGroup) Identity OrdExUnits
-> SpecTransM
ctx
(SpecRep
(THKD
('PPGroups 'NetworkGroup 'SecurityGroup) Identity OrdExUnits))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep THKD ('PPGroups 'NetworkGroup 'SecurityGroup) Identity OrdExUnits
cppMaxBlockExUnits
let
ppMaxValSize :: Integer
ppMaxValSize = Word32 -> Integer
forall a. Integral a => a -> Integer
toInteger (Word32 -> Integer)
-> (THKD ('PPGroups 'NetworkGroup 'SecurityGroup) Identity Word32
-> Word32)
-> THKD ('PPGroups 'NetworkGroup 'SecurityGroup) Identity Word32
-> Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. THKD ('PPGroups 'NetworkGroup 'SecurityGroup) Identity Word32
-> Word32
THKD ('PPGroups 'NetworkGroup 'SecurityGroup) Identity Word32
-> HKD Identity Word32
forall (t :: PPGroups) (f :: * -> *) a. THKD t f a -> HKD f a
unTHKD (THKD ('PPGroups 'NetworkGroup 'SecurityGroup) Identity Word32
-> Integer)
-> THKD ('PPGroups 'NetworkGroup 'SecurityGroup) Identity Word32
-> Integer
forall a b. (a -> b) -> a -> b
$ THKD ('PPGroups 'NetworkGroup 'SecurityGroup) Identity Word32
cppMaxValSize
ppMaxCollateralInputs :: Integer
ppMaxCollateralInputs = Word16 -> Integer
forall a. Integral a => a -> Integer
toInteger (Word16 -> Integer)
-> (THKD
('PPGroups 'NetworkGroup 'NoStakePoolGroup) Identity Word16
-> Word16)
-> THKD ('PPGroups 'NetworkGroup 'NoStakePoolGroup) Identity Word16
-> Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. THKD ('PPGroups 'NetworkGroup 'NoStakePoolGroup) Identity Word16
-> Word16
THKD ('PPGroups 'NetworkGroup 'NoStakePoolGroup) Identity Word16
-> HKD Identity Word16
forall (t :: PPGroups) (f :: * -> *) a. THKD t f a -> HKD f a
unTHKD (THKD ('PPGroups 'NetworkGroup 'NoStakePoolGroup) Identity Word16
-> Integer)
-> THKD ('PPGroups 'NetworkGroup 'NoStakePoolGroup) Identity Word16
-> Integer
forall a b. (a -> b) -> a -> b
$ THKD ('PPGroups 'NetworkGroup 'NoStakePoolGroup) Identity Word16
cppMaxCollateralInputs
PoolThresholds
ppPoolThresholds <- THKD
('PPGroups 'GovGroup 'NoStakePoolGroup)
Identity
PoolVotingThresholds
-> SpecTransM
ctx
(SpecRep
(THKD
('PPGroups 'GovGroup 'NoStakePoolGroup)
Identity
PoolVotingThresholds))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep THKD
('PPGroups 'GovGroup 'NoStakePoolGroup)
Identity
PoolVotingThresholds
cppPoolVotingThresholds
DrepThresholds
ppDrepThresholds <- THKD
('PPGroups 'GovGroup 'NoStakePoolGroup)
Identity
DRepVotingThresholds
-> SpecTransM
ctx
(SpecRep
(THKD
('PPGroups 'GovGroup 'NoStakePoolGroup)
Identity
DRepVotingThresholds))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep THKD
('PPGroups 'GovGroup 'NoStakePoolGroup)
Identity
DRepVotingThresholds
cppDRepVotingThresholds
let
ppCcMinSize :: Integer
ppCcMinSize = Word16 -> Integer
forall a. Integral a => a -> Integer
toInteger (Word16 -> Integer)
-> (THKD ('PPGroups 'GovGroup 'NoStakePoolGroup) Identity Word16
-> Word16)
-> THKD ('PPGroups 'GovGroup 'NoStakePoolGroup) Identity Word16
-> Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. THKD ('PPGroups 'GovGroup 'NoStakePoolGroup) Identity Word16
-> Word16
THKD ('PPGroups 'GovGroup 'NoStakePoolGroup) Identity Word16
-> HKD Identity Word16
forall (t :: PPGroups) (f :: * -> *) a. THKD t f a -> HKD f a
unTHKD (THKD ('PPGroups 'GovGroup 'NoStakePoolGroup) Identity Word16
-> Integer)
-> THKD ('PPGroups 'GovGroup 'NoStakePoolGroup) Identity Word16
-> Integer
forall a b. (a -> b) -> a -> b
$ THKD ('PPGroups 'GovGroup 'NoStakePoolGroup) Identity Word16
cppCommitteeMinSize
ppCcMaxTermLength :: Integer
ppCcMaxTermLength = Word32 -> Integer
forall a. Integral a => a -> Integer
toInteger (Word32 -> Integer)
-> (THKD
('PPGroups 'GovGroup 'NoStakePoolGroup) Identity EpochInterval
-> Word32)
-> THKD
('PPGroups 'GovGroup 'NoStakePoolGroup) Identity EpochInterval
-> Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. EpochInterval -> Word32
unEpochInterval (EpochInterval -> Word32)
-> (THKD
('PPGroups 'GovGroup 'NoStakePoolGroup) Identity EpochInterval
-> EpochInterval)
-> THKD
('PPGroups 'GovGroup 'NoStakePoolGroup) Identity EpochInterval
-> Word32
forall b c a. (b -> c) -> (a -> b) -> a -> c
. THKD ('PPGroups 'GovGroup 'NoStakePoolGroup) Identity EpochInterval
-> EpochInterval
THKD ('PPGroups 'GovGroup 'NoStakePoolGroup) Identity EpochInterval
-> HKD Identity EpochInterval
forall (t :: PPGroups) (f :: * -> *) a. THKD t f a -> HKD f a
unTHKD (THKD
('PPGroups 'GovGroup 'NoStakePoolGroup) Identity EpochInterval
-> Integer)
-> THKD
('PPGroups 'GovGroup 'NoStakePoolGroup) Identity EpochInterval
-> Integer
forall a b. (a -> b) -> a -> b
$ THKD ('PPGroups 'GovGroup 'NoStakePoolGroup) Identity EpochInterval
cppCommitteeMaxTermLength
Integer
ppGovActionLifetime <- THKD ('PPGroups 'GovGroup 'NoStakePoolGroup) Identity EpochInterval
-> SpecTransM
ctx
(SpecRep
(THKD
('PPGroups 'GovGroup 'NoStakePoolGroup) Identity EpochInterval))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep THKD ('PPGroups 'GovGroup 'NoStakePoolGroup) Identity EpochInterval
cppGovActionLifetime
Integer
ppGovActionDeposit <- THKD ('PPGroups 'GovGroup 'SecurityGroup) Identity Coin
-> SpecTransM
ctx
(SpecRep (THKD ('PPGroups 'GovGroup 'SecurityGroup) Identity Coin))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep THKD ('PPGroups 'GovGroup 'SecurityGroup) Identity Coin
cppGovActionDeposit
Integer
ppDrepDeposit <- THKD ('PPGroups 'GovGroup 'NoStakePoolGroup) Identity Coin
-> SpecTransM
ctx
(SpecRep
(THKD ('PPGroups 'GovGroup 'NoStakePoolGroup) Identity Coin))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep THKD ('PPGroups 'GovGroup 'NoStakePoolGroup) Identity Coin
cppDRepDeposit
Integer
ppDrepActivity <- THKD ('PPGroups 'GovGroup 'NoStakePoolGroup) Identity EpochInterval
-> SpecTransM
ctx
(SpecRep
(THKD
('PPGroups 'GovGroup 'NoStakePoolGroup) Identity EpochInterval))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep THKD ('PPGroups 'GovGroup 'NoStakePoolGroup) Identity EpochInterval
cppDRepActivity
Rational
ppMonetaryExpansion <- THKD
('PPGroups 'EconomicGroup 'NoStakePoolGroup) Identity UnitInterval
-> SpecTransM
ctx
(SpecRep
(THKD
('PPGroups 'EconomicGroup 'NoStakePoolGroup)
Identity
UnitInterval))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep THKD
('PPGroups 'EconomicGroup 'NoStakePoolGroup) Identity UnitInterval
cppRho
Rational
ppTreasuryCut <- THKD
('PPGroups 'EconomicGroup 'NoStakePoolGroup) Identity UnitInterval
-> SpecTransM
ctx
(SpecRep
(THKD
('PPGroups 'EconomicGroup 'NoStakePoolGroup)
Identity
UnitInterval))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep THKD
('PPGroups 'EconomicGroup 'NoStakePoolGroup) Identity UnitInterval
cppTau
PParams -> SpecTransM ctx PParams
forall a. a -> SpecTransM ctx a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Agda.MkPParams {Integer
Rational
()
(Integer, Integer)
PoolThresholds
DrepThresholds
ppA :: Integer
ppB :: Integer
ppA0 :: Rational
ppMinFeeRefScriptCoinsPerByte :: Rational
ppCollateralPercentage :: Integer
ppMaxBlockSize :: Integer
ppMaxTxSize :: Integer
ppMaxHeaderSize :: Integer
ppKeyDeposit :: Integer
ppPoolDeposit :: Integer
ppEmax :: Integer
ppNopt :: Integer
ppPv :: (Integer, Integer)
ppMinUTxOValue :: Integer
ppCoinsPerUTxOByte :: Integer
ppCostmdls :: ()
ppPrices :: ()
ppMaxRefScriptSizePerTx :: Integer
ppMaxRefScriptSizePerBlock :: Integer
ppRefScriptCostStride :: Integer
ppRefScriptCostMultiplier :: Rational
ppMaxTxExUnits :: (Integer, Integer)
ppMaxBlockExUnits :: (Integer, Integer)
ppMaxValSize :: Integer
ppMaxCollateralInputs :: Integer
ppPoolThresholds :: PoolThresholds
ppDrepThresholds :: DrepThresholds
ppCcMinSize :: Integer
ppCcMaxTermLength :: Integer
ppGovActionLifetime :: Integer
ppGovActionDeposit :: Integer
ppDrepDeposit :: Integer
ppDrepActivity :: Integer
ppMonetaryExpansion :: Rational
ppTreasuryCut :: Rational
ppMaxBlockSize :: Integer
ppMaxTxSize :: Integer
ppMaxHeaderSize :: Integer
ppMaxTxExUnits :: (Integer, Integer)
ppMaxBlockExUnits :: (Integer, Integer)
ppMaxValSize :: Integer
ppMaxCollateralInputs :: Integer
ppPv :: (Integer, Integer)
ppA :: Integer
ppB :: Integer
ppKeyDeposit :: Integer
ppPoolDeposit :: Integer
ppMonetaryExpansion :: Rational
ppTreasuryCut :: Rational
ppCoinsPerUTxOByte :: Integer
ppPrices :: ()
ppMinFeeRefScriptCoinsPerByte :: Rational
ppMaxRefScriptSizePerTx :: Integer
ppMaxRefScriptSizePerBlock :: Integer
ppRefScriptCostStride :: Integer
ppRefScriptCostMultiplier :: Rational
ppMinUTxOValue :: Integer
ppEmax :: Integer
ppNopt :: Integer
ppA0 :: Rational
ppCollateralPercentage :: Integer
ppCostmdls :: ()
ppPoolThresholds :: PoolThresholds
ppDrepThresholds :: DrepThresholds
ppCcMinSize :: Integer
ppCcMaxTermLength :: Integer
ppGovActionLifetime :: Integer
ppGovActionDeposit :: Integer
ppDrepDeposit :: Integer
ppDrepActivity :: Integer
..}
instance
SpecTranslate ctx (PParamsHKD Identity era) =>
SpecTranslate ctx (PParams era)
where
type SpecRep (PParams era) = SpecRep (PParamsHKD Identity era)
toSpecRep :: PParams era -> SpecTransM ctx (SpecRep (PParams era))
toSpecRep (PParams PParamsHKD Identity era
x) = PParamsHKD Identity era
-> SpecTransM ctx (SpecRep (PParamsHKD Identity era))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep PParamsHKD Identity era
x
instance SpecTranslate ctx a => SpecTranslate ctx (Set a) where
type SpecRep (Set a) = Agda.HSSet (SpecRep a)
toSpecRep :: Set a -> SpecTransM ctx (SpecRep (Set a))
toSpecRep = ([SpecRep a] -> HSSet (SpecRep a))
-> SpecTransM ctx [SpecRep a] -> SpecTransM ctx (HSSet (SpecRep a))
forall a b. (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [SpecRep a] -> HSSet (SpecRep a)
forall a. [a] -> HSSet a
Agda.MkHSSet (SpecTransM ctx [SpecRep a] -> SpecTransM ctx (HSSet (SpecRep a)))
-> (Set a -> SpecTransM ctx [SpecRep a])
-> Set a
-> SpecTransM ctx (HSSet (SpecRep a))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> SpecTransM ctx (SpecRep a))
-> [a] -> SpecTransM ctx [SpecRep a]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse a -> SpecTransM ctx (SpecRep a)
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep ([a] -> SpecTransM ctx [SpecRep a])
-> (Set a -> [a]) -> Set a -> SpecTransM ctx [SpecRep a]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set a -> [a]
forall a. Set a -> [a]
Set.toList
instance SpecTranslate ctx a => SpecTranslate ctx (StrictSeq a) where
type SpecRep (StrictSeq a) = [SpecRep a]
toSpecRep :: StrictSeq a -> SpecTransM ctx (SpecRep (StrictSeq a))
toSpecRep = (a -> SpecTransM ctx (SpecRep a))
-> [a] -> SpecTransM ctx [SpecRep a]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse a -> SpecTransM ctx (SpecRep a)
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep ([a] -> SpecTransM ctx [SpecRep a])
-> (StrictSeq a -> [a])
-> StrictSeq a
-> SpecTransM ctx [SpecRep a]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. StrictSeq a -> [a]
forall a. StrictSeq a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList
instance SpecTranslate ctx a => SpecTranslate ctx (Seq a) where
type SpecRep (Seq a) = [SpecRep a]
toSpecRep :: Seq a -> SpecTransM ctx (SpecRep (Seq a))
toSpecRep = (a -> SpecTransM ctx (SpecRep a))
-> [a] -> SpecTransM ctx [SpecRep a]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse a -> SpecTransM ctx (SpecRep a)
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep ([a] -> SpecTransM ctx [SpecRep a])
-> (Seq a -> [a]) -> Seq a -> SpecTransM ctx [SpecRep a]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Seq a -> [a]
forall a. Seq a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList
instance SpecTranslate ctx a => SpecTranslate ctx (Sized a) where
type SpecRep (Sized a) = SpecRep a
toSpecRep :: Sized a -> SpecTransM ctx (SpecRep (Sized a))
toSpecRep (Sized a
x Int64
_) = a -> SpecTransM ctx (SpecRep a)
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep a
x
instance SpecTranslate ctx ValidityInterval where
type SpecRep ValidityInterval = (Maybe Integer, Maybe Integer)
toSpecRep :: ValidityInterval -> SpecTransM ctx (SpecRep ValidityInterval)
toSpecRep (ValidityInterval StrictMaybe SlotNo
lo StrictMaybe SlotNo
hi) = (StrictMaybe SlotNo, StrictMaybe SlotNo)
-> SpecTransM
ctx (SpecRep (StrictMaybe SlotNo, StrictMaybe SlotNo))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep (StrictMaybe SlotNo
lo, StrictMaybe SlotNo
hi)
instance SpecTranslate ctx (KeyHash r) where
type SpecRep (KeyHash r) = Integer
toSpecRep :: KeyHash r -> SpecTransM ctx (SpecRep (KeyHash r))
toSpecRep (KeyHash Hash ADDRHASH (VerKeyDSIGN DSIGN)
h) = Hash ADDRHASH (VerKeyDSIGN DSIGN)
-> SpecTransM ctx (SpecRep (Hash ADDRHASH (VerKeyDSIGN DSIGN)))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep Hash ADDRHASH (VerKeyDSIGN DSIGN)
h
vkeyToInteger :: VKey kd -> Integer
vkeyToInteger :: forall (kd :: KeyRole). VKey kd -> Integer
vkeyToInteger = Nat -> Integer
forall a. Integral a => a -> Integer
toInteger (Nat -> Integer) -> (VKey kd -> Nat) -> VKey kd -> Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ByteString -> Nat
bytesToNatural (ByteString -> Nat) -> (VKey kd -> ByteString) -> VKey kd -> Nat
forall b c a. (b -> c) -> (a -> b) -> a -> c
. VerKeyDSIGN DSIGN -> ByteString
forall v. DSIGNAlgorithm v => VerKeyDSIGN v -> ByteString
rawSerialiseVerKeyDSIGN (VerKeyDSIGN DSIGN -> ByteString)
-> (VKey kd -> VerKeyDSIGN DSIGN) -> VKey kd -> ByteString
forall b c a. (b -> c) -> (a -> b) -> a -> c
. VKey kd -> VerKeyDSIGN DSIGN
forall (kd :: KeyRole). VKey kd -> VerKeyDSIGN DSIGN
unVKey
vkeyFromInteger :: Integer -> Maybe (VKey kd)
vkeyFromInteger :: forall (kd :: KeyRole). Integer -> Maybe (VKey kd)
vkeyFromInteger = (VerKeyDSIGN DSIGN -> VKey kd)
-> Maybe (VerKeyDSIGN DSIGN) -> Maybe (VKey kd)
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap VerKeyDSIGN DSIGN -> VKey kd
forall (kd :: KeyRole). VerKeyDSIGN DSIGN -> VKey kd
VKey (Maybe (VerKeyDSIGN DSIGN) -> Maybe (VKey kd))
-> (Integer -> Maybe (VerKeyDSIGN DSIGN))
-> Integer
-> Maybe (VKey kd)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ByteString -> Maybe (VerKeyDSIGN DSIGN)
forall v. DSIGNAlgorithm v => ByteString -> Maybe (VerKeyDSIGN v)
rawDeserialiseVerKeyDSIGN (ByteString -> Maybe (VerKeyDSIGN DSIGN))
-> (Integer -> ByteString) -> Integer -> Maybe (VerKeyDSIGN DSIGN)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Nat -> ByteString
naturalToBytes Int
32 (Nat -> ByteString) -> (Integer -> Nat) -> Integer -> ByteString
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> Nat
forall a. Num a => Integer -> a
fromInteger
signatureToInteger :: DSIGNAlgorithm v => SigDSIGN v -> Integer
signatureToInteger :: forall v. DSIGNAlgorithm v => SigDSIGN v -> Integer
signatureToInteger = Nat -> Integer
forall a. Integral a => a -> Integer
toInteger (Nat -> Integer) -> (SigDSIGN v -> Nat) -> SigDSIGN v -> Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ByteString -> Nat
bytesToNatural (ByteString -> Nat)
-> (SigDSIGN v -> ByteString) -> SigDSIGN v -> Nat
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SigDSIGN v -> ByteString
forall v. DSIGNAlgorithm v => SigDSIGN v -> ByteString
rawSerialiseSigDSIGN
signatureFromInteger :: DSIGNAlgorithm v => Integer -> Maybe (SigDSIGN v)
signatureFromInteger :: forall v. DSIGNAlgorithm v => Integer -> Maybe (SigDSIGN v)
signatureFromInteger = ByteString -> Maybe (SigDSIGN v)
forall v. DSIGNAlgorithm v => ByteString -> Maybe (SigDSIGN v)
rawDeserialiseSigDSIGN (ByteString -> Maybe (SigDSIGN v))
-> (Integer -> ByteString) -> Integer -> Maybe (SigDSIGN v)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Nat -> ByteString
naturalToBytes Int
64 (Nat -> ByteString) -> (Integer -> Nat) -> Integer -> ByteString
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> Nat
forall a. Num a => Integer -> a
fromInteger
instance SpecTranslate ctx (VKey k) where
type SpecRep (VKey k) = Agda.HSVKey
toSpecRep :: VKey k -> SpecTransM ctx (SpecRep (VKey k))
toSpecRep VKey k
x = do
let hvkVKey :: Integer
hvkVKey = VKey k -> Integer
forall (kd :: KeyRole). VKey kd -> Integer
vkeyToInteger VKey k
x
Integer
hvkStoredHash <- Hash ADDRHASH (VerKeyDSIGN DSIGN)
-> SpecTransM ctx (SpecRep (Hash ADDRHASH (VerKeyDSIGN DSIGN)))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep (forall v h.
(DSIGNAlgorithm v, HashAlgorithm h) =>
VerKeyDSIGN v -> Hash h (VerKeyDSIGN v)
hashVerKeyDSIGN @_ @ADDRHASH (VerKeyDSIGN DSIGN -> Hash ADDRHASH (VerKeyDSIGN DSIGN))
-> VerKeyDSIGN DSIGN -> Hash ADDRHASH (VerKeyDSIGN DSIGN)
forall a b. (a -> b) -> a -> b
$ VKey k -> VerKeyDSIGN DSIGN
forall (kd :: KeyRole). VKey kd -> VerKeyDSIGN DSIGN
unVKey VKey k
x)
HSVKey -> SpecTransM ctx HSVKey
forall a. a -> SpecTransM ctx a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Agda.MkHSVKey {Integer
hvkVKey :: Integer
hvkStoredHash :: Integer
hvkVKey :: Integer
hvkStoredHash :: Integer
..}
instance DSIGNAlgorithm v => SpecTranslate ctx (SignedDSIGN v a) where
type SpecRep (SignedDSIGN v a) = Integer
toSpecRep :: SignedDSIGN v a -> SpecTransM ctx (SpecRep (SignedDSIGN v a))
toSpecRep (SignedDSIGN SigDSIGN v
x) = Integer -> SpecTransM ctx Integer
forall a. a -> SpecTransM ctx a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Integer -> SpecTransM ctx Integer)
-> Integer -> SpecTransM ctx Integer
forall a b. (a -> b) -> a -> b
$ SigDSIGN v -> Integer
forall v. DSIGNAlgorithm v => SigDSIGN v -> Integer
signatureToInteger SigDSIGN v
x
instance SpecTranslate ctx (WitVKey k) where
type SpecRep (WitVKey k) = (SpecRep (VKey k), Integer)
toSpecRep :: WitVKey k -> SpecTransM ctx (SpecRep (WitVKey k))
toSpecRep (WitVKey VKey k
vk SignedDSIGN DSIGN (Hash HASH EraIndependentTxBody)
sk) = (VKey k, SignedDSIGN DSIGN (Hash HASH EraIndependentTxBody))
-> SpecTransM
ctx
(SpecRep
(VKey k, SignedDSIGN DSIGN (Hash HASH EraIndependentTxBody)))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep (VKey k
vk, SignedDSIGN DSIGN (Hash HASH EraIndependentTxBody)
sk)
instance Era era => SpecTranslate ctx (TxDats era) where
type SpecRep (TxDats era) = Agda.HSMap Agda.DataHash Agda.Datum
toSpecRep :: TxDats era -> SpecTransM ctx (SpecRep (TxDats era))
toSpecRep (TxDats Map DataHash (Data era)
x) = Map DataHash (Data era)
-> SpecTransM ctx (SpecRep (Map DataHash (Data era)))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep Map DataHash (Data era)
x
instance
( SpecTranslate ctx k
, SpecTranslate ctx v
) =>
SpecTranslate ctx (Map k v)
where
type SpecRep (Map k v) = Agda.HSMap (SpecRep k) (SpecRep v)
toSpecRep :: Map k v -> SpecTransM ctx (SpecRep (Map k v))
toSpecRep = ([(SpecRep k, SpecRep v)] -> HSMap (SpecRep k) (SpecRep v))
-> SpecTransM ctx [(SpecRep k, SpecRep v)]
-> SpecTransM ctx (HSMap (SpecRep k) (SpecRep v))
forall a b. (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [(SpecRep k, SpecRep v)] -> HSMap (SpecRep k) (SpecRep v)
forall k v. [(k, v)] -> HSMap k v
Agda.MkHSMap (SpecTransM ctx [(SpecRep k, SpecRep v)]
-> SpecTransM ctx (HSMap (SpecRep k) (SpecRep v)))
-> (Map k v -> SpecTransM ctx [(SpecRep k, SpecRep v)])
-> Map k v
-> SpecTransM ctx (HSMap (SpecRep k) (SpecRep v))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((k, v) -> SpecTransM ctx (SpecRep k, SpecRep v))
-> [(k, v)] -> SpecTransM ctx [(SpecRep k, SpecRep v)]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse ((k -> SpecTransM ctx (SpecRep k))
-> (v -> SpecTransM ctx (SpecRep v))
-> (k, v)
-> SpecTransM ctx (SpecRep k, SpecRep v)
forall (t :: * -> * -> *) (f :: * -> *) a c b d.
(Bitraversable t, Applicative f) =>
(a -> f c) -> (b -> f d) -> t a b -> f (t c d)
bimapM k -> SpecTransM ctx (SpecRep k)
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep v -> SpecTransM ctx (SpecRep v)
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep) ([(k, v)] -> SpecTransM ctx [(SpecRep k, SpecRep v)])
-> (Map k v -> [(k, v)])
-> Map k v
-> SpecTransM ctx [(SpecRep k, SpecRep v)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Map k v -> [(k, v)]
forall k a. Map k a -> [(k, a)]
Map.toList
instance SpecTranslate ctx Word64 where
type SpecRep Word64 = Integer
toSpecRep :: Word64 -> SpecTransM ctx (SpecRep Word64)
toSpecRep = Integer -> SpecTransM ctx Integer
forall a. a -> SpecTransM ctx a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Integer -> SpecTransM ctx Integer)
-> (Word64 -> Integer) -> Word64 -> SpecTransM ctx Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Word64 -> Integer
forall a. Integral a => a -> Integer
toInteger
instance SpecTranslate ctx Word32 where
type SpecRep Word32 = Integer
toSpecRep :: Word32 -> SpecTransM ctx (SpecRep Word32)
toSpecRep = Integer -> SpecTransM ctx Integer
forall a. a -> SpecTransM ctx a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Integer -> SpecTransM ctx Integer)
-> (Word32 -> Integer) -> Word32 -> SpecTransM ctx Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Word32 -> Integer
forall a. Integral a => a -> Integer
toInteger
instance SpecTranslate ctx (AlonzoPlutusPurpose AsIx era) where
type SpecRep (AlonzoPlutusPurpose AsIx era) = Agda.RdmrPtr
toSpecRep :: AlonzoPlutusPurpose AsIx era
-> SpecTransM ctx (SpecRep (AlonzoPlutusPurpose AsIx era))
toSpecRep = \case
AlonzoSpending (AsIx Word32
i) -> (Tag, Integer) -> SpecTransM ctx (Tag, Integer)
forall a. a -> SpecTransM ctx a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Tag
Agda.Spend, Word32 -> Integer
forall a. Integral a => a -> Integer
toInteger Word32
i)
AlonzoMinting (AsIx Word32
i) -> (Tag, Integer) -> SpecTransM ctx (Tag, Integer)
forall a. a -> SpecTransM ctx a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Tag
Agda.Mint, Word32 -> Integer
forall a. Integral a => a -> Integer
toInteger Word32
i)
AlonzoCertifying (AsIx Word32
i) -> (Tag, Integer) -> SpecTransM ctx (Tag, Integer)
forall a. a -> SpecTransM ctx a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Tag
Agda.Cert, Word32 -> Integer
forall a. Integral a => a -> Integer
toInteger Word32
i)
AlonzoRewarding (AsIx Word32
i) -> (Tag, Integer) -> SpecTransM ctx (Tag, Integer)
forall a. a -> SpecTransM ctx a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Tag
Agda.Rewrd, Word32 -> Integer
forall a. Integral a => a -> Integer
toInteger Word32
i)
instance SpecTranslate ctx (ConwayPlutusPurpose AsIx era) where
type SpecRep (ConwayPlutusPurpose AsIx era) = Agda.RdmrPtr
toSpecRep :: ConwayPlutusPurpose AsIx era
-> SpecTransM ctx (SpecRep (ConwayPlutusPurpose AsIx era))
toSpecRep = \case
ConwaySpending (AsIx Word32
i) -> (Tag, Integer) -> SpecTransM ctx (Tag, Integer)
forall a. a -> SpecTransM ctx a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Tag
Agda.Spend, Word32 -> Integer
forall a. Integral a => a -> Integer
toInteger Word32
i)
ConwayMinting (AsIx Word32
i) -> (Tag, Integer) -> SpecTransM ctx (Tag, Integer)
forall a. a -> SpecTransM ctx a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Tag
Agda.Mint, Word32 -> Integer
forall a. Integral a => a -> Integer
toInteger Word32
i)
ConwayCertifying (AsIx Word32
i) -> (Tag, Integer) -> SpecTransM ctx (Tag, Integer)
forall a. a -> SpecTransM ctx a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Tag
Agda.Cert, Word32 -> Integer
forall a. Integral a => a -> Integer
toInteger Word32
i)
ConwayRewarding (AsIx Word32
i) -> (Tag, Integer) -> SpecTransM ctx (Tag, Integer)
forall a. a -> SpecTransM ctx a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Tag
Agda.Rewrd, Word32 -> Integer
forall a. Integral a => a -> Integer
toInteger Word32
i)
ConwayVoting (AsIx Word32
i) -> (Tag, Integer) -> SpecTransM ctx (Tag, Integer)
forall a. a -> SpecTransM ctx a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Tag
Agda.Vote, Word32 -> Integer
forall a. Integral a => a -> Integer
toInteger Word32
i)
ConwayProposing (AsIx Word32
i) -> (Tag, Integer) -> SpecTransM ctx (Tag, Integer)
forall a. a -> SpecTransM ctx a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Tag
Agda.Propose, Word32 -> Integer
forall a. Integral a => a -> Integer
toInteger Word32
i)
instance
( SpecTranslate ctx a
, SpecTranslate ctx b
) =>
SpecTranslate ctx (a, b)
where
type SpecRep (a, b) = (SpecRep a, SpecRep b)
toSpecRep :: (a, b) -> SpecTransM ctx (SpecRep (a, b))
toSpecRep (a
x, b
y) = (,) (SpecRep a -> SpecRep b -> (SpecRep a, SpecRep b))
-> SpecTransM ctx (SpecRep a)
-> SpecTransM ctx (SpecRep b -> (SpecRep a, SpecRep b))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> SpecTransM ctx (SpecRep a)
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep a
x SpecTransM ctx (SpecRep b -> (SpecRep a, SpecRep b))
-> SpecTransM ctx (SpecRep b)
-> SpecTransM ctx (SpecRep a, SpecRep b)
forall a b.
SpecTransM ctx (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> b -> SpecTransM ctx (SpecRep b)
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep b
y
instance Era era => SpecTranslate ctx (Data era) where
type SpecRep (Data era) = Agda.DataHash
toSpecRep :: Data era -> SpecTransM ctx (SpecRep (Data era))
toSpecRep = DataHash -> SpecTransM ctx Integer
DataHash -> SpecTransM ctx (SpecRep DataHash)
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep (DataHash -> SpecTransM ctx Integer)
-> (Data era -> DataHash) -> Data era -> SpecTransM ctx Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Data era -> DataHash
forall x i. HashAnnotated x i => x -> SafeHash i
hashAnnotated
instance
( AlonzoEraScript era
, SpecTranslate ctx (PlutusPurpose AsIx era)
) =>
SpecTranslate ctx (Redeemers era)
where
type
SpecRep (Redeemers era) =
Agda.HSMap (SpecRep (PlutusPurpose AsIx era)) (Agda.Redeemer, Agda.ExUnits)
toSpecRep :: Redeemers era -> SpecTransM ctx (SpecRep (Redeemers era))
toSpecRep (Redeemers Map (PlutusPurpose AsIx era) (Data era, ExUnits)
x) = Map (PlutusPurpose AsIx era) (Data era, ExUnits)
-> SpecTransM
ctx (SpecRep (Map (PlutusPurpose AsIx era) (Data era, ExUnits)))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep Map (PlutusPurpose AsIx era) (Data era, ExUnits)
x
instance
( AlonzoEraScript era
, SpecTranslate ctx (PlutusPurpose AsIx era)
, SpecRep (PlutusPurpose AsIx era) ~ Agda.RdmrPtr
, Script era ~ AlonzoScript era
, NativeScript era ~ Timelock era
) =>
SpecTranslate ctx (AlonzoTxWits era)
where
type SpecRep (AlonzoTxWits era) = Agda.TxWitnesses
toSpecRep :: AlonzoTxWits era -> SpecTransM ctx (SpecRep (AlonzoTxWits era))
toSpecRep AlonzoTxWits era
x =
HSMap HSVKey Integer
-> HSSet (Either HSTimelock HSPlutusScript)
-> HSMap Integer Integer
-> HSMap (Tag, Integer) (Integer, (Integer, Integer))
-> TxWitnesses
Agda.MkTxWitnesses
(HSMap HSVKey Integer
-> HSSet (Either HSTimelock HSPlutusScript)
-> HSMap Integer Integer
-> HSMap (Tag, Integer) (Integer, (Integer, Integer))
-> TxWitnesses)
-> SpecTransM ctx (HSMap HSVKey Integer)
-> SpecTransM
ctx
(HSSet (Either HSTimelock HSPlutusScript)
-> HSMap Integer Integer
-> HSMap (Tag, Integer) (Integer, (Integer, Integer))
-> TxWitnesses)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ([(HSVKey, Integer)] -> HSMap HSVKey Integer)
-> SpecTransM ctx [(HSVKey, Integer)]
-> SpecTransM ctx (HSMap HSVKey Integer)
forall a b. (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [(HSVKey, Integer)] -> HSMap HSVKey Integer
forall k v. [(k, v)] -> HSMap k v
Agda.MkHSMap ([WitVKey 'Witness] -> SpecTransM ctx (SpecRep [WitVKey 'Witness])
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep [WitVKey 'Witness]
txWitsMap)
SpecTransM
ctx
(HSSet (Either HSTimelock HSPlutusScript)
-> HSMap Integer Integer
-> HSMap (Tag, Integer) (Integer, (Integer, Integer))
-> TxWitnesses)
-> SpecTransM ctx (HSSet (Either HSTimelock HSPlutusScript))
-> SpecTransM
ctx
(HSMap Integer Integer
-> HSMap (Tag, Integer) (Integer, (Integer, Integer))
-> TxWitnesses)
forall a b.
SpecTransM ctx (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ([Either HSTimelock HSPlutusScript]
-> HSSet (Either HSTimelock HSPlutusScript))
-> SpecTransM ctx [Either HSTimelock HSPlutusScript]
-> SpecTransM ctx (HSSet (Either HSTimelock HSPlutusScript))
forall a b. (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [Either HSTimelock HSPlutusScript]
-> HSSet (Either HSTimelock HSPlutusScript)
forall a. [a] -> HSSet a
Agda.MkHSSet ([AlonzoScript era] -> SpecTransM ctx (SpecRep [AlonzoScript era])
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep (Map ScriptHash (AlonzoScript era) -> [AlonzoScript era]
forall k a. Map k a -> [a]
Map.elems (Map ScriptHash (AlonzoScript era) -> [AlonzoScript era])
-> Map ScriptHash (AlonzoScript era) -> [AlonzoScript era]
forall a b. (a -> b) -> a -> b
$ AlonzoTxWits era -> Map ScriptHash (Script era)
forall era.
AlonzoEraScript era =>
AlonzoTxWits era -> Map ScriptHash (Script era)
txscripts AlonzoTxWits era
x))
SpecTransM
ctx
(HSMap Integer Integer
-> HSMap (Tag, Integer) (Integer, (Integer, Integer))
-> TxWitnesses)
-> SpecTransM ctx (HSMap Integer Integer)
-> SpecTransM
ctx
(HSMap (Tag, Integer) (Integer, (Integer, Integer)) -> TxWitnesses)
forall a b.
SpecTransM ctx (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> TxDats era -> SpecTransM ctx (SpecRep (TxDats era))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep (AlonzoTxWits era -> TxDats era
forall era. AlonzoEraScript era => AlonzoTxWits era -> TxDats era
txdats AlonzoTxWits era
x)
SpecTransM
ctx
(HSMap (Tag, Integer) (Integer, (Integer, Integer)) -> TxWitnesses)
-> SpecTransM
ctx (HSMap (Tag, Integer) (Integer, (Integer, Integer)))
-> SpecTransM ctx TxWitnesses
forall a b.
SpecTransM ctx (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Redeemers era -> SpecTransM ctx (SpecRep (Redeemers era))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep (AlonzoTxWits era -> Redeemers era
forall era.
AlonzoEraScript era =>
AlonzoTxWits era -> Redeemers era
txrdmrs AlonzoTxWits era
x)
where
txWitsMap :: [WitVKey 'Witness]
txWitsMap = Set (WitVKey 'Witness) -> [WitVKey 'Witness]
forall a. Set a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList (AlonzoTxWits era -> Set (WitVKey 'Witness)
forall era.
AlonzoEraScript era =>
AlonzoTxWits era -> Set (WitVKey 'Witness)
txwitsVKey AlonzoTxWits era
x)
instance SpecTranslate ctx a => SpecTranslate ctx (StrictMaybe a) where
type SpecRep (StrictMaybe a) = Maybe (SpecRep a)
toSpecRep :: StrictMaybe a -> SpecTransM ctx (SpecRep (StrictMaybe a))
toSpecRep = Maybe a -> SpecTransM ctx (Maybe (SpecRep a))
Maybe a -> SpecTransM ctx (SpecRep (Maybe a))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep (Maybe a -> SpecTransM ctx (Maybe (SpecRep a)))
-> (StrictMaybe a -> Maybe a)
-> StrictMaybe a
-> SpecTransM ctx (Maybe (SpecRep a))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. StrictMaybe a -> Maybe a
forall a. StrictMaybe a -> Maybe a
strictMaybeToMaybe
instance SpecTranslate ctx a => SpecTranslate ctx (Maybe a) where
type SpecRep (Maybe a) = Maybe (SpecRep a)
toSpecRep :: Maybe a -> SpecTransM ctx (SpecRep (Maybe a))
toSpecRep = (a -> SpecTransM ctx (SpecRep a))
-> Maybe a -> SpecTransM ctx (Maybe (SpecRep a))
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Maybe a -> f (Maybe b)
traverse a -> SpecTransM ctx (SpecRep a)
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep
instance Era era => SpecTranslate ctx (AlonzoTxAuxData era) where
type SpecRep (AlonzoTxAuxData era) = Agda.AuxiliaryData
toSpecRep :: AlonzoTxAuxData era
-> SpecTransM ctx (SpecRep (AlonzoTxAuxData era))
toSpecRep = SafeHash EraIndependentTxAuxData -> SpecTransM ctx Integer
SafeHash EraIndependentTxAuxData
-> SpecTransM ctx (SpecRep (SafeHash EraIndependentTxAuxData))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep (SafeHash EraIndependentTxAuxData -> SpecTransM ctx Integer)
-> (AlonzoTxAuxData era -> SafeHash EraIndependentTxAuxData)
-> AlonzoTxAuxData era
-> SpecTransM ctx Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AlonzoTxAuxData era -> SafeHash EraIndependentTxAuxData
forall x i. HashAnnotated x i => x -> SafeHash i
hashAnnotated
instance SpecTranslate ctx ScriptHash where
type SpecRep ScriptHash = Integer
toSpecRep :: ScriptHash -> SpecTransM ctx (SpecRep ScriptHash)
toSpecRep (ScriptHash Hash ADDRHASH EraIndependentScript
h) = Hash ADDRHASH EraIndependentScript
-> SpecTransM ctx (SpecRep (Hash ADDRHASH EraIndependentScript))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep Hash ADDRHASH EraIndependentScript
h
instance SpecTranslate ctx (Credential k) where
type SpecRep (Credential k) = Agda.Credential
toSpecRep :: Credential k -> SpecTransM ctx (SpecRep (Credential k))
toSpecRep (KeyHashObj KeyHash k
h) = Integer -> Credential
Agda.KeyHashObj (Integer -> Credential)
-> SpecTransM ctx Integer -> SpecTransM ctx Credential
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> KeyHash k -> SpecTransM ctx (SpecRep (KeyHash k))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep KeyHash k
h
toSpecRep (ScriptHashObj ScriptHash
h) = Integer -> Credential
Agda.ScriptObj (Integer -> Credential)
-> SpecTransM ctx Integer -> SpecTransM ctx Credential
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ScriptHash -> SpecTransM ctx (SpecRep ScriptHash)
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep ScriptHash
h
instance SpecTranslate ctx Network where
type SpecRep Network = Integer
toSpecRep :: Network -> SpecTransM ctx (SpecRep Network)
toSpecRep = Integer -> SpecTransM ctx Integer
forall a. a -> SpecTransM ctx a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Integer -> SpecTransM ctx Integer)
-> (Network -> Integer) -> Network -> SpecTransM ctx Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Int -> Integer) -> (Network -> Int) -> Network -> Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Network -> Int
forall a. Enum a => a -> Int
fromEnum
instance SpecTranslate ctx RewardAccount where
type SpecRep RewardAccount = Agda.RwdAddr
toSpecRep :: RewardAccount -> SpecTransM ctx (SpecRep RewardAccount)
toSpecRep (RewardAccount Network
n StakeCredential
c) = Integer -> Credential -> RwdAddr
Agda.RwdAddr (Integer -> Credential -> RwdAddr)
-> SpecTransM ctx Integer -> SpecTransM ctx (Credential -> RwdAddr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Network -> SpecTransM ctx (SpecRep Network)
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep Network
n SpecTransM ctx (Credential -> RwdAddr)
-> SpecTransM ctx Credential -> SpecTransM ctx RwdAddr
forall a b.
SpecTransM ctx (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> StakeCredential -> SpecTransM ctx (SpecRep StakeCredential)
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep StakeCredential
c
instance SpecTranslate ctx PoolParams where
type SpecRep PoolParams = Agda.PoolParams
toSpecRep :: PoolParams -> SpecTransM ctx (SpecRep PoolParams)
toSpecRep PoolParams {Set (KeyHash 'Staking)
StrictMaybe PoolMetadata
KeyHash 'StakePool
VRFVerKeyHash 'StakePoolVRF
RewardAccount
Coin
StrictSeq StakePoolRelay
UnitInterval
ppId :: KeyHash 'StakePool
ppVrf :: VRFVerKeyHash 'StakePoolVRF
ppPledge :: Coin
ppCost :: Coin
ppMargin :: UnitInterval
ppRewardAccount :: RewardAccount
ppOwners :: Set (KeyHash 'Staking)
ppRelays :: StrictSeq StakePoolRelay
ppMetadata :: StrictMaybe PoolMetadata
ppId :: PoolParams -> KeyHash 'StakePool
ppVrf :: PoolParams -> VRFVerKeyHash 'StakePoolVRF
ppPledge :: PoolParams -> Coin
ppCost :: PoolParams -> Coin
ppMargin :: PoolParams -> UnitInterval
ppRewardAccount :: PoolParams -> RewardAccount
ppOwners :: PoolParams -> Set (KeyHash 'Staking)
ppRelays :: PoolParams -> StrictSeq StakePoolRelay
ppMetadata :: PoolParams -> StrictMaybe PoolMetadata
..} =
HSSet Integer
-> Integer -> Rational -> Integer -> Credential -> PoolParams
Agda.PoolParams
(HSSet Integer
-> Integer -> Rational -> Integer -> Credential -> PoolParams)
-> SpecTransM ctx (HSSet Integer)
-> SpecTransM
ctx (Integer -> Rational -> Integer -> Credential -> PoolParams)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Set (KeyHash 'Staking)
-> SpecTransM ctx (SpecRep (Set (KeyHash 'Staking)))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep Set (KeyHash 'Staking)
ppOwners
SpecTransM
ctx (Integer -> Rational -> Integer -> Credential -> PoolParams)
-> SpecTransM ctx Integer
-> SpecTransM ctx (Rational -> Integer -> Credential -> PoolParams)
forall a b.
SpecTransM ctx (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Coin -> SpecTransM ctx (SpecRep Coin)
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep Coin
ppCost
SpecTransM ctx (Rational -> Integer -> Credential -> PoolParams)
-> SpecTransM ctx Rational
-> SpecTransM ctx (Integer -> Credential -> PoolParams)
forall a b.
SpecTransM ctx (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> UnitInterval -> SpecTransM ctx (SpecRep UnitInterval)
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep UnitInterval
ppMargin
SpecTransM ctx (Integer -> Credential -> PoolParams)
-> SpecTransM ctx Integer
-> SpecTransM ctx (Credential -> PoolParams)
forall a b.
SpecTransM ctx (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Coin -> SpecTransM ctx (SpecRep Coin)
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep Coin
ppPledge
SpecTransM ctx (Credential -> PoolParams)
-> SpecTransM ctx Credential -> SpecTransM ctx PoolParams
forall a b.
SpecTransM ctx (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> StakeCredential -> SpecTransM ctx (SpecRep StakeCredential)
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep (RewardAccount -> StakeCredential
raCredential RewardAccount
ppRewardAccount)
instance SpecTranslate ctx DRep where
type SpecRep DRep = Agda.VDeleg
toSpecRep :: DRep -> SpecTransM ctx (SpecRep DRep)
toSpecRep (DRepCredential Credential 'DRepRole
c) = GovRole -> Credential -> VDeleg
Agda.CredVoter GovRole
Agda.DRep (Credential -> VDeleg)
-> SpecTransM ctx Credential -> SpecTransM ctx VDeleg
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Credential 'DRepRole
-> SpecTransM ctx (SpecRep (Credential 'DRepRole))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep Credential 'DRepRole
c
toSpecRep DRep
DRepAlwaysAbstain = VDeleg -> SpecTransM ctx VDeleg
forall a. a -> SpecTransM ctx a
forall (f :: * -> *) a. Applicative f => a -> f a
pure VDeleg
Agda.AbstainRep
toSpecRep DRep
DRepAlwaysNoConfidence = VDeleg -> SpecTransM ctx VDeleg
forall a. a -> SpecTransM ctx a
forall (f :: * -> *) a. Applicative f => a -> f a
pure VDeleg
Agda.NoConfidenceRep
instance SpecTranslate ctx Url where
type SpecRep Url = T.Text
toSpecRep :: Url -> SpecTransM ctx (SpecRep Url)
toSpecRep = Text -> SpecTransM ctx Text
forall a. a -> SpecTransM ctx a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Text -> SpecTransM ctx Text)
-> (Url -> Text) -> Url -> SpecTransM ctx Text
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Url -> Text
urlToText
instance SpecTranslate ctx Anchor where
type SpecRep Anchor = Agda.Anchor
toSpecRep :: Anchor -> SpecTransM ctx (SpecRep Anchor)
toSpecRep (Anchor Url
url SafeHash AnchorData
h) = Text -> Integer -> Anchor
Agda.Anchor (Text -> Integer -> Anchor)
-> SpecTransM ctx Text -> SpecTransM ctx (Integer -> Anchor)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Url -> SpecTransM ctx (SpecRep Url)
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep Url
url SpecTransM ctx (Integer -> Anchor)
-> SpecTransM ctx Integer -> SpecTransM ctx Anchor
forall a b.
SpecTransM ctx (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> SafeHash AnchorData
-> SpecTransM ctx (SpecRep (SafeHash AnchorData))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep SafeHash AnchorData
h
instance SpecTranslate ctx TxId where
type SpecRep TxId = Agda.TxId
toSpecRep :: TxId -> SpecTransM ctx (SpecRep TxId)
toSpecRep (TxId SafeHash EraIndependentTxBody
x) = SafeHash EraIndependentTxBody
-> SpecTransM ctx (SpecRep (SafeHash EraIndependentTxBody))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep SafeHash EraIndependentTxBody
x
instance SpecTranslate ctx Withdrawals where
type SpecRep Withdrawals = Agda.Wdrl
toSpecRep :: Withdrawals -> SpecTransM ctx (SpecRep Withdrawals)
toSpecRep (Withdrawals Map RewardAccount Coin
w) = Map RewardAccount Coin
-> SpecTransM ctx (SpecRep (Map RewardAccount Coin))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep Map RewardAccount Coin
w
instance SpecTranslate ctx TxAuxDataHash where
type SpecRep TxAuxDataHash = Agda.DataHash
toSpecRep :: TxAuxDataHash -> SpecTransM ctx (SpecRep TxAuxDataHash)
toSpecRep (TxAuxDataHash SafeHash EraIndependentTxAuxData
x) = SafeHash EraIndependentTxAuxData
-> SpecTransM ctx (SpecRep (SafeHash EraIndependentTxAuxData))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep SafeHash EraIndependentTxAuxData
x
data ConwayTxBodyTransContext = ConwayTxBodyTransContext
{ ConwayTxBodyTransContext -> Integer
ctbtcSizeTx :: !Integer
, ConwayTxBodyTransContext -> TxId
ctbtcTxId :: !TxId
}
instance Inject ConwayTxBodyTransContext Integer where
inject :: ConwayTxBodyTransContext -> Integer
inject = ConwayTxBodyTransContext -> Integer
ctbtcSizeTx
instance Inject ConwayTxBodyTransContext TxId where
inject :: ConwayTxBodyTransContext -> TxId
inject = ConwayTxBodyTransContext -> TxId
ctbtcTxId
instance SpecTranslate ctx IsValid where
type SpecRep IsValid = Bool
toSpecRep :: IsValid -> SpecTransM ctx (SpecRep IsValid)
toSpecRep (IsValid Bool
b) = Bool -> SpecTransM ctx Bool
forall a. a -> SpecTransM ctx a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
b
instance
( SpecTranslate ctx (TxWits era)
, SpecTranslate ctx (TxAuxData era)
, SpecTranslate ConwayTxBodyTransContext (TxBody era)
, SpecRep (TxWits era) ~ Agda.TxWitnesses
, SpecRep (TxAuxData era) ~ Agda.AuxiliaryData
, SpecRep (TxBody era) ~ Agda.TxBody
, Tx era ~ AlonzoTx era
, EraTx era
, BabbageEraTxBody era
) =>
SpecTranslate ctx (AlonzoTx era)
where
type SpecRep (AlonzoTx era) = Agda.Tx
toSpecRep :: AlonzoTx era -> SpecTransM ctx (SpecRep (AlonzoTx era))
toSpecRep AlonzoTx era
tx =
TxBody -> TxWitnesses -> Bool -> Maybe Integer -> Tx
Agda.MkTx
(TxBody -> TxWitnesses -> Bool -> Maybe Integer -> Tx)
-> SpecTransM ctx TxBody
-> SpecTransM ctx (TxWitnesses -> Bool -> Maybe Integer -> Tx)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ConwayTxBodyTransContext
-> SpecTransM ConwayTxBodyTransContext TxBody
-> SpecTransM ctx TxBody
forall ctx a ctx'. ctx -> SpecTransM ctx a -> SpecTransM ctx' a
withCtx
(Integer -> TxId -> ConwayTxBodyTransContext
ConwayTxBodyTransContext (AlonzoTx era
tx AlonzoTx era -> Getting Integer (AlonzoTx era) Integer -> Integer
forall s a. s -> Getting a s a -> a
^. Getting Integer (Tx era) Integer
Getting Integer (AlonzoTx era) Integer
forall era. EraTx era => SimpleGetter (Tx era) Integer
SimpleGetter (Tx era) Integer
sizeTxF) (Tx era -> TxId
forall era. EraTx era => Tx era -> TxId
txIdTx Tx era
AlonzoTx era
tx))
(TxBody era
-> SpecTransM ConwayTxBodyTransContext (SpecRep (TxBody era))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep (AlonzoTx era -> TxBody era
forall era. AlonzoTx era -> TxBody era
body AlonzoTx era
tx))
SpecTransM ctx (TxWitnesses -> Bool -> Maybe Integer -> Tx)
-> SpecTransM ctx TxWitnesses
-> SpecTransM ctx (Bool -> Maybe Integer -> Tx)
forall a b.
SpecTransM ctx (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> TxWits era -> SpecTransM ctx (SpecRep (TxWits era))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep (AlonzoTx era -> TxWits era
forall era. AlonzoTx era -> TxWits era
wits AlonzoTx era
tx)
SpecTransM ctx (Bool -> Maybe Integer -> Tx)
-> SpecTransM ctx Bool -> SpecTransM ctx (Maybe Integer -> Tx)
forall a b.
SpecTransM ctx (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> IsValid -> SpecTransM ctx (SpecRep IsValid)
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep (AlonzoTx era -> IsValid
forall era. AlonzoTx era -> IsValid
isValid AlonzoTx era
tx)
SpecTransM ctx (Maybe Integer -> Tx)
-> SpecTransM ctx (Maybe Integer) -> SpecTransM ctx Tx
forall a b.
SpecTransM ctx (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> StrictMaybe (TxAuxData era)
-> SpecTransM ctx (SpecRep (StrictMaybe (TxAuxData era)))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep (AlonzoTx era -> StrictMaybe (TxAuxData era)
forall era. AlonzoTx era -> StrictMaybe (TxAuxData era)
auxiliaryData AlonzoTx era
tx)
instance
( EraPParams era
, ToExpr (PParamsHKD StrictMaybe era)
) =>
SpecTranslate ctx (ConwayGovPredFailure era)
where
type SpecRep (ConwayGovPredFailure era) = OpaqueErrorString
toSpecRep :: ConwayGovPredFailure era
-> SpecTransM ctx (SpecRep (ConwayGovPredFailure era))
toSpecRep = OpaqueErrorString -> SpecTransM ctx OpaqueErrorString
forall a. a -> SpecTransM ctx a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (OpaqueErrorString -> SpecTransM ctx OpaqueErrorString)
-> (ConwayGovPredFailure era -> OpaqueErrorString)
-> ConwayGovPredFailure era
-> SpecTransM ctx OpaqueErrorString
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ConwayGovPredFailure era -> OpaqueErrorString
forall a. ToExpr a => a -> OpaqueErrorString
showOpaqueErrorString
instance SpecTranslate ctx (GovPurposeId r c) where
type SpecRep (GovPurposeId r c) = (Agda.TxId, Integer)
toSpecRep :: GovPurposeId r c -> SpecTransM ctx (SpecRep (GovPurposeId r c))
toSpecRep (GovPurposeId GovActionId
gaId) = GovActionId -> SpecTransM ctx (SpecRep GovActionId)
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep GovActionId
gaId
instance SpecTranslate ctx UnitInterval where
type SpecRep UnitInterval = Agda.Rational
toSpecRep :: UnitInterval -> SpecTransM ctx (SpecRep UnitInterval)
toSpecRep = Rational -> SpecTransM ctx Rational
forall a. a -> SpecTransM ctx a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rational -> SpecTransM ctx Rational)
-> (UnitInterval -> Rational)
-> UnitInterval
-> SpecTransM ctx Rational
forall b c a. (b -> c) -> (a -> b) -> a -> c
. UnitInterval -> Rational
forall r. BoundedRational r => r -> Rational
unboundRational
instance SpecTranslate ctx (Committee era) where
type SpecRep (Committee era) = (Agda.HSMap Agda.Credential Agda.Epoch, Agda.Rational)
toSpecRep :: Committee era -> SpecTransM ctx (SpecRep (Committee era))
toSpecRep (Committee Map (Credential 'ColdCommitteeRole) EpochNo
members UnitInterval
threshold) = (Map (Credential 'ColdCommitteeRole) EpochNo, UnitInterval)
-> SpecTransM
ctx
(SpecRep
(Map (Credential 'ColdCommitteeRole) EpochNo, UnitInterval))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep (Map (Credential 'ColdCommitteeRole) EpochNo
members, UnitInterval
threshold)
instance SpecTranslate ctx (Constitution era) where
type SpecRep (Constitution era) = (Agda.DataHash, Maybe Agda.ScriptHash)
toSpecRep :: Constitution era -> SpecTransM ctx (SpecRep (Constitution era))
toSpecRep (Constitution (Anchor Url
_ SafeHash AnchorData
h) StrictMaybe ScriptHash
policy) = (SafeHash AnchorData, StrictMaybe ScriptHash)
-> SpecTransM
ctx (SpecRep (SafeHash AnchorData, StrictMaybe ScriptHash))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep (SafeHash AnchorData
h, StrictMaybe ScriptHash
policy)
instance
( EraPParams era
, SpecTranslate ctx (PParamsHKD Identity era)
, SpecRep (PParamsHKD Identity era) ~ Agda.PParams
) =>
SpecTranslate ctx (EnactState era)
where
type SpecRep (EnactState era) = Agda.EnactState
toSpecRep :: EnactState era -> SpecTransM ctx (SpecRep (EnactState era))
toSpecRep EnactState {Map StakeCredential Coin
StrictMaybe (Committee era)
PParams era
Constitution era
GovRelation StrictMaybe era
Coin
ensCommittee :: StrictMaybe (Committee era)
ensConstitution :: Constitution era
ensCurPParams :: PParams era
ensPrevPParams :: PParams era
ensTreasury :: Coin
ensWithdrawals :: Map StakeCredential Coin
ensPrevGovActionIds :: GovRelation StrictMaybe era
ensCommittee :: forall era. EnactState era -> StrictMaybe (Committee era)
ensConstitution :: forall era. EnactState era -> Constitution era
ensCurPParams :: forall era. EnactState era -> PParams era
ensPrevPParams :: forall era. EnactState era -> PParams era
ensTreasury :: forall era. EnactState era -> Coin
ensWithdrawals :: forall era. EnactState era -> Map StakeCredential Coin
ensPrevGovActionIds :: forall era. EnactState era -> GovRelation StrictMaybe era
..} =
(Maybe (HSMap Credential Integer, Rational), (Integer, Integer))
-> ((Integer, Maybe Integer), (Integer, Integer))
-> ((Integer, Integer), (Integer, Integer))
-> (PParams, (Integer, Integer))
-> HSMap RwdAddr Integer
-> EnactState
Agda.MkEnactState
((Maybe (HSMap Credential Integer, Rational), (Integer, Integer))
-> ((Integer, Maybe Integer), (Integer, Integer))
-> ((Integer, Integer), (Integer, Integer))
-> (PParams, (Integer, Integer))
-> HSMap RwdAddr Integer
-> EnactState)
-> SpecTransM
ctx
(Maybe (HSMap Credential Integer, Rational), (Integer, Integer))
-> SpecTransM
ctx
(((Integer, Maybe Integer), (Integer, Integer))
-> ((Integer, Integer), (Integer, Integer))
-> (PParams, (Integer, Integer))
-> HSMap RwdAddr Integer
-> EnactState)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StrictMaybe (Committee era)
-> StrictMaybe (GovPurposeId 'CommitteePurpose era)
-> SpecTransM
ctx (SpecRep (StrictMaybe (Committee era)), (Integer, Integer))
forall {a} {a} {b} {ctx} {a}.
(SpecRep a ~ (a, b), SpecTranslate ctx a, SpecTranslate ctx a,
Num a, Num b) =>
a -> StrictMaybe a -> SpecTransM ctx (SpecRep a, (a, b))
transHashProtected StrictMaybe (Committee era)
ensCommittee StrictMaybe (GovPurposeId 'CommitteePurpose era)
grCommittee
SpecTransM
ctx
(((Integer, Maybe Integer), (Integer, Integer))
-> ((Integer, Integer), (Integer, Integer))
-> (PParams, (Integer, Integer))
-> HSMap RwdAddr Integer
-> EnactState)
-> SpecTransM ctx ((Integer, Maybe Integer), (Integer, Integer))
-> SpecTransM
ctx
(((Integer, Integer), (Integer, Integer))
-> (PParams, (Integer, Integer))
-> HSMap RwdAddr Integer
-> EnactState)
forall a b.
SpecTransM ctx (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Constitution era
-> StrictMaybe (GovPurposeId 'ConstitutionPurpose era)
-> SpecTransM ctx (SpecRep (Constitution era), (Integer, Integer))
forall {a} {a} {b} {ctx} {a}.
(SpecRep a ~ (a, b), SpecTranslate ctx a, SpecTranslate ctx a,
Num a, Num b) =>
a -> StrictMaybe a -> SpecTransM ctx (SpecRep a, (a, b))
transHashProtected Constitution era
ensConstitution StrictMaybe (GovPurposeId 'ConstitutionPurpose era)
grConstitution
SpecTransM
ctx
(((Integer, Integer), (Integer, Integer))
-> (PParams, (Integer, Integer))
-> HSMap RwdAddr Integer
-> EnactState)
-> SpecTransM ctx ((Integer, Integer), (Integer, Integer))
-> SpecTransM
ctx
((PParams, (Integer, Integer))
-> HSMap RwdAddr Integer -> EnactState)
forall a b.
SpecTransM ctx (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ProtVer
-> StrictMaybe (GovPurposeId 'HardForkPurpose era)
-> SpecTransM ctx (SpecRep ProtVer, (Integer, Integer))
forall {a} {a} {b} {ctx} {a}.
(SpecRep a ~ (a, b), SpecTranslate ctx a, SpecTranslate ctx a,
Num a, Num b) =>
a -> StrictMaybe a -> SpecTransM ctx (SpecRep a, (a, b))
transHashProtected (PParams era
ensCurPParams PParams era -> Getting ProtVer (PParams era) ProtVer -> ProtVer
forall s a. s -> Getting a s a -> a
^. Getting ProtVer (PParams era) ProtVer
forall era. EraPParams era => Lens' (PParams era) ProtVer
Lens' (PParams era) ProtVer
ppProtocolVersionL) StrictMaybe (GovPurposeId 'HardForkPurpose era)
grHardFork
SpecTransM
ctx
((PParams, (Integer, Integer))
-> HSMap RwdAddr Integer -> EnactState)
-> SpecTransM ctx (PParams, (Integer, Integer))
-> SpecTransM ctx (HSMap RwdAddr Integer -> EnactState)
forall a b.
SpecTransM ctx (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> PParams era
-> StrictMaybe (GovPurposeId 'PParamUpdatePurpose era)
-> SpecTransM ctx (SpecRep (PParams era), (Integer, Integer))
forall {a} {a} {b} {ctx} {a}.
(SpecRep a ~ (a, b), SpecTranslate ctx a, SpecTranslate ctx a,
Num a, Num b) =>
a -> StrictMaybe a -> SpecTransM ctx (SpecRep a, (a, b))
transHashProtected PParams era
ensCurPParams StrictMaybe (GovPurposeId 'PParamUpdatePurpose era)
grPParamUpdate
SpecTransM ctx (HSMap RwdAddr Integer -> EnactState)
-> SpecTransM ctx (HSMap RwdAddr Integer)
-> SpecTransM ctx EnactState
forall a b.
SpecTransM ctx (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Map StakeCredential Coin -> SpecTransM ctx (HSMap RwdAddr Integer)
forall {a} {ctx}.
(SpecRep a ~ Credential, SpecTranslate ctx a) =>
Map a Coin -> SpecTransM ctx (HSMap RwdAddr Integer)
transWithdrawals Map StakeCredential Coin
ensWithdrawals
where
GovRelation {StrictMaybe (GovPurposeId 'PParamUpdatePurpose era)
StrictMaybe (GovPurposeId 'HardForkPurpose era)
StrictMaybe (GovPurposeId 'CommitteePurpose era)
StrictMaybe (GovPurposeId 'ConstitutionPurpose era)
grCommittee :: StrictMaybe (GovPurposeId 'CommitteePurpose era)
grConstitution :: StrictMaybe (GovPurposeId 'ConstitutionPurpose era)
grHardFork :: StrictMaybe (GovPurposeId 'HardForkPurpose era)
grPParamUpdate :: StrictMaybe (GovPurposeId 'PParamUpdatePurpose era)
grPParamUpdate :: forall (f :: * -> *) era.
GovRelation f era -> f (GovPurposeId 'PParamUpdatePurpose era)
grHardFork :: forall (f :: * -> *) era.
GovRelation f era -> f (GovPurposeId 'HardForkPurpose era)
grCommittee :: forall (f :: * -> *) era.
GovRelation f era -> f (GovPurposeId 'CommitteePurpose era)
grConstitution :: forall (f :: * -> *) era.
GovRelation f era -> f (GovPurposeId 'ConstitutionPurpose era)
..} = GovRelation StrictMaybe era
ensPrevGovActionIds
transWithdrawals :: Map a Coin -> SpecTransM ctx (HSMap RwdAddr Integer)
transWithdrawals Map a Coin
ws = ([(RwdAddr, Integer)] -> HSMap RwdAddr Integer)
-> SpecTransM ctx [(RwdAddr, Integer)]
-> SpecTransM ctx (HSMap RwdAddr Integer)
forall a b. (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [(RwdAddr, Integer)] -> HSMap RwdAddr Integer
forall k v. [(k, v)] -> HSMap k v
Agda.MkHSMap (SpecTransM ctx [(RwdAddr, Integer)]
-> SpecTransM ctx (HSMap RwdAddr Integer))
-> (((a, Coin) -> SpecTransM ctx (RwdAddr, Integer))
-> SpecTransM ctx [(RwdAddr, Integer)])
-> ((a, Coin) -> SpecTransM ctx (RwdAddr, Integer))
-> SpecTransM ctx (HSMap RwdAddr Integer)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(a, Coin)]
-> ((a, Coin) -> SpecTransM ctx (RwdAddr, Integer))
-> SpecTransM ctx [(RwdAddr, Integer)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM (Map a Coin -> [(a, Coin)]
forall k a. Map k a -> [(k, a)]
Map.toList Map a Coin
ws) (((a, Coin) -> SpecTransM ctx (RwdAddr, Integer))
-> SpecTransM ctx (HSMap RwdAddr Integer))
-> ((a, Coin) -> SpecTransM ctx (RwdAddr, Integer))
-> SpecTransM ctx (HSMap RwdAddr Integer)
forall a b. (a -> b) -> a -> b
$
\(a
cred, Coin Integer
amount) -> do
Credential
agdaCred <- a -> SpecTransM ctx (SpecRep a)
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep a
cred
Integer
network <- Network -> SpecTransM ctx (SpecRep Network)
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep Network
Testnet
(RwdAddr, Integer) -> SpecTransM ctx (RwdAddr, Integer)
forall a. a -> SpecTransM ctx a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Integer -> Credential -> RwdAddr
Agda.RwdAddr Integer
network Credential
agdaCred, Integer
amount)
transHashProtected :: a -> StrictMaybe a -> SpecTransM ctx (SpecRep a, (a, b))
transHashProtected a
x StrictMaybe a
h = do
SpecRep a
committee <- a -> SpecTransM ctx (SpecRep a)
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep a
x
(a, b)
agdaLastId <- case StrictMaybe a
h of
SJust a
lastId -> a -> SpecTransM ctx (SpecRep a)
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep a
lastId
StrictMaybe a
SNothing -> (a, b) -> SpecTransM ctx (a, b)
forall a. a -> SpecTransM ctx a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (a
0, b
0)
(SpecRep a, (a, b)) -> SpecTransM ctx (SpecRep a, (a, b))
forall a. a -> SpecTransM ctx a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SpecRep a
committee, (a, b)
agdaLastId)
instance SpecTranslate ctx Voter where
type SpecRep Voter = Agda.Voter
toSpecRep :: Voter -> SpecTransM ctx (SpecRep Voter)
toSpecRep (CommitteeVoter Credential 'HotCommitteeRole
c) = (GovRole
Agda.CC,) (Credential -> (GovRole, Credential))
-> SpecTransM ctx Credential
-> SpecTransM ctx (GovRole, Credential)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Credential 'HotCommitteeRole
-> SpecTransM ctx (SpecRep (Credential 'HotCommitteeRole))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep Credential 'HotCommitteeRole
c
toSpecRep (DRepVoter Credential 'DRepRole
c) = (GovRole
Agda.DRep,) (Credential -> (GovRole, Credential))
-> SpecTransM ctx Credential
-> SpecTransM ctx (GovRole, Credential)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Credential 'DRepRole
-> SpecTransM ctx (SpecRep (Credential 'DRepRole))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep Credential 'DRepRole
c
toSpecRep (StakePoolVoter KeyHash 'StakePool
kh) = (GovRole
Agda.SPO,) (Credential -> (GovRole, Credential))
-> SpecTransM ctx Credential
-> SpecTransM ctx (GovRole, Credential)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Credential 'StakePool
-> SpecTransM ctx (SpecRep (Credential 'StakePool))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep (KeyHash 'StakePool -> Credential 'StakePool
forall (kr :: KeyRole). KeyHash kr -> Credential kr
KeyHashObj KeyHash 'StakePool
kh)
instance SpecTranslate ctx Vote where
type SpecRep Vote = Agda.Vote
toSpecRep :: Vote -> SpecTransM ctx (SpecRep Vote)
toSpecRep Vote
VoteYes = Vote -> SpecTransM ctx Vote
forall a. a -> SpecTransM ctx a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Vote
Agda.Yes
toSpecRep Vote
VoteNo = Vote -> SpecTransM ctx Vote
forall a. a -> SpecTransM ctx a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Vote
Agda.No
toSpecRep Vote
Abstain = Vote -> SpecTransM ctx Vote
forall a. a -> SpecTransM ctx a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Vote
Agda.Abstain
instance SpecTranslate ctx (VotingProcedures era) where
type SpecRep (VotingProcedures era) = [Agda.GovVote]
toSpecRep :: VotingProcedures era
-> SpecTransM ctx (SpecRep (VotingProcedures era))
toSpecRep = (Voter
-> GovActionId
-> VotingProcedure era
-> SpecTransM ctx [GovVote]
-> SpecTransM ctx [GovVote])
-> SpecTransM ctx [GovVote]
-> VotingProcedures era
-> SpecTransM ctx [GovVote]
forall era c.
(Voter -> GovActionId -> VotingProcedure era -> c -> c)
-> c -> VotingProcedures era -> c
foldrVotingProcedures Voter
-> GovActionId
-> VotingProcedure era
-> SpecTransM ctx [GovVote]
-> SpecTransM ctx [GovVote]
go ([GovVote] -> SpecTransM ctx [GovVote]
forall a. a -> SpecTransM ctx a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [])
where
go ::
Voter ->
GovActionId ->
VotingProcedure era ->
SpecTransM ctx [Agda.GovVote] ->
SpecTransM ctx [Agda.GovVote]
go :: Voter
-> GovActionId
-> VotingProcedure era
-> SpecTransM ctx [GovVote]
-> SpecTransM ctx [GovVote]
go Voter
voter GovActionId
gaId VotingProcedure era
votingProcedure SpecTransM ctx [GovVote]
m =
(:)
(GovVote -> [GovVote] -> [GovVote])
-> SpecTransM ctx GovVote
-> SpecTransM ctx ([GovVote] -> [GovVote])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ( (Integer, Integer)
-> (GovRole, Credential) -> Vote -> Maybe Anchor -> GovVote
Agda.GovVote
((Integer, Integer)
-> (GovRole, Credential) -> Vote -> Maybe Anchor -> GovVote)
-> SpecTransM ctx (Integer, Integer)
-> SpecTransM
ctx ((GovRole, Credential) -> Vote -> Maybe Anchor -> GovVote)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> GovActionId -> SpecTransM ctx (SpecRep GovActionId)
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep GovActionId
gaId
SpecTransM
ctx ((GovRole, Credential) -> Vote -> Maybe Anchor -> GovVote)
-> SpecTransM ctx (GovRole, Credential)
-> SpecTransM ctx (Vote -> Maybe Anchor -> GovVote)
forall a b.
SpecTransM ctx (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Voter -> SpecTransM ctx (SpecRep Voter)
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep Voter
voter
SpecTransM ctx (Vote -> Maybe Anchor -> GovVote)
-> SpecTransM ctx Vote -> SpecTransM ctx (Maybe Anchor -> GovVote)
forall a b.
SpecTransM ctx (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Vote -> SpecTransM ctx (SpecRep Vote)
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep (VotingProcedure era -> Vote
forall era. VotingProcedure era -> Vote
vProcVote VotingProcedure era
votingProcedure)
SpecTransM ctx (Maybe Anchor -> GovVote)
-> SpecTransM ctx (Maybe Anchor) -> SpecTransM ctx GovVote
forall a b.
SpecTransM ctx (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> StrictMaybe Anchor -> SpecTransM ctx (SpecRep (StrictMaybe Anchor))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep (VotingProcedure era -> StrictMaybe Anchor
forall era. VotingProcedure era -> StrictMaybe Anchor
vProcAnchor VotingProcedure era
votingProcedure)
)
SpecTransM ctx ([GovVote] -> [GovVote])
-> SpecTransM ctx [GovVote] -> SpecTransM ctx [GovVote]
forall a b.
SpecTransM ctx (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> SpecTransM ctx [GovVote]
m
instance SpecTranslate ctx Word16 where
type SpecRep Word16 = Integer
toSpecRep :: Word16 -> SpecTransM ctx (SpecRep Word16)
toSpecRep = Integer -> SpecTransM ctx Integer
forall a. a -> SpecTransM ctx a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Integer -> SpecTransM ctx Integer)
-> (Word16 -> Integer) -> Word16 -> SpecTransM ctx Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Word16 -> Integer
forall a. Integral a => a -> Integer
toInteger
instance SpecTranslate ctx NonNegativeInterval where
type SpecRep NonNegativeInterval = Agda.Rational
toSpecRep :: NonNegativeInterval -> SpecTransM ctx (SpecRep NonNegativeInterval)
toSpecRep = Rational -> SpecTransM ctx Rational
forall a. a -> SpecTransM ctx a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rational -> SpecTransM ctx Rational)
-> (NonNegativeInterval -> Rational)
-> NonNegativeInterval
-> SpecTransM ctx Rational
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NonNegativeInterval -> Rational
forall r. BoundedRational r => r -> Rational
unboundRational
instance SpecTranslate ctx (ConwayPParams StrictMaybe era) where
type SpecRep (ConwayPParams StrictMaybe era) = Agda.PParamsUpdate
toSpecRep :: ConwayPParams StrictMaybe era
-> SpecTransM ctx (SpecRep (ConwayPParams StrictMaybe era))
toSpecRep (ConwayPParams {THKD ('PPGroups 'NetworkGroup 'SecurityGroup) StrictMaybe Word16
THKD ('PPGroups 'NetworkGroup 'SecurityGroup) StrictMaybe Word32
THKD
('PPGroups 'NetworkGroup 'SecurityGroup) StrictMaybe OrdExUnits
THKD ('PPGroups 'NetworkGroup 'NoStakePoolGroup) StrictMaybe Word16
THKD
('PPGroups 'NetworkGroup 'NoStakePoolGroup) StrictMaybe OrdExUnits
THKD
('PPGroups 'EconomicGroup 'SecurityGroup) StrictMaybe CoinPerByte
THKD ('PPGroups 'EconomicGroup 'SecurityGroup) StrictMaybe Coin
THKD
('PPGroups 'EconomicGroup 'SecurityGroup)
StrictMaybe
NonNegativeInterval
THKD
('PPGroups 'EconomicGroup 'NoStakePoolGroup) StrictMaybe Prices
THKD ('PPGroups 'EconomicGroup 'NoStakePoolGroup) StrictMaybe Coin
THKD
('PPGroups 'EconomicGroup 'NoStakePoolGroup)
StrictMaybe
UnitInterval
THKD
('PPGroups 'TechnicalGroup 'NoStakePoolGroup) StrictMaybe Word16
THKD
('PPGroups 'TechnicalGroup 'NoStakePoolGroup)
StrictMaybe
CostModels
THKD
('PPGroups 'TechnicalGroup 'NoStakePoolGroup)
StrictMaybe
EpochInterval
THKD
('PPGroups 'TechnicalGroup 'NoStakePoolGroup)
StrictMaybe
NonNegativeInterval
THKD ('PPGroups 'GovGroup 'SecurityGroup) StrictMaybe Coin
THKD ('PPGroups 'GovGroup 'NoStakePoolGroup) StrictMaybe Word16
THKD ('PPGroups 'GovGroup 'NoStakePoolGroup) StrictMaybe Coin
THKD
('PPGroups 'GovGroup 'NoStakePoolGroup)
StrictMaybe
DRepVotingThresholds
THKD
('PPGroups 'GovGroup 'NoStakePoolGroup)
StrictMaybe
PoolVotingThresholds
THKD
('PPGroups 'GovGroup 'NoStakePoolGroup) StrictMaybe EpochInterval
HKDNoUpdate StrictMaybe ProtVer
cppMinFeeA :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD ('PPGroups 'EconomicGroup 'SecurityGroup) f Coin
cppMinFeeB :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD ('PPGroups 'EconomicGroup 'SecurityGroup) f Coin
cppMaxBBSize :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD ('PPGroups 'NetworkGroup 'SecurityGroup) f Word32
cppMaxTxSize :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD ('PPGroups 'NetworkGroup 'SecurityGroup) f Word32
cppMaxBHSize :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD ('PPGroups 'NetworkGroup 'SecurityGroup) f Word16
cppKeyDeposit :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD ('PPGroups 'EconomicGroup 'NoStakePoolGroup) f Coin
cppPoolDeposit :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD ('PPGroups 'EconomicGroup 'NoStakePoolGroup) f Coin
cppEMax :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD
('PPGroups 'TechnicalGroup 'NoStakePoolGroup) f EpochInterval
cppNOpt :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD ('PPGroups 'TechnicalGroup 'NoStakePoolGroup) f Word16
cppA0 :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD
('PPGroups 'TechnicalGroup 'NoStakePoolGroup) f NonNegativeInterval
cppRho :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD ('PPGroups 'EconomicGroup 'NoStakePoolGroup) f UnitInterval
cppTau :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD ('PPGroups 'EconomicGroup 'NoStakePoolGroup) f UnitInterval
cppProtocolVersion :: forall (f :: * -> *) era.
ConwayPParams f era -> HKDNoUpdate f ProtVer
cppMinPoolCost :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD ('PPGroups 'EconomicGroup 'NoStakePoolGroup) f Coin
cppCoinsPerUTxOByte :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD ('PPGroups 'EconomicGroup 'SecurityGroup) f CoinPerByte
cppCostModels :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD ('PPGroups 'TechnicalGroup 'NoStakePoolGroup) f CostModels
cppPrices :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD ('PPGroups 'EconomicGroup 'NoStakePoolGroup) f Prices
cppMaxTxExUnits :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD ('PPGroups 'NetworkGroup 'NoStakePoolGroup) f OrdExUnits
cppMaxBlockExUnits :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD ('PPGroups 'NetworkGroup 'SecurityGroup) f OrdExUnits
cppMaxValSize :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD ('PPGroups 'NetworkGroup 'SecurityGroup) f Word32
cppCollateralPercentage :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD ('PPGroups 'TechnicalGroup 'NoStakePoolGroup) f Word16
cppMaxCollateralInputs :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD ('PPGroups 'NetworkGroup 'NoStakePoolGroup) f Word16
cppPoolVotingThresholds :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD
('PPGroups 'GovGroup 'NoStakePoolGroup) f PoolVotingThresholds
cppDRepVotingThresholds :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD
('PPGroups 'GovGroup 'NoStakePoolGroup) f DRepVotingThresholds
cppCommitteeMinSize :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD ('PPGroups 'GovGroup 'NoStakePoolGroup) f Word16
cppCommitteeMaxTermLength :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD ('PPGroups 'GovGroup 'NoStakePoolGroup) f EpochInterval
cppGovActionLifetime :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD ('PPGroups 'GovGroup 'NoStakePoolGroup) f EpochInterval
cppGovActionDeposit :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD ('PPGroups 'GovGroup 'SecurityGroup) f Coin
cppDRepDeposit :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD ('PPGroups 'GovGroup 'NoStakePoolGroup) f Coin
cppDRepActivity :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD ('PPGroups 'GovGroup 'NoStakePoolGroup) f EpochInterval
cppMinFeeRefScriptCostPerByte :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD
('PPGroups 'EconomicGroup 'SecurityGroup) f NonNegativeInterval
cppMinFeeA :: THKD ('PPGroups 'EconomicGroup 'SecurityGroup) StrictMaybe Coin
cppMinFeeB :: THKD ('PPGroups 'EconomicGroup 'SecurityGroup) StrictMaybe Coin
cppMaxBBSize :: THKD ('PPGroups 'NetworkGroup 'SecurityGroup) StrictMaybe Word32
cppMaxTxSize :: THKD ('PPGroups 'NetworkGroup 'SecurityGroup) StrictMaybe Word32
cppMaxBHSize :: THKD ('PPGroups 'NetworkGroup 'SecurityGroup) StrictMaybe Word16
cppKeyDeposit :: THKD ('PPGroups 'EconomicGroup 'NoStakePoolGroup) StrictMaybe Coin
cppPoolDeposit :: THKD ('PPGroups 'EconomicGroup 'NoStakePoolGroup) StrictMaybe Coin
cppEMax :: THKD
('PPGroups 'TechnicalGroup 'NoStakePoolGroup)
StrictMaybe
EpochInterval
cppNOpt :: THKD
('PPGroups 'TechnicalGroup 'NoStakePoolGroup) StrictMaybe Word16
cppA0 :: THKD
('PPGroups 'TechnicalGroup 'NoStakePoolGroup)
StrictMaybe
NonNegativeInterval
cppRho :: THKD
('PPGroups 'EconomicGroup 'NoStakePoolGroup)
StrictMaybe
UnitInterval
cppTau :: THKD
('PPGroups 'EconomicGroup 'NoStakePoolGroup)
StrictMaybe
UnitInterval
cppProtocolVersion :: HKDNoUpdate StrictMaybe ProtVer
cppMinPoolCost :: THKD ('PPGroups 'EconomicGroup 'NoStakePoolGroup) StrictMaybe Coin
cppCoinsPerUTxOByte :: THKD
('PPGroups 'EconomicGroup 'SecurityGroup) StrictMaybe CoinPerByte
cppCostModels :: THKD
('PPGroups 'TechnicalGroup 'NoStakePoolGroup)
StrictMaybe
CostModels
cppPrices :: THKD
('PPGroups 'EconomicGroup 'NoStakePoolGroup) StrictMaybe Prices
cppMaxTxExUnits :: THKD
('PPGroups 'NetworkGroup 'NoStakePoolGroup) StrictMaybe OrdExUnits
cppMaxBlockExUnits :: THKD
('PPGroups 'NetworkGroup 'SecurityGroup) StrictMaybe OrdExUnits
cppMaxValSize :: THKD ('PPGroups 'NetworkGroup 'SecurityGroup) StrictMaybe Word32
cppCollateralPercentage :: THKD
('PPGroups 'TechnicalGroup 'NoStakePoolGroup) StrictMaybe Word16
cppMaxCollateralInputs :: THKD ('PPGroups 'NetworkGroup 'NoStakePoolGroup) StrictMaybe Word16
cppPoolVotingThresholds :: THKD
('PPGroups 'GovGroup 'NoStakePoolGroup)
StrictMaybe
PoolVotingThresholds
cppDRepVotingThresholds :: THKD
('PPGroups 'GovGroup 'NoStakePoolGroup)
StrictMaybe
DRepVotingThresholds
cppCommitteeMinSize :: THKD ('PPGroups 'GovGroup 'NoStakePoolGroup) StrictMaybe Word16
cppCommitteeMaxTermLength :: THKD
('PPGroups 'GovGroup 'NoStakePoolGroup) StrictMaybe EpochInterval
cppGovActionLifetime :: THKD
('PPGroups 'GovGroup 'NoStakePoolGroup) StrictMaybe EpochInterval
cppGovActionDeposit :: THKD ('PPGroups 'GovGroup 'SecurityGroup) StrictMaybe Coin
cppDRepDeposit :: THKD ('PPGroups 'GovGroup 'NoStakePoolGroup) StrictMaybe Coin
cppDRepActivity :: THKD
('PPGroups 'GovGroup 'NoStakePoolGroup) StrictMaybe EpochInterval
cppMinFeeRefScriptCostPerByte :: THKD
('PPGroups 'EconomicGroup 'SecurityGroup)
StrictMaybe
NonNegativeInterval
..}) = do
Maybe Integer
ppuA <- THKD ('PPGroups 'EconomicGroup 'SecurityGroup) StrictMaybe Coin
-> SpecTransM
ctx
(SpecRep
(THKD ('PPGroups 'EconomicGroup 'SecurityGroup) StrictMaybe Coin))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep THKD ('PPGroups 'EconomicGroup 'SecurityGroup) StrictMaybe Coin
cppMinFeeA
Maybe Integer
ppuB <- THKD ('PPGroups 'EconomicGroup 'SecurityGroup) StrictMaybe Coin
-> SpecTransM
ctx
(SpecRep
(THKD ('PPGroups 'EconomicGroup 'SecurityGroup) StrictMaybe Coin))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep THKD ('PPGroups 'EconomicGroup 'SecurityGroup) StrictMaybe Coin
cppMinFeeB
Maybe Rational
ppuA0 <- THKD
('PPGroups 'TechnicalGroup 'NoStakePoolGroup)
StrictMaybe
NonNegativeInterval
-> SpecTransM
ctx
(SpecRep
(THKD
('PPGroups 'TechnicalGroup 'NoStakePoolGroup)
StrictMaybe
NonNegativeInterval))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep THKD
('PPGroups 'TechnicalGroup 'NoStakePoolGroup)
StrictMaybe
NonNegativeInterval
cppA0
Maybe Rational
ppuMinFeeRefScriptCoinsPerByte <- THKD
('PPGroups 'EconomicGroup 'SecurityGroup)
StrictMaybe
NonNegativeInterval
-> SpecTransM
ctx
(SpecRep
(THKD
('PPGroups 'EconomicGroup 'SecurityGroup)
StrictMaybe
NonNegativeInterval))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep THKD
('PPGroups 'EconomicGroup 'SecurityGroup)
StrictMaybe
NonNegativeInterval
cppMinFeeRefScriptCostPerByte
Maybe Integer
ppuCollateralPercentage <- THKD
('PPGroups 'TechnicalGroup 'NoStakePoolGroup) StrictMaybe Word16
-> SpecTransM
ctx
(SpecRep
(THKD
('PPGroups 'TechnicalGroup 'NoStakePoolGroup) StrictMaybe Word16))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep THKD
('PPGroups 'TechnicalGroup 'NoStakePoolGroup) StrictMaybe Word16
cppCollateralPercentage
let
ppuMaxBlockSize :: Maybe Integer
ppuMaxBlockSize = (Word32 -> Integer) -> Maybe Word32 -> Maybe Integer
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Word32 -> Integer
forall a. Integral a => a -> Integer
toInteger (Maybe Word32 -> Maybe Integer)
-> (THKD
('PPGroups 'NetworkGroup 'SecurityGroup) StrictMaybe Word32
-> Maybe Word32)
-> THKD ('PPGroups 'NetworkGroup 'SecurityGroup) StrictMaybe Word32
-> Maybe Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. StrictMaybe Word32 -> Maybe Word32
forall a. StrictMaybe a -> Maybe a
strictMaybeToMaybe (StrictMaybe Word32 -> Maybe Word32)
-> (THKD
('PPGroups 'NetworkGroup 'SecurityGroup) StrictMaybe Word32
-> StrictMaybe Word32)
-> THKD ('PPGroups 'NetworkGroup 'SecurityGroup) StrictMaybe Word32
-> Maybe Word32
forall b c a. (b -> c) -> (a -> b) -> a -> c
. THKD ('PPGroups 'NetworkGroup 'SecurityGroup) StrictMaybe Word32
-> StrictMaybe Word32
THKD ('PPGroups 'NetworkGroup 'SecurityGroup) StrictMaybe Word32
-> HKD StrictMaybe Word32
forall (t :: PPGroups) (f :: * -> *) a. THKD t f a -> HKD f a
unTHKD (THKD ('PPGroups 'NetworkGroup 'SecurityGroup) StrictMaybe Word32
-> Maybe Integer)
-> THKD ('PPGroups 'NetworkGroup 'SecurityGroup) StrictMaybe Word32
-> Maybe Integer
forall a b. (a -> b) -> a -> b
$ THKD ('PPGroups 'NetworkGroup 'SecurityGroup) StrictMaybe Word32
cppMaxBBSize
ppuMaxTxSize :: Maybe Integer
ppuMaxTxSize = (Word32 -> Integer) -> Maybe Word32 -> Maybe Integer
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Word32 -> Integer
forall a. Integral a => a -> Integer
toInteger (Maybe Word32 -> Maybe Integer)
-> (THKD
('PPGroups 'NetworkGroup 'SecurityGroup) StrictMaybe Word32
-> Maybe Word32)
-> THKD ('PPGroups 'NetworkGroup 'SecurityGroup) StrictMaybe Word32
-> Maybe Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. StrictMaybe Word32 -> Maybe Word32
forall a. StrictMaybe a -> Maybe a
strictMaybeToMaybe (StrictMaybe Word32 -> Maybe Word32)
-> (THKD
('PPGroups 'NetworkGroup 'SecurityGroup) StrictMaybe Word32
-> StrictMaybe Word32)
-> THKD ('PPGroups 'NetworkGroup 'SecurityGroup) StrictMaybe Word32
-> Maybe Word32
forall b c a. (b -> c) -> (a -> b) -> a -> c
. THKD ('PPGroups 'NetworkGroup 'SecurityGroup) StrictMaybe Word32
-> StrictMaybe Word32
THKD ('PPGroups 'NetworkGroup 'SecurityGroup) StrictMaybe Word32
-> HKD StrictMaybe Word32
forall (t :: PPGroups) (f :: * -> *) a. THKD t f a -> HKD f a
unTHKD (THKD ('PPGroups 'NetworkGroup 'SecurityGroup) StrictMaybe Word32
-> Maybe Integer)
-> THKD ('PPGroups 'NetworkGroup 'SecurityGroup) StrictMaybe Word32
-> Maybe Integer
forall a b. (a -> b) -> a -> b
$ THKD ('PPGroups 'NetworkGroup 'SecurityGroup) StrictMaybe Word32
cppMaxTxSize
ppuMaxHeaderSize :: Maybe Integer
ppuMaxHeaderSize = (Word16 -> Integer) -> Maybe Word16 -> Maybe Integer
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Word16 -> Integer
forall a. Integral a => a -> Integer
toInteger (Maybe Word16 -> Maybe Integer)
-> (THKD
('PPGroups 'NetworkGroup 'SecurityGroup) StrictMaybe Word16
-> Maybe Word16)
-> THKD ('PPGroups 'NetworkGroup 'SecurityGroup) StrictMaybe Word16
-> Maybe Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. StrictMaybe Word16 -> Maybe Word16
forall a. StrictMaybe a -> Maybe a
strictMaybeToMaybe (StrictMaybe Word16 -> Maybe Word16)
-> (THKD
('PPGroups 'NetworkGroup 'SecurityGroup) StrictMaybe Word16
-> StrictMaybe Word16)
-> THKD ('PPGroups 'NetworkGroup 'SecurityGroup) StrictMaybe Word16
-> Maybe Word16
forall b c a. (b -> c) -> (a -> b) -> a -> c
. THKD ('PPGroups 'NetworkGroup 'SecurityGroup) StrictMaybe Word16
-> StrictMaybe Word16
THKD ('PPGroups 'NetworkGroup 'SecurityGroup) StrictMaybe Word16
-> HKD StrictMaybe Word16
forall (t :: PPGroups) (f :: * -> *) a. THKD t f a -> HKD f a
unTHKD (THKD ('PPGroups 'NetworkGroup 'SecurityGroup) StrictMaybe Word16
-> Maybe Integer)
-> THKD ('PPGroups 'NetworkGroup 'SecurityGroup) StrictMaybe Word16
-> Maybe Integer
forall a b. (a -> b) -> a -> b
$ THKD ('PPGroups 'NetworkGroup 'SecurityGroup) StrictMaybe Word16
cppMaxBHSize
Maybe Integer
ppuKeyDeposit <- THKD ('PPGroups 'EconomicGroup 'NoStakePoolGroup) StrictMaybe Coin
-> SpecTransM
ctx
(SpecRep
(THKD
('PPGroups 'EconomicGroup 'NoStakePoolGroup) StrictMaybe Coin))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep THKD ('PPGroups 'EconomicGroup 'NoStakePoolGroup) StrictMaybe Coin
cppKeyDeposit
Maybe Integer
ppuPoolDeposit <- THKD ('PPGroups 'EconomicGroup 'NoStakePoolGroup) StrictMaybe Coin
-> SpecTransM
ctx
(SpecRep
(THKD
('PPGroups 'EconomicGroup 'NoStakePoolGroup) StrictMaybe Coin))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep THKD ('PPGroups 'EconomicGroup 'NoStakePoolGroup) StrictMaybe Coin
cppPoolDeposit
Maybe Integer
ppuEmax <- THKD
('PPGroups 'TechnicalGroup 'NoStakePoolGroup)
StrictMaybe
EpochInterval
-> SpecTransM
ctx
(SpecRep
(THKD
('PPGroups 'TechnicalGroup 'NoStakePoolGroup)
StrictMaybe
EpochInterval))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep THKD
('PPGroups 'TechnicalGroup 'NoStakePoolGroup)
StrictMaybe
EpochInterval
cppEMax
Maybe Integer
ppuNopt <- Maybe Integer -> SpecTransM ctx (SpecRep (Maybe Integer))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep ((Word16 -> Integer) -> Maybe Word16 -> Maybe Integer
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Word16 -> Integer
forall a. Integral a => a -> Integer
toInteger (Maybe Word16 -> Maybe Integer)
-> (StrictMaybe Word16 -> Maybe Word16)
-> StrictMaybe Word16
-> Maybe Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. StrictMaybe Word16 -> Maybe Word16
forall a. StrictMaybe a -> Maybe a
strictMaybeToMaybe (StrictMaybe Word16 -> Maybe Integer)
-> StrictMaybe Word16 -> Maybe Integer
forall a b. (a -> b) -> a -> b
$ THKD
('PPGroups 'TechnicalGroup 'NoStakePoolGroup) StrictMaybe Word16
-> HKD StrictMaybe Word16
forall (t :: PPGroups) (f :: * -> *) a. THKD t f a -> HKD f a
unTHKD THKD
('PPGroups 'TechnicalGroup 'NoStakePoolGroup) StrictMaybe Word16
cppNOpt)
let
ppuPv :: Maybe a
ppuPv = Maybe a
forall a. Maybe a
Nothing
ppuMinUTxOValue :: Maybe a
ppuMinUTxOValue = Maybe a
forall a. Maybe a
Nothing
Maybe Integer
ppuCoinsPerUTxOByte <- THKD
('PPGroups 'EconomicGroup 'SecurityGroup) StrictMaybe CoinPerByte
-> SpecTransM
ctx
(SpecRep
(THKD
('PPGroups 'EconomicGroup 'SecurityGroup) StrictMaybe CoinPerByte))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep THKD
('PPGroups 'EconomicGroup 'SecurityGroup) StrictMaybe CoinPerByte
cppCoinsPerUTxOByte
Maybe ()
ppuCostmdls <- THKD
('PPGroups 'TechnicalGroup 'NoStakePoolGroup)
StrictMaybe
CostModels
-> SpecTransM
ctx
(SpecRep
(THKD
('PPGroups 'TechnicalGroup 'NoStakePoolGroup)
StrictMaybe
CostModels))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep THKD
('PPGroups 'TechnicalGroup 'NoStakePoolGroup)
StrictMaybe
CostModels
cppCostModels
Maybe ()
ppuPrices <- THKD
('PPGroups 'EconomicGroup 'NoStakePoolGroup) StrictMaybe Prices
-> SpecTransM
ctx
(SpecRep
(THKD
('PPGroups 'EconomicGroup 'NoStakePoolGroup) StrictMaybe Prices))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep THKD
('PPGroups 'EconomicGroup 'NoStakePoolGroup) StrictMaybe Prices
cppPrices
let
ppuMaxRefScriptSizePerTx :: Maybe a
ppuMaxRefScriptSizePerTx = Maybe a
forall a. Maybe a
Nothing
ppuMaxRefScriptSizePerBlock :: Maybe a
ppuMaxRefScriptSizePerBlock = Maybe a
forall a. Maybe a
Nothing
ppuRefScriptCostStride :: Maybe a
ppuRefScriptCostStride = Maybe a
forall a. Maybe a
Nothing
ppuRefScriptCostMultiplier :: Maybe a
ppuRefScriptCostMultiplier = Maybe a
forall a. Maybe a
Nothing
Maybe (Integer, Integer)
ppuMaxTxExUnits <- THKD
('PPGroups 'NetworkGroup 'NoStakePoolGroup) StrictMaybe OrdExUnits
-> SpecTransM
ctx
(SpecRep
(THKD
('PPGroups 'NetworkGroup 'NoStakePoolGroup)
StrictMaybe
OrdExUnits))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep THKD
('PPGroups 'NetworkGroup 'NoStakePoolGroup) StrictMaybe OrdExUnits
cppMaxTxExUnits
Maybe (Integer, Integer)
ppuMaxBlockExUnits <- THKD
('PPGroups 'NetworkGroup 'SecurityGroup) StrictMaybe OrdExUnits
-> SpecTransM
ctx
(SpecRep
(THKD
('PPGroups 'NetworkGroup 'SecurityGroup) StrictMaybe OrdExUnits))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep THKD
('PPGroups 'NetworkGroup 'SecurityGroup) StrictMaybe OrdExUnits
cppMaxBlockExUnits
let
ppuMaxValSize :: Maybe Integer
ppuMaxValSize = (Word32 -> Integer) -> Maybe Word32 -> Maybe Integer
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Word32 -> Integer
forall a. Integral a => a -> Integer
toInteger (Maybe Word32 -> Maybe Integer)
-> (THKD
('PPGroups 'NetworkGroup 'SecurityGroup) StrictMaybe Word32
-> Maybe Word32)
-> THKD ('PPGroups 'NetworkGroup 'SecurityGroup) StrictMaybe Word32
-> Maybe Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. StrictMaybe Word32 -> Maybe Word32
forall a. StrictMaybe a -> Maybe a
strictMaybeToMaybe (StrictMaybe Word32 -> Maybe Word32)
-> (THKD
('PPGroups 'NetworkGroup 'SecurityGroup) StrictMaybe Word32
-> StrictMaybe Word32)
-> THKD ('PPGroups 'NetworkGroup 'SecurityGroup) StrictMaybe Word32
-> Maybe Word32
forall b c a. (b -> c) -> (a -> b) -> a -> c
. THKD ('PPGroups 'NetworkGroup 'SecurityGroup) StrictMaybe Word32
-> StrictMaybe Word32
THKD ('PPGroups 'NetworkGroup 'SecurityGroup) StrictMaybe Word32
-> HKD StrictMaybe Word32
forall (t :: PPGroups) (f :: * -> *) a. THKD t f a -> HKD f a
unTHKD (THKD ('PPGroups 'NetworkGroup 'SecurityGroup) StrictMaybe Word32
-> Maybe Integer)
-> THKD ('PPGroups 'NetworkGroup 'SecurityGroup) StrictMaybe Word32
-> Maybe Integer
forall a b. (a -> b) -> a -> b
$ THKD ('PPGroups 'NetworkGroup 'SecurityGroup) StrictMaybe Word32
cppMaxValSize
ppuMaxCollateralInputs :: Maybe Integer
ppuMaxCollateralInputs = (Word16 -> Integer) -> Maybe Word16 -> Maybe Integer
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Word16 -> Integer
forall a. Integral a => a -> Integer
toInteger (Maybe Word16 -> Maybe Integer)
-> (THKD
('PPGroups 'NetworkGroup 'NoStakePoolGroup) StrictMaybe Word16
-> Maybe Word16)
-> THKD
('PPGroups 'NetworkGroup 'NoStakePoolGroup) StrictMaybe Word16
-> Maybe Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. StrictMaybe Word16 -> Maybe Word16
forall a. StrictMaybe a -> Maybe a
strictMaybeToMaybe (StrictMaybe Word16 -> Maybe Word16)
-> (THKD
('PPGroups 'NetworkGroup 'NoStakePoolGroup) StrictMaybe Word16
-> StrictMaybe Word16)
-> THKD
('PPGroups 'NetworkGroup 'NoStakePoolGroup) StrictMaybe Word16
-> Maybe Word16
forall b c a. (b -> c) -> (a -> b) -> a -> c
. THKD ('PPGroups 'NetworkGroup 'NoStakePoolGroup) StrictMaybe Word16
-> StrictMaybe Word16
THKD ('PPGroups 'NetworkGroup 'NoStakePoolGroup) StrictMaybe Word16
-> HKD StrictMaybe Word16
forall (t :: PPGroups) (f :: * -> *) a. THKD t f a -> HKD f a
unTHKD (THKD
('PPGroups 'NetworkGroup 'NoStakePoolGroup) StrictMaybe Word16
-> Maybe Integer)
-> THKD
('PPGroups 'NetworkGroup 'NoStakePoolGroup) StrictMaybe Word16
-> Maybe Integer
forall a b. (a -> b) -> a -> b
$ THKD ('PPGroups 'NetworkGroup 'NoStakePoolGroup) StrictMaybe Word16
cppMaxCollateralInputs
Maybe PoolThresholds
ppuPoolThresholds <- THKD
('PPGroups 'GovGroup 'NoStakePoolGroup)
StrictMaybe
PoolVotingThresholds
-> SpecTransM
ctx
(SpecRep
(THKD
('PPGroups 'GovGroup 'NoStakePoolGroup)
StrictMaybe
PoolVotingThresholds))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep THKD
('PPGroups 'GovGroup 'NoStakePoolGroup)
StrictMaybe
PoolVotingThresholds
cppPoolVotingThresholds
Maybe DrepThresholds
ppuDrepThresholds <- THKD
('PPGroups 'GovGroup 'NoStakePoolGroup)
StrictMaybe
DRepVotingThresholds
-> SpecTransM
ctx
(SpecRep
(THKD
('PPGroups 'GovGroup 'NoStakePoolGroup)
StrictMaybe
DRepVotingThresholds))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep THKD
('PPGroups 'GovGroup 'NoStakePoolGroup)
StrictMaybe
DRepVotingThresholds
cppDRepVotingThresholds
let
ppuCcMinSize :: Maybe Integer
ppuCcMinSize = (Word16 -> Integer) -> Maybe Word16 -> Maybe Integer
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Word16 -> Integer
forall a. Integral a => a -> Integer
toInteger (Maybe Word16 -> Maybe Integer)
-> (StrictMaybe Word16 -> Maybe Word16)
-> StrictMaybe Word16
-> Maybe Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. StrictMaybe Word16 -> Maybe Word16
forall a. StrictMaybe a -> Maybe a
strictMaybeToMaybe (StrictMaybe Word16 -> Maybe Integer)
-> StrictMaybe Word16 -> Maybe Integer
forall a b. (a -> b) -> a -> b
$ THKD ('PPGroups 'GovGroup 'NoStakePoolGroup) StrictMaybe Word16
-> HKD StrictMaybe Word16
forall (t :: PPGroups) (f :: * -> *) a. THKD t f a -> HKD f a
unTHKD THKD ('PPGroups 'GovGroup 'NoStakePoolGroup) StrictMaybe Word16
cppCommitteeMinSize
ppuCcMaxTermLength :: Maybe Integer
ppuCcMaxTermLength =
(EpochInterval -> Integer) -> Maybe EpochInterval -> Maybe Integer
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Word32 -> Integer
forall a. Integral a => a -> Integer
toInteger (Word32 -> Integer)
-> (EpochInterval -> Word32) -> EpochInterval -> Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. EpochInterval -> Word32
unEpochInterval) (Maybe EpochInterval -> Maybe Integer)
-> (StrictMaybe EpochInterval -> Maybe EpochInterval)
-> StrictMaybe EpochInterval
-> Maybe Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. StrictMaybe EpochInterval -> Maybe EpochInterval
forall a. StrictMaybe a -> Maybe a
strictMaybeToMaybe (StrictMaybe EpochInterval -> Maybe Integer)
-> StrictMaybe EpochInterval -> Maybe Integer
forall a b. (a -> b) -> a -> b
$ THKD
('PPGroups 'GovGroup 'NoStakePoolGroup) StrictMaybe EpochInterval
-> HKD StrictMaybe EpochInterval
forall (t :: PPGroups) (f :: * -> *) a. THKD t f a -> HKD f a
unTHKD THKD
('PPGroups 'GovGroup 'NoStakePoolGroup) StrictMaybe EpochInterval
cppCommitteeMaxTermLength
Maybe Integer
ppuGovActionLifetime <- THKD
('PPGroups 'GovGroup 'NoStakePoolGroup) StrictMaybe EpochInterval
-> SpecTransM
ctx
(SpecRep
(THKD
('PPGroups 'GovGroup 'NoStakePoolGroup) StrictMaybe EpochInterval))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep THKD
('PPGroups 'GovGroup 'NoStakePoolGroup) StrictMaybe EpochInterval
cppGovActionLifetime
Maybe Integer
ppuGovActionDeposit <- THKD ('PPGroups 'GovGroup 'SecurityGroup) StrictMaybe Coin
-> SpecTransM
ctx
(SpecRep
(THKD ('PPGroups 'GovGroup 'SecurityGroup) StrictMaybe Coin))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep THKD ('PPGroups 'GovGroup 'SecurityGroup) StrictMaybe Coin
cppGovActionDeposit
Maybe Integer
ppuDrepDeposit <- THKD ('PPGroups 'GovGroup 'NoStakePoolGroup) StrictMaybe Coin
-> SpecTransM
ctx
(SpecRep
(THKD ('PPGroups 'GovGroup 'NoStakePoolGroup) StrictMaybe Coin))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep THKD ('PPGroups 'GovGroup 'NoStakePoolGroup) StrictMaybe Coin
cppDRepDeposit
Maybe Integer
ppuDrepActivity <- THKD
('PPGroups 'GovGroup 'NoStakePoolGroup) StrictMaybe EpochInterval
-> SpecTransM
ctx
(SpecRep
(THKD
('PPGroups 'GovGroup 'NoStakePoolGroup) StrictMaybe EpochInterval))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep THKD
('PPGroups 'GovGroup 'NoStakePoolGroup) StrictMaybe EpochInterval
cppDRepActivity
Maybe Rational
ppuMonetaryExpansion <- THKD
('PPGroups 'EconomicGroup 'NoStakePoolGroup)
StrictMaybe
UnitInterval
-> SpecTransM
ctx
(SpecRep
(THKD
('PPGroups 'EconomicGroup 'NoStakePoolGroup)
StrictMaybe
UnitInterval))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep THKD
('PPGroups 'EconomicGroup 'NoStakePoolGroup)
StrictMaybe
UnitInterval
cppRho
Maybe Rational
ppuTreasuryCut <- THKD
('PPGroups 'EconomicGroup 'NoStakePoolGroup)
StrictMaybe
UnitInterval
-> SpecTransM
ctx
(SpecRep
(THKD
('PPGroups 'EconomicGroup 'NoStakePoolGroup)
StrictMaybe
UnitInterval))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep THKD
('PPGroups 'EconomicGroup 'NoStakePoolGroup)
StrictMaybe
UnitInterval
cppTau
PParamsUpdate -> SpecTransM ctx PParamsUpdate
forall a. a -> SpecTransM ctx a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Agda.MkPParamsUpdate {Maybe Integer
Maybe Rational
Maybe ()
Maybe (Integer, Integer)
Maybe PoolThresholds
Maybe DrepThresholds
forall a. Maybe a
ppuA :: Maybe Integer
ppuB :: Maybe Integer
ppuA0 :: Maybe Rational
ppuMinFeeRefScriptCoinsPerByte :: Maybe Rational
ppuCollateralPercentage :: Maybe Integer
ppuMaxBlockSize :: Maybe Integer
ppuMaxTxSize :: Maybe Integer
ppuMaxHeaderSize :: Maybe Integer
ppuKeyDeposit :: Maybe Integer
ppuPoolDeposit :: Maybe Integer
ppuEmax :: Maybe Integer
ppuNopt :: Maybe Integer
ppuPv :: forall a. Maybe a
ppuMinUTxOValue :: forall a. Maybe a
ppuCoinsPerUTxOByte :: Maybe Integer
ppuCostmdls :: Maybe ()
ppuPrices :: Maybe ()
ppuMaxRefScriptSizePerTx :: forall a. Maybe a
ppuMaxRefScriptSizePerBlock :: forall a. Maybe a
ppuRefScriptCostStride :: forall a. Maybe a
ppuRefScriptCostMultiplier :: forall a. Maybe a
ppuMaxTxExUnits :: Maybe (Integer, Integer)
ppuMaxBlockExUnits :: Maybe (Integer, Integer)
ppuMaxValSize :: Maybe Integer
ppuMaxCollateralInputs :: Maybe Integer
ppuPoolThresholds :: Maybe PoolThresholds
ppuDrepThresholds :: Maybe DrepThresholds
ppuCcMinSize :: Maybe Integer
ppuCcMaxTermLength :: Maybe Integer
ppuGovActionLifetime :: Maybe Integer
ppuGovActionDeposit :: Maybe Integer
ppuDrepDeposit :: Maybe Integer
ppuDrepActivity :: Maybe Integer
ppuMonetaryExpansion :: Maybe Rational
ppuTreasuryCut :: Maybe Rational
ppuMaxBlockSize :: Maybe Integer
ppuMaxTxSize :: Maybe Integer
ppuMaxHeaderSize :: Maybe Integer
ppuMaxValSize :: Maybe Integer
ppuMaxCollateralInputs :: Maybe Integer
ppuMaxTxExUnits :: Maybe (Integer, Integer)
ppuMaxBlockExUnits :: Maybe (Integer, Integer)
ppuPv :: Maybe (Integer, Integer)
ppuA :: Maybe Integer
ppuB :: Maybe Integer
ppuKeyDeposit :: Maybe Integer
ppuPoolDeposit :: Maybe Integer
ppuMonetaryExpansion :: Maybe Rational
ppuTreasuryCut :: Maybe Rational
ppuCoinsPerUTxOByte :: Maybe Integer
ppuPrices :: Maybe ()
ppuMinFeeRefScriptCoinsPerByte :: Maybe Rational
ppuMaxRefScriptSizePerTx :: Maybe Integer
ppuMaxRefScriptSizePerBlock :: Maybe Integer
ppuRefScriptCostStride :: Maybe Integer
ppuRefScriptCostMultiplier :: Maybe Rational
ppuMinUTxOValue :: Maybe Integer
ppuA0 :: Maybe Rational
ppuEmax :: Maybe Integer
ppuNopt :: Maybe Integer
ppuCollateralPercentage :: Maybe Integer
ppuCostmdls :: Maybe ()
ppuDrepThresholds :: Maybe DrepThresholds
ppuPoolThresholds :: Maybe PoolThresholds
ppuGovActionLifetime :: Maybe Integer
ppuGovActionDeposit :: Maybe Integer
ppuDrepDeposit :: Maybe Integer
ppuDrepActivity :: Maybe Integer
ppuCcMinSize :: Maybe Integer
ppuCcMaxTermLength :: Maybe Integer
..}
instance
SpecTranslate ctx (PParamsHKD StrictMaybe era) =>
SpecTranslate ctx (PParamsUpdate era)
where
type SpecRep (PParamsUpdate era) = SpecRep (PParamsHKD StrictMaybe era)
toSpecRep :: PParamsUpdate era -> SpecTransM ctx (SpecRep (PParamsUpdate era))
toSpecRep (PParamsUpdate PParamsHKD StrictMaybe era
ppu) = PParamsHKD StrictMaybe era
-> SpecTransM ctx (SpecRep (PParamsHKD StrictMaybe era))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep PParamsHKD StrictMaybe era
ppu
instance
( EraPParams era
, SpecTranslate ctx (PParamsHKD StrictMaybe era)
, SpecRep (PParamsHKD StrictMaybe era) ~ Agda.PParamsUpdate
) =>
SpecTranslate ctx (GovAction era)
where
type SpecRep (GovAction era) = Agda.GovAction
toSpecRep :: GovAction era -> SpecTransM ctx (SpecRep (GovAction era))
toSpecRep (ParameterChange StrictMaybe (GovPurposeId 'PParamUpdatePurpose era)
_ PParamsUpdate era
ppu StrictMaybe ScriptHash
_) = PParamsUpdate -> GovAction
Agda.ChangePParams (PParamsUpdate -> GovAction)
-> SpecTransM ctx PParamsUpdate -> SpecTransM ctx GovAction
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> PParamsUpdate era -> SpecTransM ctx (SpecRep (PParamsUpdate era))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep PParamsUpdate era
ppu
toSpecRep (HardForkInitiation StrictMaybe (GovPurposeId 'HardForkPurpose era)
_ ProtVer
pv) = (Integer, Integer) -> GovAction
Agda.TriggerHF ((Integer, Integer) -> GovAction)
-> SpecTransM ctx (Integer, Integer) -> SpecTransM ctx GovAction
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ProtVer -> SpecTransM ctx (SpecRep ProtVer)
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep ProtVer
pv
toSpecRep (TreasuryWithdrawals Map RewardAccount Coin
withdrawals StrictMaybe ScriptHash
_) =
HSMap RwdAddr Integer -> GovAction
Agda.TreasuryWdrl
(HSMap RwdAddr Integer -> GovAction)
-> SpecTransM ctx (HSMap RwdAddr Integer)
-> SpecTransM ctx GovAction
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Map RewardAccount Coin
-> SpecTransM ctx (SpecRep (Map RewardAccount Coin))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep Map RewardAccount Coin
withdrawals
toSpecRep (NoConfidence StrictMaybe (GovPurposeId 'CommitteePurpose era)
_) = GovAction -> SpecTransM ctx GovAction
forall a. a -> SpecTransM ctx a
forall (f :: * -> *) a. Applicative f => a -> f a
pure GovAction
Agda.NoConfidence
toSpecRep (UpdateCommittee StrictMaybe (GovPurposeId 'CommitteePurpose era)
_ Set (Credential 'ColdCommitteeRole)
remove Map (Credential 'ColdCommitteeRole) EpochNo
add UnitInterval
threshold) =
HSMap Credential Integer
-> HSSet Credential -> Rational -> GovAction
Agda.UpdateCommittee
(HSMap Credential Integer
-> HSSet Credential -> Rational -> GovAction)
-> SpecTransM ctx (HSMap Credential Integer)
-> SpecTransM ctx (HSSet Credential -> Rational -> GovAction)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Map (Credential 'ColdCommitteeRole) EpochNo
-> SpecTransM
ctx (SpecRep (Map (Credential 'ColdCommitteeRole) EpochNo))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep Map (Credential 'ColdCommitteeRole) EpochNo
add
SpecTransM ctx (HSSet Credential -> Rational -> GovAction)
-> SpecTransM ctx (HSSet Credential)
-> SpecTransM ctx (Rational -> GovAction)
forall a b.
SpecTransM ctx (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Set (Credential 'ColdCommitteeRole)
-> SpecTransM ctx (SpecRep (Set (Credential 'ColdCommitteeRole)))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep Set (Credential 'ColdCommitteeRole)
remove
SpecTransM ctx (Rational -> GovAction)
-> SpecTransM ctx Rational -> SpecTransM ctx GovAction
forall a b.
SpecTransM ctx (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> UnitInterval -> SpecTransM ctx (SpecRep UnitInterval)
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep UnitInterval
threshold
toSpecRep (NewConstitution StrictMaybe (GovPurposeId 'ConstitutionPurpose era)
_ (Constitution (Anchor Url
_ SafeHash AnchorData
h) StrictMaybe ScriptHash
policy)) =
Integer -> Maybe Integer -> GovAction
Agda.NewConstitution
(Integer -> Maybe Integer -> GovAction)
-> SpecTransM ctx Integer
-> SpecTransM ctx (Maybe Integer -> GovAction)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SafeHash AnchorData
-> SpecTransM ctx (SpecRep (SafeHash AnchorData))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep SafeHash AnchorData
h
SpecTransM ctx (Maybe Integer -> GovAction)
-> SpecTransM ctx (Maybe Integer) -> SpecTransM ctx GovAction
forall a b.
SpecTransM ctx (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> StrictMaybe ScriptHash
-> SpecTransM ctx (SpecRep (StrictMaybe ScriptHash))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep StrictMaybe ScriptHash
policy
toSpecRep GovAction era
InfoAction = GovAction -> SpecTransM ctx GovAction
forall a. a -> SpecTransM ctx a
forall (f :: * -> *) a. Applicative f => a -> f a
pure GovAction
Agda.Info
instance SpecTranslate ctx a => SpecTranslate ctx (OSet a) where
type SpecRep (OSet a) = [SpecRep a]
toSpecRep :: OSet a -> SpecTransM ctx (SpecRep (OSet a))
toSpecRep = (a -> SpecTransM ctx (SpecRep a))
-> [a] -> SpecTransM ctx [SpecRep a]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse a -> SpecTransM ctx (SpecRep a)
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep ([a] -> SpecTransM ctx [SpecRep a])
-> (OSet a -> [a]) -> OSet a -> SpecTransM ctx [SpecRep a]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. OSet a -> [a]
forall a. OSet a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList
instance
( SpecTranslate ctx k
, SpecTranslate ctx v
, Ord k
) =>
SpecTranslate ctx (OMap k v)
where
type SpecRep (OMap k v) = [(SpecRep k, SpecRep v)]
toSpecRep :: OMap k v -> SpecTransM ctx (SpecRep (OMap k v))
toSpecRep = ((k, v) -> SpecTransM ctx (SpecRep k, SpecRep v))
-> [(k, v)] -> SpecTransM ctx [(SpecRep k, SpecRep v)]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse ((k -> SpecTransM ctx (SpecRep k))
-> (v -> SpecTransM ctx (SpecRep v))
-> (k, v)
-> SpecTransM ctx (SpecRep k, SpecRep v)
forall (t :: * -> * -> *) (f :: * -> *) a c b d.
(Bitraversable t, Applicative f) =>
(a -> f c) -> (b -> f d) -> t a b -> f (t c d)
bimapM k -> SpecTransM ctx (SpecRep k)
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep v -> SpecTransM ctx (SpecRep v)
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep) ([(k, v)] -> SpecTransM ctx [(SpecRep k, SpecRep v)])
-> (OMap k v -> [(k, v)])
-> OMap k v
-> SpecTransM ctx [(SpecRep k, SpecRep v)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. OMap k v -> [(k, v)]
forall k v. Ord k => OMap k v -> [(k, v)]
OMap.assocList
instance
( EraPParams era
, SpecTranslate ctx (PParamsHKD StrictMaybe era)
, SpecRep (PParamsHKD StrictMaybe era) ~ Agda.PParamsUpdate
) =>
SpecTranslate ctx (ProposalProcedure era)
where
type SpecRep (ProposalProcedure era) = Agda.GovProposal
toSpecRep :: ProposalProcedure era
-> SpecTransM ctx (SpecRep (ProposalProcedure era))
toSpecRep ProposalProcedure {Anchor
GovAction era
RewardAccount
Coin
pProcDeposit :: Coin
pProcReturnAddr :: RewardAccount
pProcGovAction :: GovAction era
pProcAnchor :: Anchor
pProcDeposit :: forall era. ProposalProcedure era -> Coin
pProcReturnAddr :: forall era. ProposalProcedure era -> RewardAccount
pProcGovAction :: forall era. ProposalProcedure era -> GovAction era
pProcAnchor :: forall era. ProposalProcedure era -> Anchor
..} =
GovAction
-> (Integer, Integer)
-> Maybe Integer
-> Integer
-> RwdAddr
-> Anchor
-> GovProposal
Agda.MkGovProposal
(GovAction
-> (Integer, Integer)
-> Maybe Integer
-> Integer
-> RwdAddr
-> Anchor
-> GovProposal)
-> SpecTransM ctx GovAction
-> SpecTransM
ctx
((Integer, Integer)
-> Maybe Integer -> Integer -> RwdAddr -> Anchor -> GovProposal)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> GovAction era -> SpecTransM ctx (SpecRep (GovAction era))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep GovAction era
pProcGovAction
SpecTransM
ctx
((Integer, Integer)
-> Maybe Integer -> Integer -> RwdAddr -> Anchor -> GovProposal)
-> SpecTransM ctx (Integer, Integer)
-> SpecTransM
ctx (Maybe Integer -> Integer -> RwdAddr -> Anchor -> GovProposal)
forall a b.
SpecTransM ctx (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> GovActionId -> SpecTransM ctx (SpecRep GovActionId)
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep (StrictMaybe GovActionId -> GovAction era -> GovActionId
forall era. StrictMaybe GovActionId -> GovAction era -> GovActionId
nullifyIfNotNeeded StrictMaybe GovActionId
prevActionId GovAction era
pProcGovAction)
SpecTransM
ctx (Maybe Integer -> Integer -> RwdAddr -> Anchor -> GovProposal)
-> SpecTransM ctx (Maybe Integer)
-> SpecTransM ctx (Integer -> RwdAddr -> Anchor -> GovProposal)
forall a b.
SpecTransM ctx (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> StrictMaybe ScriptHash
-> SpecTransM ctx (SpecRep (StrictMaybe ScriptHash))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep StrictMaybe ScriptHash
policy
SpecTransM ctx (Integer -> RwdAddr -> Anchor -> GovProposal)
-> SpecTransM ctx Integer
-> SpecTransM ctx (RwdAddr -> Anchor -> GovProposal)
forall a b.
SpecTransM ctx (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Coin -> SpecTransM ctx (SpecRep Coin)
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep Coin
pProcDeposit
SpecTransM ctx (RwdAddr -> Anchor -> GovProposal)
-> SpecTransM ctx RwdAddr -> SpecTransM ctx (Anchor -> GovProposal)
forall a b.
SpecTransM ctx (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> RewardAccount -> SpecTransM ctx (SpecRep RewardAccount)
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep RewardAccount
pProcReturnAddr
SpecTransM ctx (Anchor -> GovProposal)
-> SpecTransM ctx Anchor -> SpecTransM ctx GovProposal
forall a b.
SpecTransM ctx (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Anchor -> SpecTransM ctx (SpecRep Anchor)
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep Anchor
pProcAnchor
where
prevActionId :: StrictMaybe GovActionId
prevActionId = GovAction era -> StrictMaybe GovActionId
forall era. GovAction era -> StrictMaybe GovActionId
prevGovActionId GovAction era
pProcGovAction
policy :: StrictMaybe ScriptHash
policy =
case GovAction era
pProcGovAction of
TreasuryWithdrawals Map RewardAccount Coin
_ StrictMaybe ScriptHash
sh -> StrictMaybe ScriptHash
sh
ParameterChange StrictMaybe (GovPurposeId 'PParamUpdatePurpose era)
_ PParamsUpdate era
_ StrictMaybe ScriptHash
sh -> StrictMaybe ScriptHash
sh
GovAction era
_ -> StrictMaybe ScriptHash
forall a. StrictMaybe a
SNothing
prevGovActionId :: GovAction era -> StrictMaybe GovActionId
prevGovActionId :: forall era. GovAction era -> StrictMaybe GovActionId
prevGovActionId GovAction era
action =
case GovAction era
action of
ParameterChange StrictMaybe (GovPurposeId 'PParamUpdatePurpose era)
x PParamsUpdate era
_ StrictMaybe ScriptHash
_ -> GovPurposeId 'PParamUpdatePurpose era -> GovActionId
forall (p :: GovActionPurpose) era.
GovPurposeId p era -> GovActionId
unGovPurposeId (GovPurposeId 'PParamUpdatePurpose era -> GovActionId)
-> StrictMaybe (GovPurposeId 'PParamUpdatePurpose era)
-> StrictMaybe GovActionId
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StrictMaybe (GovPurposeId 'PParamUpdatePurpose era)
x
HardForkInitiation StrictMaybe (GovPurposeId 'HardForkPurpose era)
x ProtVer
_ -> GovPurposeId 'HardForkPurpose era -> GovActionId
forall (p :: GovActionPurpose) era.
GovPurposeId p era -> GovActionId
unGovPurposeId (GovPurposeId 'HardForkPurpose era -> GovActionId)
-> StrictMaybe (GovPurposeId 'HardForkPurpose era)
-> StrictMaybe GovActionId
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StrictMaybe (GovPurposeId 'HardForkPurpose era)
x
UpdateCommittee StrictMaybe (GovPurposeId 'CommitteePurpose era)
x Set (Credential 'ColdCommitteeRole)
_ Map (Credential 'ColdCommitteeRole) EpochNo
_ UnitInterval
_ -> GovPurposeId 'CommitteePurpose era -> GovActionId
forall (p :: GovActionPurpose) era.
GovPurposeId p era -> GovActionId
unGovPurposeId (GovPurposeId 'CommitteePurpose era -> GovActionId)
-> StrictMaybe (GovPurposeId 'CommitteePurpose era)
-> StrictMaybe GovActionId
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StrictMaybe (GovPurposeId 'CommitteePurpose era)
x
NoConfidence StrictMaybe (GovPurposeId 'CommitteePurpose era)
x -> GovPurposeId 'CommitteePurpose era -> GovActionId
forall (p :: GovActionPurpose) era.
GovPurposeId p era -> GovActionId
unGovPurposeId (GovPurposeId 'CommitteePurpose era -> GovActionId)
-> StrictMaybe (GovPurposeId 'CommitteePurpose era)
-> StrictMaybe GovActionId
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StrictMaybe (GovPurposeId 'CommitteePurpose era)
x
NewConstitution StrictMaybe (GovPurposeId 'ConstitutionPurpose era)
x Constitution era
_ -> GovPurposeId 'ConstitutionPurpose era -> GovActionId
forall (p :: GovActionPurpose) era.
GovPurposeId p era -> GovActionId
unGovPurposeId (GovPurposeId 'ConstitutionPurpose era -> GovActionId)
-> StrictMaybe (GovPurposeId 'ConstitutionPurpose era)
-> StrictMaybe GovActionId
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StrictMaybe (GovPurposeId 'ConstitutionPurpose era)
x
GovAction era
_ -> StrictMaybe GovActionId
forall a. StrictMaybe a
SNothing
nullGovActionId :: GovActionId
nullGovActionId :: GovActionId
nullGovActionId = TxId -> GovActionIx -> GovActionId
GovActionId (SafeHash EraIndependentTxBody -> TxId
TxId SafeHash EraIndependentTxBody
forall a. Default a => a
def) (Word16 -> GovActionIx
GovActionIx Word16
0)
nullifyIfNotNeeded :: StrictMaybe GovActionId -> GovAction era -> GovActionId
nullifyIfNotNeeded :: forall era. StrictMaybe GovActionId -> GovAction era -> GovActionId
nullifyIfNotNeeded StrictMaybe GovActionId
SNothing = GovActionId -> GovAction era -> GovActionId
forall a b. a -> b -> a
const GovActionId
nullGovActionId
nullifyIfNotNeeded (SJust GovActionId
gaId) = \case
TreasuryWithdrawals {} -> GovActionId
nullGovActionId
GovAction era
InfoAction -> GovActionId
nullGovActionId
GovAction era
_ -> GovActionId
gaId
unionsHSMaps :: [Agda.HSMap k v] -> Agda.HSMap k v
unionsHSMaps :: forall k v. [HSMap k v] -> HSMap k v
unionsHSMaps [] = [(k, v)] -> HSMap k v
forall k v. [(k, v)] -> HSMap k v
Agda.MkHSMap []
unionsHSMaps ((Agda.MkHSMap [(k, v)]
x) : [HSMap k v]
xs) =
let Agda.MkHSMap [(k, v)]
xs' = [HSMap k v] -> HSMap k v
forall k v. [HSMap k v] -> HSMap k v
unionsHSMaps [HSMap k v]
xs
in [(k, v)] -> HSMap k v
forall k v. [(k, v)] -> HSMap k v
Agda.MkHSMap ([(k, v)] -> HSMap k v) -> [(k, v)] -> HSMap k v
forall a b. (a -> b) -> a -> b
$ [(k, v)]
x [(k, v)] -> [(k, v)] -> [(k, v)]
forall a. Semigroup a => a -> a -> a
<> [(k, v)]
xs'
mapHSMapKey :: (k -> l) -> Agda.HSMap k v -> Agda.HSMap l v
mapHSMapKey :: forall k l v. (k -> l) -> HSMap k v -> HSMap l v
mapHSMapKey k -> l
f (Agda.MkHSMap [(k, v)]
l) = [(l, v)] -> HSMap l v
forall k v. [(k, v)] -> HSMap k v
Agda.MkHSMap ([(l, v)] -> HSMap l v) -> [(l, v)] -> HSMap l v
forall a b. (a -> b) -> a -> b
$ (k -> l) -> (k, v) -> (l, v)
forall a b c. (a -> b) -> (a, c) -> (b, c)
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first k -> l
f ((k, v) -> (l, v)) -> [(k, v)] -> [(l, v)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(k, v)]
l
instance
( EraPParams era
, SpecTranslate ctx (PParamsHKD StrictMaybe era)
, SpecRep (PParamsHKD StrictMaybe era) ~ Agda.PParamsUpdate
) =>
SpecTranslate ctx (GovActionState era)
where
type SpecRep (GovActionState era) = Agda.GovActionState
toSpecRep :: GovActionState era -> SpecTransM ctx (SpecRep (GovActionState era))
toSpecRep gas :: GovActionState era
gas@GovActionState {Map (KeyHash 'StakePool) Vote
Map (Credential 'DRepRole) Vote
Map (Credential 'HotCommitteeRole) Vote
ProposalProcedure era
GovActionId
EpochNo
gasId :: GovActionId
gasCommitteeVotes :: Map (Credential 'HotCommitteeRole) Vote
gasDRepVotes :: Map (Credential 'DRepRole) Vote
gasStakePoolVotes :: Map (KeyHash 'StakePool) Vote
gasProposalProcedure :: ProposalProcedure era
gasProposedIn :: EpochNo
gasExpiresAfter :: EpochNo
gasId :: forall era. GovActionState era -> GovActionId
gasCommitteeVotes :: forall era.
GovActionState era -> Map (Credential 'HotCommitteeRole) Vote
gasDRepVotes :: forall era. GovActionState era -> Map (Credential 'DRepRole) Vote
gasStakePoolVotes :: forall era. GovActionState era -> Map (KeyHash 'StakePool) Vote
gasProposalProcedure :: forall era. GovActionState era -> ProposalProcedure era
gasProposedIn :: forall era. GovActionState era -> EpochNo
gasExpiresAfter :: forall era. GovActionState era -> EpochNo
..} = do
HSMap (GovRole, Credential) Vote
-> RwdAddr
-> Integer
-> GovAction
-> (Integer, Integer)
-> GovActionState
Agda.MkGovActionState
(HSMap (GovRole, Credential) Vote
-> RwdAddr
-> Integer
-> GovAction
-> (Integer, Integer)
-> GovActionState)
-> SpecTransM ctx (HSMap (GovRole, Credential) Vote)
-> SpecTransM
ctx
(RwdAddr
-> Integer -> GovAction -> (Integer, Integer) -> GovActionState)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SpecTransM ctx (HSMap (GovRole, Credential) Vote)
agdaVoteMap
SpecTransM
ctx
(RwdAddr
-> Integer -> GovAction -> (Integer, Integer) -> GovActionState)
-> SpecTransM ctx RwdAddr
-> SpecTransM
ctx (Integer -> GovAction -> (Integer, Integer) -> GovActionState)
forall a b.
SpecTransM ctx (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> RewardAccount -> SpecTransM ctx (SpecRep RewardAccount)
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep (GovActionState era -> RewardAccount
forall era. GovActionState era -> RewardAccount
gasReturnAddr GovActionState era
gas)
SpecTransM
ctx (Integer -> GovAction -> (Integer, Integer) -> GovActionState)
-> SpecTransM ctx Integer
-> SpecTransM
ctx (GovAction -> (Integer, Integer) -> GovActionState)
forall a b.
SpecTransM ctx (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> EpochNo -> SpecTransM ctx (SpecRep EpochNo)
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep EpochNo
gasExpiresAfter
SpecTransM ctx (GovAction -> (Integer, Integer) -> GovActionState)
-> SpecTransM ctx GovAction
-> SpecTransM ctx ((Integer, Integer) -> GovActionState)
forall a b.
SpecTransM ctx (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> GovAction era -> SpecTransM ctx (SpecRep (GovAction era))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep GovAction era
action
SpecTransM ctx ((Integer, Integer) -> GovActionState)
-> SpecTransM ctx (Integer, Integer)
-> SpecTransM ctx GovActionState
forall a b.
SpecTransM ctx (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> GovActionId -> SpecTransM ctx (SpecRep GovActionId)
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep (StrictMaybe GovActionId -> GovAction era -> GovActionId
forall era. StrictMaybe GovActionId -> GovAction era -> GovActionId
nullifyIfNotNeeded (GovAction era -> StrictMaybe GovActionId
forall era. GovAction era -> StrictMaybe GovActionId
prevGovActionId GovAction era
action) GovAction era
action)
where
action :: GovAction era
action = GovActionState era -> GovAction era
forall era. GovActionState era -> GovAction era
gasAction GovActionState era
gas
agdaVoteMap :: SpecTransM ctx (Agda.HSMap (Agda.GovRole, Agda.Credential) Agda.Vote)
agdaVoteMap :: SpecTransM ctx (HSMap (GovRole, Credential) Vote)
agdaVoteMap = do
HSMap Credential Vote
drepVotes <- Map (Credential 'DRepRole) Vote
-> SpecTransM ctx (SpecRep (Map (Credential 'DRepRole) Vote))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep Map (Credential 'DRepRole) Vote
gasDRepVotes
HSMap Credential Vote
ccVotes <- Map (Credential 'HotCommitteeRole) Vote
-> SpecTransM
ctx (SpecRep (Map (Credential 'HotCommitteeRole) Vote))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep Map (Credential 'HotCommitteeRole) Vote
gasCommitteeVotes
HSMap Integer Vote
spoVotes <- Map (KeyHash 'StakePool) Vote
-> SpecTransM ctx (SpecRep (Map (KeyHash 'StakePool) Vote))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep Map (KeyHash 'StakePool) Vote
gasStakePoolVotes
HSMap (GovRole, Credential) Vote
-> SpecTransM ctx (HSMap (GovRole, Credential) Vote)
forall a. a -> SpecTransM ctx a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (HSMap (GovRole, Credential) Vote
-> SpecTransM ctx (HSMap (GovRole, Credential) Vote))
-> HSMap (GovRole, Credential) Vote
-> SpecTransM ctx (HSMap (GovRole, Credential) Vote)
forall a b. (a -> b) -> a -> b
$
[HSMap (GovRole, Credential) Vote]
-> HSMap (GovRole, Credential) Vote
forall k v. [HSMap k v] -> HSMap k v
unionsHSMaps
[ (Credential -> (GovRole, Credential))
-> HSMap Credential Vote -> HSMap (GovRole, Credential) Vote
forall k l v. (k -> l) -> HSMap k v -> HSMap l v
mapHSMapKey (GovRole
Agda.DRep,) HSMap Credential Vote
drepVotes
, (Credential -> (GovRole, Credential))
-> HSMap Credential Vote -> HSMap (GovRole, Credential) Vote
forall k l v. (k -> l) -> HSMap k v -> HSMap l v
mapHSMapKey (GovRole
Agda.CC,) HSMap Credential Vote
ccVotes
, (Integer -> (GovRole, Credential))
-> HSMap Integer Vote -> HSMap (GovRole, Credential) Vote
forall k l v. (k -> l) -> HSMap k v -> HSMap l v
mapHSMapKey (\Integer
h -> (GovRole
Agda.SPO, Integer -> Credential
Agda.KeyHashObj Integer
h)) HSMap Integer Vote
spoVotes
]
instance SpecTranslate ctx GovActionIx where
type SpecRep GovActionIx = Integer
toSpecRep :: GovActionIx -> SpecTransM ctx (SpecRep GovActionIx)
toSpecRep = Integer -> SpecTransM ctx Integer
forall a. a -> SpecTransM ctx a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Integer -> SpecTransM ctx Integer)
-> (GovActionIx -> Integer)
-> GovActionIx
-> SpecTransM ctx Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Word16 -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Word16 -> Integer)
-> (GovActionIx -> Word16) -> GovActionIx -> Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. GovActionIx -> Word16
unGovActionIx
instance SpecTranslate ctx GovActionId where
type SpecRep GovActionId = Agda.GovActionID
toSpecRep :: GovActionId -> SpecTransM ctx (SpecRep GovActionId)
toSpecRep (GovActionId TxId
txId GovActionIx
gaIx) = (TxId, GovActionIx) -> SpecTransM ctx (SpecRep (TxId, GovActionIx))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep (TxId
txId, GovActionIx
gaIx)
instance
( EraPParams era
, SpecTranslate ctx (PParamsHKD StrictMaybe era)
, SpecRep (PParamsHKD StrictMaybe era) ~ Agda.PParamsUpdate
) =>
SpecTranslate ctx (Proposals era)
where
type SpecRep (Proposals era) = Agda.GovState
toSpecRep :: Proposals era -> SpecTransM ctx (SpecRep (Proposals era))
toSpecRep = OMap GovActionId (GovActionState era)
-> SpecTransM ctx [((Integer, Integer), GovActionState)]
OMap GovActionId (GovActionState era)
-> SpecTransM ctx (SpecRep (OMap GovActionId (GovActionState era)))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep (OMap GovActionId (GovActionState era)
-> SpecTransM ctx [((Integer, Integer), GovActionState)])
-> (Proposals era -> OMap GovActionId (GovActionState era))
-> Proposals era
-> SpecTransM ctx [((Integer, Integer), GovActionState)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. OMap GovActionId (GovActionState era)
-> OMap GovActionId (GovActionState era)
prioritySort (OMap GovActionId (GovActionState era)
-> OMap GovActionId (GovActionState era))
-> (Proposals era -> OMap GovActionId (GovActionState era))
-> Proposals era
-> OMap GovActionId (GovActionState era)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Getting
(OMap GovActionId (GovActionState era))
(Proposals era)
(OMap GovActionId (GovActionState era))
-> Proposals era -> OMap GovActionId (GovActionState era)
forall a s. Getting a s a -> s -> a
view Getting
(OMap GovActionId (GovActionState era))
(Proposals era)
(OMap GovActionId (GovActionState era))
forall era (f :: * -> *).
Functor f =>
(OMap GovActionId (GovActionState era)
-> f (OMap GovActionId (GovActionState era)))
-> Proposals era -> f (Proposals era)
pPropsL
where
prioritySort ::
OMap GovActionId (GovActionState era) ->
OMap GovActionId (GovActionState era)
prioritySort :: OMap GovActionId (GovActionState era)
-> OMap GovActionId (GovActionState era)
prioritySort = [Item (OMap GovActionId (GovActionState era))]
-> OMap GovActionId (GovActionState era)
[GovActionState era] -> OMap GovActionId (GovActionState era)
forall l. IsList l => [Item l] -> l
Exts.fromList ([GovActionState era] -> OMap GovActionId (GovActionState era))
-> (OMap GovActionId (GovActionState era) -> [GovActionState era])
-> OMap GovActionId (GovActionState era)
-> OMap GovActionId (GovActionState era)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (GovActionState era -> Int)
-> [GovActionState era] -> [GovActionState era]
forall b a. Ord b => (a -> b) -> [a] -> [a]
sortOn (GovAction era -> Int
forall era. GovAction era -> Int
actionPriority (GovAction era -> Int)
-> (GovActionState era -> GovAction era)
-> GovActionState era
-> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. GovActionState era -> GovAction era
forall era. GovActionState era -> GovAction era
gasAction) ([GovActionState era] -> [GovActionState era])
-> (OMap GovActionId (GovActionState era) -> [GovActionState era])
-> OMap GovActionId (GovActionState era)
-> [GovActionState era]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. OMap GovActionId (GovActionState era)
-> [Item (OMap GovActionId (GovActionState era))]
OMap GovActionId (GovActionState era) -> [GovActionState era]
forall l. IsList l => l -> [Item l]
Exts.toList
instance SpecTranslate ctx MaryValue where
type SpecRep MaryValue = Agda.Coin
toSpecRep :: MaryValue -> SpecTransM ctx (SpecRep MaryValue)
toSpecRep = Coin -> SpecTransM ctx Integer
Coin -> SpecTransM ctx (SpecRep Coin)
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep (Coin -> SpecTransM ctx Integer)
-> (MaryValue -> Coin) -> MaryValue -> SpecTransM ctx Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MaryValue -> Coin
forall t. Val t => t -> Coin
coin
instance
( ToExpr (PredicateFailure (EraRule "DELEG" era))
, ToExpr (PredicateFailure (EraRule "GOVCERT" era))
, ToExpr (PredicateFailure (EraRule "POOL" era))
) =>
SpecTranslate ctx (ConwayCertPredFailure era)
where
type SpecRep (ConwayCertPredFailure era) = OpaqueErrorString
toSpecRep :: ConwayCertPredFailure era
-> SpecTransM ctx (SpecRep (ConwayCertPredFailure era))
toSpecRep = OpaqueErrorString -> SpecTransM ctx OpaqueErrorString
forall a. a -> SpecTransM ctx a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (OpaqueErrorString -> SpecTransM ctx OpaqueErrorString)
-> (ConwayCertPredFailure era -> OpaqueErrorString)
-> ConwayCertPredFailure era
-> SpecTransM ctx OpaqueErrorString
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ConwayCertPredFailure era -> OpaqueErrorString
forall a. ToExpr a => a -> OpaqueErrorString
showOpaqueErrorString
instance (SpecTranslate ctx a, Compactible a) => SpecTranslate ctx (CompactForm a) where
type SpecRep (CompactForm a) = SpecRep a
toSpecRep :: CompactForm a -> SpecTransM ctx (SpecRep (CompactForm a))
toSpecRep = a -> SpecTransM ctx (SpecRep a)
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep (a -> SpecTransM ctx (SpecRep a))
-> (CompactForm a -> a)
-> CompactForm a
-> SpecTransM ctx (SpecRep a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CompactForm a -> a
forall a. Compactible a => CompactForm a -> a
fromCompact
instance SpecTranslate ctx CommitteeAuthorization where
type
SpecRep CommitteeAuthorization =
SpecRep (Maybe (Credential 'HotCommitteeRole))
toSpecRep :: CommitteeAuthorization
-> SpecTransM ctx (SpecRep CommitteeAuthorization)
toSpecRep (CommitteeHotCredential Credential 'HotCommitteeRole
c) = Maybe (Credential 'HotCommitteeRole)
-> SpecTransM ctx (SpecRep (Maybe (Credential 'HotCommitteeRole)))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep (Maybe (Credential 'HotCommitteeRole)
-> SpecTransM ctx (SpecRep (Maybe (Credential 'HotCommitteeRole))))
-> Maybe (Credential 'HotCommitteeRole)
-> SpecTransM ctx (SpecRep (Maybe (Credential 'HotCommitteeRole)))
forall a b. (a -> b) -> a -> b
$ Credential 'HotCommitteeRole
-> Maybe (Credential 'HotCommitteeRole)
forall a. a -> Maybe a
Just Credential 'HotCommitteeRole
c
toSpecRep (CommitteeMemberResigned StrictMaybe Anchor
_) =
Maybe (Credential 'HotCommitteeRole)
-> SpecTransM ctx (SpecRep (Maybe (Credential 'HotCommitteeRole)))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep (Maybe (Credential 'HotCommitteeRole)
-> SpecTransM ctx (SpecRep (Maybe (Credential 'HotCommitteeRole))))
-> Maybe (Credential 'HotCommitteeRole)
-> SpecTransM ctx (SpecRep (Maybe (Credential 'HotCommitteeRole)))
forall a b. (a -> b) -> a -> b
$
forall a. Maybe a
Nothing @(Credential 'HotCommitteeRole)
instance SpecTranslate ctx (CommitteeState era) where
type
SpecRep (CommitteeState era) =
SpecRep (Map (Credential 'ColdCommitteeRole) CommitteeAuthorization)
toSpecRep :: CommitteeState era -> SpecTransM ctx (SpecRep (CommitteeState era))
toSpecRep = Map (Credential 'ColdCommitteeRole) CommitteeAuthorization
-> SpecTransM ctx (HSMap Credential (Maybe Credential))
Map (Credential 'ColdCommitteeRole) CommitteeAuthorization
-> SpecTransM
ctx
(SpecRep
(Map (Credential 'ColdCommitteeRole) CommitteeAuthorization))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep (Map (Credential 'ColdCommitteeRole) CommitteeAuthorization
-> SpecTransM ctx (HSMap Credential (Maybe Credential)))
-> (CommitteeState era
-> Map (Credential 'ColdCommitteeRole) CommitteeAuthorization)
-> CommitteeState era
-> SpecTransM ctx (HSMap Credential (Maybe Credential))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CommitteeState era
-> Map (Credential 'ColdCommitteeRole) CommitteeAuthorization
forall era.
CommitteeState era
-> Map (Credential 'ColdCommitteeRole) CommitteeAuthorization
csCommitteeCreds
instance SpecTranslate ctx IndividualPoolStake where
type SpecRep IndividualPoolStake = SpecRep Coin
toSpecRep :: IndividualPoolStake -> SpecTransM ctx (SpecRep IndividualPoolStake)
toSpecRep (IndividualPoolStake Rational
_ CompactForm Coin
c VRFVerKeyHash 'StakePoolVRF
_) = CompactForm Coin -> SpecTransM ctx (SpecRep (CompactForm Coin))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep CompactForm Coin
c
instance SpecTranslate ctx PoolDistr where
type SpecRep PoolDistr = Agda.HSMap Agda.VDeleg Agda.Coin
toSpecRep :: PoolDistr -> SpecTransM ctx (SpecRep PoolDistr)
toSpecRep (PoolDistr Map (KeyHash 'StakePool) IndividualPoolStake
ps CompactForm Coin
_) = do
Agda.MkHSMap [(Integer, Integer)]
l <- Map (KeyHash 'StakePool) IndividualPoolStake
-> SpecTransM
ctx (SpecRep (Map (KeyHash 'StakePool) IndividualPoolStake))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep Map (KeyHash 'StakePool) IndividualPoolStake
ps
HSMap VDeleg Integer -> SpecTransM ctx (HSMap VDeleg Integer)
forall a. a -> SpecTransM ctx a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (HSMap VDeleg Integer -> SpecTransM ctx (HSMap VDeleg Integer))
-> ([(VDeleg, Integer)] -> HSMap VDeleg Integer)
-> [(VDeleg, Integer)]
-> SpecTransM ctx (HSMap VDeleg Integer)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(VDeleg, Integer)] -> HSMap VDeleg Integer
forall k v. [(k, v)] -> HSMap k v
Agda.MkHSMap ([(VDeleg, Integer)] -> SpecTransM ctx (HSMap VDeleg Integer))
-> [(VDeleg, Integer)] -> SpecTransM ctx (HSMap VDeleg Integer)
forall a b. (a -> b) -> a -> b
$ (Integer -> VDeleg) -> (Integer, Integer) -> (VDeleg, Integer)
forall a b c. (a -> b) -> (a, c) -> (b, c)
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first (GovRole -> Credential -> VDeleg
Agda.CredVoter GovRole
Agda.SPO (Credential -> VDeleg)
-> (Integer -> Credential) -> Integer -> VDeleg
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> Credential
Agda.KeyHashObj) ((Integer, Integer) -> (VDeleg, Integer))
-> [(Integer, Integer)] -> [(VDeleg, Integer)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Integer, Integer)]
l
instance
Inject ctx Coin =>
SpecTranslate ctx (RatifyEnv era)
where
type SpecRep (RatifyEnv era) = Agda.RatifyEnv
toSpecRep :: RatifyEnv era -> SpecTransM ctx (SpecRep (RatifyEnv era))
toSpecRep RatifyEnv {Map (KeyHash 'StakePool) PoolParams
Map DRep (CompactForm Coin)
Map StakeCredential DRep
Map (Credential 'DRepRole) DRepState
PoolDistr
CommitteeState era
InstantStake era
EpochNo
reInstantStake :: InstantStake era
reStakePoolDistr :: PoolDistr
reDRepDistr :: Map DRep (CompactForm Coin)
reDRepState :: Map (Credential 'DRepRole) DRepState
reCurrentEpoch :: EpochNo
reCommitteeState :: CommitteeState era
reDelegatees :: Map StakeCredential DRep
rePoolParams :: Map (KeyHash 'StakePool) PoolParams
reInstantStake :: forall era. RatifyEnv era -> InstantStake era
reStakePoolDistr :: forall era. RatifyEnv era -> PoolDistr
reDRepDistr :: forall era. RatifyEnv era -> Map DRep (CompactForm Coin)
reDRepState :: forall era. RatifyEnv era -> Map (Credential 'DRepRole) DRepState
reCurrentEpoch :: forall era. RatifyEnv era -> EpochNo
reCommitteeState :: forall era. RatifyEnv era -> CommitteeState era
reDelegatees :: forall era. RatifyEnv era -> Map StakeCredential DRep
rePoolParams :: forall era. RatifyEnv era -> Map (KeyHash 'StakePool) PoolParams
..} = do
let
stakeDistrs :: SpecTransM ctx StakeDistrs
stakeDistrs = do
Agda.MkHSMap [(VDeleg, Integer)]
stakeDistrsMap <- PoolDistr -> SpecTransM ctx (SpecRep PoolDistr)
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep PoolDistr
reStakePoolDistr
[(VDeleg, Integer)]
drepDistrsMap <- [(DRep, CompactForm Coin)]
-> SpecTransM ctx (SpecRep [(DRep, CompactForm Coin)])
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep ([(DRep, CompactForm Coin)]
-> SpecTransM ctx (SpecRep [(DRep, CompactForm Coin)]))
-> [(DRep, CompactForm Coin)]
-> SpecTransM ctx (SpecRep [(DRep, CompactForm Coin)])
forall a b. (a -> b) -> a -> b
$ Map DRep (CompactForm Coin) -> [(DRep, CompactForm Coin)]
forall k a. Map k a -> [(k, a)]
Map.toList Map DRep (CompactForm Coin)
reDRepDistr
StakeDistrs -> SpecTransM ctx StakeDistrs
forall a. a -> SpecTransM ctx a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (StakeDistrs -> SpecTransM ctx StakeDistrs)
-> (HSMap VDeleg Integer -> StakeDistrs)
-> HSMap VDeleg Integer
-> SpecTransM ctx StakeDistrs
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HSMap VDeleg Integer -> StakeDistrs
Agda.StakeDistrs (HSMap VDeleg Integer -> SpecTransM ctx StakeDistrs)
-> HSMap VDeleg Integer -> SpecTransM ctx StakeDistrs
forall a b. (a -> b) -> a -> b
$ [(VDeleg, Integer)] -> HSMap VDeleg Integer
forall k v. [(k, v)] -> HSMap k v
Agda.MkHSMap ([(VDeleg, Integer)]
stakeDistrsMap [(VDeleg, Integer)] -> [(VDeleg, Integer)] -> [(VDeleg, Integer)]
forall a. Semigroup a => a -> a -> a
<> [(VDeleg, Integer)]
drepDistrsMap)
dreps :: SpecTransM ctx (SpecRep (Map (Credential 'DRepRole) EpochNo))
dreps = Map (Credential 'DRepRole) EpochNo
-> SpecTransM ctx (SpecRep (Map (Credential 'DRepRole) EpochNo))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep (Map (Credential 'DRepRole) EpochNo
-> SpecTransM ctx (SpecRep (Map (Credential 'DRepRole) EpochNo)))
-> Map (Credential 'DRepRole) EpochNo
-> SpecTransM ctx (SpecRep (Map (Credential 'DRepRole) EpochNo))
forall a b. (a -> b) -> a -> b
$ (DRepState -> EpochNo)
-> Map (Credential 'DRepRole) DRepState
-> Map (Credential 'DRepRole) EpochNo
forall a b k. (a -> b) -> Map k a -> Map k b
Map.map DRepState -> EpochNo
drepExpiry Map (Credential 'DRepRole) DRepState
reDRepState
Coin
treasury <- forall b ctx. Inject ctx b => SpecTransM ctx b
askCtx @Coin
StakeDistrs
-> Integer
-> HSMap Credential Integer
-> HSMap Credential (Maybe Credential)
-> Integer
-> HSMap Integer PoolParams
-> HSMap Credential VDeleg
-> RatifyEnv
Agda.MkRatifyEnv
(StakeDistrs
-> Integer
-> HSMap Credential Integer
-> HSMap Credential (Maybe Credential)
-> Integer
-> HSMap Integer PoolParams
-> HSMap Credential VDeleg
-> RatifyEnv)
-> SpecTransM ctx StakeDistrs
-> SpecTransM
ctx
(Integer
-> HSMap Credential Integer
-> HSMap Credential (Maybe Credential)
-> Integer
-> HSMap Integer PoolParams
-> HSMap Credential VDeleg
-> RatifyEnv)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SpecTransM ctx StakeDistrs
stakeDistrs
SpecTransM
ctx
(Integer
-> HSMap Credential Integer
-> HSMap Credential (Maybe Credential)
-> Integer
-> HSMap Integer PoolParams
-> HSMap Credential VDeleg
-> RatifyEnv)
-> SpecTransM ctx Integer
-> SpecTransM
ctx
(HSMap Credential Integer
-> HSMap Credential (Maybe Credential)
-> Integer
-> HSMap Integer PoolParams
-> HSMap Credential VDeleg
-> RatifyEnv)
forall a b.
SpecTransM ctx (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> EpochNo -> SpecTransM ctx (SpecRep EpochNo)
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep EpochNo
reCurrentEpoch
SpecTransM
ctx
(HSMap Credential Integer
-> HSMap Credential (Maybe Credential)
-> Integer
-> HSMap Integer PoolParams
-> HSMap Credential VDeleg
-> RatifyEnv)
-> SpecTransM ctx (HSMap Credential Integer)
-> SpecTransM
ctx
(HSMap Credential (Maybe Credential)
-> Integer
-> HSMap Integer PoolParams
-> HSMap Credential VDeleg
-> RatifyEnv)
forall a b.
SpecTransM ctx (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> SpecTransM ctx (HSMap Credential Integer)
SpecTransM ctx (SpecRep (Map (Credential 'DRepRole) EpochNo))
dreps
SpecTransM
ctx
(HSMap Credential (Maybe Credential)
-> Integer
-> HSMap Integer PoolParams
-> HSMap Credential VDeleg
-> RatifyEnv)
-> SpecTransM ctx (HSMap Credential (Maybe Credential))
-> SpecTransM
ctx
(Integer
-> HSMap Integer PoolParams
-> HSMap Credential VDeleg
-> RatifyEnv)
forall a b.
SpecTransM ctx (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> CommitteeState era -> SpecTransM ctx (SpecRep (CommitteeState era))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep CommitteeState era
reCommitteeState
SpecTransM
ctx
(Integer
-> HSMap Integer PoolParams
-> HSMap Credential VDeleg
-> RatifyEnv)
-> SpecTransM ctx Integer
-> SpecTransM
ctx
(HSMap Integer PoolParams -> HSMap Credential VDeleg -> RatifyEnv)
forall a b.
SpecTransM ctx (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Coin -> SpecTransM ctx (SpecRep Coin)
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep Coin
treasury
SpecTransM
ctx
(HSMap Integer PoolParams -> HSMap Credential VDeleg -> RatifyEnv)
-> SpecTransM ctx (HSMap Integer PoolParams)
-> SpecTransM ctx (HSMap Credential VDeleg -> RatifyEnv)
forall a b.
SpecTransM ctx (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Map (KeyHash 'StakePool) PoolParams
-> SpecTransM ctx (SpecRep (Map (KeyHash 'StakePool) PoolParams))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep Map (KeyHash 'StakePool) PoolParams
rePoolParams
SpecTransM ctx (HSMap Credential VDeleg -> RatifyEnv)
-> SpecTransM ctx (HSMap Credential VDeleg)
-> SpecTransM ctx RatifyEnv
forall a b.
SpecTransM ctx (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Map StakeCredential DRep
-> SpecTransM ctx (SpecRep (Map StakeCredential DRep))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep Map StakeCredential DRep
reDelegatees
instance SpecTranslate ctx Bool where
type SpecRep Bool = Bool
toSpecRep :: Bool -> SpecTransM ctx (SpecRep Bool)
toSpecRep = Bool -> SpecTransM ctx Bool
Bool -> SpecTransM ctx (SpecRep Bool)
forall a. a -> SpecTransM ctx a
forall (f :: * -> *) a. Applicative f => a -> f a
pure
instance
( EraPParams era
, SpecRep (PParamsHKD Identity era) ~ Agda.PParams
, SpecTranslate ctx (PParamsHKD Identity era)
, Inject ctx [GovActionState era]
, ToExpr (PParamsHKD StrictMaybe era)
, SpecRep (PParamsHKD StrictMaybe era) ~ Agda.PParamsUpdate
, SpecTranslate ctx (PParamsHKD StrictMaybe era)
) =>
SpecTranslate ctx (RatifyState era)
where
type SpecRep (RatifyState era) = Agda.RatifyState
toSpecRep :: RatifyState era -> SpecTransM ctx (SpecRep (RatifyState era))
toSpecRep RatifyState {Bool
Set GovActionId
EnactState era
Seq (GovActionState era)
rsEnactState :: EnactState era
rsEnacted :: Seq (GovActionState era)
rsExpired :: Set GovActionId
rsDelayed :: Bool
rsEnactState :: forall era. RatifyState era -> EnactState era
rsEnacted :: forall era. RatifyState era -> Seq (GovActionState era)
rsExpired :: forall era. RatifyState era -> Set GovActionId
rsDelayed :: forall era. RatifyState era -> Bool
..} = do
Map GovActionId (GovActionState era)
govActionMap <-
(Map GovActionId (GovActionState era)
-> GovActionState era -> Map GovActionId (GovActionState era))
-> Map GovActionId (GovActionState era)
-> [GovActionState era]
-> Map GovActionId (GovActionState era)
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' (\Map GovActionId (GovActionState era)
acc GovActionState era
gas -> GovActionId
-> GovActionState era
-> Map GovActionId (GovActionState era)
-> Map GovActionId (GovActionState era)
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert (GovActionState era -> GovActionId
forall era. GovActionState era -> GovActionId
gasId GovActionState era
gas) GovActionState era
gas Map GovActionId (GovActionState era)
acc) Map GovActionId (GovActionState era)
forall a. Monoid a => a
mempty
([GovActionState era] -> Map GovActionId (GovActionState era))
-> SpecTransM ctx [GovActionState era]
-> SpecTransM ctx (Map GovActionId (GovActionState era))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall b ctx. Inject ctx b => SpecTransM ctx b
askCtx @[GovActionState era]
let
lookupGAS :: GovActionId
-> SpecTransM ctx (Set (GovActionId, GovActionState era))
-> SpecTransM ctx (Set (GovActionId, GovActionState era))
lookupGAS GovActionId
gaId SpecTransM ctx (Set (GovActionId, GovActionState era))
m = do
case GovActionId
-> Map GovActionId (GovActionState era)
-> Maybe (GovActionState era)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup GovActionId
gaId Map GovActionId (GovActionState era)
govActionMap of
Just GovActionState era
x -> (GovActionId, GovActionState era)
-> Set (GovActionId, GovActionState era)
-> Set (GovActionId, GovActionState era)
forall a. Ord a => a -> Set a -> Set a
Set.insert (GovActionId
gaId, GovActionState era
x) (Set (GovActionId, GovActionState era)
-> Set (GovActionId, GovActionState era))
-> SpecTransM ctx (Set (GovActionId, GovActionState era))
-> SpecTransM ctx (Set (GovActionId, GovActionState era))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SpecTransM ctx (Set (GovActionId, GovActionState era))
m
Maybe (GovActionState era)
Nothing ->
Text -> SpecTransM ctx (Set (GovActionId, GovActionState era))
forall a. Text -> SpecTransM ctx a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (Text -> SpecTransM ctx (Set (GovActionId, GovActionState era)))
-> Text -> SpecTransM ctx (Set (GovActionId, GovActionState era))
forall a b. (a -> b) -> a -> b
$
Text
"gaId: "
Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> [Char] -> Text
T.pack (GovActionId -> [Char]
forall a. ToExpr a => a -> [Char]
showExpr GovActionId
gaId)
Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
"\n\ngovActionMap: "
Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> [Char] -> Text
T.pack (Map GovActionId (GovActionState era) -> [Char]
forall a. ToExpr a => a -> [Char]
showExpr Map GovActionId (GovActionState era)
govActionMap)
Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
"\n\nGovActionId is not contained in the govActionMap"
Set (GovActionId, GovActionState era)
removed <-
(GovActionId
-> SpecTransM ctx (Set (GovActionId, GovActionState era))
-> SpecTransM ctx (Set (GovActionId, GovActionState era)))
-> SpecTransM ctx (Set (GovActionId, GovActionState era))
-> Set GovActionId
-> SpecTransM ctx (Set (GovActionId, GovActionState era))
forall a b. (a -> b -> b) -> b -> Set a -> b
Set.foldr'
GovActionId
-> SpecTransM ctx (Set (GovActionId, GovActionState era))
-> SpecTransM ctx (Set (GovActionId, GovActionState era))
lookupGAS
(Set (GovActionId, GovActionState era)
-> SpecTransM ctx (Set (GovActionId, GovActionState era))
forall a. a -> SpecTransM ctx a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Set (GovActionId, GovActionState era)
forall a. Set a
Set.empty)
(Set GovActionId
rsExpired Set GovActionId -> Set GovActionId -> Set GovActionId
forall a. Ord a => Set a -> Set a -> Set a
`Set.union` [GovActionId] -> Set GovActionId
forall a. Ord a => [a] -> Set a
Set.fromList (GovActionState era -> GovActionId
forall era. GovActionState era -> GovActionId
gasId (GovActionState era -> GovActionId)
-> [GovActionState era] -> [GovActionId]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Seq (GovActionState era) -> [GovActionState era]
forall a. Seq a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList Seq (GovActionState era)
rsEnacted))
EnactState
-> HSSet ((Integer, Integer), GovActionState)
-> Bool
-> RatifyState
Agda.MkRatifyState
(EnactState
-> HSSet ((Integer, Integer), GovActionState)
-> Bool
-> RatifyState)
-> SpecTransM ctx EnactState
-> SpecTransM
ctx
(HSSet ((Integer, Integer), GovActionState) -> Bool -> RatifyState)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> EnactState era -> SpecTransM ctx (SpecRep (EnactState era))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep EnactState era
rsEnactState
SpecTransM
ctx
(HSSet ((Integer, Integer), GovActionState) -> Bool -> RatifyState)
-> SpecTransM ctx (HSSet ((Integer, Integer), GovActionState))
-> SpecTransM ctx (Bool -> RatifyState)
forall a b.
SpecTransM ctx (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Set (GovActionId, GovActionState era)
-> SpecTransM ctx (SpecRep (Set (GovActionId, GovActionState era)))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep Set (GovActionId, GovActionState era)
removed
SpecTransM ctx (Bool -> RatifyState)
-> SpecTransM ctx Bool -> SpecTransM ctx RatifyState
forall a b.
SpecTransM ctx (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Bool -> SpecTransM ctx (SpecRep Bool)
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep Bool
rsDelayed
instance
( EraPParams era
, SpecTranslate ctx (PParamsHKD StrictMaybe era)
, SpecRep (PParamsHKD StrictMaybe era) ~ Agda.PParamsUpdate
) =>
SpecTranslate ctx (RatifySignal era)
where
type
SpecRep (RatifySignal era) =
SpecRep [(GovActionId, GovActionState era)]
toSpecRep :: RatifySignal era -> SpecTransM ctx (SpecRep (RatifySignal era))
toSpecRep (RatifySignal StrictSeq (GovActionState era)
x) =
StrictSeq (GovActionId, GovActionState era)
-> SpecTransM
ctx (SpecRep (StrictSeq (GovActionId, GovActionState era)))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep (StrictSeq (GovActionId, GovActionState era)
-> SpecTransM
ctx (SpecRep (StrictSeq (GovActionId, GovActionState era))))
-> StrictSeq (GovActionId, GovActionState era)
-> SpecTransM
ctx (SpecRep (StrictSeq (GovActionId, GovActionState era)))
forall a b. (a -> b) -> a -> b
$
(\gas :: GovActionState era
gas@GovActionState {GovActionId
gasId :: forall era. GovActionState era -> GovActionId
gasId :: GovActionId
gasId} -> (GovActionId
gasId, GovActionState era
gas)) (GovActionState era -> (GovActionId, GovActionState era))
-> StrictSeq (GovActionState era)
-> StrictSeq (GovActionId, GovActionState era)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StrictSeq (GovActionState era)
x
instance
( EraPParams era
, SpecTranslate ctx (PParamsHKD StrictMaybe era)
, SpecRep (PParamsHKD StrictMaybe era) ~ Agda.PParamsUpdate
) =>
SpecTranslate ctx (EnactSignal era)
where
type SpecRep (EnactSignal era) = SpecRep (GovAction era)
toSpecRep :: EnactSignal era -> SpecTransM ctx (SpecRep (EnactSignal era))
toSpecRep (EnactSignal GovActionId
_ GovAction era
ga) = GovAction era -> SpecTransM ctx (SpecRep (GovAction era))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep GovAction era
ga
instance ToExpr (EpochExecEnv era)
instance Era era => NFData (EpochExecEnv era)
instance HasSimpleRep (EpochExecEnv era)
instance Era era => HasSpec (EpochExecEnv era)
instance SpecTranslate ctx (EpochExecEnv era) where
type SpecRep (EpochExecEnv era) = ()
toSpecRep :: EpochExecEnv era -> SpecTransM ctx (SpecRep (EpochExecEnv era))
toSpecRep EpochExecEnv era
_ = () -> SpecTransM ctx ()
forall a. a -> SpecTransM ctx a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
data ConwayExecEnactEnv era = ConwayExecEnactEnv
{ forall era. ConwayExecEnactEnv era -> GovActionId
ceeeGid :: GovActionId
, forall era. ConwayExecEnactEnv era -> Coin
ceeeTreasury :: Coin
, forall era. ConwayExecEnactEnv era -> EpochNo
ceeeEpoch :: EpochNo
}
deriving ((forall x.
ConwayExecEnactEnv era -> Rep (ConwayExecEnactEnv era) x)
-> (forall x.
Rep (ConwayExecEnactEnv era) x -> ConwayExecEnactEnv era)
-> Generic (ConwayExecEnactEnv era)
forall x. Rep (ConwayExecEnactEnv era) x -> ConwayExecEnactEnv era
forall x. ConwayExecEnactEnv era -> Rep (ConwayExecEnactEnv era) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall era x.
Rep (ConwayExecEnactEnv era) x -> ConwayExecEnactEnv era
forall era x.
ConwayExecEnactEnv era -> Rep (ConwayExecEnactEnv era) x
$cfrom :: forall era x.
ConwayExecEnactEnv era -> Rep (ConwayExecEnactEnv era) x
from :: forall x. ConwayExecEnactEnv era -> Rep (ConwayExecEnactEnv era) x
$cto :: forall era x.
Rep (ConwayExecEnactEnv era) x -> ConwayExecEnactEnv era
to :: forall x. Rep (ConwayExecEnactEnv era) x -> ConwayExecEnactEnv era
Generic, ConwayExecEnactEnv era -> ConwayExecEnactEnv era -> Bool
(ConwayExecEnactEnv era -> ConwayExecEnactEnv era -> Bool)
-> (ConwayExecEnactEnv era -> ConwayExecEnactEnv era -> Bool)
-> Eq (ConwayExecEnactEnv era)
forall era.
ConwayExecEnactEnv era -> ConwayExecEnactEnv era -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall era.
ConwayExecEnactEnv era -> ConwayExecEnactEnv era -> Bool
== :: ConwayExecEnactEnv era -> ConwayExecEnactEnv era -> Bool
$c/= :: forall era.
ConwayExecEnactEnv era -> ConwayExecEnactEnv era -> Bool
/= :: ConwayExecEnactEnv era -> ConwayExecEnactEnv era -> Bool
Eq, Int -> ConwayExecEnactEnv era -> ShowS
[ConwayExecEnactEnv era] -> ShowS
ConwayExecEnactEnv era -> [Char]
(Int -> ConwayExecEnactEnv era -> ShowS)
-> (ConwayExecEnactEnv era -> [Char])
-> ([ConwayExecEnactEnv era] -> ShowS)
-> Show (ConwayExecEnactEnv era)
forall era. Int -> ConwayExecEnactEnv era -> ShowS
forall era. [ConwayExecEnactEnv era] -> ShowS
forall era. ConwayExecEnactEnv era -> [Char]
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall era. Int -> ConwayExecEnactEnv era -> ShowS
showsPrec :: Int -> ConwayExecEnactEnv era -> ShowS
$cshow :: forall era. ConwayExecEnactEnv era -> [Char]
show :: ConwayExecEnactEnv era -> [Char]
$cshowList :: forall era. [ConwayExecEnactEnv era] -> ShowS
showList :: [ConwayExecEnactEnv era] -> ShowS
Show)
instance Inject (ConwayExecEnactEnv era) () where
inject :: ConwayExecEnactEnv era -> ()
inject ConwayExecEnactEnv era
_ = ()
instance ToExpr (ConwayExecEnactEnv era)
instance Era era => NFData (ConwayExecEnactEnv era)
instance HasSimpleRep (ConwayExecEnactEnv era)
instance Era era => HasSpec (ConwayExecEnactEnv era)
instance SpecTranslate ctx (ConwayExecEnactEnv era) where
type SpecRep (ConwayExecEnactEnv era) = Agda.EnactEnv
toSpecRep :: ConwayExecEnactEnv era
-> SpecTransM ctx (SpecRep (ConwayExecEnactEnv era))
toSpecRep ConwayExecEnactEnv {GovActionId
Coin
EpochNo
ceeeGid :: forall era. ConwayExecEnactEnv era -> GovActionId
ceeeTreasury :: forall era. ConwayExecEnactEnv era -> Coin
ceeeEpoch :: forall era. ConwayExecEnactEnv era -> EpochNo
ceeeGid :: GovActionId
ceeeTreasury :: Coin
ceeeEpoch :: EpochNo
..} =
(Integer, Integer) -> Integer -> Integer -> EnactEnv
Agda.MkEnactEnv
((Integer, Integer) -> Integer -> Integer -> EnactEnv)
-> SpecTransM ctx (Integer, Integer)
-> SpecTransM ctx (Integer -> Integer -> EnactEnv)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> GovActionId -> SpecTransM ctx (SpecRep GovActionId)
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep GovActionId
ceeeGid
SpecTransM ctx (Integer -> Integer -> EnactEnv)
-> SpecTransM ctx Integer -> SpecTransM ctx (Integer -> EnactEnv)
forall a b.
SpecTransM ctx (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Coin -> SpecTransM ctx (SpecRep Coin)
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep Coin
ceeeTreasury
SpecTransM ctx (Integer -> EnactEnv)
-> SpecTransM ctx Integer -> SpecTransM ctx EnactEnv
forall a b.
SpecTransM ctx (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> EpochNo -> SpecTransM ctx (SpecRep EpochNo)
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep EpochNo
ceeeEpoch
committeeCredentialToStrictMaybe ::
CommitteeAuthorization ->
StrictMaybe (Credential 'HotCommitteeRole)
committeeCredentialToStrictMaybe :: CommitteeAuthorization
-> StrictMaybe (Credential 'HotCommitteeRole)
committeeCredentialToStrictMaybe (CommitteeHotCredential Credential 'HotCommitteeRole
c) = Credential 'HotCommitteeRole
-> StrictMaybe (Credential 'HotCommitteeRole)
forall a. a -> StrictMaybe a
SJust Credential 'HotCommitteeRole
c
committeeCredentialToStrictMaybe (CommitteeMemberResigned StrictMaybe Anchor
_) = StrictMaybe (Credential 'HotCommitteeRole)
forall a. StrictMaybe a
SNothing
instance SpecTranslate ctx DepositPurpose where
type SpecRep DepositPurpose = Agda.DepositPurpose
toSpecRep :: DepositPurpose -> SpecTransM ctx (SpecRep DepositPurpose)
toSpecRep (CredentialDeposit StakeCredential
cred) =
Credential -> DepositPurpose
Agda.CredentialDeposit (Credential -> DepositPurpose)
-> SpecTransM ctx Credential -> SpecTransM ctx DepositPurpose
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StakeCredential -> SpecTransM ctx (SpecRep StakeCredential)
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep StakeCredential
cred
toSpecRep (PoolDeposit KeyHash 'StakePool
kh) =
Integer -> DepositPurpose
Agda.PoolDeposit (Integer -> DepositPurpose)
-> SpecTransM ctx Integer -> SpecTransM ctx DepositPurpose
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> KeyHash 'StakePool -> SpecTransM ctx (SpecRep (KeyHash 'StakePool))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep KeyHash 'StakePool
kh
toSpecRep (DRepDeposit Credential 'DRepRole
cred) =
Credential -> DepositPurpose
Agda.DRepDeposit (Credential -> DepositPurpose)
-> SpecTransM ctx Credential -> SpecTransM ctx DepositPurpose
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Credential 'DRepRole
-> SpecTransM ctx (SpecRep (Credential 'DRepRole))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep Credential 'DRepRole
cred
toSpecRep (GovActionDeposit GovActionId
gid) =
(Integer, Integer) -> DepositPurpose
Agda.GovActionDeposit ((Integer, Integer) -> DepositPurpose)
-> SpecTransM ctx (Integer, Integer)
-> SpecTransM ctx DepositPurpose
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> GovActionId -> SpecTransM ctx (SpecRep GovActionId)
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep GovActionId
gid