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

module Test.Cardano.Ledger.Conformance.SpecTranslate.Core (
  committeeCredentialToStrictMaybe,
  vkeyToInteger,
  vkeyFromInteger,
  signatureToInteger,
  signatureFromInteger,
) where

import Cardano.Crypto.DSIGN (DSIGNAlgorithm (..), SignedDSIGN (..))
import Cardano.Crypto.Util (bytesToNatural, naturalToBytes)
import Cardano.Ledger.Address (
  AccountAddress (..),
  AccountId (..),
  Addr (..),
  BootstrapAddress (..),
 )
import Cardano.Ledger.BaseTypes (
  BlocksMade (..),
  EpochInterval (..),
  EpochNo (..),
  Network (..),
  ProtVer (..),
  SlotNo (..),
  TxIx (..),
  getVersion,
 )
import Cardano.Ledger.Coin (Coin (..))
import Cardano.Ledger.Conway.Core (
  ADDRHASH,
  Hash,
  KeyHash (..),
  KeyRole (..),
  PParams (..),
  PParamsHKD,
  PParamsUpdate (..),
  ScriptHash (..),
 )
import Cardano.Ledger.Conway.State
import Cardano.Ledger.Credential (Credential (..), StakeReference (..))
import Cardano.Ledger.Keys (VKey (..))
import Cardano.Ledger.Keys.WitVKey (WitVKey (..))
import Cardano.Ledger.Plutus.ExUnits (Prices)
import Control.Monad (forM)
import Control.Monad.Except (throwError)
import Data.Functor.Identity (Identity (..))
import qualified Data.Map as Map
import Data.Maybe.Strict (StrictMaybe (..))
import GHC.Natural (naturalToInteger)
import qualified MAlonzo.Code.Ledger.Core.Foreign.API as Agda
import Test.Cardano.Ledger.Conformance.SpecTranslate.Base
import Test.Cardano.Ledger.Conformance.Utils

instance SpecTranslate era TxIx where
  type SpecRep era TxIx = Integer

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

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

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

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

  toSpecRep :: BootstrapAddress
-> SpecTransM
     era
     (SpecContext era BootstrapAddress)
     (SpecRep era BootstrapAddress)
toSpecRep BootstrapAddress
_ = Text -> SpecTransM era () BootstrapAddr
forall a. Text -> SpecTransM era () a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError Text
"Cannot translate bootstrap addresses"

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

  toSpecRep :: Addr -> SpecTransM era (SpecContext era Addr) (SpecRep era Addr)
toSpecRep (Addr Network
nw Credential Payment
pc StakeReference
sr) =
    BaseAddr -> Either BaseAddr BootstrapAddr
forall a b. a -> Either a b
Left
      (BaseAddr -> Either BaseAddr BootstrapAddr)
-> SpecTransM era () BaseAddr
-> SpecTransM era () (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 era () Integer
-> SpecTransM era () (Credential -> Maybe Credential -> BaseAddr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Network
-> SpecTransM era (SpecContext era Network) (SpecRep era Network)
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep Network
nw SpecTransM era () (Credential -> Maybe Credential -> BaseAddr)
-> SpecTransM era () Credential
-> SpecTransM era () (Maybe Credential -> BaseAddr)
forall a b.
SpecTransM era () (a -> b)
-> SpecTransM era () a -> SpecTransM era () b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Credential Payment
-> SpecTransM
     era
     (SpecContext era (Credential Payment))
     (SpecRep era (Credential Payment))
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep Credential Payment
pc SpecTransM era () (Maybe Credential -> BaseAddr)
-> SpecTransM era () (Maybe Credential)
-> SpecTransM era () BaseAddr
forall a b.
SpecTransM era () (a -> b)
-> SpecTransM era () a -> SpecTransM era () b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> StakeReference
-> SpecTransM
     era (SpecContext era StakeReference) (SpecRep era StakeReference)
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era 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 era () BootstrapAddr
-> SpecTransM era () (Either BaseAddr BootstrapAddr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> BootstrapAddress
-> SpecTransM
     era
     (SpecContext era BootstrapAddress)
     (SpecRep era BootstrapAddress)
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep BootstrapAddress
ba

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

  toSpecRep :: Hash a b
-> SpecTransM
     era (SpecContext era (Hash a b)) (SpecRep era (Hash a b))
toSpecRep = Integer -> SpecTransM era () Integer
forall a. a -> SpecTransM era () a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Integer -> SpecTransM era () Integer)
-> (Hash a b -> Integer) -> Hash a b -> SpecTransM era () 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 era ScriptHash where
  type SpecRep era ScriptHash = Integer

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

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

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

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

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

instance SpecTranslate era Network where
  type SpecRep era Network = Integer

  toSpecRep :: Network
-> SpecTransM era (SpecContext era Network) (SpecRep era Network)
toSpecRep = Integer -> SpecTransM era () Integer
forall a. a -> SpecTransM era () a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Integer -> SpecTransM era () Integer)
-> (Network -> Integer) -> Network -> SpecTransM era () 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

deriving instance SpecTranslate era Coin

deriving instance SpecTranslate era SlotNo

deriving instance SpecTranslate era EpochNo

deriving instance SpecTranslate era EpochInterval

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

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

instance SpecTranslate era Prices where
  type SpecRep era Prices = ()

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

instance SpecTranslate era AccountAddress where
  type SpecRep era AccountAddress = Agda.RewardAddress

  toSpecRep :: AccountAddress
-> SpecTransM
     era (SpecContext era AccountAddress) (SpecRep era AccountAddress)
toSpecRep (AccountAddress Network
n (AccountId Credential Staking
c)) = Integer -> Credential -> RewardAddress
Agda.RewardAddress (Integer -> Credential -> RewardAddress)
-> SpecTransM era () Integer
-> SpecTransM era () (Credential -> RewardAddress)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Network
-> SpecTransM era (SpecContext era Network) (SpecRep era Network)
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep Network
n SpecTransM era () (Credential -> RewardAddress)
-> SpecTransM era () Credential -> SpecTransM era () RewardAddress
forall a b.
SpecTransM era () (a -> b)
-> SpecTransM era () a -> SpecTransM era () b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Credential Staking
-> SpecTransM
     era
     (SpecContext era (Credential Staking))
     (SpecRep era (Credential Staking))
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep Credential Staking
c

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

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

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

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

vkeyToInteger :: VKey kd -> Integer
vkeyToInteger :: forall (kd :: KeyRole). VKey kd -> Integer
vkeyToInteger = Natural -> Integer
forall a. Integral a => a -> Integer
toInteger (Natural -> Integer) -> (VKey kd -> Natural) -> VKey kd -> Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ByteString -> Natural
bytesToNatural (ByteString -> Natural)
-> (VKey kd -> ByteString) -> VKey kd -> Natural
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 -> Natural -> ByteString
naturalToBytes Int
32 (Natural -> ByteString)
-> (Integer -> Natural) -> Integer -> ByteString
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> Natural
forall a. Num a => Integer -> a
fromInteger

signatureToInteger :: DSIGNAlgorithm v => SigDSIGN v -> Integer
signatureToInteger :: forall v. DSIGNAlgorithm v => SigDSIGN v -> Integer
signatureToInteger = Natural -> Integer
forall a. Integral a => a -> Integer
toInteger (Natural -> Integer)
-> (SigDSIGN v -> Natural) -> SigDSIGN v -> Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ByteString -> Natural
bytesToNatural (ByteString -> Natural)
-> (SigDSIGN v -> ByteString) -> SigDSIGN v -> Natural
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 -> Natural -> ByteString
naturalToBytes Int
64 (Natural -> ByteString)
-> (Integer -> Natural) -> Integer -> ByteString
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> Natural
forall a. Num a => Integer -> a
fromInteger

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

  toSpecRep :: VKey k
-> SpecTransM era (SpecContext era (VKey k)) (SpecRep era (VKey k))
toSpecRep VKey k
x = do
    let hvkVKey :: Integer
hvkVKey = VKey k -> Integer
forall (kd :: KeyRole). VKey kd -> Integer
vkeyToInteger VKey k
x
    hvkStoredHash <- Hash ADDRHASH (VerKeyDSIGN DSIGN)
-> SpecTransM
     era
     (SpecContext era (Hash ADDRHASH (VerKeyDSIGN DSIGN)))
     (SpecRep era (Hash ADDRHASH (VerKeyDSIGN DSIGN)))
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era 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)
    pure Agda.MkHSVKey {..}

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

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

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

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

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

  toSpecRep :: CommitteeAuthorization
-> SpecTransM
     era
     (SpecContext era CommitteeAuthorization)
     (SpecRep era CommitteeAuthorization)
toSpecRep (CommitteeHotCredential Credential HotCommitteeRole
c) = Maybe (Credential HotCommitteeRole)
-> SpecTransM
     era
     (SpecContext era (Maybe (Credential HotCommitteeRole)))
     (SpecRep era (Maybe (Credential HotCommitteeRole)))
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep (Maybe (Credential HotCommitteeRole)
 -> SpecTransM
      era
      (SpecContext era (Maybe (Credential HotCommitteeRole)))
      (SpecRep era (Maybe (Credential HotCommitteeRole))))
-> Maybe (Credential HotCommitteeRole)
-> SpecTransM
     era
     (SpecContext era (Maybe (Credential HotCommitteeRole)))
     (SpecRep era (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
     era
     (SpecContext era (Maybe (Credential HotCommitteeRole)))
     (SpecRep era (Maybe (Credential HotCommitteeRole)))
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep (Maybe (Credential HotCommitteeRole)
 -> SpecTransM
      era
      (SpecContext era (Maybe (Credential HotCommitteeRole)))
      (SpecRep era (Maybe (Credential HotCommitteeRole))))
-> Maybe (Credential HotCommitteeRole)
-> SpecTransM
     era
     (SpecContext era (Maybe (Credential HotCommitteeRole)))
     (SpecRep era (Maybe (Credential HotCommitteeRole)))
forall a b. (a -> b) -> a -> b
$
      forall a. Maybe a
Nothing @(Credential HotCommitteeRole)

instance SpecTranslate era (CommitteeState era) where
  type
    SpecRep era (CommitteeState era) =
      Agda.HSMap (SpecRep era (Credential ColdCommitteeRole)) (SpecRep era CommitteeAuthorization)

  toSpecRep :: CommitteeState era
-> SpecTransM
     era
     (SpecContext era (CommitteeState era))
     (SpecRep era (CommitteeState era))
toSpecRep = Map (Credential ColdCommitteeRole) CommitteeAuthorization
-> SpecTransM era () (HSMap Credential (Maybe Credential))
Map (Credential ColdCommitteeRole) CommitteeAuthorization
-> SpecTransM
     era
     ()
     (HSMap
        (SpecRep era (Credential ColdCommitteeRole))
        (SpecRep era CommitteeAuthorization))
forall era k v ctx.
(SpecTranslate era k, SpecTranslate era v, SpecContext era k ~ ctx,
 SpecContext era v ~ ctx) =>
Map k v
-> SpecTransM era ctx (HSMap (SpecRep era k) (SpecRep era v))
toSpecRepMap (Map (Credential ColdCommitteeRole) CommitteeAuthorization
 -> SpecTransM era () (HSMap Credential (Maybe Credential)))
-> (CommitteeState era
    -> Map (Credential ColdCommitteeRole) CommitteeAuthorization)
-> CommitteeState era
-> SpecTransM era () (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

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 era IndividualPoolStake where
  type SpecRep era IndividualPoolStake = SpecRep era Coin

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

instance SpecTranslate era PoolDistr where
  type SpecRep era PoolDistr = Agda.HSMap (SpecRep era (KeyHash StakePool)) Agda.Coin

  toSpecRep :: PoolDistr
-> SpecTransM
     era (SpecContext era PoolDistr) (SpecRep era PoolDistr)
toSpecRep (PoolDistr Map (KeyHash StakePool) IndividualPoolStake
ps NonZero Coin
_) = Map (KeyHash StakePool) IndividualPoolStake
-> SpecTransM
     era
     ()
     (HSMap
        (SpecRep era (KeyHash StakePool))
        (SpecRep era IndividualPoolStake))
forall era k v ctx.
(SpecTranslate era k, SpecTranslate era v, SpecContext era k ~ ctx,
 SpecContext era v ~ ctx) =>
Map k v
-> SpecTransM era ctx (HSMap (SpecRep era k) (SpecRep era v))
toSpecRepMap Map (KeyHash StakePool) IndividualPoolStake
ps

instance SpecTranslate era BlocksMade where
  type SpecRep era BlocksMade = Agda.HSMap Integer Integer

  toSpecRep :: BlocksMade
-> SpecTransM
     era (SpecContext era BlocksMade) (SpecRep era BlocksMade)
toSpecRep (BlocksMade Map (KeyHash StakePool) Natural
m) = do
    xs <- [(KeyHash StakePool, Natural)]
-> ((KeyHash StakePool, Natural)
    -> SpecTransM era () (Integer, Integer))
-> SpecTransM era () [(Integer, Integer)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM (Map (KeyHash StakePool) Natural -> [(KeyHash StakePool, Natural)]
forall k a. Map k a -> [(k, a)]
Map.toList Map (KeyHash StakePool) Natural
m) (((KeyHash StakePool, Natural)
  -> SpecTransM era () (Integer, Integer))
 -> SpecTransM era () [(Integer, Integer)])
-> ((KeyHash StakePool, Natural)
    -> SpecTransM era () (Integer, Integer))
-> SpecTransM era () [(Integer, Integer)]
forall a b. (a -> b) -> a -> b
$ \(KeyHash StakePool
k, Natural
v) -> do
      k' <- KeyHash StakePool
-> SpecTransM
     era
     (SpecContext era (KeyHash StakePool))
     (SpecRep era (KeyHash StakePool))
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep KeyHash StakePool
k
      pure (k', naturalToInteger v)
    pure $ Agda.MkHSMap xs

instance SpecNormalize Agda.BaseAddr

instance SpecNormalize Agda.BootstrapAddr

instance SpecNormalize Agda.Credential

instance SpecNormalize Agda.RewardAddress